theory Ctac

lemma simpl_final_basic_opts_exec[OF _ refl refl]:
  "\<Gamma> \<turnstile> \<langle>c, xs\<rangle> \<Rightarrow> xs' \<Longrightarrow> xs = Normal t \<Longrightarrow> xs' = Normal t'
    \<Longrightarrow> (case simpl_final_basic_opts c of None \<Rightarrow> t' = t
            | Some f \<Rightarrow> \<exists>s. t' = f s)" apply (induct arbitrary: t t' rule: exec.induct, simp_all) apply metis apply atomize apply clarsimp apply (case_tac s') apply (auto split: option.split_asm)[1] apply (auto elim!: exec_elim_cases) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,xs\<rangle> \<Rightarrow> xs'; xs = Normal t; xs' = Normal t'\<rbrakk> \<Longrightarrow> case simpl_final_basic_opts c of None \<Rightarrow> t' = t | Some f \<Rightarrow> \<exists>s. t' = f s proof (prove)
goal (2 subgoals):
 1. \<And>f s t t'. \<lbrakk>s = t; f t = t'\<rbrakk> \<Longrightarrow> \<exists>s. t' = f s
 2. \<And>c\<^sub>1 s s' c\<^sub>2 t ta t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal ta\<rangle> \<Rightarrow> s'; \<And>t t'. \<lbrakk>ta = t; s' = Normal t'\<rbrakk> \<Longrightarrow> case simpl_final_basic_opts c\<^sub>1 of None \<Rightarrow> t' = t | Some f \<Rightarrow> \<exists>s. t' = f s; \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> Normal t'; \<And>t t'a. \<lbrakk>s' = Normal t; t' = t'a\<rbrakk> \<Longrightarrow> case simpl_final_basic_opts c\<^sub>2 of None \<Rightarrow> t'a = t | Some f \<Rightarrow> \<exists>s. t'a = f s; s = ta; t = Normal t'\<rbrakk> \<Longrightarrow> case case simpl_final_basic_opts c\<^sub>2 of None \<Rightarrow> simpl_final_basic_opts c\<^sub>1 | Some x \<Rightarrow> Some x of None \<Rightarrow> t' = ta | Some f \<Rightarrow> \<exists>s. t' = f s proof (prove)
goal (1 subgoal):
 1. \<And>c\<^sub>1 s s' c\<^sub>2 t ta t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal ta\<rangle> \<Rightarrow> s'; \<And>t t'. \<lbrakk>ta = t; s' = Normal t'\<rbrakk> \<Longrightarrow> case simpl_final_basic_opts c\<^sub>1 of None \<Rightarrow> t' = t | Some f \<Rightarrow> \<exists>s. t' = f s; \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> Normal t'; \<And>t t'a. \<lbrakk>s' = Normal t; t' = t'a\<rbrakk> \<Longrightarrow> case simpl_final_basic_opts c\<^sub>2 of None \<Rightarrow> t'a = t | Some f \<Rightarrow> \<exists>s. t'a = f s; s = ta; t = Normal t'\<rbrakk> \<Longrightarrow> case case simpl_final_basic_opts c\<^sub>2 of None \<Rightarrow> simpl_final_basic_opts c\<^sub>1 | Some x \<Rightarrow> Some x of None \<Rightarrow> t' = ta | Some f \<Rightarrow> \<exists>s. t' = f s proof (prove)
goal (1 subgoal):
 1. \<And>c\<^sub>1 s s' c\<^sub>2 t ta t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal ta\<rangle> \<Rightarrow> s'; \<forall>t t'. ta = t \<longrightarrow> s' = Normal t' \<longrightarrow> (case simpl_final_basic_opts c\<^sub>1 of None \<Rightarrow> t' = t | Some f \<Rightarrow> \<exists>s. t' = f s); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> Normal t'; \<forall>t t'a. s' = Normal t \<longrightarrow> t' = t'a \<longrightarrow> (case simpl_final_basic_opts c\<^sub>2 of None \<Rightarrow> t'a = t | Some f \<Rightarrow> \<exists>s. t'a = f s); s = ta; t = Normal t'\<rbrakk> \<Longrightarrow> case case simpl_final_basic_opts c\<^sub>2 of None \<Rightarrow> simpl_final_basic_opts c\<^sub>1 | Some x \<Rightarrow> Some x of None \<Rightarrow> t' = ta | Some f \<Rightarrow> \<exists>s. t' = f s proof (prove)
goal (1 subgoal):
 1. \<And>c\<^sub>1 s' c\<^sub>2 ta t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal ta\<rangle> \<Rightarrow> s'; \<forall>t'. s' = Normal t' \<longrightarrow> (case simpl_final_basic_opts c\<^sub>1 of None \<Rightarrow> t' = ta | Some f \<Rightarrow> \<exists>s. t' = f s); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> Normal t'; \<forall>t. s' = Normal t \<longrightarrow> (case simpl_final_basic_opts c\<^sub>2 of None \<Rightarrow> t' = t | Some f \<Rightarrow> \<exists>s. t' = f s)\<rbrakk> \<Longrightarrow> case case simpl_final_basic_opts c\<^sub>2 of None \<Rightarrow> simpl_final_basic_opts c\<^sub>1 | Some x \<Rightarrow> Some x of None \<Rightarrow> t' = ta | Some f \<Rightarrow> \<exists>s. t' = f s proof (prove)
goal (4 subgoals):
 1. \<And>c\<^sub>1 s' c\<^sub>2 ta t' x1. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal ta\<rangle> \<Rightarrow> s'; \<forall>t'. s' = Normal t' \<longrightarrow> (case simpl_final_basic_opts c\<^sub>1 of None \<Rightarrow> t' = ta | Some f \<Rightarrow> \<exists>s. t' = f s); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> Normal t'; \<forall>t. s' = Normal t \<longrightarrow> (case simpl_final_basic_opts c\<^sub>2 of None \<Rightarrow> t' = t | Some f \<Rightarrow> \<exists>s. t' = f s); s' = Normal x1\<rbrakk> \<Longrightarrow> case case simpl_final_basic_opts c\<^sub>2 of None \<Rightarrow> simpl_final_basic_opts c\<^sub>1 | Some x \<Rightarrow> Some x of None \<Rightarrow> t' = ta | Some f \<Rightarrow> \<exists>s. t' = f s
 2. \<And>c\<^sub>1 s' c\<^sub>2 ta t' x2. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal ta\<rangle> \<Rightarrow> s'; \<forall>t'. s' = Normal t' \<longrightarrow> (case simpl_final_basic_opts c\<^sub>1 of None \<Rightarrow> t' = ta | Some f \<Rightarrow> \<exists>s. t' = f s); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> Normal t'; \<forall>t. s' = Normal t \<longrightarrow> (case simpl_final_basic_opts c\<^sub>2 of None \<Rightarrow> t' = t | Some f \<Rightarrow> \<exists>s. t' = f s); s' = Abrupt x2\<rbrakk> \<Longrightarrow> case case simpl_final_basic_opts c\<^sub>2 of None \<Rightarrow> simpl_final_basic_opts c\<^sub>1 | Some x \<Rightarrow> Some x of None \<Rightarrow> t' = ta | Some f \<Rightarrow> \<exists>s. t' = f s
 3. \<And>c\<^sub>1 s' c\<^sub>2 ta t' x3. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal ta\<rangle> \<Rightarrow> s'; \<forall>t'. s' = Normal t' \<longrightarrow> (case simpl_final_basic_opts c\<^sub>1 of None \<Rightarrow> t' = ta | Some f \<Rightarrow> \<exists>s. t' = f s); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> Normal t'; \<forall>t. s' = Normal t \<longrightarrow> (case simpl_final_basic_opts c\<^sub>2 of None \<Rightarrow> t' = t | Some f \<Rightarrow> \<exists>s. t' = f s); s' = Fault x3\<rbrakk> \<Longrightarrow> case case simpl_final_basic_opts c\<^sub>2 of None \<Rightarrow> simpl_final_basic_opts c\<^sub>1 | Some x \<Rightarrow> Some x of None \<Rightarrow> t' = ta | Some f \<Rightarrow> \<exists>s. t' = f s
 4. \<And>c\<^sub>1 s' c\<^sub>2 ta t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal ta\<rangle> \<Rightarrow> s'; \<forall>t'. s' = Normal t' \<longrightarrow> (case simpl_final_basic_opts c\<^sub>1 of None \<Rightarrow> t' = ta | Some f \<Rightarrow> \<exists>s. t' = f s); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> Normal t'; \<forall>t. s' = Normal t \<longrightarrow> (case simpl_final_basic_opts c\<^sub>2 of None \<Rightarrow> t' = t | Some f \<Rightarrow> \<exists>s. t' = f s); s' = Stuck\<rbrakk> \<Longrightarrow> case case simpl_final_basic_opts c\<^sub>2 of None \<Rightarrow> simpl_final_basic_opts c\<^sub>1 | Some x \<Rightarrow> Some x of None \<Rightarrow> t' = ta | Some f \<Rightarrow> \<exists>s. t' = f s proof (prove)
goal (3 subgoals):
 1. \<And>c\<^sub>1 s' c\<^sub>2 ta t' x2. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal ta\<rangle> \<Rightarrow> s'; \<forall>t'. s' = Normal t' \<longrightarrow> (case simpl_final_basic_opts c\<^sub>1 of None \<Rightarrow> t' = ta | Some f \<Rightarrow> \<exists>s. t' = f s); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> Normal t'; \<forall>t. s' = Normal t \<longrightarrow> (case simpl_final_basic_opts c\<^sub>2 of None \<Rightarrow> t' = t | Some f \<Rightarrow> \<exists>s. t' = f s); s' = Abrupt x2\<rbrakk> \<Longrightarrow> case case simpl_final_basic_opts c\<^sub>2 of None \<Rightarrow> simpl_final_basic_opts c\<^sub>1 | Some x \<Rightarrow> Some x of None \<Rightarrow> t' = ta | Some f \<Rightarrow> \<exists>s. t' = f s
 2. \<And>c\<^sub>1 s' c\<^sub>2 ta t' x3. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal ta\<rangle> \<Rightarrow> s'; \<forall>t'. s' = Normal t' \<longrightarrow> (case simpl_final_basic_opts c\<^sub>1 of None \<Rightarrow> t' = ta | Some f \<Rightarrow> \<exists>s. t' = f s); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> Normal t'; \<forall>t. s' = Normal t \<longrightarrow> (case simpl_final_basic_opts c\<^sub>2 of None \<Rightarrow> t' = t | Some f \<Rightarrow> \<exists>s. t' = f s); s' = Fault x3\<rbrakk> \<Longrightarrow> case case simpl_final_basic_opts c\<^sub>2 of None \<Rightarrow> simpl_final_basic_opts c\<^sub>1 | Some x \<Rightarrow> Some x of None \<Rightarrow> t' = ta | Some f \<Rightarrow> \<exists>s. t' = f s
 3. \<And>c\<^sub>1 s' c\<^sub>2 ta t'. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal ta\<rangle> \<Rightarrow> s'; \<forall>t'. s' = Normal t' \<longrightarrow> (case simpl_final_basic_opts c\<^sub>1 of None \<Rightarrow> t' = ta | Some f \<Rightarrow> \<exists>s. t' = f s); \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> Normal t'; \<forall>t. s' = Normal t \<longrightarrow> (case simpl_final_basic_opts c\<^sub>2 of None \<Rightarrow> t' = t | Some f \<Rightarrow> \<exists>s. t' = f s); s' = Stuck\<rbrakk> \<Longrightarrow> case case simpl_final_basic_opts c\<^sub>2 of None \<Rightarrow> simpl_final_basic_opts c\<^sub>1 | Some x \<Rightarrow> Some x of None \<Rightarrow> t' = ta | Some f \<Rightarrow> \<exists>s. t' = f s proof (prove)
goal:
No subgoals!