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