80 apply(induct_tac a) |
80 apply(induct_tac a) |
81 apply(simp_all add: Quotient_rep_reflp[OF q]) |
81 apply(simp_all add: Quotient_rep_reflp[OF q]) |
82 apply(rule list_all2_rel[OF q]) |
82 apply(rule list_all2_rel[OF q]) |
83 done |
83 done |
84 |
84 |
85 lemma cons_prs_aux: |
|
86 assumes q: "Quotient R Abs Rep" |
|
87 shows "(map Abs) ((Rep h) # (map Rep t)) = h # t" |
|
88 by (induct t) (simp_all add: Quotient_abs_rep[OF q]) |
|
89 |
|
90 lemma cons_prs[quot_preserve]: |
85 lemma cons_prs[quot_preserve]: |
91 assumes q: "Quotient R Abs Rep" |
86 assumes q: "Quotient R Abs Rep" |
92 shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)" |
87 shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)" |
93 by (simp only: fun_eq_iff fun_map_def cons_prs_aux[OF q]) |
88 by (auto simp add: fun_eq_iff comp_def Quotient_abs_rep [OF q]) |
94 (simp) |
|
95 |
89 |
96 lemma cons_rsp[quot_respect]: |
90 lemma cons_rsp[quot_respect]: |
97 assumes q: "Quotient R Abs Rep" |
91 assumes q: "Quotient R Abs Rep" |
98 shows "(R ===> list_all2 R ===> list_all2 R) (op #) (op #)" |
92 shows "(R ===> list_all2 R ===> list_all2 R) (op #) (op #)" |
99 by (auto) |
93 by auto |
100 |
94 |
101 lemma nil_prs[quot_preserve]: |
95 lemma nil_prs[quot_preserve]: |
102 assumes q: "Quotient R Abs Rep" |
96 assumes q: "Quotient R Abs Rep" |
103 shows "map Abs [] = []" |
97 shows "map Abs [] = []" |
104 by simp |
98 by simp |
118 lemma map_prs[quot_preserve]: |
112 lemma map_prs[quot_preserve]: |
119 assumes a: "Quotient R1 abs1 rep1" |
113 assumes a: "Quotient R1 abs1 rep1" |
120 and b: "Quotient R2 abs2 rep2" |
114 and b: "Quotient R2 abs2 rep2" |
121 shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map" |
115 shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map" |
122 and "((abs1 ---> id) ---> map rep1 ---> id) map = map" |
116 and "((abs1 ---> id) ---> map rep1 ---> id) map = map" |
123 by (simp_all only: fun_eq_iff fun_map_def map_prs_aux[OF a b]) |
117 by (simp_all only: fun_eq_iff map_prs_aux[OF a b] comp_def) |
124 (simp_all add: Quotient_abs_rep[OF a]) |
118 (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
|
119 |
125 |
120 |
126 lemma map_rsp[quot_respect]: |
121 lemma map_rsp[quot_respect]: |
127 assumes q1: "Quotient R1 Abs1 Rep1" |
122 assumes q1: "Quotient R1 Abs1 Rep1" |
128 and q2: "Quotient R2 Abs2 Rep2" |
123 and q2: "Quotient R2 Abs2 Rep2" |
129 shows "((R1 ===> R2) ===> (list_all2 R1) ===> list_all2 R2) map map" |
124 shows "((R1 ===> R2) ===> (list_all2 R1) ===> list_all2 R2) map map" |
130 and "((R1 ===> op =) ===> (list_all2 R1) ===> op =) map map" |
125 and "((R1 ===> op =) ===> (list_all2 R1) ===> op =) map map" |
131 apply simp_all |
126 apply (simp_all add: fun_rel_def) |
132 apply(rule_tac [!] allI)+ |
127 apply(rule_tac [!] allI)+ |
133 apply(rule_tac [!] impI) |
128 apply(rule_tac [!] impI) |
134 apply(rule_tac [!] allI)+ |
129 apply(rule_tac [!] allI)+ |
135 apply (induct_tac [!] xa ya rule: list_induct2') |
130 apply (induct_tac [!] xa ya rule: list_induct2') |
136 apply simp_all |
131 apply simp_all |
144 |
139 |
145 lemma foldr_prs[quot_preserve]: |
140 lemma foldr_prs[quot_preserve]: |
146 assumes a: "Quotient R1 abs1 rep1" |
141 assumes a: "Quotient R1 abs1 rep1" |
147 and b: "Quotient R2 abs2 rep2" |
142 and b: "Quotient R2 abs2 rep2" |
148 shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr" |
143 shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr" |
149 by (simp only: fun_eq_iff fun_map_def foldr_prs_aux[OF a b]) |
144 apply (simp add: fun_eq_iff) |
|
145 by (simp only: fun_eq_iff foldr_prs_aux[OF a b]) |
150 (simp) |
146 (simp) |
151 |
147 |
152 lemma foldl_prs_aux: |
148 lemma foldl_prs_aux: |
153 assumes a: "Quotient R1 abs1 rep1" |
149 assumes a: "Quotient R1 abs1 rep1" |
154 and b: "Quotient R2 abs2 rep2" |
150 and b: "Quotient R2 abs2 rep2" |
158 |
154 |
159 lemma foldl_prs[quot_preserve]: |
155 lemma foldl_prs[quot_preserve]: |
160 assumes a: "Quotient R1 abs1 rep1" |
156 assumes a: "Quotient R1 abs1 rep1" |
161 and b: "Quotient R2 abs2 rep2" |
157 and b: "Quotient R2 abs2 rep2" |
162 shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl" |
158 shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl" |
163 by (simp only: fun_eq_iff fun_map_def foldl_prs_aux[OF a b]) |
159 by (simp add: fun_eq_iff foldl_prs_aux [OF a b]) |
164 (simp) |
|
165 |
160 |
166 lemma list_all2_empty: |
161 lemma list_all2_empty: |
167 shows "list_all2 R [] b \<Longrightarrow> length b = 0" |
162 shows "list_all2 R [] b \<Longrightarrow> length b = 0" |
168 by (induct b) (simp_all) |
163 by (induct b) (simp_all) |
169 |
164 |
170 (* induct_tac doesn't accept 'arbitrary', so we manually 'spec' *) |
165 (* induct_tac doesn't accept 'arbitrary', so we manually 'spec' *) |
171 lemma foldl_rsp[quot_respect]: |
166 lemma foldl_rsp[quot_respect]: |
172 assumes q1: "Quotient R1 Abs1 Rep1" |
167 assumes q1: "Quotient R1 Abs1 Rep1" |
173 and q2: "Quotient R2 Abs2 Rep2" |
168 and q2: "Quotient R2 Abs2 Rep2" |
174 shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_all2 R2 ===> R1) foldl foldl" |
169 shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_all2 R2 ===> R1) foldl foldl" |
175 apply(auto) |
170 apply(auto simp add: fun_rel_def) |
176 apply (subgoal_tac "R1 xa ya \<longrightarrow> list_all2 R2 xb yb \<longrightarrow> R1 (foldl x xa xb) (foldl y ya yb)") |
171 apply (subgoal_tac "R1 xa ya \<longrightarrow> list_all2 R2 xb yb \<longrightarrow> R1 (foldl x xa xb) (foldl y ya yb)") |
177 apply simp |
172 apply simp |
178 apply (rule_tac x="xa" in spec) |
173 apply (rule_tac x="xa" in spec) |
179 apply (rule_tac x="ya" in spec) |
174 apply (rule_tac x="ya" in spec) |
180 apply (rule_tac xs="xb" and ys="yb" in list_induct2) |
175 apply (rule_tac xs="xb" and ys="yb" in list_induct2) |
184 |
179 |
185 lemma foldr_rsp[quot_respect]: |
180 lemma foldr_rsp[quot_respect]: |
186 assumes q1: "Quotient R1 Abs1 Rep1" |
181 assumes q1: "Quotient R1 Abs1 Rep1" |
187 and q2: "Quotient R2 Abs2 Rep2" |
182 and q2: "Quotient R2 Abs2 Rep2" |
188 shows "((R1 ===> R2 ===> R2) ===> list_all2 R1 ===> R2 ===> R2) foldr foldr" |
183 shows "((R1 ===> R2 ===> R2) ===> list_all2 R1 ===> R2 ===> R2) foldr foldr" |
189 apply auto |
184 apply (auto simp add: fun_rel_def) |
190 apply(subgoal_tac "R2 xb yb \<longrightarrow> list_all2 R1 xa ya \<longrightarrow> R2 (foldr x xa xb) (foldr y ya yb)") |
185 apply(subgoal_tac "R2 xb yb \<longrightarrow> list_all2 R1 xa ya \<longrightarrow> R2 (foldr x xa xb) (foldr y ya yb)") |
191 apply simp |
186 apply simp |
192 apply (rule_tac xs="xa" and ys="ya" in list_induct2) |
187 apply (rule_tac xs="xa" and ys="ya" in list_induct2) |
193 apply (rule list_all2_lengthD) |
188 apply (rule list_all2_lengthD) |
194 apply (simp_all) |
189 apply (simp_all) |
222 qed |
217 qed |
223 qed |
218 qed |
224 |
219 |
225 lemma[quot_respect]: |
220 lemma[quot_respect]: |
226 "((R ===> R ===> op =) ===> list_all2 R ===> list_all2 R ===> op =) list_all2 list_all2" |
221 "((R ===> R ===> op =) ===> list_all2 R ===> list_all2 R ===> op =) list_all2 list_all2" |
227 by (simp add: list_all2_rsp) |
222 by (simp add: list_all2_rsp fun_rel_def) |
228 |
223 |
229 lemma[quot_preserve]: |
224 lemma[quot_preserve]: |
230 assumes a: "Quotient R abs1 rep1" |
225 assumes a: "Quotient R abs1 rep1" |
231 shows "((abs1 ---> abs1 ---> id) ---> map rep1 ---> map rep1 ---> id) list_all2 = list_all2" |
226 shows "((abs1 ---> abs1 ---> id) ---> map rep1 ---> map rep1 ---> id) list_all2 = list_all2" |
232 apply (simp add: fun_eq_iff) |
227 apply (simp add: fun_eq_iff) |