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
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');;
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
18 TAUT `~(p /\ q) <=> ~p \/ ~q`;
19 TAUT `~(p \/ q) <=> ~p /\ ~q`;
20 TAUT `~(p ==> q) <=> p /\ ~q`;
21 TAUT `p ==> q <=> ~p \/ q`;
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;;
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
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
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
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;;
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;;
95 let k0 = (TRANS thm1a thm2a)
97 let k2 = CONV_RULE (LAND_CONV (RAND_CONV (ALPHA_CONV `x:real`))) k1
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))`
110 TRANS (ASSUME `T <=> (?x. x * y > &0)`) (ASSUME `(?z. z * y > &0) <=> F`)
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`)
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))`
127 (LIFT_QELIM_CONV AFN_DLO_CONV ((CNNF_CONV LFN_DLO_CONV) THENC DNF_CONV)
128 (fun v -> DLOBASIC_CONV)) THENC (REWRITE_CONV[]);;