diff --git a/src/HOL/Nominal/Examples/Fsub.thy b/src/HOL/Nominal/Examples/Fsub.thy --- a/src/HOL/Nominal/Examples/Fsub.thy +++ b/src/HOL/Nominal/Examples/Fsub.thy @@ -1,1886 +1,1853 @@ (*<*) theory Fsub imports "HOL-Nominal.Nominal" begin (*>*) text\Authors: Christian Urban, Benjamin Pierce, Dimitrios Vytiniotis Stephanie Weirich Steve Zdancewic Julien Narboux Stefan Berghofer with great help from Markus Wenzel.\ section \Types for Names, Nominal Datatype Declaration for Types and Terms\ no_syntax "_Map" :: "maplets => 'a \ 'b" ("(1[_])") text \The main point of this solution is to use names everywhere (be they bound, binding or free). In System \FSUB{} there are two kinds of names corresponding to type-variables and to term-variables. These two kinds of names are represented in the nominal datatype package as atom-types \tyvrs\ and \vrs\:\ atom_decl tyvrs vrs text\There are numerous facts that come with this declaration: for example that there are infinitely many elements in \tyvrs\ and \vrs\.\ text\The constructors for types and terms in System \FSUB{} contain abstractions over type-variables and term-variables. The nominal datatype package uses \\\\\\ to indicate where abstractions occur.\ nominal_datatype ty = Tvar "tyvrs" | Top | Arrow "ty" "ty" (infixr "\" 200) | Forall "\tyvrs\ty" "ty" nominal_datatype trm = Var "vrs" | Abs "\vrs\trm" "ty" | TAbs "\tyvrs\trm" "ty" | App "trm" "trm" (infixl "\" 200) | TApp "trm" "ty" (infixl "\\<^sub>\" 200) text \To be polite to the eye, some more familiar notation is introduced. Because of the change in the order of arguments, one needs to use translation rules, instead of syntax annotations at the term-constructors as given above for \<^term>\Arrow\.\ abbreviation Forall_syn :: "tyvrs \ ty \ ty \ ty" ("(3\_<:_./ _)" [0, 0, 10] 10) where "\X<:T\<^sub>1. T\<^sub>2 \ ty.Forall X T\<^sub>2 T\<^sub>1" abbreviation Abs_syn :: "vrs \ ty \ trm \ trm" ("(3\_:_./ _)" [0, 0, 10] 10) where "\x:T. t \ trm.Abs x t T" abbreviation TAbs_syn :: "tyvrs \ ty \ trm \ trm" ("(3\_<:_./ _)" [0, 0, 10] 10) where "\X<:T. t \ trm.TAbs X t T" text \Again there are numerous facts that are proved automatically for \<^typ>\ty\ and \<^typ>\trm\: for example that the set of free variables, i.e.~the \support\, is finite. However note that nominal-datatype declarations do \emph{not} define ``classical" constructor-based datatypes, but rather define $\alpha$-equivalence classes---we can for example show that $\alpha$-equivalent \<^typ>\ty\s and \<^typ>\trm\s are equal:\ lemma alpha_illustration: shows "(\X<:T. Tvar X) = (\Y<:T. Tvar Y)" and "(\x:T. Var x) = (\y:T. Var y)" by (simp_all add: ty.inject trm.inject alpha calc_atm fresh_atm) section \SubTyping Contexts\ nominal_datatype binding = VarB vrs ty | TVarB tyvrs ty type_synonym env = "binding list" text \Typing contexts are represented as lists that ``grow" on the left; we thereby deviating from the convention in the POPLmark-paper. The lists contain pairs of type-variables and types (this is sufficient for Part 1A).\ text \In order to state validity-conditions for typing-contexts, the notion of a \dom\ of a typing-context is handy.\ nominal_primrec "tyvrs_of" :: "binding \ tyvrs set" where "tyvrs_of (VarB x y) = {}" | "tyvrs_of (TVarB x y) = {x}" by auto nominal_primrec "vrs_of" :: "binding \ vrs set" where "vrs_of (VarB x y) = {x}" | "vrs_of (TVarB x y) = {}" by auto primrec "ty_dom" :: "env \ tyvrs set" where "ty_dom [] = {}" | "ty_dom (X#\) = (tyvrs_of X)\(ty_dom \)" primrec "trm_dom" :: "env \ vrs set" where "trm_dom [] = {}" | "trm_dom (X#\) = (vrs_of X)\(trm_dom \)" lemma vrs_of_eqvt[eqvt]: fixes pi ::"tyvrs prm" and pi'::"vrs prm" shows "pi \(tyvrs_of x) = tyvrs_of (pi\x)" and "pi'\(tyvrs_of x) = tyvrs_of (pi'\x)" and "pi \(vrs_of x) = vrs_of (pi\x)" and "pi'\(vrs_of x) = vrs_of (pi'\x)" by (nominal_induct x rule: binding.strong_induct) (simp_all add: tyvrs_of.simps eqvts) lemma doms_eqvt[eqvt]: fixes pi::"tyvrs prm" and pi'::"vrs prm" shows "pi \(ty_dom \) = ty_dom (pi\\)" and "pi'\(ty_dom \) = ty_dom (pi'\\)" and "pi \(trm_dom \) = trm_dom (pi\\)" and "pi'\(trm_dom \) = trm_dom (pi'\\)" by (induct \) (simp_all add: eqvts) lemma finite_vrs: shows "finite (tyvrs_of x)" and "finite (vrs_of x)" by (nominal_induct rule:binding.strong_induct) auto lemma finite_doms: shows "finite (ty_dom \)" and "finite (trm_dom \)" -by (induct \) (auto simp add: finite_vrs) +by (induct \) (auto simp: finite_vrs) lemma ty_dom_supp: shows "(supp (ty_dom \)) = (ty_dom \)" and "(supp (trm_dom \)) = (trm_dom \)" by (simp only: at_fin_set_supp at_tyvrs_inst at_vrs_inst finite_doms)+ lemma ty_dom_inclusion: assumes a: "(TVarB X T)\set \" shows "X\(ty_dom \)" using a by (induct \) (auto) lemma ty_binding_existence: assumes "X \ (tyvrs_of a)" shows "\T.(TVarB X T=a)" using assms by (nominal_induct a rule: binding.strong_induct) (auto) lemma ty_dom_existence: assumes a: "X\(ty_dom \)" shows "\T.(TVarB X T)\set \" using a - apply (induct \, auto) - apply (rename_tac a \') - apply (subgoal_tac "\T.(TVarB X T=a)") - apply (auto) - apply (auto simp add: ty_binding_existence) -done +proof (induction \) + case Nil then show ?case by simp +next + case (Cons a \) then show ?case + using ty_binding_existence by fastforce +qed lemma doms_append: shows "ty_dom (\@\) = ((ty_dom \) \ (ty_dom \))" and "trm_dom (\@\) = ((trm_dom \) \ (trm_dom \))" by (induct \) (auto) lemma ty_vrs_prm_simp: fixes pi::"vrs prm" and S::"ty" shows "pi\S = S" -by (induct S rule: ty.induct) (auto simp add: calc_atm) +by (induct S rule: ty.induct) (auto simp: calc_atm) lemma fresh_ty_dom_cons: fixes X::"tyvrs" shows "X\(ty_dom (Y#\)) = (X\(tyvrs_of Y) \ X\(ty_dom \))" - apply (nominal_induct rule:binding.strong_induct) - apply (auto) - apply (simp add: fresh_def supp_def eqvts) - apply (simp add: fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_doms) - apply (simp add: fresh_def supp_def eqvts) - apply (simp add: fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_doms)+ - done +proof (nominal_induct rule:binding.strong_induct) + case (VarB vrs ty) + then show ?case by auto +next + case (TVarB tyvrs ty) + then show ?case + by (simp add: at_fin_set_supp at_tyvrs_inst finite_doms(1) fresh_def supp_atm(1)) +qed lemma tyvrs_fresh: fixes X::"tyvrs" assumes "X \ a" shows "X \ tyvrs_of a" and "X \ vrs_of a" using assms - apply (nominal_induct a rule:binding.strong_induct) - apply (auto) - apply (fresh_guess)+ -done + by (nominal_induct a rule:binding.strong_induct) (force simp: fresh_singleton)+ lemma fresh_dom: fixes X::"tyvrs" assumes a: "X\\" shows "X\(ty_dom \)" using a -apply(induct \) -apply(simp add: fresh_set_empty) -apply(simp only: fresh_ty_dom_cons) -apply(auto simp add: fresh_prod fresh_list_cons tyvrs_fresh) -done +proof (induct \) + case Nil then show ?case by auto +next + case (Cons a \) then show ?case + by (meson fresh_list_cons fresh_ty_dom_cons tyvrs_fresh(1)) +qed text \Not all lists of type \<^typ>\env\ are well-formed. One condition requires that in \<^term>\TVarB X S#\\ all free variables of \<^term>\S\ must be in the \<^term>\ty_dom\ of \<^term>\\\, that is \<^term>\S\ must be \closed\ in \<^term>\\\. The set of free variables of \<^term>\S\ is the \support\ of \<^term>\S\.\ definition "closed_in" :: "ty \ env \ bool" ("_ closed'_in _" [100,100] 100) where "S closed_in \ \ (supp S)\(ty_dom \)" lemma closed_in_eqvt[eqvt]: fixes pi::"tyvrs prm" assumes a: "S closed_in \" shows "(pi\S) closed_in (pi\\)" using a proof - from a have "pi\(S closed_in \)" by (simp add: perm_bool) then show "(pi\S) closed_in (pi\\)" by (simp add: closed_in_def eqvts) qed lemma tyvrs_vrs_prm_simp: fixes pi::"vrs prm" shows "tyvrs_of (pi\a) = tyvrs_of a" - apply (nominal_induct rule:binding.strong_induct) - apply (simp_all add: eqvts) - apply (simp add: dj_perm_forget[OF dj_tyvrs_vrs]) - done + by (nominal_induct rule:binding.strong_induct) (auto simp: vrs_prm_tyvrs_def) lemma ty_vrs_fresh: fixes x::"vrs" and T::"ty" shows "x \ T" by (simp add: fresh_def supp_def ty_vrs_prm_simp) lemma ty_dom_vrs_prm_simp: fixes pi::"vrs prm" and \::"env" shows "(ty_dom (pi\\)) = (ty_dom \)" - apply(induct \) - apply (simp add: eqvts) - apply(simp add: tyvrs_vrs_prm_simp) -done +by (induct \) (auto simp: tyvrs_vrs_prm_simp) lemma closed_in_eqvt'[eqvt]: fixes pi::"vrs prm" assumes a: "S closed_in \" shows "(pi\S) closed_in (pi\\)" -using a -by (simp add: closed_in_def ty_dom_vrs_prm_simp ty_vrs_prm_simp) + using assms closed_in_def ty_dom_vrs_prm_simp ty_vrs_prm_simp by force lemma fresh_vrs_of: fixes x::"vrs" shows "x\vrs_of b = x\b" by (nominal_induct b rule: binding.strong_induct) (simp_all add: fresh_singleton fresh_set_empty ty_vrs_fresh fresh_atm) lemma fresh_trm_dom: fixes x::"vrs" shows "x\ trm_dom \ = x\\" by (induct \) - (simp_all add: fresh_set_empty fresh_list_cons + (simp_all add: fresh_list_cons fresh_fin_union [OF pt_vrs_inst at_vrs_inst fs_vrs_inst] - finite_doms finite_vrs fresh_vrs_of fresh_list_nil) + finite_doms finite_vrs fresh_vrs_of) lemma closed_in_fresh: "(X::tyvrs) \ ty_dom \ \ T closed_in \ \ X \ T" - by (auto simp add: closed_in_def fresh_def ty_dom_supp) + by (auto simp: closed_in_def fresh_def ty_dom_supp) text \Now validity of a context is a straightforward inductive definition.\ inductive valid_rel :: "env \ bool" ("\ _ ok" [100] 100) where valid_nil[simp]: "\ [] ok" | valid_consT[simp]: "\\ \ ok; X\(ty_dom \); T closed_in \\ \ \ (TVarB X T#\) ok" | valid_cons [simp]: "\\ \ ok; x\(trm_dom \); T closed_in \\ \ \ (VarB x T#\) ok" equivariance valid_rel declare binding.inject [simp add] declare trm.inject [simp add] inductive_cases validE[elim]: "\ (TVarB X T#\) ok" "\ (VarB x T#\) ok" "\ (b#\) ok" declare binding.inject [simp del] declare trm.inject [simp del] lemma validE_append: assumes a: "\ (\@\) ok" shows "\ \ ok" using a proof (induct \) case (Cons a \') then show ?case - by (nominal_induct a rule:binding.strong_induct) - (auto elim: validE) + by (nominal_induct a rule:binding.strong_induct) auto qed (auto) lemma replace_type: assumes a: "\ (\@(TVarB X T)#\) ok" and b: "S closed_in \" shows "\ (\@(TVarB X S)#\) ok" using a b proof(induct \) case Nil - then show ?case by (auto elim: validE intro: valid_cons simp add: doms_append closed_in_def) + then show ?case by (auto intro: valid_cons simp add: doms_append closed_in_def) next case (Cons a \') then show ?case by (nominal_induct a rule:binding.strong_induct) - (auto elim: validE intro!: valid_cons simp add: doms_append closed_in_def) + (auto intro!: valid_cons simp add: doms_append closed_in_def) qed text \Well-formed contexts have a unique type-binding for a type-variable.\ lemma uniqueness_of_ctxt: fixes \::"env" assumes a: "\ \ ok" and b: "(TVarB X T)\set \" and c: "(TVarB X S)\set \" shows "T=S" using a b c proof (induct) case (valid_consT \ X' T') moreover { fix \'::"env" assume a: "X'\(ty_dom \')" have "\(\T.(TVarB X' T)\(set \'))" using a proof (induct \') case (Cons Y \') thus "\ (\T.(TVarB X' T)\set(Y#\'))" by (simp add: fresh_ty_dom_cons fresh_fin_union[OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_vrs finite_doms, - auto simp add: fresh_atm fresh_singleton) + auto simp: fresh_atm fresh_singleton) qed (simp) } - ultimately show "T=S" by (auto simp add: binding.inject) + ultimately show "T=S" by (auto simp: binding.inject) qed (auto) lemma uniqueness_of_ctxt': fixes \::"env" assumes a: "\ \ ok" and b: "(VarB x T)\set \" and c: "(VarB x S)\set \" shows "T=S" using a b c proof (induct) case (valid_cons \ x' T') moreover { fix \'::"env" assume a: "x'\(trm_dom \')" have "\(\T.(VarB x' T)\(set \'))" using a proof (induct \') case (Cons y \') thus "\ (\T.(VarB x' T)\set(y#\'))" by (simp add: fresh_fin_union[OF pt_vrs_inst at_vrs_inst fs_vrs_inst] finite_vrs finite_doms, - auto simp add: fresh_atm fresh_singleton) + auto simp: fresh_atm fresh_singleton) qed (simp) } - ultimately show "T=S" by (auto simp add: binding.inject) + ultimately show "T=S" by (auto simp: binding.inject) qed (auto) section \Size and Capture-Avoiding Substitution for Types\ nominal_primrec size_ty :: "ty \ nat" where "size_ty (Tvar X) = 1" | "size_ty (Top) = 1" | "size_ty (T1 \ T2) = (size_ty T1) + (size_ty T2) + 1" | "X \ T1 \ size_ty (\X<:T1. T2) = (size_ty T1) + (size_ty T2) + 1" - apply (finite_guess)+ - apply (rule TrueI)+ - apply (simp add: fresh_nat) - apply (fresh_guess)+ - done + by (finite_guess | fresh_guess | simp)+ nominal_primrec subst_ty :: "ty \ tyvrs \ ty \ ty" ("_[_ \ _]\<^sub>\" [300, 0, 0] 300) where "(Tvar X)[Y \ T]\<^sub>\ = (if X=Y then T else Tvar X)" | "(Top)[Y \ T]\<^sub>\ = Top" | "(T\<^sub>1 \ T\<^sub>2)[Y \ T]\<^sub>\ = T\<^sub>1[Y \ T]\<^sub>\ \ T\<^sub>2[Y \ T]\<^sub>\" | "X\(Y,T,T\<^sub>1) \ (\X<:T\<^sub>1. T\<^sub>2)[Y \ T]\<^sub>\ = (\X<:T\<^sub>1[Y \ T]\<^sub>\. T\<^sub>2[Y \ T]\<^sub>\)" - apply (finite_guess)+ - apply (rule TrueI)+ - apply (simp add: abs_fresh) - apply (fresh_guess)+ - done + by (finite_guess | fresh_guess | simp add: abs_fresh)+ lemma subst_eqvt[eqvt]: fixes pi::"tyvrs prm" and T::"ty" shows "pi\(T[X \ T']\<^sub>\) = (pi\T)[(pi\X) \ (pi\T')]\<^sub>\" by (nominal_induct T avoiding: X T' rule: ty.strong_induct) (perm_simp add: fresh_bij)+ lemma subst_eqvt'[eqvt]: fixes pi::"vrs prm" and T::"ty" shows "pi\(T[X \ T']\<^sub>\) = (pi\T)[(pi\X) \ (pi\T')]\<^sub>\" by (nominal_induct T avoiding: X T' rule: ty.strong_induct) (perm_simp add: fresh_left)+ lemma type_subst_fresh: fixes X::"tyvrs" assumes "X\T" and "X\P" shows "X\T[Y \ P]\<^sub>\" -using assms -by (nominal_induct T avoiding: X Y P rule:ty.strong_induct) - (auto simp add: abs_fresh) + using assms + by (nominal_induct T avoiding: X Y P rule:ty.strong_induct) + (auto simp: abs_fresh) lemma fresh_type_subst_fresh: - assumes "X\T'" - shows "X\T[X \ T']\<^sub>\" -using assms -by (nominal_induct T avoiding: X T' rule: ty.strong_induct) - (auto simp add: fresh_atm abs_fresh fresh_nat) + assumes "X\T'" + shows "X\T[X \ T']\<^sub>\" + using assms + by (nominal_induct T avoiding: X T' rule: ty.strong_induct) + (auto simp: fresh_atm abs_fresh) lemma type_subst_identity: "X\T \ T[X \ U]\<^sub>\ = T" by (nominal_induct T avoiding: X U rule: ty.strong_induct) (simp_all add: fresh_atm abs_fresh) lemma type_substitution_lemma: "X \ Y \ X\L \ M[X \ N]\<^sub>\[Y \ L]\<^sub>\ = M[Y \ L]\<^sub>\[X \ N[Y \ L]\<^sub>\]\<^sub>\" by (nominal_induct M avoiding: X Y N L rule: ty.strong_induct) - (auto simp add: type_subst_fresh type_subst_identity) + (auto simp: type_subst_fresh type_subst_identity) lemma type_subst_rename: "Y\T \ ([(Y,X)]\T)[Y \ U]\<^sub>\ = T[X \ U]\<^sub>\" by (nominal_induct T avoiding: X Y U rule: ty.strong_induct) (simp_all add: fresh_atm calc_atm abs_fresh fresh_aux) nominal_primrec subst_tyb :: "binding \ tyvrs \ ty \ binding" ("_[_ \ _]\<^sub>b" [100,100,100] 100) where "(TVarB X U)[Y \ T]\<^sub>b = TVarB X (U[Y \ T]\<^sub>\)" | "(VarB X U)[Y \ T]\<^sub>b = VarB X (U[Y \ T]\<^sub>\)" by auto lemma binding_subst_fresh: fixes X::"tyvrs" assumes "X\a" and "X\P" shows "X\a[Y \ P]\<^sub>b" using assms by (nominal_induct a rule: binding.strong_induct) - (auto simp add: type_subst_fresh) + (auto simp: type_subst_fresh) lemma binding_subst_identity: shows "X\B \ B[X \ U]\<^sub>b = B" by (induct B rule: binding.induct) (simp_all add: fresh_atm type_subst_identity) primrec subst_tyc :: "env \ tyvrs \ ty \ env" ("_[_ \ _]\<^sub>e" [100,100,100] 100) where "([])[Y \ T]\<^sub>e= []" | "(B#\)[Y \ T]\<^sub>e = (B[Y \ T]\<^sub>b)#(\[Y \ T]\<^sub>e)" lemma ctxt_subst_fresh': fixes X::"tyvrs" assumes "X\\" and "X\P" shows "X\\[Y \ P]\<^sub>e" using assms by (induct \) - (auto simp add: fresh_list_cons binding_subst_fresh) + (auto simp: fresh_list_cons binding_subst_fresh) lemma ctxt_subst_mem_TVarB: "TVarB X T \ set \ \ TVarB X (T[Y \ U]\<^sub>\) \ set (\[Y \ U]\<^sub>e)" by (induct \) auto lemma ctxt_subst_mem_VarB: "VarB x T \ set \ \ VarB x (T[Y \ U]\<^sub>\) \ set (\[Y \ U]\<^sub>e)" by (induct \) auto lemma ctxt_subst_identity: "X\\ \ \[X \ U]\<^sub>e = \" by (induct \) (simp_all add: fresh_list_cons binding_subst_identity) lemma ctxt_subst_append: "(\ @ \)[X \ T]\<^sub>e = \[X \ T]\<^sub>e @ \[X \ T]\<^sub>e" by (induct \) simp_all nominal_primrec subst_trm :: "trm \ vrs \ trm \ trm" ("_[_ \ _]" [300, 0, 0] 300) where "(Var x)[y \ t'] = (if x=y then t' else (Var x))" | "(t1 \ t2)[y \ t'] = t1[y \ t'] \ t2[y \ t']" | "(t \\<^sub>\ T)[y \ t'] = t[y \ t'] \\<^sub>\ T" | "X\(T,t') \ (\X<:T. t)[y \ t'] = (\X<:T. t[y \ t'])" | "x\(y,t') \ (\x:T. t)[y \ t'] = (\x:T. t[y \ t'])" apply(finite_guess)+ apply(rule TrueI)+ apply(simp add: abs_fresh)+ apply(fresh_guess add: ty_vrs_fresh abs_fresh)+ done lemma subst_trm_fresh_tyvar: fixes X::"tyvrs" shows "X\t \ X\u \ X\t[x \ u]" by (nominal_induct t avoiding: x u rule: trm.strong_induct) - (auto simp add: trm.fresh abs_fresh) + (auto simp: abs_fresh) lemma subst_trm_fresh_var: "x\u \ x\t[x \ u]" by (nominal_induct t avoiding: x u rule: trm.strong_induct) (simp_all add: abs_fresh fresh_atm ty_vrs_fresh) lemma subst_trm_eqvt[eqvt]: fixes pi::"tyvrs prm" and t::"trm" shows "pi\(t[x \ u]) = (pi\t)[(pi\x) \ (pi\u)]" by (nominal_induct t avoiding: x u rule: trm.strong_induct) (perm_simp add: fresh_left)+ lemma subst_trm_eqvt'[eqvt]: fixes pi::"vrs prm" and t::"trm" shows "pi\(t[x \ u]) = (pi\t)[(pi\x) \ (pi\u)]" by (nominal_induct t avoiding: x u rule: trm.strong_induct) (perm_simp add: fresh_left)+ lemma subst_trm_rename: "y\t \ ([(y, x)] \ t)[y \ u] = t[x \ u]" by (nominal_induct t avoiding: x y u rule: trm.strong_induct) (simp_all add: fresh_atm calc_atm abs_fresh fresh_aux ty_vrs_fresh perm_fresh_fresh) nominal_primrec (freshness_context: "T2::ty") subst_trm_ty :: "trm \ tyvrs \ ty \ trm" ("_[_ \\<^sub>\ _]" [300, 0, 0] 300) where "(Var x)[Y \\<^sub>\ T2] = Var x" | "(t1 \ t2)[Y \\<^sub>\ T2] = t1[Y \\<^sub>\ T2] \ t2[Y \\<^sub>\ T2]" | "(t1 \\<^sub>\ T)[Y \\<^sub>\ T2] = t1[Y \\<^sub>\ T2] \\<^sub>\ T[Y \ T2]\<^sub>\" | "X\(Y,T,T2) \ (\X<:T. t)[Y \\<^sub>\ T2] = (\X<:T[Y \ T2]\<^sub>\. t[Y \\<^sub>\ T2])" | "(\x:T. t)[Y \\<^sub>\ T2] = (\x:T[Y \ T2]\<^sub>\. t[Y \\<^sub>\ T2])" -apply(finite_guess)+ -apply(rule TrueI)+ -apply(simp add: abs_fresh ty_vrs_fresh)+ -apply(simp add: type_subst_fresh) +apply(finite_guess | simp add: abs_fresh ty_vrs_fresh type_subst_fresh)+ apply(fresh_guess add: ty_vrs_fresh abs_fresh)+ done lemma subst_trm_ty_fresh: fixes X::"tyvrs" shows "X\t \ X\T \ X\t[Y \\<^sub>\ T]" by (nominal_induct t avoiding: Y T rule: trm.strong_induct) - (auto simp add: abs_fresh type_subst_fresh) + (auto simp: abs_fresh type_subst_fresh) lemma subst_trm_ty_fresh': "X\T \ X\t[X \\<^sub>\ T]" by (nominal_induct t avoiding: X T rule: trm.strong_induct) (simp_all add: abs_fresh fresh_type_subst_fresh fresh_atm) lemma subst_trm_ty_eqvt[eqvt]: fixes pi::"tyvrs prm" and t::"trm" shows "pi\(t[X \\<^sub>\ T]) = (pi\t)[(pi\X) \\<^sub>\ (pi\T)]" by (nominal_induct t avoiding: X T rule: trm.strong_induct) (perm_simp add: fresh_bij subst_eqvt)+ lemma subst_trm_ty_eqvt'[eqvt]: fixes pi::"vrs prm" and t::"trm" shows "pi\(t[X \\<^sub>\ T]) = (pi\t)[(pi\X) \\<^sub>\ (pi\T)]" by (nominal_induct t avoiding: X T rule: trm.strong_induct) (perm_simp add: fresh_left subst_eqvt')+ lemma subst_trm_ty_rename: "Y\t \ ([(Y, X)] \ t)[Y \\<^sub>\ U] = t[X \\<^sub>\ U]" by (nominal_induct t avoiding: X Y U rule: trm.strong_induct) (simp_all add: fresh_atm calc_atm abs_fresh fresh_aux type_subst_rename) section \Subtyping-Relation\ text \The definition for the subtyping-relation follows quite closely what is written in the POPLmark-paper, except for the premises dealing with well-formed contexts and the freshness constraint \<^term>\X\\\ in the \S_Forall\-rule. (The freshness constraint is specific to the \emph{nominal approach}. Note, however, that the constraint does \emph{not} make the subtyping-relation ``partial"\ldots because we work over $\alpha$-equivalence classes.)\ inductive subtype_of :: "env \ ty \ ty \ bool" ("_\_<:_" [100,100,100] 100) where SA_Top[intro]: "\\ \ ok; S closed_in \\ \ \ \ S <: Top" | SA_refl_TVar[intro]: "\\ \ ok; X \ ty_dom \\\ \ \ Tvar X <: Tvar X" | SA_trans_TVar[intro]: "\(TVarB X S) \ set \; \ \ S <: T\ \ \ \ (Tvar X) <: T" | SA_arrow[intro]: "\\ \ T\<^sub>1 <: S\<^sub>1; \ \ S\<^sub>2 <: T\<^sub>2\ \ \ \ (S\<^sub>1 \ S\<^sub>2) <: (T\<^sub>1 \ T\<^sub>2)" | SA_all[intro]: "\\ \ T\<^sub>1 <: S\<^sub>1; ((TVarB X T\<^sub>1)#\) \ S\<^sub>2 <: T\<^sub>2\ \ \ \ (\X<:S\<^sub>1. S\<^sub>2) <: (\X<:T\<^sub>1. T\<^sub>2)" lemma subtype_implies_ok: fixes X::"tyvrs" assumes a: "\ \ S <: T" shows "\ \ ok" using a by (induct) (auto) lemma subtype_implies_closed: assumes a: "\ \ S <: T" shows "S closed_in \ \ T closed_in \" using a proof (induct) case (SA_Top \ S) have "Top closed_in \" by (simp add: closed_in_def ty.supp) moreover have "S closed_in \" by fact ultimately show "S closed_in \ \ Top closed_in \" by simp next case (SA_trans_TVar X S \ T) have "(TVarB X S)\set \" by fact hence "X \ ty_dom \" by (rule ty_dom_inclusion) hence "(Tvar X) closed_in \" by (simp add: closed_in_def ty.supp supp_atm) moreover have "S closed_in \ \ T closed_in \" by fact hence "T closed_in \" by force ultimately show "(Tvar X) closed_in \ \ T closed_in \" by simp -qed (auto simp add: closed_in_def ty.supp supp_atm abs_supp) +qed (auto simp: closed_in_def ty.supp supp_atm abs_supp) lemma subtype_implies_fresh: fixes X::"tyvrs" assumes a1: "\ \ S <: T" and a2: "X\\" shows "X\S \ X\T" proof - from a1 have "\ \ ok" by (rule subtype_implies_ok) with a2 have "X\ty_dom(\)" by (simp add: fresh_dom) moreover from a1 have "S closed_in \ \ T closed_in \" by (rule subtype_implies_closed) hence "supp S \ ((supp (ty_dom \))::tyvrs set)" and "supp T \ ((supp (ty_dom \))::tyvrs set)" by (simp_all add: ty_dom_supp closed_in_def) - ultimately show "X\S \ X\T" by (force simp add: supp_prod fresh_def) + ultimately show "X\S \ X\T" by (force simp: supp_prod fresh_def) qed lemma valid_ty_dom_fresh: fixes X::"tyvrs" assumes valid: "\ \ ok" shows "X\(ty_dom \) = X\\" using valid - apply induct - apply (simp add: fresh_list_nil fresh_set_empty) - apply (simp_all add: binding.fresh fresh_list_cons - fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_doms fresh_atm) - apply (auto simp add: closed_in_fresh) - done +proof induct + case valid_nil + then show ?case by auto +next + case (valid_consT \ X T) + then show ?case + by (auto simp: fresh_list_cons closed_in_fresh + fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_doms) +next + case (valid_cons \ x T) + then show ?case + using fresh_atm by (auto simp: fresh_list_cons closed_in_fresh) +qed equivariance subtype_of nominal_inductive subtype_of apply (simp_all add: abs_fresh) - apply (fastforce simp add: valid_ty_dom_fresh dest: subtype_implies_ok) - apply (force simp add: closed_in_fresh dest: subtype_implies_closed subtype_implies_ok)+ + apply (fastforce simp: valid_ty_dom_fresh dest: subtype_implies_ok) + apply (force simp: closed_in_fresh dest: subtype_implies_closed subtype_implies_ok)+ done section \Reflexivity of Subtyping\ lemma subtype_reflexivity: assumes a: "\ \ ok" and b: "T closed_in \" shows "\ \ T <: T" using a b proof(nominal_induct T avoiding: \ rule: ty.strong_induct) case (Forall X T\<^sub>1 T\<^sub>2) have ih_T\<^sub>1: "\\. \\ \ ok; T\<^sub>1 closed_in \\ \ \ \ T\<^sub>1 <: T\<^sub>1" by fact have ih_T\<^sub>2: "\\. \\ \ ok; T\<^sub>2 closed_in \\ \ \ \ T\<^sub>2 <: T\<^sub>2" by fact have fresh_cond: "X\\" by fact hence fresh_ty_dom: "X\(ty_dom \)" by (simp add: fresh_dom) have "(\X<:T\<^sub>2. T\<^sub>1) closed_in \" by fact hence closed\<^sub>T2: "T\<^sub>2 closed_in \" and closed\<^sub>T1: "T\<^sub>1 closed_in ((TVarB X T\<^sub>2)#\)" - by (auto simp add: closed_in_def ty.supp abs_supp) + by (auto simp: closed_in_def ty.supp abs_supp) have ok: "\ \ ok" by fact hence ok': "\ ((TVarB X T\<^sub>2)#\) ok" using closed\<^sub>T2 fresh_ty_dom by simp have "\ \ T\<^sub>2 <: T\<^sub>2" using ih_T\<^sub>2 closed\<^sub>T2 ok by simp moreover have "((TVarB X T\<^sub>2)#\) \ T\<^sub>1 <: T\<^sub>1" using ih_T\<^sub>1 closed\<^sub>T1 ok' by simp ultimately show "\ \ (\X<:T\<^sub>2. T\<^sub>1) <: (\X<:T\<^sub>2. T\<^sub>1)" using fresh_cond by (simp add: subtype_of.SA_all) -qed (auto simp add: closed_in_def ty.supp supp_atm) +qed (auto simp: closed_in_def ty.supp supp_atm) lemma subtype_reflexivity_semiautomated: assumes a: "\ \ ok" and b: "T closed_in \" shows "\ \ T <: T" using a b apply(nominal_induct T avoiding: \ rule: ty.strong_induct) -apply(auto simp add: ty.supp abs_supp supp_atm closed_in_def) +apply(auto simp: ty.supp abs_supp supp_atm closed_in_def) \ \Too bad that this instantiation cannot be found automatically by \isakeyword{auto}; \isakeyword{blast} would find it if we had not used an explicit definition for \closed_in_def\.\ apply(drule_tac x="(TVarB tyvrs ty2)#\" in meta_spec) apply(force dest: fresh_dom simp add: closed_in_def) done section \Weakening\ text \In order to prove weakening we introduce the notion of a type-context extending another. This generalization seems to make the proof for weakening to be smoother than if we had strictly adhered to the version in the POPLmark-paper.\ definition extends :: "env \ env \ bool" ("_ extends _" [100,100] 100) where "\ extends \ \ \X Q. (TVarB X Q)\set \ \ (TVarB X Q)\set \" lemma extends_ty_dom: - assumes a: "\ extends \" + assumes "\ extends \" shows "ty_dom \ \ ty_dom \" - using a - apply (auto simp add: extends_def) - apply (drule ty_dom_existence) - apply (force simp add: ty_dom_inclusion) - done + using assms + by (meson extends_def subsetI ty_dom_existence ty_dom_inclusion) lemma extends_closed: - assumes a1: "T closed_in \" - and a2: "\ extends \" + assumes "T closed_in \" and "\ extends \" shows "T closed_in \" - using a1 a2 - by (auto dest: extends_ty_dom simp add: closed_in_def) + by (meson assms closed_in_def extends_ty_dom order.trans) lemma extends_memb: assumes a: "\ extends \" and b: "(TVarB X T) \ set \" shows "(TVarB X T) \ set \" using a b by (simp add: extends_def) lemma weakening: assumes a: "\ \ S <: T" and b: "\ \ ok" and c: "\ extends \" shows "\ \ S <: T" using a b c proof (nominal_induct \ S T avoiding: \ rule: subtype_of.strong_induct) case (SA_Top \ S) have lh_drv_prem: "S closed_in \" by fact have "\ \ ok" by fact moreover have "\ extends \" by fact hence "S closed_in \" using lh_drv_prem by (simp only: extends_closed) ultimately show "\ \ S <: Top" by force next case (SA_trans_TVar X S \ T) have lh_drv_prem: "(TVarB X S) \ set \" by fact have ih: "\\. \ \ ok \ \ extends \ \ \ \ S <: T" by fact have ok: "\ \ ok" by fact have extends: "\ extends \" by fact have "(TVarB X S) \ set \" using lh_drv_prem extends by (simp only: extends_memb) moreover have "\ \ S <: T" using ok extends ih by simp ultimately show "\ \ Tvar X <: T" using ok by force next case (SA_refl_TVar \ X) have lh_drv_prem: "X \ ty_dom \" by fact have "\ \ ok" by fact moreover have "\ extends \" by fact hence "X \ ty_dom \" using lh_drv_prem by (force dest: extends_ty_dom) ultimately show "\ \ Tvar X <: Tvar X" by force next case (SA_arrow \ T\<^sub>1 S\<^sub>1 S\<^sub>2 T\<^sub>2) thus "\ \ S\<^sub>1 \ S\<^sub>2 <: T\<^sub>1 \ T\<^sub>2" by blast next case (SA_all \ T\<^sub>1 S\<^sub>1 X S\<^sub>2 T\<^sub>2) have fresh_cond: "X\\" by fact hence fresh_dom: "X\(ty_dom \)" by (simp add: fresh_dom) have ih\<^sub>1: "\\. \ \ ok \ \ extends \ \ \ \ T\<^sub>1 <: S\<^sub>1" by fact have ih\<^sub>2: "\\. \ \ ok \ \ extends ((TVarB X T\<^sub>1)#\) \ \ \ S\<^sub>2 <: T\<^sub>2" by fact have lh_drv_prem: "\ \ T\<^sub>1 <: S\<^sub>1" by fact hence closed\<^sub>T1: "T\<^sub>1 closed_in \" by (simp add: subtype_implies_closed) have ok: "\ \ ok" by fact have ext: "\ extends \" by fact have "T\<^sub>1 closed_in \" using ext closed\<^sub>T1 by (simp only: extends_closed) hence "\ ((TVarB X T\<^sub>1)#\) ok" using fresh_dom ok by force moreover - have "((TVarB X T\<^sub>1)#\) extends ((TVarB X T\<^sub>1)#\)" using ext by (force simp add: extends_def) + have "((TVarB X T\<^sub>1)#\) extends ((TVarB X T\<^sub>1)#\)" using ext by (force simp: extends_def) ultimately have "((TVarB X T\<^sub>1)#\) \ S\<^sub>2 <: T\<^sub>2" using ih\<^sub>2 by simp moreover have "\ \ T\<^sub>1 <: S\<^sub>1" using ok ext ih\<^sub>1 by simp ultimately show "\ \ (\X<:S\<^sub>1. S\<^sub>2) <: (\X<:T\<^sub>1. T\<^sub>2)" using ok by (force intro: SA_all) qed text \In fact all ``non-binding" cases can be solved automatically:\ lemma weakening_more_automated: assumes a: "\ \ S <: T" and b: "\ \ ok" and c: "\ extends \" shows "\ \ S <: T" using a b c proof (nominal_induct \ S T avoiding: \ rule: subtype_of.strong_induct) case (SA_all \ T\<^sub>1 S\<^sub>1 X S\<^sub>2 T\<^sub>2) have fresh_cond: "X\\" by fact hence fresh_dom: "X\(ty_dom \)" by (simp add: fresh_dom) have ih\<^sub>1: "\\. \ \ ok \ \ extends \ \ \ \ T\<^sub>1 <: S\<^sub>1" by fact have ih\<^sub>2: "\\. \ \ ok \ \ extends ((TVarB X T\<^sub>1)#\) \ \ \ S\<^sub>2 <: T\<^sub>2" by fact have lh_drv_prem: "\ \ T\<^sub>1 <: S\<^sub>1" by fact hence closed\<^sub>T1: "T\<^sub>1 closed_in \" by (simp add: subtype_implies_closed) have ok: "\ \ ok" by fact have ext: "\ extends \" by fact have "T\<^sub>1 closed_in \" using ext closed\<^sub>T1 by (simp only: extends_closed) hence "\ ((TVarB X T\<^sub>1)#\) ok" using fresh_dom ok by force moreover - have "((TVarB X T\<^sub>1)#\) extends ((TVarB X T\<^sub>1)#\)" using ext by (force simp add: extends_def) + have "((TVarB X T\<^sub>1)#\) extends ((TVarB X T\<^sub>1)#\)" using ext by (force simp: extends_def) ultimately have "((TVarB X T\<^sub>1)#\) \ S\<^sub>2 <: T\<^sub>2" using ih\<^sub>2 by simp moreover have "\ \ T\<^sub>1 <: S\<^sub>1" using ok ext ih\<^sub>1 by simp ultimately show "\ \ (\X<:S\<^sub>1. S\<^sub>2) <: (\X<:T\<^sub>1. T\<^sub>2)" using ok by (force intro: SA_all) qed (blast intro: extends_closed extends_memb dest: extends_ty_dom)+ section \Transitivity and Narrowing\ text \Some inversion lemmas that are needed in the transitivity and narrowing proof.\ declare ty.inject [simp add] inductive_cases S_TopE: "\ \ Top <: T" inductive_cases S_ArrowE_left: "\ \ S\<^sub>1 \ S\<^sub>2 <: T" declare ty.inject [simp del] lemma S_ForallE_left: shows "\\ \ (\X<:S\<^sub>1. S\<^sub>2) <: T; X\\; X\S\<^sub>1; X\T\ \ T = Top \ (\T\<^sub>1 T\<^sub>2. T = (\X<:T\<^sub>1. T\<^sub>2) \ \ \ T\<^sub>1 <: S\<^sub>1 \ ((TVarB X T\<^sub>1)#\) \ S\<^sub>2 <: T\<^sub>2)" -apply(erule subtype_of.strong_cases[where X="X"]) -apply(auto simp add: abs_fresh ty.inject alpha) -done + using subtype_of.strong_cases[where X="X"] + by(force simp: abs_fresh ty.inject alpha) text \Next we prove the transitivity and narrowing for the subtyping-relation. The POPLmark-paper says the following: \begin{quote} \begin{lemma}[Transitivity and Narrowing] \ \begin{enumerate} \item If \<^term>\\ \ S<:Q\ and \<^term>\\ \ Q<:T\, then \<^term>\\ \ S<:T\. \item If \\,X<:Q,\ \ M<:N\ and \<^term>\\ \ P<:Q\ then \\,X<:P,\ \ M<:N\. \end{enumerate} \end{lemma} The two parts are proved simultaneously, by induction on the size of \<^term>\Q\. The argument for part (2) assumes that part (1) has been established already for the \<^term>\Q\ in question; part (1) uses part (2) only for strictly smaller \<^term>\Q\. \end{quote} For the induction on the size of \<^term>\Q\, we use the induction-rule \measure_induct_rule\: \begin{center} @{thm measure_induct_rule[of "size_ty",no_vars]} \end{center} That means in order to show a property \<^term>\P a\ for all \<^term>\a\, the induct-rule requires to prove that for all \<^term>\x\ \<^term>\P x\ holds using the assumption that for all \<^term>\y\ whose size is strictly smaller than that of \<^term>\x\ the property \<^term>\P y\ holds.\ lemma shows subtype_transitivity: "\\S<:Q \ \\Q<:T \ \\S<:T" and subtype_narrow: "(\@[(TVarB X Q)]@\)\M<:N \ \\P<:Q \ (\@[(TVarB X P)]@\)\M<:N" proof (induct Q arbitrary: \ S T \ X P M N taking: "size_ty" rule: measure_induct_rule) case (less Q) have IH_trans: "\Q' \ S T. \size_ty Q' < size_ty Q; \\S<:Q'; \\Q'<:T\ \ \\S<:T" by fact have IH_narrow: "\Q' \ \ X M N P. \size_ty Q' < size_ty Q; (\@[(TVarB X Q')]@\)\M<:N; \\P<:Q'\ \ (\@[(TVarB X P)]@\)\M<:N" by fact { fix \ S T have "\\ \ S <: Q; \ \ Q <: T\ \ \ \ S <: T" proof (induct \ S Q\Q rule: subtype_of.induct) case (SA_Top \ S) then have rh_drv: "\ \ Top <: T" by simp then have T_inst: "T = Top" by (auto elim: S_TopE) from \\ \ ok\ and \S closed_in \\ have "\ \ S <: Top" by auto then show "\ \ S <: T" using T_inst by simp next case (SA_trans_TVar Y U \) then have IH_inner: "\ \ U <: T" by simp have "(TVarB Y U) \ set \" by fact with IH_inner show "\ \ Tvar Y <: T" by auto next case (SA_refl_TVar \ X) then show "\ \ Tvar X <: T" by simp next case (SA_arrow \ Q\<^sub>1 S\<^sub>1 S\<^sub>2 Q\<^sub>2) then have rh_drv: "\ \ Q\<^sub>1 \ Q\<^sub>2 <: T" by simp from \Q\<^sub>1 \ Q\<^sub>2 = Q\ have Q\<^sub>12_less: "size_ty Q\<^sub>1 < size_ty Q" "size_ty Q\<^sub>2 < size_ty Q" by auto have lh_drv_prm\<^sub>1: "\ \ Q\<^sub>1 <: S\<^sub>1" by fact have lh_drv_prm\<^sub>2: "\ \ S\<^sub>2 <: Q\<^sub>2" by fact from rh_drv have "T=Top \ (\T\<^sub>1 T\<^sub>2. T=T\<^sub>1\T\<^sub>2 \ \\T\<^sub>1<:Q\<^sub>1 \ \\Q\<^sub>2<:T\<^sub>2)" by (auto elim: S_ArrowE_left) moreover have "S\<^sub>1 closed_in \" and "S\<^sub>2 closed_in \" using lh_drv_prm\<^sub>1 lh_drv_prm\<^sub>2 by (simp_all add: subtype_implies_closed) hence "(S\<^sub>1 \ S\<^sub>2) closed_in \" by (simp add: closed_in_def ty.supp) moreover have "\ \ ok" using rh_drv by (rule subtype_implies_ok) moreover { assume "\T\<^sub>1 T\<^sub>2. T = T\<^sub>1\T\<^sub>2 \ \ \ T\<^sub>1 <: Q\<^sub>1 \ \ \ Q\<^sub>2 <: T\<^sub>2" then obtain T\<^sub>1 T\<^sub>2 where T_inst: "T = T\<^sub>1 \ T\<^sub>2" and rh_drv_prm\<^sub>1: "\ \ T\<^sub>1 <: Q\<^sub>1" and rh_drv_prm\<^sub>2: "\ \ Q\<^sub>2 <: T\<^sub>2" by force from IH_trans[of "Q\<^sub>1"] have "\ \ T\<^sub>1 <: S\<^sub>1" using Q\<^sub>12_less rh_drv_prm\<^sub>1 lh_drv_prm\<^sub>1 by simp moreover from IH_trans[of "Q\<^sub>2"] have "\ \ S\<^sub>2 <: T\<^sub>2" using Q\<^sub>12_less rh_drv_prm\<^sub>2 lh_drv_prm\<^sub>2 by simp ultimately have "\ \ S\<^sub>1 \ S\<^sub>2 <: T\<^sub>1 \ T\<^sub>2" by auto then have "\ \ S\<^sub>1 \ S\<^sub>2 <: T" using T_inst by simp } ultimately show "\ \ S\<^sub>1 \ S\<^sub>2 <: T" by blast next case (SA_all \ Q\<^sub>1 S\<^sub>1 X S\<^sub>2 Q\<^sub>2) then have rh_drv: "\ \ (\X<:Q\<^sub>1. Q\<^sub>2) <: T" by simp have lh_drv_prm\<^sub>1: "\ \ Q\<^sub>1 <: S\<^sub>1" by fact have lh_drv_prm\<^sub>2: "((TVarB X Q\<^sub>1)#\) \ S\<^sub>2 <: Q\<^sub>2" by fact then have "X\\" by (force dest: subtype_implies_ok simp add: valid_ty_dom_fresh) then have fresh_cond: "X\\" "X\Q\<^sub>1" "X\T" using rh_drv lh_drv_prm\<^sub>1 by (simp_all add: subtype_implies_fresh) from rh_drv have "T = Top \ (\T\<^sub>1 T\<^sub>2. T = (\X<:T\<^sub>1. T\<^sub>2) \ \ \ T\<^sub>1 <: Q\<^sub>1 \ ((TVarB X T\<^sub>1)#\) \ Q\<^sub>2 <: T\<^sub>2)" using fresh_cond by (simp add: S_ForallE_left) moreover have "S\<^sub>1 closed_in \" and "S\<^sub>2 closed_in ((TVarB X Q\<^sub>1)#\)" using lh_drv_prm\<^sub>1 lh_drv_prm\<^sub>2 by (simp_all add: subtype_implies_closed) - then have "(\X<:S\<^sub>1. S\<^sub>2) closed_in \" by (force simp add: closed_in_def ty.supp abs_supp) + then have "(\X<:S\<^sub>1. S\<^sub>2) closed_in \" by (force simp: closed_in_def ty.supp abs_supp) moreover have "\ \ ok" using rh_drv by (rule subtype_implies_ok) moreover { assume "\T\<^sub>1 T\<^sub>2. T=(\X<:T\<^sub>1. T\<^sub>2) \ \\T\<^sub>1<:Q\<^sub>1 \ ((TVarB X T\<^sub>1)#\)\Q\<^sub>2<:T\<^sub>2" then obtain T\<^sub>1 T\<^sub>2 where T_inst: "T = (\X<:T\<^sub>1. T\<^sub>2)" and rh_drv_prm\<^sub>1: "\ \ T\<^sub>1 <: Q\<^sub>1" and rh_drv_prm\<^sub>2:"((TVarB X T\<^sub>1)#\) \ Q\<^sub>2 <: T\<^sub>2" by force have "(\X<:Q\<^sub>1. Q\<^sub>2) = Q" by fact then have Q\<^sub>12_less: "size_ty Q\<^sub>1 < size_ty Q" "size_ty Q\<^sub>2 < size_ty Q" using fresh_cond by auto from IH_trans[of "Q\<^sub>1"] have "\ \ T\<^sub>1 <: S\<^sub>1" using lh_drv_prm\<^sub>1 rh_drv_prm\<^sub>1 Q\<^sub>12_less by blast moreover from IH_narrow[of "Q\<^sub>1" "[]"] have "((TVarB X T\<^sub>1)#\) \ S\<^sub>2 <: Q\<^sub>2" using Q\<^sub>12_less lh_drv_prm\<^sub>2 rh_drv_prm\<^sub>1 by simp with IH_trans[of "Q\<^sub>2"] have "((TVarB X T\<^sub>1)#\) \ S\<^sub>2 <: T\<^sub>2" using Q\<^sub>12_less rh_drv_prm\<^sub>2 by simp ultimately have "\ \ (\X<:S\<^sub>1. S\<^sub>2) <: (\X<:T\<^sub>1. T\<^sub>2)" using fresh_cond by (simp add: subtype_of.SA_all) hence "\ \ (\X<:S\<^sub>1. S\<^sub>2) <: T" using T_inst by simp } ultimately show "\ \ (\X<:S\<^sub>1. S\<^sub>2) <: T" by blast qed } note transitivity_lemma = this { \ \The transitivity proof is now by the auxiliary lemma.\ case 1 from \\ \ S <: Q\ and \\ \ Q <: T\ show "\ \ S <: T" by (rule transitivity_lemma) next case 2 from \(\@[(TVarB X Q)]@\) \ M <: N\ and \\ \ P<:Q\ show "(\@[(TVarB X P)]@\) \ M <: N" proof (induct "\@[(TVarB X Q)]@\" M N arbitrary: \ X \ rule: subtype_of.induct) case (SA_Top S \ X \) from \\ \ P <: Q\ have "P closed_in \" by (simp add: subtype_implies_closed) with \\ (\@[(TVarB X Q)]@\) ok\ have "\ (\@[(TVarB X P)]@\) ok" by (simp add: replace_type) moreover from \S closed_in (\@[(TVarB X Q)]@\)\ have "S closed_in (\@[(TVarB X P)]@\)" by (simp add: closed_in_def doms_append) ultimately show "(\@[(TVarB X P)]@\) \ S <: Top" by (simp add: subtype_of.SA_Top) next case (SA_trans_TVar Y S N \ X \) then have IH_inner: "(\@[(TVarB X P)]@\) \ S <: N" and lh_drv_prm: "(TVarB Y S) \ set (\@[(TVarB X Q)]@\)" and rh_drv: "\ \ P<:Q" and ok\<^sub>Q: "\ (\@[(TVarB X Q)]@\) ok" by (simp_all add: subtype_implies_ok) then have ok\<^sub>P: "\ (\@[(TVarB X P)]@\) ok" by (simp add: subtype_implies_ok) show "(\@[(TVarB X P)]@\) \ Tvar Y <: N" proof (cases "X=Y") case False have "X\Y" by fact hence "(TVarB Y S)\set (\@[(TVarB X P)]@\)" using lh_drv_prm by (simp add:binding.inject) with IH_inner show "(\@[(TVarB X P)]@\) \ Tvar Y <: N" by (simp add: subtype_of.SA_trans_TVar) next case True have memb\<^sub>XQ: "(TVarB X Q)\set (\@[(TVarB X Q)]@\)" by simp have memb\<^sub>XP: "(TVarB X P)\set (\@[(TVarB X P)]@\)" by simp have eq: "X=Y" by fact hence "S=Q" using ok\<^sub>Q lh_drv_prm memb\<^sub>XQ by (simp only: uniqueness_of_ctxt) hence "(\@[(TVarB X P)]@\) \ Q <: N" using IH_inner by simp moreover have "(\@[(TVarB X P)]@\) extends \" by (simp add: extends_def) hence "(\@[(TVarB X P)]@\) \ P <: Q" using rh_drv ok\<^sub>P by (simp only: weakening) ultimately have "(\@[(TVarB X P)]@\) \ P <: N" by (simp add: transitivity_lemma) then show "(\@[(TVarB X P)]@\) \ Tvar Y <: N" using memb\<^sub>XP eq by auto qed next case (SA_refl_TVar Y \ X \) from \\ \ P <: Q\ have "P closed_in \" by (simp add: subtype_implies_closed) with \\ (\@[(TVarB X Q)]@\) ok\ have "\ (\@[(TVarB X P)]@\) ok" by (simp add: replace_type) moreover from \Y \ ty_dom (\@[(TVarB X Q)]@\)\ have "Y \ ty_dom (\@[(TVarB X P)]@\)" by (simp add: doms_append) ultimately show "(\@[(TVarB X P)]@\) \ Tvar Y <: Tvar Y" by (simp add: subtype_of.SA_refl_TVar) next case (SA_arrow S\<^sub>1 Q\<^sub>1 Q\<^sub>2 S\<^sub>2 \ X \) then show "(\@[(TVarB X P)]@\) \ Q\<^sub>1 \ Q\<^sub>2 <: S\<^sub>1 \ S\<^sub>2" by blast next case (SA_all T\<^sub>1 S\<^sub>1 Y S\<^sub>2 T\<^sub>2 \ X \) have IH_inner\<^sub>1: "(\@[(TVarB X P)]@\) \ T\<^sub>1 <: S\<^sub>1" and IH_inner\<^sub>2: "(((TVarB Y T\<^sub>1)#\)@[(TVarB X P)]@\) \ S\<^sub>2 <: T\<^sub>2" by (fastforce intro: SA_all)+ then show "(\@[(TVarB X P)]@\) \ (\Y<:S\<^sub>1. S\<^sub>2) <: (\Y<:T\<^sub>1. T\<^sub>2)" by auto qed } qed section \Typing\ inductive typing :: "env \ trm \ ty \ bool" ("_ \ _ : _" [60,60,60] 60) where T_Var[intro]: "\ VarB x T \ set \; \ \ ok \ \ \ \ Var x : T" | T_App[intro]: "\ \ \ t\<^sub>1 : T\<^sub>1 \ T\<^sub>2; \ \ t\<^sub>2 : T\<^sub>1 \ \ \ \ t\<^sub>1 \ t\<^sub>2 : T\<^sub>2" | T_Abs[intro]: "\ VarB x T\<^sub>1 # \ \ t\<^sub>2 : T\<^sub>2 \ \ \ \ (\x:T\<^sub>1. t\<^sub>2) : T\<^sub>1 \ T\<^sub>2" | T_Sub[intro]: "\ \ \ t : S; \ \ S <: T \ \ \ \ t : T" | T_TAbs[intro]:"\ TVarB X T\<^sub>1 # \ \ t\<^sub>2 : T\<^sub>2 \ \ \ \ (\X<:T\<^sub>1. t\<^sub>2) : (\X<:T\<^sub>1. T\<^sub>2)" | T_TApp[intro]:"\X\(\,t\<^sub>1,T\<^sub>2); \ \ t\<^sub>1 : (\X<:T\<^sub>11. T\<^sub>12); \ \ T\<^sub>2 <: T\<^sub>11\ \ \ \ t\<^sub>1 \\<^sub>\ T\<^sub>2 : (T\<^sub>12[X \ T\<^sub>2]\<^sub>\)" equivariance typing lemma better_T_TApp: assumes H1: "\ \ t\<^sub>1 : (\X<:T11. T12)" and H2: "\ \ T2 <: T11" shows "\ \ t\<^sub>1 \\<^sub>\ T2 : (T12[X \ T2]\<^sub>\)" proof - obtain Y::tyvrs where Y: "Y \ (X, T12, \, t\<^sub>1, T2)" by (rule exists_fresh) (rule fin_supp) then have "Y \ (\, t\<^sub>1, T2)" by simp moreover from Y have "(\X<:T11. T12) = (\Y<:T11. [(Y, X)] \ T12)" - by (auto simp add: ty.inject alpha' fresh_prod fresh_atm) + by (auto simp: ty.inject alpha' fresh_prod fresh_atm) with H1 have "\ \ t\<^sub>1 : (\Y<:T11. [(Y, X)] \ T12)" by simp ultimately have "\ \ t\<^sub>1 \\<^sub>\ T2 : (([(Y, X)] \ T12)[Y \ T2]\<^sub>\)" using H2 by (rule T_TApp) with Y show ?thesis by (simp add: type_subst_rename) qed lemma typing_ok: assumes "\ \ t : T" shows "\ \ ok" using assms by (induct) (auto) nominal_inductive typing by (auto dest!: typing_ok intro: closed_in_fresh fresh_dom type_subst_fresh simp: abs_fresh fresh_type_subst_fresh ty_vrs_fresh valid_ty_dom_fresh fresh_trm_dom) lemma ok_imp_VarB_closed_in: assumes ok: "\ \ ok" shows "VarB x T \ set \ \ T closed_in \" using ok - by induct (auto simp add: binding.inject closed_in_def) + by induct (auto simp: binding.inject closed_in_def) lemma tyvrs_of_subst: "tyvrs_of (B[X \ T]\<^sub>b) = tyvrs_of B" by (nominal_induct B rule: binding.strong_induct) simp_all lemma ty_dom_subst: "ty_dom (\[X \ T]\<^sub>e) = ty_dom \" by (induct \) (simp_all add: tyvrs_of_subst) lemma vrs_of_subst: "vrs_of (B[X \ T]\<^sub>b) = vrs_of B" by (nominal_induct B rule: binding.strong_induct) simp_all lemma trm_dom_subst: "trm_dom (\[X \ T]\<^sub>e) = trm_dom \" by (induct \) (simp_all add: vrs_of_subst) lemma subst_closed_in: "T closed_in (\ @ TVarB X S # \) \ U closed_in \ \ T[X \ U]\<^sub>\ closed_in (\[X \ U]\<^sub>e @ \)" - apply (nominal_induct T avoiding: X U \ rule: ty.strong_induct) - apply (simp add: closed_in_def ty.supp supp_atm doms_append ty_dom_subst) - apply blast - apply (simp add: closed_in_def ty.supp) - apply (simp add: closed_in_def ty.supp) - apply (simp add: closed_in_def ty.supp abs_supp) - apply (drule_tac x = X in meta_spec) - apply (drule_tac x = U in meta_spec) - apply (drule_tac x = "(TVarB tyvrs ty2) # \" in meta_spec) - apply (simp add: doms_append ty_dom_subst) - apply blast - done +proof (nominal_induct T avoiding: X U \ rule: ty.strong_induct) + case (Tvar tyvrs) + then show ?case + by (auto simp add: closed_in_def ty.supp supp_atm doms_append ty_dom_subst) +next + case Top + then show ?case + using closed_in_def fresh_def by fastforce +next + case (Arrow ty1 ty2) + then show ?case + by (simp add: closed_in_def ty.supp) +next + case (Forall tyvrs ty1 ty2) + then have "supp (ty1[X \ U]\<^sub>\) \ ty_dom (\[X \ U]\<^sub>e @ TVarB tyvrs ty2 # \)" + apply (simp add: closed_in_def ty.supp abs_supp) + by (metis Diff_subset_conv Un_left_commute doms_append(1) le_supI2 ty_dom.simps(2) tyvrs_of.simps(2)) + with Forall show ?case + by (auto simp add: closed_in_def ty.supp abs_supp doms_append) +qed lemmas subst_closed_in' = subst_closed_in [where \="[]", simplified] lemma typing_closed_in: assumes "\ \ t : T" shows "T closed_in \" using assms proof induct case (T_Var x T \) from \\ \ ok\ and \VarB x T \ set \\ show ?case by (rule ok_imp_VarB_closed_in) next case (T_App \ t\<^sub>1 T\<^sub>1 T\<^sub>2 t\<^sub>2) - then show ?case by (auto simp add: ty.supp closed_in_def) + then show ?case by (auto simp: ty.supp closed_in_def) next case (T_Abs x T\<^sub>1 \ t\<^sub>2 T\<^sub>2) from \VarB x T\<^sub>1 # \ \ t\<^sub>2 : T\<^sub>2\ have "T\<^sub>1 closed_in \" by (auto dest: typing_ok) - with T_Abs show ?case by (auto simp add: ty.supp closed_in_def) + with T_Abs show ?case by (auto simp: ty.supp closed_in_def) next case (T_Sub \ t S T) from \\ \ S <: T\ show ?case by (simp add: subtype_implies_closed) next case (T_TAbs X T\<^sub>1 \ t\<^sub>2 T\<^sub>2) from \TVarB X T\<^sub>1 # \ \ t\<^sub>2 : T\<^sub>2\ have "T\<^sub>1 closed_in \" by (auto dest: typing_ok) - with T_TAbs show ?case by (auto simp add: ty.supp closed_in_def abs_supp) + with T_TAbs show ?case by (auto simp: ty.supp closed_in_def abs_supp) next case (T_TApp X \ t\<^sub>1 T2 T11 T12) then have "T12 closed_in (TVarB X T11 # \)" - by (auto simp add: closed_in_def ty.supp abs_supp) + by (auto simp: closed_in_def ty.supp abs_supp) moreover from T_TApp have "T2 closed_in \" by (simp add: subtype_implies_closed) ultimately show ?case by (rule subst_closed_in') qed subsection \Evaluation\ inductive val :: "trm \ bool" where Abs[intro]: "val (\x:T. t)" | TAbs[intro]: "val (\X<:T. t)" equivariance val inductive_cases val_inv_auto[elim]: "val (Var x)" "val (t1 \ t2)" "val (t1 \\<^sub>\ t2)" inductive eval :: "trm \ trm \ bool" ("_ \ _" [60,60] 60) where E_Abs : "\ x \ v\<^sub>2; val v\<^sub>2 \ \ (\x:T\<^sub>11. t\<^sub>12) \ v\<^sub>2 \ t\<^sub>12[x \ v\<^sub>2]" | E_App1 [intro]: "t \ t' \ t \ u \ t' \ u" | E_App2 [intro]: "\ val v; t \ t' \ \ v \ t \ v \ t'" | E_TAbs : "X \ (T\<^sub>11, T\<^sub>2) \ (\X<:T\<^sub>11. t\<^sub>12) \\<^sub>\ T\<^sub>2 \ t\<^sub>12[X \\<^sub>\ T\<^sub>2]" | E_TApp [intro]: "t \ t' \ t \\<^sub>\ T \ t' \\<^sub>\ T" lemma better_E_Abs[intro]: assumes H: "val v2" shows "(\x:T11. t12) \ v2 \ t12[x \ v2]" proof - obtain y::vrs where y: "y \ (x, t12, v2)" by (rule exists_fresh) (rule fin_supp) then have "y \ v2" by simp then have "(\y:T11. [(y, x)] \ t12) \ v2 \ ([(y, x)] \ t12)[y \ v2]" using H by (rule E_Abs) moreover from y have "(\x:T11. t12) \ v2 = (\y:T11. [(y, x)] \ t12) \ v2" - by (auto simp add: trm.inject alpha' fresh_prod fresh_atm) + by (auto simp: trm.inject alpha' fresh_prod fresh_atm) ultimately have "(\x:T11. t12) \ v2 \ ([(y, x)] \ t12)[y \ v2]" by simp with y show ?thesis by (simp add: subst_trm_rename) qed lemma better_E_TAbs[intro]: "(\X<:T11. t12) \\<^sub>\ T2 \ t12[X \\<^sub>\ T2]" proof - obtain Y::tyvrs where Y: "Y \ (X, t12, T11, T2)" by (rule exists_fresh) (rule fin_supp) then have "Y \ (T11, T2)" by simp then have "(\Y<:T11. [(Y, X)] \ t12) \\<^sub>\ T2 \ ([(Y, X)] \ t12)[Y \\<^sub>\ T2]" by (rule E_TAbs) moreover from Y have "(\X<:T11. t12) \\<^sub>\ T2 = (\Y<:T11. [(Y, X)] \ t12) \\<^sub>\ T2" - by (auto simp add: trm.inject alpha' fresh_prod fresh_atm) + by (auto simp: trm.inject alpha' fresh_prod fresh_atm) ultimately have "(\X<:T11. t12) \\<^sub>\ T2 \ ([(Y, X)] \ t12)[Y \\<^sub>\ T2]" by simp with Y show ?thesis by (simp add: subst_trm_ty_rename) qed equivariance eval nominal_inductive eval by (simp_all add: abs_fresh ty_vrs_fresh subst_trm_fresh_tyvar subst_trm_fresh_var subst_trm_ty_fresh') inductive_cases eval_inv_auto[elim]: "Var x \ t'" "(\x:T. t) \ t'" "(\X<:T. t) \ t'" lemma ty_dom_cons: shows "ty_dom (\@[VarB X Q]@\) = ty_dom (\@\)" by (induct \) (auto) lemma closed_in_cons: assumes "S closed_in (\ @ VarB X Q # \)" shows "S closed_in (\@\)" using assms ty_dom_cons closed_in_def by auto lemma closed_in_weaken: "T closed_in (\ @ \) \ T closed_in (\ @ B # \)" - by (auto simp add: closed_in_def doms_append) + by (auto simp: closed_in_def doms_append) lemma closed_in_weaken': "T closed_in \ \ T closed_in (\ @ \)" - by (auto simp add: closed_in_def doms_append) + by (auto simp: closed_in_def doms_append) lemma valid_subst: assumes ok: "\ (\ @ TVarB X Q # \) ok" and closed: "P closed_in \" shows "\ (\[X \ P]\<^sub>e @ \) ok" using ok closed - apply (induct \) - apply simp_all - apply (erule validE) - apply assumption - apply (erule validE) - apply simp - apply (rule valid_consT) - apply assumption - apply (simp add: doms_append ty_dom_subst) - apply (simp add: fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_doms) - apply (rule_tac S=Q in subst_closed_in') - apply (simp add: closed_in_def doms_append ty_dom_subst) - apply (simp add: closed_in_def doms_append) - apply blast - apply simp - apply (rule valid_cons) - apply assumption - apply (simp add: doms_append trm_dom_subst) - apply (rule_tac S=Q in subst_closed_in') - apply (simp add: closed_in_def doms_append ty_dom_subst) - apply (simp add: closed_in_def doms_append) - apply blast - done +proof (induct \) + case Nil + then show ?case + by auto +next + case (Cons a \) + then have *: "\ (a # \ @ TVarB X Q # \) ok" + by fastforce + then show ?case + apply (rule validE) + using Cons + apply (simp add: at_tyvrs_inst closed doms_append(1) finite_doms(1) fresh_fin_insert fs_tyvrs_inst pt_tyvrs_inst subst_closed_in ty_dom_subst) + by (simp add: doms_append(2) subst_closed_in Cons.hyps closed trm_dom_subst) +qed lemma ty_dom_vrs: shows "ty_dom (G @ [VarB x Q] @ D) = ty_dom (G @ D)" -by (induct G) (auto) + by (induct G) (auto) lemma valid_cons': assumes "\ (\ @ VarB x Q # \) ok" shows "\ (\ @ \) ok" using assms proof (induct "\ @ VarB x Q # \" arbitrary: \ \) case valid_nil have "[] = \ @ VarB x Q # \" by fact then have "False" by auto then show ?case by auto next case (valid_consT G X T) then show ?case proof (cases \) case Nil with valid_consT show ?thesis by simp next case (Cons b bs) with valid_consT have "\ (bs @ \) ok" by simp moreover from Cons and valid_consT have "X \ ty_dom (bs @ \)" by (simp add: doms_append) moreover from Cons and valid_consT have "T closed_in (bs @ \)" by (simp add: closed_in_def doms_append) ultimately have "\ (TVarB X T # bs @ \) ok" by (rule valid_rel.valid_consT) with Cons and valid_consT show ?thesis by simp qed next case (valid_cons G x T) then show ?case proof (cases \) case Nil with valid_cons show ?thesis by simp next case (Cons b bs) with valid_cons have "\ (bs @ \) ok" by simp moreover from Cons and valid_cons have "x \ trm_dom (bs @ \)" by (simp add: doms_append finite_doms fresh_fin_insert [OF pt_vrs_inst at_vrs_inst fs_vrs_inst]) moreover from Cons and valid_cons have "T closed_in (bs @ \)" by (simp add: closed_in_def doms_append) ultimately have "\ (VarB x T # bs @ \) ok" by (rule valid_rel.valid_cons) with Cons and valid_cons show ?thesis by simp qed qed text \A.5(6)\ lemma type_weaken: assumes "(\@\) \ t : T" and "\ (\ @ B # \) ok" shows "(\ @ B # \) \ t : T" using assms proof(nominal_induct "\ @ \" t T avoiding: \ \ B rule: typing.strong_induct) case (T_Var x T) then show ?case by auto next case (T_App X t\<^sub>1 T\<^sub>2 T\<^sub>11 T\<^sub>12) then show ?case by force next case (T_Abs y T\<^sub>1 t\<^sub>2 T\<^sub>2 \ \) then have "VarB y T\<^sub>1 # \ @ \ \ t\<^sub>2 : T\<^sub>2" by simp then have closed: "T\<^sub>1 closed_in (\ @ \)" by (auto dest: typing_ok) have "\ (VarB y T\<^sub>1 # \ @ B # \) ok" - apply (rule valid_cons) - apply (rule T_Abs) - apply (simp add: doms_append - fresh_fin_insert [OF pt_vrs_inst at_vrs_inst fs_vrs_inst] - fresh_fin_union [OF pt_vrs_inst at_vrs_inst fs_vrs_inst] - finite_doms finite_vrs fresh_vrs_of T_Abs fresh_trm_dom) - apply (rule closed_in_weaken) - apply (rule closed) - done + by (simp add: T_Abs closed closed_in_weaken fresh_list_append fresh_list_cons fresh_trm_dom) then have "\ ((VarB y T\<^sub>1 # \) @ B # \) ok" by simp with _ have "(VarB y T\<^sub>1 # \) @ B # \ \ t\<^sub>2 : T\<^sub>2" by (rule T_Abs) simp then have "VarB y T\<^sub>1 # \ @ B # \ \ t\<^sub>2 : T\<^sub>2" by simp then show ?case by (rule typing.T_Abs) next case (T_Sub t S T \ \) from refl and \\ (\ @ B # \) ok\ have "\ @ B # \ \ t : S" by (rule T_Sub) moreover from \(\ @ \)\S<:T\ and \\ (\ @ B # \) ok\ have "(\ @ B # \)\S<:T" by (rule weakening) (simp add: extends_def T_Sub) ultimately show ?case by (rule typing.T_Sub) next case (T_TAbs X T\<^sub>1 t\<^sub>2 T\<^sub>2 \ \) from \TVarB X T\<^sub>1 # \ @ \ \ t\<^sub>2 : T\<^sub>2\ have closed: "T\<^sub>1 closed_in (\ @ \)" by (auto dest: typing_ok) have "\ (TVarB X T\<^sub>1 # \ @ B # \) ok" - apply (rule valid_consT) - apply (rule T_TAbs) - apply (simp add: doms_append - fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] - fresh_fin_union [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] - finite_doms finite_vrs tyvrs_fresh T_TAbs fresh_dom) - apply (rule closed_in_weaken) - apply (rule closed) - done + by (simp add: T_TAbs at_tyvrs_inst closed closed_in_weaken doms_append finite_doms finite_vrs + fresh_dom fresh_fin_union fs_tyvrs_inst pt_tyvrs_inst tyvrs_fresh) then have "\ ((TVarB X T\<^sub>1 # \) @ B # \) ok" by simp with _ have "(TVarB X T\<^sub>1 # \) @ B # \ \ t\<^sub>2 : T\<^sub>2" by (rule T_TAbs) simp then have "TVarB X T\<^sub>1 # \ @ B # \ \ t\<^sub>2 : T\<^sub>2" by simp then show ?case by (rule typing.T_TAbs) next case (T_TApp X t\<^sub>1 T2 T11 T12 \ \) have "\ @ B # \ \ t\<^sub>1 : (\X<:T11. T12)" by (rule T_TApp refl)+ moreover from \(\ @ \)\T2<:T11\ and \\ (\ @ B # \) ok\ have "(\ @ B # \)\T2<:T11" by (rule weakening) (simp add: extends_def T_TApp) ultimately show ?case by (rule better_T_TApp) qed lemma type_weaken': "\ \ t : T \ \ (\@\) ok \ (\@\) \ t : T" - apply (induct \) - apply simp_all - apply (erule validE) - apply (insert type_weaken [of "[]", simplified]) - apply simp_all - done +proof (induct \) + case Nil + then show ?case by auto +next + case (Cons a \) + then show ?case + by (metis append_Cons append_Nil type_weaken validE(3)) +qed text \A.6\ lemma strengthening: assumes "(\ @ VarB x Q # \) \ S <: T" shows "(\@\) \ S <: T" using assms proof (induct "\ @ VarB x Q # \" S T arbitrary: \) case (SA_Top S) then have "\ (\ @ \) ok" by (auto dest: valid_cons') moreover have "S closed_in (\ @ \)" using SA_Top by (auto dest: closed_in_cons) ultimately show ?case using subtype_of.SA_Top by auto next case (SA_refl_TVar X) from \\ (\ @ VarB x Q # \) ok\ have h1:"\ (\ @ \) ok" by (auto dest: valid_cons') have "X \ ty_dom (\ @ VarB x Q # \)" using SA_refl_TVar by auto then have h2:"X \ ty_dom (\ @ \)" using ty_dom_vrs by auto show ?case using h1 h2 by auto next case (SA_all T1 S1 X S2 T2) have h1:"((TVarB X T1 # \) @ \)\S2<:T2" by (fastforce intro: SA_all) have h2:"(\ @ \)\T1<:S1" using SA_all by auto then show ?case using h1 h2 by auto qed (auto) lemma narrow_type: \ \A.7\ assumes H: "\ @ (TVarB X Q) # \ \ t : T" shows "\ \ P <: Q \ \ @ (TVarB X P) # \ \ t : T" using H proof (nominal_induct "\ @ (TVarB X Q) # \" t T avoiding: P arbitrary: \ rule: typing.strong_induct) case (T_Var x T P D) then have "VarB x T \ set (D @ TVarB X P # \)" and "\ (D @ TVarB X P # \) ok" by (auto intro: replace_type dest!: subtype_implies_closed) then show ?case by auto next case (T_App t1 T1 T2 t2 P D) then show ?case by force next case (T_Abs x T1 t2 T2 P D) then show ?case by (fastforce dest: typing_ok) next case (T_Sub t S T P D) then show ?case using subtype_narrow by fastforce next case (T_TAbs X' T1 t2 T2 P D) then show ?case by (fastforce dest: typing_ok) next case (T_TApp X' t1 T2 T11 T12 P D) then have "D @ TVarB X P # \ \ t1 : Forall X' T12 T11" by fastforce moreover have "(D @ [TVarB X Q] @ \) \ T2<:T11" using T_TApp by auto then have "(D @ [TVarB X P] @ \) \ T2<:T11" using \\\P<:Q\ by (rule subtype_narrow) moreover from T_TApp have "X' \ (D @ TVarB X P # \, t1, T2)" by (simp add: fresh_list_append fresh_list_cons fresh_prod) ultimately show ?case by auto qed subsection \Substitution lemmas\ subsubsection \Substition Preserves Typing\ theorem subst_type: \ \A.8\ assumes H: "(\ @ (VarB x U) # \) \ t : T" shows "\ \ u : U \ \ @ \ \ t[x \ u] : T" using H proof (nominal_induct "\ @ (VarB x U) # \" t T avoiding: x u arbitrary: \ rule: typing.strong_induct) case (T_Var y T x u D) show ?case proof (cases "x = y") assume eq:"x=y" then have "T=U" using T_Var uniqueness_of_ctxt' by auto then show ?case using eq T_Var by (auto intro: type_weaken' dest: valid_cons') next assume "x\y" then show ?case using T_Var - by (auto simp add:binding.inject dest: valid_cons') + by (auto simp:binding.inject dest: valid_cons') qed next case (T_App t1 T1 T2 t2 x u D) then show ?case by force next case (T_Abs y T1 t2 T2 x u D) then show ?case by force next case (T_Sub t S T x u D) then have "D @ \ \ t[x \ u] : S" by auto moreover have "(D @ \) \ S<:T" using T_Sub by (auto dest: strengthening) ultimately show ?case by auto next case (T_TAbs X T1 t2 T2 x u D) from \TVarB X T1 # D @ VarB x U # \ \ t2 : T2\ have "X \ T1" - by (auto simp add: valid_ty_dom_fresh dest: typing_ok intro!: closed_in_fresh) + by (auto simp: valid_ty_dom_fresh dest: typing_ok intro!: closed_in_fresh) with \X \ u\ and T_TAbs show ?case by fastforce next case (T_TApp X t1 T2 T11 T12 x u D) then have "(D@\) \T2<:T11" using T_TApp by (auto dest: strengthening) then show "((D @ \) \ ((t1 \\<^sub>\ T2)[x \ u]) : (T12[X \ T2]\<^sub>\))" using T_TApp - by (force simp add: fresh_prod fresh_list_append fresh_list_cons subst_trm_fresh_tyvar) + by (force simp: fresh_prod fresh_list_append fresh_list_cons subst_trm_fresh_tyvar) qed subsubsection \Type Substitution Preserves Subtyping\ lemma substT_subtype: \ \A.10\ assumes H: "(\ @ ((TVarB X Q) # \)) \ S <: T" shows "\ \ P <: Q \ (\[X \ P]\<^sub>e @ \) \ S[X \ P]\<^sub>\ <: T[X \ P]\<^sub>\" using H proof (nominal_induct "\ @ TVarB X Q # \" S T avoiding: X P arbitrary: \ rule: subtype_of.strong_induct) case (SA_Top S X P D) then have "\ (D @ TVarB X Q # \) ok" by simp moreover have closed: "P closed_in \" using SA_Top subtype_implies_closed by auto ultimately have "\ (D[X \ P]\<^sub>e @ \) ok" by (rule valid_subst) moreover from SA_Top have "S closed_in (D @ TVarB X Q # \)" by simp then have "S[X \ P]\<^sub>\ closed_in (D[X \ P]\<^sub>e @ \)" using closed by (rule subst_closed_in) ultimately show ?case by auto next case (SA_trans_TVar Y S T X P D) have h:"(D @ TVarB X Q # \)\S<:T" by fact then have ST: "(D[X \ P]\<^sub>e @ \) \ S[X \ P]\<^sub>\ <: T[X \ P]\<^sub>\" using SA_trans_TVar by auto from h have G_ok: "\ (D @ TVarB X Q # \) ok" by (rule subtype_implies_ok) from G_ok and SA_trans_TVar have X_\_ok: "\ (TVarB X Q # \) ok" by (auto intro: validE_append) show "(D[X \ P]\<^sub>e @ \) \ Tvar Y[X \ P]\<^sub>\<:T[X \ P]\<^sub>\" proof (cases "X = Y") assume eq: "X = Y" from eq and SA_trans_TVar have "TVarB Y Q \ set (D @ TVarB X Q # \)" by simp with G_ok have QS: "Q = S" using \TVarB Y S \ set (D @ TVarB X Q # \)\ by (rule uniqueness_of_ctxt) from X_\_ok have "X \ ty_dom \" and "Q closed_in \" by auto then have XQ: "X \ Q" by (rule closed_in_fresh) note \\\P<:Q\ moreover from ST have "\ (D[X \ P]\<^sub>e @ \) ok" by (rule subtype_implies_ok) moreover have "(D[X \ P]\<^sub>e @ \) extends \" by (simp add: extends_def) ultimately have "(D[X \ P]\<^sub>e @ \) \ P<:Q" by (rule weakening) with QS have "(D[X \ P]\<^sub>e @ \) \ P<:S" by simp moreover from XQ and ST and QS have "(D[X \ P]\<^sub>e @ \) \ S<:T[X \ P]\<^sub>\" by (simp add: type_subst_identity) ultimately have "(D[X \ P]\<^sub>e @ \) \ P<:T[X \ P]\<^sub>\" by (rule subtype_transitivity) with eq show ?case by simp next assume neq: "X \ Y" with SA_trans_TVar have "TVarB Y S \ set D \ TVarB Y S \ set \" by (simp add: binding.inject) then show ?case proof assume "TVarB Y S \ set D" then have "TVarB Y (S[X \ P]\<^sub>\) \ set (D[X \ P]\<^sub>e)" by (rule ctxt_subst_mem_TVarB) then have "TVarB Y (S[X \ P]\<^sub>\) \ set (D[X \ P]\<^sub>e @ \)" by simp with neq and ST show ?thesis by auto next assume Y: "TVarB Y S \ set \" from X_\_ok have "X \ ty_dom \" and "\ \ ok" by auto then have "X \ \" by (simp add: valid_ty_dom_fresh) with Y have "X \ S" - by (induct \) (auto simp add: fresh_list_nil fresh_list_cons) + by (induct \) (auto simp: fresh_list_nil fresh_list_cons) with ST have "(D[X \ P]\<^sub>e @ \)\S<:T[X \ P]\<^sub>\" by (simp add: type_subst_identity) moreover from Y have "TVarB Y S \ set (D[X \ P]\<^sub>e @ \)" by simp ultimately show ?thesis using neq by auto qed qed next case (SA_refl_TVar Y X P D) note \\ (D @ TVarB X Q # \) ok\ moreover from SA_refl_TVar have closed: "P closed_in \" by (auto dest: subtype_implies_closed) ultimately have ok: "\ (D[X \ P]\<^sub>e @ \) ok" using valid_subst by auto from closed have closed': "P closed_in (D[X \ P]\<^sub>e @ \)" by (simp add: closed_in_weaken') show ?case proof (cases "X = Y") assume "X = Y" with closed' and ok show ?thesis by (auto intro: subtype_reflexivity) next assume neq: "X \ Y" with SA_refl_TVar have "Y \ ty_dom (D[X \ P]\<^sub>e @ \)" by (simp add: ty_dom_subst doms_append) with neq and ok show ?thesis by auto qed next case (SA_arrow T1 S1 S2 T2 X P D) then have h1:"(D[X \ P]\<^sub>e @ \)\T1[X \ P]\<^sub>\<:S1[X \ P]\<^sub>\" using SA_arrow by auto from SA_arrow have h2:"(D[X \ P]\<^sub>e @ \)\S2[X \ P]\<^sub>\<:T2[X \ P]\<^sub>\" using SA_arrow by auto show ?case using subtype_of.SA_arrow h1 h2 by auto next case (SA_all T1 S1 Y S2 T2 X P D) then have Y: "Y \ ty_dom (D @ TVarB X Q # \)" by (auto dest: subtype_implies_ok intro: fresh_dom) moreover from SA_all have "S1 closed_in (D @ TVarB X Q # \)" by (auto dest: subtype_implies_closed) ultimately have S1: "Y \ S1" by (rule closed_in_fresh) from SA_all have "T1 closed_in (D @ TVarB X Q # \)" by (auto dest: subtype_implies_closed) with Y have T1: "Y \ T1" by (rule closed_in_fresh) with SA_all and S1 show ?case by force qed subsubsection \Type Substitution Preserves Typing\ theorem substT_type: \ \A.11\ assumes H: "(D @ TVarB X Q # G) \ t : T" shows "G \ P <: Q \ (D[X \ P]\<^sub>e @ G) \ t[X \\<^sub>\ P] : T[X \ P]\<^sub>\" using H proof (nominal_induct "D @ TVarB X Q # G" t T avoiding: X P arbitrary: D rule: typing.strong_induct) case (T_Var x T X P D') have "G\P<:Q" by fact then have "P closed_in G" using subtype_implies_closed by auto moreover note \\ (D' @ TVarB X Q # G) ok\ ultimately have "\ (D'[X \ P]\<^sub>e @ G) ok" using valid_subst by auto moreover note \VarB x T \ set (D' @ TVarB X Q # G)\ then have "VarB x T \ set D' \ VarB x T \ set G" by simp then have "(VarB x (T[X \ P]\<^sub>\)) \ set (D'[X \ P]\<^sub>e @ G)" proof assume "VarB x T \ set D'" then have "VarB x (T[X \ P]\<^sub>\) \ set (D'[X \ P]\<^sub>e)" by (rule ctxt_subst_mem_VarB) then show ?thesis by simp next assume x: "VarB x T \ set G" from T_Var have ok: "\ G ok" by (auto dest: subtype_implies_ok) then have "X \ ty_dom G" using T_Var by (auto dest: validE_append) with ok have "X \ G" by (simp add: valid_ty_dom_fresh) moreover from x have "VarB x T \ set (D' @ G)" by simp then have "VarB x (T[X \ P]\<^sub>\) \ set ((D' @ G)[X \ P]\<^sub>e)" by (rule ctxt_subst_mem_VarB) ultimately show ?thesis by (simp add: ctxt_subst_append ctxt_subst_identity) qed ultimately show ?case by auto next case (T_App t1 T1 T2 t2 X P D') then have "D'[X \ P]\<^sub>e @ G \ t1[X \\<^sub>\ P] : (T1 \ T2)[X \ P]\<^sub>\" by auto moreover from T_App have "D'[X \ P]\<^sub>e @ G \ t2[X \\<^sub>\ P] : T1[X \ P]\<^sub>\" by auto ultimately show ?case by auto next case (T_Abs x T1 t2 T2 X P D') then show ?case by force next case (T_Sub t S T X P D') then show ?case using substT_subtype by force next case (T_TAbs X' T1 t2 T2 X P D') then have "X' \ ty_dom (D' @ TVarB X Q # G)" and "T1 closed_in (D' @ TVarB X Q # G)" by (auto dest: typing_ok) then have "X' \ T1" by (rule closed_in_fresh) with T_TAbs show ?case by force next case (T_TApp X' t1 T2 T11 T12 X P D') then have "X' \ ty_dom (D' @ TVarB X Q # G)" by (simp add: fresh_dom) moreover from T_TApp have "T11 closed_in (D' @ TVarB X Q # G)" by (auto dest: subtype_implies_closed) ultimately have X': "X' \ T11" by (rule closed_in_fresh) from T_TApp have "D'[X \ P]\<^sub>e @ G \ t1[X \\<^sub>\ P] : (\X'<:T11. T12)[X \ P]\<^sub>\" by simp with X' and T_TApp show ?case - by (auto simp add: fresh_atm type_substitution_lemma + by (auto simp: fresh_atm type_substitution_lemma fresh_list_append fresh_list_cons ctxt_subst_fresh' type_subst_fresh subst_trm_ty_fresh intro: substT_subtype) qed lemma Abs_type: \ \A.13(1)\ assumes H: "\ \ (\x:S. s) : T" and H': "\ \ T <: U \ U'" and H'': "x \ \" obtains S' where "\ \ U <: S" and "(VarB x S) # \ \ s : S'" and "\ \ S' <: U'" using H H' H'' proof (nominal_induct \ t \ "\x:S. s" T avoiding: x arbitrary: U U' S s rule: typing.strong_induct) case (T_Abs y T\<^sub>1 \ t\<^sub>2 T\<^sub>2) from \\ \ T\<^sub>1 \ T\<^sub>2 <: U \ U'\ obtain ty1: "\ \ U <: S" and ty2: "\ \ T\<^sub>2 <: U'" using T_Abs by cases (simp_all add: ty.inject trm.inject alpha fresh_atm) from T_Abs have "VarB y S # \ \ [(y, x)] \ s : T\<^sub>2" by (simp add: trm.inject alpha fresh_atm) then have "[(y, x)] \ (VarB y S # \) \ [(y, x)] \ [(y, x)] \ s : [(y, x)] \ T\<^sub>2" by (rule typing.eqvt) moreover from T_Abs have "y \ \" by (auto dest!: typing_ok simp add: fresh_trm_dom) ultimately have "VarB x S # \ \ s : T\<^sub>2" using T_Abs by (perm_simp add: ty_vrs_prm_simp) with ty1 show ?case using ty2 by (rule T_Abs) next case (T_Sub \ t S T) then show ?case using subtype_transitivity by blast qed simp_all lemma subtype_reflexivity_from_typing: assumes "\ \ t : T" shows "\ \ T <: T" using assms subtype_reflexivity typing_ok typing_closed_in by simp lemma Abs_type': assumes H: "\ \ (\x:S. s) : U \ U'" and H': "x \ \" obtains S' where "\ \ U <: S" and "(VarB x S) # \ \ s : S'" and "\ \ S' <: U'" using H subtype_reflexivity_from_typing [OF H] H' by (rule Abs_type) lemma TAbs_type: \ \A.13(2)\ assumes H: "\ \ (\X<:S. s) : T" and H': "\ \ T <: (\X<:U. U')" and fresh: "X \ \" "X \ S" "X \ U" obtains S' where "\ \ U <: S" and "(TVarB X U # \) \ s : S'" and "(TVarB X U # \) \ S' <: U'" using H H' fresh proof (nominal_induct \ t \ "\X<:S. s" T avoiding: X U U' S arbitrary: s rule: typing.strong_induct) case (T_TAbs Y T\<^sub>1 \ t\<^sub>2 T\<^sub>2) from \TVarB Y T\<^sub>1 # \ \ t\<^sub>2 : T\<^sub>2\ have Y: "Y \ \" by (auto dest!: typing_ok simp add: valid_ty_dom_fresh) from \Y \ U'\ and \Y \ X\ have "(\X<:U. U') = (\Y<:U. [(Y, X)] \ U')" by (simp add: ty.inject alpha' fresh_atm) with T_TAbs have "\ \ (\Y<:S. T\<^sub>2) <: (\Y<:U. [(Y, X)] \ U')" by (simp add: trm.inject) then obtain ty1: "\ \ U <: S" and ty2: "(TVarB Y U # \) \ T\<^sub>2 <: ([(Y, X)] \ U')" using T_TAbs Y by (cases rule: subtype_of.strong_cases [where X=Y]) (simp_all add: ty.inject alpha abs_fresh) note ty1 moreover from T_TAbs have "TVarB Y S # \ \ ([(Y, X)] \ s) : T\<^sub>2" by (simp add: trm.inject alpha fresh_atm) then have "[(Y, X)] \ (TVarB Y S # \) \ [(Y, X)] \ [(Y, X)] \ s : [(Y, X)] \ T\<^sub>2" by (rule typing.eqvt) with \X \ \\ \X \ S\ Y \Y \ S\ have "TVarB X S # \ \ s : [(Y, X)] \ T\<^sub>2" by perm_simp then have "TVarB X U # \ \ s : [(Y, X)] \ T\<^sub>2" using ty1 by (rule narrow_type [of "[]", simplified]) moreover from ty2 have "([(Y, X)] \ (TVarB Y U # \)) \ ([(Y, X)] \ T\<^sub>2) <: ([(Y, X)] \ [(Y, X)] \ U')" by (rule subtype_of.eqvt) with \X \ \\ \X \ U\ Y \Y \ U\ have "(TVarB X U # \) \ ([(Y, X)] \ T\<^sub>2) <: U'" by perm_simp ultimately show ?case by (rule T_TAbs) next case (T_Sub \ t S T) then show ?case using subtype_transitivity by blast qed simp_all lemma TAbs_type': assumes H: "\ \ (\X<:S. s) : (\X<:U. U')" and fresh: "X \ \" "X \ S" "X \ U" obtains S' where "\ \ U <: S" and "(TVarB X U # \) \ s : S'" and "(TVarB X U # \) \ S' <: U'" using H subtype_reflexivity_from_typing [OF H] fresh by (rule TAbs_type) theorem preservation: \ \A.20\ assumes H: "\ \ t : T" shows "t \ t' \ \ \ t' : T" using H proof (nominal_induct avoiding: t' rule: typing.strong_induct) case (T_App \ t\<^sub>1 T\<^sub>11 T\<^sub>12 t\<^sub>2 t') obtain x::vrs where x_fresh: "x \ (\, t\<^sub>1 \ t\<^sub>2, t')" by (rule exists_fresh) (rule fin_supp) obtain X::tyvrs where "X \ (t\<^sub>1 \ t\<^sub>2, t')" by (rule exists_fresh) (rule fin_supp) with \t\<^sub>1 \ t\<^sub>2 \ t'\ show ?case proof (cases rule: eval.strong_cases [where x=x and X=X]) case (E_Abs v\<^sub>2 T\<^sub>11' t\<^sub>12) with T_App and x_fresh have h: "\ \ (\x:T\<^sub>11'. t\<^sub>12) : T\<^sub>11 \ T\<^sub>12" by (simp add: trm.inject fresh_prod) moreover from x_fresh have "x \ \" by simp ultimately obtain S' where T\<^sub>11: "\ \ T\<^sub>11 <: T\<^sub>11'" and t\<^sub>12: "(VarB x T\<^sub>11') # \ \ t\<^sub>12 : S'" and S': "\ \ S' <: T\<^sub>12" by (rule Abs_type') blast from \\ \ t\<^sub>2 : T\<^sub>11\ have "\ \ t\<^sub>2 : T\<^sub>11'" using T\<^sub>11 by (rule T_Sub) with t\<^sub>12 have "\ \ t\<^sub>12[x \ t\<^sub>2] : S'" by (rule subst_type [where \="[]", simplified]) hence "\ \ t\<^sub>12[x \ t\<^sub>2] : T\<^sub>12" using S' by (rule T_Sub) with E_Abs and x_fresh show ?thesis by (simp add: trm.inject fresh_prod) next case (E_App1 t''' t'' u) hence "t\<^sub>1 \ t''" by (simp add:trm.inject) hence "\ \ t'' : T\<^sub>11 \ T\<^sub>12" by (rule T_App) hence "\ \ t'' \ t\<^sub>2 : T\<^sub>12" using \\ \ t\<^sub>2 : T\<^sub>11\ by (rule typing.T_App) with E_App1 show ?thesis by (simp add:trm.inject) next case (E_App2 v t''' t'') hence "t\<^sub>2 \ t''" by (simp add:trm.inject) hence "\ \ t'' : T\<^sub>11" by (rule T_App) with T_App(1) have "\ \ t\<^sub>1 \ t'' : T\<^sub>12" by (rule typing.T_App) with E_App2 show ?thesis by (simp add:trm.inject) qed (simp_all add: fresh_prod) next case (T_TApp X \ t\<^sub>1 T\<^sub>2 T\<^sub>11 T\<^sub>12 t') obtain x::vrs where "x \ (t\<^sub>1 \\<^sub>\ T\<^sub>2, t')" by (rule exists_fresh) (rule fin_supp) with \t\<^sub>1 \\<^sub>\ T\<^sub>2 \ t'\ show ?case proof (cases rule: eval.strong_cases [where X=X and x=x]) case (E_TAbs T\<^sub>11' T\<^sub>2' t\<^sub>12) with T_TApp have "\ \ (\X<:T\<^sub>11'. t\<^sub>12) : (\X<:T\<^sub>11. T\<^sub>12)" and "X \ \" and "X \ T\<^sub>11'" by (simp_all add: trm.inject) moreover from \\\T\<^sub>2<:T\<^sub>11\ and \X \ \\ have "X \ T\<^sub>11" by (blast intro: closed_in_fresh fresh_dom dest: subtype_implies_closed) ultimately obtain S' where "TVarB X T\<^sub>11 # \ \ t\<^sub>12 : S'" and "(TVarB X T\<^sub>11 # \) \ S' <: T\<^sub>12" by (rule TAbs_type') blast hence "TVarB X T\<^sub>11 # \ \ t\<^sub>12 : T\<^sub>12" by (rule T_Sub) hence "\ \ t\<^sub>12[X \\<^sub>\ T\<^sub>2] : T\<^sub>12[X \ T\<^sub>2]\<^sub>\" using \\ \ T\<^sub>2 <: T\<^sub>11\ by (rule substT_type [where D="[]", simplified]) with T_TApp and E_TAbs show ?thesis by (simp add: trm.inject) next case (E_TApp t''' t'' T) from E_TApp have "t\<^sub>1 \ t''" by (simp add: trm.inject) then have "\ \ t'' : (\X<:T\<^sub>11. T\<^sub>12)" by (rule T_TApp) then have "\ \ t'' \\<^sub>\ T\<^sub>2 : T\<^sub>12[X \ T\<^sub>2]\<^sub>\" using \\ \ T\<^sub>2 <: T\<^sub>11\ by (rule better_T_TApp) with E_TApp show ?thesis by (simp add: trm.inject) qed (simp_all add: fresh_prod) next case (T_Sub \ t S T t') have "t \ t'" by fact hence "\ \ t' : S" by (rule T_Sub) moreover have "\ \ S <: T" by fact ultimately show ?case by (rule typing.T_Sub) qed (auto) lemma Fun_canonical: \ \A.14(1)\ assumes ty: "[] \ v : T\<^sub>1 \ T\<^sub>2" shows "val v \ \x t S. v = (\x:S. t)" using ty proof (induct "[]::env" v "T\<^sub>1 \ T\<^sub>2" arbitrary: T\<^sub>1 T\<^sub>2) case (T_Sub t S) from \[] \ S <: T\<^sub>1 \ T\<^sub>2\ obtain S\<^sub>1 S\<^sub>2 where S: "S = S\<^sub>1 \ S\<^sub>2" - by cases (auto simp add: T_Sub) + by cases (auto simp: T_Sub) then show ?case using \val t\ by (rule T_Sub) qed (auto) lemma TyAll_canonical: \ \A.14(3)\ fixes X::tyvrs assumes ty: "[] \ v : (\X<:T\<^sub>1. T\<^sub>2)" shows "val v \ \X t S. v = (\X<:S. t)" using ty proof (induct "[]::env" v "\X<:T\<^sub>1. T\<^sub>2" arbitrary: X T\<^sub>1 T\<^sub>2) case (T_Sub t S) from \[] \ S <: (\X<:T\<^sub>1. T\<^sub>2)\ obtain X S\<^sub>1 S\<^sub>2 where S: "S = (\X<:S\<^sub>1. S\<^sub>2)" - by cases (auto simp add: T_Sub) + by cases (auto simp: T_Sub) then show ?case using T_Sub by auto qed (auto) theorem progress: assumes "[] \ t : T" shows "val t \ (\t'. t \ t')" using assms proof (induct "[]::env" t T) case (T_App t\<^sub>1 T\<^sub>11 T\<^sub>12 t\<^sub>2) hence "val t\<^sub>1 \ (\t'. t\<^sub>1 \ t')" by simp thus ?case proof assume t\<^sub>1_val: "val t\<^sub>1" with T_App obtain x t3 S where t\<^sub>1: "t\<^sub>1 = (\x:S. t3)" by (auto dest!: Fun_canonical) from T_App have "val t\<^sub>2 \ (\t'. t\<^sub>2 \ t')" by simp thus ?case proof assume "val t\<^sub>2" with t\<^sub>1 have "t\<^sub>1 \ t\<^sub>2 \ t3[x \ t\<^sub>2]" by auto thus ?case by auto next assume "\t'. t\<^sub>2 \ t'" then obtain t' where "t\<^sub>2 \ t'" by auto with t\<^sub>1_val have "t\<^sub>1 \ t\<^sub>2 \ t\<^sub>1 \ t'" by auto thus ?case by auto qed next assume "\t'. t\<^sub>1 \ t'" then obtain t' where "t\<^sub>1 \ t'" by auto hence "t\<^sub>1 \ t\<^sub>2 \ t' \ t\<^sub>2" by auto thus ?case by auto qed next case (T_TApp X t\<^sub>1 T\<^sub>2 T\<^sub>11 T\<^sub>12) hence "val t\<^sub>1 \ (\t'. t\<^sub>1 \ t')" by simp thus ?case proof assume "val t\<^sub>1" with T_TApp obtain x t S where "t\<^sub>1 = (\x<:S. t)" by (auto dest!: TyAll_canonical) hence "t\<^sub>1 \\<^sub>\ T\<^sub>2 \ t[x \\<^sub>\ T\<^sub>2]" by auto thus ?case by auto next assume "\t'. t\<^sub>1 \ t'" thus ?case by auto qed qed (auto) end diff --git a/src/HOL/Nominal/Examples/Pattern.thy b/src/HOL/Nominal/Examples/Pattern.thy --- a/src/HOL/Nominal/Examples/Pattern.thy +++ b/src/HOL/Nominal/Examples/Pattern.thy @@ -1,850 +1,861 @@ section \Simply-typed lambda-calculus with let and tuple patterns\ theory Pattern imports "HOL-Nominal.Nominal" begin no_syntax "_Map" :: "maplets => 'a \ 'b" ("(1[_])") atom_decl name nominal_datatype ty = Atom nat | Arrow ty ty (infixr "\" 200) | TupleT ty ty (infixr "\" 210) lemma fresh_type [simp]: "(a::name) \ (T::ty)" by (induct T rule: ty.induct) (simp_all add: fresh_nat) lemma supp_type [simp]: "supp (T::ty) = ({} :: name set)" by (induct T rule: ty.induct) (simp_all add: ty.supp supp_nat) lemma perm_type: "(pi::name prm) \ (T::ty) = T" by (induct T rule: ty.induct) (simp_all add: perm_nat_def) nominal_datatype trm = Var name | Tuple trm trm ("(1'\_,/ _'\)") | Abs ty "\name\trm" | App trm trm (infixl "\" 200) | Let ty trm btrm and btrm = Base trm | Bind ty "\name\btrm" abbreviation Abs_syn :: "name \ ty \ trm \ trm" ("(3\_:_./ _)" [0, 0, 10] 10) where "\x:T. t \ Abs T x t" datatype pat = PVar name ty | PTuple pat pat ("(1'\\_,/ _'\\)") (* FIXME: The following should be done automatically by the nominal package *) overloading pat_perm \ "perm :: name prm \ pat \ pat" (unchecked) begin primrec pat_perm where "pat_perm pi (PVar x ty) = PVar (pi \ x) (pi \ ty)" | "pat_perm pi \\p, q\\ = \\pat_perm pi p, pat_perm pi q\\" end declare pat_perm.simps [eqvt] lemma supp_PVar [simp]: "((supp (PVar x T))::name set) = supp x" by (simp add: supp_def perm_fresh_fresh) lemma supp_PTuple [simp]: "((supp \\p, q\\)::name set) = supp p \ supp q" by (simp add: supp_def Collect_disj_eq del: disj_not1) instance pat :: pt_name proof fix x :: pat show "([]::(name \ _) list) \ x = x" by (induct x) simp_all fix pi1 pi2 :: "(name \ name) list" show "(pi1 @ pi2) \ x = pi1 \ pi2 \ x" by (induct x) (simp_all add: pt_name2) assume "pi1 \ pi2" then show "pi1 \ x = pi2 \ x" by (induct x) (simp_all add: pt_name3) qed instance pat :: fs_name proof fix x :: pat show "finite (supp x::name set)" by (induct x) (simp_all add: fin_supp) qed (* the following function cannot be defined using nominal_primrec, *) (* since variable parameters are currently not allowed. *) primrec abs_pat :: "pat \ btrm \ btrm" ("(3\[_]./ _)" [0, 10] 10) where "(\[PVar x T]. t) = Bind T x t" | "(\[\\p, q\\]. t) = (\[p]. \[q]. t)" lemma abs_pat_eqvt [eqvt]: "(pi :: name prm) \ (\[p]. t) = (\[pi \ p]. (pi \ t))" by (induct p arbitrary: t) simp_all lemma abs_pat_fresh [simp]: "(x::name) \ (\[p]. t) = (x \ supp p \ x \ t)" by (induct p arbitrary: t) (simp_all add: abs_fresh supp_atm) lemma abs_pat_alpha: assumes fresh: "((pi::name prm) \ supp p::name set) \* t" and pi: "set pi \ supp p \ pi \ supp p" shows "(\[p]. t) = (\[pi \ p]. pi \ t)" proof - note pt_name_inst at_name_inst pi moreover have "(supp p::name set) \* (\[p]. t)" by (simp add: fresh_star_def) moreover from fresh have "(pi \ supp p::name set) \* (\[p]. t)" by (simp add: fresh_star_def) ultimately have "pi \ (\[p]. t) = (\[p]. t)" by (rule pt_freshs_freshs) then show ?thesis by (simp add: eqvts) qed primrec pat_vars :: "pat \ name list" where "pat_vars (PVar x T) = [x]" | "pat_vars \\p, q\\ = pat_vars q @ pat_vars p" lemma pat_vars_eqvt [eqvt]: "(pi :: name prm) \ (pat_vars p) = pat_vars (pi \ p)" by (induct p rule: pat.induct) (simp_all add: eqvts) lemma set_pat_vars_supp: "set (pat_vars p) = supp p" by (induct p) (auto simp add: supp_atm) lemma distinct_eqvt [eqvt]: "(pi :: name prm) \ (distinct (xs::name list)) = distinct (pi \ xs)" by (induct xs) (simp_all add: eqvts) primrec pat_type :: "pat \ ty" where "pat_type (PVar x T) = T" | "pat_type \\p, q\\ = pat_type p \ pat_type q" lemma pat_type_eqvt [eqvt]: "(pi :: name prm) \ (pat_type p) = pat_type (pi \ p)" by (induct p) simp_all lemma pat_type_perm_eq: "pat_type ((pi :: name prm) \ p) = pat_type p" by (induct p) (simp_all add: perm_type) type_synonym ctx = "(name \ ty) list" inductive ptyping :: "pat \ ty \ ctx \ bool" ("\ _ : _ \ _" [60, 60, 60] 60) where PVar: "\ PVar x T : T \ [(x, T)]" | PTuple: "\ p : T \ \\<^sub>1 \ \ q : U \ \\<^sub>2 \ \ \\p, q\\ : T \ U \ \\<^sub>2 @ \\<^sub>1" lemma pat_vars_ptyping: assumes "\ p : T \ \" shows "pat_vars p = map fst \" using assms by induct simp_all inductive valid :: "ctx \ bool" where Nil [intro!]: "valid []" | Cons [intro!]: "valid \ \ x \ \ \ valid ((x, T) # \)" inductive_cases validE[elim!]: "valid ((x, T) # \)" lemma fresh_ctxt_set_eq: "((x::name) \ (\::ctx)) = (x \ fst ` set \)" by (induct \) (auto simp add: fresh_list_nil fresh_list_cons fresh_prod fresh_atm) lemma valid_distinct: "valid \ = distinct (map fst \)" by (induct \) (auto simp add: fresh_ctxt_set_eq [symmetric]) abbreviation "sub_ctx" :: "ctx \ ctx \ bool" ("_ \ _") where "\\<^sub>1 \ \\<^sub>2 \ \x. x \ set \\<^sub>1 \ x \ set \\<^sub>2" abbreviation Let_syn :: "pat \ trm \ trm \ trm" ("(LET (_ =/ _)/ IN (_))" 10) where "LET p = t IN u \ Let (pat_type p) t (\[p]. Base u)" inductive typing :: "ctx \ trm \ ty \ bool" ("_ \ _ : _" [60, 60, 60] 60) where Var [intro]: "valid \ \ (x, T) \ set \ \ \ \ Var x : T" | Tuple [intro]: "\ \ t : T \ \ \ u : U \ \ \ \t, u\ : T \ U" | Abs [intro]: "(x, T) # \ \ t : U \ \ \ (\x:T. t) : T \ U" | App [intro]: "\ \ t : T \ U \ \ \ u : T \ \ \ t \ u : U" | Let: "((supp p)::name set) \* t \ \ \ t : T \ \ p : T \ \ \ \ @ \ \ u : U \ \ \ (LET p = t IN u) : U" equivariance ptyping equivariance valid equivariance typing lemma valid_typing: assumes "\ \ t : T" shows "valid \" using assms by induct auto lemma pat_var: assumes "\ p : T \ \" shows "(supp p::name set) = supp \" using assms by induct (auto simp add: supp_list_nil supp_list_cons supp_prod supp_list_append) lemma valid_app_fresh: assumes "valid (\ @ \)" and "(x::name) \ supp \" shows "x \ \" using assms by (induct \) (auto simp add: supp_list_nil supp_list_cons supp_prod supp_atm fresh_list_append) lemma pat_freshs: assumes "\ p : T \ \" shows "(supp p::name set) \* c = (supp \::name set) \* c" using assms by (auto simp add: fresh_star_def pat_var) lemma valid_app_mono: assumes "valid (\ @ \\<^sub>1)" and "(supp \::name set) \* \\<^sub>2" and "valid \\<^sub>2" and "\\<^sub>1 \ \\<^sub>2" shows "valid (\ @ \\<^sub>2)" using assms by (induct \) (auto simp add: supp_list_cons fresh_star_Un_elim supp_prod fresh_list_append supp_atm fresh_star_insert_elim fresh_star_empty_elim) nominal_inductive2 typing avoids Abs: "{x}" | Let: "(supp p)::name set" by (auto simp add: fresh_star_def abs_fresh fin_supp pat_var dest!: valid_typing valid_app_fresh) lemma better_T_Let [intro]: assumes t: "\ \ t : T" and p: "\ p : T \ \" and u: "\ @ \ \ u : U" shows "\ \ (LET p = t IN u) : U" proof - obtain pi::"name prm" where pi: "(pi \ (supp p::name set)) \* (t, Base u, \)" and pi': "set pi \ supp p \ (pi \ supp p)" by (rule at_set_avoiding [OF at_name_inst fin_supp fin_supp]) from p u have p_fresh: "(supp p::name set) \* \" by (auto simp add: fresh_star_def pat_var dest!: valid_typing valid_app_fresh) from pi have p_fresh': "(pi \ (supp p::name set)) \* \" by (simp add: fresh_star_prod_elim) from pi have p_fresh'': "(pi \ (supp p::name set)) \* Base u" by (simp add: fresh_star_prod_elim) from pi have "(supp (pi \ p)::name set) \* t" by (simp add: fresh_star_prod_elim eqvts) moreover note t moreover from p have "pi \ (\ p : T \ \)" by (rule perm_boolI) then have "\ (pi \ p) : T \ (pi \ \)" by (simp add: eqvts perm_type) moreover from u have "pi \ (\ @ \ \ u : U)" by (rule perm_boolI) with pt_freshs_freshs [OF pt_name_inst at_name_inst pi' p_fresh p_fresh'] have "(pi \ \) @ \ \ (pi \ u) : U" by (simp add: eqvts perm_type) ultimately have "\ \ (LET (pi \ p) = t IN (pi \ u)) : U" by (rule Let) then show ?thesis by (simp add: abs_pat_alpha [OF p_fresh'' pi'] pat_type_perm_eq) qed lemma weakening: assumes "\\<^sub>1 \ t : T" and "valid \\<^sub>2" and "\\<^sub>1 \ \\<^sub>2" shows "\\<^sub>2 \ t : T" using assms proof (nominal_induct \\<^sub>1 t T avoiding: \\<^sub>2 rule: typing.strong_induct) case (Abs x T \ t U) then show ?case by (simp add: typing.Abs valid.Cons) next case (Let p t \ T \ u U) then show ?case by (smt (verit, ccfv_threshold) Un_iff pat_freshs set_append typing.simps valid_app_mono valid_typing) qed auto inductive match :: "pat \ trm \ (name \ trm) list \ bool" ("\ _ \ _ \ _" [50, 50, 50] 50) where PVar: "\ PVar x T \ t \ [(x, t)]" | PProd: "\ p \ t \ \ \ \ q \ u \ \' \ \ \\p, q\\ \ \t, u\ \ \ @ \'" fun lookup :: "(name \ trm) list \ name \ trm" where "lookup [] x = Var x" | "lookup ((y, e) # \) x = (if x = y then e else lookup \ x)" lemma lookup_eqvt[eqvt]: fixes pi :: "name prm" and \ :: "(name \ trm) list" and X :: "name" shows "pi \ (lookup \ X) = lookup (pi \ \) (pi \ X)" by (induct \) (auto simp add: eqvts) nominal_primrec psubst :: "(name \ trm) list \ trm \ trm" ("_\_\" [95,0] 210) and psubstb :: "(name \ trm) list \ btrm \ btrm" ("_\_\\<^sub>b" [95,0] 210) where "\\Var x\ = (lookup \ x)" | "\\t \ u\ = \\t\ \ \\u\" | "\\\t, u\\ = \\\t\, \\u\\" | "\\Let T t u\ = Let T (\\t\) (\\u\\<^sub>b)" | "x \ \ \ \\\x:T. t\ = (\x:T. \\t\)" | "\\Base t\\<^sub>b = Base (\\t\)" | "x \ \ \ \\Bind T x t\\<^sub>b = Bind T x (\\t\\<^sub>b)" by (finite_guess | simp add: abs_fresh | fresh_guess)+ lemma lookup_fresh: "x = y \ x \ set (map fst \) \ \(y, t)\set \. x \ t \ x \ lookup \ y" by (induct \) (use fresh_atm in force)+ lemma psubst_fresh: assumes "x \ set (map fst \)" and "\(y, t)\set \. x \ t" shows "x \ \\t\" and "x \ \\t'\\<^sub>b" using assms proof (nominal_induct t and t' avoiding: \ rule: trm_btrm.strong_inducts) case (Var name) then show ?case by (metis lookup_fresh simps(1)) qed (auto simp: abs_fresh) lemma psubst_eqvt[eqvt]: fixes pi :: "name prm" shows "pi \ (\\t\) = (pi \ \)\pi \ t\" and "pi \ (\\t'\\<^sub>b) = (pi \ \)\pi \ t'\\<^sub>b" by (nominal_induct t and t' avoiding: \ rule: trm_btrm.strong_inducts) (simp_all add: eqvts fresh_bij) abbreviation subst :: "trm \ name \ trm \ trm" ("_[_\_]" [100,0,0] 100) where "t[x\t'] \ [(x,t')]\t\" abbreviation substb :: "btrm \ name \ trm \ btrm" ("_[_\_]\<^sub>b" [100,0,0] 100) where "t[x\t']\<^sub>b \ [(x,t')]\t\\<^sub>b" lemma lookup_forget: "(supp (map fst \)::name set) \* x \ lookup \ x = Var x" by (induct \) (auto simp add: split_paired_all fresh_star_def fresh_atm supp_list_cons supp_atm) lemma supp_fst: "(x::name) \ supp (map fst (\::(name \ trm) list)) \ x \ supp \" by (induct \) (auto simp add: supp_list_nil supp_list_cons supp_prod) lemma psubst_forget: "(supp (map fst \)::name set) \* t \ \\t\ = t" "(supp (map fst \)::name set) \* t' \ \\t'\\<^sub>b = t'" proof (nominal_induct t and t' avoiding: \ rule: trm_btrm.strong_inducts) case (Var name) then show ?case by (simp add: fresh_star_set lookup_forget) next case (Abs ty name trm) then show ?case apply (simp add: fresh_def) by (metis abs_fresh(1) fresh_star_set supp_fst trm.fresh(3)) next case (Bind ty name btrm) then show ?case apply (simp add: fresh_def) by (metis abs_fresh(1) btrm.fresh(2) fresh_star_set supp_fst) qed (auto simp: fresh_star_set) -lemma psubst_nil: "[]\t\ = t" "[]\t'\\<^sub>b = t'" +lemma psubst_nil[simp]: "[]\t\ = t" "[]\t'\\<^sub>b = t'" by (induct t and t' rule: trm_btrm.inducts) (simp_all add: fresh_list_nil) lemma psubst_cons: assumes "(supp (map fst \)::name set) \* u" shows "((x, u) # \)\t\ = \\t[x\u]\" and "((x, u) # \)\t'\\<^sub>b = \\t'[x\u]\<^sub>b\\<^sub>b" using assms by (nominal_induct t and t' avoiding: x u \ rule: trm_btrm.strong_inducts) (simp_all add: fresh_list_nil fresh_list_cons psubst_forget) lemma psubst_append: "(supp (map fst (\\<^sub>1 @ \\<^sub>2))::name set) \* map snd (\\<^sub>1 @ \\<^sub>2) \ (\\<^sub>1 @ \\<^sub>2)\t\ = \\<^sub>2\\\<^sub>1\t\\" - by (induct \\<^sub>1 arbitrary: t) - (simp_all add: psubst_nil split_paired_all supp_list_cons psubst_cons fresh_star_def - fresh_list_cons fresh_list_append supp_list_append) +proof (induct \\<^sub>1 arbitrary: t) + case Nil + then show ?case + by (auto simp: psubst_nil) +next + case (Cons a \\<^sub>1) + then show ?case + proof (cases a) + case (Pair a b) + with Cons show ?thesis + apply (simp add: supp_list_cons fresh_star_set fresh_list_cons) + by (metis Un_iff fresh_star_set map_append psubst_cons(1) supp_list_append) + qed +qed lemma abs_pat_psubst [simp]: "(supp p::name set) \* \ \ \\\[p]. t\\<^sub>b = (\[p]. \\t\\<^sub>b)" by (induct p arbitrary: t) (auto simp add: fresh_star_def supp_atm) lemma valid_insert: assumes "valid (\ @ [(x, T)] @ \)" shows "valid (\ @ \)" using assms by (induct \) (auto simp add: fresh_list_append fresh_list_cons) lemma fresh_set: shows "y \ xs = (\x\set xs. y \ x)" by (induct xs) (simp_all add: fresh_list_nil fresh_list_cons) lemma context_unique: assumes "valid \" and "(x, T) \ set \" and "(x, U) \ set \" shows "T = U" using assms by induct (auto simp add: fresh_set fresh_prod fresh_atm) lemma subst_type_aux: assumes a: "\ @ [(x, U)] @ \ \ t : T" and b: "\ \ u : U" shows "\ @ \ \ t[x\u] : T" using a b proof (nominal_induct \'\"\ @ [(x, U)] @ \" t T avoiding: x u \ rule: typing.strong_induct) case (Var y T x u \) from \valid (\ @ [(x, U)] @ \)\ have valid: "valid (\ @ \)" by (rule valid_insert) show "\ @ \ \ Var y[x\u] : T" proof cases assume eq: "x = y" from Var eq have "T = U" by (auto intro: context_unique) with Var eq valid show "\ @ \ \ Var y[x\u] : T" by (auto intro: weakening) next assume ineq: "x \ y" from Var ineq have "(y, T) \ set (\ @ \)" by simp then show "\ @ \ \ Var y[x\u] : T" using ineq valid by auto qed next case (Tuple t\<^sub>1 T\<^sub>1 t\<^sub>2 T\<^sub>2) from refl \\ \ u : U\ have "\ @ \ \ t\<^sub>1[x\u] : T\<^sub>1" by (rule Tuple) moreover from refl \\ \ u : U\ have "\ @ \ \ t\<^sub>2[x\u] : T\<^sub>2" by (rule Tuple) ultimately have "\ @ \ \ \t\<^sub>1[x\u], t\<^sub>2[x\u]\ : T\<^sub>1 \ T\<^sub>2" .. then show ?case by simp next case (Let p t T \' s S) from refl \\ \ u : U\ have "\ @ \ \ t[x\u] : T" by (rule Let) moreover note \\ p : T \ \'\ moreover have "\' @ (\ @ [(x, U)] @ \) = (\' @ \) @ [(x, U)] @ \" by simp then have "(\' @ \) @ \ \ s[x\u] : S" using \\ \ u : U\ by (rule Let) then have "\' @ \ @ \ \ s[x\u] : S" by simp ultimately have "\ @ \ \ (LET p = t[x\u] IN s[x\u]) : S" by (rule better_T_Let) moreover from Let have "(supp p::name set) \* [(x, u)]" by (simp add: fresh_star_def fresh_list_nil fresh_list_cons) ultimately show ?case by simp next case (Abs y T t S) have "(y, T) # \ @ [(x, U)] @ \ = ((y, T) # \) @ [(x, U)] @ \" by simp then have "((y, T) # \) @ \ \ t[x\u] : S" using \\ \ u : U\ by (rule Abs) then have "(y, T) # \ @ \ \ t[x\u] : S" by simp then have "\ @ \ \ (\y:T. t[x\u]) : T \ S" by (rule typing.Abs) moreover from Abs have "y \ [(x, u)]" by (simp add: fresh_list_nil fresh_list_cons) ultimately show ?case by simp next case (App t\<^sub>1 T S t\<^sub>2) from refl \\ \ u : U\ have "\ @ \ \ t\<^sub>1[x\u] : T \ S" by (rule App) moreover from refl \\ \ u : U\ have "\ @ \ \ t\<^sub>2[x\u] : T" by (rule App) ultimately have "\ @ \ \ (t\<^sub>1[x\u]) \ (t\<^sub>2[x\u]) : S" by (rule typing.App) then show ?case by simp qed lemmas subst_type = subst_type_aux [of "[]", simplified] lemma match_supp_fst: assumes "\ p \ u \ \" shows "(supp (map fst \)::name set) = supp p" using assms by induct (simp_all add: supp_list_nil supp_list_cons supp_list_append) lemma match_supp_snd: assumes "\ p \ u \ \" shows "(supp (map snd \)::name set) = supp u" using assms by induct (simp_all add: supp_list_nil supp_list_cons supp_list_append trm.supp) lemma match_fresh: "\ p \ u \ \ \ (supp p::name set) \* u \ (supp (map fst \)::name set) \* map snd \" by (simp add: fresh_star_def fresh_def match_supp_fst match_supp_snd) lemma match_type_aux: assumes "\ p : U \ \" and "\\<^sub>2 \ u : U" and "\\<^sub>1 @ \ @ \\<^sub>2 \ t : T" and "\ p \ u \ \" and "(supp p::name set) \* u" shows "\\<^sub>1 @ \\<^sub>2 \ \\t\ : T" using assms proof (induct arbitrary: \\<^sub>1 \\<^sub>2 t u T \) case (PVar x U) from \\\<^sub>1 @ [(x, U)] @ \\<^sub>2 \ t : T\ \\\<^sub>2 \ u : U\ have "\\<^sub>1 @ \\<^sub>2 \ t[x\u] : T" by (rule subst_type_aux) moreover from \\ PVar x U \ u \ \\ have "\ = [(x, u)]" by cases simp_all ultimately show ?case by simp next case (PTuple p S \\<^sub>1 q U \\<^sub>2) from \\ \\p, q\\ \ u \ \\ obtain u\<^sub>1 u\<^sub>2 \\<^sub>1 \\<^sub>2 where u: "u = \u\<^sub>1, u\<^sub>2\" and \: "\ = \\<^sub>1 @ \\<^sub>2" and p: "\ p \ u\<^sub>1 \ \\<^sub>1" and q: "\ q \ u\<^sub>2 \ \\<^sub>2" by cases simp_all with PTuple have "\\<^sub>2 \ \u\<^sub>1, u\<^sub>2\ : S \ U" by simp then obtain u\<^sub>1: "\\<^sub>2 \ u\<^sub>1 : S" and u\<^sub>2: "\\<^sub>2 \ u\<^sub>2 : U" by cases (simp_all add: ty.inject trm.inject) note u\<^sub>1 moreover from \\\<^sub>1 @ (\\<^sub>2 @ \\<^sub>1) @ \\<^sub>2 \ t : T\ have "(\\<^sub>1 @ \\<^sub>2) @ \\<^sub>1 @ \\<^sub>2 \ t : T" by simp moreover note p moreover from \supp \\p, q\\ \* u\ and u have "(supp p::name set) \* u\<^sub>1" by (simp add: fresh_star_def) ultimately have \\<^sub>1: "(\\<^sub>1 @ \\<^sub>2) @ \\<^sub>2 \ \\<^sub>1\t\ : T" by (rule PTuple) note u\<^sub>2 moreover from \\<^sub>1 have "\\<^sub>1 @ \\<^sub>2 @ \\<^sub>2 \ \\<^sub>1\t\ : T" by simp moreover note q moreover from \supp \\p, q\\ \* u\ and u have "(supp q::name set) \* u\<^sub>2" by (simp add: fresh_star_def) ultimately have "\\<^sub>1 @ \\<^sub>2 \ \\<^sub>2\\\<^sub>1\t\\ : T" by (rule PTuple) moreover from \\ \\p, q\\ \ u \ \\ \supp \\p, q\\ \* u\ have "(supp (map fst \)::name set) \* map snd \" by (rule match_fresh) ultimately show ?case using \ by (simp add: psubst_append) qed lemmas match_type = match_type_aux [where \\<^sub>1="[]", simplified] inductive eval :: "trm \ trm \ bool" ("_ \ _" [60,60] 60) where TupleL: "t \ t' \ \t, u\ \ \t', u\" | TupleR: "u \ u' \ \t, u\ \ \t, u'\" | Abs: "t \ t' \ (\x:T. t) \ (\x:T. t')" | AppL: "t \ t' \ t \ u \ t' \ u" | AppR: "u \ u' \ t \ u \ t \ u'" | Beta: "x \ u \ (\x:T. t) \ u \ t[x\u]" | Let: "((supp p)::name set) \* t \ distinct (pat_vars p) \ \ p \ t \ \ \ (LET p = t IN u) \ \\u\" equivariance match equivariance eval lemma match_vars: assumes "\ p \ t \ \" and "x \ supp p" shows "x \ set (map fst \)" using assms by induct (auto simp add: supp_atm) lemma match_fresh_mono: assumes "\ p \ t \ \" and "(x::name) \ t" shows "\(y, t)\set \. x \ t" using assms by induct auto nominal_inductive2 eval avoids Abs: "{x}" | Beta: "{x}" | Let: "(supp p)::name set" proof (simp_all add: fresh_star_def abs_fresh fin_supp) show "x \ t[x\u]" if "x \ u" for x t u by (simp add: \x \ u\ psubst_fresh(1)) next show "\x\supp p. (x::name) \ \\u\" if "\x\supp p. (x::name) \ t" and "\ p \ t \ \" for p t \ u by (meson that match_fresh_mono match_vars psubst_fresh(1)) qed lemma typing_case_Abs: assumes ty: "\ \ (\x:T. t) : S" and fresh: "x \ \" and R: "\U. S = T \ U \ (x, T) # \ \ t : U \ P" shows P using ty proof cases case (Abs x' T' t' U) obtain y::name where y: "y \ (x, \, \x':T'. t')" by (rule exists_fresh) (auto intro: fin_supp) from \(\x:T. t) = (\x':T'. t')\ [symmetric] have x: "x \ (\x':T'. t')" by (simp add: abs_fresh) have x': "x' \ (\x':T'. t')" by (simp add: abs_fresh) from \(x', T') # \ \ t' : U\ have x'': "x' \ \" by (auto dest: valid_typing) have "(\x:T. t) = (\x':T'. t')" by fact also from x x' y have "\ = [(x, y)] \ [(x', y)] \ (\x':T'. t')" by (simp only: perm_fresh_fresh fresh_prod) also have "\ = (\x:T'. [(x, y)] \ [(x', y)] \ t')" by (simp add: swap_simps perm_fresh_fresh) finally have "(\x:T. t) = (\x:T'. [(x, y)] \ [(x', y)] \ t')" . then have T: "T = T'" and t: "[(x, y)] \ [(x', y)] \ t' = t" by (simp_all add: trm.inject alpha) from Abs T have "S = T \ U" by simp moreover from \(x', T') # \ \ t' : U\ have "[(x, y)] \ [(x', y)] \ ((x', T') # \ \ t' : U)" by (simp add: perm_bool) with T t y x'' fresh have "(x, T) # \ \ t : U" by (simp add: eqvts swap_simps perm_fresh_fresh fresh_prod) ultimately show ?thesis by (rule R) qed simp_all nominal_primrec ty_size :: "ty \ nat" where "ty_size (Atom n) = 0" | "ty_size (T \ U) = ty_size T + ty_size U + 1" | "ty_size (T \ U) = ty_size T + ty_size U + 1" by (rule TrueI)+ lemma bind_tuple_ineq: "ty_size (pat_type p) < ty_size U \ Bind U x t \ (\[p]. u)" by (induct p arbitrary: U x t u) (auto simp add: btrm.inject) lemma valid_appD: assumes "valid (\ @ \)" shows "valid \" "valid \" using assms by (induct \'\"\ @ \" arbitrary: \ \) (auto simp add: Cons_eq_append_conv fresh_list_append) lemma valid_app_freshs: assumes "valid (\ @ \)" shows "(supp \::name set) \* \" "(supp \::name set) \* \" using assms by (induct \'\"\ @ \" arbitrary: \ \) (auto simp add: Cons_eq_append_conv fresh_star_def fresh_list_nil fresh_list_cons supp_list_nil supp_list_cons fresh_list_append supp_prod fresh_prod supp_atm fresh_atm dest: notE [OF iffD1 [OF fresh_def]]) lemma perm_mem_left: "(x::name) \ ((pi::name prm) \ A) \ (rev pi \ x) \ A" by (drule perm_boolI [of _ "rev pi"]) (simp add: eqvts perm_pi_simp) lemma perm_mem_right: "(rev (pi::name prm) \ (x::name)) \ A \ x \ (pi \ A)" by (drule perm_boolI [of _ pi]) (simp add: eqvts perm_pi_simp) lemma perm_cases: assumes pi: "set pi \ A \ A" shows "((pi::name prm) \ B) \ A \ B" proof fix x assume "x \ pi \ B" then show "x \ A \ B" using pi proof (induct pi arbitrary: x B rule: rev_induct) case Nil then show ?case by simp next case (snoc y xs) then show ?case apply simp by (metis SigmaE perm_mem_left perm_pi_simp(2) pt_name2 swap_simps(3)) qed qed lemma abs_pat_alpha': assumes eq: "(\[p]. t) = (\[q]. u)" and ty: "pat_type p = pat_type q" and pv: "distinct (pat_vars p)" and qv: "distinct (pat_vars q)" shows "\pi::name prm. p = pi \ q \ t = pi \ u \ set pi \ (supp p \ supp q) \ (supp p \ supp q)" using assms proof (induct p arbitrary: q t u) case (PVar x T) note PVar' = this show ?case proof (cases q) case (PVar x' T') with \(\[PVar x T]. t) = (\[q]. u)\ have "x = x' \ t = u \ x \ x' \ t = [(x, x')] \ u \ x \ u" by (simp add: btrm.inject alpha) then show ?thesis proof assume "x = x' \ t = u" with PVar PVar' have "PVar x T = ([]::name prm) \ q \ t = ([]::name prm) \ u \ set ([]::name prm) \ (supp (PVar x T) \ supp q) \ (supp (PVar x T) \ supp q)" by simp then show ?thesis .. next assume "x \ x' \ t = [(x, x')] \ u \ x \ u" with PVar PVar' have "PVar x T = [(x, x')] \ q \ t = [(x, x')] \ u \ set [(x, x')] \ (supp (PVar x T) \ supp q) \ (supp (PVar x T) \ supp q)" by (simp add: perm_swap swap_simps supp_atm perm_type) then show ?thesis .. qed next case (PTuple p\<^sub>1 p\<^sub>2) with PVar have "ty_size (pat_type p\<^sub>1) < ty_size T" by simp then have "Bind T x t \ (\[p\<^sub>1]. \[p\<^sub>2]. u)" by (rule bind_tuple_ineq) moreover from PTuple PVar have "Bind T x t = (\[p\<^sub>1]. \[p\<^sub>2]. u)" by simp ultimately show ?thesis .. qed next case (PTuple p\<^sub>1 p\<^sub>2) note PTuple' = this show ?case proof (cases q) case (PVar x T) with PTuple have "ty_size (pat_type p\<^sub>1) < ty_size T" by auto then have "Bind T x u \ (\[p\<^sub>1]. \[p\<^sub>2]. t)" by (rule bind_tuple_ineq) moreover from PTuple PVar have "Bind T x u = (\[p\<^sub>1]. \[p\<^sub>2]. t)" by simp ultimately show ?thesis .. next case (PTuple p\<^sub>1' p\<^sub>2') with PTuple' have "(\[p\<^sub>1]. \[p\<^sub>2]. t) = (\[p\<^sub>1']. \[p\<^sub>2']. u)" by simp moreover from PTuple PTuple' have "pat_type p\<^sub>1 = pat_type p\<^sub>1'" by (simp add: ty.inject) moreover from PTuple' have "distinct (pat_vars p\<^sub>1)" by simp moreover from PTuple PTuple' have "distinct (pat_vars p\<^sub>1')" by simp ultimately have "\pi::name prm. p\<^sub>1 = pi \ p\<^sub>1' \ (\[p\<^sub>2]. t) = pi \ (\[p\<^sub>2']. u) \ set pi \ (supp p\<^sub>1 \ supp p\<^sub>1') \ (supp p\<^sub>1 \ supp p\<^sub>1')" by (rule PTuple') then obtain pi::"name prm" where "p\<^sub>1 = pi \ p\<^sub>1'" "(\[p\<^sub>2]. t) = pi \ (\[p\<^sub>2']. u)" and pi: "set pi \ (supp p\<^sub>1 \ supp p\<^sub>1') \ (supp p\<^sub>1 \ supp p\<^sub>1')" by auto from \(\[p\<^sub>2]. t) = pi \ (\[p\<^sub>2']. u)\ have "(\[p\<^sub>2]. t) = (\[pi \ p\<^sub>2']. pi \ u)" by (simp add: eqvts) moreover from PTuple PTuple' have "pat_type p\<^sub>2 = pat_type (pi \ p\<^sub>2')" by (simp add: ty.inject pat_type_perm_eq) moreover from PTuple' have "distinct (pat_vars p\<^sub>2)" by simp moreover from PTuple PTuple' have "distinct (pat_vars (pi \ p\<^sub>2'))" by (simp add: pat_vars_eqvt [symmetric] distinct_eqvt [symmetric]) ultimately have "\pi'::name prm. p\<^sub>2 = pi' \ pi \ p\<^sub>2' \ t = pi' \ pi \ u \ set pi' \ (supp p\<^sub>2 \ supp (pi \ p\<^sub>2')) \ (supp p\<^sub>2 \ supp (pi \ p\<^sub>2'))" by (rule PTuple') then obtain pi'::"name prm" where "p\<^sub>2 = pi' \ pi \ p\<^sub>2'" "t = pi' \ pi \ u" and pi': "set pi' \ (supp p\<^sub>2 \ supp (pi \ p\<^sub>2')) \ (supp p\<^sub>2 \ supp (pi \ p\<^sub>2'))" by auto from PTuple PTuple' have "pi \ distinct (pat_vars \\p\<^sub>1', p\<^sub>2'\\)" by simp then have "distinct (pat_vars \\pi \ p\<^sub>1', pi \ p\<^sub>2'\\)" by (simp only: eqvts) with \p\<^sub>1 = pi \ p\<^sub>1'\ PTuple' have fresh: "(supp p\<^sub>2 \ supp (pi \ p\<^sub>2') :: name set) \* p\<^sub>1" by (auto simp add: set_pat_vars_supp fresh_star_def fresh_def eqvts) from \p\<^sub>1 = pi \ p\<^sub>1'\ have "pi' \ (p\<^sub>1 = pi \ p\<^sub>1')" by (rule perm_boolI) with pt_freshs_freshs [OF pt_name_inst at_name_inst pi' fresh fresh] have "p\<^sub>1 = pi' \ pi \ p\<^sub>1'" by (simp add: eqvts) with \p\<^sub>2 = pi' \ pi \ p\<^sub>2'\ have "\\p\<^sub>1, p\<^sub>2\\ = (pi' @ pi) \ \\p\<^sub>1', p\<^sub>2'\\" by (simp add: pt_name2) moreover have "((supp p\<^sub>2 \ (pi \ supp p\<^sub>2')) \ (supp p\<^sub>2 \ (pi \ supp p\<^sub>2'))::(name \ name) set) \ (supp p\<^sub>2 \ (supp p\<^sub>1 \ supp p\<^sub>1' \ supp p\<^sub>2')) \ (supp p\<^sub>2 \ (supp p\<^sub>1 \ supp p\<^sub>1' \ supp p\<^sub>2'))" by (rule subset_refl Sigma_mono Un_mono perm_cases [OF pi])+ with pi' have "set pi' \ \" by (simp add: supp_eqvt [symmetric]) with pi have "set (pi' @ pi) \ (supp \\p\<^sub>1, p\<^sub>2\\ \ supp \\p\<^sub>1', p\<^sub>2'\\) \ (supp \\p\<^sub>1, p\<^sub>2\\ \ supp \\p\<^sub>1', p\<^sub>2'\\)" by (simp add: Sigma_Un_distrib1 Sigma_Un_distrib2 Un_ac) blast moreover note \t = pi' \ pi \ u\ ultimately have "\\p\<^sub>1, p\<^sub>2\\ = (pi' @ pi) \ q \ t = (pi' @ pi) \ u \ set (pi' @ pi) \ (supp \\p\<^sub>1, p\<^sub>2\\ \ supp q) \ (supp \\p\<^sub>1, p\<^sub>2\\ \ supp q)" using PTuple by (simp add: pt_name2) then show ?thesis .. qed qed lemma typing_case_Let: assumes ty: "\ \ (LET p = t IN u) : U" and fresh: "(supp p::name set) \* \" and distinct: "distinct (pat_vars p)" and R: "\T \. \ \ t : T \ \ p : T \ \ \ \ @ \ \ u : U \ P" shows P using ty proof cases case (Let p' t' T \ u') then have "(supp \::name set) \* \" by (auto intro: valid_typing valid_app_freshs) with Let have "(supp p'::name set) \* \" by (simp add: pat_var) with fresh have fresh': "(supp p \ supp p' :: name set) \* \" by (auto simp add: fresh_star_def) from Let have "(\[p]. Base u) = (\[p']. Base u')" by (simp add: trm.inject) moreover from Let have "pat_type p = pat_type p'" by (simp add: trm.inject) moreover note distinct moreover from \\ @ \ \ u' : U\ have "valid (\ @ \)" by (rule valid_typing) then have "valid \" by (rule valid_appD) with \\ p' : T \ \\ have "distinct (pat_vars p')" by (simp add: valid_distinct pat_vars_ptyping) ultimately have "\pi::name prm. p = pi \ p' \ Base u = pi \ Base u' \ set pi \ (supp p \ supp p') \ (supp p \ supp p')" by (rule abs_pat_alpha') then obtain pi::"name prm" where pi: "p = pi \ p'" "u = pi \ u'" and pi': "set pi \ (supp p \ supp p') \ (supp p \ supp p')" by (auto simp add: btrm.inject) from Let have "\ \ t : T" by (simp add: trm.inject) moreover from \\ p' : T \ \\ have "\ (pi \ p') : (pi \ T) \ (pi \ \)" by (simp add: ptyping.eqvt) with pi have "\ p : T \ (pi \ \)" by (simp add: perm_type) moreover from Let have "(pi \ \) @ (pi \ \) \ (pi \ u') : (pi \ U)" by (simp add: append_eqvt [symmetric] typing.eqvt) with pi have "(pi \ \) @ \ \ u : U" by (simp add: perm_type pt_freshs_freshs [OF pt_name_inst at_name_inst pi' fresh' fresh']) ultimately show ?thesis by (rule R) qed simp_all lemma preservation: assumes "t \ t'" and "\ \ t : T" shows "\ \ t' : T" using assms proof (nominal_induct avoiding: \ T rule: eval.strong_induct) case (TupleL t t' u) from \\ \ \t, u\ : T\ obtain T\<^sub>1 T\<^sub>2 where "T = T\<^sub>1 \ T\<^sub>2" "\ \ t : T\<^sub>1" "\ \ u : T\<^sub>2" by cases (simp_all add: trm.inject) from \\ \ t : T\<^sub>1\ have "\ \ t' : T\<^sub>1" by (rule TupleL) then have "\ \ \t', u\ : T\<^sub>1 \ T\<^sub>2" using \\ \ u : T\<^sub>2\ by (rule Tuple) with \T = T\<^sub>1 \ T\<^sub>2\ show ?case by simp next case (TupleR u u' t) from \\ \ \t, u\ : T\ obtain T\<^sub>1 T\<^sub>2 where "T = T\<^sub>1 \ T\<^sub>2" "\ \ t : T\<^sub>1" "\ \ u : T\<^sub>2" by cases (simp_all add: trm.inject) from \\ \ u : T\<^sub>2\ have "\ \ u' : T\<^sub>2" by (rule TupleR) with \\ \ t : T\<^sub>1\ have "\ \ \t, u'\ : T\<^sub>1 \ T\<^sub>2" by (rule Tuple) with \T = T\<^sub>1 \ T\<^sub>2\ show ?case by simp next case (Abs t t' x S) from \\ \ (\x:S. t) : T\ \x \ \\ obtain U where T: "T = S \ U" and U: "(x, S) # \ \ t : U" by (rule typing_case_Abs) from U have "(x, S) # \ \ t' : U" by (rule Abs) then have "\ \ (\x:S. t') : S \ U" by (rule typing.Abs) with T show ?case by simp next case (Beta x u S t) from \\ \ (\x:S. t) \ u : T\ \x \ \\ obtain "(x, S) # \ \ t : T" and "\ \ u : S" by cases (auto simp add: trm.inject ty.inject elim: typing_case_Abs) then show ?case by (rule subst_type) next case (Let p t \ u) from \\ \ (LET p = t IN u) : T\ \supp p \* \\ \distinct (pat_vars p)\ obtain U \ where "\ p : U \ \" "\ \ t : U" "\ @ \ \ u : T" by (rule typing_case_Let) then show ?case using \\ p \ t \ \\ \supp p \* t\ by (rule match_type) next case (AppL t t' u) from \\ \ t \ u : T\ obtain U where t: "\ \ t : U \ T" and u: "\ \ u : U" by cases (auto simp add: trm.inject) from t have "\ \ t' : U \ T" by (rule AppL) then show ?case using u by (rule typing.App) next case (AppR u u' t) from \\ \ t \ u : T\ obtain U where t: "\ \ t : U \ T" and u: "\ \ u : U" by cases (auto simp add: trm.inject) from u have "\ \ u' : U" by (rule AppR) with t show ?case by (rule typing.App) qed end diff --git a/src/HOL/Nominal/Nominal.thy b/src/HOL/Nominal/Nominal.thy --- a/src/HOL/Nominal/Nominal.thy +++ b/src/HOL/Nominal/Nominal.thy @@ -1,3430 +1,3430 @@ theory Nominal imports "HOL-Library.Infinite_Set" "HOL-Library.Old_Datatype" keywords "atom_decl" :: thy_decl and "nominal_datatype" :: thy_defn and "equivariance" :: thy_decl and "nominal_primrec" "nominal_inductive" "nominal_inductive2" :: thy_goal_defn and "avoids" begin declare [[typedef_overloaded]] section \Permutations\ (*======================*) type_synonym 'x prm = "('x \ 'x) list" (* polymorphic constants for permutation and swapping *) consts perm :: "'x prm \ 'a \ 'a" (infixr \\\ 80) swap :: "('x \ 'x) \ 'x \ 'x" (* a "private" copy of the option type used in the abstraction function *) datatype 'a noption = nSome 'a | nNone datatype_compat noption (* a "private" copy of the product type used in the nominal induct method *) datatype ('a, 'b) nprod = nPair 'a 'b datatype_compat nprod (* an auxiliary constant for the decision procedure involving *) (* permutations (to avoid loops when using perm-compositions) *) definition "perm_aux pi x = pi\x" (* overloaded permutation operations *) overloading perm_fun \ "perm :: 'x prm \ ('a\'b) \ ('a\'b)" (unchecked) perm_bool \ "perm :: 'x prm \ bool \ bool" (unchecked) perm_set \ "perm :: 'x prm \ 'a set \ 'a set" (unchecked) perm_unit \ "perm :: 'x prm \ unit \ unit" (unchecked) perm_prod \ "perm :: 'x prm \ ('a\'b) \ ('a\'b)" (unchecked) perm_list \ "perm :: 'x prm \ 'a list \ 'a list" (unchecked) perm_option \ "perm :: 'x prm \ 'a option \ 'a option" (unchecked) perm_char \ "perm :: 'x prm \ char \ char" (unchecked) perm_nat \ "perm :: 'x prm \ nat \ nat" (unchecked) perm_int \ "perm :: 'x prm \ int \ int" (unchecked) perm_noption \ "perm :: 'x prm \ 'a noption \ 'a noption" (unchecked) perm_nprod \ "perm :: 'x prm \ ('a, 'b) nprod \ ('a, 'b) nprod" (unchecked) begin definition perm_fun :: "'x prm \ ('a \ 'b) \ 'a \ 'b" where "perm_fun pi f = (\x. pi \ f (rev pi \ x))" definition perm_bool :: "'x prm \ bool \ bool" where "perm_bool pi b = b" definition perm_set :: "'x prm \ 'a set \ 'a set" where "perm_set pi X = {pi \ x | x. x \ X}" primrec perm_unit :: "'x prm \ unit \ unit" where "perm_unit pi () = ()" primrec perm_prod :: "'x prm \ ('a\'b) \ ('a\'b)" where "perm_prod pi (x, y) = (pi\x, pi\y)" primrec perm_list :: "'x prm \ 'a list \ 'a list" where nil_eqvt: "perm_list pi [] = []" | cons_eqvt: "perm_list pi (x#xs) = (pi\x)#(pi\xs)" primrec perm_option :: "'x prm \ 'a option \ 'a option" where some_eqvt: "perm_option pi (Some x) = Some (pi\x)" | none_eqvt: "perm_option pi None = None" definition perm_char :: "'x prm \ char \ char" where "perm_char pi c = c" definition perm_nat :: "'x prm \ nat \ nat" where "perm_nat pi i = i" definition perm_int :: "'x prm \ int \ int" where "perm_int pi i = i" primrec perm_noption :: "'x prm \ 'a noption \ 'a noption" where nsome_eqvt: "perm_noption pi (nSome x) = nSome (pi\x)" | nnone_eqvt: "perm_noption pi nNone = nNone" primrec perm_nprod :: "'x prm \ ('a, 'b) nprod \ ('a, 'b) nprod" where "perm_nprod pi (nPair x y) = nPair (pi\x) (pi\y)" end (* permutations on booleans *) lemmas perm_bool = perm_bool_def lemma true_eqvt [simp]: "pi \ True \ True" by (simp add: perm_bool_def) lemma false_eqvt [simp]: "pi \ False \ False" by (simp add: perm_bool_def) lemma perm_boolI: assumes a: "P" shows "pi\P" using a by (simp add: perm_bool) lemma perm_boolE: assumes a: "pi\P" shows "P" using a by (simp add: perm_bool) lemma if_eqvt: fixes pi::"'a prm" shows "pi\(if b then c1 else c2) = (if (pi\b) then (pi\c1) else (pi\c2))" by (simp add: perm_fun_def) lemma imp_eqvt: shows "pi\(A\B) = ((pi\A)\(pi\B))" by (simp add: perm_bool) lemma conj_eqvt: shows "pi\(A\B) = ((pi\A)\(pi\B))" by (simp add: perm_bool) lemma disj_eqvt: shows "pi\(A\B) = ((pi\A)\(pi\B))" by (simp add: perm_bool) lemma neg_eqvt: shows "pi\(\ A) = (\ (pi\A))" by (simp add: perm_bool) (* permutation on sets *) -lemma empty_eqvt: +lemma empty_eqvt[simp]: shows "pi\{} = {}" by (simp add: perm_set_def) lemma union_eqvt: shows "(pi\(X\Y)) = (pi\X) \ (pi\Y)" by (auto simp add: perm_set_def) lemma insert_eqvt: shows "pi\(insert x X) = insert (pi\x) (pi\X)" by (auto simp add: perm_set_def) (* permutations on products *) lemma fst_eqvt: "pi\(fst x) = fst (pi\x)" by (cases x) simp lemma snd_eqvt: "pi\(snd x) = snd (pi\x)" by (cases x) simp (* permutation on lists *) lemma append_eqvt: fixes pi :: "'x prm" and l1 :: "'a list" and l2 :: "'a list" shows "pi\(l1@l2) = (pi\l1)@(pi\l2)" by (induct l1) auto lemma rev_eqvt: fixes pi :: "'x prm" and l :: "'a list" shows "pi\(rev l) = rev (pi\l)" by (induct l) (simp_all add: append_eqvt) lemma set_eqvt: fixes pi :: "'x prm" and xs :: "'a list" shows "pi\(set xs) = set (pi\xs)" by (induct xs) (auto simp add: empty_eqvt insert_eqvt) (* permutation on characters and strings *) lemma perm_string: fixes s::"string" shows "pi\s = s" by (induct s)(auto simp add: perm_char_def) section \permutation equality\ (*==============================*) definition prm_eq :: "'x prm \ 'x prm \ bool" (\ _ \ _ \ [80,80] 80) where "pi1 \ pi2 \ (\a::'x. pi1\a = pi2\a)" section \Support, Freshness and Supports\ (*========================================*) definition supp :: "'a \ ('x set)" where "supp x = {a . (infinite {b . [(a,b)]\x \ x})}" definition fresh :: "'x \ 'a \ bool" (\_ \ _\ [80,80] 80) where "a \ x \ a \ supp x" definition supports :: "'x set \ 'a \ bool" (infixl \supports\ 80) where "S supports x \ (\a b. (a\S \ b\S \ [(a,b)]\x=x))" (* lemmas about supp *) lemma supp_fresh_iff: fixes x :: "'a" shows "(supp x) = {a::'x. \a\x}" by (simp add: fresh_def) -lemma supp_unit: +lemma supp_unit[simp]: shows "supp () = {}" by (simp add: supp_def) -lemma supp_set_empty: +lemma supp_set_empty[simp]: shows "supp {} = {}" by (force simp add: supp_def empty_eqvt) lemma supp_prod: fixes x :: "'a" and y :: "'b" shows "(supp (x,y)) = (supp x)\(supp y)" by (force simp add: supp_def Collect_imp_eq Collect_neg_eq) lemma supp_nprod: fixes x :: "'a" and y :: "'b" shows "(supp (nPair x y)) = (supp x)\(supp y)" by (force simp add: supp_def Collect_imp_eq Collect_neg_eq) -lemma supp_list_nil: +lemma supp_list_nil[simp]: shows "supp [] = {}" by (simp add: supp_def) lemma supp_list_cons: fixes x :: "'a" and xs :: "'a list" shows "supp (x#xs) = (supp x)\(supp xs)" by (auto simp add: supp_def Collect_imp_eq Collect_neg_eq) lemma supp_list_append: fixes xs :: "'a list" and ys :: "'a list" shows "supp (xs@ys) = (supp xs)\(supp ys)" by (induct xs) (auto simp add: supp_list_nil supp_list_cons) lemma supp_list_rev: fixes xs :: "'a list" shows "supp (rev xs) = (supp xs)" by (induct xs, auto simp add: supp_list_append supp_list_cons supp_list_nil) -lemma supp_bool: +lemma supp_bool[simp]: fixes x :: "bool" shows "supp x = {}" by (cases "x") (simp_all add: supp_def) -lemma supp_some: +lemma supp_some[simp]: fixes x :: "'a" shows "supp (Some x) = (supp x)" by (simp add: supp_def) -lemma supp_none: +lemma supp_none[simp]: fixes x :: "'a" shows "supp (None) = {}" by (simp add: supp_def) -lemma supp_int: +lemma supp_int[simp]: fixes i::"int" shows "supp (i) = {}" by (simp add: supp_def perm_int_def) -lemma supp_nat: +lemma supp_nat[simp]: fixes n::"nat" shows "(supp n) = {}" by (simp add: supp_def perm_nat_def) -lemma supp_char: +lemma supp_char[simp]: fixes c::"char" shows "(supp c) = {}" by (simp add: supp_def perm_char_def) -lemma supp_string: +lemma supp_string[simp]: fixes s::"string" shows "(supp s) = {}" by (simp add: supp_def perm_string) (* lemmas about freshness *) -lemma fresh_set_empty: +lemma fresh_set_empty[simp]: shows "a\{}" by (simp add: fresh_def supp_set_empty) -lemma fresh_unit: +lemma fresh_unit[simp]: shows "a\()" by (simp add: fresh_def supp_unit) lemma fresh_prod: fixes a :: "'x" and x :: "'a" and y :: "'b" shows "a\(x,y) = (a\x \ a\y)" by (simp add: fresh_def supp_prod) -lemma fresh_list_nil: +lemma fresh_list_nil[simp]: fixes a :: "'x" shows "a\[]" by (simp add: fresh_def supp_list_nil) lemma fresh_list_cons: fixes a :: "'x" and x :: "'a" and xs :: "'a list" shows "a\(x#xs) = (a\x \ a\xs)" by (simp add: fresh_def supp_list_cons) lemma fresh_list_append: fixes a :: "'x" and xs :: "'a list" and ys :: "'a list" shows "a\(xs@ys) = (a\xs \ a\ys)" by (simp add: fresh_def supp_list_append) -lemma fresh_list_rev: +lemma fresh_list_rev[simp]: fixes a :: "'x" and xs :: "'a list" shows "a\(rev xs) = a\xs" by (simp add: fresh_def supp_list_rev) -lemma fresh_none: +lemma fresh_none[simp]: fixes a :: "'x" shows "a\None" by (simp add: fresh_def supp_none) -lemma fresh_some: +lemma fresh_some[simp]: fixes a :: "'x" and x :: "'a" shows "a\(Some x) = a\x" by (simp add: fresh_def supp_some) -lemma fresh_int: +lemma fresh_int[simp]: fixes a :: "'x" and i :: "int" shows "a\i" by (simp add: fresh_def supp_int) -lemma fresh_nat: +lemma fresh_nat[simp]: fixes a :: "'x" and n :: "nat" shows "a\n" by (simp add: fresh_def supp_nat) -lemma fresh_char: +lemma fresh_char[simp]: fixes a :: "'x" and c :: "char" shows "a\c" by (simp add: fresh_def supp_char) -lemma fresh_string: +lemma fresh_string[simp]: fixes a :: "'x" and s :: "string" shows "a\s" by (simp add: fresh_def supp_string) -lemma fresh_bool: +lemma fresh_bool[simp]: fixes a :: "'x" and b :: "bool" shows "a\b" by (simp add: fresh_def supp_bool) text \Normalization of freshness results; cf.\ \nominal_induct\\ lemma fresh_unit_elim: shows "(a\() \ PROP C) \ PROP C" by (simp add: fresh_def supp_unit) lemma fresh_prod_elim: shows "(a\(x,y) \ PROP C) \ (a\x \ a\y \ PROP C)" by rule (simp_all add: fresh_prod) (* this rule needs to be added before the fresh_prodD is *) (* added to the simplifier with mksimps *) lemma [simp]: shows "a\x1 \ a\x2 \ a\(x1,x2)" by (simp add: fresh_prod) lemma fresh_prodD: shows "a\(x,y) \ a\x" and "a\(x,y) \ a\y" by (simp_all add: fresh_prod) ML \ val mksimps_pairs = (\<^const_name>\Nominal.fresh\, @{thms fresh_prodD}) :: mksimps_pairs; \ declaration \fn _ => Simplifier.map_ss (Simplifier.set_mksimps (mksimps mksimps_pairs)) \ section \Abstract Properties for Permutations and Atoms\ (*=========================================================*) (* properties for being a permutation type *) definition "pt TYPE('a) TYPE('x) \ (\(x::'a). ([]::'x prm)\x = x) \ (\(pi1::'x prm) (pi2::'x prm) (x::'a). (pi1@pi2)\x = pi1\(pi2\x)) \ (\(pi1::'x prm) (pi2::'x prm) (x::'a). pi1 \ pi2 \ pi1\x = pi2\x)" (* properties for being an atom type *) definition "at TYPE('x) \ (\(x::'x). ([]::'x prm)\x = x) \ (\(a::'x) (b::'x) (pi::'x prm) (x::'x). ((a,b)#(pi::'x prm))\x = swap (a,b) (pi\x)) \ (\(a::'x) (b::'x) (c::'x). swap (a,b) c = (if a=c then b else (if b=c then a else c))) \ (infinite (UNIV::'x set))" (* property of two atom-types being disjoint *) definition "disjoint TYPE('x) TYPE('y) \ (\(pi::'x prm)(x::'y). pi\x = x) \ (\(pi::'y prm)(x::'x). pi\x = x)" (* composition property of two permutation on a type 'a *) definition "cp TYPE ('a) TYPE('x) TYPE('y) \ (\(pi2::'y prm) (pi1::'x prm) (x::'a) . pi1\(pi2\x) = (pi1\pi2)\(pi1\x))" (* property of having finite support *) definition "fs TYPE('a) TYPE('x) \ \(x::'a). finite ((supp x)::'x set)" section \Lemmas about the atom-type properties\ (*==============================================*) lemma at1: fixes x::"'x" assumes a: "at TYPE('x)" shows "([]::'x prm)\x = x" using a by (simp add: at_def) lemma at2: fixes a ::"'x" and b ::"'x" and x ::"'x" and pi::"'x prm" assumes a: "at TYPE('x)" shows "((a,b)#pi)\x = swap (a,b) (pi\x)" using a by (simp only: at_def) lemma at3: fixes a ::"'x" and b ::"'x" and c ::"'x" assumes a: "at TYPE('x)" shows "swap (a,b) c = (if a=c then b else (if b=c then a else c))" using a by (simp only: at_def) (* rules to calculate simple permutations *) lemmas at_calc = at2 at1 at3 lemma at_swap_simps: fixes a ::"'x" and b ::"'x" assumes a: "at TYPE('x)" shows "[(a,b)]\a = b" and "[(a,b)]\b = a" and "\a\c; b\c\ \ [(a,b)]\c = c" using a by (simp_all add: at_calc) lemma at4: assumes a: "at TYPE('x)" shows "infinite (UNIV::'x set)" using a by (simp add: at_def) lemma at_append: fixes pi1 :: "'x prm" and pi2 :: "'x prm" and c :: "'x" assumes at: "at TYPE('x)" shows "(pi1@pi2)\c = pi1\(pi2\c)" proof (induct pi1) case Nil show ?case by (simp add: at1[OF at]) next case (Cons x xs) have "(xs@pi2)\c = xs\(pi2\c)" by fact also have "(x#xs)@pi2 = x#(xs@pi2)" by simp ultimately show ?case by (cases "x", simp add: at2[OF at]) qed lemma at_swap: fixes a :: "'x" and b :: "'x" and c :: "'x" assumes at: "at TYPE('x)" shows "swap (a,b) (swap (a,b) c) = c" by (auto simp add: at3[OF at]) lemma at_rev_pi: fixes pi :: "'x prm" and c :: "'x" assumes at: "at TYPE('x)" shows "(rev pi)\(pi\c) = c" proof(induct pi) case Nil show ?case by (simp add: at1[OF at]) next case (Cons x xs) thus ?case by (cases "x", simp add: at2[OF at] at_append[OF at] at1[OF at] at_swap[OF at]) qed lemma at_pi_rev: fixes pi :: "'x prm" and x :: "'x" assumes at: "at TYPE('x)" shows "pi\((rev pi)\x) = x" by (rule at_rev_pi[OF at, of "rev pi" _,simplified]) lemma at_bij1: fixes pi :: "'x prm" and x :: "'x" and y :: "'x" assumes at: "at TYPE('x)" and a: "(pi\x) = y" shows "x=(rev pi)\y" proof - from a have "y=(pi\x)" by (rule sym) thus ?thesis by (simp only: at_rev_pi[OF at]) qed lemma at_bij2: fixes pi :: "'x prm" and x :: "'x" and y :: "'x" assumes at: "at TYPE('x)" and a: "((rev pi)\x) = y" shows "x=pi\y" proof - from a have "y=((rev pi)\x)" by (rule sym) thus ?thesis by (simp only: at_pi_rev[OF at]) qed lemma at_bij: fixes pi :: "'x prm" and x :: "'x" and y :: "'x" assumes at: "at TYPE('x)" shows "(pi\x = pi\y) = (x=y)" proof assume "pi\x = pi\y" hence "x=(rev pi)\(pi\y)" by (rule at_bij1[OF at]) thus "x=y" by (simp only: at_rev_pi[OF at]) next assume "x=y" thus "pi\x = pi\y" by simp qed lemma at_supp: fixes x :: "'x" assumes at: "at TYPE('x)" shows "supp x = {x}" by(auto simp: supp_def Collect_conj_eq Collect_imp_eq at_calc[OF at] at4[OF at]) lemma at_fresh: fixes a :: "'x" and b :: "'x" assumes at: "at TYPE('x)" shows "(a\b) = (a\b)" by (simp add: at_supp[OF at] fresh_def) lemma at_prm_fresh1: fixes c :: "'x" and pi:: "'x prm" assumes at: "at TYPE('x)" and a: "c\pi" shows "\(a,b)\set pi. c\a \ c\b" using a by (induct pi) (auto simp add: fresh_list_cons fresh_prod at_fresh[OF at]) lemma at_prm_fresh2: fixes c :: "'x" and pi:: "'x prm" assumes at: "at TYPE('x)" and a: "\(a,b)\set pi. c\a \ c\b" shows "pi\c = c" using a by(induct pi) (auto simp add: at1[OF at] at2[OF at] at3[OF at]) lemma at_prm_fresh: fixes c :: "'x" and pi:: "'x prm" assumes at: "at TYPE('x)" and a: "c\pi" shows "pi\c = c" by (rule at_prm_fresh2[OF at], rule at_prm_fresh1[OF at, OF a]) lemma at_prm_rev_eq: fixes pi1 :: "'x prm" and pi2 :: "'x prm" assumes at: "at TYPE('x)" shows "((rev pi1) \ (rev pi2)) = (pi1 \ pi2)" proof (simp add: prm_eq_def, auto) fix x assume "\x::'x. (rev pi1)\x = (rev pi2)\x" hence "(rev (pi1::'x prm))\(pi2\(x::'x)) = (rev (pi2::'x prm))\(pi2\x)" by simp hence "(rev (pi1::'x prm))\((pi2::'x prm)\x) = (x::'x)" by (simp add: at_rev_pi[OF at]) hence "(pi2::'x prm)\x = (pi1::'x prm)\x" by (simp add: at_bij2[OF at]) thus "pi1\x = pi2\x" by simp next fix x assume "\x::'x. pi1\x = pi2\x" hence "(pi1::'x prm)\((rev pi2)\x) = (pi2::'x prm)\((rev pi2)\(x::'x))" by simp hence "(pi1::'x prm)\((rev pi2)\(x::'x)) = x" by (simp add: at_pi_rev[OF at]) hence "(rev pi2)\x = (rev pi1)\(x::'x)" by (simp add: at_bij1[OF at]) thus "(rev pi1)\x = (rev pi2)\(x::'x)" by simp qed lemma at_prm_eq_append: fixes pi1 :: "'x prm" and pi2 :: "'x prm" and pi3 :: "'x prm" assumes at: "at TYPE('x)" and a: "pi1 \ pi2" shows "(pi3@pi1) \ (pi3@pi2)" using a by (simp add: prm_eq_def at_append[OF at] at_bij[OF at]) lemma at_prm_eq_append': fixes pi1 :: "'x prm" and pi2 :: "'x prm" and pi3 :: "'x prm" assumes at: "at TYPE('x)" and a: "pi1 \ pi2" shows "(pi1@pi3) \ (pi2@pi3)" using a by (simp add: prm_eq_def at_append[OF at]) lemma at_prm_eq_trans: fixes pi1 :: "'x prm" and pi2 :: "'x prm" and pi3 :: "'x prm" assumes a1: "pi1 \ pi2" and a2: "pi2 \ pi3" shows "pi1 \ pi3" using a1 a2 by (auto simp add: prm_eq_def) lemma at_prm_eq_refl: fixes pi :: "'x prm" shows "pi \ pi" by (simp add: prm_eq_def) lemma at_prm_rev_eq1: fixes pi1 :: "'x prm" and pi2 :: "'x prm" assumes at: "at TYPE('x)" shows "pi1 \ pi2 \ (rev pi1) \ (rev pi2)" by (simp add: at_prm_rev_eq[OF at]) lemma at_ds1: fixes a :: "'x" assumes at: "at TYPE('x)" shows "[(a,a)] \ []" by (force simp add: prm_eq_def at_calc[OF at]) lemma at_ds2: fixes pi :: "'x prm" and a :: "'x" and b :: "'x" assumes at: "at TYPE('x)" shows "([(a,b)]@pi) \ (pi@[((rev pi)\a,(rev pi)\b)])" by (force simp add: prm_eq_def at_append[OF at] at_bij[OF at] at_pi_rev[OF at] at_rev_pi[OF at] at_calc[OF at]) lemma at_ds3: fixes a :: "'x" and b :: "'x" and c :: "'x" assumes at: "at TYPE('x)" and a: "distinct [a,b,c]" shows "[(a,c),(b,c),(a,c)] \ [(a,b)]" using a by (force simp add: prm_eq_def at_calc[OF at]) lemma at_ds4: fixes a :: "'x" and b :: "'x" and pi :: "'x prm" assumes at: "at TYPE('x)" shows "(pi@[(a,(rev pi)\b)]) \ ([(pi\a,b)]@pi)" by (force simp add: prm_eq_def at_append[OF at] at_calc[OF at] at_bij[OF at] at_pi_rev[OF at] at_rev_pi[OF at]) lemma at_ds5: fixes a :: "'x" and b :: "'x" assumes at: "at TYPE('x)" shows "[(a,b)] \ [(b,a)]" by (force simp add: prm_eq_def at_calc[OF at]) lemma at_ds5': fixes a :: "'x" and b :: "'x" assumes at: "at TYPE('x)" shows "[(a,b),(b,a)] \ []" by (force simp add: prm_eq_def at_calc[OF at]) lemma at_ds6: fixes a :: "'x" and b :: "'x" and c :: "'x" assumes at: "at TYPE('x)" and a: "distinct [a,b,c]" shows "[(a,c),(a,b)] \ [(b,c),(a,c)]" using a by (force simp add: prm_eq_def at_calc[OF at]) lemma at_ds7: fixes pi :: "'x prm" assumes at: "at TYPE('x)" shows "((rev pi)@pi) \ []" by (simp add: prm_eq_def at1[OF at] at_append[OF at] at_rev_pi[OF at]) lemma at_ds8_aux: fixes pi :: "'x prm" and a :: "'x" and b :: "'x" and c :: "'x" assumes at: "at TYPE('x)" shows "pi\(swap (a,b) c) = swap (pi\a,pi\b) (pi\c)" by (force simp add: at_calc[OF at] at_bij[OF at]) lemma at_ds8: fixes pi1 :: "'x prm" and pi2 :: "'x prm" and a :: "'x" and b :: "'x" assumes at: "at TYPE('x)" shows "(pi1@pi2) \ ((pi1\pi2)@pi1)" proof(induct_tac pi2) show "(pi1 @ []) \ (pi1 \ [] @ pi1)" by(simp add: prm_eq_def) show "\a l. (pi1 @ l) \ (pi1 \ l @ pi1) \ (pi1 @ a # l) \ (pi1 \ (a # l) @ pi1) " by(auto simp add: prm_eq_def at at2 at_append at_ds8_aux) qed lemma at_ds9: fixes pi1 :: "'x prm" and pi2 :: "'x prm" and a :: "'x" and b :: "'x" assumes at: "at TYPE('x)" shows " ((rev pi2)@(rev pi1)) \ ((rev pi1)@(rev (pi1\pi2)))" using at at_ds8 at_prm_rev_eq1 rev_append by fastforce lemma at_ds10: fixes pi :: "'x prm" and a :: "'x" and b :: "'x" assumes "at TYPE('x)" and "b\(rev pi)" shows "([(pi\a,b)]@pi) \ (pi@[(a,b)])" by (metis assms at_bij1 at_ds2 at_prm_fresh) \ \there always exists an atom that is not being in a finite set\ lemma ex_in_inf: fixes A::"'x set" assumes at: "at TYPE('x)" and fs: "finite A" obtains c::"'x" where "c\A" using at at4 ex_new_if_finite fs by blast text \there always exists a fresh name for an object with finite support\ lemma at_exists_fresh': fixes x :: "'a" assumes at: "at TYPE('x)" and fs: "finite ((supp x)::'x set)" shows "\c::'x. c\x" by (auto simp add: fresh_def intro: ex_in_inf[OF at, OF fs]) lemma at_exists_fresh: fixes x :: "'a" assumes at: "at TYPE('x)" and fs: "finite ((supp x)::'x set)" obtains c::"'x" where "c\x" by (auto intro: ex_in_inf[OF at, OF fs] simp add: fresh_def) lemma at_finite_select: fixes S::"'a set" assumes a: "at TYPE('a)" and b: "finite S" shows "\x. x \ S" by (meson a b ex_in_inf) lemma at_different: assumes at: "at TYPE('x)" shows "\(b::'x). a\b" proof - have "infinite (UNIV::'x set)" by (rule at4[OF at]) hence inf2: "infinite (UNIV-{a})" by (rule infinite_remove) have "(UNIV-{a}) \ ({}::'x set)" by (metis finite.emptyI inf2) hence "\(b::'x). b\(UNIV-{a})" by blast then obtain b::"'x" where mem2: "b\(UNIV-{a})" by blast from mem2 have "a\b" by blast then show "\(b::'x). a\b" by blast qed \ \the at-props imply the pt-props\ lemma at_pt_inst: assumes at: "at TYPE('x)" shows "pt TYPE('x) TYPE('x)" using at at_append at_def prm_eq_def pt_def by fastforce section \finite support properties\ (*===================================*) lemma fs1: fixes x :: "'a" assumes a: "fs TYPE('a) TYPE('x)" shows "finite ((supp x)::'x set)" using a by (simp add: fs_def) lemma fs_at_inst: fixes a :: "'x" assumes at: "at TYPE('x)" shows "fs TYPE('x) TYPE('x)" by (simp add: at at_supp fs_def) lemma fs_unit_inst: shows "fs TYPE(unit) TYPE('x)" by(simp add: fs_def supp_unit) lemma fs_prod_inst: assumes fsa: "fs TYPE('a) TYPE('x)" and fsb: "fs TYPE('b) TYPE('x)" shows "fs TYPE('a\'b) TYPE('x)" by (simp add: assms fs1 supp_prod fs_def) lemma fs_nprod_inst: assumes fsa: "fs TYPE('a) TYPE('x)" and fsb: "fs TYPE('b) TYPE('x)" shows "fs TYPE(('a,'b) nprod) TYPE('x)" unfolding fs_def by (metis assms finite_Un fs_def nprod.exhaust supp_nprod) lemma fs_list_inst: assumes "fs TYPE('a) TYPE('x)" shows "fs TYPE('a list) TYPE('x)" unfolding fs_def by (clarify, induct_tac x) (auto simp: fs1 assms supp_list_nil supp_list_cons) lemma fs_option_inst: assumes fs: "fs TYPE('a) TYPE('x)" shows "fs TYPE('a option) TYPE('x)" unfolding fs_def by (metis assms finite.emptyI fs1 option.exhaust supp_none supp_some) section \Lemmas about the permutation properties\ (*=================================================*) lemma pt1: fixes x::"'a" assumes a: "pt TYPE('a) TYPE('x)" shows "([]::'x prm)\x = x" using a by (simp add: pt_def) lemma pt2: fixes pi1::"'x prm" and pi2::"'x prm" and x ::"'a" assumes a: "pt TYPE('a) TYPE('x)" shows "(pi1@pi2)\x = pi1\(pi2\x)" using a by (simp add: pt_def) lemma pt3: fixes pi1::"'x prm" and pi2::"'x prm" and x ::"'a" assumes a: "pt TYPE('a) TYPE('x)" shows "pi1 \ pi2 \ pi1\x = pi2\x" using a by (simp add: pt_def) lemma pt3_rev: fixes pi1::"'x prm" and pi2::"'x prm" and x ::"'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "pi1 \ pi2 \ (rev pi1)\x = (rev pi2)\x" by (rule pt3[OF pt], simp add: at_prm_rev_eq[OF at]) section \composition properties\ (* ============================== *) lemma cp1: fixes pi1::"'x prm" and pi2::"'y prm" and x ::"'a" assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)" shows "pi1\(pi2\x) = (pi1\pi2)\(pi1\x)" using cp by (simp add: cp_def) lemma cp_pt_inst: assumes "pt TYPE('a) TYPE('x)" and "at TYPE('x)" shows "cp TYPE('a) TYPE('x) TYPE('x)" using assms at_ds8 cp_def pt2 pt3 by fastforce section \disjointness properties\ (*=================================*) lemma dj_perm_forget: fixes pi::"'y prm" and x ::"'x" assumes dj: "disjoint TYPE('x) TYPE('y)" shows "pi\x=x" using dj by (simp_all add: disjoint_def) lemma dj_perm_set_forget: fixes pi::"'y prm" and x ::"'x set" assumes dj: "disjoint TYPE('x) TYPE('y)" shows "pi\x=x" using dj by (simp_all add: perm_set_def disjoint_def) lemma dj_perm_perm_forget: fixes pi1::"'x prm" and pi2::"'y prm" assumes dj: "disjoint TYPE('x) TYPE('y)" shows "pi2\pi1=pi1" using dj by (induct pi1, auto simp add: disjoint_def) lemma dj_cp: fixes pi1::"'x prm" and pi2::"'y prm" and x ::"'a" assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)" and dj: "disjoint TYPE('y) TYPE('x)" shows "pi1\(pi2\x) = (pi2)\(pi1\x)" by (simp add: cp1[OF cp] dj_perm_perm_forget[OF dj]) lemma dj_supp: fixes a::"'x" assumes dj: "disjoint TYPE('x) TYPE('y)" shows "(supp a) = ({}::'y set)" by (simp add: supp_def dj_perm_forget[OF dj]) lemma at_fresh_ineq: fixes a :: "'x" and b :: "'y" assumes dj: "disjoint TYPE('y) TYPE('x)" shows "a\b" by (simp add: fresh_def dj_supp[OF dj]) section \permutation type instances\ (* ===================================*) lemma pt_fun_inst: assumes pta: "pt TYPE('a) TYPE('x)" and ptb: "pt TYPE('b) TYPE('x)" and at: "at TYPE('x)" shows "pt TYPE('a\'b) TYPE('x)" unfolding pt_def using assms by (auto simp add: perm_fun_def pt1 pt2 ptb pt3 pt3_rev) -lemma pt_bool_inst: +lemma pt_bool_inst[simp]: shows "pt TYPE(bool) TYPE('x)" by (simp add: pt_def perm_bool_def) lemma pt_set_inst: assumes pt: "pt TYPE('a) TYPE('x)" shows "pt TYPE('a set) TYPE('x)" unfolding pt_def by(auto simp add: perm_set_def pt1[OF pt] pt2[OF pt] pt3[OF pt]) -lemma pt_unit_inst: +lemma pt_unit_inst[simp]: shows "pt TYPE(unit) TYPE('x)" by (simp add: pt_def) lemma pt_prod_inst: assumes pta: "pt TYPE('a) TYPE('x)" and ptb: "pt TYPE('b) TYPE('x)" shows "pt TYPE('a \ 'b) TYPE('x)" using assms pt1 pt2 pt3 by(auto simp add: pt_def) lemma pt_list_nil: fixes xs :: "'a list" assumes pt: "pt TYPE('a) TYPE ('x)" shows "([]::'x prm)\xs = xs" by (induct_tac xs) (simp_all add: pt1[OF pt]) lemma pt_list_append: fixes pi1 :: "'x prm" and pi2 :: "'x prm" and xs :: "'a list" assumes pt: "pt TYPE('a) TYPE ('x)" shows "(pi1@pi2)\xs = pi1\(pi2\xs)" by (induct_tac xs) (simp_all add: pt2[OF pt]) lemma pt_list_prm_eq: fixes pi1 :: "'x prm" and pi2 :: "'x prm" and xs :: "'a list" assumes pt: "pt TYPE('a) TYPE ('x)" shows "pi1 \ pi2 \ pi1\xs = pi2\xs" by (induct_tac xs) (simp_all add: pt3[OF pt]) lemma pt_list_inst: assumes pt: "pt TYPE('a) TYPE('x)" shows "pt TYPE('a list) TYPE('x)" by (simp add: pt pt_def pt_list_append pt_list_nil pt_list_prm_eq) lemma pt_option_inst: assumes pta: "pt TYPE('a) TYPE('x)" shows "pt TYPE('a option) TYPE('x)" proof - have "([]::('x \ _) list) \ x = x" for x :: "'a option" by (metis assms none_eqvt not_None_eq pt1 some_eqvt) moreover have "(pi1 @ pi2) \ x = pi1 \ pi2 \ x" for pi1 pi2 :: "('x \ 'x) list" and x :: "'a option" by (metis assms none_eqvt option.collapse pt2 some_eqvt) moreover have "pi1 \ x = pi2 \ x" if "pi1 \ pi2" for pi1 pi2 :: "('x \ 'x) list" and x :: "'a option" using that pt3[OF pta] by (metis none_eqvt not_Some_eq some_eqvt) ultimately show ?thesis by (auto simp add: pt_def) qed lemma pt_noption_inst: assumes pta: "pt TYPE('a) TYPE('x)" shows "pt TYPE('a noption) TYPE('x)" proof - have "([]::('x \ _) list) \ x = x" for x :: "'a noption" by (metis assms nnone_eqvt noption.exhaust nsome_eqvt pt1) moreover have "(pi1 @ pi2) \ x = pi1 \ pi2 \ x" for pi1 pi2 :: "('x \ 'x) list" and x :: "'a noption" using pt2[OF pta] by (metis nnone_eqvt noption.exhaust nsome_eqvt) moreover have "pi1 \ x = pi2 \ x" if "pi1 \ pi2" for pi1 pi2 :: "('x \ 'x) list" and x :: "'a noption" using that pt3[OF pta] by (metis nnone_eqvt noption.exhaust nsome_eqvt) ultimately show ?thesis by (auto simp add: pt_def) qed lemma pt_nprod_inst: assumes pta: "pt TYPE('a) TYPE('x)" and ptb: "pt TYPE('b) TYPE('x)" shows "pt TYPE(('a,'b) nprod) TYPE('x)" proof - have "([]::('x \ _) list) \ x = x" for x :: "('a, 'b) nprod" by (metis assms(1) nprod.exhaust perm_nprod.simps pt1 ptb) moreover have "(pi1 @ pi2) \ x = pi1 \ pi2 \ x" for pi1 pi2 :: "('x \ 'x) list" and x :: "('a, 'b) nprod" using pt2[OF pta] pt2[OF ptb] by (metis nprod.exhaust perm_nprod.simps) moreover have "pi1 \ x = pi2 \ x" if "pi1 \ pi2" for pi1 pi2 :: "('x \ 'x) list" and x :: "('a, 'b) nprod" using that pt3[OF pta] pt3[OF ptb] by (smt (verit) nprod.exhaust perm_nprod.simps) ultimately show ?thesis by (auto simp add: pt_def) qed section \further lemmas for permutation types\ (*==============================================*) lemma pt_rev_pi: fixes pi :: "'x prm" and x :: "'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "(rev pi)\(pi\x) = x" proof - have "((rev pi)@pi) \ ([]::'x prm)" by (simp add: at_ds7[OF at]) hence "((rev pi)@pi)\(x::'a) = ([]::'x prm)\x" by (simp add: pt3[OF pt]) thus ?thesis by (simp add: pt1[OF pt] pt2[OF pt]) qed lemma pt_pi_rev: fixes pi :: "'x prm" and x :: "'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "pi\((rev pi)\x) = x" by (simp add: pt_rev_pi[OF pt, OF at,of "rev pi" "x",simplified]) lemma pt_bij1: fixes pi :: "'x prm" and x :: "'a" and y :: "'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and a: "(pi\x) = y" shows "x=(rev pi)\y" proof - from a have "y=(pi\x)" by (rule sym) thus ?thesis by (simp only: pt_rev_pi[OF pt, OF at]) qed lemma pt_bij2: fixes pi :: "'x prm" and x :: "'a" and y :: "'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and a: "x = (rev pi)\y" shows "(pi\x)=y" using a by (simp add: pt_pi_rev[OF pt, OF at]) lemma pt_bij: fixes pi :: "'x prm" and x :: "'a" and y :: "'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "(pi\x = pi\y) = (x=y)" proof assume "pi\x = pi\y" hence "x=(rev pi)\(pi\y)" by (rule pt_bij1[OF pt, OF at]) thus "x=y" by (simp only: pt_rev_pi[OF pt, OF at]) next assume "x=y" thus "pi\x = pi\y" by simp qed lemma pt_eq_eqvt: fixes pi :: "'x prm" and x :: "'a" and y :: "'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "pi\(x=y) = (pi\x = pi\y)" using pt at by (auto simp add: pt_bij perm_bool) lemma pt_bij3: fixes pi :: "'x prm" and x :: "'a" and y :: "'a" assumes a: "x=y" shows "(pi\x = pi\y)" using a by simp lemma pt_bij4: fixes pi :: "'x prm" and x :: "'a" and y :: "'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and a: "pi\x = pi\y" shows "x = y" using a by (simp add: pt_bij[OF pt, OF at]) lemma pt_swap_bij: fixes a :: "'x" and b :: "'x" and x :: "'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "[(a,b)]\([(a,b)]\x) = x" by (rule pt_bij2[OF pt, OF at], simp) lemma pt_swap_bij': fixes a :: "'x" and b :: "'x" and x :: "'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "[(a,b)]\([(b,a)]\x) = x" by (metis assms at_ds5 pt_def pt_swap_bij) lemma pt_swap_bij'': fixes a :: "'x" and x :: "'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "[(a,a)]\x = x" by (metis assms at_ds1 pt_def) lemma supp_singleton: shows "supp {x} = supp x" by (force simp add: supp_def perm_set_def) lemma fresh_singleton: shows "a\{x} = a\x" by (simp add: fresh_def supp_singleton) lemma pt_set_bij1: fixes pi :: "'x prm" and x :: "'a" and X :: "'a set" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "((pi\x)\X) = (x\((rev pi)\X))" by (force simp add: perm_set_def pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at]) lemma pt_set_bij1a: fixes pi :: "'x prm" and x :: "'a" and X :: "'a set" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "(x\(pi\X)) = (((rev pi)\x)\X)" by (force simp add: perm_set_def pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at]) lemma pt_set_bij: fixes pi :: "'x prm" and x :: "'a" and X :: "'a set" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "((pi\x)\(pi\X)) = (x\X)" by (simp add: perm_set_def pt_bij[OF pt, OF at]) lemma pt_in_eqvt: fixes pi :: "'x prm" and x :: "'a" and X :: "'a set" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "pi\(x\X)=((pi\x)\(pi\X))" using assms by (auto simp add: pt_set_bij perm_bool) lemma pt_set_bij2: fixes pi :: "'x prm" and x :: "'a" and X :: "'a set" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and a: "x\X" shows "(pi\x)\(pi\X)" using a by (simp add: pt_set_bij[OF pt, OF at]) lemma pt_set_bij2a: fixes pi :: "'x prm" and x :: "'a" and X :: "'a set" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and a: "x\((rev pi)\X)" shows "(pi\x)\X" using a by (simp add: pt_set_bij1[OF pt, OF at]) lemma pt_subseteq_eqvt: fixes pi :: "'x prm" and Y :: "'a set" and X :: "'a set" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "(pi\(X\Y)) = ((pi\X)\(pi\Y))" by (auto simp add: perm_set_def perm_bool pt_bij[OF pt, OF at]) lemma pt_set_diff_eqvt: fixes X::"'a set" and Y::"'a set" and pi::"'x prm" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "pi\(X - Y) = (pi\X) - (pi\Y)" by (auto simp add: perm_set_def pt_bij[OF pt, OF at]) lemma pt_Collect_eqvt: fixes pi::"'x prm" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "pi\{x::'a. P x} = {x. P ((rev pi)\x)}" proof - have "\y. x = pi \ y \ P y" if "P (rev pi \ x)" for x using that by (metis at pt pt_pi_rev) then show ?thesis by (auto simp add: perm_set_def pt_rev_pi [OF assms]) qed \ \some helper lemmas for the pt_perm_supp_ineq lemma\ lemma Collect_permI: fixes pi :: "'x prm" and x :: "'a" assumes a: "\x. (P1 x = P2 x)" shows "{pi\x| x. P1 x} = {pi\x| x. P2 x}" using a by force lemma Infinite_cong: assumes a: "X = Y" shows "infinite X = infinite Y" using a by (simp) lemma pt_set_eq_ineq: fixes pi :: "'y prm" assumes pt: "pt TYPE('x) TYPE('y)" and at: "at TYPE('y)" shows "{pi\x| x::'x. P x} = {x::'x. P ((rev pi)\x)}" by (force simp only: pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at]) lemma pt_inject_on_ineq: fixes X :: "'y set" and pi :: "'x prm" assumes pt: "pt TYPE('y) TYPE('x)" and at: "at TYPE('x)" shows "inj_on (perm pi) X" proof (unfold inj_on_def, intro strip) fix x::"'y" and y::"'y" assume "pi\x = pi\y" thus "x=y" by (simp add: pt_bij[OF pt, OF at]) qed lemma pt_set_finite_ineq: fixes X :: "'x set" and pi :: "'y prm" assumes pt: "pt TYPE('x) TYPE('y)" and at: "at TYPE('y)" shows "finite (pi\X) = finite X" proof - have image: "(pi\X) = (perm pi ` X)" by (force simp only: perm_set_def) show ?thesis proof (rule iffI) assume "finite (pi\X)" hence "finite (perm pi ` X)" using image by (simp) thus "finite X" using pt_inject_on_ineq[OF pt, OF at] by (rule finite_imageD) next assume "finite X" hence "finite (perm pi ` X)" by (rule finite_imageI) thus "finite (pi\X)" using image by (simp) qed qed lemma pt_set_infinite_ineq: fixes X :: "'x set" and pi :: "'y prm" assumes pt: "pt TYPE('x) TYPE('y)" and at: "at TYPE('y)" shows "infinite (pi\X) = infinite X" using pt at by (simp add: pt_set_finite_ineq) lemma pt_perm_supp_ineq: fixes pi :: "'x prm" and x :: "'a" assumes pta: "pt TYPE('a) TYPE('x)" and ptb: "pt TYPE('y) TYPE('x)" and at: "at TYPE('x)" and cp: "cp TYPE('a) TYPE('x) TYPE('y)" shows "(pi\((supp x)::'y set)) = supp (pi\x)" (is "?LHS = ?RHS") proof - have "?LHS = {pi\a | a. infinite {b. [(a,b)]\x \ x}}" by (simp add: supp_def perm_set_def) also have "\ = {pi\a | a. infinite {pi\b | b. [(a,b)]\x \ x}}" proof (rule Collect_permI, rule allI, rule iffI) fix a assume "infinite {b::'y. [(a,b)]\x \ x}" hence "infinite (pi\{b::'y. [(a,b)]\x \ x})" by (simp add: pt_set_infinite_ineq[OF ptb, OF at]) thus "infinite {pi\b |b::'y. [(a,b)]\x \ x}" by (simp add: perm_set_def) next fix a assume "infinite {pi\b |b::'y. [(a,b)]\x \ x}" hence "infinite (pi\{b::'y. [(a,b)]\x \ x})" by (simp add: perm_set_def) thus "infinite {b::'y. [(a,b)]\x \ x}" by (simp add: pt_set_infinite_ineq[OF ptb, OF at]) qed also have "\ = {a. infinite {b::'y. [((rev pi)\a,(rev pi)\b)]\x \ x}}" by (simp add: pt_set_eq_ineq[OF ptb, OF at]) also have "\ = {a. infinite {b. pi\([((rev pi)\a,(rev pi)\b)]\x) \ (pi\x)}}" by (simp add: pt_bij[OF pta, OF at]) also have "\ = {a. infinite {b. [(a,b)]\(pi\x) \ (pi\x)}}" proof (rule Collect_cong, rule Infinite_cong, rule Collect_cong) fix a::"'y" and b::"'y" have "pi\(([((rev pi)\a,(rev pi)\b)])\x) = [(a,b)]\(pi\x)" by (simp add: cp1[OF cp] pt_pi_rev[OF ptb, OF at]) thus "(pi\([((rev pi)\a,(rev pi)\b)]\x) \ pi\x) = ([(a,b)]\(pi\x) \ pi\x)" by simp qed finally show "?LHS = ?RHS" by (simp add: supp_def) qed lemma pt_perm_supp: fixes pi :: "'x prm" and x :: "'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "(pi\((supp x)::'x set)) = supp (pi\x)" by (rule pt_perm_supp_ineq) (auto simp: assms at_pt_inst cp_pt_inst) lemma pt_supp_finite_pi: fixes pi :: "'x prm" and x :: "'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and f: "finite ((supp x)::'x set)" shows "finite ((supp (pi\x))::'x set)" by (metis at at_pt_inst f pt pt_perm_supp pt_set_finite_ineq) lemma pt_fresh_left_ineq: fixes pi :: "'x prm" and x :: "'a" and a :: "'y" assumes pta: "pt TYPE('a) TYPE('x)" and ptb: "pt TYPE('y) TYPE('x)" and at: "at TYPE('x)" and cp: "cp TYPE('a) TYPE('x) TYPE('y)" shows "a\(pi\x) = ((rev pi)\a)\x" using pt_perm_supp_ineq[OF pta, OF ptb, OF at, OF cp] pt_set_bij1[OF ptb, OF at] by (simp add: fresh_def) lemma pt_fresh_right_ineq: fixes pi :: "'x prm" and x :: "'a" and a :: "'y" assumes pta: "pt TYPE('a) TYPE('x)" and ptb: "pt TYPE('y) TYPE('x)" and at: "at TYPE('x)" and cp: "cp TYPE('a) TYPE('x) TYPE('y)" shows "(pi\a)\x = a\((rev pi)\x)" by (simp add: assms pt_fresh_left_ineq) lemma pt_fresh_bij_ineq: fixes pi :: "'x prm" and x :: "'a" and a :: "'y" assumes pta: "pt TYPE('a) TYPE('x)" and ptb: "pt TYPE('y) TYPE('x)" and at: "at TYPE('x)" and cp: "cp TYPE('a) TYPE('x) TYPE('y)" shows "(pi\a)\(pi\x) = a\x" using assms pt_bij1 pt_fresh_right_ineq by fastforce lemma pt_fresh_left: fixes pi :: "'x prm" and x :: "'a" and a :: "'x" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "a\(pi\x) = ((rev pi)\a)\x" by (simp add: assms at_pt_inst cp_pt_inst pt_fresh_left_ineq) lemma pt_fresh_right: fixes pi :: "'x prm" and x :: "'a" and a :: "'x" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "(pi\a)\x = a\((rev pi)\x)" by (simp add: assms at_pt_inst cp_pt_inst pt_fresh_right_ineq) lemma pt_fresh_bij: fixes pi :: "'x prm" and x :: "'a" and a :: "'x" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "(pi\a)\(pi\x) = a\x" by (metis assms pt_bij1 pt_fresh_right) lemma pt_fresh_bij1: fixes pi :: "'x prm" and x :: "'a" and a :: "'x" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and a: "a\x" shows "(pi\a)\(pi\x)" using a by (simp add: pt_fresh_bij[OF pt, OF at]) lemma pt_fresh_bij2: fixes pi :: "'x prm" and x :: "'a" and a :: "'x" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and a: "(pi\a)\(pi\x)" shows "a\x" using a by (simp add: pt_fresh_bij[OF pt, OF at]) lemma pt_fresh_eqvt: fixes pi :: "'x prm" and x :: "'a" and a :: "'x" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "pi\(a\x) = (pi\a)\(pi\x)" by (simp add: perm_bool pt_fresh_bij[OF pt, OF at]) lemma pt_perm_fresh1: fixes a :: "'x" and b :: "'x" and x :: "'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE ('x)" and a1: "\(a\x)" and a2: "b\x" shows "[(a,b)]\x \ x" proof assume neg: "[(a,b)]\x = x" from a1 have a1':"a\(supp x)" by (simp add: fresh_def) from a2 have a2':"b\(supp x)" by (simp add: fresh_def) from a1' a2' have a3: "a\b" by force from a1' have "([(a,b)]\a)\([(a,b)]\(supp x))" by (simp only: pt_set_bij[OF at_pt_inst[OF at], OF at]) hence "b\([(a,b)]\(supp x))" by (simp add: at_calc[OF at]) hence "b\(supp ([(a,b)]\x))" by (simp add: pt_perm_supp[OF pt,OF at]) with a2' neg show False by simp qed (* the next two lemmas are needed in the proof *) (* of the structural induction principle *) lemma pt_fresh_aux: fixes a::"'x" and b::"'x" and c::"'x" and x::"'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE ('x)" assumes a1: "c\a" and a2: "a\x" and a3: "c\x" shows "c\([(a,b)]\x)" using a1 a2 a3 by (simp_all add: pt_fresh_left[OF pt, OF at] at_calc[OF at]) lemma pt_fresh_perm_app: fixes pi :: "'x prm" and a :: "'x" and x :: "'y" assumes pt: "pt TYPE('y) TYPE('x)" and at: "at TYPE('x)" and h1: "a\pi" and h2: "a\x" shows "a\(pi\x)" using assms proof - have "a\(rev pi)"using h1 by (simp add: fresh_list_rev) then have "(rev pi)\a = a" by (simp add: at_prm_fresh[OF at]) then have "((rev pi)\a)\x" using h2 by simp thus "a\(pi\x)" by (simp add: pt_fresh_right[OF pt, OF at]) qed lemma pt_fresh_perm_app_ineq: fixes pi::"'x prm" and c::"'y" and x::"'a" assumes pta: "pt TYPE('a) TYPE('x)" and ptb: "pt TYPE('y) TYPE('x)" and at: "at TYPE('x)" and cp: "cp TYPE('a) TYPE('x) TYPE('y)" and dj: "disjoint TYPE('y) TYPE('x)" assumes a: "c\x" shows "c\(pi\x)" using a by (simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj]) lemma pt_fresh_eqvt_ineq: fixes pi::"'x prm" and c::"'y" and x::"'a" assumes pta: "pt TYPE('a) TYPE('x)" and ptb: "pt TYPE('y) TYPE('x)" and at: "at TYPE('x)" and cp: "cp TYPE('a) TYPE('x) TYPE('y)" and dj: "disjoint TYPE('y) TYPE('x)" shows "pi\(c\x) = (pi\c)\(pi\x)" by (simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj] perm_bool) \ \the co-set of a finite set is infinte\ lemma finite_infinite: assumes a: "finite {b::'x. P b}" and b: "infinite (UNIV::'x set)" shows "infinite {b. \P b}" proof - from a b have "infinite (UNIV - {b::'x. P b})" by (simp add: Diff_infinite_finite) moreover have "{b::'x. \P b} = UNIV - {b::'x. P b}" by auto ultimately show "infinite {b::'x. \P b}" by simp qed lemma pt_fresh_fresh: fixes x :: "'a" and a :: "'x" and b :: "'x" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE ('x)" and a1: "a\x" and a2: "b\x" shows "[(a,b)]\x=x" proof (cases "a=b") assume "a=b" hence "[(a,b)] \ []" by (simp add: at_ds1[OF at]) hence "[(a,b)]\x=([]::'x prm)\x" by (rule pt3[OF pt]) thus ?thesis by (simp only: pt1[OF pt]) next assume c2: "a\b" from a1 have f1: "finite {c. [(a,c)]\x \ x}" by (simp add: fresh_def supp_def) from a2 have f2: "finite {c. [(b,c)]\x \ x}" by (simp add: fresh_def supp_def) from f1 and f2 have f3: "finite {c. perm [(a,c)] x \ x \ perm [(b,c)] x \ x}" by (force simp only: Collect_disj_eq) have "infinite {c. [(a,c)]\x = x \ [(b,c)]\x = x}" by (simp add: finite_infinite[OF f3,OF at4[OF at], simplified]) hence "infinite ({c. [(a,c)]\x = x \ [(b,c)]\x = x}-{a,b})" by (force dest: Diff_infinite_finite) hence "({c. [(a,c)]\x = x \ [(b,c)]\x = x}-{a,b}) \ {}" by (metis finite_set set_empty2) hence "\c. c\({c. [(a,c)]\x = x \ [(b,c)]\x = x}-{a,b})" by (force) then obtain c where eq1: "[(a,c)]\x = x" and eq2: "[(b,c)]\x = x" and ineq: "a\c \ b\c" by (force) hence "[(a,c)]\([(b,c)]\([(a,c)]\x)) = x" by simp hence eq3: "[(a,c),(b,c),(a,c)]\x = x" by (simp add: pt2[OF pt,symmetric]) from c2 ineq have "[(a,c),(b,c),(a,c)] \ [(a,b)]" by (simp add: at_ds3[OF at]) hence "[(a,c),(b,c),(a,c)]\x = [(a,b)]\x" by (rule pt3[OF pt]) thus ?thesis using eq3 by simp qed lemma pt_pi_fresh_fresh: fixes x :: "'a" and pi :: "'x prm" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE ('x)" and a: "\(a,b)\set pi. a\x \ b\x" shows "pi\x=x" using a proof (induct pi) case Nil show "([]::'x prm)\x = x" by (rule pt1[OF pt]) next case (Cons ab pi) have a: "\(a,b)\set (ab#pi). a\x \ b\x" by fact have ih: "(\(a,b)\set pi. a\x \ b\x) \ pi\x=x" by fact obtain a b where e: "ab=(a,b)" by (cases ab) (auto) from a have a': "a\x" "b\x" using e by auto have "(ab#pi)\x = ([(a,b)]@pi)\x" using e by simp also have "\ = [(a,b)]\(pi\x)" by (simp only: pt2[OF pt]) also have "\ = [(a,b)]\x" using ih a by simp also have "\ = x" using a' by (simp add: pt_fresh_fresh[OF pt, OF at]) finally show "(ab#pi)\x = x" by simp qed lemma pt_perm_compose: fixes pi1 :: "'x prm" and pi2 :: "'x prm" and x :: "'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "pi2\(pi1\x) = (pi2\pi1)\(pi2\x)" proof - have "(pi2@pi1) \ ((pi2\pi1)@pi2)" by (rule at_ds8 [OF at]) hence "(pi2@pi1)\x = ((pi2\pi1)@pi2)\x" by (rule pt3[OF pt]) thus ?thesis by (simp add: pt2[OF pt]) qed lemma pt_perm_compose': fixes pi1 :: "'x prm" and pi2 :: "'x prm" and x :: "'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "(pi2\pi1)\x = pi2\(pi1\((rev pi2)\x))" proof - have "pi2\(pi1\((rev pi2)\x)) = (pi2\pi1)\(pi2\((rev pi2)\x))" by (rule pt_perm_compose[OF pt, OF at]) also have "\ = (pi2\pi1)\x" by (simp add: pt_pi_rev[OF pt, OF at]) finally have "pi2\(pi1\((rev pi2)\x)) = (pi2\pi1)\x" by simp thus ?thesis by simp qed lemma pt_perm_compose_rev: fixes pi1 :: "'x prm" and pi2 :: "'x prm" and x :: "'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "(rev pi2)\((rev pi1)\x) = (rev pi1)\(rev (pi1\pi2)\x)" proof - have "((rev pi2)@(rev pi1)) \ ((rev pi1)@(rev (pi1\pi2)))" by (rule at_ds9[OF at]) hence "((rev pi2)@(rev pi1))\x = ((rev pi1)@(rev (pi1\pi2)))\x" by (rule pt3[OF pt]) thus ?thesis by (simp add: pt2[OF pt]) qed section \equivariance for some connectives\ lemma pt_all_eqvt: fixes pi :: "'x prm" and x :: "'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "pi\(\(x::'a). P x) = (\(x::'a). pi\(P ((rev pi)\x)))" by (smt (verit, ccfv_threshold) assms pt_bij1 true_eqvt) lemma pt_ex_eqvt: fixes pi :: "'x prm" and x :: "'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "pi\(\(x::'a). P x) = (\(x::'a). pi\(P ((rev pi)\x)))" proof - have "\x. P x \ P (rev pi \ pi \ x)" by (simp add: assms(1) at pt_rev_pi) then show ?thesis by(auto simp add: perm_bool perm_fun_def) qed lemma pt_ex1_eqvt: fixes pi :: "'x prm" and x :: "'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "(pi\(\!x. P (x::'a))) = (\!x. pi\(P (rev pi\x)))" unfolding Ex1_def by (simp add: pt_ex_eqvt[OF pt at] conj_eqvt pt_all_eqvt[OF pt at] imp_eqvt pt_eq_eqvt[OF pt at] pt_pi_rev[OF pt at]) lemma pt_the_eqvt: fixes pi :: "'x prm" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and unique: "\!x. P x" shows "pi\(THE(x::'a). P x) = (THE(x::'a). pi\(P ((rev pi)\x)))" by (smt (verit, best) assms perm_bool_def pt_rev_pi theI_unique unique) section \facts about supports\ (*==============================*) lemma supports_subset: fixes x :: "'a" and S1 :: "'x set" and S2 :: "'x set" assumes a: "S1 supports x" and b: "S1 \ S2" shows "S2 supports x" using a b by (force simp add: supports_def) lemma supp_is_subset: fixes S :: "'x set" and x :: "'a" assumes a1: "S supports x" and a2: "finite S" shows "(supp x)\S" proof (rule ccontr) assume "\(supp x \ S)" hence "\a. a\(supp x) \ a\S" by force then obtain a where b1: "a\supp x" and b2: "a\S" by force from a1 b2 have "\b. (b\S \ ([(a,b)]\x = x))" by (unfold supports_def, force) hence "{b. [(a,b)]\x \ x}\S" by force with a2 have "finite {b. [(a,b)]\x \ x}" by (simp add: finite_subset) hence "a\(supp x)" by (unfold supp_def, auto) with b1 show False by simp qed lemma supp_supports: fixes x :: "'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE ('x)" shows "((supp x)::'x set) supports x" proof (unfold supports_def, intro strip) fix a b assume "(a::'x)\(supp x) \ (b::'x)\(supp x)" hence "a\x" and "b\x" by (auto simp add: fresh_def) thus "[(a,b)]\x = x" by (rule pt_fresh_fresh[OF pt, OF at]) qed lemma supports_finite: fixes S :: "'x set" and x :: "'a" assumes a1: "S supports x" and a2: "finite S" shows "finite ((supp x)::'x set)" proof - have "(supp x)\S" using a1 a2 by (rule supp_is_subset) thus ?thesis using a2 by (simp add: finite_subset) qed lemma supp_is_inter: fixes x :: "'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE ('x)" and fs: "fs TYPE('a) TYPE('x)" shows "((supp x)::'x set) = (\{S. finite S \ S supports x})" proof (rule equalityI) show "((supp x)::'x set) \ (\{S. finite S \ S supports x})" proof (clarify) fix S c assume b: "c\((supp x)::'x set)" and "finite (S::'x set)" and "S supports x" hence "((supp x)::'x set)\S" by (simp add: supp_is_subset) with b show "c\S" by force qed next show "(\{S. finite S \ S supports x}) \ ((supp x)::'x set)" proof (clarify, simp) fix c assume d: "\(S::'x set). finite S \ S supports x \ c\S" have "((supp x)::'x set) supports x" by (rule supp_supports[OF pt, OF at]) with d fs1[OF fs] show "c\supp x" by force qed qed lemma supp_is_least_supports: fixes S :: "'x set" and x :: "'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE ('x)" and a1: "S supports x" and a2: "finite S" and a3: "\S'. (S' supports x) \ S\S'" shows "S = (supp x)" proof (rule equalityI) show "((supp x)::'x set)\S" using a1 a2 by (rule supp_is_subset) next have "((supp x)::'x set) supports x" by (rule supp_supports[OF pt, OF at]) with a3 show "S\supp x" by force qed lemma supports_set: fixes S :: "'x set" and X :: "'a set" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE ('x)" and a: "\x\X. (\(a::'x) (b::'x). a\S\b\S \ ([(a,b)]\x)\X)" shows "S supports X" proof - have "x \ X" if "a \ S" "b \ S" and "x \ [(a, b)] \ X" for a b x using that by (metis a assms(1) at pt_pi_rev pt_set_bij1a) moreover have "x \ [(a, b)] \ X" if "a \ S" "b \ S" and "x \ X" for a b x using that by (simp add: a assms(1) at pt_set_bij1a) ultimately show ?thesis by (meson subsetI subset_antisym supports_def) qed lemma supports_fresh: fixes S :: "'x set" and a :: "'x" and x :: "'a" assumes a1: "S supports x" and a2: "finite S" and a3: "a\S" shows "a\x" by (meson assms fresh_def in_mono supp_is_subset) lemma at_fin_set_supports: fixes X::"'x set" assumes at: "at TYPE('x)" shows "X supports X" proof - have "\a b. a\X \ b\X \ [(a,b)]\X = X" by (auto simp add: perm_set_def at_calc[OF at]) then show ?thesis by (simp add: supports_def) qed lemma infinite_Collection: assumes a1:"infinite X" and a2:"\b\X. P(b)" shows "infinite {b\X. P(b)}" using assms rev_finite_subset by fastforce lemma at_fin_set_supp: fixes X::"'x set" assumes at: "at TYPE('x)" and fs: "finite X" shows "(supp X) = X" proof (rule subset_antisym) show "(supp X) \ X" using at_fin_set_supports[OF at] using fs by (simp add: supp_is_subset) next have inf: "infinite (UNIV-X)" using at4[OF at] fs by (auto simp add: Diff_infinite_finite) { fix a::"'x" assume asm: "a\X" hence "\b\(UNIV-X). [(a,b)]\X\X" by (auto simp add: perm_set_def at_calc[OF at]) with inf have "infinite {b\(UNIV-X). [(a,b)]\X\X}" by (rule infinite_Collection) hence "infinite {b. [(a,b)]\X\X}" by (rule_tac infinite_super, auto) hence "a\(supp X)" by (simp add: supp_def) } then show "X\(supp X)" by blast qed lemma at_fin_set_fresh: fixes X::"'x set" assumes at: "at TYPE('x)" and fs: "finite X" shows "(x \ X) = (x \ X)" by (simp add: at_fin_set_supp fresh_def at fs) section \Permutations acting on Functions\ (*==========================================*) lemma pt_fun_app_eq: fixes f :: "'a\'b" and x :: "'a" and pi :: "'x prm" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "pi\(f x) = (pi\f)(pi\x)" by (simp add: perm_fun_def pt_rev_pi[OF pt, OF at]) \ \sometimes pt_fun_app_eq does too much; this lemma 'corrects it'\ lemma pt_perm: fixes x :: "'a" and pi1 :: "'x prm" and pi2 :: "'x prm" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE ('x)" shows "(pi1\perm pi2)(pi1\x) = pi1\(pi2\x)" by (simp add: pt_fun_app_eq[OF pt, OF at]) lemma pt_fun_eq: fixes f :: "'a\'b" and pi :: "'x prm" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "(pi\f = f) = (\ x. pi\(f x) = f (pi\x))" (is "?LHS = ?RHS") proof assume a: "?LHS" show "?RHS" proof fix x have "pi\(f x) = (pi\f)(pi\x)" by (simp add: pt_fun_app_eq[OF pt, OF at]) also have "\ = f (pi\x)" using a by simp finally show "pi\(f x) = f (pi\x)" by simp qed next assume b: "?RHS" show "?LHS" proof (rule ccontr) assume "(pi\f) \ f" hence "\x. (pi\f) x \ f x" by (simp add: fun_eq_iff) then obtain x where b1: "(pi\f) x \ f x" by force from b have "pi\(f ((rev pi)\x)) = f (pi\((rev pi)\x))" by force hence "(pi\f)(pi\((rev pi)\x)) = f (pi\((rev pi)\x))" by (simp add: pt_fun_app_eq[OF pt, OF at]) hence "(pi\f) x = f x" by (simp add: pt_pi_rev[OF pt, OF at]) with b1 show "False" by simp qed qed \ \two helper lemmas for the equivariance of functions\ lemma pt_swap_eq_aux: fixes y :: "'a" and pi :: "'x prm" assumes pt: "pt TYPE('a) TYPE('x)" and a: "\(a::'x) (b::'x). [(a,b)]\y = y" shows "pi\y = y" proof(induct pi) case Nil show ?case by (simp add: pt1[OF pt]) next case (Cons x xs) have ih: "xs\y = y" by fact obtain a b where p: "x=(a,b)" by force have "((a,b)#xs)\y = ([(a,b)]@xs)\y" by simp also have "\ = [(a,b)]\(xs\y)" by (simp only: pt2[OF pt]) finally show ?case using a ih p by simp qed lemma pt_swap_eq: fixes y :: "'a" assumes pt: "pt TYPE('a) TYPE('x)" shows "(\(a::'x) (b::'x). [(a,b)]\y = y) = (\pi::'x prm. pi\y = y)" by (force intro: pt_swap_eq_aux[OF pt]) lemma pt_eqvt_fun1a: fixes f :: "'a\'b" assumes pta: "pt TYPE('a) TYPE('x)" and ptb: "pt TYPE('b) TYPE('x)" and at: "at TYPE('x)" and a: "((supp f)::'x set)={}" shows "\(pi::'x prm). pi\f = f" proof (intro strip) fix pi have "\a b. a\((supp f)::'x set) \ b\((supp f)::'x set) \ (([(a,b)]\f) = f)" by (intro strip, fold fresh_def, simp add: pt_fresh_fresh[OF pt_fun_inst[OF pta, OF ptb, OF at],OF at]) with a have "\(a::'x) (b::'x). ([(a,b)]\f) = f" by force hence "\(pi::'x prm). pi\f = f" by (simp add: pt_swap_eq[OF pt_fun_inst[OF pta, OF ptb, OF at]]) thus "(pi::'x prm)\f = f" by simp qed lemma pt_eqvt_fun1b: fixes f :: "'a\'b" assumes a: "\(pi::'x prm). pi\f = f" shows "((supp f)::'x set)={}" using a by (simp add: supp_def) lemma pt_eqvt_fun1: fixes f :: "'a\'b" assumes pta: "pt TYPE('a) TYPE('x)" and ptb: "pt TYPE('b) TYPE('x)" and at: "at TYPE('x)" shows "(((supp f)::'x set)={}) = (\(pi::'x prm). pi\f = f)" (is "?LHS = ?RHS") by (rule iffI, simp add: pt_eqvt_fun1a[OF pta, OF ptb, OF at], simp add: pt_eqvt_fun1b) lemma pt_eqvt_fun2a: fixes f :: "'a\'b" assumes pta: "pt TYPE('a) TYPE('x)" and ptb: "pt TYPE('b) TYPE('x)" and at: "at TYPE('x)" assumes a: "((supp f)::'x set)={}" shows "\(pi::'x prm) (x::'a). pi\(f x) = f(pi\x)" proof (intro strip) fix pi x from a have b: "\(pi::'x prm). pi\f = f" by (simp add: pt_eqvt_fun1[OF pta, OF ptb, OF at]) have "(pi::'x prm)\(f x) = (pi\f)(pi\x)" by (simp add: pt_fun_app_eq[OF pta, OF at]) with b show "(pi::'x prm)\(f x) = f (pi\x)" by force qed lemma pt_eqvt_fun2b: fixes f :: "'a\'b" assumes pt1: "pt TYPE('a) TYPE('x)" and pt2: "pt TYPE('b) TYPE('x)" and at: "at TYPE('x)" assumes a: "\(pi::'x prm) (x::'a). pi\(f x) = f(pi\x)" shows "((supp f)::'x set)={}" proof - from a have "\(pi::'x prm). pi\f = f" by (simp add: pt_fun_eq[OF pt1, OF at, symmetric]) thus ?thesis by (simp add: supp_def) qed lemma pt_eqvt_fun2: fixes f :: "'a\'b" assumes pta: "pt TYPE('a) TYPE('x)" and ptb: "pt TYPE('b) TYPE('x)" and at: "at TYPE('x)" shows "(((supp f)::'x set)={}) = (\(pi::'x prm) (x::'a). pi\(f x) = f(pi\x))" by (rule iffI, simp add: pt_eqvt_fun2a[OF pta, OF ptb, OF at], simp add: pt_eqvt_fun2b[OF pta, OF ptb, OF at]) lemma pt_supp_fun_subset: fixes f :: "'a\'b" assumes pta: "pt TYPE('a) TYPE('x)" and ptb: "pt TYPE('b) TYPE('x)" and at: "at TYPE('x)" and f1: "finite ((supp f)::'x set)" and f2: "finite ((supp x)::'x set)" shows "supp (f x) \ (((supp f)\(supp x))::'x set)" proof - have s1: "((supp f)\((supp x)::'x set)) supports (f x)" proof (simp add: supports_def, fold fresh_def, auto) fix a::"'x" and b::"'x" assume "a\f" and "b\f" hence a1: "[(a,b)]\f = f" by (rule pt_fresh_fresh[OF pt_fun_inst[OF pta, OF ptb, OF at], OF at]) assume "a\x" and "b\x" hence a2: "[(a,b)]\x = x" by (rule pt_fresh_fresh[OF pta, OF at]) from a1 a2 show "[(a,b)]\(f x) = (f x)" by (simp add: pt_fun_app_eq[OF pta, OF at]) qed from f1 f2 have "finite ((supp f)\((supp x)::'x set))" by force with s1 show ?thesis by (rule supp_is_subset) qed lemma pt_empty_supp_fun_subset: fixes f :: "'a\'b" assumes pta: "pt TYPE('a) TYPE('x)" and ptb: "pt TYPE('b) TYPE('x)" and at: "at TYPE('x)" and e: "(supp f)=({}::'x set)" shows "supp (f x) \ ((supp x)::'x set)" proof (unfold supp_def, auto) fix a::"'x" assume a1: "finite {b. [(a, b)]\x \ x}" assume "infinite {b. [(a, b)]\(f x) \ f x}" hence a2: "infinite {b. f ([(a, b)]\x) \ f x}" using e by (simp add: pt_eqvt_fun2[OF pta, OF ptb, OF at]) have a3: "{b. f ([(a,b)]\x) \ f x}\{b. [(a,b)]\x \ x}" by force from a1 a2 a3 show False by (force dest: finite_subset) qed section \Facts about the support of finite sets of finitely supported things\ (*=============================================================================*) definition X_to_Un_supp :: "('a set) \ 'x set" where "X_to_Un_supp X \ \x\X. ((supp x)::'x set)" lemma UNION_f_eqvt: fixes X::"('a set)" and f::"'a \ 'x set" and pi::"'x prm" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "pi\(\x\X. f x) = (\x\(pi\X). (pi\f) x)" proof - have pt_x: "pt TYPE('x) TYPE('x)" by (force intro: at_pt_inst at) show ?thesis proof - have "\x. (\u. x = pi \ u \ u \ X) \ pi \ z \ (pi \ f) x" if "y \ X" and "z \ f y" for y z using that by (metis assms at_pt_inst pt_fun_app_eq pt_set_bij) moreover have "\u. x = pi \ u \ (\x\X. u \ f x)" if "x \ (pi \ f) (pi \ y)" and "y \ X" for x y using that by (metis at at_pi_rev pt pt_fun_app_eq pt_set_bij1a pt_x) ultimately show ?thesis by (auto simp: perm_set_def) qed qed lemma X_to_Un_supp_eqvt: fixes X::"('a set)" and pi::"'x prm" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "pi\(X_to_Un_supp X) = ((X_to_Un_supp (pi\X))::'x set)" by (metis UNION_f_eqvt X_to_Un_supp_def assms pt_fun_eq pt_perm_supp) lemma Union_supports_set: fixes X::"('a set)" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "(\x\X. ((supp x)::'x set)) supports X" by (simp add: assms fresh_def pt_fresh_fresh supports_set) lemma Union_of_fin_supp_sets: fixes X::"('a set)" assumes fs: "fs TYPE('a) TYPE('x)" and fi: "finite X" shows "finite (\x\X. ((supp x)::'x set))" using fi by (induct, auto simp add: fs1[OF fs]) lemma Union_included_in_supp: fixes X::"('a set)" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and fs: "fs TYPE('a) TYPE('x)" and fi: "finite X" shows "(\x\X. ((supp x)::'x set)) \ supp X" proof - have "supp ((X_to_Un_supp X)::'x set) \ ((supp X)::'x set)" proof (rule pt_empty_supp_fun_subset) show "supp (\a. X_to_Un_supp (a::'a set)::'x set) = ({}::'x set)" by (simp add: X_to_Un_supp_eqvt at at_pt_inst pt pt_eqvt_fun2b pt_set_inst) qed (use assms at_pt_inst pt_set_inst in auto) hence "supp (\x\X. ((supp x)::'x set)) \ ((supp X)::'x set)" by (simp add: X_to_Un_supp_def) moreover have "supp (\x\X. ((supp x)::'x set)) = (\x\X. ((supp x)::'x set))" using Union_of_fin_supp_sets at at_fin_set_supp fi fs by auto ultimately show ?thesis by force qed lemma supp_of_fin_sets: fixes X::"('a set)" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and fs: "fs TYPE('a) TYPE('x)" and fi: "finite X" shows "(supp X) = (\x\X. ((supp x)::'x set))" proof (rule equalityI) have "finite (\ (supp ` X)::'x set)" using Union_of_fin_supp_sets fi fs by blast then show "(supp X::'x set) \ \ (supp ` X)" by (metis Union_supports_set at pt supp_is_subset) next show "(\x\X. (supp x::'x set)) \ supp X" by (simp add: Union_included_in_supp at fi fs pt) qed lemma supp_fin_union: fixes X::"('a set)" and Y::"('a set)" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and fs: "fs TYPE('a) TYPE('x)" and f1: "finite X" and f2: "finite Y" shows "(supp (X\Y)) = (supp X)\((supp Y)::'x set)" using f1 f2 by (force simp add: supp_of_fin_sets[OF pt, OF at, OF fs]) lemma supp_fin_insert: fixes X::"('a set)" and x::"'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and fs: "fs TYPE('a) TYPE('x)" and f: "finite X" shows "(supp (insert x X)) = (supp x)\((supp X)::'x set)" proof - have "(supp (insert x X)) = ((supp ({x}\(X::'a set)))::'x set)" by simp also have "\ = (supp {x})\(supp X)" by (rule supp_fin_union[OF pt, OF at, OF fs], simp_all add: f) finally show "(supp (insert x X)) = (supp x)\((supp X)::'x set)" by (simp add: supp_singleton) qed lemma fresh_fin_union: fixes X::"('a set)" and Y::"('a set)" and a::"'x" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and fs: "fs TYPE('a) TYPE('x)" and f1: "finite X" and f2: "finite Y" shows "a\(X\Y) = (a\X \ a\Y)" by (simp add: assms fresh_def supp_fin_union) lemma fresh_fin_insert: fixes X::"('a set)" and x::"'a" and a::"'x" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and fs: "fs TYPE('a) TYPE('x)" and f: "finite X" shows "a\(insert x X) = (a\x \ a\X)" by (simp add: assms fresh_def supp_fin_insert) lemma fresh_fin_insert1: fixes X::"('a set)" and x::"'a" and a::"'x" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and fs: "fs TYPE('a) TYPE('x)" and f: "finite X" and a1: "a\x" and a2: "a\X" shows "a\(insert x X)" using a1 a2 by (simp add: fresh_fin_insert[OF pt, OF at, OF fs, OF f]) lemma pt_list_set_supp: fixes xs :: "'a list" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and fs: "fs TYPE('a) TYPE('x)" shows "supp (set xs) = ((supp xs)::'x set)" proof - have "supp (set xs) = (\x\(set xs). ((supp x)::'x set))" by (rule supp_of_fin_sets[OF pt, OF at, OF fs], rule finite_set) also have "(\x\(set xs). ((supp x)::'x set)) = (supp xs)" proof(induct xs) case Nil show ?case by (simp add: supp_list_nil) next case (Cons h t) thus ?case by (simp add: supp_list_cons) qed finally show ?thesis by simp qed lemma pt_list_set_fresh: fixes a :: "'x" and xs :: "'a list" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and fs: "fs TYPE('a) TYPE('x)" shows "a\(set xs) = a\xs" by (simp add: fresh_def pt_list_set_supp[OF pt, OF at, OF fs]) section \generalisation of freshness to lists and sets of atoms\ (*================================================================*) consts fresh_star :: "'b \ 'a \ bool" (\_ \* _\ [100,100] 100) overloading fresh_star_set \ "fresh_star :: 'b set \ 'a \ bool" begin definition fresh_star_set: "xs\*c \ \x::'b\xs. x\(c::'a)" end overloading frsh_star_list \ "fresh_star :: 'b list \ 'a \ bool" begin definition fresh_star_list: "xs\*c \ \x::'b\set xs. x\(c::'a)" end lemmas fresh_star_def = fresh_star_list fresh_star_set lemma fresh_star_prod_set: fixes xs::"'a set" shows "xs\*(a,b) = (xs\*a \ xs\*b)" by (auto simp add: fresh_star_def fresh_prod) lemma fresh_star_prod_list: fixes xs::"'a list" shows "xs\*(a,b) = (xs\*a \ xs\*b)" by (auto simp add: fresh_star_def fresh_prod) lemmas fresh_star_prod = fresh_star_prod_list fresh_star_prod_set lemma fresh_star_set_eq: "set xs \* c = xs \* c" by (simp add: fresh_star_def) lemma fresh_star_Un_elim: "((S \ T) \* c \ PROP C) \ (S \* c \ T \* c \ PROP C)" proof assume \
: "(S \ T) \* c \ PROP C" and c: "S \* c" "T \* c" show "PROP C" using c by (intro \
) (metis Un_iff fresh_star_set) qed (auto simp: fresh_star_def) lemma fresh_star_insert_elim: "(insert x S \* c \ PROP C) \ (x \ c \ S \* c \ PROP C)" by rule (simp_all add: fresh_star_def) lemma fresh_star_empty_elim: "({} \* c \ PROP C) \ PROP C" by (simp add: fresh_star_def) text \Normalization of freshness results; see \ \nominal_induct\\ lemma fresh_star_unit_elim: shows "((a::'a set)\*() \ PROP C) \ PROP C" and "((b::'a list)\*() \ PROP C) \ PROP C" by (simp_all add: fresh_star_def fresh_def supp_unit) lemma fresh_star_prod_elim: shows "((a::'a set)\*(x,y) \ PROP C) \ (a\*x \ a\*y \ PROP C)" and "((b::'a list)\*(x,y) \ PROP C) \ (b\*x \ b\*y \ PROP C)" by (rule, simp_all add: fresh_star_prod)+ lemma pt_fresh_star_bij_ineq: fixes pi :: "'x prm" and x :: "'a" and a :: "'y set" and b :: "'y list" assumes pta: "pt TYPE('a) TYPE('x)" and ptb: "pt TYPE('y) TYPE('x)" and at: "at TYPE('x)" and cp: "cp TYPE('a) TYPE('x) TYPE('y)" shows "(pi\a)\*(pi\x) = a\*x" and "(pi\b)\*(pi\x) = b\*x" unfolding fresh_star_def proof - have "y \ x" if "\z\pi \ a. z \ pi \ x" and "y \ a" for y using that by (meson assms at pt_fresh_bij_ineq pt_set_bij2) moreover have "y \ pi \ x" if "\z\a. z \ x" and "y \ pi \ a" for y using that by (simp add: assms pt_fresh_left_ineq pt_set_bij1a) moreover have "y \ x" if "\z\set (pi \ b). z \ pi \ x" and "y \ set b" for y using that by (metis at cp pt_fresh_bij_ineq pt_set_bij pta ptb set_eqvt) moreover have "y \ pi \ x" if "\z\set b. z \ x" and "y \ set (pi \ b)" for y using that by (metis at cp pt_fresh_left_ineq pt_set_bij1a pta ptb set_eqvt) ultimately show "(\xa\pi \ a. xa \ pi \ x) = (\xa\a. xa \ x)" "(\xa\set (pi \ b). xa \ pi \ x) = (\xa\set b. xa \ x)" by blast+ qed lemma pt_fresh_star_bij: fixes pi :: "'x prm" and x :: "'a" and a :: "'x set" and b :: "'x list" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "(pi\a)\*(pi\x) = a\*x" and "(pi\b)\*(pi\x) = b\*x" proof (rule pt_fresh_star_bij_ineq) show "(pi \ b) \* (pi \ x) = b \* x" by (simp add: at at_pt_inst cp_pt_inst pt pt_fresh_star_bij_ineq) qed (auto simp: at pt at_pt_inst cp_pt_inst) lemma pt_fresh_star_eqvt: fixes pi :: "'x prm" and x :: "'a" and a :: "'x set" and b :: "'x list" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "pi\(a\*x) = (pi\a)\*(pi\x)" and "pi\(b\*x) = (pi\b)\*(pi\x)" by (simp_all add: perm_bool pt_fresh_star_bij[OF pt, OF at]) lemma pt_fresh_star_eqvt_ineq: fixes pi::"'x prm" and a::"'y set" and b::"'y list" and x::"'a" assumes pta: "pt TYPE('a) TYPE('x)" and ptb: "pt TYPE('y) TYPE('x)" and at: "at TYPE('x)" and cp: "cp TYPE('a) TYPE('x) TYPE('y)" and dj: "disjoint TYPE('y) TYPE('x)" shows "pi\(a\*x) = (pi\a)\*(pi\x)" and "pi\(b\*x) = (pi\b)\*(pi\x)" by (simp_all add: pt_fresh_star_bij_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj] perm_bool) lemma pt_freshs_freshs: assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE ('x)" and pi: "set (pi::'x prm) \ Xs \ Ys" and Xs: "Xs \* (x::'a)" and Ys: "Ys \* x" shows "pi\x = x" using pi proof (induct pi) case Nil show ?case by (simp add: pt1 [OF pt]) next case (Cons p pi) obtain a b where p: "p = (a, b)" by (cases p) with Cons Xs Ys have "a \ x" "b \ x" by (simp_all add: fresh_star_def) with Cons p show ?case by (simp add: pt_fresh_fresh [OF pt at] pt2 [OF pt, of "[(a, b)]" pi, simplified]) qed lemma pt_fresh_star_pi: fixes x::"'a" and pi::"'x prm" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and a: "((supp x)::'x set)\* pi" shows "pi\x = x" using a apply(induct pi) apply (simp add: assms(1) pt1) apply(auto simp add: fresh_star_def fresh_list_cons fresh_prod pt1[OF pt]) by (metis Cons_eq_append_conv append_self_conv2 assms(1) at at_fresh fresh_def pt2 pt_fresh_fresh) section \Infrastructure lemmas for strong rule inductions\ (*==========================================================*) text \ For every set of atoms, there is another set of atoms avoiding a finitely supported c and there is a permutation which 'translates' between both sets. \ lemma at_set_avoiding_aux: fixes Xs::"'a set" and As::"'a set" assumes at: "at TYPE('a)" and b: "Xs \ As" and c: "finite As" and d: "finite ((supp c)::'a set)" shows "\(pi::'a prm). (pi\Xs)\*c \ (pi\Xs) \ As = {} \ set pi \ Xs \ (pi\Xs)" proof - from b c have "finite Xs" by (simp add: finite_subset) then show ?thesis using b proof (induct) case empty have "({}::'a set)\*c" by (simp add: fresh_star_def) moreover have "({}::'a set) \ As = {}" by simp moreover have "set ([]::'a prm) \ {} \ {}" by simp ultimately show ?case by (simp add: empty_eqvt) next case (insert x Xs) then have ih: "\pi. (pi\Xs)\*c \ (pi\Xs) \ As = {} \ set pi \ Xs \ (pi\Xs)" by simp then obtain pi where a1: "(pi\Xs)\*c" and a2: "(pi\Xs) \ As = {}" and a4: "set pi \ Xs \ (pi\Xs)" by blast have b: "x\Xs" by fact have d1: "finite As" by fact have d2: "finite Xs" by fact have d3: "({x} \ Xs) \ As" using insert(4) by simp from d d1 d2 obtain y::"'a" where fr: "y\(c,pi\Xs,As)" apply(rule_tac at_exists_fresh[OF at, where x="(c,pi\Xs,As)"]) apply(auto simp add: supp_prod at_supp[OF at] at_fin_set_supp[OF at] pt_supp_finite_pi[OF pt_set_inst[OF at_pt_inst[OF at]] at]) done have "({y}\(pi\Xs))\*c" using a1 fr by (simp add: fresh_star_def) moreover have "({y}\(pi\Xs))\As = {}" using a2 d1 fr by (simp add: fresh_prod at_fin_set_fresh[OF at]) moreover have "pi\x=x" using a4 b a2 d3 by (rule_tac at_prm_fresh2[OF at]) (auto) then have "set ((pi\x,y)#pi) \ ({x} \ Xs) \ ({y}\(pi\Xs))" using a4 by auto moreover have "(((pi\x,y)#pi)\({x} \ Xs)) = {y}\(pi\Xs)" proof - have eq: "[(pi\x,y)]\(pi\Xs) = (pi\Xs)" proof - have "(pi\x)\(pi\Xs)" using b d2 by (simp add: pt_fresh_bij [OF pt_set_inst [OF at_pt_inst [OF at]], OF at] at_fin_set_fresh [OF at]) moreover have "y\(pi\Xs)" using fr by simp ultimately show "[(pi\x,y)]\(pi\Xs) = (pi\Xs)" by (simp add: pt_fresh_fresh[OF pt_set_inst [OF at_pt_inst[OF at]], OF at]) qed have "(((pi\x,y)#pi)\({x}\Xs)) = ([(pi\x,y)]\(pi\({x}\Xs)))" by (simp add: pt2[symmetric, OF pt_set_inst [OF at_pt_inst[OF at]]]) also have "\ = {y}\([(pi\x,y)]\(pi\Xs))" by (simp only: union_eqvt perm_set_def at_calc[OF at])(auto) finally show "(((pi\x,y)#pi)\({x} \ Xs)) = {y}\(pi\Xs)" using eq by simp qed ultimately show ?case by (rule_tac x="(pi\x,y)#pi" in exI) (auto) qed qed lemma at_set_avoiding: fixes Xs::"'a set" assumes at: "at TYPE('a)" and a: "finite Xs" and b: "finite ((supp c)::'a set)" obtains pi::"'a prm" where "(pi\Xs)\*c" and "set pi \ Xs \ (pi\Xs)" using a b at_set_avoiding_aux[OF at, where Xs="Xs" and As="Xs" and c="c"] by (blast) section \composition instances\ (* ============================= *) lemma cp_list_inst: assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)" shows "cp TYPE ('a list) TYPE('x) TYPE('y)" using c1 apply(clarsimp simp add: cp_def) by (induct_tac x) auto lemma cp_set_inst: assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)" shows "cp TYPE ('a set) TYPE('x) TYPE('y)" using c1 unfolding cp_def perm_set_def by (smt (verit) Collect_cong mem_Collect_eq) lemma cp_option_inst: assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)" shows "cp TYPE ('a option) TYPE('x) TYPE('y)" using c1 unfolding cp_def by (metis none_eqvt not_None_eq some_eqvt) lemma cp_noption_inst: assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)" shows "cp TYPE ('a noption) TYPE('x) TYPE('y)" using c1 unfolding cp_def by (metis nnone_eqvt noption.exhaust nsome_eqvt) lemma cp_unit_inst: shows "cp TYPE (unit) TYPE('x) TYPE('y)" by (simp add: cp_def) lemma cp_bool_inst: shows "cp TYPE (bool) TYPE('x) TYPE('y)" apply(clarsimp simp add: cp_def) by (induct_tac x) auto lemma cp_prod_inst: assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)" and c2: "cp TYPE ('b) TYPE('x) TYPE('y)" shows "cp TYPE ('a\'b) TYPE('x) TYPE('y)" using c1 c2 by (simp add: cp_def) lemma cp_fun_inst: assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)" and c2: "cp TYPE ('b) TYPE('x) TYPE('y)" and pt: "pt TYPE ('y) TYPE('x)" and at: "at TYPE ('x)" shows "cp TYPE ('a\'b) TYPE('x) TYPE('y)" using c1 c2 by(auto simp add: cp_def perm_fun_def fun_eq_iff at pt pt_list_inst pt_prod_inst pt_rev_pi rev_eqvt) section \Andy's freshness lemma\ (*================================*) lemma freshness_lemma: fixes h :: "'x\'a" assumes pta: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and f1: "finite ((supp h)::'x set)" and a: "\a::'x. a\(h,h a)" shows "\fr::'a. \a::'x. a\h \ (h a) = fr" proof - have ptb: "pt TYPE('x) TYPE('x)" by (simp add: at_pt_inst[OF at]) have ptc: "pt TYPE('x\'a) TYPE('x)" by (simp add: pt_fun_inst[OF ptb, OF pta, OF at]) from a obtain a0 where a1: "a0\h" and a2: "a0\(h a0)" by (force simp add: fresh_prod) show ?thesis proof let ?fr = "h (a0::'x)" show "\(a::'x). (a\h \ ((h a) = ?fr))" proof (intro strip) fix a assume a3: "(a::'x)\h" show "h (a::'x) = h a0" proof (cases "a=a0") case True thus "h (a::'x) = h a0" by simp next case False assume "a\a0" hence c1: "a\((supp a0)::'x set)" by (simp add: fresh_def[symmetric] at_fresh[OF at]) have c2: "a\((supp h)::'x set)" using a3 by (simp add: fresh_def) from c1 c2 have c3: "a\((supp h)\((supp a0)::'x set))" by force have f2: "finite ((supp a0)::'x set)" by (simp add: at_supp[OF at]) from f1 f2 have "((supp (h a0))::'x set)\((supp h)\(supp a0))" by (simp add: pt_supp_fun_subset[OF ptb, OF pta, OF at]) hence "a\((supp (h a0))::'x set)" using c3 by force hence "a\(h a0)" by (simp add: fresh_def) with a2 have d1: "[(a0,a)]\(h a0) = (h a0)" by (rule pt_fresh_fresh[OF pta, OF at]) from a1 a3 have d2: "[(a0,a)]\h = h" by (rule pt_fresh_fresh[OF ptc, OF at]) from d1 have "h a0 = [(a0,a)]\(h a0)" by simp also have "\= ([(a0,a)]\h)([(a0,a)]\a0)" by (simp add: pt_fun_app_eq[OF ptb, OF at]) also have "\ = h ([(a0,a)]\a0)" using d2 by simp also have "\ = h a" by (simp add: at_calc[OF at]) finally show "h a = h a0" by simp qed qed qed qed lemma freshness_lemma_unique: fixes h :: "'x\'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and f1: "finite ((supp h)::'x set)" and a: "\(a::'x). a\(h,h a)" shows "\!(fr::'a). \(a::'x). a\h \ (h a) = fr" proof (rule ex_ex1I) from pt at f1 a show "\fr::'a. \a::'x. a\h \ h a = fr" by (simp add: freshness_lemma) next fix fr1 fr2 assume b1: "\a::'x. a\h \ h a = fr1" assume b2: "\a::'x. a\h \ h a = fr2" from a obtain a where "(a::'x)\h" by (force simp add: fresh_prod) with b1 b2 have "h a = fr1 \ h a = fr2" by force thus "fr1 = fr2" by force qed \ \packaging the freshness lemma into a function\ definition fresh_fun :: "('x\'a)\'a" where "fresh_fun (h) \ THE fr. (\(a::'x). a\h \ (h a) = fr)" lemma fresh_fun_app: fixes h :: "'x\'a" and a :: "'x" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and f1: "finite ((supp h)::'x set)" and a: "\(a::'x). a\(h,h a)" and b: "a\h" shows "(fresh_fun h) = (h a)" proof (unfold fresh_fun_def, rule the_equality) show "\(a'::'x). a'\h \ h a' = h a" proof (intro strip) fix a'::"'x" assume c: "a'\h" from pt at f1 a have "\(fr::'a). \(a::'x). a\h \ (h a) = fr" by (rule freshness_lemma) with b c show "h a' = h a" by force qed next fix fr::"'a" assume "\a. a\h \ h a = fr" with b show "fr = h a" by force qed lemma fresh_fun_app': fixes h :: "'x\'a" and a :: "'x" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and f1: "finite ((supp h)::'x set)" and a: "a\h" "a\h a" shows "(fresh_fun h) = (h a)" by (meson assms fresh_fun_app fresh_prod pt) lemma fresh_fun_equiv_ineq: fixes h :: "'y\'a" and pi:: "'x prm" assumes pta: "pt TYPE('a) TYPE('x)" and ptb: "pt TYPE('y) TYPE('x)" and ptb':"pt TYPE('a) TYPE('y)" and at: "at TYPE('x)" and at': "at TYPE('y)" and cpa: "cp TYPE('a) TYPE('x) TYPE('y)" and cpb: "cp TYPE('y) TYPE('x) TYPE('y)" and f1: "finite ((supp h)::'y set)" and a1: "\(a::'y). a\(h,h a)" shows "pi\(fresh_fun h) = fresh_fun(pi\h)" (is "?LHS = ?RHS") proof - have ptd: "pt TYPE('y) TYPE('y)" by (simp add: at_pt_inst[OF at']) have ptc: "pt TYPE('y\'a) TYPE('x)" by (simp add: pt_fun_inst[OF ptb, OF pta, OF at]) have cpc: "cp TYPE('y\'a) TYPE ('x) TYPE ('y)" by (rule cp_fun_inst[OF cpb cpa ptb at]) have f2: "finite ((supp (pi\h))::'y set)" proof - from f1 have "finite (pi\((supp h)::'y set))" by (simp add: pt_set_finite_ineq[OF ptb, OF at]) thus ?thesis by (simp add: pt_perm_supp_ineq[OF ptc, OF ptb, OF at, OF cpc]) qed from a1 obtain a' where c0: "a'\(h,h a')" by force hence c1: "a'\h" and c2: "a'\(h a')" by (simp_all add: fresh_prod) have c3: "(pi\a')\(pi\h)" using c1 by (simp add: pt_fresh_bij_ineq[OF ptc, OF ptb, OF at, OF cpc]) have c4: "(pi\a')\(pi\h) (pi\a')" proof - from c2 have "(pi\a')\(pi\(h a'))" by (simp add: pt_fresh_bij_ineq[OF pta, OF ptb, OF at,OF cpa]) thus ?thesis by (simp add: pt_fun_app_eq[OF ptb, OF at]) qed have a2: "\(a::'y). a\(pi\h,(pi\h) a)" using c3 c4 by (force simp add: fresh_prod) have d1: "?LHS = pi\(h a')" using c1 a1 by (simp add: fresh_fun_app[OF ptb', OF at', OF f1]) have d2: "?RHS = (pi\h) (pi\a')" using c3 a2 by (simp add: fresh_fun_app[OF ptb', OF at', OF f2]) show ?thesis using d1 d2 by (simp add: pt_fun_app_eq[OF ptb, OF at]) qed lemma fresh_fun_equiv: fixes h :: "'x\'a" and pi:: "'x prm" assumes pta: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and f1: "finite ((supp h)::'x set)" and a1: "\(a::'x). a\(h,h a)" shows "pi\(fresh_fun h) = fresh_fun(pi\h)" (is "?LHS = ?RHS") proof - have ptb: "pt TYPE('x) TYPE('x)" by (simp add: at_pt_inst[OF at]) have ptc: "pt TYPE('x\'a) TYPE('x)" by (simp add: pt_fun_inst[OF ptb, OF pta, OF at]) have f2: "finite ((supp (pi\h))::'x set)" proof - from f1 have "finite (pi\((supp h)::'x set))" by (simp add: pt_set_finite_ineq[OF ptb, OF at]) thus ?thesis by (simp add: pt_perm_supp[OF ptc, OF at]) qed from a1 obtain a' where c0: "a'\(h,h a')" by force hence c1: "a'\h" and c2: "a'\(h a')" by (simp_all add: fresh_prod) have c3: "(pi\a')\(pi\h)" using c1 by (simp add: pt_fresh_bij[OF ptc, OF at]) have c4: "(pi\a')\(pi\h) (pi\a')" proof - from c2 have "(pi\a')\(pi\(h a'))" by (simp add: pt_fresh_bij[OF pta, OF at]) thus ?thesis by (simp add: pt_fun_app_eq[OF ptb, OF at]) qed have a2: "\(a::'x). a\(pi\h,(pi\h) a)" using c3 c4 by (force simp add: fresh_prod) have d1: "?LHS = pi\(h a')" using c1 a1 by (simp add: fresh_fun_app[OF pta, OF at, OF f1]) have d2: "?RHS = (pi\h) (pi\a')" using c3 a2 by (simp add: fresh_fun_app[OF pta, OF at, OF f2]) show ?thesis using d1 d2 by (simp add: pt_fun_app_eq[OF ptb, OF at]) qed lemma fresh_fun_supports: fixes h :: "'x\'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and f1: "finite ((supp h)::'x set)" and a: "\(a::'x). a\(h,h a)" shows "((supp h)::'x set) supports (fresh_fun h)" by(simp flip: fresh_def add: supports_def assms at_pt_inst fresh_fun_equiv pt_fresh_fresh pt_fun_inst) section \Abstraction function\ (*==============================*) lemma pt_abs_fun_inst: assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "pt TYPE('x\('a noption)) TYPE('x)" by (simp add: at at_pt_inst pt pt_fun_inst pt_noption_inst) definition abs_fun :: "'x\'a\('x\('a noption))" (\[_]._\ [100,100] 100) where "[a].x \ (\b. (if b=a then nSome(x) else (if b\x then nSome([(a,b)]\x) else nNone)))" (* FIXME: should be called perm_if and placed close to the definition of permutations on bools *) lemma abs_fun_if: fixes pi :: "'x prm" and x :: "'a" and y :: "'a" and c :: "bool" shows "pi\(if c then x else y) = (if c then (pi\x) else (pi\y))" by force lemma abs_fun_pi_ineq: fixes a :: "'y" and x :: "'a" and pi :: "'x prm" assumes pta: "pt TYPE('a) TYPE('x)" and ptb: "pt TYPE('y) TYPE('x)" and at: "at TYPE('x)" and cp: "cp TYPE('a) TYPE('x) TYPE('y)" shows "pi\([a].x) = [(pi\a)].(pi\x)" unfolding fun_eq_iff proof fix y have "(((rev pi)\y) = a) = (y = pi\a)" by (metis at pt_rev_pi ptb) moreover have "(((rev pi)\y)\x) = (y\(pi\x))" by (simp add: assms pt_fresh_left_ineq) moreover have "pi\([(a,(rev pi)\y)]\x) = [(pi\a,y)]\(pi\x)" using assms cp1[OF cp] by (simp add: pt_pi_rev) ultimately show "(pi \ [a].x) y = ([(pi \ a)].(pi \ x)) y" by (simp add: abs_fun_def perm_fun_def) qed lemma abs_fun_pi: fixes a :: "'x" and x :: "'a" and pi :: "'x prm" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "pi\([a].x) = [(pi\a)].(pi\x)" by (simp add: abs_fun_pi_ineq at at_pt_inst cp_pt_inst pt) lemma abs_fun_eq1: fixes x :: "'a" and y :: "'a" and a :: "'x" shows "([a].x = [a].y) = (x = y)" by (metis abs_fun_def noption.inject) lemma abs_fun_eq2: fixes x :: "'a" and y :: "'a" and a :: "'x" and b :: "'x" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and a1: "a\b" and a2: "[a].x = [b].y" shows "x=[(a,b)]\y \ a\y" proof - from a2 have "\c::'x. ([a].x) c = ([b].y) c" by (force simp add: fun_eq_iff) hence "([a].x) a = ([b].y) a" by simp hence a3: "nSome(x) = ([b].y) a" by (simp add: abs_fun_def) show "x=[(a,b)]\y \ a\y" proof (cases "a\y") assume a4: "a\y" hence "x=[(b,a)]\y" using a3 a1 by (simp add: abs_fun_def) moreover have "[(a,b)]\y = [(b,a)]\y" by (rule pt3[OF pt], rule at_ds5[OF at]) ultimately show ?thesis using a4 by simp next assume "\a\y" hence "nSome(x) = nNone" using a1 a3 by (simp add: abs_fun_def) hence False by simp thus ?thesis by simp qed qed lemma abs_fun_eq3: fixes x :: "'a" and y :: "'a" and a :: "'x" and b :: "'x" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and a1: "a\b" and a2: "x=[(a,b)]\y" and a3: "a\y" shows "[a].x =[b].y" proof - show ?thesis proof (simp only: abs_fun_def fun_eq_iff, intro strip) fix c::"'x" let ?LHS = "if c=a then nSome(x) else if c\x then nSome([(a,c)]\x) else nNone" and ?RHS = "if c=b then nSome(y) else if c\y then nSome([(b,c)]\y) else nNone" show "?LHS=?RHS" proof - have "(c=a) \ (c=b) \ (c\a \ c\b)" by blast moreover \ \case c=a\ { have "nSome(x) = nSome([(a,b)]\y)" using a2 by simp also have "\ = nSome([(b,a)]\y)" by (simp, rule pt3[OF pt], rule at_ds5[OF at]) finally have "nSome(x) = nSome([(b,a)]\y)" by simp moreover assume "c=a" ultimately have "?LHS=?RHS" using a1 a3 by simp } moreover \ \case c=b\ { have a4: "y=[(a,b)]\x" using a2 by (simp only: pt_swap_bij[OF pt, OF at]) hence "a\([(a,b)]\x)" using a3 by simp hence "b\x" by (simp add: at_calc[OF at] pt_fresh_left[OF pt, OF at]) moreover assume "c=b" ultimately have "?LHS=?RHS" using a1 a4 by simp } moreover \ \case c\a \ c\b\ { assume a5: "c\a \ c\b" moreover have "c\x = c\y" using a2 a5 by (force simp add: at_calc[OF at] pt_fresh_left[OF pt, OF at]) moreover have "c\y \ [(a,c)]\x = [(b,c)]\y" proof (intro strip) assume a6: "c\y" have "[(a,c),(b,c),(a,c)] \ [(a,b)]" using a1 a5 by (force intro: at_ds3[OF at]) hence "[(a,c)]\([(b,c)]\([(a,c)]\y)) = [(a,b)]\y" by (simp add: pt2[OF pt, symmetric] pt3[OF pt]) hence "[(a,c)]\([(b,c)]\y) = [(a,b)]\y" using a3 a6 by (simp add: pt_fresh_fresh[OF pt, OF at]) hence "[(a,c)]\([(b,c)]\y) = x" using a2 by simp hence "[(b,c)]\y = [(a,c)]\x" by (drule_tac pt_bij1[OF pt, OF at], simp) thus "[(a,c)]\x = [(b,c)]\y" by simp qed ultimately have "?LHS=?RHS" by simp } ultimately show "?LHS = ?RHS" by blast qed qed qed (* alpha equivalence *) lemma abs_fun_eq: fixes x :: "'a" and y :: "'a" and a :: "'x" and b :: "'x" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "([a].x = [b].y) = ((a=b \ x=y)\(a\b \ x=[(a,b)]\y \ a\y))" proof (rule iffI) assume b: "[a].x = [b].y" show "(a=b \ x=y)\(a\b \ x=[(a,b)]\y \ a\y)" proof (cases "a=b") case True with b show ?thesis by (simp add: abs_fun_eq1) next case False with b show ?thesis by (simp add: abs_fun_eq2[OF pt, OF at]) qed next assume "(a=b \ x=y)\(a\b \ x=[(a,b)]\y \ a\y)" thus "[a].x = [b].y" proof assume "a=b \ x=y" thus ?thesis by simp next assume "a\b \ x=[(a,b)]\y \ a\y" thus ?thesis by (simp add: abs_fun_eq3[OF pt, OF at]) qed qed (* symmetric version of alpha-equivalence *) lemma abs_fun_eq': fixes x :: "'a" and y :: "'a" and a :: "'x" and b :: "'x" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "([a].x = [b].y) = ((a=b \ x=y)\(a\b \ [(b,a)]\x=y \ b\x))" by (auto simp add: abs_fun_eq[OF pt, OF at] pt_swap_bij'[OF pt, OF at] pt_fresh_left[OF pt, OF at] at_calc[OF at]) (* alpha_equivalence with a fresh name *) lemma abs_fun_fresh: fixes x :: "'a" and y :: "'a" and c :: "'x" and a :: "'x" and b :: "'x" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and fr: "c\a" "c\b" "c\x" "c\y" shows "([a].x = [b].y) = ([(a,c)]\x = [(b,c)]\y)" proof (rule iffI) assume eq0: "[a].x = [b].y" show "[(a,c)]\x = [(b,c)]\y" proof (cases "a=b") case True then show ?thesis using eq0 by (simp add: pt_bij[OF pt, OF at] abs_fun_eq[OF pt, OF at]) next case False have ineq: "a\b" by fact with eq0 have eq: "x=[(a,b)]\y" and fr': "a\y" by (simp_all add: abs_fun_eq[OF pt, OF at]) from eq have "[(a,c)]\x = [(a,c)]\[(a,b)]\y" by (simp add: pt_bij[OF pt, OF at]) also have "\ = ([(a,c)]\[(a,b)])\([(a,c)]\y)" by (rule pt_perm_compose[OF pt, OF at]) also have "\ = [(c,b)]\y" using ineq fr fr' by (simp add: pt_fresh_fresh[OF pt, OF at] at_calc[OF at]) also have "\ = [(b,c)]\y" by (rule pt3[OF pt], rule at_ds5[OF at]) finally show ?thesis by simp qed next assume eq: "[(a,c)]\x = [(b,c)]\y" thus "[a].x = [b].y" proof (cases "a=b") case True then show ?thesis using eq by (simp add: pt_bij[OF pt, OF at] abs_fun_eq[OF pt, OF at]) next case False have ineq: "a\b" by fact from fr have "([(a,c)]\c)\([(a,c)]\x)" by (simp add: pt_fresh_bij[OF pt, OF at]) hence "a\([(b,c)]\y)" using eq fr by (simp add: at_calc[OF at]) hence fr0: "a\y" using ineq fr by (simp add: pt_fresh_left[OF pt, OF at] at_calc[OF at]) from eq have "x = (rev [(a,c)])\([(b,c)]\y)" by (rule pt_bij1[OF pt, OF at]) also have "\ = [(a,c)]\([(b,c)]\y)" by simp also have "\ = ([(a,c)]\[(b,c)])\([(a,c)]\y)" by (rule pt_perm_compose[OF pt, OF at]) also have "\ = [(b,a)]\y" using ineq fr fr0 by (simp add: pt_fresh_fresh[OF pt, OF at] at_calc[OF at]) also have "\ = [(a,b)]\y" by (rule pt3[OF pt], rule at_ds5[OF at]) finally show ?thesis using ineq fr0 by (simp add: abs_fun_eq[OF pt, OF at]) qed qed lemma abs_fun_fresh': fixes x :: "'a" and y :: "'a" and c :: "'x" and a :: "'x" and b :: "'x" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and as: "[a].x = [b].y" and fr: "c\a" "c\b" "c\x" "c\y" shows "x = [(a,c)]\[(b,c)]\y" using assms by (metis abs_fun_fresh pt_swap_bij) lemma abs_fun_supp_approx: fixes x :: "'a" and a :: "'x" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "((supp ([a].x))::'x set) \ (supp (x,a))" proof fix c assume "c\((supp ([a].x))::'x set)" hence "infinite {b. [(c,b)]\([a].x) \ [a].x}" by (simp add: supp_def) hence "infinite {b. [([(c,b)]\a)].([(c,b)]\x) \ [a].x}" by (simp add: abs_fun_pi[OF pt, OF at]) moreover have "{b. [([(c,b)]\a)].([(c,b)]\x) \ [a].x} \ {b. ([(c,b)]\x,[(c,b)]\a) \ (x, a)}" by force ultimately have "infinite {b. ([(c,b)]\x,[(c,b)]\a) \ (x, a)}" by (simp add: infinite_super) thus "c\(supp (x,a))" by (simp add: supp_def) qed lemma abs_fun_finite_supp: fixes x :: "'a" and a :: "'x" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and f: "finite ((supp x)::'x set)" shows "finite ((supp ([a].x))::'x set)" proof - from f have "finite ((supp (x,a))::'x set)" by (simp add: supp_prod at_supp[OF at]) moreover have "((supp ([a].x))::'x set) \ (supp (x,a))" by (rule abs_fun_supp_approx[OF pt, OF at]) ultimately show ?thesis by (simp add: finite_subset) qed lemma fresh_abs_funI1: fixes x :: "'a" and a :: "'x" and b :: "'x" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and f: "finite ((supp x)::'x set)" and a1: "b\x" and a2: "a\b" shows "b\([a].x)" proof - have "\c::'x. c\(b,a,x,[a].x)" proof (rule at_exists_fresh'[OF at], auto simp add: supp_prod at_supp[OF at] f) show "finite ((supp ([a].x))::'x set)" using f by (simp add: abs_fun_finite_supp[OF pt, OF at]) qed then obtain c where fr1: "c\b" and fr2: "c\a" and fr3: "c\x" and fr4: "c\([a].x)" by (force simp add: fresh_prod at_fresh[OF at]) have e: "[(c,b)]\([a].x) = [a].([(c,b)]\x)" using a2 fr1 fr2 by (force simp add: abs_fun_pi[OF pt, OF at] at_calc[OF at]) from fr4 have "([(c,b)]\c)\ ([(c,b)]\([a].x))" by (simp add: pt_fresh_bij[OF pt_abs_fun_inst[OF pt, OF at], OF at]) hence "b\([a].([(c,b)]\x))" using fr1 fr2 e by (simp add: at_calc[OF at]) thus ?thesis using a1 fr3 by (simp add: pt_fresh_fresh[OF pt, OF at]) qed lemma fresh_abs_funE: fixes a :: "'x" and b :: "'x" and x :: "'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and f: "finite ((supp x)::'x set)" and a1: "b\([a].x)" and a2: "b\a" shows "b\x" proof - have "\c::'x. c\(b,a,x,[a].x)" proof (rule at_exists_fresh'[OF at], auto simp add: supp_prod at_supp[OF at] f) show "finite ((supp ([a].x))::'x set)" using f by (simp add: abs_fun_finite_supp[OF pt, OF at]) qed then obtain c where fr1: "b\c" and fr2: "c\a" and fr3: "c\x" and fr4: "c\([a].x)" by (force simp add: fresh_prod at_fresh[OF at]) have "[a].x = [(b,c)]\([a].x)" using a1 fr4 by (simp add: pt_fresh_fresh[OF pt_abs_fun_inst[OF pt, OF at], OF at]) hence "[a].x = [a].([(b,c)]\x)" using fr2 a2 by (force simp add: abs_fun_pi[OF pt, OF at] at_calc[OF at]) hence b: "([(b,c)]\x) = x" by (simp add: abs_fun_eq1) from fr3 have "([(b,c)]\c)\([(b,c)]\x)" by (simp add: pt_fresh_bij[OF pt, OF at]) thus ?thesis using b fr1 by (simp add: at_calc[OF at]) qed lemma fresh_abs_funI2: fixes a :: "'x" and x :: "'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and f: "finite ((supp x)::'x set)" shows "a\([a].x)" proof - have "\c::'x. c\(a,x)" by (rule at_exists_fresh'[OF at], auto simp add: supp_prod at_supp[OF at] f) then obtain c where fr1: "a\c" and fr1_sym: "c\a" and fr2: "c\x" by (force simp add: fresh_prod at_fresh[OF at]) have "c\([a].x)" using f fr1 fr2 by (simp add: fresh_abs_funI1[OF pt, OF at]) hence "([(c,a)]\c)\([(c,a)]\([a].x))" using fr1 by (simp only: pt_fresh_bij[OF pt_abs_fun_inst[OF pt, OF at], OF at]) hence a: "a\([c].([(c,a)]\x))" using fr1_sym by (simp add: abs_fun_pi[OF pt, OF at] at_calc[OF at]) have "[c].([(c,a)]\x) = ([a].x)" using fr1_sym fr2 by (simp add: abs_fun_eq[OF pt, OF at]) thus ?thesis using a by simp qed lemma fresh_abs_fun_iff: fixes a :: "'x" and b :: "'x" and x :: "'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and f: "finite ((supp x)::'x set)" shows "(b\([a].x)) = (b=a \ b\x)" by (auto dest: fresh_abs_funE[OF pt, OF at,OF f] intro: fresh_abs_funI1[OF pt, OF at,OF f] fresh_abs_funI2[OF pt, OF at,OF f]) lemma abs_fun_supp: fixes a :: "'x" and x :: "'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" and f: "finite ((supp x)::'x set)" shows "supp ([a].x) = (supp x)-{a}" by (force simp add: supp_fresh_iff fresh_abs_fun_iff[OF pt, OF at, OF f]) (* maybe needs to be better stated as supp intersection supp *) lemma abs_fun_supp_ineq: fixes a :: "'y" and x :: "'a" assumes pta: "pt TYPE('a) TYPE('x)" and ptb: "pt TYPE('y) TYPE('x)" and at: "at TYPE('x)" and cp: "cp TYPE('a) TYPE('x) TYPE('y)" and dj: "disjoint TYPE('y) TYPE('x)" shows "((supp ([a].x))::'x set) = (supp x)" unfolding supp_def using abs_fun_pi_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj] by (smt (verit, ccfv_threshold) Collect_cong abs_fun_eq1) lemma fresh_abs_fun_iff_ineq: fixes a :: "'y" and b :: "'x" and x :: "'a" assumes pta: "pt TYPE('a) TYPE('x)" and ptb: "pt TYPE('y) TYPE('x)" and at: "at TYPE('x)" and cp: "cp TYPE('a) TYPE('x) TYPE('y)" and dj: "disjoint TYPE('y) TYPE('x)" shows "b\([a].x) = b\x" by (simp add: fresh_def abs_fun_supp_ineq[OF pta, OF ptb, OF at, OF cp, OF dj]) section \abstraction type for the parsing in nominal datatype\ (*==============================================================*) inductive_set ABS_set :: "('x\('a noption)) set" where ABS_in: "(abs_fun a x)\ABS_set" definition "ABS = ABS_set" typedef ('x, 'a) ABS (\\_\_\ [1000,1000] 1000) = "ABS::('x\('a noption)) set" morphisms Rep_ABS Abs_ABS unfolding ABS_def proof fix x::"'a" and a::"'x" show "(abs_fun a x)\ ABS_set" by (rule ABS_in) qed section \lemmas for deciding permutation equations\ (*===================================================*) lemma perm_aux_fold: shows "perm_aux pi x = pi\x" by (simp only: perm_aux_def) lemma pt_perm_compose_aux: fixes pi1 :: "'x prm" and pi2 :: "'x prm" and x :: "'a" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "pi2\(pi1\x) = perm_aux (pi2\pi1) (pi2\x)" proof - have "(pi2@pi1) \ ((pi2\pi1)@pi2)" by (rule at_ds8[OF at]) hence "(pi2@pi1)\x = ((pi2\pi1)@pi2)\x" by (rule pt3[OF pt]) thus ?thesis by (simp add: pt2[OF pt] perm_aux_def) qed lemma cp1_aux: fixes pi1::"'x prm" and pi2::"'y prm" and x ::"'a" assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)" shows "pi1\(pi2\x) = perm_aux (pi1\pi2) (pi1\x)" using cp by (simp add: cp_def perm_aux_def) lemma perm_eq_app: fixes f :: "'a\'b" and x :: "'a" and pi :: "'x prm" assumes pt: "pt TYPE('a) TYPE('x)" and at: "at TYPE('x)" shows "(pi\(f x)=y) = ((pi\f)(pi\x)=y)" by (simp add: pt_fun_app_eq[OF pt, OF at]) lemma perm_eq_lam: fixes f :: "'a\'b" and x :: "'a" and pi :: "'x prm" shows "((pi\(\x. f x))=y) = ((\x. (pi\(f ((rev pi)\x))))=y)" by (simp add: perm_fun_def) section \test\ lemma at_prm_eq_compose: fixes pi1 :: "'x prm" and pi2 :: "'x prm" and pi3 :: "'x prm" assumes at: "at TYPE('x)" and a: "pi1 \ pi2" shows "(pi3\pi1) \ (pi3\pi2)" proof - have pt: "pt TYPE('x) TYPE('x)" by (rule at_pt_inst[OF at]) have pt_prm: "pt TYPE('x prm) TYPE('x)" by (rule pt_list_inst[OF pt_prod_inst[OF pt, OF pt]]) from a show ?thesis by (auto simp add: prm_eq_def at pt pt_perm_compose') qed (************************) (* Various eqvt-lemmas *) -lemma Zero_nat_eqvt: +lemma Zero_nat_eqvt[simp]: shows "pi\(0::nat) = 0" by (auto simp add: perm_nat_def) -lemma One_nat_eqvt: +lemma One_nat_eqvt[simp]: shows "pi\(1::nat) = 1" by (simp add: perm_nat_def) lemma Suc_eqvt: shows "pi\(Suc x) = Suc (pi\x)" by (auto simp add: perm_nat_def) lemma numeral_nat_eqvt: shows "pi\((numeral n)::nat) = numeral n" by (simp add: perm_nat_def perm_int_def) lemma max_nat_eqvt: fixes x::"nat" shows "pi\(max x y) = max (pi\x) (pi\y)" by (simp add:perm_nat_def) lemma min_nat_eqvt: fixes x::"nat" shows "pi\(min x y) = min (pi\x) (pi\y)" by (simp add:perm_nat_def) lemma plus_nat_eqvt: fixes x::"nat" shows "pi\(x + y) = (pi\x) + (pi\y)" by (simp add:perm_nat_def) lemma minus_nat_eqvt: fixes x::"nat" shows "pi\(x - y) = (pi\x) - (pi\y)" by (simp add:perm_nat_def) lemma mult_nat_eqvt: fixes x::"nat" shows "pi\(x * y) = (pi\x) * (pi\y)" by (simp add:perm_nat_def) lemma div_nat_eqvt: fixes x::"nat" shows "pi\(x div y) = (pi\x) div (pi\y)" by (simp add:perm_nat_def) -lemma Zero_int_eqvt: +lemma Zero_int_eqvt[simp]: shows "pi\(0::int) = 0" by (auto simp add: perm_int_def) -lemma One_int_eqvt: +lemma One_int_eqvt[simp]: shows "pi\(1::int) = 1" by (simp add: perm_int_def) -lemma numeral_int_eqvt: +lemma numeral_int_eqvt[simp]: shows "pi\((numeral n)::int) = numeral n" using perm_int_def by blast -lemma neg_numeral_int_eqvt: +lemma neg_numeral_int_eqvt[simp]: shows "pi\((- numeral n)::int) = - numeral n" by (simp add: perm_int_def) lemma max_int_eqvt: fixes x::"int" shows "pi\(max (x::int) y) = max (pi\x) (pi\y)" by (simp add:perm_int_def) lemma min_int_eqvt: fixes x::"int" shows "pi\(min x y) = min (pi\x) (pi\y)" by (simp add:perm_int_def) lemma plus_int_eqvt: fixes x::"int" shows "pi\(x + y) = (pi\x) + (pi\y)" by (simp add:perm_int_def) lemma minus_int_eqvt: fixes x::"int" shows "pi\(x - y) = (pi\x) - (pi\y)" by (simp add:perm_int_def) lemma mult_int_eqvt: fixes x::"int" shows "pi\(x * y) = (pi\x) * (pi\y)" by (simp add:perm_int_def) lemma div_int_eqvt: fixes x::"int" shows "pi\(x div y) = (pi\x) div (pi\y)" by (simp add:perm_int_def) (*******************************************************) (* Setup of the theorem attributes eqvt and eqvt_force *) ML_file \nominal_thmdecls.ML\ setup "NominalThmDecls.setup" lemmas [eqvt] = (* connectives *) if_eqvt imp_eqvt disj_eqvt conj_eqvt neg_eqvt true_eqvt false_eqvt imp_eqvt [folded HOL.induct_implies_def] (* datatypes *) perm_unit.simps perm_list.simps append_eqvt perm_prod.simps fst_eqvt snd_eqvt perm_option.simps (* nats *) Suc_eqvt Zero_nat_eqvt One_nat_eqvt min_nat_eqvt max_nat_eqvt plus_nat_eqvt minus_nat_eqvt mult_nat_eqvt div_nat_eqvt (* ints *) Zero_int_eqvt One_int_eqvt min_int_eqvt max_int_eqvt plus_int_eqvt minus_int_eqvt mult_int_eqvt div_int_eqvt (* sets *) union_eqvt empty_eqvt insert_eqvt set_eqvt (* the lemmas numeral_nat_eqvt numeral_int_eqvt do not conform with the *) (* usual form of an eqvt-lemma, but they are needed for analysing *) (* permutations on nats and ints *) lemmas [eqvt_force] = numeral_nat_eqvt numeral_int_eqvt neg_numeral_int_eqvt (***************************************) (* setup for the individial atom-kinds *) (* and nominal datatypes *) ML_file \nominal_atoms.ML\ (************************************************************) (* various tactics for analysing permutations, supports etc *) ML_file \nominal_permeq.ML\ method_setup perm_simp = \NominalPermeq.perm_simp_meth\ \simp rules and simprocs for analysing permutations\ method_setup perm_simp_debug = \NominalPermeq.perm_simp_meth_debug\ \simp rules and simprocs for analysing permutations including debugging facilities\ method_setup perm_extend_simp = \NominalPermeq.perm_extend_simp_meth\ \tactic for deciding equalities involving permutations\ method_setup perm_extend_simp_debug = \NominalPermeq.perm_extend_simp_meth_debug\ \tactic for deciding equalities involving permutations including debugging facilities\ method_setup supports_simp = \NominalPermeq.supports_meth\ \tactic for deciding whether something supports something else\ method_setup supports_simp_debug = \NominalPermeq.supports_meth_debug\ \tactic for deciding whether something supports something else including debugging facilities\ method_setup finite_guess = \NominalPermeq.finite_guess_meth\ \tactic for deciding whether something has finite support\ method_setup finite_guess_debug = \NominalPermeq.finite_guess_meth_debug\ \tactic for deciding whether something has finite support including debugging facilities\ method_setup fresh_guess = \NominalPermeq.fresh_guess_meth\ \tactic for deciding whether an atom is fresh for something\ method_setup fresh_guess_debug = \NominalPermeq.fresh_guess_meth_debug\ \tactic for deciding whether an atom is fresh for something including debugging facilities\ (*****************************************************************) (* tactics for generating fresh names and simplifying fresh_funs *) ML_file \nominal_fresh_fun.ML\ method_setup generate_fresh = \ Args.type_name {proper = true, strict = true} >> (fn s => fn ctxt => SIMPLE_METHOD (generate_fresh_tac ctxt s)) \ "generate a name fresh for all the variables in the goal" method_setup fresh_fun_simp = \ Scan.lift (Args.parens (Args.$$$ "no_asm") >> K true || Scan.succeed false) >> (fn b => fn ctxt => SIMPLE_METHOD' (fresh_fun_tac ctxt b)) \ "delete one inner occurrence of fresh_fun" (************************************************) (* main file for constructing nominal datatypes *) lemma allE_Nil: assumes "\x. P x" obtains "P []" using assms .. ML_file \nominal_datatype.ML\ (******************************************************) (* primitive recursive functions on nominal datatypes *) ML_file \nominal_primrec.ML\ (****************************************************) (* inductive definition involving nominal datatypes *) ML_file \nominal_inductive.ML\ ML_file \nominal_inductive2.ML\ (*****************************************) (* setup for induction principles method *) ML_file \nominal_induct.ML\ method_setup nominal_induct = \NominalInduct.nominal_induct_method\ \nominal induction\ end