# HG changeset patch
# User haftmann
# Date 1324739698 -3600
# Node ID 296d9a9c8d24d63b24175573890229ba7cbc9e8e
# Parent  d3325de5f2999b37bbfffa7197507f5234951d69
treatment of type constructor `set`

diff -r d3325de5f299 -r 296d9a9c8d24 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Sat Dec 24 15:55:03 2011 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Dec 24 16:14:58 2011 +0100
@@ -494,6 +494,7 @@
       val pt_optn_inst  = @{thm "pt_option_inst"};
       val pt_noptn_inst = @{thm "pt_noption_inst"};
       val pt_fun_inst   = @{thm "pt_fun_inst"};
+      val pt_set_inst   = @{thm "pt_set_inst"};
 
      (* for all atom-kind combinations <ak>/<ak'> show that        *)
      (* every <ak> is an instance of pt_<ak'>; the proof for       *)
@@ -541,6 +542,7 @@
                      rtac (thm RS pt1) 1, rtac (thm RS pt2) 1, rtac (thm RS pt3) 1, atac 1];
 
           val pt_thm_fun   = at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst));
+          val pt_thm_set   = at_thm RS (pt_inst RS pt_set_inst);
           val pt_thm_noptn = pt_inst RS pt_noptn_inst; 
           val pt_thm_optn  = pt_inst RS pt_optn_inst; 
           val pt_thm_list  = pt_inst RS pt_list_inst;
@@ -550,6 +552,7 @@
        in
         thy
         |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
+        |> AxClass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
         |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
         |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
         |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
diff -r d3325de5f299 -r 296d9a9c8d24 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Sat Dec 24 15:55:03 2011 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Sat Dec 24 16:14:58 2011 +0100
@@ -244,7 +244,7 @@
         NONE => thm' RS sym
       | SOME fs' =>
           let
-            val U = List.last (binder_types T);
+            val U = HOLogic.dest_setT (body_type T);
             val Ts = HOLogic.strip_ptupleT fs' U;
             (* FIXME: should cterm_instantiate increment indexes? *)
             val arg_cong' = Thm.incr_indexes (Thm.maxidx_of thm + 1) arg_cong;
@@ -351,7 +351,7 @@
   end;
 
 val to_pred_att = Thm.rule_attribute o to_pred;
-    
+
 
 (**** convert theorem in predicate notation to set notation ****)
 
@@ -421,7 +421,7 @@
       | infer (t $ u) = infer t #> infer u
       | infer _ = I;
     val new_arities = filter_out
-      (fn (x as Free (_, T), _) => member (op =) params x andalso length (binder_types T) > 1
+      (fn (x as Free (_, T), _) => member (op =) params x andalso length (binder_types T) > 0
         | _ => false) (fold (snd #> infer) intros []);
     val params' = map (fn x =>
       (case AList.lookup op = new_arities x of
@@ -447,7 +447,7 @@
     val ((cs', cs_info), eqns) = cs |> map (fn c as Free (s, T) =>
       let
         val fs = the_default [] (AList.lookup op = new_arities c);
-        val (Us, U) = split_last (binder_types T);
+        val (Us, U) = strip_type T |> apsnd HOLogic.dest_setT;
         val _ = Us = paramTs orelse error (Pretty.string_of (Pretty.chunks
           [Pretty.str "Argument types",
            Pretty.block (Pretty.commas (map (Syntax.pretty_typ lthy) Us)),