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
529
+ − 19
lemma equivp_list_eq:
+ − 20
shows "equivp list_eq"
+ − 21
unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
163
+ − 22
apply(auto intro: list_eq.intros list_eq_refl)
+ − 23
done
+ − 24
+ − 25
quotient fset = "'a list" / "list_eq"
529
+ − 26
apply(rule equivp_list_eq)
163
+ − 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
529
+ − 62
thm Quotient_fset
163
+ − 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
lemma fs1_strong_cases:
+ − 139
fixes X :: "'a list"
+ − 140
shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a memb Y) \<and> (X \<approx> a # Y)))"
+ − 141
apply (induct X)
+ − 142
apply (simp)
+ − 143
apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons m1)
+ − 144
done
+ − 145
296
+ − 146
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
+ − 147
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
+ − 148
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
+ − 149
"IN \<equiv> membship"
163
+ − 150
+ − 151
term membship
+ − 152
term IN
+ − 153
thm IN_def
+ − 154
274
+ − 155
term fold1
+ − 156
quotient_def
+ − 157
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
+ − 158
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
+ − 159
"FOLD \<equiv> fold1"
194
+ − 160
+ − 161
term fold1
+ − 162
term fold
+ − 163
thm fold_def
+ − 164
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
+ − 165
quotient_def
254
+ − 166
fmap::"('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
225
+ − 167
where
254
+ − 168
"fmap \<equiv> map"
194
+ − 169
+ − 170
term map
+ − 171
term fmap
+ − 172
thm fmap_def
+ − 173
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
+ − 174
lemma memb_rsp:
163
+ − 175
fixes z
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 176
assumes a: "x \<approx> y"
163
+ − 177
shows "(z memb x) = (z memb y)"
+ − 178
using a by induct auto
+ − 179
506
+ − 180
lemma ho_memb_rsp[quotient_rsp]:
164
+ − 181
"(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)"
214
+ − 182
by (simp add: memb_rsp)
164
+ − 183
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
+ − 184
lemma card1_rsp:
163
+ − 185
fixes a b :: "'a list"
+ − 186
assumes e: "a \<approx> b"
+ − 187
shows "card1 a = card1 b"
214
+ − 188
using e by induct (simp_all add:memb_rsp)
163
+ − 189
506
+ − 190
lemma ho_card1_rsp[quotient_rsp]:
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 191
"(op \<approx> ===> op =) card1 card1"
214
+ − 192
by (simp add: card1_rsp)
171
13aab4c59096
More infrastructure for automatic lifting of theorems lifted before
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 193
506
+ − 194
lemma cons_rsp[quotient_rsp]:
163
+ − 195
fixes z
+ − 196
assumes a: "xs \<approx> ys"
+ − 197
shows "(z # xs) \<approx> (z # ys)"
+ − 198
using a by (rule list_eq.intros(5))
+ − 199
506
+ − 200
lemma ho_cons_rsp[quotient_rsp]:
228
+ − 201
"(op = ===> op \<approx> ===> op \<approx>) op # op #"
214
+ − 202
by (simp add: cons_rsp)
164
+ − 203
175
+ − 204
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
+ − 205
assumes a : "l1 \<approx> l2"
214
+ − 206
shows "(l1 @ s) \<approx> (l2 @ s)"
163
+ − 207
using a
214
+ − 208
by (induct) (auto intro: list_eq.intros list_eq_refl)
+ − 209
+ − 210
lemma append_end:
+ − 211
shows "(e # l) \<approx> (l @ [e])"
+ − 212
apply (induct l)
+ − 213
apply (auto intro: list_eq.intros list_eq_refl)
+ − 214
done
+ − 215
+ − 216
lemma rev_rsp:
+ − 217
shows "a \<approx> rev a"
+ − 218
apply (induct a)
+ − 219
apply simp
+ − 220
apply (rule list_eq_refl)
+ − 221
apply simp_all
+ − 222
apply (rule list_eq.intros(6))
+ − 223
prefer 2
+ − 224
apply (rule append_rsp_fst)
+ − 225
apply assumption
+ − 226
apply (rule append_end)
+ − 227
done
163
+ − 228
214
+ − 229
lemma append_sym_rsp:
+ − 230
shows "(a @ b) \<approx> (b @ a)"
+ − 231
apply (rule list_eq.intros(6))
+ − 232
apply (rule append_rsp_fst)
+ − 233
apply (rule rev_rsp)
+ − 234
apply (rule list_eq.intros(6))
+ − 235
apply (rule rev_rsp)
+ − 236
apply (simp)
+ − 237
apply (rule append_rsp_fst)
+ − 238
apply (rule list_eq.intros(3))
+ − 239
apply (rule rev_rsp)
+ − 240
done
+ − 241
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
+ − 242
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
+ − 243
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
+ − 244
assumes b : "l2 \<approx> r2 "
214
+ − 245
shows "(l1 @ l2) \<approx> (r1 @ r2)"
+ − 246
apply (rule list_eq.intros(6))
+ − 247
apply (rule append_rsp_fst)
+ − 248
using a apply (assumption)
+ − 249
apply (rule list_eq.intros(6))
+ − 250
apply (rule append_sym_rsp)
+ − 251
apply (rule list_eq.intros(6))
+ − 252
apply (rule append_rsp_fst)
+ − 253
using b apply (assumption)
+ − 254
apply (rule append_sym_rsp)
+ − 255
done
175
+ − 256
506
+ − 257
lemma ho_append_rsp[quotient_rsp]:
228
+ − 258
"(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
214
+ − 259
by (simp add: append_rsp)
175
+ − 260
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
+ − 261
lemma map_rsp:
194
+ − 262
assumes a: "a \<approx> b"
+ − 263
shows "map f a \<approx> map f b"
+ − 264
using a
+ − 265
apply (induct)
+ − 266
apply(auto intro: list_eq.intros)
+ − 267
done
+ − 268
506
+ − 269
lemma ho_map_rsp[quotient_rsp]:
294
+ − 270
"(op = ===> op \<approx> ===> op \<approx>) map map"
+ − 271
by (simp add: map_rsp)
194
+ − 272
294
+ − 273
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
+ − 274
"(map f (a @ b)) \<approx> (map f a) @ (map f b)"
215
+ − 275
by simp (rule list_eq_refl)
194
+ − 276
506
+ − 277
lemma ho_fold_rsp[quotient_rsp]:
294
+ − 278
"(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1"
536
+ − 279
apply (auto)
294
+ − 280
apply (case_tac "rsp_fold x")
+ − 281
prefer 2
+ − 282
apply (erule_tac list_eq.induct)
+ − 283
apply (simp_all)
+ − 284
apply (erule_tac list_eq.induct)
+ − 285
apply (simp_all)
+ − 286
apply (auto simp add: memb_rsp rsp_fold_def)
+ − 287
done
241
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 288
254
+ − 289
print_quotients
+ − 290
226
+ − 291
ML {* val qty = @{typ "'a fset"} *}
+ − 292
ML {* val rsp_thms =
458
+ − 293
@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} *}
206
+ − 294
364
+ − 295
ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
+ − 296
ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *}
506
+ − 297
ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *}
314
+ − 298
364
+ − 299
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
+ − 300
apply(tactic {* procedure_tac @{context} @{thm m1} 1 *})
477
6c88b42da228
A bit of progress; but the object-logic vs meta-logic distinction is troublesome.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 301
apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
525
+ − 302
apply(tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
506
+ − 303
apply(tactic {* clean_tac @{context} 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
+ − 304
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
+ − 305
364
+ − 306
lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"
+ − 307
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
+ − 308
364
+ − 309
lemma "INSERT a (INSERT a x) = INSERT a x"
+ − 310
apply (tactic {* lift_tac_fset @{context} @{thm list_eq.intros(4)} 1 *})
+ − 311
done
+ − 312
367
+ − 313
lemma "x = xa \<Longrightarrow> INSERT a x = INSERT a xa"
364
+ − 314
apply (tactic {* lift_tac_fset @{context} @{thm list_eq.intros(5)} 1 *})
+ − 315
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
+ − 316
367
+ − 317
lemma "CARD x = Suc n \<Longrightarrow> (\<exists>a b. \<not> IN a b & x = INSERT a b)"
364
+ − 318
apply (tactic {* lift_tac_fset @{context} @{thm card1_suc} 1 *})
+ − 319
done
+ − 320
+ − 321
lemma "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))"
+ − 322
apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *})
+ − 323
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
+ − 324
442
7beed9b75ea2
renamed LAMBDA_RES_TAC and WEAK_LAMBDA_RES_TAC to lower case names
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 325
lemma "FOLD f g (z::'b) (INSERT a x) =
364
+ − 326
(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
+ − 327
apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
364
+ − 328
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
+ − 329
525
+ − 330
ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
482
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 331
368
+ − 332
lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
+ − 333
apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
+ − 334
done
+ − 335
367
+ − 336
lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"
+ − 337
apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *})
+ − 338
done
+ − 339
477
6c88b42da228
A bit of progress; but the object-logic vs meta-logic distinction is troublesome.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 340
376
+ − 341
lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
462
+ − 342
apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
392
+ − 343
apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
432
+ − 344
apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
398
+ − 345
prefer 2
506
+ − 346
apply(tactic {* clean_tac @{context} 1 *})
481
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 347
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 348
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 349
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 350
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 351
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 352
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 353
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 354
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 355
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 356
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 357
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 358
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 359
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 360
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* D *) (* reflexivity of basic relations *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 361
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 362
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 363
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 364
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 365
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 366
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* C *) (* = and extensionality *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 367
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 368
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 369
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 370
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 371
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 372
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 373
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 374
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 375
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 376
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 377
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 378
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 379
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 380
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 381
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 382
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 383
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 384
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 7 *) (* respectfulness *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 385
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 386
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 387
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 388
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
7f97c52021c9
Fixed unlam for non-abstractions and updated list_induct_part proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 389
apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
516
+ − 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*}) (* E *) (* R x y assumptions *)
414
+ − 393
done
390
+ − 394
482
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 395
lemma list_induct_part:
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 396
assumes a: "P (x :: 'a list) ([] :: 'c list)"
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 397
assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)"
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 398
shows "P x l"
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 399
apply (rule_tac P="P x" in list.induct)
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 400
apply (rule a)
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 401
apply (rule b)
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 402
apply (assumption)
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 403
done
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 404
506
+ − 405
ML {* quot *}
+ − 406
thm quotient_thm
+ − 407
482
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 408
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"
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 409
apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 410
done
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 411
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 412
lemma "P (x :: 'a fset) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 413
apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 414
done
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 415
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 416
lemma "P (x :: 'a fset) ([] :: 'c list) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (e # t)) \<Longrightarrow> P x l"
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 417
apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 418
done
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 419
483
+ − 420
quotient fset2 = "'a list" / "list_eq"
529
+ − 421
apply(rule equivp_list_eq)
483
+ − 422
done
+ − 423
+ − 424
quotient_def
+ − 425
EMPTY2 :: "'a fset2"
+ − 426
where
+ − 427
"EMPTY2 \<equiv> ([]::'a list)"
+ − 428
+ − 429
quotient_def
+ − 430
INSERT2 :: "'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2"
+ − 431
where
+ − 432
"INSERT2 \<equiv> op #"
+ − 433
529
+ − 434
ML {* val quot = @{thms Quotient_fset Quotient_fset2} *}
507
f7569f994195
the error occurs in APPLY_RSP_TAC where the wrong quotient (for LIST_REL) is applied
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 435
ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
f7569f994195
the error occurs in APPLY_RSP_TAC where the wrong quotient (for LIST_REL) is applied
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 436
ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *}
483
+ − 437
+ − 438
lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
+ − 439
apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
+ − 440
done
+ − 441
+ − 442
lemma "P (x :: 'a fset) (EMPTY2 :: 'c fset2) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT2 e t)) \<Longrightarrow> P x l"
+ − 443
apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
+ − 444
done
+ − 445
273
+ − 446
quotient_def
276
+ − 447
fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
273
+ − 448
where
+ − 449
"fset_rec \<equiv> list_rec"
+ − 450
292
+ − 451
quotient_def
+ − 452
fset_case::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
+ − 453
where
+ − 454
"fset_case \<equiv> list_case"
+ − 455
296
+ − 456
(* Probably not true without additional assumptions about the function *)
506
+ − 457
lemma list_rec_rsp[quotient_rsp]:
292
+ − 458
"(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec"
536
+ − 459
apply (auto)
296
+ − 460
apply (erule_tac list_eq.induct)
+ − 461
apply (simp_all)
292
+ − 462
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
+ − 463
506
+ − 464
lemma list_case_rsp[quotient_rsp]:
292
+ − 465
"(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
536
+ − 466
apply (auto)
292
+ − 467
sorry
+ − 468
+ − 469
ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}
508
+ − 470
ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *}
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
+ − 471
376
+ − 472
lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"
+ − 473
apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *})
+ − 474
done
+ − 475
+ − 476
lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa"
+ − 477
apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *})
+ − 478
done
348
+ − 479
496
+ − 480
163
+ − 481
end