theory SimplRewrite

lemma exec_statefn_simulates_Basic:
  "\<lbrakk> \<And>s. \<lbrakk> s \<in> S; g (fn s) \<notin> fn ` (- T) \<rbrakk> \<Longrightarrow> fn (f s) = g (fn s) \<rbrakk>
      \<Longrightarrow> exec_statefn_simulates fn S T (Basic f) (Basic g)" apply atomize apply (rule exec_statefn_simulatesI) apply (erule exec.cases, simp_all, clarsimp) apply (drule spec, drule(1) mp) apply (drule mp) apply clarsimp apply (metis exec.Basic Compl_iff) apply clarsimp apply (blast intro: exec.Basic) done

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