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
290
a0be84b0c707
removed typing information from get_fun in quotient_def; *potentially* dangerous
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 179 ML {* prop_of @{thm fmap_def} *}
a0be84b0c707
removed typing information from get_fun in quotient_def; *potentially* dangerous
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 180
274
+ − 181 ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def FOLD_def} *}
163
+ − 182
164
+ − 183 lemma memb_rsp:
163
+ − 184 fixes z
+ − 185 assumes a: "list_eq x y"
+ − 186 shows "(z memb x) = (z memb y)"
+ − 187 using a by induct auto
+ − 188
164
+ − 189 lemma ho_memb_rsp:
+ − 190 "(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)"
214
+ − 191 by (simp add: memb_rsp)
164
+ − 192
163
+ − 193 lemma card1_rsp:
+ − 194 fixes a b :: "'a list"
+ − 195 assumes e: "a \<approx> b"
+ − 196 shows "card1 a = card1 b"
214
+ − 197 using e by induct (simp_all add:memb_rsp)
163
+ − 198
228
+ − 199 lemma ho_card1_rsp: "(op \<approx> ===> op =) card1 card1"
214
+ − 200 by (simp add: card1_rsp)
171
13aab4c59096
More infrastructure for automatic lifting of theorems lifted before
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 201
164
+ − 202 lemma cons_rsp:
163
+ − 203 fixes z
+ − 204 assumes a: "xs \<approx> ys"
+ − 205 shows "(z # xs) \<approx> (z # ys)"
+ − 206 using a by (rule list_eq.intros(5))
+ − 207
164
+ − 208 lemma ho_cons_rsp:
228
+ − 209 "(op = ===> op \<approx> ===> op \<approx>) op # op #"
214
+ − 210 by (simp add: cons_rsp)
164
+ − 211
175
+ − 212 lemma append_rsp_fst:
163
+ − 213 assumes a : "list_eq l1 l2"
214
+ − 214 shows "(l1 @ s) \<approx> (l2 @ s)"
163
+ − 215 using a
214
+ − 216 by (induct) (auto intro: list_eq.intros list_eq_refl)
+ − 217
+ − 218 lemma append_end:
+ − 219 shows "(e # l) \<approx> (l @ [e])"
+ − 220 apply (induct l)
+ − 221 apply (auto intro: list_eq.intros list_eq_refl)
+ − 222 done
+ − 223
+ − 224 lemma rev_rsp:
+ − 225 shows "a \<approx> rev a"
+ − 226 apply (induct a)
+ − 227 apply simp
+ − 228 apply (rule list_eq_refl)
+ − 229 apply simp_all
+ − 230 apply (rule list_eq.intros(6))
+ − 231 prefer 2
+ − 232 apply (rule append_rsp_fst)
+ − 233 apply assumption
+ − 234 apply (rule append_end)
+ − 235 done
163
+ − 236
214
+ − 237 lemma append_sym_rsp:
+ − 238 shows "(a @ b) \<approx> (b @ a)"
+ − 239 apply (rule list_eq.intros(6))
+ − 240 apply (rule append_rsp_fst)
+ − 241 apply (rule rev_rsp)
+ − 242 apply (rule list_eq.intros(6))
+ − 243 apply (rule rev_rsp)
+ − 244 apply (simp)
+ − 245 apply (rule append_rsp_fst)
+ − 246 apply (rule list_eq.intros(3))
+ − 247 apply (rule rev_rsp)
+ − 248 done
+ − 249
+ − 250 lemma append_rsp:
+ − 251 assumes a : "list_eq l1 r1"
+ − 252 assumes b : "list_eq l2 r2 "
+ − 253 shows "(l1 @ l2) \<approx> (r1 @ r2)"
+ − 254 apply (rule list_eq.intros(6))
+ − 255 apply (rule append_rsp_fst)
+ − 256 using a apply (assumption)
+ − 257 apply (rule list_eq.intros(6))
+ − 258 apply (rule append_sym_rsp)
+ − 259 apply (rule list_eq.intros(6))
+ − 260 apply (rule append_rsp_fst)
+ − 261 using b apply (assumption)
+ − 262 apply (rule append_sym_rsp)
+ − 263 done
175
+ − 264
194
+ − 265 lemma ho_append_rsp:
228
+ − 266 "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
214
+ − 267 by (simp add: append_rsp)
175
+ − 268
194
+ − 269 lemma map_rsp:
+ − 270 assumes a: "a \<approx> b"
+ − 271 shows "map f a \<approx> map f b"
+ − 272 using a
+ − 273 apply (induct)
+ − 274 apply(auto intro: list_eq.intros)
+ − 275 done
+ − 276
+ − 277 lemma ho_map_rsp:
294
+ − 278 "(op = ===> op \<approx> ===> op \<approx>) map map"
+ − 279 by (simp add: map_rsp)
194
+ − 280
294
+ − 281 lemma map_append:
258
+ − 282 "(map f (a @ b)) \<approx>
+ − 283 (map f a) @ (map f b)"
215
+ − 284 by simp (rule list_eq_refl)
194
+ − 285
273
+ − 286 lemma ho_fold_rsp:
294
+ − 287 "(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1"
292
+ − 288 apply (auto simp add: FUN_REL_EQ)
294
+ − 289 apply (case_tac "rsp_fold x")
+ − 290 prefer 2
+ − 291 apply (erule_tac list_eq.induct)
+ − 292 apply (simp_all)
+ − 293 apply (erule_tac list_eq.induct)
+ − 294 apply (simp_all)
+ − 295 apply (auto simp add: memb_rsp rsp_fold_def)
+ − 296 done
241
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 297
254
+ − 298 print_quotients
+ − 299
+ − 300
226
+ − 301 ML {* val qty = @{typ "'a fset"} *}
+ − 302 ML {* val rsp_thms =
273
+ − 303 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp}
226
+ − 304 @ @{thms ho_all_prs ho_ex_prs} *}
206
+ − 305
239
+ − 306 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *}
172
da38ce2711a6
More infrastructure for automatic lifting of theorems lifted before
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 307
314
+ − 308 thm m2
+ − 309
317
+ − 310 thm neq_Nil_conv
+ − 311 term REP_fset
+ − 312 term "op --->"
+ − 313 thm INSERT_def
+ − 314 ML {* val defs_sym = flat (map (add_lower_defs @{context}) @{thms INSERT_def}) *}
+ − 315 (*ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *}*)
226
+ − 316 ML {* lift_thm_fset @{context} @{thm m1} *}
+ − 317 ML {* lift_thm_fset @{context} @{thm m2} *}
+ − 318 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *}
+ − 319 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *}
+ − 320 ML {* lift_thm_fset @{context} @{thm card1_suc} *}
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 ML {* lift_thm_fset @{context} @{thm map_append} *}
251
+ − 322 ML {* lift_thm_fset @{context} @{thm append_assoc} *}
267
3764566c1151
Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 323 ML {* lift_thm_fset @{context} @{thm list.induct} *}
273
+ − 324 ML {* lift_thm_fset @{context} @{thm fold1.simps(2)} *}
309
+ − 325 ML {* lift_thm_fset @{context} @{thm not_mem_card1} *}
171
13aab4c59096
More infrastructure for automatic lifting of theorems lifted before
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 326
273
+ − 327 quotient_def
276
+ − 328 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
273
+ − 329 where
+ − 330 "fset_rec \<equiv> list_rec"
+ − 331
292
+ − 332 quotient_def
+ − 333 fset_case::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
+ − 334 where
+ − 335 "fset_case \<equiv> list_case"
+ − 336
296
+ − 337 (* Probably not true without additional assumptions about the function *)
292
+ − 338 lemma list_rec_rsp:
+ − 339 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec"
+ − 340 apply (auto simp add: FUN_REL_EQ)
296
+ − 341 apply (erule_tac list_eq.induct)
+ − 342 apply (simp_all)
292
+ − 343 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
+ − 344
292
+ − 345 lemma list_case_rsp:
+ − 346 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
+ − 347 apply (auto simp add: FUN_REL_EQ)
+ − 348 sorry
+ − 349
+ − 350
+ − 351 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}
+ − 352 ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *}
+ − 353
+ − 354 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *}
+ − 355
300
+ − 356
292
+ − 357 ML {* map (lift_thm_fset @{context}) @{thms list.recs} *}
+ − 358 ML {* map (lift_thm_fset @{context}) @{thms list.cases} *}
248
6ed87b3d358c
Finally merged the code of the versions of regularize and tested examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 359
304
+ − 360 lemma list_induct_part:
+ − 361 assumes a: "P (x :: 'a list) ([] :: 'a list)"
+ − 362 assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)"
+ − 363 shows "P x l"
+ − 364 apply (rule_tac P="P x" in list.induct)
+ − 365 apply (rule a)
+ − 366 apply (rule b)
+ − 367 apply (assumption)
+ − 368 done
273
+ − 369
292
+ − 370
+ − 371 (* Construction site starts here *)
+ − 372
+ − 373
273
+ − 374 ML {* val consts = lookup_quot_consts defs *}
+ − 375 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
+ − 376 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *}
+ − 377
296
+ − 378 thm list.recs(2)
304
+ − 379 ML {* val t_a = atomize_thm @{thm list_induct_part} *}
334
+ − 380
+ − 381
285
+ − 382 (* prove {* build_regularize_goal t_a rty rel @{context} *}
+ − 383 ML_prf {* fun tac ctxt = FIRST' [
251
+ − 384 rtac rel_refl,
+ − 385 atac,
285
+ − 386 rtac @{thm universal_twice},
+ − 387 (rtac @{thm impI} THEN' atac),
+ − 388 rtac @{thm implication_twice},
334
+ − 389 //comented out rtac @{thm equality_twice}, //
285
+ − 390 EqSubst.eqsubst_tac ctxt [0]
239
+ − 391 [(@{thm equiv_res_forall} OF [rel_eqv]),
285
+ − 392 (@{thm equiv_res_exists} OF [rel_eqv])],
252
e30997c88050
Regularize for equalities and a better tactic. "alpha.cases" now lifts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 393 (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl),
e30997c88050
Regularize for equalities and a better tactic. "alpha.cases" now lifts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 394 (rtac @{thm RIGHT_RES_FORALL_REGULAR})
285
+ − 395 ]; *}
252
e30997c88050
Regularize for equalities and a better tactic. "alpha.cases" now lifts.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 396 apply (atomize(full))
285
+ − 397 apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *})
334
+ − 398 done *)
305
+ − 399 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *}
273
+ − 400 ML {*
285
+ − 401 val rt = build_repabs_term @{context} t_r consts rty qty
+ − 402 val rg = Logic.mk_equals ((Thm.prop_of t_r), rt);
172
da38ce2711a6
More infrastructure for automatic lifting of theorems lifted before
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 403 *}
300
+ − 404 prove {* Syntax.check_term @{context} rg *}
309
+ − 405 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *}
172
da38ce2711a6
More infrastructure for automatic lifting of theorems lifted before
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 406 apply(atomize(full))
194
+ − 407 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
273
+ − 408 done
305
+ − 409 ML {*
+ − 410 val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms
172
da38ce2711a6
More infrastructure for automatic lifting of theorems lifted before
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 411 *}
241
60acf3d3a4a0
Finding applications and duplicates filtered out in abstractions
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 412
292
+ − 413 ML {* val abs = findabs rty (prop_of (t_a)) *}
+ − 414 ML {* val aps = findaps rty (prop_of (t_a)) *}
285
+ − 415 ML {* val lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *}
+ − 416 ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *}
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
+ − 417 ML {* val lam_prs_thms = map Thm.varifyT lam_prs_thms *}
292
+ − 418 ML {* t_t *}
289
7e8617f20b59
Remaining fixes for polymorphic types. map_append now lifts properly with 'a list and 'b list.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 419 ML {* val (alls, exs) = findallex @{context} rty qty (prop_of t_a); *}
285
+ − 420 ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *}
304
+ − 421 ML {* val t_l0 = repeat_eqsubst_thm @{context} (app_prs_thms) t_t *}
+ − 422 ML app_prs_thms
296
+ − 423 ML {* val t_l = repeat_eqsubst_thm @{context} (lam_prs_thms) t_l0 *}
304
+ − 424 ML lam_prs_thms
+ − 425 ML {* val t_id = simp_ids @{context} t_l *}
+ − 426 thm INSERT_def
292
+ − 427 ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *}
+ − 428 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_id *}
304
+ − 429 ML allthms
+ − 430 thm FORALL_PRS
309
+ − 431 ML {* val t_al = MetaSimplifier.rewrite_rule (allthms) t_d *}
+ − 432 ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_al *}
304
+ − 433 ML {* ObjectLogic.rulify t_s *}
+ − 434
+ − 435 ML {* val gl = @{term "P (x :: 'a list) (EMPTY :: 'a fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"} *}
+ − 436 ML {* val vars = map Free (Term.add_frees gl []) *}
+ − 437 ML {* fun lambda_all (var as Free(_, T)) trm = (Term.all T) $ lambda var trm *}
+ − 438 ML {* val gla = fold lambda_all vars gl *}
332
+ − 439 ML {* val glf = Type.legacy_freeze gla *}
304
+ − 440 ML {* val glac = (snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of @{theory} glf)) *}
309
+ − 441
+ − 442 ML {*
+ − 443 fun apply_subt2 f trm trm2 =
+ − 444 case (trm, trm2) of
+ − 445 (Abs (x, T, t), Abs (x2, T2, t2)) =>
+ − 446 let
+ − 447 val (x', t') = Term.dest_abs (x, T, t);
+ − 448 val (x2', t2') = Term.dest_abs (x2, T2, t2)
+ − 449 val (s1, s2) = f t' t2';
+ − 450 in
+ − 451 (Term.absfree (x', T, s1),
+ − 452 Term.absfree (x2', T2, s2))
+ − 453 end
+ − 454 | _ => f trm trm2
+ − 455 *}
+ − 456
317
+ − 457 (*ML_prf {*
+ − 458 val concl = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ()))))
+ − 459 val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP2})
+ − 460 val insts = Thm.first_order_match (pat, concl)
+ − 461 val t = Drule.instantiate insts @{thm APPLY_RSP2}
+ − 462 *}*)
+ − 463
309
+ − 464 ML {*
+ − 465 fun tyRel2 lthy ty gty =
+ − 466 if ty = gty then HOLogic.eq_const ty else
+ − 467
317
+ − 468 case quotdata_lookup lthy (fst (dest_Type gty)) of
309
+ − 469 SOME quotdata =>
+ − 470 if Sign.typ_instance (ProofContext.theory_of lthy) (ty, #rtyp quotdata) then
+ − 471 case #rel quotdata of
+ − 472 Const(s, _) => Const(s, dummyT)
+ − 473 | _ => error "tyRel2 fail: relation is not a constant"
+ − 474 else error "tyRel2 fail: a non-lifted type lifted to a lifted type"
+ − 475 | NONE => (case (ty, gty) of
+ − 476 (Type (s, tys), Type (s2, tys2)) =>
+ − 477 if s = s2 andalso length tys = length tys2 then
+ − 478 let
+ − 479 val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys;
+ − 480 val ty_out = ty --> ty --> @{typ bool};
+ − 481 val tys_out = tys_rel ---> ty_out;
+ − 482 in
+ − 483 (case (maps_lookup (ProofContext.theory_of lthy) s) of
+ − 484 SOME (info) => list_comb (Const (#relfun info, tys_out),
+ − 485 map2 (tyRel2 lthy) tys tys2)
+ − 486 | NONE => HOLogic.eq_const ty
+ − 487 )
+ − 488 end
+ − 489 else error "tyRel2 fail: different type structures"
+ − 490 | _ => HOLogic.eq_const ty)
+ − 491 *}
+ − 492
332
+ − 493 ML mk_babs
+ − 494
+ − 495 ML {*
+ − 496 fun mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty)
+ − 497 fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool})
+ − 498 fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool})
+ − 499 fun mk_resp ty = Const (@{const_name Respects}, [[ty, ty] ---> @{typ bool}, ty] ---> @{typ bool})
+ − 500 *}
+ − 501
+ − 502
309
+ − 503 ML {*
+ − 504 fun my_reg2 lthy trm gtrm =
+ − 505 case (trm, gtrm) of
+ − 506 (Abs (x, T, t), Abs (x2, T2, t2)) =>
+ − 507 if not (T = T2) then
+ − 508 let
+ − 509 val rrel = tyRel2 lthy T T2;
+ − 510 val (s1, s2) = apply_subt2 (my_reg2 lthy) trm gtrm
+ − 511 in
+ − 512 (((mk_babs (fastype_of trm) T) $ (mk_resp T $ rrel) $ s1),
+ − 513 ((mk_babs (fastype_of gtrm) T2) $ (mk_resp T2 $ (HOLogic.eq_const dummyT)) $ s2))
+ − 514 end
+ − 515 else
+ − 516 let
+ − 517 val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2
+ − 518 in
+ − 519 (Abs(x, T, s1), Abs(x2, T2, s2))
+ − 520 end
+ − 521 | (Const (@{const_name "All"}, ty) $ (t as Abs (_, T, _)),
+ − 522 Const (@{const_name "All"}, ty') $ (t2 as Abs (_, T2, _))) =>
+ − 523 if not (T = T2) then
+ − 524 let
+ − 525 val ty1 = domain_type ty;
+ − 526 val ty2 = domain_type ty1;
+ − 527 val ty'1 = domain_type ty';
+ − 528 val ty'2 = domain_type ty'1;
+ − 529 val rrel = tyRel2 lthy T T2;
+ − 530 val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2;
+ − 531 in
+ − 532 (((mk_ball ty1) $ (mk_resp ty2 $ rrel) $ s1),
+ − 533 ((mk_ball ty'1) $ (mk_resp ty'2 $ (HOLogic.eq_const dummyT)) $ s2))
+ − 534 end
+ − 535 else
+ − 536 let
+ − 537 val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2
+ − 538 in
+ − 539 ((Const (@{const_name "All"}, ty) $ s1),
+ − 540 (Const (@{const_name "All"}, ty') $ s2))
+ − 541 end
+ − 542 | (Const (@{const_name "Ex"}, ty) $ (t as Abs (_, T, _)),
+ − 543 Const (@{const_name "Ex"}, ty') $ (t2 as Abs (_, T2, _))) =>
+ − 544 if not (T = T2) then
+ − 545 let
+ − 546 val ty1 = domain_type ty
+ − 547 val ty2 = domain_type ty1
+ − 548 val ty'1 = domain_type ty'
+ − 549 val ty'2 = domain_type ty'1
+ − 550 val rrel = tyRel2 lthy T T2
+ − 551 val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2
+ − 552 in
+ − 553 (((mk_bex ty1) $ (mk_resp ty2 $ rrel) $ s1),
+ − 554 ((mk_bex ty'1) $ (mk_resp ty'2 $ (HOLogic.eq_const dummyT)) $ s2))
+ − 555 end
+ − 556 else
+ − 557 let
+ − 558 val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2
+ − 559 in
+ − 560 ((Const (@{const_name "Ex"}, ty) $ s1),
+ − 561 (Const (@{const_name "Ex"}, ty') $ s2))
+ − 562 end
+ − 563 | (Const (@{const_name "op ="}, T) $ t, (Const (@{const_name "op ="}, T2) $ t2)) =>
+ − 564 let
+ − 565 val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2
+ − 566 val rhs = Const (@{const_name "op ="}, T2) $ s2
+ − 567 in
+ − 568 if not (T = T2) then
+ − 569 ((tyRel2 lthy T T2) $ s1, rhs)
+ − 570 else
+ − 571 (Const (@{const_name "op ="}, T) $ s1, rhs)
+ − 572 end
+ − 573 | (t $ t', t2 $ t2') =>
+ − 574 let
+ − 575 val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2
+ − 576 val (s1', s2') = apply_subt2 (my_reg2 lthy) t' t2'
+ − 577 in
+ − 578 (s1 $ s1', s2 $ s2')
+ − 579 end
+ − 580 | (Const c1, Const c2) => (Const c1, Const c2) (* c2 may be lifted *)
+ − 581 | (Bound i, Bound j) => (* Bounds are replaced, so should never happen? *)
+ − 582 if i = j then (Bound i, Bound j) else error "my_reg2: different Bounds"
+ − 583 | (Free (n, T), Free(n2, T2)) => if n = n2 then (Free (n, T), Free (n2, T2))
+ − 584 else error ("my_ref2: different variables: " ^ n ^ ", " ^ n2)
+ − 585 | _ => error "my_reg2: terms don't agree"
+ − 586 *}
+ − 587
+ − 588
+ − 589 ML {* prop_of t_a *}
+ − 590 ML {* term_of glac *}
+ − 591 ML {* val (tta, ttb) = (my_reg2 @{context} (prop_of t_a) (term_of glac)) *}
333
+ − 592
+ − 593 (* Does not work. *)
334
+ − 594 ML {*
+ − 595 prop_of t_a
+ − 596 |> Syntax.string_of_term @{context}
+ − 597 |> writeln
+ − 598 *}
+ − 599
+ − 600 ML {*
+ − 601 (term_of glac)
+ − 602 |> Syntax.string_of_term @{context}
+ − 603 |> writeln
+ − 604 *}
+ − 605
335
+ − 606 ML {* val tta = REGULARIZE_trm @{context} (prop_of t_a) (term_of glac) *}
333
+ − 607
309
+ − 608 ML {* val tt = Syntax.check_term @{context} tta *}
334
+ − 609
+ − 610
309
+ − 611
+ − 612 prove t_r: {* Logic.mk_implies
+ − 613 ((prop_of t_a), tt) *}
+ − 614 ML_prf {* fun tac ctxt = FIRST' [
+ − 615 rtac rel_refl,
+ − 616 atac,
+ − 617 rtac @{thm universal_twice},
+ − 618 (rtac @{thm impI} THEN' atac),
+ − 619 rtac @{thm implication_twice},
+ − 620 (*rtac @{thm equality_twice},*)
+ − 621 EqSubst.eqsubst_tac ctxt [0]
+ − 622 [(@{thm equiv_res_forall} OF [rel_eqv]),
+ − 623 (@{thm equiv_res_exists} OF [rel_eqv])],
+ − 624 (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl),
+ − 625 (rtac @{thm RIGHT_RES_FORALL_REGULAR})
+ − 626 ]; *}
+ − 627
+ − 628 apply (atomize(full))
+ − 629 apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *})
+ − 630 done
+ − 631
+ − 632 ML {* val t_r = @{thm t_r} OF [t_a] *}
+ − 633
+ − 634 ML {* val ttg = Syntax.check_term @{context} ttb *}
+ − 635
+ − 636 ML {*
+ − 637 fun is_lifted_const h gh = is_Const h andalso is_Const gh andalso not (h = gh)
+ − 638
+ − 639 fun mkrepabs lthy ty gty t =
+ − 640 let
+ − 641 val qenv = distinct (op=) (diff (gty, ty) [])
+ − 642 (* val _ = sanity_chk qenv lthy *)
+ − 643 val ty = fastype_of t
+ − 644 val abs = get_fun absF qenv lthy gty $ t
+ − 645 val rep = get_fun repF qenv lthy gty $ abs
+ − 646 in
+ − 647 Syntax.check_term lthy rep
+ − 648 end
+ − 649 *}
+ − 650
+ − 651 ML {*
+ − 652 cterm_of @{theory} (mkrepabs @{context} @{typ "'a list \<Rightarrow> bool"} @{typ "'a fset \<Rightarrow> bool"} @{term "f :: ('a list \<Rightarrow> bool)"})
+ − 653 *}
+ − 654
+ − 655
+ − 656
+ − 657 ML {*
+ − 658 fun build_repabs_term lthy trm gtrm =
+ − 659 case (trm, gtrm) of
+ − 660 (Abs (a as (_, T, _)), Abs (a2 as (_, T2, _))) =>
+ − 661 let
+ − 662 val (vs, t) = Term.dest_abs a;
+ − 663 val (_, g) = Term.dest_abs a2;
+ − 664 val v = Free(vs, T);
+ − 665 val t' = lambda v (build_repabs_term lthy t g);
+ − 666 val ty = fastype_of trm;
+ − 667 val gty = fastype_of gtrm;
+ − 668 in
+ − 669 if (ty = gty) then t' else
+ − 670 mkrepabs lthy ty gty (
+ − 671 if (T = T2) then t' else
+ − 672 lambda v (t' $ (mkrepabs lthy T T2 v))
+ − 673 )
+ − 674 end
+ − 675 | _ =>
+ − 676 case (Term.strip_comb trm, Term.strip_comb gtrm) of
+ − 677 ((Const(@{const_name Respects}, _), _), _) => trm
+ − 678 | ((h, tms), (gh, gtms)) =>
+ − 679 let
+ − 680 val ty = fastype_of trm;
+ − 681 val gty = fastype_of gtrm;
+ − 682 val tms' = map2 (build_repabs_term lthy) tms gtms
+ − 683 val t' = list_comb(h, tms')
+ − 684 in
+ − 685 if ty = gty then t' else
+ − 686 if is_lifted_const h gh then mkrepabs lthy ty gty t' else
+ − 687 if (Term.is_Free h) andalso (length tms > 0) then mkrepabs lthy ty gty t' else t'
+ − 688 end
+ − 689 *}
+ − 690
+ − 691 ML {* val ttt = build_repabs_term @{context} tt ttg *}
+ − 692 ML {* val si = simp_ids_trm (cterm_of @{theory} ttt) *}
+ − 693 prove t_t: {* Logic.mk_equals ((Thm.prop_of t_r), term_of si) *}
+ − 694 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *}
+ − 695 apply(atomize(full))
+ − 696 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
+ − 697 apply (rule FUN_QUOTIENT)
+ − 698 apply (rule FUN_QUOTIENT)
+ − 699 apply (rule IDENTITY_QUOTIENT)
+ − 700 apply (rule FUN_QUOTIENT)
+ − 701 apply (rule QUOTIENT_fset)
+ − 702 apply (rule IDENTITY_QUOTIENT)
+ − 703 apply (rule IDENTITY_QUOTIENT)
+ − 704 apply (rule IDENTITY_QUOTIENT)
+ − 705 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 706 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 707 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 708 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
+ − 709 apply (rule IDENTITY_QUOTIENT)
+ − 710 apply (rule IDENTITY_QUOTIENT)
+ − 711 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 712 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 713 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 714 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 715 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 716 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 717 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 718 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 719 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 720 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 721 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
+ − 722 apply (rule IDENTITY_QUOTIENT)
+ − 723 apply (rule FUN_QUOTIENT)
+ − 724 apply (rule QUOTIENT_fset)
+ − 725 apply (rule IDENTITY_QUOTIENT)
+ − 726 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 727 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 728 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 729 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 730 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 731 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 732 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 733 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 734 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 735 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 736 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 737 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 738 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 739 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 740 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 741 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 742 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 743 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
317
+ − 744 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
+ − 745 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
+ − 746 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *})
+ − 747 apply assumption
+ − 748 apply (rule refl)
309
+ − 749 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 750 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
317
+ − 751 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
+ − 752 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
+ − 753 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *})
309
+ − 754 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 755 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 756 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
+ − 757 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
317
+ − 758 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
+ − 759 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *})
309
+ − 760 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 761 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 762 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 763 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})
+ − 764 done
+ − 765
+ − 766 thm t_t
+ − 767 ML {* val t_t = @{thm Pure.equal_elim_rule1} OF [@{thm t_t}, t_r] *}
+ − 768 ML {* val t_l = repeat_eqsubst_thm @{context} (lam_prs_thms) t_t *}
+ − 769 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_l *}
+ − 770 ML {* val t_al = MetaSimplifier.rewrite_rule (allthms) t_d *}
+ − 771 ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_al *}
+ − 772
178
945786a68ec6
Finally lifted induction, with some manually added simplification lemmas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 773
163
+ − 774 ML {*
226
+ − 775 fun lift_thm_fset_note name thm lthy =
163
+ − 776 let
226
+ − 777 val lifted_thm = lift_thm_fset lthy thm;
163
+ − 778 val (_, lthy2) = note (name, lifted_thm) lthy;
+ − 779 in
+ − 780 lthy2
+ − 781 end;
+ − 782 *}
+ − 783
226
+ − 784 local_setup {*
+ − 785 lift_thm_fset_note @{binding "m1l"} @{thm m1} #>
+ − 786 lift_thm_fset_note @{binding "m2l"} @{thm m2} #>
+ − 787 lift_thm_fset_note @{binding "leqi4l"} @{thm list_eq.intros(4)} #>
+ − 788 lift_thm_fset_note @{binding "leqi5l"} @{thm list_eq.intros(5)}
163
+ − 789 *}
226
+ − 790 thm m1l
+ − 791 thm m2l
+ − 792 thm leqi4l
+ − 793 thm leqi5l
163
+ − 794
+ − 795 end