# HG changeset patch # User Christian Urban # Date 1271688936 -7200 # Node ID 996d4411e95e72a91fe8997aa8008197b1eeea4d # Parent 54ad41f9e505b3e89ace33fe51fa3e475b9a4686 tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability) diff -r 54ad41f9e505 -r 996d4411e95e Nominal-General/nominal_library.ML --- a/Nominal-General/nominal_library.ML Mon Apr 19 15:37:54 2010 +0200 +++ b/Nominal-General/nominal_library.ML Mon Apr 19 16:55:36 2010 +0200 @@ -7,6 +7,8 @@ signature NOMINAL_LIBRARY = sig val mk_minus: term -> term + val mk_plus: term -> term -> term + val mk_perm_ty: typ -> term -> term -> term val mk_perm: term -> term -> term val dest_perm: term -> term * term @@ -20,7 +22,10 @@ struct fun mk_minus p = - Const (@{const_name "uminus"}, @{typ "perm => perm"}) $ p + @{term "uminus::perm => perm"} $ p + +fun mk_plus p q = + @{term "plus::perm => perm => perm"} $ p $ q fun mk_perm_ty ty p trm = Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm diff -r 54ad41f9e505 -r 996d4411e95e Nominal/Fv.thy --- a/Nominal/Fv.thy Mon Apr 19 15:37:54 2010 +0200 +++ b/Nominal/Fv.thy Mon Apr 19 16:55:36 2010 +0200 @@ -274,7 +274,6 @@ end; *} -ML {* fun add_perm (p1, p2) = Const(@{const_name plus}, @{typ "perm \ perm \ perm"}) $ p1 $ p2 *} ML {* fun non_rec_binds l = @@ -596,7 +595,7 @@ val fv = mk_compound_fv fvs; val alphas = map (nth alpha_frees) ((body_index dt) :: bound_in_ty_nos); val alpha = mk_compound_alpha alphas; - val pi = foldr1 add_perm (distinct (op =) rpis); + val pi = foldr1 (uncurry mk_plus) (distinct (op =) rpis); val alpha_gen_pre = Const (atyp_const atyp, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; val alpha_gen = Syntax.check_term lthy alpha_gen_pre in @@ -618,7 +617,7 @@ val rhs = mk_pair (rhs_binds, arg2); val alpha = nth alpha_frees (body_index dt); val fv = nth fv_frees (body_index dt); - val pi = foldr1 add_perm (distinct (op =) rpis); + val pi = foldr1 (uncurry mk_plus) (distinct (op =) rpis); val alpha_const = alpha_const_for_binds rbinds; val alpha_gen_pre = Const (alpha_const, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; val alpha_gen = Syntax.check_term lthy alpha_gen_pre diff -r 54ad41f9e505 -r 996d4411e95e Nominal/Perm.thy --- a/Nominal/Perm.thy Mon Apr 19 15:37:54 2010 +0200 +++ b/Nominal/Perm.thy Mon Apr 19 16:55:36 2010 +0200 @@ -3,11 +3,6 @@ begin ML {* - open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *) - open Nominal_Library; -*} - -ML {* fun quotient_lift_consts_export qtys spec ctxt = let val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt; @@ -26,54 +21,53 @@ val perm_types = map fastype_of perm_frees; val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); fun glc ((perm, T), x) = - HOLogic.mk_eq (perm $ @{term "0 :: perm"} $ Free (x, T), Free (x, T)) + HOLogic.mk_eq (perm $ @{term "0::perm"} $ Free (x, T), Free (x, T)) val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames))); fun tac _ = EVERY [ - indtac induct perm_indnames 1, + Datatype_Aux.indtac induct perm_indnames 1, ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_zero} :: perm_def))) ]; in - split_conj_thm (Goal.prove lthy perm_indnames [] gl tac) + Datatype_Aux.split_conj_thm (Goal.prove lthy perm_indnames [] gl tac) end; *} ML {* fun prove_perm_append lthy induct perm_def perm_frees = let - val add_perm = @{term "op + :: (perm \ perm \ perm)"} val pi1 = Free ("pi1", @{typ perm}); val pi2 = Free ("pi2", @{typ perm}); val perm_types = map fastype_of perm_frees val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); fun glc ((perm, T), x) = HOLogic.mk_eq ( - perm $ (add_perm $ pi1 $ pi2) $ Free (x, T), + perm $ (mk_plus pi1 pi2) $ Free (x, T), perm $ pi1 $ (perm $ pi2 $ Free (x, T))) - val gl = + val goal = (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames)))) fun tac _ = EVERY [ - indtac induct perm_indnames 1, + Datatype_Aux.indtac induct perm_indnames 1, ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_plus} :: perm_def))) ] in - split_conj_thm (Goal.prove lthy ("pi1" :: "pi2" :: perm_indnames) [] gl tac) + Datatype_Aux.split_conj_thm (Goal.prove lthy ("pi1" :: "pi2" :: perm_indnames) [] goal tac) end; *} ML {* -fun define_raw_perms (dt_info : info) number thy = +fun define_raw_perms (dt_info : Datatype_Aux.info) number thy = let val {descr, induct, sorts, ...} = dt_info; val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; val full_tnames = List.take (all_full_tnames, number); - fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); + fun nth_dtyp i = Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i); val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) => - "permute_" ^ name_of_typ (nth_dtyp i)) descr); + "permute_" ^ Datatype_Aux.name_of_typ (nth_dtyp i)) descr); val perm_types = map (fn (i, _) => let val T = nth_dtyp i in @{typ perm} --> T --> T end) descr; @@ -81,17 +75,17 @@ val pi = Free ("pi", @{typ perm}); fun perm_eq_constr i (cname, dts) = let - val Ts = map (typ_of_dtyp descr sorts) dts; + val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) dts; val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); val args = map Free (names ~~ Ts); val c = Const (cname, Ts ---> (nth_dtyp i)); fun perm_arg (dt, x) = let val T = type_of x in - if is_rec_type dt then + if Datatype_Aux.is_rec_type dt then let val (Us, _) = strip_type T in list_abs (map (pair "x") Us, - Free (nth perm_names_types' (body_index dt)) $ pi $ + Free (nth perm_names_types' (Datatype_Aux.body_index dt)) $ pi $ list_comb (x, map (fn (i, U) => (mk_perm_ty U (mk_minus pi) (Bound i))) ((length Us - 1 downto 0) ~~ Us))) @@ -180,18 +174,18 @@ (* Test atom_decl name -datatype rtrm1 = - rVr1 "name" -| rAp1 "rtrm1" "rtrm1 list" -| rLm1 "name" "rtrm1" -| rLt1 "bp" "rtrm1" "rtrm1" +datatype trm = + Var "name" +| App "trm" "trm list" +| Lam "name" "trm" +| Let "bp" "trm" "trm" and bp = BUnit -| BVr "name" -| BPr "bp" "bp" +| BVar "name" +| BPair "bp" "bp" -setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Perm.rtrm1", "Perm.bp"] *} +setup {* snd o define_raw_perms ["trm", "bp"] ["Perm.trm", "Perm.bp"] *} print_theorems *)