Tutorial/Custom_inference_rules.ml

   1 let near_ring_axioms =
   2   `(!x. 0 + x = x) /\
   3    (!x. neg x + x = 0) /\
   4    (!x y z. (x + y) + z = x + y + z) /\
   5    (!x y z. (x * y) * z = x * y * z) /\
   6    (!x y z. (x + y) * z = (x * z) + (y * z))`;;
   7
   8 (**** Works eventually but takes a very long time
   9 MESON[]
  10  `(!x. 0 + x = x) /\
  11   (!x. neg x + x = 0) /\
  12   (!x y z. (x + y) + z = x + y + z) /\
  13   (!x y z. (x * y) * z = x * y * z) /\
  14   (!x y z. (x + y) * z = (x * z) + (y * z))
  15   ==> !a. 0 * a = 0`;;
  16  ****)
  17
  18 let is_realvar w x = is_var x & not(mem x w);;
  19
  20 let rec real_strip w tm =
  21   if mem tm w then tm,[] else
  22   let l,r = dest_comb tm in
  23   let f,args = real_strip w l in f,args@[r];;
  24
  25 let weight lis (f,n) (g,m) =
  26   let i = index f lis and j = index g lis in
  27   i > j or i = j & n > m;;
  28
  29 let rec lexord ord l1 l2 =
  30   match (l1,l2) with
  31     (h1::t1,h2::t2) -> if ord h1 h2 then length t1 = length t2
  32                        else h1 = h2 & lexord ord t1 t2
  33   | _ -> false;;
  34
  35 let rec lpo_gt w s t =
  36   if is_realvar w t then not(s = t) & mem t (frees s)
  37   else if is_realvar w s or is_abs s or is_abs t then false else
  38   let f,fargs = real_strip w s and g,gargs = real_strip w t in
  39   exists (fun si -> lpo_ge w si t) fargs or
  40         forall (lpo_gt w s) gargs &
  41         (f = g & lexord (lpo_gt w) fargs gargs or
  42          weight w (f,length fargs) (g,length gargs))
  43 and lpo_ge w s t = (s = t) or lpo_gt w s t;;
  44
  45 let rec istriv w env x t =
  46   if is_realvar w t then t = x or defined env t & istriv w env x (apply env t)
  47   else if is_const t then false else
  48   let f,args = strip_comb t in
  49   exists (istriv w env x) args & failwith "cyclic";;
  50
  51 let rec unify w env tp =
  52   match tp with
  53    ((Var(_,_) as x),t) | (t,(Var(_,_) as x)) when not(mem x w) ->
  54         if defined env x then unify w env (apply env x,t)
  55         else if istriv w env x t then env else (x|->t) env
  56   | (Comb(f,x),Comb(g,y)) -> unify w (unify w env (x,y)) (f,g)
  57   | (s,t) -> if s = t then env else failwith "unify: not unifiable";;
  58
  59 let fullunify w (s,t) =
  60   let env = unify w undefined (s,t) in
  61   let th = map (fun (x,t) -> (t,x)) (graph env) in
  62   let rec subs t =
  63     let t' = vsubst th t in
  64     if t' = t then t else subs t' in
  65   map (fun (t,x) -> (subs t,x)) th;;
  66
  67 let rec listcases fn rfn lis acc =
  68   match lis with
  69     [] -> acc
  70   | h::t -> fn h (fun i h' -> rfn i (h'::map REFL t)) @
  71             listcases fn (fun i t' -> rfn i (REFL h::t')) t acc;;
  72
  73 let LIST_MK_COMB f ths = rev_itlist (fun s t -> MK_COMB(t,s)) ths (REFL f);;
  74
  75 let rec overlaps w th tm rfn =
  76   let l,r = dest_eq(concl th) in
  77   if not (is_comb tm) then [] else
  78   let f,args = strip_comb tm in
  79   listcases (overlaps w th) (fun i a -> rfn i (LIST_MK_COMB f a)) args
  80             (try [rfn (fullunify w (l,tm)) th] with Failure _ -> []);;
  81
  82 let crit1 w eq1 eq2 =
  83   let l1,r1 = dest_eq(concl eq1)
  84   and l2,r2 = dest_eq(concl eq2) in
  85   overlaps w eq1 l2 (fun i th -> TRANS (SYM(INST i th)) (INST i eq2));;
  86
  87 let fixvariables s th =
  88   let fvs = subtract (frees(concl th)) (freesl(hyp th)) in
  89   let gvs = map2 (fun v n -> mk_var(s^string_of_int n,type_of v))
  90                  fvs (1--length fvs) in
  91   INST (zip gvs fvs) th;;
  92
  93 let renamepair (th1,th2) = fixvariables "x" th1,fixvariables "y" th2;;
  94
  95 let critical_pairs w tha thb =
  96   let th1,th2 = renamepair (tha,thb) in crit1 w th1 th2 @ crit1 w th2 th1;;
  97
  98 let normalize_and_orient w eqs th =
  99   let th' = GEN_REWRITE_RULE TOP_DEPTH_CONV eqs th in
 100   let s',t' = dest_eq(concl th') in
 101   if lpo_ge w s' t' then th' else if lpo_ge w t' s' then SYM th'
 102   else failwith "Can't orient equation";;
 103
 104 let status(eqs,crs) eqs0 =
 105   if eqs = eqs0 & (length crs) mod 1000 <> 0 then () else
 106   (print_string(string_of_int(length eqs)^" equations and "^
 107                 string_of_int(length crs)^" pending critical pairs");
 108    print_newline());;
 109
 110 let left_reducible eqs eq =
 111   can (CHANGED_CONV(GEN_REWRITE_CONV (LAND_CONV o ONCE_DEPTH_CONV) eqs))
 112       (concl eq);;
 113
 114 let rec complete w (eqs,crits) =
 115   match crits with
 116     (eq::ocrits) ->
 117         let trip =
 118           try let eq' = normalize_and_orient w eqs eq in
 119               let s',t' = dest_eq(concl eq') in
 120               if s' = t' then (eqs,ocrits) else
 121               let crits',eqs' = partition(left_reducible [eq']) eqs in
 122               let eqs'' = eq'::eqs' in
 123               eqs'',
 124               ocrits @ crits' @ itlist ((@) o critical_pairs w eq') eqs'' []
 125           with Failure _ ->
 126               if exists (can (normalize_and_orient w eqs)) ocrits
 127               then (eqs,ocrits@[eq])
 128               else failwith "complete: no orientable equations" in
 129         status trip eqs; complete w trip
 130   | [] -> eqs;;
 131
 132 let complete_equations wts eqs =
 133   let eqs' = map (normalize_and_orient wts []) eqs in
 134   complete wts ([],eqs');;
 135
 136 complete_equations [`1`; `( * ):num->num->num`; `i:num->num`]
 137   [SPEC_ALL(ASSUME `!a b. i(a) * a * b = b`)];;
 138
 139 complete_equations [`c:A`; `f:A->A`]
 140  (map SPEC_ALL (CONJUNCTS (ASSUME
 141    `((f(f(f(f(f c))))) = c:A) /\ (f(f(f c)) = c)`)));;
 142
 143 let eqs = map SPEC_ALL (CONJUNCTS (ASSUME
 144   `(!x. 1 * x = x) /\ (!x. i(x) * x = 1) /\
 145    (!x y z. (x * y) * z = x * y * z)`)) in
 146 map concl (complete_equations [`1`; `( * ):num->num->num`; `i:num->num`] eqs);;
 147
 148 let COMPLETE_TAC w th =
 149   let eqs = map SPEC_ALL (CONJUNCTS(SPEC_ALL th)) in
 150   let eqs' = complete_equations w eqs in
 151   MAP_EVERY (ASSUME_TAC o GEN_ALL) eqs';;
 152
 153 g `(!x. 1 * x = x) /\
 154    (!x. i(x) * x = 1) /\
 155    (!x y z. (x * y) * z = x * y * z)
 156    ==> !x y. i(y) * i(i(i(x * i(y)))) * x = 1`;;
 157
 158 e (DISCH_THEN(COMPLETE_TAC [`1`; `( * ):num->num->num`; `i:num->num`]));;
 159 e(ASM_REWRITE_TAC[]);;
 160
 161 g `(!x. 0 + x = x) /\
 162      (!x. neg x + x = 0) /\
 163      (!x y z. (x + y) + z = x + y + z) /\
 164      (!x y z. (x * y) * z = x * y * z) /\
 165      (!x y z. (x + y) * z = (x * z) + (y * z))
 166      ==> (neg 0  * (x * y + z + neg(neg(w + z))) + neg(neg b + neg a) =
 167           a + b)`;;
 168
 169 e (DISCH_THEN(COMPLETE_TAC
 170      [`0`; `(+):num->num->num`; `neg:num->num`; `( * ):num->num->num`]));;
 171 e(ASM_REWRITE_TAC[]);;
 172
 173 (**** Could have done this instead
 174 e (DISCH_THEN(COMPLETE_TAC
 175       [`0`; `(+):num->num->num`; `( * ):num->num->num`; `neg:num->num`]));;
 176 ****)