theory SimplRewrite

lemma exec_statefn_simulates_DynCom:
  "\<lbrakk> \<And>s. s \<in> S \<Longrightarrow> exec_statefn_simulates f S T (g s) (h (f s)) \<rbrakk>
      \<Longrightarrow> exec_statefn_simulates f S T (DynCom g) (DynCom h)" apply atomize apply (clarsimp simp add: exec_statefn_simulates_def) apply (erule exec.cases, simp_all) apply (fastforce intro: exec.intros) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. s \<in> S \<Longrightarrow> exec_statefn_simulates f S T (g s) (h (f s))) \<Longrightarrow> exec_statefn_simulates f S T (DynCom g) (DynCom h) proof (prove)
goal (1 subgoal):
 1. \<forall>s. s \<in> S \<longrightarrow> exec_statefn_simulates f S T (g s) (h (f s)) \<Longrightarrow> exec_statefn_simulates f S T (DynCom g) (DynCom h) proof (prove)
goal (1 subgoal):
 1. \<And>s \<Gamma> t. \<lbrakk>\<forall>s. s \<in> S \<longrightarrow> (\<forall>sa\<in>S. \<forall>\<Gamma> t. \<Gamma>\<turnstile> \<langle>g s,Normal sa\<rangle> \<Rightarrow> t \<longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>h (f s),Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>h (f s),Normal (f sa)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>h (f s),Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'))); s \<in> S; \<Gamma>\<turnstile> \<langle>DynCom g,Normal s\<rangle> \<Rightarrow> t; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>DynCom h,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t; \<forall>t'\<in>- T. \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>DynCom h,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>DynCom h,Normal (f s)\<rangle> \<Rightarrow> Fault ft proof (prove)
goal (1 subgoal):
 1. \<And>s \<Gamma> t c sa ta. \<lbrakk>\<forall>s. s \<in> S \<longrightarrow> (\<forall>sa\<in>S. \<forall>\<Gamma> t. \<Gamma>\<turnstile> \<langle>c s,Normal sa\<rangle> \<Rightarrow> t \<longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>h (f s),Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>h (f s),Normal (f sa)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>h (f s),Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'))); sa \<in> S; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>DynCom h,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta; \<forall>t'\<in>- T. \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>DynCom h,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); g = c; s = sa; t = ta; \<Gamma>\<turnstile> \<langle>c sa,Normal sa\<rangle> \<Rightarrow> ta\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>DynCom h,Normal (f sa)\<rangle> \<Rightarrow> Fault ft proof (prove)
goal:
No subgoals!