Update from HH
[hl193./.git] / 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 ****)