1 (* Title: ZF/ex/rmap |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Inductive definition of an operator to "map" a relation over a list |
|
7 *) |
|
8 |
|
9 structure Rmap = Inductive_Fun |
|
10 (val thy = List.thy addconsts [(["rmap"],"i=>i")]; |
|
11 val rec_doms = [("rmap", "list(domain(r))*list(range(r))")]; |
|
12 val sintrs = |
|
13 ["<Nil,Nil> : rmap(r)", |
|
14 |
|
15 "[| <x,y>: r; <xs,ys> : rmap(r) |] ==> \ |
|
16 \ <Cons(x,xs), Cons(y,ys)> : rmap(r)"]; |
|
17 val monos = []; |
|
18 val con_defs = []; |
|
19 val type_intrs = [domainI,rangeI] @ List.intrs @ [SigmaI] |
|
20 val type_elims = [SigmaE2]); |
|
21 |
|
22 goalw Rmap.thy Rmap.defs "!!r s. r<=s ==> rmap(r) <= rmap(s)"; |
|
23 by (rtac lfp_mono 1); |
|
24 by (REPEAT (rtac Rmap.bnd_mono 1)); |
|
25 by (REPEAT (ares_tac ([Sigma_mono, list_mono, domain_mono, range_mono] @ |
|
26 basic_monos) 1)); |
|
27 val rmap_mono = result(); |
|
28 |
|
29 val rmap_induct = standard |
|
30 (Rmap.mutual_induct RS spec RS spec RSN (2,rev_mp)); |
|
31 |
|
32 val Nil_rmap_case = Rmap.mk_cases List.con_defs "<Nil,zs> : rmap(r)" |
|
33 and Cons_rmap_case = Rmap.mk_cases List.con_defs "<Cons(x,xs),zs> : rmap(r)"; |
|
34 |
|
35 val rmap_cs = ZF_cs addIs Rmap.intrs |
|
36 addSEs [Nil_rmap_case, Cons_rmap_case]; |
|
37 |
|
38 goal Rmap.thy "!!r. r <= A*B ==> rmap(r) <= list(A)*list(B)"; |
|
39 by (rtac (Rmap.dom_subset RS subset_trans) 1); |
|
40 by (REPEAT (ares_tac [domain_rel_subset, range_rel_subset, |
|
41 Sigma_mono, list_mono] 1)); |
|
42 val rmap_rel_type = result(); |
|
43 |
|
44 goal Rmap.thy |
|
45 "!!r. [| ALL x:A. EX y. <x,y>: r; xs: list(A) |] ==> \ |
|
46 \ EX y. <xs, y> : rmap(r)"; |
|
47 by (etac List.induct 1); |
|
48 by (ALLGOALS (fast_tac rmap_cs)); |
|
49 val rmap_total = result(); |
|
50 |
|
51 goal Rmap.thy |
|
52 "!!r. [| ALL x y z. <x,y>: r --> <x,z>: r --> y=z; \ |
|
53 \ <xs, ys> : rmap(r) |] ==> \ |
|
54 \ ALL zs. <xs, zs> : rmap(r) --> ys=zs"; |
|
55 by (etac rmap_induct 1); |
|
56 by (ALLGOALS (fast_tac rmap_cs)); |
|
57 val rmap_functional_lemma = result(); |
|
58 val rmap_functional = standard (rmap_functional_lemma RS spec RS mp); |
|
59 |
|
60 (** If f is a function then rmap(f) behaves as expected. **) |
|
61 |
|
62 goal Rmap.thy "!!f. f: A->B ==> rmap(f): list(A)->list(B)"; |
|
63 by (etac PiE 1); |
|
64 by (rtac PiI 1); |
|
65 by (etac rmap_rel_type 1); |
|
66 by (rtac (rmap_total RS ex_ex1I) 1); |
|
67 by (assume_tac 2); |
|
68 by (fast_tac (ZF_cs addSEs [bspec RS ex1E]) 1); |
|
69 by (rtac rmap_functional 1); |
|
70 by (REPEAT (assume_tac 2)); |
|
71 by (fast_tac (ZF_cs addSEs [bspec RS ex1_equalsE]) 1); |
|
72 val rmap_fun_type = result(); |
|
73 |
|
74 goalw Rmap.thy [apply_def] "rmap(f)`Nil = Nil"; |
|
75 by (fast_tac (rmap_cs addIs [the_equality]) 1); |
|
76 val rmap_Nil = result(); |
|
77 |
|
78 goal Rmap.thy "!!f. [| f: A->B; x: A; xs: list(A) |] ==> \ |
|
79 \ rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)"; |
|
80 by (rtac apply_equality 1); |
|
81 by (REPEAT (ares_tac ([apply_Pair, rmap_fun_type] @ Rmap.intrs) 1)); |
|
82 val rmap_Cons = result(); |
|