--- 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
*)