920
+ − 1
(* Title: QuotBase.thy
+ − 2
Author: Cezary Kaliszyk and Christian Urban
+ − 3
*)
+ − 4
+ − 5
theory QuotBase
807
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 6
imports Plain ATP_Linkup Predicate
0
+ − 7
begin
+ − 8
920
+ − 9
text {*
+ − 10
Basic definition for equivalence relations
+ − 11
that are represented by predicates.
+ − 12
*}
+ − 13
543
+ − 14
definition
+ − 15
"equivp E \<equiv> \<forall>x y. E x y = (E x = E y)"
0
+ − 16
+ − 17
definition
528
+ − 18
"reflp E \<equiv> \<forall>x. E x x"
0
+ − 19
543
+ − 20
definition
528
+ − 21
"symp E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x"
0
+ − 22
+ − 23
definition
528
+ − 24
"transp E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z"
0
+ − 25
528
+ − 26
lemma equivp_reflp_symp_transp:
+ − 27
shows "equivp E = (reflp E \<and> symp E \<and> transp E)"
543
+ − 28
unfolding equivp_def reflp_def symp_def transp_def expand_fun_eq
920
+ − 29
by blast
0
+ − 30
528
+ − 31
lemma equivp_reflp:
+ − 32
shows "equivp E \<Longrightarrow> (\<And>x. E x x)"
593
18eac4596ef1
QuotProd with product_quotient and a 3 respects and preserves lemmas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 33
by (simp only: equivp_reflp_symp_transp reflp_def)
18eac4596ef1
QuotProd with product_quotient and a 3 respects and preserves lemmas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 34
18eac4596ef1
QuotProd with product_quotient and a 3 respects and preserves lemmas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 35
lemma equivp_symp:
18eac4596ef1
QuotProd with product_quotient and a 3 respects and preserves lemmas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 36
shows "equivp E \<Longrightarrow> (\<And>x y. E x y \<Longrightarrow> E y x)"
18eac4596ef1
QuotProd with product_quotient and a 3 respects and preserves lemmas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 37
by (metis equivp_reflp_symp_transp symp_def)
18eac4596ef1
QuotProd with product_quotient and a 3 respects and preserves lemmas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 38
18eac4596ef1
QuotProd with product_quotient and a 3 respects and preserves lemmas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 39
lemma equivp_transp:
18eac4596ef1
QuotProd with product_quotient and a 3 respects and preserves lemmas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 40
shows "equivp E \<Longrightarrow> (\<And>x y z. E x y \<Longrightarrow> E y z \<Longrightarrow> E x z)"
721
+ − 41
by (metis equivp_reflp_symp_transp transp_def)
217
+ − 42
700
91b079db7380
added Larry's theory; introduced lemma equivpI; added something to the TODO about error messages
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 43
lemma equivpI:
91b079db7380
added Larry's theory; introduced lemma equivpI; added something to the TODO about error messages
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 44
assumes "reflp R" "symp R" "transp R"
91b079db7380
added Larry's theory; introduced lemma equivpI; added something to the TODO about error messages
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 45
shows "equivp R"
721
+ − 46
using assms by (simp add: equivp_reflp_symp_transp)
700
91b079db7380
added Larry's theory; introduced lemma equivpI; added something to the TODO about error messages
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 47
919
+ − 48
lemma eq_imp_rel:
+ − 49
shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
+ − 50
by (simp add: equivp_reflp)
+ − 51
921
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 52
lemma identity_equivp:
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 53
shows "equivp (op =)"
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 54
unfolding equivp_def
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 55
by auto
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 56
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 57
920
+ − 58
text {* Partial equivalences: not yet used anywhere *}
0
+ − 59
definition
541
+ − 60
"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)))"
0
+ − 61
921
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 62
lemma equivp_implies_part_equivp:
528
+ − 63
assumes a: "equivp E"
541
+ − 64
shows "part_equivp E"
920
+ − 65
using a
+ − 66
unfolding equivp_def part_equivp_def
543
+ − 67
by auto
0
+ − 68
920
+ − 69
text {* Composition of Relations *}
841
+ − 70
abbreviation
+ − 71
rel_conj (infixr "OOO" 75)
+ − 72
where
+ − 73
"r1 OOO r2 \<equiv> r1 OO r2 OO r1"
+ − 74
936
+ − 75
lemma eq_comp_r:
+ − 76
shows "((op =) OOO R) = R"
+ − 77
by (auto simp add: expand_fun_eq)
921
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 78
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 79
section {* Respects predicate *}
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 80
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 81
definition
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 82
Respects
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 83
where
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 84
"Respects R x \<equiv> (R x x)"
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 85
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 86
lemma in_respects:
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 87
shows "(x \<in> Respects R) = R x x"
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 88
unfolding mem_def Respects_def
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 89
by simp
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 90
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 91
section {* Function map and function relation *}
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 92
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 93
definition
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 94
fun_map (infixr "--->" 55)
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 95
where
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 96
[simp]: "fun_map f g h x = g (h (f x))"
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 97
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 98
definition
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 99
fun_rel (infixr "===>" 55)
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 100
where
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 101
[simp]: "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 102
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 103
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 104
lemma fun_map_id:
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 105
shows "(id ---> id) = id"
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 106
by (simp add: expand_fun_eq id_def)
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 107
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 108
lemma fun_rel_eq:
926
+ − 109
shows "((op =) ===> (op =)) = (op =)"
+ − 110
by (simp add: expand_fun_eq)
921
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 111
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 112
lemma fun_rel_id:
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 113
assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 114
shows "(R1 ===> R2) f g"
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 115
using a by simp
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 116
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 117
lemma fun_rel_id_asm:
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 118
assumes a: "\<And>x y. R1 x y \<Longrightarrow> (A \<longrightarrow> R2 (f x) (g y))"
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 119
shows "A \<longrightarrow> (R1 ===> R2) f g"
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 120
using a by auto
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 121
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 122
920
+ − 123
section {* Quotient Predicate *}
0
+ − 124
920
+ − 125
definition
+ − 126
"Quotient E Abs Rep \<equiv>
+ − 127
(\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. E (Rep a) (Rep a)) \<and>
+ − 128
(\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"
841
+ − 129
540
c0b13fb70d6d
More code cleaning and renaming: moved rsp and prs lemmas from Int to QuotList
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 130
lemma Quotient_abs_rep:
528
+ − 131
assumes a: "Quotient E Abs Rep"
920
+ − 132
shows "Abs (Rep a) = a"
+ − 133
using a
+ − 134
unfolding Quotient_def
543
+ − 135
by simp
0
+ − 136
541
+ − 137
lemma Quotient_rep_reflp:
528
+ − 138
assumes a: "Quotient E Abs Rep"
541
+ − 139
shows "E (Rep a) (Rep a)"
920
+ − 140
using a
+ − 141
unfolding Quotient_def
543
+ − 142
by blast
0
+ − 143
539
+ − 144
lemma Quotient_rel:
528
+ − 145
assumes a: "Quotient E Abs Rep"
0
+ − 146
shows " E r s = (E r r \<and> E s s \<and> (Abs r = Abs s))"
920
+ − 147
using a
+ − 148
unfolding Quotient_def
543
+ − 149
by blast
0
+ − 150
541
+ − 151
lemma Quotient_rel_rep:
528
+ − 152
assumes a: "Quotient R Abs Rep"
920
+ − 153
shows "R (Rep a) (Rep b) = (a = b)"
+ − 154
using a
+ − 155
unfolding Quotient_def
543
+ − 156
by metis
0
+ − 157
540
c0b13fb70d6d
More code cleaning and renaming: moved rsp and prs lemmas from Int to QuotList
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 158
lemma Quotient_rep_abs:
528
+ − 159
assumes a: "Quotient R Abs Rep"
459
+ − 160
shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
543
+ − 161
using a unfolding Quotient_def
+ − 162
by blast
0
+ − 163
721
+ − 164
lemma Quotient_rel_abs:
+ − 165
assumes a: "Quotient E Abs Rep"
+ − 166
shows "E r s \<Longrightarrow> Abs r = Abs s"
+ − 167
using a unfolding Quotient_def
+ − 168
by blast
+ − 169
528
+ − 170
lemma Quotient_symp:
+ − 171
assumes a: "Quotient E Abs Rep"
+ − 172
shows "symp E"
543
+ − 173
using a unfolding Quotient_def symp_def
+ − 174
by metis
0
+ − 175
528
+ − 176
lemma Quotient_transp:
+ − 177
assumes a: "Quotient E Abs Rep"
+ − 178
shows "transp E"
543
+ − 179
using a unfolding Quotient_def transp_def
+ − 180
by metis
0
+ − 181
920
+ − 182
lemma identity_quotient:
+ − 183
shows "Quotient (op =) id id"
+ − 184
unfolding Quotient_def id_def
+ − 185
by blast
+ − 186
537
+ − 187
lemma fun_quotient:
528
+ − 188
assumes q1: "Quotient R1 abs1 rep1"
+ − 189
and q2: "Quotient R2 abs2 rep2"
+ − 190
shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
0
+ − 191
proof -
+ − 192
have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
+ − 193
apply(simp add: expand_fun_eq)
+ − 194
using q1 q2
528
+ − 195
apply(simp add: Quotient_def)
0
+ − 196
done
+ − 197
moreover
+ − 198
have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
+ − 199
apply(auto)
528
+ − 200
using q1 q2 unfolding Quotient_def
0
+ − 201
apply(metis)
+ − 202
done
+ − 203
moreover
+ − 204
have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
+ − 205
(rep1 ---> abs2) r = (rep1 ---> abs2) s)"
+ − 206
apply(auto simp add: expand_fun_eq)
528
+ − 207
using q1 q2 unfolding Quotient_def
0
+ − 208
apply(metis)
528
+ − 209
using q1 q2 unfolding Quotient_def
0
+ − 210
apply(metis)
528
+ − 211
using q1 q2 unfolding Quotient_def
0
+ − 212
apply(metis)
528
+ − 213
using q1 q2 unfolding Quotient_def
0
+ − 214
apply(metis)
+ − 215
done
+ − 216
ultimately
528
+ − 217
show "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
+ − 218
unfolding Quotient_def by blast
0
+ − 219
qed
+ − 220
921
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 221
lemma abs_o_rep:
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 222
assumes a: "Quotient R Abs Rep"
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 223
shows "Abs o Rep = id"
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 224
apply(rule ext)
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 225
apply(simp add: Quotient_abs_rep[OF a])
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 226
done
0
+ − 227
527
+ − 228
lemma equals_rsp:
528
+ − 229
assumes q: "Quotient R Abs Rep"
519
ebfd747b47ab
Change equiv_trans2 to EQUALS_RSP, since we can prove it for any quotient type, not only for eqv relations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 230
and a: "R xa xb" "R ya yb"
ebfd747b47ab
Change equiv_trans2 to EQUALS_RSP, since we can prove it for any quotient type, not only for eqv relations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 231
shows "R xa ya = R xb yb"
543
+ − 232
using Quotient_symp[OF q] Quotient_transp[OF q] unfolding symp_def transp_def
+ − 233
using a by blast
0
+ − 234
527
+ − 235
lemma lambda_prs:
528
+ − 236
assumes q1: "Quotient R1 Abs1 Rep1"
+ − 237
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
+ − 238
shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
543
+ − 239
unfolding expand_fun_eq
+ − 240
using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
+ − 241
by simp
0
+ − 242
527
+ − 243
lemma lambda_prs1:
528
+ − 244
assumes q1: "Quotient R1 Abs1 Rep1"
+ − 245
and q2: "Quotient R2 Abs2 Rep2"
527
+ − 246
shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
543
+ − 247
unfolding expand_fun_eq
+ − 248
using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
+ − 249
by simp
253
e169a99c6ada
Automatic computation of application preservation and manually finished "alpha.induct". Slow...
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 250
542
+ − 251
lemma rep_abs_rsp:
528
+ − 252
assumes q: "Quotient R Abs Rep"
459
+ − 253
and a: "R x1 x2"
+ − 254
shows "R x1 (Rep (Abs x2))"
921
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 255
using a
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 256
by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q])
0
+ − 257
721
+ − 258
lemma rep_abs_rsp_left:
+ − 259
assumes q: "Quotient R Abs Rep"
+ − 260
and a: "R x1 x2"
+ − 261
shows "R (Rep (Abs x1)) x2"
921
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 262
using a
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 263
by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q])
721
+ − 264
527
+ − 265
(* In the following theorem R1 can be instantiated with anything,
516
+ − 266
but we know some of the types of the Rep and Abs functions;
543
+ − 267
so by solving Quotient assumptions we can get a unique R1 that
+ − 268
will be provable; which is why we need to use apply_rsp and
+ − 269
not the primed version *)
527
+ − 270
lemma apply_rsp:
841
+ − 271
fixes f g::"'a \<Rightarrow> 'c"
528
+ − 272
assumes q: "Quotient R1 Abs1 Rep1"
516
+ − 273
and a: "(R1 ===> R2) f g" "R1 x y"
841
+ − 274
shows "R2 (f x) (g y)"
543
+ − 275
using a by simp
516
+ − 276
527
+ − 277
lemma apply_rsp':
317
+ − 278
assumes a: "(R1 ===> R2) f g" "R1 x y"
+ − 279
shows "R2 (f x) (g y)"
543
+ − 280
using a by simp
458
+ − 281
921
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 282
section {* lemmas for regularisation of ball and bex *}
543
+ − 283
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
+ − 284
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
+ − 285
fixes P :: "'a \<Rightarrow> bool"
528
+ − 286
assumes a: "equivp R"
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
+ − 287
shows "Ball (Respects R) P = (All P)"
542
+ − 288
by (metis equivp_def in_respects a)
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
+ − 289
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
+ − 290
lemma bex_reg_eqv:
93
+ − 291
fixes P :: "'a \<Rightarrow> bool"
528
+ − 292
assumes a: "equivp R"
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
+ − 293
shows "Bex (Respects R) P = (Ex P)"
542
+ − 294
by (metis equivp_def in_respects a)
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
+ − 295
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
+ − 296
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
+ − 297
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
+ − 298
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
+ − 299
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
+ − 300
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
+ − 301
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
+ − 302
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
+ − 303
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
+ − 304
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
+ − 305
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
+ − 306
lemma ball_reg_left:
528
+ − 307
assumes a: "equivp R"
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
+ − 308
shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P"
542
+ − 309
by (metis equivp_reflp in_respects a)
93
+ − 310
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
+ − 311
lemma bex_reg_right:
528
+ − 312
assumes a: "equivp R"
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
+ − 313
shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P"
542
+ − 314
by (metis equivp_reflp in_respects a)
93
+ − 315
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
+ − 316
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
+ − 317
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
+ − 318
and x::"'a"
528
+ − 319
assumes a: "equivp R2"
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
+ − 320
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
+ − 321
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
+ − 322
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
+ − 323
apply(drule_tac x="\<lambda>y. f x" in bspec)
605
120e479ed367
first attempt to deal with Babs in regularise and cleaning (not yet working)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 324
apply(simp add: in_respects)
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
+ − 325
apply(rule impI)
528
+ − 326
using a equivp_reflp_symp_transp[of "R2"]
+ − 327
apply(simp add: reflp_def)
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
+ − 328
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
+ − 329
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
+ − 330
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
+ − 331
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
+ − 332
lemma bex_reg_eqv_range:
528
+ − 333
assumes a: "equivp R2"
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
+ − 334
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
+ − 335
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
+ − 336
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
+ − 337
apply(simp)
542
+ − 338
apply(simp add: Respects_def in_respects)
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
+ − 339
apply(rule impI)
528
+ − 340
using a equivp_reflp_symp_transp[of "R2"]
+ − 341
apply(simp add: reflp_def)
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
+ − 342
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
+ − 343
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
+ − 344
lemma all_reg:
96
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 345
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
+ − 346
and b: "All P"
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 347
shows "All Q"
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 348
using a b by (metis)
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 349
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
+ − 350
lemma ex_reg:
96
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 351
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
+ − 352
and b: "Ex P"
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 353
shows "Ex Q"
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 354
using a b by (metis)
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 355
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
+ − 356
lemma ball_reg:
96
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 357
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
+ − 358
and b: "Ball R P"
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 359
shows "Ball R Q"
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 360
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
+ − 361
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
+ − 362
lemma bex_reg:
96
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 363
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
+ − 364
and b: "Bex R P"
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 365
shows "Bex R Q"
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 366
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
+ − 367
432
+ − 368
lemma ball_all_comm:
+ − 369
"(\<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))"
721
+ − 370
by auto
432
+ − 371
+ − 372
lemma bex_ex_comm:
+ − 373
"((\<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))"
721
+ − 374
by auto
96
4da714704611
A number of lemmas for REGULARIZE_TAC and regularizing card1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 375
921
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 376
section {* Bounded abstraction *}
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 377
595
+ − 378
definition
+ − 379
Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+ − 380
where
+ − 381
"(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
+ − 382
+ − 383
lemma babs_rsp:
+ − 384
assumes q: "Quotient R1 Abs1 Rep1"
+ − 385
and a: "(R1 ===> R2) f g"
+ − 386
shows "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"
+ − 387
apply (auto simp add: Babs_def)
+ − 388
apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
+ − 389
using a apply (simp add: Babs_def)
+ − 390
apply (simp add: in_respects)
+ − 391
using Quotient_rel[OF q]
+ − 392
by metis
+ − 393
607
+ − 394
lemma babs_prs:
+ − 395
assumes q1: "Quotient R1 Abs1 Rep1"
+ − 396
and q2: "Quotient R2 Abs2 Rep2"
927
+ − 397
shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f"
+ − 398
apply (rule ext)
+ − 399
apply (simp)
607
+ − 400
apply (subgoal_tac "Rep1 x \<in> Respects R1")
+ − 401
apply (simp add: Babs_def Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+ − 402
apply (simp add: in_respects Quotient_rel_rep[OF q1])
+ − 403
done
+ − 404
696
fd718dde1d61
Simplification of Babses for regularize; will probably become injection
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 405
lemma babs_simp:
fd718dde1d61
Simplification of Babses for regularize; will probably become injection
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 406
assumes q: "Quotient R1 Abs Rep"
fd718dde1d61
Simplification of Babses for regularize; will probably become injection
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 407
shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)"
721
+ − 408
apply(rule iffI)
+ − 409
apply(simp_all only: babs_rsp[OF q])
+ − 410
apply(auto simp add: Babs_def)
+ − 411
apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
+ − 412
apply(metis Babs_def)
+ − 413
apply (simp add: in_respects)
+ − 414
using Quotient_rel[OF q]
+ − 415
by metis
696
fd718dde1d61
Simplification of Babses for regularize; will probably become injection
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 416
841
+ − 417
(* If a user proves that a particular functional relation
+ − 418
is an equivalence this may be useful in regularising *)
605
120e479ed367
first attempt to deal with Babs in regularise and cleaning (not yet working)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 419
lemma babs_reg_eqv:
120e479ed367
first attempt to deal with Babs in regularise and cleaning (not yet working)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 420
shows "equivp R \<Longrightarrow> Babs (Respects R) P = P"
721
+ − 421
by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp)
605
120e479ed367
first attempt to deal with Babs in regularise and cleaning (not yet working)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 422
921
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 423
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 424
(* 3 lemmas needed for proving repabs_inj *)
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 425
lemma ball_rsp:
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 426
assumes a: "(R ===> (op =)) f g"
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 427
shows "Ball (Respects R) f = Ball (Respects R) g"
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 428
using a by (simp add: Ball_def in_respects)
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 429
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 430
lemma bex_rsp:
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 431
assumes a: "(R ===> (op =)) f g"
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 432
shows "(Bex (Respects R) f = Bex (Respects R) g)"
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 433
using a by (simp add: Bex_def in_respects)
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 434
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 435
lemma bex1_rsp:
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 436
assumes a: "(R ===> (op =)) f g"
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 437
shows "(Bex1 (Respects R) f = Bex1 (Respects R) g)"
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 438
using a
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 439
by (simp add: Ex1_def Bex1_def in_respects) auto
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 440
913
+ − 441
(* 3 lemmas needed for cleaning of quantifiers *)
458
+ − 442
lemma all_prs:
528
+ − 443
assumes a: "Quotient R absf repf"
458
+ − 444
shows "Ball (Respects R) ((absf ---> id) f) = All f"
913
+ − 445
using a unfolding Quotient_def Ball_def in_respects fun_map_def id_apply
+ − 446
by metis
162
+ − 447
458
+ − 448
lemma ex_prs:
528
+ − 449
assumes a: "Quotient R absf repf"
458
+ − 450
shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
913
+ − 451
using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply
+ − 452
by metis
171
13aab4c59096
More infrastructure for automatic lifting of theorems lifted before
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 453
921
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 454
section {* Bexeq quantifier *}
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 455
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 456
definition
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 457
Bexeq :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 458
where
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 459
"Bexeq R P \<equiv> (\<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)))"
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 460
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 461
(* TODO/FIXME: simplify the repetitions in this proof *)
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 462
lemma bexeq_rsp:
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 463
assumes a: "Quotient R absf repf"
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 464
shows "((R ===> op =) ===> op =) (Bexeq R) (Bexeq R)"
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 465
apply simp
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 466
unfolding Bexeq_def
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 467
apply rule
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 468
apply rule
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 469
apply rule
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 470
apply rule
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 471
apply (erule conjE)+
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 472
apply (erule bexE)
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 473
apply rule
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 474
apply (rule_tac x="xa" in bexI)
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 475
apply metis
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 476
apply metis
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 477
apply rule+
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 478
apply (erule_tac x="xb" in ballE)
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 479
prefer 2
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 480
apply (metis)
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 481
apply (erule_tac x="ya" in ballE)
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 482
prefer 2
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 483
apply (metis)
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 484
apply (metis in_respects)
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 485
apply (erule conjE)+
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 486
apply (erule bexE)
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 487
apply rule
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 488
apply (rule_tac x="xa" in bexI)
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 489
apply metis
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 490
apply metis
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 491
apply rule+
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 492
apply (erule_tac x="xb" in ballE)
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 493
prefer 2
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 494
apply (metis)
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 495
apply (erule_tac x="ya" in ballE)
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 496
prefer 2
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 497
apply (metis)
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 498
apply (metis in_respects)
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 499
done
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 500
908
+ − 501
lemma ex1_prs:
+ − 502
assumes a: "Quotient R absf repf"
910
+ − 503
shows "((absf ---> id) ---> id) (Bexeq R) f = Ex1 f"
+ − 504
apply simp
908
+ − 505
apply (subst Bexeq_def)
+ − 506
apply (subst Bex_def)
+ − 507
apply (subst Ex1_def)
+ − 508
apply simp
+ − 509
apply rule
+ − 510
apply (erule conjE)+
+ − 511
apply (erule_tac exE)
+ − 512
apply (erule conjE)
+ − 513
apply (subgoal_tac "\<forall>y. R y y \<longrightarrow> f (absf y) \<longrightarrow> R x y")
+ − 514
apply (rule_tac x="absf x" in exI)
+ − 515
apply (thin_tac "\<forall>x\<in>Respects R. \<forall>y\<in>Respects R. f (absf x) \<and> f (absf y) \<longrightarrow> R x y")
+ − 516
apply (simp)
+ − 517
apply rule+
+ − 518
using a unfolding Quotient_def
+ − 519
apply metis
+ − 520
apply rule+
+ − 521
apply (erule_tac x="x" in ballE)
+ − 522
apply (erule_tac x="y" in ballE)
+ − 523
apply simp
+ − 524
apply (simp add: in_respects)
+ − 525
apply (simp add: in_respects)
+ − 526
apply (erule_tac exE)
+ − 527
apply rule
+ − 528
apply (rule_tac x="repf x" in exI)
+ − 529
apply (simp only: in_respects)
+ − 530
apply rule
+ − 531
apply (metis Quotient_rel_rep[OF a])
+ − 532
using a unfolding Quotient_def apply (simp)
+ − 533
apply rule+
+ − 534
using a unfolding Quotient_def in_respects
+ − 535
apply metis
+ − 536
done
+ − 537
946
+ − 538
lemma bex1_bexeq_reg: "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bexeq R (\<lambda>x. P x))"
+ − 539
apply (simp add: Bex1_def Ex1_def Bexeq_def in_respects)
+ − 540
apply clarify
+ − 541
apply auto
+ − 542
apply (rule bexI)
+ − 543
apply assumption
+ − 544
apply (simp add: in_respects)
+ − 545
apply (simp add: in_respects)
+ − 546
apply auto
+ − 547
done
+ − 548
921
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 549
section {* Various respects and preserve lemmas *}
697
+ − 550
554
+ − 551
lemma quot_rel_rsp:
+ − 552
assumes a: "Quotient R Abs Rep"
+ − 553
shows "(R ===> R ===> op =) R R"
+ − 554
apply(rule fun_rel_id)+
+ − 555
apply(rule equals_rsp[OF a])
+ − 556
apply(assumption)+
+ − 557
done
+ − 558
721
+ − 559
lemma o_prs:
+ − 560
assumes q1: "Quotient R1 Abs1 Rep1"
+ − 561
and q2: "Quotient R2 Abs2 Rep2"
+ − 562
and q3: "Quotient R3 Abs3 Rep3"
+ − 563
shows "(Rep1 ---> Abs3) (((Abs2 ---> Rep3) f) o ((Abs1 ---> Rep2) g)) = f o g"
+ − 564
using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3]
+ − 565
unfolding o_def expand_fun_eq by simp
541
+ − 566
721
+ − 567
lemma o_rsp:
+ − 568
assumes q1: "Quotient R1 Abs1 Rep1"
+ − 569
and q2: "Quotient R2 Abs2 Rep2"
+ − 570
and q3: "Quotient R3 Abs3 Rep3"
+ − 571
and a1: "(R2 ===> R3) f1 f2"
+ − 572
and a2: "(R1 ===> R2) g1 g2"
+ − 573
shows "(R1 ===> R3) (f1 o g1) (f2 o g2)"
+ − 574
using a1 a2 unfolding o_def expand_fun_eq
+ − 575
by (auto)
+ − 576
+ − 577
lemma cond_prs:
+ − 578
assumes a: "Quotient R absf repf"
+ − 579
shows "absf (if a then repf b else repf c) = (if a then b else c)"
+ − 580
using a unfolding Quotient_def by auto
+ − 581
+ − 582
lemma if_prs:
+ − 583
assumes q: "Quotient R Abs Rep"
+ − 584
shows "Abs (If a (Rep b) (Rep c)) = If a b c"
+ − 585
using Quotient_abs_rep[OF q] by auto
+ − 586
+ − 587
(* q not used *)
+ − 588
lemma if_rsp:
+ − 589
assumes q: "Quotient R Abs Rep"
+ − 590
and a: "a1 = a2" "R b1 b2" "R c1 c2"
+ − 591
shows "R (If a1 b1 c1) (If a2 b2 c2)"
+ − 592
using a by auto
+ − 593
+ − 594
lemma let_prs:
+ − 595
assumes q1: "Quotient R1 Abs1 Rep1"
+ − 596
and q2: "Quotient R2 Abs2 Rep2"
+ − 597
shows "Abs2 (Let (Rep1 x) ((Abs1 ---> Rep2) f)) = Let x f"
+ − 598
using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] by auto
+ − 599
+ − 600
lemma let_rsp:
+ − 601
assumes q1: "Quotient R1 Abs1 Rep1"
+ − 602
and a1: "(R1 ===> R2) f g"
+ − 603
and a2: "R1 x y"
+ − 604
shows "R2 ((Let x f)::'c) ((Let y g)::'c)"
+ − 605
using apply_rsp[OF q1 a1] a2 by auto
543
+ − 606
+ − 607
+ − 608
(******************************************)
+ − 609
(* REST OF THE FILE IS UNUSED (until now) *)
+ − 610
(******************************************)
656
c86a47d4966e
Temporarily repeated fun_map_tac 4 times. Cleaning for all examples work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 611
921
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 612
text {*
542
+ − 613
lemma in_fun:
+ − 614
shows "x \<in> ((f ---> g) s) = g (f x \<in> s)"
721
+ − 615
by (simp add: mem_def)
921
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 616
721
+ − 617
lemma respects_thm:
542
+ − 618
shows "Respects (R1 ===> R2) f = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (f y))"
721
+ − 619
unfolding Respects_def
+ − 620
by (simp add: expand_fun_eq)
542
+ − 621
721
+ − 622
lemma respects_rep_abs:
542
+ − 623
assumes a: "Quotient R1 Abs1 Rep1"
+ − 624
and b: "Respects (R1 ===> R2) f"
+ − 625
and c: "R1 x x"
+ − 626
shows "R2 (f (Rep1 (Abs1 x))) (f x)"
721
+ − 627
using a b[simplified respects_thm] c unfolding Quotient_def
+ − 628
by blast
542
+ − 629
721
+ − 630
lemma respects_mp:
542
+ − 631
assumes a: "Respects (R1 ===> R2) f"
+ − 632
and b: "R1 x y"
+ − 633
shows "R2 (f x) (f y)"
721
+ − 634
using a b unfolding Respects_def
+ − 635
by simp
542
+ − 636
721
+ − 637
lemma respects_o:
542
+ − 638
assumes a: "Respects (R2 ===> R3) f"
+ − 639
and b: "Respects (R1 ===> R2) g"
+ − 640
shows "Respects (R1 ===> R3) (f o g)"
721
+ − 641
using a b unfolding Respects_def
+ − 642
by simp
542
+ − 643
721
+ − 644
lemma fun_rel_eq_rel:
542
+ − 645
assumes q1: "Quotient R1 Abs1 Rep1"
+ − 646
and q2: "Quotient R2 Abs2 Rep2"
721
+ − 647
shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \<and> (Respects (R1 ===> R2) g)
542
+ − 648
\<and> ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))"
721
+ − 649
using fun_quotient[OF q1 q2] unfolding Respects_def Quotient_def expand_fun_eq
+ − 650
by blast
542
+ − 651
721
+ − 652
lemma let_babs:
+ − 653
"v \<in> r \<Longrightarrow> Let v (Babs r lam) = Let v lam"
+ − 654
by (simp add: Babs_def)
542
+ − 655
721
+ − 656
lemma fun_rel_equals:
542
+ − 657
assumes q1: "Quotient R1 Abs1 Rep1"
+ − 658
and q2: "Quotient R2 Abs2 Rep2"
+ − 659
and r1: "Respects (R1 ===> R2) f"
+ − 660
and r2: "Respects (R1 ===> R2) g"
+ − 661
shows "((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g) = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
721
+ − 662
apply(rule_tac iffI)
913
+ − 663
apply(rule)+
+ − 664
apply (rule apply_rsp'[of "R1" "R2"])
+ − 665
apply(subst Quotient_rel[OF fun_quotient[OF q1 q2]])
+ − 666
apply auto
721
+ − 667
using fun_quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def
913
+ − 668
apply (metis let_rsp q1)
+ − 669
apply (metis fun_rel_eq_rel let_rsp q1 q2 r2)
721
+ − 670
using r1 unfolding Respects_def expand_fun_eq
+ − 671
apply(simp (no_asm_use))
+ − 672
apply(metis Quotient_rel[OF q2] Quotient_rel_rep[OF q1])
+ − 673
done
542
+ − 674
+ − 675
(* ask Peter: fun_rel_IMP used twice *)
+ − 676
lemma fun_rel_IMP2:
+ − 677
assumes q1: "Quotient R1 Abs1 Rep1"
+ − 678
and q2: "Quotient R2 Abs2 Rep2"
+ − 679
and r1: "Respects (R1 ===> R2) f"
+ − 680
and r2: "Respects (R1 ===> R2) g"
+ − 681
and a: "(Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g"
+ − 682
shows "R1 x y \<Longrightarrow> R2 (f x) (g y)"
721
+ − 683
using q1 q2 r1 r2 a
+ − 684
by (simp add: fun_rel_equals)
542
+ − 685
721
+ − 686
lemma lambda_rep_abs_rsp:
542
+ − 687
assumes r1: "\<And>r r'. R1 r r' \<Longrightarrow>R1 r (Rep1 (Abs1 r'))"
+ − 688
and r2: "\<And>r r'. R2 r r' \<Longrightarrow>R2 r (Rep2 (Abs2 r'))"
+ − 689
shows "(R1 ===> R2) f1 f2 \<Longrightarrow> (R1 ===> R2) f1 ((Abs1 ---> Rep2) ((Rep1 ---> Abs2) f2))"
721
+ − 690
using r1 r2 by auto
543
+ − 691
+ − 692
(* ask peter what are literal_case *)
+ − 693
(* literal_case_PRS *)
+ − 694
(* literal_case_RSP *)
721
+ − 695
(* Cez: !f x. literal_case f x = f x *)
543
+ − 696
+ − 697
(* We use id_simps which includes id_apply; so these 2 theorems can be removed *)
721
+ − 698
lemma id_prs:
543
+ − 699
assumes q: "Quotient R Abs Rep"
721
+ − 700
shows "Abs (id (Rep e)) = id e"
+ − 701
using Quotient_abs_rep[OF q] by auto
543
+ − 702
721
+ − 703
lemma id_rsp:
543
+ − 704
assumes q: "Quotient R Abs Rep"
+ − 705
and a: "R e1 e2"
+ − 706
shows "R (id e1) (id e2)"
721
+ − 707
using a by auto
543
+ − 708
921
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 709
*}
dae038c8cd69
properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 710
93
+ − 711
end
95
+ − 712