# HG changeset patch # User haftmann # Date 1236334257 -3600 # Node ID 6c74ef5a349f51eb23311dce44a078250d86b4da # Parent d6bffd97d8d56e1f3c3b25530f31dccc3721444a# Parent 8f4d5eaa98789e18e746fbe27659f247d3a7c9ff merged diff -r 8f4d5eaa9878 -r 6c74ef5a349f Admin/makedist --- a/Admin/makedist Fri Mar 06 11:10:18 2009 +0100 +++ b/Admin/makedist Fri Mar 06 11:10:57 2009 +0100 @@ -144,7 +144,7 @@ echo "###" find . -name .cvsignore -print | xargs rm -rf -find . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -x +find . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -f -x find . -print | xargs chmod u+rw ./Admin/build all || fail "Failed to build distribution" diff -r 8f4d5eaa9878 -r 6c74ef5a349f doc-src/IsarImplementation/Thy/Logic.thy --- a/doc-src/IsarImplementation/Thy/Logic.thy Fri Mar 06 11:10:18 2009 +0100 +++ b/doc-src/IsarImplementation/Thy/Logic.thy Fri Mar 06 11:10:57 2009 +0100 @@ -556,7 +556,7 @@ @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\ @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\ @{index_ML Thm.axiom: "theory -> string -> thm"} \\ - @{index_ML Thm.add_oracle: "bstring * ('a -> cterm) -> theory + @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory"} \\ \end{mldecls} \begin{mldecls} @@ -613,7 +613,7 @@ \item @{ML Thm.axiom}~@{text "thy name"} retrieves a named axiom, cf.\ @{text "axiom"} in \figref{fig:prim-rules}. - \item @{ML Thm.add_oracle}~@{text "(name, oracle)"} produces a named + \item @{ML Thm.add_oracle}~@{text "(binding, oracle)"} produces a named oracle rule, essentially generating arbitrary axioms on the fly, cf.\ @{text "axiom"} in \figref{fig:prim-rules}. diff -r 8f4d5eaa9878 -r 6c74ef5a349f doc-src/IsarImplementation/Thy/Prelim.thy --- a/doc-src/IsarImplementation/Thy/Prelim.thy Fri Mar 06 11:10:18 2009 +0100 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy Fri Mar 06 11:10:57 2009 +0100 @@ -682,7 +682,7 @@ text %mlref {* \begin{mldecls} - @{index_ML NameSpace.base: "string -> string"} \\ + @{index_ML NameSpace.base_name: "string -> string"} \\ @{index_ML NameSpace.qualifier: "string -> string"} \\ @{index_ML NameSpace.append: "string -> string -> string"} \\ @{index_ML NameSpace.implode: "string list -> string"} \\ @@ -698,14 +698,15 @@ @{index_ML_type NameSpace.T} \\ @{index_ML NameSpace.empty: NameSpace.T} \\ @{index_ML NameSpace.merge: "NameSpace.T * NameSpace.T -> NameSpace.T"} \\ - @{index_ML NameSpace.declare: "NameSpace.naming -> binding -> NameSpace.T -> string * NameSpace.T"} \\ + @{index_ML NameSpace.declare: "NameSpace.naming -> binding -> NameSpace.T -> + string * NameSpace.T"} \\ @{index_ML NameSpace.intern: "NameSpace.T -> string -> string"} \\ @{index_ML NameSpace.extern: "NameSpace.T -> string -> string"} \\ \end{mldecls} \begin{description} - \item @{ML NameSpace.base}~@{text "name"} returns the base name of a + \item @{ML NameSpace.base_name}~@{text "name"} returns the base name of a qualified name. \item @{ML NameSpace.qualifier}~@{text "name"} returns the qualifier @@ -728,8 +729,8 @@ \item @{ML NameSpace.add_path}~@{text "path naming"} augments the naming policy by extending its path component. - \item @{ML NameSpace.full_name}@{text "naming binding"} turns a name - binding (usually a basic name) into the fully qualified + \item @{ML NameSpace.full_name}~@{text "naming binding"} turns a + name binding (usually a basic name) into the fully qualified internal name, according to the given naming policy. \item @{ML_type NameSpace.T} represents name spaces. @@ -755,8 +756,8 @@ \item @{ML NameSpace.extern}~@{text "space name"} externalizes a (fully qualified) internal name. - This operation is mostly for printing! Note unqualified names are - produced via @{ML NameSpace.base}. + This operation is mostly for printing! User code should not rely on + the precise result too much. \end{description} *} diff -r 8f4d5eaa9878 -r 6c74ef5a349f etc/settings --- a/etc/settings Fri Mar 06 11:10:18 2009 +0100 +++ b/etc/settings Fri Mar 06 11:10:57 2009 +0100 @@ -262,8 +262,6 @@ # zChaff (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML) #ZCHAFF_HOME=/usr/local/bin -#ZCHAFF_VERSION=2004.5.13 -#ZCHAFF_VERSION=2004.11.15 # BerkMin561 (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML) #BERKMIN_HOME=/usr/local/bin diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Docs/MainDoc.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Docs/MainDoc.thy Fri Mar 06 11:10:57 2009 +0100 @@ -0,0 +1,470 @@ +(*<*) +theory MainDoc +imports Main +begin + +ML {* +fun pretty_term_type_only ctxt (t, T) = + (if fastype_of t = Sign.certify_typ (ProofContext.theory_of ctxt) T then () + else error "term_type_only: type mismatch"; + Syntax.pretty_typ ctxt T) + +val _ = ThyOutput.add_commands + [("term_type_only", ThyOutput.args (Args.term -- Args.typ_abbrev) (ThyOutput.output pretty_term_type_only))]; +*} +(*>*) +text{* + +\begin{abstract} +This document lists the main types, functions and syntax provided by theory @{theory Main}. It is meant as a quick overview of what is available. The sophisicated class structure is only hinted at. +\end{abstract} + +\section{HOL} + +The basic logic: @{prop "x = y"}, @{const True}, @{const False}, @{prop"Not P"}, @{prop"P & Q"}, @{prop "P | Q"}, @{prop "P --> Q"}, @{prop"ALL x. P"}, @{prop"EX x. P"}, @{prop"EX! x. P"}, @{term"THE x. P"}. + +Overloaded operators: + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +@{text "0"} & @{typeof HOL.zero}\\ +@{text "1"} & @{typeof HOL.one}\\ +@{const HOL.plus} & @{typeof HOL.plus}\\ +@{const HOL.minus} & @{typeof HOL.minus}\\ +@{const HOL.uminus} & @{typeof HOL.uminus}\\ +@{const HOL.times} & @{typeof HOL.times}\\ +@{const HOL.inverse} & @{typeof HOL.inverse}\\ +@{const HOL.divide} & @{typeof HOL.divide}\\ +@{const HOL.abs} & @{typeof HOL.abs}\\ +@{const HOL.sgn} & @{typeof HOL.sgn}\\ +@{const HOL.less_eq} & @{typeof HOL.less_eq}\\ +@{const HOL.less} & @{typeof HOL.less}\\ +@{const HOL.default} & @{typeof HOL.default}\\ +@{const HOL.undefined} & @{typeof HOL.undefined}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +@{term"~(x = y)"} & @{term[source]"\ (x = y)"}\\ +@{term[source]"P \ Q"} & @{term"P \ Q"}\\ +@{term"If x y z"} & @{term[source]"If x y z"}\\ +@{term"Let e\<^isub>1 (%x. e\<^isub>2)"} & @{term[source]"Let e\<^isub>1 (\x. e\<^isub>2)"}\\ +@{term"abs x"} & @{term[source]"abs x"}\\ +@{term"uminus x"} & @{term[source]"uminus x"}\\ +\end{supertabular} + +\section{Orderings} + +A collection of classes constraining @{text"\"} and @{text"<"}: +preorders, partial orders, linear orders, dense linear orders and wellorders. + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +@{const Orderings.Least} & @{typeof Orderings.Least}\\ +@{const Orderings.min} & @{typeof Orderings.min}\\ +@{const Orderings.max} & @{typeof Orderings.max}\\ +@{const Orderings.mono} & @{typeof Orderings.mono}\\ +\end{tabular} + +\subsubsection*{Syntax} + +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +@{term[source]"x \ y"} & @{term"x \ y"}\\ +@{term[source]"x > y"} & @{term"x > y"}\\ +@{term"ALL x<=y. P"} & @{term[source]"\x. x \ y \ P"}\\ +@{term"ALL xx. x < y \ P"}\\ +@{term"ALL x>=y. P"} & @{term[source]"\x. x \ y \ P"}\\ +@{term"ALL x>y. P"} & @{term[source]"\x. x > y \ P"}\\ +@{term"LEAST x. P"} & @{term[source]"Least (\x. P)"}\\ +\end{supertabular} + +Similar for @{text"\"} instead of @{text"\"}. + +\section{Set} + +Sets are predicates: @{text[source]"'a set = 'a \ bool"} +\bigskip + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +@{const "{}"} & @{term_type_only "{}" "'a set"}\\ +@{const insert} & @{term_type_only insert "'a\'a set\'a set"}\\ +@{const Collect} & @{term_type_only Collect "('a\bool)\'a set"}\\ +@{const "op :"} & @{term_type_only "op :" "'a\'a set\bool"}\\ +@{const "op Un"} & @{term_type_only "op Un" "'a set\'a set \ 'a set"}\\ +@{const "op Int"} & @{term_type_only "op Int" "'a set\'a set \ 'a set"}\\ +@{const UNION} & @{term_type_only UNION "'a set\('a \ 'b set) \ 'b set"}\\ +@{const INTER} & @{term_type_only INTER "'a set\('a \ 'b set) \ 'b set"}\\ +@{const Union} & @{term_type_only Union "'a set set\'a set"}\\ +@{const Inter} & @{term_type_only Inter "'a set set\'a set"}\\ +@{const Pow} & @{term_type_only Pow "'a set \'a set set"}\\ +@{const UNIV} & @{term_type_only UNIV "'a set"}\\ +@{const image} & @{term_type_only image "('a\'b)\'a set\'b set"}\\ +@{const Ball} & @{term_type_only Ball "'a set\('a\bool)\bool"}\\ +@{const Bex} & @{term_type_only Bex "'a set\('a\bool)\bool"}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +@{text"{x\<^isub>1,\,x\<^isub>n}"} & @{text"insert x\<^isub>1 (\ (insert x\<^isub>n {})\)"}\\ +@{term"x ~: A"} & @{term[source]"\(x \ A)"}\\ +@{term"A \ B"} & @{term[source]"A \ B"}\\ +@{term"A \ B"} & @{term[source]"A < B"}\\ +@{term[source]"A \ B"} & @{term[source]"B \ A"}\\ +@{term[source]"A \ B"} & @{term[source]"B < A"}\\ +@{term"{x. P}"} & @{term[source]"Collect(\x. P)"}\\ +@{term"UN x:I. A"} & @{term[source]"UNION I (\x. A)"}\\ +@{term"UN x. A"} & @{term[source]"UNION UNIV (\x. A)"}\\ +@{term"INT x:I. A"} & @{term[source]"INTER I (\x. A)"}\\ +@{term"INT x. A"} & @{term[source]"INTER UNIV (\x. A)"}\\ +@{term"ALL x:A. P"} & @{term[source]"Ball A (\x. P)"}\\ +@{term"EX x:A. P"} & @{term[source]"Bex A (\x. P)"}\\ +@{term"range f"} & @{term[source]"f ` UNIV"}\\ +\end{supertabular} + + +\section{Fun} + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +@{const "Fun.id"} & @{typeof Fun.id}\\ +@{const "Fun.comp"} & @{typeof Fun.comp}\\ +@{const "Fun.inj_on"} & @{term_type_only Fun.inj_on "('a\'b)\'a set\bool"}\\ +@{const "Fun.inj"} & @{typeof Fun.inj}\\ +@{const "Fun.surj"} & @{typeof Fun.surj}\\ +@{const "Fun.bij"} & @{typeof Fun.bij}\\ +@{const "Fun.bij_betw"} & @{term_type_only Fun.bij_betw "('a\'b)\'a set\'b set\bool"}\\ +@{const "Fun.fun_upd"} & @{typeof Fun.fun_upd}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +@{term"fun_upd f x y"} & @{term[source]"fun_upd f x y"}\\ +@{text"f(x\<^isub>1:=y\<^isub>1,\,x\<^isub>n:=y\<^isub>n)"} & @{text"f(x\<^isub>1:=y\<^isub>1)\(x\<^isub>n:=y\<^isub>n)"}\\ +\end{tabular} + + +\section{Fixed Points} + +Theory: @{theory Inductive}. + +Least and greatest fixed points in a complete lattice @{typ 'a}: + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +@{const Inductive.lfp} & @{typeof Inductive.lfp}\\ +@{const Inductive.gfp} & @{typeof Inductive.gfp}\\ +\end{tabular} + +Note that in particular sets (@{typ"'a \ bool"}) are complete lattices. + +\section{Sum\_Type} + +Type constructor @{text"+"}. + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +@{const Sum_Type.Inl} & @{typeof Sum_Type.Inl}\\ +@{const Sum_Type.Inr} & @{typeof Sum_Type.Inr}\\ +@{const Sum_Type.Plus} & @{term_type_only Sum_Type.Plus "'a set\'b set\('a+'b)set"} +\end{tabular} + + +\section{Product\_Type} + +Types @{typ unit} and @{text"\"}. + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +@{const Product_Type.Unity} & @{typeof Product_Type.Unity}\\ +@{const Pair} & @{typeof Pair}\\ +@{const fst} & @{typeof fst}\\ +@{const snd} & @{typeof snd}\\ +@{const split} & @{typeof split}\\ +@{const curry} & @{typeof curry}\\ +@{const Product_Type.Times} & @{typeof Product_Type.Times}\\ +@{const Product_Type.Sigma} & @{term_type_only Product_Type.Sigma "'a set\('a\'b set)\('a*'b)set"}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +@{term"Pair a b"} & @{term[source]"Pair a b"}\\ +@{term"split (\x y. t)"} & @{term[source]"split (\x y. t)"}\\ +\end{tabular} + +Pairs may be nested. Nesting to the right is printed as a tuple, +e.g.\ \mbox{@{term"(a,b,c)"}} is really @{text"(a,(b,c))"}. +Pattern matching with pairs and tuples extends to all binders, +e.g.\ @{prop"ALL (x,y):A. P"}, @{term"{(x,y). P}"}, etc. + + +\section{Relation} + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +@{const Relation.converse} & @{term_type_only Relation.converse "('a * 'b)set \ ('b*'a)set"}\\ +@{const Relation.rel_comp} & @{term_type_only Relation.rel_comp "('a*'b)set\('c*'a)set\('c*'b)set"}\\ +@{const Relation.Image} & @{term_type_only Relation.Image "('a*'b)set\'a set\'b set"}\\ +@{const Relation.inv_image} & @{term_type_only Relation.inv_image "('a*'a)set\('b\'a)\('b*'b)set"}\\ +@{const Relation.Id_on} & @{term_type_only Relation.Id_on "'a set\('a*'a)set"}\\ +@{const Relation.Id} & @{term_type_only Relation.Id "('a*'a)set"}\\ +@{const Relation.Domain} & @{term_type_only Relation.Domain "('a*'b)set\'a set"}\\ +@{const Relation.Range} & @{term_type_only Relation.Range "('a*'b)set\'b set"}\\ +@{const Relation.Field} & @{term_type_only Relation.Field "('a*'a)set\'a set"}\\ +@{const Relation.refl_on} & @{term_type_only Relation.refl_on "'a set\('a*'a)set\bool"}\\ +@{const Relation.refl} & @{term_type_only Relation.refl "('a*'a)set\bool"}\\ +@{const Relation.sym} & @{term_type_only Relation.sym "('a*'a)set\bool"}\\ +@{const Relation.antisym} & @{term_type_only Relation.antisym "('a*'a)set\bool"}\\ +@{const Relation.trans} & @{term_type_only Relation.trans "('a*'a)set\bool"}\\ +@{const Relation.irrefl} & @{term_type_only Relation.irrefl "('a*'a)set\bool"}\\ +@{const Relation.total_on} & @{term_type_only Relation.total_on "'a set\('a*'a)set\bool"}\\ +@{const Relation.total} & @{term_type_only Relation.total "('a*'a)set\bool"}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +@{term"converse r"} & @{term[source]"converse r"} +\end{tabular} + +\section{Equiv\_Relations} + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +@{const Equiv_Relations.equiv} & @{term_type_only Equiv_Relations.equiv "'a set \ ('a*'a)set\bool"}\\ +@{const Equiv_Relations.quotient} & @{term_type_only Equiv_Relations.quotient "'a set \ ('a \ 'a) set \ 'a set set"}\\ +@{const Equiv_Relations.congruent} & @{term_type_only Equiv_Relations.congruent "('a*'a)set\('a\'b)\bool"}\\ +@{const Equiv_Relations.congruent2} & @{term_type_only Equiv_Relations.congruent2 "('a*'a)set\('b*'b)set\('a\'b\'c)\bool"}\\ +%@ {const Equiv_Relations.} & @ {term_type_only Equiv_Relations. ""}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +@{term"congruent r f"} & @{term[source]"congruent r f"}\\ +@{term"congruent2 r r f"} & @{term[source]"congruent2 r r f"}\\ +\end{tabular} + + +\section{Transitive\_Closure} + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +@{const Transitive_Closure.rtrancl} & @{term_type_only Transitive_Closure.rtrancl "('a*'a)set\('a*'a)set"}\\ +@{const Transitive_Closure.trancl} & @{term_type_only Transitive_Closure.trancl "('a*'a)set\('a*'a)set"}\\ +@{const Transitive_Closure.reflcl} & @{term_type_only Transitive_Closure.reflcl "('a*'a)set\('a*'a)set"}\\ +\end{tabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +@{term"rtrancl r"} & @{term[source]"rtrancl r"}\\ +@{term"trancl r"} & @{term[source]"trancl r"}\\ +@{term"reflcl r"} & @{term[source]"reflcl r"} +\end{tabular} + + +\section{Algebra} + +Theories @{theory OrderedGroup} and @{theory Ring_and_Field} define a large +collection of classes describing common algebraic structures from semigroups +up to fields. Everything is done in terms of @{const plus}, @{const times} +and other overloaded operators. + + +\section{Nat} + +@{datatype nat} +\bigskip + +\begin{tabular}{@ {} lllllll @ {}} +@{term "op + :: nat \ nat \ nat"} & +@{term "op - :: nat \ nat \ nat"} & +@{term "op * :: nat \ nat \ nat"} & +@{term "op ^ :: nat \ nat \ nat"} & +@{term "op div :: nat \ nat \ nat"}& +@{term "op mod :: nat \ nat \ nat"}& +@{term "op dvd :: nat \ nat \ bool"}\\ +@{term "op \ :: nat \ nat \ bool"} & +@{term "op < :: nat \ nat \ bool"} & +@{term "min :: nat \ nat \ nat"} & +@{term "max :: nat \ nat \ nat"} & +@{term "Min :: nat set \ nat"} & +@{term "Max :: nat set \ nat"}\\ +\end{tabular} + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +@{const Nat.of_nat} & @{typeof Nat.of_nat} +\end{tabular} + +\section{Int} + +Type @{typ int} +\bigskip + +\begin{tabular}{@ {} llllllll @ {}} +@{term "op + :: int \ int \ int"} & +@{term "op - :: int \ int \ int"} & +@{term "uminus :: int \ int"} & +@{term "op * :: int \ int \ int"} & +@{term "op ^ :: int \ nat \ int"} & +@{term "op div :: int \ int \ int"}& +@{term "op mod :: int \ int \ int"}& +@{term "op dvd :: int \ int \ bool"}\\ +@{term "op \ :: int \ int \ bool"} & +@{term "op < :: int \ int \ bool"} & +@{term "min :: int \ int \ int"} & +@{term "max :: int \ int \ int"} & +@{term "Min :: int set \ int"} & +@{term "Max :: int set \ int"}\\ +@{term "abs :: int \ int"} & +@{term "sgn :: int \ int"}\\ +\end{tabular} + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +@{const Int.nat} & @{typeof Int.nat}\\ +@{const Int.of_int} & @{typeof Int.of_int}\\ +@{const Int.Ints} & @{term_type_only Int.Ints "'a::ring_1 set"}\\ +\end{tabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +@{term"of_nat::nat\int"} & @{term[source]"of_nat"}\\ +\end{tabular} + + +\section{Wellfounded} + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +@{const Wellfounded.wf} & @{term_type_only Wellfounded.wf "('a*'a)set\bool"}\\ +@{const Wellfounded.acyclic} & @{term_type_only Wellfounded.acyclic "('a*'a)set\bool"}\\ +@{const Wellfounded.acc} & @{term_type_only Wellfounded.acc "('a*'a)set\'a set"}\\ +@{const Wellfounded.measure} & @{term_type_only Wellfounded.measure "('a\nat)\('a*'a)set"}\\ +@{const Wellfounded.lex_prod} & @{term_type_only Wellfounded.lex_prod "('a*'a)set\('b*'b)set\(('a*'b)*('a*'b))set"}\\ +@{const Wellfounded.mlex_prod} & @{term_type_only Wellfounded.mlex_prod "('a\nat)\('a*'a)set\('a*'a)set"}\\ +@{const Wellfounded.less_than} & @{term_type_only Wellfounded.less_than "(nat*nat)set"}\\ +@{const Wellfounded.pred_nat} & @{term_type_only Wellfounded.pred_nat "(nat*nat)set"}\\ +\end{supertabular} + + +\section{Power} + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +@{const Power.power} & @{typeof Power.power} +\end{tabular} + + +\section{Iterated Functions and Relations} + +Theory: @{theory Relation_Power} + +Iterated functions \ @{term[source]"(f::'a\'a) ^ n"} \ +and relations \ @{term[source]"(r::('a\'a)set) ^ n"}. + + +\section{Option} + +@{datatype option} +\bigskip + +\begin{tabular}{@ {} l @ {~::~} l @ {}} +@{const Option.the} & @{typeof Option.the}\\ +@{const Option.map} & @{typ[source]"('a \ 'b) \ 'a option \ 'b option"}\\ +@{const Option.set} & @{term_type_only Option.set "'a option \ 'a set"} +\end{tabular} + +\section{List} + +@{datatype list} +\bigskip + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +@{const List.append} & @{typeof List.append}\\ +@{const List.butlast} & @{typeof List.butlast}\\ +@{const List.concat} & @{typeof List.concat}\\ +@{const List.distinct} & @{typeof List.distinct}\\ +@{const List.drop} & @{typeof List.drop}\\ +@{const List.dropWhile} & @{typeof List.dropWhile}\\ +@{const List.filter} & @{typeof List.filter}\\ +@{const List.foldl} & @{typeof List.foldl}\\ +@{const List.foldr} & @{typeof List.foldr}\\ +@{const List.hd} & @{typeof List.hd}\\ +@{const List.last} & @{typeof List.last}\\ +@{const List.length} & @{typeof List.length}\\ +@{const List.lenlex} & @{term_type_only List.lenlex "('a*'a)set\('a list * 'a list)set"}\\ +@{const List.lex} & @{term_type_only List.lex "('a*'a)set\('a list * 'a list)set"}\\ +@{const List.lexn} & @{term_type_only List.lexn "('a*'a)set\nat\('a list * 'a list)set"}\\ +@{const List.lexord} & @{term_type_only List.lexord "('a*'a)set\('a list * 'a list)set"}\\ +@{const List.listrel} & @{term_type_only List.listrel "('a*'a)set\('a list * 'a list)set"}\\ +@{const List.lists} & @{term_type_only List.lists "'a set\'a list set"}\\ +@{const List.listset} & @{term_type_only List.listset "'a set list \ 'a list set"}\\ +@{const List.listsum} & @{typeof List.listsum}\\ +@{const List.list_all2} & @{typeof List.list_all2}\\ +@{const List.list_update} & @{typeof List.list_update}\\ +@{const List.map} & @{typeof List.map}\\ +@{const List.measures} & @{term_type_only List.measures "('a\nat)list\('a*'a)set"}\\ +@{const List.remdups} & @{typeof List.remdups}\\ +@{const List.removeAll} & @{typeof List.removeAll}\\ +@{const List.remove1} & @{typeof List.remove1}\\ +@{const List.replicate} & @{typeof List.replicate}\\ +@{const List.rev} & @{typeof List.rev}\\ +@{const List.rotate} & @{typeof List.rotate}\\ +@{const List.rotate1} & @{typeof List.rotate1}\\ +@{const List.set} & @{term_type_only List.set "'a list \ 'a set"}\\ +@{const List.sort} & @{typeof List.sort}\\ +@{const List.sorted} & @{typeof List.sorted}\\ +@{const List.splice} & @{typeof List.splice}\\ +@{const List.sublist} & @{typeof List.sublist}\\ +@{const List.take} & @{typeof List.take}\\ +@{const List.takeWhile} & @{typeof List.takeWhile}\\ +@{const List.tl} & @{typeof List.tl}\\ +@{const List.upt} & @{typeof List.upt}\\ +@{const List.upto} & @{typeof List.upto}\\ +@{const List.zip} & @{typeof List.zip}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +@{text"[x\<^isub>1,\,x\<^isub>n]"} & @{text"x\<^isub>1 # \ # x\<^isub>n # []"}\\ +@{term"[m.. xs]"} & @{term"map (%x. e) xs"}\\ +@{term"[x \ xs. b]"} & @{term[source]"filter (\x. b) xs"} \\ +@{term"xs[n := x]"} & @{term[source]"list_update xs n x"}\\ +@{term"\x\xs. e"} & @{term[source]"listsum (map (\x. e) xs)"}\\ +\end{supertabular} +\medskip + +Comprehension: @{text"[e. q\<^isub>1, \, q\<^isub>n]"} where each +qualifier @{text q\<^isub>i} is either a generator @{text"pat \ e"} or a +guard, i.e.\ boolean expression. + +\section{Map} + +Maps model partial functions and are often used as finite tables. However, +the domain of a map may be infinite. + +@{text"'a \ 'b = 'a \ 'b option"} +\bigskip + +\begin{supertabular}{@ {} l @ {~::~} l @ {}} +@{const Map.empty} & @{typeof Map.empty}\\ +@{const Map.map_add} & @{typeof Map.map_add}\\ +@{const Map.map_comp} & @{typeof Map.map_comp}\\ +@{const Map.restrict_map} & @{term_type_only Map.restrict_map "('a\'b option)\'a set\('a\'b option)"}\\ +@{const Map.dom} & @{term_type_only Map.dom "('a\'b option)\'a set"}\\ +@{const Map.ran} & @{term_type_only Map.ran "('a\'b option)\'b set"}\\ +@{const Map.map_le} & @{typeof Map.map_le}\\ +@{const Map.map_of} & @{typeof Map.map_of}\\ +@{const Map.map_upds} & @{typeof Map.map_upds}\\ +\end{supertabular} + +\subsubsection*{Syntax} + +\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}} +@{text"empty"} & @{term"\x. None"}\\ +@{term"m(x:=Some y)"} & @{term[source]"m(x:=Some y)"}\\ +@{text"m(x\<^isub>1\y\<^isub>1,\,x\<^isub>n\y\<^isub>n)"} & @{text[source]"m(x\<^isub>1\y\<^isub>1)\(x\<^isub>n\y\<^isub>n)"}\\ +@{term"map_upds m xs ys"} & @{term[source]"map_upds m xs ys"}\\ +\end{tabular} + +*} +(*<*) +end +(*>*) \ No newline at end of file diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Docs/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Docs/ROOT.ML Fri Mar 06 11:10:57 2009 +0100 @@ -0,0 +1,2 @@ +use_thy "MainDoc"; + diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Docs/document/root.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Docs/document/root.tex Fri Mar 06 11:10:57 2009 +0100 @@ -0,0 +1,65 @@ +\documentclass[11pt,a4paper]{article} +\usepackage{isabelle,isabellesym} + +% further packages required for unusual symbols (see also +% isabellesym.sty), use only when needed + +%\usepackage{amssymb} + %for \, \, \, \, \, \, + %\, \, \, \, \, + %\, \, \ + +%\usepackage[greek,english]{babel} + %option greek for \ + %option english (default language) for \, \ + +%\usepackage[latin1]{inputenc} + %for \, \, \, \, + %\, \, \ + +%\usepackage[only,bigsqcap]{stmaryrd} + %for \ + +%\usepackage{eufrak} + %for \ ... \, \ ... \ (also included in amssymb) + +%\usepackage{textcomp} + %for \, \ + +% this should be the last package used +\usepackage{pdfsetup} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + +% for uniform font size +\renewcommand{\isastyle}{\isastyleminor} + +\parindent 0pt\parskip 0.5ex + +\usepackage{supertabular} + +\begin{document} + +\title{What's in Main} +\author{} +\date{} +\maketitle + +%\setcounter{tocdepth}{1} +%\tableofcontents + +% generated text of all theories +\input{session} + +% optional bibliography +%\bibliographystyle{abbrv} +%\bibliography{root} + +\end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Nominal/nominal_fresh_fun.ML --- a/src/HOL/Nominal/nominal_fresh_fun.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Fri Mar 06 11:10:57 2009 +0100 @@ -72,7 +72,7 @@ let val thy = theory_of_thm thm; (* the parsing function returns a qualified name, we get back the base name *) - val atom_basename = Sign.base_name atom_name; + val atom_basename = NameSpace.base_name atom_name; val goal = List.nth(prems_of thm, i-1); val ps = Logic.strip_params goal; val Ts = rev (map snd ps); @@ -159,7 +159,7 @@ NONE => all_tac thm | SOME atom_name => let - val atom_basename = Sign.base_name atom_name; + val atom_basename = NameSpace.base_name atom_name; val pt_name_inst = get_dyn_thm thy ("pt_"^atom_basename^"_inst") atom_basename; val at_name_inst = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename; fun inst_fresh vars params i st = diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Nominal/nominal_inductive.ML Fri Mar 06 11:10:57 2009 +0100 @@ -199,7 +199,7 @@ val atomTs = distinct op = (maps (map snd o #2) prems); val ind_sort = if null atomTs then HOLogic.typeS else Sign.certify_sort thy (map (fn T => Sign.intern_class thy - ("fs_" ^ Sign.base_name (fst (dest_Type T)))) atomTs); + ("fs_" ^ NameSpace.base_name (fst (dest_Type T)))) atomTs); val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt'); val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt'; val fsT = TFree (fs_ctxt_tyname, ind_sort); @@ -273,7 +273,7 @@ val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp"; val pt2_atoms = map (fn aT => PureThy.get_thm thy - ("pt_" ^ Sign.base_name (fst (dest_Type aT)) ^ "2")) atomTs; + ("pt_" ^ NameSpace.base_name (fst (dest_Type aT)) ^ "2")) atomTs; val eqvt_ss = Simplifier.theory_context thy HOL_basic_ss addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms) addsimprocs [mk_perm_bool_simproc ["Fun.id"], @@ -281,7 +281,7 @@ val fresh_bij = PureThy.get_thms thy "fresh_bij"; val perm_bij = PureThy.get_thms thy "perm_bij"; val fs_atoms = map (fn aT => PureThy.get_thm thy - ("fs_" ^ Sign.base_name (fst (dest_Type aT)) ^ "1")) atomTs; + ("fs_" ^ NameSpace.base_name (fst (dest_Type aT)) ^ "1")) atomTs; val exists_fresh' = PureThy.get_thms thy "exists_fresh'"; val fresh_atm = PureThy.get_thms thy "fresh_atm"; val swap_simps = PureThy.get_thms thy "swap_simps"; @@ -545,7 +545,7 @@ ctxt'' |> Proof.theorem_i NONE (fn thss => fn ctxt => let - val rec_name = space_implode "_" (map Sign.base_name names); + val rec_name = space_implode "_" (map NameSpace.base_name names); val rec_qualified = Binding.qualify false rec_name; val ind_case_names = RuleCases.case_names induct_cases; val induct_cases' = InductivePackage.partition_rules' raw_induct @@ -575,7 +575,7 @@ Attrib.internal (K (RuleCases.consumes 1))]), strong_inducts) |> snd |> LocalTheory.notes Thm.theoremK (map (fn ((name, elim), (_, cases)) => - ((Binding.name (NameSpace.qualified (Sign.base_name name) "strong_cases"), + ((Binding.name (NameSpace.qualified (NameSpace.base_name name) "strong_cases"), [Attrib.internal (K (RuleCases.case_names (map snd cases))), Attrib.internal (K (RuleCases.consumes 1))]), [([elim], [])])) (strong_cases ~~ induct_cases')) |> snd @@ -665,7 +665,7 @@ in ctxt |> LocalTheory.notes Thm.theoremK (map (fn (name, ths) => - ((Binding.name (NameSpace.qualified (Sign.base_name name) "eqvt"), + ((Binding.name (NameSpace.qualified (NameSpace.base_name name) "eqvt"), [Attrib.internal (K NominalThmDecls.eqvt_add)]), [(ths, [])])) (names ~~ transp thss)) |> snd end; diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Nominal/nominal_inductive2.ML Fri Mar 06 11:10:57 2009 +0100 @@ -229,7 +229,7 @@ val atoms = map (fst o dest_Type) atomTs; val ind_sort = if null atomTs then HOLogic.typeS else Sign.certify_sort thy (map (fn a => Sign.intern_class thy - ("fs_" ^ Sign.base_name a)) atoms); + ("fs_" ^ NameSpace.base_name a)) atoms); val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt'); val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt'; val fsT = TFree (fs_ctxt_tyname, ind_sort); @@ -296,7 +296,7 @@ val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp"; val pt2_atoms = map (fn a => PureThy.get_thm thy - ("pt_" ^ Sign.base_name a ^ "2")) atoms; + ("pt_" ^ NameSpace.base_name a ^ "2")) atoms; val eqvt_ss = Simplifier.theory_context thy HOL_basic_ss addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms) addsimprocs [mk_perm_bool_simproc ["Fun.id"], @@ -324,7 +324,7 @@ val atom = fst (dest_Type T); val {at_inst, ...} = NominalAtoms.the_atom_info thy atom; val fs_atom = PureThy.get_thm thy - ("fs_" ^ Sign.base_name atom ^ "1"); + ("fs_" ^ NameSpace.base_name atom ^ "1"); val avoid_th = Drule.instantiate' [SOME (ctyp_of thy (fastype_of p))] [SOME (cterm_of thy p)] ([at_inst, fin, fs_atom] MRS @{thm at_set_avoiding}); @@ -452,7 +452,7 @@ ctxt'' |> Proof.theorem_i NONE (fn thss => fn ctxt => let - val rec_name = space_implode "_" (map Sign.base_name names); + val rec_name = space_implode "_" (map NameSpace.base_name names); val rec_qualified = Binding.qualify false rec_name; val ind_case_names = RuleCases.case_names induct_cases; val induct_cases' = InductivePackage.partition_rules' raw_induct diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Nominal/nominal_package.ML Fri Mar 06 11:10:57 2009 +0100 @@ -49,9 +49,9 @@ fun dt_cases (descr: descr) (_, args, constrs) = let - fun the_bname i = Sign.base_name (#1 (valOf (AList.lookup (op =) descr i))); + fun the_bname i = NameSpace.base_name (#1 (valOf (AList.lookup (op =) descr i))); val bnames = map the_bname (distinct op = (List.concat (map dt_recs args))); - in map (fn (c, _) => space_implode "_" (Sign.base_name c :: bnames)) constrs end; + in map (fn (c, _) => space_implode "_" (NameSpace.base_name c :: bnames)) constrs end; fun induct_cases descr = @@ -364,7 +364,7 @@ val pi2 = Free ("pi2", permT); val pt_inst = pt_inst_of thy2 a; val pt2' = pt_inst RS pt2; - val pt2_ax = PureThy.get_thm thy2 (NameSpace.map_base (fn s => "pt_" ^ s ^ "2") a); + val pt2_ax = PureThy.get_thm thy2 (NameSpace.map_base_name (fn s => "pt_" ^ s ^ "2") a); in List.take (map standard (split_conj_thm (Goal.prove_global thy2 [] [] (augment_sort thy2 [pt_class_of thy2 a] @@ -399,7 +399,7 @@ val pt_inst = pt_inst_of thy2 a; val pt3' = pt_inst RS pt3; val pt3_rev' = at_inst RS (pt_inst RS pt3_rev); - val pt3_ax = PureThy.get_thm thy2 (NameSpace.map_base (fn s => "pt_" ^ s ^ "3") a); + val pt3_ax = PureThy.get_thm thy2 (NameSpace.map_base_name (fn s => "pt_" ^ s ^ "3") a); in List.take (map standard (split_conj_thm (Goal.prove_global thy2 [] [] (augment_sort thy2 [pt_class_of thy2 a] (Logic.mk_implies @@ -664,7 +664,7 @@ asm_full_simp_tac (simpset_of thy addsimps [Rep RS perm_closed RS Abs_inverse]) 1, asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy - ("pt_" ^ Sign.base_name atom ^ "3")]) 1]) thy + ("pt_" ^ NameSpace.base_name atom ^ "3")]) 1]) thy end) (Abs_inverse_thms ~~ Rep_inverse_thms ~~ Rep_thms ~~ perm_defs ~~ new_type_names ~~ tyvars ~~ perm_closed_thms); @@ -798,7 +798,7 @@ val def = Logic.mk_equals (lhs, Const (abs_name, T' --> T) $ rhs); val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (rep_name, T --> T') $ lhs, rhs)); - val def_name = (Sign.base_name cname) ^ "_def"; + val def_name = (NameSpace.base_name cname) ^ "_def"; val ([def_thm], thy') = thy |> Sign.add_consts_i [(cname', constrT, mx)] |> (PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)] @@ -889,7 +889,7 @@ map (fn ((cname, dts), constr_rep_thm) => let val cname = Sign.intern_const thy8 - (NameSpace.append tname (Sign.base_name cname)); + (NameSpace.append tname (NameSpace.base_name cname)); val permT = mk_permT (Type (atom, [])); val pi = Free ("pi", permT); @@ -945,7 +945,7 @@ if null dts then NONE else SOME let val cname = Sign.intern_const thy8 - (NameSpace.append tname (Sign.base_name cname)); + (NameSpace.append tname (NameSpace.base_name cname)); fun make_inj ((dts, dt), (j, args1, args2, eqs)) = let @@ -987,7 +987,7 @@ in List.concat (map (fn (cname, dts) => map (fn atom => let val cname = Sign.intern_const thy8 - (NameSpace.append tname (Sign.base_name cname)); + (NameSpace.append tname (NameSpace.base_name cname)); val atomT = Type (atom, []); fun process_constr ((dts, dt), (j, args1, args2)) = @@ -1100,7 +1100,7 @@ (fn _ => indtac dt_induct indnames 1 THEN ALLGOALS (asm_full_simp_tac (simpset_of thy8 addsimps (abs_supp @ supp_atm @ - PureThy.get_thms thy8 ("fs_" ^ Sign.base_name atom ^ "1") @ + PureThy.get_thms thy8 ("fs_" ^ NameSpace.base_name atom ^ "1") @ List.concat supp_thms))))), length new_type_names)) end) atoms; @@ -1232,9 +1232,9 @@ val fin_set_fresh = map (fn s => at_inst_of thy9 s RS at_fin_set_fresh) dt_atoms; val pt1_atoms = map (fn Type (s, _) => - PureThy.get_thm thy9 ("pt_" ^ Sign.base_name s ^ "1")) dt_atomTs; + PureThy.get_thm thy9 ("pt_" ^ NameSpace.base_name s ^ "1")) dt_atomTs; val pt2_atoms = map (fn Type (s, _) => - PureThy.get_thm thy9 ("pt_" ^ Sign.base_name s ^ "2") RS sym) dt_atomTs; + PureThy.get_thm thy9 ("pt_" ^ NameSpace.base_name s ^ "2") RS sym) dt_atomTs; val exists_fresh' = PureThy.get_thms thy9 "exists_fresh'"; val fs_atoms = PureThy.get_thms thy9 "fin_supp"; val abs_supp = PureThy.get_thms thy9 "abs_supp"; @@ -1559,7 +1559,7 @@ val rec_fin_supp_thms = map (fn aT => let - val name = Sign.base_name (fst (dest_Type aT)); + val name = NameSpace.base_name (fst (dest_Type aT)); val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1"); val aset = HOLogic.mk_setT aT; val finite = Const ("Finite_Set.finite", aset --> HOLogic.boolT); @@ -1598,7 +1598,7 @@ val rec_fresh_thms = map (fn ((aT, eqvt_ths), finite_prems) => let - val name = Sign.base_name (fst (dest_Type aT)); + val name = NameSpace.base_name (fst (dest_Type aT)); val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1"); val a = Free ("a", aT); val freshs = map (fn (f, fT) => HOLogic.mk_Trueprop @@ -2012,10 +2012,10 @@ val (reccomb_defs, thy12) = thy11 |> Sign.add_consts_i (map (fn ((name, T), T') => - (Sign.base_name name, rec_fn_Ts @ [T] ---> T', NoSyn)) + (NameSpace.base_name name, rec_fn_Ts @ [T] ---> T', NoSyn)) (reccomb_names ~~ recTs ~~ rec_result_Ts)) |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') => - (Binding.name (Sign.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T, + (Binding.name (NameSpace.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T, Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T', set $ Free ("x", T) $ Free ("y", T')))))) (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)); diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Nominal/nominal_permeq.ML --- a/src/HOL/Nominal/nominal_permeq.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Nominal/nominal_permeq.ML Fri Mar 06 11:10:57 2009 +0100 @@ -110,7 +110,7 @@ Type("fun",[Type("List.list",[Type("*",[Type(n,_),_])]),_])) $ pi $ (f $ x)) => (if (applicable_app f) then let - val name = Sign.base_name n + val name = NameSpace.base_name n val at_inst = PureThy.get_thm sg ("at_" ^ name ^ "_inst") val pt_inst = PureThy.get_thm sg ("pt_" ^ name ^ "_inst") in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end @@ -198,8 +198,8 @@ Type ("fun", [Type ("List.list", [Type ("*", [U as Type (uname,_),_])]),_])) $ pi2 $ t)) => let - val tname' = Sign.base_name tname - val uname' = Sign.base_name uname + val tname' = NameSpace.base_name tname + val uname' = NameSpace.base_name uname in if pi1 <> pi2 then (* only apply the composition rule in this case *) if T = U then diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Nominal/nominal_primrec.ML --- a/src/HOL/Nominal/nominal_primrec.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Nominal/nominal_primrec.ML Fri Mar 06 11:10:57 2009 +0100 @@ -207,7 +207,7 @@ val frees = ls @ x :: rs; val raw_rhs = list_abs_free (frees, list_comb (Const (rec_name, dummyT), fs @ [Free x])) - val def_name = Thm.def_name (Sign.base_name fname); + val def_name = Thm.def_name (NameSpace.base_name fname); val rhs = singleton (Syntax.check_terms ctxt) raw_rhs; val SOME var = get_first (fn ((b, _), mx) => if Binding.name_of b = fname then SOME (b, mx) else NONE) fixes; @@ -286,7 +286,7 @@ fold_map (apfst (snd o snd) oo LocalTheory.define Thm.definitionK o fst) defs'; val qualify = Binding.qualify false - (space_implode "_" (map (Sign.base_name o #1) defs)); + (space_implode "_" (map (NameSpace.base_name o #1) defs)); val names_atts' = map (apfst qualify) names_atts; val cert = cterm_of (ProofContext.theory_of lthy'); diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Nominal/nominal_thmdecls.ML --- a/src/HOL/Nominal/nominal_thmdecls.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Fri Mar 06 11:10:57 2009 +0100 @@ -115,7 +115,7 @@ (Var (n,ty))) => let (* FIXME: this should be an operation the library *) - val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm) + val class_name = (NameSpace.map_base_name (fn s => "pt_"^s) tyatm) in if (Sign.of_sort thy (ty,[class_name])) then [(pi,typi)] diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/SizeChange/Graphs.thy --- a/src/HOL/SizeChange/Graphs.thy Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/SizeChange/Graphs.thy Fri Mar 06 11:10:57 2009 +0100 @@ -351,7 +351,7 @@ lemma in_tcl: "has_edge (tcl G) a x b = (\n>0. has_edge (G ^ n) a x b)" - apply (auto simp: tcl_is_SUP in_SUP simp del: power_graph.simps) + apply (auto simp: tcl_is_SUP in_SUP simp del: power_graph.simps power_Suc) apply (rule_tac x = "n - 1" in exI, auto) done diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Statespace/distinct_tree_prover.ML --- a/src/HOL/Statespace/distinct_tree_prover.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Statespace/distinct_tree_prover.ML Fri Mar 06 11:10:57 2009 +0100 @@ -352,14 +352,14 @@ | distinctTree_tac _ _ _ = no_tac; fun distinctFieldSolver names = mk_solver' "distinctFieldSolver" - (fn ss => case #context (#1 (rep_ss ss)) of + (fn ss => case try Simplifier.the_context ss of SOME ctxt => SUBGOAL (distinctTree_tac names ctxt) | NONE => fn i => no_tac) fun distinct_simproc names = Simplifier.simproc @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"] (fn thy => fn ss => fn (Const ("op =",_)$x$y) => - case #context (#1 (rep_ss ss)) of + case try Simplifier.the_context ss of SOME ctxt => Option.map (fn neq => neq_to_eq_False OF [neq]) (get_fst_success (neq_x_y ctxt x y) names) | NONE => NONE diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Statespace/state_fun.ML --- a/src/HOL/Statespace/state_fun.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Statespace/state_fun.ML Fri Mar 06 11:10:57 2009 +0100 @@ -146,7 +146,7 @@ val ct = cterm_of thy (Const ("StateFun.lookup",lT)$destr$n$(fst (mk_upds s))); - val ctxt = the (#context (#1 (rep_ss ss))); + val ctxt = Simplifier.the_context ss; val basic_ss = #1 (StateFunData.get (Context.Proof ctxt)); val ss' = Simplifier.context (Config.map MetaSimplifier.simp_depth_limit (K 100) ctxt) basic_ss; @@ -241,7 +241,7 @@ end | mk_updterm _ t = init_seed t; - val ctxt = the (#context (#1 (rep_ss ss))) |> + val ctxt = Simplifier.the_context ss |> Config.map MetaSimplifier.simp_depth_limit (K 100); val ss1 = Simplifier.context ctxt ss'; val ss2 = Simplifier.context ctxt @@ -336,17 +336,17 @@ [] => "" | c::cs => String.implode (Char.toUpper c::cs )) -fun mkName (Type (T,args)) = concat (map mkName args) ^ mkUpper (NameSpace.base T) - | mkName (TFree (x,_)) = mkUpper (NameSpace.base x) - | mkName (TVar ((x,_),_)) = mkUpper (NameSpace.base x); +fun mkName (Type (T,args)) = concat (map mkName args) ^ mkUpper (NameSpace.base_name T) + | mkName (TFree (x,_)) = mkUpper (NameSpace.base_name x) + | mkName (TVar ((x,_),_)) = mkUpper (NameSpace.base_name x); fun is_datatype thy n = is_some (Symtab.lookup (DatatypePackage.get_datatypes thy) n); -fun mk_map ("List.list") = Syntax.const "List.map" - | mk_map n = Syntax.const ("StateFun." ^ "map_" ^ NameSpace.base n); +fun mk_map "List.list" = Syntax.const "List.map" + | mk_map n = Syntax.const ("StateFun.map_" ^ NameSpace.base_name n); fun gen_constr_destr comp prfx thy (Type (T,[])) = - Syntax.const (deco prfx (mkUpper (NameSpace.base T))) + Syntax.const (deco prfx (mkUpper (NameSpace.base_name T))) | gen_constr_destr comp prfx thy (T as Type ("fun",_)) = let val (argTs,rangeT) = strip_type T; in comp @@ -360,11 +360,11 @@ then (* datatype args are recursively embedded into val *) (case argTs of [argT] => comp - ((Syntax.const (deco prfx (mkUpper (NameSpace.base T))))) + ((Syntax.const (deco prfx (mkUpper (NameSpace.base_name T))))) ((mk_map T $ gen_constr_destr comp prfx thy argT)) | _ => raise (TYPE ("StateFun.gen_constr_destr",[T'],[]))) else (* type args are not recursively embedded into val *) - Syntax.const (deco prfx (concat (map mkName argTs) ^ mkUpper (NameSpace.base T))) + Syntax.const (deco prfx (concat (map mkName argTs) ^ mkUpper (NameSpace.base_name T))) | gen_constr_destr thy _ _ T = raise (TYPE ("StateFun.gen_constr_destr",[T],[])); val mk_constr = gen_constr_destr (fn a => fn b => Syntax.const "Fun.comp" $ a $ b) "" diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Statespace/state_space.ML Fri Mar 06 11:10:57 2009 +0100 @@ -236,14 +236,14 @@ | distinctTree_tac _ _ = no_tac; val distinctNameSolver = mk_solver' "distinctNameSolver" - (fn ss => case #context (#1 (rep_ss ss)) of + (fn ss => case try Simplifier.the_context ss of SOME ctxt => SUBGOAL (distinctTree_tac ctxt) | NONE => fn i => no_tac) val distinct_simproc = Simplifier.simproc @{theory HOL} "StateSpace.distinct_simproc" ["x = y"] (fn thy => fn ss => (fn (Const ("op =",_)$(x as Free _)$(y as Free _)) => - (case #context (#1 (rep_ss ss)) of + (case try Simplifier.the_context ss of SOME ctxt => Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq]) (neq_x_y ctxt x y) | NONE => NONE) @@ -645,7 +645,7 @@ fun update_tr ctxt [s,Free (n,_),v] = gen_update_tr false ctxt n v s; fun update_tr' ctxt [_$Free (prj,_),_$Free (inj,_),n as (_$Free (name,_)),(Const (k,_)$v),s] = - if NameSpace.base k = NameSpace.base KN then + if NameSpace.base_name k = NameSpace.base_name KN then (case get_comp (Context.Proof ctxt) name of SOME (T,_) => if inj=inject_name T andalso prj=project_name T then Syntax.const "_statespace_update" $ s $ n $ v diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Tools/TFL/post.ML --- a/src/HOL/Tools/TFL/post.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Tools/TFL/post.ML Fri Mar 06 11:10:57 2009 +0100 @@ -223,7 +223,7 @@ *---------------------------------------------------------------------------*) fun define_i strict thy cs ss congs wfs fid R eqs = let val {functional,pats} = Prim.mk_functional thy eqs - val (thy, def) = Prim.wfrec_definition0 thy (Sign.base_name fid) R functional + val (thy, def) = Prim.wfrec_definition0 thy (NameSpace.base_name fid) R functional val {induct, rules, tcs} = simplify_defn strict thy cs ss congs wfs fid pats def val rules' = @@ -248,7 +248,7 @@ fun defer_i thy congs fid eqs = let val {rules,R,theory,full_pats_TCs,SV,...} = - Prim.lazyR_def thy (Sign.base_name fid) congs eqs + Prim.lazyR_def thy (NameSpace.base_name fid) congs eqs val f = func_of_cond_eqn (concl (R.CONJUNCT1 rules handle U.ERR _ => rules)); val dummy = writeln "Proving induction theorem ..."; val induction = Prim.mk_induction theory diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Tools/TFL/tfl.ML Fri Mar 06 11:10:57 2009 +0100 @@ -349,7 +349,7 @@ | L => mk_functional_err ("The following clauses are redundant (covered by preceding clauses): " ^ commas (map (fn i => Int.toString (i + 1)) L)) - in {functional = Abs(Sign.base_name fname, ftype, + in {functional = Abs(NameSpace.base_name fname, ftype, abstract_over (atom, absfree(aname,atype, case_tm))), pats = patts2} diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Tools/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_abs_proofs.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Fri Mar 06 11:10:57 2009 +0100 @@ -235,10 +235,10 @@ val (reccomb_defs, thy2) = thy1 |> Sign.add_consts_i (map (fn ((name, T), T') => - (Sign.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn)) + (NameSpace.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn)) (reccomb_names ~~ recTs ~~ rec_result_Ts)) |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') => - (Binding.name (Sign.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T, + (Binding.name (NameSpace.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T, Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T', set $ Free ("x", T) $ Free ("y", T')))))) (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)) @@ -316,8 +316,8 @@ val fns = (List.concat (Library.take (i, case_dummy_fns))) @ fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns))); val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T'); - val decl = ((Binding.name (Sign.base_name name), caseT), NoSyn); - val def = (Binding.name (Sign.base_name name ^ "_def"), + val decl = ((Binding.name (NameSpace.base_name name), caseT), NoSyn); + val def = (Binding.name (NameSpace.base_name name ^ "_def"), Logic.mk_equals (list_comb (Const (name, caseT), fns1), list_comb (reccomb, (List.concat (Library.take (i, case_dummy_fns))) @ fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns))) ))); diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Tools/datatype_aux.ML --- a/src/HOL/Tools/datatype_aux.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Tools/datatype_aux.ML Fri Mar 06 11:10:57 2009 +0100 @@ -224,7 +224,7 @@ | mk_fun_dtyp (T :: Ts) U = DtType ("fun", [T, mk_fun_dtyp Ts U]); fun name_of_typ (Type (s, Ts)) = - let val s' = Sign.base_name s + let val s' = NameSpace.base_name s in space_implode "_" (List.filter (not o equal "") (map name_of_typ Ts) @ [if Syntax.is_identifier s' then s' else "x"]) end diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Tools/datatype_package.ML Fri Mar 06 11:10:57 2009 +0100 @@ -174,9 +174,9 @@ fun dt_cases (descr: descr) (_, args, constrs) = let - fun the_bname i = Sign.base_name (#1 (the (AList.lookup (op =) descr i))); + fun the_bname i = NameSpace.base_name (#1 (the (AList.lookup (op =) descr i))); val bnames = map the_bname (distinct (op =) (maps dt_recs args)); - in map (fn (c, _) => space_implode "_" (Sign.base_name c :: bnames)) constrs end; + in map (fn (c, _) => space_implode "_" (NameSpace.base_name c :: bnames)) constrs end; fun induct_cases descr = @@ -519,7 +519,7 @@ val cs = map (apsnd (map norm_constr)) raw_cs; val dtyps_of_typ = map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs)) o fst o strip_type; - val new_type_names = map NameSpace.base (the_default (map fst cs) alt_names); + val new_type_names = map NameSpace.base_name (the_default (map fst cs) alt_names); fun mk_spec (i, (tyco, constr)) = (i, (tyco, map (DtTFree o fst) vs, diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Tools/datatype_prop.ML --- a/src/HOL/Tools/datatype_prop.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Tools/datatype_prop.ML Fri Mar 06 11:10:57 2009 +0100 @@ -47,7 +47,7 @@ let fun type_name (TFree (name, _)) = implode (tl (explode name)) | type_name (Type (name, _)) = - let val name' = Sign.base_name name + let val name' = NameSpace.base_name name in if Syntax.is_identifier name' then name' else "x" end; in indexify_names (map type_name Ts) end; diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Tools/datatype_realizer.ML --- a/src/HOL/Tools/datatype_realizer.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Tools/datatype_realizer.ML Fri Mar 06 11:10:57 2009 +0100 @@ -168,7 +168,7 @@ val Ts = map (typ_of_dtyp descr sorts) cargs; val frees = Name.variant_list ["P", "y"] (DatatypeProp.make_tnames Ts) ~~ Ts; val free_ts = map Free frees; - val r = Free ("r" ^ NameSpace.base cname, Ts ---> rT) + val r = Free ("r" ^ NameSpace.base_name cname, Ts ---> rT) in (r, list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))), HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Tools/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_rep_proofs.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Fri Mar 06 11:10:57 2009 +0100 @@ -236,7 +236,7 @@ val lhs = list_comb (Const (cname, constrT), l_args); val rhs = mk_univ_inj r_args n i; val def = Logic.mk_equals (lhs, Const (abs_name, Univ_elT --> T) $ rhs); - val def_name = Sign.base_name cname ^ "_def"; + val def_name = NameSpace.base_name cname ^ "_def"; val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (rep_name, T --> Univ_elT) $ lhs, rhs)); val ([def_thm], thy') = @@ -343,7 +343,7 @@ val (fs, eqns, isos) = Library.foldl process_dt (([], [], []), ds); val fTs = map fastype_of fs; - val defs = map (fn (rec_name, (T, iso_name)) => (Binding.name (Sign.base_name iso_name ^ "_def"), + val defs = map (fn (rec_name, (T, iso_name)) => (Binding.name (NameSpace.base_name iso_name ^ "_def"), Logic.mk_equals (Const (iso_name, T --> Univ_elT), list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs)))) (rec_names ~~ isos); val (def_thms, thy') = diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Tools/function_package/size.ML --- a/src/HOL/Tools/function_package/size.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Tools/function_package/size.ML Fri Mar 06 11:10:57 2009 +0100 @@ -87,7 +87,7 @@ recTs1 ~~ alt_names' |> map (fn (T as Type (s, _), optname) => let - val s' = the_default (Sign.base_name s) optname ^ "_size"; + val s' = the_default (NameSpace.base_name s) optname ^ "_size"; val s'' = Sign.full_bname thy s' in (s'', @@ -140,7 +140,7 @@ val ((size_def_thms, size_def_thms'), thy') = thy |> Sign.add_consts_i (map (fn (s, T) => - (Sign.base_name s, param_size_fTs @ [T] ---> HOLogic.natT, NoSyn)) + (NameSpace.base_name s, param_size_fTs @ [T] ---> HOLogic.natT, NoSyn)) (size_names ~~ recTs1)) |> PureThy.add_defs false (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs))) @@ -221,8 +221,8 @@ fun add_size_thms (new_type_names as name :: _) thy = let val info as {descr, alt_names, ...} = DatatypePackage.the_datatype thy name; - val prefix = NameSpace.map_base (K (space_implode "_" - (the_default (map Sign.base_name new_type_names) alt_names))) name; + val prefix = NameSpace.map_base_name (K (space_implode "_" + (the_default (map NameSpace.base_name new_type_names) alt_names))) name; val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt => is_rec_type dt andalso not (null (fst (strip_dtyp dt)))) cargs) constrs) descr in if no_size then thy diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Tools/inductive_package.ML Fri Mar 06 11:10:57 2009 +0100 @@ -698,7 +698,7 @@ ctxt1 |> LocalTheory.note kind ((rec_qualified (Binding.name "intros"), []), intrs') ||>> fold_map (fn (name, (elim, cases)) => - LocalTheory.note kind ((Binding.name (NameSpace.qualified (Sign.base_name name) "cases"), + LocalTheory.note kind ((Binding.name (NameSpace.qualified (NameSpace.base_name name) "cases"), [Attrib.internal (K (RuleCases.case_names cases)), Attrib.internal (K (RuleCases.consumes 1)), Attrib.internal (K (Induct.cases_pred name)), diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Tools/inductive_realizer.ML Fri Mar 06 11:10:57 2009 +0100 @@ -68,8 +68,8 @@ val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl (prop_of (hd intrs)))); val params = map dest_Var (Library.take (nparms, ts)); - val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs); - fun constr_of_intr intr = (Sign.base_name (name_of_thm intr), + val tname = space_implode "_" (NameSpace.base_name s ^ "T" :: vs); + fun constr_of_intr intr = (NameSpace.base_name (name_of_thm intr), map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @ filter_out (equal Extraction.nullT) (map (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)), @@ -112,7 +112,7 @@ val rT = if n then Extraction.nullT else Type (space_implode "_" (s ^ "T" :: vs), map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs); - val r = if n then Extraction.nullt else Var ((Sign.base_name s, 0), rT); + val r = if n then Extraction.nullt else Var ((NameSpace.base_name s, 0), rT); val S = list_comb (h, params @ xs); val rvs = relevant_vars S; val vs' = map fst rvs \\ vs; @@ -195,7 +195,7 @@ in if conclT = Extraction.nullT then list_abs_free (map dest_Free xs, HOLogic.unit) else list_abs_free (map dest_Free xs, list_comb - (Free ("r" ^ Sign.base_name (name_of_thm intr), + (Free ("r" ^ NameSpace.base_name (name_of_thm intr), map fastype_of (rev args) ---> conclT), rev args)) end @@ -217,7 +217,7 @@ end) (premss ~~ dummies); val frees = fold Term.add_frees fs []; val Ts = map fastype_of fs; - fun name_of_fn intr = "r" ^ Sign.base_name (name_of_thm intr) + fun name_of_fn intr = "r" ^ NameSpace.base_name (name_of_thm intr) in fst (fold_map (fn concl => fn names => let val T = Extraction.etype_of thy vs [] concl @@ -245,7 +245,7 @@ |-> (fn dtinfo => pair ((map fst dts), SOME dtinfo)) handle DatatypeAux.Datatype_Empty name' => let - val name = Sign.base_name name'; + val name = NameSpace.base_name name'; val dname = Name.variant used "Dummy" in thy @@ -296,7 +296,7 @@ val thy1' = thy1 |> Theory.copy |> - Sign.add_types (map (fn s => (Sign.base_name s, ar, NoSyn)) tnames) |> + Sign.add_types (map (fn s => (NameSpace.base_name s, ar, NoSyn)) tnames) |> fold (fn s => AxClass.axiomatize_arity (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |> Extraction.add_typeof_eqns_i ty_eqs; @@ -335,7 +335,7 @@ let val Const (s, T) = head_of (HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr)); - val s' = Sign.base_name s; + val s' = NameSpace.base_name s; val T' = Logic.unvarifyT T in (((Binding.name s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) rintrs)); val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT T)) @@ -349,7 +349,7 @@ {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Binding.empty, coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} rlzpreds rlzparams (map (fn (rintr, intr) => - ((Binding.name (Sign.base_name (name_of_thm intr)), []), + ((Binding.name (NameSpace.base_name (name_of_thm intr)), []), subst_atomic rlzpreds' (Logic.unvarify rintr))) (rintrs ~~ maps snd rss)) [] ||> Sign.absolute_path; diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Tools/old_primrec_package.ML --- a/src/HOL/Tools/old_primrec_package.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Tools/old_primrec_package.ML Fri Mar 06 11:10:57 2009 +0100 @@ -212,7 +212,7 @@ ((map snd ls) @ [dummyT]) (list_comb (Const (rec_name, dummyT), fs @ map Bound (0 ::(length ls downto 1)))) - val def_name = Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def"; + val def_name = NameSpace.base_name fname ^ "_" ^ NameSpace.base_name tname ^ "_def"; val def_prop = singleton (Syntax.check_terms (ProofContext.init thy)) (Logic.mk_equals (Const (fname, dummyT), rhs)); @@ -269,7 +269,7 @@ else primrec_err ("functions " ^ commas_quote (map fst nameTs2) ^ "\nare not mutually recursive"); val primrec_name = - if alt_name = "" then (space_implode "_" (map (Sign.base_name o #1) defs)) else alt_name; + if alt_name = "" then (space_implode "_" (map (NameSpace.base_name o #1) defs)) else alt_name; val (defs_thms', thy') = thy |> Sign.add_path primrec_name diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Tools/primrec_package.ML --- a/src/HOL/Tools/primrec_package.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Tools/primrec_package.ML Fri Mar 06 11:10:57 2009 +0100 @@ -191,7 +191,7 @@ (map snd ls @ [dummyT]) (list_comb (Const (rec_name, dummyT), fs @ map Bound (0 :: (length ls downto 1)))) - val def_name = Thm.def_name (Sign.base_name fname); + val def_name = Thm.def_name (NameSpace.base_name fname); val rhs = singleton (Syntax.check_terms ctxt) raw_rhs; val SOME var = get_first (fn ((b, _), mx) => if Binding.name_of b = fname then SOME (b, mx) else NONE) fixes; @@ -247,7 +247,7 @@ val _ = if gen_eq_set (op =) (names1, names2) then () else primrec_error ("functions " ^ commas_quote names2 ^ "\nare not mutually recursive"); - val prefix = space_implode "_" (map (Sign.base_name o #1) defs); + val prefix = space_implode "_" (map (NameSpace.base_name o #1) defs); val qualify = Binding.qualify false prefix; val spec' = (map o apfst) (fn (b, attrs) => (qualify b, Code.add_default_eqn_attrib :: attrs)) spec; diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Tools/recdef_package.ML --- a/src/HOL/Tools/recdef_package.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Tools/recdef_package.ML Fri Mar 06 11:10:57 2009 +0100 @@ -193,7 +193,7 @@ val _ = requires_recdef thy; val name = Sign.intern_const thy raw_name; - val bname = Sign.base_name name; + val bname = NameSpace.base_name name; val _ = writeln ("Defining recursive function " ^ quote name ^ " ..."); val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs); @@ -233,7 +233,7 @@ fun gen_defer_recdef tfl_fn eval_thms raw_name eqs raw_congs thy = let val name = Sign.intern_const thy raw_name; - val bname = Sign.base_name name; + val bname = NameSpace.base_name name; val _ = requires_recdef thy; val _ = writeln ("Deferred recursive function " ^ quote name ^ " ..."); diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Tools/record_package.ML Fri Mar 06 11:10:57 2009 +0100 @@ -122,7 +122,7 @@ (* syntax *) fun prune n xs = Library.drop (n, xs); -fun prefix_base s = NameSpace.map_base (fn bname => s ^ bname); +fun prefix_base s = NameSpace.map_base_name (fn bname => s ^ bname); val Trueprop = HOLogic.mk_Trueprop; fun All xs t = Term.list_all_free (xs, t); @@ -702,7 +702,7 @@ SOME flds => (let val (f::fs) = but_last (map fst flds); - val flds' = Sign.extern_const thy f :: map NameSpace.base fs; + val flds' = Sign.extern_const thy f :: map NameSpace.base_name fs; val (args',more) = split_last args; in (flds'~~args')@field_lst more end handle Library.UnequalLengths => [("",t)]) @@ -804,7 +804,7 @@ => (let val (f :: fs) = but_last flds; val flds' = apfst (Sign.extern_const thy) f - :: map (apfst NameSpace.base) fs; + :: map (apfst NameSpace.base_name) fs; val (args', more) = split_last args; val alphavars = map varifyT (but_last alphas); val subst = fold2 (curry (Sign.typ_match thy)) @@ -1069,7 +1069,7 @@ val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get thy; (*fun mk_abs_var x t = (x, fastype_of t);*) - fun sel_name u = NameSpace.base (unsuffix updateN u); + fun sel_name u = NameSpace.base_name (unsuffix updateN u); fun seed s (upd as Const (more,Type(_,[mT,_]))$ k $ r) = if has_field extfields s (domain_type' mT) then upd else seed s r @@ -1463,7 +1463,7 @@ in map rewrite_rule [abs_inject, abs_inverse, abs_induct] end; in thy - |> TypecopyPackage.add_typecopy (suffix ext_typeN (Sign.base_name name), alphas) repT NONE + |> TypecopyPackage.add_typecopy (suffix ext_typeN (NameSpace.base_name name), alphas) repT NONE |-> (fn (name, _) => `(fn thy => get_thms thy name)) end; @@ -1474,7 +1474,7 @@ fun extension_definition full name fields names alphas zeta moreT more vars thy = let - val base = Sign.base_name; + val base = NameSpace.base_name; val fieldTs = (map snd fields); val alphas_zeta = alphas@[zeta]; val alphas_zetaTs = map (fn n => TFree (n, HOLogic.typeS)) alphas_zeta; @@ -1760,7 +1760,7 @@ val alphas = map fst args; val name = Sign.full_bname thy bname; val full = Sign.full_bname_path thy bname; - val base = Sign.base_name; + val base = NameSpace.base_name; val (bfields, field_syntax) = split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields); diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Tools/refute.ML Fri Mar 06 11:10:57 2009 +0100 @@ -63,6 +63,7 @@ val close_form : Term.term -> Term.term val get_classdef : theory -> string -> (string * Term.term) option + val norm_rhs : Term.term -> Term.term val get_def : theory -> string * Term.typ -> (string * Term.term) option val get_typedef : theory -> Term.typ -> (string * Term.term) option val is_IDT_constructor : theory -> string * Term.typ -> bool @@ -548,6 +549,20 @@ end; (* ------------------------------------------------------------------------- *) +(* norm_rhs: maps f ?t1 ... ?tn == rhs to %t1...tn. rhs *) +(* ------------------------------------------------------------------------- *) + + fun norm_rhs eqn = + let + fun lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t)) + | lambda v t = raise TERM ("lambda", [v, t]) + val (lhs, rhs) = Logic.dest_equals eqn + val (_, args) = Term.strip_comb lhs + in + fold lambda (rev args) rhs + end + +(* ------------------------------------------------------------------------- *) (* get_def: looks up the definition of a constant, as created by "constdefs" *) (* ------------------------------------------------------------------------- *) @@ -555,16 +570,6 @@ fun get_def thy (s, T) = let - (* maps f ?t1 ... ?tn == rhs to %t1...tn. rhs *) - fun norm_rhs eqn = - let - fun lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t)) - | lambda v t = raise TERM ("lambda", [v, t]) - val (lhs, rhs) = Logic.dest_equals eqn - val (_, args) = Term.strip_comb lhs - in - fold lambda (rev args) rhs - end (* (string * Term.term) list -> (string * Term.term) option *) fun get_def_ax [] = NONE | get_def_ax ((axname, ax) :: axioms) = diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Tools/res_atp.ML Fri Mar 06 11:10:57 2009 +0100 @@ -34,8 +34,6 @@ val convergence = 3.2; (*Higher numbers allow longer inference chains*) val follow_defs = false; (*Follow definitions. Makes problems bigger.*) val include_all = true; -val include_simpset = false; -val include_claset = false; val include_atpset = true; (***************************************************************) @@ -380,7 +378,7 @@ (*Ignore blacklisted basenames*) fun add_multi_names ((a, ths), pairs) = - if (Sign.base_name a) mem_string ResAxioms.multi_base_blacklist then pairs + if (NameSpace.base_name a) mem_string ResAxioms.multi_base_blacklist then pairs else add_single_names ((a, ths), pairs); fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a; @@ -409,17 +407,11 @@ (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems"))) (name_thm_pairs ctxt)) else - let val claset_thms = - if include_claset then ResAxioms.claset_rules_of ctxt - else [] - val simpset_thms = - if include_simpset then ResAxioms.simpset_rules_of ctxt - else [] - val atpset_thms = + let val atpset_thms = if include_atpset then ResAxioms.atpset_rules_of ctxt else [] val _ = (Output.debug (fn () => "ATP theorems: "); app display_thm atpset_thms) - in claset_thms @ simpset_thms @ atpset_thms end + in atpset_thms end val user_rules = filter check_named (map ResAxioms.pairname (if null user_thms then whitelist else user_thms)) diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Tools/res_axioms.ML Fri Mar 06 11:10:57 2009 +0100 @@ -15,8 +15,6 @@ val expand_defs_tac: thm -> tactic val combinators: thm -> thm val neg_conjecture_clauses: thm -> int -> thm list * (string * typ) list - val claset_rules_of: Proof.context -> (string * thm) list (*FIXME DELETE*) - val simpset_rules_of: Proof.context -> (string * thm) list (*FIXME DELETE*) val atpset_rules_of: Proof.context -> (string * thm) list val suppress_endtheory: bool ref (*for emergency use where endtheory causes problems*) val setup: theory -> theory @@ -342,7 +340,7 @@ (*Skolemize a named theorem, with Skolem functions as additional premises.*) fun skolem_thm (s, th) = - if member (op =) multi_base_blacklist (Sign.base_name s) orelse bad_for_atp th then [] + if member (op =) multi_base_blacklist (NameSpace.base_name s) orelse bad_for_atp th then [] else let val ctxt0 = Variable.thm_context th @@ -378,24 +376,10 @@ end; -(**** Extract and Clausify theorems from a theory's claset and simpset ****) +(**** Rules from the context ****) fun pairname th = (Thm.get_name_hint th, th); -fun rules_of_claset cs = - let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs - val intros = safeIs @ hazIs - val elims = map Classical.classical_rule (safeEs @ hazEs) - in map pairname (intros @ elims) end; - -fun rules_of_simpset ss = - let val ({rules,...}, _) = rep_ss ss - val simps = Net.entries rules - in map (fn r => (#name r, #thm r)) simps end; - -fun claset_rules_of ctxt = rules_of_claset (local_claset_of ctxt); -fun simpset_rules_of ctxt = rules_of_simpset (local_simpset_of ctxt); - fun atpset_rules_of ctxt = map pairname (ResAtpset.get ctxt); @@ -444,7 +428,7 @@ val new_facts = (PureThy.facts_of thy, []) |-> Facts.fold_static (fn (name, ths) => if already_seen thy name then I else cons (name, ths)); val new_thms = (new_facts, []) |-> fold (fn (name, ths) => - if member (op =) multi_base_blacklist (Sign.base_name name) then I + if member (op =) multi_base_blacklist (NameSpace.base_name name) then I else fold_index (fn (i, th) => if bad_for_atp th orelse is_some (lookup_cache thy th) then I else cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths); diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Tools/sat_solver.ML --- a/src/HOL/Tools/sat_solver.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Tools/sat_solver.ML Fri Mar 06 11:10:57 2009 +0100 @@ -914,10 +914,6 @@ fun zchaff fm = let val _ = if (getenv "ZCHAFF_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () - val _ = if (getenv "ZCHAFF_VERSION") <> "2004.5.13" andalso - (getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else () - (* both versions of zChaff appear to have the same interface, so we do *) - (* not actually need to distinguish between them in the following code *) val serial_str = serial_string () val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf")) val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) @@ -943,11 +939,12 @@ let fun berkmin fm = let - val _ = if (getenv "BERKMIN_HOME") = "" orelse (getenv "BERKMIN_EXE") = "" then raise SatSolver.NOT_CONFIGURED else () + val _ = if (getenv "BERKMIN_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () val serial_str = serial_string () val inpath = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf")) val outpath = File.tmp_path (Path.explode ("result" ^ serial_str)) - val cmd = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath) + val exec = getenv "BERKMIN_EXE" + val cmd = (getenv "BERKMIN_HOME") ^ "/" ^ (if exec = "" then "BerkMin561" else exec) ^ " " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath) fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) fun readfn () = SatSolver.read_std_result_file outpath ("Satisfiable !!", "solution =", "UNSATISFIABLE !!") val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/Tools/specification_package.ML --- a/src/HOL/Tools/specification_package.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/Tools/specification_package.ML Fri Mar 06 11:10:57 2009 +0100 @@ -24,7 +24,7 @@ val ctype = domain_type (type_of P) val cname_full = Sign.intern_const thy cname val cdefname = if thname = "" - then Thm.def_name (Sign.base_name cname) + then Thm.def_name (NameSpace.base_name cname) else thname val def_eq = Logic.mk_equals (Const(cname_full,ctype), HOLogic.choice_const ctype $ P) @@ -50,7 +50,7 @@ val ctype = domain_type (type_of P) val cname_full = Sign.intern_const thy cname val cdefname = if thname = "" - then Thm.def_name (Sign.base_name cname) + then Thm.def_name (NameSpace.base_name cname) else thname val co = Const(cname_full,ctype) val thy' = Theory.add_finals_i covld [co] thy @@ -154,7 +154,7 @@ fun mk_exist (c,prop) = let val T = type_of c - val cname = Sign.base_name (fst (dest_Const c)) + val cname = NameSpace.base_name (fst (dest_Const c)) val vname = if Syntax.is_identifier cname then cname else "x" diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOL/ex/Quickcheck_Generators.thy --- a/src/HOL/ex/Quickcheck_Generators.thy Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOL/ex/Quickcheck_Generators.thy Fri Mar 06 11:10:57 2009 +0100 @@ -138,7 +138,7 @@ let val this_ty = Type (hd tycos, map TFree vs); val this_ty' = StateMonad.liftT (term_ty this_ty) @{typ seed}; - val random_name = NameSpace.base @{const_name random}; + val random_name = NameSpace.base_name @{const_name random}; val random'_name = random_name ^ "_" ^ Class.type_name (hd tycos) ^ "'"; fun random ty = Sign.mk_const thy (@{const_name random}, [ty]); val random' = Free (random'_name, diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOLCF/Tools/domain/domain_axioms.ML --- a/src/HOLCF/Tools/domain/domain_axioms.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOLCF/Tools/domain/domain_axioms.ML Fri Mar 06 11:10:57 2009 +0100 @@ -22,7 +22,7 @@ val dc_rep = %%:(dname^"_rep"); val x_name'= "x"; val x_name = idx_name eqs x_name' (n+1); - val dnam = Sign.base_name dname; + val dnam = NameSpace.base_name dname; val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name')); val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name')); diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOLCF/Tools/domain/domain_extender.ML --- a/src/HOLCF/Tools/domain/domain_extender.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOLCF/Tools/domain/domain_extender.ML Fri Mar 06 11:10:57 2009 +0100 @@ -103,7 +103,7 @@ (Sign.full_bname thy''' dname, map (Syntax.read_typ_global thy''') vs)) o fst) eqs'''; val cons''' = map snd eqs'''; - fun thy_type (dname,tvars) = (Sign.base_name dname, length tvars, NoSyn); + fun thy_type (dname,tvars) = (NameSpace.base_name dname, length tvars, NoSyn); fun thy_arity (dname,tvars) = (dname, map (snd o dest_TFree) tvars, pcpoS); val thy'' = thy''' |> Sign.add_types (map thy_type dtnvs) |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs; @@ -114,7 +114,7 @@ val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs'; fun strip ss = Library.drop (find_index_eq "'" ss +1, ss); fun typid (Type (id,_)) = - let val c = hd (Symbol.explode (Sign.base_name id)) + let val c = hd (Symbol.explode (NameSpace.base_name id)) in if Symbol.is_letter c then c else "t" end | typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id))) | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id)); @@ -133,7 +133,7 @@ ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs); in theorems_thy - |> Sign.add_path (Sign.base_name comp_dnam) + |> Sign.add_path (NameSpace.base_name comp_dnam) |> (snd o (PureThy.add_thmss [((Binding.name "rews", List.concat rewss @ take_rews), [])])) |> Sign.parent_path end; diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOLCF/Tools/domain/domain_syntax.ML --- a/src/HOLCF/Tools/domain/domain_syntax.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOLCF/Tools/domain/domain_syntax.ML Fri Mar 06 11:10:57 2009 +0100 @@ -25,7 +25,7 @@ in val dtype = Type(dname,typevars); val dtype2 = foldr1 mk_ssumT (map prod cons'); - val dnam = Sign.base_name dname; + val dnam = NameSpace.base_name dname; val const_rep = (dnam^"_rep" , dtype ->> dtype2, NoSyn); val const_abs = (dnam^"_abs" , dtype2 ->> dtype , NoSyn); val const_when = (dnam^"_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn); diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOLCF/Tools/domain/domain_theorems.ML --- a/src/HOLCF/Tools/domain/domain_theorems.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML Fri Mar 06 11:10:57 2009 +0100 @@ -606,7 +606,7 @@ in thy - |> Sign.add_path (Sign.base_name dname) + |> Sign.add_path (NameSpace.base_name dname) |> (snd o (PureThy.add_thmss (map (Thm.no_attributes o apfst Binding.name) [ ("iso_rews" , iso_rews ), ("exhaust" , [exhaust] ), diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/HOLCF/Tools/fixrec_package.ML --- a/src/HOLCF/Tools/fixrec_package.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/HOLCF/Tools/fixrec_package.ML Fri Mar 06 11:10:57 2009 +0100 @@ -181,7 +181,7 @@ val fixpoint = mk_fix (lambda_ctuple lhss (mk_ctuple rhss)); fun one_def (l as Free(n,_)) r = - let val b = Sign.base_name n + let val b = NameSpace.base_name n in ((Binding.name (b^"_def"), []), r) end | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form"; fun defs [] _ = [] @@ -230,7 +230,7 @@ fun taken_names (t : term) : bstring list = let - fun taken (Const(a,_), bs) = insert (op =) (Sign.base_name a) bs + fun taken (Const(a,_), bs) = insert (op =) (NameSpace.base_name a) bs | taken (Free(a,_) , bs) = insert (op =) a bs | taken (f $ u , bs) = taken (f, taken (u, bs)) | taken (Abs(a,_,t), bs) = taken (t, insert (op =) a bs) diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Pure/General/binding.ML --- a/src/Pure/General/binding.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Pure/General/binding.ML Fri Mar 06 11:10:57 2009 +0100 @@ -10,17 +10,18 @@ signature BINDING = sig type binding - val dest: binding -> (string * bool) list * (string * bool) list * bstring + val dest: binding -> (string * bool) list * bstring val verbose: bool ref val str_of: binding -> string val make: bstring * Position.T -> binding + val pos_of: binding -> Position.T val name: bstring -> binding - val pos_of: binding -> Position.T val name_of: binding -> string val map_name: (bstring -> bstring) -> binding -> binding val empty: binding val is_empty: binding -> bool val qualify: bool -> string -> binding -> binding + val prefix_of: binding -> (string * bool) list val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding val add_prefix: bool -> string -> binding -> binding end; @@ -32,13 +33,11 @@ (* datatype *) -type component = string * bool; (*name with mandatory flag*) - datatype binding = Binding of - {prefix: component list, (*system prefix*) - qualifier: component list, (*user qualifier*) - name: bstring, (*base name*) - pos: Position.T}; (*source position*) + {prefix: (string * bool) list, (*system prefix*) + qualifier: (string * bool) list, (*user qualifier*) + name: bstring, (*base name*) + pos: Position.T}; (*source position*) fun make_binding (prefix, qualifier, name, pos) = Binding {prefix = prefix, qualifier = qualifier, name = name, pos = pos}; @@ -46,7 +45,7 @@ fun map_binding f (Binding {prefix, qualifier, name, pos}) = make_binding (f (prefix, qualifier, name, pos)); -fun dest (Binding {prefix, qualifier, name, ...}) = (prefix, qualifier, name); +fun dest (Binding {prefix, qualifier, name, ...}) = (prefix @ qualifier, name); (* diagnostic output *) @@ -92,6 +91,8 @@ (* system prefix *) +fun prefix_of (Binding {prefix, ...}) = prefix; + fun map_prefix f = map_binding (fn (prefix, qualifier, name, pos) => (f prefix, qualifier, name, pos)); diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Pure/General/graph.ML --- a/src/Pure/General/graph.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Pure/General/graph.ML Fri Mar 06 11:10:57 2009 +0100 @@ -21,7 +21,6 @@ val maximals: 'a T -> key list val subgraph: (key -> bool) -> 'a T -> 'a T val map_nodes: ('a -> 'b) -> 'a T -> 'b T - val fold_map_nodes: (key * 'a -> 'b -> 'c * 'b) -> 'a T -> 'b -> 'c T * 'b val get_node: 'a T -> key -> 'a (*exception UNDEF*) val map_node: key -> ('a -> 'a) -> 'a T -> 'a T val map_node_yield: key -> ('a -> 'b * 'a) -> 'a T -> 'b * 'a T @@ -116,9 +115,6 @@ fun map_nodes f (Graph tab) = Graph (Table.map (fn (i, ps) => (f i, ps)) tab); -fun fold_map_nodes f (Graph tab) = - apfst Graph o Table.fold_map (fn (k, (i, ps)) => f (k, i) #> apfst (rpair ps)) tab; - fun get_node G = #1 o get_entry G; fun map_node x f = map_entry x (fn (i, ps) => (f i, ps)); diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Pure/General/name_space.ML Fri Mar 06 11:10:57 2009 +0100 @@ -25,9 +25,9 @@ val explode: string -> string list val append: string -> string -> string val qualified: string -> string -> string - val base: string -> string + val base_name: string -> string val qualifier: string -> string - val map_base: (string -> string) -> string -> string + val map_base_name: (string -> string) -> string -> string type T val empty: T val intern: T -> xstring -> string @@ -78,14 +78,14 @@ if path = "" orelse name = "" then name else path ^ separator ^ name; -fun base "" = "" - | base name = List.last (explode_name name); +fun base_name "" = "" + | base_name name = List.last (explode_name name); fun qualifier "" = "" | qualifier name = implode_name (#1 (split_last (explode_name name))); -fun map_base _ "" = "" - | map_base f name = +fun map_base_name _ "" = "" + | map_base_name f name = let val names = explode_name name in implode_name (nth_map (length names - 1) f names) end; @@ -123,7 +123,7 @@ datatype T = NameSpace of (string list * string list) Symtab.table * (*internals, hidden internals*) - string list Symtab.table; (*externals*) + xstring list Symtab.table; (*externals*) val empty = NameSpace (Symtab.empty, Symtab.empty); @@ -153,15 +153,15 @@ fun extern_flags {long_names, short_names, unique_names} space name = let - fun valid unique xname = - let val (name', uniq) = lookup space xname - in name = name' andalso (uniq orelse not unique) end; + fun valid require_unique xname = + let val (name', is_unique) = lookup space xname + in name = name' andalso (not require_unique orelse is_unique) end; fun ext [] = if valid false name then name else hidden name | ext (nm :: nms) = if valid unique_names nm then nm else ext nms; in if long_names then name - else if short_names then base name + else if short_names then base_name name else ext (get_accesses space name) end; @@ -204,7 +204,7 @@ let val names = valid_accesses space name in space |> add_name' name name - |> fold (del_name name) (if fully then names else names inter_string [base name]) + |> fold (del_name name) (if fully then names else names inter_string [base_name name]) |> fold (del_name_extra name) (get_accesses space name) end; @@ -278,8 +278,8 @@ fun full_name naming binding = let - val (prefix, qualifier, bname) = Binding.dest binding; - val naming' = apply_prefix (prefix @ qualifier) naming; + val (prfx, bname) = Binding.dest binding; + val naming' = apply_prefix prfx naming; in full naming' bname end; @@ -287,8 +287,8 @@ fun declare naming binding space = let - val (prefix, qualifier, bname) = Binding.dest binding; - val naming' = apply_prefix (prefix @ qualifier) naming; + val (prfx, bname) = Binding.dest binding; + val naming' = apply_prefix prfx naming; val name = full naming' bname; val names = explode_name name; diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Pure/General/table.ML --- a/src/Pure/General/table.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Pure/General/table.ML Fri Mar 06 11:10:57 2009 +0100 @@ -24,7 +24,6 @@ val map': (key -> 'a -> 'b) -> 'a table -> 'b table val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a - val fold_map: (key * 'b -> 'a -> 'c * 'a) -> 'b table -> 'a -> 'c table * 'a val dest: 'a table -> (key * 'a) list val keys: 'a table -> key list val exists: (key * 'a -> bool) -> 'a table -> bool @@ -112,25 +111,6 @@ fold left (f p1 (fold mid (f p2 (fold right x)))); in fold end; -fun fold_map_table f = - let - fun fold_map Empty s = (Empty, s) - | fold_map (Branch2 (left, p as (k, x), right)) s = - s - |> fold_map left - ||>> f p - ||>> fold_map right - |-> (fn ((l, e), r) => pair (Branch2 (l, (k, e), r))) - | fold_map (Branch3 (left, p1 as (k1, x1), mid, p2 as (k2, x2), right)) s = - s - |> fold_map left - ||>> f p1 - ||>> fold_map mid - ||>> f p2 - ||>> fold_map right - |-> (fn ((((l, e1), m), e2), r) => pair (Branch3 (l, (k1, e1), m, (k2, e2), r))) - in fold_map end; - fun dest tab = fold_rev_table cons tab []; fun keys tab = fold_rev_table (cons o #1) tab []; @@ -366,7 +346,7 @@ fun join f (table1, table2) = let fun add (key, y) tab = modify key (fn NONE => y | SOME x => f key (x, y)) tab; - in fold_table add table2 table1 end; + in if pointer_eq (table1, table2) then table1 else fold_table add table2 table1 end; fun merge eq = join (fn key => fn xy => if eq xy then raise SAME else raise DUP key); @@ -398,7 +378,6 @@ val map' = map_table; val fold = fold_table; val fold_rev = fold_rev_table; -val fold_map = fold_map_table; end; diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Pure/Isar/calculation.ML --- a/src/Pure/Isar/calculation.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Pure/Isar/calculation.ML Fri Mar 06 11:10:57 2009 +0100 @@ -114,7 +114,7 @@ fun print_calculation false _ _ = () | print_calculation true ctxt calc = Pretty.writeln - (ProofContext.pretty_fact ctxt (ProofContext.full_bname ctxt calculationN, calc)); + (ProofContext.pretty_fact ctxt (ProofContext.full_name ctxt (Binding.name calculationN), calc)); (* also and finally *) diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Pure/Isar/class_target.ML --- a/src/Pure/Isar/class_target.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Pure/Isar/class_target.ML Fri Mar 06 11:10:57 2009 +0100 @@ -300,7 +300,7 @@ map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) o these_operations thy; fun redeclare_const thy c = - let val b = Sign.base_name c + let val b = NameSpace.base_name c in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end; fun synchronize_class_syntax sort base_sort ctxt = @@ -358,7 +358,7 @@ (* class target *) -val class_prefix = Logic.const_of_class o Sign.base_name; +val class_prefix = Logic.const_of_class o NameSpace.base_name; fun declare class pos ((c, mx), dict) thy = let @@ -475,7 +475,7 @@ fun type_name "*" = "prod" | type_name "+" = "sum" - | type_name s = sanatize_name (NameSpace.base s); + | type_name s = sanatize_name (NameSpace.base_name s); fun resort_terms pp algebra consts constraints ts = let diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Pure/Isar/element.ML Fri Mar 06 11:10:57 2009 +0100 @@ -202,7 +202,7 @@ let val head = if Thm.has_name_hint th then Pretty.block [Pretty.command kind, - Pretty.brk 1, Pretty.str (Sign.base_name (Thm.get_name_hint th) ^ ":")] + Pretty.brk 1, Pretty.str (NameSpace.base_name (Thm.get_name_hint th) ^ ":")] else Pretty.command kind in Pretty.block (Pretty.fbreaks (head :: prts)) end; diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Fri Mar 06 11:10:57 2009 +0100 @@ -150,10 +150,12 @@ val oracle = SymbolPos.content (SymbolPos.explode (oracle_txt, pos)); val txt = "local\n\ - \ val name = " ^ quote name ^ ";\n\ + \ val name = " ^ ML_Syntax.print_string name ^ ";\n\ + \ val pos = " ^ ML_Syntax.print_position pos ^ ";\n\ + \ val binding = Binding.make (name, pos);\n\ \ val oracle = " ^ oracle ^ ";\n\ \in\n\ - \ val " ^ name ^ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (name, oracle))));\n\ + \ val " ^ name ^ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, oracle))));\n\ \end;\n"; in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false pos txt)) end; diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Pure/Isar/proof.ML Fri Mar 06 11:10:57 2009 +0100 @@ -1006,7 +1006,7 @@ fun after_local' [[th]] = put_thms false (AutoBind.thisN, SOME [th]); fun after_global' [[th]] = ProofContext.put_thms false (AutoBind.thisN, SOME [th]); val after_qed' = (after_local', after_global'); - val this_name = ProofContext.full_bname goal_ctxt AutoBind.thisN; + val this_name = ProofContext.full_name goal_ctxt (Binding.name AutoBind.thisN); val result_ctxt = state diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Pure/Isar/proof_context.ML Fri Mar 06 11:10:57 2009 +0100 @@ -23,7 +23,6 @@ val set_stmt: bool -> Proof.context -> Proof.context val naming_of: Proof.context -> NameSpace.naming val full_name: Proof.context -> binding -> string - val full_bname: Proof.context -> bstring -> string val consts_of: Proof.context -> Consts.T val const_syntax_name: Proof.context -> string -> string val the_const_constraint: Proof.context -> string -> typ @@ -243,9 +242,7 @@ map_mode (fn (_, pattern, schematic, abbrev) => (stmt, pattern, schematic, abbrev)); val naming_of = #naming o rep_context; - val full_name = NameSpace.full_name o naming_of; -fun full_bname thy = NameSpace.full_name (naming_of thy) o Binding.name; val syntax_of = #syntax o rep_context; val syn_of = LocalSyntax.syn_of o syntax_of; @@ -266,11 +263,9 @@ fun transfer_syntax thy = map_syntax (LocalSyntax.rebuild thy) #> - map_consts (fn consts as (local_consts, global_consts) => - let val thy_consts = Sign.consts_of thy in - if Consts.eq_consts (thy_consts, global_consts) then consts - else (Consts.merge (local_consts, thy_consts), thy_consts) - end); + map_consts (fn (local_consts, _) => + let val thy_consts = Sign.consts_of thy + in (Consts.merge (local_consts, thy_consts), thy_consts) end); fun transfer thy = Context.transfer_proof thy #> transfer_syntax thy; diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Pure/Isar/proof_display.ML --- a/src/Pure/Isar/proof_display.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Pure/Isar/proof_display.ML Fri Mar 06 11:10:57 2009 +0100 @@ -75,7 +75,7 @@ fun pretty_fact_name (kind, "") = Pretty.str kind | pretty_fact_name (kind, name) = Pretty.block [Pretty.str kind, Pretty.brk 1, - Pretty.str (NameSpace.base name), Pretty.str ":"]; + Pretty.str (NameSpace.base_name name), Pretty.str ":"]; fun pretty_facts ctxt = flat o (separate [Pretty.fbrk, Pretty.str "and "]) o diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Pure/Isar/skip_proof.ML --- a/src/Pure/Isar/skip_proof.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Pure/Isar/skip_proof.ML Fri Mar 06 11:10:57 2009 +0100 @@ -20,7 +20,7 @@ (* oracle setup *) val (_, skip_proof) = Context.>>> (Context.map_theory_result - (Thm.add_oracle ("skip_proof", fn (thy, prop) => + (Thm.add_oracle (Binding.name "skip_proof", fn (thy, prop) => if ! quick_and_dirty then Thm.cterm_of thy prop else error "Proof may be skipped in quick_and_dirty mode only!"))); diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Pure/Isar/theory_target.ML Fri Mar 06 11:10:57 2009 +0100 @@ -188,7 +188,7 @@ val arg = (b', Term.close_schematic_term rhs'); val similar_body = Type.similar_types (rhs, rhs'); (* FIXME workaround based on educated guess *) - val (prefix', _, _) = Binding.dest b'; + val prefix' = Binding.prefix_of b'; val class_global = Binding.name_of b = Binding.name_of b' andalso not (null prefix') andalso (fst o snd o split_last) prefix' = Class_Target.class_prefix target; @@ -330,7 +330,7 @@ fun init_lthy (ta as Target {target, instantiation, overloading, ...}) = Data.put ta #> - LocalTheory.init (NameSpace.base target) + LocalTheory.init (NameSpace.base_name target) {pretty = pretty ta, abbrev = abbrev ta, define = define ta, diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Pure/ML/ml_antiquote.ML --- a/src/Pure/ML/ml_antiquote.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Pure/ML/ml_antiquote.ML Fri Mar 06 11:10:57 2009 +0100 @@ -110,7 +110,7 @@ fun type_ syn = (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, c) => #1 (Term.dest_Type (ProofContext.read_tyname ctxt c)) - |> syn ? Sign.base_name + |> syn ? NameSpace.base_name |> ML_Syntax.print_string)); val _ = inline "type_name" (type_ false); diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Pure/ProofGeneral/proof_general_emacs.ML --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Fri Mar 06 11:10:57 2009 +0100 @@ -39,7 +39,7 @@ then XML.output_markup (name, props) else Markup.no_output; val (bg2, en2) = - if (case ts of [XML.Text _] => false | _ => true) then Markup.no_output + if null ts then Markup.no_output else if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P") else if name = Markup.sendbackN then (special "W", special "X") else if name = Markup.hiliteN then (special "0", special "1") diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Pure/Thy/thm_deps.ML --- a/src/Pure/Thy/thm_deps.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Pure/Thy/thm_deps.ML Fri Mar 06 11:10:57 2009 +0100 @@ -33,7 +33,7 @@ | _ => ["global"]); val parents = filter_out (fn s => s = "") (map (#1 o #2) thms'); val entry = - {name = Sign.base_name name, + {name = NameSpace.base_name name, ID = name, dir = space_implode "/" (session @ prefix), unfold = false, diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Pure/axclass.ML --- a/src/Pure/axclass.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Pure/axclass.ML Fri Mar 06 11:10:57 2009 +0100 @@ -158,7 +158,7 @@ (* maintain instances *) -fun instance_name (a, c) = NameSpace.base c ^ "_" ^ NameSpace.base a; +fun instance_name (a, c) = NameSpace.base_name c ^ "_" ^ NameSpace.base_name a; val get_instances = #1 o #2 o AxClassData.get; val map_instances = AxClassData.map o apsnd o apfst; @@ -367,7 +367,7 @@ | NONE => error ("Illegal type for instantiation of class parameter: " ^ quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T)); val name_inst = instance_name (tyco, class) ^ "_inst"; - val c' = NameSpace.base c ^ "_" ^ NameSpace.base tyco; + val c' = NameSpace.base_name c ^ "_" ^ NameSpace.base_name tyco; val T' = Type.strip_sorts T; in thy @@ -391,7 +391,7 @@ val (c', eq) = get_inst_param thy (c, tyco); val prop = Logic.mk_equals (Const (c', T), t); val name' = Thm.def_name_optional - (NameSpace.base c ^ "_" ^ NameSpace.base tyco) name; + (NameSpace.base_name c ^ "_" ^ NameSpace.base_name tyco) name; in thy |> Thm.add_def false false (Binding.name name', prop) diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Pure/codegen.ML --- a/src/Pure/codegen.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Pure/codegen.ML Fri Mar 06 11:10:57 2009 +0100 @@ -938,7 +938,7 @@ in e () end; val (_, evaluation_conv) = Context.>>> (Context.map_theory_result - (Thm.add_oracle ("evaluation", fn ct => + (Thm.add_oracle (Binding.name "evaluation", fn ct => let val thy = Thm.theory_of_cterm ct; val t = Thm.term_of ct; diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Pure/consts.ML --- a/src/Pure/consts.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Pure/consts.ML Fri Mar 06 11:10:57 2009 +0100 @@ -8,7 +8,6 @@ signature CONSTS = sig type T - val eq_consts: T * T -> bool val abbrevs_of: T -> string list -> (term * term) list val dest: T -> {constants: (typ * term option) NameSpace.table, @@ -52,23 +51,21 @@ datatype T = Consts of {decls: ((decl * abbrev option) * serial) NameSpace.table, constraints: typ Symtab.table, - rev_abbrevs: (term * term) list Symtab.table} * stamp; - -fun eq_consts (Consts (_, s1), Consts (_, s2)) = s1 = s2; + rev_abbrevs: (term * term) list Symtab.table}; fun make_consts (decls, constraints, rev_abbrevs) = - Consts ({decls = decls, constraints = constraints, rev_abbrevs = rev_abbrevs}, stamp ()); + Consts {decls = decls, constraints = constraints, rev_abbrevs = rev_abbrevs}; -fun map_consts f (Consts ({decls, constraints, rev_abbrevs}, _)) = +fun map_consts f (Consts {decls, constraints, rev_abbrevs}) = make_consts (f (decls, constraints, rev_abbrevs)); -fun abbrevs_of (Consts ({rev_abbrevs, ...}, _)) modes = +fun abbrevs_of (Consts {rev_abbrevs, ...}) modes = maps (Symtab.lookup_list rev_abbrevs) modes; (* dest consts *) -fun dest (Consts ({decls = (space, decls), constraints, ...}, _)) = +fun dest (Consts {decls = (space, decls), constraints, ...}) = {constants = (space, Symtab.fold (fn (c, (({T, ...}, abbr), _)) => Symtab.update (c, (T, Option.map #rhs abbr))) decls Symtab.empty), @@ -77,7 +74,7 @@ (* lookup consts *) -fun the_const (Consts ({decls = (_, tab), ...}, _)) c = +fun the_const (Consts {decls = (_, tab), ...}) c = (case Symtab.lookup tab c of SOME (decl, _) => decl | NONE => raise TYPE ("Unknown constant: " ^ quote c, [], [])); @@ -99,7 +96,7 @@ val is_monomorphic = null oo type_arguments; -fun the_constraint (consts as Consts ({constraints, ...}, _)) c = +fun the_constraint (consts as Consts {constraints, ...}) c = (case Symtab.lookup constraints c of SOME T => T | NONE => type_scheme consts c); @@ -107,7 +104,7 @@ (* name space and syntax *) -fun space_of (Consts ({decls = (space, _), ...}, _)) = space; +fun space_of (Consts {decls = (space, _), ...}) = space; val intern = NameSpace.intern o space_of; val extern = NameSpace.extern o space_of; @@ -120,7 +117,7 @@ fun syntax consts (c, mx) = let val ({T, authentic, ...}, _) = the_const consts c handle TYPE (msg, _, _) => error msg; - val c' = if authentic then Syntax.constN ^ c else NameSpace.base c; + val c' = if authentic then Syntax.constN ^ c else NameSpace.base_name c; in (c', T, mx) end; fun syntax_name consts c = #1 (syntax consts (c, NoSyn)); @@ -267,17 +264,16 @@ val expand_term = certify pp tsig true consts; val force_expand = mode = PrintMode.internal; + val _ = Term.exists_subterm Term.is_Var raw_rhs andalso + error ("Illegal schematic variables on rhs of abbreviation: " ^ Binding.str_of b); + val rhs = raw_rhs |> Term.map_types (Type.cert_typ tsig) - |> cert_term; + |> cert_term + |> Term.close_schematic_term; val normal_rhs = expand_term rhs; val T = Term.fastype_of rhs; val lhs = Const (NameSpace.full_name naming b, T); - - fun err msg = (warning (* FIXME should be error *) (msg ^ " on rhs of abbreviation:\n" ^ - Pretty.string_of_term pp (Logic.mk_equals (lhs, rhs))); true); - val _ = Term.exists_subterm Term.is_Var rhs andalso err "Illegal schematic variables"; - val _ = null (Term.hidden_polymorphism rhs) orelse err "Extra type variables"; in consts |> map_consts (fn (decls, constraints, rev_abbrevs) => let @@ -307,8 +303,8 @@ val empty = make_consts (NameSpace.empty_table, Symtab.empty, Symtab.empty); fun merge - (Consts ({decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1}, _), - Consts ({decls = decls2, constraints = constraints2, rev_abbrevs = rev_abbrevs2}, _)) = + (Consts {decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1}, + Consts {decls = decls2, constraints = constraints2, rev_abbrevs = rev_abbrevs2}) = let val decls' = NameSpace.merge_tables (eq_snd (op =)) (decls1, decls2) handle Symtab.DUP c => err_dup_const c; diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Pure/logic.ML --- a/src/Pure/logic.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Pure/logic.ML Fri Mar 06 11:10:57 2009 +0100 @@ -230,7 +230,7 @@ (* class relations *) fun name_classrel (c1, c2) = - NameSpace.base c1 ^ "_" ^ NameSpace.base c2; + NameSpace.base_name c1 ^ "_" ^ NameSpace.base_name c2; fun mk_classrel (c1, c2) = mk_inclass (Term.aT [c1], c2); @@ -243,8 +243,8 @@ (* type arities *) fun name_arities (t, _, S) = - let val b = NameSpace.base t - in S |> map (fn c => NameSpace.base c ^ "_" ^ b) end; + let val b = NameSpace.base_name t + in S |> map (fn c => NameSpace.base_name c ^ "_" ^ b) end; fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c])); diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Pure/old_term.ML --- a/src/Pure/old_term.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Pure/old_term.ML Fri Mar 06 11:10:57 2009 +0100 @@ -39,7 +39,7 @@ (*Accumulates the names in the term, suppressing duplicates. Includes Frees and Consts. For choosing unambiguous bound var names.*) -fun add_term_names (Const(a,_), bs) = insert (op =) (NameSpace.base a) bs +fun add_term_names (Const(a,_), bs) = insert (op =) (NameSpace.base_name a) bs | add_term_names (Free(a,_), bs) = insert (op =) a bs | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs)) | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs) diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Pure/primitive_defs.ML --- a/src/Pure/primitive_defs.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Pure/primitive_defs.ML Fri Mar 06 11:10:57 2009 +0100 @@ -81,7 +81,7 @@ fun mk_defpair (lhs, rhs) = (case Term.head_of lhs of Const (name, _) => - (NameSpace.base name ^ "_def", Logic.mk_equals (lhs, rhs)) + (NameSpace.base_name name ^ "_def", Logic.mk_equals (lhs, rhs)) | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs])); end; diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Pure/sign.ML --- a/src/Pure/sign.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Pure/sign.ML Fri Mar 06 11:10:57 2009 +0100 @@ -14,7 +14,6 @@ consts: Consts.T} val naming_of: theory -> NameSpace.naming val full_name: theory -> binding -> string - val base_name: string -> bstring val full_bname: theory -> bstring -> string val full_bname_path: theory -> string -> bstring -> string val syn_of: theory -> Syntax.syntax @@ -185,7 +184,6 @@ (* naming *) val naming_of = #naming o rep_sg; -val base_name = NameSpace.base; val full_name = NameSpace.full_name o naming_of; fun full_bname thy = NameSpace.full_name (naming_of thy) o Binding.name; diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Pure/term.ML --- a/src/Pure/term.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Pure/term.ML Fri Mar 06 11:10:57 2009 +0100 @@ -490,7 +490,7 @@ fun declare_term_names tm = fold_aterms - (fn Const (a, _) => Name.declare (NameSpace.base a) + (fn Const (a, _) => Name.declare (NameSpace.base_name a) | Free (a, _) => Name.declare a | _ => I) tm #> fold_types declare_typ_names tm; @@ -721,7 +721,7 @@ fun lambda v t = let val x = (case v of - Const (x, _) => NameSpace.base x + Const (x, _) => NameSpace.base_name x | Free (x, _) => x | Var ((x, _), _) => x | _ => Name.uu) @@ -805,8 +805,8 @@ fun close_schematic_term t = let val extra_types = map (fn v => Const ("TYPE", itselfT (TVar v))) (hidden_polymorphism t); - val extra_terms = map Var (rev (add_vars t [])); - in fold_rev lambda (extra_types @ extra_terms) t end; + val extra_terms = map Var (add_vars t []); + in fold lambda (extra_terms @ extra_types) t end; diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Pure/thm.ML --- a/src/Pure/thm.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Pure/thm.ML Fri Mar 06 11:10:57 2009 +0100 @@ -151,7 +151,7 @@ val proof_of: thm -> proof val join_proof: thm -> unit val extern_oracles: theory -> xstring list - val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory + val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory end; structure Thm:> THM = @@ -1698,7 +1698,7 @@ structure Oracles = TheoryDataFun ( - type T = stamp NameSpace.table; + type T = serial NameSpace.table; val empty = NameSpace.empty_table; val copy = I; val extend = I; @@ -1708,13 +1708,12 @@ val extern_oracles = map #1 o NameSpace.extern_table o Oracles.get; -fun add_oracle (bname, oracle) thy = +fun add_oracle (b, oracle) thy = let val naming = Sign.naming_of thy; - val name = NameSpace.full_name naming (Binding.name bname); - val thy' = thy |> Oracles.map (fn (space, tab) => - (NameSpace.declare naming (Binding.name bname) space |> snd, - Symtab.update_new (name, stamp ()) tab handle Symtab.DUP dup => err_dup_ora dup)); + val (name, tab') = NameSpace.bind naming (b, serial ()) (Oracles.get thy) + handle Symtab.DUP _ => err_dup_ora (Binding.str_of b); + val thy' = Oracles.put tab' thy; in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end; end; diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Tools/Compute_Oracle/compute.ML --- a/src/Tools/Compute_Oracle/compute.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Tools/Compute_Oracle/compute.ML Fri Mar 06 11:10:57 2009 +0100 @@ -371,7 +371,7 @@ fun merge_shyps shyps1 shyps2 = Sorttab.keys (add_shyps shyps2 (add_shyps shyps1 Sorttab.empty)) val (_, export_oracle) = Context.>>> (Context.map_theory_result - (Thm.add_oracle ("compute", fn (thy, hyps, shyps, prop) => + (Thm.add_oracle (Binding.name "compute", fn (thy, hyps, shyps, prop) => let val shyptab = add_shyps shyps Sorttab.empty fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Tools/code/code_haskell.ML --- a/src/Tools/code/code_haskell.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Tools/code/code_haskell.ML Fri Mar 06 11:10:57 2009 +0100 @@ -34,7 +34,7 @@ fun pr_haskell_stmt naming labelled_name syntax_class syntax_tyco syntax_const init_syms deresolve is_cons contr_classparam_typs deriving_show = let - val deresolve_base = NameSpace.base o deresolve; + val deresolve_base = NameSpace.base_name o deresolve; fun class_name class = case syntax_class class of NONE => deresolve class | SOME class => class; @@ -143,7 +143,7 @@ @ str "=" :: str "error" @@ (str o (fn s => s ^ ";") o ML_Syntax.print_string - o NameSpace.base o NameSpace.qualifier) name + o NameSpace.base_name o NameSpace.qualifier) name ) ] end @@ -155,7 +155,7 @@ let val consts = map_filter (fn c => if (is_some o syntax_const) c - then NONE else (SOME o NameSpace.base o deresolve) c) + then NONE else (SOME o NameSpace.base_name o deresolve) c) ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []); val vars = init_syms |> Code_Name.intro_vars consts @@ -255,7 +255,7 @@ let val (c_inst_name, (_, tys)) = c_inst; val const = if (is_some o syntax_const) c_inst_name - then NONE else (SOME o NameSpace.base o deresolve) c_inst_name; + then NONE else (SOME o NameSpace.base_name o deresolve) c_inst_name; val proto_rhs = Code_Thingol.eta_expand k (c_inst, []); val (vs, rhs) = unfold_abs_pure proto_rhs; val vars = init_syms @@ -360,7 +360,7 @@ val reserved_names = Code_Name.make_vars reserved_names; fun pr_stmt qualified = pr_haskell_stmt naming labelled_name syntax_class syntax_tyco syntax_const reserved_names - (if qualified then deresolver else NameSpace.base o deresolver) + (if qualified then deresolver else NameSpace.base_name o deresolver) is_cons contr_classparam_typs (if string_classes then deriving_show else K false); fun pr_module name content = @@ -379,7 +379,7 @@ |> map_filter (try deresolver); val qualified = is_none module_name andalso map deresolver stmt_names @ deps' - |> map NameSpace.base + |> map NameSpace.base_name |> has_duplicates (op =); val imports = deps' |> map NameSpace.qualifier diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Tools/code/code_ml.ML --- a/src/Tools/code/code_ml.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Tools/code/code_ml.ML Fri Mar 06 11:10:57 2009 +0100 @@ -47,7 +47,7 @@ let val pr_label_classrel = translate_string (fn "." => "__" | c => c) o NameSpace.qualifier; - val pr_label_classparam = NameSpace.base o NameSpace.qualifier; + val pr_label_classparam = NameSpace.base_name o NameSpace.qualifier; fun pr_dicts fxy ds = let fun pr_dictvar (v, (_, 1)) = Code_Name.first_upper v ^ "_" @@ -163,7 +163,7 @@ fun pr_stmt (MLExc (name, n)) = let val exc_str = - (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name; + (ML_Syntax.print_string o NameSpace.base_name o NameSpace.qualifier) name; in concat ( str (if n = 0 then "val" else "fun") @@ -179,7 +179,7 @@ let val consts = map_filter (fn c => if (is_some o syntax_const) c - then NONE else (SOME o NameSpace.base o deresolve) c) + then NONE else (SOME o NameSpace.base_name o deresolve) c) (Code_Thingol.fold_constnames (insert (op =)) t []); val vars = reserved_names |> Code_Name.intro_vars consts; @@ -204,7 +204,7 @@ let val consts = map_filter (fn c => if (is_some o syntax_const) c - then NONE else (SOME o NameSpace.base o deresolve) c) + then NONE else (SOME o NameSpace.base_name o deresolve) c) ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []); val vars = reserved_names |> Code_Name.intro_vars consts @@ -473,7 +473,7 @@ fun pr_stmt (MLExc (name, n)) = let val exc_str = - (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name; + (ML_Syntax.print_string o NameSpace.base_name o NameSpace.qualifier) name; in concat ( str "let" @@ -488,7 +488,7 @@ let val consts = map_filter (fn c => if (is_some o syntax_const) c - then NONE else (SOME o NameSpace.base o deresolve) c) + then NONE else (SOME o NameSpace.base_name o deresolve) c) (Code_Thingol.fold_constnames (insert (op =)) t []); val vars = reserved_names |> Code_Name.intro_vars consts; @@ -508,7 +508,7 @@ let val consts = map_filter (fn c => if (is_some o syntax_const) c - then NONE else (SOME o NameSpace.base o deresolve) c) + then NONE else (SOME o NameSpace.base_name o deresolve) c) ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []); val vars = reserved_names |> Code_Name.intro_vars consts @@ -524,7 +524,7 @@ let val consts = map_filter (fn c => if (is_some o syntax_const) c - then NONE else (SOME o NameSpace.base o deresolve) c) + then NONE else (SOME o NameSpace.base_name o deresolve) c) ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []); val vars = reserved_names |> Code_Name.intro_vars consts @@ -552,7 +552,7 @@ let val consts = map_filter (fn c => if (is_some o syntax_const) c - then NONE else (SOME o NameSpace.base o deresolve) c) + then NONE else (SOME o NameSpace.base_name o deresolve) c) ((fold o Code_Thingol.fold_constnames) (insert (op =)) (map (snd o fst) eqs) []); val vars = reserved_names diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Tools/code/code_thingol.ML --- a/src/Tools/code/code_thingol.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Tools/code/code_thingol.ML Fri Mar 06 11:10:57 2009 +0100 @@ -246,15 +246,15 @@ in NameSpace.append prefix base end; in -fun namify_class thy = namify thy NameSpace.base thyname_of_class; +fun namify_class thy = namify thy NameSpace.base_name thyname_of_class; fun namify_classrel thy = namify thy (fn (class1, class2) => - NameSpace.base class2 ^ "_" ^ NameSpace.base class1) (fn thy => thyname_of_class thy o fst); + NameSpace.base_name class2 ^ "_" ^ NameSpace.base_name class1) (fn thy => thyname_of_class thy o fst); (*order fits nicely with composed projections*) fun namify_tyco thy "fun" = "Pure.fun" - | namify_tyco thy tyco = namify thy NameSpace.base thyname_of_tyco tyco; + | namify_tyco thy tyco = namify thy NameSpace.base_name thyname_of_tyco tyco; fun namify_instance thy = namify thy (fn (class, tyco) => - NameSpace.base class ^ "_" ^ NameSpace.base tyco) thyname_of_instance; -fun namify_const thy = namify thy NameSpace.base thyname_of_const; + NameSpace.base_name class ^ "_" ^ NameSpace.base_name tyco) thyname_of_instance; +fun namify_const thy = namify thy NameSpace.base_name thyname_of_const; end; (* local *) diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/Tools/nbe.ML --- a/src/Tools/nbe.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/Tools/nbe.ML Fri Mar 06 11:10:57 2009 +0100 @@ -466,7 +466,7 @@ (* evaluation oracle *) val (_, norm_oracle) = Context.>>> (Context.map_theory_result - (Thm.add_oracle ("norm", fn (thy, t, naming, program, vs_ty_t, deps) => + (Thm.add_oracle (Binding.name "norm", fn (thy, t, naming, program, vs_ty_t, deps) => Thm.cterm_of thy (Logic.mk_equals (t, eval thy t naming program vs_ty_t deps))))); fun add_triv_classes thy = diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/ZF/Tools/datatype_package.ML Fri Mar 06 11:10:57 2009 +0100 @@ -74,7 +74,7 @@ Syntax.string_of_term_global thy t); val rec_names = map (#1 o dest_Const) rec_hds - val rec_base_names = map Sign.base_name rec_names + val rec_base_names = map NameSpace.base_name rec_names val big_rec_base_name = space_implode "_" rec_base_names val thy_path = thy |> Sign.add_path big_rec_base_name diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/ZF/Tools/induct_tacs.ML --- a/src/ZF/Tools/induct_tacs.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/ZF/Tools/induct_tacs.ML Fri Mar 06 11:10:57 2009 +0100 @@ -157,7 +157,7 @@ in thy - |> Sign.add_path (Sign.base_name big_rec_name) + |> Sign.add_path (NameSpace.base_name big_rec_name) |> PureThy.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy)) |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy)) diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/ZF/Tools/inductive_package.ML Fri Mar 06 11:10:57 2009 +0100 @@ -80,7 +80,7 @@ val rec_names = map (#1 o dest_Const) rec_hds and (Const(_,recT),rec_params) = strip_comb (hd rec_tms); - val rec_base_names = map Sign.base_name rec_names; + val rec_base_names = map NameSpace.base_name rec_names; val dummy = assert_all Syntax.is_identifier rec_base_names (fn a => "Base name of recursive set not an identifier: " ^ a); @@ -377,7 +377,7 @@ mutual recursion to invariably be a disjoint sum.*) fun mk_predpair rec_tm = let val rec_name = (#1 o dest_Const o head_of) rec_tm - val pfree = Free(pred_name ^ "_" ^ Sign.base_name rec_name, + val pfree = Free(pred_name ^ "_" ^ NameSpace.base_name rec_name, elem_factors ---> FOLogic.oT) val qconcl = List.foldr FOLogic.mk_all diff -r 8f4d5eaa9878 -r 6c74ef5a349f src/ZF/Tools/primrec_package.ML --- a/src/ZF/Tools/primrec_package.ML Fri Mar 06 11:10:18 2009 +0100 +++ b/src/ZF/Tools/primrec_package.ML Fri Mar 06 11:10:57 2009 +0100 @@ -139,7 +139,7 @@ (** make definition **) (*the recursive argument*) - val rec_arg = Free (Name.variant (map #1 (ls@rs)) (Sign.base_name big_rec_name), + val rec_arg = Free (Name.variant (map #1 (ls@rs)) (NameSpace.base_name big_rec_name), Ind_Syntax.iT) val def_tm = Logic.mk_equals @@ -153,7 +153,7 @@ writeln ("primrec def:\n" ^ Syntax.string_of_term_global thy def_tm) else(); - (Sign.base_name fname ^ "_" ^ Sign.base_name big_rec_name ^ "_def", + (NameSpace.base_name fname ^ "_" ^ NameSpace.base_name big_rec_name ^ "_def", def_tm) end; @@ -168,7 +168,7 @@ val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns); val ([def_thm], thy1) = thy - |> Sign.add_path (Sign.base_name fname) + |> Sign.add_path (NameSpace.base_name fname) |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name def)]; val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)