equal
deleted
inserted
replaced
1 theory QuotList |
1 theory QuotList |
2 imports QuotMain List |
2 imports QuotMain List |
3 begin |
3 begin |
4 |
4 |
5 fun |
5 fun |
6 list_rel |
6 list_rel |
15 |
15 |
16 |
16 |
17 text {* should probably be in Sum_Type.thy *} |
17 text {* should probably be in Sum_Type.thy *} |
18 lemma split_list_all: |
18 lemma split_list_all: |
19 shows "(\<forall>x. P x) \<longleftrightarrow> P [] \<and> (\<forall>x xs. P (x#xs))" |
19 shows "(\<forall>x. P x) \<longleftrightarrow> P [] \<and> (\<forall>x xs. P (x#xs))" |
20 apply(auto) |
20 apply(auto) |
21 apply(case_tac x) |
21 apply(case_tac x) |
22 apply(simp_all) |
22 apply(simp_all) |
23 done |
23 done |
24 |
24 |
25 lemma map_id[id_simps]: "map id \<equiv> id" |
25 lemma map_id[id_simps]: |
26 apply(rule eq_reflection) |
26 shows "map id = id" |
27 apply(simp add: expand_fun_eq) |
27 apply(simp add: expand_fun_eq) |
28 apply(rule allI) |
28 apply(rule allI) |
29 apply(induct_tac x) |
29 apply(induct_tac x) |
30 apply(simp_all) |
30 apply(simp_all) |
31 done |
31 done |
110 shows "(R ===> list_rel R ===> list_rel R) (op #) (op #)" |
110 shows "(R ===> list_rel R ===> list_rel R) (op #) (op #)" |
111 by (auto) |
111 by (auto) |
112 |
112 |
113 lemma nil_prs[quot_preserve]: |
113 lemma nil_prs[quot_preserve]: |
114 assumes q: "Quotient R Abs Rep" |
114 assumes q: "Quotient R Abs Rep" |
115 shows "map Abs [] \<equiv> []" |
115 shows "map Abs [] = []" |
116 by (simp) |
116 by simp |
117 |
117 |
118 lemma nil_rsp[quot_respect]: |
118 lemma nil_rsp[quot_respect]: |
119 assumes q: "Quotient R Abs Rep" |
119 assumes q: "Quotient R Abs Rep" |
120 shows "list_rel R [] []" |
120 shows "list_rel R [] []" |
121 by simp |
121 by simp |
213 apply (rule list_rel_len) |
213 apply (rule list_rel_len) |
214 apply (simp_all) |
214 apply (simp_all) |
215 done |
215 done |
216 |
216 |
217 lemma list_rel_eq[id_simps]: |
217 lemma list_rel_eq[id_simps]: |
218 shows "list_rel (op =) \<equiv> (op =)" |
218 shows "(list_rel (op =)) = (op =)" |
219 apply(rule eq_reflection) |
|
220 unfolding expand_fun_eq |
219 unfolding expand_fun_eq |
221 apply(rule allI)+ |
220 apply(rule allI)+ |
222 apply(induct_tac x xa rule: list_induct2') |
221 apply(induct_tac x xa rule: list_induct2') |
223 apply(simp_all) |
222 apply(simp_all) |
224 done |
223 done |