kings-crown/FVELER_Isabelle huggingface dataset:
theory AutoCorresModifiesProofs

lemma returnOk_inv[valid_inv]:
  "\<lbrace>I\<rbrace> returnOk x \<lbrace>\<lambda>_. I\<rbrace>" apply (simp add: returnOk_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>I\<rbrace> returnOk x \<lbrace>\<lambda>_. I\<rbrace> proof (prove)
goal:
No subgoals!
theory AutoCorresModifiesProofs

lemma getsE_inv[valid_inv]:
  "\<lbrace>I\<rbrace> getsE f \<lbrace>\<lambda>r. I\<rbrace>" apply (unfold getsE_def) apply (blast intro: liftE_inv gets_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>I\<rbrace> getsE f \<lbrace>\<lambda>r. I\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>I\<rbrace> liftE (gets f) \<lbrace>\<lambda>r. I\<rbrace> proof (prove)
goal:
No subgoals!
theory AutoCorresModifiesProofs

lemma skipE_inv[valid_inv]:
  "\<lbrace>I\<rbrace> skipE \<lbrace>\<lambda>r. I\<rbrace>" apply (unfold skipE_def) apply (blast intro: liftE_inv returnOk_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>I\<rbrace> skipE \<lbrace>\<lambda>r. I\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>I\<rbrace> returnOk () \<lbrace>\<lambda>r. I\<rbrace> proof (prove)
goal:
No subgoals!
theory AutoCorresModifiesProofs

lemma modifyE_inv[valid_inv]:
  "(\<And>s. I s \<Longrightarrow> I (f s)) \<Longrightarrow> \<lbrace>I\<rbrace> modifyE f \<lbrace>\<lambda>_. I\<rbrace>" apply (unfold modifyE_def) apply (blast intro: liftE_inv modify_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. I s \<Longrightarrow> I (f s)) \<Longrightarrow> \<lbrace>I\<rbrace> modifyE f \<lbrace>\<lambda>_. I\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>s. I s \<Longrightarrow> I (f s)) \<Longrightarrow> \<lbrace>I\<rbrace> liftE (modify f) \<lbrace>\<lambda>_. I\<rbrace> proof (prove)
goal:
No subgoals!
theory AutoCorresModifiesProofs

lemma guardE_inv[valid_inv]:
  "\<lbrace>I\<rbrace> guardE G \<lbrace>\<lambda>_. I\<rbrace>" apply (unfold guardE_def) apply (blast intro: liftE_inv guard_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>I\<rbrace> guardE G \<lbrace>\<lambda>_. I\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>I\<rbrace> liftE (guard G) \<lbrace>\<lambda>_. I\<rbrace> proof (prove)
goal:
No subgoals!
theory AutoCorresModifiesProofs

lemma whenE_inv[valid_inv]:
  "\<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace> \<Longrightarrow> \<lbrace>I\<rbrace> whenE c f \<lbrace>\<lambda>_. I\<rbrace>" apply (unfold whenE_def) apply (auto intro: returnOk_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace> \<Longrightarrow> \<lbrace>I\<rbrace> whenE c f \<lbrace>\<lambda>_. I\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace> \<Longrightarrow> \<lbrace>I\<rbrace> if c then f else returnOk () \<lbrace>\<lambda>_. I\<rbrace> proof (prove)
goal:
No subgoals!
theory AutoCorresModifiesProofs

lemma unless_inv[valid_inv]:
  "\<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace> \<Longrightarrow> \<lbrace>I\<rbrace> unless c f \<lbrace>\<lambda>_. I\<rbrace>" apply (unfold unless_def) by (rule when_inv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace> \<Longrightarrow> \<lbrace>I\<rbrace> unless c f \<lbrace>\<lambda>_. I\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace> \<Longrightarrow> \<lbrace>I\<rbrace> when (\<not> c) f \<lbrace>\<lambda>_. I\<rbrace>
theory AutoCorresModifiesProofs

lemma unlessE_inv[valid_inv]:
  "\<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace> \<Longrightarrow> \<lbrace>I\<rbrace> unlessE c f \<lbrace>\<lambda>_. I\<rbrace>" apply (unfold unlessE_def) by (auto intro: returnOk_inv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace> \<Longrightarrow> \<lbrace>I\<rbrace> unlessE c f \<lbrace>\<lambda>_. I\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace> \<Longrightarrow> \<lbrace>I\<rbrace> if c then returnOk () else f \<lbrace>\<lambda>_. I\<rbrace>
theory AutoCorresModifiesProofs

lemma handleE'_inv[valid_inv]:
  "\<lbrakk> \<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>; \<And>e. \<lbrace>I\<rbrace> h e \<lbrace>\<lambda>_. I\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>I\<rbrace> handleE' f h \<lbrace>\<lambda>_. I\<rbrace>" by (fastforce simp: handleE'_def intro: return_inv bind_inv split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>; \<And>e. \<lbrace>I\<rbrace> h e \<lbrace>\<lambda>_. I\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>I\<rbrace> f <handle2> h \<lbrace>\<lambda>_. I\<rbrace>
theory AutoCorresModifiesProofs

lemma handleE_inv[valid_inv]:
  "\<lbrakk> \<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>; \<And>e. \<lbrace>I\<rbrace> h e \<lbrace>\<lambda>_. I\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>I\<rbrace> handleE f h \<lbrace>\<lambda>_. I\<rbrace>" apply (unfold handleE_def) by (rule handleE'_inv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>; \<And>e. \<lbrace>I\<rbrace> h e \<lbrace>\<lambda>_. I\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>I\<rbrace> f <handle> h \<lbrace>\<lambda>_. I\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>; \<And>e. \<lbrace>I\<rbrace> h e \<lbrace>\<lambda>_. I\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>I\<rbrace> f <handle2> h \<lbrace>\<lambda>_. I\<rbrace>
theory AutoCorresModifiesProofs

lemma measure_call_inv[valid_inv]:
  "\<lbrakk>\<And>m. \<lbrace>I\<rbrace> f m \<lbrace>\<lambda>_. I\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>I\<rbrace> measure_call f \<lbrace>\<lambda>_. I\<rbrace>" by (fastforce simp: measure_call_def valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>m. \<lbrace>I\<rbrace> f m \<lbrace>\<lambda>_. I\<rbrace>) \<Longrightarrow> \<lbrace>I\<rbrace> measure_call f \<lbrace>\<lambda>_. I\<rbrace>
theory AutoCorresModifiesProofs

lemma modifies_recursive_0: "\<lbrace>I\<rbrace> do guard (\<lambda>_. (0 :: nat) < 0); f od \<lbrace>\<lambda>_. I\<rbrace>" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>I\<rbrace> do guard (\<lambda>_. 0 < 0);
f
od \<lbrace>\<lambda>_. I\<rbrace>
theory AutoCorres_C

lemma corres_to_ccorres:
  assumes rf_sr_def: "rf_sr \<equiv> {(s,s'). cstate_relation s (globals s')}"
  assumes acc: "ac_corres globals check_term \<Gamma> ret_xf G (liftE ac) c"
  assumes cac: "corres_underlying {(s,s'). cstate_relation s s'} True True R P Q a ac"
  assumes pre: "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> P s \<and> Q (globals s')"
  assumes p_g: "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> G s'"
  assumes ret: "\<And>r s'. R r (ret_xf s') \<longrightarrow> R' r (ret_xf' s')"
  shows "ccorresG rf_sr \<Gamma> R' ret_xf' P' Q' [] a c" apply (rule corres_to_ccorres_extra_globals[OF rf_sr_def acc, where g="K ()" and R="\<lambda>v. R v o fst"]) apply (simp add: liftM_def[symmetric]) apply (rule corres_rel_imp, rule cac) apply (auto simp: pre p_g ret) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorresG rf_sr \<Gamma> R' ret_xf' P' Q' [] a c proof (prove)
goal (4 subgoals):
 1. corres_underlying {(s, s'). cstate_relation s s'} True True (\<lambda>v. R v \<circ> fst) ?P ?Q a (do x <- ac;
y <- gets (K ());
return (x, y)
od)
 2. \<And>s s'. \<lbrakk>cstate_relation s (globals s'); P' s \<and> s' \<in> Q'\<rbrakk> \<Longrightarrow> ?P s \<and> ?Q (globals s')
 3. \<And>s s'. \<lbrakk>cstate_relation s (globals s'); P' s \<and> s' \<in> Q'\<rbrakk> \<Longrightarrow> G s'
 4. \<And>r s'. (R r \<circ> fst) (ret_xf s', K () (globals s')) \<longrightarrow> R' r (ret_xf' s') proof (prove)
goal (4 subgoals):
 1. corres_underlying {(x, y). cstate_relation x y} True True (\<lambda>x. R x \<circ> fst \<circ> (\<lambda>x. (x, ()))) ?P ?Q a ac
 2. \<And>s s'. \<lbrakk>cstate_relation s (globals s'); P' s \<and> s' \<in> Q'\<rbrakk> \<Longrightarrow> ?P s \<and> ?Q (globals s')
 3. \<And>s s'. \<lbrakk>cstate_relation s (globals s'); P' s \<and> s' \<in> Q'\<rbrakk> \<Longrightarrow> G s'
 4. \<And>r s'. (R r \<circ> fst) (ret_xf s', K () (globals s')) \<longrightarrow> R' r (ret_xf' s') proof (prove)
goal (4 subgoals):
 1. \<And>x y. R x y \<Longrightarrow> (R x \<circ> fst \<circ> (\<lambda>x. (x, ()))) y
 2. \<And>s s'. \<lbrakk>cstate_relation s (globals s'); P' s \<and> s' \<in> Q'\<rbrakk> \<Longrightarrow> P s \<and> Q (globals s')
 3. \<And>s s'. \<lbrakk>cstate_relation s (globals s'); P' s \<and> s' \<in> Q'\<rbrakk> \<Longrightarrow> G s'
 4. \<And>r s'. (R r \<circ> fst) (ret_xf s', K () (globals s')) \<longrightarrow> R' r (ret_xf' s') proof (prove)
goal:
No subgoals!
theory AutoCorres_C

lemma corres_to_ccorres_extra_globals_rv_spec:
  assumes "rf_sr \<equiv> {(s,s'). cstate_relation s (globals s')}"
  assumes "ac_corres globals check_term \<Gamma> ret_xf G (liftE ac) c"
  assumes "corres_underlying {(s,s'). cstate_relation s s'} True True
                             (\<lambda>r (x,y). \<forall>s'. x = ret_xf s' \<and> y = g (globals s') \<longrightarrow> R' r (ret_xf' s'))
                             P Q a (do x \<leftarrow> ac; y \<leftarrow> gets g; return (x, y) od)"
  assumes "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> P s \<and> Q (globals s')"
  assumes "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> G s'"
  shows "ccorresG rf_sr \<Gamma> R' ret_xf' P' Q' [] a c" using assms by (auto intro: corres_to_ccorres_extra_globals)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorresG rf_sr \<Gamma> R' ret_xf' P' Q' [] a c proof (prove)
using this:
rf_sr \<equiv> {(s, s'). cstate_relation s (globals s')}
ac_corres globals check_term \<Gamma> ret_xf G (liftE ac) c
corres_underlying {(s, s'). cstate_relation s s'} True True (\<lambda>r (x, y). \<forall>s'. x = ret_xf s' \<and> y = g (globals s') \<longrightarrow> R' r (ret_xf' s')) P Q a (do x <- ac;
y <- gets g;
return (x, y)
od)
\<lbrakk>cstate_relation ?s (globals ?s'); P' ?s \<and> ?s' \<in> Q'\<rbrakk> \<Longrightarrow> P ?s \<and> Q (globals ?s')
\<lbrakk>cstate_relation ?s (globals ?s'); P' ?s \<and> ?s' \<in> Q'\<rbrakk> \<Longrightarrow> G ?s'

goal (1 subgoal):
 1. ccorresG rf_sr \<Gamma> R' ret_xf' P' Q' [] a c
theory AutoCorres_C

lemma corres_to_ccorres_rv_spec:
  assumes "rf_sr \<equiv> {(s,s'). cstate_relation s (globals s')}"
  assumes "ac_corres globals check_term \<Gamma> ret_xf G (liftE ac) c"
  assumes "corres_underlying {(s,s'). cstate_relation s s'} True True
                             (\<lambda>r r'. \<forall>s'. r' = ret_xf s' \<longrightarrow> R' r (ret_xf' s')) P Q a ac"
  assumes "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> P s \<and> Q (globals s')"
  assumes "\<And>s s'. cstate_relation s (globals s') \<Longrightarrow> P' s \<and> s' \<in> Q' \<Longrightarrow> G s'"
  shows "ccorresG rf_sr \<Gamma> R' ret_xf' P' Q' [] a c" using assms by (auto intro: corres_to_ccorres)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorresG rf_sr \<Gamma> R' ret_xf' P' Q' [] a c proof (prove)
using this:
rf_sr \<equiv> {(s, s'). cstate_relation s (globals s')}
ac_corres globals check_term \<Gamma> ret_xf G (liftE ac) c
corres_underlying {(s, s'). cstate_relation s s'} True True (\<lambda>r r'. \<forall>s'. r' = ret_xf s' \<longrightarrow> R' r (ret_xf' s')) P Q a ac
\<lbrakk>cstate_relation ?s (globals ?s'); P' ?s \<and> ?s' \<in> Q'\<rbrakk> \<Longrightarrow> P ?s \<and> Q (globals ?s')
\<lbrakk>cstate_relation ?s (globals ?s'); P' ?s \<and> ?s' \<in> Q'\<rbrakk> \<Longrightarrow> G ?s'

goal (1 subgoal):
 1. ccorresG rf_sr \<Gamma> R' ret_xf' P' Q' [] a c
theory AutoCorres_C

lemma in_AC_call_simpl:
  fixes r s s' arg_pred ret_xf \<Gamma> f_'proc
  shows "(r, s') \<in> fst (AC_call_L1 arg_pred globals ret_xf (L1_call_simpl check_term \<Gamma> f_'proc) s) \<Longrightarrow>
         \<exists>cs cs'. s = globals cs \<and> arg_pred cs \<and>
                  (check_term \<longrightarrow> \<Gamma> \<turnstile> Call f_'proc \<down> Normal cs) \<and>
                  \<Gamma> \<turnstile> \<langle>Call f_'proc, Normal cs\<rangle> \<Rightarrow> Normal cs' \<and>
                  s' = globals cs' \<and> r = ret_xf cs'" apply (clarsimp simp: AC_call_L1_def L2_call_L1_def L1_call_simpl_def
                        in_monad liftM_def select_def select_f_def
                 split: xstate.splits sum.splits) apply (rename_tac cs cs' status; case_tac status; fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (r, s') \<in> fst (AC_call_L1 arg_pred globals ret_xf (L1_call_simpl check_term \<Gamma> f_'proc) s) \<Longrightarrow> \<exists>cs cs'. s = globals cs \<and> arg_pred cs \<and> (check_term \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal cs) \<and> \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal cs\<rangle> \<Rightarrow> Normal cs' \<and> s' = globals cs' \<and> r = ret_xf cs' proof (prove)
goal (1 subgoal):
 1. \<And>sa b xa. \<lbrakk>\<forall>x1. xa = Normal x1 \<longrightarrow> \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal sa\<rangle> \<Rightarrow> Normal x1 \<and> b = x1; \<forall>x2. xa \<noteq> Abrupt x2; \<forall>x3. xa \<noteq> Fault x3; xa \<noteq> Stuck; r = ret_xf b; arg_pred sa; check_term \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal sa; s' = globals b; s = globals sa\<rbrakk> \<Longrightarrow> \<exists>cs. globals sa = globals cs \<and> arg_pred cs \<and> (check_term \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal cs) \<and> (\<exists>cs'. \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal cs\<rangle> \<Rightarrow> Normal cs' \<and> globals b = globals cs' \<and> ret_xf b = ret_xf cs') proof (prove)
goal:
No subgoals!
theory AutoCorres_C

lemma ccorres_to_corres_pre_globals_Int:
  assumes "ccorres_to_corres_pre Q E Q' s'"
  shows "ccorres_to_corres_pre (P and Q) E ({s'. P (globals s')} \<inter> Q') s'" using assms by (simp add: ccorres_to_corres_pre_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_to_corres_pre (P and Q) E ({s'. P (globals s')} \<inter> Q') s' proof (prove)
using this:
ccorres_to_corres_pre Q E Q' s'

goal (1 subgoal):
 1. ccorres_to_corres_pre (P and Q) E ({s'. P (globals s')} \<inter> Q') s'
theory AutoCorres_C

lemma ccorres_to_corres_pre_local_Int:
  assumes "f s' = x"
  assumes "ccorres_to_corres_pre Q (K (P x) and E) Q' s'"
  shows "ccorres_to_corres_pre Q E ({s'. P (f s')} \<inter> Q') s'" using assms by (simp add: ccorres_to_corres_pre_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_to_corres_pre Q E ({s'. P (f s')} \<inter> Q') s' proof (prove)
using this:
f s' = x
ccorres_to_corres_pre Q (K (P x) and E) Q' s'

goal (1 subgoal):
 1. ccorres_to_corres_pre Q E ({s'. P (f s')} \<inter> Q') s'
theory AutoCorres_C

lemma ccorres_to_corres_pre_UNIV_Int:
  assumes "ccorres_to_corres_pre Q E Q' s'"
  shows "ccorres_to_corres_pre Q E (UNIV \<inter> Q') s'" using assms by (simp add: ccorres_to_corres_pre_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_to_corres_pre Q E (UNIV \<inter> Q') s' proof (prove)
using this:
ccorres_to_corres_pre Q E Q' s'

goal (1 subgoal):
 1. ccorres_to_corres_pre Q E (UNIV \<inter> Q') s'
theory AutoCorres_C

lemma ccorres_to_corres_pre_finalise:
  "E s' \<Longrightarrow> ccorres_to_corres_pre \<top> E UNIV s'" by (simp add: ccorres_to_corres_pre_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. E s' \<Longrightarrow> ccorres_to_corres_pre (\<lambda>_. True) E UNIV s'
theory AutoCorres_C

lemma ccorres_to_corres_partial:
  assumes rf_sr_def: "rf_sr \<equiv> {(s,s'). cstate_relation s (globals s')}"
  assumes ac_def: "ac_f \<equiv> AC_call_L1 G globals ret_xf (L1_call_simpl check_term \<Gamma> f_'proc)"
  assumes ccorres: "ccorresG rf_sr \<Gamma> R' ret_xf' P Q' [] dspec_f (Call f_'proc)"
  assumes pre: "\<And>s'. G s' \<Longrightarrow> ccorres_to_corres_pre Q \<top> Q' s'"
  assumes ret: "\<And>r s'. R r (ret_xf s') \<longleftrightarrow> R' r (ret_xf' s')"
  shows "corres_underlying {(s, s'). cstate_relation s s'} True False R P Q dspec_f ac_f" using ccorres ret pre unfolding ac_def ccorres_to_corres_pre_def by (fastforce simp: unif_rrel_def corres_underlying_def ccorres_underlying_def rf_sr_def
                intro: EHOther dest: in_AC_call_simpl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying {(s, s'). cstate_relation s s'} True False R P Q dspec_f ac_f proof (prove)
using this:
ccorresG rf_sr \<Gamma> R' ret_xf' P Q' [] dspec_f (Call f_'proc)
R ?r (ret_xf ?s') = R' ?r (ret_xf' ?s')
G ?s' \<Longrightarrow> ccorres_to_corres_pre Q (\<lambda>_. True) Q' ?s'

goal (1 subgoal):
 1. corres_underlying {(s, s'). cstate_relation s s'} True False R P Q dspec_f ac_f proof (prove)
using this:
ccorresG rf_sr \<Gamma> R' ret_xf' P Q' [] dspec_f (Call f_'proc)
R ?r (ret_xf ?s') = R' ?r (ret_xf' ?s')
G ?s' \<Longrightarrow> Q (globals ?s') \<longrightarrow> True \<and> ?s' \<in> Q'

goal (1 subgoal):
 1. corres_underlying {(s, s'). cstate_relation s s'} True False R P Q dspec_f (AC_call_L1 G globals ret_xf (L1_call_simpl check_term \<Gamma> f_'proc))
theory AutoCorres_C

lemma collect_lift:
  "Collect (\<lambda>s. s0 = s \<and> f s) = Collect (\<lambda>s. s0 = s \<and> f s0)" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {s. s0 = s \<and> f s} = \<lbrace>s0. f s0\<rbrace>
theory AutoCorres_C

lemma collect_unlift:
  "Collect (\<lambda>s. s0 = s \<and> f s0 s) = Collect (\<lambda>s. s0 = s \<and> f s s)" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {s. s0 = s \<and> f s0 s} = {s. s0 = s \<and> f s s}
theory AutoCorres_C

lemma exec_no_fault:
  assumes asms: "s \<in> P"
  and     ce: "Gamma \<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> Fault f"
  and  valid: "Gamma \<turnstile> P c Q, A"
  shows   "False" using valid ce asms apply - apply (frule hoare_sound) apply (clarsimp simp: Nondet_Monad.bind_def cvalid_def split_def HoarePartialDef.valid_def) apply (drule spec, drule spec, drule (1) mp) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. False proof (prove)
using this:
Gamma\<turnstile> P c Q,A
Gamma\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Fault f
s \<in> P

goal (1 subgoal):
 1. False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Gamma\<turnstile> P c Q,A; Gamma\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Fault f; s \<in> P\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Gamma\<turnstile> P c Q,A; Gamma\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Fault f; s \<in> P; Gamma,{}\<Turnstile>\<^bsub>/{}\<^esub> P c Q,A\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Gamma\<turnstile> P c Q,A; Gamma\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Fault f; s \<in> P; \<forall>s t. Gamma\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` A\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Gamma\<turnstile> P c Q,A; Gamma\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Fault f; s \<in> P; Normal s \<in> Normal ` P \<longrightarrow> Fault f \<in> Normal ` Q \<or> Fault f \<in> Abrupt ` A\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory AutoCorres_C

lemma exec_no_stuck:
  assumes asms: "s \<in> P"
  and     ce: "Gamma \<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> Stuck"
  and  valid: "Gamma \<turnstile> P c Q, A"
  shows   "False" using valid ce asms apply - apply (frule hoare_sound) apply (clarsimp simp: Nondet_Monad.bind_def cvalid_def split_def HoarePartialDef.valid_def) apply (drule spec, drule spec, drule (1) mp) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. False proof (prove)
using this:
Gamma\<turnstile> P c Q,A
Gamma\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Stuck
s \<in> P

goal (1 subgoal):
 1. False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Gamma\<turnstile> P c Q,A; Gamma\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Stuck; s \<in> P\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Gamma\<turnstile> P c Q,A; Gamma\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Stuck; s \<in> P; Gamma,{}\<Turnstile>\<^bsub>/{}\<^esub> P c Q,A\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Gamma\<turnstile> P c Q,A; Gamma\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Stuck; s \<in> P; \<forall>s t. Gamma\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` A\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Gamma\<turnstile> P c Q,A; Gamma\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Stuck; s \<in> P; Normal s \<in> Normal ` P \<longrightarrow> Stuck \<in> Normal ` Q \<or> Stuck \<in> Abrupt ` A\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory AutoCorres_C

lemma [terminates_trivial]:
  "\<lbrakk> \<And>s. \<Gamma> \<turnstile> c \<down> Normal s \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Guard F G c \<down> Normal s" apply (blast intro: terminates.Guard terminates.GuardFault) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. \<Gamma>\<turnstile>c \<down> Normal s) \<Longrightarrow> \<Gamma>\<turnstile>Guard F G c \<down> Normal s proof (prove)
goal:
No subgoals!
theory AutoCorres_C

lemma [terminates_trivial]:
  "\<lbrakk> \<And>s. \<Gamma> \<turnstile> c1 \<down> Normal s; \<And>s. \<Gamma> \<turnstile> c2 \<down> Normal s \<rbrakk> \<Longrightarrow>
   \<Gamma> \<turnstile> Cond C c1 c2 \<down> Normal s" apply (blast intro: terminates.CondTrue terminates.CondFalse) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. \<Gamma>\<turnstile>c1 \<down> Normal s; \<And>s. \<Gamma>\<turnstile>c2 \<down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>Cond C c1 c2 \<down> Normal s proof (prove)
goal:
No subgoals!
theory AutoCorres_C

lemma [terminates_trivial]:
  "\<lbrakk> \<Gamma> \<turnstile> c1 \<down> Normal s; \<And>s. \<Gamma> \<turnstile> c2 \<down> Normal s \<rbrakk> \<Longrightarrow>
   \<Gamma> \<turnstile> c1;;c2 \<down> Normal s" apply (erule terminates.Seq) apply clarsimp apply (case_tac s'; auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile>c1 \<down> Normal s; \<And>s. \<Gamma>\<turnstile>c2 \<down> Normal s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c1;;
c2 \<down> Normal s proof (prove)
goal (1 subgoal):
 1. (\<And>s. \<Gamma>\<turnstile>c2 \<down> Normal s) \<Longrightarrow> \<forall>s'. \<Gamma>\<turnstile> \<langle>c1,Normal s\<rangle> \<Rightarrow> s' \<longrightarrow> \<Gamma>\<turnstile>c2 \<down> s' proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>\<And>s. \<Gamma>\<turnstile>c2 \<down> Normal s; \<Gamma>\<turnstile> \<langle>c1,Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>c2 \<down> s' proof (prove)
goal:
No subgoals!