66 val (mp1, mp2) = (get_p1 th_1, get_p1 th_1') |
66 val (mp1, mp2) = (get_p1 th_1, get_p1 th_1') |
67 val (pp1, pp2) = (get_p1 th_2, get_p1 th_2') |
67 val (pp1, pp2) = (get_p1 th_2, get_p1 th_2') |
68 fun fw mi th th' th'' = |
68 fun fw mi th th' th'' = |
69 let |
69 let |
70 val th0 = if mi then |
70 val th0 = if mi then |
71 Drule.instantiate_normalize ([],[(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th |
71 Drule.instantiate_normalize (TVars.empty, Vars.make [(p1_v, p1),(p2_v, p2),(mp1_v, mp1), (mp2_v, mp2)]) th |
72 else Drule.instantiate_normalize ([],[(p1_v, p1),(p2_v, p2),(mp1_v, pp1), (mp2_v, pp2)]) th |
72 else Drule.instantiate_normalize (TVars.empty, Vars.make [(p1_v, p1),(p2_v, p2),(mp1_v, pp1), (mp2_v, pp2)]) th |
73 in Thm.implies_elim (Thm.implies_elim th0 th') th'' end |
73 in Thm.implies_elim (Thm.implies_elim th0 th') th'' end |
74 in (fw true th1 th_1 th_1', fw false th2 th_2 th_2', |
74 in (fw true th1 th_1 th_1', fw false th2 th_2 th_2', |
75 fw true th3 th_3 th_3', fw false th4 th_4 th_4', fw true th5 th_5 th_5') |
75 fw true th3 th_3 th_3', fw false th4 th_4 th_4', fw true th5 th_5 th_5') |
76 end |
76 end |
77 val U_v = dest_Var (Thm.term_of (Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 (Thm.cprop_of qe))))) |
77 val U_v = dest_Var (Thm.term_of (Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 (Thm.cprop_of qe))))) |
113 val [minf_conj, minf_disj, minf_eq, minf_neq, minf_lt, |
113 val [minf_conj, minf_disj, minf_eq, minf_neq, minf_lt, |
114 minf_le, minf_gt, minf_ge, minf_P] = minf |
114 minf_le, minf_gt, minf_ge, minf_P] = minf |
115 val [pinf_conj, pinf_disj, pinf_eq, pinf_neq, pinf_lt, |
115 val [pinf_conj, pinf_disj, pinf_eq, pinf_neq, pinf_lt, |
116 pinf_le, pinf_gt, pinf_ge, pinf_P] = pinf |
116 pinf_le, pinf_gt, pinf_ge, pinf_P] = pinf |
117 val [nmi_conj, nmi_disj, nmi_eq, nmi_neq, nmi_lt, |
117 val [nmi_conj, nmi_disj, nmi_eq, nmi_neq, nmi_lt, |
118 nmi_le, nmi_gt, nmi_ge, nmi_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) nmi |
118 nmi_le, nmi_gt, nmi_ge, nmi_P] = map (Drule.instantiate_normalize (TVars.empty, Vars.make [(U_v,cU)])) nmi |
119 val [npi_conj, npi_disj, npi_eq, npi_neq, npi_lt, |
119 val [npi_conj, npi_disj, npi_eq, npi_neq, npi_lt, |
120 npi_le, npi_gt, npi_ge, npi_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) npi |
120 npi_le, npi_gt, npi_ge, npi_P] = map (Drule.instantiate_normalize (TVars.empty, Vars.make [(U_v,cU)])) npi |
121 val [ld_conj, ld_disj, ld_eq, ld_neq, ld_lt, |
121 val [ld_conj, ld_disj, ld_eq, ld_neq, ld_lt, |
122 ld_le, ld_gt, ld_ge, ld_P] = map (Drule.instantiate_normalize ([],[(U_v,cU)])) ld |
122 ld_le, ld_gt, ld_ge, ld_P] = map (Drule.instantiate_normalize (TVars.empty, Vars.make [(U_v,cU)])) ld |
123 |
123 |
124 fun decomp_mpinf fm = |
124 fun decomp_mpinf fm = |
125 case Thm.term_of fm of |
125 case Thm.term_of fm of |
126 Const(\<^const_name>\<open>HOL.conj\<close>,_)$_$_ => |
126 Const(\<^const_name>\<open>HOL.conj\<close>,_)$_$_ => |
127 let val (p,q) = Thm.dest_binop fm |
127 let val (p,q) = Thm.dest_binop fm |