681 val cert = Thm.cterm_of defs_thy; |
681 val cert = Thm.cterm_of defs_thy; |
682 |
682 |
683 val intro = Goal.prove_global defs_thy [] norm_ts statement |
683 val intro = Goal.prove_global defs_thy [] norm_ts statement |
684 (fn {context = ctxt, ...} => |
684 (fn {context = ctxt, ...} => |
685 rewrite_goals_tac ctxt [pred_def] THEN |
685 rewrite_goals_tac ctxt [pred_def] THEN |
686 compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN |
686 compose_tac defs_ctxt (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN |
687 compose_tac (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1); |
687 compose_tac defs_ctxt |
|
688 (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1); |
688 |
689 |
689 val conjuncts = |
690 val conjuncts = |
690 (Drule.equal_elim_rule2 OF |
691 (Drule.equal_elim_rule2 OF |
691 [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (cert statement))]) |
692 [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (cert statement))]) |
692 |> Conjunction.elim_balanced (length ts); |
693 |> Conjunction.elim_balanced (length ts); |
693 |
694 |
694 val (_, axioms_ctxt) = defs_ctxt |
695 val (_, axioms_ctxt) = defs_ctxt |
695 |> Assumption.add_assumes (maps (#hyps o Thm.crep_thm) (defs @ conjuncts)); |
696 |> Assumption.add_assumes (maps (#hyps o Thm.crep_thm) (defs @ conjuncts)); |
696 val axioms = ts ~~ conjuncts |> map (fn (t, ax) => |
697 val axioms = ts ~~ conjuncts |> map (fn (t, ax) => |
697 Element.prove_witness axioms_ctxt t |
698 Element.prove_witness axioms_ctxt t |
698 (rewrite_goals_tac axioms_ctxt defs THEN compose_tac (false, ax, 0) 1)); |
699 (rewrite_goals_tac axioms_ctxt defs THEN compose_tac axioms_ctxt (false, ax, 0) 1)); |
699 in ((statement, intro, axioms), defs_thy) end; |
700 in ((statement, intro, axioms), defs_thy) end; |
700 |
701 |
701 in |
702 in |
702 |
703 |
703 (* main predicate definition function *) |
704 (* main predicate definition function *) |