# HG changeset patch # User Christian Urban # Date 1291732059 0 # Node ID b136721eedb23ab958038d9c9bc83a59108babe6 # Parent 0f289a52edbe9dd16926797448d5a5af0d8400af automated permute_bn theorems diff -r 0f289a52edbe -r b136721eedb2 Nominal/Ex/CoreHaskell.thy --- a/Nominal/Ex/CoreHaskell.thy Tue Dec 07 14:27:21 2010 +0000 +++ b/Nominal/Ex/CoreHaskell.thy Tue Dec 07 14:27:39 2010 +0000 @@ -86,6 +86,7 @@ (* generated theorems *) +thm core_haskell.permute_bn thm core_haskell.perm_bn_alpha thm core_haskell.perm_bn_simps thm core_haskell.bn_finite diff -r 0f289a52edbe -r b136721eedb2 Nominal/Ex/Foo1.thy --- a/Nominal/Ex/Foo1.thy Tue Dec 07 14:27:21 2010 +0000 +++ b/Nominal/Ex/Foo1.thy Tue Dec 07 14:27:39 2010 +0000 @@ -35,6 +35,7 @@ | "bn4 (BNil) = {}" | "bn4 (BAs a as) = {atom a} \ bn4 as" +thm foo.permute_bn thm foo.perm_bn_alpha thm foo.perm_bn_simps thm foo.bn_finite @@ -55,43 +56,6 @@ thm foo.fresh thm foo.bn_finite - -lemma tt1: - shows "(p \ bn1 as) = bn1 (permute_bn1 p as)" -apply(induct as rule: foo.inducts(2)) -apply(auto)[7] -apply(simp add: foo.perm_bn_simps foo.bn_defs) -apply(simp add: atom_eqvt) -apply(auto) -done - -lemma tt2: - shows "(p \ bn2 as) = bn2 (permute_bn2 p as)" -apply(induct as rule: foo.inducts(2)) -apply(auto)[7] -apply(simp add: foo.perm_bn_simps foo.bn_defs) -apply(simp add: atom_eqvt) -apply(auto) -done - -lemma tt3: - shows "(p \ bn3 as) = bn3 (permute_bn3 p as)" -apply(induct as rule: foo.inducts(2)) -apply(auto)[7] -apply(simp add: foo.perm_bn_simps foo.bn_defs) -apply(simp add: atom_eqvt) -apply(auto) -done - -lemma tt4: - shows "(p \ bn4 as) = bn4 (permute_bn4 p as)" -apply(induct as rule: foo.inducts(3)) -apply(auto)[8] -apply(simp add: foo.perm_bn_simps foo.bn_defs permute_set_eq) -apply(simp add: foo.perm_bn_simps foo.bn_defs) -apply(simp add: atom_eqvt insert_eqvt) -done - lemma strong_exhaust1: fixes c::"'a::fs" assumes "\name. y = Var name \ P" diff -r 0f289a52edbe -r b136721eedb2 Nominal/Ex/Foo2.thy --- a/Nominal/Ex/Foo2.thy Tue Dec 07 14:27:21 2010 +0000 +++ b/Nominal/Ex/Foo2.thy Tue Dec 07 14:27:39 2010 +0000 @@ -24,6 +24,8 @@ "bn (As x y t a) = [atom x] @ bn a" | "bn (As_Nil) = []" +thm foo.bn_defs +thm foo.permute_bn thm foo.perm_bn_alpha thm foo.perm_bn_simps thm foo.bn_finite @@ -43,57 +45,61 @@ thm foo.supp thm foo.fresh -lemma tt1: - shows "(p \ bn as) = bn (permute_bn p as)" -apply(induct as rule: foo.inducts(2)) -apply(auto)[5] -apply(simp only: foo.perm_bn_simps foo.bn_defs) -apply(perm_simp) -apply(simp only:) -apply(simp only: foo.perm_bn_simps foo.bn_defs) -apply(perm_simp add: foo.fv_bn_eqvt) -apply(simp only:) -done - text {* tests by cu *} -lemma yy: +lemma set_renaming_perm: assumes a: "p \ bs \ bs = {}" and b: "finite bs" shows "\q. q \ bs = p \ bs \ supp q \ bs \ (p \ bs)" using b a -apply(induct) -apply(simp add: permute_set_eq) -apply(rule_tac x="0" in exI) -apply(simp add: supp_perm) -apply(perm_simp) -apply(drule meta_mp) -apply(auto simp add: fresh_star_def fresh_finite_insert)[1] -apply(erule exE) -apply(simp) -apply(case_tac "q \ x = p \ x") -apply(rule_tac x="q" in exI) -apply(auto)[1] -apply(rule_tac x="((q \ x) \ (p \ x)) + q" in exI) -apply(subgoal_tac "p \ x \ p \ F") -apply(subgoal_tac "q \ x \ p \ F") -apply(simp add: swap_set_not_in) -apply(rule subset_trans) -apply(rule supp_plus_perm) -apply(simp) -apply(rule conjI) -apply(simp add: supp_swap) -apply(simp add: supp_perm) -apply(auto)[1] -apply(auto)[1] -apply(erule conjE)+ -apply(drule sym) -apply(simp add: mem_permute_iff) -apply(simp add: mem_permute_iff) -done - +proof (induct) + case empty + have "0 \ {} = p \ {} \ supp (0::perm) \ {} \ p \ {}" + by (simp add: permute_set_eq supp_perm) + then show "\q. q \ {} = p \ {} \ supp q \ {} \ p \ {}" by blast +next + case (insert a bs) + then have " \q. q \ bs = p \ bs \ supp q \ bs \ p \ bs" + by (perm_simp) (auto) + then obtain q where *: "q \ bs = p \ bs" and **: "supp q \ bs \ p \ bs" by blast + { assume 1: "q \ a = p \ a" + have "q \ insert a bs = p \ insert a bs" using 1 * by (simp add: insert_eqvt) + moreover + have "supp q \ insert a bs \ p \ insert a bs" + using ** by (auto simp add: insert_eqvt) + ultimately + have "\q. q \ insert a bs = p \ insert a bs \ supp q \ insert a bs \ p \ insert a bs" by blast + } + moreover + { assume 2: "q \ a \ p \ a" + def q' \ "((q \ a) \ (p \ a)) + q" + { have "(q \ a) \ (p \ bs)" using `a \ bs` *[symmetric] by (simp add: mem_permute_iff) + moreover + have "(p \ a) \ (p \ bs)" using `a \ bs` by (simp add: mem_permute_iff) + ultimately + have "q' \ insert a bs = p \ insert a bs" using 2 * unfolding q'_def + by (simp add: insert_eqvt swap_set_not_in) + } + moreover + { have "{q \ a, p \ a} \ insert a bs \ p \ insert a bs" + using ** `a \ bs` `p \ insert a bs \ insert a bs = {}` + by (auto simp add: supp_perm insert_eqvt) + then have "supp (q \ a \ p \ a) \ insert a bs \ p \ insert a bs" by (simp add: supp_swap) + moreover + have "supp q \ insert a bs \ p \ insert a bs" + using ** by (auto simp add: 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. q \ insert a bs = p \ insert a bs \ supp q \ insert a bs \ p \ insert a bs" by blast + } + ultimately show "\q. q \ insert a bs = p \ insert a bs \ supp q \ insert a bs \ p \ insert a bs" + by blast +qed lemma Abs_rename_set: @@ -103,7 +109,8 @@ shows "\y. [bs]set. x = [p \ bs]set. y" proof - from a b have "p \ bs \ bs = {}" using at_fresh_star_inter by (auto simp add: fresh_star_Pair) - with yy obtain q where *: "q \ bs = p \ bs" and **: "supp q \ bs \ (p \ bs)" using b by metis + with set_renaming_perm + obtain q where *: "q \ bs = p \ bs" and **: "supp q \ bs \ (p \ bs)" using b by metis have "[bs]set. x = q \ ([bs]set. x)" apply(rule perm_supp_eq[symmetric]) using a ** @@ -124,7 +131,8 @@ shows "\y. [bs]res. x = [p \ bs]res. y" proof - from a b have "p \ bs \ bs = {}" using at_fresh_star_inter by (simp add: fresh_star_Pair) - with yy obtain q where *: "q \ bs = p \ bs" and **: "supp q \ bs \ (p \ bs)" using b by metis + with set_renaming_perm + obtain q where *: "q \ bs = p \ bs" and **: "supp q \ bs \ (p \ bs)" using b by metis have "[bs]res. x = q \ ([bs]res. x)" apply(rule perm_supp_eq[symmetric]) using a ** @@ -138,54 +146,60 @@ then show "\y. [bs]res. x = [p \ bs]res. y" by blast qed -lemma zz0: - assumes "p \ bs = q \ bs" - and a: "a \ set bs" - shows "p \ a = q \ a" -using assms -by (induct bs) (auto) - -lemma zz: +lemma list_renaming_perm: fixes bs::"atom list" - assumes "(p \ (set bs)) \ (set bs) = {}" + assumes a: "(p \ (set bs)) \ (set bs) = {}" shows "\q. q \ bs = p \ bs \ supp q \ (set bs) \ (p \ (set bs))" -using assms -apply(induct bs) -apply(simp add: permute_set_eq) -apply(rule_tac x="0" in exI) -apply(simp add: supp_perm) -apply(drule meta_mp) -apply(perm_simp) -apply(auto)[1] -apply(erule exE) -apply(simp) -apply(case_tac "a \ set bs") -apply(rule_tac x="q" in exI) -apply(perm_simp) -apply(auto dest: zz0)[1] -apply(subgoal_tac "q \ a \ p \ bs") -apply(subgoal_tac "p \ a \ p \ bs") -apply(rule_tac x="((q \ a) \ (p \ a)) + q" in exI) -apply(simp add: swap_fresh_fresh) -apply(rule subset_trans) -apply(rule supp_plus_perm) -apply(simp) -apply(rule conjI) -apply(simp add: supp_swap) -apply(simp add: supp_perm) -apply(perm_simp) -apply(auto simp add: fresh_def supp_of_atom_list)[1] -apply(perm_simp) -apply(auto)[1] -apply(simp add: fresh_permute_iff) -apply(simp add: fresh_def supp_of_atom_list) -apply(erule conjE)+ -apply(drule sym) -apply(drule sym) -apply(simp) -apply(simp add: fresh_permute_iff) -apply(auto simp add: fresh_def supp_of_atom_list)[1] -done +using a +proof (induct bs) + case Nil + have "0 \ [] = p \ [] \ supp (0::perm) \ set [] \ p \ set []" + by (simp add: permute_set_eq supp_perm) + then show "\q. q \ [] = p \ [] \ supp q \ set [] \ p \ (set [])" by blast +next + case (Cons a bs) + then have " \q. q \ bs = p \ bs \ supp q \ set bs \ p \ (set bs)" + by (perm_simp) (auto) + then obtain q where *: "q \ bs = p \ bs" 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 "q \ (a # bs) = p \ (a # bs)" using * by simp + moreover + have "supp q \ set (a # bs) \ p \ (set (a # bs))" using ** by (auto simp add: insert_eqvt) + ultimately + have "\q. q \ (a # bs) = p \ (a # bs) \ supp q \ set (a # bs) \ p \ (set (a # bs))" by blast + } + moreover + { assume 2: "a \ set bs" + def q' \ "((q \ a) \ (p \ a)) + q" + { have "(q \ a) \ (p \ bs)" using `a \ set bs` *[symmetric] + by (simp add: fresh_permute_iff) (simp add: fresh_def supp_of_atom_list) + moreover + have "(p \ a) \ (p \ bs)" using `a \ set bs` + by (simp add: fresh_permute_iff) (simp add: fresh_def supp_of_atom_list) + ultimately + have "q' \ (a # bs) = p \ (a # bs)" using 2 * unfolding q'_def + by (simp add: swap_fresh_fresh) + } + moreover + { have "{q \ a, p \ a} \ set (a # bs) \ p \ (set (a # bs))" + using ** `a \ set bs` `p \ (set (a # bs)) \ set (a # bs) = {}` + by (auto simp add: supp_perm insert_eqvt) + then have "supp (q \ a \ p \ a) \ set (a # bs) \ p \ set (a # bs)" by (simp add: supp_swap) + moreover + have "supp q \ set (a # bs) \ p \ (set (a # bs))" + using ** by (auto simp add: 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. q \ (a # bs) = p \ (a # bs) \ supp q \ set (a # bs) \ p \ (set (a # bs))" by blast + } + ultimately show "\q. q \ (a # bs) = p \ (a # bs) \ supp q \ set (a # bs) \ p \ (set (a # bs))" + by blast +qed + lemma Abs_rename_list: fixes x::"'a::fs" @@ -194,7 +208,8 @@ proof - from a have "p \ (set bs) \ (set bs) = {}" using at_fresh_star_inter by (simp add: fresh_star_Pair fresh_star_set) - with zz obtain q where *: "q \ bs = p \ bs" and **: "supp q \ set bs \ (p \ set bs)" by metis + with list_renaming_perm + obtain q where *: "q \ bs = p \ bs" and **: "supp q \ set bs \ (p \ set bs)" by metis have "[bs]lst. x = q \ ([bs]lst. x)" apply(rule perm_supp_eq[symmetric]) using a ** @@ -208,6 +223,23 @@ then show "\y. [bs]lst. x = [p \ bs]lst. y" by blast qed +(* +thm at_set_avoiding1[THEN exE] + + +lemma Let1_rename: + fixes c::"'a::fs" + shows "\name' trm'. {atom name'} \* c \ Lam name trm = Lam name' trm'" +apply(simp only: foo.eq_iff) +apply(rule at_set_avoiding1[where c="(c, atom name, trm)" and xs="set [atom name]", THEN exE]) +apply(simp) +apply(simp add: finite_supp) +apply(perm_simp) +apply(rule Abs_rename_list[THEN exE]) +apply(simp only: set_eqvt) +apply +sorry +*) lemma test6: fixes c::"'a::fs" @@ -224,6 +256,14 @@ apply(rule assms(2)) apply(rule exI)+ apply(assumption) +(* lam case *) +(* +apply(rule Let1_rename) +apply(rule assms(3)) +apply(assumption) +apply(simp) +*) + apply(subgoal_tac "\p. (p \ {atom name}) \* (c, [atom name], trm)") apply(erule exE) apply(insert Abs_rename_list)[1] @@ -245,10 +285,10 @@ apply(rule at_set_avoiding1) apply(simp) apply(simp add: finite_supp) +(* let1 case *) apply(subgoal_tac "\p. (p \ ((set (bn assg1)) \ (set (bn assg2)))) \* (c, bn assg1, bn assg2, trm1, trm2)") apply(erule exE) apply(rule assms(4)) -apply(simp only:) apply(simp only: foo.eq_iff) apply(insert Abs_rename_list)[1] apply(drule_tac x="p" in meta_spec) @@ -264,7 +304,7 @@ apply(simp only: union_eqvt fresh_star_Pair set.simps fresh_star_Un, simp) apply(erule exE)+ apply(rule exI)+ -apply(perm_simp add: tt1) +apply(perm_simp add: foo.permute_bn) apply(rule conjI) apply(simp add: fresh_star_Pair fresh_star_Un) apply(erule conjE)+ @@ -282,6 +322,7 @@ apply(rule at_set_avoiding1) apply(simp) apply(simp add: finite_supp) +(* let2 case *) apply(subgoal_tac "\p. (p \ ({atom name1} \ {atom name2})) \* (c, atom name1, atom name2, trm1, trm2)") apply(erule exE) apply(rule assms(5)) @@ -309,7 +350,7 @@ apply(auto simp add: fresh_star_def fresh_Pair fresh_Nil fresh_Cons)[1] apply(erule exE)+ apply(rule exI)+ -apply(perm_simp add: tt1) +apply(perm_simp add: foo.permute_bn) apply(rule conjI) prefer 2 apply(rule conjI) diff -r 0f289a52edbe -r b136721eedb2 Nominal/Ex/Multi_Recs2.thy --- a/Nominal/Ex/Multi_Recs2.thy Tue Dec 07 14:27:21 2010 +0000 +++ b/Nominal/Ex/Multi_Recs2.thy Tue Dec 07 14:27:39 2010 +0000 @@ -50,7 +50,7 @@ | "b_fnclause (K x pat exp) = {atom x}" - +thm fun_recs.permute_bn thm fun_recs.perm_bn_alpha thm fun_recs.perm_bn_simps thm fun_recs.bn_finite diff -r 0f289a52edbe -r b136721eedb2 Nominal/Nominal2.thy --- a/Nominal/Nominal2.thy Tue Dec 07 14:27:21 2010 +0000 +++ b/Nominal/Nominal2.thy Tue Dec 07 14:27:39 2010 +0000 @@ -1,15 +1,11 @@ theory Nominal2 imports Nominal2_Base Nominal2_Eqvt Nominal2_Abs -uses ("nominal_dt_rawperm.ML") - ("nominal_dt_rawfuns.ML") +uses ("nominal_dt_rawfuns.ML") ("nominal_dt_alpha.ML") ("nominal_dt_quot.ML") begin -use "nominal_dt_rawperm.ML" -ML {* open Nominal_Dt_RawPerm *} - use "nominal_dt_rawfuns.ML" ML {* open Nominal_Dt_RawFuns *} @@ -614,6 +610,12 @@ qalpha_refl_thms lthyC else [] + (* proving the relationship of bn and permute_bn *) + val qpermute_bn_thms = + if get_STEPS lthy > 33 + then prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qfv_qbn_eqvts lthyC + else [] + (* noting the theorems *) (* generating the prefix for the theorem names *) @@ -641,6 +643,7 @@ ||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps) ||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms) ||>> Local_Theory.note ((thms_suffix "perm_bn_alpha", []), qperm_bn_alpha_thms) + ||>> Local_Theory.note ((thms_suffix "permute_bn", []), qpermute_bn_thms) in (0, lthy9') end handle TEST ctxt => (0, ctxt) diff -r 0f289a52edbe -r b136721eedb2 Nominal/nominal_dt_quot.ML --- a/Nominal/nominal_dt_quot.ML Tue Dec 07 14:27:21 2010 +0000 +++ b/Nominal/nominal_dt_quot.ML Tue Dec 07 14:27:39 2010 +0000 @@ -35,7 +35,9 @@ 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 end structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = @@ -323,6 +325,7 @@ 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 @@ -344,7 +347,31 @@ |> map (simplify (HOL_basic_ss 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, @{typ 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 (HOL_basic_ss addsimps ss), + TRY o Nominal_Permeq.eqvt_strict_tac ctxt' qbn_eqvts [], + TRY o asm_full_simp_tac HOL_basic_ss] + in + induct_prove qtys props qinduct (K ss_tac) ctxt' + |> ProofContext.export ctxt' ctxt + |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) + end end (* structure *) diff -r 0f289a52edbe -r b136721eedb2 Nominal/nominal_dt_rawfuns.ML --- a/Nominal/nominal_dt_rawfuns.ML Tue Dec 07 14:27:21 2010 +0000 +++ b/Nominal/nominal_dt_rawfuns.ML Tue Dec 07 14:27:39 2010 +0000 @@ -2,7 +2,7 @@ Author: Cezary Kaliszyk Author: Christian Urban - Definitions of the raw fv and fv_bn functions + Definitions of the raw fv, fv_bn and permute functions. *) signature NOMINAL_DT_RAWFUNS = @@ -41,6 +41,9 @@ local_theory -> (term list * thm list * local_theory) val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm list + + val define_raw_perms: string list -> typ list -> (string * sort) list -> term list -> thm -> + local_theory -> (term list * thm list * thm list) * local_theory end @@ -368,6 +371,7 @@ HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) end + fun raw_prove_eqvt consts ind_thms simps ctxt = if null consts then [] else @@ -390,5 +394,117 @@ |> ProofContext.export ctxt'' ctxt end + + +(*** raw permutation functions ***) + +(** proves the two pt-type class properties **) + +fun prove_permute_zero induct perm_defs perm_fns lthy = + let + val perm_types = map (body_type o fastype_of) perm_fns + val perm_indnames = 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 simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs) + + val tac = (Datatype_Aux.indtac induct perm_indnames + THEN_ALL_NEW asm_simp_tac simps) 1 + in + Goal.prove lthy perm_indnames [] goals (K tac) + |> Datatype_Aux.split_conj_thm + end + + +fun prove_permute_plus induct perm_defs perm_fns lthy = + let + val p = Free ("p", @{typ perm}) + val q = Free ("q", @{typ perm}) + val perm_types = map (body_type o fastype_of) perm_fns + val perm_indnames = 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 simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs) + + val tac = (Datatype_Aux.indtac induct perm_indnames + THEN_ALL_NEW asm_simp_tac simps) 1 + in + Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac) + |> Datatype_Aux.split_conj_thm + end + + +fun mk_perm_eq ty_perm_assoc cnstr = + let + fun lookup_perm p (ty, arg) = + case (AList.lookup (op=) ty_perm_assoc ty) of + SOME perm => perm $ p $ arg + | NONE => Const (@{const_name permute}, perm_ty ty) $ p $ arg + + val p = Free ("p", @{typ perm}) + val (arg_tys, ty) = + fastype_of cnstr + |> strip_type + + val arg_names = Name.variant_list ["p"] (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 + (Attrib.empty_binding, eq) + end + + +fun define_raw_perms full_ty_names tys tvs constrs induct_thm lthy = + let + val perm_fn_names = full_ty_names + |> map Long_Name.base_name + |> map (prefix "permute_") + + val perm_fn_types = map perm_ty 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 (tys ~~ perm_fn_frees)) constrs + + fun tac _ (_, _, simps) = + Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac 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 (full_ty_names, tvs, @{sort pt}) + |> Primrec.add_primrec perm_fn_binds perm_eqs + + val perm_zero_thms = prove_permute_zero induct_thm perm_eq_thms perm_funs lthy' + val perm_plus_thms = prove_permute_plus induct_thm 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 + + end (* structure *) diff -r 0f289a52edbe -r b136721eedb2 Nominal/nominal_dt_rawperm.ML --- a/Nominal/nominal_dt_rawperm.ML Tue Dec 07 14:27:21 2010 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,130 +0,0 @@ -(* Title: nominal_dt_rawperm.ML - Author: Cezary Kaliszyk - Author: Christian Urban - - Definitions of the raw permutations and - proof that the raw datatypes are in the - pt-class. -*) - -signature NOMINAL_DT_RAWPERM = -sig - val define_raw_perms: string list -> typ list -> (string * sort) list -> term list -> thm -> - local_theory -> (term list * thm list * thm list) * local_theory -end - - -structure Nominal_Dt_RawPerm: NOMINAL_DT_RAWPERM = -struct - - -(** proves the two pt-type class properties **) - -fun prove_permute_zero induct perm_defs perm_fns lthy = - let - val perm_types = map (body_type o fastype_of) perm_fns - val perm_indnames = 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 simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs) - - val tac = (Datatype_Aux.indtac induct perm_indnames - THEN_ALL_NEW asm_simp_tac simps) 1 - in - Goal.prove lthy perm_indnames [] goals (K tac) - |> Datatype_Aux.split_conj_thm - end - - -fun prove_permute_plus induct perm_defs perm_fns lthy = - let - val p = Free ("p", @{typ perm}) - val q = Free ("q", @{typ perm}) - val perm_types = map (body_type o fastype_of) perm_fns - val perm_indnames = 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 simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs) - - val tac = (Datatype_Aux.indtac induct perm_indnames - THEN_ALL_NEW asm_simp_tac simps) 1 - in - Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac) - |> Datatype_Aux.split_conj_thm - end - - -fun mk_perm_eq ty_perm_assoc cnstr = - let - fun lookup_perm p (ty, arg) = - case (AList.lookup (op=) ty_perm_assoc ty) of - SOME perm => perm $ p $ arg - | NONE => Const (@{const_name permute}, perm_ty ty) $ p $ arg - - val p = Free ("p", @{typ perm}) - val (arg_tys, ty) = - fastype_of cnstr - |> strip_type - - val arg_names = Name.variant_list ["p"] (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 - (Attrib.empty_binding, eq) - end - - -fun define_raw_perms full_ty_names tys tvs constrs induct_thm lthy = - let - val perm_fn_names = full_ty_names - |> map Long_Name.base_name - |> map (prefix "permute_") - - val perm_fn_types = map perm_ty 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 (tys ~~ perm_fn_frees)) constrs - - fun tac _ (_, _, simps) = - Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac 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 (full_ty_names, tvs, @{sort pt}) - |> Primrec.add_primrec perm_fn_binds perm_eqs - - val perm_zero_thms = prove_permute_zero induct_thm perm_eq_thms perm_funs lthy' - val perm_plus_thms = prove_permute_plus induct_thm 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 - - -end (* structure *) -