376 " Proving monotonicity ..."; |
376 " Proving monotonicity ..."; |
377 (if skip_mono then Goal.prove_sorry else Goal.prove_future) ctxt |
377 (if skip_mono then Goal.prove_sorry else Goal.prove_future) ctxt |
378 [] [] |
378 [] [] |
379 (HOLogic.mk_Trueprop |
379 (HOLogic.mk_Trueprop |
380 (Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun)) |
380 (Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun)) |
381 (fn _ => EVERY [rtac @{thm monoI} 1, |
381 (fn _ => EVERY [resolve_tac @{thms monoI} 1, |
382 REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI'}] 1), |
382 REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI'}] 1), |
383 REPEAT (FIRST |
383 REPEAT (FIRST |
384 [atac 1, |
384 [assume_tac 1, |
385 resolve_tac (map (mk_mono ctxt) monos @ get_monos ctxt) 1, |
385 resolve_tac (map (mk_mono ctxt) monos @ get_monos ctxt) 1, |
386 etac @{thm le_funE} 1, dtac @{thm le_boolD} 1])])); |
386 eresolve_tac @{thms le_funE} 1, |
|
387 dresolve_tac @{thms le_boolD} 1])])); |
387 |
388 |
388 |
389 |
389 (* prove introduction rules *) |
390 (* prove introduction rules *) |
390 |
391 |
391 fun prove_intrs quiet_mode coind mono fp_def k intr_ts rec_preds_defs ctxt ctxt' = |
392 fun prove_intrs quiet_mode coind mono fp_def k intr_ts rec_preds_defs ctxt ctxt' = |
399 val rules = [refl, TrueI, @{lemma "~ False" by (rule notI)}, exI, conjI]; |
400 val rules = [refl, TrueI, @{lemma "~ False" by (rule notI)}, exI, conjI]; |
400 |
401 |
401 val intrs = map_index (fn (i, intr) => |
402 val intrs = map_index (fn (i, intr) => |
402 Goal.prove_sorry ctxt [] [] intr (fn _ => EVERY |
403 Goal.prove_sorry ctxt [] [] intr (fn _ => EVERY |
403 [rewrite_goals_tac ctxt rec_preds_defs, |
404 [rewrite_goals_tac ctxt rec_preds_defs, |
404 rtac (unfold RS iffD2) 1, |
405 resolve_tac [unfold RS iffD2] 1, |
405 EVERY1 (select_disj (length intr_ts) (i + 1)), |
406 EVERY1 (select_disj (length intr_ts) (i + 1)), |
406 (*Not ares_tac, since refl must be tried before any equality assumptions; |
407 (*Not ares_tac, since refl must be tried before any equality assumptions; |
407 backtracking may occur if the premises have extra variables!*) |
408 backtracking may occur if the premises have extra variables!*) |
408 DEPTH_SOLVE_1 (resolve_tac rules 1 APPEND assume_tac 1)]) |
409 DEPTH_SOLVE_1 (resolve_tac rules 1 APPEND assume_tac 1)]) |
409 |> singleton (Proof_Context.export ctxt ctxt')) intr_ts |
410 |> singleton (Proof_Context.export ctxt ctxt')) intr_ts |
445 in |
446 in |
446 (Goal.prove_sorry ctxt'' [] prems P |
447 (Goal.prove_sorry ctxt'' [] prems P |
447 (fn {context = ctxt4, prems} => EVERY |
448 (fn {context = ctxt4, prems} => EVERY |
448 [cut_tac (hd prems) 1, |
449 [cut_tac (hd prems) 1, |
449 rewrite_goals_tac ctxt4 rec_preds_defs, |
450 rewrite_goals_tac ctxt4 rec_preds_defs, |
450 dtac (unfold RS iffD1) 1, |
451 dresolve_tac [unfold RS iffD1] 1, |
451 REPEAT (FIRSTGOAL (eresolve_tac rules1)), |
452 REPEAT (FIRSTGOAL (eresolve_tac rules1)), |
452 REPEAT (FIRSTGOAL (eresolve_tac rules2)), |
453 REPEAT (FIRSTGOAL (eresolve_tac rules2)), |
453 EVERY (map (fn prem => |
454 EVERY (map (fn prem => |
454 DEPTH_SOLVE_1 (ares_tac [rewrite_rule ctxt4 rec_preds_defs prem, conjI] 1)) |
455 DEPTH_SOLVE_1 (ares_tac [rewrite_rule ctxt4 rec_preds_defs prem, conjI] 1)) |
455 (tl prems))]) |
456 (tl prems))]) |
492 if null c_intrs then @{term False} |
493 if null c_intrs then @{term False} |
493 else foldr1 HOLogic.mk_disj (map mk_intr_conj c_intrs); |
494 else foldr1 HOLogic.mk_disj (map mk_intr_conj c_intrs); |
494 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); |
495 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); |
495 fun prove_intr1 (i, _) = Subgoal.FOCUS_PREMS (fn {params, prems, ...} => |
496 fun prove_intr1 (i, _) = Subgoal.FOCUS_PREMS (fn {params, prems, ...} => |
496 EVERY1 (select_disj (length c_intrs) (i + 1)) THEN |
497 EVERY1 (select_disj (length c_intrs) (i + 1)) THEN |
497 EVERY (replicate (length params) (rtac @{thm exI} 1)) THEN |
498 EVERY (replicate (length params) (resolve_tac @{thms exI} 1)) THEN |
498 (if null prems then rtac @{thm TrueI} 1 |
499 (if null prems then resolve_tac @{thms TrueI} 1 |
499 else |
500 else |
500 let |
501 let |
501 val (prems', last_prem) = split_last prems; |
502 val (prems', last_prem) = split_last prems; |
502 in |
503 in |
503 EVERY (map (fn prem => (rtac @{thm conjI} 1 THEN rtac prem 1)) prems') THEN |
504 EVERY (map (fn prem => |
504 rtac last_prem 1 |
505 (resolve_tac @{thms conjI} 1 THEN resolve_tac [prem] 1)) prems') THEN |
|
506 resolve_tac [last_prem] 1 |
505 end)) ctxt' 1; |
507 end)) ctxt' 1; |
506 fun prove_intr2 (((_, _, us, _), ts, params'), intr) = |
508 fun prove_intr2 (((_, _, us, _), ts, params'), intr) = |
507 EVERY (replicate (length params') (etac @{thm exE} 1)) THEN |
509 EVERY (replicate (length params') (eresolve_tac @{thms exE} 1)) THEN |
508 (if null ts andalso null us then rtac intr 1 |
510 (if null ts andalso null us then resolve_tac [intr] 1 |
509 else |
511 else |
510 EVERY (replicate (length ts + length us - 1) (etac @{thm conjE} 1)) THEN |
512 EVERY (replicate (length ts + length us - 1) (eresolve_tac @{thms conjE} 1)) THEN |
511 Subgoal.FOCUS_PREMS (fn {context = ctxt'', params, prems, ...} => |
513 Subgoal.FOCUS_PREMS (fn {context = ctxt'', params, prems, ...} => |
512 let |
514 let |
513 val (eqs, prems') = chop (length us) prems; |
515 val (eqs, prems') = chop (length us) prems; |
514 val rew_thms = map (fn th => th RS @{thm eq_reflection}) eqs; |
516 val rew_thms = map (fn th => th RS @{thm eq_reflection}) eqs; |
515 in |
517 in |
516 rewrite_goal_tac ctxt'' rew_thms 1 THEN |
518 rewrite_goal_tac ctxt'' rew_thms 1 THEN |
517 rtac intr 1 THEN |
519 resolve_tac [intr] 1 THEN |
518 EVERY (map (fn p => rtac p 1) prems') |
520 EVERY (map (fn p => resolve_tac [p] 1) prems') |
519 end) ctxt' 1); |
521 end) ctxt' 1); |
520 in |
522 in |
521 Goal.prove_sorry ctxt' [] [] eq (fn _ => |
523 Goal.prove_sorry ctxt' [] [] eq (fn _ => |
522 rtac @{thm iffI} 1 THEN etac (#1 elim) 1 THEN |
524 resolve_tac @{thms iffI} 1 THEN |
|
525 eresolve_tac [#1 elim] 1 THEN |
523 EVERY (map_index prove_intr1 c_intrs) THEN |
526 EVERY (map_index prove_intr1 c_intrs) THEN |
524 (if null c_intrs then etac @{thm FalseE} 1 |
527 (if null c_intrs then eresolve_tac @{thms FalseE} 1 |
525 else |
528 else |
526 let val (c_intrs', last_c_intr) = split_last c_intrs in |
529 let val (c_intrs', last_c_intr) = split_last c_intrs in |
527 EVERY (map (fn ci => etac @{thm disjE} 1 THEN prove_intr2 ci) c_intrs') THEN |
530 EVERY (map (fn ci => eresolve_tac @{thms disjE} 1 THEN prove_intr2 ci) c_intrs') THEN |
528 prove_intr2 last_c_intr |
531 prove_intr2 last_c_intr |
529 end)) |
532 end)) |
530 |> rulify ctxt' |
533 |> rulify ctxt' |
531 |> singleton (Proof_Context.export ctxt' ctxt'') |
534 |> singleton (Proof_Context.export ctxt' ctxt'') |
532 end; |
535 end; |
727 val raw_fp_induct = mono RS (fp_def RS @{thm def_lfp_induct}); |
730 val raw_fp_induct = mono RS (fp_def RS @{thm def_lfp_induct}); |
728 |
731 |
729 val induct = Goal.prove_sorry ctxt'' [] ind_prems ind_concl |
732 val induct = Goal.prove_sorry ctxt'' [] ind_prems ind_concl |
730 (fn {context = ctxt3, prems} => EVERY |
733 (fn {context = ctxt3, prems} => EVERY |
731 [rewrite_goals_tac ctxt3 [inductive_conj_def], |
734 [rewrite_goals_tac ctxt3 [inductive_conj_def], |
732 DETERM (rtac raw_fp_induct 1), |
735 DETERM (resolve_tac [raw_fp_induct] 1), |
733 REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI}] 1), |
736 REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI}] 1), |
734 rewrite_goals_tac ctxt3 simp_thms2, |
737 rewrite_goals_tac ctxt3 simp_thms2, |
735 (*This disjE separates out the introduction rules*) |
738 (*This disjE separates out the introduction rules*) |
736 REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])), |
739 REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])), |
737 (*Now break down the individual cases. No disjE here in case |
740 (*Now break down the individual cases. No disjE here in case |
738 some premise involves disjunction.*) |
741 some premise involves disjunction.*) |
739 REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac ctxt3)), |
742 REPEAT (FIRSTGOAL (eresolve_tac [conjE] ORELSE' bound_hyp_subst_tac ctxt3)), |
740 REPEAT (FIRSTGOAL |
743 REPEAT (FIRSTGOAL |
741 (resolve_tac [conjI, impI] ORELSE' (etac notE THEN' atac))), |
744 (resolve_tac [conjI, impI] ORELSE' (eresolve_tac [notE] THEN' assume_tac))), |
742 EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule ctxt3 |
745 EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule ctxt3 |
743 (inductive_conj_def :: rec_preds_defs @ simp_thms2) prem, |
746 (inductive_conj_def :: rec_preds_defs @ simp_thms2) prem, |
744 conjI, refl] 1)) prems)]); |
747 conjI, refl] 1)) prems)]); |
745 |
748 |
746 val lemma = Goal.prove_sorry ctxt'' [] [] |
749 val lemma = Goal.prove_sorry ctxt'' [] [] |
747 (Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn {context = ctxt3, ...} => EVERY |
750 (Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn {context = ctxt3, ...} => EVERY |
748 [rewrite_goals_tac ctxt3 rec_preds_defs, |
751 [rewrite_goals_tac ctxt3 rec_preds_defs, |
749 REPEAT (EVERY |
752 REPEAT (EVERY |
750 [REPEAT (resolve_tac [conjI, impI] 1), |
753 [REPEAT (resolve_tac [conjI, impI] 1), |
751 REPEAT (eresolve_tac [@{thm le_funE}, @{thm le_boolE}] 1), |
754 REPEAT (eresolve_tac [@{thm le_funE}, @{thm le_boolE}] 1), |
752 atac 1, |
755 assume_tac 1, |
753 rewrite_goals_tac ctxt3 simp_thms1, |
756 rewrite_goals_tac ctxt3 simp_thms1, |
754 atac 1])]); |
757 assume_tac 1])]); |
755 |
758 |
756 in singleton (Proof_Context.export ctxt'' ctxt''') (induct RS lemma) end; |
759 in singleton (Proof_Context.export ctxt'' ctxt''') (induct RS lemma) end; |
757 |
760 |
758 |
761 |
759 |
762 |