# HG changeset patch # User Christian Urban # Date 1271742287 -7200 # Node ID 8e0bfb14f6bfdd761e33562537071a525d65cc37 # Parent f8c8e2afcc18f2e39e00d438481569105efc626c optimised the code of define_raw_perm diff -r f8c8e2afcc18 -r 8e0bfb14f6bf Nominal-General/nominal_library.ML --- a/Nominal-General/nominal_library.ML Mon Apr 19 17:26:07 2010 +0200 +++ b/Nominal-General/nominal_library.ML Tue Apr 20 07:44:47 2010 +0200 @@ -9,6 +9,7 @@ val mk_minus: term -> term val mk_plus: term -> term -> term + val perm_ty: typ -> typ val mk_perm_ty: typ -> term -> term -> term val mk_perm: term -> term -> term val dest_perm: term -> term * term @@ -27,8 +28,10 @@ fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q +fun perm_ty ty = @{typ perm} --> ty --> ty + fun mk_perm_ty ty p trm = - Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm + Const (@{const_name "permute"}, perm_ty ty) $ p $ trm fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm diff -r f8c8e2afcc18 -r 8e0bfb14f6bf Nominal/Perm.thy --- a/Nominal/Perm.thy Mon Apr 19 17:26:07 2010 +0200 +++ b/Nominal/Perm.thy Tue Apr 20 07:44:47 2010 +0200 @@ -59,71 +59,122 @@ end; *} + +(* definitions of the permute function for a raw nominal datatype *) + ML {* -fun define_raw_perms (dt_info : Datatype_Aux.info) number thy = +fun nth_dtyp dt_descr sorts i = + Datatype_Aux.typ_of_dtyp dt_descr sorts (Datatype_Aux.DtRec i); +*} + +ML {* +(* permutation function for one argument *) +fun perm_arg permute_fns pi (arg_dty, arg) = +let + val T = type_of arg +in + if Datatype_Aux.is_rec_type arg_dty + then + let + val (Us, _) = strip_type T + val indxs_tys = (length Us - 1 downto 0) ~~ Us + in + list_abs (map (pair "x") Us, + Free (nth permute_fns (Datatype_Aux.body_index arg_dty)) $ pi $ + list_comb (arg, map (fn (i, U) => (mk_perm_ty U (mk_minus pi) (Bound i))) indxs_tys)) + end + else mk_perm_ty T pi arg +end +*} + +ML {* +(* equation for permutation function for one constructor *) +fun perm_eq_constr thy dt_descr sorts permute_fns i (cnstr_name, dts) = +let + val pi = Free ("p", @{typ perm}) + val arg_tys = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts + val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys) + val args = map Free (arg_names ~~ arg_tys) + val cnstr = Const (cnstr_name, arg_tys ---> (nth_dtyp dt_descr sorts i)) + val lhs = Free (nth permute_fns i) $ pi $ list_comb (cnstr, args) + val rhs = list_comb (cnstr, map (perm_arg permute_fns pi) (dts ~~ args)) + val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) +in + (Attrib.empty_binding, eq) +end +*} + +ML {* +(* defines the permutation functions for raw datatypes and + proves that they are instances of pt +*) +fun define_raw_perms (dt_info : Datatype_Aux.info) dt_nos 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 = Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i); - val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) => - "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; - val perm_names_types' = perm_names' ~~ perm_types; - val pi = Free ("pi", @{typ perm}); - fun perm_eq_constr i (cname, dts) = - let - 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 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' (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))) - end - else (mk_perm_ty T pi x) - end; - in - (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq - (Free (nth perm_names_types' i) $ - Free ("pi", @{typ perm}) $ list_comb (c, args), - list_comb (c, map perm_arg (dts ~~ args))))) - end; - fun perm_eq (i, (_, _, constrs)) = map (perm_eq_constr i) constrs; - val perm_eqs = maps perm_eq descr; - val lthy = - Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; - val ((perm_frees, perm_ldef), lthy') = - Primrec.add_primrec - (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy; - val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, number); - val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, number) - val perms_name = space_implode "_" perm_names' - val perms_zero_bind = Binding.name (perms_name ^ "_zero") - val perms_append_bind = Binding.name (perms_name ^ "_append") - fun tac _ (_, simps, _) = - (Class.intro_classes_tac []) THEN (ALLGOALS (resolve_tac simps)); - fun morphism phi (dfs, simps, fvs) = - (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs); + val {descr as dt_descr, induct, sorts, ...} = dt_info; + val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr; + val full_tnames = List.take (all_full_tnames, dt_nos); + + val perm_fn_names = Datatype_Prop.indexify_names (map (fn (i, _) => + "permute_" ^ Datatype_Aux.name_of_typ (nth_dtyp dt_descr sorts i)) dt_descr); + + val perm_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr + + val permute_fns = perm_fn_names ~~ perm_types + + fun perm_eq (i, (_, _, constrs)) = + map (perm_eq_constr thy dt_descr sorts permute_fns i) constrs; + + val perm_eqs = maps perm_eq dt_descr; + + val lthy = + Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; + + val ((perm_frees, perm_ldef), lthy') = + Primrec.add_primrec + (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy; + + val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, dt_nos); + val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, dt_nos) + val perms_name = space_implode "_" perm_fn_names + val perms_zero_bind = Binding.name (perms_name ^ "_zero") + val perms_append_bind = Binding.name (perms_name ^ "_append") + fun tac _ (_, simps, _) = + (Class.intro_classes_tac []) THEN (ALLGOALS (resolve_tac simps)); + fun morphism phi (dfs, simps, fvs) = + (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs); in - lthy' - |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_empty_thms)) - |> snd o (Local_Theory.note ((perms_append_bind, []), perm_append_thms)) - |> Class_Target.prove_instantiation_exit_result morphism tac - (perm_ldef, (perm_empty_thms @ perm_append_thms), perm_frees) + lthy' + |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_empty_thms)) + |> snd o (Local_Theory.note ((perms_append_bind, []), perm_append_thms)) + |> Class_Target.prove_instantiation_exit_result morphism tac + (perm_ldef, (perm_empty_thms @ perm_append_thms), perm_frees) end +*} +(* Test *) +atom_decl name + +datatype trm = + Var "name" +| App "trm" "trm list" +| Lam "name" "trm" +| Let "bp" "trm" "trm" +and bp = + BUnit +| BVar "name" +| BPair "bp" "bp" + +setup {* fn thy => +let + val info = Datatype.the_info thy "Perm.trm" +in + define_raw_perms info 2 thy |> snd +end *} +print_theorems +*) + ML {* fun define_lifted_perms qtys full_tnames name_term_pairs thms thy = let @@ -171,8 +222,8 @@ -(* Test -atom_decl name +(* Test *) +(*atom_decl name datatype trm = Var "name" @@ -184,8 +235,14 @@ | BVar "name" | BPair "bp" "bp" +setup {* fn thy => +let + val inf = Datatype.the_info thy "Perm.trm" +in + define_raw_perms inf 2 thy |> snd +end +*} -setup {* snd o define_raw_perms ["trm", "bp"] ["Perm.trm", "Perm.bp"] *} print_theorems *)