# HG changeset patch # User Christian Urban # Date 1289752487 0 # Node ID 8193bbaa07feb0f1bda4a7ff3036136b1d7fd0cd # Parent 41137dc935ff07e84a0a7d0e23c8bf9a07bd659c merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy diff -r 41137dc935ff -r 8193bbaa07fe Nominal-General/Atoms.thy --- a/Nominal-General/Atoms.thy Sun Nov 14 12:09:14 2010 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,222 +0,0 @@ -(* Title: Atoms - Authors: Brian Huffman, Christian Urban - - Instantiations of concrete atoms -*) -theory Atoms -imports Nominal2_Base -uses "~~/src/Tools/subtyping.ML" -begin - - - -section {* @{const nat_of} is an example of a function - without finite support *} - - -lemma not_fresh_nat_of: - shows "\ a \ nat_of" -unfolding fresh_def supp_def -proof (clarsimp) - assume "finite {b. (a \ b) \ nat_of \ nat_of}" - hence "finite ({a} \ {b. (a \ b) \ nat_of \ nat_of})" - by simp - then obtain b where - b1: "b \ a" and - b2: "sort_of b = sort_of a" and - b3: "(a \ b) \ nat_of = nat_of" - by (rule obtain_atom) auto - have "nat_of a = (a \ b) \ (nat_of a)" by (simp add: permute_nat_def) - also have "\ = ((a \ b) \ nat_of) ((a \ b) \ a)" by (simp add: permute_fun_app_eq) - also have "\ = nat_of ((a \ b) \ a)" using b3 by simp - also have "\ = nat_of b" using b2 by simp - finally have "nat_of a = nat_of b" by simp - with b2 have "a = b" by (simp add: atom_components_eq_iff) - with b1 show "False" by simp -qed - -lemma supp_nat_of: - shows "supp nat_of = UNIV" - using not_fresh_nat_of [unfolded fresh_def] by auto - - -section {* Manual instantiation of class @{text at}. *} - -typedef (open) name = "{a. sort_of a = Sort ''name'' []}" -by (rule exists_eq_simple_sort) - -instantiation name :: at -begin - -definition - "p \ a = Abs_name (p \ Rep_name a)" - -definition - "atom a = Rep_name a" - -instance -apply (rule at_class) -apply (rule type_definition_name) -apply (rule atom_name_def) -apply (rule permute_name_def) -done - -end - -lemma sort_of_atom_name: - shows "sort_of (atom (a::name)) = Sort ''name'' []" - unfolding atom_name_def using Rep_name by simp - -text {* Custom syntax for concrete atoms of type at *} - -term "a:::name" - -text {* - a:::name stands for (atom a) with a being of concrete atom - type name. The above lemma can therefore also be stated as - - "sort_of (a:::name) = Sort ''name'' []" - - This does not work for multi-sorted atoms. -*} - - -section {* Automatic instantiation of class @{text at}. *} - -atom_decl name2 - -lemma sort_of_atom_name2: - "sort_of (atom (a::name2)) = Sort ''Atoms.name2'' []" -unfolding atom_name2_def -using Rep_name2 -by simp - -text {* example swappings *} -lemma - fixes a b::"atom" - assumes "sort_of a = sort_of b" - shows "(a \ b) \ (a, b) = (b, a)" -using assms -by simp - -lemma - fixes a b::"name2" - shows "(a \ b) \ (a, b) = (b, a)" -by simp - -section {* An example for multiple-sort atoms *} - -datatype ty = - TVar string -| Fun ty ty ("_ \ _") - -primrec - sort_of_ty::"ty \ atom_sort" -where - "sort_of_ty (TVar s) = Sort ''TVar'' [Sort s []]" -| "sort_of_ty (Fun ty1 ty2) = Sort ''Fun'' [sort_of_ty ty1, sort_of_ty ty2]" - -lemma sort_of_ty_eq_iff: - shows "sort_of_ty x = sort_of_ty y \ x = y" -apply(induct x arbitrary: y) -apply(case_tac [!] y) -apply(simp_all) -done - -declare sort_of_ty.simps [simp del] - -typedef (open) var = "{a. sort_of a \ range sort_of_ty}" - by (rule_tac x="Atom (sort_of_ty x) y" in exI, simp) - -instantiation var :: at_base -begin - -definition - "p \ a = Abs_var (p \ Rep_var a)" - -definition - "atom a = Rep_var a" - -instance -apply (rule at_base_class) -apply (rule type_definition_var) -apply (rule atom_var_def) -apply (rule permute_var_def) -done - -end - -text {* Constructor for variables. *} - -definition - Var :: "nat \ ty \ var" -where - "Var x t = Abs_var (Atom (sort_of_ty t) x)" - -lemma Var_eq_iff [simp]: - shows "Var x s = Var y t \ x = y \ s = t" - unfolding Var_def - by (auto simp add: Abs_var_inject sort_of_ty_eq_iff) - -lemma sort_of_atom_var [simp]: - "sort_of (atom (Var n ty)) = sort_of_ty ty" - unfolding atom_var_def Var_def - by (simp add: Abs_var_inverse) - -lemma - assumes "\ \ \" - shows "(Var x \ \ Var y \) \ (Var x \, Var x \) = (Var y \, Var x \)" - using assms by simp - -text {* Projecting out the type component of a variable. *} - -definition - ty_of :: "var \ ty" -where - "ty_of x = inv sort_of_ty (sort_of (atom x))" - -text {* - Functions @{term Var}/@{term ty_of} satisfy many of the same - properties as @{term Atom}/@{term sort_of}. -*} - -lemma ty_of_Var [simp]: - shows "ty_of (Var x t) = t" - unfolding ty_of_def - unfolding sort_of_atom_var - apply (rule inv_f_f) - apply (simp add: inj_on_def sort_of_ty_eq_iff) - done - -lemma ty_of_permute [simp]: - shows "ty_of (p \ x) = ty_of x" - unfolding ty_of_def - unfolding atom_eqvt [symmetric] - by simp - - -section {* Tests with subtyping and automatic coercions *} - -setup Subtyping.setup - -atom_decl var1 -atom_decl var2 - -declare [[coercion "atom::var1\atom"]] - -declare [[coercion "atom::var2\atom"]] - -lemma - fixes a::"var1" and b::"var2" - shows "a \ t \ b \ t" -oops - -(* does not yet work: it needs image as - coercion map *) - -lemma - fixes as::"var1 set" - shows "atom ` as \* t" -oops - -end diff -r 41137dc935ff -r 8193bbaa07fe Nominal-General/Nominal2_Base.thy --- a/Nominal-General/Nominal2_Base.thy Sun Nov 14 12:09:14 2010 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2024 +0,0 @@ -(* Title: Nominal2_Base - Authors: Brian Huffman, Christian Urban - - Basic definitions and lemma infrastructure for - Nominal Isabelle. -*) -theory Nominal2_Base -imports Main Infinite_Set - "~~/src/HOL/Quotient_Examples/FSet" -uses ("nominal_library.ML") - ("nominal_atoms.ML") -begin - -section {* Atoms and Sorts *} - -text {* A simple implementation for atom_sorts is strings. *} -(* types atom_sort = string *) - -text {* To deal with Church-like binding we use trees of - strings as sorts. *} - -datatype atom_sort = Sort "string" "atom_sort list" - -datatype atom = Atom atom_sort nat - - -text {* Basic projection function. *} - -primrec - sort_of :: "atom \ atom_sort" -where - "sort_of (Atom s i) = s" - -primrec - nat_of :: "atom \ nat" -where - "nat_of (Atom s n) = n" - - -text {* There are infinitely many atoms of each sort. *} -lemma INFM_sort_of_eq: - shows "INFM a. sort_of a = s" -proof - - have "INFM i. sort_of (Atom s i) = s" by simp - moreover have "inj (Atom s)" by (simp add: inj_on_def) - ultimately show "INFM a. sort_of a = s" by (rule INFM_inj) -qed - -lemma infinite_sort_of_eq: - shows "infinite {a. sort_of a = s}" - using INFM_sort_of_eq unfolding INFM_iff_infinite . - -lemma atom_infinite [simp]: - shows "infinite (UNIV :: atom set)" - using subset_UNIV infinite_sort_of_eq - by (rule infinite_super) - -lemma obtain_atom: - fixes X :: "atom set" - assumes X: "finite X" - obtains a where "a \ X" "sort_of a = s" -proof - - from X have "MOST a. a \ X" - unfolding MOST_iff_cofinite by simp - with INFM_sort_of_eq - have "INFM a. sort_of a = s \ a \ X" - by (rule INFM_conjI) - then obtain a where "a \ X" "sort_of a = s" - by (auto elim: INFM_E) - then show ?thesis .. -qed - -lemma atom_components_eq_iff: - fixes a b :: atom - 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 = - "{f. bij f \ finite {a. f a \ a} \ (\a. sort_of (f a) = sort_of a)}" -proof - show "id \ ?perm" by simp -qed - -lemma permI: - assumes "bij f" and "MOST x. f x = x" and "\a. sort_of (f a) = sort_of a" - shows "f \ perm" - using assms unfolding perm_def MOST_iff_cofinite by simp - -lemma perm_is_bij: "f \ perm \ bij f" - unfolding perm_def by simp - -lemma perm_is_finite: "f \ perm \ finite {a. f a \ a}" - unfolding perm_def by simp - -lemma perm_is_sort_respecting: "f \ perm \ sort_of (f a) = sort_of a" - unfolding perm_def by simp - -lemma perm_MOST: "f \ perm \ MOST x. f x = x" - unfolding perm_def MOST_iff_cofinite by simp - -lemma perm_id: "id \ perm" - unfolding perm_def by simp - -lemma perm_comp: - assumes f: "f \ perm" and g: "g \ perm" - shows "(f \ g) \ perm" -apply (rule permI) -apply (rule bij_comp) -apply (rule perm_is_bij [OF g]) -apply (rule perm_is_bij [OF f]) -apply (rule MOST_rev_mp [OF perm_MOST [OF g]]) -apply (rule MOST_rev_mp [OF perm_MOST [OF f]]) -apply (simp) -apply (simp add: perm_is_sort_respecting [OF f]) -apply (simp add: perm_is_sort_respecting [OF g]) -done - -lemma perm_inv: - assumes f: "f \ perm" - shows "(inv f) \ perm" -apply (rule permI) -apply (rule bij_imp_bij_inv) -apply (rule perm_is_bij [OF f]) -apply (rule MOST_mono [OF perm_MOST [OF f]]) -apply (erule subst, rule inv_f_f) -apply (rule bij_is_inj [OF perm_is_bij [OF f]]) -apply (rule perm_is_sort_respecting [OF f, THEN sym, THEN trans]) -apply (simp add: surj_f_inv_f [OF bij_is_surj [OF perm_is_bij [OF f]]]) -done - -lemma bij_Rep_perm: "bij (Rep_perm p)" - using Rep_perm [of p] unfolding perm_def by simp - -lemma finite_Rep_perm: "finite {a. Rep_perm p a \ a}" - using Rep_perm [of p] unfolding perm_def by simp - -lemma sort_of_Rep_perm: "sort_of (Rep_perm p a) = sort_of a" - using Rep_perm [of p] unfolding perm_def by simp - -lemma Rep_perm_ext: - "Rep_perm p1 = Rep_perm p2 \ p1 = p2" - by (simp add: fun_eq_iff Rep_perm_inject [symmetric]) - -instance perm :: size .. - -subsection {* Permutations form a group *} - -instantiation perm :: group_add -begin - -definition - "0 = Abs_perm id" - -definition - "- p = Abs_perm (inv (Rep_perm p))" - -definition - "p + q = Abs_perm (Rep_perm p \ Rep_perm q)" - -definition - "(p1::perm) - p2 = p1 + - p2" - -lemma Rep_perm_0: "Rep_perm 0 = id" - unfolding zero_perm_def - by (simp add: Abs_perm_inverse perm_id) - -lemma Rep_perm_add: - "Rep_perm (p1 + p2) = Rep_perm p1 \ Rep_perm p2" - unfolding plus_perm_def - by (simp add: Abs_perm_inverse perm_comp Rep_perm) - -lemma Rep_perm_uminus: - "Rep_perm (- p) = inv (Rep_perm p)" - unfolding uminus_perm_def - by (simp add: Abs_perm_inverse perm_inv Rep_perm) - -instance -apply default -unfolding Rep_perm_inject [symmetric] -unfolding minus_perm_def -unfolding Rep_perm_add -unfolding Rep_perm_uminus -unfolding Rep_perm_0 -by (simp_all add: o_assoc inv_o_cancel [OF bij_is_inj [OF bij_Rep_perm]]) - -end - - -section {* Implementation of swappings *} - -definition - swap :: "atom \ atom \ perm" ("'(_ \ _')") -where - "(a \ b) = - Abs_perm (if sort_of a = sort_of b - then (\c. if a = c then b else if b = c then a else c) - else id)" - -lemma Rep_perm_swap: - "Rep_perm (a \ b) = - (if sort_of a = sort_of b - then (\c. if a = c then b else if b = c then a else c) - else id)" -unfolding swap_def -apply (rule Abs_perm_inverse) -apply (rule permI) -apply (auto simp add: bij_def inj_on_def surj_def)[1] -apply (rule MOST_rev_mp [OF MOST_neq(1) [of a]]) -apply (rule MOST_rev_mp [OF MOST_neq(1) [of b]]) -apply (simp) -apply (simp) -done - -lemmas Rep_perm_simps = - Rep_perm_0 - Rep_perm_add - Rep_perm_uminus - Rep_perm_swap - -lemma swap_different_sorts [simp]: - "sort_of a \ sort_of b \ (a \ b) = 0" - by (rule Rep_perm_ext) (simp add: Rep_perm_simps) - -lemma swap_cancel: - "(a \ b) + (a \ b) = 0" - by (rule Rep_perm_ext) - (simp add: Rep_perm_simps fun_eq_iff) - -lemma swap_self [simp]: - "(a \ a) = 0" - by (rule Rep_perm_ext, simp add: Rep_perm_simps fun_eq_iff) - -lemma minus_swap [simp]: - "- (a \ b) = (a \ b)" - by (rule minus_unique [OF swap_cancel]) - -lemma swap_commute: - "(a \ b) = (b \ a)" - by (rule Rep_perm_ext) - (simp add: Rep_perm_swap fun_eq_iff) - -lemma swap_triple: - assumes "a \ b" and "c \ b" - assumes "sort_of a = sort_of b" "sort_of b = sort_of c" - shows "(a \ c) + (b \ c) + (a \ c) = (a \ b)" - using assms - by (rule_tac Rep_perm_ext) - (auto simp add: Rep_perm_simps fun_eq_iff) - - -section {* Permutation Types *} - -text {* - Infix syntax for @{text permute} has higher precedence than - addition, but lower than unary minus. -*} - -class pt = - fixes permute :: "perm \ 'a \ 'a" ("_ \ _" [76, 75] 75) - assumes permute_zero [simp]: "0 \ x = x" - assumes permute_plus [simp]: "(p + q) \ x = p \ (q \ x)" -begin - -lemma permute_diff [simp]: - shows "(p - q) \ x = p \ - q \ x" - unfolding diff_minus by simp - -lemma permute_minus_cancel [simp]: - shows "p \ - p \ x = x" - and "- p \ p \ x = x" - unfolding permute_plus [symmetric] by simp_all - -lemma permute_swap_cancel [simp]: - shows "(a \ b) \ (a \ b) \ x = x" - unfolding permute_plus [symmetric] - by (simp add: swap_cancel) - -lemma permute_swap_cancel2 [simp]: - shows "(a \ b) \ (b \ a) \ x = x" - unfolding permute_plus [symmetric] - by (simp add: swap_commute) - -lemma inj_permute [simp]: - shows "inj (permute p)" - by (rule inj_on_inverseI) - (rule permute_minus_cancel) - -lemma surj_permute [simp]: - shows "surj (permute p)" - by (rule surjI, rule permute_minus_cancel) - -lemma bij_permute [simp]: - shows "bij (permute p)" - by (rule bijI [OF inj_permute surj_permute]) - -lemma inv_permute: - shows "inv (permute p) = permute (- p)" - by (rule inv_equality) (simp_all) - -lemma permute_minus: - shows "permute (- p) = inv (permute p)" - by (simp add: inv_permute) - -lemma permute_eq_iff [simp]: - shows "p \ x = p \ y \ x = y" - by (rule inj_permute [THEN inj_eq]) - -end - -subsection {* Permutations for atoms *} - -instantiation atom :: pt -begin - -definition - "p \ a = (Rep_perm p) a" - -instance -apply(default) -apply(simp_all add: permute_atom_def Rep_perm_simps) -done - -end - -lemma sort_of_permute [simp]: - shows "sort_of (p \ a) = sort_of a" - unfolding permute_atom_def by (rule sort_of_Rep_perm) - -lemma swap_atom: - shows "(a \ b) \ c = - (if sort_of a = sort_of b - then (if c = a then b else if c = b then a else c) else c)" - unfolding permute_atom_def - by (simp add: Rep_perm_swap) - -lemma swap_atom_simps [simp]: - "sort_of a = sort_of b \ (a \ b) \ a = b" - "sort_of a = sort_of b \ (a \ b) \ b = a" - "c \ a \ c \ b \ (a \ b) \ c = c" - unfolding swap_atom by simp_all - -lemma expand_perm_eq: - fixes p q :: "perm" - shows "p = q \ (\a::atom. p \ a = q \ a)" - unfolding permute_atom_def - by (metis Rep_perm_ext ext) - - -subsection {* Permutations for permutations *} - -instantiation perm :: pt -begin - -definition - "p \ q = p + q - p" - -instance -apply default -apply (simp add: permute_perm_def) -apply (simp add: permute_perm_def diff_minus minus_add add_assoc) -done - -end - -lemma permute_self: - shows "p \ p = p" - 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) - -subsection {* Permutations for functions *} - -instantiation "fun" :: (pt, pt) pt -begin - -definition - "p \ f = (\x. p \ (f (- p \ x)))" - -instance -apply default -apply (simp add: permute_fun_def) -apply (simp add: permute_fun_def minus_add) -done - -end - -lemma permute_fun_app_eq: - shows "p \ (f x) = (p \ f) (p \ x)" - unfolding permute_fun_def by simp - - -subsection {* Permutations for booleans *} - -instantiation bool :: pt -begin - -definition "p \ (b::bool) = b" - -instance -apply(default) -apply(simp_all add: permute_bool_def) -done - -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 permute_boolE: - fixes P::"bool" - shows "p \ P \ P" - by (simp add: permute_bool_def) - -lemma permute_boolI: - fixes P::"bool" - shows "P \ p \ P" - by(simp add: permute_bool_def) - -subsection {* Permutations for sets *} - -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 - apply(auto simp add: mem_def) - apply(rule_tac x="- p \ x" in exI) - apply(simp) - done - -lemma permute_set_eq_image: - shows "p \ X = permute p ` X" - unfolding permute_set_eq by auto - -lemma permute_set_eq_vimage: - shows "p \ X = permute (- p) -` X" - unfolding permute_fun_def permute_bool_def - unfolding vimage_def Collect_def mem_def .. - -lemma swap_set_not_in: - assumes a: "a \ S" "b \ S" - shows "(a \ b) \ S = S" - unfolding permute_set_eq - using a by (auto simp add: swap_atom) - -lemma swap_set_in: - assumes a: "a \ S" "b \ S" "sort_of a = sort_of b" - shows "(a \ b) \ S \ S" - unfolding permute_set_eq - using a by (auto simp add: swap_atom) - -lemma mem_permute_iff: - shows "(p \ x) \ (p \ X) \ x \ X" - 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 - by (simp add: permute_fun_def permute_bool_def) - -lemma insert_eqvt: - shows "p \ (insert x A) = insert (p \ x) (p \ A)" - unfolding permute_set_eq_image image_insert .. - - -subsection {* Permutations for units *} - -instantiation unit :: pt -begin - -definition "p \ (u::unit) = u" - -instance -by (default) (simp_all add: permute_unit_def) - -end - - -subsection {* Permutations for products *} - -instantiation prod :: (pt, pt) pt -begin - -primrec - permute_prod -where - Pair_eqvt: "p \ (x, y) = (p \ x, p \ y)" - -instance -by default auto - -end - -subsection {* Permutations for sums *} - -instantiation sum :: (pt, pt) pt -begin - -primrec - permute_sum -where - "p \ (Inl x) = Inl (p \ x)" -| "p \ (Inr y) = Inr (p \ y)" - -instance -by (default) (case_tac [!] x, simp_all) - -end - -subsection {* Permutations for lists *} - -instantiation list :: (pt) pt -begin - -primrec - permute_list -where - "p \ [] = []" -| "p \ (x # xs) = p \ x # p \ xs" - -instance -by (default) (induct_tac [!] x, simp_all) - -end - -lemma set_eqvt: - shows "p \ (set xs) = set (p \ xs)" - by (induct xs) (simp_all add: empty_eqvt insert_eqvt) - -subsection {* Permutations for options *} - -instantiation option :: (pt) pt -begin - -primrec - permute_option -where - "p \ None = None" -| "p \ (Some x) = Some (p \ x)" - -instance -by (default) (induct_tac [!] x, simp_all) - -end - - -subsection {* Permutations for fsets *} - -lemma permute_fset_rsp[quot_respect]: - shows "(op = ===> list_eq ===> list_eq) permute permute" - unfolding fun_rel_def - by (simp add: set_eqvt[symmetric]) - -instantiation fset :: (pt) pt -begin - -quotient_definition - "permute_fset :: perm \ 'a fset \ 'a fset" -is - "permute :: perm \ 'a list \ 'a list" - -instance -proof - fix x :: "'a fset" and p q :: "perm" - show "0 \ x = x" by (descending) (simp) - show "(p + q) \ x = p \ q \ x" by (descending) (simp) -qed - -end - -lemma permute_fset [simp]: - fixes S::"('a::pt) fset" - shows "(p \ {||}) = ({||} ::('a::pt) fset)" - and "(p \ insert_fset x S) = insert_fset (p \ x) (p \ S)" - by (lifting permute_list.simps) - - - -subsection {* Permutations for @{typ char}, @{typ nat}, and @{typ int} *} - -instantiation char :: pt -begin - -definition "p \ (c::char) = c" - -instance -by (default) (simp_all add: permute_char_def) - -end - -instantiation nat :: pt -begin - -definition "p \ (n::nat) = n" - -instance -by (default) (simp_all add: permute_nat_def) - -end - -instantiation int :: pt -begin - -definition "p \ (i::int) = i" - -instance -by (default) (simp_all add: permute_int_def) - -end - - -section {* Pure types *} - -text {* Pure types will have always empty support. *} - -class pure = pt + - assumes permute_pure: "p \ x = x" - -text {* Types @{typ unit} and @{typ bool} are pure. *} - -instance unit :: pure -proof qed (rule permute_unit_def) - -instance bool :: pure -proof qed (rule permute_bool_def) - -text {* Other type constructors preserve purity. *} - -instance "fun" :: (pure, pure) pure -by default (simp add: permute_fun_def permute_pure) - -instance prod :: (pure, pure) pure -by default (induct_tac x, simp add: permute_pure) - -instance sum :: (pure, pure) pure -by default (induct_tac x, simp_all add: permute_pure) - -instance list :: (pure) pure -by default (induct_tac x, simp_all add: permute_pure) - -instance option :: (pure) pure -by default (induct_tac x, simp_all add: permute_pure) - - -subsection {* Types @{typ char}, @{typ nat}, and @{typ int} *} - -instance char :: pure -proof qed (rule permute_char_def) - -instance nat :: pure -proof qed (rule permute_nat_def) - -instance int :: pure -proof qed (rule permute_int_def) - - -subsection {* Supp, Freshness and Supports *} - -context pt -begin - -definition - supp :: "'a \ atom set" -where - "supp x = {a. infinite {b. (a \ b) \ x \ x}}" - -end - -definition - fresh :: "atom \ 'a::pt \ bool" ("_ \ _" [55, 55] 55) -where - "a \ x \ a \ supp x" - -lemma supp_conv_fresh: - shows "supp x = {a. \ a \ x}" - unfolding fresh_def by simp - -lemma swap_rel_trans: - assumes "sort_of a = sort_of b" - assumes "sort_of b = sort_of c" - assumes "(a \ c) \ x = x" - assumes "(b \ c) \ x = x" - shows "(a \ b) \ x = x" -proof (cases) - assume "a = b \ c = b" - with assms show "(a \ b) \ x = x" by auto -next - assume *: "\ (a = b \ c = b)" - have "((a \ c) + (b \ c) + (a \ c)) \ x = x" - using assms by simp - also have "(a \ c) + (b \ c) + (a \ c) = (a \ b)" - using assms * by (simp add: swap_triple) - finally show "(a \ b) \ x = x" . -qed - -lemma swap_fresh_fresh: - assumes a: "a \ x" - and b: "b \ x" - shows "(a \ b) \ x = x" -proof (cases) - assume asm: "sort_of a = sort_of b" - have "finite {c. (a \ c) \ x \ x}" "finite {c. (b \ c) \ x \ x}" - using a b unfolding fresh_def supp_def by simp_all - then have "finite ({c. (a \ c) \ x \ x} \ {c. (b \ c) \ x \ x})" by simp - then obtain c - where "(a \ c) \ x = x" "(b \ c) \ x = x" "sort_of c = sort_of b" - by (rule obtain_atom) (auto) - then show "(a \ b) \ x = x" using asm by (rule_tac swap_rel_trans) (simp_all) -next - assume "sort_of a \ sort_of b" - then show "(a \ b) \ x = x" by simp -qed - - -subsection {* supp and fresh are equivariant *} - -lemma finite_Collect_bij: - assumes a: "bij f" - shows "finite {x. P (f x)} = finite {x. P x}" -by (metis a finite_vimage_iff vimage_Collect_eq) - -lemma fresh_permute_iff: - shows "(p \ a) \ (p \ x) \ a \ x" -proof - - have "(p \ a) \ (p \ x) \ finite {b. (p \ a \ b) \ p \ x \ p \ x}" - unfolding fresh_def supp_def by simp - also have "\ \ finite {b. (p \ a \ p \ b) \ p \ x \ p \ x}" - using bij_permute by (rule finite_Collect_bij[symmetric]) - also have "\ \ finite {b. p \ (a \ b) \ x \ p \ x}" - by (simp only: permute_eqvt [of p] swap_eqvt) - also have "\ \ finite {b. (a \ b) \ x \ x}" - by (simp only: permute_eq_iff) - also have "\ \ a \ x" - unfolding fresh_def supp_def by simp - finally show "(p \ a) \ (p \ x) \ a \ x" . -qed - -lemma fresh_eqvt: - shows "p \ (a \ x) = (p \ a) \ (p \ x)" - unfolding permute_bool_def - by (simp add: fresh_permute_iff) - -lemma supp_eqvt: - fixes p :: "perm" - and x :: "'a::pt" - shows "p \ (supp x) = supp (p \ x)" - unfolding supp_conv_fresh - unfolding Collect_def - unfolding permute_fun_def - by (simp add: Not_eqvt fresh_eqvt) - -subsection {* supports *} - -definition - supports :: "atom set \ 'a::pt \ bool" (infixl "supports" 80) -where - "S supports x \ \a b. (a \ S \ b \ S \ (a \ b) \ x = x)" - -lemma supp_is_subset: - fixes S :: "atom set" - and x :: "'a::pt" - assumes a1: "S supports x" - and a2: "finite S" - shows "(supp x) \ S" -proof (rule ccontr) - assume "\ (supp x \ S)" - 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) - then have "a \ (supp x)" unfolding supp_def by simp - with b1 show False by simp -qed - -lemma supports_finite: - fixes S :: "atom set" - and x :: "'a::pt" - assumes a1: "S supports x" - and a2: "finite S" - shows "finite (supp x)" -proof - - have "(supp x) \ S" using a1 a2 by (rule supp_is_subset) - then show "finite (supp x)" using a2 by (simp add: finite_subset) -qed - -lemma supp_supports: - fixes x :: "'a::pt" - shows "(supp x) supports x" -unfolding supports_def -proof (intro strip) - fix a b - assume "a \ (supp x) \ b \ (supp x)" - then have "a \ x" and "b \ x" by (simp_all add: fresh_def) - then show "(a \ b) \ x = x" by (simp add: swap_fresh_fresh) -qed - -lemma supp_is_least_supports: - fixes S :: "atom set" - and x :: "'a::pt" - assumes a1: "S supports x" - and a2: "finite S" - and a3: "\S'. finite S' \ (S' supports x) \ S \ S'" - shows "(supp x) = S" -proof (rule equalityI) - show "(supp x) \ S" using a1 a2 by (rule supp_is_subset) - with a2 have fin: "finite (supp x)" by (rule rev_finite_subset) - have "(supp x) supports x" by (rule supp_supports) - with fin a3 show "S \ supp x" by blast -qed - -lemma subsetCI: - shows "(\x. x \ A \ x \ B \ False) \ A \ B" - by auto - -lemma finite_supp_unique: - assumes a1: "S supports x" - assumes a2: "finite S" - assumes a3: "\a b. \a \ S; b \ S; sort_of a = sort_of b\ \ (a \ b) \ x \ x" - shows "(supp x) = S" - using a1 a2 -proof (rule supp_is_least_supports) - fix S' - assume "finite S'" and "S' supports x" - show "S \ S'" - proof (rule subsetCI) - fix a - assume "a \ S" and "a \ S'" - have "finite (S \ S')" - using `finite S` `finite S'` by simp - then obtain b where "b \ S \ S'" and "sort_of b = sort_of a" - by (rule obtain_atom) - then have "b \ S" and "b \ S'" and "sort_of a = sort_of b" - by simp_all - then have "(a \ b) \ x = x" - using `a \ S'` `S' supports x` by (simp add: supports_def) - moreover have "(a \ b) \ x \ x" - using `a \ S` `b \ S` `sort_of a = sort_of b` - by (rule a3) - ultimately show "False" by simp - qed -qed - -section {* Support w.r.t. relations *} - -text {* - This definition is used for unquotient types, where - alpha-equivalence does not coincide with equality. -*} - -definition - "supp_rel R x = {a. infinite {b. \(R ((a \ b) \ x) x)}}" - - - -section {* Finitely-supported types *} - -class fs = pt + - assumes finite_supp: "finite (supp x)" - -lemma pure_supp: - shows "supp (x::'a::pure) = {}" - unfolding supp_def by (simp add: permute_pure) - -lemma pure_fresh: - fixes x::"'a::pure" - shows "a \ x" - unfolding fresh_def by (simp add: pure_supp) - -instance pure < fs -by default (simp add: pure_supp) - - -subsection {* Type @{typ atom} is finitely-supported. *} - -lemma supp_atom: - shows "supp a = {a}" -apply (rule finite_supp_unique) -apply (clarsimp simp add: supports_def) -apply simp -apply simp -done - -lemma fresh_atom: - shows "a \ b \ a \ b" - unfolding fresh_def supp_atom by simp - -instance atom :: fs -by default (simp add: supp_atom) - -section {* Support for finite sets of atoms *} - - -lemma supp_finite_atom_set: - fixes S::"atom set" - assumes "finite S" - shows "supp S = S" - apply(rule finite_supp_unique) - apply(simp add: supports_def) - apply(simp add: swap_set_not_in) - apply(rule assms) - apply(simp add: swap_set_in) -done - -section {* Type @{typ perm} is finitely-supported. *} - -lemma perm_swap_eq: - shows "(a \ b) \ p = p \ (p \ (a \ b)) = (a \ b)" -unfolding permute_perm_def -by (metis add_diff_cancel minus_perm_def) - -lemma supports_perm: - shows "{a. p \ a \ a} supports p" - unfolding supports_def - unfolding perm_swap_eq - by (simp add: swap_eqvt) - -lemma finite_perm_lemma: - shows "finite {a::atom. p \ a \ a}" - using finite_Rep_perm [of p] - unfolding permute_atom_def . - -lemma supp_perm: - shows "supp p = {a. p \ a \ a}" -apply (rule finite_supp_unique) -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) -done - -lemma fresh_perm: - shows "a \ p \ p \ a = a" - unfolding fresh_def - by (simp add: supp_perm) - -lemma supp_swap: - shows "supp (a \ b) = (if a = b \ sort_of a \ sort_of b then {} else {a, b})" - by (auto simp add: supp_perm swap_atom) - -lemma fresh_zero_perm: - shows "a \ (0::perm)" - unfolding fresh_perm by simp - -lemma supp_zero_perm: - shows "supp (0::perm) = {}" - unfolding supp_perm by simp - -lemma fresh_plus_perm: - fixes p q::perm - assumes "a \ p" "a \ q" - shows "a \ (p + q)" - using assms - unfolding fresh_def - by (auto simp add: supp_perm) - -lemma supp_plus_perm: - fixes p q::perm - shows "supp (p + q) \ supp p \ supp q" - by (auto simp add: supp_perm) - -lemma fresh_minus_perm: - fixes p::perm - shows "a \ (- p) \ a \ p" - unfolding fresh_def - unfolding supp_perm - apply(simp) - apply(metis permute_minus_cancel) - done - -lemma supp_minus_perm: - fixes p::perm - shows "supp (- p) = supp p" - 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 -proof - fix a::"atom" - show "(p + q) \ a = (q + p) \ a" - proof - - { assume "a \ supp p" "a \ supp q" - then have "(p + q) \ a = (q + p) \ a" - by (simp add: supp_perm) - } - moreover - { assume a: "a \ supp p" "a \ supp q" - then have "p \ a \ supp p" by (simp add: supp_perm) - then have "p \ a \ supp q" using asm by auto - with a have "(p + q) \ a = (q + p) \ a" - by (simp add: supp_perm) - } - moreover - { assume a: "a \ supp p" "a \ supp q" - then have "q \ a \ supp q" by (simp add: supp_perm) - then have "q \ a \ supp p" using asm by auto - with a have "(p + q) \ a = (q + p) \ a" - by (simp add: supp_perm) - } - ultimately show "(p + q) \ a = (q + p) \ a" - using asm by blast - qed -qed - -section {* Finite Support instances for other types *} - - -subsection {* Type @{typ "'a \ 'b"} is finitely-supported. *} - -lemma supp_Pair: - shows "supp (x, y) = supp x \ supp y" - by (simp add: supp_def Collect_imp_eq Collect_neg_eq) - -lemma fresh_Pair: - shows "a \ (x, y) \ a \ x \ a \ y" - by (simp add: fresh_def supp_Pair) - -lemma supp_Unit: - shows "supp () = {}" - by (simp add: supp_def) - -lemma fresh_Unit: - shows "a \ ()" - by (simp add: fresh_def supp_Unit) - -instance prod :: (fs, fs) fs -apply default -apply (induct_tac x) -apply (simp add: supp_Pair finite_supp) -done - - -subsection {* Type @{typ "'a + 'b"} is finitely supported *} - -lemma supp_Inl: - shows "supp (Inl x) = supp x" - by (simp add: supp_def) - -lemma supp_Inr: - shows "supp (Inr x) = supp x" - by (simp add: supp_def) - -lemma fresh_Inl: - shows "a \ Inl x \ a \ x" - by (simp add: fresh_def supp_Inl) - -lemma fresh_Inr: - shows "a \ Inr y \ a \ y" - by (simp add: fresh_def supp_Inr) - -instance sum :: (fs, fs) fs -apply default -apply (induct_tac x) -apply (simp_all add: supp_Inl supp_Inr finite_supp) -done - - -subsection {* Type @{typ "'a option"} is finitely supported *} - -lemma supp_None: - shows "supp None = {}" -by (simp add: supp_def) - -lemma supp_Some: - shows "supp (Some x) = supp x" - by (simp add: supp_def) - -lemma fresh_None: - shows "a \ None" - by (simp add: fresh_def supp_None) - -lemma fresh_Some: - shows "a \ Some x \ a \ x" - by (simp add: fresh_def supp_Some) - -instance option :: (fs) fs -apply default -apply (induct_tac x) -apply (simp_all add: supp_None supp_Some finite_supp) -done - - -subsubsection {* Type @{typ "'a list"} is finitely supported *} - -lemma supp_Nil: - shows "supp [] = {}" - by (simp add: supp_def) - -lemma supp_Cons: - shows "supp (x # xs) = supp x \ supp xs" -by (simp add: supp_def Collect_imp_eq Collect_neg_eq) - -lemma fresh_Nil: - shows "a \ []" - by (simp add: fresh_def supp_Nil) - -lemma fresh_Cons: - shows "a \ (x # xs) \ a \ x \ a \ xs" - by (simp add: fresh_def supp_Cons) - -instance list :: (fs) fs -apply default -apply (induct_tac x) -apply (simp_all add: supp_Nil supp_Cons finite_supp) -done - - -section {* Support and Freshness for Applications *} - -lemma fresh_conv_MOST: - shows "a \ x \ (MOST b. (a \ b) \ x = x)" - 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 - by (elim MOST_rev_mp, simp) - -lemma supp_fun_app: - shows "supp (f x) \ (supp f) \ (supp x)" - using fresh_fun_app - unfolding fresh_def - by auto - -text {* Support of Equivariant Functions *} - -lemma supp_fun_eqvt: - assumes a: "\p. p \ f = f" - shows "supp f = {}" - unfolding supp_def - using a by simp - -lemma fresh_fun_eqvt_app: - assumes a: "\p. p \ f = f" - shows "a \ x \ a \ f x" -proof - - from a have "supp f = {}" by (simp add: supp_fun_eqvt) - then show "a \ x \ a \ f x" - unfolding fresh_def - using supp_fun_app by auto -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_finite_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_finite_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_finite_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_finite_supp_sets[OF fin]) -apply(rule Union_included_in_supp[OF fin]) -done - -lemma finite_sets_supp: - fixes S::"('a::fs set)" - assumes "finite S" - shows "finite (supp S)" -using assms -by (simp only: supp_of_finite_sets Union_of_finite_supp_sets) - -lemma supp_of_finite_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_finite_sets) - -lemma supp_of_finite_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_finite_sets) - - -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 - by (simp add: fset_eqvt fset_cong) - -lemma supp_empty_fset [simp]: - shows "supp {||} = {}" - unfolding supp_def - by simp - -lemma supp_insert_fset [simp]: - fixes x::"'a::fs" - and S::"'a fset" - shows "supp (insert_fset x S) = supp x \ supp S" - apply(subst supp_fset[symmetric]) - apply(simp add: supp_fset supp_of_finite_insert) - done - -lemma fset_finite_supp: - fixes S::"('a::fs) fset" - shows "finite (supp S)" - by (induct S) (simp_all add: finite_supp) - - -instance fset :: (fs) fs - apply (default) - apply (rule fset_finite_supp) - done - - -section {* Fresh-Star *} - - -text {* The fresh-star generalisation of fresh is used in strong - induction principles. *} - -definition - fresh_star :: "atom set \ 'a::pt \ bool" ("_ \* _" [80,80] 80) -where - "as \* x \ \a \ as. a \ x" - -lemma fresh_star_supp_conv: - shows "supp x \* y \ supp y \* x" -by (auto simp add: fresh_star_def fresh_def) - -lemma fresh_star_prod: - fixes as::"atom set" - shows "as \* (x, y) = (as \* x \ as \* y)" - by (auto simp add: fresh_star_def fresh_Pair) - -lemma fresh_star_union: - shows "(as \ bs) \* x = (as \* x \ bs \* x)" - by (auto simp add: fresh_star_def) - -lemma fresh_star_insert: - shows "(insert a as) \* x = (a \ x \ as \* x)" - by (auto simp add: fresh_star_def) - -lemma fresh_star_Un_elim: - "((as \ bs) \* x \ PROP C) \ (as \* x \ bs \* x \ PROP C)" - unfolding fresh_star_def - apply(rule) - apply(erule meta_mp) - apply(auto) - done - -lemma fresh_star_insert_elim: - "(insert a as \* x \ PROP C) \ (a \ x \ as \* x \ PROP C)" - unfolding fresh_star_def - by rule (simp_all add: fresh_star_def) - -lemma fresh_star_empty_elim: - "({} \* x \ PROP C) \ PROP C" - by (simp add: fresh_star_def) - -lemma fresh_star_unit_elim: - shows "(a \* () \ PROP C) \ PROP C" - by (simp add: fresh_star_def fresh_Unit) - -lemma fresh_star_prod_elim: - shows "(a \* (x, y) \ PROP C) \ (a \* x \ a \* y \ PROP C)" - by (rule, simp_all add: fresh_star_prod) - -lemma fresh_star_zero: - shows "as \* (0::perm)" - unfolding fresh_star_def - by (simp add: fresh_zero_perm) - -lemma fresh_star_plus: - fixes p q::perm - shows "\a \* p; a \* q\ \ a \* (p + q)" - unfolding fresh_star_def - by (simp add: fresh_plus_perm) - -lemma fresh_star_permute_iff: - shows "(p \ a) \* (p \ x) \ a \* x" - unfolding fresh_star_def - by (metis mem_permute_iff permute_minus_cancel(1) fresh_permute_iff) - -lemma fresh_star_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 - - -section {* Induction principle for permutations *} - - -lemma perm_struct_induct[consumes 1, case_names zero swap]: - assumes S: "supp p \ S" - and zero: "P 0" - and swap: "\p a b. \P p; supp p \ S; a \ S; b \ S; a \ b; sort_of a = sort_of b\ \ P ((a \ b) + p)" - shows "P p" -proof - - have "finite (supp p)" by (simp add: finite_supp) - then show "P p" using S - proof(induct A\"supp p" arbitrary: p rule: finite_psubset_induct) - case (psubset p) - 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 p" using zero by simp - } - moreover - { assume "supp p \ {}" - then obtain a where a0: "a \ supp p" by blast - then have a1: "p \ a \ S" "a \ S" "sort_of (p \ a) = sort_of a" "p \ a \ a" - using as by (auto simp add: supp_atom supp_perm swap_atom) - let ?q = "(p \ a \ a) + p" - have a2: "supp ?q \ supp p" unfolding supp_perm by (auto simp add: swap_atom) - moreover - have "a \ supp ?q" by (simp add: supp_perm) - then have "supp ?q \ supp p" using a0 by auto - ultimately have "supp ?q \ supp p" using a2 by auto - then have "P ?q" using ih by simp - moreover - 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) - ultimately have "P p" by simp - } - ultimately show "P p" by blast - qed -qed - -lemma perm_simple_struct_induct[case_names zero swap]: - assumes zero: "P 0" - and swap: "\p a b. \P p; a \ b; sort_of a = sort_of b\ \ P ((a \ b) + p)" - shows "P p" -by (rule_tac S="supp p" in perm_struct_induct) - (auto intro: zero swap) - -lemma perm_subset_induct[consumes 1, case_names zero swap plus]: - assumes S: "supp p \ S" - assumes zero: "P 0" - assumes swap: "\a b. \sort_of a = sort_of b; a \ b; a \ S; b \ S\ \ P (a \ b)" - assumes plus: "\p1 p2. \P p1; P p2; supp p1 \ S; supp p2 \ S\ \ P (p1 + p2)" - shows "P p" -using S -by (induct p rule: perm_struct_induct) - (auto intro: zero plus swap simp add: supp_swap) - -lemma supp_perm_eq: - assumes "(supp x) \* p" - shows "p \ x = x" -proof - - from assms have "supp p \ {a. a \ x}" - unfolding supp_perm fresh_star_def fresh_def by auto - then show "p \ x = x" - proof (induct p rule: perm_struct_induct) - case zero - show "0 \ x = x" by simp - next - case (swap p a b) - then have "a \ x" "b \ x" "p \ x = x" by simp_all - then show "((a \ b) + p) \ x = x" by (simp add: swap_fresh_fresh) - qed -qed - -lemma supp_perm_eq_test: - assumes "(supp x) \* p" - shows "p \ x = x" -proof - - from assms have "supp p \ {a. a \ x}" - unfolding supp_perm fresh_star_def fresh_def by auto - then show "p \ x = x" - proof (induct p rule: perm_subset_induct) - case zero - show "0 \ x = x" by simp - next - case (swap a b) - then have "a \ x" "b \ x" by simp_all - then show "(a \ b) \ x = x" by (simp add: swap_fresh_fresh) - next - case (plus p1 p2) - have "p1 \ x = x" "p2 \ x = x" by fact+ - then show "(p1 + p2) \ x = x" by simp - qed -qed - - -section {* Avoiding of atom sets *} - -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::"atom set" - and As::"atom set" - assumes b: "Xs \ As" - and c: "finite As" - shows "\p. (p \ Xs) \ As = {} \ (supp p) \ (Xs \ (p \ Xs))" -proof - - from b c have "finite Xs" by (rule finite_subset) - then show ?thesis using b - proof (induct rule: finite_subset_induct) - case empty - have "0 \ {} \ As = {}" by simp - moreover - have "supp (0::perm) \ {} \ 0 \ {}" by (simp add: supp_zero_perm) - ultimately show ?case by blast - next - case (insert x Xs) - then obtain p where - p1: "(p \ Xs) \ As = {}" and - p2: "supp p \ (Xs \ (p \ Xs))" by blast - from `x \ As` p1 have "x \ p \ Xs" by fast - with `x \ Xs` p2 have "x \ supp p" by fast - hence px: "p \ x = x" unfolding supp_perm by simp - have "finite (As \ p \ Xs)" - using `finite As` `finite Xs` - by (simp add: permute_set_eq_image) - then obtain y where "y \ (As \ p \ Xs)" "sort_of y = sort_of x" - by (rule obtain_atom) - hence y: "y \ As" "y \ p \ Xs" "sort_of y = sort_of x" - by simp_all - let ?q = "(x \ y) + p" - have q: "?q \ insert x Xs = insert y (p \ Xs)" - unfolding insert_eqvt - using `p \ x = x` `sort_of y = sort_of x` - using `x \ p \ Xs` `y \ p \ Xs` - by (simp add: swap_atom swap_set_not_in) - have "?q \ insert x Xs \ As = {}" - using `y \ As` `p \ Xs \ As = {}` - unfolding q by simp - moreover - have "supp ?q \ insert x Xs \ ?q \ insert x Xs" - using p2 unfolding q - by (intro subset_trans [OF supp_plus_perm]) - (auto simp add: supp_swap) - ultimately show ?case by blast - qed -qed - -lemma at_set_avoiding: - assumes a: "finite Xs" - and b: "finite (supp c)" - obtains p::"perm" where "(p \ Xs)\*c" and "(supp p) \ (Xs \ (p \ Xs))" - using a b at_set_avoiding_aux [where Xs="Xs" and As="Xs \ supp c"] - unfolding fresh_star_def fresh_def by blast - -lemma at_set_avoiding2: - assumes "finite xs" - and "finite (supp c)" "finite (supp x)" - and "xs \* x" - shows "\p. (p \ xs) \* c \ supp x \* p" -using assms -apply(erule_tac c="(c, x)" in at_set_avoiding) -apply(simp add: supp_Pair) -apply(rule_tac x="p" in exI) -apply(simp add: fresh_star_prod) -apply(rule fresh_star_supp_conv) -apply(auto simp add: fresh_star_def) -done - -lemma at_set_avoiding2_atom: - assumes "finite (supp c)" "finite (supp x)" - and b: "a \ x" - shows "\p. (p \ a) \ c \ supp x \* p" -proof - - have a: "{a} \* x" unfolding fresh_star_def by (simp add: b) - obtain p where p1: "(p \ {a}) \* c" and p2: "supp x \* p" - using at_set_avoiding2[of "{a}" "c" "x"] assms a by blast - have c: "(p \ a) \ c" using p1 - unfolding fresh_star_def Ball_def - by(erule_tac x="p \ a" in allE) (simp add: permute_set_eq) - hence "p \ a \ c \ supp x \* p" using p2 by blast - then show "\p. (p \ a) \ c \ supp x \* p" by blast -qed - - -section {* Concrete Atoms Types *} - -text {* - Class @{text at_base} allows types containing multiple sorts of atoms. - Class @{text at} only allows types with a single sort. -*} - -class at_base = pt + - fixes atom :: "'a \ atom" - assumes atom_eq_iff [simp]: "atom a = atom b \ a = b" - assumes atom_eqvt: "p \ (atom a) = atom (p \ a)" - -class at = at_base + - assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)" - -lemma supp_at_base: - fixes a::"'a::at_base" - shows "supp a = {atom a}" - by (simp add: supp_atom [symmetric] supp_def atom_eqvt) - -lemma fresh_at_base: - shows "a \ b \ a \ atom b" - unfolding fresh_def by (simp add: supp_at_base) - -instance at_base < fs -proof qed (simp add: supp_at_base) - -lemma at_base_infinite [simp]: - shows "infinite (UNIV :: 'a::at_base set)" (is "infinite ?U") -proof - obtain a :: 'a where "True" by auto - assume "finite ?U" - hence "finite (atom ` ?U)" - by (rule finite_imageI) - then obtain b where b: "b \ atom ` ?U" "sort_of b = sort_of (atom a)" - by (rule obtain_atom) - from b(2) have "b = atom ((atom a \ b) \ a)" - unfolding atom_eqvt [symmetric] - by (simp add: swap_atom) - hence "b \ atom ` ?U" by simp - with b(1) show "False" by simp -qed - -lemma swap_at_base_simps [simp]: - fixes x y::"'a::at_base" - shows "sort_of (atom x) = sort_of (atom y) \ (atom x \ atom y) \ x = y" - and "sort_of (atom x) = sort_of (atom y) \ (atom x \ atom y) \ y = x" - and "atom x \ a \ atom x \ b \ (a \ b) \ x = x" - unfolding atom_eq_iff [symmetric] - unfolding atom_eqvt [symmetric] - by simp_all - -lemma obtain_at_base: - assumes X: "finite X" - obtains a::"'a::at_base" where "atom a \ X" -proof - - have "inj (atom :: 'a \ atom)" - by (simp add: inj_on_def) - with X have "finite (atom -` X :: 'a set)" - by (rule finite_vimageI) - with at_base_infinite have "atom -` X \ (UNIV :: 'a set)" - by auto - then obtain a :: 'a where "atom a \ X" - by auto - thus ?thesis .. -qed - -lemma supp_finite_set_at_base: - assumes a: "finite S" - shows "supp S = atom ` S" -apply(simp add: supp_of_finite_sets[OF a]) -apply(simp add: supp_at_base) -apply(auto) -done - -section {* Infrastructure for concrete atom types *} - -section {* A swapping operation for concrete atoms *} - -definition - flip :: "'a::at_base \ 'a \ perm" ("'(_ \ _')") -where - "(a \ b) = (atom a \ atom b)" - -lemma flip_self [simp]: "(a \ a) = 0" - unfolding flip_def by (rule swap_self) - -lemma flip_commute: "(a \ b) = (b \ a)" - unfolding flip_def by (rule swap_commute) - -lemma minus_flip [simp]: "- (a \ b) = (a \ b)" - unfolding flip_def by (rule minus_swap) - -lemma add_flip_cancel: "(a \ b) + (a \ b) = 0" - unfolding flip_def by (rule swap_cancel) - -lemma permute_flip_cancel [simp]: "(a \ b) \ (a \ b) \ x = x" - unfolding permute_plus [symmetric] add_flip_cancel by simp - -lemma permute_flip_cancel2 [simp]: "(a \ b) \ (b \ a) \ x = x" - by (simp add: flip_commute) - -lemma flip_eqvt: - fixes a b c::"'a::at_base" - shows "p \ (a \ b) = (p \ a \ p \ b)" - unfolding flip_def - by (simp add: swap_eqvt atom_eqvt) - -lemma flip_at_base_simps [simp]: - shows "sort_of (atom a) = sort_of (atom b) \ (a \ b) \ a = b" - and "sort_of (atom a) = sort_of (atom b) \ (a \ b) \ b = a" - and "\a \ c; b \ c\ \ (a \ b) \ c = c" - and "sort_of (atom a) \ sort_of (atom b) \ (a \ b) \ x = x" - unfolding flip_def - unfolding atom_eq_iff [symmetric] - unfolding atom_eqvt [symmetric] - by simp_all - -text {* the following two lemmas do not hold for at_base, - only for single sort atoms from at *} - -lemma permute_flip_at: - fixes a b c::"'a::at" - shows "(a \ b) \ c = (if c = a then b else if c = b then a else c)" - unfolding flip_def - apply (rule atom_eq_iff [THEN iffD1]) - apply (subst atom_eqvt [symmetric]) - apply (simp add: swap_atom) - done - -lemma flip_at_simps [simp]: - fixes a b::"'a::at" - shows "(a \ b) \ a = b" - and "(a \ b) \ b = a" - unfolding permute_flip_at by simp_all - -lemma flip_fresh_fresh: - fixes a b::"'a::at_base" - assumes "atom a \ x" "atom b \ x" - shows "(a \ b) \ x = x" -using assms -by (simp add: flip_def swap_fresh_fresh) - -subsection {* Syntax for coercing at-elements to the atom-type *} - -syntax - "_atom_constrain" :: "logic \ type \ logic" ("_:::_" [4, 0] 3) - -translations - "_atom_constrain a t" => "CONST atom (_constrain a t)" - - -subsection {* A lemma for proving instances of class @{text at}. *} - -setup {* Sign.add_const_constraint (@{const_name "permute"}, NONE) *} -setup {* Sign.add_const_constraint (@{const_name "atom"}, NONE) *} - -text {* - New atom types are defined as subtypes of @{typ atom}. -*} - -lemma exists_eq_simple_sort: - shows "\a. a \ {a. sort_of a = s}" - by (rule_tac x="Atom s 0" in exI, simp) - -lemma exists_eq_sort: - shows "\a. a \ {a. sort_of a \ range sort_fun}" - by (rule_tac x="Atom (sort_fun x) y" in exI, simp) - -lemma at_base_class: - fixes sort_fun :: "'b \atom_sort" - fixes Rep :: "'a \ atom" and Abs :: "atom \ 'a" - assumes type: "type_definition Rep Abs {a. sort_of a \ range sort_fun}" - assumes atom_def: "\a. atom a = Rep a" - assumes permute_def: "\p a. p \ a = Abs (p \ Rep a)" - shows "OFCLASS('a, at_base_class)" -proof - interpret type_definition Rep Abs "{a. sort_of a \ range sort_fun}" by (rule type) - have sort_of_Rep: "\a. sort_of (Rep a) \ range sort_fun" using Rep by simp - fix a b :: 'a and p p1 p2 :: perm - show "0 \ a = a" - unfolding permute_def by (simp add: Rep_inverse) - show "(p1 + p2) \ a = p1 \ p2 \ a" - unfolding permute_def by (simp add: Abs_inverse sort_of_Rep) - show "atom a = atom b \ a = b" - unfolding atom_def by (simp add: Rep_inject) - show "p \ atom a = atom (p \ a)" - unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep) -qed - -(* -lemma at_class: - fixes s :: atom_sort - fixes Rep :: "'a \ atom" and Abs :: "atom \ 'a" - assumes type: "type_definition Rep Abs {a. sort_of a \ range (\x::unit. s)}" - assumes atom_def: "\a. atom a = Rep a" - assumes permute_def: "\p a. p \ a = Abs (p \ Rep a)" - shows "OFCLASS('a, at_class)" -proof - interpret type_definition Rep Abs "{a. sort_of a \ range (\x::unit. s)}" by (rule type) - have sort_of_Rep: "\a. sort_of (Rep a) = s" using Rep by (simp add: image_def) - fix a b :: 'a and p p1 p2 :: perm - show "0 \ a = a" - unfolding permute_def by (simp add: Rep_inverse) - show "(p1 + p2) \ a = p1 \ p2 \ a" - unfolding permute_def by (simp add: Abs_inverse sort_of_Rep) - show "sort_of (atom a) = sort_of (atom b)" - unfolding atom_def by (simp add: sort_of_Rep) - show "atom a = atom b \ a = b" - unfolding atom_def by (simp add: Rep_inject) - show "p \ atom a = atom (p \ a)" - unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep) -qed -*) - -lemma at_class: - fixes s :: atom_sort - fixes Rep :: "'a \ atom" and Abs :: "atom \ 'a" - assumes type: "type_definition Rep Abs {a. sort_of a = s}" - assumes atom_def: "\a. atom a = Rep a" - assumes permute_def: "\p a. p \ a = Abs (p \ Rep a)" - shows "OFCLASS('a, at_class)" -proof - interpret type_definition Rep Abs "{a. sort_of a = s}" by (rule type) - have sort_of_Rep: "\a. sort_of (Rep a) = s" using Rep by (simp add: image_def) - fix a b :: 'a and p p1 p2 :: perm - show "0 \ a = a" - unfolding permute_def by (simp add: Rep_inverse) - show "(p1 + p2) \ a = p1 \ p2 \ a" - unfolding permute_def by (simp add: Abs_inverse sort_of_Rep) - show "sort_of (atom a) = sort_of (atom b)" - unfolding atom_def by (simp add: sort_of_Rep) - show "atom a = atom b \ a = b" - unfolding atom_def by (simp add: Rep_inject) - show "p \ atom a = atom (p \ a)" - unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep) -qed - -setup {* Sign.add_const_constraint - (@{const_name "permute"}, SOME @{typ "perm \ 'a::pt \ 'a"}) *} -setup {* Sign.add_const_constraint - (@{const_name "atom"}, SOME @{typ "'a::at_base \ atom"}) *} - - - -section {* The freshness lemma according to Andy Pitts *} - -lemma freshness_lemma: - fixes h :: "'a::at \ 'b::pt" - assumes a: "\a. atom a \ (h, h a)" - shows "\x. \a. atom a \ h \ h a = x" -proof - - from a obtain b where a1: "atom b \ h" and a2: "atom b \ h b" - by (auto simp add: fresh_Pair) - show "\x. \a. atom a \ h \ h a = x" - proof (intro exI allI impI) - fix a :: 'a - assume a3: "atom a \ h" - show "h a = h b" - proof (cases "a = b") - assume "a = b" - thus "h a = h b" by simp - next - assume "a \ b" - hence "atom a \ b" by (simp add: fresh_at_base) - with a3 have "atom a \ h b" - by (rule fresh_fun_app) - with a2 have d1: "(atom b \ atom a) \ (h b) = (h b)" - by (rule swap_fresh_fresh) - from a1 a3 have d2: "(atom b \ atom a) \ h = h" - by (rule swap_fresh_fresh) - from d1 have "h b = (atom b \ atom a) \ (h b)" by simp - also have "\ = ((atom b \ atom a) \ h) ((atom b \ atom a) \ b)" - by (rule permute_fun_app_eq) - also have "\ = h a" - using d2 by simp - finally show "h a = h b" by simp - qed - qed -qed - -lemma freshness_lemma_unique: - fixes h :: "'a::at \ 'b::pt" - assumes a: "\a. atom a \ (h, h a)" - shows "\!x. \a. atom a \ h \ h a = x" -proof (rule ex_ex1I) - from a show "\x. \a. atom a \ h \ h a = x" - by (rule freshness_lemma) -next - fix x y - assume x: "\a. atom a \ h \ h a = x" - assume y: "\a. atom a \ h \ h a = y" - from a x y show "x = y" - by (auto simp add: fresh_Pair) -qed - -text {* packaging the freshness lemma into a function *} - -definition - fresh_fun :: "('a::at \ 'b::pt) \ 'b" -where - "fresh_fun h = (THE x. \a. atom a \ h \ h a = x)" - -lemma fresh_fun_apply: - fixes h :: "'a::at \ 'b::pt" - assumes a: "\a. atom a \ (h, h a)" - assumes b: "atom a \ h" - shows "fresh_fun h = h a" -unfolding fresh_fun_def -proof (rule the_equality) - show "\a'. atom a' \ h \ h a' = h a" - proof (intro strip) - fix a':: 'a - assume c: "atom a' \ h" - from a have "\x. \a. atom a \ h \ h a = x" by (rule freshness_lemma) - with b c show "h a' = h a" by auto - qed -next - fix fr :: 'b - assume "\a. atom a \ h \ h a = fr" - with b show "fr = h a" by auto -qed - -lemma fresh_fun_apply': - fixes h :: "'a::at \ 'b::pt" - assumes a: "atom a \ h" "atom a \ h a" - shows "fresh_fun h = h a" - apply (rule fresh_fun_apply) - apply (auto simp add: fresh_Pair intro: a) - done - -lemma fresh_fun_eqvt: - fixes h :: "'a::at \ 'b::pt" - assumes a: "\a. atom a \ (h, h a)" - shows "p \ (fresh_fun h) = fresh_fun (p \ h)" - using a - apply (clarsimp simp add: fresh_Pair) - apply (subst fresh_fun_apply', assumption+) - apply (drule fresh_permute_iff [where p=p, THEN iffD2]) - apply (drule fresh_permute_iff [where p=p, THEN iffD2]) - apply (simp add: atom_eqvt permute_fun_app_eq [where f=h]) - apply (erule (1) fresh_fun_apply' [symmetric]) - done - -lemma fresh_fun_supports: - fixes h :: "'a::at \ 'b::pt" - assumes a: "\a. atom a \ (h, h a)" - shows "(supp h) supports (fresh_fun h)" - apply (simp add: supports_def fresh_def [symmetric]) - apply (simp add: fresh_fun_eqvt [OF a] swap_fresh_fresh) - done - -notation fresh_fun (binder "FRESH " 10) - -lemma FRESH_f_iff: - fixes P :: "'a::at \ 'b::pure" - fixes f :: "'b \ 'c::pure" - assumes P: "finite (supp P)" - shows "(FRESH x. f (P x)) = f (FRESH x. P x)" -proof - - obtain a::'a where "atom a \ supp P" - using P by (rule obtain_at_base) - hence "atom a \ P" - by (simp add: fresh_def) - show "(FRESH x. f (P x)) = f (FRESH x. P x)" - apply (subst fresh_fun_apply' [where a=a, OF _ pure_fresh]) - apply (cut_tac `atom a \ P`) - apply (simp add: fresh_conv_MOST) - apply (elim MOST_rev_mp, rule MOST_I, clarify) - apply (simp add: permute_fun_def permute_pure fun_eq_iff) - apply (subst fresh_fun_apply' [where a=a, OF `atom a \ P` pure_fresh]) - apply (rule refl) - done -qed - -lemma FRESH_binop_iff: - fixes P :: "'a::at \ 'b::pure" - fixes Q :: "'a::at \ 'c::pure" - fixes binop :: "'b \ 'c \ 'd::pure" - assumes P: "finite (supp P)" - and Q: "finite (supp Q)" - shows "(FRESH x. binop (P x) (Q x)) = binop (FRESH x. P x) (FRESH x. Q x)" -proof - - from assms have "finite (supp P \ supp Q)" by simp - then obtain a::'a where "atom a \ (supp P \ supp Q)" - by (rule obtain_at_base) - hence "atom a \ P" and "atom a \ Q" - by (simp_all add: fresh_def) - show ?thesis - apply (subst fresh_fun_apply' [where a=a, OF _ pure_fresh]) - apply (cut_tac `atom a \ P` `atom a \ Q`) - apply (simp add: fresh_conv_MOST) - apply (elim MOST_rev_mp, rule MOST_I, clarify) - apply (simp add: permute_fun_def permute_pure fun_eq_iff) - apply (subst fresh_fun_apply' [where a=a, OF `atom a \ P` pure_fresh]) - apply (subst fresh_fun_apply' [where a=a, OF `atom a \ Q` pure_fresh]) - apply (rule refl) - done -qed - -lemma FRESH_conj_iff: - fixes P Q :: "'a::at \ bool" - assumes P: "finite (supp P)" and Q: "finite (supp Q)" - shows "(FRESH x. P x \ Q x) \ (FRESH x. P x) \ (FRESH x. Q x)" -using P Q by (rule FRESH_binop_iff) - -lemma FRESH_disj_iff: - fixes P Q :: "'a::at \ bool" - assumes P: "finite (supp P)" and Q: "finite (supp Q)" - shows "(FRESH x. P x \ Q x) \ (FRESH x. P x) \ (FRESH x. Q x)" -using P Q by (rule FRESH_binop_iff) - - -section {* Library functions for the nominal infrastructure *} - -use "nominal_library.ML" - - -section {* Automation for creating concrete atom types *} - -text {* at the moment only single-sort concrete atoms are supported *} - -use "nominal_atoms.ML" - - - -end diff -r 41137dc935ff -r 8193bbaa07fe Nominal-General/Nominal2_Eqvt.thy --- a/Nominal-General/Nominal2_Eqvt.thy Sun Nov 14 12:09:14 2010 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,382 +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 imp_eqvt - imp_eqvt[folded induct_implies_def] - uminus_eqvt - - (* nominal *) - supp_eqvt fresh_eqvt fresh_star_eqvt add_perm_eqvt atom_eqvt - swap_eqvt flip_eqvt - - (* datatypes *) - Pair_eqvt permute_list.simps - - (* sets *) - mem_eqvt empty_eqvt insert_eqvt set_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_eqvt[eqvt]: - shows "p \ (\!x. P x) = (\!x. (p \ P) x)" - unfolding Ex1_def - by (perm_simp) (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 (- 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 supp_set_empty: - shows "supp {} = {}" - unfolding supp_def - by (simp add: empty_eqvt) - -lemma fresh_set_empty: - shows "a \ {}" - by (simp add: fresh_def supp_set_empty) - -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 inter_eqvt[eqvt]: - shows "p \ (A \ B) = (p \ A) \ (p \ B)" - unfolding Int_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 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 - by (perm_simp) (rule refl) - -lemma Union_eqvt[eqvt]: - shows "p \ (\ S) = \ (p \ S)" - unfolding Union_eq - 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 .. - -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_finite_insert) -done - - -section {* List Operations *} - -lemma append_eqvt[eqvt]: - shows "p \ (xs @ ys) = (p \ xs) @ (p \ ys)" - by (induct xs) auto - -lemma supp_append: - shows "supp (xs @ ys) = supp xs \ supp ys" - by (induct xs) (auto simp add: supp_Nil supp_Cons) - -lemma fresh_append: - shows "a \ (xs @ ys) \ a \ xs \ a \ ys" - by (induct xs) (simp_all add: fresh_Nil fresh_Cons) - -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) - - -subsection {* Equivariance for fsets *} - -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 41137dc935ff -r 8193bbaa07fe Nominal-General/ROOT.ML --- a/Nominal-General/ROOT.ML Sun Nov 14 12:09:14 2010 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,7 +0,0 @@ - -no_document use_thys - ["Nominal2_Base", - "Nominal2_Eqvt", - "Nominal2_Atoms", - "Nominal2_Supp", - "Atoms"]; diff -r 41137dc935ff -r 8193bbaa07fe Nominal-General/nominal_atoms.ML --- a/Nominal-General/nominal_atoms.ML Sun Nov 14 12:09:14 2010 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,83 +0,0 @@ -(* Title: nominal_atoms/ML - Authors: Brian Huffman, Christian Urban - - Command for defining concrete atom types. - - At the moment, only single-sorted atom types - are supported. -*) - -signature ATOM_DECL = -sig - val add_atom_decl: (binding * (binding option)) -> theory -> theory -end; - -structure Atom_Decl :> ATOM_DECL = -struct - -fun atom_decl_set (str : string) : term = - let - val a = Free ("a", @{typ atom}); - val s = Const (@{const_name "Sort"}, @{typ "string => atom_sort list => atom_sort"}) - $ HOLogic.mk_string str $ HOLogic.nil_const @{typ "atom_sort"}; - in - HOLogic.mk_Collect ("a", @{typ atom}, HOLogic.mk_eq (mk_sort_of a, s)) - end - -fun add_atom_decl (name : binding, arg : binding option) (thy : theory) = - let - val _ = Theory.requires thy "Nominal2_Base" "nominal logic"; - val str = Sign.full_name thy name; - - (* typedef *) - val set = atom_decl_set str; - val tac = rtac @{thm exists_eq_simple_sort} 1; - val ((full_tname, info as ({Rep_name, Abs_name, ...}, {type_definition, ...})), thy) = - Typedef.add_typedef_global false NONE (name, [], NoSyn) set NONE tac thy; - - (* definition of atom and permute *) - val newT = #abs_type (fst info); - val RepC = Const (Rep_name, newT --> @{typ atom}); - val AbsC = Const (Abs_name, @{typ atom} --> newT); - val a = Free ("a", newT); - val p = Free ("p", @{typ perm}); - val atom_eqn = - HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_atom a, RepC $ a)); - val permute_eqn = - HOLogic.mk_Trueprop (HOLogic.mk_eq - (mk_perm p a, AbsC $ (mk_perm p (RepC $ a)))); - val atom_def_name = - Binding.prefix_name "atom_" (Binding.suffix_name "_def" name); - val permute_def_name = - Binding.prefix_name "permute_" (Binding.suffix_name "_def" name); - - (* at class instance *) - val lthy = - Class.instantiation ([full_tname], [], @{sort at}) thy; - val ((_, (_, permute_ldef)), lthy) = - Specification.definition (NONE, ((permute_def_name, []), permute_eqn)) lthy; - val ((_, (_, atom_ldef)), lthy) = - Specification.definition (NONE, ((atom_def_name, []), atom_eqn)) lthy; - val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy); - val permute_def = singleton (ProofContext.export lthy ctxt_thy) permute_ldef; - val atom_def = singleton (ProofContext.export lthy ctxt_thy) atom_ldef; - val class_thm = @{thm at_class} OF [type_definition, atom_def, permute_def]; - val thy = lthy - |> Class.prove_instantiation_instance (K (Tactic.rtac class_thm 1)) - |> Local_Theory.exit_global; - in - thy - end; - -(** outer syntax **) - -local structure P = Parse and K = Keyword in - -val _ = - Outer_Syntax.command "atom_decl" "declaration of a concrete atom type" K.thy_decl - ((P.binding -- Scan.option (Args.parens (P.binding))) >> - (Toplevel.print oo (Toplevel.theory o add_atom_decl))); - -end; - -end; diff -r 41137dc935ff -r 8193bbaa07fe Nominal-General/nominal_eqvt.ML --- a/Nominal-General/nominal_eqvt.ML Sun Nov 14 12:09:14 2010 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,142 +0,0 @@ -(* Title: nominal_eqvt.ML - Author: Stefan Berghofer (original code) - Author: Christian Urban - - Automatic proofs for equivariance of inductive predicates. -*) - -signature NOMINAL_EQVT = -sig - val eqvt_rel_tac: Proof.context -> string list -> term -> thm -> thm list -> int -> tactic - val eqvt_rel_single_case_tac: Proof.context -> string list -> term -> thm -> int -> tactic - - val equivariance: bool -> term list -> thm -> thm list -> Proof.context -> thm list * local_theory - val equivariance_cmd: string -> Proof.context -> local_theory -end - -structure Nominal_Eqvt : NOMINAL_EQVT = -struct - -open Nominal_Permeq; -open Nominal_ThmDecls; - -val atomize_conv = - MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE)) - (HOL_basic_ss addsimps @{thms induct_atomize}); -val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv); -fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1 - (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt)); - - -(** equivariance tactics **) - -val perm_boolE = @{thm permute_boolE} -val perm_cancel = @{thms permute_minus_cancel(2)} - -fun eqvt_rel_single_case_tac ctxt pred_names pi intro = - let - val thy = ProofContext.theory_of ctxt - val cpi = Thm.cterm_of thy (mk_minus pi) - val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE - val simps1 = HOL_basic_ss addsimps @{thms permute_fun_def minus_minus split_paired_all} - val simps2 = HOL_basic_ss addsimps @{thms permute_bool_def} - in - eqvt_strict_tac ctxt [] pred_names THEN' - SUBPROOF (fn {prems, context as ctxt, ...} => - let - val prems' = map (transform_prem2 ctxt pred_names) prems - val tac1 = resolve_tac prems' - val tac2 = EVERY' [ rtac pi_intro_rule, - eqvt_strict_tac ctxt perm_cancel pred_names, resolve_tac prems' ] - val tac3 = EVERY' [ rtac pi_intro_rule, - eqvt_strict_tac ctxt perm_cancel pred_names, simp_tac simps1, - simp_tac simps2, resolve_tac prems'] - in - (rtac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3]) 1 - end) ctxt - end - -fun eqvt_rel_tac ctxt pred_names pi induct intros = - let - val cases = map (eqvt_rel_single_case_tac ctxt pred_names pi) intros - in - EVERY' (rtac induct :: cases) - end - - -(** equivariance procedure *) - -fun prepare_goal pi pred = - let - val (c, xs) = strip_comb pred; - in - HOLogic.mk_imp (pred, list_comb (c, map (mk_perm pi) xs)) - end - -(* stores thm under name.eqvt and adds [eqvt]-attribute *) - -fun note_named_thm (name, thm) ctxt = - let - val thm_name = Binding.qualified_name - (Long_Name.qualify (Long_Name.base_name name) "eqvt") - val attr = Attrib.internal (K eqvt_add) - val ((_, [thm']), ctxt') = Local_Theory.note ((thm_name, [attr]), [thm]) ctxt - in - (thm', ctxt') - end - -fun equivariance note_flag pred_trms raw_induct intrs ctxt = - let - val is_already_eqvt = - filter (is_eqvt ctxt) pred_trms - |> map (Syntax.string_of_term ctxt) - val _ = if null is_already_eqvt then () - else error ("Already equivariant: " ^ commas is_already_eqvt) - - val pred_names = map (fst o dest_Const) pred_trms - val raw_induct' = atomize_induct ctxt raw_induct - val intrs' = map atomize_intr intrs - - val (([raw_concl], [raw_pi]), ctxt') = - ctxt - |> Variable.import_terms false [concl_of raw_induct'] - ||>> Variable.variant_fixes ["p"] - val pi = Free (raw_pi, @{typ perm}) - - val preds = map (fst o HOLogic.dest_imp) - (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl)); - - val goal = HOLogic.mk_Trueprop - (foldr1 HOLogic.mk_conj (map (prepare_goal pi) preds)) - - val thms = Goal.prove ctxt' [] [] goal - (fn {context,...} => eqvt_rel_tac context pred_names pi raw_induct' intrs' 1) - |> Datatype_Aux.split_conj_thm - |> ProofContext.export ctxt' ctxt - |> map (fn th => th RS mp) - |> map zero_var_indexes - in - if note_flag - then fold_map note_named_thm (pred_names ~~ thms) ctxt - else (thms, ctxt) - end - -fun equivariance_cmd pred_name ctxt = - let - val thy = ProofContext.theory_of ctxt - val (_, {preds, raw_induct, intrs, ...}) = - Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) - in - equivariance true preds raw_induct intrs ctxt |> snd - end - -local structure P = Parse and K = Keyword in - -val _ = - Outer_Syntax.local_theory "equivariance" - "Proves equivariance for inductive predicate involving nominal datatypes." - K.thy_decl (P.xname >> equivariance_cmd); - -end; - -end (* structure *) diff -r 41137dc935ff -r 8193bbaa07fe Nominal-General/nominal_library.ML --- a/Nominal-General/nominal_library.ML Sun Nov 14 12:09:14 2010 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,372 +0,0 @@ -(* Title: nominal_library.ML - Author: Christian Urban - - Basic functions for nominal. -*) - -signature NOMINAL_LIBRARY = -sig - val is_true: term -> bool - - val last2: 'a list -> 'a * 'a - - val dest_listT: typ -> typ - - val size_const: typ -> 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 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 mk_atom_ty: typ -> term -> term - val mk_atom: term -> term - - val supp_ty: typ -> typ - val supp_const: typ -> term - val mk_supp_ty: typ -> term -> term - val mk_supp: term -> term - - val supp_rel_ty: typ -> typ - val supp_rel_const: typ -> term - val mk_supp_rel_ty: typ -> term -> term -> term - val mk_supp_rel: term -> term -> term - - val supports_const: typ -> term - val mk_supports_ty: typ -> term -> term -> term - val mk_supports: term -> term -> term - - val finite_const: typ -> term - 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 - val fold_union: term list -> term - val fold_append: term list -> term - val mk_conj: term * term -> term - val fold_conj: term list -> term - - (* fresh arguments for a term *) - val fresh_args: Proof.context -> term -> term list - - (* datatype operations *) - type cns_info = (term * typ * typ list * bool list) list - - val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list - val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ - val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> cns_info list - val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> cns_info - val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list - - (* tactics for function package *) - val pat_completeness_simp: thm list -> Proof.context -> tactic - val prove_termination: thm list -> Proof.context -> Function.info * local_theory - - (* transformations of premises in inductions *) - val transform_prem1: Proof.context -> string list -> thm -> thm - val transform_prem2: Proof.context -> string list -> thm -> thm - - (* transformation into the object logic *) - val atomize: thm -> thm - -end - - -structure Nominal_Library: NOMINAL_LIBRARY = -struct - -fun is_true @{term "Trueprop True"} = true - | is_true _ = false - -fun last2 [] = raise Empty - | last2 [_] = raise Empty - | last2 [x, y] = (x, y) - | last2 (_ :: xs) = last2 xs - -fun dest_listT (Type (@{type_name list}, [T])) = T - | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) - -fun size_const ty = Const (@{const_name size}, ty --> @{typ nat}) - -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 mk_perm_ty ty p trm = Const (@{const_name "permute"}, perm_ty 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"}; -fun mk_atom_ty ty t = Const (@{const_name "atom"}, atom_ty ty) $ t; -fun mk_atom t = mk_atom_ty (fastype_of t) t; - - -fun supp_ty ty = ty --> @{typ "atom set"}; -fun supp_const ty = Const (@{const_name supp}, supp_ty ty) -fun mk_supp_ty ty t = supp_const ty $ t -fun mk_supp t = mk_supp_ty (fastype_of t) t - -fun supp_rel_ty ty = ([ty, ty] ---> @{typ bool}) --> ty --> @{typ "atom set"}; -fun supp_rel_const ty = Const (@{const_name supp_rel}, supp_rel_ty ty) -fun mk_supp_rel_ty ty r t = supp_rel_const ty $ r $ t -fun mk_supp_rel r t = mk_supp_rel_ty (fastype_of t) r t - -fun supports_const ty = Const (@{const_name supports}, [@{typ "atom set"}, ty] ---> @{typ bool}); -fun mk_supports_ty ty t1 t2 = supports_const ty $ t1 $ t2; -fun mk_supports t1 t2 = mk_supports_ty (fastype_of t2) t1 t2; - -fun finite_const ty = Const (@{const_name finite}, ty --> @{typ bool}) -fun mk_finite_ty ty t = finite_const ty $ t -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 *) - -fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"} - | mk_diff (t1, @{term "{}::atom set"}) = t1 - | mk_diff (@{term "set ([]::atom list)"}, _) = @{term "set ([]::atom list)"} - | mk_diff (t1, @{term "set ([]::atom list)"}) = t1 - | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2) - -fun mk_append (t1, @{term "[]::atom list"}) = t1 - | mk_append (@{term "[]::atom list"}, t2) = t2 - | mk_append (t1, t2) = HOLogic.mk_binop @{const_name "append"} (t1, t2) - -fun mk_union (t1, @{term "{}::atom set"}) = t1 - | mk_union (@{term "{}::atom set"}, t2) = t2 - | mk_union (t1, @{term "set ([]::atom list)"}) = t1 - | mk_union (@{term "set ([]::atom list)"}, t2) = t2 - | mk_union (t1, t2) = HOLogic.mk_binop @{const_name "sup"} (t1, t2) - -fun fold_union trms = fold_rev (curry mk_union) trms @{term "{}::atom set"} -fun fold_append trms = fold_rev (curry mk_append) trms @{term "[]::atom list"} - -fun mk_conj (t1, @{term "True"}) = t1 - | mk_conj (@{term "True"}, t2) = t2 - | mk_conj (t1, t2) = HOLogic.mk_conj (t1, t2) - -fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"} - - -(* produces fresh arguments for a term *) - -fun fresh_args ctxt f = - f |> fastype_of - |> binder_types - |> map (pair "z") - |> Variable.variant_frees ctxt [f] - |> map Free - - - -(** datatypes **) - -(* constructor infos *) -type cns_info = (term * typ * typ list * bool list) list - -(* returns the type of the nth datatype *) -fun all_dtyps descr sorts = - map (fn n => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n)) (0 upto (length descr - 1)) - -fun nth_dtyp descr sorts n = - Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n); - -(* returns info about constructors in a datatype *) -fun all_dtyp_constrs_info descr = - map (fn (_, (ty, vs, constrs)) => map (pair (ty, vs)) constrs) descr - -(* returns the constants of the constructors plus the - corresponding type and types of arguments *) -fun all_dtyp_constrs_types descr sorts = - let - fun aux ((ty_name, vs), (cname, args)) = - let - val vs_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) vs - val ty = Type (ty_name, vs_tys) - val arg_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) args - val is_rec = map Datatype_Aux.is_rec_type args - in - (Const (cname, arg_tys ---> ty), ty, arg_tys, is_rec) - end - in - map (map aux) (all_dtyp_constrs_info descr) - end - -fun nth_dtyp_constrs_types descr sorts n = - nth (all_dtyp_constrs_types descr sorts) n - - -(* generates for every datatype a name str ^ dt_name - plus and index for multiple occurences of a string *) -fun prefix_dt_names descr sorts str = - let - fun get_nth_name (i, _) = - Datatype_Aux.name_of_typ (nth_dtyp descr sorts i) - in - Datatype_Prop.indexify_names - (map (prefix str o get_nth_name) descr) - end - - - -(** function package tactics **) - -fun pat_completeness_simp simps lthy = - let - val simp_set = HOL_basic_ss addsimps (@{thms sum.inject sum.distinct} @ simps) - in - Pat_Completeness.pat_completeness_tac lthy 1 - THEN ALLGOALS (asm_full_simp_tac simp_set) - end - - -fun prove_termination_tac size_simps ctxt = - let - val natT = @{typ nat} - fun prod_size_const fT sT = - let - val fT_fun = fT --> natT - val sT_fun = sT --> natT - val prodT = Type (@{type_name prod}, [fT, sT]) - in - Const (@{const_name prod_size}, [fT_fun, sT_fun, prodT] ---> natT) - end - - fun mk_size_measure T = - case T of - (Type (@{type_name Sum_Type.sum}, [fT, sT])) => - SumTree.mk_sumcase fT sT natT (mk_size_measure fT) (mk_size_measure sT) - | (Type (@{type_name Product_Type.prod}, [fT, sT])) => - prod_size_const fT sT $ (mk_size_measure fT) $ (mk_size_measure sT) - | _ => size_const T - - fun mk_measure_trm T = - HOLogic.dest_setT T - |> fst o HOLogic.dest_prodT - |> mk_size_measure - |> curry (op $) (Const (@{const_name "measure"}, dummyT)) - |> Syntax.check_term ctxt - - val ss = HOL_ss addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral - zero_less_Suc prod.size(1) mult_Suc_right} @ size_simps - val ss' = ss addsimprocs Nat_Numeral_Simprocs.cancel_numerals - in - Function_Relation.relation_tac ctxt mk_measure_trm - THEN_ALL_NEW simp_tac ss' - end - -fun prove_termination size_simps ctxt = - Function.prove_termination NONE - (HEADGOAL (prove_termination_tac size_simps ctxt)) ctxt - -(** transformations of premises (in inductive proofs) **) - -(* - given the theorem F[t]; proves the theorem F[f t] - - - F needs to be monotone - - f returns either SOME for a term it fires on - and NONE elsewhere -*) -fun map_term f t = - (case f t of - NONE => map_term' f t - | x => x) -and map_term' f (t $ u) = - (case (map_term f t, map_term f u) of - (NONE, NONE) => NONE - | (SOME t'', NONE) => SOME (t'' $ u) - | (NONE, SOME u'') => SOME (t $ u'') - | (SOME t'', SOME u'') => SOME (t'' $ u'')) - | map_term' f (Abs (s, T, t)) = - (case map_term f t of - NONE => NONE - | SOME t'' => SOME (Abs (s, T, t''))) - | map_term' _ _ = NONE; - -fun map_thm_tac ctxt tac thm = - let - val monos = Inductive.get_monos ctxt - val simps = HOL_basic_ss addsimps @{thms split_def} - in - EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, - REPEAT_DETERM (FIRSTGOAL (simp_tac simps THEN' resolve_tac monos)), - REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))] - end - -fun map_thm ctxt f tac thm = - let - val opt_goal_trm = map_term f (prop_of thm) - in - case opt_goal_trm of - NONE => thm - | SOME goal => - Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm) - end - -(* - inductive premises can be of the form - R ... /\ P ...; split_conj_i picks out - the part R or P part -*) -fun split_conj1 names (Const (@{const_name "conj"}, _) $ f1 $ _) = - (case head_of f1 of - Const (name, _) => if member (op =) names name then SOME f1 else NONE - | _ => NONE) -| split_conj1 _ _ = NONE; - -fun split_conj2 names (Const (@{const_name "conj"}, _) $ f1 $ f2) = - (case head_of f1 of - Const (name, _) => if member (op =) names name then SOME f2 else NONE - | _ => NONE) -| split_conj2 _ _ = NONE; - -fun transform_prem1 ctxt names thm = - map_thm ctxt (split_conj1 names) (etac conjunct1 1) thm - -fun transform_prem2 ctxt names thm = - map_thm ctxt (split_conj2 names) (etac conjunct2 1) thm - - -(* transformes a theorem into one of the object logic *) -val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars - -end (* structure *) - -open Nominal_Library; \ No newline at end of file diff -r 41137dc935ff -r 8193bbaa07fe Nominal-General/nominal_permeq.ML --- a/Nominal-General/nominal_permeq.ML Sun Nov 14 12:09:14 2010 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,174 +0,0 @@ -(* Title: nominal_permeq.ML - Author: Christian Urban - Author: Brian Huffman -*) - -signature NOMINAL_PERMEQ = -sig - val eqvt_tac: Proof.context -> thm list -> string list -> int -> tactic - val eqvt_strict_tac: Proof.context -> thm list -> string list -> int -> tactic - - val perm_simp_meth: thm list * string list -> Proof.context -> Method.method - val perm_strict_simp_meth: thm list * string list -> Proof.context -> Method.method - val args_parser: (thm list * string list) context_parser - - val trace_eqvt: bool Config.T - val setup: theory -> theory -end; - -(* - -- eqvt_tac and eqvt_strict_tac take a list of theorems - which are first tried to simplify permutations - - the string list contains constants that should not be - analysed (for example there is no raw eqvt-lemma for - the constant The); therefore it should not be analysed - -- setting [[trace_eqvt = true]] switches on tracing - information - -*) - -structure Nominal_Permeq: NOMINAL_PERMEQ = -struct - -open Nominal_ThmDecls; - -(* tracing infrastructure *) -val (trace_eqvt, trace_eqvt_setup) = Attrib.config_bool "trace_eqvt" (K false); - -fun trace_enabled ctxt = Config.get ctxt trace_eqvt - -fun trace_msg ctxt result = - let - val lhs_str = Syntax.string_of_term ctxt (term_of (Thm.lhs_of result)) - val rhs_str = Syntax.string_of_term ctxt (term_of (Thm.rhs_of result)) - in - warning (Pretty.string_of (Pretty.strs ["Rewriting", lhs_str, "to", rhs_str])) - end - -fun trace_conv ctxt conv ctrm = - let - val result = conv ctrm - in - if Thm.is_reflexive result - then result - else (trace_msg ctxt result; result) - end - -(* this conversion always fails, but prints - out the analysed term *) -fun trace_info_conv ctxt ctrm = - let - val trm = term_of ctrm - val _ = case (head_of trm) of - @{const "Trueprop"} => () - | _ => warning ("Analysing term " ^ Syntax.string_of_term ctxt trm) - in - Conv.no_conv ctrm - end - -(* conversion for applications *) -fun eqvt_apply_conv ctrm = - case (term_of ctrm) of - Const (@{const_name "permute"}, _) $ _ $ (_ $ _) => - let - val (perm, t) = Thm.dest_comb ctrm - val (_, p) = Thm.dest_comb perm - val (f, x) = Thm.dest_comb t - val a = ctyp_of_term x; - val b = ctyp_of_term t; - val ty_insts = map SOME [b, a] - val term_insts = map SOME [p, f, x] - in - Drule.instantiate' ty_insts term_insts @{thm eqvt_apply} - end - | _ => Conv.no_conv ctrm - -(* conversion for lambdas *) -fun eqvt_lambda_conv ctrm = - case (term_of ctrm) of - Const (@{const_name "permute"}, _) $ _ $ (Abs _) => - Conv.rewr_conv @{thm eqvt_lambda} ctrm - | _ => Conv.no_conv ctrm - - -(* conversion that raises an error or prints a warning message, - if a permutation on a constant or application cannot be analysed *) - -fun is_excluded excluded (Const (a, _)) = member (op=) excluded a - | is_excluded _ _ = false - -fun progress_info_conv ctxt strict_flag excluded ctrm = - let - fun msg trm = - if is_excluded excluded trm then () else - (if strict_flag then error else warning) - ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm)) - - val _ = case (term_of ctrm) of - Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm - | Const (@{const_name "permute"}, _) $ _ $ (trm as _ $ _) => msg trm - | _ => () - in - Conv.all_conv ctrm - end - -(* main conversion *) -fun eqvt_conv ctxt strict_flag user_thms excluded ctrm = - let - val first_conv_wrapper = - if trace_enabled ctxt - then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt)) - else Conv.first_conv - - val pre_thms = map safe_mk_equiv user_thms @ @{thms eqvt_bound} @ get_eqvts_raw_thms ctxt - val post_thms = map safe_mk_equiv @{thms permute_pure} - in - first_conv_wrapper - [ Conv.rewrs_conv pre_thms, - eqvt_apply_conv, - eqvt_lambda_conv, - Conv.rewrs_conv post_thms, - progress_info_conv ctxt strict_flag excluded - ] ctrm - end - -(* the eqvt-tactics first eta-normalise goals in - order to avoid problems with inductions in the - equivaraince command. *) - -(* raises an error if some permutations cannot be eliminated *) -fun eqvt_strict_tac ctxt user_thms excluded = - CONVERSION (Conv.top_conv - (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt true user_thms excluded)) ctxt) - -(* prints a warning message if some permutations cannot be eliminated *) -fun eqvt_tac ctxt user_thms excluded = - CONVERSION (Conv.top_conv - (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt false user_thms excluded)) ctxt) - -(* setup of the configuration value *) -val setup = - trace_eqvt_setup - - -(** methods **) -fun unless_more_args scan = Scan.unless (Scan.lift ((Args.$$$ "exclude") -- Args.colon)) scan - -val add_thms_parser = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- - Scan.repeat (unless_more_args Attrib.multi_thm) >> flat) []; - -val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- - (Scan.repeat (Args.const true))) [] - -val args_parser = add_thms_parser -- exclude_consts_parser - -fun perm_simp_meth (thms, consts) ctxt = - SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt thms consts)) - -fun perm_strict_simp_meth (thms, consts) ctxt = - SIMPLE_METHOD (HEADGOAL (eqvt_strict_tac ctxt thms consts)) - -end; (* structure *) diff -r 41137dc935ff -r 8193bbaa07fe Nominal-General/nominal_thmdecls.ML --- a/Nominal-General/nominal_thmdecls.ML Sun Nov 14 12:09:14 2010 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,237 +0,0 @@ -(* Title: nominal_thmdecls.ML - Author: Christian Urban - - Infrastructure for the lemma collection "eqvts". - - Provides the attributes [eqvt] and [eqvt_raw], and the theorem - lists eqvts and eqvts_raw. The first attribute will store the - theorem in the eqvts list and also in the eqvts_raw list. For - the latter the theorem is expected to be of the form - - p o (c x1 x2 ...) = c (p o x1) (p o x2) ... (1) - - or - - c x1 x2 ... ==> c (p o x1) (p o x2) ... (2) - - and it is stored in the form - - p o c == c - - The [eqvt_raw] attribute just adds the theorem to eqvts_raw. - - TODO: In case of the form in (2) one should also - add the equational form to eqvts -*) - -signature NOMINAL_THMDECLS = -sig - val eqvt_add: attribute - val eqvt_del: attribute - val eqvt_raw_add: attribute - val eqvt_raw_del: attribute - val setup: theory -> theory - val get_eqvts_thms: Proof.context -> thm list - val get_eqvts_raw_thms: Proof.context -> thm list - val eqvt_transform: Proof.context -> thm -> thm - val is_eqvt: Proof.context -> term -> bool -end; - -structure Nominal_ThmDecls: NOMINAL_THMDECLS = -struct - -structure EqvtData = Generic_Data -( type T = thm Item_Net.T; - val empty = Thm.full_rules; - val extend = I; - val merge = Item_Net.merge); - -structure EqvtRawData = Generic_Data -( type T = thm Termtab.table; - val empty = Termtab.empty; - val extend = I; - val merge = Termtab.merge (K true)); - -val eqvts = Item_Net.content o EqvtData.get; -val eqvts_raw = map snd o Termtab.dest o EqvtRawData.get; - -val get_eqvts_thms = eqvts o Context.Proof; -val get_eqvts_raw_thms = eqvts_raw o Context.Proof; - -val add_thm = EqvtData.map o Item_Net.update; -val del_thm = EqvtData.map o Item_Net.remove; - -fun add_raw_thm thm = - case prop_of thm of - Const ("==", _) $ _ $ (c as Const _) => EqvtRawData.map (Termtab.update (c, thm)) - | _ => raise THM ("Theorem must be a meta-equality where the right-hand side is a constant.", 0, [thm]) - -fun del_raw_thm thm = - case prop_of thm of - Const ("==", _) $ _ $ (c as Const _) => EqvtRawData.map (Termtab.delete c) - | _ => raise THM ("Theorem must be a meta-equality where the right-hand side is a constant.", 0, [thm]) - -fun is_eqvt ctxt trm = - case trm of - (c as Const _) => Termtab.defined (EqvtRawData.get (Context.Proof ctxt)) c - | _ => raise TERM ("Term must be a constsnt.", [trm]) - - - -(** transformation of eqvt lemmas **) - -fun get_perms trm = - case trm of - Const (@{const_name permute}, _) $ _ $ (Bound _) => - raise TERM ("get_perms called on bound", [trm]) - | Const (@{const_name permute}, _) $ p $ _ => [p] - | t $ u => get_perms t @ get_perms u - | Abs (_, _, t) => get_perms t - | _ => [] - -fun put_perm p trm = - case trm of - Bound _ => trm - | Const _ => trm - | t $ u => put_perm p t $ put_perm p u - | Abs (x, ty, t) => Abs (x, ty, put_perm p t) - | _ => mk_perm p trm - -(* tests whether there is a disagreement between the permutations, - and that there is at least one permutation *) -fun is_bad_list [] = true - | is_bad_list [_] = false - | is_bad_list (p::q::ps) = if p = q then is_bad_list (q::ps) else true - - -(* transforms equations into the "p o c == c"-form - from p o (c x1 ...xn) = c (p o x1) ... (p o xn) *) - -fun eqvt_transform_eq_tac thm = -let - val ss_thms = @{thms permute_minus_cancel permute_prod.simps split_paired_all} -in - REPEAT o FIRST' - [CHANGED o simp_tac (HOL_basic_ss addsimps ss_thms), - rtac (thm RS @{thm trans}), - rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}] -end - -fun eqvt_transform_eq ctxt thm = - let - val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm)) - handle TERM _ => error "Equivariance lemma must be an equality." - val (p, t) = dest_perm lhs - handle TERM _ => error "Equivariance lemma is not of the form p \ c... = c..." - - val ps = get_perms rhs handle TERM _ => [] - val (c, c') = (head_of t, head_of rhs) - val msg = "Equivariance lemma is not of the right form " - in - if c <> c' - then error (msg ^ "(constants do not agree).") - else if is_bad_list (p :: ps) - then error (msg ^ "(permutations do not agree).") - else if not (rhs aconv (put_perm p t)) - then error (msg ^ "(arguments do not agree).") - else if is_Const t - then safe_mk_equiv thm - else - let - val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c)) - val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt - in - Goal.prove ctxt [] [] goal' (fn _ => eqvt_transform_eq_tac thm 1) - |> singleton (ProofContext.export ctxt' ctxt) - |> safe_mk_equiv - |> zero_var_indexes - end - end - -(* transforms equations into the "p o c == c"-form - from R x1 ...xn ==> R (p o x1) ... (p o xn) *) - -fun eqvt_transform_imp_tac ctxt p p' thm = - let - val thy = ProofContext.theory_of ctxt - val cp = Thm.cterm_of thy p - val cp' = Thm.cterm_of thy (mk_minus p') - val thm' = Drule.cterm_instantiate [(cp, cp')] thm - val simp = HOL_basic_ss addsimps @{thms permute_minus_cancel(2)} - in - EVERY' [rtac @{thm iffI}, dtac @{thm permute_boolE}, rtac thm, atac, - rtac @{thm permute_boolI}, dtac thm', full_simp_tac simp] - end - -fun eqvt_transform_imp ctxt thm = - let - val (prem, concl) = pairself HOLogic.dest_Trueprop (Logic.dest_implies (prop_of thm)) - val (c, c') = (head_of prem, head_of concl) - val ps = get_perms concl handle TERM _ => [] - val p = try hd ps - val msg = "Equivariance lemma is not of the right form " - in - if c <> c' - then error (msg ^ "(constants do not agree).") - else if is_bad_list ps - then error (msg ^ "(permutations do not agree).") - else if not (concl aconv (put_perm (the p) prem)) - then error (msg ^ "(arguments do not agree).") - else - let - val prem' = mk_perm (the p) prem - val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (prem', concl)) - val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt - in - Goal.prove ctxt' [] [] goal' - (fn _ => eqvt_transform_imp_tac ctxt' (the p) p' thm 1) - |> singleton (ProofContext.export ctxt' ctxt) - end - end - -fun eqvt_transform ctxt thm = - case (prop_of thm) of - @{const "Trueprop"} $ (Const (@{const_name "HOL.eq"}, _) $ - (Const (@{const_name "permute"}, _) $ _ $ _) $ _) => - eqvt_transform_eq ctxt thm - | @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) => - eqvt_transform_imp ctxt thm |> eqvt_transform_eq ctxt - | _ => raise error "Only _ = _ and _ ==> _ cases are implemented." - - -(** attributes **) - -val eqvt_add = Thm.declaration_attribute - (fn thm => fn context => - let - val thm' = eqvt_transform (Context.proof_of context) thm - in - context |> add_thm thm |> add_raw_thm thm' - end) - -val eqvt_del = Thm.declaration_attribute - (fn thm => fn context => - let - val thm' = eqvt_transform (Context.proof_of context) thm - in - context |> del_thm thm |> del_raw_thm thm' - end) - -val eqvt_raw_add = Thm.declaration_attribute add_raw_thm; -val eqvt_raw_del = Thm.declaration_attribute del_raw_thm; - - -(** setup function **) - -val setup = - Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) - (cat_lines ["Declaration of equivariance lemmas - they will automtically be", - "brought into the form p o c == c"]) #> - Attrib.setup @{binding "eqvt_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_del) - (cat_lines ["Declaration of equivariance lemmas - no", - "transformation is performed"]) #> - Global_Theory.add_thms_dynamic (@{binding "eqvts"}, eqvts) #> - Global_Theory.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw); - - -end; diff -r 41137dc935ff -r 8193bbaa07fe Nominal/Abs.thy --- a/Nominal/Abs.thy Sun Nov 14 12:09:14 2010 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,587 +0,0 @@ -theory Abs -imports "../Nominal-General/Nominal2_Base" - "../Nominal-General/Nominal2_Eqvt" - "Quotient" - "Quotient_List" - "Quotient_Product" -begin - - -section {* Abstractions *} - -fun - alpha_set -where - alpha_set[simp del]: - "alpha_set (bs, x) R f pi (cs, y) \ - f x - bs = f y - cs \ - (f x - bs) \* pi \ - R (pi \ x) y \ - pi \ bs = cs" - -fun - alpha_res -where - alpha_res[simp del]: - "alpha_res (bs, x) R f pi (cs, y) \ - f x - bs = f y - cs \ - (f x - bs) \* pi \ - R (pi \ x) y" - -fun - alpha_lst -where - alpha_lst[simp del]: - "alpha_lst (bs, x) R f pi (cs, y) \ - f x - set bs = f y - set cs \ - (f x - set bs) \* pi \ - R (pi \ x) y \ - pi \ bs = cs" - -lemmas alphas = alpha_set.simps alpha_res.simps alpha_lst.simps - -notation - alpha_set ("_ \set _ _ _ _" [100, 100, 100, 100, 100] 100) and - alpha_res ("_ \res _ _ _ _" [100, 100, 100, 100, 100] 100) and - alpha_lst ("_ \lst _ _ _ _" [100, 100, 100, 100, 100] 100) - -section {* Mono *} - -lemma [mono]: - shows "R1 \ R2 \ alpha_set bs R1 \ alpha_set bs R2" - and "R1 \ R2 \ alpha_res bs R1 \ alpha_res bs R2" - and "R1 \ R2 \ alpha_lst cs R1 \ alpha_lst cs R2" - by (case_tac [!] bs, case_tac [!] cs) - (auto simp add: le_fun_def le_bool_def alphas) - -section {* Equivariance *} - -lemma alpha_eqvt[eqvt]: - shows "(bs, x) \set R f q (cs, y) \ (p \ bs, p \ x) \set (p \ R) (p \ f) (p \ q) (p \ cs, p \ y)" - and "(bs, x) \res R f q (cs, y) \ (p \ bs, p \ x) \res (p \ R) (p \ f) (p \ q) (p \ cs, p \ y)" - and "(ds, x) \lst R f q (es, y) \ (p \ ds, p \ x) \lst (p \ R) (p \ f) (p \ q) (p \ es, p \ y)" - unfolding alphas - unfolding permute_eqvt[symmetric] - unfolding set_eqvt[symmetric] - unfolding permute_fun_app_eq[symmetric] - unfolding Diff_eqvt[symmetric] - by (auto simp add: permute_bool_def fresh_star_permute_iff) - - -section {* Equivalence *} - -lemma alpha_refl: - assumes a: "R x x" - shows "(bs, x) \set R f 0 (bs, x)" - and "(bs, x) \res R f 0 (bs, x)" - and "(cs, x) \lst R f 0 (cs, x)" - using a - unfolding alphas - unfolding fresh_star_def - by (simp_all add: fresh_zero_perm) - -lemma alpha_sym: - assumes a: "R (p \ x) y \ R (- p \ y) x" - shows "(bs, x) \set R f p (cs, y) \ (cs, y) \set R f (- p) (bs, x)" - and "(bs, x) \res R f p (cs, y) \ (cs, y) \res R f (- p) (bs, x)" - and "(ds, x) \lst R f p (es, y) \ (es, y) \lst R f (- p) (ds, x)" - unfolding alphas fresh_star_def - using a - by (auto simp add: fresh_minus_perm) - -lemma alpha_trans: - assumes a: "\R (p \ x) y; R (q \ y) z\ \ R ((q + p) \ x) z" - shows "\(bs, x) \set R f p (cs, y); (cs, y) \set R f q (ds, z)\ \ (bs, x) \set R f (q + p) (ds, z)" - and "\(bs, x) \res R f p (cs, y); (cs, y) \res R f q (ds, z)\ \ (bs, x) \res R f (q + p) (ds, z)" - and "\(es, x) \lst R f p (gs, y); (gs, y) \lst R f q (hs, z)\ \ (es, x) \lst R f (q + p) (hs, z)" - using a - unfolding alphas fresh_star_def - by (simp_all add: fresh_plus_perm) - -lemma alpha_sym_eqvt: - assumes a: "R (p \ x) y \ R y (p \ x)" - and b: "p \ R = R" - shows "(bs, x) \set R f p (cs, y) \ (cs, y) \set R f (- p) (bs, x)" - and "(bs, x) \res R f p (cs, y) \ (cs, y) \res R f (- p) (bs, x)" - and "(ds, x) \lst R f p (es, y) \ (es, y) \lst R f (- p) (ds, x)" -apply(auto intro!: alpha_sym) -apply(drule_tac [!] a) -apply(rule_tac [!] p="p" in permute_boolE) -apply(perm_simp add: permute_minus_cancel b) -apply(assumption) -apply(perm_simp add: permute_minus_cancel b) -apply(assumption) -apply(perm_simp add: permute_minus_cancel b) -apply(assumption) -done - -lemma alpha_set_trans_eqvt: - assumes b: "(cs, y) \set R f q (ds, z)" - and a: "(bs, x) \set R f p (cs, y)" - and d: "q \ R = R" - and c: "\R (p \ x) y; R y (- q \ z)\ \ R (p \ x) (- q \ z)" - shows "(bs, x) \set R f (q + p) (ds, z)" -apply(rule alpha_trans) -defer -apply(rule a) -apply(rule b) -apply(drule c) -apply(rule_tac p="q" in permute_boolE) -apply(perm_simp add: permute_minus_cancel d) -apply(assumption) -apply(rotate_tac -1) -apply(drule_tac p="q" in permute_boolI) -apply(perm_simp add: permute_minus_cancel d) -apply(simp add: permute_eqvt[symmetric]) -done - -lemma alpha_res_trans_eqvt: - assumes b: "(cs, y) \res R f q (ds, z)" - and a: "(bs, x) \res R f p (cs, y)" - and d: "q \ R = R" - and c: "\R (p \ x) y; R y (- q \ z)\ \ R (p \ x) (- q \ z)" - shows "(bs, x) \res R f (q + p) (ds, z)" -apply(rule alpha_trans) -defer -apply(rule a) -apply(rule b) -apply(drule c) -apply(rule_tac p="q" in permute_boolE) -apply(perm_simp add: permute_minus_cancel d) -apply(assumption) -apply(rotate_tac -1) -apply(drule_tac p="q" in permute_boolI) -apply(perm_simp add: permute_minus_cancel d) -apply(simp add: permute_eqvt[symmetric]) -done - -lemma alpha_lst_trans_eqvt: - assumes b: "(cs, y) \lst R f q (ds, z)" - and a: "(bs, x) \lst R f p (cs, y)" - and d: "q \ R = R" - and c: "\R (p \ x) y; R y (- q \ z)\ \ R (p \ x) (- q \ z)" - shows "(bs, x) \lst R f (q + p) (ds, z)" -apply(rule alpha_trans) -defer -apply(rule a) -apply(rule b) -apply(drule c) -apply(rule_tac p="q" in permute_boolE) -apply(perm_simp add: permute_minus_cancel d) -apply(assumption) -apply(rotate_tac -1) -apply(drule_tac p="q" in permute_boolI) -apply(perm_simp add: permute_minus_cancel d) -apply(simp add: permute_eqvt[symmetric]) -done - -lemmas alpha_trans_eqvt = alpha_set_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt - - -section {* General Abstractions *} - -fun - alpha_abs_set -where - [simp del]: - "alpha_abs_set (bs, x) (cs, y) \ (\p. (bs, x) \set (op=) supp p (cs, y))" - -fun - alpha_abs_lst -where - [simp del]: - "alpha_abs_lst (bs, x) (cs, y) \ (\p. (bs, x) \lst (op=) supp p (cs, y))" - -fun - alpha_abs_res -where - [simp del]: - "alpha_abs_res (bs, x) (cs, y) \ (\p. (bs, x) \res (op=) supp p (cs, y))" - -notation - alpha_abs_set (infix "\abs'_set" 50) and - alpha_abs_lst (infix "\abs'_lst" 50) and - alpha_abs_res (infix "\abs'_res" 50) - -lemmas alphas_abs = alpha_abs_set.simps alpha_abs_res.simps alpha_abs_lst.simps - - -lemma alphas_abs_refl: - shows "(bs, x) \abs_set (bs, x)" - and "(bs, x) \abs_res (bs, x)" - and "(cs, x) \abs_lst (cs, x)" - unfolding alphas_abs - unfolding alphas - unfolding fresh_star_def - by (rule_tac [!] x="0" in exI) - (simp_all add: fresh_zero_perm) - -lemma alphas_abs_sym: - shows "(bs, x) \abs_set (cs, y) \ (cs, y) \abs_set (bs, x)" - and "(bs, x) \abs_res (cs, y) \ (cs, y) \abs_res (bs, x)" - and "(ds, x) \abs_lst (es, y) \ (es, y) \abs_lst (ds, x)" - unfolding alphas_abs - unfolding alphas - unfolding fresh_star_def - by (erule_tac [!] exE, rule_tac [!] x="-p" in exI) - (auto simp add: fresh_minus_perm) - -lemma alphas_abs_trans: - shows "\(bs, x) \abs_set (cs, y); (cs, y) \abs_set (ds, z)\ \ (bs, x) \abs_set (ds, z)" - and "\(bs, x) \abs_res (cs, y); (cs, y) \abs_res (ds, z)\ \ (bs, x) \abs_res (ds, z)" - and "\(es, x) \abs_lst (gs, y); (gs, y) \abs_lst (hs, z)\ \ (es, x) \abs_lst (hs, z)" - unfolding alphas_abs - unfolding alphas - unfolding fresh_star_def - apply(erule_tac [!] exE, erule_tac [!] exE) - apply(rule_tac [!] x="pa + p" in exI) - by (simp_all add: fresh_plus_perm) - -lemma alphas_abs_eqvt: - shows "(bs, x) \abs_set (cs, y) \ (p \ bs, p \ x) \abs_set (p \ cs, p \ y)" - and "(bs, x) \abs_res (cs, y) \ (p \ bs, p \ x) \abs_res (p \ cs, p \ y)" - and "(ds, x) \abs_lst (es, y) \ (p \ ds, p \ x) \abs_lst (p \ es, p \ y)" - unfolding alphas_abs - unfolding alphas - unfolding set_eqvt[symmetric] - unfolding supp_eqvt[symmetric] - unfolding Diff_eqvt[symmetric] - apply(erule_tac [!] exE) - apply(rule_tac [!] x="p \ pa" in exI) - by (auto simp add: fresh_star_permute_iff permute_eqvt[symmetric]) - -quotient_type - 'a abs_set = "(atom set \ 'a::pt)" / "alpha_abs_set" -and 'b abs_res = "(atom set \ 'b::pt)" / "alpha_abs_res" -and 'c abs_lst = "(atom list \ 'c::pt)" / "alpha_abs_lst" - apply(rule_tac [!] equivpI) - unfolding reflp_def symp_def transp_def - by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:) - -quotient_definition - Abs_set ("[_]set. _" [60, 60] 60) -where - "Abs_set::atom set \ ('a::pt) \ 'a abs_set" -is - "Pair::atom set \ ('a::pt) \ (atom set \ 'a)" - -quotient_definition - Abs_res ("[_]res. _" [60, 60] 60) -where - "Abs_res::atom set \ ('a::pt) \ 'a abs_res" -is - "Pair::atom set \ ('a::pt) \ (atom set \ 'a)" - -quotient_definition - Abs_lst ("[_]lst. _" [60, 60] 60) -where - "Abs_lst::atom list \ ('a::pt) \ 'a abs_lst" -is - "Pair::atom list \ ('a::pt) \ (atom list \ 'a)" - -lemma [quot_respect]: - shows "(op= ===> op= ===> alpha_abs_set) Pair Pair" - and "(op= ===> op= ===> alpha_abs_res) Pair Pair" - and "(op= ===> op= ===> alpha_abs_lst) Pair Pair" - unfolding fun_rel_def - by (auto intro: alphas_abs_refl) - -lemma [quot_respect]: - shows "(op= ===> alpha_abs_set ===> alpha_abs_set) permute permute" - and "(op= ===> alpha_abs_res ===> alpha_abs_res) permute permute" - and "(op= ===> alpha_abs_lst ===> alpha_abs_lst) permute permute" - unfolding fun_rel_def - by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt) - -lemma Abs_eq_iff: - shows "Abs_set bs x = Abs_set cs y \ (\p. (bs, x) \set (op =) supp p (cs, y))" - and "Abs_res bs x = Abs_res cs y \ (\p. (bs, x) \res (op =) supp p (cs, y))" - and "Abs_lst bsl x = Abs_lst csl y \ (\p. (bsl, x) \lst (op =) supp p (csl, y))" - by (lifting alphas_abs) - -lemma Abs_exhausts: - shows "(\as (x::'a::pt). y1 = Abs_set as x \ P1) \ P1" - and "(\as (x::'a::pt). y2 = Abs_res as x \ P2) \ P2" - and "(\as (x::'a::pt). y3 = Abs_lst as x \ P3) \ P3" - by (lifting prod.exhaust[where 'a="atom set" and 'b="'a"] - prod.exhaust[where 'a="atom set" and 'b="'a"] - prod.exhaust[where 'a="atom list" and 'b="'a"]) - -instantiation abs_set :: (pt) pt -begin - -quotient_definition - "permute_abs_set::perm \ ('a::pt abs_set) \ 'a abs_set" -is - "permute:: perm \ (atom set \ 'a::pt) \ (atom set \ 'a::pt)" - -lemma permute_Abs_set[simp]: - fixes x::"'a::pt" - shows "(p \ (Abs_set as x)) = Abs_set (p \ as) (p \ x)" - by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"]) - -instance - apply(default) - apply(case_tac [!] x rule: Abs_exhausts(1)) - apply(simp_all) - done - -end - -instantiation abs_res :: (pt) pt -begin - -quotient_definition - "permute_abs_res::perm \ ('a::pt abs_res) \ 'a abs_res" -is - "permute:: perm \ (atom set \ 'a::pt) \ (atom set \ 'a::pt)" - -lemma permute_Abs_res[simp]: - fixes x::"'a::pt" - shows "(p \ (Abs_res as x)) = Abs_res (p \ as) (p \ x)" - by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"]) - -instance - apply(default) - apply(case_tac [!] x rule: Abs_exhausts(2)) - apply(simp_all) - done - -end - -instantiation abs_lst :: (pt) pt -begin - -quotient_definition - "permute_abs_lst::perm \ ('a::pt abs_lst) \ 'a abs_lst" -is - "permute:: perm \ (atom list \ 'a::pt) \ (atom list \ 'a::pt)" - -lemma permute_Abs_lst[simp]: - fixes x::"'a::pt" - shows "(p \ (Abs_lst as x)) = Abs_lst (p \ as) (p \ x)" - by (lifting permute_prod.simps[where 'a="atom list" and 'b="'a"]) - -instance - apply(default) - apply(case_tac [!] x rule: Abs_exhausts(3)) - apply(simp_all) - done - -end - -lemmas permute_Abs[eqvt] = permute_Abs_set permute_Abs_res permute_Abs_lst - - -lemma Abs_swap1: - assumes a1: "a \ (supp x) - bs" - and a2: "b \ (supp x) - bs" - shows "Abs_set bs x = Abs_set ((a \ b) \ bs) ((a \ b) \ x)" - and "Abs_res bs x = Abs_res ((a \ b) \ bs) ((a \ b) \ x)" - unfolding Abs_eq_iff - unfolding alphas - unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] - unfolding fresh_star_def fresh_def - unfolding swap_set_not_in[OF a1 a2] - using a1 a2 - by (rule_tac [!] x="(a \ b)" in exI) - (auto simp add: supp_perm swap_atom) - -lemma Abs_swap2: - assumes a1: "a \ (supp x) - (set bs)" - and a2: "b \ (supp x) - (set bs)" - shows "Abs_lst bs x = Abs_lst ((a \ b) \ bs) ((a \ b) \ x)" - unfolding Abs_eq_iff - unfolding alphas - unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric] - unfolding fresh_star_def fresh_def - unfolding swap_set_not_in[OF a1 a2] - using a1 a2 - by (rule_tac [!] x="(a \ b)" in exI) - (auto simp add: supp_perm swap_atom) - -lemma Abs_supports: - shows "((supp x) - as) supports (Abs_set as x)" - and "((supp x) - as) supports (Abs_res as x)" - and "((supp x) - set bs) supports (Abs_lst bs x)" - unfolding supports_def - unfolding permute_Abs - by (simp_all add: Abs_swap1[symmetric] Abs_swap2[symmetric]) - -function - supp_set :: "('a::pt) abs_set \ atom set" -where - "supp_set (Abs_set as x) = supp x - as" -apply(case_tac x rule: Abs_exhausts(1)) -apply(simp) -apply(simp add: Abs_eq_iff alphas_abs alphas) -done - -termination supp_set - by (auto intro!: local.termination) - -function - supp_res :: "('a::pt) abs_res \ atom set" -where - "supp_res (Abs_res as x) = supp x - as" -apply(case_tac x rule: Abs_exhausts(2)) -apply(simp) -apply(simp add: Abs_eq_iff alphas_abs alphas) -done - -termination supp_res - by (auto intro!: local.termination) - -function - supp_lst :: "('a::pt) abs_lst \ atom set" -where - "supp_lst (Abs_lst cs x) = (supp x) - (set cs)" -apply(case_tac x rule: Abs_exhausts(3)) -apply(simp) -apply(simp add: Abs_eq_iff alphas_abs alphas) -done - -termination supp_lst - by (auto intro!: local.termination) - -lemma [eqvt]: - shows "(p \ supp_set x) = supp_set (p \ x)" - and "(p \ supp_res y) = supp_res (p \ y)" - and "(p \ supp_lst z) = supp_lst (p \ z)" - apply(case_tac x rule: Abs_exhausts(1)) - apply(simp add: supp_eqvt Diff_eqvt) - apply(case_tac y rule: Abs_exhausts(2)) - apply(simp add: supp_eqvt Diff_eqvt) - apply(case_tac z rule: Abs_exhausts(3)) - apply(simp add: supp_eqvt Diff_eqvt set_eqvt) - done - -lemma Abs_fresh_aux: - shows "a \ Abs bs x \ a \ supp_set (Abs bs x)" - and "a \ Abs_res bs x \ a \ supp_res (Abs_res bs x)" - and "a \ Abs_lst cs x \ a \ supp_lst (Abs_lst cs x)" - by (rule_tac [!] fresh_fun_eqvt_app) - (simp_all only: eqvts_raw) - -lemma Abs_supp_subset1: - assumes a: "finite (supp x)" - shows "(supp x) - as \ supp (Abs_set as x)" - and "(supp x) - as \ supp (Abs_res as x)" - and "(supp x) - (set bs) \ supp (Abs_lst bs x)" - unfolding supp_conv_fresh - by (auto dest!: Abs_fresh_aux) - (simp_all add: fresh_def supp_finite_atom_set a) - -lemma Abs_supp_subset2: - assumes a: "finite (supp x)" - shows "supp (Abs_set as x) \ (supp x) - as" - and "supp (Abs_res as x) \ (supp x) - as" - and "supp (Abs_lst bs x) \ (supp x) - (set bs)" - by (rule_tac [!] supp_is_subset) - (simp_all add: Abs_supports a) - -lemma Abs_finite_supp: - assumes a: "finite (supp x)" - shows "supp (Abs_set as x) = (supp x) - as" - and "supp (Abs_res as x) = (supp x) - as" - and "supp (Abs_lst bs x) = (supp x) - (set bs)" - by (rule_tac [!] subset_antisym) - (simp_all add: Abs_supp_subset1[OF a] Abs_supp_subset2[OF a]) - -lemma supp_Abs: - fixes x::"'a::fs" - shows "supp (Abs_set as x) = (supp x) - as" - and "supp (Abs_res as x) = (supp x) - as" - and "supp (Abs_lst bs x) = (supp x) - (set bs)" - by (rule_tac [!] Abs_finite_supp) - (simp_all add: finite_supp) - -instance abs_set :: (fs) fs - apply(default) - apply(case_tac x rule: Abs_exhausts(1)) - apply(simp add: supp_Abs finite_supp) - done - -instance abs_res :: (fs) fs - apply(default) - apply(case_tac x rule: Abs_exhausts(2)) - apply(simp add: supp_Abs finite_supp) - done - -instance abs_lst :: (fs) fs - apply(default) - apply(case_tac x rule: Abs_exhausts(3)) - apply(simp add: supp_Abs finite_supp) - done - -lemma Abs_fresh_iff: - fixes x::"'a::fs" - shows "a \ Abs_set bs x \ a \ bs \ (a \ bs \ a \ x)" - and "a \ Abs_res bs x \ a \ bs \ (a \ bs \ a \ x)" - and "a \ Abs_lst cs x \ a \ (set cs) \ (a \ (set cs) \ a \ x)" - unfolding fresh_def - unfolding supp_Abs - by auto - -lemma Abs_fresh_star: - fixes x::"'a::fs" - shows "as \* Abs_set as x" - and "as \* Abs_res as x" - and "set bs \* Abs_lst bs x" - unfolding fresh_star_def - by(simp_all add: Abs_fresh_iff) - - -section {* Infrastructure for building tuples of relations and functions *} - -fun - prod_fv :: "('a \ atom set) \ ('b \ atom set) \ ('a \ 'b) \ atom set" -where - "prod_fv fv1 fv2 (x, y) = fv1 x \ fv2 y" - -definition - prod_alpha :: "('a \ 'a \ bool) \ ('b \ 'b \ bool) \ ('a \ 'b \ 'a \ 'b \ bool)" -where - "prod_alpha = prod_rel" - -lemma [quot_respect]: - shows "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv" - unfolding fun_rel_def - unfolding prod_rel_def - by auto - -lemma [quot_preserve]: - assumes q1: "Quotient R1 abs1 rep1" - and q2: "Quotient R2 abs2 rep2" - shows "((abs1 ---> id) ---> (abs2 ---> id) ---> prod_fun rep1 rep2 ---> id) prod_fv = prod_fv" - by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) - -lemma [mono]: - shows "A <= B \ C <= D ==> prod_alpha A C <= prod_alpha B D" - unfolding prod_alpha_def - by auto - -lemma [eqvt]: - shows "p \ prod_alpha A B x y = prod_alpha (p \ A) (p \ B) (p \ x) (p \ y)" - unfolding prod_alpha_def - unfolding prod_rel_def - by (perm_simp) (rule refl) - -lemma [eqvt]: - shows "p \ prod_fv A B (x, y) = prod_fv (p \ A) (p \ B) (p \ x, p \ y)" - unfolding prod_fv.simps - by (perm_simp) (rule refl) - -lemma prod_fv_supp: - shows "prod_fv supp supp = supp" -by (rule ext) - (auto simp add: prod_fv.simps supp_Pair) - -lemma prod_alpha_eq: - shows "prod_alpha (op=) (op=) = (op=)" -unfolding prod_alpha_def -by (auto intro!: ext) - - -end - diff -r 41137dc935ff -r 8193bbaa07fe Nominal/Atoms.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Atoms.thy Sun Nov 14 16:34:47 2010 +0000 @@ -0,0 +1,222 @@ +(* Title: Atoms + Authors: Brian Huffman, Christian Urban + + Instantiations of concrete atoms +*) +theory Atoms +imports Nominal2_Base +uses "~~/src/Tools/subtyping.ML" +begin + + + +section {* @{const nat_of} is an example of a function + without finite support *} + + +lemma not_fresh_nat_of: + shows "\ a \ nat_of" +unfolding fresh_def supp_def +proof (clarsimp) + assume "finite {b. (a \ b) \ nat_of \ nat_of}" + hence "finite ({a} \ {b. (a \ b) \ nat_of \ nat_of})" + by simp + then obtain b where + b1: "b \ a" and + b2: "sort_of b = sort_of a" and + b3: "(a \ b) \ nat_of = nat_of" + by (rule obtain_atom) auto + have "nat_of a = (a \ b) \ (nat_of a)" by (simp add: permute_nat_def) + also have "\ = ((a \ b) \ nat_of) ((a \ b) \ a)" by (simp add: permute_fun_app_eq) + also have "\ = nat_of ((a \ b) \ a)" using b3 by simp + also have "\ = nat_of b" using b2 by simp + finally have "nat_of a = nat_of b" by simp + with b2 have "a = b" by (simp add: atom_components_eq_iff) + with b1 show "False" by simp +qed + +lemma supp_nat_of: + shows "supp nat_of = UNIV" + using not_fresh_nat_of [unfolded fresh_def] by auto + + +section {* Manual instantiation of class @{text at}. *} + +typedef (open) name = "{a. sort_of a = Sort ''name'' []}" +by (rule exists_eq_simple_sort) + +instantiation name :: at +begin + +definition + "p \ a = Abs_name (p \ Rep_name a)" + +definition + "atom a = Rep_name a" + +instance +apply (rule at_class) +apply (rule type_definition_name) +apply (rule atom_name_def) +apply (rule permute_name_def) +done + +end + +lemma sort_of_atom_name: + shows "sort_of (atom (a::name)) = Sort ''name'' []" + unfolding atom_name_def using Rep_name by simp + +text {* Custom syntax for concrete atoms of type at *} + +term "a:::name" + +text {* + a:::name stands for (atom a) with a being of concrete atom + type name. The above lemma can therefore also be stated as + + "sort_of (a:::name) = Sort ''name'' []" + + This does not work for multi-sorted atoms. +*} + + +section {* Automatic instantiation of class @{text at}. *} + +atom_decl name2 + +lemma sort_of_atom_name2: + "sort_of (atom (a::name2)) = Sort ''Atoms.name2'' []" +unfolding atom_name2_def +using Rep_name2 +by simp + +text {* example swappings *} +lemma + fixes a b::"atom" + assumes "sort_of a = sort_of b" + shows "(a \ b) \ (a, b) = (b, a)" +using assms +by simp + +lemma + fixes a b::"name2" + shows "(a \ b) \ (a, b) = (b, a)" +by simp + +section {* An example for multiple-sort atoms *} + +datatype ty = + TVar string +| Fun ty ty ("_ \ _") + +primrec + sort_of_ty::"ty \ atom_sort" +where + "sort_of_ty (TVar s) = Sort ''TVar'' [Sort s []]" +| "sort_of_ty (Fun ty1 ty2) = Sort ''Fun'' [sort_of_ty ty1, sort_of_ty ty2]" + +lemma sort_of_ty_eq_iff: + shows "sort_of_ty x = sort_of_ty y \ x = y" +apply(induct x arbitrary: y) +apply(case_tac [!] y) +apply(simp_all) +done + +declare sort_of_ty.simps [simp del] + +typedef (open) var = "{a. sort_of a \ range sort_of_ty}" + by (rule_tac x="Atom (sort_of_ty x) y" in exI, simp) + +instantiation var :: at_base +begin + +definition + "p \ a = Abs_var (p \ Rep_var a)" + +definition + "atom a = Rep_var a" + +instance +apply (rule at_base_class) +apply (rule type_definition_var) +apply (rule atom_var_def) +apply (rule permute_var_def) +done + +end + +text {* Constructor for variables. *} + +definition + Var :: "nat \ ty \ var" +where + "Var x t = Abs_var (Atom (sort_of_ty t) x)" + +lemma Var_eq_iff [simp]: + shows "Var x s = Var y t \ x = y \ s = t" + unfolding Var_def + by (auto simp add: Abs_var_inject sort_of_ty_eq_iff) + +lemma sort_of_atom_var [simp]: + "sort_of (atom (Var n ty)) = sort_of_ty ty" + unfolding atom_var_def Var_def + by (simp add: Abs_var_inverse) + +lemma + assumes "\ \ \" + shows "(Var x \ \ Var y \) \ (Var x \, Var x \) = (Var y \, Var x \)" + using assms by simp + +text {* Projecting out the type component of a variable. *} + +definition + ty_of :: "var \ ty" +where + "ty_of x = inv sort_of_ty (sort_of (atom x))" + +text {* + Functions @{term Var}/@{term ty_of} satisfy many of the same + properties as @{term Atom}/@{term sort_of}. +*} + +lemma ty_of_Var [simp]: + shows "ty_of (Var x t) = t" + unfolding ty_of_def + unfolding sort_of_atom_var + apply (rule inv_f_f) + apply (simp add: inj_on_def sort_of_ty_eq_iff) + done + +lemma ty_of_permute [simp]: + shows "ty_of (p \ x) = ty_of x" + unfolding ty_of_def + unfolding atom_eqvt [symmetric] + by simp + + +section {* Tests with subtyping and automatic coercions *} + +setup Subtyping.setup + +atom_decl var1 +atom_decl var2 + +declare [[coercion "atom::var1\atom"]] + +declare [[coercion "atom::var2\atom"]] + +lemma + fixes a::"var1" and b::"var2" + shows "a \ t \ b \ t" +oops + +(* does not yet work: it needs image as + coercion map *) + +lemma + fixes as::"var1 set" + shows "atom ` as \* t" +oops + +end diff -r 41137dc935ff -r 8193bbaa07fe Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Sun Nov 14 12:09:14 2010 +0000 +++ b/Nominal/Nominal2.thy Sun Nov 14 16:34:47 2010 +0000 @@ -1,8 +1,6 @@ theory Nominal2 imports - "../Nominal-General/Nominal2_Base" - "../Nominal-General/Nominal2_Eqvt" - "Abs" + Nominal2_Base Nominal2_Eqvt Nominal2_Abs uses ("nominal_dt_rawperm.ML") ("nominal_dt_rawfuns.ML") ("nominal_dt_alpha.ML") diff -r 41137dc935ff -r 8193bbaa07fe Nominal/Nominal2_Abs.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Nominal2_Abs.thy Sun Nov 14 16:34:47 2010 +0000 @@ -0,0 +1,587 @@ +theory Nominal2_Abs +imports "Nominal2_Base" + "Nominal2_Eqvt" + "Quotient" + "Quotient_List" + "Quotient_Product" +begin + + +section {* Abstractions *} + +fun + alpha_set +where + alpha_set[simp del]: + "alpha_set (bs, x) R f pi (cs, y) \ + f x - bs = f y - cs \ + (f x - bs) \* pi \ + R (pi \ x) y \ + pi \ bs = cs" + +fun + alpha_res +where + alpha_res[simp del]: + "alpha_res (bs, x) R f pi (cs, y) \ + f x - bs = f y - cs \ + (f x - bs) \* pi \ + R (pi \ x) y" + +fun + alpha_lst +where + alpha_lst[simp del]: + "alpha_lst (bs, x) R f pi (cs, y) \ + f x - set bs = f y - set cs \ + (f x - set bs) \* pi \ + R (pi \ x) y \ + pi \ bs = cs" + +lemmas alphas = alpha_set.simps alpha_res.simps alpha_lst.simps + +notation + alpha_set ("_ \set _ _ _ _" [100, 100, 100, 100, 100] 100) and + alpha_res ("_ \res _ _ _ _" [100, 100, 100, 100, 100] 100) and + alpha_lst ("_ \lst _ _ _ _" [100, 100, 100, 100, 100] 100) + +section {* Mono *} + +lemma [mono]: + shows "R1 \ R2 \ alpha_set bs R1 \ alpha_set bs R2" + and "R1 \ R2 \ alpha_res bs R1 \ alpha_res bs R2" + and "R1 \ R2 \ alpha_lst cs R1 \ alpha_lst cs R2" + by (case_tac [!] bs, case_tac [!] cs) + (auto simp add: le_fun_def le_bool_def alphas) + +section {* Equivariance *} + +lemma alpha_eqvt[eqvt]: + shows "(bs, x) \set R f q (cs, y) \ (p \ bs, p \ x) \set (p \ R) (p \ f) (p \ q) (p \ cs, p \ y)" + and "(bs, x) \res R f q (cs, y) \ (p \ bs, p \ x) \res (p \ R) (p \ f) (p \ q) (p \ cs, p \ y)" + and "(ds, x) \lst R f q (es, y) \ (p \ ds, p \ x) \lst (p \ R) (p \ f) (p \ q) (p \ es, p \ y)" + unfolding alphas + unfolding permute_eqvt[symmetric] + unfolding set_eqvt[symmetric] + unfolding permute_fun_app_eq[symmetric] + unfolding Diff_eqvt[symmetric] + by (auto simp add: permute_bool_def fresh_star_permute_iff) + + +section {* Equivalence *} + +lemma alpha_refl: + assumes a: "R x x" + shows "(bs, x) \set R f 0 (bs, x)" + and "(bs, x) \res R f 0 (bs, x)" + and "(cs, x) \lst R f 0 (cs, x)" + using a + unfolding alphas + unfolding fresh_star_def + by (simp_all add: fresh_zero_perm) + +lemma alpha_sym: + assumes a: "R (p \ x) y \ R (- p \ y) x" + shows "(bs, x) \set R f p (cs, y) \ (cs, y) \set R f (- p) (bs, x)" + and "(bs, x) \res R f p (cs, y) \ (cs, y) \res R f (- p) (bs, x)" + and "(ds, x) \lst R f p (es, y) \ (es, y) \lst R f (- p) (ds, x)" + unfolding alphas fresh_star_def + using a + by (auto simp add: fresh_minus_perm) + +lemma alpha_trans: + assumes a: "\R (p \ x) y; R (q \ y) z\ \ R ((q + p) \ x) z" + shows "\(bs, x) \set R f p (cs, y); (cs, y) \set R f q (ds, z)\ \ (bs, x) \set R f (q + p) (ds, z)" + and "\(bs, x) \res R f p (cs, y); (cs, y) \res R f q (ds, z)\ \ (bs, x) \res R f (q + p) (ds, z)" + and "\(es, x) \lst R f p (gs, y); (gs, y) \lst R f q (hs, z)\ \ (es, x) \lst R f (q + p) (hs, z)" + using a + unfolding alphas fresh_star_def + by (simp_all add: fresh_plus_perm) + +lemma alpha_sym_eqvt: + assumes a: "R (p \ x) y \ R y (p \ x)" + and b: "p \ R = R" + shows "(bs, x) \set R f p (cs, y) \ (cs, y) \set R f (- p) (bs, x)" + and "(bs, x) \res R f p (cs, y) \ (cs, y) \res R f (- p) (bs, x)" + and "(ds, x) \lst R f p (es, y) \ (es, y) \lst R f (- p) (ds, x)" +apply(auto intro!: alpha_sym) +apply(drule_tac [!] a) +apply(rule_tac [!] p="p" in permute_boolE) +apply(perm_simp add: permute_minus_cancel b) +apply(assumption) +apply(perm_simp add: permute_minus_cancel b) +apply(assumption) +apply(perm_simp add: permute_minus_cancel b) +apply(assumption) +done + +lemma alpha_set_trans_eqvt: + assumes b: "(cs, y) \set R f q (ds, z)" + and a: "(bs, x) \set R f p (cs, y)" + and d: "q \ R = R" + and c: "\R (p \ x) y; R y (- q \ z)\ \ R (p \ x) (- q \ z)" + shows "(bs, x) \set R f (q + p) (ds, z)" +apply(rule alpha_trans) +defer +apply(rule a) +apply(rule b) +apply(drule c) +apply(rule_tac p="q" in permute_boolE) +apply(perm_simp add: permute_minus_cancel d) +apply(assumption) +apply(rotate_tac -1) +apply(drule_tac p="q" in permute_boolI) +apply(perm_simp add: permute_minus_cancel d) +apply(simp add: permute_eqvt[symmetric]) +done + +lemma alpha_res_trans_eqvt: + assumes b: "(cs, y) \res R f q (ds, z)" + and a: "(bs, x) \res R f p (cs, y)" + and d: "q \ R = R" + and c: "\R (p \ x) y; R y (- q \ z)\ \ R (p \ x) (- q \ z)" + shows "(bs, x) \res R f (q + p) (ds, z)" +apply(rule alpha_trans) +defer +apply(rule a) +apply(rule b) +apply(drule c) +apply(rule_tac p="q" in permute_boolE) +apply(perm_simp add: permute_minus_cancel d) +apply(assumption) +apply(rotate_tac -1) +apply(drule_tac p="q" in permute_boolI) +apply(perm_simp add: permute_minus_cancel d) +apply(simp add: permute_eqvt[symmetric]) +done + +lemma alpha_lst_trans_eqvt: + assumes b: "(cs, y) \lst R f q (ds, z)" + and a: "(bs, x) \lst R f p (cs, y)" + and d: "q \ R = R" + and c: "\R (p \ x) y; R y (- q \ z)\ \ R (p \ x) (- q \ z)" + shows "(bs, x) \lst R f (q + p) (ds, z)" +apply(rule alpha_trans) +defer +apply(rule a) +apply(rule b) +apply(drule c) +apply(rule_tac p="q" in permute_boolE) +apply(perm_simp add: permute_minus_cancel d) +apply(assumption) +apply(rotate_tac -1) +apply(drule_tac p="q" in permute_boolI) +apply(perm_simp add: permute_minus_cancel d) +apply(simp add: permute_eqvt[symmetric]) +done + +lemmas alpha_trans_eqvt = alpha_set_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt + + +section {* General Abstractions *} + +fun + alpha_abs_set +where + [simp del]: + "alpha_abs_set (bs, x) (cs, y) \ (\p. (bs, x) \set (op=) supp p (cs, y))" + +fun + alpha_abs_lst +where + [simp del]: + "alpha_abs_lst (bs, x) (cs, y) \ (\p. (bs, x) \lst (op=) supp p (cs, y))" + +fun + alpha_abs_res +where + [simp del]: + "alpha_abs_res (bs, x) (cs, y) \ (\p. (bs, x) \res (op=) supp p (cs, y))" + +notation + alpha_abs_set (infix "\abs'_set" 50) and + alpha_abs_lst (infix "\abs'_lst" 50) and + alpha_abs_res (infix "\abs'_res" 50) + +lemmas alphas_abs = alpha_abs_set.simps alpha_abs_res.simps alpha_abs_lst.simps + + +lemma alphas_abs_refl: + shows "(bs, x) \abs_set (bs, x)" + and "(bs, x) \abs_res (bs, x)" + and "(cs, x) \abs_lst (cs, x)" + unfolding alphas_abs + unfolding alphas + unfolding fresh_star_def + by (rule_tac [!] x="0" in exI) + (simp_all add: fresh_zero_perm) + +lemma alphas_abs_sym: + shows "(bs, x) \abs_set (cs, y) \ (cs, y) \abs_set (bs, x)" + and "(bs, x) \abs_res (cs, y) \ (cs, y) \abs_res (bs, x)" + and "(ds, x) \abs_lst (es, y) \ (es, y) \abs_lst (ds, x)" + unfolding alphas_abs + unfolding alphas + unfolding fresh_star_def + by (erule_tac [!] exE, rule_tac [!] x="-p" in exI) + (auto simp add: fresh_minus_perm) + +lemma alphas_abs_trans: + shows "\(bs, x) \abs_set (cs, y); (cs, y) \abs_set (ds, z)\ \ (bs, x) \abs_set (ds, z)" + and "\(bs, x) \abs_res (cs, y); (cs, y) \abs_res (ds, z)\ \ (bs, x) \abs_res (ds, z)" + and "\(es, x) \abs_lst (gs, y); (gs, y) \abs_lst (hs, z)\ \ (es, x) \abs_lst (hs, z)" + unfolding alphas_abs + unfolding alphas + unfolding fresh_star_def + apply(erule_tac [!] exE, erule_tac [!] exE) + apply(rule_tac [!] x="pa + p" in exI) + by (simp_all add: fresh_plus_perm) + +lemma alphas_abs_eqvt: + shows "(bs, x) \abs_set (cs, y) \ (p \ bs, p \ x) \abs_set (p \ cs, p \ y)" + and "(bs, x) \abs_res (cs, y) \ (p \ bs, p \ x) \abs_res (p \ cs, p \ y)" + and "(ds, x) \abs_lst (es, y) \ (p \ ds, p \ x) \abs_lst (p \ es, p \ y)" + unfolding alphas_abs + unfolding alphas + unfolding set_eqvt[symmetric] + unfolding supp_eqvt[symmetric] + unfolding Diff_eqvt[symmetric] + apply(erule_tac [!] exE) + apply(rule_tac [!] x="p \ pa" in exI) + by (auto simp add: fresh_star_permute_iff permute_eqvt[symmetric]) + +quotient_type + 'a abs_set = "(atom set \ 'a::pt)" / "alpha_abs_set" +and 'b abs_res = "(atom set \ 'b::pt)" / "alpha_abs_res" +and 'c abs_lst = "(atom list \ 'c::pt)" / "alpha_abs_lst" + apply(rule_tac [!] equivpI) + unfolding reflp_def symp_def transp_def + by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:) + +quotient_definition + Abs_set ("[_]set. _" [60, 60] 60) +where + "Abs_set::atom set \ ('a::pt) \ 'a abs_set" +is + "Pair::atom set \ ('a::pt) \ (atom set \ 'a)" + +quotient_definition + Abs_res ("[_]res. _" [60, 60] 60) +where + "Abs_res::atom set \ ('a::pt) \ 'a abs_res" +is + "Pair::atom set \ ('a::pt) \ (atom set \ 'a)" + +quotient_definition + Abs_lst ("[_]lst. _" [60, 60] 60) +where + "Abs_lst::atom list \ ('a::pt) \ 'a abs_lst" +is + "Pair::atom list \ ('a::pt) \ (atom list \ 'a)" + +lemma [quot_respect]: + shows "(op= ===> op= ===> alpha_abs_set) Pair Pair" + and "(op= ===> op= ===> alpha_abs_res) Pair Pair" + and "(op= ===> op= ===> alpha_abs_lst) Pair Pair" + unfolding fun_rel_def + by (auto intro: alphas_abs_refl) + +lemma [quot_respect]: + shows "(op= ===> alpha_abs_set ===> alpha_abs_set) permute permute" + and "(op= ===> alpha_abs_res ===> alpha_abs_res) permute permute" + and "(op= ===> alpha_abs_lst ===> alpha_abs_lst) permute permute" + unfolding fun_rel_def + by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt) + +lemma Abs_eq_iff: + shows "Abs_set bs x = Abs_set cs y \ (\p. (bs, x) \set (op =) supp p (cs, y))" + and "Abs_res bs x = Abs_res cs y \ (\p. (bs, x) \res (op =) supp p (cs, y))" + and "Abs_lst bsl x = Abs_lst csl y \ (\p. (bsl, x) \lst (op =) supp p (csl, y))" + by (lifting alphas_abs) + +lemma Abs_exhausts: + shows "(\as (x::'a::pt). y1 = Abs_set as x \ P1) \ P1" + and "(\as (x::'a::pt). y2 = Abs_res as x \ P2) \ P2" + and "(\as (x::'a::pt). y3 = Abs_lst as x \ P3) \ P3" + by (lifting prod.exhaust[where 'a="atom set" and 'b="'a"] + prod.exhaust[where 'a="atom set" and 'b="'a"] + prod.exhaust[where 'a="atom list" and 'b="'a"]) + +instantiation abs_set :: (pt) pt +begin + +quotient_definition + "permute_abs_set::perm \ ('a::pt abs_set) \ 'a abs_set" +is + "permute:: perm \ (atom set \ 'a::pt) \ (atom set \ 'a::pt)" + +lemma permute_Abs_set[simp]: + fixes x::"'a::pt" + shows "(p \ (Abs_set as x)) = Abs_set (p \ as) (p \ x)" + by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"]) + +instance + apply(default) + apply(case_tac [!] x rule: Abs_exhausts(1)) + apply(simp_all) + done + +end + +instantiation abs_res :: (pt) pt +begin + +quotient_definition + "permute_abs_res::perm \ ('a::pt abs_res) \ 'a abs_res" +is + "permute:: perm \ (atom set \ 'a::pt) \ (atom set \ 'a::pt)" + +lemma permute_Abs_res[simp]: + fixes x::"'a::pt" + shows "(p \ (Abs_res as x)) = Abs_res (p \ as) (p \ x)" + by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"]) + +instance + apply(default) + apply(case_tac [!] x rule: Abs_exhausts(2)) + apply(simp_all) + done + +end + +instantiation abs_lst :: (pt) pt +begin + +quotient_definition + "permute_abs_lst::perm \ ('a::pt abs_lst) \ 'a abs_lst" +is + "permute:: perm \ (atom list \ 'a::pt) \ (atom list \ 'a::pt)" + +lemma permute_Abs_lst[simp]: + fixes x::"'a::pt" + shows "(p \ (Abs_lst as x)) = Abs_lst (p \ as) (p \ x)" + by (lifting permute_prod.simps[where 'a="atom list" and 'b="'a"]) + +instance + apply(default) + apply(case_tac [!] x rule: Abs_exhausts(3)) + apply(simp_all) + done + +end + +lemmas permute_Abs[eqvt] = permute_Abs_set permute_Abs_res permute_Abs_lst + + +lemma Abs_swap1: + assumes a1: "a \ (supp x) - bs" + and a2: "b \ (supp x) - bs" + shows "Abs_set bs x = Abs_set ((a \ b) \ bs) ((a \ b) \ x)" + and "Abs_res bs x = Abs_res ((a \ b) \ bs) ((a \ b) \ x)" + unfolding Abs_eq_iff + unfolding alphas + unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] + unfolding fresh_star_def fresh_def + unfolding swap_set_not_in[OF a1 a2] + using a1 a2 + by (rule_tac [!] x="(a \ b)" in exI) + (auto simp add: supp_perm swap_atom) + +lemma Abs_swap2: + assumes a1: "a \ (supp x) - (set bs)" + and a2: "b \ (supp x) - (set bs)" + shows "Abs_lst bs x = Abs_lst ((a \ b) \ bs) ((a \ b) \ x)" + unfolding Abs_eq_iff + unfolding alphas + unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric] + unfolding fresh_star_def fresh_def + unfolding swap_set_not_in[OF a1 a2] + using a1 a2 + by (rule_tac [!] x="(a \ b)" in exI) + (auto simp add: supp_perm swap_atom) + +lemma Abs_supports: + shows "((supp x) - as) supports (Abs_set as x)" + and "((supp x) - as) supports (Abs_res as x)" + and "((supp x) - set bs) supports (Abs_lst bs x)" + unfolding supports_def + unfolding permute_Abs + by (simp_all add: Abs_swap1[symmetric] Abs_swap2[symmetric]) + +function + supp_set :: "('a::pt) abs_set \ atom set" +where + "supp_set (Abs_set as x) = supp x - as" +apply(case_tac x rule: Abs_exhausts(1)) +apply(simp) +apply(simp add: Abs_eq_iff alphas_abs alphas) +done + +termination supp_set + by (auto intro!: local.termination) + +function + supp_res :: "('a::pt) abs_res \ atom set" +where + "supp_res (Abs_res as x) = supp x - as" +apply(case_tac x rule: Abs_exhausts(2)) +apply(simp) +apply(simp add: Abs_eq_iff alphas_abs alphas) +done + +termination supp_res + by (auto intro!: local.termination) + +function + supp_lst :: "('a::pt) abs_lst \ atom set" +where + "supp_lst (Abs_lst cs x) = (supp x) - (set cs)" +apply(case_tac x rule: Abs_exhausts(3)) +apply(simp) +apply(simp add: Abs_eq_iff alphas_abs alphas) +done + +termination supp_lst + by (auto intro!: local.termination) + +lemma [eqvt]: + shows "(p \ supp_set x) = supp_set (p \ x)" + and "(p \ supp_res y) = supp_res (p \ y)" + and "(p \ supp_lst z) = supp_lst (p \ z)" + apply(case_tac x rule: Abs_exhausts(1)) + apply(simp add: supp_eqvt Diff_eqvt) + apply(case_tac y rule: Abs_exhausts(2)) + apply(simp add: supp_eqvt Diff_eqvt) + apply(case_tac z rule: Abs_exhausts(3)) + apply(simp add: supp_eqvt Diff_eqvt set_eqvt) + done + +lemma Abs_fresh_aux: + shows "a \ Abs bs x \ a \ supp_set (Abs bs x)" + and "a \ Abs_res bs x \ a \ supp_res (Abs_res bs x)" + and "a \ Abs_lst cs x \ a \ supp_lst (Abs_lst cs x)" + by (rule_tac [!] fresh_fun_eqvt_app) + (simp_all only: eqvts_raw) + +lemma Abs_supp_subset1: + assumes a: "finite (supp x)" + shows "(supp x) - as \ supp (Abs_set as x)" + and "(supp x) - as \ supp (Abs_res as x)" + and "(supp x) - (set bs) \ supp (Abs_lst bs x)" + unfolding supp_conv_fresh + by (auto dest!: Abs_fresh_aux) + (simp_all add: fresh_def supp_finite_atom_set a) + +lemma Abs_supp_subset2: + assumes a: "finite (supp x)" + shows "supp (Abs_set as x) \ (supp x) - as" + and "supp (Abs_res as x) \ (supp x) - as" + and "supp (Abs_lst bs x) \ (supp x) - (set bs)" + by (rule_tac [!] supp_is_subset) + (simp_all add: Abs_supports a) + +lemma Abs_finite_supp: + assumes a: "finite (supp x)" + shows "supp (Abs_set as x) = (supp x) - as" + and "supp (Abs_res as x) = (supp x) - as" + and "supp (Abs_lst bs x) = (supp x) - (set bs)" + by (rule_tac [!] subset_antisym) + (simp_all add: Abs_supp_subset1[OF a] Abs_supp_subset2[OF a]) + +lemma supp_Abs: + fixes x::"'a::fs" + shows "supp (Abs_set as x) = (supp x) - as" + and "supp (Abs_res as x) = (supp x) - as" + and "supp (Abs_lst bs x) = (supp x) - (set bs)" + by (rule_tac [!] Abs_finite_supp) + (simp_all add: finite_supp) + +instance abs_set :: (fs) fs + apply(default) + apply(case_tac x rule: Abs_exhausts(1)) + apply(simp add: supp_Abs finite_supp) + done + +instance abs_res :: (fs) fs + apply(default) + apply(case_tac x rule: Abs_exhausts(2)) + apply(simp add: supp_Abs finite_supp) + done + +instance abs_lst :: (fs) fs + apply(default) + apply(case_tac x rule: Abs_exhausts(3)) + apply(simp add: supp_Abs finite_supp) + done + +lemma Abs_fresh_iff: + fixes x::"'a::fs" + shows "a \ Abs_set bs x \ a \ bs \ (a \ bs \ a \ x)" + and "a \ Abs_res bs x \ a \ bs \ (a \ bs \ a \ x)" + and "a \ Abs_lst cs x \ a \ (set cs) \ (a \ (set cs) \ a \ x)" + unfolding fresh_def + unfolding supp_Abs + by auto + +lemma Abs_fresh_star: + fixes x::"'a::fs" + shows "as \* Abs_set as x" + and "as \* Abs_res as x" + and "set bs \* Abs_lst bs x" + unfolding fresh_star_def + by(simp_all add: Abs_fresh_iff) + + +section {* Infrastructure for building tuples of relations and functions *} + +fun + prod_fv :: "('a \ atom set) \ ('b \ atom set) \ ('a \ 'b) \ atom set" +where + "prod_fv fv1 fv2 (x, y) = fv1 x \ fv2 y" + +definition + prod_alpha :: "('a \ 'a \ bool) \ ('b \ 'b \ bool) \ ('a \ 'b \ 'a \ 'b \ bool)" +where + "prod_alpha = prod_rel" + +lemma [quot_respect]: + shows "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv" + unfolding fun_rel_def + unfolding prod_rel_def + by auto + +lemma [quot_preserve]: + assumes q1: "Quotient R1 abs1 rep1" + and q2: "Quotient R2 abs2 rep2" + shows "((abs1 ---> id) ---> (abs2 ---> id) ---> prod_fun rep1 rep2 ---> id) prod_fv = prod_fv" + by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) + +lemma [mono]: + shows "A <= B \ C <= D ==> prod_alpha A C <= prod_alpha B D" + unfolding prod_alpha_def + by auto + +lemma [eqvt]: + shows "p \ prod_alpha A B x y = prod_alpha (p \ A) (p \ B) (p \ x) (p \ y)" + unfolding prod_alpha_def + unfolding prod_rel_def + by (perm_simp) (rule refl) + +lemma [eqvt]: + shows "p \ prod_fv A B (x, y) = prod_fv (p \ A) (p \ B) (p \ x, p \ y)" + unfolding prod_fv.simps + by (perm_simp) (rule refl) + +lemma prod_fv_supp: + shows "prod_fv supp supp = supp" +by (rule ext) + (auto simp add: prod_fv.simps supp_Pair) + +lemma prod_alpha_eq: + shows "prod_alpha (op=) (op=) = (op=)" +unfolding prod_alpha_def +by (auto intro!: ext) + + +end + diff -r 41137dc935ff -r 8193bbaa07fe Nominal/Nominal2_Base.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Nominal2_Base.thy Sun Nov 14 16:34:47 2010 +0000 @@ -0,0 +1,2024 @@ +(* Title: Nominal2_Base + Authors: Brian Huffman, Christian Urban + + Basic definitions and lemma infrastructure for + Nominal Isabelle. +*) +theory Nominal2_Base +imports Main Infinite_Set + "~~/src/HOL/Quotient_Examples/FSet" +uses ("nominal_library.ML") + ("nominal_atoms.ML") +begin + +section {* Atoms and Sorts *} + +text {* A simple implementation for atom_sorts is strings. *} +(* types atom_sort = string *) + +text {* To deal with Church-like binding we use trees of + strings as sorts. *} + +datatype atom_sort = Sort "string" "atom_sort list" + +datatype atom = Atom atom_sort nat + + +text {* Basic projection function. *} + +primrec + sort_of :: "atom \ atom_sort" +where + "sort_of (Atom s i) = s" + +primrec + nat_of :: "atom \ nat" +where + "nat_of (Atom s n) = n" + + +text {* There are infinitely many atoms of each sort. *} +lemma INFM_sort_of_eq: + shows "INFM a. sort_of a = s" +proof - + have "INFM i. sort_of (Atom s i) = s" by simp + moreover have "inj (Atom s)" by (simp add: inj_on_def) + ultimately show "INFM a. sort_of a = s" by (rule INFM_inj) +qed + +lemma infinite_sort_of_eq: + shows "infinite {a. sort_of a = s}" + using INFM_sort_of_eq unfolding INFM_iff_infinite . + +lemma atom_infinite [simp]: + shows "infinite (UNIV :: atom set)" + using subset_UNIV infinite_sort_of_eq + by (rule infinite_super) + +lemma obtain_atom: + fixes X :: "atom set" + assumes X: "finite X" + obtains a where "a \ X" "sort_of a = s" +proof - + from X have "MOST a. a \ X" + unfolding MOST_iff_cofinite by simp + with INFM_sort_of_eq + have "INFM a. sort_of a = s \ a \ X" + by (rule INFM_conjI) + then obtain a where "a \ X" "sort_of a = s" + by (auto elim: INFM_E) + then show ?thesis .. +qed + +lemma atom_components_eq_iff: + fixes a b :: atom + 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 = + "{f. bij f \ finite {a. f a \ a} \ (\a. sort_of (f a) = sort_of a)}" +proof + show "id \ ?perm" by simp +qed + +lemma permI: + assumes "bij f" and "MOST x. f x = x" and "\a. sort_of (f a) = sort_of a" + shows "f \ perm" + using assms unfolding perm_def MOST_iff_cofinite by simp + +lemma perm_is_bij: "f \ perm \ bij f" + unfolding perm_def by simp + +lemma perm_is_finite: "f \ perm \ finite {a. f a \ a}" + unfolding perm_def by simp + +lemma perm_is_sort_respecting: "f \ perm \ sort_of (f a) = sort_of a" + unfolding perm_def by simp + +lemma perm_MOST: "f \ perm \ MOST x. f x = x" + unfolding perm_def MOST_iff_cofinite by simp + +lemma perm_id: "id \ perm" + unfolding perm_def by simp + +lemma perm_comp: + assumes f: "f \ perm" and g: "g \ perm" + shows "(f \ g) \ perm" +apply (rule permI) +apply (rule bij_comp) +apply (rule perm_is_bij [OF g]) +apply (rule perm_is_bij [OF f]) +apply (rule MOST_rev_mp [OF perm_MOST [OF g]]) +apply (rule MOST_rev_mp [OF perm_MOST [OF f]]) +apply (simp) +apply (simp add: perm_is_sort_respecting [OF f]) +apply (simp add: perm_is_sort_respecting [OF g]) +done + +lemma perm_inv: + assumes f: "f \ perm" + shows "(inv f) \ perm" +apply (rule permI) +apply (rule bij_imp_bij_inv) +apply (rule perm_is_bij [OF f]) +apply (rule MOST_mono [OF perm_MOST [OF f]]) +apply (erule subst, rule inv_f_f) +apply (rule bij_is_inj [OF perm_is_bij [OF f]]) +apply (rule perm_is_sort_respecting [OF f, THEN sym, THEN trans]) +apply (simp add: surj_f_inv_f [OF bij_is_surj [OF perm_is_bij [OF f]]]) +done + +lemma bij_Rep_perm: "bij (Rep_perm p)" + using Rep_perm [of p] unfolding perm_def by simp + +lemma finite_Rep_perm: "finite {a. Rep_perm p a \ a}" + using Rep_perm [of p] unfolding perm_def by simp + +lemma sort_of_Rep_perm: "sort_of (Rep_perm p a) = sort_of a" + using Rep_perm [of p] unfolding perm_def by simp + +lemma Rep_perm_ext: + "Rep_perm p1 = Rep_perm p2 \ p1 = p2" + by (simp add: fun_eq_iff Rep_perm_inject [symmetric]) + +instance perm :: size .. + +subsection {* Permutations form a group *} + +instantiation perm :: group_add +begin + +definition + "0 = Abs_perm id" + +definition + "- p = Abs_perm (inv (Rep_perm p))" + +definition + "p + q = Abs_perm (Rep_perm p \ Rep_perm q)" + +definition + "(p1::perm) - p2 = p1 + - p2" + +lemma Rep_perm_0: "Rep_perm 0 = id" + unfolding zero_perm_def + by (simp add: Abs_perm_inverse perm_id) + +lemma Rep_perm_add: + "Rep_perm (p1 + p2) = Rep_perm p1 \ Rep_perm p2" + unfolding plus_perm_def + by (simp add: Abs_perm_inverse perm_comp Rep_perm) + +lemma Rep_perm_uminus: + "Rep_perm (- p) = inv (Rep_perm p)" + unfolding uminus_perm_def + by (simp add: Abs_perm_inverse perm_inv Rep_perm) + +instance +apply default +unfolding Rep_perm_inject [symmetric] +unfolding minus_perm_def +unfolding Rep_perm_add +unfolding Rep_perm_uminus +unfolding Rep_perm_0 +by (simp_all add: o_assoc inv_o_cancel [OF bij_is_inj [OF bij_Rep_perm]]) + +end + + +section {* Implementation of swappings *} + +definition + swap :: "atom \ atom \ perm" ("'(_ \ _')") +where + "(a \ b) = + Abs_perm (if sort_of a = sort_of b + then (\c. if a = c then b else if b = c then a else c) + else id)" + +lemma Rep_perm_swap: + "Rep_perm (a \ b) = + (if sort_of a = sort_of b + then (\c. if a = c then b else if b = c then a else c) + else id)" +unfolding swap_def +apply (rule Abs_perm_inverse) +apply (rule permI) +apply (auto simp add: bij_def inj_on_def surj_def)[1] +apply (rule MOST_rev_mp [OF MOST_neq(1) [of a]]) +apply (rule MOST_rev_mp [OF MOST_neq(1) [of b]]) +apply (simp) +apply (simp) +done + +lemmas Rep_perm_simps = + Rep_perm_0 + Rep_perm_add + Rep_perm_uminus + Rep_perm_swap + +lemma swap_different_sorts [simp]: + "sort_of a \ sort_of b \ (a \ b) = 0" + by (rule Rep_perm_ext) (simp add: Rep_perm_simps) + +lemma swap_cancel: + "(a \ b) + (a \ b) = 0" + by (rule Rep_perm_ext) + (simp add: Rep_perm_simps fun_eq_iff) + +lemma swap_self [simp]: + "(a \ a) = 0" + by (rule Rep_perm_ext, simp add: Rep_perm_simps fun_eq_iff) + +lemma minus_swap [simp]: + "- (a \ b) = (a \ b)" + by (rule minus_unique [OF swap_cancel]) + +lemma swap_commute: + "(a \ b) = (b \ a)" + by (rule Rep_perm_ext) + (simp add: Rep_perm_swap fun_eq_iff) + +lemma swap_triple: + assumes "a \ b" and "c \ b" + assumes "sort_of a = sort_of b" "sort_of b = sort_of c" + shows "(a \ c) + (b \ c) + (a \ c) = (a \ b)" + using assms + by (rule_tac Rep_perm_ext) + (auto simp add: Rep_perm_simps fun_eq_iff) + + +section {* Permutation Types *} + +text {* + Infix syntax for @{text permute} has higher precedence than + addition, but lower than unary minus. +*} + +class pt = + fixes permute :: "perm \ 'a \ 'a" ("_ \ _" [76, 75] 75) + assumes permute_zero [simp]: "0 \ x = x" + assumes permute_plus [simp]: "(p + q) \ x = p \ (q \ x)" +begin + +lemma permute_diff [simp]: + shows "(p - q) \ x = p \ - q \ x" + unfolding diff_minus by simp + +lemma permute_minus_cancel [simp]: + shows "p \ - p \ x = x" + and "- p \ p \ x = x" + unfolding permute_plus [symmetric] by simp_all + +lemma permute_swap_cancel [simp]: + shows "(a \ b) \ (a \ b) \ x = x" + unfolding permute_plus [symmetric] + by (simp add: swap_cancel) + +lemma permute_swap_cancel2 [simp]: + shows "(a \ b) \ (b \ a) \ x = x" + unfolding permute_plus [symmetric] + by (simp add: swap_commute) + +lemma inj_permute [simp]: + shows "inj (permute p)" + by (rule inj_on_inverseI) + (rule permute_minus_cancel) + +lemma surj_permute [simp]: + shows "surj (permute p)" + by (rule surjI, rule permute_minus_cancel) + +lemma bij_permute [simp]: + shows "bij (permute p)" + by (rule bijI [OF inj_permute surj_permute]) + +lemma inv_permute: + shows "inv (permute p) = permute (- p)" + by (rule inv_equality) (simp_all) + +lemma permute_minus: + shows "permute (- p) = inv (permute p)" + by (simp add: inv_permute) + +lemma permute_eq_iff [simp]: + shows "p \ x = p \ y \ x = y" + by (rule inj_permute [THEN inj_eq]) + +end + +subsection {* Permutations for atoms *} + +instantiation atom :: pt +begin + +definition + "p \ a = (Rep_perm p) a" + +instance +apply(default) +apply(simp_all add: permute_atom_def Rep_perm_simps) +done + +end + +lemma sort_of_permute [simp]: + shows "sort_of (p \ a) = sort_of a" + unfolding permute_atom_def by (rule sort_of_Rep_perm) + +lemma swap_atom: + shows "(a \ b) \ c = + (if sort_of a = sort_of b + then (if c = a then b else if c = b then a else c) else c)" + unfolding permute_atom_def + by (simp add: Rep_perm_swap) + +lemma swap_atom_simps [simp]: + "sort_of a = sort_of b \ (a \ b) \ a = b" + "sort_of a = sort_of b \ (a \ b) \ b = a" + "c \ a \ c \ b \ (a \ b) \ c = c" + unfolding swap_atom by simp_all + +lemma expand_perm_eq: + fixes p q :: "perm" + shows "p = q \ (\a::atom. p \ a = q \ a)" + unfolding permute_atom_def + by (metis Rep_perm_ext ext) + + +subsection {* Permutations for permutations *} + +instantiation perm :: pt +begin + +definition + "p \ q = p + q - p" + +instance +apply default +apply (simp add: permute_perm_def) +apply (simp add: permute_perm_def diff_minus minus_add add_assoc) +done + +end + +lemma permute_self: + shows "p \ p = p" + 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) + +subsection {* Permutations for functions *} + +instantiation "fun" :: (pt, pt) pt +begin + +definition + "p \ f = (\x. p \ (f (- p \ x)))" + +instance +apply default +apply (simp add: permute_fun_def) +apply (simp add: permute_fun_def minus_add) +done + +end + +lemma permute_fun_app_eq: + shows "p \ (f x) = (p \ f) (p \ x)" + unfolding permute_fun_def by simp + + +subsection {* Permutations for booleans *} + +instantiation bool :: pt +begin + +definition "p \ (b::bool) = b" + +instance +apply(default) +apply(simp_all add: permute_bool_def) +done + +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 permute_boolE: + fixes P::"bool" + shows "p \ P \ P" + by (simp add: permute_bool_def) + +lemma permute_boolI: + fixes P::"bool" + shows "P \ p \ P" + by(simp add: permute_bool_def) + +subsection {* Permutations for sets *} + +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 + apply(auto simp add: mem_def) + apply(rule_tac x="- p \ x" in exI) + apply(simp) + done + +lemma permute_set_eq_image: + shows "p \ X = permute p ` X" + unfolding permute_set_eq by auto + +lemma permute_set_eq_vimage: + shows "p \ X = permute (- p) -` X" + unfolding permute_fun_def permute_bool_def + unfolding vimage_def Collect_def mem_def .. + +lemma swap_set_not_in: + assumes a: "a \ S" "b \ S" + shows "(a \ b) \ S = S" + unfolding permute_set_eq + using a by (auto simp add: swap_atom) + +lemma swap_set_in: + assumes a: "a \ S" "b \ S" "sort_of a = sort_of b" + shows "(a \ b) \ S \ S" + unfolding permute_set_eq + using a by (auto simp add: swap_atom) + +lemma mem_permute_iff: + shows "(p \ x) \ (p \ X) \ x \ X" + 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 + by (simp add: permute_fun_def permute_bool_def) + +lemma insert_eqvt: + shows "p \ (insert x A) = insert (p \ x) (p \ A)" + unfolding permute_set_eq_image image_insert .. + + +subsection {* Permutations for units *} + +instantiation unit :: pt +begin + +definition "p \ (u::unit) = u" + +instance +by (default) (simp_all add: permute_unit_def) + +end + + +subsection {* Permutations for products *} + +instantiation prod :: (pt, pt) pt +begin + +primrec + permute_prod +where + Pair_eqvt: "p \ (x, y) = (p \ x, p \ y)" + +instance +by default auto + +end + +subsection {* Permutations for sums *} + +instantiation sum :: (pt, pt) pt +begin + +primrec + permute_sum +where + "p \ (Inl x) = Inl (p \ x)" +| "p \ (Inr y) = Inr (p \ y)" + +instance +by (default) (case_tac [!] x, simp_all) + +end + +subsection {* Permutations for lists *} + +instantiation list :: (pt) pt +begin + +primrec + permute_list +where + "p \ [] = []" +| "p \ (x # xs) = p \ x # p \ xs" + +instance +by (default) (induct_tac [!] x, simp_all) + +end + +lemma set_eqvt: + shows "p \ (set xs) = set (p \ xs)" + by (induct xs) (simp_all add: empty_eqvt insert_eqvt) + +subsection {* Permutations for options *} + +instantiation option :: (pt) pt +begin + +primrec + permute_option +where + "p \ None = None" +| "p \ (Some x) = Some (p \ x)" + +instance +by (default) (induct_tac [!] x, simp_all) + +end + + +subsection {* Permutations for fsets *} + +lemma permute_fset_rsp[quot_respect]: + shows "(op = ===> list_eq ===> list_eq) permute permute" + unfolding fun_rel_def + by (simp add: set_eqvt[symmetric]) + +instantiation fset :: (pt) pt +begin + +quotient_definition + "permute_fset :: perm \ 'a fset \ 'a fset" +is + "permute :: perm \ 'a list \ 'a list" + +instance +proof + fix x :: "'a fset" and p q :: "perm" + show "0 \ x = x" by (descending) (simp) + show "(p + q) \ x = p \ q \ x" by (descending) (simp) +qed + +end + +lemma permute_fset [simp]: + fixes S::"('a::pt) fset" + shows "(p \ {||}) = ({||} ::('a::pt) fset)" + and "(p \ insert_fset x S) = insert_fset (p \ x) (p \ S)" + by (lifting permute_list.simps) + + + +subsection {* Permutations for @{typ char}, @{typ nat}, and @{typ int} *} + +instantiation char :: pt +begin + +definition "p \ (c::char) = c" + +instance +by (default) (simp_all add: permute_char_def) + +end + +instantiation nat :: pt +begin + +definition "p \ (n::nat) = n" + +instance +by (default) (simp_all add: permute_nat_def) + +end + +instantiation int :: pt +begin + +definition "p \ (i::int) = i" + +instance +by (default) (simp_all add: permute_int_def) + +end + + +section {* Pure types *} + +text {* Pure types will have always empty support. *} + +class pure = pt + + assumes permute_pure: "p \ x = x" + +text {* Types @{typ unit} and @{typ bool} are pure. *} + +instance unit :: pure +proof qed (rule permute_unit_def) + +instance bool :: pure +proof qed (rule permute_bool_def) + +text {* Other type constructors preserve purity. *} + +instance "fun" :: (pure, pure) pure +by default (simp add: permute_fun_def permute_pure) + +instance prod :: (pure, pure) pure +by default (induct_tac x, simp add: permute_pure) + +instance sum :: (pure, pure) pure +by default (induct_tac x, simp_all add: permute_pure) + +instance list :: (pure) pure +by default (induct_tac x, simp_all add: permute_pure) + +instance option :: (pure) pure +by default (induct_tac x, simp_all add: permute_pure) + + +subsection {* Types @{typ char}, @{typ nat}, and @{typ int} *} + +instance char :: pure +proof qed (rule permute_char_def) + +instance nat :: pure +proof qed (rule permute_nat_def) + +instance int :: pure +proof qed (rule permute_int_def) + + +subsection {* Supp, Freshness and Supports *} + +context pt +begin + +definition + supp :: "'a \ atom set" +where + "supp x = {a. infinite {b. (a \ b) \ x \ x}}" + +end + +definition + fresh :: "atom \ 'a::pt \ bool" ("_ \ _" [55, 55] 55) +where + "a \ x \ a \ supp x" + +lemma supp_conv_fresh: + shows "supp x = {a. \ a \ x}" + unfolding fresh_def by simp + +lemma swap_rel_trans: + assumes "sort_of a = sort_of b" + assumes "sort_of b = sort_of c" + assumes "(a \ c) \ x = x" + assumes "(b \ c) \ x = x" + shows "(a \ b) \ x = x" +proof (cases) + assume "a = b \ c = b" + with assms show "(a \ b) \ x = x" by auto +next + assume *: "\ (a = b \ c = b)" + have "((a \ c) + (b \ c) + (a \ c)) \ x = x" + using assms by simp + also have "(a \ c) + (b \ c) + (a \ c) = (a \ b)" + using assms * by (simp add: swap_triple) + finally show "(a \ b) \ x = x" . +qed + +lemma swap_fresh_fresh: + assumes a: "a \ x" + and b: "b \ x" + shows "(a \ b) \ x = x" +proof (cases) + assume asm: "sort_of a = sort_of b" + have "finite {c. (a \ c) \ x \ x}" "finite {c. (b \ c) \ x \ x}" + using a b unfolding fresh_def supp_def by simp_all + then have "finite ({c. (a \ c) \ x \ x} \ {c. (b \ c) \ x \ x})" by simp + then obtain c + where "(a \ c) \ x = x" "(b \ c) \ x = x" "sort_of c = sort_of b" + by (rule obtain_atom) (auto) + then show "(a \ b) \ x = x" using asm by (rule_tac swap_rel_trans) (simp_all) +next + assume "sort_of a \ sort_of b" + then show "(a \ b) \ x = x" by simp +qed + + +subsection {* supp and fresh are equivariant *} + +lemma finite_Collect_bij: + assumes a: "bij f" + shows "finite {x. P (f x)} = finite {x. P x}" +by (metis a finite_vimage_iff vimage_Collect_eq) + +lemma fresh_permute_iff: + shows "(p \ a) \ (p \ x) \ a \ x" +proof - + have "(p \ a) \ (p \ x) \ finite {b. (p \ a \ b) \ p \ x \ p \ x}" + unfolding fresh_def supp_def by simp + also have "\ \ finite {b. (p \ a \ p \ b) \ p \ x \ p \ x}" + using bij_permute by (rule finite_Collect_bij[symmetric]) + also have "\ \ finite {b. p \ (a \ b) \ x \ p \ x}" + by (simp only: permute_eqvt [of p] swap_eqvt) + also have "\ \ finite {b. (a \ b) \ x \ x}" + by (simp only: permute_eq_iff) + also have "\ \ a \ x" + unfolding fresh_def supp_def by simp + finally show "(p \ a) \ (p \ x) \ a \ x" . +qed + +lemma fresh_eqvt: + shows "p \ (a \ x) = (p \ a) \ (p \ x)" + unfolding permute_bool_def + by (simp add: fresh_permute_iff) + +lemma supp_eqvt: + fixes p :: "perm" + and x :: "'a::pt" + shows "p \ (supp x) = supp (p \ x)" + unfolding supp_conv_fresh + unfolding Collect_def + unfolding permute_fun_def + by (simp add: Not_eqvt fresh_eqvt) + +subsection {* supports *} + +definition + supports :: "atom set \ 'a::pt \ bool" (infixl "supports" 80) +where + "S supports x \ \a b. (a \ S \ b \ S \ (a \ b) \ x = x)" + +lemma supp_is_subset: + fixes S :: "atom set" + and x :: "'a::pt" + assumes a1: "S supports x" + and a2: "finite S" + shows "(supp x) \ S" +proof (rule ccontr) + assume "\ (supp x \ S)" + 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) + then have "a \ (supp x)" unfolding supp_def by simp + with b1 show False by simp +qed + +lemma supports_finite: + fixes S :: "atom set" + and x :: "'a::pt" + assumes a1: "S supports x" + and a2: "finite S" + shows "finite (supp x)" +proof - + have "(supp x) \ S" using a1 a2 by (rule supp_is_subset) + then show "finite (supp x)" using a2 by (simp add: finite_subset) +qed + +lemma supp_supports: + fixes x :: "'a::pt" + shows "(supp x) supports x" +unfolding supports_def +proof (intro strip) + fix a b + assume "a \ (supp x) \ b \ (supp x)" + then have "a \ x" and "b \ x" by (simp_all add: fresh_def) + then show "(a \ b) \ x = x" by (simp add: swap_fresh_fresh) +qed + +lemma supp_is_least_supports: + fixes S :: "atom set" + and x :: "'a::pt" + assumes a1: "S supports x" + and a2: "finite S" + and a3: "\S'. finite S' \ (S' supports x) \ S \ S'" + shows "(supp x) = S" +proof (rule equalityI) + show "(supp x) \ S" using a1 a2 by (rule supp_is_subset) + with a2 have fin: "finite (supp x)" by (rule rev_finite_subset) + have "(supp x) supports x" by (rule supp_supports) + with fin a3 show "S \ supp x" by blast +qed + +lemma subsetCI: + shows "(\x. x \ A \ x \ B \ False) \ A \ B" + by auto + +lemma finite_supp_unique: + assumes a1: "S supports x" + assumes a2: "finite S" + assumes a3: "\a b. \a \ S; b \ S; sort_of a = sort_of b\ \ (a \ b) \ x \ x" + shows "(supp x) = S" + using a1 a2 +proof (rule supp_is_least_supports) + fix S' + assume "finite S'" and "S' supports x" + show "S \ S'" + proof (rule subsetCI) + fix a + assume "a \ S" and "a \ S'" + have "finite (S \ S')" + using `finite S` `finite S'` by simp + then obtain b where "b \ S \ S'" and "sort_of b = sort_of a" + by (rule obtain_atom) + then have "b \ S" and "b \ S'" and "sort_of a = sort_of b" + by simp_all + then have "(a \ b) \ x = x" + using `a \ S'` `S' supports x` by (simp add: supports_def) + moreover have "(a \ b) \ x \ x" + using `a \ S` `b \ S` `sort_of a = sort_of b` + by (rule a3) + ultimately show "False" by simp + qed +qed + +section {* Support w.r.t. relations *} + +text {* + This definition is used for unquotient types, where + alpha-equivalence does not coincide with equality. +*} + +definition + "supp_rel R x = {a. infinite {b. \(R ((a \ b) \ x) x)}}" + + + +section {* Finitely-supported types *} + +class fs = pt + + assumes finite_supp: "finite (supp x)" + +lemma pure_supp: + shows "supp (x::'a::pure) = {}" + unfolding supp_def by (simp add: permute_pure) + +lemma pure_fresh: + fixes x::"'a::pure" + shows "a \ x" + unfolding fresh_def by (simp add: pure_supp) + +instance pure < fs +by default (simp add: pure_supp) + + +subsection {* Type @{typ atom} is finitely-supported. *} + +lemma supp_atom: + shows "supp a = {a}" +apply (rule finite_supp_unique) +apply (clarsimp simp add: supports_def) +apply simp +apply simp +done + +lemma fresh_atom: + shows "a \ b \ a \ b" + unfolding fresh_def supp_atom by simp + +instance atom :: fs +by default (simp add: supp_atom) + +section {* Support for finite sets of atoms *} + + +lemma supp_finite_atom_set: + fixes S::"atom set" + assumes "finite S" + shows "supp S = S" + apply(rule finite_supp_unique) + apply(simp add: supports_def) + apply(simp add: swap_set_not_in) + apply(rule assms) + apply(simp add: swap_set_in) +done + +section {* Type @{typ perm} is finitely-supported. *} + +lemma perm_swap_eq: + shows "(a \ b) \ p = p \ (p \ (a \ b)) = (a \ b)" +unfolding permute_perm_def +by (metis add_diff_cancel minus_perm_def) + +lemma supports_perm: + shows "{a. p \ a \ a} supports p" + unfolding supports_def + unfolding perm_swap_eq + by (simp add: swap_eqvt) + +lemma finite_perm_lemma: + shows "finite {a::atom. p \ a \ a}" + using finite_Rep_perm [of p] + unfolding permute_atom_def . + +lemma supp_perm: + shows "supp p = {a. p \ a \ a}" +apply (rule finite_supp_unique) +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) +done + +lemma fresh_perm: + shows "a \ p \ p \ a = a" + unfolding fresh_def + by (simp add: supp_perm) + +lemma supp_swap: + shows "supp (a \ b) = (if a = b \ sort_of a \ sort_of b then {} else {a, b})" + by (auto simp add: supp_perm swap_atom) + +lemma fresh_zero_perm: + shows "a \ (0::perm)" + unfolding fresh_perm by simp + +lemma supp_zero_perm: + shows "supp (0::perm) = {}" + unfolding supp_perm by simp + +lemma fresh_plus_perm: + fixes p q::perm + assumes "a \ p" "a \ q" + shows "a \ (p + q)" + using assms + unfolding fresh_def + by (auto simp add: supp_perm) + +lemma supp_plus_perm: + fixes p q::perm + shows "supp (p + q) \ supp p \ supp q" + by (auto simp add: supp_perm) + +lemma fresh_minus_perm: + fixes p::perm + shows "a \ (- p) \ a \ p" + unfolding fresh_def + unfolding supp_perm + apply(simp) + apply(metis permute_minus_cancel) + done + +lemma supp_minus_perm: + fixes p::perm + shows "supp (- p) = supp p" + 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 +proof + fix a::"atom" + show "(p + q) \ a = (q + p) \ a" + proof - + { assume "a \ supp p" "a \ supp q" + then have "(p + q) \ a = (q + p) \ a" + by (simp add: supp_perm) + } + moreover + { assume a: "a \ supp p" "a \ supp q" + then have "p \ a \ supp p" by (simp add: supp_perm) + then have "p \ a \ supp q" using asm by auto + with a have "(p + q) \ a = (q + p) \ a" + by (simp add: supp_perm) + } + moreover + { assume a: "a \ supp p" "a \ supp q" + then have "q \ a \ supp q" by (simp add: supp_perm) + then have "q \ a \ supp p" using asm by auto + with a have "(p + q) \ a = (q + p) \ a" + by (simp add: supp_perm) + } + ultimately show "(p + q) \ a = (q + p) \ a" + using asm by blast + qed +qed + +section {* Finite Support instances for other types *} + + +subsection {* Type @{typ "'a \ 'b"} is finitely-supported. *} + +lemma supp_Pair: + shows "supp (x, y) = supp x \ supp y" + by (simp add: supp_def Collect_imp_eq Collect_neg_eq) + +lemma fresh_Pair: + shows "a \ (x, y) \ a \ x \ a \ y" + by (simp add: fresh_def supp_Pair) + +lemma supp_Unit: + shows "supp () = {}" + by (simp add: supp_def) + +lemma fresh_Unit: + shows "a \ ()" + by (simp add: fresh_def supp_Unit) + +instance prod :: (fs, fs) fs +apply default +apply (induct_tac x) +apply (simp add: supp_Pair finite_supp) +done + + +subsection {* Type @{typ "'a + 'b"} is finitely supported *} + +lemma supp_Inl: + shows "supp (Inl x) = supp x" + by (simp add: supp_def) + +lemma supp_Inr: + shows "supp (Inr x) = supp x" + by (simp add: supp_def) + +lemma fresh_Inl: + shows "a \ Inl x \ a \ x" + by (simp add: fresh_def supp_Inl) + +lemma fresh_Inr: + shows "a \ Inr y \ a \ y" + by (simp add: fresh_def supp_Inr) + +instance sum :: (fs, fs) fs +apply default +apply (induct_tac x) +apply (simp_all add: supp_Inl supp_Inr finite_supp) +done + + +subsection {* Type @{typ "'a option"} is finitely supported *} + +lemma supp_None: + shows "supp None = {}" +by (simp add: supp_def) + +lemma supp_Some: + shows "supp (Some x) = supp x" + by (simp add: supp_def) + +lemma fresh_None: + shows "a \ None" + by (simp add: fresh_def supp_None) + +lemma fresh_Some: + shows "a \ Some x \ a \ x" + by (simp add: fresh_def supp_Some) + +instance option :: (fs) fs +apply default +apply (induct_tac x) +apply (simp_all add: supp_None supp_Some finite_supp) +done + + +subsubsection {* Type @{typ "'a list"} is finitely supported *} + +lemma supp_Nil: + shows "supp [] = {}" + by (simp add: supp_def) + +lemma supp_Cons: + shows "supp (x # xs) = supp x \ supp xs" +by (simp add: supp_def Collect_imp_eq Collect_neg_eq) + +lemma fresh_Nil: + shows "a \ []" + by (simp add: fresh_def supp_Nil) + +lemma fresh_Cons: + shows "a \ (x # xs) \ a \ x \ a \ xs" + by (simp add: fresh_def supp_Cons) + +instance list :: (fs) fs +apply default +apply (induct_tac x) +apply (simp_all add: supp_Nil supp_Cons finite_supp) +done + + +section {* Support and Freshness for Applications *} + +lemma fresh_conv_MOST: + shows "a \ x \ (MOST b. (a \ b) \ x = x)" + 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 + by (elim MOST_rev_mp, simp) + +lemma supp_fun_app: + shows "supp (f x) \ (supp f) \ (supp x)" + using fresh_fun_app + unfolding fresh_def + by auto + +text {* Support of Equivariant Functions *} + +lemma supp_fun_eqvt: + assumes a: "\p. p \ f = f" + shows "supp f = {}" + unfolding supp_def + using a by simp + +lemma fresh_fun_eqvt_app: + assumes a: "\p. p \ f = f" + shows "a \ x \ a \ f x" +proof - + from a have "supp f = {}" by (simp add: supp_fun_eqvt) + then show "a \ x \ a \ f x" + unfolding fresh_def + using supp_fun_app by auto +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_finite_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_finite_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_finite_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_finite_supp_sets[OF fin]) +apply(rule Union_included_in_supp[OF fin]) +done + +lemma finite_sets_supp: + fixes S::"('a::fs set)" + assumes "finite S" + shows "finite (supp S)" +using assms +by (simp only: supp_of_finite_sets Union_of_finite_supp_sets) + +lemma supp_of_finite_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_finite_sets) + +lemma supp_of_finite_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_finite_sets) + + +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 + by (simp add: fset_eqvt fset_cong) + +lemma supp_empty_fset [simp]: + shows "supp {||} = {}" + unfolding supp_def + by simp + +lemma supp_insert_fset [simp]: + fixes x::"'a::fs" + and S::"'a fset" + shows "supp (insert_fset x S) = supp x \ supp S" + apply(subst supp_fset[symmetric]) + apply(simp add: supp_fset supp_of_finite_insert) + done + +lemma fset_finite_supp: + fixes S::"('a::fs) fset" + shows "finite (supp S)" + by (induct S) (simp_all add: finite_supp) + + +instance fset :: (fs) fs + apply (default) + apply (rule fset_finite_supp) + done + + +section {* Fresh-Star *} + + +text {* The fresh-star generalisation of fresh is used in strong + induction principles. *} + +definition + fresh_star :: "atom set \ 'a::pt \ bool" ("_ \* _" [80,80] 80) +where + "as \* x \ \a \ as. a \ x" + +lemma fresh_star_supp_conv: + shows "supp x \* y \ supp y \* x" +by (auto simp add: fresh_star_def fresh_def) + +lemma fresh_star_prod: + fixes as::"atom set" + shows "as \* (x, y) = (as \* x \ as \* y)" + by (auto simp add: fresh_star_def fresh_Pair) + +lemma fresh_star_union: + shows "(as \ bs) \* x = (as \* x \ bs \* x)" + by (auto simp add: fresh_star_def) + +lemma fresh_star_insert: + shows "(insert a as) \* x = (a \ x \ as \* x)" + by (auto simp add: fresh_star_def) + +lemma fresh_star_Un_elim: + "((as \ bs) \* x \ PROP C) \ (as \* x \ bs \* x \ PROP C)" + unfolding fresh_star_def + apply(rule) + apply(erule meta_mp) + apply(auto) + done + +lemma fresh_star_insert_elim: + "(insert a as \* x \ PROP C) \ (a \ x \ as \* x \ PROP C)" + unfolding fresh_star_def + by rule (simp_all add: fresh_star_def) + +lemma fresh_star_empty_elim: + "({} \* x \ PROP C) \ PROP C" + by (simp add: fresh_star_def) + +lemma fresh_star_unit_elim: + shows "(a \* () \ PROP C) \ PROP C" + by (simp add: fresh_star_def fresh_Unit) + +lemma fresh_star_prod_elim: + shows "(a \* (x, y) \ PROP C) \ (a \* x \ a \* y \ PROP C)" + by (rule, simp_all add: fresh_star_prod) + +lemma fresh_star_zero: + shows "as \* (0::perm)" + unfolding fresh_star_def + by (simp add: fresh_zero_perm) + +lemma fresh_star_plus: + fixes p q::perm + shows "\a \* p; a \* q\ \ a \* (p + q)" + unfolding fresh_star_def + by (simp add: fresh_plus_perm) + +lemma fresh_star_permute_iff: + shows "(p \ a) \* (p \ x) \ a \* x" + unfolding fresh_star_def + by (metis mem_permute_iff permute_minus_cancel(1) fresh_permute_iff) + +lemma fresh_star_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 + + +section {* Induction principle for permutations *} + + +lemma perm_struct_induct[consumes 1, case_names zero swap]: + assumes S: "supp p \ S" + and zero: "P 0" + and swap: "\p a b. \P p; supp p \ S; a \ S; b \ S; a \ b; sort_of a = sort_of b\ \ P ((a \ b) + p)" + shows "P p" +proof - + have "finite (supp p)" by (simp add: finite_supp) + then show "P p" using S + proof(induct A\"supp p" arbitrary: p rule: finite_psubset_induct) + case (psubset p) + 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 p" using zero by simp + } + moreover + { assume "supp p \ {}" + then obtain a where a0: "a \ supp p" by blast + then have a1: "p \ a \ S" "a \ S" "sort_of (p \ a) = sort_of a" "p \ a \ a" + using as by (auto simp add: supp_atom supp_perm swap_atom) + let ?q = "(p \ a \ a) + p" + have a2: "supp ?q \ supp p" unfolding supp_perm by (auto simp add: swap_atom) + moreover + have "a \ supp ?q" by (simp add: supp_perm) + then have "supp ?q \ supp p" using a0 by auto + ultimately have "supp ?q \ supp p" using a2 by auto + then have "P ?q" using ih by simp + moreover + 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) + ultimately have "P p" by simp + } + ultimately show "P p" by blast + qed +qed + +lemma perm_simple_struct_induct[case_names zero swap]: + assumes zero: "P 0" + and swap: "\p a b. \P p; a \ b; sort_of a = sort_of b\ \ P ((a \ b) + p)" + shows "P p" +by (rule_tac S="supp p" in perm_struct_induct) + (auto intro: zero swap) + +lemma perm_subset_induct[consumes 1, case_names zero swap plus]: + assumes S: "supp p \ S" + assumes zero: "P 0" + assumes swap: "\a b. \sort_of a = sort_of b; a \ b; a \ S; b \ S\ \ P (a \ b)" + assumes plus: "\p1 p2. \P p1; P p2; supp p1 \ S; supp p2 \ S\ \ P (p1 + p2)" + shows "P p" +using S +by (induct p rule: perm_struct_induct) + (auto intro: zero plus swap simp add: supp_swap) + +lemma supp_perm_eq: + assumes "(supp x) \* p" + shows "p \ x = x" +proof - + from assms have "supp p \ {a. a \ x}" + unfolding supp_perm fresh_star_def fresh_def by auto + then show "p \ x = x" + proof (induct p rule: perm_struct_induct) + case zero + show "0 \ x = x" by simp + next + case (swap p a b) + then have "a \ x" "b \ x" "p \ x = x" by simp_all + then show "((a \ b) + p) \ x = x" by (simp add: swap_fresh_fresh) + qed +qed + +lemma supp_perm_eq_test: + assumes "(supp x) \* p" + shows "p \ x = x" +proof - + from assms have "supp p \ {a. a \ x}" + unfolding supp_perm fresh_star_def fresh_def by auto + then show "p \ x = x" + proof (induct p rule: perm_subset_induct) + case zero + show "0 \ x = x" by simp + next + case (swap a b) + then have "a \ x" "b \ x" by simp_all + then show "(a \ b) \ x = x" by (simp add: swap_fresh_fresh) + next + case (plus p1 p2) + have "p1 \ x = x" "p2 \ x = x" by fact+ + then show "(p1 + p2) \ x = x" by simp + qed +qed + + +section {* Avoiding of atom sets *} + +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::"atom set" + and As::"atom set" + assumes b: "Xs \ As" + and c: "finite As" + shows "\p. (p \ Xs) \ As = {} \ (supp p) \ (Xs \ (p \ Xs))" +proof - + from b c have "finite Xs" by (rule finite_subset) + then show ?thesis using b + proof (induct rule: finite_subset_induct) + case empty + have "0 \ {} \ As = {}" by simp + moreover + have "supp (0::perm) \ {} \ 0 \ {}" by (simp add: supp_zero_perm) + ultimately show ?case by blast + next + case (insert x Xs) + then obtain p where + p1: "(p \ Xs) \ As = {}" and + p2: "supp p \ (Xs \ (p \ Xs))" by blast + from `x \ As` p1 have "x \ p \ Xs" by fast + with `x \ Xs` p2 have "x \ supp p" by fast + hence px: "p \ x = x" unfolding supp_perm by simp + have "finite (As \ p \ Xs)" + using `finite As` `finite Xs` + by (simp add: permute_set_eq_image) + then obtain y where "y \ (As \ p \ Xs)" "sort_of y = sort_of x" + by (rule obtain_atom) + hence y: "y \ As" "y \ p \ Xs" "sort_of y = sort_of x" + by simp_all + let ?q = "(x \ y) + p" + have q: "?q \ insert x Xs = insert y (p \ Xs)" + unfolding insert_eqvt + using `p \ x = x` `sort_of y = sort_of x` + using `x \ p \ Xs` `y \ p \ Xs` + by (simp add: swap_atom swap_set_not_in) + have "?q \ insert x Xs \ As = {}" + using `y \ As` `p \ Xs \ As = {}` + unfolding q by simp + moreover + have "supp ?q \ insert x Xs \ ?q \ insert x Xs" + using p2 unfolding q + by (intro subset_trans [OF supp_plus_perm]) + (auto simp add: supp_swap) + ultimately show ?case by blast + qed +qed + +lemma at_set_avoiding: + assumes a: "finite Xs" + and b: "finite (supp c)" + obtains p::"perm" where "(p \ Xs)\*c" and "(supp p) \ (Xs \ (p \ Xs))" + using a b at_set_avoiding_aux [where Xs="Xs" and As="Xs \ supp c"] + unfolding fresh_star_def fresh_def by blast + +lemma at_set_avoiding2: + assumes "finite xs" + and "finite (supp c)" "finite (supp x)" + and "xs \* x" + shows "\p. (p \ xs) \* c \ supp x \* p" +using assms +apply(erule_tac c="(c, x)" in at_set_avoiding) +apply(simp add: supp_Pair) +apply(rule_tac x="p" in exI) +apply(simp add: fresh_star_prod) +apply(rule fresh_star_supp_conv) +apply(auto simp add: fresh_star_def) +done + +lemma at_set_avoiding2_atom: + assumes "finite (supp c)" "finite (supp x)" + and b: "a \ x" + shows "\p. (p \ a) \ c \ supp x \* p" +proof - + have a: "{a} \* x" unfolding fresh_star_def by (simp add: b) + obtain p where p1: "(p \ {a}) \* c" and p2: "supp x \* p" + using at_set_avoiding2[of "{a}" "c" "x"] assms a by blast + have c: "(p \ a) \ c" using p1 + unfolding fresh_star_def Ball_def + by(erule_tac x="p \ a" in allE) (simp add: permute_set_eq) + hence "p \ a \ c \ supp x \* p" using p2 by blast + then show "\p. (p \ a) \ c \ supp x \* p" by blast +qed + + +section {* Concrete Atoms Types *} + +text {* + Class @{text at_base} allows types containing multiple sorts of atoms. + Class @{text at} only allows types with a single sort. +*} + +class at_base = pt + + fixes atom :: "'a \ atom" + assumes atom_eq_iff [simp]: "atom a = atom b \ a = b" + assumes atom_eqvt: "p \ (atom a) = atom (p \ a)" + +class at = at_base + + assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)" + +lemma supp_at_base: + fixes a::"'a::at_base" + shows "supp a = {atom a}" + by (simp add: supp_atom [symmetric] supp_def atom_eqvt) + +lemma fresh_at_base: + shows "a \ b \ a \ atom b" + unfolding fresh_def by (simp add: supp_at_base) + +instance at_base < fs +proof qed (simp add: supp_at_base) + +lemma at_base_infinite [simp]: + shows "infinite (UNIV :: 'a::at_base set)" (is "infinite ?U") +proof + obtain a :: 'a where "True" by auto + assume "finite ?U" + hence "finite (atom ` ?U)" + by (rule finite_imageI) + then obtain b where b: "b \ atom ` ?U" "sort_of b = sort_of (atom a)" + by (rule obtain_atom) + from b(2) have "b = atom ((atom a \ b) \ a)" + unfolding atom_eqvt [symmetric] + by (simp add: swap_atom) + hence "b \ atom ` ?U" by simp + with b(1) show "False" by simp +qed + +lemma swap_at_base_simps [simp]: + fixes x y::"'a::at_base" + shows "sort_of (atom x) = sort_of (atom y) \ (atom x \ atom y) \ x = y" + and "sort_of (atom x) = sort_of (atom y) \ (atom x \ atom y) \ y = x" + and "atom x \ a \ atom x \ b \ (a \ b) \ x = x" + unfolding atom_eq_iff [symmetric] + unfolding atom_eqvt [symmetric] + by simp_all + +lemma obtain_at_base: + assumes X: "finite X" + obtains a::"'a::at_base" where "atom a \ X" +proof - + have "inj (atom :: 'a \ atom)" + by (simp add: inj_on_def) + with X have "finite (atom -` X :: 'a set)" + by (rule finite_vimageI) + with at_base_infinite have "atom -` X \ (UNIV :: 'a set)" + by auto + then obtain a :: 'a where "atom a \ X" + by auto + thus ?thesis .. +qed + +lemma supp_finite_set_at_base: + assumes a: "finite S" + shows "supp S = atom ` S" +apply(simp add: supp_of_finite_sets[OF a]) +apply(simp add: supp_at_base) +apply(auto) +done + +section {* Infrastructure for concrete atom types *} + +section {* A swapping operation for concrete atoms *} + +definition + flip :: "'a::at_base \ 'a \ perm" ("'(_ \ _')") +where + "(a \ b) = (atom a \ atom b)" + +lemma flip_self [simp]: "(a \ a) = 0" + unfolding flip_def by (rule swap_self) + +lemma flip_commute: "(a \ b) = (b \ a)" + unfolding flip_def by (rule swap_commute) + +lemma minus_flip [simp]: "- (a \ b) = (a \ b)" + unfolding flip_def by (rule minus_swap) + +lemma add_flip_cancel: "(a \ b) + (a \ b) = 0" + unfolding flip_def by (rule swap_cancel) + +lemma permute_flip_cancel [simp]: "(a \ b) \ (a \ b) \ x = x" + unfolding permute_plus [symmetric] add_flip_cancel by simp + +lemma permute_flip_cancel2 [simp]: "(a \ b) \ (b \ a) \ x = x" + by (simp add: flip_commute) + +lemma flip_eqvt: + fixes a b c::"'a::at_base" + shows "p \ (a \ b) = (p \ a \ p \ b)" + unfolding flip_def + by (simp add: swap_eqvt atom_eqvt) + +lemma flip_at_base_simps [simp]: + shows "sort_of (atom a) = sort_of (atom b) \ (a \ b) \ a = b" + and "sort_of (atom a) = sort_of (atom b) \ (a \ b) \ b = a" + and "\a \ c; b \ c\ \ (a \ b) \ c = c" + and "sort_of (atom a) \ sort_of (atom b) \ (a \ b) \ x = x" + unfolding flip_def + unfolding atom_eq_iff [symmetric] + unfolding atom_eqvt [symmetric] + by simp_all + +text {* the following two lemmas do not hold for at_base, + only for single sort atoms from at *} + +lemma permute_flip_at: + fixes a b c::"'a::at" + shows "(a \ b) \ c = (if c = a then b else if c = b then a else c)" + unfolding flip_def + apply (rule atom_eq_iff [THEN iffD1]) + apply (subst atom_eqvt [symmetric]) + apply (simp add: swap_atom) + done + +lemma flip_at_simps [simp]: + fixes a b::"'a::at" + shows "(a \ b) \ a = b" + and "(a \ b) \ b = a" + unfolding permute_flip_at by simp_all + +lemma flip_fresh_fresh: + fixes a b::"'a::at_base" + assumes "atom a \ x" "atom b \ x" + shows "(a \ b) \ x = x" +using assms +by (simp add: flip_def swap_fresh_fresh) + +subsection {* Syntax for coercing at-elements to the atom-type *} + +syntax + "_atom_constrain" :: "logic \ type \ logic" ("_:::_" [4, 0] 3) + +translations + "_atom_constrain a t" => "CONST atom (_constrain a t)" + + +subsection {* A lemma for proving instances of class @{text at}. *} + +setup {* Sign.add_const_constraint (@{const_name "permute"}, NONE) *} +setup {* Sign.add_const_constraint (@{const_name "atom"}, NONE) *} + +text {* + New atom types are defined as subtypes of @{typ atom}. +*} + +lemma exists_eq_simple_sort: + shows "\a. a \ {a. sort_of a = s}" + by (rule_tac x="Atom s 0" in exI, simp) + +lemma exists_eq_sort: + shows "\a. a \ {a. sort_of a \ range sort_fun}" + by (rule_tac x="Atom (sort_fun x) y" in exI, simp) + +lemma at_base_class: + fixes sort_fun :: "'b \atom_sort" + fixes Rep :: "'a \ atom" and Abs :: "atom \ 'a" + assumes type: "type_definition Rep Abs {a. sort_of a \ range sort_fun}" + assumes atom_def: "\a. atom a = Rep a" + assumes permute_def: "\p a. p \ a = Abs (p \ Rep a)" + shows "OFCLASS('a, at_base_class)" +proof + interpret type_definition Rep Abs "{a. sort_of a \ range sort_fun}" by (rule type) + have sort_of_Rep: "\a. sort_of (Rep a) \ range sort_fun" using Rep by simp + fix a b :: 'a and p p1 p2 :: perm + show "0 \ a = a" + unfolding permute_def by (simp add: Rep_inverse) + show "(p1 + p2) \ a = p1 \ p2 \ a" + unfolding permute_def by (simp add: Abs_inverse sort_of_Rep) + show "atom a = atom b \ a = b" + unfolding atom_def by (simp add: Rep_inject) + show "p \ atom a = atom (p \ a)" + unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep) +qed + +(* +lemma at_class: + fixes s :: atom_sort + fixes Rep :: "'a \ atom" and Abs :: "atom \ 'a" + assumes type: "type_definition Rep Abs {a. sort_of a \ range (\x::unit. s)}" + assumes atom_def: "\a. atom a = Rep a" + assumes permute_def: "\p a. p \ a = Abs (p \ Rep a)" + shows "OFCLASS('a, at_class)" +proof + interpret type_definition Rep Abs "{a. sort_of a \ range (\x::unit. s)}" by (rule type) + have sort_of_Rep: "\a. sort_of (Rep a) = s" using Rep by (simp add: image_def) + fix a b :: 'a and p p1 p2 :: perm + show "0 \ a = a" + unfolding permute_def by (simp add: Rep_inverse) + show "(p1 + p2) \ a = p1 \ p2 \ a" + unfolding permute_def by (simp add: Abs_inverse sort_of_Rep) + show "sort_of (atom a) = sort_of (atom b)" + unfolding atom_def by (simp add: sort_of_Rep) + show "atom a = atom b \ a = b" + unfolding atom_def by (simp add: Rep_inject) + show "p \ atom a = atom (p \ a)" + unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep) +qed +*) + +lemma at_class: + fixes s :: atom_sort + fixes Rep :: "'a \ atom" and Abs :: "atom \ 'a" + assumes type: "type_definition Rep Abs {a. sort_of a = s}" + assumes atom_def: "\a. atom a = Rep a" + assumes permute_def: "\p a. p \ a = Abs (p \ Rep a)" + shows "OFCLASS('a, at_class)" +proof + interpret type_definition Rep Abs "{a. sort_of a = s}" by (rule type) + have sort_of_Rep: "\a. sort_of (Rep a) = s" using Rep by (simp add: image_def) + fix a b :: 'a and p p1 p2 :: perm + show "0 \ a = a" + unfolding permute_def by (simp add: Rep_inverse) + show "(p1 + p2) \ a = p1 \ p2 \ a" + unfolding permute_def by (simp add: Abs_inverse sort_of_Rep) + show "sort_of (atom a) = sort_of (atom b)" + unfolding atom_def by (simp add: sort_of_Rep) + show "atom a = atom b \ a = b" + unfolding atom_def by (simp add: Rep_inject) + show "p \ atom a = atom (p \ a)" + unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep) +qed + +setup {* Sign.add_const_constraint + (@{const_name "permute"}, SOME @{typ "perm \ 'a::pt \ 'a"}) *} +setup {* Sign.add_const_constraint + (@{const_name "atom"}, SOME @{typ "'a::at_base \ atom"}) *} + + + +section {* The freshness lemma according to Andy Pitts *} + +lemma freshness_lemma: + fixes h :: "'a::at \ 'b::pt" + assumes a: "\a. atom a \ (h, h a)" + shows "\x. \a. atom a \ h \ h a = x" +proof - + from a obtain b where a1: "atom b \ h" and a2: "atom b \ h b" + by (auto simp add: fresh_Pair) + show "\x. \a. atom a \ h \ h a = x" + proof (intro exI allI impI) + fix a :: 'a + assume a3: "atom a \ h" + show "h a = h b" + proof (cases "a = b") + assume "a = b" + thus "h a = h b" by simp + next + assume "a \ b" + hence "atom a \ b" by (simp add: fresh_at_base) + with a3 have "atom a \ h b" + by (rule fresh_fun_app) + with a2 have d1: "(atom b \ atom a) \ (h b) = (h b)" + by (rule swap_fresh_fresh) + from a1 a3 have d2: "(atom b \ atom a) \ h = h" + by (rule swap_fresh_fresh) + from d1 have "h b = (atom b \ atom a) \ (h b)" by simp + also have "\ = ((atom b \ atom a) \ h) ((atom b \ atom a) \ b)" + by (rule permute_fun_app_eq) + also have "\ = h a" + using d2 by simp + finally show "h a = h b" by simp + qed + qed +qed + +lemma freshness_lemma_unique: + fixes h :: "'a::at \ 'b::pt" + assumes a: "\a. atom a \ (h, h a)" + shows "\!x. \a. atom a \ h \ h a = x" +proof (rule ex_ex1I) + from a show "\x. \a. atom a \ h \ h a = x" + by (rule freshness_lemma) +next + fix x y + assume x: "\a. atom a \ h \ h a = x" + assume y: "\a. atom a \ h \ h a = y" + from a x y show "x = y" + by (auto simp add: fresh_Pair) +qed + +text {* packaging the freshness lemma into a function *} + +definition + fresh_fun :: "('a::at \ 'b::pt) \ 'b" +where + "fresh_fun h = (THE x. \a. atom a \ h \ h a = x)" + +lemma fresh_fun_apply: + fixes h :: "'a::at \ 'b::pt" + assumes a: "\a. atom a \ (h, h a)" + assumes b: "atom a \ h" + shows "fresh_fun h = h a" +unfolding fresh_fun_def +proof (rule the_equality) + show "\a'. atom a' \ h \ h a' = h a" + proof (intro strip) + fix a':: 'a + assume c: "atom a' \ h" + from a have "\x. \a. atom a \ h \ h a = x" by (rule freshness_lemma) + with b c show "h a' = h a" by auto + qed +next + fix fr :: 'b + assume "\a. atom a \ h \ h a = fr" + with b show "fr = h a" by auto +qed + +lemma fresh_fun_apply': + fixes h :: "'a::at \ 'b::pt" + assumes a: "atom a \ h" "atom a \ h a" + shows "fresh_fun h = h a" + apply (rule fresh_fun_apply) + apply (auto simp add: fresh_Pair intro: a) + done + +lemma fresh_fun_eqvt: + fixes h :: "'a::at \ 'b::pt" + assumes a: "\a. atom a \ (h, h a)" + shows "p \ (fresh_fun h) = fresh_fun (p \ h)" + using a + apply (clarsimp simp add: fresh_Pair) + apply (subst fresh_fun_apply', assumption+) + apply (drule fresh_permute_iff [where p=p, THEN iffD2]) + apply (drule fresh_permute_iff [where p=p, THEN iffD2]) + apply (simp add: atom_eqvt permute_fun_app_eq [where f=h]) + apply (erule (1) fresh_fun_apply' [symmetric]) + done + +lemma fresh_fun_supports: + fixes h :: "'a::at \ 'b::pt" + assumes a: "\a. atom a \ (h, h a)" + shows "(supp h) supports (fresh_fun h)" + apply (simp add: supports_def fresh_def [symmetric]) + apply (simp add: fresh_fun_eqvt [OF a] swap_fresh_fresh) + done + +notation fresh_fun (binder "FRESH " 10) + +lemma FRESH_f_iff: + fixes P :: "'a::at \ 'b::pure" + fixes f :: "'b \ 'c::pure" + assumes P: "finite (supp P)" + shows "(FRESH x. f (P x)) = f (FRESH x. P x)" +proof - + obtain a::'a where "atom a \ supp P" + using P by (rule obtain_at_base) + hence "atom a \ P" + by (simp add: fresh_def) + show "(FRESH x. f (P x)) = f (FRESH x. P x)" + apply (subst fresh_fun_apply' [where a=a, OF _ pure_fresh]) + apply (cut_tac `atom a \ P`) + apply (simp add: fresh_conv_MOST) + apply (elim MOST_rev_mp, rule MOST_I, clarify) + apply (simp add: permute_fun_def permute_pure fun_eq_iff) + apply (subst fresh_fun_apply' [where a=a, OF `atom a \ P` pure_fresh]) + apply (rule refl) + done +qed + +lemma FRESH_binop_iff: + fixes P :: "'a::at \ 'b::pure" + fixes Q :: "'a::at \ 'c::pure" + fixes binop :: "'b \ 'c \ 'd::pure" + assumes P: "finite (supp P)" + and Q: "finite (supp Q)" + shows "(FRESH x. binop (P x) (Q x)) = binop (FRESH x. P x) (FRESH x. Q x)" +proof - + from assms have "finite (supp P \ supp Q)" by simp + then obtain a::'a where "atom a \ (supp P \ supp Q)" + by (rule obtain_at_base) + hence "atom a \ P" and "atom a \ Q" + by (simp_all add: fresh_def) + show ?thesis + apply (subst fresh_fun_apply' [where a=a, OF _ pure_fresh]) + apply (cut_tac `atom a \ P` `atom a \ Q`) + apply (simp add: fresh_conv_MOST) + apply (elim MOST_rev_mp, rule MOST_I, clarify) + apply (simp add: permute_fun_def permute_pure fun_eq_iff) + apply (subst fresh_fun_apply' [where a=a, OF `atom a \ P` pure_fresh]) + apply (subst fresh_fun_apply' [where a=a, OF `atom a \ Q` pure_fresh]) + apply (rule refl) + done +qed + +lemma FRESH_conj_iff: + fixes P Q :: "'a::at \ bool" + assumes P: "finite (supp P)" and Q: "finite (supp Q)" + shows "(FRESH x. P x \ Q x) \ (FRESH x. P x) \ (FRESH x. Q x)" +using P Q by (rule FRESH_binop_iff) + +lemma FRESH_disj_iff: + fixes P Q :: "'a::at \ bool" + assumes P: "finite (supp P)" and Q: "finite (supp Q)" + shows "(FRESH x. P x \ Q x) \ (FRESH x. P x) \ (FRESH x. Q x)" +using P Q by (rule FRESH_binop_iff) + + +section {* Library functions for the nominal infrastructure *} + +use "nominal_library.ML" + + +section {* Automation for creating concrete atom types *} + +text {* at the moment only single-sort concrete atoms are supported *} + +use "nominal_atoms.ML" + + + +end diff -r 41137dc935ff -r 8193bbaa07fe Nominal/Nominal2_Eqvt.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Nominal2_Eqvt.thy Sun Nov 14 16:34:47 2010 +0000 @@ -0,0 +1,382 @@ +(* 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 imp_eqvt + imp_eqvt[folded induct_implies_def] + uminus_eqvt + + (* nominal *) + supp_eqvt fresh_eqvt fresh_star_eqvt add_perm_eqvt atom_eqvt + swap_eqvt flip_eqvt + + (* datatypes *) + Pair_eqvt permute_list.simps + + (* sets *) + mem_eqvt empty_eqvt insert_eqvt set_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_eqvt[eqvt]: + shows "p \ (\!x. P x) = (\!x. (p \ P) x)" + unfolding Ex1_def + by (perm_simp) (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 (- 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 supp_set_empty: + shows "supp {} = {}" + unfolding supp_def + by (simp add: empty_eqvt) + +lemma fresh_set_empty: + shows "a \ {}" + by (simp add: fresh_def supp_set_empty) + +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 inter_eqvt[eqvt]: + shows "p \ (A \ B) = (p \ A) \ (p \ B)" + unfolding Int_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 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 + by (perm_simp) (rule refl) + +lemma Union_eqvt[eqvt]: + shows "p \ (\ S) = \ (p \ S)" + unfolding Union_eq + 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 .. + +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_finite_insert) +done + + +section {* List Operations *} + +lemma append_eqvt[eqvt]: + shows "p \ (xs @ ys) = (p \ xs) @ (p \ ys)" + by (induct xs) auto + +lemma supp_append: + shows "supp (xs @ ys) = supp xs \ supp ys" + by (induct xs) (auto simp add: supp_Nil supp_Cons) + +lemma fresh_append: + shows "a \ (xs @ ys) \ a \ xs \ a \ ys" + by (induct xs) (simp_all add: fresh_Nil fresh_Cons) + +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) + + +subsection {* Equivariance for fsets *} + +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 41137dc935ff -r 8193bbaa07fe Nominal/ROOT.ML --- a/Nominal/ROOT.ML Sun Nov 14 12:09:14 2010 +0000 +++ b/Nominal/ROOT.ML Sun Nov 14 16:34:47 2010 +0000 @@ -1,7 +1,8 @@ no_document use_thys - ["../Nominal-General/Atoms", + ["Atoms", + "Nominal2_Abs", "Ex/Classical", "Ex/Datatypes", "Ex/Ex1", diff -r 41137dc935ff -r 8193bbaa07fe Nominal/nominal_atoms.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/nominal_atoms.ML Sun Nov 14 16:34:47 2010 +0000 @@ -0,0 +1,83 @@ +(* Title: nominal_atoms/ML + Authors: Brian Huffman, Christian Urban + + Command for defining concrete atom types. + + At the moment, only single-sorted atom types + are supported. +*) + +signature ATOM_DECL = +sig + val add_atom_decl: (binding * (binding option)) -> theory -> theory +end; + +structure Atom_Decl :> ATOM_DECL = +struct + +fun atom_decl_set (str : string) : term = + let + val a = Free ("a", @{typ atom}); + val s = Const (@{const_name "Sort"}, @{typ "string => atom_sort list => atom_sort"}) + $ HOLogic.mk_string str $ HOLogic.nil_const @{typ "atom_sort"}; + in + HOLogic.mk_Collect ("a", @{typ atom}, HOLogic.mk_eq (mk_sort_of a, s)) + end + +fun add_atom_decl (name : binding, arg : binding option) (thy : theory) = + let + val _ = Theory.requires thy "Nominal2_Base" "nominal logic"; + val str = Sign.full_name thy name; + + (* typedef *) + val set = atom_decl_set str; + val tac = rtac @{thm exists_eq_simple_sort} 1; + val ((full_tname, info as ({Rep_name, Abs_name, ...}, {type_definition, ...})), thy) = + Typedef.add_typedef_global false NONE (name, [], NoSyn) set NONE tac thy; + + (* definition of atom and permute *) + val newT = #abs_type (fst info); + val RepC = Const (Rep_name, newT --> @{typ atom}); + val AbsC = Const (Abs_name, @{typ atom} --> newT); + val a = Free ("a", newT); + val p = Free ("p", @{typ perm}); + val atom_eqn = + HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_atom a, RepC $ a)); + val permute_eqn = + HOLogic.mk_Trueprop (HOLogic.mk_eq + (mk_perm p a, AbsC $ (mk_perm p (RepC $ a)))); + val atom_def_name = + Binding.prefix_name "atom_" (Binding.suffix_name "_def" name); + val permute_def_name = + Binding.prefix_name "permute_" (Binding.suffix_name "_def" name); + + (* at class instance *) + val lthy = + Class.instantiation ([full_tname], [], @{sort at}) thy; + val ((_, (_, permute_ldef)), lthy) = + Specification.definition (NONE, ((permute_def_name, []), permute_eqn)) lthy; + val ((_, (_, atom_ldef)), lthy) = + Specification.definition (NONE, ((atom_def_name, []), atom_eqn)) lthy; + val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy); + val permute_def = singleton (ProofContext.export lthy ctxt_thy) permute_ldef; + val atom_def = singleton (ProofContext.export lthy ctxt_thy) atom_ldef; + val class_thm = @{thm at_class} OF [type_definition, atom_def, permute_def]; + val thy = lthy + |> Class.prove_instantiation_instance (K (Tactic.rtac class_thm 1)) + |> Local_Theory.exit_global; + in + thy + end; + +(** outer syntax **) + +local structure P = Parse and K = Keyword in + +val _ = + Outer_Syntax.command "atom_decl" "declaration of a concrete atom type" K.thy_decl + ((P.binding -- Scan.option (Args.parens (P.binding))) >> + (Toplevel.print oo (Toplevel.theory o add_atom_decl))); + +end; + +end; diff -r 41137dc935ff -r 8193bbaa07fe Nominal/nominal_eqvt.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/nominal_eqvt.ML Sun Nov 14 16:34:47 2010 +0000 @@ -0,0 +1,142 @@ +(* Title: nominal_eqvt.ML + Author: Stefan Berghofer (original code) + Author: Christian Urban + + Automatic proofs for equivariance of inductive predicates. +*) + +signature NOMINAL_EQVT = +sig + val eqvt_rel_tac: Proof.context -> string list -> term -> thm -> thm list -> int -> tactic + val eqvt_rel_single_case_tac: Proof.context -> string list -> term -> thm -> int -> tactic + + val equivariance: bool -> term list -> thm -> thm list -> Proof.context -> thm list * local_theory + val equivariance_cmd: string -> Proof.context -> local_theory +end + +structure Nominal_Eqvt : NOMINAL_EQVT = +struct + +open Nominal_Permeq; +open Nominal_ThmDecls; + +val atomize_conv = + MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE)) + (HOL_basic_ss addsimps @{thms induct_atomize}); +val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv); +fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1 + (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt)); + + +(** equivariance tactics **) + +val perm_boolE = @{thm permute_boolE} +val perm_cancel = @{thms permute_minus_cancel(2)} + +fun eqvt_rel_single_case_tac ctxt pred_names pi intro = + let + val thy = ProofContext.theory_of ctxt + val cpi = Thm.cterm_of thy (mk_minus pi) + val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE + val simps1 = HOL_basic_ss addsimps @{thms permute_fun_def minus_minus split_paired_all} + val simps2 = HOL_basic_ss addsimps @{thms permute_bool_def} + in + eqvt_strict_tac ctxt [] pred_names THEN' + SUBPROOF (fn {prems, context as ctxt, ...} => + let + val prems' = map (transform_prem2 ctxt pred_names) prems + val tac1 = resolve_tac prems' + val tac2 = EVERY' [ rtac pi_intro_rule, + eqvt_strict_tac ctxt perm_cancel pred_names, resolve_tac prems' ] + val tac3 = EVERY' [ rtac pi_intro_rule, + eqvt_strict_tac ctxt perm_cancel pred_names, simp_tac simps1, + simp_tac simps2, resolve_tac prems'] + in + (rtac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3]) 1 + end) ctxt + end + +fun eqvt_rel_tac ctxt pred_names pi induct intros = + let + val cases = map (eqvt_rel_single_case_tac ctxt pred_names pi) intros + in + EVERY' (rtac induct :: cases) + end + + +(** equivariance procedure *) + +fun prepare_goal pi pred = + let + val (c, xs) = strip_comb pred; + in + HOLogic.mk_imp (pred, list_comb (c, map (mk_perm pi) xs)) + end + +(* stores thm under name.eqvt and adds [eqvt]-attribute *) + +fun note_named_thm (name, thm) ctxt = + let + val thm_name = Binding.qualified_name + (Long_Name.qualify (Long_Name.base_name name) "eqvt") + val attr = Attrib.internal (K eqvt_add) + val ((_, [thm']), ctxt') = Local_Theory.note ((thm_name, [attr]), [thm]) ctxt + in + (thm', ctxt') + end + +fun equivariance note_flag pred_trms raw_induct intrs ctxt = + let + val is_already_eqvt = + filter (is_eqvt ctxt) pred_trms + |> map (Syntax.string_of_term ctxt) + val _ = if null is_already_eqvt then () + else error ("Already equivariant: " ^ commas is_already_eqvt) + + val pred_names = map (fst o dest_Const) pred_trms + val raw_induct' = atomize_induct ctxt raw_induct + val intrs' = map atomize_intr intrs + + val (([raw_concl], [raw_pi]), ctxt') = + ctxt + |> Variable.import_terms false [concl_of raw_induct'] + ||>> Variable.variant_fixes ["p"] + val pi = Free (raw_pi, @{typ perm}) + + val preds = map (fst o HOLogic.dest_imp) + (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl)); + + val goal = HOLogic.mk_Trueprop + (foldr1 HOLogic.mk_conj (map (prepare_goal pi) preds)) + + val thms = Goal.prove ctxt' [] [] goal + (fn {context,...} => eqvt_rel_tac context pred_names pi raw_induct' intrs' 1) + |> Datatype_Aux.split_conj_thm + |> ProofContext.export ctxt' ctxt + |> map (fn th => th RS mp) + |> map zero_var_indexes + in + if note_flag + then fold_map note_named_thm (pred_names ~~ thms) ctxt + else (thms, ctxt) + end + +fun equivariance_cmd pred_name ctxt = + let + val thy = ProofContext.theory_of ctxt + val (_, {preds, raw_induct, intrs, ...}) = + Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) + in + equivariance true preds raw_induct intrs ctxt |> snd + end + +local structure P = Parse and K = Keyword in + +val _ = + Outer_Syntax.local_theory "equivariance" + "Proves equivariance for inductive predicate involving nominal datatypes." + K.thy_decl (P.xname >> equivariance_cmd); + +end; + +end (* structure *) diff -r 41137dc935ff -r 8193bbaa07fe Nominal/nominal_library.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/nominal_library.ML Sun Nov 14 16:34:47 2010 +0000 @@ -0,0 +1,372 @@ +(* Title: nominal_library.ML + Author: Christian Urban + + Basic functions for nominal. +*) + +signature NOMINAL_LIBRARY = +sig + val is_true: term -> bool + + val last2: 'a list -> 'a * 'a + + val dest_listT: typ -> typ + + val size_const: typ -> 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 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 mk_atom_ty: typ -> term -> term + val mk_atom: term -> term + + val supp_ty: typ -> typ + val supp_const: typ -> term + val mk_supp_ty: typ -> term -> term + val mk_supp: term -> term + + val supp_rel_ty: typ -> typ + val supp_rel_const: typ -> term + val mk_supp_rel_ty: typ -> term -> term -> term + val mk_supp_rel: term -> term -> term + + val supports_const: typ -> term + val mk_supports_ty: typ -> term -> term -> term + val mk_supports: term -> term -> term + + val finite_const: typ -> term + 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 + val fold_union: term list -> term + val fold_append: term list -> term + val mk_conj: term * term -> term + val fold_conj: term list -> term + + (* fresh arguments for a term *) + val fresh_args: Proof.context -> term -> term list + + (* datatype operations *) + type cns_info = (term * typ * typ list * bool list) list + + val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list + val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ + val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> cns_info list + val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> cns_info + val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list + + (* tactics for function package *) + val pat_completeness_simp: thm list -> Proof.context -> tactic + val prove_termination: thm list -> Proof.context -> Function.info * local_theory + + (* transformations of premises in inductions *) + val transform_prem1: Proof.context -> string list -> thm -> thm + val transform_prem2: Proof.context -> string list -> thm -> thm + + (* transformation into the object logic *) + val atomize: thm -> thm + +end + + +structure Nominal_Library: NOMINAL_LIBRARY = +struct + +fun is_true @{term "Trueprop True"} = true + | is_true _ = false + +fun last2 [] = raise Empty + | last2 [_] = raise Empty + | last2 [x, y] = (x, y) + | last2 (_ :: xs) = last2 xs + +fun dest_listT (Type (@{type_name list}, [T])) = T + | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []) + +fun size_const ty = Const (@{const_name size}, ty --> @{typ nat}) + +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 mk_perm_ty ty p trm = Const (@{const_name "permute"}, perm_ty 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"}; +fun mk_atom_ty ty t = Const (@{const_name "atom"}, atom_ty ty) $ t; +fun mk_atom t = mk_atom_ty (fastype_of t) t; + + +fun supp_ty ty = ty --> @{typ "atom set"}; +fun supp_const ty = Const (@{const_name supp}, supp_ty ty) +fun mk_supp_ty ty t = supp_const ty $ t +fun mk_supp t = mk_supp_ty (fastype_of t) t + +fun supp_rel_ty ty = ([ty, ty] ---> @{typ bool}) --> ty --> @{typ "atom set"}; +fun supp_rel_const ty = Const (@{const_name supp_rel}, supp_rel_ty ty) +fun mk_supp_rel_ty ty r t = supp_rel_const ty $ r $ t +fun mk_supp_rel r t = mk_supp_rel_ty (fastype_of t) r t + +fun supports_const ty = Const (@{const_name supports}, [@{typ "atom set"}, ty] ---> @{typ bool}); +fun mk_supports_ty ty t1 t2 = supports_const ty $ t1 $ t2; +fun mk_supports t1 t2 = mk_supports_ty (fastype_of t2) t1 t2; + +fun finite_const ty = Const (@{const_name finite}, ty --> @{typ bool}) +fun mk_finite_ty ty t = finite_const ty $ t +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 *) + +fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"} + | mk_diff (t1, @{term "{}::atom set"}) = t1 + | mk_diff (@{term "set ([]::atom list)"}, _) = @{term "set ([]::atom list)"} + | mk_diff (t1, @{term "set ([]::atom list)"}) = t1 + | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2) + +fun mk_append (t1, @{term "[]::atom list"}) = t1 + | mk_append (@{term "[]::atom list"}, t2) = t2 + | mk_append (t1, t2) = HOLogic.mk_binop @{const_name "append"} (t1, t2) + +fun mk_union (t1, @{term "{}::atom set"}) = t1 + | mk_union (@{term "{}::atom set"}, t2) = t2 + | mk_union (t1, @{term "set ([]::atom list)"}) = t1 + | mk_union (@{term "set ([]::atom list)"}, t2) = t2 + | mk_union (t1, t2) = HOLogic.mk_binop @{const_name "sup"} (t1, t2) + +fun fold_union trms = fold_rev (curry mk_union) trms @{term "{}::atom set"} +fun fold_append trms = fold_rev (curry mk_append) trms @{term "[]::atom list"} + +fun mk_conj (t1, @{term "True"}) = t1 + | mk_conj (@{term "True"}, t2) = t2 + | mk_conj (t1, t2) = HOLogic.mk_conj (t1, t2) + +fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"} + + +(* produces fresh arguments for a term *) + +fun fresh_args ctxt f = + f |> fastype_of + |> binder_types + |> map (pair "z") + |> Variable.variant_frees ctxt [f] + |> map Free + + + +(** datatypes **) + +(* constructor infos *) +type cns_info = (term * typ * typ list * bool list) list + +(* returns the type of the nth datatype *) +fun all_dtyps descr sorts = + map (fn n => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n)) (0 upto (length descr - 1)) + +fun nth_dtyp descr sorts n = + Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec n); + +(* returns info about constructors in a datatype *) +fun all_dtyp_constrs_info descr = + map (fn (_, (ty, vs, constrs)) => map (pair (ty, vs)) constrs) descr + +(* returns the constants of the constructors plus the + corresponding type and types of arguments *) +fun all_dtyp_constrs_types descr sorts = + let + fun aux ((ty_name, vs), (cname, args)) = + let + val vs_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) vs + val ty = Type (ty_name, vs_tys) + val arg_tys = map (Datatype_Aux.typ_of_dtyp descr sorts) args + val is_rec = map Datatype_Aux.is_rec_type args + in + (Const (cname, arg_tys ---> ty), ty, arg_tys, is_rec) + end + in + map (map aux) (all_dtyp_constrs_info descr) + end + +fun nth_dtyp_constrs_types descr sorts n = + nth (all_dtyp_constrs_types descr sorts) n + + +(* generates for every datatype a name str ^ dt_name + plus and index for multiple occurences of a string *) +fun prefix_dt_names descr sorts str = + let + fun get_nth_name (i, _) = + Datatype_Aux.name_of_typ (nth_dtyp descr sorts i) + in + Datatype_Prop.indexify_names + (map (prefix str o get_nth_name) descr) + end + + + +(** function package tactics **) + +fun pat_completeness_simp simps lthy = + let + val simp_set = HOL_basic_ss addsimps (@{thms sum.inject sum.distinct} @ simps) + in + Pat_Completeness.pat_completeness_tac lthy 1 + THEN ALLGOALS (asm_full_simp_tac simp_set) + end + + +fun prove_termination_tac size_simps ctxt = + let + val natT = @{typ nat} + fun prod_size_const fT sT = + let + val fT_fun = fT --> natT + val sT_fun = sT --> natT + val prodT = Type (@{type_name prod}, [fT, sT]) + in + Const (@{const_name prod_size}, [fT_fun, sT_fun, prodT] ---> natT) + end + + fun mk_size_measure T = + case T of + (Type (@{type_name Sum_Type.sum}, [fT, sT])) => + SumTree.mk_sumcase fT sT natT (mk_size_measure fT) (mk_size_measure sT) + | (Type (@{type_name Product_Type.prod}, [fT, sT])) => + prod_size_const fT sT $ (mk_size_measure fT) $ (mk_size_measure sT) + | _ => size_const T + + fun mk_measure_trm T = + HOLogic.dest_setT T + |> fst o HOLogic.dest_prodT + |> mk_size_measure + |> curry (op $) (Const (@{const_name "measure"}, dummyT)) + |> Syntax.check_term ctxt + + val ss = HOL_ss addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral + zero_less_Suc prod.size(1) mult_Suc_right} @ size_simps + val ss' = ss addsimprocs Nat_Numeral_Simprocs.cancel_numerals + in + Function_Relation.relation_tac ctxt mk_measure_trm + THEN_ALL_NEW simp_tac ss' + end + +fun prove_termination size_simps ctxt = + Function.prove_termination NONE + (HEADGOAL (prove_termination_tac size_simps ctxt)) ctxt + +(** transformations of premises (in inductive proofs) **) + +(* + given the theorem F[t]; proves the theorem F[f t] + + - F needs to be monotone + - f returns either SOME for a term it fires on + and NONE elsewhere +*) +fun map_term f t = + (case f t of + NONE => map_term' f t + | x => x) +and map_term' f (t $ u) = + (case (map_term f t, map_term f u) of + (NONE, NONE) => NONE + | (SOME t'', NONE) => SOME (t'' $ u) + | (NONE, SOME u'') => SOME (t $ u'') + | (SOME t'', SOME u'') => SOME (t'' $ u'')) + | map_term' f (Abs (s, T, t)) = + (case map_term f t of + NONE => NONE + | SOME t'' => SOME (Abs (s, T, t''))) + | map_term' _ _ = NONE; + +fun map_thm_tac ctxt tac thm = + let + val monos = Inductive.get_monos ctxt + val simps = HOL_basic_ss addsimps @{thms split_def} + in + EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, + REPEAT_DETERM (FIRSTGOAL (simp_tac simps THEN' resolve_tac monos)), + REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))] + end + +fun map_thm ctxt f tac thm = + let + val opt_goal_trm = map_term f (prop_of thm) + in + case opt_goal_trm of + NONE => thm + | SOME goal => + Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm) + end + +(* + inductive premises can be of the form + R ... /\ P ...; split_conj_i picks out + the part R or P part +*) +fun split_conj1 names (Const (@{const_name "conj"}, _) $ f1 $ _) = + (case head_of f1 of + Const (name, _) => if member (op =) names name then SOME f1 else NONE + | _ => NONE) +| split_conj1 _ _ = NONE; + +fun split_conj2 names (Const (@{const_name "conj"}, _) $ f1 $ f2) = + (case head_of f1 of + Const (name, _) => if member (op =) names name then SOME f2 else NONE + | _ => NONE) +| split_conj2 _ _ = NONE; + +fun transform_prem1 ctxt names thm = + map_thm ctxt (split_conj1 names) (etac conjunct1 1) thm + +fun transform_prem2 ctxt names thm = + map_thm ctxt (split_conj2 names) (etac conjunct2 1) thm + + +(* transformes a theorem into one of the object logic *) +val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars + +end (* structure *) + +open Nominal_Library; \ No newline at end of file diff -r 41137dc935ff -r 8193bbaa07fe Nominal/nominal_permeq.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/nominal_permeq.ML Sun Nov 14 16:34:47 2010 +0000 @@ -0,0 +1,174 @@ +(* Title: nominal_permeq.ML + Author: Christian Urban + Author: Brian Huffman +*) + +signature NOMINAL_PERMEQ = +sig + val eqvt_tac: Proof.context -> thm list -> string list -> int -> tactic + val eqvt_strict_tac: Proof.context -> thm list -> string list -> int -> tactic + + val perm_simp_meth: thm list * string list -> Proof.context -> Method.method + val perm_strict_simp_meth: thm list * string list -> Proof.context -> Method.method + val args_parser: (thm list * string list) context_parser + + val trace_eqvt: bool Config.T + val setup: theory -> theory +end; + +(* + +- eqvt_tac and eqvt_strict_tac take a list of theorems + which are first tried to simplify permutations + + the string list contains constants that should not be + analysed (for example there is no raw eqvt-lemma for + the constant The); therefore it should not be analysed + +- setting [[trace_eqvt = true]] switches on tracing + information + +*) + +structure Nominal_Permeq: NOMINAL_PERMEQ = +struct + +open Nominal_ThmDecls; + +(* tracing infrastructure *) +val (trace_eqvt, trace_eqvt_setup) = Attrib.config_bool "trace_eqvt" (K false); + +fun trace_enabled ctxt = Config.get ctxt trace_eqvt + +fun trace_msg ctxt result = + let + val lhs_str = Syntax.string_of_term ctxt (term_of (Thm.lhs_of result)) + val rhs_str = Syntax.string_of_term ctxt (term_of (Thm.rhs_of result)) + in + warning (Pretty.string_of (Pretty.strs ["Rewriting", lhs_str, "to", rhs_str])) + end + +fun trace_conv ctxt conv ctrm = + let + val result = conv ctrm + in + if Thm.is_reflexive result + then result + else (trace_msg ctxt result; result) + end + +(* this conversion always fails, but prints + out the analysed term *) +fun trace_info_conv ctxt ctrm = + let + val trm = term_of ctrm + val _ = case (head_of trm) of + @{const "Trueprop"} => () + | _ => warning ("Analysing term " ^ Syntax.string_of_term ctxt trm) + in + Conv.no_conv ctrm + end + +(* conversion for applications *) +fun eqvt_apply_conv ctrm = + case (term_of ctrm) of + Const (@{const_name "permute"}, _) $ _ $ (_ $ _) => + let + val (perm, t) = Thm.dest_comb ctrm + val (_, p) = Thm.dest_comb perm + val (f, x) = Thm.dest_comb t + val a = ctyp_of_term x; + val b = ctyp_of_term t; + val ty_insts = map SOME [b, a] + val term_insts = map SOME [p, f, x] + in + Drule.instantiate' ty_insts term_insts @{thm eqvt_apply} + end + | _ => Conv.no_conv ctrm + +(* conversion for lambdas *) +fun eqvt_lambda_conv ctrm = + case (term_of ctrm) of + Const (@{const_name "permute"}, _) $ _ $ (Abs _) => + Conv.rewr_conv @{thm eqvt_lambda} ctrm + | _ => Conv.no_conv ctrm + + +(* conversion that raises an error or prints a warning message, + if a permutation on a constant or application cannot be analysed *) + +fun is_excluded excluded (Const (a, _)) = member (op=) excluded a + | is_excluded _ _ = false + +fun progress_info_conv ctxt strict_flag excluded ctrm = + let + fun msg trm = + if is_excluded excluded trm then () else + (if strict_flag then error else warning) + ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm)) + + val _ = case (term_of ctrm) of + Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm + | Const (@{const_name "permute"}, _) $ _ $ (trm as _ $ _) => msg trm + | _ => () + in + Conv.all_conv ctrm + end + +(* main conversion *) +fun eqvt_conv ctxt strict_flag user_thms excluded ctrm = + let + val first_conv_wrapper = + if trace_enabled ctxt + then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt)) + else Conv.first_conv + + val pre_thms = map safe_mk_equiv user_thms @ @{thms eqvt_bound} @ get_eqvts_raw_thms ctxt + val post_thms = map safe_mk_equiv @{thms permute_pure} + in + first_conv_wrapper + [ Conv.rewrs_conv pre_thms, + eqvt_apply_conv, + eqvt_lambda_conv, + Conv.rewrs_conv post_thms, + progress_info_conv ctxt strict_flag excluded + ] ctrm + end + +(* the eqvt-tactics first eta-normalise goals in + order to avoid problems with inductions in the + equivaraince command. *) + +(* raises an error if some permutations cannot be eliminated *) +fun eqvt_strict_tac ctxt user_thms excluded = + CONVERSION (Conv.top_conv + (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt true user_thms excluded)) ctxt) + +(* prints a warning message if some permutations cannot be eliminated *) +fun eqvt_tac ctxt user_thms excluded = + CONVERSION (Conv.top_conv + (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt false user_thms excluded)) ctxt) + +(* setup of the configuration value *) +val setup = + trace_eqvt_setup + + +(** methods **) +fun unless_more_args scan = Scan.unless (Scan.lift ((Args.$$$ "exclude") -- Args.colon)) scan + +val add_thms_parser = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- + Scan.repeat (unless_more_args Attrib.multi_thm) >> flat) []; + +val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- + (Scan.repeat (Args.const true))) [] + +val args_parser = add_thms_parser -- exclude_consts_parser + +fun perm_simp_meth (thms, consts) ctxt = + SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt thms consts)) + +fun perm_strict_simp_meth (thms, consts) ctxt = + SIMPLE_METHOD (HEADGOAL (eqvt_strict_tac ctxt thms consts)) + +end; (* structure *) diff -r 41137dc935ff -r 8193bbaa07fe Nominal/nominal_thmdecls.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/nominal_thmdecls.ML Sun Nov 14 16:34:47 2010 +0000 @@ -0,0 +1,237 @@ +(* Title: nominal_thmdecls.ML + Author: Christian Urban + + Infrastructure for the lemma collection "eqvts". + + Provides the attributes [eqvt] and [eqvt_raw], and the theorem + lists eqvts and eqvts_raw. The first attribute will store the + theorem in the eqvts list and also in the eqvts_raw list. For + the latter the theorem is expected to be of the form + + p o (c x1 x2 ...) = c (p o x1) (p o x2) ... (1) + + or + + c x1 x2 ... ==> c (p o x1) (p o x2) ... (2) + + and it is stored in the form + + p o c == c + + The [eqvt_raw] attribute just adds the theorem to eqvts_raw. + + TODO: In case of the form in (2) one should also + add the equational form to eqvts +*) + +signature NOMINAL_THMDECLS = +sig + val eqvt_add: attribute + val eqvt_del: attribute + val eqvt_raw_add: attribute + val eqvt_raw_del: attribute + val setup: theory -> theory + val get_eqvts_thms: Proof.context -> thm list + val get_eqvts_raw_thms: Proof.context -> thm list + val eqvt_transform: Proof.context -> thm -> thm + val is_eqvt: Proof.context -> term -> bool +end; + +structure Nominal_ThmDecls: NOMINAL_THMDECLS = +struct + +structure EqvtData = Generic_Data +( type T = thm Item_Net.T; + val empty = Thm.full_rules; + val extend = I; + val merge = Item_Net.merge); + +structure EqvtRawData = Generic_Data +( type T = thm Termtab.table; + val empty = Termtab.empty; + val extend = I; + val merge = Termtab.merge (K true)); + +val eqvts = Item_Net.content o EqvtData.get; +val eqvts_raw = map snd o Termtab.dest o EqvtRawData.get; + +val get_eqvts_thms = eqvts o Context.Proof; +val get_eqvts_raw_thms = eqvts_raw o Context.Proof; + +val add_thm = EqvtData.map o Item_Net.update; +val del_thm = EqvtData.map o Item_Net.remove; + +fun add_raw_thm thm = + case prop_of thm of + Const ("==", _) $ _ $ (c as Const _) => EqvtRawData.map (Termtab.update (c, thm)) + | _ => raise THM ("Theorem must be a meta-equality where the right-hand side is a constant.", 0, [thm]) + +fun del_raw_thm thm = + case prop_of thm of + Const ("==", _) $ _ $ (c as Const _) => EqvtRawData.map (Termtab.delete c) + | _ => raise THM ("Theorem must be a meta-equality where the right-hand side is a constant.", 0, [thm]) + +fun is_eqvt ctxt trm = + case trm of + (c as Const _) => Termtab.defined (EqvtRawData.get (Context.Proof ctxt)) c + | _ => raise TERM ("Term must be a constsnt.", [trm]) + + + +(** transformation of eqvt lemmas **) + +fun get_perms trm = + case trm of + Const (@{const_name permute}, _) $ _ $ (Bound _) => + raise TERM ("get_perms called on bound", [trm]) + | Const (@{const_name permute}, _) $ p $ _ => [p] + | t $ u => get_perms t @ get_perms u + | Abs (_, _, t) => get_perms t + | _ => [] + +fun put_perm p trm = + case trm of + Bound _ => trm + | Const _ => trm + | t $ u => put_perm p t $ put_perm p u + | Abs (x, ty, t) => Abs (x, ty, put_perm p t) + | _ => mk_perm p trm + +(* tests whether there is a disagreement between the permutations, + and that there is at least one permutation *) +fun is_bad_list [] = true + | is_bad_list [_] = false + | is_bad_list (p::q::ps) = if p = q then is_bad_list (q::ps) else true + + +(* transforms equations into the "p o c == c"-form + from p o (c x1 ...xn) = c (p o x1) ... (p o xn) *) + +fun eqvt_transform_eq_tac thm = +let + val ss_thms = @{thms permute_minus_cancel permute_prod.simps split_paired_all} +in + REPEAT o FIRST' + [CHANGED o simp_tac (HOL_basic_ss addsimps ss_thms), + rtac (thm RS @{thm trans}), + rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}] +end + +fun eqvt_transform_eq ctxt thm = + let + val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm)) + handle TERM _ => error "Equivariance lemma must be an equality." + val (p, t) = dest_perm lhs + handle TERM _ => error "Equivariance lemma is not of the form p \ c... = c..." + + val ps = get_perms rhs handle TERM _ => [] + val (c, c') = (head_of t, head_of rhs) + val msg = "Equivariance lemma is not of the right form " + in + if c <> c' + then error (msg ^ "(constants do not agree).") + else if is_bad_list (p :: ps) + then error (msg ^ "(permutations do not agree).") + else if not (rhs aconv (put_perm p t)) + then error (msg ^ "(arguments do not agree).") + else if is_Const t + then safe_mk_equiv thm + else + let + val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c)) + val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt + in + Goal.prove ctxt [] [] goal' (fn _ => eqvt_transform_eq_tac thm 1) + |> singleton (ProofContext.export ctxt' ctxt) + |> safe_mk_equiv + |> zero_var_indexes + end + end + +(* transforms equations into the "p o c == c"-form + from R x1 ...xn ==> R (p o x1) ... (p o xn) *) + +fun eqvt_transform_imp_tac ctxt p p' thm = + let + val thy = ProofContext.theory_of ctxt + val cp = Thm.cterm_of thy p + val cp' = Thm.cterm_of thy (mk_minus p') + val thm' = Drule.cterm_instantiate [(cp, cp')] thm + val simp = HOL_basic_ss addsimps @{thms permute_minus_cancel(2)} + in + EVERY' [rtac @{thm iffI}, dtac @{thm permute_boolE}, rtac thm, atac, + rtac @{thm permute_boolI}, dtac thm', full_simp_tac simp] + end + +fun eqvt_transform_imp ctxt thm = + let + val (prem, concl) = pairself HOLogic.dest_Trueprop (Logic.dest_implies (prop_of thm)) + val (c, c') = (head_of prem, head_of concl) + val ps = get_perms concl handle TERM _ => [] + val p = try hd ps + val msg = "Equivariance lemma is not of the right form " + in + if c <> c' + then error (msg ^ "(constants do not agree).") + else if is_bad_list ps + then error (msg ^ "(permutations do not agree).") + else if not (concl aconv (put_perm (the p) prem)) + then error (msg ^ "(arguments do not agree).") + else + let + val prem' = mk_perm (the p) prem + val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (prem', concl)) + val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt + in + Goal.prove ctxt' [] [] goal' + (fn _ => eqvt_transform_imp_tac ctxt' (the p) p' thm 1) + |> singleton (ProofContext.export ctxt' ctxt) + end + end + +fun eqvt_transform ctxt thm = + case (prop_of thm) of + @{const "Trueprop"} $ (Const (@{const_name "HOL.eq"}, _) $ + (Const (@{const_name "permute"}, _) $ _ $ _) $ _) => + eqvt_transform_eq ctxt thm + | @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) => + eqvt_transform_imp ctxt thm |> eqvt_transform_eq ctxt + | _ => raise error "Only _ = _ and _ ==> _ cases are implemented." + + +(** attributes **) + +val eqvt_add = Thm.declaration_attribute + (fn thm => fn context => + let + val thm' = eqvt_transform (Context.proof_of context) thm + in + context |> add_thm thm |> add_raw_thm thm' + end) + +val eqvt_del = Thm.declaration_attribute + (fn thm => fn context => + let + val thm' = eqvt_transform (Context.proof_of context) thm + in + context |> del_thm thm |> del_raw_thm thm' + end) + +val eqvt_raw_add = Thm.declaration_attribute add_raw_thm; +val eqvt_raw_del = Thm.declaration_attribute del_raw_thm; + + +(** setup function **) + +val setup = + Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) + (cat_lines ["Declaration of equivariance lemmas - they will automtically be", + "brought into the form p o c == c"]) #> + Attrib.setup @{binding "eqvt_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_del) + (cat_lines ["Declaration of equivariance lemmas - no", + "transformation is performed"]) #> + Global_Theory.add_thms_dynamic (@{binding "eqvts"}, eqvts) #> + Global_Theory.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw); + + +end; diff -r 41137dc935ff -r 8193bbaa07fe Pearl-jv/Paper.thy --- a/Pearl-jv/Paper.thy Sun Nov 14 12:09:14 2010 +0000 +++ b/Pearl-jv/Paper.thy Sun Nov 14 16:34:47 2010 +0000 @@ -1,8 +1,8 @@ (*<*) theory Paper -imports "../Nominal-General/Nominal2_Base" - "../Nominal-General/Nominal2_Eqvt" - "../Nominal-General/Atoms" +imports "../Nominal/Nominal2_Base" + "../Nominal/Nominal2_Eqvt" + "../Nominal/Atoms" "../Nominal/Abs" "LaTeXsugar" begin diff -r 41137dc935ff -r 8193bbaa07fe Pearl-jv/ROOT.ML --- a/Pearl-jv/ROOT.ML Sun Nov 14 12:09:14 2010 +0000 +++ b/Pearl-jv/ROOT.ML Sun Nov 14 16:34:47 2010 +0000 @@ -1,7 +1,7 @@ -no_document use_thys ["../Nominal-General/Nominal2_Base", - "../Nominal-General/Nominal2_Eqvt", - "../Nominal-General/Atoms", - "../Nominal/Abs", +no_document use_thys ["../Nominal/Nominal2_Base", + "../Nominal/Nominal2_Eqvt", + "../Nominal/Atoms", + "../Nominal/Nominal2_Abs", "LaTeXsugar"]; use_thys ["Paper"]; \ No newline at end of file diff -r 41137dc935ff -r 8193bbaa07fe Pearl/Paper.thy --- a/Pearl/Paper.thy Sun Nov 14 12:09:14 2010 +0000 +++ b/Pearl/Paper.thy Sun Nov 14 16:34:47 2010 +0000 @@ -1,8 +1,8 @@ (*<*) theory Paper -imports "../Nominal-General/Nominal2_Base" - "../Nominal-General/Nominal2_Eqvt" - "../Nominal-General/Atoms" +imports "../Nominal/Nominal2_Base" + "../Nominal/Nominal2_Eqvt" + "../Nominal/Atoms" "LaTeXsugar" begin diff -r 41137dc935ff -r 8193bbaa07fe Pearl/ROOT.ML --- a/Pearl/ROOT.ML Sun Nov 14 12:09:14 2010 +0000 +++ b/Pearl/ROOT.ML Sun Nov 14 16:34:47 2010 +0000 @@ -1,6 +1,6 @@ -no_document use_thys ["../Nominal-General/Nominal2_Base", - "../Nominal-General/Nominal2_Eqvt", - "../Nominal-General/Atoms", +no_document use_thys ["../Nominal/Nominal2_Base", + "../Nominal/Nominal2_Eqvt", + "../Nominal/Atoms", "LaTeXsugar"]; use_thys ["Paper"]; \ No newline at end of file diff -r 41137dc935ff -r 8193bbaa07fe README --- a/README Sun Nov 14 12:09:14 2010 +0000 +++ b/README Sun Nov 14 16:34:47 2010 +0000 @@ -9,8 +9,6 @@ Nominal/Ex ... examples for new implementation -Nominal-General . implementation of the abstract nominal theory - @@ -28,6 +26,6 @@ Pearl ... accepted at ITP Pearl-jv ... journal version -Quotient-Paper .. submitted to SAC +Quotient-Paper .. accepted to SAC Slides ... various talks Christian gave recently \ No newline at end of file