author | haftmann |
Thu, 08 Jul 2010 16:19:24 +0200 | |
changeset 37744 | 3daaf23b9ab4 |
parent 37145 | 01aa36932739 |
child 39754 | 150f831ce4a3 |
permissions | -rw-r--r-- |
37744 | 1 |
(* Title: HOL/Tools/Function/function.ML |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
2 |
Author: Alexander Krauss, TU Muenchen |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
3 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
4 |
A package for general recursive function definitions. |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
5 |
Isar commands. |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
6 |
*) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
7 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
8 |
signature FUNCTION = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
9 |
sig |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
10 |
include FUNCTION_DATA |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
11 |
|
36520 | 12 |
val add_function: (binding * typ option * mixfix) list -> |
13 |
(Attrib.binding * term) list -> Function_Common.function_config -> |
|
36522
e80a95279ef6
return info record (relative to auxiliary context!)
krauss
parents:
36520
diff
changeset
|
14 |
(Proof.context -> tactic) -> local_theory -> info * local_theory |
36520 | 15 |
|
16 |
val add_function_cmd: (binding * string option * mixfix) list -> |
|
17 |
(Attrib.binding * string) list -> Function_Common.function_config -> |
|
36522
e80a95279ef6
return info record (relative to auxiliary context!)
krauss
parents:
36520
diff
changeset
|
18 |
(Proof.context -> tactic) -> local_theory -> info * local_theory |
36520 | 19 |
|
36519
46bf776a81e0
ML interface uses plain command names, following conventions from typedef
krauss
parents:
36518
diff
changeset
|
20 |
val function: (binding * typ option * mixfix) list -> |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
21 |
(Attrib.binding * term) list -> Function_Common.function_config -> |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
22 |
local_theory -> Proof.state |
34230 | 23 |
|
36519
46bf776a81e0
ML interface uses plain command names, following conventions from typedef
krauss
parents:
36518
diff
changeset
|
24 |
val function_cmd: (binding * string option * mixfix) list -> |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
25 |
(Attrib.binding * string) list -> Function_Common.function_config -> |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
26 |
local_theory -> Proof.state |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
27 |
|
36547
2a9d0ec8c10d
return updated info record after termination proof
krauss
parents:
36522
diff
changeset
|
28 |
val prove_termination: term option -> tactic -> local_theory -> |
2a9d0ec8c10d
return updated info record after termination proof
krauss
parents:
36522
diff
changeset
|
29 |
info * local_theory |
2a9d0ec8c10d
return updated info record after termination proof
krauss
parents:
36522
diff
changeset
|
30 |
val prove_termination_cmd: string option -> tactic -> local_theory -> |
2a9d0ec8c10d
return updated info record after termination proof
krauss
parents:
36522
diff
changeset
|
31 |
info * local_theory |
36520 | 32 |
|
36519
46bf776a81e0
ML interface uses plain command names, following conventions from typedef
krauss
parents:
36518
diff
changeset
|
33 |
val termination : term option -> local_theory -> Proof.state |
46bf776a81e0
ML interface uses plain command names, following conventions from typedef
krauss
parents:
36518
diff
changeset
|
34 |
val termination_cmd : string option -> local_theory -> Proof.state |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
35 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
36 |
val setup : theory -> theory |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
37 |
val get_congs : Proof.context -> thm list |
34230 | 38 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
39 |
val get_info : Proof.context -> term -> info |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
40 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
41 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
42 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
43 |
structure Function : FUNCTION = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
44 |
struct |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
45 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
46 |
open Function_Lib |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
47 |
open Function_Common |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
48 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
49 |
val simp_attribs = map (Attrib.internal o K) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
50 |
[Simplifier.simp_add, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
51 |
Code.add_default_eqn_attribute, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
52 |
Nitpick_Simps.add] |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
53 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
54 |
val psimp_attribs = map (Attrib.internal o K) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
55 |
[Simplifier.simp_add, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
56 |
Nitpick_Psimps.add] |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
57 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
58 |
fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
59 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
60 |
fun add_simps fnames post sort extra_qualify label mod_binding moreatts |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
61 |
simps lthy = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
62 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
63 |
val spec = post simps |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
64 |
|> map (apfst (apsnd (fn ats => moreatts @ ats))) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
65 |
|> map (apfst (apfst extra_qualify)) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
66 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
67 |
val (saved_spec_simps, lthy) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
68 |
fold_map Local_Theory.note spec lthy |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
69 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
70 |
val saved_simps = maps snd saved_spec_simps |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
71 |
val simps_by_f = sort saved_simps |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
72 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
73 |
fun add_for_f fname simps = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
74 |
Local_Theory.note |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
75 |
((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
76 |
#> snd |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
77 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
78 |
(saved_simps, fold2 add_for_f fnames simps_by_f lthy) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
79 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
80 |
|
36518
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
81 |
fun prepare_function is_external prep default_constraint fixspec eqns config lthy = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
82 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
83 |
val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx)) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
84 |
val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
85 |
val fixes = map (apfst (apfst Binding.name_of)) fixes0; |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
86 |
val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0; |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
87 |
val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
88 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
89 |
val defname = mk_defname fixes |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
90 |
val FunctionConfig {partials, ...} = config |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
91 |
|
36519
46bf776a81e0
ML interface uses plain command names, following conventions from typedef
krauss
parents:
36518
diff
changeset
|
92 |
val ((goal_state, cont), lthy') = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
93 |
Function_Mutual.prepare_function_mutual config defname fixes eqs lthy |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
94 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
95 |
fun afterqed [[proof]] lthy = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
96 |
let |
35756
cfde251d03a5
refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function
bulwahn
parents:
35410
diff
changeset
|
97 |
val FunctionResult {fs, R, psimps, trsimps, simple_pinducts, |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
98 |
termination, domintros, cases, ...} = |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
99 |
cont (Thm.close_derivation proof) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
100 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
101 |
val fnames = map (fst o fst) fixes |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
102 |
fun qualify n = Binding.name n |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
103 |
|> Binding.qualify true defname |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
104 |
val conceal_partial = if partials then I else Binding.conceal |
33394
9c6980f2eb39
conceal "termination" rule, used only by special tools
krauss
parents:
33369
diff
changeset
|
105 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
106 |
val addsmps = add_simps fnames post sort_cont |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
107 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
108 |
val (((psimps', pinducts'), (_, [termination'])), lthy) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
109 |
lthy |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
110 |
|> addsmps (conceal_partial o Binding.qualify false "partial") |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
111 |
"psimps" conceal_partial psimp_attribs psimps |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
112 |
||> fold_option (snd oo addsmps I "simps" I simp_attribs) trsimps |
35756
cfde251d03a5
refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function
bulwahn
parents:
35410
diff
changeset
|
113 |
||> fold_option (Spec_Rules.add Spec_Rules.Equational o pair fs) trsimps |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
114 |
||>> Local_Theory.note ((conceal_partial (qualify "pinduct"), |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
115 |
[Attrib.internal (K (Rule_Cases.case_names cnames)), |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
116 |
Attrib.internal (K (Rule_Cases.consumes 1)), |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
117 |
Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
118 |
||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination]) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
119 |
||> (snd o Local_Theory.note ((qualify "cases", |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
120 |
[Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases])) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
121 |
||> fold_option (snd oo curry Local_Theory.note (qualify "domintros", [])) domintros |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
122 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
123 |
val info = { add_simps=addsmps, case_names=cnames, psimps=psimps', |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
124 |
pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination', |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
125 |
fs=fs, R=R, defname=defname, is_partial=true } |
34230 | 126 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
127 |
val _ = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
128 |
if not is_external then () |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
129 |
else Specification.print_consts lthy (K false) (map fst fixes) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
130 |
in |
36522
e80a95279ef6
return info record (relative to auxiliary context!)
krauss
parents:
36520
diff
changeset
|
131 |
(info, |
e80a95279ef6
return info record (relative to auxiliary context!)
krauss
parents:
36520
diff
changeset
|
132 |
lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info)) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
133 |
end |
36520 | 134 |
in |
36519
46bf776a81e0
ML interface uses plain command names, following conventions from typedef
krauss
parents:
36518
diff
changeset
|
135 |
((goal_state, afterqed), lthy') |
36518
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
136 |
end |
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
137 |
|
36520 | 138 |
fun gen_add_function is_external prep default_constraint fixspec eqns config tac lthy = |
139 |
let |
|
140 |
val ((goal_state, afterqed), lthy') = |
|
141 |
prepare_function is_external prep default_constraint fixspec eqns config lthy |
|
142 |
val pattern_thm = |
|
143 |
case SINGLE (tac lthy') goal_state of |
|
144 |
NONE => error "pattern completeness and compatibility proof failed" |
|
145 |
| SOME st => Goal.finish lthy' st |
|
146 |
in |
|
147 |
lthy' |
|
148 |
|> afterqed [[pattern_thm]] |
|
149 |
end |
|
150 |
||
151 |
val add_function = |
|
37145
01aa36932739
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
wenzelm
parents:
36960
diff
changeset
|
152 |
gen_add_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS) |
36520 | 153 |
val add_function_cmd = gen_add_function true Specification.read_spec "_::type" |
154 |
||
36519
46bf776a81e0
ML interface uses plain command names, following conventions from typedef
krauss
parents:
36518
diff
changeset
|
155 |
fun gen_function is_external prep default_constraint fixspec eqns config lthy = |
36518
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
156 |
let |
36520 | 157 |
val ((goal_state, afterqed), lthy') = |
36518
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
158 |
prepare_function is_external prep default_constraint fixspec eqns config lthy |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
159 |
in |
36518
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
160 |
lthy' |
36522
e80a95279ef6
return info record (relative to auxiliary context!)
krauss
parents:
36520
diff
changeset
|
161 |
|> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]] |
36519
46bf776a81e0
ML interface uses plain command names, following conventions from typedef
krauss
parents:
36518
diff
changeset
|
162 |
|> Proof.refine (Method.primitive_text (K goal_state)) |> Seq.hd |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
163 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
164 |
|
36519
46bf776a81e0
ML interface uses plain command names, following conventions from typedef
krauss
parents:
36518
diff
changeset
|
165 |
val function = |
37145
01aa36932739
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
wenzelm
parents:
36960
diff
changeset
|
166 |
gen_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS) |
36519
46bf776a81e0
ML interface uses plain command names, following conventions from typedef
krauss
parents:
36518
diff
changeset
|
167 |
val function_cmd = gen_function true Specification.read_spec "_::type" |
36520 | 168 |
|
36518
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
169 |
fun prepare_termination_proof prep_term raw_term_opt lthy = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
170 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
171 |
val term_opt = Option.map (prep_term lthy) raw_term_opt |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
172 |
val info = the (case term_opt of |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
173 |
SOME t => (import_function_data t lthy |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
174 |
handle Option.Option => |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
175 |
error ("Not a function: " ^ quote (Syntax.string_of_term lthy t))) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
176 |
| NONE => (import_last_function lthy handle Option.Option => error "Not a function")) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
177 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
178 |
val { termination, fs, R, add_simps, case_names, psimps, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
179 |
pinducts, defname, ...} = info |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
180 |
val domT = domain_type (fastype_of R) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
181 |
val goal = HOLogic.mk_Trueprop |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
182 |
(HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT))) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
183 |
fun afterqed [[totality]] lthy = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
184 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
185 |
val totality = Thm.close_derivation totality |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
186 |
val remove_domain_condition = |
35410 | 187 |
full_simplify (HOL_basic_ss addsimps [totality, @{thm True_implies_equals}]) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
188 |
val tsimps = map remove_domain_condition psimps |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
189 |
val tinduct = map remove_domain_condition pinducts |
34230 | 190 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
191 |
fun qualify n = Binding.name n |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
192 |
|> Binding.qualify true defname |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
193 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
194 |
lthy |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
195 |
|> add_simps I "simps" I simp_attribs tsimps |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
196 |
||>> Local_Theory.note |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
197 |
((qualify "induct", |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
198 |
[Attrib.internal (K (Rule_Cases.case_names case_names))]), |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
199 |
tinduct) |
36547
2a9d0ec8c10d
return updated info record after termination proof
krauss
parents:
36522
diff
changeset
|
200 |
|-> (fn (simps, (_, inducts)) => fn lthy => |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
201 |
let val info' = { is_partial=false, defname=defname, add_simps=add_simps, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
202 |
case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
203 |
simps=SOME simps, inducts=SOME inducts, termination=termination } |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
204 |
in |
36547
2a9d0ec8c10d
return updated info record after termination proof
krauss
parents:
36522
diff
changeset
|
205 |
(info', |
2a9d0ec8c10d
return updated info record after termination proof
krauss
parents:
36522
diff
changeset
|
206 |
lthy |
2a9d0ec8c10d
return updated info record after termination proof
krauss
parents:
36522
diff
changeset
|
207 |
|> Local_Theory.declaration false (add_function_data o morph_function_data info') |
2a9d0ec8c10d
return updated info record after termination proof
krauss
parents:
36522
diff
changeset
|
208 |
|> Spec_Rules.add Spec_Rules.Equational (fs, tsimps)) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
209 |
end) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
210 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
211 |
in |
36518
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
212 |
(goal, afterqed, termination) |
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
213 |
end |
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
214 |
|
36520 | 215 |
fun gen_prove_termination prep_term raw_term_opt tac lthy = |
216 |
let |
|
217 |
val (goal, afterqed, termination) = |
|
218 |
prepare_termination_proof prep_term raw_term_opt lthy |
|
219 |
||
220 |
val totality = Goal.prove lthy [] [] goal (K tac) |
|
221 |
in |
|
222 |
afterqed [[totality]] lthy |
|
223 |
end |
|
224 |
||
225 |
val prove_termination = gen_prove_termination Syntax.check_term |
|
226 |
val prove_termination_cmd = gen_prove_termination Syntax.read_term |
|
227 |
||
36519
46bf776a81e0
ML interface uses plain command names, following conventions from typedef
krauss
parents:
36518
diff
changeset
|
228 |
fun gen_termination prep_term raw_term_opt lthy = |
36518
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
229 |
let |
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
230 |
val (goal, afterqed, termination) = prepare_termination_proof prep_term raw_term_opt lthy |
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
231 |
in |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
232 |
lthy |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
233 |
|> ProofContext.note_thmss "" |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
234 |
[((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
235 |
|> ProofContext.note_thmss "" |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
236 |
[((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
237 |
|> ProofContext.note_thmss "" |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
238 |
[((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]), |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
239 |
[([Goal.norm_result termination], [])])] |> snd |
36547
2a9d0ec8c10d
return updated info record after termination proof
krauss
parents:
36522
diff
changeset
|
240 |
|> Proof.theorem NONE (snd oo afterqed) [[(goal, [])]] |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
241 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
242 |
|
36519
46bf776a81e0
ML interface uses plain command names, following conventions from typedef
krauss
parents:
36518
diff
changeset
|
243 |
val termination = gen_termination Syntax.check_term |
46bf776a81e0
ML interface uses plain command names, following conventions from typedef
krauss
parents:
36518
diff
changeset
|
244 |
val termination_cmd = gen_termination Syntax.read_term |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
245 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
246 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
247 |
(* Datatype hook to declare datatype congs as "function_congs" *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
248 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
249 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
250 |
fun add_case_cong n thy = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
251 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
252 |
val cong = #case_cong (Datatype.the_info thy n) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
253 |
|> safe_mk_meta_eq |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
254 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
255 |
Context.theory_map |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
256 |
(Function_Ctx_Tree.map_function_congs (Thm.add_thm cong)) thy |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
257 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
258 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
259 |
val setup_case_cong = Datatype.interpretation (K (fold add_case_cong)) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
260 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
261 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
262 |
(* setup *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
263 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
264 |
val setup = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
265 |
Attrib.setup @{binding fundef_cong} |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
266 |
(Attrib.add_del Function_Ctx_Tree.cong_add Function_Ctx_Tree.cong_del) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
267 |
"declaration of congruence rule for function definitions" |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
268 |
#> setup_case_cong |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
269 |
#> Function_Relation.setup |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
270 |
#> Function_Common.Termination_Simps.setup |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
271 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
272 |
val get_congs = Function_Ctx_Tree.get_function_congs |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
273 |
|
34230 | 274 |
fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t |
275 |
|> the_single |> snd |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
276 |
|
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36547
diff
changeset
|
277 |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
278 |
(* outer syntax *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
279 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
280 |
val _ = |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36547
diff
changeset
|
281 |
Outer_Syntax.local_theory_to_proof "function" "define general recursive functions" |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36547
diff
changeset
|
282 |
Keyword.thy_goal |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
283 |
(function_parser default_config |
36519
46bf776a81e0
ML interface uses plain command names, following conventions from typedef
krauss
parents:
36518
diff
changeset
|
284 |
>> (fn ((config, fixes), statements) => function_cmd fixes statements config)) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
285 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
286 |
val _ = |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36547
diff
changeset
|
287 |
Outer_Syntax.local_theory_to_proof "termination" "prove termination of a recursive function" |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36547
diff
changeset
|
288 |
Keyword.thy_goal |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36547
diff
changeset
|
289 |
(Scan.option Parse.term >> termination_cmd) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
290 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
291 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
292 |
end |