# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1285595475 14400
# Node ID 5ac9a74d22fd7911142c2bc1888e29a085877a72
# Parent  d0961e6d6881b0c1c14592b6664726b10564d873
post-processed eq_iff and supp threormes according to the fv-supp equality

diff -r d0961e6d6881 -r 5ac9a74d22fd Nominal/Ex/Let.thy
--- a/Nominal/Ex/Let.thy	Mon Sep 27 04:56:49 2010 -0400
+++ b/Nominal/Ex/Let.thy	Mon Sep 27 09:51:15 2010 -0400
@@ -18,36 +18,21 @@
   "bn ANil = []"
 | "bn (ACons x t as) = (atom x) # (bn as)"
 
+
 thm trm_assn.fv_defs
-thm trm_assn.eq_iff trm_assn.bn_defs
+thm trm_assn.eq_iff 
 thm trm_assn.bn_defs
 thm trm_assn.perm_simps
-thm trm_assn.induct[no_vars]
-thm trm_assn.inducts[no_vars]
+thm trm_assn.induct
+thm trm_assn.inducts
 thm trm_assn.distinct
 thm trm_assn.supp
-thm trm_assn.fv_defs[simplified trm_assn.supp(1-2)]
 
 
-
-lemma fv_supp:
-  shows "fv_trm = supp"
-  and   "fv_assn = supp"
-apply(rule ext)
-apply(rule trm_assn.supp)
-apply(rule ext)
-apply(rule trm_assn.supp)
-done
-
-lemmas eq_iffs = trm_assn.eq_iff[folded fv_supp[symmetric], folded Abs_eq_iff]
-
-lemmas supps = trm_assn.fv_defs[simplified trm_assn.supp(1-2)]
-
 lemma supp_fresh_eq:
   assumes "supp x = supp y"
   shows "a \<sharp> x \<longleftrightarrow> a \<sharp> y"
-using assms
-by (simp add: fresh_def)
+using assms by (simp add: fresh_def)
 
 lemma supp_not_in:
   assumes "x = y"
@@ -56,12 +41,12 @@
 by (simp add: fresh_def)
 
 lemmas freshs =
-  supps(1)[THEN supp_not_in, folded fresh_def]
-  supps(2)[THEN supp_not_in, simplified, folded fresh_def]
-  supps(3)[THEN supp_not_in, folded fresh_def]
-  supps(4)[THEN supp_not_in, folded fresh_def]
-  supps(5)[THEN supp_not_in, simplified, folded fresh_def]
-  supps(6)[THEN supp_not_in, simplified, folded fresh_def]
+  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))"
diff -r d0961e6d6881 -r 5ac9a74d22fd Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Mon Sep 27 04:56:49 2010 -0400
+++ b/Nominal/Ex/SingleLet.thy	Mon Sep 27 09:51:15 2010 -0400
@@ -21,7 +21,6 @@
 where
   "bn (As x y t) = [atom x]"
 
-
 thm single_let.distinct
 thm single_let.induct
 thm single_let.inducts
@@ -37,9 +36,6 @@
 thm single_let.supp
 thm single_let.size
 
-thm single_let.supp(1-2)
-thm single_let.fv_defs[simplified single_let.supp(1-2)]
-
 
 end
 
diff -r d0961e6d6881 -r 5ac9a74d22fd Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Mon Sep 27 04:56:49 2010 -0400
+++ b/Nominal/Nominal2.thy	Mon Sep 27 09:51:15 2010 -0400
@@ -568,7 +568,15 @@
       qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC
     else []
 
- 
+  (* 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)))
+
+  val qsupp_constrs = qfv_defs
+    |> map (simplify (HOL_basic_ss addsimps (take (length qfvs) qfv_supp_thms)))
+
   (* noting the theorems *)  
 
   (* generating the prefix for the theorem names *)
@@ -578,7 +586,7 @@
 
   val (_, lthy9') = lthyC
      |> Local_Theory.note ((thms_suffix "distinct", []), qdistincts) 
-     ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs)
+     ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs')
      ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) 
      ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) 
      ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) 
@@ -590,7 +598,7 @@
      ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts)
      ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms)
      ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms)
-     ||>> Local_Theory.note ((thms_suffix "supp", []), qfv_supp_thms)
+     ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs)
 in
   (0, lthy9')
 end handle TEST ctxt => (0, ctxt)
diff -r d0961e6d6881 -r 5ac9a74d22fd Nominal/nominal_dt_supp.ML
--- a/Nominal/nominal_dt_supp.ML	Mon Sep 27 04:56:49 2010 -0400
+++ b/Nominal/nominal_dt_supp.ML	Mon Sep 27 09:51:15 2010 -0400
@@ -186,6 +186,8 @@
         end)
   in
     induct_prove qtys (goals1 @ goals2) qinduct tac ctxt
+    |> map atomize
+    |> map (simplify (HOL_basic_ss addsimps @{thms fun_eq_iff[symmetric]}))
   end