HOLogic.mk_set, HOLogic.dest_set
authorhaftmann
Wed Mar 11 15:56:51 2009 +0100 (2009-03-11)
changeset 304507655e6533209
parent 30449 4caf15ae8c26
child 30451 11e5e8bb28f9
HOLogic.mk_set, HOLogic.dest_set
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_package.ML
src/HOL/SizeChange/sct.ML
src/HOL/Tools/Qelim/langford.ML
src/HOL/Tools/function_package/scnp_reconstruct.ML
src/HOL/Tools/hologic.ML
src/HOL/Tools/refute.ML
     1.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Mar 11 15:56:50 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Mar 11 15:56:51 2009 +0100
     1.3 @@ -75,11 +75,6 @@
     1.4    | add_binders thy i (Abs (_, _, t)) bs = add_binders thy (i + 1) t bs
     1.5    | add_binders thy i _ bs = bs;
     1.6  
     1.7 -fun mk_set T [] = Const (@{const_name Set.empty}, HOLogic.mk_setT T)
     1.8 -  | mk_set T (x :: xs) =
     1.9 -      Const ("insert", T --> HOLogic.mk_setT T --> HOLogic.mk_setT T) $ x $
    1.10 -        mk_set T xs;
    1.11 -
    1.12  fun split_conj f names (Const ("op &", _) $ p $ q) _ = (case head_of p of
    1.13        Const (name, _) =>
    1.14          if name mem names then SOME (f p q) else NONE
    1.15 @@ -216,7 +211,7 @@
    1.16        in
    1.17          (params,
    1.18           if null avoids then
    1.19 -           map (fn (T, ts) => (mk_set T ts, T))
    1.20 +           map (fn (T, ts) => (HOLogic.mk_set T ts, T))
    1.21               (fold (add_binders thy 0) (prems @ [concl]) [])
    1.22           else case AList.lookup op = avoids name of
    1.23             NONE => []
     2.1 --- a/src/HOL/Nominal/nominal_package.ML	Wed Mar 11 15:56:50 2009 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_package.ML	Wed Mar 11 15:56:51 2009 +0100
     2.3 @@ -1011,7 +1011,7 @@
     2.4              (augment_sort thy8 pt_cp_sort
     2.5                (HOLogic.mk_Trueprop (HOLogic.mk_eq
     2.6                  (supp c,
     2.7 -                 if null dts then Const (@{const_name Set.empty}, HOLogic.mk_setT atomT)
     2.8 +                 if null dts then HOLogic.mk_set atomT []
     2.9                   else foldr1 (HOLogic.mk_binop @{const_name Un}) (map supp args2)))))
    2.10              (fn _ =>
    2.11                simp_tac (HOL_basic_ss addsimps (supp_def ::
     3.1 --- a/src/HOL/SizeChange/sct.ML	Wed Mar 11 15:56:50 2009 +0100
     3.2 +++ b/src/HOL/SizeChange/sct.ML	Wed Mar 11 15:56:51 2009 +0100
     3.3 @@ -266,13 +266,6 @@
     3.4  
     3.5  fun mk_edge m G n = HOLogic.mk_prod (m, HOLogic.mk_prod (G, n))
     3.6  
     3.7 -fun mk_set T [] = Const (@{const_name Set.empty}, HOLogic.mk_setT T)
     3.8 -  | mk_set T (x :: xs) = Const (@{const_name insert},
     3.9 -      T --> HOLogic.mk_setT T --> HOLogic.mk_setT T) $ x $ mk_set T xs
    3.10 -
    3.11 -fun dest_set (Const (@{const_name Set.empty}, _)) = []
    3.12 -  | dest_set (Const (@{const_name insert}, _) $ x $ xs) = x :: dest_set xs
    3.13 -
    3.14  val in_graph_tac =
    3.15      simp_tac (HOL_basic_ss addsimps has_edge_simps) 1
    3.16      THEN SIMPSET (fn x => simp_tac x 1) (* FIXME reduce simpset *)
    3.17 @@ -333,7 +326,7 @@
    3.18  
    3.19  
    3.20        val ACG = map_filter (fn (Graph (G, _),(m, n)) => SOME (mk_edge (mk_number m) G (mk_number n)) | _ => NONE) (flat parts ~~ flat pairs)
    3.21 -                    |> mk_set (edgeT HOLogic.natT scgT)
    3.22 +                    |> HOLogic.mk_set (edgeT HOLogic.natT scgT)
    3.23                      |> curry op $ (graph_const HOLogic.natT scgT)
    3.24  
    3.25  
     4.1 --- a/src/HOL/Tools/Qelim/langford.ML	Wed Mar 11 15:56:50 2009 +0100
     4.2 +++ b/src/HOL/Tools/Qelim/langford.ML	Wed Mar 11 15:56:51 2009 +0100
     4.3 @@ -11,14 +11,6 @@
     4.4  structure LangfordQE :LANGFORD_QE = 
     4.5  struct
     4.6  
     4.7 -val dest_set =
     4.8 - let 
     4.9 -  fun h acc ct = 
    4.10 -   case term_of ct of
    4.11 -     Const (@{const_name Set.empty}, _) => acc
    4.12 -   | Const (@{const_name insert}, _) $ _ $ t => h (Thm.dest_arg1 ct :: acc) (Thm.dest_arg ct)
    4.13 -in h [] end;
    4.14 -
    4.15  fun prove_finite cT u = 
    4.16  let val [th0,th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"}
    4.17      fun ins x th =
    4.18 @@ -44,7 +36,7 @@
    4.19             val cT = ctyp_of_term a
    4.20             val ne = instantiate' [SOME cT] [SOME a, SOME A] 
    4.21                      @{thm insert_not_empty}
    4.22 -           val f = prove_finite cT (dest_set S)
    4.23 +           val f = prove_finite cT (HOLogic.dest_set S)
    4.24         in (ne, f) end
    4.25  
    4.26       val qe = case (term_of L, term_of U) of 
     5.1 --- a/src/HOL/Tools/function_package/scnp_reconstruct.ML	Wed Mar 11 15:56:50 2009 +0100
     5.2 +++ b/src/HOL/Tools/function_package/scnp_reconstruct.ML	Wed Mar 11 15:56:51 2009 +0100
     5.3 @@ -142,11 +142,6 @@
     5.4  
     5.5  val setT = HOLogic.mk_setT
     5.6  
     5.7 -fun mk_set T [] = Const (@{const_name Set.empty}, setT T)
     5.8 -  | mk_set T (x :: xs) =
     5.9 -      Const (@{const_name insert}, T --> setT T --> setT T) $
    5.10 -            x $ mk_set T xs
    5.11 -
    5.12  fun set_member_tac m i =
    5.13    if m = 0 then rtac @{thm insertI1} i
    5.14    else rtac @{thm insertI2} i THEN set_member_tac (m - 1) i
    5.15 @@ -276,7 +271,7 @@
    5.16          THEN steps_tac label strict (nth lev q) (nth lev p)
    5.17        end
    5.18  
    5.19 -    val (mk_set, setT) = if label = MS then (mk_mset, msetT) else (mk_set, setT)
    5.20 +    val (mk_set, setT) = if label = MS then (mk_mset, msetT) else (HOLogic.mk_set, setT)
    5.21  
    5.22      fun tag_pair p (i, tag) =
    5.23        HOLogic.pair_const natT natT $
     6.1 --- a/src/HOL/Tools/hologic.ML	Wed Mar 11 15:56:50 2009 +0100
     6.2 +++ b/src/HOL/Tools/hologic.ML	Wed Mar 11 15:56:51 2009 +0100
     6.3 @@ -11,13 +11,20 @@
     6.4    val typeT: typ
     6.5    val boolN: string
     6.6    val boolT: typ
     6.7 +  val Trueprop: term
     6.8 +  val mk_Trueprop: term -> term
     6.9 +  val dest_Trueprop: term -> term
    6.10    val true_const: term
    6.11    val false_const: term
    6.12    val mk_setT: typ -> typ
    6.13    val dest_setT: typ -> typ
    6.14 -  val Trueprop: term
    6.15 -  val mk_Trueprop: term -> term
    6.16 -  val dest_Trueprop: term -> term
    6.17 +  val Collect_const: typ -> term
    6.18 +  val mk_Collect: string * typ * term -> term
    6.19 +  val mk_mem: term * term -> term
    6.20 +  val dest_mem: term -> term * term
    6.21 +  val mk_set: typ -> term list -> term
    6.22 +  val dest_set: term -> term list
    6.23 +  val mk_UNIV: typ -> term
    6.24    val conj_intr: thm -> thm -> thm
    6.25    val conj_elim: thm -> thm * thm
    6.26    val conj_elims: thm -> thm list
    6.27 @@ -43,12 +50,7 @@
    6.28    val exists_const: typ -> term
    6.29    val mk_exists: string * typ * term -> term
    6.30    val choice_const: typ -> term
    6.31 -  val Collect_const: typ -> term
    6.32 -  val mk_Collect: string * typ * term -> term
    6.33    val class_eq: string
    6.34 -  val mk_mem: term * term -> term
    6.35 -  val dest_mem: term -> term * term
    6.36 -  val mk_UNIV: typ -> term
    6.37    val mk_binop: string -> term * term -> term
    6.38    val mk_binrel: string -> term * term -> term
    6.39    val dest_bin: string -> typ -> term -> term * term
    6.40 @@ -139,6 +141,30 @@
    6.41  fun dest_setT (Type ("fun", [T, Type ("bool", [])])) = T
    6.42    | dest_setT T = raise TYPE ("dest_setT: set type expected", [T], []);
    6.43  
    6.44 +fun mk_set T ts =
    6.45 +  let
    6.46 +    val sT = mk_setT T;
    6.47 +    val empty = Const ("Orderings.bot", sT);
    6.48 +    fun insert t u = Const ("insert", T --> sT --> sT) $ t $ u;
    6.49 +  in fold_rev insert ts empty end;
    6.50 +
    6.51 +fun mk_UNIV T = Const ("Set.UNIV", mk_setT T);
    6.52 +
    6.53 +fun dest_set (Const ("Orderings.bot", _)) = []
    6.54 +  | dest_set (Const ("insert", _) $ t $ u) = t :: dest_set u
    6.55 +  | dest_set t = raise TERM ("dest_set", [t]);
    6.56 +
    6.57 +fun Collect_const T = Const ("Collect", (T --> boolT) --> mk_setT T);
    6.58 +fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T, t);
    6.59 +
    6.60 +fun mk_mem (x, A) =
    6.61 +  let val setT = fastype_of A in
    6.62 +    Const ("op :", dest_setT setT --> setT --> boolT) $ x $ A
    6.63 +  end;
    6.64 +
    6.65 +fun dest_mem (Const ("op :", _) $ x $ A) = (x, A)
    6.66 +  | dest_mem t = raise TERM ("dest_mem", [t]);
    6.67 +
    6.68  
    6.69  (* logic *)
    6.70  
    6.71 @@ -212,21 +238,8 @@
    6.72  
    6.73  fun choice_const T = Const("Hilbert_Choice.Eps", (T --> boolT) --> T);
    6.74  
    6.75 -fun Collect_const T = Const ("Collect", [T --> boolT] ---> mk_setT T);
    6.76 -fun mk_Collect (a, T, t) = Collect_const T $ absfree (a, T, t);
    6.77 -
    6.78  val class_eq = "HOL.eq";
    6.79  
    6.80 -fun mk_mem (x, A) =
    6.81 -  let val setT = fastype_of A in
    6.82 -    Const ("op :", [dest_setT setT, setT] ---> boolT) $ x $ A
    6.83 -  end;
    6.84 -
    6.85 -fun dest_mem (Const ("op :", _) $ x $ A) = (x, A)
    6.86 -  | dest_mem t = raise TERM ("dest_mem", [t]);
    6.87 -
    6.88 -fun mk_UNIV T = Const ("Set.UNIV", mk_setT T);
    6.89 -
    6.90  
    6.91  (* binary operations and relations *)
    6.92  
     7.1 --- a/src/HOL/Tools/refute.ML	Wed Mar 11 15:56:50 2009 +0100
     7.2 +++ b/src/HOL/Tools/refute.ML	Wed Mar 11 15:56:51 2009 +0100
     7.3 @@ -2111,7 +2111,7 @@
     7.4            val HOLogic_prodT = HOLogic.mk_prodT (T1, T2)
     7.5            val HOLogic_setT  = HOLogic.mk_setT HOLogic_prodT
     7.6            (* Term.term *)
     7.7 -          val HOLogic_empty_set = Const (@{const_name Set.empty}, HOLogic_setT)
     7.8 +          val HOLogic_empty_set = HOLogic.mk_set HOLogic_prodT []
     7.9            val HOLogic_insert    =
    7.10              Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
    7.11          in
    7.12 @@ -3187,7 +3187,7 @@
    7.13          val HOLogic_prodT = HOLogic.mk_prodT (T1, T2)
    7.14          val HOLogic_setT  = HOLogic.mk_setT HOLogic_prodT
    7.15          (* Term.term *)
    7.16 -        val HOLogic_empty_set = Const (@{const_name Set.empty}, HOLogic_setT)
    7.17 +        val HOLogic_empty_set = HOLogic.mk_set HOLogic_prodT []
    7.18          val HOLogic_insert    =
    7.19            Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
    7.20        in