# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1268332871 -3600
# Node ID bc9ed52bcef51d34ed20b63652ef6c18124225cc
# Parent  ccbcebef56f339a465faf34fe6f531dffc479274
support of atoms at the end of Abs.thy

diff -r ccbcebef56f3 -r bc9ed52bcef5 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Thu Mar 11 19:24:07 2010 +0100
+++ b/Nominal/Abs.thy	Thu Mar 11 19:41:11 2010 +0100
@@ -723,6 +723,30 @@
   "distinct_perms [] = True"
 | "distinct_perms (p # ps) = (supp p \<inter> supp ps = {} \<and> distinct_perms ps)"
 
+(* support of concrete atom sets *)
+
+atom_decl name
+
+lemma atom_eqvt_raw:
+  fixes p::"perm"
+  shows "(p \<bullet> atom) = atom"
+by (simp add: expand_fun_eq permute_fun_def atom_eqvt)
+
+lemma atom_image_cong:
+  shows "(atom ` X = atom ` Y) = (X = Y)"
+apply(rule inj_image_eq_iff)
+apply(simp add: inj_on_def)
+done
+
+lemma
+  fixes as::"name set"
+  shows "supp (atom ` as) = supp as"
+apply(simp add: supp_def)
+apply(simp add: image_eqvt)
+apply(simp add: atom_eqvt_raw)
+apply(simp add: atom_image_cong)
+done
+
 
 
 end
diff -r ccbcebef56f3 -r bc9ed52bcef5 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Thu Mar 11 19:24:07 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 11 19:41:11 2010 +0100
@@ -510,7 +510,7 @@
   fun prep_bn env bn_str =
     case (Syntax.read_term lthy bn_str) of
        Free (x, _) => (NONE, env_lookup env x)
-     | Const (a, T) $ Free (x, _) => (SOME (Const (a, T), true), env_lookup env x)
+     | Const (a, T) $ Free (x, _) => (SOME (Const (a, T), false), env_lookup env x)
      | _ => error (bn_str ^ " not allowed as binding specification.");  
  
   fun prep_typ env (i, opt_name) =