1(*---------------------------------------------------------------------------*) 2(* Defines a type of equivalence classes, and transfers a list of *) 3(* functions and theorems about the representatives over to the new type. *) 4(* It returns a list of the transferred theorems. *) 5(* *) 6(* name - desired name of new type *) 7(* *) 8(* equiv - Theorem that R is an equivalence relation; in the form: *) 9(* |- !x y. x R y = (R x = R y) *) 10(* *) 11(* fnlist - list of {fname,func,fixity} where fname is the new function *) 12(* name, func is the old term, and fixity gives the parsing *) 13(* status. *) 14(* *) 15(* welldefs - theorems asserting that the old functions are welldefined; *) 16(* of the form |- (x1 R y1) /\ .. /\ (xn R yn) ==> *) 17(* (f x1 .. xn) R (f y1 .. yn) *) 18(* where "R" becomes "=" for types other than the *) 19(* representing type. *) 20(* *) 21(* thlist - List of theorems about the old functions *) 22(* *) 23(* Restrictions: *) 24(* *) 25(* * R must be an equivalence relation over the whole type, no subsets. *) 26(* *) 27(* * All original functions must be curried (as are the new ones). *) 28(* *) 29(* * The theorems must have all variables bound by existential or *) 30(* universal quantifiers. *) 31(* *) 32(* * The theorems must be obviously `well-defined', i.e. invariant under *) 33(* substitution [t/u] whenever |- t R u. Essentially "R" becomes "=" and *) 34(* old functions become the new ones. *) 35(* *) 36(* * All arguments/results of the representing type will be transferred *) 37(* to the new type. *) 38(* *) 39(* Author: John Harrison *) 40(*---------------------------------------------------------------------------*) 41 42structure EquivType :> EquivType = 43struct 44 45(* The Standard Header *) 46open HolKernel Parse boolLib liteLib; 47 48(* Fix the grammar used by this file *) 49val ambient_grammars = Parse.current_grammars(); 50val _ = Parse.temp_set_grammars boolTheory.bool_grammars 51 52val LAND_CONV = RATOR_CONV o RAND_CONV; 53val PROVE = Tactical.default_prover 54 55fun MK_COMB_TAC (asl,w) = 56 let val (l,r) = dest_eq w 57 val (l1,l2) = dest_comb l 58 val (r1,r2) = dest_comb r in 59 ([(asl,mk_eq(l1,r1)), (asl,mk_eq(l2,r2))],end_itlist (curry MK_COMB)) end; 60 61 62(*---------------------------------------------------------------------------*) 63(* Define this as hol90 dislikes genvars in constant definitions *) 64(* N.B. This is hopelessly crude. *) 65(*---------------------------------------------------------------------------*) 66 67fun upto from to = 68 if from>to then [] 69 else from::upto (from+1) to; 70 71fun wargs tylist = 72 let val nums = upto 1 (length tylist) 73(* val nms = map (fn n => implode ("T"::(explode(chr(n + ord"0"))))) nums in*) 74 val nms = map (fn n => "T"^Lib.int_to_string n) nums 75 in 76 map mk_var (zip nms tylist) 77 end; 78 79(*---------------------------------------------------------------------------*) 80(* Now the main function. *) 81(*---------------------------------------------------------------------------*) 82 83 84fun define_equivalence_type{name=tyname, equiv, defs = fnlist, 85 welldefs, old_thms = thlist} = 86 let 87 val absname = "mk_"^tyname and repname = "dest_"^tyname 88 val eqv = (rator o rhs o rhs o snd o strip_forall o concl) equiv 89 val repty = (hd o snd o dest_type o type_of) eqv 90 val tydef = 91 let val rtm = ���\c. ?x. c = ^eqv x��� in 92 new_type_definition(tyname, 93 PROVE(���?c. ^rtm c���, 94 BETA_TAC THEN 95 MAP_EVERY EXISTS_TAC [���^eqv x���, ���x:^(ty_antiq(repty))���] 96 THEN REFL_TAC)) end 97 val tybij = BETA_RULE 98 (define_new_type_bijections {name = tyname^"_tybij", 99 ABS = absname, 100 REP = repname, 101 tyax = tydef}) 102 val absty = mk_type(tyname,[]) 103 val (abs,rep) = ((I ## rator) o dest_comb o lhs o snd o dest_forall 104 o fst o dest_conj o concl) tybij 105 106 val refl = PROVE 107 (���!h. ^eqv h h���, 108 GEN_TAC THEN REWRITE_TAC[equiv] THEN REFL_TAC) 109 val sym = PROVE 110 (���!h i. ^eqv h i = ^eqv i h���, 111 REWRITE_TAC[equiv] THEN MATCH_ACCEPT_TAC EQ_SYM_EQ) 112 val trans = PROVE 113 (���!h i j. ^eqv h i /\ ^eqv i j ==> ^eqv h j���, 114 REPEAT GEN_TAC THEN REWRITE_TAC[equiv] THEN 115 MATCH_ACCEPT_TAC EQ_TRANS) 116 117 val EQ_AP = PROVE 118 (���!p q. (p = q) ==> ^eqv p q���, 119 REPEAT GEN_TAC THEN DISCH_THEN SUBST1_TAC THEN 120 MATCH_ACCEPT_TAC refl) 121 122 val EQ_WELLDEF = PROVE 123 (���!x1 x2 y1 y2. (^eqv x1 x2) /\ (^eqv y1 y2) ==> 124 ((^eqv x1 y1) = (^eqv x2 y2))���, 125 REPEAT GEN_TAC THEN DISCH_TAC THEN EQ_TAC THENL 126 [RULE_ASSUM_TAC(ONCE_REWRITE_RULE[sym]), ALL_TAC] THEN 127 POP_ASSUM(CONJUNCTS_THEN2 (fn th => DISCH_THEN(MP_TAC o CONJ th)) ASSUME_TAC) 128 THEN DISCH_THEN(MP_TAC o MATCH_MP trans) THEN 129 RULE_ASSUM_TAC(ONCE_REWRITE_RULE[sym]) THEN 130 POP_ASSUM(fn th => DISCH_THEN(MP_TAC o C CONJ th)) THEN 131 DISCH_THEN(ACCEPT_TAC o MATCH_MP trans)) 132 133 val DEST_MK_EQCLASS = PROVE 134 (���!v. ^rep (^abs (^eqv v)) = ^eqv v���, 135 GEN_TAC THEN REWRITE_TAC[GSYM tybij] THEN 136 EXISTS_TAC ���v:^(ty_antiq(repty))��� THEN REFL_TAC) 137 138 val SAME_REP = PROVE 139 (���!h i. ^eqv h i ==> ^eqv h ($@ (^eqv i))���, 140 REPEAT GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC trans THEN 141 EXISTS_TAC ���i:^(ty_antiq(repty))��� THEN ASM_REWRITE_TAC[] THEN 142 MATCH_MP_TAC SELECT_AX THEN 143 EXISTS_TAC ���i:^(ty_antiq(repty))��� THEN MATCH_ACCEPT_TAC refl) 144 145 val SAME_RCR = PROVE 146 (���!h i. (^eqv($@(^rep h)) = ^eqv($@(^rep i))) = (h = i)���, 147 let val th = SYM(REWRITE_RULE[equiv] 148 (SPECL [���h:^(ty_antiq(repty))���, 149 ���h:^(ty_antiq(repty))���] 150 SAME_REP)) 151 val th2 = REWRITE_RULE[CONJUNCT1 tybij] 152 (SPEC ���^rep h���(CONJUNCT2 tybij)) 153 val th3 = SPEC ���i:^(ty_antiq(absty))��� 154 (GEN ���h:^(ty_antiq(absty))��� th2) in 155 REPEAT GEN_TAC THEN MAP_EVERY CHOOSE_TAC [th2, th3] THEN 156 ASM_REWRITE_TAC[th] THEN EVERY_ASSUM(SUBST1_TAC o SYM) THEN EQ_TAC THENL 157 [DISCH_THEN(MP_TAC o AP_TERM abs), DISCH_THEN SUBST1_TAC] THEN 158 REWRITE_TAC[tybij] end) 159 160 val R_MK_COMB_TAC = FIRST 161 [W(C (curry op THEN) (GEN_TAC THEN CONV_TAC 162 (RAND_CONV BETA_CONV THENC LAND_CONV BETA_CONV)) o 163 CONV_TAC o X_FUN_EQ_CONV o fst o dest_abs o lhs o snd), 164 FIRST(map MATCH_MP_TAC (EQ_WELLDEF::welldefs)) THEN REPEAT CONJ_TAC, 165 MK_COMB_TAC, 166 MATCH_MP_TAC SAME_REP, 167 MATCH_MP_TAC EQ_AP, 168 FIRST (map MATCH_ACCEPT_TAC [refl, EQ_REFL])] 169 170 fun EQC_FORALL_CONV tm = 171 let val v = fst(dest_forall tm) 172 val v' = (mk_var o(I##(K absty o assert(curry op = repty))) o dest_var) 173 v 174 val th1 = GEN v' (SPEC ���$@(^rep ^v')��� (ASSUME tm)) 175 val tm' = concl th1 176 val th2 = ASSUME tm' 177 val th3 = GEN v (SPEC ���^abs (^eqv ^v)��� th2) 178 val th4 = Rewrite.GEN_REWRITE_RULE ONCE_DEPTH_CONV 179 Rewrite.empty_rewrites [DEST_MK_EQCLASS] th3 180 val tm'' = concl th4 181 val peq = mk_eq(tm,tm'') 182 val th5 = PROVE(peq,REPEAT R_MK_COMB_TAC) 183 val th6 = EQ_MP(SYM th5) th4 in 184 IMP_ANTISYM_RULE (DISCH_ALL th1) (DISCH_ALL th6) end 185 186 val EQC_EXISTS_CONV = 187 let val neg2 = SPEC ���x:bool��� (CONJUNCT1 NOT_CLAUSES) in 188 REWR_CONV(SYM neg2) THENC 189 RAND_CONV(NOT_EXISTS_CONV THENC EQC_FORALL_CONV) THENC 190 NOT_FORALL_CONV THENC RAND_CONV(ABS_CONV(REWR_CONV neg2)) end 191 192 193 fun transconv tm = 194 if is_abs tm then (mk_abs o (I ## transconv) o dest_abs) tm 195 else 196 let val (opp,tms) = (I ## map transconv) (strip_comb tm) in 197 if (mem opp (map #func fnlist) andalso (type_of tm = repty)) then 198 ���$@(^rep(^abs(^eqv ^(list_mk_comb(opp,tms)))))��� 199 else if tms = [] then opp 200 else list_mk_comb(transconv opp,tms) end 201 202 fun TRANSFORM_CONV tm = 203 let val th1 = 204 QCONV (DEPTH_CONV(EQC_FORALL_CONV ORELSEC EQC_EXISTS_CONV)) tm 205 val tm1 = rhs(concl th1) 206 val th2 = PROVE 207 (mk_eq(tm1,transconv tm1), 208 REWRITE_TAC[DEST_MK_EQCLASS] THEN 209 REPEAT R_MK_COMB_TAC) in 210 TRANS th1 th2 211 end 212 213 fun dest_funtype ty = 214 if ty=repty then [ty] 215 else let val (l,r) = dom_rng ty 216 in [l]@dest_funtype r 217 end handle HOL_ERR _ => [ty] 218 219 fun define_fun {def_name,fname,func=tm,fixity} = 220 let val tyl = dest_funtype(type_of tm) 221 val ntyl = map (fn ty => if ty = repty then absty else ty) tyl 222 val rty = end_itlist (fn t1 => fn t2 => mk_type("fun",[t1,t2])) ntyl 223 val args = wargs (butlast ntyl) 224 val rargs = map (fn tm => if (type_of tm = absty) 225 then���$@ (^rep ^tm)��� 226 else tm) 227 args 228 val l = list_mk_comb(mk_var(fname,rty),args) 229 val r = let val r0 = list_mk_comb(tm,rargs) 230 in if type_of r0 = repty 231 then ���^abs (^eqv ^r0)��� 232 else r0 233 end 234 in 235 (case fixity of SOME fxty => Parse.set_fixity fname fxty | NONE => ()); 236 new_definition(def_name, mk_eq(l,r)) 237 end 238 239 val newdefs = map define_fun fnlist 240 241 val newthms = map (REWRITE_RULE(map GSYM newdefs) o 242 REWRITE_RULE[equiv, SAME_RCR] o 243 CONV_RULE TRANSFORM_CONV) thlist 244 in 245 newthms 246end; 247 248val _ = Parse.temp_set_grammars ambient_grammars 249 250end (* EquivType *) 251