let ACI_CONJ =
  let rec build ths tm =
    if is_conj tm then
      let l,r = dest_conj tm in CONJ (build ths l) (build ths r)
    else find (fun th -> concl th = tm) ths in
    fun p p' ->
      let cjs = CONJUNCTS(ASSUME p) and cjs' = CONJUNCTS(ASSUME p') in
      let th = build cjs p' and th' = build cjs' p in
        IMP_ANTISYM_RULE (DISCH_ALL th) (DISCH_ALL th');;

let QE_SIMPLIFY_CONV =
  
let NOT_EXISTS_UNIQUE_THM = 
prove (`~(?!x. P x) <=> (!x. ~P x) \/ ?x x'. P x /\ P x' /\ ~(x = x')`,
REWRITE_TAC[EXISTS_UNIQUE_THM; DE_MORGAN_THM; NOT_EXISTS_THM] THEN REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; CONJ_ASSOC]) in let tauts = [TAUT `~(~p) <=> p`; TAUT `~(p /\ q) <=> ~p \/ ~q`; TAUT `~(p \/ q) <=> ~p /\ ~q`; TAUT `~(p ==> q) <=> p /\ ~q`; TAUT `p ==> q <=> ~p \/ q`; NOT_FORALL_THM; NOT_EXISTS_THM; EXISTS_UNIQUE_THM; NOT_EXISTS_UNIQUE_THM; TAUT `~(p <=> q) <=> (p /\ ~q) \/ (~p /\ q)`; TAUT `(p <=> q) <=> (p /\ q) \/ (~p /\ ~q)`; TAUT `~(p /\ q \/ ~p /\ r) <=> p /\ ~q \/ ~p /\ ~r`] in GEN_REWRITE_CONV TOP_SWEEP_CONV tauts;;
let OR_ASSOC = TAUT `(a \/ b) \/ c <=> a \/ b \/ c`;;
let forall_thm = 
prove(`!P. (!x. P x) <=> ~ (?x. ~ P x)`,
MESON_TAC[]) and or_exists_conv = PURE_REWRITE_CONV[OR_EXISTS_THM] and triv_exists_conv = REWR_CONV EXISTS_SIMP and push_exists_conv = REWR_CONV RIGHT_EXISTS_AND_THM and not_tm = `(~)` and or_tm = `(\/)` and t_tm = `T` and f_tm = `F`;;
let LIFT_QELIM_CONV afn_conv nfn_conv qfn_conv = let rec qelift_conv vars fm = if fm = t_tm or fm = f_tm then REFL fm else if is_neg fm then let thm1 = qelift_conv vars (dest_neg fm) in MK_COMB(REFL not_tm,thm1) else if is_conj fm or is_disj fm or is_imp fm or is_iff fm then let (op,p,q) = get_binop fm in let thm1 = qelift_conv vars p in let thm2 = qelift_conv vars q in MK_COMB(MK_COMB((REFL op),thm1),thm2) else if is_forall fm then let (x,p) = dest_forall fm in let nex_thm = BETA_RULE (ISPEC (mk_abs(x,p)) forall_thm) in let nex_thm' = CONV_RULE (LAND_CONV (RAND_CONV (ALPHA_CONV x))) nex_thm in let nex_thm'' = CONV_RULE (RAND_CONV (RAND_CONV (RAND_CONV (ALPHA_CONV x)))) nex_thm' in let elim_thm = qelift_conv vars (mk_exists(x,mk_neg p)) in TRANS nex_thm'' (MK_COMB (REFL not_tm,elim_thm)) else if is_exists fm then let (x,p) = dest_exists fm in let thm1 = qelift_conv (x::vars) p in let thm1a = MK_EXISTS x thm1 in let thm1b = PURE_REWRITE_RULE[OR_ASSOC] thm1a in let thm2 = nfn_conv (rhs(concl thm1)) in let thm2a = MK_EXISTS x thm2 in let thm2b = PURE_REWRITE_RULE[OR_ASSOC] thm2a in let djs = disjuncts (rhs (concl thm2)) in let djthms = map (qelim x vars) djs in let thm3 = end_itlist (fun thm1 thm2 -> MK_COMB(MK_COMB (REFL or_tm,thm1),thm2)) djthms in let split_ex_thm = GSYM (or_exists_conv (lhs (concl thm3))) in let thm3a = TRANS split_ex_thm thm3 in TRANS (TRANS thm1b thm2b) thm3a else afn_conv vars fm and qelim x vars p = let cjs = conjuncts p in let ycjs,ncjs = partition (mem x o frees) cjs in if ycjs = [] then triv_exists_conv(mk_exists(x,p)) else if ncjs = [] then qfn_conv vars (mk_exists(x,p)) else let th1 = ACI_CONJ p (mk_conj(list_mk_conj ncjs,list_mk_conj ycjs)) in let th2 = CONV_RULE (RAND_CONV push_exists_conv) (MK_EXISTS x th1) in let t1,t2 = dest_comb (rand(concl th2)) in TRANS th2 (AP_TERM t1 (qfn_conv vars t2)) in fun fm -> ((qelift_conv (frees fm)) THENC QE_SIMPLIFY_CONV) fm;; (* let afn_conv,nfn_conv,qfn_conv = POLYATOM_CONV,(EVALC_CONV THENC SIMPLIFY_CONV),BASIC_REAL_QELIM_CONV let LIFT_QELIM_CONV afn_conv nfn_conv qfn_conv = fun fm -> ((qelift_conv (frees fm)) THENC QE_SIMPLIFY_CONV) fm;; let k0 = (TRANS thm1a thm2a) let k1 = thm3a let k2 = CONV_RULE (LAND_CONV (RAND_CONV (ALPHA_CONV `x:real`))) k1 TRANS k0 k2 let vars = [] let fm,vars = !lqc_fm,!lqc_vars let fm = `?x y z. x * y * z < &0` let p = `~((&0 + y * (&0 + x * &1) = &0) <=> (&0 + x * &1 = &0) \/ (&0 + y * &1 = &0))` #trace qelift_conv #trace qelim TRANS (ASSUME `T <=> (?x. x * y > &0)`) (ASSUME `(?z. z * y > &0) <=> F`) MATCH_TRANS (ASSUME `T <=> (?x. x * y > &0)`) (ASSUME `?z. z * y > &0 <=> F`) MATCH_EQ_MP (ASSUME `(?x. x * y > &0) <=> F`) (ASSUME `?z. z * y > &0`) qelift_conv vars fm let fm = `?x y. x * y = &0` let fm = `!y. (x * y = &0) <=> (x = &0) \/ (y = &0)` let fm = `?y. (x * y = &0) <=> (x = &0) \/ (y = &0)` let fm = `?y. ~ ((x * y = &0) <=> (x = &0) \/ (y = &0))` let fm = `?x. ~(!y. (x * y = &0) <=> (x = &0) \/ (y = &0))` let vars = [ry;rx] let vars = [rx] let QELIM_DLO_CONV = (LIFT_QELIM_CONV AFN_DLO_CONV ((CNNF_CONV LFN_DLO_CONV) THENC DNF_CONV) (fun v -> DLOBASIC_CONV)) THENC (REWRITE_CONV[]);; *)