# HG changeset patch
# User berghofe
# Date 1235662443 -3600
# Node ID bd78f08b0ba1708005360e11d23b79a4ec8c368e
# Parent  f3b3b0e3d1844e7659048e7fc71b703f983a92d3
Added postprocessing rules for fresh_star.

diff -r f3b3b0e3d184 -r bd78f08b0ba1 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Thu Feb 26 16:32:46 2009 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Thu Feb 26 16:34:03 2009 +0100
@@ -397,6 +397,25 @@
 
 lemmas fresh_star_prod = fresh_star_prod_list fresh_star_prod_set
 
+lemma fresh_star_set_eq: "set xs \<sharp>* c = xs \<sharp>* c"
+  by (simp add: fresh_star_def)
+
+lemma fresh_star_Un_elim:
+  "((S \<union> T) \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (S \<sharp>* c \<Longrightarrow> T \<sharp>* c \<Longrightarrow> PROP C)"
+  apply rule
+  apply (simp_all add: fresh_star_def)
+  apply (erule meta_mp)
+  apply blast
+  done
+
+lemma fresh_star_insert_elim:
+  "(insert x S \<sharp>* c \<Longrightarrow> PROP C) \<equiv> (x \<sharp> c \<Longrightarrow> S \<sharp>* c \<Longrightarrow> PROP C)"
+  by rule (simp_all add: fresh_star_def)
+
+lemma fresh_star_empty_elim:
+  "({} \<sharp>* c \<Longrightarrow> PROP C) \<equiv> PROP C"
+  by (simp add: fresh_star_def)
+
 text {* Normalization of freshness results; cf.\ @{text nominal_induct} *}
 
 lemma fresh_star_unit_elim: 
diff -r f3b3b0e3d184 -r bd78f08b0ba1 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Thu Feb 26 16:32:46 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Thu Feb 26 16:34:03 2009 +0100
@@ -28,6 +28,11 @@
 fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
   (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt));
 
+val fresh_postprocess =
+  Simplifier.full_simplify (HOL_basic_ss addsimps
+    [@{thm fresh_star_set_eq}, @{thm fresh_star_Un_elim},
+     @{thm fresh_star_insert_elim}, @{thm fresh_star_empty_elim}]);
+
 fun preds_of ps t = gen_inter (op = o apfst dest_Free) (ps, Term.add_frees t []);
 
 val perm_bool = mk_meta_eq (thm "perm_bool");
@@ -192,12 +197,15 @@
           handle TERM _ =>
             error ("Expression " ^ quote s ^ " to be avoided in case " ^
               quote name ^ " is not a set type");
-        val ps = map mk sets
+        fun add_set p [] = [p]
+          | add_set (t, T) ((u, U) :: ps) =
+              if T = U then
+                let val S = HOLogic.mk_setT T
+                in (Const (@{const_name "op Un"}, S --> S --> S) $ u $ t, T) :: ps
+                end
+              else (u, U) :: add_set (t, T) ps
       in
-        case duplicates op = (map snd ps) of
-          [] => ps
-        | Ts => error ("More than one set in case " ^ quote name ^
-            " for type(s) " ^ commas_quote (map (Syntax.string_of_typ ctxt') Ts))
+        fold (mk #> add_set) sets []
       end;
 
     val prems = map (fn (prem, name) =>
@@ -436,7 +444,9 @@
           REPEAT (REPEAT (resolve_tac [conjI, impI] 1) THEN
             etac impE 1 THEN atac 1 THEN REPEAT (etac @{thm allE_Nil} 1) THEN
             asm_full_simp_tac (simpset_of thy) 1)
-        end) |> singleton (ProofContext.export ctxt' ctxt);
+        end) |>
+        fresh_postprocess |>
+        singleton (ProofContext.export ctxt' ctxt);
 
   in
     ctxt'' |>