equal
deleted
inserted
replaced
1 theory QuotList |
1 (* Title: QuotList.thy |
|
2 Author: Cezary Kaliszyk and Christian Urban |
|
3 *) |
|
4 theory QuotList |
2 imports QuotMain List |
5 imports QuotMain List |
3 begin |
6 begin |
|
7 |
|
8 section {* Quotient infrastructure for the list type. *} |
4 |
9 |
5 fun |
10 fun |
6 list_rel |
11 list_rel |
7 where |
12 where |
8 "list_rel R [] [] = True" |
13 "list_rel R [] [] = True" |
10 | "list_rel R [] (x#xs) = False" |
15 | "list_rel R [] (x#xs) = False" |
11 | "list_rel R (x#xs) (y#ys) = (R x y \<and> list_rel R xs ys)" |
16 | "list_rel R (x#xs) (y#ys) = (R x y \<and> list_rel R xs ys)" |
12 |
17 |
13 declare [[map list = (map, list_rel)]] |
18 declare [[map list = (map, list_rel)]] |
14 |
19 |
15 |
|
16 |
|
17 text {* should probably be in Sum_Type.thy *} |
|
18 lemma split_list_all: |
20 lemma split_list_all: |
19 shows "(\<forall>x. P x) \<longleftrightarrow> P [] \<and> (\<forall>x xs. P (x#xs))" |
21 shows "(\<forall>x. P x) \<longleftrightarrow> P [] \<and> (\<forall>x xs. P (x#xs))" |
20 apply(auto) |
22 apply(auto) |
21 apply(case_tac x) |
23 apply(case_tac x) |
22 apply(simp_all) |
24 apply(simp_all) |