# HG changeset patch # User Cezary Kaliszyk # Date 1272268873 -7200 # Node ID 27cdc0a3a7631e2a977be87d3fcefb00bee0de21 # Parent a0c7290a4e2770b4c089902cadbdf75c6a836c05# Parent 7de54c9f81ac880f254c398369595a962987f7cc merge ??? diff -r a0c7290a4e27 -r 27cdc0a3a763 Attic/FIXME-TODO --- a/Attic/FIXME-TODO Wed Apr 21 12:25:52 2010 +0200 +++ b/Attic/FIXME-TODO Mon Apr 26 10:01:13 2010 +0200 @@ -67,6 +67,3 @@ That means "qconst :: qty" is not read as a term, but as two entities. - -- Restrict automatic translation to particular quotient types - diff -r a0c7290a4e27 -r 27cdc0a3a763 Attic/Prove.thy --- a/Attic/Prove.thy Wed Apr 21 12:25:52 2010 +0200 +++ b/Attic/Prove.thy Mon Apr 26 10:01:13 2010 +0200 @@ -15,7 +15,7 @@ let val trm = ML_Context.evaluate lthy true ("r", r) txt in - Proof.theorem_i NONE (after_qed name_spec) [[(trm,[])]] lthy + Proof.theorem NONE (after_qed name_spec) [[(trm,[])]] lthy end val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source diff -r a0c7290a4e27 -r 27cdc0a3a763 Attic/Quot/Examples/FSet3.thy --- a/Attic/Quot/Examples/FSet3.thy Wed Apr 21 12:25:52 2010 +0200 +++ b/Attic/Quot/Examples/FSet3.thy Mon Apr 26 10:01:13 2010 +0200 @@ -2,154 +2,6 @@ imports "../../../Nominal/FSet" begin -notation - list_eq (infix "\" 50) - -lemma fset_exhaust[case_names fempty finsert, cases type: fset]: - shows "\S = {||} \ P; \x S'. S = finsert x S' \ P\ \ P" -by (lifting list.exhaust) - -(* PROBLEM: these lemmas needs to be restated, since *) -(* concat.simps(1) and concat.simps(2) contain the *) -(* type variables ?'a1.0 (which are turned into frees *) -(* 'a_1 *) - -lemma concat1: - shows "concat [] \ []" -by (simp) - -lemma concat2: - shows "concat (x # xs) \ x @ concat xs" -by (simp) - -lemma concat_rsp: - "\list_rel op \ x x'; x' \ y'; list_rel op \ y' y\ \ concat x \ concat y" - apply (induct x y arbitrary: x' y' rule: list_induct2') - apply simp - defer defer - apply (simp only: concat.simps) - sorry - -lemma [quot_respect]: - shows "(list_rel op \ OOO op \ ===> op \) concat concat" - apply (simp only: fun_rel_def) - apply clarify - apply (rule concat_rsp) - apply assumption+ - done - -lemma nil_rsp2[quot_respect]: "(list_rel op \ OOO op \) [] []" - by (metis nil_rsp list_rel.simps(1) pred_compI) - -lemma set_in_eq: "(\e. ((e \ A) \ (e \ B))) \ A = B" - apply (rule eq_reflection) - apply auto - done - -lemma map_rel_cong: "b \ ba \ map f b \ map f ba" - unfolding list_eq.simps - apply(simp only: set_map set_in_eq) - done - -lemma quotient_compose_list_pre: - "(list_rel op \ OOO op \) r s = - ((list_rel op \ OOO op \) r r \ (list_rel op \ OOO op \) s s \ - abs_fset (map abs_fset r) = abs_fset (map abs_fset s))" - apply rule - apply rule - apply rule - apply (rule list_rel_refl) - apply (metis equivp_def fset_equivp) - apply rule - apply (rule equivp_reflp[OF fset_equivp]) - apply (rule list_rel_refl) - apply (metis equivp_def fset_equivp) - apply(rule) - apply rule - apply (rule list_rel_refl) - apply (metis equivp_def fset_equivp) - apply rule - apply (rule equivp_reflp[OF fset_equivp]) - apply (rule list_rel_refl) - apply (metis equivp_def fset_equivp) - apply (subgoal_tac "map abs_fset r \ map abs_fset s") - apply (metis Quotient_rel[OF Quotient_fset]) - apply (auto simp only:)[1] - apply (subgoal_tac "map abs_fset r = map abs_fset b") - prefer 2 - apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]]) - apply (subgoal_tac "map abs_fset s = map abs_fset ba") - prefer 2 - apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]]) - apply (simp only: map_rel_cong) - apply rule - apply (rule rep_abs_rsp[of "list_rel op \" "map abs_fset"]) - apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) - apply (rule list_rel_refl) - apply (metis equivp_def fset_equivp) - apply rule - prefer 2 - apply (rule rep_abs_rsp_left[of "list_rel op \" "map abs_fset"]) - apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) - apply (rule list_rel_refl) - apply (metis equivp_def fset_equivp) - apply (erule conjE)+ - apply (subgoal_tac "map abs_fset r \ map abs_fset s") - prefer 2 - apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp) - apply (rule map_rel_cong) - apply (assumption) - done - -lemma quotient_compose_list[quot_thm]: - shows "Quotient ((list_rel op \) OOO (op \)) - (abs_fset \ (map abs_fset)) ((map rep_fset) \ rep_fset)" - unfolding Quotient_def comp_def - apply (rule)+ - apply (simp add: abs_o_rep[OF Quotient_fset] id_simps Quotient_abs_rep[OF Quotient_fset]) - apply (rule) - apply (rule) - apply (rule) - apply (rule list_rel_refl) - apply (metis equivp_def fset_equivp) - apply (rule) - apply (rule equivp_reflp[OF fset_equivp]) - apply (rule list_rel_refl) - apply (metis equivp_def fset_equivp) - apply rule - apply rule - apply (rule quotient_compose_list_pre) - done - -lemma fconcat_empty: - shows "fconcat {||} = {||}" - apply(lifting concat1) - apply(cleaning) - apply(simp add: comp_def bot_fset_def) - done - -lemma insert_rsp2[quot_respect]: - "(op \ ===> list_rel op \ OOO op \ ===> list_rel op \ OOO op \) op # op #" - apply auto - apply (simp add: set_in_eq) - apply (rule_tac b="x # b" in pred_compI) - apply auto - apply (rule_tac b="x # ba" in pred_compI) - apply auto - done - -lemma append_rsp[quot_respect]: - "(op \ ===> op \ ===> op \) op @ op @" - by (auto) - -lemma fconcat_insert: - shows "fconcat (finsert x S) = x |\| fconcat S" - apply(lifting concat2) - apply(cleaning) - apply (simp add: finsert_def fconcat_def comp_def) - apply cleaning - done - (* TBD *) text {* syntax for fset comprehensions (adapted from lists) *} diff -r a0c7290a4e27 -r 27cdc0a3a763 Attic/Quot/Examples/IntEx.thy --- a/Attic/Quot/Examples/IntEx.thy Wed Apr 21 12:25:52 2010 +0200 +++ b/Attic/Quot/Examples/IntEx.thy Mon Apr 26 10:01:13 2010 +0200 @@ -165,27 +165,6 @@ apply(lifting plus_assoc_pre) done -lemma int_induct_raw: - assumes a: "P (0::nat, 0)" - and b: "\i. P i \ P (my_plus i (1,0))" - and c: "\i. P i \ P (my_plus i (my_neg (1,0)))" - shows "P x" - apply(case_tac x) apply(simp) - apply(rule_tac x="b" in spec) - apply(rule_tac Nat.induct) - apply(rule allI) - apply(rule_tac Nat.induct) - using a b c apply(auto) - done - -lemma int_induct: - assumes a: "P ZERO" - and b: "\i. P i \ P (PLUS i ONE)" - and c: "\i. P i \ P (PLUS i (NEG ONE))" - shows "P x" - using a b c - by (lifting int_induct_raw) - lemma ex1tst: "Bex1_rel (op \) (\x :: nat \ nat. x \ x)" sorry diff -r a0c7290a4e27 -r 27cdc0a3a763 Attic/Quot/Examples/IntEx2.thy --- a/Attic/Quot/Examples/IntEx2.thy Wed Apr 21 12:25:52 2010 +0200 +++ b/Attic/Quot/Examples/IntEx2.thy Mon Apr 26 10:01:13 2010 +0200 @@ -76,7 +76,7 @@ lemma plus_raw_rsp[quot_respect]: shows "(op \ ===> op \ ===> op \) plus_raw plus_raw" -by auto + by auto lemma uminus_raw_rsp[quot_respect]: shows "(op \ ===> op \) uminus_raw uminus_raw" @@ -85,70 +85,70 @@ lemma mult_raw_fst: assumes a: "x \ z" shows "mult_raw x y \ mult_raw z y" -using a -apply(cases x, cases y, cases z) -apply(auto simp add: mult_raw.simps intrel.simps) -apply(rename_tac u v w x y z) -apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x") -apply(simp add: mult_ac) -apply(simp add: add_mult_distrib [symmetric]) -done + using a + apply(cases x, cases y, cases z) + apply(auto simp add: mult_raw.simps intrel.simps) + apply(rename_tac u v w x y z) + apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x") + apply(simp add: mult_ac) + apply(simp add: add_mult_distrib [symmetric]) + done lemma mult_raw_snd: assumes a: "x \ z" shows "mult_raw y x \ mult_raw y z" -using a -apply(cases x, cases y, cases z) -apply(auto simp add: mult_raw.simps intrel.simps) -apply(rename_tac u v w x y z) -apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x") -apply(simp add: mult_ac) -apply(simp add: add_mult_distrib [symmetric]) -done + using a + apply(cases x, cases y, cases z) + apply(auto simp add: mult_raw.simps intrel.simps) + apply(rename_tac u v w x y z) + apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x") + apply(simp add: mult_ac) + apply(simp add: add_mult_distrib [symmetric]) + done lemma mult_raw_rsp[quot_respect]: shows "(op \ ===> op \ ===> op \) mult_raw mult_raw" -apply(simp only: fun_rel_def) -apply(rule allI | rule impI)+ -apply(rule equivp_transp[OF int_equivp]) -apply(rule mult_raw_fst) -apply(assumption) -apply(rule mult_raw_snd) -apply(assumption) -done + apply(simp only: fun_rel_def) + apply(rule allI | rule impI)+ + apply(rule equivp_transp[OF int_equivp]) + apply(rule mult_raw_fst) + apply(assumption) + apply(rule mult_raw_snd) + apply(assumption) + done lemma le_raw_rsp[quot_respect]: shows "(op \ ===> op \ ===> op =) le_raw le_raw" -by auto + by auto lemma plus_assoc_raw: shows "plus_raw (plus_raw i j) k \ plus_raw i (plus_raw j k)" -by (cases i, cases j, cases k) (simp) + by (cases i, cases j, cases k) (simp) lemma plus_sym_raw: shows "plus_raw i j \ plus_raw j i" -by (cases i, cases j) (simp) + by (cases i, cases j) (simp) lemma plus_zero_raw: shows "plus_raw (0, 0) i \ i" -by (cases i) (simp) + by (cases i) (simp) lemma plus_minus_zero_raw: shows "plus_raw (uminus_raw i) i \ (0, 0)" -by (cases i) (simp) + by (cases i) (simp) lemma times_assoc_raw: shows "mult_raw (mult_raw i j) k \ mult_raw i (mult_raw j k)" -by (cases i, cases j, cases k) - (simp add: algebra_simps) + by (cases i, cases j, cases k) + (simp add: algebra_simps) lemma times_sym_raw: shows "mult_raw i j \ mult_raw j i" -by (cases i, cases j) (simp add: algebra_simps) + by (cases i, cases j) (simp add: algebra_simps) lemma times_one_raw: shows "mult_raw (1, 0) i \ i" -by (cases i) (simp) + by (cases i) (simp) lemma times_plus_comm_raw: shows "mult_raw (plus_raw i j) k \ plus_raw (mult_raw i k) (mult_raw j k)" @@ -189,19 +189,19 @@ lemma plus_raw_rsp_aux: assumes a: "a \ b" "c \ d" shows "plus_raw a c \ plus_raw b d" -using a -by (cases a, cases b, cases c, cases d) - (simp) + using a + by (cases a, cases b, cases c, cases d) + (simp) lemma add: - "(abs_int (x,y)) + (abs_int (u,v)) = - (abs_int (x + u, y + v))" -apply(simp add: plus_int_def id_simps) -apply(fold plus_raw.simps) -apply(rule Quotient_rel_abs[OF Quotient_int]) -apply(rule plus_raw_rsp_aux) -apply(simp_all add: rep_abs_rsp_left[OF Quotient_int]) -done + "(abs_int (x,y)) + (abs_int (u,v)) = + (abs_int (x + u, y + v))" + apply(simp add: plus_int_def id_simps) + apply(fold plus_raw.simps) + apply(rule Quotient_rel_abs[OF Quotient_int]) + apply(rule plus_raw_rsp_aux) + apply(simp_all add: rep_abs_rsp_left[OF Quotient_int]) + done definition int_of_nat_raw: "int_of_nat_raw m = (m :: nat, 0 :: nat)" @@ -211,30 +211,29 @@ lemma[quot_respect]: shows "(op = ===> op \) int_of_nat_raw int_of_nat_raw" -by (simp add: equivp_reflp[OF int_equivp]) + by (simp add: equivp_reflp[OF int_equivp]) lemma int_of_nat: shows "of_nat m = int_of_nat m" -apply (induct m) -apply (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add) -done + by (induct m) + (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add) lemma le_antisym_raw: shows "le_raw i j \ le_raw j i \ i \ j" -by (cases i, cases j) (simp) + by (cases i, cases j) (simp) lemma le_refl_raw: shows "le_raw i i" -by (cases i) (simp) + by (cases i) (simp) lemma le_trans_raw: shows "le_raw i j \ le_raw j k \ le_raw i k" -by (cases i, cases j, cases k) (simp) + by (cases i, cases j, cases k) (simp) lemma le_cases_raw: shows "le_raw i j \ le_raw j i" -by (cases i, cases j) - (simp add: linorder_linear) + by (cases i, cases j) + (simp add: linorder_linear) instance int :: linorder proof @@ -268,8 +267,7 @@ lemma le_plus_raw: shows "le_raw i j \ le_raw (plus_raw k i) (plus_raw k j)" -by (cases i, cases j, cases k) (simp) - + by (cases i, cases j, cases k) (simp) instance int :: ordered_cancel_ab_semigroup_add proof @@ -285,21 +283,21 @@ fixes i j::int and k::nat shows "i < j \ 0 < k \ of_nat k * i < of_nat k * j" -apply(induct "k") -apply(simp) -apply(case_tac "k = 0") -apply(simp_all add: left_distrib add_strict_mono) -done + apply(induct "k") + apply(simp) + apply(case_tac "k = 0") + apply(simp_all add: left_distrib add_strict_mono) + done lemma zero_le_imp_eq_int_raw: fixes k::"(nat \ nat)" shows "less_raw (0, 0) k \ (\n > 0. k \ int_of_nat_raw n)" -apply(cases k) -apply(simp add:int_of_nat_raw) -apply(auto) -apply(rule_tac i="b" and j="a" in less_Suc_induct) -apply(auto) -done + apply(cases k) + apply(simp add:int_of_nat_raw) + apply(auto) + apply(rule_tac i="b" and j="a" in less_Suc_induct) + apply(auto) + done lemma zero_le_imp_eq_int: fixes k::int @@ -311,11 +309,8 @@ fixes i j k::int assumes a: "i < j" "0 < k" shows "k * i < k * j" -using a -using a -apply(drule_tac zero_le_imp_eq_int) -apply(auto simp add: zmult_zless_mono2_lemma) -done + using a + by (drule_tac zero_le_imp_eq_int) (auto simp add: zmult_zless_mono2_lemma) text{*The integers form an ordered integral domain*} instance int :: linordered_idom @@ -335,6 +330,31 @@ left_diff_distrib [of "z1::int" "z2" "w", standard] right_diff_distrib [of "w::int" "z1" "z2", standard] +lemma int_induct_raw: + assumes a: "P (0::nat, 0)" + and b: "\i. P i \ P (plus_raw i (1, 0))" + and c: "\i. P i \ P (plus_raw i (uminus_raw (1, 0)))" + shows "P x" +proof (cases x, clarify) + fix a b + show "P (a, b)" + proof (induct a arbitrary: b rule: Nat.induct) + case zero + show "P (0, b)" using assms by (induct b) auto + next + case (Suc n) + then show ?case using assms by auto + qed +qed + +lemma int_induct: + fixes x :: int + assumes a: "P 0" + and b: "\i. P i \ P (i + 1)" + and c: "\i. P i \ P (i - 1)" + shows "P x" + using a b c unfolding minus_int_def + by (lifting int_induct_raw) subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*} diff -r a0c7290a4e27 -r 27cdc0a3a763 Nominal-General/Nominal2_Atoms.thy --- a/Nominal-General/Nominal2_Atoms.thy Wed Apr 21 12:25:52 2010 +0200 +++ b/Nominal-General/Nominal2_Atoms.thy Mon Apr 26 10:01:13 2010 +0200 @@ -5,6 +5,7 @@ *) theory Nominal2_Atoms imports Nominal2_Base + Nominal2_Eqvt uses ("nominal_atoms.ML") begin @@ -20,6 +21,8 @@ assumes atom_eq_iff [simp]: "atom a = atom b \ a = b" assumes atom_eqvt: "p \ (atom a) = atom (p \ a)" +declare atom_eqvt[eqvt] + class at = at_base + assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)" @@ -75,6 +78,107 @@ thus ?thesis .. qed +lemma atom_image_cong: + fixes X Y::"('a::at_base) set" + shows "(atom ` X = atom ` Y) = (X = Y)" + apply(rule inj_image_eq_iff) + apply(simp add: inj_on_def) + done + +lemma atom_image_supp: + "supp S = supp (atom ` S)" + apply(simp add: supp_def) + apply(simp add: image_eqvt) + apply(subst (2) permute_fun_def) + apply(simp add: atom_eqvt) + apply(simp add: atom_image_cong) + done + +lemma supp_finite_at_set: + fixes S::"('a::at) set" + assumes a: "finite S" + shows "supp S = atom ` S" + apply(rule finite_supp_unique) + apply(simp add: supports_def) + apply(rule allI)+ + apply(rule impI) + apply(rule swap_fresh_fresh) + apply(simp add: fresh_def) + apply(simp add: atom_image_supp) + apply(subst supp_finite_atom_set) + apply(rule finite_imageI) + apply(simp add: a) + apply(simp) + apply(simp add: fresh_def) + apply(simp add: atom_image_supp) + apply(subst supp_finite_atom_set) + apply(rule finite_imageI) + apply(simp add: a) + apply(simp) + apply(rule finite_imageI) + apply(simp add: a) + apply(drule swap_set_in) + apply(assumption) + apply(simp) + apply(simp add: image_eqvt) + apply(simp add: permute_fun_def) + apply(simp add: atom_eqvt) + apply(simp add: atom_image_cong) + done + +lemma supp_finite_at_set_aux: + fixes S::"('a::at) set" + assumes a: "finite S" + shows "supp S = atom ` S" +proof + show "supp S \ ((atom::'a::at \ atom) ` S)" + apply(rule supp_is_subset) + apply(simp add: supports_def) + apply(rule allI)+ + apply(rule impI) + apply(rule swap_fresh_fresh) + apply(simp add: fresh_def) + apply(simp add: atom_image_supp) + apply(subst supp_finite_atom_set) + apply(rule finite_imageI) + apply(simp add: a) + apply(simp) + apply(simp add: fresh_def) + apply(simp add: atom_image_supp) + apply(subst supp_finite_atom_set) + apply(rule finite_imageI) + apply(simp add: a) + apply(simp) + apply(rule finite_imageI) + apply(simp add: a) + done +next + have "supp ((atom::'a::at \ atom) ` S) \ supp ((op `) (atom::'a::at \ atom)) \ supp S" + by (simp add: supp_fun_app) + moreover + have "supp ((op `) (atom::'a::at \ atom)) = {}" + apply(rule supp_fun_eqvt) + apply(perm_simp) + apply(simp) + done + moreover + have "supp ((atom::'a::at \ atom) ` S) = ((atom::'a::at \ atom) ` S)" + apply(subst supp_finite_atom_set) + apply(rule finite_imageI) + apply(simp add: a) + apply(simp) + done + ultimately + show "((atom::'a::at \ atom) ` S) \ supp S" by simp +qed + + +lemma supp_at_insert: + fixes S::"('a::at) set" + assumes a: "finite S" + shows "supp (insert a S) = supp a \ supp S" + using a by (simp add: supp_finite_at_set supp_at_base) + section {* A swapping operation for concrete atoms *} diff -r a0c7290a4e27 -r 27cdc0a3a763 Nominal-General/Nominal2_Base.thy --- a/Nominal-General/Nominal2_Base.thy Wed Apr 21 12:25:52 2010 +0200 +++ b/Nominal-General/Nominal2_Base.thy Mon Apr 26 10:01:13 2010 +0200 @@ -29,6 +29,11 @@ where "sort_of (Atom s i) = s" +primrec + nat_of :: "atom \ nat" +where + "nat_of (Atom s n) = n" + text {* There are infinitely many atoms of each sort. *} lemma INFM_sort_of_eq: @@ -63,6 +68,11 @@ then show ?thesis .. qed +lemma atom_components_eq_iff: + fixes a b :: atom + shows "a = b \ sort_of a = sort_of b \ nat_of a = nat_of b" + by (induct a, induct b, simp) + section {* Sort-Respecting Permutations *} typedef perm = @@ -459,7 +469,6 @@ unfolding permute_set_eq using a by (auto simp add: swap_atom) - subsection {* Permutations for units *} instantiation unit :: pt @@ -835,6 +844,24 @@ instance atom :: fs by default (simp add: supp_atom) +section {* Support for finite sets of atoms *} + +lemma supp_finite_atom_set: + fixes S::"atom set" + assumes "finite S" + shows "supp S = S" + apply(rule finite_supp_unique) + apply(simp add: supports_def) + apply(simp add: swap_set_not_in) + apply(rule assms) + apply(simp add: swap_set_in) +done + +lemma supp_atom_insert: + fixes S::"atom set" + assumes a: "finite S" + shows "supp (insert a S) = supp a \ supp S" + using a by (simp add: supp_finite_atom_set supp_atom) section {* Type @{typ perm} is finitely-supported. *} @@ -1054,32 +1081,18 @@ unfolding fresh_def by auto -(* alternative proof *) -lemma - shows "supp (f x) \ (supp f) \ (supp x)" -proof (rule subsetCI) - fix a::"atom" - assume a: "a \ supp (f x)" - assume b: "a \ supp f \ supp x" - then have "finite {b. (a \ b) \ f \ f}" "finite {b. (a \ b) \ x \ x}" - unfolding supp_def by auto - then have "finite ({b. (a \ b) \ f \ f} \ {b. (a \ b) \ x \ x})" by simp - moreover - have "{b. ((a \ b) \ f) ((a \ b) \ x) \ f x} \ ({b. (a \ b) \ f \ f} \ {b. (a \ b) \ x \ x})" - by auto - ultimately have "finite {b. ((a \ b) \ f) ((a \ b) \ x) \ f x}" - using finite_subset by auto - then have "a \ supp (f x)" unfolding supp_def - by (simp add: permute_fun_app_eq) - with a show "False" by simp -qed - +lemma supp_fun_eqvt: + assumes a: "\p. p \ f = f" + shows "supp f = {}" + unfolding supp_def + using a by simp + + lemma fresh_fun_eqvt_app: assumes a: "\p. p \ f = f" shows "a \ x \ a \ f x" proof - - from a have "supp f = {}" - unfolding supp_def by simp + 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 diff -r a0c7290a4e27 -r 27cdc0a3a763 Nominal-General/Nominal2_Eqvt.thy --- a/Nominal-General/Nominal2_Eqvt.thy Wed Apr 21 12:25:52 2010 +0200 +++ b/Nominal-General/Nominal2_Eqvt.thy Mon Apr 26 10:01:13 2010 +0200 @@ -6,7 +6,7 @@ (contains many, but not all such lemmas). *) theory Nominal2_Eqvt -imports Nominal2_Base Nominal2_Atoms +imports Nominal2_Base uses ("nominal_thmdecls.ML") ("nominal_permeq.ML") ("nominal_eqvt.ML") @@ -249,7 +249,7 @@ imp_eqvt [folded induct_implies_def] (* nominal *) - supp_eqvt fresh_eqvt + supp_eqvt fresh_eqvt add_perm_eqvt (* datatypes *) permute_prod.simps append_eqvt rev_eqvt set_eqvt @@ -259,8 +259,7 @@ empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt image_eqvt - atom_eqvt add_perm_eqvt - + lemmas [eqvt_raw] = permute_eqvt_raw[THEN eq_reflection] (* the normal version of this lemma loops *) @@ -288,22 +287,13 @@ use "nominal_permeq.ML" setup Nominal_Permeq.setup -ML {* -val test1 = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) []; -val test2 = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- - (Scan.repeat (Args.const true))) [] -*} - method_setup perm_simp = - {* test1 -- test2 >> - (fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt [] consts))) *} - {* pushes permutations inside *} + {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *} + {* pushes permutations inside. *} method_setup perm_strict_simp = - {* test1 -- test2 >> - (fn (thms, consts) => fn ctxt => SIMPLE_METHOD (HEADGOAL - (Nominal_Permeq.eqvt_strict_tac ctxt thms consts))) *} - {* pushes permutations inside, raises an error if it cannot solve all permutations *} + {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *} + {* pushes permutations inside, raises an error if it cannot solve all permutations. *} declare [[trace_eqvt = true]] diff -r a0c7290a4e27 -r 27cdc0a3a763 Nominal-General/Nominal2_Supp.thy --- a/Nominal-General/Nominal2_Supp.thy Wed Apr 21 12:25:52 2010 +0200 +++ b/Nominal-General/Nominal2_Supp.thy Mon Apr 26 10:01:13 2010 +0200 @@ -11,6 +11,7 @@ section {* Fresh-Star *} + text {* The fresh-star generalisation of fresh is used in strong induction principles. *} @@ -127,9 +128,8 @@ moreover have "supp ?q \ insert x Xs \ ?q \ insert x Xs" using p2 unfolding q - apply (intro subset_trans [OF supp_plus_perm]) - apply (auto simp add: supp_swap) - done + by (intro subset_trans [OF supp_plus_perm]) + (auto simp add: supp_swap) ultimately show ?case by blast qed qed @@ -158,20 +158,21 @@ lemma at_set_avoiding2_atom: assumes "finite (supp c)" "finite (supp x)" - and b: "xa \ x" - shows "\p. (p \ xa) \ c \ supp x \* p" + and b: "a \ x" + shows "\p. (p \ a) \ c \ supp x \* p" proof - - have a: "{xa} \* x" unfolding fresh_star_def by (simp add: b) - obtain p where p1: "(p \ {xa}) \* c" and p2: "supp x \* p" - using at_set_avoiding2[of "{xa}" "c" "x"] assms a by blast - have c: "(p \ xa) \ c" using p1 + 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 \ xa" in allE) (simp add: eqvts) - hence "p \ xa \ c \ supp x \* p" using p2 by blast - then show ?thesis by blast + by (erule_tac x="p \ a" in allE) (simp add: eqvts) + hence "p \ a \ c \ supp x \* p" using p2 by blast + then show "\p. (p \ a) \ c \ supp x \* p" by blast qed -section {* The freshness lemma according to Andrew Pitts *} + +section {* The freshness lemma according to Andy Pitts *} lemma freshness_lemma: fixes h :: "'a::at \ 'b::pt" @@ -339,17 +340,9 @@ using P Q by (rule FRESH_binop_iff) -section {* An example of a function without finite support *} +section {* @{const nat_of} is an example of a function + without finite support *} -primrec - nat_of :: "atom \ nat" -where - "nat_of (Atom s n) = n" - -lemma atom_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) lemma not_fresh_nat_of: shows "\ a \ nat_of" @@ -368,7 +361,7 @@ also have "\ = nat_of ((a \ b) \ a)" using b3 by simp also have "\ = nat_of b" using b2 by simp finally have "nat_of a = nat_of b" by simp - with b2 have "a = b" by (simp add: atom_eq_iff) + with b2 have "a = b" by (simp add: atom_components_eq_iff) with b1 show "False" by simp qed @@ -377,30 +370,17 @@ using not_fresh_nat_of [unfolded fresh_def] by auto -section {* Support for finite sets of atoms *} +section {* Induction principle for permutations *} + -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 - -text {* Induction principle for permutations *} - -lemma perm_subset_induct_aux [consumes 1, case_names zero swap plus]: +lemma perm_struct_induct[consumes 1, case_names zero swap]: assumes S: "supp p \ S" - assumes zero: "P 0" - assumes swap: "\a b. supp (a \ b) \ S \ P (a \ b)" - assumes plus: "\p1 p2. \P p1; P p2; supp p1 \ S; supp p2 \ S\ \ P (p1 + p2)" + 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 ?thesis using S + 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 @@ -412,38 +392,42 @@ moreover { assume "supp p \ {}" then obtain a where a0: "a \ supp p" by blast - then have a1: "supp (- p \ a \ a) \ S" using as + then have a1: "p \ a \ S" "a \ S" "sort_of (p \ a) = sort_of a" "p \ a \ a" using as by (auto simp add: supp_atom supp_perm swap_atom) - let ?q = "p + (- p \ a \ a)" + let ?q = "(p \ a \ a) + p" have a2: "supp ?q \ supp p" unfolding supp_perm by (auto simp add: swap_atom) moreover have "a \ supp ?q" by (simp add: supp_perm) then have "supp ?q \ supp p" using a0 by auto - ultimately have "supp ?q \ supp p" using as by auto + ultimately have "supp ?q \ supp p" using a2 by auto then have "P ?q" using ih by simp moreover have "supp ?q \ S" using as a2 by simp - moreover - have "P (- p \ a \ a)" using a1 swap by simp - ultimately - have "P (?q + (- p \ a \ a))" using a1 plus by simp + ultimately have "P ((p \ a \ a) + ?q)" using as a1 swap by simp moreover - have "p = ?q + (- p \ a \ a)" by (simp add: expand_perm_eq) + have "p = (p \ a \ a) + ?q" by (simp add: expand_perm_eq) ultimately have "P p" by simp } ultimately show "P p" by blast qed qed -lemma perm_subset_induct [consumes 1, case_names zero swap plus]: +lemma perm_simple_struct_induct[case_names zero swap]: + assumes zero: "P 0" + and swap: "\p a b. \P p; a \ b; sort_of a = sort_of b\ \ P ((a \ b) + p)" + shows "P p" +by (rule_tac S="supp p" in perm_struct_induct) + (auto intro: zero swap) + +lemma perm_subset_induct[consumes 1, case_names zero swap plus]: assumes S: "supp p \ S" assumes zero: "P 0" assumes swap: "\a b. \sort_of a = sort_of b; a \ b; a \ S; b \ S\ \ P (a \ b)" assumes plus: "\p1 p2. \P p1; P p2; supp p1 \ S; supp p2 \ S\ \ P (p1 + p2)" shows "P p" -apply(rule perm_subset_induct_aux[OF S]) -apply(auto simp add: zero swap plus supp_swap split: if_splits) -done +using S +by (induct p rule: perm_struct_induct) + (auto intro: zero plus swap simp add: supp_swap) lemma supp_perm_eq: assumes "(supp x) \* p" @@ -452,6 +436,23 @@ from assms have "supp p \ {a. a \ x}" unfolding supp_perm fresh_star_def fresh_def by auto then show "p \ x = x" + proof (induct p rule: perm_struct_induct) + case zero + show "0 \ x = x" by simp + next + case (swap p a b) + then have "a \ x" "b \ x" "p \ x = x" by simp_all + then show "((a \ b) + p) \ x = x" by (simp add: swap_fresh_fresh) + qed +qed + +lemma supp_perm_eq_test: + assumes "(supp x) \* p" + shows "p \ x = x" +proof - + from assms have "supp p \ {a. a \ x}" + unfolding supp_perm fresh_star_def fresh_def by auto + then show "p \ x = x" proof (induct p rule: perm_subset_induct) case zero show "0 \ x = x" by simp diff -r a0c7290a4e27 -r 27cdc0a3a763 Nominal-General/nominal_eqvt.ML --- a/Nominal-General/nominal_eqvt.ML Wed Apr 21 12:25:52 2010 +0200 +++ b/Nominal-General/nominal_eqvt.ML Mon Apr 26 10:01:13 2010 +0200 @@ -9,7 +9,7 @@ sig val equivariance: string -> Proof.context -> local_theory val eqvt_rel_tac: Proof.context -> string list -> term -> thm -> thm list -> int -> tactic - val eqvt_rel_case_tac: Proof.context -> string list -> term -> thm -> int -> tactic + val eqvt_rel_single_case_tac: Proof.context -> string list -> term -> thm -> int -> tactic end structure Nominal_Eqvt : NOMINAL_EQVT = @@ -27,9 +27,10 @@ (** - proves F[f t] from F[t] which is the given theorem + 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 + - f returns either SOME for a term it fires on and NONE elsewhere **) fun map_term f t = @@ -90,7 +91,7 @@ val perm_cancel = @{thms permute_minus_cancel(2)} val perm_expand_bool = @{thms permute_fun_def minus_minus permute_bool_def} -fun eqvt_rel_case_tac ctxt pred_names pi intro = +fun eqvt_rel_single_case_tac ctxt pred_names pi intro = let val thy = ProofContext.theory_of ctxt val cpi = Thm.cterm_of thy (mk_minus pi) @@ -113,7 +114,7 @@ fun eqvt_rel_tac ctxt pred_names pi induct intros = let - val cases = map (eqvt_rel_case_tac ctxt pred_names pi) intros + val cases = map (eqvt_rel_single_case_tac ctxt pred_names pi) intros in EVERY' (rtac induct :: cases) end @@ -150,9 +151,10 @@ val raw_induct = atomize_induct ctxt raw_induct val intros = map atomize_intr intrs val params_no = length (Inductive.params_of raw_induct) - val (([raw_concl], [raw_pi]), ctxt') = ctxt - |> Variable.import_terms false [concl_of raw_induct] - ||>> Variable.variant_fixes ["p"] + val (([raw_concl], [raw_pi]), ctxt') = + ctxt + |> Variable.import_terms false [concl_of raw_induct] + ||>> Variable.variant_fixes ["p"] val pi = Free (raw_pi, @{typ perm}) val preds = map (fst o HOLogic.dest_imp) (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl)); @@ -171,7 +173,7 @@ val _ = OuterSyntax.local_theory "equivariance" - "prove equivariance for inductive predicate involving nominal datatypes" + "Proves equivariance for inductive predicate involving nominal datatypes." K.thy_decl (P.xname >> equivariance); end; diff -r a0c7290a4e27 -r 27cdc0a3a763 Nominal-General/nominal_permeq.ML --- a/Nominal-General/nominal_permeq.ML Wed Apr 21 12:25:52 2010 +0200 +++ b/Nominal-General/nominal_permeq.ML Mon Apr 26 10:01:13 2010 +0200 @@ -7,6 +7,11 @@ sig val eqvt_tac: Proof.context -> thm list -> string list -> int -> tactic val eqvt_strict_tac: Proof.context -> thm list -> string list -> int -> tactic + + val perm_simp_meth: thm list * string list -> Proof.context -> Method.method + val perm_strict_simp_meth: thm list * string list -> Proof.context -> Method.method + val args_parser: (thm list * string list) context_parser + val trace_eqvt: bool Config.T val setup: theory -> theory end; @@ -157,4 +162,21 @@ val setup = trace_eqvt_setup + +(** methods **) + +val add_thms_parser = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) []; +val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- + (Scan.repeat (Args.const true))) [] + +val args_parser = + add_thms_parser -- exclude_consts_parser || + exclude_consts_parser -- add_thms_parser >> swap + +fun perm_simp_meth (thms, consts) ctxt = + SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt thms consts)) + +fun perm_strict_simp_meth (thms, consts) ctxt = + SIMPLE_METHOD (HEADGOAL (eqvt_strict_tac ctxt thms consts)) + end; (* structure *) \ No newline at end of file diff -r a0c7290a4e27 -r 27cdc0a3a763 Nominal-General/nominal_thmdecls.ML --- a/Nominal-General/nominal_thmdecls.ML Wed Apr 21 12:25:52 2010 +0200 +++ b/Nominal-General/nominal_thmdecls.ML Mon Apr 26 10:01:13 2010 +0200 @@ -45,7 +45,8 @@ fun get_ps trm = case trm of - Const (@{const_name permute}, _) $ p $ (Bound _) => raise TERM ("get_ps", [trm]) + Const (@{const_name permute}, _) $ p $ (Bound _) => + raise TERM ("get_ps called on bound", [trm]) | Const (@{const_name permute}, _) $ p $ _ => [p] | t $ u => get_ps t @ get_ps u | Abs (_, _, t) => get_ps t @@ -59,7 +60,8 @@ | Abs (x, ty, t) => Abs (x, ty, put_p p t) | _ => mk_perm p trm -(* tests whether the lists of ps all agree, and that there is at least one p *) +(* tests whether there is a disagreement between the permutations, + and that there is at least one permutation *) fun is_bad_list [] = true | is_bad_list [_] = false | is_bad_list (p::q::ps) = if p = q then is_bad_list (q::ps) else true @@ -88,8 +90,7 @@ fun add_raw_thm thm = case prop_of thm of - Const ("==", _) $ _ $ _ => - EqvtRawData.map (Item_Net.update (zero_var_indexes thm)) + Const ("==", _) $ _ $ _ => (EqvtRawData.map o Item_Net.update) thm | _ => raise THM ("Theorem must be a meta-equality", 0, [thm]) val del_raw_thm = EqvtRawData.map o Item_Net.remove; @@ -98,7 +99,7 @@ (** transformation of eqvt lemmas **) -(* transforms equations into the "p o c = c"-form +(* transforms equations into the "p o c == c"-form from p o (c x1 ...xn) = c (p o x1) ... (p o xn) *) fun eqvt_transform_eq_tac thm = @@ -113,18 +114,21 @@ fun eqvt_transform_eq ctxt thm = let - val ((p, t), rhs) = apfst dest_perm - (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))) - handle TERM _ => error "Eqvt lemma is not of the form p \ c... = c..." + val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm)) + handle TERM _ => error "Equivariance lemma must be an equality." + val (p, t) = dest_perm lhs + handle TERM _ => error "Equivariance lemma is not of the form p \ c... = c..." + val ps = get_ps rhs handle TERM _ => [] val (c, c') = (head_of t, head_of rhs) + val msg = "Equivariance lemma is not of the right form " in if c <> c' - then error "Eqvt lemma is not of the right form (constants do not agree)" + then error (msg ^ "(constants do not agree).") else if is_bad_list (p::ps) - then error "Eqvt lemma is not of the right form (permutations do not agree)" + then error (msg ^ "(permutations do not agree).") else if not (rhs aconv (put_p p t)) - then error "Eqvt lemma is not of the right form (arguments do not agree)" + then error (msg ^ "(arguments do not agree).") else if is_Const t then safe_mk_equiv thm else @@ -135,14 +139,16 @@ Goal.prove ctxt [] [] goal' (fn _ => eqvt_transform_eq_tac thm 1) |> singleton (ProofContext.export ctxt' ctxt) |> safe_mk_equiv + |> zero_var_indexes end end -(* transforms equations into the "p o c = c"-form +(* transforms equations into the "p o c == c"-form from R x1 ...xn ==> R (p o x1) ... (p o xn) *) -fun eqvt_transform_imp_tac thy p p' thm = +fun eqvt_transform_imp_tac ctxt p p' thm = let + val thy = ProofContext.theory_of ctxt val cp = Thm.cterm_of thy p val cp' = Thm.cterm_of thy (mk_minus p') val thm' = Drule.cterm_instantiate [(cp, cp')] thm @@ -154,18 +160,18 @@ fun eqvt_transform_imp ctxt thm = let - val thy = ProofContext.theory_of ctxt val (prem, concl) = pairself HOLogic.dest_Trueprop (Logic.dest_implies (prop_of thm)) val (c, c') = (head_of prem, head_of concl) val ps = get_ps concl handle TERM _ => [] val p = try hd ps + val msg = "Equivariance lemma is not of the right form " in if c <> c' - then error "Eqvt lemma is not of the right form (constants do not agree)" + then error (msg ^ "(constants do not agree).") else if is_bad_list ps - then error "Eqvt lemma is not of the right form (permutations do not agree)" + then error (msg ^ "(permutations do not agree).") else if not (concl aconv (put_p (the p) prem)) - then error "Eqvt lemma is not of the right form (arguments do not agree)" + then error (msg ^ "(arguments do not agree).") else let val prem' = mk_perm (the p) prem @@ -173,7 +179,7 @@ val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt in Goal.prove ctxt' [] [] goal' - (fn _ => eqvt_transform_imp_tac thy (the p) p' thm 1) + (fn _ => eqvt_transform_imp_tac ctxt' (the p) p' thm 1) |> singleton (ProofContext.export ctxt' ctxt) |> eqvt_transform_eq ctxt end diff -r a0c7290a4e27 -r 27cdc0a3a763 Nominal/Abs.thy --- a/Nominal/Abs.thy Wed Apr 21 12:25:52 2010 +0200 +++ b/Nominal/Abs.thy Mon Apr 26 10:01:13 2010 +0200 @@ -2,8 +2,8 @@ imports "../Nominal-General/Nominal2_Atoms" "../Nominal-General/Nominal2_Eqvt" "../Nominal-General/Nominal2_Supp" - "Nominal2_FSet" "Quotient" + "Quotient_List" "Quotient_Product" begin @@ -129,16 +129,22 @@ by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:) quotient_definition + Abs ("[_]set. _" [60, 60] 60) +where "Abs::atom set \ ('a::pt) \ 'a abs_gen" is "Pair::atom set \ ('a::pt) \ (atom set \ 'a)" quotient_definition + Abs_res ("[_]res. _" [60, 60] 60) +where "Abs_res::atom set \ ('a::pt) \ 'a abs_res" is "Pair::atom set \ ('a::pt) \ (atom set \ 'a)" quotient_definition + Abs_lst ("[_]lst. _" [60, 60] 60) +where "Abs_lst::atom list \ ('a::pt) \ 'a abs_lst" is "Pair::atom list \ ('a::pt) \ (atom list \ 'a)" @@ -169,9 +175,8 @@ shows "Abs bs x = Abs cs y \ (bs, x) \abs (cs, y)" and "Abs_res bs x = Abs_res cs y \ (bs, x) \abs_res (cs, y)" and "Abs_lst ds x = Abs_lst hs y \ (ds, x) \abs_lst (hs, y)" - apply(simp_all add: alphas_abs) - apply(lifting alphas_abs) - done + unfolding alphas_abs + by (lifting alphas_abs) instantiation abs_gen :: (pt) pt begin @@ -327,9 +332,8 @@ shows "a \ Abs bs x \ a \ supp_gen (Abs bs x)" and "a \ Abs_res bs x \ a \ supp_res (Abs_res bs x)" and "a \ Abs_lst cs x \ a \ supp_lst (Abs_lst cs x)" - apply(rule_tac [!] fresh_fun_eqvt_app) - apply(simp_all add: eqvts_raw) - done + by (rule_tac [!] fresh_fun_eqvt_app) + (simp_all add: eqvts_raw) lemma supp_abs_subset1: assumes a: "finite (supp x)" @@ -337,36 +341,32 @@ and "(supp x) - as \ supp (Abs_res as x)" and "(supp x) - (set bs) \ supp (Abs_lst bs x)" unfolding supp_conv_fresh - apply(auto dest!: aux_fresh) - apply(simp_all add: fresh_def supp_finite_atom_set a) - done + by (auto dest!: aux_fresh) + (simp_all add: fresh_def supp_finite_atom_set a) lemma supp_abs_subset2: assumes a: "finite (supp x)" shows "supp (Abs as x) \ (supp x) - as" and "supp (Abs_res as x) \ (supp x) - as" and "supp (Abs_lst bs x) \ (supp x) - (set bs)" - apply(rule_tac [!] supp_is_subset) - apply(simp_all add: abs_supports a) - done + by (rule_tac [!] supp_is_subset) + (simp_all add: abs_supports a) lemma abs_finite_supp: assumes a: "finite (supp x)" shows "supp (Abs as x) = (supp x) - as" and "supp (Abs_res as x) = (supp x) - as" and "supp (Abs_lst bs x) = (supp x) - (set bs)" - apply(rule_tac [!] subset_antisym) - apply(simp_all add: supp_abs_subset1[OF a] supp_abs_subset2[OF a]) - done + by (rule_tac [!] subset_antisym) + (simp_all add: supp_abs_subset1[OF a] supp_abs_subset2[OF a]) lemma supp_abs: fixes x::"'a::fs" shows "supp (Abs as x) = (supp x) - as" and "supp (Abs_res as x) = (supp x) - as" and "supp (Abs_lst bs x) = (supp x) - (set bs)" - apply(rule_tac [!] abs_finite_supp) - apply(simp_all add: finite_supp) - done + by (rule_tac [!] abs_finite_supp) + (simp_all add: finite_supp) instance abs_gen :: (fs) fs apply(default) @@ -397,101 +397,12 @@ section {* BELOW is stuff that may or may not be needed *} -lemma - fixes t1 s1::"'a::fs" - and t2 s2::"'b::fs" - shows "Abs as (t1, t2) = Abs as (s1, s2) \ (Abs as t1 = Abs as s1 \ Abs as t2 = Abs as s2)" -apply(subst abs_eq_iff) -apply(subst alphas_abs) -apply(subst alphas) -apply(rule impI) -apply(erule exE) -apply(simp add: supp_Pair) -apply(simp add: Un_Diff) -apply(simp add: fresh_star_union) -apply(erule conjE)+ -apply(rule conjI) -apply(rule trans) -apply(rule sym) -apply(rule_tac p="p" in supp_perm_eq) -apply(simp add: supp_abs) -apply(simp) -apply(rule trans) -apply(rule sym) -apply(rule_tac p="p" in supp_perm_eq) -apply(simp add: supp_abs) -apply(simp) -done - -lemma - fixes t1 s1::"'a::fs" - and t2 s2::"'b::fs" - shows "Abs as (t1, t2) = Abs bs (s1, s2) \ (Abs as t1 = Abs bs s1 \ Abs as t2 = Abs bs s2)" -apply(subst abs_eq_iff) -apply(subst alphas_abs) -apply(subst alphas) -apply(rule impI) -apply(erule exE) -apply(simp add: supp_Pair) -apply(simp add: Un_Diff) -apply(simp add: fresh_star_union) -apply(erule conjE)+ -apply(rule conjI) -apply(rule trans) -apply(rule sym) -apply(rule_tac p="p" in supp_perm_eq) -apply(simp add: supp_abs) -apply(simp) -apply(rule trans) -apply(rule sym) -apply(rule_tac p="p" in supp_perm_eq) -apply(simp add: supp_abs) -apply(simp) -done - -lemma fresh_star_eq: - assumes a: "as \* p" - shows "\a \ as. p \ a = a" -using a by (simp add: fresh_star_def fresh_def supp_perm) - -lemma fresh_star_set_eq: - assumes a: "as \* p" - shows "p \ as = as" -using a -apply(simp add: fresh_star_def fresh_def supp_perm permute_set_eq) -apply(auto) -by (metis permute_atom_def) - -lemma - fixes t1 s1::"'a::fs" - and t2 s2::"'b::fs" - assumes asm: "finite as" - shows "(Abs as t1 = Abs bs s1 \ Abs as t2 = Abs bs s2) \ Abs as (t1, t2) = Abs bs (s1, s2)" -apply(subst abs_eq_iff) -apply(subst abs_eq_iff) -apply(subst alphas_abs) -apply(subst alphas_abs) -apply(subst alphas) -apply(subst alphas) -apply(rule impI) -apply(erule exE | erule conjE)+ -apply(simp add: abs_eq_iff) -apply(simp add: alphas_abs) -apply(simp add: alphas) -apply(rule conjI) -apply(simp add: supp_Pair Un_Diff) -oops - - - -(* support of concrete atom sets *) - lemma supp_atom_image: fixes as::"'a::at_base set" shows "supp (atom ` as) = supp as" apply(simp add: supp_def) apply(simp add: image_eqvt) -apply(simp add: atom_eqvt_raw) +apply(simp add: eqvts_raw) apply(simp add: atom_image_cong) done diff -r a0c7290a4e27 -r 27cdc0a3a763 Nominal/Ex/Ex1rec.thy --- a/Nominal/Ex/Ex1rec.thy Wed Apr 21 12:25:52 2010 +0200 +++ b/Nominal/Ex/Ex1rec.thy Mon Apr 26 10:01:13 2010 +0200 @@ -6,27 +6,27 @@ ML {* val _ = recursive := true *} ML {* val _ = alpha_type := AlphaGen *} -nominal_datatype lam' = - VAR' "name" -| APP' "lam'" "lam'" -| LAM' x::"name" t::"lam'" bind x in t -| LET' bp::"bp'" t::"lam'" bind "bi' bp" in t -and bp' = - BP' "name" "lam'" +nominal_datatype lam = + VAR "name" +| APP "lam" "lam" +| LAM x::"name" t::"lam" bind x in t +| LET bp::"bp" t::"lam" bind "bi bp" in t +and bp = + BP "name" "lam" binder - bi'::"bp' \ atom set" + bi::"bp \ atom set" where - "bi' (BP' x t) = {atom x}" + "bi (BP x t) = {atom x}" -thm lam'_bp'.fv -thm lam'_bp'.eq_iff[no_vars] -thm lam'_bp'.bn -thm lam'_bp'.perm -thm lam'_bp'.induct -thm lam'_bp'.inducts -thm lam'_bp'.distinct -ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *} -thm lam'_bp'.fv[simplified lam'_bp'.supp] +thm lam_bp.fv +thm lam_bp.eq_iff[no_vars] +thm lam_bp.bn +thm lam_bp.perm +thm lam_bp.induct +thm lam_bp.inducts +thm lam_bp.distinct +ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *} +thm lam_bp.fv[simplified lam_bp.supp] end diff -r a0c7290a4e27 -r 27cdc0a3a763 Nominal/Ex/ExPS8.thy --- a/Nominal/Ex/ExPS8.thy Wed Apr 21 12:25:52 2010 +0200 +++ b/Nominal/Ex/ExPS8.thy Mon Apr 26 10:01:13 2010 +0200 @@ -11,41 +11,41 @@ the reference. *) ML {* val _ = recursive := false *} -nominal_datatype exp8 = +nominal_datatype exp = EVar name | EUnit -| EPair exp8 exp8 -| ELetRec l::lrbs8 e::exp8 bind "b_lrbs8 l" in e (* rec *) +| EPair exp exp +| ELetRec l::lrbs e::exp bind "b_lrbs l" in e (* rec *) and fnclause = - K x::name p::pat8 f::exp8 bind "b_pat p" in f (* non-rec *) + K x::name p::pat f::exp bind "b_pat p" in f (* non-rec *) and fnclauses = S fnclause | ORs fnclause fnclauses -and lrb8 = +and lrb = Clause fnclauses -and lrbs8 = - Single lrb8 -| More lrb8 lrbs8 -and pat8 = +and lrbs = + Single lrb +| More lrb lrbs +and pat = PVar name | PUnit -| PPair pat8 pat8 +| PPair pat pat binder - b_lrbs8 :: "lrbs8 \ atom set" and - b_pat :: "pat8 \ atom set" and + b_lrbs :: "lrbs \ atom set" and + b_pat :: "pat \ atom set" and b_fnclauses :: "fnclauses \ atom set" and b_fnclause :: "fnclause \ atom set" and - b_lrb8 :: "lrb8 \ atom set" + b_lrb :: "lrb \ atom set" where - "b_lrbs8 (Single l) = b_lrb8 l" -| "b_lrbs8 (More l ls) = b_lrb8 l \ b_lrbs8 ls" + "b_lrbs (Single l) = b_lrb l" +| "b_lrbs (More l ls) = b_lrb l \ b_lrbs ls" | "b_pat (PVar x) = {atom x}" | "b_pat (PUnit) = {}" | "b_pat (PPair p1 p2) = b_pat p1 \ b_pat p2" | "b_fnclauses (S fc) = (b_fnclause fc)" | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \ (b_fnclauses fcs)" -| "b_lrb8 (Clause fcs) = (b_fnclauses fcs)" -| "b_fnclause (K x pat exp8) = {atom x}" +| "b_lrb (Clause fcs) = (b_fnclauses fcs)" +| "b_fnclause (K x pat exp) = {atom x}" thm exp7_lrb_lrbs.eq_iff thm exp7_lrb_lrbs.supp diff -r a0c7290a4e27 -r 27cdc0a3a763 Nominal/Ex/Lambda.thy --- a/Nominal/Ex/Lambda.thy Wed Apr 21 12:25:52 2010 +0200 +++ b/Nominal/Ex/Lambda.thy Mon Apr 26 10:01:13 2010 +0200 @@ -126,44 +126,109 @@ typing :: "(name\ty) list \ lam \ ty \ bool" ("_ \ _ : _" [60,60,60] 60) where t_Var[intro]: "\valid \; (x, T) \ set \\ \ \ \ Var x : T" - | t_App[intro]: "\\ \ t1 : T1 \ T2 \ \ \ t2 : T1\ \ \ \ App t1 t2 : T2" + | t_App[intro]: "\\ \ t1 : T1 \ T2; \ \ t2 : T1\ \ \ \ App t1 t2 : T2" | t_Lam[intro]: "\atom x \ \; (x, T1) # \ \ t : T2\ \ \ \ Lam x t : T1 \ T2" -inductive - typing' :: "(name\ty) list\lam\ty\bool" ("_ \ _ : _" [60,60,60] 60) -where - t'_Var[intro]: "\valid \; (x,T)\set \\ \ \ \ Var x : T" - | t'_App[intro]: "\\ \ t1 : T1\T2 \ \ \ t2 : T1\ \ \ \ App t1 t2 : T2" - | t'_Lam[intro]: "\atom x\\;(x,T1)#\ \ t : T2\ \ \ \ Lam x t : T1\T2" - -inductive - typing2' :: "(name\ty) list\lam\ty\bool" ("_ 2\ _ : _" [60,60,60] 60) -where - t2'_Var[intro]: "\valid \; (x,T)\set \\ \ \ 2\ Var x : T" - | t2'_App[intro]: "\\ 2\ t1 : T1\T2 \ \ 2\ t2 : T1\ \ \ 2\ App t1 t2 : T2" - | t2'_Lam[intro]: "\atom x\\;(x,T1)#\ 2\ t : T2\ \ \ 2\ Lam x t : T1\T2" - -inductive - typing'' :: "(name\ty) list\lam\ty\bool" ("_ |\ _ : _" [60,60,60] 60) -and valid' :: "(name\ty) list \ bool" -where - v1[intro]: "valid' []" - | v2[intro]: "\valid' \;atom x\\\\ valid' ((x,T)#\)" - | t'_Var[intro]: "\valid' \; (x,T)\set \\ \ \ |\ Var x : T" - | t'_App[intro]: "\\ |\ t1 : T1\T2; \ |\ t2 : T1\ \ \ |\ App t1 t2 : T2" - | t'_Lam[intro]: "\atom x\\;(x,T1)#\ |\ t : T2\ \ \ |\ Lam x t : T1\T2" - equivariance valid equivariance typing -equivariance typing' -equivariance typing2' -equivariance typing'' thm valid.eqvt thm typing.eqvt thm eqvts thm eqvts_raw +thm typing.induct[of "\" "t" "T", no_vars] + +lemma + fixes c::"'a::fs" + assumes a: "\ \ t : T" + and a1: "\\ x T c. \valid \; (x, T) \ set \\ \ P c \ (Var x) T" + and a2: "\\ t1 T1 T2 t2 c. \\ \ t1 : T1 \ T2; \d. P d \ t1 T1 \ T2; \ \ t2 : T1; \d. P d \ t2 T1\ + \ P c \ (App t1 t2) T2" + and a3: "\x \ T1 t T2 c. \atom x \ c; atom x \ \; (x, T1) # \ \ t : T2; \d. P d ((x, T1) # \) t T2\ + \ P c \ (Lam x t) T1 \ T2" + shows "P c \ t T" +proof - + from a have "\p c. P c (p \ \) (p \ t) (p \ T)" + proof (induct) + case (t_Var \ x T p c) + then show ?case + apply - + apply(perm_strict_simp) + apply(rule a1) + apply(rule_tac p="-p" in permute_boolE) + apply(perm_strict_simp add: permute_minus_cancel) + apply(assumption) + apply(rule_tac p="-p" in permute_boolE) + apply(perm_strict_simp add: permute_minus_cancel) + apply(assumption) + done + next + case (t_App \ t1 T1 T2 t2 p c) + then show ?case + apply - + apply(perm_strict_simp) + apply(rule_tac ?T1.0="p \ T1" in a2) + apply(rule_tac p="-p" in permute_boolE) + apply(perm_strict_simp add: permute_minus_cancel) + apply(assumption) + apply(assumption) + apply(rule_tac p="-p" in permute_boolE) + apply(perm_strict_simp add: permute_minus_cancel) + apply(assumption) + apply(assumption) + done + next + case (t_Lam x \ T1 t T2 p c) + then show ?case + apply - + apply(subgoal_tac "\q. (q \ {p \ atom x}) \* c \ + supp (p \ \, p \ Lam x t, p \ (T1 \ T2)) \* q") + apply(erule exE) + apply(rule_tac t="p \ \" and s="q \ p \ \" in subst) + apply(rule supp_perm_eq) + apply(simp add: supp_Pair fresh_star_union) + apply(rule_tac t="p \ Lam x t" and s="q \ p \ Lam x t" in subst) + apply(rule supp_perm_eq) + apply(simp add: supp_Pair fresh_star_union) + apply(rule_tac t="p \ (T1 \ T2)" and s="q \ p \ (T1 \ T2)" in subst) + apply(rule supp_perm_eq) + apply(simp add: supp_Pair fresh_star_union) + apply(simp add: eqvts) + apply(rule a3) + apply(simp add: fresh_star_def) + apply(rule_tac p="-q" in permute_boolE) + apply(perm_strict_simp add: permute_minus_cancel) + apply(rule_tac p="-p" in permute_boolE) + apply(perm_strict_simp add: permute_minus_cancel) + apply(assumption) + apply(rule_tac p="-q" in permute_boolE) + apply(perm_strict_simp add: permute_minus_cancel) + apply(rule_tac p="-p" in permute_boolE) + apply(perm_strict_simp add: permute_minus_cancel) + apply(assumption) + apply(drule_tac x="d" in meta_spec) + apply(drule_tac x="q + p" in meta_spec) + apply(simp) + apply(rule at_set_avoiding2) + apply(simp add: finite_supp) + apply(simp add: finite_supp) + apply(simp add: finite_supp) + apply(rule_tac p="-p" in permute_boolE) + apply(perm_strict_simp add: permute_minus_cancel) + (* supplied by the user *) + apply(simp add: fresh_star_prod) + apply(simp add: fresh_star_def) + + + done +(* HERE *) + + + + + + inductive tt :: "('a \ 'a \ bool) \ ('a \ 'a \ bool)" @@ -189,27 +254,9 @@ declare permute_lam_raw.simps[eqvt] declare alpha_gen_eqvt[eqvt] equivariance alpha_lam_raw' + thm eqvts_raw - - -(* HERE *) - -lemma - assumes a: "alpha_lam_raw' t1 t2" - shows "alpha_lam_raw' (p \ t1) (p \ t2)" -using a -apply(induct) -apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac - @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a1} 1*}) -apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac - @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a2} 1*}) -(* -apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac - @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a3} 1*}) -*) -oops - section {* size function *} lemma size_eqvt_raw: @@ -367,6 +414,29 @@ done *) + +ML {* + +fun prove_strong_ind (pred_name, avoids) ctxt = + Proof.theorem NONE (K I) [] ctxt + +local structure P = OuterParse and K = OuterKeyword in + +val _ = + OuterSyntax.local_theory_to_proof "nominal_inductive" + "proves strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal + (P.xname -- (Scan.optional (P.$$$ "avoids" |-- P.enum1 "|" (P.name -- + (P.$$$ ":" |-- P.and_list1 P.term))) []) >> prove_strong_ind) + +end; + +*} + +(* +nominal_inductive typing +*) + + end diff -r a0c7290a4e27 -r 27cdc0a3a763 Nominal/Ex/TypeSchemes.thy --- a/Nominal/Ex/TypeSchemes.thy Wed Apr 21 12:25:52 2010 +0200 +++ b/Nominal/Ex/TypeSchemes.thy Mon Apr 26 10:01:13 2010 +0200 @@ -108,10 +108,9 @@ apply (simp add: fin_fset_to_set) apply (simp add: finite_supp) apply (simp add: eqvts finite_supp) - apply (subst atom_eqvt_raw[symmetric]) - apply (subst fmap_eqvt[symmetric]) - apply (subst fset_to_set_eqvt[symmetric]) - apply (simp only: fresh_star_permute_iff) + apply (rule_tac p=" -p" in permute_boolE) + apply(simp add: eqvts) + apply(simp add: permute_fun_def atom_eqvt) apply (simp add: fresh_star_def) apply clarify apply (simp add: fresh_def) diff -r a0c7290a4e27 -r 27cdc0a3a763 Nominal/FSet.thy --- a/Nominal/FSet.thy Wed Apr 21 12:25:52 2010 +0200 +++ b/Nominal/FSet.thy Mon Apr 26 10:01:13 2010 +0200 @@ -71,6 +71,85 @@ else f a (ffold_raw f z A) else z)" +text {* Composition Quotient *} + +lemma list_rel_refl: + shows "(list_rel op \) r r" + by (rule list_rel_refl) (metis equivp_def fset_equivp) + +lemma compose_list_refl: + shows "(list_rel op \ OOO op \) r r" +proof + show c: "list_rel op \ r r" by (rule list_rel_refl) + have d: "r \ r" by (rule equivp_reflp[OF fset_equivp]) + show b: "(op \ OO list_rel op \) r r" by (rule pred_compI) (rule d, rule c) +qed + +lemma Quotient_fset_list: + shows "Quotient (list_rel op \) (map abs_fset) (map rep_fset)" + by (fact list_quotient[OF Quotient_fset]) + +lemma set_in_eq: "(\e. ((e \ A) \ (e \ B))) \ A = B" + by (rule eq_reflection) auto + +lemma map_rel_cong: "b \ ba \ map f b \ map f ba" + unfolding list_eq.simps + by (simp only: set_map set_in_eq) + +lemma quotient_compose_list[quot_thm]: + shows "Quotient ((list_rel op \) OOO (op \)) + (abs_fset \ (map abs_fset)) ((map rep_fset) \ rep_fset)" + unfolding Quotient_def comp_def +proof (intro conjI allI) + fix a r s + show "abs_fset (map abs_fset (map rep_fset (rep_fset a))) = a" + by (simp add: abs_o_rep[OF Quotient_fset] Quotient_abs_rep[OF Quotient_fset] map_id) + have b: "list_rel op \ (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))" + by (rule list_rel_refl) + have c: "(op \ OO list_rel op \) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))" + by (rule, rule equivp_reflp[OF fset_equivp]) (rule b) + show "(list_rel op \ OOO op \) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))" + by (rule, rule list_rel_refl) (rule c) + show "(list_rel op \ OOO op \) r s = ((list_rel op \ OOO op \) r r \ + (list_rel op \ OOO op \) s s \ abs_fset (map abs_fset r) = abs_fset (map abs_fset s))" + proof (intro iffI conjI) + show "(list_rel op \ OOO op \) r r" by (rule compose_list_refl) + show "(list_rel op \ OOO op \) s s" by (rule compose_list_refl) + next + assume a: "(list_rel op \ OOO op \) r s" + then have b: "map abs_fset r \ map abs_fset s" proof (elim pred_compE) + fix b ba + assume c: "list_rel op \ r b" + assume d: "b \ ba" + assume e: "list_rel op \ ba s" + have f: "map abs_fset r = map abs_fset b" + using Quotient_rel[OF Quotient_fset_list] c by blast + have "map abs_fset ba = map abs_fset s" + using Quotient_rel[OF Quotient_fset_list] e by blast + then have g: "map abs_fset s = map abs_fset ba" by simp + then show "map abs_fset r \ map abs_fset s" using d f map_rel_cong by simp + qed + then show "abs_fset (map abs_fset r) = abs_fset (map abs_fset s)" + using Quotient_rel[OF Quotient_fset] by blast + next + assume a: "(list_rel op \ OOO op \) r r \ (list_rel op \ OOO op \) s s + \ abs_fset (map abs_fset r) = abs_fset (map abs_fset s)" + then have s: "(list_rel op \ OOO op \) s s" by simp + have d: "map abs_fset r \ map abs_fset s" + by (subst Quotient_rel[OF Quotient_fset]) (simp add: a) + have b: "map rep_fset (map abs_fset r) \ map rep_fset (map abs_fset s)" + by (rule map_rel_cong[OF d]) + have y: "list_rel op \ (map rep_fset (map abs_fset s)) s" + by (fact rep_abs_rsp_left[OF Quotient_fset_list, OF list_rel_refl[of s]]) + have c: "(op \ OO list_rel op \) (map rep_fset (map abs_fset r)) s" + by (rule pred_compI) (rule b, rule y) + have z: "list_rel op \ r (map rep_fset (map abs_fset r))" + by (fact rep_abs_rsp[OF Quotient_fset_list, OF list_rel_refl[of r]]) + then show "(list_rel op \ OOO op \) r s" + using a c pred_compI by simp + qed +qed + text {* Respectfullness *} lemma [quot_respect]: @@ -178,7 +257,7 @@ apply (induct b) apply (simp_all add: not_memb_nil) apply (auto) - apply (simp_all add: memb_delete_raw not_memb_delete_raw_ident rsp_fold_def memb_cons_iff) + apply (simp_all add: memb_delete_raw not_memb_delete_raw_ident rsp_fold_def memb_cons_iff) done lemma ffold_raw_rsp_pre: @@ -217,6 +296,44 @@ "(op = ===> op = ===> op \ ===> op =) ffold_raw ffold_raw" by (simp add: memb_def[symmetric] ffold_raw_rsp_pre) +lemma concat_rsp_pre: + assumes a: "list_rel op \ x x'" + and b: "x' \ y'" + and c: "list_rel op \ y' y" + and d: "\x\set x. xa \ set x" + shows "\x\set y. xa \ set x" +proof - + obtain xb where e: "xb \ set x" and f: "xa \ set xb" using d by auto + have "\y. y \ set x' \ xb \ y" by (rule list_rel_find_element[OF e a]) + then obtain ya where h: "ya \ set x'" and i: "xb \ ya" by auto + have j: "ya \ set y'" using b h by simp + have "\yb. yb \ set y \ ya \ yb" by (rule list_rel_find_element[OF j c]) + then show ?thesis using f i by auto +qed + +lemma [quot_respect]: + shows "(list_rel op \ OOO op \ ===> op \) concat concat" +proof (rule fun_relI, elim pred_compE) + fix a b ba bb + assume a: "list_rel op \ a ba" + assume b: "ba \ bb" + assume c: "list_rel op \ bb b" + have "\x. (\xa\set a. x \ set xa) = (\xa\set b. x \ set xa)" proof + fix x + show "(\xa\set a. x \ set xa) = (\xa\set b. x \ set xa)" proof + assume d: "\xa\set a. x \ set xa" + show "\xa\set b. x \ set xa" by (rule concat_rsp_pre[OF a b c d]) + next + assume e: "\xa\set b. x \ set xa" + have a': "list_rel op \ ba a" by (rule list_rel_symp[OF list_eq_equivp, OF a]) + have b': "bb \ ba" by (rule equivp_symp[OF list_eq_equivp, OF b]) + have c': "list_rel op \ b bb" by (rule list_rel_symp[OF list_eq_equivp, OF c]) + show "\xa\set a. x \ set xa" by (rule concat_rsp_pre[OF c' b' a' e]) + qed + qed + then show "concat a \ concat b" by simp +qed + text {* Distributive lattice with bot *} lemma sub_list_not_eq: @@ -375,11 +492,124 @@ "fin :: 'a \ 'a fset \ bool" is "memb" abbreviation - fnotin :: "'a \ 'a fset \ bool" ("_ |\| _" [50, 51] 50) + fnotin :: "'a \ 'a fset \ bool" (infix "|\|" 50) where "x |\| S \ \ (x |\| S)" -section {* Augmenting an fset -- @{const finsert} *} +section {* Other constants on the Quotient Type *} + +quotient_definition + "fcard :: 'a fset \ nat" +is + "fcard_raw" + +quotient_definition + "fmap :: ('a \ 'b) \ 'a fset \ 'b fset" +is + "map" + +quotient_definition + "fdelete :: 'a fset \ 'a \ 'a fset" + is "delete_raw" + +quotient_definition + "fset_to_set :: 'a fset \ 'a set" + is "set" + +quotient_definition + "ffold :: ('a \ 'b \ 'b) \ 'b \ 'a fset \ 'b" + is "ffold_raw" + +quotient_definition + "fconcat :: ('a fset) fset \ 'a fset" +is + "concat" + +text {* Compositional Respectfullness and Preservation *} + +lemma [quot_respect]: "(list_rel op \ OOO op \) [] []" + by (fact compose_list_refl) + +lemma [quot_preserve]: "(abs_fset \ map f) [] = abs_fset []" + by simp + +lemma [quot_respect]: + "(op \ ===> list_rel op \ OOO op \ ===> list_rel op \ OOO op \) op # op #" + apply auto + apply (simp add: set_in_eq) + apply (rule_tac b="x # b" in pred_compI) + apply auto + apply (rule_tac b="x # ba" in pred_compI) + apply auto + done + +lemma [quot_preserve]: + "(rep_fset ---> (map rep_fset \ rep_fset) ---> (abs_fset \ map abs_fset)) op # = finsert" + by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset] + abs_o_rep[OF Quotient_fset] map_id finsert_def) + +lemma [quot_preserve]: + "((map rep_fset \ rep_fset) ---> (map rep_fset \ rep_fset) ---> (abs_fset \ map abs_fset)) op @ = funion" + by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset] + abs_o_rep[OF Quotient_fset] map_id sup_fset_def) + +lemma list_rel_app_l: + assumes a: "reflp R" + and b: "list_rel R l r" + shows "list_rel R (z @ l) (z @ r)" + by (induct z) (simp_all add: b rev_iffD1[OF a meta_eq_to_obj_eq[OF reflp_def]]) + +lemma append_rsp2_pre0: + assumes a:"list_rel op \ x x'" + shows "list_rel op \ (x @ z) (x' @ z)" + using a apply (induct x x' rule: list_induct2') + by simp_all (rule list_rel_refl) + +lemma append_rsp2_pre1: + assumes a:"list_rel op \ x x'" + shows "list_rel op \ (z @ x) (z @ x')" + using a apply (induct x x' arbitrary: z rule: list_induct2') + apply (rule list_rel_refl) + apply (simp_all del: list_eq.simps) + apply (rule list_rel_app_l) + apply (simp_all add: reflp_def) + done + +lemma append_rsp2_pre: + assumes a:"list_rel op \ x x'" + and b: "list_rel op \ z z'" + shows "list_rel op \ (x @ z) (x' @ z')" + apply (rule list_rel_transp[OF fset_equivp]) + apply (rule append_rsp2_pre0) + apply (rule a) + using b apply (induct z z' rule: list_induct2') + apply (simp_all only: append_Nil2) + apply (rule list_rel_refl) + apply simp_all + apply (rule append_rsp2_pre1) + apply simp + done + +lemma [quot_respect]: + "(list_rel op \ OOO op \ ===> list_rel op \ OOO op \ ===> list_rel op \ OOO op \) op @ op @" +proof (intro fun_relI, elim pred_compE) + fix x y z w x' z' y' w' :: "'a list list" + assume a:"list_rel op \ x x'" + and b: "x' \ y'" + and c: "list_rel op \ y' y" + assume aa: "list_rel op \ z z'" + and bb: "z' \ w'" + and cc: "list_rel op \ w' w" + have a': "list_rel op \ (x @ z) (x' @ z')" using a aa append_rsp2_pre by auto + have b': "x' @ z' \ y' @ w'" using b bb by simp + have c': "list_rel op \ (y' @ w') (y @ w)" using c cc append_rsp2_pre by auto + have d': "(op \ OO list_rel op \) (x' @ z') (y @ w)" + by (rule pred_compI) (rule b', rule c') + show "(list_rel op \ OOO op \) (x @ z) (y @ w)" + by (rule pred_compI) (rule a', rule d') +qed + +text {* Raw theorems. Finsert, memb, singleron, sub_list *} lemma nil_not_cons: shows "\ ([] \ x # xs)" @@ -398,30 +628,20 @@ shows "memb x xs \ memb x (y # xs)" by (simp add: memb_def) -section {* Singletons *} - lemma singleton_list_eq: shows "[x] \ [y] \ x = y" by (simp add: id_simps) auto -section {* sub_list *} - lemma sub_list_cons: "sub_list (x # xs) ys = (memb x ys \ sub_list xs ys)" by (auto simp add: memb_def sub_list_def) -section {* Cardinality of finite sets *} - -quotient_definition - "fcard :: 'a fset \ nat" -is - "fcard_raw" +text {* Cardinality of finite sets *} lemma fcard_raw_0: shows "fcard_raw xs = 0 \ xs \ []" by (induct xs) (auto simp add: memb_def) - lemma fcard_raw_not_memb: shows "\ memb x xs \ fcard_raw (x # xs) = Suc (fcard_raw xs)" by auto @@ -432,7 +652,7 @@ using a by (induct xs) (auto simp add: memb_def split: if_splits) -lemma singleton_fcard_1: +lemma singleton_fcard_1: shows "set xs = {x} \ fcard_raw xs = 1" by (induct xs) (auto simp add: memb_def subset_insert) @@ -451,11 +671,7 @@ assumes a: "fcard_raw A = Suc n" shows "\a. memb a A" using a - apply (induct A) - apply simp - apply (rule_tac x="a" in exI) - apply (simp add: memb_def) - done + by (induct A) (auto simp add: memb_def) lemma memb_card_not_0: assumes a: "memb a A" @@ -466,12 +682,7 @@ then show ?thesis using fcard_raw_0[of A] by simp qed -section {* fmap *} - -quotient_definition - "fmap :: ('a \ 'b) \ 'a fset \ 'b fset" -is - "map" +text {* fmap *} lemma map_append: "map f (xs @ ys) \ (map f xs) @ (map f ys)" @@ -526,28 +737,10 @@ "fcard_raw (delete_raw xs y) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)" by (simp add: fdelete_raw_filter fcard_raw_delete_one) - - - - lemma finter_raw_empty: "finter_raw l [] = []" by (induct l) (simp_all add: not_memb_nil) -section {* Constants on the Quotient Type *} - -quotient_definition - "fdelete :: 'a fset \ 'a \ 'a fset" - is "delete_raw" - -quotient_definition - "fset_to_set :: 'a fset \ 'a set" - is "set" - -quotient_definition - "ffold :: ('a \ 'b \ 'b) \ 'b \ 'a fset \ 'b" - is "ffold_raw" - lemma set_cong: shows "(set x = set y) = (x \ y)" by auto @@ -556,12 +749,6 @@ "inj f \ (map f l \ map f m) = (l \ m)" by (simp add: expand_set_eq[symmetric] inj_image_eq_iff) -quotient_definition - "fconcat :: ('a fset) fset \ 'a fset" -is - "concat" - - text {* alternate formulation with a different decomposition principle and a proof of equivalence *} @@ -604,42 +791,44 @@ "xs \ ys \ delete_raw xs x \ delete_raw ys x" by (simp add: memb_def[symmetric] memb_delete_raw) -lemma list_eq2_equiv_aux: - assumes a: "fcard_raw l = n" - and b: "l \ r" - shows "list_eq2 l r" -using a b -proof (induct n arbitrary: l r) - case 0 - have "fcard_raw l = 0" by fact - then have "\x. \ memb x l" using memb_card_not_0[of _ l] by auto - then have z: "l = []" using no_memb_nil by auto - then have "r = []" using `l \ r` by simp - then show ?case using z list_eq2_refl by simp -next - case (Suc m) - have b: "l \ r" by fact - have d: "fcard_raw l = Suc m" by fact - have "\a. memb a l" by (rule fcard_raw_suc_memb[OF d]) - then obtain a where e: "memb a l" by auto - then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b by auto - have f: "fcard_raw (delete_raw l a) = m" using fcard_raw_delete[of l a] e d by simp - have g: "delete_raw l a \ delete_raw r a" using delete_raw_rsp[OF b] by simp - have g': "list_eq2 (delete_raw l a) (delete_raw r a)" by (rule Suc.hyps[OF f g]) - have h: "list_eq2 (a # delete_raw l a) (a # delete_raw r a)" by (rule list_eq2.intros(5)[OF g']) - have i: "list_eq2 l (a # delete_raw l a)" by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]]) - have "list_eq2 l (a # delete_raw r a)" by (rule list_eq2.intros(6)[OF i h]) - then show ?case using list_eq2.intros(6)[OF _ memb_delete_list_eq2[OF e']] by simp -qed - lemma list_eq2_equiv: "(l \ r) \ (list_eq2 l r)" proof show "list_eq2 l r \ l \ r" by (induct rule: list_eq2.induct) auto - show "l \ r \ list_eq2 l r" using list_eq2_equiv_aux by blast +next + { + fix n + assume a: "fcard_raw l = n" and b: "l \ r" + have "list_eq2 l r" + using a b + proof (induct n arbitrary: l r) + case 0 + have "fcard_raw l = 0" by fact + then have "\x. \ memb x l" using memb_card_not_0[of _ l] by auto + then have z: "l = []" using no_memb_nil by auto + then have "r = []" using `l \ r` by simp + then show ?case using z list_eq2_refl by simp + next + case (Suc m) + have b: "l \ r" by fact + have d: "fcard_raw l = Suc m" by fact + have "\a. memb a l" by (rule fcard_raw_suc_memb[OF d]) + then obtain a where e: "memb a l" by auto + then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b by auto + have f: "fcard_raw (delete_raw l a) = m" using fcard_raw_delete[of l a] e d by simp + have g: "delete_raw l a \ delete_raw r a" using delete_raw_rsp[OF b] by simp + have g': "list_eq2 (delete_raw l a) (delete_raw r a)" by (rule Suc.hyps[OF f g]) + have h: "list_eq2 (a # delete_raw l a) (a # delete_raw r a)" by (rule list_eq2.intros(5)[OF g']) + have i: "list_eq2 l (a # delete_raw l a)" + by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]]) + have "list_eq2 l (a # delete_raw r a)" by (rule list_eq2.intros(6)[OF i h]) + then show ?case using list_eq2.intros(6)[OF _ memb_delete_list_eq2[OF e']] by simp + qed + } + then show "l \ r \ list_eq2 l r" by blast qed -section {* lifted part *} +text {* Lifted theorems *} lemma not_fin_fnil: "x |\| {||}" by (lifting not_memb_nil) @@ -742,10 +931,6 @@ shows "S |\| {||} = S" by (lifting append_Nil2) -thm sup.commute[where 'a="'a fset"] - -thm sup.assoc[where 'a="'a fset"] - lemma singleton_union_left: "{|a|} |\| S = finsert a S" by simp @@ -779,15 +964,7 @@ case (finsert x S) have asm: "P S" by fact show "P (finsert x S)" - proof(cases "x |\| S") - case True - have "x |\| S" by fact - then show "P (finsert x S)" using asm by simp - next - case False - have "x |\| S" by fact - then show "P (finsert x S)" using prem2 asm by simp - qed + by (cases "x |\| S") (simp_all add: asm prem2) qed lemma fset_induct2: @@ -876,7 +1053,8 @@ "(finsert x xs |\| ys) = (x |\| ys \ xs |\| ys)" by (lifting sub_list_cons) -thm sub_list_def[simplified memb_def[symmetric], quot_lifted, no_vars] +lemma "xs |\| ys \ \x. x |\| xs \ x |\| ys" + by (lifting sub_list_def[simplified memb_def[symmetric]]) lemma fsubset_fin: "xs |\| ys = (\x. x |\| xs \ x |\| ys)" by (rule meta_eq_to_obj_eq) @@ -911,6 +1089,19 @@ using assms by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]]) +text {* concat *} + +lemma fconcat_empty: + shows "fconcat {||} = {||}" + by (lifting concat.simps(1)) + +lemma fconcat_insert: + shows "fconcat (finsert x S) = x |\| fconcat S" + by (lifting concat.simps(2)) + +lemma "fconcat (xs |\| ys) = fconcat xs |\| fconcat ys" + by (lifting concat_append) + ML {* fun dest_fsetT (Type ("FSet.fset", [T])) = T | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); diff -r a0c7290a4e27 -r 27cdc0a3a763 Nominal/Manual/Term8.thy --- a/Nominal/Manual/Term8.thy Wed Apr 21 12:25:52 2010 +0200 +++ b/Nominal/Manual/Term8.thy Mon Apr 26 10:01:13 2010 +0200 @@ -1,5 +1,5 @@ theory Term8 -imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove" +imports "../../Nominal-General/Nominal2_Atoms" "../../Nominal-General/Nominal2_Eqvt" "../../Nominal-General/Nominal2_Supp" "../Abs" "../Perm" "../Fv" "../Rsp" "../Lift" "../../Attic/Prove" begin atom_decl name @@ -20,42 +20,55 @@ setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term8.rfoo8") 2 *} print_theorems -local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term8.rfoo8") [ - [[[]], [[], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *} +ML define_fv_alpha_export +local_setup {* snd o define_fv_alpha_export (Datatype.the_info @{theory} "Term8.rfoo8") [ + [[], [(SOME (@{term rbv8}, false), 0, 1, AlphaGen)]], [[], [(NONE, 1, 2, AlphaGen)]]] + [(@{term "rbv8"}, 1, [[], [(0, NONE), (2, SOME @{term rbv8})]])] *} notation alpha_rfoo8 ("_ \f' _" [100, 100] 100) and alpha_rbar8 ("_ \b' _" [100, 100] 100) -thm alpha_rfoo8_alpha_rbar8.intros - +thm alpha_rfoo8_alpha_rbar8_alpha_rbv8.intros[no_vars] +thm fv_rbar8.simps fv_rfoo8_fv_rbv8.simps inductive alpha8f :: "rfoo8 \ rfoo8 \ bool" ("_ \f _" [100, 100] 100) and alpha8b :: "rbar8 \ rbar8 \ bool" ("_ \b _" [100, 100] 100) +and + alpha8bv:: "rbar8 \ rbar8 \ bool" ("_ \bv _" [100, 100] 100) where - a1: "a = b \ (Foo0 a) \f (Foo0 b)" -| a2: "a = b \ (Bar0 a) \b (Bar0 b)" -| a3: "b1 \b b2 \ (\pi. (((rbv8 b1), t1) \gen alpha8f fv_rfoo8 pi ((rbv8 b2), t2))) \ Foo1 b1 t1 \f Foo1 b2 t2" -| a4: "v1 = v2 \ (\pi. (({atom x1}, t1) \gen alpha8b fv_rbar8 pi ({atom x2}, t2))) \ Bar1 v1 x1 t1 \b Bar1 v2 x2 t2" + "name = namea \ Foo0 name \f Foo0 namea" +| "\pi. rbar8 \bv rbar8a \ + (rbv8 rbar8, rfoo8) \gen alpha8f fv_rfoo8 pi (rbv8 rbar8a, rfoo8a) \ + Foo1 rbar8 rfoo8 \f Foo1 rbar8a rfoo8a" +| "name = namea \ Bar0 name \b Bar0 namea" +| "\pi. name1 = name1a \ ({atom name2}, rbar8) \gen alpha8b fv_rbv8 pi ({atom name2a}, rbar8a) \ + Bar1 name1 name2 rbar8 \b Bar1 name1a name2a rbar8a" +| "name = namea \ alpha8bv (Bar0 name) (Bar0 namea)" +| "({atom name2}, rbar8) \gen alpha8b fv_rbv8 pi ({atom name2a}, rbar8a) \ + alpha8bv (Bar1 name1 name2 rbar8) (Bar1 name1a name2a rbar8a)" lemma "(alpha8b ===> op =) rbv8 rbv8" - apply simp apply clarify - apply (erule alpha8f_alpha8b.inducts(2)) + apply rule + apply (induct_tac a b rule: alpha8f_alpha8b_alpha8bv.inducts(2)) apply (simp_all) -done + done lemma fv_rbar8_rsp_hlp: "x \b y \ fv_rbar8 x = fv_rbar8 y" - apply (erule alpha8f_alpha8b.inducts(2)) + apply (erule alpha8f_alpha8b_alpha8bv.inducts(2)) apply (simp_all add: alpha_gen) -done + apply clarify + sorry + lemma "(alpha8b ===> op =) fv_rbar8 fv_rbar8" apply simp apply clarify apply (simp add: fv_rbar8_rsp_hlp) -done + done lemma "(alpha8f ===> op =) fv_rfoo8 fv_rfoo8" apply simp apply clarify - apply (erule alpha8f_alpha8b.inducts(1)) + apply (erule alpha8f_alpha8b_alpha8bv.inducts(1)) apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp) + done end diff -r a0c7290a4e27 -r 27cdc0a3a763 Nominal/NewParser.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/NewParser.thy Mon Apr 26 10:01:13 2010 +0200 @@ -0,0 +1,510 @@ +theory NewParser +imports "../Nominal-General/Nominal2_Atoms" + "../Nominal-General/Nominal2_Eqvt" + "../Nominal-General/Nominal2_Supp" + "Perm" "Equivp" "Rsp" "Lift" +begin + +section{* Interface for nominal_datatype *} + + +ML {* +(* nominal datatype parser *) +local + structure P = OuterParse; + structure S = Scan + + fun triple1 ((x, y), z) = (x, y, z) + fun triple2 (x, (y, z)) = (x, y, z) + fun tuple ((x, y, z), u) = (x, y, z, u) + fun tswap (((x, y), z), u) = (x, y, u, z) +in + +val _ = OuterKeyword.keyword "bind" +val _ = OuterKeyword.keyword "bind_set" +val _ = OuterKeyword.keyword "bind_res" + +val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ + +val bind_mode = P.$$$ "bind" || P.$$$ "bind_set" || P.$$$ "bind_res" + +val bind_clauses = + P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple1) + +val cnstr_parser = + P.binding -- S.repeat anno_typ -- bind_clauses -- P.opt_mixfix >> tswap + +(* datatype parser *) +val dt_parser = + (P.type_args -- P.binding -- P.opt_mixfix >> triple1) -- + (P.$$$ "=" |-- P.enum1 "|" cnstr_parser) >> tuple + +(* binding function parser *) +val bnfun_parser = + S.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([], []) + +(* main parser *) +val main_parser = + P.and_list1 dt_parser -- bnfun_parser >> triple2 + +end +*} + +ML {* +datatype bmodes = + BEmy of int +| BLst of ((term option * int) list) * (int list) +| BSet of ((term option * int) list) * (int list) +| BRes of ((term option * int) list) * (int list) +*} + +ML {* +fun get_cnstrs dts = + map (fn (_, _, _, constrs) => constrs) dts + +fun get_typed_cnstrs dts = + flat (map (fn (_, bn, _, constrs) => + (map (fn (bn', _, _) => (Binding.name_of bn, Binding.name_of bn')) constrs)) dts) + +fun get_cnstr_strs dts = + map (fn (bn, _, _) => Binding.name_of bn) (flat (get_cnstrs dts)) + +fun get_bn_fun_strs bn_funs = + map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs +*} + +ML {* +fun add_primrec_wrapper funs eqs lthy = + if null funs then (([], []), lthy) + else + let + val eqs' = map (fn (_, eq) => (Attrib.empty_binding, eq)) eqs + val funs' = map (fn (bn, ty, mx) => (bn, SOME ty, mx)) funs + in + Primrec.add_primrec funs' eqs' lthy + end +*} + +ML {* +fun add_datatype_wrapper dt_names dts = +let + val conf = Datatype.default_config +in + Local_Theory.theory_result (Datatype.add_datatype conf dt_names dts) +end +*} + + +text {* Infrastructure for adding "_raw" to types and terms *} + +ML {* +fun add_raw s = s ^ "_raw" +fun add_raws ss = map add_raw ss +fun raw_bind bn = Binding.suffix_name "_raw" bn + +fun replace_str ss s = + case (AList.lookup (op=) ss s) of + SOME s' => s' + | NONE => s + +fun replace_typ ty_ss (Type (a, Ts)) = Type (replace_str ty_ss a, map (replace_typ ty_ss) Ts) + | replace_typ ty_ss T = T + +fun raw_dts ty_ss dts = +let + fun raw_dts_aux1 (bind, tys, mx) = + (raw_bind bind, map (replace_typ ty_ss) tys, mx) + + fun raw_dts_aux2 (ty_args, bind, mx, constrs) = + (ty_args, raw_bind bind, mx, map raw_dts_aux1 constrs) +in + map raw_dts_aux2 dts +end + +fun replace_aterm trm_ss (Const (a, T)) = Const (replace_str trm_ss a, T) + | replace_aterm trm_ss (Free (a, T)) = Free (replace_str trm_ss a, T) + | replace_aterm trm_ss trm = trm + +fun replace_term trm_ss ty_ss trm = + trm |> Term.map_aterms (replace_aterm trm_ss) |> map_types (replace_typ ty_ss) +*} + +ML {* +fun rawify_dts dt_names dts dts_env = +let + val raw_dts = raw_dts dts_env dts + val raw_dt_names = add_raws dt_names +in + (raw_dt_names, raw_dts) +end +*} + +ML {* +fun rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs = +let + val bn_funs' = map (fn (bn, ty, mx) => + (raw_bind bn, replace_typ dts_env ty, mx)) bn_funs + + val bn_eqs' = map (fn (attr, trm) => + (attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm)) bn_eqs +in + (bn_funs', bn_eqs') +end +*} + +ML {* +fun rawify_bclauses dts_env cnstrs_env bn_fun_env bclauses = +let + fun rawify_bnds bnds = + map (apfst (Option.map (replace_term (cnstrs_env @ bn_fun_env) dts_env))) bnds + + fun rawify_bclause (BEmy n) = BEmy n + | rawify_bclause (BLst (bnds, bdys)) = BLst (rawify_bnds bnds, bdys) + | rawify_bclause (BSet (bnds, bdys)) = BSet (rawify_bnds bnds, bdys) + | rawify_bclause (BRes (bnds, bdys)) = BRes (rawify_bnds bnds, bdys) +in + map (map (map rawify_bclause)) bclauses +end +*} + +text {* What does the prep_bn code do? Cezary's Function? *} + +ML {* +fun strip_bn_fun t = + case t of + Const (@{const_name sup}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r + | Const (@{const_name append}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r + | Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y => + (i, NONE) :: strip_bn_fun y + | Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y => + (i, NONE) :: strip_bn_fun y + | Const (@{const_name bot}, _) => [] + | Const (@{const_name Nil}, _) => [] + | (f as Free _) $ Bound i => [(i, SOME f)] + | _ => error ("Unsupported binding function: " ^ (PolyML.makestring t)) +*} + +ML {* +fun find [] _ = error ("cannot find element") + | find ((x, z)::xs) y = if (Long_Name.base_name x) = y then z else find xs y +*} + +ML {* +fun prep_bn dt_names dts eqs = +let + fun aux eq = + let + val (lhs, rhs) = eq + |> strip_qnt_body "all" + |> HOLogic.dest_Trueprop + |> HOLogic.dest_eq + val (bn_fun, [cnstr]) = strip_comb lhs + val (_, ty) = dest_Free 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 rhs_elements = strip_bn_fun rhs + val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements + in + (dt_index, (bn_fun, (cnstr_head, included))) + end + fun order dts i ts = + let + val dt = nth dts i + val cts = map (fn (x, _, _) => Binding.name_of x) ((fn (_, _, _, x) => x) dt) + val ts' = map (fn (x, y) => (fst (dest_Const x), y)) ts + in + map (find ts') cts + end + + val unordered = AList.group (op=) (map aux eqs) + val unordered' = map (fn (x, y) => (x, AList.group (op=) y)) unordered + val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered' +in + ordered +end +*} + + +ML {* +fun raw_nominal_decls dts bn_funs bn_eqs binds lthy = +let + val thy = ProofContext.theory_of lthy + val thy_name = Context.theory_name thy + + val dt_names = map (fn (_, s, _, _) => Binding.name_of s) dts + val dt_full_names = map (Long_Name.qualify thy_name) dt_names + val dt_full_names' = add_raws dt_full_names + val dts_env = dt_full_names ~~ dt_full_names' + + val cnstrs = get_cnstr_strs dts + val cnstrs_ty = get_typed_cnstrs dts + val cnstrs_full_names = map (Long_Name.qualify thy_name) cnstrs + val cnstrs_full_names' = map (fn (x, y) => Long_Name.qualify thy_name + (Long_Name.qualify (add_raw x) (add_raw y))) cnstrs_ty + val cnstrs_env = cnstrs_full_names ~~ cnstrs_full_names' + + val bn_fun_strs = get_bn_fun_strs bn_funs + val bn_fun_strs' = add_raws bn_fun_strs + val bn_fun_env = bn_fun_strs ~~ bn_fun_strs' + val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name)) + (bn_fun_strs ~~ bn_fun_strs') + + val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env + + val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs + + val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds + + val raw_bns = prep_bn dt_full_names' raw_dts (map snd raw_bn_eqs) +in + lthy + |> add_datatype_wrapper raw_dt_names raw_dts + ||>> add_primrec_wrapper raw_bn_funs raw_bn_eqs + ||>> pair raw_bclauses + ||>> pair raw_bns +end +*} + +ML {* +fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = +let + val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_bclauses), raw_bns), lthy1) = + raw_nominal_decls dts bn_funs bn_eqs bclauses lthy + + val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names); + val {descr, sorts, ...} = dtinfo; + + val ((raw_perm_def, raw_perm_simps, perms), lthy2) = + Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy1; +in + ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy2) +end +*} + +section {* Preparing and parsing of the specification *} + +ML {* +(* parsing the datatypes and declaring *) +(* constructors in the local theory *) +fun prepare_dts dt_strs lthy = +let + val thy = ProofContext.theory_of lthy + + fun mk_type full_tname tvrs = + Type (full_tname, map (fn a => TVar ((a, 0), [])) tvrs) + + fun prep_cnstr full_tname tvs (cname, anno_tys, mx, _) = + let + val tys = map (Syntax.read_typ lthy o snd) anno_tys + val ty = mk_type full_tname tvs + in + ((cname, tys ---> ty, mx), (cname, tys, mx)) + end + + fun prep_dt (tvs, tname, mx, cnstrs) = + let + val full_tname = Sign.full_name thy tname + val (cnstrs', cnstrs'') = + split_list (map (prep_cnstr full_tname tvs) cnstrs) + in + (cnstrs', (tvs, tname, mx, cnstrs'')) + end + + val (cnstrs, dts) = split_list (map prep_dt dt_strs) +in + lthy + |> Local_Theory.theory (Sign.add_consts_i (flat cnstrs)) + |> pair dts +end +*} + +ML {* +(* parsing the binding function specification and *) +(* declaring the functions in the local theory *) +fun prepare_bn_funs bn_fun_strs bn_eq_strs lthy = +let + val ((bn_funs, bn_eqs), _) = + Specification.read_spec bn_fun_strs bn_eq_strs lthy + + fun prep_bn_fun ((bn, T), mx) = (bn, T, mx) + + val bn_funs' = map prep_bn_fun bn_funs +in + lthy + |> Local_Theory.theory (Sign.add_consts_i bn_funs') + |> pair (bn_funs', bn_eqs) +end +*} + +text {* associates every SOME with the index in the list; drops NONEs *} +ML {* +fun indexify xs = +let + fun mapp _ [] = [] + | mapp i (NONE :: xs) = mapp (i + 1) xs + | mapp i (SOME x :: xs) = (x, i) :: mapp (i + 1) xs +in + mapp 0 xs +end + +fun index_lookup xs x = + case AList.lookup (op=) xs x of + SOME x => x + | NONE => error ("Cannot find " ^ x ^ " as argument annotation."); +*} + +ML {* +fun prepare_bclauses dt_strs lthy = +let + val annos_bclauses = + get_cnstrs dt_strs + |> map (map (fn (_, antys, _, bns) => (map fst antys, bns))) + + fun prep_binder env bn_str = + case (Syntax.read_term lthy bn_str) of + Free (x, _) => (NONE, index_lookup env x) + | Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), index_lookup env x) + | _ => error ("The term " ^ bn_str ^ " is not allowed as binding function.") + + fun prep_body env bn_str = index_lookup env bn_str + + fun prep_mode "bind" = BLst + | prep_mode "bind_set" = BSet + | prep_mode "bind_res" = BRes + + fun prep_bclause env (mode, binders, bodies) = + let + val binders' = map (prep_binder env) binders + val bodies' = map (prep_body env) bodies + in + prep_mode mode (binders', bodies') + end + + fun prep_bclauses (annos, bclause_strs) = + let + val env = indexify annos (* for every label, associate the index *) + in + map (prep_bclause env) bclause_strs + end +in + map (map prep_bclauses) annos_bclauses +end +*} + +text {* + adds an empty binding clause for every argument + that is not already part of a binding clause +*} + +ML {* +fun included i bcs = +let + fun incl (BEmy j) = i = j + | incl (BLst (bns, bds)) = (i mem (map snd bns)) orelse (i mem bds) + | incl (BSet (bns, bds)) = (i mem (map snd bns)) orelse (i mem bds) + | incl (BRes (bns, bds)) = (i mem (map snd bns)) orelse (i mem bds) +in + exists incl bcs +end +*} + +ML {* +fun complete dt_strs bclauses = +let + val args = + get_cnstrs dt_strs + |> map (map (fn (_, antys, _, _) => length antys)) + + fun complt n bcs = + let + fun add bcs i = (if included i bcs then [] else [BEmy i]) + in + bcs @ (flat (map_range (add bcs) n)) + end +in + map2 (map2 complt) args bclauses +end +*} + +ML {* +fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy = +let + fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx) + val lthy0 = + Local_Theory.theory (Sign.add_types (map prep_typ dt_strs)) lthy + val (dts, lthy1) = prepare_dts dt_strs lthy0 + val ((bn_funs, bn_eqs), lthy2) = prepare_bn_funs bn_fun_strs bn_eq_strs lthy1 + val bclauses = prepare_bclauses dt_strs lthy2 + val bclauses' = complete dt_strs bclauses +in + nominal_datatype2 dts bn_funs bn_eqs bclauses' lthy |> snd +end + + +(* Command Keyword *) + +val _ = OuterSyntax.local_theory "nominal_datatype" "test" OuterKeyword.thy_decl + (main_parser >> nominal_datatype2_cmd) +*} + + + +atom_decl name + +nominal_datatype exp = + EVar name +| EUnit +| EPair q1::exp q2::exp bind_set q1 q2 in q1 q2 +| ELetRec l::lrbs e::exp bind "b_lrbs l" in e l + +and fnclause = + K x::name p::pat f::exp bind_res "b_pat p" in f + +and fnclauses = + S fnclause +| ORs fnclause fnclauses + +and lrb = + Clause fnclauses + +and lrbs = + Single lrb +| More lrb lrbs + +and pat = + PVar name +| PUnit +| PPair pat pat + +binder + b_lrbs :: "lrbs \ atom set" and + b_pat :: "pat \ atom set" and + b_fnclauses :: "fnclauses \ atom set" and + b_fnclause :: "fnclause \ atom set" and + b_lrb :: "lrb \ atom set" + +where + "b_lrbs (Single l) = b_lrb l" +| "b_lrbs (More l ls) = b_lrb l \ b_lrbs ls" +| "b_pat (PVar x) = {atom x}" +| "b_pat (PUnit) = {}" +| "b_pat (PPair p1 p2) = b_pat p1 \ b_pat p2" +| "b_fnclauses (S fc) = (b_fnclause fc)" +| "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \ (b_fnclauses fcs)" +| "b_lrb (Clause fcs) = (b_fnclauses fcs)" +| "b_fnclause (K x pat exp) = {atom x}" + + +typ exp_raw +thm exp_raw_fnclause_raw_fnclauses_raw_lrb_raw_lrbs_raw_pat_raw.induct[no_vars] +thm b_fnclause_raw_b_fnclauses_raw_b_lrb_raw_b_lrbs_raw_b_pat_raw.simps[no_vars] +thm permute_exp_raw_permute_fnclause_raw_permute_fnclauses_raw_permute_lrb_raw_permute_lrbs_raw_permute_pat_raw.simps[no_vars] + + + + +end + + + diff -r a0c7290a4e27 -r 27cdc0a3a763 Nominal/Nominal2_FSet.thy --- a/Nominal/Nominal2_FSet.thy Wed Apr 21 12:25:52 2010 +0200 +++ b/Nominal/Nominal2_FSet.thy Mon Apr 26 10:01:13 2010 +0200 @@ -71,55 +71,6 @@ apply (simp add: atom_fmap_cong) done -lemma supp_atom_insert: - "finite (xs :: atom set) \ supp (insert x xs) = supp x \ supp xs" - apply (simp add: supp_finite_atom_set) - apply (simp add: supp_atom) - done - -lemma atom_image_cong: - shows "(atom ` X = atom ` Y) = (X = Y)" - apply(rule inj_image_eq_iff) - apply(simp add: inj_on_def) - done - -lemma atom_eqvt_raw: - fixes p::"perm" - shows "(p \ atom) = atom" - apply(perm_simp) - apply(simp) - done - -lemma supp_finite_at_set: - fixes S::"('a :: at) set" - assumes a: "finite S" - shows "supp S = atom ` S" - apply(rule finite_supp_unique) - apply(simp add: supports_def) - apply (rule finite_induct[OF a]) - apply (simp add: eqvts) - apply (simp) - apply clarify - apply (subst atom_image_cong[symmetric]) - apply (subst atom_eqvt_raw[symmetric]) - apply (subst eqvts[symmetric]) - apply (rule swap_set_not_in) - apply simp_all - apply(rule finite_imageI) - apply(rule a) - apply (subst atom_image_cong[symmetric]) - apply (subst atom_eqvt_raw[symmetric]) - apply (subst eqvts[symmetric]) - apply (rule swap_set_in) - apply simp_all - done - -lemma supp_at_insert: - "finite (xs :: ('a :: at) set) \ supp (insert x xs) = supp x \ supp xs" - apply (simp add: supp_finite_at_set) - apply (simp add: supp_at_base) - done - lemma supp_atom_finsert: "supp (finsert (x :: atom) S) = supp x \ supp S" apply (subst supp_fset_to_set[symmetric]) @@ -129,7 +80,8 @@ done lemma supp_at_finsert: - "supp (finsert (x :: 'a :: at) S) = supp x \ supp S" + fixes S::"('a::at) fset" + shows "supp (finsert x S) = supp x \ supp S" apply (subst supp_fset_to_set[symmetric]) apply (simp add: supp_finite_atom_set) apply (simp add: supp_at_insert[OF fin_fset_to_set]) diff -r a0c7290a4e27 -r 27cdc0a3a763 Nominal/Parser.thy --- a/Nominal/Parser.thy Wed Apr 21 12:25:52 2010 +0200 +++ b/Nominal/Parser.thy Mon Apr 26 10:01:13 2010 +0200 @@ -625,9 +625,14 @@ map_index (prep_typ binds) annos end + val result = map (map (map (map (fn (a, b, c) => + (a, b, c, if !alpha_type=AlphaLst andalso a = NONE then AlphaGen else !alpha_type))))) + (map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs))) + + val _ = warning (@{make_string} result) + in - map (map (map (map (fn (a, b, c) => (a, b, c, if !alpha_type=AlphaLst andalso a = NONE then AlphaGen else !alpha_type))))) - (map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs))) + result end *} diff -r a0c7290a4e27 -r 27cdc0a3a763 PAPER-TODO --- a/PAPER-TODO Wed Apr 21 12:25:52 2010 +0200 +++ b/PAPER-TODO Mon Apr 26 10:01:13 2010 +0200 @@ -12,9 +12,6 @@ I didn't quite get top of second column, p. 6 -"the problem Pottier and Cheney pointed out": I had forgotten it in the -meantime - the equation in the first actuall bullet on p. 8 lacks it =? missing v. spaces, top of 2nd col p. 8 \ No newline at end of file diff -r a0c7290a4e27 -r 27cdc0a3a763 Paper/Paper.thy --- a/Paper/Paper.thy Wed Apr 21 12:25:52 2010 +0200 +++ b/Paper/Paper.thy Mon Apr 26 10:01:13 2010 +0200 @@ -338,7 +338,7 @@ (Note that this means also the term-constructors for variables, applications and lambda are lifted to the quotient level.) This construction, of course, only works if alpha-equivalence is indeed an equivalence relation, and the - lifted definitions and theorems are respectful w.r.t.~alpha-equivalence. + ``raw'' definitions and theorems are respectful w.r.t.~alpha-equivalence. For example, we will not be able to lift a bound-variable function. Although this function can be defined for raw terms, it does not respect alpha-equivalence and therefore cannot be lifted. To sum up, every lifting @@ -352,7 +352,7 @@ known as Core-Haskell (see Figure~\ref{corehas}). This term language involves patterns that have lists of type-, coercion- and term-variables, all of which are bound in @{text "\"}-expressions. One - difficulty is that we do not know in advance how many variables need to + feature is that we do not know in advance how many variables need to be bound. Another is that each bound variable comes with a kind or type annotation. Representing such binders with single binders and reasoning about them in a theorem prover would be a major pain. \medskip @@ -932,9 +932,9 @@ \begin{center} \begin{tabular}{l} - \isacommand{bind}\; {\it binder}\; \isacommand{in}\; {\it label}\\ - \isacommand{bind\_set}\; {\it binder}\; \isacommand{in}\; {\it label}\\ - \isacommand{bind\_res}\; {\it binder}\; \isacommand{in}\; {\it label}\\ + \isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it labels}\\ + \isacommand{bind\_set}\; {\it binders}\; \isacommand{in}\; {\it labels}\\ + \isacommand{bind\_res}\; {\it binders}\; \isacommand{in}\; {\it labels}\\ \end{tabular} \end{center} @@ -943,15 +943,15 @@ the second is for sets of binders (the order does not matter, but the cardinality does) and the last is for sets of binders (with vacuous binders preserving alpha-equivalence). The ``\isacommand{in}-part'' of a binding - clause will be called the \emph{body}; the ``\isacommand{bind}-part'' will - be called the \emph{binder}. + clause will be called \emph{body}; the ``\isacommand{bind}-part'' will + be called \emph{binder}. In addition we distinguish between \emph{shallow} and \emph{deep} - binders. Shallow binders are of the form \isacommand{bind}\; {\it label}\; - \isacommand{in}\; {\it label'} (similar for the other two modes). The - restriction we impose on shallow binders is that the {\it label} must either - refer to a type that is an atom type or to a type that is a finite set or - list of an atom type. Two examples for the use of shallow binders are the + binders. Shallow binders are of the form \isacommand{bind}\; {\it labels}\; + \isacommand{in}\; {\it labels'} (similar for the other two modes). The + restriction we impose on shallow binders is that the {\it labels} must either + refer to atom types or to finite sets or + lists of atom types. Two examples for the use of shallow binders are the specification of lambda-terms, where a single name is bound, and type-schemes, where a finite set of names is bound: @@ -1111,8 +1111,9 @@ Having dealt with all syntax matters, the problem now is how we can turn specifications into actual type definitions in Isabelle/HOL and then - establish a reasoning infrastructure for them. Because of the problem - Pottier and Cheney pointed out, we cannot in general re-arrange arguments of + establish a reasoning infrastructure for them. As + Pottier and Cheney pointed out \cite{Pottier06,Cheney5}, we cannot in general + re-arrange arguments of term-constructors so that binders and their bodies are next to each other, and then use the type constructors @{text "abs_set"}, @{text "abs_res"} and @{text "abs_list"} from Section \ref{sec:binders}. Therefore we will first