theory SimplRewrite

lemma exec_statefn_simulates_Call:
  "bij f \<Longrightarrow> exec_statefn_simulates f S T (Call c) (Call c)" apply (rule exec_statefn_simulatesI) apply (intro disjI1) apply (erule exec.cases, simp_all) apply (rule exec.intros, simp) apply (simp add: add_statefn_exec bij_imp_bij_inv option.map_comp o_def
                    inv_inv_eq) apply (simp add: add_statefn_comp
                    inj_iff[THEN iffD1, OF bij_is_inj] inv_inv_eq bij_imp_bij_inv
                    map_option_case inv_f_f[OF bij_is_inj] add_statefn_xstate_comp) apply (fastforce intro: exec.intros) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bij f \<Longrightarrow> exec_statefn_simulates f S T (Call c) (Call c) proof (prove)
goal (1 subgoal):
 1. \<And>s \<Gamma> t. \<lbrakk>bij f; s \<in> S; \<Gamma>\<turnstile> \<langle>Call c,Normal s\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Call c,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Call c,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Call c,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (1 subgoal):
 1. \<And>s \<Gamma> t. \<lbrakk>bij f; s \<in> S; \<Gamma>\<turnstile> \<langle>Call c,Normal s\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Call c,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t proof (prove)
goal (2 subgoals):
 1. \<And>s \<Gamma> t p bdy sa ta. \<lbrakk>bij f; sa \<in> S; c = p; s = sa; t = ta; \<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> ta\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Call p,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta
 2. \<And>s \<Gamma> t p sa. \<lbrakk>bij f; sa \<in> S; c = p; s = sa; t = Stuck; \<Gamma> p = None\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Call p,Normal (f sa)\<rangle> \<Rightarrow> Stuck proof (prove)
goal (2 subgoals):
 1. \<And>s \<Gamma> t p bdy sa ta. \<lbrakk>bij f; sa \<in> S; c = p; s = sa; t = ta; \<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> ta\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) bdy,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta
 2. \<And>s \<Gamma> t p sa. \<lbrakk>bij f; sa \<in> S; c = p; s = sa; t = Stuck; \<Gamma> p = None\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Call p,Normal (f sa)\<rangle> \<Rightarrow> Stuck proof (prove)
goal (2 subgoals):
 1. \<And>s \<Gamma> t p bdy sa ta. \<lbrakk>bij f; sa \<in> S; c = p; s = sa; t = ta; \<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> ta\<rbrakk> \<Longrightarrow> (\<lambda>x. map_option (\<lambda>x. add_statefn f (add_statefn (inv f) x)) (\<Gamma> x))\<turnstile> \<langle>bdy,Normal (inv f (f sa))\<rangle> \<Rightarrow> add_statefn_xstate (inv f) (add_statefn_xstate f ta)
 2. \<And>s \<Gamma> t p sa. \<lbrakk>bij f; sa \<in> S; c = p; s = sa; t = Stuck; \<Gamma> p = None\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Call p,Normal (f sa)\<rangle> \<Rightarrow> Stuck proof (prove)
goal (1 subgoal):
 1. \<And>s \<Gamma> t p sa. \<lbrakk>bij f; sa \<in> S; c = p; s = sa; t = Stuck; \<Gamma> p = None\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Call p,Normal (f sa)\<rangle> \<Rightarrow> Stuck proof (prove)
goal:
No subgoals!