Rqe/lift_qelim.ml

   1 let ACI_CONJ =
   2   let rec build ths tm =
   3     if is_conj tm then
   4       let l,r = dest_conj tm in CONJ (build ths l) (build ths r)
   5     else find (fun th -> concl th = tm) ths in
   6     fun p p' ->
   7       let cjs = CONJUNCTS(ASSUME p) and cjs' = CONJUNCTS(ASSUME p') in
   8       let th = build cjs p' and th' = build cjs' p in
   9         IMP_ANTISYM_RULE (DISCH_ALL th) (DISCH_ALL th');;
  10
  11 let QE_SIMPLIFY_CONV =
  12   let NOT_EXISTS_UNIQUE_THM = prove
  13    (`~(?!x. P x) <=> (!x. ~P x) \/ ?x x'. P x /\ P x' /\ ~(x = x')`,
  14     REWRITE_TAC[EXISTS_UNIQUE_THM; DE_MORGAN_THM; NOT_EXISTS_THM] THEN
  15     REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; CONJ_ASSOC]) in
  16   let tauts =
  17     [TAUT `~(~p) <=> p`;
  18      TAUT `~(p /\ q) <=> ~p \/ ~q`;
  19      TAUT `~(p \/ q) <=> ~p /\ ~q`;
  20      TAUT `~(p ==> q) <=> p /\ ~q`;
  21      TAUT `p ==> q <=> ~p \/ q`;
  22      NOT_FORALL_THM;
  23      NOT_EXISTS_THM;
  24      EXISTS_UNIQUE_THM;
  25      NOT_EXISTS_UNIQUE_THM;
  26      TAUT `~(p <=> q) <=> (p /\ ~q) \/ (~p /\ q)`;
  27      TAUT `(p <=> q) <=> (p /\ q) \/ (~p /\ ~q)`;
  28      TAUT `~(p /\ q \/ ~p /\ r) <=> p /\ ~q \/ ~p /\ ~r`] in
  29   GEN_REWRITE_CONV TOP_SWEEP_CONV tauts;;
  30
  31 let OR_ASSOC = TAUT `(a \/ b) \/ c <=> a \/ b \/ c`;;
  32 let forall_thm = prove(`!P. (!x. P x) <=> ~ (?x. ~ P x)`,MESON_TAC[])
  33 and or_exists_conv = PURE_REWRITE_CONV[OR_EXISTS_THM]
  34 and triv_exists_conv = REWR_CONV EXISTS_SIMP
  35 and push_exists_conv = REWR_CONV RIGHT_EXISTS_AND_THM
  36 and not_tm = `(~)`
  37 and or_tm = `(\/)`
  38 and t_tm = `T`
  39 and f_tm = `F`;;
  40
  41 let LIFT_QELIM_CONV afn_conv nfn_conv qfn_conv =
  42   let rec qelift_conv vars fm =
  43     if fm = t_tm or fm = f_tm then REFL fm
  44     else if is_neg fm then
  45       let thm1 = qelift_conv vars (dest_neg fm) in
  46         MK_COMB(REFL not_tm,thm1)
  47     else if is_conj fm or is_disj fm or is_imp fm or is_iff fm then
  48       let (op,p,q) = get_binop fm in
  49       let thm1 = qelift_conv vars p in
  50       let thm2 = qelift_conv vars q in
  51         MK_COMB(MK_COMB((REFL op),thm1),thm2)
  52     else if is_forall fm then
  53       let (x,p) = dest_forall fm in
  54       let nex_thm = BETA_RULE (ISPEC (mk_abs(x,p)) forall_thm) in
  55       let nex_thm' = CONV_RULE (LAND_CONV (RAND_CONV (ALPHA_CONV x))) nex_thm in
  56       let nex_thm'' = CONV_RULE (RAND_CONV (RAND_CONV (RAND_CONV (ALPHA_CONV x)))) nex_thm' in
  57       let elim_thm = qelift_conv vars (mk_exists(x,mk_neg p)) in
  58         TRANS nex_thm'' (MK_COMB (REFL not_tm,elim_thm))
  59     else if is_exists fm then
  60       let (x,p) = dest_exists fm in
  61       let thm1 = qelift_conv (x::vars) p in
  62       let thm1a = MK_EXISTS x thm1 in
  63       let thm1b = PURE_REWRITE_RULE[OR_ASSOC] thm1a in
  64       let thm2 = nfn_conv (rhs(concl thm1)) in
  65       let thm2a = MK_EXISTS x thm2 in
  66       let thm2b = PURE_REWRITE_RULE[OR_ASSOC] thm2a in
  67       let djs = disjuncts (rhs (concl thm2)) in
  68       let djthms = map (qelim x vars) djs in
  69       let thm3 = end_itlist
  70         (fun thm1 thm2 -> MK_COMB(MK_COMB (REFL or_tm,thm1),thm2)) djthms in
  71       let split_ex_thm = GSYM (or_exists_conv (lhs (concl thm3))) in
  72       let thm3a = TRANS split_ex_thm thm3 in
  73         TRANS (TRANS thm1b thm2b) thm3a
  74     else
  75       afn_conv vars fm
  76   and qelim x vars p =
  77     let cjs = conjuncts p in
  78     let ycjs,ncjs = partition (mem x o frees) cjs in
  79     if ycjs = [] then triv_exists_conv(mk_exists(x,p))
  80     else if ncjs = [] then qfn_conv vars (mk_exists(x,p)) else
  81     let th1 = ACI_CONJ p (mk_conj(list_mk_conj ncjs,list_mk_conj ycjs)) in
  82     let th2 = CONV_RULE (RAND_CONV push_exists_conv) (MK_EXISTS x th1) in
  83     let t1,t2 = dest_comb (rand(concl th2)) in
  84     TRANS th2 (AP_TERM t1 (qfn_conv vars t2)) in
  85   fun fm -> ((qelift_conv (frees fm)) THENC QE_SIMPLIFY_CONV) fm;;
  86
  87
  88
  89 (*
  90 let afn_conv,nfn_conv,qfn_conv = POLYATOM_CONV,(EVALC_CONV THENC SIMPLIFY_CONV),BASIC_REAL_QELIM_CONV
  91 let LIFT_QELIM_CONV afn_conv nfn_conv qfn_conv =
  92   fun fm -> ((qelift_conv (frees fm)) THENC QE_SIMPLIFY_CONV) fm;;
  93
  94
  95 let k0 = (TRANS thm1a thm2a)
  96 let k1 = thm3a
  97 let k2 = CONV_RULE (LAND_CONV (RAND_CONV (ALPHA_CONV `x:real`))) k1
  98 TRANS k0 k2
  99
 100
 101 let vars = []
 102 let fm,vars = !lqc_fm,!lqc_vars
 103 let fm = `?x y z. x * y * z < &0`
 104 let p = `~((&0 + y * (&0 + x * &1) = &0) <=> (&0 + x * &1 = &0) \/ (&0 + y * &1 = &0))`
 105 #trace qelift_conv
 106 #trace qelim
 107
 108
 109
 110 TRANS (ASSUME `T <=> (?x. x * y > &0)`) (ASSUME `(?z. z * y > &0) <=> F`)
 111
 112 MATCH_TRANS (ASSUME `T <=> (?x. x * y > &0)`) (ASSUME `?z. z * y > &0 <=> F`)
 113 MATCH_EQ_MP (ASSUME `(?x. x * y > &0) <=> F`) (ASSUME `?z. z * y > &0`)
 114
 115 qelift_conv vars fm
 116
 117
 118 let fm = `?x y. x * y = &0`
 119 let fm = `!y. (x * y = &0) <=> (x = &0) \/ (y = &0)`
 120 let fm = `?y. (x * y = &0) <=> (x = &0) \/ (y = &0)`
 121 let fm = `?y. ~ ((x * y = &0) <=> (x = &0) \/ (y = &0))`
 122 let fm = `?x. ~(!y. (x * y = &0) <=> (x = &0) \/ (y = &0))`
 123 let vars = [ry;rx]
 124 let vars = [rx]
 125
 126 let QELIM_DLO_CONV =
 127   (LIFT_QELIM_CONV AFN_DLO_CONV ((CNNF_CONV LFN_DLO_CONV) THENC DNF_CONV)
 128     (fun v -> DLOBASIC_CONV)) THENC (REWRITE_CONV[]);;
 129 *)