theory SimplRewrite

lemma exec_statefn_simulates_additional_Guards:
  "exec_statefn_simulates f S T a (b ;; Guard F (G \<inter> G') c)
        \<Longrightarrow> exec_statefn_simulates f S T a (b ;; Guard F G (Guard F' G' c))" apply (rule exec_statefn_simulatesI) apply (drule(2) exec_statefn_simulatesD) apply (elim disjE exE) apply (erule exec_Normal_elim_cases) apply (case_tac s', auto elim!: exec_Normal_elim_cases,
           (blast intro: exec.Seq exec.Guard exec.GuardFault)+)[1] apply (erule exec_Normal_elim_cases) apply (case_tac s', auto elim!: exec_Normal_elim_cases,
          (blast intro: exec.Seq exec.Guard exec.GuardFault)+)[1] apply (clarsimp elim!: exec_Normal_elim_cases) apply (case_tac s', auto elim!: exec_Normal_elim_cases,
         (blast intro: exec.Seq exec.Guard exec.GuardFault)+)[1] done

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