# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1285604357 14400
# Node ID 2e174807c89107efe92d60921e1524cb6daddc52
# Parent  5ac9a74d22fd7911142c2bc1888e29a085877a72
added postprocessed fresh-lemmas for constructors

diff -r 5ac9a74d22fd -r 2e174807c891 Nominal/Ex/Let.thy
--- a/Nominal/Ex/Let.thy	Mon Sep 27 09:51:15 2010 -0400
+++ b/Nominal/Ex/Let.thy	Mon Sep 27 12:19:17 2010 -0400
@@ -27,26 +27,8 @@
 thm trm_assn.inducts
 thm trm_assn.distinct
 thm trm_assn.supp
-
-
-lemma supp_fresh_eq:
-  assumes "supp x = supp y"
-  shows "a \<sharp> x \<longleftrightarrow> a \<sharp> y"
-using assms by (simp add: fresh_def)
+thm trm_assn.fresh
 
-lemma supp_not_in:
-  assumes "x = y"
-  shows "a \<notin> x \<longleftrightarrow> a \<notin> y"
-using assms
-by (simp add: fresh_def)
-
-lemmas freshs =
-  trm_assn.supp(1)[THEN supp_not_in, folded fresh_def]
-  trm_assn.supp(2)[THEN supp_not_in, simplified, folded fresh_def]
-  trm_assn.supp(3)[THEN supp_not_in, folded fresh_def]
-  trm_assn.supp(4)[THEN supp_not_in, folded fresh_def]
-  trm_assn.supp(5)[THEN supp_not_in, simplified, folded fresh_def]
-  trm_assn.supp(6)[THEN supp_not_in, simplified, folded fresh_def]
 
 lemma fin_bn:
   shows "finite (set (bn l))"
@@ -83,7 +65,7 @@
 apply(simp)
 apply(rule test_trm_test_assn.intros)
 apply(assumption)
-apply(simp add: freshs fresh_star_def)
+apply(simp add: trm_assn.fresh fresh_star_def)
 apply(simp)
 defer
 apply(simp)
@@ -93,10 +75,11 @@
 apply(assumption)
 apply(assumption)
 apply(rule_tac t = "Let (p \<bullet> assn) (p \<bullet> trm)" in subst)
-apply(rule eq_iffs(4)[THEN iffD2])
+apply(rule trm_assn.eq_iff(4)[THEN iffD2])
 defer
 apply(rule test_trm_test_assn.intros)
 prefer 3
+apply(simp add: fresh_star_def trm_assn.fresh)
 thm freshs
 --"HERE"
 
diff -r 5ac9a74d22fd -r 2e174807c891 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Mon Sep 27 09:51:15 2010 -0400
+++ b/Nominal/Ex/SingleLet.thy	Mon Sep 27 12:19:17 2010 -0400
@@ -13,7 +13,7 @@
 | Let a::"assg" t::"trm"  bind "bn a" in t
 | Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind (set) x in y t t1 t2
 | Bar x::"name" y::"name" t::"trm" bind y x in t x y
-| Baz x::"name" t1::"trm" t2::"trm" bind (set) x in t1, bind (set) x in t2 
+| Baz x::"name" t1::"trm" t2::"trm" bind (set) x in t1, bind (res) x in t2 
 and assg =
   As "name" x::"name" t::"trm" bind x in t
 binder
@@ -21,6 +21,8 @@
 where
   "bn (As x y t) = [atom x]"
 
+
+
 thm single_let.distinct
 thm single_let.induct
 thm single_let.inducts
@@ -34,7 +36,7 @@
 thm single_let.supports
 thm single_let.fsupp
 thm single_let.supp
-thm single_let.size
+thm single_let.fresh
 
 
 end
diff -r 5ac9a74d22fd -r 2e174807c891 Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Mon Sep 27 09:51:15 2010 -0400
+++ b/Nominal/Ex/TypeSchemes.thy	Mon Sep 27 12:19:17 2010 -0400
@@ -24,7 +24,7 @@
 thm ty_tys.fv_bn_eqvt
 thm ty_tys.size_eqvt
 thm ty_tys.supports
-thm ty_tys.fsupp
+thm ty_tys.supp
 
 (* defined as two separate nominal datatypes *)
 
@@ -45,7 +45,7 @@
 thm tys2.fv_bn_eqvt
 thm tys2.size_eqvt
 thm tys2.supports
-thm tys2.fsupp
+thm tys2.supp
 
 
 
diff -r 5ac9a74d22fd -r 2e174807c891 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Mon Sep 27 09:51:15 2010 -0400
+++ b/Nominal/Nominal2.thy	Mon Sep 27 12:19:17 2010 -0400
@@ -571,12 +571,24 @@
   (* postprocessing of eq and fv theorems *)
 
   val qeq_iffs' = qeq_iffs
-    |> map (simplify (HOL_basic_ss addsimps 
-         (@{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]} @ qfv_supp_thms)))
+    |> map (simplify (HOL_basic_ss addsimps qfv_supp_thms))
+    |> map (simplify (HOL_basic_ss addsimps @{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]}))
 
   val qsupp_constrs = qfv_defs
     |> map (simplify (HOL_basic_ss addsimps (take (length qfvs) qfv_supp_thms)))
 
+  val transform_thm = @{lemma "x = y \<Longrightarrow> a \<notin> x \<longleftrightarrow> a \<notin> y" by simp}
+  val transform_thms = 
+    [ @{lemma "a \<notin> (S \<union> T) \<longleftrightarrow> a \<notin> S \<and> a \<notin> T" by simp}, 
+      @{lemma "a \<notin> (S - T) \<longleftrightarrow> a \<notin> S \<or> a \<in> T" by simp}, 
+      @{lemma "(lhs = (a \<notin> {})) \<longleftrightarrow> lhs" by simp}, 
+      @{thm fresh_def[symmetric]}]
+
+  val qfresh_constrs = qsupp_constrs
+    |> map (fn thm => thm RS transform_thm) 
+    |> map (simplify (HOL_basic_ss addsimps transform_thms))
+
+
   (* noting the theorems *)  
 
   (* generating the prefix for the theorem names *)
@@ -599,6 +611,7 @@
      ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms)
      ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms)
      ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs)
+     ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs)
 in
   (0, lthy9')
 end handle TEST ctxt => (0, ctxt)
diff -r 5ac9a74d22fd -r 2e174807c891 Nominal/nominal_dt_supp.ML
--- a/Nominal/nominal_dt_supp.ML	Mon Sep 27 09:51:15 2010 -0400
+++ b/Nominal/nominal_dt_supp.ML	Mon Sep 27 12:19:17 2010 -0400
@@ -20,8 +20,6 @@
 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP =
 struct
 
-fun lookup xs x = the (AList.lookup (op=) xs x)
-
 (* supports lemmas for constructors *)
 
 fun mk_supports_goal ctxt qtrm =