theory Ctac

lemma ceqv_xpres_call_hoarep_gen:
  assumes mod: "\<forall>s. \<Gamma>\<turnstile>\<^bsub>/F s\<^esub> (P s) Call f (Q s),(A s)"
  assumes args: "ceqv_xpres_call_restore_args f i i''"
  assumes init: "ceqv_xpres_rewrite_basic xf v i'' i'"
  assumes reset: "\<And>t. ceqv_xpres_basic_preserves (call i f reset ret) xf v
                        (\<lambda>s. i' s \<in> P (x s) \<longrightarrow> t \<in> Q (x s) \<or> t \<in> A (x s))
                        (\<lambda>s. reset s t) pres_reset"
  assumes xpr: "\<And>s t. ceqv_xpres \<Gamma> xf v pres_reset (ret s t) pres_norm pres_abr abnormal (ret' s t)"
  shows "ceqv_xpres_call \<Gamma> xf v f reset i ret pres_norm pres_abr abnormal i' ret'" proof (cases pres_reset) case True note xpr' = xpr[simplified True] show ?thesis unfolding ceqv_xpres_call_def args[unfolded ceqv_xpres_call_restore_args_def] apply (rule ceqv_xpresI) apply (rule call_ceqv_hoarep_gen[OF mod _ xpr'[THEN ceqv_xpres_ceqvD]]) apply (simp add: rewrite_xf_def init[unfolded ceqv_xpres_rewrite_basic_def]) using reset apply (fastforce simp: True ceqv_xpres_basic_preserves_def) apply (rule xpres_strong_call_hoarep_gen[OF mod _ ceqv_xpres_xpresD[OF xpr']]) using reset by (fastforce simp: True ceqv_xpres_basic_preserves_def
                                  init[unfolded ceqv_xpres_rewrite_basic_def]) next case False have 1: "pres_norm = abnormal \<and> \<not> pres_abr \<and> ret' = ret" using xpr by (auto simp: False ceqv_xpres_def) then show ?thesis unfolding ceqv_xpres_call_def args[unfolded ceqv_xpres_call_restore_args_def] using init xpr[simplified False, THEN ceqv_xpres_abnormalD] apply (clarsimp simp add: 1 ceqv_xpres_def ceqv_def ceqv_xpres_rewrite_basic_def
                            xpres_strong_abnormal_iff xpres_abnormal_call) by (auto elim!: exec_call_Normal_elim exec_call
                  exec_callAbrupt exec_callFault exec_callStuck exec_callUndefined) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv_xpres_call \<Gamma> xf v f reset i ret pres_norm pres_abr abnormal i' ret' proof (state)
goal (2 subgoals):
 1. pres_reset \<Longrightarrow> ceqv_xpres_call \<Gamma> xf v f reset i ret pres_norm pres_abr abnormal i' ret'
 2. \<not> pres_reset \<Longrightarrow> ceqv_xpres_call \<Gamma> xf v f reset i ret pres_norm pres_abr abnormal i' ret' proof (state)
this:
pres_reset

goal (2 subgoals):
 1. pres_reset \<Longrightarrow> ceqv_xpres_call \<Gamma> xf v f reset i ret pres_norm pres_abr abnormal i' ret'
 2. \<not> pres_reset \<Longrightarrow> ceqv_xpres_call \<Gamma> xf v f reset i ret pres_norm pres_abr abnormal i' ret' proof (state)
this:
ceqv_xpres \<Gamma> xf v True (ret ?s ?t) pres_norm pres_abr abnormal (ret' ?s ?t)

goal (2 subgoals):
 1. pres_reset \<Longrightarrow> ceqv_xpres_call \<Gamma> xf v f reset i ret pres_norm pres_abr abnormal i' ret'
 2. \<not> pres_reset \<Longrightarrow> ceqv_xpres_call \<Gamma> xf v f reset i ret pres_norm pres_abr abnormal i' ret' proof (prove)
goal (1 subgoal):
 1. ceqv_xpres_call \<Gamma> xf v f reset i ret pres_norm pres_abr abnormal i' ret' proof (prove)
goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf v True (call i'' f reset ret) pres_norm pres_abr abnormal (call i' f reset ret') proof (prove)
goal (2 subgoals):
 1. \<And>s t. ceqv \<Gamma> xf v s t (call i'' f reset ret) (call i' f reset ret')
 2. xpres_strong \<Gamma> xf v (call i'' f reset ret) pres_norm pres_abr abnormal proof (prove)
goal (3 subgoals):
 1. \<And>s t sa. rewrite_xf xf sa v i'' i'
 2. \<And>s t sa ta. \<lbrakk>xf sa = v; i' sa \<in> P (?x3 s t sa) \<longrightarrow> ta \<in> Q (?x3 s t sa) \<or> ta \<in> A (?x3 s t sa)\<rbrakk> \<Longrightarrow> xf (reset sa ta) = v
 3. xpres_strong \<Gamma> xf v (call i'' f reset ret) pres_norm pres_abr abnormal proof (prove)
goal (2 subgoals):
 1. \<And>s t sa ta. \<lbrakk>xf sa = v; i' sa \<in> P (?x3 s t sa) \<longrightarrow> ta \<in> Q (?x3 s t sa) \<or> ta \<in> A (?x3 s t sa)\<rbrakk> \<Longrightarrow> xf (reset sa ta) = v
 2. xpres_strong \<Gamma> xf v (call i'' f reset ret) pres_norm pres_abr abnormal proof (prove)
using this:
ceqv_xpres_basic_preserves (call i f reset ret) xf v (\<lambda>s. i' s \<in> P (x s) \<longrightarrow> ?t \<in> Q (x s) \<or> ?t \<in> A (x s)) (\<lambda>s. reset s ?t) pres_reset

goal (2 subgoals):
 1. \<And>s t sa ta. \<lbrakk>xf sa = v; i' sa \<in> P (?x3 s t sa) \<longrightarrow> ta \<in> Q (?x3 s t sa) \<or> ta \<in> A (?x3 s t sa)\<rbrakk> \<Longrightarrow> xf (reset sa ta) = v
 2. xpres_strong \<Gamma> xf v (call i'' f reset ret) pres_norm pres_abr abnormal proof (prove)
goal (1 subgoal):
 1. xpres_strong \<Gamma> xf v (call i'' f reset ret) pres_norm pres_abr abnormal proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>xf s = v; i'' s \<in> P (?x32 s) \<longrightarrow> t \<in> Q (?x32 s) \<or> t \<in> A (?x32 s)\<rbrakk> \<Longrightarrow> xf (reset s t) = v proof (prove)
using this:
ceqv_xpres_basic_preserves (call i f reset ret) xf v (\<lambda>s. i' s \<in> P (x s) \<longrightarrow> ?t \<in> Q (x s) \<or> ?t \<in> A (x s)) (\<lambda>s. reset s ?t) pres_reset

goal (1 subgoal):
 1. \<And>s t. \<lbrakk>xf s = v; i'' s \<in> P (?x32 s) \<longrightarrow> t \<in> Q (?x32 s) \<or> t \<in> A (?x32 s)\<rbrakk> \<Longrightarrow> xf (reset s t) = v proof (state)
this:
ceqv_xpres_call \<Gamma> xf v f reset i ret pres_norm pres_abr abnormal i' ret'

goal (1 subgoal):
 1. \<not> pres_reset \<Longrightarrow> ceqv_xpres_call \<Gamma> xf v f reset i ret pres_norm pres_abr abnormal i' ret' proof (state)
goal (1 subgoal):
 1. \<not> pres_reset \<Longrightarrow> ceqv_xpres_call \<Gamma> xf v f reset i ret pres_norm pres_abr abnormal i' ret' proof (state)
this:
\<not> pres_reset

goal (1 subgoal):
 1. \<not> pres_reset \<Longrightarrow> ceqv_xpres_call \<Gamma> xf v f reset i ret pres_norm pres_abr abnormal i' ret' proof (prove)
goal (1 subgoal):
 1. pres_norm = abnormal \<and> \<not> pres_abr \<and> ret' = ret proof (prove)
using this:
ceqv_xpres \<Gamma> xf v pres_reset (ret ?s ?t) pres_norm pres_abr abnormal (ret' ?s ?t)

goal (1 subgoal):
 1. pres_norm = abnormal \<and> \<not> pres_abr \<and> ret' = ret proof (state)
this:
pres_norm = abnormal \<and> \<not> pres_abr \<and> ret' = ret

goal (1 subgoal):
 1. \<not> pres_reset \<Longrightarrow> ceqv_xpres_call \<Gamma> xf v f reset i ret pres_norm pres_abr abnormal i' ret' proof (chain)
picking this:
pres_norm = abnormal \<and> \<not> pres_abr \<and> ret' = ret proof (prove)
using this:
pres_norm = abnormal \<and> \<not> pres_abr \<and> ret' = ret

goal (1 subgoal):
 1. ceqv_xpres_call \<Gamma> xf v f reset i ret pres_norm pres_abr abnormal i' ret' proof (prove)
using this:
pres_norm = abnormal \<and> \<not> pres_abr \<and> ret' = ret

goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf v True (call i'' f reset ret) pres_norm pres_abr abnormal (call i' f reset ret') proof (prove)
using this:
pres_norm = abnormal \<and> \<not> pres_abr \<and> ret' = ret
ceqv_xpres_rewrite_basic xf v i'' i'
xpres_abnormal \<Gamma> (ret ?s1 ?t1) abnormal

goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf v True (call i'' f reset ret) pres_norm pres_abr abnormal (call i' f reset ret') proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>\<forall>sa. xf sa = xf s \<longrightarrow> i'' sa = i' sa; \<And>s t. xpres_abnormal \<Gamma> (ret s t) abnormal; v = xf s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call i'' f reset ret,Normal s\<rangle> \<Rightarrow> t = \<Gamma>\<turnstile> \<langle>call i' f reset ret,Normal s\<rangle> \<Rightarrow> t proof (state)
this:
ceqv_xpres_call \<Gamma> xf v f reset i ret pres_norm pres_abr abnormal i' ret'

goal:
No subgoals!