1.1 --- a/NEWS Sat Mar 17 11:35:18 2012 +0100
1.2 +++ b/NEWS Sat Mar 17 11:57:03 2012 +0100
1.3 @@ -48,6 +48,10 @@
1.4
1.5 *** Pure ***
1.6
1.7 +* Command 'definition' no longer exports the foundational "raw_def"
1.8 +into the user context. Minor INCOMPATIBILITY, may use the regular
1.9 +"def" result with attribute "abs_def" to imitate the old version.
1.10 +
1.11 * Attribute "abs_def" turns an equation of the form "f x y == t" into
1.12 "f == %x y. t", which ensures that "simp" or "unfold" steps always
1.13 expand it. This also works for object-logic equality. (Formerly
2.1 --- a/src/HOL/Orderings.thy Sat Mar 17 11:35:18 2012 +0100
2.2 +++ b/src/HOL/Orderings.thy Sat Mar 17 11:57:03 2012 +0100
2.3 @@ -1314,7 +1314,6 @@
2.4
2.5 definition
2.6 [no_atp]: "\<top> = (\<lambda>x. \<top>)"
2.7 -declare top_fun_def_raw [no_atp]
2.8
2.9 lemma top_apply [simp] (* CANDIDATE [code] *):
2.10 "\<top> x = \<top>"
3.1 --- a/src/HOL/Quickcheck.thy Sat Mar 17 11:35:18 2012 +0100
3.2 +++ b/src/HOL/Quickcheck.thy Sat Mar 17 11:57:03 2012 +0100
3.3 @@ -43,8 +43,9 @@
3.4 instantiation itself :: (typerep) random
3.5 begin
3.6
3.7 -definition random_itself :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
3.8 - "random_itself _ = Pair (Code_Evaluation.valtermify TYPE('a))"
3.9 +definition
3.10 + random_itself :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a itself \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
3.11 +where "random_itself _ = Pair (Code_Evaluation.valtermify TYPE('a))"
3.12
3.13 instance ..
3.14
3.15 @@ -73,7 +74,9 @@
3.16 instantiation nat :: random
3.17 begin
3.18
3.19 -definition random_nat :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed" where
3.20 +definition random_nat :: "code_numeral \<Rightarrow> Random.seed
3.21 + \<Rightarrow> (nat \<times> (unit \<Rightarrow> Code_Evaluation.term)) \<times> Random.seed"
3.22 +where
3.23 "random_nat i = Random.range (i + 1) \<circ>\<rightarrow> (\<lambda>k. Pair (
3.24 let n = Code_Numeral.nat_of k
3.25 in (n, \<lambda>_. Code_Evaluation.term_of n)))"
3.26 @@ -100,18 +103,22 @@
3.27 text {* Towards @{typ "'a \<Rightarrow> 'b"} *}
3.28
3.29 axiomatization random_fun_aux :: "typerep \<Rightarrow> typerep \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> term)
3.30 - \<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed)
3.31 + \<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
3.32 + \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed)
3.33 \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
3.34
3.35 definition random_fun_lift :: "(Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
3.36 - \<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
3.37 - "random_fun_lift f = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Evaluation.term_of f Random.split_seed"
3.38 + \<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
3.39 +where
3.40 + "random_fun_lift f =
3.41 + random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Evaluation.term_of f Random.split_seed"
3.42
3.43 instantiation "fun" :: ("{equal, term_of}", random) random
3.44 begin
3.45
3.46 -definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
3.47 - "random i = random_fun_lift (random i)"
3.48 +definition
3.49 + random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
3.50 + where "random i = random_fun_lift (random i)"
3.51
3.52 instance ..
3.53
3.54 @@ -119,19 +126,21 @@
3.55
3.56 text {* Towards type copies and datatypes *}
3.57
3.58 -definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
3.59 - "collapse f = (f \<circ>\<rightarrow> id)"
3.60 +definition collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a"
3.61 + where "collapse f = (f \<circ>\<rightarrow> id)"
3.62
3.63 -definition beyond :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral" where
3.64 - "beyond k l = (if l > k then l else 0)"
3.65 +definition beyond :: "code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
3.66 + where "beyond k l = (if l > k then l else 0)"
3.67
3.68 -lemma beyond_zero:
3.69 - "beyond k 0 = 0"
3.70 +lemma beyond_zero: "beyond k 0 = 0"
3.71 by (simp add: beyond_def)
3.72
3.73
3.74 -definition (in term_syntax) [code_unfold]: "valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)"
3.75 -definition (in term_syntax) [code_unfold]: "valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s"
3.76 +definition (in term_syntax) [code_unfold]:
3.77 + "valterm_emptyset = Code_Evaluation.valtermify ({} :: ('a :: typerep) set)"
3.78 +
3.79 +definition (in term_syntax) [code_unfold]:
3.80 + "valtermify_insert x s = Code_Evaluation.valtermify insert {\<cdot>} (x :: ('a :: typerep * _)) {\<cdot>} s"
3.81
3.82 instantiation set :: (random) random
3.83 begin
3.84 @@ -139,12 +148,17 @@
3.85 primrec random_aux_set
3.86 where
3.87 "random_aux_set 0 j = collapse (Random.select_weight [(1, Pair valterm_emptyset)])"
3.88 -| "random_aux_set (Code_Numeral.Suc i) j = collapse (Random.select_weight [(1, Pair valterm_emptyset), (Code_Numeral.Suc i, random j \<circ>\<rightarrow> (%x. random_aux_set i j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
3.89 +| "random_aux_set (Code_Numeral.Suc i) j =
3.90 + collapse (Random.select_weight
3.91 + [(1, Pair valterm_emptyset),
3.92 + (Code_Numeral.Suc i,
3.93 + random j \<circ>\<rightarrow> (%x. random_aux_set i j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
3.94
3.95 lemma [code]:
3.96 - "random_aux_set i j = collapse (Random.select_weight [(1, Pair valterm_emptyset), (i, random j \<circ>\<rightarrow> (%x. random_aux_set (i - 1) j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
3.97 + "random_aux_set i j =
3.98 + collapse (Random.select_weight [(1, Pair valterm_emptyset),
3.99 + (i, random j \<circ>\<rightarrow> (%x. random_aux_set (i - 1) j \<circ>\<rightarrow> (%s. Pair (valtermify_insert x s))))])"
3.100 proof (induct i rule: code_numeral.induct)
3.101 -print_cases
3.102 case zero
3.103 show ?case by (subst select_weight_drop_zero[symmetric])
3.104 (simp add: filter.simps random_aux_set.simps[simplified])
3.105 @@ -153,9 +167,7 @@
3.106 show ?case by (simp only: random_aux_set.simps(2)[of "i"] Suc_code_numeral_minus_one)
3.107 qed
3.108
3.109 -definition random_set
3.110 -where
3.111 - "random_set i = random_aux_set i i"
3.112 +definition "random_set i = random_aux_set i i"
3.113
3.114 instance ..
3.115
3.116 @@ -190,13 +202,15 @@
3.117 subsection {* The Random-Predicate Monad *}
3.118
3.119 fun iter' ::
3.120 - "'a itself => code_numeral => code_numeral => code_numeral * code_numeral => ('a::random) Predicate.pred"
3.121 + "'a itself => code_numeral => code_numeral => code_numeral * code_numeral
3.122 + => ('a::random) Predicate.pred"
3.123 where
3.124 "iter' T nrandom sz seed = (if nrandom = 0 then bot_class.bot else
3.125 let ((x, _), seed') = random sz seed
3.126 in Predicate.Seq (%u. Predicate.Insert x (iter' T (nrandom - 1) sz seed')))"
3.127
3.128 -definition iter :: "code_numeral => code_numeral => code_numeral * code_numeral => ('a::random) Predicate.pred"
3.129 +definition iter :: "code_numeral => code_numeral => code_numeral * code_numeral
3.130 + => ('a::random) Predicate.pred"
3.131 where
3.132 "iter nrandom sz seed = iter' (TYPE('a)) nrandom sz seed"
3.133
3.134 @@ -248,22 +262,25 @@
3.135 where "map f P = bind P (single o f)"
3.136
3.137 hide_fact
3.138 - random_bool_def random_bool_def_raw
3.139 - random_itself_def random_itself_def_raw
3.140 - random_char_def random_char_def_raw
3.141 - random_literal_def random_literal_def_raw
3.142 - random_nat_def random_nat_def_raw
3.143 - random_int_def random_int_def_raw
3.144 - random_fun_lift_def random_fun_lift_def_raw
3.145 - random_fun_def random_fun_def_raw
3.146 - collapse_def collapse_def_raw
3.147 - beyond_def beyond_def_raw beyond_zero
3.148 + random_bool_def
3.149 + random_itself_def
3.150 + random_char_def
3.151 + random_literal_def
3.152 + random_nat_def
3.153 + random_int_def
3.154 + random_fun_lift_def
3.155 + random_fun_def
3.156 + collapse_def
3.157 + beyond_def
3.158 + beyond_zero
3.159 random_aux_rec
3.160
3.161 hide_const (open) catch_match random collapse beyond random_fun_aux random_fun_lift
3.162
3.163 -hide_fact (open) iter'.simps iter_def empty_def single_def bind_def union_def if_randompred_def iterate_upto_def not_randompred_def Random_def map_def
3.164 +hide_fact (open) iter'.simps iter_def empty_def single_def bind_def union_def
3.165 + if_randompred_def iterate_upto_def not_randompred_def Random_def map_def
3.166 hide_type (open) randompred
3.167 -hide_const (open) iter' iter empty single bind union if_randompred iterate_upto not_randompred Random map
3.168 +hide_const (open) iter' iter empty single bind union if_randompred
3.169 + iterate_upto not_randompred Random map
3.170
3.171 end
4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sat Mar 17 11:35:18 2012 +0100
4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sat Mar 17 11:57:03 2012 +0100
4.3 @@ -867,8 +867,7 @@
4.4 (not (Config.get ctxt ignore_no_atp) andalso
4.5 is_package_def name0) orelse
4.6 exists (fn s => String.isSuffix s name0)
4.7 - (multi_base_blacklist ctxt ho_atp) orelse
4.8 - String.isSuffix "_def_raw" (* FIXME: crude hack *) name0) then
4.9 + (multi_base_blacklist ctxt ho_atp)) then
4.10 I
4.11 else
4.12 let
5.1 --- a/src/Pure/Isar/locale.ML Sat Mar 17 11:35:18 2012 +0100
5.2 +++ b/src/Pure/Isar/locale.ML Sat Mar 17 11:57:03 2012 +0100
5.3 @@ -406,7 +406,7 @@
5.4 | SOME export => collect_mixins context (name, morph $> export) $> export);
5.5 val morph' = transfer input $> morph $> mixin;
5.6 val notes' =
5.7 - grouped 50 Par_List.map
5.8 + grouped 100 Par_List.map
5.9 (Element.transform_ctxt morph' o Notes o #1) (#notes (the_locale thy name));
5.10 in
5.11 fold_rev (fn elem => fn res => activ_elem (Element.transform_ctxt (transfer res) elem) res)
6.1 --- a/src/Pure/Tools/find_consts.ML Sat Mar 17 11:35:18 2012 +0100
6.2 +++ b/src/Pure/Tools/find_consts.ML Sat Mar 17 11:57:03 2012 +0100
6.3 @@ -36,11 +36,11 @@
6.4 fun opt_not f (c as (_, (ty, _))) =
6.5 if is_some (f c) then NONE else SOME (Term.size_of_typ ty);
6.6
6.7 -fun filter_const _ NONE = NONE
6.8 - | filter_const f (SOME (c, r)) =
6.9 +fun filter_const _ _ NONE = NONE
6.10 + | filter_const c f (SOME rank) =
6.11 (case f c of
6.12 NONE => NONE
6.13 - | SOME i => SOME (c, Int.min (r, i)));
6.14 + | SOME i => SOME (Int.min (rank, i)));
6.15
6.16
6.17 (* pretty results *)
6.18 @@ -103,14 +103,13 @@
6.19 val consts = Sign.consts_of thy;
6.20 val (_, consts_tab) = #constants (Consts.dest consts);
6.21 fun eval_entry c =
6.22 - fold filter_const (user_visible consts :: criteria)
6.23 - (SOME (c, low_ranking));
6.24 + fold (filter_const c) (user_visible consts :: criteria) (SOME low_ranking);
6.25
6.26 val matches =
6.27 - Symtab.fold (cons o eval_entry) consts_tab []
6.28 - |> map_filter I
6.29 - |> sort (rev_order o int_ord o pairself snd)
6.30 - |> map (apsnd fst o fst);
6.31 + Symtab.fold (fn c => (case eval_entry c of NONE => I | SOME rank => cons (rank, c)))
6.32 + consts_tab []
6.33 + |> sort (prod_ord (rev_order o int_ord) (string_ord o pairself fst))
6.34 + |> map (apsnd fst o snd);
6.35 in
6.36 Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) ::
6.37 Pretty.str "" ::
7.1 --- a/src/Pure/Tools/find_theorems.ML Sat Mar 17 11:35:18 2012 +0100
7.2 +++ b/src/Pure/Tools/find_theorems.ML Sat Mar 17 11:57:03 2012 +0100
7.3 @@ -420,7 +420,10 @@
7.4 then by the substitution size*)
7.5 fun result_ord (((p0, s0), _), ((p1, s1), _)) =
7.6 prod_ord int_ord int_ord ((p1, s1), (p0, s0));
7.7 - in map_filter eval_filters theorems |> sort result_ord |> map #2 end;
7.8 + in
7.9 + grouped 100 Par_List.map eval_filters theorems
7.10 + |> map_filter I |> sort result_ord |> map #2
7.11 + end;
7.12
7.13 fun lazy_filter filters =
7.14 let
7.15 @@ -581,7 +584,7 @@
7.16 (if null theorems then [Pretty.str "nothing found"]
7.17 else
7.18 [Pretty.str (tally_msg ^ ":"), Pretty.str ""] @
7.19 - map (pretty_theorem ctxt) theorems)
7.20 + grouped 10 Par_List.map (pretty_theorem ctxt) theorems)
7.21 end |> Pretty.chunks |> Pretty.writeln;
7.22
7.23 fun print_theorems ctxt =