theory SimplRewrite

lemma exec_statefn_simulates_Spec:
  "\<lbrakk> bij f; \<And>s. \<lbrakk> s \<in> S; \<forall>t. (f s, f t) \<in> R' \<longrightarrow> t \<in> T \<rbrakk>
            \<Longrightarrow> \<forall>t. ((s, t) \<in> R) = ((f s, f t) \<in> R') \<rbrakk>
      \<Longrightarrow> exec_statefn_simulates f S T (Spec R) (Spec R')" apply (rule exec_statefn_simulatesI) apply (erule exec_Normal_elim_cases, simp_all) apply (blast intro: exec.Spec) apply (case_tac "\<forall>t. (f s, f t) \<in> R' \<longrightarrow> t \<in> T") apply clarsimp apply (subgoal_tac "\<forall>t. (f s, f (inv f t)) \<notin> R'") apply (simp add: surj_f_inv_f bij_is_surj) apply (blast intro: exec.SpecStuck) apply clarsimp apply (blast intro: exec.Spec) done

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