--- a/src/HOL/Int.thy Tue Mar 31 11:04:05 2009 +0200
+++ b/src/HOL/Int.thy Tue Mar 31 11:04:34 2009 +0200
@@ -12,7 +12,7 @@
uses
("Tools/numeral.ML")
("Tools/numeral_syntax.ML")
- ("~~/src/Provers/Arith/assoc_fold.ML")
+ "~~/src/Provers/Arith/assoc_fold.ML"
"~~/src/Provers/Arith/cancel_numerals.ML"
"~~/src/Provers/Arith/combine_numerals.ML"
("Tools/int_arith.ML")
@@ -1525,7 +1525,17 @@
lemmas zle_int = of_nat_le_iff [where 'a=int]
lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
-use "~~/src/Provers/Arith/assoc_fold.ML"
+subsection {* Setting up simplification procedures *}
+
+lemmas int_arith_rules =
+ neg_le_iff_le numeral_0_eq_0 numeral_1_eq_1
+ minus_zero diff_minus left_minus right_minus
+ mult_zero_left mult_zero_right mult_Bit1 mult_1_right
+ mult_minus_left mult_minus_right
+ minus_add_distrib minus_minus mult_assoc
+ of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult
+ of_int_0 of_int_1 of_int_add of_int_mult
+
use "Tools/int_arith.ML"
declaration {* K Int_Arith.setup *}
--- a/src/HOL/Orderings.thy Tue Mar 31 11:04:05 2009 +0200
+++ b/src/HOL/Orderings.thy Tue Mar 31 11:04:34 2009 +0200
@@ -384,15 +384,11 @@
(** Diagnostic command **)
-val print = Toplevel.unknown_context o
- Toplevel.keep (Toplevel.node_case
- (Context.cases (print_structures o ProofContext.init) print_structures)
- (print_structures o Proof.context_of));
-
val _ =
OuterSyntax.improper_command "print_orders"
"print order structures available to transitivity reasoner" OuterKeyword.diag
- (Scan.succeed (Toplevel.no_timing o print));
+ (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+ Toplevel.keep (print_structures o Toplevel.context_of)));
(** Setup **)
--- a/src/HOL/Tools/atp_manager.ML Tue Mar 31 11:04:05 2009 +0200
+++ b/src/HOL/Tools/atp_manager.ML Tue Mar 31 11:04:34 2009 +0200
@@ -19,7 +19,7 @@
val kill: unit -> unit
val info: unit -> unit
val messages: int option -> unit
- type prover = int -> int -> Proof.context * (thm list * thm) -> bool * string
+ type prover = int -> int -> Proof.context * (thm list * thm) -> bool * string
val add_prover: string -> prover -> theory -> theory
val print_provers: theory -> unit
val sledgehammer: string list -> Proof.state -> unit
@@ -96,6 +96,12 @@
State {timeout_heap = timeout_heap, oldest_heap = oldest_heap,
active = active, cancelling = cancelling, messages = messages, store = store};
+fun empty_state state =
+ let
+ val State {active = active, cancelling = cancelling, messages = messages, ...} =
+ Synchronized.value state
+ in (null active) andalso (null cancelling) andalso (null messages) end;
+
val state = Synchronized.var "atp_manager" (make_state ThreadHeap.empty ThreadHeap.empty [] [] [] []);
@@ -127,7 +133,7 @@
(if length store <= message_store_limit then store
else #1 (chop message_store_limit store))
in make_state timeout_heap oldest_heap active' cancelling' (message' :: messages) store' end
- | NONE =>state));
+ | NONE => state));
(* kill excessive atp threads *)
@@ -162,12 +168,14 @@
fun print_new_messages () =
let val to_print = Synchronized.change_result state
(fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
- (messages, make_state timeout_heap oldest_heap active cancelling [] store))
- in if null to_print then ()
- else priority ("Sledgehammer: " ^ (space_implode "\n\n" to_print)) end;
+ (messages, make_state timeout_heap oldest_heap active cancelling [] store))
+ in
+ if null to_print then ()
+ else priority ("Sledgehammer: " ^ space_implode "\n\n" to_print)
+ end;
-(* start a watching thread which runs forever -- only one may exist *)
+(* start a watching thread -- only one may exist *)
fun check_thread_manager () = CRITICAL (fn () =>
if (case ! managing_thread of SOME thread => Thread.isActive thread | NONE => false)
@@ -197,7 +205,7 @@
in SOME (map #2 timeout_threads, state') end
end
in
- while true do
+ while not (empty_state state) do
(Synchronized.timed_access state time_limit action
|> these
|> List.app (unregister (false, "Interrupted (reached timeout)"));
@@ -211,14 +219,14 @@
(* thread is registered here by sledgehammer *)
fun register birthtime deadtime (thread, desc) =
- (check_thread_manager ();
- Synchronized.change state
+ (Synchronized.change state
(fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
let
val timeout_heap' = ThreadHeap.insert (deadtime, thread) timeout_heap
val oldest_heap' = ThreadHeap.insert (birthtime, thread) oldest_heap
val active' = update_thread (thread, (birthtime, deadtime, desc)) active
- in make_state timeout_heap' oldest_heap' active' cancelling messages store end));
+ in make_state timeout_heap' oldest_heap' active' cancelling messages store end);
+ check_thread_manager ());
@@ -307,7 +315,7 @@
val _ = SimpleThread.fork true (fn () =>
let
val _ = register birthtime deadtime (Thread.self (), desc)
- val result = prover (get_timeout ()) i (Proof.get_goal proof_state)
+ val result = prover (get_timeout ()) i (Proof.get_goal proof_state)
handle ResHolClause.TOO_TRIVIAL
=> (true, "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
| ERROR msg
@@ -355,7 +363,7 @@
val _ =
OuterSyntax.command "sledgehammer" "call all automatic theorem provers" K.diag
(Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
- Toplevel.keep ((sledgehammer names) o Toplevel.proof_of)));
+ Toplevel.keep (sledgehammer names o Toplevel.proof_of)));
end;
--- a/src/HOL/Tools/function_package/fundef_common.ML Tue Mar 31 11:04:05 2009 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML Tue Mar 31 11:04:34 2009 +0200
@@ -65,7 +65,7 @@
defname : string,
(* contains no logical entities: invariant under morphisms *)
- add_simps : (string -> string) -> string -> Attrib.src list -> thm list
+ add_simps : (binding -> binding) -> string -> Attrib.src list -> thm list
-> local_theory -> thm list * local_theory,
case_names : string list,
@@ -289,8 +289,8 @@
(* Preprocessors *)
type fixes = ((string * typ) * mixfix) list
-type 'a spec = ((bstring * Attrib.src list) * 'a list) list
-type preproc = fundef_config -> bool list -> Proof.context -> fixes -> term spec
+type 'a spec = (Attrib.binding * 'a list) list
+type preproc = fundef_config -> Proof.context -> fixes -> term spec
-> (term list * (thm list -> thm spec) * (thm list -> thm list list) * string list)
val fname_of = fst o dest_Free o fst o strip_comb o fst
@@ -301,9 +301,9 @@
| mk_case_names _ n 1 = [n]
| mk_case_names _ n k = map (fn i => n ^ "_" ^ string_of_int i) (1 upto k)
-fun empty_preproc check _ _ ctxt fixes spec =
+fun empty_preproc check _ ctxt fixes spec =
let
- val (nas,tss) = split_list spec
+ val (bnds, tss) = split_list spec
val ts = flat tss
val _ = check ctxt fixes ts
val fnames = map (fst o fst) fixes
@@ -314,9 +314,9 @@
|> map (map snd)
(* using theorem names for case name currently disabled *)
- val cnames = map_index (fn (i, (n,_)) => mk_case_names i "" 1) nas |> flat
+ val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat
in
- (ts, curry op ~~ nas o Library.unflat tss, sort, cnames)
+ (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames)
end
structure Preprocessor = GenericDataFun
@@ -344,23 +344,9 @@
fun config_parser default =
(Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 option_parser) --| P.$$$ ")") [])
>> (fn opts => fold apply_opt opts default)
-
- val otherwise = P.$$$ "(" |-- P.$$$ "otherwise" --| P.$$$ ")"
-
- fun pipe_error t =
- P.!!! (Scan.fail_with (K (cat_lines ["Equations must be separated by " ^ quote "|", quote t])))
-
- val statement_ow =
- SpecParse.opt_thm_name ":" -- (P.prop -- Scan.optional (otherwise >> K true) false)
- --| Scan.ahead ((P.term :-- pipe_error) || Scan.succeed ("",""))
-
- val statements_ow = P.enum1 "|" statement_ow
-
- val flags_statements = statements_ow
- >> (fn sow => (map (snd o snd) sow, map (apsnd fst) sow))
in
fun fundef_parser default_cfg =
- config_parser default_cfg -- P.fixes --| P.where_ -- flags_statements
+ config_parser default_cfg -- P.fixes -- SpecParse.where_alt_specs
end
--- a/src/HOL/Tools/function_package/fundef_datatype.ML Tue Mar 31 11:04:05 2009 +0200
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML Tue Mar 31 11:04:34 2009 +0200
@@ -15,10 +15,10 @@
val add_fun : FundefCommon.fundef_config ->
(binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
- bool list -> bool -> local_theory -> Proof.context
+ bool -> local_theory -> Proof.context
val add_fun_cmd : FundefCommon.fundef_config ->
(binding * string option * mixfix) list -> (Attrib.binding * string) list ->
- bool list -> bool -> local_theory -> Proof.context
+ bool -> local_theory -> Proof.context
end
structure FundefDatatype : FUNDEF_DATATYPE =
@@ -235,50 +235,40 @@
end
fun add_catchall ctxt fixes spec =
- let
- val catchalls = mk_catchall fixes (mk_arities (map (split_def ctxt) (map snd spec)))
- in
- spec @ map (pair true) catchalls
- end
+ spec @ mk_catchall fixes (mk_arities (map (split_def ctxt) spec))
fun warn_if_redundant ctxt origs tss =
let
fun msg t = "Ignoring redundant equation: " ^ quote (Syntax.string_of_term ctxt t)
val (tss', _) = chop (length origs) tss
- fun check ((_, t), []) = (Output.warning (msg t); [])
- | check ((_, t), s) = s
+ fun check (t, []) = (Output.warning (msg t); [])
+ | check (t, s) = s
in
(map check (origs ~~ tss'); tss)
end
-fun sequential_preproc (config as FundefConfig {sequential, ...}) flags ctxt fixes spec =
- let
- val enabled = sequential orelse exists I flags
- in
- if enabled then
+fun sequential_preproc (config as FundefConfig {sequential, ...}) ctxt fixes spec =
+ if sequential then
let
- val flags' = if sequential then map (K true) flags else flags
-
- val (nas, eqss) = split_list spec
+ val (bnds, eqss) = split_list spec
val eqs = map the_single eqss
val feqs = eqs
|> tap (check_defs ctxt fixes) (* Standard checks *)
|> tap (map (check_pats ctxt)) (* More checks for sequential mode *)
- |> curry op ~~ flags'
val compleqs = add_catchall ctxt fixes feqs (* Completion *)
val spliteqs = warn_if_redundant ctxt feqs
- (FundefSplit.split_some_equations ctxt compleqs)
+ (FundefSplit.split_all_equations ctxt compleqs)
fun restore_spec thms =
- nas ~~ Library.take (length nas, Library.unflat spliteqs thms)
+ bnds ~~ Library.take (length bnds, Library.unflat spliteqs thms)
- val spliteqs' = flat (Library.take (length nas, spliteqs))
+ val spliteqs' = flat (Library.take (length bnds, spliteqs))
val fnames = map (fst o fst) fixes
val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) spliteqs'
@@ -286,18 +276,17 @@
|> map (map snd)
- val nas' = nas @ replicate (length spliteqs - length nas) ("",[])
+ val bnds' = bnds @ replicate (length spliteqs - length bnds) Attrib.empty_binding
(* using theorem names for case name currently disabled *)
- val case_names = map_index (fn (i, ((n, _), es)) => mk_case_names i "" (length es))
- (nas' ~~ spliteqs)
+ val case_names = map_index (fn (i, (_, es)) => mk_case_names i "" (length es))
+ (bnds' ~~ spliteqs)
|> flat
in
(flat spliteqs, restore_spec, sort, case_names)
end
else
- FundefCommon.empty_preproc check_defs config flags ctxt fixes spec
- end
+ FundefCommon.empty_preproc check_defs config ctxt fixes spec
val setup =
Method.setup @{binding pat_completeness} (Scan.succeed pat_completeness)
@@ -308,11 +297,11 @@
val fun_config = FundefConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*),
domintros=false, tailrec=false }
-fun gen_fun add config fixes statements flags int lthy =
+fun gen_fun add config fixes statements int lthy =
let val group = serial_string () in
lthy
|> LocalTheory.set_group group
- |> add fixes statements config flags
+ |> add fixes statements config
|> by_pat_completeness_auto int
|> LocalTheory.restore
|> LocalTheory.set_group group
@@ -329,7 +318,7 @@
val _ =
OuterSyntax.local_theory' "fun" "define general recursive functions (short version)" K.thy_decl
(fundef_parser fun_config
- >> (fn ((config, fixes), (flags, statements)) => add_fun_cmd config fixes statements flags));
+ >> (fn ((config, fixes), statements) => add_fun_cmd config fixes statements));
end
--- a/src/HOL/Tools/function_package/fundef_package.ML Tue Mar 31 11:04:05 2009 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML Tue Mar 31 11:04:34 2009 +0200
@@ -10,13 +10,11 @@
val add_fundef : (binding * typ option * mixfix) list
-> (Attrib.binding * term) list
-> FundefCommon.fundef_config
- -> bool list
-> local_theory
-> Proof.state
val add_fundef_cmd : (binding * string option * mixfix) list
- -> (Attrib.binding * string) list
+ -> (Attrib.binding * string) list
-> FundefCommon.fundef_config
- -> bool list
-> local_theory
-> Proof.state
@@ -36,20 +34,28 @@
open FundefLib
open FundefCommon
+val simp_attribs = map (Attrib.internal o K)
+ [Simplifier.simp_add,
+ Code.add_default_eqn_attribute,
+ Nitpick_Const_Simp_Thms.add]
+
+val psimp_attribs = map (Attrib.internal o K)
+ [Simplifier.simp_add,
+ Nitpick_Const_Psimp_Thms.add]
+
fun note_theorem ((name, atts), ths) =
LocalTheory.note Thm.theoremK ((Binding.qualified_name name, atts), ths)
-fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
+fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
fun add_simps fnames post sort extra_qualify label moreatts simps lthy =
let
- val atts = Attrib.internal (K Simplifier.simp_add) :: moreatts
val spec = post simps
- |> map (apfst (apsnd (append atts)))
+ |> map (apfst (apsnd (fn ats => moreatts @ ats)))
|> map (apfst (apfst extra_qualify))
val (saved_spec_simps, lthy) =
- fold_map note_theorem spec lthy
+ fold_map (LocalTheory.note Thm.theoremK) spec lthy
val saved_simps = flat (map snd saved_spec_simps)
val simps_by_f = sort saved_simps
@@ -72,15 +78,15 @@
val (((psimps', pinducts'), (_, [termination'])), lthy) =
lthy
- |> addsmps (Long_Name.qualify "partial") "psimps"
- [Attrib.internal (K Nitpick_Const_Psimp_Thms.add)] psimps
- ||> fold_option (snd oo addsmps I "simps" [Attrib.internal (K Nitpick_Const_Simp_Thms.add)]) trsimps
+ |> addsmps (Binding.qualify false "partial") "psimps"
+ psimp_attribs psimps
+ ||> fold_option (snd oo addsmps I "simps" simp_attribs) trsimps
||>> note_theorem ((qualify "pinduct",
[Attrib.internal (K (RuleCases.case_names cnames)),
Attrib.internal (K (RuleCases.consumes 1)),
Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
||>> note_theorem ((qualify "termination", []), [termination])
- ||> (snd o note_theorem ((qualify "cases",
+ ||> (snd o note_theorem ((qualify "cases",
[Attrib.internal (K (RuleCases.case_names cnames))]), [cases]))
||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
@@ -90,18 +96,18 @@
if not do_print then ()
else Specification.print_consts lthy (K false) (map fst fixes)
in
- lthy
+ lthy
|> LocalTheory.declaration (add_fundef_data o morph_fundef_data cdata)
end
-fun gen_add_fundef is_external prep default_constraint fixspec eqns config flags lthy =
+fun gen_add_fundef is_external prep default_constraint fixspec eqns config lthy =
let
val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
val fixes = map (apfst (apfst Binding.name_of)) fixes0;
- val spec = map (fn ((b, atts), prop) => ((Binding.name_of b, atts), [prop])) spec0;
- val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
+ val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0;
+ val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config ctxt' fixes spec
val defname = mk_defname fixes
@@ -131,14 +137,10 @@
val tsimps = map remove_domain_condition psimps
val tinduct = map remove_domain_condition pinducts
- val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
- val allatts = (not has_guards ? cons Code.add_default_eqn_attrib)
- [Attrib.internal (K Nitpick_Const_Simp_Thms.add)]
-
val qualify = Long_Name.qualify defname;
in
lthy
- |> add_simps I "simps" allatts tsimps |> snd
+ |> add_simps I "simps" simp_attribs tsimps |> snd
|> note_theorem ((qualify "induct", [Attrib.internal (K (RuleCases.case_names case_names))]), tinduct) |> snd
end
@@ -209,12 +211,10 @@
local structure P = OuterParse and K = OuterKeyword in
-val _ = OuterKeyword.keyword "otherwise";
-
val _ =
OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal
(fundef_parser default_config
- >> (fn ((config, fixes), (flags, statements)) => add_fundef_cmd fixes statements config flags));
+ >> (fn ((config, fixes), statements) => add_fundef_cmd fixes statements config));
val _ =
OuterSyntax.local_theory_to_proof "termination" "prove termination of a recursive function" K.thy_goal
--- a/src/HOL/Tools/int_arith.ML Tue Mar 31 11:04:05 2009 +0200
+++ b/src/HOL/Tools/int_arith.ML Tue Mar 31 11:04:34 2009 +0200
@@ -26,9 +26,6 @@
val reorient_simproc =
Arith_Data.prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc);
-(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*)
-val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym];
-
(** Utilities **)
@@ -176,10 +173,12 @@
val num_ss = HOL_ss settermless numtermless;
+(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*)
+val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym];
(*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *)
-val add_0s = thms "add_0s";
-val mult_1s = thms "mult_1s" @ [thm"mult_1_left", thm"mult_1_right", thm"divide_1"];
+val add_0s = @{thms add_0s};
+val mult_1s = @{thms mult_1s mult_1_left mult_1_right divide_1};
(*Simplify inverse Numeral1, a/Numeral1*)
val inverse_1s = [@{thm inverse_numeral_1}];
@@ -208,16 +207,21 @@
(*push the unary minus down: - x * y = x * - y *)
val minus_mult_eq_1_to_2 =
- [@{thm minus_mult_left} RS sym, @{thm minus_mult_right}] MRS trans |> standard;
+ [@{thm mult_minus_left}, @{thm minus_mult_right}] MRS trans |> standard;
(*to extract again any uncancelled minuses*)
val minus_from_mult_simps =
- [@{thm minus_minus}, @{thm minus_mult_left} RS sym, @{thm minus_mult_right} RS sym];
+ [@{thm minus_minus}, @{thm mult_minus_left}, @{thm mult_minus_right}];
(*combine unary minus with numeric literals, however nested within a product*)
val mult_minus_simps =
[@{thm mult_assoc}, @{thm minus_mult_left}, minus_mult_eq_1_to_2];
+val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
+ diff_simps @ minus_simps @ @{thms add_ac}
+val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
+val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
+
structure CancelNumeralsCommon =
struct
val mk_sum = mk_sum
@@ -227,10 +231,6 @@
val find_first_coeff = find_first_coeff []
val trans_tac = K Arith_Data.trans_tac
- val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
- diff_simps @ minus_simps @ @{thms add_ac}
- val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
- val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
fun norm_tac ss =
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
@@ -310,10 +310,6 @@
val prove_conv = Arith_Data.prove_conv_nohyps
val trans_tac = K Arith_Data.trans_tac
- val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
- diff_simps @ minus_simps @ @{thms add_ac}
- val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
- val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
fun norm_tac ss =
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
@@ -340,12 +336,9 @@
val prove_conv = Arith_Data.prove_conv_nohyps
val trans_tac = K Arith_Data.trans_tac
- val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
- inverse_1s @ divide_simps @ diff_simps @ minus_simps @ @{thms add_ac}
- val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
- val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
+ val norm_ss1a = norm_ss1 addsimps inverse_1s @ divide_simps
fun norm_tac ss =
- ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
+ ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1a))
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
@@ -516,14 +509,7 @@
val add_rules =
simp_thms @ @{thms arith_simps} @ @{thms rel_simps} @ @{thms arith_special} @
- [@{thm neg_le_iff_le}, @{thm numeral_0_eq_0}, @{thm numeral_1_eq_1},
- @{thm minus_zero}, @{thm diff_minus}, @{thm left_minus}, @{thm right_minus},
- @{thm mult_zero_left}, @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right},
- @{thm minus_mult_left} RS sym, @{thm minus_mult_right} RS sym,
- @{thm minus_add_distrib}, @{thm minus_minus}, @{thm mult_assoc},
- @{thm of_nat_0}, @{thm of_nat_1}, @{thm of_nat_Suc}, @{thm of_nat_add},
- @{thm of_nat_mult}, @{thm of_int_0}, @{thm of_int_1}, @{thm of_int_add},
- @{thm of_int_mult}]
+ @{thms int_arith_rules}
val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
--- a/src/HOL/ex/Numeral.thy Tue Mar 31 11:04:05 2009 +0200
+++ b/src/HOL/ex/Numeral.thy Tue Mar 31 11:04:34 2009 +0200
@@ -507,54 +507,78 @@
context ordered_idom
begin
-lemma minus_of_num_less_of_num_iff [numeral]: "- of_num m < of_num n"
+lemma minus_of_num_less_of_num_iff: "- of_num m < of_num n"
proof -
have "- of_num m < 0" by (simp add: of_num_pos)
also have "0 < of_num n" by (simp add: of_num_pos)
finally show ?thesis .
qed
-lemma minus_of_num_less_one_iff [numeral]: "- of_num n < 1"
-proof -
- have "- of_num n < 0" by (simp add: of_num_pos)
- also have "0 < 1" by simp
- finally show ?thesis .
-qed
+lemma minus_of_num_less_one_iff: "- of_num n < 1"
+using minus_of_num_less_of_num_iff [of n One] by (simp add: of_num_one)
-lemma minus_one_less_of_num_iff [numeral]: "- 1 < of_num n"
-proof -
- have "- 1 < 0" by simp
- also have "0 < of_num n" by (simp add: of_num_pos)
- finally show ?thesis .
-qed
+lemma minus_one_less_of_num_iff: "- 1 < of_num n"
+using minus_of_num_less_of_num_iff [of One n] by (simp add: of_num_one)
-lemma minus_of_num_le_of_num_iff [numeral]: "- of_num m \<le> of_num n"
+lemma minus_one_less_one_iff: "- 1 < 1"
+using minus_of_num_less_of_num_iff [of One One] by (simp add: of_num_one)
+
+lemma minus_of_num_le_of_num_iff: "- of_num m \<le> of_num n"
by (simp add: less_imp_le minus_of_num_less_of_num_iff)
-lemma minus_of_num_le_one_iff [numeral]: "- of_num n \<le> 1"
+lemma minus_of_num_le_one_iff: "- of_num n \<le> 1"
by (simp add: less_imp_le minus_of_num_less_one_iff)
-lemma minus_one_le_of_num_iff [numeral]: "- 1 \<le> of_num n"
+lemma minus_one_le_of_num_iff: "- 1 \<le> of_num n"
by (simp add: less_imp_le minus_one_less_of_num_iff)
-lemma of_num_le_minus_of_num_iff [numeral]: "\<not> of_num m \<le> - of_num n"
+lemma minus_one_le_one_iff: "- 1 \<le> 1"
+ by (simp add: less_imp_le minus_one_less_one_iff)
+
+lemma of_num_le_minus_of_num_iff: "\<not> of_num m \<le> - of_num n"
by (simp add: not_le minus_of_num_less_of_num_iff)
-lemma one_le_minus_of_num_iff [numeral]: "\<not> 1 \<le> - of_num n"
+lemma one_le_minus_of_num_iff: "\<not> 1 \<le> - of_num n"
by (simp add: not_le minus_of_num_less_one_iff)
-lemma of_num_le_minus_one_iff [numeral]: "\<not> of_num n \<le> - 1"
+lemma of_num_le_minus_one_iff: "\<not> of_num n \<le> - 1"
by (simp add: not_le minus_one_less_of_num_iff)
-lemma of_num_less_minus_of_num_iff [numeral]: "\<not> of_num m < - of_num n"
+lemma one_le_minus_one_iff: "\<not> 1 \<le> - 1"
+ by (simp add: not_le minus_one_less_one_iff)
+
+lemma of_num_less_minus_of_num_iff: "\<not> of_num m < - of_num n"
by (simp add: not_less minus_of_num_le_of_num_iff)
-lemma one_less_minus_of_num_iff [numeral]: "\<not> 1 < - of_num n"
+lemma one_less_minus_of_num_iff: "\<not> 1 < - of_num n"
by (simp add: not_less minus_of_num_le_one_iff)
-lemma of_num_less_minus_one_iff [numeral]: "\<not> of_num n < - 1"
+lemma of_num_less_minus_one_iff: "\<not> of_num n < - 1"
by (simp add: not_less minus_one_le_of_num_iff)
+lemma one_less_minus_one_iff: "\<not> 1 < - 1"
+ by (simp add: not_less minus_one_le_one_iff)
+
+lemmas le_signed_numeral_special [numeral] =
+ minus_of_num_le_of_num_iff
+ minus_of_num_le_one_iff
+ minus_one_le_of_num_iff
+ minus_one_le_one_iff
+ of_num_le_minus_of_num_iff
+ one_le_minus_of_num_iff
+ of_num_le_minus_one_iff
+ one_le_minus_one_iff
+
+lemmas less_signed_numeral_special [numeral] =
+ minus_of_num_less_of_num_iff
+ minus_of_num_less_one_iff
+ minus_one_less_of_num_iff
+ minus_one_less_one_iff
+ of_num_less_minus_of_num_iff
+ one_less_minus_of_num_iff
+ of_num_less_minus_one_iff
+ one_less_minus_one_iff
+
end
subsubsection {*
--- a/src/HOLCF/FOCUS/Fstream.thy Tue Mar 31 11:04:05 2009 +0200
+++ b/src/HOLCF/FOCUS/Fstream.thy Tue Mar 31 11:04:34 2009 +0200
@@ -87,9 +87,6 @@
apply (cut_tac fscons_not_empty)
apply (fast dest: eq_UU_iff [THEN iffD2])
apply (simp add: fscons_def2)
-apply (drule stream_flat_prefix)
-apply (rule Def_not_UU)
-apply (fast)
done
lemma fstream_prefix' [simp]:
--- a/src/HOLCF/FOCUS/Fstreams.thy Tue Mar 31 11:04:05 2009 +0200
+++ b/src/HOLCF/FOCUS/Fstreams.thy Tue Mar 31 11:04:34 2009 +0200
@@ -173,13 +173,12 @@
lemma fstreams_prefix: "<a> ooo s << t ==> EX tt. t = <a> ooo tt & s << tt"
apply (simp add: fsingleton_def2)
apply (insert stream_prefix [of "Def a" s t], auto)
-by (auto simp add: stream.inverts)
+done
lemma fstreams_prefix': "x << <a> ooo z = (x = <> | (EX y. x = <a> ooo y & y << z))"
apply (auto, case_tac "x=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
apply (simp add: fsingleton_def2, auto)
-apply (auto simp add: stream.inverts)
apply (drule ax_flat, simp)
by (erule sconc_mono)
@@ -197,8 +196,7 @@
by auto
lemma fstreams_mono: "<a> ooo b << <a> ooo c ==> b << c"
-apply (simp add: fsingleton_def2)
-by (auto simp add: stream.inverts)
+by (simp add: fsingleton_def2)
lemma fsmap_UU[simp]: "fsmap f$UU = UU"
by (simp add: fsmap_def)
@@ -220,7 +218,6 @@
apply (drule stream_exhaust_eq [THEN iffD1], auto)
apply (case_tac "y=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
-apply (auto simp add: stream.inverts)
apply (simp add: flat_less_iff)
apply (case_tac "s=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
@@ -344,7 +341,3 @@
by (erule ch2ch_monofun, simp)
end
-
-
-
-
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy Tue Mar 31 11:04:05 2009 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Tue Mar 31 11:04:34 2009 +0200
@@ -322,7 +322,6 @@
lemma Cons_inject_less_eq: "(a>>s<<b>>t) = (a = b & s<<t)"
apply (simp add: Consq_def2)
-apply (simp add: seq.inverts)
done
lemma seq_take_Cons: "seq_take (Suc n)$(a>>x) = a>> (seq_take n$x)"
@@ -661,7 +660,7 @@
(Forall (%x. ~P x) ys & Finite ys)"
apply (rule_tac x="ys" in Seq_induct)
(* adm *)
-apply (simp add: seq.compacts Forall_def sforall_def)
+apply (simp add: Forall_def sforall_def)
(* base cases *)
apply simp
apply simp
--- a/src/HOLCF/Tools/domain/domain_theorems.ML Tue Mar 31 11:04:05 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML Tue Mar 31 11:04:34 2009 +0200
@@ -607,23 +607,23 @@
in
thy
|> Sign.add_path (Long_Name.base_name dname)
- |> (snd o (PureThy.add_thmss (map (Thm.no_attributes o apfst Binding.name) [
- ("iso_rews" , iso_rews ),
- ("exhaust" , [exhaust] ),
- ("casedist" , [casedist]),
- ("when_rews", when_rews ),
- ("compacts", con_compacts),
- ("con_rews", con_rews),
- ("sel_rews", sel_rews),
- ("dis_rews", dis_rews),
- ("pat_rews", pat_rews),
- ("dist_les", dist_les),
- ("dist_eqs", dist_eqs),
- ("inverts" , inverts ),
- ("injects" , injects ),
- ("copy_rews", copy_rews)])))
- |> (snd o PureThy.add_thmss
- [((Binding.name "match_rews", mat_rews), [Simplifier.simp_add])])
+ |> (snd o PureThy.add_thmss [
+ ((Binding.name "iso_rews" , iso_rews ), [Simplifier.simp_add]),
+ ((Binding.name "exhaust" , [exhaust] ), []),
+ ((Binding.name "casedist" , [casedist]), [Induct.cases_type (Long_Name.base_name dname)]),
+ ((Binding.name "when_rews", when_rews ), [Simplifier.simp_add]),
+ ((Binding.name "compacts", con_compacts), [Simplifier.simp_add]),
+ ((Binding.name "con_rews", con_rews), [Simplifier.simp_add]),
+ ((Binding.name "sel_rews", sel_rews), [Simplifier.simp_add]),
+ ((Binding.name "dis_rews", dis_rews), [Simplifier.simp_add]),
+ ((Binding.name "pat_rews", pat_rews), [Simplifier.simp_add]),
+ ((Binding.name "dist_les", dist_les), [Simplifier.simp_add]),
+ ((Binding.name "dist_eqs", dist_eqs), [Simplifier.simp_add]),
+ ((Binding.name "inverts" , inverts ), [Simplifier.simp_add]),
+ ((Binding.name "injects" , injects ), [Simplifier.simp_add]),
+ ((Binding.name "copy_rews", copy_rews), [Simplifier.simp_add]),
+ ((Binding.name "match_rews", mat_rews), [Simplifier.simp_add])
+ ])
|> Sign.parent_path
|> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
pat_rews @ dist_les @ dist_eqs @ copy_rews)
--- a/src/HOLCF/ex/Stream.thy Tue Mar 31 11:04:05 2009 +0200
+++ b/src/HOLCF/ex/Stream.thy Tue Mar 31 11:04:34 2009 +0200
@@ -81,15 +81,13 @@
lemma stream_prefix:
"[| a && s << t; a ~= UU |] ==> EX b tt. t = b && tt & b ~= UU & s << tt"
-apply (insert stream.exhaust [of t], auto)
-by (auto simp add: stream.inverts)
+by (insert stream.exhaust [of t], auto)
lemma stream_prefix':
"b ~= UU ==> x << b && z =
(x = UU | (EX a y. x = a && y & a ~= UU & a << b & y << z))"
apply (case_tac "x=UU",auto)
-apply (drule stream_exhaust_eq [THEN iffD1],auto)
-by (auto simp add: stream.inverts)
+by (drule stream_exhaust_eq [THEN iffD1],auto)
(*
@@ -100,7 +98,6 @@
lemma stream_flat_prefix:
"[| x && xs << y && ys; (x::'a::flat) ~= UU|] ==> x = y & xs << ys"
apply (case_tac "y=UU",auto)
-apply (auto simp add: stream.inverts)
by (drule ax_flat,simp)
@@ -280,17 +277,17 @@
section "coinduction"
lemma stream_coind_lemma2: "!s1 s2. R s1 s2 --> ft$s1 = ft$s2 & R (rt$s1) (rt$s2) ==> stream_bisim R"
-apply (simp add: stream.bisim_def,clarsimp)
-apply (case_tac "x=UU",clarsimp)
-apply (erule_tac x="UU" in allE,simp)
-apply (case_tac "x'=UU",simp)
-apply (drule stream_exhaust_eq [THEN iffD1],auto)+
-apply (case_tac "x'=UU",auto)
-apply (erule_tac x="a && y" in allE)
-apply (erule_tac x="UU" in allE)+
-apply (auto,drule stream_exhaust_eq [THEN iffD1],clarsimp)
-apply (erule_tac x="a && y" in allE)
-apply (erule_tac x="aa && ya" in allE)
+ apply (simp add: stream.bisim_def,clarsimp)
+ apply (case_tac "x=UU",clarsimp)
+ apply (erule_tac x="UU" in allE,simp)
+ apply (case_tac "x'=UU",simp)
+ apply (drule stream_exhaust_eq [THEN iffD1],auto)+
+ apply (case_tac "x'=UU",auto)
+ apply (erule_tac x="a && y" in allE)
+ apply (erule_tac x="UU" in allE)+
+ apply (auto,drule stream_exhaust_eq [THEN iffD1],clarsimp)
+ apply (erule_tac x="a && y" in allE)
+ apply (erule_tac x="aa && ya" in allE) back
by auto
@@ -327,7 +324,6 @@
apply (erule stream_finite_ind [of s], auto)
apply (case_tac "t=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1],auto)
-apply (auto simp add: stream.inverts)
apply (erule_tac x="y" in allE, simp)
by (rule stream_finite_lemma1, simp)
@@ -374,8 +370,6 @@
lemma slen_scons_eq: "(Fin (Suc n) < #x) = (? a y. x = a && y & a ~= \<bottom> & Fin n < #y)"
apply (auto, case_tac "x=UU",auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
-apply (rule_tac x="a" in exI)
-apply (rule_tac x="y" in exI, simp)
apply (case_tac "#y") apply simp_all
apply (case_tac "#y") apply simp_all
done
@@ -387,15 +381,11 @@
by (simp add: slen_def)
lemma slen_scons_eq_rev: "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a && y | a = \<bottom> | #y < Fin (Suc n))"
-apply (rule stream.casedist [of x], auto)
-apply ((*drule sym,*) drule scons_eq_UU [THEN iffD1],auto)
-apply (simp add: zero_inat_def)
-apply (subgoal_tac "s=y & aa=a", simp)
-apply (simp_all add: not_less iSuc_Fin)
-apply (case_tac "#y") apply (simp_all add: iSuc_Fin)
-apply (case_tac "aa=UU", auto)
-apply (erule_tac x="a" in allE, simp)
-apply (case_tac "#s") apply (simp_all add: iSuc_Fin)
+ apply (rule stream.casedist [of x], auto)
+ apply ((*drule sym,*) drule scons_eq_UU [THEN iffD1],auto)
+ apply (simp add: zero_inat_def)
+ apply (case_tac "#s") apply (simp_all add: iSuc_Fin)
+ apply (case_tac "#s") apply (simp_all add: iSuc_Fin)
done
lemma slen_take_lemma4 [rule_format]:
@@ -463,8 +453,7 @@
apply (erule stream_finite_ind [of s], auto)
apply (case_tac "t=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
-apply (erule_tac x="y" in allE, auto)
-by (auto simp add: stream.inverts)
+done
lemma slen_mono: "s << t ==> #s <= #t"
apply (case_tac "stream_finite t")
@@ -493,7 +482,6 @@
apply (case_tac "y=UU", clarsimp)
apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)+
apply (erule_tac x="ya" in allE, simp)
-apply (auto simp add: stream.inverts)
by (drule ax_flat, simp)
lemma slen_strict_mono_lemma:
@@ -501,7 +489,6 @@
apply (erule stream_finite_ind, auto)
apply (case_tac "sa=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
-apply (simp add: stream.inverts, clarsimp)
by (drule ax_flat, simp)
lemma slen_strict_mono: "[|stream_finite t; s ~= t; s << (t::'a::flat stream) |] ==> #s < #t"
@@ -653,7 +640,7 @@
apply (simp add: i_th_def i_rt_Suc_back)
apply (rule stream.casedist [of "i_rt n s1"],simp)
apply (rule stream.casedist [of "i_rt n s2"],auto)
-by (intro monofun_cfun, auto)
+done
lemma i_th_stream_take_Suc [rule_format]:
"ALL s. i_th n (stream_take (Suc n)$s) = i_th n s"
--- a/src/Pure/General/binding.ML Tue Mar 31 11:04:05 2009 +0200
+++ b/src/Pure/General/binding.ML Tue Mar 31 11:04:34 2009 +0200
@@ -84,8 +84,9 @@
let val (qualifier, name) = split_last (Long_Name.explode s)
in make_binding ([], map (rpair false) qualifier, name, Position.none) end;
-fun qualified_name_of (Binding {qualifier, name, ...}) =
- Long_Name.implode (map #1 qualifier @ [name]);
+fun qualified_name_of (b as Binding {qualifier, name, ...}) =
+ if is_empty b then ""
+ else Long_Name.implode (map #1 qualifier @ [name]);
(* system prefix *)
--- a/src/Pure/Isar/expression.ML Tue Mar 31 11:04:05 2009 +0200
+++ b/src/Pure/Isar/expression.ML Tue Mar 31 11:04:34 2009 +0200
@@ -335,7 +335,7 @@
local
fun prep_full_context_statement parse_typ parse_prop prep_vars_elem prep_inst prep_vars_inst prep_expr
- strict do_close raw_import init_body raw_elems raw_concl ctxt1 =
+ {strict, do_close, fixed_frees} raw_import init_body raw_elems raw_concl ctxt1 =
let
val thy = ProofContext.theory_of ctxt1;
@@ -370,6 +370,17 @@
val fors = prep_vars_inst fixed ctxt1 |> fst;
val ctxt2 = ctxt1 |> ProofContext.add_fixes fors |> snd;
val (_, insts', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], ctxt2);
+
+ val add_free = fold_aterms
+ (fn Free (x, T) => not (Variable.is_fixed ctxt3 x) ? insert (op =) (x, T) | _ => I);
+ val _ =
+ if fixed_frees then ()
+ else
+ (case fold (fold add_free o snd o snd) insts' [] of
+ [] => ()
+ | frees => error ("Illegal free variables in expression: " ^
+ commas_quote (map (Syntax.string_of_term ctxt3 o Free) (rev frees))));
+
val ctxt4 = init_body ctxt3;
val (elems, ctxt5) = fold (prep_elem insts') raw_elems ([], ctxt4);
val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5);
@@ -410,7 +421,8 @@
fun prep_statement prep activate raw_elems raw_concl context =
let
val ((_, _, elems, concl), _) =
- prep true false ([], []) I raw_elems raw_concl context;
+ prep {strict = true, do_close = false, fixed_frees = true}
+ ([], []) I raw_elems raw_concl context;
val (_, context') = context |>
ProofContext.set_stmt true |>
fold_map activate elems;
@@ -434,7 +446,8 @@
fun prep_declaration prep activate raw_import init_body raw_elems context =
let
val ((fixed, deps, elems, _), (parms, ctxt')) =
- prep false true raw_import init_body raw_elems [] context ;
+ prep {strict = false, do_close = true, fixed_frees = false}
+ raw_import init_body raw_elems [] context;
(* Declare parameters and imported facts *)
val context' = context |>
fix_params fixed |>
@@ -469,7 +482,7 @@
val thy = ProofContext.theory_of context;
val ((fixed, deps, _, _), _) =
- prep true true expression I [] [] context;
+ prep {strict = true, do_close = true, fixed_frees = true} expression I [] [] context;
(* proof obligations *)
val propss = map (props_of thy) deps;
--- a/src/Pure/Isar/isar_cmd.ML Tue Mar 31 11:04:05 2009 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Tue Mar 31 11:04:34 2009 +0200
@@ -1,7 +1,7 @@
(* Title: Pure/Isar/isar_cmd.ML
Author: Markus Wenzel, TU Muenchen
-Derived Isar commands.
+Miscellaneous Isar commands.
*)
signature ISAR_CMD =
@@ -298,7 +298,7 @@
(* current working directory *)
-fun cd path = Toplevel.imperative (fn () => (File.cd path));
+fun cd path = Toplevel.imperative (fn () => File.cd path);
val pwd = Toplevel.imperative (fn () => writeln (Path.implode (File.pwd ())));
@@ -344,10 +344,9 @@
val print_theorems_theory = Toplevel.keep (fn state =>
Toplevel.theory_of state |>
- (case Toplevel.previous_node_of state of
- SOME prev_node =>
- ProofDisplay.print_theorems_diff (ProofContext.theory_of (Toplevel.context_node prev_node))
- | _ => ProofDisplay.print_theorems));
+ (case Toplevel.previous_context_of state of
+ SOME prev => ProofDisplay.print_theorems_diff (ProofContext.theory_of prev)
+ | NONE => ProofDisplay.print_theorems));
val print_theorems = Toplevel.unknown_context o print_theorems_theory o print_theorems_proof;
--- a/src/Pure/Isar/toplevel.ML Tue Mar 31 11:04:05 2009 +0200
+++ b/src/Pure/Isar/toplevel.ML Tue Mar 31 11:04:34 2009 +0200
@@ -8,21 +8,14 @@
sig
exception UNDEF
type generic_theory
- type node
- val theory_node: node -> generic_theory option
- val proof_node: node -> ProofNode.T option
- val cases_node: (generic_theory -> 'a) -> (Proof.state -> 'a) -> node -> 'a
- val context_node: node -> Proof.context
type state
val toplevel: state
val is_toplevel: state -> bool
val is_theory: state -> bool
val is_proof: state -> bool
val level: state -> int
- val previous_node_of: state -> node option
- val node_of: state -> node
- val node_case: (generic_theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a
val presentation_context_of: state -> Proof.context
+ val previous_context_of: state -> Proof.context option
val context_of: state -> Proof.context
val generic_theory_of: state -> generic_theory
val theory_of: state -> theory
@@ -170,8 +163,6 @@
(* current node *)
-fun previous_node_of (State (_, prev)) = Option.map #1 prev;
-
fun node_of (State (NONE, _)) = raise UNDEF
| node_of (State (SOME (node, _), _)) = node;
@@ -186,6 +177,9 @@
| SOME node => context_node node
| NONE => raise UNDEF);
+fun previous_context_of (State (_, NONE)) = NONE
+ | previous_context_of (State (_, SOME (prev, _))) = SOME (context_node prev);
+
val context_of = node_case Context.proof_of Proof.context_of;
val generic_theory_of = node_case I (Context.Proof o Proof.context_of);
val theory_of = node_case Context.theory_of Proof.theory_of;
--- a/src/Pure/Tools/find_theorems.ML Tue Mar 31 11:04:05 2009 +0200
+++ b/src/Pure/Tools/find_theorems.ML Tue Mar 31 11:04:34 2009 +0200
@@ -11,8 +11,8 @@
Pattern of 'term
val tac_limit: int ref
val limit: int ref
- val find_theorems: Proof.context -> thm option -> bool ->
- (bool * string criterion) list -> (Facts.ref * thm) list
+ val find_theorems: Proof.context -> thm option -> int option -> bool ->
+ (bool * string criterion) list -> int option * (Facts.ref * thm) list
val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T
val print_theorems: Proof.context -> thm option -> int option -> bool ->
(bool * string criterion) list -> unit
@@ -254,12 +254,13 @@
in app (opt_add r r', consts', fs) end;
in app end;
+
in
fun filter_criterion ctxt opt_goal (b, c) =
(if b then I else (apfst opt_not)) o filter_crit ctxt opt_goal c;
-fun all_filters filters thms =
+fun sorted_filter filters thms =
let
fun eval_filters thm = app_filters thm (SOME (0, 0), NONE, filters);
@@ -270,6 +271,15 @@
prod_ord int_ord int_ord ((p1, s1), (p0, s0));
in map_filter eval_filters thms |> sort thm_ord |> map #2 end;
+fun lazy_filter filters = let
+ fun lazy_match thms = Seq.make (fn () => first_match thms)
+
+ and first_match [] = NONE
+ | first_match (thm::thms) =
+ case app_filters thm (SOME (0, 0), NONE, filters) of
+ NONE => first_match thms
+ | SOME (_, t) => SOME (t, lazy_match thms);
+ in lazy_match end;
end;
@@ -334,7 +344,7 @@
val limit = ref 40;
-fun find_theorems ctxt opt_goal rem_dups raw_criteria =
+fun find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
let
val assms = ProofContext.get_fact ctxt (Facts.named "local.assms")
handle ERROR _ => [];
@@ -344,13 +354,25 @@
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
val filters = map (filter_criterion ctxt opt_goal') criteria;
- val raw_matches = all_filters filters (all_facts_of ctxt);
+ fun find_all facts =
+ let
+ val raw_matches = sorted_filter filters facts;
+
+ val matches =
+ if rem_dups
+ then rem_thm_dups (nicer_shortest ctxt) raw_matches
+ else raw_matches;
- val matches =
- if rem_dups
- then rem_thm_dups (nicer_shortest ctxt) raw_matches
- else raw_matches;
- in matches end;
+ val len = length matches;
+ val lim = the_default (! limit) opt_limit;
+ in (SOME len, Library.drop (len - lim, matches)) end;
+
+ val find =
+ if rem_dups orelse is_none opt_limit
+ then find_all
+ else pair NONE o Seq.list_of o Seq.take (the opt_limit) o lazy_filter filters
+
+ in find (all_facts_of ctxt) end;
fun pretty_thm ctxt (thmref, thm) = Pretty.block
@@ -362,11 +384,16 @@
val start = start_timing ();
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
- val matches = find_theorems ctxt opt_goal rem_dups raw_criteria;
-
- val len = length matches;
- val lim = the_default (! limit) opt_limit;
- val thms = Library.drop (len - lim, matches);
+ val (foundo, thms) = find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria;
+ val returned = length thms;
+
+ val tally_msg =
+ case foundo of
+ NONE => "displaying " ^ string_of_int returned ^ " theorems"
+ | SOME found => "found " ^ string_of_int found ^ " theorems" ^
+ (if returned < found
+ then " (" ^ string_of_int returned ^ " displayed)"
+ else "");
val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs";
in
@@ -374,16 +401,12 @@
:: Pretty.str "" ::
(if null thms then [Pretty.str ("nothing found" ^ end_msg)]
else
- [Pretty.str ("found " ^ string_of_int len ^ " theorems" ^
- (if len <= lim then ""
- else " (" ^ string_of_int lim ^ " displayed)")
- ^ end_msg ^ ":"), Pretty.str ""] @
+ [Pretty.str (tally_msg ^ end_msg ^ ":"), Pretty.str ""] @
map (pretty_thm ctxt) thms)
|> Pretty.chunks |> Pretty.writeln
end;
-
(** command syntax **)
fun find_theorems_cmd ((opt_lim, rem_dups), spec) =
--- a/src/Tools/auto_solve.ML Tue Mar 31 11:04:05 2009 +0200
+++ b/src/Tools/auto_solve.ML Tue Mar 31 11:04:34 2009 +0200
@@ -13,6 +13,7 @@
sig
val auto : bool ref
val auto_time_limit : int ref
+ val limit : int ref
val seek_solution : bool -> Proof.state -> Proof.state
end;
@@ -22,6 +23,7 @@
val auto = ref false;
val auto_time_limit = ref 2500;
+val limit = ref 5;
fun seek_solution int state =
let
@@ -34,9 +36,9 @@
handle TERM _ => t::conj_to_list ts;
val crits = [(true, FindTheorems.Solves)];
- fun find g = (NONE, FindTheorems.find_theorems ctxt g true crits);
- fun find_cterm g = (SOME g, FindTheorems.find_theorems ctxt
- (SOME (Goal.init g)) true crits);
+ fun find g = (NONE, snd (FindTheorems.find_theorems ctxt g (SOME (!limit)) false crits));
+ fun find_cterm g = (SOME g, snd (FindTheorems.find_theorems ctxt
+ (SOME (Goal.init g)) (SOME (!limit)) false crits));
fun prt_result (goal, results) =
let