Merged.
--- 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=""
--- 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}}
--- 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 *}
--- 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 \<rightarrow> L"} an order-preserving map.
+ Then @{text "\<Sqinter>{x \<in> L | f(x) \<le> 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 \<in> L | f(x) \<le> x}"} and @{text "a =
+ \<Sqinter>H"}. For all @{text "x \<in> H"} we have @{text "a \<le> x"}, so @{text
+ "f(a) \<le> f(x) \<le> x"}. Thus @{text "f(a)"} is a lower bound of @{text
+ H}, whence @{text "f(a) \<le> 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)) \<le>
+ f(a)"}. This says @{text "f(a) \<in> H"}, so @{text "a \<le> 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 \<Rightarrow> 'a"
+ assumes "mono f"
+ shows "\<exists>a. f a = a"
proof
- let ?H = "{u. f u <= u}"
- let ?a = "Inter ?H"
-
- assume mono: "mono f"
+ let ?H = "{u. f u \<le> u}"
+ let ?a = "\<Sqinter>?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 \<in> ?H"
+ then have "?a \<le> x" by (rule Inf_lower)
+ with `mono f` have "f ?a \<le> f x" ..
+ also from `x \<in> ?H` have "\<dots> \<le> x" ..
+ finally have "f ?a \<le> x" .
}
- hence ge: "f ?a <= ?a" by (rule Inter_greatest)
+ then have "f ?a \<le> ?a" by (rule Inf_greatest)
{
- also presume "... <= f ?a"
+ also presume "\<dots> \<le> 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 \<le> ?a` have "f (f ?a) \<le> f ?a" ..
+ then have "f ?a \<in> ?H" ..
+ then show "?a \<le> 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 \<Rightarrow> 'a"
+ assumes "mono f"
+ shows "\<exists>a. f a = a"
proof
- let ?H = "{u. f u <= u}"
- let ?a = "Inter ?H"
-
- assume mono: "mono f"
+ let ?H = "{u. f u \<le> u}"
+ let ?a = "\<Sqinter>?H"
show "f ?a = ?a"
proof (rule order_antisym)
- show ge: "f ?a <= ?a"
- proof (rule Inter_greatest)
+ show "f ?a \<le> ?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 \<in> ?H"
+ then have "?a \<le> x" by (rule Inf_lower)
+ with `mono f` have "f ?a \<le> f x" ..
+ also from `x \<in> ?H` have "\<dots> \<le> x" ..
+ finally show "f ?a \<le> 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 \<le> f ?a"
+ proof (rule Inf_lower)
+ from `mono f` and `f ?a \<le> ?a` have "f (f ?a) \<le> f ?a" ..
+ then show "f ?a \<in> ?H" ..
qed
qed
qed
--- 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}
--- 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 **)
--- 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]:
- "\<not> Sup {}"
+ "\<not> \<Squnion>{}"
unfolding Sup_bool_def by auto
--- 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;
--- 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
--- 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
--- 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
--- 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]
--- 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 \<le> of_num n"
+lemma minus_one_less_one_iff: "- 1 < 1"
+using minus_of_num_less_of_num_iff [of One One] by (simp add: of_num_one)
+
+lemma minus_of_num_le_of_num_iff: "- of_num m \<le> of_num n"
by (simp add: less_imp_le minus_of_num_less_of_num_iff)
-lemma minus_of_num_le_one_iff [numeral]: "- of_num n \<le> 1"
+lemma minus_of_num_le_one_iff: "- of_num n \<le> 1"
by (simp add: less_imp_le minus_of_num_less_one_iff)
-lemma minus_one_le_of_num_iff [numeral]: "- 1 \<le> of_num n"
+lemma minus_one_le_of_num_iff: "- 1 \<le> of_num n"
by (simp add: less_imp_le minus_one_less_of_num_iff)
-lemma of_num_le_minus_of_num_iff [numeral]: "\<not> of_num m \<le> - of_num n"
+lemma minus_one_le_one_iff: "- 1 \<le> 1"
+ by (simp add: less_imp_le minus_one_less_one_iff)
+
+lemma of_num_le_minus_of_num_iff: "\<not> of_num m \<le> - of_num n"
by (simp add: not_le minus_of_num_less_of_num_iff)
-lemma one_le_minus_of_num_iff [numeral]: "\<not> 1 \<le> - of_num n"
+lemma one_le_minus_of_num_iff: "\<not> 1 \<le> - of_num n"
by (simp add: not_le minus_of_num_less_one_iff)
-lemma of_num_le_minus_one_iff [numeral]: "\<not> of_num n \<le> - 1"
+lemma of_num_le_minus_one_iff: "\<not> of_num n \<le> - 1"
by (simp add: not_le minus_one_less_of_num_iff)
-lemma of_num_less_minus_of_num_iff [numeral]: "\<not> of_num m < - of_num n"
+lemma one_le_minus_one_iff: "\<not> 1 \<le> - 1"
+ by (simp add: not_le minus_one_less_one_iff)
+
+lemma of_num_less_minus_of_num_iff: "\<not> of_num m < - of_num n"
by (simp add: not_less minus_of_num_le_of_num_iff)
-lemma one_less_minus_of_num_iff [numeral]: "\<not> 1 < - of_num n"
+lemma one_less_minus_of_num_iff: "\<not> 1 < - of_num n"
by (simp add: not_less minus_of_num_le_one_iff)
-lemma of_num_less_minus_one_iff [numeral]: "\<not> of_num n < - 1"
+lemma of_num_less_minus_one_iff: "\<not> of_num n < - 1"
by (simp add: not_less minus_one_le_of_num_iff)
+lemma one_less_minus_one_iff: "\<not> 1 < - 1"
+ by (simp add: not_less minus_one_le_one_iff)
+
+lemmas le_signed_numeral_special [numeral] =
+ minus_of_num_le_of_num_iff
+ minus_of_num_le_one_iff
+ minus_one_le_of_num_iff
+ minus_one_le_one_iff
+ of_num_le_minus_of_num_iff
+ one_le_minus_of_num_iff
+ of_num_le_minus_one_iff
+ one_le_minus_one_iff
+
+lemmas less_signed_numeral_special [numeral] =
+ minus_of_num_less_of_num_iff
+ minus_of_num_less_one_iff
+ minus_one_less_of_num_iff
+ minus_one_less_one_iff
+ of_num_less_minus_of_num_iff
+ one_less_minus_of_num_iff
+ of_num_less_minus_one_iff
+ one_less_minus_one_iff
+
end
subsubsection {*
--- a/src/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 \<Rightarrow> next yield xq | Some (x, Q) \<Rightarrow> Some (x, Predicate.Seq (\<lambda>_. Predicate.Join Q xq)))"
-primrec pull :: "('a Predicate.pred \<Rightarrow> ('a \<times> 'a Predicate.pred) option)
- \<Rightarrow> nat \<Rightarrow> 'a Predicate.pred \<Rightarrow> 'a list \<times> 'a Predicate.pred" where
- "pull yield 0 P = ([], \<bottom>)"
- | "pull yield (Suc n) P = (case yield P
- of None \<Rightarrow> ([], \<bottom>) | Some (x, Q) \<Rightarrow> 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 "\<bottom> :: 'a Predicate.pred"} (*replace bottom with sequence to evaluate*)
+end
+*}
+
+fun anamorph :: "('b \<Rightarrow> ('a \<times> 'b) option) \<Rightarrow> index \<Rightarrow> 'b \<Rightarrow> 'a list \<times> 'b" where
+ "anamorph f k x = (if k = 0 then ([], x)
+ else case f x of None \<Rightarrow> ([], x) | Some (v, y) \<Rightarrow> 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 "\<bottom> :: 'a Predicate.pred"} (*replace bottom with sequence to evaluate*)
+end
+*}
end
\ No newline at end of file
--- 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]:
--- 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: "<a> ooo s << t ==> EX tt. t = <a> ooo tt & s << tt"
apply (simp add: fsingleton_def2)
apply (insert stream_prefix [of "Def a" s t], auto)
-by (auto simp add: stream.inverts)
+done
lemma fstreams_prefix': "x << <a> ooo z = (x = <> | (EX y. x = <a> ooo y & y << z))"
apply (auto, case_tac "x=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
apply (simp add: fsingleton_def2, auto)
-apply (auto simp add: stream.inverts)
apply (drule ax_flat, simp)
by (erule sconc_mono)
@@ -197,8 +196,7 @@
by auto
lemma fstreams_mono: "<a> ooo b << <a> ooo c ==> b << c"
-apply (simp add: fsingleton_def2)
-by (auto simp add: stream.inverts)
+by (simp add: fsingleton_def2)
lemma fsmap_UU[simp]: "fsmap f$UU = UU"
by (simp add: fsmap_def)
@@ -220,7 +218,6 @@
apply (drule stream_exhaust_eq [THEN iffD1], auto)
apply (case_tac "y=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
-apply (auto simp add: stream.inverts)
apply (simp add: flat_less_iff)
apply (case_tac "s=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
@@ -344,7 +341,3 @@
by (erule ch2ch_monofun, simp)
end
-
-
-
-
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy Tue Mar 31 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<<b>>t) = (a = b & s<<t)"
apply (simp add: Consq_def2)
-apply (simp add: seq.inverts)
done
lemma seq_take_Cons: "seq_take (Suc n)$(a>>x) = a>> (seq_take n$x)"
@@ -661,7 +660,7 @@
(Forall (%x. ~P x) ys & Finite ys)"
apply (rule_tac x="ys" in Seq_induct)
(* adm *)
-apply (simp add: seq.compacts Forall_def sforall_def)
+apply (simp add: Forall_def sforall_def)
(* base cases *)
apply simp
apply simp
--- a/src/HOLCF/Tools/domain/domain_theorems.ML Tue Mar 31 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)
--- 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 ~= \<bottom> & Fin n < #y)"
apply (auto, case_tac "x=UU",auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
-apply (rule_tac x="a" in exI)
-apply (rule_tac x="y" in exI, simp)
apply (case_tac "#y") apply simp_all
apply (case_tac "#y") apply simp_all
done
@@ -387,15 +381,11 @@
by (simp add: slen_def)
lemma slen_scons_eq_rev: "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a && y | a = \<bottom> | #y < Fin (Suc n))"
-apply (rule stream.casedist [of x], auto)
-apply ((*drule sym,*) drule scons_eq_UU [THEN iffD1],auto)
-apply (simp add: zero_inat_def)
-apply (subgoal_tac "s=y & aa=a", simp)
-apply (simp_all add: not_less iSuc_Fin)
-apply (case_tac "#y") apply (simp_all add: iSuc_Fin)
-apply (case_tac "aa=UU", auto)
-apply (erule_tac x="a" in allE, simp)
-apply (case_tac "#s") apply (simp_all add: iSuc_Fin)
+ apply (rule stream.casedist [of x], auto)
+ apply ((*drule sym,*) drule scons_eq_UU [THEN iffD1],auto)
+ apply (simp add: zero_inat_def)
+ apply (case_tac "#s") apply (simp_all add: iSuc_Fin)
+ apply (case_tac "#s") apply (simp_all add: iSuc_Fin)
done
lemma slen_take_lemma4 [rule_format]:
@@ -463,8 +453,7 @@
apply (erule stream_finite_ind [of s], auto)
apply (case_tac "t=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1], auto)
-apply (erule_tac x="y" in allE, auto)
-by (auto simp add: stream.inverts)
+done
lemma slen_mono: "s << t ==> #s <= #t"
apply (case_tac "stream_finite t")
@@ -493,7 +482,6 @@
apply (case_tac "y=UU", clarsimp)
apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)+
apply (erule_tac x="ya" in allE, simp)
-apply (auto simp add: stream.inverts)
by (drule ax_flat, simp)
lemma slen_strict_mono_lemma:
@@ -501,7 +489,6 @@
apply (erule stream_finite_ind, auto)
apply (case_tac "sa=UU", auto)
apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
-apply (simp add: stream.inverts, clarsimp)
by (drule ax_flat, simp)
lemma slen_strict_mono: "[|stream_finite t; s ~= t; s << (t::'a::flat stream) |] ==> #s < #t"
@@ -653,7 +640,7 @@
apply (simp add: i_th_def i_rt_Suc_back)
apply (rule stream.casedist [of "i_rt n s1"],simp)
apply (rule stream.casedist [of "i_rt n s2"],auto)
-by (intro monofun_cfun, auto)
+done
lemma i_th_stream_take_Suc [rule_format]:
"ALL s. i_th n (stream_take (Suc n)$s) = i_th n s"
--- a/src/Pure/General/binding.ML Tue Mar 31 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 *)
--- 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;
--- 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;
--- 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;
--- 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 ()))
#>
--- 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
--- 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;
--- 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;
--- 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) =
--- 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