equal
deleted
inserted
replaced
297 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *} |
297 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *} |
298 |
298 |
299 lemma "IN x EMPTY = False" |
299 lemma "IN x EMPTY = False" |
300 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *}) |
300 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *}) |
301 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
301 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
302 apply(tactic {* all_inj_repabs_tac' @{context} [rel_refl] [trans2] 1 *}) |
302 apply(tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) |
303 apply(tactic {* clean_tac @{context} 1*}) |
303 apply(tactic {* clean_tac @{context} 1*}) |
304 done |
304 done |
305 |
305 |
306 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)" |
306 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)" |
307 by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *}) |
307 by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *}) |
325 lemma "FOLD f g (z::'b) (INSERT a x) = |
325 lemma "FOLD f g (z::'b) (INSERT a x) = |
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)" |
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)" |
327 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) |
327 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) |
328 done |
328 done |
329 |
329 |
330 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac' lthy [rel_refl] [trans2] *} |
330 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *} |
331 |
331 |
332 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" |
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 *}) |
333 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *}) |
334 done |
334 done |
335 |
335 |