author | haftmann |
Thu, 08 Jan 2015 18:23:27 +0100 | |
changeset 59321 | 2b40fb12b09d |
parent 59159 | 9312710451f5 |
child 59627 | bb1e4a35d506 |
permissions | -rw-r--r-- |
33098 | 1 |
(* Title: HOL/Tools/Function/fun.ML |
2 |
Author: Alexander Krauss, TU Muenchen |
|
3 |
||
41114 | 4 |
Command "fun": Function definitions with pattern splitting/completion |
5 |
and automated termination proofs. |
|
33098 | 6 |
*) |
7 |
||
8 |
signature FUNCTION_FUN = |
|
9 |
sig |
|
44237
2a2040c9d898
export Function_Fun.fun_config for user convenience;
wenzelm
parents:
43329
diff
changeset
|
10 |
val fun_config : Function_Common.function_config |
36523
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
11 |
val add_fun : (binding * typ option * mixfix) list -> |
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
12 |
(Attrib.binding * term) list -> Function_Common.function_config -> |
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
13 |
local_theory -> Proof.context |
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
14 |
val add_fun_cmd : (binding * string option * mixfix) list -> |
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
15 |
(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:
44237
diff
changeset
|
16 |
bool -> local_theory -> Proof.context |
33098 | 17 |
end |
18 |
||
19 |
structure Function_Fun : FUNCTION_FUN = |
|
20 |
struct |
|
21 |
||
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
33098
diff
changeset
|
22 |
open Function_Lib |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
33098
diff
changeset
|
23 |
open Function_Common |
33098 | 24 |
|
25 |
||
26 |
fun check_pats ctxt geq = |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
27 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
28 |
fun err str = error (cat_lines ["Malformed definition:", |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
29 |
str ^ " not allowed in sequential mode.", |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
30 |
Syntax.string_of_term ctxt geq]) |
42361 | 31 |
val thy = Proof_Context.theory_of ctxt |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
32 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
33 |
fun check_constr_pattern (Bound _) = () |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
34 |
| check_constr_pattern t = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
35 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
36 |
val (hd, args) = strip_comb t |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
37 |
in |
54407
e95831757903
ported part of function package to new 'Ctr_Sugar' abstraction
blanchet
parents:
49965
diff
changeset
|
38 |
(case hd of |
e95831757903
ported part of function package to new 'Ctr_Sugar' abstraction
blanchet
parents:
49965
diff
changeset
|
39 |
Const (hd_s, hd_T) => |
e95831757903
ported part of function package to new 'Ctr_Sugar' abstraction
blanchet
parents:
49965
diff
changeset
|
40 |
(case body_type hd_T of |
e95831757903
ported part of function package to new 'Ctr_Sugar' abstraction
blanchet
parents:
49965
diff
changeset
|
41 |
Type (Tname, _) => |
e95831757903
ported part of function package to new 'Ctr_Sugar' abstraction
blanchet
parents:
49965
diff
changeset
|
42 |
(case Ctr_Sugar.ctr_sugar_of ctxt Tname of |
e95831757903
ported part of function package to new 'Ctr_Sugar' abstraction
blanchet
parents:
49965
diff
changeset
|
43 |
SOME {ctrs, ...} => exists (fn Const (s, _) => s = hd_s) ctrs |
e95831757903
ported part of function package to new 'Ctr_Sugar' abstraction
blanchet
parents:
49965
diff
changeset
|
44 |
| NONE => false) |
e95831757903
ported part of function package to new 'Ctr_Sugar' abstraction
blanchet
parents:
49965
diff
changeset
|
45 |
| _ => false) |
e95831757903
ported part of function package to new 'Ctr_Sugar' abstraction
blanchet
parents:
49965
diff
changeset
|
46 |
| _ => false) orelse err "Non-constructor pattern"; |
e95831757903
ported part of function package to new 'Ctr_Sugar' abstraction
blanchet
parents:
49965
diff
changeset
|
47 |
map check_constr_pattern args; |
e95831757903
ported part of function package to new 'Ctr_Sugar' abstraction
blanchet
parents:
49965
diff
changeset
|
48 |
() |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
49 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
50 |
|
39276
2ad95934521f
improved error message for common mistake (fun f where "g x = ...")
krauss
parents:
36960
diff
changeset
|
51 |
val (_, qs, gs, args, _) = split_def ctxt (K true) geq |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
52 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
53 |
val _ = if not (null gs) then err "Conditional equations" else () |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
54 |
val _ = map check_constr_pattern args |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
55 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
56 |
(* just count occurrences to check linearity *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
57 |
val _ = if fold (fold_aterms (fn Bound _ => Integer.add 1 | _ => I)) args 0 > length qs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
58 |
then err "Nonlinear patterns" else () |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
59 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
60 |
() |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
61 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
62 |
|
33098 | 63 |
fun mk_catchall fixes arity_of = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
64 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
65 |
fun mk_eqn ((fname, fT), _) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
66 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
67 |
val n = arity_of fname |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
68 |
val (argTs, rT) = chop n (binder_types fT) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
69 |
|> apsnd (fn Ts => Ts ---> body_type fT) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
70 |
|
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
43323
diff
changeset
|
71 |
val qs = map Free (Name.invent Name.context "a" n ~~ argTs) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
72 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
73 |
HOLogic.mk_eq(list_comb (Free (fname, fT), qs), |
56254 | 74 |
Const (@{const_name undefined}, rT)) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
75 |
|> HOLogic.mk_Trueprop |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
76 |
|> fold_rev Logic.all qs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
77 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
78 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
79 |
map mk_eqn fixes |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
80 |
end |
33098 | 81 |
|
82 |
fun add_catchall ctxt fixes spec = |
|
39276
2ad95934521f
improved error message for common mistake (fun f where "g x = ...")
krauss
parents:
36960
diff
changeset
|
83 |
let val fqgars = map (split_def ctxt (K true)) spec |
33098 | 84 |
val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars |
85 |
|> AList.lookup (op =) #> the |
|
86 |
in |
|
87 |
spec @ mk_catchall fixes arity_of |
|
88 |
end |
|
89 |
||
48099
e7e647949c95
fun command: produce hard failure when equations do not contribute to the specification (i.e., are covered by preceding clauses), to avoid confusing inexperienced users
krauss
parents:
46961
diff
changeset
|
90 |
fun further_checks ctxt origs tss = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
91 |
let |
48099
e7e647949c95
fun command: produce hard failure when equations do not contribute to the specification (i.e., are covered by preceding clauses), to avoid confusing inexperienced users
krauss
parents:
46961
diff
changeset
|
92 |
fun fail_redundant t = |
e7e647949c95
fun command: produce hard failure when equations do not contribute to the specification (i.e., are covered by preceding clauses), to avoid confusing inexperienced users
krauss
parents:
46961
diff
changeset
|
93 |
error (cat_lines ["Equation is redundant (covered by preceding clauses):", Syntax.string_of_term ctxt t]) |
42947
fcb6250bf6b4
fun command produces warning when patterns are incomplete (somewhat analogous to primrec)
krauss
parents:
42793
diff
changeset
|
94 |
fun warn_missing strs = |
43277 | 95 |
warning (cat_lines ("Missing patterns in function definition:" :: strs)) |
42947
fcb6250bf6b4
fun command produces warning when patterns are incomplete (somewhat analogous to primrec)
krauss
parents:
42793
diff
changeset
|
96 |
|
fcb6250bf6b4
fun command produces warning when patterns are incomplete (somewhat analogous to primrec)
krauss
parents:
42793
diff
changeset
|
97 |
val (tss', added) = chop (length origs) tss |
33098 | 98 |
|
42947
fcb6250bf6b4
fun command produces warning when patterns are incomplete (somewhat analogous to primrec)
krauss
parents:
42793
diff
changeset
|
99 |
val _ = case chop 3 (flat added) of |
fcb6250bf6b4
fun command produces warning when patterns are incomplete (somewhat analogous to primrec)
krauss
parents:
42793
diff
changeset
|
100 |
([], []) => () |
fcb6250bf6b4
fun command produces warning when patterns are incomplete (somewhat analogous to primrec)
krauss
parents:
42793
diff
changeset
|
101 |
| (eqs, []) => warn_missing (map (Syntax.string_of_term ctxt) eqs) |
fcb6250bf6b4
fun command produces warning when patterns are incomplete (somewhat analogous to primrec)
krauss
parents:
42793
diff
changeset
|
102 |
| (eqs, rest) => warn_missing (map (Syntax.string_of_term ctxt) eqs |
fcb6250bf6b4
fun command produces warning when patterns are incomplete (somewhat analogous to primrec)
krauss
parents:
42793
diff
changeset
|
103 |
@ ["(" ^ string_of_int (length rest) ^ " more)"]) |
fcb6250bf6b4
fun command produces warning when patterns are incomplete (somewhat analogous to primrec)
krauss
parents:
42793
diff
changeset
|
104 |
|
fcb6250bf6b4
fun command produces warning when patterns are incomplete (somewhat analogous to primrec)
krauss
parents:
42793
diff
changeset
|
105 |
val _ = (origs ~~ tss') |
48099
e7e647949c95
fun command: produce hard failure when equations do not contribute to the specification (i.e., are covered by preceding clauses), to avoid confusing inexperienced users
krauss
parents:
46961
diff
changeset
|
106 |
|> map (fn (t, ts) => if null ts then fail_redundant t else ()) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
107 |
in |
42947
fcb6250bf6b4
fun command produces warning when patterns are incomplete (somewhat analogous to primrec)
krauss
parents:
42793
diff
changeset
|
108 |
() |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
109 |
end |
33098 | 110 |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
33098
diff
changeset
|
111 |
fun sequential_preproc (config as FunctionConfig {sequential, ...}) ctxt fixes spec = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
112 |
if sequential then |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
113 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
114 |
val (bnds, eqss) = split_list spec |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
115 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
116 |
val eqs = map the_single eqss |
33098 | 117 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
118 |
val feqs = eqs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
119 |
|> tap (check_defs ctxt fixes) (* Standard checks *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
120 |
|> tap (map (check_pats ctxt)) (* More checks for sequential mode *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
121 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
122 |
val compleqs = add_catchall ctxt fixes feqs (* Completion *) |
33098 | 123 |
|
42947
fcb6250bf6b4
fun command produces warning when patterns are incomplete (somewhat analogous to primrec)
krauss
parents:
42793
diff
changeset
|
124 |
val spliteqs = Function_Split.split_all_equations ctxt compleqs |
48099
e7e647949c95
fun command: produce hard failure when equations do not contribute to the specification (i.e., are covered by preceding clauses), to avoid confusing inexperienced users
krauss
parents:
46961
diff
changeset
|
125 |
|> tap (further_checks ctxt feqs) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
126 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
127 |
fun restore_spec thms = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
128 |
bnds ~~ take (length bnds) (unflat spliteqs thms) |
33098 | 129 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
130 |
val spliteqs' = flat (take (length bnds) spliteqs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
131 |
val fnames = map (fst o fst) fixes |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
132 |
val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) spliteqs' |
33098 | 133 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
134 |
fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) (indices ~~ xs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
135 |
|> map (map snd) |
33098 | 136 |
|
137 |
||
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
138 |
val bnds' = bnds @ replicate (length spliteqs - length bnds) Attrib.empty_binding |
33098 | 139 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
140 |
(* using theorem names for case name currently disabled *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
141 |
val case_names = map_index (fn (i, (_, es)) => mk_case_names i "" (length es)) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
142 |
(bnds' ~~ spliteqs) |> flat |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
143 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
144 |
(flat spliteqs, restore_spec, sort, case_names) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
145 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
146 |
else |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
147 |
Function_Common.empty_preproc check_defs config ctxt fixes spec |
33098 | 148 |
|
58826 | 149 |
val _ = Theory.setup (Context.theory_map (Function_Common.set_preproc sequential_preproc)) |
150 |
||
33098 | 151 |
|
152 |
||
41417 | 153 |
val fun_config = FunctionConfig { sequential=true, default=NONE, |
41846
b368a7aee46a
removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents:
41417
diff
changeset
|
154 |
domintros=false, partials=false } |
33098 | 155 |
|
44239
47ecd30e018d
less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);
wenzelm
parents:
44237
diff
changeset
|
156 |
fun gen_add_fun add lthy = |
36523
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
157 |
let |
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
158 |
fun pat_completeness_auto ctxt = |
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
159 |
Pat_Completeness.pat_completeness_tac ctxt 1 |
42793 | 160 |
THEN auto_tac ctxt |
36523
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
161 |
fun prove_termination lthy = |
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
162 |
Function.prove_termination NONE |
59159 | 163 |
(Function_Common.termination_prover_tac lthy) lthy |
36523
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
164 |
in |
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
165 |
lthy |
44239
47ecd30e018d
less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);
wenzelm
parents:
44237
diff
changeset
|
166 |
|> add pat_completeness_auto |> snd |
36547
2a9d0ec8c10d
return updated info record after termination proof
krauss
parents:
36523
diff
changeset
|
167 |
|> prove_termination |> snd |
36523
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
168 |
end |
33098 | 169 |
|
44239
47ecd30e018d
less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);
wenzelm
parents:
44237
diff
changeset
|
170 |
fun add_fun a b c = gen_add_fun (Function.add_function a b c) |
47ecd30e018d
less verbosity for 'function' and 'fun': observe "int" flag more carefully (cf. a32ca9165928);
wenzelm
parents:
44237
diff
changeset
|
171 |
fun add_fun_cmd a b c int = gen_add_fun (fn tac => Function.add_function_cmd a b c tac int) |
33098 | 172 |
|
173 |
||
174 |
||
175 |
val _ = |
|
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
45639
diff
changeset
|
176 |
Outer_Syntax.local_theory' @{command_spec "fun"} |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
45639
diff
changeset
|
177 |
"define general recursive functions (short version)" |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
45639
diff
changeset
|
178 |
(function_parser fun_config |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
45639
diff
changeset
|
179 |
>> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config)) |
33098 | 180 |
|
181 |
end |