# HG changeset patch # User Cezary Kaliszyk # Date 1299037741 -32400 # Node ID 7fd879774d9b29dfed7fa676182a9ae0b92f4a73 # Parent 61d30863e5d159c683fe75f03965ad427d7c3eac# Parent ff22039df778799555ab706616b9fbb36dfa00cf merge diff -r ff22039df778 -r 7fd879774d9b Nominal/Eqvt.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Eqvt.thy Wed Mar 02 12:49:01 2011 +0900 @@ -0,0 +1,105 @@ +(* Title: Nominal2_Eqvt + Author: Brian Huffman, + Author: Christian Urban + + Test cases for perm_simp +*) +theory Eqvt +imports Nominal2_Base +begin + + +declare [[trace_eqvt = false]] +(* declare [[trace_eqvt = true]] *) + +lemma + fixes B::"'a::pt" + shows "p \ (B = C)" +apply(perm_simp) +oops + +lemma + fixes B::"bool" + shows "p \ (B = C)" +apply(perm_simp) +oops + +lemma + fixes B::"bool" + shows "p \ (A \ B = C)" +apply (perm_simp) +oops + +lemma + shows "p \ (\(x::'a::pt). A \ (B::'a \ bool) x = C) = foo" +apply(perm_simp) +oops + +lemma + shows "p \ (\B::bool. A \ (B = C)) = foo" +apply (perm_simp) +oops + +lemma + shows "p \ (\x y. \z. x = z \ x = y \ z \ x) = foo" +apply (perm_simp) +oops + +lemma + shows "p \ (\f x. f (g (f x))) = foo" +apply (perm_simp) +oops + +lemma + fixes p q::"perm" + and x::"'a::pt" + shows "p \ (q \ x) = foo" +apply(perm_simp) +oops + +lemma + fixes p q r::"perm" + and x::"'a::pt" + shows "p \ (q \ r \ x) = foo" +apply(perm_simp) +oops + +lemma + fixes p r::"perm" + shows "p \ (\q::perm. q \ (r \ x)) = foo" +apply (perm_simp) +oops + +lemma + fixes C D::"bool" + shows "B (p \ (C = D))" +apply(perm_simp) +oops + +declare [[trace_eqvt = false]] + +text {* there is no raw eqvt-rule for The *} +lemma "p \ (THE x. P x) = foo" +apply(perm_strict_simp exclude: The) +apply(perm_simp exclude: The) +oops + +lemma + fixes P :: "(('b \ bool) \ ('b::pt)) \ ('a::pt)" + shows "p \ (P The) = foo" +apply(perm_simp exclude: The) +oops + +lemma + fixes P :: "('a::pt) \ ('b::pt) \ bool" + shows "p \ (\(a, b). P a b) = (\(a, b). (p \ P) a b)" +apply(perm_simp) +oops + +thm eqvts +thm eqvts_raw + +ML {* Nominal_ThmDecls.is_eqvt @{context} @{term "supp"} *} + + +end diff -r ff22039df778 -r 7fd879774d9b Nominal/Ex/TypeVarsTest.thy --- a/Nominal/Ex/TypeVarsTest.thy Wed Mar 02 12:48:00 2011 +0900 +++ b/Nominal/Ex/TypeVarsTest.thy Wed Mar 02 12:49:01 2011 +0900 @@ -38,6 +38,12 @@ thm lam.fv_bn_eqvt thm lam.size_eqvt +(* FIXME: only works for type variables 'a 'b 'c *) + +nominal_datatype ('a, 'b, 'c) psi = + PsiNil +| Output "'a" "'a" "('a, 'b, 'c) psi" + end diff -r ff22039df778 -r 7fd879774d9b Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Wed Mar 02 12:48:00 2011 +0900 +++ b/Nominal/Nominal2.thy Wed Mar 02 12:49:01 2011 +0900 @@ -1,6 +1,6 @@ theory Nominal2 imports - Nominal2_Base Nominal2_Eqvt Nominal2_Abs + Nominal2_Base Nominal2_Abs uses ("nominal_dt_rawfuns.ML") ("nominal_dt_alpha.ML") ("nominal_dt_quot.ML") diff -r ff22039df778 -r 7fd879774d9b Nominal/Nominal2_Abs.thy --- a/Nominal/Nominal2_Abs.thy Wed Mar 02 12:48:00 2011 +0900 +++ b/Nominal/Nominal2_Abs.thy Wed Mar 02 12:49:01 2011 +0900 @@ -1,6 +1,5 @@ theory Nominal2_Abs imports "Nominal2_Base" - "Nominal2_Eqvt" "~~/src/HOL/Quotient" "~~/src/HOL/Library/Quotient_List" "~~/src/HOL/Library/Quotient_Product" @@ -768,6 +767,15 @@ unfolding fresh_star_def by(auto simp add: Abs_fresh_iff) +lemma Abs_fresh_star2: + fixes x::"'a::fs" + shows "as \ bs = {} \ as \* Abs_set bs x \ as \* x" + and "as \ bs = {} \ as \* Abs_res bs x \ as \* x" + and "cs \ set ds = {} \ cs \* Abs_lst ds x \ cs \* x" + unfolding fresh_star_def Abs_fresh_iff + by auto + + lemma Abs1_eq: fixes x::"'a::fs" shows "Abs_set {a} x = Abs_set {a} y \ x = y" diff -r ff22039df778 -r 7fd879774d9b Nominal/Nominal2_Base.thy --- a/Nominal/Nominal2_Base.thy Wed Mar 02 12:48:00 2011 +0900 +++ b/Nominal/Nominal2_Base.thy Wed Mar 02 12:49:01 2011 +0900 @@ -8,8 +8,12 @@ imports Main "~~/src/HOL/Library/Infinite_Set" "~~/src/HOL/Quotient_Examples/FSet" -uses ("nominal_library.ML") +uses ("nominal_basics.ML") + ("nominal_thmdecls.ML") + ("nominal_permeq.ML") + ("nominal_library.ML") ("nominal_atoms.ML") + ("nominal_eqvt.ML") begin section {* Atoms and Sorts *} @@ -76,6 +80,7 @@ shows "a = b \ sort_of a = sort_of b \ nat_of a = nat_of b" by (induct a, induct b, simp) + section {* Sort-Respecting Permutations *} typedef perm = @@ -146,7 +151,8 @@ instance perm :: size .. -subsection {* Permutations form a group *} + +subsection {* Permutations form a (multiplicative) group *} instantiation perm :: group_add begin @@ -343,7 +349,7 @@ "c \ a \ c \ b \ (a \ b) \ c = c" unfolding swap_atom by simp_all -lemma expand_perm_eq: +lemma perm_eq_iff: fixes p q :: "perm" shows "p = q \ (\a::atom. p \ a = q \ a)" unfolding permute_atom_def @@ -371,30 +377,11 @@ unfolding permute_perm_def by (simp add: diff_minus add_assoc) -lemma permute_eqvt: - shows "p \ (q \ x) = (p \ q) \ (p \ x)" - unfolding permute_perm_def by simp - -lemma zero_perm_eqvt: - shows "p \ (0::perm) = 0" - unfolding permute_perm_def by simp - -lemma add_perm_eqvt: - fixes p p1 p2 :: perm - shows "p \ (p1 + p2) = p \ p1 + p \ p2" - unfolding permute_perm_def - by (simp add: expand_perm_eq) - -lemma swap_eqvt: - shows "p \ (a \ b) = (p \ a \ p \ b)" - unfolding permute_perm_def - by (auto simp add: swap_atom expand_perm_eq) - -lemma uminus_eqvt: - fixes p q::"perm" - shows "p \ (- q) = - (p \ q)" - unfolding permute_perm_def - by (simp add: diff_minus minus_add add_assoc) +lemma pemute_minus_self: + shows "- p \ p = p" + unfolding permute_perm_def + by (simp add: diff_minus add_assoc) + subsection {* Permutations for functions *} @@ -431,38 +418,6 @@ end -lemma Not_eqvt: - 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 all_eqvt: - shows "p \ (\x. P x) = (\x. (p \ P) x)" - unfolding permute_fun_def permute_bool_def - by (auto, drule_tac x="p \ x" in spec, simp) - -lemma ex1_eqvt: - shows "p \ (\!x. P x) = (\!x. (p \ P) x)" - unfolding Ex1_def - apply(simp add: ex_eqvt) - unfolding permute_fun_def - apply(simp add: conj_eqvt all_eqvt) - unfolding permute_fun_def - apply(simp add: imp_eqvt permute_bool_def) - done - lemma permute_boolE: fixes P::"bool" shows "p \ P \ P" @@ -477,7 +432,6 @@ lemma permute_set_eq: fixes x::"'a::pt" - and p::"perm" shows "(p \ X) = {p \ x | x. x \ X}" unfolding permute_fun_def unfolding permute_bool_def @@ -497,15 +451,8 @@ lemma permute_finite [simp]: shows "finite (p \ X) = finite X" -apply(simp add: permute_set_eq_image) -apply(rule iffI) -apply(drule finite_imageD) -using inj_permute[where p="p"] -apply(simp add: inj_on_def) -apply(assumption) -apply(rule finite_imageI) -apply(assumption) -done + unfolding permute_set_eq_vimage + using bij_permute by (rule finite_vimage_iff) lemma swap_set_not_in: assumes a: "a \ S" "b \ S" @@ -536,11 +483,6 @@ unfolding mem_def permute_fun_def permute_bool_def by simp -lemma mem_eqvt: - shows "p \ (x \ A) \ (p \ x) \ (p \ A)" - unfolding mem_def - by (simp add: permute_fun_app_eq) - lemma empty_eqvt: shows "p \ {} = {}" unfolding empty_def Collect_def @@ -550,23 +492,8 @@ shows "p \ (insert x A) = insert (p \ x) (p \ A)" unfolding permute_set_eq_image image_insert .. -lemma Collect_eqvt: - shows "p \ {x. P x} = {x. (p \ P) x}" - unfolding Collect_def permute_fun_def .. - -lemma inter_eqvt: - shows "p \ (A \ B) = (p \ A) \ (p \ B)" - unfolding Int_def - apply(simp add: Collect_eqvt) - apply(simp add: permute_fun_def) - apply(simp add: conj_eqvt) - apply(simp add: mem_eqvt) - apply(simp add: permute_fun_def) - done - - - -subsection {* Permutations for units *} + +subsection {* Permutations for @{typ unit} *} instantiation unit :: pt begin @@ -610,7 +537,7 @@ end -subsection {* Permutations for lists *} +subsection {* Permutations for @{typ "'a list"} *} instantiation list :: (pt) pt begin @@ -630,7 +557,9 @@ shows "p \ (set xs) = set (p \ xs)" by (induct xs) (simp_all add: empty_eqvt insert_eqvt) -subsection {* Permutations for options *} + + +subsection {* Permutations for @{typ "'a option"} *} instantiation option :: (pt) pt begin @@ -647,7 +576,7 @@ end -subsection {* Permutations for fsets *} +subsection {* Permutations for @{typ "'a fset"} *} lemma permute_fset_rsp[quot_respect]: shows "(op = ===> list_eq ===> list_eq) permute permute" @@ -677,6 +606,9 @@ and "(p \ insert_fset x S) = insert_fset (p \ x) (p \ S)" by (lifting permute_list.simps) +lemma fset_eqvt: + shows "p \ (fset S) = fset (p \ S)" + by (lifting set_eqvt) subsection {* Permutations for @{typ char}, @{typ nat}, and @{typ int} *} @@ -757,7 +689,350 @@ instance int :: pure proof qed (rule permute_int_def) -subsection {* Supp, Freshness and Supports *} + +section {* Infrastructure for Equivariance and Perm_simp *} + +subsection {* Basic functions about permutations *} + +use "nominal_basics.ML" + + +subsection {* Eqvt infrastructure *} + +text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *} + +use "nominal_thmdecls.ML" +setup "Nominal_ThmDecls.setup" + + +lemmas [eqvt] = + (* pt types *) + permute_prod.simps + permute_list.simps + permute_option.simps + permute_sum.simps + + (* sets *) + empty_eqvt insert_eqvt set_eqvt + + (* fsets *) + permute_fset fset_eqvt + + + +subsection {* perm_simp infrastructure *} + +definition + "unpermute p = permute (- p)" + +lemma eqvt_apply: + fixes f :: "'a::pt \ 'b::pt" + and x :: "'a::pt" + shows "p \ (f x) \ (p \ f) (p \ x)" + unfolding permute_fun_def by simp + +lemma eqvt_lambda: + fixes f :: "'a::pt \ 'b::pt" + shows "p \ (\x. f x) \ (\x. p \ (f (unpermute p x)))" + unfolding permute_fun_def unpermute_def by simp + +lemma eqvt_bound: + shows "p \ unpermute p x \ x" + unfolding unpermute_def by simp + +text {* provides perm_simp methods *} + +use "nominal_permeq.ML" +setup Nominal_Permeq.setup + +method_setup perm_simp = + {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *} + {* pushes permutations inside. *} + +method_setup perm_strict_simp = + {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *} + {* pushes permutations inside, raises an error if it cannot solve all permutations. *} + + +subsubsection {* Equivariance for permutations and swapping *} + +lemma permute_eqvt: + shows "p \ (q \ x) = (p \ q) \ (p \ x)" + unfolding permute_perm_def by simp + +(* the normal version of this lemma would cause loops *) +lemma permute_eqvt_raw[eqvt_raw]: + shows "p \ permute \ permute" +apply(simp add: fun_eq_iff permute_fun_def) +apply(subst permute_eqvt) +apply(simp) +done + +lemma zero_perm_eqvt [eqvt]: + shows "p \ (0::perm) = 0" + unfolding permute_perm_def by simp + +lemma add_perm_eqvt [eqvt]: + fixes p p1 p2 :: perm + shows "p \ (p1 + p2) = p \ p1 + p \ p2" + unfolding permute_perm_def + by (simp add: perm_eq_iff) + +lemma swap_eqvt [eqvt]: + shows "p \ (a \ b) = (p \ a \ p \ b)" + unfolding permute_perm_def + by (auto simp add: swap_atom perm_eq_iff) + +lemma uminus_eqvt [eqvt]: + fixes p q::"perm" + shows "p \ (- q) = - (p \ q)" + unfolding permute_perm_def + by (simp add: diff_minus minus_add add_assoc) + + +subsubsection {* Equivariance of Logical Operators *} + +lemma eq_eqvt [eqvt]: + shows "p \ (x = y) \ (p \ x) = (p \ y)" + unfolding permute_eq_iff permute_bool_def .. + +lemma Not_eqvt [eqvt]: + shows "p \ (\ A) \ \ (p \ A)" + 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 imp_eqvt [eqvt]: + shows "p \ (A \ B) \ (p \ A) \ (p \ B)" + by (simp add: permute_bool_def) + +declare imp_eqvt[folded induct_implies_def, eqvt] + +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 all_eqvt [eqvt]: + shows "p \ (\x. P x) = (\x. (p \ P) x)" + unfolding permute_fun_def permute_bool_def + by (auto, drule_tac x="p \ x" in spec, simp) + +declare all_eqvt[folded induct_forall_def, eqvt] + +lemma ex1_eqvt [eqvt]: + shows "p \ (\!x. P x) = (\!x. (p \ P) x)" + unfolding Ex1_def + by (perm_simp) (rule refl) + +lemma mem_eqvt [eqvt]: + shows "p \ (x \ A) \ (p \ x) \ (p \ A)" + unfolding mem_def + by (simp add: permute_fun_app_eq) + +lemma Collect_eqvt [eqvt]: + shows "p \ {x. P x} = {x. (p \ P) x}" + unfolding Collect_def permute_fun_def .. + +lemma inter_eqvt [eqvt]: + shows "p \ (A \ B) = (p \ A) \ (p \ B)" + unfolding Int_def + by (perm_simp) (rule refl) + +lemma image_eqvt [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 if_eqvt [eqvt]: + shows "p \ (if b then x else y) = (if p \ b then p \ x else p \ y)" + by (simp add: permute_fun_def permute_bool_def) + +lemma True_eqvt [eqvt]: + shows "p \ True = True" + unfolding permute_bool_def .. + +lemma False_eqvt [eqvt]: + shows "p \ False = False" + unfolding permute_bool_def .. + +lemma disj_eqvt [eqvt]: + shows "p \ (A \ B) \ (p \ A) \ (p \ B)" + by (simp add: permute_bool_def) + +lemma all_eqvt2: + shows "p \ (\x. P x) = (\x. p \ P (- p \ x))" + by (perm_simp add: permute_minus_cancel) (rule refl) + +lemma ex_eqvt2: + shows "p \ (\x. P x) = (\x. p \ P (- p \ x))" + by (perm_simp add: permute_minus_cancel) (rule refl) + +lemma ex1_eqvt2: + shows "p \ (\!x. P x) = (\!x. p \ P (- p \ x))" + by (perm_simp add: permute_minus_cancel) (rule refl) + +lemma the_eqvt: + assumes unique: "\!x. P x" + shows "(p \ (THE x. P x)) = (THE x. (p \ P) x)" + apply(rule the1_equality [symmetric]) + apply(rule_tac p="-p" in permute_boolE) + apply(perm_simp add: permute_minus_cancel) + apply(rule unique) + apply(rule_tac p="-p" in permute_boolE) + apply(perm_simp add: permute_minus_cancel) + apply(rule theI'[OF unique]) + done + +lemma the_eqvt2: + assumes unique: "\!x. P x" + shows "(p \ (THE x. P x)) = (THE x. p \ P (- p \ x))" + apply(rule the1_equality [symmetric]) + apply(simp add: ex1_eqvt2[symmetric]) + apply(simp add: permute_bool_def unique) + apply(simp add: permute_bool_def) + apply(rule theI'[OF unique]) + done + +subsubsection {* Equivariance set operations *} + +lemma Bex_eqvt [eqvt]: + shows "p \ (\x \ S. P x) = (\x \ (p \ S). (p \ P) x)" + unfolding Bex_def + by (perm_simp) (rule refl) + +lemma Ball_eqvt [eqvt]: + shows "p \ (\x \ S. P x) = (\x \ (p \ S). (p \ P) x)" + unfolding Ball_def + by (perm_simp) (rule refl) + +lemma UNIV_eqvt [eqvt]: + shows "p \ UNIV = UNIV" + unfolding UNIV_def + by (perm_simp) (rule refl) + +lemma union_eqvt [eqvt]: + shows "p \ (A \ B) = (p \ A) \ (p \ B)" + unfolding Un_def + by (perm_simp) (rule refl) + +lemma Diff_eqvt [eqvt]: + fixes A B :: "'a::pt set" + shows "p \ (A - B) = (p \ A) - (p \ B)" + unfolding set_diff_eq + by (perm_simp) (rule refl) + +lemma Compl_eqvt [eqvt]: + fixes A :: "'a::pt set" + shows "p \ (- A) = - (p \ A)" + unfolding Compl_eq_Diff_UNIV + by (perm_simp) (rule refl) + +lemma subset_eqvt [eqvt]: + shows "p \ (S \ T) \ (p \ S) \ (p \ T)" + unfolding subset_eq + by (perm_simp) (rule refl) + +lemma psubset_eqvt [eqvt]: + shows "p \ (S \ T) \ (p \ S) \ (p \ T)" + unfolding psubset_eq + by (perm_simp) (rule refl) + +lemma vimage_eqvt [eqvt]: + shows "p \ (f -` A) = (p \ f) -` (p \ A)" + unfolding vimage_def + by (perm_simp) (rule refl) + +lemma Union_eqvt [eqvt]: + shows "p \ (\ S) = \ (p \ S)" + unfolding Union_eq + by (perm_simp) (rule refl) + +(* FIXME: eqvt attribute *) +lemma Sigma_eqvt: + shows "(p \ (X \ Y)) = (p \ X) \ (p \ Y)" +unfolding Sigma_def +unfolding UNION_eq_Union_image +by (perm_simp) (rule refl) + +lemma finite_eqvt [eqvt]: + shows "p \ finite A = finite (p \ A)" + unfolding permute_finite permute_bool_def .. + +subsubsection {* Equivariance for product operations *} + +lemma fst_eqvt [eqvt]: + "p \ (fst x) = fst (p \ x)" + by (cases x) simp + +lemma snd_eqvt [eqvt]: + "p \ (snd x) = snd (p \ x)" + by (cases x) simp + +lemma split_eqvt [eqvt]: + shows "p \ (split P x) = split (p \ P) (p \ x)" + unfolding split_def + by (perm_simp) (rule refl) + + +subsubsection {* Equivariance for list operations *} + +lemma append_eqvt [eqvt]: + shows "p \ (xs @ ys) = (p \ xs) @ (p \ ys)" + by (induct xs) auto + +lemma rev_eqvt [eqvt]: + shows "p \ (rev xs) = rev (p \ xs)" + by (induct xs) (simp_all add: append_eqvt) + +lemma map_eqvt [eqvt]: + shows "p \ (map f xs) = map (p \ f) (p \ xs)" + by (induct xs) (simp_all, simp only: permute_fun_app_eq) + +lemma removeAll_eqvt [eqvt]: + shows "p \ (removeAll x xs) = removeAll (p \ x) (p \ xs)" + by (induct xs) (auto) + +lemma filter_eqvt [eqvt]: + shows "p \ (filter f xs) = filter (p \ f) (p \ xs)" +apply(induct xs) +apply(simp) +apply(simp only: filter.simps permute_list.simps if_eqvt) +apply(simp only: permute_fun_app_eq) +done + +lemma distinct_eqvt [eqvt]: + shows "p \ (distinct xs) = distinct (p \ xs)" +apply(induct xs) +apply(simp add: permute_bool_def) +apply(simp add: conj_eqvt Not_eqvt mem_eqvt set_eqvt) +done + +lemma length_eqvt [eqvt]: + shows "p \ (length xs) = length (p \ xs)" +by (induct xs) (simp_all add: permute_pure) + + +subsubsection {* Equivariance for @{typ "'a fset"} *} + +lemma in_fset_eqvt [eqvt]: + shows "(p \ (x |\| S)) = ((p \ x) |\| (p \ S))" +unfolding in_fset +by (perm_simp) (simp) + +lemma union_fset_eqvt [eqvt]: + shows "(p \ (S |\| T)) = ((p \ S) |\| (p \ T))" +by (induct S) (simp_all) + +lemma map_fset_eqvt [eqvt]: + shows "p \ (map_fset f S) = map_fset (p \ f) (p \ S)" + by (lifting map_eqvt) + + +section {* Supp, Freshness and Supports *} context pt begin @@ -767,13 +1042,13 @@ where "supp x = {a. infinite {b. (a \ b) \ x \ x}}" -end - definition - fresh :: "atom \ 'a::pt \ bool" ("_ \ _" [55, 55] 55) + fresh :: "atom \ 'a \ bool" ("_ \ _" [55, 55] 55) where "a \ x \ a \ supp x" +end + lemma supp_conv_fresh: shows "supp x = {a. \ a \ x}" unfolding fresh_def by simp @@ -838,12 +1113,12 @@ finally show "(p \ a) \ (p \ x) \ a \ x" . qed -lemma fresh_eqvt: +lemma fresh_eqvt [eqvt]: shows "p \ (a \ x) = (p \ a) \ (p \ x)" unfolding permute_bool_def by (simp add: fresh_permute_iff) -lemma supp_eqvt: +lemma supp_eqvt [eqvt]: shows "p \ (supp x) = supp (p \ x)" unfolding supp_conv_fresh unfolding Collect_def @@ -863,7 +1138,7 @@ qed -subsection {* supports *} +section {* supports *} definition supports :: "atom set \ 'a::pt \ bool" (infixl "supports" 80) @@ -881,7 +1156,7 @@ then obtain a where b1: "a \ supp x" and b2: "a \ S" by auto from a1 b2 have "\b. b \ S \ (a \ b) \ x = x" unfolding supports_def by auto then have "{b. (a \ b) \ x \ x} \ S" by auto - with a2 have "finite {b. (a \ b)\x \ x}" by (simp add: finite_subset) + with a2 have "finite {b. (a \ b) \ x \ x}" by (simp add: finite_subset) then have "a \ (supp x)" unfolding supp_def by simp with b1 show False by simp qed @@ -972,7 +1247,8 @@ assumes finite_supp: "finite (supp x)" lemma pure_supp: - shows "supp (x::'a::pure) = {}" + fixes x::"'a::pure" + shows "supp x = {}" unfolding supp_def by (simp add: permute_pure) lemma pure_fresh: @@ -1026,7 +1302,7 @@ apply (rule supports_perm) apply (rule finite_perm_lemma) apply (simp add: perm_swap_eq swap_eqvt) -apply (auto simp add: expand_perm_eq swap_atom) +apply (auto simp add: perm_eq_iff swap_atom) done lemma fresh_perm: @@ -1074,14 +1350,11 @@ unfolding supp_conv_fresh by (simp add: fresh_minus_perm) -instance perm :: fs -by default (simp add: supp_perm finite_perm_lemma) - lemma plus_perm_eq: fixes p q::"perm" assumes asm: "supp p \ supp q = {}" shows "p + q = q + p" -unfolding expand_perm_eq +unfolding perm_eq_iff proof fix a::"atom" show "(p + q) \ a = (q + p) \ a" @@ -1135,6 +1408,10 @@ by blast qed +instance perm :: fs +by default (simp add: supp_perm finite_perm_lemma) + + section {* Finite Support instances for other types *} @@ -1240,6 +1517,25 @@ shows "a \ (xs @ ys) \ a \ xs \ a \ ys" by (induct xs) (simp_all add: fresh_Nil fresh_Cons) +lemma supp_rev: + shows "supp (rev xs) = supp xs" + by (induct xs) (auto simp add: supp_append supp_Cons supp_Nil) + +lemma fresh_rev: + shows "a \ rev xs \ a \ xs" + by (induct xs) (auto simp add: fresh_append fresh_Cons fresh_Nil) + +lemma supp_removeAll: + fixes x::"atom" + shows "supp (removeAll x xs) = supp xs - {x}" + by (induct xs) + (auto simp add: supp_Nil supp_Cons supp_atom) + +lemma supp_of_atom_list: + fixes as::"atom list" + shows "supp as = set as" +by (induct as) + (simp_all add: supp_Nil supp_Cons supp_atom) instance list :: (fs) fs apply default @@ -1247,12 +1543,6 @@ apply (simp_all add: supp_Nil supp_Cons finite_supp) done -lemma supp_of_atom_list: - fixes as::"atom list" - shows "supp as = set as" -by (induct as) - (simp_all add: supp_Nil supp_Cons supp_atom) - section {* Support and Freshness for Applications *} @@ -1261,19 +1551,12 @@ unfolding fresh_def supp_def unfolding MOST_iff_cofinite by simp -lemma supp_subset_fresh: - assumes a: "\a. a \ x \ a \ y" - shows "supp y \ supp x" - using a - unfolding fresh_def - by blast - lemma fresh_fun_app: assumes "a \ f" and "a \ x" shows "a \ f x" using assms unfolding fresh_conv_MOST - unfolding permute_fun_app_eq + unfolding permute_fun_app_eq by (elim MOST_rev_mp, simp) lemma supp_fun_app: @@ -1282,11 +1565,19 @@ unfolding fresh_def by auto -text {* Equivariant Functions *} + +subsection {* Equivariance Predicate @{text eqvt} and @{text eqvt_at}*} definition "eqvt f \ \p. p \ f = f" + +text {* equivariance of a function at a given argument *} + +definition + "eqvt_at f x \ \p. p \ (f x) = f (p \ x)" + + lemma eqvtI: shows "(\p. p \ f \ f) \ eqvt f" unfolding eqvt_def @@ -1310,9 +1601,12 @@ using supp_fun_app by auto qed -text {* equivariance of a function at a given argument *} -definition - "eqvt_at f x \ \p. p \ (f x) = f (p \ x)" +lemma supp_fun_app_eqvt: + assumes a: "eqvt f" + shows "supp (f x) \ supp x" + using fresh_fun_eqvt_app[OF a] + unfolding fresh_def + by auto lemma supp_eqvt_at: assumes asm: "eqvt_at f x" @@ -1346,7 +1640,8 @@ using supp_eqvt_at[OF asm fin] by auto -text {* helper functions for nominal_functions *} + +subsection {* helper functions for nominal_functions *} lemma the_default_eqvt: assumes unique: "\!x. P x" @@ -1409,6 +1704,7 @@ using assms by (auto intro: fundef_ex1_eqvt) + section {* Support of Finite Sets of Finitely Supported Elements *} text {* support and freshness for atom sets *} @@ -1438,27 +1734,6 @@ unfolding fresh_def by (auto simp add: supp_finite_atom_set assms) - -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) - unfolding eqvt_def - unfolding permute_fun_def - apply(simp) - unfolding UNION_def - unfolding Collect_def - unfolding Bex_def - apply(simp add: ex_eqvt) - unfolding permute_fun_def - apply(simp add: conj_eqvt) - apply(simp add: mem_eqvt) - apply(simp add: supp_eqvt) - unfolding permute_fun_def - apply(simp) - apply(assumption) - done - lemma Union_supports_set: shows "(\x \ S. supp x) supports S" proof - @@ -1482,12 +1757,14 @@ assumes fin: "finite S" shows "(\x\S. supp x) \ supp S" proof - + have eqvt: "eqvt (\S. \ supp ` S)" + unfolding eqvt_def + by (perm_simp) (simp) have "(\x\S. supp x) = supp (\x\S. supp x)" - by (rule supp_finite_atom_set[symmetric]) - (rule Union_of_finite_supp_sets[OF fin]) - also have "\ \ supp S" - by (rule supp_subset_fresh) - (simp add: Union_fresh) + by (rule supp_finite_atom_set[symmetric]) (rule Union_of_finite_supp_sets[OF fin]) + also have "\ = supp ((\S. \ supp ` S) S)" by simp + also have "\ \ supp S" using eqvt + by (rule supp_fun_app_eqvt) finally show "(\x\S. supp x) \ supp S" . qed @@ -1557,10 +1834,6 @@ subsection {* Type @{typ "'a fset"} is finitely supported *} -lemma fset_eqvt: - shows "p \ (fset S) = fset (p \ S)" - by (lifting set_eqvt) - lemma supp_fset [simp]: shows "supp (fset S) = supp S" unfolding supp_def @@ -1596,6 +1869,16 @@ shows "finite (supp S)" by (induct S) (simp_all add: finite_supp) +lemma supp_union_fset: + fixes S T::"'a::fs fset" + shows "supp (S |\| T) = supp S \ supp T" +by (induct S) (auto) + +lemma fresh_union_fset: + fixes S T::"'a::fs fset" + shows "a \ S |\| T \ a \ S \ a \ T" +unfolding fresh_def +by (simp add: supp_union_fset) instance fset :: (fs) fs apply (default) @@ -1654,7 +1937,6 @@ done lemma fresh_star_atom_set_conv: - fixes p::"perm" assumes fresh: "as \* bs" and fin: "finite as" "finite bs" shows "bs \* as" @@ -1662,6 +1944,13 @@ unfolding fresh_star_def fresh_def by (auto simp add: supp_finite_atom_set fin) +lemma atom_fresh_star_disjoint: + assumes fin: "finite bs" + shows "as \* bs \ (as \ bs = {})" + +unfolding fresh_star_def fresh_def +by (auto simp add: supp_finite_atom_set fin) + lemma fresh_star_Pair: shows "as \* (x, y) = (as \* x \ as \* y)" @@ -1738,23 +2027,11 @@ unfolding fresh_star_def by (metis mem_permute_iff permute_minus_cancel(1) fresh_permute_iff) -lemma fresh_star_eqvt: +lemma fresh_star_eqvt [eqvt]: shows "p \ (as \* x) \ (p \ as) \* (p \ x)" unfolding fresh_star_def -unfolding Ball_def -apply(simp add: all_eqvt) -apply(subst permute_fun_def) -apply(simp add: imp_eqvt fresh_eqvt mem_eqvt) -done - -lemma at_fresh_star_inter: - assumes a: "(p \ bs) \* bs" - and b: "finite bs" - shows "p \ bs \ bs = {}" -using a b -unfolding fresh_star_def -unfolding fresh_def -by (auto simp add: supp_finite_atom_set) +by (perm_simp) (rule refl) + section {* Induction principle for permutations *} @@ -1773,7 +2050,7 @@ then have ih: "\q. supp q \ supp p \ P q" by auto have as: "supp p \ S" by fact { assume "supp p = {}" - then have "p = 0" by (simp add: supp_perm expand_perm_eq) + then have "p = 0" by (simp add: supp_perm perm_eq_iff) then have "P p" using zero by simp } moreover @@ -1792,7 +2069,7 @@ have "supp ?q \ S" using as a2 by simp ultimately have "P ((p \ a \ a) + ?q)" using as a1 swap by simp moreover - have "p = (p \ a \ a) + ?q" by (simp add: expand_perm_eq) + have "p = (p \ a \ a) + ?q" by (simp add: perm_eq_iff) ultimately have "P p" by simp } ultimately show "P p" by blast @@ -2186,6 +2463,8 @@ assumes atom_eq_iff [simp]: "atom a = atom b \ a = b" assumes atom_eqvt: "p \ (atom a) = atom (p \ a)" +declare atom_eqvt[eqvt] + class at = at_base + assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)" @@ -2295,6 +2574,7 @@ where "(a \ b) = (atom a \ atom b)" + lemma flip_self [simp]: "(a \ a) = 0" unfolding flip_def by (rule swap_self) @@ -2313,7 +2593,7 @@ lemma permute_flip_cancel2 [simp]: "(a \ b) \ (b \ a) \ x = x" by (simp add: flip_commute) -lemma flip_eqvt: +lemma flip_eqvt [eqvt]: fixes a b c::"'a::at_base" shows "p \ (a \ b) = (p \ a \ p \ b)" unfolding flip_def @@ -2633,5 +2913,10 @@ use "nominal_atoms.ML" +section {* automatic equivariance procedure for inductive definitions *} + +use "nominal_eqvt.ML" + + end diff -r ff22039df778 -r 7fd879774d9b Nominal/Nominal2_Eqvt.thy --- a/Nominal/Nominal2_Eqvt.thy Wed Mar 02 12:48:00 2011 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,426 +0,0 @@ -(* Title: Nominal2_Eqvt - Author: Brian Huffman, - Author: Christian Urban - - Equivariance, supp and freshness lemmas for various operators - (contains many, but not all such lemmas). -*) -theory Nominal2_Eqvt -imports Nominal2_Base -uses ("nominal_thmdecls.ML") - ("nominal_permeq.ML") - ("nominal_eqvt.ML") -begin - - -section {* Permsimp and Eqvt infrastructure *} - -text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *} - -use "nominal_thmdecls.ML" -setup "Nominal_ThmDecls.setup" - - -section {* eqvt lemmas *} - -lemmas [eqvt] = - conj_eqvt Not_eqvt ex_eqvt all_eqvt ex1_eqvt imp_eqvt uminus_eqvt - imp_eqvt[folded induct_implies_def] - all_eqvt[folded induct_forall_def] - - (* nominal *) - supp_eqvt fresh_eqvt fresh_star_eqvt add_perm_eqvt atom_eqvt - swap_eqvt flip_eqvt - - (* datatypes *) - Pair_eqvt permute_list.simps permute_option.simps - permute_sum.simps - - (* sets *) - mem_eqvt empty_eqvt insert_eqvt set_eqvt inter_eqvt - - (* fsets *) - permute_fset fset_eqvt - - -text {* helper lemmas for the perm_simp *} - -definition - "unpermute p = permute (- p)" - -lemma eqvt_apply: - fixes f :: "'a::pt \ 'b::pt" - and x :: "'a::pt" - shows "p \ (f x) \ (p \ f) (p \ x)" - unfolding permute_fun_def by simp - -lemma eqvt_lambda: - fixes f :: "'a::pt \ 'b::pt" - shows "p \ (\x. f x) \ (\x. p \ (f (unpermute p x)))" - unfolding permute_fun_def unpermute_def by simp - -lemma eqvt_bound: - shows "p \ unpermute p x \ x" - unfolding unpermute_def by simp - -text {* provides perm_simp methods *} - -use "nominal_permeq.ML" -setup Nominal_Permeq.setup - -method_setup perm_simp = - {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *} - {* pushes permutations inside. *} - -method_setup perm_strict_simp = - {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *} - {* pushes permutations inside, raises an error if it cannot solve all permutations. *} - -(* the normal version of this lemma would cause loops *) -lemma permute_eqvt_raw[eqvt_raw]: - shows "p \ permute \ permute" -apply(simp add: fun_eq_iff permute_fun_def) -apply(subst permute_eqvt) -apply(simp) -done - -subsection {* Equivariance of Logical Operators *} - -lemma eq_eqvt[eqvt]: - shows "p \ (x = y) \ (p \ x) = (p \ y)" - unfolding permute_eq_iff permute_bool_def .. - -lemma if_eqvt[eqvt]: - shows "p \ (if b then x else y) = (if p \ b then p \ x else p \ y)" - by (simp add: permute_fun_def permute_bool_def) - -lemma True_eqvt[eqvt]: - shows "p \ True = True" - unfolding permute_bool_def .. - -lemma False_eqvt[eqvt]: - shows "p \ False = False" - unfolding permute_bool_def .. - -lemma disj_eqvt[eqvt]: - shows "p \ (A \ B) = ((p \ A) \ (p \ B))" - by (simp add: permute_bool_def) - -lemma all_eqvt2: - shows "p \ (\x. P x) = (\x. p \ P (- p \ x))" - by (perm_simp add: permute_minus_cancel) (rule refl) - -lemma ex_eqvt2: - shows "p \ (\x. P x) = (\x. p \ P (- p \ x))" - by (perm_simp add: permute_minus_cancel) (rule refl) - -lemma ex1_eqvt2: - shows "p \ (\!x. P x) = (\!x. p \ P (- p \ x))" - by (perm_simp add: permute_minus_cancel) (rule refl) - -lemma the_eqvt: - assumes unique: "\!x. P x" - shows "(p \ (THE x. P x)) = (THE x. (p \ P) x)" - apply(rule the1_equality [symmetric]) - apply(rule_tac p="-p" in permute_boolE) - apply(perm_simp add: permute_minus_cancel) - apply(rule unique) - apply(rule_tac p="-p" in permute_boolE) - apply(perm_simp add: permute_minus_cancel) - apply(rule theI'[OF unique]) - done - -lemma the_eqvt2: - assumes unique: "\!x. P x" - shows "(p \ (THE x. P x)) = (THE x. p \ P (- p \ x))" - apply(rule the1_equality [symmetric]) - apply(simp add: ex1_eqvt2[symmetric]) - apply(simp add: permute_bool_def unique) - apply(simp add: permute_bool_def) - apply(rule theI'[OF unique]) - done - -subsection {* Equivariance Set Operations *} - -lemma not_mem_eqvt: - shows "p \ (x \ A) \ (p \ x) \ (p \ A)" - by (perm_simp) (rule refl) - -lemma Collect_eqvt[eqvt]: - shows "p \ {x. P x} = {x. (p \ P) x}" - unfolding Collect_def permute_fun_def .. - -lemma Collect_eqvt2: - shows "p \ {x. P x} = {x. p \ (P (-p \ x))}" - by (perm_simp add: permute_minus_cancel) (rule refl) - -lemma Bex_eqvt[eqvt]: - shows "p \ (\x \ S. P x) = (\x \ (p \ S). (p \ P) x)" - unfolding Bex_def - by (perm_simp) (rule refl) - -lemma Ball_eqvt[eqvt]: - shows "p \ (\x \ S. P x) = (\x \ (p \ S). (p \ P) x)" - unfolding Ball_def - by (perm_simp) (rule refl) - -lemma UNIV_eqvt[eqvt]: - shows "p \ UNIV = UNIV" - unfolding UNIV_def - by (perm_simp) (rule refl) - -lemma union_eqvt[eqvt]: - shows "p \ (A \ B) = (p \ A) \ (p \ B)" - unfolding Un_def - by (perm_simp) (rule refl) - -lemma Diff_eqvt[eqvt]: - fixes A B :: "'a::pt set" - shows "p \ (A - B) = p \ A - p \ B" - unfolding set_diff_eq - by (perm_simp) (rule refl) - -lemma Compl_eqvt[eqvt]: - fixes A :: "'a::pt set" - shows "p \ (- A) = - (p \ A)" - unfolding Compl_eq_Diff_UNIV - by (perm_simp) (rule refl) - -lemma subset_eqvt[eqvt]: - shows "p \ (S \ T) \ (p \ S) \ (p \ T)" - unfolding subset_eq - by (perm_simp) (rule refl) - -lemma psubset_eqvt[eqvt]: - shows "p \ (S \ T) \ (p \ S) \ (p \ T)" - unfolding psubset_eq - by (perm_simp) (rule refl) - -lemma image_eqvt[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 - by (perm_simp) (rule refl) - -lemma Union_eqvt[eqvt]: - shows "p \ (\ S) = \ (p \ S)" - unfolding Union_eq - by (perm_simp) (rule refl) - -lemma Sigma_eqvt: - shows "(p \ (X \ Y)) = (p \ X) \ (p \ Y)" -unfolding Sigma_def -unfolding UNION_eq_Union_image -by (perm_simp) (rule refl) - -lemma finite_permute_iff: - shows "finite (p \ A) \ finite A" - unfolding permute_set_eq_vimage - using bij_permute by (rule finite_vimage_iff) - -lemma finite_eqvt[eqvt]: - shows "p \ finite A = finite (p \ A)" - unfolding finite_permute_iff permute_bool_def .. - - -section {* List Operations *} - -lemma append_eqvt[eqvt]: - shows "p \ (xs @ ys) = (p \ xs) @ (p \ ys)" - by (induct xs) auto - -lemma rev_eqvt[eqvt]: - shows "p \ (rev xs) = rev (p \ xs)" - by (induct xs) (simp_all add: append_eqvt) - -lemma supp_rev: - shows "supp (rev xs) = supp xs" - by (induct xs) (auto simp add: supp_append supp_Cons supp_Nil) - -lemma fresh_rev: - shows "a \ rev xs \ a \ xs" - by (induct xs) (auto simp add: fresh_append fresh_Cons fresh_Nil) - -lemma map_eqvt[eqvt]: - shows "p \ (map f xs) = map (p \ f) (p \ xs)" - by (induct xs) (simp_all, simp only: permute_fun_app_eq) - -lemma removeAll_eqvt[eqvt]: - shows "p \ (removeAll x xs) = removeAll (p \ x) (p \ xs)" - by (induct xs) (auto) - -lemma supp_removeAll: - fixes x::"atom" - shows "supp (removeAll x xs) = supp xs - {x}" - by (induct xs) - (auto simp add: supp_Nil supp_Cons supp_atom) - -lemma filter_eqvt[eqvt]: - shows "p \ (filter f xs) = filter (p \ f) (p \ xs)" -apply(induct xs) -apply(simp) -apply(simp only: filter.simps permute_list.simps if_eqvt) -apply(simp only: permute_fun_app_eq) -done - -lemma distinct_eqvt[eqvt]: - shows "p \ (distinct xs) = distinct (p \ xs)" -apply(induct xs) -apply(simp add: permute_bool_def) -apply(simp add: conj_eqvt Not_eqvt mem_eqvt set_eqvt) -done - -lemma length_eqvt[eqvt]: - shows "p \ (length xs) = length (p \ xs)" -by (induct xs) (simp_all add: permute_pure) - - -subsection {* Equivariance Finite-Set Operations *} - -lemma in_fset_eqvt[eqvt]: - shows "(p \ (x |\| S)) = ((p \ x) |\| (p \ S))" -unfolding in_fset -by (perm_simp) (simp) - -lemma union_fset_eqvt[eqvt]: - shows "(p \ (S |\| T)) = ((p \ S) |\| (p \ T))" -by (induct S) (simp_all) - -lemma supp_union_fset: - fixes S T::"'a::fs fset" - shows "supp (S |\| T) = supp S \ supp T" -by (induct S) (auto) - -lemma fresh_union_fset: - fixes S T::"'a::fs fset" - shows "a \ S |\| T \ a \ S \ a \ T" -unfolding fresh_def -by (simp add: supp_union_fset) - -lemma map_fset_eqvt[eqvt]: - shows "p \ (map_fset f S) = map_fset (p \ f) (p \ S)" - by (lifting map_eqvt) - - -subsection {* Product Operations *} - -lemma fst_eqvt[eqvt]: - "p \ (fst x) = fst (p \ x)" - by (cases x) simp - -lemma snd_eqvt[eqvt]: - "p \ (snd x) = snd (p \ x)" - by (cases x) simp - -lemma split_eqvt[eqvt]: - shows "p \ (split P x) = split (p \ P) (p \ x)" - unfolding split_def - by (perm_simp) (rule refl) - - -section {* Test cases *} - - -declare [[trace_eqvt = false]] -(* declare [[trace_eqvt = true]] *) - -lemma - fixes B::"'a::pt" - shows "p \ (B = C)" -apply(perm_simp) -oops - -lemma - fixes B::"bool" - shows "p \ (B = C)" -apply(perm_simp) -oops - -lemma - fixes B::"bool" - shows "p \ (A \ B = C)" -apply (perm_simp) -oops - -lemma - shows "p \ (\(x::'a::pt). A \ (B::'a \ bool) x = C) = foo" -apply(perm_simp) -oops - -lemma - shows "p \ (\B::bool. A \ (B = C)) = foo" -apply (perm_simp) -oops - -lemma - shows "p \ (\x y. \z. x = z \ x = y \ z \ x) = foo" -apply (perm_simp) -oops - -lemma - shows "p \ (\f x. f (g (f x))) = foo" -apply (perm_simp) -oops - -lemma - fixes p q::"perm" - and x::"'a::pt" - shows "p \ (q \ x) = foo" -apply(perm_simp) -oops - -lemma - fixes p q r::"perm" - and x::"'a::pt" - shows "p \ (q \ r \ x) = foo" -apply(perm_simp) -oops - -lemma - fixes p r::"perm" - shows "p \ (\q::perm. q \ (r \ x)) = foo" -apply (perm_simp) -oops - -lemma - fixes C D::"bool" - shows "B (p \ (C = D))" -apply(perm_simp) -oops - -declare [[trace_eqvt = false]] - -text {* there is no raw eqvt-rule for The *} -lemma "p \ (THE x. P x) = foo" -apply(perm_strict_simp exclude: The) -apply(perm_simp exclude: The) -oops - -lemma - fixes P :: "(('b \ bool) \ ('b::pt)) \ ('a::pt)" - shows "p \ (P The) = foo" -apply(perm_simp exclude: The) -oops - -lemma - fixes P :: "('a::pt) \ ('b::pt) \ bool" - shows "p \ (\(a, b). P a b) = (\(a, b). (p \ P) a b)" -apply(perm_simp) -oops - -thm eqvts -thm eqvts_raw - -ML {* Nominal_ThmDecls.is_eqvt @{context} @{term "supp"} *} - - -section {* automatic equivariance procedure for inductive definitions *} - -use "nominal_eqvt.ML" - -end diff -r ff22039df778 -r 7fd879774d9b Nominal/ROOT.ML --- a/Nominal/ROOT.ML Wed Mar 02 12:48:00 2011 +0900 +++ b/Nominal/ROOT.ML Wed Mar 02 12:49:01 2011 +0900 @@ -2,6 +2,7 @@ no_document use_thys ["Atoms", + "Eqvt", "Ex/Weakening", "Ex/Classical", "Ex/Datatypes", diff -r ff22039df778 -r 7fd879774d9b Nominal/nominal_basics.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/nominal_basics.ML Wed Mar 02 12:49:01 2011 +0900 @@ -0,0 +1,152 @@ +(* Title: nominal_basic.ML + Author: Christian Urban + + Basic functions for nominal. +*) + +signature NOMINAL_BASIC = +sig + val trace: bool Unsynchronized.ref + val trace_msg: (unit -> string) -> unit + + val last2: 'a list -> 'a * 'a + val split_last2: 'a list -> 'a list * 'a * 'a + val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list + val order_default: ('a * 'a -> bool) -> 'b -> 'a list -> ('a * 'b) list -> 'b list + val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list + val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list + val split_filter: ('a -> bool) -> 'a list -> 'a list * 'a list + val fold_left: ('a * 'a -> 'a) -> 'a list -> 'a -> 'a + + val is_true: term -> bool + + val dest_listT: typ -> typ + val dest_fsetT: typ -> typ + + val mk_id: term -> term + val mk_all: (string * typ) -> term -> term + val mk_All: (string * typ) -> term -> term + val mk_exists: (string * typ) -> term -> term + + val sum_case_const: typ -> typ -> typ -> term + val mk_sum_case: term -> term -> term + + val mk_equiv: thm -> thm + val safe_mk_equiv: thm -> thm + + val mk_minus: term -> term + val mk_plus: term -> term -> term + + val perm_ty: typ -> typ + val perm_const: typ -> term + val mk_perm_ty: typ -> term -> term -> term + val mk_perm: term -> term -> term + val dest_perm: term -> term * term + +end + + +structure Nominal_Basic: NOMINAL_BASIC = +struct + +val trace = Unsynchronized.ref false +fun trace_msg msg = if ! trace then tracing (msg ()) else () + + +(* orders an AList according to keys - every key needs to be there *) +fun order eq keys list = + map (the o AList.lookup eq list) keys + +(* orders an AList according to keys - returns default for non-existing keys *) +fun order_default eq default keys list = + map (the_default default o AList.lookup eq list) keys + +(* remove duplicates *) +fun remove_dups eq [] = [] + | remove_dups eq (x :: xs) = + if member eq xs x + then remove_dups eq xs + else x :: remove_dups eq xs + +fun last2 [] = raise Empty + | last2 [_] = raise Empty + | last2 [x, y] = (x, y) + | last2 (_ :: xs) = last2 xs + +fun split_last2 xs = + let + val (xs', x) = split_last xs + val (xs'', y) = split_last xs' + in + (xs'', y, x) + end + +fun map4 _ [] [] [] [] = [] + | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us + +fun split_filter f [] = ([], []) + | split_filter f (x :: xs) = + let + val (r, l) = split_filter f xs + in + if f x + then (x :: r, l) + else (r, x :: l) + end + +(* to be used with left-infix binop-operations *) +fun fold_left f [] z = z + | fold_left f [x] z = x + | fold_left f (x :: y :: xs) z = fold_left f (f (x, y) :: xs) z + + + +fun is_true @{term "Trueprop True"} = true + | is_true _ = false + +fun dest_listT (Type (@{type_name list}, [T])) = T + | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) + +fun dest_fsetT (Type (@{type_name fset}, [T])) = T + | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); + + +fun mk_id trm = HOLogic.id_const (fastype_of trm) $ trm + +fun mk_all (a, T) t = Term.all T $ Abs (a, T, t) + +fun mk_All (a, T) t = HOLogic.all_const T $ Abs (a, T, t) + +fun mk_exists (a, T) t = HOLogic.exists_const T $ Abs (a, T, t) + +fun sum_case_const ty1 ty2 ty3 = + Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3) + +fun mk_sum_case trm1 trm2 = + let + val ([ty1], ty3) = strip_type (fastype_of trm1) + val ty2 = domain_type (fastype_of trm2) + in + sum_case_const ty1 ty2 ty3 $ trm1 $ trm2 + end + + +fun mk_equiv r = r RS @{thm eq_reflection}; +fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; + + +fun mk_minus p = @{term "uminus::perm => perm"} $ p + +fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q + +fun perm_ty ty = @{typ "perm"} --> ty --> ty +fun perm_const ty = Const (@{const_name "permute"}, perm_ty ty) +fun mk_perm_ty ty p trm = perm_const ty $ p $ trm +fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm + +fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) + | dest_perm t = raise TERM ("dest_perm", [t]); + +end (* structure *) + +open Nominal_Basic; \ No newline at end of file diff -r ff22039df778 -r 7fd879774d9b Nominal/nominal_library.ML --- a/Nominal/nominal_library.ML Wed Mar 02 12:48:00 2011 +0900 +++ b/Nominal/nominal_library.ML Wed Mar 02 12:49:01 2011 +0900 @@ -1,45 +1,11 @@ (* Title: nominal_library.ML Author: Christian Urban - Basic functions for nominal. + Library functions for nominal. *) signature NOMINAL_LIBRARY = sig - val trace: bool Unsynchronized.ref - val trace_msg: (unit -> string) -> unit - - val last2: 'a list -> 'a * 'a - val split_last2: 'a list -> 'a list * 'a * 'a - val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list - val order_default: ('a * 'a -> bool) -> 'b -> 'a list -> ('a * 'b) list -> 'b list - val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list - val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list - val split_filter: ('a -> bool) -> 'a list -> 'a list * 'a list - val fold_left: ('a * 'a -> 'a) -> 'a list -> 'a -> 'a - - val is_true: term -> bool - - val dest_listT: typ -> typ - val dest_fsetT: typ -> typ - - val mk_id: term -> term - val mk_all: (string * typ) -> term -> term - val mk_All: (string * typ) -> term -> term - val mk_exists: (string * typ) -> term -> term - - val sum_case_const: typ -> typ -> typ -> term - val mk_sum_case: term -> term -> term - - val mk_minus: term -> term - val mk_plus: term -> term -> term - - val perm_ty: typ -> typ - val perm_const: typ -> term - val mk_perm_ty: typ -> term -> term -> term - val mk_perm: term -> term -> term - val dest_perm: term -> term * term - val mk_sort_of: term -> term val atom_ty: typ -> typ val atom_const: typ -> term @@ -91,9 +57,6 @@ val mk_finite_ty: typ -> term -> term val mk_finite: term -> term - val mk_equiv: thm -> thm - val safe_mk_equiv: thm -> thm - val mk_diff: term * term -> term val mk_append: term * term -> term val mk_union: term * term -> term @@ -144,101 +107,6 @@ structure Nominal_Library: NOMINAL_LIBRARY = struct -val trace = Unsynchronized.ref false -fun trace_msg msg = if ! trace then tracing (msg ()) else () - - -(* orders an AList according to keys - every key needs to be there *) -fun order eq keys list = - map (the o AList.lookup eq list) keys - -(* orders an AList according to keys - returns default for non-existing keys *) -fun order_default eq default keys list = - map (the_default default o AList.lookup eq list) keys - -(* remove duplicates *) -fun remove_dups eq [] = [] - | remove_dups eq (x :: xs) = - if member eq xs x - then remove_dups eq xs - else x :: remove_dups eq xs - -fun last2 [] = raise Empty - | last2 [_] = raise Empty - | last2 [x, y] = (x, y) - | last2 (_ :: xs) = last2 xs - -fun split_last2 xs = - let - val (xs', x) = split_last xs - val (xs'', y) = split_last xs' - in - (xs'', y, x) - end - -fun map4 _ [] [] [] [] = [] - | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us - -fun split_filter f [] = ([], []) - | split_filter f (x :: xs) = - let - val (r, l) = split_filter f xs - in - if f x - then (x :: r, l) - else (r, x :: l) - end - -(* to be used with left-infix binop-operations *) -fun fold_left f [] z = z - | fold_left f [x] z = x - | fold_left f (x :: y :: xs) z = fold_left f (f (x, y) :: xs) z - - - -fun is_true @{term "Trueprop True"} = true - | is_true _ = false - -fun dest_listT (Type (@{type_name list}, [T])) = T - | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) - -fun dest_fsetT (Type (@{type_name fset}, [T])) = T - | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); - - -fun mk_id trm = HOLogic.id_const (fastype_of trm) $ trm - -fun mk_all (a, T) t = Term.all T $ Abs (a, T, t) - -fun mk_All (a, T) t = HOLogic.all_const T $ Abs (a, T, t) - -fun mk_exists (a, T) t = HOLogic.exists_const T $ Abs (a, T, t) - -fun sum_case_const ty1 ty2 ty3 = - Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3) - -fun mk_sum_case trm1 trm2 = - let - val ([ty1], ty3) = strip_type (fastype_of trm1) - val ty2 = domain_type (fastype_of trm2) - in - sum_case_const ty1 ty2 ty3 $ trm1 $ trm2 - end - - - -fun mk_minus p = @{term "uminus::perm => perm"} $ p - -fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q - -fun perm_ty ty = @{typ "perm"} --> ty --> ty -fun perm_const ty = Const (@{const_name "permute"}, perm_ty ty) -fun mk_perm_ty ty p trm = perm_const ty $ p $ trm -fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm - -fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t) - | dest_perm t = raise TERM ("dest_perm", [t]); - fun mk_sort_of t = @{term "sort_of"} $ t; fun atom_ty ty = ty --> @{typ "atom"}; @@ -358,10 +226,6 @@ fun mk_finite t = mk_finite_ty (fastype_of t) t -fun mk_equiv r = r RS @{thm eq_reflection}; -fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r; - - (* functions that construct differences, appends and unions but avoid producing empty atom sets or empty atom lists *) diff -r ff22039df778 -r 7fd879774d9b Pearl-jv/Paper.thy --- a/Pearl-jv/Paper.thy Wed Mar 02 12:48:00 2011 +0900 +++ b/Pearl-jv/Paper.thy Wed Mar 02 12:49:01 2011 +0900 @@ -1,9 +1,8 @@ (*<*) theory Paper imports "../Nominal/Nominal2_Base" - "../Nominal/Nominal2_Eqvt" "../Nominal/Atoms" - "../Nominal/Abs" + "../Nominal/Nominal2_Abs" "LaTeXsugar" begin @@ -41,15 +40,11 @@ (*>*) -(* - TODO: write about supp of finite sets, abstraction over finite sets -*) - section {* Introduction *} text {* Nominal Isabelle provides a proving infratructure for convenient reasoning - about programming language calculi involving binders such as lambda abstractions or + about programming language calculi involving binders, such as lambda abstractions or quantifications in type schemes: \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% @@ -59,129 +54,14 @@ \noindent At its core Nominal Isabelle is based on the nominal logic work by Pitts at - al \cite{GabbayPitts02,Pitts03}. The most basic notion in this work is a + al \cite{GabbayPitts02,Pitts03}, whose most basic notion is a sort-respecting permutation operation defined over a countably infinite - collection of sorted atoms. The atoms are used for representing variable names - that might be bound or free. Multiple sorts are necessary for being able to - represent different kinds of variables. For example, in the language Mini-ML - there are bound term variables in lambda abstractions and bound type variables in - type schemes. In order to be able to separate them, each kind of variables needs to be - represented by a different sort of atoms. - - The existing nominal logic work usually leaves implicit the sorting - information for atoms and as far as we know leaves out a description of how - sorts are represented. In our formalisation, we therefore have to make a - design decision about how to implement sorted atoms and sort-respecting - permutations. One possibility, which we described in \cite{Urban08}, is to - have separate types for the different - kinds of atoms, say types @{text "\\<^isub>1,\,\\<^isub>n"}. With this - design one can represent permutations as lists of pairs of atoms and the - operation of applying a permutation to an object as the function - - - @{text [display,indent=10] "_ \ _ :: (\ \ \) list \ \ \ \"} - - \noindent - where @{text "\"} stands for a type of atoms and @{text "\"} for the type - of the objects on which the permutation acts. For atoms - the permutation operation is defined over the length of lists as follows - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} - @{text "[] \ c"} & @{text "="} & @{text c}\\ - @{text "(a b)::\ \ c"} & @{text "="} & - $\begin{cases} @{text a} & \textrm{if}~@{text "\ \ c = b"}\\ - @{text b} & \textrm{if}~@{text "\ \ c = a"}\\ - @{text "\ \ c"} & \textrm{otherwise}\end{cases}$ - \end{tabular}\hfill\numbered{atomperm} - \end{isabelle} - - \noindent - where we write @{text "(a b)"} for a swapping of atoms @{text "a"} and - @{text "b"}. For atoms with different type than the permutation, we - define @{text "\ \ c \ c"}. - - With the separate atom types and the list representation of permutations it - is impossible in systems like Isabelle/HOL to state an ``ill-sorted'' - permutation, since the type system excludes lists containing atoms of - different type. However, a disadvantage is that whenever we need to - generalise induction hypotheses by quantifying over permutations, we have to - build quantifications like - - @{text [display,indent=10] "\\\<^isub>1 \ \\\<^isub>n. \"} - - \noindent - where the @{text "\\<^isub>i"} are of type @{text "(\\<^isub>i \ \\<^isub>i) list"}. - The reason is that the permutation operation behaves differently for - every @{text "\\<^isub>i"} and the type system does not allow use to have a - single quantification to stand for all permutations. Similarly, the - notion of support - - @{text [display,indent=10] "supp _ :: \ \ \ set"} - - \noindent - which we will define later, cannot be - used to express the support of an object over \emph{all} atoms. The reason - is that support can behave differently for each @{text - "\\<^isub>i"}. This problem is annoying, because if we need to know in - a statement that an object, say @{text "x"}, is finitely supported we end up - with having to state premises of the form - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}l} - @{text "finite ((supp x) :: \\<^isub>1 set) , \, finite ((supp x) :: \\<^isub>n set)"} - \end{tabular}\hfill\numbered{fssequence} - \end{isabelle} - - \noindent - Because of these disadvantages, we will use in this paper a single unified atom type to - represent atoms of different sorts. Consequently, we have to deal with the - case that a swapping of two atoms is ill-sorted: we cannot rely anymore on - the type systems to exclude them. - - We also will not represent permutations as lists of pairs of atoms (as done in - \cite{Urban08}). Although an - advantage of this representation is that the basic operations on - permutations are already defined in Isabelle's list library: composition of - two permutations (written @{text "_ @ _"}) is just list append, and - inversion of a permutation (written @{text "_\<^sup>-\<^sup>1"}) is just - list reversal, and another advantage is that there is a well-understood - induction principle for lists, a disadvantage is that permutations - do not have unique representations as lists. We have to explicitly identify - them according to the relation + collection of sorted atoms. The nominal logic work has been starting + point for a number of formalisations, most notable Norrish \cite{norrish04} + in HOL4, Aydemir et al \cite{AydemirBohannonWeirich07} in Coq and our own + work in Isabelle/HOL. - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}l} - @{text "\\<^isub>1 \ \\<^isub>2 \ \a. \\<^isub>1 \ a = \\<^isub>2 \ a"} - \end{tabular}\hfill\numbered{permequ} - \end{isabelle} - - \noindent - This is a problem when lifting the permutation operation to other types, for - example sets, functions and so on. For this we need to ensure that every definition - is well-behaved in the sense that it satisfies some - \emph{permutation properties}. In the list representation we need - to state these properties as follows: - - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}} - i) & @{text "[] \ x = x"}\\ - ii) & @{text "(\\<^isub>1 @ \\<^isub>2) \ x = \\<^isub>1 \ (\\<^isub>2 \ x)"}\\ - iii) & if @{text "\\<^isub>1 \ \\<^isub>2"} then @{text "\\<^isub>1 \ x = \\<^isub>2 \ x"} - \end{tabular}\hfill\numbered{permprops} - \end{isabelle} - - \noindent - where the last clause explicitly states that the permutation operation has - to produce the same result for related permutations. Moreover, - ``permutations-as-lists'' do not satisfy the group properties. This means by - using this representation we will not be able to reuse the extensive - reasoning infrastructure in Isabelle about groups. Because of this, we will represent - in this paper permutations as functions from atoms to atoms. This representation - is unique and satisfies the laws of non-commutative groups. - Using a single atom type to represent atoms of different sorts and representing permutations as functions are not new ideas; see \cite{GunterOsbornPopescu09} \footnote{function rep.} The main contribution @@ -199,6 +79,24 @@ section {* Sorted Atoms and Sort-Respecting Permutations *} text {* + The most basic notion in this work is a + sort-respecting permutation operation defined over a countably infinite + collection of sorted atoms. The atoms are used for representing variable names + that might be bound or free. Multiple sorts are necessary for being able to + represent different kinds of variables. For example, in the language Mini-ML + there are bound term variables in lambda abstractions and bound type variables in + type schemes. In order to be able to separate them, each kind of variables needs to be + represented by a different sort of atoms. + + + The existing nominal logic work usually leaves implicit the sorting + information for atoms and as far as we know leaves out a description of how + sorts are represented. In our formalisation, we therefore have to make a + design decision about how to implement sorted atoms and sort-respecting + permutations. One possibility, which we described in \cite{Urban08}, is to + have separate types for the different + kinds of atoms, say types @{text "\\<^isub>1,\,\\<^isub>n"}. + In the nominal logic work of Pitts, binders and bound variables are represented by \emph{atoms}. As stated above, we need to have different \emph{sorts} of atoms to be able to bind different kinds of variables. A @@ -314,7 +212,7 @@ @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm} @{thm plus_perm_def[where p="\\<^isub>1" and q="\\<^isub>2", THEN eq_reflection]} \hspace{4mm} @{thm uminus_perm_def[where p="\", THEN eq_reflection]} \hspace{4mm} - @{thm diff_def[where a="\\<^isub>1" and b="\\<^isub>2"]} + @{thm minus_perm_def[where ?p1.0="\\<^isub>1" and ?p2.0="\\<^isub>2"]} \end{tabular} \end{isabelle} @@ -1202,184 +1100,123 @@ *} -section {* Multi-Sorted Concrete Atoms *} - -(*<*) -datatype ty = TVar string | Fun ty ty ("_ \ _") -(*>*) - -text {* - The formalisation presented so far allows us to streamline proofs and reduce - the amount of custom ML-code in the existing implementation of Nominal - Isabelle. In this section we describe a mechanism that extends the - capabilities of Nominal Isabelle. This mechanism is about variables with - additional information, for example typing constraints. - While we leave a detailed treatment of binders and binding of variables for a - later paper, we will have a look here at how such variables can be - represented by concrete atoms. - - In the previous section we considered concrete atoms that can be used in - simple binders like \emph{@{text "\x. x"}}. Such concrete atoms do - not carry any information beyond their identities---comparing for equality - is really the only way to analyse ordinary concrete atoms. - However, in ``Church-style'' lambda-terms \cite{Church40} and in the terms - underlying HOL-systems \cite{PittsHOL4} binders and bound variables have a - more complicated structure. For example in the ``Church-style'' lambda-term - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}l} - @{text "\x\<^isub>\. x\<^isub>\ x\<^isub>\"} - \end{tabular}\hfill\numbered{church} - \end{isabelle} - - \noindent - both variables and binders include typing information indicated by @{text \} - and @{text \}. In this setting, we treat @{text "x\<^isub>\"} and @{text - "x\<^isub>\"} as distinct variables (assuming @{term "\\\"}) so that the - variable @{text "x\<^isub>\"} is bound by the lambda-abstraction, but not - @{text "x\<^isub>\"}. - - To illustrate how we can deal with this phenomenon, let us represent object - types like @{text \} and @{text \} by the datatype - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}l} - \isacommand{datatype}~~@{text "ty = TVar string | ty \ ty"} - \end{tabular} - \end{isabelle} - - \noindent - If we attempt to encode a variable naively as a pair of a @{text name} and a @{text ty}, we have the - problem that a swapping, say @{term "(x \ y)"}, applied to the pair @{text "((x, \), (x, \))"} - will always permute \emph{both} occurrences of @{text x}, even if the types - @{text "\"} and @{text "\"} are different. This is unwanted, because it will - eventually mean that both occurrences of @{text x} will become bound by a - corresponding binder. - - Another attempt might be to define variables as an instance of the concrete - atom type class, where a @{text ty} is somehow encoded within each variable. - Remember we defined atoms as the datatype: -*} - - datatype atom\\ = Atom\\ string nat - -text {* - \noindent - Considering our method of defining concrete atom types, the usage of a string - for the sort of atoms seems a natural choice. However, none of the results so - far depend on this choice and we are free to change it. - One possibility is to encode types or any other information by making the sort - argument parametric as follows: -*} - - datatype 'a \atom\\\ = \Atom\\ 'a nat - -text {* - \noindent - The problem with this possibility is that we are then back in the old - situation where our permutation operation is parametric in two types and - this would require to work around Isabelle/HOL's restriction on type - classes. Fortunately, encoding the types in a separate parameter is not - necessary for what we want to achieve, as we only have to know when two - types are equal or not. The solution is to use a different sort for each - object type. Then we can use the fact that permutations respect \emph{sorts} to - ensure that permutations also respect \emph{object types}. In order to do - this, we must define an injective function @{text "sort_ty"} mapping from - object types to sorts. For defining functions like @{text "sort_ty"}, it is - more convenient to use a tree datatype for sorts. Therefore we define -*} - - datatype sort = Sort string "(sort list)" - datatype atom\\\\ = Atom\\\\ sort nat - -text {* - \noindent - With this definition, - the sorts we considered so far can be encoded just as \mbox{@{text "Sort s []"}}. - The point, however, is that we can now define the function @{text sort_ty} simply as - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \begin{tabular}{@ {}l} - @{text "sort_ty (TVar s) = Sort ''TVar'' [Sort s []]"}\\ - @{text "sort_ty (\\<^isub>1 \ \\<^isub>2) = Sort ''Fun'' [sort_ty \\<^isub>1, sort_ty \\<^isub>2]"} - \end{tabular}\hfill\numbered{sortty} - \end{isabelle} - - \noindent - which can easily be shown to be injective. - - Having settled on what the sorts should be for ``Church-like'' atoms, we have to - give a subtype definition for concrete atoms. Previously we identified a subtype consisting - of atoms of only one specified sort. This must be generalised to all sorts the - function @{text "sort_ty"} might produce, i.e.~the - range of @{text "sort_ty"}. Therefore we define - - \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - \isacommand{typedef}\ \ @{text var} = @{term "{a. sort a : range sort_ty}"} - \end{isabelle} - - \noindent - This command gives us again injective representation and abstraction - functions. We will write them also as \mbox{@{text "\_\ :: var \ atom"}} and - @{text "\_\ :: atom \ var"}, respectively. - - We can define the permutation operation for @{text var} as @{thm - permute_var_def[where p="\", THEN eq_reflection, no_vars]} and the - injective function to type @{typ atom} as @{thm atom_var_def[THEN - eq_reflection, no_vars]}. Finally, we can define a constructor function that - makes a @{text var} from a variable name and an object type: - - @{thm [display,indent=10] Var_def[where t="\", THEN eq_reflection, no_vars]} - - \noindent - With these definitions we can verify all the properties for concrete atom - types except Property \ref{atomprops}@{text ".iii)"}, which requires every - atom to have the same sort. This last property is clearly not true for type - @{text "var"}. - This fact is slightly unfortunate since this - property allowed us to use the type-checker in order to shield the user from - all sort-constraints. But this failure is expected here, because we cannot - burden the type-system of Isabelle/HOL with the task of deciding when two - object types are equal. This means we sometimes need to explicitly state sort - constraints or explicitly discharge them, but as we will see in the lemma - below this seems a natural price to pay in these circumstances. - - To sum up this section, the encoding of type-information into atoms allows us - to form the swapping @{term "(Var x \ \ Var y \)"} and to prove the following - lemma -*} - - lemma - assumes asm: "\ \ \" - shows "(Var x \ \ Var y \) \ (Var x \, Var x \) = (Var y \, Var x \)" - using asm by simp - -text {* - \noindent - As we expect, the atom @{term "Var x \"} is left unchanged by the - swapping. With this we can faithfully represent bindings in languages - involving ``Church-style'' terms and bindings as shown in \eqref{church}. We - expect that the creation of such atoms can be easily automated so that the - user just needs to specify \isacommand{atom\_decl}~~@{text "var (ty)"} - where the argument, or arguments, are datatypes for which we can automatically - define an injective function like @{text "sort_ty"} (see \eqref{sortty}). - Our hope is that with this approach Benzmueller and Paulson can make - headway with formalising their results - about simple type theory \cite{PaulsonBenzmueller}. - Because of its limitations, they did not attempt this with the old version - of Nominal Isabelle. We also hope we can make progress with formalisations of - HOL-based languages. -*} section {* Related Work *} text {* Add here comparison with old work. - The main point is that the above reasoning blends smoothly with the reasoning infrastructure of Isabelle/HOL; no custom ML-code is necessary and a single type class suffices. + + With this + design one can represent permutations as lists of pairs of atoms and the + operation of applying a permutation to an object as the function + + + @{text [display,indent=10] "_ \ _ :: (\ \ \) list \ \ \ \"} + + \noindent + where @{text "\"} stands for a type of atoms and @{text "\"} for the type + of the objects on which the permutation acts. For atoms + the permutation operation is defined over the length of lists as follows + + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + \begin{tabular}{@ {}r@ {\hspace{2mm}}c@ {\hspace{2mm}}l} + @{text "[] \ c"} & @{text "="} & @{text c}\\ + @{text "(a b)::\ \ c"} & @{text "="} & + $\begin{cases} @{text a} & \textrm{if}~@{text "\ \ c = b"}\\ + @{text b} & \textrm{if}~@{text "\ \ c = a"}\\ + @{text "\ \ c"} & \textrm{otherwise}\end{cases}$ + \end{tabular}\hfill\numbered{atomperm} + \end{isabelle} + + \noindent + where we write @{text "(a b)"} for a swapping of atoms @{text "a"} and + @{text "b"}. For atoms with different type than the permutation, we + define @{text "\ \ c \ c"}. + + With the separate atom types and the list representation of permutations it + is impossible in systems like Isabelle/HOL to state an ``ill-sorted'' + permutation, since the type system excludes lists containing atoms of + different type. However, a disadvantage is that whenever we need to + generalise induction hypotheses by quantifying over permutations, we have to + build quantifications like + + @{text [display,indent=10] "\\\<^isub>1 \ \\\<^isub>n. \"} + + \noindent + where the @{text "\\<^isub>i"} are of type @{text "(\\<^isub>i \ \\<^isub>i) list"}. + The reason is that the permutation operation behaves differently for + every @{text "\\<^isub>i"} and the type system does not allow use to have a + single quantification to stand for all permutations. Similarly, the + notion of support + + @{text [display,indent=10] "supp _ :: \ \ \ set"} + + \noindent + which we will define later, cannot be + used to express the support of an object over \emph{all} atoms. The reason + is that support can behave differently for each @{text + "\\<^isub>i"}. This problem is annoying, because if we need to know in + a statement that an object, say @{text "x"}, is finitely supported we end up + with having to state premises of the form + + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + \begin{tabular}{@ {}l} + @{text "finite ((supp x) :: \\<^isub>1 set) , \, finite ((supp x) :: \\<^isub>n set)"} + \end{tabular}\hfill\numbered{fssequence} + \end{isabelle} + + \noindent + Because of these disadvantages, we will use in this paper a single unified atom type to + represent atoms of different sorts. Consequently, we have to deal with the + case that a swapping of two atoms is ill-sorted: we cannot rely anymore on + the type systems to exclude them. + + We also will not represent permutations as lists of pairs of atoms (as done in + \cite{Urban08}). Although an + advantage of this representation is that the basic operations on + permutations are already defined in Isabelle's list library: composition of + two permutations (written @{text "_ @ _"}) is just list append, and + inversion of a permutation (written @{text "_\<^sup>-\<^sup>1"}) is just + list reversal, and another advantage is that there is a well-understood + induction principle for lists, a disadvantage is that permutations + do not have unique representations as lists. We have to explicitly identify + them according to the relation + + + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + \begin{tabular}{@ {}l} + @{text "\\<^isub>1 \ \\<^isub>2 \ \a. \\<^isub>1 \ a = \\<^isub>2 \ a"} + \end{tabular}\hfill\numbered{permequ} + \end{isabelle} + + \noindent + This is a problem when lifting the permutation operation to other types, for + example sets, functions and so on. For this we need to ensure that every definition + is well-behaved in the sense that it satisfies some + \emph{permutation properties}. In the list representation we need + to state these properties as follows: + + + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + \begin{tabular}{@ {}r@ {\hspace{4mm}}p{10cm}} + i) & @{text "[] \ x = x"}\\ + ii) & @{text "(\\<^isub>1 @ \\<^isub>2) \ x = \\<^isub>1 \ (\\<^isub>2 \ x)"}\\ + iii) & if @{text "\\<^isub>1 \ \\<^isub>2"} then @{text "\\<^isub>1 \ x = \\<^isub>2 \ x"} + \end{tabular}\hfill\numbered{permprops} + \end{isabelle} + + \noindent + where the last clause explicitly states that the permutation operation has + to produce the same result for related permutations. Moreover, + ``permutations-as-lists'' do not satisfy the group properties. This means by + using this representation we will not be able to reuse the extensive + reasoning infrastructure in Isabelle about groups. Because of this, we will represent + in this paper permutations as functions from atoms to atoms. This representation + is unique and satisfies the laws of non-commutative groups. *} diff -r ff22039df778 -r 7fd879774d9b Pearl-jv/ROOT.ML --- a/Pearl-jv/ROOT.ML Wed Mar 02 12:48:00 2011 +0900 +++ b/Pearl-jv/ROOT.ML Wed Mar 02 12:49:01 2011 +0900 @@ -1,5 +1,4 @@ no_document use_thys ["../Nominal/Nominal2_Base", - "../Nominal/Nominal2_Eqvt", "../Nominal/Atoms", "../Nominal/Nominal2_Abs", "LaTeXsugar"]; diff -r ff22039df778 -r 7fd879774d9b Pearl-jv/document/root.bib --- a/Pearl-jv/document/root.bib Wed Mar 02 12:48:00 2011 +0900 +++ b/Pearl-jv/document/root.bib Wed Mar 02 12:49:01 2011 +0900 @@ -8,6 +8,17 @@ year = "2008" } +@InProceedings{norrish04, + author = {M.~Norrish}, + title = {{R}ecursive {F}unction {D}efinition for {T}ypes with {B}inders}, + booktitle = {Proc.~of the 17th International Conference Theorem Proving in + Higher Order Logics (TPHOLs)}, + pages = {241--256}, + year = {2004}, + volume = {3223}, + series = {LNCS} +} + @InProceedings{GunterOsbornPopescu09, author = {E.L.~Gunter and C.J.~Osborn and A.~Popescu}, title = {{T}heory {S}upport for {W}eak {H}igher {O}rder {A}bstract {S}yntax in @@ -19,6 +30,16 @@ series = {ENTCS} } +@InProceedings{AydemirBohannonWeirich07, + author = {B.~Aydemir and A.~Bohannon and S.~Weihrich}, + title = {{N}ominal {R}easoning {T}echniques in {C}oq ({E}xtended {A}bstract)}, + booktitle = {Proc.~of the 1st International Workshop on Logical Frameworks and Meta-Languages: + Theory and Practice (LFMTP)}, + pages = {69--77}, + year = {2007}, + series = {ENTCS} +} + @Unpublished{SatoPollack10, author = {M.~Sato and R.~Pollack}, title = {{E}xternal and {I}nternal {S}yntax of the {L}ambda-{C}alculus}, diff -r ff22039df778 -r 7fd879774d9b Pearl-jv/document/root.tex --- a/Pearl-jv/document/root.tex Wed Mar 02 12:48:00 2011 +0900 +++ b/Pearl-jv/document/root.tex Wed Mar 02 12:49:01 2011 +0900 @@ -36,12 +36,13 @@ Pitts et al introduced a beautiful theory about names and binding based on the notions of atoms, permutations and support. The engineering challenge is to smoothly adapt this theory to a theorem prover environment, in our case -Isabelle/HOL. We present a formalisation of this work that is based on a -unified atom type and that represents permutations by bijective functions from -atoms to atoms. Interestingly, we allow swappings, which are permutations -build from two atoms, to be ill-sorted. Furthermore we extend the nominal -logic work with names that carry additional information and with a -formalisation of abstractions that bind finite sets of names. +Isabelle/HOL. For this we have to formulate the theory so that it is +compatible with choice principles, which the work by Pitts is not. We +present a formalisation of this work that is based on a unified atom type +and that represents permutations by bijective functions from atoms to atoms. +Interestingly, we allow swappings, which are permutations build from two +atoms, to be ill-sorted. We also describe a formalisation of an +abstraction operator that binds sets of names. \end{abstract} % generated text of all theories diff -r ff22039df778 -r 7fd879774d9b Pearl/Paper.thy --- a/Pearl/Paper.thy Wed Mar 02 12:48:00 2011 +0900 +++ b/Pearl/Paper.thy Wed Mar 02 12:49:01 2011 +0900 @@ -1,7 +1,6 @@ (*<*) theory Paper imports "../Nominal/Nominal2_Base" - "../Nominal/Nominal2_Eqvt" "../Nominal/Atoms" "LaTeXsugar" begin @@ -346,7 +345,7 @@ @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm} @{thm plus_perm_def[where p="\\<^isub>1" and q="\\<^isub>2", THEN eq_reflection]} \hspace{4mm} @{thm uminus_perm_def[where p="\", THEN eq_reflection]} \hspace{4mm} - @{thm diff_def[where a="\\<^isub>1" and b="\\<^isub>2"]} + @{thm minus_perm_def[where ?p1.0="\\<^isub>1" and ?p2.0="\\<^isub>2"]} \end{tabular} \end{isabelle} diff -r ff22039df778 -r 7fd879774d9b Pearl/ROOT.ML --- a/Pearl/ROOT.ML Wed Mar 02 12:48:00 2011 +0900 +++ b/Pearl/ROOT.ML Wed Mar 02 12:49:01 2011 +0900 @@ -1,5 +1,4 @@ no_document use_thys ["../Nominal/Nominal2_Base", - "../Nominal/Nominal2_Eqvt", "../Nominal/Atoms", "LaTeXsugar"];