664 |
664 |
665 val cert = Thm.cterm_of defs_thy; |
665 val cert = Thm.cterm_of defs_thy; |
666 |
666 |
667 val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ => |
667 val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ => |
668 rewrite_goals_tac [pred_def] THEN |
668 rewrite_goals_tac [pred_def] THEN |
669 Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN |
669 compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN |
670 Tactic.compose_tac (false, |
670 compose_tac (false, 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 |
671 |
673 val conjuncts = |
672 val conjuncts = |
674 (Drule.equal_elim_rule2 OF [body_eq, rewrite_rule [pred_def] (Thm.assume (cert statement))]) |
673 (Drule.equal_elim_rule2 OF [body_eq, rewrite_rule [pred_def] (Thm.assume (cert statement))]) |
675 |> Conjunction.elim_balanced (length ts); |
674 |> Conjunction.elim_balanced (length ts); |
676 val axioms = ts ~~ conjuncts |> map (fn (t, ax) => |
675 val axioms = ts ~~ conjuncts |> map (fn (t, ax) => |
677 Element.prove_witness defs_ctxt t |
676 Element.prove_witness defs_ctxt t |
678 (rewrite_goals_tac defs THEN |
677 (rewrite_goals_tac defs THEN compose_tac (false, ax, 0) 1)); |
679 Tactic.compose_tac (false, ax, 0) 1)); |
|
680 in ((statement, intro, axioms), defs_thy) end; |
678 in ((statement, intro, axioms), defs_thy) end; |
681 |
679 |
682 in |
680 in |
683 |
681 |
684 (* main predicate definition function *) |
682 (* main predicate definition function *) |