# HG changeset patch
# User haftmann
# Date 1236783411 -3600
# Node ID 7655e6533209977ca03a9fadf5a17760a78a627a
# Parent  4caf15ae8c2652b62be1ed610bdb9ed1220506ea
HOLogic.mk_set, HOLogic.dest_set

diff -r 4caf15ae8c26 -r 7655e6533209 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Mar 11 15:56:50 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Mar 11 15:56:51 2009 +0100
@@ -75,11 +75,6 @@
   | add_binders thy i (Abs (_, _, t)) bs = add_binders thy (i + 1) t bs
   | add_binders thy i _ bs = bs;
 
-fun mk_set T [] = Const (@{const_name Set.empty}, HOLogic.mk_setT T)
-  | mk_set T (x :: xs) =
-      Const ("insert", T --> HOLogic.mk_setT T --> HOLogic.mk_setT T) $ x $
-        mk_set T xs;
-
 fun split_conj f names (Const ("op &", _) $ p $ q) _ = (case head_of p of
       Const (name, _) =>
         if name mem names then SOME (f p q) else NONE
@@ -216,7 +211,7 @@
       in
         (params,
          if null avoids then
-           map (fn (T, ts) => (mk_set T ts, T))
+           map (fn (T, ts) => (HOLogic.mk_set T ts, T))
              (fold (add_binders thy 0) (prems @ [concl]) [])
          else case AList.lookup op = avoids name of
            NONE => []
diff -r 4caf15ae8c26 -r 7655e6533209 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Wed Mar 11 15:56:50 2009 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Wed Mar 11 15:56:51 2009 +0100
@@ -1011,7 +1011,7 @@
             (augment_sort thy8 pt_cp_sort
               (HOLogic.mk_Trueprop (HOLogic.mk_eq
                 (supp c,
-                 if null dts then Const (@{const_name Set.empty}, HOLogic.mk_setT atomT)
+                 if null dts then HOLogic.mk_set atomT []
                  else foldr1 (HOLogic.mk_binop @{const_name Un}) (map supp args2)))))
             (fn _ =>
               simp_tac (HOL_basic_ss addsimps (supp_def ::
diff -r 4caf15ae8c26 -r 7655e6533209 src/HOL/SizeChange/sct.ML
--- a/src/HOL/SizeChange/sct.ML	Wed Mar 11 15:56:50 2009 +0100
+++ b/src/HOL/SizeChange/sct.ML	Wed Mar 11 15:56:51 2009 +0100
@@ -266,13 +266,6 @@
 
 fun mk_edge m G n = HOLogic.mk_prod (m, HOLogic.mk_prod (G, n))
 
-fun mk_set T [] = Const (@{const_name Set.empty}, HOLogic.mk_setT T)
-  | mk_set T (x :: xs) = Const (@{const_name insert},
-      T --> HOLogic.mk_setT T --> HOLogic.mk_setT T) $ x $ mk_set T xs
-
-fun dest_set (Const (@{const_name Set.empty}, _)) = []
-  | dest_set (Const (@{const_name insert}, _) $ x $ xs) = x :: dest_set xs
-
 val in_graph_tac =
     simp_tac (HOL_basic_ss addsimps has_edge_simps) 1
     THEN SIMPSET (fn x => simp_tac x 1) (* FIXME reduce simpset *)
@@ -333,7 +326,7 @@
 
 
       val ACG = map_filter (fn (Graph (G, _),(m, n)) => SOME (mk_edge (mk_number m) G (mk_number n)) | _ => NONE) (flat parts ~~ flat pairs)
-                    |> mk_set (edgeT HOLogic.natT scgT)
+                    |> HOLogic.mk_set (edgeT HOLogic.natT scgT)
                     |> curry op $ (graph_const HOLogic.natT scgT)
 
 
diff -r 4caf15ae8c26 -r 7655e6533209 src/HOL/Tools/Qelim/langford.ML
--- a/src/HOL/Tools/Qelim/langford.ML	Wed Mar 11 15:56:50 2009 +0100
+++ b/src/HOL/Tools/Qelim/langford.ML	Wed Mar 11 15:56:51 2009 +0100
@@ -11,14 +11,6 @@
 structure LangfordQE :LANGFORD_QE = 
 struct
 
-val dest_set =
- let 
-  fun h acc ct = 
-   case term_of ct of
-     Const (@{const_name Set.empty}, _) => acc
-   | Const (@{const_name insert}, _) $ _ $ t => h (Thm.dest_arg1 ct :: acc) (Thm.dest_arg ct)
-in h [] end;
-
 fun prove_finite cT u = 
 let val [th0,th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"}
     fun ins x th =
@@ -44,7 +36,7 @@
            val cT = ctyp_of_term a
            val ne = instantiate' [SOME cT] [SOME a, SOME A] 
                     @{thm insert_not_empty}
-           val f = prove_finite cT (dest_set S)
+           val f = prove_finite cT (HOLogic.dest_set S)
        in (ne, f) end
 
      val qe = case (term_of L, term_of U) of 
diff -r 4caf15ae8c26 -r 7655e6533209 src/HOL/Tools/function_package/scnp_reconstruct.ML
--- a/src/HOL/Tools/function_package/scnp_reconstruct.ML	Wed Mar 11 15:56:50 2009 +0100
+++ b/src/HOL/Tools/function_package/scnp_reconstruct.ML	Wed Mar 11 15:56:51 2009 +0100
@@ -142,11 +142,6 @@
 
 val setT = HOLogic.mk_setT
 
-fun mk_set T [] = Const (@{const_name Set.empty}, setT T)
-  | mk_set T (x :: xs) =
-      Const (@{const_name insert}, T --> setT T --> setT T) $
-            x $ mk_set T xs
-
 fun set_member_tac m i =
   if m = 0 then rtac @{thm insertI1} i
   else rtac @{thm insertI2} i THEN set_member_tac (m - 1) i
@@ -276,7 +271,7 @@
         THEN steps_tac label strict (nth lev q) (nth lev p)
       end
 
-    val (mk_set, setT) = if label = MS then (mk_mset, msetT) else (mk_set, setT)
+    val (mk_set, setT) = if label = MS then (mk_mset, msetT) else (HOLogic.mk_set, setT)
 
     fun tag_pair p (i, tag) =
       HOLogic.pair_const natT natT $
diff -r 4caf15ae8c26 -r 7655e6533209 src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Wed Mar 11 15:56:50 2009 +0100
+++ b/src/HOL/Tools/hologic.ML	Wed Mar 11 15:56:51 2009 +0100
@@ -11,13 +11,20 @@
   val typeT: typ
   val boolN: string
   val boolT: typ
+  val Trueprop: term
+  val mk_Trueprop: term -> term
+  val dest_Trueprop: term -> term
   val true_const: term
   val false_const: term
   val mk_setT: typ -> typ
   val dest_setT: typ -> typ
-  val Trueprop: term
-  val mk_Trueprop: term -> term
-  val dest_Trueprop: term -> term
+  val Collect_const: typ -> term
+  val mk_Collect: string * typ * term -> term
+  val mk_mem: term * term -> term
+  val dest_mem: term -> term * term
+  val mk_set: typ -> term list -> term
+  val dest_set: term -> term list
+  val mk_UNIV: typ -> term
   val conj_intr: thm -> thm -> thm
   val conj_elim: thm -> thm * thm
   val conj_elims: thm -> thm list
@@ -43,12 +50,7 @@
   val exists_const: typ -> term
   val mk_exists: string * typ * term -> term
   val choice_const: typ -> term
-  val Collect_const: typ -> term
-  val mk_Collect: string * typ * term -> term
   val class_eq: string
-  val mk_mem: term * term -> term
-  val dest_mem: term -> term * term
-  val mk_UNIV: typ -> term
   val mk_binop: string -> term * term -> term
   val mk_binrel: string -> term * term -> term
   val dest_bin: string -> typ -> term -> term * term
@@ -139,6 +141,30 @@
 fun dest_setT (Type ("fun", [T, Type ("bool", [])])) = T
   | dest_setT T = raise TYPE ("dest_setT: set type expected", [T], []);
 
+fun mk_set T ts =
+  let
+    val sT = mk_setT T;
+    val empty = Const ("Orderings.bot", sT);
+    fun insert t u = Const ("insert", T --> sT --> sT) $ t $ u;
+  in fold_rev insert ts empty end;
+
+fun mk_UNIV T = Const ("Set.UNIV", mk_setT T);
+
+fun dest_set (Const ("Orderings.bot", _)) = []
+  | dest_set (Const ("insert", _) $ t $ u) = t :: dest_set u
+  | dest_set t = raise TERM ("dest_set", [t]);
+
+fun Collect_const T = Const ("Collect", (T --> boolT) --> mk_setT T);
+fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T, t);
+
+fun mk_mem (x, A) =
+  let val setT = fastype_of A in
+    Const ("op :", dest_setT setT --> setT --> boolT) $ x $ A
+  end;
+
+fun dest_mem (Const ("op :", _) $ x $ A) = (x, A)
+  | dest_mem t = raise TERM ("dest_mem", [t]);
+
 
 (* logic *)
 
@@ -212,21 +238,8 @@
 
 fun choice_const T = Const("Hilbert_Choice.Eps", (T --> boolT) --> T);
 
-fun Collect_const T = Const ("Collect", [T --> boolT] ---> mk_setT T);
-fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T, t);
-
 val class_eq = "HOL.eq";
 
-fun mk_mem (x, A) =
-  let val setT = fastype_of A in
-    Const ("op :", [dest_setT setT, setT] ---> boolT) $ x $ A
-  end;
-
-fun dest_mem (Const ("op :", _) $ x $ A) = (x, A)
-  | dest_mem t = raise TERM ("dest_mem", [t]);
-
-fun mk_UNIV T = Const ("Set.UNIV", mk_setT T);
-
 
 (* binary operations and relations *)
 
diff -r 4caf15ae8c26 -r 7655e6533209 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Wed Mar 11 15:56:50 2009 +0100
+++ b/src/HOL/Tools/refute.ML	Wed Mar 11 15:56:51 2009 +0100
@@ -2111,7 +2111,7 @@
           val HOLogic_prodT = HOLogic.mk_prodT (T1, T2)
           val HOLogic_setT  = HOLogic.mk_setT HOLogic_prodT
           (* Term.term *)
-          val HOLogic_empty_set = Const (@{const_name Set.empty}, HOLogic_setT)
+          val HOLogic_empty_set = HOLogic.mk_set HOLogic_prodT []
           val HOLogic_insert    =
             Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
         in
@@ -3187,7 +3187,7 @@
         val HOLogic_prodT = HOLogic.mk_prodT (T1, T2)
         val HOLogic_setT  = HOLogic.mk_setT HOLogic_prodT
         (* Term.term *)
-        val HOLogic_empty_set = Const (@{const_name Set.empty}, HOLogic_setT)
+        val HOLogic_empty_set = HOLogic.mk_set HOLogic_prodT []
         val HOLogic_insert    =
           Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
       in