author | haftmann |
Fri, 19 Nov 2010 11:44:46 +0100 | |
changeset 40863 | ab551d108feb |
parent 40850 | 91e583511113 |
child 41062 | fa64f6278568 |
permissions | -rw-r--r-- |
kaliszyk@35222 | 1 |
(* Title: Quotient.thy |
kaliszyk@35222 | 2 |
Author: Cezary Kaliszyk and Christian Urban |
kaliszyk@35222 | 3 |
*) |
kaliszyk@35222 | 4 |
|
huffman@35294 | 5 |
header {* Definition of Quotient Types *} |
huffman@35294 | 6 |
|
kaliszyk@35222 | 7 |
theory Quotient |
haftmann@40699 | 8 |
imports Plain Hilbert_Choice Equiv_Relations |
kaliszyk@35222 | 9 |
uses |
wenzelm@38275 | 10 |
("Tools/Quotient/quotient_info.ML") |
wenzelm@38275 | 11 |
("Tools/Quotient/quotient_typ.ML") |
wenzelm@38275 | 12 |
("Tools/Quotient/quotient_def.ML") |
wenzelm@38275 | 13 |
("Tools/Quotient/quotient_term.ML") |
wenzelm@38275 | 14 |
("Tools/Quotient/quotient_tacs.ML") |
kaliszyk@35222 | 15 |
begin |
kaliszyk@35222 | 16 |
|
kaliszyk@35222 | 17 |
|
kaliszyk@35222 | 18 |
text {* |
kaliszyk@35222 | 19 |
Basic definition for equivalence relations |
kaliszyk@35222 | 20 |
that are represented by predicates. |
kaliszyk@35222 | 21 |
*} |
kaliszyk@35222 | 22 |
|
kaliszyk@35222 | 23 |
definition |
haftmann@40699 | 24 |
"reflp E \<longleftrightarrow> (\<forall>x. E x x)" |
haftmann@40699 | 25 |
|
haftmann@40699 | 26 |
lemma refl_reflp: |
haftmann@40699 | 27 |
"refl A \<longleftrightarrow> reflp (\<lambda>x y. (x, y) \<in> A)" |
haftmann@40699 | 28 |
by (simp add: refl_on_def reflp_def) |
kaliszyk@35222 | 29 |
|
kaliszyk@35222 | 30 |
definition |
haftmann@40699 | 31 |
"symp E \<longleftrightarrow> (\<forall>x y. E x y \<longrightarrow> E y x)" |
haftmann@40699 | 32 |
|
haftmann@40699 | 33 |
lemma sym_symp: |
haftmann@40699 | 34 |
"sym A \<longleftrightarrow> symp (\<lambda>x y. (x, y) \<in> A)" |
haftmann@40699 | 35 |
by (simp add: sym_def symp_def) |
kaliszyk@35222 | 36 |
|
kaliszyk@35222 | 37 |
definition |
haftmann@40699 | 38 |
"transp E \<longleftrightarrow> (\<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z)" |
haftmann@40699 | 39 |
|
haftmann@40699 | 40 |
lemma trans_transp: |
haftmann@40699 | 41 |
"trans A \<longleftrightarrow> transp (\<lambda>x y. (x, y) \<in> A)" |
haftmann@40699 | 42 |
by (auto simp add: trans_def transp_def) |
kaliszyk@35222 | 43 |
|
kaliszyk@35222 | 44 |
definition |
haftmann@40699 | 45 |
"equivp E \<longleftrightarrow> (\<forall>x y. E x y = (E x = E y))" |
kaliszyk@35222 | 46 |
|
kaliszyk@35222 | 47 |
lemma equivp_reflp_symp_transp: |
kaliszyk@35222 | 48 |
shows "equivp E = (reflp E \<and> symp E \<and> transp E)" |
nipkow@39535 | 49 |
unfolding equivp_def reflp_def symp_def transp_def fun_eq_iff |
kaliszyk@35222 | 50 |
by blast |
kaliszyk@35222 | 51 |
|
haftmann@40699 | 52 |
lemma equiv_equivp: |
haftmann@40699 | 53 |
"equiv UNIV A \<longleftrightarrow> equivp (\<lambda>x y. (x, y) \<in> A)" |
haftmann@40699 | 54 |
by (simp add: equiv_def equivp_reflp_symp_transp refl_reflp sym_symp trans_transp) |
haftmann@40699 | 55 |
|
kaliszyk@35222 | 56 |
lemma equivp_reflp: |
kaliszyk@35222 | 57 |
shows "equivp E \<Longrightarrow> E x x" |
kaliszyk@35222 | 58 |
by (simp only: equivp_reflp_symp_transp reflp_def) |
kaliszyk@35222 | 59 |
|
kaliszyk@35222 | 60 |
lemma equivp_symp: |
kaliszyk@35222 | 61 |
shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y x" |
haftmann@40699 | 62 |
by (simp add: equivp_def) |
kaliszyk@35222 | 63 |
|
kaliszyk@35222 | 64 |
lemma equivp_transp: |
kaliszyk@35222 | 65 |
shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y z \<Longrightarrow> E x z" |
haftmann@40699 | 66 |
by (simp add: equivp_def) |
kaliszyk@35222 | 67 |
|
kaliszyk@35222 | 68 |
lemma equivpI: |
kaliszyk@35222 | 69 |
assumes "reflp R" "symp R" "transp R" |
kaliszyk@35222 | 70 |
shows "equivp R" |
kaliszyk@35222 | 71 |
using assms by (simp add: equivp_reflp_symp_transp) |
kaliszyk@35222 | 72 |
|
kaliszyk@35222 | 73 |
lemma identity_equivp: |
kaliszyk@35222 | 74 |
shows "equivp (op =)" |
kaliszyk@35222 | 75 |
unfolding equivp_def |
kaliszyk@35222 | 76 |
by auto |
kaliszyk@35222 | 77 |
|
kaliszyk@37493 | 78 |
text {* Partial equivalences *} |
kaliszyk@35222 | 79 |
|
kaliszyk@35222 | 80 |
definition |
haftmann@40699 | 81 |
"part_equivp E \<longleftrightarrow> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))" |
kaliszyk@35222 | 82 |
|
kaliszyk@35222 | 83 |
lemma equivp_implies_part_equivp: |
kaliszyk@35222 | 84 |
assumes a: "equivp E" |
kaliszyk@35222 | 85 |
shows "part_equivp E" |
kaliszyk@35222 | 86 |
using a |
kaliszyk@35222 | 87 |
unfolding equivp_def part_equivp_def |
kaliszyk@35222 | 88 |
by auto |
kaliszyk@35222 | 89 |
|
kaliszyk@37493 | 90 |
lemma part_equivp_symp: |
kaliszyk@37493 | 91 |
assumes e: "part_equivp R" |
kaliszyk@37493 | 92 |
and a: "R x y" |
kaliszyk@37493 | 93 |
shows "R y x" |
kaliszyk@37493 | 94 |
using e[simplified part_equivp_def] a |
kaliszyk@37493 | 95 |
by (metis) |
kaliszyk@37493 | 96 |
|
kaliszyk@37493 | 97 |
lemma part_equivp_typedef: |
kaliszyk@37493 | 98 |
shows "part_equivp R \<Longrightarrow> \<exists>d. d \<in> (\<lambda>c. \<exists>x. R x x \<and> c = R x)" |
kaliszyk@37493 | 99 |
unfolding part_equivp_def mem_def |
kaliszyk@37493 | 100 |
apply clarify |
kaliszyk@37493 | 101 |
apply (intro exI) |
kaliszyk@37493 | 102 |
apply (rule conjI) |
kaliszyk@37493 | 103 |
apply assumption |
kaliszyk@37493 | 104 |
apply (rule refl) |
kaliszyk@37493 | 105 |
done |
kaliszyk@37493 | 106 |
|
kaliszyk@40212 | 107 |
lemma part_equivp_refl_symp_transp: |
kaliszyk@40212 | 108 |
shows "part_equivp E \<longleftrightarrow> ((\<exists>x. E x x) \<and> symp E \<and> transp E)" |
kaliszyk@40212 | 109 |
proof |
kaliszyk@40212 | 110 |
assume "part_equivp E" |
kaliszyk@40212 | 111 |
then show "(\<exists>x. E x x) \<and> symp E \<and> transp E" |
kaliszyk@40212 | 112 |
unfolding part_equivp_def symp_def transp_def |
kaliszyk@40212 | 113 |
by metis |
kaliszyk@40212 | 114 |
next |
kaliszyk@40212 | 115 |
assume a: "(\<exists>x. E x x) \<and> symp E \<and> transp E" |
kaliszyk@40212 | 116 |
then have b: "(\<forall>x y. E x y \<longrightarrow> E y x)" and c: "(\<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z)" |
kaliszyk@40212 | 117 |
unfolding symp_def transp_def by (metis, metis) |
kaliszyk@40212 | 118 |
have "(\<forall>x y. E x y = (E x x \<and> E y y \<and> E x = E y))" |
kaliszyk@40212 | 119 |
proof (intro allI iffI conjI) |
kaliszyk@40212 | 120 |
fix x y |
kaliszyk@40212 | 121 |
assume d: "E x y" |
kaliszyk@40212 | 122 |
then show "E x x" using b c by metis |
kaliszyk@40212 | 123 |
show "E y y" using b c d by metis |
kaliszyk@40212 | 124 |
show "E x = E y" unfolding fun_eq_iff using b c d by metis |
kaliszyk@40212 | 125 |
next |
kaliszyk@40212 | 126 |
fix x y |
kaliszyk@40212 | 127 |
assume "E x x \<and> E y y \<and> E x = E y" |
kaliszyk@40212 | 128 |
then show "E x y" using b c by metis |
kaliszyk@40212 | 129 |
qed |
kaliszyk@40212 | 130 |
then show "part_equivp E" unfolding part_equivp_def using a by metis |
kaliszyk@40212 | 131 |
qed |
kaliszyk@40212 | 132 |
|
haftmann@40699 | 133 |
lemma part_equivpI: |
haftmann@40699 | 134 |
assumes "\<exists>x. R x x" "symp R" "transp R" |
haftmann@40699 | 135 |
shows "part_equivp R" |
haftmann@40699 | 136 |
using assms by (simp add: part_equivp_refl_symp_transp) |
haftmann@40699 | 137 |
|
kaliszyk@35222 | 138 |
text {* Composition of Relations *} |
kaliszyk@35222 | 139 |
|
kaliszyk@35222 | 140 |
abbreviation |
kaliszyk@35222 | 141 |
rel_conj (infixr "OOO" 75) |
kaliszyk@35222 | 142 |
where |
kaliszyk@35222 | 143 |
"r1 OOO r2 \<equiv> r1 OO r2 OO r1" |
kaliszyk@35222 | 144 |
|
kaliszyk@35222 | 145 |
lemma eq_comp_r: |
kaliszyk@35222 | 146 |
shows "((op =) OOO R) = R" |
nipkow@39535 | 147 |
by (auto simp add: fun_eq_iff) |
kaliszyk@35222 | 148 |
|
huffman@35294 | 149 |
subsection {* Respects predicate *} |
kaliszyk@35222 | 150 |
|
kaliszyk@35222 | 151 |
definition |
haftmann@40699 | 152 |
Respects :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set" |
kaliszyk@35222 | 153 |
where |
haftmann@40699 | 154 |
"Respects R x = R x x" |
kaliszyk@35222 | 155 |
|
kaliszyk@35222 | 156 |
lemma in_respects: |
haftmann@40699 | 157 |
shows "x \<in> Respects R \<longleftrightarrow> R x x" |
kaliszyk@35222 | 158 |
unfolding mem_def Respects_def |
kaliszyk@35222 | 159 |
by simp |
kaliszyk@35222 | 160 |
|
huffman@35294 | 161 |
subsection {* Function map and function relation *} |
kaliszyk@35222 | 162 |
|
haftmann@40850 | 163 |
notation map_fun (infixr "--->" 55) |
haftmann@40699 | 164 |
|
haftmann@40850 | 165 |
lemma map_fun_id: |
haftmann@40699 | 166 |
"(id ---> id) = id" |
haftmann@40850 | 167 |
by (simp add: fun_eq_iff) |
kaliszyk@35222 | 168 |
|
kaliszyk@35222 | 169 |
definition |
haftmann@40863 | 170 |
fun_rel :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool" (infixr "===>" 55) |
kaliszyk@35222 | 171 |
where |
haftmann@40699 | 172 |
"fun_rel E1 E2 = (\<lambda>f g. \<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))" |
kaliszyk@35222 | 173 |
|
kaliszyk@36276 | 174 |
lemma fun_relI [intro]: |
haftmann@40699 | 175 |
assumes "\<And>x y. E1 x y \<Longrightarrow> E2 (f x) (g y)" |
haftmann@40699 | 176 |
shows "(E1 ===> E2) f g" |
kaliszyk@36276 | 177 |
using assms by (simp add: fun_rel_def) |
kaliszyk@35222 | 178 |
|
haftmann@40699 | 179 |
lemma fun_relE: |
haftmann@40699 | 180 |
assumes "(E1 ===> E2) f g" and "E1 x y" |
haftmann@40699 | 181 |
obtains "E2 (f x) (g y)" |
haftmann@40699 | 182 |
using assms by (simp add: fun_rel_def) |
kaliszyk@35222 | 183 |
|
kaliszyk@35222 | 184 |
lemma fun_rel_eq: |
kaliszyk@35222 | 185 |
shows "((op =) ===> (op =)) = (op =)" |
haftmann@40699 | 186 |
by (auto simp add: fun_eq_iff elim: fun_relE) |
kaliszyk@35222 | 187 |
|
kaliszyk@35222 | 188 |
|
huffman@35294 | 189 |
subsection {* Quotient Predicate *} |
kaliszyk@35222 | 190 |
|
kaliszyk@35222 | 191 |
definition |
haftmann@40699 | 192 |
"Quotient E Abs Rep \<longleftrightarrow> |
kaliszyk@35222 | 193 |
(\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. E (Rep a) (Rep a)) \<and> |
kaliszyk@35222 | 194 |
(\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))" |
kaliszyk@35222 | 195 |
|
kaliszyk@35222 | 196 |
lemma Quotient_abs_rep: |
kaliszyk@35222 | 197 |
assumes a: "Quotient E Abs Rep" |
kaliszyk@35222 | 198 |
shows "Abs (Rep a) = a" |
kaliszyk@35222 | 199 |
using a |
kaliszyk@35222 | 200 |
unfolding Quotient_def |
kaliszyk@35222 | 201 |
by simp |
kaliszyk@35222 | 202 |
|
kaliszyk@35222 | 203 |
lemma Quotient_rep_reflp: |
kaliszyk@35222 | 204 |
assumes a: "Quotient E Abs Rep" |
kaliszyk@35222 | 205 |
shows "E (Rep a) (Rep a)" |
kaliszyk@35222 | 206 |
using a |
kaliszyk@35222 | 207 |
unfolding Quotient_def |
kaliszyk@35222 | 208 |
by blast |
kaliszyk@35222 | 209 |
|
kaliszyk@35222 | 210 |
lemma Quotient_rel: |
kaliszyk@35222 | 211 |
assumes a: "Quotient E Abs Rep" |
kaliszyk@35222 | 212 |
shows " E r s = (E r r \<and> E s s \<and> (Abs r = Abs s))" |
kaliszyk@35222 | 213 |
using a |
kaliszyk@35222 | 214 |
unfolding Quotient_def |
kaliszyk@35222 | 215 |
by blast |
kaliszyk@35222 | 216 |
|
kaliszyk@35222 | 217 |
lemma Quotient_rel_rep: |
kaliszyk@35222 | 218 |
assumes a: "Quotient R Abs Rep" |
kaliszyk@35222 | 219 |
shows "R (Rep a) (Rep b) = (a = b)" |
kaliszyk@35222 | 220 |
using a |
kaliszyk@35222 | 221 |
unfolding Quotient_def |
kaliszyk@35222 | 222 |
by metis |
kaliszyk@35222 | 223 |
|
kaliszyk@35222 | 224 |
lemma Quotient_rep_abs: |
kaliszyk@35222 | 225 |
assumes a: "Quotient R Abs Rep" |
kaliszyk@35222 | 226 |
shows "R r r \<Longrightarrow> R (Rep (Abs r)) r" |
kaliszyk@35222 | 227 |
using a unfolding Quotient_def |
kaliszyk@35222 | 228 |
by blast |
kaliszyk@35222 | 229 |
|
kaliszyk@35222 | 230 |
lemma Quotient_rel_abs: |
kaliszyk@35222 | 231 |
assumes a: "Quotient E Abs Rep" |
kaliszyk@35222 | 232 |
shows "E r s \<Longrightarrow> Abs r = Abs s" |
kaliszyk@35222 | 233 |
using a unfolding Quotient_def |
kaliszyk@35222 | 234 |
by blast |
kaliszyk@35222 | 235 |
|
kaliszyk@35222 | 236 |
lemma Quotient_symp: |
kaliszyk@35222 | 237 |
assumes a: "Quotient E Abs Rep" |
kaliszyk@35222 | 238 |
shows "symp E" |
kaliszyk@35222 | 239 |
using a unfolding Quotient_def symp_def |
kaliszyk@35222 | 240 |
by metis |
kaliszyk@35222 | 241 |
|
kaliszyk@35222 | 242 |
lemma Quotient_transp: |
kaliszyk@35222 | 243 |
assumes a: "Quotient E Abs Rep" |
kaliszyk@35222 | 244 |
shows "transp E" |
kaliszyk@35222 | 245 |
using a unfolding Quotient_def transp_def |
kaliszyk@35222 | 246 |
by metis |
kaliszyk@35222 | 247 |
|
kaliszyk@35222 | 248 |
lemma identity_quotient: |
kaliszyk@35222 | 249 |
shows "Quotient (op =) id id" |
kaliszyk@35222 | 250 |
unfolding Quotient_def id_def |
kaliszyk@35222 | 251 |
by blast |
kaliszyk@35222 | 252 |
|
kaliszyk@35222 | 253 |
lemma fun_quotient: |
kaliszyk@35222 | 254 |
assumes q1: "Quotient R1 abs1 rep1" |
kaliszyk@35222 | 255 |
and q2: "Quotient R2 abs2 rep2" |
kaliszyk@35222 | 256 |
shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" |
kaliszyk@35222 | 257 |
proof - |
haftmann@40699 | 258 |
have "\<And>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a" |
haftmann@40699 | 259 |
using q1 q2 by (simp add: Quotient_def fun_eq_iff) |
kaliszyk@35222 | 260 |
moreover |
haftmann@40699 | 261 |
have "\<And>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)" |
haftmann@40699 | 262 |
by (rule fun_relI) |
haftmann@40699 | 263 |
(insert q1 q2 Quotient_rel_abs [of R1 abs1 rep1] Quotient_rel_rep [of R2 abs2 rep2], |
haftmann@40699 | 264 |
simp (no_asm) add: Quotient_def, simp) |
kaliszyk@35222 | 265 |
moreover |
haftmann@40699 | 266 |
have "\<And>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and> |
kaliszyk@35222 | 267 |
(rep1 ---> abs2) r = (rep1 ---> abs2) s)" |
haftmann@40699 | 268 |
apply(auto simp add: fun_rel_def fun_eq_iff) |
kaliszyk@35222 | 269 |
using q1 q2 unfolding Quotient_def |
kaliszyk@35222 | 270 |
apply(metis) |
kaliszyk@35222 | 271 |
using q1 q2 unfolding Quotient_def |
kaliszyk@35222 | 272 |
apply(metis) |
kaliszyk@35222 | 273 |
using q1 q2 unfolding Quotient_def |
kaliszyk@35222 | 274 |
apply(metis) |
kaliszyk@35222 | 275 |
using q1 q2 unfolding Quotient_def |
kaliszyk@35222 | 276 |
apply(metis) |
kaliszyk@35222 | 277 |
done |
kaliszyk@35222 | 278 |
ultimately |
kaliszyk@35222 | 279 |
show "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" |
kaliszyk@35222 | 280 |
unfolding Quotient_def by blast |
kaliszyk@35222 | 281 |
qed |
kaliszyk@35222 | 282 |
|
kaliszyk@35222 | 283 |
lemma abs_o_rep: |
kaliszyk@35222 | 284 |
assumes a: "Quotient R Abs Rep" |
kaliszyk@35222 | 285 |
shows "Abs o Rep = id" |
nipkow@39535 | 286 |
unfolding fun_eq_iff |
kaliszyk@35222 | 287 |
by (simp add: Quotient_abs_rep[OF a]) |
kaliszyk@35222 | 288 |
|
kaliszyk@35222 | 289 |
lemma equals_rsp: |
kaliszyk@35222 | 290 |
assumes q: "Quotient R Abs Rep" |
kaliszyk@35222 | 291 |
and a: "R xa xb" "R ya yb" |
kaliszyk@35222 | 292 |
shows "R xa ya = R xb yb" |
kaliszyk@35222 | 293 |
using a Quotient_symp[OF q] Quotient_transp[OF q] |
kaliszyk@35222 | 294 |
unfolding symp_def transp_def |
kaliszyk@35222 | 295 |
by blast |
kaliszyk@35222 | 296 |
|
kaliszyk@35222 | 297 |
lemma lambda_prs: |
kaliszyk@35222 | 298 |
assumes q1: "Quotient R1 Abs1 Rep1" |
kaliszyk@35222 | 299 |
and q2: "Quotient R2 Abs2 Rep2" |
kaliszyk@35222 | 300 |
shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)" |
nipkow@39535 | 301 |
unfolding fun_eq_iff |
kaliszyk@35222 | 302 |
using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] |
haftmann@40699 | 303 |
by (simp add:) |
kaliszyk@35222 | 304 |
|
kaliszyk@35222 | 305 |
lemma lambda_prs1: |
kaliszyk@35222 | 306 |
assumes q1: "Quotient R1 Abs1 Rep1" |
kaliszyk@35222 | 307 |
and q2: "Quotient R2 Abs2 Rep2" |
kaliszyk@35222 | 308 |
shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)" |
nipkow@39535 | 309 |
unfolding fun_eq_iff |
kaliszyk@35222 | 310 |
using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] |
haftmann@40699 | 311 |
by (simp add:) |
kaliszyk@35222 | 312 |
|
kaliszyk@35222 | 313 |
lemma rep_abs_rsp: |
kaliszyk@35222 | 314 |
assumes q: "Quotient R Abs Rep" |
kaliszyk@35222 | 315 |
and a: "R x1 x2" |
kaliszyk@35222 | 316 |
shows "R x1 (Rep (Abs x2))" |
kaliszyk@35222 | 317 |
using a Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q] |
kaliszyk@35222 | 318 |
by metis |
kaliszyk@35222 | 319 |
|
kaliszyk@35222 | 320 |
lemma rep_abs_rsp_left: |
kaliszyk@35222 | 321 |
assumes q: "Quotient R Abs Rep" |
kaliszyk@35222 | 322 |
and a: "R x1 x2" |
kaliszyk@35222 | 323 |
shows "R (Rep (Abs x1)) x2" |
kaliszyk@35222 | 324 |
using a Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q] |
kaliszyk@35222 | 325 |
by metis |
kaliszyk@35222 | 326 |
|
kaliszyk@35222 | 327 |
text{* |
kaliszyk@35222 | 328 |
In the following theorem R1 can be instantiated with anything, |
kaliszyk@35222 | 329 |
but we know some of the types of the Rep and Abs functions; |
kaliszyk@35222 | 330 |
so by solving Quotient assumptions we can get a unique R1 that |
kaliszyk@35236 | 331 |
will be provable; which is why we need to use @{text apply_rsp} and |
kaliszyk@35222 | 332 |
not the primed version *} |
kaliszyk@35222 | 333 |
|
kaliszyk@35222 | 334 |
lemma apply_rsp: |
kaliszyk@35222 | 335 |
fixes f g::"'a \<Rightarrow> 'c" |
kaliszyk@35222 | 336 |
assumes q: "Quotient R1 Abs1 Rep1" |
kaliszyk@35222 | 337 |
and a: "(R1 ===> R2) f g" "R1 x y" |
kaliszyk@35222 | 338 |
shows "R2 (f x) (g y)" |
haftmann@40699 | 339 |
using a by (auto elim: fun_relE) |
kaliszyk@35222 | 340 |
|
kaliszyk@35222 | 341 |
lemma apply_rsp': |
kaliszyk@35222 | 342 |
assumes a: "(R1 ===> R2) f g" "R1 x y" |
kaliszyk@35222 | 343 |
shows "R2 (f x) (g y)" |
haftmann@40699 | 344 |
using a by (auto elim: fun_relE) |
kaliszyk@35222 | 345 |
|
huffman@35294 | 346 |
subsection {* lemmas for regularisation of ball and bex *} |
kaliszyk@35222 | 347 |
|
kaliszyk@35222 | 348 |
lemma ball_reg_eqv: |
kaliszyk@35222 | 349 |
fixes P :: "'a \<Rightarrow> bool" |
kaliszyk@35222 | 350 |
assumes a: "equivp R" |
kaliszyk@35222 | 351 |
shows "Ball (Respects R) P = (All P)" |
kaliszyk@35222 | 352 |
using a |
kaliszyk@35222 | 353 |
unfolding equivp_def |
kaliszyk@35222 | 354 |
by (auto simp add: in_respects) |
kaliszyk@35222 | 355 |
|
kaliszyk@35222 | 356 |
lemma bex_reg_eqv: |
kaliszyk@35222 | 357 |
fixes P :: "'a \<Rightarrow> bool" |
kaliszyk@35222 | 358 |
assumes a: "equivp R" |
kaliszyk@35222 | 359 |
shows "Bex (Respects R) P = (Ex P)" |
kaliszyk@35222 | 360 |
using a |
kaliszyk@35222 | 361 |
unfolding equivp_def |
kaliszyk@35222 | 362 |
by (auto simp add: in_respects) |
kaliszyk@35222 | 363 |
|
kaliszyk@35222 | 364 |
lemma ball_reg_right: |
kaliszyk@35222 | 365 |
assumes a: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x" |
kaliszyk@35222 | 366 |
shows "All P \<longrightarrow> Ball R Q" |
blanchet@40137 | 367 |
using a by (metis Collect_def Collect_mem_eq) |
kaliszyk@35222 | 368 |
|
kaliszyk@35222 | 369 |
lemma bex_reg_left: |
kaliszyk@35222 | 370 |
assumes a: "\<And>x. R x \<Longrightarrow> Q x \<longrightarrow> P x" |
kaliszyk@35222 | 371 |
shows "Bex R Q \<longrightarrow> Ex P" |
blanchet@40137 | 372 |
using a by (metis Collect_def Collect_mem_eq) |
kaliszyk@35222 | 373 |
|
kaliszyk@35222 | 374 |
lemma ball_reg_left: |
kaliszyk@35222 | 375 |
assumes a: "equivp R" |
kaliszyk@35222 | 376 |
shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P" |
kaliszyk@35222 | 377 |
using a by (metis equivp_reflp in_respects) |
kaliszyk@35222 | 378 |
|
kaliszyk@35222 | 379 |
lemma bex_reg_right: |
kaliszyk@35222 | 380 |
assumes a: "equivp R" |
kaliszyk@35222 | 381 |
shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P" |
kaliszyk@35222 | 382 |
using a by (metis equivp_reflp in_respects) |
kaliszyk@35222 | 383 |
|
kaliszyk@35222 | 384 |
lemma ball_reg_eqv_range: |
kaliszyk@35222 | 385 |
fixes P::"'a \<Rightarrow> bool" |
kaliszyk@35222 | 386 |
and x::"'a" |
kaliszyk@35222 | 387 |
assumes a: "equivp R2" |
kaliszyk@35222 | 388 |
shows "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))" |
kaliszyk@35222 | 389 |
apply(rule iffI) |
kaliszyk@35222 | 390 |
apply(rule allI) |
kaliszyk@35222 | 391 |
apply(drule_tac x="\<lambda>y. f x" in bspec) |
haftmann@40699 | 392 |
apply(simp add: in_respects fun_rel_def) |
kaliszyk@35222 | 393 |
apply(rule impI) |
kaliszyk@35222 | 394 |
using a equivp_reflp_symp_transp[of "R2"] |
kaliszyk@35222 | 395 |
apply(simp add: reflp_def) |
kaliszyk@35222 | 396 |
apply(simp) |
kaliszyk@35222 | 397 |
apply(simp) |
kaliszyk@35222 | 398 |
done |
kaliszyk@35222 | 399 |
|
kaliszyk@35222 | 400 |
lemma bex_reg_eqv_range: |
kaliszyk@35222 | 401 |
assumes a: "equivp R2" |
kaliszyk@35222 | 402 |
shows "(Bex (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = Ex (\<lambda>f. P (f x)))" |
kaliszyk@35222 | 403 |
apply(auto) |
kaliszyk@35222 | 404 |
apply(rule_tac x="\<lambda>y. f x" in bexI) |
kaliszyk@35222 | 405 |
apply(simp) |
haftmann@40699 | 406 |
apply(simp add: Respects_def in_respects fun_rel_def) |
kaliszyk@35222 | 407 |
apply(rule impI) |
kaliszyk@35222 | 408 |
using a equivp_reflp_symp_transp[of "R2"] |
kaliszyk@35222 | 409 |
apply(simp add: reflp_def) |
kaliszyk@35222 | 410 |
done |
kaliszyk@35222 | 411 |
|
kaliszyk@35222 | 412 |
(* Next four lemmas are unused *) |
kaliszyk@35222 | 413 |
lemma all_reg: |
kaliszyk@35222 | 414 |
assumes a: "!x :: 'a. (P x --> Q x)" |
kaliszyk@35222 | 415 |
and b: "All P" |
kaliszyk@35222 | 416 |
shows "All Q" |
kaliszyk@35222 | 417 |
using a b by (metis) |
kaliszyk@35222 | 418 |
|
kaliszyk@35222 | 419 |
lemma ex_reg: |
kaliszyk@35222 | 420 |
assumes a: "!x :: 'a. (P x --> Q x)" |
kaliszyk@35222 | 421 |
and b: "Ex P" |
kaliszyk@35222 | 422 |
shows "Ex Q" |
kaliszyk@35222 | 423 |
using a b by metis |
kaliszyk@35222 | 424 |
|
kaliszyk@35222 | 425 |
lemma ball_reg: |
kaliszyk@35222 | 426 |
assumes a: "!x :: 'a. (R x --> P x --> Q x)" |
kaliszyk@35222 | 427 |
and b: "Ball R P" |
kaliszyk@35222 | 428 |
shows "Ball R Q" |
blanchet@40137 | 429 |
using a b by (metis Collect_def Collect_mem_eq) |
kaliszyk@35222 | 430 |
|
kaliszyk@35222 | 431 |
lemma bex_reg: |
kaliszyk@35222 | 432 |
assumes a: "!x :: 'a. (R x --> P x --> Q x)" |
kaliszyk@35222 | 433 |
and b: "Bex R P" |
kaliszyk@35222 | 434 |
shows "Bex R Q" |
blanchet@40137 | 435 |
using a b by (metis Collect_def Collect_mem_eq) |
kaliszyk@35222 | 436 |
|
kaliszyk@35222 | 437 |
|
kaliszyk@35222 | 438 |
lemma ball_all_comm: |
kaliszyk@35222 | 439 |
assumes "\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)" |
kaliszyk@35222 | 440 |
shows "(\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y)" |
kaliszyk@35222 | 441 |
using assms by auto |
kaliszyk@35222 | 442 |
|
kaliszyk@35222 | 443 |
lemma bex_ex_comm: |
kaliszyk@35222 | 444 |
assumes "(\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)" |
kaliszyk@35222 | 445 |
shows "(\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y)" |
kaliszyk@35222 | 446 |
using assms by auto |
kaliszyk@35222 | 447 |
|
huffman@35294 | 448 |
subsection {* Bounded abstraction *} |
kaliszyk@35222 | 449 |
|
kaliszyk@35222 | 450 |
definition |
haftmann@40699 | 451 |
Babs :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
kaliszyk@35222 | 452 |
where |
kaliszyk@35222 | 453 |
"x \<in> p \<Longrightarrow> Babs p m x = m x" |
kaliszyk@35222 | 454 |
|
kaliszyk@35222 | 455 |
lemma babs_rsp: |
kaliszyk@35222 | 456 |
assumes q: "Quotient R1 Abs1 Rep1" |
kaliszyk@35222 | 457 |
and a: "(R1 ===> R2) f g" |
kaliszyk@35222 | 458 |
shows "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)" |
haftmann@40699 | 459 |
apply (auto simp add: Babs_def in_respects fun_rel_def) |
kaliszyk@35222 | 460 |
apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1") |
haftmann@40699 | 461 |
using a apply (simp add: Babs_def fun_rel_def) |
haftmann@40699 | 462 |
apply (simp add: in_respects fun_rel_def) |
kaliszyk@35222 | 463 |
using Quotient_rel[OF q] |
kaliszyk@35222 | 464 |
by metis |
kaliszyk@35222 | 465 |
|
kaliszyk@35222 | 466 |
lemma babs_prs: |
kaliszyk@35222 | 467 |
assumes q1: "Quotient R1 Abs1 Rep1" |
kaliszyk@35222 | 468 |
and q2: "Quotient R2 Abs2 Rep2" |
kaliszyk@35222 | 469 |
shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f" |
kaliszyk@35222 | 470 |
apply (rule ext) |
haftmann@40699 | 471 |
apply (simp add:) |
kaliszyk@35222 | 472 |
apply (subgoal_tac "Rep1 x \<in> Respects R1") |
kaliszyk@35222 | 473 |
apply (simp add: Babs_def Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
kaliszyk@35222 | 474 |
apply (simp add: in_respects Quotient_rel_rep[OF q1]) |
kaliszyk@35222 | 475 |
done |
kaliszyk@35222 | 476 |
|
kaliszyk@35222 | 477 |
lemma babs_simp: |
kaliszyk@35222 | 478 |
assumes q: "Quotient R1 Abs Rep" |
kaliszyk@35222 | 479 |
shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)" |
kaliszyk@35222 | 480 |
apply(rule iffI) |
kaliszyk@35222 | 481 |
apply(simp_all only: babs_rsp[OF q]) |
haftmann@40699 | 482 |
apply(auto simp add: Babs_def fun_rel_def) |
kaliszyk@35222 | 483 |
apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1") |
kaliszyk@35222 | 484 |
apply(metis Babs_def) |
kaliszyk@35222 | 485 |
apply (simp add: in_respects) |
kaliszyk@35222 | 486 |
using Quotient_rel[OF q] |
kaliszyk@35222 | 487 |
by metis |
kaliszyk@35222 | 488 |
|
kaliszyk@35222 | 489 |
(* If a user proves that a particular functional relation |
kaliszyk@35222 | 490 |
is an equivalence this may be useful in regularising *) |
kaliszyk@35222 | 491 |
lemma babs_reg_eqv: |
kaliszyk@35222 | 492 |
shows "equivp R \<Longrightarrow> Babs (Respects R) P = P" |
nipkow@39535 | 493 |
by (simp add: fun_eq_iff Babs_def in_respects equivp_reflp) |
kaliszyk@35222 | 494 |
|
kaliszyk@35222 | 495 |
|
kaliszyk@35222 | 496 |
(* 3 lemmas needed for proving repabs_inj *) |
kaliszyk@35222 | 497 |
lemma ball_rsp: |
kaliszyk@35222 | 498 |
assumes a: "(R ===> (op =)) f g" |
kaliszyk@35222 | 499 |
shows "Ball (Respects R) f = Ball (Respects R) g" |
haftmann@40699 | 500 |
using a by (auto simp add: Ball_def in_respects elim: fun_relE) |
kaliszyk@35222 | 501 |
|
kaliszyk@35222 | 502 |
lemma bex_rsp: |
kaliszyk@35222 | 503 |
assumes a: "(R ===> (op =)) f g" |
kaliszyk@35222 | 504 |
shows "(Bex (Respects R) f = Bex (Respects R) g)" |
haftmann@40699 | 505 |
using a by (auto simp add: Bex_def in_respects elim: fun_relE) |
kaliszyk@35222 | 506 |
|
kaliszyk@35222 | 507 |
lemma bex1_rsp: |
kaliszyk@35222 | 508 |
assumes a: "(R ===> (op =)) f g" |
kaliszyk@35222 | 509 |
shows "Ex1 (\<lambda>x. x \<in> Respects R \<and> f x) = Ex1 (\<lambda>x. x \<in> Respects R \<and> g x)" |
haftmann@40699 | 510 |
using a by (auto elim: fun_relE simp add: Ex1_def in_respects) |
kaliszyk@35222 | 511 |
|
kaliszyk@35222 | 512 |
(* 2 lemmas needed for cleaning of quantifiers *) |
kaliszyk@35222 | 513 |
lemma all_prs: |
kaliszyk@35222 | 514 |
assumes a: "Quotient R absf repf" |
kaliszyk@35222 | 515 |
shows "Ball (Respects R) ((absf ---> id) f) = All f" |
haftmann@40850 | 516 |
using a unfolding Quotient_def Ball_def in_respects id_apply comp_def map_fun_def |
kaliszyk@35222 | 517 |
by metis |
kaliszyk@35222 | 518 |
|
kaliszyk@35222 | 519 |
lemma ex_prs: |
kaliszyk@35222 | 520 |
assumes a: "Quotient R absf repf" |
kaliszyk@35222 | 521 |
shows "Bex (Respects R) ((absf ---> id) f) = Ex f" |
haftmann@40850 | 522 |
using a unfolding Quotient_def Bex_def in_respects id_apply comp_def map_fun_def |
kaliszyk@35222 | 523 |
by metis |
kaliszyk@35222 | 524 |
|
huffman@35294 | 525 |
subsection {* @{text Bex1_rel} quantifier *} |
kaliszyk@35222 | 526 |
|
kaliszyk@35222 | 527 |
definition |
kaliszyk@35222 | 528 |
Bex1_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" |
kaliszyk@35222 | 529 |
where |
kaliszyk@35222 | 530 |
"Bex1_rel R P \<longleftrightarrow> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))" |
kaliszyk@35222 | 531 |
|
kaliszyk@35222 | 532 |
lemma bex1_rel_aux: |
kaliszyk@35222 | 533 |
"\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R x\<rbrakk> \<Longrightarrow> Bex1_rel R y" |
kaliszyk@35222 | 534 |
unfolding Bex1_rel_def |
kaliszyk@35222 | 535 |
apply (erule conjE)+ |
kaliszyk@35222 | 536 |
apply (erule bexE) |
kaliszyk@35222 | 537 |
apply rule |
kaliszyk@35222 | 538 |
apply (rule_tac x="xa" in bexI) |
kaliszyk@35222 | 539 |
apply metis |
kaliszyk@35222 | 540 |
apply metis |
kaliszyk@35222 | 541 |
apply rule+ |
kaliszyk@35222 | 542 |
apply (erule_tac x="xaa" in ballE) |
kaliszyk@35222 | 543 |
prefer 2 |
kaliszyk@35222 | 544 |
apply (metis) |
kaliszyk@35222 | 545 |
apply (erule_tac x="ya" in ballE) |
kaliszyk@35222 | 546 |
prefer 2 |
kaliszyk@35222 | 547 |
apply (metis) |
kaliszyk@35222 | 548 |
apply (metis in_respects) |
kaliszyk@35222 | 549 |
done |
kaliszyk@35222 | 550 |
|
kaliszyk@35222 | 551 |
lemma bex1_rel_aux2: |
kaliszyk@35222 | 552 |
"\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R y\<rbrakk> \<Longrightarrow> Bex1_rel R x" |
kaliszyk@35222 | 553 |
unfolding Bex1_rel_def |
kaliszyk@35222 | 554 |
apply (erule conjE)+ |
kaliszyk@35222 | 555 |
apply (erule bexE) |
kaliszyk@35222 | 556 |
apply rule |
kaliszyk@35222 | 557 |
apply (rule_tac x="xa" in bexI) |
kaliszyk@35222 | 558 |
apply metis |
kaliszyk@35222 | 559 |
apply metis |
kaliszyk@35222 | 560 |
apply rule+ |
kaliszyk@35222 | 561 |
apply (erule_tac x="xaa" in ballE) |
kaliszyk@35222 | 562 |
prefer 2 |
kaliszyk@35222 | 563 |
apply (metis) |
kaliszyk@35222 | 564 |
apply (erule_tac x="ya" in ballE) |
kaliszyk@35222 | 565 |
prefer 2 |
kaliszyk@35222 | 566 |
apply (metis) |
kaliszyk@35222 | 567 |
apply (metis in_respects) |
kaliszyk@35222 | 568 |
done |
kaliszyk@35222 | 569 |
|
kaliszyk@35222 | 570 |
lemma bex1_rel_rsp: |
kaliszyk@35222 | 571 |
assumes a: "Quotient R absf repf" |
kaliszyk@35222 | 572 |
shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)" |
haftmann@40699 | 573 |
apply (simp add: fun_rel_def) |
kaliszyk@35222 | 574 |
apply clarify |
kaliszyk@35222 | 575 |
apply rule |
kaliszyk@35222 | 576 |
apply (simp_all add: bex1_rel_aux bex1_rel_aux2) |
kaliszyk@35222 | 577 |
apply (erule bex1_rel_aux2) |
kaliszyk@35222 | 578 |
apply assumption |
kaliszyk@35222 | 579 |
done |
kaliszyk@35222 | 580 |
|
kaliszyk@35222 | 581 |
|
kaliszyk@35222 | 582 |
lemma ex1_prs: |
kaliszyk@35222 | 583 |
assumes a: "Quotient R absf repf" |
kaliszyk@35222 | 584 |
shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f" |
haftmann@40699 | 585 |
apply (simp add:) |
kaliszyk@35222 | 586 |
apply (subst Bex1_rel_def) |
kaliszyk@35222 | 587 |
apply (subst Bex_def) |
kaliszyk@35222 | 588 |
apply (subst Ex1_def) |
kaliszyk@35222 | 589 |
apply simp |
kaliszyk@35222 | 590 |
apply rule |
kaliszyk@35222 | 591 |
apply (erule conjE)+ |
kaliszyk@35222 | 592 |
apply (erule_tac exE) |
kaliszyk@35222 | 593 |
apply (erule conjE) |
kaliszyk@35222 | 594 |
apply (subgoal_tac "\<forall>y. R y y \<longrightarrow> f (absf y) \<longrightarrow> R x y") |
kaliszyk@35222 | 595 |
apply (rule_tac x="absf x" in exI) |
kaliszyk@35222 | 596 |
apply (simp) |
kaliszyk@35222 | 597 |
apply rule+ |
kaliszyk@35222 | 598 |
using a unfolding Quotient_def |
kaliszyk@35222 | 599 |
apply metis |
kaliszyk@35222 | 600 |
apply rule+ |
kaliszyk@35222 | 601 |
apply (erule_tac x="x" in ballE) |
kaliszyk@35222 | 602 |
apply (erule_tac x="y" in ballE) |
kaliszyk@35222 | 603 |
apply simp |
kaliszyk@35222 | 604 |
apply (simp add: in_respects) |
kaliszyk@35222 | 605 |
apply (simp add: in_respects) |
kaliszyk@35222 | 606 |
apply (erule_tac exE) |
kaliszyk@35222 | 607 |
apply rule |
kaliszyk@35222 | 608 |
apply (rule_tac x="repf x" in exI) |
kaliszyk@35222 | 609 |
apply (simp only: in_respects) |
kaliszyk@35222 | 610 |
apply rule |
kaliszyk@35222 | 611 |
apply (metis Quotient_rel_rep[OF a]) |
kaliszyk@35222 | 612 |
using a unfolding Quotient_def apply (simp) |
kaliszyk@35222 | 613 |
apply rule+ |
kaliszyk@35222 | 614 |
using a unfolding Quotient_def in_respects |
kaliszyk@35222 | 615 |
apply metis |
kaliszyk@35222 | 616 |
done |
kaliszyk@35222 | 617 |
|
kaliszyk@38941 | 618 |
lemma bex1_bexeq_reg: |
kaliszyk@38941 | 619 |
shows "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))" |
kaliszyk@35222 | 620 |
apply (simp add: Ex1_def Bex1_rel_def in_respects) |
kaliszyk@35222 | 621 |
apply clarify |
kaliszyk@35222 | 622 |
apply auto |
kaliszyk@35222 | 623 |
apply (rule bexI) |
kaliszyk@35222 | 624 |
apply assumption |
kaliszyk@35222 | 625 |
apply (simp add: in_respects) |
kaliszyk@35222 | 626 |
apply (simp add: in_respects) |
kaliszyk@35222 | 627 |
apply auto |
kaliszyk@35222 | 628 |
done |
kaliszyk@35222 | 629 |
|
kaliszyk@38941 | 630 |
lemma bex1_bexeq_reg_eqv: |
kaliszyk@38941 | 631 |
assumes a: "equivp R" |
kaliszyk@38941 | 632 |
shows "(\<exists>!x. P x) \<longrightarrow> Bex1_rel R P" |
kaliszyk@38941 | 633 |
using equivp_reflp[OF a] |
kaliszyk@38941 | 634 |
apply (intro impI) |
kaliszyk@38941 | 635 |
apply (elim ex1E) |
kaliszyk@38941 | 636 |
apply (rule mp[OF bex1_bexeq_reg]) |
kaliszyk@38941 | 637 |
apply (rule_tac a="x" in ex1I) |
kaliszyk@38941 | 638 |
apply (subst in_respects) |
kaliszyk@38941 | 639 |
apply (rule conjI) |
kaliszyk@38941 | 640 |
apply assumption |
kaliszyk@38941 | 641 |
apply assumption |
kaliszyk@38941 | 642 |
apply clarify |
kaliszyk@38941 | 643 |
apply (erule_tac x="xa" in allE) |
kaliszyk@38941 | 644 |
apply simp |
kaliszyk@38941 | 645 |
done |
kaliszyk@38941 | 646 |
|
huffman@35294 | 647 |
subsection {* Various respects and preserve lemmas *} |
kaliszyk@35222 | 648 |
|
kaliszyk@35222 | 649 |
lemma quot_rel_rsp: |
kaliszyk@35222 | 650 |
assumes a: "Quotient R Abs Rep" |
kaliszyk@35222 | 651 |
shows "(R ===> R ===> op =) R R" |
urbanc@38541 | 652 |
apply(rule fun_relI)+ |
kaliszyk@35222 | 653 |
apply(rule equals_rsp[OF a]) |
kaliszyk@35222 | 654 |
apply(assumption)+ |
kaliszyk@35222 | 655 |
done |
kaliszyk@35222 | 656 |
|
kaliszyk@35222 | 657 |
lemma o_prs: |
kaliszyk@35222 | 658 |
assumes q1: "Quotient R1 Abs1 Rep1" |
kaliszyk@35222 | 659 |
and q2: "Quotient R2 Abs2 Rep2" |
kaliszyk@35222 | 660 |
and q3: "Quotient R3 Abs3 Rep3" |
kaliszyk@36215 | 661 |
shows "((Abs2 ---> Rep3) ---> (Abs1 ---> Rep2) ---> (Rep1 ---> Abs3)) op \<circ> = op \<circ>" |
kaliszyk@36215 | 662 |
and "(id ---> (Abs1 ---> id) ---> Rep1 ---> id) op \<circ> = op \<circ>" |
kaliszyk@35222 | 663 |
using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3] |
haftmann@40699 | 664 |
by (simp_all add: fun_eq_iff) |
kaliszyk@35222 | 665 |
|
kaliszyk@35222 | 666 |
lemma o_rsp: |
kaliszyk@36215 | 667 |
"((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) op \<circ> op \<circ>" |
kaliszyk@36215 | 668 |
"(op = ===> (R1 ===> op =) ===> R1 ===> op =) op \<circ> op \<circ>" |
haftmann@40699 | 669 |
by (auto intro!: fun_relI elim: fun_relE) |
kaliszyk@35222 | 670 |
|
kaliszyk@35222 | 671 |
lemma cond_prs: |
kaliszyk@35222 | 672 |
assumes a: "Quotient R absf repf" |
kaliszyk@35222 | 673 |
shows "absf (if a then repf b else repf c) = (if a then b else c)" |
kaliszyk@35222 | 674 |
using a unfolding Quotient_def by auto |
kaliszyk@35222 | 675 |
|
kaliszyk@35222 | 676 |
lemma if_prs: |
kaliszyk@35222 | 677 |
assumes q: "Quotient R Abs Rep" |
kaliszyk@36123 | 678 |
shows "(id ---> Rep ---> Rep ---> Abs) If = If" |
kaliszyk@36123 | 679 |
using Quotient_abs_rep[OF q] |
nipkow@39535 | 680 |
by (auto simp add: fun_eq_iff) |
kaliszyk@35222 | 681 |
|
kaliszyk@35222 | 682 |
lemma if_rsp: |
kaliszyk@35222 | 683 |
assumes q: "Quotient R Abs Rep" |
kaliszyk@36123 | 684 |
shows "(op = ===> R ===> R ===> R) If If" |
haftmann@40699 | 685 |
by (auto intro!: fun_relI) |
kaliszyk@35222 | 686 |
|
kaliszyk@35222 | 687 |
lemma let_prs: |
kaliszyk@35222 | 688 |
assumes q1: "Quotient R1 Abs1 Rep1" |
kaliszyk@35222 | 689 |
and q2: "Quotient R2 Abs2 Rep2" |
kaliszyk@37033 | 690 |
shows "(Rep2 ---> (Abs2 ---> Rep1) ---> Abs1) Let = Let" |
kaliszyk@37033 | 691 |
using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] |
nipkow@39535 | 692 |
by (auto simp add: fun_eq_iff) |
kaliszyk@35222 | 693 |
|
kaliszyk@35222 | 694 |
lemma let_rsp: |
kaliszyk@37033 | 695 |
shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let" |
haftmann@40699 | 696 |
by (auto intro!: fun_relI elim: fun_relE) |
kaliszyk@35222 | 697 |
|
kaliszyk@39090 | 698 |
lemma mem_rsp: |
kaliszyk@39090 | 699 |
shows "(R1 ===> (R1 ===> R2) ===> R2) op \<in> op \<in>" |
haftmann@40699 | 700 |
by (auto intro!: fun_relI elim: fun_relE simp add: mem_def) |
kaliszyk@39090 | 701 |
|
kaliszyk@39090 | 702 |
lemma mem_prs: |
kaliszyk@39090 | 703 |
assumes a1: "Quotient R1 Abs1 Rep1" |
kaliszyk@39090 | 704 |
and a2: "Quotient R2 Abs2 Rep2" |
kaliszyk@39090 | 705 |
shows "(Rep1 ---> (Abs1 ---> Rep2) ---> Abs2) op \<in> = op \<in>" |
nipkow@39535 | 706 |
by (simp add: fun_eq_iff mem_def Quotient_abs_rep[OF a1] Quotient_abs_rep[OF a2]) |
kaliszyk@39090 | 707 |
|
kaliszyk@39893 | 708 |
lemma id_rsp: |
kaliszyk@39893 | 709 |
shows "(R ===> R) id id" |
haftmann@40699 | 710 |
by (auto intro: fun_relI) |
kaliszyk@39893 | 711 |
|
kaliszyk@39893 | 712 |
lemma id_prs: |
kaliszyk@39893 | 713 |
assumes a: "Quotient R Abs Rep" |
kaliszyk@39893 | 714 |
shows "(Rep ---> Abs) id = id" |
haftmann@40699 | 715 |
by (simp add: fun_eq_iff Quotient_abs_rep [OF a]) |
kaliszyk@39893 | 716 |
|
kaliszyk@39893 | 717 |
|
kaliszyk@35222 | 718 |
locale quot_type = |
kaliszyk@35222 | 719 |
fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
kaliszyk@35222 | 720 |
and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" |
kaliszyk@35222 | 721 |
and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" |
kaliszyk@37493 | 722 |
assumes equivp: "part_equivp R" |
kaliszyk@37493 | 723 |
and rep_prop: "\<And>y. \<exists>x. R x x \<and> Rep y = R x" |
kaliszyk@35222 | 724 |
and rep_inverse: "\<And>x. Abs (Rep x) = x" |
kaliszyk@37493 | 725 |
and abs_inverse: "\<And>c. (\<exists>x. ((R x x) \<and> (c = R x))) \<Longrightarrow> (Rep (Abs c)) = c" |
kaliszyk@35222 | 726 |
and rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)" |
kaliszyk@35222 | 727 |
begin |
kaliszyk@35222 | 728 |
|
kaliszyk@35222 | 729 |
definition |
haftmann@40699 | 730 |
abs :: "'a \<Rightarrow> 'b" |
kaliszyk@35222 | 731 |
where |
haftmann@40699 | 732 |
"abs x = Abs (R x)" |
kaliszyk@35222 | 733 |
|
kaliszyk@35222 | 734 |
definition |
haftmann@40699 | 735 |
rep :: "'b \<Rightarrow> 'a" |
kaliszyk@35222 | 736 |
where |
kaliszyk@35222 | 737 |
"rep a = Eps (Rep a)" |
kaliszyk@35222 | 738 |
|
kaliszyk@37493 | 739 |
lemma homeier5: |
kaliszyk@37493 | 740 |
assumes a: "R r r" |
kaliszyk@37493 | 741 |
shows "Rep (Abs (R r)) = R r" |
kaliszyk@37493 | 742 |
apply (subst abs_inverse) |
kaliszyk@37493 | 743 |
using a by auto |
kaliszyk@35222 | 744 |
|
kaliszyk@37493 | 745 |
theorem homeier6: |
kaliszyk@37493 | 746 |
assumes a: "R r r" |
kaliszyk@37493 | 747 |
and b: "R s s" |
kaliszyk@37493 | 748 |
shows "Abs (R r) = Abs (R s) \<longleftrightarrow> R r = R s" |
kaliszyk@37493 | 749 |
by (metis a b homeier5) |
kaliszyk@35222 | 750 |
|
kaliszyk@37493 | 751 |
theorem homeier8: |
kaliszyk@37493 | 752 |
assumes "R r r" |
kaliszyk@37493 | 753 |
shows "R (Eps (R r)) = R r" |
kaliszyk@37493 | 754 |
using assms equivp[simplified part_equivp_def] |
kaliszyk@37493 | 755 |
apply clarify |
kaliszyk@37493 | 756 |
by (metis assms exE_some) |
kaliszyk@35222 | 757 |
|
kaliszyk@35222 | 758 |
lemma Quotient: |
kaliszyk@35222 | 759 |
shows "Quotient R abs rep" |
kaliszyk@37493 | 760 |
unfolding Quotient_def abs_def rep_def |
kaliszyk@37493 | 761 |
proof (intro conjI allI) |
kaliszyk@37493 | 762 |
fix a r s |
kaliszyk@37493 | 763 |
show "Abs (R (Eps (Rep a))) = a" |
kaliszyk@37493 | 764 |
by (metis equivp exE_some part_equivp_def rep_inverse rep_prop) |
kaliszyk@37493 | 765 |
show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (R r) = Abs (R s))" |
kaliszyk@37493 | 766 |
by (metis homeier6 equivp[simplified part_equivp_def]) |
kaliszyk@37493 | 767 |
show "R (Eps (Rep a)) (Eps (Rep a))" proof - |
kaliszyk@37493 | 768 |
obtain x where r: "R x x" and rep: "Rep a = R x" using rep_prop[of a] by auto |
kaliszyk@37493 | 769 |
have "R (Eps (R x)) x" using homeier8 r by simp |
kaliszyk@37493 | 770 |
then have "R x (Eps (R x))" using part_equivp_symp[OF equivp] by fast |
kaliszyk@37493 | 771 |
then have "R (Eps (R x)) (Eps (R x))" using homeier8[OF r] by simp |
kaliszyk@37493 | 772 |
then show "R (Eps (Rep a)) (Eps (Rep a))" using rep by simp |
kaliszyk@37493 | 773 |
qed |
kaliszyk@37493 | 774 |
qed |
kaliszyk@35222 | 775 |
|
kaliszyk@35222 | 776 |
end |
kaliszyk@35222 | 777 |
|
kaliszyk@37493 | 778 |
|
huffman@35294 | 779 |
subsection {* ML setup *} |
kaliszyk@35222 | 780 |
|
kaliszyk@35222 | 781 |
text {* Auxiliary data for the quotient package *} |
kaliszyk@35222 | 782 |
|
wenzelm@38275 | 783 |
use "Tools/Quotient/quotient_info.ML" |
kaliszyk@35222 | 784 |
|
haftmann@40850 | 785 |
declare [[map "fun" = (map_fun, fun_rel)]] |
kaliszyk@35222 | 786 |
|
kaliszyk@35222 | 787 |
lemmas [quot_thm] = fun_quotient |
kaliszyk@39893 | 788 |
lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp mem_rsp id_rsp |
kaliszyk@39893 | 789 |
lemmas [quot_preserve] = if_prs o_prs let_prs mem_prs id_prs |
kaliszyk@35222 | 790 |
lemmas [quot_equiv] = identity_equivp |
kaliszyk@35222 | 791 |
|
kaliszyk@35222 | 792 |
|
kaliszyk@35222 | 793 |
text {* Lemmas about simplifying id's. *} |
kaliszyk@35222 | 794 |
lemmas [id_simps] = |
kaliszyk@35222 | 795 |
id_def[symmetric] |
haftmann@40850 | 796 |
map_fun_id |
kaliszyk@35222 | 797 |
id_apply |
kaliszyk@35222 | 798 |
id_o |
kaliszyk@35222 | 799 |
o_id |
kaliszyk@35222 | 800 |
eq_comp_r |
kaliszyk@35222 | 801 |
|
kaliszyk@35222 | 802 |
text {* Translation functions for the lifting process. *} |
wenzelm@38275 | 803 |
use "Tools/Quotient/quotient_term.ML" |
kaliszyk@35222 | 804 |
|
kaliszyk@35222 | 805 |
|
kaliszyk@35222 | 806 |
text {* Definitions of the quotient types. *} |
wenzelm@38275 | 807 |
use "Tools/Quotient/quotient_typ.ML" |
kaliszyk@35222 | 808 |
|
kaliszyk@35222 | 809 |
|
kaliszyk@35222 | 810 |
text {* Definitions for quotient constants. *} |
wenzelm@38275 | 811 |
use "Tools/Quotient/quotient_def.ML" |
kaliszyk@35222 | 812 |
|
kaliszyk@35222 | 813 |
|
kaliszyk@35222 | 814 |
text {* |
kaliszyk@35222 | 815 |
An auxiliary constant for recording some information |
kaliszyk@35222 | 816 |
about the lifted theorem in a tactic. |
kaliszyk@35222 | 817 |
*} |
kaliszyk@35222 | 818 |
definition |
haftmann@40699 | 819 |
Quot_True :: "'a \<Rightarrow> bool" |
haftmann@40699 | 820 |
where |
haftmann@40699 | 821 |
"Quot_True x \<longleftrightarrow> True" |
kaliszyk@35222 | 822 |
|
kaliszyk@35222 | 823 |
lemma |
kaliszyk@35222 | 824 |
shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P" |
kaliszyk@35222 | 825 |
and QT_ex: "Quot_True (Ex P) \<Longrightarrow> Quot_True P" |
kaliszyk@35222 | 826 |
and QT_ex1: "Quot_True (Ex1 P) \<Longrightarrow> Quot_True P" |
kaliszyk@35222 | 827 |
and QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True (P x))" |
kaliszyk@35222 | 828 |
and QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)" |
kaliszyk@35222 | 829 |
by (simp_all add: Quot_True_def ext) |
kaliszyk@35222 | 830 |
|
kaliszyk@35222 | 831 |
lemma QT_imp: "Quot_True a \<equiv> Quot_True b" |
kaliszyk@35222 | 832 |
by (simp add: Quot_True_def) |
kaliszyk@35222 | 833 |
|
kaliszyk@35222 | 834 |
|
kaliszyk@35222 | 835 |
text {* Tactics for proving the lifted theorems *} |
wenzelm@38275 | 836 |
use "Tools/Quotient/quotient_tacs.ML" |
kaliszyk@35222 | 837 |
|
huffman@35294 | 838 |
subsection {* Methods / Interface *} |
kaliszyk@35222 | 839 |
|
kaliszyk@35222 | 840 |
method_setup lifting = |
urbanc@37593 | 841 |
{* Attrib.thms >> (fn thms => fn ctxt => |
urbanc@39088 | 842 |
SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt [] thms))) *} |
kaliszyk@35222 | 843 |
{* lifts theorems to quotient types *} |
kaliszyk@35222 | 844 |
|
kaliszyk@35222 | 845 |
method_setup lifting_setup = |
urbanc@37593 | 846 |
{* Attrib.thm >> (fn thm => fn ctxt => |
urbanc@39088 | 847 |
SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_procedure_tac ctxt [] thm))) *} |
kaliszyk@35222 | 848 |
{* sets up the three goals for the quotient lifting procedure *} |
kaliszyk@35222 | 849 |
|
urbanc@37593 | 850 |
method_setup descending = |
urbanc@39088 | 851 |
{* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_tac ctxt []))) *} |
urbanc@37593 | 852 |
{* decends theorems to the raw level *} |
urbanc@37593 | 853 |
|
urbanc@37593 | 854 |
method_setup descending_setup = |
urbanc@39088 | 855 |
{* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_procedure_tac ctxt []))) *} |
urbanc@37593 | 856 |
{* sets up the three goals for the decending theorems *} |
urbanc@37593 | 857 |
|
kaliszyk@35222 | 858 |
method_setup regularize = |
kaliszyk@35222 | 859 |
{* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.regularize_tac ctxt))) *} |
kaliszyk@35222 | 860 |
{* proves the regularization goals from the quotient lifting procedure *} |
kaliszyk@35222 | 861 |
|
kaliszyk@35222 | 862 |
method_setup injection = |
kaliszyk@35222 | 863 |
{* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.all_injection_tac ctxt))) *} |
kaliszyk@35222 | 864 |
{* proves the rep/abs injection goals from the quotient lifting procedure *} |
kaliszyk@35222 | 865 |
|
kaliszyk@35222 | 866 |
method_setup cleaning = |
kaliszyk@35222 | 867 |
{* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.clean_tac ctxt))) *} |
kaliszyk@35222 | 868 |
{* proves the cleaning goals from the quotient lifting procedure *} |
kaliszyk@35222 | 869 |
|
kaliszyk@35222 | 870 |
attribute_setup quot_lifted = |
kaliszyk@35222 | 871 |
{* Scan.succeed Quotient_Tacs.lifted_attrib *} |
kaliszyk@35222 | 872 |
{* lifts theorems to quotient types *} |
kaliszyk@35222 | 873 |
|
kaliszyk@35222 | 874 |
no_notation |
kaliszyk@35222 | 875 |
rel_conj (infixr "OOO" 75) and |
haftmann@40850 | 876 |
map_fun (infixr "--->" 55) and |
kaliszyk@35222 | 877 |
fun_rel (infixr "===>" 55) |
kaliszyk@35222 | 878 |
|
kaliszyk@35222 | 879 |
end |