6 *) |
6 *) |
7 |
7 |
8 signature TFL = |
8 signature TFL = |
9 sig |
9 sig |
10 val define_i: bool -> theory -> claset -> simpset -> thm list -> thm list -> xstring -> |
10 val define_i: bool -> theory -> claset -> simpset -> thm list -> thm list -> xstring -> |
11 term -> term list -> theory * {rules: (thm * int) list, induct: thm, tcs: term list} |
11 term -> term list -> theory * {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} |
12 val define: bool -> theory -> claset -> simpset -> thm list -> thm list -> xstring -> |
12 val define: bool -> theory -> claset -> simpset -> thm list -> thm list -> xstring -> |
13 string -> string list -> theory * {rules: (thm * int) list, induct: thm, tcs: term list} |
13 string -> string list -> theory * {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} |
14 val defer_i: theory -> thm list -> xstring -> term list -> theory * thm |
14 val defer_i: theory -> thm list -> xstring -> term list -> theory * thm |
15 val defer: theory -> thm list -> xstring -> string list -> theory * thm |
15 val defer: theory -> thm list -> xstring -> string list -> theory * thm |
16 end; |
16 end; |
17 |
17 |
18 structure Tfl: TFL = |
18 structure Tfl: TFL = |
202 * Defining a function with an associated termination relation. |
202 * Defining a function with an associated termination relation. |
203 *---------------------------------------------------------------------------*) |
203 *---------------------------------------------------------------------------*) |
204 fun define_i strict thy cs ss congs wfs fid R eqs = |
204 fun define_i strict thy cs ss congs wfs fid R eqs = |
205 let val {functional,pats} = Prim.mk_functional thy eqs |
205 let val {functional,pats} = Prim.mk_functional thy eqs |
206 val (thy, def) = Prim.wfrec_definition0 thy (Long_Name.base_name fid) R functional |
206 val (thy, def) = Prim.wfrec_definition0 thy (Long_Name.base_name fid) R functional |
|
207 val (lhs, _) = Logic.dest_equals (prop_of def) |
207 val {induct, rules, tcs} = |
208 val {induct, rules, tcs} = |
208 simplify_defn strict thy cs ss congs wfs fid pats def |
209 simplify_defn strict thy cs ss congs wfs fid pats def |
209 val rules' = |
210 val rules' = |
210 if strict then derive_init_eqs thy rules eqs |
211 if strict then derive_init_eqs thy rules eqs |
211 else rules |
212 else rules |
212 in (thy, {rules = rules', induct = induct, tcs = tcs}) end; |
213 in (thy, {lhs = lhs, rules = rules', induct = induct, tcs = tcs}) end; |
213 |
214 |
214 fun define strict thy cs ss congs wfs fid R seqs = |
215 fun define strict thy cs ss congs wfs fid R seqs = |
215 define_i strict thy cs ss congs wfs fid |
216 define_i strict thy cs ss congs wfs fid |
216 (Syntax.read_term_global thy R) (map (Syntax.read_term_global thy) seqs) |
217 (Syntax.read_term_global thy R) (map (Syntax.read_term_global thy) seqs) |
217 handle U.ERR {mesg,...} => error mesg; |
218 handle U.ERR {mesg,...} => error mesg; |