709 end

   709 lemma not_in_union: "c \<notin> a \<union> b \<equiv> (c \<notin> a \<and> c \<notin> b)"

   710 by auto

   711 

   712 ML {*

   713 fun supports_tac perm =

   714   simp_tac (HOL_ss addsimps @{thms supports_def not_in_union} @ perm) THEN_ALL_NEW (

   715     REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conjs THEN'

   716     asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric]

   717       swap_fresh_fresh fresh_atom swap_at_base_simps(3)}))

   718 *}

   719 

   720 ML {*

   721 fun mk_supports_eq cnstr =

   722 let

   723   val (tys, ty) = (strip_type o fastype_of) cnstr

   724   val names = Datatype_Prop.make_tnames tys

   725   val frees = map Free (names ~~ tys)

   726   val rhs = list_comb (cnstr, frees)

   727   fun mk_supp ty x =

   728     Const (@{const_name supp}, ty --> @{typ "atom set"}) $ x

   729   fun mk_supp_arg (x, ty) =

   730     if is_atom @{theory} ty then mk_supp @{typ atom} (mk_atom ty $ x) else

   731     if is_atom_set @{theory} ty then mk_supp @{typ "atom set"} (mk_atoms x)

   732     else mk_supp ty x

   733   val lhss = map mk_supp_arg (frees ~~ tys)

   734   val supports = Const(@{const_name "supports"}, @{typ "atom set"} --> ty --> @{typ bool})

   735   val eq = HOLogic.mk_Trueprop (supports $ mk_union lhss $ rhs)

   736 in

   737   (names, eq)

   738 end

   739 *}

   740 

   741 end