0
+ − 1
theory QuotScript
+ − 2
imports Main
+ − 3
begin
+ − 4
+ − 5
definition
+ − 6
"EQUIV E \<equiv> \<forall>x y. E x y = (E x = E y)"
+ − 7
+ − 8
definition
+ − 9
"REFL E \<equiv> \<forall>x. E x x"
+ − 10
+ − 11
definition
+ − 12
"SYM E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x"
+ − 13
+ − 14
definition
+ − 15
"TRANS E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z"
+ − 16
+ − 17
lemma EQUIV_REFL_SYM_TRANS:
+ − 18
shows "EQUIV E = (REFL E \<and> SYM E \<and> TRANS E)"
+ − 19
unfolding EQUIV_def REFL_def SYM_def TRANS_def expand_fun_eq
+ − 20
by (blast)
+ − 21
217
+ − 22
lemma EQUIV_REFL:
416
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 23
shows "EQUIV E \<Longrightarrow> (\<And>x. E x x)"
3f3927f793d4
Removing arguments of tactics: absrep, rel_refl, reps_same are computed.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 24
by (simp add: EQUIV_REFL_SYM_TRANS REFL_def)
217
+ − 25
0
+ − 26
definition
+ − 27
"PART_EQUIV 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)))"
+ − 28
+ − 29
lemma EQUIV_IMP_PART_EQUIV:
+ − 30
assumes a: "EQUIV E"
+ − 31
shows "PART_EQUIV E"
+ − 32
using a unfolding EQUIV_def PART_EQUIV_def
+ − 33
by auto
+ − 34
+ − 35
definition
+ − 36
"QUOTIENT E Abs Rep \<equiv> (\<forall>a. Abs (Rep a) = a) \<and>
+ − 37
(\<forall>a. E (Rep a) (Rep a)) \<and>
+ − 38
(\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"
+ − 39
+ − 40
lemma QUOTIENT_ABS_REP:
+ − 41
assumes a: "QUOTIENT E Abs Rep"
+ − 42
shows "Abs (Rep a) = a"
+ − 43
using a unfolding QUOTIENT_def
+ − 44
by simp
+ − 45
+ − 46
lemma QUOTIENT_REP_REFL:
+ − 47
assumes a: "QUOTIENT E Abs Rep"
+ − 48
shows "E (Rep a) (Rep a)"
+ − 49
using a unfolding QUOTIENT_def
+ − 50
by blast
+ − 51
+ − 52
lemma QUOTIENT_REL:
+ − 53
assumes a: "QUOTIENT E Abs Rep"
+ − 54
shows " E r s = (E r r \<and> E s s \<and> (Abs r = Abs s))"
+ − 55
using a unfolding QUOTIENT_def
+ − 56
by blast
+ − 57
+ − 58
lemma QUOTIENT_REL_ABS:
+ − 59
assumes a: "QUOTIENT E Abs Rep"
+ − 60
shows "E r s \<Longrightarrow> Abs r = Abs s"
+ − 61
using a unfolding QUOTIENT_def
+ − 62
by blast
+ − 63
+ − 64
lemma QUOTIENT_REL_ABS_EQ:
+ − 65
assumes a: "QUOTIENT E Abs Rep"
+ − 66
shows "E r r \<Longrightarrow> E s s \<Longrightarrow> E r s = (Abs r = Abs s)"
+ − 67
using a unfolding QUOTIENT_def
+ − 68
by blast
+ − 69
+ − 70
lemma QUOTIENT_REL_REP:
459
+ − 71
assumes a: "QUOTIENT R Abs Rep"
+ − 72
shows "R (Rep a) (Rep b) = (a = b)"
0
+ − 73
using a unfolding QUOTIENT_def
+ − 74
by metis
+ − 75
+ − 76
lemma QUOTIENT_REP_ABS:
459
+ − 77
assumes a: "QUOTIENT R Abs Rep"
+ − 78
shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
0
+ − 79
using a unfolding QUOTIENT_def
+ − 80
by blast
+ − 81
+ − 82
lemma IDENTITY_EQUIV:
+ − 83
shows "EQUIV (op =)"
+ − 84
unfolding EQUIV_def
+ − 85
by auto
+ − 86
+ − 87
lemma IDENTITY_QUOTIENT:
126
+ − 88
shows "QUOTIENT (op =) id id"
+ − 89
unfolding QUOTIENT_def id_def
0
+ − 90
by blast
+ − 91
+ − 92
lemma QUOTIENT_SYM:
+ − 93
assumes a: "QUOTIENT E Abs Rep"
+ − 94
shows "SYM E"
+ − 95
using a unfolding QUOTIENT_def SYM_def
+ − 96
by metis
+ − 97
+ − 98
lemma QUOTIENT_TRANS:
+ − 99
assumes a: "QUOTIENT E Abs Rep"
+ − 100
shows "TRANS E"
+ − 101
using a unfolding QUOTIENT_def TRANS_def
+ − 102
by metis
+ − 103
+ − 104
fun
93
+ − 105
prod_rel
+ − 106
where
+ − 107
"prod_rel r1 r2 = (\<lambda>(a,b) (c,d). r1 a c \<and> r2 b d)"
+ − 108
+ − 109
fun
112
+ − 110
fun_map
0
+ − 111
where
+ − 112
"fun_map f g h x = g (h (f x))"
+ − 113
112
+ − 114
0
+ − 115
abbreviation
112
+ − 116
fun_map_syn (infixr "--->" 55)
0
+ − 117
where
112
+ − 118
"f ---> g \<equiv> fun_map f g"
0
+ − 119
+ − 120
lemma FUN_MAP_I:
126
+ − 121
shows "(id ---> id) = id"
+ − 122
by (simp add: expand_fun_eq id_def)
0
+ − 123
+ − 124
lemma IN_FUN:
+ − 125
shows "x \<in> ((f ---> g) s) = g (f x \<in> s)"
+ − 126
by (simp add: mem_def)
+ − 127
+ − 128
fun
+ − 129
FUN_REL
+ − 130
where
+ − 131
"FUN_REL E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
+ − 132
+ − 133
abbreviation
228
+ − 134
FUN_REL_syn (infixr "===>" 55)
0
+ − 135
where
228
+ − 136
"E1 ===> E2 \<equiv> FUN_REL E1 E2"
0
+ − 137
+ − 138
lemma FUN_REL_EQ:
+ − 139
"(op =) ===> (op =) = (op =)"
+ − 140
by (simp add: expand_fun_eq)
+ − 141
+ − 142
lemma FUN_QUOTIENT:
+ − 143
assumes q1: "QUOTIENT R1 abs1 rep1"
+ − 144
and q2: "QUOTIENT R2 abs2 rep2"
+ − 145
shows "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
+ − 146
proof -
+ − 147
have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
+ − 148
apply(simp add: expand_fun_eq)
+ − 149
using q1 q2
+ − 150
apply(simp add: QUOTIENT_def)
+ − 151
done
+ − 152
moreover
+ − 153
have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
+ − 154
apply(auto)
+ − 155
using q1 q2 unfolding QUOTIENT_def
+ − 156
apply(metis)
+ − 157
done
+ − 158
moreover
+ − 159
have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
+ − 160
(rep1 ---> abs2) r = (rep1 ---> abs2) s)"
+ − 161
apply(auto simp add: expand_fun_eq)
+ − 162
using q1 q2 unfolding QUOTIENT_def
+ − 163
apply(metis)
+ − 164
using q1 q2 unfolding QUOTIENT_def
+ − 165
apply(metis)
+ − 166
using q1 q2 unfolding QUOTIENT_def
+ − 167
apply(metis)
+ − 168
using q1 q2 unfolding QUOTIENT_def
+ − 169
apply(metis)
+ − 170
done
+ − 171
ultimately
+ − 172
show "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
+ − 173
unfolding QUOTIENT_def by blast
+ − 174
qed
+ − 175
+ − 176
definition
+ − 177
Respects
+ − 178
where
+ − 179
"Respects R x \<equiv> (R x x)"
+ − 180
+ − 181
lemma IN_RESPECTS:
+ − 182
shows "(x \<in> Respects R) = R x x"
+ − 183
unfolding mem_def Respects_def by simp
+ − 184
+ − 185
lemma RESPECTS_THM:
+ − 186
shows "Respects (R1 ===> R2) f = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (f y))"
+ − 187
unfolding Respects_def
+ − 188
by (simp add: expand_fun_eq)
+ − 189
+ − 190
lemma RESPECTS_MP:
+ − 191
assumes a: "Respects (R1 ===> R2) f"
+ − 192
and b: "R1 x y"
+ − 193
shows "R2 (f x) (f y)"
+ − 194
using a b unfolding Respects_def
+ − 195
by simp
+ − 196
+ − 197
lemma RESPECTS_REP_ABS:
+ − 198
assumes a: "QUOTIENT R1 Abs1 Rep1"
+ − 199
and b: "Respects (R1 ===> R2) f"
+ − 200
and c: "R1 x x"
+ − 201
shows "R2 (f (Rep1 (Abs1 x))) (f x)"
+ − 202
using a b[simplified RESPECTS_THM] c unfolding QUOTIENT_def
+ − 203
by blast
+ − 204
+ − 205
lemma RESPECTS_o:
+ − 206
assumes a: "Respects (R2 ===> R3) f"
+ − 207
and b: "Respects (R1 ===> R2) g"
+ − 208
shows "Respects (R1 ===> R3) (f o g)"
+ − 209
using a b unfolding Respects_def
+ − 210
by simp
+ − 211
+ − 212
(*
+ − 213
definition
+ − 214
"RES_EXISTS_EQUIV R P \<equiv> (\<exists>x \<in> Respects R. P x) \<and>
+ − 215
(\<forall>x\<in> Respects R. \<forall>y\<in> Respects R. P x \<and> P y \<longrightarrow> R x y)"
+ − 216
*)
+ − 217
+ − 218
lemma FUN_REL_EQ_REL:
+ − 219
assumes q1: "QUOTIENT R1 Abs1 Rep1"
+ − 220
and q2: "QUOTIENT R2 Abs2 Rep2"
+ − 221
shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \<and> (Respects (R1 ===> R2) g)
+ − 222
\<and> ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))"
+ − 223
using FUN_QUOTIENT[OF q1 q2] unfolding Respects_def QUOTIENT_def expand_fun_eq
+ − 224
by blast
+ − 225
458
+ − 226
(* TODO: it is the same as APPLY_RSP *)
0
+ − 227
(* q1 and q2 not used; see next lemma *)
+ − 228
lemma FUN_REL_MP:
+ − 229
assumes q1: "QUOTIENT R1 Abs1 Rep1"
+ − 230
and q2: "QUOTIENT R2 Abs2 Rep2"
+ − 231
shows "(R1 ===> R2) f g \<Longrightarrow> R1 x y \<Longrightarrow> R2 (f x) (g y)"
+ − 232
by simp
+ − 233
+ − 234
lemma FUN_REL_IMP:
+ − 235
shows "(R1 ===> R2) f g \<Longrightarrow> R1 x y \<Longrightarrow> R2 (f x) (g y)"
+ − 236
by simp
+ − 237
+ − 238
lemma FUN_REL_EQUALS:
+ − 239
assumes q1: "QUOTIENT R1 Abs1 Rep1"
+ − 240
and q2: "QUOTIENT R2 Abs2 Rep2"
+ − 241
and r1: "Respects (R1 ===> R2) f"
+ − 242
and r2: "Respects (R1 ===> R2) g"
+ − 243
shows "((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g) = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
+ − 244
apply(rule_tac iffI)
+ − 245
using FUN_QUOTIENT[OF q1 q2] r1 r2 unfolding QUOTIENT_def Respects_def
+ − 246
apply(metis FUN_REL_IMP)
+ − 247
using r1 unfolding Respects_def expand_fun_eq
+ − 248
apply(simp (no_asm_use))
+ − 249
apply(metis QUOTIENT_REL[OF q2] QUOTIENT_REL_REP[OF q1])
+ − 250
done
+ − 251
+ − 252
(* ask Peter: FUN_REL_IMP used twice *)
+ − 253
lemma FUN_REL_IMP2:
+ − 254
assumes q1: "QUOTIENT R1 Abs1 Rep1"
+ − 255
and q2: "QUOTIENT R2 Abs2 Rep2"
+ − 256
and r1: "Respects (R1 ===> R2) f"
+ − 257
and r2: "Respects (R1 ===> R2) g"
+ − 258
and a: "(Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g"
+ − 259
shows "R1 x y \<Longrightarrow> R2 (f x) (g y)"
+ − 260
using q1 q2 r1 r2 a
+ − 261
by (simp add: FUN_REL_EQUALS)
+ − 262
459
+ − 263
(* We don't use it, it is exactly the same as QUOTIENT_REL_REP but wrong way *)
0
+ − 264
lemma EQUALS_PRS:
+ − 265
assumes q: "QUOTIENT R Abs Rep"
+ − 266
shows "(x = y) = R (Rep x) (Rep y)"
459
+ − 267
by (rule QUOTIENT_REL_REP[OF q, symmetric])
0
+ − 268
+ − 269
lemma EQUALS_RSP:
+ − 270
assumes q: "QUOTIENT R Abs Rep"
+ − 271
and a: "R x1 x2" "R y1 y2"
+ − 272
shows "R x1 y1 = R x2 y2"
+ − 273
using QUOTIENT_SYM[OF q] QUOTIENT_TRANS[OF q] unfolding SYM_def TRANS_def
+ − 274
using a by blast
+ − 275
+ − 276
lemma LAMBDA_PRS:
+ − 277
assumes q1: "QUOTIENT R1 Abs1 Rep1"
+ − 278
and q2: "QUOTIENT R2 Abs2 Rep2"
253
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 279
shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
0
+ − 280
unfolding expand_fun_eq
+ − 281
using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2]
+ − 282
by simp
+ − 283
+ − 284
lemma LAMBDA_PRS1:
+ − 285
assumes q1: "QUOTIENT R1 Abs1 Rep1"
+ − 286
and q2: "QUOTIENT R2 Abs2 Rep2"
+ − 287
shows "(\<lambda>x. f x) = (Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x)"
+ − 288
unfolding expand_fun_eq
253
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 289
using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2]
459
+ − 290
by simp
253
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 291
459
+ − 292
(* Not used since applic_prs proves a version for an arbitrary number of arguments *)
253
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 293
lemma APP_PRS:
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 294
assumes q1: "QUOTIENT R1 abs1 rep1"
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 295
and q2: "QUOTIENT R2 abs2 rep2"
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 296
shows "abs2 ((abs1 ---> rep2) f (rep1 x)) = f x"
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 297
unfolding expand_fun_eq
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 298
using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2]
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 299
by simp
0
+ − 300
+ − 301
(* Ask Peter: assumption q1 and q2 not used and lemma is the 'identity' *)
+ − 302
lemma LAMBDA_RSP:
+ − 303
assumes q1: "QUOTIENT R1 Abs1 Rep1"
+ − 304
and q2: "QUOTIENT R2 Abs2 Rep2"
+ − 305
and a: "(R1 ===> R2) f1 f2"
+ − 306
shows "(R1 ===> R2) (\<lambda>x. f1 x) (\<lambda>y. f2 y)"
+ − 307
by (rule a)
+ − 308
+ − 309
(* ASK Peter about next four lemmas in quotientScript
+ − 310
lemma ABSTRACT_PRS:
+ − 311
assumes q1: "QUOTIENT R1 Abs1 Rep1"
+ − 312
and q2: "QUOTIENT R2 Abs2 Rep2"
+ − 313
shows "f = (Rep1 ---> Abs2) ???"
+ − 314
*)
+ − 315
+ − 316
lemma LAMBDA_REP_ABS_RSP:
+ − 317
assumes r1: "\<And>r r'. R1 r r' \<Longrightarrow>R1 r (Rep1 (Abs1 r'))"
+ − 318
and r2: "\<And>r r'. R2 r r' \<Longrightarrow>R2 r (Rep2 (Abs2 r'))"
+ − 319
shows "(R1 ===> R2) f1 f2 \<Longrightarrow> (R1 ===> R2) f1 ((Abs1 ---> Rep2) ((Rep1 ---> Abs2) f2))"
+ − 320
using r1 r2 by auto
+ − 321
+ − 322
lemma REP_ABS_RSP:
+ − 323
assumes q: "QUOTIENT R Abs Rep"
+ − 324
and a: "R x1 x2"
+ − 325
shows "R x1 (Rep (Abs x2))"
459
+ − 326
using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q])
+ − 327
+ − 328
(* Not used *)
+ − 329
lemma REP_ABS_RSP_LEFT:
+ − 330
assumes q: "QUOTIENT R Abs Rep"
+ − 331
and a: "R x1 x2"
113
+ − 332
and "R (Rep (Abs x1)) x2"
459
+ − 333
shows "R x1 (Rep (Abs x2))"
+ − 334
using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q] QUOTIENT_SYM[of q])
0
+ − 335
+ − 336
(* ----------------------------------------------------- *)
+ − 337
(* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE, *)
+ − 338
(* RES_FORALL, RES_EXISTS, RES_EXISTS_EQUIV *)
+ − 339
(* ----------------------------------------------------- *)
+ − 340
+ − 341
(* bool theory: COND, LET *)
+ − 342
+ − 343
lemma IF_PRS:
+ − 344
assumes q: "QUOTIENT R Abs Rep"
+ − 345
shows "If a b c = Abs (If a (Rep b) (Rep c))"
+ − 346
using QUOTIENT_ABS_REP[OF q] by auto
+ − 347
+ − 348
(* ask peter: no use of q *)
+ − 349
lemma IF_RSP:
+ − 350
assumes q: "QUOTIENT R Abs Rep"
+ − 351
and a: "a1 = a2" "R b1 b2" "R c1 c2"
+ − 352
shows "R (If a1 b1 c1) (If a2 b2 c2)"
+ − 353
using a by auto
+ − 354
+ − 355
lemma LET_PRS:
+ − 356
assumes q1: "QUOTIENT R1 Abs1 Rep1"
+ − 357
and q2: "QUOTIENT R2 Abs2 Rep2"
+ − 358
shows "Let x f = Abs2 (Let (Rep1 x) ((Abs1 ---> Rep2) f))"
+ − 359
using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] by auto
+ − 360
+ − 361
lemma LET_RSP:
+ − 362
assumes q1: "QUOTIENT R1 Abs1 Rep1"
+ − 363
and q2: "QUOTIENT R2 Abs2 Rep2"
+ − 364
and a1: "(R1 ===> R2) f g"
+ − 365
and a2: "R1 x y"
+ − 366
shows "R2 (Let x f) (Let y g)"
+ − 367
using FUN_REL_MP[OF q1 q2 a1] a2
+ − 368
by auto
+ − 369
+ − 370
+ − 371
(* ask peter what are literal_case *)
+ − 372
(* literal_case_PRS *)
+ − 373
(* literal_case_RSP *)
+ − 374
+ − 375
+ − 376
(* FUNCTION APPLICATION *)
+ − 377
+ − 378
lemma APPLY_PRS:
+ − 379
assumes q1: "QUOTIENT R1 Abs1 Rep1"
+ − 380
and q2: "QUOTIENT R2 Abs2 Rep2"
+ − 381
shows "f x = Abs2 (((Abs1 ---> Rep2) f) (Rep1 x))"
+ − 382
using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] by auto
+ − 383
+ − 384
(* ask peter: no use of q1 q2 *)
+ − 385
lemma APPLY_RSP:
+ − 386
assumes q1: "QUOTIENT R1 Abs1 Rep1"
+ − 387
and q2: "QUOTIENT R2 Abs2 Rep2"
+ − 388
and a: "(R1 ===> R2) f g" "R1 x y"
+ − 389
shows "R2 (f x) (g y)"
+ − 390
using a by (rule FUN_REL_IMP)
+ − 391
317
+ − 392
lemma APPLY_RSP2:
+ − 393
assumes a: "(R1 ===> R2) f g" "R1 x y"
+ − 394
shows "R2 (f x) (g y)"
+ − 395
using a by (rule FUN_REL_IMP)
+ − 396
0
+ − 397
+ − 398
(* combinators: I, K, o, C, W *)
+ − 399
459
+ − 400
(* We use id_simps which includes id_apply; so these 2 theorems can be removed *)
0
+ − 401
lemma I_PRS:
+ − 402
assumes q: "QUOTIENT R Abs Rep"
126
+ − 403
shows "id e = Abs (id (Rep e))"
0
+ − 404
using QUOTIENT_ABS_REP[OF q] by auto
+ − 405
+ − 406
lemma I_RSP:
+ − 407
assumes q: "QUOTIENT R Abs Rep"
+ − 408
and a: "R e1 e2"
126
+ − 409
shows "R (id e1) (id e2)"
0
+ − 410
using a by auto
+ − 411
+ − 412
lemma o_PRS:
+ − 413
assumes q1: "QUOTIENT R1 Abs1 Rep1"
+ − 414
and q2: "QUOTIENT R2 Abs2 Rep2"
+ − 415
and q3: "QUOTIENT R3 Abs3 Rep3"
+ − 416
shows "f o g = (Rep1 ---> Abs3) (((Abs2 ---> Rep3) f) o ((Abs1 ---> Rep2) g))"
+ − 417
using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] QUOTIENT_ABS_REP[OF q3]
+ − 418
unfolding o_def expand_fun_eq
+ − 419
by simp
+ − 420
+ − 421
lemma o_RSP:
+ − 422
assumes q1: "QUOTIENT R1 Abs1 Rep1"
+ − 423
and q2: "QUOTIENT R2 Abs2 Rep2"
+ − 424
and q3: "QUOTIENT R3 Abs3 Rep3"
+ − 425
and a1: "(R2 ===> R3) f1 f2"
+ − 426
and a2: "(R1 ===> R2) g1 g2"
+ − 427
shows "(R1 ===> R3) (f1 o g1) (f2 o g2)"
+ − 428
using a1 a2 unfolding o_def expand_fun_eq
+ − 429
by (auto)
+ − 430
96
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 431
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 432
458
+ − 433
+ − 434
+ − 435
lemma COND_PRS:
+ − 436
assumes a: "QUOTIENT R absf repf"
+ − 437
shows "(if a then b else c) = absf (if a then repf b else repf c)"
+ − 438
using a unfolding QUOTIENT_def by auto
+ − 439
+ − 440
+ − 441
+ − 442
+ − 443
427
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 444
(* Set of lemmas for regularisation of ball and bex *)
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 445
lemma ball_reg_eqv:
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 446
fixes P :: "'a \<Rightarrow> bool"
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 447
assumes a: "EQUIV R"
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 448
shows "Ball (Respects R) P = (All P)"
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 449
by (metis EQUIV_def IN_RESPECTS a)
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 450
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 451
lemma bex_reg_eqv:
93
+ − 452
fixes P :: "'a \<Rightarrow> bool"
427
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 453
assumes a: "EQUIV R"
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 454
shows "Bex (Respects R) P = (Ex P)"
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 455
by (metis EQUIV_def IN_RESPECTS a)
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 456
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 457
lemma ball_reg_right:
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 458
assumes a: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x"
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 459
shows "All P \<longrightarrow> Ball R Q"
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 460
by (metis COMBC_def Collect_def Collect_mem_eq a)
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 461
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 462
lemma bex_reg_left:
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 463
assumes a: "\<And>x. R x \<Longrightarrow> Q x \<longrightarrow> P x"
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 464
shows "Bex R Q \<longrightarrow> Ex P"
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 465
by (metis COMBC_def Collect_def Collect_mem_eq a)
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 466
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 467
lemma ball_reg_left:
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 468
assumes a: "EQUIV R"
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 469
shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P"
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 470
by (metis EQUIV_REFL IN_RESPECTS a)
93
+ − 471
427
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 472
lemma bex_reg_right:
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 473
assumes a: "EQUIV R"
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 474
shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P"
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 475
by (metis EQUIV_REFL IN_RESPECTS a)
93
+ − 476
427
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 477
lemma ball_reg_eqv_range:
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 478
fixes P::"'a \<Rightarrow> bool"
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 479
and x::"'a"
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 480
assumes a: "EQUIV R2"
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 481
shows "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))"
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 482
apply(rule iffI)
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 483
apply(rule allI)
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 484
apply(drule_tac x="\<lambda>y. f x" in bspec)
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 485
apply(simp add: Respects_def IN_RESPECTS)
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 486
apply(rule impI)
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 487
using a EQUIV_REFL_SYM_TRANS[of "R2"]
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 488
apply(simp add: REFL_def)
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 489
apply(simp)
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 490
apply(simp)
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 491
done
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 492
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 493
lemma bex_reg_eqv_range:
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 494
fixes P::"'a \<Rightarrow> bool"
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 495
and x::"'a"
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 496
assumes a: "EQUIV R2"
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 497
shows "(Bex (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = Ex (\<lambda>f. P (f x)))"
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 498
apply(auto)
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 499
apply(rule_tac x="\<lambda>y. f x" in bexI)
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 500
apply(simp)
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 501
apply(simp add: Respects_def IN_RESPECTS)
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 502
apply(rule impI)
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 503
using a EQUIV_REFL_SYM_TRANS[of "R2"]
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 504
apply(simp add: REFL_def)
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 505
done
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 506
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 507
lemma all_reg:
96
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 508
assumes a: "!x :: 'a. (P x --> Q x)"
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 509
and b: "All P"
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 510
shows "All Q"
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 511
using a b by (metis)
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 512
427
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 513
lemma ex_reg:
96
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 514
assumes a: "!x :: 'a. (P x --> Q x)"
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 515
and b: "Ex P"
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 516
shows "Ex Q"
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 517
using a b by (metis)
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 518
427
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 519
lemma ball_reg:
96
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 520
assumes a: "!x :: 'a. (R x --> P x --> Q x)"
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 521
and b: "Ball R P"
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 522
shows "Ball R Q"
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 523
using a b by (metis COMBC_def Collect_def Collect_mem_eq)
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 524
427
5a3965aa4d80
Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 525
lemma bex_reg:
96
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 526
assumes a: "!x :: 'a. (R x --> P x --> Q x)"
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 527
and b: "Bex R P"
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 528
shows "Bex R Q"
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 529
using a b by (metis COMBC_def Collect_def Collect_mem_eq)
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 530
432
+ − 531
lemma ball_all_comm:
+ − 532
"(\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)) \<Longrightarrow> ((\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y))"
+ − 533
by auto
+ − 534
+ − 535
lemma bex_ex_comm:
+ − 536
"((\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)) \<Longrightarrow> ((\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y))"
+ − 537
by auto
96
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 538
458
+ − 539
(* 2 lemmas needed for proving repabs_inj *)
+ − 540
lemma ball_rsp:
+ − 541
assumes a: "(R ===> (op =)) f g"
+ − 542
shows "Ball (Respects R) f = Ball (Respects R) g"
+ − 543
using a by (simp add: Ball_def IN_RESPECTS)
153
+ − 544
458
+ − 545
lemma bex_rsp:
+ − 546
assumes a: "(R ===> (op =)) f g"
+ − 547
shows "(Bex (Respects R) f = Bex (Respects R) g)"
+ − 548
using a by (simp add: Bex_def IN_RESPECTS)
171
13aab4c59096
More infrastructure for automatic lifting of theorems lifted before
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 549
458
+ − 550
(* 2 lemmas needed for cleaning of quantifiers *)
+ − 551
lemma all_prs:
162
+ − 552
assumes a: "QUOTIENT R absf repf"
458
+ − 553
shows "Ball (Respects R) ((absf ---> id) f) = All f"
+ − 554
using a unfolding QUOTIENT_def
183
6acf9e001038
proved the two lemmas in QuotScript (reformulated them without leading forall)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 555
by (metis IN_RESPECTS fun_map.simps id_apply)
162
+ − 556
458
+ − 557
lemma ex_prs:
187
+ − 558
assumes a: "QUOTIENT R absf repf"
458
+ − 559
shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
+ − 560
using a unfolding QUOTIENT_def
+ − 561
by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply)
171
13aab4c59096
More infrastructure for automatic lifting of theorems lifted before
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 562
93
+ − 563
end
95
+ − 564