author | haftmann |
Fri, 20 Apr 2007 17:58:26 +0200 | |
changeset 22760 | 6eafeffe801c |
parent 22733 | 0b14bb35be90 |
child 22846 | fb79144af9a3 |
permissions | -rw-r--r-- |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/function_package/fundef_common.ML |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
2 |
ID: $Id$ |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
3 |
Author: Alexander Krauss, TU Muenchen |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
4 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
5 |
A package for general recursive function definitions. |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
6 |
Common type definitions and other infrastructure. |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
7 |
*) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
8 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
9 |
structure FundefCommon = |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
10 |
struct |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
11 |
|
22498
62cdd4b3e96b
made function syntax strict, requiring | to separate equations; cleanup
krauss
parents:
22279
diff
changeset
|
12 |
(* Profiling *) |
21255
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset
|
13 |
val profile = ref false; |
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset
|
14 |
|
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset
|
15 |
fun PROFILE msg = if !profile then timeap_msg msg else I |
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset
|
16 |
|
22498
62cdd4b3e96b
made function syntax strict, requiring | to separate equations; cleanup
krauss
parents:
22279
diff
changeset
|
17 |
|
62cdd4b3e96b
made function syntax strict, requiring | to separate equations; cleanup
krauss
parents:
22279
diff
changeset
|
18 |
val acc_const_name = "Accessible_Part.acc" |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20289
diff
changeset
|
19 |
fun mk_acc domT R = |
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
20 |
Const (acc_const_name, (domT --> domT --> HOLogic.boolT) --> domT --> HOLogic.boolT) $ R |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
21 |
|
21319
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21255
diff
changeset
|
22 |
val function_name = suffix "C" |
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21255
diff
changeset
|
23 |
val graph_name = suffix "_graph" |
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21255
diff
changeset
|
24 |
val rel_name = suffix "_rel" |
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21255
diff
changeset
|
25 |
val dom_name = suffix "_dom" |
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21255
diff
changeset
|
26 |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
27 |
type depgraph = int IntGraph.T |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
28 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
29 |
datatype ctx_tree |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
30 |
= Leaf of term |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
31 |
| Cong of (term * thm * depgraph * ((string * typ) list * thm list * ctx_tree) list) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
32 |
| RCall of (term * ctx_tree) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
33 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
34 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
35 |
|
19583
c5fa77b03442
function-package: Changed record usage to make sml/nj happy...
krauss
parents:
19564
diff
changeset
|
36 |
datatype fundef_result = |
c5fa77b03442
function-package: Changed record usage to make sml/nj happy...
krauss
parents:
19564
diff
changeset
|
37 |
FundefResult of |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
38 |
{ |
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
39 |
fs: term list, |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20289
diff
changeset
|
40 |
G: term, |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20289
diff
changeset
|
41 |
R: term, |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset
|
42 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20289
diff
changeset
|
43 |
psimps : thm list, |
22166 | 44 |
trsimps : thm list option, |
45 |
||
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset
|
46 |
subset_pinducts : thm list, |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset
|
47 |
simple_pinducts : thm list, |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset
|
48 |
cases : thm, |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset
|
49 |
termination : thm, |
22166 | 50 |
domintros : thm list option |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset
|
51 |
} |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset
|
52 |
|
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
53 |
|
21255
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset
|
54 |
datatype fundef_context_data = |
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset
|
55 |
FundefCtxData of |
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset
|
56 |
{ |
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
57 |
defname : string, |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
58 |
|
22166 | 59 |
add_simps : string -> Attrib.src list -> thm list -> local_theory -> thm list * local_theory, |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19617
diff
changeset
|
60 |
|
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
61 |
fs : term list, |
21255
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset
|
62 |
R : term, |
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset
|
63 |
|
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset
|
64 |
psimps: thm list, |
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset
|
65 |
pinducts: thm list, |
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset
|
66 |
termination: thm |
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset
|
67 |
} |
617fdb08abe9
added profiling code, improved handling of proof terms, generation of domain
krauss
parents:
21237
diff
changeset
|
68 |
|
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
69 |
fun morph_fundef_data phi (FundefCtxData {add_simps, fs, R, psimps, pinducts, termination, defname}) = |
22623 | 70 |
let |
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
71 |
val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
72 |
val name = Morphism.name phi |
22623 | 73 |
in |
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
74 |
FundefCtxData { add_simps = add_simps (* contains no logical entities *), |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
75 |
fs = map term fs, R = term R, psimps = fact psimps, |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
76 |
pinducts = fact pinducts, termination = thm termination, |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
77 |
defname = name defname } |
22623 | 78 |
end |
79 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20289
diff
changeset
|
80 |
structure FundefData = GenericDataFun |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
81 |
(struct |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
82 |
val name = "HOL/function_def/data"; |
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
83 |
type T = (term * fundef_context_data) NetRules.T |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
84 |
|
22760 | 85 |
val empty = NetRules.init |
86 |
(op aconv o pairself fst : (term * fundef_context_data) * (term * fundef_context_data) -> bool) |
|
87 |
fst; |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
88 |
val copy = I; |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
89 |
val extend = I; |
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
90 |
fun merge _ (tab1, tab2) = NetRules.merge (tab1, tab2) |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
91 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
92 |
fun print _ _ = (); |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
93 |
end); |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
94 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
95 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
96 |
structure FundefCongs = GenericDataFun |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
97 |
(struct |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
98 |
val name = "HOL/function_def/congs" |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
99 |
type T = thm list |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
100 |
val empty = [] |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
101 |
val extend = I |
21319
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21255
diff
changeset
|
102 |
fun merge _ = Drule.merge_rules |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
103 |
fun print _ _ = () |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
104 |
end); |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
105 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
106 |
|
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
107 |
(* Generally useful?? *) |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
108 |
fun lift_morphism thy f = |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
109 |
let |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
110 |
val term = Drule.term_rule thy f |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
111 |
in |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
112 |
Morphism.thm_morphism f $> Morphism.term_morphism term $> Morphism.typ_morphism (Logic.type_map term) |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
113 |
end |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
114 |
|
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
115 |
fun import_fundef_data t ctxt = |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
116 |
let |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
117 |
val thy = Context.theory_of ctxt |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
118 |
val ct = cterm_of thy t |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
119 |
val inst_morph = lift_morphism thy o Thm.instantiate |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
120 |
|
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
121 |
fun match data = |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
122 |
SOME (morph_fundef_data (inst_morph (Thm.cterm_match (cterm_of thy (fst data), ct))) (snd data)) |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
123 |
handle Pattern.MATCH => NONE |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
124 |
in |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
125 |
get_first match (NetRules.retrieve (FundefData.get ctxt) t) |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
126 |
end |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
127 |
|
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
128 |
fun import_last_fundef ctxt = |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
129 |
case NetRules.rules (FundefData.get ctxt) of |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
130 |
[] => NONE |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
131 |
| (t, data) :: _ => |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
132 |
let |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
133 |
val ([t'], ctxt') = Variable.import_terms true [t] (Context.proof_of ctxt) |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
134 |
in |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
135 |
import_fundef_data t' (Context.Proof ctxt') |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
136 |
end |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
137 |
|
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
138 |
val all_fundef_data = NetRules.rules o FundefData.get |
21319
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21255
diff
changeset
|
139 |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
140 |
val map_fundef_congs = FundefCongs.map |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
141 |
val get_fundef_congs = FundefCongs.get |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
142 |
|
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset
|
143 |
|
21319
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21255
diff
changeset
|
144 |
|
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
145 |
structure TerminationRule = GenericDataFun |
21319
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21255
diff
changeset
|
146 |
(struct |
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21255
diff
changeset
|
147 |
val name = "HOL/function_def/termination" |
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
148 |
type T = thm list |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
149 |
val empty = [] |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
150 |
val extend = I |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
151 |
fun merge _ = Drule.merge_rules |
21319
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21255
diff
changeset
|
152 |
fun print _ _ = () |
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21255
diff
changeset
|
153 |
end); |
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21255
diff
changeset
|
154 |
|
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
155 |
val get_termination_rules = TerminationRule.get |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
156 |
val store_termination_rule = TerminationRule.map o cons |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
157 |
val apply_termination_rule = resolve_tac o get_termination_rules o Context.Proof |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
158 |
|
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
159 |
fun add_fundef_data (data as FundefCtxData {fs, termination, ...}) = |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
160 |
FundefData.map (fold (fn f => NetRules.insert (f, data)) fs) |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
161 |
#> store_termination_rule termination |
21319
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21255
diff
changeset
|
162 |
|
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21255
diff
changeset
|
163 |
|
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21255
diff
changeset
|
164 |
|
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset
|
165 |
(* Configuration management *) |
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset
|
166 |
datatype fundef_opt |
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset
|
167 |
= Sequential |
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset
|
168 |
| Default of string |
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset
|
169 |
| Preprocessor of string |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20874
diff
changeset
|
170 |
| Target of xstring |
21319
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21255
diff
changeset
|
171 |
| DomIntros |
22166 | 172 |
| Tailrec |
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset
|
173 |
|
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset
|
174 |
datatype fundef_config |
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset
|
175 |
= FundefConfig of |
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset
|
176 |
{ |
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset
|
177 |
sequential: bool, |
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset
|
178 |
default: string, |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20874
diff
changeset
|
179 |
preprocessor: string option, |
21319
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21255
diff
changeset
|
180 |
target: xstring option, |
22166 | 181 |
domintros: bool, |
182 |
tailrec: bool |
|
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset
|
183 |
} |
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset
|
184 |
|
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset
|
185 |
|
22166 | 186 |
val default_config = FundefConfig { sequential=false, default="%x. arbitrary", preprocessor=NONE, |
187 |
target=NONE, domintros=false, tailrec=false } |
|
188 |
||
189 |
val fun_config = FundefConfig { sequential=true, default="%x. arbitrary", preprocessor=NONE, |
|
190 |
target=NONE, domintros=false, tailrec=false } |
|
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset
|
191 |
|
22166 | 192 |
fun apply_opt Sequential (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) = |
193 |
FundefConfig {sequential=true, default=default, preprocessor=preprocessor, target=target, domintros=domintros, tailrec=tailrec } |
|
194 |
| apply_opt (Default d) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) = |
|
195 |
FundefConfig {sequential=sequential, default=d, preprocessor=preprocessor, target=target, domintros=domintros, tailrec=tailrec } |
|
196 |
| apply_opt (Preprocessor p) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec}) = |
|
197 |
FundefConfig {sequential=sequential, default=default, preprocessor=SOME p, target=target, domintros=domintros, tailrec=tailrec } |
|
198 |
| apply_opt (Target t) (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) = |
|
199 |
FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=SOME t, domintros=domintros, tailrec=tailrec } |
|
200 |
| apply_opt DomIntros (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) = |
|
201 |
FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=true,tailrec=tailrec } |
|
202 |
| apply_opt Tailrec (FundefConfig {sequential, default, preprocessor, target, domintros,tailrec }) = |
|
203 |
FundefConfig {sequential=sequential, default=default, preprocessor=preprocessor, target=target, domintros=domintros,tailrec=true } |
|
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset
|
204 |
|
22498
62cdd4b3e96b
made function syntax strict, requiring | to separate equations; cleanup
krauss
parents:
22279
diff
changeset
|
205 |
fun target_of (FundefConfig {target, ...}) = target |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20874
diff
changeset
|
206 |
|
22498
62cdd4b3e96b
made function syntax strict, requiring | to separate equations; cleanup
krauss
parents:
22279
diff
changeset
|
207 |
local |
62cdd4b3e96b
made function syntax strict, requiring | to separate equations; cleanup
krauss
parents:
22279
diff
changeset
|
208 |
structure P = OuterParse and K = OuterKeyword |
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset
|
209 |
|
22498
62cdd4b3e96b
made function syntax strict, requiring | to separate equations; cleanup
krauss
parents:
22279
diff
changeset
|
210 |
val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false |
62cdd4b3e96b
made function syntax strict, requiring | to separate equations; cleanup
krauss
parents:
22279
diff
changeset
|
211 |
|
62cdd4b3e96b
made function syntax strict, requiring | to separate equations; cleanup
krauss
parents:
22279
diff
changeset
|
212 |
val option_parser = (P.$$$ "sequential" >> K Sequential) |
62cdd4b3e96b
made function syntax strict, requiring | to separate equations; cleanup
krauss
parents:
22279
diff
changeset
|
213 |
|| ((P.reserved "default" |-- P.term) >> Default) |
62cdd4b3e96b
made function syntax strict, requiring | to separate equations; cleanup
krauss
parents:
22279
diff
changeset
|
214 |
|| (P.reserved "domintros" >> K DomIntros) |
62cdd4b3e96b
made function syntax strict, requiring | to separate equations; cleanup
krauss
parents:
22279
diff
changeset
|
215 |
|| (P.reserved "tailrec" >> K Tailrec) |
62cdd4b3e96b
made function syntax strict, requiring | to separate equations; cleanup
krauss
parents:
22279
diff
changeset
|
216 |
|| ((P.$$$ "in" |-- P.xname) >> Target) |
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset
|
217 |
|
22498
62cdd4b3e96b
made function syntax strict, requiring | to separate equations; cleanup
krauss
parents:
22279
diff
changeset
|
218 |
fun config_parser def = (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 (P.group "option" option_parser)) --| P.$$$ ")") []) |
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20874
diff
changeset
|
219 |
>> (fn opts => fold apply_opt opts def) |
22166 | 220 |
|
22498
62cdd4b3e96b
made function syntax strict, requiring | to separate equations; cleanup
krauss
parents:
22279
diff
changeset
|
221 |
fun pipe_list1 s = P.enum1 "|" s |
62cdd4b3e96b
made function syntax strict, requiring | to separate equations; cleanup
krauss
parents:
22279
diff
changeset
|
222 |
|
62cdd4b3e96b
made function syntax strict, requiring | to separate equations; cleanup
krauss
parents:
22279
diff
changeset
|
223 |
val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")" |
62cdd4b3e96b
made function syntax strict, requiring | to separate equations; cleanup
krauss
parents:
22279
diff
changeset
|
224 |
|
62cdd4b3e96b
made function syntax strict, requiring | to separate equations; cleanup
krauss
parents:
22279
diff
changeset
|
225 |
fun pipe_error t = P.!!! (Scan.fail_with (K (cat_lines ["Equations must be separated by " ^ quote "|", quote t]))) |
62cdd4b3e96b
made function syntax strict, requiring | to separate equations; cleanup
krauss
parents:
22279
diff
changeset
|
226 |
|
62cdd4b3e96b
made function syntax strict, requiring | to separate equations; cleanup
krauss
parents:
22279
diff
changeset
|
227 |
val statement_ow = SpecParse.opt_thm_name ":" -- (P.prop -- Scan.optional (otherwise >> K true) false) |
62cdd4b3e96b
made function syntax strict, requiring | to separate equations; cleanup
krauss
parents:
22279
diff
changeset
|
228 |
--| Scan.ahead ((P.term :-- pipe_error) || Scan.succeed ("","")) |
62cdd4b3e96b
made function syntax strict, requiring | to separate equations; cleanup
krauss
parents:
22279
diff
changeset
|
229 |
|
62cdd4b3e96b
made function syntax strict, requiring | to separate equations; cleanup
krauss
parents:
22279
diff
changeset
|
230 |
val statements_ow = pipe_list1 statement_ow |
62cdd4b3e96b
made function syntax strict, requiring | to separate equations; cleanup
krauss
parents:
22279
diff
changeset
|
231 |
in |
62cdd4b3e96b
made function syntax strict, requiring | to separate equations; cleanup
krauss
parents:
22279
diff
changeset
|
232 |
fun fundef_parser default_cfg = config_parser default_cfg -- P.fixes --| P.$$$ "where" -- statements_ow |
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset
|
233 |
end |
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20523
diff
changeset
|
234 |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
235 |
end |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
236 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
237 |
(* Common Abbreviations *) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
238 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
239 |
structure FundefAbbrev = |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
240 |
struct |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
241 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
242 |
fun implies_elim_swp x y = implies_elim y x |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
243 |
|
22498
62cdd4b3e96b
made function syntax strict, requiring | to separate equations; cleanup
krauss
parents:
22279
diff
changeset
|
244 |
(* HOL abbreviations *) |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
245 |
val boolT = HOLogic.boolT |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
246 |
val mk_prod = HOLogic.mk_prod |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
247 |
val mk_eq = HOLogic.mk_eq |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20289
diff
changeset
|
248 |
val eq_const = HOLogic.eq_const |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
249 |
val Trueprop = HOLogic.mk_Trueprop |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
250 |
val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
251 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
252 |
fun free_to_var (Free (v,T)) = Var ((v,0),T) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
253 |
| free_to_var _ = raise Match |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
254 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
255 |
fun var_to_free (Var ((v,_),T)) = Free (v,T) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
256 |
| var_to_free _ = raise Match |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
257 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
258 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
259 |
end |