57 apply(simp add: Quotient_rep_reflp[OF q]) |
57 apply(simp add: Quotient_rep_reflp[OF q]) |
58 apply(rule allI)+ |
58 apply(rule allI)+ |
59 apply(rule list_rel_rel[OF q]) |
59 apply(rule list_rel_rel[OF q]) |
60 done |
60 done |
61 |
61 |
62 lemma map_id[id_simps]: "map id \<equiv> id" |
62 lemma map_id[id_simps]: "map id = id" |
63 apply (rule eq_reflection) |
|
64 apply (rule ext) |
63 apply (rule ext) |
65 apply (rule_tac list="x" in list.induct) |
64 apply (rule_tac list="x" in list.induct) |
66 apply (simp_all) |
65 apply (simp_all) |
67 done |
66 done |
68 |
67 |
69 lemma cons_prs_aux: |
68 lemma cons_prs_aux: |
70 assumes q: "Quotient R Abs Rep" |
69 assumes q: "Quotient R Abs Rep" |
71 shows "(map Abs) ((Rep h) # (map Rep t)) = h # t" |
70 shows "(map Abs) ((Rep h) # (map Rep t)) = h # t" |
72 by (induct t) (simp_all add: Quotient_abs_rep[OF q]) |
71 by (induct t) (simp_all add: Quotient_abs_rep[OF q]) |
73 |
72 |
74 lemma cons_prs[quot_preserve]: |
73 lemma cons_prs[quot_preserve]: |
75 assumes q: "Quotient R Abs Rep" |
74 assumes q: "Quotient R Abs Rep" |
76 shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)" |
75 shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)" |
77 by (simp only: expand_fun_eq fun_map_def cons_prs_aux[OF q]) |
76 by (simp only: expand_fun_eq fun_map_def cons_prs_aux[OF q]) (simp) |
78 (simp) |
|
79 |
77 |
80 lemma cons_rsp[quot_respect]: |
78 lemma cons_rsp[quot_respect]: |
81 assumes q: "Quotient R Abs Rep" |
79 assumes q: "Quotient R Abs Rep" |
82 shows "(R ===> list_rel R ===> list_rel R) op # op #" |
80 shows "(R ===> list_rel R ===> list_rel R) op # op #" |
83 by (auto) |
81 by auto |
84 |
82 |
85 lemma nil_prs[quot_preserve]: |
83 lemma nil_prs[quot_preserve]: |
86 assumes q: "Quotient R Abs Rep" |
84 assumes q: "Quotient R Abs Rep" |
87 shows "map Abs [] \<equiv> []" |
85 shows "map Abs [] = []" |
88 by (simp) |
86 by simp |
89 |
87 |
90 lemma nil_rsp[quot_respect]: |
88 lemma nil_rsp[quot_respect]: |
91 assumes q: "Quotient R Abs Rep" |
89 assumes q: "Quotient R Abs Rep" |
92 shows "list_rel R [] []" |
90 shows "list_rel R [] []" |
93 by simp |
91 by simp |
94 |
92 |
95 lemma map_prs_aux: |
93 lemma map_prs_aux: |
96 assumes a: "Quotient R1 abs1 rep1" |
94 assumes a: "Quotient R1 abs1 rep1" |
97 and b: "Quotient R2 abs2 rep2" |
95 and b: "Quotient R2 abs2 rep2" |
98 shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l" |
96 shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l" |
99 by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
97 by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
100 |
98 |
101 |
99 |
102 lemma map_prs[quot_preserve]: |
100 lemma map_prs[quot_preserve]: |
103 assumes a: "Quotient R1 abs1 rep1" |
101 assumes a: "Quotient R1 abs1 rep1" |
104 and b: "Quotient R2 abs2 rep2" |
102 and b: "Quotient R2 abs2 rep2" |
105 shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map" |
103 shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map" |
106 by (simp only: expand_fun_eq fun_map_def map_prs_aux[OF a b]) |
104 by (simp only: expand_fun_eq fun_map_def map_prs_aux[OF a b]) (simp) |
107 (simp) |
|
108 |
105 |
109 |
106 |
110 lemma map_rsp[quot_respect]: |
107 lemma map_rsp[quot_respect]: |
111 assumes q1: "Quotient R1 Abs1 Rep1" |
108 assumes q1: "Quotient R1 Abs1 Rep1" |
112 and q2: "Quotient R2 Abs2 Rep2" |
109 and q2: "Quotient R2 Abs2 Rep2" |
113 shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map" |
110 shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map" |
114 apply(simp) |
111 apply(simp) |
115 apply(rule allI)+ |
112 apply(rule allI)+ |
116 apply(rule impI) |
113 apply(rule impI) |
117 apply(rule allI)+ |
114 apply(rule allI)+ |
118 apply (induct_tac xa ya rule: list_induct2') |
115 apply (induct_tac xa ya rule: list_induct2') |
119 apply simp_all |
116 apply simp_all |
120 done |
117 done |
121 |
118 |
122 lemma foldr_prs_aux: |
119 lemma foldr_prs_aux: |
123 assumes a: "Quotient R1 abs1 rep1" |
120 assumes a: "Quotient R1 abs1 rep1" |
124 and b: "Quotient R2 abs2 rep2" |
121 and b: "Quotient R2 abs2 rep2" |
125 shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e" |
122 shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e" |
126 by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
123 by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
127 |
124 |
128 lemma foldr_prs[quot_preserve]: |
125 lemma foldr_prs[quot_preserve]: |
129 assumes a: "Quotient R1 abs1 rep1" |
126 assumes a: "Quotient R1 abs1 rep1" |
130 and b: "Quotient R2 abs2 rep2" |
127 and b: "Quotient R2 abs2 rep2" |
131 shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr" |
128 shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr" |
132 by (simp only: expand_fun_eq fun_map_def foldr_prs_aux[OF a b]) |
129 by (simp only: expand_fun_eq fun_map_def foldr_prs_aux[OF a b]) (simp) |
133 (simp) |
|
134 |
130 |
135 lemma foldl_prs_aux: |
131 lemma foldl_prs_aux: |
136 assumes a: "Quotient R1 abs1 rep1" |
132 assumes a: "Quotient R1 abs1 rep1" |
137 and b: "Quotient R2 abs2 rep2" |
133 and b: "Quotient R2 abs2 rep2" |
138 shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l" |
134 shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l" |
139 by (induct l arbitrary:e) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
135 by (induct l arbitrary:e) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
140 |
|
141 |
136 |
142 lemma foldl_prs[quot_preserve]: |
137 lemma foldl_prs[quot_preserve]: |
143 assumes a: "Quotient R1 abs1 rep1" |
138 assumes a: "Quotient R1 abs1 rep1" |
144 and b: "Quotient R2 abs2 rep2" |
139 and b: "Quotient R2 abs2 rep2" |
145 shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl" |
140 shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl" |
146 by (simp only: expand_fun_eq fun_map_def foldl_prs_aux[OF a b]) |
141 by (simp only: expand_fun_eq fun_map_def foldl_prs_aux[OF a b]) (simp) |
147 (simp) |
|
148 |
142 |
149 lemma list_rel_empty: "list_rel R [] b \<Longrightarrow> length b = 0" |
143 lemma list_rel_empty: |
150 by (induct b) (simp_all) |
144 "list_rel R [] b \<Longrightarrow> length b = 0" |
|
145 by (induct b) (simp_all) |
151 |
146 |
152 lemma list_rel_len: "list_rel R a b \<Longrightarrow> length a = length b" |
147 lemma list_rel_len: |
153 apply (induct a arbitrary: b) |
148 "list_rel R a b \<Longrightarrow> length a = length b" |
154 apply (simp add: list_rel_empty) |
149 apply (induct a arbitrary: b) |
155 apply (case_tac b) |
150 apply (simp add: list_rel_empty) |
156 apply simp_all |
151 apply (case_tac b) |
157 done |
152 apply simp_all |
|
153 done |
158 |
154 |
159 (* induct_tac doesn't accept 'arbitrary', so we manually 'spec' *) |
155 (* induct_tac doesn't accept 'arbitrary', so we manually 'spec' *) |
160 lemma foldl_rsp[quot_respect]: |
156 lemma foldl_rsp[quot_respect]: |
161 assumes q1: "Quotient R1 Abs1 Rep1" |
157 assumes q1: "Quotient R1 Abs1 Rep1" |
162 and q2: "Quotient R2 Abs2 Rep2" |
158 and q2: "Quotient R2 Abs2 Rep2" |
163 shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl" |
159 shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl" |
164 apply(auto) |
160 apply(auto) |
165 apply (subgoal_tac "R1 xa ya \<longrightarrow> list_rel R2 xb yb \<longrightarrow> R1 (foldl x xa xb) (foldl y ya yb)") |
161 apply (subgoal_tac "R1 xa ya \<longrightarrow> list_rel R2 xb yb \<longrightarrow> R1 (foldl x xa xb) (foldl y ya yb)") |
166 apply simp |
162 apply simp |
167 apply (rule_tac x="xa" in spec) |
163 apply (rule_tac x="xa" in spec) |
168 apply (rule_tac x="ya" in spec) |
164 apply (rule_tac x="ya" in spec) |
169 apply (rule_tac xs="xb" and ys="yb" in list_induct2) |
165 apply (rule_tac xs="xb" and ys="yb" in list_induct2) |
170 apply (rule list_rel_len) |
166 apply (rule list_rel_len) |
171 apply (simp_all) |
167 apply (simp_all) |
172 done |
168 done |
173 |
169 |
174 lemma foldr_rsp[quot_respect]: |
170 lemma foldr_rsp[quot_respect]: |
175 assumes q1: "Quotient R1 Abs1 Rep1" |
171 assumes q1: "Quotient R1 Abs1 Rep1" |
176 and q2: "Quotient R2 Abs2 Rep2" |
172 and q2: "Quotient R2 Abs2 Rep2" |
177 shows "((R1 ===> R2 ===> R2) ===> list_rel R1 ===> R2 ===> R2) foldr foldr" |
173 shows "((R1 ===> R2 ===> R2) ===> list_rel R1 ===> R2 ===> R2) foldr foldr" |
178 apply auto |
174 apply auto |
179 apply(subgoal_tac "R2 xb yb \<longrightarrow> list_rel R1 xa ya \<longrightarrow> R2 (foldr x xa xb) (foldr y ya yb)") |
175 apply(subgoal_tac "R2 xb yb \<longrightarrow> list_rel R1 xa ya \<longrightarrow> R2 (foldr x xa xb) (foldr y ya yb)") |
180 apply simp |
176 apply simp |
181 apply (rule_tac xs="xa" and ys="ya" in list_induct2) |
177 apply (rule_tac xs="xa" and ys="ya" in list_induct2) |
182 apply (rule list_rel_len) |
178 apply (rule list_rel_len) |
183 apply (simp_all) |
179 apply (simp_all) |
184 done |
180 done |
185 |
181 |
186 lemma list_rel_eq[id_simps]: |
182 lemma list_rel_eq[id_simps]: |
187 shows "list_rel (op =) \<equiv> (op =)" |
183 shows "(list_rel (op =)) = (op =)" |
188 apply(rule eq_reflection) |
184 unfolding expand_fun_eq |
189 unfolding expand_fun_eq |
185 apply(rule allI)+ |
190 apply(rule allI)+ |
186 apply(induct_tac x xa rule: list_induct2') |
191 apply(induct_tac x xa rule: list_induct2') |
187 apply(simp_all) |
192 apply(simp_all) |
188 done |
193 done |
|
194 |
189 |
195 lemma list_rel_refl: |
190 lemma list_rel_refl: |
196 assumes a: "\<And>x y. R x y = (R x = R y)" |
191 assumes a: "\<And>x y. R x y = (R x = R y)" |
197 shows "list_rel R x x" |
192 shows "list_rel R x x" |
198 by (induct x) (auto simp add: a) |
193 by (induct x) (auto simp add: a) |
199 |
194 |
200 end |
195 end |