author | paulson |
Tue, 03 Jun 1997 11:08:08 +0200 | |
changeset 3391 | 5e45dd3b64e9 |
parent 3333 | 0bbf06e86c06 |
child 3405 | 2cccd0e3e9ea |
permissions | -rw-r--r-- |
3302 | 1 |
(* Title: TFL/tfl |
2 |
ID: $Id$ |
|
3 |
Author: Konrad Slind, Cambridge University Computer Laboratory |
|
4 |
Copyright 1997 University of Cambridge |
|
5 |
||
3391
5e45dd3b64e9
More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents:
3333
diff
changeset
|
6 |
Main module |
3302 | 7 |
*) |
8 |
||
2112 | 9 |
signature TFL_sig = |
10 |
sig |
|
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
11 |
datatype pattern = GIVEN of term * int |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
12 |
| OMITTED of term * int |
2112 | 13 |
|
3391
5e45dd3b64e9
More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents:
3333
diff
changeset
|
14 |
val mk_functional : theory -> term list |
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
15 |
-> {functional:term, |
2112 | 16 |
pats: pattern list} |
17 |
||
3333
0bbf06e86c06
Now checks the name of the function being defined;
paulson
parents:
3302
diff
changeset
|
18 |
val wfrec_definition0 : theory -> string -> term -> term -> thm * theory |
3191 | 19 |
|
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
20 |
val post_definition : theory * (thm * pattern list) |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
21 |
-> {theory : theory, |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
22 |
rules : thm, |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
23 |
TCs : term list list, |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
24 |
full_pats_TCs : (term * term list) list, |
3191 | 25 |
patterns : pattern list} |
26 |
||
2112 | 27 |
|
3391
5e45dd3b64e9
More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents:
3333
diff
changeset
|
28 |
val wfrec_eqns : theory -> term list |
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
29 |
-> {WFR : term, |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
30 |
proto_def : term, |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
31 |
extracta :(thm * term list) list, |
2112 | 32 |
pats : pattern list} |
33 |
||
34 |
||
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
35 |
val lazyR_def : theory |
3391
5e45dd3b64e9
More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
paulson
parents:
3333
diff
changeset
|
36 |
-> term list |
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
37 |
-> {theory:theory, |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
38 |
rules :thm, |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
39 |
R :term, |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
40 |
full_pats_TCs :(term * term list) list, |
2112 | 41 |
patterns: pattern list} |
42 |
||
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
43 |
val mk_induction : theory |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
44 |
-> term -> term |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
45 |
-> (term * term list) list |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
46 |
-> thm |
2112 | 47 |
|
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
48 |
val postprocess: {WFtac:tactic, terminator:tactic, simplifier:cterm -> thm} |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
49 |
-> theory |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
50 |
-> {rules:thm, induction:thm, TCs:term list list} |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
51 |
-> {rules:thm, induction:thm, nested_tcs:thm list} |
2112 | 52 |
|
53 |
structure Context |
|
54 |
: sig |
|
3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
55 |
val read : unit -> thm list |
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
3191
diff
changeset
|
56 |
val write : thm list -> unit |
2112 | 57 |
end |
58 |
end; |