52 split_conj_thm (Goal.prove lthy ("pi1" :: "pi2" :: perm_indnames) [] gl tac) |
52 split_conj_thm (Goal.prove lthy ("pi1" :: "pi2" :: perm_indnames) [] gl tac) |
53 end; |
53 end; |
54 *} |
54 *} |
55 |
55 |
56 ML {* |
56 ML {* |
57 (* TODO: full_name can be obtained from new_type_names with Datatype *) |
57 fun define_raw_perms (dt_info : info) number thy = |
58 fun define_raw_perms new_type_names full_tnames thy = |
|
59 let |
58 let |
60 val {descr, induct, ...} = Datatype.the_info thy (hd full_tnames); |
59 val {descr, induct, sorts, ...} = dt_info; |
61 (* TODO: [] should be the sorts that we'll take from the specification *) |
60 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; |
62 val sorts = []; |
61 val full_tnames = List.take (all_full_tnames, number); |
63 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
62 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
64 val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) => |
63 val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) => |
65 "permute_" ^ name_of_typ (nth_dtyp i)) descr); |
64 "permute_" ^ name_of_typ (nth_dtyp i)) descr); |
66 val perm_types = map (fn (i, _) => |
65 val perm_types = map (fn (i, _) => |
67 let val T = nth_dtyp i |
66 let val T = nth_dtyp i |
99 Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; |
98 Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; |
100 (* TODO: Use the version of prmrec that gives the names explicitely. *) |
99 (* TODO: Use the version of prmrec that gives the names explicitely. *) |
101 val ((perm_frees, perm_ldef), lthy') = |
100 val ((perm_frees, perm_ldef), lthy') = |
102 Primrec.add_primrec |
101 Primrec.add_primrec |
103 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy; |
102 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy; |
104 val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, length new_type_names); |
103 val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, number); |
105 val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, length new_type_names) |
104 val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, number) |
106 val perms_name = space_implode "_" perm_names' |
105 val perms_name = space_implode "_" perm_names' |
107 val perms_zero_bind = Binding.name (perms_name ^ "_zero") |
106 val perms_zero_bind = Binding.name (perms_name ^ "_zero") |
108 val perms_append_bind = Binding.name (perms_name ^ "_append") |
107 val perms_append_bind = Binding.name (perms_name ^ "_append") |
109 fun tac _ (_, simps, _) = |
108 fun tac _ (_, simps, _) = |
110 (Class.intro_classes_tac []) THEN (ALLGOALS (resolve_tac simps)); |
109 (Class.intro_classes_tac []) THEN (ALLGOALS (resolve_tac simps)); |