[STATEMENT]
lemma typ_ok_code:
  assumes "exe_wf_theory' \<Theta>"
  shows "typ_ok (translate_theory \<Theta>) ty = exetyp_ok \<Theta> ty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. typ_ok (translate_theory \<Theta>) ty = exetyp_ok \<Theta> ty
[PROOF STEP]
using assms typ_ok_sig_code
[PROOF STATE]
proof (prove)
using this:
exe_wf_theory' \<Theta>
exe_osig_conds (exesorts ?\<Sigma>) \<Longrightarrow> typ_ok_sig (translate_signature ?\<Sigma>) ?ty = exetyp_ok_sig ?\<Sigma> ?ty

goal (1 subgoal):
 1. typ_ok (translate_theory \<Theta>) ty = exetyp_ok \<Theta> ty
[PROOF STEP]
by (metis exe_sig_conds_def exe_wf_theory.simps exe_wf_theory_code exesignature.exhaust
      exetheory.sel(1) sig.simps translate_theory.elims typ_ok_def wf_type_iff_typ_ok_sig)


[STATEMENT]
lemma execlass_leq_code: "class_leq (set cs) c1 c2 = execlass_leq cs c1 c2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class_leq (set cs) c1 c2 = execlass_leq cs c1 c2
[PROOF STEP]
by (simp add: class_leq_def class_les_def member_def)


[STATEMENT]
lemma exehas_sort_imp_has_sort:
  assumes "exe_osig_conds (sub, tcs)"
  shows "exehas_sort (sub, tcs) T S \<Longrightarrow> has_sort (translate_osig (sub, tcs)) T S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exehas_sort (sub, tcs) T S \<Longrightarrow> has_sort (translate_osig (sub, tcs)) T S
[PROOF STEP]
proof (induction T arbitrary: S)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2 S. \<lbrakk>\<And>x2a S. \<lbrakk>x2a \<in> set x2; exehas_sort (sub, tcs) x2a S\<rbrakk> \<Longrightarrow> has_sort (translate_osig (sub, tcs)) x2a S; exehas_sort (sub, tcs) (Ty x1 x2) S\<rbrakk> \<Longrightarrow> has_sort (translate_osig (sub, tcs)) (Ty x1 x2) S
 2. \<And>x1 x2 S. exehas_sort (sub, tcs) (Tv x1 x2) S \<Longrightarrow> has_sort (translate_osig (sub, tcs)) (Tv x1 x2) S
[PROOF STEP]
case (Ty n Ts)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2a \<in> set Ts; exehas_sort (sub, tcs) ?x2a ?S\<rbrakk> \<Longrightarrow> has_sort (translate_osig (sub, tcs)) ?x2a ?S
exehas_sort (sub, tcs) (Ty n Ts) S

goal (2 subgoals):
 1. \<And>x1 x2 S. \<lbrakk>\<And>x2a S. \<lbrakk>x2a \<in> set x2; exehas_sort (sub, tcs) x2a S\<rbrakk> \<Longrightarrow> has_sort (translate_osig (sub, tcs)) x2a S; exehas_sort (sub, tcs) (Ty x1 x2) S\<rbrakk> \<Longrightarrow> has_sort (translate_osig (sub, tcs)) (Ty x1 x2) S
 2. \<And>x1 x2 S. exehas_sort (sub, tcs) (Tv x1 x2) S \<Longrightarrow> has_sort (translate_osig (sub, tcs)) (Tv x1 x2) S
[PROOF STEP]
obtain sub' tcs' where sub'_tcs': "translate_osig (sub, tcs) = (sub', tcs')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>sub' tcs'. translate_osig (sub, tcs) = (sub', tcs') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
translate_osig (sub, tcs) = (sub', tcs')

goal (2 subgoals):
 1. \<And>x1 x2 S. \<lbrakk>\<And>x2a S. \<lbrakk>x2a \<in> set x2; exehas_sort (sub, tcs) x2a S\<rbrakk> \<Longrightarrow> has_sort (translate_osig (sub, tcs)) x2a S; exehas_sort (sub, tcs) (Ty x1 x2) S\<rbrakk> \<Longrightarrow> has_sort (translate_osig (sub, tcs)) (Ty x1 x2) S
 2. \<And>x1 x2 S. exehas_sort (sub, tcs) (Tv x1 x2) S \<Longrightarrow> has_sort (translate_osig (sub, tcs)) (Tv x1 x2) S
[PROOF STEP]
obtain mgd where mgd: "tcs' n = Some mgd"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>mgd. tcs' n = Some mgd \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Ty.prems sub'_tcs'
[PROOF STATE]
proof (prove)
using this:
exehas_sort (sub, tcs) (Ty n Ts) S
translate_osig (sub, tcs) = (sub', tcs')

goal (1 subgoal):
 1. (\<And>mgd. tcs' n = Some mgd \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (simp split: option.splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>\<forall>C\<in>S. (\<exists>y. lookup (\<lambda>k. k = C) x2 = Some y) \<and> (\<forall>x2a. lookup (\<lambda>k. k = C) x2 = Some x2a \<longrightarrow> list_all2 (exehas_sort (sub, tcs)) Ts x2a); (if exe_osig_conds (sub, tcs) then (set sub, translate_ars tcs) else ({}, [STR ''A'' \<mapsto> [STR ''A'' \<mapsto> [insert STR ''A'' full_sort]]])) = (sub', tcs'); \<And>mgd. tcs' n = Some mgd \<Longrightarrow> thesis; lookup (\<lambda>k. k = n) tcs = Some x2\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (metis assms exe_ars_conds_def exe_osig_conds_def in_alist_imp_in_map_of lookup_eq_map_of_ap
        map_of_SomeD snd_conv)
[PROOF STATE]
proof (state)
this:
tcs' n = Some mgd

goal (2 subgoals):
 1. \<And>x1 x2 S. \<lbrakk>\<And>x2a S. \<lbrakk>x2a \<in> set x2; exehas_sort (sub, tcs) x2a S\<rbrakk> \<Longrightarrow> has_sort (translate_osig (sub, tcs)) x2a S; exehas_sort (sub, tcs) (Ty x1 x2) S\<rbrakk> \<Longrightarrow> has_sort (translate_osig (sub, tcs)) (Ty x1 x2) S
 2. \<And>x1 x2 S. exehas_sort (sub, tcs) (Tv x1 x2) S \<Longrightarrow> has_sort (translate_osig (sub, tcs)) (Tv x1 x2) S
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_sort (translate_osig (sub, tcs)) (Ty n Ts) S
[PROOF STEP]
proof (subst sub'_tcs', rule has_sort_Ty[of tcs', OF mgd], rule ballI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. c \<in> S \<Longrightarrow> \<exists>Ss. mgd c = Some Ss \<and> list_all2 (has_sort (sub', tcs')) Ts Ss
[PROOF STEP]
fix c
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. c \<in> S \<Longrightarrow> \<exists>Ss. mgd c = Some Ss \<and> list_all2 (has_sort (sub', tcs')) Ts Ss
[PROOF STEP]
assume asm: "c\<in>S"
[PROOF STATE]
proof (state)
this:
c \<in> S

goal (1 subgoal):
 1. \<And>c. c \<in> S \<Longrightarrow> \<exists>Ss. mgd c = Some Ss \<and> list_all2 (has_sort (sub', tcs')) Ts Ss
[PROOF STEP]
have l: "lookup (\<lambda>k. k=n) (map (apsnd map_of) tcs) = Some mgd"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (\<lambda>k. k = n) (map (apsnd map_of) tcs) = Some mgd
[PROOF STEP]
by (metis assms lookup_eq_map_of_ap mgd snd_conv sub'_tcs' translate_ars.simps translate_osig.simps)
[PROOF STATE]
proof (state)
this:
lookup (\<lambda>k. k = n) (map (apsnd map_of) tcs) = Some mgd

goal (1 subgoal):
 1. \<And>c. c \<in> S \<Longrightarrow> \<exists>Ss. mgd c = Some Ss \<and> list_all2 (has_sort (sub', tcs')) Ts Ss
[PROOF STEP]
hence "\<exists>x. (lookup (\<lambda>k. k=n) tcs) = Some x"
[PROOF STATE]
proof (prove)
using this:
lookup (\<lambda>k. k = n) (map (apsnd map_of) tcs) = Some mgd

goal (1 subgoal):
 1. \<exists>x. lookup (\<lambda>k. k = n) tcs = Some x
[PROOF STEP]
by (induction tcs) auto
[PROOF STATE]
proof (state)
this:
\<exists>x. lookup (\<lambda>k. k = n) tcs = Some x

goal (1 subgoal):
 1. \<And>c. c \<in> S \<Longrightarrow> \<exists>Ss. mgd c = Some Ss \<and> list_all2 (has_sort (sub', tcs')) Ts Ss
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. lookup (\<lambda>k. k = n) tcs = Some x
[PROOF STEP]
obtain pre_mgd where pre_mgd: "(lookup (\<lambda>k. k=n) tcs) = Some pre_mgd"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. lookup (\<lambda>k. k = n) tcs = Some x

goal (1 subgoal):
 1. (\<And>pre_mgd. lookup (\<lambda>k. k = n) tcs = Some pre_mgd \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
lookup (\<lambda>k. k = n) tcs = Some pre_mgd

goal (1 subgoal):
 1. \<And>c. c \<in> S \<Longrightarrow> \<exists>Ss. mgd c = Some Ss \<and> list_all2 (has_sort (sub', tcs')) Ts Ss
[PROOF STEP]
have pre_mgd_mgd: "map_of pre_mgd = mgd"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of pre_mgd = mgd
[PROOF STEP]
by (metis l assms exe_ars_conds_def
          exe_osig_conds_def in_alist_imp_in_map_of lookup_eq_map_of_ap map_of_SomeD
          option.sel pre_mgd snd_conv translate_ars.simps)
[PROOF STATE]
proof (state)
this:
map_of pre_mgd = mgd

goal (1 subgoal):
 1. \<And>c. c \<in> S \<Longrightarrow> \<exists>Ss. mgd c = Some Ss \<and> list_all2 (has_sort (sub', tcs')) Ts Ss
[PROOF STEP]
obtain Ss where Ss: "lookup (\<lambda>k. k=c) pre_mgd = Some Ss"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Ss. lookup (\<lambda>k. k = c) pre_mgd = Some Ss \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Ty.prems asm
[PROOF STATE]
proof (prove)
using this:
exehas_sort (sub, tcs) (Ty n Ts) S
c \<in> S

goal (1 subgoal):
 1. (\<And>Ss. lookup (\<lambda>k. k = c) pre_mgd = Some Ss \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: pre_mgd split: option.splits)
[PROOF STATE]
proof (state)
this:
lookup (\<lambda>k. k = c) pre_mgd = Some Ss

goal (1 subgoal):
 1. \<And>c. c \<in> S \<Longrightarrow> \<exists>Ss. mgd c = Some Ss \<and> list_all2 (has_sort (sub', tcs')) Ts Ss
[PROOF STEP]
hence cond: "list_all2 (exehas_sort (sub,tcs)) Ts Ss"
[PROOF STATE]
proof (prove)
using this:
lookup (\<lambda>k. k = c) pre_mgd = Some Ss

goal (1 subgoal):
 1. list_all2 (exehas_sort (sub, tcs)) Ts Ss
[PROOF STEP]
using \<open>exehas_sort (sub, tcs) (Ty n Ts) S\<close>asm pre_mgd
[PROOF STATE]
proof (prove)
using this:
lookup (\<lambda>k. k = c) pre_mgd = Some Ss
exehas_sort (sub, tcs) (Ty n Ts) S
c \<in> S
lookup (\<lambda>k. k = n) tcs = Some pre_mgd

goal (1 subgoal):
 1. list_all2 (exehas_sort (sub, tcs)) Ts Ss
[PROOF STEP]
by (auto split: option.splits)
[PROOF STATE]
proof (state)
this:
list_all2 (exehas_sort (sub, tcs)) Ts Ss

goal (1 subgoal):
 1. \<And>c. c \<in> S \<Longrightarrow> \<exists>Ss. mgd c = Some Ss \<and> list_all2 (has_sort (sub', tcs')) Ts Ss
[PROOF STEP]
from Ss
[PROOF STATE]
proof (chain)
picking this:
lookup (\<lambda>k. k = c) pre_mgd = Some Ss
[PROOF STEP]
have "mgd c = Some Ss"
[PROOF STATE]
proof (prove)
using this:
lookup (\<lambda>k. k = c) pre_mgd = Some Ss

goal (1 subgoal):
 1. mgd c = Some Ss
[PROOF STEP]
by (simp add: lookup_eq_map_of_ap pre_mgd_mgd)
[PROOF STATE]
proof (state)
this:
mgd c = Some Ss

goal (1 subgoal):
 1. \<And>c. c \<in> S \<Longrightarrow> \<exists>Ss. mgd c = Some Ss \<and> list_all2 (has_sort (sub', tcs')) Ts Ss
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
mgd c = Some Ss
[PROOF STEP]
show "\<exists>Ss. mgd c = Some Ss \<and> list_all2 (has_sort (sub', tcs')) Ts Ss"
[PROOF STATE]
proof (prove)
using this:
mgd c = Some Ss

goal (1 subgoal):
 1. \<exists>Ss. mgd c = Some Ss \<and> list_all2 (has_sort (sub', tcs')) Ts Ss
[PROOF STEP]
using cond Ty.IH list.rel_mono_strong sub'_tcs'
[PROOF STATE]
proof (prove)
using this:
mgd c = Some Ss
list_all2 (exehas_sort (sub, tcs)) Ts Ss
\<lbrakk>?x2a \<in> set Ts; exehas_sort (sub, tcs) ?x2a ?S\<rbrakk> \<Longrightarrow> has_sort (translate_osig (sub, tcs)) ?x2a ?S
\<lbrakk>list_all2 ?R ?x ?y; \<And>z yb. \<lbrakk>z \<in> set ?x; yb \<in> set ?y; ?R z yb\<rbrakk> \<Longrightarrow> ?Ra z yb\<rbrakk> \<Longrightarrow> list_all2 ?Ra ?x ?y
translate_osig (sub, tcs) = (sub', tcs')

goal (1 subgoal):
 1. \<exists>Ss. mgd c = Some Ss \<and> list_all2 (has_sort (sub', tcs')) Ts Ss
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>Ss. mgd c = Some Ss \<and> list_all2 (has_sort (sub', tcs')) Ts Ss

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
has_sort (translate_osig (sub, tcs)) (Ty n Ts) S

goal (1 subgoal):
 1. \<And>x1 x2 S. exehas_sort (sub, tcs) (Tv x1 x2) S \<Longrightarrow> has_sort (translate_osig (sub, tcs)) (Tv x1 x2) S
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 S. exehas_sort (sub, tcs) (Tv x1 x2) S \<Longrightarrow> has_sort (translate_osig (sub, tcs)) (Tv x1 x2) S
[PROOF STEP]
case (Tv n S)
[PROOF STATE]
proof (state)
this:
exehas_sort (sub, tcs) (Tv n Sa__) S

goal (1 subgoal):
 1. \<And>x1 x2 S. exehas_sort (sub, tcs) (Tv x1 x2) S \<Longrightarrow> has_sort (translate_osig (sub, tcs)) (Tv x1 x2) S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
exehas_sort (sub, tcs) (Tv n Sa__) S
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
exehas_sort (sub, tcs) (Tv n Sa__) S

goal (1 subgoal):
 1. has_sort (translate_osig (sub, tcs)) (Tv n Sa__) S
[PROOF STEP]
by (metis assms exehas_sort.simps(1) exesort_les_code has_sort_Tv prod.collapse translate_osig.simps)
[PROOF STATE]
proof (state)
this:
has_sort (translate_osig (sub, tcs)) (Tv n Sa__) S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma has_sort_imp_exehas_sort:
  assumes "exe_osig_conds (sub, tcs)"
  shows "has_sort (translate_osig (sub, tcs)) T S \<Longrightarrow> exehas_sort (sub, tcs) T S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_sort (translate_osig (sub, tcs)) T S \<Longrightarrow> exehas_sort (sub, tcs) T S
[PROOF STEP]
proof (induction T arbitrary: S)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2 S. \<lbrakk>\<And>x2a S. \<lbrakk>x2a \<in> set x2; has_sort (translate_osig (sub, tcs)) x2a S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) x2a S; has_sort (translate_osig (sub, tcs)) (Ty x1 x2) S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) (Ty x1 x2) S
 2. \<And>x1 x2 S. has_sort (translate_osig (sub, tcs)) (Tv x1 x2) S \<Longrightarrow> exehas_sort (sub, tcs) (Tv x1 x2) S
[PROOF STEP]
case (Ty n Ts)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2a \<in> set Ts; has_sort (translate_osig (sub, tcs)) ?x2a ?S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) ?x2a ?S
has_sort (translate_osig (sub, tcs)) (Ty n Ts) S

goal (2 subgoals):
 1. \<And>x1 x2 S. \<lbrakk>\<And>x2a S. \<lbrakk>x2a \<in> set x2; has_sort (translate_osig (sub, tcs)) x2a S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) x2a S; has_sort (translate_osig (sub, tcs)) (Ty x1 x2) S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) (Ty x1 x2) S
 2. \<And>x1 x2 S. has_sort (translate_osig (sub, tcs)) (Tv x1 x2) S \<Longrightarrow> exehas_sort (sub, tcs) (Tv x1 x2) S
[PROOF STEP]
obtain sub' tcs' where sub'_tcs': "translate_osig (sub, tcs) = (sub', tcs')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>sub' tcs'. translate_osig (sub, tcs) = (sub', tcs') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
translate_osig (sub, tcs) = (sub', tcs')

goal (2 subgoals):
 1. \<And>x1 x2 S. \<lbrakk>\<And>x2a S. \<lbrakk>x2a \<in> set x2; has_sort (translate_osig (sub, tcs)) x2a S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) x2a S; has_sort (translate_osig (sub, tcs)) (Ty x1 x2) S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) (Ty x1 x2) S
 2. \<And>x1 x2 S. has_sort (translate_osig (sub, tcs)) (Tv x1 x2) S \<Longrightarrow> exehas_sort (sub, tcs) (Tv x1 x2) S
[PROOF STEP]
obtain mgd where mgd: "tcs' n = Some mgd"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>mgd. tcs' n = Some mgd \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Ty.prems sub'_tcs' has_sort.simps
[PROOF STATE]
proof (prove)
using this:
has_sort (translate_osig (sub, tcs)) (Ty n Ts) S
translate_osig (sub, tcs) = (sub', tcs')
has_sort ?a1.0 ?a2.0 ?a3.0 = ((\<exists>sub S S' tcs a. ?a1.0 = (sub, tcs) \<and> ?a2.0 = Tv a S \<and> ?a3.0 = S' \<and> sort_leq sub S S') \<or> (\<exists>tcs \<kappa> dm S sub Ts. ?a1.0 = (sub, tcs) \<and> ?a2.0 = Ty \<kappa> Ts \<and> ?a3.0 = S \<and> tcs \<kappa> = Some dm \<and> (\<forall>c\<in>S. \<exists>Ss. dm c = Some Ss \<and> list_all2 (has_sort (sub, tcs)) Ts Ss)))

goal (1 subgoal):
 1. (\<And>mgd. tcs' n = Some mgd \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto split: option.splits)
[PROOF STATE]
proof (state)
this:
tcs' n = Some mgd

goal (2 subgoals):
 1. \<And>x1 x2 S. \<lbrakk>\<And>x2a S. \<lbrakk>x2a \<in> set x2; has_sort (translate_osig (sub, tcs)) x2a S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) x2a S; has_sort (translate_osig (sub, tcs)) (Ty x1 x2) S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) (Ty x1 x2) S
 2. \<And>x1 x2 S. has_sort (translate_osig (sub, tcs)) (Tv x1 x2) S \<Longrightarrow> exehas_sort (sub, tcs) (Tv x1 x2) S
[PROOF STEP]
hence "lookup (\<lambda>k. k=n) (map (apsnd map_of) tcs) = Some mgd"
[PROOF STATE]
proof (prove)
using this:
tcs' n = Some mgd

goal (1 subgoal):
 1. lookup (\<lambda>k. k = n) (map (apsnd map_of) tcs) = Some mgd
[PROOF STEP]
by (metis assms lookup_eq_map_of_ap prod.inject sub'_tcs' translate_ars.simps translate_osig.simps)
[PROOF STATE]
proof (state)
this:
lookup (\<lambda>k. k = n) (map (apsnd map_of) tcs) = Some mgd

goal (2 subgoals):
 1. \<And>x1 x2 S. \<lbrakk>\<And>x2a S. \<lbrakk>x2a \<in> set x2; has_sort (translate_osig (sub, tcs)) x2a S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) x2a S; has_sort (translate_osig (sub, tcs)) (Ty x1 x2) S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) (Ty x1 x2) S
 2. \<And>x1 x2 S. has_sort (translate_osig (sub, tcs)) (Tv x1 x2) S \<Longrightarrow> exehas_sort (sub, tcs) (Tv x1 x2) S
[PROOF STEP]
have l: "lookup (\<lambda>k. k=n) (map (apsnd map_of) tcs) = Some mgd"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (\<lambda>k. k = n) (map (apsnd map_of) tcs) = Some mgd
[PROOF STEP]
by (metis assms lookup_eq_map_of_ap mgd snd_conv sub'_tcs'
        translate_ars.simps translate_osig.simps)
[PROOF STATE]
proof (state)
this:
lookup (\<lambda>k. k = n) (map (apsnd map_of) tcs) = Some mgd

goal (2 subgoals):
 1. \<And>x1 x2 S. \<lbrakk>\<And>x2a S. \<lbrakk>x2a \<in> set x2; has_sort (translate_osig (sub, tcs)) x2a S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) x2a S; has_sort (translate_osig (sub, tcs)) (Ty x1 x2) S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) (Ty x1 x2) S
 2. \<And>x1 x2 S. has_sort (translate_osig (sub, tcs)) (Tv x1 x2) S \<Longrightarrow> exehas_sort (sub, tcs) (Tv x1 x2) S
[PROOF STEP]
hence "\<exists>x. (lookup (\<lambda>k. k=n) tcs) = Some x"
[PROOF STATE]
proof (prove)
using this:
lookup (\<lambda>k. k = n) (map (apsnd map_of) tcs) = Some mgd

goal (1 subgoal):
 1. \<exists>x. lookup (\<lambda>k. k = n) tcs = Some x
[PROOF STEP]
by (induction tcs) auto
[PROOF STATE]
proof (state)
this:
\<exists>x. lookup (\<lambda>k. k = n) tcs = Some x

goal (2 subgoals):
 1. \<And>x1 x2 S. \<lbrakk>\<And>x2a S. \<lbrakk>x2a \<in> set x2; has_sort (translate_osig (sub, tcs)) x2a S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) x2a S; has_sort (translate_osig (sub, tcs)) (Ty x1 x2) S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) (Ty x1 x2) S
 2. \<And>x1 x2 S. has_sort (translate_osig (sub, tcs)) (Tv x1 x2) S \<Longrightarrow> exehas_sort (sub, tcs) (Tv x1 x2) S
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. lookup (\<lambda>k. k = n) tcs = Some x
[PROOF STEP]
obtain pre_mgd where pre_mgd: "(lookup (\<lambda>k. k=n) tcs) = Some pre_mgd"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. lookup (\<lambda>k. k = n) tcs = Some x

goal (1 subgoal):
 1. (\<And>pre_mgd. lookup (\<lambda>k. k = n) tcs = Some pre_mgd \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
lookup (\<lambda>k. k = n) tcs = Some pre_mgd

goal (2 subgoals):
 1. \<And>x1 x2 S. \<lbrakk>\<And>x2a S. \<lbrakk>x2a \<in> set x2; has_sort (translate_osig (sub, tcs)) x2a S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) x2a S; has_sort (translate_osig (sub, tcs)) (Ty x1 x2) S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) (Ty x1 x2) S
 2. \<And>x1 x2 S. has_sort (translate_osig (sub, tcs)) (Tv x1 x2) S \<Longrightarrow> exehas_sort (sub, tcs) (Tv x1 x2) S
[PROOF STEP]
have pre_mgd_mgd: "map_of pre_mgd = mgd"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of pre_mgd = mgd
[PROOF STEP]
by (metis l assms exe_ars_conds_def
        exe_osig_conds_def in_alist_imp_in_map_of lookup_eq_map_of_ap map_of_SomeD option.sel
        pre_mgd snd_conv translate_ars.simps)
[PROOF STATE]
proof (state)
this:
map_of pre_mgd = mgd

goal (2 subgoals):
 1. \<And>x1 x2 S. \<lbrakk>\<And>x2a S. \<lbrakk>x2a \<in> set x2; has_sort (translate_osig (sub, tcs)) x2a S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) x2a S; has_sort (translate_osig (sub, tcs)) (Ty x1 x2) S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) (Ty x1 x2) S
 2. \<And>x1 x2 S. has_sort (translate_osig (sub, tcs)) (Tv x1 x2) S \<Longrightarrow> exehas_sort (sub, tcs) (Tv x1 x2) S
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
map_of pre_mgd = mgd

goal (2 subgoals):
 1. \<And>x1 x2 S. \<lbrakk>\<And>x2a S. \<lbrakk>x2a \<in> set x2; has_sort (translate_osig (sub, tcs)) x2a S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) x2a S; has_sort (translate_osig (sub, tcs)) (Ty x1 x2) S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) (Ty x1 x2) S
 2. \<And>x1 x2 S. has_sort (translate_osig (sub, tcs)) (Tv x1 x2) S \<Longrightarrow> exehas_sort (sub, tcs) (Tv x1 x2) S
[PROOF STEP]
fix c
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2 S. \<lbrakk>\<And>x2a S. \<lbrakk>x2a \<in> set x2; has_sort (translate_osig (sub, tcs)) x2a S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) x2a S; has_sort (translate_osig (sub, tcs)) (Ty x1 x2) S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) (Ty x1 x2) S
 2. \<And>x1 x2 S. has_sort (translate_osig (sub, tcs)) (Tv x1 x2) S \<Longrightarrow> exehas_sort (sub, tcs) (Tv x1 x2) S
[PROOF STEP]
assume asm: "c\<in>S"
[PROOF STATE]
proof (state)
this:
c \<in> S

goal (2 subgoals):
 1. \<And>x1 x2 S. \<lbrakk>\<And>x2a S. \<lbrakk>x2a \<in> set x2; has_sort (translate_osig (sub, tcs)) x2a S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) x2a S; has_sort (translate_osig (sub, tcs)) (Ty x1 x2) S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) (Ty x1 x2) S
 2. \<And>x1 x2 S. has_sort (translate_osig (sub, tcs)) (Tv x1 x2) S \<Longrightarrow> exehas_sort (sub, tcs) (Tv x1 x2) S
[PROOF STEP]
obtain Ss where Ss: "lookup (\<lambda>k. k=c) pre_mgd = Some Ss"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Ss. lookup (\<lambda>k. k = c) pre_mgd = Some Ss \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>c \<in> S\<close> \<open>map_of pre_mgd = mgd\<close> sub'_tcs' mgd assms Ty.prems has_sort.simps
[PROOF STATE]
proof (prove)
using this:
c \<in> S
map_of pre_mgd = mgd
translate_osig (sub, tcs) = (sub', tcs')
tcs' n = Some mgd
exe_osig_conds (sub, tcs)
has_sort (translate_osig (sub, tcs)) (Ty n Ts) S
has_sort ?a1.0 ?a2.0 ?a3.0 = ((\<exists>sub S S' tcs a. ?a1.0 = (sub, tcs) \<and> ?a2.0 = Tv a S \<and> ?a3.0 = S' \<and> sort_leq sub S S') \<or> (\<exists>tcs \<kappa> dm S sub Ts. ?a1.0 = (sub, tcs) \<and> ?a2.0 = Ty \<kappa> Ts \<and> ?a3.0 = S \<and> tcs \<kappa> = Some dm \<and> (\<forall>c\<in>S. \<exists>Ss. dm c = Some Ss \<and> list_all2 (has_sort (sub, tcs)) Ts Ss)))

goal (1 subgoal):
 1. (\<And>Ss. lookup (\<lambda>k. k = c) pre_mgd = Some Ss \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: dom_map_of_conv_image_fst domIff eq_fst_iff exe_ars_conds_def
          map_of_eq_None_iff classes_translate lookup_eq_map_of_ap split: typ.splits
          dest!: domD intro!: domI)
[PROOF STATE]
proof (state)
this:
lookup (\<lambda>k. k = c) pre_mgd = Some Ss

goal (2 subgoals):
 1. \<And>x1 x2 S. \<lbrakk>\<And>x2a S. \<lbrakk>x2a \<in> set x2; has_sort (translate_osig (sub, tcs)) x2a S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) x2a S; has_sort (translate_osig (sub, tcs)) (Ty x1 x2) S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) (Ty x1 x2) S
 2. \<And>x1 x2 S. has_sort (translate_osig (sub, tcs)) (Tv x1 x2) S \<Longrightarrow> exehas_sort (sub, tcs) (Tv x1 x2) S
[PROOF STEP]
have l: "length Ts = length Ss"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length Ts = length Ss
[PROOF STEP]
using asm mgd pre_mgd Ty.prems assms sub'_tcs' Ss list_all2_lengthD pre_mgd_mgd
[PROOF STATE]
proof (prove)
using this:
c \<in> S
tcs' n = Some mgd
lookup (\<lambda>k. k = n) tcs = Some pre_mgd
has_sort (translate_osig (sub, tcs)) (Ty n Ts) S
exe_osig_conds (sub, tcs)
translate_osig (sub, tcs) = (sub', tcs')
lookup (\<lambda>k. k = c) pre_mgd = Some Ss
list_all2 ?P ?xs ?ys \<Longrightarrow> length ?xs = length ?ys
map_of pre_mgd = mgd

goal (1 subgoal):
 1. length Ts = length Ss
[PROOF STEP]
by (fastforce simp add: has_sort.simps lookup_eq_map_of_ap)
[PROOF STATE]
proof (state)
this:
length Ts = length Ss

goal (2 subgoals):
 1. \<And>x1 x2 S. \<lbrakk>\<And>x2a S. \<lbrakk>x2a \<in> set x2; has_sort (translate_osig (sub, tcs)) x2a S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) x2a S; has_sort (translate_osig (sub, tcs)) (Ty x1 x2) S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) (Ty x1 x2) S
 2. \<And>x1 x2 S. has_sort (translate_osig (sub, tcs)) (Tv x1 x2) S \<Longrightarrow> exehas_sort (sub, tcs) (Tv x1 x2) S
[PROOF STEP]
have 1: "\<forall>c \<in> S. \<exists>Ss . mgd c = Some Ss \<and> list_all2 (has_sort (sub', tcs')) Ts Ss"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c\<in>S. \<exists>Ss. mgd c = Some Ss \<and> list_all2 (has_sort (sub', tcs')) Ts Ss
[PROOF STEP]
using mgd Ty.prems has_sort.simps sub'_tcs'
[PROOF STATE]
proof (prove)
using this:
tcs' n = Some mgd
has_sort (translate_osig (sub, tcs)) (Ty n Ts) S
has_sort ?a1.0 ?a2.0 ?a3.0 = ((\<exists>sub S S' tcs a. ?a1.0 = (sub, tcs) \<and> ?a2.0 = Tv a S \<and> ?a3.0 = S' \<and> sort_leq sub S S') \<or> (\<exists>tcs \<kappa> dm S sub Ts. ?a1.0 = (sub, tcs) \<and> ?a2.0 = Ty \<kappa> Ts \<and> ?a3.0 = S \<and> tcs \<kappa> = Some dm \<and> (\<forall>c\<in>S. \<exists>Ss. dm c = Some Ss \<and> list_all2 (has_sort (sub, tcs)) Ts Ss)))
translate_osig (sub, tcs) = (sub', tcs')

goal (1 subgoal):
 1. \<forall>c\<in>S. \<exists>Ss. mgd c = Some Ss \<and> list_all2 (has_sort (sub', tcs')) Ts Ss
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>c\<in>S. \<exists>Ss. mgd c = Some Ss \<and> list_all2 (has_sort (sub', tcs')) Ts Ss

goal (2 subgoals):
 1. \<And>x1 x2 S. \<lbrakk>\<And>x2a S. \<lbrakk>x2a \<in> set x2; has_sort (translate_osig (sub, tcs)) x2a S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) x2a S; has_sort (translate_osig (sub, tcs)) (Ty x1 x2) S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) (Ty x1 x2) S
 2. \<And>x1 x2 S. has_sort (translate_osig (sub, tcs)) (Tv x1 x2) S \<Longrightarrow> exehas_sort (sub, tcs) (Tv x1 x2) S
[PROOF STEP]
have cond: "list_all2 (exehas_sort (sub,tcs)) Ts Ss"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all2 (exehas_sort (sub, tcs)) Ts Ss
[PROOF STEP]
apply (rule list_all2_all_nthI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length Ts = length Ss
 2. \<And>n. n < length Ts \<Longrightarrow> exehas_sort (sub, tcs) (Ts ! n) (Ss ! n)
[PROOF STEP]
using l
[PROOF STATE]
proof (prove)
using this:
length Ts = length Ss

goal (2 subgoals):
 1. length Ts = length Ss
 2. \<And>n. n < length Ts \<Longrightarrow> exehas_sort (sub, tcs) (Ts ! n) (Ss ! n)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. n < length Ts \<Longrightarrow> exehas_sort (sub, tcs) (Ts ! n) (Ss ! n)
[PROOF STEP]
subgoal premises p for m
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exehas_sort (sub, tcs) (Ts ! m) (Ss ! m)
[PROOF STEP]
apply (rule Ty.IH)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Ts ! m \<in> set Ts
 2. has_sort (translate_osig (sub, tcs)) (Ts ! m) (Ss ! m)
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
m < length Ts

goal (2 subgoals):
 1. Ts ! m \<in> set Ts
 2. has_sort (translate_osig (sub, tcs)) (Ts ! m) (Ss ! m)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_sort (translate_osig (sub, tcs)) (Ts ! m) (Ss ! m)
[PROOF STEP]
using p Ty.prems assms 1
[PROOF STATE]
proof (prove)
using this:
m < length Ts
has_sort (translate_osig (sub, tcs)) (Ty n Ts) S
exe_osig_conds (sub, tcs)
\<forall>c\<in>S. \<exists>Ss. mgd c = Some Ss \<and> list_all2 (has_sort (sub', tcs')) Ts Ss

goal (1 subgoal):
 1. has_sort (translate_osig (sub, tcs)) (Ts ! m) (Ss ! m)
[PROOF STEP]
by (metis Ss asm list_all2_conv_all_nth lookup_eq_map_of_ap option.sel pre_mgd_mgd sub'_tcs')
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
list_all2 (exehas_sort (sub, tcs)) Ts Ss

goal (2 subgoals):
 1. \<And>x1 x2 S. \<lbrakk>\<And>x2a S. \<lbrakk>x2a \<in> set x2; has_sort (translate_osig (sub, tcs)) x2a S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) x2a S; has_sort (translate_osig (sub, tcs)) (Ty x1 x2) S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) (Ty x1 x2) S
 2. \<And>x1 x2 S. has_sort (translate_osig (sub, tcs)) (Tv x1 x2) S \<Longrightarrow> exehas_sort (sub, tcs) (Tv x1 x2) S
[PROOF STEP]
have "(\<forall>C \<in> S.
    case lookup (\<lambda>k. k=C) pre_mgd of
        None \<Rightarrow> False
      | Some Ss \<Rightarrow> list_all2 (exehas_sort (sub,tcs)) Ts Ss)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>C\<in>S. case lookup (\<lambda>k. k = C) pre_mgd of None \<Rightarrow> False | Some Ss \<Rightarrow> list_all2 (exehas_sort (sub, tcs)) Ts Ss
[PROOF STEP]
by (metis "1" Ty.IH list_all2_conv_all_nth lookup_eq_map_of_ap nth_mem option.simps(5)
        pre_mgd_mgd sub'_tcs')
[PROOF STATE]
proof (state)
this:
\<forall>C\<in>S. case lookup (\<lambda>k. k = C) pre_mgd of None \<Rightarrow> False | Some Ss \<Rightarrow> list_all2 (exehas_sort (sub, tcs)) Ts Ss

goal (2 subgoals):
 1. \<And>x1 x2 S. \<lbrakk>\<And>x2a S. \<lbrakk>x2a \<in> set x2; has_sort (translate_osig (sub, tcs)) x2a S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) x2a S; has_sort (translate_osig (sub, tcs)) (Ty x1 x2) S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) (Ty x1 x2) S
 2. \<And>x1 x2 S. has_sort (translate_osig (sub, tcs)) (Tv x1 x2) S \<Longrightarrow> exehas_sort (sub, tcs) (Tv x1 x2) S
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?c2 \<in> S \<Longrightarrow> \<forall>C\<in>S. case lookup (\<lambda>k. k = C) pre_mgd of None \<Rightarrow> False | Some Ss \<Rightarrow> list_all2 (exehas_sort (sub, tcs)) Ts Ss

goal (2 subgoals):
 1. \<And>x1 x2 S. \<lbrakk>\<And>x2a S. \<lbrakk>x2a \<in> set x2; has_sort (translate_osig (sub, tcs)) x2a S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) x2a S; has_sort (translate_osig (sub, tcs)) (Ty x1 x2) S\<rbrakk> \<Longrightarrow> exehas_sort (sub, tcs) (Ty x1 x2) S
 2. \<And>x1 x2 S. has_sort (translate_osig (sub, tcs)) (Tv x1 x2) S \<Longrightarrow> exehas_sort (sub, tcs) (Tv x1 x2) S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?c2 \<in> S \<Longrightarrow> \<forall>C\<in>S. case lookup (\<lambda>k. k = C) pre_mgd of None \<Rightarrow> False | Some Ss \<Rightarrow> list_all2 (exehas_sort (sub, tcs)) Ts Ss
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?c2 \<in> S \<Longrightarrow> \<forall>C\<in>S. case lookup (\<lambda>k. k = C) pre_mgd of None \<Rightarrow> False | Some Ss \<Rightarrow> list_all2 (exehas_sort (sub, tcs)) Ts Ss

goal (1 subgoal):
 1. exehas_sort (sub, tcs) (Ty n Ts) S
[PROOF STEP]
using pre_mgd
[PROOF STATE]
proof (prove)
using this:
?c2 \<in> S \<Longrightarrow> \<forall>C\<in>S. case lookup (\<lambda>k. k = C) pre_mgd of None \<Rightarrow> False | Some Ss \<Rightarrow> list_all2 (exehas_sort (sub, tcs)) Ts Ss
lookup (\<lambda>k. k = n) tcs = Some pre_mgd

goal (1 subgoal):
 1. exehas_sort (sub, tcs) (Ty n Ts) S
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
exehas_sort (sub, tcs) (Ty n Ts) S

goal (1 subgoal):
 1. \<And>x1 x2 S. has_sort (translate_osig (sub, tcs)) (Tv x1 x2) S \<Longrightarrow> exehas_sort (sub, tcs) (Tv x1 x2) S
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 S. has_sort (translate_osig (sub, tcs)) (Tv x1 x2) S \<Longrightarrow> exehas_sort (sub, tcs) (Tv x1 x2) S
[PROOF STEP]
case (Tv n S)
[PROOF STATE]
proof (state)
this:
has_sort (translate_osig (sub, tcs)) (Tv n Sa__) S

goal (1 subgoal):
 1. \<And>x1 x2 S. has_sort (translate_osig (sub, tcs)) (Tv x1 x2) S \<Longrightarrow> exehas_sort (sub, tcs) (Tv x1 x2) S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
has_sort (translate_osig (sub, tcs)) (Tv n Sa__) S
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
has_sort (translate_osig (sub, tcs)) (Tv n Sa__) S

goal (1 subgoal):
 1. exehas_sort (sub, tcs) (Tv n Sa__) S
[PROOF STEP]
using assms exesort_les_code has_sort_Tv_imp_sort_leq
[PROOF STATE]
proof (prove)
using this:
has_sort (translate_osig (sub, tcs)) (Tv n Sa__) S
exe_osig_conds (sub, tcs)
sort_leq (set ?cs) ?c1.0 ?c2.0 = exesort_leq ?cs ?c1.0 ?c2.0
has_sort ?oss (Tv ?idn ?S) ?S' \<Longrightarrow> sort_leq (subclass ?oss) ?S ?S'

goal (1 subgoal):
 1. exehas_sort (sub, tcs) (Tv n Sa__) S
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
exehas_sort (sub, tcs) (Tv n Sa__) S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma has_sort_code:
  assumes "exe_osig_conds oss"
  shows "has_sort (translate_osig oss) T S = exehas_sort oss T S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_sort (translate_osig oss) T S = exehas_sort oss T S
[PROOF STEP]
by (metis assms exehas_sort_imp_has_sort has_sort_imp_exehas_sort prod.collapse)


[STATEMENT]
lemma has_sort_code':
  assumes "exe_wf_theory' \<Theta>"
  shows "has_sort (osig (sig (translate_theory \<Theta>))) T S
    = exehas_sort (exesorts (exesig \<Theta>)) T S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_sort (osig (sig (translate_theory \<Theta>))) T S = exehas_sort (exesorts (exesig \<Theta>)) T S
[PROOF STEP]
apply (cases \<Theta> rule: exetheory_full_exhaust)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>const_type typ_arity sorts axioms. \<Theta> = ExeTheory (ExeSignature const_type typ_arity sorts) axioms \<Longrightarrow> has_sort (osig (sig (translate_theory \<Theta>))) T S = exehas_sort (exesorts (exesig \<Theta>)) T S
[PROOF STEP]
using assms has_sort_code
[PROOF STATE]
proof (prove)
using this:
exe_wf_theory' \<Theta>
exe_osig_conds ?oss \<Longrightarrow> has_sort (translate_osig ?oss) ?T ?S = exehas_sort ?oss ?T ?S

goal (1 subgoal):
 1. \<And>const_type typ_arity sorts axioms. \<Theta> = ExeTheory (ExeSignature const_type typ_arity sorts) axioms \<Longrightarrow> has_sort (osig (sig (translate_theory \<Theta>))) T S = exehas_sort (exesorts (exesig \<Theta>)) T S
[PROOF STEP]
by auto


[STATEMENT]
lemma inst_ok_code1:
  assumes "exe_wf_theory' \<Theta>"
  shows "list_all (exetyp_ok \<Theta>) (map snd insts) = list_all (typ_ok (translate_theory \<Theta>)) (map snd insts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all (exetyp_ok \<Theta>) (map snd insts) = list_all (typ_ok (translate_theory \<Theta>)) (map snd insts)
[PROOF STEP]
using assms typ_ok_code
[PROOF STATE]
proof (prove)
using this:
exe_wf_theory' \<Theta>
exe_wf_theory' ?\<Theta> \<Longrightarrow> typ_ok (translate_theory ?\<Theta>) ?ty = exetyp_ok ?\<Theta> ?ty

goal (1 subgoal):
 1. list_all (exetyp_ok \<Theta>) (map snd insts) = list_all (typ_ok (translate_theory \<Theta>)) (map snd insts)
[PROOF STEP]
by (auto simp add: list_all_iff)


[STATEMENT]
lemma inst_ok_code2:
  assumes "exe_wf_theory' \<Theta>"
  shows "list_all (\<lambda>((idn, S), T) . has_sort (osig (sig (translate_theory \<Theta>))) T S) insts
    = list_all (\<lambda>((idn, S), T) . exehas_sort (exesorts (exesig \<Theta>)) T S) insts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all (\<lambda>((idn, S), T). has_sort (osig (sig (translate_theory \<Theta>))) T S) insts = list_all (\<lambda>((idn, S), T). exehas_sort (exesorts (exesig \<Theta>)) T S) insts
[PROOF STEP]
using has_sort_code' assms
[PROOF STATE]
proof (prove)
using this:
exe_wf_theory' ?\<Theta> \<Longrightarrow> has_sort (osig (sig (translate_theory ?\<Theta>))) ?T ?S = exehas_sort (exesorts (exesig ?\<Theta>)) ?T ?S
exe_wf_theory' \<Theta>

goal (1 subgoal):
 1. list_all (\<lambda>((idn, S), T). has_sort (osig (sig (translate_theory \<Theta>))) T S) insts = list_all (\<lambda>((idn, S), T). exehas_sort (exesorts (exesig \<Theta>)) T S) insts
[PROOF STEP]
by auto


[STATEMENT]
lemma inst_ok_code:
  assumes "exe_wf_theory' \<Theta>"
  shows "inst_ok (translate_theory \<Theta>) insts = exeinst_ok \<Theta> insts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inst_ok (translate_theory \<Theta>) insts = exeinst_ok \<Theta> insts
[PROOF STEP]
using inst_ok_code1 inst_ok_code2 assms
[PROOF STATE]
proof (prove)
using this:
exe_wf_theory' ?\<Theta> \<Longrightarrow> list_all (exetyp_ok ?\<Theta>) (map snd ?insts) = list_all (typ_ok (translate_theory ?\<Theta>)) (map snd ?insts)
exe_wf_theory' ?\<Theta> \<Longrightarrow> list_all (\<lambda>((idn, S), T). has_sort (osig (sig (translate_theory ?\<Theta>))) T S) ?insts = list_all (\<lambda>((idn, S), T). exehas_sort (exesorts (exesig ?\<Theta>)) T S) ?insts
exe_wf_theory' \<Theta>

goal (1 subgoal):
 1. inst_ok (translate_theory \<Theta>) insts = exeinst_ok \<Theta> insts
[PROOF STEP]
by auto


[STATEMENT]
lemma term_ok_code:
  assumes "exe_wf_theory' \<Theta>"
  shows "term_ok (translate_theory \<Theta>) t = exeterm_ok \<Theta> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. term_ok (translate_theory \<Theta>) t = exeterm_ok \<Theta> t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
exe_wf_theory' \<Theta>

goal (1 subgoal):
 1. term_ok (translate_theory \<Theta>) t = exeterm_ok \<Theta> t
[PROOF STEP]
apply (cases \<Theta> rule: exetheory_full_exhaust)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>const_type typ_arity sorts axioms. \<lbrakk>exe_wf_theory' \<Theta>; \<Theta> = ExeTheory (ExeSignature const_type typ_arity sorts) axioms\<rbrakk> \<Longrightarrow> term_ok (translate_theory \<Theta>) t = exeterm_ok \<Theta> t
[PROOF STEP]
by (metis exe_sig_conds_def exe_wf_theory'.simps exeterm_ok_def exetheory.sel(1)
      sig.simps term_okD1 term_okD2 term_okI wt_term_code translate_theory.simps)


[STATEMENT]
lemma of_class_code1:
  assumes "exe_wf_theory' thy"
  shows "(has_sort (osig (sig (translate_theory thy))) ty {c} \<and> typ_ok (translate_theory thy) ty)
    = (exehas_sort (exesorts (exesig thy)) ty {c} \<and> exetyp_ok thy ty)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (has_sort (osig (sig (translate_theory thy))) ty (insert c full_sort) \<and> typ_ok (translate_theory thy) ty) = (exehas_sort (exesorts (exesig thy)) ty (insert c full_sort) \<and> exetyp_ok thy ty)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (has_sort (osig (sig (translate_theory thy))) ty (insert c full_sort) \<and> typ_ok (translate_theory thy) ty) = (exehas_sort (exesorts (exesig thy)) ty (insert c full_sort) \<and> exetyp_ok thy ty)
[PROOF STEP]
have "has_sort (osig (sig (translate_theory thy))) ty {c}
    = exehas_sort (exesorts (exesig thy)) ty {c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_sort (osig (sig (translate_theory thy))) ty (insert c full_sort) = exehas_sort (exesorts (exesig thy)) ty (insert c full_sort)
[PROOF STEP]
using has_sort_code' assms
[PROOF STATE]
proof (prove)
using this:
exe_wf_theory' ?\<Theta> \<Longrightarrow> has_sort (osig (sig (translate_theory ?\<Theta>))) ?T ?S = exehas_sort (exesorts (exesig ?\<Theta>)) ?T ?S
exe_wf_theory' thy

goal (1 subgoal):
 1. has_sort (osig (sig (translate_theory thy))) ty (insert c full_sort) = exehas_sort (exesorts (exesig thy)) ty (insert c full_sort)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
has_sort (osig (sig (translate_theory thy))) ty (insert c full_sort) = exehas_sort (exesorts (exesig thy)) ty (insert c full_sort)

goal (1 subgoal):
 1. (has_sort (osig (sig (translate_theory thy))) ty (insert c full_sort) \<and> typ_ok (translate_theory thy) ty) = (exehas_sort (exesorts (exesig thy)) ty (insert c full_sort) \<and> exetyp_ok thy ty)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
has_sort (osig (sig (translate_theory thy))) ty (insert c full_sort) = exehas_sort (exesorts (exesig thy)) ty (insert c full_sort)

goal (1 subgoal):
 1. (has_sort (osig (sig (translate_theory thy))) ty (insert c full_sort) \<and> typ_ok (translate_theory thy) ty) = (exehas_sort (exesorts (exesig thy)) ty (insert c full_sort) \<and> exetyp_ok thy ty)
[PROOF STEP]
have "typ_ok (translate_theory thy) ty = exetyp_ok thy ty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. typ_ok (translate_theory thy) ty = exetyp_ok thy ty
[PROOF STEP]
using typ_ok_code assms
[PROOF STATE]
proof (prove)
using this:
exe_wf_theory' ?\<Theta> \<Longrightarrow> typ_ok (translate_theory ?\<Theta>) ?ty = exetyp_ok ?\<Theta> ?ty
exe_wf_theory' thy

goal (1 subgoal):
 1. typ_ok (translate_theory thy) ty = exetyp_ok thy ty
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
typ_ok (translate_theory thy) ty = exetyp_ok thy ty

goal (1 subgoal):
 1. (has_sort (osig (sig (translate_theory thy))) ty (insert c full_sort) \<and> typ_ok (translate_theory thy) ty) = (exehas_sort (exesorts (exesig thy)) ty (insert c full_sort) \<and> exetyp_ok thy ty)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
has_sort (osig (sig (translate_theory thy))) ty (insert c full_sort) = exehas_sort (exesorts (exesig thy)) ty (insert c full_sort)
typ_ok (translate_theory thy) ty = exetyp_ok thy ty
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
has_sort (osig (sig (translate_theory thy))) ty (insert c full_sort) = exehas_sort (exesorts (exesig thy)) ty (insert c full_sort)
typ_ok (translate_theory thy) ty = exetyp_ok thy ty

goal (1 subgoal):
 1. (has_sort (osig (sig (translate_theory thy))) ty (insert c full_sort) \<and> typ_ok (translate_theory thy) ty) = (exehas_sort (exesorts (exesig thy)) ty (insert c full_sort) \<and> exetyp_ok thy ty)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(has_sort (osig (sig (translate_theory thy))) ty (insert c full_sort) \<and> typ_ok (translate_theory thy) ty) = (exehas_sort (exesorts (exesig thy)) ty (insert c full_sort) \<and> exetyp_ok thy ty)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma of_class_code2:
  assumes "exe_wf_theory' thy"
  shows "const_type (sig (translate_theory thy)) (const_of_class c)
    = lookup (\<lambda>k. k=const_of_class c) (execonst_type_of (exesig thy))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. const_type (sig (translate_theory thy)) (const_of_class c) = lookup (\<lambda>k. k = const_of_class c) (execonst_type_of (exesig thy))
[PROOF STEP]
by (metis assms const_type_of_lookup_code exe_wf_theory_code
      exe_wf_theory_translate_imp_wf_theory exetheory.sel(1) illformed_theory_not_wf_theory
      sig.simps translate_theory.elims)


[STATEMENT]
lemma replay'_code:
  assumes "exe_wf_theory' thy"
  shows "replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P
[PROOF STEP]
proof (induction P arbitrary: vs ns Hs)
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>x1 x2a vs ns Hs. replay' (translate_theory thy) vs ns Hs (PAxm x1 x2a) = exereplay' thy vs ns Hs (PAxm x1 x2a)
 2. \<And>x vs ns Hs. replay' (translate_theory thy) vs ns Hs (PBound x) = exereplay' thy vs ns Hs (PBound x)
 3. \<And>x1 P vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (Abst x1 P) = exereplay' thy vs ns Hs (Abst x1 P)
 4. \<And>x1 P vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (AbsP x1 P) = exereplay' thy vs ns Hs (AbsP x1 P)
 5. \<And>P x2a vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (Appt P x2a) = exereplay' thy vs ns Hs (Appt P x2a)
 6. \<And>P1 P2 vs ns Hs. \<lbrakk>\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P1 = exereplay' thy vs ns Hs P1; \<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P2 = exereplay' thy vs ns Hs P2\<rbrakk> \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (AppP P1 P2) = exereplay' thy vs ns Hs (AppP P1 P2)
 7. \<And>x1 x2a vs ns Hs. replay' (translate_theory thy) vs ns Hs (OfClass x1 x2a) = exereplay' thy vs ns Hs (OfClass x1 x2a)
 8. \<And>x vs ns Hs. replay' (translate_theory thy) vs ns Hs (Hyp x) = exereplay' thy vs ns Hs (Hyp x)
[PROOF STEP]
case (PAxm ax tys)
[PROOF STATE]
proof (state)
this:

goal (8 subgoals):
 1. \<And>x1 x2a vs ns Hs. replay' (translate_theory thy) vs ns Hs (PAxm x1 x2a) = exereplay' thy vs ns Hs (PAxm x1 x2a)
 2. \<And>x vs ns Hs. replay' (translate_theory thy) vs ns Hs (PBound x) = exereplay' thy vs ns Hs (PBound x)
 3. \<And>x1 P vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (Abst x1 P) = exereplay' thy vs ns Hs (Abst x1 P)
 4. \<And>x1 P vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (AbsP x1 P) = exereplay' thy vs ns Hs (AbsP x1 P)
 5. \<And>P x2a vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (Appt P x2a) = exereplay' thy vs ns Hs (Appt P x2a)
 6. \<And>P1 P2 vs ns Hs. \<lbrakk>\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P1 = exereplay' thy vs ns Hs P1; \<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P2 = exereplay' thy vs ns Hs P2\<rbrakk> \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (AppP P1 P2) = exereplay' thy vs ns Hs (AppP P1 P2)
 7. \<And>x1 x2a vs ns Hs. replay' (translate_theory thy) vs ns Hs (OfClass x1 x2a) = exereplay' thy vs ns Hs (OfClass x1 x2a)
 8. \<And>x vs ns Hs. replay' (translate_theory thy) vs ns Hs (Hyp x) = exereplay' thy vs ns Hs (Hyp x)
[PROOF STEP]
have wf: "wf_theory (translate_theory thy)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_theory (translate_theory thy)
[PROOF STEP]
by (simp add: assms exe_wf_theory_code exe_wf_theory_translate_imp_wf_theory)
[PROOF STATE]
proof (state)
this:
wf_theory (translate_theory thy)

goal (8 subgoals):
 1. \<And>x1 x2a vs ns Hs. replay' (translate_theory thy) vs ns Hs (PAxm x1 x2a) = exereplay' thy vs ns Hs (PAxm x1 x2a)
 2. \<And>x vs ns Hs. replay' (translate_theory thy) vs ns Hs (PBound x) = exereplay' thy vs ns Hs (PBound x)
 3. \<And>x1 P vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (Abst x1 P) = exereplay' thy vs ns Hs (Abst x1 P)
 4. \<And>x1 P vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (AbsP x1 P) = exereplay' thy vs ns Hs (AbsP x1 P)
 5. \<And>P x2a vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (Appt P x2a) = exereplay' thy vs ns Hs (Appt P x2a)
 6. \<And>P1 P2 vs ns Hs. \<lbrakk>\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P1 = exereplay' thy vs ns Hs P1; \<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P2 = exereplay' thy vs ns Hs P2\<rbrakk> \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (AppP P1 P2) = exereplay' thy vs ns Hs (AppP P1 P2)
 7. \<And>x1 x2a vs ns Hs. replay' (translate_theory thy) vs ns Hs (OfClass x1 x2a) = exereplay' thy vs ns Hs (OfClass x1 x2a)
 8. \<And>x vs ns Hs. replay' (translate_theory thy) vs ns Hs (Hyp x) = exereplay' thy vs ns Hs (Hyp x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wf_theory (translate_theory thy)

goal (8 subgoals):
 1. \<And>x1 x2a vs ns Hs. replay' (translate_theory thy) vs ns Hs (PAxm x1 x2a) = exereplay' thy vs ns Hs (PAxm x1 x2a)
 2. \<And>x vs ns Hs. replay' (translate_theory thy) vs ns Hs (PBound x) = exereplay' thy vs ns Hs (PBound x)
 3. \<And>x1 P vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (Abst x1 P) = exereplay' thy vs ns Hs (Abst x1 P)
 4. \<And>x1 P vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (AbsP x1 P) = exereplay' thy vs ns Hs (AbsP x1 P)
 5. \<And>P x2a vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (Appt P x2a) = exereplay' thy vs ns Hs (Appt P x2a)
 6. \<And>P1 P2 vs ns Hs. \<lbrakk>\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P1 = exereplay' thy vs ns Hs P1; \<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P2 = exereplay' thy vs ns Hs P2\<rbrakk> \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (AppP P1 P2) = exereplay' thy vs ns Hs (AppP P1 P2)
 7. \<And>x1 x2a vs ns Hs. replay' (translate_theory thy) vs ns Hs (OfClass x1 x2a) = exereplay' thy vs ns Hs (OfClass x1 x2a)
 8. \<And>x vs ns Hs. replay' (translate_theory thy) vs ns Hs (Hyp x) = exereplay' thy vs ns Hs (Hyp x)
[PROOF STEP]
have inst: "inst_ok (translate_theory thy) tys \<longleftrightarrow> exeinst_ok thy tys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inst_ok (translate_theory thy) tys = exeinst_ok thy tys
[PROOF STEP]
by (simp add: assms inst_ok_code1 inst_ok_code2)
[PROOF STATE]
proof (state)
this:
inst_ok (translate_theory thy) tys = exeinst_ok thy tys

goal (8 subgoals):
 1. \<And>x1 x2a vs ns Hs. replay' (translate_theory thy) vs ns Hs (PAxm x1 x2a) = exereplay' thy vs ns Hs (PAxm x1 x2a)
 2. \<And>x vs ns Hs. replay' (translate_theory thy) vs ns Hs (PBound x) = exereplay' thy vs ns Hs (PBound x)
 3. \<And>x1 P vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (Abst x1 P) = exereplay' thy vs ns Hs (Abst x1 P)
 4. \<And>x1 P vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (AbsP x1 P) = exereplay' thy vs ns Hs (AbsP x1 P)
 5. \<And>P x2a vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (Appt P x2a) = exereplay' thy vs ns Hs (Appt P x2a)
 6. \<And>P1 P2 vs ns Hs. \<lbrakk>\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P1 = exereplay' thy vs ns Hs P1; \<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P2 = exereplay' thy vs ns Hs P2\<rbrakk> \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (AppP P1 P2) = exereplay' thy vs ns Hs (AppP P1 P2)
 7. \<And>x1 x2a vs ns Hs. replay' (translate_theory thy) vs ns Hs (OfClass x1 x2a) = exereplay' thy vs ns Hs (OfClass x1 x2a)
 8. \<And>x vs ns Hs. replay' (translate_theory thy) vs ns Hs (Hyp x) = exereplay' thy vs ns Hs (Hyp x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
inst_ok (translate_theory thy) tys = exeinst_ok thy tys

goal (8 subgoals):
 1. \<And>x1 x2a vs ns Hs. replay' (translate_theory thy) vs ns Hs (PAxm x1 x2a) = exereplay' thy vs ns Hs (PAxm x1 x2a)
 2. \<And>x vs ns Hs. replay' (translate_theory thy) vs ns Hs (PBound x) = exereplay' thy vs ns Hs (PBound x)
 3. \<And>x1 P vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (Abst x1 P) = exereplay' thy vs ns Hs (Abst x1 P)
 4. \<And>x1 P vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (AbsP x1 P) = exereplay' thy vs ns Hs (AbsP x1 P)
 5. \<And>P x2a vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (Appt P x2a) = exereplay' thy vs ns Hs (Appt P x2a)
 6. \<And>P1 P2 vs ns Hs. \<lbrakk>\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P1 = exereplay' thy vs ns Hs P1; \<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P2 = exereplay' thy vs ns Hs P2\<rbrakk> \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (AppP P1 P2) = exereplay' thy vs ns Hs (AppP P1 P2)
 7. \<And>x1 x2a vs ns Hs. replay' (translate_theory thy) vs ns Hs (OfClass x1 x2a) = exereplay' thy vs ns Hs (OfClass x1 x2a)
 8. \<And>x vs ns Hs. replay' (translate_theory thy) vs ns Hs (Hyp x) = exereplay' thy vs ns Hs (Hyp x)
[PROOF STEP]
have tok: "term_ok (translate_theory thy) ax \<longleftrightarrow> exeterm_ok thy ax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. term_ok (translate_theory thy) ax = exeterm_ok thy ax
[PROOF STEP]
using assms term_ok_code
[PROOF STATE]
proof (prove)
using this:
exe_wf_theory' thy
exe_wf_theory' ?\<Theta> \<Longrightarrow> term_ok (translate_theory ?\<Theta>) ?t = exeterm_ok ?\<Theta> ?t

goal (1 subgoal):
 1. term_ok (translate_theory thy) ax = exeterm_ok thy ax
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
term_ok (translate_theory thy) ax = exeterm_ok thy ax

goal (8 subgoals):
 1. \<And>x1 x2a vs ns Hs. replay' (translate_theory thy) vs ns Hs (PAxm x1 x2a) = exereplay' thy vs ns Hs (PAxm x1 x2a)
 2. \<And>x vs ns Hs. replay' (translate_theory thy) vs ns Hs (PBound x) = exereplay' thy vs ns Hs (PBound x)
 3. \<And>x1 P vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (Abst x1 P) = exereplay' thy vs ns Hs (Abst x1 P)
 4. \<And>x1 P vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (AbsP x1 P) = exereplay' thy vs ns Hs (AbsP x1 P)
 5. \<And>P x2a vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (Appt P x2a) = exereplay' thy vs ns Hs (Appt P x2a)
 6. \<And>P1 P2 vs ns Hs. \<lbrakk>\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P1 = exereplay' thy vs ns Hs P1; \<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P2 = exereplay' thy vs ns Hs P2\<rbrakk> \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (AppP P1 P2) = exereplay' thy vs ns Hs (AppP P1 P2)
 7. \<And>x1 x2a vs ns Hs. replay' (translate_theory thy) vs ns Hs (OfClass x1 x2a) = exereplay' thy vs ns Hs (OfClass x1 x2a)
 8. \<And>x vs ns Hs. replay' (translate_theory thy) vs ns Hs (Hyp x) = exereplay' thy vs ns Hs (Hyp x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
term_ok (translate_theory thy) ax = exeterm_ok thy ax

goal (8 subgoals):
 1. \<And>x1 x2a vs ns Hs. replay' (translate_theory thy) vs ns Hs (PAxm x1 x2a) = exereplay' thy vs ns Hs (PAxm x1 x2a)
 2. \<And>x vs ns Hs. replay' (translate_theory thy) vs ns Hs (PBound x) = exereplay' thy vs ns Hs (PBound x)
 3. \<And>x1 P vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (Abst x1 P) = exereplay' thy vs ns Hs (Abst x1 P)
 4. \<And>x1 P vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (AbsP x1 P) = exereplay' thy vs ns Hs (AbsP x1 P)
 5. \<And>P x2a vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (Appt P x2a) = exereplay' thy vs ns Hs (Appt P x2a)
 6. \<And>P1 P2 vs ns Hs. \<lbrakk>\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P1 = exereplay' thy vs ns Hs P1; \<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P2 = exereplay' thy vs ns Hs P2\<rbrakk> \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (AppP P1 P2) = exereplay' thy vs ns Hs (AppP P1 P2)
 7. \<And>x1 x2a vs ns Hs. replay' (translate_theory thy) vs ns Hs (OfClass x1 x2a) = exereplay' thy vs ns Hs (OfClass x1 x2a)
 8. \<And>x vs ns Hs. replay' (translate_theory thy) vs ns Hs (Hyp x) = exereplay' thy vs ns Hs (Hyp x)
[PROOF STEP]
have ax: "ax \<in> axioms (translate_theory thy) \<longleftrightarrow> ax \<in> set (exeaxioms_of thy)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ax \<in> axioms (translate_theory thy)) = (ax \<in> set (exeaxioms_of thy))
[PROOF STEP]
by (metis axioms.simps wf exetheory.sel(2) illformed_theory_not_wf_theory translate_theory.elims)
[PROOF STATE]
proof (state)
this:
(ax \<in> axioms (translate_theory thy)) = (ax \<in> set (exeaxioms_of thy))

goal (8 subgoals):
 1. \<And>x1 x2a vs ns Hs. replay' (translate_theory thy) vs ns Hs (PAxm x1 x2a) = exereplay' thy vs ns Hs (PAxm x1 x2a)
 2. \<And>x vs ns Hs. replay' (translate_theory thy) vs ns Hs (PBound x) = exereplay' thy vs ns Hs (PBound x)
 3. \<And>x1 P vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (Abst x1 P) = exereplay' thy vs ns Hs (Abst x1 P)
 4. \<And>x1 P vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (AbsP x1 P) = exereplay' thy vs ns Hs (AbsP x1 P)
 5. \<And>P x2a vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (Appt P x2a) = exereplay' thy vs ns Hs (Appt P x2a)
 6. \<And>P1 P2 vs ns Hs. \<lbrakk>\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P1 = exereplay' thy vs ns Hs P1; \<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P2 = exereplay' thy vs ns Hs P2\<rbrakk> \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (AppP P1 P2) = exereplay' thy vs ns Hs (AppP P1 P2)
 7. \<And>x1 x2a vs ns Hs. replay' (translate_theory thy) vs ns Hs (OfClass x1 x2a) = exereplay' thy vs ns Hs (OfClass x1 x2a)
 8. \<And>x vs ns Hs. replay' (translate_theory thy) vs ns Hs (Hyp x) = exereplay' thy vs ns Hs (Hyp x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
wf_theory (translate_theory thy)
inst_ok (translate_theory thy) tys = exeinst_ok thy tys
term_ok (translate_theory thy) ax = exeterm_ok thy ax
(ax \<in> axioms (translate_theory thy)) = (ax \<in> set (exeaxioms_of thy))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
wf_theory (translate_theory thy)
inst_ok (translate_theory thy) tys = exeinst_ok thy tys
term_ok (translate_theory thy) ax = exeterm_ok thy ax
(ax \<in> axioms (translate_theory thy)) = (ax \<in> set (exeaxioms_of thy))

goal (1 subgoal):
 1. replay' (translate_theory thy) vs ns Hs (PAxm ax tys) = exereplay' thy vs ns Hs (PAxm ax tys)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
replay' (translate_theory thy) vs ns Hs (PAxm ax tys) = exereplay' thy vs ns Hs (PAxm ax tys)

goal (7 subgoals):
 1. \<And>x vs ns Hs. replay' (translate_theory thy) vs ns Hs (PBound x) = exereplay' thy vs ns Hs (PBound x)
 2. \<And>x1 P vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (Abst x1 P) = exereplay' thy vs ns Hs (Abst x1 P)
 3. \<And>x1 P vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (AbsP x1 P) = exereplay' thy vs ns Hs (AbsP x1 P)
 4. \<And>P x2a vs ns Hs. (\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P = exereplay' thy vs ns Hs P) \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (Appt P x2a) = exereplay' thy vs ns Hs (Appt P x2a)
 5. \<And>P1 P2 vs ns Hs. \<lbrakk>\<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P1 = exereplay' thy vs ns Hs P1; \<And>vs ns Hs. replay' (translate_theory thy) vs ns Hs P2 = exereplay' thy vs ns Hs P2\<rbrakk> \<Longrightarrow> replay' (translate_theory thy) vs ns Hs (AppP P1 P2) = exereplay' thy vs ns Hs (AppP P1 P2)
 6. \<And>x1 x2a vs ns Hs. replay' (translate_theory thy) vs ns Hs (OfClass x1 x2a) = exereplay' thy vs ns Hs (OfClass x1 x2a)
 7. \<And>x vs ns Hs. replay' (translate_theory thy) vs ns Hs (Hyp x) = exereplay' thy vs ns Hs (Hyp x)
[PROOF STEP]
qed (use assms term_ok_code typ_ok_code of_class_code1 of_class_code2
      in \<open>auto simp only: replay'.simps exereplay'.simps split: if_splits\<close>)


[STATEMENT]
lemma replay''_code:
  assumes "exe_wf_theory' thy"
  shows "replay'' (translate_theory thy) vs ns Hs P = exereplay'' thy vs ns Hs P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. replay'' (translate_theory thy) vs ns Hs P = exereplay'' thy vs ns Hs P
[PROOF STEP]
by (simp add: assms replay'_code)


[STATEMENT]
lemma replay_code:
  assumes "exe_wf_theory' thy"
  shows "replay (translate_theory thy) P = exereplay thy P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. replay (translate_theory thy) P = exereplay thy P
[PROOF STEP]
using assms replay''_code term_ok_code
[PROOF STATE]
proof (prove)
using this:
exe_wf_theory' thy
exe_wf_theory' ?thy \<Longrightarrow> replay'' (translate_theory ?thy) ?vs ?ns ?Hs ?P = exereplay'' ?thy ?vs ?ns ?Hs ?P
exe_wf_theory' ?\<Theta> \<Longrightarrow> term_ok (translate_theory ?\<Theta>) ?t = exeterm_ok ?\<Theta> ?t

goal (1 subgoal):
 1. replay (translate_theory thy) P = exereplay thy P
[PROOF STEP]
by auto


[STATEMENT]
lemma exe_check_proof_iff_check_proof:
  "exe_check_proof e P res \<longleftrightarrow> check_proof (translate_theory e) P res"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exe_check_proof e P res = check_proof (translate_theory e) P res
[PROOF STEP]
using check_proof_def exe_check_proof_def wf_theory_translate_iff_exe_wf_theory
[PROOF STATE]
proof (prove)
using this:
check_proof ?thy ?P ?res \<equiv> wf_theory ?thy \<and> replay ?thy ?P = Some ?res
exe_check_proof ?e ?P ?res \<equiv> exe_wf_theory' ?e \<and> exereplay ?e ?P = Some ?res
wf_theory (translate_theory ?a) = exe_wf_theory ?a

goal (1 subgoal):
 1. exe_check_proof e P res = check_proof (translate_theory e) P res
[PROOF STEP]
by (metis exe_wf_theory_code replay_code)


[STATEMENT]
lemma check_proof_sound:
  shows "exe_check_proof e P res \<Longrightarrow> translate_theory e, set (hyps P) \<turnstile> res"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exe_check_proof e P res \<Longrightarrow> translate_theory e,set (hyps P) \<turnstile> res
[PROOF STEP]
by (simp add: check_proof_sound exe_check_proof_iff_check_proof)


[STATEMENT]
lemma check_proof_really_sound:
  shows "exe_check_proof e P res \<Longrightarrow> translate_theory e, set (hyps P) \<tturnstile> res"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exe_check_proof e P res \<Longrightarrow> translate_theory e,set (hyps P) \<tturnstile> res
[PROOF STEP]
by (simp add: check_proof_really_sound exe_check_proof_iff_check_proof)


[STATEMENT]
theorem HT_idem: "HT(HT(P)) = HT(P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HT (HT P) = HT P
[PROOF STEP]
by rel_auto


[STATEMENT]
theorem HT_mono: "P \<sqsubseteq> Q \<Longrightarrow> HT(P) \<sqsubseteq> HT(Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<sqsubseteq> Q \<Longrightarrow> HT P \<sqsubseteq> HT Q
[PROOF STEP]
by rel_auto


[STATEMENT]
theorem HT_continuous: "Continuous HT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Continuous HT
[PROOF STEP]
by rel_auto


[STATEMENT]
lemma HT_Wait: "HT(Wait(n)) = Wait(n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HT (Wait n) = Wait n
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma HT_Wait_closed [closure]: "Wait(n) is HT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Wait n is HT
[PROOF STEP]
by (simp add: HT_Wait Healthy_def)


[STATEMENT]
lemma HT_skip_closed [closure]: "II is HT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. II is HT
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma HT_seqr_closed [closure]:
  "\<lbrakk> P is HT; Q is HT \<rbrakk> \<Longrightarrow> P ;; Q is HT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P is HT; Q is HT\<rbrakk> \<Longrightarrow> P ;; Q is HT
[PROOF STEP]
by (rel_auto, meson dual_order.trans) \<comment> \<open> Sledgehammer required \<close>


[STATEMENT]
lemma HT_assign_closed [closure]: "\<lbrakk> vwb_lens x; clock \<bowtie> x \<rbrakk> \<Longrightarrow> x := v is HT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vwb_lens x; clock \<bowtie> x\<rbrakk> \<Longrightarrow> x := v is HT
[PROOF STEP]
by (rel_auto, metis (mono_tags, lifting) eq_iff lens.select_convs(1) lens_indep_get st_time.select_convs(1))


[STATEMENT]
lemma HT_assign_closed' [closure]: "\<lbrakk> vwb_lens x; x \<subseteq>\<^sub>L st \<rbrakk> \<Longrightarrow> x := v is HT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vwb_lens x; x \<subseteq>\<^sub>L st\<rbrakk> \<Longrightarrow> x := v is HT
[PROOF STEP]
by (rel_auto)


[STATEMENT]
theorem Wait_skip: "Wait(0) = II"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Wait 0 = II
[PROOF STEP]
by (rel_auto)


[STATEMENT]
theorem Wait_Wait: "Wait(m) ;; Wait(n) = Wait (m + n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Wait m ;; Wait n = Wait (m + n)
[PROOF STEP]
by (rel_auto)


[STATEMENT]
theorem Wait_cond: "Wait(m) ;; (P \<triangleleft> b \<triangleright>\<^sub>r Q) = (Wait m ;; P) \<triangleleft> b\<lbrakk>&clock+\<guillemotleft>m\<guillemotright>/&clock\<rbrakk> \<triangleright>\<^sub>r (Wait m ;; Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Wait m ;; (P \<triangleleft> b \<triangleright>\<^sub>r Q) = Wait m ;; P \<triangleleft> b\<lbrakk>&clock + \<guillemotleft>m\<guillemotright>/&clock\<rbrakk> \<triangleright>\<^sub>r Wait m ;; Q
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma cfun_map_below_ID:
  assumes e: "e \<sqsubseteq> ID"
  shows "cfun_map\<cdot>e\<cdot>e \<sqsubseteq> ID"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cfun_map\<cdot>e\<cdot>e \<sqsubseteq> ID
[PROOF STEP]
proof(intro cfun_belowI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. cfun_map\<cdot>e\<cdot>e\<cdot>x\<cdot>xa \<sqsubseteq> ID\<cdot>x\<cdot>xa
[PROOF STEP]
fix f x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. cfun_map\<cdot>e\<cdot>e\<cdot>x\<cdot>xa \<sqsubseteq> ID\<cdot>x\<cdot>xa
[PROOF STEP]
from e
[PROOF STATE]
proof (chain)
picking this:
e \<sqsubseteq> ID
[PROOF STEP]
have "cfun_map\<cdot>e\<cdot>e\<cdot>f\<cdot>x \<sqsubseteq> ID\<cdot>(f\<cdot>(ID\<cdot>x))"
[PROOF STATE]
proof (prove)
using this:
e \<sqsubseteq> ID

goal (1 subgoal):
 1. cfun_map\<cdot>e\<cdot>e\<cdot>f\<cdot>x \<sqsubseteq> ID\<cdot>(f\<cdot>(ID\<cdot>x))
[PROOF STEP]
by (simp del: ID1) (fast intro: monofun_cfun)
[PROOF STATE]
proof (state)
this:
cfun_map\<cdot>e\<cdot>e\<cdot>f\<cdot>x \<sqsubseteq> ID\<cdot>(f\<cdot>(ID\<cdot>x))

goal (1 subgoal):
 1. \<And>x xa. cfun_map\<cdot>e\<cdot>e\<cdot>x\<cdot>xa \<sqsubseteq> ID\<cdot>x\<cdot>xa
[PROOF STEP]
thus "cfun_map\<cdot>e\<cdot>e\<cdot>f\<cdot>x \<sqsubseteq> ID\<cdot>f\<cdot>x"
[PROOF STATE]
proof (prove)
using this:
cfun_map\<cdot>e\<cdot>e\<cdot>f\<cdot>x \<sqsubseteq> ID\<cdot>(f\<cdot>(ID\<cdot>x))

goal (1 subgoal):
 1. cfun_map\<cdot>e\<cdot>e\<cdot>f\<cdot>x \<sqsubseteq> ID\<cdot>f\<cdot>x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cfun_map\<cdot>e\<cdot>e\<cdot>f\<cdot>x \<sqsubseteq> ID\<cdot>f\<cdot>x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cfun_below_ID:
  "\<lbrakk> f \<sqsubseteq> ID; x \<sqsubseteq> y \<rbrakk> \<Longrightarrow> f\<cdot>x \<sqsubseteq> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<sqsubseteq> ID; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f\<cdot>x \<sqsubseteq> y
[PROOF STEP]
by (auto simp: cfun_below_iff elim: below_trans)


[STATEMENT]
lemma oo_below:
  "\<lbrakk> f \<sqsubseteq> f'; g \<sqsubseteq> g' \<rbrakk> \<Longrightarrow> f oo g \<sqsubseteq> f' oo g'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<sqsubseteq> f'; g \<sqsubseteq> g'\<rbrakk> \<Longrightarrow> f oo g \<sqsubseteq> f' oo g'
[PROOF STEP]
by (simp add: oo_def cfun_below_iff monofun_cfun)


[STATEMENT]
lemma cont_case_nat[simp]:
  "\<lbrakk>cont (\<lambda>x. f x); \<And>n. cont (\<lambda>x. g x n) \<rbrakk> \<Longrightarrow> cont (\<lambda>x. case_nat (f x) (g x) n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cont f; \<And>n. cont (\<lambda>x. g x n)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. case n of 0 \<Rightarrow> f x | Suc xa \<Rightarrow> g x xa)
[PROOF STEP]
by (cases n, simp_all)


[STATEMENT]
lemma cont2cont_if_below_const [cont2cont, simp]:
  assumes f: "cont (\<lambda>x. f x)" and g: "cont (\<lambda>x. g x)"
  shows "cont (\<lambda>x. if f x \<sqsubseteq> d then \<bottom> else g x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont (\<lambda>x. if f x \<sqsubseteq> d then \<bottom> else g x)
[PROOF STEP]
proof (rule cont_apply [OF f])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. cont (\<lambda>y. if y \<sqsubseteq> d then \<bottom> else g x)
 2. \<And>y. cont (\<lambda>x. if y \<sqsubseteq> d then \<bottom> else g x)
[PROOF STEP]
show "\<And>x. cont (\<lambda>y. if y \<sqsubseteq> d then \<bottom> else g x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. cont (\<lambda>y. if y \<sqsubseteq> d then \<bottom> else g x)
[PROOF STEP]
unfolding cont_def is_lub_def is_ub_def ball_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>Y. chain Y \<longrightarrow> (\<forall>xa. (if Y xa \<sqsubseteq> d then \<bottom> else g x) \<sqsubseteq> (if Lub Y \<sqsubseteq> d then \<bottom> else g x)) \<and> (\<forall>u. (\<forall>xa. (if Y xa \<sqsubseteq> d then \<bottom> else g x) \<sqsubseteq> u) \<longrightarrow> (if Lub Y \<sqsubseteq> d then \<bottom> else g x) \<sqsubseteq> u)
[PROOF STEP]
by (simp add: lub_below_iff)
[PROOF STATE]
proof (state)
this:
cont (\<lambda>y. if y \<sqsubseteq> d then \<bottom> else g ?x)

goal (1 subgoal):
 1. \<And>y. cont (\<lambda>x. if y \<sqsubseteq> d then \<bottom> else g x)
[PROOF STEP]
show "\<And>y. cont (\<lambda>x. if y \<sqsubseteq> d then \<bottom> else g x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. cont (\<lambda>x. if y \<sqsubseteq> d then \<bottom> else g x)
[PROOF STEP]
by (simp add: g)
[PROOF STATE]
proof (state)
this:
cont (\<lambda>x. if ?y \<sqsubseteq> d then \<bottom> else g x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cont2cont_foldl [simp, cont2cont]:
  fixes f :: "'a::cpo \<Rightarrow> 'b::cpo \<Rightarrow> 'c::cpo \<Rightarrow> 'b"
  fixes xs :: "'c list"
  fixes z :: "'a \<Rightarrow> 'b"
  assumes "cont (\<lambda>(x, y, z). f x y z)"
  assumes "cont z"
  shows "cont (\<lambda>x. foldl (f x) (z x) xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont (\<lambda>x. foldl (f x) (z x) xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cont (\<lambda>(x, y, z). f x y z)
cont z

goal (1 subgoal):
 1. cont (\<lambda>x. foldl (f x) (z x) xs)
[PROOF STEP]
by (induct xs rule: rev_induct) (auto simp: prod_cont_iff intro: cont_apply)


[STATEMENT]
lemma cont2cont_foldr [simp, cont2cont]:
  fixes f :: "'a::cpo \<Rightarrow> 'c::cpo \<Rightarrow> 'b::cpo \<Rightarrow> 'b"
  fixes xs :: "'c list"
  fixes z :: "'a \<Rightarrow> 'b"
  assumes "cont (\<lambda>(x, y, z). f x y z)"
  assumes "cont z"
  shows "cont (\<lambda>x. foldr (f x) xs (z x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cont (\<lambda>x. foldr (f x) xs (z x))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
cont (\<lambda>(x, y, z). f x y z)
cont z

goal (1 subgoal):
 1. cont (\<lambda>x. foldr (f x) xs (z x))
[PROOF STEP]
by (induct xs) (auto simp: prod_cont_iff intro: cont_apply)


[STATEMENT]
lemma fix_argument_promote:
  assumes "cont g"
  shows "(\<Lambda> x. fix\<cdot>(g x)) = fix\<cdot>(\<Lambda> f x. g x\<cdot>(f\<cdot>x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> x. fix\<cdot>(g x)) = (\<mu> f. \<Lambda> x. g x\<cdot>(f\<cdot>x))
[PROOF STEP]
proof(rule below_antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<Lambda> x. fix\<cdot>(g x)) \<sqsubseteq> (\<mu> f. \<Lambda> x. g x\<cdot>(f\<cdot>x))
 2. (\<mu> f. \<Lambda> x. g x\<cdot>(f\<cdot>x)) \<sqsubseteq> (\<Lambda> x. fix\<cdot>(g x))
[PROOF STEP]
have "(\<Lambda> x. g x\<cdot>(fix\<cdot>(g x))) = (\<Lambda> x. fix\<cdot>(g x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> x. g x\<cdot>(fix\<cdot>(g x))) = (\<Lambda> x. fix\<cdot>(g x))
[PROOF STEP]
by (subst fix_eq) simp
[PROOF STATE]
proof (state)
this:
(\<Lambda> x. g x\<cdot>(fix\<cdot>(g x))) = (\<Lambda> x. fix\<cdot>(g x))

goal (2 subgoals):
 1. (\<Lambda> x. fix\<cdot>(g x)) \<sqsubseteq> (\<mu> f. \<Lambda> x. g x\<cdot>(f\<cdot>x))
 2. (\<mu> f. \<Lambda> x. g x\<cdot>(f\<cdot>x)) \<sqsubseteq> (\<Lambda> x. fix\<cdot>(g x))
[PROOF STEP]
with \<open>cont g\<close>
[PROOF STATE]
proof (chain)
picking this:
cont g
(\<Lambda> x. g x\<cdot>(fix\<cdot>(g x))) = (\<Lambda> x. fix\<cdot>(g x))
[PROOF STEP]
show "fix\<cdot>(\<Lambda> f x. g x\<cdot>(f\<cdot>x)) \<sqsubseteq> (\<Lambda> x. fix\<cdot>(g x))"
[PROOF STATE]
proof (prove)
using this:
cont g
(\<Lambda> x. g x\<cdot>(fix\<cdot>(g x))) = (\<Lambda> x. fix\<cdot>(g x))

goal (1 subgoal):
 1. (\<mu> f. \<Lambda> x. g x\<cdot>(f\<cdot>x)) \<sqsubseteq> (\<Lambda> x. fix\<cdot>(g x))
[PROOF STEP]
by (simp add: fix_least cont2cont_LAM)
[PROOF STATE]
proof (state)
this:
(\<mu> f. \<Lambda> x. g x\<cdot>(f\<cdot>x)) \<sqsubseteq> (\<Lambda> x. fix\<cdot>(g x))

goal (1 subgoal):
 1. (\<Lambda> x. fix\<cdot>(g x)) \<sqsubseteq> (\<mu> f. \<Lambda> x. g x\<cdot>(f\<cdot>x))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Lambda> x. fix\<cdot>(g x)) \<sqsubseteq> (\<mu> f. \<Lambda> x. g x\<cdot>(f\<cdot>x))
[PROOF STEP]
show "(\<Lambda> x. fix\<cdot>(g x)) \<sqsubseteq> fix\<cdot>(\<Lambda> f x. g x\<cdot>(f\<cdot>x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> x. fix\<cdot>(g x)) \<sqsubseteq> (\<mu> f. \<Lambda> x. g x\<cdot>(f\<cdot>x))
[PROOF STEP]
proof(rule cfun_belowI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<Lambda> x. fix\<cdot>(g x))\<cdot>x \<sqsubseteq> (\<mu> f. \<Lambda> x. g x\<cdot>(f\<cdot>x))\<cdot>x
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<Lambda> x. fix\<cdot>(g x))\<cdot>x \<sqsubseteq> (\<mu> f. \<Lambda> x. g x\<cdot>(f\<cdot>x))\<cdot>x
[PROOF STEP]
from \<open>cont g\<close>
[PROOF STATE]
proof (chain)
picking this:
cont g
[PROOF STEP]
have "g y\<cdot>(fix\<cdot>(\<Lambda> f x. g x\<cdot>(f\<cdot>x))\<cdot>y) = fix\<cdot>(\<Lambda> f x. g x\<cdot>(f\<cdot>x))\<cdot>y"
[PROOF STATE]
proof (prove)
using this:
cont g

goal (1 subgoal):
 1. g y\<cdot>((\<mu> f. \<Lambda> x. g x\<cdot>(f\<cdot>x))\<cdot>y) = (\<mu> f. \<Lambda> x. g x\<cdot>(f\<cdot>x))\<cdot>y
[PROOF STEP]
by (subst fix_eq, simp add: cont2cont_LAM)
[PROOF STATE]
proof (state)
this:
g y\<cdot>((\<mu> f. \<Lambda> x. g x\<cdot>(f\<cdot>x))\<cdot>y) = (\<mu> f. \<Lambda> x. g x\<cdot>(f\<cdot>x))\<cdot>y

goal (1 subgoal):
 1. \<And>x. (\<Lambda> x. fix\<cdot>(g x))\<cdot>x \<sqsubseteq> (\<mu> f. \<Lambda> x. g x\<cdot>(f\<cdot>x))\<cdot>x
[PROOF STEP]
with \<open>cont g\<close>
[PROOF STATE]
proof (chain)
picking this:
cont g
g y\<cdot>((\<mu> f. \<Lambda> x. g x\<cdot>(f\<cdot>x))\<cdot>y) = (\<mu> f. \<Lambda> x. g x\<cdot>(f\<cdot>x))\<cdot>y
[PROOF STEP]
show "(\<Lambda> x. fix\<cdot>(g x))\<cdot>y \<sqsubseteq> fix\<cdot>(\<Lambda> f x. g x\<cdot>(f\<cdot>x))\<cdot>y"
[PROOF STATE]
proof (prove)
using this:
cont g
g y\<cdot>((\<mu> f. \<Lambda> x. g x\<cdot>(f\<cdot>x))\<cdot>y) = (\<mu> f. \<Lambda> x. g x\<cdot>(f\<cdot>x))\<cdot>y

goal (1 subgoal):
 1. (\<Lambda> x. fix\<cdot>(g x))\<cdot>y \<sqsubseteq> (\<mu> f. \<Lambda> x. g x\<cdot>(f\<cdot>x))\<cdot>y
[PROOF STEP]
by (simp add: fix_least)
[PROOF STATE]
proof (state)
this:
(\<Lambda> x. fix\<cdot>(g x))\<cdot>y \<sqsubseteq> (\<mu> f. \<Lambda> x. g x\<cdot>(f\<cdot>x))\<cdot>y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Lambda> x. fix\<cdot>(g x)) \<sqsubseteq> (\<mu> f. \<Lambda> x. g x\<cdot>(f\<cdot>x))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fix_argument_promote_fun:
  fixes g :: "'a::type \<Rightarrow> 'b::pcpo \<rightarrow> 'b"
  shows "(\<lambda>x. fix\<cdot>(g x)) = (\<mu> f. (\<lambda>x. g x\<cdot>(f x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. fix\<cdot>(g x)) = (\<mu> x. (\<lambda>xa. g xa\<cdot>(x xa)))
[PROOF STEP]
proof(rule below_antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>x. fix\<cdot>(g x)) \<sqsubseteq> (\<mu> x. (\<lambda>xa. g xa\<cdot>(x xa)))
 2. (\<mu> x. (\<lambda>xa. g xa\<cdot>(x xa))) \<sqsubseteq> (\<lambda>x. fix\<cdot>(g x))
[PROOF STEP]
have "(\<lambda>x. g x\<cdot>(fix\<cdot>(g x))) = (\<lambda>x. fix\<cdot>(g x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. g x\<cdot>(fix\<cdot>(g x))) = (\<lambda>x. fix\<cdot>(g x))
[PROOF STEP]
by (subst fix_eq) simp
[PROOF STATE]
proof (state)
this:
(\<lambda>x. g x\<cdot>(fix\<cdot>(g x))) = (\<lambda>x. fix\<cdot>(g x))

goal (2 subgoals):
 1. (\<lambda>x. fix\<cdot>(g x)) \<sqsubseteq> (\<mu> x. (\<lambda>xa. g xa\<cdot>(x xa)))
 2. (\<mu> x. (\<lambda>xa. g xa\<cdot>(x xa))) \<sqsubseteq> (\<lambda>x. fix\<cdot>(g x))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. g x\<cdot>(fix\<cdot>(g x))) = (\<lambda>x. fix\<cdot>(g x))
[PROOF STEP]
show "(\<mu> f. (\<lambda>x. g x\<cdot>(f x))) \<sqsubseteq> (\<lambda>x. fix\<cdot>(g x))"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. g x\<cdot>(fix\<cdot>(g x))) = (\<lambda>x. fix\<cdot>(g x))

goal (1 subgoal):
 1. (\<mu> x. (\<lambda>xa. g xa\<cdot>(x xa))) \<sqsubseteq> (\<lambda>x. fix\<cdot>(g x))
[PROOF STEP]
by (simp add: fix_least cont_fun)
[PROOF STATE]
proof (state)
this:
(\<mu> x. (\<lambda>xa. g xa\<cdot>(x xa))) \<sqsubseteq> (\<lambda>x. fix\<cdot>(g x))

goal (1 subgoal):
 1. (\<lambda>x. fix\<cdot>(g x)) \<sqsubseteq> (\<mu> x. (\<lambda>xa. g xa\<cdot>(x xa)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. fix\<cdot>(g x)) \<sqsubseteq> (\<mu> x. (\<lambda>xa. g xa\<cdot>(x xa)))
[PROOF STEP]
show "(\<lambda>x. fix\<cdot>(g x)) \<sqsubseteq> (\<mu> f. (\<lambda>x. g x\<cdot>(f x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. fix\<cdot>(g x)) \<sqsubseteq> (\<mu> x. (\<lambda>xa. g xa\<cdot>(x xa)))
[PROOF STEP]
proof(rule fun_belowI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. fix\<cdot>(g x) \<sqsubseteq> (\<mu> x. (\<lambda>xa. g xa\<cdot>(x xa))) x
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. fix\<cdot>(g x) \<sqsubseteq> (\<mu> x. (\<lambda>xa. g xa\<cdot>(x xa))) x
[PROOF STEP]
have "g y\<cdot>((\<mu> f. (\<lambda>x. g x\<cdot>(f x))) y) = (\<mu> f. (\<lambda>x. g x\<cdot>(f x))) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g y\<cdot>((\<mu> x. (\<lambda>xa. g xa\<cdot>(x xa))) y) = (\<mu> x. (\<lambda>xa. g xa\<cdot>(x xa))) y
[PROOF STEP]
by (subst fix_eq, simp add: cont_fun)
[PROOF STATE]
proof (state)
this:
g y\<cdot>((\<mu> x. (\<lambda>xa. g xa\<cdot>(x xa))) y) = (\<mu> x. (\<lambda>xa. g xa\<cdot>(x xa))) y

goal (1 subgoal):
 1. \<And>x. fix\<cdot>(g x) \<sqsubseteq> (\<mu> x. (\<lambda>xa. g xa\<cdot>(x xa))) x
[PROOF STEP]
thus "fix\<cdot>(g y) \<sqsubseteq> (\<mu> f. (\<lambda>x. g x\<cdot>(f x))) y"
[PROOF STATE]
proof (prove)
using this:
g y\<cdot>((\<mu> x. (\<lambda>xa. g xa\<cdot>(x xa))) y) = (\<mu> x. (\<lambda>xa. g xa\<cdot>(x xa))) y

goal (1 subgoal):
 1. fix\<cdot>(g y) \<sqsubseteq> (\<mu> x. (\<lambda>xa. g xa\<cdot>(x xa))) y
[PROOF STEP]
by (simp add: fix_least)
[PROOF STATE]
proof (state)
this:
fix\<cdot>(g y) \<sqsubseteq> (\<mu> x. (\<lambda>xa. g xa\<cdot>(x xa))) y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>x. fix\<cdot>(g x)) \<sqsubseteq> (\<mu> x. (\<lambda>xa. g xa\<cdot>(x xa)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma adm_cart_prod [intro, simp]:
  assumes X: "adm (\<lambda>x. x \<in> X)"
  assumes Y: "adm (\<lambda>x. x \<in> Y)"
  shows "adm (\<lambda>x. x \<in> X \<times> Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adm (\<lambda>x. x \<in> X \<times> Y)
[PROOF STEP]
proof(rule admI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Ya. \<lbrakk>chain Ya; \<forall>i. Ya i \<in> X \<times> Y\<rbrakk> \<Longrightarrow> (\<Squnion>i. Ya i) \<in> X \<times> Y
[PROOF STEP]
fix A
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Ya. \<lbrakk>chain Ya; \<forall>i. Ya i \<in> X \<times> Y\<rbrakk> \<Longrightarrow> (\<Squnion>i. Ya i) \<in> X \<times> Y
[PROOF STEP]
assume A: "chain A" and Ai: "\<forall>i. A i \<in> X \<times> Y"
[PROOF STATE]
proof (state)
this:
chain A
\<forall>i. A i \<in> X \<times> Y

goal (1 subgoal):
 1. \<And>Ya. \<lbrakk>chain Ya; \<forall>i. Ya i \<in> X \<times> Y\<rbrakk> \<Longrightarrow> (\<Squnion>i. Ya i) \<in> X \<times> Y
[PROOF STEP]
from Ai
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. A i \<in> X \<times> Y
[PROOF STEP]
have "\<forall>i. fst (A i) \<in> X" and "\<forall>i. snd (A i) \<in> Y"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. A i \<in> X \<times> Y

goal (1 subgoal):
 1. \<forall>i. fst (A i) \<in> X &&& \<forall>i. snd (A i) \<in> Y
[PROOF STEP]
by (auto simp: mem_Times_iff)
[PROOF STATE]
proof (state)
this:
\<forall>i. fst (A i) \<in> X
\<forall>i. snd (A i) \<in> Y

goal (1 subgoal):
 1. \<And>Ya. \<lbrakk>chain Ya; \<forall>i. Ya i \<in> X \<times> Y\<rbrakk> \<Longrightarrow> (\<Squnion>i. Ya i) \<in> X \<times> Y
[PROOF STEP]
with A X Y
[PROOF STATE]
proof (chain)
picking this:
chain A
adm (\<lambda>x. x \<in> X)
adm (\<lambda>x. x \<in> Y)
\<forall>i. fst (A i) \<in> X
\<forall>i. snd (A i) \<in> Y
[PROOF STEP]
show "Lub A \<in> X \<times> Y"
[PROOF STATE]
proof (prove)
using this:
chain A
adm (\<lambda>x. x \<in> X)
adm (\<lambda>x. x \<in> Y)
\<forall>i. fst (A i) \<in> X
\<forall>i. snd (A i) \<in> Y

goal (1 subgoal):
 1. Lub A \<in> X \<times> Y
[PROOF STEP]
by (auto intro: admD intro!: adm_subst simp: lub_prod)
[PROOF STATE]
proof (state)
this:
Lub A \<in> X \<times> Y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma adm_exists_unique [intro, simp]:
  assumes Q: "\<And>y. adm (\<lambda>x. Q x y)"
  assumes P: "\<And>x x'. P x \<and> P x' \<longrightarrow> x = x'"
  shows "adm (\<lambda>x. \<exists>y. P y \<and> Q x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adm (\<lambda>x. \<exists>y. P y \<and> Q x y)
[PROOF STEP]
proof(rule admI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; \<forall>i. \<exists>y. P y \<and> Q (Y i) y\<rbrakk> \<Longrightarrow> \<exists>y. P y \<and> Q (\<Squnion>i. Y i) y
[PROOF STEP]
fix Y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; \<forall>i. \<exists>y. P y \<and> Q (Y i) y\<rbrakk> \<Longrightarrow> \<exists>y. P y \<and> Q (\<Squnion>i. Y i) y
[PROOF STEP]
assume Y: "chain Y" and Yi: "\<forall>i. \<exists>y. P y \<and> Q (Y i) y"
[PROOF STATE]
proof (state)
this:
chain Y
\<forall>i. \<exists>y. P y \<and> Q (Y i) y

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; \<forall>i. \<exists>y. P y \<and> Q (Y i) y\<rbrakk> \<Longrightarrow> \<exists>y. P y \<and> Q (\<Squnion>i. Y i) y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
chain Y
\<forall>i. \<exists>y. P y \<and> Q (Y i) y
[PROOF STEP]
obtain y where Py: "P y"
[PROOF STATE]
proof (prove)
using this:
chain Y
\<forall>i. \<exists>y. P y \<and> Q (Y i) y

goal (1 subgoal):
 1. (\<And>y. P y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P y

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; \<forall>i. \<exists>y. P y \<and> Q (Y i) y\<rbrakk> \<Longrightarrow> \<exists>y. P y \<and> Q (\<Squnion>i. Y i) y
[PROOF STEP]
with P Q Y Yi
[PROOF STATE]
proof (chain)
picking this:
P ?x \<and> P ?x' \<longrightarrow> ?x = ?x'
adm (\<lambda>x. Q x ?y)
chain Y
\<forall>i. \<exists>y. P y \<and> Q (Y i) y
P y
[PROOF STEP]
have "Q (Lub Y) y"
[PROOF STATE]
proof (prove)
using this:
P ?x \<and> P ?x' \<longrightarrow> ?x = ?x'
adm (\<lambda>x. Q x ?y)
chain Y
\<forall>i. \<exists>y. P y \<and> Q (Y i) y
P y

goal (1 subgoal):
 1. Q (Lub Y) y
[PROOF STEP]
by - (rule admD, fastforce+)
[PROOF STATE]
proof (state)
this:
Q (Lub Y) y

goal (1 subgoal):
 1. \<And>Y. \<lbrakk>chain Y; \<forall>i. \<exists>y. P y \<and> Q (Y i) y\<rbrakk> \<Longrightarrow> \<exists>y. P y \<and> Q (\<Squnion>i. Y i) y
[PROOF STEP]
with Py
[PROOF STATE]
proof (chain)
picking this:
P y
Q (Lub Y) y
[PROOF STEP]
show "\<exists>y. P y \<and> Q (Lub Y) y"
[PROOF STATE]
proof (prove)
using this:
P y
Q (Lub Y) y

goal (1 subgoal):
 1. \<exists>y. P y \<and> Q (Lub Y) y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>y. P y \<and> Q (Lub Y) y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma below_monicI:
  "(\<And>x y. f x \<sqsubseteq> f y \<Longrightarrow> x \<sqsubseteq> y) \<Longrightarrow> below_monic f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. f x \<sqsubseteq> f y \<Longrightarrow> x \<sqsubseteq> y) \<Longrightarrow> below_monic f
[PROOF STEP]
unfolding below_monic_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. f x \<sqsubseteq> f y \<Longrightarrow> x \<sqsubseteq> y) \<Longrightarrow> \<forall>x y. f x \<sqsubseteq> f y \<longrightarrow> x \<sqsubseteq> y
[PROOF STEP]
by simp


[STATEMENT]
lemma below_monicE:
  "\<lbrakk> below_monic f; f x \<sqsubseteq> f y \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>below_monic f; f x \<sqsubseteq> f y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> y
[PROOF STEP]
unfolding below_monic_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x y. f x \<sqsubseteq> f y \<longrightarrow> x \<sqsubseteq> y; f x \<sqsubseteq> f y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> y
[PROOF STEP]
by simp


[STATEMENT]
lemma below_monic_inj:
  "below_monic (f :: 'a::cpo \<Rightarrow> 'b::cpo) \<Longrightarrow> inj f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. below_monic f \<Longrightarrow> inj f
[PROOF STEP]
by (auto intro!: below_antisym injI elim: below_monicE)


[STATEMENT]
lemma below_monic_indexed:
  assumes "below_monic_cfun f"
  shows "below_monic (\<lambda>y i. f\<cdot>(y i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. below_monic (\<lambda>y i. f\<cdot>(y i))
[PROOF STEP]
by (metis (no_types, lifting) assms below_fun_def below_monicE below_monicI)


[STATEMENT]
lemma below_monic_ID [iff]:
  "below_monic_cfun ID"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. below_monic_cfun ID
[PROOF STEP]
by (rule below_monicI) simp


[STATEMENT]
lemma below_monic_cfcomp [iff]:
  "below_monic_cfun f \<Longrightarrow> below_monic_cfun (cfcomp\<cdot>f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. below_monic_cfun f \<Longrightarrow> below_monic_cfun (cfcomp\<cdot>f)
[PROOF STEP]
by (rule below_monicI) (auto simp: cfun_below_iff elim: below_monicE)


[STATEMENT]
lemma below_monic_K [iff]:
  "below_monic_cfun f \<Longrightarrow> below_monic_cfun (\<Lambda> c _. f\<cdot>c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. below_monic_cfun f \<Longrightarrow> below_monic_cfun (\<Lambda> c uu_. f\<cdot>c)
[PROOF STEP]
by (rule below_monicI) (auto simp: cfun_below_iff elim: below_monicE)


[STATEMENT]
lemma below_monic_fun_K [iff]:
  "below_monic_cfun f \<Longrightarrow> below_monic_cfun (\<Lambda> c. (\<lambda>_. f\<cdot>c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. below_monic_cfun f \<Longrightarrow> below_monic_cfun (\<Lambda> c. (\<lambda>_. f\<cdot>c))
[PROOF STEP]
by (rule below_monicI) (auto simp: fun_below_iff dest: below_monicE)


[STATEMENT]
lemma below_monic_cfcomp2 [iff]:
  "\<lbrakk> below_monic_cfun f; below_monic_cfun g \<rbrakk> \<Longrightarrow> below_monic_cfun (f oo g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>below_monic_cfun f; below_monic_cfun g\<rbrakk> \<Longrightarrow> below_monic_cfun (f oo g)
[PROOF STEP]
by (rule below_monicI) (auto simp: cfun_below_iff elim: below_monicE)


[STATEMENT]
lemma below_monic_pair [iff]:
  "\<lbrakk> below_monic_cfun f; below_monic_cfun g \<rbrakk> \<Longrightarrow> below_monic_cfun (\<Lambda> x. (f\<cdot>x, g\<cdot>x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>below_monic_cfun f; below_monic_cfun g\<rbrakk> \<Longrightarrow> below_monic_cfun (\<Lambda> x. (f\<cdot>x, g\<cdot>x))
[PROOF STEP]
by (rule below_monicI) (auto simp: cfun_below_iff elim: below_monicE)


[STATEMENT]
lemma below_monic_pair_split [iff]:
  "\<lbrakk> below_monic_cfun f; below_monic_cfun g \<rbrakk> \<Longrightarrow> below_monic_cfun (\<Lambda> x. (f\<cdot>(fst x), g\<cdot>(snd x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>below_monic_cfun f; below_monic_cfun g\<rbrakk> \<Longrightarrow> below_monic_cfun (\<Lambda> x. (f\<cdot>(fst x), g\<cdot>(snd x)))
[PROOF STEP]
by (rule below_monicI) (auto simp: cfun_below_iff elim: below_monicE)


[STATEMENT]
lemma below_monic_sinl [iff]:
  "below_monic_cfun sinl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. below_monic_cfun sinl
[PROOF STEP]
by (rule below_monicI) (auto simp: cfun_below_iff elim: below_monicE)


[STATEMENT]
lemma below_monic_sinr [iff]:
  "below_monic_cfun sinr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. below_monic_cfun sinr
[PROOF STEP]
by (rule below_monicI) (auto simp: cfun_below_iff elim: below_monicE)


[STATEMENT]
lemma below_monic_chain_inv:
  fixes f :: "'a::cpo \<Rightarrow> 'b::cpo"
  assumes Y: "chain (Y :: nat \<Rightarrow> 'b::cpo)"
  assumes Yi: "\<forall>i. \<exists>y. Y i = f y \<and> P y"
  assumes f: "below_monic f"
  shows "\<exists>Y'. chain Y' \<and> (\<forall>i. Y i = f (Y' i) \<and> P (Y' i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Y'. chain Y' \<and> (\<forall>i. Y i = f (Y' i) \<and> P (Y' i))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>Y'. chain Y' \<and> (\<forall>i. Y i = f (Y' i) \<and> P (Y' i))
[PROOF STEP]
let ?Y' = "\<lambda>i. SOME y. Y i = f y \<and> P y"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>Y'. chain Y' \<and> (\<forall>i. Y i = f (Y' i) \<and> P (Y' i))
[PROOF STEP]
have "chain ?Y'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. chain (\<lambda>i. SOME y. Y i = f y \<and> P y)
[PROOF STEP]
proof(rule chainI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. (SOME y. Y i = f y \<and> P y) \<sqsubseteq> (SOME y. Y (Suc i) = f y \<and> P y)
[PROOF STEP]
fix i :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. (SOME y. Y i = f y \<and> P y) \<sqsubseteq> (SOME y. Y (Suc i) = f y \<and> P y)
[PROOF STEP]
show "(SOME x. Y i = f x \<and> P x) \<sqsubseteq> (SOME y. Y (Suc i) = f y \<and> P y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME x. Y i = f x \<and> P x) \<sqsubseteq> (SOME y. Y (Suc i) = f y \<and> P y)
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME x. Y i = f x \<and> P x) \<sqsubseteq> (SOME y. Y (Suc i) = f y \<and> P y)
[PROOF STEP]
using spec[OF Yi, where x=i] spec[OF Yi, where x="Suc i"]
[PROOF STATE]
proof (prove)
using this:
\<exists>y. Y i = f y \<and> P y
\<exists>y. Y (Suc i) = f y \<and> P y

goal (1 subgoal):
 1. (SOME x. Y i = f x \<and> P x) \<sqsubseteq> (SOME y. Y (Suc i) = f y \<and> P y)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y ya. \<lbrakk>Y i = f y; P y; Y (Suc i) = f ya; P ya\<rbrakk> \<Longrightarrow> (SOME x. f y = f x \<and> P x) \<sqsubseteq> (SOME y. f ya = f y \<and> P y)
[PROOF STEP]
apply (rule someI2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y ya. \<lbrakk>Y i = f y; P y; Y (Suc i) = f ya; P ya\<rbrakk> \<Longrightarrow> f ya = f (?a6 y ya) \<and> P (?a6 y ya)
 2. \<And>y ya yb. \<lbrakk>Y i = f y; P y; Y (Suc i) = f ya; P ya; f ya = f yb \<and> P yb\<rbrakk> \<Longrightarrow> (SOME x. f y = f x \<and> P x) \<sqsubseteq> yb
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y ya yb. \<lbrakk>Y i = f y; P y; Y (Suc i) = f ya; P ya; f ya = f yb \<and> P yb\<rbrakk> \<Longrightarrow> (SOME x. f y = f x \<and> P x) \<sqsubseteq> yb
[PROOF STEP]
apply (rule someI2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y ya yb. \<lbrakk>Y i = f y; P y; Y (Suc i) = f ya; P ya; f ya = f yb \<and> P yb\<rbrakk> \<Longrightarrow> f y = f (?a13 y ya yb) \<and> P (?a13 y ya yb)
 2. \<And>y ya yb x. \<lbrakk>Y i = f y; P y; Y (Suc i) = f ya; P ya; f ya = f yb \<and> P yb; f y = f x \<and> P x\<rbrakk> \<Longrightarrow> x \<sqsubseteq> yb
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y ya yb x. \<lbrakk>Y i = f y; P y; Y (Suc i) = f ya; P ya; f ya = f yb \<and> P yb; f y = f x \<and> P x\<rbrakk> \<Longrightarrow> x \<sqsubseteq> yb
[PROOF STEP]
apply (rule below_monicE[OF f])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y ya yb x. \<lbrakk>Y i = f y; P y; Y (Suc i) = f ya; P ya; f ya = f yb \<and> P yb; f y = f x \<and> P x\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f yb
[PROOF STEP]
using chain_mono[OF Y, where i=i and j="Suc i"]
[PROOF STATE]
proof (prove)
using this:
i \<le> Suc i \<Longrightarrow> Y i \<sqsubseteq> Y (Suc i)

goal (1 subgoal):
 1. \<And>y ya yb x. \<lbrakk>Y i = f y; P y; Y (Suc i) = f ya; P ya; f ya = f yb \<and> P yb; f y = f x \<and> P x\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f yb
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(SOME x. Y i = f x \<and> P x) \<sqsubseteq> (SOME y. Y (Suc i) = f y \<and> P y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
chain (\<lambda>i. SOME y. Y i = f y \<and> P y)

goal (1 subgoal):
 1. \<exists>Y'. chain Y' \<and> (\<forall>i. Y i = f (Y' i) \<and> P (Y' i))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
chain (\<lambda>i. SOME y. Y i = f y \<and> P y)

goal (1 subgoal):
 1. \<exists>Y'. chain Y' \<and> (\<forall>i. Y i = f (Y' i) \<and> P (Y' i))
[PROOF STEP]
from Yi
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. \<exists>y. Y i = f y \<and> P y
[PROOF STEP]
have "Y i = f (?Y' i) \<and> P (?Y' i)" for i
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<exists>y. Y i = f y \<and> P y

goal (1 subgoal):
 1. Y i = f (SOME y. Y i = f y \<and> P y) \<and> P (SOME y. Y i = f y \<and> P y)
[PROOF STEP]
by (metis (mono_tags, lifting) someI_ex)
[PROOF STATE]
proof (state)
this:
Y ?i = f (SOME y. Y ?i = f y \<and> P y) \<and> P (SOME y. Y ?i = f y \<and> P y)

goal (1 subgoal):
 1. \<exists>Y'. chain Y' \<and> (\<forall>i. Y i = f (Y' i) \<and> P (Y' i))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
chain (\<lambda>i. SOME y. Y i = f y \<and> P y)
Y ?i = f (SOME y. Y ?i = f y \<and> P y) \<and> P (SOME y. Y ?i = f y \<and> P y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
chain (\<lambda>i. SOME y. Y i = f y \<and> P y)
Y ?i = f (SOME y. Y ?i = f y \<and> P y) \<and> P (SOME y. Y ?i = f y \<and> P y)

goal (1 subgoal):
 1. \<exists>Y'. chain Y' \<and> (\<forall>i. Y i = f (Y' i) \<and> P (Y' i))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>Y'. chain Y' \<and> (\<forall>i. Y i = f (Y' i) \<and> P (Y' i))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma adm_below_monic_exists:
  "\<lbrakk> adm P; below_monic (f::'a::cpo \<Rightarrow> 'b::cpo); cont f \<rbrakk> \<Longrightarrow> adm (\<lambda>x. \<exists>y. x = f y \<and> P y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>adm P; below_monic f; cont f\<rbrakk> \<Longrightarrow> adm (\<lambda>x. \<exists>y. x = f y \<and> P y)
[PROOF STEP]
apply (rule admI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Y. \<lbrakk>adm P; below_monic f; cont f; chain Y; \<forall>i. \<exists>y. Y i = f y \<and> P y\<rbrakk> \<Longrightarrow> \<exists>y. (\<Squnion>i. Y i) = f y \<and> P y
[PROOF STEP]
apply (drule below_monic_chain_inv)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Y. \<lbrakk>adm P; below_monic f; cont f; \<forall>i. \<exists>y. Y i = f y \<and> P y\<rbrakk> \<Longrightarrow> \<forall>i. \<exists>y. Y i = ?f2 Y y \<and> ?P2 Y y
 2. \<And>Y. \<lbrakk>adm P; below_monic f; cont f; \<forall>i. \<exists>y. Y i = f y \<and> P y\<rbrakk> \<Longrightarrow> below_monic (?f2 Y)
 3. \<And>Y. \<lbrakk>adm P; below_monic f; cont f; \<forall>i. \<exists>y. Y i = f y \<and> P y; \<exists>Y'. chain Y' \<and> (\<forall>i. Y i = ?f2 Y (Y' i) \<and> ?P2 Y (Y' i))\<rbrakk> \<Longrightarrow> \<exists>y. (\<Squnion>i. Y i) = f y \<and> P y
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Y. \<lbrakk>adm P; below_monic f; cont f; \<forall>i. \<exists>y. Y i = f y \<and> P y; \<exists>Y'. chain Y' \<and> (\<forall>i. Y i = f (Y' i) \<and> P (Y' i))\<rbrakk> \<Longrightarrow> \<exists>y. (\<Squnion>i. Y i) = f y \<and> P y
[PROOF STEP]
apply (metis (full_types) admD cont2contlubE lub_eq)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ctstate_assume_state: "p_tag_ctstate p = s \<Longrightarrow>
    matches (common_matcher, \<alpha>) (ctstate_assume_state s m) a p \<longleftrightarrow> matches (common_matcher, \<alpha>) m a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_tag_ctstate p = s \<Longrightarrow> matches (common_matcher, \<alpha>) (ctstate_assume_state s m) a p = matches (common_matcher, \<alpha>) m a p
[PROOF STEP]
apply(rule matches_iff_apply_f)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p_tag_ctstate p = s \<Longrightarrow> ternary_ternary_eval (map_match_tac common_matcher p (ctstate_assume_state s m)) = ternary_ternary_eval (map_match_tac common_matcher p m)
[PROOF STEP]
by(induction m rule: ctstate_assume_state.induct) (simp_all)


[STATEMENT]
lemma ctstate_assume_new_simple_ruleset: "simple_ruleset rs \<Longrightarrow> simple_ruleset (ctstate_assume_new rs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simple_ruleset rs \<Longrightarrow> simple_ruleset (ctstate_assume_new rs)
[PROOF STEP]
by (simp add: ctstate_assume_new_def optimize_matches_simple_ruleset)