transferScript.sml

1Theory transfer
2
3Overload flip[local] = “combin$C”
4
5(* uniqueness, which might also be termed injectivity *)
6Definition right_unique_def:
7  right_unique (R : 'a -> 'b -> bool) <=>
8    !a b1 b2. R a b1 /\ R a b2 ==> b1 = b2
9End
10Theorem right_unique_EQ[simp]: right_unique (=)
11Proof simp[right_unique_def]
12QED
13
14Definition left_unique_def:
15  left_unique (R: 'a -> 'b -> bool) <=>
16    !a1 a2 b. R a1 b /\ R a2 b ==> a1 = a2
17End
18Theorem left_unique_EQ[simp]: left_unique (=)
19Proof simp[left_unique_def]
20QED
21
22Definition bi_unique_def:
23  bi_unique R <=> left_unique R /\ right_unique R
24End
25
26Theorem bi_unique_implied:
27  left_unique r /\ right_unique r ==> bi_unique r
28Proof
29  simp[bi_unique_def]
30QED
31
32Theorem bi_unique_EQ[simp]: bi_unique (=)
33Proof simp[bi_unique_def]
34QED
35
36(* totality or surjectivity *)
37Definition total_def: total (R : 'a -> 'b -> bool) <=> !x:'a. ?y. R x y
38End
39
40Definition surj_def: surj (R : 'a -> 'b -> bool) <=> !y:'b. ?x. R x y
41End
42
43Definition bitotal_def: bitotal (R : 'a -> 'b -> bool) <=> total R /\ surj R
44End
45
46Theorem bitotal_implied:
47  total r /\ surj r ==> bitotal r
48Proof
49  simp[bitotal_def]
50QED
51
52Theorem total_EQ[simp]:      total (=)
53Proof simp[total_def]
54QED
55
56Theorem surj_EQ[simp]:       surj (=)
57Proof simp[surj_def]
58QED
59
60Theorem bitotal_EQ[simp]:    bitotal (=)
61Proof simp[bitotal_def]
62QED
63
64Definition equalityp_def:    equalityp A <=> A = (=)
65End
66
67Theorem eq_equalityp[simp]:  equalityp (=)
68Proof simp[equalityp_def]
69QED
70
71
72Theorem equalityp_applied:   equalityp A ==> A x x
73Proof simp[equalityp_def]
74QED
75
76Theorem FUN_REL_def =
77        quotientTheory.FUN_REL
78          |> CONV_RULE $ STRIP_QUANT_CONV $ RAND_CONV
79                       $ RENAME_VARS_CONV ["a", "b"]
80
81val _ = set_mapped_fixity {
82  tok = "|==>", fixity = Infixr 490, term_name = "===>"
83 };
84
85Theorem FUN_REL_COMB:
86  (AB |==> CD) f g /\ AB a b ==> CD (f a) (g b)
87Proof simp[FUN_REL_def]
88QED
89
90Theorem FUN_REL_COMB_EQ:
91  (AB1 ===> CD) f g /\ AB2 a b ==> AB1 = AB2 ==> CD (f a) (g b)
92Proof
93  rpt strip_tac >> gvs[] >> irule FUN_REL_COMB >> metis_tac[]
94QED
95
96Theorem FUN_REL_IFF_IMP:
97  (AB |==> (=)) P Q ==> (AB |==> (==>)) P Q /\ (AB |==> combin$C (==>)) P Q
98Proof
99  simp[FUN_REL_def] >> metis_tac[]
100QED
101
102Theorem equalityp_FUN_REL:
103  equalityp AB /\ equalityp CD ==> equalityp (AB |==> CD)
104Proof
105  simp[equalityp_def, FUN_REL_def]
106QED
107
108Theorem EQ_bi_unique:
109  bi_unique AB ==> (AB |==> AB |==> (=)) (=) (=)
110Proof
111  simp[FUN_REL_def, bi_unique_def, left_unique_def, right_unique_def] >>
112  metis_tac[]
113QED
114
115Theorem surj_eqeq:
116  surj ($= ===> $=)
117Proof
118  simp[quotientTheory.FUN_REL_EQ]
119QED
120
121(* ----------------------------------------------------------------------
122    FUN_REL strengthen to iff
123   ---------------------------------------------------------------------- *)
124
125Theorem FUN_REL_iff_imp_strengthen:
126  (AB |==> (=)) P Q ==> (AB |==> (==>)) P Q
127Proof
128  simp[FUN_REL_def] >> metis_tac[]
129QED
130
131Theorem FUN_REL_iff_cimp_strengthen:
132  (AB |==> (=)) P Q ==> (AB |==> flip (==>)) P Q
133Proof
134  simp[FUN_REL_def] >> metis_tac[]
135QED
136
137
138(* ----------------------------------------------------------------------
139    forall
140   ---------------------------------------------------------------------- *)
141
142Theorem ALL_IFF:
143  bitotal AB ==> ((AB |==> (=)) |==> (=)) (!) (!)
144Proof
145  simp[bitotal_def, FUN_REL_def, total_def, surj_def] >> rpt strip_tac >>
146  rename [‘$! a = $! b’] >>
147  ‘a = (\x. a x) /\ b = (\y. b y)’ by simp[FUN_EQ_THM] >>
148  ntac 2 (pop_assum SUBST1_TAC) >> metis_tac[]
149QED
150
151Theorem ALL_surj_RDOM:
152  surj AB ==> ((AB |==> (=)) |==> (=)) (RES_FORALL (RDOM AB)) (!)
153Proof
154  simp[FUN_REL_def, surj_def] >> rpt strip_tac >> rename [‘_ a = $! b’] >>
155  ‘b = (\y. b y)’ by simp[FUN_EQ_THM] >>
156  simp[RES_FORALL_THM, relationTheory.RDOM_DEF, IN_DEF] >>
157  pop_assum SUBST1_TAC >> metis_tac[]
158QED
159
160Theorem ALL_surj_imp_imp:
161  surj AB ==> ((AB |==> (==>)) |==> (==>)) (!) (!)
162Proof
163  simp[surj_def, FUN_REL_def] >> ntac 4 strip_tac >>
164  ‘a = (\x. a x) /\ b = (\y. b y)’ by simp[FUN_EQ_THM] >>
165  ntac 2 (pop_assum SUBST1_TAC) >> metis_tac[]
166QED
167
168Theorem ALL_surj_iff_imp:
169  surj AB ==> ((AB |==> (=)) |==> (==>)) (!) (!)
170Proof
171  simp[surj_def, FUN_REL_def] >> strip_tac >>
172  map_every qx_gen_tac [‘a’, ‘b’] >>
173  ‘a = (\x. a x) /\ b = (\y. b y)’ by simp[FUN_EQ_THM] >>
174  ntac 2 (pop_assum SUBST1_TAC) >> metis_tac[]
175QED
176
177Theorem RRANGE_EQ[simp]:
178  RRANGE (=) = K T
179Proof
180  simp[pred_setTheory.EXTENSION, IN_DEF, relationTheory.RRANGE]
181QED
182
183Theorem RDOM_EQ[simp]:
184  RDOM (=) = K T
185Proof
186  simp[pred_setTheory.EXTENSION, IN_DEF, relationTheory.RDOM_DEF]
187QED
188
189Theorem ALL_total_RRANGE:
190  total AB ==> ((AB |==> (=)) |==> (=)) (!) (RES_FORALL (RRANGE AB))
191Proof
192  simp[total_def, FUN_REL_def, RES_FORALL_THM, IN_DEF,
193       relationTheory.RRANGE] >> strip_tac >> qx_gen_tac ‘a’ >>
194  ‘a = (\x. a x)’ by simp[FUN_EQ_THM] >> pop_assum SUBST1_TAC >>
195  metis_tac[]
196QED
197
198Theorem ALL_total_iff_imp_RRANGE:
199  total AB ==> ((AB |==> (=)) |==> (==>)) (!) (RES_FORALL (RRANGE AB))
200Proof
201  simp[total_def, FUN_REL_def, RES_FORALL_THM, IN_DEF,
202       relationTheory.RRANGE] >>
203  strip_tac >> qx_gen_tac ‘a’ >>
204  ‘a = (\x. a x)’ by simp[FUN_EQ_THM] >> pop_assum SUBST1_TAC >>
205  metis_tac[]
206QED
207
208Theorem ALL_total_cimp_cimp:
209  total AB ==> ((AB |==> flip (==>)) |==> flip (==>)) (!) (!)
210Proof
211  simp[total_def, FUN_REL_def] >> strip_tac >>
212  map_every qx_gen_tac [‘a’, ‘b’] >>
213  ‘a = (\x. a x) /\ b = (\y. b y)’ by simp[FUN_EQ_THM] >>
214  ntac 2 (pop_assum SUBST1_TAC) >> metis_tac[]
215QED
216
217Theorem ALL_total_iff_cimp:
218  total AB ==> ((AB |==> (=)) |==> flip (==>)) (!) (!)
219Proof
220  simp[total_def, FUN_REL_def] >> strip_tac >>
221  map_every qx_gen_tac [‘a’, ‘b’] >>
222  ‘a = (\x. a x) /\ b = (\y. b y)’ by simp[FUN_EQ_THM] >>
223  ntac 2 (pop_assum SUBST1_TAC) >> metis_tac[]
224QED
225
226(* ----------------------------------------------------------------------
227    exists
228   ---------------------------------------------------------------------- *)
229
230Theorem EXISTS_bitotal :
231  bitotal AB ==> ((AB |==> (=)) |==> (=)) (?) (?)
232Proof
233  simp[FUN_REL_def, bitotal_def, total_def, surj_def] >> strip_tac >>
234  qx_genl_tac [‘aP’, ‘bP’] >> strip_tac >>
235  ‘aP = (\a. aP a) /\ bP = (\b. bP b)’ by simp[FUN_EQ_THM] >>
236  ntac 2 (pop_assum SUBST1_TAC) >> metis_tac[]
237QED
238
239Theorem EXISTS_IFF_RDOM:
240  surj AB ==> ((AB |==> (=)) |==> (=)) (RES_EXISTS (RDOM AB)) (?)
241Proof
242  simp[FUN_REL_def, bitotal_def, total_def, surj_def, RES_EXISTS_THM, IN_DEF] >>
243  strip_tac >> qx_genl_tac [‘aP’, ‘bP’] >> strip_tac >>
244  ‘bP = (\b. bP b)’ by simp[FUN_EQ_THM] >> pop_assum SUBST1_TAC >>
245  simp[relationTheory.RDOM_DEF] >> metis_tac[]
246QED
247
248Theorem EXISTS_IFF_RRANGE:
249  total AB ==> ((AB |==> (=)) |==> (=)) (?) (RES_EXISTS (RRANGE AB))
250Proof
251  simp[FUN_REL_def, bitotal_def, total_def, surj_def, RES_EXISTS_THM, IN_DEF] >>
252  strip_tac >> qx_genl_tac [‘aP’, ‘bP’] >> strip_tac >>
253  ‘aP = (\a. aP a)’ by simp[FUN_EQ_THM] >> pop_assum SUBST1_TAC >>
254  simp[relationTheory.RRANGE] >> metis_tac[]
255QED
256
257Theorem EXISTS_total_iff_imp:
258  total AB ==> ((AB |==> (=)) |==> $==>) (?) (?)
259Proof
260  simp[FUN_REL_def, bitotal_def, total_def, surj_def] >> strip_tac >>
261  qx_genl_tac [‘aP’, ‘bP’] >> strip_tac >>
262  ‘aP = (\a. aP a) /\ bP = (\b. bP b)’ by simp[FUN_EQ_THM] >>
263  ntac 2 (pop_assum SUBST1_TAC) >> metis_tac[]
264QED
265
266Theorem EXISTS_total_imp_imp:
267  total AB ==> ((AB |==> $==>) |==> $==>) (?) (?)
268Proof
269  simp[FUN_REL_def, bitotal_def, total_def, surj_def] >> strip_tac >>
270  qx_genl_tac [‘aP’, ‘bP’] >> strip_tac >>
271  ‘aP = (\a. aP a) /\ bP = (\b. bP b)’ by simp[FUN_EQ_THM] >>
272  ntac 2 (pop_assum SUBST1_TAC) >> metis_tac[]
273QED
274
275Theorem EXISTS_surj_iff_cimp:
276  surj AB ==> ((AB |==> $=) |==> flip $==>) (?) (?)
277Proof
278  simp[FUN_REL_def, bitotal_def, total_def, surj_def] >> strip_tac >>
279  qx_genl_tac [‘aP’, ‘bP’] >> strip_tac >>
280  ‘aP = (\a. aP a) /\ bP = (\b. bP b)’ by simp[FUN_EQ_THM] >>
281  ntac 2 (pop_assum SUBST1_TAC) >> metis_tac[]
282QED
283
284Theorem EXISTS_surj_cimp_cimp:
285  surj AB ==> ((AB |==> flip $==>) |==> flip $==>) (?) (?)
286Proof
287  simp[FUN_REL_def, bitotal_def, total_def, surj_def] >> strip_tac >>
288  qx_genl_tac [‘aP’, ‘bP’] >> strip_tac >>
289  ‘aP = (\a. aP a) /\ bP = (\b. bP b)’ by simp[FUN_EQ_THM] >>
290  ntac 2 (pop_assum SUBST1_TAC) >> metis_tac[]
291QED
292
293Theorem total_total_sets:
294  total AB /\ left_unique AB ==> total (AB |==> $<=>)
295Proof
296  simp[FUN_REL_def, total_def, left_unique_def] >> rw[] >>
297  qexists_tac ‘{ b | ?a. a IN x /\ AB a b }’  >> simp[IN_DEF] >> metis_tac[]
298QED
299
300Theorem surj_sets:
301  surj AB /\ right_unique AB ==> surj (AB |==> $<=>)
302Proof
303  rw[FUN_REL_def, surj_def, right_unique_def] >>
304  rename [‘AB _ _ ==> (_ _ <=> bset _)’] >>
305  qexists_tac ‘{ a | ?b. bset b /\ AB a b }’ >> simp[] >>
306  metis_tac[]
307QED
308
309(* ----------------------------------------------------------------------
310    Implications
311   ---------------------------------------------------------------------- *)
312
313Theorem cimp_imp:
314  ((==>) |==> flip (==>) |==> flip (==>)) (==>) (==>)
315Proof
316  simp[FUN_REL_def, FORALL_BOOL]
317QED
318
319Theorem eq_imp:
320  ((=) |==> (=) |==> (=)) (==>) (==>)
321Proof
322  simp[FUN_REL_def]
323QED
324
325Theorem imp_conj :
326  ((==>) |==> (==>) |==> (==>)) (/\) (/\)
327Proof
328  simp[FUN_REL_def]
329QED
330
331Theorem imp_disj:
332  ((==>) |==> (==>) |==> (==>)) (\/) (\/)
333Proof
334  simp[FUN_REL_def] >> metis_tac[]
335QED
336
337Theorem cimp_disj:
338  (flip (==>) |==> flip (==>) |==> flip (==>)) (\/) (\/)
339Proof
340  simp[FUN_REL_def] >> metis_tac[]
341QED
342
343(* ----------------------------------------------------------------------
344    COND
345   ---------------------------------------------------------------------- *)
346
347Theorem COND_rule:
348  ((=) |==> AB |==> AB |==> AB) COND COND
349Proof
350  simp[FUN_REL_def] >> rw[] >> rw[]
351QED
352
353(* ----------------------------------------------------------------------
354    Combinators: LET, FUNPOW, ...
355   ---------------------------------------------------------------------- *)
356
357Theorem LET_rule:
358  ((AB |==> CD) |==> (AB |==> CD)) LET LET
359Proof
360  simp[FUN_REL_def]
361QED
362
363Theorem FUNPOW_rule:
364  ((AB |==> AB) |==> (=) |==> AB |==> AB) FUNPOW FUNPOW
365Proof
366  simp[FUN_REL_def] >> rw[] >> rename [‘AB (FUNPOW f n a) (FUNPOW g n b)’] >>
367  qpat_x_assum ‘AB a b’ mp_tac >>
368  map_every qid_spec_tac [‘a’, ‘b’, ‘n’] >> Induct >>
369  simp[arithmeticTheory.FUNPOW_SUC]
370QED
371
372(* ----------------------------------------------------------------------
373    Pairs
374   ---------------------------------------------------------------------- *)
375
376Theorem PAIR_REL_def = pairTheory.PAIR_REL
377Theorem equalityp_PAIR_REL:
378  equalityp AB /\ equalityp CD ==> equalityp (AB ### CD)
379Proof
380  simp[equalityp_def, PAIR_REL_def, FUN_EQ_THM, pairTheory.FORALL_PROD]
381QED
382
383Theorem FST_CORRECT:
384  (PAIR_REL AB CD |==> AB) FST FST
385Proof
386  simp[PAIR_REL_def, FUN_REL_def, pairTheory.FORALL_PROD]
387QED
388
389Theorem SND_CORRECT:
390  (PAIR_REL AB CD |==> CD) SND SND
391Proof
392  simp[PAIR_REL_def, FUN_REL_def, pairTheory.FORALL_PROD]
393QED
394
395Theorem COMMA_CORRECT:
396  (AB |==> CD |==> PAIR_REL AB CD) $, $,
397Proof
398  simp[PAIR_REL_def, FUN_REL_def, pairTheory.FORALL_PROD]
399QED
400
401Definition PAIRU_def:
402  PAIRU AB (a,()) b <=> AB a b
403End
404
405Theorem PAIRU_COMMA:
406  (AB |==> (=) |==> PAIRU AB) $, K
407Proof
408  simp[PAIRU_def, pairTheory.FORALL_PROD, FUN_REL_def]
409QED
410
411Definition UPAIR_def:
412  UPAIR AB ((),a) b <=> AB a b
413End
414
415Theorem UPAIR_COMMA:
416  ((=) |==> AB |==> UPAIR AB) $, (K I)
417Proof
418  simp[UPAIR_def, pairTheory.FORALL_PROD, FUN_REL_def]
419QED
420
421Theorem pair_CASE_CONG:
422  ((AB ### CD) |==> (AB |==> CD |==> EF) |==> EF) pair_CASE pair_CASE
423Proof
424  simp[FUN_REL_def, pairTheory.FORALL_PROD]
425QED
426
427(* ----------------------------------------------------------------------
428    Unit
429   ---------------------------------------------------------------------- *)
430
431Theorem UREL_EQ:
432  () = ()
433Proof simp[]
434QED
435
436(* ----------------------------------------------------------------------
437    Options
438   ---------------------------------------------------------------------- *)
439
440Theorem OPTREL_MAP:
441  ((AB |==> CD) |==> OPTREL AB |==> OPTREL CD) OPTION_MAP OPTION_MAP
442Proof
443  simp[FUN_REL_def] >> simp[optionTheory.FORALL_OPTION]
444QED
445
446Theorem OPTREL_total:
447  total AB ==> total (OPTREL AB)
448Proof
449  simp[optionTheory.OPTREL_def, total_def, EXISTS_OR_THM] >> strip_tac >>
450  Cases >> simp[]
451QED
452
453Theorem OPTREL_surj:
454  surj AB ==> surj (OPTREL AB)
455Proof
456  simp[optionTheory.OPTREL_def, surj_def, EXISTS_OR_THM] >> strip_tac >>
457  Cases >> simp[]
458QED
459
460Theorem OPTREL_left_unique:
461  left_unique AB ==> left_unique (OPTREL AB)
462Proof
463  simp[left_unique_def, optionTheory.OPTREL_def, optionTheory.FORALL_OPTION]
464QED
465
466Theorem OPTREL_right_unique:
467  right_unique AB ==> right_unique (OPTREL AB)
468Proof
469  simp[right_unique_def, optionTheory.OPTREL_def, optionTheory.FORALL_OPTION]
470QED
471
472Theorem equalityp_OPTREL:
473  equalityp AB ==> equalityp (OPTREL AB)
474Proof
475  simp[equalityp_def]
476QED
477
478Theorem option_CASE_CONG:
479  (OPTREL AB |==> CD |==> (AB |==> CD) |==> CD) option_CASE option_CASE
480Proof
481  simp[FUN_REL_def, optionTheory.FORALL_OPTION]
482QED
483
484Theorem OPTION_BIND_rule:
485  (OPTREL AB |==> (AB |==> OPTREL CD) |==> OPTREL CD) OPTION_BIND OPTION_BIND
486Proof
487  simp[FUN_REL_def] >> rw[optionTheory.OPTREL_def]
488QED
489
490Theorem NONE_rule:
491  OPTREL AB NONE NONE
492Proof
493  simp[]
494QED
495
496Theorem SOME_rule:
497  (AB |==> OPTREL AB) SOME SOME
498Proof
499  simp[FUN_REL_def]
500QED
501
502
503
504(* ----------------------------------------------------------------------
505    Lists
506   ---------------------------------------------------------------------- *)
507
508Theorem equalityp_LIST_REL:
509  equalityp AB ==> equalityp (LIST_REL AB)
510Proof
511  simp[equalityp_def]
512QED
513
514Theorem LIST_REL_right_unique:
515  right_unique AB ==> right_unique (LIST_REL AB)
516Proof
517  simp[right_unique_def] >> strip_tac >> Induct >> simp[PULL_EXISTS] >>
518  metis_tac[]
519QED
520
521Theorem LIST_REL_left_unique:
522  left_unique AB ==> left_unique (LIST_REL AB)
523Proof
524  simp[left_unique_def] >> strip_tac >> Induct_on ‘LIST_REL’ >>
525  simp[PULL_EXISTS] >> metis_tac[]
526QED
527
528Theorem LIST_REL_surj:
529  surj AB ==> surj (LIST_REL AB)
530Proof
531  simp[surj_def] >> strip_tac >> Induct >> simp[PULL_EXISTS] >> metis_tac[]
532QED
533
534Theorem LIST_REL_total:
535  total AB ==> total (LIST_REL AB)
536Proof
537  simp[total_def] >> strip_tac >> Induct >> simp[] >> metis_tac[]
538QED
539
540Theorem list_CASE_CONG:
541  (LIST_REL AB |==> CD |==> (AB |==> LIST_REL AB |==> CD) |==> CD)
542    list_CASE
543    list_CASE
544Proof
545  simp[FUN_REL_def, Once listTheory.FORALL_LIST, PULL_EXISTS]
546QED
547
548Theorem NIL_rule:
549  LIST_REL AB [] []
550Proof
551  simp[]
552QED
553
554Theorem CONS_rule:
555  (AB |==> LIST_REL AB |==> LIST_REL AB) CONS CONS
556Proof
557  simp[FUN_REL_def]
558QED
559
560Theorem TL_rule:
561  (LIST_REL AB |==> LIST_REL AB) TL TL
562Proof
563  simp[FUN_REL_def] >> Cases >> Cases >> simp[]
564QED
565
566Theorem LENGTH_rule:
567  (LIST_REL AB |==> (=)) LENGTH LENGTH
568Proof
569  simp[FUN_REL_def, SF SFY_ss, listTheory.EVERY2_LENGTH]
570QED
571
572Theorem FOLDL_rule:
573  ((CD |==> AB |==> CD) |==> CD |==> LIST_REL AB |==> CD) FOLDL FOLDL
574Proof
575  simp[FUN_REL_def] >> rw[] >> rename [‘CD (FOLDL f A xs) (FOLDL g B ys)’] >>
576  map_every (C qpat_x_assum mp_tac) [‘CD A B’, ‘LIST_REL _ _ _’] >>
577  map_every qid_spec_tac [‘xs’, ‘ys’, ‘A’, ‘B’] >>
578  Induct_on ‘LIST_REL’ >> simp[]
579QED
580
581Theorem FOLDR_rule:
582  ((AB |==> CD |==> CD) |==> CD |==> LIST_REL AB |==> CD) FOLDR FOLDR
583Proof
584  simp[FUN_REL_def] >> rw[] >> rename [‘CD (FOLDR f A xs) (FOLDR g B ys)’] >>
585  map_every (C qpat_x_assum mp_tac) [‘CD A B’, ‘LIST_REL _ _ _’] >>
586  map_every qid_spec_tac [‘xs’, ‘ys’, ‘A’, ‘B’] >>
587  Induct_on ‘LIST_REL’ >> simp[]
588QED
589
590Theorem MAP_rule:
591  ((AB |==> CD) |==> LIST_REL AB |==> LIST_REL CD) MAP MAP
592Proof
593  simp[FUN_REL_def] >> rw[] >> rename [‘LIST_REL CD (MAP f xs) (MAP g ys)’] >>
594  qpat_x_assum ‘LIST_REL _ _ _ ’ mp_tac >>
595  Induct_on ‘LIST_REL’ >> simp[]
596QED
597
598Theorem ALL_DISTINCT_rule:
599  left_unique AB ==> right_unique AB ==>
600  (LIST_REL AB |==> (=)) ALL_DISTINCT ALL_DISTINCT
601Proof
602  rw[left_unique_def, right_unique_def, FUN_REL_def] >>
603  qpat_x_assum ‘LIST_REL _ _ _ ’ mp_tac >> Induct_on ‘LIST_REL’ >>
604  simp[] >> rw[] >> iff_tac >> rw[] >>
605  metis_tac[listTheory.LIST_REL_MEM_IMP_R, listTheory.LIST_REL_MEM_IMP]
606QED
607