kings-crown/FVELER_Isabelle huggingface dataset:
theory Simpl_Rewrite

lemma com_eq_Seq_Skip [C_simp]:
  "c;;Skip \<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, simp) apply (case_tac s'; (simp, (erule exec_elim_cases; simp)?)) apply (rule exec.Skip) done

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

lemma com_eq_Cond_empty [C_simp_pre]:
  "com_eq (b = {}) (Cond b c1 c2) c2" by (clarsimp simp: com_eq_def, case_tac s, auto intro: exec.CondFalse elim!: exec_elim_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. local.com_eq (b = {}) (Cond b c1 c2) c2
theory Simpl_Rewrite

lemma com_eq_Cond_UNIV [C_simp_pre]:
  "com_eq (b = UNIV) (Cond b c1 c2) c1" by (clarsimp simp: com_eq_def, case_tac s, auto intro: exec.CondTrue  elim!: exec_elim_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. local.com_eq (b = UNIV) (Cond b c1 c2) c1
theory Simpl_Rewrite

lemma exec_Cond_cases:
  "\<lbrakk>s \<in> b \<Longrightarrow> \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow>
  \<Gamma>\<turnstile> \<langle>Cond b c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow> t" by (cases "s \<in> b") (auto intro: exec.CondTrue exec.CondFalse)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<in> b \<Longrightarrow> \<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; s \<notin> b \<Longrightarrow> \<Gamma>\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond b c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow> t
theory Simpl_Rewrite

lemma com_eq_Cond_both [C_simp]:
  "Cond b c c \<sim> c" by (clarsimp simp: com_eq_def, case_tac s, auto intro: exec_Cond_cases elim!: exec_elim_cases)

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

lemma com_eq_While_empty [C_simp_pre]:
  "com_eq (b = {}) (While b c) Skip" by (auto simp: com_eq_def intro: exec.WhileFalse exec.Skip elim!: exec_elim_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. local.com_eq (b = {}) (While b c) SKIP
theory Simpl_Rewrite

lemma com_eq_whileAnno_empty [C_simp_pre]:
  "com_eq (b = {}) (whileAnno b I V c) Skip" by (simp add: com_eq_While_empty whileAnno_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. local.com_eq (b = {}) (whileAnno b I V c) SKIP
theory Simpl_Rewrite

lemma com_eq_Guard_UNIV [C_simp_pre]:
  "com_eq (b = UNIV) (Guard f b c) c" by (clarsimp simp: com_eq_def, case_tac s, auto intro: exec.Guard elim!: exec_elim_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. local.com_eq (b = UNIV) (Guard f b c) c
theory Simpl_Rewrite

lemma com_eq_Guard_empty [C_simp_pre]:
  "com_eq (c \<noteq> Skip \<and> b = {}) (Guard f b c) (Guard f {} Skip)" by (clarsimp simp: com_eq_def, case_tac s, auto intro: exec.GuardFault elim!: exec_elim_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. local.com_eq (c \<noteq> SKIP \<and> b = {}) (Guard f b c) (Guard f {} SKIP)
theory Simpl_Rewrite

lemma com_eq_Catch_Skip [C_simp]:
  "Catch Skip c \<sim> Skip" by (auto simp: com_eq_def intro: exec.CatchMiss exec.Skip elim!: exec_elim_cases)

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

lemma com_eq_Catch_Throw [C_simp]:
  "Catch Throw c \<sim> c" by (clarsimp simp: com_eq_def, case_tac s)
     (auto intro: exec.CatchMatch exec.Throw elim!: exec_elim_cases)

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

lemma never_continues_rewrite_com_eq:
  "c \<sim> c' \<Longrightarrow> never_continues_if t c \<Longrightarrow> never_continues_if t c'" apply (simp add: never_continues_def2) apply (elim imp_forward all_forward, assumption) apply (rule com_eq_trans, rule com_eq_Seq, erule com_eq_sym, rule com_eq_refl) by (erule com_eq_trans[rotated])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<sim> c'; local.never_continues_if t c\<rbrakk> \<Longrightarrow> local.never_continues_if t c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<sim> c'; t \<longrightarrow> (\<forall>r. c;; r \<sim> c)\<rbrakk> \<Longrightarrow> t \<longrightarrow> (\<forall>r. c';; r \<sim> c') proof (prove)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>c \<sim> c'; c;; r \<sim> c\<rbrakk> \<Longrightarrow> c';; r \<sim> c' proof (prove)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>c \<sim> c'; c;; r \<sim> c\<rbrakk> \<Longrightarrow> c;; r \<sim> c'
theory Simpl_Rewrite

lemma never_continues_Throw [C_simp_throws]:
  "never_continues Throw" by (auto simp: never_continues_def elim: exec_elim_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. local.never_continues THROW
theory Simpl_Rewrite

lemma While_UNIV_helper:
  "\<Gamma> \<turnstile> \<langle>c',s\<rangle> \<Rightarrow> s'' \<Longrightarrow> c' = While UNIV c \<Longrightarrow> s'' = Normal s' \<Longrightarrow> False" by (induct rule: exec.induct) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile> \<langle>c',s\<rangle> \<Rightarrow> s''; c' = While UNIV c; s'' = Normal s'\<rbrakk> \<Longrightarrow> False
theory Simpl_Rewrite

lemma never_continues_While_UNIV [C_simp_throws]:
  "never_continues (While UNIV c)" by (auto simp: never_continues_def elim: While_UNIV_helper)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. local.never_continues (While UNIV c)
theory Simpl_Rewrite

lemma never_continues_While_True [C_simp_throws]:
  "never_continues (WHILE True DO c OD)" by (simp add: whileAnno_def never_continues_While_UNIV)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. local.never_continues (WHILE True DO c OD)
theory Simpl_Rewrite

lemma never_continues_Guard_False [C_simp_throws]:
  "never_continues (Guard f {} c)" by (auto simp: never_continues_def elim: exec_elim_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. local.never_continues (Guard f {} c)
theory Simpl_Rewrite

lemma never_continues_Seq1:
  "never_continues_if t c1 \<Longrightarrow> never_continues_if t (c1;;c2)" apply (clarsimp simp: never_continues_def2) apply (frule spec[of _ c2], erule com_eq_trans[rotated, OF com_eq_sym]) apply (rule com_eq_trans[OF com_eq_Seq_assoc_r]) by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. local.never_continues_if t c1 \<Longrightarrow> local.never_continues_if t (c1;; c2) proof (prove)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>t; \<forall>r. c1;; r \<sim> c1\<rbrakk> \<Longrightarrow> c1;; c2;; r \<sim> c1;; c2 proof (prove)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>t; \<forall>r. c1;; r \<sim> c1\<rbrakk> \<Longrightarrow> c1;; c2;; r \<sim> c1 proof (prove)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>t; \<forall>r. c1;; r \<sim> c1\<rbrakk> \<Longrightarrow> c1;; (c2;; r) \<sim> c1
theory Simpl_Rewrite

lemma never_continues_Seq2:
  "never_continues_if t c2 \<Longrightarrow> never_continues_if t (c1;;c2)" apply (clarsimp simp: never_continues_def2) apply (rule com_eq_trans[OF com_eq_Seq_assoc_r]) apply (rule com_eq_Seq[OF com_eq_refl]) by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. local.never_continues_if t c2 \<Longrightarrow> local.never_continues_if t (c1;; c2) proof (prove)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>t; \<forall>r. c2;; r \<sim> c2\<rbrakk> \<Longrightarrow> c1;; c2;; r \<sim> c1;; c2 proof (prove)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>t; \<forall>r. c2;; r \<sim> c2\<rbrakk> \<Longrightarrow> c1;; (c2;; r) \<sim> c1;; c2 proof (prove)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>t; \<forall>r. c2;; r \<sim> c2\<rbrakk> \<Longrightarrow> c2;; r \<sim> c2
theory Simpl_Rewrite

lemma never_continues_Cond:
  "never_continues_if t1 c1 \<Longrightarrow> never_continues_if t2 c2 \<Longrightarrow> never_continues_if (t1 \<and> t2) (Cond b c1 c2)" by (auto simp: never_continues_def elim: exec_elim_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>local.never_continues_if t1 c1; local.never_continues_if t2 c2\<rbrakk> \<Longrightarrow> local.never_continues_if (t1 \<and> t2) (Cond b c1 c2)
theory Simpl_Rewrite

lemma never_continues_Guard:
  "never_continues_if t c \<Longrightarrow> never_continues_if t (Guard f b c)" by (auto simp: never_continues_def elim: exec_elim_cases)

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

lemma never_continues_Catch:
  "never_continues_if tc c \<Longrightarrow> never_continues_if th h \<Longrightarrow> never_continues_if (tc \<and> th) (Catch c h)" by (auto simp: never_continues_def elim: exec_elim_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>local.never_continues_if tc c; local.never_continues_if th h\<rbrakk> \<Longrightarrow> local.never_continues_if (tc \<and> th) (TRY c CATCH h END)
theory Simpl_Rewrite

lemma never_continues_False:
  "never_continues_if False c" by (simp add: never_continues_def)

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

lemma com_eq_homD:
  "c \<sim> c' \<Longrightarrow> P c' \<longrightarrow> P c" using com_eq_hom by (simp add: com_eq_hom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c \<sim> c' \<Longrightarrow> P c' \<longrightarrow> P c proof (prove)
using this:
local.com_eq_hom P

goal (1 subgoal):
 1. c \<sim> c' \<Longrightarrow> P c' \<longrightarrow> P c
theory Simpl_Rewrite

lemma never_continues_opt_None:
  "never_continues_opt None t" by (simp add: never_continues_opt_def never_continues_False)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. local.never_continues_opt None t
theory Simpl_Rewrite

lemma com_ctxt_focus_enter:
  "com_ctxt_focus c None [] \<Longrightarrow> P c" by (simp add: com_ctxt_focus_defs never_continues_False)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. local.com_ctxt_focus c None [] \<Longrightarrow> P c
theory Simpl_Rewrite

lemma com_ctxt_focus_exit:
  "P c \<Longrightarrow> com_ctxt_focus c t []" by (simp add: com_ctxt_focus_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P c \<Longrightarrow> local.com_ctxt_focus c t []
theory Simpl_Rewrite

lemma nc_opt_rewrite_com_eq:
  "c \<sim> c' \<Longrightarrow> never_continues_opt t c \<Longrightarrow> never_continues_opt t c'" by (simp add: never_continues_opt_def never_continues_rewrite_com_eq)

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

lemma ctxt_P_rewrite_com_eq:
  "c \<sim> c' \<Longrightarrow> com_ctxt_P c' cs \<Longrightarrow> com_ctxt_P c cs" proof (induct cs arbitrary: c c') case Nil thus ?case by (simp add: com_eq_homD) next case (Cons c'' cs) show ?case using Cons.prems(2) by (cases c''; clarsimp elim!: Cons.hyps[rotated];
          intro com_eq_intros com_eq_refl Cons.prems(1)) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<sim> c'; local.com_ctxt_P c' cs\<rbrakk> \<Longrightarrow> local.com_ctxt_P c cs proof (state)
goal (2 subgoals):
 1. \<And>c c'. \<lbrakk>c \<sim> c'; local.com_ctxt_P c' []\<rbrakk> \<Longrightarrow> local.com_ctxt_P c []
 2. \<And>a cs c c'. \<lbrakk>\<And>c c'. \<lbrakk>c \<sim> c'; local.com_ctxt_P c' cs\<rbrakk> \<Longrightarrow> local.com_ctxt_P c cs; c \<sim> c'; local.com_ctxt_P c' (a # cs)\<rbrakk> \<Longrightarrow> local.com_ctxt_P c (a # cs) proof (state)
this:
c \<sim> c'
local.com_ctxt_P c' []

goal (2 subgoals):
 1. \<And>c c'. \<lbrakk>c \<sim> c'; local.com_ctxt_P c' []\<rbrakk> \<Longrightarrow> local.com_ctxt_P c []
 2. \<And>a cs c c'. \<lbrakk>\<And>c c'. \<lbrakk>c \<sim> c'; local.com_ctxt_P c' cs\<rbrakk> \<Longrightarrow> local.com_ctxt_P c cs; c \<sim> c'; local.com_ctxt_P c' (a # cs)\<rbrakk> \<Longrightarrow> local.com_ctxt_P c (a # cs) proof (prove)
using this:
c \<sim> c'
local.com_ctxt_P c' []

goal (1 subgoal):
 1. local.com_ctxt_P c [] proof (state)
this:
local.com_ctxt_P c []

goal (1 subgoal):
 1. \<And>a cs c c'. \<lbrakk>\<And>c c'. \<lbrakk>c \<sim> c'; local.com_ctxt_P c' cs\<rbrakk> \<Longrightarrow> local.com_ctxt_P c cs; c \<sim> c'; local.com_ctxt_P c' (a # cs)\<rbrakk> \<Longrightarrow> local.com_ctxt_P c (a # cs) proof (state)
goal (1 subgoal):
 1. \<And>a cs c c'. \<lbrakk>\<And>c c'. \<lbrakk>c \<sim> c'; local.com_ctxt_P c' cs\<rbrakk> \<Longrightarrow> local.com_ctxt_P c cs; c \<sim> c'; local.com_ctxt_P c' (a # cs)\<rbrakk> \<Longrightarrow> local.com_ctxt_P c (a # cs) proof (state)
this:
\<lbrakk>?c \<sim> ?c'; local.com_ctxt_P ?c' cs\<rbrakk> \<Longrightarrow> local.com_ctxt_P ?c cs
c \<sim> c'
local.com_ctxt_P c' (c'' # cs)

goal (1 subgoal):
 1. \<And>a cs c c'. \<lbrakk>\<And>c c'. \<lbrakk>c \<sim> c'; local.com_ctxt_P c' cs\<rbrakk> \<Longrightarrow> local.com_ctxt_P c cs; c \<sim> c'; local.com_ctxt_P c' (a # cs)\<rbrakk> \<Longrightarrow> local.com_ctxt_P c (a # cs) proof (prove)
goal (1 subgoal):
 1. local.com_ctxt_P c (c'' # cs) proof (prove)
using this:
local.com_ctxt_P c' (c'' # cs)

goal (1 subgoal):
 1. local.com_ctxt_P c (c'' # cs) proof (state)
this:
local.com_ctxt_P c (c'' # cs)

goal:
No subgoals!
theory Simpl_Rewrite

lemma com_ctxt_focus_rewrite:
  "com_eq p c c' \<Longrightarrow> p \<Longrightarrow> com_ctxt_focus c' t cs \<Longrightarrow> com_ctxt_focus c t cs" by (simp add: com_ctxt_focus_def nc_opt_rewrite_com_eq ctxt_P_rewrite_com_eq)

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

lemma com_ctxt_focus_set_never_continues:
  "never_continues_if t c \<Longrightarrow> com_ctxt_focus c (Some t) cs \<Longrightarrow> com_ctxt_focus c None cs" by (simp add: com_ctxt_focus_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>local.never_continues_if t c; local.com_ctxt_focus c (Some t) cs\<rbrakk> \<Longrightarrow> local.com_ctxt_focus c None cs
theory Simpl_Rewrite

lemma com_ctxt_focus_update_never_continues:
  "never_continues_if t c \<Longrightarrow> com_ctxt_focus c (Some (t \<or> t')) cs \<Longrightarrow> com_ctxt_focus c (Some t') cs" by (cases t; cases t'; simp add: com_ctxt_focus_defs)

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

lemma com_ctxt_focus_left:
  "com_ctxt_focus c None (Seq1C c' # cs) \<Longrightarrow> com_ctxt_focus (Seq c c') None cs"
  "com_ctxt_focus c None (CondTC b c' # cs) \<Longrightarrow> com_ctxt_focus (Cond b c c') None cs"
  "com_ctxt_focus c None (WhileC b # cs) \<Longrightarrow> com_ctxt_focus (While b c) None cs"
  "com_ctxt_focus c None (WhileAnnoC b I V # cs) \<Longrightarrow> com_ctxt_focus (whileAnno b I V c) None cs"
  "com_ctxt_focus c None (GuardC f b # cs) \<Longrightarrow> com_ctxt_focus (Guard f b c) None cs"
  "com_ctxt_focus c None (TryC c' # cs) \<Longrightarrow> com_ctxt_focus (Catch c c') None cs" by (auto simp: com_ctxt_focus_def never_continues_opt_None)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((local.com_ctxt_focus c None (Seq1C c' # cs) \<Longrightarrow> local.com_ctxt_focus (c;; c') None cs) &&& (local.com_ctxt_focus c None (CondTC b c' # cs) \<Longrightarrow> local.com_ctxt_focus (Cond b c c') None cs) &&& (local.com_ctxt_focus c None (WhileC b # cs) \<Longrightarrow> local.com_ctxt_focus (While b c) None cs)) &&& (local.com_ctxt_focus c None (WhileAnnoC b I V # cs) \<Longrightarrow> local.com_ctxt_focus (whileAnno b I V c) None cs) &&& (local.com_ctxt_focus c None (GuardC f b # cs) \<Longrightarrow> local.com_ctxt_focus (Guard f b c) None cs) &&& (local.com_ctxt_focus c None (TryC c' # cs) \<Longrightarrow> local.com_ctxt_focus (TRY c CATCH c' END) None cs)
theory Simpl_Rewrite

lemma com_ctxt_focus_right:
  "com_ctxt_focus c' None (Seq2C c # cs) \<Longrightarrow> com_ctxt_focus c (Some False) (Seq1C c' # cs)"
  "com_ctxt_focus c' None (CondFC b c t # cs) \<Longrightarrow> com_ctxt_focus c (Some t) (CondTC b c' # cs)"
  "com_ctxt_focus c' None (HandlerC c t # cs) \<Longrightarrow> com_ctxt_focus c (Some t) (TryC c' # cs)" by (auto simp: com_ctxt_focus_defs never_continues_False)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (local.com_ctxt_focus c' None (Seq2C c # cs) \<Longrightarrow> local.com_ctxt_focus c (Some False) (Seq1C c' # cs)) &&& (local.com_ctxt_focus c' None (CondFC b c t # cs) \<Longrightarrow> local.com_ctxt_focus c (Some t) (CondTC b c' # cs)) &&& (local.com_ctxt_focus c' None (HandlerC c t # cs) \<Longrightarrow> local.com_ctxt_focus c (Some t) (TryC c' # cs))
theory Simpl_Rewrite

lemma com_ctxt_P_Seq1:
  "never_continues c \<Longrightarrow> com_ctxt_P c cs \<Longrightarrow> com_ctxt_P (Seq c c') cs" by (auto simp: never_continues_def2 elim: ctxt_P_rewrite_com_eq)

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

lemma com_ctxt_unfocus_simple:
  "com_ctxt_focus c (Some True) cs \<Longrightarrow> com_ctxt_focus c (Some True) (Seq1C c' # cs)"
  "com_ctxt_focus (Seq c' c) (Some t) cs \<Longrightarrow> com_ctxt_focus c (Some t) (Seq2C c' # cs)"
  "com_ctxt_focus (While b c) (Some False) cs \<Longrightarrow> com_ctxt_focus c (Some t) (WhileC b # cs)"
  "com_ctxt_focus (whileAnno b I V c) (Some False) cs \<Longrightarrow> com_ctxt_focus c (Some t) (WhileAnnoC b I V # cs)"
  "com_ctxt_focus (Guard f b c) (Some t) cs \<Longrightarrow> com_ctxt_focus c (Some t) (GuardC f b # cs)" by (auto simp: com_ctxt_focus_defs never_continues_False com_ctxt_P_Seq1 never_continues_Seq2 never_continues_Guard)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((local.com_ctxt_focus c (Some True) cs \<Longrightarrow> local.com_ctxt_focus c (Some True) (Seq1C c' # cs)) &&& (local.com_ctxt_focus (c';; c) (Some t) cs \<Longrightarrow> local.com_ctxt_focus c (Some t) (Seq2C c' # cs))) &&& (local.com_ctxt_focus (While b c) (Some False) cs \<Longrightarrow> local.com_ctxt_focus c (Some t) (WhileC b # cs)) &&& (local.com_ctxt_focus (whileAnno b I V c) (Some False) cs \<Longrightarrow> local.com_ctxt_focus c (Some t) (WhileAnnoC b I V # cs)) &&& (local.com_ctxt_focus (Guard f b c) (Some t) cs \<Longrightarrow> local.com_ctxt_focus c (Some t) (GuardC f b # cs))
theory Simpl_Rewrite

lemma com_ctxt_unfocus_complex:
  "com_ctxt_focus (Cond b c' c) (Some (t' \<and> t)) cs \<Longrightarrow> com_ctxt_focus c (Some t) (CondFC b c' t' # cs)"
  "com_ctxt_focus (Catch c' c) (Some (t' \<and> t)) cs \<Longrightarrow> com_ctxt_focus c (Some t) (HandlerC c' t' # cs)" by (auto simp: com_ctxt_focus_defs never_continues_False never_continues_Cond never_continues_Catch)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (local.com_ctxt_focus (Cond b c' c) (Some (t' \<and> t)) cs \<Longrightarrow> local.com_ctxt_focus c (Some t) (CondFC b c' t' # cs)) &&& (local.com_ctxt_focus (TRY c' CATCH c END) (Some (t' \<and> t)) cs \<Longrightarrow> local.com_ctxt_focus c (Some t) (HandlerC c' t' # cs))
theory CCorres_Rewrite

lemma ccorres_com_eq_hom:
  "com_eq_hom \<Gamma> (ccorres_underlying sr \<Gamma> r xf r' xf' P P' hs H)" by (auto simp: com_eq_hom_def com_eq_def semantic_equiv_def ceqv_def
           elim: ccorres_semantic_equivD2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. com_eq_hom \<Gamma> (ccorres_underlying sr \<Gamma> r xf r' xf' P P' hs H)
theory CCorres_Rewrite

lemma hoarep_com_eq_hom:
  "com_eq_hom \<Gamma> (\<lambda>c. hoarep \<Gamma> {} F P c Q A)" by (auto simp: com_eq_hom_def com_eq_def ceqv_def
           elim: exec_eq_is_valid_eq0[rotated])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. com_eq_hom \<Gamma> (\<lambda>c. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> P c Q,A)
theory CCorres_Rewrite

lemma hoarep_spec_com_eq_hom:
  "com_eq_hom \<Gamma> (\<lambda>c. \<forall>s. hoarep \<Gamma> {} (F s) (P s) c (Q s) (A s))" by (fastforce simp: com_eq_hom_def com_eq_def ceqv_def
                elim: exec_eq_is_valid_eq0[rotated])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. com_eq_hom \<Gamma> (\<lambda>c. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/F s\<^esub> (P s) c (Q s),(A s))
theory CCorresLemmas

lemma ccorres_nohs:
  "ccorres_underlying sr \<Gamma> r xf r xf P P' [] a b
      \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs a b" apply (rule ccorres_handlers_weaken) apply (erule ccorres_rel_imp2, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorresG sr \<Gamma> r xf P P' [] a b \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs a b proof (prove)
goal (1 subgoal):
 1. ccorresG sr \<Gamma> r xf P P' [] a b \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' [] a b proof (prove)
goal:
No subgoals!
theory CCorresLemmas

lemma ccorres_liftE_Seq:
  assumes cc: "ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs (a >>= b) (c ;; d)"
  shows   "ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs (liftE a >>=E b) (c ;; d)" apply (simp add: liftE_bindE cc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs (liftE a >>=E b) (c;;
d) proof (prove)
goal:
No subgoals!