1 theory Prove |
1 theory Prove |
2 imports Main QuotScript QuotList |
2 imports Main |
3 uses ("quotient.ML") |
|
4 begin |
3 begin |
5 |
|
6 locale QUOT_TYPE = |
|
7 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
8 and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" |
|
9 and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" |
|
10 assumes equiv: "EQUIV R" |
|
11 and rep_prop: "\<And>y. \<exists>x. Rep y = R x" |
|
12 and rep_inverse: "\<And>x. Abs (Rep x) = x" |
|
13 and abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)" |
|
14 and rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)" |
|
15 begin |
|
16 |
|
17 definition |
|
18 "ABS x \<equiv> Abs (R x)" |
|
19 |
|
20 definition |
|
21 "REP a = Eps (Rep a)" |
|
22 |
|
23 lemma lem9: |
|
24 shows "R (Eps (R x)) = R x" |
|
25 proof - |
|
26 have a: "R x x" using equiv by (simp add: EQUIV_REFL_SYM_TRANS REFL_def) |
|
27 then have "R x (Eps (R x))" by (rule someI) |
|
28 then show "R (Eps (R x)) = R x" |
|
29 using equiv unfolding EQUIV_def by simp |
|
30 qed |
|
31 |
|
32 theorem thm10: |
|
33 shows "ABS (REP a) \<equiv> a" |
|
34 apply (rule eq_reflection) |
|
35 unfolding ABS_def REP_def |
|
36 proof - |
|
37 from rep_prop |
|
38 obtain x where eq: "Rep a = R x" by auto |
|
39 have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp |
|
40 also have "\<dots> = Abs (R x)" using lem9 by simp |
|
41 also have "\<dots> = Abs (Rep a)" using eq by simp |
|
42 also have "\<dots> = a" using rep_inverse by simp |
|
43 finally |
|
44 show "Abs (R (Eps (Rep a))) = a" by simp |
|
45 qed |
|
46 |
|
47 lemma REP_refl: |
|
48 shows "R (REP a) (REP a)" |
|
49 unfolding REP_def |
|
50 by (simp add: equiv[simplified EQUIV_def]) |
|
51 |
|
52 lemma lem7: |
|
53 shows "(R x = R y) = (Abs (R x) = Abs (R y))" |
|
54 apply(rule iffI) |
|
55 apply(simp) |
|
56 apply(drule rep_inject[THEN iffD2]) |
|
57 apply(simp add: abs_inverse) |
|
58 done |
|
59 |
|
60 theorem thm11: |
|
61 shows "R r r' = (ABS r = ABS r')" |
|
62 unfolding ABS_def |
|
63 by (simp only: equiv[simplified EQUIV_def] lem7) |
|
64 |
|
65 |
|
66 lemma REP_ABS_rsp: |
|
67 shows "R f (REP (ABS g)) = R f g" |
|
68 and "R (REP (ABS g)) f = R g f" |
|
69 by (simp_all add: thm10 thm11) |
|
70 |
|
71 lemma QUOTIENT: |
|
72 "QUOTIENT R ABS REP" |
|
73 apply(unfold QUOTIENT_def) |
|
74 apply(simp add: thm10) |
|
75 apply(simp add: REP_refl) |
|
76 apply(subst thm11[symmetric]) |
|
77 apply(simp add: equiv[simplified EQUIV_def]) |
|
78 done |
|
79 |
|
80 lemma R_trans: |
|
81 assumes ab: "R a b" |
|
82 and bc: "R b c" |
|
83 shows "R a c" |
|
84 proof - |
|
85 have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp |
|
86 moreover have ab: "R a b" by fact |
|
87 moreover have bc: "R b c" by fact |
|
88 ultimately show "R a c" unfolding TRANS_def by blast |
|
89 qed |
|
90 |
|
91 lemma R_sym: |
|
92 assumes ab: "R a b" |
|
93 shows "R b a" |
|
94 proof - |
|
95 have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp |
|
96 then show "R b a" using ab unfolding SYM_def by blast |
|
97 qed |
|
98 |
|
99 lemma R_trans2: |
|
100 assumes ac: "R a c" |
|
101 and bd: "R b d" |
|
102 shows "R a b = R c d" |
|
103 proof |
|
104 assume "R a b" |
|
105 then have "R b a" using R_sym by blast |
|
106 then have "R b c" using ac R_trans by blast |
|
107 then have "R c b" using R_sym by blast |
|
108 then show "R c d" using bd R_trans by blast |
|
109 next |
|
110 assume "R c d" |
|
111 then have "R a d" using ac R_trans by blast |
|
112 then have "R d a" using R_sym by blast |
|
113 then have "R b a" using bd R_trans by blast |
|
114 then show "R a b" using R_sym by blast |
|
115 qed |
|
116 |
|
117 lemma REPS_same: |
|
118 shows "R (REP a) (REP b) \<equiv> (a = b)" |
|
119 proof - |
|
120 have "R (REP a) (REP b) = (a = b)" |
|
121 proof |
|
122 assume as: "R (REP a) (REP b)" |
|
123 from rep_prop |
|
124 obtain x y |
|
125 where eqs: "Rep a = R x" "Rep b = R y" by blast |
|
126 from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp |
|
127 then have "R x (Eps (R y))" using lem9 by simp |
|
128 then have "R (Eps (R y)) x" using R_sym by blast |
|
129 then have "R y x" using lem9 by simp |
|
130 then have "R x y" using R_sym by blast |
|
131 then have "ABS x = ABS y" using thm11 by simp |
|
132 then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp |
|
133 then show "a = b" using rep_inverse by simp |
|
134 next |
|
135 assume ab: "a = b" |
|
136 have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp |
|
137 then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto |
|
138 qed |
|
139 then show "R (REP a) (REP b) \<equiv> (a = b)" by simp |
|
140 qed |
|
141 |
|
142 end |
|
143 |
|
144 use "quotient.ML" |
|
145 |
4 |
146 ML {* |
5 ML {* |
147 val r = ref (NONE:(unit -> term) option) |
6 val r = ref (NONE:(unit -> term) option) |
148 *} |
7 *} |
149 |
8 |