56 apply(rule allI)+ |
56 apply(rule allI)+ |
57 apply(rule list_rel_rel[OF q]) |
57 apply(rule list_rel_rel[OF q]) |
58 done |
58 done |
59 |
59 |
60 |
60 |
|
61 lemma cons_prs: |
|
62 assumes q: "Quotient R Abs Rep" |
|
63 shows "(map Abs) ((Rep h) # (map Rep t)) = h # t" |
|
64 by (induct t) (simp_all add: Quotient_abs_rep[OF q]) |
61 |
65 |
|
66 lemma cons_rsp: |
|
67 assumes q: "Quotient R Abs Rep" |
|
68 shows "(R ===> list_rel R ===> list_rel R) op # op #" |
|
69 by (auto) |
62 |
70 |
63 |
71 lemma nil_prs: |
64 |
|
65 (* Rest is not used *) |
|
66 |
|
67 |
|
68 lemma CONS_PRS: |
|
69 assumes q: "Quotient R Abs Rep" |
72 assumes q: "Quotient R Abs Rep" |
70 shows "(h#t) = (map Abs) ((Rep h)#(map Rep t))" |
73 shows "map Abs [] \<equiv> []" |
71 by (induct t) (simp_all add: Quotient_ABS_REP[OF q]) |
|
72 |
|
73 lemma CONS_RSP: |
|
74 assumes q: "Quotient R Abs Rep" |
|
75 and a: "R h1 h2" "list_rel R t1 t2" |
|
76 shows "list_rel R (h1#t1) (h2#t2)" |
|
77 using a by (auto) |
|
78 |
|
79 lemma NIL_PRS: |
|
80 assumes q: "Quotient R Abs Rep" |
|
81 shows "[] = (map Abs [])" |
|
82 by (simp) |
74 by (simp) |
83 |
75 |
84 lemma NIL_RSP: |
76 lemma nil_rsp: |
85 assumes q: "Quotient R Abs Rep" |
77 assumes q: "Quotient R Abs Rep" |
86 shows "list_rel R [] []" |
78 shows "list_rel R [] []" |
87 by simp |
79 by simp |
88 |
80 |
89 lemma MAP_PRS: |
81 lemma map_prs: |
90 assumes q1: "Quotient R1 Abs1 Rep1" |
82 assumes a: "Quotient R1 abs1 rep1" |
91 and q2: "Quotient R2 Abs2 Rep2" |
83 and b: "Quotient R2 abs2 rep2" |
92 shows "map f l = (map Abs2) (map ((Abs1 ---> Rep2) f) (map Rep1 l))" |
84 shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l" |
93 by (induct l) |
85 by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
94 (simp_all add: Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2]) |
|
95 |
86 |
96 lemma MAP_RSP: |
87 (* We need an ho version *) |
|
88 lemma map_rsp: |
97 assumes q1: "Quotient R1 Abs1 Rep1" |
89 assumes q1: "Quotient R1 Abs1 Rep1" |
98 and q2: "Quotient R2 Abs2 Rep2" |
90 and q2: "Quotient R2 Abs2 Rep2" |
99 and a: "(R1 ===> R2) f1 f2" |
91 and a: "(R1 ===> R2) f1 f2" |
100 and b: "list_rel R1 l1 l2" |
92 and b: "list_rel R1 l1 l2" |
101 shows "list_rel R2 (map f1 l1) (map f2 l2)" |
93 shows "list_rel R2 (map f1 l1) (map f2 l2)" |
102 using b a |
94 using b a |
103 by (induct l1 l2 rule: list_induct2') |
95 by (induct l1 l2 rule: list_induct2') (simp_all) |
104 (simp_all) |
96 |
|
97 lemma foldr_prs: |
|
98 assumes a: "Quotient R1 abs1 rep1" |
|
99 and b: "Quotient R2 abs2 rep2" |
|
100 shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e" |
|
101 by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
|
102 |
|
103 lemma foldl_prs: |
|
104 assumes a: "Quotient R1 abs1 rep1" |
|
105 and b: "Quotient R2 abs2 rep2" |
|
106 shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l" |
|
107 by (induct l arbitrary:e) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
105 |
108 |
106 |
109 |
|
110 |
|
111 |
|
112 |
|
113 |
|
114 |
|
115 (* TODO: Rest are unused *) |
107 |
116 |
108 lemma LIST_map_id: |
117 lemma LIST_map_id: |
109 shows "map (\<lambda>x. x) = (\<lambda>x. x)" |
118 shows "map (\<lambda>x. x) = (\<lambda>x. x)" |
110 by simp |
119 by simp |
111 |
120 |