author | wenzelm |
Sat, 01 Apr 2000 20:21:39 +0200 | |
changeset 8657 | b9475dad85ed |
parent 8625 | 93a11ebacf32 |
child 8711 | 00ec2ba9174d |
permissions | -rw-r--r-- |
6429 | 1 |
(* Title: HOL/Tools/recdef_package.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
||
5 |
Wrapper module for Konrad Slind's TFL package. |
|
6 |
*) |
|
7 |
||
8 |
signature RECDEF_PACKAGE = |
|
9 |
sig |
|
10 |
val quiet_mode: bool ref |
|
6439 | 11 |
val print_recdefs: theory -> unit |
8657 | 12 |
val get_recdef: theory -> string |
13 |
-> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option |
|
14 |
val add_recdef: xstring -> string -> ((bstring * string) * Args.src list) list |
|
15 |
-> simpset option -> (xstring * Args.src list) list -> theory |
|
16 |
-> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list} |
|
17 |
val add_recdef_i: xstring -> term -> ((bstring * term) * theory attribute list) list |
|
18 |
-> simpset option -> (thm * theory attribute list) list |
|
19 |
-> theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list} |
|
6557 | 20 |
val defer_recdef: xstring -> string list -> (xstring * Args.src list) list |
21 |
-> theory -> theory * {induct_rules: thm} |
|
22 |
val defer_recdef_i: xstring -> term list -> (thm * theory attribute list) list |
|
23 |
-> theory -> theory * {induct_rules: thm} |
|
6439 | 24 |
val setup: (theory -> theory) list |
6429 | 25 |
end; |
26 |
||
27 |
structure RecdefPackage: RECDEF_PACKAGE = |
|
28 |
struct |
|
29 |
||
30 |
val quiet_mode = Tfl.quiet_mode; |
|
31 |
val message = Tfl.message; |
|
32 |
||
33 |
||
6439 | 34 |
|
35 |
(** theory data **) |
|
36 |
||
37 |
(* data kind 'HOL/recdef' *) |
|
38 |
||
8657 | 39 |
type recdef_info = {simps: thm list, rules: thm list list, induct: thm, tcs: term list}; |
6439 | 40 |
|
41 |
structure RecdefArgs = |
|
42 |
struct |
|
43 |
val name = "HOL/recdef"; |
|
44 |
type T = recdef_info Symtab.table; |
|
45 |
||
46 |
val empty = Symtab.empty; |
|
6557 | 47 |
val copy = I; |
6439 | 48 |
val prep_ext = I; |
49 |
val merge: T * T -> T = Symtab.merge (K true); |
|
50 |
||
51 |
fun print sg tab = |
|
52 |
Pretty.writeln (Pretty.strs ("recdefs:" :: |
|
6851 | 53 |
map #1 (Sign.cond_extern_table sg Sign.constK tab))); |
6439 | 54 |
end; |
55 |
||
56 |
structure RecdefData = TheoryDataFun(RecdefArgs); |
|
57 |
val print_recdefs = RecdefData.print; |
|
6429 | 58 |
|
6439 | 59 |
|
60 |
(* get and put data *) |
|
61 |
||
8481
89d498a8d3f6
get_recdef now returns None instead of raising ERROR.
berghofe
parents:
8430
diff
changeset
|
62 |
fun get_recdef thy name = Symtab.lookup (RecdefData.get thy, name); |
6439 | 63 |
|
64 |
fun put_recdef name info thy = |
|
6429 | 65 |
let |
6439 | 66 |
val tab = Symtab.update_new ((name, info), RecdefData.get thy) |
67 |
handle Symtab.DUP _ => error ("Duplicate recursive function definition " ^ quote name); |
|
68 |
in RecdefData.put tab thy end; |
|
69 |
||
70 |
||
71 |
||
72 |
(** add_recdef(_i) **) |
|
73 |
||
6557 | 74 |
fun requires_recdef thy = Theory.requires thy "Recdef" "recursive functions"; |
75 |
||
8657 | 76 |
fun gen_add_recdef tfl_fn prep_att prep_ss app_thms raw_name R eq_srcs raw_ss raw_congs thy = |
6439 | 77 |
let |
78 |
val name = Sign.intern_const (Theory.sign_of thy) raw_name; |
|
79 |
val bname = Sign.base_name name; |
|
80 |
||
6557 | 81 |
val _ = requires_recdef thy; |
6429 | 82 |
val _ = message ("Defining recursive function " ^ quote name ^ " ..."); |
83 |
||
8657 | 84 |
val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs); |
85 |
val eq_atts = map (map (prep_att thy)) raw_eq_atts; |
|
6429 | 86 |
val ss = (case raw_ss of None => Simplifier.simpset_of thy | Some x => prep_ss x); |
7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7262
diff
changeset
|
87 |
val (thy, congs) = thy |> app_thms raw_congs; |
8657 | 88 |
|
89 |
val (thy, {rules = rules_idx, induct, tcs}) = tfl_fn thy name R (ss, congs) eqs; |
|
90 |
val rules = map (map #1) (Library.partition_eq Library.eq_snd rules_idx); |
|
91 |
val simp_att = if null tcs then [Simplifier.simp_add_global] else []; |
|
92 |
||
8430 | 93 |
val case_numbers = map Library.string_of_int (1 upto Thm.nprems_of induct); |
8657 | 94 |
val (thy, (simps' :: rules', [induct'])) = |
7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7262
diff
changeset
|
95 |
thy |
6439 | 96 |
|> Theory.add_path bname |
8657 | 97 |
|> PureThy.add_thmss ((("simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts)) |
8430 | 98 |
|>>> PureThy.add_thms [(("induct", induct), [RuleCases.case_names case_numbers])]; |
8657 | 99 |
val result = {simps = simps', rules = rules', induct = induct', tcs = tcs}; |
7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7262
diff
changeset
|
100 |
val thy = |
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7262
diff
changeset
|
101 |
thy |
6439 | 102 |
|> put_recdef name result |
6429 | 103 |
|> Theory.parent_path; |
7798
42e94b618f34
return stored thms with proper naming in derivation;
wenzelm
parents:
7262
diff
changeset
|
104 |
in (thy, result) end; |
6429 | 105 |
|
8657 | 106 |
val add_recdef = gen_add_recdef Tfl.define Attrib.global_attribute I IsarThy.apply_theorems; |
107 |
val add_recdef_x = gen_add_recdef Tfl.define Attrib.global_attribute |
|
108 |
(Simplifier.simpset_of o ThyInfo.get_theory) IsarThy.apply_theorems; |
|
109 |
val add_recdef_i = gen_add_recdef Tfl.define_i (K I) I IsarThy.apply_theorems_i; |
|
6429 | 110 |
|
111 |
||
6557 | 112 |
|
113 |
(** defer_recdef(_i) **) |
|
114 |
||
115 |
fun gen_defer_recdef tfl_fn app_thms raw_name eqs raw_congs thy = |
|
116 |
let |
|
117 |
val name = Sign.intern_const (Theory.sign_of thy) raw_name; |
|
118 |
val bname = Sign.base_name name; |
|
119 |
||
120 |
val _ = requires_recdef thy; |
|
121 |
val _ = message ("Deferred recursive function " ^ quote name ^ " ..."); |
|
122 |
||
123 |
val (thy1, congs) = thy |> app_thms raw_congs; |
|
124 |
val (thy2, induct_rules) = tfl_fn thy1 name congs eqs; |
|
8430 | 125 |
val (thy3, [induct_rules']) = |
6557 | 126 |
thy2 |
127 |
|> Theory.add_path bname |
|
128 |
|> PureThy.add_thms [(("induct_rules", induct_rules), [])] |
|
8430 | 129 |
|>> Theory.parent_path; |
130 |
in (thy3, {induct_rules = induct_rules'}) end; |
|
6557 | 131 |
|
132 |
val defer_recdef = gen_defer_recdef Tfl.defer IsarThy.apply_theorems; |
|
133 |
val defer_recdef_i = gen_defer_recdef Tfl.defer_i IsarThy.apply_theorems_i; |
|
134 |
||
135 |
||
136 |
||
6439 | 137 |
(** package setup **) |
138 |
||
139 |
(* setup theory *) |
|
140 |
||
141 |
val setup = [RecdefData.init]; |
|
142 |
||
143 |
||
6429 | 144 |
(* outer syntax *) |
145 |
||
6723 | 146 |
local structure P = OuterParse and K = OuterSyntax.Keyword in |
6429 | 147 |
|
148 |
val recdef_decl = |
|
8657 | 149 |
P.name -- P.term -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment) -- |
6723 | 150 |
Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (P.xthms1 --| P.$$$ ")")) [] -- |
151 |
Scan.option (P.$$$ "(" |-- P.$$$ "simpset" |-- P.!!! (P.name --| P.$$$ ")")) |
|
8657 | 152 |
>> (fn ((((f, R), eqs), congs), ss) => #1 o add_recdef_x f R (map P.triple_swap eqs) ss congs); |
6429 | 153 |
|
154 |
val recdefP = |
|
6723 | 155 |
OuterSyntax.command "recdef" "define general recursive functions (TFL)" K.thy_decl |
6429 | 156 |
(recdef_decl >> Toplevel.theory); |
157 |
||
6557 | 158 |
|
159 |
val defer_recdef_decl = |
|
8657 | 160 |
P.name -- Scan.repeat1 P.prop -- |
6723 | 161 |
Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (P.xthms1 --| P.$$$ ")")) [] |
6557 | 162 |
>> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs); |
163 |
||
164 |
val defer_recdefP = |
|
6723 | 165 |
OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)" K.thy_decl |
6557 | 166 |
(defer_recdef_decl >> Toplevel.theory); |
167 |
||
6429 | 168 |
val _ = OuterSyntax.add_keywords ["congs", "simpset"]; |
6557 | 169 |
val _ = OuterSyntax.add_parsers [recdefP, defer_recdefP]; |
6429 | 170 |
|
171 |
end; |
|
172 |
||
173 |
||
174 |
end; |