--- a/src/HOL/FunDef.thy Wed Mar 11 13:53:51 2009 +0100
+++ b/src/HOL/FunDef.thy Wed Mar 11 18:32:23 2009 +0100
@@ -229,7 +229,7 @@
definition "max_strict = max_ext pair_less"
definition [code del]: "max_weak = max_ext pair_leq \<union> {({}, {})}"
definition [code del]: "min_strict = min_ext pair_less"
-definition "min_weak = min_ext pair_leq \<union> {({}, {})}"
+definition [code del]: "min_weak = min_ext pair_leq \<union> {({}, {})}"
lemma wf_pair_less[simp]: "wf pair_less"
by (auto simp: pair_less_def)
--- a/src/HOL/Import/proof_kernel.ML Wed Mar 11 13:53:51 2009 +0100
+++ b/src/HOL/Import/proof_kernel.ML Wed Mar 11 18:32:23 2009 +0100
@@ -264,7 +264,6 @@
structure Lib =
struct
-fun wrap b e s = String.concat[b,s,e]
fun assoc x =
let
@@ -280,9 +279,6 @@
| itr (a::rst) = i=a orelse itr rst
in itr L end;
-fun mk_set [] = []
- | mk_set (a::rst) = insert (op =) a (mk_set rst)
-
fun [] union S = S
| S union [] = S
| (a::rst) union S2 = rst union (insert (op =) a S2)
--- a/src/HOL/Nominal/nominal_inductive2.ML Wed Mar 11 13:53:51 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML Wed Mar 11 18:32:23 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 13:53:51 2009 +0100
+++ b/src/HOL/Nominal/nominal_package.ML Wed Mar 11 18:32:23 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 13:53:51 2009 +0100
+++ b/src/HOL/SizeChange/sct.ML Wed Mar 11 18:32:23 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/cooper.ML Wed Mar 11 13:53:51 2009 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML Wed Mar 11 18:32:23 2009 +0100
@@ -428,7 +428,7 @@
in
fun provein x S =
case term_of S of
- Const(@{const_name Set.empty}, _) => error "Unexpected error in Cooper please email Amine Chaieb"
+ Const(@{const_name Set.empty}, _) => error "Unexpected error in Cooper, please email Amine Chaieb"
| Const(@{const_name insert}, _) $ y $ _ =>
let val (cy,S') = Thm.dest_binop S
in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
--- a/src/HOL/Tools/function_package/fundef_lib.ML Wed Mar 11 13:53:51 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_lib.ML Wed Mar 11 18:32:23 2009 +0100
@@ -167,12 +167,10 @@
end
(* instance for unions *)
-fun regroup_union_conv t =
- regroup_conv (@{const_name Set.empty})
- @{const_name Un}
- (map (fn t => t RS eq_reflection) (@{thms "Un_ac"} @
- @{thms "Un_empty_right"} @
- @{thms "Un_empty_left"})) t
+fun regroup_union_conv t = regroup_conv @{const_name Set.empty} @{const_name Un}
+ (map (fn t => t RS eq_reflection) (@{thms "Un_ac"} @
+ @{thms "Un_empty_right"} @
+ @{thms "Un_empty_left"})) t
end
--- a/src/HOL/Tools/function_package/scnp_reconstruct.ML Wed Mar 11 13:53:51 2009 +0100
+++ b/src/HOL/Tools/function_package/scnp_reconstruct.ML Wed Mar 11 18:32:23 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 13:53:51 2009 +0100
+++ b/src/HOL/Tools/hologic.ML Wed Mar 11 18:32:23 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/hologic.ML
- ID: $Id$
Author: Lawrence C Paulson and Markus Wenzel
Abstract syntax operations for HOL.
@@ -11,13 +10,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 +49,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 +140,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 ("Set.empty", 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 +237,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/primrec_package.ML Wed Mar 11 13:53:51 2009 +0100
+++ b/src/HOL/Tools/primrec_package.ML Wed Mar 11 18:32:23 2009 +0100
@@ -26,7 +26,7 @@
fun primrec_error msg = raise PrimrecError (msg, NONE);
fun primrec_error_eqn msg eqn = raise PrimrecError (msg, SOME eqn);
-fun message s = if ! Toplevel.debug then () else writeln s;
+fun message s = if ! Toplevel.debug then tracing s else ();
(* preprocessing of equations *)
@@ -187,14 +187,13 @@
fun make_def ctxt fixes fs (fname, ls, rec_name, tname) =
let
- val raw_rhs = fold_rev (fn T => fn t => Abs ("", T, t))
- (map snd ls @ [dummyT])
- (list_comb (Const (rec_name, dummyT),
- fs @ map Bound (0 :: (length ls downto 1))))
+ val SOME (var, varT) = get_first (fn ((b, T), mx) =>
+ if Binding.name_of b = fname then SOME ((b, mx), T) else NONE) fixes;
val def_name = Thm.def_name (Long_Name.base_name fname);
- val rhs = singleton (Syntax.check_terms ctxt) raw_rhs;
- val SOME var = get_first (fn ((b, _), mx) =>
- if Binding.name_of b = fname then SOME (b, mx) else NONE) fixes;
+ val raw_rhs = fold_rev (fn T => fn t => Abs ("", T, t)) (map snd ls @ [dummyT])
+ (list_comb (Const (rec_name, dummyT), fs @ map Bound (0 :: (length ls downto 1))))
+ val rhs = singleton (Syntax.check_terms ctxt)
+ (TypeInfer.constrain varT raw_rhs);
in (var, ((Binding.name def_name, []), rhs)) end;
@@ -220,12 +219,12 @@
raw_fixes (map (single o apsnd single) raw_spec) ctxt
in (fixes, map (apsnd the_single) spec) end;
-fun prove_spec ctxt names rec_rewrites defs =
+fun prove_spec ctxt names rec_rewrites defs eqs =
let
val rewrites = map mk_meta_eq rec_rewrites @ map (snd o snd) defs;
fun tac _ = EVERY [rewrite_goals_tac rewrites, rtac refl 1];
val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names);
- in map (fn (a, t) => (a, [Goal.prove ctxt [] [] t tac])) end;
+ in map (fn (a, t) => (a, [Goal.prove ctxt [] [] t tac])) eqs end;
fun gen_primrec set_group prep_spec raw_fixes raw_spec lthy =
let
--- a/src/HOL/Tools/refute.ML Wed Mar 11 13:53:51 2009 +0100
+++ b/src/HOL/Tools/refute.ML Wed Mar 11 18:32:23 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
--- a/src/HOL/ex/ExecutableContent.thy Wed Mar 11 13:53:51 2009 +0100
+++ b/src/HOL/ex/ExecutableContent.thy Wed Mar 11 18:32:23 2009 +0100
@@ -24,6 +24,4 @@
"~~/src/HOL/ex/Records"
begin
-declare min_weak_def [code del]
-
end