theory SimplRewrite

lemma add_statefn_exec1:
  assumes bij: "bij f"
  shows "\<Gamma> \<turnstile> \<langle>c, xs\<rangle> \<Rightarrow> t
        \<Longrightarrow> (map_option (add_statefn (inv f)) o \<Gamma>) \<turnstile> \<langle>add_statefn (inv f) c,
                 add_statefn_xstate f xs\<rangle> \<Rightarrow> add_statefn_xstate f t" proof (induct rule: exec.induct) case Basic show ?case apply simp apply (rule_tac P="exec G c xs" for G c xs in subst[rotated], rule exec.Basic) apply (simp add: inv_inv_eq bij inv_f_f bij_is_inj) done qed (auto intro: exec.intros simp: inv_f_f[OF bij_is_inj, OF bij]
       surj_f_inv_f[OF bij_is_surj, OF bij])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>c,xs\<rangle> \<Rightarrow> t \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) c,add_statefn_xstate f xs\<rangle> \<Rightarrow> add_statefn_xstate f t proof (state)
goal (20 subgoals):
 1. \<And>s. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) SKIP,add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f (Normal s)
 2. \<And>s g c t fa. \<lbrakk>s \<in> g; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) c,add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f t\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) (Guard fa g c),add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f t
 3. \<And>s g fa c. s \<notin> g \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) (Guard fa g c),add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f (Fault fa)
 4. \<And>c fa. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) c,add_statefn_xstate f (Fault fa)\<rangle> \<Rightarrow> add_statefn_xstate f (Fault fa)
 5. \<And>fa s. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) (Basic fa),add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f (Normal (fa s))
 6. \<And>s t r. (s, t) \<in> r \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) (Spec r),add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f (Normal t)
 7. \<And>s r. \<forall>t. (s, t) \<notin> r \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) (Spec r),add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f Stuck
 8. \<And>c\<^sub>1 s s' c\<^sub>2 t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) c\<^sub>1,add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f s'; \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) c\<^sub>2,add_statefn_xstate f s'\<rangle> \<Rightarrow> add_statefn_xstate f t\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) (c\<^sub>1;;
c\<^sub>2),add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f t
 9. \<And>s b c\<^sub>1 t c\<^sub>2. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) c\<^sub>1,add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f t\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) (Cond b c\<^sub>1 c\<^sub>2),add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f t
 10. \<And>s b c\<^sub>2 t c\<^sub>1. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) c\<^sub>2,add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f t\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) (Cond b c\<^sub>1 c\<^sub>2),add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f t
A total of 20 subgoals... proof (state)
this:


goal (20 subgoals):
 1. \<And>s. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) SKIP,add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f (Normal s)
 2. \<And>s g c t fa. \<lbrakk>s \<in> g; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) c,add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f t\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) (Guard fa g c),add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f t
 3. \<And>s g fa c. s \<notin> g \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) (Guard fa g c),add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f (Fault fa)
 4. \<And>c fa. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) c,add_statefn_xstate f (Fault fa)\<rangle> \<Rightarrow> add_statefn_xstate f (Fault fa)
 5. \<And>fa s. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) (Basic fa),add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f (Normal (fa s))
 6. \<And>s t r. (s, t) \<in> r \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) (Spec r),add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f (Normal t)
 7. \<And>s r. \<forall>t. (s, t) \<notin> r \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) (Spec r),add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f Stuck
 8. \<And>c\<^sub>1 s s' c\<^sub>2 t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) c\<^sub>1,add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f s'; \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) c\<^sub>2,add_statefn_xstate f s'\<rangle> \<Rightarrow> add_statefn_xstate f t\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) (c\<^sub>1;;
c\<^sub>2),add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f t
 9. \<And>s b c\<^sub>1 t c\<^sub>2. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) c\<^sub>1,add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f t\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) (Cond b c\<^sub>1 c\<^sub>2),add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f t
 10. \<And>s b c\<^sub>2 t c\<^sub>1. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) c\<^sub>2,add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f t\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) (Cond b c\<^sub>1 c\<^sub>2),add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f t
A total of 20 subgoals... proof (prove)
goal (1 subgoal):
 1. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) (Basic f_),add_statefn_xstate f (Normal s_)\<rangle> \<Rightarrow> add_statefn_xstate f (Normal (f_ s_)) proof (prove)
goal (1 subgoal):
 1. (\<lambda>a. map_option (add_statefn (inv f)) (\<Gamma> a))\<turnstile> \<langle>Basic (\<lambda>s. inv (inv f) (f_ (inv f s))),Normal (f s_)\<rangle> \<Rightarrow> Normal (f (f_ s_)) proof (prove)
goal (1 subgoal):
 1. Normal (inv (inv f) (f_ (inv f (f s_)))) = Normal (f (f_ s_)) proof (prove)
goal:
No subgoals! proof (state)
this:
(map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) (Basic f_),add_statefn_xstate f (Normal s_)\<rangle> \<Rightarrow> add_statefn_xstate f (Normal (f_ s_))

goal (19 subgoals):
 1. \<And>s. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) SKIP,add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f (Normal s)
 2. \<And>s g c t fa. \<lbrakk>s \<in> g; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) c,add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f t\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) (Guard fa g c),add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f t
 3. \<And>s g fa c. s \<notin> g \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) (Guard fa g c),add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f (Fault fa)
 4. \<And>c fa. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) c,add_statefn_xstate f (Fault fa)\<rangle> \<Rightarrow> add_statefn_xstate f (Fault fa)
 5. \<And>s t r. (s, t) \<in> r \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) (Spec r),add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f (Normal t)
 6. \<And>s r. \<forall>t. (s, t) \<notin> r \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) (Spec r),add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f Stuck
 7. \<And>c\<^sub>1 s s' c\<^sub>2 t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) c\<^sub>1,add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f s'; \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) c\<^sub>2,add_statefn_xstate f s'\<rangle> \<Rightarrow> add_statefn_xstate f t\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) (c\<^sub>1;;
c\<^sub>2),add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f t
 8. \<And>s b c\<^sub>1 t c\<^sub>2. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) c\<^sub>1,add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f t\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) (Cond b c\<^sub>1 c\<^sub>2),add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f t
 9. \<And>s b c\<^sub>2 t c\<^sub>1. \<lbrakk>s \<notin> b; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) c\<^sub>2,add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f t\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) (Cond b c\<^sub>1 c\<^sub>2),add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f t
 10. \<And>s b c s' t. \<lbrakk>s \<in> b; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> s'; (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) c,add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f s'; \<Gamma>\<turnstile> \<langle>While b c,s'\<rangle> \<Rightarrow> t; (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) (While b c),add_statefn_xstate f s'\<rangle> \<Rightarrow> add_statefn_xstate f t\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>add_statefn (inv f) (While b c),add_statefn_xstate f (Normal s)\<rangle> \<Rightarrow> add_statefn_xstate f t
A total of 19 subgoals...