theory SimplRewrite

lemma exec_statefn_simulates_While:
  assumes bij: "bij f" shows
  "\<lbrakk> \<And>s. \<lbrakk> s \<in> S \<or> f s \<in> com_final_guards UNIV b;
            f s \<in> com_initial_guards b \<or> s \<in> T \<rbrakk>
            \<Longrightarrow> s \<in> C = (f s \<in> C');
       exec_statefn_simulates f C {s. (s \<in> S \<or> f s \<in> com_final_guards UNIV b)
            \<and> (f s \<in> com_initial_guards b \<or> s \<in> T)} a b \<rbrakk>
        \<Longrightarrow> exec_statefn_simulates f S T (While C a) (While C' b)" apply (rule exec_statefn_simulatesI) apply (rule_tac S="f ` S \<union> com_final_guards UNIV b"
           in exec_statefn_simulates_While_lemma[rule_format]) apply (auto simp add: inj_image_mem_iff[OF bij_is_inj, OF bij]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. \<lbrakk>s \<in> S \<or> f s \<in> com_final_guards UNIV b; f s \<in> com_initial_guards b \<or> s \<in> T\<rbrakk> \<Longrightarrow> (s \<in> C) = (f s \<in> C'); exec_statefn_simulates f C {s. (s \<in> S \<or> f s \<in> com_final_guards UNIV b) \<and> (f s \<in> com_initial_guards b \<or> s \<in> T)} a b\<rbrakk> \<Longrightarrow> exec_statefn_simulates f S T (While C a) (While C' b) proof (prove)
goal (1 subgoal):
 1. \<And>s \<Gamma> t. \<lbrakk>\<And>s. \<lbrakk>s \<in> S \<or> f s \<in> com_final_guards UNIV b; f s \<in> com_initial_guards b \<or> s \<in> T\<rbrakk> \<Longrightarrow> (s \<in> C) = (f s \<in> C'); exec_statefn_simulates f C {s. (s \<in> S \<or> f s \<in> com_final_guards UNIV b) \<and> (f s \<in> com_initial_guards b \<or> s \<in> T)} a b; s \<in> S; \<Gamma>\<turnstile> \<langle>While C a,Normal s\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>While C' b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (5 subgoals):
 1. \<And>s \<Gamma> t. \<lbrakk>\<And>s. \<lbrakk>s \<in> S \<or> f s \<in> com_final_guards UNIV b; f s \<in> com_initial_guards b \<or> s \<in> T\<rbrakk> \<Longrightarrow> (s \<in> C) = (f s \<in> C'); exec_statefn_simulates f C {s. (s \<in> S \<or> f s \<in> com_final_guards UNIV b) \<and> (f s \<in> com_initial_guards b \<or> s \<in> T)} a b; s \<in> S; \<Gamma>\<turnstile> \<langle>While C a,Normal s\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> exec_statefn_simulates f (?C2 s \<Gamma> t) {s. f s \<in> f ` S \<union> com_final_guards UNIV b \<and> (f s \<in> com_initial_guards b \<or> f s \<notin> f ` (- T))} (?a2 s \<Gamma> t) b
 2. \<And>s \<Gamma> t sa. \<lbrakk>\<And>s. \<lbrakk>s \<in> S \<or> f s \<in> com_final_guards UNIV b; f s \<in> com_initial_guards b \<or> s \<in> T\<rbrakk> \<Longrightarrow> (s \<in> C) = (f s \<in> C'); exec_statefn_simulates f C {s. (s \<in> S \<or> f s \<in> com_final_guards UNIV b) \<and> (f s \<in> com_initial_guards b \<or> s \<in> T)} a b; s \<in> S; \<Gamma>\<turnstile> \<langle>While C a,Normal s\<rangle> \<Rightarrow> t; f sa \<in> f ` S \<union> com_final_guards UNIV b; f sa \<in> com_initial_guards b \<or> f sa \<notin> f ` (- T)\<rbrakk> \<Longrightarrow> (sa \<in> ?C2 s \<Gamma> t) = (f sa \<in> C')
 3. \<And>s \<Gamma> t. \<lbrakk>\<And>s. \<lbrakk>s \<in> S \<or> f s \<in> com_final_guards UNIV b; f s \<in> com_initial_guards b \<or> s \<in> T\<rbrakk> \<Longrightarrow> (s \<in> C) = (f s \<in> C'); exec_statefn_simulates f C {s. (s \<in> S \<or> f s \<in> com_final_guards UNIV b) \<and> (f s \<in> com_initial_guards b \<or> s \<in> T)} a b; s \<in> S; \<Gamma>\<turnstile> \<langle>While C a,Normal s\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> com_final_guards UNIV b \<subseteq> f ` S \<union> com_final_guards UNIV b
 4. \<And>s \<Gamma> t. \<lbrakk>\<And>s. \<lbrakk>s \<in> S \<or> f s \<in> com_final_guards UNIV b; f s \<in> com_initial_guards b \<or> s \<in> T\<rbrakk> \<Longrightarrow> (s \<in> C) = (f s \<in> C'); exec_statefn_simulates f C {s. (s \<in> S \<or> f s \<in> com_final_guards UNIV b) \<and> (f s \<in> com_initial_guards b \<or> s \<in> T)} a b; s \<in> S; \<Gamma>\<turnstile> \<langle>While C a,Normal s\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>?bdy2 s \<Gamma> t,?xs2 s \<Gamma> t\<rangle> \<Rightarrow> t
 5. \<And>s \<Gamma> t. \<lbrakk>\<And>s. \<lbrakk>s \<in> S \<or> f s \<in> com_final_guards UNIV b; f s \<in> com_initial_guards b \<or> s \<in> T\<rbrakk> \<Longrightarrow> (s \<in> C) = (f s \<in> C'); exec_statefn_simulates f C {s. (s \<in> S \<or> f s \<in> com_final_guards UNIV b) \<and> (f s \<in> com_initial_guards b \<or> s \<in> T)} a b; s \<in> S; \<Gamma>\<turnstile> \<langle>While C a,Normal s\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> ?bdy2 s \<Gamma> t = While (?C2 s \<Gamma> t) (?a2 s \<Gamma> t) \<and> ?xs2 s \<Gamma> t = Normal s \<and> f s \<in> f ` S \<union> com_final_guards UNIV b proof (prove)
goal:
No subgoals!