equal
deleted
inserted
replaced
1 theory QuotList |
1 theory QuotList |
2 imports QuotScript List |
2 imports QuotMain List |
3 begin |
3 begin |
4 |
4 |
5 fun |
5 fun |
6 list_rel |
6 list_rel |
7 where |
7 where |
8 "list_rel R [] [] = True" |
8 "list_rel R [] [] = True" |
9 | "list_rel R (x#xs) [] = False" |
9 | "list_rel R (x#xs) [] = False" |
10 | "list_rel R [] (x#xs) = False" |
10 | "list_rel R [] (x#xs) = False" |
11 | "list_rel R (x#xs) (y#ys) = (R x y \<and> list_rel R xs ys)" |
11 | "list_rel R (x#xs) (y#ys) = (R x y \<and> list_rel R xs ys)" |
12 |
12 |
13 lemma list_equivp: |
13 declare [[map list = (map, list_rel)]] |
|
14 |
|
15 lemma list_equivp[quotient_equiv]: |
14 assumes a: "equivp R" |
16 assumes a: "equivp R" |
15 shows "equivp (list_rel R)" |
17 shows "equivp (list_rel R)" |
16 unfolding equivp_def |
18 unfolding equivp_def |
17 apply(rule allI)+ |
19 apply(rule allI)+ |
18 apply(induct_tac x y rule: list_induct2') |
20 apply(induct_tac x y rule: list_induct2') |
36 apply(simp_all) |
38 apply(simp_all) |
37 using Quotient_rel[OF q] |
39 using Quotient_rel[OF q] |
38 apply(metis) |
40 apply(metis) |
39 done |
41 done |
40 |
42 |
41 lemma list_quotient: |
43 lemma list_quotient[quotient_thm]: |
42 assumes q: "Quotient R Abs Rep" |
44 assumes q: "Quotient R Abs Rep" |
43 shows "Quotient (list_rel R) (map Abs) (map Rep)" |
45 shows "Quotient (list_rel R) (map Abs) (map Rep)" |
44 unfolding Quotient_def |
46 unfolding Quotient_def |
45 apply(rule conjI) |
47 apply(rule conjI) |
46 apply(rule allI) |
48 apply(rule allI) |
55 apply(simp add: Quotient_rep_reflp[OF q]) |
57 apply(simp add: Quotient_rep_reflp[OF q]) |
56 apply(rule allI)+ |
58 apply(rule allI)+ |
57 apply(rule list_rel_rel[OF q]) |
59 apply(rule list_rel_rel[OF q]) |
58 done |
60 done |
59 |
61 |
|
62 lemma map_id: "map id \<equiv> id" |
|
63 apply (rule eq_reflection) |
|
64 apply (rule ext) |
|
65 apply (rule_tac list="x" in list.induct) |
|
66 apply (simp_all) |
|
67 done |
|
68 |
60 |
69 |
61 lemma cons_prs: |
70 lemma cons_prs: |
62 assumes q: "Quotient R Abs Rep" |
71 assumes q: "Quotient R Abs Rep" |
63 shows "(map Abs) ((Rep h) # (map Rep t)) = h # t" |
72 shows "(map Abs) ((Rep h) # (map Rep t)) = h # t" |
64 by (induct t) (simp_all add: Quotient_abs_rep[OF q]) |
73 by (induct t) (simp_all add: Quotient_abs_rep[OF q]) |
65 |
74 |
66 lemma cons_rsp: |
75 lemma cons_rsp[quotient_rsp]: |
67 assumes q: "Quotient R Abs Rep" |
76 assumes q: "Quotient R Abs Rep" |
68 shows "(R ===> list_rel R ===> list_rel R) op # op #" |
77 shows "(R ===> list_rel R ===> list_rel R) op # op #" |
69 by (auto) |
78 by (auto) |
70 |
79 |
71 lemma nil_prs: |
80 lemma nil_prs: |
72 assumes q: "Quotient R Abs Rep" |
81 assumes q: "Quotient R Abs Rep" |
73 shows "map Abs [] \<equiv> []" |
82 shows "map Abs [] \<equiv> []" |
74 by (simp) |
83 by (simp) |
75 |
84 |
76 lemma nil_rsp: |
85 lemma nil_rsp[quotient_rsp]: |
77 assumes q: "Quotient R Abs Rep" |
86 assumes q: "Quotient R Abs Rep" |
78 shows "list_rel R [] []" |
87 shows "list_rel R [] []" |
79 by simp |
88 by simp |
80 |
89 |
81 lemma map_prs: |
90 lemma map_prs: |
130 |
139 |
131 (* TODO: induct_tac doesn't accept 'arbitrary'. |
140 (* TODO: induct_tac doesn't accept 'arbitrary'. |
132 induct doesn't accept 'rule'. |
141 induct doesn't accept 'rule'. |
133 that's why the proof uses manual generalisation and needs assumptions |
142 that's why the proof uses manual generalisation and needs assumptions |
134 both in conclusion for induction and in assumptions. *) |
143 both in conclusion for induction and in assumptions. *) |
135 lemma foldl_rsp: |
144 lemma foldl_rsp[quotient_rsp]: |
136 assumes q1: "Quotient R1 Abs1 Rep1" |
145 assumes q1: "Quotient R1 Abs1 Rep1" |
137 and q2: "Quotient R2 Abs2 Rep2" |
146 and q2: "Quotient R2 Abs2 Rep2" |
138 shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl" |
147 shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl" |
139 apply auto |
148 apply auto |
140 apply (subgoal_tac "R1 xa ya \<longrightarrow> list_rel R2 xb yb \<longrightarrow> R1 (foldl x xa xb) (foldl y ya yb)") |
149 apply (subgoal_tac "R1 xa ya \<longrightarrow> list_rel R2 xb yb \<longrightarrow> R1 (foldl x xa xb) (foldl y ya yb)") |
151 |
160 |
152 |
161 |
153 |
162 |
154 (* TODO: Rest are unused *) |
163 (* TODO: Rest are unused *) |
155 |
164 |
156 lemma list_map_id: |
|
157 shows "map (\<lambda>x. x) = (\<lambda>x. x)" |
|
158 by simp |
|
159 |
|
160 lemma list_rel_eq: |
165 lemma list_rel_eq: |
161 shows "list_rel (op =) \<equiv> (op =)" |
166 shows "list_rel (op =) \<equiv> (op =)" |
162 apply(rule eq_reflection) |
167 apply(rule eq_reflection) |
163 unfolding expand_fun_eq |
168 unfolding expand_fun_eq |
164 apply(rule allI)+ |
169 apply(rule allI)+ |