equal
deleted
inserted
replaced
5 header {* Quotient infrastructure for the list type *} |
5 header {* Quotient infrastructure for the list type *} |
6 |
6 |
7 theory Quotient_List |
7 theory Quotient_List |
8 imports Main Quotient_Syntax |
8 imports Main Quotient_Syntax |
9 begin |
9 begin |
10 |
|
11 declare [[map list = list_all2]] |
|
12 |
10 |
13 lemma map_id [id_simps]: |
11 lemma map_id [id_simps]: |
14 "map id = id" |
12 "map id = id" |
15 by (fact List.map.id) |
13 by (fact List.map.id) |
16 |
14 |
73 from assms have "\<And>x y. R x x \<and> R y y \<and> Abs x = Abs y \<longleftrightarrow> R x y" by (rule Quotient_rel) |
71 from assms have "\<And>x y. R x x \<and> R y y \<and> Abs x = Abs y \<longleftrightarrow> R x y" by (rule Quotient_rel) |
74 then show "list_all2 R xs ys \<longleftrightarrow> list_all2 R xs xs \<and> list_all2 R ys ys \<and> map Abs xs = map Abs ys" |
72 then show "list_all2 R xs ys \<longleftrightarrow> list_all2 R xs xs \<and> list_all2 R ys ys \<and> map Abs xs = map Abs ys" |
75 by (induct xs ys rule: list_induct2') auto |
73 by (induct xs ys rule: list_induct2') auto |
76 qed |
74 qed |
77 |
75 |
|
76 declare [[map list = (list_all2, list_quotient)]] |
|
77 |
78 lemma cons_prs [quot_preserve]: |
78 lemma cons_prs [quot_preserve]: |
79 assumes q: "Quotient R Abs Rep" |
79 assumes q: "Quotient R Abs Rep" |
80 shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)" |
80 shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)" |
81 by (auto simp add: fun_eq_iff comp_def Quotient_abs_rep [OF q]) |
81 by (auto simp add: fun_eq_iff comp_def Quotient_abs_rep [OF q]) |
82 |
82 |