theory SimplRewrite

lemma exec_statefn_simulates_Cond:
  "\<lbrakk> \<And>s. s \<in> S \<Longrightarrow> (s \<in> C) = (f s \<in> C'); exec_statefn_simulates f (S \<inter> C) T a b;
            exec_statefn_simulates f (S \<inter> - C) T c d \<rbrakk>
        \<Longrightarrow> exec_statefn_simulates f S T (Cond C a c) (Cond C' b d)" apply atomize apply (rule exec_statefn_simulatesI) apply (erule exec.cases, simp_all) apply clarsimp apply (drule spec, drule(1) mp, simp) apply (drule(1) exec_statefn_simulatesD, simp) apply (auto intro: exec.CondTrue)[1] apply clarsimp apply (drule spec, drule(1) mp, simp) apply (drule(1) exec_statefn_simulatesD, simp) apply (auto intro: exec.CondFalse)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. s \<in> S \<Longrightarrow> (s \<in> C) = (f s \<in> C'); exec_statefn_simulates f (S \<inter> C) T a b; exec_statefn_simulates f (S \<inter> - C) T c d\<rbrakk> \<Longrightarrow> exec_statefn_simulates f S T (Cond C a c) (Cond C' b d) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. s \<in> S \<longrightarrow> (s \<in> C) = (f s \<in> C'); exec_statefn_simulates f (S \<inter> C) T a b; exec_statefn_simulates f (S \<inter> - C) T c d\<rbrakk> \<Longrightarrow> exec_statefn_simulates f S T (Cond C a c) (Cond C' b d) proof (prove)
goal (1 subgoal):
 1. \<And>s \<Gamma> t. \<lbrakk>\<forall>s. s \<in> S \<longrightarrow> (s \<in> C) = (f s \<in> C'); exec_statefn_simulates f (S \<inter> C) T a b; exec_statefn_simulates f (S \<inter> - C) T c d; s \<in> S; \<Gamma>\<turnstile> \<langle>Cond C a c,Normal s\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (2 subgoals):
 1. \<And>s \<Gamma> t sa ba ta. \<lbrakk>\<forall>s. s \<in> S \<longrightarrow> (s \<in> ba) = (f s \<in> C'); exec_statefn_simulates f (S \<inter> ba) T a b; exec_statefn_simulates f (S \<inter> - ba) T c d; sa \<in> S; C = ba; s = sa; t = ta; f sa \<in> C'; \<Gamma>\<turnstile> \<langle>a,Normal sa\<rangle> \<Rightarrow> ta\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta \<or> (\<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'))
 2. \<And>s \<Gamma> t sa ba ta. \<lbrakk>\<forall>s. s \<in> S \<longrightarrow> (s \<in> ba) = (f s \<in> C'); exec_statefn_simulates f (S \<inter> ba) T a b; exec_statefn_simulates f (S \<inter> - ba) T c d; sa \<in> S; C = ba; s = sa; t = ta; f sa \<notin> C'; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> ta\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta \<or> (\<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (2 subgoals):
 1. \<And>\<Gamma> sa ta. \<lbrakk>\<forall>s. s \<in> S \<longrightarrow> (s \<in> C) = (f s \<in> C'); exec_statefn_simulates f (S \<inter> C) T a b; exec_statefn_simulates f (S \<inter> - C) T c d; sa \<in> S; f sa \<in> C'; \<Gamma>\<turnstile> \<langle>a,Normal sa\<rangle> \<Rightarrow> ta; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,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>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t')\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft
 2. \<And>s \<Gamma> t sa ba ta. \<lbrakk>\<forall>s. s \<in> S \<longrightarrow> (s \<in> ba) = (f s \<in> C'); exec_statefn_simulates f (S \<inter> ba) T a b; exec_statefn_simulates f (S \<inter> - ba) T c d; sa \<in> S; C = ba; s = sa; t = ta; f sa \<notin> C'; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> ta\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta \<or> (\<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (2 subgoals):
 1. \<And>\<Gamma> sa ta. \<lbrakk>exec_statefn_simulates f (S \<inter> C) T a b; exec_statefn_simulates f (S \<inter> - C) T c d; sa \<in> S; f sa \<in> C'; \<Gamma>\<turnstile> \<langle>a,Normal sa\<rangle> \<Rightarrow> ta; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,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>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); sa \<in> C\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft
 2. \<And>s \<Gamma> t sa ba ta. \<lbrakk>\<forall>s. s \<in> S \<longrightarrow> (s \<in> ba) = (f s \<in> C'); exec_statefn_simulates f (S \<inter> ba) T a b; exec_statefn_simulates f (S \<inter> - ba) T c d; sa \<in> S; C = ba; s = sa; t = ta; f sa \<notin> C'; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> ta\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta \<or> (\<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (2 subgoals):
 1. \<And>\<Gamma> sa ta. \<lbrakk>exec_statefn_simulates f (S \<inter> C) T a b; exec_statefn_simulates f (S \<inter> - C) T c d; sa \<in> S; f sa \<in> C'; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,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>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); sa \<in> C; (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> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft
 2. \<And>s \<Gamma> t sa ba ta. \<lbrakk>\<forall>s. s \<in> S \<longrightarrow> (s \<in> ba) = (f s \<in> C'); exec_statefn_simulates f (S \<inter> ba) T a b; exec_statefn_simulates f (S \<inter> - ba) T c d; sa \<in> S; C = ba; s = sa; t = ta; f sa \<notin> C'; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> ta\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta \<or> (\<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (1 subgoal):
 1. \<And>s \<Gamma> t sa ba ta. \<lbrakk>\<forall>s. s \<in> S \<longrightarrow> (s \<in> ba) = (f s \<in> C'); exec_statefn_simulates f (S \<inter> ba) T a b; exec_statefn_simulates f (S \<inter> - ba) T c d; sa \<in> S; C = ba; s = sa; t = ta; f sa \<notin> C'; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> ta\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta \<or> (\<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (1 subgoal):
 1. \<And>\<Gamma> sa ta. \<lbrakk>\<forall>s. s \<in> S \<longrightarrow> (s \<in> C) = (f s \<in> C'); exec_statefn_simulates f (S \<inter> C) T a b; exec_statefn_simulates f (S \<inter> - C) T c d; sa \<in> S; f sa \<notin> C'; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> ta; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,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>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t')\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft proof (prove)
goal (1 subgoal):
 1. \<And>\<Gamma> sa ta. \<lbrakk>exec_statefn_simulates f (S \<inter> C) T a b; exec_statefn_simulates f (S \<inter> - C) T c d; sa \<in> S; f sa \<notin> C'; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> ta; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,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>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); sa \<notin> C\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft proof (prove)
goal (1 subgoal):
 1. \<And>\<Gamma> sa ta. \<lbrakk>exec_statefn_simulates f (S \<inter> C) T a b; exec_statefn_simulates f (S \<inter> - C) T c d; sa \<in> S; f sa \<notin> C'; \<not> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,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>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'); sa \<notin> C; (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>d,Normal (f sa)\<rangle> \<Rightarrow> add_statefn_xstate f ta \<or> (\<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>d,Normal (f sa)\<rangle> \<Rightarrow> Normal (f t'))\<rbrakk> \<Longrightarrow> \<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>Cond C' b d,Normal (f sa)\<rangle> \<Rightarrow> Fault ft proof (prove)
goal:
No subgoals!