equal
deleted
inserted
replaced
43 assumes a: "equivp E" |
43 assumes a: "equivp E" |
44 shows "part_equivp E" |
44 shows "part_equivp E" |
45 using a unfolding equivp_def part_equivp_def |
45 using a unfolding equivp_def part_equivp_def |
46 by auto |
46 by auto |
47 |
47 |
|
48 |
|
49 abbreviation |
|
50 rel_conj (infixr "OOO" 75) |
|
51 where |
|
52 "r1 OOO r2 \<equiv> r1 OO r2 OO r1" |
|
53 |
48 definition |
54 definition |
49 "Quotient E Abs Rep \<equiv> (\<forall>a. Abs (Rep a) = a) \<and> |
55 "Quotient E Abs Rep \<equiv> (\<forall>a. Abs (Rep a) = a) \<and> |
50 (\<forall>a. E (Rep a) (Rep a)) \<and> |
56 (\<forall>a. E (Rep a) (Rep a)) \<and> |
51 (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))" |
57 (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))" |
|
58 |
|
59 (* TEST |
|
60 lemma |
|
61 fixes Abs1::"'b \<Rightarrow> 'c" |
|
62 and Abs2::"'a \<Rightarrow> 'b" |
|
63 and Rep1::"'c \<Rightarrow> 'b" |
|
64 and Rep2::"'b \<Rightarrow> 'a" |
|
65 assumes "Quotient R1 Abs1 Rep1" |
|
66 and "Quotient R2 Abs2 Rep2" |
|
67 shows "Quotient (f R2 R1) (Abs1 \<circ> Abs2) (Rep2 \<circ> Rep1)" |
|
68 *) |
52 |
69 |
53 lemma Quotient_abs_rep: |
70 lemma Quotient_abs_rep: |
54 assumes a: "Quotient E Abs Rep" |
71 assumes a: "Quotient E Abs Rep" |
55 shows "Abs (Rep a) \<equiv> a" |
72 shows "Abs (Rep a) \<equiv> a" |
56 using a unfolding Quotient_def |
73 using a unfolding Quotient_def |
120 "f ---> g \<equiv> fun_map f g" |
137 "f ---> g \<equiv> fun_map f g" |
121 |
138 |
122 lemma fun_map_id: |
139 lemma fun_map_id: |
123 shows "(id ---> id) = id" |
140 shows "(id ---> id) = id" |
124 by (simp add: expand_fun_eq id_def) |
141 by (simp add: expand_fun_eq id_def) |
|
142 |
125 |
143 |
126 fun |
144 fun |
127 fun_rel |
145 fun_rel |
128 where |
146 where |
129 "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))" |
147 "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))" |
219 but we know some of the types of the Rep and Abs functions; |
237 but we know some of the types of the Rep and Abs functions; |
220 so by solving Quotient assumptions we can get a unique R1 that |
238 so by solving Quotient assumptions we can get a unique R1 that |
221 will be provable; which is why we need to use apply_rsp and |
239 will be provable; which is why we need to use apply_rsp and |
222 not the primed version *) |
240 not the primed version *) |
223 lemma apply_rsp: |
241 lemma apply_rsp: |
|
242 fixes f g::"'a \<Rightarrow> 'c" |
224 assumes q: "Quotient R1 Abs1 Rep1" |
243 assumes q: "Quotient R1 Abs1 Rep1" |
225 and a: "(R1 ===> R2) f g" "R1 x y" |
244 and a: "(R1 ===> R2) f g" "R1 x y" |
226 shows "R2 ((f::'a\<Rightarrow>'c) x) ((g::'a\<Rightarrow>'c) y)" |
245 shows "R2 (f x) (g y)" |
227 using a by simp |
246 using a by simp |
228 |
247 |
229 lemma apply_rsp': |
248 lemma apply_rsp': |
230 assumes a: "(R1 ===> R2) f g" "R1 x y" |
249 assumes a: "(R1 ===> R2) f g" "R1 x y" |
231 shows "R2 (f x) (g y)" |
250 shows "R2 (f x) (g y)" |
377 apply(metis Babs_def) |
396 apply(metis Babs_def) |
378 apply (simp add: in_respects) |
397 apply (simp add: in_respects) |
379 using Quotient_rel[OF q] |
398 using Quotient_rel[OF q] |
380 by metis |
399 by metis |
381 |
400 |
382 (* If a user proves that a particular functional relation is an equivalence |
401 (* If a user proves that a particular functional relation |
383 this may be useful in regularising *) |
402 is an equivalence this may be useful in regularising *) |
384 lemma babs_reg_eqv: |
403 lemma babs_reg_eqv: |
385 shows "equivp R \<Longrightarrow> Babs (Respects R) P = P" |
404 shows "equivp R \<Longrightarrow> Babs (Respects R) P = P" |
386 by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp) |
405 by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp) |
387 |
406 |
388 (* 2 lemmas needed for cleaning of quantifiers *) |
407 (* 2 lemmas needed for cleaning of quantifiers *) |