1(*=======================================================================
2 * Support for AC reasoning.
3 *=====================================================================*)
4
5structure AC :> AC =
6struct
7
8open HolKernel boolSyntax Drule Conv liteLib Ho_Rewrite Abbrev;
9
10val INST = HolKernel.INST
11
12infix 5 |->
13infix THENCQC THENQC
14fun ERR x = STRUCT_ERR "AC" x;
15fun WRAP_ERR x = STRUCT_WRAP "AC" x;
16
17fun AC thms = EQT_ELIM o AC_CONV thms;
18
19(* ------------------------------------------------------------------------- *)
20(* ACI equivalence for conjunctions.                                         *)
21(* ------------------------------------------------------------------------- *)
22
23val CONJ_ACI =
24    let fun FIND_CONJS thl tm =
25        let val (l,r) = dest_conj tm
26        in CONJ (FIND_CONJS thl l) (FIND_CONJS thl r)
27        end handle HOL_ERR _ => first (fn th => concl th = tm) thl
28    in fn tm =>
29        let val (l,r) = dest_eq tm
30            val thl = CONJUNCTS(ASSUME l)
31            and thr = CONJUNCTS(ASSUME r)
32        in IMP_ANTISYM_RULE (DISCH_ALL (FIND_CONJS thl r))
33                            (DISCH_ALL (FIND_CONJS thr l))
34        end
35    end;;
36
37(* ------------------------------------------------------------------------- *)
38(* AC canonicalizing under a given ordering.                                 *)
39(* ------------------------------------------------------------------------- *)
40
41fun list_mk_binop oper = end_foldr (mk_binop oper);;
42
43fun AC_CANON_GEN_CONV acthms =
44 let val oper = rator(rator(rand(repeat (body o rand) (concl (snd acthms)))))
45     val AC_fn = AC acthms
46 in fn order => fn tm =>
47    let val op' = repeat rator tm
48    in if can (ho_match_term [] empty_tmset oper) op'
49       then let val op' = repeat rator tm
50                val tmlist = binops op' tm
51                val stmlist = Listsort.sort order tmlist
52                val tm' = list_mk_binop op' stmlist
53            in AC_fn(mk_eq(tm,tm'))
54            end
55            handle HOL_ERR _ => REFL tm
56       else failwith "AC_CANON_GEN_CONV"
57    end
58 end;
59
60(* ------------------------------------------------------------------------- *)
61(* And under the arbitrary term ordering.                                    *)
62(* ------------------------------------------------------------------------- *)
63
64fun AC_CANON_CONV acthms = AC_CANON_GEN_CONV acthms Term.compare;
65
66
67(*- -------------------------------------------------------------------------*
68 * DISTRIB_CONV                                                              *
69 *                                                                           *
70 * Distribution conversion. This could be optimized a bit by splitting up    *
71 * the toplevel product and collecting all those which aren't sums; these'd  *
72 * then only need to be distributed once and for all. Hardly worth it!       *
73 *                                                                           *
74 * Taken directly from the GTT source code, by JRH. Translation by           *
75 * Donald Syme.  Jan 96.                                                     *
76 * --------------------------------------------------------------------------*)
77
78val DISTRIB_CONV =
79  let fun RAW_DISTRIB_CONV lth rth hop lop =
80        let val DISTRIB0_QCONV = GEN_REWRITE_CONV I [lth, rth]
81            fun DISTRIB1_QCONV tm =
82                  (DISTRIB0_QCONV THENCQC
83                    (COMB2_QCONV (RAND_CONV DISTRIB1_QCONV) DISTRIB1_QCONV)) tm
84            fun DISTRIB2_QCONV tm =
85              let val (xop,r) = dest_comb tm
86                  val (oper,l) = dest_comb xop
87              in if oper = lop
88                 then COMB2_QCONV (RAND_CONV DISTRIB2_QCONV) DISTRIB2_QCONV tm
89                 else if oper = hop
90                      then ((COMB2_QCONV (RAND_CONV DISTRIB2_QCONV)
91                                 DISTRIB2_QCONV) THENQC DISTRIB1_QCONV) tm
92                      else ERR("DISTRIB2_QCONV","")
93              end
94        in
95           TRY_CONV DISTRIB2_QCONV
96        end
97  in
98  fn (lth0,rth0) =>
99     case boolSyntax.strip_comb(rand(snd(strip_forall(concl lth0))))
100      of (lop0,[_,htm]) =>
101          (let val hop0 = rator(rator htm)
102           in if type_vars_in_term hop0 = []
103              then RAW_DISTRIB_CONV lth0 rth0 hop0 lop0
104              else let val vty = type_of htm
105                   in fn tm =>
106                       let val tyins = match_type vty (type_of tm)
107                           val INST_fn = INST_TYPE tyins
108                           and inst_fn = inst tyins
109                       in
110                          RAW_DISTRIB_CONV (INST_fn lth0) (INST_fn rth0)
111                                           (inst_fn hop0) (inst_fn lop0) tm
112                       end
113                   end
114           end handle HOL_ERR _ => failwith "DISTRIB_CONV")
115       | _ => failwith "DISTRIB_CONV"
116  end;
117
118
119
120(*---------------------------------------------------------------------------*
121 * Efficient left-association conversion.                                    *
122 *                                                                           *
123 * Taken directly from the GTT source code, by JRH. Translation by           *
124 * Donald Syme.  Jan 96.                                                     *
125 * ------------------------------------------------------------------------- *)
126
127val ASSOC_CONV =
128  let fun MK_ASSOC_CONV oper assoc t1 t2 t3 =
129      let fun ASSOC_CONV tm =
130          let val (l,r) = dest_binop oper tm
131          in ASSOC_ACC_CONV l (ASSOC_CONV r)
132             handle HOL_ERR _ => ASSOC_TAC_CONV l r
133          end
134          and ASSOC_TAC_CONV tm rtm =
135              let val (l,r) = dest_binop oper tm
136                  val ppth = INST [t1 |-> l,t2 |-> r, t3 |-> rtm] assoc
137              in TRANS ppth (ASSOC_ACC_CONV l (ASSOC_TAC_CONV r rtm))
138                  handle HOL_ERR _ =>
139                      TRANS ppth (ASSOC_TAC_CONV l (rand(rand(concl ppth))))
140                      handle HOL_ERR _ => ppth
141              end
142          and ASSOC_ACC_CONV tm ath =
143              let val (l,r) = dest_binop oper tm
144                  val qth = ASSOC_ACC_CONV r ath
145                  val rth = ASSOC_ACC_CONV l qth
146              in
147               TRANS
148                 (INST [t1|->l, t2|->r, t3|->rand(rator(concl ath))] assoc) rth
149              end
150          handle HOL_ERR _  => AP_TERM (mk_comb(oper,tm)) ath
151      in fn tm => ASSOC_CONV tm handle HOL_ERR _ => REFL tm
152      end
153  in fn rassoc =>
154      let val assoc = SYM(SPEC_ALL rassoc)
155          val (opt1,t23) = dest_comb(rand(concl(assoc)))
156          val (oper,t1) = dest_comb opt1
157          val t2 = rand(rator t23) and t3 = rand t23
158      in
159         if type_vars(type_of oper) = []
160         then MK_ASSOC_CONV oper assoc t1 t2 t3
161         else fn tm =>
162             let val xop = rator(rator tm)
163             in case ho_match_term [] empty_tmset oper xop
164                 of ([],tyin) =>
165                     (let val inst_fn = Term.inst tyin
166                          val assoc' = Thm.INST_TYPE tyin assoc
167                          and t1' = inst_fn t1
168                          and t2' = inst_fn t2
169                          and t3' = inst_fn t3
170                      in
171                        MK_ASSOC_CONV xop assoc' t1' t2' t3' tm
172                      end handle HOL_ERR _ => REFL tm)
173                  | _ => REFL tm
174             end
175      end
176  end
177
178end (* struct *)
179