equal
deleted
inserted
replaced
669 Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN |
669 Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN |
670 Tactic.compose_tac (false, |
670 Tactic.compose_tac (false, |
671 Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1); |
671 Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1); |
672 |
672 |
673 val conjuncts = |
673 val conjuncts = |
674 (Drule.equal_elim_rule2 OF [body_eq, |
674 (Drule.equal_elim_rule2 OF [body_eq, rewrite_rule [pred_def] (Thm.assume (cert statement))]) |
675 Raw_Simplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))]) |
|
676 |> Conjunction.elim_balanced (length ts); |
675 |> Conjunction.elim_balanced (length ts); |
677 val axioms = ts ~~ conjuncts |> map (fn (t, ax) => |
676 val axioms = ts ~~ conjuncts |> map (fn (t, ax) => |
678 Element.prove_witness defs_ctxt t |
677 Element.prove_witness defs_ctxt t |
679 (rewrite_goals_tac defs THEN |
678 (rewrite_goals_tac defs THEN |
680 Tactic.compose_tac (false, ax, 0) 1)); |
679 Tactic.compose_tac (false, ax, 0) 1)); |