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