--- a/doc-src/IsarImplementation/Thy/Local_Theory.thy Wed Aug 11 17:59:33 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Local_Theory.thy Wed Aug 11 20:25:44 2010 +0200
@@ -97,7 +97,7 @@
text %mlref {*
\begin{mldecls}
@{index_ML_type local_theory: Proof.context} \\
- @{index_ML Theory_Target.init: "string option -> theory -> local_theory"} \\[1ex]
+ @{index_ML Named_Target.init: "string option -> theory -> local_theory"} \\[1ex]
@{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) ->
local_theory -> (term * (string * thm)) * local_theory"} \\
@{index_ML Local_Theory.note: "Attrib.binding * thm list ->
@@ -114,7 +114,7 @@
with operations on expecting a regular @{text "ctxt:"}~@{ML_type
Proof.context}.
- \item @{ML Theory_Target.init}~@{text "NONE thy"} initializes a
+ \item @{ML Named_Target.init}~@{text "NONE thy"} initializes a
trivial local theory from the given background theory.
Alternatively, @{text "SOME name"} may be given to initialize a
@{command locale} or @{command class} context (a fully-qualified
--- a/doc-src/IsarImplementation/Thy/document/Local_Theory.tex Wed Aug 11 17:59:33 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Local_Theory.tex Wed Aug 11 20:25:44 2010 +0200
@@ -123,7 +123,7 @@
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML type}{local\_theory}\verb|type local_theory = Proof.context| \\
- \indexdef{}{ML}{Theory\_Target.init}\verb|Theory_Target.init: string option -> theory -> local_theory| \\[1ex]
+ \indexdef{}{ML}{Named\_Target.init}\verb|Named_Target.init: string option -> theory -> local_theory| \\[1ex]
\indexdef{}{ML}{Local\_Theory.define}\verb|Local_Theory.define: (binding * mixfix) * (Attrib.binding * term) ->|\isasep\isanewline%
\verb| local_theory -> (term * (string * thm)) * local_theory| \\
\indexdef{}{ML}{Local\_Theory.note}\verb|Local_Theory.note: Attrib.binding * thm list ->|\isasep\isanewline%
@@ -139,7 +139,7 @@
any value \isa{lthy{\isacharcolon}}~\verb|local_theory| can be also used
with operations on expecting a regular \isa{ctxt{\isacharcolon}}~\verb|Proof.context|.
- \item \verb|Theory_Target.init|~\isa{NONE\ thy} initializes a
+ \item \verb|Named_Target.init|~\isa{NONE\ thy} initializes a
trivial local theory from the given background theory.
Alternatively, \isa{SOME\ name} may be given to initialize a
\hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} or \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} context (a fully-qualified
--- a/src/HOL/Hoare/Arith2.thy Wed Aug 11 17:59:33 2010 +0200
+++ b/src/HOL/Hoare/Arith2.thy Wed Aug 11 20:25:44 2010 +0200
@@ -9,17 +9,16 @@
imports Main
begin
-definition "cd" :: "[nat, nat, nat] => bool" where
- "cd x m n == x dvd m & x dvd n"
-
-definition gcd :: "[nat, nat] => nat" where
- "gcd m n == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
+definition "cd" :: "[nat, nat, nat] => bool"
+ where "cd x m n \<longleftrightarrow> x dvd m & x dvd n"
-consts fac :: "nat => nat"
+definition gcd :: "[nat, nat] => nat"
+ where "gcd m n = (SOME x. cd x m n & (!y.(cd y m n) --> y<=x))"
-primrec
+primrec fac :: "nat => nat"
+where
"fac 0 = Suc 0"
- "fac(Suc n) = (Suc n)*fac(n)"
+| "fac (Suc n) = Suc n * fac n"
subsubsection {* cd *}
--- a/src/HOL/Hoare/Heap.thy Wed Aug 11 17:59:33 2010 +0200
+++ b/src/HOL/Hoare/Heap.thy Wed Aug 11 20:25:44 2010 +0200
@@ -57,8 +57,8 @@
subsection "Non-repeating paths"
-definition distPath :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool" where
- "distPath h x as y \<equiv> Path h x as y \<and> distinct as"
+definition distPath :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool"
+ where "distPath h x as y \<longleftrightarrow> Path h x as y \<and> distinct as"
text{* The term @{term"distPath h x as y"} expresses the fact that a
non-repeating path @{term as} connects location @{term x} to location
@@ -82,8 +82,8 @@
subsubsection "Relational abstraction"
-definition List :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> bool" where
-"List h x as == Path h x as Null"
+definition List :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> bool"
+ where "List h x as = Path h x as Null"
lemma [simp]: "List h x [] = (x = Null)"
by(simp add:List_def)
@@ -133,11 +133,11 @@
subsection "Functional abstraction"
-definition islist :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> bool" where
-"islist h p == \<exists>as. List h p as"
+definition islist :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> bool"
+ where "islist h p \<longleftrightarrow> (\<exists>as. List h p as)"
-definition list :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list" where
-"list h p == SOME as. List h p as"
+definition list :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a list"
+ where "list h p = (SOME as. List h p as)"
lemma List_conv_islist_list: "List h p as = (islist h p \<and> as = list h p)"
apply(simp add:islist_def list_def)
--- a/src/HOL/Hoare/Hoare_Logic.thy Wed Aug 11 17:59:33 2010 +0200
+++ b/src/HOL/Hoare/Hoare_Logic.thy Wed Aug 11 20:25:44 2010 +0200
@@ -41,8 +41,8 @@
"Sem (Basic f) s s'" "Sem (c1;c2) s s'"
"Sem (IF b THEN c1 ELSE c2 FI) s s'"
-definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" where
- "Valid p c q == !s s'. Sem c s s' --> s : p --> s' : q"
+definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
+ where "Valid p c q \<longleftrightarrow> (!s s'. Sem c s s' --> s : p --> s' : q)"
--- a/src/HOL/Hoare/Pointer_Examples.thy Wed Aug 11 17:59:33 2010 +0200
+++ b/src/HOL/Hoare/Pointer_Examples.thy Wed Aug 11 20:25:44 2010 +0200
@@ -216,18 +216,19 @@
text"This is still a bit rough, especially the proof."
-definition cor :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
-"cor P Q == if P then True else Q"
+definition cor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
+ where "cor P Q \<longleftrightarrow> (if P then True else Q)"
-definition cand :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
-"cand P Q == if P then Q else False"
+definition cand :: "bool \<Rightarrow> bool \<Rightarrow> bool"
+ where "cand P Q \<longleftrightarrow> (if P then Q else False)"
-fun merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list" where
-"merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f)
- else y # merge(x#xs,ys,f))" |
-"merge(x#xs,[],f) = x # merge(xs,[],f)" |
-"merge([],y#ys,f) = y # merge([],ys,f)" |
-"merge([],[],f) = []"
+fun merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list"
+where
+ "merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f)
+ else y # merge(x#xs,ys,f))"
+| "merge(x#xs,[],f) = x # merge(xs,[],f)"
+| "merge([],y#ys,f) = y # merge([],ys,f)"
+| "merge([],[],f) = []"
text{* Simplifies the proof a little: *}
@@ -336,8 +337,9 @@
Path}. Since the result is not that convincing, we do not prove any of
the lemmas.*}
-consts ispath:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool"
- path:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> 'a list"
+axiomatization
+ ispath :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" and
+ path :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> 'a list"
text"First some basic lemmas:"
@@ -479,8 +481,8 @@
subsection "Storage allocation"
-definition new :: "'a set \<Rightarrow> 'a" where
-"new A == SOME a. a \<notin> A"
+definition new :: "'a set \<Rightarrow> 'a"
+ where "new A = (SOME a. a \<notin> A)"
lemma new_notin:
--- a/src/HOL/Hoare/Pointer_ExamplesAbort.thy Wed Aug 11 17:59:33 2010 +0200
+++ b/src/HOL/Hoare/Pointer_ExamplesAbort.thy Wed Aug 11 20:25:44 2010 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Hoare/Pointer_ExamplesAbort.thy
- ID: $Id$
Author: Tobias Nipkow
Copyright 2002 TUM
--- a/src/HOL/Hoare/Pointers0.thy Wed Aug 11 17:59:33 2010 +0200
+++ b/src/HOL/Hoare/Pointers0.thy Wed Aug 11 20:25:44 2010 +0200
@@ -44,11 +44,10 @@
subsection "Paths in the heap"
-consts
- Path :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
-primrec
-"Path h x [] y = (x = y)"
-"Path h x (a#as) y = (x \<noteq> Null \<and> x = a \<and> Path h (h a) as y)"
+primrec Path :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
+where
+ "Path h x [] y = (x = y)"
+| "Path h x (a#as) y = (x \<noteq> Null \<and> x = a \<and> Path h (h a) as y)"
lemma [iff]: "Path h Null xs y = (xs = [] \<and> y = Null)"
apply(case_tac xs)
@@ -73,8 +72,8 @@
subsubsection "Relational abstraction"
-definition List :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> bool" where
-"List h x as == Path h x as Null"
+definition List :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> bool"
+ where "List h x as = Path h x as Null"
lemma [simp]: "List h x [] = (x = Null)"
by(simp add:List_def)
@@ -121,11 +120,11 @@
subsection "Functional abstraction"
-definition islist :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> bool" where
-"islist h p == \<exists>as. List h p as"
+definition islist :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> bool"
+ where "islist h p \<longleftrightarrow> (\<exists>as. List h p as)"
-definition list :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list" where
-"list h p == SOME as. List h p as"
+definition list :: "('a::ref \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list"
+ where "list h p = (SOME as. List h p as)"
lemma List_conv_islist_list: "List h p as = (islist h p \<and> as = list h p)"
apply(simp add:islist_def list_def)
@@ -404,8 +403,8 @@
subsection "Storage allocation"
-definition new :: "'a set \<Rightarrow> 'a::ref" where
-"new A == SOME a. a \<notin> A & a \<noteq> Null"
+definition new :: "'a set \<Rightarrow> 'a::ref"
+ where "new A = (SOME a. a \<notin> A & a \<noteq> Null)"
lemma new_notin:
--- a/src/HOL/Hoare/README.html Wed Aug 11 17:59:33 2010 +0200
+++ b/src/HOL/Hoare/README.html Wed Aug 11 20:25:44 2010 +0200
@@ -1,7 +1,5 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<HTML>
<HEAD>
--- a/src/HOL/Hoare/SchorrWaite.thy Wed Aug 11 17:59:33 2010 +0200
+++ b/src/HOL/Hoare/SchorrWaite.thy Wed Aug 11 20:25:44 2010 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Hoare/SchorrWaite.thy
- ID: $Id$
Author: Farhad Mehta
Copyright 2003 TUM
@@ -146,14 +145,15 @@
apply(simp add:fun_upd_apply S_def)+
done
-consts
+primrec
--"Recursive definition of what is means for a the graph/stack structure to be reconstructible"
stkOk :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> ('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow>'a list \<Rightarrow> bool"
-primrec
-stkOk_nil: "stkOk c l r iL iR t [] = True"
-stkOk_cons: "stkOk c l r iL iR t (p#stk) = (stkOk c l r iL iR (Ref p) (stk) \<and>
- iL p = (if c p then l p else t) \<and>
- iR p = (if c p then t else r p))"
+where
+ stkOk_nil: "stkOk c l r iL iR t [] = True"
+| stkOk_cons:
+ "stkOk c l r iL iR t (p#stk) = (stkOk c l r iL iR (Ref p) (stk) \<and>
+ iL p = (if c p then l p else t) \<and>
+ iR p = (if c p then t else r p))"
text {* Rewrite rules for stkOk *}
--- a/src/HOL/Hoare/SepLogHeap.thy Wed Aug 11 17:59:33 2010 +0200
+++ b/src/HOL/Hoare/SepLogHeap.thy Wed Aug 11 20:25:44 2010 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Hoare/Heap.thy
- ID: $Id$
Author: Tobias Nipkow
Copyright 2002 TUM
@@ -18,11 +17,10 @@
subsection "Paths in the heap"
-consts
- Path :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> bool"
-primrec
-"Path h x [] y = (x = y)"
-"Path h x (a#as) y = (x\<noteq>0 \<and> a=x \<and> (\<exists>b. h x = Some b \<and> Path h b as y))"
+primrec Path :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> bool"
+where
+ "Path h x [] y = (x = y)"
+| "Path h x (a#as) y = (x\<noteq>0 \<and> a=x \<and> (\<exists>b. h x = Some b \<and> Path h b as y))"
lemma [iff]: "Path h 0 xs y = (xs = [] \<and> y = 0)"
by (cases xs) simp_all
@@ -41,8 +39,8 @@
subsection "Lists on the heap"
-definition List :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> bool" where
-"List h x as == Path h x as 0"
+definition List :: "heap \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> bool"
+ where "List h x as = Path h x as 0"
lemma [simp]: "List h x [] = (x = 0)"
by (simp add: List_def)
--- a/src/HOL/Hoare/Separation.thy Wed Aug 11 17:59:33 2010 +0200
+++ b/src/HOL/Hoare/Separation.thy Wed Aug 11 20:25:44 2010 +0200
@@ -16,20 +16,20 @@
text{* The semantic definition of a few connectives: *}
-definition ortho :: "heap \<Rightarrow> heap \<Rightarrow> bool" (infix "\<bottom>" 55) where
-"h1 \<bottom> h2 == dom h1 \<inter> dom h2 = {}"
+definition ortho :: "heap \<Rightarrow> heap \<Rightarrow> bool" (infix "\<bottom>" 55)
+ where "h1 \<bottom> h2 \<longleftrightarrow> dom h1 \<inter> dom h2 = {}"
-definition is_empty :: "heap \<Rightarrow> bool" where
-"is_empty h == h = empty"
+definition is_empty :: "heap \<Rightarrow> bool"
+ where "is_empty h \<longleftrightarrow> h = empty"
-definition singl:: "heap \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
-"singl h x y == dom h = {x} & h x = Some y"
+definition singl:: "heap \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+ where "singl h x y \<longleftrightarrow> dom h = {x} & h x = Some y"
-definition star:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)" where
-"star P Q == \<lambda>h. \<exists>h1 h2. h = h1++h2 \<and> h1 \<bottom> h2 \<and> P h1 \<and> Q h2"
+definition star:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)"
+ where "star P Q = (\<lambda>h. \<exists>h1 h2. h = h1++h2 \<and> h1 \<bottom> h2 \<and> P h1 \<and> Q h2)"
-definition wand:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)" where
-"wand P Q == \<lambda>h. \<forall>h'. h' \<bottom> h \<and> P h' \<longrightarrow> Q(h++h')"
+definition wand:: "(heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool) \<Rightarrow> (heap \<Rightarrow> bool)"
+ where "wand P Q = (\<lambda>h. \<forall>h'. h' \<bottom> h \<and> P h' \<longrightarrow> Q(h++h'))"
text{*This is what assertions look like without any syntactic sugar: *}
--- a/src/HOL/Tools/inductive_codegen.ML Wed Aug 11 17:59:33 2010 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Wed Aug 11 20:25:44 2010 +0200
@@ -830,10 +830,10 @@
str "case Seq.pull (testf p) of", Pretty.brk 1,
str "SOME ", mk_tuple [mk_tuple (map (str o fst) args'), str "_"],
str " =>", Pretty.brk 1, str "SOME ",
- Pretty.block (str "[" ::
- Pretty.commas (map (fn (s, T) => Pretty.block
- [mk_term_of gr "Generated" false T, Pretty.brk 1, str s]) args') @
- [str "]"]), Pretty.brk 1,
+ Pretty.enum "," "[" "]"
+ (map (fn (s, T) => Pretty.block
+ [mk_term_of gr "Generated" false T, Pretty.brk 1, str s]) args'),
+ Pretty.brk 1,
str "| NONE => NONE);"]) ^
"\n\nend;\n";
val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s;
--- a/src/Pure/Isar/attrib.ML Wed Aug 11 17:59:33 2010 +0200
+++ b/src/Pure/Isar/attrib.ML Wed Aug 11 20:25:44 2010 +0200
@@ -16,7 +16,6 @@
val defined: theory -> string -> bool
val attribute: theory -> src -> attribute
val attribute_i: theory -> src -> attribute
- val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
val map_specs: ('a -> 'att) ->
(('c * 'a list) * 'b) list -> (('c * 'att list) * 'b) list
val map_facts: ('a -> 'att) ->
@@ -25,6 +24,7 @@
val map_facts_refs: ('a -> 'att) -> ('b -> 'fact) ->
(('c * 'a list) * ('b * 'a list) list) list ->
(('c * 'att list) * ('fact * 'att list) list) list
+ val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
val crude_closure: Proof.context -> src -> src
val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
@@ -94,8 +94,7 @@
fun pretty_attribs _ [] = []
| pretty_attribs ctxt srcs =
- [Pretty.enclose "[" "]"
- (Pretty.commas (map (Args.pretty_src ctxt o Args.map_name (extern ctxt)) srcs))];
+ [Pretty.enum "," "[" "]" (map (Args.pretty_src ctxt o Args.map_name (extern ctxt)) srcs)];
(* get attributes *)
@@ -115,11 +114,6 @@
fun attribute thy = attribute_i thy o intern_src thy;
-fun eval_thms ctxt args = ProofContext.note_thmss ""
- [(Thm.empty_binding, args |> map (fn (a, atts) =>
- (ProofContext.get_fact ctxt a, map (attribute (ProofContext.theory_of ctxt)) atts)))] ctxt
- |> fst |> maps snd;
-
(* attributed declarations *)
@@ -129,6 +123,15 @@
fun map_facts_refs f g = map_facts f #> map (apsnd (map (apfst g)));
+(* fact expressions *)
+
+fun eval_thms ctxt srcs = ctxt
+ |> ProofContext.note_thmss ""
+ (map_facts_refs (attribute (ProofContext.theory_of ctxt)) (ProofContext.get_fact ctxt)
+ [((Binding.empty, []), srcs)])
+ |> fst |> maps snd;
+
+
(* crude_closure *)
(*Produce closure without knowing facts in advance! The following
--- a/src/Pure/Isar/calculation.ML Wed Aug 11 17:59:33 2010 +0200
+++ b/src/Pure/Isar/calculation.ML Wed Aug 11 20:25:44 2010 +0200
@@ -37,8 +37,10 @@
((Item_Net.merge (trans1, trans2), Thm.merge_thms (sym1, sym2)), NONE);
);
+val get_rules = #1 o Data.get o Context.Proof;
+
fun print_rules ctxt =
- let val ((trans, sym), _) = Data.get (Context.Proof ctxt) in
+ let val (trans, sym) = get_rules ctxt in
[Pretty.big_list "transitivity rules:"
(map (Display.pretty_thm ctxt) (Item_Net.content trans)),
Pretty.big_list "symmetry rules:" (map (Display.pretty_thm ctxt) sym)]
@@ -122,21 +124,21 @@
(* also and finally *)
-val get_rules = #1 o Data.get o Context.Proof o Proof.context_of;
-
fun calculate prep_rules final raw_rules int state =
let
+ val ctxt = Proof.context_of state;
+
val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
val eq_prop = op aconv o pairself (Envir.beta_eta_contract o strip_assums_concl);
fun projection ths th = exists (curry eq_prop th) ths;
- val opt_rules = Option.map (prep_rules state) raw_rules;
+ val opt_rules = Option.map (prep_rules ctxt) raw_rules;
fun combine ths =
(case opt_rules of SOME rules => rules
| NONE =>
(case ths of
- [] => Item_Net.content (#1 (get_rules state))
- | th :: _ => Item_Net.retrieve (#1 (get_rules state)) (strip_assums_concl th)))
+ [] => Item_Net.content (#1 (get_rules ctxt))
+ | th :: _ => Item_Net.retrieve (#1 (get_rules ctxt)) (strip_assums_concl th)))
|> Seq.of_list |> Seq.maps (Drule.multi_resolve ths)
|> Seq.filter (not o projection ths);
@@ -154,9 +156,9 @@
end;
val also = calculate (K I) false;
-val also_cmd = calculate Proof.get_thmss_cmd false;
+val also_cmd = calculate Attrib.eval_thms false;
val finally = calculate (K I) true;
-val finally_cmd = calculate Proof.get_thmss_cmd true;
+val finally_cmd = calculate Attrib.eval_thms true;
(* moreover and ultimately *)
--- a/src/Pure/Isar/isar_cmd.ML Wed Aug 11 17:59:33 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Wed Aug 11 20:25:44 2010 +0200
@@ -416,7 +416,7 @@
fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
Thm_Deps.thm_deps (Toplevel.theory_of state)
- (Proof.get_thmss_cmd (Toplevel.enter_proof_body state) args));
+ (Attrib.eval_thms (Toplevel.context_of state) args));
(* find unused theorems *)
@@ -450,20 +450,20 @@
local
-fun string_of_stmts state args =
- Proof.get_thmss_cmd state args
- |> map (Element.pretty_statement (Proof.context_of state) Thm.theoremK)
+fun string_of_stmts ctxt args =
+ Attrib.eval_thms ctxt args
+ |> map (Element.pretty_statement ctxt Thm.theoremK)
|> Pretty.chunks2 |> Pretty.string_of;
-fun string_of_thms state args =
- Pretty.string_of (Display.pretty_thms (Proof.context_of state) (Proof.get_thmss_cmd state args));
+fun string_of_thms ctxt args =
+ Pretty.string_of (Display.pretty_thms ctxt (Attrib.eval_thms ctxt args));
fun string_of_prfs full state arg =
Pretty.string_of
(case arg of
NONE =>
let
- val {context = ctxt, goal = thm} = Proof.simple_goal state;
+ val {context = ctxt, goal = thm} = Proof.simple_goal (Toplevel.proof_of state);
val thy = ProofContext.theory_of ctxt;
val prf = Thm.proof_of thm;
val prop = Thm.full_prop_of thm;
@@ -472,20 +472,19 @@
Proof_Syntax.pretty_proof ctxt
(if full then Reconstruct.reconstruct_proof thy prop prf' else prf')
end
- | SOME args => Pretty.chunks
- (map (Proof_Syntax.pretty_proof_of (Proof.context_of state) full)
- (Proof.get_thmss_cmd state args)));
+ | SOME srcs =>
+ let val ctxt = Toplevel.context_of state
+ in map (Proof_Syntax.pretty_proof_of ctxt full) (Attrib.eval_thms ctxt srcs) end
+ |> Pretty.chunks);
-fun string_of_prop state s =
+fun string_of_prop ctxt s =
let
- val ctxt = Proof.context_of state;
val prop = Syntax.read_prop ctxt s;
val ctxt' = Variable.auto_fixes prop ctxt;
in Pretty.string_of (Pretty.quote (Syntax.pretty_term ctxt' prop)) end;
-fun string_of_term state s =
+fun string_of_term ctxt s =
let
- val ctxt = Proof.context_of state;
val t = Syntax.read_term ctxt s;
val T = Term.type_of t;
val ctxt' = Variable.auto_fixes t ctxt;
@@ -495,24 +494,21 @@
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)])
end;
-fun string_of_type state s =
- let
- val ctxt = Proof.context_of state;
- val T = Syntax.read_typ ctxt s;
+fun string_of_type ctxt s =
+ let val T = Syntax.read_typ ctxt s
in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end;
fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
- Print_Mode.with_modes modes (fn () =>
- writeln (string_of (Toplevel.enter_proof_body state) arg)) ());
+ Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) ());
in
-val print_stmts = print_item string_of_stmts;
-val print_thms = print_item string_of_thms;
+val print_stmts = print_item (string_of_stmts o Toplevel.context_of);
+val print_thms = print_item (string_of_thms o Toplevel.context_of);
val print_prfs = print_item o string_of_prfs;
-val print_prop = print_item string_of_prop;
-val print_term = print_item string_of_term;
-val print_type = print_item string_of_type;
+val print_prop = print_item (string_of_prop o Toplevel.context_of);
+val print_term = print_item (string_of_term o Toplevel.context_of);
+val print_type = print_item (string_of_type o Toplevel.context_of);
end;
--- a/src/Pure/Isar/proof.ML Wed Aug 11 17:59:33 2010 +0200
+++ b/src/Pure/Isar/proof.ML Wed Aug 11 20:25:44 2010 +0200
@@ -60,7 +60,6 @@
val def_cmd: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state
val chain: state -> state
val chain_facts: thm list -> state -> state
- val get_thmss_cmd: state -> (Facts.ref * Attrib.src list) list -> thm list
val note_thmss: (Thm.binding * (thm list * attribute list) list) list -> state -> state
val note_thmss_cmd: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
val from_thmss: ((thm list * attribute list) list) list -> state -> state
@@ -679,8 +678,6 @@
val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
-fun get_thmss_cmd state srcs = the_facts (note_thmss_cmd [((Binding.empty, []), srcs)] state);
-
end;
--- a/src/Pure/Isar/proof_context.ML Wed Aug 11 17:59:33 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML Wed Aug 11 20:25:44 2010 +0200
@@ -1123,7 +1123,7 @@
val type_notation = gen_notation (K type_syntax);
val notation = gen_notation const_syntax;
-fun target_type_notation add mode args phi =
+fun target_type_notation add mode args phi =
let
val args' = args |> map_filter (fn (T, mx) =>
let
--- a/src/Pure/Isar/toplevel.ML Wed Aug 11 17:59:33 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML Wed Aug 11 20:25:44 2010 +0200
@@ -20,7 +20,6 @@
val theory_of: state -> theory
val proof_of: state -> Proof.state
val proof_position_of: state -> int
- val enter_proof_body: state -> Proof.state
val end_theory: Position.T -> state -> theory
val print_state_context: state -> unit
val print_state: bool -> state -> unit
@@ -188,8 +187,6 @@
Proof (prf, _) => Proof_Node.position prf
| _ => raise UNDEF);
-val enter_proof_body = node_case (Proof.init o Context.proof_of) Proof.enter_forward;
-
fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = Theory.end_theory thy
| end_theory pos _ = error ("Unfinished theory at end of input" ^ Position.str_of pos);
--- a/src/Pure/Syntax/ast.ML Wed Aug 11 17:59:33 2010 +0200
+++ b/src/Pure/Syntax/ast.ML Wed Aug 11 20:25:44 2010 +0200
@@ -75,8 +75,7 @@
fun pretty_ast (Constant a) = Pretty.quote (Pretty.str a)
| pretty_ast (Variable x) = Pretty.str x
- | pretty_ast (Appl asts) =
- Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));
+ | pretty_ast (Appl asts) = Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));
fun pretty_rule (lhs, rhs) =
Pretty.block [pretty_ast lhs, Pretty.str " ->", Pretty.brk 2, pretty_ast rhs];
--- a/src/Pure/Tools/find_consts.ML Wed Aug 11 17:59:33 2010 +0200
+++ b/src/Pure/Tools/find_consts.ML Wed Aug 11 20:25:44 2010 +0200
@@ -28,24 +28,13 @@
(* matching types/consts *)
fun matches_subtype thy typat =
- let
- val p = can (fn ty => Sign.typ_match thy (typat, ty) Vartab.empty);
-
- fun fs [] = false
- | fs (t :: ts) = f t orelse fs ts
+ Term.exists_subtype (fn ty => Sign.typ_instance thy (ty, typat));
- and f (t as Type (_, ars)) = p t orelse fs ars
- | f t = p t;
- in f end;
-
-fun check_const p (nm, (ty, _)) =
- if p (nm, ty)
- then SOME (Term.size_of_typ ty)
- else NONE;
+fun check_const pred (nm, (ty, _)) =
+ if pred (nm, ty) then SOME (Term.size_of_typ ty) else NONE;
fun opt_not f (c as (_, (ty, _))) =
- if is_some (f c)
- then NONE else SOME (Term.size_of_typ ty);
+ if is_some (f c) then NONE else SOME (Term.size_of_typ ty);
fun filter_const _ NONE = NONE
| filter_const f (SOME (c, r)) =
@@ -71,8 +60,7 @@
val ty' = Logic.unvarifyT_global ty;
in
Pretty.block
- [Pretty.quote (Pretty.str nm), Pretty.fbrk,
- Pretty.str "::", Pretty.brk 1,
+ [Pretty.str nm, Pretty.str " ::", Pretty.brk 1,
Pretty.quote (Syntax.pretty_typ ctxt ty')]
end;
@@ -128,35 +116,35 @@
val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
in
- Pretty.big_list "searched for:" (map pretty_criterion raw_criteria)
- :: Pretty.str ""
- :: (Pretty.str o implode)
- (if null matches
- then ["nothing found", end_msg]
- else ["found ", (string_of_int o length) matches,
- " constants", end_msg, ":"])
- :: Pretty.str ""
- :: map (pretty_const ctxt) matches
- |> Pretty.chunks
- |> Pretty.writeln
- end;
+ Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) ::
+ Pretty.str "" ::
+ Pretty.str
+ (if null matches
+ then "nothing found" ^ end_msg
+ else "found " ^ string_of_int (length matches) ^ " constant(s)" ^ end_msg ^ ":") ::
+ Pretty.str "" ::
+ map (pretty_const ctxt) matches
+ end |> Pretty.chunks |> Pretty.writeln;
(* command syntax *)
-fun find_consts_cmd spec =
- Toplevel.unknown_theory o Toplevel.keep (fn state =>
- find_consts (Proof.context_of (Toplevel.enter_proof_body state)) spec);
+local
val criterion =
Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Strict ||
Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
Parse.xname >> Loose;
+in
+
val _ =
Outer_Syntax.improper_command "find_consts" "search constants by type pattern" Keyword.diag
(Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion)
- >> (Toplevel.no_timing oo find_consts_cmd));
+ >> (fn spec => Toplevel.no_timing o
+ Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec)));
end;
+end;
+
--- a/src/Pure/Tools/find_theorems.ML Wed Aug 11 17:59:33 2010 +0200
+++ b/src/Pure/Tools/find_theorems.ML Wed Aug 11 20:25:44 2010 +0200
@@ -433,36 +433,27 @@
val tally_msg =
(case foundo of
- NONE => "displaying " ^ string_of_int returned ^ " theorems"
+ NONE => "displaying " ^ string_of_int returned ^ " theorem(s)"
| SOME found =>
- "found " ^ string_of_int found ^ " theorems" ^
+ "found " ^ string_of_int found ^ " theorem(s)" ^
(if returned < found
then " (" ^ string_of_int returned ^ " displayed)"
else ""));
val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
in
- Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria)
- :: Pretty.str "" ::
- (if null thms then [Pretty.str ("nothing found" ^ end_msg)]
- else
- [Pretty.str (tally_msg ^ end_msg ^ ":"), Pretty.str ""] @
+ Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) ::
+ Pretty.str "" ::
+ (if null thms then [Pretty.str ("nothing found" ^ end_msg)]
+ else
+ [Pretty.str (tally_msg ^ end_msg ^ ":"), Pretty.str ""] @
map (pretty_thm ctxt) thms)
- |> Pretty.chunks |> Pretty.writeln
- end;
+ end |> Pretty.chunks |> Pretty.writeln;
(** command syntax **)
-fun find_theorems_cmd ((opt_lim, rem_dups), spec) =
- Toplevel.unknown_theory o Toplevel.keep (fn state =>
- let
- val proof_state = Toplevel.enter_proof_body state;
- val ctxt = Proof.context_of proof_state;
- val opt_goal = try Proof.simple_goal proof_state |> Option.map #goal;
- in print_theorems ctxt opt_goal opt_lim rem_dups spec end);
-
local
val criterion =
@@ -486,7 +477,13 @@
Outer_Syntax.improper_command "find_theorems" "print theorems meeting specified criteria"
Keyword.diag
(options -- Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion))
- >> (Toplevel.no_timing oo find_theorems_cmd));
+ >> (fn ((opt_lim, rem_dups), spec) =>
+ Toplevel.no_timing o
+ Toplevel.keep (fn state =>
+ let
+ val ctxt = Toplevel.context_of state;
+ val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal;
+ in print_theorems ctxt opt_goal opt_lim rem_dups spec end)));
end;
--- a/src/Pure/codegen.ML Wed Aug 11 17:59:33 2010 +0200
+++ b/src/Pure/codegen.ML Wed Aug 11 20:25:44 2010 +0200
@@ -889,9 +889,8 @@
mk_app false (str "testf") (map (str o fst) args),
Pretty.brk 1, str "then NONE",
Pretty.brk 1, str "else ",
- Pretty.block [str "SOME ", Pretty.block (str "[" ::
- Pretty.commas (map (fn (s, _) => str (s ^ "_t ()")) args) @
- [str "]"])]]),
+ Pretty.block [str "SOME ",
+ Pretty.enum "," "[" "]" (map (fn (s, _) => str (s ^ "_t ()")) args)]]),
str ");"]) ^
"\n\nend;\n";
val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s;