author | blanchet |
Mon, 20 Jan 2014 21:32:41 +0100 | |
changeset 55085 | 0e8e4dc55866 |
parent 54883 | dd04a8b654fc |
child 55404 | 5cb95b79a51f |
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 setup : theory -> theory |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
36 |
val get_congs : Proof.context -> thm list |
34230 | 37 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
38 |
val get_info : Proof.context -> term -> info |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
39 |
end |
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 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
42 |
structure Function : FUNCTION = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
43 |
struct |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
44 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
45 |
open Function_Lib |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
46 |
open Function_Common |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
47 |
|
45592 | 48 |
val simp_attribs = |
49 |
@{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
|
50 |
|
45592 | 51 |
val psimp_attribs = |
52 |
@{attributes [nitpick_psimp]} |
|
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 |
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
|
55 |
|
53604 | 56 |
fun note_qualified suffix attrs (fname, thms) = |
57 |
Local_Theory.note ((Binding.qualify true fname (Binding.name suffix), |
|
58 |
map (Attrib.internal o K) attrs), thms) |
|
59 |
#> apfst snd |
|
60 |
||
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
61 |
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
|
62 |
simps lthy = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
63 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
64 |
val spec = post simps |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
65 |
|> map (apfst (apsnd (fn ats => moreatts @ ats))) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
66 |
|> map (apfst (apfst extra_qualify)) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
67 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
68 |
val (saved_spec_simps, lthy) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
69 |
fold_map Local_Theory.note spec lthy |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
70 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
71 |
val saved_simps = maps snd saved_spec_simps |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
72 |
val simps_by_f = sort saved_simps |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
73 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
74 |
fun add_for_f fname simps = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
75 |
Local_Theory.note |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
76 |
((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
|
77 |
#> snd |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
78 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
79 |
(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
|
80 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
81 |
|
44239
47ecd30e018d
less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);
wenzelm
parents:
44192
diff
changeset
|
82 |
fun prepare_function do_print prep default_constraint fixspec eqns config lthy = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
83 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
84 |
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
|
85 |
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
|
86 |
val fixes = map (apfst (apfst Binding.name_of)) fixes0; |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
87 |
val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0; |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
88 |
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
|
89 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
90 |
val defname = mk_defname fixes |
41846
b368a7aee46a
removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents:
41417
diff
changeset
|
91 |
val FunctionConfig {partials, default, ...} = config |
41417 | 92 |
val _ = |
44052 | 93 |
if is_some default |
94 |
then legacy_feature "\"function (default)\" -- use 'partial_function' instead" |
|
41417 | 95 |
else () |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
96 |
|
36519
46bf776a81e0
ML interface uses plain command names, following conventions from typedef
krauss
parents:
36518
diff
changeset
|
97 |
val ((goal_state, cont), lthy') = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
98 |
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
|
99 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
100 |
fun afterqed [[proof]] lthy = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
101 |
let |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
102 |
val result = cont (Thm.close_derivation proof) |
52384 | 103 |
val FunctionResult {fs, R, dom, psimps, simple_pinducts, |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
104 |
termination, domintros, cases, ...} = result |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
105 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
106 |
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
|
107 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
108 |
val fnames = map (fst o fst) fixes |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
109 |
fun qualify n = Binding.name n |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
110 |
|> Binding.qualify true defname |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
111 |
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
|
112 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
113 |
val addsmps = add_simps fnames post sort_cont |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
114 |
|
53604 | 115 |
val (((((psimps', [pinducts']), [termination']), cases'), pelims'), lthy) = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
116 |
lthy |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
117 |
|> addsmps (conceal_partial o Binding.qualify false "partial") |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
118 |
"psimps" conceal_partial psimp_attribs psimps |
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
|
119 |
||>> Local_Theory.notes [((conceal_partial (qualify "pinduct"), []), |
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
|
120 |
simple_pinducts |> map (fn th => ([th], |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
121 |
[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
|
122 |
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
|
123 |
Attrib.internal (K (Induct.induct_pred ""))])))] |
52383 | 124 |
||>> (apfst snd o Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination])) |
53604 | 125 |
||>> fold_map (note_qualified "cases" [Rule_Cases.case_names cnames]) (fnames ~~ map single cases) (* TODO: case names *) |
126 |
||>> fold_map (note_qualified "pelims" [Rule_Cases.consumes 1, Rule_Cases.constraints 1]) (fnames ~~ pelims) |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
127 |
||> (case domintros of NONE => I | SOME thms => |
40076 | 128 |
Local_Theory.note ((qualify "domintros", []), thms) #> snd) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
129 |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
130 |
val info = { 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
|
131 |
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
|
132 |
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
|
133 |
pelims=pelims',elims=NONE} |
34230 | 134 |
|
44239
47ecd30e018d
less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);
wenzelm
parents:
44192
diff
changeset
|
135 |
val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
136 |
in |
44239
47ecd30e018d
less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);
wenzelm
parents:
44192
diff
changeset
|
137 |
(info, |
45291
57cd50f98fdc
uniform Local_Theory.declaration with explicit params;
wenzelm
parents:
45290
diff
changeset
|
138 |
lthy |> Local_Theory.declaration {syntax = false, pervasive = false} |
57cd50f98fdc
uniform Local_Theory.declaration with explicit params;
wenzelm
parents:
45290
diff
changeset
|
139 |
(add_function_data o transform_function_data info)) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
140 |
end |
36520 | 141 |
in |
36519
46bf776a81e0
ML interface uses plain command names, following conventions from typedef
krauss
parents:
36518
diff
changeset
|
142 |
((goal_state, afterqed), lthy') |
36518
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
143 |
end |
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
144 |
|
44239
47ecd30e018d
less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);
wenzelm
parents:
44192
diff
changeset
|
145 |
fun gen_add_function do_print prep default_constraint fixspec eqns config tac lthy = |
36520 | 146 |
let |
147 |
val ((goal_state, afterqed), lthy') = |
|
44239
47ecd30e018d
less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);
wenzelm
parents:
44192
diff
changeset
|
148 |
prepare_function do_print prep default_constraint fixspec eqns config lthy |
36520 | 149 |
val pattern_thm = |
150 |
case SINGLE (tac lthy') goal_state of |
|
151 |
NONE => error "pattern completeness and compatibility proof failed" |
|
152 |
| SOME st => Goal.finish lthy' st |
|
153 |
in |
|
154 |
lthy' |
|
155 |
|> afterqed [[pattern_thm]] |
|
156 |
end |
|
157 |
||
158 |
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
|
159 |
gen_add_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS) |
44239
47ecd30e018d
less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);
wenzelm
parents:
44192
diff
changeset
|
160 |
fun add_function_cmd a b c d int = gen_add_function int Specification.read_spec "_::type" a b c d |
36520 | 161 |
|
44239
47ecd30e018d
less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);
wenzelm
parents:
44192
diff
changeset
|
162 |
fun gen_function do_print prep default_constraint fixspec eqns config lthy = |
36518
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
163 |
let |
36520 | 164 |
val ((goal_state, afterqed), lthy') = |
44239
47ecd30e018d
less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);
wenzelm
parents:
44192
diff
changeset
|
165 |
prepare_function do_print prep default_constraint fixspec eqns config lthy |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
166 |
in |
36518
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
167 |
lthy' |
36522
e80a95279ef6
return info record (relative to auxiliary context!)
krauss
parents:
36520
diff
changeset
|
168 |
|> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]] |
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
53614
diff
changeset
|
169 |
|> Proof.refine (Method.primitive_text (K (K goal_state))) |> Seq.hd |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
170 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
171 |
|
36519
46bf776a81e0
ML interface uses plain command names, following conventions from typedef
krauss
parents:
36518
diff
changeset
|
172 |
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
|
173 |
gen_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS) |
44239
47ecd30e018d
less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);
wenzelm
parents:
44192
diff
changeset
|
174 |
fun function_cmd a b c int = gen_function int Specification.read_spec "_::type" a b c |
36520 | 175 |
|
36518
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
176 |
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
|
177 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
178 |
val term_opt = Option.map (prep_term lthy) raw_term_opt |
48995 | 179 |
val info = |
49967
69774b4f5b8a
recovered explicit error message, which was lost in b8570ea1ce25;
wenzelm
parents:
48995
diff
changeset
|
180 |
(case term_opt of |
69774b4f5b8a
recovered explicit error message, which was lost in b8570ea1ce25;
wenzelm
parents:
48995
diff
changeset
|
181 |
SOME t => |
69774b4f5b8a
recovered explicit error message, which was lost in b8570ea1ce25;
wenzelm
parents:
48995
diff
changeset
|
182 |
(case import_function_data t lthy of |
69774b4f5b8a
recovered explicit error message, which was lost in b8570ea1ce25;
wenzelm
parents:
48995
diff
changeset
|
183 |
SOME info => info |
69774b4f5b8a
recovered explicit error message, which was lost in b8570ea1ce25;
wenzelm
parents:
48995
diff
changeset
|
184 |
| 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
|
185 |
| NONE => |
69774b4f5b8a
recovered explicit error message, which was lost in b8570ea1ce25;
wenzelm
parents:
48995
diff
changeset
|
186 |
(case import_last_function lthy of |
69774b4f5b8a
recovered explicit error message, which was lost in b8570ea1ce25;
wenzelm
parents:
48995
diff
changeset
|
187 |
SOME info => info |
69774b4f5b8a
recovered explicit error message, which was lost in b8570ea1ce25;
wenzelm
parents:
48995
diff
changeset
|
188 |
| NONE => error "Not a function")) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
189 |
|
48995 | 190 |
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
|
191 |
pinducts, defname, fnames, cases, dom, pelims, ...} = info |
48995 | 192 |
val domT = domain_type (fastype_of R) |
193 |
val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT))) |
|
194 |
fun afterqed [[totality]] lthy = |
|
195 |
let |
|
196 |
val totality = Thm.close_derivation totality |
|
197 |
val remove_domain_condition = |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50771
diff
changeset
|
198 |
full_simplify (put_simpset HOL_basic_ss lthy |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
50771
diff
changeset
|
199 |
addsimps [totality, @{thm True_implies_equals}]) |
48995 | 200 |
val tsimps = map remove_domain_condition psimps |
201 |
val tinduct = map remove_domain_condition pinducts |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
202 |
val telims = map (map remove_domain_condition) pelims |
34230 | 203 |
|
48995 | 204 |
fun qualify n = Binding.name n |
205 |
|> Binding.qualify true defname |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
206 |
|
48995 | 207 |
in |
208 |
lthy |
|
209 |
|> add_simps I "simps" I simp_attribs tsimps |
|
210 |
||>> Local_Theory.note |
|
211 |
((qualify "induct", |
|
212 |
[Attrib.internal (K (Rule_Cases.case_names case_names))]), |
|
213 |
tinduct) |
|
53614
8c51fc24d83c
omit automatic Induct.cases_pred declaration, which breaks many existing proofs
krauss
parents:
53604
diff
changeset
|
214 |
||>> fold_map (note_qualified "elims" [Rule_Cases.consumes 1, Rule_Cases.constraints 1]) (fnames ~~ telims) |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
215 |
|-> (fn ((simps,(_,inducts)), elims) => fn lthy => |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
216 |
let val info' = { is_partial=false, defname=defname, fnames=fnames, add_simps=add_simps, |
52384 | 217 |
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
|
218 |
simps=SOME simps, inducts=SOME inducts, termination=termination, cases=cases, pelims=pelims, elims=SOME elims} |
48995 | 219 |
in |
220 |
(info', |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
221 |
lthy |
48995 | 222 |
|> Local_Theory.declaration {syntax = false, pervasive = false} |
223 |
(add_function_data o transform_function_data info') |
|
224 |
|> Spec_Rules.add Spec_Rules.Equational (fs, tsimps)) |
|
225 |
end) |
|
226 |
end |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
227 |
in |
36518
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
228 |
(goal, afterqed, termination) |
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
229 |
end |
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
230 |
|
36520 | 231 |
fun gen_prove_termination prep_term raw_term_opt tac lthy = |
232 |
let |
|
233 |
val (goal, afterqed, termination) = |
|
234 |
prepare_termination_proof prep_term raw_term_opt lthy |
|
235 |
||
236 |
val totality = Goal.prove lthy [] [] goal (K tac) |
|
237 |
in |
|
238 |
afterqed [[totality]] lthy |
|
239 |
end |
|
240 |
||
241 |
val prove_termination = gen_prove_termination Syntax.check_term |
|
242 |
val prove_termination_cmd = gen_prove_termination Syntax.read_term |
|
243 |
||
36519
46bf776a81e0
ML interface uses plain command names, following conventions from typedef
krauss
parents:
36518
diff
changeset
|
244 |
fun gen_termination prep_term raw_term_opt lthy = |
36518
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
245 |
let |
a33b986f2e22
function: better separate Isar integration from actual functionality
krauss
parents:
36323
diff
changeset
|
246 |
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
|
247 |
in |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
248 |
lthy |
42361 | 249 |
|> Proof_Context.note_thmss "" |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
250 |
[((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd |
42361 | 251 |
|> Proof_Context.note_thmss "" |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
252 |
[((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd |
42361 | 253 |
|> Proof_Context.note_thmss "" |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
254 |
[((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]), |
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
53614
diff
changeset
|
255 |
[([Goal.norm_result lthy termination], [])])] |> snd |
36547
2a9d0ec8c10d
return updated info record after termination proof
krauss
parents:
36522
diff
changeset
|
256 |
|> Proof.theorem NONE (snd oo afterqed) [[(goal, [])]] |
34232
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 |
|
36519
46bf776a81e0
ML interface uses plain command names, following conventions from typedef
krauss
parents:
36518
diff
changeset
|
259 |
val termination = gen_termination Syntax.check_term |
46bf776a81e0
ML interface uses plain command names, following conventions from typedef
krauss
parents:
36518
diff
changeset
|
260 |
val termination_cmd = gen_termination Syntax.read_term |
33099
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 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
263 |
(* Datatype hook to declare datatype congs as "function_congs" *) |
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 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
266 |
fun add_case_cong n thy = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
267 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
268 |
val cong = #case_cong (Datatype.the_info thy n) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
269 |
|> safe_mk_meta_eq |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
270 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
271 |
Context.theory_map |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34231
diff
changeset
|
272 |
(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
|
273 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
274 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
275 |
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
|
276 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
277 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
278 |
(* setup *) |
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 setup = |
55085
0e8e4dc55866
moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
blanchet
parents:
54883
diff
changeset
|
281 |
setup_case_cong |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
282 |
#> Function_Common.Termination_Simps.setup |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
283 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
284 |
val get_congs = Function_Ctx_Tree.get_function_congs |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
285 |
|
34230 | 286 |
fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t |
287 |
|> the_single |> snd |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
288 |
|
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36547
diff
changeset
|
289 |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
290 |
(* outer syntax *) |
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 |
val _ = |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
45592
diff
changeset
|
293 |
Outer_Syntax.local_theory_to_proof' @{command_spec "function"} |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
45592
diff
changeset
|
294 |
"define general recursive functions" |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
45592
diff
changeset
|
295 |
(function_parser default_config |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
45592
diff
changeset
|
296 |
>> (fn ((config, fixes), statements) => function_cmd fixes statements config)) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
297 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
298 |
val _ = |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
45592
diff
changeset
|
299 |
Outer_Syntax.local_theory_to_proof @{command_spec "termination"} |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
45592
diff
changeset
|
300 |
"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
|
301 |
(Scan.option Parse.term >> termination_cmd) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
302 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
303 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
304 |
end |