equal
deleted
inserted
replaced
332 (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)" |
332 (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)" |
333 apply (tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) |
333 apply (tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) |
334 done |
334 done |
335 |
335 |
336 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" |
336 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" |
|
337 apply(tactic {* Induct.fix_tac @{context} 0 [("x", @{typ "'b fset"}), ("xa", @{typ "'b fset"})] 1 *}) |
|
338 apply(tactic {* ObjectLogic.full_atomize_tac 1 *}) |
337 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *}) |
339 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *}) |
338 done |
340 done |
339 |
341 |
340 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)" |
342 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)" |
341 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) |
343 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) |