theory Corres_UL_C

lemma exec_handlers_Hoare_from_vcg_fails:
  "\<lbrakk> \<Gamma> \<turnstile>\<^bsub>/F\<^esub> P c {},UNIV; UNIV \<subseteq> A \<rbrakk> \<Longrightarrow> exec_handlers_Hoare \<Gamma> P (c # cs) Q A" apply (drule hoare_sound) apply (simp add: cvalid_def HoarePartialDef.valid_def
                   exec_handlers_Hoare_def split del: if_split) apply (clarsimp split del: if_split) apply (erule exec_handlers.cases, simp_all) apply (cases cs) apply (auto elim!: exec_handlers.cases)[1] apply clarsimp apply (frule exec_handlers_Cons_le) apply auto done

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