Rqe/basic.ml

   1
   2 (* ---------------------------------------------------------------------- *)
   3 (*  Operators                                                             *)
   4 (* ---------------------------------------------------------------------- *)
   5 let dest_beq = dest_binop `(<=>)`;;
   6 let t_tm = `T`;;
   7 let f_tm = `F`;;
   8
   9 parse_as_infix ("<>",(12,"right"));;
  10
  11 let NEQ = new_definition
  12  `x <> y <=> ~(x = y)`;;
  13
  14 let nqt = `(<>):A -> A -> bool`;;
  15 let mk_neq (l,r) =
  16   try
  17       let ty = type_of l in
  18       let nqt' = inst[ty,aty] nqt in
  19         mk_comb(mk_comb(nqt',l),r)
  20   with Failure _ -> failwith "mk_neq";;
  21
  22 (* ---------------------------------------------------------------------- *)
  23 (*  Unfiled                                                               *)
  24 (* ---------------------------------------------------------------------- *)
  25
  26 let IMP_AND_THM = TAUT `(p ==> q ==> r) <=> (p /\ q ==> r)`;;
  27 let AND_IMP_THM = TAUT `(p /\ q ==> r) <=> (p ==> q ==> r)`;;
  28
  29 let is_pos tm = not (is_neg tm);;
  30
  31 let CONJ_LIST thms =
  32     end_itlist CONJ thms;;
  33
  34 (*
  35 CONJ_LIST [TRUTH;TRUTH;TRUTH]
  36 *)