author | wenzelm |
Mon, 18 Apr 2016 14:30:24 +0200 | |
changeset 63011 | 301e631666a0 |
parent 63006 | 89d19aa73081 |
child 63019 | 80ef19b51493 |
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 |
|
41114 | 4 |
Main entry points to the function package. |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
5 |
*) |
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 |
signature FUNCTION = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
8 |
sig |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
9 |
include FUNCTION_DATA |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
10 |
|
36520 | 11 |
val add_function: (binding * typ option * mixfix) list -> |
12 |
(Attrib.binding * term) list -> Function_Common.function_config -> |
|
36522
e80a95279ef6
return info record (relative to auxiliary context!)
krauss
parents:
36520
diff
changeset
|
13 |
(Proof.context -> tactic) -> local_theory -> info * local_theory |
36520 | 14 |
|
15 |
val add_function_cmd: (binding * string option * mixfix) list -> |
|
16 |
(Attrib.binding * string) list -> Function_Common.function_config -> |
|
44239
47ecd30e018d
less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);
wenzelm
parents:
44192
diff
changeset
|
17 |
(Proof.context -> tactic) -> bool -> local_theory -> info * local_theory |
36520 | 18 |
|
36519
46bf776a81e0
ML interface uses plain command names, following conventions from typedef
krauss
parents:
36518
diff
changeset
|
19 |
val function: (binding * typ option * mixfix) list -> |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
20 |
(Attrib.binding * term) list -> Function_Common.function_config -> |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
21 |
local_theory -> Proof.state |
34230 | 22 |
|
36519
46bf776a81e0
ML interface uses plain command names, following conventions from typedef
krauss
parents:
36518
diff
changeset
|
23 |
val function_cmd: (binding * string option * mixfix) list -> |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
24 |
(Attrib.binding * string) list -> Function_Common.function_config -> |
44239
47ecd30e018d
less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);
wenzelm
parents:
44192
diff
changeset
|
25 |
bool -> local_theory -> Proof.state |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
26 |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
27 |
val prove_termination: term option -> tactic -> local_theory -> |
36547
2a9d0ec8c10d
return updated info record after termination proof
krauss
parents:
36522
diff
changeset
|
28 |
info * local_theory |
2a9d0ec8c10d
return updated info record after termination proof
krauss
parents:
36522
diff
changeset
|
29 |
val prove_termination_cmd: string option -> tactic -> local_theory -> |
2a9d0ec8c10d
return updated info record after termination proof
krauss
parents:
36522
diff
changeset
|
30 |
info * local_theory |
36520 | 31 |
|
36519
46bf776a81e0
ML interface uses plain command names, following conventions from typedef
krauss
parents:
36518
diff
changeset
|
32 |
val termination : term option -> local_theory -> Proof.state |
46bf776a81e0
ML interface uses plain command names, following conventions from typedef
krauss
parents:
36518
diff
changeset
|
33 |
val termination_cmd : string option -> local_theory -> Proof.state |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
34 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
35 |
val get_congs : Proof.context -> thm list |
34230 | 36 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
37 |
val get_info : Proof.context -> term -> info |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
38 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
39 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
40 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
41 |
structure Function : FUNCTION = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
42 |
struct |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
43 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
44 |
open Function_Lib |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
45 |
open Function_Common |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
46 |
|
45592 | 47 |
val simp_attribs = |
48 |
@{attributes [simp, nitpick_simp]} @ [Attrib.internal (K Code.add_default_eqn_attribute)] |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
49 |
|
45592 | 50 |
val psimp_attribs = |
51 |
@{attributes [nitpick_psimp]} |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
52 |
|
53604 | 53 |
fun note_qualified suffix attrs (fname, thms) = |
63005 | 54 |
Local_Theory.note ((derived_name fname suffix, map (Attrib.internal o K) attrs), thms) |
53604 | 55 |
#> apfst snd |
56 |
||
63005 | 57 |
fun add_simps fnames post sort extra_qualify label mod_binding moreatts simps lthy = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
58 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
59 |
val spec = post simps |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
60 |
|> map (apfst (apsnd (fn ats => moreatts @ ats))) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
61 |
|> map (apfst (apfst extra_qualify)) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
62 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
63 |
val (saved_spec_simps, lthy) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
64 |
fold_map Local_Theory.note spec lthy |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
65 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
66 |
val saved_simps = maps snd saved_spec_simps |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
67 |
val simps_by_f = sort saved_simps |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
68 |
|
63004 | 69 |
fun note fname simps = |
63005 | 70 |
Local_Theory.note ((mod_binding (derived_name fname label), []), simps) #> snd |
63004 | 71 |
in (saved_simps, fold2 note fnames simps_by_f lthy) end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
72 |
|
62774
cfcb20bbdbd8
reconcile object-logic constraint vs. mixfix constraint;
wenzelm
parents:
61841
diff
changeset
|
73 |
fun prepare_function do_print prep fixspec eqns config lthy = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
74 |
let |
62996 | 75 |
val ((fixes0, spec0), ctxt') = prep fixspec eqns lthy |
76 |
val fixes = map (apfst (apfst Binding.name_of)) fixes0 |
|
77 |
val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
78 |
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
|
79 |
|
63004 | 80 |
val fnames = map (fst o fst) fixes0 |
63006 | 81 |
val defname = Binding.conglomerate fnames; |
62996 | 82 |
|
41846
b368a7aee46a
removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents:
41417
diff
changeset
|
83 |
val FunctionConfig {partials, default, ...} = config |
41417 | 84 |
val _ = |
44052 | 85 |
if is_some default |
86 |
then legacy_feature "\"function (default)\" -- use 'partial_function' instead" |
|
41417 | 87 |
else () |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
88 |
|
36519
46bf776a81e0
ML interface uses plain command names, following conventions from typedef
krauss
parents:
36518
diff
changeset
|
89 |
val ((goal_state, cont), lthy') = |
63011 | 90 |
Function_Mutual.prepare_function_mutual config defname fixes0 eqs lthy |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
91 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
92 |
fun afterqed [[proof]] lthy = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
93 |
let |
60643 | 94 |
val result = cont lthy (Thm.close_derivation proof) |
52384 | 95 |
val FunctionResult {fs, R, dom, psimps, simple_pinducts, |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
96 |
termination, domintros, cases, ...} = result |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
97 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
98 |
val pelims = Function_Elims.mk_partial_elim_rules lthy result |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
99 |
|
59859 | 100 |
val concealed_partial = if partials then I else Binding.concealed |
33394
9c6980f2eb39
conceal "termination" rule, used only by special tools
krauss
parents:
33369
diff
changeset
|
101 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
102 |
val addsmps = add_simps fnames post sort_cont |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
103 |
|
53604 | 104 |
val (((((psimps', [pinducts']), [termination']), cases'), pelims'), lthy) = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
105 |
lthy |
59859 | 106 |
|> addsmps (concealed_partial o Binding.qualify false "partial") |
107 |
"psimps" concealed_partial psimp_attribs psimps |
|
63005 | 108 |
||>> Local_Theory.notes [((concealed_partial (derived_name defname "pinduct"), []), |
50771
2852f997bfb5
prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
wenzelm
parents:
49967
diff
changeset
|
109 |
simple_pinducts |> map (fn th => ([th], |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
110 |
[Attrib.internal (K (Rule_Cases.case_names cnames)), |
50771
2852f997bfb5
prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
wenzelm
parents:
49967
diff
changeset
|
111 |
Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th))), |
2852f997bfb5
prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
wenzelm
parents:
49967
diff
changeset
|
112 |
Attrib.internal (K (Induct.induct_pred ""))])))] |
63004 | 113 |
||>> (apfst snd o |
63005 | 114 |
Local_Theory.note |
115 |
((Binding.concealed (derived_name defname "termination"), []), [termination])) |
|
63004 | 116 |
||>> fold_map (note_qualified "cases" [Rule_Cases.case_names cnames]) |
117 |
(fnames ~~ map single cases) (* TODO: case names *) |
|
118 |
||>> fold_map (note_qualified "pelims" [Rule_Cases.consumes 1, Rule_Cases.constraints 1]) |
|
119 |
(fnames ~~ pelims) |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
120 |
||> (case domintros of NONE => I | SOME thms => |
63005 | 121 |
Local_Theory.note ((derived_name defname "domintros", []), thms) #> snd) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
122 |
|
63004 | 123 |
val info = |
124 |
{ add_simps=addsmps, fnames=fnames, case_names=cnames, psimps=psimps', |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
125 |
pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination', |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
126 |
fs=fs, R=R, dom=dom, defname=defname, is_partial=true, cases=flat cases', |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
127 |
pelims=pelims',elims=NONE} |
34230 | 128 |
|
56932
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56254
diff
changeset
|
129 |
val _ = |
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56254
diff
changeset
|
130 |
Proof_Display.print_consts do_print (Position.thread_data ()) lthy |
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56254
diff
changeset
|
131 |
(K false) (map fst fixes) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
132 |
in |
44239
47ecd30e018d
less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);
wenzelm
parents:
44192
diff
changeset
|
133 |
(info, |
45291
57cd50f98fdc
uniform Local_Theory.declaration with explicit params;
wenzelm
parents:
45290
diff
changeset
|
134 |
lthy |> Local_Theory.declaration {syntax = false, pervasive = false} |
63004 | 135 |
(fn phi => add_function_data (transform_function_data phi info))) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
136 |
end |
36520 | 137 |
in |
36519
46bf776a81e0
ML interface uses plain command names, following conventions from typedef
krauss
parents:
36518
diff
changeset
|
138 |
((goal_state, afterqed), lthy') |
36518
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
139 |
end |
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
140 |
|
62774
cfcb20bbdbd8
reconcile object-logic constraint vs. mixfix constraint;
wenzelm
parents:
61841
diff
changeset
|
141 |
fun gen_add_function do_print prep fixspec eqns config tac lthy = |
36520 | 142 |
let |
143 |
val ((goal_state, afterqed), lthy') = |
|
62774
cfcb20bbdbd8
reconcile object-logic constraint vs. mixfix constraint;
wenzelm
parents:
61841
diff
changeset
|
144 |
prepare_function do_print prep fixspec eqns config lthy |
36520 | 145 |
val pattern_thm = |
146 |
case SINGLE (tac lthy') goal_state of |
|
147 |
NONE => error "pattern completeness and compatibility proof failed" |
|
148 |
| SOME st => Goal.finish lthy' st |
|
149 |
in |
|
150 |
lthy' |
|
151 |
|> afterqed [[pattern_thm]] |
|
152 |
end |
|
153 |
||
62774
cfcb20bbdbd8
reconcile object-logic constraint vs. mixfix constraint;
wenzelm
parents:
61841
diff
changeset
|
154 |
val add_function = gen_add_function false Specification.check_spec |
cfcb20bbdbd8
reconcile object-logic constraint vs. mixfix constraint;
wenzelm
parents:
61841
diff
changeset
|
155 |
fun add_function_cmd a b c d int = gen_add_function int Specification.read_spec a b c d |
60499 | 156 |
|
62774
cfcb20bbdbd8
reconcile object-logic constraint vs. mixfix constraint;
wenzelm
parents:
61841
diff
changeset
|
157 |
fun gen_function do_print prep fixspec eqns config lthy = |
36518
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
158 |
let |
36520 | 159 |
val ((goal_state, afterqed), lthy') = |
62774
cfcb20bbdbd8
reconcile object-logic constraint vs. mixfix constraint;
wenzelm
parents:
61841
diff
changeset
|
160 |
prepare_function do_print prep fixspec eqns config lthy |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
161 |
in |
36518
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
162 |
lthy' |
59582 | 163 |
|> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (Thm.concl_of goal_state), [])]] |
61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61112
diff
changeset
|
164 |
|> Proof.refine_singleton (Method.primitive_text (K (K goal_state))) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
165 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
166 |
|
62774
cfcb20bbdbd8
reconcile object-logic constraint vs. mixfix constraint;
wenzelm
parents:
61841
diff
changeset
|
167 |
val function = gen_function false Specification.check_spec |
cfcb20bbdbd8
reconcile object-logic constraint vs. mixfix constraint;
wenzelm
parents:
61841
diff
changeset
|
168 |
fun function_cmd a b c int = gen_function int Specification.read_spec a b c |
36520 | 169 |
|
36518
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
170 |
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
|
171 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
172 |
val term_opt = Option.map (prep_term lthy) raw_term_opt |
48995 | 173 |
val info = |
49967
69774b4f5b8a
recovered explicit error message, which was lost in b8570ea1ce25;
wenzelm
parents:
48995
diff
changeset
|
174 |
(case term_opt of |
69774b4f5b8a
recovered explicit error message, which was lost in b8570ea1ce25;
wenzelm
parents:
48995
diff
changeset
|
175 |
SOME t => |
69774b4f5b8a
recovered explicit error message, which was lost in b8570ea1ce25;
wenzelm
parents:
48995
diff
changeset
|
176 |
(case import_function_data t lthy of |
69774b4f5b8a
recovered explicit error message, which was lost in b8570ea1ce25;
wenzelm
parents:
48995
diff
changeset
|
177 |
SOME info => info |
69774b4f5b8a
recovered explicit error message, which was lost in b8570ea1ce25;
wenzelm
parents:
48995
diff
changeset
|
178 |
| NONE => error ("Not a function: " ^ quote (Syntax.string_of_term lthy t))) |
69774b4f5b8a
recovered explicit error message, which was lost in b8570ea1ce25;
wenzelm
parents:
48995
diff
changeset
|
179 |
| NONE => |
69774b4f5b8a
recovered explicit error message, which was lost in b8570ea1ce25;
wenzelm
parents:
48995
diff
changeset
|
180 |
(case import_last_function lthy of |
69774b4f5b8a
recovered explicit error message, which was lost in b8570ea1ce25;
wenzelm
parents:
48995
diff
changeset
|
181 |
SOME info => info |
69774b4f5b8a
recovered explicit error message, which was lost in b8570ea1ce25;
wenzelm
parents:
48995
diff
changeset
|
182 |
| NONE => error "Not a function")) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
183 |
|
48995 | 184 |
val { termination, fs, R, add_simps, case_names, psimps, |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
185 |
pinducts, defname, fnames, cases, dom, pelims, ...} = info |
48995 | 186 |
val domT = domain_type (fastype_of R) |
187 |
val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT))) |
|
188 |
fun afterqed [[totality]] lthy = |
|
189 |
let |
|
190 |
val totality = Thm.close_derivation totality |
|
191 |
val remove_domain_condition = |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50771
diff
changeset
|
192 |
full_simplify (put_simpset HOL_basic_ss lthy |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50771
diff
changeset
|
193 |
addsimps [totality, @{thm True_implies_equals}]) |
48995 | 194 |
val tsimps = map remove_domain_condition psimps |
195 |
val tinduct = map remove_domain_condition pinducts |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
196 |
val telims = map (map remove_domain_condition) pelims |
48995 | 197 |
in |
198 |
lthy |
|
199 |
|> add_simps I "simps" I simp_attribs tsimps |
|
200 |
||>> Local_Theory.note |
|
63005 | 201 |
((derived_name defname "induct", [Attrib.internal (K (Rule_Cases.case_names case_names))]), |
48995 | 202 |
tinduct) |
63004 | 203 |
||>> fold_map (note_qualified "elims" [Rule_Cases.consumes 1, Rule_Cases.constraints 1]) |
204 |
(fnames ~~ telims) |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
205 |
|-> (fn ((simps,(_,inducts)), elims) => fn lthy => |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
206 |
let val info' = { is_partial=false, defname=defname, fnames=fnames, add_simps=add_simps, |
52384 | 207 |
case_names=case_names, fs=fs, R=R, dom=dom, psimps=psimps, pinducts=pinducts, |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
208 |
simps=SOME simps, inducts=SOME inducts, termination=termination, cases=cases, pelims=pelims, elims=SOME elims} |
48995 | 209 |
in |
210 |
(info', |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
211 |
lthy |
48995 | 212 |
|> Local_Theory.declaration {syntax = false, pervasive = false} |
63004 | 213 |
(fn phi => add_function_data (transform_function_data phi info')) |
48995 | 214 |
|> Spec_Rules.add Spec_Rules.Equational (fs, tsimps)) |
215 |
end) |
|
216 |
end |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
217 |
in |
36518
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
218 |
(goal, afterqed, termination) |
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
219 |
end |
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
220 |
|
36520 | 221 |
fun gen_prove_termination prep_term raw_term_opt tac lthy = |
222 |
let |
|
223 |
val (goal, afterqed, termination) = |
|
224 |
prepare_termination_proof prep_term raw_term_opt lthy |
|
225 |
||
226 |
val totality = Goal.prove lthy [] [] goal (K tac) |
|
227 |
in |
|
228 |
afterqed [[totality]] lthy |
|
229 |
end |
|
230 |
||
231 |
val prove_termination = gen_prove_termination Syntax.check_term |
|
232 |
val prove_termination_cmd = gen_prove_termination Syntax.read_term |
|
233 |
||
36519
46bf776a81e0
ML interface uses plain command names, following conventions from typedef
krauss
parents:
36518
diff
changeset
|
234 |
fun gen_termination prep_term raw_term_opt lthy = |
36518
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
235 |
let |
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
236 |
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
|
237 |
in |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
238 |
lthy |
42361 | 239 |
|> Proof_Context.note_thmss "" |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
240 |
[((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd |
42361 | 241 |
|> Proof_Context.note_thmss "" |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
242 |
[((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd |
42361 | 243 |
|> Proof_Context.note_thmss "" |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
244 |
[((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]), |
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
53614
diff
changeset
|
245 |
[([Goal.norm_result lthy termination], [])])] |> snd |
36547
2a9d0ec8c10d
return updated info record after termination proof
krauss
parents:
36522
diff
changeset
|
246 |
|> Proof.theorem NONE (snd oo afterqed) [[(goal, [])]] |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
247 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
248 |
|
36519
46bf776a81e0
ML interface uses plain command names, following conventions from typedef
krauss
parents:
36518
diff
changeset
|
249 |
val termination = gen_termination Syntax.check_term |
46bf776a81e0
ML interface uses plain command names, following conventions from typedef
krauss
parents:
36518
diff
changeset
|
250 |
val termination_cmd = gen_termination Syntax.read_term |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
251 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
252 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
253 |
(* Datatype hook to declare datatype congs as "function_congs" *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
254 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
255 |
fun add_case_cong n thy = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
256 |
let |
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57959
diff
changeset
|
257 |
val cong = #case_cong (Old_Datatype_Data.the_info thy n) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
258 |
|> safe_mk_meta_eq |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
259 |
in |
61112 | 260 |
Context.theory_map (Function_Context_Tree.add_function_cong cong) thy |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
261 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
262 |
|
58826 | 263 |
val _ = Theory.setup (Old_Datatype_Data.interpretation (K (fold add_case_cong))) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
264 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
265 |
|
58826 | 266 |
(* get info *) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
267 |
|
58816 | 268 |
val get_congs = Function_Context_Tree.get_function_congs |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
269 |
|
59159 | 270 |
fun get_info ctxt t = Item_Net.retrieve (get_functions ctxt) t |
34230 | 271 |
|> the_single |> snd |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
272 |
|
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36547
diff
changeset
|
273 |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
274 |
(* outer syntax *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
275 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
276 |
val _ = |
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59859
diff
changeset
|
277 |
Outer_Syntax.local_theory_to_proof' @{command_keyword function} |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
45592
diff
changeset
|
278 |
"define general recursive functions" |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
45592
diff
changeset
|
279 |
(function_parser default_config |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
45592
diff
changeset
|
280 |
>> (fn ((config, fixes), statements) => function_cmd fixes statements config)) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
281 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
282 |
val _ = |
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59859
diff
changeset
|
283 |
Outer_Syntax.local_theory_to_proof @{command_keyword termination} |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
45592
diff
changeset
|
284 |
"prove termination of a recursive function" |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
45592
diff
changeset
|
285 |
(Scan.option Parse.term >> termination_cmd) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
286 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
287 |
end |