575 |> Thm.forall_elim_vars 0 |
575 |> Thm.forall_elim_vars 0 |
576 |> fold (curry op COMP) ex1s |
576 |> fold (curry op COMP) ex1s |
577 |> Thm.implies_intr (ihyp) |
577 |> Thm.implies_intr (ihyp) |
578 |> Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x))) |
578 |> Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x))) |
579 |> Thm.forall_intr (cterm_of thy x) |
579 |> Thm.forall_intr (cterm_of thy x) |
580 |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *) |
580 |> (fn it => Drule.compose (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *) |
581 |> (fn it => fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it) |
581 |> (fn it => fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it) |
582 |
582 |
583 val goalstate = |
583 val goalstate = |
584 Conjunction.intr (Conjunction.intr (Conjunction.intr graph_is_function complete) invariant) G_eqvt |
584 Conjunction.intr (Conjunction.intr (Conjunction.intr graph_is_function complete) invariant) G_eqvt |
585 |> Thm.close_derivation |
585 |> Thm.close_derivation |
586 |> Goal.protect |
586 |> Goal.protect 0 |
587 |> fold_rev (Thm.implies_intr o cprop_of) compat |
587 |> fold_rev (Thm.implies_intr o cprop_of) compat |
588 |> Thm.implies_intr (cprop_of complete) |
588 |> Thm.implies_intr (cprop_of complete) |
589 |> Thm.implies_intr (cprop_of invariant) |
589 |> Thm.implies_intr (cprop_of invariant) |
590 |> Thm.implies_intr (cprop_of G_eqvt) |
590 |> Thm.implies_intr (cprop_of G_eqvt) |
591 in |
591 in |
968 |> Thm.implies_intr R_z_x |
968 |> Thm.implies_intr R_z_x |
969 |> Thm.forall_intr (cterm_of thy z) |
969 |> Thm.forall_intr (cterm_of thy z) |
970 |> (fn it => it COMP accI) |
970 |> (fn it => it COMP accI) |
971 |> Thm.implies_intr ihyp |
971 |> Thm.implies_intr ihyp |
972 |> Thm.forall_intr (cterm_of thy x) |
972 |> Thm.forall_intr (cterm_of thy x) |
973 |> (fn it => Drule.compose_single(it,2,wf_induct_rule)) |
973 |> (fn it => Drule.compose (it, 2, wf_induct_rule)) |
974 |> curry op RS (Thm.assume wfR') |
974 |> curry op RS (Thm.assume wfR') |
975 |> forall_intr_vars |
975 |> forall_intr_vars |
976 |> (fn it => it COMP allI) |
976 |> (fn it => it COMP allI) |
977 |> fold Thm.implies_intr hyps |
977 |> fold Thm.implies_intr hyps |
978 |> Thm.implies_intr wfR' |
978 |> Thm.implies_intr wfR' |