1148
+ − 1
(* Title: Quotient.thy
759
+ − 2
Author: Cezary Kaliszyk and Christian Urban
+ − 3
*)
+ − 4
1128
+ − 5
theory Quotient
1127
+ − 6
imports Plain ATP_Linkup
1122
+ − 7
uses
+ − 8
("quotient_info.ML")
+ − 9
("quotient_typ.ML")
+ − 10
("quotient_def.ML")
+ − 11
("quotient_term.ML")
+ − 12
("quotient_tacs.ML")
597
+ − 13
begin
+ − 14
1137
36d596cb63a2
moved "strange" lemma to quotient_tacs; marked a number of lemmas as unused; tuned
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 15
1127
+ − 16
text {*
+ − 17
Basic definition for equivalence relations
+ − 18
that are represented by predicates.
+ − 19
*}
+ − 20
+ − 21
definition
1137
36d596cb63a2
moved "strange" lemma to quotient_tacs; marked a number of lemmas as unused; tuned
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 22
"equivp E \<equiv> \<forall>x y. E x y = (E x = E y)"
1127
+ − 23
+ − 24
definition
1137
36d596cb63a2
moved "strange" lemma to quotient_tacs; marked a number of lemmas as unused; tuned
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 25
"reflp E \<equiv> \<forall>x. E x x"
1127
+ − 26
+ − 27
definition
1137
36d596cb63a2
moved "strange" lemma to quotient_tacs; marked a number of lemmas as unused; tuned
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 28
"symp E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x"
1127
+ − 29
+ − 30
definition
1137
36d596cb63a2
moved "strange" lemma to quotient_tacs; marked a number of lemmas as unused; tuned
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 31
"transp E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z"
1127
+ − 32
+ − 33
lemma equivp_reflp_symp_transp:
+ − 34
shows "equivp E = (reflp E \<and> symp E \<and> transp E)"
+ − 35
unfolding equivp_def reflp_def symp_def transp_def expand_fun_eq
+ − 36
by blast
+ − 37
+ − 38
lemma equivp_reflp:
+ − 39
shows "equivp E \<Longrightarrow> E x x"
+ − 40
by (simp only: equivp_reflp_symp_transp reflp_def)
+ − 41
+ − 42
lemma equivp_symp:
+ − 43
shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y x"
+ − 44
by (metis equivp_reflp_symp_transp symp_def)
+ − 45
+ − 46
lemma equivp_transp:
+ − 47
shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y z \<Longrightarrow> E x z"
+ − 48
by (metis equivp_reflp_symp_transp transp_def)
+ − 49
+ − 50
lemma equivpI:
+ − 51
assumes "reflp R" "symp R" "transp R"
+ − 52
shows "equivp R"
+ − 53
using assms by (simp add: equivp_reflp_symp_transp)
+ − 54
+ − 55
lemma identity_equivp:
+ − 56
shows "equivp (op =)"
+ − 57
unfolding equivp_def
+ − 58
by auto
+ − 59
1137
36d596cb63a2
moved "strange" lemma to quotient_tacs; marked a number of lemmas as unused; tuned
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 60
text {* Partial equivalences: not yet used anywhere *}
1127
+ − 61
+ − 62
definition
1137
36d596cb63a2
moved "strange" lemma to quotient_tacs; marked a number of lemmas as unused; tuned
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 63
"part_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))"
1127
+ − 64
+ − 65
lemma equivp_implies_part_equivp:
+ − 66
assumes a: "equivp E"
+ − 67
shows "part_equivp E"
1128
+ − 68
using a
1127
+ − 69
unfolding equivp_def part_equivp_def
+ − 70
by auto
+ − 71
+ − 72
text {* Composition of Relations *}
+ − 73
1128
+ − 74
abbreviation
1127
+ − 75
rel_conj (infixr "OOO" 75)
+ − 76
where
+ − 77
"r1 OOO r2 \<equiv> r1 OO r2 OO r1"
+ − 78
1128
+ − 79
lemma eq_comp_r:
1127
+ − 80
shows "((op =) OOO R) = R"
+ − 81
by (auto simp add: expand_fun_eq)
+ − 82
+ − 83
section {* Respects predicate *}
+ − 84
+ − 85
definition
+ − 86
Respects
+ − 87
where
1137
36d596cb63a2
moved "strange" lemma to quotient_tacs; marked a number of lemmas as unused; tuned
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 88
"Respects R x \<equiv> R x x"
1127
+ − 89
+ − 90
lemma in_respects:
+ − 91
shows "(x \<in> Respects R) = R x x"
1128
+ − 92
unfolding mem_def Respects_def
1127
+ − 93
by simp
+ − 94
+ − 95
section {* Function map and function relation *}
+ − 96
+ − 97
definition
+ − 98
fun_map (infixr "--->" 55)
+ − 99
where
+ − 100
[simp]: "fun_map f g h x = g (h (f x))"
+ − 101
+ − 102
definition
+ − 103
fun_rel (infixr "===>" 55)
+ − 104
where
+ − 105
[simp]: "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
+ − 106
+ − 107
+ − 108
lemma fun_map_id:
+ − 109
shows "(id ---> id) = id"
+ − 110
by (simp add: expand_fun_eq id_def)
+ − 111
+ − 112
lemma fun_rel_eq:
+ − 113
shows "((op =) ===> (op =)) = (op =)"
+ − 114
by (simp add: expand_fun_eq)
+ − 115
+ − 116
lemma fun_rel_id:
+ − 117
assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
+ − 118
shows "(R1 ===> R2) f g"
+ − 119
using a by simp
+ − 120
+ − 121
lemma fun_rel_id_asm:
+ − 122
assumes a: "\<And>x y. R1 x y \<Longrightarrow> (A \<longrightarrow> R2 (f x) (g y))"
+ − 123
shows "A \<longrightarrow> (R1 ===> R2) f g"
+ − 124
using a by auto
+ − 125
+ − 126
+ − 127
section {* Quotient Predicate *}
+ − 128
+ − 129
definition
1137
36d596cb63a2
moved "strange" lemma to quotient_tacs; marked a number of lemmas as unused; tuned
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 130
"Quotient E Abs Rep \<equiv>
1127
+ − 131
(\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. E (Rep a) (Rep a)) \<and>
+ − 132
(\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"
+ − 133
+ − 134
lemma Quotient_abs_rep:
+ − 135
assumes a: "Quotient E Abs Rep"
+ − 136
shows "Abs (Rep a) = a"
1128
+ − 137
using a
1127
+ − 138
unfolding Quotient_def
+ − 139
by simp
+ − 140
+ − 141
lemma Quotient_rep_reflp:
+ − 142
assumes a: "Quotient E Abs Rep"
+ − 143
shows "E (Rep a) (Rep a)"
1128
+ − 144
using a
1127
+ − 145
unfolding Quotient_def
+ − 146
by blast
+ − 147
+ − 148
lemma Quotient_rel:
+ − 149
assumes a: "Quotient E Abs Rep"
+ − 150
shows " E r s = (E r r \<and> E s s \<and> (Abs r = Abs s))"
1128
+ − 151
using a
1127
+ − 152
unfolding Quotient_def
+ − 153
by blast
+ − 154
+ − 155
lemma Quotient_rel_rep:
+ − 156
assumes a: "Quotient R Abs Rep"
+ − 157
shows "R (Rep a) (Rep b) = (a = b)"
1128
+ − 158
using a
1127
+ − 159
unfolding Quotient_def
+ − 160
by metis
+ − 161
+ − 162
lemma Quotient_rep_abs:
+ − 163
assumes a: "Quotient R Abs Rep"
+ − 164
shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
+ − 165
using a unfolding Quotient_def
+ − 166
by blast
+ − 167
+ − 168
lemma Quotient_rel_abs:
+ − 169
assumes a: "Quotient E Abs Rep"
+ − 170
shows "E r s \<Longrightarrow> Abs r = Abs s"
+ − 171
using a unfolding Quotient_def
+ − 172
by blast
+ − 173
+ − 174
lemma Quotient_symp:
+ − 175
assumes a: "Quotient E Abs Rep"
+ − 176
shows "symp E"
+ − 177
using a unfolding Quotient_def symp_def
+ − 178
by metis
+ − 179
+ − 180
lemma Quotient_transp:
+ − 181
assumes a: "Quotient E Abs Rep"
+ − 182
shows "transp E"
+ − 183
using a unfolding Quotient_def transp_def
+ − 184
by metis
+ − 185
+ − 186
lemma identity_quotient:
+ − 187
shows "Quotient (op =) id id"
+ − 188
unfolding Quotient_def id_def
+ − 189
by blast
+ − 190
+ − 191
lemma fun_quotient:
+ − 192
assumes q1: "Quotient R1 abs1 rep1"
+ − 193
and q2: "Quotient R2 abs2 rep2"
+ − 194
shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
+ − 195
proof -
+ − 196
have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
1128
+ − 197
using q1 q2
1127
+ − 198
unfolding Quotient_def
+ − 199
unfolding expand_fun_eq
+ − 200
by simp
+ − 201
moreover
+ − 202
have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
1128
+ − 203
using q1 q2
1127
+ − 204
unfolding Quotient_def
+ − 205
by (simp (no_asm)) (metis)
+ − 206
moreover
1128
+ − 207
have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
1127
+ − 208
(rep1 ---> abs2) r = (rep1 ---> abs2) s)"
+ − 209
unfolding expand_fun_eq
+ − 210
apply(auto)
+ − 211
using q1 q2 unfolding Quotient_def
+ − 212
apply(metis)
+ − 213
using q1 q2 unfolding Quotient_def
+ − 214
apply(metis)
+ − 215
using q1 q2 unfolding Quotient_def
+ − 216
apply(metis)
+ − 217
using q1 q2 unfolding Quotient_def
+ − 218
apply(metis)
+ − 219
done
+ − 220
ultimately
+ − 221
show "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
+ − 222
unfolding Quotient_def by blast
+ − 223
qed
+ − 224
+ − 225
lemma abs_o_rep:
+ − 226
assumes a: "Quotient R Abs Rep"
+ − 227
shows "Abs o Rep = id"
+ − 228
unfolding expand_fun_eq
+ − 229
by (simp add: Quotient_abs_rep[OF a])
+ − 230
+ − 231
lemma equals_rsp:
+ − 232
assumes q: "Quotient R Abs Rep"
+ − 233
and a: "R xa xb" "R ya yb"
+ − 234
shows "R xa ya = R xb yb"
1128
+ − 235
using a Quotient_symp[OF q] Quotient_transp[OF q]
1127
+ − 236
unfolding symp_def transp_def
+ − 237
by blast
+ − 238
+ − 239
lemma lambda_prs:
+ − 240
assumes q1: "Quotient R1 Abs1 Rep1"
+ − 241
and q2: "Quotient R2 Abs2 Rep2"
+ − 242
shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
+ − 243
unfolding expand_fun_eq
+ − 244
using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
+ − 245
by simp
+ − 246
+ − 247
lemma lambda_prs1:
+ − 248
assumes q1: "Quotient R1 Abs1 Rep1"
+ − 249
and q2: "Quotient R2 Abs2 Rep2"
+ − 250
shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
+ − 251
unfolding expand_fun_eq
+ − 252
using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
+ − 253
by simp
+ − 254
+ − 255
lemma rep_abs_rsp:
+ − 256
assumes q: "Quotient R Abs Rep"
+ − 257
and a: "R x1 x2"
+ − 258
shows "R x1 (Rep (Abs x2))"
+ − 259
using a Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]
+ − 260
by metis
+ − 261
+ − 262
lemma rep_abs_rsp_left:
+ − 263
assumes q: "Quotient R Abs Rep"
+ − 264
and a: "R x1 x2"
+ − 265
shows "R (Rep (Abs x1)) x2"
+ − 266
using a Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]
+ − 267
by metis
+ − 268
1128
+ − 269
text{*
1127
+ − 270
In the following theorem R1 can be instantiated with anything,
+ − 271
but we know some of the types of the Rep and Abs functions;
+ − 272
so by solving Quotient assumptions we can get a unique R1 that
+ − 273
will be provable; which is why we need to use apply_rsp and
+ − 274
not the primed version *}
+ − 275
+ − 276
lemma apply_rsp:
+ − 277
fixes f g::"'a \<Rightarrow> 'c"
+ − 278
assumes q: "Quotient R1 Abs1 Rep1"
+ − 279
and a: "(R1 ===> R2) f g" "R1 x y"
+ − 280
shows "R2 (f x) (g y)"
+ − 281
using a by simp
+ − 282
+ − 283
lemma apply_rsp':
+ − 284
assumes a: "(R1 ===> R2) f g" "R1 x y"
+ − 285
shows "R2 (f x) (g y)"
+ − 286
using a by simp
+ − 287
+ − 288
section {* lemmas for regularisation of ball and bex *}
+ − 289
+ − 290
lemma ball_reg_eqv:
+ − 291
fixes P :: "'a \<Rightarrow> bool"
+ − 292
assumes a: "equivp R"
+ − 293
shows "Ball (Respects R) P = (All P)"
1128
+ − 294
using a
1127
+ − 295
unfolding equivp_def
+ − 296
by (auto simp add: in_respects)
+ − 297
+ − 298
lemma bex_reg_eqv:
+ − 299
fixes P :: "'a \<Rightarrow> bool"
+ − 300
assumes a: "equivp R"
+ − 301
shows "Bex (Respects R) P = (Ex P)"
1128
+ − 302
using a
1127
+ − 303
unfolding equivp_def
+ − 304
by (auto simp add: in_respects)
+ − 305
+ − 306
lemma ball_reg_right:
+ − 307
assumes a: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x"
+ − 308
shows "All P \<longrightarrow> Ball R Q"
+ − 309
using a by (metis COMBC_def Collect_def Collect_mem_eq)
+ − 310
+ − 311
lemma bex_reg_left:
+ − 312
assumes a: "\<And>x. R x \<Longrightarrow> Q x \<longrightarrow> P x"
+ − 313
shows "Bex R Q \<longrightarrow> Ex P"
+ − 314
using a by (metis COMBC_def Collect_def Collect_mem_eq)
+ − 315
+ − 316
lemma ball_reg_left:
+ − 317
assumes a: "equivp R"
+ − 318
shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P"
+ − 319
using a by (metis equivp_reflp in_respects)
+ − 320
+ − 321
lemma bex_reg_right:
+ − 322
assumes a: "equivp R"
+ − 323
shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P"
+ − 324
using a by (metis equivp_reflp in_respects)
+ − 325
+ − 326
lemma ball_reg_eqv_range:
+ − 327
fixes P::"'a \<Rightarrow> bool"
+ − 328
and x::"'a"
+ − 329
assumes a: "equivp R2"
+ − 330
shows "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))"
+ − 331
apply(rule iffI)
+ − 332
apply(rule allI)
+ − 333
apply(drule_tac x="\<lambda>y. f x" in bspec)
+ − 334
apply(simp add: in_respects)
+ − 335
apply(rule impI)
+ − 336
using a equivp_reflp_symp_transp[of "R2"]
+ − 337
apply(simp add: reflp_def)
+ − 338
apply(simp)
+ − 339
apply(simp)
+ − 340
done
+ − 341
+ − 342
lemma bex_reg_eqv_range:
+ − 343
assumes a: "equivp R2"
+ − 344
shows "(Bex (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = Ex (\<lambda>f. P (f x)))"
+ − 345
apply(auto)
+ − 346
apply(rule_tac x="\<lambda>y. f x" in bexI)
+ − 347
apply(simp)
+ − 348
apply(simp add: Respects_def in_respects)
+ − 349
apply(rule impI)
+ − 350
using a equivp_reflp_symp_transp[of "R2"]
+ − 351
apply(simp add: reflp_def)
+ − 352
done
+ − 353
1137
36d596cb63a2
moved "strange" lemma to quotient_tacs; marked a number of lemmas as unused; tuned
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 354
(* Next four lemmas are unused *)
1127
+ − 355
lemma all_reg:
+ − 356
assumes a: "!x :: 'a. (P x --> Q x)"
+ − 357
and b: "All P"
+ − 358
shows "All Q"
+ − 359
using a b by (metis)
+ − 360
+ − 361
lemma ex_reg:
+ − 362
assumes a: "!x :: 'a. (P x --> Q x)"
+ − 363
and b: "Ex P"
+ − 364
shows "Ex Q"
+ − 365
using a b by metis
+ − 366
+ − 367
lemma ball_reg:
+ − 368
assumes a: "!x :: 'a. (R x --> P x --> Q x)"
+ − 369
and b: "Ball R P"
+ − 370
shows "Ball R Q"
+ − 371
using a b by (metis COMBC_def Collect_def Collect_mem_eq)
+ − 372
+ − 373
lemma bex_reg:
+ − 374
assumes a: "!x :: 'a. (R x --> P x --> Q x)"
+ − 375
and b: "Bex R P"
+ − 376
shows "Bex R Q"
+ − 377
using a b by (metis COMBC_def Collect_def Collect_mem_eq)
+ − 378
1137
36d596cb63a2
moved "strange" lemma to quotient_tacs; marked a number of lemmas as unused; tuned
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 379
1127
+ − 380
lemma ball_all_comm:
+ − 381
assumes "\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)"
+ − 382
shows "(\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y)"
+ − 383
using assms by auto
+ − 384
+ − 385
lemma bex_ex_comm:
+ − 386
assumes "(\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)"
+ − 387
shows "(\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y)"
+ − 388
using assms by auto
+ − 389
+ − 390
section {* Bounded abstraction *}
+ − 391
+ − 392
definition
+ − 393
Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+ − 394
where
+ − 395
"x \<in> p \<Longrightarrow> Babs p m x = m x"
+ − 396
+ − 397
lemma babs_rsp:
+ − 398
assumes q: "Quotient R1 Abs1 Rep1"
+ − 399
and a: "(R1 ===> R2) f g"
+ − 400
shows "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"
+ − 401
apply (auto simp add: Babs_def in_respects)
+ − 402
apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
+ − 403
using a apply (simp add: Babs_def)
+ − 404
apply (simp add: in_respects)
+ − 405
using Quotient_rel[OF q]
+ − 406
by metis
+ − 407
+ − 408
lemma babs_prs:
+ − 409
assumes q1: "Quotient R1 Abs1 Rep1"
+ − 410
and q2: "Quotient R2 Abs2 Rep2"
+ − 411
shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f"
+ − 412
apply (rule ext)
+ − 413
apply (simp)
+ − 414
apply (subgoal_tac "Rep1 x \<in> Respects R1")
+ − 415
apply (simp add: Babs_def Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+ − 416
apply (simp add: in_respects Quotient_rel_rep[OF q1])
+ − 417
done
+ − 418
+ − 419
lemma babs_simp:
+ − 420
assumes q: "Quotient R1 Abs Rep"
+ − 421
shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)"
+ − 422
apply(rule iffI)
+ − 423
apply(simp_all only: babs_rsp[OF q])
+ − 424
apply(auto simp add: Babs_def)
+ − 425
apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
+ − 426
apply(metis Babs_def)
+ − 427
apply (simp add: in_respects)
+ − 428
using Quotient_rel[OF q]
+ − 429
by metis
+ − 430
1128
+ − 431
(* If a user proves that a particular functional relation
1127
+ − 432
is an equivalence this may be useful in regularising *)
+ − 433
lemma babs_reg_eqv:
+ − 434
shows "equivp R \<Longrightarrow> Babs (Respects R) P = P"
+ − 435
by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp)
+ − 436
+ − 437
+ − 438
(* 3 lemmas needed for proving repabs_inj *)
+ − 439
lemma ball_rsp:
+ − 440
assumes a: "(R ===> (op =)) f g"
+ − 441
shows "Ball (Respects R) f = Ball (Respects R) g"
+ − 442
using a by (simp add: Ball_def in_respects)
+ − 443
+ − 444
lemma bex_rsp:
+ − 445
assumes a: "(R ===> (op =)) f g"
+ − 446
shows "(Bex (Respects R) f = Bex (Respects R) g)"
+ − 447
using a by (simp add: Bex_def in_respects)
+ − 448
+ − 449
lemma bex1_rsp:
+ − 450
assumes a: "(R ===> (op =)) f g"
+ − 451
shows "Ex1 (\<lambda>x. x \<in> Respects R \<and> f x) = Ex1 (\<lambda>x. x \<in> Respects R \<and> g x)"
1128
+ − 452
using a
1127
+ − 453
by (simp add: Ex1_def in_respects) auto
+ − 454
+ − 455
(* 2 lemmas needed for cleaning of quantifiers *)
+ − 456
lemma all_prs:
+ − 457
assumes a: "Quotient R absf repf"
+ − 458
shows "Ball (Respects R) ((absf ---> id) f) = All f"
+ − 459
using a unfolding Quotient_def Ball_def in_respects fun_map_def id_apply
+ − 460
by metis
+ − 461
+ − 462
lemma ex_prs:
+ − 463
assumes a: "Quotient R absf repf"
+ − 464
shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
+ − 465
using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply
+ − 466
by metis
+ − 467
+ − 468
section {* Bex1_rel quantifier *}
+ − 469
+ − 470
definition
+ − 471
Bex1_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
+ − 472
where
+ − 473
"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)))"
+ − 474
+ − 475
lemma bex1_rel_aux:
+ − 476
"\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R x\<rbrakk> \<Longrightarrow> Bex1_rel R y"
+ − 477
unfolding Bex1_rel_def
+ − 478
apply (erule conjE)+
+ − 479
apply (erule bexE)
+ − 480
apply rule
+ − 481
apply (rule_tac x="xa" in bexI)
+ − 482
apply metis
+ − 483
apply metis
+ − 484
apply rule+
+ − 485
apply (erule_tac x="xaa" in ballE)
+ − 486
prefer 2
+ − 487
apply (metis)
+ − 488
apply (erule_tac x="ya" in ballE)
+ − 489
prefer 2
+ − 490
apply (metis)
+ − 491
apply (metis in_respects)
+ − 492
done
+ − 493
+ − 494
lemma bex1_rel_aux2:
+ − 495
"\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R y\<rbrakk> \<Longrightarrow> Bex1_rel R x"
+ − 496
unfolding Bex1_rel_def
+ − 497
apply (erule conjE)+
+ − 498
apply (erule bexE)
+ − 499
apply rule
+ − 500
apply (rule_tac x="xa" in bexI)
+ − 501
apply metis
+ − 502
apply metis
+ − 503
apply rule+
+ − 504
apply (erule_tac x="xaa" in ballE)
+ − 505
prefer 2
+ − 506
apply (metis)
+ − 507
apply (erule_tac x="ya" in ballE)
+ − 508
prefer 2
+ − 509
apply (metis)
+ − 510
apply (metis in_respects)
+ − 511
done
+ − 512
+ − 513
lemma bex1_rel_rsp:
+ − 514
assumes a: "Quotient R absf repf"
+ − 515
shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)"
+ − 516
apply simp
+ − 517
apply clarify
+ − 518
apply rule
+ − 519
apply (simp_all add: bex1_rel_aux bex1_rel_aux2)
+ − 520
apply (erule bex1_rel_aux2)
+ − 521
apply assumption
+ − 522
done
+ − 523
+ − 524
+ − 525
lemma ex1_prs:
+ − 526
assumes a: "Quotient R absf repf"
+ − 527
shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f"
+ − 528
apply simp
+ − 529
apply (subst Bex1_rel_def)
+ − 530
apply (subst Bex_def)
+ − 531
apply (subst Ex1_def)
+ − 532
apply simp
+ − 533
apply rule
+ − 534
apply (erule conjE)+
+ − 535
apply (erule_tac exE)
+ − 536
apply (erule conjE)
+ − 537
apply (subgoal_tac "\<forall>y. R y y \<longrightarrow> f (absf y) \<longrightarrow> R x y")
+ − 538
apply (rule_tac x="absf x" in exI)
+ − 539
apply (simp)
+ − 540
apply rule+
+ − 541
using a unfolding Quotient_def
+ − 542
apply metis
+ − 543
apply rule+
+ − 544
apply (erule_tac x="x" in ballE)
+ − 545
apply (erule_tac x="y" in ballE)
+ − 546
apply simp
+ − 547
apply (simp add: in_respects)
+ − 548
apply (simp add: in_respects)
+ − 549
apply (erule_tac exE)
+ − 550
apply rule
+ − 551
apply (rule_tac x="repf x" in exI)
+ − 552
apply (simp only: in_respects)
+ − 553
apply rule
+ − 554
apply (metis Quotient_rel_rep[OF a])
+ − 555
using a unfolding Quotient_def apply (simp)
+ − 556
apply rule+
+ − 557
using a unfolding Quotient_def in_respects
+ − 558
apply metis
+ − 559
done
+ − 560
+ − 561
lemma bex1_bexeq_reg: "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))"
+ − 562
apply (simp add: Ex1_def Bex1_rel_def in_respects)
+ − 563
apply clarify
+ − 564
apply auto
+ − 565
apply (rule bexI)
+ − 566
apply assumption
+ − 567
apply (simp add: in_respects)
+ − 568
apply (simp add: in_respects)
+ − 569
apply auto
+ − 570
done
+ − 571
+ − 572
section {* Various respects and preserve lemmas *}
+ − 573
+ − 574
lemma quot_rel_rsp:
+ − 575
assumes a: "Quotient R Abs Rep"
+ − 576
shows "(R ===> R ===> op =) R R"
+ − 577
apply(rule fun_rel_id)+
+ − 578
apply(rule equals_rsp[OF a])
+ − 579
apply(assumption)+
+ − 580
done
+ − 581
+ − 582
lemma o_prs:
+ − 583
assumes q1: "Quotient R1 Abs1 Rep1"
+ − 584
and q2: "Quotient R2 Abs2 Rep2"
+ − 585
and q3: "Quotient R3 Abs3 Rep3"
+ − 586
shows "(Rep1 ---> Abs3) (((Abs2 ---> Rep3) f) o ((Abs1 ---> Rep2) g)) = f o g"
+ − 587
using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3]
+ − 588
unfolding o_def expand_fun_eq by simp
+ − 589
+ − 590
lemma o_rsp:
+ − 591
assumes q1: "Quotient R1 Abs1 Rep1"
+ − 592
and q2: "Quotient R2 Abs2 Rep2"
+ − 593
and q3: "Quotient R3 Abs3 Rep3"
+ − 594
and a1: "(R2 ===> R3) f1 f2"
+ − 595
and a2: "(R1 ===> R2) g1 g2"
+ − 596
shows "(R1 ===> R3) (f1 o g1) (f2 o g2)"
+ − 597
using a1 a2 unfolding o_def expand_fun_eq
+ − 598
by (auto)
+ − 599
+ − 600
lemma cond_prs:
+ − 601
assumes a: "Quotient R absf repf"
+ − 602
shows "absf (if a then repf b else repf c) = (if a then b else c)"
+ − 603
using a unfolding Quotient_def by auto
+ − 604
+ − 605
lemma if_prs:
+ − 606
assumes q: "Quotient R Abs Rep"
+ − 607
shows "Abs (If a (Rep b) (Rep c)) = If a b c"
+ − 608
using Quotient_abs_rep[OF q] by auto
+ − 609
+ − 610
(* q not used *)
+ − 611
lemma if_rsp:
+ − 612
assumes q: "Quotient R Abs Rep"
+ − 613
and a: "a1 = a2" "R b1 b2" "R c1 c2"
+ − 614
shows "R (If a1 b1 c1) (If a2 b2 c2)"
+ − 615
using a by auto
+ − 616
+ − 617
lemma let_prs:
+ − 618
assumes q1: "Quotient R1 Abs1 Rep1"
+ − 619
and q2: "Quotient R2 Abs2 Rep2"
+ − 620
shows "Abs2 (Let (Rep1 x) ((Abs1 ---> Rep2) f)) = Let x f"
+ − 621
using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] by auto
+ − 622
+ − 623
lemma let_rsp:
+ − 624
assumes q1: "Quotient R1 Abs1 Rep1"
+ − 625
and a1: "(R1 ===> R2) f g"
+ − 626
and a2: "R1 x y"
+ − 627
shows "R2 ((Let x f)::'c) ((Let y g)::'c)"
+ − 628
using apply_rsp[OF q1 a1] a2 by auto
+ − 629
1124
+ − 630
locale quot_type =
597
+ − 631
fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+ − 632
and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
+ − 633
and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
+ − 634
assumes equivp: "equivp R"
+ − 635
and rep_prop: "\<And>y. \<exists>x. Rep y = R x"
+ − 636
and rep_inverse: "\<And>x. Abs (Rep x) = x"
+ − 637
and abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
+ − 638
and rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
+ − 639
begin
+ − 640
+ − 641
definition
719
+ − 642
abs::"'a \<Rightarrow> 'b"
597
+ − 643
where
719
+ − 644
"abs x \<equiv> Abs (R x)"
597
+ − 645
+ − 646
definition
719
+ − 647
rep::"'b \<Rightarrow> 'a"
597
+ − 648
where
719
+ − 649
"rep a = Eps (Rep a)"
597
+ − 650
1122
+ − 651
lemma homeier_lem9:
597
+ − 652
shows "R (Eps (R x)) = R x"
+ − 653
proof -
+ − 654
have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def)
+ − 655
then have "R x (Eps (R x))" by (rule someI)
+ − 656
then show "R (Eps (R x)) = R x"
+ − 657
using equivp unfolding equivp_def by simp
+ − 658
qed
+ − 659
1122
+ − 660
theorem homeier_thm10:
930
68c1f378a70a
All eq_reflections apart from the one of 'id_apply' can be removed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 661
shows "abs (rep a) = a"
719
+ − 662
unfolding abs_def rep_def
597
+ − 663
proof -
+ − 664
from rep_prop
+ − 665
obtain x where eq: "Rep a = R x" by auto
+ − 666
have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp
1122
+ − 667
also have "\<dots> = Abs (R x)" using homeier_lem9 by simp
597
+ − 668
also have "\<dots> = Abs (Rep a)" using eq by simp
+ − 669
also have "\<dots> = a" using rep_inverse by simp
+ − 670
finally
+ − 671
show "Abs (R (Eps (Rep a))) = a" by simp
+ − 672
qed
+ − 673
1122
+ − 674
lemma homeier_lem7:
919
+ − 675
shows "(R x = R y) = (Abs (R x) = Abs (R y))" (is "?LHS = ?RHS")
+ − 676
proof -
+ − 677
have "?RHS = (Rep (Abs (R x)) = Rep (Abs (R y)))" by (simp add: rep_inject)
+ − 678
also have "\<dots> = ?LHS" by (simp add: abs_inverse)
+ − 679
finally show "?LHS = ?RHS" by simp
+ − 680
qed
597
+ − 681
1122
+ − 682
theorem homeier_thm11:
719
+ − 683
shows "R r r' = (abs r = abs r')"
1116
+ − 684
unfolding abs_def
1122
+ − 685
by (simp only: equivp[simplified equivp_def] homeier_lem7)
597
+ − 686
920
+ − 687
lemma rep_refl:
+ − 688
shows "R (rep a) (rep a)"
1116
+ − 689
unfolding rep_def
+ − 690
by (simp add: equivp[simplified equivp_def])
920
+ − 691
+ − 692
719
+ − 693
lemma rep_abs_rsp:
+ − 694
shows "R f (rep (abs g)) = R f g"
+ − 695
and "R (rep (abs g)) f = R g f"
1122
+ − 696
by (simp_all add: homeier_thm10 homeier_thm11)
597
+ − 697
+ − 698
lemma Quotient:
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 699
shows "Quotient R abs rep"
1116
+ − 700
unfolding Quotient_def
1122
+ − 701
apply(simp add: homeier_thm10)
1116
+ − 702
apply(simp add: rep_refl)
1122
+ − 703
apply(subst homeier_thm11[symmetric])
1116
+ − 704
apply(simp add: equivp[simplified equivp_def])
+ − 705
done
597
+ − 706
+ − 707
end
+ − 708
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 709
section {* ML setup *}
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 710
919
+ − 711
text {* Auxiliary data for the quotient package *}
869
ce5f78f0eac5
Finished organising an efficient datastructure for qconst_info.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 712
597
+ − 713
use "quotient_info.ML"
+ − 714
+ − 715
declare [[map "fun" = (fun_map, fun_rel)]]
615
386a6b1a5203
the lift_tac produces a warning message if one of the three automatic proofs fails
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 716
909
+ − 717
lemmas [quot_thm] = fun_quotient
911
+ − 718
lemmas [quot_respect] = quot_rel_rsp
648
830b58c2fa94
decoupled QuotProd from QuotMain and also started new cleaning strategy
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 719
lemmas [quot_equiv] = identity_equivp
597
+ − 720
919
+ − 721
+ − 722
text {* Lemmas about simplifying id's. *}
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 723
lemmas [id_simps] =
925
+ − 724
id_def[symmetric]
930
68c1f378a70a
All eq_reflections apart from the one of 'id_apply' can be removed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 725
fun_map_id
939
ce774af6b964
Changed the lambda_prs_simple_conv to use id_apply, now last eq_reflection can be removed from id_simps.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 726
id_apply
930
68c1f378a70a
All eq_reflections apart from the one of 'id_apply' can be removed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 727
id_o
68c1f378a70a
All eq_reflections apart from the one of 'id_apply' can be removed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 728
o_id
825
+ − 729
eq_comp_r
774
b4ffb8826105
moved get_fun into quotient_term; this simplifies the overall including structure of the package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 730
919
+ − 731
text {* Translation functions for the lifting process. *}
1127
+ − 732
use "quotient_term.ML"
774
b4ffb8826105
moved get_fun into quotient_term; this simplifies the overall including structure of the package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 733
b4ffb8826105
moved get_fun into quotient_term; this simplifies the overall including structure of the package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 734
919
+ − 735
text {* Definitions of the quotient types. *}
725
+ − 736
use "quotient_typ.ML"
597
+ − 737
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 738
919
+ − 739
text {* Definitions for quotient constants. *}
597
+ − 740
use "quotient_def.ML"
+ − 741
759
+ − 742
1122
+ − 743
text {*
+ − 744
An auxiliary constant for recording some information
+ − 745
about the lifted theorem in a tactic.
919
+ − 746
*}
758
+ − 747
definition
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 748
"Quot_True x \<equiv> True"
605
120e479ed367
first attempt to deal with Babs in regularise and cleaning (not yet working)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 749
1127
+ − 750
lemma
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 751
shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P"
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 752
and QT_ex: "Quot_True (Ex P) \<Longrightarrow> Quot_True P"
907
+ − 753
and QT_ex1: "Quot_True (Ex1 P) \<Longrightarrow> Quot_True P"
1113
+ − 754
and QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True (P x))"
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 755
and QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)"
1116
+ − 756
by (simp_all add: Quot_True_def ext)
751
+ − 757
773
d6acae26d027
tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 758
lemma QT_imp: "Quot_True a \<equiv> Quot_True b"
1116
+ − 759
by (simp add: Quot_True_def)
751
+ − 760
1122
+ − 761
919
+ − 762
text {* Tactics for proving the lifted theorems *}
758
+ − 763
use "quotient_tacs.ML"
751
+ − 764
689
+ − 765
section {* Methods / Interface *}
+ − 766
632
+ − 767
method_setup lifting =
1143
+ − 768
{* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt thms))) *}
1122
+ − 769
{* lifts theorems to quotient types *}
632
+ − 770
+ − 771
method_setup lifting_setup =
1143
+ − 772
{* Attrib.thm >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.procedure_tac ctxt thms))) *}
1122
+ − 773
{* sets up the three goals for the quotient lifting procedure *}
632
+ − 774
+ − 775
method_setup regularize =
1143
+ − 776
{* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.regularize_tac ctxt))) *}
1122
+ − 777
{* proves the regularization goals from the quotient lifting procedure *}
632
+ − 778
+ − 779
method_setup injection =
1143
+ − 780
{* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.all_injection_tac ctxt))) *}
1122
+ − 781
{* proves the rep/abs injection goals from the quotient lifting procedure *}
632
+ − 782
+ − 783
method_setup cleaning =
1143
+ − 784
{* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.clean_tac ctxt))) *}
1122
+ − 785
{* proves the cleaning goals from the quotient lifting procedure *}
632
+ − 786
1068
+ − 787
attribute_setup quot_lifted =
1077
+ − 788
{* Scan.succeed Quotient_Tacs.lifted_attrib *}
1122
+ − 789
{* lifts theorems to quotient types *}
1068
+ − 790
1129
+ − 791
no_notation
+ − 792
rel_conj (infixr "OOO" 75) and
+ − 793
fun_map (infixr "--->" 55) and
+ − 794
fun_rel (infixr "===>" 55)
+ − 795
597
+ − 796
end
+ − 797