--- 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 => []
--- 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 ::
--- 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)
--- 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
--- 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 $
--- 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 *)
--- 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