theory CCorresLemmas

lemma exec_handlers_Hoare_call_Basic:
  "\<lbrakk> \<forall>s' t x. s' \<in> P \<longrightarrow> g s' t (ret s' t) \<in> Q; UNIV \<subseteq> A \<rbrakk> \<Longrightarrow>
    exec_handlers_Hoare \<Gamma> P (call initfn p ret (\<lambda>x y. Basic (g x y)) # hs) Q A" apply (clarsimp simp: exec_handlers_Hoare_def
             split del: if_split) apply (erule exec_handlers.cases) apply clarsimp apply (erule exec_call_Normal_elim, simp_all)[1] apply (auto elim!: exec_Normal_elim_cases)[1] apply (frule exec_handlers_less2, clarsimp+) apply (clarsimp simp: subset_iff split: if_split_asm) apply (auto elim!: exec_Normal_elim_cases
                      exec_call_Normal_elim) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s' t x. s' \<in> P \<longrightarrow> g s' t (ret s' t) \<in> Q; UNIV \<subseteq> A\<rbrakk> \<Longrightarrow> exec_handlers_Hoare \<Gamma> P (call initfn p ret (\<lambda>x y. Basic (g x y)) # hs) Q A proof (prove)
goal (1 subgoal):
 1. \<And>s n x. \<lbrakk>\<forall>s'. s' \<in> P \<longrightarrow> (\<forall>t. g s' t (ret s' t) \<in> Q); UNIV \<subseteq> A; \<Gamma>\<turnstile>\<^sub>h \<langle>call initfn p ret (\<lambda>x y. Basic (g x y)) # hs,s\<rangle> \<Rightarrow> (n, Normal x); s \<in> P; x \<in> (if n = length hs then - Q else - A)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s n x h sa z hsa na t. \<lbrakk>\<forall>s'. s' \<in> P \<longrightarrow> (\<forall>t. g s' t (ret s' t) \<in> Q); UNIV \<subseteq> A; s \<in> P; x \<in> (if n = length hs then - Q else - A); s = sa; call initfn p ret (\<lambda>x y. Basic (g x y)) # hs = h # hsa; n = na; Normal x = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hsa,z\<rangle> \<Rightarrow> (na, t)\<rbrakk> \<Longrightarrow> False
 2. \<And>s n x h sa t hsa. \<lbrakk>\<forall>s'. s' \<in> P \<longrightarrow> (\<forall>t. g s' t (ret s' t) \<in> Q); UNIV \<subseteq> A; s \<in> P; x \<in> (if n = length hs then - Q else - A); s = sa; call initfn p ret (\<lambda>x y. Basic (g x y)) # hs = h # hsa; n = length hsa; Normal x = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> False
 3. \<And>s n x sa. \<lbrakk>\<forall>s'. s' \<in> P \<longrightarrow> (\<forall>t. g s' t (ret s' t) \<in> Q); UNIV \<subseteq> A; s \<in> P; x \<in> (if n = length hs then - Q else - A); s = sa; call initfn p ret (\<lambda>x y. Basic (g x y)) # hs = []; n = 0; Normal x = Abrupt sa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>x sa z na. \<lbrakk>\<forall>s'. s' \<in> P \<longrightarrow> (\<forall>t. g s' t (ret s' t) \<in> Q); UNIV \<subseteq> A; sa \<in> P; x \<in> (if na = length hs then - Q else - A); \<Gamma>\<turnstile> \<langle>call initfn p ret (\<lambda>x y. Basic (g x y)),Normal sa\<rangle> \<Rightarrow> Abrupt z; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (na, Normal x)\<rbrakk> \<Longrightarrow> False
 2. \<And>s n x h sa t hsa. \<lbrakk>\<forall>s'. s' \<in> P \<longrightarrow> (\<forall>t. g s' t (ret s' t) \<in> Q); UNIV \<subseteq> A; s \<in> P; x \<in> (if n = length hs then - Q else - A); s = sa; call initfn p ret (\<lambda>x y. Basic (g x y)) # hs = h # hsa; n = length hsa; Normal x = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> False
 3. \<And>s n x sa. \<lbrakk>\<forall>s'. s' \<in> P \<longrightarrow> (\<forall>t. g s' t (ret s' t) \<in> Q); UNIV \<subseteq> A; s \<in> P; x \<in> (if n = length hs then - Q else - A); s = sa; call initfn p ret (\<lambda>x y. Basic (g x y)) # hs = []; n = 0; Normal x = Abrupt sa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>x sa z na bdy t'. \<lbrakk>\<forall>s'. s' \<in> P \<longrightarrow> (\<forall>t. g s' t (ret s' t) \<in> Q); UNIV \<subseteq> A; sa \<in> P; x \<in> (if na = length hs then - Q else - A); \<Gamma>\<turnstile>\<^sub>h \<langle>hs,z\<rangle> \<Rightarrow> (na, Normal x); \<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (initfn sa)\<rangle> \<Rightarrow> Normal t'; \<Gamma>\<turnstile> \<langle>Basic (g sa t'),Normal (ret sa t')\<rangle> \<Rightarrow> Abrupt z\<rbrakk> \<Longrightarrow> False
 2. \<And>x sa z na bdy t'. \<lbrakk>\<forall>s'. s' \<in> P \<longrightarrow> (\<forall>t. g s' t (ret s' t) \<in> Q); UNIV \<subseteq> A; sa \<in> P; x \<in> (if na = length hs then - Q else - A); \<Gamma>\<turnstile>\<^sub>h \<langle>hs,ret sa t'\<rangle> \<Rightarrow> (na, Normal x); \<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (initfn sa)\<rangle> \<Rightarrow> Abrupt t'; z = ret sa t'\<rbrakk> \<Longrightarrow> False
 3. \<And>s n x h sa t hsa. \<lbrakk>\<forall>s'. s' \<in> P \<longrightarrow> (\<forall>t. g s' t (ret s' t) \<in> Q); UNIV \<subseteq> A; s \<in> P; x \<in> (if n = length hs then - Q else - A); s = sa; call initfn p ret (\<lambda>x y. Basic (g x y)) # hs = h # hsa; n = length hsa; Normal x = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> False
 4. \<And>s n x sa. \<lbrakk>\<forall>s'. s' \<in> P \<longrightarrow> (\<forall>t. g s' t (ret s' t) \<in> Q); UNIV \<subseteq> A; s \<in> P; x \<in> (if n = length hs then - Q else - A); s = sa; call initfn p ret (\<lambda>x y. Basic (g x y)) # hs = []; n = 0; Normal x = Abrupt sa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>x sa z na bdy t'. \<lbrakk>\<forall>s'. s' \<in> P \<longrightarrow> (\<forall>t. g s' t (ret s' t) \<in> Q); UNIV \<subseteq> A; sa \<in> P; x \<in> (if na = length hs then - Q else - A); \<Gamma>\<turnstile>\<^sub>h \<langle>hs,ret sa t'\<rangle> \<Rightarrow> (na, Normal x); \<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (initfn sa)\<rangle> \<Rightarrow> Abrupt t'; z = ret sa t'\<rbrakk> \<Longrightarrow> False
 2. \<And>s n x h sa t hsa. \<lbrakk>\<forall>s'. s' \<in> P \<longrightarrow> (\<forall>t. g s' t (ret s' t) \<in> Q); UNIV \<subseteq> A; s \<in> P; x \<in> (if n = length hs then - Q else - A); s = sa; call initfn p ret (\<lambda>x y. Basic (g x y)) # hs = h # hsa; n = length hsa; Normal x = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> False
 3. \<And>s n x sa. \<lbrakk>\<forall>s'. s' \<in> P \<longrightarrow> (\<forall>t. g s' t (ret s' t) \<in> Q); UNIV \<subseteq> A; s \<in> P; x \<in> (if n = length hs then - Q else - A); s = sa; call initfn p ret (\<lambda>x y. Basic (g x y)) # hs = []; n = 0; Normal x = Abrupt sa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>x sa na bdy t' v. \<lbrakk>\<forall>s'. s' \<in> P \<longrightarrow> (\<forall>t. g s' t (ret s' t) \<in> Q); UNIV \<subseteq> A; sa \<in> P; x \<in> (if na = length hs then - Q else - A); \<Gamma>\<turnstile>\<^sub>h \<langle>hs,ret sa t'\<rangle> \<Rightarrow> (na, Normal x); \<Gamma> p = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (initfn sa)\<rangle> \<Rightarrow> Abrupt t'; length hs - na = Suc v\<rbrakk> \<Longrightarrow> False
 2. \<And>s n x h sa t hsa. \<lbrakk>\<forall>s'. s' \<in> P \<longrightarrow> (\<forall>t. g s' t (ret s' t) \<in> Q); UNIV \<subseteq> A; s \<in> P; x \<in> (if n = length hs then - Q else - A); s = sa; call initfn p ret (\<lambda>x y. Basic (g x y)) # hs = h # hsa; n = length hsa; Normal x = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> False
 3. \<And>s n x sa. \<lbrakk>\<forall>s'. s' \<in> P \<longrightarrow> (\<forall>t. g s' t (ret s' t) \<in> Q); UNIV \<subseteq> A; s \<in> P; x \<in> (if n = length hs then - Q else - A); s = sa; call initfn p ret (\<lambda>x y. Basic (g x y)) # hs = []; n = 0; Normal x = Abrupt sa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s n x h sa t hsa. \<lbrakk>\<forall>s'. s' \<in> P \<longrightarrow> (\<forall>t. g s' t (ret s' t) \<in> Q); UNIV \<subseteq> A; s \<in> P; x \<in> (if n = length hs then - Q else - A); s = sa; call initfn p ret (\<lambda>x y. Basic (g x y)) # hs = h # hsa; n = length hsa; Normal x = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> False
 2. \<And>s n x sa. \<lbrakk>\<forall>s'. s' \<in> P \<longrightarrow> (\<forall>t. g s' t (ret s' t) \<in> Q); UNIV \<subseteq> A; s \<in> P; x \<in> (if n = length hs then - Q else - A); s = sa; call initfn p ret (\<lambda>x y. Basic (g x y)) # hs = []; n = 0; Normal x = Abrupt sa\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!