author | wenzelm |
Fri, 13 May 2011 22:55:00 +0200 | |
changeset 42793 | 88bee9f6eec7 |
parent 42361 | 23f352990944 |
child 42947 | fcb6250bf6b4 |
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 |
|
36523
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
10 |
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
|
11 |
(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
|
12 |
local_theory -> Proof.context |
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
13 |
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
|
14 |
(Attrib.binding * string) list -> Function_Common.function_config -> |
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
15 |
local_theory -> Proof.context |
33098 | 16 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
17 |
val setup : theory -> theory |
33098 | 18 |
end |
19 |
||
20 |
structure Function_Fun : FUNCTION_FUN = |
|
21 |
struct |
|
22 |
||
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
33098
diff
changeset
|
23 |
open Function_Lib |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
33098
diff
changeset
|
24 |
open Function_Common |
33098 | 25 |
|
26 |
||
27 |
fun check_pats ctxt geq = |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
28 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
29 |
fun err str = error (cat_lines ["Malformed definition:", |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
30 |
str ^ " not allowed in sequential mode.", |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
31 |
Syntax.string_of_term ctxt geq]) |
42361 | 32 |
val thy = Proof_Context.theory_of ctxt |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
33 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
34 |
fun check_constr_pattern (Bound _) = () |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
35 |
| check_constr_pattern t = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
36 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
37 |
val (hd, args) = strip_comb t |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
38 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
39 |
(((case Datatype.info_of_constr thy (dest_Const hd) of |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
40 |
SOME _ => () |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
41 |
| NONE => err "Non-constructor pattern") |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
42 |
handle TERM ("dest_Const", _) => err "Non-constructor patterns"); |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
43 |
map check_constr_pattern args; |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
44 |
()) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
45 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
46 |
|
39276
2ad95934521f
improved error message for common mistake (fun f where "g x = ...")
krauss
parents:
36960
diff
changeset
|
47 |
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
|
48 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
49 |
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
|
50 |
val _ = map check_constr_pattern args |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
51 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
52 |
(* just count occurrences to check linearity *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
53 |
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
|
54 |
then err "Nonlinear patterns" else () |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
55 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
56 |
() |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
57 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
58 |
|
33098 | 59 |
fun mk_catchall fixes arity_of = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
60 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
61 |
fun mk_eqn ((fname, fT), _) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
62 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
63 |
val n = arity_of fname |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
64 |
val (argTs, rT) = chop n (binder_types fT) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
65 |
|> apsnd (fn Ts => Ts ---> body_type fT) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
66 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
67 |
val qs = map Free (Name.invent_list [] "a" n ~~ argTs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
68 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
69 |
HOLogic.mk_eq(list_comb (Free (fname, fT), qs), |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
70 |
Const ("HOL.undefined", rT)) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
71 |
|> HOLogic.mk_Trueprop |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
72 |
|> fold_rev Logic.all qs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
73 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
74 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
75 |
map mk_eqn fixes |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
76 |
end |
33098 | 77 |
|
78 |
fun add_catchall ctxt fixes spec = |
|
39276
2ad95934521f
improved error message for common mistake (fun f where "g x = ...")
krauss
parents:
36960
diff
changeset
|
79 |
let val fqgars = map (split_def ctxt (K true)) spec |
33098 | 80 |
val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars |
81 |
|> AList.lookup (op =) #> the |
|
82 |
in |
|
83 |
spec @ mk_catchall fixes arity_of |
|
84 |
end |
|
85 |
||
86 |
fun warn_if_redundant ctxt origs tss = |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
87 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
88 |
fun msg t = "Ignoring redundant equation: " ^ quote (Syntax.string_of_term ctxt t) |
33098 | 89 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
90 |
val (tss', _) = chop (length origs) tss |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
91 |
fun check (t, []) = (warning (msg t); []) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
92 |
| check (t, s) = s |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
93 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
94 |
(map check (origs ~~ tss'); tss) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
95 |
end |
33098 | 96 |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
33098
diff
changeset
|
97 |
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
|
98 |
if sequential then |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
99 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
100 |
val (bnds, eqss) = split_list spec |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
101 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
102 |
val eqs = map the_single eqss |
33098 | 103 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
104 |
val feqs = eqs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
105 |
|> tap (check_defs ctxt fixes) (* Standard checks *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
106 |
|> 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
|
107 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
108 |
val compleqs = add_catchall ctxt fixes feqs (* Completion *) |
33098 | 109 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
110 |
val spliteqs = warn_if_redundant ctxt feqs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
111 |
(Function_Split.split_all_equations ctxt compleqs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
112 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
113 |
fun restore_spec thms = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
114 |
bnds ~~ take (length bnds) (unflat spliteqs thms) |
33098 | 115 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
116 |
val spliteqs' = flat (take (length bnds) spliteqs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
117 |
val fnames = map (fst o fst) fixes |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
118 |
val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) spliteqs' |
33098 | 119 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
120 |
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
|
121 |
|> map (map snd) |
33098 | 122 |
|
123 |
||
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
124 |
val bnds' = bnds @ replicate (length spliteqs - length bnds) Attrib.empty_binding |
33098 | 125 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
126 |
(* using theorem names for case name currently disabled *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
127 |
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
|
128 |
(bnds' ~~ spliteqs) |> flat |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
129 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
130 |
(flat spliteqs, restore_spec, sort, case_names) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
131 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
132 |
else |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33957
diff
changeset
|
133 |
Function_Common.empty_preproc check_defs config ctxt fixes spec |
33098 | 134 |
|
135 |
val setup = |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
33098
diff
changeset
|
136 |
Context.theory_map (Function_Common.set_preproc sequential_preproc) |
33098 | 137 |
|
138 |
||
41417 | 139 |
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
|
140 |
domintros=false, partials=false } |
33098 | 141 |
|
36523
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
142 |
fun gen_add_fun add fixes statements config lthy = |
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
143 |
let |
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
144 |
fun pat_completeness_auto ctxt = |
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
145 |
Pat_Completeness.pat_completeness_tac ctxt 1 |
42793 | 146 |
THEN auto_tac ctxt |
36523
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
147 |
fun prove_termination lthy = |
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
148 |
Function.prove_termination NONE |
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
149 |
(Function_Common.get_termination_prover lthy lthy) lthy |
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
150 |
in |
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
151 |
lthy |
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
152 |
|> add fixes statements config pat_completeness_auto |> snd |
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
153 |
|> Local_Theory.restore |
36547
2a9d0ec8c10d
return updated info record after termination proof
krauss
parents:
36523
diff
changeset
|
154 |
|> prove_termination |> snd |
36523
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
155 |
end |
33098 | 156 |
|
36523
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
157 |
val add_fun = gen_add_fun Function.add_function |
a294e4ebe0a3
clarified signature; simpler implementation in terms of function's tactic interface
krauss
parents:
36521
diff
changeset
|
158 |
val add_fun_cmd = gen_add_fun Function.add_function_cmd |
33098 | 159 |
|
160 |
||
161 |
||
162 |
val _ = |
|
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36547
diff
changeset
|
163 |
Outer_Syntax.local_theory "fun" "define general recursive functions (short version)" |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36547
diff
changeset
|
164 |
Keyword.thy_decl |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
33098
diff
changeset
|
165 |
(function_parser fun_config |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36547
diff
changeset
|
166 |
>> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config)) |
33098 | 167 |
|
168 |
end |