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