1 theory AbsRepTest |
|
2 imports "../Quotient" "../Quotient_List" "../Quotient_Option" "../Quotient_Sum" "../Quotient_Product" List |
|
3 begin |
|
4 |
|
5 |
|
6 (* |
|
7 ML_command "ProofContext.debug := false" |
|
8 ML_command "ProofContext.verbose := false" |
|
9 *) |
|
10 |
|
11 ML {* open Quotient_Term *} |
|
12 |
|
13 ML {* |
|
14 fun test_funs flag ctxt (rty, qty) = |
|
15 (absrep_fun_chk flag ctxt (rty, qty) |
|
16 |> Syntax.string_of_term ctxt |
|
17 |> writeln; |
|
18 equiv_relation_chk ctxt (rty, qty) |
|
19 |> Syntax.string_of_term ctxt |
|
20 |> writeln) |
|
21 *} |
|
22 |
|
23 definition |
|
24 erel1 (infixl "\<approx>1" 50) |
|
25 where |
|
26 "erel1 \<equiv> \<lambda>xs ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" |
|
27 |
|
28 quotient_type |
|
29 'a fset = "'a list" / erel1 |
|
30 apply(rule equivpI) |
|
31 unfolding erel1_def reflp_def symp_def transp_def |
|
32 by auto |
|
33 |
|
34 definition |
|
35 erel2 (infixl "\<approx>2" 50) |
|
36 where |
|
37 "erel2 \<equiv> \<lambda>(xs::('a * 'a) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" |
|
38 |
|
39 quotient_type |
|
40 'a foo = "('a * 'a) list" / erel2 |
|
41 apply(rule equivpI) |
|
42 unfolding erel2_def reflp_def symp_def transp_def |
|
43 by auto |
|
44 |
|
45 definition |
|
46 erel3 (infixl "\<approx>3" 50) |
|
47 where |
|
48 "erel3 \<equiv> \<lambda>(xs::('a * int) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" |
|
49 |
|
50 quotient_type |
|
51 'a bar = "('a * int) list" / "erel3" |
|
52 apply(rule equivpI) |
|
53 unfolding erel3_def reflp_def symp_def transp_def |
|
54 by auto |
|
55 |
|
56 fun |
|
57 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infixl "\<approx>4" 50) |
|
58 where |
|
59 "intrel (x, y) (u, v) = (x + v = u + y)" |
|
60 |
|
61 quotient_type myint = "nat \<times> nat" / intrel |
|
62 by (auto simp add: equivp_def expand_fun_eq) |
|
63 |
|
64 ML {* |
|
65 test_funs AbsF @{context} |
|
66 (@{typ "nat \<times> nat"}, |
|
67 @{typ "myint"}) |
|
68 *} |
|
69 |
|
70 ML {* |
|
71 test_funs AbsF @{context} |
|
72 (@{typ "('a * 'a) list"}, |
|
73 @{typ "'a foo"}) |
|
74 *} |
|
75 |
|
76 ML {* |
|
77 test_funs RepF @{context} |
|
78 (@{typ "(('a * 'a) list * 'b)"}, |
|
79 @{typ "('a foo * 'b)"}) |
|
80 *} |
|
81 |
|
82 ML {* |
|
83 test_funs AbsF @{context} |
|
84 (@{typ "(('a list) * int) list"}, |
|
85 @{typ "('a fset) bar"}) |
|
86 *} |
|
87 |
|
88 ML {* |
|
89 test_funs AbsF @{context} |
|
90 (@{typ "('a list)"}, |
|
91 @{typ "('a fset)"}) |
|
92 *} |
|
93 |
|
94 ML {* |
|
95 test_funs AbsF @{context} |
|
96 (@{typ "('a list) list"}, |
|
97 @{typ "('a fset) fset"}) |
|
98 *} |
|
99 |
|
100 |
|
101 ML {* |
|
102 test_funs AbsF @{context} |
|
103 (@{typ "((nat * nat) list) list"}, |
|
104 @{typ "((myint) fset) fset"}) |
|
105 *} |
|
106 |
|
107 ML {* |
|
108 test_funs AbsF @{context} |
|
109 (@{typ "(('a * 'a) list) list"}, |
|
110 @{typ "(('a * 'a) fset) fset"}) |
|
111 *} |
|
112 |
|
113 ML {* |
|
114 test_funs AbsF @{context} |
|
115 (@{typ "(nat * nat) list"}, |
|
116 @{typ "myint fset"}) |
|
117 *} |
|
118 |
|
119 ML {* |
|
120 test_funs AbsF @{context} |
|
121 (@{typ "('a list) list \<Rightarrow> 'a list"}, |
|
122 @{typ "('a fset) fset \<Rightarrow> 'a fset"}) |
|
123 *} |
|
124 |
|
125 lemma OO_sym_inv: |
|
126 assumes sr: "symp r" |
|
127 and ss: "symp s" |
|
128 shows "(r OO s) x y = (s OO r) y x" |
|
129 using sr ss |
|
130 unfolding symp_def |
|
131 apply (metis pred_comp.intros pred_compE ss symp_def) |
|
132 done |
|
133 |
|
134 lemma abs_o_rep: |
|
135 assumes a: "Quotient r absf repf" |
|
136 shows "absf o repf = id" |
|
137 apply(rule ext) |
|
138 apply(simp add: Quotient_abs_rep[OF a]) |
|
139 done |
|
140 |
|
141 lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B" |
|
142 apply (rule eq_reflection) |
|
143 apply auto |
|
144 done |
|
145 |
|
146 lemma map_rel_cong: "b \<approx>1 ba \<Longrightarrow> map f b \<approx>1 map f ba" |
|
147 unfolding erel1_def |
|
148 apply(simp only: set_map set_in_eq) |
|
149 done |
|
150 |
|
151 lemma quotient_compose_list_gen_pre: |
|
152 assumes a: "equivp r2" |
|
153 and b: "Quotient r2 abs2 rep2" |
|
154 shows "(list_rel r2 OOO op \<approx>1) r s = |
|
155 ((list_rel r2 OOO op \<approx>1) r r \<and> (list_rel r2 OOO op \<approx>1) s s \<and> |
|
156 abs_fset (map abs2 r) = abs_fset (map abs2 s))" |
|
157 apply rule |
|
158 apply rule |
|
159 apply rule |
|
160 apply (rule list_rel_refl) |
|
161 apply (metis equivp_def a) |
|
162 apply rule |
|
163 apply (rule equivp_reflp[OF fset_equivp]) |
|
164 apply (rule list_rel_refl) |
|
165 apply (metis equivp_def a) |
|
166 apply(rule) |
|
167 apply rule |
|
168 apply (rule list_rel_refl) |
|
169 apply (metis equivp_def a) |
|
170 apply rule |
|
171 apply (rule equivp_reflp[OF fset_equivp]) |
|
172 apply (rule list_rel_refl) |
|
173 apply (metis equivp_def a) |
|
174 apply (subgoal_tac "map abs2 r \<approx>1 map abs2 s") |
|
175 apply (metis Quotient_rel[OF Quotient_fset]) |
|
176 apply (auto)[1] |
|
177 apply (subgoal_tac "map abs2 r = map abs2 b") |
|
178 prefer 2 |
|
179 apply (metis Quotient_rel[OF list_quotient[OF b]]) |
|
180 apply (subgoal_tac "map abs2 s = map abs2 ba") |
|
181 prefer 2 |
|
182 apply (metis Quotient_rel[OF list_quotient[OF b]]) |
|
183 apply (simp add: map_rel_cong) |
|
184 apply rule |
|
185 apply (rule rep_abs_rsp[of "list_rel r2" "map abs2"]) |
|
186 apply (rule list_quotient) |
|
187 apply (rule b) |
|
188 apply (rule list_rel_refl) |
|
189 apply (metis equivp_def a) |
|
190 apply rule |
|
191 prefer 2 |
|
192 apply (rule rep_abs_rsp_left[of "list_rel r2" "map abs2"]) |
|
193 apply (rule list_quotient) |
|
194 apply (rule b) |
|
195 apply (rule list_rel_refl) |
|
196 apply (metis equivp_def a) |
|
197 apply (erule conjE)+ |
|
198 apply (subgoal_tac "map abs2 r \<approx>1 map abs2 s") |
|
199 apply (rule map_rel_cong) |
|
200 apply (assumption) |
|
201 apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp a b) |
|
202 done |
|
203 |
|
204 lemma quotient_compose_list_gen: |
|
205 assumes a: "Quotient r2 abs2 rep2" |
|
206 and b: "equivp r2" (* reflp is not enough *) |
|
207 shows "Quotient ((list_rel r2) OOO (op \<approx>1)) |
|
208 (abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)" |
|
209 unfolding Quotient_def comp_def |
|
210 apply (rule)+ |
|
211 apply (simp add: abs_o_rep[OF a] id_simps Quotient_abs_rep[OF Quotient_fset]) |
|
212 apply (rule) |
|
213 apply (rule) |
|
214 apply (rule) |
|
215 apply (rule list_rel_refl) |
|
216 apply (metis b equivp_def) |
|
217 apply (rule) |
|
218 apply (rule equivp_reflp[OF fset_equivp]) |
|
219 apply (rule list_rel_refl) |
|
220 apply (metis b equivp_def) |
|
221 apply rule |
|
222 apply rule |
|
223 apply(rule quotient_compose_list_gen_pre[OF b a]) |
|
224 done |
|
225 |
|
226 (* This is the general statement but the types of abs2 and rep2 |
|
227 are wrong as can be seen in following exanples *) |
|
228 lemma quotient_compose_general: |
|
229 assumes a2: "Quotient r1 abs1 rep1" |
|
230 and "Quotient r2 abs2 rep2" |
|
231 shows "Quotient ((list_rel r2) OOO r1) |
|
232 (abs1 \<circ> (map abs2)) ((map rep2) \<circ> rep1)" |
|
233 sorry |
|
234 |
|
235 thm quotient_compose_list_gen[OF Quotient_fset fset_equivp] |
|
236 thm quotient_compose_general[OF Quotient_fset] |
|
237 (* Doesn't work: *) |
|
238 (* thm quotient_compose_general[OF Quotient_fset Quotient_fset] *) |
|
239 |
|
240 end |
|