equal
deleted
inserted
replaced
12 | "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys" |
12 | "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys" |
13 | "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3" |
13 | "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3" |
14 |
14 |
15 lemma list_eq_refl: |
15 lemma list_eq_refl: |
16 shows "xs \<approx> xs" |
16 shows "xs \<approx> xs" |
17 apply (induct xs) |
17 by (induct xs) (auto intro: list_eq.intros) |
18 apply (auto intro: list_eq.intros) |
|
19 done |
|
20 |
18 |
21 lemma equiv_list_eq: |
19 lemma equiv_list_eq: |
22 shows "EQUIV list_eq" |
20 shows "EQUIV list_eq" |
23 unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def |
21 unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def |
24 apply(auto intro: list_eq.intros list_eq_refl) |
22 apply(auto intro: list_eq.intros list_eq_refl) |
176 term fmap |
174 term fmap |
177 thm fmap_def |
175 thm fmap_def |
178 |
176 |
179 ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def FOLD_def} *} |
177 ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def FOLD_def} *} |
180 |
178 |
181 lemma memb_rsp[quot_rsp]: |
179 lemma memb_rsp: |
182 fixes z |
180 fixes z |
183 assumes a: "x \<approx> y" |
181 assumes a: "x \<approx> y" |
184 shows "(z memb x) = (z memb y)" |
182 shows "(z memb x) = (z memb y)" |
185 using a by induct auto |
183 using a by induct auto |
186 |
184 |
187 lemma ho_memb_rsp[quot_rsp]: |
185 lemma ho_memb_rsp[quot_rsp]: |
188 "(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)" |
186 "(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)" |
189 by (simp add: memb_rsp) |
187 by (simp add: memb_rsp) |
190 |
188 |
191 lemma card1_rsp[quot_rsp]: |
189 lemma card1_rsp: |
192 fixes a b :: "'a list" |
190 fixes a b :: "'a list" |
193 assumes e: "a \<approx> b" |
191 assumes e: "a \<approx> b" |
194 shows "card1 a = card1 b" |
192 shows "card1 a = card1 b" |
195 using e by induct (simp_all add:memb_rsp) |
193 using e by induct (simp_all add:memb_rsp) |
196 |
194 |
244 apply (rule append_rsp_fst) |
242 apply (rule append_rsp_fst) |
245 apply (rule list_eq.intros(3)) |
243 apply (rule list_eq.intros(3)) |
246 apply (rule rev_rsp) |
244 apply (rule rev_rsp) |
247 done |
245 done |
248 |
246 |
249 lemma append_rsp[quot_rsp]: |
247 lemma append_rsp: |
250 assumes a : "l1 \<approx> r1" |
248 assumes a : "l1 \<approx> r1" |
251 assumes b : "l2 \<approx> r2 " |
249 assumes b : "l2 \<approx> r2 " |
252 shows "(l1 @ l2) \<approx> (r1 @ r2)" |
250 shows "(l1 @ l2) \<approx> (r1 @ r2)" |
253 apply (rule list_eq.intros(6)) |
251 apply (rule list_eq.intros(6)) |
254 apply (rule append_rsp_fst) |
252 apply (rule append_rsp_fst) |
263 |
261 |
264 lemma ho_append_rsp[quot_rsp]: |
262 lemma ho_append_rsp[quot_rsp]: |
265 "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @" |
263 "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @" |
266 by (simp add: append_rsp) |
264 by (simp add: append_rsp) |
267 |
265 |
268 lemma map_rsp[quot_rsp]: |
266 lemma map_rsp: |
269 assumes a: "a \<approx> b" |
267 assumes a: "a \<approx> b" |
270 shows "map f a \<approx> map f b" |
268 shows "map f a \<approx> map f b" |
271 using a |
269 using a |
272 apply (induct) |
270 apply (induct) |
273 apply(auto intro: list_eq.intros) |
271 apply(auto intro: list_eq.intros) |