theory SimplRewrite

lemma exec_statefn_simulates_Guard_lhs:
  "\<lbrakk> S \<subseteq> G; exec_statefn_simulates f S T a b \<rbrakk>
     \<Longrightarrow> exec_statefn_simulates f S T (Guard E G a) b" apply (rule exec_statefn_simulatesI) apply (erule exec.cases, simp_all) apply (drule(1) exec_statefn_simulatesD, simp) apply (auto intro: exec.intros) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S \<subseteq> G; exec_statefn_simulates f S T a b\<rbrakk> \<Longrightarrow> exec_statefn_simulates f S T (Guard E G a) b proof (prove)
goal (1 subgoal):
 1. \<And>s \<Gamma> t. \<lbrakk>S \<subseteq> G; exec_statefn_simulates f S T a b; s \<in> S; \<Gamma>\<turnstile> \<langle>Guard E G a,Normal s\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (2 subgoals):
 1. \<And>s \<Gamma> t sa g ta. \<lbrakk>S \<subseteq> g; exec_statefn_simulates f S T a b; sa \<in> S; G = g; s = sa; t = ta; sa \<in> g; \<Gamma>\<turnstile> \<langle>a,Normal sa\<rangle> \<Rightarrow> ta\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta \<or> (\<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'))
 2. \<And>s \<Gamma> t sa g. \<lbrakk>S \<subseteq> g; exec_statefn_simulates f S T a b; sa \<in> S; G = g; s = sa; t = Fault E; sa \<notin> g\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Fault E \<or> (\<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (2 subgoals):
 1. \<And>s \<Gamma> t sa g ta. \<lbrakk>S \<subseteq> g; exec_statefn_simulates f S T a b; sa \<in> S; G = g; s = sa; t = ta; sa \<in> g; (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta \<or> (\<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'))\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta \<or> (\<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'))
 2. \<And>s \<Gamma> t sa g. \<lbrakk>S \<subseteq> g; exec_statefn_simulates f S T a b; sa \<in> S; G = g; s = sa; t = Fault E; sa \<notin> g\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Fault E \<or> (\<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal:
No subgoals!