66 val dummyPs = map (fn (Var (_, Type (_, [T', T'']))) => |
66 val dummyPs = map (fn (Var (_, Type (_, [T', T'']))) => |
67 Abs ("z", T', Const ("True", T''))) induct_Ps; |
67 Abs ("z", T', Const ("True", T''))) induct_Ps; |
68 val P = Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", maxidx+1), T), Bound 0) $ |
68 val P = Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", maxidx+1), T), Bound 0) $ |
69 Var (("P", 0), HOLogic.boolT)) |
69 Var (("P", 0), HOLogic.boolT)) |
70 val insts = Library.take (i, dummyPs) @ (P::(Library.drop (i + 1, dummyPs))); |
70 val insts = Library.take (i, dummyPs) @ (P::(Library.drop (i + 1, dummyPs))); |
71 val cert = cterm_of (Theory.sign_of thy); |
71 val cert = cterm_of thy; |
72 val insts' = (map cert induct_Ps) ~~ (map cert insts); |
72 val insts' = (map cert induct_Ps) ~~ (map cert insts); |
73 val induct' = refl RS ((List.nth |
73 val induct' = refl RS ((List.nth |
74 (split_conj_thm (cterm_instantiate insts' induct), i)) RSN (2, rev_mp)) |
74 (split_conj_thm (cterm_instantiate insts' induct), i)) RSN (2, rev_mp)) |
75 |
75 |
76 in OldGoals.prove_goalw_cterm [] (cert t) (fn prems => |
76 in |
77 [rtac induct' 1, |
77 standard (Goal.prove thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t) |
78 REPEAT (rtac TrueI 1), |
78 (fn prems => EVERY |
79 REPEAT ((rtac impI 1) THEN (eresolve_tac prems 1)), |
79 [rtac induct' 1, |
80 REPEAT (rtac TrueI 1)]) |
80 REPEAT (rtac TrueI 1), |
|
81 REPEAT ((rtac impI 1) THEN (eresolve_tac prems 1)), |
|
82 REPEAT (rtac TrueI 1)])) |
81 end; |
83 end; |
82 |
84 |
83 val casedist_thms = map prove_casedist_thm ((0 upto (length newTs - 1)) ~~ |
85 val casedist_thms = map prove_casedist_thm ((0 upto (length newTs - 1)) ~~ |
84 (DatatypeProp.make_casedists descr sorts) ~~ newTs) |
86 (DatatypeProp.make_casedists descr sorts) ~~ newTs) |
85 in thy |> store_thms_atts "exhaust" new_type_names (map single case_names_exhausts) casedist_thms end; |
87 in thy |> store_thms_atts "exhaust" new_type_names (map single case_names_exhausts) casedist_thms end; |
199 val rec_unique_ts = map (fn (((set_t, T1), T2), i) => |
201 val rec_unique_ts = map (fn (((set_t, T1), T2), i) => |
200 Const ("Ex1", (T2 --> HOLogic.boolT) --> HOLogic.boolT) $ |
202 Const ("Ex1", (T2 --> HOLogic.boolT) --> HOLogic.boolT) $ |
201 absfree ("y", T2, HOLogic.mk_mem (HOLogic.mk_prod |
203 absfree ("y", T2, HOLogic.mk_mem (HOLogic.mk_prod |
202 (mk_Free "x" T1 i, Free ("y", T2)), set_t))) |
204 (mk_Free "x" T1 i, Free ("y", T2)), set_t))) |
203 (rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs)); |
205 (rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs)); |
204 val cert = cterm_of (Theory.sign_of thy1) |
206 val cert = cterm_of thy1 |
205 val insts = map (fn ((i, T), t) => absfree ("x" ^ (string_of_int i), T, t)) |
207 val insts = map (fn ((i, T), t) => absfree ("x" ^ (string_of_int i), T, t)) |
206 ((1 upto length recTs) ~~ recTs ~~ rec_unique_ts); |
208 ((1 upto length recTs) ~~ recTs ~~ rec_unique_ts); |
207 val induct' = cterm_instantiate ((map cert induct_Ps) ~~ |
209 val induct' = cterm_instantiate ((map cert induct_Ps) ~~ |
208 (map cert insts)) induct; |
210 (map cert insts)) induct; |
209 val (tac, _) = Library.foldl mk_unique_tac |
211 val (tac, _) = Library.foldl mk_unique_tac |
210 (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_tac) 1 |
212 (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_tac) 1 |
211 THEN rewtac (mk_meta_eq choice_eq), rec_intrs), |
213 THEN rewtac (mk_meta_eq choice_eq), rec_intrs), |
212 descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts); |
214 descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts); |
213 |
215 |
214 in split_conj_thm (OldGoals.prove_goalw_cterm [] |
216 in split_conj_thm (standard (Goal.prove thy1 [] [] |
215 (cert (HOLogic.mk_Trueprop (mk_conj rec_unique_ts))) (K [tac])) |
217 (HOLogic.mk_Trueprop (mk_conj rec_unique_ts)) (K tac))) |
216 end; |
218 end; |
217 |
219 |
218 val rec_total_thms = map (fn r => r RS theI') rec_unique_thms; |
220 val rec_total_thms = map (fn r => r RS theI') rec_unique_thms; |
219 |
221 |
220 (* define primrec combinators *) |
222 (* define primrec combinators *) |
242 |
244 |
243 (* prove characteristic equations for primrec combinators *) |
245 (* prove characteristic equations for primrec combinators *) |
244 |
246 |
245 val _ = message "Proving characteristic theorems for primrec combinators ..." |
247 val _ = message "Proving characteristic theorems for primrec combinators ..." |
246 |
248 |
247 val rec_thms = map (fn t => OldGoals.prove_goalw_cterm reccomb_defs |
249 val rec_thms = map (fn t => standard (Goal.prove thy2 [] [] t |
248 (cterm_of (Theory.sign_of thy2) t) (fn _ => |
250 (fn _ => EVERY |
249 [rtac the1_equality 1, |
251 [rewrite_goals_tac reccomb_defs, |
|
252 rtac the1_equality 1, |
250 resolve_tac rec_unique_thms 1, |
253 resolve_tac rec_unique_thms 1, |
251 resolve_tac rec_intrs 1, |
254 resolve_tac rec_intrs 1, |
252 REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)])) |
255 REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)]))) |
253 (DatatypeProp.make_primrecs new_type_names descr sorts thy2) |
256 (DatatypeProp.make_primrecs new_type_names descr sorts thy2) |
254 |
257 |
255 in |
258 in |
256 thy2 |> Theory.add_path (space_implode "_" new_type_names) |> |
259 thy2 |> Theory.add_path (space_implode "_" new_type_names) |> |
257 PureThy.add_thmss [(("recs", rec_thms), [])] |>> |
260 PureThy.add_thmss [(("recs", rec_thms), [])] |>> |
316 |
319 |
317 in (defs @ [def_thm], thy') |
320 in (defs @ [def_thm], thy') |
318 end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~ |
321 end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~ |
319 (Library.take (length newTs, reccomb_names))); |
322 (Library.take (length newTs, reccomb_names))); |
320 |
323 |
321 val case_thms = map (map (fn t => OldGoals.prove_goalw_cterm (case_defs @ |
324 val case_thms = map (map (fn t => standard (Goal.prove thy2 [] [] t |
322 (map mk_meta_eq primrec_thms)) (cterm_of (Theory.sign_of thy2) t) |
325 (fn _ => EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1])))) |
323 (fn _ => [rtac refl 1]))) |
|
324 (DatatypeProp.make_cases new_type_names descr sorts thy2) |
326 (DatatypeProp.make_cases new_type_names descr sorts thy2) |
325 |
327 |
326 in |
328 in |
327 thy2 |> |
329 thy2 |> |
328 parent_path flat_names |> |
330 parent_path flat_names |> |
343 val newTs = Library.take (length (hd descr), recTs); |
345 val newTs = Library.take (length (hd descr), recTs); |
344 |
346 |
345 fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'), |
347 fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'), |
346 exhaustion), case_thms'), T) = |
348 exhaustion), case_thms'), T) = |
347 let |
349 let |
348 val cert = cterm_of (Theory.sign_of thy); |
350 val cert = cterm_of thy; |
349 val _ $ (_ $ lhs $ _) = hd (Logic.strip_assums_hyp (hd (prems_of exhaustion))); |
351 val _ $ (_ $ lhs $ _) = hd (Logic.strip_assums_hyp (hd (prems_of exhaustion))); |
350 val exhaustion' = cterm_instantiate |
352 val exhaustion' = cterm_instantiate |
351 [(cert lhs, cert (Free ("x", T)))] exhaustion; |
353 [(cert lhs, cert (Free ("x", T)))] exhaustion; |
352 val tacsf = K [rtac exhaustion' 1, ALLGOALS (asm_simp_tac |
354 val tacf = K (EVERY [rtac exhaustion' 1, ALLGOALS (asm_simp_tac |
353 (HOL_ss addsimps (dist_rewrites' @ inject @ case_thms')))] |
355 (HOL_ss addsimps (dist_rewrites' @ inject @ case_thms')))]) |
354 in |
356 in |
355 (OldGoals.prove_goalw_cterm [] (cert t1) tacsf, |
357 (standard (Goal.prove thy [] [] t1 tacf), |
356 OldGoals.prove_goalw_cterm [] (cert t2) tacsf) |
358 standard (Goal.prove thy [] [] t2 tacf)) |
357 end; |
359 end; |
358 |
360 |
359 val split_thm_pairs = map prove_split_thms |
361 val split_thm_pairs = map prove_split_thms |
360 ((DatatypeProp.make_splits new_type_names descr sorts thy) ~~ constr_inject ~~ |
362 ((DatatypeProp.make_splits new_type_names descr sorts thy) ~~ constr_inject ~~ |
361 dist_rewrites ~~ casedist_thms ~~ case_thms ~~ newTs); |
363 dist_rewrites ~~ casedist_thms ~~ case_thms ~~ newTs); |
417 (size_names ~~ recTs ~~ def_names ~~ reccomb_names)) |>> |
419 (size_names ~~ recTs ~~ def_names ~~ reccomb_names)) |>> |
418 parent_path flat_names; |
420 parent_path flat_names; |
419 |
421 |
420 val rewrites = size_def_thms @ map mk_meta_eq primrec_thms; |
422 val rewrites = size_def_thms @ map mk_meta_eq primrec_thms; |
421 |
423 |
422 val size_thms = map (fn t => OldGoals.prove_goalw_cterm rewrites |
424 val size_thms = map (fn t => standard (Goal.prove thy' [] [] t |
423 (cterm_of (Theory.sign_of thy') t) (fn _ => [rtac refl 1])) |
425 (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]))) |
424 (DatatypeProp.make_size descr sorts thy') |
426 (DatatypeProp.make_size descr sorts thy') |
425 |
427 |
426 in |
428 in |
427 thy' |> Theory.add_path big_name |> |
429 thy' |> Theory.add_path big_name |> |
428 PureThy.add_thmss [(("size", size_thms), [])] |>> |
430 PureThy.add_thmss [(("size", size_thms), [])] |>> |
430 end; |
432 end; |
431 |
433 |
432 fun prove_weak_case_congs new_type_names descr sorts thy = |
434 fun prove_weak_case_congs new_type_names descr sorts thy = |
433 let |
435 let |
434 fun prove_weak_case_cong t = |
436 fun prove_weak_case_cong t = |
435 OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) t) |
437 standard (Goal.prove thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t) |
436 (fn prems => [rtac ((hd prems) RS arg_cong) 1]) |
438 (fn prems => EVERY [rtac ((hd prems) RS arg_cong) 1])) |
437 |
439 |
438 val weak_case_congs = map prove_weak_case_cong (DatatypeProp.make_weak_case_congs |
440 val weak_case_congs = map prove_weak_case_cong (DatatypeProp.make_weak_case_congs |
439 new_type_names descr sorts thy) |
441 new_type_names descr sorts thy) |
440 |
442 |
441 in thy |> store_thms "weak_case_cong" new_type_names weak_case_congs end; |
443 in thy |> store_thms "weak_case_cong" new_type_names weak_case_congs end; |
451 (* For goal i, select the correct disjunct to attack, then prove it *) |
453 (* For goal i, select the correct disjunct to attack, then prove it *) |
452 fun tac i 0 = EVERY [TRY (rtac disjI1 i), |
454 fun tac i 0 = EVERY [TRY (rtac disjI1 i), |
453 hyp_subst_tac i, REPEAT (rtac exI i), rtac refl i] |
455 hyp_subst_tac i, REPEAT (rtac exI i), rtac refl i] |
454 | tac i n = rtac disjI2 i THEN tac i (n - 1) |
456 | tac i n = rtac disjI2 i THEN tac i (n - 1) |
455 in |
457 in |
456 OldGoals.prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) t) (fn _ => |
458 standard (Goal.prove thy [] [] t (fn _ => |
457 [rtac allI 1, |
459 EVERY [rtac allI 1, |
458 exh_tac (K exhaustion) 1, |
460 exh_tac (K exhaustion) 1, |
459 ALLGOALS (fn i => tac i (i-1))]) |
461 ALLGOALS (fn i => tac i (i-1))])) |
460 end; |
462 end; |
461 |
463 |
462 val nchotomys = |
464 val nchotomys = |
463 map prove_nchotomy (DatatypeProp.make_nchotomys descr sorts ~~ casedist_thms) |
465 map prove_nchotomy (DatatypeProp.make_nchotomys descr sorts ~~ casedist_thms) |
464 |
466 |
473 val cert = cterm_of (Theory.sign_of thy); |
475 val cert = cterm_of (Theory.sign_of thy); |
474 val nchotomy' = nchotomy RS spec; |
476 val nchotomy' = nchotomy RS spec; |
475 val nchotomy'' = cterm_instantiate |
477 val nchotomy'' = cterm_instantiate |
476 [(cert (hd (add_term_vars (concl_of nchotomy', []))), cert Ma)] nchotomy' |
478 [(cert (hd (add_term_vars (concl_of nchotomy', []))), cert Ma)] nchotomy' |
477 in |
479 in |
478 OldGoals.prove_goalw_cterm [] (cert t) (fn prems => |
480 standard (Goal.prove thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t) |
479 let val simplify = asm_simp_tac (HOL_ss addsimps (prems @ case_rewrites)) |
481 (fn prems => |
480 in [simp_tac (HOL_ss addsimps [hd prems]) 1, |
482 let val simplify = asm_simp_tac (HOL_ss addsimps (prems @ case_rewrites)) |
481 cut_facts_tac [nchotomy''] 1, |
483 in EVERY [simp_tac (HOL_ss addsimps [hd prems]) 1, |
482 REPEAT (etac disjE 1 THEN REPEAT (etac exE 1) THEN simplify 1), |
484 cut_facts_tac [nchotomy''] 1, |
483 REPEAT (etac exE 1) THEN simplify 1 (* Get last disjunct *)] |
485 REPEAT (etac disjE 1 THEN REPEAT (etac exE 1) THEN simplify 1), |
484 end) |
486 REPEAT (etac exE 1) THEN simplify 1 (* Get last disjunct *)] |
|
487 end)) |
485 end; |
488 end; |
486 |
489 |
487 val case_congs = map prove_case_cong (DatatypeProp.make_case_congs |
490 val case_congs = map prove_case_cong (DatatypeProp.make_case_congs |
488 new_type_names descr sorts thy ~~ nchotomys ~~ case_thms) |
491 new_type_names descr sorts thy ~~ nchotomys ~~ case_thms) |
489 |
492 |