467 fun mk_intr_conj (((_, _, us, _), ts, params'), _) = |
467 fun mk_intr_conj (((_, _, us, _), ts, params'), _) = |
468 let |
468 let |
469 fun list_ex ([], t) = t |
469 fun list_ex ([], t) = t |
470 | list_ex ((a, T) :: vars, t) = |
470 | list_ex ((a, T) :: vars, t) = |
471 HOLogic.exists_const T $ Abs (a, T, list_ex (vars, t)); |
471 HOLogic.exists_const T $ Abs (a, T, list_ex (vars, t)); |
472 val conjs = map2 (curry HOLogic.mk_eq) frees us @ (map HOLogic.dest_Trueprop ts); |
472 val conjs = map2 (curry HOLogic.mk_eq) frees us @ map HOLogic.dest_Trueprop ts; |
473 in |
473 in |
474 list_ex (params', if null conjs then @{term True} else foldr1 HOLogic.mk_conj conjs) |
474 list_ex (params', if null conjs then @{term True} else foldr1 HOLogic.mk_conj conjs) |
475 end; |
475 end; |
476 val lhs = list_comb (c, params @ frees); |
476 val lhs = list_comb (c, params @ frees); |
477 val rhs = |
477 val rhs = |
478 if null c_intrs then @{term False} |
478 if null c_intrs then @{term False} |
479 else foldr1 HOLogic.mk_disj (map mk_intr_conj c_intrs); |
479 else foldr1 HOLogic.mk_disj (map mk_intr_conj c_intrs); |
480 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); |
480 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); |
481 fun prove_intr1 (i, _) = Subgoal.FOCUS_PREMS (fn {params, prems, ...} => |
481 fun prove_intr1 (i, _) = Subgoal.FOCUS_PREMS (fn {params, prems, ...} => |
482 let |
482 EVERY1 (select_disj (length c_intrs) (i + 1)) THEN |
483 val (prems', last_prem) = split_last prems; |
483 EVERY (replicate (length params) (rtac @{thm exI} 1)) THEN |
484 in |
484 (if null prems then rtac @{thm TrueI} 1 |
485 EVERY1 (select_disj (length c_intrs) (i + 1)) THEN |
485 else |
486 EVERY (replicate (length params) (rtac @{thm exI} 1)) THEN |
486 let |
487 EVERY (map (fn prem => (rtac @{thm conjI} 1 THEN rtac prem 1)) prems') THEN |
487 val (prems', last_prem) = split_last prems; |
488 rtac last_prem 1 |
488 in |
489 end) ctxt' 1; |
489 EVERY (map (fn prem => (rtac @{thm conjI} 1 THEN rtac prem 1)) prems') THEN |
|
490 rtac last_prem 1 |
|
491 end)) ctxt' 1; |
490 fun prove_intr2 (((_, _, us, _), ts, params'), intr) = |
492 fun prove_intr2 (((_, _, us, _), ts, params'), intr) = |
491 EVERY (replicate (length params') (etac @{thm exE} 1)) THEN |
493 EVERY (replicate (length params') (etac @{thm exE} 1)) THEN |
492 EVERY (replicate (length ts + length us - 1) (etac @{thm conjE} 1)) THEN |
494 (if null ts andalso null us then rtac intr 1 |
493 Subgoal.FOCUS_PREMS (fn {params, prems, ...} => |
495 else |
494 let |
496 EVERY (replicate (length ts + length us - 1) (etac @{thm conjE} 1)) THEN |
495 val (eqs, prems') = chop (length us) prems; |
497 Subgoal.FOCUS_PREMS (fn {params, prems, ...} => |
496 val rew_thms = map (fn th => th RS @{thm eq_reflection}) eqs; |
498 let |
497 in |
499 val (eqs, prems') = chop (length us) prems; |
498 rewrite_goal_tac rew_thms 1 THEN |
500 val rew_thms = map (fn th => th RS @{thm eq_reflection}) eqs; |
499 rtac intr 1 THEN |
501 in |
500 EVERY (map (fn p => rtac p 1) prems') |
502 rewrite_goal_tac rew_thms 1 THEN |
501 end) ctxt' 1; |
503 rtac intr 1 THEN |
|
504 EVERY (map (fn p => rtac p 1) prems') |
|
505 end) ctxt' 1); |
502 in |
506 in |
503 Skip_Proof.prove ctxt' [] [] eq (fn _ => |
507 Skip_Proof.prove ctxt' [] [] eq (fn _ => |
504 rtac @{thm iffI} 1 THEN etac (#1 elim) 1 THEN |
508 rtac @{thm iffI} 1 THEN etac (#1 elim) 1 THEN |
505 EVERY (map_index prove_intr1 c_intrs) THEN |
509 EVERY (map_index prove_intr1 c_intrs) THEN |
506 (if null c_intrs then etac @{thm FalseE} 1 |
510 (if null c_intrs then etac @{thm FalseE} 1 |