163
+ − 1
theory FSet
+ − 2
imports QuotMain
+ − 3
begin
+ − 4
+ − 5
inductive
+ − 6
list_eq (infix "\<approx>" 50)
+ − 7
where
+ − 8
"a#b#xs \<approx> b#a#xs"
+ − 9
| "[] \<approx> []"
+ − 10
| "xs \<approx> ys \<Longrightarrow> ys \<approx> xs"
+ − 11
| "a#a#xs \<approx> a#xs"
+ − 12
| "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys"
+ − 13
| "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3"
+ − 14
+ − 15
lemma list_eq_refl:
+ − 16
shows "xs \<approx> xs"
451
586e3dc4afdb
Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 17
by (induct xs) (auto intro: list_eq.intros)
163
+ − 18
+ − 19
lemma equiv_list_eq:
+ − 20
shows "EQUIV list_eq"
+ − 21
unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def
+ − 22
apply(auto intro: list_eq.intros list_eq_refl)
+ − 23
done
+ − 24
+ − 25
quotient fset = "'a list" / "list_eq"
+ − 26
apply(rule equiv_list_eq)
+ − 27
done
+ − 28
+ − 29
print_theorems
+ − 30
+ − 31
typ "'a fset"
+ − 32
thm "Rep_fset"
+ − 33
thm "ABS_fset_def"
+ − 34
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 35
quotient_def
231
c643938b846a
updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 36
EMPTY :: "'a fset"
c643938b846a
updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 37
where
c643938b846a
updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 38
"EMPTY \<equiv> ([]::'a list)"
163
+ − 39
+ − 40
term Nil
+ − 41
term EMPTY
+ − 42
thm EMPTY_def
+ − 43
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 44
quotient_def
254
+ − 45
INSERT :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
231
c643938b846a
updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 46
where
c643938b846a
updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 47
"INSERT \<equiv> op #"
163
+ − 48
+ − 49
term Cons
+ − 50
term INSERT
+ − 51
thm INSERT_def
+ − 52
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 53
quotient_def
231
c643938b846a
updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 54
FUNION :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
c643938b846a
updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 55
where
c643938b846a
updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 56
"FUNION \<equiv> (op @)"
163
+ − 57
+ − 58
term append
231
c643938b846a
updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 59
term FUNION
c643938b846a
updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 60
thm FUNION_def
163
+ − 61
+ − 62
thm QUOTIENT_fset
+ − 63
+ − 64
thm QUOT_TYPE_I_fset.thm11
+ − 65
+ − 66
+ − 67
fun
+ − 68
membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infix "memb" 100)
+ − 69
where
+ − 70
m1: "(x memb []) = False"
+ − 71
| m2: "(x memb (y#xs)) = ((x=y) \<or> (x memb xs))"
+ − 72
+ − 73
fun
+ − 74
card1 :: "'a list \<Rightarrow> nat"
+ − 75
where
+ − 76
card1_nil: "(card1 []) = 0"
+ − 77
| card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))"
+ − 78
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 79
quotient_def
231
c643938b846a
updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 80
CARD :: "'a fset \<Rightarrow> nat"
c643938b846a
updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 81
where
c643938b846a
updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 82
"CARD \<equiv> card1"
163
+ − 83
+ − 84
term card1
231
c643938b846a
updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 85
term CARD
c643938b846a
updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 86
thm CARD_def
163
+ − 87
+ − 88
(* text {*
+ − 89
Maybe make_const_def should require a theorem that says that the particular lifted function
+ − 90
respects the relation. With it such a definition would be impossible:
+ − 91
make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+ − 92
*}*)
+ − 93
+ − 94
lemma card1_0:
+ − 95
fixes a :: "'a list"
+ − 96
shows "(card1 a = 0) = (a = [])"
214
+ − 97
by (induct a) auto
163
+ − 98
+ − 99
lemma not_mem_card1:
+ − 100
fixes x :: "'a"
+ − 101
fixes xs :: "'a list"
309
+ − 102
shows "(~(x memb xs)) = (card1 (x # xs) = Suc (card1 xs))"
+ − 103
by auto
163
+ − 104
+ − 105
lemma mem_cons:
+ − 106
fixes x :: "'a"
+ − 107
fixes xs :: "'a list"
+ − 108
assumes a : "x memb xs"
+ − 109
shows "x # xs \<approx> xs"
214
+ − 110
using a by (induct xs) (auto intro: list_eq.intros )
163
+ − 111
+ − 112
lemma card1_suc:
+ − 113
fixes xs :: "'a list"
+ − 114
fixes n :: "nat"
+ − 115
assumes c: "card1 xs = Suc n"
+ − 116
shows "\<exists>a ys. ~(a memb ys) \<and> xs \<approx> (a # ys)"
+ − 117
using c
+ − 118
apply(induct xs)
+ − 119
apply (metis Suc_neq_Zero card1_0)
+ − 120
apply (metis QUOT_TYPE_I_fset.R_trans card1_cons list_eq_refl mem_cons)
+ − 121
done
+ − 122
294
+ − 123
definition
+ − 124
rsp_fold
+ − 125
where
+ − 126
"rsp_fold f = ((!u v. (f u v = f v u)) \<and> (!u v w. ((f u (f v w) = f (f u v) w))))"
+ − 127
163
+ − 128
primrec
+ − 129
fold1
+ − 130
where
+ − 131
"fold1 f (g :: 'a \<Rightarrow> 'b) (z :: 'b) [] = z"
+ − 132
| "fold1 f g z (a # A) =
294
+ − 133
(if rsp_fold f
163
+ − 134
then (
+ − 135
if (a memb A) then (fold1 f g z A) else (f (g a) (fold1 f g z A))
+ − 136
) else z)"
+ − 137
+ − 138
(* fold1_def is not usable, but: *)
+ − 139
thm fold1.simps
+ − 140
+ − 141
lemma fs1_strong_cases:
+ − 142
fixes X :: "'a list"
+ − 143
shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a memb Y) \<and> (X \<approx> a # Y)))"
+ − 144
apply (induct X)
+ − 145
apply (simp)
+ − 146
apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons m1)
+ − 147
done
+ − 148
296
+ − 149
quotient_def
231
c643938b846a
updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 150
IN :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool"
c643938b846a
updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 151
where
c643938b846a
updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 152
"IN \<equiv> membship"
163
+ − 153
+ − 154
term membship
+ − 155
term IN
+ − 156
thm IN_def
+ − 157
274
+ − 158
term fold1
+ − 159
quotient_def
+ − 160
FOLD :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a"
231
c643938b846a
updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 161
where
c643938b846a
updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 162
"FOLD \<equiv> fold1"
194
+ − 163
+ − 164
term fold1
+ − 165
term fold
+ − 166
thm fold_def
+ − 167
268
4d58c02289ca
simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 168
quotient_def
254
+ − 169
fmap::"('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
225
+ − 170
where
254
+ − 171
"fmap \<equiv> map"
194
+ − 172
+ − 173
term map
+ − 174
term fmap
+ − 175
thm fmap_def
+ − 176
274
+ − 177
ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def FOLD_def} *}
163
+ − 178
451
586e3dc4afdb
Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 179
lemma memb_rsp:
163
+ − 180
fixes z
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 181
assumes a: "x \<approx> y"
163
+ − 182
shows "(z memb x) = (z memb y)"
+ − 183
using a by induct auto
+ − 184
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 185
lemma ho_memb_rsp[quot_rsp]:
164
+ − 186
"(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)"
214
+ − 187
by (simp add: memb_rsp)
164
+ − 188
451
586e3dc4afdb
Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 189
lemma card1_rsp:
163
+ − 190
fixes a b :: "'a list"
+ − 191
assumes e: "a \<approx> b"
+ − 192
shows "card1 a = card1 b"
214
+ − 193
using e by induct (simp_all add:memb_rsp)
163
+ − 194
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 195
lemma ho_card1_rsp[quot_rsp]:
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 196
"(op \<approx> ===> op =) card1 card1"
214
+ − 197
by (simp add: card1_rsp)
171
13aab4c59096
More infrastructure for automatic lifting of theorems lifted before
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 198
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 199
lemma cons_rsp[quot_rsp]:
163
+ − 200
fixes z
+ − 201
assumes a: "xs \<approx> ys"
+ − 202
shows "(z # xs) \<approx> (z # ys)"
+ − 203
using a by (rule list_eq.intros(5))
+ − 204
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 205
lemma ho_cons_rsp[quot_rsp]:
228
+ − 206
"(op = ===> op \<approx> ===> op \<approx>) op # op #"
214
+ − 207
by (simp add: cons_rsp)
164
+ − 208
175
+ − 209
lemma append_rsp_fst:
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 210
assumes a : "l1 \<approx> l2"
214
+ − 211
shows "(l1 @ s) \<approx> (l2 @ s)"
163
+ − 212
using a
214
+ − 213
by (induct) (auto intro: list_eq.intros list_eq_refl)
+ − 214
+ − 215
lemma append_end:
+ − 216
shows "(e # l) \<approx> (l @ [e])"
+ − 217
apply (induct l)
+ − 218
apply (auto intro: list_eq.intros list_eq_refl)
+ − 219
done
+ − 220
+ − 221
lemma rev_rsp:
+ − 222
shows "a \<approx> rev a"
+ − 223
apply (induct a)
+ − 224
apply simp
+ − 225
apply (rule list_eq_refl)
+ − 226
apply simp_all
+ − 227
apply (rule list_eq.intros(6))
+ − 228
prefer 2
+ − 229
apply (rule append_rsp_fst)
+ − 230
apply assumption
+ − 231
apply (rule append_end)
+ − 232
done
163
+ − 233
214
+ − 234
lemma append_sym_rsp:
+ − 235
shows "(a @ b) \<approx> (b @ a)"
+ − 236
apply (rule list_eq.intros(6))
+ − 237
apply (rule append_rsp_fst)
+ − 238
apply (rule rev_rsp)
+ − 239
apply (rule list_eq.intros(6))
+ − 240
apply (rule rev_rsp)
+ − 241
apply (simp)
+ − 242
apply (rule append_rsp_fst)
+ − 243
apply (rule list_eq.intros(3))
+ − 244
apply (rule rev_rsp)
+ − 245
done
+ − 246
451
586e3dc4afdb
Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 247
lemma append_rsp:
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 248
assumes a : "l1 \<approx> r1"
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 249
assumes b : "l2 \<approx> r2 "
214
+ − 250
shows "(l1 @ l2) \<approx> (r1 @ r2)"
+ − 251
apply (rule list_eq.intros(6))
+ − 252
apply (rule append_rsp_fst)
+ − 253
using a apply (assumption)
+ − 254
apply (rule list_eq.intros(6))
+ − 255
apply (rule append_sym_rsp)
+ − 256
apply (rule list_eq.intros(6))
+ − 257
apply (rule append_rsp_fst)
+ − 258
using b apply (assumption)
+ − 259
apply (rule append_sym_rsp)
+ − 260
done
175
+ − 261
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 262
lemma ho_append_rsp[quot_rsp]:
228
+ − 263
"(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
214
+ − 264
by (simp add: append_rsp)
175
+ − 265
451
586e3dc4afdb
Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 266
lemma map_rsp:
194
+ − 267
assumes a: "a \<approx> b"
+ − 268
shows "map f a \<approx> map f b"
+ − 269
using a
+ − 270
apply (induct)
+ − 271
apply(auto intro: list_eq.intros)
+ − 272
done
+ − 273
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 274
lemma ho_map_rsp[quot_rsp]:
294
+ − 275
"(op = ===> op \<approx> ===> op \<approx>) map map"
+ − 276
by (simp add: map_rsp)
194
+ − 277
294
+ − 278
lemma map_append:
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 279
"(map f (a @ b)) \<approx> (map f a) @ (map f b)"
215
+ − 280
by simp (rule list_eq_refl)
194
+ − 281
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 282
lemma ho_fold_rsp[quot_rsp]:
294
+ − 283
"(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1"
292
+ − 284
apply (auto simp add: FUN_REL_EQ)
294
+ − 285
apply (case_tac "rsp_fold x")
+ − 286
prefer 2
+ − 287
apply (erule_tac list_eq.induct)
+ − 288
apply (simp_all)
+ − 289
apply (erule_tac list_eq.induct)
+ − 290
apply (simp_all)
+ − 291
apply (auto simp add: memb_rsp rsp_fold_def)
+ − 292
done
241
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 293
254
+ − 294
print_quotients
+ − 295
226
+ − 296
ML {* val qty = @{typ "'a fset"} *}
+ − 297
ML {* val rsp_thms =
458
+ − 298
@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} *}
206
+ − 299
364
+ − 300
ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
+ − 301
ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *}
+ − 302
ML {* val consts = lookup_quot_consts defs *}
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 303
ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *}
314
+ − 304
455
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 305
thm m1
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 306
364
+ − 307
lemma "IN x EMPTY = False"
455
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 308
apply(tactic {* procedure_tac @{context} @{thm m1} 1 *})
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 309
apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 310
apply(tactic {* all_inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
466
+ − 311
apply(tactic {* clean_tac @{context} [quot] defs 1*})
455
9cb45d022524
tried to improve the inj_repabs_trm function but left the new part commented out
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 312
done
353
9a0e8ab42ee8
fixed the error by a temporary fix (the data of the eqivalence relation should be only its name)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 313
364
+ − 314
lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"
+ − 315
by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *})
356
51aafebf4d06
Another theorem for which the new regularize differs from old one, so the goal is not proved. But it seems, that the new one is better.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 316
364
+ − 317
lemma "INSERT a (INSERT a x) = INSERT a x"
+ − 318
apply (tactic {* lift_tac_fset @{context} @{thm list_eq.intros(4)} 1 *})
+ − 319
done
+ − 320
367
+ − 321
lemma "x = xa \<Longrightarrow> INSERT a x = INSERT a xa"
364
+ − 322
apply (tactic {* lift_tac_fset @{context} @{thm list_eq.intros(5)} 1 *})
+ − 323
done
353
9a0e8ab42ee8
fixed the error by a temporary fix (the data of the eqivalence relation should be only its name)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 324
367
+ − 325
lemma "CARD x = Suc n \<Longrightarrow> (\<exists>a b. \<not> IN a b & x = INSERT a b)"
364
+ − 326
apply (tactic {* lift_tac_fset @{context} @{thm card1_suc} 1 *})
+ − 327
done
+ − 328
+ − 329
lemma "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))"
+ − 330
apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *})
+ − 331
done
356
51aafebf4d06
Another theorem for which the new regularize differs from old one, so the goal is not proved. But it seems, that the new one is better.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 332
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 333
ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}
442
7beed9b75ea2
renamed LAMBDA_RES_TAC and WEAK_LAMBDA_RES_TAC to lower case names
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 334
7beed9b75ea2
renamed LAMBDA_RES_TAC and WEAK_LAMBDA_RES_TAC to lower case names
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 335
lemma "FOLD f g (z::'b) (INSERT a x) =
364
+ − 336
(if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"
442
7beed9b75ea2
renamed LAMBDA_RES_TAC and WEAK_LAMBDA_RES_TAC to lower case names
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 337
apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
364
+ − 338
done
356
51aafebf4d06
Another theorem for which the new regularize differs from old one, so the goal is not proved. But it seems, that the new one is better.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 339
368
+ − 340
lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
+ − 341
apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
+ − 342
done
+ − 343
367
+ − 344
lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"
+ − 345
apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *})
+ − 346
done
+ − 347
390
+ − 348
lemma cheat: "P" sorry
+ − 349
376
+ − 350
lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
462
+ − 351
apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
+ − 352
ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
392
+ − 353
apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
432
+ − 354
apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
398
+ − 355
prefer 2
466
+ − 356
apply(tactic {* clean_tac @{context} [quot] defs 1 *})
445
+ − 357
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
+ − 358
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+ − 359
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
+ − 360
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
+ − 361
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+ − 362
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
+ − 363
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
+ − 364
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
+ − 365
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+ − 366
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+ − 367
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+ − 368
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+ − 369
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+ − 370
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* D *) (* reflexivity of basic relations *)
+ − 371
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
+ − 372
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
+ − 373
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+ − 374
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
+ − 375
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+ − 376
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* C *) (* = and extensionality *)
+ − 377
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
+ − 378
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+ − 379
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
+ − 380
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
+ − 381
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
+ − 382
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+ − 383
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+ − 384
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+ − 385
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+ − 386
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+ − 387
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+ − 388
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+ − 389
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+ − 390
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+ − 391
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+ − 392
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+ − 393
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+ − 394
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 7 *) (* respectfulness *)
+ − 395
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+ − 396
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+ − 397
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+ − 398
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+ − 399
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
414
+ − 400
done
390
+ − 401
273
+ − 402
quotient_def
276
+ − 403
fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
273
+ − 404
where
+ − 405
"fset_rec \<equiv> list_rec"
+ − 406
292
+ − 407
quotient_def
+ − 408
fset_case::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
+ − 409
where
+ − 410
"fset_case \<equiv> list_case"
+ − 411
296
+ − 412
(* Probably not true without additional assumptions about the function *)
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 413
lemma list_rec_rsp[quot_rsp]:
292
+ − 414
"(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec"
+ − 415
apply (auto simp add: FUN_REL_EQ)
296
+ − 416
apply (erule_tac list_eq.induct)
+ − 417
apply (simp_all)
292
+ − 418
sorry
289
7e8617f20b59
Remaining fixes for polymorphic types. map_append now lifts properly with 'a list and 'b list.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 419
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 420
lemma list_case_rsp[quot_rsp]:
292
+ − 421
"(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
+ − 422
apply (auto simp add: FUN_REL_EQ)
+ − 423
sorry
+ − 424
+ − 425
ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}
+ − 426
ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *}
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 427
ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *}
356
51aafebf4d06
Another theorem for which the new regularize differs from old one, so the goal is not proved. But it seems, that the new one is better.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 428
376
+ − 429
lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"
+ − 430
apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *})
+ − 431
done
+ − 432
+ − 433
lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa"
+ − 434
apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *})
+ − 435
done
348
+ − 436
304
+ − 437
lemma list_induct_part:
386
+ − 438
assumes a: "P (x :: 'a list) ([] :: 'c list)"
304
+ − 439
assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)"
+ − 440
shows "P x l"
+ − 441
apply (rule_tac P="P x" in list.induct)
+ − 442
apply (rule a)
+ − 443
apply (rule b)
+ − 444
apply (assumption)
+ − 445
done
273
+ − 446
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 447
ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}
292
+ − 448
379
+ − 449
(* Construction site starts here *)
386
+ − 450
lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
389
+ − 451
apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *})
432
+ − 452
apply (tactic {* regularize_tac @{context} [rel_eqv] 1 *})
462
+ − 453
prefer 2
466
+ − 454
apply (tactic {* clean_tac @{context} [quot] defs 1 *})
309
+ − 455
apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
+ − 456
apply (rule FUN_QUOTIENT)
+ − 457
apply (rule FUN_QUOTIENT)
+ − 458
apply (rule IDENTITY_QUOTIENT)
+ − 459
apply (rule FUN_QUOTIENT)
+ − 460
apply (rule QUOTIENT_fset)
+ − 461
apply (rule IDENTITY_QUOTIENT)
+ − 462
apply (rule IDENTITY_QUOTIENT)
+ − 463
apply (rule IDENTITY_QUOTIENT)
445
+ − 464
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 465
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 466
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 467
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 468
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
309
+ − 469
apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
+ − 470
apply (rule IDENTITY_QUOTIENT)
+ − 471
apply (rule IDENTITY_QUOTIENT)
445
+ − 472
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 473
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 474
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 475
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 476
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 477
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 478
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 479
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 480
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
452
7ba2c16fe0c8
Removed unnecessary HOL_ss which proved one of the subgoals.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 481
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
309
+ − 482
apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
+ − 483
apply (rule IDENTITY_QUOTIENT)
+ − 484
apply (rule FUN_QUOTIENT)
+ − 485
apply (rule QUOTIENT_fset)
+ − 486
apply (rule IDENTITY_QUOTIENT)
445
+ − 487
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 488
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 489
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 490
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 491
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 492
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 493
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 494
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 495
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 496
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 497
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 498
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 499
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 500
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 501
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 502
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 503
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 504
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
317
+ − 505
apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
459
+ − 506
apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
317
+ − 507
apply assumption
+ − 508
apply (rule refl)
445
+ − 509
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 510
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
317
+ − 511
apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
+ − 512
apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
459
+ − 513
apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
445
+ − 514
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 515
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 516
apply (tactic {* REPEAT_ALL_NEW (inj_repabs_tac_fset @{context}) 1 *})
+ − 517
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
317
+ − 518
apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
459
+ − 519
apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
445
+ − 520
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 521
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 522
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+ − 523
apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
309
+ − 524
done
+ − 525
163
+ − 526
end