5 lemma LIST_map_id: |
5 lemma LIST_map_id: |
6 shows "map (\<lambda>x. x) = (\<lambda>x. x)" |
6 shows "map (\<lambda>x. x) = (\<lambda>x. x)" |
7 by simp |
7 by simp |
8 |
8 |
9 fun |
9 fun |
10 LIST_REL |
10 list_rel |
11 where |
11 where |
12 "LIST_REL R [] [] = True" |
12 "list_rel R [] [] = True" |
13 | "LIST_REL R (x#xs) [] = False" |
13 | "list_rel R (x#xs) [] = False" |
14 | "LIST_REL R [] (x#xs) = False" |
14 | "list_rel R [] (x#xs) = False" |
15 | "LIST_REL R (x#xs) (y#ys) = (R x y \<and> LIST_REL R xs ys)" |
15 | "list_rel R (x#xs) (y#ys) = (R x y \<and> list_rel R xs ys)" |
16 |
16 |
17 lemma LIST_REL_EQ: |
17 lemma list_rel_EQ: |
18 shows "LIST_REL (op =) \<equiv> (op =)" |
18 shows "list_rel (op =) \<equiv> (op =)" |
19 apply(rule eq_reflection) |
19 apply(rule eq_reflection) |
20 unfolding expand_fun_eq |
20 unfolding expand_fun_eq |
21 apply(rule allI)+ |
21 apply(rule allI)+ |
22 apply(induct_tac x xa rule: list_induct2') |
22 apply(induct_tac x xa rule: list_induct2') |
23 apply(simp_all) |
23 apply(simp_all) |
24 done |
24 done |
25 |
25 |
26 lemma LIST_REL_REFL: |
26 lemma list_rel_REFL: |
27 assumes a: "\<And>x y. R x y = (R x = R y)" |
27 assumes a: "\<And>x y. R x y = (R x = R y)" |
28 shows "LIST_REL R x x" |
28 shows "list_rel R x x" |
29 by (induct x) (auto simp add: a) |
29 by (induct x) (auto simp add: a) |
30 |
30 |
31 lemma LIST_equivp: |
31 lemma LIST_equivp: |
32 assumes a: "equivp R" |
32 assumes a: "equivp R" |
33 shows "equivp (LIST_REL R)" |
33 shows "equivp (list_rel R)" |
34 unfolding equivp_def |
34 unfolding equivp_def |
35 apply(rule allI)+ |
35 apply(rule allI)+ |
36 apply(induct_tac x y rule: list_induct2') |
36 apply(induct_tac x y rule: list_induct2') |
37 apply(simp) |
37 apply(simp) |
38 apply(simp add: expand_fun_eq) |
38 apply(simp add: expand_fun_eq) |
39 apply(metis LIST_REL.simps(1) LIST_REL.simps(2)) |
39 apply(metis list_rel.simps(1) list_rel.simps(2)) |
40 apply(simp add: expand_fun_eq) |
40 apply(simp add: expand_fun_eq) |
41 apply(metis LIST_REL.simps(1) LIST_REL.simps(2)) |
41 apply(metis list_rel.simps(1) list_rel.simps(2)) |
42 apply(simp add: expand_fun_eq) |
42 apply(simp add: expand_fun_eq) |
43 apply(rule iffI) |
43 apply(rule iffI) |
44 apply(rule allI) |
44 apply(rule allI) |
45 apply(case_tac x) |
45 apply(case_tac x) |
46 apply(simp) |
46 apply(simp) |
47 apply(simp) |
47 apply(simp) |
48 using a |
48 using a |
49 apply(unfold equivp_def) |
49 apply(unfold equivp_def) |
50 apply(auto)[1] |
50 apply(auto)[1] |
51 apply(metis LIST_REL.simps(4)) |
51 apply(metis list_rel.simps(4)) |
52 done |
52 done |
53 |
53 |
54 lemma LIST_REL_REL: |
54 lemma list_rel_REL: |
55 assumes q: "Quotient R Abs Rep" |
55 assumes q: "Quotient R Abs Rep" |
56 shows "LIST_REL R r s = (LIST_REL R r r \<and> LIST_REL R s s \<and> (map Abs r = map Abs s))" |
56 shows "list_rel R r s = (list_rel R r r \<and> list_rel R s s \<and> (map Abs r = map Abs s))" |
57 apply(induct r s rule: list_induct2') |
57 apply(induct r s rule: list_induct2') |
58 apply(simp_all) |
58 apply(simp_all) |
59 using Quotient_REL[OF q] |
59 using Quotient_REL[OF q] |
60 apply(metis) |
60 apply(metis) |
61 done |
61 done |
62 |
62 |
63 lemma LIST_Quotient: |
63 lemma list_quotient: |
64 assumes q: "Quotient R Abs Rep" |
64 assumes q: "Quotient R Abs Rep" |
65 shows "Quotient (LIST_REL R) (map Abs) (map Rep)" |
65 shows "Quotient (list_rel R) (map Abs) (map Rep)" |
66 unfolding Quotient_def |
66 unfolding Quotient_def |
67 apply(rule conjI) |
67 apply(rule conjI) |
68 apply(rule allI) |
68 apply(rule allI) |
69 apply(induct_tac a) |
69 apply(induct_tac a) |
70 apply(simp) |
70 apply(simp) |
74 apply(induct_tac a) |
74 apply(induct_tac a) |
75 apply(simp) |
75 apply(simp) |
76 apply(simp) |
76 apply(simp) |
77 apply(simp add: Quotient_REP_reflp[OF q]) |
77 apply(simp add: Quotient_REP_reflp[OF q]) |
78 apply(rule allI)+ |
78 apply(rule allI)+ |
79 apply(rule LIST_REL_REL[OF q]) |
79 apply(rule list_rel_REL[OF q]) |
80 done |
80 done |
81 |
81 |
82 lemma CONS_PRS: |
82 lemma CONS_PRS: |
83 assumes q: "Quotient R Abs Rep" |
83 assumes q: "Quotient R Abs Rep" |
84 shows "(h#t) = (map Abs) ((Rep h)#(map Rep t))" |
84 shows "(h#t) = (map Abs) ((Rep h)#(map Rep t))" |
85 by (induct t) (simp_all add: Quotient_ABS_REP[OF q]) |
85 by (induct t) (simp_all add: Quotient_ABS_REP[OF q]) |
86 |
86 |
87 lemma CONS_RSP: |
87 lemma CONS_RSP: |
88 assumes q: "Quotient R Abs Rep" |
88 assumes q: "Quotient R Abs Rep" |
89 and a: "R h1 h2" "LIST_REL R t1 t2" |
89 and a: "R h1 h2" "list_rel R t1 t2" |
90 shows "LIST_REL R (h1#t1) (h2#t2)" |
90 shows "list_rel R (h1#t1) (h2#t2)" |
91 using a by (auto) |
91 using a by (auto) |
92 |
92 |
93 lemma NIL_PRS: |
93 lemma NIL_PRS: |
94 assumes q: "Quotient R Abs Rep" |
94 assumes q: "Quotient R Abs Rep" |
95 shows "[] = (map Abs [])" |
95 shows "[] = (map Abs [])" |
96 by (simp) |
96 by (simp) |
97 |
97 |
98 lemma NIL_RSP: |
98 lemma NIL_RSP: |
99 assumes q: "Quotient R Abs Rep" |
99 assumes q: "Quotient R Abs Rep" |
100 shows "LIST_REL R [] []" |
100 shows "list_rel R [] []" |
101 by simp |
101 by simp |
102 |
102 |
103 lemma MAP_PRS: |
103 lemma MAP_PRS: |
104 assumes q1: "Quotient R1 Abs1 Rep1" |
104 assumes q1: "Quotient R1 Abs1 Rep1" |
105 and q2: "Quotient R2 Abs2 Rep2" |
105 and q2: "Quotient R2 Abs2 Rep2" |
108 (simp_all add: Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2]) |
108 (simp_all add: Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2]) |
109 |
109 |
110 lemma MAP_RSP: |
110 lemma MAP_RSP: |
111 assumes q1: "Quotient R1 Abs1 Rep1" |
111 assumes q1: "Quotient R1 Abs1 Rep1" |
112 and q2: "Quotient R2 Abs2 Rep2" |
112 and q2: "Quotient R2 Abs2 Rep2" |
113 and a: "(R1 ===> R2) f1 f2" |
113 and a: "(R1 ===> R2) f1 f2" |
114 and b: "LIST_REL R1 l1 l2" |
114 and b: "list_rel R1 l1 l2" |
115 shows "LIST_REL R2 (map f1 l1) (map f2 l2)" |
115 shows "list_rel R2 (map f1 l1) (map f2 l2)" |
116 using b a |
116 using b a |
117 by (induct l1 l2 rule: list_induct2') |
117 by (induct l1 l2 rule: list_induct2') |
118 (simp_all) |
118 (simp_all) |
119 |
119 |
120 |
120 |