0
+ − 1 theory Quotients
+ − 2 imports Main
+ − 3 begin
+ − 4
+ − 5 definition
+ − 6 "REFL E \<equiv> \<forall>x. E x x"
+ − 7
+ − 8 definition
+ − 9 "SYM E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x"
+ − 10
+ − 11 definition
+ − 12 "TRANS E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z"
+ − 13
+ − 14 definition
+ − 15 "NONEMPTY E \<equiv> \<exists>x. E x x"
+ − 16
+ − 17 definition
+ − 18 "EQUIV E \<equiv> REFL E \<and> SYM E \<and> TRANS E"
+ − 19
+ − 20 definition
+ − 21 "EQUIV_PROP E \<equiv> (\<forall>x y. E x y = (E x = E y))"
+ − 22
+ − 23 lemma EQUIV_PROP_EQUALITY:
+ − 24 shows "EQUIV_PROP (op =)"
+ − 25 unfolding EQUIV_PROP_def expand_fun_eq
+ − 26 by (blast)
+ − 27
+ − 28 lemma EQUIV_implies_EQUIV_PROP:
+ − 29 assumes a: "REFL E"
+ − 30 and b: "SYM E"
+ − 31 and c: "TRANS E"
+ − 32 shows "EQUIV_PROP E"
+ − 33 using a b c
+ − 34 unfolding EQUIV_PROP_def REFL_def SYM_def TRANS_def expand_fun_eq
+ − 35 by (metis)
+ − 36
+ − 37 lemma EQUIV_PROP_implies_REFL:
+ − 38 assumes a: "EQUIV_PROP E"
+ − 39 shows "REFL E"
+ − 40 using a
+ − 41 unfolding EQUIV_PROP_def REFL_def expand_fun_eq
+ − 42 by (metis)
+ − 43
+ − 44 lemma EQUIV_PROP_implies_SYM:
+ − 45 assumes a: "EQUIV_PROP E"
+ − 46 shows "SYM E"
+ − 47 using a
+ − 48 unfolding EQUIV_PROP_def SYM_def expand_fun_eq
+ − 49 by (metis)
+ − 50
+ − 51 lemma EQUIV_PROP_implies_TRANS:
+ − 52 assumes a: "EQUIV_PROP E"
+ − 53 shows "TRANS E"
+ − 54 using a
+ − 55 unfolding EQUIV_PROP_def TRANS_def expand_fun_eq
+ − 56 by (blast)
+ − 57
+ − 58 ML {*
+ − 59 fun equiv_refl thm = thm RS @{thm EQUIV_PROP_implies_REFL}
+ − 60 fun equiv_sym thm = thm RS @{thm EQUIV_PROP_implies_SYM}
+ − 61 fun equiv_trans thm = thm RS @{thm EQUIV_PROP_implies_TRANS}
+ − 62
+ − 63 fun refl_sym_trans_equiv thm1 thm2 thm3 = [thm1,thm2,thm3] MRS @{thm EQUIV_implies_EQUIV_PROP}
+ − 64 *}
+ − 65
+ − 66
+ − 67 fun
+ − 68 LIST_REL
+ − 69 where
+ − 70 "LIST_REL R [] [] = True"
+ − 71 | "LIST_REL R (x#xs) [] = False"
+ − 72 | "LIST_REL R [] (x#xs) = False"
+ − 73 | "LIST_REL R (x#xs) (y#ys) = (R x y \<and> LIST_REL R xs ys)"
+ − 74
+ − 75 fun
+ − 76 OPTION_REL
+ − 77 where
+ − 78 "OPTION_REL R None None = True"
+ − 79 | "OPTION_REL R (Some x) None = False"
+ − 80 | "OPTION_REL R None (Some x) = False"
+ − 81 | "OPTION_REL R (Some x) (Some y) = R x y"
+ − 82
+ − 83 fun
+ − 84 option_map
+ − 85 where
+ − 86 "option_map f None = None"
+ − 87 | "option_map f (Some x) = Some (f x)"
+ − 88
+ − 89 fun
+ − 90 PROD_REL
+ − 91 where
+ − 92 "PROD_REL R1 R2 (a1,a2) (b1,b2) = (R1 a1 b1 \<and> R2 a2 b2)"
+ − 93
+ − 94 fun
+ − 95 prod_map
+ − 96 where
+ − 97 "prod_map f1 f2 (a,b) = (f1 a, f2 b)"
+ − 98
+ − 99 fun
+ − 100 SUM_REL
+ − 101 where
+ − 102 "SUM_REL R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
+ − 103 | "SUM_REL R1 R2 (Inl a1) (Inr b2) = False"
+ − 104 | "SUM_REL R1 R2 (Inr a2) (Inl b1) = False"
+ − 105 | "SUM_REL R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
+ − 106
+ − 107 fun
+ − 108 sum_map
+ − 109 where
+ − 110 "sum_map f1 f2 (Inl a) = Inl (f1 a)"
+ − 111 | "sum_map f1 f2 (Inr a) = Inr (f2 a)"
+ − 112
+ − 113 fun
+ − 114 FUN_REL
+ − 115 where
+ − 116 "FUN_REL R1 R2 f g = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
+ − 117
+ − 118 fun
+ − 119 fun_map
+ − 120 where
+ − 121 "fun_map f g h x = g (h (f x))"
+ − 122
+ − 123 definition
+ − 124 "QUOTIENT_ABS_REP Abs Rep \<equiv> (\<forall>a. Abs (Rep a) = a)"
+ − 125
+ − 126
+ − 127
+ − 128 definition
+ − 129 "QUOTIENT R Abs Rep \<equiv> (\<forall>a. Abs (Rep a) = a) \<and>
+ − 130 (\<forall>a. R (Rep a) (Rep a)) \<and>
+ − 131 (\<forall>r s. R r s = (R r r \<and> R s s \<and> (Abs r = Abs s)))"
+ − 132
+ − 133 lemma QUOTIENT_ID:
+ − 134 shows "QUOTIENT (op =) id id"
+ − 135 unfolding QUOTIENT_def id_def
+ − 136 by (blast)
+ − 137
+ − 138 lemma QUOTIENT_PROD:
+ − 139 assumes a: "QUOTIENT E1 Abs1 Rep1"
+ − 140 and b: "QUOTIENT E2 Abs2 Rep2"
3
+ − 141 shows "QUOTIENT (PROD_REL E1 E2) (prod_map Abs1 Abs2) (prod_map Rep1 Rep2)"
0
+ − 142 using a b unfolding QUOTIENT_def
+ − 143 oops
+ − 144
+ − 145 lemma QUOTIENT_ABS_REP_LIST:
+ − 146 assumes a: "QUOTIENT_ABS_REP Abs Rep"
+ − 147 shows "QUOTIENT_ABS_REP (map Abs) (map Rep)"
+ − 148 using a
+ − 149 unfolding QUOTIENT_ABS_REP_def
+ − 150 apply(rule_tac allI)
+ − 151 apply(induct_tac a rule: list.induct)
+ − 152 apply(auto)
+ − 153 done
+ − 154
+ − 155 definition
+ − 156 eqclass ("[_]_")
+ − 157 where
+ − 158 "[x]E \<equiv> E x"
+ − 159
+ − 160 definition
+ − 161 QUOTIENT_SET :: "'a set \<Rightarrow> ('a \<Rightarrow>'a\<Rightarrow>bool) \<Rightarrow> ('a set) set" ("_'/#'/_")
+ − 162 where
+ − 163 "S/#/E = {[x]E | x. x\<in>S}"
+ − 164
+ − 165 definition
+ − 166 QUOTIENT_UNIV
+ − 167 where
+ − 168 "QUOTIENT_UNIV TYPE('a) E \<equiv> (UNIV::'a set)/#/E"
+ − 169
+ − 170 consts MY::"'a\<Rightarrow>'a\<Rightarrow>bool"
+ − 171 axioms my1: "REFL MY"
+ − 172 axioms my2: "SYM MY"
+ − 173 axioms my3: "TRANS MY"
+ − 174
+ − 175 term "QUOTIENT_UNIV TYPE('a) MY"
+ − 176 term "\<lambda>f. \<exists>x. f = [x]MY"
+ − 177
+ − 178 typedef 'a quot = "\<lambda>f::'a\<Rightarrow>bool. \<exists>x. f = [x]MY"
+ − 179 by (auto simp add: mem_def)
+ − 180
+ − 181 thm Abs_quot_inverse Rep_quot_inverse Abs_quot_inject Rep_quot_inject Rep_quot
+ − 182 thm Abs_quot_cases Rep_quot_cases Abs_quot_induct Rep_quot_induct
+ − 183
+ − 184 lemma lem2:
+ − 185 shows "([x]MY = [y]MY) = MY x y"
+ − 186 apply(rule iffI)
+ − 187 apply(simp add: eqclass_def)
+ − 188 using my1
+ − 189 apply(auto simp add: REFL_def)[1]
+ − 190 apply(simp add: eqclass_def expand_fun_eq)
+ − 191 apply(rule allI)
+ − 192 apply(rule iffI)
+ − 193 apply(subgoal_tac "MY y x")
+ − 194 using my3
+ − 195 apply(simp add: TRANS_def)[1]
+ − 196 apply(drule_tac x="y" in spec)
+ − 197 apply(drule_tac x="x" in spec)
+ − 198 apply(drule_tac x="xa" in spec)
+ − 199 apply(simp)
+ − 200 using my2
+ − 201 apply(simp add: SYM_def)[1]
+ − 202 oops
+ − 203
+ − 204 lemma lem6:
+ − 205 "\<forall>a. \<exists>r. Rep_quot a = [r]MY"
+ − 206 apply(rule allI)
+ − 207 apply(subgoal_tac "Rep_quot a \<in> quot")
+ − 208 apply(simp add: quot_def mem_def)
+ − 209 apply(rule Rep_quot)
+ − 210 done
+ − 211
+ − 212 lemma lem7:
+ − 213 "\<forall>x y. (Abs_quot ([x]MY) = Abs_quot ([y]MY)) = ([x]MY = [y]MY)"
+ − 214 apply(subst Abs_quot_inject)
+ − 215 apply(unfold quot_def mem_def)
+ − 216 apply(auto)
+ − 217 done
+ − 218
+ − 219 definition
+ − 220 "Abs x = Abs_quot ([x]MY)"
+ − 221
+ − 222 definition
+ − 223 "Rep a = Eps (Rep_quot a)"
+ − 224
+ − 225 lemma lem9:
+ − 226 "\<forall>r. [(Eps [r]MY)]MY = [r]MY"
+ − 227 apply(rule allI)
+ − 228 apply(subgoal_tac "MY r r \<Longrightarrow> MY r (Eps (MY r))")
+ − 229 apply(drule meta_mp)
+ − 230 apply(rule eq1[THEN spec])
+ − 231
+ − 232
+ − 233 apply(rule_tac x="MY r" in someI)
+ − 234
+ − 235 lemma
+ − 236 "(f \<in> UNIV/#/MY) = (Rep_quot (Abs_quot f) = f)"
+ − 237 apply(simp add: QUOTIENT_SET_def)
+ − 238 apply(auto)
+ − 239 apply(subgoal_tac "[x]MY \<in> quot")
+ − 240 apply(simp add: Abs_quot_inverse)
+ − 241 apply(simp add: quot_def)
+ − 242 apply(simp add: QUOTIENT_UNIV_def QUOTIENT_SET_def)
+ − 243 apply(auto)[1]
+ − 244 apply(subgoal_tac "[x]MY \<in> quot")
+ − 245 apply(simp add: Abs_quot_inverse)
+ − 246 apply(simp add: quot_def)
+ − 247 apply(simp add: QUOTIENT_UNIV_def QUOTIENT_SET_def)
+ − 248 apply(auto)[1]
+ − 249 apply(subst expand_set_eq)
+ − 250 thm Abs_quot_inverse Rep_quot_inverse Abs_quot_inject Rep_quot_inject Rep_quot
+ − 251
+ − 252 lemma
+ − 253 "\<forall>a. \<exists>r. Rep_quot a = [r]MY"
+ − 254 apply(rule allI)
+ − 255 apply(subst Abs_quot_inject[symmetric])
+ − 256 apply(rule Rep_quot)
+ − 257 apply(simp add: quot_def)
+ − 258 apply(simp add: QUOTIENT_UNIV_def QUOTIENT_SET_def)
+ − 259 apply(auto)[1]
+ − 260 apply(simp add: Rep_quot_inverse)
+ − 261 thm Abs_quot_inverse Rep_quot_inverse Abs_quot_inject Rep_quot_inject Rep_quot
+ − 262 apply(subst Abs_quot_inject[symmetric])
+ − 263 proof -
+ − 264 have "[r]MY \<in> quot"
+ − 265 apply(simp add: quot_def)
+ − 266 apply(simp add: QUOTIENT_UNIV_def QUOTIENT_SET_def)
+ − 267 apply(auto)
+ − 268
+ − 269 thm Abs_quot_inverse
+ − 270
+ − 271
+ − 272 thm Abs_quot_inverse
+ − 273 apply(simp add: Rep_quot_inverse)
+ − 274
+ − 275
+ − 276 thm Rep_quot_inverse
+ − 277
+ − 278 term ""
+ − 279
+ − 280 lemma
+ − 281 assumes a: "EQUIV2 E"
+ − 282 shows "([x]E = [y]E) = E x y"
+ − 283 using a
+ − 284 by (simp add: eqclass_def EQUIV2_def)
+ − 285
+ − 286
+ − 287
+ − 288
+ − 289
+ − 290 lemma
+ − 291 shows "QUOTIENT (op =) (\<lambda>x. x) (\<lambda>x. x)"
+ − 292 apply(unfold QUOTIENT_def)
+ − 293 apply(blast)
+ − 294 done
+ − 295
+ − 296 definition
+ − 297 fun_app ("_ ---> _")
+ − 298 where
+ − 299 "f ---> g \<equiv> \<lambda>h x. g (h (f x))"
+ − 300
+ − 301 lemma helper:
+ − 302 assumes q: "QUOTIENT R ab re"
+ − 303 and a: "R z z"
+ − 304 shows "R (re (ab z)) z"
+ − 305 using q a
+ − 306 apply(unfold QUOTIENT_def)[1]
+ − 307 apply(blast)
+ − 308 done
+ − 309
+ − 310
+ − 311 lemma
+ − 312 assumes q1: "QUOTIENT R1 abs1 rep1"
+ − 313 and q2: "QUOTIENT R2 abs2 rep2"
+ − 314 shows "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
+ − 315 proof -
+ − 316 have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
+ − 317 apply(simp add: expand_fun_eq)
+ − 318 apply(simp add: fun_app_def)
+ − 319 using q1 q2
+ − 320 apply(simp add: QUOTIENT_def)
+ − 321 done
+ − 322 moreover
+ − 323 have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
+ − 324 apply(simp add: FUN_REL_def)
+ − 325 apply(auto)
+ − 326 apply(simp add: fun_app_def)
+ − 327 using q1 q2
+ − 328 apply(unfold QUOTIENT_def)
+ − 329 apply(metis)
+ − 330 done
+ − 331 moreover
+ − 332 have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
+ − 333 (rep1 ---> abs2) r = (rep1 ---> abs2) s)"
+ − 334 apply(simp add: expand_fun_eq)
+ − 335 apply(rule allI)+
+ − 336 apply(rule iffI)
+ − 337 using q1 q2
+ − 338 apply(unfold QUOTIENT_def)[1]
+ − 339 apply(unfold fun_app_def)[1]
+ − 340 apply(unfold FUN_REL_def)[1]
+ − 341 apply(rule conjI)
+ − 342 apply(metis)
+ − 343 apply(rule conjI)
+ − 344 apply(metis)
+ − 345 apply(metis)
+ − 346 apply(erule conjE)
+ − 347 apply(simp (no_asm) add: FUN_REL_def)
+ − 348 apply(rule allI impI)+
+ − 349 apply(subgoal_tac "R1 x x \<and> R1 y y \<and> abs1 x = abs1 y")(*A*)
+ − 350 using q2
+ − 351 apply(unfold QUOTIENT_def)[1]
+ − 352 apply(unfold fun_app_def)[1]
+ − 353 apply(unfold FUN_REL_def)[1]
+ − 354 apply(subgoal_tac "R2 (r x) (r x)")(*B*)
+ − 355 apply(subgoal_tac "R2 (s y) (s y)")(*C*)
+ − 356 apply(subgoal_tac "abs2 (r x) = abs2 (s y)")(*D*)
+ − 357 apply(blast)
+ − 358 (*D*)
+ − 359 apply(metis helper q1)
+ − 360 (*C*)
+ − 361 apply(blast)
+ − 362 (*B*)
+ − 363 apply(blast)
+ − 364 (*A*)
+ − 365 using q1
+ − 366 apply(unfold QUOTIENT_def)[1]
+ − 367 apply(unfold fun_app_def)[1]
+ − 368 apply(unfold FUN_REL_def)[1]
+ − 369 apply(metis)
+ − 370 done
+ − 371 ultimately
+ − 372 show "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
+ − 373 apply(unfold QUOTIENT_def)[1]
+ − 374 apply(blast)
+ − 375 done
+ − 376 qed
+ − 377
+ − 378
+ − 379
+ − 380
+ − 381
+ − 382
+ − 383
+ − 384 definition
+ − 385 "USER R \<equiv> NONEMPTY R \<and>
+ − 386
+ − 387
+ − 388
+ − 389 typedecl tau
+ − 390 consts R::"tau \<Rightarrow> tau \<Rightarrow> bool"
+ − 391
+ − 392
+ − 393
+ − 394 definition
+ − 395 FACTOR :: "'a set \<Rightarrow> ('a \<times>'a \<Rightarrow> bool) \<Rightarrow> ('a set) set" ("_ '/'/'/ _")
+ − 396 where
+ − 397 "A /// r \<equiv> \<Union>x\<in>A. {r``{x}}"
+ − 398
+ − 399 typedef qtau = "\<lambda>c::tau\<Rightarrow>bool. (\<exists>x. R x x \<and> (c = R x))"
+ − 400 apply(rule exI)
+ − 401
+ − 402 apply(rule_tac x="R x" in exI)
+ − 403 apply(auto)
+ − 404
+ − 405 definition
+ − 406 "QUOT TYPE('a) R \<equiv> \<lambda>c::'a\<Rightarrow>bool. (\<exists>x. R x x \<and> (c = R x))"
+ − 407
+ − 408
+ − 409
+ − 410
+ − 411
+ − 412