# HG changeset patch # User haftmann # Date 1236792743 -3600 # Node ID c816b6dcc8afb0d2932ef89fb1bb72f2e1bf9823 # Parent 873fa77be5f0990680c755665245d9dc00981bf7# Parent 1e7e0d1716536221c385f6217cbe0771025d9a71 merged diff -r 873fa77be5f0 -r c816b6dcc8af src/HOL/FunDef.thy --- 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 \ {({}, {})}" definition [code del]: "min_strict = min_ext pair_less" -definition "min_weak = min_ext pair_leq \ {({}, {})}" +definition [code del]: "min_weak = min_ext pair_leq \ {({}, {})}" lemma wf_pair_less[simp]: "wf pair_less" by (auto simp: pair_less_def) diff -r 873fa77be5f0 -r c816b6dcc8af src/HOL/Import/proof_kernel.ML --- 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) diff -r 873fa77be5f0 -r c816b6dcc8af src/HOL/Nominal/nominal_inductive2.ML --- 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 => [] diff -r 873fa77be5f0 -r c816b6dcc8af src/HOL/Nominal/nominal_package.ML --- 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 :: diff -r 873fa77be5f0 -r c816b6dcc8af src/HOL/SizeChange/sct.ML --- 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) diff -r 873fa77be5f0 -r c816b6dcc8af src/HOL/Tools/Qelim/cooper.ML --- 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 diff -r 873fa77be5f0 -r c816b6dcc8af src/HOL/Tools/Qelim/langford.ML diff -r 873fa77be5f0 -r c816b6dcc8af src/HOL/Tools/function_package/fundef_lib.ML --- 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 diff -r 873fa77be5f0 -r c816b6dcc8af src/HOL/Tools/function_package/scnp_reconstruct.ML --- 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 $ diff -r 873fa77be5f0 -r c816b6dcc8af src/HOL/Tools/hologic.ML --- 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 *) diff -r 873fa77be5f0 -r c816b6dcc8af src/HOL/Tools/primrec_package.ML --- 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 diff -r 873fa77be5f0 -r c816b6dcc8af src/HOL/Tools/refute.ML --- 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 diff -r 873fa77be5f0 -r c816b6dcc8af src/HOL/ex/ExecutableContent.thy --- 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