theory CCorresLemmas

lemma exec_handlers_Hoare_from_vcg_might_fail:
  "\<lbrakk> \<Gamma> \<turnstile>\<^bsub>/F\<^esub> P c Q, A; UNIV \<subseteq> A' \<rbrakk>
    \<Longrightarrow> exec_handlers_Hoare \<Gamma> P (c # hs) Q A'" apply (clarsimp simp: exec_handlers_Hoare_def
             split del: if_split split: if_split_asm) apply (erule exec_handlers.cases; simp) apply (cases hs; simp) apply (erule exec_handlers.cases; simp) apply (frule exec_handlers_Cons_le, simp) apply (drule hoare_sound) apply (clarsimp simp: cvalid_def HoarePartialDef.valid_def) apply fastforce apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P c Q,A; UNIV \<subseteq> A'\<rbrakk> \<Longrightarrow> exec_handlers_Hoare \<Gamma> P (c # hs) Q A' proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P c Q,A; UNIV \<subseteq> A'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s\<rangle> \<Rightarrow> (length hs, Normal x); s \<in> P; x \<notin> Q\<rbrakk> \<Longrightarrow> False
 2. \<And>s n x. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P c Q,A; UNIV \<subseteq> A'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s\<rangle> \<Rightarrow> (n, Normal x); s \<in> P; n \<noteq> length hs; x \<notin> A'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s x h sa z n t. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P h Q,A; UNIV \<subseteq> A'; sa \<in> P; x \<notin> Q; s = sa; c = h; length hs = n; Normal x = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> False
 2. \<And>s x h sa t. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P h Q,A; UNIV \<subseteq> A'; sa \<in> P; x \<notin> Q; s = sa; c = h; Normal x = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> False
 3. \<And>s n x. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P c Q,A; UNIV \<subseteq> A'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s\<rangle> \<Rightarrow> (n, Normal x); s \<in> P; n \<noteq> length hs; x \<notin> A'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>s x h sa z n t. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P h Q,A; UNIV \<subseteq> A'; sa \<in> P; x \<notin> Q; s = sa; c = h; n = 0; Normal x = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>[],z\<rangle> \<Rightarrow> (0, t); hs = []\<rbrakk> \<Longrightarrow> False
 2. \<And>s x h sa z n t a list. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P h Q,A; UNIV \<subseteq> A'; sa \<in> P; x \<notin> Q; s = sa; c = h; Suc (length list) = n; Normal x = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>a # list,z\<rangle> \<Rightarrow> (n, t); hs = a # list\<rbrakk> \<Longrightarrow> False
 3. \<And>s x h sa t. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P h Q,A; UNIV \<subseteq> A'; sa \<in> P; x \<notin> Q; s = sa; c = h; Normal x = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> False
 4. \<And>s n x. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P c Q,A; UNIV \<subseteq> A'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s\<rangle> \<Rightarrow> (n, Normal x); s \<in> P; n \<noteq> length hs; x \<notin> A'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s x h sa z n t a list. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P h Q,A; UNIV \<subseteq> A'; sa \<in> P; x \<notin> Q; s = sa; c = h; Suc (length list) = n; Normal x = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>a # list,z\<rangle> \<Rightarrow> (n, t); hs = a # list\<rbrakk> \<Longrightarrow> False
 2. \<And>s x h sa t. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P h Q,A; UNIV \<subseteq> A'; sa \<in> P; x \<notin> Q; s = sa; c = h; Normal x = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> False
 3. \<And>s n x. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P c Q,A; UNIV \<subseteq> A'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s\<rangle> \<Rightarrow> (n, Normal x); s \<in> P; n \<noteq> length hs; x \<notin> A'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s x h sa t. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P h Q,A; UNIV \<subseteq> A'; sa \<in> P; x \<notin> Q; s = sa; c = h; Normal x = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> False
 2. \<And>s n x. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P c Q,A; UNIV \<subseteq> A'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s\<rangle> \<Rightarrow> (n, Normal x); s \<in> P; n \<noteq> length hs; x \<notin> A'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s x h sa t. \<lbrakk>UNIV \<subseteq> A'; sa \<in> P; x \<notin> Q; s = sa; c = h; Normal x = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t; \<Gamma>,{}\<Turnstile>\<^bsub>/F\<^esub> P h Q,A\<rbrakk> \<Longrightarrow> False
 2. \<And>s n x. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P c Q,A; UNIV \<subseteq> A'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s\<rangle> \<Rightarrow> (n, Normal x); s \<in> P; n \<noteq> length hs; x \<notin> A'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x sa. \<lbrakk>UNIV \<subseteq> A'; sa \<in> P; x \<notin> Q; \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> Normal x; \<forall>s t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<notin> Fault ` F \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` A\<rbrakk> \<Longrightarrow> False
 2. \<And>s n x. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P c Q,A; UNIV \<subseteq> A'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s\<rangle> \<Rightarrow> (n, Normal x); s \<in> P; n \<noteq> length hs; x \<notin> A'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s n x. \<lbrakk>\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P c Q,A; UNIV \<subseteq> A'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s\<rangle> \<Rightarrow> (n, Normal x); s \<in> P; n \<noteq> length hs; x \<notin> A'\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!