326 |
326 |
327 lemma "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))" |
327 lemma "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))" |
328 apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *}) |
328 apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *}) |
329 done |
329 done |
330 |
330 |
331 lemma "\<forall>f g z a x. FOLD f g (z::'b) (INSERT a x) = |
331 ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *} |
|
332 |
|
333 lemma "FOLD f g (z::'b) (INSERT a x) = |
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)" |
334 (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 *}) |
335 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) |
334 done |
336 done |
335 |
337 |
336 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" |
338 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" |
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 *}) |
342 done |
344 done |
343 |
|
344 ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *} |
|
345 |
345 |
346 lemma cheat: "P" sorry |
346 lemma cheat: "P" sorry |
347 |
347 |
348 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
348 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
349 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
349 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |