tcScript.sml

1(* file HS/FIN/tcScript.sml, created 1/23/13, revised 9/30, author F.L.Morris *)
2
3(* A theory to support implementation of Warshall's algorithm for transitive *)
4(* closure. Relations are represented as set-valued finite maps, but no      *)
5(* particular representation is presumed for the sets or maps themselves.    *)
6(* Accompanying tcTacs will offer a conversion to work with either set [...] *)
7(* sets and fmap [...] fmaps, only needing an equality-decider conversion    *)
8(* for elements/arguments, or (prefeably) with FMAPAL fmaps & ENUMERAL sets, *)
9(* needing a conversion reducing a three-valued "toto" ordering, for which   *)
10(* see totoTheory, totoTacs, and also enumeralTheory/Tacs, fmapalTheory/Tacs.*)
11
12(* app load ["pred_setLib", "pred_setTheory", "relationTheory", "pairTheory",
13"optionTheory", "TotalDefn", "bossLib", "finite_mapTheory",
14"wotTheory"]; *) (* wotTheory only for definiton of type 'a reln *)
15Theory tc
16Ancestors
17  pred_set relation pair option combin list finite_map toto
18Libs
19  pred_setLib Defn TotalDefn PairRules PairRules pairLib
20
21
22val _ = set_trace "Unicode" 0;
23val _ = ParseExtras.temp_loose_equality()
24
25(* My habitual abbreviations: *)
26
27val AR = ASM_REWRITE_TAC [];
28fun ulist x = [x];
29fun rrs th = REWRITE_RULE [SPECIFICATION] th;
30
31(* *************************************************************** *)
32
33val _ = set_fixity "^|" (Infixl 650);
34val _ = set_fixity "|^" (Infixl 650);
35val _ = set_fixity "^|^" (Infixl 650);
36
37(* Restriction of a relation to a subset of its domain, range, or both:
38^|, |^, ^|^ respectively. "RESTRICT" has been taken for mysterious purposes
39by the original relationTheory, and "DRESTRICT" by finite_mapTheory.  *)
40
41Definition DRESTR:
42  ((R:'a reln) ^| (s:'a set)) a b = a IN s /\ R a b
43End
44
45Theorem DRESTR_IN:
46  !R:'a reln s a. (R ^| s) a = if a IN s then R a else {}
47Proof
48REPEAT STRIP_TAC THEN CONV_TAC FUN_EQ_CONV THEN REWRITE_TAC [DRESTR] THEN
49GEN_TAC THEN Cases_on `a IN s` THEN AR THEN
50REWRITE_TAC [rrs NOT_IN_EMPTY]
51QED
52
53Definition RRESTR:
54  ((R:'a reln) |^ (s:'a set)) a b = b IN s /\ R a b
55End
56
57(* restriction Both fore and aft *)
58
59Definition BRESTR: (R:'a reln) ^|^ s = R ^| s |^ s
60End
61
62Theorem DRESTR_EMPTY:
63  !R:'a reln. R ^| {} = REMPTY
64Proof
65GEN_TAC THEN REPEAT (CONV_TAC FUN_EQ_CONV THEN GEN_TAC) THEN
66REWRITE_TAC [DRESTR_IN, NOT_IN_EMPTY, EMPTY_REL_DEF] THEN
67REWRITE_TAC [rrs NOT_IN_EMPTY]
68QED
69
70Theorem DRESTR_RDOM:
71  !R:'a reln. R ^| (RDOM R) = R
72Proof
73GEN_TAC THEN REPEAT (CONV_TAC FUN_EQ_CONV THEN GEN_TAC) THEN
74REWRITE_TAC [DRESTR_IN, IN_RDOM] THEN
75COND_CASES_TAC THENL
76[REFL_TAC
77,UNDISCH_THEN ``~?y. (R:'a reln) x y``
78              (REWRITE_TAC o ulist o CONV_RULE NOT_EXISTS_CONV) THEN
79 REWRITE_TAC [rrs NOT_IN_EMPTY]]
80QED
81
82Theorem REMPTY_RRESTR:
83  !s. REMPTY:'a reln |^ s = REMPTY
84Proof
85GEN_TAC THEN REPEAT (CONV_TAC FUN_EQ_CONV THEN GEN_TAC) THEN
86REWRITE_TAC [RRESTR, EMPTY_REL_DEF]
87QED
88
89Theorem O_REMPTY_O:
90  (!R:'a reln. R O REMPTY = REMPTY) /\
91  (!R:'a reln. REMPTY O R = REMPTY)
92Proof
93CONJ_TAC THEN GEN_TAC THEN REPEAT (CONV_TAC FUN_EQ_CONV THEN GEN_TAC) THEN
94REWRITE_TAC [EMPTY_REL_DEF, O_DEF]
95QED
96
97(* Define subTC, the invariant for an arrayless form of the
98   Floyd-Warshall algorithm, in as low-level and symmetrical a way as
99   possible, with an eye to using (R)TC induction principles. *)
100
101Definition subTC:  subTC (R:'a reln) s x y =
102  R x y \/ ?a b. (R ^|^ s)^* a b /\ a IN s /\ b IN s /\ R x a /\ R b y
103End
104
105(* Definition as first conceived becomes a theorem: *)
106(* Outer ^| s is meant just to trim off (x,x) pairs for x NOTIN s, and we
107   need a lemma about that: *)
108
109val RTC_trim_lem = BETA_RULE (prove (
110``!R:'a reln s y y'. (\x. x IN s) y' /\ (R ^|^ s)^* y' y ==> (\x. x IN s) y``,
111REPEAT GEN_TAC THEN MATCH_MP_TAC RTC_lifts_invariants THEN BETA_TAC THEN
112REWRITE_TAC [BRESTR, DRESTR, RRESTR] THEN REPEAT STRIP_TAC THEN AR));
113
114(* RTC_trim_lem = |- !R s y y'. y' IN s /\ (R ^|^ s)^* y' y ==> y IN s *)
115
116Theorem subTC_thm:
117  !R:'a reln s. subTC R s = R RUNION (R O ((R ^|^ s)^* ^| s) O R)
118Proof
119REPEAT GEN_TAC THEN REPEAT (CONV_TAC FUN_EQ_CONV THEN GEN_TAC) THEN
120REWRITE_TAC [subTC, O_DEF, RUNION, DRESTR] THEN
121EQ_TAC THEN STRIP_TAC THEN AR THEN DISJ2_TAC THENL
122[EXISTS_TAC ``b:'a`` THEN AR THEN
123 EXISTS_TAC ``a:'a`` THEN AR
124,EXISTS_TAC ``y':'a`` THEN EXISTS_TAC ``y:'a`` THEN AR THEN
125 IMP_RES_TAC RTC_trim_lem]
126QED
127
128Theorem subTC_EMPTY:
129  !R:'a reln. subTC R {} = R
130Proof
131GEN_TAC THEN REPEAT (CONV_TAC FUN_EQ_CONV THEN GEN_TAC) THEN
132REWRITE_TAC [subTC_thm, BRESTR, DRESTR_EMPTY, O_REMPTY_O, REMPTY_RRESTR,
133             EMPTY_REL_DEF, RUNION]
134QED
135
136(* Dec 14 new departure: figure out what is bigger or equal (in fact equal)
137   to (R ^|^ (a INSERT s))^* because that's the only way I know to use a
138   transitive closure hypothesis. *)
139
140(* seemingly needs to be proved in two stages, one with RTC_STRONG_INDUCT,
141   one with RTC_STRONG_INDUCT_RIGHT1 *)
142
143Theorem NOT_IN_RTC_EQ[local]:
144  !R:'a reln s p q. (p NOTIN s \/ q NOTIN s) /\ (R ^|^ s)^* p q ==> (p = q)
145Proof
146REPEAT GEN_TAC THEN CONV_TAC ANTE_CONJ_CONV THEN STRIP_TAC THENL
147[ONCE_REWRITE_TAC [RTC_CASES1], ONCE_REWRITE_TAC [RTC_CASES2]] THEN
148 CONV_TAC CONTRAPOS_CONV THEN DISCH_TAC THEN AR THEN
149 CONV_TAC NOT_EXISTS_CONV THEN GEN_TAC THEN
150 ASM_REWRITE_TAC [BRESTR, DRESTR, RRESTR]
151QED
152
153Theorem RTC_INSERT_MONO[local]:
154  !R:'a reln s a w z. (R ^|^ s)^* w z ==> (R ^|^ (a INSERT s))^* w z
155Proof
156REPEAT GEN_TAC THEN MATCH_MP_TAC RTC_MONOTONE THEN
157REPEAT GEN_TAC THEN REWRITE_TAC [BRESTR, DRESTR, RRESTR, IN_INSERT] THEN
158STRIP_TAC THEN AR
159QED
160
161Theorem RTC_INSERT_RIGHT_IMP[local]:
162  !R:'a reln s a w z. (R ^|^ (a INSERT s))^* w z ==>
163(R ^|^ s)^* w z \/ ((a = z) \/ ?y. y IN s /\ R a y /\ (R ^|^ s)^* y z)
164Proof
165REPEAT GEN_TAC THEN
166Cases_on `a IN s`
167THEN1 (IMP_RES_THEN SUBST1_TAC ABSORPTION_RWT THEN
168       DISCH_THEN (REWRITE_TAC o ulist)) THEN
169SUBGOAL_THEN ``(R:'a reln ^|^ s)^* w z \/
170                  ((a = z) \/ ?y. y IN s /\ R a y /\ (R ^|^ s)^* y z) =
171         (\w z. (R ^|^ s)^* w z \/
172                  ((a = z) \/ ?y. y IN s /\ R a y /\ (R ^|^ s)^* y z)) w z``
173SUBST1_TAC THEN1 (BETA_TAC THEN REFL_TAC) THEN
174MATCH_MP_TAC RTC_STRONG_INDUCT THEN BETA_TAC THEN REPEAT STRIP_TAC THEN
175ASM_REWRITE_TAC [RTC_REFL] THENL
176 [Cases_on `x = a` THENL
177  [DISJ2_TAC THEN Cases_on `y IN s` THENL
178   [DISJ2_TAC THEN EXISTS_TAC ``y:'a`` THEN AR THEN
179    Q.UNDISCH_TAC `(R ^|^ (a INSERT s)) x y` THEN
180    ASM_REWRITE_TAC [BRESTR, DRESTR, RRESTR] THEN STRIP_TAC THEN AR
181   ,DISJ1_TAC THEN Q.SUBGOAL_THEN `z = y` ASSUME_TAC THENL
182    [IMP_RES_TAC NOT_IN_RTC_EQ THEN Cases_on `a = y` THEN AR
183    ,Cases_on `a = y` THEN1 AR THEN
184     Q.SUBGOAL_THEN `x = y` (ASM_REWRITE_TAC o ulist o SYM) THEN
185     Q.SUBGOAL_THEN `y NOTIN a INSERT s` ASSUME_TAC
186     THEN1 (ASM_REWRITE_TAC [IN_INSERT] THEN
187            Q.UNDISCH_THEN `a <> y` (ACCEPT_TAC o GSYM)) THEN
188     MATCH_MP_TAC (Q.SPECL [`R`, `a INSERT s`] NOT_IN_RTC_EQ) THEN
189     CONJ_TAC THENL [AR, IMP_RES_TAC RTC_SINGLE]
190   ]]
191  ,Cases_on `y = a` THENL
192   [DISJ2_TAC THEN
193    DISJ1_TAC THEN Q.SUBGOAL_THEN `y = z` (ASM_REWRITE_TAC o ulist o SYM) THEN
194    MATCH_MP_TAC NOT_IN_RTC_EQ THEN
195    Q.EXISTS_TAC `R` THEN Q.EXISTS_TAC `s` THEN AR
196   ,DISJ1_TAC THEN
197    ONCE_REWRITE_TAC [RTC_CASES1] THEN DISJ2_TAC THEN Q.EXISTS_TAC `y` THEN
198    AR THEN Q.UNDISCH_TAC `(R ^|^ (a INSERT s)) x y` THEN
199    ASM_REWRITE_TAC [BRESTR, DRESTR, RRESTR, IN_INSERT]
200   ]]
201  ,DISJ2_TAC THEN DISJ2_TAC THEN Q.EXISTS_TAC `y'` THEN AR
202 ]
203QED
204
205Theorem RTC_INSERT_LEFT_IMP[local]:
206  !R:'a reln s a w z. (R ^|^ (a INSERT s))^* w z ==>
207   (R ^|^ s)^* w z \/ ((a = w) \/ ?x. x IN s /\ (R ^|^ s)^* w x /\ R x a)
208Proof
209REPEAT GEN_TAC THEN
210Cases_on `a IN s`
211THEN1 (IMP_RES_THEN SUBST1_TAC ABSORPTION_RWT THEN
212       DISCH_THEN (REWRITE_TAC o ulist)) THEN
213SUBGOAL_THEN ``(R:'a reln ^|^ s)^* w z \/
214                  ((a = w) \/ ?x. x IN s /\ (R ^|^ s)^* w x /\ R x a) =
215         (\w z. (R ^|^ s)^* w z \/
216                  ((a = w) \/ ?x. x IN s /\ (R ^|^ s)^* w x /\ R x a)) w z``
217SUBST1_TAC THEN1 (BETA_TAC THEN REFL_TAC) THEN
218MATCH_MP_TAC RTC_STRONG_INDUCT_RIGHT1 THEN BETA_TAC THEN REPEAT STRIP_TAC THEN
219ASM_REWRITE_TAC [RTC_REFL] THENL
220 [Cases_on `z = a` THENL
221  [DISJ2_TAC THEN Cases_on `y IN s` THENL
222   [DISJ2_TAC THEN EXISTS_TAC ``y:'a`` THEN AR THEN
223    Q.UNDISCH_TAC `(R ^|^ (a INSERT s)) y z` THEN
224    ASM_REWRITE_TAC [BRESTR, DRESTR, RRESTR] THEN STRIP_TAC THEN AR
225   ,DISJ1_TAC THEN Q.SUBGOAL_THEN `x = y` ASSUME_TAC THENL
226    [IMP_RES_TAC NOT_IN_RTC_EQ THEN Cases_on `a = y` THEN AR
227    ,Cases_on `a = y` THEN1 AR THEN
228     Q.SUBGOAL_THEN `y = z` (ASM_REWRITE_TAC o ulist) THEN
229     Q.SUBGOAL_THEN `y NOTIN a INSERT s` ASSUME_TAC
230     THEN1 (ASM_REWRITE_TAC [IN_INSERT] THEN
231            Q.UNDISCH_THEN `a <> y` (ACCEPT_TAC o GSYM)) THEN
232     MATCH_MP_TAC (Q.SPECL [`R`, `a INSERT s`] NOT_IN_RTC_EQ) THEN
233     CONJ_TAC THENL [AR, IMP_RES_TAC RTC_SINGLE]
234   ]]
235  ,Cases_on `y = a` THENL
236   [DISJ2_TAC THEN
237    DISJ1_TAC THEN Q.SUBGOAL_THEN `x = y` (ASM_REWRITE_TAC o ulist) THEN
238    MATCH_MP_TAC NOT_IN_RTC_EQ THEN
239    Q.EXISTS_TAC `R` THEN Q.EXISTS_TAC `s` THEN AR
240   ,DISJ1_TAC THEN
241    ONCE_REWRITE_TAC [RTC_CASES2] THEN DISJ2_TAC THEN Q.EXISTS_TAC `y` THEN
242    AR THEN Q.UNDISCH_TAC `(R ^|^ (a INSERT s)) y z` THEN
243    ASM_REWRITE_TAC [BRESTR, DRESTR, RRESTR, IN_INSERT]
244   ]]
245  ,DISJ2_TAC THEN DISJ2_TAC THEN Q.EXISTS_TAC `x'` THEN AR
246 ]
247QED
248
249Theorem RTC_INSERT:
250  !R:'a reln s a w z. (R ^|^ (a INSERT s))^* w z <=>
251(R ^|^ s)^* w z \/ ((a = w) \/ ?x. x IN s /\ (R ^|^ s)^* w x /\ R x a) /\
252                   ((a = z) \/ ?y. y IN s /\ R a y /\ (R ^|^ s)^* y z)
253Proof
254REPEAT GEN_TAC THEN EQ_TAC THENL
255[DISCH_TAC THEN CONV_TAC (REWR_CONV LEFT_OR_OVER_AND) THEN CONJ_TAC THENL
256 [MATCH_MP_TAC RTC_INSERT_LEFT_IMP THEN AR
257 ,MATCH_MP_TAC RTC_INSERT_RIGHT_IMP THEN AR
258 ]
259,STRIP_TAC THENL
260 [IMP_RES_TAC RTC_INSERT_MONO THEN AR
261 ,Q.UNDISCH_THEN `a = z` (CONV_TAC o RAND_CONV o REWR_CONV o SYM) THEN
262  Q.UNDISCH_THEN `a = w`
263            (CONV_TAC o RATOR_CONV o RAND_CONV o REWR_CONV o SYM) THEN
264  REWRITE_TAC [BRESTR, RRESTR, DRESTR, IN_INSERT, RTC_REFL]
265 ,ONCE_REWRITE_TAC [RTC_CASES1] THEN
266  DISJ2_TAC THEN Q.EXISTS_TAC `y` THEN CONJ_TAC THENL
267  [Q.UNDISCH_THEN `a = w` (SUBST1_TAC o SYM) THEN
268   ASM_REWRITE_TAC [BRESTR, RRESTR, DRESTR, IN_INSERT]
269  ,IMP_RES_TAC RTC_INSERT_MONO THEN AR
270  ]
271 ,Q.UNDISCH_THEN `a = z` (CONV_TAC o RAND_CONV o REWR_CONV o SYM) THEN
272  ONCE_REWRITE_TAC [RTC_CASES2] THEN
273  DISJ2_TAC THEN Q.EXISTS_TAC `x` THEN CONJ_TAC THENL
274  [IMP_RES_TAC RTC_INSERT_MONO THEN AR
275  ,ASM_REWRITE_TAC [BRESTR, RRESTR, DRESTR, IN_INSERT]
276  ]
277 ,MATCH_MP_TAC (REWRITE_RULE [transitive_def] (Q.SPEC `R` RTC_TRANSITIVE)) THEN
278  Q.EXISTS_TAC `a` THEN CONJ_TAC THENL
279  [ONCE_REWRITE_TAC [RTC_CASES2] THEN
280   DISJ2_TAC THEN Q.EXISTS_TAC `x` THEN CONJ_TAC THENL
281   [IMP_RES_TAC RTC_INSERT_MONO THEN AR
282   ,ASM_REWRITE_TAC [BRESTR, RRESTR, DRESTR, IN_INSERT]
283   ]
284  ,ONCE_REWRITE_TAC [RTC_CASES1] THEN
285   DISJ2_TAC THEN Q.EXISTS_TAC `y` THEN CONJ_TAC THENL
286   [ASM_REWRITE_TAC [BRESTR, RRESTR, DRESTR, IN_INSERT]
287   ,IMP_RES_TAC RTC_INSERT_MONO THEN AR
288]]]]
289QED
290
291Theorem NOT_EQ_RTC_IN[local]:
292  !R:'a reln s p q. p <> q \/ q <> p ==> (R ^|^ s)^* p q ==> p IN s /\ q IN s
293Proof
294REPEAT GEN_TAC THEN CONV_TAC CONTRAPOS_CONV THEN
295REWRITE_TAC [DE_MORGAN_THM, NOT_IMP] THEN REPEAT STRIP_TAC THENL
296[ALL_TAC, CONV_TAC (REWR_CONV EQ_SYM_EQ),
297 ALL_TAC, CONV_TAC (REWR_CONV EQ_SYM_EQ)] THEN
298MATCH_MP_TAC (Q.SPECL [`R`, `s`] NOT_IN_RTC_EQ) THEN AR
299QED
300
301Theorem RTC_IN_LR[local]:
302  (!R:'a reln s p q. p IN s /\ (R ^|^ s)^* p q ==> q IN s)
303Proof
304REPEAT STRIP_TAC THEN
305Cases_on `q IN s` THEN1 AR THEN
306IMP_RES_TAC NOT_IN_RTC_EQ THEN
307Q.UNDISCH_THEN `p = q` (SUBST1_TAC o SYM) THEN AR
308QED
309
310Theorem RTC_IN_RL[local]:
311  (!R:'a reln s p q. q IN s /\ (R ^|^ s)^* p q ==> p IN s)
312Proof
313REPEAT STRIP_TAC THEN
314Cases_on `p IN s` THEN1 AR THEN
315IMP_RES_TAC NOT_IN_RTC_EQ THEN
316Q.UNDISCH_THEN `p = q` SUBST1_TAC THEN AR
317QED
318
319Theorem RTC_subTC1[local]:
320  !R:'a reln s a w x. R w x /\ (R ^|^ (a INSERT s))^* x a ==>
321                      subTC R s w a
322Proof
323REPEAT GEN_TAC THEN REWRITE_TAC [subTC, RTC_INSERT] THEN STRIP_TAC THENL
324[Cases_on `a = x` THEN1 AR THEN
325 DISJ2_TAC THEN IMP_RES_TAC RTC_CASES2
326 THEN1 (Q.UNDISCH_TAC `a <> x` THEN AR) THEN
327 IMP_RES_TAC NOT_EQ_RTC_IN THEN
328 IMP_RES_TAC RTC_IN_LR THEN
329 Q.EXISTS_TAC `x` THEN Q.EXISTS_TAC `u` THEN
330 Q.UNDISCH_TAC `(R ^|^ s) u a` THEN
331 ASM_REWRITE_TAC [BRESTR, DRESTR, RRESTR]
332,AR
333,DISJ2_TAC THEN Q.EXISTS_TAC `x` THEN Q.EXISTS_TAC `x'` THEN
334 IMP_RES_TAC RTC_IN_RL THEN AR
335]
336QED
337
338Theorem RTC_subTC2[local]:
339  !R:'a reln s a y z. (R ^|^ (a INSERT s))^* a y /\ R y z ==>
340                      subTC R s a z
341Proof
342REPEAT GEN_TAC THEN REWRITE_TAC [subTC, RTC_INSERT] THEN STRIP_TAC THENL
343[Cases_on `a = y` THEN1 AR THEN
344 DISJ2_TAC THEN IMP_RES_TAC RTC_CASES1 THEN
345 IMP_RES_TAC NOT_EQ_RTC_IN THEN
346 IMP_RES_TAC RTC_IN_RL THEN
347 Q.EXISTS_TAC `u` THEN Q.EXISTS_TAC `y` THEN
348 Q.UNDISCH_TAC `(R ^|^ s) a u` THEN
349 ASM_REWRITE_TAC [BRESTR, DRESTR, RRESTR]
350,AR
351,DISJ2_TAC THEN Q.EXISTS_TAC `y'` THEN Q.EXISTS_TAC `y` THEN
352 IMP_RES_TAC RTC_IN_LR THEN AR
353]
354QED
355
356(* The big lemma: what enlarging s by one does to subTC R x *)
357
358Theorem subTC_INSERT:
359  !R:'a reln s q x y. subTC R (q INSERT s) x y <=>
360   subTC R s x y \/ subTC R s x q /\ subTC R s q y
361Proof
362REPEAT GEN_TAC THEN EQ_TAC THENL
363[CONV_TAC (LAND_CONV (REWRITE_CONV [subTC])) THEN
364 REWRITE_TAC [DISJ_IMP_THM] THEN CONJ_TAC THENL
365 [DISCH_TAC THEN ASM_REWRITE_TAC [subTC]
366 ,REPEAT (CONV_TAC LEFT_IMP_EXISTS_CONV THEN GEN_TAC) THEN
367  Cases_on `q IN s`
368  THEN1 (IMP_RES_THEN SUBST1_TAC ABSORPTION_RWT THEN
369         STRIP_TAC THEN DISJ1_TAC THEN REWRITE_TAC [subTC] THEN
370         DISJ2_TAC THEN Q.EXISTS_TAC `a` THEN Q.EXISTS_TAC `b` THEN AR) THEN
371  STRIP_TAC THEN
372  Cases_on `a = q` THENL
373  [DISJ2_TAC THEN CONJ_TAC THENL
374   [Q.UNDISCH_THEN `a = q` (SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC [subTC]
375   ,MATCH_MP_TAC RTC_subTC2 THEN Q.EXISTS_TAC `b` THEN AR THEN
376    Q.UNDISCH_THEN `a = q`
377    (CONV_TAC o RATOR_CONV o RAND_CONV o REWR_CONV o SYM) THEN AR
378   ]
379  ,Q.SUBGOAL_THEN `a IN s` ASSUME_TAC THEN1 IMP_RES_TAC IN_INSERT THEN
380   Cases_on `b = q` THENL
381   [DISJ2_TAC THEN CONJ_TAC THENL
382    [MATCH_MP_TAC RTC_subTC1 THEN Q.EXISTS_TAC `a` THEN AR THEN
383     Q.UNDISCH_THEN `b = q`
384     (CONV_TAC o RAND_CONV o REWR_CONV o SYM) THEN AR
385    ,Q.UNDISCH_THEN `b = q` (SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC [subTC]
386    ]
387   ,Q.SUBGOAL_THEN `b IN s` ASSUME_TAC THEN1 IMP_RES_TAC IN_INSERT THEN
388    Cases_on `(R ^|^ s)^* a b`
389    THEN1 (DISJ1_TAC THEN ASM_REWRITE_TAC [subTC] THEN DISJ2_TAC THEN
390           Q.EXISTS_TAC `a` THEN Q.EXISTS_TAC `b` THEN AR) THEN
391    Q.UNDISCH_TAC `(R ^|^ (q INSERT s))^* a b` THEN
392    REWRITE_TAC [RTC_INSERT] THEN
393    STRIP_TAC THENL
394    [Q.UNDISCH_TAC `a <> q` THEN Q.UNDISCH_THEN `q = a` (REWRITE_TAC o ulist)
395    ,Q.UNDISCH_TAC `a <> q` THEN AR
396    ,Q.UNDISCH_TAC `b <> q` THEN AR
397    ,DISJ2_TAC THEN CONJ_TAC THEN ASM_REWRITE_TAC [subTC] THEN DISJ2_TAC THENL
398     [Q.EXISTS_TAC `a` THEN Q.EXISTS_TAC `x'` THEN AR
399     ,Q.EXISTS_TAC `y'` THEN Q.EXISTS_TAC `b` THEN AR
400 ]]]]]
401,REWRITE_TAC [DISJ_IMP_THM] THEN REWRITE_TAC [subTC] THEN CONJ_TAC THENL
402 [STRIP_TAC THEN1 AR THEN DISJ2_TAC THEN
403  Q.EXISTS_TAC `a` THEN Q.EXISTS_TAC `b` THEN
404  IMP_RES_TAC RTC_INSERT_MONO THEN ASM_REWRITE_TAC [IN_INSERT]
405 ,STRIP_TAC THEN DISJ2_TAC THENL
406  [Q.EXISTS_TAC `q` THEN Q.EXISTS_TAC `q` THEN
407   ASM_REWRITE_TAC [IN_INSERT, RTC_REFL]
408  ,Q.EXISTS_TAC `q` THEN Q.EXISTS_TAC `b` THEN ASM_REWRITE_TAC [IN_INSERT] THEN
409   ONCE_REWRITE_TAC [RTC_CASES1] THEN DISJ2_TAC THEN
410   Q.EXISTS_TAC `a` THEN IMP_RES_TAC RTC_INSERT_MONO THEN
411   ASM_REWRITE_TAC [BRESTR, DRESTR, RRESTR, IN_INSERT]
412  ,Q.EXISTS_TAC `a` THEN Q.EXISTS_TAC `q` THEN ASM_REWRITE_TAC [IN_INSERT] THEN
413   ONCE_REWRITE_TAC [RTC_CASES2] THEN DISJ2_TAC THEN
414   Q.EXISTS_TAC `b` THEN IMP_RES_TAC RTC_INSERT_MONO THEN
415   ASM_REWRITE_TAC [BRESTR, DRESTR, RRESTR, IN_INSERT]
416  ,Q.EXISTS_TAC `a` THEN Q.EXISTS_TAC `b'` THEN ASM_REWRITE_TAC [IN_INSERT] THEN
417   MATCH_MP_TAC (REWRITE_RULE [transitive_def] RTC_TRANSITIVE) THEN
418   Q.EXISTS_TAC `q` THEN CONJ_TAC THENL
419   [ONCE_REWRITE_TAC [RTC_CASES2] THEN DISJ2_TAC THEN
420    Q.EXISTS_TAC `b` THEN IMP_RES_TAC RTC_INSERT_MONO THEN
421    ASM_REWRITE_TAC [BRESTR, DRESTR, RRESTR, IN_INSERT]
422   ,ONCE_REWRITE_TAC [RTC_CASES1] THEN DISJ2_TAC THEN
423    Q.EXISTS_TAC `a'` THEN IMP_RES_TAC RTC_INSERT_MONO THEN
424    ASM_REWRITE_TAC [BRESTR, DRESTR, RRESTR, IN_INSERT]
425]]]]
426QED
427
428Theorem subTC_RDOM:
429  !R:'a reln. subTC R (RDOM R) = R^+
430Proof
431GEN_TAC THEN REPEAT (CONV_TAC FUN_EQ_CONV THEN GEN_TAC) THEN EQ_TAC THENL
432[REWRITE_TAC [subTC, DISJ_IMP_THM] THEN
433 CONJ_TAC THEN1 MATCH_ACCEPT_TAC TC_SUBSET THEN
434 STRIP_TAC THEN
435 MATCH_MP_TAC EXTEND_RTC_TC THEN Q.EXISTS_TAC `a` THEN AR THEN
436 ONCE_REWRITE_TAC [RTC_CASES2] THEN DISJ2_TAC THEN Q.EXISTS_TAC `b` THEN
437 AR THEN Q.UNDISCH_TAC `(R ^|^ RDOM R)^* a b` THEN
438 MATCH_MP_TAC RTC_MONOTONE THEN
439 REWRITE_TAC [BRESTR, DRESTR, RRESTR] THEN REPEAT STRIP_TAC THEN AR
440,MATCH_MP_TAC TC_INDUCT THEN REWRITE_TAC [subTC] THEN
441 REPEAT STRIP_TAC
442 THEN1 AR THEN DISJ2_TAC THENL
443 [Q.EXISTS_TAC `y` THEN Q.EXISTS_TAC `y` THEN
444  ASM_REWRITE_TAC [RTC_REFL, IN_RDOM] THEN Q.EXISTS_TAC `z` THEN AR
445 ,Q.EXISTS_TAC `y` THEN Q.EXISTS_TAC `b` THEN
446  ASM_REWRITE_TAC [IN_RDOM] THEN CONJ_TAC THENL
447  [ONCE_REWRITE_TAC [RTC_CASES1] THEN DISJ2_TAC THEN Q.EXISTS_TAC `a` THEN
448   ASM_REWRITE_TAC [DRESTR, BRESTR, RRESTR, IN_RDOM]
449  ,ALL_TAC
450  ] THEN Q.EXISTS_TAC `a` THEN AR
451 ,Q.EXISTS_TAC `a` THEN Q.EXISTS_TAC `y` THEN
452  ASM_REWRITE_TAC [IN_RDOM] THEN CONJ_TAC THENL
453  [ONCE_REWRITE_TAC [RTC_CASES2] THEN DISJ2_TAC THEN Q.EXISTS_TAC `b` THEN
454   ASM_REWRITE_TAC [DRESTR, BRESTR, RRESTR, IN_RDOM]
455  ,ALL_TAC
456  ] THEN Q.EXISTS_TAC `z` THEN AR
457 ,Q.EXISTS_TAC `a` THEN Q.EXISTS_TAC `b'` THEN
458  ASM_REWRITE_TAC [IN_RDOM] THEN
459  MATCH_MP_TAC (REWRITE_RULE [transitive_def] RTC_TRANSITIVE) THEN
460  Q.EXISTS_TAC `y` THEN CONJ_TAC THENL
461  [ONCE_REWRITE_TAC [RTC_CASES2] THEN DISJ2_TAC THEN Q.EXISTS_TAC `b` THEN
462   ASM_REWRITE_TAC [DRESTR, BRESTR, RRESTR, IN_RDOM] THEN
463   Q.EXISTS_TAC `a'` THEN AR
464  ,ONCE_REWRITE_TAC [RTC_CASES1] THEN DISJ2_TAC THEN Q.EXISTS_TAC `a'` THEN
465   ASM_REWRITE_TAC [DRESTR, BRESTR, RRESTR, IN_RDOM] THEN
466   Q.EXISTS_TAC `a'` THEN AR
467]]]
468QED
469
470(* following corollary suggests how we want to compute. *)
471
472Theorem subTC_INSERT_COR:
473  !R:'a reln s x a. subTC R (x INSERT s) a =
474   if x IN subTC R s a then subTC R s a UNION subTC R s x else subTC R s a
475Proof
476REPEAT GEN_TAC THEN CONV_TAC FUN_EQ_CONV THEN GEN_TAC THEN
477REWRITE_TAC [SPECIFICATION, subTC_INSERT, COND_RATOR, rrs IN_UNION] THEN
478tautLib.TAUT_TAC
479QED
480
481Theorem RDOM_EMPTY[local]:
482  !R:'a reln. (RDOM R = {}) ==> (R = REMPTY) /\ (!s. subTC R s = REMPTY)
483Proof
484GEN_TAC THEN CONV_TAC (LAND_CONV FUN_EQ_CONV) THEN
485REWRITE_TAC [RDOM_DEF, rrs NOT_IN_EMPTY] THEN
486CONV_TAC (ONCE_DEPTH_CONV NOT_EXISTS_CONV) THEN STRIP_TAC THEN
487CONJ_TAC THEN REPEAT GEN_TAC THEN
488REPEAT (CONV_TAC FUN_EQ_CONV THEN GEN_TAC) THEN
489ASM_REWRITE_TAC [subTC, EMPTY_REL_DEF]
490QED
491
492(* *************************************************************** *)
493(* Define the mapping by which set-valued finite maps represent    *)
494(* binary relations of finite RDOM, and a one-sided inverse.       *)
495(* *************************************************************** *)
496
497Definition FMAP_TO_RELN:
498 FMAP_TO_RELN (f:'a |-> 'a set) x = if x IN FDOM f then f ' x else {}
499End
500
501Definition RELN_TO_FMAP:  RELN_TO_FMAP (R:'a reln) = FUN_FMAP R (RDOM R)
502End
503
504Theorem RDOM_SUBSET_FDOM:
505  !f:'a |-> 'a set. RDOM (FMAP_TO_RELN f) SUBSET FDOM f
506Proof
507GEN_TAC THEN
508REWRITE_TAC [SUBSET_DEF, IN_RDOM, FMAP_TO_RELN] THEN
509Cases_on `x IN FDOM f` THEN ASM_REWRITE_TAC [rrs NOT_IN_EMPTY]
510QED
511
512Theorem FINITE_RDOM:
513  !f:'a |-> 'a set. FINITE (RDOM (FMAP_TO_RELN f))
514Proof
515GEN_TAC THEN MP_TAC (SPEC_ALL RDOM_SUBSET_FDOM) THEN
516MATCH_MP_TAC SUBSET_FINITE THEN MATCH_ACCEPT_TAC FDOM_FINITE
517QED
518
519Theorem FDOM_RDOM:
520  !R:'a reln. FINITE (RDOM R) ==> (FDOM (RELN_TO_FMAP R) = RDOM R)
521Proof
522REPEAT STRIP_TAC THEN
523IMP_RES_TAC (INST_TYPE [beta |-> ``:'a set``] FUN_FMAP_DEF) THEN
524ASM_REWRITE_TAC [RELN_TO_FMAP]
525QED
526
527Theorem RELN_TO_FMAP_TO_RELN_ID:
528  !R:'a reln. FINITE (RDOM R) ==> (FMAP_TO_RELN (RELN_TO_FMAP R) = R)
529Proof
530REPEAT STRIP_TAC THEN IMP_RES_TAC FDOM_RDOM THEN
531CONV_TAC FUN_EQ_CONV THEN GEN_TAC THEN
532REWRITE_TAC [FMAP_TO_RELN] THEN
533COND_CASES_TAC THENL
534[REWRITE_TAC [RELN_TO_FMAP] THEN
535 IMP_RES_TAC (INST_TYPE [beta |-> ``:'a set``] FUN_FMAP_DEF) THEN
536 Q.UNDISCH_TAC `x IN FDOM (RELN_TO_FMAP R)` THEN AR THEN DISCH_TAC THEN
537 RES_TAC THEN AR
538,CONV_TAC (REWR_CONV EQ_SYM_EQ) THEN
539 Q.UNDISCH_TAC `x NOTIN FDOM (RELN_TO_FMAP R)` THEN
540 ASM_REWRITE_TAC [IN_RDOM, GSYM SUBSET_EMPTY, SUBSET_DEF, NOT_IN_EMPTY,
541             IN_RDOM] THEN
542 REWRITE_TAC [SPECIFICATION] THEN
543 CONV_TAC (LAND_CONV NOT_EXISTS_CONV) THEN REWRITE_TAC []]
544QED
545
546(* *** Now we may start to think about a conversion (actually two combined
547  under one name, one relying on pred_set.UNION_CONV and linear lists, the
548  other, which shoud be a somewhat nippier performer, making use of
549  an ENERMERAL-valued FMAPAL, but both following Warshall's algorithm
550  as closely as their data structures will permit) for TC.
551  Decided here not to call it "Floyd-Warshall algorithm", as Floyd's
552  addition was specifically for computing shortest paths from real
553  matrices represented edge-weighted graphs, rather than just transitive
554  closure of a relation, which Warshall had covered. Most likely, using
555  fmaps to real instead of finite sets, we could imitate
556  Floyd if there were any demand for it. *** *)
557
558Theorem RDOM_subTC:
559  !R:'a reln s. RDOM (subTC R s) = RDOM R
560Proof
561REPEAT GEN_TAC THEN CONV_TAC FUN_EQ_CONV THEN GEN_TAC THEN
562REWRITE_TAC [RDOM_DEF, subTC] THEN EQ_TAC THEN STRIP_TAC THENL
563[Q.EXISTS_TAC `y` THEN AR
564,Q.EXISTS_TAC `a` THEN AR
565,Q.EXISTS_TAC `y` THEN AR]
566QED
567
568Theorem NOT_IN_RDOM:
569  !Q:'a reln x. (Q x = {}) <=> x NOTIN RDOM Q
570Proof
571REPEAT GEN_TAC THEN REWRITE_TAC [RDOM_DEF, SPECIFICATION] THEN
572CONV_TAC (LAND_CONV FUN_EQ_CONV) THEN REWRITE_TAC [rrs NOT_IN_EMPTY] THEN
573CONV_TAC (LAND_CONV FORALL_NOT_CONV) THEN AR
574QED
575
576(* Break out the function to be used by TC_ITER  *)
577
578Definition TC_MOD:
579 TC_MOD (x:'a) (rx:'a set) (ra:'a set) = if x IN ra then ra UNION rx else ra
580End
581
582Theorem TC_MOD_EMPTY_ID:
583  !x:'a ra:'a set. TC_MOD x {} = I
584Proof
585REPEAT GEN_TAC THEN CONV_TAC FUN_EQ_CONV THEN SRW_TAC [] [TC_MOD]
586QED
587
588Theorem I_o_f:   !f:'a |-> 'b. I o_f f = f
589Proof
590SRW_TAC [] [fmap_EXT]
591QED
592
593Theorem subTC_MAX_RDOM:
594  !R:'a reln s x. x NOTIN RDOM R ==> (subTC R (x INSERT s) = subTC R s)
595Proof
596REPEAT STRIP_TAC THEN REPEAT (CONV_TAC FUN_EQ_CONV THEN GEN_TAC) THEN
597REWRITE_TAC [subTC_INSERT] THEN
598`x NOTIN RDOM (subTC R s)` by METIS_TAC [RDOM_subTC] THEN
599METIS_TAC [RDOM_DEF, SPECIFICATION]
600QED
601
602Theorem subTC_SUPERSET_RDOM:
603  !R:'a reln s. FINITE s ==>  (subTC R (RDOM R UNION s) = subTC R (RDOM R))
604Proof
605GEN_TAC THEN CONV_TAC (TOP_DEPTH_CONV FUN_EQ_CONV) THEN
606HO_MATCH_MP_TAC FINITE_INDUCT THEN CONJ_TAC THENL
607[REWRITE_TAC [UNION_EMPTY]
608,REPEAT STRIP_TAC THEN
609 `RDOM R UNION (e INSERT s) = (e INSERT RDOM R) UNION s`
610 by (SRW_TAC [] [EXTENSION, IN_UNION, IN_INSERT, DISJ_ASSOC] THEN
611     CONV_TAC (LAND_CONV (LAND_CONV (REWR_CONV DISJ_COMM))) THEN REFL_TAC) THEN
612 AR THEN Cases_on `e IN RDOM R` THENL
613 [IMP_RES_THEN (ASM_REWRITE_TAC o ulist) ABSORPTION_RWT
614 ,IMP_RES_TAC subTC_MAX_RDOM THEN ASM_REWRITE_TAC [INSERT_UNION]
615]]
616QED
617
618Theorem subTC_FDOM:   !g R:'a reln.
619(subTC R (RDOM R) = FMAP_TO_RELN g) ==> (subTC R (FDOM g) = subTC R (RDOM R))
620Proof
621REPEAT STRIP_TAC THEN
622Q.SUBGOAL_THEN `RDOM R SUBSET FDOM g`
623(SUBST1_TAC o GSYM o REWRITE_RULE [SUBSET_UNION_ABSORPTION]) THENL
624[Q.SUBGOAL_THEN `RDOM (subTC R (RDOM R)) = RDOM R` (SUBST1_TAC o SYM)
625 THEN1 MATCH_ACCEPT_TAC RDOM_subTC THEN
626 ASM_REWRITE_TAC [RDOM_SUBSET_FDOM]
627,MATCH_MP_TAC subTC_SUPERSET_RDOM THEN MATCH_ACCEPT_TAC FDOM_FINITE
628]
629QED
630
631Theorem SUBSET_FDOM_LEM:
632  !R:'a reln s f. (subTC R s = FMAP_TO_RELN f) ==> RDOM R SUBSET FDOM f
633Proof
634REPEAT STRIP_TAC THEN
635Q.SUBGOAL_THEN `RDOM R = RDOM (subTC R s)` SUBST1_TAC
636THEN1 MATCH_ACCEPT_TAC (GSYM RDOM_subTC) THEN AR THEN
637MATCH_ACCEPT_TAC RDOM_SUBSET_FDOM
638QED
639
640(* Following is what seems needed: and now it needs a name. *)
641
642Theorem subTC_FDOM_RDOM:
643  !R:'a reln f. (subTC R (FDOM f) = FMAP_TO_RELN f) ==>
644                (subTC R (RDOM R) = FMAP_TO_RELN f)
645Proof
646REPEAT STRIP_TAC THEN
647Q.SUBGOAL_THEN `subTC R (FDOM f) = subTC R (RDOM R)`
648(ASM_REWRITE_TAC o ulist o SYM) THEN
649Q.SUBGOAL_THEN `FDOM f = RDOM R UNION FDOM f`
650(fn eq => SUBST1_TAC eq THEN MATCH_MP_TAC subTC_SUPERSET_RDOM THEN
651 MATCH_ACCEPT_TAC FDOM_FINITE) THEN
652Q.SUBGOAL_THEN `RDOM R SUBSET FDOM f` MP_TAC
653THEN1 (MATCH_MP_TAC SUBSET_FDOM_LEM THEN Q.EXISTS_TAC `FDOM f` THEN AR) THEN
654RW_TAC bool_ss [SUBSET_DEF, IN_UNION, EXTENSION] THEN METIS_TAC []
655QED
656
657(* We will use fmapalTheory.o_f_bt_map to compute the o_f in the following
658   lemma, but proving the lemma is another story. *)
659
660Theorem TC_MOD_LEM:
661  !R:'a reln s x f. x IN FDOM f /\ (subTC R s = FMAP_TO_RELN f) ==>
662  (subTC R (x INSERT s) = FMAP_TO_RELN (TC_MOD x (f ' x) o_f f))
663Proof
664REPEAT STRIP_TAC THEN CONV_TAC FUN_EQ_CONV THEN GEN_TAC THEN
665ASM_REWRITE_TAC [FMAP_TO_RELN, GSYM o_f_FDOM, subTC_INSERT_COR] THEN
666Cases_on `x' IN FDOM f` THEN
667ASM_REWRITE_TAC [EXTENSION] THENL
668[IMP_RES_THEN (REWRITE_TAC o ulist)
669  (REWRITE_RULE [GSYM o_f_FDOM] (Q.SPEC `TC_MOD x (f ' x)`
670    (INST_TYPE [beta |-> ``:'a set``, gamma |-> ``:'a set``] o_f_DEF))) THEN
671 GEN_TAC THEN CONV_TAC (RAND_CONV (REWR_CONV SPECIFICATION)) THEN
672 RW_TAC bool_ss [TC_MOD, SPECIFICATION, UNION_EMPTY]
673,SRW_TAC [] []
674]
675QED
676
677(* Define the recursion over RDOM R *)
678
679Definition TC_ITER:
680 (TC_ITER [] (r:'a|->'a set) = r) /\
681 (TC_ITER (x :: d) r = TC_ITER d (TC_MOD x (r ' x) o_f r))
682End
683
684Theorem TC_ITER_THM:
685  !R:'a reln d f s. (s UNION set d = FDOM f) /\
686                    (subTC R s = FMAP_TO_RELN f) ==>
687                    (TC R = FMAP_TO_RELN (TC_ITER d f))
688Proof
689GEN_TAC THEN Induct THENL
690[REPEAT GEN_TAC THEN REWRITE_TAC [LIST_TO_SET_THM, UNION_EMPTY] THEN
691 CONV_TAC ANTE_CONJ_CONV THEN DISCH_THEN SUBST1_TAC THEN
692 DISCH_THEN (MP_TAC o MATCH_MP subTC_FDOM_RDOM) THEN
693 REWRITE_TAC [TC_ITER, subTC_RDOM]
694,REPEAT STRIP_TAC THEN
695 Q.SUBGOAL_THEN `h IN FDOM f` ASSUME_TAC THENL
696 [Q.UNDISCH_THEN `s UNION set (h::d) = FDOM f` (SUBST1_TAC o SYM) THEN
697  REWRITE_TAC [IN_UNION, MEM]
698 ,Q.SUBGOAL_THEN `(h INSERT s) UNION set d = FDOM f` ASSUME_TAC THENL
699  [Q.UNDISCH_THEN `s UNION set (h::d) = FDOM f` (SUBST1_TAC o SYM) THEN
700   REWRITE_TAC [LIST_TO_SET_THM, INSERT_UNION_EQ] THEN
701   CONV_TAC (ONCE_DEPTH_CONV (REWR_CONV UNION_COMM)) THEN
702   REWRITE_TAC [INSERT_UNION_EQ]
703  ,IMP_RES_TAC TC_MOD_LEM THEN
704   `(h INSERT s) UNION set d = FDOM (TC_MOD h (f ' h) o_f f)` by
705   ASM_REWRITE_TAC [FDOM_o_f] THEN
706   RES_TAC THEN ASM_REWRITE_TAC [TC_ITER]
707]]]
708QED