kings-crown/FVELER_Isabelle huggingface dataset:
theory Corres_UL_C

lemma ccorres_seq_cond_raise:
  "ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (Cond S x y ;; c)
    = ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (Cond S (x ;; c) (y ;; c))" apply (rule ccorres_semantic_equiv) apply (rule semantic_equivI) apply (auto elim!: exec_Normal_elim_cases intro: exec.intros) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (Cond S x y;;
c) = ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (Cond S (x;;
c) (y;;
c)) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> G' \<Longrightarrow> semantic_equiv \<Gamma> s s' (Cond S x y;;
c) (Cond S (x;;
c) (y;;
c)) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> G' \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond S x y;;
c,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>Cond S (x;;
c) (y;;
c),Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma ccorres_seq_cond_empty:
  "ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (Cond {} x y ;; c) = ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (y ;; c)" apply (rule ccorres_semantic_equiv) apply (rule semantic_equivI) apply (auto elim!: exec_Normal_elim_cases intro: exec.intros) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (Cond {} x y;;
c) = ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (y;;
c) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> G' \<Longrightarrow> semantic_equiv \<Gamma> s s' (Cond {} x y;;
c) (y;;
c) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> G' \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond {} x y;;
c,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>y;;
c,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma ccorres_seq_cond_univ:
  "ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (Cond UNIV x y ;; c) = ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (x ;; c)" apply (rule ccorres_semantic_equiv) apply (rule semantic_equivI) apply (auto elim!: exec_Normal_elim_cases intro: exec.intros) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (Cond UNIV x y;;
c) = ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (x;;
c) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> G' \<Longrightarrow> semantic_equiv \<Gamma> s s' (Cond UNIV x y;;
c) (x;;
c) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> G' \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond UNIV x y;;
c,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>x;;
c,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma ccorres_cond_true:
  "ccorres_underlying sr \<Gamma> r xf arrel axf R R' hs a c \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf R (R' \<inter> P) hs a (Cond P c d)" apply (rule ccorres_guard_imp2) apply (erule ccorres_cond_weak) apply (rule ccorres_gen_asm2 [where P = False]) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf R R' hs a c \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf R (R' \<inter> P) hs a (Cond P c d) proof (prove)
goal (2 subgoals):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf R R' hs a c \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf ?Q ?Q' hs a (Cond P c d)
 2. \<And>s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf R R' hs a c; (s, s') \<in> sr; R s; s' \<in> R' \<inter> P\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (2 subgoals):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf ?Pf3 ?Rf3 hs a d
 2. \<And>s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf R R' hs a c; (s, s') \<in> sr; R s; s' \<in> R' \<inter> P\<rbrakk> \<Longrightarrow> (R and ?Pf3) s \<and> s' \<in> R' \<inter> P \<union> ?Rf3 \<inter> - P proof (prove)
goal (2 subgoals):
 1. False \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf ?Pf3 ?G'5 hs a d
 2. \<And>s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf R R' hs a c; (s, s') \<in> sr; R s; s' \<in> R' \<inter> P\<rbrakk> \<Longrightarrow> (R and ?Pf3) s \<and> s' \<in> R' \<inter> P \<union> ?G'5 \<inter> \<lbrace>False\<rbrace> \<inter> - P proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf R R' hs a c; (s, s') \<in> sr; R s; s' \<in> R' \<inter> P\<rbrakk> \<Longrightarrow> (R and ?Pf3) s \<and> s' \<in> R' \<inter> P \<union> ?G'5 \<inter> \<lbrace>False\<rbrace> \<inter> - P proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma ccorres_cond_false:
  "ccorres_underlying sr \<Gamma> r xf arrel axf R R' hs a d
     \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf R (R' \<inter> - P) hs a (Cond P c d)" apply (rule ccorres_guard_imp2) apply (rule ccorres_cond_weak) apply (rule ccorres_gen_asm2 [where P = False]) apply simp apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf R R' hs a d \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf R (R' \<inter> - P) hs a (Cond P c d) proof (prove)
goal (2 subgoals):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf R R' hs a d \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf ?Q ?Q' hs a (Cond P c d)
 2. \<And>s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf R R' hs a d; (s, s') \<in> sr; R s; s' \<in> R' \<inter> - P\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (3 subgoals):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf R R' hs a d \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf ?Pt3 ?Rt3 hs a c
 2. ccorres_underlying sr \<Gamma> r xf arrel axf R R' hs a d \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf ?Pf3 ?Rf3 hs a d
 3. \<And>s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf R R' hs a d; (s, s') \<in> sr; R s; s' \<in> R' \<inter> - P\<rbrakk> \<Longrightarrow> (?Pt3 and ?Pf3) s \<and> s' \<in> ?Rt3 \<inter> P \<union> ?Rf3 \<inter> - P proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf R R' hs a d; False\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf ?Pt3 ?G'6 hs a c
 2. ccorres_underlying sr \<Gamma> r xf arrel axf R R' hs a d \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf ?Pf3 ?Rf3 hs a d
 3. \<And>s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf R R' hs a d; (s, s') \<in> sr; R s; s' \<in> R' \<inter> - P\<rbrakk> \<Longrightarrow> (?Pt3 and ?Pf3) s \<and> s' \<in> ?G'6 \<inter> \<lbrace>False\<rbrace> \<inter> P \<union> ?Rf3 \<inter> - P proof (prove)
goal (2 subgoals):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf R R' hs a d \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf ?Pf3 ?Rf3 hs a d
 2. \<And>s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf R R' hs a d; (s, s') \<in> sr; R s; s' \<in> R' \<inter> - P\<rbrakk> \<Longrightarrow> (?Pt3 and ?Pf3) s \<and> s' \<in> ?G'6 \<inter> \<lbrace>False\<rbrace> \<inter> P \<union> ?Rf3 \<inter> - P proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf R R' hs a d; (s, s') \<in> sr; R s; s' \<in> R' \<inter> - P\<rbrakk> \<Longrightarrow> (?Pt3 and R) s \<and> s' \<in> ?G'6 \<inter> \<lbrace>False\<rbrace> \<inter> P \<union> R' \<inter> - P proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma ccorres_cond_false_seq:
  "ccorres_underlying sr \<Gamma> r xf arrel axf R R' hs a (d ;; e)
     \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf R (R' \<inter> - P) hs a (Cond P c d ;; e)" apply (simp add: ccorres_seq_cond_raise) apply (erule ccorres_cond_false) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf R R' hs a (d;;
e) \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf R (R' \<inter> - P) hs a (Cond P c d;;
e) proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf R R' hs a (d;;
e) \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf R (R' \<inter> - P) hs a (Cond P (c;;
e) (d;;
e)) proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma ccorres_cond_true_seq:
  "ccorres_underlying sr \<Gamma> r xf arrel axf R R' hs a (c ;; e)
     \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf R (R' \<inter> P) hs a (Cond P c d ;; e)" apply (simp add: ccorres_seq_cond_raise) apply (erule ccorres_cond_true) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf R R' hs a (c;;
e) \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf R (R' \<inter> P) hs a (Cond P c d;;
e) proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf R R' hs a (c;;
e) \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf R (R' \<inter> P) hs a (Cond P (c;;
e) (d;;
e)) proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma ccorres_assume_pre:
  assumes "\<And>s. P s \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf r' xf' (P and (\<lambda>s'. s' = s)) P' hs H C"
  shows "ccorres_underlying sr \<Gamma> r xf r' xf' P P' hs H C" apply (clarsimp simp: ccorres_underlying_def) apply (frule assms) apply (simp add: ccorres_underlying_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf r' xf' P P' hs H C proof (prove)
goal (1 subgoal):
 1. \<And>a b n t. \<lbrakk>(a, b) \<in> sr; P a; b \<in> P'; \<not> snd (H a); \<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (H a). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r' xf' ra s'' | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b n t. \<lbrakk>(a, b) \<in> sr; P a; b \<in> P'; \<not> snd (H a); \<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, t); ccorres_underlying sr \<Gamma> r xf r' xf' (P and (\<lambda>s'. s' = a)) P' hs H C\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (H a). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r' xf' ra s'' | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b n t. \<lbrakk>(a, b) \<in> sr; P a; b \<in> P'; \<not> snd (H a); \<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, t); \<forall>x\<in>sr. case x of (s, s') \<Rightarrow> P s \<and> s = a \<and> s' \<in> P' \<and> \<not> snd (H s) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (H s). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r' xf' ra s'' | _ \<Rightarrow> False))\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (H a). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf r' xf' ra s'' | _ \<Rightarrow> False proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma ccorres_name_pre:
  "(\<And>s. P s \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf r' xf' (\<lambda>s'. s' = s) P' hs H C)
    \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf r' xf'  P P' hs H C" apply (rule ccorres_assume_pre) apply (rule ccorres_guard_imp) apply fastforce apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. P s \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf r' xf' (\<lambda>s'. s' = s) P' hs H C) \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf r' xf' P P' hs H C proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>s. P s \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf r' xf' (\<lambda>s'. s' = s) P' hs H C; P s\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf r' xf' (P and (\<lambda>s'. s' = s)) P' hs H C proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>\<And>s. P s \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf r' xf' (\<lambda>s'. s' = s) P' hs H C; P s\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf r' xf' (?Q2 s) (?Q'2 s) hs H C
 2. \<And>s sa. \<lbrakk>\<And>s. P s \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf r' xf' (\<lambda>s'. s' = s) P' hs H C; P s; (P and (\<lambda>s'. s' = s)) sa\<rbrakk> \<Longrightarrow> ?Q2 s sa
 3. \<And>s sa. \<lbrakk>\<And>s. P s \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf r' xf' (\<lambda>s'. s' = s) P' hs H C; P s; sa \<in> P'\<rbrakk> \<Longrightarrow> sa \<in> ?Q'2 s proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>\<And>s. P s \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf r' xf' (\<lambda>s'. s' = s) P' hs H C; P s; (P and (\<lambda>s'. s' = s)) sa\<rbrakk> \<Longrightarrow> sa = s
 2. \<And>s sa. \<lbrakk>\<And>s. P s \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf r' xf' (\<lambda>s'. s' = s) P' hs H C; P s; sa \<in> P'\<rbrakk> \<Longrightarrow> sa \<in> P' proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>\<And>s. P s \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf r' xf' (\<lambda>s'. s' = s) P' hs H C; P s; sa \<in> P'\<rbrakk> \<Longrightarrow> sa \<in> P' proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma ccorres_lhs_assoc:
  assumes cc: "ccorres_underlying sr E r xf arrel axf G G' hs (m >>= f >>= g) c"
  shows "ccorres_underlying sr E r xf arrel axf G G' hs (do x \<leftarrow> m; f x >>= g od) c" using cc by (simp add: bind_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr E r xf arrel axf G G' hs (do x <- m;
f x >>= g
od) c proof (prove)
using this:
ccorres_underlying sr E r xf arrel axf G G' hs (m >>= f >>= g) c

goal (1 subgoal):
 1. ccorres_underlying sr E r xf arrel axf G G' hs (do x <- m;
f x >>= g
od) c
theory Corres_UL_C

lemma ccorres_grab_asm:
  "(Q \<Longrightarrow> ccorres_underlying sr G rr xf ar ax P P' hs f g) \<Longrightarrow>
   ccorres_underlying sr G rr xf ar ax (P and K Q) P' hs f g" by (fastforce simp: ccorres_underlying_def)


\<comment> \<open> An experimental cong rule for rewriting everywhere reasonable, with full context.
    Can cause problems when there are schematic variables or when one of the return relations
    takes a pair as a parameter. \<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (Q \<Longrightarrow> ccorres_underlying sr G rr xf ar ax P P' hs f g) \<Longrightarrow> ccorres_underlying sr G rr xf ar ax (P and K Q) P' hs f g
theory Corres_UL_C

lemma ccorres_context_weak_cong:
  assumes "\<And>s. P s = P' s"
  assumes "\<And>s s'. \<lbrakk> (s, s') \<in> sr; P' s \<rbrakk> \<Longrightarrow> Q = Q'"
  assumes "\<And>s s'. \<lbrakk> (s, s') \<in> sr; P' s; s' \<in> Q' \<rbrakk> \<Longrightarrow> a s = a' s"
  assumes "\<And>s s' s''. \<lbrakk> (s, s') \<in> sr; P' s; s' \<in> Q' \<rbrakk>  \<Longrightarrow> \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> s'' = \<Gamma>\<turnstile> \<langle>c',Normal s'\<rangle> \<Rightarrow> s''"
  shows   "ccorres_underlying sr \<Gamma> r xf ar axf P Q hs a c
           = ccorres_underlying sr \<Gamma> r xf ar axf P' Q' hs a' c'" by (clarsimp simp: assms cong: ccorres_context_cong)

\<comment> \<open> Even more restrictive: only rewrite the abstract monad. \<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf ar axf P Q hs a c = ccorres_underlying sr \<Gamma> r xf ar axf P' Q' hs a' c'
theory Corres_UL_C

lemma ccorres_abstract_cong:
  "\<lbrakk> \<And>s s'. \<lbrakk> (s, s') \<in> sr; P s ; s' \<in> P' \<rbrakk> \<Longrightarrow> a s = b s \<rbrakk> \<Longrightarrow>
   ccorres_underlying sr G r xf ar axf P P' hs a c
   = ccorres_underlying sr G r xf ar axf P P' hs b c" by (clarsimp cong: ccorres_context_weak_cong)

\<comment> \<open> Rewrite almost everywhere, without context. This should behave the same as with normal
    term rewriting with no cong rule, except it will not rewrite the state relation or function
    environment. \<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s s'. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'\<rbrakk> \<Longrightarrow> a s = b s) \<Longrightarrow> ccorres_underlying sr G r xf ar axf P P' hs a c = ccorres_underlying sr G r xf ar axf P P' hs b c
theory Corres_UL_C

lemma ccorres_all_cong:
  "\<lbrakk> r=r'; xf=xf'; ar=ar'; axf=axf'; P=P'; Q=Q'; hs=hs'; m=m'; c=c' \<rbrakk> \<Longrightarrow>
   ccorres_underlying srel \<Gamma> r xf ar axf P Q hs m c
   = ccorres_underlying srel \<Gamma> r' xf' ar' axf' P' Q' hs' m' c'" by (simp cong: ccorres_context_cong)

\<comment> \<open> Only rewrite guards, the handler stack and function bodies, without context.
    We make this the default behaviour, so that the the return relations and extraction
    functions are stable under simplification. \<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r = r'; xf = xf'; ar = ar'; axf = axf'; P = P'; Q = Q'; hs = hs'; m = m'; c = c'\<rbrakk> \<Longrightarrow> ccorres_underlying srel \<Gamma> r xf ar axf P Q hs m c = ccorres_underlying srel \<Gamma> r' xf' ar' axf' P' Q' hs' m' c'
theory Simpl_Rewrite

lemma com_eq_weaken_guard:
  "com_eq t c c' \<Longrightarrow> (t' \<Longrightarrow> t) \<Longrightarrow> com_eq t' c c'" by (simp add: com_eq_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>local.com_eq t c c'; t' \<Longrightarrow> t\<rbrakk> \<Longrightarrow> local.com_eq t' c c'
theory Simpl_Rewrite

lemma com_eq_guard_False:
  "com_eq False c c'" by (simp add: com_eq_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. local.com_eq False c c'
theory Simpl_Rewrite

lemma com_eq_refl:
  "c \<sim> c" by (auto simp: com_eq_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c \<sim> c
theory Simpl_Rewrite

lemma com_eq_sym:
  "c \<sim> c' \<Longrightarrow> c' \<sim> c" by (auto simp: com_eq_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c \<sim> c' \<Longrightarrow> c' \<sim> c
theory Simpl_Rewrite

lemma com_eq_trans:
  "\<lbrakk> c \<sim> c'; c' \<sim> c'' \<rbrakk> \<Longrightarrow> c \<sim> c''" by (auto simp add: com_eq_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<sim> c'; c' \<sim> c''\<rbrakk> \<Longrightarrow> c \<sim> c''
theory Simpl_Rewrite

lemma com_eq_Seq:
  "\<lbrakk> c1 \<sim> c1'; c2 \<sim> c2' \<rbrakk> \<Longrightarrow> c1;;c2 \<sim> c1';;c2'" unfolding com_eq_def by (auto intro: exec.Seq elim!: exec_elim_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c1 \<sim> c1'; c2 \<sim> c2'\<rbrakk> \<Longrightarrow> c1;; c2 \<sim> c1';; c2' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>True \<longrightarrow> (\<forall>s s'. \<Gamma>\<turnstile> \<langle>c1,s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>c1',s\<rangle> \<Rightarrow> s'); True \<longrightarrow> (\<forall>s s'. \<Gamma>\<turnstile> \<langle>c2,s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>c2',s\<rangle> \<Rightarrow> s')\<rbrakk> \<Longrightarrow> True \<longrightarrow> (\<forall>s s'. \<Gamma>\<turnstile> \<langle>c1;; c2,s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>c1';; c2',s\<rangle> \<Rightarrow> s')
theory Simpl_Rewrite

lemma com_eq_Cond:
  "\<lbrakk> c1 \<sim> c1'; c2 \<sim> c2' \<rbrakk> \<Longrightarrow> Cond b c1 c2 \<sim> Cond b c1' c2'" unfolding com_eq_def by (auto intro: exec.CondTrue exec.CondFalse elim!: exec_elim_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c1 \<sim> c1'; c2 \<sim> c2'\<rbrakk> \<Longrightarrow> Cond b c1 c2 \<sim> Cond b c1' c2' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>True \<longrightarrow> (\<forall>s s'. \<Gamma>\<turnstile> \<langle>c1,s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>c1',s\<rangle> \<Rightarrow> s'); True \<longrightarrow> (\<forall>s s'. \<Gamma>\<turnstile> \<langle>c2,s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>c2',s\<rangle> \<Rightarrow> s')\<rbrakk> \<Longrightarrow> True \<longrightarrow> (\<forall>s s'. \<Gamma>\<turnstile> \<langle>Cond b c1 c2,s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>Cond b c1' c2',s\<rangle> \<Rightarrow> s')
theory Simpl_Rewrite

lemma com_eq_While:
  "c \<sim> c' \<Longrightarrow> While b c \<sim> While b c'" by (subst com_eq_def) (auto intro: com_eq_While' com_eq_While' [OF com_eq_sym])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c \<sim> c' \<Longrightarrow> While b c \<sim> While b c'
theory Simpl_Rewrite

lemma com_eq_whileAnno:
  "c \<sim> c' \<Longrightarrow> whileAnno b I V c \<sim> whileAnno b I V c'" by (clarsimp simp: whileAnno_def elim!: com_eq_While)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c \<sim> c' \<Longrightarrow> whileAnno b I V c \<sim> whileAnno b I V c'
theory Simpl_Rewrite

lemma com_eq_Guard:
  "c \<sim> c' \<Longrightarrow> Guard f b c \<sim> Guard f b c'" by (auto simp: com_eq_def intro: exec.Guard exec.GuardFault elim!: exec_elim_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c \<sim> c' \<Longrightarrow> Guard f b c \<sim> Guard f b c'
theory Simpl_Rewrite

lemma com_eq_Catch:
  "\<lbrakk> c \<sim> c'; h \<sim> h' \<rbrakk> \<Longrightarrow> Catch c h \<sim> Catch c' h'" by (auto simp: com_eq_def intro: exec.CatchMiss exec.CatchMatch elim!: exec_elim_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<sim> c'; h \<sim> h'\<rbrakk> \<Longrightarrow> TRY c CATCH h END \<sim> TRY c' CATCH h' END
theory Simpl_Rewrite

lemma com_eq_Seq_assoc_l:
  "c1;;(c2;;c3) \<sim> (c1;;c2);;c3" by (clarsimp simp: com_eq_def exec_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c1;; (c2;; c3) \<sim> c1;; c2;; c3
theory Simpl_Rewrite

lemma com_eq_Seq_assoc_r:
  "(c1;;c2);;c3 \<sim> c1;;(c2;;c3)" by (clarsimp simp: com_eq_def exec_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c1;; c2;; c3 \<sim> c1;; (c2;; c3)
theory Simpl_Rewrite

lemma com_eq_Cond_distrib_r:
  "Cond b (c1;;c) (c2;;c) \<sim> Cond b c1 c2 ;; c" by (auto simp: com_eq_def
          intro: exec.Seq exec.CondTrue exec.CondFalse
          elim!: exec_elim_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Cond b (c1;; c) (c2;; c) \<sim> Cond b c1 c2;; c
theory Simpl_Rewrite

lemma com_eq_Guard_distrib_r:
  "Guard f b (c1;;c2) \<sim> Guard f b c1 ;; c2" by (auto simp: com_eq_def
          intro: exec.Seq exec.Guard exec.GuardFault
          elim!: exec_elim_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Guard f b (c1;; c2) \<sim> Guard f b c1;; c2
theory Simpl_Rewrite

lemma com_eq_Skip_Seq [C_simp]:
  "Skip;;c \<sim> c" apply (clarsimp simp: com_eq_def) apply (rule iffI) apply (fastforce elim!: exec_elim_cases) apply (case_tac s; (simp, (erule exec_elim_cases; simp)?)) apply (rule exec.Seq, rule exec.Skip, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. SKIP;; c \<sim> c proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<Gamma>\<turnstile> \<langle>SKIP;; c,s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> s' proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<Gamma>\<turnstile> \<langle>SKIP;; c,s\<rangle> \<Rightarrow> s' \<Longrightarrow> \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> s'
 2. \<And>s s'. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> s' \<Longrightarrow> \<Gamma>\<turnstile> \<langle>SKIP;; c,s\<rangle> \<Rightarrow> s' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> s' \<Longrightarrow> \<Gamma>\<turnstile> \<langle>SKIP;; c,s\<rangle> \<Rightarrow> s' proof (prove)
goal (1 subgoal):
 1. \<And>s s' x1. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal x1\<rangle> \<Rightarrow> s'; s = Normal x1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>SKIP;; c,Normal x1\<rangle> \<Rightarrow> s' proof (prove)
goal:
No subgoals!