merged

--- a/src/HOL/Nominal/Nominal.thy	Thu Feb 26 16:00:19 2009 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Thu Feb 26 16:35:10 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: 

--- a/src/HOL/Nominal/nominal_inductive2.ML	Thu Feb 26 16:00:19 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Thu Feb 26 16:35:10 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'' |>

--- a/src/HOL/Orderings.thy	Thu Feb 26 16:00:19 2009 +0100
+++ b/src/HOL/Orderings.thy	Thu Feb 26 16:35:10 2009 +0100
@@ -331,7 +331,7 @@
 
 fun struct_tac ((s, [eq, le, less]), thms) prems =
   let
-    fun decomp thy (Trueprop $ t) =
+    fun decomp thy (@{const Trueprop} $ t) =
       let
         fun excluded t =
           (* exclude numeric types: linear arithmetic subsumes transitivity *)
@@ -350,7 +350,8 @@
 	      of NONE => NONE
 	       | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
           | dec x = rel x;
-      in dec t end;
+      in dec t end
+      | decomp thy _ = NONE;
   in
     case s of
       "order" => Order_Tac.partial_tac decomp thms prems

--- a/src/HOL/Transitive_Closure.thy	Thu Feb 26 16:00:19 2009 +0100
+++ b/src/HOL/Transitive_Closure.thy	Thu Feb 26 16:35:10 2009 +0100
@@ -646,7 +646,7 @@
     val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl};
     val rtrancl_trans = @{thm rtrancl_trans};
 
-  fun decomp (Trueprop $ t) =
+  fun decomp (@{const Trueprop} $ t) =
     let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) =
         let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
               | decr (Const ("Transitive_Closure.trancl", _ ) $ r)  = (r,"r+")
@@ -654,7 +654,8 @@
             val (rel,r) = decr (Envir.beta_eta_contract rel);
         in SOME (a,b,rel,r) end
       | dec _ =  NONE
-    in dec t end;
+    in dec t end
+    | decomp _ = NONE;
 
   end);
 
@@ -669,7 +670,7 @@
     val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp};
     val rtrancl_trans = @{thm rtranclp_trans};
 
-  fun decomp (Trueprop $ t) =
+  fun decomp (@{const Trueprop} $ t) =
     let fun dec (rel $ a $ b) =
         let fun decr (Const ("Transitive_Closure.rtranclp", _ ) $ r) = (r,"r*")
               | decr (Const ("Transitive_Closure.tranclp", _ ) $ r)  = (r,"r+")
@@ -677,7 +678,8 @@
             val (rel,r) = decr rel;
         in SOME (a, b, rel, r) end
       | dec _ =  NONE
-    in dec t end;
+    in dec t end
+    | decomp _ = NONE;
 
   end);
 *}