163
+ − 1
theory FSet
768
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 2
imports "../QuotMain" "../QuotList" List
163
+ − 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
766
df053507edba
renamed "quotient" command to "quotient_type"; needs new keyword file to be installed
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 25
quotient_type
787
5cf83fa5b36c
made the quotient_type definition more like typedef; now type variables need to be explicitly given
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 26
'a fset = "'a list" / "list_eq"
766
df053507edba
renamed "quotient" command to "quotient_type"; needs new keyword file to be installed
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 27
by (rule equivp_list_eq)
163
+ − 28
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 29
quotient_definition
705
+ − 30
"EMPTY :: 'a fset"
+ − 31
as
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 32
"[]::'a list"
163
+ − 33
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 34
quotient_definition
705
+ − 35
"INSERT :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+ − 36
as
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 37
"op #"
163
+ − 38
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 39
quotient_definition
705
+ − 40
"FUNION :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+ − 41
as
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 42
"op @"
163
+ − 43
+ − 44
fun
+ − 45
card1 :: "'a list \<Rightarrow> nat"
+ − 46
where
+ − 47
card1_nil: "(card1 []) = 0"
683
+ − 48
| card1_cons: "(card1 (x # xs)) = (if (x mem xs) then (card1 xs) else (Suc (card1 xs)))"
163
+ − 49
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 50
quotient_definition
705
+ − 51
"CARD :: 'a fset \<Rightarrow> nat"
+ − 52
as
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 53
"card1"
163
+ − 54
768
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 55
quotient_definition
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 56
"fconcat :: ('a fset) fset \<Rightarrow> 'a fset"
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 57
as
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 58
"concat"
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 59
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 60
term concat
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 61
term fconcat
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 62
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 63
text {*
163
+ − 64
Maybe make_const_def should require a theorem that says that the particular lifted function
+ − 65
respects the relation. With it such a definition would be impossible:
768
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 66
make_const_def CARD @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 67
*}
163
+ − 68
+ − 69
lemma card1_0:
+ − 70
fixes a :: "'a list"
+ − 71
shows "(card1 a = 0) = (a = [])"
214
+ − 72
by (induct a) auto
163
+ − 73
+ − 74
lemma not_mem_card1:
+ − 75
fixes x :: "'a"
+ − 76
fixes xs :: "'a list"
683
+ − 77
shows "(~(x mem xs)) = (card1 (x # xs) = Suc (card1 xs))"
309
+ − 78
by auto
163
+ − 79
+ − 80
lemma mem_cons:
+ − 81
fixes x :: "'a"
+ − 82
fixes xs :: "'a list"
683
+ − 83
assumes a : "x mem xs"
163
+ − 84
shows "x # xs \<approx> xs"
214
+ − 85
using a by (induct xs) (auto intro: list_eq.intros )
163
+ − 86
+ − 87
lemma card1_suc:
+ − 88
fixes xs :: "'a list"
+ − 89
fixes n :: "nat"
+ − 90
assumes c: "card1 xs = Suc n"
683
+ − 91
shows "\<exists>a ys. ~(a mem ys) \<and> xs \<approx> (a # ys)"
163
+ − 92
using c
+ − 93
apply(induct xs)
+ − 94
apply (metis Suc_neq_Zero card1_0)
685
+ − 95
apply (metis FSet.card1_cons list_eq.intros(6) list_eq_refl mem_cons)
163
+ − 96
done
+ − 97
294
+ − 98
definition
+ − 99
rsp_fold
+ − 100
where
+ − 101
"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))))"
+ − 102
163
+ − 103
primrec
+ − 104
fold1
+ − 105
where
+ − 106
"fold1 f (g :: 'a \<Rightarrow> 'b) (z :: 'b) [] = z"
+ − 107
| "fold1 f g z (a # A) =
294
+ − 108
(if rsp_fold f
163
+ − 109
then (
683
+ − 110
if (a mem A) then (fold1 f g z A) else (f (g a) (fold1 f g z A))
163
+ − 111
) else z)"
+ − 112
+ − 113
lemma fs1_strong_cases:
+ − 114
fixes X :: "'a list"
683
+ − 115
shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a mem Y) \<and> (X \<approx> a # Y)))"
163
+ − 116
apply (induct X)
+ − 117
apply (simp)
685
+ − 118
apply (metis List.member.simps(1) list_eq.intros(6) list_eq_refl mem_cons)
163
+ − 119
done
+ − 120
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 121
quotient_definition
705
+ − 122
"IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"
+ − 123
as
683
+ − 124
"op mem"
163
+ − 125
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 126
quotient_definition
705
+ − 127
"FOLD :: ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a"
+ − 128
as
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 129
"fold1"
194
+ − 130
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 131
quotient_definition
705
+ − 132
"fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
+ − 133
as
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 134
"map"
194
+ − 135
683
+ − 136
lemma mem_rsp:
163
+ − 137
fixes z
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 138
assumes a: "x \<approx> y"
683
+ − 139
shows "(z mem x) = (z mem y)"
163
+ − 140
using a by induct auto
+ − 141
636
+ − 142
lemma ho_memb_rsp[quot_respect]:
683
+ − 143
"(op = ===> (op \<approx> ===> op =)) (op mem) (op mem)"
+ − 144
by (simp add: mem_rsp)
164
+ − 145
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
+ − 146
lemma card1_rsp:
163
+ − 147
fixes a b :: "'a list"
+ − 148
assumes e: "a \<approx> b"
+ − 149
shows "card1 a = card1 b"
683
+ − 150
using e by induct (simp_all add: mem_rsp)
163
+ − 151
636
+ − 152
lemma ho_card1_rsp[quot_respect]:
450
2dc708ddb93a
introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 153
"(op \<approx> ===> op =) card1 card1"
214
+ − 154
by (simp add: card1_rsp)
171
13aab4c59096
More infrastructure for automatic lifting of theorems lifted before
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 155
680
+ − 156
lemma cons_rsp:
163
+ − 157
fixes z
+ − 158
assumes a: "xs \<approx> ys"
+ − 159
shows "(z # xs) \<approx> (z # ys)"
+ − 160
using a by (rule list_eq.intros(5))
+ − 161
636
+ − 162
lemma ho_cons_rsp[quot_respect]:
228
+ − 163
"(op = ===> op \<approx> ===> op \<approx>) op # op #"
214
+ − 164
by (simp add: cons_rsp)
164
+ − 165
681
+ − 166
lemma append_rsp_aux1:
+ − 167
assumes a : "l2 \<approx> r2 "
+ − 168
shows "(h @ l2) \<approx> (h @ r2)"
+ − 169
using a
+ − 170
apply(induct h)
+ − 171
apply(auto intro: list_eq.intros(5))
+ − 172
done
163
+ − 173
681
+ − 174
lemma append_rsp_aux2:
+ − 175
assumes a : "l1 \<approx> r1" "l2 \<approx> r2 "
+ − 176
shows "(l1 @ l2) \<approx> (r1 @ r2)"
+ − 177
using a
+ − 178
apply(induct arbitrary: l2 r2)
+ − 179
apply(simp_all)
+ − 180
apply(blast intro: list_eq.intros append_rsp_aux1)+
+ − 181
done
214
+ − 182
681
+ − 183
lemma append_rsp[quot_respect]:
228
+ − 184
"(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
681
+ − 185
by (auto simp add: append_rsp_aux2)
175
+ − 186
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
+ − 187
lemma map_rsp:
194
+ − 188
assumes a: "a \<approx> b"
+ − 189
shows "map f a \<approx> map f b"
+ − 190
using a
+ − 191
apply (induct)
+ − 192
apply(auto intro: list_eq.intros)
+ − 193
done
+ − 194
636
+ − 195
lemma ho_map_rsp[quot_respect]:
294
+ − 196
"(op = ===> op \<approx> ===> op \<approx>) map map"
+ − 197
by (simp add: map_rsp)
194
+ − 198
294
+ − 199
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
+ − 200
"(map f (a @ b)) \<approx> (map f a) @ (map f b)"
215
+ − 201
by simp (rule list_eq_refl)
194
+ − 202
636
+ − 203
lemma ho_fold_rsp[quot_respect]:
294
+ − 204
"(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1"
536
+ − 205
apply (auto)
294
+ − 206
apply (case_tac "rsp_fold x")
+ − 207
prefer 2
+ − 208
apply (erule_tac list_eq.induct)
+ − 209
apply (simp_all)
+ − 210
apply (erule_tac list_eq.induct)
+ − 211
apply (simp_all)
683
+ − 212
apply (auto simp add: mem_rsp rsp_fold_def)
294
+ − 213
done
241
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 214
636
+ − 215
lemma list_equiv_rsp[quot_respect]:
549
+ − 216
shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
+ − 217
by (auto intro: list_eq.intros)
+ − 218
364
+ − 219
lemma "IN x EMPTY = False"
683
+ − 220
apply(lifting member.simps(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
+ − 221
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
+ − 222
364
+ − 223
lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"
768
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 224
apply (lifting member.simps(2))
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 225
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
+ − 226
364
+ − 227
lemma "INSERT a (INSERT a x) = INSERT a x"
654
02fd9de9d45e
tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 228
apply (lifting list_eq.intros(4))
364
+ − 229
done
+ − 230
367
+ − 231
lemma "x = xa \<Longrightarrow> INSERT a x = INSERT a xa"
654
02fd9de9d45e
tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 232
apply (lifting list_eq.intros(5))
364
+ − 233
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
+ − 234
367
+ − 235
lemma "CARD x = Suc n \<Longrightarrow> (\<exists>a b. \<not> IN a b & x = INSERT a b)"
654
02fd9de9d45e
tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 236
apply (lifting card1_suc)
364
+ − 237
done
+ − 238
+ − 239
lemma "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))"
654
02fd9de9d45e
tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 240
apply (lifting not_mem_card1)
364
+ − 241
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
+ − 242
442
7beed9b75ea2
renamed LAMBDA_RES_TAC and WEAK_LAMBDA_RES_TAC to lower case names
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 243
lemma "FOLD f g (z::'b) (INSERT a x) =
364
+ − 244
(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)"
654
02fd9de9d45e
tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 245
apply(lifting fold1.simps(2))
364
+ − 246
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
+ − 247
368
+ − 248
lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
654
02fd9de9d45e
tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 249
apply (lifting map_append)
368
+ − 250
done
+ − 251
367
+ − 252
lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"
654
02fd9de9d45e
tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 253
apply (lifting append_assoc)
367
+ − 254
done
+ − 255
477
6c88b42da228
A bit of progress; but the object-logic vs meta-logic distinction is troublesome.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 256
376
+ − 257
lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
654
02fd9de9d45e
tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 258
apply(lifting list.induct)
414
+ − 259
done
390
+ − 260
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
+ − 261
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
+ − 262
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
+ − 263
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
+ − 264
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
+ − 265
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
+ − 266
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
+ − 267
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
+ − 268
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
+ − 269
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
+ − 270
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 271
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"
654
02fd9de9d45e
tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 272
apply (lifting list_induct_part)
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
+ − 273
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
+ − 274
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 275
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"
654
02fd9de9d45e
tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 276
apply (lifting list_induct_part)
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
+ − 277
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
+ − 278
767baada01dc
New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 279
lemma "P (x :: 'a fset) ([] :: 'c list) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (e # t)) \<Longrightarrow> P x l"
654
02fd9de9d45e
tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 280
apply (lifting list_induct_part)
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
+ − 281
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
+ − 282
787
5cf83fa5b36c
made the quotient_type definition more like typedef; now type variables need to be explicitly given
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 283
quotient_type 'a fset2 = "'a list" / "list_eq"
654
02fd9de9d45e
tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 284
by (rule equivp_list_eq)
483
+ − 285
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 286
quotient_definition
705
+ − 287
"EMPTY2 :: 'a fset2"
+ − 288
as
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 289
"[]::'a list"
483
+ − 290
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 291
quotient_definition
705
+ − 292
"INSERT2 :: 'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2"
+ − 293
as
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 294
"op #"
483
+ − 295
+ − 296
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"
654
02fd9de9d45e
tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 297
apply (lifting list_induct_part)
483
+ − 298
done
+ − 299
+ − 300
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"
654
02fd9de9d45e
tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 301
apply (lifting list_induct_part)
483
+ − 302
done
+ − 303
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 304
quotient_definition
705
+ − 305
"fset_rec :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
+ − 306
as
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 307
"list_rec"
273
+ − 308
767
37285ec4387d
on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 309
quotient_definition
705
+ − 310
"fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
+ − 311
as
663
0dd10a900cae
Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 312
"list_case"
292
+ − 313
296
+ − 314
(* Probably not true without additional assumptions about the function *)
636
+ − 315
lemma list_rec_rsp[quot_respect]:
292
+ − 316
"(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec"
536
+ − 317
apply (auto)
296
+ − 318
apply (erule_tac list_eq.induct)
+ − 319
apply (simp_all)
292
+ − 320
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
+ − 321
636
+ − 322
lemma list_case_rsp[quot_respect]:
292
+ − 323
"(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
536
+ − 324
apply (auto)
292
+ − 325
sorry
+ − 326
376
+ − 327
lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"
654
02fd9de9d45e
tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 328
apply (lifting list.recs(2))
376
+ − 329
done
+ − 330
+ − 331
lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa"
654
02fd9de9d45e
tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 332
apply (lifting list.cases(2))
376
+ − 333
done
348
+ − 334
609
6ce4f274b0fa
3 lambda examples in FSet. In the last one regularize_term fails.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 335
lemma ttt: "((op @) x ((op #) e [])) = (((op #) e x))"
6ce4f274b0fa
3 lambda examples in FSet. In the last one regularize_term fails.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 336
sorry
654
02fd9de9d45e
tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 337
609
6ce4f274b0fa
3 lambda examples in FSet. In the last one regularize_term fails.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 338
lemma "(FUNION x (INSERT e EMPTY)) = ((INSERT e x))"
654
02fd9de9d45e
tuned the examples and flagged the problematic cleaning lemmas in FSet
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 339
apply (lifting ttt)
609
6ce4f274b0fa
3 lambda examples in FSet. In the last one regularize_term fails.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 340
done
6ce4f274b0fa
3 lambda examples in FSet. In the last one regularize_term fails.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 341
658
+ − 342
609
6ce4f274b0fa
3 lambda examples in FSet. In the last one regularize_term fails.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 343
lemma ttt2: "(\<lambda>e. ((op @) x ((op #) e []))) = (\<lambda>e. ((op #) e x))"
6ce4f274b0fa
3 lambda examples in FSet. In the last one regularize_term fails.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 344
sorry
6ce4f274b0fa
3 lambda examples in FSet. In the last one regularize_term fails.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 345
6ce4f274b0fa
3 lambda examples in FSet. In the last one regularize_term fails.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 346
lemma "(\<lambda>e. (FUNION x (INSERT e EMPTY))) = (\<lambda>e. (INSERT e x))"
641
+ − 347
apply(lifting ttt2)
639
+ − 348
apply(regularize)
634
+ − 349
apply(rule impI)
+ − 350
apply(simp)
+ − 351
apply(rule allI)
+ − 352
apply(rule list_eq_refl)
+ − 353
done
609
6ce4f274b0fa
3 lambda examples in FSet. In the last one regularize_term fails.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 354
695
+ − 355
lemma ttt3: "(\<lambda>x. ((op @) x (e # []))) = (op #) e"
609
6ce4f274b0fa
3 lambda examples in FSet. In the last one regularize_term fails.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 356
sorry
6ce4f274b0fa
3 lambda examples in FSet. In the last one regularize_term fails.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 357
695
+ − 358
lemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = INSERT e"
+ − 359
apply(lifting ttt3)
+ − 360
apply(regularize)
+ − 361
apply(auto simp add: cons_rsp)
+ − 362
done
646
10d04ee52101
An example which is hard to lift because of the interplay between lambda_prs and unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 363
lemma hard: "(\<lambda>P. \<lambda>Q. P (Q (x::'a list))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a list)))"
10d04ee52101
An example which is hard to lift because of the interplay between lambda_prs and unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 364
sorry
10d04ee52101
An example which is hard to lift because of the interplay between lambda_prs and unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 365
10d04ee52101
An example which is hard to lift because of the interplay between lambda_prs and unfolding.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 366
lemma hard_lift: "(\<lambda>P. \<lambda>Q. P (Q (x::'a fset))) = (\<lambda>P. \<lambda>Q. Q (P (x::'a fset)))"
656
c86a47d4966e
Temporarily repeated fun_map_tac 4 times. Cleaning for all examples work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 367
apply(lifting hard)
658
+ − 368
apply(regularize)
697
+ − 369
apply(rule fun_rel_id_asm)
+ − 370
apply(subst babs_simp)
758
+ − 371
apply(tactic {* Quotient_Tacs.quotient_tac @{context} 1 *})
697
+ − 372
apply(rule fun_rel_id_asm)
+ − 373
apply(rule impI)
+ − 374
apply(rule mp[OF eq_imp_rel[OF fset_equivp]])
+ − 375
apply(drule fun_cong)
+ − 376
apply(drule fun_cong)
+ − 377
apply(assumption)
+ − 378
done
+ − 379
+ − 380
650
+ − 381
163
+ − 382
end