equal
deleted
inserted
replaced
1051 |
1051 |
1052 fun mk_partial_rules provedgoal = |
1052 fun mk_partial_rules provedgoal = |
1053 let |
1053 let |
1054 val newthy = theory_of_thm provedgoal (*FIXME*) |
1054 val newthy = theory_of_thm provedgoal (*FIXME*) |
1055 |
1055 |
1056 val (graph_is_function, complete_thm) = |
1056 val ((graph_is_function, complete_thm), graph_is_eqvt) = |
1057 provedgoal |
1057 provedgoal |
1058 |> fst o Conjunction.elim |
|
1059 |> fst o Conjunction.elim |
|
1060 |> Conjunction.elim |
1058 |> Conjunction.elim |
1061 |> apfst (Thm.forall_elim_vars 0) |
1059 |>> fst o Conjunction.elim |
|
1060 |>> Conjunction.elim |
|
1061 |>> apfst (Thm.forall_elim_vars 0) |
1062 |
1062 |
1063 val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff) |
1063 val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff) |
1064 |
1064 val f_eqvt = graph_is_function RS (graph_is_eqvt RS (f_defthm RS @{thm fundef_ex1_eqvt})) |
1065 val f_eqvt = graph_is_function RS (G_eqvt RS (f_defthm RS @{thm fundef_ex1_eqvt})) |
|
1066 |
1065 |
1067 val psimps = PROFILE "Proving simplification rules" |
1066 val psimps = PROFILE "Proving simplification rules" |
1068 (mk_psimps newthy globals R xclauses values f_iff) graph_is_function |
1067 (mk_psimps newthy globals R xclauses values f_iff) graph_is_function |
1069 |
1068 |
1070 val simple_pinduct = PROFILE "Proving partial induction rule" |
1069 val simple_pinduct = PROFILE "Proving partial induction rule" |