(* This file requires: - An Isabelle Snapshot from no earlier than October 5, 2007 *) (* This contains occurence typing with: - variables as tests - eta-expansion *) theory TypedSchemePreOr imports Nominal begin ML {*ResAtp.set_prover "vampire"*} (* ML {* ThmDeps.enable() *} *) (* datatype definitions *) atom_decl name datatype ty = Top | Int | TT | FF | Arr "ty" "ty" "latent_eff" ("_ \ _ : _" [100,100] 100) | Union "ty list" and latent_eff = NE | Latent ty constdefs "BoolTy == Union [TT , FF]" primrec (unchecked perm_ty) "pi\(ty.Top) = ty.Top" "pi\(ty.Int) = ty.Int" "pi\(TT) = TT" "pi\(FF) = FF" "pi\(\ \ \ : L) = ((pi\\) \ (pi\\) : (pi\L))" "pi\(Union l) = Union (pi\l)" "pi\latent_eff.NE = latent_eff.NE" "pi\(Latent S) = Latent (pi\S)" declare perm_ty.simps[eqvt] lemma perm_ty_latent_eff_ty_list[simp]: fixes pi ::"name prm" and \ ::"ty" and Ts ::"ty list" and l ::"latent_eff" shows "pi\\ = \" and "pi\l = l" and "pi\Ts = Ts" by (induct \ and l rule: ty_latent_eff.inducts) auto instance ty :: pt_name by intro_classes auto instance ty :: fs_name by intro_classes (simp add: supp_def) instance latent_eff :: pt_name by intro_classes auto instance latent_eff :: fs_name by intro_classes (simp add: supp_def) fun size_ty :: "ty \ nat" and size_le :: "latent_eff \ nat" where "size_ty (ty.Int) = 1" | "size_ty (TT) = 1" | "size_ty (FF) = 1" | "size_ty (Top) = 1" | "size_ty (Union []) = 1" | "size_ty (Union (t#ts)) = size_ty t + size_ty (Union ts)" | "size_ty (T1 \ T2 : L) = (size_ty T1) + (size_ty T2) + (size_le L)" | "size_le (Latent L) = size_ty L" | "size_le (latent_eff.NE) = 1" lemma size_ty_pos: "size_ty T > 0" proof (induct T ) fix l show "0 < size_ty (Union l)" by (induct l) auto qed (auto) nominal_datatype eff = NE | TE "ty" "name" | VE "name" | TT | FF nominal_datatype builtin = Add1 | NumberP | BooleanP | Nott | ProcP nominal_datatype trm = Var "name" | App "trm" "trm" | Abs "\name\trm" "ty" | Iff "trm" "trm" "trm" | Num "nat" | Bool "bool" | BI "builtin" abbreviation "lam" :: "name \ ty \ trm \ trm" ("Lam [_:_]._" [100,100,100] 100) where "Lam[x:T].b \ trm.Abs x b T" (* lemmas about names, types, effects *) lemma trm_finite_supp: fixes x::"trm" shows "finite ((supp x)::name set)" using fs_name_class.axioms[of x] by simp lemma pt_trm_inst: "pt TYPE(trm) TYPE(name)" using pt_name_inst by auto lemma fs_trm_inst: "fs TYPE(trm) TYPE(name)" using fs_name_inst by auto lemma perm_ty_latent[simp]: fixes T::"ty" and le::"latent_eff" and pi::"name prm" shows "pi\le = le \ pi\T = T" by simp lemma perm_ty: fixes T::"ty" and le::"latent_eff" and pi::"name prm" shows "pi\T = T" by simp lemma perm_builtin[simp]: fixes e::"builtin" and pi::"name prm" shows "pi\e = e" by (induct rule: builtin.weak_induct) (simp_all) lemma fresh_ty[simp]: fixes x::"name" and T::"ty" shows "x\T" by (simp add: fresh_def supp_def) lemma fresh_latent_eff[simp]: fixes x::"name" and T::"latent_eff" shows "x\T" by (simp add: fresh_def supp_def) lemma fresh_builtin[simp]: fixes x::"name" and b::"builtin" shows "x\b" by (simp add: fresh_def supp_def) lemma supp_latent_eff_ty: fixes T::ty and le::latent_eff shows " supp le = ({}::name set) \ supp T = ({}::name set)" by (simp add: supp_def) text {* size of a term *} instance trm :: size .. nominal_primrec "size (Var x) = 1" "size (BI b) = 1" "size (Bool b) = 1" "size (Num b) = 1" "size (App t1 t2) = (max (size t1) (size t2)) + 1" "size (Iff t1 t2 t3) = (max (size t1) (max (size t2) (size t3))) + 1" "size (Lam [a:T].t) = (size t) + 1" by (auto simp add: fresh_nat, finite_guess+, fresh_guess+) abbreviation "smaller_than_abb" :: "trm \ trm \ bool" ("_ \ _" [80,80] 80) where "a \ b == size a < size b" text {* complete induction on terms *} lemma trm_comp_induct[consumes 0, case_names Var App Lam BI Num Bool Iff]: fixes P::"'a::fs_name \ trm \ bool" and t::"trm" and x::"'a::fs_name" assumes a1:"!! n z. (!! x t. (t \ Var n) \ P x t) \ P z (Var n)" and a2:"!! t1 t2 z. (!! x t. (t \ App t1 t2) \ P x t) \ (!! x. P x t1) \ (!! x . P x t2) \ P z (App t1 t2)" and a3:"!! a b z T. \a \ z ; (!! x t. (t \ Lam[a:T].b) \ P x t)\ \ (!! x . P x b) \ P z (Lam[a:T].b)" and a4:"!! b z. (!! x t. (t \ BI b) \ P x t) \ P z (BI b)" and a5:"!! n z. (!! x t. (t \ Num n) \ P x t) \ P z (Num n)" and a6:"!! b z. (!! x t. (t \ Bool b) \ P x t) \ P z (Bool b)" and a7:"!! t1 t2 t3 z. (!! x t. t \ (Iff t1 t2 t3) \ P x t) \ (!! x. P x t1) \ (!! x . P x t2) \ (!! x. P x t3) \ P z (Iff t1 t2 t3)" shows "P x t" proof (induct t arbitrary: x taking:"(% t :: trm. size t)" rule: measure_induct_rule) case (less s x) thus ?case -- "This would go through automatically, but I'm skeptical of that sort of thing" proof (nominal_induct s avoiding: x rule: trm.induct) case (Var v) thus ?case using a1 by auto next case (App t1 t2) thus ?case using a2 by auto next case (Abs a b T) thus ?case using a3 by auto next case (Iff t1 t2 t3) thus ?case using a7 by auto next case (BI b) thus ?case using a4 by auto next case (Num n) thus ?case using a5 by auto next case (Bool b) thus ?case using a6 by auto qed qed text {* closed terms *} constdefs fv :: "trm \ name set" fv_def[simp]:"fv e == ((supp e):: name set)" constdefs closed :: "trm \ bool" closed_def: "closed e == (fv e = {})" lemma closed_lam: --"A statement about the free variables of lam bodies" assumes "closed (Lam[x:T].b)" (is "closed ?e") shows "fv b <= {x}" proof - have "(supp ([x].b)::name set) = supp b - {x}" using fs_name_class.axioms abs_fun_supp[of b x] pt_trm_inst at_name_inst by auto hence "supp ?e = ((((supp b):: name set) - {x}) :: name set)" using supp_latent_eff_ty trm.supp by simp thus ?thesis using prems closed_def by auto qed lemma closed_eqvt[eqvt]: fixes pi::"name prm" shows "closed e \ closed (pi\e)" proof - have A:"(pi\fv e) = fv (pi\e)" using pt_perm_supp[of pi e] at_name_inst pt_trm_inst by auto assume "closed e" hence "fv e = {}" using closed_def by simp hence "(pi\fv e) = {}" using empty_eqvt[of pi] by auto hence "closed (pi\e)" using A closed_def by auto thus ?thesis . qed text {* capture-avoiding substitution *} consts subst :: "trm \ name \ trm \ trm" ("_[_::=_]" [100,100,100] 100) nominal_primrec "(Var x)[y::=t'] = (if x=y then t' else (Var x))" "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])" "x\(y,t',T) \ (Lam[x:T].t)[y::=t'] = Lam[x:T].(t[y::=t'])" "(Iff tst thn els)[y::=t'] = (Iff (tst[y::=t']) (thn[y::=t']) (els[y::=t']))" "(BI c)[y::=t'] = (BI c)" "(Num c)[y::=t'] = (Num c)" "(Bool c)[y::=t'] = (Bool c)" by (finite_guess+, auto simp add: abs_fresh, fresh_guess+) lemma subst_eqvt[simp, eqvt]: fixes pi:: "name prm" and t1:: "trm" and t2:: "trm" and a :: "name" shows "pi\(t1[b::=t2]) = (pi\t1)[(pi\b)::=(pi\t2)]" by (nominal_induct t1 avoiding: b t2 rule: trm.induct) (auto simp add: perm_bij fresh_prod fresh_atm fresh_bij) lemma subst_rename[rule_format]: shows "c\t1 \ (t1[a::=t2] = ([(c,a)]\t1)[c::=t2])" by (nominal_induct t1 avoiding: a c t2 rule: trm.induct) (auto simp add: calc_atm fresh_atm abs_fresh fresh_nat trm.inject perm_nat_def perm_bool) lemma forget: assumes a: "a\t1" shows "t1[a::=t2] = t1" using a by (nominal_induct t1 avoiding: a t2 rule: trm.induct) (auto simp add: abs_fresh fresh_atm) lemma subst_removes_var: assumes "e1[x::=e0] = e2" and "x \ e0" shows "x \ e2" using prems proof (nominal_induct e1 avoiding: e0 x e2 rule: trm.induct) case (Var v e0' x' e2') thus ?case using at_fresh[of x' v] at_name_inst by (cases "x' = v") auto next case App thus ?case by auto next case Iff thus ?case by auto next case BI thus ?case by auto next case Num thus ?case by (auto simp add: fresh_nat) next case (Bool b) thus ?case by (auto simp add: fresh_def supp_bool trm.supp) next case (Abs v e1' T e0' x' e2') let ?body = "(e1'[x'::=e0'])" have a:"finite ((supp ?body) :: name set)" using fs_name1 by auto have f:"x' \ (e1'[x'::=e0'])" using Abs by auto hence "v \ (x',e0',T)" using Abs by auto hence "(Abs v e1' T)[x'::=e0'] = Abs v (e1'[x'::=e0']) T" by auto hence "\ = e2'" using Abs by auto have "v \ x'" using `v \ x'` at_fresh[of v x'] at_name_inst by auto hence "x' \ v" using at_fresh[of x' v] at_name_inst by auto have "x' \ T" using fresh_def supp_latent_eff_ty by auto have "x' \ [v].(e1'[x'::=e0'])" using `v ~= x'` fresh_abs_funI1[of ?body x' v ] pt_trm_inst at_name_inst a f by auto hence "x' \ Abs v (e1'[x'::=e0']) T" using f trm.fresh Abs by auto thus ?case using Abs by auto qed lemma fv_lam: fixes name shows "fv (Lam[name:T].body) = fv body - {name}" proof - have sT:"supp T = ({} :: name set)" using supp_latent_eff_ty by auto have "fv (Lam[name:T].body) = (supp ([name].body):: name set) \ supp T" using trm.supp by auto also have "\ = (supp ([name].body):: name set)" using sT by auto also have "\ = supp body - ({name} :: name set)" using abs_fun_supp[of body name] at_name_inst pt_trm_inst fs_name1[of body] by simp also have "\ = fv body - {name}" by simp finally show "fv (Lam[name:T].body) = fv body - {name}" by simp qed lemma subst_closed: assumes "e1[x::=e0] = e2" and "closed e0" shows "fv e2 <= fv e1" using prems proof (nominal_induct e1 avoiding: e0 x e2 rule: trm.induct) case (Var v e0' x' e2') thus ?case using at_fresh[of x' v] at_name_inst closed_def by (cases "x' = v") auto next case (App rator rand e0' x' e2') let ?subrator = "rator[x'::=e0']" let ?subrand = "rand[x'::=e0']" have a:"e2' = App ?subrator ?subrand" using App by simp have s1:"fv ?subrator <= fv rator" using App by simp have s2:"fv ?subrand <= fv rand" using App by simp have b:"fv e2' = fv ?subrator \ fv ?subrand" using trm.supp App a by simp have d:"fv (App rator rand) = fv rator \ fv rand" using trm.supp by simp show ?case using d s1 s2 b by auto next case BI thus ?case by auto next case Num thus ?case by (auto simp add: fresh_nat) next case (Bool b) thus ?case by (auto simp add: fresh_def supp_bool trm.supp) next case (Iff tst thn els e0' x' e2') let ?subtst = "tst[x'::=e0']" let ?subthn = "thn[x'::=e0']" let ?subels = "els[x'::=e0']" have a:"e2' = Iff ?subtst ?subthn ?subels" using Iff by simp have s1:"fv ?subtst <= fv tst" using Iff by simp have s2:"fv ?subthn <= fv thn" using Iff by simp have s3:"fv ?subels <= fv els" using Iff by simp have b:"fv e2' = fv ?subtst \ fv ?subthn \ fv ?subels" using trm.supp Iff a by auto have d:"fv (Iff tst thn els) = fv tst \ fv thn \ fv els" using trm.supp by auto show ?case using d s1 s2 s3 b by auto next case (Abs name body T e0' x' e2') have aa:"fv (body[x'::=e0']) \ fv body" using Abs by auto have a:"fv (Lam[name:T].body) = fv body - {name}" using fv_lam by simp have b:"fv (Lam[name:T].(body[x'::=e0'])) = fv (body[x'::=e0']) - {name}" using fv_lam by simp have "name \ (e0',T,x')" using Abs by auto hence c:"(Lam[name:T].(body[x'::=e0'])) = (Lam[name:T].(body))[x'::=e0']" by simp hence d:"fv e2' = fv (body[x'::=e0']) - {name}" using b Abs by auto thus ?case using a aa by auto qed lemma subst_only_var_closed: assumes "closed e0" and "fv e1 <= {x}" shows "closed (e1[x::=e0])" proof - let ?e2 = "(e1[x::=e0])" have a:"fv ?e2 <= {x}" using prems subst_closed[of e1 x e0 ?e2] by auto have "x \ e0" using prems fresh_def[of x e0] closed_def[of e0] by auto hence "x \ ?e2" using subst_removes_var[of e1 x e0 ?e2] by auto hence b:"x \ fv ?e2" using fresh_def[of x ?e2] closed_def[of ?e2] by auto from a b have "fv ?e2 = {}" by auto thus ?thesis using closed_def by simp qed lemma beta_closed_closed: assumes "closed (Lam[x:T].b)" and "closed v" shows "closed (b[x::=v])" using prems closed_lam subst_only_var_closed by auto text {* values *} inductive values :: "trm \ bool" ("_ : values" [80]) where abs_value[simp]: "Lam[x:t].b : values" | bi_value[simp]: "BI c : values" | num_value[simp]: "Num n : values" | bool_value[simp]: "Bool b : values" equivariance values abbreviation "in_values" :: "trm \ bool" ("_ \ values" [100] 100) where "e \ values \ (e : values)" abbreviation "not_in_values" :: "trm \ bool" ("_ \ values" [100] 100) where "e \ values \ (~ e : values)" lemma not_false_eqvt: fixes pi :: "name prm" and t :: "trm" assumes a:"t ~= trm.Bool False" and b:"t : values" shows "(pi\t) ~= trm.Bool False" using b a by induct (auto simp add: perm_bool) inductive_cases iff_value:"Iff a b c : values" inductive_cases app_value:"App a b : values" inductive_cases var_value:"Var a : values" nominal_inductive values by (simp add: abs_fresh) text {* Typing Constants *} consts \\<^isub>\ :: "builtin \ ty" nominal_primrec "\\<^isub>\ NumberP = (Top \ BoolTy : Latent ty.Int)" "\\<^isub>\ BooleanP = (Top \ BoolTy : Latent BoolTy)" "\\<^isub>\ ProcP = (Top \ BoolTy : Latent (Union [] \ Top : latent_eff.NE))" "\\<^isub>\ Add1 = (ty.Int \ ty.Int : latent_eff.NE)" "\\<^isub>\ Nott = (Top \ BoolTy : latent_eff.NE)" by simp_all lemma delta_t_eqvt[eqvt]: fixes pi :: "name prm" shows "pi \ \\<^isub>\ b = \\<^isub>\ (pi \ b)" by (nominal_induct b rule: builtin.induct) auto (* Delta Function *) consts \ :: "builtin \ trm \ trm option" add1_fun :: "trm \ trm option" nott_fun :: "trm \ trm option" numberp_fun :: "trm \ bool" booleanp_fun :: "trm \ bool" procp_fun :: "trm \ bool" procp_bi_fun :: "builtin \ bool" nominal_primrec "add1_fun (Num n) = Some (Num (n+1))" "add1_fun (Lam[x:ty].b) = None" "add1_fun (Iff a b c) = None" "add1_fun (App a b) = None" "add1_fun (Bool a) = None" "add1_fun (BI a) = None" "add1_fun (Var a) = None" by (auto, finite_guess+, fresh_guess+) nominal_primrec "nott_fun (Num n) = (Some (Bool False))" "nott_fun (Lam[x:ty].b) = (Some (Bool False))" "nott_fun (Iff a b c) = (Some (Bool False))" "nott_fun (App a b) = (Some (Bool False))" "nott_fun (Bool b) = Some (Bool (~b))" "nott_fun (BI a) = (Some (Bool False))" "nott_fun (Var a) = (Some (Bool False))" by (auto, finite_guess+, fresh_guess+) nominal_primrec "booleanp_fun (Bool b) = True" "booleanp_fun (Num n) = False" "booleanp_fun (Abs a b c) = False" "booleanp_fun (App a b) = False" "booleanp_fun (BI c) = False" "booleanp_fun (Var v) = False" "booleanp_fun (Iff a b c) = False" by (auto, finite_guess+, fresh_guess+) nominal_primrec "procp_fun (Bool b) = False" "procp_fun (Num n) = False" "procp_fun (Abs a b c) = True" "procp_fun (App a b) = False" "procp_fun (BI c) = True" "procp_fun (Var v) = False" "procp_fun (Iff a b c) = False" by (auto, finite_guess+, fresh_guess+) nominal_primrec "numberp_fun (Bool b) = False" "numberp_fun (Num n) = True" "numberp_fun (Abs a b c) = False" "numberp_fun (App a b) = False" "numberp_fun (BI c) = False" "numberp_fun (Var v) = False" "numberp_fun (Iff a b c) = False" by (auto, finite_guess+, fresh_guess+) nominal_primrec "\ Add1 t = add1_fun t" "\ Nott t = nott_fun t" "\ BooleanP t = Some (Bool (booleanp_fun t))" "\ NumberP t = Some (Bool (numberp_fun t))" "\ ProcP t = Some (Bool (procp_fun t))" by simp_all lemma delta_eqvt: fixes pi :: "name prm" and b :: builtin and t :: "trm" shows "\ (pi\b) (pi\t) = \ b t" proof - have A:"(pi\b) = b" by (nominal_induct b rule: builtin.induct) auto have B:"\ b (pi\t) = \ b t" proof (nominal_induct rule: builtin.induct) case Add1 thus ?case by (nominal_induct t rule: trm.induct) (auto simp add: perm_nat_def) next case Nott thus ?case by (nominal_induct t rule: trm.induct) (auto simp add: perm_bool) next case BooleanP thus ?case by (nominal_induct t rule: trm.induct) (auto simp add: perm_bool) next case NumberP thus ?case by (nominal_induct t rule: trm.induct) (auto simp add: perm_bool) next case ProcP thus ?case by (nominal_induct t rule: trm.induct) (auto simp add: perm_bool) qed from A B show ?thesis by auto qed lemma delta_eqvt2[eqvt]: fixes pi :: "name prm" and b :: builtin and t :: "trm" shows "(pi\(\ b t)) = \ (pi\b) (pi\t)" proof - have A:"(pi\b) = b" by (nominal_induct b rule: builtin.induct) auto have B:"\ b (pi\t) = (pi\(\ b t))" proof (nominal_induct rule: builtin.induct) case Add1 thus ?case by (nominal_induct t rule: trm.induct) (auto simp add: perm_nat_def) next case Nott thus ?case by (nominal_induct t rule: trm.induct) (auto simp add: perm_bool) next case BooleanP thus ?case by (nominal_induct t rule: trm.induct) (auto simp add: perm_bool) next case NumberP thus ?case by (nominal_induct t rule: trm.induct) (auto simp add: perm_bool) next case ProcP thus ?case by (nominal_induct t rule: trm.induct) (auto simp add: perm_bool) qed from A B show ?thesis by auto qed lemma delta_closed: fixes b :: builtin and t::trm assumes "\ b t = Some v" shows "closed v" using prems proof (nominal_induct b rule: builtin.induct) case Add1 thus ?case by (nominal_induct t rule: trm.induct) (auto simp add: supp_nat closed_def trm.supp) next case Nott thus ?case by (nominal_induct t rule: trm.induct) (auto simp add: supp_def perm_bool closed_def trm.supp) next case BooleanP thus ?case by (nominal_induct t rule: trm.induct) (auto simp add: supp_def perm_bool closed_def trm.supp) next case NumberP thus ?case by (nominal_induct t rule: trm.induct) (auto simp add: supp_def perm_bool closed_def trm.supp) next case ProcP thus ?case by (nominal_induct t rule: trm.induct) (auto simp add: supp_def perm_bool closed_def trm.supp) qed lemma delta_value: fixes b :: builtin and t::trm assumes "\ b t = Some v" shows "v : values" using prems proof (nominal_induct b rule: builtin.induct) case Add1 thus ?case by (nominal_induct t rule: trm.induct) auto next case Nott thus ?case by (nominal_induct t rule: trm.induct) auto next case BooleanP thus ?case by (nominal_induct t rule: trm.induct) auto next case NumberP thus ?case by (nominal_induct t rule: trm.induct) auto next case ProcP thus ?case by (nominal_induct t rule: trm.induct) auto qed text {* Evaluation contexts *} inductive_set ctxt :: "(trm \ trm) set" where C_Hole[simp, intro]: "(%t. t) \ ctxt" | C_App1[simp, intro]: "E : ctxt \ (%t . (App (E t) u)) : ctxt" | C_App2[simp, intro]: "E : ctxt \ v : values \ (%t . (App v (E t))) : ctxt" | C_Iff[simp, intro]: "E : ctxt \ (%t . (Iff (E t) thn els)) : ctxt" lemma ctxt_compose: assumes a:"E1 : ctxt" and b:"E2 : ctxt" shows "(%t. E1 (E2 t)) : ctxt" using a b by (induct E1) auto constdefs closed_ctxt :: "(trm \ trm) \ bool" closed_ctxt_def[simp]:"closed_ctxt C == (C : ctxt \ closed (C (Num 3)))" --"3 is a trivially closed term" lemma ctxt_closed: assumes "closed_ctxt C" shows "closed (C e) = closed e" using prems proof - have "C : ctxt" using prems by simp thus ?thesis using prems by (induct) (auto simp add: closed_def trm.supp) qed lemma closed_in_ctxt_closed_ctxt: assumes "closed e" and a:"C : ctxt" and "e = C L" shows "closed L \ closed_ctxt C" using a prems proof (induct C arbitrary: L e rule: ctxt.induct) case C_Hole thus ?case by (auto simp add: closed_def trm.supp supp_nat) next case (C_App1 E arg L' e') have IH:"!!e L. \closed e; E \ ctxt; e = E L\ \ closed L \ closed_ctxt E" using prems by blast have cl:"closed (App (E L') arg)" using `e' = (App (E L') arg)` `closed e'` by simp from cl have "closed arg"by (auto simp add: closed_def trm.supp) from cl have "closed (E L')" by (auto simp add: closed_def trm.supp) thus ?case using IH[of "(E L')" L'] `E : ctxt` `closed arg` by (auto simp add: trm.supp closed_def) next case (C_App2 E rator L' e') have IH:"!!e L. \closed e; E \ ctxt; e = E L\ \ closed L \ closed_ctxt E" using prems by blast have cl:"closed (App rator (E L'))" using prems by blast from cl have "closed rator" by (auto simp add: closed_def trm.supp) from cl have "closed (E L')" by (auto simp add: closed_def trm.supp) thus ?case using IH[of "(E L')" L'] `E : ctxt` `closed rator` by (auto simp add: trm.supp closed_def) next case (C_Iff E thn els L' e') let ?trm = "Iff (E L') thn els" have IH:"!!e L. \closed e; E \ ctxt; e = E L\ \ closed L \ closed_ctxt E" using prems by blast have cl:"closed ?trm" using prems by blast from cl have "closed thn" and "closed els" by (auto simp add: closed_def trm.supp) from cl have "closed (E L')" by (auto simp add: closed_def trm.supp) thus ?case using IH[of "(E L')" L'] `E : ctxt` `closed thn` `closed els` by (auto simp add: trm.supp closed_def) qed lemma closed_in_ctxt: assumes "closed (C L)" and "C : ctxt" shows "closed L" using `C : ctxt` `closed (C L)` by (induct C) (auto simp add: closed_def trm.supp) text{* Reduction *} inductive reduce :: "trm \ trm \ bool" ("_ \ _" [200,200] 200) where e_beta[simp]: "v : values \ x \ v \ (App (Lam[x:t].b) v) \ (b[x::=v])" | e_if_false[simp]: "Iff (Bool False) e1 e2 \ e2" | e_if_true[simp]: "v ~= Bool False \ v : values \ Iff v e1 e2 \ e1" | e_delta[simp]: "\v : values; \ p v = Some e\ \ App (BI p) v \ e" equivariance reduce nominal_inductive reduce by (simp_all add: abs_fresh subst_removes_var) inductive "step" :: "trm\trm\bool" (" _ \ _" [80,80]80) where step_one[intro]:"\E : ctxt; L \ R\ \ E L \ E R" inductive step_multi :: "trm \ trm \ bool" (" _ \\<^sup>* _" [80,80] 80) where sm_refl:"a \\<^sup>* a" | sm_trans:"a \ b \ b \\<^sup>* c \ a \\<^sup>* c" (* doesn't work *) (* equivariance step *) constdefs reduce_forever :: "trm \ bool" "reduce_forever e == \e' . (e \\<^sup>* e') \ (EX e''. e' \ e'')" (* reduction examples *) lemma "(App (Lam [x:t].(Var x)) (Num 4)) \ Num 4" proof - have "Num 4 : values" "x \ Num 4" by (auto simp add: fresh_nat) hence h:"(App (Lam [x:t].(Var x)) (Num 4)) \ ((Var x)[x::=(Num 4)])" by (rule e_beta) have "((Var x)[x::=(Num 4)]) = Num 4" by auto thus ?thesis using h by auto qed (* some lemmas about reduction *) lemma if_val_reduces: assumes a:"tst : values" shows "Iff tst thn els \ thn \ Iff tst thn els \ els" using a proof (nominal_induct tst rule: trm.induct) case (Bool b) thus ?case using e_if_true e_if_false by (cases b) (auto simp add: trm.inject) qed (auto) (* a helper lemma - whee abstraction *) lemma ex_help: assumes a:"e = E t \ E : ctxt \ t \ t'" shows "\E t t' . e = E t \ E \ ctxt \ t \ t'" using a by blast lemma reduce_in_ctxt: fixes e :: trm assumes ct:"C : ctxt" and ih:"(EX E L R. e = E L \ E : ctxt \ L \ R)" shows "(EX E L R. C e = E L \ E : ctxt \ L \ R)" proof - from ih ct obtain Enew tnew t'new where "e = Enew tnew" and 1:"Enew \ ctxt" and g1:"tnew \ t'new" by auto let ?E="(%t . C (Enew t))" have g3:"?E tnew = C e" using `e = Enew tnew` by auto thus "\E t t' . C e = E t \ E \ ctxt \ t \ t'" using ctxt_compose[OF ct 1] g1 g3 ex_help[of "C e" ?E tnew] by auto qed inductive_cases iff_bi_red : "(Iff (Const (BI bi)) thn els) \ e" inductive_cases iff_red : "(Iff tst thn els) \ e" lemma reduce_closed: assumes "closed L" and "L \ R" shows "closed R" using `L \ R` `closed L` proof (induct) case (e_beta v x t b) have a:"closed (Abs x b t)" using e_beta closed_def trm.supp by simp have b:"closed v" using e_beta closed_def trm.supp by simp from a b show ?case using e_beta beta_closed_closed by simp next case e_if_true thus ?case using closed_def trm.supp by auto next case e_if_false thus ?case using closed_def trm.supp by auto next case e_delta thus ?case using delta_closed by auto qed lemma step_closed: assumes A:"closed e" and B:"(e :: trm) \ e'" shows "closed e'" proof - from B obtain E L R where C:"E : ctxt" "e = E L" "L \ R" "e' = E R" by induct auto hence D:"closed L" "closed_ctxt E" using A closed_in_ctxt_closed_ctxt[of e E L] by auto hence "closed R" using C reduce_closed[of L R] by auto hence "closed e'" using C D ctxt_closed[of E R] by auto thus ?thesis . qed lemma multi_step_closed: assumes A:"closed e" and B:"e \\<^sup>* e'" shows "closed e'" using B A step_closed by induct auto text {* "partial order" (not really) between effects *} inductive subeff :: "eff \ eff \ bool"("\ _ F TT \ \ FF FF \ \ TT NE NE F1 eff.NE F1 eff.TT F1 eff.FF \ T \ T = FF" by (induct rule: subeff.induct) auto lemma no_sub_TT: "\\ T \ T = TT" by (induct rule: subeff.induct) auto constdefs simple_eff :: "eff \ bool" simple_eff_def[simp]:"simple_eff e == e = eff.NE \ e = FF \ e = TT" lemma simple_eff_cases[consumes 1, case_names NE FF TT]: fixes F::eff and P :: "eff \ bool" assumes a:"simple_eff F" and a1:"P NE" and a2:"P FF" and a3:"P TT" shows "P F" using prems by (nominal_induct F rule: eff.induct) auto lemma simple_eff_below_ne: assumes "simple_eff F" shows "\ F F1 F2 F1 ty \ bool" ("\ _ <: _" [60,60] 60) where S_Refl[intro]: "\ T <: T" | S_Fun[intro]: "\\ S1 <: T1 ; \ T2 <: S2 ; eff = eff' \ eff' = latent_eff.NE\ \ \ (T1 \ T2 : eff) <: (S1 \ S2 : eff')" | S_Top[intro]: "\ T <: Top" | S_UnionAbove[intro]: "\T : set Ts ; \ S <: T\ \ \ S <: Union Ts" | S_UnionBelow[intro]: "\!! T.( T : set Ts \ \ T <: S)\ \ \ Union Ts <: S" equivariance subtype nominal_inductive subtype done inductive_cases sub_arr_cases: "\ T <: S1 \ S2 : L" lemma subtype_arr_elim: "\\ T <: S ; S = S0 \ S1 : le\ \ (EX T0 T1. T = T0 \ T1 : le \ \ S0 <: T0 \ \ T1 <: S1) \ (EX T0 T1 le'. T = T0 \ T1 : le' \ le = latent_eff.NE \ \ S0 <: T0 \ \ T1 <: S1) \ (EX Ts. T = Union Ts)" proof (induct arbitrary: S0 S1 rule: subtype.induct) qed (auto) lemma S_TopE: assumes a: "\ Top <: T" shows "T = Top \ (EX Ts T'. T = Union Ts \ T' : set Ts \ \ Top <: T')" using a by (cases, auto) lemma S_ArrowE_left: assumes a: "\ S\<^isub>1 \ S\<^isub>2 : L <: T" shows "T = Top \ (\T\<^isub>1 T\<^isub>2. T = T\<^isub>1 \ T\<^isub>2 : L \ \ T\<^isub>1 <: S\<^isub>1 \ \ S\<^isub>2 <: T\<^isub>2) \ (\T\<^isub>1 T\<^isub>2. T = T\<^isub>1 \ T\<^isub>2 : latent_eff.NE \ \ T\<^isub>1 <: S\<^isub>1 \ \ S\<^isub>2 <: T\<^isub>2) \ (EX Ts T1. T = Union Ts \ T1 : set Ts \ \ S\<^isub>1 \ S\<^isub>2 : L <: T1)" using a by (cases, auto simp add: ty.inject) lemma union_size_ty: assumes "T : set Ts" shows "size_ty T < size_ty (Union Ts)" using prems size_ty_pos by (induct Ts) auto fun size_ty3 :: "ty*ty*ty \ nat" where size_ty3_def[simp]:"size_ty3 (a,b,c) = size_ty a + size_ty b + size_ty c" inductive_cases union_sub_cases[consumes 1, case_names 1 2 3 4]:"\ Union Ts <: S" lemma union_sub_elim: assumes A:"\ Union Ts <: T " (is "\ ?S <: T") and B:" T1 : set Ts " shows "\ T1 <: T" using prems proof (induct "X"=="(T1,?S,T)" arbitrary: T1 Ts T taking: "size_ty3" rule: measure_induct_rule) case (less X) show " \ T1 <: T" using `\ Union Ts <: T` less proof (induct rule: union_sub_cases) case 1 thus ?case by auto next case 2 thus ?case by auto next case (3 T' Ts') have X_inst:"X = (T1, ty.Union Ts, T)" . have "size_ty T' < size_ty T" using 3 union_size_ty by auto hence "\ T1 <: T'" using X_inst 3(4)[OF _ ` \ ty.Union Ts <: T'` `T1 : set Ts`] by auto thus ?case using 3 by auto next case 4 thus ?case by auto qed qed lemma S_Trans[intro]: assumes "\S<:Q" and " \Q<:T" shows "\S<:T" using prems proof (induct "X"=="(S,Q,T)" arbitrary: S Q T taking: "size_ty3" rule: measure_induct_rule) case (less X S Q T) show " \ S <: T" using `\ S <: Q` less proof (induct S Q\Q rule: subtype.induct) case S_Refl thus ?case by auto next case (S_Top A) have X_inst:"X = (A,Q,T)" . show ?case proof - { assume "EX Ts T'. T = Union Ts \ T' : set Ts \ \ Q <: T'" then obtain Ts T' where "T = Union Ts "" T' : set Ts "" \ Q <: T'" by auto hence "size_ty T' < size_ty T" using union_size_ty by auto hence "size_ty3 (A,Q,T') < size_ty3 (A,Q,T)" by auto hence "\ A <: T'" using `\ A <: Q` `\ Q <: T'` using less(1)[of "(A,Q,T')" A Q T'] X_inst by auto hence ?thesis using S_Top prems by auto } thus ?thesis using S_TopE S_Top by auto qed next case (S_Fun Q1 S1 S2 Q2 L L') hence rh_drv: " \ Q1 \ Q2 : L' <: T" by simp have X_inst:"X = (S1 \ S2 : L, Q1 \ Q2 : L', T)" using S_Fun by auto note `Q1 \ Q2 : L' = Q` hence Q12_less: "size_ty Q1 < size_ty Q" "size_ty Q2 < size_ty Q" using size_ty_pos by auto have lh_drv_prm1: " \ Q1 <: S1" by fact have lh_drv_prm2: " \ S2 <: Q2" by fact have "T=Top \ (\T1 T2 LL. T=T1\T2 : LL \ \T1<:Q1 \ \Q2<:T2 \ LL = L') \ (\T1 T2. T=T1\T2 : latent_eff.NE \ \T1<:Q1 \ \Q2<:T2) \ (EX Ts T1. T = Union Ts \ T1 : set Ts \ \ Q1 \ Q2 : L' <: T1)" using S_ArrowE_left[OF rh_drv] by auto moreover { assume "\T1 T2 LL. T=T1\T2:LL \ \T1<:Q1 \ \Q2<:T2 \ LL = L'" then obtain T1 T2 LL where T_inst: "T = T1 \ T2 : L'" and rh_drv_prm1: " \ T1 <: Q1" and rh_drv_prm2: " \ Q2 <: T2" and LL': "LL = L'" by auto from X_inst T_inst have X_inst':"X = (S1 \ S2 : L, Q1 \ Q2 : L', T1 \ T2 : L')" by simp hence "size_ty3 (T1, Q1, S1) < size_ty3 X" using size_ty_pos by auto from X_inst' lh_drv_prm1 rh_drv_prm1 have " \ T1 <: S1" using S_Fun(6)[of _ T1 Q1 S1] size_ty_pos by auto moreover from X_inst' lh_drv_prm2 rh_drv_prm2 have " \ S2 <: T2" using S_Fun(6)[of _ S2 Q2 T2] size_ty_pos by auto ultimately have " \ S1 \ S2 : L <: T1 \ T2 : LL" using LL' S_Fun by (simp add: subtype.S_Fun) hence " \ S1 \ S2 : L <: T" using T_inst LL' by simp } moreover { assume "EX Ts T1. T = Union Ts \ T1 : set Ts \ \ Q1 \ Q2 : L' <: T1" then obtain Ts T1 where T_inst: "T = Union Ts" and elem: "T1 : set Ts" and sub:"\ Q1 \ Q2 : L' <: T1" by auto have sub':"\ S1 \ S2 : L <: Q1 \ Q2 : L'" using S_Fun by simp have sz:"size_ty T1 < size_ty T" using T_inst elem union_size_ty by auto from X_inst T_inst have X_inst':"X = (S1 \ S2 : L, Q1 \ Q2 : L', Union Ts)" by simp from sub sub' X_inst' have " \ S1 \ S2 : L <: T1" using S_Fun(6)[OF _ sub' sub] sz T_inst by auto hence " \ S1 \ S2 : L <: T" using T_inst elem S_UnionAbove by auto } moreover { assume "\T1 T2. T=T1\T2:latent_eff.NE \ \T1<:Q1 \ \Q2<:T2 " then obtain T1 T2 LL where T_inst: "T = T1 \ T2 : latent_eff.NE" and rh_drv_prm1: " \ T1 <: Q1" and rh_drv_prm2: " \ Q2 <: T2" by auto from X_inst T_inst have X_inst':"X = (S1 \ S2 : L, Q1 \ Q2 : L', T1 \ T2 : latent_eff.NE)" by simp hence "size_ty3 (T1, Q1, S1) < size_ty3 X" using size_ty_pos by auto from X_inst' lh_drv_prm1 rh_drv_prm1 have " \ T1 <: S1" using S_Fun(6)[of _ T1 Q1 S1] size_ty_pos by auto moreover from X_inst' lh_drv_prm2 rh_drv_prm2 have " \ S2 <: T2" using S_Fun(6)[of _ S2 Q2 T2] size_ty_pos by auto ultimately have " \ S1 \ S2 : L <: T1 \ T2 : latent_eff.NE" using S_Fun by (simp add: subtype.S_Fun) hence " \ S1 \ S2 : L <: T" using T_inst by simp } ultimately show " \ S1 \ S2 : L <: T" by blast next case (S_UnionAbove T1 Ts S) have sub1:"\ S <: T1" . hence sub2:"\ T1 <: T" using S_UnionAbove union_sub_elim[of Ts T T1] by auto have sz:"size_ty T1 < size_ty Q" using S_UnionAbove union_size_ty by auto hence "\ S <: T" using S_UnionAbove(4)[OF _ sub1 sub2] sz S_UnionAbove(7) by auto thus ?case . next case (S_UnionBelow Ts S) have "!! T0. T0 : set Ts \ \ T0 <: T" proof - fix T0 assume "T0 : set Ts" hence sz:"size_ty T0 < size_ty (Union Ts)" using union_size_ty by auto have s1:"\ T0 <: S" using S_UnionBelow `T0 : set Ts` by auto have s2:"\ S <: T" using S_UnionBelow by auto note S_UnionBelow(6) thus "\ T0 <: T" using S_UnionBelow(3)[OF _ s1 s2] sz `S = Q` by auto qed thus ?case .. qed qed text {* type environments *} types varEnv = "(name*ty) list" text {* valid contexts *} inductive valid :: "(name\ty) list \ bool" where v1[intro]: "valid []" | v2[intro]: "\valid \;a\\\\ valid ((a,\)#\)" equivariance valid nominal_inductive valid done lemma fresh_context[rule_format]: fixes \ :: "(name\ty)list" and a :: "name" assumes a: "a\\" shows "\(\\::ty. (a,\)\set \)" using a by (induct \) (auto simp add: fresh_prod fresh_list_cons fresh_atm) lemma valid_elim: fixes \ :: "(name\ty)list" and pi:: "name prm" and a :: "name" and \ :: "ty" shows "valid ((a,\)#\) \ valid \ \ a\\" by (ind_cases "valid ((a,\)#\)") simp lemma valid_unicity[rule_format]: assumes a: "valid \" and b: "(c,\)\set \" and c: "(c,\)\set \" shows "\=\" using a b c by (induct \) (auto dest!: valid_elim fresh_context) declare fresh_list_cons[simp] declare fresh_list_nil[simp] (* environment operations *) consts env_plus :: "eff \ varEnv => varEnv" env_minus :: "eff \ varEnv => varEnv" (* original type is the SECOND argument *) constdefs less_ty :: "((ty * ty) * ty * ty) set" "less_ty == {((a,b),c,d) . (size_ty b) < (size_ty d)}" function (sequential) restrict :: "ty \ ty \ ty" where restrict_union: "restrict r (Union (ls :: ty list)) = (if (\ r <: Union ls) then r else (if (\ Union ls <: r) then (Union ls) else Union (map (restrict r) ls)))" | restrict_top:"restrict r Top = r" | restrict_other:"restrict r T = (if (\ r <: T) then r else T)" by pat_completeness auto termination using union_size_ty by (relation "measure (% (a,b). size_ty b)") auto lemma restrict_eqvt[eqvt]: fixes pi::"name prm" shows "pi\(restrict T1 T2) = restrict (pi\T1) (pi\T2)" by (induct T2) (auto) text {* this is the key lemma in the whole soundness proof *} fun simple_ty :: "ty \ bool" where "simple_ty ty.Int = True" | "simple_ty ty.TT = True" | "simple_ty ty.FF = True" | "simple_ty (A1 \ A2 : L) = True" (* | "simple_ty (Union [ty.TT,ty.FF]) = True" *) | "simple_ty T = False" lemma ty_cases[consumes 0, case_names Top Int TT FF Arr Union]: fixes P :: "ty \ bool" and T :: ty assumes a1:"P Top" and a2:"P ty.Int" and a3:"P ty.TT" and a3':"P ty.FF" and a4:"!! t1 t2 L. P (t1 \ t2 : L)" and a5:"!! Ts . P (Union Ts)" shows "P T" using ty_latent_eff.induct[of P "(%e . True)" "(%e . True)" T] prems by auto inductive_cases tt_below_union: "\ ty.TT <: ty.Union Ts" inductive_cases ff_below_union: "\ ty.FF <: ty.Union Ts" (* I believe this to be true without C, but it's easier to prove this way, and that's all we need *) lemma restrict_soundness: assumes A:"\ T0 <: T" and B:"\ T0 <: S" and C:"simple_ty T0" shows "\ T0 <: restrict S T" using prems proof (induct T arbitrary: S T0 taking:"size_ty" rule: measure_induct_rule) case (less T S T0) thus ?case proof (induct T==T rule: ty_cases) case Top thus ?case by auto next case Int thus ?case by auto next case TT thus ?case by auto next case FF thus ?case by auto next case Arr thus ?case by auto next case (Union Ts) have r:"restrict S T = (if (\ S <:T) then S else (if (\ T <: S) then T else Union (map (restrict S) Ts)))" using prems restrict_union[of S Ts] by auto thus ?case proof - { assume "\ S <: T" hence "restrict S T = S" using r by simp hence ?thesis using prems by auto } moreover { assume "\ T <: S" "~ (\ S <: T)" hence "restrict S T = T" using r by simp hence ?thesis using prems by auto } moreover { assume "~ (\ T <: S)" "~ (\ S <: T)" hence req:"restrict S T = Union (map (restrict S) Ts)" using r by auto have T:"\ T0 <: Union Ts" using prems by simp have "?this \ ?thesis" proof (ind_cases "\ T0 <: Union Ts") assume 0:"Union Ts = T0" thus ?thesis using `simple_ty T0` by (induct T0 rule: simple_ty.induct) auto next fix Ts' assume "T0 = ty.Union Ts'" thus ?thesis using `simple_ty T0` by (induct T0 rule: simple_ty.induct) auto (* hence 1:"T0 = Union [ty.TT,ty.FF]" using `simple_ty T0` by (induct T0 rule: simple_ty.induct) auto have "\ ty.TT <: T0" using 1 by auto hence "\ ty.TT <: Union Ts" "\ ty.TT <: T" "\ ty.TT <: S" using T `\ T0 <: S` `\ T0 <: T` by auto hence "EX \ . \ : set Ts \ \ ty.TT <: \" using tt_below_union by auto then guess \ by auto hence "size_ty \ < size_ty T" using prems union_size_ty by auto note prems(4)[OF `size_ty \ < size_ty T` `\ ty.TT <: \` `\ ty.TT <: S`, simplified] hence A_tt:"\ ty.TT <: restrict S \" . have mem:"restrict S \ : set (map (restrict S) Ts)" using `\ : set Ts` by auto hence "\ ty.TT <: Union (map (restrict S) Ts)" using A_tt S_UnionAbove by auto hence tt_sub:"\ ty.TT <: restrict S T" using req by auto have "\ ty.FF <: T0" using 1 by auto hence "\ ty.FF <: Union Ts" "\ ty.FF <: T" "\ ty.FF <: S" using T `\ T0 <: S` `\ T0 <: T` by auto hence "EX \ . \ : set Ts \ \ ty.FF <: \" using ff_below_union by auto then guess \ by auto hence "size_ty \ < size_ty T" using prems union_size_ty by auto note prems(4)[OF `size_ty \ < size_ty T` `\ ty.FF <: \` `\ ty.FF <: S`, simplified] hence A_ff:"\ ty.FF <: restrict S \" . have mem:"restrict S \ : set (map (restrict S) Ts)" using `\ : set Ts` by auto hence "\ ty.FF <: Union (map (restrict S) Ts)" using A_ff S_UnionAbove by auto hence ff_sub:"\ ty.FF <: restrict S T" using req by auto from ff_sub tt_sub have "\ Union [ty.TT, ty.FF] <: restrict S T" by auto thus ?thesis using 1 by auto *) next fix T' assume "T' : set Ts" "\ T0 <: T'" have 1:"\ T0 <: restrict S T'" using union_size_ty prems by auto have 2:"set (map (restrict S) Ts) = (restrict S) ` set Ts" by auto have 3:"T' : set Ts" using prems by auto have 4:"restrict S T' : set (map (restrict S) Ts)" using 2 3 by auto hence "\ T0 <: Union (map (restrict S) Ts)" using subtype.S_UnionAbove[OF 4 1] by auto thus ?thesis using req by auto qed hence ?thesis using T by simp } ultimately show ?thesis by auto qed qed qed function (sequential) remove :: "ty \ ty \ ty" where remove_union: "remove r (Union (ls :: ty list)) = (if (\ Union ls <: r) then (Union []) else Union (map (remove r) ls))" | remove_other:"remove r T = (if (\ T <: r) then (Union []) else T)" by pat_completeness auto termination using union_size_ty by (relation "measure (% (a,b). size_ty b)") auto lemma remove_eqvt[eqvt]: fixes pi::"name prm" shows "pi\(remove T1 T2) = remove (pi\T1) (pi\T2)" by (induct T2) (auto) lemma remove_soundness: assumes A:"\ T0 <: T" and B:"~ (\ T0 <: S)" and C:"simple_ty T0" shows "\ T0 <: remove S T" using prems proof (induct T arbitrary: S T0 taking:"size_ty" rule: measure_induct_rule) case (less T S T0) thus ?case proof (induct T==T rule: ty_cases) case (Union Ts) have r:"remove S T = (if (\ T <:S) then (Union []) else Union (map (remove S) Ts))" using prems remove_union[of S Ts] by auto thus ?case proof - { assume "\ T <: S" hence "remove S T = (Union [])" using r by simp hence ?thesis using prems by auto } moreover { assume "~ (\ T <: S)" hence req:"remove S T = Union (map (remove S) Ts)" using r by auto have T:"\ T0 <: Union Ts" using prems by simp have "?this \ ?thesis" proof (ind_cases "\ T0 <: Union Ts") assume 0:"Union Ts = T0" thus ?thesis using `simple_ty T0` by auto next fix Ts' assume "T0 = ty.Union Ts'" thus ?thesis using `simple_ty T0` by auto next fix T' assume "T' : set Ts" "\ T0 <: T'" have 1:"\ T0 <: remove S T'" using union_size_ty prems by auto have 2:"set (map (remove S) Ts) = (remove S) ` set Ts" by auto have 3:"T' : set Ts" using prems by auto have 4:"remove S T' : set (map (remove S) Ts)" using 2 3 by auto hence "\ T0 <: Union (map (remove S) Ts)" using subtype.S_UnionAbove[OF 4 1] by auto thus ?thesis using req by auto qed hence ?thesis using T by simp } ultimately show ?thesis by auto qed qed (auto) qed lemma restrict_remove_soundness: assumes A:"\ T0 <: T" and B:"simple_ty T0" shows "(\ T0 <: S \ \ T0 <: restrict S T) \ (~ (\ T0 <: S) \ \ T0 <: remove S T)" using restrict_soundness[OF A _ B] remove_soundness[OF A _ B] by auto fun replace :: "ty \ ty \ ty" where "replace t u = t" fun mapfun :: "(ty \ ty \ ty) \ ty \ name \ (name*ty) \ (name * ty)" where mapfun_def: "mapfun f T x (v,S) = (if (x = v) then (v, f T S) else (v,S))" constdefs envop :: "(ty \ ty \ ty) \ name \ ty \ (name*ty) list \ (name*ty) list" envop_def[simp]:"envop f n t G == map (% (v,ty). (if (n = v) then (v,f t ty) else (v,ty))) G" lemma envop_mapfun: shows "map (mapfun f T x) \ = envop f x T \ " using mapfun_def by auto lemma envop_fresh: fixes v::name assumes a:"v \ \" and c:"valid \" shows "v \ (envop f n t \)" using c a by (induct \ rule: valid.induct) auto lemma envop_valid: assumes "valid \" shows "valid (envop f n t \)" using assms envop_fresh by induct auto lemma envop_forget: assumes "valid \" and "x \ \" shows "envop f x T \ = \" using prems proof (induct rule: valid.induct) case v1 thus ?case by auto next case (v2 \' a S) have "x ~= a" and "x \ \'" using v2 fresh_list_cons fresh_atm[of x a] by auto hence A:"envop f x T ((a,S)#\') = (a,S)# (envop f x T \')" by auto thus ?case using v2 `x \ \'` by auto qed nominal_primrec "env_plus (NE) G = G" "env_plus (TE T x) G = envop restrict x T G" "env_plus (VE x) G = envop remove x (ty.FF) G" "env_plus (TT) G = G" "env_plus (FF) G = G" by auto lemma map_eqvt[eqvt]: fixes pi::"name prm" and l::"('a::pt_name) list" shows "pi\(map f l) = map (pi\f) (pi\l)" by (induct l) perm_simp+ lemma env_plus_eqvt[eqvt]: fixes pi::"name prm" shows "pi\(env_plus X G ) = env_plus (pi\X) (pi\G)" proof (nominal_induct X rule: eff.induct) case (TE T x) thus ?case by (perm_simp add: eqvts split_def) auto next case (VE x) thus ?case by (perm_simp add: eqvts split_def) auto qed(auto) nominal_primrec "env_minus (NE) G = G" "env_minus (TE T x) G = envop remove x T G" "env_minus (VE x) G = envop replace x ty.FF G" "env_minus (TT) G = G" "env_minus (FF) G = G" by auto lemma env_minus_eqvt[eqvt]: fixes pi::"name prm" shows "pi\(env_minus X G) = env_minus (pi\X) (pi\G)" proof (nominal_induct X rule: eff.induct) case (TE T x) thus ?case by (perm_simp add: eqvts perm_fun_def split_def) auto case (VE x) thus ?case by (perm_simp add: eqvts perm_fun_def split_def) qed(auto) abbreviation env_plus_syn :: "varEnv \ eff \ varEnv" ("_ |+ _" [70,70] 70) where "(G |+ eff) == env_plus eff G" abbreviation env_minus_syn :: "varEnv \ eff \ varEnv" ("_ |- _" [70,70] 70) where "(G |- eff) == env_minus eff G" --"Induction principle for type envs" lemma env_induct[case_names Nil Cons]: fixes \ :: varEnv assumes a1:"P []" and a2:"!!G v T. P G \ P ((v,T)#G)" shows "P \" using a1 a2 by (induct \) auto lemma envop_eqvt: fixes pi::"name prm" shows "envop f (pi\n) T (pi\\) = (pi\ (envop f n T \))" proof (induct \ rule: env_induct) case Nil thus ?case by auto next case (Cons G v T0) thus ?case using pt_bij4[of pi n v] pt_name_inst at_name_inst by auto qed lemma env_plus_eqvt: fixes pi::"name prm" shows "(pi\\) |+ pi\eff = pi\(\ |+ eff)" by (nominal_induct eff avoiding: \ rule: eff.induct) (auto simp add: eff.eqvts envop_eqvt simp del: envop_def) lemma env_minus_eqvt: fixes pi::"name prm" shows "(pi\\) |- pi\eff = pi\(\ |- eff)" by (nominal_induct eff avoiding: \ rule: eff.induct) (auto simp add: eff.eqvts envop_eqvt simp del: envop_def) lemma env_plus_simple_eff: assumes "simple_eff eff" shows "\ |+ eff = \" using prems by (induct eff rule: simple_eff_cases) auto lemma env_minus_simple_eff: assumes "simple_eff eff" shows "\ |- eff = \" using prems by (induct eff rule: simple_eff_cases) auto fun comb_eff :: "eff \ eff \ eff \ eff" where "comb_eff F1 F2 F3 = eff.NE" lemma comb_eff_eqvt[eqvt]: fixes pi :: "name prm" shows "(pi\ (comb_eff F1 F2 F3)) = comb_eff (pi\F1) (pi\F2) (pi\F3) " using comb_eff.simps by auto text {* type judgments *} inductive typing :: "varEnv \ trm \ ty \ eff \ bool" (" _ \ _ : _ ; _ " [60,60,60,60] 60) where T_Var[intro]: "\valid \; (v,T)\set \\\ \ \ Var v : T ; VE v" | T_Const[intro]: "valid \ \ \\<^isub>\ b = T \ \ \ (BI b) : T ; TT" | T_Num[intro]: "valid \ \ \ \ (Num n) : ty.Int ; TT" | T_True[intro]: "valid \ \ \ \ (Bool True) : ty.TT ; TT" | T_False[intro]: "valid \ \ \ \ (Bool False) : ty.FF ; FF" | T_Abs[intro]: "\x \ \; ((x,T1)#\) \ b : T2; eff\ \ \ \ Lam [x:T1].b : (T1\T2 : latent_eff.NE) ; TT" | T_App[intro]: "\(\ \ e1 : U ; eff1) ; \ U <: (T0 \ T1 : le); (\ \ e2 : T; eff2) ; \ T <: T0\ \ \ \ App e1 e2 : T1 ; NE" | T_AppPred[intro]: "\\ \ e1 : U; eff1; \ U <: (T0 \ T1 : Latent S); \ \ e2 : T; VE x ; \ T <: T0\ \ \ \ App e1 e2 : T1 ; TE S x" | T_If[intro]: "\\ \ e1 : T1; eff1; (\ |+ eff1) \ e2 : T2; eff2; (\ |- eff1) \ e3 : T3; eff3; \ T2 <: T; \ T3 <: T\ \ \ \ (Iff e1 e2 e3) : T ; comb_eff eff1 eff2 eff3" | T_AppPredTrue[intro]: "\\ \ e1 : U; eff1; \ U <: (T0 \ T1 : Latent S); \ \ e2 : T; eff2 ; \ T <: T0; \ T <: S\ \ \ \ App e1 e2 : T1 ; TT" | T_AppPredFalse[intro]: "\\ \ e1 : U; eff1; \ U <: (T0 \ T1 : Latent S); \ \ e2 : T; eff2 ; \ T <: T0; ~(\ T <: S) ; e2 : values ; closed e2\ \ \ \ App e1 e2 : T1 ; FF" | T_IfTrue[intro]: "\\ \ e1 : T1 ; TT ; \ \ e2 : T2 ; eff; \ T2 <: T\ \ \ \ (Iff e1 e2 e3) : T ; NE" | T_IfFalse[intro]: "\\ \ e1 : T1 ; FF ; \ \ e3 : T3 ; eff; \ T3 <: T\ \ \ \ (Iff e1 e2 e3) : T ; NE" | T_AbsPred[intro]: "\x \ \; ((x,T1)#\) \ b : T2; TE S x\ \ \ \ Lam [x:T1].b : (T1\T2 : Latent S) ; TT" equivariance typing nominal_inductive typing by (auto simp add: abs_fresh) text {* then we begin on preservation *} abbreviation "sub" :: "(name\ty) list \ (name\ty) list \ bool" (" _ \ _ " [80,80] 80) where "\1 \ \2 \ \a \. (a,\)\set \1 \ (a,\)\set \2" lemma envplus_empty: shows "env_plus eff [] = []" by (nominal_induct rule: eff.induct) auto lemma envminus_empty: shows "env_minus eff [] = []" by (nominal_induct rule: eff.induct) auto lemma w_lem1: fixes \ \' assumes "\ \ \'" and a:"valid \'" shows "map f \ \ map f \'" proof - let ?mapfun = f from prems have "set \ <= set \'" by auto hence "set (map ?mapfun \) <= set (map ?mapfun \')" by auto hence "(map ?mapfun \) \ (map ?mapfun \')" by blast thus ?thesis . qed lemma weakening_envplus: assumes b:"\ \ \'" and a:"valid \'" shows "env_plus eff \ \ env_plus eff \'" using a prems w_lem1[of \ \'] by (nominal_induct eff avoiding: \ \' rule: eff.induct) auto lemma weakening_envminus: assumes "\ \ \'" and a:"valid \'" and b:"valid \" shows "env_minus eff \ \ env_minus eff \'" using a prems w_lem1[of \ \'] by (nominal_induct eff avoiding: \ \' rule: eff.induct) auto lemma envplus_valid: assumes "valid \" shows "valid (\ |+ F)" using prems proof (induct rule: valid.induct) case v1 thus ?case using envplus_empty by auto next case (v2 \' a T) from v2 show ?case proof (nominal_induct rule: eff.induct) case (TE S x) let ?op = "restrict" let ?G = "((a, T) # \')" let ?mapfun = "(% (v,ty). (if (x = v) then (v,?op S ty) else (v,ty)))" have C:"valid (map ?mapfun \')" using v2 `valid (\' |+ TE S x)` by auto hence D:"a \ (map ?mapfun \')" using v2 envop_fresh `valid (\' |+ TE S x)` by auto thus ?case proof (cases "a = x") case False from D have E:"valid ((a,T)# (map ?mapfun \'))" using C by auto from False have B:"?G |+ TE S x = ((a,T)# (map ?mapfun \'))" by auto thus ?thesis using E by auto next case True hence B:"?G |+ TE S x = ((a,?op S T)# (map ?mapfun \'))" by auto from D have E:"valid ((a,?op S T)# (map ?mapfun \'))" using C by auto thus ?thesis using B by auto qed next case (VE x) thus ?case proof - let ?op = "remove" let ?G = "((a, T) # \')" let ?mapfun = "(% (v,ty). (if (x = v) then (v,?op ty.FF ty) else (v,ty)))" have C:"valid (map ?mapfun \')" using v2 `valid (\' |+ VE x)` by auto hence D:"a \ (map ?mapfun \')" using v2 envop_fresh `valid (\' |+ VE x)` by auto thus ?case proof (cases "a = x") case False from D have E:"valid ((a,T)# (map ?mapfun \'))" using C by auto from False have B:"?G |+ VE x = ((a,T)# (map ?mapfun \'))" by auto thus ?thesis using E by auto next case True hence B:"?G |+ VE x = ((a,?op ty.FF T)# (map ?mapfun \'))" by auto from D have E:"valid ((a,?op ty.FF T)# (map ?mapfun \'))" using C by auto thus ?thesis using B by auto qed qed qed (auto) qed lemma envminus_valid: assumes "valid \" shows "valid (\ |- F)" using prems proof (induct rule: valid.induct) case v1 thus ?case using envminus_empty by auto next case (v2 \' a T) thus ?case proof (nominal_induct rule: eff.induct) case (TE S x) let ?op = "remove" let ?G = "((a, T) # \')" let ?mapfun = "(% (v,ty). (if (x = v) then (v,?op S ty) else (v,ty)))" have C:"valid (map ?mapfun \')" using v2 `valid (\' |- TE S x)` by auto hence D:"a \ (map ?mapfun \')" using v2 envop_fresh `valid (\' |- TE S x)` by auto thus ?case proof (cases "a = x") case False from D have E:"valid ((a,T)# (map ?mapfun \'))" using C by auto from False have B:"?G |- TE S x = ((a,T)# (map ?mapfun \'))" by auto thus ?thesis using E by auto next case True hence B:"?G |- TE S x = ((a,?op S T)# (map ?mapfun \'))" by auto from D have E:"valid ((a,?op S T)# (map ?mapfun \'))" using C by auto thus ?thesis using B by auto qed next case (VE x) thus ?case proof - let ?op = "replace" let ?G = "((a, T) # \')" let ?mapfun = "(% (v,ty). (if (x = v) then (v,?op ty.FF ty) else (v,ty)))" have C:"valid (map ?mapfun \')" using v2 `valid (\' |- VE x)` by auto hence D:"a \ (map ?mapfun \')" using v2 envop_fresh `valid (\' |- VE x)` by auto thus ?case proof (cases "a = x") case False from D have E:"valid ((a,T)# (map ?mapfun \'))" using C by auto from False have B:"?G |- VE x = ((a,T)# (map ?mapfun \'))" by auto thus ?thesis using E by auto next case True hence B:"?G |- VE x = ((a,?op ty.FF T)# (map ?mapfun \'))" by auto from D have E:"valid ((a,?op ty.FF T)# (map ?mapfun \'))" using C by auto thus ?thesis using B by auto qed qed qed (auto) qed lemma weakening: assumes a: "\1 \ t : \ ; F" and b: "valid \2" and c: "\1 \ \2" and d:"valid \1" shows "\2 \ t:\ ; F" using a b c d proof (nominal_induct \1 t \ F avoiding: \2 rule: typing.strong_induct) case (T_If \ t1 T1 F1 t2 T2 F2 t3 T3 F3 T \2) have A:"valid (\ |+ F1)" using T_If envplus_valid by auto have B:"valid (\ |- F1)" using T_If envminus_valid by auto have A':"valid (\2 |+ F1)" using T_If envplus_valid by auto have B':"valid (\2 |- F1)" using T_If envminus_valid by auto have C:"(\ |+ F1) \ (\2 |+ F1)" using T_If weakening_envplus by auto have D:"(\ |- F1) \ (\2 |- F1)" using T_If weakening_envminus by auto show ?case using T_If A B C D A' B' by blast qed (auto | atomize)+ (* FIXME: before using meta-connectives and the new induction *) (* method, this was completely automatic *) (* need weakening lemmas about env+/- *) lemma "[] \ (Lam[x:Top]. (Iff (App (BI NumberP) (Var x)) (App (BI Add1) (Var x)) (Num 12))) : (Top \ ty.Int : latent_eff.NE) ; TT" apply (rule T_Abs) apply (auto simp add: fresh_def supp_def perm_fun_def) apply (rule T_If) apply auto apply (rule T_AppPred) apply (auto simp add: valid.intros) apply (rule T_App) apply (rule T_Const) defer apply ( simp add: valid.intros) apply (rule S_Refl) apply (rule T_Var) apply (simp add: valid.intros)+ apply (rule S_Refl) apply (simp add: valid.intros)+ done (* inductive cases about typing *) inductive_cases iff_t_cases : "G \ Iff tst thn els : t ; e" inductive_cases app_bi_cases : "G \ App (Const (BI b)) rand : t ; e" inductive_cases type_arr_case_num: "\ \ ((Num n)) : (T1 \ T2 : eff) ; eff'" inductive_cases type_arr_case_bool: "\ \ ((Bool b)) : (T1 \ T2 : eff) ; eff'" inductive_cases type_bi_case: "\ \ ((BI b)) : t ; eff" inductive_cases type_add1_case: "\ \ ((BI Add1)) : t ; eff" inductive_cases bi_typing_cases: "\ \ (BI b) : t ; eff" inductive_cases abs_ty_int: "\ \ (Abs x body t) : ty.Int ; eff'" inductive_cases abs_ty_bool: "\ \ (Abs x body t) : BoolTy ; eff'" inductive_cases const_ty_int: "\ \ e : ty.Int ; eff'" inductive_cases const_ty_bool: "\ \ e : BoolTy ; eff'" inductive_cases iff_false_ty: "\ \ Iff (Bool False) thn els : t ; eff" inductive_cases app_bi_ty: "\ \ App (BI b) arg : t ; eff" (* Typing Values*) lemma false_ty_elim[rule_format]: "\ \ (trm.Bool False) : \ ; eff \ \ = ty.FF \ eff = FF \ valid \" apply (ind_cases "\ \ (trm.Bool False) : \ ; eff") apply (auto simp add: trm.inject) done lemma num_ty_elim[rule_format]: "\ \ (Num n) : \ ; eff \ \ = ty.Int \ eff = TT \ valid \" by (ind_cases "\ \ (Num n) : \ ; eff") auto lemma true_ty_elim[rule_format]: "\ \ (trm.Bool True) : \ ; eff \ \ = ty.TT \ eff = TT \ valid \ " by (ind_cases "\ \ (trm.Bool True) : \ ; eff") (auto simp add: trm.inject) lemma bool_ty_elim[rule_format]: "\ \ (trm.Bool b) : \ ; eff \ (\ = ty.TT \ \ = ty.FF) \ valid \ " apply (ind_cases "\ \ (trm.Bool b) : \ ; eff") apply (auto simp add: trm.inject) done lemma bi_ty_elim[rule_format]: "\ \ (BI b) : \ ; eff \ eff = TT \ \ = \\<^isub>\ b \ valid \" apply (ind_cases "\ \ (BI b) : \ ; eff") apply (auto simp add: trm.inject) done inductive_cases bool_sub_int: "\ BoolTy <: ty.Int" inductive_cases tt_sub_int: "\ ty.TT <: ty.Int" inductive_cases ff_sub_int: "\ ty.FF <: ty.Int" thm bool_sub_int inductive_cases arr_sub_int: "\ A\B:L <: ty.Int" inductive_cases int_sub_tt: "\ ty.Int <: ty.TT" inductive_cases int_sub_ff: "\ ty.Int <: ty.FF" inductive_cases arr_sub_tt: "\ A\B:L <: ty.TT" inductive_cases arr_sub_ff: "\ A\B:L <: ty.FF" inductive_cases int_sub_bool_cases: "\ ty.Int <: Union [ty.TT, ty.FF]" inductive_cases arr_sub_bool_cases: "\ A\B:L <: Union [ty.TT, ty.FF]" declare BoolTy_def[simp] lemma int_sub_bool: assumes "\ ty.Int <: BoolTy" shows "P" using prems proof - have "\ ty.Int <: ty.TT \ \ ty.Int <: ty.FF" using prems int_sub_bool_cases by auto thus ?thesis using int_sub_ff int_sub_tt by auto qed lemma arr_sub_bool: assumes "\ A\B:L <: BoolTy" shows "P" using prems proof - have "\ A\B:L <: ty.TT \ \ A\B:L <: ty.FF" using prems arr_sub_bool_cases[of A B L] by auto thus ?thesis using arr_sub_ff[of A B L] arr_sub_tt[of A B L] by auto qed thm int_sub_bool inductive_cases abs_ty_elim2[consumes 1, case_names 1]: "\ \ Lam[x:S].b : T ; eff" lemma int_value: assumes a:"v : values" and b:"\ \ v : T ; F" and c:"\ T <: ty.Int" shows "EX n. v = (Num n)" using prems proof (induct rule: values.induct) case num_value thus ?case by auto next case (bool_value b) hence "T = ty.TT \ T = ty.FF" using bool_ty_elim by auto thus ?case using bool_value tt_sub_int ff_sub_int by auto next case (abs_value b S x) thus ?case using arr_sub_int by (induct rule: abs_ty_elim2) auto next case (bi_value b) thus ?case using bi_ty_elim[of \ b T F] using arr_sub_int by (nominal_induct b rule: builtin.induct) auto qed lemma bool_value: assumes a:"v : values" and b:"\ \ v : T ; F" and c:"\ T <: BoolTy" shows "EX b. v = (Bool b)" using prems proof (induct rule: values.induct) case num_value thus ?case using num_ty_elim[of \ _ T F] int_sub_bool by auto next case (bool_value b) thus ?case by auto next case (abs_value b S x) thus ?case using arr_sub_bool by (induct rule: abs_ty_elim2) auto next case (bi_value b) thus ?case using bi_ty_elim[of \ b T F] using arr_sub_bool by (nominal_induct b rule: builtin.induct) auto qed lemma value_int_ty: assumes a:"\ \ e : ty.Int ; eff" and b: "e : values" shows "EX n. e = (Num n)" using b a int_value[of e _ ty.Int] by auto lemma value_bool_ty: assumes a:"\ \ e : BoolTy ; eff" and b: "e : values" shows "EX b. e = (Bool b)" using b a bool_value[OF b a] by auto lemma typing_bi: assumes a:"\ \ (BI b) : t ; eff" shows "t = \\<^isub>\ b" using a bi_typing_cases[of \ b t eff "t = \\<^isub>\ b"] by (simp add: trm.inject) inductive_cases arr_sub_arr_cases:"\ A1 \ A2 : L <: B1 \ B2 : L'" lemma typed_prim_reduce: assumes a:"\ \ (BI b) : U ; eff" and b:"\ \ v : T ; eff'" and c:"v : values" and sub:"\ T <: T0" and d: "\ U <: T0 \ T1 : le" shows "EX v'. \ b v = Some v'" using a b c d sub proof (nominal_induct b rule: builtin.induct) case Add1 have "U = \\<^isub>\ Add1" using Add1 typing_bi[of \ Add1 "U" eff] by simp hence "U = ty.Int \ ty.Int : latent_eff.NE" by auto hence "\ T <: ty.Int " and "le = latent_eff.NE" using sub d arr_sub_arr_cases[of ty.Int ty.Int latent_eff.NE T0 T1 le] by auto hence "EX n. v = (Num n)" using c b int_value by auto then obtain n where "v = (Num n)" by auto thus ?case by (auto simp add: \.simps) next case Nott show ?case using `v : values` Nott by (induct v rule: values.induct) auto next case NumberP thus ?case by auto next case BooleanP thus ?case by auto next case ProcP thus ?case by auto qed text {* Progress together with necessary lemmas *} (* first some lemmas about decomposing various kinds of syntax *) lemma if_decomp: assumes b:"closed tst \ (\E L R. tst = E L \ E \ ctxt \ L \ R) \ tst : values" and c:"closed (Iff tst thn els)" shows "(EX E L R. (Iff tst thn els) = E L \ E : ctxt \ L \ R) \ (Iff tst thn els) : values" proof - { assume "tst : values" hence "EX E L R. Iff tst thn els = E L \ E : ctxt \ (L \ R)" using if_val_reduces[of tst thn els] ex_help[of "Iff tst thn els" "(%t. t)"] by auto } moreover { assume asm:"~ tst : values" have cl:"closed tst" using `closed (Iff tst thn els)` by (auto simp add: closed_def trm.supp) hence ih:"\E t t'. tst = E t \ E \ ctxt \ t \ t'" using b asm by auto hence "\E t t' . Iff tst thn els = E t \ E \ ctxt \ t \ t'" using reduce_in_ctxt[of "(%t . (Iff t thn els))"] ih by auto } ultimately show ?thesis by auto qed inductive_cases tt_sub_arr_cases: "\ ty.TT <:A1 \ A2 : L" inductive_cases ff_sub_arr_cases: "\ ty.FF <:A1 \ A2 : L" inductive_cases num_sub_arr_cases: "\ ty.Int <:A1 \ A2 : L" lemma app_decomp: assumes a:" G \ rator : U ; eff1" and a':"\ U <: T0 \ T1 : le" and aa:" G \ rand : T ; eff" and b:"closed rator \ (\E L R. rator = E L \ E \ ctxt \ L \ R) \ rator \ values" and bb:"closed rand \ (\E L R. rand = E L \ E \ ctxt \ L \ R) \ rand \ values" and c:"closed (App rator rand)" and sub:"\ T <: T0" shows "(EX E L R. (App rator rand) = E L \ E : ctxt \ L \ R) \ (App rator rand) : values" proof - have well_typed:"G \ (App rator rand) : T1 ; eff.NE" using T_App[of G rator U eff1 T0 T1 le rand T eff] a a' aa sub by auto have "closed rator" using c by (auto simp add: closed_def trm.supp) hence ih1:"(\E L R. rator = E L \ E \ ctxt \ L \ R) \ rator \ values" using b by simp have "closed rand" using c by (auto simp add: closed_def trm.supp) hence ih2:"(\E L R. rand = E L \ E \ ctxt \ L \ R) \ rand \ values" using bb by simp { assume asm1:"rator \ values" and asm2:"rand \ values" hence "(EX E L R. (App rator rand) = E L \ E : ctxt \ L \ R)" using asm1 a aa a' sub well_typed proof (nominal_induct avoiding: rand rule: values.strong_induct ) case (abs_value x t b) let ?E = "(%t. t)" let ?L = "App (Abs x b t) rand" have "?L \ (b[x::=rand])" by (rule e_beta) thus ?case using ex_help[of ?L ?E ?L] by auto next case (bool_value b) hence "U = ty.TT \ U = ty.FF" using true_ty_elim false_ty_elim by (cases b) auto thus ?case using tt_sub_arr_cases[of T0 T1 le] ff_sub_arr_cases[of T0 T1 le] `\ U <: T0 \ T1 : le` by blast next case (num_value b) hence "U = ty.Int" using num_ty_elim by auto thus ?case using num_sub_arr_cases[of T0 T1 le] num_value by auto next case (bi_value b) let ?E = "(%t. t)" let ?L = "App ((BI b)) rand" have h:"\v. (\ b rand) = (Some v) \ App ((BI b)) rand \ v" using bi_value by auto have "EX v . (\ b rand) = (Some v)" using bi_value typed_prim_reduce[of G b U] by auto then obtain v' where "(\ b rand) = (Some v')" by auto then show ?case using h[of v'] ex_help[of ?L ?E] by auto qed } moreover { assume asm1:"rator \ values" and asm2:"rand \ values" have "\E t t' . App rator rand = E t \ E \ ctxt \ t \ t'" using asm1 asm2 reduce_in_ctxt[of "(%t . (App rator t))"] ih2 by auto } moreover { assume asm:"rator \ values" have "\E t t' . App rator rand = E t \ E \ ctxt \ t \ t'" using asm reduce_in_ctxt[of "(%t . (App t rand))"] ih1 by auto } ultimately show ?thesis by auto qed (* then the main lemma, that every well typed term can be decomposed into a context and a redex *) lemma decomposition: assumes a:"closed e" and b:"\ \ e : t ; eff" shows "(EX E L R. e = E L \ E : ctxt \ L \ R) \ e : values" using b a proof (induct rule: typing.induct) case T_Var thus ?case using closed_def by (auto simp add: at_supp at_name_inst trm.supp) next case T_If thus ?case using if_decomp by auto next case T_IfTrue thus ?case using if_decomp by auto next case T_IfFalse thus ?case using if_decomp by auto next case T_App thus ?case using app_decomp by auto next case T_AppPred thus ?case using app_decomp by auto next case T_AppPredTrue thus ?case using app_decomp by auto next case T_AppPredFalse thus ?case using app_decomp by auto qed (simp_all) (* The value cases are automatic *) (* Now we conclude progress *) theorem progress: assumes typed:"\ \ e : t ; eff" and cl:"closed e" shows "e : values \ (EX e'. e \ e')" proof (cases "e : values") case False hence "(\E L R. e = E L \ E \ ctxt \ L \ R)" using decomposition[OF cl typed] by auto thus ?thesis by auto qed (simp) (* Some useful lemmas for deriving facts from typing derivations *) inductive_cases app_ty_elim2[consumes 1, case_names 1 2 3 4]: "\ \ App t1 t2 : \ ; eff" thm app_ty_elim2 inductive_cases iff_ty_elim2[consumes 1, case_names 1 2 3]: "\ \ Iff t1 t2 t3 : T ; eff" thm abs_ty_elim2 (* slow *) lemma app_ty_elim[rule_format]: "\ \ App t1 t2 : \ ; eff \ \ T0 T0' T1 le eff' eff'' U. (\ \ t1 : U ; eff' \ \ \ t2 : T0' ; eff'' \ \ U <: T0 \ T1 : le \ \ T0' <: T0 \ T1 = \)" apply (ind_cases "\ \ App t1 t2 : \ ; eff") apply (auto simp add: trm.inject ty.inject) by metis+ lemma abs_ty_elim_eff[rule_format]: "\\ \ Lam[a:T0].b : \ ; eff\ \ eff = eff.TT" by (ind_cases "\ \ Lam[a:T0].b : \ ; eff") (auto simp add: trm.inject) lemma abs_ty_elim[rule_format]: "\\ \ Lam[a:T0].b : \ ; eff ; a \ \\ \ \ T1 eff' L S. ((a,T0)#\ \ b : T1 ; eff' \ \ = (T0 \ T1 : L) \ eff = eff.TT \ ((eff' = TE S a \ L = Latent S) \ L = latent_eff.NE))" apply (ind_cases "\ \ Lam[a:T0].b: \ ; eff") apply(auto simp add: trm.distinct trm.inject alpha) apply(drule_tac pi="[(a,x)]::name prm" in typing.eqvt) apply(auto) apply(subgoal_tac "([(a,x)]::name prm)\\ = \")(*A*) apply(force simp add: calc_atm) (*A*) apply(force intro!: pt_fresh_fresh[OF pt_name_inst, OF at_name_inst]) apply(drule_tac pi="[(a,x)]::name prm" in typing.eqvt) apply(auto) apply(subgoal_tac "([(a,x)]::name prm)\\ = \")(*A*) apply(force simp add: calc_atm) (*A*) apply(force intro!: pt_fresh_fresh[OF pt_name_inst, OF at_name_inst]) done inductive_cases abs_ty_cases[consumes 1, case_names 1 2]:"\ \ Lam[a:T0].b: \ ; eff" thm abs_ty_cases (* lemma app_abs_ty_elim_eff[rule_format]: "\\ \ App (Abs x b T) t2 : \ ; eff ; x \ \\ \ eff = eff.NE" proof (ind_cases "\ \ App (Abs x b T) t2 : \ ; eff", auto simp add: trm.inject abs_ty_elim) fix T0 S eff1 U assume "\ \ Lam [x:T].b : U ; eff1 "" \ U <: T0 \ \ : Latent S" "x \ \" then obtain T1 L where "U = T \ T1 : L" using abs_ty_elim[of \ x b T "U" L] by auto thus False using prems arr_sub_arr_cases[of T _ latent_eff.NE T0 \ "Latent S"] by (auto simp add: ty.inject) next fix T0 S eff1 U assume "\ \ Lam [x:T].b : U ; eff1 "" \ U <: T0 \ \ : Latent S" "x \ \" then obtain T1 where "U = T \ T1 : latent_eff.NE" using abs_ty_elim[of \ x b T "U"] by auto thus False using prems arr_sub_arr_cases[of T _ latent_eff.NE T0 \ "Latent S"] by (auto simp add: ty.inject) next fix T0 S eff1 U assume "\ \ Lam [x:T].b : U ; eff1 "" \ U <: T0 \ \ : Latent S" "x \ \" then obtain T1 where "U = T \ T1 : latent_eff.NE" using abs_ty_elim[of \ x b T "U"] by auto thus False using prems arr_sub_arr_cases[of T _ latent_eff.NE T0 \ "Latent S"] by (auto simp add: ty.inject) qed *) lemma if_ty_elim_weak[rule_format]: "\ \ Iff t1 t2 t3: \ ; eff \ \ T0 eff'. (\ \ t1 : T0 ; eff') \ eff = NE" by (ind_cases "\ \ Iff t1 t2 t3: \ ; eff") (auto simp add: trm.inject) lemma if_ty_elim[rule_format]: "\ \ Iff t1 t2 t3: \ ; eff \ (\ T1 T2 T3 F1 F2 F3. (\ \ t1 : T1 ; F1) \ \ |+ F1 \ t2 : T2 ; F2 \ \ |- F1 \ t3 : T3 ; F3 \ \ T2 <: \ \ \ T3 <: \ \ eff = NE) \ (\ T1 T3 F3. (\ \ t1 : T1 ; FF) \ \ \ t3 : T3 ; F3 \ \ T3 <: \ \ eff = NE) \ (\ T1 T2 F2. (\ \ t1 : T1 ; TT) \ \ \ t2 : T2 ; F2 \ \ T2 <: \ \ eff = NE)" proof (ind_cases "\ \ Iff t1 t2 t3: \ ; eff") fix e1 T1 eff1 e2 T2 eff2 e3 T3 eff3 assume "Iff t1 t2 t3 = Iff e1 e2 e3"" eff = eff.NE"" \ \ e1 : T1 ; eff1"" env_plus eff1 \ \ e2 : T2 ; eff2 " "env_minus eff1 \ \ e3 : T3 ; eff3"" \ T2 <: \"" \ T3 <: \" hence A:"t1 = e1" "t2 = e2" "t3 = e3" using trm.inject by auto thus ?thesis using prems by blast next fix e1 T1 e2 T2 effa e3 assume "Iff t1 t2 t3 = Iff e1 e2 e3"" eff = eff.NE"" \ \ e1 : T1 ; TT "" \ \ e2 : T2 ; effa "" \ T2 <: \" thus ?thesis by (auto simp add: trm.inject) next fix e1 T1 e2 T3 effa e3 assume "Iff t1 t2 t3 = Iff e1 e2 e3"" eff = eff.NE"" \ \ e1 : T1 ; FF "" \ \ e3 : T3 ; effa "" \ T3 <: \" thus ?thesis by (auto simp add: trm.inject) qed inductive_cases iff_false_ty_cases: "\ \ Iff (trm.Bool False) t2 t3: \ ; eff" inductive_cases ff_eff_cases: "\ \ e : T; FF" inductive_cases tt_eff_cases: "\ \ e : T; TT" inductive_cases ne_eff_cases: "\ \ e : T; NE" lemma if_true_ty_elim[rule_format]: "\\ \ Iff v t2 t3: \ ; eff ; v : values; v ~= Bool False\ \ \ T0 eff'. ((\ \ t2 : T0 ; eff') \ \ T0 <: \ \ eff = NE)" proof (ind_cases "\ \ Iff (v) t2 t3: \ ; eff") fix eff1 eff2 T1 T2 e1 e2 e3 assume "v : values" "env_plus eff1 \ \ e2 : T2 ; eff2" "Iff v t2 t3 = Iff e1 e2 e3" "\ T2 <: \" "\ \ e1 : T1 ; eff1" "eff = NE" have "\ \ v : T1 ; eff1" using prems by (simp add: trm.inject) have "eff1 = eff.NE \ eff1 = FF \ eff1 = TT" using `v : values` `\ \ v : T1 ; eff1` proof (induct rule: values.induct) case (abs_value b T x) thus ?case using abs_value abs_ty_elim_eff by auto next case (num_value n) thus ?case using num_ty_elim by auto next case (bool_value n) thus ?case using false_ty_elim true_ty_elim by (cases n) auto next case bi_value thus ?case using bi_ty_elim by auto qed hence "env_plus eff1 \ = \" by auto hence "\ \ e2 : T2 ; eff2 \ \ T2 <: \" using prems by auto thus ?thesis using prems by (auto simp add: trm.inject) next fix e1 T2 e2 e3 effa assume "Iff v t2 t3 = Iff e1 e2 e3" "\ \ e2 : T2 ; effa" "\ T2 <: \" "eff = NE" thus ?thesis by (auto simp add: trm.inject) next fix e1 T1 e3 T3 effa e2 assume "v : values" "v \ trm.Bool False" "Iff v t2 t3 = Iff e1 e2 e3" "\ \ e1 : T1 ; FF" "eff = NE" have "v = e1" using prems trm.inject by auto hence tv:"\ \ v : T1 ; FF" by simp have "v = Bool False" using `v : values` tv proof (induct v rule: values.induct) case (abs_value x T b) thus ?case using abs_ty_elim_eff[of \ x b T T1 FF] by auto next case (num_value n) thus ?case using num_ty_elim[of _ _ _ FF] by auto next case (bool_value n) thus ?case using true_ty_elim[of _ _ FF] by (cases n) auto next case bi_value thus ?case using bi_ty_elim[of _ _ _ FF] by auto qed show ?thesis using `v = Bool False` `v ~= Bool False` by auto qed lemma if_false_ty_elim[rule_format]: "\ \ Iff (trm.Bool False) t2 t3: \ ; eff \ \ T0 eff'. ((\ \ t3 : T0 ; eff') \ \ T0 <: \ \ eff = eff.NE)" proof (ind_cases "\ \ Iff (trm.Bool False) t2 t3: \ ; eff") fix e1 e2 e3 T1 assume "Iff (trm.Bool False) t2 t3 = Iff e1 e2 e3" and "\ \ e1 : T1 ; TT" hence "\ \ (trm.Bool False) : T1 ; TT" by (simp add: trm.inject) hence "TT = FF" using false_ty_elim[of \ T1 TT] by simp thus ?thesis by (simp) next fix e1 e2 e3 T1 T3 effa assume "Iff (trm.Bool False) t2 t3 = Iff e1 e2 e3" and " eff = eff.NE"and" \ \ e1 : T1 ; FF" and " \ \ e3 : T3 ; effa"and " \ T3 <: \" thus ?thesis by (auto simp add: trm.inject) next fix e1 e2 e3 T1 T3 eff1 eff3 assume "Iff (trm.Bool False) t2 t3 = Iff e1 e2 e3" and "eff = eff.NE" and f:"\ \ e1 : T1 ; eff1" and g:"env_minus eff1 \ \ e3 : T3 ; eff3" and "\ T3 <: \" hence "e1 = Bool False" and "t3 = e3" by (auto simp add: trm.inject) hence "eff1 = FF" using f false_ty_elim by auto hence "env_minus eff1 \ = \" by simp hence "\ \ e3 : T3 ; eff3" using g by simp thus ?thesis using `t3 = e3` `\ T3 <: \` `eff = eff.NE` by auto qed lemma var_ty_elim: "\ \ Var v : \ ; eff \ (v,\) : set \ \ eff = VE v \ valid \" by (ind_cases "\ \ Var v : \ ; eff") (auto simp add: trm.inject) inductive_cases app_ty_ff:"\ \ App e arg : T' ; FF" lemma app_ty_ff_elim: "\ \ App rator rand : T ; FF \ EX S T0 le F1 T0' F2 U. \ \ rator : U ; F1 \ \ \ rand : T0' ; F2 \ \ T0' <: T0 \ \ U <: T0 \ T : le \ le = Latent S \ (~ (\ T0' <: S)) \ rand : values \ closed rand" proof (ind_cases "\ \ App rator rand : T ; FF") fix e1 T0 S eff1 e2 Ta eff2 U assume "App rator rand = App e1 e2 "" \ \ e1 : U ; eff1 " "\ U <: T0 \ T : Latent S" "\ \ e2 : Ta ; eff2 ""\ Ta <: T0""~ (\ Ta <: S)" "e2 : values" "closed e2" have a:" \ \ rator : U ; eff1 " using prems trm.inject by auto have b:"\ \ rand : Ta ; eff2" using prems trm.inject by auto have c:"rand : values" "closed rand" using prems trm.inject by auto from a b c prems show ?thesis by blast qed lemma app_ty_tt_elim: "\ \ App rator rand : T ; TT \ EX S T0 le F1 T0' F2 U. \ \ rator : U ; F1 \ \ \ rand : T0' ; F2 \ \ T0' <: T0 \ \ U <: T0 \ T : le \ le = Latent S \ \ T0' <: S " proof (ind_cases "\ \ App rator rand : T ; TT") fix e1 T0 S eff1 e2 Ta eff2 U assume "App rator rand = App e1 e2 "" \ \ e1 : U ; eff1 " "\ U <: T0 \ T : Latent S" "\ \ e2 : Ta ; eff2 ""\ Ta <: T0"" \ Ta <: S" have a:" \ \ rator : U ; eff1 " using prems trm.inject by auto have b:"\ \ rand : Ta ; eff2" using prems trm.inject by auto from a b prems show ?thesis by blast qed text {* values don't have union types *} lemma value_simple_type: assumes A:"\ \ v : T ; F" and B:"v : values" shows "simple_ty T" using B A proof (nominal_induct v avoiding: \ rule: values.strong_induct) case (bi_value b) thus ?case using bi_ty_elim[of \ b T F] by (nominal_induct b rule: builtin.induct) (auto simp add: trm.inject) next case num_value thus ?case using num_ty_elim[OF num_value] by auto next case bool_value thus ?case using bool_ty_elim[OF bool_value] by auto next case (abs_value a T' b \') thus ?case using abs_ty_elim[of \' a b T' T F] by auto qed text {* lemmas about the effects of closed terms *} lemma ve_not_closed: "\ \ e : T ; eff.VE x \ x : supp e" by (ind_cases "\ \ e : T ; eff.VE x") (auto simp add: eff.inject trm.supp at_supp supp_atm) lemma te_not_closed: "\ \ e : T ; eff.TE T' x \ x : supp e" proof (ind_cases "\ \ e : T ; eff.TE T' x") fix e1 T0 S eff1 e2 Ta xa assume "e = App e1 e2" "TE T' x = TE S xa" "\ \ e2 : Ta ; VE xa" have "x = xa" using prems eff.inject by auto hence "\ \ e2 : Ta ; VE x" using prems eff.inject by auto hence "x : supp e2" using ve_not_closed by auto thus "x : supp e" using prems trm.supp by auto qed lemma closed_eff: assumes "closed e" and "\ \ e : T ; eff" shows "simple_eff eff" using prems proof (nominal_induct eff rule: eff.induct) case (VE name) thus ?case using ve_not_closed[of _ e _ name] closed_def by auto next case (TE _ name) thus ?case using te_not_closed[of _ e _ _ name] closed_def by auto qed (auto) lemma closed_eff_below_NE: assumes "closed e" and "\ \ e : T ; eff" shows "\ eff \ (Num n) : ty.Int ; eff" inductive_cases trm_ty_int_case: "\ \ e : ty.Int ; eff" inductive_cases const_ty_bool_case: "\ \ (Bool b) : BoolTy ; eff" lemma add1_eff_ne: "\ \ (App (BI Add1) v) : T1 ; eff1 \ eff1 = eff.NE" proof (ind_cases " \ \ (App (BI Add1) v) : T1 ; eff1") assume "eff1 = eff.NE" thus ?thesis by simp next fix T0 T1 S eff1a e1 e2 U assume "\ \ e1 : U ; eff1a" "App (BI Add1) v = App e1 e2" "\ U <: T0 \ T1 : Latent S" hence "\ \ (BI Add1) : U ; eff1a" by (simp add: trm.inject) hence "\\<^isub>\ Add1 = U" using type_add1_case[of \ "U"] by (auto simp add: trm.inject) hence "\ = ty.Int \ ty.Int : latent_eff.NE" by auto thus ?thesis using prems arr_sub_arr_cases[of ty.Int ty.Int latent_eff.NE] by (auto simp add: ty.inject) next fix T0 T1 S eff1a e1 e2 U assume "\ \ e1 : U ; eff1a" "App (BI Add1) v = App e1 e2" "\ U <: T0 \ T1 : Latent S" hence "\ \ (BI Add1) : U ; eff1a" by (simp add: trm.inject) hence "\\<^isub>\ Add1 = U" using type_add1_case[of \ "U"] by (auto simp add: trm.inject) hence "\ = ty.Int \ ty.Int : latent_eff.NE" by auto thus ?thesis using prems arr_sub_arr_cases[of ty.Int ty.Int latent_eff.NE] by (auto simp add: ty.inject) next fix T0 T1 S eff1a e1 e2 U assume "\ \ e1 : U ; eff1a" "App (BI Add1) v = App e1 e2" "\ U <: T0 \ T1 : Latent S" hence "\ \ (BI Add1) : U ; eff1a" by (simp add: trm.inject) hence "\\<^isub>\ Add1 = U" using type_add1_case[of \ "U"] by (auto simp add: trm.inject) hence "\ = ty.Int \ ty.Int : latent_eff.NE" by auto thus ?thesis using prems arr_sub_arr_cases[of ty.Int ty.Int latent_eff.NE] by (auto simp add: ty.inject) qed inductive_cases type_nott_case: "\ \ (BI Nott) : t ; e" lemma nott_eff_ne: "\ \ (App (BI Nott) v) : T1 ; eff1 \ eff1 = eff.NE" proof (ind_cases " \ \ (App (BI Nott) v) : T1 ; eff1") assume "eff1 = eff.NE" thus ?thesis by simp next fix T0 T1 S eff1a e1 e2 U assume "\ \ e1 : U ; eff1a" "App (BI Nott) v = App e1 e2" "\ U <: T0 \ T1 : Latent S" hence "\ \ (BI Nott) : U ; eff1a" by (simp add: trm.inject) hence "\\<^isub>\ Nott = U" using type_nott_case[of \ "U"] by (auto simp add: trm.inject) hence "\ = Top \ BoolTy : latent_eff.NE" by auto thus ?thesis using prems arr_sub_arr_cases[of Top BoolTy latent_eff.NE] by (auto simp add: ty.inject) next fix T0 T1 S eff1a e1 e2 U assume "\ \ e1 : U ; eff1a" "App (BI Nott) v = App e1 e2" "\ U <: T0 \ T1 : Latent S" hence "\ \ (BI Nott) : U ; eff1a" by (simp add: trm.inject) hence "\\<^isub>\ Nott = U" using type_nott_case[of \ "U"] by (auto simp add: trm.inject) hence "\ = Top \ BoolTy : latent_eff.NE" by auto thus ?thesis using prems arr_sub_arr_cases[of Top BoolTy latent_eff.NE] by (auto simp add: ty.inject) next fix T0 T1 S eff1a e1 e2 U assume "\ \ e1 : U ; eff1a" "App (BI Nott) v = App e1 e2" "\ U <: T0 \ T1 : Latent S" hence "\ \ (BI Nott) : U ; eff1a" by (simp add: trm.inject) hence "\\<^isub>\ Nott = U" using type_nott_case[of \ "U"] by (auto simp add: trm.inject) hence "\ = Top \ BoolTy : latent_eff.NE" by auto thus ?thesis using prems arr_sub_arr_cases[of Top BoolTy latent_eff.NE] by (auto simp add: ty.inject) qed inductive_cases type_booleanp_case: "\ \ (BI BooleanP) : t ; e" lemma value_eff: assumes "v : values" and "\ \ v : T ; eff" shows "simple_eff eff" using prems proof (induct v rule :values.induct) case abs_value thus ?case using abs_ty_elim_eff by auto next case num_value thus ?case using num_ty_elim by auto next case (bool_value b) thus ?case using true_ty_elim false_ty_elim by (cases b) auto next case bi_value thus ?case using bi_ty_elim by auto qed lemma booleanp_eff_simple: "\\ \ (App (BI BooleanP) v) : T1 ; eff1 ; v : values\ \ simple_eff eff1" proof (ind_cases " \ \ (App (BI BooleanP) v) : T1 ; eff1") fix T0 T1 S eff1a e1 e2 xa T assume "\ \ e2 : T ; VE xa" "App (BI BooleanP) v = App e1 e2" "v : values" hence "VE xa = eff.NE \ VE xa = eff.TT \ VE xa = eff.FF " using value_eff[of v \ T "VE xa"] by (auto simp add: trm.inject) thus ?thesis using ty.distinct by auto qed (auto) lemma numberp_eff_simple: "\\ \ (App (BI NumberP) v) : T1 ; eff1 ; v : values\ \ simple_eff eff1" proof (ind_cases " \ \ (App (BI NumberP) v) : T1 ; eff1") fix T0 T1 S eff1a e1 e2 xa T assume "\ \ e2 : T ; VE xa" "App (BI NumberP) v = App e1 e2" "v : values" hence "VE xa = eff.NE \ VE xa = eff.TT \ VE xa = eff.FF " using value_eff[of v \ T "VE xa"] by (auto simp add: trm.inject) thus ?thesis using ty.distinct by auto qed (auto) lemma procp_eff_simple: "\\ \ (App (BI ProcP) v) : T1 ; eff1 ; v : values\ \ simple_eff eff1" proof (ind_cases " \ \ (App (BI ProcP) v) : T1 ; eff1") fix T0 T1 S eff1a e1 e2 xa T assume "\ \ e2 : T ; VE xa" "App (BI ProcP) v = App e1 e2" "v : values" hence "VE xa = eff.NE \ VE xa = eff.TT \ VE xa = eff.FF " using value_eff[of v \ T "VE xa"] by (auto simp add: trm.inject) thus ?thesis using ty.distinct by auto qed (auto) inductive_cases app_boolp_ff: "\ \ (App (BI BooleanP) v) : T1 ; FF" lemma booleanp_FF_preserved: assumes "\ \ (App (BI BooleanP) v) : T1 ; FF" and "v : values" and "\ BooleanP v = Some u" shows "u = Bool False" using `v : values` prems proof (induct v rule: values.induct) case (bool_value b) let ?P = "\ \ App (BI BooleanP) (trm.Bool b) : T1 ; FF" have "?P ==> ?case" proof (ind_cases ?P) fix S T e1 e2 T0 eff1 eff2 U assume "App (BI BooleanP) (trm.Bool b) = App e1 e2" "\ \ e1 : U ; eff1 " "\ \ e2 : T ; eff2" "~ (\ T <: S)" "e2 : values" "\ U <: T0 \ T1 : Latent S" hence a:"\ \ (BI BooleanP) : U ; eff1 " using trm.inject by auto from prems have b:"\ \ Bool b : T ; eff2" using trm.inject by auto have "U = Top \ BoolTy : Latent BoolTy" using a bi_ty_elim[of \ BooleanP "U"] by auto hence c:"S = BoolTy" using prems arr_sub_arr_cases[of Top BoolTy _ T0 T1 "Latent S"] latent_eff.inject by auto from b have d:"T = ty.TT \ T = ty.FF" using true_ty_elim false_ty_elim by (cases b) auto from c d have "\ T <: S" by auto thus ?thesis using prems by auto qed thus ?case using bool_value by auto qed (auto) lemma typing_valid: assumes "\ \ e : T ; F" shows "valid \" using prems proof (induct) case (T_Abs a \ T b T' F') thus ?case using valid_elim[of a T \] by auto next case (T_AbsPred a \ T b T' F') thus ?case using valid_elim[of a T \] by auto qed (auto) lemma booleanp_TT_preserved: assumes "\ \ (App (BI BooleanP) v) : T1 ; TT" and "v : values" and "\ BooleanP v = Some u" shows "u = Bool True" proof - note app_ty_tt_elim[of \ "(BI BooleanP)" v T1] then obtain A1 U T0 T1 S eff1 eff2 where A:"\ \ (BI BooleanP) : U ; eff1" "\ U <: A1 \ T1 : Latent S" "\ \ v : T0 ; eff2" "\ T0 <: A1" "\ T0 <: S" using prems by auto hence B:"U = Top \ BoolTy : Latent BoolTy " using bi_ty_elim[of \ BooleanP U] by auto hence C:"\ T0 <: BoolTy" using prems arr_sub_arr_cases[of Top BoolTy "Latent BoolTy" _ _ "Latent S"] latent_eff.inject A by auto then obtain b where D:"v = Bool b" using A bool_value[of v \ T0] prems by auto thus ?thesis using prems by auto qed lemma booleanp_soundness_eff: assumes "\ \ App (BI BooleanP) v : T ; F" and "v : values" and "\ BooleanP v = Some u" and "\ \ u : T' ; F'" shows "\ F' T' F'] booleanp_FF_preserved by auto next case TT thus ?case using true_ty_elim[of \ T' F'] booleanp_TT_preserved by auto qed qed inductive_cases app_nump_ff: "\ \ (App (BI NumberP) v) : T1 ; FF" thm app_nump_ff lemma numberp_FF_preserved: assumes "\ \ (App (BI NumberP) v) : T1 ; FF" and "v : values" and "\ NumberP v = Some u" shows "u = Bool False" using `v : values` prems proof (induct v rule: values.induct) case (bool_value b) thus ?case by (cases b) auto next case (num_value b) let ?P = "\ \ App (BI NumberP) (trm.Num b) : T1 ; FF" have "?P ==> ?case" proof (ind_cases ?P) fix S T e1 e2 T0 eff1 eff2 U assume "App (BI NumberP) (trm.Num b) = App e1 e2" "\ \ e1 : U ; eff1 " "\ \ e2 : T ; eff2" "~ (\ T <: S)" "e2 : values" "\ U <: T0 \ T1 : Latent S" hence a:"\ \ (BI NumberP) : U ; eff1 " using trm.inject by auto from prems have b:"\ \ Num b : T ; eff2" using trm.inject by auto have "U = Top \ BoolTy : Latent ty.Int" using a bi_ty_elim[of \ NumberP "U"] by auto hence c:"S = ty.Int" using prems arr_sub_arr_cases[of Top _ _ T0 T1 "Latent S"] latent_eff.inject by auto from b have d:"T = ty.Int" using num_ty_elim by auto from c d have "\ T <: S" by auto thus ?thesis using prems by auto qed thus ?case using num_value by auto qed (auto) lemma numberp_TT_preserved: assumes "\ \ (App (BI NumberP) v) : T1 ; TT" and "v : values" and "\ NumberP v = Some u" shows "u = Bool True" proof - note app_ty_tt_elim[of \ "(BI NumberP)" v T1] then obtain A1 U T0 T1 S eff1 eff2 where A:"\ \ (BI NumberP) : U ; eff1" "\ U <: A1 \ T1 : Latent S" "\ \ v : T0 ; eff2" "\ T0 <: A1" "\ T0 <: S" using prems by auto hence B:"U = Top \ BoolTy : Latent ty.Int " using bi_ty_elim[of \ NumberP U] by auto hence C:"\ T0 <: ty.Int" using prems arr_sub_arr_cases[of Top BoolTy "Latent ty.Int" _ _ "Latent S"] latent_eff.inject A by auto then obtain b where D:"v = Num b" using A int_value[of v \ T0] prems by auto thus ?thesis using prems by auto qed lemma numberp_soundness_eff: assumes "\ \ App (BI NumberP) v : T ; F" and "v : values" and "\ NumberP v = Some u" and "\ \ u : T' ; F'" shows "\ F' T' F'] numberp_FF_preserved by auto next case TT thus ?case using true_ty_elim[of \ T' F'] numberp_TT_preserved by auto qed qed lemma empty_un_bot: fixes T :: ty shows "\ Union [] <: T" by auto lemma all_fun_ty_below: fixes S T :: ty shows "\ S \ T : F <: (Union []) \ Top : latent_eff.NE" by (rule S_Fun) auto inductive_cases below_latent_ne_cases: "\ S \ T : F <: S' \ T' : latent_eff.NE" thm below_latent_ne_cases inductive_cases app_procp_ff: "\ \ (App (BI ProcP) v) : T1 ; FF" thm app_nump_ff thm app_procp_ff lemma procp_FF_preserved: assumes "\ \ (App (BI ProcP) v) : T1 ; FF" and "v : values" and "\ ProcP v = Some u" shows "u = Bool False" using `v : values` prems proof (nominal_induct v avoiding: \ rule: values.strong_induct) case (bool_value b) thus ?case by (cases b) auto next case (num_value b) thus ?case by auto next case (abs_value x t b) let ?P = "\ \ App (BI ProcP) (Lam[x:t].b) : T1 ; FF" have "?P ==> ?case" proof (ind_cases ?P) fix e1 U eff1 T0 S e2 T eff2 assume "App (BI ProcP) (Lam [x:t].b) = App e1 e2 "" \ \ e1 : U ; eff1 "" \ U <: T0 \ T1 : Latent S " "\ \ e2 : T ; eff2 "" \ T <: T0 "" \ \ T <: S "" e2 \ values "" closed e2" hence a:"\ \ (BI ProcP) : U ; eff1 " using trm.inject by auto from prems have b:"\ \ Lam[x:t].b : T ; eff2" using trm.inject by auto have "U = Top \ BoolTy : Latent (Union [] \ Top : latent_eff.NE)" using a bi_ty_elim[of \ ProcP "U"] by auto hence c:"S = Union [] \ Top : latent_eff.NE" using prems arr_sub_arr_cases[of Top _ _ T0 T1 "Latent S"] latent_eff.inject by auto have "EX A1 A2 L. T = A1 \ A2 : L" using abs_ty_elim[OF b `x \ \`] by auto then obtain A1 A2 L where d:"T = A1 \ A2 : L" by auto from c d have "\ T <: S" using all_fun_ty_below by auto thus ?thesis using prems by auto qed thus ?case using abs_value by auto next case (bi_value c) let ?P = "\ \ App (BI ProcP) (BI c) : T1 ; FF" have "?P ==> ?case" proof (ind_cases ?P) fix e1 U eff1 T0 S e2 T eff2 assume "App (BI ProcP) (BI c) = App e1 e2 "" \ \ e1 : U ; eff1 "" \ U <: T0 \ T1 : Latent S " "\ \ e2 : T ; eff2 "" \ T <: T0 "" \ \ T <: S "" e2 \ values "" closed e2" hence a:"\ \ (BI ProcP) : U ; eff1 " using trm.inject by auto from prems have b:"\ \ (BI c) : T ; eff2" using trm.inject by auto have "U = Top \ BoolTy : Latent (Union [] \ Top : latent_eff.NE)" using a bi_ty_elim[of \ ProcP "U"] by auto hence c:"S = Union [] \ Top : latent_eff.NE" using prems arr_sub_arr_cases[of Top _ _ T0 T1 "Latent S"] latent_eff.inject by auto have b':"T = \\<^isub>\ c" using bi_ty_elim[OF b] by auto hence "EX A1 A2 FA. T = A1 \ A2 : FA" by (nominal_induct c rule: builtin.induct) auto then obtain A1 A2 F where d:"T = A1 \ A2 : F" by auto hence "\ T <: S" using c d all_fun_ty_below by auto thus ?thesis using prems by auto qed thus ?case using bi_value by auto qed lemma proc_value: assumes "\ \ v : T ; F" and "v : values" and "\ T <: (A1 \ A2 : latent_eff.NE)" shows "EX x b t. v = Lam[x:t].b \ (EX c. v = BI c)" using `v : values` prems proof (nominal_induct v avoiding: \ rule: values.strong_induct) case abs_value thus ?case by auto next case (bool_value b) hence "T = ty.TT \ T = ty.FF" using bool_ty_elim by auto thus ?case using sub_arr_cases[of T A1 A2 latent_eff.NE] using bool_value by auto next case (num_value b) hence "T = ty.Int" using num_ty_elim by auto thus ?case using sub_arr_cases[of T A1 A2 latent_eff.NE] using num_value by auto next case (bi_value c) thus ?case by auto qed lemma procp_TT_preserved: assumes "\ \ (App (BI ProcP) v) : T1 ; TT" and "v : values" and "\ ProcP v = Some u" shows "u = Bool True" proof - note app_ty_tt_elim[of \ "(BI ProcP)" v T1] then obtain A1 U T0 T1 S eff1 eff2 where A:"\ \ (BI ProcP) : U ; eff1" "\ U <: A1 \ T1 : Latent S" "\ \ v : T0 ; eff2" "\ T0 <: A1" "\ T0 <: S" using prems by auto hence B:"U = Top \ BoolTy : Latent (Union [] \ Top : latent_eff.NE) " using bi_ty_elim[of \ ProcP U] by auto hence C:"\ T0 <: (Union [] \ Top : latent_eff.NE)" using prems arr_sub_arr_cases[of Top BoolTy "Latent (Union [] \ Top : latent_eff.NE)" _ _ "Latent S"] latent_eff.inject A by auto moreover { assume D:"EX x b t. v = Lam[x:t].b" then obtain x b t where "v = Lam[x:t].b" by auto hence ?thesis using prems by auto } moreover { assume "EX c. v = BI c" then obtain c where "v = BI c" by auto hence ?thesis using prems by (nominal_induct c rule: builtin.induct) auto } ultimately show ?thesis using prems proc_value[of \ v T0 eff2 "Union []" Top] by auto qed lemma procp_soundness_eff: assumes "\ \ App (BI ProcP) v : T ; F" and "v : values" and "\ ProcP v = Some u" and "\ \ u : T' ; F'" shows "\ F' T' F'] procp_FF_preserved by auto next case TT thus ?case using true_ty_elim[of \ T' F'] procp_TT_preserved by auto qed qed text {* soundness of the \ rule *} lemma bool_sub_boolty[simp]: "\ ty.FF <: BoolTy" "\ ty.TT <: BoolTy" by auto lemma delta_soundness: assumes "\\<^isub>\ b = (T0 \ T1 : le)" and "v : values" and "\ \ v : T ; eff1" and "\ T <: T0" and "\ \ (App (BI b) v) : T1' ; eff" and "\ T1 <: T1'" and "\ b v = Some u" and "valid \" shows "EX eff' T1'. \ \ u : T1' ; eff' \ \ eff' \ T1' <: T1" using prems proof (nominal_induct b rule: builtin.induct) case Add1 hence a:"eff = NE" using add1_eff_ne[of \ v T1' eff] by auto have "EX eff'. \ \ u : T1 ; eff'" using `v : values` `valid \` Add1 by (induct v rule: values.induct) (auto simp add: ty.inject) then obtain eff' where b:"\ \ u : T1 ; eff'" by auto have "simple_eff eff'" using delta_closed[of Add1 v u] closed_eff b Add1 by auto hence c:"\ eff' v T1' eff] by auto have "EX eff' T1'. \ \ u : T1' ; eff' \ \ T1' <: T1" using `v : values` `valid \` Nott proof (induct v rule: values.induct) case (bool_value b) thus ?case using bool_value bool_sub_boolty by (cases b) auto next case num_value thus ?case using bool_sub_boolty by auto next case bi_value thus ?case using bool_sub_boolty by auto next case abs_value thus ?case using bool_sub_boolty by auto qed then obtain eff' T1' where b:"\ \ u : T1' ; eff'" and b':"\ T1' <: T1" by auto have "simple_eff eff'" using delta_closed[of Nott v u] closed_eff b Nott by auto hence c:"\ eff' " using typing_valid prems by auto have "T1 = BoolTy" using BooleanP by (simp add: ty.inject) then obtain bb where veq:"\ BooleanP v = Some (Bool bb)" by (nominal_induct v rule: trm.induct) (auto) hence "EX T1' eff'. \ \ u : T1' ; eff' \ \ T1' <: T1" using `T1 = BoolTy` BooleanP bool_sub_boolty proof (cases bb) case True hence "u = Bool True" using veq BooleanP by auto hence "\ \ u : ty.TT; TT" using `valid \` by auto thus ?thesis using `T1 = BoolTy` bool_sub_boolty by auto next case False hence "u = Bool False" using veq BooleanP by auto hence "\ \ u : ty.FF; FF" using `valid \` by auto thus ?thesis using `T1 = BoolTy` bool_sub_boolty by auto qed then obtain T1a eff' where a:"\ \ u : T1a ; eff'" and a':"\ T1a <: T1" by auto have c:"simple_eff eff'" using delta_closed[of BooleanP v u] closed_eff prems by auto have b:"simple_eff eff" using BooleanP booleanp_eff_simple by auto hence "\ eff' \ App (BI BooleanP) v : T1' ; eff` `\ BooleanP v = Some u` by auto hence "eff'= FF" using a false_ty_elim by auto thus ?case using FF by auto next case TT hence "u = Bool True" using booleanp_TT_preserved `v : values` `\ \ App (BI BooleanP) v : T1' ; eff` `\ BooleanP v = Some u` by auto hence "eff'= TT" using a true_ty_elim by auto thus ?case using TT by auto qed thus ?case using a a' by auto next case NumberP have "valid \" using typing_valid prems by auto have "T1 = BoolTy" using NumberP by (simp add: ty.inject) then obtain bb where veq:"\ NumberP v = Some (Bool bb)" by (nominal_induct v rule: trm.induct) (auto) hence "EX T1' eff'. \ \ u : T1' ; eff' \ \ T1' <: T1" using `T1 = BoolTy` NumberP bool_sub_boolty proof (cases bb) case True hence "u = Bool True" using veq NumberP by auto hence "\ \ u : ty.TT; TT" using `valid \` by auto thus ?thesis using `T1 = BoolTy` bool_sub_boolty by auto next case False hence "u = Bool False" using veq NumberP by auto hence "\ \ u : ty.FF; FF" using `valid \` by auto thus ?thesis using `T1 = BoolTy` bool_sub_boolty by auto qed then obtain T1a eff' where a:"\ \ u : T1a ; eff'" and a':"\ T1a <: T1" by auto have c:"simple_eff eff'" using delta_closed[of NumberP v u] closed_eff prems by auto have b:"simple_eff eff" using NumberP numberp_eff_simple by auto hence "\ eff' \ App (BI NumberP) v : T1' ; eff` `\ NumberP v = Some u` by auto hence "eff'= FF" using a false_ty_elim by auto thus ?case using FF by auto next case TT hence "u = Bool True" using numberp_TT_preserved `v : values` `\ \ App (BI NumberP) v : T1' ; eff` `\ NumberP v = Some u` by auto hence "eff'= TT" using a true_ty_elim by auto thus ?case using TT by auto qed thus ?case using a a' by auto next case ProcP have "valid \" using typing_valid prems by auto have "T1 = BoolTy" using ProcP by (simp add: ty.inject) then obtain bb where veq:"\ ProcP v = Some (Bool bb)" by (nominal_induct v rule: trm.induct) (auto) hence "EX T1' eff'. \ \ u : T1' ; eff' \ \ T1' <: T1" using `T1 = BoolTy` ProcP bool_sub_boolty proof (cases bb) case True hence "u = Bool True" using veq ProcP by auto hence "\ \ u : ty.TT; TT" using `valid \` by auto thus ?thesis using `T1 = BoolTy` bool_sub_boolty by auto next case False hence "u = Bool False" using veq ProcP by auto hence "\ \ u : ty.FF; FF" using `valid \` by auto thus ?thesis using `T1 = BoolTy` bool_sub_boolty by auto qed then obtain T1a eff' where a:"\ \ u : T1a ; eff'" and a':"\ T1a <: T1" by auto have c:"simple_eff eff'" using delta_closed[of ProcP v u] closed_eff prems by auto have b:"simple_eff eff" using ProcP procp_eff_simple by auto hence "\ eff' \ App (BI ProcP) v : T1' ; eff` `\ ProcP v = Some u` by auto hence "eff'= FF" using a false_ty_elim by auto thus ?case using FF by auto next case TT hence "u = Bool True" using procp_TT_preserved `v : values` `\ \ App (BI ProcP) v : T1' ; eff` `\ ProcP v = Some u` by auto hence "eff'= TT" using a true_ty_elim by auto thus ?case using TT by auto qed thus ?case using a a' by auto qed lemma simple_eff_below_ve: assumes "simple_eff F" shows "\ F F F F = VE x" using prems by induct auto consts remove_env :: "'a list => 'a => 'a list" ("_ - _" [100,100] 100) primrec "[] - x = []" "(y#xs) - x = (if x=y then (xs - x) else y#(xs - x))" lemma fresh_remove: fixes a::"name" and \::"(name\ty) list" assumes a: "a\\" shows "a\(\ - (x,T))" using a by (induct \) (auto simp add: fresh_list_cons) lemma valid_remove: fixes pair::"name\ty" assumes a: "valid \" shows "valid (\ - (x,T))" using a by (induct \) (auto simp add: fresh_remove) lemma set_remove: assumes a: "(a,T)\set \" and b: "a\x" shows "(a,T)\set (\ - (x,T'))" using a b by (induct \) (auto) lemma closed_elim:"closed e \ (supp e = ({}::name set))" using closed_def by auto lemma set_remove_comm: shows "set (l - a) = (set l) - {a}" by (induct l) auto lemma envplus_set: shows "set (\ |+ TE T x) = (mapfun restrict T x) ` set \" proof - have A:"!! a b. a = b \ set a = set b" by auto have "\ |+ TE T x = map (mapfun restrict T x) \" by auto hence "set (\ |+ TE T x) = set (map (mapfun restrict T x) \)" using A[of "(\ |+ TE T x)" "map (mapfun restrict T x) \"] by auto also have "\ = (mapfun restrict T x) ` set \" by auto ultimately show ?thesis by auto qed lemma envminus_set: shows "set (\ |- TE T x) = (mapfun remove T x) ` set \" proof - have A:"!! a b. a = b \ set a = set b" by auto have "\ |- TE T x = map (mapfun remove T x) \" by auto hence "set (\ |- TE T x) = set (map (mapfun remove T x) \)" using A[of "(\ |- TE T x)" "map (mapfun remove T x) \"] by auto also have "\ = (mapfun remove T x) ` set \" by auto ultimately show ?thesis by auto qed lemma envplus_set_ve: shows "set (\ |+ VE x) = (mapfun remove ty.FF x) ` set \" proof - have A:"!! a b. a = b \ set a = set b" by auto have "\ |+ VE x = map (mapfun remove ty.FF x) \" by auto hence "set (\ |+ VE x) = set (map (mapfun remove ty.FF x) \)" using A[of "(\ |+ VE x)" "map (mapfun remove ty.FF x) \"] by auto also have "\ = (mapfun remove ty.FF x) ` set \" by auto ultimately show ?thesis by auto qed lemma envminus_set_ve: shows "set (\ |- VE x) = (mapfun replace ty.FF x) ` set \" proof - have A:"!! a b. a = b \ set a = set b" by auto have "\ |- VE x = map (mapfun replace ty.FF x) \" by auto hence "set (\ |- VE x) = set (map (mapfun replace ty.FF x) \)" using A[of "(\ |- VE x)" "map (mapfun replace ty.FF x) \"] by auto also have "\ = (mapfun replace ty.FF x) ` set \" by auto ultimately show ?thesis by auto qed lemma fresh_weakening: assumes a:"x\e" and b:"\ \ e : T ; F" and c: "valid \" shows "(\ - (x,T')) \ e : T ; F" using b a c proof (nominal_induct \ e T F avoiding: x T' rule: typing.strong_induct) case T_Var thus ?case by(force simp add: fresh_atm abs_fresh set_remove valid_remove fresh_remove)+ next case (T_App \' _ _ t1 t2) thus ?case by(force simp add: fresh_atm abs_fresh set_remove valid_remove fresh_remove) next case T_Abs thus ?case by(force simp add: fresh_atm abs_fresh set_remove valid_remove fresh_remove)+ next case T_AbsPred thus ?case by(force simp add: fresh_atm abs_fresh set_remove valid_remove fresh_remove)+ next case T_AppPred thus ?case by(force simp add: fresh_atm abs_fresh set_remove valid_remove fresh_remove)+ next case T_IfTrue thus ?case by(force simp add: fresh_atm abs_fresh set_remove valid_remove fresh_remove)+ next case T_IfFalse thus ?case by(force simp add: fresh_atm abs_fresh set_remove valid_remove fresh_remove)+ next case T_True thus ?case by(force simp add: fresh_atm abs_fresh set_remove valid_remove fresh_remove)+ next case T_False thus ?case by(force simp add: fresh_atm abs_fresh set_remove valid_remove fresh_remove)+ next case T_Num thus ?case by(force simp add: fresh_atm abs_fresh set_remove valid_remove fresh_remove)+ next case T_Const thus ?case by(force simp add: fresh_atm abs_fresh set_remove valid_remove fresh_remove)+ next case (T_AppPredTrue \' e1 U F1 T0 T1 S e2 T F2 x T') have A:"x \ e1" "x \ e2" using T_AppPredTrue by auto hence "\' - (x,T') \ e1 : U; F1" using T_AppPredTrue by auto also have "\' - (x,T') \ e2 : T ; F2" using T_AppPredTrue A by auto ultimately show ?case using T_AppPredTrue(3) `\ T <: T0` `\ T <: S` by auto next case (T_AppPredFalse \' e1 U F1 T0 T1 S e2 T F2 x T') have A:"x \ e1" "x \ e2" using T_AppPredFalse by auto hence "\' - (x,T') \ e1 : U ; F1" using T_AppPredFalse by auto also have "\' - (x,T') \ e2 : T ; F2" using T_AppPredFalse A by auto ultimately show ?case using `~ (\ T <: S)` `\ T <: T0` `e2 : values` `closed e2` T_AppPredFalse(3) by auto next case (T_If \' e1 T1 F1 e2 T2 F2 e3 T3 F3 T x) have A:"x \ e1" "x \ e2" "x \ e3" using T_If by auto have "\' - (x,T') \ e1 : T1 ; F1" using T_If A by auto thus ?case using T_If proof (nominal_induct "F1" rule: eff.induct) case NE from NE have 1:"\' - (x, T') \ e1 : T1 ; eff.NE" by auto from NE have 2:"(\' - (x, T') |+ eff.NE) \ e2 : T2 ; F2" by auto from NE have 3:"(\' - (x, T') |- eff.NE) \ e3 : T3 ; F3" by auto from 1 2 3 show ?case using `\ T2 <: T` `\ T3 <: T` .. next case TT from TT have 1:"\' - (x, T') \ e1 : T1 ; eff.TT" by auto from TT have 2:"(\' - (x, T') |+ eff.TT) \ e2 : T2 ; F2" by auto from 1 2 show ?case using `\ T2 <: T` by auto next case FF from FF have 1:"\' - (x, T') \ e1 : T1 ; eff.FF" by auto from FF have 3:"(\' - (x, T') |+ eff.FF) \ e3 : T3 ; F3" by auto from 1 3 show ?case using `\ T3 <: T` by auto next case (VE z) from VE have 1:"\' - (x, T') \ e1 : T1 ; VE z" by auto have val1:"valid (\' |+ VE z)" using VE envplus_valid[of \' "VE z"] by auto have val2:"valid (\' |- VE z)" using VE envminus_valid[of \' "VE z"] by auto have "valid (\' |- VE z)" using VE envminus_valid[of \' "VE z"] by auto have A0:"!!T0 . (\' |- VE z) - (x, T0) \ e3 : T3 ; F3" using VE(7) A `valid (\' |- VE z)` by auto have A:"!!T0 . (\' |+ VE z) - (x, T0) \ e2 : T2 ; F2" using VE(5) A `valid (\' |+ VE z)` by auto let ?op = "replace" let ?mapfun = "(% (v,ty). (if (x = v) then (v,?op ty.FF ty) else (v,ty)))" have B:"!! p. set ((\' |+ VE z) - p) = ((mapfun remove ty.FF z) ` (set \')) - {p}" using envplus_set_ve set_remove_comm[of "(\' |+ VE z)"] by auto have image_lem:"!! f S v. (f ` S) - {(f v)} <= (f ` (S - {v}))" by auto note image_lem[of "mapfun remove ty.FF z" "set \'" "(x,T0)"] have eq1:"!! p. mapfun remove ty.FF z ` set \' - {mapfun remove ty.FF z p} = set ((\' |+ VE z) - (mapfun remove ty.FF z p))" using envplus_set_ve set_remove_comm[of "(\' |+ VE z)"] by auto have eq2:"!! p. mapfun remove ty.FF z ` (set \' - {p}) = set (\' - p |+ VE z)" proof - fix p show "mapfun remove ty.FF z ` (set \' - {p}) = set (\' - p |+ VE z)" using envplus_set_ve[of _ "\' - p"] set_remove_comm[of \'] by auto qed have eq3:"!! x T0. mapfun remove ty.FF z (x,T0) = (x, (if (x = z) then (remove ty.FF T0) else (T0)))" by auto let ?removeT' = "(if (x = z) then (remove ty.FF T') else (T'))" have goal:"((\' |+ VE z) - (x,?removeT')) \ ((\' - (x,T')) |+ VE z)" proof - have " mapfun remove ty.FF z ` set \' - {mapfun remove ty.FF z (x,T')} <= mapfun remove ty.FF z ` (set \' - {(x,T')})" using image_lem[of "mapfun remove ty.FF z" "set \'" "(x,T')"] by auto hence " mapfun remove ty.FF z ` set \' - {mapfun remove ty.FF z (x,T')} <= set ((\' - ((x,T'))) |+ VE z)" using eq2[of " (x, T')"] by auto hence "set ((\' |+ VE z) - (mapfun remove ty.FF z (x,T'))) <= set ((\' - ((x,T'))) |+ VE z)" using eq1[of "(x,T')"] by auto hence "set ((\' |+ VE z) - (x,?removeT')) <= set ((\' - (x,T')) |+ VE z)" using eq3 by auto thus ?thesis by auto qed have val3:"valid ((\' |+ VE z) - (x,?removeT'))" using val1 valid_remove by auto have "valid ((\' - (x, T')))" using `valid \'` valid_remove envplus_valid by auto hence val4:"valid ((\' - (x, T')) |+ VE z)" using envplus_valid[of "\' - (x, T')" "VE z"] by auto from A have "(\' |+ VE z) - (x,?removeT') \ e2 : T2 ; F2" by auto hence 2:"(\' - (x, T')) |+ VE z \ e2 : T2 ; F2" using goal val3 val4 weakening[of "(\' |+ VE z) - (x,?removeT')" e2 T2 F2 "\' - (x,T') |+ VE z"] by auto have eq4:"!! p. mapfun replace ty.FF z ` set \' - {mapfun replace ty.FF z p} = set ((\' |- VE z) - (mapfun replace ty.FF z p))" using envminus_set_ve[of _ \'] set_remove_comm[of "(\' |- VE z)"] by auto have eq5:"!! p. mapfun replace ty.FF z ` (set \' - {p}) = set (\' - p |- VE z)" proof - fix p show "mapfun replace ty.FF z ` (set \' - {p}) = set (\' - p |- VE z)" using envminus_set_ve[of _ "\' - p" ] set_remove_comm[of \'] by auto qed have eq6:"!! x T0. mapfun replace ty.FF z (x,T0) = (x, (if (x = z) then (replace ty.FF T0) else (T0)))" by auto let ?replaceT' = "(if (x = z) then (replace ty.FF T') else (T'))" have goal':"((\' |- VE z) - (x,?replaceT')) \ ((\' - (x,T')) |- VE z)" proof - have " mapfun replace ty.FF z ` set \' - {mapfun replace ty.FF z (x,T')} <= mapfun replace ty.FF z ` (set \' - {(x,T')})" using image_lem[of "mapfun replace ty.FF z" "set \'" "(x,T')"] by auto hence " mapfun replace ty.FF z ` set \' - {mapfun replace ty.FF z (x,T')} <= set ((\' - ((x,T'))) |- VE z)" using eq5[of " (x, T')"] by auto hence "set ((\' |- VE z) - (mapfun replace ty.FF z (x,T'))) <= set ((\' - ((x,T'))) |- VE z)" using eq4[of "(x,T')"] by auto hence "set ((\' |- VE z) - (x,?replaceT')) <= set ((\' - (x,T')) |- VE z)" using eq6 by auto thus ?thesis by auto qed have val5:"valid ((\' |- VE z) - (x,?replaceT'))" using val2 valid_remove by auto have "valid ((\' - (x, T')))" using `valid \'` valid_remove envminus_valid by auto hence val6:"valid ((\' - (x, T')) |- VE z)" using envminus_valid[of "\' - (x, T')" "VE z"] by auto from A0 have "(\' |- VE z) - (x,?replaceT') \ e3 : T3 ; F3" by auto hence 3:"(\' - (x, T')) |- VE z \ e3 : T3 ; F3" using goal' val5 val6 weakening[of "(\' |- VE z) - (x,?replaceT')" e3 T3 F3 "\' - (x,T') |- VE z"] by auto from 1 2 3 show ?case using `\ T2 <: T` `\ T3 <: T` .. next case (TE U z) from TE have 1:"\' - (x, T') \ e1 : T1 ; TE U z" by auto have val1:"valid (\' |+ TE U z)" using TE envplus_valid[of \' "TE U z"] by auto have val2:"valid (\' |- TE U z)" using TE envminus_valid[of \' "TE U z"] by auto have "valid (\' |- TE U z)" using TE envminus_valid[of \' "TE U z"] by auto have A0:"!!T0 . (\' |- TE U z) - (x, T0) \ e3 : T3 ; F3" using TE(7) A `valid (\' |- TE U z)` by auto have A:"!!T0 . (\' |+ TE U z) - (x, T0) \ e2 : T2 ; F2" using TE(5) A `valid (\' |+ TE U z)` by auto let ?op = "remove" let ?mapfun = "(% (v,ty). (if (x = v) then (v,?op S ty) else (v,ty)))" have B:"!! p. set ((\' |+ TE U z) - p) = ((mapfun restrict U z) ` (set \')) - {p}" using envplus_set set_remove_comm[of "(\' |+ TE U z)"] by auto have image_lem:"!! f S v. (f ` S) - {(f v)} <= (f ` (S - {v}))" by auto note image_lem[of "mapfun restrict U z" "set \'" "(x,T0)"] have eq1:"!! p. mapfun restrict U z ` set \' - {mapfun restrict U z p} = set ((\' |+ TE U z) - (mapfun restrict U z p))" using envplus_set set_remove_comm[of "(\' |+ TE U z)"] by auto have eq2:"!! p. mapfun restrict U z ` (set \' - {p}) = set (\' - p |+ TE U z)" proof - fix p show "mapfun restrict U z ` (set \' - {p}) = set (\' - p |+ TE U z)" using envplus_set[of _ _ "\' - p"] set_remove_comm[of \'] by auto qed have eq3:"!! x T0. mapfun restrict U z (x,T0) = (x, (if (x = z) then (restrict U T0) else (T0)))" by auto let ?restrictT' = "(if (x = z) then (restrict U T') else (T'))" have goal:"((\' |+ TE U z) - (x,?restrictT')) \ ((\' - (x,T')) |+ TE U z)" proof - have " mapfun restrict U z ` set \' - {mapfun restrict U z (x,T')} <= mapfun restrict U z ` (set \' - {(x,T')})" using image_lem[of "mapfun restrict U z" "set \'" "(x,T')"] by auto hence " mapfun restrict U z ` set \' - {mapfun restrict U z (x,T')} <= set ((\' - ((x,T'))) |+ TE U z)" using eq2[of " (x, T')"] by auto hence "set ((\' |+ TE U z) - (mapfun restrict U z (x,T'))) <= set ((\' - ((x,T'))) |+ TE U z)" using eq1[of "(x,T')"] by auto hence "set ((\' |+ TE U z) - (x,?restrictT')) <= set ((\' - (x,T')) |+ TE U z)" using eq3 by auto thus ?thesis by auto qed have val3:"valid ((\' |+ TE U z) - (x,?restrictT'))" using val1 valid_remove by auto have "valid ((\' - (x, T')))" using `valid \'` valid_remove envplus_valid by auto hence val4:"valid ((\' - (x, T')) |+ TE U z)" using envplus_valid[of "\' - (x, T')" "TE U z"] by auto from A have "(\' |+ TE U z) - (x,?restrictT') \ e2 : T2 ; F2" by auto hence 2:"(\' - (x, T')) |+ TE U z \ e2 : T2 ; F2" using goal val3 val4 weakening[of "(\' |+ TE U z) - (x,?restrictT')" e2 T2 F2 "\' - (x,T') |+ TE U z"] by auto have eq4:"!! p. mapfun remove U z ` set \' - {mapfun remove U z p} = set ((\' |- TE U z) - (mapfun remove U z p))" using envminus_set[of _ _ \'] set_remove_comm[of "(\' |- TE U z)"] by auto have eq5:"!! p. mapfun remove U z ` (set \' - {p}) = set (\' - p |- TE U z)" proof - fix p show "mapfun remove U z ` (set \' - {p}) = set (\' - p |- TE U z)" using envminus_set[of _ _ "\' - p" ] set_remove_comm[of \'] by auto qed have eq6:"!! x T0. mapfun remove U z (x,T0) = (x, (if (x = z) then (remove U T0) else (T0)))" by auto let ?removeT' = "(if (x = z) then (remove U T') else (T'))" have goal':"((\' |- TE U z) - (x,?removeT')) \ ((\' - (x,T')) |- TE U z)" proof - have " mapfun remove U z ` set \' - {mapfun remove U z (x,T')} <= mapfun remove U z ` (set \' - {(x,T')})" using image_lem[of "mapfun remove U z" "set \'" "(x,T')"] by auto hence " mapfun remove U z ` set \' - {mapfun remove U z (x,T')} <= set ((\' - ((x,T'))) |- TE U z)" using eq5[of " (x, T')"] by auto hence "set ((\' |- TE U z) - (mapfun remove U z (x,T'))) <= set ((\' - ((x,T'))) |- TE U z)" using eq4[of "(x,T')"] by auto hence "set ((\' |- TE U z) - (x,?removeT')) <= set ((\' - (x,T')) |- TE U z)" using eq6 by auto thus ?thesis by auto qed have val5:"valid ((\' |- TE U z) - (x,?removeT'))" using val2 valid_remove by auto have "valid ((\' - (x, T')))" using `valid \'` valid_remove envminus_valid by auto hence val6:"valid ((\' - (x, T')) |- TE U z)" using envminus_valid[of "\' - (x, T')" "TE U z"] by auto from A0 have "(\' |- TE U z) - (x,?removeT') \ e3 : T3 ; F3" by auto hence 3:"(\' - (x, T')) |- TE U z \ e3 : T3 ; F3" using goal' val5 val6 weakening[of "(\' |- TE U z) - (x,?removeT')" e3 T3 F3 "\' - (x,T') |- TE U z"] by auto from 1 2 3 show ?case using `\ T2 <: T` `\ T3 <: T` .. qed qed lemma fresh_weakening_cons: assumes "valid ((a,S)#\)" (is "valid ?\") and "(a,S)# \ \ e : T ; F" and "a \ e" shows "\ \ e : T ; F" proof - have v1:"valid \" using prems valid_elim by blast hence v2:"valid (\ - (a,S))" using valid_remove by auto have A:"?\ - (a,S) \ e : T ; F" using prems fresh_weakening[of a e ?\ T F S] by auto have "?\ - (a,S) = \ - (a,S)" by auto hence B:"\ - (a,S) \ \" by (induct \) auto thus ?thesis using A weakening[of _ e T F \] v1 v2 by auto qed lemma closed_empty_env: assumes "closed e" and "\ \ e : T ; F" and "valid \" shows "[] \ e : T ; F" using `valid \` prems proof (induct \ rule: valid.induct) case v1 thus ?case by simp next case (v2 \' a S) have "a \ e" using `closed e` closed_def fresh_def[of a e] by auto thus ?case using v2 fresh_weakening_cons by auto qed lemma closed_any_env: assumes "closed e" and "\ \ e : T ; F" and val1:"valid \" and val2:"valid \'" shows "\' \ e : T ; F" using prems closed_empty_env weakening proof - have A:"[] \ e : T ; F" using prems closed_empty_env by auto note weakening have B:"[] \ \'" by auto from A B val1 val2 have "\' \ e : T ; F" using weakening by blast thus ?thesis by simp qed inductive_cases ve_ty_elim: "\ \ e : T ; VE x" lemma te_ty_elim: "\ \ t1 : T ; TE U z \ EX f A A1 Fn S B. t1 = (App f (Var z)) \ \ \ f : B ; Fn \ \ B <: A1 \ T : Latent U \ \ \ (Var z) : A ; VE z \ \ A <: A1 " proof (ind_cases "\ \ t1 : T ; TE U z") fix e1 T0 eff1 e2 Ta x S B assume "t1 = App e1 e2" "TE U z = TE S x" "\ \ e1 : B ; eff1 "" \ \ e2 : Ta ; VE x " "\ B <: T0 \ T : Latent S" "\ Ta <: T0" from prems have A:"e2 = Var x" using ve_ty_elim[of \ e2 Ta x] eff.inject by auto hence B:"t1 = App e1 (Var z)" using prems trm.inject eff.inject by auto have C:" \ \ (Var z) : Ta ; VE z" using prems A trm.inject eff.inject by auto have D:" \ \ e1 : B ; eff1" using ty.inject latent_eff.inject prems eff.inject by auto have E:"\ B <: T0 \ T : Latent U" using ty.inject latent_eff.inject prems eff.inject by auto from `\ Ta <: T0` B C D E show ?thesis by blast qed lemma unique_var_typing: assumes "(x,T)#\ \ Var x : T; VE x" and "(x,T)#\ \ Var x : T' ; VE x" shows "T = T'" proof (rule ccontr) assume "T ~= T'" have "(x,T) : set ((x,T)#\)" using var_ty_elim[of _ x T "VE x"] prems by auto have "(x,T') : set ((x,T)#\)" "valid ((x,T)#\)" using var_ty_elim[of "((x,T)#\)" x T' "VE x"] prems by auto hence A:"(x,T') : set \" "valid \" "x \ \" using prems valid_elim[of x T \] by auto have "x : supp \" using `valid \` A proof (induct \ rule: valid.induct) case v1 thus ?case by auto next case (v2 \' a S) hence "x \ (a,S)" "x \ \'" using fresh_list_cons by auto hence "x \ a" by auto hence "x ~= a" using fresh_atm by auto hence "(x,T') : set \'" using v2 by auto have "valid \'" using v2 valid_elim[of a S \'] by auto hence "x : supp \'" using v2 `(x,T') : set \'` `x \ \'` by auto hence "x : supp (a,S) \ supp \'" by auto hence "x : (supp ((a,S)#\') :: name set)" using supp_list_cons[of "(a,S)" \'] by force thus ?case by simp qed hence "~ (x \ \)" using fresh_def[of x \] by blast thus False using `x \ \` by auto qed inductive_cases tt_sub_ff:"\ ty.TT <: ty.FF" inductive_cases ff_sub_tt:"\ ty.FF <: ty.TT" lemma value_effect_tt_or_ff: assumes "v : values" and "\ \ v : T ; F" shows "F = FF \ v = Bool False \ F = TT \ v ~= Bool False" using prems proof (nominal_induct v avoiding: \ rule: values.strong_induct) case num_value thus ?case using num_ty_elim by auto next case bi_value thus ?case using bi_ty_elim by auto next case abs_value thus ?case using abs_ty_elim[of \ _ _ _ T F] by auto next case (bool_value b) thus ?case using true_ty_elim false_ty_elim by (cases b) auto qed lemma remove_fresh_env: assumes A:"y \ \" and B:"valid \" shows "\ - (y,T) = \" using B A proof (induct \ rule: valid.induct) case v1 thus ?case by auto next case (v2 \' a S) have "y \ a" "y \ \'" using `y \ ((a, S) # \')` using fresh_atm[of y a] fresh_list_cons by auto hence "((a, S) # \') - (y, T) = (a, S) # (\' - (y, T))" by auto thus ?case using v2 `y \ \'` by auto qed lemma subst_preserve_TE_app: assumes tapp:"(y,T0)#\ \ App e1 e2 : T ; TE S x" and neq:"y \ x" and val:"valid ((y,T0)#\)" and ih: "!! t bc bf . \t \ App e1 e2; (y, T0) # \ \ t : bc ; bf \ \ \T' F'. \ \ t[y::=v] : T' ; F' \ \ T' <: bc \ \ F' \ (App e1 e2)[y::=v] : T ; TE S x" proof - note te_ty_elim[OF tapp] then obtain f A A1 Fn Sa B where sz:"App e1 e2 = App f (Var x)" and tf:"(y, T0) # \ \ f : B ; Fn "" \ B <: A1 \ T : Latent S" and tvx:"(y, T0) # \ \ Var x : A ; VE x" and sub:" \ A <: A1" by auto hence "e1 = f" and "e2 = Var x" using trm.inject by auto hence "e2[y::=v] = Var x" using `y \ x` forget by auto hence tsub:" (y, T0)#\ \ e2[y::=v] : A ; VE x" using `e2=Var x` tvx by auto have fr:"y \ e2[y::=v]" using `e2 = Var x``e2[y::=v] = Var x` `y \ x` using fresh_atm by auto have "y \ \" "valid \" using valid_elim[OF val] by auto hence "((y, T0) # \) - (y, T0) = \" using remove_fresh_env[OF `y \ \` `valid \`] by auto hence te2:"\ \ e2[y::=v] : A ; VE x" using fresh_weakening[OF fr tsub `valid ((y,T0)#\)`, of T0] by auto have szf:"f \ App e1 e2" using sz by auto note ih[OF szf tf(1)] then obtain T' F' where tfsub:"\ \ f[y::=v] : T' ; F' "" \ T' <: B " "\ F' T' <: A1 \ T : Latent S " using `\ B <: A1 \ T : Latent S` by auto hence "\ \ (App f e2)[y::=v] : T ; TE S x" using te2 tfsub `\ A <: A1` by auto thus ?thesis using sz using trm.inject by auto qed inductive_cases te_elim_auto: "\ \ e : T ; TE S x" thm te_elim_auto lemma subst_preserve_TE: fixes v assumes tapp:"(y,T0)#\ \ e : T ; TE S x" and neq:"y \ x" and val:"valid ((y,T0)#\)" and ih: "!! t bc bf . \t \ e; (y, T0) # \ \ t : bc ; bf \ \ \T' F'. \ \ t[y::=v] : T' ; F' \ \ T' <: bc \ \ F' \ e[y::=v] : T ; TE S x" proof - obtain e1 e2 where "e = App e1 e2" using te_elim_auto[OF tapp, of thesis] by auto hence A:"(y,T0)#\ \ App e1 e2 : T ; TE S x" using tapp by auto note subst_preserve_TE_app[OF A neq val , of v] have "!! t bc bf . \t \ App e1 e2; (y, T0) # \ \ t : bc ; bf \ \ \T' F'. \ \ t[y::=v] : T' ; F' \ \ T' <: bc \ \ F' \ App e1 e2[y::=v] : T ; TE S x" using subst_preserve_TE_app[OF A neq val , of v] by auto thus ?thesis using `e = App e1 e2` by auto qed inductive_cases lam_latent_eff_elim_auto: "\ \ Lam[x:T].b : S1 \ S2 : Latent U ; F" thm lam_latent_eff_elim_auto lemma preserve_subst: assumes "(x,T0)#\ \ e : T ; F" and "\ \ e' : T1 ; G" and "\ T1 <: T0" and "valid ((x,T0)#\)" and "closed e'" and "e' : values" shows "EX T' F'. \ \ e[x::=e'] : T' ; F' \ \ T' <: T \ \ F' x e' T T1 T0 F G rule: trm_comp_induct) case (Var v) have a1: "\ \e':T1;G" by fact have a2: "((x,T0)#\) \ Var v:T;F" by fact hence a21: "(v,T)\set((x,T0)#\)" and a22: "valid((x,T0)#\)" and a22b:"F = VE v" using var_ty_elim[of "(x, T0) # \"] by auto from a22 have a23: "valid \" and a24: "x\\" by (auto dest: valid_elim) from a24 have a25: "\(\\. (x,\)\set \)" by (rule fresh_context) show ?case proof (cases "v=x") assume case1: "v=x" hence "(Var v)[x::=e'] = e'" by simp hence A:"\ \ (Var v)[x::=e'] : T1; G" using Var by auto have "simple_eff G" using closed_eff `closed e'` prems by auto hence C:"\ G set \" by force with case1 a25 show False by force qed hence D:"\ T1 <: T" using `\ T1 <: T0` by auto have "~ (\S y. F = TE S y)" using a22b by auto thus ?thesis using A a22b C D by blast next assume case2: "v\x" with a21 have a26: "(v,T)\set \" by force have a27:" Var v[x::=e'] = Var v" using case2 by simp from a23 a26 a27 have "\ \ Var v:T;VE v" by force thus ?thesis using a27 a22b by auto qed next case (Num n) have A:"(Num n)[x::=e'] = Num n" by auto have B:"F = eff.TT" using Num num_ty_elim by auto have "T = ty.Int" using num_ty_elim Num by auto hence "\ \ (Num n)[x::=e'] : T ; eff.TT" using Num A valid_elim[of x T0 \] by auto thus ?case using Num B by auto next case (Bool b) have v:"valid \" using prems typing_valid by auto have A:"(Bool b)[x::=e'] = Bool b" by auto thus ?case proof (cases b) case True hence B:"T = ty.TT" and "F = TT" using Bool true_ty_elim by auto thus ?thesis using A v True by auto next case False hence B:"T = ty.FF" and "F = FF" using Bool false_ty_elim by auto thus ?thesis using A v False by auto qed next case (BI b) have A:"(BI b)[x::=e'] = (BI b)" by auto have B:"F = eff.TT" using BI bi_ty_elim by auto have "T = \\<^isub>\ b" using bi_ty_elim BI by auto hence "\ \ (BI b)[x::=e'] : T ; eff.TT" using BI A valid_elim[of x T0 \] by auto thus ?case using BI B by auto next case (App s1 s2 \' x' e'' T' T1' T0' F' G') have ih_s1: "\c \ T F T' F' e' \. ((c,\)#\) \ s1:T; F \ closed e' \ e' : values \ valid ((c,\)#\) \ \\ e': T' ; F' \ \ T' <: \ \ EX S G. \ \ s1[c::=e']:S ; G \ \ S <: T \ \ G c \ T F T' F' e' \. ((c,\)#\) \ s2:T; F \ closed e' \ e' : values \ valid ((c,\)#\) \ \\ e': T' ; F' \ \ T' <: \ \ EX S G. \ \ s2[c::=e']:S ; G \ \ S <: T \ \ G ')\App s1 s2 : T'; F'" . from appty have elim1:"\T0 T0'a T1 le eff' eff'' U.(x',T0')#\' \ s1 :U;eff' \ (x',T0')# \'\ s2 : T0'a;eff'' \ \ U <: T0\T1:le \ \ T0'a <: T0 \ T1 = T'" using app_ty_elim by auto from appty have elim2:"(x', T0') # \' \ App s1 s2 : T' ; FF \ \T0 T0'a leS eff' eff'' le U.(x',T0')#\' \ s1 :U;eff' \ (x',T0')# \'\ s2 : T0'a;eff'' \ \ T0'a <: T0\ \ U <: T0\T':le \ le = Latent leS \ ~ (\ T0'a <: leS) \ s2 : values \ closed s2" using app_ty_ff_elim[of "((x',T0')#\')" s1 s2 T'] by blast have elim3:"(x', T0') # \' \ App s1 s2 : T' ; TT \ \T0 T0'a leS eff' eff'' U le.(x',T0')#\' \ s1 :U;eff' \ (x',T0')# \'\ s2 : T0'a;eff'' \ \ T0'a <: T0 \ \ U <: T0\T':le \ le = Latent leS \ \ T0'a <: leS " using app_ty_tt_elim[of "((x',T0')#\')" s1 s2 T'] by blast from elim1 obtain T0 T0'a T1 le eff' eff'' U where P:"(x',T0')#\' \ s1 :U;eff'"" (x',T0')# \'\ s2 : T0'a;eff''"" \ T0'a <: T0 "" T1 = T'" "\ U <: T0\T1:le" by auto hence "EX S1 G1. \' \ s1[x'::=e''] : S1 ; G1 \ \ S1 <: U \ \ G1 ' \ s1[x'::=e''] : S1 ; G1 "" \ S1 <: U" "\ G1 S1 <: T0\T1:le" using P Q by auto (* then apply ih_s2, get something about the substition of s2, and put it all back together. *) from P have "EX S G. \' \ s2[x'::=e'']:S ; G \ \ S <: T0'a \ \ G ' T0'a eff''] App by auto then obtain S2 G2 where S:"\' \ s2[x'::=e'']:S2 ; G2 "" \ S2 <: T0'a" "\ G2 S2 <: T0" using P S by auto have L1:"\' \ App ?ns1 ?ns2 : T1 ; NE" using Q S sub1 sub2 by auto have L2:"T1 = T'" . show ?case using appty proof (nominal_induct F' rule: eff.induct) case NE thus ?case using L1 L2 by auto next case VE thus ?case using L1 L2 by auto next case (TE ty var) thus ?case using L1 L2 by auto next case TT from elim3 TT obtain T0 T0'a T1 le leS eff' eff'' U where P:"(x',T0')#\' \ s1 :U;eff'"" (x',T0')# \'\ s2 : T0'a;eff''"" \ T0'a <: T0 "" T1 = T'" "\ U <: T0\T1:le" "le = Latent leS" "\ T0'a <: leS" by auto hence "EX S1 G1. \' \ s1[x'::=e''] : S1 ; G1 \ \ S1 <: U \ \ G1 ' \ s1[x'::=e''] : S1 ; G1 "" \ S1 <: U" "\ G1 S1 <: T0\T1:le" using P by auto (* then apply ih_s2, get something about the substition of s2, and put it all back together. *) from P have "EX S G. \' \ s2[x'::=e'']:S ; G \ \ S <: T0'a \ \ G ' T0'a eff''] App by auto then obtain S2 G2 where S:"\' \ s2[x'::=e'']:S2 ; G2 "" \ S2 <: T0'a" "\ G2 S2 <: leS" using `\ S2 <: T0'a` `\ T0'a <: leS` by auto have L1:"\' \ App ?ns1 ?ns2 : T1 ; TT" using P Q R S noover T_AppPredFalse[of \' " s1[x'::=e'']" U] by auto have L2:"T1 = T'" . from L1 L2 show ?case by auto next case FF from elim2 FF obtain T0 T0'a T1 le leS eff' eff'' U where P:"(x',T0')#\' \ s1 :U;eff'"" (x',T0')# \'\ s2 : T0'a;eff''"" \ T0'a <: T0 "" T1 = T'" "\ U <: T0\T1:le" "le = Latent leS" "~ (\ T0'a <: leS)" "s2 :values" "closed s2" by auto hence "EX S1 G1. \' \ s1[x'::=e''] : S1 ; G1 \ \ S1 <: U \ \ G1 ' \ s1[x'::=e''] : S1 ; G1 "" \ S1 <: U" "\ G1 S1 <: T0\T1:le" using P by auto (* then apply ih_s2, get something about the substition of s2, and put it all back together. *) from P have "EX S G. \' \ s2[x'::=e'']:S ; G \ \ S <: T0'a \ \ G ' T0'a eff''] App by auto then obtain S2 G2 where S:"\' \ s2[x'::=e'']:S2 ; G2 "" \ S2 <: T0'a" "\ G2 s2" using closed_def fresh_def[of x' s2] `closed s2` by auto hence "s2 = ?ns2" using forget by auto hence S':"\' \ ?ns2 : T0'a ; eff''" using `(x',T0')#\' \ s2 : T0'a ; eff''` fresh_weakening_cons `valid ((x',T0')#\')` `x' \ s2` by auto have noover: "~(\ T0'a <: leS)" . have T:"closed ?ns2" "?ns2 : values" using `s2 = ?ns2` `closed s2` `s2 : values` by auto have L1:"\' \ App ?ns1 ?ns2 : T1 ; FF" using P Q R S' T noover by auto have L2:"T1 = T'" by fact from L1 L2 show ?case by auto qed next case (Lam a body \' x' e'' T' T1' T0' F' G' ty ) hence f1: "a\\'" and f2: "a\x'" and f2': "x'\a" and f3: "a\e''" and f4: "a\((x',T0')#\')" by (auto simp add: fresh_atm fresh_prod fresh_list_cons) have c1: "((x',T0')#\')\Lam [a:ty].body : T' ; F'" by fact (* hence "\\2 eff L S. ((a,ty)#(x',T0')#\') \ body : \2 ; eff \ T'=ty\\2:L \ F' = TT" using f4 abs_ty_elim by auto *) then obtain \2 eff L S where c11: "T'=ty\\2:L" and c12: "((a,ty)#(x',T0')#\') \ body : \2 ; eff" and "F' = TT" and c13:"L = latent_eff.NE \ (eff = TE S a \ L = Latent S)" using f4 abs_ty_elim by blast from c12 have "valid ((a,ty)#(x',T0')#\')" using Lam by auto hence ca: "valid \'" and cb: "a\\'" and cc: "x'\\'" by (auto dest: valid_elim simp add: fresh_list_cons) have c2: "((a,ty)#(x',T0')#\') \ ((x',T0')#(a,ty)#\')" by force have c3: "valid ((x',T0')#(a,ty)#\')" by (rule v2, rule v2, auto simp add: fresh_list_cons fresh_prod ca cb cc f2' fresh_ty) from c12 c2 c3 have c14: "((x',T0')#(a,ty)#\') \ body : \2 ; eff" using `valid ((a, ty) # (x', T0') # \')` by (force intro: weakening) let ?inner\ = "(a,ty)#\'" have validig:"valid ?inner\" using `a \ \'` `valid \'` by auto have c15:"\' \ ?inner\" by auto hence c16:"?inner\ \ e'' : T1' ; G'" using weakening[of \' _ _ _ ?inner\] `\' \ e'' : T1' ; G'` validig `valid \'` by simp have "EX TA0 FA0. ?inner\ \ body[x'::=e''] : TA0 ; FA0 \ \ TA0 <: \2 \ \ FA0 \2 eff e'' T1' G'] ` \ T1' <: T0'` `valid ((x', T0') # (a, ty) # \')` c14 `closed e''` `e'' : values` by auto then obtain TA0 FA0 where body_ty:"?inner\ \ body[x'::=e''] : TA0 ; FA0 "" \ TA0 <: \2" by auto hence L11:"\' \ (Lam[a:ty].(body[x'::=e''])) : ty \ TA0 : latent_eff.NE; eff.TT" using `a \ \'` by auto note Lam(9)[OF _ _ `(a, ty)# \' \ e'' : T1' ; G'` `\ T1' <: T0'` `valid ((x', T0')# (a, ty) # \')` `closed e''` `e'' : values`] hence "!! t bc bf . \t \ Lam [a:ty].body; (x', T0') #(a, ty)# \' \ t : bc ; bf \ \ \T' F'. (a, ty)#\' \ t[x'::=e''] : T' ; F' \ \ T' <: bc \ \ F' t \ body; (x', T0') # (a, ty)#\' \ t : bc ; bf \ \ \T' F'. (a, ty)#\' \ t[x'::=e''] : T' ; F' \ \ T' <: bc \ \ F' \' \ (Lam[a:ty].(body[x'::=e''])) : ty \ \2 : Latent S; eff.TT" proof - assume "L = Latent S" hence "eff = TE S a" using c13 by auto hence c12':"(a, ty) # (x', T0') # \' \ body : \2 ; TE S a" using c12 by simp have c12'':" (x', T0') # (a, ty) # \' \ body : \2 ; TE S a" using weakening[OF c12' _ c2 ] using `valid ((x', T0') # (a, ty) # \')` `valid ((a, ty) # (x', T0') # \')` by auto have f2':"x' \ a" using f2 by auto note body_ty subst_preserve_TE[OF c12'' f2' `valid ((x', T0') # (a, ty) # \')` , of e''] hence "(a, ty) # \' \ body[x'::=e''] : \2 ; TE S a" using ih_body by auto hence "?inner\ \ body[x'::=e''] : \2 ; TE S a " . thus ?thesis using `a \ \'` by auto qed (* from L11 L12 have L1:"\' \ (Lam[a:ty].(body[x'::=e''])) : ty \ TA0 : L; eff.TT" using c13 by auto *) have L21:"\ ty \ TA0 : L <: T'" using c11 ` \ TA0 <: \2` by auto have L22: "\ ty \ \2 : L <: T'" using c11 by auto have L3:"(Lam[a:ty].body)[x'::=e''] = (Lam[a:ty].(body[x'::=e'']))" using Lam by auto have L4:"\ eff.TT (Lam [a:ty].body) : T ; TE S x \ False" proof - fix Env a ty body T S x assume "Env \ (Lam [a:ty].body) : T ; TE S x" have " Env \ (Lam [a:ty].body) : T ; TE S x \ False" by (ind_cases " Env \ (Lam [a:ty].body) : T ; TE S x") thus False using prems by auto qed from L11 L12 L21 L22 L3 L4 L5[of \' a _ ty ] c13 show ?case by auto next case (Iff t1 t2 t3 \' x' e'' T' T0' T1' F' G') let ?\ = "(x', T1') # \'" have A:"(\ T1 T2 T3 F1 F2 F3. (?\ \ t1 : T1 ; F1) \ ?\ |+ F1 \ t2 : T2 ; F2 \ ?\ |- F1 \ t3 : T3 ; F3 \ \ T2 <: T' \ \ T3 <: T' \ F' = NE) \ (\ T1 T3 F3. (?\ \ t1 : T1 ; FF) \ ?\ \ t3 : T3 ; F3 \ \ T3 <: T' \ F' = NE) \ (\ T1 T2 F2. (?\ \ t1 : T1 ; TT) \ ?\ \ t2 : T2 ; F2 \ \ T2 <: T' \ F' = NE)" using Iff if_ty_elim by auto thus ?case proof - { assume "(\ T1 T2 T3 F1 F2 F3. (?\ \ t1 : T1 ; F1) \ ?\ |+ F1 \ t2 : T2 ; F2 \ ?\ |- F1 \ t3 : T3 ; F3 \ \ T2 <: T' \ \ T3 <: T' \ F' = NE)" then obtain T1 T2 T3 F1 F2 F3 where "?\ \ t1 : T1 ; F1 "" ?\ |+ F1 \ t2 : T2 ; F2 "" ?\ |- F1 \ t3 : T3 ; F3 "" \ T2 <: T'""\ T3 <: T'""F' = NE" by auto hence ?thesis proof (nominal_induct F1 rule: eff.induct) case NE from NE have "\S1 G1. \' \ t1[x'::=e''] : S1 ; G1 \ \ S1 <: T1 \ \ G1 ' \ t1[x'::=e''] : S1 ; G1 "" \ S1 <: T1 "" \ G1 G1 \ t2 : T2 ; F2)" using prems by auto have p2:"(?\ \ t3 : T3 ; F3)" using prems by auto from p1 have "\S2 G2. \' \ t2[x'::=e''] : S2 ; G2 \ \ S2 <: T2 \ \ G2 ' \ t2[x'::=e''] : S2 ; G2 "" \ S2 <: T2 "" \ G2 S3 G3. \' \ t3[x'::=e''] : S3 ; G3 \ \ S3 <: T3 \ \ G3 ' \ t3[x'::=e''] : S3 ; G3 "" \ S3 <: T3 "" \ G3 ' |+ G1 \ t2[x'::=e''] : S2 ; G2" using B simple by auto have C':"\' |- G1 \ t3[x'::=e''] : S3 ; G3" using C simple by auto have D:"\ S2 <: T'" using prems B by auto have E:"\ S3 <: T'" using prems C by auto from A B' C' D E have " \' \ Iff t1 t2 t3[x'::=e''] : T' ; comb_eff G1 G2 G3" by (auto simp del: comb_eff.simps) thus ?case using `F' = NE` by auto next case TT from TT have "\S1 G1. \' \ t1[x'::=e''] : S1 ; G1 \ \ S1 <: T1 \ \ G1 ' \ t1[x'::=e''] : S1 ; G1 "" \ S1 <: T1 "" \ G1 \ t2 : T2 ; F2)" using prems by auto have p2:"(?\ \ t3 : T3 ; F3)" using prems by auto from p1 have "\S2 G2. \' \ t2[x'::=e''] : S2 ; G2 \ \ S2 <: T2 \ \ G2 ' \ t2[x'::=e''] : S2 ; G2 "" \ S2 <: T2 "" \ G2 S3 G3. \' \ t3[x'::=e''] : S3 ; G3 \ \ S3 <: T3 \ \ G3 ' \ t3[x'::=e''] : S3 ; G3 "" \ S3 <: T3 "" \ G3 ' |+ G1 \ t2[x'::=e''] : S2 ; G2" using B simple by auto have C':"\' |- G1 \ t3[x'::=e''] : S3 ; G3" using C simple by auto have D:"\ S2 <: T'" using prems B by auto have E:"\ S3 <: T'" using prems C by auto from A B' C' D E have " \' \ Iff t1 t2 t3[x'::=e''] : T' ; comb_eff G1 G2 G3" by (auto simp del: comb_eff.simps) thus ?case using `F' = NE` by auto next case FF from FF have "\S1 G1. \' \ t1[x'::=e''] : S1 ; G1 \ \ S1 <: T1 \ \ G1 ' \ t1[x'::=e''] : S1 ; G1 "" \ S1 <: T1 "" \ G1 \ t2 : T2 ; F2)" using prems by auto have p2:"(?\ \ t3 : T3 ; F3)" using prems by auto from p1 have "\S2 G2. \' \ t2[x'::=e''] : S2 ; G2 \ \ S2 <: T2 \ \ G2 ' \ t2[x'::=e''] : S2 ; G2 "" \ S2 <: T2 "" \ G2 S3 G3. \' \ t3[x'::=e''] : S3 ; G3 \ \ S3 <: T3 \ \ G3 ' \ t3[x'::=e''] : S3 ; G3 "" \ S3 <: T3 "" \ G3 ' |+ G1 \ t2[x'::=e''] : S2 ; G2" using B simple by auto have C':"\' |- G1 \ t3[x'::=e''] : S3 ; G3" using C simple by auto have D:"\ S2 <: T'" using prems B by auto have E:"\ S3 <: T'" using prems C by auto from A B' C' D E have " \' \ Iff t1 t2 t3[x'::=e''] : T' ; comb_eff G1 G2 G3" by (auto simp del: comb_eff.simps) thus ?case using `F' = NE` by auto next case (VE z) hence A:"t1 = (Var z) " "?\ \ Var z : T1 ; VE z" using ve_ty_elim[OF `?\ \ t1 : T1; VE z`] using eff.inject by auto have size1:"(Var z\Iff t1 t2 t3)" using A by simp note Iff(1)[of "Var z"] hence ih_f:"!! c \ \ T F e' T0 F0 . (c,\)#\ \ (Var z) : T ; F \ \ \ e' : T0 ; F0 \ \ T0 <: \ \ valid ((c,\)#\) \ closed e' \ e' : values \ EX T' F' . \ \ (Var z)[c::=e'] : T' ; F' \ \ T' <: T \ \ F' ' \ (Var z)[x'::=e''] : A' ; Fn' \ \ A' <: T1 \ \ Fn' ' \ (Var z)[x'::=e''] : A' ; Fn' \ \ A' <:T1" by auto let ?mapfun = "(%f. (% (v,ty). (if (z = v) then (v,f ty.FF ty) else (v,ty))))" let ?\1 = "(map (?mapfun remove) \')" let ?\2 = "(map (?mapfun replace) \')" have "valid \'" using `valid ?\` using valid_elim[of x' T1' \'] by auto show ?case proof (cases "x' = z") case True from A True have "(Var z)[x'::=e''] = e''" by auto hence D:"\' \ (Var z)[x'::=e''] : T0' ; G'" "closed ((Var z)[x'::=e''])" "((Var z)[x'::=e'']) : values" using Iff by auto have "\ T0' <: T1'" . note var_ty_elim[of ?\ z _ "VE z"] hence "(x', T1') : set ?\" using A True by auto have "?\ \ (Var x') : T1' ; VE x'" using `valid ?\` by auto have "simple_ty T0'" using `\' \ e'' : T0' ; G'` `e'' : values` value_simple_type by auto let ?mapfun = "(%f. (% (v,ty). (if (z = v) then (v,f ty.FF ty) else (v,ty))))" let ?\1 = "(map (?mapfun remove) \')" let ?\2 = "(map (?mapfun replace) \')" have "?\1 = envop remove z ty.FF \'" by auto have "?\2 = envop replace z ty.FF \'" by auto have "x' \ \'" using Iff valid_elim[of x' T1' \'] by auto hence "?\1 = \'" using True envop_forget `valid \'` by auto hence GA:"?\ |+ VE z = (x',remove ty.FF T1') # \'" using True by auto hence G1:"\ \ t2 : T2; F2" using `(?\ |+ VE z)\ t2 : T2 ; F2` by auto have "?\2 = \'" using `x' \ \'` True envop_forget `valid \'` by auto hence "?\ |- VE z = (x',replace ty.FF T1') # \'" using True by auto hence GB:"?\ |- VE z = (x',ty.FF) # \'" by auto hence G2:"\ \ t3 : T3; F3" using `(?\ |- VE z)\ t3 : T3 ; F3` by auto have "valid (?\ |+ VE z)" using `valid ?\` envplus_valid[of ?\ "VE z"] by auto hence G3:"valid ((x',remove ty.FF T1') # \')" using GA by auto have "valid (?\ |- VE z)" using `valid ?\` envminus_valid[of ?\ "VE z"] by auto hence G4:"valid ((x',ty.FF) # \')" using GB by auto show ?thesis proof (cases "e'' = Bool False") case True hence "(Var z)[x'::=e''] = Bool False" using `x' = z` by auto hence "t1[x'::=e''] = Bool False" using `t1 = Var z` by auto hence X1:"?\ \ t1[x'::=e''] : ty.FF ; FF" using `valid ?\` by auto have "\' \ e'' : ty.FF ; FF" using True `valid \'` by auto note `?\ |- VE z = (x', ty.FF) # \'` hence "valid ((x', ty.FF) # \')" using G4 by auto have X2:"(x', ty.FF) # \' \ t3 : T3 ; F3" using VE `?\ |- VE z = (x', ty.FF) # \'` by auto note Iff(4)[ OF X2 `\' \ e'' : ty.FF ; FF ` _ `valid ((x', ty.FF) # \')`] then obtain T'' F'' where X3:"\' \ t3[x'::=e''] : T'' ; F'' " and X4:" \ T'' <: T3 "" \ F'' T'' <: T'" using `\ T3 <: T'` by auto hence "\' \ Iff (Bool False) (t2[x'::=e'']) (t3[x'::=e'']) : T'' ; NE" using `valid \'` X3 by auto hence "\' \ (Iff t1 t2 t3)[x'::=e''] : T'' ; NE" using ` t1[x'::=e''] = Bool False` by auto thus ?thesis using `\ T'' <: T'` `F' = NE` by auto next case False hence "(Var z)[x'::=e''] = e''" using `x' = z` by auto hence "t1[x'::=e''] = e''" using `t1 = Var z` by auto hence X1:"\' \ t1[x'::=e''] : T0' ; G'" by auto have "\' \ e'' : T0' ; G'" . hence "G' = TT" using value_effect_tt_or_ff[OF `e'' : values` `\' \ e'' : T0' ; G'`] False by auto hence X2:"\' \ t1[x'::=e''] : T0' ; TT" using X1 by auto have "\ T0' <: T1'" . have X3:"\ \ T0' <: ty.FF" proof (rule ccontr) assume "\\ \ T0' <: ty.FF" hence "\ T0' <: ty.FF" by simp hence "\ T0' <: BoolTy" using BoolTy_def by auto hence "EX b. e'' = Bool b" using bool_value `e'' : values ` `\' \ e'' : T0' ; G'` by auto then obtain b where A:"e'' = Bool b" by auto thus False proof (cases b) case False thus ?thesis using A `e'' ~= Bool False` by auto next case True hence "T0' = ty.TT" using `\' \ e'' : T0' ; G'` A true_ty_elim by auto thus ?thesis using `\ T0' <: ty.FF` tt_sub_ff by auto qed qed let ?rty = "remove ty.FF T1'" note `?\ |+ VE z = (x', ?rty) # \'` hence "valid ((x', ?rty) # \')" using G3 by auto have X2:"(x', ?rty) # \' \ t2 : T2 ; F2" using VE `?\ |+ VE z = (x', ?rty) # \'` by auto note Iff(3)[ OF X2 `\' \ e'' : T0' ; G' ` _ `valid ((x', ?rty) # \')`] then obtain T'' F'' where X3:"\' \ t2[x'::=e''] : T'' ; F'' " and X4:" \ T'' <: T2 "" \ F'' T0' <: T1'` X3 `simple_ty T0'`] by auto hence "\ T'' <: T'" using `\ T2 <: T'` by auto hence "\' \ Iff e'' (t2[x'::=e'']) (t3[x'::=e'']) : T'' ; NE" using `valid \'` X3 `\' \ e'' : T0' ; G' ` `G' = TT` by auto hence "\' \ (Iff t1 t2 t3)[x'::=e''] : T'' ; NE" using ` t1[x'::=e''] = e''` by auto thus ?thesis using `\ T'' <: T'` `F' = NE` by auto qed next case False from A False have "(Var z)[x'::=e''] = (Var z)" by auto hence D:"\' \ (Var z)[x'::=e''] : T1 ; VE z" using False A proof - have q1:"?\ \ Var z : T1 ; VE z" using A by auto have "x' \ Var z" using trm.fresh False fresh_atm by auto hence "\' \ Var z : T1 ; VE z" using q1 fresh_weakening_cons `valid ((x',T1')# \')` by auto thus ?thesis using `(Var z)[x'::=e''] = Var z` by auto qed hence typetst: "\' \ t1[x'::=e''] : T1 ; VE z" using A by auto have F:"?\ |+ VE z = (x',T1') # ?\1" using False by auto hence H:"(x',T1') # ?\1 \ t2 : T2 ; F2" using `?\ |+ VE z \ t2 : T2 ; F2` by auto hence K:"valid ?\1" using envop_valid `valid \'` by auto have J:"?\1 \ e'' : T0' ; G'" using K `valid \'` closed_any_env `closed e''` Iff by blast have "x' \ ?\1" using Iff valid_elim[of x' T1' \'] envop_fresh[of x' \' remove] `valid \'` by auto hence "valid ((x',T1')#?\1)" using `valid ?\1` by auto hence ex1:"\S2 G2. ?\1 \ t2[x'::=e''] : S2 ; G2 \ \ S2 <: T2 \ \ G2 |- VE z = (x',T1') # ?\2" using False by auto hence H:"(x',T1') # ?\2 \ t3 : T3 ; F3" using `?\ |- VE z \ t3 : T3 ; F3` by auto hence K:"valid ?\2" using envop_valid `valid \'` by auto have J:"?\2 \ e'' : T0' ; G'" using K `valid \'` closed_any_env `closed e''` Iff by blast have "x' \ ?\2" using Iff valid_elim[of x' T1' \'] envop_fresh[of x' \' _ z _] `valid \'` by auto hence "valid ((x',T1')#?\2)" using `valid ?\2` by auto hence ex2:"\S3 G3. ?\2 \ t3[x'::=e''] : S3 ; G3 \ \ S3 <: T3 \ \ G3 1 \ t2[x'::=e''] : S2 ; G2"" \ S2 <: T'" using `\ T2 <: T'` by auto from ex2 obtain S3 G3 where 2:"?\2 \ t3[x'::=e''] : S3 ; G3"" \ S3 <: T'" using `\ T3 <: T'` by auto have 4:"?\1 = \' |+ (VE z)" by auto have 5:"?\2 = \' |- (VE z)" by auto have X:"!! G G' e T F. G = G' \ G \ e : T ; F \ G' \ e : T ; F" by auto from 1 4 have 6:"\' |+ (VE z) \ t2[x'::=e''] : S2 ; G2" using X[of ?\1 "\' |+ (VE z)" " t2[x'::=e'']" S2 G2] by blast from 2 5 have 7:"\' |- (VE z) \ t3[x'::=e''] : S3 ; G3" using X[of ?\2 "\' |- (VE z)" " t3[x'::=e'']" S3 G3] by blast from typetst 1 2 6 7 have "\' \ (Iff t1 t2 t3)[x'::=e''] : T' ; comb_eff (VE z) G2 G3" by (auto simp del: comb_eff.simps) thus ?thesis using `F' = NE` by auto qed next case (TE U z) have "EX f A A1 Fn B. t1 = (App f (Var z)) \ (x', T1') # \' \ f : B ; Fn \ \ B <: A1 \ T1 : Latent U \ (x', T1') # \' \ (Var z) : A ; VE z \ \ A <: A1" using TE te_ty_elim[of ?\ t1 T1 U z] by auto then obtain f A1 A Fn B where A:"t1 = (App f (Var z)) "" (x', T1') # \' \ f : B ; Fn" "\ B <: A1 \ T1 : Latent U" "(x', T1') # \' \ (Var z) : A ; VE z "" \ A <: A1" by auto have size1:"(f\Iff t1 t2 t3)" using A(1) by (simp ) note Iff(1)[of f] hence ih_f:"!! c \ \ T F e' T0 F0 . (c,\)#\ \ f : T ; F \ \ \ e' : T0 ; F0 \ \ T0 <: \ \ valid ((c,\)#\) \ closed e' \ e' : values \ EX T' F' . \ \ f[c::=e'] : T' ; F' \ \ T' <: T \ \ F' ' \ f[x'::=e''] : A' ; Fn' \ \ A' <: B \ \ Fn' ' \ f[x'::=e''] : A' ; Fn' \ \ A' <:B" by auto let ?mapfun = "(%f. (% (v,ty). (if (z = v) then (v,f U ty) else (v,ty))))" let ?\1 = "(map (?mapfun restrict) \')" let ?\2 = "(map (?mapfun remove) \')" have "valid \'" using `valid ?\` using valid_elim[of x' T1' \'] by auto show ?case proof (cases "x' = z") case True from A True have "(Var z)[x'::=e''] = e''" by auto hence D:"\' \ (Var z)[x'::=e''] : T0' ; G'" "closed ((Var z)[x'::=e''])" "((Var z)[x'::=e'']) : values" using Iff by auto have "\ T0' <: T1'" . note var_ty_elim[of ?\ z A "VE z"] hence "(x', A) : set ?\" using A True by auto have "?\ \ (Var x') : T1' ; VE x'" using `valid ?\` by auto hence "T1' = A" using A unique_var_typing[of ] True by auto have "\ T0' <: T1'" . hence "\ T0' <: A" using `T1' = A` by simp have "simple_ty T0'" using `\' \ e'' : T0' ; G'` `e'' : values` value_simple_type by auto have or:" (\ T0' <: U \ \ T0' <: restrict U T1') \ (~ (\ T0' <: U) \ \ T0' <: remove U T1')" using `\' \ e'' : T0' ; G'` `e'' : values` `\ T0' <: T1'` `closed e''` `simple_ty T0'` restrict_remove_soundness by auto have "?\1 = envop restrict z U \'" by auto have "?\2 = envop remove z U \'" by auto have "x' \ \'" using Iff valid_elim[of x' T1' \'] by auto hence "?\1 = \'" using True envop_forget `valid \'` by auto hence GA:"?\ |+ TE U z = (x',restrict U T1') # \'" using True by auto hence G1:"\ \ t2 : T2; F2" using `(?\ |+ TE U z)\ t2 : T2 ; F2` by auto have "?\2 = \'" using `x' \ \'` True envop_forget `valid \'` by auto hence GB:"?\ |- TE U z = (x',remove U T1') # \'" using True by auto hence G2:"\ \ t3 : T3; F3" using `(?\ |- TE U z)\ t3 : T3 ; F3` by auto have "valid (?\ |+ TE U z)" using `valid ?\` envplus_valid[of ?\ "TE U z"] by auto hence G3:"valid ((x',restrict U T1') # \')" using GA by auto have "valid (?\ |- TE U z)" using `valid ?\` envminus_valid[of ?\ "TE U z"] by auto hence G4:"valid ((x',remove U T1') # \')" using GB by auto show ?thesis proof - { assume "\ T0' <: U "" \ T0' <: restrict U T1'" have 2:"(x', restrict U T1') # \' \ t2 : T2 ; F2 " using `?\ |+ TE U z \ t2 : T2 ; F2` GA by auto note Iff(2)[of x' "restrict U T1'" \' T2 F2 e'' T0' G'] hence "\S2 G2. \' \ t2[x'::=e''] : S2 ; G2 \ \ S2 <: T2 \ \ G2 '|+ eff.TT \ t2[x'::=e''] : S2 ; G2 "" \ S2 <: T2 "" \ G2 T0' <: A1" "\ A' <: A1 \ T1 : Latent U" using A B D `\ T0' <: A` by auto hence "\' \ (App f (Var z))[x'::=e''] : T1 ; eff.TT" using A B D `\ T0' <: A` `\ T0' <: U` using T_AppPredTrue[of \' _ A' Fn' A1 T1 U _ T0' G'] by auto hence L3:"\' \ t1[x'::=e''] : T1 ; eff.TT" using `t1 = App f (Var z)` by auto have "\ S2 <: T'" using L1 `\ T2 <: T'` by auto hence "\'\ (Iff t1 t2 t3)[x'::=e''] : T' ; eff.NE" using L3 ` \'|+eff.TT \ t2[x'::=e''] : S2 ; G2` by auto hence ?thesis using `F' = NE` by auto } moreover { assume "~ (\ T0' <: U) "" \ T0' <: remove U T1'" have 3:"(x', remove U T1') # \' \ t3 : T3 ; F3 " using `?\ |- TE U z \ t3 : T3 ; F3` GB by auto note Iff(3)[of x' "remove U T1'" \' T3 F3 e'' T0' G'] hence "\S3 G3. \' \ t3[x'::=e''] : S3 ; G3 \ \ S3 <: T3 \ \ G3 '|+ eff.FF \ t3[x'::=e''] : S3 ; G3 "" \ S3 <: T3 "" \ G3 T0' <: A1" using A B D `\ T0' <: A` by auto hence "\' \ (App f (Var z))[x'::=e''] : T1 ; eff.FF" using A B D `\ T0' <: A` `~ (\ T0' <: U)` using T_AppPredFalse[of \' _ A' Fn' A1 T1 U _ T0' G'] by auto hence L3:"\' \ t1[x'::=e''] : T1 ; eff.FF" using `t1 = App f (Var z)` by auto have "\ S3 <: T'" using L1 `\ T3 <: T'` by auto hence "\'\ (Iff t1 t2 t3)[x'::=e''] : T' ; eff.NE" using L3 ` \'|+eff.FF \ t3[x'::=e''] : S3 ; G3` by auto hence ?thesis using `F' = NE` by auto } ultimately show ?thesis using or by auto qed next case False from A False have "(Var z)[x'::=e''] = (Var z)" by auto hence D:"\' \ (Var z)[x'::=e''] : A ; VE z" using False A proof - have q1:"?\ \ Var z : A ; VE z" . have "x' \ Var z" using trm.fresh False fresh_atm by auto hence "\' \ Var z : A ; VE z" using q1 fresh_weakening_cons `valid ((x',T1')# \')` by auto thus ?thesis using `(Var z)[x'::=e''] = Var z` by auto qed from A B D have "\' \ App (f[x'::=e'']) ((Var z)[x'::=e'']) : T1 ; TE U z" by auto hence typetst: "\' \ t1[x'::=e''] : T1 ; TE U z" using A by auto have F:"?\ |+ TE U z = (x',T1') # ?\1" using False by auto hence H:"(x',T1') # ?\1 \ t2 : T2 ; F2" using `?\ |+ TE U z \ t2 : T2 ; F2` by auto hence K:"valid ?\1" using envop_valid `valid \'` by auto have J:"?\1 \ e'' : T0' ; G'" using K `valid \'` closed_any_env `closed e''` Iff by blast have "x' \ ?\1" using Iff valid_elim[of x' T1' \'] envop_fresh[of x' \' restrict z U] `valid \'` by auto hence "valid ((x',T1')#?\1)" using `valid ?\1` by auto hence ex1:"\S2 G2. ?\1 \ t2[x'::=e''] : S2 ; G2 \ \ S2 <: T2 \ \ G2 |- TE U z = (x',T1') # ?\2" using False by auto hence H:"(x',T1') # ?\2 \ t3 : T3 ; F3" using `?\ |- TE U z \ t3 : T3 ; F3` by auto hence K:"valid ?\2" using envop_valid `valid \'` by auto have J:"?\2 \ e'' : T0' ; G'" using K `valid \'` closed_any_env `closed e''` Iff by blast have "x' \ ?\2" using Iff valid_elim[of x' T1' \'] envop_fresh[of x' \' remove z U] `valid \'` by auto hence "valid ((x',T1')#?\2)" using `valid ?\2` by auto hence ex2:"\S3 G3. ?\2 \ t3[x'::=e''] : S3 ; G3 \ \ S3 <: T3 \ \ G3 1 \ t2[x'::=e''] : S2 ; G2"" \ S2 <: T'" using `\ T2 <: T'` by auto from ex2 obtain S3 G3 where 2:"?\2 \ t3[x'::=e''] : S3 ; G3"" \ S3 <: T'" using `\ T3 <: T'` by auto have 4:"?\1 = \' |+ (TE U z)" by auto have 5:"?\2 = \' |- (TE U z)" by auto have X:"!! G G' e T F. G = G' \ G \ e : T ; F \ G' \ e : T ; F" by auto from 1 4 have 6:"\' |+ (TE U z) \ t2[x'::=e''] : S2 ; G2" using X[of ?\1 "\' |+ (TE U z)" " t2[x'::=e'']" S2 G2] by blast from 2 5 have 7:"\' |- (TE U z) \ t3[x'::=e''] : S3 ; G3" using X[of ?\2 "\' |- (TE U z)" " t3[x'::=e'']" S3 G3] by blast from typetst 1 2 6 7 have "\' \ (Iff t1 t2 t3)[x'::=e''] : T' ; comb_eff (TE U z) G2 G3" by (auto simp del: comb_eff.simps) thus ?thesis using `F' = NE` by auto qed qed } moreover { assume "\ T1 T3 F3. (?\ \ t1 : T1 ; FF) \ ?\ \ t3 : T3 ; F3 \ \ T3 <: T' \ F' = NE" then obtain T1 T3 F3 where "?\ \ t1 : T1 ; FF" "?\ \ t3 : T3 ; F3" "\ T3 <: T'" "F' = NE" by auto hence "\S1 G1. \' \ t1[x'::=e''] : S1 ; G1 \ \ S1 <: T1 \ \ G1 ' \ t1[x'::=e''] : S1 ; G1 "" \ S1 <: T1 "" \ G1 ' \ t1[x'::=e''] : S1 ; FF " using B no_sub_FF by auto from prems have "\S3 G3. \' \ t3[x'::=e''] : S3 ; G3 \ \ S3 <: T3 \ \ G3 ' \ t3[x'::=e''] : S3 ; G3 ""\ S3 <: T3" by auto from B C D have "\' \ (Iff (t1[x'::=e'']) (t2[x'::=e'']) (t3[x'::=e''])) : S3 ; eff.NE" by auto hence ?thesis using `\ T3 <: T'` `\ S3 <: T3` `F' = NE` by auto } moreover { assume "\ T1 T2 F2. (?\ \ t1 : T1 ; TT) \ ?\ \ t2 : T2 ; F2 \ \ T2 <: T' \ F' = NE" then obtain T1 T2 F2 where "?\ \ t1 : T1 ; TT" "?\ \ t2 : T2 ; F2" "\ T2 <: T'" "F' = NE" by auto hence "\S1 G1. \' \ t1[x'::=e''] : S1 ; G1 \ \ S1 <: T1 \ \ G1 ' \ t1[x'::=e''] : S1 ; G1 "" \ S1 <: T1 "" \ G1 ' \ t1[x'::=e''] : S1 ; TT " using B no_sub_TT by auto from prems have "\S2 G2. \' \ t2[x'::=e''] : S2 ; G2 \ \ S2 <: T2 \ \ G2 ' \ t2[x'::=e''] : S2 ; G2 ""\ S2 <: T2" by auto from B C D have "\' \ (Iff (t1[x'::=e'']) (t2[x'::=e'']) (t3[x'::=e''])) : S2 ; eff.NE" by auto hence ?thesis using `\ T2 <: T'` `\ S2 <: T2` `F' = NE` by auto } ultimately show ?thesis using A by blast qed qed lemma subst_produces_TT: assumes ty:"(x,T0)#\ \ e : T ; TE S x" and vty:"\ \ v : T0' ; F" and A:"\ T0' <: T0" and B:"valid ((x,T0)#\)" and C:"closed v" and D:"v : values" and E:"\ T0' <: S" shows "EX T'. \ \ e[x::=v] : T' ; TT \ \ T' <: T" proof - obtain f A A1 Fn Sa B where eq:"e = App f (Var x)" and fty:"(x, T0) # \ \ f : B ; Fn " and bsub:" \ B <: A1 \ T : Latent S " and xty:" (x, T0) # \ \ Var x : A ; VE x " and asub:" \ A <: A1" using te_ty_elim[OF ty] by auto note preserve_subst[OF fty vty A B C D] then obtain T' F' where X1:"\ \ f[x::=v] : T' ; F' " and " \ T' <: B "" \ F' T' <: A1 \ T : Latent S" using bsub by auto have "(Var x)[x::=v] = v" by simp hence X3:"\ \ (Var x)[x::=v] : T0' ; F" using vty by auto have "(x, T0) # \ \ Var x : T0 ; VE x" using `valid ((x, T0) # \)` by auto hence "T0 = A" using xty unique_var_typing by auto hence "\ T0' <: A1" using A asub by auto from X1 X2 X3 show ?thesis using T_AppPredTrue[OF X1 X2 X3 `\ T0' <: A1` E] using asub E eq by auto qed lemma subst_produces_FF: assumes ty:"(x,T0)#\ \ e : T ; TE S x" and vty:"\ \ v : T0' ; F" and A:"\ T0' <: T0" and B:"valid ((x,T0)#\)" and C:"closed v" and D:"v : values" and E:"~ \ T0' <: S" shows "EX T'. \ \ e[x::=v] : T' ; FF \ \ T' <: T" proof - obtain f A A1 Fn Sa B where eq:"e = App f (Var x)" and fty:"(x, T0) # \ \ f : B ; Fn " and bsub:" \ B <: A1 \ T : Latent S " and xty:" (x, T0) # \ \ Var x : A ; VE x " and asub:" \ A <: A1" using te_ty_elim[OF ty] by auto note preserve_subst[OF fty vty A B C D] then obtain T' F' where X1:"\ \ f[x::=v] : T' ; F' " and " \ T' <: B "" \ F' T' <: A1 \ T : Latent S" using bsub by auto have veq:"(Var x)[x::=v] = v" by simp hence X3:"\ \ (Var x)[x::=v] : T0' ; F" using vty by auto have "(x, T0) # \ \ Var x : T0 ; VE x" using `valid ((x, T0) # \)` by auto hence "T0 = A" using xty unique_var_typing by auto hence "\ T0' <: A1" using A asub by auto from X1 X2 X3 show ?thesis using T_AppPredFalse[OF X1 X2 X3 `\ T0' <: A1` E] using asub E eq C D veq by auto qed inductive_cases beta_cases:"App (Abs x b T) v \ e " inductive_cases beta_TT_cases:"\ \ App (Abs x b T) v : T' ; TT" inductive_cases beta_FF_cases:"\ \ App (Abs x b T) v : T' ; FF" lemma preserve_red: assumes typed:"\ \ e : t ; eff" and cl:"closed e" and red:"e \ e'" and val:"valid \" shows "EX t' eff'. \ \ e' : t' ; eff' \ \ t' <: t \ \ eff' t rule: reduce.strong_induct) case (e_delta v' p v \ T) thm app_ty_elim[of \ "(BI p)" v' T eff] hence "\T0 T0' T1 le eff' eff'' U. \ \ BI p : U ; eff' \ \ \ v' : T0' ; eff'' \ \ U <: T0 \ T1 : le \ \ T0' <: T0 \ T1 = T" using app_ty_elim[of \ "(BI p)" v' T eff] by simp then obtain T0 T0' T1 le eff' eff'' U where A1:" \ \ BI p : U ; eff'" and A2:"\ \ v' : T0' ; eff''" and A3:"\ T0' <: T0" and A4:"T1 = T" and A5:"\ U <: T0 \ T1 : le" by auto hence "U = \\<^isub>\ p" using e_delta typing_bi[of \ p _ eff'] by simp then obtain A0 A1 LA where "\\<^isub>\ p = A0 \ A1 : LA" "U = A0 \ A1 : LA" by (nominal_induct p rule: builtin.induct) auto hence "\ A0 \ A1 : LA <: T0 \ T1 : le" using `\ U <: T0 \ T1 : le` by auto hence B:"le = LA \ le = latent_eff.NE" "\ T0 <: A0" "\ A1 <: T1" using arr_sub_arr_cases[of A0 A1 LA T0 T1 le] by auto have C1:" \ \ App (BI p) v' : T1 ; eff" using prems `T1 = T` by auto have C2:"\ T0' <: A0" and C3:"\ A1 <: T " using B A3 A4 by auto have C4:"valid \" . note delta_soundness[OF `\\<^isub>\ p = A0 \ A1 : LA` `v' : values` `\ \ v' : T0' ; eff''` C2 e_delta(3) C3 `\ p v' = Some v` C4] then obtain A1' eff' where "\ \ v : A1' ; eff' "" \ eff' A1' <: A1" by auto thus ?case using C3 by auto next case (e_if_false thn els \' t') have "eff = NE" using if_false_ty_elim[of _ _ _ _ eff] e_if_false by auto have " \T0 eff'. \' \ els : T0 ; eff' \ \ T0 <: t' " using if_false_ty_elim[of \' thn els t' eff] e_if_false by auto then obtain T0 eff' where f:"\' \ els : T0 ; eff'" and g:"\ T0 <: t'" by auto have "closed els" using e_if_false closed_def trm.supp by auto hence "simple_eff eff'" using closed_eff f by auto hence h:"\ eff' ' t') have "eff = NE" using if_true_ty_elim[of \' v thn els _ eff] e_if_true by auto have " \T0 eff'. \' \ thn : T0 ; eff' \ \ T0 <: t' " using if_true_ty_elim[of \' v thn els t' eff] e_if_true by auto then obtain T0 eff' where f:"\' \ thn : T0 ; eff'" and g:"\ T0 <: t'" by auto have "closed thn" using e_if_true closed_def trm.supp by auto hence "simple_eff eff'" using closed_eff f by auto hence h:"\ eff' ' T') hence "simple_eff eff" using closed_eff by auto thm app_ty_elim[of \' "(Lam[x:T].b)" v t eff] (* hence "eff = NE" using app_abs_ty_elim_eff by auto *) from e_beta have "\T0 T0' T1 le eff' eff'' U. \' \ Abs x b T : U ; eff' \ \' \ v : T0' ; eff'' \ \ T0' <: T0 \ T1 = T' \ \ U <: T0 \ T1 : le" using app_ty_elim[of \' "Abs x b T" v T' eff] by blast then obtain T0 T0' T1 le eff' eff'' U where " \' \ Lam[x:T].b :U; eff'" and "\' \ v : T0' ; eff''" and "\ T0' <: T0" and "T1 = T'" and usub:"\ U <: T0 \ T1 : le " by auto hence "\T1a eff2 L S. (x,T)#\' \ b : T1a ; eff2 \ U = T \ T1a : L \ (L = Latent S \ eff2 = TE S x \ L = latent_eff.NE)" using abs_ty_elim[of \' x b T "U" eff'] e_beta `x \ \'` by auto then obtain T1a eff2 L S where bty:"(x,T)#\' \ b : T1a ; eff2" and ueq:"U = T \ T1a : L" and "(L = Latent S \ eff2 = TE S x \ L = latent_eff.NE)" by auto have "closed v" using e_beta closed_def trm.supp by auto have "v : values" using e_beta beta_cases[of _ _ _ v _ "v : values"] trm.inject by auto have "\ T0 <: T" using usub ueq arr_sub_arr_cases[of T T1a L T0 T1 le] by auto have "\ T1a <: T1" using usub ueq arr_sub_arr_cases[of T T1a L T0 T1 le] by auto hence "\ T1a <: T'" using `T1 = T'` by simp have "\ T0' <: T" using ` \ T0' <: T0` `\T0<:T` by auto have " \T'a F'. \' \ b[x::=v] : T'a ; F' \ \ T'a <: T1a" using preserve_subst[of x T \' b T1a eff2 v T0' eff''] `\' \ v : T0' ; eff''` bty `\ T0' <: T` `x \ \'` `valid \'` `closed v` `v : values` by auto then obtain T'a F' where a:"\' \ b[x::=v] : T'a ; F'" and b:"\ T'a <: T1a" by auto have "closed (b[x::=v])" using e_beta reduce_closed by blast hence c:"simple_eff F'" using a closed_eff by auto have ?case using `simple_eff eff` e_beta a b proof (induct eff rule: simple_eff_cases) case NE thus ?case using simple_eff_below_ne[of F'] c a b `\ T1a <: T'` by auto next case TT obtain U T0 Ta S eff1 eff2 where X1:"\' \ (Lam [x:T].b) : U ; eff1 " and X2:"\ U <: T0 \ T' : Latent S" and X3:" \' \ v : Ta ; eff2 " "\ Ta <: T0"" \ Ta <: S" using trm.inject beta_TT_cases[OF TT(5), of thesis] by auto note abs_ty_elim[OF X1 `x \ \'`] then obtain T1' eff' L S' where f: "(x, T) # \' \ b : T1' ; eff' " " U = T \ T1' : L " " eff1 = eff.TT " " (eff' = TE S' x \ L = Latent S' \ L = latent_eff.NE)" by auto hence "eff' = TE S x" "\ T0 <: T" "\ T1' <: T'"using `U = T \ T1' : L` X2 using arr_sub_arr_cases[of T T1' L T0 T' "Latent S"] by auto hence X4:"(x, T) # \' \ b : T1' ; TE S x" using f by auto have valcons:"valid ((x,T)#\')" using `valid \'` `x \ \'` by auto have "\ Ta <: T" using `\ Ta <: T0``\ T0 <: T` by auto have "EX T2'. \' \ b[x::=v] : T2' ; TT \ \ T2' <: T1'" using X3 using subst_produces_TT[OF X4 `\' \ v : Ta ; eff2` `\ Ta <: T` valcons ` closed v`` v \ values` `\ Ta <: S`] by auto thus ?case using `\ T1' <: T'` by auto next case FF obtain U T0 Ta S eff1 eff2 where X1:"\' \ (Lam [x:T].b) : U ; eff1 " and X2:"\ U <: T0 \ T' : Latent S" and X3:" \' \ v : Ta ; eff2 " "\ Ta <: T0""~ \ Ta <: S" using trm.inject beta_FF_cases[OF FF(5), of thesis] by auto note abs_ty_elim[OF X1 `x \ \'`] then obtain T1' eff' L S' where f: "(x, T) # \' \ b : T1' ; eff' " " U = T \ T1' : L " " eff1 = eff.TT " " (eff' = TE S' x \ L = Latent S' \ L = latent_eff.NE)" by auto hence "eff' = TE S x" "\ T0 <: T" "\ T1' <: T'" using `U = T \ T1' : L` X2 using arr_sub_arr_cases[of T T1' L T0 T' "Latent S"] by auto hence X4:"(x, T) # \' \ b : T1' ; TE S x" using f by auto have valcons:"valid ((x,T)#\')" using `valid \'` `x \ \'` by auto have "\ Ta <: T" using `\ Ta <: T0``\ T0 <: T` by auto hence "EX T2'. \' \ b[x::=v] : T2' ; FF \ \ T2' <: T1'" using X3 using subst_produces_FF[OF X4 `\' \ v : Ta ; eff2` `\ Ta <: T` valcons ` closed v`` v \ values` _] by auto thus ?case using `\ T1' <: T'` by auto qed thus ?case . qed lemma value_no_ctxt: assumes "v : values" and "v = E t" and "E : ctxt" shows "E = (% t . t)" using prems proof (induct) case bi_value show ?case using `E : ctxt` bi_value by (induct E rule: ctxt.induct) (auto simp add: trm.inject) next case num_value show ?case using `E : ctxt` num_value by (induct E rule: ctxt.induct) (auto simp add: trm.inject) next case abs_value show ?case using `E : ctxt` abs_value by (induct E rule: ctxt.induct) (auto simp add: trm.inject) next case bool_value show ?case using `E : ctxt` bool_value by (induct E rule: ctxt.induct) (auto simp add: trm.inject) qed lemma subst_in_ctxt_preserves_type: assumes a:"\ \ u : T ; F" and b:"C : ctxt" and c:"u = C e" and "~ (e : values)" and "closed (C e)" and "closed (C e')" and "!! T0 F0 . \ \ e : T0 ; F0 \ EX T1 F1. \ \ e' : T1 ; F1 \ \ T1 <: T0 \ \ F1 \ C e' : S ; G \ \ S <: T \ \ G \ e : T ; F" using C_Hole by simp hence "EX S G. \ \ e' : S; G \ \ S <: T \ \ G \ App (E t) arg : T' ; F'" using C_App1 by auto hence D:"simple_eff F'" using C_App1 closed_eff by auto thus ?case using C_App1 A B C proof (induct rule: simple_eff_cases) case NE hence "EX T0 T0' T1 le eff' eff'' U. \ \ E t :U ; eff' \ \ \ arg : T0' ; eff'' \ \ U <: T0 \ T1 : le \ \ T0' <: T0 \ T1 = T'" using app_ty_elim by auto then obtain T0 T0' le eff' eff'' U where a:"\ \ E t : U ; eff'" and b:"\ \ arg : T0' ; eff''" and c:"\ T0' <: T0" and d:"\ U <: T0 \ T' : le" by auto have "\S G. \ \ E t' : S ; G \ \ S <: U \ \ G values` C_App1 by auto then obtain S G where et'ty:"\ \ E t' : S ; G " and subarr:" \ S <: U " and "\ G \ App (E t') arg : T' ; NE" using b c d by auto thus ?case by auto next case FF have "EX S T0 T0' le F1 F2 U. \ \ E t : U ; F1 \ \ \ arg : T0' ; F2 \ \ T0' <: T0 \ le = Latent S \ ~ (\ T0' <: S) \ arg : values \ closed arg \ \ U <: T0 \ T' : le" using `\ \ App (E t) arg : T' ; FF` app_ty_ff_elim[of \ "E t" arg T'] by blast then obtain S T0 T0' F1 F2 U where a:"\ \ E t :U ; F1" and b:"\ \ arg : T0' ; F2 " and c:"\ T0' <: T0 " and d:" ~ (\ T0' <: S)" "closed arg" "arg : values" " \ U <: T0 \ T' : Latent S" by auto have "\S' G. \ \ E t' : S' ; G \ \ S' <: U \ \ G \ E t' : S' ; G " and subarr:" \ S' <: U" and "\ G \ App (E t') arg : T' ; FF" using b c d by auto thus ?case by auto next case TT have "EX S T0 T0' le F1 F2 U. \ \ E t : U ; F1 \ \ \ arg : T0' ; F2 \ \ T0' <: T0 \ le = Latent S \ \ T0' <: S \ \ U <: T0 \ T' : le" using `\ \ App (E t) arg : T' ; TT` app_ty_tt_elim[of \ "E t" arg T'] by blast then obtain S T0 T0' F1 F2 U where a:"\ \ E t : U ; F1" and b:"\ \ arg : T0' ; F2 " and c:"\ T0' <: T0 " and d:"\ T0' <: S" "\ U <: T0 \ T' : Latent S" by auto have "\S' G. \ \ E t' : S' ; G \ \ S' <: U \ \ G \ E t' : S' ; G " and subarr:" \ S' <: U " and "\ G \ App (E t') arg : T' ; TT" using b c d by auto thus ?case by auto qed next case (C_App2 E v u' t t' T' F') have A:"closed (E t)" and B:"closed (E t')" using C_App2 closed_def trm.supp by auto have C:"\ \ App v (E t) : T' ; F'" using C_App2 by auto hence D:"simple_eff F'" using C_App2 closed_eff by auto thus ?case using C_App2 A B C proof (induct rule: simple_eff_cases) case NE have "\T0 T0' T1 le eff' eff'' U. \ \ v : U ; eff' \ \ \ E t : T0' ; eff'' \ \ T0' <: T0 \ T1 = T' \ \ U <: T0 \ T1 : le" using app_ty_elim[of \ v "E t" T' F'] `\ \ App v (E t) : T' ; F'` by blast then obtain T0 T0' le eff' eff'' U where a:"\ \ v : U ; eff'" " \ \ E t : T0' ; eff'' " "\ T0' <: T0" "\ U <: T0 \ T' : le" by auto hence "\S G. \ \ E t' : S ; G \ \ S <: T0' \ \ G \ E t' : S ; G "" \ S <: T0'" by auto hence "\ \ App v (E t') : T' ; eff.NE" using a `\ T0' <: T0` by auto thus ?case by auto next case FF have "\S T0 T0' le eff' eff'' U. \ \ v : U ; eff' \ \ \ E t : T0' ; eff'' \ \ T0' <: T0 \ le = Latent S \ ~ (\ T0' <: S) \ E t : values \ closed (E t) \ \ U <: T0 \ T' : le" using app_ty_ff_elim[of \ v "E t" T'] `\ \ App v (E t) : T' ; FF` by blast then obtain S T0 T0' le eff' eff'' U where "\ \ v : U ; eff' "" \ \ E t : T0' ; eff'' "" \ T0' <: T0 " " ~ (\ T0' <: S) " " E t : values "" closed (E t)" by auto hence "E = (% t. t)" using value_no_ctxt[of "E t" E t] `E : ctxt` by simp hence "t : values" using `E t : values` by simp thus ?case using `t \ values` by auto next case TT have "\S T0 T0' le eff' eff'' U. \ \ v : U ; eff' \ \ \ E t : T0' ; eff'' \ \ T0' <: T0 \ le = Latent S \ \ T0' <: S \ \ U <: T0 \ T' : le" using app_ty_tt_elim[of \ v "E t" T'] `\ \ App v (E t) : T' ; TT` by blast then obtain S T0 T0' le eff' eff'' U where a:"\ \ v : U ; eff' "" \ \ E t : T0' ; eff'' "" \ T0' <: T0 " " \ T0' <: S" "\ U <: T0 \ T' : Latent S" by auto hence "\S' G. \ \ E t' : S' ; G \ \ S' <: T0' \ \ G \ E t' : S' ; G "" \ S' <: T0'" by auto have "\ S' <: S" using ` \ S' <: T0'` `\ T0' <: S` by auto have "\ S' <: T0" using `\ S' <: T0'` `\ T0' <: T0` by auto hence "\ \ App v (E t') : T' ; TT" using b T_AppPredTrue[OF a(1) a(5) b(1) `\ S' <: T0` ] using `\ S' <: S` by auto thus ?case by auto qed next case (C_Iff E thn els u' t t' T' F') have A:"closed (E t)" and B:"closed (E t')" using C_Iff closed_def trm.supp by auto have C:"\ \ Iff (E t) thn els: T' ; F'" using C_Iff by auto hence bigor: "(\T1 T2 T3 F1 F2 F3. \ \ E t : T1 ; F1 \ \ |+ F1 \ thn : T2 ; F2 \ \ |- F1 \ els : T3 ; F3 \ \ T2 <: T' \ \ T3 <: T' \ F' = eff.NE) \ (\T1 T3 F3. \ \ E t : T1 ; FF \ \ \ els : T3 ; F3 \ \ T3 <: T' \ F' = eff.NE) \ (\T1 T2 F2. \ \ E t : T1 ; TT \ \ \ thn : T2 ; F2 \ \ T2 <: T' \ F' = eff.NE)" using if_ty_elim[of \ "(E t)" thn els T' F'] by auto thus ?case proof - { assume "(\T1 T2 T3 F1 F2 F3. \ \ E t : T1 ; F1 \ \ |+ F1 \ thn : T2 ; F2 \ \ |- F1 \ els : T3 ; F3 \ \ T2 <: T' \ \ T3 <: T' \ F' = eff.NE)" then obtain T1 T2 T3 F1 F2 F3 where P:"\ \ E t : T1 ; F1""\ |+ F1 \ thn : T2 ; F2""\ |- F1 \ els : T3 ; F3""\ T2 <: T'""\ T3 <: T'""F' = eff.NE" by auto have "closed (E t)" and "closed (E t')" using prems trm.supp closed_def by auto hence "EX T1' F1'. \ \ E t' : T1' ; F1' \ \ T1' <: T1 \ \ F1' \ E t' : T1' ; F1' "" \ T1' <: T1 "" \ F1' |+ F1 = \" "\ |- F1 = \" "\ |+ F1' = \" "\ |- F1' = \" by (auto simp add: env_plus_simple_eff) hence "\ |+ F1' \ thn : T2 ; F2 " "\ |- F1' \ els : T3 ; F3" using P by auto hence "\ \ Iff (E t') thn els : T'; comb_eff F1' F2 F3" using `\ \ E t' : T1' ; F1'` ` \ T2 <: T' `` \ T3 <: T'` by (auto simp del: comb_eff.simps) hence ?thesis using `F' = NE` by auto } moreover { assume "(\T1 T3 F3. \ \ E t : T1 ; FF \ \ \ els : T3 ; F3 \ \ T3 <: T' \ F' = eff.NE)" then obtain T1 T3 F3 where P:"\ \ E t : T1 ; FF "" \ \ els : T3 ; F3 "" \ T3 <: T'"" F' = eff.NE" by auto have "closed (E t)" and "closed (E t')" using prems trm.supp closed_def by auto hence "EX T1' F1'. \ \ E t' : T1' ; F1' \ \ T1' <: T1 \ \ F1' \ E t' : T1' ; F1' "" \ T1' <: T1 "" \ F1' \ E t' : T1' ; FF " using Q by auto hence ?thesis using P by auto } moreover { assume "(\T1 T2 F2. \ \ E t : T1 ; TT \ \ \ thn : T2 ; F2 \ \ T2 <: T' \ F' = eff.NE)" then obtain T1 T2 F2 where P:"\ \ E t : T1 ; TT "" \ \ thn : T2 ; F2 "" \ T2 <: T'"" F' = eff.NE" by auto have "closed (E t)" and "closed (E t')" using prems trm.supp closed_def by auto hence "EX T1' F1'. \ \ E t' : T1' ; F1' \ \ T1' <: T1 \ \ F1' \ E t' : T1' ; F1' "" \ T1' <: T1 "" \ F1' \ E t' : T1' ; TT " using Q by auto hence ?thesis using P by auto } ultimately show ?thesis using bigor by blast qed qed lemma typing_ctxt: assumes a:"\ \ C L : T ; eff" and b:"C : ctxt" shows "EX T' eff'. \ \ L : T' ; eff'" using b a proof(induct C arbitrary: T eff rule: ctxt.induct ) case C_Hole thus ?case by auto next case (C_App1 C' arg S) hence ih: "!! T0 eff. \ \ C' L : T0 ; eff \ \T' a. \ \ L : T' ; a" by simp obtain T0 T0' T1 le eff' eff'' U where "\ \ C' L : U ; eff'" "\ \ arg : T0' ; eff''" "\ T0' <: T0 \ T1 = S" "\ U <: T0 \ T1 : le" using app_ty_elim[of \ "C' L" arg S eff] ` \ \ App (C' L) arg : S ; eff` by blast thus ?case using ih by auto next case (C_App2 C' rator S F) hence ih: "!! T0 eff. \ \ C' L : T0 ; eff \ \T' a. \ \ L : T' ; a" by simp obtain T0 T0' T1 le eff' eff'' U where "\ \ rator : U ; eff'" "\ \ C' L : T0' ; eff''" "\ T0' <: T0 \ T1 = S" "\ U <: T0 \ T1 : le" using app_ty_elim[of \ rator "C' L" S F] ` \ \ App rator (C' L) : S ; F` by blast thus ?case using ih by auto next case (C_Iff C' thn els S F) hence ih: "!! T0 eff. \ \ C' L : T0 ; eff \ \T' a. \ \ L : T' ; a" by simp obtain T0 eff' where "\ \ C' L : T0 ; eff'" using if_ty_elim[of \ "C' L" thn els S F] ` \ \ Iff (C' L) thn els : S ; F` by auto thus ?case using ih by auto qed inductive_cases step_cases: "(e::trm) \ e'" inductive_cases bi_reduce:"BI b \ x" inductive_cases bool_reduce:"Bool b \ x" inductive_cases abs_reduce:"(Lam[a:T].b) \ x" inductive_cases num_reduce:"Num n \ x" lemma value_reduce_step: assumes A:"v : values" and B:"v \ (v'::trm)" shows "v \ v'" using B A proof(induct) fix E L R assume "E : ctxt" "L \ R" "E L \ values" hence "E L = L" and "E R = R" using value_no_ctxt by auto thus "E L \ E R" using prems by auto qed lemma value_not_step: assumes "v : values" shows "~ (EX v'. v \ v')" proof(rule ccontr, simp) assume "\v'. v \ v'" then obtain v' where A:"v \ v'" by auto show False using `v : values` A proof (induct v rule: values.induct) case (bi_value b) thus ?case using bi_reduce by auto next case num_value thus ?case using num_reduce by auto next case abs_value thus ?case using abs_reduce by blast next case bool_value thus ?case using bool_reduce by auto qed qed lemma value_not_reduce: fixes v v' :: trm assumes "v : values" shows "~ (EX v'. v \ v')" proof (rule ccontr) assume "\ \ (\v'. v \ v')" then obtain v' where "v \ v'" by auto hence A:"v \ v'" using value_reduce_step prems by auto show False using `v : values` A value_not_step by auto qed theorem preservation: fixes e e' :: trm assumes typed:"\ \ e : t ; eff" and cl:"closed e" and red:"e \ e'" shows "EX t' eff'. \ \ e' : t' ; eff' \ \ t' <: t \ \ eff' " using typing_valid typed by auto obtain C L R where "e = C L" "e' = C R" and "L \ R" and "C : ctxt" using red step_cases[of e e' thesis] by auto hence f:"EX T F. \ \ L : T ; F" using typed typing_ctxt by auto have "L \ values" using `L \ R` value_not_step by auto have "closed L" and "closed_ctxt C" using closed_in_ctxt_closed_ctxt[of e C L] `C : ctxt` cl `e = C L` by auto hence "closed R" using reduce_closed[of L R] `L \ R` by auto hence "closed (C R)" and "closed (C L)" using `closed_ctxt C` ctxt_closed[of C L] ctxt_closed[of C R] `closed L` by auto have " \T0 F0. \ \ L : T0 ; F0 \ \T1 F1. \ \ R : T1 ; F1 \ \ T1 <: T0 \ \ F1 \ L : T0 ; F0 \ (\T1 F1. \ \ R : T1 ; F1 \ \ T1 <: T0 \ \ F1 R` closed_in_ctxt[of C L] cl preserve_red[of \ L T0 F0 R] `closed L` val by auto qed hence "\S G. \ \ C R : S ; G \ \ S <: t \ \ G e t eff C L R] typed `e = C L` `closed (C L)` `closed (C R)` `L \ values`by auto thus ?thesis using `e' = C R` by auto qed text {* soundness *} lemma soundness_finite: fixes e e' e'' :: trm assumes A:"\ \ e : T ; F" and B:"e \\<^sup>* e'" and C:"~ (EX e''. e' \ e'')" and E:"closed e" shows "EX T' F'. (e' : values \ \ \ e' : T' ; F' \ \ T' <: T \ \ F' T F rule: step_multi.induct) case (sm_refl v) have "v : values" using sm_refl progress[of \ v T F] by auto thus ?case using sm_refl by auto next case (sm_trans a b c) have "closed b" "closed c" using `closed a` `b \\<^sup>* c` `a \ b` step_closed[of a b] multi_step_closed[of b c] by auto then obtain T' F' where 1:"\ \ b : T' ; F'" "\ T' <: T" "\ F' a T F b] sm_trans by auto then obtain T'' F'' where 2:"\ \ c : T'' ; F''" "\ T'' <: T'" "\ F'' T' F'] sm_trans `closed b` by blast have "\ T'' <: T" using 1 2 by auto have 3:"simple_eff F" using prems closed_eff by auto have 4:"simple_eff F'" using 1 prems closed_eff `closed b` by auto have 5:"simple_eff F''" using prems closed_eff `closed c` by auto from 3 4 5 have "\ F'' T'' <: T` by auto qed text {* interesting fact: let e = (Iff True 3 x) then [] \ e : Int ; NE but e is not closed *} theorem soundness: assumes A:"\ \ e : T ; F" and E:"closed e" shows "reduce_forever e \ (EX v T' F'. (v : values \ e \\<^sup>* v \ \ \ v : T' ; F' \ \ T' <: T \ \ F' \<^sup>* e') \ ~(EX e''. e' \ e'')" by (auto simp add: reduce_forever_def) then obtain e'::trm where B:"e \\<^sup>* e'" and C:"~ (EX e''. e' \ e'')" by auto hence ?thesis using soundness_finite[OF A B C E] by auto } moreover { assume "reduce_forever e" hence ?thesis by simp } ultimately show ?thesis by auto qed text {* simpler type system, without silly rules *} inductive typing2 :: "varEnv \ trm \ ty \ eff \ bool" (" _ \\<^isub>2 _ : _ ; _ " [60,60,60,60] 60) where T2_Var[intro]: "\valid \; (v,T)\set \\\ \ \\<^isub>2 Var v : T ; VE v" | T2_Const[intro]: "valid \ \ \\<^isub>\ b = T \ \ \\<^isub>2 (BI b) : T ; TT" | T2_Num[intro]: "valid \ \ \ \\<^isub>2 (Num n) : ty.Int ; TT" | T2_True[intro]: "valid \ \ \ \\<^isub>2 (Bool True) : ty.TT ; TT" | T2_False[intro]: "valid \ \ \ \\<^isub>2 (Bool False) : ty.FF ; FF" | T2_Abs[intro]: "\x \ \; ((x,T1)#\) \\<^isub>2 b : T2; eff\ \ \ \\<^isub>2 Lam [x:T1].b : (T1\T2 : latent_eff.NE) ; TT" | T2_App[intro]: "\\ \\<^isub>2 e1 : U ; eff1 ; \ U <: (T0 \ T1 : le); \ \\<^isub>2 e2 : T; eff2 ; \ T <: T0\ \ \ \\<^isub>2 App e1 e2 : T1 ; NE" | T2_AppPred[intro]: "\\ \\<^isub>2 e1 : U; eff1; \ U <: (T0 \ T1 : Latent S); \ \\<^isub>2 e2 : T; VE x ; \ T <: T0\ \ \ \\<^isub>2 App e1 e2 : T1 ; TE S x" | T2_If[intro]: "\\ \\<^isub>2 e1 : T1; eff1; (\ |+ eff1) \\<^isub>2 e2 : T2; eff2; (\ |- eff1) \\<^isub>2 e3 : T3; eff3; \ T2 <: T; \ T3 <: T\ \ \ \\<^isub>2 (Iff e1 e2 e3) : T ; comb_eff eff1 eff2 eff3" | T2_AbsPred[intro]: "\x \ \; ((x,T1)#\) \\<^isub>2 b : T2; TE S x\ \ \ \\<^isub>2 Lam [x:T1].b : (T1\T2 : Latent S) ; TT" lemma typing2_typing: assumes "\ \\<^isub>2 e : T ; F" shows "\ \ e : T ; F" using prems by induct (auto simp del: comb_eff.simps) lemma typing2_soundness1: assumes A:"\ \\<^isub>2 e : T ; F" and E:"closed e" shows "reduce_forever e \ (EX v T' F'. (v : values \ e \\<^sup>* v \ \ \ v : T' ; F' \ \ T' <: T \ \ F' \\<^isub>2 e : ty.Int ; F" and E:"closed e" shows "reduce_forever e \ (EX v F'. (v : values \ (e \\<^sup>* v) \ \ \\<^isub>2 v : ty.Int ; F' \ \ F' (EX v T' F'. (v : values \ (e \\<^sup>* v) \ \ \ v : T' ; F' \ \ T' <: ty.Int \ \ F' (e \\<^sup>* v) \ \ \ v : T' ; F' \ \ T' <: ty.Int \ \ F' \\<^isub>2 v : ty.Int ; F'" using num_ty_elim[of \ _ T' F'] `\ \ v : T' ; F'` by auto thus ?thesis using `\ F' \<^sup>* v)` by auto qed (auto) qed lemma typing2_soundness_help: assumes A:"\ \\<^isub>2 e : \ ; F" and E:"closed e" and B: "((\v T' F'. v \ values \ \ \ v : T' ; F' \ \ T' <: \ \ \ F' (reduce_forever e \ (\v F'. v \ values \ \ \\<^isub>2 v : \ ; F' \ \ F' (\v F'. v \ values \ \ \\<^isub>2 v : \ ; F' \ \ F' \\<^isub>2 e : T ; F" and E:"closed e" and sub:"\ T <: BoolTy" shows "reduce_forever e \ (EX v F' T'. (v : values \ (e \\<^sup>* v) \ \ \\<^isub>2 v : T' ; F' \ \ F' \ T' <: T))" proof - from typing2_soundness1[OF A E] have B:"reduce_forever e \ (EX v T' F'. (v : values \ (e \\<^sup>* v) \ \ \ v : T' ; F' \ \ T' <: T \ \ F' (e \\<^sup>* v) \ \ \ v : T' ; F' \ \ T' <: T \ \ F' \ v : T' ; F'`] sub by auto hence "\ \\<^isub>2 Bool b : T' ; F'" using `\ \ v : T' ; F'` true_ty_elim[of \ T' F'] false_ty_elim[of \ T' F'] by (cases b) auto thus ?thesis using `v = Bool b` `e \\<^sup>* v` `v : values` `\ F' T' <: T` by blast qed (auto) qed constdefs ground_type :: "ty \ bool" "ground_type t == t = ty.Int \ t = BoolTy \ t = ty.TT \ t = ty.FF" lemma supp_env: "(a,b) : set (\ :: varEnv) \ a : supp \" by (induct \) (auto simp add: supp_list_cons supp_prod supp_atm) lemma envop_supp: assumes "valid \" shows "x : (supp (envop f n t \)) \ x : (supp \ :: name set)" proof - assume A:"x : (supp (envop f n t \))" have "!! a. a \ (supp \ :: name set) \ a \ supp (envop f n t \)" proof - fix a show "a \ (supp \ :: name set) \ a \ supp (envop f n t \)" using fresh_def[of a "envop f n t \"] envop_fresh[OF _ `valid \`] fresh_def[of a \] by auto qed hence "(supp (envop f n t \)) <= (supp \ :: name set)" by blast thus ?thesis using A by auto qed declare envop_def[simp del] lemma envplus_supp: assumes "valid \" shows "(supp (\ |+ F) :: name set) <= (supp \ :: name set)" using prems apply (nominal_induct F rule: eff.induct) apply (auto simp add: envop_supp) done lemma envminus_supp: assumes "valid \" shows "(supp (\ |- F) :: name set) <= (supp \ :: name set)" using prems apply (nominal_induct F rule: eff.induct) apply (auto simp add: envop_supp) done lemma env_supp_typing2: assumes "\ \\<^isub>2 e : T ; F" shows "fv e <= supp \" using prems proof (induct \ e T F rule: typing2.induct) case T2_Var thus ?case by (auto simp add: trm.supp supp_atm supp_env) next case T2_App thus ?case by (auto simp add: trm.supp) next case T2_AppPred thus ?case by (auto simp add: trm.supp) next case (T2_If \ _ _ F) have "valid \" using typing_valid typing2_typing[OF T2_If(1)] by auto thus ?case using T2_If envminus_supp[OF `valid \`, of F] envplus_supp[OF `valid \`, of F] by (auto simp add: trm.supp) next case T2_Abs thus ?case by (auto simp add: trm.supp fv_lam abs_supp supp_list_cons supp_prod supp_latent_eff_ty supp_atm) next case T2_AbsPred thus ?case by (auto simp add: trm.supp fv_lam abs_supp supp_list_cons supp_prod supp_latent_eff_ty supp_atm) next case (T2_Const \ b) thus ?case by (nominal_induct b rule: builtin.induct) (auto simp add: trm.supp builtin.supp) qed (auto simp add: trm.supp supp_nat supp_bool) lemma empty_env_typing2_closed: assumes "[] \\<^isub>2 e : T ; F" shows "closed e" using env_supp_typing2[OF prems] closed_def prems supp_list_nil by auto theorem ground_type_soundness: assumes A:"[] \\<^isub>2 e : T ; F" and B:"ground_type T" shows "reduce_forever e \ (EX v T' F'. (v : values \ (e \\<^sup>* v) \ [] \\<^isub>2 v : T' ; F' \ \ T' <: T \ \ F' (EX v F'. (v : values \ (e \\<^sup>* v) \ [] \\<^isub>2 v : ty.Int ; F' \ \ F' T <: BoolTy" using B by (auto simp add: ground_type_def) hence "reduce_forever e \ (EX v F' T'. (v : values \ (e \\<^sup>* v) \ [] \\<^isub>2 v : T' ; F' \ \ F' \ T' <: T))" using typing2_soundness_bool[OF A E] by auto hence ?thesis using prems by auto } ultimately show ?thesis using B ground_type_def by auto qed end lemma unique_decomposition: assumes a:"closed e" shows "\E : ctxt; E t = e; E' : ctxt; E' t' = e\ \ E = E'" using a proof (nominal_induct e rule: trm.induct) case (Var v) have f1:"E = (%t. t)" using Var by cases auto have f2:"E'= (%t. t)" using `E' : ctxt` Var by cases auto from f1 f2 show ?case by simp next case (Bool c) have f1:"E = (%t. t)" using Bool by cases auto have f2:"E'= (%t. t)" using `E' : ctxt` Bool by cases auto from f1 f2 show ?case by simp next case (Num c) have f1:"E = (%t. t)" using Num by cases auto have f2:"E'= (%t. t)" using `E' : ctxt` Num by cases auto from f1 f2 show ?case by simp next case Abs have f1:"E = (%t. t)" using `E : ctxt` Abs by cases auto have f2:"E'= (%t. t)" using `E' : ctxt` Abs by cases auto from f1 f2 show ?case by simp next case (Iff tst thn els) { assume "tst \ values" hence "EX E L R. tst = E L \ E \ ctxt \ L \ R" using decomposition have f1:"E = (%t. t)" using `E : ctxt` Iff apply cases apply (auto simp add: trm.inject) have f2:"E'= (%t. t)" using `E' : ctxt` Iff by cases auto from f1 f2 have ?case by simp { oops lemma fresh_fact: fixes a::"name" assumes a: "a\t1" and b: "a\t2" shows "a\(t1[b::=t2])" using a b by (nominal_induct t1 avoiding: a b t2 rule: trm.induct) (auto simp add: abs_fresh fresh_atm) lemma id_subs: "t[x::=Var x] = t" by (nominal_induct t avoiding: x rule: trm.induct) (simp_all add: fresh_atm) lemma random_eqvt[simp]: fixes pi :: "name prm" shows "\T. T \ set Ts \ \ T <: S \ \ pi \ T <: pi \ S \ \T. T \ set (pi \ Ts) \ \ T <: pi \ S" proof - assume 0:"\T. T \ set Ts \ \ T <: S \ \ pi \ T <: pi \ S" hence 1:"!! T. T \ set Ts \ \ T <: S \ \ pi \ T <: pi \ S" by auto have A:"(pi \ Ts) = Ts" by (induct Ts) auto have B:"pi \ S = S" by auto have "!! T. T \ set (pi \ Ts) \ \ T <: pi \ S" proof - fix T assume "T \ set (pi \ Ts)" hence "T : set Ts" using A by auto hence "\ T <: S" using 1 by auto thus "\ T <: pi \ S" using B by auto qed thus ?thesis by auto qed text {* complete induction on typing derivations *} lemma typing_induct_complete[consumes 1, case_names T_Var T_Const T_Num T_True T_False T_App T_Lam T_AppPred T_If T_AppPredTrue T_AppPredFalse T_IfTrue T_IfFalse]: fixes P :: "'a::fs_name\(name\ty) list \ trm \ ty \ eff \ bool" and \ :: "(name\ty) list" and t :: "trm" and T :: "ty" and F :: "eff" and x :: "'a::fs_name" assumes a: "\ \ t : T ; F" and a1: "\\ (a::name) \ x. valid \ \ (a,\) \ set \ \ (!! x t T \ F. (t\Var a) \ \ \ t : T ; F \ P x \ t T F) \ valid \ \ P x \ (Var a) \ (VE a)" and a2: "!! \ b T x. \\<^isub>\ b = T \ (!! x t T \ F. (t\BI b) \ \ \ t : T ; F \ P x \ t T F) \ valid \ \ P x \ (BI b) T NE" and a3: "!! \ n x. (!! x t T \ F. (t\Num n) \ \ \ t : T ; F \ P x \ t T F) \ valid \ \ P x \ (Num n) ty.Int NE" and a4: "!! \ x. (!! x t T \ F. (t\Bool True) \ \ \ t : T ; F \ P x \ t T F) \ valid \ \ P x \ (Bool True) BoolTy TT" and a5: "!! \ x. (!! x t T \ F. (t\Bool False) \ \ \ t : T ; F \ P x \ t T F) \ valid \ \ P x \ (Bool False) BoolTy FF" and a6: "\\ \ \ t1 t2 x F1 F2 le \0 U. (!! x t T \ F. (t\App t1 t2) \ \ \ t : T ; F \ P x \ t T F) \ \ \ t1 : U ; F1 \ \ U <: \\\:le \ (\z. P z \ t1 U F1) \ \ \ t2 : \0 ; F2 \ (\z. P z \ t2 \0 F2) \ \ \0 <: \ \ P x \ (App t1 t2) \ NE" and a7: "\a \ \ \ t x F0. a\x \ a\\ \ ((a,\) # \) \ t : \ ; F0 \ (\z. P z ((a,\)#\) t \ F0) \ (!! x t' T \ F. (t'\Lam[a:\].t) \ \ \ t' : T ; F \ P x \ t' T F) \ P x \ (Lam [a:\].t) (\\\:latent_eff.NE) NE" and a8: "\\ \ \ t1 t2 x F1 \0 S v U. (!! x t T \ F. t \ App t1 t2 \ \ \ t : T ; F \ P x \ t T F) \ \ \ t1 : U ; F1 \ \ U <: (\\\:Latent S) \ (\z. P z \ t1 U F1) \ \ \ t2 : \0 ; VE v \ (\z. P z \ t2 \0 (VE v)) \ \ \0 <: \ \ P x \ (App t1 t2) \ (TE S v)" and a9: "!! \ e1 e2 e3 T1 T2 T3 T eff1 eff2 eff3 x. \\ \ e1 : T1; eff1; !!z. P z \ e1 T1 eff1; (\ |+ eff1) \ e2 : T2; eff2; !!z. P z (\|+ eff1) e2 T2 eff2; (!! x t T \ F. t \ Iff e1 e2 e3 \ \ \ t : T ; F \ P x \ t T F); (\ |- eff1) \ e3 : T3; eff3; !!z. P z (\|- eff1) e3 T3 eff3; \ T2 <: T; \ T3 <: T\ \ P x \ (Iff e1 e2 e3) T NE" and a10: "!! \ e1 e2 T0 T1 T S eff1 eff2 x U. \\ \ e1 : U; eff1; \ U <: (T0 \ T1 : Latent S) ; !!z. P z \ e1 U eff1; (!! x t T \ F. t \ App e1 e2 \ \ \ t : T ; F \ P x \ t T F); \ \ e2 : T; eff2 ; !! z. P z \ e2 T eff2; \ T <: T0; \ T <: S\ \ P x \ (App e1 e2) T1 TT" and a11: "!! \ e1 e2 T0 T1 T S eff1 eff2 x U. \\ \ e1 : U; eff1; \ U <: (T0 \ T1 : Latent S) ; !!z. P z \ e1 U eff1; (!! x t T \ F. t \ App e1 e2 \ \ \ t : T ; F \ P x \ t T F); \ \ e2 : T; eff2 ; !! z. P z \ e2 T eff2; \ T <: T0; ~(\ T <: S) ; e2 : values ; closed e2\ \ P x \ (App e1 e2) T1 FF" and a12: "!! \ e1 e2 e3 T T1 T2 eff x. \\ \ e1 : T1 ; TT ; !! z. P z \ e1 T1 TT; (!! x t T \ F. t \ Iff e1 e2 e3 \ \ \ t : T ; F \ P x \ t T F); \ \ e2 : T2 ; eff; !!z .P z \ e2 T2 eff; \ T2 <: T\ \ P x \ (Iff e1 e2 e3) T NE" and a13: "!! \ e1 e2 e3 T T1 T3 eff x. \\ \ e1 : T1 ; FF ; !! z. P z \ e1 T1 FF; (!! x t T \ F. t \ Iff e1 e2 e3 \ \ \ t : T ; F \ P x \ t T F); \ \ e3 : T3 ; eff; !!z .P z \ e3 T3 eff; \ T3 <: T\ \ P x \ (Iff e1 e2 e3) T NE" shows "P x \ t T F" using a proof (nominal_induct t avoiding: x \ T F rule: trm_comp_induct) case (Var v) thus ?case using a1 var_ty_elim[of \ v T F] by auto next case (App t1 t2 x \ T) show ?case using App(4) proof (induct rule: app_ty_elim2) case 1 thus ?thesis using a6 App trm.inject ty.inject by auto next case 2 thus ?thesis using a8 App trm.inject ty.inject by auto next case 3 thus ?thesis using a10 App trm.inject ty.inject by auto next case 4 thus ?thesis using a11 App trm.inject ty.inject by auto qed next case Iff show ?case using Iff(5) proof (induct rule: iff_ty_elim2) case 1 thus ?thesis using a9 Iff trm.inject ty.inject by auto next case 2 thus ?thesis using a12 Iff trm.inject ty.inject by auto next case 3 thus ?thesis using a13 Iff trm.inject ty.inject by auto qed next case (Lam v b x \ S1 F S2) show ?case using Lam abs_ty_elim[of \ v b S2 S1 F] a7 by (auto simp add: trm.inject ty.inject) next case (BI b) thus ?case using bi_ty_elim[of \ b T F] trm.inject a2 by auto next case (Num n) thus ?case using num_ty_elim[of \ n T F] trm.inject a3 by auto next case (Bool b) thus ?case using true_ty_elim[of \ T F] false_ty_elim[of \ T F] trm.inject a4 a5 by (cases b) auto qed