|
1 theory LamTest |
|
2 imports "../Nominal2" |
|
3 begin |
|
4 |
|
5 atom_decl name |
|
6 |
|
7 nominal_datatype lam = |
|
8 Var "name" |
|
9 | App "lam" "lam" |
|
10 | Lam x::"name" l::"lam" bind x in l |
|
11 |
|
12 definition |
|
13 "eqvt x \<equiv> \<forall>p. p \<bullet> x = x" |
|
14 |
|
15 |
|
16 ML {* |
|
17 |
|
18 |
|
19 val trace = Unsynchronized.ref false |
|
20 fun trace_msg msg = if ! trace then tracing (msg ()) else () |
|
21 |
|
22 val boolT = HOLogic.boolT |
|
23 val mk_eq = HOLogic.mk_eq |
|
24 |
|
25 open Function_Lib |
|
26 open Function_Common |
|
27 |
|
28 datatype globals = Globals of |
|
29 {fvar: term, |
|
30 domT: typ, |
|
31 ranT: typ, |
|
32 h: term, |
|
33 y: term, |
|
34 x: term, |
|
35 z: term, |
|
36 a: term, |
|
37 P: term, |
|
38 D: term, |
|
39 Pbool:term} |
|
40 |
|
41 datatype rec_call_info = RCInfo of |
|
42 {RIvs: (string * typ) list, (* Call context: fixes and assumes *) |
|
43 CCas: thm list, |
|
44 rcarg: term, (* The recursive argument *) |
|
45 llRI: thm, |
|
46 h_assum: term} |
|
47 |
|
48 |
|
49 datatype clause_context = ClauseContext of |
|
50 {ctxt : Proof.context, |
|
51 qs : term list, |
|
52 gs : term list, |
|
53 lhs: term, |
|
54 rhs: term, |
|
55 cqs: cterm list, |
|
56 ags: thm list, |
|
57 case_hyp : thm} |
|
58 |
|
59 |
|
60 fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) = |
|
61 ClauseContext { ctxt = ProofContext.transfer thy ctxt, |
|
62 qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp } |
|
63 |
|
64 |
|
65 datatype clause_info = ClauseInfo of |
|
66 {no: int, |
|
67 qglr : ((string * typ) list * term list * term * term), |
|
68 cdata : clause_context, |
|
69 tree: Function_Ctx_Tree.ctx_tree, |
|
70 lGI: thm, |
|
71 RCs: rec_call_info list} |
|
72 |
|
73 |
|
74 (* Theory dependencies. *) |
|
75 val acc_induct_rule = @{thm accp_induct_rule} |
|
76 |
|
77 val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence} |
|
78 val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness} |
|
79 val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff} |
|
80 |
|
81 val acc_downward = @{thm accp_downward} |
|
82 val accI = @{thm accp.accI} |
|
83 val case_split = @{thm HOL.case_split} |
|
84 val fundef_default_value = @{thm FunDef.fundef_default_value} |
|
85 val not_acc_down = @{thm not_accp_down} |
|
86 |
|
87 |
|
88 |
|
89 fun find_calls tree = |
|
90 let |
|
91 fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = |
|
92 ([], (fixes, assumes, arg) :: xs) |
|
93 | add_Ri _ _ _ _ = raise Match |
|
94 in |
|
95 rev (Function_Ctx_Tree.traverse_tree add_Ri tree []) |
|
96 end |
|
97 *} |
|
98 |
|
99 |
|
100 ML {* |
|
101 (** building proof obligations *) |
|
102 |
|
103 fun mk_compat_proof_obligations domT ranT fvar f glrs = |
|
104 let |
|
105 val _ = tracing ("domT: " ^ @{make_string} domT) |
|
106 val _ = tracing ("ranT: " ^ @{make_string} ranT) |
|
107 val _ = tracing ("fvar: " ^ @{make_string} fvar) |
|
108 val _ = tracing ("f: " ^ @{make_string} f) |
|
109 fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) = |
|
110 let |
|
111 val shift = incr_boundvars (length qs') |
|
112 in |
|
113 Logic.mk_implies |
|
114 (HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'), |
|
115 HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs')) |
|
116 |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs') |
|
117 |> (curry Logic.mk_implies) @{term "Trueprop True"} |
|
118 |> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs') |
|
119 |> curry abstract_over fvar |
|
120 |> curry subst_bound f |
|
121 end |
|
122 in |
|
123 map mk_impl (unordered_pairs glrs) |
|
124 |> tap (fn ts => tracing ("compat_trms:\n" ^ cat_lines (map (Syntax.string_of_term @{context}) ts))) |
|
125 end |
|
126 *} |
|
127 |
|
128 ML {* |
|
129 fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs = |
|
130 let |
|
131 fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) = |
|
132 HOLogic.mk_Trueprop Pbool |
|
133 |> curry Logic.mk_implies (HOLogic.mk_Trueprop (mk_eq (x, lhs))) |
|
134 |> fold_rev (curry Logic.mk_implies) gs |
|
135 |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |
|
136 in |
|
137 HOLogic.mk_Trueprop Pbool |
|
138 |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs) |
|
139 |> mk_forall_rename ("x", x) |
|
140 |> mk_forall_rename ("P", Pbool) |
|
141 end |
|
142 |
|
143 (** making a context with it's own local bindings **) |
|
144 |
|
145 fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) = |
|
146 let |
|
147 val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt |
|
148 |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs |
|
149 |
|
150 val thy = ProofContext.theory_of ctxt' |
|
151 |
|
152 fun inst t = subst_bounds (rev qs, t) |
|
153 val gs = map inst pre_gs |
|
154 val lhs = inst pre_lhs |
|
155 val rhs = inst pre_rhs |
|
156 |
|
157 val cqs = map (cterm_of thy) qs |
|
158 val ags = map (Thm.assume o cterm_of thy) gs |
|
159 |
|
160 val case_hyp = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs)))) |
|
161 in |
|
162 ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs, |
|
163 cqs = cqs, ags = ags, case_hyp = case_hyp } |
|
164 end |
|
165 |
|
166 |
|
167 (* lowlevel term function. FIXME: remove *) |
|
168 fun abstract_over_list vs body = |
|
169 let |
|
170 fun abs lev v tm = |
|
171 if v aconv tm then Bound lev |
|
172 else |
|
173 (case tm of |
|
174 Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t) |
|
175 | t $ u => abs lev v t $ abs lev v u |
|
176 | t => t) |
|
177 in |
|
178 fold_index (fn (i, v) => fn t => abs i v t) vs body |
|
179 end |
|
180 |
|
181 |
|
182 |
|
183 fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms = |
|
184 let |
|
185 val Globals {h, ...} = globals |
|
186 |
|
187 val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata |
|
188 val cert = Thm.cterm_of (ProofContext.theory_of ctxt) |
|
189 |
|
190 (* Instantiate the GIntro thm with "f" and import into the clause context. *) |
|
191 val lGI = GIntro_thm |
|
192 |> Thm.forall_elim (cert f) |
|
193 |> fold Thm.forall_elim cqs |
|
194 |> fold Thm.elim_implies ags |
|
195 |
|
196 fun mk_call_info (rcfix, rcassm, rcarg) RI = |
|
197 let |
|
198 val llRI = RI |
|
199 |> fold Thm.forall_elim cqs |
|
200 |> fold (Thm.forall_elim o cert o Free) rcfix |
|
201 |> fold Thm.elim_implies ags |
|
202 |> fold Thm.elim_implies rcassm |
|
203 |
|
204 val h_assum = |
|
205 HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg)) |
|
206 |> fold_rev (curry Logic.mk_implies o prop_of) rcassm |
|
207 |> fold_rev (Logic.all o Free) rcfix |
|
208 |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] [] |
|
209 |> abstract_over_list (rev qs) |
|
210 in |
|
211 RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum} |
|
212 end |
|
213 |
|
214 val RC_infos = map2 mk_call_info RCs RIntro_thms |
|
215 in |
|
216 ClauseInfo {no=no, cdata=cdata, qglr=qglr, lGI=lGI, RCs=RC_infos, |
|
217 tree=tree} |
|
218 end |
|
219 *} |
|
220 |
|
221 ML {* |
|
222 fun store_compat_thms 0 thms = [] |
|
223 | store_compat_thms n thms = |
|
224 let |
|
225 val (thms1, thms2) = chop n thms |
|
226 in |
|
227 (thms1 :: store_compat_thms (n - 1) thms2) |
|
228 end |
|
229 *} |
|
230 |
|
231 |
|
232 ML {* |
|
233 (* expects i <= j *) |
|
234 fun lookup_compat_thm i j cts = |
|
235 nth (nth cts (i - 1)) (j - i) |
|
236 |
|
237 (* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *) |
|
238 (* if j < i, then turn around *) |
|
239 fun get_compat_thm thy cts i j ctxi ctxj = |
|
240 let |
|
241 val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi |
|
242 val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj |
|
243 |
|
244 val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj))) |
|
245 in if j < i then |
|
246 let |
|
247 val _ = tracing "then" |
|
248 val compat = lookup_compat_thm j i cts |
|
249 in |
|
250 compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |
|
251 |> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |
|
252 |> Thm.elim_implies @{thm TrueI} |
|
253 |> fold Thm.elim_implies agsj |
|
254 |> fold Thm.elim_implies agsi |
|
255 |> Thm.elim_implies ((Thm.assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *) |
|
256 end |
|
257 else |
|
258 let |
|
259 val _ = tracing "else" |
|
260 val compat = lookup_compat_thm i j cts |
|
261 |
|
262 fun pp s (th:thm) = tracing (s ^ " compat thm: " ^ @{make_string} th) |
|
263 in |
|
264 compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |
|
265 |> (tap (fn th => pp "*0" th)) |
|
266 |> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |
|
267 |> (tap (fn th => pp "*1" th)) |
|
268 |> Thm.elim_implies @{thm TrueI} |
|
269 |> fold Thm.elim_implies agsi |
|
270 |> (tap (fn th => pp "*2" th)) |
|
271 |> fold Thm.elim_implies agsj |
|
272 |> (tap (fn th => pp "*3" th)) |
|
273 |> Thm.elim_implies (Thm.assume lhsi_eq_lhsj) |
|
274 |> (tap (fn th => pp "*4" th)) |
|
275 |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *) |
|
276 end |
|
277 end |
|
278 *} |
|
279 |
|
280 (* WASS *) |
|
281 |
|
282 ML {* |
|
283 (* Generates the replacement lemma in fully quantified form. *) |
|
284 fun mk_replacement_lemma thy h ih_elim clause = |
|
285 let |
|
286 val ClauseInfo {cdata=ClauseContext {qs, lhs, cqs, ags, case_hyp, ...}, |
|
287 RCs, tree, ...} = clause |
|
288 local open Conv in |
|
289 val ih_conv = arg1_conv o arg_conv o arg_conv |
|
290 end |
|
291 |
|
292 val ih_elim_case = |
|
293 Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_elim |
|
294 |
|
295 val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs |
|
296 val h_assums = map (fn RCInfo {h_assum, ...} => |
|
297 Thm.assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs |
|
298 |
|
299 val (eql, _) = |
|
300 Function_Ctx_Tree.rewrite_by_tree thy h ih_elim_case (Ris ~~ h_assums) tree |
|
301 |
|
302 val replace_lemma = (eql RS meta_eq_to_obj_eq) |
|
303 |> Thm.implies_intr (cprop_of case_hyp) |
|
304 |> fold_rev (Thm.implies_intr o cprop_of) h_assums |
|
305 |> fold_rev (Thm.implies_intr o cprop_of) ags |
|
306 |> fold_rev Thm.forall_intr cqs |
|
307 |> Thm.close_derivation |
|
308 in |
|
309 replace_lemma |
|
310 end |
|
311 *} |
|
312 |
|
313 ML {* |
|
314 fun mk_uniqueness_clause thy globals compat_store clausei clausej RLj = |
|
315 let |
|
316 val Globals {h, y, x, fvar, ...} = globals |
|
317 val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei |
|
318 val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej |
|
319 |
|
320 val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...} = |
|
321 mk_clause_context x ctxti cdescj |
|
322 |
|
323 val _ = tracing "1" |
|
324 |
|
325 val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj' |
|
326 |
|
327 val _ = tracing "1A" |
|
328 |
|
329 val compat = get_compat_thm thy compat_store i j cctxi cctxj |
|
330 |
|
331 val _ = tracing "1B" |
|
332 |
|
333 val Ghsj' = map |
|
334 (fn RCInfo {h_assum, ...} => Thm.assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj |
|
335 |
|
336 val _ = tracing "2" |
|
337 |
|
338 val RLj_import = RLj |
|
339 |> fold Thm.forall_elim cqsj' |
|
340 |> fold Thm.elim_implies agsj' |
|
341 |> fold Thm.elim_implies Ghsj' |
|
342 |
|
343 val _ = tracing "3" |
|
344 |
|
345 val y_eq_rhsj'h = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h)))) |
|
346 val lhsi_eq_lhsj' = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj')))) |
|
347 (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *) |
|
348 |
|
349 val _ = tracing "4" |
|
350 in |
|
351 (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *) |
|
352 |> Thm.implies_elim RLj_import |
|
353 (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *) |
|
354 |> (fn it => trans OF [it, compat]) |
|
355 (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *) |
|
356 |> (fn it => trans OF [y_eq_rhsj'h, it]) |
|
357 (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *) |
|
358 |> fold_rev (Thm.implies_intr o cprop_of) Ghsj' |
|
359 |> fold_rev (Thm.implies_intr o cprop_of) agsj' |
|
360 (* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *) |
|
361 |> Thm.implies_intr (cprop_of y_eq_rhsj'h) |
|
362 |> Thm.implies_intr (cprop_of lhsi_eq_lhsj') |
|
363 |> fold_rev Thm.forall_intr (cterm_of thy h :: cqsj') |
|
364 end |
|
365 *} |
|
366 |
|
367 (* HERE *) |
|
368 |
|
369 ML {* |
|
370 fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei = |
|
371 let |
|
372 val Globals {x, y, ranT, fvar, ...} = globals |
|
373 val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei |
|
374 val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs |
|
375 |
|
376 val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro |
|
377 |
|
378 val _ = tracing "A" |
|
379 |
|
380 fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case) |
|
381 |> fold_rev (Thm.implies_intr o cprop_of) CCas |
|
382 |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs |
|
383 |
|
384 val existence = fold (curry op COMP o prep_RC) RCs lGI |
|
385 |
|
386 val _ = tracing "B" |
|
387 |
|
388 val P = cterm_of thy (mk_eq (y, rhsC)) |
|
389 val G_lhs_y = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y))) |
|
390 |
|
391 val _ = tracing "B2" |
|
392 |
|
393 val unique_clauses = |
|
394 map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas |
|
395 |
|
396 val _ = tracing "C" |
|
397 |
|
398 fun elim_implies_eta A AB = |
|
399 Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single |
|
400 |
|
401 val _ = tracing "D" |
|
402 |
|
403 val uniqueness = G_cases |
|
404 |> Thm.forall_elim (cterm_of thy lhs) |
|
405 |> Thm.forall_elim (cterm_of thy y) |
|
406 |> Thm.forall_elim P |
|
407 |> Thm.elim_implies G_lhs_y |
|
408 |> fold elim_implies_eta unique_clauses |
|
409 |> Thm.implies_intr (cprop_of G_lhs_y) |
|
410 |> Thm.forall_intr (cterm_of thy y) |
|
411 |
|
412 val _ = tracing "E" |
|
413 |
|
414 val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *) |
|
415 |
|
416 val exactly_one = |
|
417 ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)] |
|
418 |> curry (op COMP) existence |
|
419 |> curry (op COMP) uniqueness |
|
420 |> simplify (HOL_basic_ss addsimps [case_hyp RS sym]) |
|
421 |> Thm.implies_intr (cprop_of case_hyp) |
|
422 |> fold_rev (Thm.implies_intr o cprop_of) ags |
|
423 |> fold_rev Thm.forall_intr cqs |
|
424 |
|
425 val _ = tracing "F" |
|
426 |
|
427 val function_value = |
|
428 existence |
|
429 |> Thm.implies_intr ihyp |
|
430 |> Thm.implies_intr (cprop_of case_hyp) |
|
431 |> Thm.forall_intr (cterm_of thy x) |
|
432 |> Thm.forall_elim (cterm_of thy lhs) |
|
433 |> curry (op RS) refl |
|
434 |
|
435 val _ = tracing "G" |
|
436 in |
|
437 (exactly_one, function_value) |
|
438 end |
|
439 *} |
|
440 |
|
441 ML {* |
|
442 fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim f_def = |
|
443 let |
|
444 val Globals {h, domT, ranT, x, ...} = globals |
|
445 val thy = ProofContext.theory_of ctxt |
|
446 |
|
447 (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *) |
|
448 val ihyp = Term.all domT $ Abs ("z", domT, |
|
449 Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), |
|
450 HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $ |
|
451 Abs ("y", ranT, G $ Bound 1 $ Bound 0)))) |
|
452 |> cterm_of thy |
|
453 |
|
454 val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0 |
|
455 val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex) |
|
456 val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un) |
|
457 |> instantiate' [] [NONE, SOME (cterm_of thy h)] |
|
458 |
|
459 val _ = trace_msg (K "Proving Replacement lemmas...") |
|
460 val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses |
|
461 |
|
462 val _ = trace_msg (K "Proving cases for unique existence...") |
|
463 val (ex1s, values) = |
|
464 split_list (map (mk_uniqueness_case thy globals G f |
|
465 ihyp ih_intro G_elim compat_store clauses repLemmas) clauses) |
|
466 |
|
467 val _ = trace_msg (K "Proving: Graph is a function") |
|
468 val graph_is_function = complete |
|
469 |> Thm.forall_elim_vars 0 |
|
470 |> fold (curry op COMP) ex1s |
|
471 |> Thm.implies_intr (ihyp) |
|
472 |> Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x))) |
|
473 |> Thm.forall_intr (cterm_of thy x) |
|
474 |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *) |
|
475 |> (fn it => fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it) |
|
476 |
|
477 val goalstate = Conjunction.intr graph_is_function complete |
|
478 |> Thm.close_derivation |
|
479 |> Goal.protect |
|
480 |> fold_rev (Thm.implies_intr o cprop_of) compat |
|
481 |> Thm.implies_intr (cprop_of complete) |
|
482 in |
|
483 (goalstate, values) |
|
484 end |
|
485 |
|
486 (* wrapper -- restores quantifiers in rule specifications *) |
|
487 fun inductive_def (binding as ((R, T), _)) intrs lthy = |
|
488 let |
|
489 val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) = |
|
490 lthy |
|
491 |> Local_Theory.conceal |
|
492 |> Inductive.add_inductive_i |
|
493 {quiet_mode = true, |
|
494 verbose = ! trace, |
|
495 alt_name = Binding.empty, |
|
496 coind = false, |
|
497 no_elim = false, |
|
498 no_ind = false, |
|
499 skip_mono = true, |
|
500 fork_mono = false} |
|
501 [binding] (* relation *) |
|
502 [] (* no parameters *) |
|
503 (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *) |
|
504 [] (* no special monos *) |
|
505 ||> Local_Theory.restore_naming lthy |
|
506 |
|
507 val cert = cterm_of (ProofContext.theory_of lthy) |
|
508 fun requantify orig_intro thm = |
|
509 let |
|
510 val (qs, t) = dest_all_all orig_intro |
|
511 val frees = frees_in_term lthy t |> remove (op =) (Binding.name_of R, T) |
|
512 val vars = Term.add_vars (prop_of thm) [] |> rev |
|
513 val varmap = AList.lookup (op =) (frees ~~ map fst vars) |
|
514 #> the_default ("",0) |
|
515 in |
|
516 fold_rev (fn Free (n, T) => |
|
517 forall_intr_rename (n, cert (Var (varmap (n, T), T)))) qs thm |
|
518 end |
|
519 in |
|
520 ((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct), lthy) |
|
521 end |
|
522 *} |
|
523 |
|
524 ML {* |
|
525 fun define_graph Gname fvar domT ranT clauses RCss lthy = |
|
526 let |
|
527 val GT = domT --> ranT --> boolT |
|
528 val (Gvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Gname, GT) |
|
529 |
|
530 fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs = |
|
531 let |
|
532 fun mk_h_assm (rcfix, rcassm, rcarg) = |
|
533 HOLogic.mk_Trueprop (Free Gvar $ rcarg $ (fvar $ rcarg)) |
|
534 |> fold_rev (curry Logic.mk_implies o prop_of) rcassm |
|
535 |> fold_rev (Logic.all o Free) rcfix |
|
536 in |
|
537 HOLogic.mk_Trueprop (Free Gvar $ lhs $ rhs) |
|
538 |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs |
|
539 |> fold_rev (curry Logic.mk_implies) gs |
|
540 |> fold_rev Logic.all (fvar :: qs) |
|
541 end |
|
542 |
|
543 val G_intros = map2 mk_GIntro clauses RCss |
|
544 in |
|
545 inductive_def ((Binding.name n, T), NoSyn) G_intros lthy |
|
546 end |
|
547 *} |
|
548 |
|
549 ML {* |
|
550 fun define_function fdefname (fname, mixfix) domT ranT G default lthy = |
|
551 let |
|
552 val f_def = |
|
553 Abs ("x", domT, Const (@{const_name FunDef.THE_default}, ranT --> (ranT --> boolT) --> ranT) |
|
554 $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0)) |
|
555 |> Syntax.check_term lthy |
|
556 in |
|
557 Local_Theory.define |
|
558 ((Binding.name (function_name fname), mixfix), |
|
559 ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy |
|
560 end |
|
561 |
|
562 fun define_recursion_relation Rname domT qglrs clauses RCss lthy = |
|
563 let |
|
564 val RT = domT --> domT --> boolT |
|
565 val (Rvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Rname, RT) |
|
566 |
|
567 fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) = |
|
568 HOLogic.mk_Trueprop (Free Rvar $ rcarg $ lhs) |
|
569 |> fold_rev (curry Logic.mk_implies o prop_of) rcassm |
|
570 |> fold_rev (curry Logic.mk_implies) gs |
|
571 |> fold_rev (Logic.all o Free) rcfix |
|
572 |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |
|
573 (* "!!qs xs. CS ==> G => (r, lhs) : R" *) |
|
574 |
|
575 val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss |
|
576 |
|
577 val ((R, RIntro_thms, R_elim, _), lthy) = |
|
578 inductive_def ((Binding.name n, T), NoSyn) (flat R_intross) lthy |
|
579 in |
|
580 ((R, Library.unflat R_intross RIntro_thms, R_elim), lthy) |
|
581 end |
|
582 |
|
583 |
|
584 fun fix_globals domT ranT fvar ctxt = |
|
585 let |
|
586 val ([h, y, x, z, a, D, P, Pbool],ctxt') = Variable.variant_fixes |
|
587 ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt |
|
588 in |
|
589 (Globals {h = Free (h, domT --> ranT), |
|
590 y = Free (y, ranT), |
|
591 x = Free (x, domT), |
|
592 z = Free (z, domT), |
|
593 a = Free (a, domT), |
|
594 D = Free (D, domT --> boolT), |
|
595 P = Free (P, domT --> boolT), |
|
596 Pbool = Free (Pbool, boolT), |
|
597 fvar = fvar, |
|
598 domT = domT, |
|
599 ranT = ranT}, |
|
600 ctxt') |
|
601 end |
|
602 |
|
603 fun inst_RC thy fvar f (rcfix, rcassm, rcarg) = |
|
604 let |
|
605 fun inst_term t = subst_bound(f, abstract_over (fvar, t)) |
|
606 in |
|
607 (rcfix, map (Thm.assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg) |
|
608 end |
|
609 |
|
610 |
|
611 |
|
612 (********************************************************** |
|
613 * PROVING THE RULES |
|
614 **********************************************************) |
|
615 |
|
616 fun mk_psimps thy globals R clauses valthms f_iff graph_is_function = |
|
617 let |
|
618 val Globals {domT, z, ...} = globals |
|
619 |
|
620 fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm = |
|
621 let |
|
622 val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *) |
|
623 val z_smaller = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *) |
|
624 in |
|
625 ((Thm.assume z_smaller) RS ((Thm.assume lhs_acc) RS acc_downward)) |
|
626 |> (fn it => it COMP graph_is_function) |
|
627 |> Thm.implies_intr z_smaller |
|
628 |> Thm.forall_intr (cterm_of thy z) |
|
629 |> (fn it => it COMP valthm) |
|
630 |> Thm.implies_intr lhs_acc |
|
631 |> asm_simplify (HOL_basic_ss addsimps [f_iff]) |
|
632 |> fold_rev (Thm.implies_intr o cprop_of) ags |
|
633 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
|
634 end |
|
635 in |
|
636 map2 mk_psimp clauses valthms |
|
637 end |
|
638 |
|
639 |
|
640 (** Induction rule **) |
|
641 |
|
642 |
|
643 val acc_subset_induct = @{thm predicate1I} RS @{thm accp_subset_induct} |
|
644 |
|
645 |
|
646 fun mk_partial_induct_rule thy globals R complete_thm clauses = |
|
647 let |
|
648 val Globals {domT, x, z, a, P, D, ...} = globals |
|
649 val acc_R = mk_acc domT R |
|
650 |
|
651 val x_D = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x))) |
|
652 val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a)) |
|
653 |
|
654 val D_subset = cterm_of thy (Logic.all x |
|
655 (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x)))) |
|
656 |
|
657 val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *) |
|
658 Logic.all x (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), |
|
659 Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x), |
|
660 HOLogic.mk_Trueprop (D $ z))))) |
|
661 |> cterm_of thy |
|
662 |
|
663 (* Inductive Hypothesis: !!z. (z,x):R ==> P z *) |
|
664 val ihyp = Term.all domT $ Abs ("z", domT, |
|
665 Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), |
|
666 HOLogic.mk_Trueprop (P $ Bound 0))) |
|
667 |> cterm_of thy |
|
668 |
|
669 val aihyp = Thm.assume ihyp |
|
670 |
|
671 fun prove_case clause = |
|
672 let |
|
673 val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...}, |
|
674 RCs, qglr = (oqs, _, _, _), ...} = clause |
|
675 |
|
676 val case_hyp_conv = K (case_hyp RS eq_reflection) |
|
677 local open Conv in |
|
678 val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D |
|
679 val sih = |
|
680 fconv_rule (Conv.binder_conv |
|
681 (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp |
|
682 end |
|
683 |
|
684 fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih |
|
685 |> Thm.forall_elim (cterm_of thy rcarg) |
|
686 |> Thm.elim_implies llRI |
|
687 |> fold_rev (Thm.implies_intr o cprop_of) CCas |
|
688 |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs |
|
689 |
|
690 val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *) |
|
691 |
|
692 val step = HOLogic.mk_Trueprop (P $ lhs) |
|
693 |> fold_rev (curry Logic.mk_implies o prop_of) P_recs |
|
694 |> fold_rev (curry Logic.mk_implies) gs |
|
695 |> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs)) |
|
696 |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |
|
697 |> cterm_of thy |
|
698 |
|
699 val P_lhs = Thm.assume step |
|
700 |> fold Thm.forall_elim cqs |
|
701 |> Thm.elim_implies lhs_D |
|
702 |> fold Thm.elim_implies ags |
|
703 |> fold Thm.elim_implies P_recs |
|
704 |
|
705 val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x)) |
|
706 |> Conv.arg_conv (Conv.arg_conv case_hyp_conv) |
|
707 |> Thm.symmetric (* P lhs == P x *) |
|
708 |> (fn eql => Thm.equal_elim eql P_lhs) (* "P x" *) |
|
709 |> Thm.implies_intr (cprop_of case_hyp) |
|
710 |> fold_rev (Thm.implies_intr o cprop_of) ags |
|
711 |> fold_rev Thm.forall_intr cqs |
|
712 in |
|
713 (res, step) |
|
714 end |
|
715 |
|
716 val (cases, steps) = split_list (map prove_case clauses) |
|
717 |
|
718 val istep = complete_thm |
|
719 |> Thm.forall_elim_vars 0 |
|
720 |> fold (curry op COMP) cases (* P x *) |
|
721 |> Thm.implies_intr ihyp |
|
722 |> Thm.implies_intr (cprop_of x_D) |
|
723 |> Thm.forall_intr (cterm_of thy x) |
|
724 |
|
725 val subset_induct_rule = |
|
726 acc_subset_induct |
|
727 |> (curry op COMP) (Thm.assume D_subset) |
|
728 |> (curry op COMP) (Thm.assume D_dcl) |
|
729 |> (curry op COMP) (Thm.assume a_D) |
|
730 |> (curry op COMP) istep |
|
731 |> fold_rev Thm.implies_intr steps |
|
732 |> Thm.implies_intr a_D |
|
733 |> Thm.implies_intr D_dcl |
|
734 |> Thm.implies_intr D_subset |
|
735 |
|
736 val simple_induct_rule = |
|
737 subset_induct_rule |
|
738 |> Thm.forall_intr (cterm_of thy D) |
|
739 |> Thm.forall_elim (cterm_of thy acc_R) |
|
740 |> assume_tac 1 |> Seq.hd |
|
741 |> (curry op COMP) (acc_downward |
|
742 |> (instantiate' [SOME (ctyp_of thy domT)] |
|
743 (map (SOME o cterm_of thy) [R, x, z])) |
|
744 |> Thm.forall_intr (cterm_of thy z) |
|
745 |> Thm.forall_intr (cterm_of thy x)) |
|
746 |> Thm.forall_intr (cterm_of thy a) |
|
747 |> Thm.forall_intr (cterm_of thy P) |
|
748 in |
|
749 simple_induct_rule |
|
750 end |
|
751 |
|
752 |
|
753 (* FIXME: broken by design *) |
|
754 fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause = |
|
755 let |
|
756 val thy = ProofContext.theory_of ctxt |
|
757 val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...}, |
|
758 qglr = (oqs, _, _, _), ...} = clause |
|
759 val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs) |
|
760 |> fold_rev (curry Logic.mk_implies) gs |
|
761 |> cterm_of thy |
|
762 in |
|
763 Goal.init goal |
|
764 |> (SINGLE (resolve_tac [accI] 1)) |> the |
|
765 |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1)) |> the |
|
766 |> (SINGLE (auto_tac (clasimpset_of ctxt))) |> the |
|
767 |> Goal.conclude |
|
768 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
|
769 end |
|
770 |
|
771 |
|
772 |
|
773 (** Termination rule **) |
|
774 |
|
775 val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule} |
|
776 val wf_in_rel = @{thm FunDef.wf_in_rel} |
|
777 val in_rel_def = @{thm FunDef.in_rel_def} |
|
778 |
|
779 fun mk_nest_term_case thy globals R' ihyp clause = |
|
780 let |
|
781 val Globals {z, ...} = globals |
|
782 val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree, |
|
783 qglr=(oqs, _, _, _), ...} = clause |
|
784 |
|
785 val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp |
|
786 |
|
787 fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = |
|
788 let |
|
789 val used = (u @ sub) |
|
790 |> map (fn (ctx,thm) => Function_Ctx_Tree.export_thm thy ctx thm) |
|
791 |
|
792 val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs) |
|
793 |> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *) |
|
794 |> Function_Ctx_Tree.export_term (fixes, assumes) |
|
795 |> fold_rev (curry Logic.mk_implies o prop_of) ags |
|
796 |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |
|
797 |> cterm_of thy |
|
798 |
|
799 val thm = Thm.assume hyp |
|
800 |> fold Thm.forall_elim cqs |
|
801 |> fold Thm.elim_implies ags |
|
802 |> Function_Ctx_Tree.import_thm thy (fixes, assumes) |
|
803 |> fold Thm.elim_implies used (* "(arg, lhs) : R'" *) |
|
804 |
|
805 val z_eq_arg = HOLogic.mk_Trueprop (mk_eq (z, arg)) |
|
806 |> cterm_of thy |> Thm.assume |
|
807 |
|
808 val acc = thm COMP ih_case |
|
809 val z_acc_local = acc |
|
810 |> Conv.fconv_rule |
|
811 (Conv.arg_conv (Conv.arg_conv (K (Thm.symmetric (z_eq_arg RS eq_reflection))))) |
|
812 |
|
813 val ethm = z_acc_local |
|
814 |> Function_Ctx_Tree.export_thm thy (fixes, |
|
815 z_eq_arg :: case_hyp :: ags @ assumes) |
|
816 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
|
817 |
|
818 val sub' = sub @ [(([],[]), acc)] |
|
819 in |
|
820 (sub', (hyp :: hyps, ethm :: thms)) |
|
821 end |
|
822 | step _ _ _ _ = raise Match |
|
823 in |
|
824 Function_Ctx_Tree.traverse_tree step tree |
|
825 end |
|
826 |
|
827 |
|
828 fun mk_nest_term_rule thy globals R R_cases clauses = |
|
829 let |
|
830 val Globals { domT, x, z, ... } = globals |
|
831 val acc_R = mk_acc domT R |
|
832 |
|
833 val R' = Free ("R", fastype_of R) |
|
834 |
|
835 val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))) |
|
836 val inrel_R = Const (@{const_name FunDef.in_rel}, |
|
837 HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel |
|
838 |
|
839 val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP}, |
|
840 (domT --> domT --> boolT) --> boolT) $ R') |
|
841 |> cterm_of thy (* "wf R'" *) |
|
842 |
|
843 (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *) |
|
844 val ihyp = Term.all domT $ Abs ("z", domT, |
|
845 Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x), |
|
846 HOLogic.mk_Trueprop (acc_R $ Bound 0))) |
|
847 |> cterm_of thy |
|
848 |
|
849 val ihyp_a = Thm.assume ihyp |> Thm.forall_elim_vars 0 |
|
850 |
|
851 val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x)) |
|
852 |
|
853 val (hyps, cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([], []) |
|
854 in |
|
855 R_cases |
|
856 |> Thm.forall_elim (cterm_of thy z) |
|
857 |> Thm.forall_elim (cterm_of thy x) |
|
858 |> Thm.forall_elim (cterm_of thy (acc_R $ z)) |
|
859 |> curry op COMP (Thm.assume R_z_x) |
|
860 |> fold_rev (curry op COMP) cases |
|
861 |> Thm.implies_intr R_z_x |
|
862 |> Thm.forall_intr (cterm_of thy z) |
|
863 |> (fn it => it COMP accI) |
|
864 |> Thm.implies_intr ihyp |
|
865 |> Thm.forall_intr (cterm_of thy x) |
|
866 |> (fn it => Drule.compose_single(it,2,wf_induct_rule)) |
|
867 |> curry op RS (Thm.assume wfR') |
|
868 |> forall_intr_vars |
|
869 |> (fn it => it COMP allI) |
|
870 |> fold Thm.implies_intr hyps |
|
871 |> Thm.implies_intr wfR' |
|
872 |> Thm.forall_intr (cterm_of thy R') |
|
873 |> Thm.forall_elim (cterm_of thy (inrel_R)) |
|
874 |> curry op RS wf_in_rel |
|
875 |> full_simplify (HOL_basic_ss addsimps [in_rel_def]) |
|
876 |> Thm.forall_intr (cterm_of thy Rrel) |
|
877 end |
|
878 |
|
879 |
|
880 |
|
881 (* Tail recursion (probably very fragile) |
|
882 * |
|
883 * FIXME: |
|
884 * - Need to do forall_elim_vars on psimps: Unneccesary, if psimps would be taken from the same context. |
|
885 * - Must we really replace the fvar by f here? |
|
886 * - Splitting is not configured automatically: Problems with case? |
|
887 *) |
|
888 fun mk_trsimps octxt globals f G R f_def R_cases G_induct clauses psimps = |
|
889 let |
|
890 val Globals {domT, ranT, fvar, ...} = globals |
|
891 |
|
892 val R_cases = Thm.forall_elim_vars 0 R_cases (* FIXME: Should be already in standard form. *) |
|
893 |
|
894 val graph_implies_dom = (* "G ?x ?y ==> dom ?x" *) |
|
895 Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))] |
|
896 (HOLogic.mk_Trueprop (mk_acc domT R $ Free ("x", domT))) |
|
897 (fn {prems=[a], ...} => |
|
898 ((rtac (G_induct OF [a])) |
|
899 THEN_ALL_NEW rtac accI |
|
900 THEN_ALL_NEW etac R_cases |
|
901 THEN_ALL_NEW asm_full_simp_tac (simpset_of octxt)) 1) |
|
902 |
|
903 val default_thm = |
|
904 forall_intr_vars graph_implies_dom COMP (f_def COMP fundef_default_value) |
|
905 |
|
906 fun mk_trsimp clause psimp = |
|
907 let |
|
908 val ClauseInfo {qglr = (oqs, _, _, _), cdata = |
|
909 ClauseContext {ctxt, cqs, gs, lhs, rhs, ...}, ...} = clause |
|
910 val thy = ProofContext.theory_of ctxt |
|
911 val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs |
|
912 |
|
913 val trsimp = Logic.list_implies(gs, |
|
914 HOLogic.mk_Trueprop (HOLogic.mk_eq(f $ lhs, rhs_f))) (* "f lhs = rhs" *) |
|
915 val lhs_acc = (mk_acc domT R $ lhs) (* "acc R lhs" *) |
|
916 fun simp_default_tac ss = |
|
917 asm_full_simp_tac (ss addsimps [default_thm, Let_def]) |
|
918 in |
|
919 Goal.prove ctxt [] [] trsimp (fn _ => |
|
920 rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1 |
|
921 THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1 |
|
922 THEN (simp_default_tac (simpset_of ctxt) 1) |
|
923 THEN TRY ((etac not_acc_down 1) |
|
924 THEN ((etac R_cases) |
|
925 THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1)) |
|
926 |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
|
927 end |
|
928 in |
|
929 map2 mk_trsimp clauses psimps |
|
930 end |
|
931 |
|
932 |
|
933 fun prepare_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy = |
|
934 let |
|
935 val FunctionConfig {domintros, tailrec, default=default_opt, ...} = config |
|
936 |
|
937 val default_str = the_default "%x. undefined" default_opt (*FIXME dynamic scoping*) |
|
938 val fvar = Free (fname, fT) |
|
939 val domT = domain_type fT |
|
940 val ranT = range_type fT |
|
941 |
|
942 val default = Syntax.parse_term lthy default_str |
|
943 |> Type.constraint fT |> Syntax.check_term lthy |
|
944 |
|
945 val (globals, ctxt') = fix_globals domT ranT fvar lthy |
|
946 |
|
947 val Globals { x, h, ... } = globals |
|
948 |
|
949 val clauses = map (mk_clause_context x ctxt') abstract_qglrs |
|
950 |
|
951 val n = length abstract_qglrs |
|
952 |
|
953 fun build_tree (ClauseContext { ctxt, rhs, ...}) = |
|
954 Function_Ctx_Tree.mk_tree (fname, fT) h ctxt rhs |
|
955 |
|
956 val trees = map build_tree clauses |
|
957 val RCss = map find_calls trees |
|
958 |
|
959 val ((G, GIntro_thms, G_elim, G_induct), lthy) = |
|
960 PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy |
|
961 |
|
962 val _ = tracing ("Graph - name: " ^ @{make_string} G) |
|
963 val _ = tracing ("Graph intros:\n" ^ cat_lines (map @{make_string} GIntro_thms)) |
|
964 |
|
965 val ((f, (_, f_defthm)), lthy) = |
|
966 PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy |
|
967 |
|
968 val _ = tracing ("f - name: " ^ @{make_string} f) |
|
969 val _ = tracing ("f_defthm:\n" ^ @{make_string} f_defthm) |
|
970 |
|
971 val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss |
|
972 val trees = map (Function_Ctx_Tree.inst_tree (ProofContext.theory_of lthy) fvar f) trees |
|
973 |
|
974 val ((R, RIntro_thmss, R_elim), lthy) = |
|
975 PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy |
|
976 |
|
977 val _ = tracing ("Relation - name: " ^ @{make_string} R) |
|
978 val _ = tracing ("Relation intros:\n" ^ cat_lines (map @{make_string} RIntro_thmss)) |
|
979 |
|
980 val (_, lthy) = |
|
981 Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy |
|
982 |
|
983 val newthy = ProofContext.theory_of lthy |
|
984 val clauses = map (transfer_clause_ctx newthy) clauses |
|
985 |
|
986 val cert = cterm_of (ProofContext.theory_of lthy) |
|
987 |
|
988 val xclauses = PROFILE "xclauses" |
|
989 (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees |
|
990 RCss GIntro_thms) RIntro_thmss |
|
991 |
|
992 val complete = |
|
993 mk_completeness globals clauses abstract_qglrs |> cert |> Thm.assume |
|
994 |
|
995 val compat = |
|
996 mk_compat_proof_obligations domT ranT fvar f abstract_qglrs |
|
997 |> map (cert #> Thm.assume) |
|
998 |
|
999 val compat_store = store_compat_thms n compat |
|
1000 |
|
1001 val _ = tracing ("globals:\n" ^ @{make_string} globals) |
|
1002 val _ = tracing ("complete:\n" ^ @{make_string} complete) |
|
1003 val _ = tracing ("compat:\n" ^ @{make_string} compat) |
|
1004 val _ = tracing ("compat_store:\n" ^ @{make_string} compat_store) |
|
1005 |
|
1006 val (goalstate, values) = PROFILE "prove_stuff" |
|
1007 (prove_stuff lthy globals G f R xclauses complete compat |
|
1008 compat_store G_elim) f_defthm |
|
1009 |
|
1010 val _ = tracing ("goalstate prove_stuff thm:\n" ^ @{make_string} goalstate) |
|
1011 |
|
1012 val mk_trsimps = |
|
1013 mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses |
|
1014 |
|
1015 fun mk_partial_rules provedgoal = |
|
1016 let |
|
1017 val newthy = theory_of_thm provedgoal (*FIXME*) |
|
1018 |
|
1019 val (graph_is_function, complete_thm) = |
|
1020 provedgoal |
|
1021 |> Conjunction.elim |
|
1022 |> apfst (Thm.forall_elim_vars 0) |
|
1023 |
|
1024 val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff) |
|
1025 |
|
1026 val psimps = PROFILE "Proving simplification rules" |
|
1027 (mk_psimps newthy globals R xclauses values f_iff) graph_is_function |
|
1028 |
|
1029 val simple_pinduct = PROFILE "Proving partial induction rule" |
|
1030 (mk_partial_induct_rule newthy globals R complete_thm) xclauses |
|
1031 |
|
1032 val total_intro = PROFILE "Proving nested termination rule" |
|
1033 (mk_nest_term_rule newthy globals R R_elim) xclauses |
|
1034 |
|
1035 val dom_intros = |
|
1036 if domintros then SOME (PROFILE "Proving domain introduction rules" |
|
1037 (map (mk_domain_intro lthy globals R R_elim)) xclauses) |
|
1038 else NONE |
|
1039 val trsimps = if tailrec then SOME (mk_trsimps psimps) else NONE |
|
1040 |
|
1041 in |
|
1042 FunctionResult {fs=[f], G=G, R=R, cases=complete_thm, |
|
1043 psimps=psimps, simple_pinducts=[simple_pinduct], |
|
1044 termination=total_intro, trsimps=trsimps, |
|
1045 domintros=dom_intros} |
|
1046 end |
|
1047 in |
|
1048 ((f, goalstate, mk_partial_rules), lthy) |
|
1049 end |
|
1050 *} |
|
1051 |
|
1052 ML {* |
|
1053 open Function_Lib |
|
1054 open Function_Common |
|
1055 |
|
1056 type qgar = string * (string * typ) list * term list * term list * term |
|
1057 |
|
1058 datatype mutual_part = MutualPart of |
|
1059 {i : int, |
|
1060 i' : int, |
|
1061 fvar : string * typ, |
|
1062 cargTs: typ list, |
|
1063 f_def: term, |
|
1064 |
|
1065 f: term option, |
|
1066 f_defthm : thm option} |
|
1067 |
|
1068 datatype mutual_info = Mutual of |
|
1069 {n : int, |
|
1070 n' : int, |
|
1071 fsum_var : string * typ, |
|
1072 |
|
1073 ST: typ, |
|
1074 RST: typ, |
|
1075 |
|
1076 parts: mutual_part list, |
|
1077 fqgars: qgar list, |
|
1078 qglrs: ((string * typ) list * term list * term * term) list, |
|
1079 |
|
1080 fsum : term option} |
|
1081 |
|
1082 fun mutual_induct_Pnames n = |
|
1083 if n < 5 then fst (chop n ["P","Q","R","S"]) |
|
1084 else map (fn i => "P" ^ string_of_int i) (1 upto n) |
|
1085 |
|
1086 fun get_part fname = |
|
1087 the o find_first (fn (MutualPart {fvar=(n,_), ...}) => n = fname) |
|
1088 |
|
1089 (* FIXME *) |
|
1090 fun mk_prod_abs e (t1, t2) = |
|
1091 let |
|
1092 val bTs = rev (map snd e) |
|
1093 val T1 = fastype_of1 (bTs, t1) |
|
1094 val T2 = fastype_of1 (bTs, t2) |
|
1095 in |
|
1096 HOLogic.pair_const T1 T2 $ t1 $ t2 |
|
1097 end |
|
1098 |
|
1099 fun analyze_eqs ctxt defname fs eqs = |
|
1100 let |
|
1101 val num = length fs |
|
1102 val fqgars = map (split_def ctxt (K true)) eqs |
|
1103 val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars |
|
1104 |> AList.lookup (op =) #> the |
|
1105 |
|
1106 fun curried_types (fname, fT) = |
|
1107 let |
|
1108 val (caTs, uaTs) = chop (arity_of fname) (binder_types fT) |
|
1109 in |
|
1110 (caTs, uaTs ---> body_type fT) |
|
1111 end |
|
1112 |
|
1113 val (caTss, resultTs) = split_list (map curried_types fs) |
|
1114 val argTs = map (foldr1 HOLogic.mk_prodT) caTss |
|
1115 |
|
1116 val dresultTs = distinct (op =) resultTs |
|
1117 val n' = length dresultTs |
|
1118 |
|
1119 val RST = Balanced_Tree.make (uncurry SumTree.mk_sumT) dresultTs |
|
1120 val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) argTs |
|
1121 |
|
1122 val fsum_type = ST --> RST |
|
1123 |
|
1124 val ([fsum_var_name], _) = Variable.add_fixes [ defname ^ "_sum" ] ctxt |
|
1125 val fsum_var = (fsum_var_name, fsum_type) |
|
1126 |
|
1127 fun define (fvar as (n, _)) caTs resultT i = |
|
1128 let |
|
1129 val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *) |
|
1130 val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1 |
|
1131 |
|
1132 val f_exp = SumTree.mk_proj RST n' i' (Free fsum_var $ SumTree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars)) |
|
1133 val def = Term.abstract_over (Free fsum_var, fold_rev lambda vars f_exp) |
|
1134 |
|
1135 val rew = (n, fold_rev lambda vars f_exp) |
|
1136 in |
|
1137 (MutualPart {i=i, i'=i', fvar=fvar,cargTs=caTs,f_def=def,f=NONE,f_defthm=NONE}, rew) |
|
1138 end |
|
1139 |
|
1140 val (parts, rews) = split_list (map4 define fs caTss resultTs (1 upto num)) |
|
1141 |
|
1142 fun convert_eqs (f, qs, gs, args, rhs) = |
|
1143 let |
|
1144 val MutualPart {i, i', ...} = get_part f parts |
|
1145 in |
|
1146 (qs, gs, SumTree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args), |
|
1147 SumTree.mk_inj RST n' i' (replace_frees rews rhs) |
|
1148 |> Envir.beta_norm) |
|
1149 end |
|
1150 |
|
1151 val qglrs = map convert_eqs fqgars |
|
1152 in |
|
1153 Mutual {n=num, n'=n', fsum_var=fsum_var, ST=ST, RST=RST, |
|
1154 parts=parts, fqgars=fqgars, qglrs=qglrs, fsum=NONE} |
|
1155 end |
|
1156 |
|
1157 fun define_projections fixes mutual fsum lthy = |
|
1158 let |
|
1159 fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy = |
|
1160 let |
|
1161 val ((f, (_, f_defthm)), lthy') = |
|
1162 Local_Theory.define |
|
1163 ((Binding.name fname, mixfix), |
|
1164 ((Binding.conceal (Binding.name (fname ^ "_def")), []), |
|
1165 Term.subst_bound (fsum, f_def))) lthy |
|
1166 in |
|
1167 (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def, |
|
1168 f=SOME f, f_defthm=SOME f_defthm }, |
|
1169 lthy') |
|
1170 end |
|
1171 |
|
1172 val Mutual { n, n', fsum_var, ST, RST, parts, fqgars, qglrs, ... } = mutual |
|
1173 val (parts', lthy') = fold_map def (parts ~~ fixes) lthy |
|
1174 in |
|
1175 (Mutual { n=n, n'=n', fsum_var=fsum_var, ST=ST, RST=RST, parts=parts', |
|
1176 fqgars=fqgars, qglrs=qglrs, fsum=SOME fsum }, |
|
1177 lthy') |
|
1178 end |
|
1179 |
|
1180 fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F = |
|
1181 let |
|
1182 val thy = ProofContext.theory_of ctxt |
|
1183 |
|
1184 val oqnames = map fst pre_qs |
|
1185 val (qs, _) = Variable.variant_fixes oqnames ctxt |
|
1186 |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs |
|
1187 |
|
1188 fun inst t = subst_bounds (rev qs, t) |
|
1189 val gs = map inst pre_gs |
|
1190 val args = map inst pre_args |
|
1191 val rhs = inst pre_rhs |
|
1192 |
|
1193 val cqs = map (cterm_of thy) qs |
|
1194 val ags = map (Thm.assume o cterm_of thy) gs |
|
1195 |
|
1196 val import = fold Thm.forall_elim cqs |
|
1197 #> fold Thm.elim_implies ags |
|
1198 |
|
1199 val export = fold_rev (Thm.implies_intr o cprop_of) ags |
|
1200 #> fold_rev forall_intr_rename (oqnames ~~ cqs) |
|
1201 in |
|
1202 F ctxt (f, qs, gs, args, rhs) import export |
|
1203 end |
|
1204 |
|
1205 fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs) |
|
1206 import (export : thm -> thm) sum_psimp_eq = |
|
1207 let |
|
1208 val (MutualPart {f=SOME f, ...}) = get_part fname parts |
|
1209 |
|
1210 val psimp = import sum_psimp_eq |
|
1211 val (simp, restore_cond) = |
|
1212 case cprems_of psimp of |
|
1213 [] => (psimp, I) |
|
1214 | [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond) |
|
1215 | _ => raise General.Fail "Too many conditions" |
|
1216 |
|
1217 in |
|
1218 Goal.prove ctxt [] [] |
|
1219 (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs)) |
|
1220 (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs) |
|
1221 THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1 |
|
1222 THEN (simp_tac (simpset_of ctxt)) 1) (* FIXME: global simpset?!! *) |
|
1223 |> restore_cond |
|
1224 |> export |
|
1225 end |
|
1226 |
|
1227 fun mk_applied_form ctxt caTs thm = |
|
1228 let |
|
1229 val thy = ProofContext.theory_of ctxt |
|
1230 val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *) |
|
1231 in |
|
1232 fold (fn x => fn thm => Thm.combination thm (Thm.reflexive x)) xs thm |
|
1233 |> Conv.fconv_rule (Thm.beta_conversion true) |
|
1234 |> fold_rev Thm.forall_intr xs |
|
1235 |> Thm.forall_elim_vars 0 |
|
1236 end |
|
1237 |
|
1238 fun mutual_induct_rules lthy induct all_f_defs (Mutual {n, ST, parts, ...}) = |
|
1239 let |
|
1240 val cert = cterm_of (ProofContext.theory_of lthy) |
|
1241 val newPs = |
|
1242 map2 (fn Pname => fn MutualPart {cargTs, ...} => |
|
1243 Free (Pname, cargTs ---> HOLogic.boolT)) |
|
1244 (mutual_induct_Pnames (length parts)) parts |
|
1245 |
|
1246 fun mk_P (MutualPart {cargTs, ...}) P = |
|
1247 let |
|
1248 val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs |
|
1249 val atup = foldr1 HOLogic.mk_prod avars |
|
1250 in |
|
1251 HOLogic.tupled_lambda atup (list_comb (P, avars)) |
|
1252 end |
|
1253 |
|
1254 val Ps = map2 mk_P parts newPs |
|
1255 val case_exp = SumTree.mk_sumcases HOLogic.boolT Ps |
|
1256 |
|
1257 val induct_inst = |
|
1258 Thm.forall_elim (cert case_exp) induct |
|
1259 |> full_simplify SumTree.sumcase_split_ss |
|
1260 |> full_simplify (HOL_basic_ss addsimps all_f_defs) |
|
1261 |
|
1262 fun project rule (MutualPart {cargTs, i, ...}) k = |
|
1263 let |
|
1264 val afs = map_index (fn (j,T) => Free ("a" ^ string_of_int (j + k), T)) cargTs (* FIXME! *) |
|
1265 val inj = SumTree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs) |
|
1266 in |
|
1267 (rule |
|
1268 |> Thm.forall_elim (cert inj) |
|
1269 |> full_simplify SumTree.sumcase_split_ss |
|
1270 |> fold_rev (Thm.forall_intr o cert) (afs @ newPs), |
|
1271 k + length cargTs) |
|
1272 end |
|
1273 in |
|
1274 fst (fold_map (project induct_inst) parts 0) |
|
1275 end |
|
1276 |
|
1277 fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof = |
|
1278 let |
|
1279 val result = inner_cont proof |
|
1280 val FunctionResult {G, R, cases, psimps, trsimps, simple_pinducts=[simple_pinduct], |
|
1281 termination, domintros, ...} = result |
|
1282 |
|
1283 val (all_f_defs, fs) = |
|
1284 map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} => |
|
1285 (mk_applied_form lthy cargTs (Thm.symmetric f_def), f)) |
|
1286 parts |
|
1287 |> split_list |
|
1288 |
|
1289 val all_orig_fdefs = |
|
1290 map (fn MutualPart {f_defthm = SOME f_def, ...} => f_def) parts |
|
1291 |
|
1292 fun mk_mpsimp fqgar sum_psimp = |
|
1293 in_context lthy fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp |
|
1294 |
|
1295 val rew_ss = HOL_basic_ss addsimps all_f_defs |
|
1296 val mpsimps = map2 mk_mpsimp fqgars psimps |
|
1297 val mtrsimps = Option.map (map2 mk_mpsimp fqgars) trsimps |
|
1298 val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m |
|
1299 val mtermination = full_simplify rew_ss termination |
|
1300 val mdomintros = Option.map (map (full_simplify rew_ss)) domintros |
|
1301 in |
|
1302 FunctionResult { fs=fs, G=G, R=R, |
|
1303 psimps=mpsimps, simple_pinducts=minducts, |
|
1304 cases=cases, termination=mtermination, |
|
1305 domintros=mdomintros, trsimps=mtrsimps} |
|
1306 end |
|
1307 |
|
1308 fun prepare_function_mutual config defname fixes eqss lthy = |
|
1309 let |
|
1310 val mutual as Mutual {fsum_var=(n, T), qglrs, ...} = |
|
1311 analyze_eqs lthy defname (map fst fixes) (map Envir.beta_eta_contract eqss) |
|
1312 |
|
1313 val ((fsum, goalstate, cont), lthy') = |
|
1314 prepare_function config defname [((n, T), NoSyn)] qglrs lthy |
|
1315 |
|
1316 val (mutual', lthy'') = define_projections fixes mutual fsum lthy' |
|
1317 |
|
1318 val mutual_cont = mk_partial_rules_mutual lthy'' cont mutual' |
|
1319 in |
|
1320 ((goalstate, mutual_cont), lthy'') |
|
1321 end |
|
1322 |
|
1323 *} |
|
1324 |
|
1325 |
|
1326 ML {* |
|
1327 |
|
1328 open Function_Lib |
|
1329 open Function_Common |
|
1330 |
|
1331 val simp_attribs = map (Attrib.internal o K) |
|
1332 [Simplifier.simp_add, |
|
1333 Code.add_default_eqn_attribute, |
|
1334 Nitpick_Simps.add] |
|
1335 |
|
1336 val psimp_attribs = map (Attrib.internal o K) |
|
1337 [Nitpick_Psimps.add] |
|
1338 |
|
1339 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" |
|
1340 |
|
1341 fun add_simps fnames post sort extra_qualify label mod_binding moreatts |
|
1342 simps lthy = |
|
1343 let |
|
1344 val spec = post simps |
|
1345 |> map (apfst (apsnd (fn ats => moreatts @ ats))) |
|
1346 |> map (apfst (apfst extra_qualify)) |
|
1347 |
|
1348 val (saved_spec_simps, lthy) = |
|
1349 fold_map Local_Theory.note spec lthy |
|
1350 |
|
1351 val saved_simps = maps snd saved_spec_simps |
|
1352 val simps_by_f = sort saved_simps |
|
1353 |
|
1354 fun add_for_f fname simps = |
|
1355 Local_Theory.note |
|
1356 ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps) |
|
1357 #> snd |
|
1358 in |
|
1359 (saved_simps, fold2 add_for_f fnames simps_by_f lthy) |
|
1360 end |
|
1361 |
|
1362 fun prepare_function is_external prep default_constraint fixspec eqns config lthy = |
|
1363 let |
|
1364 val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx)) |
|
1365 val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy |
|
1366 val fixes = map (apfst (apfst Binding.name_of)) fixes0; |
|
1367 val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0; |
|
1368 val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec |
|
1369 |
|
1370 val defname = mk_defname fixes |
|
1371 val FunctionConfig {partials, tailrec, default, ...} = config |
|
1372 val _ = |
|
1373 if tailrec then Output.legacy_feature |
|
1374 "'function (tailrec)' command. Use 'partial_function (tailrec)'." |
|
1375 else () |
|
1376 val _ = |
|
1377 if is_some default then Output.legacy_feature |
|
1378 "'function (default)'. Use 'partial_function'." |
|
1379 else () |
|
1380 |
|
1381 val ((goal_state, cont), lthy') = |
|
1382 prepare_function_mutual config defname fixes eqs lthy |
|
1383 |
|
1384 fun afterqed [[proof]] lthy = |
|
1385 let |
|
1386 val FunctionResult {fs, R, psimps, trsimps, simple_pinducts, |
|
1387 termination, domintros, cases, ...} = |
|
1388 cont (Thm.close_derivation proof) |
|
1389 |
|
1390 val fnames = map (fst o fst) fixes |
|
1391 fun qualify n = Binding.name n |
|
1392 |> Binding.qualify true defname |
|
1393 val conceal_partial = if partials then I else Binding.conceal |
|
1394 |
|
1395 val addsmps = add_simps fnames post sort_cont |
|
1396 |
|
1397 val (((psimps', pinducts'), (_, [termination'])), lthy) = |
|
1398 lthy |
|
1399 |> addsmps (conceal_partial o Binding.qualify false "partial") |
|
1400 "psimps" conceal_partial psimp_attribs psimps |
|
1401 ||> (case trsimps of NONE => I | SOME thms => |
|
1402 addsmps I "simps" I simp_attribs thms #> snd |
|
1403 #> Spec_Rules.add Spec_Rules.Equational (fs, thms)) |
|
1404 ||>> Local_Theory.note ((conceal_partial (qualify "pinduct"), |
|
1405 [Attrib.internal (K (Rule_Cases.case_names cnames)), |
|
1406 Attrib.internal (K (Rule_Cases.consumes 1)), |
|
1407 Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts) |
|
1408 ||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination]) |
|
1409 ||> (snd o Local_Theory.note ((qualify "cases", |
|
1410 [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases])) |
|
1411 ||> (case domintros of NONE => I | SOME thms => |
|
1412 Local_Theory.note ((qualify "domintros", []), thms) #> snd) |
|
1413 |
|
1414 val info = { add_simps=addsmps, case_names=cnames, psimps=psimps', |
|
1415 pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination', |
|
1416 fs=fs, R=R, defname=defname, is_partial=true } |
|
1417 |
|
1418 val _ = |
|
1419 if not is_external then () |
|
1420 else Specification.print_consts lthy (K false) (map fst fixes) |
|
1421 in |
|
1422 (info, |
|
1423 lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info)) |
|
1424 end |
|
1425 in |
|
1426 ((goal_state, afterqed), lthy') |
|
1427 end |
|
1428 |
|
1429 *} |
|
1430 ML {* |
|
1431 Proof.theorem; |
|
1432 Proof.refine |
|
1433 *} |
|
1434 |
|
1435 |
|
1436 ML {* |
|
1437 fun gen_function is_external prep default_constraint fixspec eqns config lthy = |
|
1438 let |
|
1439 val ((goal_state, afterqed), lthy') = |
|
1440 prepare_function is_external prep default_constraint fixspec eqns config lthy |
|
1441 |
|
1442 val _ = tracing ("goal state:\n" ^ @{make_string} goal_state) |
|
1443 val _ = tracing ("concl of goal state:\n" ^ Syntax.string_of_term lthy' (concl_of goal_state)) |
|
1444 in |
|
1445 lthy' |
|
1446 |> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (concl_of goal_state), [])]] |
|
1447 (*|> tap (fn x => tracing ("after thm:\n" ^ Pretty.string_of (Pretty.chunks (Proof.pretty_goals true x))))*) |
|
1448 |> Proof.refine (Method.primitive_text (K goal_state)) |
|
1449 |> Seq.hd |
|
1450 (*|> tap (fn x => tracing ("after ref:\n" ^ Pretty.string_of (Pretty.chunks (Proof.pretty_goals true x))))*) |
|
1451 end |
|
1452 *} |
|
1453 |
|
1454 |
|
1455 ML {* |
|
1456 val function = gen_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS) |
|
1457 val function_cmd = gen_function true Specification.read_spec "_::type" |
|
1458 |
|
1459 fun add_case_cong n thy = |
|
1460 let |
|
1461 val cong = #case_cong (Datatype.the_info thy n) |
|
1462 |> safe_mk_meta_eq |
|
1463 in |
|
1464 Context.theory_map |
|
1465 (Function_Ctx_Tree.map_function_congs (Thm.add_thm cong)) thy |
|
1466 end |
|
1467 |
|
1468 val setup_case_cong = Datatype.interpretation (K (fold add_case_cong)) |
|
1469 |
|
1470 |
|
1471 (* setup *) |
|
1472 |
|
1473 val setup = |
|
1474 Attrib.setup @{binding fundef_cong} |
|
1475 (Attrib.add_del Function_Ctx_Tree.cong_add Function_Ctx_Tree.cong_del) |
|
1476 "declaration of congruence rule for function definitions" |
|
1477 #> setup_case_cong |
|
1478 #> Function_Relation.setup |
|
1479 #> Function_Common.Termination_Simps.setup |
|
1480 |
|
1481 val get_congs = Function_Ctx_Tree.get_function_congs |
|
1482 |
|
1483 fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t |
|
1484 |> the_single |> snd |
|
1485 |
|
1486 |
|
1487 (* outer syntax *) |
|
1488 |
|
1489 val _ = |
|
1490 Outer_Syntax.local_theory_to_proof "nominal_primrec" "define recursive functions for nominal types" |
|
1491 Keyword.thy_goal |
|
1492 (function_parser default_config |
|
1493 >> (fn ((config, fixes), statements) => function_cmd fixes statements config)) |
|
1494 *} |
|
1495 |
|
1496 ML {* trace := true *} |
|
1497 |
|
1498 nominal_primrec |
|
1499 depth :: "lam \<Rightarrow> nat" |
|
1500 where |
|
1501 "depth (Var x) = 1" |
|
1502 | "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1" |
|
1503 | "depth (Lam x t) = (depth t) + 1" |
|
1504 apply(rule_tac y="x" in lam.exhaust) |
|
1505 apply(simp_all)[3] |
|
1506 apply(simp_all only: lam.distinct) |
|
1507 apply(simp add: lam.eq_iff) |
|
1508 apply(simp add: lam.eq_iff) |
|
1509 sorry |
|
1510 |
|
1511 nominal_primrec |
|
1512 frees :: "lam \<Rightarrow> name set" |
|
1513 where |
|
1514 "frees (Var x) = {x}" |
|
1515 | "frees (App t1 t2) = (frees t1) \<union> (frees t2)" |
|
1516 | "frees (Lam x t) = (frees t) - {x}" |
|
1517 apply(rule_tac y="x" in lam.exhaust) |
|
1518 apply(simp_all)[3] |
|
1519 apply(simp_all only: lam.distinct) |
|
1520 apply(simp add: lam.eq_iff) |
|
1521 apply(simp add: lam.eq_iff) |
|
1522 apply(simp add: lam.eq_iff) |
|
1523 sorry |
|
1524 |
|
1525 nominal_primrec |
|
1526 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [100,100,100] 100) |
|
1527 where |
|
1528 "(Var x)[y ::= s] = (if x=y then s else (Var x))" |
|
1529 | "(App t\<^isub>1 t\<^isub>2)[y ::= s] = App (t\<^isub>1[y ::= s]) (t\<^isub>2[y ::= s])" |
|
1530 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])" |
|
1531 apply(case_tac x) |
|
1532 apply(simp) |
|
1533 apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust) |
|
1534 apply(simp_all add: lam.distinct)[3] |
|
1535 apply(auto)[1] |
|
1536 apply(auto)[1] |
|
1537 apply(simp add: fresh_star_def) |
|
1538 apply(simp_all add: lam.distinct)[5] |
|
1539 apply(simp add: lam.eq_iff) |
|
1540 apply(simp add: lam.eq_iff) |
|
1541 apply(simp add: lam.eq_iff) |
|
1542 sorry |
|
1543 |
|
1544 |
|
1545 |
|
1546 end |
|
1547 |
|
1548 |
|
1549 |