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"
+ − 17
apply (induct xs)
+ − 18
apply (auto intro: list_eq.intros)
+ − 19
done
+ − 20
+ − 21
lemma equiv_list_eq:
+ − 22
shows "EQUIV list_eq"
+ − 23
unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def
+ − 24
apply(auto intro: list_eq.intros list_eq_refl)
+ − 25
done
+ − 26
+ − 27
quotient fset = "'a list" / "list_eq"
+ − 28
apply(rule equiv_list_eq)
+ − 29
done
+ − 30
+ − 31
print_theorems
+ − 32
+ − 33
typ "'a fset"
+ − 34
thm "Rep_fset"
+ − 35
thm "ABS_fset_def"
+ − 36
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
+ − 37
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
+ − 38
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
+ − 39
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
+ − 40
"EMPTY \<equiv> ([]::'a list)"
163
+ − 41
+ − 42
term Nil
+ − 43
term EMPTY
+ − 44
thm EMPTY_def
+ − 45
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
+ − 46
quotient_def
254
+ − 47
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
+ − 48
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
+ − 49
"INSERT \<equiv> op #"
163
+ − 50
+ − 51
term Cons
+ − 52
term INSERT
+ − 53
thm INSERT_def
+ − 54
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
+ − 55
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
+ − 56
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
+ − 57
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
+ − 58
"FUNION \<equiv> (op @)"
163
+ − 59
+ − 60
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
+ − 61
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
+ − 62
thm FUNION_def
163
+ − 63
+ − 64
thm QUOTIENT_fset
+ − 65
+ − 66
thm QUOT_TYPE_I_fset.thm11
+ − 67
+ − 68
+ − 69
fun
+ − 70
membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infix "memb" 100)
+ − 71
where
+ − 72
m1: "(x memb []) = False"
+ − 73
| m2: "(x memb (y#xs)) = ((x=y) \<or> (x memb xs))"
+ − 74
+ − 75
fun
+ − 76
card1 :: "'a list \<Rightarrow> nat"
+ − 77
where
+ − 78
card1_nil: "(card1 []) = 0"
+ − 79
| card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))"
+ − 80
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
+ − 81
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
+ − 82
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
+ − 83
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
+ − 84
"CARD \<equiv> card1"
163
+ − 85
+ − 86
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
+ − 87
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
+ − 88
thm CARD_def
163
+ − 89
+ − 90
(* text {*
+ − 91
Maybe make_const_def should require a theorem that says that the particular lifted function
+ − 92
respects the relation. With it such a definition would be impossible:
+ − 93
make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+ − 94
*}*)
+ − 95
+ − 96
lemma card1_0:
+ − 97
fixes a :: "'a list"
+ − 98
shows "(card1 a = 0) = (a = [])"
214
+ − 99
by (induct a) auto
163
+ − 100
+ − 101
lemma not_mem_card1:
+ − 102
fixes x :: "'a"
+ − 103
fixes xs :: "'a list"
309
+ − 104
shows "(~(x memb xs)) = (card1 (x # xs) = Suc (card1 xs))"
+ − 105
by auto
163
+ − 106
+ − 107
lemma mem_cons:
+ − 108
fixes x :: "'a"
+ − 109
fixes xs :: "'a list"
+ − 110
assumes a : "x memb xs"
+ − 111
shows "x # xs \<approx> xs"
214
+ − 112
using a by (induct xs) (auto intro: list_eq.intros )
163
+ − 113
+ − 114
lemma card1_suc:
+ − 115
fixes xs :: "'a list"
+ − 116
fixes n :: "nat"
+ − 117
assumes c: "card1 xs = Suc n"
+ − 118
shows "\<exists>a ys. ~(a memb ys) \<and> xs \<approx> (a # ys)"
+ − 119
using c
+ − 120
apply(induct xs)
+ − 121
apply (metis Suc_neq_Zero card1_0)
+ − 122
apply (metis QUOT_TYPE_I_fset.R_trans card1_cons list_eq_refl mem_cons)
+ − 123
done
+ − 124
294
+ − 125
definition
+ − 126
rsp_fold
+ − 127
where
+ − 128
"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))))"
+ − 129
163
+ − 130
primrec
+ − 131
fold1
+ − 132
where
+ − 133
"fold1 f (g :: 'a \<Rightarrow> 'b) (z :: 'b) [] = z"
+ − 134
| "fold1 f g z (a # A) =
294
+ − 135
(if rsp_fold f
163
+ − 136
then (
+ − 137
if (a memb A) then (fold1 f g z A) else (f (g a) (fold1 f g z A))
+ − 138
) else z)"
+ − 139
+ − 140
(* fold1_def is not usable, but: *)
+ − 141
thm fold1.simps
+ − 142
+ − 143
lemma fs1_strong_cases:
+ − 144
fixes X :: "'a list"
+ − 145
shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a memb Y) \<and> (X \<approx> a # Y)))"
+ − 146
apply (induct X)
+ − 147
apply (simp)
+ − 148
apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons m1)
+ − 149
done
+ − 150
296
+ − 151
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
+ − 152
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
+ − 153
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
+ − 154
"IN \<equiv> membship"
163
+ − 155
+ − 156
term membship
+ − 157
term IN
+ − 158
thm IN_def
+ − 159
274
+ − 160
term fold1
+ − 161
quotient_def
+ − 162
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
+ − 163
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
+ − 164
"FOLD \<equiv> fold1"
194
+ − 165
+ − 166
term fold1
+ − 167
term fold
+ − 168
thm fold_def
+ − 169
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
+ − 170
quotient_def
254
+ − 171
fmap::"('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
225
+ − 172
where
254
+ − 173
"fmap \<equiv> map"
194
+ − 174
+ − 175
term map
+ − 176
term fmap
+ − 177
thm fmap_def
+ − 178
274
+ − 179
ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def FOLD_def} *}
163
+ − 180
164
+ − 181
lemma memb_rsp:
163
+ − 182
fixes z
+ − 183
assumes a: "list_eq x y"
+ − 184
shows "(z memb x) = (z memb y)"
+ − 185
using a by induct auto
+ − 186
164
+ − 187
lemma ho_memb_rsp:
+ − 188
"(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)"
214
+ − 189
by (simp add: memb_rsp)
164
+ − 190
163
+ − 191
lemma card1_rsp:
+ − 192
fixes a b :: "'a list"
+ − 193
assumes e: "a \<approx> b"
+ − 194
shows "card1 a = card1 b"
214
+ − 195
using e by induct (simp_all add:memb_rsp)
163
+ − 196
228
+ − 197
lemma ho_card1_rsp: "(op \<approx> ===> op =) card1 card1"
214
+ − 198
by (simp add: card1_rsp)
171
13aab4c59096
More infrastructure for automatic lifting of theorems lifted before
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 199
164
+ − 200
lemma cons_rsp:
163
+ − 201
fixes z
+ − 202
assumes a: "xs \<approx> ys"
+ − 203
shows "(z # xs) \<approx> (z # ys)"
+ − 204
using a by (rule list_eq.intros(5))
+ − 205
164
+ − 206
lemma ho_cons_rsp:
228
+ − 207
"(op = ===> op \<approx> ===> op \<approx>) op # op #"
214
+ − 208
by (simp add: cons_rsp)
164
+ − 209
175
+ − 210
lemma append_rsp_fst:
163
+ − 211
assumes a : "list_eq l1 l2"
214
+ − 212
shows "(l1 @ s) \<approx> (l2 @ s)"
163
+ − 213
using a
214
+ − 214
by (induct) (auto intro: list_eq.intros list_eq_refl)
+ − 215
+ − 216
lemma append_end:
+ − 217
shows "(e # l) \<approx> (l @ [e])"
+ − 218
apply (induct l)
+ − 219
apply (auto intro: list_eq.intros list_eq_refl)
+ − 220
done
+ − 221
+ − 222
lemma rev_rsp:
+ − 223
shows "a \<approx> rev a"
+ − 224
apply (induct a)
+ − 225
apply simp
+ − 226
apply (rule list_eq_refl)
+ − 227
apply simp_all
+ − 228
apply (rule list_eq.intros(6))
+ − 229
prefer 2
+ − 230
apply (rule append_rsp_fst)
+ − 231
apply assumption
+ − 232
apply (rule append_end)
+ − 233
done
163
+ − 234
214
+ − 235
lemma append_sym_rsp:
+ − 236
shows "(a @ b) \<approx> (b @ a)"
+ − 237
apply (rule list_eq.intros(6))
+ − 238
apply (rule append_rsp_fst)
+ − 239
apply (rule rev_rsp)
+ − 240
apply (rule list_eq.intros(6))
+ − 241
apply (rule rev_rsp)
+ − 242
apply (simp)
+ − 243
apply (rule append_rsp_fst)
+ − 244
apply (rule list_eq.intros(3))
+ − 245
apply (rule rev_rsp)
+ − 246
done
+ − 247
+ − 248
lemma append_rsp:
+ − 249
assumes a : "list_eq l1 r1"
+ − 250
assumes b : "list_eq l2 r2 "
+ − 251
shows "(l1 @ l2) \<approx> (r1 @ r2)"
+ − 252
apply (rule list_eq.intros(6))
+ − 253
apply (rule append_rsp_fst)
+ − 254
using a apply (assumption)
+ − 255
apply (rule list_eq.intros(6))
+ − 256
apply (rule append_sym_rsp)
+ − 257
apply (rule list_eq.intros(6))
+ − 258
apply (rule append_rsp_fst)
+ − 259
using b apply (assumption)
+ − 260
apply (rule append_sym_rsp)
+ − 261
done
175
+ − 262
194
+ − 263
lemma ho_append_rsp:
228
+ − 264
"(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
214
+ − 265
by (simp add: append_rsp)
175
+ − 266
194
+ − 267
lemma map_rsp:
+ − 268
assumes a: "a \<approx> b"
+ − 269
shows "map f a \<approx> map f b"
+ − 270
using a
+ − 271
apply (induct)
+ − 272
apply(auto intro: list_eq.intros)
+ − 273
done
+ − 274
+ − 275
lemma ho_map_rsp:
294
+ − 276
"(op = ===> op \<approx> ===> op \<approx>) map map"
+ − 277
by (simp add: map_rsp)
194
+ − 278
294
+ − 279
lemma map_append:
258
+ − 280
"(map f (a @ b)) \<approx>
+ − 281
(map f a) @ (map f b)"
215
+ − 282
by simp (rule list_eq_refl)
194
+ − 283
273
+ − 284
lemma ho_fold_rsp:
294
+ − 285
"(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1"
292
+ − 286
apply (auto simp add: FUN_REL_EQ)
294
+ − 287
apply (case_tac "rsp_fold x")
+ − 288
prefer 2
+ − 289
apply (erule_tac list_eq.induct)
+ − 290
apply (simp_all)
+ − 291
apply (erule_tac list_eq.induct)
+ − 292
apply (simp_all)
+ − 293
apply (auto simp add: memb_rsp rsp_fold_def)
+ − 294
done
241
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 295
254
+ − 296
print_quotients
+ − 297
+ − 298
226
+ − 299
ML {* val qty = @{typ "'a fset"} *}
+ − 300
ML {* val rsp_thms =
273
+ − 301
@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp}
226
+ − 302
@ @{thms ho_all_prs ho_ex_prs} *}
206
+ − 303
364
+ − 304
ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
+ − 305
ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *}
+ − 306
ML {* val consts = lookup_quot_consts defs *}
+ − 307
ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *}
314
+ − 308
364
+ − 309
lemma "IN x EMPTY = False"
+ − 310
by (tactic {* lift_tac_fset @{context} @{thm m1} 1 *})
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
+ − 311
364
+ − 312
lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"
+ − 313
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
+ − 314
364
+ − 315
lemma "INSERT a (INSERT a x) = INSERT a x"
+ − 316
apply (tactic {* lift_tac_fset @{context} @{thm list_eq.intros(4)} 1 *})
+ − 317
done
+ − 318
367
+ − 319
lemma "x = xa \<Longrightarrow> INSERT a x = INSERT a xa"
364
+ − 320
apply (tactic {* lift_tac_fset @{context} @{thm list_eq.intros(5)} 1 *})
+ − 321
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
+ − 322
367
+ − 323
lemma "CARD x = Suc n \<Longrightarrow> (\<exists>a b. \<not> IN a b & x = INSERT a b)"
364
+ − 324
apply (tactic {* lift_tac_fset @{context} @{thm card1_suc} 1 *})
+ − 325
done
+ − 326
+ − 327
lemma "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))"
+ − 328
apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *})
+ − 329
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
+ − 330
364
+ − 331
lemma "\<forall>f g z a x. FOLD f g (z::'b) (INSERT a x) =
+ − 332
(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)"
+ − 333
apply (tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
+ − 334
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
+ − 335
368
+ − 336
lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
+ − 337
apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
+ − 338
done
+ − 339
367
+ − 340
lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"
+ − 341
apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *})
+ − 342
done
+ − 343
376
+ − 344
ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *}
+ − 345
ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *}
+ − 346
lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
+ − 347
apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *})
+ − 348
apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *})
+ − 349
apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
+ − 350
done
171
13aab4c59096
More infrastructure for automatic lifting of theorems lifted before
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 351
273
+ − 352
quotient_def
276
+ − 353
fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
273
+ − 354
where
+ − 355
"fset_rec \<equiv> list_rec"
+ − 356
292
+ − 357
quotient_def
+ − 358
fset_case::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
+ − 359
where
+ − 360
"fset_case \<equiv> list_case"
+ − 361
296
+ − 362
(* Probably not true without additional assumptions about the function *)
292
+ − 363
lemma list_rec_rsp:
+ − 364
"(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec"
+ − 365
apply (auto simp add: FUN_REL_EQ)
296
+ − 366
apply (erule_tac list_eq.induct)
+ − 367
apply (simp_all)
292
+ − 368
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
+ − 369
292
+ − 370
lemma list_case_rsp:
+ − 371
"(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
+ − 372
apply (auto simp add: FUN_REL_EQ)
+ − 373
sorry
+ − 374
+ − 375
ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}
+ − 376
ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *}
376
+ − 377
ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same 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
+ − 378
376
+ − 379
ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.recs(2)})) *}
+ − 380
ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *}
+ − 381
lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"
+ − 382
apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *})
+ − 383
apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *})
+ − 384
apply (tactic {* (simp_tac (HOL_ss addsimps
+ − 385
@{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id})) 1 *})
+ − 386
ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *}
+ − 387
apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1 *})
+ − 388
apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
+ − 389
done
+ − 390
+ − 391
ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.cases(2)})) *}
+ − 392
ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *}
+ − 393
lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa"
+ − 394
apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *})
+ − 395
apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *})
+ − 396
apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
+ − 397
done
348
+ − 398
304
+ − 399
lemma list_induct_part:
+ − 400
assumes a: "P (x :: 'a list) ([] :: 'a list)"
+ − 401
assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)"
+ − 402
shows "P x l"
+ − 403
apply (rule_tac P="P x" in list.induct)
+ − 404
apply (rule a)
+ − 405
apply (rule b)
+ − 406
apply (assumption)
+ − 407
done
273
+ − 408
292
+ − 409
379
+ − 410
ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *}
292
+ − 411
334
+ − 412
+ − 413
384
+ − 414
+ − 415
ML {*
+ − 416
fun lambda_prs_conv1 ctxt quot ctrm =
+ − 417
case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) =>
+ − 418
let
+ − 419
val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1);
+ − 420
val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2);
+ − 421
val thy = ProofContext.theory_of ctxt;
+ − 422
val [cty_a, cty_b, cty_c, cty_d] = map (ctyp_of thy) [ty_a, ty_b, ty_c, ty_d]
+ − 423
val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_d];
+ − 424
val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
+ − 425
val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS};
+ − 426
val tac =
+ − 427
(compose_tac (false, lpi, 2)) THEN_ALL_NEW
+ − 428
(quotient_tac quot);
+ − 429
val gc = Drule.strip_imp_concl (cprop_of lpi);
+ − 430
val t = Goal.prove_internal [] gc (fn _ => tac 1)
+ − 431
val te = @{thm eq_reflection} OF [t]
+ − 432
val ts = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] te
+ − 433
val tl = Thm.lhs_of ts
+ − 434
val _ = tracing (Syntax.string_of_term @{context} (term_of ctrm));
+ − 435
val _ = tracing (Syntax.string_of_term @{context} (term_of tl));
+ − 436
val insts = matching_prs (ProofContext.theory_of ctxt) (term_of tl) (term_of ctrm);
+ − 437
val ti = Drule.eta_contraction_rule (Drule.instantiate insts ts);
+ − 438
(* val _ = tracing (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*)
+ − 439
in
+ − 440
Conv.rewr_conv ti ctrm
+ − 441
end
+ − 442
handle _ => Conv.all_conv ctrm
+ − 443
+ − 444
*}
+ − 445
ML {*
+ − 446
fun lambda_prs_conv ctxt quot ctrm =
+ − 447
case (term_of ctrm) of
+ − 448
(Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs (_, _, x)) =>
+ − 449
(Conv.arg_conv (Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt)
+ − 450
then_conv (lambda_prs_conv1 ctxt quot)) ctrm
+ − 451
| _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm
+ − 452
| Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm
+ − 453
| _ => Conv.all_conv ctrm
+ − 454
*}
+ − 455
+ − 456
ML {*
+ − 457
fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) =>
+ − 458
CONVERSION
+ − 459
(Conv.params_conv ~1 (fn ctxt =>
+ − 460
(Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv
+ − 461
Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i)
+ − 462
*}
+ − 463
+ − 464
379
+ − 465
(* Construction site starts here *)
+ − 466
lemma "P (x :: 'a list) (EMPTY :: 'a fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
+ − 467
apply (tactic {* procedure_tac @{thm list_induct_part} @{context} 1 *})
+ − 468
apply (tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *})
309
+ − 469
apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
+ − 470
apply (rule FUN_QUOTIENT)
+ − 471
apply (rule FUN_QUOTIENT)
+ − 472
apply (rule IDENTITY_QUOTIENT)
+ − 473
apply (rule FUN_QUOTIENT)
+ − 474
apply (rule QUOTIENT_fset)
+ − 475
apply (rule IDENTITY_QUOTIENT)
+ − 476
apply (rule IDENTITY_QUOTIENT)
+ − 477
apply (rule IDENTITY_QUOTIENT)
+ − 478
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 479
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 480
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 481
apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
+ − 482
apply (rule IDENTITY_QUOTIENT)
+ − 483
apply (rule IDENTITY_QUOTIENT)
+ − 484
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 485
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 486
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 487
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 488
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 489
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 490
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 491
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 492
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 493
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 494
apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
+ − 495
apply (rule IDENTITY_QUOTIENT)
+ − 496
apply (rule FUN_QUOTIENT)
+ − 497
apply (rule QUOTIENT_fset)
+ − 498
apply (rule IDENTITY_QUOTIENT)
+ − 499
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 500
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 501
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 502
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 503
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 504
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 505
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 506
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 507
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 508
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 509
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 510
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 511
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 512
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 513
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 514
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 515
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 516
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
317
+ − 517
apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
+ − 518
apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
+ − 519
apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *})
+ − 520
apply assumption
+ − 521
apply (rule refl)
309
+ − 522
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 523
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
317
+ − 524
apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
+ − 525
apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
+ − 526
apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *})
309
+ − 527
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 528
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 529
apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
+ − 530
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
317
+ − 531
apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
+ − 532
apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *})
309
+ − 533
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 534
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 535
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 536
apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
384
+ − 537
apply (simp only:map_id)
+ − 538
apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *})
+ − 539
ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *}
+ − 540
apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1 *})
+ − 541
apply (tactic {* lambda_prs_tac @{context} quot 1 *})
+ − 542
ML_prf {* val t = applic_prs @{context} rty qty absrep @{typ "('b \<Rightarrow> 'a list \<Rightarrow> bool)"} *}
+ − 543
apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] [t]) 1 *})
+ − 544
apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
309
+ − 545
done
+ − 546
163
+ − 547
end