301 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
301 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
302 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} |
302 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} |
303 ML {* val consts = lookup_quot_consts defs *} |
303 ML {* val consts = lookup_quot_consts defs *} |
304 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *} |
304 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *} |
305 |
305 |
|
306 thm m1 |
|
307 |
306 lemma "IN x EMPTY = False" |
308 lemma "IN x EMPTY = False" |
307 by (tactic {* lift_tac_fset @{context} @{thm m1} 1 *}) |
309 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *}) |
|
310 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
|
311 apply(tactic {* all_inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
|
312 ML_prf {* |
|
313 val rtrm = @{term "\<forall>x. IN x EMPTY = False"} |
|
314 val qtrm = @{term "\<forall>x. x memb [] = False"} |
|
315 val aps = find_aps rtrm qtrm |
|
316 *} |
|
317 unfolding IN_def EMPTY_def |
|
318 apply(tactic {* clean_tac @{context} [quot] defs aps 1*}) |
|
319 done |
308 |
320 |
309 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)" |
321 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)" |
310 by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *}) |
322 by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *}) |
311 |
323 |
312 lemma "INSERT a (INSERT a x) = INSERT a x" |
324 lemma "INSERT a (INSERT a x) = INSERT a x" |