# HG changeset patch # User ballarin # Date 1238528396 -7200 # Node ID fe4331fb3806a8d7f79d139c0e61773d5480235a # Parent a53f4872400ed36867fe550e61164b44c8731147# Parent 7d6d1f9a0b41cb6f71792cfee07b73b5d0b0eb82 Merged. diff -r a53f4872400e -r fe4331fb3806 etc/settings --- a/etc/settings Tue Mar 31 21:25:08 2009 +0200 +++ b/etc/settings Tue Mar 31 21:39:56 2009 +0200 @@ -94,7 +94,7 @@ # Specifically for the HOL image HOL_USEDIR_OPTIONS="" -#HOL_USEDIR_OPTIONS="-p 2" +#HOL_USEDIR_OPTIONS="-p 2 -Q false" #Source file identification (default: full name + date stamp) ISABELLE_FILE_IDENT="" diff -r a53f4872400e -r fe4331fb3806 lib/texinputs/isabellesym.sty --- a/lib/texinputs/isabellesym.sty Tue Mar 31 21:25:08 2009 +0200 +++ b/lib/texinputs/isabellesym.sty Tue Mar 31 21:39:56 2009 +0200 @@ -249,7 +249,7 @@ \newcommand{\isasymsqunion}{\isamath{\sqcup}} \newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}} \newcommand{\isasymsqinter}{\isamath{\sqcap}} -\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires amsmath +\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires stmaryrd \newcommand{\isasymsetminus}{\isamath{\setminus}} \newcommand{\isasympropto}{\isamath{\propto}} \newcommand{\isasymuplus}{\isamath{\uplus}} diff -r a53f4872400e -r fe4331fb3806 src/HOL/Int.thy --- a/src/HOL/Int.thy Tue Mar 31 21:25:08 2009 +0200 +++ b/src/HOL/Int.thy Tue Mar 31 21:39:56 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 a53f4872400e -r fe4331fb3806 src/HOL/Isar_examples/KnasterTarski.thy --- a/src/HOL/Isar_examples/KnasterTarski.thy Tue Mar 31 21:25:08 2009 +0200 +++ b/src/HOL/Isar_examples/KnasterTarski.thy Tue Mar 31 21:39:56 2009 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Isar_examples/KnasterTarski.thy - ID: $Id$ Author: Markus Wenzel, TU Muenchen Typical textbook proof example. @@ -7,100 +6,104 @@ header {* Textbook-style reasoning: the Knaster-Tarski Theorem *} -theory KnasterTarski imports Main begin +theory KnasterTarski +imports Main Lattice_Syntax +begin subsection {* Prose version *} text {* - According to the textbook \cite[pages 93--94]{davey-priestley}, the - Knaster-Tarski fixpoint theorem is as follows.\footnote{We have - dualized the argument, and tuned the notation a little bit.} + According to the textbook \cite[pages 93--94]{davey-priestley}, the + Knaster-Tarski fixpoint theorem is as follows.\footnote{We have + dualized the argument, and tuned the notation a little bit.} - \medskip \textbf{The Knaster-Tarski Fixpoint Theorem.} Let $L$ be a - complete lattice and $f \colon L \to L$ an order-preserving map. - Then $\bigwedge \{ x \in L \mid f(x) \le x \}$ is a fixpoint of $f$. + \textbf{The Knaster-Tarski Fixpoint Theorem.} Let @{text L} be a + complete lattice and @{text "f: L \ L"} an order-preserving map. + Then @{text "\{x \ L | f(x) \ x}"} is a fixpoint of @{text f}. - \textbf{Proof.} Let $H = \{x \in L \mid f(x) \le x\}$ and $a = - \bigwedge H$. For all $x \in H$ we have $a \le x$, so $f(a) \le f(x) - \le x$. Thus $f(a)$ is a lower bound of $H$, whence $f(a) \le a$. - We now use this inequality to prove the reverse one (!) and thereby - complete the proof that $a$ is a fixpoint. Since $f$ is - order-preserving, $f(f(a)) \le f(a)$. This says $f(a) \in H$, so $a - \le f(a)$. + \textbf{Proof.} Let @{text "H = {x \ L | f(x) \ x}"} and @{text "a = + \H"}. For all @{text "x \ H"} we have @{text "a \ x"}, so @{text + "f(a) \ f(x) \ x"}. Thus @{text "f(a)"} is a lower bound of @{text + H}, whence @{text "f(a) \ a"}. We now use this inequality to prove + the reverse one (!) and thereby complete the proof that @{text a} is + a fixpoint. Since @{text f} is order-preserving, @{text "f(f(a)) \ + f(a)"}. This says @{text "f(a) \ H"}, so @{text "a \ f(a)"}. *} subsection {* Formal versions *} text {* - The Isar proof below closely follows the original presentation. - Virtually all of the prose narration has been rephrased in terms of - formal Isar language elements. Just as many textbook-style proofs, - there is a strong bias towards forward proof, and several bends - in the course of reasoning. + The Isar proof below closely follows the original presentation. + Virtually all of the prose narration has been rephrased in terms of + formal Isar language elements. Just as many textbook-style proofs, + there is a strong bias towards forward proof, and several bends in + the course of reasoning. *} -theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a" +theorem Knaster_Tarski: + fixes f :: "'a::complete_lattice \ 'a" + assumes "mono f" + shows "\a. f a = a" proof - let ?H = "{u. f u <= u}" - let ?a = "Inter ?H" - - assume mono: "mono f" + let ?H = "{u. f u \ u}" + let ?a = "\?H" show "f ?a = ?a" proof - { fix x - assume H: "x : ?H" - hence "?a <= x" by (rule Inter_lower) - with mono have "f ?a <= f x" .. - also from H have "... <= x" .. - finally have "f ?a <= x" . + assume "x \ ?H" + then have "?a \ x" by (rule Inf_lower) + with `mono f` have "f ?a \ f x" .. + also from `x \ ?H` have "\ \ x" .. + finally have "f ?a \ x" . } - hence ge: "f ?a <= ?a" by (rule Inter_greatest) + then have "f ?a \ ?a" by (rule Inf_greatest) { - also presume "... <= f ?a" + also presume "\ \ f ?a" finally (order_antisym) show ?thesis . } - from mono ge have "f (f ?a) <= f ?a" .. - hence "f ?a : ?H" by simp - thus "?a <= f ?a" by (rule Inter_lower) + from `mono f` and `f ?a \ ?a` have "f (f ?a) \ f ?a" .. + then have "f ?a \ ?H" .. + then show "?a \ f ?a" by (rule Inf_lower) qed qed text {* - Above we have used several advanced Isar language elements, such as - explicit block structure and weak assumptions. Thus we have mimicked - the particular way of reasoning of the original text. + Above we have used several advanced Isar language elements, such as + explicit block structure and weak assumptions. Thus we have + mimicked the particular way of reasoning of the original text. - In the subsequent version the order of reasoning is changed to - achieve structured top-down decomposition of the problem at the outer - level, while only the inner steps of reasoning are done in a forward - manner. We are certainly more at ease here, requiring only the most - basic features of the Isar language. + In the subsequent version the order of reasoning is changed to + achieve structured top-down decomposition of the problem at the + outer level, while only the inner steps of reasoning are done in a + forward manner. We are certainly more at ease here, requiring only + the most basic features of the Isar language. *} -theorem KnasterTarski': "mono f ==> EX a::'a set. f a = a" +theorem Knaster_Tarski': + fixes f :: "'a::complete_lattice \ 'a" + assumes "mono f" + shows "\a. f a = a" proof - let ?H = "{u. f u <= u}" - let ?a = "Inter ?H" - - assume mono: "mono f" + let ?H = "{u. f u \ u}" + let ?a = "\?H" show "f ?a = ?a" proof (rule order_antisym) - show ge: "f ?a <= ?a" - proof (rule Inter_greatest) + show "f ?a \ ?a" + proof (rule Inf_greatest) fix x - assume H: "x : ?H" - hence "?a <= x" by (rule Inter_lower) - with mono have "f ?a <= f x" .. - also from H have "... <= x" .. - finally show "f ?a <= x" . + assume "x \ ?H" + then have "?a \ x" by (rule Inf_lower) + with `mono f` have "f ?a \ f x" .. + also from `x \ ?H` have "\ \ x" .. + finally show "f ?a \ x" . qed - show "?a <= f ?a" - proof (rule Inter_lower) - from mono ge have "f (f ?a) <= f ?a" .. - thus "f ?a : ?H" by simp + show "?a \ f ?a" + proof (rule Inf_lower) + from `mono f` and `f ?a \ ?a` have "f (f ?a) \ f ?a" .. + then show "f ?a \ ?H" .. qed qed qed diff -r a53f4872400e -r fe4331fb3806 src/HOL/Isar_examples/document/style.tex --- a/src/HOL/Isar_examples/document/style.tex Tue Mar 31 21:25:08 2009 +0200 +++ b/src/HOL/Isar_examples/document/style.tex Tue Mar 31 21:39:56 2009 +0200 @@ -1,8 +1,6 @@ - -%% $Id$ - \documentclass[11pt,a4paper]{article} -\usepackage{ifthen,proof,isabelle,isabellesym} +\usepackage[only,bigsqcap]{stmaryrd} +\usepackage{ifthen,proof,amssymb,isabelle,isabellesym} \isabellestyle{it} \usepackage{pdfsetup}\urlstyle{rm} diff -r a53f4872400e -r fe4331fb3806 src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Tue Mar 31 21:25:08 2009 +0200 +++ b/src/HOL/Orderings.thy Tue Mar 31 21:39:56 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 a53f4872400e -r fe4331fb3806 src/HOL/Set.thy --- a/src/HOL/Set.thy Tue Mar 31 21:25:08 2009 +0200 +++ b/src/HOL/Set.thy Tue Mar 31 21:39:56 2009 +0200 @@ -2384,7 +2384,7 @@ unfolding Inf_bool_def by auto lemma not_Sup_empty_bool [simp]: - "\ Sup {}" + "\ \{}" unfolding Sup_bool_def by auto diff -r a53f4872400e -r fe4331fb3806 src/HOL/Tools/atp_manager.ML --- a/src/HOL/Tools/atp_manager.ML Tue Mar 31 21:25:08 2009 +0200 +++ b/src/HOL/Tools/atp_manager.ML Tue Mar 31 21:39:56 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 a53f4872400e -r fe4331fb3806 src/HOL/Tools/function_package/fundef_common.ML --- a/src/HOL/Tools/function_package/fundef_common.ML Tue Mar 31 21:25:08 2009 +0200 +++ b/src/HOL/Tools/function_package/fundef_common.ML Tue Mar 31 21:39:56 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 a53f4872400e -r fe4331fb3806 src/HOL/Tools/function_package/fundef_datatype.ML --- a/src/HOL/Tools/function_package/fundef_datatype.ML Tue Mar 31 21:25:08 2009 +0200 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML Tue Mar 31 21:39:56 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 a53f4872400e -r fe4331fb3806 src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Tue Mar 31 21:25:08 2009 +0200 +++ b/src/HOL/Tools/function_package/fundef_package.ML Tue Mar 31 21:39:56 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 a53f4872400e -r fe4331fb3806 src/HOL/Tools/int_arith.ML --- a/src/HOL/Tools/int_arith.ML Tue Mar 31 21:25:08 2009 +0200 +++ b/src/HOL/Tools/int_arith.ML Tue Mar 31 21:39:56 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 a53f4872400e -r fe4331fb3806 src/HOL/ex/Numeral.thy --- a/src/HOL/ex/Numeral.thy Tue Mar 31 21:25:08 2009 +0200 +++ b/src/HOL/ex/Numeral.thy Tue Mar 31 21:39:56 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 a53f4872400e -r fe4331fb3806 src/HOL/ex/Predicate_Compile.thy --- a/src/HOL/ex/Predicate_Compile.thy Tue Mar 31 21:25:08 2009 +0200 +++ b/src/HOL/ex/Predicate_Compile.thy Tue Mar 31 21:39:56 2009 +0200 @@ -1,5 +1,5 @@ theory Predicate_Compile -imports Complex_Main Lattice_Syntax +imports Complex_Main Code_Index Lattice_Syntax uses "predicate_compile.ML" begin @@ -12,10 +12,26 @@ | "next yield (Predicate.Join P xq) = (case yield P of None \ next yield xq | Some (x, Q) \ Some (x, Predicate.Seq (\_. Predicate.Join Q xq)))" -primrec pull :: "('a Predicate.pred \ ('a \ 'a Predicate.pred) option) - \ nat \ 'a Predicate.pred \ 'a list \ 'a Predicate.pred" where - "pull yield 0 P = ([], \)" - | "pull yield (Suc n) P = (case yield P - of None \ ([], \) | Some (x, Q) \ let (xs, R) = pull yield n Q in (x # xs, R))" +ML {* +let + fun yield (@{code Predicate.Seq} f) = @{code next} yield (f ()) +in + yield @{code "\ :: 'a Predicate.pred"} (*replace bottom with sequence to evaluate*) +end +*} + +fun anamorph :: "('b \ ('a \ 'b) option) \ index \ 'b \ 'a list \ 'b" where + "anamorph f k x = (if k = 0 then ([], x) + else case f x of None \ ([], x) | Some (v, y) \ let (vs, z) = anamorph f (k - 1) y in (v # vs, z))" + +ML {* +let + fun yield (@{code Predicate.Seq} f) = @{code next} yield (f ()) + fun yieldn k = @{code anamorph} yield k +in + yieldn 0 (*replace with number of elements to retrieve*) + @{code "\ :: 'a Predicate.pred"} (*replace bottom with sequence to evaluate*) +end +*} end \ No newline at end of file diff -r a53f4872400e -r fe4331fb3806 src/HOLCF/FOCUS/Fstream.thy --- a/src/HOLCF/FOCUS/Fstream.thy Tue Mar 31 21:25:08 2009 +0200 +++ b/src/HOLCF/FOCUS/Fstream.thy Tue Mar 31 21:39:56 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 a53f4872400e -r fe4331fb3806 src/HOLCF/FOCUS/Fstreams.thy --- a/src/HOLCF/FOCUS/Fstreams.thy Tue Mar 31 21:25:08 2009 +0200 +++ b/src/HOLCF/FOCUS/Fstreams.thy Tue Mar 31 21:39:56 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 a53f4872400e -r fe4331fb3806 src/HOLCF/IOA/meta_theory/Sequence.thy --- a/src/HOLCF/IOA/meta_theory/Sequence.thy Tue Mar 31 21:25:08 2009 +0200 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Tue Mar 31 21:39:56 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 a53f4872400e -r fe4331fb3806 src/HOLCF/Tools/domain/domain_theorems.ML --- a/src/HOLCF/Tools/domain/domain_theorems.ML Tue Mar 31 21:25:08 2009 +0200 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML Tue Mar 31 21:39:56 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 a53f4872400e -r fe4331fb3806 src/HOLCF/ex/Stream.thy --- a/src/HOLCF/ex/Stream.thy Tue Mar 31 21:25:08 2009 +0200 +++ b/src/HOLCF/ex/Stream.thy Tue Mar 31 21:39:56 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 a53f4872400e -r fe4331fb3806 src/Pure/General/binding.ML --- a/src/Pure/General/binding.ML Tue Mar 31 21:25:08 2009 +0200 +++ b/src/Pure/General/binding.ML Tue Mar 31 21:39:56 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 a53f4872400e -r fe4331fb3806 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Tue Mar 31 21:25:08 2009 +0200 +++ b/src/Pure/Isar/element.ML Tue Mar 31 21:39:56 2009 +0200 @@ -60,8 +60,9 @@ (Attrib.binding * (thm list * Attrib.src list) list) list val eq_morphism: theory -> thm list -> morphism val transfer_morphism: theory -> morphism - val activate: (typ, term, Facts.ref) ctxt list -> Proof.context -> context_i list * Proof.context - val activate_i: context_i list -> Proof.context -> context_i list * Proof.context + val init: context_i -> Context.generic -> Context.generic + val activate_i: context_i -> Proof.context -> context_i * Proof.context + val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context end; structure Element: ELEMENT = @@ -481,64 +482,54 @@ -(** activate in context, return elements and facts **) +(** activate in context **) -local +(* init *) -fun activate_elem (Fixes fixes) ctxt = - ctxt |> ProofContext.add_fixes fixes |> snd - | activate_elem (Constrains _) ctxt = - ctxt - | activate_elem (Assumes asms) ctxt = +fun init (Fixes fixes) = Context.map_proof (ProofContext.add_fixes fixes #> #2) + | init (Constrains _) = I + | init (Assumes asms) = Context.map_proof (fn ctxt => let val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms; - val ts = maps (map #1 o #2) asms'; - val (_, ctxt') = - ctxt |> fold Variable.auto_fixes ts - |> ProofContext.add_assms_i Assumption.presume_export asms'; - in ctxt' end - | activate_elem (Defines defs) ctxt = + val (_, ctxt') = ctxt + |> fold Variable.auto_fixes (maps (map #1 o #2) asms') + |> ProofContext.add_assms_i Assumption.assume_export asms'; + in ctxt' end) + | init (Defines defs) = Context.map_proof (fn ctxt => let val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs; val asms = defs' |> map (fn ((name, atts), (t, ps)) => - let val ((c, _), t') = LocalDefs.cert_def ctxt t + let val ((c, _), t') = LocalDefs.cert_def ctxt t (* FIXME adapt ps? *) in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end); - val (_, ctxt') = - ctxt |> fold (Variable.auto_fixes o #1) asms + val (_, ctxt') = ctxt + |> fold Variable.auto_fixes (map #1 asms) |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms); - in ctxt' end - | activate_elem (Notes (kind, facts)) ctxt = + in ctxt' end) + | init (Notes (kind, facts)) = (fn context => let - val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts; - val (res, ctxt') = ctxt |> ProofContext.note_thmss kind facts'; - in ctxt' end; + val facts' = Attrib.map_facts (Attrib.attribute_i (Context.theory_of context)) facts; + val context' = context |> Context.mapping + (PureThy.note_thmss kind facts' #> #2) + (ProofContext.note_thmss kind facts' #> #2); + in context' end); -fun gen_activate prep_facts raw_elems ctxt = + +(* activate *) + +fun activate_i elem ctxt = let - fun activate elem ctxt = - let val elem' = (map_ctxt_attrib Args.assignable o prep_facts ctxt) elem - in (elem', activate_elem elem' ctxt) end - val (elems, ctxt') = fold_map activate raw_elems ctxt; - in (elems |> map (map_ctxt_attrib Args.closure), ctxt') end; + val elem' = map_ctxt_attrib Args.assignable elem; + val ctxt' = Context.proof_map (init elem') ctxt; + in (map_ctxt_attrib Args.closure elem', ctxt') end; -fun check_name name = - if Long_Name.is_qualified name then error ("Illegal qualified name: " ^ quote name) - else name; - -fun prep_facts prep_name get intern ctxt = - map_ctxt - {binding = Binding.map_name prep_name, +fun activate raw_elem ctxt = + let val elem = raw_elem |> map_ctxt + {binding = tap Name.of_binding, typ = I, term = I, pattern = I, - fact = get ctxt, - attrib = intern (ProofContext.theory_of ctxt)}; - -in - -fun activate x = gen_activate (prep_facts check_name ProofContext.get_fact Attrib.intern_src) x; -fun activate_i x = gen_activate (K I) x; + fact = ProofContext.get_fact ctxt, + attrib = Attrib.intern_src (ProofContext.theory_of ctxt)} + in activate_i elem ctxt end; end; - -end; diff -r a53f4872400e -r fe4331fb3806 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Tue Mar 31 21:25:08 2009 +0200 +++ b/src/Pure/Isar/expression.ML Tue Mar 31 21:39:56 2009 +0200 @@ -70,12 +70,12 @@ fun intern thy instances = map (apfst (Locale.intern thy)) instances; -(** Parameters of expression. +(** Parameters of expression **) - Sanity check of instantiations and extraction of implicit parameters. - The latter only occurs iff strict = false. - Positional instantiations are extended to match full length of parameter list - of instantiated locale. **) +(*Sanity check of instantiations and extraction of implicit parameters. + The latter only occurs iff strict = false. + Positional instantiations are extended to match full length of parameter list + of instantiated locale.*) fun parameters_of thy strict (expr, fixed) = let @@ -88,7 +88,7 @@ (mx1 = mx2 orelse error ("Conflicting syntax for parameter " ^ quote p1 ^ " in expression")); fun params_loc loc = Locale.params_of thy loc |> map (apfst #1); - fun params_inst (expr as (loc, (prfx, Positional insts))) = + fun params_inst (loc, (prfx, Positional insts)) = let val ps = params_loc loc; val d = length ps - length insts; @@ -99,24 +99,22 @@ val ps' = (ps ~~ insts') |> map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE); in (ps', (loc, (prfx, Positional insts'))) end - | params_inst (expr as (loc, (prfx, Named insts))) = + | params_inst (loc, (prfx, Named insts)) = let val _ = reject_dups "Duplicate instantiation of the following parameter(s): " (map fst insts); - - val ps = params_loc loc; - val ps' = fold (fn (p, _) => fn ps => + val ps' = (insts, params_loc loc) |-> fold (fn (p, _) => fn ps => if AList.defined (op =) ps p then AList.delete (op =) p ps - else error (quote p ^ " not a parameter of instantiated expression")) insts ps; + else error (quote p ^ " not a parameter of instantiated expression")); in (ps', (loc, (prfx, Named insts))) end; fun params_expr is = + let + val (is', ps') = fold_map (fn i => fn ps => let - val (is', ps') = fold_map (fn i => fn ps => - let - val (ps', i') = params_inst i; - val ps'' = distinct parm_eq (ps @ ps'); - in (i', ps'') end) is [] - in (ps', is') end; + val (ps', i') = params_inst i; + val ps'' = distinct parm_eq (ps @ ps'); + in (i', ps'') end) is [] + in (ps', is') end; val (implicit, expr') = params_expr expr; @@ -158,7 +156,7 @@ (* Instantiation morphism *) -fun inst_morph (parm_names, parm_types) ((prfx, strict), insts') ctxt = +fun inst_morph (parm_names, parm_types) ((prfx, mandatory), insts') ctxt = let (* parameters *) val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst; @@ -173,13 +171,13 @@ (* instantiation *) val (type_parms'', res') = chop (length type_parms) res; val insts'' = (parm_names ~~ res') |> map_filter - (fn (inst as (x, Free (y, _))) => if x = y then NONE else SOME inst | - inst => SOME inst); + (fn inst as (x, Free (y, _)) => if x = y then NONE else SOME inst + | inst => SOME inst); val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms''); val inst = Symtab.make insts''; in (Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $> - Morphism.binding_morphism (Binding.prefix strict prfx), ctxt') + Morphism.binding_morphism (Binding.prefix mandatory prfx), ctxt') end; @@ -242,7 +240,7 @@ in ((t, Syntax.check_props (ProofContext.set_mode ProofContext.mode_pattern ctxt') pats), (ctxt', ts)) - end + end; val (cs', (context', _)) = fold_map prep cs (context, Syntax.check_terms (ProofContext.set_mode ProofContext.mode_schematic context) (map fst cs)); @@ -260,7 +258,8 @@ (fold_burrow o fold_burrow) check (inst_cs :: elem_css @ [concl_cs]) ctxt; val (elem_css', [concl_cs']) = chop (length elem_css) css'; in - (map restore_inst (insts ~~ inst_cs'), map restore_elem (elems ~~ elem_css'), + (map restore_inst (insts ~~ inst_cs'), + map restore_elem (elems ~~ elem_css'), concl_cs', ctxt') end; @@ -278,6 +277,7 @@ | declare_elem _ (Defines _) ctxt = ctxt | declare_elem _ (Notes _) ctxt = ctxt; + (** Finish locale elements **) fun closeup _ _ false elem = elem @@ -335,13 +335,13 @@ 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; val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import); - fun prep_insts (loc, (prfx, inst)) (i, insts, ctxt) = + fun prep_insts_cumulative (loc, (prfx, inst)) (i, insts, ctxt) = let val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list; val inst' = prep_inst ctxt parm_names inst; @@ -359,7 +359,7 @@ let val ctxt' = declare_elem prep_vars_elem raw_elem ctxt; val elems' = elems @ [parse_elem parse_typ parse_prop ctxt' raw_elem]; - val (_, _, _, ctxt'') = check_autofix insts elems' [] ctxt'; + val (_, _, _, ctxt'' (* FIXME not used *) ) = check_autofix insts elems' [] ctxt'; in (elems', ctxt') end; fun prep_concl raw_concl (insts, elems, ctxt) = @@ -369,11 +369,21 @@ val fors = prep_vars_inst fixed ctxt1 |> fst; val ctxt2 = ctxt1 |> ProofContext.add_fixes fors |> snd; - val (_, insts', ctxt3) = fold prep_insts raw_insts (0, [], ctxt2); + 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); + val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5); (* Retrieve parameter types *) val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Name.of_binding o #1) fixes) @@ -392,9 +402,11 @@ fun cert_full_context_statement x = prep_full_context_statement (K I) (K I) ProofContext.cert_vars make_inst ProofContext.cert_vars (K I) x; + fun cert_read_full_context_statement x = prep_full_context_statement Syntax.parse_typ Syntax.parse_prop ProofContext.read_vars make_inst ProofContext.cert_vars (K I) x; + fun read_full_context_statement x = prep_full_context_statement Syntax.parse_typ Syntax.parse_prop ProofContext.read_vars parse_inst ProofContext.read_vars intern x; @@ -409,10 +421,11 @@ 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 |> - activate elems; + fold_map activate elems; in (concl, context') end; in @@ -433,14 +446,15 @@ 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 |> fold (Context.proof_map o Locale.activate_facts) deps; val (elems', _) = context' |> ProofContext.set_stmt true |> - activate elems; + fold_map activate elems; in ((fixed, deps, elems'), (parms, ctxt')) end; in @@ -468,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; @@ -727,7 +741,8 @@ val extraTs = fold Term.add_tfrees exts' [] \\ fold Term.add_tfreesT (map snd parms) []; val _ = if null extraTs then () - else warning ("Additional type variable(s) in locale specification " ^ quote (Binding.str_of bname)); + else warning ("Additional type variable(s) in locale specification " ^ + quote (Binding.str_of bname)); val a_satisfy = Element.satisfy_morphism a_axioms; val b_satisfy = Element.satisfy_morphism b_axioms; diff -r a53f4872400e -r fe4331fb3806 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Tue Mar 31 21:25:08 2009 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Tue Mar 31 21:39:56 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 a53f4872400e -r fe4331fb3806 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Tue Mar 31 21:25:08 2009 +0200 +++ b/src/Pure/Isar/locale.ML Tue Mar 31 21:39:56 2009 +0200 @@ -245,7 +245,7 @@ val dependencies' = filter_out (fn (name, morph) => member (ident_eq thy) marked (name, instance_of thy name morph)) dependencies; in - (merge (ident_eq thy) (marked, marked'), input |> fold_rev (activate_dep thy) dependencies') + (merge (ident_eq thy) (marked, marked'), input |> fold_rev activate_dep dependencies') end; end; @@ -285,59 +285,28 @@ (if not (null defs) then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs)) else I); + val activate = activate_notes activ_elem transfer thy; in - roundup thy (activate_notes activ_elem transfer) (name, Morphism.identity) (marked, input') + roundup thy activate (name, Morphism.identity) (marked, input') end; (** Public activation functions **) -local - -fun init_elem (Fixes fixes) (Context.Proof ctxt) = - Context.Proof (ProofContext.add_fixes fixes ctxt |> snd) - | init_elem (Assumes assms) (Context.Proof ctxt) = - let - val assms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) assms; - val ctxt' = ctxt - |> fold Variable.auto_fixes (maps (map fst o snd) assms') - |> ProofContext.add_assms_i Assumption.assume_export assms' |> snd; - in Context.Proof ctxt' end - | init_elem (Defines defs) (Context.Proof ctxt) = - let - val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs; - val ctxt' = ctxt - |> fold Variable.auto_fixes (map (fst o snd) defs') - |> ProofContext.add_assms_i LocalDefs.def_export (map (fn (attn, t) => (attn, [t])) defs') - |> snd; - in Context.Proof ctxt' end - | init_elem (Notes (kind, facts)) (Context.Proof ctxt) = - let - val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts - in Context.Proof (ProofContext.note_thmss kind facts' ctxt |> snd) end - | init_elem (Notes (kind, facts)) (Context.Theory thy) = - let - val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts - in Context.Theory (PureThy.note_thmss kind facts' thy |> snd) end - | init_elem _ (Context.Theory _) = raise Fail "Bad context element in global theory"; - -in - -fun activate_declarations dep ctxt = +fun activate_declarations dep = Context.proof_map (fn context => let - val context = Context.Proof ctxt; val thy = Context.theory_of context; - val context' = roundup thy (K activate_decls) dep (get_idents context, context) |-> put_idents; - in Context.the_proof context' end; + val context' = roundup thy activate_decls dep (get_idents context, context) |-> put_idents; + in context' end); fun activate_facts dep context = let val thy = Context.theory_of context; - val activate = activate_notes init_elem (Element.transfer_morphism o Context.theory_of); + val activate = activate_notes Element.init (Element.transfer_morphism o Context.theory_of) thy; in roundup thy activate dep (get_idents context, context) |-> put_idents end; fun init name thy = - activate_all name thy init_elem (Element.transfer_morphism o Context.theory_of) + activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of) ([], Context.Proof (ProofContext.init thy)) |-> put_idents |> Context.proof_of; fun print_locale thy show_facts raw_name = @@ -354,8 +323,6 @@ |> Pretty.writeln end; -end; - (*** Registrations: interpretations in theories ***) @@ -375,8 +342,7 @@ Registrations.get #> map (#1 #> apsnd op $>); fun add_registration (name, (base_morph, export)) thy = - roundup thy (fn _ => fn (name', morph') => - Registrations.map (cons ((name', (morph', export)), stamp ()))) + roundup thy (fn (name', morph') => Registrations.map (cons ((name', (morph', export)), stamp ()))) (name, base_morph) (get_idents (Context.Theory thy), thy) |> snd; (* FIXME |-> put_global_idents ?*) @@ -398,14 +364,13 @@ end; - (*** Storing results ***) (* Theorems *) fun add_thmss loc kind args ctxt = let - val ([Notes args'], ctxt') = Element.activate_i [Notes (kind, args)] ctxt; + val (Notes args', ctxt') = Element.activate_i (Notes (kind, args)) ctxt; val ctxt'' = ctxt' |> ProofContext.theory ( (change_locale loc o apfst o apsnd) (cons (args', stamp ())) #> diff -r a53f4872400e -r fe4331fb3806 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue Mar 31 21:25:08 2009 +0200 +++ b/src/Pure/Isar/proof_context.ML Tue Mar 31 21:39:56 2009 +0200 @@ -582,8 +582,9 @@ | (SOME S, NONE) => S | (SOME S, SOME S') => if Type.eq_sort tsig (S, S') then S' - else error ("Sort constraint inconsistent with default for type variable " ^ - quote (Term.string_of_vname' xi))); + else error ("Sort constraint " ^ Syntax.string_of_sort_global thy S ^ + " inconsistent with default " ^ Syntax.string_of_sort_global thy S' ^ + " for type variable " ^ quote (Term.string_of_vname' xi))); in get end; local diff -r a53f4872400e -r fe4331fb3806 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Tue Mar 31 21:25:08 2009 +0200 +++ b/src/Pure/Isar/toplevel.ML Tue Mar 31 21:39:56 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 a53f4872400e -r fe4331fb3806 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Tue Mar 31 21:25:08 2009 +0200 +++ b/src/Pure/Thy/thy_info.ML Tue Mar 31 21:39:56 2009 +0200 @@ -371,7 +371,7 @@ val futures = fold fork tasks Symtab.empty; - val exns = rev tasks |> maps (fn (name, _) => + val exns = tasks |> maps (fn (name, _) => let val after_load = Future.join (the (Symtab.lookup futures name)); val proof_exns = join_thy name; diff -r a53f4872400e -r fe4331fb3806 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Tue Mar 31 21:25:08 2009 +0200 +++ b/src/Pure/Tools/find_theorems.ML Tue Mar 31 21:39:56 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 a53f4872400e -r fe4331fb3806 src/Tools/auto_solve.ML --- a/src/Tools/auto_solve.ML Tue Mar 31 21:25:08 2009 +0200 +++ b/src/Tools/auto_solve.ML Tue Mar 31 21:39:56 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