# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268322644 -3600
# Node ID b355cab42841f77f473b83d2d1682cb0250dfbce
# Parent  ed2ad1302fdde476888357f3599ec3325acf9d70
mk_supports_eq and supports_tac.

diff -r ed2ad1302fdd -r b355cab42841 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Thu Mar 11 16:16:15 2010 +0100
+++ b/Nominal/Fv.thy	Thu Mar 11 16:50:44 2010 +0100
@@ -706,4 +706,36 @@
 end
 *}
 
+lemma not_in_union: "c \<notin> a \<union> b \<equiv> (c \<notin> a \<and> c \<notin> b)"
+by auto
+
+ML {*
+fun supports_tac perm =
+  simp_tac (HOL_ss addsimps @{thms supports_def not_in_union} @ perm) THEN_ALL_NEW (
+    REPEAT o rtac allI THEN' REPEAT o rtac impI THEN' split_conjs THEN'
+    asm_full_simp_tac (HOL_ss addsimps @{thms fresh_def[symmetric]
+      swap_fresh_fresh fresh_atom swap_at_base_simps(3)}))
+*}
+
+ML {*
+fun mk_supports_eq cnstr =
+let
+  val (tys, ty) = (strip_type o fastype_of) cnstr
+  val names = Datatype_Prop.make_tnames tys
+  val frees = map Free (names ~~ tys)
+  val rhs = list_comb (cnstr, frees)
+  fun mk_supp ty x =
+    Const (@{const_name supp}, ty --> @{typ "atom set"}) $ x
+  fun mk_supp_arg (x, ty) =
+    if is_atom @{theory} ty then mk_supp @{typ atom} (mk_atom ty $ x) else
+    if is_atom_set @{theory} ty then mk_supp @{typ "atom set"} (mk_atoms x)
+    else mk_supp ty x
+  val lhss = map mk_supp_arg (frees ~~ tys)
+  val supports = Const(@{const_name "supports"}, @{typ "atom set"} --> ty --> @{typ bool})
+  val eq = HOLogic.mk_Trueprop (supports $ mk_union lhss $ rhs)
+in
+  (names, eq)
 end
+*}
+
+end