kings-crown/FVELER_Isabelle huggingface dataset:
theory Ctac

lemma semantic_equiv_refl:
  shows   "semantic_equiv Gamma s s' a a" by (rule semantic_equivI, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. semantic_equiv Gamma s s' a a
theory Ctac

lemma semantic_equiv_trans:
  assumes  sea: "semantic_equiv Gamma s s' a b"
  and      seb: "semantic_equiv Gamma s s' b c"
  shows   "semantic_equiv Gamma s s' a c" using sea seb by (simp add: semantic_equiv_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. semantic_equiv Gamma s s' a c proof (prove)
using this:
semantic_equiv Gamma s s' a b
semantic_equiv Gamma s s' b c

goal (1 subgoal):
 1. semantic_equiv Gamma s s' a c
theory Ctac

lemma semantic_equiv_Guard_Skip_Seq:
  shows   "semantic_equiv Gamma s s' (a ;; Guard F \<lbrace>True\<rbrace> SKIP) a" apply (rule semantic_equiv_trans) apply (rule semantic_equiv_Seq_cong) apply (rule semantic_equiv_refl) apply (rule semantic_equiv_Guard_True) apply (rule semantic_equiv_refl) apply (rule semantic_equiv_Seq_Skip) apply (rule semantic_equiv_refl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. semantic_equiv Gamma s s' (a;;
Guard F \<lbrace>True\<rbrace> SKIP) a proof (prove)
goal (2 subgoals):
 1. semantic_equiv Gamma s s' (a;;
Guard F \<lbrace>True\<rbrace> SKIP) ?b
 2. semantic_equiv Gamma s s' ?b a proof (prove)
goal (3 subgoals):
 1. \<And>s'. semantic_equiv Gamma s s' a ?a'3
 2. \<And>s. semantic_equiv Gamma s s' (Guard F \<lbrace>True\<rbrace> SKIP) ?b'3
 3. semantic_equiv Gamma s s' (?a'3;;
?b'3) a proof (prove)
goal (2 subgoals):
 1. \<And>s. semantic_equiv Gamma s s' (Guard F \<lbrace>True\<rbrace> SKIP) ?b'3
 2. semantic_equiv Gamma s s' (a;;
?b'3) a proof (prove)
goal (2 subgoals):
 1. \<And>s. semantic_equiv Gamma s s' SKIP ?b'3
 2. semantic_equiv Gamma s s' (a;;
?b'3) a proof (prove)
goal (1 subgoal):
 1. semantic_equiv Gamma s s' (a;;
SKIP) a proof (prove)
goal (1 subgoal):
 1. semantic_equiv Gamma s s' a a proof (prove)
goal:
No subgoals!
theory Ctac

lemma semantic_equiv_Seq_assoc:
  shows   "semantic_equiv Gamma s s' (a ;; (b ;; c)) (a ;; b ;; c)" apply (rule semantic_equivI) apply (rule exec_assoc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. semantic_equiv Gamma s s' (a;;
(b;;
c)) (a;;
b;;
c) proof (prove)
goal (1 subgoal):
 1. Gamma\<turnstile> \<langle>a;;
(b;;
c),Normal s\<rangle> \<Rightarrow> s' = Gamma\<turnstile> \<langle>a;;
b;;
c,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal:
No subgoals!
theory Ctac

lemma semantic_equiv_seq_assoc_eq:
  "semantic_equiv Gamma s s' (a ;; (b ;; c)) d
     = semantic_equiv Gamma s s' (a ;; b ;; c) d"
  "semantic_equiv Gamma s s' d (a ;; (b ;; c))
     = semantic_equiv Gamma s s' d (a ;; b ;; c)" by (metis semantic_equiv_trans semantic_equiv_Seq_assoc
            semantic_equiv_Seq_assoc[THEN semantic_equiv_sym[THEN iffD1]])+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. semantic_equiv Gamma s s' (a;;
(b;;
c)) d = semantic_equiv Gamma s s' (a;;
b;;
c) d &&& semantic_equiv Gamma s s' d (a;;
(b;;
c)) = semantic_equiv Gamma s s' d (a;;
b;;
c)
theory Ctac

lemma semantic_equiv_Cond_True:
  "semantic_equiv G s s' (Cond UNIV c c') c" by (auto elim!: exec_Normal_elim_cases simp: semantic_equiv_def2 intro: exec.intros)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. semantic_equiv G s s' (Cond UNIV c c') c
theory Ctac

lemma semantic_equiv_Cond_False:
  "semantic_equiv G s s' (Cond {} c c') c'" by (auto elim!: exec_Normal_elim_cases simp: semantic_equiv_def2 intro: exec.intros)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. semantic_equiv G s s' (Cond {} c c') c'
theory Ctac

lemma semantic_equiv_Cond_cases:
  "semantic_equiv G s s' a (Cond P c d)
    = semantic_equiv G s s' a (if s \<in> P then c else d)"
  "semantic_equiv G s s' (Cond P c d) e
    = semantic_equiv G s s' (if s \<in> P then c else d) e" by (auto simp: semantic_equiv_def2 elim!: exec_Normal_elim_cases intro: exec.intros)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. semantic_equiv G s s' a (Cond P c d) = semantic_equiv G s s' a (if s \<in> P then c else d) &&& semantic_equiv G s s' (Cond P c d) e = semantic_equiv G s s' (if s \<in> P then c else d) e
theory Ctac

lemma semantic_equiv_cond_seq2:
  "semantic_equiv G s s' (e;; Cond Q (c;;d) (c';;d)) (e;; Cond Q c c';; d)" apply (simp add: semantic_equiv_seq_assoc_eq[symmetric]) apply (rule semantic_equiv_Seq_cong, rule semantic_equiv_refl) by (auto simp: semantic_equiv_def2 elim!: exec_Normal_elim_cases intro: exec.intros)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. semantic_equiv G s s' (e;;
Cond Q (c;;
d) (c';;
d)) (e;;
Cond Q c c';;
d) proof (prove)
goal (1 subgoal):
 1. semantic_equiv G s s' (e;;
Cond Q (c;;
d) (c';;
d)) (e;;
(Cond Q c c';;
d)) proof (prove)
goal (1 subgoal):
 1. \<And>s. semantic_equiv G s s' (Cond Q (c;;
d) (c';;
d)) (Cond Q c c';;
d)
theory Ctac

lemma semantic_equiv_cond_seq2_seq:
  "semantic_equiv G s s' (ci;; Cond Q (c;;ce) (c';;ce);; d) (ci;; Cond Q c c';; ce;; d)" apply (simp add: semantic_equiv_seq_assoc_eq[symmetric]) apply (rule semantic_equiv_Seq_cong, rule semantic_equiv_refl) apply (simp add: semantic_equiv_seq_assoc_eq) by (auto simp: semantic_equiv_def2 elim!: exec_Normal_elim_cases intro: exec.intros)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. semantic_equiv G s s' (ci;;
Cond Q (c;;
ce) (c';;
ce);;
d) (ci;;
Cond Q c c';;
ce;;
d) proof (prove)
goal (1 subgoal):
 1. semantic_equiv G s s' (ci;;
(Cond Q (c;;
ce) (c';;
ce);;
d)) (ci;;
(Cond Q c c';;
(ce;;
d))) proof (prove)
goal (1 subgoal):
 1. \<And>s. semantic_equiv G s s' (Cond Q (c;;
ce) (c';;
ce);;
d) (Cond Q c c';;
(ce;;
d)) proof (prove)
goal (1 subgoal):
 1. \<And>s. semantic_equiv G s s' (Cond Q (c;;
ce) (c';;
ce);;
d) (Cond Q c c';;
ce;;
d)
theory Ctac

lemma ccorres_rewrite_cond_sr:
  assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> Q s \<and> s' \<in> Q' \<longrightarrow> (s' \<in> C) = (s' \<in> C') "
  and     c1: "ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs m (Cond C' c d)"
  shows   "ccorres_underlying sr \<Gamma> r xf arrel axf (P and Q) (P' \<inter> Q') hs
                              m (Cond C c d)" apply (rule ccorres_name_pre) apply (rule_tac Q="(=) s" and Q'="P' \<inter> Q' \<inter> {s'. (s, s') \<in> sr}" in stronger_ccorres_guard_imp) apply (rule ccorres_semantic_equiv[THEN iffD1, rotated]) apply (rule ccorres_guard_imp, rule c1, simp_all) apply (clarsimp simp add: semantic_equiv_Cond_cases abs semantic_equiv_refl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf (P and Q) (P' \<inter> Q') hs m (Cond C c d) proof (prove)
goal (1 subgoal):
 1. \<And>s. (P and Q) s \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (\<lambda>s'. s' = s) (P' \<inter> Q') hs m (Cond C c d) proof (prove)
goal (3 subgoals):
 1. \<And>s. (P and Q) s \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf ((=) s) (P' \<inter> Q' \<inter> {s'. (s, s') \<in> sr}) hs m (Cond C c d)
 2. \<And>s sa s'. \<lbrakk>(P and Q) s; sa = s; s' \<in> P' \<inter> Q'; (sa, s') \<in> sr\<rbrakk> \<Longrightarrow> s = sa
 3. \<And>s sa s'. \<lbrakk>(P and Q) s; sa = s; s' \<in> P' \<inter> Q'; (sa, s') \<in> sr\<rbrakk> \<Longrightarrow> s' \<in> P' \<inter> Q' \<inter> {s'. (s, s') \<in> sr} proof (prove)
goal (4 subgoals):
 1. \<And>s. (P and Q) s \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf ((=) s) (P' \<inter> Q' \<inter> {s'. (s, s') \<in> sr}) hs m (?c4 s)
 2. \<And>s sa s'. \<lbrakk>(P and Q) s; sa \<in> P' \<inter> Q' \<inter> {s'. (s, s') \<in> sr}\<rbrakk> \<Longrightarrow> semantic_equiv \<Gamma> sa s' (?c4 s) (Cond C c d)
 3. \<And>s sa s'. \<lbrakk>(P and Q) s; sa = s; s' \<in> P' \<inter> Q'; (sa, s') \<in> sr\<rbrakk> \<Longrightarrow> s = sa
 4. \<And>s sa s'. \<lbrakk>(P and Q) s; sa = s; s' \<in> P' \<inter> Q'; (sa, s') \<in> sr\<rbrakk> \<Longrightarrow> s' \<in> P' \<inter> Q' \<inter> {s'. (s, s') \<in> sr} proof (prove)
goal (1 subgoal):
 1. \<And>s sa s'. \<lbrakk>P s \<and> Q s; sa \<in> P' \<and> sa \<in> Q' \<and> (s, sa) \<in> sr\<rbrakk> \<Longrightarrow> semantic_equiv \<Gamma> sa s' (Cond C' c d) (Cond C c d) proof (prove)
goal:
No subgoals!
theory Ctac

lemma ccorres_rewrite_cond_sr_Seq:
  assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> Q s \<and> s' \<in> Q' \<longrightarrow> (s' \<in> C) = (s' \<in> C') "
  and     c1: "ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs m (Cond C' c d ;; e)"
  shows   "ccorres_underlying sr \<Gamma> r xf arrel axf (P and Q) (P' \<inter> Q') hs
                              m (Cond C c d ;; e)" apply (rule ccorres_name_pre) apply (rule_tac Q="(=) s" and Q'="P' \<inter> Q' \<inter> {s'. (s, s') \<in> sr}" in stronger_ccorres_guard_imp) apply (rule ccorres_semantic_equiv[THEN iffD1, rotated]) apply (rule ccorres_guard_imp, rule c1, simp_all) apply (rule semantic_equiv_Seq_cong) apply (clarsimp simp add: semantic_equiv_Cond_cases abs semantic_equiv_refl)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf (P and Q) (P' \<inter> Q') hs m (Cond C c d;;
e) proof (prove)
goal (1 subgoal):
 1. \<And>s. (P and Q) s \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (\<lambda>s'. s' = s) (P' \<inter> Q') hs m (Cond C c d;;
e) proof (prove)
goal (3 subgoals):
 1. \<And>s. (P and Q) s \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf ((=) s) (P' \<inter> Q' \<inter> {s'. (s, s') \<in> sr}) hs m (Cond C c d;;
e)
 2. \<And>s sa s'. \<lbrakk>(P and Q) s; sa = s; s' \<in> P' \<inter> Q'; (sa, s') \<in> sr\<rbrakk> \<Longrightarrow> s = sa
 3. \<And>s sa s'. \<lbrakk>(P and Q) s; sa = s; s' \<in> P' \<inter> Q'; (sa, s') \<in> sr\<rbrakk> \<Longrightarrow> s' \<in> P' \<inter> Q' \<inter> {s'. (s, s') \<in> sr} proof (prove)
goal (4 subgoals):
 1. \<And>s. (P and Q) s \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf ((=) s) (P' \<inter> Q' \<inter> {s'. (s, s') \<in> sr}) hs m (?c4 s)
 2. \<And>s sa s'. \<lbrakk>(P and Q) s; sa \<in> P' \<inter> Q' \<inter> {s'. (s, s') \<in> sr}\<rbrakk> \<Longrightarrow> semantic_equiv \<Gamma> sa s' (?c4 s) (Cond C c d;;
e)
 3. \<And>s sa s'. \<lbrakk>(P and Q) s; sa = s; s' \<in> P' \<inter> Q'; (sa, s') \<in> sr\<rbrakk> \<Longrightarrow> s = sa
 4. \<And>s sa s'. \<lbrakk>(P and Q) s; sa = s; s' \<in> P' \<inter> Q'; (sa, s') \<in> sr\<rbrakk> \<Longrightarrow> s' \<in> P' \<inter> Q' \<inter> {s'. (s, s') \<in> sr} proof (prove)
goal (1 subgoal):
 1. \<And>s sa s'. \<lbrakk>P s \<and> Q s; sa \<in> P' \<and> sa \<in> Q' \<and> (s, sa) \<in> sr\<rbrakk> \<Longrightarrow> semantic_equiv \<Gamma> sa s' (Cond C' c d;;
e) (Cond C c d;;
e) proof (prove)
goal (2 subgoals):
 1. \<And>s sa s' s'a. \<lbrakk>P s \<and> Q s; sa \<in> P' \<and> sa \<in> Q' \<and> (s, sa) \<in> sr\<rbrakk> \<Longrightarrow> semantic_equiv \<Gamma> sa s'a (Cond C' c d) (Cond C c d)
 2. \<And>s sa s' sb. \<lbrakk>P s \<and> Q s; sa \<in> P' \<and> sa \<in> Q' \<and> (s, sa) \<in> sr\<rbrakk> \<Longrightarrow> semantic_equiv \<Gamma> sb s' e e proof (prove)
goal:
No subgoals!
theory Ctac

lemma pis_base:
  "push_in_stmt G stmt c (c ;; stmt)" unfolding push_in_stmt_def by (clarsimp intro!: semantic_equivI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. push_in_stmt G stmt c (c;;
stmt) proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. semantic_equiv G s s' (c;;
stmt) (c;;
stmt)
theory Ctac

lemma pis_throw:
  "push_in_stmt G stmt THROW THROW" unfolding push_in_stmt_def by (auto elim!: exec_Normal_elim_cases intro: semantic_equivI exec.intros)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. push_in_stmt G stmt THROW THROW proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. semantic_equiv G s s' (THROW;;
stmt) THROW
theory Ctac

lemma pis_Seq_right:
  "push_in_stmt G stmt d d' \<Longrightarrow> push_in_stmt G stmt (c ;; d) (c ;; d')" unfolding push_in_stmt_def apply (intro allI) apply (rule semantic_equiv_trans [rotated]) apply (rule semantic_equiv_Seq_cong [OF semantic_equiv_refl]) apply (drule spec, drule spec, assumption) apply (subst semantic_equiv_sym) apply (rule semantic_equiv_Seq_assoc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. push_in_stmt G stmt d d' \<Longrightarrow> push_in_stmt G stmt (c;;
d) (c;;
d') proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. semantic_equiv G s s' (d;;
stmt) d' \<Longrightarrow> \<forall>s s'. semantic_equiv G s s' (c;;
d;;
stmt) (c;;
d') proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<forall>s s'. semantic_equiv G s s' (d;;
stmt) d' \<Longrightarrow> semantic_equiv G s s' (c;;
d;;
stmt) (c;;
d') proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<forall>s s'. semantic_equiv G s s' (d;;
stmt) d' \<Longrightarrow> semantic_equiv G s s' (?b2 s s') (c;;
d')
 2. \<And>s s'. \<forall>s s'. semantic_equiv G s s' (d;;
stmt) d' \<Longrightarrow> semantic_equiv G s s' (c;;
d;;
stmt) (?b2 s s') proof (prove)
goal (2 subgoals):
 1. \<And>s s' sa. \<forall>s s'. semantic_equiv G s s' (d;;
stmt) d' \<Longrightarrow> semantic_equiv G sa s' (?b5 s s') d'
 2. \<And>s s'. \<forall>s s'. semantic_equiv G s s' (d;;
stmt) d' \<Longrightarrow> semantic_equiv G s s' (c;;
d;;
stmt) (c;;
?b5 s s') proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<forall>s s'. semantic_equiv G s s' (d;;
stmt) d' \<Longrightarrow> semantic_equiv G s s' (c;;
d;;
stmt) (c;;
(d;;
stmt)) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<forall>s s'. semantic_equiv G s s' (d;;
stmt) d' \<Longrightarrow> semantic_equiv G s s' (c;;
(d;;
stmt)) (c;;
d;;
stmt) proof (prove)
goal:
No subgoals!
theory Ctac

lemma pis_creturn:
  "push_in_stmt G stmt (return_C xfu xf) (return_C xfu xf)" unfolding creturn_def by (rule pis_Seq_right | rule pis_throw)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. push_in_stmt G stmt (return_C xfu xf) (return_C xfu xf) proof (prove)
goal (1 subgoal):
 1. push_in_stmt G stmt (Basic (\<lambda>s. xfu (\<lambda>_. xf s) s);;
(\<acute>global_exn_var :== Return;;
THROW)) (Basic (\<lambda>s. xfu (\<lambda>_. xf s) s);;
(\<acute>global_exn_var :== Return;;
THROW))
theory Ctac

lemma pis_Cond:
  "\<lbrakk> push_in_stmt G stmt l l'; push_in_stmt G stmt r r' \<rbrakk> \<Longrightarrow>
  push_in_stmt G stmt (Cond P l r) (Cond P l' r')" unfolding push_in_stmt_def apply (intro allI) apply (drule_tac x = s in spec, drule_tac x = s' in spec)+ apply (case_tac "s \<in> P") apply (auto elim!: exec_Normal_elim_cases simp: semantic_equiv_def2 intro: exec.intros) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>push_in_stmt G stmt l l'; push_in_stmt G stmt r r'\<rbrakk> \<Longrightarrow> push_in_stmt G stmt (Cond P l r) (Cond P l' r') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s s'. semantic_equiv G s s' (l;;
stmt) l'; \<forall>s s'. semantic_equiv G s s' (r;;
stmt) r'\<rbrakk> \<Longrightarrow> \<forall>s s'. semantic_equiv G s s' (Cond P l r;;
stmt) (Cond P l' r') proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<forall>s s'. semantic_equiv G s s' (l;;
stmt) l'; \<forall>s s'. semantic_equiv G s s' (r;;
stmt) r'\<rbrakk> \<Longrightarrow> semantic_equiv G s s' (Cond P l r;;
stmt) (Cond P l' r') proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>semantic_equiv G s s' (l;;
stmt) l'; semantic_equiv G s s' (r;;
stmt) r'\<rbrakk> \<Longrightarrow> semantic_equiv G s s' (Cond P l r;;
stmt) (Cond P l' r') proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>semantic_equiv G s s' (l;;
stmt) l'; semantic_equiv G s s' (r;;
stmt) r'; s \<in> P\<rbrakk> \<Longrightarrow> semantic_equiv G s s' (Cond P l r;;
stmt) (Cond P l' r')
 2. \<And>s s'. \<lbrakk>semantic_equiv G s s' (l;;
stmt) l'; semantic_equiv G s s' (r;;
stmt) r'; s \<notin> P\<rbrakk> \<Longrightarrow> semantic_equiv G s s' (Cond P l r;;
stmt) (Cond P l' r') proof (prove)
goal:
No subgoals!
theory Ctac

lemma pis_switch_Cons:
  "\<lbrakk> push_in_stmt G stmt c c';
     push_in_stmt G stmt (switch v (x # xs)) (switch v cs)   \<rbrakk>
   \<Longrightarrow> push_in_stmt G stmt (switch v ((g, c) # (x # xs))) (switch v ((g, c') # cs))" by (simp add: pis_Cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>push_in_stmt G stmt c c'; push_in_stmt G stmt (switch v (x # xs)) (switch v cs)\<rbrakk> \<Longrightarrow> push_in_stmt G stmt (switch v ((g, c) # x # xs)) (switch v ((g, c') # cs))
theory Ctac

lemma pis_switch_Singleton:
  "\<lbrakk> push_in_stmt G stmt c c' \<rbrakk> \<Longrightarrow> push_in_stmt G stmt (switch v [(UNIV, c)]) (switch v [(UNIV, c')])" apply (clarsimp simp: push_in_stmt_def) apply (rule semantic_equiv_trans [OF _ iffD2 [OF semantic_equiv_sym, OF semantic_equiv_Cond_True]]) apply (rule semantic_equiv_trans [rotated]) apply (drule spec, drule spec, assumption) apply (rule semantic_equiv_Seq_cong [OF semantic_equiv_Cond_True semantic_equiv_refl]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. push_in_stmt G stmt c c' \<Longrightarrow> push_in_stmt G stmt (switch v [(UNIV, c)]) (switch v [(UNIV, c')]) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<forall>s s'. semantic_equiv G s s' (c;;
stmt) c' \<Longrightarrow> semantic_equiv G s s' (Cond UNIV c SKIP;;
stmt) (Cond UNIV c' SKIP) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<forall>s s'. semantic_equiv G s s' (c;;
stmt) c' \<Longrightarrow> semantic_equiv G s s' (Cond UNIV c SKIP;;
stmt) c' proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<forall>s s'. semantic_equiv G s s' (c;;
stmt) c' \<Longrightarrow> semantic_equiv G s s' (?b8 s s') c'
 2. \<And>s s'. \<forall>s s'. semantic_equiv G s s' (c;;
stmt) c' \<Longrightarrow> semantic_equiv G s s' (Cond UNIV c SKIP;;
stmt) (?b8 s s') proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<forall>s s'. semantic_equiv G s s' (c;;
stmt) c' \<Longrightarrow> semantic_equiv G s s' (Cond UNIV c SKIP;;
stmt) (c;;
stmt) proof (prove)
goal:
No subgoals!
theory Ctac

lemma pis_Guard:
  "push_in_stmt G stmt c c' \<Longrightarrow> push_in_stmt G stmt (Guard f G' c) (Guard f G' c')" unfolding push_in_stmt_def apply (intro allI) apply (rule semantic_equiv_trans [OF Guard_Seq_semantic_equiv]) apply (rule semantic_equiv_Guard_cong) apply (drule spec, erule spec) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. push_in_stmt G stmt c c' \<Longrightarrow> push_in_stmt G stmt (Guard f G' c) (Guard f G' c') proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. semantic_equiv G s s' (c;;
stmt) c' \<Longrightarrow> \<forall>s s'. semantic_equiv G s s' (Guard f G' c;;
stmt) (Guard f G' c') proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<forall>s s'. semantic_equiv G s s' (c;;
stmt) c' \<Longrightarrow> semantic_equiv G s s' (Guard f G' c;;
stmt) (Guard f G' c') proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<forall>s s'. semantic_equiv G s s' (c;;
stmt) c' \<Longrightarrow> semantic_equiv G s s' (Guard f G' (c;;
stmt)) (Guard f G' c') proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<forall>s s'. semantic_equiv G s s' (c;;
stmt) c' \<Longrightarrow> semantic_equiv G s s' (c;;
stmt) c' proof (prove)
goal:
No subgoals!
theory Ctac

lemma ccorres_special_trim_guard_DontReach_pis:
  assumes at: "push_in_stmt Gamma (Guard DontReach {} c) b b'"
  and      c: "ccorres_underlying sr Gamma r xf ar axf G G' hs a b'"
  shows   "ccorres_underlying sr Gamma r xf ar axf G G' hs a (b ;; Guard DontReach {} c)" using c at unfolding push_in_stmt_def apply - apply (erule ccorres_semantic_equivD2) apply (drule spec, erule spec) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr Gamma r xf ar axf G G' hs a (b;;
Guard DontReach {} c) proof (prove)
using this:
ccorres_underlying sr Gamma r xf ar axf G G' hs a b'
push_in_stmt Gamma (Guard DontReach {} c) b b'

goal (1 subgoal):
 1. ccorres_underlying sr Gamma r xf ar axf G G' hs a (b;;
Guard DontReach {} c) proof (prove)
using this:
ccorres_underlying sr Gamma r xf ar axf G G' hs a b'
\<forall>s s'. semantic_equiv Gamma s s' (b;;
Guard DontReach {} c) b'

goal (1 subgoal):
 1. ccorres_underlying sr Gamma r xf ar axf G G' hs a (b;;
Guard DontReach {} c) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccorres_underlying sr Gamma r xf ar axf G G' hs a b'; \<forall>s s'. semantic_equiv Gamma s s' (b;;
Guard DontReach {} c) b'\<rbrakk> \<Longrightarrow> ccorres_underlying sr Gamma r xf ar axf G G' hs a (b;;
Guard DontReach {} c) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<forall>s s'. semantic_equiv Gamma s s' (b;;
Guard DontReach {} c) b'; s \<in> G'\<rbrakk> \<Longrightarrow> semantic_equiv Gamma s s' (b;;
Guard DontReach {} c) b' proof (prove)
goal:
No subgoals!
theory Ctac

lemma rewrite_xfI:
  "(xf t = v \<Longrightarrow> f t = f' t) \<Longrightarrow> rewrite_xf xf t v f f'" unfolding rewrite_xf_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (xf t = v \<Longrightarrow> f t = f' t) \<Longrightarrow> rewrite_xf xf t v f f' proof (prove)
goal (1 subgoal):
 1. (xf t = v \<Longrightarrow> f t = f' t) \<Longrightarrow> xf t = v \<longrightarrow> f t = f' t
theory Ctac

lemma rewrite_xfD:
  "\<lbrakk> rewrite_xf xf t v f f'; xf t = v \<rbrakk> \<Longrightarrow> f t = f' t" unfolding rewrite_xf_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rewrite_xf xf t v f f'; xf t = v\<rbrakk> \<Longrightarrow> f t = f' t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xf t = v \<longrightarrow> f t = f' t; xf t = v\<rbrakk> \<Longrightarrow> f t = f' t