Lines Matching defs:ant
1090 val {ant,conseq} = dest_imp Body handle HOL_ERR _ => raise FI_ERR
1091 val fant = free_in Bvar ant
1098 if fant then boolSyntax.mk_imp(boolSyntax.mk_exists(Bvar,ant),conseq)
1099 else if fconseq then boolSyntax.mk_imp(ant,boolSyntax.mk_forall(Bvar,conseq))
1100 else boolSyntax.mk_imp(boolSyntax.mk_exists(Bvar,ant),boolSyntax.mk_forall(Bvar,conseq))
1120 let val {ant, ...} = dest_imp tm
1121 val {Bvar,Body} = dest_exists ant
1124 val th1 = GEN x' (DISCH t'(MP(ASSUME tm)(EXISTS(ant,x')(ASSUME t'))))
1126 val th2 = CHOOSE (x',ASSUME ant) (UNDISCH(SPEC x'(ASSUME rtm)))
1128 IMP_ANTISYM_RULE (DISCH tm th1) (DISCH rtm (DISCH ant th2))
1140 let val {ant,conseq} = dest_imp tm
1144 val imp1 = DISCH tm (GEN x' (DISCH ant(SPEC x'(UNDISCH(ASSUME tm)))))
1148 val imp2 = DISCH ctm (DISCH ant thm1)
1168 val {ant = P,conseq = Q} = dest_imp Body handle HOL_ERR _ => raise EI_ERR
1231 let val {ant,conseq} = dest_imp tm
1232 val {Bvar,Body} = dest_forall ant
1236 val th1 = SPEC x' (ASSUME ant)
1237 val new_imp = mk_imp{ant = t1', conseq = conseq}
1240 val imp1 = DISCH otm (CHOOSE(x',ASSUME otm)(DISCH ant thm1))
1245 val th3 = CCONTR nex (MP(ASSUME(mk_neg ant)) (GEN x' th2))
1249 val thm6 = DISJ_CASES (SPEC ant EXCLUDED_MIDDLE) thm2 thm5
1263 let val {ant,conseq} = dest_imp tm
1267 val new_imp = mk_imp{ant = ant, conseq = t2'}
1270 val imp1 = DISCH otm (CHOOSE(x',ASSUME otm) (DISCH ant thm1))
1272 val thm3 = CHOOSE (x',thm2) (EXISTS (otm,x') (DISCH ant (ASSUME t2')))
1273 val thm4 = DISCH ant (CONTR t2'(UNDISCH(ASSUME(mk_neg ant))))
1275 val thm6 = DISJ_CASES (SPEC ant EXCLUDED_MIDDLE) thm3 thm5
1489 let val {ant,conseq} = dest_imp tm
1491 and contra = mk_imp{ant = mk_neg conseq, conseq = mk_neg ant}
1493 and imp2 = DISCH ant (CCONTR conseq (UNDISCH (UNDISCH (ASSUME contra))))
1510 let val {ant,conseq} = dest_imp tm
1511 val {conj1,conj2} = dest_conj ant
1512 val ant_thm = ASSUME ant
1515 (ASSUME (mk_imp{ant=conj1,
1516 conseq=mk_imp{ant=conj2, conseq=conseq}}))
1520 (DISCH_ALL (DISCH ant imp2))
1601 let val {ant,conseq} = dest_imp imp
1602 val ant' = MK_BIN AND (handle_ant (dest_conj ant))
1604 (MK_ALL oy ny (MK_BIN IMP (ant',REFL conseq)))