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 |
387 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) |
387 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) |
388 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
388 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
389 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) |
389 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) |
390 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) |
390 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) |
391 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
391 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
|
392 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) |
|
393 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
|
394 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) |
392 done |
395 done |
393 |
396 |
394 lemma list_induct_part: |
397 lemma list_induct_part: |
395 assumes a: "P (x :: 'a list) ([] :: 'c list)" |
398 assumes a: "P (x :: 'a list) ([] :: 'c list)" |
396 assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)" |
399 assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)" |