|
1 theory Quotients |
|
2 imports Main |
|
3 begin |
|
4 |
|
5 (* Other quotients that have not been proved yet *) |
|
6 |
|
7 fun |
|
8 option_rel |
|
9 where |
|
10 "option_rel R None None = True" |
|
11 | "option_rel R (Some x) None = False" |
|
12 | "option_rel R None (Some x) = False" |
|
13 | "option_rel R (Some x) (Some y) = R x y" |
|
14 |
|
15 fun |
|
16 option_map |
|
17 where |
|
18 "option_map f None = None" |
|
19 | "option_map f (Some x) = Some (f x)" |
|
20 |
|
21 fun |
|
22 prod_rel |
|
23 where |
|
24 "prod_rel R1 R2 (a1,a2) (b1,b2) = (R1 a1 b1 \<and> R2 a2 b2)" |
|
25 |
|
26 fun |
|
27 prod_map |
|
28 where |
|
29 "prod_map f1 f2 (a,b) = (f1 a, f2 b)" |
|
30 |
|
31 fun |
|
32 sum_rel |
|
33 where |
|
34 "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1" |
|
35 | "sum_rel R1 R2 (Inl a1) (Inr b2) = False" |
|
36 | "sum_rel R1 R2 (Inr a2) (Inl b1) = False" |
|
37 | "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2" |
|
38 |
|
39 fun |
|
40 sum_map |
|
41 where |
|
42 "sum_map f1 f2 (Inl a) = Inl (f1 a)" |
|
43 | "sum_map f1 f2 (Inr a) = Inr (f2 a)" |
|
44 |
|
45 |
|
46 |
|
47 |
|
48 |
|
49 fun |
|
50 noption_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)" |
|
51 where |
|
52 "noption_map f (nSome x) = nSome (f x)" |
|
53 | "noption_map f nNone = nNone" |
|
54 |
|
55 fun |
|
56 noption_rel |
|
57 where |
|
58 "noption_rel r (nSome x) (nSome y) = r x y" |
|
59 | "noption_rel r _ _ = False" |
|
60 |
|
61 declare [[map noption = (noption_map, noption_rel)]] |
|
62 |
|
63 lemma "noption_map id = id" |
|
64 sorry |
|
65 |
|
66 lemma noption_Quotient: |
|
67 assumes q: "Quotient R Abs Rep" |
|
68 shows "Quotient (noption_rel R) (noption_map Abs) (noption_map Rep)" |
|
69 apply (unfold Quotient_def) |
|
70 apply (auto) |
|
71 using q |
|
72 apply (unfold Quotient_def) |
|
73 apply (case_tac "a :: 'b noption") |
|
74 apply (simp) |
|
75 apply (simp) |
|
76 apply (case_tac "a :: 'b noption") |
|
77 apply (simp only: option_map.simps) |
|
78 apply (subst option_rel.simps) |
|
79 (* Simp starts hanging so don't know how to continue *) |
|
80 sorry |