1 theory Quotients |
1 theory Quotients |
2 imports Main |
2 imports Main |
3 begin |
3 begin |
4 |
4 |
5 definition |
5 (* Other quotients that have not been proved yet *) |
6 "NONEMPTY E \<equiv> \<exists>x. E x x" |
|
7 |
6 |
8 fun |
7 fun |
9 OPTION_REL |
8 option_rel |
10 where |
9 where |
11 "OPTION_REL R None None = True" |
10 "option_rel R None None = True" |
12 | "OPTION_REL R (Some x) None = False" |
11 | "option_rel R (Some x) None = False" |
13 | "OPTION_REL R None (Some x) = False" |
12 | "option_rel R None (Some x) = False" |
14 | "OPTION_REL R (Some x) (Some y) = R x y" |
13 | "option_rel R (Some x) (Some y) = R x y" |
15 |
14 |
16 fun |
15 fun |
17 option_map |
16 option_map |
18 where |
17 where |
19 "option_map f None = None" |
18 "option_map f None = None" |
20 | "option_map f (Some x) = Some (f x)" |
19 | "option_map f (Some x) = Some (f x)" |
21 |
20 |
22 fun |
21 fun |
23 PROD_REL |
22 prod_rel |
24 where |
23 where |
25 "PROD_REL R1 R2 (a1,a2) (b1,b2) = (R1 a1 b1 \<and> R2 a2 b2)" |
24 "prod_rel R1 R2 (a1,a2) (b1,b2) = (R1 a1 b1 \<and> R2 a2 b2)" |
26 |
25 |
27 fun |
26 fun |
28 prod_map |
27 prod_map |
29 where |
28 where |
30 "prod_map f1 f2 (a,b) = (f1 a, f2 b)" |
29 "prod_map f1 f2 (a,b) = (f1 a, f2 b)" |
31 |
30 |
32 fun |
31 fun |
33 SUM_REL |
32 sum_rel |
34 where |
33 where |
35 "SUM_REL R1 R2 (Inl a1) (Inl b1) = R1 a1 b1" |
34 "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1" |
36 | "SUM_REL R1 R2 (Inl a1) (Inr b2) = False" |
35 | "sum_rel R1 R2 (Inl a1) (Inr b2) = False" |
37 | "SUM_REL R1 R2 (Inr a2) (Inl b1) = False" |
36 | "sum_rel R1 R2 (Inr a2) (Inl b1) = False" |
38 | "SUM_REL R1 R2 (Inr a2) (Inr b2) = R2 a2 b2" |
37 | "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2" |
39 |
38 |
40 fun |
39 fun |
41 sum_map |
40 sum_map |
42 where |
41 where |
43 "sum_map f1 f2 (Inl a) = Inl (f1 a)" |
42 "sum_map f1 f2 (Inl a) = Inl (f1 a)" |
44 | "sum_map f1 f2 (Inr a) = Inr (f2 a)" |
43 | "sum_map f1 f2 (Inr a) = Inr (f2 a)" |
45 |
44 |
46 definition |
|
47 "QUOTIENT R Abs Rep \<equiv> (\<forall>a. Abs (Rep a) = a) \<and> |
|
48 (\<forall>a. R (Rep a) (Rep a)) \<and> |
|
49 (\<forall>r s. R r s = (R r r \<and> R s s \<and> (Abs r = Abs s)))" |
|
50 |
45 |
51 lemma QUOTIENT_PROD: |
|
52 assumes a: "QUOTIENT E1 Abs1 Rep1" |
|
53 and b: "QUOTIENT E2 Abs2 Rep2" |
|
54 shows "QUOTIENT (PROD_REL E1 E2) (prod_map Abs1 Abs2) (prod_map Rep1 Rep2)" |
|
55 using a b unfolding QUOTIENT_def |
|
56 oops |
|
57 |
46 |
58 lemma QUOTIENT_ABS_REP_LIST: |
|
59 assumes a: "QUOTIENT_ABS_REP Abs Rep" |
|
60 shows "QUOTIENT_ABS_REP (map Abs) (map Rep)" |
|
61 using a |
|
62 unfolding QUOTIENT_ABS_REP_def |
|
63 apply(rule_tac allI) |
|
64 apply(induct_tac a rule: list.induct) |
|
65 apply(auto) |
|
66 done |
|
67 |
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 |