|
1 lemma in_fun: |
|
2 shows "x \<in> ((f ---> g) s) = g (f x \<in> s)" |
|
3 by (simp add: mem_def) |
|
4 |
|
5 lemma respects_thm: |
|
6 shows "Respects (R1 ===> R2) f = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (f y))" |
|
7 unfolding Respects_def |
|
8 by (simp add: expand_fun_eq) |
|
9 |
|
10 lemma respects_rep_abs: |
|
11 assumes a: "Quotient R1 Abs1 Rep1" |
|
12 and b: "Respects (R1 ===> R2) f" |
|
13 and c: "R1 x x" |
|
14 shows "R2 (f (Rep1 (Abs1 x))) (f x)" |
|
15 using a b[simplified respects_thm] c unfolding Quotient_def |
|
16 by blast |
|
17 |
|
18 lemma respects_mp: |
|
19 assumes a: "Respects (R1 ===> R2) f" |
|
20 and b: "R1 x y" |
|
21 shows "R2 (f x) (f y)" |
|
22 using a b unfolding Respects_def |
|
23 by simp |
|
24 |
|
25 lemma respects_o: |
|
26 assumes a: "Respects (R2 ===> R3) f" |
|
27 and b: "Respects (R1 ===> R2) g" |
|
28 shows "Respects (R1 ===> R3) (f o g)" |
|
29 using a b unfolding Respects_def |
|
30 by simp |
|
31 |
|
32 lemma fun_rel_eq_rel: |
|
33 assumes q1: "Quotient R1 Abs1 Rep1" |
|
34 and q2: "Quotient R2 Abs2 Rep2" |
|
35 shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \<and> (Respects (R1 ===> R2) g) |
|
36 \<and> ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))" |
|
37 using fun_quotient[OF q1 q2] unfolding Respects_def Quotient_def expand_fun_eq |
|
38 by blast |
|
39 |
|
40 lemma let_babs: |
|
41 "v \<in> r \<Longrightarrow> Let v (Babs r lam) = Let v lam" |
|
42 by (simp add: Babs_def) |
|
43 |
|
44 lemma fun_rel_equals: |
|
45 assumes q1: "Quotient R1 Abs1 Rep1" |
|
46 and q2: "Quotient R2 Abs2 Rep2" |
|
47 and r1: "Respects (R1 ===> R2) f" |
|
48 and r2: "Respects (R1 ===> R2) g" |
|
49 shows "((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g) = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))" |
|
50 apply(rule_tac iffI) |
|
51 apply(rule)+ |
|
52 apply (rule apply_rsp'[of "R1" "R2"]) |
|
53 apply(subst Quotient_rel[OF fun_quotient[OF q1 q2]]) |
|
54 apply auto |
|
55 using fun_quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def |
|
56 apply (metis let_rsp q1) |
|
57 apply (metis fun_rel_eq_rel let_rsp q1 q2 r2) |
|
58 using r1 unfolding Respects_def expand_fun_eq |
|
59 apply(simp (no_asm_use)) |
|
60 apply(metis Quotient_rel[OF q2] Quotient_rel_rep[OF q1]) |
|
61 done |
|
62 |
|
63 (* ask Peter: fun_rel_IMP used twice *) |
|
64 lemma fun_rel_IMP2: |
|
65 assumes q1: "Quotient R1 Abs1 Rep1" |
|
66 and q2: "Quotient R2 Abs2 Rep2" |
|
67 and r1: "Respects (R1 ===> R2) f" |
|
68 and r2: "Respects (R1 ===> R2) g" |
|
69 and a: "(Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g" |
|
70 shows "R1 x y \<Longrightarrow> R2 (f x) (g y)" |
|
71 using q1 q2 r1 r2 a |
|
72 by (simp add: fun_rel_equals) |
|
73 |
|
74 lemma lambda_rep_abs_rsp: |
|
75 assumes r1: "\<And>r r'. R1 r r' \<Longrightarrow>R1 r (Rep1 (Abs1 r'))" |
|
76 and r2: "\<And>r r'. R2 r r' \<Longrightarrow>R2 r (Rep2 (Abs2 r'))" |
|
77 shows "(R1 ===> R2) f1 f2 \<Longrightarrow> (R1 ===> R2) f1 ((Abs1 ---> Rep2) ((Rep1 ---> Abs2) f2))" |
|
78 using r1 r2 by auto |
|
79 |
|
80 (* We use id_simps which includes id_apply; so these 2 theorems can be removed *) |
|
81 lemma id_prs: |
|
82 assumes q: "Quotient R Abs Rep" |
|
83 shows "Abs (id (Rep e)) = id e" |
|
84 using Quotient_abs_rep[OF q] by auto |
|
85 |
|
86 lemma id_rsp: |
|
87 assumes q: "Quotient R Abs Rep" |
|
88 and a: "R e1 e2" |
|
89 shows "R (id e1) (id e2)" |
|
90 using a by auto |