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