# HG changeset patch # User Christian Urban <urbanc@in.tum.de> # Date 1272435740 -7200 # Node ID 8daf6ff5e11ab5abfa47194614fcb385bd56c717 # Parent 90758c187861c5ace002eb2986d0a010a357c383 simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base diff -r 90758c187861 -r 8daf6ff5e11a Nominal-General/Nominal2_Atoms.thy --- a/Nominal-General/Nominal2_Atoms.thy Wed Apr 28 07:27:28 2010 +0200 +++ b/Nominal-General/Nominal2_Atoms.thy Wed Apr 28 08:22:20 2010 +0200 @@ -17,7 +17,6 @@ *} lemma atom_image_cong: - fixes X Y::"('a::at_base) set" shows "(atom ` X = atom ` Y) = (X = Y)" apply(rule inj_image_eq_iff) apply(simp add: inj_on_def) @@ -33,91 +32,22 @@ done lemma supp_finite_at_set: - fixes S::"('a::at) set" - assumes a: "finite S" - shows "supp S = atom ` S" - apply(rule finite_supp_unique) - apply(simp add: supports_def) - apply(rule allI)+ - apply(rule impI) - apply(rule swap_fresh_fresh) - apply(simp add: fresh_def) - apply(simp add: atom_image_supp) - apply(subst supp_finite_atom_set) - apply(rule finite_imageI) - apply(simp add: a) - apply(simp) - apply(simp add: fresh_def) - apply(simp add: atom_image_supp) - apply(subst supp_finite_atom_set) - apply(rule finite_imageI) - apply(simp add: a) - apply(simp) - apply(rule finite_imageI) - apply(simp add: a) - apply(drule swap_set_in) - apply(assumption) - apply(simp) - apply(simp add: image_eqvt) - apply(simp add: permute_fun_def) - apply(simp add: atom_eqvt) - apply(simp add: atom_image_cong) - done - -lemma supp_finite_at_set_aux: - fixes S::"('a::at) set" assumes a: "finite S" shows "supp S = atom ` S" -proof - show "supp S \<subseteq> ((atom::'a::at \<Rightarrow> atom) ` S)" - apply(rule supp_is_subset) - apply(simp add: supports_def) - apply(rule allI)+ - apply(rule impI) - apply(rule swap_fresh_fresh) - apply(simp add: fresh_def) - apply(simp add: atom_image_supp) - apply(subst supp_finite_atom_set) - apply(rule finite_imageI) - apply(simp add: a) - apply(simp) - apply(simp add: fresh_def) - apply(simp add: atom_image_supp) - apply(subst supp_finite_atom_set) - apply(rule finite_imageI) - apply(simp add: a) - apply(simp) - apply(rule finite_imageI) - apply(simp add: a) - done -next - have "supp ((atom::'a::at \<Rightarrow> atom) ` S) \<subseteq> supp ((op `) (atom::'a::at \<Rightarrow> atom)) \<union> supp S" - by (simp add: supp_fun_app) - moreover - have "supp ((op `) (atom::'a::at \<Rightarrow> atom)) = {}" - apply(rule supp_fun_eqvt) - apply(perm_simp) - apply(simp) - done - moreover - have "supp ((atom::'a::at \<Rightarrow> atom) ` S) = ((atom::'a::at \<Rightarrow> atom) ` S)" - apply(subst supp_finite_atom_set) - apply(rule finite_imageI) - apply(simp add: a) - apply(simp) - done - ultimately - show "((atom::'a::at \<Rightarrow> atom) ` S) \<subseteq> supp S" by simp +proof - + have fin: "finite (atom ` S)" + using a by (simp add: finite_imageI) + have "supp S = supp (atom ` S)" by (rule atom_image_supp) + also have "\<dots> = atom ` S" using fin by (simp add: supp_finite_atom_set) + finally show "supp S = atom ` S" by simp qed - lemma supp_at_insert: - fixes S::"('a::at) set" + fixes a::"'a::at_base" assumes a: "finite S" shows "supp (insert a S) = supp a \<union> supp S" using a by (simp add: supp_finite_at_set supp_at_base) - section {* A swapping operation for concrete atoms *} definition diff -r 90758c187861 -r 8daf6ff5e11a Nominal-General/Nominal2_Base.thy --- a/Nominal-General/Nominal2_Base.thy Wed Apr 28 07:27:28 2010 +0200 +++ b/Nominal-General/Nominal2_Base.thy Wed Apr 28 08:22:20 2010 +0200 @@ -1162,6 +1162,44 @@ thus ?thesis .. qed +lemma image_eqvt: + shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)" + unfolding permute_set_eq_image + unfolding permute_fun_def [where f=f] + by (simp add: image_image) + +lemma atom_image_cong: + shows "(atom ` X = atom ` Y) = (X = Y)" + apply(rule inj_image_eq_iff) + apply(simp add: inj_on_def) + done + +lemma atom_image_supp: + shows "supp S = supp (atom ` S)" + apply(simp add: supp_def) + apply(simp add: image_eqvt) + apply(subst (2) permute_fun_def) + apply(simp add: atom_eqvt) + apply(simp add: atom_image_cong) + done + +lemma supp_finite_at_set: + assumes a: "finite S" + shows "supp S = atom ` S" +proof - + have fin: "finite (atom ` S)" + using a by (simp add: finite_imageI) + have "supp S = supp (atom ` S)" by (rule atom_image_supp) + also have "\<dots> = atom ` S" using fin by (simp add: supp_finite_atom_set) + finally show "supp S = atom ` S" by simp +qed + +lemma supp_at_insert: + fixes a::"'a::at_base" + assumes a: "finite S" + shows "supp (insert a S) = supp a \<union> supp S" + using a by (simp add: supp_finite_at_set supp_at_base) + section {* library functions for the nominal infrastructure *} use "nominal_library.ML" diff -r 90758c187861 -r 8daf6ff5e11a Nominal-General/Nominal2_Eqvt.thy --- a/Nominal-General/Nominal2_Eqvt.thy Wed Apr 28 07:27:28 2010 +0200 +++ b/Nominal-General/Nominal2_Eqvt.thy Wed Apr 28 08:22:20 2010 +0200 @@ -152,12 +152,6 @@ unfolding vimage_def permute_fun_def [where f=f] unfolding Collect_eqvt2 mem_eqvt .. -lemma image_eqvt: - shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)" - unfolding permute_set_eq_image - unfolding permute_fun_def [where f=f] - by (simp add: image_image) - lemma finite_permute_iff: shows "finite (p \<bullet> A) \<longleftrightarrow> finite A" unfolding permute_set_eq_vimage diff -r 90758c187861 -r 8daf6ff5e11a Nominal/NewFv.thy --- a/Nominal/NewFv.thy Wed Apr 28 07:27:28 2010 +0200 +++ b/Nominal/NewFv.thy Wed Apr 28 08:22:20 2010 +0200 @@ -233,12 +233,13 @@ val fv_nums = 0 upto (length fv_frees - 1) val fv_eqs = map2 (fv thy dt_descr sorts fv_frees bn_fvbn) bclauses (fv_frees ~~ fv_nums); - val fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) - val fv_eqs_binds = map (fn x => (Attrib.empty_binding, x)) (flat fv_eqs @ flat fv_bn_eqs) + + val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) + val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs) val lthy' = lthy - |> Function.add_function fv_names fv_eqs_binds Function_Common.default_config + |> Function.add_function all_fv_names all_fv_eqs Function_Common.default_config |> by_pat_completeness_auto |> Local_Theory.restore |> termination_by (Lexicographic_Order.lexicographic_order) diff -r 90758c187861 -r 8daf6ff5e11a Nominal/NewParser.thy --- a/Nominal/NewParser.thy Wed Apr 28 07:27:28 2010 +0200 +++ b/Nominal/NewParser.thy Wed Apr 28 08:22:20 2010 +0200 @@ -1,5 +1,5 @@ theory NewParser -imports "../Nominal-General/Nominal2_Atoms" +imports "../Nominal-General/Nominal2_Base" "../Nominal-General/Nominal2_Eqvt" "../Nominal-General/Nominal2_Supp" "Perm" "NewFv" @@ -449,9 +449,22 @@ (main_parser >> nominal_datatype2_cmd) *} - +atom_decl name -atom_decl name +nominal_datatype lam = + Var name +| App lam lam +| Lam x::name t::lam bind_set x in t +| Let p::pt t::lam bind_set "bn p" in t +and pt = + P1 name +| P2 pt pt +binder + bn::"pt \<Rightarrow> atom set" +where + "bn (P1 x) = {atom x}" +| "bn (P2 p1 p2) = bn p1 \<union> bn p2" + nominal_datatype exp = EVar name @@ -507,10 +520,10 @@ (* some further tests *) -nominal_datatype lam = - Var "name" -| App "lam" "lam list" -| Lam x::"name" t::"lam" bind x in t +nominal_datatype lam2 = + Var2 "name" +| App2 "lam2" "lam2 list" +| Lam2 x::"name" t::"lam2" bind x in t nominal_datatype ty = Var "name" diff -r 90758c187861 -r 8daf6ff5e11a Nominal/Perm.thy --- a/Nominal/Perm.thy Wed Apr 28 07:27:28 2010 +0200 +++ b/Nominal/Perm.thy Wed Apr 28 08:22:20 2010 +0200 @@ -12,7 +12,8 @@ *} ML {* -(* generates for every datatype a name str ^ dt_name *) +(* generates for every datatype a name str ^ dt_name + plus and index for multiple occurences of a string *) fun prefix_dt_names dt_descr sorts str = let fun get_nth_name (i, _) =