Rqe/simplify.ml

   1 (* ---------------------------------------------------------------------- *)
   2 (*  Simplification                                                        *)
   3 (* ---------------------------------------------------------------------- *)
   4
   5 (*
   6 let psimplify1 fm =
   7   match fm with
   8     Not False -> True
   9   | Not True -> False
  10   | And(False,q) -> False
  11   | And(p,False) -> False
  12   | And(True,q) -> q
  13   | And(p,True) -> p
  14   | Or(False,q) -> q
  15   | Or(p,False) -> p
  16   | Or(True,q) -> True
  17   | Or(p,True) -> True
  18   | Imp(False,q) -> True
  19   | Imp(True,q) -> q
  20   | Imp(p,True) -> True
  21   | Imp(p,False) -> Not p
  22   | Iff(True,q) -> q
  23   | Iff(p,True) -> p
  24   | Iff(False,q) -> Not q
  25   | Iff(p,False) -> Not p
  26   | _ -> fm;;
  27 *)
  28
  29
  30 let PSIMPLIFY1_CONV =
  31   let nt = `~T`
  32   and t = `T`
  33   and f = `F`
  34   and nf = `~F` in
  35   fun fm ->
  36   try
  37     let fm' =
  38       if fm = nt then f
  39       else if fm = nf then t
  40       else if is_conj fm then
  41         let l,r = dest_conj fm in
  42           if l = f or r = f then f
  43           else if l = t then r
  44           else if r = t then l
  45           else fm
  46       else if is_disj fm then
  47         let l,r = dest_disj fm in
  48           if l = t or r = t then t
  49           else if l = f then r
  50           else if r = f then l
  51           else fm
  52       else if is_imp fm then
  53         let l,r = dest_imp fm in
  54           if l = f then t
  55           else if r = t then t
  56           else if l = t then r
  57           else if r = f then mk_neg l
  58           else fm
  59       else if is_iff fm then
  60         let l,r = dest_beq fm in
  61           if l = f then mk_neg r
  62           else if l = t then r
  63           else if r = t then l
  64           else if r = f then mk_neg l
  65             else fm
  66       else failwith "PSIMPLIFY: 0" in
  67     let fm'' = mk_eq(fm,fm') in
  68       prove(fm'',REWRITE_TAC[])
  69   with _ -> REFL fm;;
  70
  71 (*
  72 let fm = `T /\ T`
  73 PSIMPLIFY1_CONV `T /\ A`
  74
  75 let simplify1 fm =
  76   match fm with
  77     Forall(x,p) -> if mem x (fv p) then fm else p
  78   | Exists(x,p) -> if mem x (fv p) then fm else p
  79   | _ -> psimplify1 fm;;
  80 *)
  81
  82 let SIMPLIFY1_CONV fm =
  83   if is_forall fm or is_exists fm then
  84     let x,p = dest_forall fm in
  85       if mem x (frees p) then REFL fm
  86       else  prove(mk_eq(fm,p),REWRITE_TAC[])
  87   else PSIMPLIFY1_CONV fm;;
  88
  89 (*
  90 let rec simplify fm =
  91   match fm with
  92     Not p -> simplify1 (Not(simplify p))
  93   | And(p,q) -> simplify1 (And(simplify p,simplify q))
  94   | Or(p,q) -> simplify1 (Or(simplify p,simplify q))
  95   | Imp(p,q) -> simplify1 (Imp(simplify p,simplify q))
  96   | Iff(p,q) -> simplify1 (Iff(simplify p,simplify q))
  97   | Forall(x,p) -> simplify1(Forall(x,simplify p))
  98   | Exists(x,p) -> simplify1(Exists(x,simplify p))
  99   | _ -> fm;;
 100 *)
 101
 102 let rec SIMPLIFY_CONV =
 103   let not_tm = `(~)`
 104   and ex_tm = `(?)` in
 105   fun fm ->
 106   if is_neg fm then
 107     let thm1 = SIMPLIFY_CONV (dest_neg fm) in
 108     let thm2 = AP_TERM not_tm thm1 in
 109     let l,r = dest_eq (concl thm2) in
 110     let thm3 = SIMPLIFY1_CONV r in
 111       TRANS thm2 thm3
 112   else if is_conj fm or is_disj fm or is_imp fm or is_iff fm then
 113     let op,l,r = get_binop fm in
 114     let l_thm = SIMPLIFY_CONV l in
 115     let r_thm = SIMPLIFY_CONV r in
 116     let a_thm = (curry MK_COMB) (AP_TERM op l_thm) r_thm in
 117     let al,ar = dest_eq (concl a_thm) in
 118     let thm = SIMPLIFY1_CONV ar in
 119       TRANS a_thm thm
 120   else if is_forall fm or is_exists fm then
 121     let x,bod = dest_quant fm in
 122     let bod_thm = SIMPLIFY_CONV bod in
 123     let lam_thm = ABS x bod_thm in
 124     let q_thm = AP_TERM ex_tm lam_thm in
 125     let l,r = dest_eq (concl q_thm) in
 126     let thm = SIMPLIFY1_CONV r in
 127       TRANS q_thm thm
 128   else REFL fm;;
 129
 130
 131
 132 (*
 133
 134 SIMPLIFY_CONV `T /\ T \/ F`
 135
 136 let operations =
 137   ["=",(=/); "<",(</); ">",(>/); "<=",(<=/); ">=",(>=/);
 138    "divides",(fun x y -> mod_num y x =/ Int 0)];;
 139
 140 let evalc_atom at =
 141   match at with
 142     R(p,[s;t]) ->
 143         (try if assoc p operations (dest_numeral s) (dest_numeral t)
 144              then True else False
 145          with Failure _ -> Atom at)
 146   | _ -> Atom at;;
 147
 148 let evalc = onatoms evalc_atom;;
 149 *)
 150
 151 let REAL_LEAF_CONV fm =
 152   let op,l,r = get_binop fm in
 153     if op = rlt then
 154       REAL_RAT_LT_CONV fm
 155     else if op = rgt then
 156       REAL_RAT_GT_CONV fm
 157     else if op = rle then
 158       REAL_RAT_LE_CONV fm
 159     else if op = rge then
 160       REAL_RAT_GE_CONV fm
 161     else if op = req then
 162       REAL_RAT_EQ_CONV fm
 163     else failwith "REAL_LEAF_CONV";;
 164
 165 let EVALC_CONV = DEPTH_CONV REAL_LEAF_CONV;;
 166
 167
 168
 169
 170
 171 (*
 172 EVALC_CONV `x < &0 /\ &1 < &2`
 173 (EVALC_CONV THENC SIMPLIFY_CONV) `(&0 + a * &1 = &0) /\
 174      ((&0 + b * &1 = &0) /\
 175       ((&0 + c * &1 = &0) /\ T \/
 176        &0 + c * &1 < &0 /\ F \/
 177        &0 + c * &1 > &0 /\ F) \/
 178       &0 + b * &1 < &0 /\ T \/
 179       &0 + b * &1 > &0 /\ T) \/
 180      &0 + a * &1 < &0 /\
 181      ((&0 + a * ((&0 + b * (&0 + b * -- &1)) + a * (&0 + c * &4)) = &0) /\ T \/
 182       &0 + a * ((&0 + b * (&0 + b * -- &1)) + a * (&0 + c * &4)) < &0 /\ F \/
 183       &0 + a * ((&0 + b * (&0 + b * -- &1)) + a * (&0 + c * &4)) > &0 /\ T) \/
 184      &0 + a * &1 > &0 /\
 185      ((&0 + a * ((&0 + b * (&0 + b * -- &1)) + a * (&0 + c * &4)) = &0) /\ T \/
 186       &0 + a * ((&0 + b * (&0 + b * -- &1)) + a * (&0 + c * &4)) < &0 /\ T \/
 187       &0 + a * ((&0 + b * (&0 + b * -- &1)) + a * (&0 + c * &4)) > &0 /\ &1 < &2)`
 188
 189 *)