diff --git a/thys/Nominal2/Nominal2_Base.thy b/thys/Nominal2/Nominal2_Base.thy --- a/thys/Nominal2/Nominal2_Base.thy +++ b/thys/Nominal2/Nominal2_Base.thy @@ -1,3435 +1,3435 @@ (* Title: Nominal2_Base Authors: Christian Urban, Brian Huffman, Cezary Kaliszyk Basic definitions and lemma infrastructure for Nominal Isabelle. *) theory Nominal2_Base imports "HOL-Library.Infinite_Set" "HOL-Library.Multiset" "HOL-Library.FSet" FinFun.FinFun keywords "atom_decl" "equivariance" :: thy_decl begin declare [[typedef_overloaded]] 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 n) = 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\ definition "perm \ {f. bij f \ finite {a. f a \ a} \ (\a. sort_of (f a) = sort_of a)}" typedef perm = "perm" proof show "id \ perm" unfolding perm_def 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 (multiplicative) 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 standard 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: 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: shows "(a \ b) + (a \ b) = 0" and "(a \ b) + (b \ a) = 0" by (rule_tac [!] Rep_perm_ext) (simp_all 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(1)]) 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: Rep_perm_simps fun_eq_iff) section \Permutation Types\ text \ Infix syntax for \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" using permute_plus [of p "- q" x] 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 standard 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 perm_eq_iff: 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 standard apply (simp add: permute_perm_def) apply (simp add: permute_perm_def algebra_simps) done end lemma permute_self: shows "p \ p = p" unfolding permute_perm_def by (simp add: add.assoc) lemma pemute_minus_self: shows "- p \ p = p" unfolding permute_perm_def by (simp add: add.assoc) subsection \Permutations for functions\ instantiation "fun" :: (pt, pt) pt begin definition "p \ f = (\x. p \ (f (- p \ x)))" instance apply standard 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 lemma permute_fun_comp: shows "p \ f = (permute p) o f o (permute (-p))" by (simp add: comp_def permute_fun_def) subsection \Permutations for booleans\ instantiation bool :: pt begin definition "p \ (b::bool) = b" instance apply standard apply(simp_all add: permute_bool_def) done end 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\ instantiation "set" :: (pt) pt begin definition "p \ X = {p \ x | x. x \ X}" instance apply standard apply (auto simp: permute_set_def) done end lemma permute_set_eq: shows "p \ X = {x. - p \ x \ X}" unfolding permute_set_def by (auto) (metis permute_minus_cancel(1)) lemma permute_set_eq_image: shows "p \ X = permute p ` X" unfolding permute_set_def by auto lemma permute_set_eq_vimage: shows "p \ X = permute (- p) -` X" unfolding permute_set_eq vimage_def by simp lemma permute_finite [simp]: shows "finite (p \ X) = finite X" unfolding permute_set_eq_vimage using bij_permute by (rule finite_vimage_iff) lemma swap_set_not_in: assumes a: "a \ S" "b \ S" shows "(a \ b) \ S = S" unfolding permute_set_def using a by (auto simp: 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_def using a by (auto simp: swap_atom) lemma swap_set_in_eq: assumes a: "a \ S" "b \ S" "sort_of a = sort_of b" shows "(a \ b) \ S = (S - {a}) \ {b}" unfolding permute_set_def using a by (auto simp: swap_atom) lemma swap_set_both_in: assumes a: "a \ S" "b \ S" shows "(a \ b) \ S = S" unfolding permute_set_def using a by (auto simp: swap_atom) lemma mem_permute_iff: shows "(p \ x) \ (p \ X) \ x \ X" unfolding permute_set_def by auto lemma empty_eqvt: shows "p \ {} = {}" unfolding permute_set_def by (simp) lemma insert_eqvt: shows "p \ (insert x A) = insert (p \ x) (p \ A)" unfolding permute_set_eq_image image_insert .. subsection \Permutations for @{typ unit}\ instantiation unit :: pt begin definition "p \ (u::unit) = u" instance by standard (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 standard auto end subsection \Permutations for sums\ instantiation sum :: (pt, pt) pt begin primrec permute_sum where Inl_eqvt: "p \ (Inl x) = Inl (p \ x)" | Inr_eqvt: "p \ (Inr y) = Inr (p \ y)" instance by standard (case_tac [!] x, simp_all) end subsection \Permutations for @{typ "'a list"}\ instantiation list :: (pt) pt begin primrec permute_list where Nil_eqvt: "p \ [] = []" | Cons_eqvt: "p \ (x # xs) = p \ x # p \ xs" instance by standard (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 @{typ "'a option"}\ instantiation option :: (pt) pt begin primrec permute_option where None_eqvt: "p \ None = None" | Some_eqvt: "p \ (Some x) = Some (p \ x)" instance by standard (induct_tac [!] x, simp_all) end subsection \Permutations for @{typ "'a multiset"}\ instantiation multiset :: (pt) pt begin definition "p \ M = {# p \ x. x :# M #}" instance proof fix M :: "'a multiset" and p q :: "perm" show "0 \ M = M" unfolding permute_multiset_def by (induct_tac M) (simp_all) show "(p + q) \ M = p \ q \ M" unfolding permute_multiset_def by (induct_tac M) (simp_all) qed end lemma permute_multiset [simp]: fixes M N::"('a::pt) multiset" shows "(p \ {#}) = ({#} ::('a::pt) multiset)" and "(p \ add_mset x M) = add_mset (p \ x) (p \ M)" and "(p \ (M + N)) = (p \ M) + (p \ N)" unfolding permute_multiset_def by (simp_all) subsection \Permutations for @{typ "'a fset"}\ instantiation fset :: (pt) pt begin context includes fset.lifting begin lift_definition "permute_fset" :: "perm \ 'a fset \ 'a fset" is "permute :: perm \ 'a set \ 'a set" by simp end context includes fset.lifting begin instance proof fix x :: "'a fset" and p q :: "perm" show "0 \ x = x" by transfer simp show "(p + q) \ x = p \ q \ x" by transfer simp qed end end context includes fset.lifting begin lemma permute_fset [simp]: fixes S::"('a::pt) fset" shows "(p \ {||}) = ({||} ::('a::pt) fset)" and "(p \ finsert x S) = finsert (p \ x) (p \ S)" apply (transfer, simp add: empty_eqvt) apply (transfer, simp add: insert_eqvt) done lemma fset_eqvt: shows "p \ (fset S) = fset (p \ S)" by transfer simp end subsection \Permutations for @{typ "('a, 'b) finfun"}\ instantiation finfun :: (pt, pt) pt begin lift_definition permute_finfun :: "perm \ ('a, 'b) finfun \ ('a, 'b) finfun" is "permute :: perm \ ('a \ 'b) \ ('a \ 'b)" apply(simp add: permute_fun_comp) apply(rule finfun_right_compose) apply(rule finfun_left_compose) apply(assumption) apply(simp) done instance apply standard apply(transfer) apply(simp) apply(transfer) apply(simp) done end subsection \Permutations for @{typ char}, @{typ nat}, and @{typ int}\ instantiation char :: pt begin definition "p \ (c::char) = c" instance by standard (simp_all add: permute_char_def) end instantiation nat :: pt begin definition "p \ (n::nat) = n" instance by standard (simp_all add: permute_nat_def) end instantiation int :: pt begin definition "p \ (i::int) = i" instance by standard (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 standard (simp add: permute_fun_def permute_pure) instance set :: (pure) pure by standard (simp add: permute_set_def permute_pure) instance prod :: (pure, pure) pure by standard (induct_tac x, simp add: permute_pure) instance sum :: (pure, pure) pure by standard (induct_tac x, simp_all add: permute_pure) instance list :: (pure) pure by standard (induct_tac x, simp_all add: permute_pure) instance option :: (pure) pure by standard (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) section \Infrastructure for Equivariance and \Perm_simp\\ subsection \Basic functions about permutations\ ML_file \nominal_basics.ML\ subsection \Eqvt infrastructure\ text \Setup of the theorem attributes \eqvt\ and \eqvt_raw\.\ ML_file \nominal_thmdecls.ML\ lemmas [eqvt] = (* pt types *) permute_prod.simps permute_list.simps permute_option.simps permute_sum.simps (* sets *) empty_eqvt insert_eqvt set_eqvt (* fsets *) permute_fset fset_eqvt (* multisets *) permute_multiset subsection \\perm_simp\ infrastructure\ definition "unpermute p = permute (- p)" lemma eqvt_apply: fixes f :: "'a::pt \ 'b::pt" and x :: "'a::pt" shows "p \ (f x) \ (p \ f) (p \ x)" unfolding permute_fun_def by simp lemma eqvt_lambda: fixes f :: "'a::pt \ 'b::pt" shows "p \ f \ (\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\ ML_file \nominal_permeq.ML\ 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.\ simproc_setup perm_simproc ("p \ t") = \fn _ => fn ctxt => fn ctrm => case Thm.term_of (Thm.dest_arg ctrm) of Free _ => NONE | Var _ => NONE | \<^Const_>\permute _ for _ _\ => NONE | _ => let val thm = Nominal_Permeq.eqvt_conv ctxt Nominal_Permeq.eqvt_strict_config ctrm handle ERROR _ => Thm.reflexive ctrm in if Thm.is_reflexive thm then NONE else SOME(thm) end \ subsubsection \Equivariance for permutations and swapping\ lemma permute_eqvt: shows "p \ (q \ x) = (p \ q) \ (p \ x)" unfolding permute_perm_def by simp (* the normal version of this lemma would cause loops *) lemma permute_eqvt_raw [eqvt_raw]: shows "p \ permute \ permute" apply(simp add: fun_eq_iff permute_fun_def) apply(subst permute_eqvt) apply(simp) done lemma zero_perm_eqvt [eqvt]: shows "p \ (0::perm) = 0" unfolding permute_perm_def by simp lemma add_perm_eqvt [eqvt]: fixes p p1 p2 :: perm shows "p \ (p1 + p2) = p \ p1 + p \ p2" unfolding permute_perm_def by (simp add: perm_eq_iff) lemma swap_eqvt [eqvt]: shows "p \ (a \ b) = (p \ a \ p \ b)" unfolding permute_perm_def by (auto simp: swap_atom perm_eq_iff) lemma uminus_eqvt [eqvt]: fixes p q::"perm" shows "p \ (- q) = - (p \ q)" unfolding permute_perm_def by (simp add: diff_add_eq_diff_diff_swap) subsubsection \Equivariance of Logical Operators\ lemma eq_eqvt [eqvt]: shows "p \ (x = y) \ (p \ x) = (p \ y)" unfolding permute_eq_iff permute_bool_def .. lemma Not_eqvt [eqvt]: shows "p \ (\ A) \ \ (p \ A)" by (simp add: permute_bool_def) lemma conj_eqvt [eqvt]: shows "p \ (A \ B) \ (p \ A) \ (p \ B)" by (simp add: permute_bool_def) lemma imp_eqvt [eqvt]: shows "p \ (A \ B) \ (p \ A) \ (p \ B)" by (simp add: permute_bool_def) declare imp_eqvt[folded HOL.induct_implies_def, eqvt] lemma all_eqvt [eqvt]: shows "p \ (\x. P x) = (\x. (p \ P) x)" unfolding All_def by (perm_simp) (rule refl) declare all_eqvt[folded HOL.induct_forall_def, eqvt] lemma ex_eqvt [eqvt]: shows "p \ (\x. P x) = (\x. (p \ P) x)" unfolding Ex_def by (perm_simp) (rule refl) lemma ex1_eqvt [eqvt]: shows "p \ (\!x. P x) = (\!x. (p \ P) x)" unfolding Ex1_def by (perm_simp) (rule refl) lemma if_eqvt [eqvt]: shows "p \ (if b then x else y) = (if p \ b then p \ x else p \ y)" by (simp add: permute_fun_def permute_bool_def) lemma True_eqvt [eqvt]: shows "p \ True = True" unfolding permute_bool_def .. lemma False_eqvt [eqvt]: shows "p \ False = False" unfolding permute_bool_def .. lemma disj_eqvt [eqvt]: shows "p \ (A \ B) \ (p \ A) \ (p \ B)" by (simp add: permute_bool_def) lemma all_eqvt2: shows "p \ (\x. P x) = (\x. p \ P (- p \ x))" by (perm_simp add: permute_minus_cancel) (rule refl) lemma ex_eqvt2: shows "p \ (\x. P x) = (\x. p \ P (- p \ x))" by (perm_simp add: permute_minus_cancel) (rule refl) lemma ex1_eqvt2: shows "p \ (\!x. P x) = (\!x. p \ P (- p \ x))" by (perm_simp add: permute_minus_cancel) (rule refl) lemma the_eqvt: assumes unique: "\!x. P x" shows "(p \ (THE x. P x)) = (THE x. (p \ P) x)" apply(rule the1_equality [symmetric]) apply(rule_tac p="-p" in permute_boolE) apply(perm_simp add: permute_minus_cancel) apply(rule unique) apply(rule_tac p="-p" in permute_boolE) apply(perm_simp add: permute_minus_cancel) apply(rule theI'[OF unique]) done lemma the_eqvt2: assumes unique: "\!x. P x" shows "(p \ (THE x. P x)) = (THE x. p \ P (- p \ x))" apply(rule the1_equality [symmetric]) apply(simp only: ex1_eqvt2[symmetric]) apply(simp add: permute_bool_def unique) apply(simp add: permute_bool_def) apply(rule theI'[OF unique]) done subsubsection \Equivariance of Set operators\ lemma mem_eqvt [eqvt]: shows "p \ (x \ A) \ (p \ x) \ (p \ A)" unfolding permute_bool_def permute_set_def by (auto) lemma Collect_eqvt [eqvt]: shows "p \ {x. P x} = {x. (p \ P) x}" unfolding permute_set_eq permute_fun_def by (auto simp: permute_bool_def) lemma Bex_eqvt [eqvt]: shows "p \ (\x \ S. P x) = (\x \ (p \ S). (p \ P) x)" unfolding Bex_def by simp lemma Ball_eqvt [eqvt]: shows "p \ (\x \ S. P x) = (\x \ (p \ S). (p \ P) x)" unfolding Ball_def by simp lemma image_eqvt [eqvt]: shows "p \ (f ` A) = (p \ f) ` (p \ A)" unfolding image_def by simp lemma Image_eqvt [eqvt]: shows "p \ (R `` A) = (p \ R) `` (p \ A)" unfolding Image_def by simp lemma UNIV_eqvt [eqvt]: shows "p \ UNIV = UNIV" unfolding UNIV_def by (perm_simp) (rule refl) lemma inter_eqvt [eqvt]: shows "p \ (A \ B) = (p \ A) \ (p \ B)" unfolding Int_def by simp lemma Inter_eqvt [eqvt]: shows "p \ \S = \(p \ S)" unfolding Inter_eq by simp lemma union_eqvt [eqvt]: shows "p \ (A \ B) = (p \ A) \ (p \ B)" unfolding Un_def by simp lemma Union_eqvt [eqvt]: shows "p \ \A = \(p \ A)" unfolding Union_eq by perm_simp rule lemma Diff_eqvt [eqvt]: fixes A B :: "'a::pt set" shows "p \ (A - B) = (p \ A) - (p \ B)" unfolding set_diff_eq by simp lemma Compl_eqvt [eqvt]: fixes A :: "'a::pt set" shows "p \ (- A) = - (p \ A)" unfolding Compl_eq_Diff_UNIV by simp lemma subset_eqvt [eqvt]: shows "p \ (S \ T) \ (p \ S) \ (p \ T)" unfolding subset_eq by simp lemma psubset_eqvt [eqvt]: shows "p \ (S \ T) \ (p \ S) \ (p \ T)" unfolding psubset_eq by simp lemma vimage_eqvt [eqvt]: shows "p \ (f -` A) = (p \ f) -` (p \ A)" unfolding vimage_def by simp lemma foldr_eqvt[eqvt]: "p \ foldr f xs = foldr (p \ f) (p \ xs)" apply(induct xs) apply(simp_all) apply(perm_simp exclude: foldr) apply(simp) done (* FIXME: eqvt attribute *) lemma Sigma_eqvt: shows "(p \ (X \ Y)) = (p \ X) \ (p \ Y)" unfolding Sigma_def by (perm_simp) (rule refl) text \ In order to prove that lfp is equivariant we need two auxiliary classes which specify that (<=) and Inf are equivariant. Instances for bool and fun are given. \ class le_eqvt = pt + assumes le_eqvt [eqvt]: "p \ (x \ y) = ((p \ x) \ (p \ (y :: 'a :: {order, pt})))" class inf_eqvt = pt + assumes inf_eqvt [eqvt]: "p \ (Inf X) = Inf (p \ (X :: 'a :: {complete_lattice, pt} set))" instantiation bool :: le_eqvt begin instance apply standard unfolding le_bool_def apply(perm_simp) apply(rule refl) done end instantiation "fun" :: (pt, le_eqvt) le_eqvt begin instance apply standard unfolding le_fun_def apply(perm_simp) apply(rule refl) done end instantiation bool :: inf_eqvt begin instance apply standard unfolding Inf_bool_def apply(perm_simp) apply(rule refl) done end instantiation "fun" :: (pt, inf_eqvt) inf_eqvt begin instance apply standard unfolding Inf_fun_def apply(perm_simp) apply(rule refl) done end lemma lfp_eqvt [eqvt]: fixes F::"('a \ 'b) \ ('a::pt \ 'b::{inf_eqvt, le_eqvt})" shows "p \ (lfp F) = lfp (p \ F)" unfolding lfp_def by simp lemma finite_eqvt [eqvt]: shows "p \ finite A = finite (p \ A)" unfolding finite_def by simp lemma fun_upd_eqvt[eqvt]: shows "p \ (f(x := y)) = (p \ f)((p \ x) := (p \ y))" unfolding fun_upd_def by simp lemma comp_eqvt [eqvt]: shows "p \ (f \ g) = (p \ f) \ (p \ g)" unfolding comp_def by simp subsubsection \Equivariance for product operations\ lemma fst_eqvt [eqvt]: shows "p \ (fst x) = fst (p \ x)" by (cases x) simp lemma snd_eqvt [eqvt]: shows "p \ (snd x) = snd (p \ x)" by (cases x) simp lemma split_eqvt [eqvt]: shows "p \ (case_prod P x) = case_prod (p \ P) (p \ x)" unfolding split_def by simp subsubsection \Equivariance for list operations\ lemma append_eqvt [eqvt]: shows "p \ (xs @ ys) = (p \ xs) @ (p \ ys)" by (induct xs) auto lemma rev_eqvt [eqvt]: shows "p \ (rev xs) = rev (p \ xs)" by (induct xs) (simp_all add: append_eqvt) lemma map_eqvt [eqvt]: shows "p \ (map f xs) = map (p \ f) (p \ xs)" by (induct xs) (simp_all) lemma removeAll_eqvt [eqvt]: shows "p \ (removeAll x xs) = removeAll (p \ x) (p \ xs)" by (induct xs) (auto) lemma filter_eqvt [eqvt]: shows "p \ (filter f xs) = filter (p \ f) (p \ xs)" apply(induct xs) apply(simp) apply(simp only: filter.simps permute_list.simps if_eqvt) apply(simp only: permute_fun_app_eq) done lemma distinct_eqvt [eqvt]: shows "p \ (distinct xs) = distinct (p \ xs)" apply(induct xs) apply(simp add: permute_bool_def) apply(simp add: conj_eqvt Not_eqvt mem_eqvt set_eqvt) done lemma length_eqvt [eqvt]: shows "p \ (length xs) = length (p \ xs)" by (induct xs) (simp_all add: permute_pure) subsubsection \Equivariance for @{typ "'a option"}\ lemma map_option_eqvt[eqvt]: shows "p \ (map_option f x) = map_option (p \ f) (p \ x)" by (cases x) (simp_all) subsubsection \Equivariance for @{typ "'a fset"}\ context includes fset.lifting begin lemma in_fset_eqvt [eqvt]: shows "(p \ (x |\| S)) = ((p \ x) |\| (p \ S))" by transfer simp lemma union_fset_eqvt [eqvt]: shows "(p \ (S |\| T)) = ((p \ S) |\| (p \ T))" by (induct S) (simp_all) lemma inter_fset_eqvt [eqvt]: shows "(p \ (S |\| T)) = ((p \ S) |\| (p \ T))" by transfer simp lemma subset_fset_eqvt [eqvt]: shows "(p \ (S |\| T)) = ((p \ S) |\| (p \ T))" by transfer simp lemma map_fset_eqvt [eqvt]: shows "p \ (f |`| S) = (p \ f) |`| (p \ S)" by transfer simp end subsubsection \Equivariance for @{typ "('a, 'b) finfun"}\ lemma finfun_update_eqvt [eqvt]: shows "(p \ (finfun_update f a b)) = finfun_update (p \ f) (p \ a) (p \ b)" by (transfer) (simp) lemma finfun_const_eqvt [eqvt]: shows "(p \ (finfun_const b)) = finfun_const (p \ b)" by (transfer) (simp) lemma finfun_apply_eqvt [eqvt]: shows "(p \ (finfun_apply f b)) = finfun_apply (p \ f) (p \ b)" by (transfer) (simp) section \Supp, Freshness and Supports\ context pt begin definition supp :: "'a \ atom set" where "supp x = {a. infinite {b. (a \ b) \ x \ x}}" definition fresh :: "atom \ 'a \ bool" ("_ \ _" [55, 55] 55) where "a \ x \ a \ supp x" end lemma supp_conv_fresh: shows "supp x = {a. \ a \ x}" unfolding fresh_def by simp 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 supp_eqvt [eqvt]: shows "p \ (supp x) = supp (p \ x)" unfolding supp_def by simp lemma fresh_eqvt [eqvt]: shows "p \ (a \ x) = (p \ a) \ (p \ x)" unfolding fresh_def by simp lemma fresh_permute_iff: shows "(p \ a) \ (p \ x) \ a \ x" by (simp only: fresh_eqvt[symmetric] permute_bool_def) lemma fresh_permute_left: shows "a \ p \ x \ - p \ a \ x" proof assume "a \ p \ x" then have "- p \ a \ - p \ p \ x" by (simp only: fresh_permute_iff) then show "- p \ a \ x" by simp next assume "- p \ a \ x" then have "p \ - p \ a \ p \ x" by (simp only: fresh_permute_iff) then show "a \ p \ x" by simp qed section \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 supports_fresh: fixes x :: "'a::pt" assumes a1: "S supports x" and a2: "finite S" and a3: "a \ S" shows "a \ x" unfolding fresh_def proof - have "(supp x) \ S" using a1 a2 by (rule supp_is_subset) then show "a \ (supp x)" using a3 by auto 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: fixes x::"'a::pure" shows "supp x = {}" 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 standard (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 standard (simp add: supp_atom) 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: perm_eq_iff 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: supp_perm swap_atom) lemma fresh_swap: shows "a \ (b \ c) \ (sort_of b \ sort_of c) \ b = c \ (a \ b \ a \ c)" by (simp add: fresh_def supp_swap supp_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: supp_perm) lemma supp_plus_perm: fixes p q::perm shows "supp (p + q) \ supp p \ supp q" by (auto simp: 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) lemma plus_perm_eq: fixes p q::"perm" assumes asm: "supp p \ supp q = {}" shows "p + q = q + p" unfolding perm_eq_iff 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 lemma supp_plus_perm_eq: fixes p q::perm assumes asm: "supp p \ supp q = {}" shows "supp (p + q) = supp p \ supp q" proof - { fix a::"atom" assume "a \ supp p" then have "a \ supp q" using asm by auto then have "a \ supp (p + q)" using \a \ supp p\ by (simp add: supp_perm) } moreover { fix a::"atom" assume "a \ supp q" then have "a \ supp p" using asm by auto then have "a \ supp (q + p)" using \a \ supp q\ by (simp add: supp_perm) then have "a \ supp (p + q)" using asm plus_perm_eq by metis } ultimately have "supp p \ supp q \ supp (p + q)" by blast then show "supp (p + q) = supp p \ supp q" using supp_plus_perm by blast qed lemma perm_eq_iff2: fixes p q :: "perm" shows "p = q \ (\a::atom \ supp p \ supp q. p \ a = q \ a)" unfolding perm_eq_iff apply(auto) apply(case_tac "a \ p \ a \ q") apply(simp add: fresh_perm) apply(simp add: fresh_def) done instance perm :: fs by standard (simp add: supp_perm finite_perm_lemma) 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 standard apply (case_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 standard apply (case_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 standard 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 fresh_Nil: shows "a \ []" by (simp add: fresh_def supp_Nil) lemma supp_Cons: shows "supp (x # xs) = supp x \ supp xs" by (simp add: supp_def Collect_imp_eq Collect_neg_eq) lemma fresh_Cons: shows "a \ (x # xs) \ a \ x \ a \ xs" by (simp add: fresh_def supp_Cons) lemma supp_append: shows "supp (xs @ ys) = supp xs \ supp ys" by (induct xs) (auto simp: 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 supp_rev: shows "supp (rev xs) = supp xs" by (induct xs) (auto simp: supp_append supp_Cons supp_Nil) lemma fresh_rev: shows "a \ rev xs \ a \ xs" by (induct xs) (auto simp: fresh_append fresh_Cons fresh_Nil) lemma supp_removeAll: fixes x::"atom" shows "supp (removeAll x xs) = supp xs - {x}" by (induct xs) (auto simp: supp_Nil supp_Cons supp_atom) lemma supp_of_atom_list: fixes as::"atom list" shows "supp as = set as" by (induct as) (simp_all add: supp_Nil supp_Cons supp_atom) instance list :: (fs) fs apply standard 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 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 subsection \Equivariance Predicate \eqvt\ and \eqvt_at\\ definition "eqvt f \ \p. p \ f = f" lemma eqvt_boolI: fixes f::"bool" shows "eqvt f" unfolding eqvt_def by (simp add: permute_bool_def) text \equivariance of a function at a given argument\ definition "eqvt_at f x \ \p. p \ (f x) = f (p \ x)" lemma eqvtI: shows "(\p. p \ f \ f) \ eqvt f" unfolding eqvt_def by simp lemma eqvt_at_perm: assumes "eqvt_at f x" shows "eqvt_at f (q \ x)" proof - { fix p::"perm" have "p \ (f (q \ x)) = p \ q \ (f x)" using assms by (simp add: eqvt_at_def) also have "\ = (p + q) \ (f x)" by simp also have "\ = f ((p + q) \ x)" using assms by (simp only: eqvt_at_def) finally have "p \ (f (q \ x)) = f (p \ q \ x)" by simp } then show "eqvt_at f (q \ x)" unfolding eqvt_at_def by simp qed lemma supp_fun_eqvt: assumes a: "eqvt f" shows "supp f = {}" using a unfolding eqvt_def unfolding supp_def by simp lemma fresh_fun_eqvt: assumes a: "eqvt f" shows "a \ f" using a unfolding fresh_def by (simp add: supp_fun_eqvt) lemma fresh_fun_eqvt_app: assumes a: "eqvt 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 lemma supp_fun_app_eqvt: assumes a: "eqvt f" shows "supp (f x) \ supp x" using fresh_fun_eqvt_app[OF a] unfolding fresh_def by auto lemma supp_eqvt_at: assumes asm: "eqvt_at f x" and fin: "finite (supp x)" shows "supp (f x) \ supp x" apply(rule supp_is_subset) unfolding supports_def unfolding fresh_def[symmetric] using asm apply(simp add: eqvt_at_def) apply(simp add: swap_fresh_fresh) apply(rule fin) done lemma finite_supp_eqvt_at: assumes asm: "eqvt_at f x" and fin: "finite (supp x)" shows "finite (supp (f x))" apply(rule finite_subset) apply(rule supp_eqvt_at[OF asm fin]) apply(rule fin) done lemma fresh_eqvt_at: assumes asm: "eqvt_at f x" and fin: "finite (supp x)" and fresh: "a \ x" shows "a \ f x" using fresh unfolding fresh_def using supp_eqvt_at[OF asm fin] by auto text \for handling of freshness of functions\ simproc_setup fresh_fun_simproc ("a \ (f::'a::pt \'b::pt)") = \fn _ => fn ctxt => fn ctrm => let val _ $ _ $ f = Thm.term_of ctrm in case (Term.add_frees f [], Term.add_vars f []) of ([], []) => SOME(@{thm fresh_fun_eqvt[simplified eqvt_def, THEN Eq_TrueI]}) | (x::_, []) => let val argx = Free x val absf = absfree x f val cty_inst = [SOME (Thm.ctyp_of ctxt (fastype_of argx)), SOME (Thm.ctyp_of ctxt (fastype_of f))] val ctrm_inst = [NONE, SOME (Thm.cterm_of ctxt absf), SOME (Thm.cterm_of ctxt argx)] val thm = Thm.instantiate' cty_inst ctrm_inst @{thm fresh_fun_app} in SOME(thm RS @{thm Eq_TrueI}) end | (_, _) => NONE end \ subsection \helper functions for \nominal_functions\\ lemma THE_defaultI2: assumes "\!x. P x" "\x. P x \ Q x" shows "Q (THE_default d P)" by (iprover intro: assms THE_defaultI') lemma the_default_eqvt: assumes unique: "\!x. P x" shows "(p \ (THE_default d P)) = (THE_default (p \ d) (p \ P))" apply(rule THE_default1_equality [symmetric]) apply(rule_tac p="-p" in permute_boolE) apply(simp add: ex1_eqvt) apply(rule unique) apply(rule_tac p="-p" in permute_boolE) apply(rule subst[OF permute_fun_app_eq]) apply(simp) apply(rule THE_defaultI'[OF unique]) done lemma fundef_ex1_eqvt: fixes x::"'a::pt" assumes f_def: "f == (\x::'a. THE_default (d x) (G x))" assumes eqvt: "eqvt G" assumes ex1: "\!y. G x y" shows "(p \ (f x)) = f (p \ x)" apply(simp only: f_def) apply(subst the_default_eqvt) apply(rule ex1) apply(rule THE_default1_equality [symmetric]) apply(rule_tac p="-p" in permute_boolE) apply(perm_simp add: permute_minus_cancel) using eqvt[simplified eqvt_def] apply(simp) apply(rule ex1) apply(rule THE_defaultI2) apply(rule_tac p="-p" in permute_boolE) apply(perm_simp add: permute_minus_cancel) apply(rule ex1) apply(perm_simp) using eqvt[simplified eqvt_def] apply(simp) done lemma fundef_ex1_eqvt_at: fixes x::"'a::pt" assumes f_def: "f == (\x::'a. THE_default (d x) (G x))" assumes eqvt: "eqvt G" assumes ex1: "\!y. G x y" shows "eqvt_at f x" unfolding eqvt_at_def using assms by (auto intro: fundef_ex1_eqvt) lemma fundef_ex1_prop: fixes x::"'a::pt" assumes f_def: "f == (\x::'a. THE_default (d x) (G x))" assumes P_all: "\x y. G x y \ P x y" assumes ex1: "\!y. G x y" shows "P x (f x)" unfolding f_def using ex1 apply(erule_tac ex1E) apply(rule THE_defaultI2) apply(blast) apply(rule P_all) apply(assumption) done section \Support of Finite Sets of Finitely Supported Elements\ text \support and freshness for atom sets\ 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 lemma supp_cofinite_atom_set: fixes S::"atom set" assumes "finite (UNIV - S)" shows "supp S = (UNIV - S)" apply(rule finite_supp_unique) apply(simp add: supports_def) apply(simp add: swap_set_both_in) apply(rule assms) apply(subst swap_commute) apply(simp add: swap_set_in) done lemma fresh_finite_atom_set: fixes S::"atom set" assumes "finite S" shows "a \ S \ a \ S" unfolding fresh_def by (simp add: supp_finite_atom_set[OF assms]) lemma fresh_minus_atom_set: fixes S::"atom set" assumes "finite S" shows "a \ S - T \ (a \ T \ a \ S)" unfolding fresh_def by (auto simp: supp_finite_atom_set assms) 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_def 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: 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 eqvt: "eqvt (\S. \x \ S. supp x)" unfolding eqvt_def by simp have "(\x\S. supp x) = supp (\x\S. supp x)" by (rule supp_finite_atom_set[symmetric]) (rule Union_of_finite_supp_sets[OF fin]) also have "\ \ supp S" using eqvt by (rule supp_fun_app_eqvt) 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 fresh_finite_union: fixes S T::"('a::fs) set" assumes fin1: "finite S" and fin2: "finite T" shows "a \ (S \ T) \ a \ S \ a \ T" unfolding fresh_def by (simp add: supp_of_finite_union[OF fin1 fin2]) 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) lemma fresh_finite_insert: fixes S::"('a::fs) set" assumes fin: "finite S" shows "a \ (insert x S) \ a \ x \ a \ S" using fin unfolding fresh_def by (simp add: supp_of_finite_insert) 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 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 lemma fresh_set: fixes xs :: "('a::fs) list" shows "a \ (set xs) \ a \ xs" unfolding fresh_def by (simp add: supp_set) subsection \Type @{typ "'a multiset"} is finitely supported\ lemma set_mset_eqvt [eqvt]: shows "p \ (set_mset M) = set_mset (p \ M)" by (induct M) (simp_all add: insert_eqvt empty_eqvt) lemma supp_set_mset: shows "supp (set_mset M) \ supp M" apply (rule supp_fun_app_eqvt) unfolding eqvt_def apply(perm_simp) apply(simp) done lemma Union_finite_multiset: fixes M::"'a::fs multiset" shows "finite (\{supp x | x. x \# M})" proof - have "finite (\(supp ` {x. x \# M}))" by (induct M) (simp_all add: Collect_imp_eq Collect_neg_eq finite_supp) then show "finite (\{supp x | x. x \# M})" by (simp only: image_Collect) qed lemma Union_supports_multiset: shows "\{supp x | x. x \# M} supports M" proof - have sw: "\a b. ((\x. x \# M \ (a \ b) \ x = x) \ (a \ b) \ M = M)" unfolding permute_multiset_def by (induct M) simp_all have "(\x\set_mset M. supp x) supports M" by (auto intro!: sw swap_fresh_fresh simp add: fresh_def supports_def) also have "(\x\set_mset M. supp x) = (\{supp x | x. x \# M})" by auto finally show "(\{supp x | x. x \# M}) supports M" . qed lemma Union_included_multiset: fixes M::"('a::fs multiset)" shows "(\{supp x | x. x \# M}) \ supp M" proof - have "(\{supp x | x. x \# M}) = (\x \ set_mset M. supp x)" by auto also have "... = supp (set_mset M)" by (simp add: supp_of_finite_sets) also have " ... \ supp M" by (rule supp_set_mset) finally show "(\{supp x | x. x \# M}) \ supp M" . qed lemma supp_of_multisets: fixes M::"('a::fs multiset)" shows "(supp M) = (\{supp x | x. x \# M})" apply(rule subset_antisym) apply(rule supp_is_subset) apply(rule Union_supports_multiset) apply(rule Union_finite_multiset) apply(rule Union_included_multiset) done lemma multisets_supp_finite: fixes M::"('a::fs multiset)" shows "finite (supp M)" by (simp only: supp_of_multisets Union_finite_multiset) lemma supp_of_multiset_union: fixes M N::"('a::fs) multiset" shows "supp (M + N) = supp M \ supp N" by (auto simp: supp_of_multisets) lemma supp_empty_mset [simp]: shows "supp {#} = {}" unfolding supp_def by simp instance multiset :: (fs) fs by standard (rule multisets_supp_finite) subsection \Type @{typ "'a fset"} is finitely supported\ 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 fresh_empty_fset: shows "a \ {||}" unfolding fresh_def by (simp) lemma supp_finsert [simp]: fixes x::"'a::fs" and S::"'a fset" shows "supp (finsert x S) = supp x \ supp S" apply(subst supp_fset[symmetric]) apply(simp add: supp_of_finite_insert) done lemma fresh_finsert: fixes x::"'a::fs" and S::"'a fset" shows "a \ finsert x S \ a \ x \ a \ S" unfolding fresh_def by simp lemma fset_finite_supp: fixes S::"('a::fs) fset" shows "finite (supp S)" by (induct S) (simp_all add: finite_supp) lemma supp_union_fset: fixes S T::"'a::fs fset" shows "supp (S |\| T) = supp S \ supp T" by (induct S) (auto) lemma fresh_union_fset: fixes S T::"'a::fs fset" shows "a \ S |\| T \ a \ S \ a \ T" unfolding fresh_def by (simp add: supp_union_fset) instance fset :: (fs) fs by standard (rule fset_finite_supp) subsection \Type @{typ "('a, 'b) finfun"} is finitely supported\ lemma fresh_finfun_const: shows "a \ (finfun_const b) \ a \ b" by (simp add: fresh_def supp_def) lemma fresh_finfun_update: shows "\a \ f; a \ x; a \ y\ \ a \ finfun_update f x y" unfolding fresh_conv_MOST unfolding finfun_update_eqvt by (elim MOST_rev_mp) (simp) lemma supp_finfun_const: shows "supp (finfun_const b) = supp(b)" by (simp add: supp_def) lemma supp_finfun_update: shows "supp (finfun_update f x y) \ supp(f, x, y)" using fresh_finfun_update by (auto simp: fresh_def supp_Pair) instance finfun :: (fs, fs) fs apply standard apply(induct_tac x rule: finfun_weak_induct) apply(simp add: supp_finfun_const finite_supp) apply(rule finite_subset) apply(rule supp_finfun_update) apply(simp add: supp_Pair finite_supp) done section \Freshness and Fresh-Star\ lemma fresh_Unit_elim: shows "(a \ () \ PROP C) \ PROP C" by (simp add: fresh_Unit) lemma fresh_Pair_elim: shows "(a \ (x, y) \ PROP C) \ (a \ x \ a \ y \ PROP C)" by rule (simp_all add: fresh_Pair) (* this rule needs to be added before the fresh_prodD is *) (* added to the simplifier with mksimps *) lemma [simp]: shows "a \ x1 \ a \ x2 \ a \ (x1, x2)" by (simp add: fresh_Pair) lemma fresh_PairD: shows "a \ (x, y) \ a \ x" and "a \ (x, y) \ a \ y" by (simp_all add: fresh_Pair) declaration \fn _ => let val mksimps_pairs = (@{const_name Nominal2_Base.fresh}, @{thms fresh_PairD}) :: mksimps_pairs in Simplifier.map_ss (fn ss => Simplifier.set_mksimps (mksimps mksimps_pairs) ss) end \ 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: fresh_star_def fresh_def) lemma fresh_star_perm_set_conv: fixes p::"perm" assumes fresh: "as \* p" and fin: "finite as" shows "supp p \* as" apply(rule fresh_star_supp_conv) apply(simp add: supp_finite_atom_set fin fresh) done lemma fresh_star_atom_set_conv: assumes fresh: "as \* bs" and fin: "finite as" "finite bs" shows "bs \* as" using fresh unfolding fresh_star_def fresh_def by (auto simp: supp_finite_atom_set fin) lemma atom_fresh_star_disjoint: assumes fin: "finite bs" shows "as \* bs \ (as \ bs = {})" unfolding fresh_star_def fresh_def by (auto simp: supp_finite_atom_set fin) lemma fresh_star_Pair: shows "as \* (x, y) = (as \* x \ as \* y)" by (auto simp: fresh_star_def fresh_Pair) lemma fresh_star_list: shows "as \* (xs @ ys) \ as \* xs \ as \* ys" and "as \* (x # xs) \ as \* x \ as \* xs" and "as \* []" by (auto simp: fresh_star_def fresh_Nil fresh_Cons fresh_append) lemma fresh_star_set: fixes xs::"('a::fs) list" shows "as \* set xs \ as \* xs" unfolding fresh_star_def by (simp add: fresh_set) lemma fresh_star_singleton: fixes a::"atom" shows "as \* {a} \ as \* a" by (simp add: fresh_star_def fresh_finite_insert fresh_set_empty) lemma fresh_star_fset: fixes xs::"('a::fs) list" shows "as \* fset S \ as \* S" by (simp add: fresh_star_def fresh_def) lemma fresh_star_Un: shows "(as \ bs) \* x = (as \* x \ bs \* x)" by (auto simp: fresh_star_def) lemma fresh_star_insert: shows "(insert a as) \* x = (a \ x \ as \* x)" by (auto simp: 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_Pair_elim: shows "(a \* (x, y) \ PROP C) \ (a \* x \ a \* y \ PROP C)" by (rule, simp_all add: fresh_star_Pair) 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 [eqvt]: shows "p \ (as \* x) \ (p \ as) \* (p \ x)" unfolding fresh_star_def by simp section \Induction principle for permutations\ lemma smaller_supp: assumes a: "a \ supp p" shows "supp ((p \ a \ a) + p) \ supp p" proof - have "supp ((p \ a \ a) + p) \ supp p" unfolding supp_perm by (auto simp: swap_atom) moreover have "a \ supp ((p \ a \ a) + p)" by (simp add: supp_perm) then have "supp ((p \ a \ a) + p) \ supp p" using a by auto ultimately show "supp ((p \ a \ a) + p) \ supp p" by auto qed 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 perm_eq_iff) 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: supp_atom supp_perm swap_atom) let ?q = "(p \ a \ a) + p" have a2: "supp ?q \ supp p" using a0 smaller_supp by simp 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: perm_eq_iff) 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_struct_induct2[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 perm_simple_struct_induct2[case_names zero swap plus]: assumes zero: "P 0" assumes swap: "\a b. \sort_of a = sort_of b; a \ b\ \ P (a \ b)" assumes plus: "\p1 p2. \P p1; P p2\ \ P (p1 + p2)" shows "P p" by (rule_tac S="supp p" in perm_struct_induct2) (auto intro: zero swap plus) lemma supp_perm_singleton: fixes p::"perm" shows "supp p \ {b} \ p = 0" proof - { assume "supp p \ {b}" then have "p = 0" by (induct p rule: perm_struct_induct) (simp_all) } then show "supp p \ {b} \ p = 0" by (auto simp: supp_zero_perm) qed lemma supp_perm_pair: fixes p::"perm" shows "supp p \ {a, b} \ p = 0 \ p = (b \ a)" proof - { assume "supp p \ {a, b}" then have "p = 0 \ p = (b \ a)" apply (induct p rule: perm_struct_induct) apply (auto simp: swap_cancel supp_zero_perm supp_swap) apply (simp add: swap_commute) done } then show "supp p \ {a, b} \ p = 0 \ p = (b \ a)" by (auto simp: supp_zero_perm supp_swap split: if_splits) qed 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 text \same lemma as above, but proved with a different induction principle\ 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_struct_induct2) 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 lemma perm_supp_eq: assumes a: "(supp p) \* x" 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_induct2) 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 lemma supp_perm_perm_eq: assumes a: "\a \ supp x. p \ a = q \ a" shows "p \ x = q \ x" proof - from a have "\a \ supp x. (-q + p) \ a = a" by simp then have "\a \ supp x. a \ supp (-q + p)" unfolding supp_perm by simp then have "supp x \* (-q + p)" unfolding fresh_star_def fresh_def by simp then have "(-q + p) \ x = x" by (simp only: supp_perm_eq) then show "p \ x = q \ x" by (metis permute_minus_cancel permute_plus) qed text \disagreement set\ definition dset :: "perm \ perm \ atom set" where "dset p q = {a::atom. p \ a \ q \ a}" lemma ds_fresh: assumes "dset p q \* x" shows "p \ x = q \ x" using assms unfolding dset_def fresh_star_def fresh_def by (auto intro: supp_perm_perm_eq) lemma atom_set_perm_eq: assumes a: "as \* p" shows "p \ as = as" proof - from a have "supp p \ {a. a \ as}" unfolding supp_perm fresh_star_def fresh_def by auto then show "p \ as = as" proof (induct p rule: perm_struct_induct) case zero show "0 \ as = as" by simp next case (swap p a b) then have "a \ as" "b \ as" "p \ as = as" by simp_all then show "((a \ b) + p) \ as = as" by (simp add: swap_set_not_in) 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 \ supp p)" using \finite As\ \finite Xs\ by (simp add: permute_set_eq_image finite_supp) then obtain y where "y \ (As \ p \ Xs \ supp p)" "sort_of y = sort_of x" by (rule obtain_atom) hence y: "y \ As" "y \ p \ Xs" "y \ supp p" "sort_of y = sort_of x" by simp_all hence py: "p \ y = y" "x \ y" using \x \ As\ by (auto simp: supp_perm) 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 (x \ y) \ supp p = {}" using px py \sort_of y = sort_of x\ unfolding supp_swap by (simp add: supp_perm) then have "supp ?q = (supp (x \ y) \ supp p)" by (simp add: supp_plus_perm_eq) then have "supp ?q = insert x Xs \ ?q \ insert x Xs" using p2 \sort_of y = sort_of x\ \x \ y\ unfolding q supp_swap by auto 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_avoiding1: assumes "finite xs" and "finite (supp c)" shows "\p. (p \ xs) \* c" using assms apply(erule_tac c="c" in at_set_avoiding) apply(auto) done 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_Pair) apply(rule fresh_star_supp_conv) apply(auto simp: fresh_star_def) done lemma at_set_avoiding3: assumes "finite xs" and "finite (supp c)" "finite (supp x)" and "xs \* x" shows "\p. (p \ xs) \* c \ supp x \* p \ supp p = xs \ (p \ xs)" 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_Pair) apply(rule fresh_star_supp_conv) apply(auto simp: 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_def) hence "p \ a \ c \ supp x \* p" using p2 by blast then show "\p. (p \ a) \ c \ supp x \* p" by blast qed section \Renaming permutations\ lemma set_renaming_perm: assumes b: "finite bs" shows "\q. (\b \ bs. q \ b = p \ b) \ supp q \ bs \ (p \ bs)" using b proof (induct) case empty have "(\b \ {}. 0 \ b = p \ b) \ supp (0::perm) \ {} \ p \ {}" by (simp add: permute_set_def supp_perm) then show "\q. (\b \ {}. q \ b = p \ b) \ supp q \ {} \ p \ {}" by blast next case (insert a bs) then have " \q. (\b \ bs. q \ b = p \ b) \ supp q \ bs \ p \ bs" by simp then obtain q where *: "\b \ bs. q \ b = p \ b" and **: "supp q \ bs \ p \ bs" by (metis empty_subsetI insert(3) supp_swap) { assume 1: "q \ a = p \ a" have "\b \ (insert a bs). q \ b = p \ b" using 1 * by simp moreover have "supp q \ insert a bs \ p \ insert a bs" using ** by (auto simp: insert_eqvt) ultimately have "\q. (\b \ insert a bs. q \ b = p \ b) \ supp q \ insert a bs \ p \ insert a bs" by blast } moreover { assume 2: "q \ a \ p \ a" define q' where "q' = ((q \ a) \ (p \ a)) + q" have "\b \ insert a bs. q' \ b = p \ b" using 2 * \a \ bs\ unfolding q'_def by (auto simp: swap_atom) moreover { have "{q \ a, p \ a} \ insert a bs \ p \ insert a bs" using ** apply (auto simp: supp_perm insert_eqvt) apply (subgoal_tac "q \ a \ bs \ p \ bs") apply(auto)[1] apply(subgoal_tac "q \ a \ {a. q \ a \ a}") apply(blast) apply(simp) done then have "supp (q \ a \ p \ a) \ insert a bs \ p \ insert a bs" unfolding supp_swap by auto moreover have "supp q \ insert a bs \ p \ insert a bs" using ** by (auto simp: insert_eqvt) ultimately have "supp q' \ insert a bs \ p \ insert a bs" unfolding q'_def using supp_plus_perm by blast } ultimately have "\q. (\b \ insert a bs. q \ b = p \ b) \ supp q \ insert a bs \ p \ insert a bs" by blast } ultimately show "\q. (\b \ insert a bs. q \ b = p \ b) \ supp q \ insert a bs \ p \ insert a bs" by blast qed lemma set_renaming_perm2: shows "\q. (\b \ bs. q \ b = p \ b) \ supp q \ bs \ (p \ bs)" proof - have "finite (bs \ supp p)" by (simp add: finite_supp) then obtain q where *: "\b \ bs \ supp p. q \ b = p \ b" and **: "supp q \ (bs \ supp p) \ (p \ (bs \ supp p))" using set_renaming_perm by blast from ** have "supp q \ bs \ (p \ bs)" by (auto simp: inter_eqvt) moreover have "\b \ bs - supp p. q \ b = p \ b" apply(auto) apply(subgoal_tac "b \ supp q") apply(simp add: fresh_def[symmetric]) apply(simp add: fresh_perm) apply(clarify) apply(rotate_tac 2) apply(drule subsetD[OF **]) apply(simp add: inter_eqvt supp_eqvt permute_self) done ultimately have "(\b \ bs. q \ b = p \ b) \ supp q \ bs \ (p \ bs)" using * by auto then show "\q. (\b \ bs. q \ b = p \ b) \ supp q \ bs \ (p \ bs)" by blast qed lemma list_renaming_perm: shows "\q. (\b \ set bs. q \ b = p \ b) \ supp q \ set bs \ (p \ set bs)" proof (induct bs) case (Cons a bs) then have " \q. (\b \ set bs. q \ b = p \ b) \ supp q \ set bs \ p \ (set bs)" by simp then obtain q where *: "\b \ set bs. q \ b = p \ b" and **: "supp q \ set bs \ p \ (set bs)" by (blast) { assume 1: "a \ set bs" have "q \ a = p \ a" using * 1 by (induct bs) (auto) then have "\b \ set (a # bs). q \ b = p \ b" using * by simp moreover have "supp q \ set (a # bs) \ p \ (set (a # bs))" using ** by (auto simp: insert_eqvt) ultimately have "\q. (\b \ set (a # bs). q \ b = p \ b) \ supp q \ set (a # bs) \ p \ (set (a # bs))" by blast } moreover { assume 2: "a \ set bs" define q' where "q' = ((q \ a) \ (p \ a)) + q" have "\b \ set (a # bs). q' \ b = p \ b" unfolding q'_def using 2 * \a \ set bs\ by (auto simp: swap_atom) moreover { have "{q \ a, p \ a} \ set (a # bs) \ p \ (set (a # bs))" using ** apply (auto simp: supp_perm insert_eqvt) apply (subgoal_tac "q \ a \ set bs \ p \ set bs") apply(auto)[1] apply(subgoal_tac "q \ a \ {a. q \ a \ a}") apply(blast) apply(simp) done then have "supp (q \ a \ p \ a) \ set (a # bs) \ p \ set (a # bs)" unfolding supp_swap by auto moreover have "supp q \ set (a # bs) \ p \ (set (a # bs))" using ** by (auto simp: insert_eqvt) ultimately have "supp q' \ set (a # bs) \ p \ (set (a # bs))" unfolding q'_def using supp_plus_perm by blast } ultimately have "\q. (\b \ set (a # bs). q \ b = p \ b) \ supp q \ set (a # bs) \ p \ (set (a # bs))" by blast } ultimately show "\q. (\b \ set (a # bs). q \ b = p \ b) \ supp q \ set (a # bs) \ p \ (set (a # bs))" by blast next case Nil have "(\b \ set []. 0 \ b = p \ b) \ supp (0::perm) \ set [] \ p \ set []" by (simp add: supp_zero_perm) then show "\q. (\b \ set []. q \ b = p \ b) \ supp q \ set [] \ p \ (set [])" by blast qed section \Concrete Atoms Types\ text \ Class \at_base\ allows types containing multiple sorts of atoms. Class \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)" declare atom_eqvt [eqvt] class at = at_base + assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)" lemma sort_ineq [simp]: assumes "sort_of (atom a) \ sort_of (atom b)" shows "atom a \ atom b" using assms by metis 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 "sort_of a \ sort_of (atom b) \ a \ b" and "a \ b \ a \ atom b" unfolding fresh_def apply(simp_all add: supp_at_base) apply(metis) done (* solves the freshness only if the inequality can be shown by the simproc below *) lemma fresh_ineq_at_base [simp]: shows "a \ atom b \ a \ b" by (simp add: fresh_at_base) lemma fresh_atom_at_base [simp]: fixes b::"'a::at_base" shows "a \ atom b \ a \ b" by (simp add: fresh_def supp_at_base supp_atom) lemma fresh_star_atom_at_base: fixes b::"'a::at_base" shows "as \* atom b \ as \* b" by (simp add: fresh_star_def fresh_atom_at_base) lemma if_fresh_at_base [simp]: shows "atom a \ x \ P (if a = x then t else s) = P s" and "atom a \ x \ P (if x = a then t else s) = P s" by (simp_all add: fresh_at_base) simproc_setup fresh_ineq ("x \ (y::'a::at_base)") = \fn _ => fn ctxt => fn ctrm => case Thm.term_of ctrm of \<^Const_>\Not for \<^Const_>\HOL.eq _ for lhs rhs\\ => let fun first_is_neg lhs rhs [] = NONE | first_is_neg lhs rhs (thm::thms) = (case Thm.prop_of thm of _ $ \<^Const_>\Not for \<^Const_>\HOL.eq _ for l r\\ => (if l = lhs andalso r = rhs then SOME(thm) else if r = lhs andalso l = rhs then SOME(thm RS @{thm not_sym}) else first_is_neg lhs rhs thms) | _ => first_is_neg lhs rhs thms) val simp_thms = @{thms fresh_Pair fresh_at_base atom_eq_iff} val prems = Simplifier.prems_of ctxt |> filter (fn thm => case Thm.prop_of thm of _ $ \<^Const_>\fresh _ for \_ $ a\ b\ => (let val atms = a :: HOLogic.strip_tuple b in member (op =) atms lhs andalso member (op =) atms rhs end) | _ => false) |> map (simplify (put_simpset HOL_basic_ss ctxt addsimps simp_thms)) |> map (HOLogic.conj_elims ctxt) |> flat in case first_is_neg lhs rhs prems of SOME(thm) => SOME(thm RS @{thm Eq_TrueI}) | NONE => NONE end | _ => NONE \ 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 obtain_fresh': assumes fin: "finite (supp x)" obtains a::"'a::at_base" where "atom a \ x" using obtain_at_base[where X="supp x"] by (auto simp: fresh_def fin) lemma obtain_fresh: fixes x::"'b::fs" obtains a::"'a::at_base" where "atom a \ x" by (rule obtain_fresh') (auto simp: finite_supp) 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 (* FIXME lemma supp_cofinite_set_at_base: assumes a: "finite (UNIV - S)" shows "supp S = atom ` (UNIV - S)" apply(rule finite_supp_unique) *) lemma fresh_finite_set_at_base: fixes a::"'a::at_base" assumes a: "finite S" shows "atom a \ S \ a \ S" unfolding fresh_def apply(simp add: supp_finite_set_at_base[OF a]) apply(subst inj_image_mem_iff) apply(simp add: inj_on_def) apply(simp) done lemma fresh_at_base_permute_iff [simp]: fixes a::"'a::at_base" shows "atom (p \ a) \ p \ x \ atom a \ x" unfolding atom_eqvt[symmetric] by (simp only: fresh_permute_iff) lemma fresh_at_base_permI: shows "atom a \ p \ p \ a = a" by (simp add: fresh_def supp_perm) section \Infrastructure for concrete atom types\ definition flip :: "'a::at_base \ 'a \ perm" ("'(_ \ _')") where "(a \ b) = (atom a \ atom b)" lemma flip_fresh_fresh: assumes "atom a \ x" "atom b \ x" shows "(a \ b) \ x = x" using assms by (simp add: flip_def swap_fresh_fresh) 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 [eqvt]: 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 flip_triple: fixes a b c::"'a::at" assumes "a \ b" and "c \ b" shows "(a \ c) + (b \ c) + (a \ c) = (a \ b)" unfolding flip_def by (rule swap_triple) (simp_all add: assms) 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 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 \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 lemma at_class_sort: fixes s :: atom_sort fixes Rep :: "'a \ atom" and Abs :: "atom \ 'a" fixes a::"'a" assumes type: "type_definition Rep Abs {a. sort_of a = s}" assumes atom_def: "\a. atom a = Rep a" shows "sort_of (atom a) = s" using atom_def type unfolding type_definition_def by simp 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 \Library functions for the nominal infrastructure\ ML_file \nominal_library.ML\ 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: 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: fresh_Pair) qed text \packaging the freshness lemma into a function\ definition Fresh :: "('a::at \ 'b::pt) \ 'b" where "Fresh h = (THE x. \a. atom a \ h \ h a = x)" lemma Fresh_apply: fixes h :: "'a::at \ 'b::pt" assumes a: "\a. atom a \ (h, h a)" assumes b: "atom a \ h" shows "Fresh h = h a" unfolding Fresh_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_apply': fixes h :: "'a::at \ 'b::pt" assumes a: "atom a \ h" "atom a \ h a" shows "Fresh h = h a" apply (rule Fresh_apply) apply (auto simp: fresh_Pair intro: a) done simproc_setup Fresh_simproc ("Fresh (h::'a::at \ 'b::pt)") = \fn _ => fn ctxt => fn ctrm => let val _ $ h = Thm.term_of ctrm val atoms = Simplifier.prems_of ctxt |> map_filter (fn thm => case Thm.prop_of thm of _ $ \<^Const_>\fresh _ for \<^Const_>\atom _ for atm\ _\ => SOME atm | _ => NONE) |> distinct (op =) fun get_thm atm = let val goal1 = HOLogic.mk_Trueprop (mk_fresh (mk_atom atm) h) val goal2 = HOLogic.mk_Trueprop (mk_fresh (mk_atom atm) (h $ atm)) - val thm1 = Goal.prove ctxt [] [] goal1 (K (asm_simp_tac ctxt 1)) - val thm2 = Goal.prove ctxt [] [] goal2 (K (asm_simp_tac ctxt 1)) + val thm1 = Goal.prove ctxt [] [] goal1 (fn {context = ctxt', ...} => asm_simp_tac ctxt' 1) + val thm2 = Goal.prove ctxt [] [] goal2 (fn {context = ctxt', ...} => asm_simp_tac ctxt' 1) in SOME (@{thm Fresh_apply'} OF [thm1, thm2] RS eq_reflection) end handle ERROR _ => NONE in get_first get_thm atoms end \ lemma Fresh_eqvt: fixes h :: "'a::at \ 'b::pt" assumes a: "\a. atom a \ (h, h a)" shows "p \ (Fresh h) = Fresh (p \ h)" proof - from a obtain a::"'a::at" where fr: "atom a \ h" "atom a \ h a" by (metis fresh_Pair) then have fr_p: "atom (p \ a) \ (p \ h)" "atom (p \ a) \ (p \ h) (p \ a)" by (metis atom_eqvt fresh_permute_iff eqvt_apply)+ have "p \ (Fresh h) = p \ (h a)" using fr by simp also have "... = (p \ h) (p \ a)" by simp also have "... = Fresh (p \ h)" using fr_p by simp finally show "p \ (Fresh h) = Fresh (p \ h)" . qed lemma Fresh_supports: fixes h :: "'a::at \ 'b::pt" assumes a: "\a. atom a \ (h, h a)" shows "(supp h) supports (Fresh h)" apply (simp add: supports_def fresh_def [symmetric]) apply (simp add: Fresh_eqvt [OF a] swap_fresh_fresh) done notation Fresh (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 \ P" using P by (rule obtain_fresh') then show "(FRESH x. f (P x)) = f (FRESH x. P x)" by (simp add: pure_fresh) 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, Q))" by (simp add: supp_Pair) then obtain a::'a where "atom a \ (P, Q)" by (rule obtain_fresh') then show ?thesis by (simp add: pure_fresh) 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 \Automation for creating concrete atom types\ text \At the moment only single-sort concrete atoms are supported.\ ML_file \nominal_atoms.ML\ section \Automatic equivariance procedure for inductive definitions\ ML_file \nominal_eqvt.ML\ end diff --git a/thys/Nominal2/nominal_dt_alpha.ML b/thys/Nominal2/nominal_dt_alpha.ML --- a/thys/Nominal2/nominal_dt_alpha.ML +++ b/thys/Nominal2/nominal_dt_alpha.ML @@ -1,870 +1,873 @@ (* Title: nominal_dt_alpha.ML Author: Cezary Kaliszyk Author: Christian Urban Definitions and proofs for the alpha-relations. *) signature NOMINAL_DT_ALPHA = sig val comb_binders: Proof.context -> bmode -> term list -> (term option * int) list -> term val define_raw_alpha: raw_dt_info -> bn_info list -> bclause list list list -> term list -> Proof.context -> alpha_result * local_theory val induct_prove: typ list -> (typ * (term -> term)) list -> thm -> (Proof.context -> int -> tactic) -> Proof.context -> thm list val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> (Proof.context -> int -> tactic) -> Proof.context -> thm list val raw_prove_alpha_distincts: Proof.context -> alpha_result -> raw_dt_info -> thm list val raw_prove_alpha_eq_iff: Proof.context -> alpha_result -> raw_dt_info -> thm list val raw_prove_refl: Proof.context -> alpha_result -> thm -> thm list val raw_prove_sym: Proof.context -> alpha_result -> thm list -> thm list val raw_prove_trans: Proof.context -> alpha_result -> thm list -> thm list -> thm list val raw_prove_equivp: Proof.context -> alpha_result -> thm list -> thm list -> thm list -> thm list * thm list val raw_prove_bn_imp: Proof.context -> alpha_result -> thm list val raw_fv_bn_rsp_aux: Proof.context -> alpha_result -> term list -> term list -> term list -> thm list -> thm list val raw_size_rsp_aux: Proof.context -> alpha_result -> thm list -> thm list val raw_constrs_rsp: Proof.context -> alpha_result -> term list list -> thm list -> thm list list val raw_alpha_bn_rsp: alpha_result -> thm list -> thm list -> thm list val raw_perm_bn_rsp: Proof.context -> alpha_result -> term list -> thm list -> thm list val mk_funs_rsp: Proof.context -> thm -> thm val mk_alpha_permute_rsp: Proof.context -> thm -> thm end structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = struct open Nominal_Permeq open Nominal_Dt_Data fun lookup xs x = the (AList.lookup (op=) xs x) fun group xs = AList.group (op=) xs (** definition of the inductive rules for alpha and alpha_bn **) (* construct the compound terms for prod_fv and prod_alpha *) fun mk_prod_fv (t1, t2) = let val A = domain_type (fastype_of t1) val B = domain_type (fastype_of t2) in \<^Const>\prod_fv A B for t1 t2\ end fun mk_prod_alpha (t1, t2) = let val A = domain_type (fastype_of t1) val B = domain_type (fastype_of t2) in \<^Const>\prod_alpha A B for t1 t2\ end (* generates the compound binder terms *) fun comb_binders lthy bmode args binders = let fun bind_set lthy args (NONE, i) = setify lthy (nth args i) | bind_set _ args (SOME bn, i) = bn $ (nth args i) fun bind_lst lthy args (NONE, i) = listify lthy (nth args i) | bind_lst _ args (SOME bn, i) = bn $ (nth args i) val (combine_fn, bind_fn) = case bmode of Lst => (mk_append, bind_lst) | Set => (mk_union, bind_set) | Res => (mk_union, bind_set) in binders |> map (bind_fn lthy args) |> foldl1 combine_fn end (* produces the term for an alpha with abstraction *) fun mk_alpha_term bmode fv alpha args args' binders binders' = let val (alpha_name, binder_ty) = case bmode of Lst => (@{const_name "alpha_lst"}, @{typ "atom list"}) | Set => (@{const_name "alpha_set"}, @{typ "atom set"}) | Res => (@{const_name "alpha_res"}, @{typ "atom set"}) val ty = fastype_of args val pair_ty = HOLogic.mk_prodT (binder_ty, ty) val alpha_ty = [ty, ty] ---> @{typ "bool"} val fv_ty = ty --> @{typ "atom set"} val pair_lhs = HOLogic.mk_prod (binders, args) val pair_rhs = HOLogic.mk_prod (binders', args') in HOLogic.exists_const \<^Type>\perm\ $ Abs ("p", \<^Type>\perm\, Const (alpha_name, [pair_ty, alpha_ty, fv_ty, @{typ "perm"}, pair_ty] ---> @{typ bool}) $ pair_lhs $ alpha $ fv $ (Bound 0) $ pair_rhs) end (* for non-recursive binders we have to produce alpha_bn premises *) fun mk_alpha_bn_prem alpha_bn_map args args' bodies binder = case binder of (NONE, _) => [] | (SOME bn, i) => if member (op=) bodies i then [] else [lookup alpha_bn_map bn $ nth args i $ nth args' i] (* generate the premises for an alpha rule; mk_frees is used if no binders are present *) fun mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause = let fun mk_frees i = let val arg = nth args i val arg' = nth args' i val ty = fastype_of arg in if nth is_rec i then fst (lookup alpha_map ty) $ arg $ arg' else HOLogic.mk_eq (arg, arg') end fun mk_alpha_fv i = let val ty = fastype_of (nth args i) in case AList.lookup (op=) alpha_map ty of NONE => (HOLogic.eq_const ty, supp_const ty) | SOME (alpha, fv) => (alpha, fv) end in case bclause of BC (_, [], bodies) => map (HOLogic.mk_Trueprop o mk_frees) bodies | BC (bmode, binders, bodies) => let val (alphas, fvs) = split_list (map mk_alpha_fv bodies) val comp_fv = foldl1 mk_prod_fv fvs val comp_alpha = foldl1 mk_prod_alpha alphas val comp_args = foldl1 HOLogic.mk_prod (map (nth args) bodies) val comp_args' = foldl1 HOLogic.mk_prod (map (nth args') bodies) val comp_binders = comb_binders lthy bmode args binders val comp_binders' = comb_binders lthy bmode args' binders val alpha_prem = mk_alpha_term bmode comp_fv comp_alpha comp_args comp_args' comp_binders comp_binders' val alpha_bn_prems = flat (map (mk_alpha_bn_prem alpha_bn_map args args' bodies) binders) in map HOLogic.mk_Trueprop (alpha_prem::alpha_bn_prems) end end (* produces the introduction rule for an alpha rule *) fun mk_alpha_intros lthy alpha_map alpha_bn_map (constr, ty, arg_tys, is_rec) bclauses = let val arg_names = Old_Datatype_Prop.make_tnames arg_tys val arg_names' = Name.variant_list arg_names arg_names val args = map Free (arg_names ~~ arg_tys) val args' = map Free (arg_names' ~~ arg_tys) val alpha = fst (lookup alpha_map ty) val concl = HOLogic.mk_Trueprop (alpha $ list_comb (constr, args) $ list_comb (constr, args')) val prems = map (mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args')) bclauses in Library.foldr Logic.mk_implies (flat prems, concl) end (* produces the premise of an alpha-bn rule; we only need to treat the case special where the binding clause is empty; - if the body is not included in the bn_info, then we either produce an equation or an alpha-premise - if the body is included in the bn_info, then we create either a recursive call to alpha-bn, or no premise *) fun mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args') bclause = let fun mk_alpha_bn_prem i = let val arg = nth args i val arg' = nth args' i val ty = fastype_of arg in case AList.lookup (op=) bn_args i of NONE => (case (AList.lookup (op=) alpha_map ty) of NONE => [HOLogic.mk_eq (arg, arg')] | SOME (alpha, _) => [alpha $ arg $ arg']) | SOME (NONE) => [] | SOME (SOME bn) => [lookup alpha_bn_map bn $ arg $ arg'] end in case bclause of BC (_, [], bodies) => map HOLogic.mk_Trueprop (flat (map mk_alpha_bn_prem bodies)) | _ => mk_alpha_prems lthy alpha_map alpha_bn_map is_rec (args, args') bclause end fun mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map (bn_args, (constr, _, arg_tys, is_rec)) bclauses = let val arg_names = Old_Datatype_Prop.make_tnames arg_tys val arg_names' = Name.variant_list arg_names arg_names val args = map Free (arg_names ~~ arg_tys) val args' = map Free (arg_names' ~~ arg_tys) val alpha_bn = lookup alpha_bn_map bn_trm val concl = HOLogic.mk_Trueprop (alpha_bn $ list_comb (constr, args) $ list_comb (constr, args')) val prems = map (mk_alpha_bn lthy alpha_map alpha_bn_map bn_args is_rec (args, args')) bclauses in Library.foldr Logic.mk_implies (flat prems, concl) end fun mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = let val nth_constrs_info = nth constrs_info bn_n val nth_bclausess = nth bclausesss bn_n in map2 (mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess end fun define_raw_alpha raw_dt_info bn_info bclausesss fvs lthy = let val RawDtInfo {raw_dt_names, raw_tys, raw_cns_info, ...} = raw_dt_info val alpha_names = map (prefix "alpha_" o Long_Name.base_name) raw_dt_names val alpha_tys = map (fn ty => [ty, ty] ---> @{typ bool}) raw_tys val alpha_frees = map Free (alpha_names ~~ alpha_tys) val alpha_map = raw_tys ~~ (alpha_frees ~~ fvs) val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info) val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns val alpha_bn_names = map (prefix "alpha_") bn_names val alpha_bn_arg_tys = map (nth raw_tys) bn_tys val alpha_bn_tys = map (fn ty => [ty, ty] ---> @{typ "bool"}) alpha_bn_arg_tys val alpha_bn_frees = map Free (alpha_bn_names ~~ alpha_bn_tys) val alpha_bn_map = bns ~~ alpha_bn_frees val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) raw_cns_info bclausesss val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map raw_cns_info bclausesss) bn_info val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn)) (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys) val all_alpha_intros = map (pair Binding.empty_atts) (flat alpha_intros @ flat alpha_bn_intros) val (alpha_info, lthy') = lthy |> Local_Theory.begin_nested |> snd |> Inductive.add_inductive {quiet_mode = true, verbose = false, alt_name = Binding.empty, coind = false, no_elim = false, no_ind = false, skip_mono = false} all_alpha_names [] all_alpha_intros [] |> Local_Theory.end_nested_result Inductive.transform_result; val phi = Proof_Context.export_morphism lthy' (Proof_Context.transfer (Proof_Context.theory_of lthy') lthy); val alpha_info_global = Inductive.transform_result phi alpha_info; val all_alpha_trms = #preds alpha_info_global |> map Type.legacy_freeze (*FIXME*) val alpha_raw_induct = #raw_induct alpha_info_global val alpha_intros = #intrs alpha_info_global; val alpha_cases = #elims alpha_info_global; val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms val alpha_tys = map (domain_type o fastype_of) alpha_trms val alpha_bn_tys = map (domain_type o fastype_of) alpha_bn_trms val alpha_names = map (fst o dest_Const) alpha_trms val alpha_bn_names = map (fst o dest_Const) alpha_bn_trms in (AlphaResult {alpha_names = alpha_names, alpha_trms = alpha_trms, alpha_tys = alpha_tys, alpha_bn_names = alpha_bn_names, alpha_bn_trms = alpha_bn_trms, alpha_bn_tys = alpha_bn_tys, alpha_intros = alpha_intros, alpha_cases = alpha_cases, alpha_raw_induct = alpha_raw_induct}, lthy') end (** induction proofs **) (* proof by structural induction over data types *) fun induct_prove tys props induct_thm cases_tac ctxt = let val (arg_names, ctxt') = Variable.variant_fixes (replicate (length tys) "x") ctxt val args = map2 (curry Free) arg_names tys val true_trms = replicate (length tys) (K \<^Const>\True\) fun apply_all x fs = map (fn f => f x) fs val goals = group (props @ (tys ~~ true_trms)) |> map snd |> map2 apply_all args |> map fold_conj |> foldr1 HOLogic.mk_conj |> HOLogic.mk_Trueprop fun tac ctxt = HEADGOAL (DETERM o (resolve_tac ctxt [induct_thm]) THEN_ALL_NEW (REPEAT_ALL_NEW (FIRST' [resolve_tac ctxt @{thms TrueI conjI}, cases_tac ctxt]))) in - Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context) + Goal.prove ctxt' [] [] goals (tac o #context) |> singleton (Proof_Context.export ctxt' ctxt) |> Old_Datatype_Aux.split_conj_thm |> map Old_Datatype_Aux.split_conj_thm |> flat |> filter_out (is_true o Thm.concl_of) |> map zero_var_indexes end (* proof by rule induction over the alpha-definitions *) fun alpha_prove alphas props alpha_induct_thm cases_tac ctxt = let val arg_tys = map (domain_type o fastype_of) alphas val ((arg_names1, arg_names2), ctxt') = ctxt |> Variable.variant_fixes (replicate (length alphas) "x") ||>> Variable.variant_fixes (replicate (length alphas) "y") val args1 = map2 (curry Free) arg_names1 arg_tys val args2 = map2 (curry Free) arg_names2 arg_tys val true_trms = replicate (length alphas) (K \<^Const>\True\) fun apply_all x fs = map (fn f => f x) fs val goals_rhs = group (props @ (alphas ~~ true_trms)) |> map snd |> map2 apply_all (args1 ~~ args2) |> map fold_conj fun apply_trm_pair t (ar1, ar2) = t $ ar1 $ ar2 val goals_lhs = map2 apply_trm_pair alphas (args1 ~~ args2) val goals = (map2 (curry HOLogic.mk_imp) goals_lhs goals_rhs) |> foldr1 HOLogic.mk_conj |> HOLogic.mk_Trueprop fun tac ctxt = HEADGOAL (DETERM o (resolve_tac ctxt [alpha_induct_thm]) THEN_ALL_NEW FIRST' [resolve_tac ctxt @{thms TrueI}, cases_tac ctxt]) in - Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context) + Goal.prove ctxt' [] [] goals (tac o #context) |> singleton (Proof_Context.export ctxt' ctxt) |> Old_Datatype_Aux.split_conj_thm |> map (fn th => th RS mp) |> map Old_Datatype_Aux.split_conj_thm |> flat |> filter_out (is_true o Thm.concl_of) |> map zero_var_indexes end (** produces the distinctness theorems **) (* transforms the distinctness theorems of the constructors into "not-alphas" of the constructors *) fun mk_distinct_goal ty_trm_assoc neq = let val (Const (@{const_name "HOL.eq"}, ty_eq) $ lhs $ rhs) = HOLogic.dest_not (HOLogic.dest_Trueprop neq) val ty_str = fst (dest_Type (domain_type ty_eq)) in Const (lookup ty_trm_assoc ty_str, ty_eq) $ lhs $ rhs |> HOLogic.mk_not |> HOLogic.mk_Trueprop end fun distinct_tac ctxt cases_thms distinct_thms = resolve_tac ctxt [notI] THEN' eresolve_tac ctxt cases_thms THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps distinct_thms) fun raw_prove_alpha_distincts ctxt alpha_result raw_dt_info = let val AlphaResult {alpha_names, alpha_cases, ...} = alpha_result val RawDtInfo {raw_dt_names, raw_distinct_thms, ...} = raw_dt_info val ty_trm_assoc = raw_dt_names ~~ alpha_names fun mk_alpha_distinct raw_distinct_trm = let val goal = mk_distinct_goal ty_trm_assoc raw_distinct_trm in Goal.prove ctxt [] [] goal - (K (distinct_tac ctxt alpha_cases raw_distinct_thms 1)) + (fn {context = ctxt', ...} => distinct_tac ctxt' alpha_cases raw_distinct_thms 1) end in map (mk_alpha_distinct o Thm.prop_of) raw_distinct_thms end (** produces the alpha_eq_iff simplification rules **) (* in case a theorem is of the form (Rel Const Const), it will be rewritten to ((Rel Const = Const) = True) *) fun mk_simp_rule thm = case Thm.prop_of thm of \<^Const_>\Trueprop for \_ $ Const _ $ Const _\\ => thm RS @{thm eqTrueI} | _ => thm fun alpha_eq_iff_tac ctxt dist_inj intros elims = SOLVED' (asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps intros)) ORELSE' (resolve_tac ctxt @{thms iffI} THEN' RANGE [eresolve_tac ctxt elims THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps dist_inj), asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps intros)]) fun mk_alpha_eq_iff_goal thm = let val prop = Thm.prop_of thm; val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop); val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop); fun list_conj l = foldr1 HOLogic.mk_conj l; in if hyps = [] then HOLogic.mk_Trueprop concl else HOLogic.mk_Trueprop (HOLogic.mk_eq (concl, list_conj hyps)) end; fun raw_prove_alpha_eq_iff ctxt alpha_result raw_dt_info = let val AlphaResult {alpha_intros, alpha_cases, ...} = alpha_result val RawDtInfo {raw_distinct_thms, raw_inject_thms, ...} = raw_dt_info val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt; val goals = map mk_alpha_eq_iff_goal thms_imp; - val tac = alpha_eq_iff_tac ctxt (raw_distinct_thms @ raw_inject_thms) alpha_intros alpha_cases 1; - val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals; + fun tac goal_ctxt = + alpha_eq_iff_tac goal_ctxt (raw_distinct_thms @ raw_inject_thms) alpha_intros alpha_cases 1; + val thms = map (fn goal => Goal.prove ctxt' [] [] goal (tac o #context)) goals; in Variable.export ctxt' ctxt thms |> map mk_simp_rule end (** reflexivity proof for the alphas **) val exi_zero = @{lemma "P (0::perm) \ (\x. P x)" by auto} fun cases_tac intros ctxt = let val prod_simps = @{thms split_conv prod_alpha_def rel_prod_conv} val unbound_tac = REPEAT o (eresolve_tac ctxt @{thms conjE}) THEN' assume_tac ctxt val bound_tac = EVERY' [ resolve_tac ctxt [exi_zero], resolve_tac ctxt @{thms alpha_refl}, asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ] in resolve_tac ctxt intros THEN_ALL_NEW FIRST' [resolve_tac ctxt @{thms refl}, unbound_tac, bound_tac] end fun raw_prove_refl ctxt alpha_result raw_dt_induct = let val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_intros, ...} = alpha_result val props = map (fn (ty, c) => (ty, fn x => c $ x $ x)) ((alpha_tys ~~ alpha_trms) @ (alpha_bn_tys ~~ alpha_bn_trms)) in induct_prove alpha_tys props raw_dt_induct (cases_tac alpha_intros) ctxt end (** symmetry proof for the alphas **) val exi_neg = @{lemma "(\(p::perm). P p) \ (\q. P q \ Q (- q)) \ \p. Q p" by (erule exE, rule_tac x="-p" in exI, auto)} (* for premises that contain binders *) fun prem_bound_tac pred_names alpha_eqvt ctxt = let fun trans_prem_tac pred_names ctxt = SUBPROOF (fn {prems, context = ctxt', ...} => let val prems' = map (transform_prem1 ctxt' pred_names) prems in resolve_tac ctxt' prems' 1 end) ctxt val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def rel_prod_conv alphas} in EVERY' [ eresolve_tac ctxt [exi_neg], resolve_tac ctxt @{thms alpha_sym_eqvt}, asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps), eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' resolve_tac ctxt @{thms refl}, trans_prem_tac pred_names ctxt] end fun raw_prove_sym ctxt alpha_result alpha_eqvt = let val AlphaResult {alpha_names, alpha_trms, alpha_bn_names, alpha_bn_trms, alpha_intros, alpha_raw_induct, ...} = alpha_result val alpha_trms = alpha_trms @ alpha_bn_trms val alpha_names = alpha_names @ alpha_bn_names val props = map (fn t => fn (x, y) => t $ y $ x) alpha_trms fun tac ctxt = resolve_tac ctxt alpha_intros THEN_ALL_NEW FIRST' [assume_tac ctxt, resolve_tac ctxt @{thms sym} THEN' assume_tac ctxt, prem_bound_tac alpha_names alpha_eqvt ctxt] in alpha_prove alpha_trms (alpha_trms ~~ props) alpha_raw_induct tac ctxt end (** transitivity proof for alphas **) (* applies cases rules and resolves them with the last premise *) fun ecases_tac cases = Subgoal.FOCUS (fn {context = ctxt, prems, ...} => HEADGOAL (resolve_tac ctxt cases THEN' resolve_tac ctxt [List.last prems])) fun aatac pred_names = SUBPROOF (fn {context = ctxt, prems, ...} => HEADGOAL (resolve_tac ctxt (map (transform_prem1 ctxt pred_names) prems))) (* instantiates exI with the permutation p + q *) val perm_inst_tac = Subgoal.FOCUS (fn {context = ctxt, params, ...} => let val (p, q) = apply2 snd (last2 params) val pq_inst = foldl1 (uncurry Thm.apply) [@{cterm "plus::perm => perm => perm"}, p, q] val exi_inst = Thm.instantiate' [SOME (@{ctyp "perm"})] [NONE, SOME pq_inst] @{thm exI} in HEADGOAL (resolve_tac ctxt [exi_inst]) end) fun non_trivial_cases_tac pred_names intros alpha_eqvt ctxt = let val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def rel_prod_conv} in resolve_tac ctxt intros THEN_ALL_NEW (asm_simp_tac (put_simpset HOL_basic_ss ctxt) THEN' TRY o EVERY' (* if binders are present *) [ eresolve_tac ctxt @{thms exE}, eresolve_tac ctxt @{thms exE}, perm_inst_tac ctxt, resolve_tac ctxt @{thms alpha_trans_eqvt}, assume_tac ctxt, aatac pred_names ctxt, eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' resolve_tac ctxt @{thms refl}, asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ]) end fun prove_trans_tac alpha_result raw_dt_thms alpha_eqvt ctxt = let val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, alpha_cases, ...} = alpha_result val alpha_names = alpha_names @ alpha_bn_names fun all_cases ctxt = asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps raw_dt_thms) THEN' TRY o non_trivial_cases_tac alpha_names alpha_intros alpha_eqvt ctxt in EVERY' [ resolve_tac ctxt @{thms allI}, resolve_tac ctxt @{thms impI}, ecases_tac alpha_cases ctxt THEN_ALL_NEW all_cases ctxt ] end fun prep_trans_goal alpha_trm (arg1, arg2) = let val arg_ty = fastype_of arg1 val mid = alpha_trm $ arg2 $ (Bound 0) val rhs = alpha_trm $ arg1 $ (Bound 0) in HOLogic.all_const arg_ty $ Abs ("z", arg_ty, HOLogic.mk_imp (mid, rhs)) end fun raw_prove_trans ctxt alpha_result raw_dt_thms alpha_eqvt = let val AlphaResult {alpha_trms, alpha_bn_trms, alpha_raw_induct, ...} = alpha_result val alpha_trms = alpha_trms @ alpha_bn_trms val props = map prep_trans_goal alpha_trms in alpha_prove alpha_trms (alpha_trms ~~ props) alpha_raw_induct (prove_trans_tac alpha_result raw_dt_thms alpha_eqvt) ctxt end (** proves the equivp predicate for all alphas **) val reflp_def' = @{lemma "reflp R == \x. R x x" by (simp add: reflp_def refl_on_def)} val symp_def' = @{lemma "symp R \ \x y . R x y --> R y x" by (simp add: symp_def sym_def)} val transp_def' = @{lemma "transp R \ \x y. R x y \ (\z. R y z \ R x z)" by (rule eq_reflection, auto simp add: trans_def transp_def)} fun raw_prove_equivp ctxt alpha_result refl symm trans = let val AlphaResult {alpha_trms, alpha_bn_trms, ...} = alpha_result val refl' = map (fold_rule ctxt [reflp_def'] o atomize ctxt) refl val symm' = map (fold_rule ctxt [symp_def'] o atomize ctxt) symm val trans' = map (fold_rule ctxt [transp_def'] o atomize ctxt) trans fun prep_goal t = \<^Const>\Trueprop for \<^Const>\equivp \domain_type (fastype_of t)\ for t\\ in Goal.prove_common ctxt NONE [] [] (map prep_goal (alpha_trms @ alpha_bn_trms)) - (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (resolve_tac ctxt @{thms equivpI} THEN' - RANGE [resolve_tac ctxt refl', resolve_tac ctxt symm', resolve_tac ctxt trans'])))) + (fn {context = ctxt', ...} => + HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (resolve_tac ctxt' @{thms equivpI} THEN' + RANGE [resolve_tac ctxt' refl', resolve_tac ctxt' symm', resolve_tac ctxt' trans']))) |> chop (length alpha_trms) end (* proves that alpha_raw implies alpha_bn *) fun raw_prove_bn_imp_tac alpha_result ctxt = SUBPROOF (fn {prems, context = ctxt', ...} => let val AlphaResult {alpha_names, alpha_intros, ...} = alpha_result val prems' = flat (map Old_Datatype_Aux.split_conj_thm prems) val prems'' = map (transform_prem1 ctxt' alpha_names) prems' in HEADGOAL (REPEAT_ALL_NEW (FIRST' [ resolve_tac ctxt' @{thms TrueI}, resolve_tac ctxt' @{thms conjI}, resolve_tac ctxt' prems', resolve_tac ctxt' prems'', resolve_tac ctxt' alpha_intros ])) end) ctxt fun raw_prove_bn_imp ctxt alpha_result = let val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_raw_induct, ...} = alpha_result val arg_ty = domain_type o fastype_of val ty_assoc = alpha_tys ~~ alpha_trms val props = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => t $ x $ y)) alpha_bn_trms in alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_raw_induct (raw_prove_bn_imp_tac alpha_result) ctxt end (* respectfulness for fv_raw / bn_raw *) fun raw_fv_bn_rsp_aux ctxt alpha_result fvs bns fv_bns simps = let val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_raw_induct, ...} = alpha_result val arg_ty = domain_type o fastype_of val ty_assoc = alpha_tys ~~ alpha_trms fun mk_eq' t x y = HOLogic.mk_eq (t $ x, t $ y) val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) fvs val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) (bns @ fv_bns) val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => mk_eq' t2 x y)) alpha_bn_trms fv_bns val simpset = put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_fv.simps set_simps append.simps} @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) in alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_raw_induct (K (asm_full_simp_tac simpset)) ctxt end (* respectfulness for size *) fun raw_size_rsp_aux ctxt alpha_result simps = let val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_raw_induct, ...} = alpha_result fun mk_prop ty (x, y) = HOLogic.mk_eq (HOLogic.size_const ty $ x, HOLogic.size_const ty $ y) val props = (alpha_trms @ alpha_bn_trms) ~~ (map mk_prop (alpha_tys @ alpha_bn_tys)) val simpset = put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_alpha_def rel_prod_conv permute_prod_def prod.case prod.rec}) val tac = (TRY o REPEAT o eresolve_tac ctxt @{thms exE}) THEN' asm_full_simp_tac simpset in alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_raw_induct (K tac) ctxt end (* respectfulness for constructors *) fun raw_constr_rsp_tac ctxt alpha_intros simps = let val pre_simpset = put_simpset HOL_ss ctxt addsimps @{thms rel_fun_def} val post_simpset = put_simpset HOL_ss ctxt addsimps @{thms alphas prod_alpha_def rel_prod_conv prod_fv.simps fresh_star_zero permute_zero prod.case} @ simps in asm_full_simp_tac pre_simpset THEN' REPEAT o (resolve_tac ctxt @{thms allI impI}) THEN' resolve_tac ctxt alpha_intros THEN_ALL_NEW (TRY o (resolve_tac ctxt [exi_zero]) THEN' asm_full_simp_tac post_simpset) end fun raw_constrs_rsp ctxt alpha_result constrs simps = let val AlphaResult {alpha_trms, alpha_tys, alpha_intros, ...} = alpha_result fun lookup ty = case AList.lookup (op=) (alpha_tys ~~ alpha_trms) ty of NONE => HOLogic.eq_const ty | SOME alpha => alpha fun rel_fun_app (t1, t2) = Const (@{const_name "rel_fun"}, dummyT) $ t1 $ t2 fun prep_goal trm = trm |> strip_type o fastype_of |> (fn (tys, ty) => tys @ [ty]) |> map lookup |> foldr1 rel_fun_app |> (fn t => t $ trm $ trm) |> Syntax.check_term ctxt |> HOLogic.mk_Trueprop in map (fn constrs => Goal.prove_common ctxt NONE [] [] (map prep_goal constrs) - (K (HEADGOAL - (Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac ctxt alpha_intros simps)))) constrs + (fn {context = ctxt', ...} => + HEADGOAL + (Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac ctxt' alpha_intros simps))) constrs end (* rsp lemmas for alpha_bn relations *) val rsp_equivp = @{lemma "[|equivp Q; !!x y. R x y ==> Q x y|] ==> (R ===> R ===> (=)) Q Q" by (simp only: rel_fun_def equivp_def, metis)} (* we have to reorder the alpha_bn_imps theorems in order to be in order with alpha_bn_trms *) fun raw_alpha_bn_rsp alpha_result alpha_bn_equivp alpha_bn_imps = let val AlphaResult {alpha_bn_trms, ...} = alpha_result fun mk_map thm = thm |> `Thm.prop_of |>> List.last o snd o strip_comb |>> HOLogic.dest_Trueprop |>> head_of |>> fst o dest_Const val alpha_bn_imps' = map (lookup (map mk_map alpha_bn_imps) o fst o dest_Const) alpha_bn_trms fun mk_thm thm1 thm2 = (Thm.forall_intr_vars thm2) COMP (thm1 RS rsp_equivp) in map2 mk_thm alpha_bn_equivp alpha_bn_imps' end (* rsp for permute_bn functions *) val perm_bn_rsp = @{lemma "(\x y p. R x y \ R (f p x) (f p y)) \ ((=) ===> R ===> R) f f" by (simp add: rel_fun_def)} fun raw_prove_perm_bn_tac alpha_result simps ctxt = SUBPROOF (fn {prems, context = ctxt', ...} => let val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, ...} = alpha_result val prems' = flat (map Old_Datatype_Aux.split_conj_thm prems) val prems'' = map (transform_prem1 ctxt' (alpha_names @ alpha_bn_names)) prems' in HEADGOAL (simp_tac (put_simpset HOL_basic_ss ctxt' addsimps (simps @ prems')) THEN' TRY o REPEAT_ALL_NEW (FIRST' [ resolve_tac ctxt' @{thms TrueI}, resolve_tac ctxt' @{thms conjI}, resolve_tac ctxt' @{thms refl}, resolve_tac ctxt' prems', resolve_tac ctxt' prems'', resolve_tac ctxt' alpha_intros ])) end) ctxt fun raw_perm_bn_rsp ctxt alpha_result perm_bns simps = let val AlphaResult {alpha_trms, alpha_tys, alpha_bn_trms, alpha_bn_tys, alpha_raw_induct, ...} = alpha_result val perm_bn_ty = range_type o range_type o fastype_of val ty_assoc = (alpha_tys @ alpha_bn_tys) ~~ (alpha_trms @ alpha_bn_trms) val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt val p = Free (p, \<^Type>\perm\) fun mk_prop t = let val alpha_trm = lookup ty_assoc (perm_bn_ty t) in (alpha_trm, fn (x, y) => alpha_trm $ (t $ p $ x) $ (t $ p $ y)) end val goals = map mk_prop perm_bns in alpha_prove (alpha_trms @ alpha_bn_trms) goals alpha_raw_induct (raw_prove_perm_bn_tac alpha_result simps) ctxt |> Proof_Context.export ctxt' ctxt |> map (atomize ctxt) |> map single |> map (curry (op OF) perm_bn_rsp) end (* transformation of the natural rsp-lemmas into standard form *) val fun_rsp = @{lemma "(\x y. R x y \ f x = f y) \ (R ===> (=)) f f" by (simp add: rel_fun_def)} fun mk_funs_rsp ctxt thm = thm |> atomize ctxt |> single |> curry (op OF) fun_rsp val permute_rsp = @{lemma "(\x y p. R x y \ R (permute p x) (permute p y)) ==> ((=) ===> R ===> R) permute permute" by (simp add: rel_fun_def)} fun mk_alpha_permute_rsp ctxt thm = thm |> atomize ctxt |> single |> curry (op OF) permute_rsp end (* structure *) diff --git a/thys/Nominal2/nominal_dt_quot.ML b/thys/Nominal2/nominal_dt_quot.ML --- a/thys/Nominal2/nominal_dt_quot.ML +++ b/thys/Nominal2/nominal_dt_quot.ML @@ -1,751 +1,754 @@ (* Title: nominal_dt_alpha.ML Author: Christian Urban Author: Cezary Kaliszyk Performing quotient constructions, lifting theorems and deriving support properties for the quotient types. *) signature NOMINAL_DT_QUOT = sig val define_qtypes: (string list * binding * mixfix) list -> typ list -> term list -> thm list -> local_theory -> Quotient_Info.quotients list * local_theory val define_qconsts: typ list -> (string * term * mixfix * thm) list -> local_theory -> Quotient_Info.quotconsts list * local_theory val define_qperms: typ list -> string list -> (string * sort) list -> (string * term * mixfix * thm) list -> thm list -> local_theory -> local_theory val define_qsizes: typ list -> string list -> (string * sort) list -> (string * term * mixfix * thm) list -> local_theory -> local_theory val lift_thms: typ list -> thm list -> thm list -> Proof.context -> thm list * Proof.context val prove_supports: Proof.context -> thm list -> term list -> thm list val prove_fsupp: Proof.context -> typ list -> thm -> thm list -> thm list val fs_instance: typ list -> string list -> (string * sort) list -> thm list -> local_theory -> local_theory val prove_fv_supp: typ list -> term list -> term list -> term list -> term list -> thm list -> thm list -> thm list -> thm list -> thm -> bclause list list -> Proof.context -> thm list val prove_bns_finite: typ list -> term list -> thm -> thm list -> Proof.context -> thm list val prove_perm_bn_alpha_thms: typ list -> term list -> term list -> thm -> thm list -> thm list -> thm list -> Proof.context -> thm list val prove_permute_bn_thms: typ list -> term list -> term list -> thm -> thm list -> thm list -> thm list -> Proof.context -> thm list val prove_strong_exhausts: Proof.context -> thm list -> bclause list list list -> thm list -> thm list -> thm list -> thm list -> thm list -> thm list val prove_strong_induct: Proof.context -> thm -> thm list -> thm list -> bclause list list list -> thm list end structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = struct open Nominal_Permeq fun lookup xs x = the (AList.lookup (op=) xs x) (* defines the quotient types *) fun define_qtypes qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy = let val qty_args1 = map2 (fn ty => fn trm => (ty, trm, false)) alpha_tys alpha_trms val qty_args2 = map2 (fn descr => fn args1 => (descr, args1, (NONE, NONE))) qtys_descr qty_args1 val qty_args3 = qty_args2 ~~ alpha_equivp_thms in fold_map (Quotient_Type.add_quotient_type {overloaded = false}) qty_args3 lthy end (* a wrapper for lifting a raw constant *) fun lift_raw_const qtys (qconst_name, rconst, mx', rsp_thm) lthy = let val rty = fastype_of rconst val qty = Quotient_Term.derive_qtyp lthy qtys rty val lhs_raw = Free (qconst_name, qty) val rhs_raw = rconst val raw_var = (Binding.name qconst_name, NONE, mx') val ((binding, _, mx), ctxt) = Proof_Context.cert_var raw_var lthy val lhs = Syntax.check_term ctxt lhs_raw val rhs = Syntax.check_term ctxt rhs_raw val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined." val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction" val _ = if is_Const rhs then () else warning "The definiens is not a constant" in Quotient_Def.add_quotient_def (((binding, mx), Binding.empty_atts), (lhs, rhs)) rsp_thm ctxt end (* defines quotient constants *) fun define_qconsts qtys consts_specs lthy = let val (qconst_infos, lthy') = fold_map (lift_raw_const qtys) consts_specs lthy val phi = Proof_Context.export_morphism lthy' (Proof_Context.transfer (Proof_Context.theory_of lthy') lthy) in (map (Quotient_Info.transform_quotconsts phi) qconst_infos, lthy') end (* defines the quotient permutations and proves pt-class *) fun define_qperms qtys qfull_ty_names tvs perm_specs raw_perm_laws lthy = let val lthy1 = lthy |> Local_Theory.exit_global |> Class.instantiation (qfull_ty_names, tvs, @{sort pt}) val (_, lthy2) = define_qconsts qtys perm_specs lthy1 val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws lthy2 val lifted_perm_laws = map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws' |> Variable.exportT lthy3 lthy2 fun tac ctxt = Class.intro_classes_tac ctxt [] THEN (ALLGOALS (resolve_tac ctxt lifted_perm_laws)) in lthy2 |> Class.prove_instantiation_exit tac |> Named_Target.theory_init end (* defines the size functions and proves size-class *) fun define_qsizes qtys qfull_ty_names tvs size_specs lthy = let fun tac ctxt = Class.intro_classes_tac ctxt [] in lthy |> Local_Theory.exit_global |> Class.instantiation (qfull_ty_names, tvs, @{sort size}) |> snd o (define_qconsts qtys size_specs) |> Class.prove_instantiation_exit tac |> Named_Target.theory_init end (* lifts a theorem and cleans all "_raw" parts from variable names *) local val any = Scan.one (Symbol.not_eof) val raw = Scan.this_string "_raw" val exclude = Scan.repeat (Scan.unless raw any) --| raw >> implode val parser = Scan.repeat (exclude || any) in fun unraw_str s = s |> raw_explode |> Scan.finite Symbol.stopper parser >> implode |> fst end fun unraw_vars_thm ctxt thm = let fun unraw_var_str ((s, i), T) = ((unraw_str s, i), T) val vars = Term.add_vars (Thm.prop_of thm) [] val vars' = map (Thm.cterm_of ctxt o Var o unraw_var_str) vars in Thm.instantiate (TVars.empty, Vars.make (vars ~~ vars')) thm end fun unraw_bounds_thm th = let val trm = Thm.prop_of th val trm' = Term.map_abs_vars unraw_str trm in Thm.rename_boundvars trm trm' th end fun lift_thms qtys simps thms ctxt = (map (Quotient_Tacs.lifted ctxt qtys simps #> unraw_bounds_thm #> unraw_vars_thm ctxt #> Drule.zero_var_indexes) thms, ctxt) fun mk_supports_goal ctxt qtrm = let val vs = fresh_args ctxt qtrm val rhs = list_comb (qtrm, vs) val lhs = fold (curry HOLogic.mk_prod) vs @{term "()"} |> mk_supp in mk_supports lhs rhs |> HOLogic.mk_Trueprop end fun supports_tac ctxt perm_simps = let val simpset1 = put_simpset HOL_basic_ss ctxt addsimps @{thms supports_def fresh_def[symmetric]} val simpset2 = put_simpset HOL_ss ctxt addsimps @{thms swap_fresh_fresh fresh_Pair} in EVERY' [ simp_tac simpset1, eqvt_tac ctxt (eqvt_strict_config addpres perm_simps), simp_tac simpset2 ] end fun prove_supports_single ctxt perm_simps qtrm = let val goal = mk_supports_goal ctxt qtrm val ctxt' = Proof_Context.augment goal ctxt in Goal.prove ctxt' [] [] goal - (K (HEADGOAL (supports_tac ctxt perm_simps))) + (fn {context = goal_ctxt, ...} => HEADGOAL (supports_tac goal_ctxt perm_simps)) |> singleton (Proof_Context.export ctxt' ctxt) end fun prove_supports ctxt perm_simps qtrms = map (prove_supports_single ctxt perm_simps) qtrms (* finite supp lemmas for qtypes *) fun prove_fsupp ctxt qtys qinduct qsupports_thms = let val (vs, ctxt') = Variable.variant_fixes (replicate (length qtys) "x") ctxt val goals = vs ~~ qtys |> map Free |> map (mk_finite o mk_supp) |> foldr1 (HOLogic.mk_conj) |> HOLogic.mk_Trueprop val tac = EVERY' [ resolve_tac ctxt' @{thms supports_finite}, resolve_tac ctxt' qsupports_thms, asm_simp_tac (put_simpset HOL_ss ctxt' addsimps @{thms finite_supp supp_Pair finite_Un}) ] in Goal.prove ctxt' [] [] goals - (K (HEADGOAL (resolve_tac ctxt' [qinduct] THEN_ALL_NEW tac))) + (fn {context = goal_ctxt, ...} => + HEADGOAL (resolve_tac goal_ctxt [qinduct] THEN_ALL_NEW tac)) |> singleton (Proof_Context.export ctxt' ctxt) |> Old_Datatype_Aux.split_conj_thm |> map zero_var_indexes end (* finite supp instances *) fun fs_instance qtys qfull_ty_names tvs qfsupp_thms lthy = let val lthy1 = lthy |> Local_Theory.exit_global |> Class.instantiation (qfull_ty_names, tvs, @{sort fs}) fun tac ctxt = Class.intro_classes_tac ctxt [] THEN (ALLGOALS (resolve_tac ctxt qfsupp_thms)) in lthy1 |> Class.prove_instantiation_exit tac |> Named_Target.theory_init end (* proves that fv and fv_bn equals supp *) fun gen_mk_goals fv supp = let val arg_ty = fastype_of fv |> domain_type in (arg_ty, fn x => HOLogic.mk_eq (fv $ x, supp x)) end fun mk_fvs_goals fv = gen_mk_goals fv mk_supp fun mk_fv_bns_goals fv_bn alpha_bn = gen_mk_goals fv_bn (mk_supp_rel alpha_bn) fun add_simpset ctxt thms = put_simpset HOL_basic_ss ctxt addsimps thms fun symmetric thms = map (fn thm => thm RS @{thm sym}) thms val supp_Abs_set = @{thms supp_Abs(1)[symmetric]} val supp_Abs_res = @{thms supp_Abs(2)[symmetric]} val supp_Abs_lst = @{thms supp_Abs(3)[symmetric]} fun mk_supp_abs ctxt (BC (Set, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_set | mk_supp_abs ctxt (BC (Res, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_res | mk_supp_abs ctxt (BC (Lst, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_lst fun mk_supp_abs_tac ctxt [] = [] | mk_supp_abs_tac ctxt (BC (_, [], _)::xs) = mk_supp_abs_tac ctxt xs | mk_supp_abs_tac ctxt (bc::xs) = (DETERM o mk_supp_abs ctxt bc)::mk_supp_abs_tac ctxt xs fun mk_bn_supp_abs_tac ctxt trm = trm |> fastype_of |> body_type |> (fn ty => case ty of @{typ "atom set"} => simp_tac (add_simpset ctxt supp_Abs_set) | @{typ "atom list"} => simp_tac (add_simpset ctxt supp_Abs_lst) | _ => raise TERM ("mk_bn_supp_abs_tac", [trm])) val thms1 = @{thms supp_Pair supp_eqvt[symmetric] Un_assoc conj_assoc} val thms2 = @{thms de_Morgan_conj Collect_disj_eq finite_Un} val thms3 = @{thms alphas prod_alpha_def prod_fv.simps rel_prod_conv permute_prod_def prod.rec prod.case prod.inject not_True_eq_False empty_def[symmetric] finite.emptyI} fun prove_fv_supp qtys qtrms fvs fv_bns alpha_bns fv_simps eq_iffs perm_simps fv_bn_eqvts qinduct bclausess ctxt = let val goals1 = map mk_fvs_goals fvs val goals2 = map2 mk_fv_bns_goals fv_bns alpha_bns fun tac ctxt = SUBGOAL (fn (goal, i) => let val (fv_fun, arg) = goal |> Envir.eta_contract |> Logic.strip_assums_concl |> HOLogic.dest_Trueprop |> fst o HOLogic.dest_eq |> dest_comb val supp_abs_tac = case (AList.lookup (op=) (qtrms ~~ bclausess) (head_of arg)) of SOME bclauses => EVERY' (mk_supp_abs_tac ctxt bclauses) | NONE => mk_bn_supp_abs_tac ctxt fv_fun val eqvt_rconfig = eqvt_relaxed_config addpres (perm_simps @ fv_bn_eqvts) in EVERY' [ TRY o asm_full_simp_tac (add_simpset ctxt (@{thm supp_Pair[symmetric]}::fv_simps)), TRY o supp_abs_tac, TRY o simp_tac (add_simpset ctxt @{thms supp_def supp_rel_def}), TRY o eqvt_tac ctxt eqvt_rconfig, TRY o simp_tac (add_simpset ctxt (@{thms Abs_eq_iff} @ eq_iffs)), TRY o asm_full_simp_tac (add_simpset ctxt thms3), TRY o simp_tac (add_simpset ctxt thms2), TRY o asm_full_simp_tac (add_simpset ctxt (thms1 @ (symmetric fv_bn_eqvts)))] i end) in induct_prove qtys (goals1 @ goals2) qinduct tac ctxt |> map (atomize ctxt) |> map (simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms fun_eq_iff[symmetric]})) end fun prove_bns_finite qtys qbns qinduct qbn_simps ctxt = let fun mk_goal qbn = let val arg_ty = domain_type (fastype_of qbn) val finite = @{term "finite :: atom set => bool"} in (arg_ty, fn x => finite $ (to_set (qbn $ x))) end val props = map mk_goal qbns val ss_tac = asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps (qbn_simps @ @{thms set_simps set_append finite_insert finite.emptyI finite_Un})) in induct_prove qtys props qinduct (K ss_tac) ctxt end fun prove_perm_bn_alpha_thms qtys qperm_bns alpha_bns qinduct qperm_bn_simps qeq_iffs qalpha_refls ctxt = let val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt val p = Free (p, \<^Type>\perm\) fun mk_goal qperm_bn alpha_bn = let val arg_ty = domain_type (fastype_of alpha_bn) in (arg_ty, fn x => (mk_id (Abs ("", arg_ty, alpha_bn $ Bound 0 $ (qperm_bn $ p $ Bound 0)))) $ x) end val props = map2 mk_goal qperm_bns alpha_bns val ss = @{thm id_def}::qperm_bn_simps @ qeq_iffs @ qalpha_refls val ss_tac = asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps ss) in induct_prove qtys props qinduct (K ss_tac) ctxt' |> Proof_Context.export ctxt' ctxt |> map (simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms id_def})) end fun prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qbn_eqvts ctxt = let val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt val p = Free (p, \<^Type>\perm\) fun mk_goal qbn qperm_bn = let val arg_ty = domain_type (fastype_of qbn) in (arg_ty, fn x => (mk_id (Abs ("", arg_ty, HOLogic.mk_eq (mk_perm p (qbn $ Bound 0), qbn $ (qperm_bn $ p $ Bound 0)))) $ x)) end val props = map2 mk_goal qbns qperm_bns val ss = @{thm id_def}::qperm_bn_simps @ qbn_defs val ss_tac = EVERY' [asm_full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps ss), TRY o eqvt_tac ctxt' (eqvt_strict_config addpres qbn_eqvts), TRY o asm_full_simp_tac (put_simpset HOL_basic_ss ctxt')] in induct_prove qtys props qinduct (K ss_tac) ctxt' |> Proof_Context.export ctxt' ctxt |> map (simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms id_def})) end (*** proves strong exhauts theorems ***) (* fixme: move into nominal_library *) fun abs_const bmode ty = let val (const_name, binder_ty, abs_ty) = case bmode of Lst => (@{const_name "Abs_lst"}, @{typ "atom list"}, @{type_name abs_lst}) | Set => (@{const_name "Abs_set"}, @{typ "atom set"}, @{type_name abs_set}) | Res => (@{const_name "Abs_res"}, @{typ "atom set"}, @{type_name abs_res}) in Const (const_name, [binder_ty, ty] ---> Type (abs_ty, [ty])) end fun mk_abs bmode trm1 trm2 = abs_const bmode (fastype_of trm2) $ trm1 $ trm2 fun is_abs_eq thm = let fun is_abs trm = case head_of trm of \<^Const_>\Abs_set _\ => true | \<^Const_>\Abs_lst _\ => true | \<^Const_>\Abs_res _\ => true | _ => false in thm |> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst |> is_abs end (* adds a freshness condition to the assumptions *) fun mk_ecase_prems lthy c (params, prems, concl) bclauses = let val tys = map snd params val binders = get_all_binders bclauses fun prep_binder (opt, i) = let val t = Bound (length tys - i - 1) in case opt of NONE => setify_ty lthy (nth tys i) t | SOME bn => to_set_ty (fastype_of1 (tys, bn $ t)) (bn $ t) end val prems' = case binders of [] => prems (* case: no binders *) | _ => binders (* case: binders *) |> map prep_binder |> fold_union_env tys |> (fn t => mk_fresh_star t c) |> (fn t => HOLogic.mk_Trueprop t :: prems) in mk_full_horn params prems' concl end (* derives the freshness theorem that there exists a p, such that (p o as) #* (c, t1,..., tn) *) fun fresh_thm ctxt c parms binders bn_finite_thms = let fun prep_binder (opt, i) = case opt of NONE => setify ctxt (nth parms i) | SOME bn => to_set (bn $ (nth parms i)) fun prep_binder2 (opt, i) = case opt of NONE => atomify ctxt (nth parms i) | SOME bn => bn $ (nth parms i) val rhs = HOLogic.mk_tuple ([c] @ parms @ (map prep_binder2 binders)) val lhs = binders |> map prep_binder |> fold_union |> mk_perm (Bound 0) val goal = mk_fresh_star lhs rhs |> mk_exists ("p", \<^Type>\perm\) |> HOLogic.mk_Trueprop val ss = bn_finite_thms @ @{thms supp_Pair finite_supp finite_sets_supp} @ @{thms finite.intros finite_Un finite_set finite_fset} in Goal.prove ctxt [] [] goal - (K (HEADGOAL (resolve_tac ctxt @{thms at_set_avoiding1} - THEN_ALL_NEW (simp_tac (put_simpset HOL_ss ctxt addsimps ss))))) + (fn {context = ctxt', ...} => + HEADGOAL (resolve_tac ctxt' @{thms at_set_avoiding1} + THEN_ALL_NEW (simp_tac (put_simpset HOL_ss ctxt' addsimps ss)))) end (* derives an abs_eq theorem of the form Exists q. [as].x = [p o as].(q o x) for non-recursive binders Exists q. [as].x = [q o as].(q o x) for recursive binders *) fun abs_eq_thm ctxt fprops p parms bn_eqvt permute_bns (bclause as (BC (bmode, binders, bodies))) = case binders of [] => [] | _ => let val rec_flag = is_recursive_binder bclause val binder_trm = comb_binders ctxt bmode parms binders val body_trm = foldl1 HOLogic.mk_prod (map (nth parms) bodies) val abs_lhs = mk_abs bmode binder_trm body_trm val abs_rhs = if rec_flag then mk_abs bmode (mk_perm (Bound 0) binder_trm) (mk_perm (Bound 0) body_trm) else mk_abs bmode (mk_perm p binder_trm) (mk_perm (Bound 0) body_trm) val abs_eq = HOLogic.mk_eq (abs_lhs, abs_rhs) val peq = HOLogic.mk_eq (mk_perm (Bound 0) binder_trm, mk_perm p binder_trm) val goal = HOLogic.mk_conj (abs_eq, peq) |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t)) |> HOLogic.mk_Trueprop val ss = fprops @ @{thms set_simps set_append union_eqvt} @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset fresh_star_set} - val tac1 = + fun tac1 ctxt' = if rec_flag - then resolve_tac ctxt @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'} - else resolve_tac ctxt @{thms Abs_rename_set Abs_rename_res Abs_rename_lst} + then resolve_tac ctxt' @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'} + else resolve_tac ctxt' @{thms Abs_rename_set Abs_rename_res Abs_rename_lst} - val tac2 = - EVERY' [simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss), - TRY o simp_tac (put_simpset HOL_ss ctxt)] + fun tac2 ctxt' = + EVERY' [simp_tac (put_simpset HOL_basic_ss ctxt' addsimps ss), + TRY o simp_tac (put_simpset HOL_ss ctxt')] in - [ Goal.prove ctxt [] [] goal (K (HEADGOAL (tac1 THEN_ALL_NEW tac2))) + [ Goal.prove ctxt [] [] goal (fn {context = ctxt', ...} => + HEADGOAL (tac1 ctxt' THEN_ALL_NEW tac2 ctxt')) |> (if rec_flag then eqvt_rule ctxt (eqvt_strict_config addpres bn_eqvt) else eqvt_rule ctxt (eqvt_strict_config addpres permute_bns)) ] end val setify = @{lemma "xs = ys ==> set xs = set ys" by simp} -fun case_tac ctxt c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas +fun case_tac goal_ctxt c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas prems bclausess qexhaust_thm = let fun aux_tac prem bclauses = case (get_all_binders bclauses) of - [] => EVERY' [resolve_tac ctxt [prem], assume_tac ctxt] - | binders => Subgoal.SUBPROOF (fn {params, prems, concl, context = ctxt, ...} => + [] => EVERY' [resolve_tac goal_ctxt [prem], assume_tac goal_ctxt] + | binders => Subgoal.SUBPROOF (fn {params, prems, concl, context = goal_ctxt1, ...} => let val parms = map (Thm.term_of o snd) params - val fthm = fresh_thm ctxt c parms binders bn_finite_thms + val fthm = fresh_thm goal_ctxt1 c parms binders bn_finite_thms val ss = @{thms fresh_star_Pair union_eqvt fresh_star_Un} val (([(_, fperm)], fprops), ctxt') = Obtain.result - (fn ctxt' => EVERY1 [eresolve_tac ctxt [exE], - full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps ss), - REPEAT o (eresolve_tac ctxt @{thms conjE})]) [fthm] ctxt + (fn goal_ctxt2 => + EVERY1 [eresolve_tac goal_ctxt2 [exE], + full_simp_tac (put_simpset HOL_basic_ss goal_ctxt2 addsimps ss), + REPEAT o (eresolve_tac goal_ctxt2 @{thms conjE})]) [fthm] goal_ctxt1 val abs_eq_thms = flat (map (abs_eq_thm ctxt' fprops (Thm.term_of fperm) parms bn_eqvt permute_bns) bclauses) val ((_, eqs), ctxt'') = Obtain.result - (fn ctxt'' => EVERY1 - [ REPEAT o (eresolve_tac ctxt @{thms exE}), - REPEAT o (eresolve_tac ctxt @{thms conjE}), - REPEAT o (dresolve_tac ctxt [setify]), - full_simp_tac (put_simpset HOL_basic_ss ctxt'' + (fn goal_ctxt3 => EVERY1 + [ REPEAT o (eresolve_tac goal_ctxt3 @{thms exE}), + REPEAT o (eresolve_tac goal_ctxt3 @{thms conjE}), + REPEAT o (dresolve_tac goal_ctxt3 [setify]), + full_simp_tac (put_simpset HOL_basic_ss goal_ctxt3 addsimps @{thms set_append set_simps})]) abs_eq_thms ctxt' val (abs_eqs, peqs) = split_filter is_abs_eq eqs val fprops' = map (eqvt_rule ctxt'' (eqvt_strict_config addpres permute_bns)) fprops @ map (eqvt_rule ctxt'' (eqvt_strict_config addpres bn_eqvt)) fprops (* for freshness conditions *) - val tac1 = SOLVED' (EVERY' - [ simp_tac (put_simpset HOL_basic_ss ctxt'' addsimps peqs), - rewrite_goal_tac ctxt'' (@{thms fresh_star_Un[THEN eq_reflection]}), - conj_tac ctxt'' (DETERM o resolve_tac ctxt'' fprops') ]) + fun tac1 ctxt = SOLVED' (EVERY' + [ simp_tac (put_simpset HOL_basic_ss ctxt addsimps peqs), + rewrite_goal_tac ctxt (@{thms fresh_star_Un[THEN eq_reflection]}), + conj_tac ctxt (DETERM o resolve_tac ctxt fprops') ]) (* for equalities between constructors *) - val tac2 = SOLVED' (EVERY' + fun tac2 ctxt = SOLVED' (EVERY' [ resolve_tac ctxt [@{thm ssubst} OF prems], - rewrite_goal_tac ctxt'' (map safe_mk_equiv eq_iff_thms), - rewrite_goal_tac ctxt'' (map safe_mk_equiv abs_eqs), - conj_tac ctxt'' (DETERM o resolve_tac ctxt'' (@{thms refl} @ perm_bn_alphas)) ]) + rewrite_goal_tac ctxt (map safe_mk_equiv eq_iff_thms), + rewrite_goal_tac ctxt (map safe_mk_equiv abs_eqs), + conj_tac ctxt (DETERM o resolve_tac ctxt (@{thms refl} @ perm_bn_alphas)) ]) (* proves goal "P" *) val side_thm = Goal.prove ctxt'' [] [] (Thm.term_of concl) - (K (EVERY1 [ resolve_tac ctxt'' [prem], RANGE [tac1, tac2] ])) - |> singleton (Proof_Context.export ctxt'' ctxt) + (fn {context = goal_ctxt4, ...} => + EVERY1 [ resolve_tac goal_ctxt4 [prem], RANGE [tac1 goal_ctxt4, tac2 goal_ctxt4]]) + |> singleton (Proof_Context.export ctxt'' goal_ctxt1) in - resolve_tac ctxt [side_thm] 1 - end) ctxt + resolve_tac goal_ctxt1 [side_thm] 1 + end) goal_ctxt in - EVERY1 [resolve_tac ctxt [qexhaust_thm], RANGE (map2 aux_tac prems bclausess)] + EVERY1 [resolve_tac goal_ctxt [qexhaust_thm], RANGE (map2 aux_tac prems bclausess)] end fun prove_strong_exhausts lthy exhausts bclausesss bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas = let val ((_, exhausts'), lthy') = Variable.import true exhausts lthy val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy' val c = Free (c, TFree (a, @{sort fs})) val (ecases, main_concls) = exhausts' (* ecases are of the form (params, prems, concl) *) |> map Thm.prop_of |> map Logic.strip_horn |> split_list val ecases' = (map o map) strip_full_horn ecases val premss = (map2 o map2) (mk_ecase_prems lthy'' c) ecases' bclausesss - fun tac bclausess exhaust {prems, context} = - case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas - prems bclausess exhaust - fun prove prems bclausess exhaust concl = - Goal.prove lthy'' [] prems concl (tac bclausess exhaust) + Goal.prove lthy'' [] prems concl (fn {prems, context = goal_ctxt} => + case_tac goal_ctxt c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas + prems bclausess exhaust) in map4 prove premss bclausesss exhausts' main_concls |> Proof_Context.export lthy'' lthy end (** strong induction theorems **) fun add_c_prop c c_ty trm = let val (P, arg) = dest_comb trm val (P_name, P_ty) = dest_Free P val (ty_args, bool) = strip_type P_ty in Free (P_name, (c_ty :: ty_args) ---> bool) $ c $ arg end fun add_qnt_c_prop c_name c_ty trm = trm |> HOLogic.dest_Trueprop |> incr_boundvars 1 |> add_c_prop (Bound 0) c_ty |> HOLogic.mk_Trueprop |> mk_all (c_name, c_ty) fun prep_prem lthy c c_name c_ty bclauses (params, prems, concl) = let val tys = map snd params val binders = get_all_binders bclauses fun prep_binder (opt, i) = let val t = Bound (length tys - i - 1) in case opt of NONE => setify_ty lthy (nth tys i) t | SOME bn => to_set_ty (fastype_of1 (tys, bn $ t)) (bn $ t) end val prems' = prems |> map (incr_boundvars 1) |> map (add_qnt_c_prop c_name c_ty) val prems'' = case binders of [] => prems' (* case: no binders *) | _ => binders (* case: binders *) |> map prep_binder |> fold_union_env tys |> incr_boundvars 1 |> (fn t => mk_fresh_star_ty c_ty t (Bound 0)) |> (fn t => HOLogic.mk_Trueprop t :: prems') val concl' = concl |> HOLogic.dest_Trueprop |> incr_boundvars 1 |> add_c_prop (Bound 0) c_ty |> HOLogic.mk_Trueprop in mk_full_horn (params @ [(c_name, c_ty)]) prems'' concl' end fun prove_strong_induct lthy induct exhausts size_thms bclausesss = let - val ((_, [induct']), lthy') = Variable.import true [induct] lthy + val ((_, [induct']), ctxt') = Variable.import true [induct] lthy - val ([c_name, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy' + val ([c_name, a], ctxt'') = Variable.variant_fixes ["c", "'a"] ctxt' val c_ty = TFree (a, @{sort fs}) val c = Free (c_name, c_ty) val (prems, concl) = induct' |> Thm.prop_of |> Logic.strip_horn val concls = concl |> HOLogic.dest_Trueprop |> HOLogic.dest_conj |> map (add_c_prop c c_ty) |> map HOLogic.mk_Trueprop val prems' = prems |> map strip_full_horn - |> map2 (prep_prem lthy'' c c_name c_ty) (flat bclausesss) + |> map2 (prep_prem ctxt'' c c_name c_ty) (flat bclausesss) - fun pat_tac ctxt thm = - Subgoal.FOCUS (fn {params, context = ctxt', ...} => + fun pat_tac goal_ctxt thm = + Subgoal.FOCUS (fn {params, context = goal_ctxt1, ...} => let val ty_parms = map (fn (_, ct) => (fastype_of (Thm.term_of ct), ct)) params val vs = Term.add_vars (Thm.prop_of thm) [] val vs_tys = map (Type.legacy_freeze_type o snd) vs val assigns = map (lookup ty_parms) vs_tys - val thm' = infer_instantiate ctxt' (map #1 vs ~~ assigns) thm + val thm' = infer_instantiate goal_ctxt1 (map #1 vs ~~ assigns) thm in - resolve_tac ctxt' [thm'] 1 - end) ctxt - THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_basic_ss ctxt) + resolve_tac goal_ctxt1 [thm'] 1 + end) goal_ctxt + THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_basic_ss goal_ctxt) fun size_simp_tac ctxt = simp_tac (put_simpset size_ss ctxt addsimps (@{thms comp_def snd_conv} @ size_thms)) in - Goal.prove_common lthy'' NONE [] prems' concls - (fn {prems, context = ctxt} => - Induction_Schema.induction_schema_tac ctxt prems - THEN RANGE (map (pat_tac ctxt) exhausts) 1 - THEN prove_termination_ind ctxt 1 - THEN ALLGOALS (size_simp_tac ctxt)) - |> Proof_Context.export lthy'' lthy + Goal.prove_common ctxt'' NONE [] prems' concls + (fn {prems, context = goal_ctxt} => + Induction_Schema.induction_schema_tac goal_ctxt prems + THEN RANGE (map (pat_tac goal_ctxt) exhausts) 1 + THEN prove_termination_ind goal_ctxt 1 + THEN ALLGOALS (size_simp_tac goal_ctxt)) + |> Proof_Context.export ctxt'' lthy end end (* structure *) diff --git a/thys/Nominal2/nominal_dt_rawfuns.ML b/thys/Nominal2/nominal_dt_rawfuns.ML --- a/thys/Nominal2/nominal_dt_rawfuns.ML +++ b/thys/Nominal2/nominal_dt_rawfuns.ML @@ -1,557 +1,557 @@ (* Title: nominal_dt_rawfuns.ML Author: Cezary Kaliszyk Author: Christian Urban Definitions of the raw fv, fv_bn and permute functions. *) signature NOMINAL_DT_RAWFUNS = sig val get_all_binders: bclause list -> (term option * int) list val is_recursive_binder: bclause -> bool val define_raw_bns: raw_dt_info -> (binding * typ option * mixfix) list -> Specification.multi_specs -> local_theory -> (term list * thm list * bn_info list * thm list * local_theory) val define_raw_fvs: raw_dt_info -> bn_info list -> bclause list list list -> Proof.context -> term list * term list * thm list * thm list * local_theory val define_raw_bn_perms: raw_dt_info -> bn_info list -> local_theory -> (term list * thm list * local_theory) val define_raw_perms: raw_dt_info -> local_theory -> (term list * thm list * thm list) * local_theory val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm list end structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS = struct open Nominal_Permeq fun get_all_binders bclauses = bclauses |> map (fn (BC (_, binders, _)) => binders) |> flat |> remove_dups (op =) fun is_recursive_binder (BC (_, binders, bodies)) = case (inter (op =) (map snd binders) bodies) of nil => false | _ => true fun lookup xs x = the (AList.lookup (op=) xs x) (** functions that define the raw binding functions **) (* strip_bn_fun takes a rhs of a bn function: this can only contain unions or appends of elements; in case of recursive calls it returns also the applied bn function *) fun strip_bn_fun ctxt args t = let fun aux t = case t of \<^Const_>\sup _ for l r\ => aux l @ aux r | \<^Const_>\append _ for l r\ => aux l @ aux r | \<^Const_>\insert _ for \<^Const_>\atom _ for \x as Var _\\ y\ => (find_index (equal x) args, NONE) :: aux y | \<^Const>\Cons _ for \<^Const_>\atom _ for \x as Var _\\ y\ => (find_index (equal x) args, NONE) :: aux y | \<^Const_>\bot _\ => [] | \<^Const_>\Nil _\ => [] | (f as Const _) $ (x as Var _) => [(find_index (equal x) args, SOME f)] | _ => error ("Unsupported binding function: " ^ (Syntax.string_of_term ctxt t)) in aux t end (** definition of the raw binding functions **) fun prep_bn_info ctxt dt_names dts bn_funs eqs = let fun process_eq eq = let val (lhs, rhs) = eq |> HOLogic.dest_Trueprop |> HOLogic.dest_eq val (bn_fun, [cnstr]) = strip_comb lhs val (_, ty) = dest_Const bn_fun val (ty_name, _) = dest_Type (domain_type ty) val dt_index = find_index (fn x => x = ty_name) dt_names val (cnstr_head, cnstr_args) = strip_comb cnstr val cnstr_name = Long_Name.base_name (fst (dest_Const cnstr_head)) val rhs_elements = strip_bn_fun ctxt cnstr_args rhs in ((bn_fun, dt_index), (cnstr_name, rhs_elements)) end (* order according to constructor names *) fun cntrs_order ((bn, dt_index), data) = let val dt = nth dts dt_index val cts = snd dt val ct_names = map (Binding.name_of o (fn (x, _, _) => x)) cts in (bn, (bn, dt_index, order (op=) ct_names data)) end in eqs |> map process_eq |> AList.group (op=) (* eqs grouped according to bn_functions *) |> map cntrs_order (* inner data ordered according to constructors *) |> order (op=) bn_funs (* ordered according to bn_functions *) end fun define_raw_bns raw_dt_info raw_bn_funs raw_bn_eqs lthy = if null raw_bn_funs then ([], [], [], [], lthy) else let val RawDtInfo {raw_dt_names, raw_dts, raw_inject_thms, raw_distinct_thms, raw_size_thms, ...} = raw_dt_info val lthy1 = lthy |> Local_Theory.begin_nested |> snd |> Function.add_function raw_bn_funs raw_bn_eqs Function_Common.default_config (pat_completeness_simp (raw_inject_thms @ raw_distinct_thms)) |> snd |> Local_Theory.end_nested; val ({fs, simps, inducts, ...}, lthy2) = prove_termination_fun raw_size_thms lthy1 val raw_bn_induct = the inducts val raw_bn_eqs = the simps val raw_bn_info = prep_bn_info lthy raw_dt_names raw_dts fs (map Thm.prop_of raw_bn_eqs) in (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy2) end (** functions that construct the equations for fv and fv_bn **) fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (bmode, binders, bodies)) = let fun mk_fv_body i = let val arg = nth args i val ty = fastype_of arg in case AList.lookup (op=) fv_map ty of NONE => mk_supp arg | SOME fv => fv $ arg end fun bind_set (NONE, i) = (setify lthy (nth args i), @{term "{}::atom set"}) | bind_set (SOME bn, i) = (bn $ (nth args i), if member (op=) bodies i then @{term "{}::atom set"} else lookup fv_bn_map bn $ (nth args i)) fun bind_lst (NONE, i) = (listify lthy (nth args i), @{term "[]::atom list"}) | bind_lst (SOME bn, i) = (bn $ (nth args i), if member (op=) bodies i then @{term "[]::atom list"} else lookup fv_bn_map bn $ (nth args i)) val (combine_fn, bind_fn) = case bmode of Lst => (fold_append, bind_lst) | Set => (fold_union, bind_set) | Res => (fold_union, bind_set) val t1 = map mk_fv_body bodies val (t2, t3) = binders |> map bind_fn |> split_list |> apply2 combine_fn in mk_union (mk_diff (fold_union t1, to_set t2), to_set t3) end (* in case of fv_bn we have to treat the case special, where an "empty" binding clause is given *) fun mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause = let fun mk_fv_bn_body i = let val arg = nth args i val ty = fastype_of arg in case AList.lookup (op=) bn_args i of NONE => (case (AList.lookup (op=) fv_map ty) of NONE => mk_supp arg | SOME fv => fv $ arg) | SOME (NONE) => @{term "{}::atom set"} | SOME (SOME bn) => lookup fv_bn_map bn $ arg end in case bclause of BC (_, [], bodies) => fold_union (map mk_fv_bn_body bodies) | _ => mk_fv_rhs lthy fv_map fv_bn_map args bclause end fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys, _) bclauses = let val arg_names = Old_Datatype_Prop.make_tnames arg_tys val args = map Free (arg_names ~~ arg_tys) val fv = lookup fv_map ty val lhs = fv $ list_comb (constr, args) val rhs_trms = map (mk_fv_rhs lthy fv_map fv_bn_map args) bclauses val rhs = fold_union rhs_trms in HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) end fun mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys, _)) bclauses = let val arg_names = Old_Datatype_Prop.make_tnames arg_tys val args = map Free (arg_names ~~ arg_tys) val fv_bn = lookup fv_bn_map bn_trm val lhs = fv_bn $ list_comb (constr, args) val rhs_trms = map (mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args) bclauses val rhs = fold_union rhs_trms in HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) end fun mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss (bn_trm, bn_n, bn_argss) = let val nth_constrs_info = nth constrs_info bn_n val nth_bclausess = nth bclausesss bn_n in map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess end fun define_raw_fvs raw_dt_info bn_info bclausesss lthy = let val RawDtInfo {raw_dt_names, raw_tys, raw_cns_info, raw_inject_thms, raw_distinct_thms, raw_size_thms, ...} = raw_dt_info val fv_names = map (prefix "fv_" o Long_Name.base_name) raw_dt_names val fv_tys = map (fn ty => ty --> @{typ "atom set"}) raw_tys val fv_frees = map Free (fv_names ~~ fv_tys); val fv_map = raw_tys ~~ fv_frees val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info) val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns val fv_bn_names = map (prefix "fv_") bn_names val fv_bn_arg_tys = map (nth raw_tys) bn_tys val fv_bn_tys = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys val fv_bn_frees = map Free (fv_bn_names ~~ fv_bn_tys) val fv_bn_map = bns ~~ fv_bn_frees val fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) raw_cns_info bclausesss val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map raw_cns_info bclausesss) bn_info val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) val all_fun_eqs = map (fn t => ((Binding.empty_atts, t), [], [])) (flat fv_eqs @ flat fv_bn_eqs) val lthy' = lthy |> Local_Theory.begin_nested |> snd |> Function.add_function all_fun_names all_fun_eqs Function_Common.default_config (pat_completeness_simp (raw_inject_thms @ raw_distinct_thms)) |> snd |> Local_Theory.end_nested; val ({fs, simps, inducts, ...}, lthy'') = prove_termination_fun raw_size_thms lthy' val morphism = Proof_Context.export_morphism lthy'' (Proof_Context.transfer (Proof_Context.theory_of lthy'') lthy) val simps_exp = map (Morphism.thm morphism) (the simps) val inducts_exp = map (Morphism.thm morphism) (the inducts) val (fvs', fv_bns') = chop (length fv_frees) fs (* grafting the types so that they coincide with the input into the function package *) val fvs'' = map2 (fn t => fn ty => Const (fst (dest_Const t), ty) ) fvs' fv_tys val fv_bns'' = map2 (fn t => fn ty => Const (fst (dest_Const t), ty) ) fv_bns' fv_bn_tys in (fvs'', fv_bns'', simps_exp, inducts_exp, lthy'') end (** definition of raw permute_bn functions **) fun mk_perm_bn_eq_rhs p perm_bn_map bn_args (i, arg) = case AList.lookup (op=) bn_args i of NONE => arg | SOME (NONE) => mk_perm p arg | SOME (SOME bn) => (lookup perm_bn_map bn) $ p $ arg fun mk_perm_bn_eq lthy bn_trm perm_bn_map bn_args (constr, _, arg_tys, _) = let val p = Free ("p", \<^Type>\perm\) val arg_names = Old_Datatype_Prop.make_tnames arg_tys val args = map Free (arg_names ~~ arg_tys) val perm_bn = lookup perm_bn_map bn_trm val lhs = perm_bn $ p $ list_comb (constr, args) val rhs = list_comb (constr, map_index (mk_perm_bn_eq_rhs p perm_bn_map bn_args) args) in HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) end fun mk_perm_bn_eqs lthy perm_bn_map cns_info (bn_trm, bn_n, bn_argss) = let val nth_cns_info = nth cns_info bn_n in map2 (mk_perm_bn_eq lthy bn_trm perm_bn_map) bn_argss nth_cns_info end fun define_raw_bn_perms raw_dt_info bn_info lthy = if null bn_info then ([], [], lthy) else let val RawDtInfo {raw_tys, raw_cns_info, raw_inject_thms, raw_distinct_thms, raw_size_thms, ...} = raw_dt_info val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info) val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns val perm_bn_names = map (prefix "permute_") bn_names val perm_bn_arg_tys = map (nth raw_tys) bn_tys val perm_bn_tys = map (fn ty => @{typ "perm"} --> ty --> ty) perm_bn_arg_tys val perm_bn_frees = map Free (perm_bn_names ~~ perm_bn_tys) val perm_bn_map = bns ~~ perm_bn_frees val perm_bn_eqs = map (mk_perm_bn_eqs lthy perm_bn_map raw_cns_info) bn_info val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) perm_bn_names val all_fun_eqs = map (fn t => ((Binding.empty_atts, t), [], [])) (flat perm_bn_eqs) val prod_simps = @{thms prod.inject HOL.simp_thms} val lthy' = lthy |> Local_Theory.begin_nested |> snd |> Function.add_function all_fun_names all_fun_eqs Function_Common.default_config (pat_completeness_simp (prod_simps @ raw_inject_thms @ raw_distinct_thms)) |> snd |> Local_Theory.end_nested; val ({fs, simps, ...}, lthy'') = prove_termination_fun raw_size_thms lthy' val morphism = Proof_Context.export_morphism lthy'' (Proof_Context.transfer (Proof_Context.theory_of lthy'') lthy) val simps_exp = map (Morphism.thm morphism) (the simps) in (fs, simps_exp, lthy'') end (*** raw permutation functions ***) (** proves the two pt-type class properties **) fun prove_permute_zero induct bnfs perm_defs perm_fns ctxt = let val perm_types = map (body_type o fastype_of) perm_fns val perm_indnames = Old_Datatype_Prop.make_tnames perm_types fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T)) val goals = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) val map_ids = map BNF_Def.map_ident_of_bnf bnfs val rules = @{thm permute_zero} :: perm_defs @ map_ids val congs = map BNF_Def.map_cong0_of_bnf bnfs in Goal.prove ctxt perm_indnames [] goals (fn {context = ctxt', ...} => (Old_Datatype_Aux.ind_tac ctxt' induct perm_indnames THEN_ALL_NEW asm_simp_tac (fold Simplifier.add_cong congs (put_simpset HOL_basic_ss ctxt' addsimps rules))) 1) |> Old_Datatype_Aux.split_conj_thm end fun prove_permute_plus induct bnfs perm_defs perm_fns ctxt = let val p = Free ("p", \<^Type>\perm\) val q = Free ("q", \<^Type>\perm\) val perm_types = map (body_type o fastype_of) perm_fns val perm_indnames = Old_Datatype_Prop.make_tnames perm_types fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq (perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T))) val goals = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) val map_comps = map BNF_Def.map_comp_of_bnf bnfs val rules = @{thms permute_plus o_def} @ perm_defs @ map_comps val congs = map BNF_Def.map_cong0_of_bnf bnfs in Goal.prove ctxt ("p" :: "q" :: perm_indnames) [] goals (fn {context = ctxt', ...} => (Old_Datatype_Aux.ind_tac ctxt' induct perm_indnames THEN_ALL_NEW asm_simp_tac (fold Simplifier.add_cong congs (put_simpset HOL_basic_ss ctxt' addsimps rules))) 1) |> Old_Datatype_Aux.split_conj_thm end (* Return the map operator for the given type, along with its list of argument types, if a map operator exists; otherwise return NONE *) fun mk_map_of_type lthy (Type (c, tys)) = let fun mk_map bnf = let val live = BNF_Def.live_of_bnf bnf val t = BNF_Def.mk_map live tys tys (BNF_Def.map_of_bnf bnf) val (map_arg_tys, _) = BNF_Util.strip_typeN live (fastype_of t) in (t, map domain_type map_arg_tys) end in Option.map mk_map (BNF_Def.bnf_of lthy c) end | mk_map_of_type _ _ = NONE fun mk_perm_eq lthy ty_perm_assoc cnstr = let (* permute function with boolean flag indicating recursion *) fun mk_perm p ty = case (AList.lookup (op=) ty_perm_assoc ty) of SOME perm => (perm $ p, true) | NONE => (case mk_map_of_type lthy ty of SOME (t, tys) => let val (ts, recs) = split_list (map (mk_perm p) tys) in if exists I recs then (list_comb (t, ts), true) else (perm_const ty $ p, false) end | NONE => (perm_const ty $ p, false)) fun lookup_perm p (ty, arg) = fst (mk_perm p ty) $ arg val p = Free ("p", \<^Type>\perm\) val (arg_tys, ty) = strip_type (fastype_of cnstr) val arg_names = Name.variant_list ["p"] (Old_Datatype_Prop.make_tnames arg_tys) val args = map Free (arg_names ~~ arg_tys) val lhs = lookup_perm p (ty, list_comb (cnstr, args)) val rhs = list_comb (cnstr, map (lookup_perm p) (arg_tys ~~ args)) val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) in ((Binding.empty_atts, eq), [], []) end fun define_raw_perms raw_dt_info lthy = let val RawDtInfo {raw_dt_names, raw_fp_sugars, raw_tys, raw_ty_args, raw_all_cns, raw_induct_thm, ...} = raw_dt_info val bnfs = (#fp_nesting_bnfs o hd) raw_fp_sugars val perm_fn_names = raw_dt_names |> map Long_Name.base_name |> map (prefix "permute_") val perm_fn_types = map perm_ty raw_tys val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types) val perm_fn_binds = map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names val perm_eqs = map (mk_perm_eq lthy (raw_tys ~~ perm_fn_frees)) (flat raw_all_cns) fun tac ctxt (_, _, simps) = Class.intro_classes_tac ctxt [] THEN ALLGOALS (resolve_tac ctxt simps) fun morphism phi (fvs, dfs, simps) = (map (Morphism.term phi) fvs, map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps); val ((perm_funs, perm_eq_thms), lthy') = lthy |> Local_Theory.exit_global |> Class.instantiation (raw_dt_names, raw_ty_args, @{sort pt}) |> BNF_LFP_Compat.primrec perm_fn_binds perm_eqs val perm_zero_thms = prove_permute_zero raw_induct_thm bnfs perm_eq_thms perm_funs lthy' val perm_plus_thms = prove_permute_plus raw_induct_thm bnfs perm_eq_thms perm_funs lthy' in lthy' |> Class.prove_instantiation_exit_result morphism tac (perm_funs, perm_eq_thms, perm_zero_thms @ perm_plus_thms) ||> Named_Target.theory_init end (** equivarance proofs **) val eqvt_apply_sym = @{thm eqvt_apply[symmetric]} fun subproof_tac const_names simps = SUBPROOF (fn {prems, context = ctxt, ...} => HEADGOAL (simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps) THEN' eqvt_tac ctxt (eqvt_relaxed_config addexcls const_names) THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps (prems @ [eqvt_apply_sym])))) fun prove_eqvt_tac insts ind_thms const_names simps ctxt = HEADGOAL (Object_Logic.full_atomize_tac ctxt THEN' (DETERM o (Induct_Tacs.induct_tac ctxt insts (SOME ind_thms))) THEN_ALL_NEW subproof_tac const_names simps ctxt) fun mk_eqvt_goal pi const arg = let val lhs = mk_perm pi (const $ arg) val rhs = const $ (mk_perm pi arg) in HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) end fun raw_prove_eqvt consts ind_thms simps ctxt = if null consts then [] else let val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt val p = Free (p, \<^Type>\perm\) val arg_tys = consts |> map fastype_of |> map domain_type val (arg_names, ctxt'') = Variable.variant_fixes (Old_Datatype_Prop.make_tnames arg_tys) ctxt' val args = map Free (arg_names ~~ arg_tys) val goals = map2 (mk_eqvt_goal p) consts args val insts = map (single o SOME) arg_names val const_names = map (fst o dest_Const) consts in - Goal.prove_common ctxt'' NONE [] [] goals (fn {context, ...} => - prove_eqvt_tac insts ind_thms const_names simps context) + Goal.prove_common ctxt'' NONE [] [] goals (fn {context = goal_ctxt, ...} => + prove_eqvt_tac insts ind_thms const_names simps goal_ctxt) |> Proof_Context.export ctxt'' ctxt end end (* structure *) diff --git a/thys/Nominal2/nominal_eqvt.ML b/thys/Nominal2/nominal_eqvt.ML --- a/thys/Nominal2/nominal_eqvt.ML +++ b/thys/Nominal2/nominal_eqvt.ML @@ -1,147 +1,147 @@ (* Title: nominal_eqvt.ML Author: Stefan Berghofer (original code) Author: Christian Urban Author: Tjark Weber Automatic proofs for equivariance of inductive predicates. *) signature NOMINAL_EQVT = sig val raw_equivariance: Proof.context -> term list -> thm -> thm list -> thm list val equivariance_cmd: string -> Proof.context -> local_theory end structure Nominal_Eqvt : NOMINAL_EQVT = struct open Nominal_Permeq; open Nominal_ThmDecls; fun atomize_conv ctxt = Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE)) (put_simpset HOL_basic_ss ctxt addsimps @{thms induct_atomize}) fun atomize_intr ctxt = Conv.fconv_rule (Conv.prems_conv ~1 (atomize_conv ctxt)) fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1 - (Conv.params_conv ~1 (K (Conv.prems_conv ~1 (atomize_conv ctxt))) ctxt)) + (Conv.params_conv ~1 (Conv.prems_conv ~1 o atomize_conv) ctxt)) (** equivariance tactics **) fun eqvt_rel_single_case_tac ctxt pred_names pi intro = let val cpi = Thm.cterm_of ctxt pi val pi_intro_rule = Thm.instantiate' [] [NONE, SOME cpi] @{thm permute_boolI} val eqvt_sconfig = eqvt_strict_config addexcls pred_names in eqvt_tac ctxt eqvt_sconfig THEN' - SUBPROOF (fn {prems, context as ctxt, ...} => + SUBPROOF (fn {prems, context = goal_ctxt, ...} => let val simps1 = - put_simpset HOL_basic_ss ctxt addsimps @{thms permute_fun_def permute_self split_paired_all} + put_simpset HOL_basic_ss goal_ctxt addsimps @{thms permute_fun_def permute_self split_paired_all} val simps2 = - put_simpset HOL_basic_ss ctxt addsimps @{thms permute_bool_def permute_minus_cancel(2)} - val prems' = map (transform_prem2 ctxt pred_names) prems - val prems'' = map (fn thm => eqvt_rule ctxt eqvt_sconfig (thm RS pi_intro_rule)) prems' + put_simpset HOL_basic_ss goal_ctxt addsimps @{thms permute_bool_def permute_minus_cancel(2)} + val prems' = map (transform_prem2 goal_ctxt pred_names) prems + val prems'' = map (fn thm => eqvt_rule goal_ctxt eqvt_sconfig (thm RS pi_intro_rule)) prems' val prems''' = map (simplify simps2 o simplify simps1) prems'' in - HEADGOAL (resolve_tac ctxt [intro] THEN_ALL_NEW - resolve_tac ctxt (prems' @ prems'' @ prems''')) + HEADGOAL (resolve_tac goal_ctxt [intro] THEN_ALL_NEW + resolve_tac goal_ctxt (prems' @ prems'' @ prems''')) 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' ((DETERM o resolve_tac ctxt [induct]) :: cases) end (** equivariance procedure **) fun prepare_goal ctxt pi pred_with_args = let val (c, xs) = strip_comb pred_with_args fun is_nonfixed_Free (Free (s, _)) = not (Variable.is_fixed ctxt s) | is_nonfixed_Free _ = false fun mk_perm_nonfixed_Free t = if is_nonfixed_Free t then mk_perm pi t else t in HOLogic.mk_imp (pred_with_args, list_comb (c, map mk_perm_nonfixed_Free xs)) end fun name_of (Const (s, _)) = s fun raw_equivariance ctxt preds raw_induct intrs = let (* FIXME: polymorphic predicates should either be rejected or specialized to arguments of sort pt *) val is_already_eqvt = filter (is_eqvt ctxt) preds val _ = if null is_already_eqvt then () else error ("Already equivariant: " ^ commas (map (Syntax.string_of_term ctxt) is_already_eqvt)) val pred_names = map (name_of o head_of) preds val raw_induct' = atomize_induct ctxt raw_induct val intrs' = map (atomize_intr ctxt) intrs val (([raw_concl], [raw_pi]), ctxt') = ctxt |> Variable.import_terms false [Thm.concl_of raw_induct'] ||>> Variable.variant_fixes ["p"] val pi = Free (raw_pi, \<^Type>\perm\) val preds_with_args = raw_concl |> HOLogic.dest_Trueprop |> HOLogic.dest_conj |> map (fst o HOLogic.dest_imp) val goal = preds_with_args |> map (prepare_goal ctxt pi) |> foldr1 HOLogic.mk_conj |> HOLogic.mk_Trueprop in Goal.prove ctxt' [] [] goal - (fn {context, ...} => eqvt_rel_tac context pred_names pi raw_induct' intrs' 1) + (fn {context = goal_ctxt, ...} => eqvt_rel_tac goal_ctxt pred_names pi raw_induct' intrs' 1) |> Old_Datatype_Aux.split_conj_thm |> Proof_Context.export ctxt' ctxt |> map (fn th => th RS mp) |> map zero_var_indexes 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 (** equivariance command **) fun equivariance_cmd pred_name ctxt = let val ({names, ...}, {preds, raw_induct, intrs, ...}) = Inductive.the_inductive_global ctxt (long_name ctxt pred_name) val thms = raw_equivariance ctxt preds raw_induct intrs in fold_map note_named_thm (names ~~ thms) ctxt |> snd end val _ = Outer_Syntax.local_theory @{command_keyword equivariance} "Proves equivariance for inductive predicate involving nominal datatypes." (Parse.const >> equivariance_cmd) end (* structure *) diff --git a/thys/Nominal2/nominal_inductive.ML b/thys/Nominal2/nominal_inductive.ML --- a/thys/Nominal2/nominal_inductive.ML +++ b/thys/Nominal2/nominal_inductive.ML @@ -1,440 +1,441 @@ (* Title: nominal_inductive.ML Author: Christian Urban Author: Tjark Weber Infrastructure for proving strong induction theorems for inductive predicates involving nominal datatypes. Code based on an earlier version by Stefan Berghofer. *) signature NOMINAL_INDUCTIVE = sig val prove_strong_inductive: string list -> string list -> term list list -> thm -> thm list -> Proof.context -> Proof.state val prove_strong_inductive_cmd: xstring * (string * string list) list -> Proof.context -> Proof.state end structure Nominal_Inductive : NOMINAL_INDUCTIVE = struct fun mk_cplus p q = Thm.apply (Thm.apply @{cterm "plus :: perm => perm => perm"} p) q fun mk_cminus p = Thm.apply @{cterm "uminus :: perm => perm"} p fun minus_permute_intro_tac ctxt p = resolve_tac ctxt [Thm.instantiate' [] [SOME (mk_cminus p)] @{thm permute_boolE}] fun minus_permute_elim p thm = thm RS (Thm.instantiate' [] [NONE, SOME (mk_cminus p)] @{thm permute_boolI}) (* fixme: move to nominal_library *) fun real_head_of \<^Const_>\Trueprop for t\ = real_head_of t | real_head_of \<^Const_>\Pure.imp for _ t\ = real_head_of t | real_head_of \<^Const_>\Pure.all _ for \Abs (_, _, t)\\ = real_head_of t | real_head_of \<^Const_>\All _ for \Abs (_, _, t)\\ = real_head_of t | real_head_of \<^Const_>\HOL.induct_forall _ for \Abs (_, _, t)\\ = real_head_of t | real_head_of t = head_of t fun mk_vc_compat (avoid, avoid_trm) prems concl_args params = if null avoid then [] else let val vc_goal = concl_args |> HOLogic.mk_tuple |> mk_fresh_star avoid_trm |> HOLogic.mk_Trueprop |> (curry Logic.list_implies) prems |> fold_rev (Logic.all o Free) params val finite_goal = avoid_trm |> mk_finite |> HOLogic.mk_Trueprop |> (curry Logic.list_implies) prems |> fold_rev (Logic.all o Free) params in [vc_goal, finite_goal] end (* fixme: move to nominal_library *) fun map_term prop f trm = if prop trm then f trm else case trm of (t1 $ t2) => map_term prop f t1 $ map_term prop f t2 | Abs (x, T, t) => Abs (x, T, map_term prop f t) | _ => trm fun add_p_c p (c, c_ty) trm = let val (P, args) = strip_comb trm val (P_name, P_ty) = dest_Free P val (ty_args, bool) = strip_type P_ty val args' = map (mk_perm p) args in list_comb (Free (P_name, (c_ty :: ty_args) ---> bool), c :: args') |> (fn t => HOLogic.all_const c_ty $ lambda c t ) |> (fn t => HOLogic.all_const \<^Type>\perm\ $ lambda p t) end fun induct_forall_const T = \<^Const>\HOL.induct_forall T\ fun mk_induct_forall (a, T) t = induct_forall_const T $ Abs (a, T, t) fun add_c_prop qnt Ps (c, c_name, c_ty) trm = let fun add t = let val (P, args) = strip_comb t val (P_name, P_ty) = dest_Free P val (ty_args, bool) = strip_type P_ty val args' = args |> qnt ? map (incr_boundvars 1) in list_comb (Free (P_name, (c_ty :: ty_args) ---> bool), c :: args') |> qnt ? mk_induct_forall (c_name, c_ty) end in map_term (member (op =) Ps o head_of) add trm end fun prep_prem Ps c_name c_ty (avoid, avoid_trm) (params, prems, concl) = let val prems' = prems |> map (incr_boundvars 1) |> map (add_c_prop true Ps (Bound 0, c_name, c_ty)) val avoid_trm' = avoid_trm |> fold_rev absfree (params @ [(c_name, c_ty)]) |> strip_abs_body |> (fn t => mk_fresh_star_ty c_ty t (Bound 0)) |> HOLogic.mk_Trueprop val prems'' = if null avoid then prems' else avoid_trm' :: prems' val concl' = concl |> incr_boundvars 1 |> add_c_prop false Ps (Bound 0, c_name, c_ty) in mk_full_horn (params @ [(c_name, c_ty)]) prems'' concl' end (* fixme: move to nominal_library *) fun same_name (Free (a1, _), Free (a2, _)) = (a1 = a2) | same_name (Var (a1, _), Var (a2, _)) = (a1 = a2) | same_name (Const (a1, _), Const (a2, _)) = (a1 = a2) | same_name _ = false (* local abbreviations *) local open Nominal_Permeq in (* by default eqvt_strict_config contains unwanted @{thm permute_pure} *) val eqvt_sconfig = eqvt_strict_config addpres @{thms permute_minus_cancel} fun eqvt_stac ctxt = eqvt_tac ctxt eqvt_sconfig fun eqvt_srule ctxt = eqvt_rule ctxt eqvt_sconfig end val all_elims = let fun spec' ct = Thm.instantiate' [SOME (Thm.ctyp_of_cterm ct)] [NONE, SOME ct] @{thm spec} in fold (fn ct => fn th => th RS spec' ct) end fun helper_tac flag prm p ctxt = Subgoal.SUBPROOF (fn {context = ctxt', prems, ...} => let val prems' = prems |> map (minus_permute_elim p) |> map (eqvt_srule ctxt') val prm' = (prems' MRS prm) |> flag ? (all_elims [p]) |> flag ? (eqvt_srule ctxt') in asm_full_simp_tac (put_simpset HOL_ss ctxt' addsimps (prm' :: @{thms HOL.induct_forall_def})) 1 end) ctxt fun non_binder_tac prem intr_cvars Ps ctxt = Subgoal.SUBPROOF (fn {context = ctxt', params, prems, ...} => let val (prms, p, _) = split_last2 (map snd params) val prm_tys = map (fastype_of o Thm.term_of) prms val cperms = map (Thm.cterm_of ctxt' o perm_const) prm_tys val p_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 p ct2) cperms prms val prem' = prem |> infer_instantiate ctxt' (map (#1 o dest_Var o Thm.term_of) intr_cvars ~~ p_prms) |> eqvt_srule ctxt' (* for inductive-premises*) fun tac1 prm = helper_tac true prm p ctxt' (* for non-inductive premises *) fun tac2 prm = EVERY' [ minus_permute_intro_tac ctxt' p, eqvt_stac ctxt', helper_tac false prm p ctxt' ] fun select prm (t, i) = (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i in EVERY1 [ eqvt_stac ctxt', resolve_tac ctxt' [prem'], RANGE (map (SUBGOAL o select) prems) ] end) ctxt fun fresh_thm ctxt user_thm p c concl_args avoid_trm = let val conj1 = mk_fresh_star (mk_perm (Bound 0) (mk_perm p avoid_trm)) c val conj2 = mk_fresh_star_ty \<^Type>\perm\ (mk_supp (HOLogic.mk_tuple (map (mk_perm p) concl_args))) (Bound 0) val fresh_goal = mk_exists ("q", \<^Type>\perm\) (HOLogic.mk_conj (conj1, conj2)) |> HOLogic.mk_Trueprop val ss = @{thms finite_supp supp_Pair finite_Un permute_finite} @ @{thms fresh_star_Pair fresh_star_permute_iff} val simp = asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps ss) in Goal.prove ctxt [] [] fresh_goal - (K (HEADGOAL (resolve_tac ctxt @{thms at_set_avoiding2} + (fn {context = goal_ctxt, ...} => + HEADGOAL (resolve_tac goal_ctxt @{thms at_set_avoiding2} THEN_ALL_NEW EVERY' [cut_facts_tac user_thm, REPEAT o - eresolve_tac ctxt @{thms conjE}, simp]))) + eresolve_tac goal_ctxt @{thms conjE}, simp])) end val supp_perm_eq' = @{lemma "fresh_star (supp (permute p x)) q ==> permute p x == permute (q + p) x" by (simp add: supp_perm_eq)} val fresh_star_plus = @{lemma "fresh_star (permute q (permute p x)) c ==> fresh_star (permute (q + p) x) c" by (simp add: permute_plus)} fun binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt = Subgoal.FOCUS (fn {context = ctxt, params, prems, concl, ...} => let val (prms, p, c) = split_last2 (map snd params) val prm_trms = map Thm.term_of prms val prm_tys = map fastype_of prm_trms val avoid_trm' = subst_free (param_trms ~~ prm_trms) avoid_trm val concl_args' = map (subst_free (param_trms ~~ prm_trms)) concl_args val user_thm' = map (infer_instantiate ctxt (map (#1 o dest_Var o Thm.term_of) intr_cvars ~~ prms)) user_thm |> map (full_simplify (put_simpset HOL_ss ctxt addsimps (@{thm fresh_star_Pair}::prems))) val fthm = fresh_thm ctxt user_thm' (Thm.term_of p) (Thm.term_of c) concl_args' avoid_trm' val (([(_, q)], fprop :: fresh_eqs), ctxt') = Obtain.result (K (EVERY1 [eresolve_tac ctxt @{thms exE}, full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms supp_Pair fresh_star_Un}), REPEAT o eresolve_tac ctxt @{thms conjE}, dresolve_tac ctxt [fresh_star_plus], REPEAT o dresolve_tac ctxt [supp_perm_eq']])) [fthm] ctxt val expand_conv = Conv.try_conv (Conv.rewrs_conv fresh_eqs) fun expand_conv_bot ctxt = Conv.bottom_conv (K expand_conv) ctxt val cperms = map (Thm.cterm_of ctxt' o perm_const) prm_tys val qp_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 (mk_cplus q p) ct2) cperms prms val prem' = prem |> infer_instantiate ctxt' (map (#1 o dest_Var o Thm.term_of) intr_cvars ~~ qp_prms) |> eqvt_srule ctxt' val fprop' = eqvt_srule ctxt' fprop val tac_fresh = simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [fprop']) (* for inductive-premises*) - fun tac1 prm = helper_tac true prm (mk_cplus q p) ctxt' + fun tac1 goal_ctxt prm = helper_tac true prm (mk_cplus q p) goal_ctxt (* for non-inductive premises *) - fun tac2 prm = - EVERY' [ minus_permute_intro_tac ctxt' (mk_cplus q p), - eqvt_stac ctxt', - helper_tac false prm (mk_cplus q p) ctxt' ] + fun tac2 goal_ctxt prm = + EVERY' [ minus_permute_intro_tac goal_ctxt (mk_cplus q p), + eqvt_stac goal_ctxt, + helper_tac false prm (mk_cplus q p) goal_ctxt ] - fun select prm (t, i) = - (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i + fun select goal_ctxt prm (t, i) = + (if member same_name Ps (real_head_of t) then tac1 goal_ctxt prm else tac2 goal_ctxt prm) i val side_thm = Goal.prove ctxt' [] [] (Thm.term_of concl) - (fn {context = ctxt'', ...} => - EVERY1 [ CONVERSION (expand_conv_bot ctxt''), - eqvt_stac ctxt'', - resolve_tac ctxt'' [prem'], - RANGE (tac_fresh :: map (SUBGOAL o select) prems) ]) + (fn {context = goal_ctxt, ...} => + EVERY1 [ CONVERSION (expand_conv_bot goal_ctxt), + eqvt_stac goal_ctxt, + resolve_tac goal_ctxt [prem'], + RANGE (tac_fresh :: map (SUBGOAL o select goal_ctxt) prems) ]) |> singleton (Proof_Context.export ctxt' ctxt) in resolve_tac ctxt [side_thm] 1 end) ctxt fun case_tac ctxt Ps avoid avoid_trm intr_cvars param_trms prem user_thm concl_args = let val tac1 = non_binder_tac prem intr_cvars Ps ctxt val tac2 = binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt in EVERY' [ resolve_tac ctxt @{thms allI}, resolve_tac ctxt @{thms allI}, if null avoid then tac1 else tac2 ] end fun prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms concl_args {prems, context = ctxt} = let val cases_tac = @{map 7} (case_tac ctxt Ps) avoids avoid_trms intr_cvars param_trms prems user_thms concl_args in EVERY1 [ DETERM o resolve_tac ctxt [raw_induct], RANGE cases_tac ] end val normalise = @{lemma "(Q \ (\p c. P p c)) \ (\c. Q \ P (0::perm) c)" by simp} fun prove_strong_inductive pred_names rule_names avoids raw_induct intrs ctxt = let val ((_, [raw_induct']), ctxt') = Variable.import true [raw_induct] ctxt val (ind_prems, ind_concl) = raw_induct' |> Thm.prop_of |> Logic.strip_horn |>> map strip_full_horn val params = map (fn (x, _, _) => x) ind_prems val param_trms = (map o map) Free params val intr_vars_tys = map (fn t => rev (Term.add_vars (Thm.prop_of t) [])) intrs val intr_vars = (map o map) fst intr_vars_tys val intr_vars_substs = map2 (curry (op ~~)) intr_vars param_trms val intr_cvars = (map o map) (Thm.cterm_of ctxt o Var) intr_vars_tys val (intr_prems, intr_concls) = intrs |> map Thm.prop_of |> map2 subst_Vars intr_vars_substs |> map Logic.strip_horn |> split_list val intr_concls_args = map (snd o fixed_nonfixed_args ctxt' o HOLogic.dest_Trueprop) intr_concls val avoid_trms = avoids |> (map o map) (setify ctxt') |> map fold_union val vc_compat_goals = map4 mk_vc_compat (avoids ~~ avoid_trms) intr_prems intr_concls_args params val ([c_name, a, p], ctxt'') = Variable.variant_fixes ["c", "'a", "p"] ctxt' val c_ty = TFree (a, @{sort fs}) val c = Free (c_name, c_ty) val p = Free (p, \<^Type>\perm\) val (preconds, ind_concls) = ind_concl |> HOLogic.dest_Trueprop |> HOLogic.dest_conj |> map HOLogic.dest_imp |> split_list val Ps = map (fst o strip_comb) ind_concls val ind_concl' = ind_concls |> map (add_p_c p (c, c_ty)) |> (curry (op ~~)) preconds |> map HOLogic.mk_imp |> fold_conj |> HOLogic.mk_Trueprop val ind_prems' = ind_prems |> map2 (prep_prem Ps c_name c_ty) (avoids ~~ avoid_trms) fun after_qed ctxt_outside user_thms ctxt = let val strong_ind_thms = Goal.prove ctxt [] ind_prems' ind_concl' (prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms intr_concls_args) |> singleton (Proof_Context.export ctxt ctxt_outside) |> Old_Datatype_Aux.split_conj_thm |> map (fn thm => thm RS normalise) |> map (asm_full_simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms permute_zero induct_rulify})) |> map (Drule.rotate_prems (length ind_prems')) |> map zero_var_indexes val qualified_thm_name = pred_names |> map Long_Name.base_name |> space_implode "_" |> (fn s => Binding.qualify false s (Binding.name "strong_induct")) val attrs = [ Attrib.internal (K (Rule_Cases.consumes 1)), Attrib.internal (K (Rule_Cases.case_names rule_names)) ] in ctxt |> Local_Theory.note ((qualified_thm_name, attrs), strong_ind_thms) |> snd end in Proof.theorem NONE (after_qed ctxt) ((map o map) (rpair []) vc_compat_goals) ctxt'' end fun prove_strong_inductive_cmd (pred_name, avoids) ctxt = let val ({names, ...}, {raw_induct, intrs, ...}) = Inductive.the_inductive_global ctxt (long_name ctxt pred_name) val rule_names = hd names |> the o Induct.lookup_inductP ctxt |> fst o Rule_Cases.get |> map (fst o fst) val case_names = map fst avoids val _ = case duplicates (op =) case_names of [] => () | xs => error ("Duplicate case names: " ^ commas_quote xs) val _ = case subtract (op =) rule_names case_names of [] => () | xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs) val avoids_ordered = order_default (op =) [] rule_names avoids fun read_avoids avoid_trms intr = let (* fixme hack *) val (((_, inst), _), ctxt') = Variable.import true [intr] ctxt val trms = build (inst |> Vars.fold (cons o Thm.term_of o snd)) val ctxt'' = fold Variable.declare_term trms ctxt' in map (Syntax.read_term ctxt'') avoid_trms end val avoid_trms = map2 read_avoids avoids_ordered intrs in prove_strong_inductive names rule_names avoid_trms raw_induct intrs ctxt end (* outer syntax *) local val single_avoid_parser = Parse.name -- (@{keyword ":"} |-- Parse.and_list1 Parse.term) val avoids_parser = Scan.optional (@{keyword "avoids"} |-- Parse.enum1 "|" single_avoid_parser) [] val main_parser = Parse.name -- avoids_parser in val _ = Outer_Syntax.local_theory_to_proof @{command_keyword nominal_inductive} "prove strong induction theorem for inductive predicate involving nominal datatypes" (main_parser >> prove_strong_inductive_cmd) end end diff --git a/thys/Nominal2/nominal_library.ML b/thys/Nominal2/nominal_library.ML --- a/thys/Nominal2/nominal_library.ML +++ b/thys/Nominal2/nominal_library.ML @@ -1,488 +1,488 @@ (* Title: nominal_library.ML Author: Christian Urban Library functions for nominal. *) signature NOMINAL_LIBRARY = sig val mk_sort_of: term -> term val atom_ty: typ -> typ val atom_const: typ -> term val mk_atom_ty: typ -> term -> term val mk_atom: term -> term val mk_atom_set_ty: typ -> term -> term val mk_atom_set: term -> term val mk_atom_fset_ty: typ -> term -> term val mk_atom_fset: term -> term val mk_atom_list_ty: typ -> term -> term val mk_atom_list: term -> term val is_atom: Proof.context -> typ -> bool val is_atom_set: Proof.context -> typ -> bool val is_atom_fset: Proof.context -> typ -> bool val is_atom_list: Proof.context -> typ -> bool val to_set_ty: typ -> term -> term val to_set: term -> term val atomify_ty: Proof.context -> typ -> term -> term val atomify: Proof.context -> term -> term val setify_ty: Proof.context -> typ -> term -> term val setify: Proof.context -> term -> term val listify_ty: Proof.context -> typ -> term -> term val listify: Proof.context -> term -> term val fresh_const: typ -> term val mk_fresh_ty: typ -> term -> term -> term val mk_fresh: term -> term -> term val fresh_star_const: typ -> term val mk_fresh_star_ty: typ -> term -> term -> term val mk_fresh_star: term -> term -> term val supp_const: typ -> term val mk_supp_ty: typ -> term -> term val mk_supp: term -> term 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_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 val fold_conj_balanced: term list -> term (* functions for de-Bruijn open terms *) val mk_binop_env: typ list -> string -> term * term -> term val mk_union_env: typ list -> term * term -> term val fold_union_env: typ list -> term list -> term (* fresh arguments for a term *) val fresh_args: Proof.context -> term -> term list (* some logic operations *) val strip_full_horn: term -> (string * typ) list * term list * term val mk_full_horn: (string * typ) list -> term list -> term -> term (* datatype operations *) type cns_info = (term * typ * typ list * bool list) list val all_dtyp_constrs_types: Old_Datatype_Aux.descr -> cns_info list (* tactics for function package *) val size_ss: simpset val pat_completeness_simp: thm list -> Proof.context -> tactic val prove_termination_ind: Proof.context -> int -> tactic val prove_termination_fun: 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: Proof.context -> thm -> thm val atomize_rule: Proof.context -> int -> thm -> thm val atomize_concl: Proof.context -> thm -> thm (* applies a tactic to a formula composed of conjunctions *) val conj_tac: Proof.context -> (int -> tactic) -> int -> tactic end structure Nominal_Library: NOMINAL_LIBRARY = struct fun mk_sort_of t = \<^Const>\sort_of for t\; fun atom_ty ty = ty --> @{typ "atom"}; fun atom_const ty = \<^Const>\atom ty\ fun mk_atom_ty ty t = atom_const ty $ t; fun mk_atom t = mk_atom_ty (fastype_of t) t; fun mk_atom_set_ty ty t = let val atom_ty = HOLogic.dest_setT ty in \<^Const>\image atom_ty \<^Type>\atom\ for \atom_const atom_ty\ t\ end fun mk_atom_fset_ty ty t = let val atom_ty = dest_fsetT ty in \<^Const>\fimage atom_ty \<^Type>\atom\ for \atom_const atom_ty\ t\ end fun mk_atom_list_ty ty t = let val atom_ty = dest_listT ty in \<^Const>\map atom_ty \<^Type>\atom\ for \atom_const atom_ty\ t\ end fun mk_atom_set t = mk_atom_set_ty (fastype_of t) t fun mk_atom_fset t = mk_atom_fset_ty (fastype_of t) t fun mk_atom_list t = mk_atom_list_ty (fastype_of t) t (* coerces a list into a set *) fun to_set_ty ty t = case ty of @{typ "atom list"} => @{term "set :: atom list => atom set"} $ t | @{typ "atom fset"} => @{term "fset :: atom fset => atom set"} $ t | _ => t fun to_set t = to_set_ty (fastype_of t) t (* testing for concrete atom types *) fun is_atom ctxt ty = Sign.of_sort (Proof_Context.theory_of ctxt) (ty, @{sort at_base}) fun is_atom_set ctxt \<^Type>\fun ty \<^Type>\bool\\ = is_atom ctxt ty | is_atom_set _ _ = false; fun is_atom_fset ctxt \<^Type>\fset ty\ = is_atom ctxt ty | is_atom_fset _ _ = false; fun is_atom_list ctxt \<^Type>\list ty\ = is_atom ctxt ty | is_atom_list _ _ = false (* functions that coerce singletons, sets, fsets and lists of concrete atoms into general atoms sets / lists *) fun atomify_ty ctxt ty t = if is_atom ctxt ty then mk_atom_ty ty t else if is_atom_set ctxt ty then mk_atom_set_ty ty t else if is_atom_fset ctxt ty then mk_atom_fset_ty ty t else if is_atom_list ctxt ty then mk_atom_list_ty ty t else raise TERM ("atomify: term is not an atom, set or list of atoms", [t]) fun setify_ty ctxt ty t = if is_atom ctxt ty then HOLogic.mk_set \<^Type>\atom\ [mk_atom_ty ty t] else if is_atom_set ctxt ty then mk_atom_set_ty ty t else if is_atom_fset ctxt ty then @{term "fset :: atom fset => atom set"} $ mk_atom_fset_ty ty t else if is_atom_list ctxt ty then @{term "set :: atom list => atom set"} $ mk_atom_list_ty ty t else raise TERM ("setify: term is not an atom, set or list of atoms", [t]) fun listify_ty ctxt ty t = if is_atom ctxt ty then HOLogic.mk_list \<^Type>\atom\ [mk_atom_ty ty t] else if is_atom_list ctxt ty then mk_atom_list_ty ty t else raise TERM ("listify: term is not an atom or list of atoms", [t]) fun atomify ctxt t = atomify_ty ctxt (fastype_of t) t fun setify ctxt t = setify_ty ctxt (fastype_of t) t fun listify ctxt t = listify_ty ctxt (fastype_of t) t fun fresh_const ty = \<^Const>\fresh ty\ fun mk_fresh_ty ty t1 t2 = fresh_const ty $ t1 $ t2 fun mk_fresh t1 t2 = mk_fresh_ty (fastype_of t2) t1 t2 fun fresh_star_const ty = \<^Const>\fresh_star ty\ fun mk_fresh_star_ty ty t1 t2 = fresh_star_const ty $ t1 $ t2 fun mk_fresh_star t1 t2 = mk_fresh_star_ty (fastype_of t2) t1 t2 fun supp_const ty = \<^Const>\supp 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_const ty = \<^Const>\supp_rel 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>\supports ty\; 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>\finite ty\ fun mk_finite_ty ty t = finite_const ty $ t fun mk_finite t = mk_finite_ty (HOLogic.dest_setT (fastype_of t)) t (* 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"} fun fold_conj_balanced ts = Balanced_Tree.make HOLogic.mk_conj ts (* functions for de-Bruijn open terms *) fun mk_binop_env tys c (t, u) = let val ty = fastype_of1 (tys, t) in Const (c, [ty, ty] ---> ty) $ t $ u end fun mk_union_env tys (t1, @{term "{}::atom set"}) = t1 | mk_union_env tys (@{term "{}::atom set"}, t2) = t2 | mk_union_env tys (t1, @{term "set ([]::atom list)"}) = t1 | mk_union_env tys (@{term "set ([]::atom list)"}, t2) = t2 | mk_union_env tys (t1, t2) = mk_binop_env tys @{const_name "sup"} (t1, t2) fun fold_union_env tys trms = fold_left (mk_union_env tys) trms @{term "{}::atom set"} (* 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 (** some logic operations **) (* decompses a formula into params, premises and a conclusion *) fun strip_full_horn trm = let fun strip_outer_params \<^Const_>\Pure.all _ for \Abs (a, T, t)\\ = strip_outer_params t |>> cons (a, T) | strip_outer_params B = ([], B) val (params, body) = strip_outer_params trm val (prems, concl) = Logic.strip_horn body in (params, prems, concl) end (* composes a formula out of params, premises and a conclusion *) fun mk_full_horn params prems concl = Logic.list_implies (prems, concl) |> fold_rev mk_all params (** datatypes **) (* constructor infos *) type cns_info = (term * typ * typ list * bool list) list (* - term for constructor constant - type of the constructor - types of the arguments - flags indicating whether the argument is recursive *) (* 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 = let fun aux ((ty_name, vs), (cname, args)) = let val vs_tys = map (Old_Datatype_Aux.typ_of_dtyp descr) vs val ty = Type (ty_name, vs_tys) val arg_tys = map (Old_Datatype_Aux.typ_of_dtyp descr) args val is_rec = map Old_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 (** function package tactics **) fun pat_completeness_simp simps ctxt = let val simpset = put_simpset HOL_basic_ss ctxt addsimps (@{thms sum.inject sum.distinct} @ simps) in Pat_Completeness.pat_completeness_tac ctxt 1 THEN ALLGOALS (asm_full_simp_tac simpset) end (* simpset for size goals *) val size_ss = simpset_of (put_simpset HOL_ss @{context} addsimprocs [@{simproc natless_cancel_numerals}] addsimps @{thms in_measure wf_measure sum.case add_Suc_right add.right_neutral zero_less_Suc prod.size(1) mult_Suc_right}) val natT = @{typ nat} fun size_prod_const T1 T2 = \<^Const>\size_prod T1 T2\ fun snd_const T1 T2 = \<^Const>\Product_Type.snd T1 T2\ fun mk_measure_trm f ctxt T = HOLogic.dest_setT T |> fst o HOLogic.dest_prodT |> f |> curry (op $) \<^Const>\measure dummyT\ |> Syntax.check_term ctxt (* wf-goal arising in induction_schema *) fun prove_termination_ind ctxt = let fun mk_size_measure T = case T of \<^Type>\sum T1 T2\ => Sum_Tree.mk_sumcase T1 T2 \<^Type>\nat\ (mk_size_measure T1) (mk_size_measure T2) | \<^Type>\prod T1 T2\ => HOLogic.mk_comp (mk_size_measure T2, snd_const T1 T2) | _ => HOLogic.size_const T val measure_trm = mk_measure_trm (mk_size_measure) ctxt in Function_Relation.relation_tac ctxt measure_trm end (* wf-goal arising in function definitions *) fun prove_termination_fun size_simps ctxt = let fun mk_size_measure T = case T of \<^Type>\sum T1 T2\ => Sum_Tree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure T2) | \<^Type>\prod T1 T2\ => size_prod_const T1 T2 $ (mk_size_measure T1) $ (mk_size_measure T2) | _ => HOLogic.size_const T val measure_trm = mk_measure_trm (mk_size_measure) ctxt val tac = Function_Relation.relation_tac ctxt measure_trm THEN_ALL_NEW simp_tac (put_simpset size_ss ctxt addsimps size_simps) in Function.prove_termination NONE (HEADGOAL tac) ctxt end (** 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 simpset = put_simpset HOL_basic_ss ctxt addsimps @{thms split_def} in EVERY [cut_facts_tac [thm] 1, eresolve_tac ctxt [rev_mp] 1, REPEAT_DETERM (FIRSTGOAL (simp_tac simpset THEN' resolve_tac ctxt monos)), - REPEAT_DETERM (resolve_tac ctxt [impI] 1 THEN (assume_tac ctxt 1 ORELSE tac))] + REPEAT_DETERM (resolve_tac ctxt [impI] 1 THEN (assume_tac ctxt 1 ORELSE tac ctxt))] end fun map_thm ctxt f tac thm = let val opt_goal_trm = map_term f (Thm.prop_of thm) in case opt_goal_trm of NONE => thm | SOME goal => - Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm) + Goal.prove ctxt [] [] goal (fn {context = ctxt', ...} => 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_>\conj for 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_>\conj for 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) (eresolve_tac ctxt [conjunct1] 1) thm + map_thm ctxt (split_conj1 names) (fn ctxt' => eresolve_tac ctxt' [conjunct1] 1) thm fun transform_prem2 ctxt names thm = - map_thm ctxt (split_conj2 names) (eresolve_tac ctxt [conjunct2] 1) thm + map_thm ctxt (split_conj2 names) (fn ctxt' => eresolve_tac ctxt' [conjunct2] 1) thm (* transforms a theorem into one of the object logic *) fun atomize ctxt = Conv.fconv_rule (Object_Logic.atomize ctxt) o Thm.forall_intr_vars; fun atomize_rule ctxt i thm = Conv.fconv_rule (Conv.concl_conv i (Object_Logic.atomize ctxt)) thm fun atomize_concl ctxt thm = atomize_rule ctxt (length (Thm.prems_of thm)) thm (* applies a tactic to a formula composed of conjunctions *) fun conj_tac ctxt tac i = let fun select (trm, i) = case trm of \<^Const_>\Trueprop for t'\ => select (t', i) | \<^Const_>\conj for _ _\ => EVERY' [resolve_tac ctxt @{thms conjI}, RANGE [conj_tac ctxt tac, conj_tac ctxt tac]] i | _ => tac i in SUBGOAL select i end end (* structure *) open Nominal_Library; diff --git a/thys/Nominal2/nominal_mutual.ML b/thys/Nominal2/nominal_mutual.ML --- a/thys/Nominal2/nominal_mutual.ML +++ b/thys/Nominal2/nominal_mutual.ML @@ -1,508 +1,514 @@ (* Nominal Mutual Functions Author: Christian Urban heavily based on the code of Alexander Krauss (code forked on 14 January 2011) Joachim Breitner helped with the auxiliary graph definitions (7 August 2012) Mutual recursive nominal function definitions. *) signature NOMINAL_FUNCTION_MUTUAL = sig val prepare_nominal_function_mutual : Nominal_Function_Common.nominal_function_config -> string (* defname *) -> ((string * typ) * mixfix) list -> term list -> local_theory -> ((thm (* goalstate *) * (Proof.context -> thm -> Nominal_Function_Common.nominal_function_result) (* proof continuation *) ) * local_theory) end structure Nominal_Function_Mutual: NOMINAL_FUNCTION_MUTUAL = struct open Function_Lib open Function_Common open Nominal_Function_Common type qgar = string * (string * typ) list * term list * term list * term datatype mutual_part = MutualPart of {i : int, i' : int, fvar : string * typ, cargTs: typ list, f_def: term, f: term option, f_defthm : thm option} datatype mutual_info = Mutual of {n : int, n' : int, fsum_var : string * typ, ST: typ, RST: typ, parts: mutual_part list, fqgars: qgar list, qglrs: ((string * typ) list * term list * term * term) list, fsum : term option} fun mutual_induct_Pnames n = if n < 5 then fst (chop n ["P","Q","R","S"]) else map (fn i => "P" ^ string_of_int i) (1 upto n) fun get_part fname = the o find_first (fn (MutualPart {fvar=(n,_), ...}) => n = fname) (* FIXME *) fun mk_prod_abs e (t1, t2) = let val bTs = rev (map snd e) val T1 = fastype_of1 (bTs, t1) val T2 = fastype_of1 (bTs, t2) in HOLogic.pair_const T1 T2 $ t1 $ t2 end fun analyze_eqs ctxt defname fs eqs = let val num = length fs val fqgars = map (split_def ctxt (K true)) eqs val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars |> AList.lookup (op =) #> the fun curried_types (fname, fT) = let val (caTs, uaTs) = chop (arity_of fname) (binder_types fT) in (caTs, uaTs ---> body_type fT) end val (caTss, resultTs) = split_list (map curried_types fs) val argTs = map (foldr1 HOLogic.mk_prodT) caTss val dresultTs = distinct (op =) resultTs val n' = length dresultTs val RST = Balanced_Tree.make (uncurry Sum_Tree.mk_sumT) dresultTs val ST = Balanced_Tree.make (uncurry Sum_Tree.mk_sumT) argTs val fsum_type = ST --> RST val ([fsum_var_name], _) = Variable.add_fixes [ defname ^ "_sum" ] ctxt val fsum_var = (fsum_var_name, fsum_type) fun define (fvar as (n, _)) caTs resultT i = let val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *) val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1 val f_exp = Sum_Tree.mk_proj RST n' i' (Free fsum_var $ Sum_Tree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars)) val def = Term.abstract_over (Free fsum_var, fold_rev lambda vars f_exp) val rew = (n, fold_rev lambda vars f_exp) in (MutualPart {i=i, i'=i', fvar=fvar,cargTs=caTs,f_def=def,f=NONE,f_defthm=NONE}, rew) end val (parts, rews) = split_list (map4 define fs caTss resultTs (1 upto num)) fun convert_eqs (f, qs, gs, args, rhs) = let val MutualPart {i, i', ...} = get_part f parts val rhs' = rhs |> map_aterms (fn t as Free (n, _) => the_default t (AList.lookup (op =) rews n) | t => t) in (qs, gs, Sum_Tree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args), Envir.beta_norm (Sum_Tree.mk_inj RST n' i' rhs')) end val qglrs = map convert_eqs fqgars in Mutual {n=num, n'=n', fsum_var=fsum_var, ST=ST, RST=RST, parts=parts, fqgars=fqgars, qglrs=qglrs, fsum=NONE} end fun define_projections fixes mutual fsum lthy = let fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy = let val ((f, (_, f_defthm)), lthy') = Local_Theory.define ((Binding.name fname, mixfix), ((Binding.concealed (Binding.name (fname ^ "_def")), []), Term.subst_bound (fsum, f_def))) lthy in (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def, f=SOME f, f_defthm=SOME f_defthm }, lthy') end val Mutual { n, n', fsum_var, ST, RST, parts, fqgars, qglrs, ... } = mutual val (parts', lthy') = fold_map def (parts ~~ fixes) lthy in (Mutual { n=n, n'=n', fsum_var=fsum_var, ST=ST, RST=RST, parts=parts', fqgars=fqgars, qglrs=qglrs, fsum=SOME fsum }, lthy') end fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F = let val oqnames = map fst pre_qs val (qs, _) = Variable.variant_fixes oqnames ctxt |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs fun inst t = subst_bounds (rev qs, t) val gs = map inst pre_gs val args = map inst pre_args val rhs = inst pre_rhs val cqs = map (Thm.cterm_of ctxt) qs val (ags, ctxt') = fold_map Thm.assume_hyps (map (Thm.cterm_of ctxt) gs) ctxt val import = fold Thm.forall_elim cqs #> fold Thm.elim_implies ags val export = fold_rev (Thm.implies_intr o Thm.cprop_of) ags #> fold_rev forall_intr_rename (oqnames ~~ cqs) in F ctxt' (f, qs, gs, args, rhs) import export end fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs) import (export : thm -> thm) sum_psimp_eq = let val (MutualPart {f=SOME f, ...}) = get_part fname parts val psimp = import sum_psimp_eq val ((simp, restore_cond), ctxt') = case cprems_of psimp of [] => ((psimp, I), ctxt) | [cond] => let val (asm, ctxt') = Thm.assume_hyps cond ctxt in ((Thm.implies_elim psimp asm, Thm.implies_intr cond), ctxt') end | _ => raise General.Fail "Too many conditions" in Goal.prove ctxt' [] [] (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs)) - (fn _ => (Local_Defs.unfold_tac ctxt' all_orig_fdefs) - THEN EqSubst.eqsubst_tac ctxt' [0] [simp] 1 - THEN (simp_tac ctxt') 1) + (fn {context = goal_ctxt, ...} => + (Local_Defs.unfold_tac goal_ctxt all_orig_fdefs) + THEN EqSubst.eqsubst_tac goal_ctxt [0] [simp] 1 + THEN (simp_tac goal_ctxt) 1) |> restore_cond |> export end val inl_perm = @{lemma "x = Inl y ==> projl (permute p x) = permute p (projl x)" by simp} val inr_perm = @{lemma "x = Inr y ==> projr (permute p x) = permute p (projr x)" by simp} fun recover_mutual_eqvt eqvt_thm all_orig_fdefs parts ctxt (fname, _, _, args, _) import (export : thm -> thm) sum_psimp_eq = let val (MutualPart {f=SOME f, ...}) = get_part fname parts val psimp = import sum_psimp_eq val ((cond, simp, restore_cond), ctxt') = case cprems_of psimp of [] => (([], psimp, I), ctxt) | [cond] => let val (asm, ctxt') = Thm.assume_hyps cond ctxt in (([asm], Thm.implies_elim psimp asm, Thm.implies_intr cond), ctxt') end | _ => raise General.Fail "Too many conditions" val ([p], ctxt'') = ctxt' |> fold Variable.declare_term args |> Variable.variant_fixes ["p"] val p = Free (p, \<^Type>\perm\) val simpset = put_simpset HOL_basic_ss ctxt'' addsimps @{thms permute_sum.simps[symmetric] Pair_eqvt[symmetric] sum.sel} @ [(cond MRS eqvt_thm) RS @{thm sym}] @ [inl_perm, inr_perm, simp] val goal_lhs = mk_perm p (list_comb (f, args)) val goal_rhs = list_comb (f, map (mk_perm p) args) in Goal.prove ctxt'' [] [] (HOLogic.Trueprop $ HOLogic.mk_eq (goal_lhs, goal_rhs)) - (fn _ => Local_Defs.unfold_tac ctxt'' all_orig_fdefs + (fn {context = goal_ctxt, ...} => + Local_Defs.unfold_tac goal_ctxt all_orig_fdefs THEN (asm_full_simp_tac simpset 1)) |> singleton (Proof_Context.export ctxt'' ctxt) |> restore_cond |> export end fun mk_applied_form ctxt caTs thm = let val xs = map_index (fn (i,T) => Thm.cterm_of ctxt (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *) in fold (fn x => fn thm => Thm.combination thm (Thm.reflexive x)) xs thm |> Conv.fconv_rule (Thm.beta_conversion true) |> fold_rev Thm.forall_intr xs |> Thm.forall_elim_vars 0 end fun mutual_induct_rules ctxt induct all_f_defs (Mutual {n, ST, parts, ...}) = let val cert = Thm.cterm_of ctxt val newPs = map2 (fn Pname => fn MutualPart {cargTs, ...} => Free (Pname, cargTs ---> HOLogic.boolT)) (mutual_induct_Pnames (length parts)) parts fun mk_P (MutualPart {cargTs, ...}) P = let val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs val atup = foldr1 HOLogic.mk_prod avars in HOLogic.tupled_lambda atup (list_comb (P, avars)) end val Ps = map2 mk_P parts newPs val case_exp = Sum_Tree.mk_sumcases HOLogic.boolT Ps val induct_inst = Thm.forall_elim (cert case_exp) induct |> full_simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt) |> full_simplify (put_simpset HOL_basic_ss ctxt addsimps all_f_defs) fun project rule (MutualPart {cargTs, i, ...}) k = let val afs = map_index (fn (j,T) => Free ("a" ^ string_of_int (j + k), T)) cargTs (* FIXME! *) val inj = Sum_Tree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs) in (rule |> Thm.forall_elim (cert inj) |> full_simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt) |> fold_rev (Thm.forall_intr o cert) (afs @ newPs), k + length cargTs) end in fst (fold_map (project induct_inst) parts 0) end fun forall_elim s \<^Const_>\Pure.all _ for \Abs (_, _, t)\\ = subst_bound (s, t) | forall_elim _ t = t val forall_elim_list = fold forall_elim fun split_conj_thm th = (split_conj_thm (th RS conjunct1)) @ (split_conj_thm (th RS conjunct2)) handle THM _ => [th]; fun prove_eqvt ctxt fs argTss eqvts_thms induct_thms = let fun aux argTs s = argTs |> map (pair s) |> Variable.variant_frees ctxt fs val argss' = map2 aux argTss (Name.invent (Variable.names_of ctxt) "" (length fs)) val argss = (map o map) Free argss' val arg_namess = (map o map) fst argss' val insts = (map o map) SOME arg_namess val ([p_name], ctxt') = Variable.variant_fixes ["p"] ctxt val p = Free (p_name, \<^Type>\perm\) (* extracting the acc-premises from the induction theorems *) val acc_prems = map Thm.prop_of induct_thms |> map2 forall_elim_list argss |> map (strip_qnt_body @{const_name Pure.all}) |> map (curry Logic.nth_prem 1) |> map HOLogic.dest_Trueprop fun mk_goal acc_prem (f, args) = let val goal_lhs = mk_perm p (list_comb (f, args)) val goal_rhs = list_comb (f, map (mk_perm p) args) in HOLogic.mk_imp (acc_prem, HOLogic.mk_eq (goal_lhs, goal_rhs)) end val goal = fold_conj_balanced (map2 mk_goal acc_prems (fs ~~ argss)) |> HOLogic.mk_Trueprop val induct_thm = case induct_thms of [thm] => thm |> Variable.gen_all ctxt' |> Thm.permute_prems 0 1 |> (fn thm => atomize_rule ctxt' (length (Thm.prems_of thm) - 1) thm) | thms => thms |> map (Variable.gen_all ctxt') |> map (Rule_Cases.add_consumes 1) |> snd o Rule_Cases.strict_mutual_rule ctxt' |> atomize_concl ctxt' fun tac ctxt thm = resolve_tac ctxt [Variable.gen_all ctxt thm] THEN_ALL_NEW assume_tac ctxt in Goal.prove ctxt' (flat arg_namess) [] goal - (fn {context = ctxt'', ...} => - HEADGOAL (DETERM o (resolve_tac ctxt'' [induct_thm]) THEN' - RANGE (map (tac ctxt'') eqvts_thms))) + (fn {context = goal_ctxt, ...} => + HEADGOAL (DETERM o (resolve_tac goal_ctxt [induct_thm]) THEN' + RANGE (map (tac goal_ctxt) eqvts_thms))) |> singleton (Proof_Context.export ctxt' ctxt) |> split_conj_thm |> map (fn th => th RS mp) end fun mk_partial_rules_mutual ctxt inner_cont (m as Mutual {parts, fqgars, ...}) proof = let val result = inner_cont proof val NominalFunctionResult {G, R, cases, psimps, simple_pinducts=[simple_pinduct], termination, domintros, eqvts=[eqvt],...} = result val (all_f_defs, fs) = map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} => (mk_applied_form ctxt cargTs (Thm.symmetric f_def), f)) parts |> split_list val all_orig_fdefs = map (fn MutualPart {f_defthm = SOME f_def, ...} => f_def) parts val cargTss = map (fn MutualPart {f = SOME f, cargTs, ...} => cargTs) parts fun mk_mpsimp fqgar sum_psimp = in_context ctxt fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp fun mk_meqvts fqgar sum_psimp = in_context ctxt fqgar (recover_mutual_eqvt eqvt all_orig_fdefs parts) sum_psimp val rew_simpset = put_simpset HOL_basic_ss ctxt addsimps all_f_defs val mpsimps = map2 mk_mpsimp fqgars psimps val minducts = mutual_induct_rules ctxt simple_pinduct all_f_defs m val mtermination = full_simplify rew_simpset termination val mdomintros = Option.map (map (full_simplify rew_simpset)) domintros val meqvts = map2 mk_meqvts fqgars psimps val meqvt_funs = prove_eqvt ctxt fs cargTss meqvts minducts in NominalFunctionResult { fs=fs, G=G, R=R, psimps=mpsimps, simple_pinducts=minducts, cases=cases, termination=mtermination, domintros=mdomintros, eqvts=meqvt_funs } end (* nominal *) fun subst_all s (Q $ Abs(_, _, t)) = let val vs = map Free (Term.add_frees s []) in fold Logic.all vs (subst_bound (s, t)) end fun mk_comp_dummy t s = Const (@{const_name comp}, dummyT) $ t $ s fun all v t = let val T = Term.fastype_of v in Logic.all_const T $ absdummy T (abstract_over (v, t)) end (* nominal *) fun prepare_nominal_function_mutual config defname fixes eqss lthy = let val mutual as Mutual {fsum_var=(n, T), qglrs, ...} = analyze_eqs lthy defname (map fst fixes) (map Envir.beta_eta_contract eqss) - val ((fsum, G, GIntro_thms, G_induct, goalstate, cont), lthy') = + val ((fsum, G, GIntro_thms, G_induct, goalstate, cont), lthy1) = Nominal_Function_Core.prepare_nominal_function config defname [((n, T), NoSyn)] qglrs lthy - val (mutual' as Mutual {n', parts, ST, RST, ...}, lthy'') = define_projections fixes mutual fsum lthy' + val (mutual' as Mutual {n', parts, ST, RST, ...}, lthy2) = define_projections fixes mutual fsum lthy1 (* defining the auxiliary graph *) fun mk_cases (MutualPart {i', fvar as (n, T), ...}) = let val (tys, ty) = strip_type T val fun_var = Free (n ^ "_aux", HOLogic.mk_tupleT tys --> ty) val inj_fun = absdummy dummyT (Sum_Tree.mk_inj RST n' i' (Bound 0)) in - Syntax.check_term lthy'' (mk_comp_dummy inj_fun fun_var) + Syntax.check_term lthy2 (mk_comp_dummy inj_fun fun_var) end val case_sum_exp = map mk_cases parts |> Sum_Tree.mk_sumcases RST val (G_name, G_type) = dest_Free G val G_name_aux = G_name ^ "_aux" val subst = [(G, Free (G_name_aux, G_type))] val GIntros_aux = GIntro_thms |> map Thm.prop_of |> map (Term.subst_free subst) |> map (subst_all case_sum_exp) - val ((G_aux, GIntro_aux_thms, _, G_aux_induct), lthy''') = - Nominal_Function_Core.inductive_def ((Binding.name G_name_aux, G_type), NoSyn) GIntros_aux lthy'' + val ((G_aux, GIntro_aux_thms, _, G_aux_induct), lthy3) = + Nominal_Function_Core.inductive_def ((Binding.name G_name_aux, G_type), NoSyn) GIntros_aux lthy2 - fun mutual_cont ctxt = mk_partial_rules_mutual lthy''' (cont ctxt) mutual' + fun mutual_cont ctxt = mk_partial_rules_mutual lthy3 (cont ctxt) mutual' (* proof of equivalence between graph and auxiliary graph *) val x = Var(("x", 0), ST) val y = Var(("y", 1), RST) val G_aux_prem = HOLogic.mk_Trueprop (G_aux $ x $ y) val G_prem = HOLogic.mk_Trueprop (G $ x $ y) fun mk_inj_goal (MutualPart {i', ...}) = let val injs = Sum_Tree.mk_inj ST n' i' (Bound 0) val projs = y |> Sum_Tree.mk_proj RST n' i' |> Sum_Tree.mk_inj RST n' i' in Const (@{const_name "All"}, dummyT) $ absdummy dummyT (HOLogic.mk_imp (HOLogic.mk_eq(x, injs), HOLogic.mk_eq(projs, y))) end val goal_inj = Logic.mk_implies (G_aux_prem, HOLogic.mk_Trueprop (fold_conj (map mk_inj_goal parts))) |> all x |> all y - |> Syntax.check_term lthy''' + |> Syntax.check_term lthy3 val goal_iff1 = Logic.mk_implies (G_aux_prem, G_prem) |> all x |> all y val goal_iff2 = Logic.mk_implies (G_prem, G_aux_prem) |> all x |> all y val simp_thms = @{thms sum.sel sum.inject sum.case sum.distinct o_apply} - val simpset0 = put_simpset HOL_basic_ss lthy''' addsimps simp_thms - val simpset1 = put_simpset HOL_ss lthy''' addsimps simp_thms - - val inj_thm = Goal.prove lthy''' [] [] goal_inj - (K (HEADGOAL (DETERM o eresolve_tac lthy''' [G_aux_induct] - THEN_ALL_NEW asm_simp_tac simpset1))) - - fun aux_tac thm = - resolve_tac lthy''' [Variable.gen_all lthy''' thm] THEN_ALL_NEW - asm_full_simp_tac (simpset1 addsimps [inj_thm]) + fun simpset0 goal_ctxt = put_simpset HOL_basic_ss goal_ctxt addsimps simp_thms + fun simpset1 goal_ctxt = put_simpset HOL_ss goal_ctxt addsimps simp_thms - val iff1_thm = Goal.prove lthy''' [] [] goal_iff1 - (K (HEADGOAL (DETERM o eresolve_tac lthy''' [G_aux_induct] - THEN' RANGE (map aux_tac GIntro_thms)))) - |> Variable.gen_all lthy''' - val iff2_thm = Goal.prove lthy''' [] [] goal_iff2 - (K (HEADGOAL (DETERM o eresolve_tac lthy''' [G_induct] THEN' RANGE - (map (aux_tac o simplify simpset0) GIntro_aux_thms)))) - |> Variable.gen_all lthy''' + val inj_thm = Goal.prove lthy3 [] [] goal_inj + (fn {context = goal_ctxt, ...} => + HEADGOAL (DETERM o eresolve_tac goal_ctxt [G_aux_induct] + THEN_ALL_NEW asm_simp_tac (simpset1 goal_ctxt))) - val iff_thm = Goal.prove lthy''' [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (G, G_aux))) - (K (HEADGOAL (EVERY' ((map (resolve_tac lthy''' o single) @{thms ext ext iffI}) @ - [eresolve_tac lthy''' [iff2_thm], eresolve_tac lthy''' [iff1_thm]])))) + fun aux_tac goal_ctxt thm = + resolve_tac goal_ctxt [Variable.gen_all goal_ctxt thm] THEN_ALL_NEW + asm_full_simp_tac (simpset1 goal_ctxt addsimps [inj_thm]) - val tac = HEADGOAL (simp_tac (put_simpset HOL_basic_ss lthy''' addsimps [iff_thm])) + val iff1_thm = Goal.prove lthy3 [] [] goal_iff1 + (fn {context = goal_ctxt, ...} => + HEADGOAL (DETERM o eresolve_tac goal_ctxt [G_aux_induct] + THEN' RANGE (map (aux_tac goal_ctxt) GIntro_thms))) + |> Variable.gen_all lthy3 + val iff2_thm = Goal.prove lthy3 [] [] goal_iff2 + (fn {context = goal_ctxt, ...} => + HEADGOAL (DETERM o eresolve_tac lthy3 [G_induct] + THEN' RANGE (map (aux_tac goal_ctxt o simplify (simpset0 goal_ctxt)) GIntro_aux_thms))) + |> Variable.gen_all lthy3 + + val iff_thm = Goal.prove lthy3 [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (G, G_aux))) + (fn {context = goal_ctxt, ...} => + HEADGOAL (EVERY' ((map (resolve_tac goal_ctxt o single) @{thms ext ext iffI}) @ + [eresolve_tac goal_ctxt [iff2_thm], eresolve_tac goal_ctxt [iff1_thm]]))) + + val tac = HEADGOAL (simp_tac (put_simpset HOL_basic_ss lthy3 addsimps [iff_thm])) val goalstate' = case (SINGLE tac) goalstate of NONE => error "auxiliary equivalence proof failed" | SOME st => st in - ((goalstate', mutual_cont), lthy''') + ((goalstate', mutual_cont), lthy3) end end diff --git a/thys/Nominal2/nominal_thmdecls.ML b/thys/Nominal2/nominal_thmdecls.ML --- a/thys/Nominal2/nominal_thmdecls.ML +++ b/thys/Nominal2/nominal_thmdecls.ML @@ -1,328 +1,328 @@ (* Title: nominal_thmdecls.ML Author: Christian Urban Author: Tjark Weber Infrastructure for the lemma collections "eqvts", "eqvts_raw". Provides the attributes [eqvt] and [eqvt_raw], and the theorem lists "eqvts" and "eqvts_raw". The [eqvt] attribute expects a theorem of the form ?p \ (c ?x1 ?x2 ...) = c (?p \ ?x1) (?p \ ?x2) ... (1) or, if c is a relation with arity >= 1, of the form c ?x1 ?x2 ... ==> c (?p \ ?x1) (?p \ ?x2) ... (2) [eqvt] will store this theorem in the form (1) or, if c is a relation with arity >= 1, in the form c (?p \ ?x1) (?p \ ?x2) ... = c ?x1 ?x2 ... (3) in "eqvts". (The orientation of (3) was chosen because Isabelle's simplifier uses equations from left to right.) [eqvt] will also derive and store the theorem ?p \ c == c (4) in "eqvts_raw". (1)-(4) are all logically equivalent. We consider (1) and (2) to be more end-user friendly, i.e., slightly more natural to understand and prove, while (3) and (4) make the rewriting system for equivariance more predictable and less prone to looping in Isabelle. The [eqvt_raw] attribute expects a theorem of the form (4), and merely stores it in "eqvts_raw". [eqvt_raw] is provided because certain equivariance theorems would lead to looping when used for simplification in the form (1): notably, equivariance of permute (infix \), i.e., ?p \ (?q \ ?x) = (?p \ ?q) \ (?p \ ?x). To support binders such as All/Ex/Ball/Bex etc., which are typically applied to abstractions, argument terms ?xi (as well as permuted arguments ?p \ ?xi) in (1)-(3) need not be eta- contracted, i.e., they may be of the form "%z. ?xi z" or "%z. (?p \ ?x) z", respectively. For convenience, argument terms ?xi (as well as permuted arguments ?p \ ?xi) in (1)-(3) may actually be tuples, e.g., "(?xi, ?xj)" or "(?p \ ?xi, ?p \ ?xj)", respectively. In (1)-(4), "c" is either a (global) constant or a locally fixed parameter, e.g., of a locale or type class. *) signature NOMINAL_THMDECLS = sig val eqvt_add: attribute val eqvt_del: attribute val eqvt_raw_add: attribute val eqvt_raw_del: attribute 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.item_net; val extend = I; val merge = Item_Net.merge); (* EqvtRawData is implemented with a Termtab (rather than an Item_Net) so that we can efficiently decide whether a given constant has a corresponding equivariance theorem stored, cf. the function is_eqvt. *) 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 _ = Theory.setup (Global_Theory.add_thms_dynamic (@{binding "eqvts"}, eqvts) #> Global_Theory.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw)) val get_eqvts_thms = eqvts o Context.Proof val get_eqvts_raw_thms = eqvts_raw o Context.Proof (** raw equivariance lemmas **) (* Returns true iff an equivariance lemma exists in "eqvts_raw" for a given term. *) val is_eqvt = Termtab.defined o EqvtRawData.get o Context.Proof (* Returns c if thm is of the form (4), raises an error otherwise. *) fun key_of_raw_thm context thm = let fun error_msg () = error ("Theorem must be of the form \"?p \ c \ c\", with c a constant or fixed parameter:\n" ^ Syntax.string_of_term (Context.proof_of context) (Thm.prop_of thm)) in case Thm.prop_of thm of \<^Const_>\Pure.eq _ for \<^Const_>\permute _ for p c\ c'\ => if is_Var p andalso is_fixed (Context.proof_of context) c andalso c aconv c' then c else error_msg () | _ => error_msg () end fun add_raw_thm thm context = let val c = key_of_raw_thm context thm in if Termtab.defined (EqvtRawData.get context) c then warning ("Replacing existing raw equivariance theorem for \"" ^ Syntax.string_of_term (Context.proof_of context) c ^ "\".") else (); EqvtRawData.map (Termtab.update (c, thm)) context end fun del_raw_thm thm context = let val c = key_of_raw_thm context thm in if Termtab.defined (EqvtRawData.get context) c then EqvtRawData.map (Termtab.delete c) context else ( warning ("Cannot delete non-existing raw equivariance theorem for \"" ^ Syntax.string_of_term (Context.proof_of context) c ^ "\"."); context ) end (** adding/deleting lemmas to/from "eqvts" **) fun add_thm thm context = ( if Item_Net.member (EqvtData.get context) thm then warning ("Theorem already declared as equivariant:\n" ^ Syntax.string_of_term (Context.proof_of context) (Thm.prop_of thm)) else (); EqvtData.map (Item_Net.update thm) context ) fun del_thm thm context = ( if Item_Net.member (EqvtData.get context) thm then EqvtData.map (Item_Net.remove thm) context else ( warning ("Cannot delete non-existing equivariance theorem:\n" ^ Syntax.string_of_term (Context.proof_of context) (Thm.prop_of thm)); context ) ) (** transformation of equivariance lemmas **) (* Transforms a theorem of the form (1) into the form (4). *) local fun tac ctxt thm = let val ss_thms = @{thms "permute_minus_cancel" "permute_prod.simps" "split_paired_all"} in REPEAT o FIRST' [CHANGED o simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss_thms), resolve_tac ctxt [thm RS @{thm trans}], resolve_tac ctxt @{thms trans[OF "permute_fun_def"]} THEN' resolve_tac ctxt @{thms ext}] end in fun thm_4_of_1 ctxt thm = let val (p, c) = thm |> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst |> dest_perm ||> fst o (fixed_nonfixed_args ctxt) 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 {context, ...} => tac context thm 1) + Goal.prove ctxt [] [] goal' (fn {context = goal_ctxt, ...} => tac goal_ctxt thm 1) |> singleton (Proof_Context.export ctxt' ctxt) |> (fn th => th RS @{thm "eq_reflection"}) |> zero_var_indexes end handle TERM _ => raise THM ("thm_4_of_1", 0, [thm]) end (* local *) (* Transforms a theorem of the form (2) into the form (1). *) local fun tac ctxt thm thm' = let val ss_thms = @{thms "permute_minus_cancel"(2)} in EVERY' [resolve_tac ctxt @{thms iffI}, dresolve_tac ctxt @{thms permute_boolE}, resolve_tac ctxt [thm], assume_tac ctxt, resolve_tac ctxt @{thms permute_boolI}, dresolve_tac ctxt [thm'], full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss_thms)] end in fun thm_1_of_2 ctxt thm = let val (prem, concl) = thm |> Thm.prop_of |> Logic.dest_implies |> apply2 HOLogic.dest_Trueprop (* since argument terms "?p \ ?x1" may actually be eta-expanded or tuples, we need the following function to find ?p *) fun find_perm \<^Const_>\permute _ for \p as Var _\ _\ = p | find_perm \<^Const_>\Pair _ _ for x _\ = find_perm x | find_perm (Abs (_, _, body)) = find_perm body | find_perm _ = raise THM ("thm_3_of_2", 0, [thm]) val p = concl |> dest_comb |> snd |> find_perm val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p prem, concl)) val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt val thm' = infer_instantiate ctxt' [(#1 (dest_Var p), Thm.cterm_of ctxt' (mk_minus p'))] thm in - Goal.prove ctxt' [] [] goal' (fn {context = ctxt'', ...} => tac ctxt'' thm thm' 1) + Goal.prove ctxt' [] [] goal' (fn {context = goal_ctxt, ...} => tac goal_ctxt thm thm' 1) |> singleton (Proof_Context.export ctxt' ctxt) end handle TERM _ => raise THM ("thm_1_of_2", 0, [thm]) end (* local *) (* Transforms a theorem of the form (1) into the form (3). *) fun thm_3_of_1 _ thm = (thm RS (@{thm "permute_bool_def"} RS @{thm "sym"} RS @{thm "trans"}) RS @{thm "sym"}) |> zero_var_indexes local val msg = cat_lines ["Equivariance theorem must be of the form", " ?p \ (c ?x1 ?x2 ...) = c (?p \ ?x1) (?p \ ?x2) ...", "or, if c is a relation with arity >= 1, of the form", " c ?x1 ?x2 ... ==> c (?p \ ?x1) (?p \ ?x2) ..."] in (* Transforms a theorem of the form (1) or (2) into the form (4). *) fun eqvt_transform ctxt thm = (case Thm.prop_of thm of \<^Const_>\Trueprop for _\ => thm_4_of_1 ctxt thm | \<^Const_>\Pure.imp for _ _\ => thm_4_of_1 ctxt (thm_1_of_2 ctxt thm) | _ => error msg) handle THM _ => error msg (* Transforms a theorem of the form (1) into theorems of the form (1) (or, if c is a relation with arity >= 1, of the form (3)) and (4); transforms a theorem of the form (2) into theorems of the form (3) and (4). *) fun eqvt_and_raw_transform ctxt thm = (case Thm.prop_of thm of \<^Const_>\Trueprop for \<^Const_>\HOL.eq _ for _ c_args\\ => let val th' = if fastype_of c_args = @{typ "bool"} andalso (not o null) (snd (fixed_nonfixed_args ctxt c_args)) then thm_3_of_1 ctxt thm else thm in (th', thm_4_of_1 ctxt thm) end | \<^Const_>\Pure.imp for _ _\ => let val th1 = thm_1_of_2 ctxt thm in (thm_3_of_1 ctxt th1, thm_4_of_1 ctxt th1) end | _ => error msg) handle THM _ => error msg end (* local *) (** attributes **) val eqvt_raw_add = Thm.declaration_attribute add_raw_thm val eqvt_raw_del = Thm.declaration_attribute del_raw_thm fun eqvt_add_or_del eqvt_fn raw_fn = Thm.declaration_attribute (fn thm => fn context => let val (eqvt, raw) = eqvt_and_raw_transform (Context.proof_of context) thm in context |> eqvt_fn eqvt |> raw_fn raw end) val eqvt_add = eqvt_add_or_del add_thm add_raw_thm val eqvt_del = eqvt_add_or_del del_thm del_raw_thm val _ = Theory.setup (Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) "Declaration of equivariance lemmas - they will automatically be brought into the form ?p \ c \ c" #> Attrib.setup @{binding "eqvt_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_del) "Declaration of raw equivariance lemmas - no transformation is performed") end;