# HG changeset patch # User haftmann # Date 1238490274 -7200 # Node ID 461da7178275efbbd09a4f6cdc876c1c1142b7e1 # Parent 83642621425affbc5f5064f9dd55e9d34bf6786b# Parent 684720b0b9e69f9c5f9daa1f7c5f97431a17aa38 merged diff -r 83642621425a -r 461da7178275 src/HOL/Int.thy --- 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 *} diff -r 83642621425a -r 461da7178275 src/HOL/Orderings.thy --- 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 **) diff -r 83642621425a -r 461da7178275 src/HOL/Tools/atp_manager.ML --- 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; diff -r 83642621425a -r 461da7178275 src/HOL/Tools/function_package/fundef_common.ML --- 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 diff -r 83642621425a -r 461da7178275 src/HOL/Tools/function_package/fundef_datatype.ML --- 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 diff -r 83642621425a -r 461da7178275 src/HOL/Tools/function_package/fundef_package.ML --- 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 diff -r 83642621425a -r 461da7178275 src/HOL/Tools/int_arith.ML --- 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] diff -r 83642621425a -r 461da7178275 src/HOL/ex/Numeral.thy --- 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 \ 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 \ 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 \ 1" +lemma minus_of_num_le_one_iff: "- of_num n \ 1" by (simp add: less_imp_le minus_of_num_less_one_iff) -lemma minus_one_le_of_num_iff [numeral]: "- 1 \ of_num n" +lemma minus_one_le_of_num_iff: "- 1 \ of_num n" by (simp add: less_imp_le minus_one_less_of_num_iff) -lemma of_num_le_minus_of_num_iff [numeral]: "\ of_num m \ - of_num n" +lemma minus_one_le_one_iff: "- 1 \ 1" + by (simp add: less_imp_le minus_one_less_one_iff) + +lemma of_num_le_minus_of_num_iff: "\ of_num m \ - of_num n" by (simp add: not_le minus_of_num_less_of_num_iff) -lemma one_le_minus_of_num_iff [numeral]: "\ 1 \ - of_num n" +lemma one_le_minus_of_num_iff: "\ 1 \ - of_num n" by (simp add: not_le minus_of_num_less_one_iff) -lemma of_num_le_minus_one_iff [numeral]: "\ of_num n \ - 1" +lemma of_num_le_minus_one_iff: "\ of_num n \ - 1" by (simp add: not_le minus_one_less_of_num_iff) -lemma of_num_less_minus_of_num_iff [numeral]: "\ of_num m < - of_num n" +lemma one_le_minus_one_iff: "\ 1 \ - 1" + by (simp add: not_le minus_one_less_one_iff) + +lemma of_num_less_minus_of_num_iff: "\ 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]: "\ 1 < - of_num n" +lemma one_less_minus_of_num_iff: "\ 1 < - of_num n" by (simp add: not_less minus_of_num_le_one_iff) -lemma of_num_less_minus_one_iff [numeral]: "\ of_num n < - 1" +lemma of_num_less_minus_one_iff: "\ of_num n < - 1" by (simp add: not_less minus_one_le_of_num_iff) +lemma one_less_minus_one_iff: "\ 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 {* diff -r 83642621425a -r 461da7178275 src/HOLCF/FOCUS/Fstream.thy --- 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]: diff -r 83642621425a -r 461da7178275 src/HOLCF/FOCUS/Fstreams.thy --- 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: " ooo s << t ==> EX tt. t = 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 << ooo z = (x = <> | (EX y. x = 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: " ooo b << 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 - - - - diff -r 83642621425a -r 461da7178275 src/HOLCF/IOA/meta_theory/Sequence.thy --- 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<>t) = (a = b & s<>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 diff -r 83642621425a -r 461da7178275 src/HOLCF/Tools/domain/domain_theorems.ML --- 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) diff -r 83642621425a -r 461da7178275 src/HOLCF/ex/Stream.thy --- 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 ~= \ & 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 = \ | #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" diff -r 83642621425a -r 461da7178275 src/Pure/General/binding.ML --- 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 *) diff -r 83642621425a -r 461da7178275 src/Pure/Isar/expression.ML --- 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; diff -r 83642621425a -r 461da7178275 src/Pure/Isar/isar_cmd.ML --- 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; diff -r 83642621425a -r 461da7178275 src/Pure/Isar/toplevel.ML --- 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; diff -r 83642621425a -r 461da7178275 src/Pure/Tools/find_theorems.ML --- 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) = diff -r 83642621425a -r 461da7178275 src/Tools/auto_solve.ML --- 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