examples/HolCheck/lzConv.sml

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)))