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 

   332 

   332 

   333 lemma "FOLD f g (z::'b) (INSERT a x) =

   333 lemma "FOLD f g (z::'b) (INSERT a x) =

   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)"

   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)"

   335 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})

   335 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})

   336 done

   336 done

   443   apply (rule b)

   443   apply (rule b)

   444   apply (assumption)

   444   apply (assumption)

   445   done

   445   done

   446 

   446 

   447 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}

   447 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}

   449 

   448 

   450 (* Construction site starts here *)

   449 (* Construction site starts here *)

   451 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"

   450 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"

   452 apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *})

   451 apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *})

   453 apply (tactic {* regularize_tac @{context} [rel_eqv] 1 *})

   452 apply (tactic {* regularize_tac @{context} [rel_eqv] 1 *})