422 quotient fset2 = "'a list" / "list_eq"

   423   apply(rule equiv_list_eq)

   424   done

   425 

   426 quotient_def

   427   EMPTY2 :: "'a fset2"

   428 where

   429   "EMPTY2 \<equiv> ([]::'a list)"

   430 

   431 quotient_def

   432   INSERT2 :: "'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2"

   433 where

   434   "INSERT2 \<equiv> op #"

   435 

   436 ML {* val defs = @{thms EMPTY2_def INSERT2_def} @ defs *}

   437 ML {* val quot = @{thms QUOTIENT_fset QUOTIENT_fset2} *}

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

   439 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty quot defs *}

   440 

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

   442 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})

   443 done

   444 

   445 lemma "P (x :: 'a fset) (EMPTY2 :: 'c fset2) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT2 e t)) \<Longrightarrow> P x l"

   446 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})

   447 done

   448