# HG changeset patch # User Christian Urban # Date 1283550183 -28800 # Node ID 47c840599a6b9267041e5b0416a2588f6994ba46 # Parent 07ffa4e416595582e208113b4b0dcc4db3aeddcd cleaned a bit various thy-files in Nominal-General diff -r 07ffa4e41659 -r 47c840599a6b Nominal-General/Nominal2_Base.thy --- a/Nominal-General/Nominal2_Base.thy Fri Sep 03 22:35:35 2010 +0800 +++ b/Nominal-General/Nominal2_Base.thy Sat Sep 04 05:43:03 2010 +0800 @@ -430,6 +430,19 @@ shows "p \ (\ A) = (\ (p \ A))" by (simp add: permute_bool_def) +lemma conj_eqvt: + shows "p \ (A \ B) = ((p \ A) \ (p \ B))" + by (simp add: permute_bool_def) + +lemma imp_eqvt: + shows "p \ (A \ B) = ((p \ A) \ (p \ B))" + by (simp add: permute_bool_def) + +lemma ex_eqvt: + shows "p \ (\x. P x) = (\x. (p \ P) x)" + unfolding permute_fun_def permute_bool_def + by (auto, rule_tac x="p \ x" in exI, simp) + lemma permute_boolE: fixes P::"bool" shows "p \ P \ P" @@ -851,6 +864,7 @@ section {* Support for finite sets of atoms *} + lemma supp_finite_atom_set: fixes S::"atom set" assumes "finite S" @@ -862,12 +876,6 @@ apply(simp add: swap_set_in) done -lemma supp_atom_insert: - fixes S::"atom set" - assumes a: "finite S" - shows "supp (insert a S) = supp a \ supp S" - using a by (simp add: supp_finite_atom_set supp_atom) - section {* Type @{typ perm} is finitely-supported. *} lemma perm_swap_eq: @@ -1065,6 +1073,7 @@ apply (simp_all add: supp_Nil supp_Cons finite_supp) done + section {* Support and freshness for applications *} lemma fresh_conv_MOST: @@ -1112,6 +1121,78 @@ qed +section {* Support of Finite Sets of Finitely Supported Elements *} + +lemma Union_fresh: + shows "a \ S \ a \ (\x \ S. supp x)" + unfolding Union_image_eq[symmetric] + apply(rule_tac f="\S. \ supp ` S" in fresh_fun_eqvt_app) + apply(simp add: permute_fun_def UNION_def Collect_def Bex_def ex_eqvt mem_def conj_eqvt) + apply(subst permute_fun_app_eq) + back + apply(simp add: supp_eqvt) + apply(assumption) + done + +lemma Union_supports_set: + shows "(\x \ S. supp x) supports S" +proof - + { fix a b + have "\x \ S. (a \ b) \ x = x \ (a \ b) \ S = S" + unfolding permute_set_eq by force + } + then show "(\x \ S. supp x) supports S" + unfolding supports_def + by (simp add: fresh_def[symmetric] swap_fresh_fresh) +qed + +lemma Union_of_fin_supp_sets: + fixes S::"('a::fs set)" + assumes fin: "finite S" + shows "finite (\x\S. supp x)" + using fin by (induct) (auto simp add: finite_supp) + +lemma Union_included_in_supp: + fixes S::"('a::fs set)" + assumes fin: "finite S" + shows "(\x\S. supp x) \ supp S" +proof - + have "(\x\S. supp x) = supp (\x\S. supp x)" + by (rule supp_finite_atom_set[symmetric]) + (rule Union_of_fin_supp_sets[OF fin]) + also have "\ \ supp S" + by (rule supp_subset_fresh) + (simp add: Union_fresh) + finally show "(\x\S. supp x) \ supp S" . +qed + +lemma supp_of_fin_sets: + fixes S::"('a::fs set)" + assumes fin: "finite S" + shows "(supp S) = (\x\S. supp x)" +apply(rule subset_antisym) +apply(rule supp_is_subset) +apply(rule Union_supports_set) +apply(rule Union_of_fin_supp_sets[OF fin]) +apply(rule Union_included_in_supp[OF fin]) +done + +lemma supp_of_fin_union: + fixes S T::"('a::fs) set" + assumes fin1: "finite S" + and fin2: "finite T" + shows "supp (S \ T) = supp S \ supp T" + using fin1 fin2 + by (simp add: supp_of_fin_sets) + +lemma supp_of_fin_insert: + fixes S::"('a::fs) set" + assumes fin: "finite S" + shows "supp (insert x S) = supp x \ supp S" + using fin + by (simp add: supp_of_fin_sets) + + section {* Concrete atoms types *} text {* @@ -1179,44 +1260,18 @@ thus ?thesis .. qed -lemma image_eqvt: - shows "p \ (f ` A) = (p \ f) ` (p \ 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_set_at_base: assumes a: "finite S" shows "supp S = atom ` S" -proof - - have fin: "finite (atom ` S)" using a by simp - have "supp S = supp (atom ` S)" by (rule atom_image_supp) - also have "\ = atom ` S" using fin by (simp add: supp_finite_atom_set) - finally show "supp S = atom ` S" by simp -qed +apply(simp add: supp_of_fin_sets[OF a]) +apply(simp add: supp_at_base) +apply(auto) +done -lemma supp_at_base_insert: - fixes a::"'a::at_base" - assumes a: "finite S" - shows "supp (insert a S) = supp a \ supp S" - using a by (simp add: supp_finite_set_at_base supp_at_base) section {* library functions for the nominal infrastructure *} use "nominal_library.ML" + + end diff -r 07ffa4e41659 -r 47c840599a6b Nominal-General/Nominal2_Eqvt.thy --- a/Nominal-General/Nominal2_Eqvt.thy Fri Sep 03 22:35:35 2010 +0800 +++ b/Nominal-General/Nominal2_Eqvt.thy Sat Sep 04 05:43:03 2010 +0800 @@ -20,6 +20,20 @@ use "nominal_thmdecls.ML" setup "Nominal_ThmDecls.setup" + +section {* eqvt lemmas *} + +lemmas [eqvt] = + conj_eqvt Not_eqvt ex_eqvt imp_eqvt + imp_eqvt[folded induct_implies_def] + + (* nominal *) + supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt swap_eqvt uminus_eqvt + + (* datatypes *) + Pair_eqvt permute_list.simps + + text {* helper lemmas for the perm_simp *} definition @@ -79,14 +93,6 @@ shows "p \ False = False" unfolding permute_bool_def .. -lemma imp_eqvt[eqvt]: - shows "p \ (A \ B) = ((p \ A) \ (p \ B))" - by (simp add: permute_bool_def) - -lemma conj_eqvt[eqvt]: - shows "p \ (A \ B) = ((p \ A) \ (p \ B))" - by (simp add: permute_bool_def) - lemma disj_eqvt[eqvt]: shows "p \ (A \ B) = ((p \ A) \ (p \ B))" by (simp add: permute_bool_def) @@ -104,11 +110,6 @@ shows "p \ (\x. P x) = (\x. p \ P (- p \ x))" by (perm_simp add: permute_minus_cancel) (rule refl) -lemma ex_eqvt[eqvt]: - shows "p \ (\x. P x) = (\x. (p \ P) x)" - unfolding permute_fun_def permute_bool_def - by (auto, rule_tac x="p \ x" in exI, simp) - lemma ex_eqvt2: shows "p \ (\x. P x) = (\x. p \ P (- p \ x))" by (perm_simp add: permute_minus_cancel) (rule refl) @@ -211,6 +212,12 @@ shows "p \ (insert x A) = insert (p \ x) (p \ A)" unfolding permute_set_eq_image image_insert .. +lemma image_eqvt: + shows "p \ (f ` A) = (p \ f) ` (p \ A)" + unfolding permute_set_eq_image + unfolding permute_fun_def [where f=f] + by (simp add: image_image) + lemma vimage_eqvt[eqvt]: shows "p \ (f -` A) = (p \ f) -` (p \ A)" unfolding vimage_def @@ -230,6 +237,15 @@ shows "p \ finite A = finite (p \ A)" unfolding finite_permute_iff permute_bool_def .. +lemma supp_set: + fixes xs :: "('a::fs) list" + shows "supp (set xs) = supp xs" +apply(induct xs) +apply(simp add: supp_set_empty supp_Nil) +apply(simp add: supp_Cons supp_of_fin_insert) +done + + section {* List Operations *} lemma append_eqvt[eqvt]: @@ -295,20 +311,6 @@ shows "a \ ()" by (simp add: fresh_def supp_unit) -section {* additional eqvt lemmas *} - -lemmas [eqvt] = - imp_eqvt [folded induct_implies_def] - - (* nominal *) - supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt swap_eqvt uminus_eqvt - - (* datatypes *) - Pair_eqvt permute_list.simps - - (* sets *) - image_eqvt - section {* Test cases *} diff -r 07ffa4e41659 -r 47c840599a6b Nominal-General/Nominal2_Supp.thy --- a/Nominal-General/Nominal2_Supp.thy Fri Sep 03 22:35:35 2010 +0800 +++ b/Nominal-General/Nominal2_Supp.thy Sat Sep 04 05:43:03 2010 +0800 @@ -474,81 +474,4 @@ qed -section {* Support of Finite Sets of Finitely Supported Elements *} - -lemma Union_fresh: - shows "a \ S \ a \ (\x \ S. supp x)" - unfolding Union_image_eq[symmetric] - apply(rule_tac f="\S. \ supp ` S" in fresh_fun_eqvt_app) - apply(perm_simp) - apply(rule refl) - apply(assumption) - done - -lemma Union_supports_set: - shows "(\x \ S. supp x) supports S" -proof - - { fix a b - have "\x \ S. (a \ b) \ x = x \ (a \ b) \ S = S" - unfolding permute_set_eq by force - } - then show "(\x \ S. supp x) supports S" - unfolding supports_def - by (simp add: fresh_def[symmetric] swap_fresh_fresh) -qed - -lemma Union_of_fin_supp_sets: - fixes S::"('a::fs set)" - assumes fin: "finite S" - shows "finite (\x\S. supp x)" - using fin by (induct) (auto simp add: finite_supp) - -lemma Union_included_in_supp: - fixes S::"('a::fs set)" - assumes fin: "finite S" - shows "(\x\S. supp x) \ supp S" -proof - - have "(\x\S. supp x) = supp (\x\S. supp x)" - by (rule supp_finite_atom_set[symmetric]) - (rule Union_of_fin_supp_sets[OF fin]) - also have "\ \ supp S" - by (rule supp_subset_fresh) - (simp add: Union_fresh) - finally show "(\x\S. supp x) \ supp S" . -qed - -lemma supp_of_fin_sets: - fixes S::"('a::fs set)" - assumes fin: "finite S" - shows "(supp S) = (\x\S. supp x)" -apply(rule subset_antisym) -apply(rule supp_is_subset) -apply(rule Union_supports_set) -apply(rule Union_of_fin_supp_sets[OF fin]) -apply(rule Union_included_in_supp[OF fin]) -done - -lemma supp_of_fin_union: - fixes S T::"('a::fs) set" - assumes fin1: "finite S" - and fin2: "finite T" - shows "supp (S \ T) = supp S \ supp T" - using fin1 fin2 - by (simp add: supp_of_fin_sets) - -lemma supp_of_fin_insert: - fixes S::"('a::fs) set" - assumes fin: "finite S" - shows "supp (insert x S) = supp x \ supp S" - using fin - by (simp add: supp_of_fin_sets) - -lemma supp_set: - fixes xs :: "('a::fs) list" - shows "supp (set xs) = supp xs" -apply(induct xs) -apply(simp add: supp_set_empty supp_Nil) -apply(simp add: supp_Cons supp_of_fin_insert) -done - end diff -r 07ffa4e41659 -r 47c840599a6b Nominal/Nominal2_FSet.thy --- a/Nominal/Nominal2_FSet.thy Fri Sep 03 22:35:35 2010 +0800 +++ b/Nominal/Nominal2_FSet.thy Sat Sep 04 05:43:03 2010 +0800 @@ -36,14 +36,12 @@ end -lemma permute_fset[simp]: +lemma permute_fset[simp, eqvt]: fixes S::"('a::pt) fset" shows "(p \ {||}) = ({||} ::('a::pt) fset)" and "p \ finsert x S = finsert (p \ x) (p \ S)" by (lifting permute_list.simps) -declare permute_fset[eqvt] - lemma fmap_eqvt[eqvt]: shows "p \ (fmap f S) = fmap (p \ f) (p \ S)" by (lifting map_eqvt) @@ -113,7 +111,7 @@ apply (simp add: fresh_set_empty) apply simp apply (unfold fresh_def) - apply (simp add: supp_atom_insert) + apply (simp add: supp_of_fin_insert) apply (rule conjI) apply (unfold fresh_star_def) apply simp diff -r 07ffa4e41659 -r 47c840599a6b Pearl-jv/Paper.thy --- a/Pearl-jv/Paper.thy Fri Sep 03 22:35:35 2010 +0800 +++ b/Pearl-jv/Paper.thy Sat Sep 04 05:43:03 2010 +0800 @@ -44,6 +44,8 @@ section {* Introduction *} text {* + TODO: write about supp of finite sets + Nominal Isabelle provides a proving infratructure for convenient reasoning about programming languages. At its core Nominal Isabelle is based on the nominal logic work by Pitts at al