22166
|
1 |
(* Title: HOL/Tools/function_package/fundef_core.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Alexander Krauss, TU Muenchen
|
|
4 |
|
|
5 |
A package for general recursive function definitions.
|
|
6 |
Main functionality
|
|
7 |
*)
|
|
8 |
|
|
9 |
signature FUNDEF_CORE =
|
|
10 |
sig
|
|
11 |
val prepare_fundef : FundefCommon.fundef_config
|
|
12 |
-> string (* defname *)
|
|
13 |
-> (string * typ * mixfix) (* defined symbol *)
|
|
14 |
-> ((string * typ) list * term list * term * term) list (* specification *)
|
|
15 |
-> string (* default_value, not parsed yet *)
|
|
16 |
-> local_theory
|
|
17 |
|
|
18 |
-> (term (* f *)
|
|
19 |
* thm (* goalstate *)
|
|
20 |
* (thm -> FundefCommon.fundef_result) (* continuation *)
|
|
21 |
) * local_theory
|
|
22 |
|
|
23 |
end
|
|
24 |
|
|
25 |
structure FundefCore : FUNDEF_CORE =
|
|
26 |
struct
|
|
27 |
|
|
28 |
|
|
29 |
open FundefLib
|
|
30 |
open FundefCommon
|
|
31 |
open FundefAbbrev
|
|
32 |
|
|
33 |
datatype globals =
|
|
34 |
Globals of {
|
|
35 |
fvar: term,
|
|
36 |
domT: typ,
|
|
37 |
ranT: typ,
|
|
38 |
h: term,
|
|
39 |
y: term,
|
|
40 |
x: term,
|
|
41 |
z: term,
|
|
42 |
a: term,
|
|
43 |
P: term,
|
|
44 |
D: term,
|
|
45 |
Pbool:term
|
|
46 |
}
|
|
47 |
|
|
48 |
|
|
49 |
datatype rec_call_info =
|
|
50 |
RCInfo of
|
|
51 |
{
|
|
52 |
RIvs: (string * typ) list, (* Call context: fixes and assumes *)
|
|
53 |
CCas: thm list,
|
|
54 |
rcarg: term, (* The recursive argument *)
|
|
55 |
|
|
56 |
llRI: thm,
|
|
57 |
h_assum: term
|
|
58 |
}
|
|
59 |
|
|
60 |
|
|
61 |
datatype clause_context =
|
|
62 |
ClauseContext of
|
|
63 |
{
|
|
64 |
ctxt : Proof.context,
|
|
65 |
|
|
66 |
qs : term list,
|
|
67 |
gs : term list,
|
|
68 |
lhs: term,
|
|
69 |
rhs: term,
|
|
70 |
|
|
71 |
cqs: cterm list,
|
|
72 |
ags: thm list,
|
|
73 |
case_hyp : thm
|
|
74 |
}
|
|
75 |
|
|
76 |
|
|
77 |
fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) =
|
|
78 |
ClauseContext { ctxt = ProofContext.transfer thy ctxt,
|
|
79 |
qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp }
|
|
80 |
|
|
81 |
|
|
82 |
datatype clause_info =
|
|
83 |
ClauseInfo of
|
|
84 |
{
|
|
85 |
no: int,
|
|
86 |
qglr : ((string * typ) list * term list * term * term),
|
|
87 |
cdata : clause_context,
|
|
88 |
|
|
89 |
tree: ctx_tree,
|
|
90 |
lGI: thm,
|
|
91 |
RCs: rec_call_info list
|
|
92 |
}
|
|
93 |
|
|
94 |
|
|
95 |
(* Theory dependencies. *)
|
|
96 |
val Pair_inject = thm "Product_Type.Pair_inject";
|
|
97 |
|
|
98 |
val acc_induct_rule = thm "FunDef.accP_induct_rule"
|
|
99 |
|
|
100 |
val ex1_implies_ex = thm "FunDef.fundef_ex1_existence"
|
|
101 |
val ex1_implies_un = thm "FunDef.fundef_ex1_uniqueness"
|
|
102 |
val ex1_implies_iff = thm "FunDef.fundef_ex1_iff"
|
|
103 |
|
|
104 |
val acc_downward = thm "FunDef.accP_downward"
|
|
105 |
val accI = thm "FunDef.accPI"
|
|
106 |
val case_split = thm "HOL.case_split_thm"
|
|
107 |
val fundef_default_value = thm "FunDef.fundef_default_value"
|
|
108 |
val not_accP_down = thm "FunDef.not_accP_down"
|
|
109 |
|
|
110 |
|
|
111 |
|
|
112 |
fun find_calls tree =
|
|
113 |
let
|
|
114 |
fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = ([], (fixes, assumes, arg) :: xs)
|
|
115 |
| add_Ri _ _ _ _ = raise Match
|
|
116 |
in
|
|
117 |
rev (FundefCtxTree.traverse_tree add_Ri tree [])
|
|
118 |
end
|
|
119 |
|
|
120 |
|
|
121 |
(** building proof obligations *)
|
|
122 |
|
|
123 |
fun mk_compat_proof_obligations domT ranT fvar f glrs =
|
|
124 |
let
|
|
125 |
fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
|
|
126 |
let
|
|
127 |
val shift = incr_boundvars (length qs')
|
|
128 |
in
|
|
129 |
(implies $ Trueprop (eq_const domT $ shift lhs $ lhs')
|
|
130 |
$ Trueprop (eq_const ranT $ shift rhs $ rhs'))
|
|
131 |
|> fold_rev (curry Logic.mk_implies) (map shift gs @ gs')
|
|
132 |
|> fold_rev (fn (n,T) => fn b => all T $ Abs(n,T,b)) (qs @ qs')
|
|
133 |
|> curry abstract_over fvar
|
|
134 |
|> curry subst_bound f
|
|
135 |
end
|
|
136 |
in
|
|
137 |
map mk_impl (unordered_pairs glrs)
|
|
138 |
end
|
|
139 |
|
|
140 |
|
|
141 |
fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs =
|
|
142 |
let
|
|
143 |
fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) =
|
|
144 |
Trueprop Pbool
|
|
145 |
|> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
|
|
146 |
|> fold_rev (curry Logic.mk_implies) gs
|
|
147 |
|> fold_rev mk_forall_rename (map fst oqs ~~ qs)
|
|
148 |
in
|
|
149 |
Trueprop Pbool
|
|
150 |
|> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs)
|
|
151 |
|> mk_forall_rename ("x", x)
|
|
152 |
|> mk_forall_rename ("P", Pbool)
|
|
153 |
end
|
|
154 |
|
|
155 |
(** making a context with it's own local bindings **)
|
|
156 |
|
|
157 |
fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) =
|
|
158 |
let
|
|
159 |
val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
|
|
160 |
|>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
|
|
161 |
|
|
162 |
val thy = ProofContext.theory_of ctxt'
|
|
163 |
|
|
164 |
fun inst t = subst_bounds (rev qs, t)
|
|
165 |
val gs = map inst pre_gs
|
|
166 |
val lhs = inst pre_lhs
|
|
167 |
val rhs = inst pre_rhs
|
|
168 |
|
|
169 |
val cqs = map (cterm_of thy) qs
|
|
170 |
val ags = map (assume o cterm_of thy) gs
|
|
171 |
|
|
172 |
val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
|
|
173 |
in
|
|
174 |
ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs,
|
|
175 |
cqs = cqs, ags = ags, case_hyp = case_hyp }
|
|
176 |
end
|
|
177 |
|
|
178 |
|
|
179 |
(* lowlevel term function *)
|
|
180 |
fun abstract_over_list vs body =
|
|
181 |
let
|
|
182 |
exception SAME;
|
|
183 |
fun abs lev v tm =
|
|
184 |
if v aconv tm then Bound lev
|
|
185 |
else
|
|
186 |
(case tm of
|
|
187 |
Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t)
|
|
188 |
| t $ u => (abs lev v t $ (abs lev v u handle SAME => u) handle SAME => t $ abs lev v u)
|
|
189 |
| _ => raise SAME);
|
|
190 |
in
|
|
191 |
fold_index (fn (i,v) => fn t => abs i v t handle SAME => t) vs body
|
|
192 |
end
|
|
193 |
|
|
194 |
|
|
195 |
|
|
196 |
fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =
|
|
197 |
let
|
|
198 |
val Globals {h, fvar, x, ...} = globals
|
|
199 |
|
|
200 |
val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
|
|
201 |
val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
|
|
202 |
|
|
203 |
(* Instantiate the GIntro thm with "f" and import into the clause context. *)
|
|
204 |
val lGI = GIntro_thm
|
|
205 |
|> forall_elim (cert f)
|
|
206 |
|> fold forall_elim cqs
|
|
207 |
|> fold implies_elim_swp ags
|
|
208 |
|
|
209 |
fun mk_call_info (rcfix, rcassm, rcarg) RI =
|
|
210 |
let
|
|
211 |
val llRI = RI
|
|
212 |
|> fold forall_elim cqs
|
|
213 |
|> fold (forall_elim o cert o Free) rcfix
|
|
214 |
|> fold implies_elim_swp ags
|
|
215 |
|> fold implies_elim_swp rcassm
|
|
216 |
|
|
217 |
val h_assum =
|
|
218 |
Trueprop (G $ rcarg $ (h $ rcarg))
|
|
219 |
|> fold_rev (curry Logic.mk_implies o prop_of) rcassm
|
|
220 |
|> fold_rev (mk_forall o Free) rcfix
|
|
221 |
|> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []
|
|
222 |
|> abstract_over_list (rev qs)
|
|
223 |
in
|
|
224 |
RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum}
|
|
225 |
end
|
|
226 |
|
|
227 |
val RC_infos = map2 mk_call_info RCs RIntro_thms
|
|
228 |
in
|
|
229 |
ClauseInfo
|
|
230 |
{
|
|
231 |
no=no,
|
|
232 |
cdata=cdata,
|
|
233 |
qglr=qglr,
|
|
234 |
|
|
235 |
lGI=lGI,
|
|
236 |
RCs=RC_infos,
|
|
237 |
tree=tree
|
|
238 |
}
|
|
239 |
end
|
|
240 |
|
|
241 |
|
|
242 |
|
|
243 |
|
|
244 |
|
|
245 |
|
|
246 |
|
|
247 |
(* replace this by a table later*)
|
|
248 |
fun store_compat_thms 0 thms = []
|
|
249 |
| store_compat_thms n thms =
|
|
250 |
let
|
|
251 |
val (thms1, thms2) = chop n thms
|
|
252 |
in
|
|
253 |
(thms1 :: store_compat_thms (n - 1) thms2)
|
|
254 |
end
|
|
255 |
|
|
256 |
(* expects i <= j *)
|
|
257 |
fun lookup_compat_thm i j cts =
|
|
258 |
nth (nth cts (i - 1)) (j - i)
|
|
259 |
|
|
260 |
(* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *)
|
|
261 |
(* if j < i, then turn around *)
|
|
262 |
fun get_compat_thm thy cts i j ctxi ctxj =
|
|
263 |
let
|
|
264 |
val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi
|
|
265 |
val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj
|
|
266 |
|
|
267 |
val lhsi_eq_lhsj = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj)))
|
|
268 |
in if j < i then
|
|
269 |
let
|
|
270 |
val compat = lookup_compat_thm j i cts
|
|
271 |
in
|
|
272 |
compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
|
|
273 |
|> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
|
|
274 |
|> fold implies_elim_swp agsj
|
|
275 |
|> fold implies_elim_swp agsi
|
|
276 |
|> implies_elim_swp ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
|
|
277 |
end
|
|
278 |
else
|
|
279 |
let
|
|
280 |
val compat = lookup_compat_thm i j cts
|
|
281 |
in
|
|
282 |
compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
|
|
283 |
|> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
|
|
284 |
|> fold implies_elim_swp agsi
|
|
285 |
|> fold implies_elim_swp agsj
|
|
286 |
|> implies_elim_swp (assume lhsi_eq_lhsj)
|
|
287 |
|> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
|
|
288 |
end
|
|
289 |
end
|
|
290 |
|
|
291 |
|
|
292 |
|
|
293 |
|
|
294 |
(* Generates the replacement lemma in fully quantified form. *)
|
|
295 |
fun mk_replacement_lemma thy h ih_elim clause =
|
|
296 |
let
|
|
297 |
val ClauseInfo {cdata=ClauseContext {qs, lhs, rhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause
|
|
298 |
|
|
299 |
val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim
|
|
300 |
|
|
301 |
val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
|
|
302 |
val h_assums = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
|
|
303 |
|
|
304 |
val ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *)
|
|
305 |
|
|
306 |
val (eql, _) = FundefCtxTree.rewrite_by_tree thy h ih_elim_case_inst (Ris ~~ h_assums) tree
|
|
307 |
|
|
308 |
val replace_lemma = (eql RS meta_eq_to_obj_eq)
|
|
309 |
|> implies_intr (cprop_of case_hyp)
|
|
310 |
|> fold_rev (implies_intr o cprop_of) h_assums
|
|
311 |
|> fold_rev (implies_intr o cprop_of) ags
|
|
312 |
|> fold_rev forall_intr cqs
|
|
313 |
|> Goal.close_result
|
|
314 |
in
|
|
315 |
replace_lemma
|
|
316 |
end
|
|
317 |
|
|
318 |
|
|
319 |
fun mk_uniqueness_clause thy globals f compat_store clausei clausej RLj =
|
|
320 |
let
|
|
321 |
val Globals {h, y, x, fvar, ...} = globals
|
|
322 |
val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei
|
|
323 |
val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej
|
|
324 |
|
|
325 |
val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...}
|
|
326 |
= mk_clause_context x ctxti cdescj
|
|
327 |
|
|
328 |
val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj'
|
|
329 |
val compat = get_compat_thm thy compat_store i j cctxi cctxj
|
|
330 |
val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj
|
|
331 |
|
|
332 |
val RLj_import =
|
|
333 |
RLj |> fold forall_elim cqsj'
|
|
334 |
|> fold implies_elim_swp agsj'
|
|
335 |
|> fold implies_elim_swp Ghsj'
|
|
336 |
|
|
337 |
val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h))))
|
|
338 |
val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
|
|
339 |
in
|
|
340 |
(trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
|
|
341 |
|> implies_elim RLj_import (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
|
|
342 |
|> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
|
|
343 |
|> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
|
|
344 |
|> fold_rev (implies_intr o cprop_of) Ghsj'
|
|
345 |
|> fold_rev (implies_intr o cprop_of) agsj' (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *)
|
|
346 |
|> implies_intr (cprop_of y_eq_rhsj'h)
|
|
347 |
|> implies_intr (cprop_of lhsi_eq_lhsj')
|
|
348 |
|> fold_rev forall_intr (cterm_of thy h :: cqsj')
|
|
349 |
end
|
|
350 |
|
|
351 |
|
|
352 |
|
|
353 |
fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
|
|
354 |
let
|
|
355 |
val Globals {x, y, ranT, fvar, ...} = globals
|
|
356 |
val ClauseInfo {cdata = ClauseContext {lhs, rhs, qs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
|
|
357 |
val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
|
|
358 |
|
|
359 |
val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
|
|
360 |
|
|
361 |
fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
|
|
362 |
|> fold_rev (implies_intr o cprop_of) CCas
|
|
363 |
|> fold_rev (forall_intr o cterm_of thy o Free) RIvs
|
|
364 |
|
|
365 |
val existence = fold (curry op COMP o prep_RC) RCs lGI
|
|
366 |
|
|
367 |
val P = cterm_of thy (mk_eq (y, rhsC))
|
|
368 |
val G_lhs_y = assume (cterm_of thy (Trueprop (G $ lhs $ y)))
|
|
369 |
|
|
370 |
val unique_clauses = map2 (mk_uniqueness_clause thy globals f compat_store clausei) clauses rep_lemmas
|
|
371 |
|
|
372 |
val uniqueness = G_cases
|
|
373 |
|> forall_elim (cterm_of thy lhs)
|
|
374 |
|> forall_elim (cterm_of thy y)
|
|
375 |
|> forall_elim P
|
|
376 |
|> implies_elim_swp G_lhs_y
|
|
377 |
|> fold implies_elim_swp unique_clauses
|
|
378 |
|> implies_intr (cprop_of G_lhs_y)
|
|
379 |
|> forall_intr (cterm_of thy y)
|
|
380 |
|
|
381 |
val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *)
|
|
382 |
|
|
383 |
val exactly_one =
|
|
384 |
ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)]
|
|
385 |
|> curry (op COMP) existence
|
|
386 |
|> curry (op COMP) uniqueness
|
|
387 |
|> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
|
|
388 |
|> implies_intr (cprop_of case_hyp)
|
|
389 |
|> fold_rev (implies_intr o cprop_of) ags
|
|
390 |
|> fold_rev forall_intr cqs
|
|
391 |
|
|
392 |
val function_value =
|
|
393 |
existence
|
|
394 |
|> implies_intr ihyp
|
|
395 |
|> implies_intr (cprop_of case_hyp)
|
|
396 |
|> forall_intr (cterm_of thy x)
|
|
397 |
|> forall_elim (cterm_of thy lhs)
|
|
398 |
|> curry (op RS) refl
|
|
399 |
in
|
|
400 |
(exactly_one, function_value)
|
|
401 |
end
|
|
402 |
|
|
403 |
|
|
404 |
|
|
405 |
|
|
406 |
fun prove_stuff thy congs globals G f R clauses complete compat compat_store G_elim f_def =
|
|
407 |
let
|
|
408 |
val Globals {h, domT, ranT, x, ...} = globals
|
|
409 |
|
|
410 |
(* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
|
|
411 |
val ihyp = all domT $ Abs ("z", domT,
|
|
412 |
implies $ Trueprop (R $ Bound 0 $ x)
|
|
413 |
$ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
|
|
414 |
Abs ("y", ranT, G $ Bound 1 $ Bound 0)))
|
|
415 |
|> cterm_of thy
|
|
416 |
|
|
417 |
val ihyp_thm = assume ihyp |> forall_elim_vars 0
|
|
418 |
val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
|
|
419 |
val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
|
|
420 |
|
|
421 |
val _ = Output.debug (K "Proving Replacement lemmas...")
|
|
422 |
val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
|
|
423 |
|
|
424 |
val _ = Output.debug (K "Proving cases for unique existence...")
|
|
425 |
val (ex1s, values) =
|
|
426 |
split_list (map (mk_uniqueness_case thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
|
|
427 |
|
|
428 |
val _ = Output.debug (K "Proving: Graph is a function") (* FIXME: Rewrite this proof. *)
|
|
429 |
val graph_is_function = complete
|
|
430 |
|> forall_elim_vars 0
|
|
431 |
|> fold (curry op COMP) ex1s
|
|
432 |
|> implies_intr (ihyp)
|
|
433 |
|> implies_intr (cterm_of thy (Trueprop (mk_acc domT R $ x)))
|
|
434 |
|> forall_intr (cterm_of thy x)
|
|
435 |
|> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
|
|
436 |
|> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it)
|
|
437 |
|
|
438 |
val goalstate = Conjunction.intr graph_is_function complete
|
|
439 |
|> Goal.close_result
|
|
440 |
|> Goal.protect
|
|
441 |
|> fold_rev (implies_intr o cprop_of) compat
|
|
442 |
|> implies_intr (cprop_of complete)
|
|
443 |
in
|
|
444 |
(goalstate, values)
|
|
445 |
end
|
|
446 |
|
|
447 |
|
|
448 |
fun define_graph Gname fvar domT ranT clauses RCss lthy =
|
|
449 |
let
|
|
450 |
val GT = domT --> ranT --> boolT
|
|
451 |
val Gvar = Free (the_single (Variable.variant_frees lthy [] [(Gname, GT)]))
|
|
452 |
|
|
453 |
fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
|
|
454 |
let
|
|
455 |
fun mk_h_assm (rcfix, rcassm, rcarg) =
|
|
456 |
Trueprop (Gvar $ rcarg $ (fvar $ rcarg))
|
|
457 |
|> fold_rev (curry Logic.mk_implies o prop_of) rcassm
|
|
458 |
|> fold_rev (mk_forall o Free) rcfix
|
|
459 |
in
|
|
460 |
Trueprop (Gvar $ lhs $ rhs)
|
|
461 |
|> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
|
|
462 |
|> fold_rev (curry Logic.mk_implies) gs
|
|
463 |
|> fold_rev mk_forall (fvar :: qs)
|
|
464 |
end
|
|
465 |
|
|
466 |
val G_intros = map2 mk_GIntro clauses RCss
|
|
467 |
|
|
468 |
val (GIntro_thms, (G, G_elim, G_induct, lthy)) =
|
|
469 |
FundefInductiveWrap.inductive_def G_intros ((dest_Free Gvar, NoSyn), lthy)
|
|
470 |
in
|
|
471 |
((G, GIntro_thms, G_elim, G_induct), lthy)
|
|
472 |
end
|
|
473 |
|
|
474 |
|
|
475 |
|
|
476 |
fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
|
|
477 |
let
|
|
478 |
val f_def =
|
|
479 |
Abs ("x", domT, Const ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $
|
|
480 |
Abs ("y", ranT, G $ Bound 1 $ Bound 0))
|
|
481 |
|> Envir.beta_norm (* FIXME: LocalTheory.def does not work if not beta-normal *)
|
|
482 |
|
|
483 |
val ((f, (_, f_defthm)), lthy) =
|
|
484 |
LocalTheory.def Thm.internalK ((fname ^ "C", mixfix), ((fdefname, []), f_def)) lthy
|
|
485 |
in
|
|
486 |
((f, f_defthm), lthy)
|
|
487 |
end
|
|
488 |
|
|
489 |
|
|
490 |
fun define_recursion_relation Rname domT ranT fvar f qglrs clauses RCss lthy =
|
|
491 |
let
|
|
492 |
|
|
493 |
val RT = domT --> domT --> boolT
|
|
494 |
val Rvar = Free (the_single (Variable.variant_frees lthy [] [(Rname, RT)]))
|
|
495 |
|
|
496 |
fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
|
|
497 |
Trueprop (Rvar $ rcarg $ lhs)
|
|
498 |
|> fold_rev (curry Logic.mk_implies o prop_of) rcassm
|
|
499 |
|> fold_rev (curry Logic.mk_implies) gs
|
|
500 |
|> fold_rev (mk_forall o Free) rcfix
|
|
501 |
|> fold_rev mk_forall_rename (map fst oqs ~~ qs)
|
|
502 |
(* "!!qs xs. CS ==> G => (r, lhs) : R" *)
|
|
503 |
|
|
504 |
val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
|
|
505 |
|
|
506 |
val (RIntro_thmss, (R, R_elim, _, lthy)) =
|
|
507 |
fold_burrow FundefInductiveWrap.inductive_def R_intross ((dest_Free Rvar, NoSyn), lthy)
|
|
508 |
in
|
|
509 |
((R, RIntro_thmss, R_elim), lthy)
|
|
510 |
end
|
|
511 |
|
|
512 |
|
|
513 |
fun fix_globals domT ranT fvar ctxt =
|
|
514 |
let
|
|
515 |
val ([h, y, x, z, a, D, P, Pbool],ctxt') =
|
|
516 |
Variable.variant_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
|
|
517 |
in
|
|
518 |
(Globals {h = Free (h, domT --> ranT),
|
|
519 |
y = Free (y, ranT),
|
|
520 |
x = Free (x, domT),
|
|
521 |
z = Free (z, domT),
|
|
522 |
a = Free (a, domT),
|
|
523 |
D = Free (D, domT --> boolT),
|
|
524 |
P = Free (P, domT --> boolT),
|
|
525 |
Pbool = Free (Pbool, boolT),
|
|
526 |
fvar = fvar,
|
|
527 |
domT = domT,
|
|
528 |
ranT = ranT
|
|
529 |
},
|
|
530 |
ctxt')
|
|
531 |
end
|
|
532 |
|
|
533 |
|
|
534 |
|
|
535 |
fun inst_RC thy fvar f (rcfix, rcassm, rcarg) =
|
|
536 |
let
|
|
537 |
fun inst_term t = subst_bound(f, abstract_over (fvar, t))
|
|
538 |
in
|
|
539 |
(rcfix, map (assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg)
|
|
540 |
end
|
|
541 |
|
|
542 |
|
|
543 |
|
|
544 |
(**********************************************************
|
|
545 |
* PROVING THE RULES
|
|
546 |
**********************************************************)
|
|
547 |
|
|
548 |
fun mk_psimps thy globals R clauses valthms f_iff graph_is_function =
|
|
549 |
let
|
|
550 |
val Globals {domT, z, ...} = globals
|
|
551 |
|
|
552 |
fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm =
|
|
553 |
let
|
|
554 |
val lhs_acc = cterm_of thy (Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *)
|
|
555 |
val z_smaller = cterm_of thy (Trueprop (R $ z $ lhs)) (* "R z lhs" *)
|
|
556 |
in
|
|
557 |
((assume z_smaller) RS ((assume lhs_acc) RS acc_downward))
|
|
558 |
|> (fn it => it COMP graph_is_function)
|
|
559 |
|> implies_intr z_smaller
|
|
560 |
|> forall_intr (cterm_of thy z)
|
|
561 |
|> (fn it => it COMP valthm)
|
|
562 |
|> implies_intr lhs_acc
|
|
563 |
|> asm_simplify (HOL_basic_ss addsimps [f_iff])
|
|
564 |
|> fold_rev (implies_intr o cprop_of) ags
|
|
565 |
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
|
|
566 |
end
|
|
567 |
in
|
|
568 |
map2 mk_psimp clauses valthms
|
|
569 |
end
|
|
570 |
|
|
571 |
|
|
572 |
(** Induction rule **)
|
|
573 |
|
|
574 |
|
|
575 |
val acc_subset_induct = thm "FunDef.accP_subset_induct"
|
|
576 |
|
|
577 |
fun mk_partial_induct_rule thy globals R complete_thm clauses =
|
|
578 |
let
|
|
579 |
val Globals {domT, x, z, a, P, D, ...} = globals
|
|
580 |
val acc_R = mk_acc domT R
|
|
581 |
|
|
582 |
val x_D = assume (cterm_of thy (Trueprop (D $ x)))
|
|
583 |
val a_D = cterm_of thy (Trueprop (D $ a))
|
|
584 |
|
|
585 |
val D_subset = cterm_of thy (mk_forall x (implies $ Trueprop (D $ x) $ Trueprop (acc_R $ x)))
|
|
586 |
|
|
587 |
val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *)
|
|
588 |
mk_forall x
|
|
589 |
(mk_forall z (Logic.mk_implies (Trueprop (D $ x),
|
|
590 |
Logic.mk_implies (Trueprop (R $ z $ x),
|
|
591 |
Trueprop (D $ z)))))
|
|
592 |
|> cterm_of thy
|
|
593 |
|
|
594 |
|
|
595 |
(* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
|
|
596 |
val ihyp = all domT $ Abs ("z", domT,
|
|
597 |
implies $ Trueprop (R $ Bound 0 $ x)
|
|
598 |
$ Trueprop (P $ Bound 0))
|
|
599 |
|> cterm_of thy
|
|
600 |
|
|
601 |
val aihyp = assume ihyp
|
|
602 |
|
|
603 |
fun prove_case clause =
|
|
604 |
let
|
|
605 |
val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs,
|
|
606 |
qglr = (oqs, _, _, _), ...} = clause
|
|
607 |
|
|
608 |
val replace_x_ss = HOL_basic_ss addsimps [case_hyp]
|
|
609 |
val lhs_D = simplify replace_x_ss x_D (* lhs : D *)
|
|
610 |
val sih = full_simplify replace_x_ss aihyp
|
|
611 |
|
|
612 |
fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
|
|
613 |
sih |> forall_elim (cterm_of thy rcarg)
|
|
614 |
|> implies_elim_swp llRI
|
|
615 |
|> fold_rev (implies_intr o cprop_of) CCas
|
|
616 |
|> fold_rev (forall_intr o cterm_of thy o Free) RIvs
|
|
617 |
|
|
618 |
val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *)
|
|
619 |
|
|
620 |
val step = Trueprop (P $ lhs)
|
|
621 |
|> fold_rev (curry Logic.mk_implies o prop_of) P_recs
|
|
622 |
|> fold_rev (curry Logic.mk_implies) gs
|
|
623 |
|> curry Logic.mk_implies (Trueprop (D $ lhs))
|
|
624 |
|> fold_rev mk_forall_rename (map fst oqs ~~ qs)
|
|
625 |
|> cterm_of thy
|
|
626 |
|
|
627 |
val P_lhs = assume step
|
|
628 |
|> fold forall_elim cqs
|
|
629 |
|> implies_elim_swp lhs_D
|
|
630 |
|> fold_rev implies_elim_swp ags
|
|
631 |
|> fold implies_elim_swp P_recs
|
|
632 |
|
|
633 |
val res = cterm_of thy (Trueprop (P $ x))
|
|
634 |
|> Simplifier.rewrite replace_x_ss
|
|
635 |
|> symmetric (* P lhs == P x *)
|
|
636 |
|> (fn eql => equal_elim eql P_lhs) (* "P x" *)
|
|
637 |
|> implies_intr (cprop_of case_hyp)
|
|
638 |
|> fold_rev (implies_intr o cprop_of) ags
|
|
639 |
|> fold_rev forall_intr cqs
|
|
640 |
in
|
|
641 |
(res, step)
|
|
642 |
end
|
|
643 |
|
|
644 |
val (cases, steps) = split_list (map prove_case clauses)
|
|
645 |
|
|
646 |
val istep = complete_thm
|
|
647 |
|> forall_elim_vars 0
|
|
648 |
|> fold (curry op COMP) cases (* P x *)
|
|
649 |
|> implies_intr ihyp
|
|
650 |
|> implies_intr (cprop_of x_D)
|
|
651 |
|> forall_intr (cterm_of thy x)
|
|
652 |
|
|
653 |
val subset_induct_rule =
|
|
654 |
acc_subset_induct
|
|
655 |
|> (curry op COMP) (assume D_subset)
|
|
656 |
|> (curry op COMP) (assume D_dcl)
|
|
657 |
|> (curry op COMP) (assume a_D)
|
|
658 |
|> (curry op COMP) istep
|
|
659 |
|> fold_rev implies_intr steps
|
|
660 |
|> implies_intr a_D
|
|
661 |
|> implies_intr D_dcl
|
|
662 |
|> implies_intr D_subset
|
|
663 |
|
|
664 |
val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule
|
|
665 |
|
|
666 |
val simple_induct_rule =
|
|
667 |
subset_induct_rule
|
|
668 |
|> forall_intr (cterm_of thy D)
|
|
669 |
|> forall_elim (cterm_of thy acc_R)
|
|
670 |
|> assume_tac 1 |> Seq.hd
|
|
671 |
|> (curry op COMP) (acc_downward
|
|
672 |
|> (instantiate' [SOME (ctyp_of thy domT)]
|
|
673 |
(map (SOME o cterm_of thy) [R, x, z]))
|
|
674 |
|> forall_intr (cterm_of thy z)
|
|
675 |
|> forall_intr (cterm_of thy x))
|
|
676 |
|> forall_intr (cterm_of thy a)
|
|
677 |
|> forall_intr (cterm_of thy P)
|
|
678 |
in
|
|
679 |
(subset_induct_all, simple_induct_rule)
|
|
680 |
end
|
|
681 |
|
|
682 |
|
|
683 |
|
|
684 |
(* FIXME: This should probably use fixed goals, to be more reliable and faster *)
|
|
685 |
fun mk_domain_intro thy (Globals {domT, ...}) R R_cases clause =
|
|
686 |
let
|
|
687 |
val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...},
|
|
688 |
qglr = (oqs, _, _, _), ...} = clause
|
|
689 |
val goal = Trueprop (mk_acc domT R $ lhs)
|
|
690 |
|> fold_rev (curry Logic.mk_implies) gs
|
|
691 |
|> cterm_of thy
|
|
692 |
in
|
|
693 |
Goal.init goal
|
|
694 |
|> (SINGLE (resolve_tac [accI] 1)) |> the
|
|
695 |
|> (SINGLE (eresolve_tac [forall_elim_vars 0 R_cases] 1)) |> the
|
|
696 |
|> (SINGLE (CLASIMPSET auto_tac)) |> the
|
|
697 |
|> Goal.conclude
|
|
698 |
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
|
|
699 |
end
|
|
700 |
|
|
701 |
|
|
702 |
|
|
703 |
(** Termination rule **)
|
|
704 |
|
|
705 |
val wf_induct_rule = thm "FunDef.wfP_induct_rule";
|
|
706 |
val wf_in_rel = thm "FunDef.wf_in_rel";
|
|
707 |
val in_rel_def = thm "FunDef.in_rel_def";
|
|
708 |
|
|
709 |
fun mk_nest_term_case thy globals R' ihyp clause =
|
|
710 |
let
|
|
711 |
val Globals {x, z, ...} = globals
|
|
712 |
val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree,
|
|
713 |
qglr=(oqs, _, _, _), ...} = clause
|
|
714 |
|
|
715 |
val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
|
|
716 |
|
|
717 |
fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) =
|
|
718 |
let
|
|
719 |
val used = map (fn ((f,a),thm) => FundefCtxTree.export_thm thy (f, map prop_of a) thm) (u @ sub)
|
|
720 |
|
|
721 |
val hyp = Trueprop (R' $ arg $ lhs)
|
|
722 |
|> fold_rev (curry Logic.mk_implies o prop_of) used
|
|
723 |
|> FundefCtxTree.export_term (fixes, map prop_of assumes)
|
|
724 |
|> fold_rev (curry Logic.mk_implies o prop_of) ags
|
|
725 |
|> fold_rev mk_forall_rename (map fst oqs ~~ qs)
|
|
726 |
|> cterm_of thy
|
|
727 |
|
|
728 |
val thm = assume hyp
|
|
729 |
|> fold forall_elim cqs
|
|
730 |
|> fold implies_elim_swp ags
|
|
731 |
|> FundefCtxTree.import_thm thy (fixes, assumes) (* "(arg, lhs) : R'" *)
|
|
732 |
|> fold implies_elim_swp used
|
|
733 |
|
|
734 |
val acc = thm COMP ih_case
|
|
735 |
|
|
736 |
val z_eq_arg = cterm_of thy (Trueprop (HOLogic.mk_eq (z, arg)))
|
|
737 |
|
|
738 |
val arg_eq_z = (assume z_eq_arg) RS sym
|
|
739 |
|
|
740 |
val z_acc = simplify (HOL_basic_ss addsimps [arg_eq_z]) acc (* fragile, slow... *)
|
|
741 |
|> implies_intr (cprop_of case_hyp)
|
|
742 |
|> implies_intr z_eq_arg
|
|
743 |
|
|
744 |
val z_eq_arg = assume (cterm_of thy (Trueprop (mk_eq (z, arg))))
|
|
745 |
val x_eq_lhs = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
|
|
746 |
|
|
747 |
val ethm = (z_acc OF [z_eq_arg, x_eq_lhs])
|
|
748 |
|> FundefCtxTree.export_thm thy (fixes,
|
|
749 |
prop_of z_eq_arg :: prop_of x_eq_lhs :: map prop_of (ags @ assumes))
|
|
750 |
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
|
|
751 |
|
|
752 |
val sub' = sub @ [(([],[]), acc)]
|
|
753 |
in
|
|
754 |
(sub', (hyp :: hyps, ethm :: thms))
|
|
755 |
end
|
|
756 |
| step _ _ _ _ = raise Match
|
|
757 |
in
|
|
758 |
FundefCtxTree.traverse_tree step tree
|
|
759 |
end
|
|
760 |
|
|
761 |
|
|
762 |
fun mk_nest_term_rule thy globals R R_cases clauses =
|
|
763 |
let
|
|
764 |
val Globals { domT, x, z, ... } = globals
|
|
765 |
val acc_R = mk_acc domT R
|
|
766 |
|
|
767 |
val R' = Free ("R", fastype_of R)
|
|
768 |
|
|
769 |
val Rrel = Free ("R", mk_relT (domT, domT))
|
|
770 |
val inrel_R = Const ("FunDef.in_rel", mk_relT (domT, domT) --> fastype_of R) $ Rrel
|
|
771 |
|
|
772 |
val wfR' = cterm_of thy (Trueprop (Const ("FunDef.wfP", (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
|
|
773 |
|
|
774 |
(* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
|
|
775 |
val ihyp = all domT $ Abs ("z", domT,
|
|
776 |
implies $ Trueprop (R' $ Bound 0 $ x)
|
|
777 |
$ Trueprop (acc_R $ Bound 0))
|
|
778 |
|> cterm_of thy
|
|
779 |
|
|
780 |
val ihyp_a = assume ihyp |> forall_elim_vars 0
|
|
781 |
|
|
782 |
val R_z_x = cterm_of thy (Trueprop (R $ z $ x))
|
|
783 |
|
|
784 |
val (hyps,cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([],[])
|
|
785 |
in
|
|
786 |
R_cases
|
|
787 |
|> forall_elim (cterm_of thy z)
|
|
788 |
|> forall_elim (cterm_of thy x)
|
|
789 |
|> forall_elim (cterm_of thy (acc_R $ z))
|
|
790 |
|> curry op COMP (assume R_z_x)
|
|
791 |
|> fold_rev (curry op COMP) cases
|
|
792 |
|> implies_intr R_z_x
|
|
793 |
|> forall_intr (cterm_of thy z)
|
|
794 |
|> (fn it => it COMP accI)
|
|
795 |
|> implies_intr ihyp
|
|
796 |
|> forall_intr (cterm_of thy x)
|
|
797 |
|> (fn it => Drule.compose_single(it,2,wf_induct_rule))
|
|
798 |
|> curry op RS (assume wfR')
|
|
799 |
|> fold implies_intr hyps
|
|
800 |
|> implies_intr wfR'
|
|
801 |
|> forall_intr (cterm_of thy R')
|
|
802 |
|> forall_elim (cterm_of thy (inrel_R))
|
|
803 |
|> curry op RS wf_in_rel
|
|
804 |
|> full_simplify (HOL_basic_ss addsimps [in_rel_def])
|
|
805 |
|> forall_intr (cterm_of thy Rrel)
|
|
806 |
end
|
|
807 |
|
|
808 |
|
|
809 |
|
|
810 |
(* Tail recursion (probably very fragile)
|
|
811 |
*
|
|
812 |
* FIXME:
|
|
813 |
* - Need to do forall_elim_vars on psimps: Unneccesary, if psimps would be taken from the same context.
|
|
814 |
* - Must we really replace the fvar by f here?
|
|
815 |
* - Splitting is not configured automatically: Problems with case?
|
|
816 |
*)
|
|
817 |
fun mk_trsimps octxt globals f G R f_def R_cases G_induct clauses psimps =
|
|
818 |
let
|
|
819 |
val Globals {domT, ranT, fvar, ...} = globals
|
|
820 |
|
|
821 |
val R_cases = forall_elim_vars 0 R_cases (* FIXME: Should be already in standard form. *)
|
|
822 |
|
|
823 |
val graph_implies_dom = (* "G ?x ?y ==> dom ?x" *)
|
|
824 |
Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))]
|
|
825 |
(HOLogic.mk_Trueprop (mk_acc domT R $ Free ("x", domT)))
|
|
826 |
(fn {prems=[a], ...} =>
|
|
827 |
((rtac (G_induct OF [a]))
|
|
828 |
THEN_ALL_NEW (rtac accI)
|
|
829 |
THEN_ALL_NEW (etac R_cases)
|
|
830 |
THEN_ALL_NEW (SIMPSET' asm_full_simp_tac)) 1)
|
|
831 |
|
|
832 |
val default_thm = (forall_intr_vars graph_implies_dom) COMP (f_def COMP fundef_default_value)
|
|
833 |
|
|
834 |
fun mk_trsimp clause psimp =
|
|
835 |
let
|
|
836 |
val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {ctxt, cqs, qs, gs, lhs, rhs, ...}, ...} = clause
|
|
837 |
val thy = ProofContext.theory_of ctxt
|
|
838 |
val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs
|
|
839 |
|
|
840 |
val trsimp = Logic.list_implies(gs, HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *)
|
|
841 |
val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *)
|
|
842 |
in
|
|
843 |
Goal.prove ctxt [] [] trsimp
|
|
844 |
(fn _ =>
|
|
845 |
rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
|
|
846 |
THEN (rtac (forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
|
|
847 |
THEN (SIMPSET (fn ss => asm_full_simp_tac (ss addsimps [default_thm]) 1))
|
|
848 |
THEN (etac not_accP_down 1)
|
|
849 |
THEN ((etac R_cases) THEN_ALL_NEW (SIMPSET' (fn ss => asm_full_simp_tac (ss addsimps [default_thm])))) 1)
|
|
850 |
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
|
|
851 |
end
|
|
852 |
in
|
|
853 |
map2 mk_trsimp clauses psimps
|
|
854 |
end
|
|
855 |
|
|
856 |
|
|
857 |
fun prepare_fundef config defname (fname, fT, mixfix) abstract_qglrs default_str lthy =
|
|
858 |
let
|
|
859 |
val FundefConfig {domintros, tailrec, ...} = config
|
|
860 |
|
|
861 |
val fvar = Free (fname, fT)
|
|
862 |
val domT = domain_type fT
|
|
863 |
val ranT = range_type fT
|
|
864 |
|
|
865 |
val [default] = fst (Variable.importT_terms (fst (ProofContext.read_termTs lthy (K false) (K NONE) (K NONE) [] [(default_str, fT)])) lthy) (* FIXME *)
|
|
866 |
|
|
867 |
val congs = get_fundef_congs (Context.Proof lthy)
|
|
868 |
val (globals, ctxt') = fix_globals domT ranT fvar lthy
|
|
869 |
|
|
870 |
val Globals { x, h, ... } = globals
|
|
871 |
|
|
872 |
val clauses = map (mk_clause_context x ctxt') abstract_qglrs
|
|
873 |
|
|
874 |
val n = length abstract_qglrs
|
|
875 |
|
|
876 |
val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs) (* FIXME: Save in theory *)
|
|
877 |
|
|
878 |
fun build_tree (ClauseContext { ctxt, rhs, ...}) =
|
|
879 |
FundefCtxTree.mk_tree congs_deps (fname, fT) h ctxt rhs
|
|
880 |
|
|
881 |
val trees = map build_tree clauses
|
|
882 |
val RCss = map find_calls trees
|
|
883 |
|
|
884 |
val ((G, GIntro_thms, G_elim, G_induct), lthy) =
|
|
885 |
PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
|
|
886 |
|
|
887 |
val ((f, f_defthm), lthy) =
|
|
888 |
PROFILE "def_fun" (define_function (defname ^ "_sum_def") (fname, mixfix) domT ranT G default) lthy
|
|
889 |
|
|
890 |
val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
|
|
891 |
val trees = map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
|
|
892 |
|
|
893 |
val ((R, RIntro_thmss, R_elim), lthy) =
|
|
894 |
PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
|
|
895 |
|
|
896 |
val (_, lthy) =
|
|
897 |
LocalTheory.abbrev Syntax.default_mode ((defname ^ "_dom", NoSyn), mk_acc domT R) lthy
|
|
898 |
|
|
899 |
val newthy = ProofContext.theory_of lthy
|
|
900 |
val clauses = map (transfer_clause_ctx newthy) clauses
|
|
901 |
|
|
902 |
val cert = cterm_of (ProofContext.theory_of lthy)
|
|
903 |
|
|
904 |
val xclauses = PROFILE "xclauses" (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms) RIntro_thmss
|
|
905 |
|
|
906 |
val complete = mk_completeness globals clauses abstract_qglrs |> cert |> assume
|
|
907 |
val compat = mk_compat_proof_obligations domT ranT fvar f abstract_qglrs |> map (cert #> assume)
|
|
908 |
|
|
909 |
val compat_store = store_compat_thms n compat
|
|
910 |
|
|
911 |
val (goalstate, values) = PROFILE "prove_stuff" (prove_stuff newthy congs globals G f R xclauses complete compat compat_store G_elim) f_defthm
|
|
912 |
|
|
913 |
val mk_trsimps = mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses
|
|
914 |
|
|
915 |
fun mk_partial_rules provedgoal =
|
|
916 |
let
|
|
917 |
val newthy = theory_of_thm provedgoal (*FIXME*)
|
|
918 |
|
|
919 |
val (graph_is_function, complete_thm) =
|
|
920 |
provedgoal
|
|
921 |
|> Conjunction.elim
|
|
922 |
|> apfst (forall_elim_vars 0)
|
|
923 |
|
|
924 |
val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
|
|
925 |
|
|
926 |
val psimps = PROFILE "Proving simplification rules" (mk_psimps newthy globals R xclauses values f_iff) graph_is_function
|
|
927 |
|
|
928 |
val (subset_pinduct, simple_pinduct) = PROFILE "Proving partial induction rule"
|
|
929 |
(mk_partial_induct_rule newthy globals R complete_thm) xclauses
|
|
930 |
|
|
931 |
|
|
932 |
val total_intro = PROFILE "Proving nested termination rule" (mk_nest_term_rule newthy globals R R_elim) xclauses
|
|
933 |
|
|
934 |
val dom_intros = if domintros
|
|
935 |
then SOME (PROFILE "Proving domain introduction rules" (map (mk_domain_intro newthy globals R R_elim)) xclauses)
|
|
936 |
else NONE
|
|
937 |
val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE
|
|
938 |
|
|
939 |
in
|
|
940 |
FundefResult {f=f, G=G, R=R, cases=complete_thm,
|
|
941 |
psimps=psimps, subset_pinducts=[subset_pinduct], simple_pinducts=[simple_pinduct],
|
|
942 |
termination=total_intro, trsimps=trsimps,
|
|
943 |
domintros=dom_intros}
|
|
944 |
end
|
|
945 |
in
|
|
946 |
((f, goalstate, mk_partial_rules), lthy)
|
|
947 |
end
|
|
948 |
|
|
949 |
|
|
950 |
|
|
951 |
|
|
952 |
end
|