10 | "list_rel R [] (x#xs) = False" |
10 | "list_rel R [] (x#xs) = False" |
11 | "list_rel R (x#xs) (y#ys) = (R x y \<and> list_rel R xs ys)" |
11 | "list_rel R (x#xs) (y#ys) = (R x y \<and> list_rel R xs ys)" |
12 |
12 |
13 declare [[map list = (map, list_rel)]] |
13 declare [[map list = (map, list_rel)]] |
14 |
14 |
|
15 |
|
16 |
|
17 text {* should probably be in Sum_Type.thy *} |
|
18 lemma split_list_all: |
|
19 shows "(\<forall>x. P x) \<longleftrightarrow> P [] \<and> (\<forall>x xs. P (x#xs))" |
|
20 apply(auto) |
|
21 apply(case_tac x) |
|
22 apply(simp_all) |
|
23 done |
|
24 |
|
25 lemma map_id[id_simps]: "map id \<equiv> id" |
|
26 apply(rule eq_reflection) |
|
27 apply(simp add: expand_fun_eq) |
|
28 apply(rule allI) |
|
29 apply(induct_tac x) |
|
30 apply(simp_all) |
|
31 done |
|
32 |
|
33 |
|
34 lemma list_rel_reflp: |
|
35 shows "equivp R \<Longrightarrow> list_rel R xs xs" |
|
36 apply(induct xs) |
|
37 apply(simp_all add: equivp_reflp) |
|
38 done |
|
39 |
|
40 lemma list_rel_symp: |
|
41 assumes a: "equivp R" |
|
42 shows "list_rel R xs ys \<Longrightarrow> list_rel R ys xs" |
|
43 apply(induct xs ys rule: list_induct2') |
|
44 apply(simp_all) |
|
45 apply(rule equivp_symp[OF a]) |
|
46 apply(simp) |
|
47 done |
|
48 |
|
49 lemma list_rel_transp: |
|
50 assumes a: "equivp R" |
|
51 shows "list_rel R xs1 xs2 \<Longrightarrow> list_rel R xs2 xs3 \<Longrightarrow> list_rel R xs1 xs3" |
|
52 apply(induct xs1 xs2 arbitrary: xs3 rule: list_induct2') |
|
53 apply(simp_all) |
|
54 apply(case_tac xs3) |
|
55 apply(simp_all) |
|
56 apply(rule equivp_transp[OF a]) |
|
57 apply(auto) |
|
58 done |
|
59 |
15 lemma list_equivp[quot_equiv]: |
60 lemma list_equivp[quot_equiv]: |
16 assumes a: "equivp R" |
61 assumes a: "equivp R" |
17 shows "equivp (list_rel R)" |
62 shows "equivp (list_rel R)" |
18 unfolding equivp_def |
63 apply(rule equivpI) |
19 apply(rule allI)+ |
64 unfolding reflp_def symp_def transp_def |
20 apply(induct_tac x y rule: list_induct2') |
65 apply(subst split_list_all) |
21 apply(simp_all add: expand_fun_eq) |
66 apply(simp add: equivp_reflp[OF a] list_rel_reflp[OF a]) |
22 apply(metis list_rel.simps(1) list_rel.simps(2)) |
67 apply(blast intro: list_rel_symp[OF a]) |
23 apply(metis list_rel.simps(1) list_rel.simps(2)) |
68 apply(blast intro: list_rel_transp[OF a]) |
24 apply(rule iffI) |
|
25 apply(rule allI) |
|
26 apply(case_tac x) |
|
27 apply(simp_all) |
|
28 using a |
|
29 apply(unfold equivp_def) |
|
30 apply(auto)[1] |
|
31 apply(metis list_rel.simps(4)) |
|
32 done |
69 done |
33 |
70 |
34 lemma list_rel_rel: |
71 lemma list_rel_rel: |
35 assumes q: "Quotient R Abs Rep" |
72 assumes q: "Quotient R Abs Rep" |
36 shows "list_rel R r s = (list_rel R r r \<and> list_rel R s s \<and> (map Abs r = map Abs s))" |
73 shows "list_rel R r s = (list_rel R r r \<and> list_rel R s s \<and> (map Abs r = map Abs s))" |
42 |
79 |
43 lemma list_quotient[quot_thm]: |
80 lemma list_quotient[quot_thm]: |
44 assumes q: "Quotient R Abs Rep" |
81 assumes q: "Quotient R Abs Rep" |
45 shows "Quotient (list_rel R) (map Abs) (map Rep)" |
82 shows "Quotient (list_rel R) (map Abs) (map Rep)" |
46 unfolding Quotient_def |
83 unfolding Quotient_def |
|
84 apply(subst split_list_all) |
|
85 apply(simp add: Quotient_abs_rep[OF q] abs_o_rep[OF q] map_id) |
47 apply(rule conjI) |
86 apply(rule conjI) |
48 apply(rule allI) |
87 apply(rule allI) |
49 apply(induct_tac a) |
88 apply(induct_tac a) |
50 apply(simp) |
89 apply(simp) |
51 apply(simp add: Quotient_abs_rep[OF q]) |
|
52 apply(rule conjI) |
|
53 apply(rule allI) |
|
54 apply(induct_tac a) |
|
55 apply(simp) |
|
56 apply(simp) |
90 apply(simp) |
57 apply(simp add: Quotient_rep_reflp[OF q]) |
91 apply(simp add: Quotient_rep_reflp[OF q]) |
58 apply(rule allI)+ |
92 apply(rule allI)+ |
59 apply(rule list_rel_rel[OF q]) |
93 apply(rule list_rel_rel[OF q]) |
60 done |
94 done |
61 |
95 |
62 lemma map_id[id_simps]: "map id \<equiv> id" |
|
63 apply (rule eq_reflection) |
|
64 apply (rule ext) |
|
65 apply (rule_tac list="x" in list.induct) |
|
66 apply (simp_all) |
|
67 done |
|
68 |
96 |
69 lemma cons_prs_aux: |
97 lemma cons_prs_aux: |
70 assumes q: "Quotient R Abs Rep" |
98 assumes q: "Quotient R Abs Rep" |
71 shows "(map Abs) ((Rep h) # (map Rep t)) = h # t" |
99 shows "(map Abs) ((Rep h) # (map Rep t)) = h # t" |
72 by (induct t) (simp_all add: Quotient_abs_rep[OF q]) |
100 by (induct t) (simp_all add: Quotient_abs_rep[OF q]) |
73 |
101 |
74 lemma cons_prs[quot_preserve]: |
102 lemma cons_prs[quot_preserve]: |
75 assumes q: "Quotient R Abs Rep" |
103 assumes q: "Quotient R Abs Rep" |
76 shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)" |
104 shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)" |
77 by (simp only: expand_fun_eq fun_map_def cons_prs_aux[OF q]) |
105 by (simp only: expand_fun_eq fun_map_def cons_prs_aux[OF q]) |
78 (simp) |
106 (simp) |
79 |
107 |
80 lemma cons_rsp[quot_respect]: |
108 lemma cons_rsp[quot_respect]: |
81 assumes q: "Quotient R Abs Rep" |
109 assumes q: "Quotient R Abs Rep" |
82 shows "(R ===> list_rel R ===> list_rel R) op # op #" |
110 shows "(R ===> list_rel R ===> list_rel R) (op #) (op #)" |
83 by (auto) |
111 by (auto) |
84 |
112 |
85 lemma nil_prs[quot_preserve]: |
113 lemma nil_prs[quot_preserve]: |
86 assumes q: "Quotient R Abs Rep" |
114 assumes q: "Quotient R Abs Rep" |
87 shows "map Abs [] \<equiv> []" |
115 shows "map Abs [] \<equiv> []" |
88 by (simp) |
116 by (simp) |
89 |
117 |
90 lemma nil_rsp[quot_respect]: |
118 lemma nil_rsp[quot_respect]: |
91 assumes q: "Quotient R Abs Rep" |
119 assumes q: "Quotient R Abs Rep" |
92 shows "list_rel R [] []" |
120 shows "list_rel R [] []" |
93 by simp |
121 by simp |
94 |
122 |
95 lemma map_prs_aux: |
123 lemma map_prs_aux: |
96 assumes a: "Quotient R1 abs1 rep1" |
124 assumes a: "Quotient R1 abs1 rep1" |
97 and b: "Quotient R2 abs2 rep2" |
125 and b: "Quotient R2 abs2 rep2" |
98 shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l" |
126 shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l" |
99 by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
127 by (induct l) |
|
128 (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
100 |
129 |
101 |
130 |
102 lemma map_prs[quot_preserve]: |
131 lemma map_prs[quot_preserve]: |
103 assumes a: "Quotient R1 abs1 rep1" |
132 assumes a: "Quotient R1 abs1 rep1" |
104 and b: "Quotient R2 abs2 rep2" |
133 and b: "Quotient R2 abs2 rep2" |
105 shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map" |
134 shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map" |
106 by (simp only: expand_fun_eq fun_map_def map_prs_aux[OF a b]) |
135 by (simp only: expand_fun_eq fun_map_def map_prs_aux[OF a b]) |
107 (simp) |
136 (simp) |
108 |
137 |
109 |
138 |
110 lemma map_rsp[quot_respect]: |
139 lemma map_rsp[quot_respect]: |
111 assumes q1: "Quotient R1 Abs1 Rep1" |
140 assumes q1: "Quotient R1 Abs1 Rep1" |
112 and q2: "Quotient R2 Abs2 Rep2" |
141 and q2: "Quotient R2 Abs2 Rep2" |
113 shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map" |
142 shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map" |
114 apply(simp) |
143 apply(simp) |
115 apply(rule allI)+ |
144 apply(rule allI)+ |
116 apply(rule impI) |
145 apply(rule impI) |
117 apply(rule allI)+ |
146 apply(rule allI)+ |
118 apply (induct_tac xa ya rule: list_induct2') |
147 apply (induct_tac xa ya rule: list_induct2') |
119 apply simp_all |
148 apply simp_all |
120 done |
149 done |
121 |
150 |
122 lemma foldr_prs_aux: |
151 lemma foldr_prs_aux: |
123 assumes a: "Quotient R1 abs1 rep1" |
152 assumes a: "Quotient R1 abs1 rep1" |
124 and b: "Quotient R2 abs2 rep2" |
153 and b: "Quotient R2 abs2 rep2" |
125 shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e" |
154 shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e" |
126 by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
155 by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
127 |
156 |
128 lemma foldr_prs[quot_preserve]: |
157 lemma foldr_prs[quot_preserve]: |
129 assumes a: "Quotient R1 abs1 rep1" |
158 assumes a: "Quotient R1 abs1 rep1" |
130 and b: "Quotient R2 abs2 rep2" |
159 and b: "Quotient R2 abs2 rep2" |
131 shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr" |
160 shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr" |
132 by (simp only: expand_fun_eq fun_map_def foldr_prs_aux[OF a b]) |
161 by (simp only: expand_fun_eq fun_map_def foldr_prs_aux[OF a b]) |
133 (simp) |
162 (simp) |
134 |
163 |
135 lemma foldl_prs_aux: |
164 lemma foldl_prs_aux: |
136 assumes a: "Quotient R1 abs1 rep1" |
165 assumes a: "Quotient R1 abs1 rep1" |
137 and b: "Quotient R2 abs2 rep2" |
166 and b: "Quotient R2 abs2 rep2" |
138 shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l" |
167 shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l" |
139 by (induct l arbitrary:e) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
168 by (induct l arbitrary:e) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
140 |
169 |
141 |
170 |
142 lemma foldl_prs[quot_preserve]: |
171 lemma foldl_prs[quot_preserve]: |
143 assumes a: "Quotient R1 abs1 rep1" |
172 assumes a: "Quotient R1 abs1 rep1" |
144 and b: "Quotient R2 abs2 rep2" |
173 and b: "Quotient R2 abs2 rep2" |
145 shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl" |
174 shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl" |
146 by (simp only: expand_fun_eq fun_map_def foldl_prs_aux[OF a b]) |
175 by (simp only: expand_fun_eq fun_map_def foldl_prs_aux[OF a b]) |
147 (simp) |
176 (simp) |
148 |
177 |
149 lemma list_rel_empty: "list_rel R [] b \<Longrightarrow> length b = 0" |
178 lemma list_rel_empty: |
150 by (induct b) (simp_all) |
179 shows "list_rel R [] b \<Longrightarrow> length b = 0" |
151 |
180 by (induct b) (simp_all) |
152 lemma list_rel_len: "list_rel R a b \<Longrightarrow> length a = length b" |
181 |
153 apply (induct a arbitrary: b) |
182 lemma list_rel_len: |
154 apply (simp add: list_rel_empty) |
183 shows "list_rel R a b \<Longrightarrow> length a = length b" |
155 apply (case_tac b) |
184 apply (induct a arbitrary: b) |
156 apply simp_all |
185 apply (simp add: list_rel_empty) |
157 done |
186 apply (case_tac b) |
|
187 apply simp_all |
|
188 done |
158 |
189 |
159 (* induct_tac doesn't accept 'arbitrary', so we manually 'spec' *) |
190 (* induct_tac doesn't accept 'arbitrary', so we manually 'spec' *) |
160 lemma foldl_rsp[quot_respect]: |
191 lemma foldl_rsp[quot_respect]: |
161 assumes q1: "Quotient R1 Abs1 Rep1" |
192 assumes q1: "Quotient R1 Abs1 Rep1" |
162 and q2: "Quotient R2 Abs2 Rep2" |
193 and q2: "Quotient R2 Abs2 Rep2" |
163 shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl" |
194 shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl" |
164 apply(auto) |
195 apply(auto) |
165 apply (subgoal_tac "R1 xa ya \<longrightarrow> list_rel R2 xb yb \<longrightarrow> R1 (foldl x xa xb) (foldl y ya yb)") |
196 apply (subgoal_tac "R1 xa ya \<longrightarrow> list_rel R2 xb yb \<longrightarrow> R1 (foldl x xa xb) (foldl y ya yb)") |
166 apply simp |
197 apply simp |
167 apply (rule_tac x="xa" in spec) |
198 apply (rule_tac x="xa" in spec) |
168 apply (rule_tac x="ya" in spec) |
199 apply (rule_tac x="ya" in spec) |
169 apply (rule_tac xs="xb" and ys="yb" in list_induct2) |
200 apply (rule_tac xs="xb" and ys="yb" in list_induct2) |
170 apply (rule list_rel_len) |
201 apply (rule list_rel_len) |
171 apply (simp_all) |
202 apply (simp_all) |
172 done |
203 done |
173 |
204 |
174 lemma foldr_rsp[quot_respect]: |
205 lemma foldr_rsp[quot_respect]: |
175 assumes q1: "Quotient R1 Abs1 Rep1" |
206 assumes q1: "Quotient R1 Abs1 Rep1" |
176 and q2: "Quotient R2 Abs2 Rep2" |
207 and q2: "Quotient R2 Abs2 Rep2" |
177 shows "((R1 ===> R2 ===> R2) ===> list_rel R1 ===> R2 ===> R2) foldr foldr" |
208 shows "((R1 ===> R2 ===> R2) ===> list_rel R1 ===> R2 ===> R2) foldr foldr" |
178 apply auto |
209 apply auto |
179 apply(subgoal_tac "R2 xb yb \<longrightarrow> list_rel R1 xa ya \<longrightarrow> R2 (foldr x xa xb) (foldr y ya yb)") |
210 apply(subgoal_tac "R2 xb yb \<longrightarrow> list_rel R1 xa ya \<longrightarrow> R2 (foldr x xa xb) (foldr y ya yb)") |
180 apply simp |
211 apply simp |
181 apply (rule_tac xs="xa" and ys="ya" in list_induct2) |
212 apply (rule_tac xs="xa" and ys="ya" in list_induct2) |
182 apply (rule list_rel_len) |
213 apply (rule list_rel_len) |
183 apply (simp_all) |
214 apply (simp_all) |
184 done |
215 done |
185 |
216 |
186 lemma list_rel_eq[id_simps]: |
217 lemma list_rel_eq[id_simps]: |
187 shows "list_rel (op =) \<equiv> (op =)" |
218 shows "list_rel (op =) \<equiv> (op =)" |
188 apply(rule eq_reflection) |
219 apply(rule eq_reflection) |
189 unfolding expand_fun_eq |
220 unfolding expand_fun_eq |
190 apply(rule allI)+ |
221 apply(rule allI)+ |
191 apply(induct_tac x xa rule: list_induct2') |
222 apply(induct_tac x xa rule: list_induct2') |
192 apply(simp_all) |
223 apply(simp_all) |
193 done |
224 done |
194 |
225 |
195 lemma list_rel_refl: |
226 lemma list_rel_refl: |
196 assumes a: "\<And>x y. R x y = (R x = R y)" |
227 assumes a: "\<And>x y. R x y = (R x = R y)" |
197 shows "list_rel R x x" |
228 shows "list_rel R x x" |
198 by (induct x) (auto simp add: a) |
229 by (induct x) (auto simp add: a) |
199 |
230 |
200 end |
231 end |