Rqe/testform.ml

   1 (* ====================================================================== *)
   2 (*  TESTFORM                                                              *)
   3 (* ====================================================================== *)
   4
   5 let rec TESTFORM var interpsigns_thm set_thm fm =
   6   let polys,set,signs = dest_interpsigns interpsigns_thm in
   7   let polys' = dest_list polys in
   8   let signs' = dest_list signs in
   9   if fm = t_tm then BETA_RULE (ISPECL [set] t_thm)
  10   else if fm = f_tm then BETA_RULE (ISPECL [set] f_thm)
  11   else if is_neg fm then
  12     let lam = mk_abs (var,dest_neg fm) in
  13     let thm = TESTFORM var interpsigns_thm set_thm (dest_neg fm) in
  14     if is_pos (concl thm) then
  15       MATCH_MP (BETA_RULE (ISPECL [lam;set] neg_thm_p)) thm
  16     else if is_neg (concl thm) then
  17       MATCH_MP (BETA_RULE (ISPECL [lam;set] neg_thm_n)) thm
  18     else failwith "error"
  19   else if is_conj fm then
  20     let a,b = dest_conj fm in
  21     let a',b' = mk_abs (var,a),mk_abs (var,b) in
  22     let thma = TESTFORM var interpsigns_thm set_thm a  in
  23     let thmb = TESTFORM var interpsigns_thm set_thm b  in
  24     if is_neg (concl thma) && is_neg (concl thmb) then
  25       MATCH_MPL [BETA_RULE (ISPECL [a';b';set] and_thm_nn);set_thm;thma;thmb]
  26     else if is_neg (concl thma) && is_pos (concl thmb) then
  27       MATCH_MPL [BETA_RULE (ISPECL [a';b';set] and_thm_np);set_thm;thma;thmb]
  28     else if is_pos (concl thma) && is_neg (concl thmb) then
  29       MATCH_MPL [BETA_RULE (ISPECL [a';b';set] and_thm_pn);set_thm;thma;thmb]
  30     else if is_pos (concl thma) && is_pos (concl thmb) then
  31       MATCH_MPL [BETA_RULE (ISPECL [a';b';set] and_thm_pp);set_thm;thma;thmb]
  32     else failwith "error"
  33   else if is_disj fm then
  34     let a,b = dest_disj fm in
  35     let a',b' = mk_abs (var,a),mk_abs (var,b) in
  36     let thma = TESTFORM var interpsigns_thm set_thm a  in
  37     let thmb = TESTFORM var interpsigns_thm set_thm b  in
  38     if is_neg (concl thma) && is_neg (concl thmb) then
  39       MATCH_MPL [BETA_RULE (ISPECL [a';b';set] or_thm_nn);set_thm;thma;thmb]
  40     else if is_pos (concl thma) then
  41       MATCH_MPL [BETA_RULE (ISPECL [a';b';set] or_thm_p);set_thm;thma]
  42     else if is_pos (concl thmb) then
  43       MATCH_MPL [BETA_RULE (ISPECL [a';b';set] or_thm_q);set_thm;thmb]
  44     else failwith "error"
  45   else if is_imp fm then
  46     let a,b = dest_imp fm in
  47     let a',b' = mk_abs (var,a),mk_abs (var,b) in
  48     let thma = TESTFORM var interpsigns_thm set_thm a  in
  49     let thmb = TESTFORM var interpsigns_thm set_thm b  in
  50     if is_neg (concl thma) then
  51       MATCH_MPL [BETA_RULE (ISPECL [a';b';set] imp_thm_n);set_thm;thma]
  52     else if is_pos (concl thma) && is_neg (concl thmb) then
  53       MATCH_MPL [BETA_RULE (ISPECL [a';b';set] imp_thm_pn);set_thm;thma;thmb]
  54     else if is_pos (concl thma) && is_pos (concl thmb) then
  55       MATCH_MPL [BETA_RULE (ISPECL [a';b';set] imp_thm_pp);set_thm;thmb]
  56     else failwith "error"
  57   else if is_iff fm then
  58     let a,b = dest_eq fm in
  59     let a',b' = mk_abs (var,a),mk_abs (var,b) in
  60     let thma = TESTFORM var interpsigns_thm set_thm a  in
  61     let thmb = TESTFORM var interpsigns_thm set_thm b  in
  62     if is_neg (concl thma) && is_neg (concl thmb) then
  63       MATCH_MPL [BETA_RULE (ISPECL [a';b';set] iff_thm_nn);set_thm;thma;thmb]
  64     else if is_neg (concl thma) && is_pos (concl thmb) then
  65       MATCH_MPL [BETA_RULE (ISPECL [a';b';set] iff_thm_np);set_thm;thma;thmb]
  66     else if is_pos (concl thma) && is_neg (concl thmb) then
  67       MATCH_MPL [BETA_RULE (ISPECL [a';b';set] iff_thm_pn);set_thm;thma;thmb]
  68     else if is_pos (concl thma) && is_pos (concl thmb) then
  69       MATCH_MPL [BETA_RULE (ISPECL [a';b';set] iff_thm_pp);set_thm;thma;thmb]
  70     else failwith "error"
  71   else (* an atom *)
  72     let op,p,_ = get_binop fm in
  73     let lam = mk_abs (var,p) in
  74     let ind =
  75       try
  76         index lam polys'
  77       with Failure "index" -> failwith "TESTFORM: Poly not present in list" in
  78     let sign = ith ind signs' in
  79     let thm = ith ind (interpsigns_thms interpsigns_thm) in
  80     let thm_op,thm_p,_ =
  81       get_binop (snd (dest_imp (snd (dest_forall (concl thm))))) in
  82     if op = req then
  83       if thm_op = req then thm
  84       else if thm_op = rlt then
  85         MATCH_MPL [BETA_RULE (ISPECL [lam;set] lt_eq_thm);thm]
  86       else if thm_op = rgt then
  87         MATCH_MPL [BETA_RULE (ISPECL [lam;set] gt_eq_thm);thm]
  88       else failwith "error"
  89     else if op = rlt then
  90       if thm_op = rlt then thm
  91       else if  thm_op = req then
  92         MATCH_MPL [BETA_RULE (ISPECL [lam;set] eq_lt_thm);thm]
  93       else if thm_op = rgt then
  94         MATCH_MPL [BETA_RULE (ISPECL [lam;set] gt_lt_thm);thm]
  95       else failwith "error"
  96     else if op = rgt then
  97       if thm_op = rgt then thm
  98       else if  thm_op = req then
  99         MATCH_MPL [BETA_RULE (ISPECL [lam;set] eq_gt_thm);thm]
 100       else if thm_op = rlt then
 101         MATCH_MPL [BETA_RULE (ISPECL [lam;set] lt_gt_thm);thm]
 102       else failwith "error"
 103     else if op = rle then
 104       if thm_op = rlt then
 105         MATCH_MPL [BETA_RULE (ISPECL [lam;set] lt_le_thm);thm]
 106       else if  thm_op = req then
 107         MATCH_MPL [BETA_RULE (ISPECL [lam;set] eq_le_thm);thm]
 108       else if thm_op = rgt then
 109         MATCH_MPL [BETA_RULE (ISPECL [lam;set] gt_le_thm);thm]
 110       else failwith "error"
 111     else if op = rge then
 112       if thm_op = rlt then
 113         MATCH_MPL [BETA_RULE (ISPECL [lam;set] lt_ge_thm);thm]
 114       else if  thm_op = req then
 115         MATCH_MPL [BETA_RULE (ISPECL [lam;set] eq_ge_thm);thm]
 116       else if thm_op = rgt then
 117         MATCH_MPL [BETA_RULE (ISPECL [lam;set] gt_ge_thm);thm]
 118       else failwith "error"
 119     else failwith "error" ;;
 120
 121 let TESTFORM var interpsigns_thm set_thm fm =
 122   let start_time = Sys.time() in
 123   let res = TESTFORM var interpsigns_thm set_thm fm in
 124     testform_timer +.= (Sys.time() -. start_time);
 125     res;;
 126
 127
 128 let tvar,tmat,tfm = ref `T`,ref TRUTH,ref `T`;;
 129 (*
 130 let var,mat_thm,fm = !tvar,!tmat,!tfm
 131 *)
 132
 133 let COMBINE_TESTFORMS =
 134   let lem1 = TAUT `(T ==> a) <=> a`
 135   and lem2 = TAUT `(T /\ x) <=> x`
 136   and imat_tm = `interpmat` in
 137   fun var mat_thm fm ->
 138   tvar := var;
 139   tmat := mat_thm;
 140   tfm := fm;
 141   (* if not (fst (strip_comb (concl mat_thm)) = imat_tm) then failwith "not a mat thm" else *)
 142   let mat_thm' = (CONV_RULE (RATOR_CONV (RAND_CONV (LIST_CONV (ALPHA_CONV var))))) mat_thm in
 143   let rol_thm,all2_thm = interpmat_thms mat_thm' in
 144   let ord_thms = rol_nonempty_thms rol_thm in
 145   let part_thm = PARTITION_LINE_CONV (snd(dest_comb(concl rol_thm))) in
 146   let isigns_thms = CONJUNCTS(REWRITE_RULE[ALL2;part_thm] all2_thm) in
 147   let ex_thms = map2 (fun x y -> TESTFORM var x y fm) isigns_thms ord_thms in
 148   if exists (fun x -> is_forall(concl x)) ex_thms then
 149     let witness_thm = find (fun x -> is_forall(concl x)) ex_thms in
 150     let i = try index witness_thm ex_thms with _ -> failwith "COMBINE_TESTFORMS: witness not present" in
 151     let ord_thm = ith i ord_thms in
 152     let x,bod = dest_exists (concl ord_thm) in
 153     if bod = t_tm then
 154       let thm1 = ISPEC var witness_thm in
 155       let thm2 = PURE_REWRITE_RULE[lem1] thm1 in
 156       let exists_thm = EXISTS (mk_exists(var,concl thm2),var) thm2 in
 157         EQT_INTRO exists_thm
 158     else
 159       let nv = new_var real_ty in
 160       let ord_thm' = CONV_RULE (RAND_CONV (ALPHA_CONV nv)) ord_thm in
 161       let y,bod = dest_exists (concl ord_thm') in
 162       let ass_thm = ASSUME bod in
 163       let thm = MATCH_MP witness_thm ass_thm in
 164       let exists_thm = EXISTS (mk_exists(y,concl thm) ,y) thm in
 165       let ret = CHOOSE (nv,ord_thm) exists_thm in
 166         EQT_INTRO ret
 167   else
 168     if length ord_thms = 1 & snd(dest_exists(concl (hd ord_thms))) = t_tm then
 169       PURE_REWRITE_RULE[lem2] (EQF_INTRO (hd ex_thms)) else
 170     let ex_thms' = map (MATCH_MP NOT_EXISTS_CONJ_THM) ex_thms in
 171     let len = length ex_thms' in
 172     let first,[t1;t2] = chop_list (len-2) ex_thms' in
 173     let base = MATCH_MPL[testform_itlem;t1;t2] in
 174     let ex_thm = itlist (fun x y -> MATCH_MPL[testform_itlem;x;y]) first base in
 175     let cover_thm = ROL_COVERS rol_thm in
 176     let pre_thm = MATCH_MP ex_thm (ISPEC var cover_thm) in
 177     let gen_thm = GEN var pre_thm in
 178     let ret = MATCH_EQ_MP FORALL_NOT_THM gen_thm in
 179       EQF_INTRO ret;;
 180
 181 let COMBINE_TESTFORMS var mat_thm fm =
 182   let start_time = Sys.time() in
 183   let res = COMBINE_TESTFORMS var mat_thm fm in
 184     combine_testforms_timer +.= (Sys.time() -. start_time);
 185     res;;
 186
 187 (* {{{ Examples *)
 188 (*
 189
 190 let var,mat_thm,fm =
 191 rx,ASSUME `interpsigns [\x. &1 + x * (&0 + x * &1)] (\x. T) [Pos]`,ASSUME `?x:real. T`
 192
 193
 194 let ex_thms = map2 (fun x y -> TESTFORM var x y fm) isigns_thms ord_thms in
 195 TESTFORM ry (hd isigns_thms) (hd ord_thms) fm
 196 TESTFORM ry (hd isigns_thms) (hd ord_thms) `&1 + y * (&0 + x * -- &1) <= &0`
 197 TESTFORM ry (hd isigns_thms) (hd ord_thms) `(&1 + x * (&0 + x * -- &1)) + y * (&0 + y * -- &1) < &0`
 198 TESTFORM ry (hd isigns_thms) (hd ord_thms) `(&1 + y * (&0 + x * -- &1) <= &0) /\ (&1 + x * (&0 + x * -- &1)) + y * (&0 + y * -- &1) < &0`
 199 let fm = `(&1 + y * (&0 + x * -- &1) <= &0) /\ (&1 + x * (&0 + x * -- &1)) + y * (&0 + y * -- &1) < &0`
 200
 201 let var,mat_thm,fm =
 202 ry,
 203 ASSUME `interpmat [] [\y. (&1 + x * (&0 + x * -- &1)) + y * (&0 + y * -- &1); \y. &1 + y * (&0 + x * -- &1)] [[Neg; Pos]]`,
 204 `~((&1 + x * (&0 + x * -- &1)) + y * (&0 + y * -- &1) < &0 /\ &1 + y * (&0 + x * -- &1) <= &0)`
 205
 206 let var,mat_thm,fm =
 207 ry,
 208 ASSUME `interpmat [x_354]
 209         [\y. (&1 + x * -- &1) + y * (&0 + x * -- &2); \x. &1 + x * -- &1;
 210         \y. (&1 + x * -- &1) + y * (&0 + x * -- &2)]
 211         [[Neg; Pos; Neg]; [Neg; Zero; Neg]; [Neg; Neg; Neg]]`,
 212 `~(&1 + x * -- &1 < &0 /\ &1 + y * -- &1 < &0
 213      ==> (&1 + x * -- &1) + y * (&0 + x * -- &2) < &0)`
 214
 215
 216 *)
 217
 218 (* }}} *)