--- a/Admin/Mercurial/isabelle-style.diff Wed Mar 03 08:49:11 2010 -0800
+++ b/Admin/Mercurial/isabelle-style.diff Wed Mar 03 10:40:40 2010 -0800
@@ -1,34 +1,38 @@
-diff -r gitweb/changelogentry.tmpl isabelle/changelogentry.tmpl
-2,8c2
-< <a class="title" href="{url}rev/#node|short#{sessionvars%urlparameter}"><span class="age">#date|age# ago</span>#desc|strip|firstline|escape#<span class="logtags"> {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span></a>
-< </div>
-< <div class="title_text">
-< <div class="log_link">
-< <a href="{url}rev/#node|short#{sessionvars%urlparameter}">changeset</a><br/>
-< </div>
-< <i>#author|obfuscate# [#date|rfc822date#] rev #rev#</i><br/>
----
-> <a class="title" href="{url}rev/#node|short#{sessionvars%urlparameter}"><span class="age">#date|age# ago</span>#author|obfuscate# [#date|rfc822date#] rev #rev#<span class="logtags"> {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span></a>
-12a7,9
-> <div class="files">
-> #files#
-> </div>
-diff -r gitweb/changeset.tmpl isabelle/changeset.tmpl
-19c19
-< <a class="title" href="{url}raw-rev/#node|short#">#desc|strip|escape|firstline# <span class="logtags">{inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span></a>
----
-> <a class="title" href="{url}raw-rev/#node|short#">#desc|strip|escape# <span class="logtags">{inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span></a>
-diff -r gitweb/map isabelle/map
-29c29
-< annotateline = '<tr style="font-family:monospace" class="parity#parity#"><td class="linenr" style="text-align: right;"><a href="#url#annotate/#node|short#/#file|urlescape#{sessionvars%urlparameter}#l{targetline}" title="{node|short}: {desc|escape|firstline}">#author|user#@#rev#</a></td><td><pre><a class="linenr" href="##lineid#" id="#lineid#">#linenumber#</a></pre></td><td><pre>#line|escape#</pre></td></tr>'
----
-> annotateline = '<tr style="font-family:monospace" class="parity#parity#"><td class="linenr" style="text-align: right;"><a href="#url#annotate/#node|short#/#file|urlescape#{sessionvars%urlparameter}#l{targetline}" title="{node|short}: {desc|escape}">#author|user#@#rev#</a></td><td><pre><a class="linenr" href="##lineid#" id="#lineid#">#linenumber#</a></pre></td><td><pre>#line|escape#</pre></td></tr>'
-59,60c59,60
-< shortlogentry = '<tr class="parity#parity#"><td class="age"><i>#date|age# ago</i></td><td><i>#author|person#</i></td><td><a class="list" href="{url}rev/#node|short#{sessionvars%urlparameter}"><b>#desc|strip|firstline|escape#</b> <span class="logtags">{inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span></a></td><td class="link" nowrap><a href="{url}rev/#node|short#{sessionvars%urlparameter}">changeset</a> | <a href="{url}file/#node|short#{sessionvars%urlparameter}">files</a></td></tr>'
-< filelogentry = '<tr class="parity#parity#"><td class="age"><i>#date|age# ago</i></td><td><a class="list" href="{url}rev/#node|short#{sessionvars%urlparameter}"><b>#desc|strip|firstline|escape#</b></a></td><td class="link"><a href="{url}file/#node|short#/#file|urlescape#{sessionvars%urlparameter}">file</a> | <a href="{url}diff/#node|short#/#file|urlescape#{sessionvars%urlparameter}">diff</a> | <a href="{url}annotate/#node|short#/#file|urlescape#{sessionvars%urlparameter}">annotate</a> #rename%filelogrename#</td></tr>'
----
-> shortlogentry = '<tr class="parity#parity#"><td class="age"><i>#date|age# ago</i></td><td><i>#date|shortdate#</i></td><td><i>#author|person#</i></td><td><a class="list" href="{url}rev/#node|short#{sessionvars%urlparameter}"><b>#desc|strip|escape#</b> <span class="logtags">{inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span></a></td><td class="link" nowrap><a href="{url}rev/#node|short#{sessionvars%urlparameter}">changeset</a> | <a href="{url}file/#node|short#{sessionvars%urlparameter}">files</a></td></tr>'
-> filelogentry = '<tr class="parity#parity#"><td class="age"><i>#date|age# ago</i></td><td><i>#date|shortdate#</i></td><td><i>#author|person#</i></td><td><a class="list" href="{url}rev/#node|short#{sessionvars%urlparameter}"><b>#desc|strip|escape#</b></a></td><td class="link"><a href="{url}file/#node|short#/#file|urlescape#{sessionvars%urlparameter}">file</a> | <a href="{url}diff/#node|short#/#file|urlescape#{sessionvars%urlparameter}">diff</a> | <a href="{url}annotate/#node|short#/#file|urlescape#{sessionvars%urlparameter}">annotate</a> #rename%filelogrename#</td></tr>'
-diff -r gitweb/summary.tmpl isabelle/summary.tmpl
-34d33
-< <tr><td>owner</td><td>#owner|obfuscate#</td></tr>
+diff -u gitweb/changelogentry.tmpl isabelle/changelogentry.tmpl
+--- gitweb/changelogentry.tmpl 2010-02-01 16:34:34.000000000 +0100
++++ isabelle/changelogentry.tmpl 2010-03-03 15:12:12.000000000 +0100
+@@ -1,14 +1,12 @@
+ <div>
+-<a class="title" href="{url}rev/{node|short}{sessionvars%urlparameter}"><span class="age">{date|age}</span>{desc|strip|firstline|escape|nonempty}<span class="logtags"> {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span></a>
+-</div>
+-<div class="title_text">
+-<div class="log_link">
+-<a href="{url}rev/{node|short}{sessionvars%urlparameter}">changeset</a><br/>
+-</div>
+-<i>{author|obfuscate} [{date|rfc822date}] rev {rev}</i><br/>
++<a class="title" href="{url}rev/{node|short}{sessionvars%urlparameter}"><span class="age">{date|age}</span>
++{author|obfuscate} [{date|rfc822date}] rev {rev}<span class="logtags"> {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span></a>
+ </div>
+ <div class="log_body">
+ {desc|strip|escape|addbreaks|nonempty}
+ <br/>
++<div class="files">
++{files}
++</div>
+ <br/>
+ </div>
+diff -u gitweb/map isabelle/map
+--- gitweb/map 2010-02-01 16:34:34.000000000 +0100
++++ isabelle/map 2010-03-03 15:13:25.000000000 +0100
+@@ -206,9 +206,10 @@
+ <tr class="parity{parity}">
+ <td class="age"><i>{date|age}</i></td>
+ <td><i>{author|person}</i></td>
++ <td><i>{date|shortdate}</i></td>
+ <td>
+ <a class="list" href="{url}rev/{node|short}{sessionvars%urlparameter}">
+- <b>{desc|strip|firstline|escape|nonempty}</b>
++ <b>{desc|strip|escape|nonempty}</b>
+ <span class="logtags">{inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}</span>
+ </a>
+ </td>
--- a/NEWS Wed Mar 03 08:49:11 2010 -0800
+++ b/NEWS Wed Mar 03 10:40:40 2010 -0800
@@ -6,15 +6,20 @@
*** General ***
-* Authentic syntax for *all* term constants: provides simple and
-robust correspondence between formal entities and concrete syntax.
-Substantial INCOMPATIBILITY concerning low-level syntax translations
-(translation rules and translation functions in ML). Some hints on
-upgrading:
+* Authentic syntax for *all* logical entities (type classes, type
+constructors, term constants): provides simple and robust
+correspondence between formal entities and concrete syntax. Within
+the parse tree / AST representations, "constants" are decorated by
+their category (class, type, const) and spelled out explicitly with
+their full internal name.
+
+Substantial INCOMPATIBILITY concerning low-level syntax declarations
+and translations (translation rules and translation functions in ML).
+Some hints on upgrading:
- Many existing uses of 'syntax' and 'translations' can be replaced
- by more modern 'notation' and 'abbreviation', which are
- independent of this issue.
+ by more modern 'type_notation', 'notation' and 'abbreviation',
+ which are independent of this issue.
- 'translations' require markup within the AST; the term syntax
provides the following special forms:
@@ -27,16 +32,29 @@
system indicates accidental variables via the error "rhs contains
extra variables".
+ Type classes and type constructors are marked according to their
+ concrete syntax. Some old translations rules need to be written
+ for the "type" category, using type constructor application
+ instead of pseudo-term application of the default category
+ "logic".
+
- 'parse_translation' etc. in ML may use the following
antiquotations:
+ @{class_syntax c} -- type class c within parse tree / AST
+ @{term_syntax c} -- type constructor c within parse tree / AST
@{const_syntax c} -- ML version of "CONST c" above
@{syntax_const c} -- literally c (checked wrt. 'syntax' declarations)
+ - Literal types within 'typed_print_translations', i.e. those *not*
+ represented as pseudo-terms are represented verbatim. Use @{class
+ c} or @{type_name c} here instead of the above syntax
+ antiquotations.
+
Note that old non-authentic syntax was based on unqualified base
-names, so all of the above would coincide. Recall that 'print_syntax'
-and ML_command "set Syntax.trace_ast" help to diagnose syntax
-problems.
+names, so all of the above "constant" names would coincide. Recall
+that 'print_syntax' and ML_command "set Syntax.trace_ast" help to
+diagnose syntax problems.
* Type constructors admit general mixfix syntax, not just infix.
--- a/doc-src/Locales/Locales/Examples3.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/doc-src/Locales/Locales/Examples3.thy Wed Mar 03 10:40:40 2010 -0800
@@ -63,7 +63,7 @@
statements:
@{subgoals [display]}
This is Presburger arithmetic, which can be solved by the
- method @{text arith}. *}
+ method @{text arith}. *}
by arith+
txt {* \normalsize In order to show the equations, we put ourselves
in a situation where the lattice theorems can be used in a
--- a/doc-src/Locales/Locales/document/Examples3.tex Wed Mar 03 08:49:11 2010 -0800
+++ b/doc-src/Locales/Locales/document/Examples3.tex Wed Mar 03 10:40:40 2010 -0800
@@ -141,7 +141,7 @@
\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ {\isasymexists}sup{\isasymge}x{\isachardot}\ y\ {\isasymle}\ sup\ {\isasymand}\ {\isacharparenleft}{\isasymforall}z{\isachardot}\ x\ {\isasymle}\ z\ {\isasymand}\ y\ {\isasymle}\ z\ {\isasymlongrightarrow}\ sup\ {\isasymle}\ z{\isacharparenright}%
\end{isabelle}
This is Presburger arithmetic, which can be solved by the
- method \isa{arith}.%
+ method \isa{arith}.%
\end{isamarkuptxt}%
\isamarkuptrue%
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
--- a/src/HOL/Bali/AxSem.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Bali/AxSem.thy Wed Mar 03 10:40:40 2010 -0800
@@ -58,10 +58,9 @@
"\<lambda>Vals:v. b" == "(\<lambda>v. b) \<circ> CONST the_In3"
--{* relation on result values, state and auxiliary variables *}
-types 'a assn = "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
+types 'a assn = "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
translations
- "res" <= (type) "AxSem.res"
- "a assn" <= (type) "vals \<Rightarrow> state \<Rightarrow> a \<Rightarrow> bool"
+ (type) "'a assn" <= (type) "vals \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
definition assn_imp :: "'a assn \<Rightarrow> 'a assn \<Rightarrow> bool" (infixr "\<Rightarrow>" 25) where
"P \<Rightarrow> Q \<equiv> \<forall>Y s Z. P Y s Z \<longrightarrow> Q Y s Z"
--- a/src/HOL/Bali/Basis.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Bali/Basis.thy Wed Mar 03 10:40:40 2010 -0800
@@ -213,11 +213,6 @@
*}
(* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
-translations
- "option"<= (type) "Option.option"
- "list" <= (type) "List.list"
- "sum3" <= (type) "Basis.sum3"
-
section "quantifiers for option type"
--- a/src/HOL/Bali/Decl.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Bali/Decl.thy Wed Mar 03 10:40:40 2010 -0800
@@ -149,24 +149,24 @@
access :: acc_modi
translations
- "decl" <= (type) "\<lparr>access::acc_modi\<rparr>"
- "decl" <= (type) "\<lparr>access::acc_modi,\<dots>::'a\<rparr>"
+ (type) "decl" <= (type) "\<lparr>access::acc_modi\<rparr>"
+ (type) "decl" <= (type) "\<lparr>access::acc_modi,\<dots>::'a\<rparr>"
subsection {* Member (field or method)*}
record member = decl +
static :: stat_modi
translations
- "member" <= (type) "\<lparr>access::acc_modi,static::bool\<rparr>"
- "member" <= (type) "\<lparr>access::acc_modi,static::bool,\<dots>::'a\<rparr>"
+ (type) "member" <= (type) "\<lparr>access::acc_modi,static::bool\<rparr>"
+ (type) "member" <= (type) "\<lparr>access::acc_modi,static::bool,\<dots>::'a\<rparr>"
subsection {* Field *}
record field = member +
type :: ty
translations
- "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty\<rparr>"
- "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty,\<dots>::'a\<rparr>"
+ (type) "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty\<rparr>"
+ (type) "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty,\<dots>::'a\<rparr>"
types
fdecl (* field declaration, cf. 8.3 *)
@@ -174,7 +174,7 @@
translations
- "fdecl" <= (type) "vname \<times> field"
+ (type) "fdecl" <= (type) "vname \<times> field"
subsection {* Method *}
@@ -193,17 +193,17 @@
translations
- "mhead" <= (type) "\<lparr>access::acc_modi, static::bool,
+ (type) "mhead" <= (type) "\<lparr>access::acc_modi, static::bool,
pars::vname list, resT::ty\<rparr>"
- "mhead" <= (type) "\<lparr>access::acc_modi, static::bool,
+ (type) "mhead" <= (type) "\<lparr>access::acc_modi, static::bool,
pars::vname list, resT::ty,\<dots>::'a\<rparr>"
- "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt\<rparr>"
- "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt,\<dots>::'a\<rparr>"
- "methd" <= (type) "\<lparr>access::acc_modi, static::bool,
+ (type) "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt\<rparr>"
+ (type) "mbody" <= (type) "\<lparr>lcls::(vname \<times> ty) list,stmt::stmt,\<dots>::'a\<rparr>"
+ (type) "methd" <= (type) "\<lparr>access::acc_modi, static::bool,
pars::vname list, resT::ty,mbody::mbody\<rparr>"
- "methd" <= (type) "\<lparr>access::acc_modi, static::bool,
+ (type) "methd" <= (type) "\<lparr>access::acc_modi, static::bool,
pars::vname list, resT::ty,mbody::mbody,\<dots>::'a\<rparr>"
- "mdecl" <= (type) "sig \<times> methd"
+ (type) "mdecl" <= (type) "sig \<times> methd"
definition mhead :: "methd \<Rightarrow> mhead" where
@@ -306,13 +306,13 @@
= "qtname \<times> iface"
translations
- "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list\<rparr>"
- "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,\<dots>::'a\<rparr>"
- "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
+ (type) "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list\<rparr>"
+ (type) "ibody" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,\<dots>::'a\<rparr>"
+ (type) "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
isuperIfs::qtname list\<rparr>"
- "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
+ (type) "iface" <= (type) "\<lparr>access::acc_modi,imethods::(sig \<times> mhead) list,
isuperIfs::qtname list,\<dots>::'a\<rparr>"
- "idecl" <= (type) "qtname \<times> iface"
+ (type) "idecl" <= (type) "qtname \<times> iface"
definition ibody :: "iface \<Rightarrow> ibody" where
"ibody i \<equiv> \<lparr>access=access i,imethods=imethods i\<rparr>"
@@ -337,17 +337,17 @@
= "qtname \<times> class"
translations
- "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
+ (type) "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
methods::mdecl list,init::stmt\<rparr>"
- "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
+ (type) "cbody" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
methods::mdecl list,init::stmt,\<dots>::'a\<rparr>"
- "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
+ (type) "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
methods::mdecl list,init::stmt,
super::qtname,superIfs::qtname list\<rparr>"
- "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
+ (type) "class" <= (type) "\<lparr>access::acc_modi,cfields::fdecl list,
methods::mdecl list,init::stmt,
super::qtname,superIfs::qtname list,\<dots>::'a\<rparr>"
- "cdecl" <= (type) "qtname \<times> class"
+ (type) "cdecl" <= (type) "qtname \<times> class"
definition cbody :: "class \<Rightarrow> cbody" where
"cbody c \<equiv> \<lparr>access=access c, cfields=cfields c,methods=methods c,init=init c\<rparr>"
@@ -404,8 +404,8 @@
"classes"::"cdecl list"
translations
- "prog"<= (type) "\<lparr>ifaces::idecl list,classes::cdecl list\<rparr>"
- "prog"<= (type) "\<lparr>ifaces::idecl list,classes::cdecl list,\<dots>::'a\<rparr>"
+ (type) "prog" <= (type) "\<lparr>ifaces::idecl list,classes::cdecl list\<rparr>"
+ (type) "prog" <= (type) "\<lparr>ifaces::idecl list,classes::cdecl list,\<dots>::'a\<rparr>"
abbreviation
iface :: "prog \<Rightarrow> (qtname, iface) table"
--- a/src/HOL/Bali/DeclConcepts.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Bali/DeclConcepts.thy Wed Mar 03 10:40:40 2010 -0800
@@ -1377,7 +1377,7 @@
fspec = "vname \<times> qtname"
translations
- "fspec" <= (type) "vname \<times> qtname"
+ (type) "fspec" <= (type) "vname \<times> qtname"
definition imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
"imethds G I
--- a/src/HOL/Bali/Eval.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Bali/Eval.thy Wed Mar 03 10:40:40 2010 -0800
@@ -99,8 +99,8 @@
types vvar = "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
vals = "(val, vvar, val list) sum3"
translations
- "vvar" <= (type) "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
- "vals" <= (type)"(val, vvar, val list) sum3"
+ (type) "vvar" <= (type) "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
+ (type) "vals" <= (type) "(val, vvar, val list) sum3"
text {* To avoid redundancy and to reduce the number of rules, there is only
one evaluation rule for each syntactic term. This is also true for variables
--- a/src/HOL/Bali/Name.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Bali/Name.thy Wed Mar 03 10:40:40 2010 -0800
@@ -78,11 +78,7 @@
qtname_qtname_def: "qtname (q::'a qtname_ext_type) \<equiv> q"
translations
- "mname" <= "Name.mname"
- "xname" <= "Name.xname"
- "tname" <= "Name.tname"
- "ename" <= "Name.ename"
- "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
+ (type) "qtname" <= (type) "\<lparr>pid::pname,tid::tname\<rparr>"
(type) "'a qtname_scheme" <= (type) "\<lparr>pid::pname,tid::tname,\<dots>::'a\<rparr>"
--- a/src/HOL/Bali/State.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Bali/State.thy Wed Mar 03 10:40:40 2010 -0800
@@ -33,10 +33,10 @@
"values" :: "(vn, val) table"
translations
- "fspec" <= (type) "vname \<times> qtname"
- "vn" <= (type) "fspec + int"
- "obj" <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option\<rparr>"
- "obj" <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option,\<dots>::'a\<rparr>"
+ (type) "fspec" <= (type) "vname \<times> qtname"
+ (type) "vn" <= (type) "fspec + int"
+ (type) "obj" <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option\<rparr>"
+ (type) "obj" <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option,\<dots>::'a\<rparr>"
definition the_Arr :: "obj option \<Rightarrow> ty \<times> int \<times> (vn, val) table" where
"the_Arr obj \<equiv> SOME (T,k,t). obj = Some \<lparr>tag=Arr T k,values=t\<rparr>"
@@ -134,7 +134,7 @@
translations
"Heap" => "CONST Inl"
"Stat" => "CONST Inr"
- "oref" <= (type) "loc + qtname"
+ (type) "oref" <= (type) "loc + qtname"
definition fields_table :: "prog \<Rightarrow> qtname \<Rightarrow> (fspec \<Rightarrow> field \<Rightarrow> bool) \<Rightarrow> (fspec, ty) table" where
"fields_table G C P
@@ -213,9 +213,9 @@
= "(lname, val) table" *) (* defined in Value.thy local variables *)
translations
- "globs" <= (type) "(oref , obj) table"
- "heap" <= (type) "(loc , obj) table"
-(* "locals" <= (type) "(lname, val) table" *)
+ (type) "globs" <= (type) "(oref , obj) table"
+ (type) "heap" <= (type) "(loc , obj) table"
+(* (type) "locals" <= (type) "(lname, val) table" *)
datatype st = (* pure state, i.e. contents of all variables *)
st globs locals
@@ -567,10 +567,8 @@
state = "abopt \<times> st" --{* state including abruption information *}
translations
- "abopt" <= (type) "State.abrupt option"
- "abopt" <= (type) "abrupt option"
- "state" <= (type) "abopt \<times> State.st"
- "state" <= (type) "abopt \<times> st"
+ (type) "abopt" <= (type) "abrupt option"
+ (type) "state" <= (type) "abopt \<times> st"
abbreviation
Norm :: "st \<Rightarrow> state"
--- a/src/HOL/Bali/Table.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Bali/Table.thy Wed Mar 03 10:40:40 2010 -0800
@@ -42,8 +42,7 @@
where "table_of \<equiv> map_of"
translations
- (type)"'a \<rightharpoonup> 'b" <= (type)"'a \<Rightarrow> 'b Datatype.option"
- (type)"('a, 'b) table" <= (type)"'a \<rightharpoonup> 'b"
+ (type) "('a, 'b) table" <= (type) "'a \<rightharpoonup> 'b"
(* ### To map *)
lemma map_add_find_left[simp]:
--- a/src/HOL/Bali/Term.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Bali/Term.thy Wed Mar 03 10:40:40 2010 -0800
@@ -88,7 +88,7 @@
statement *}
translations
- "locals" <= (type) "(lname, val) table"
+ (type) "locals" <= (type) "(lname, val) table"
datatype inv_mode --{* invocation mode for method calls *}
= Static --{* static *}
@@ -100,8 +100,8 @@
parTs::"ty list"
translations
- "sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>"
- "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
+ (type) "sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>"
+ (type) "sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
--{* function codes for unary operations *}
datatype unop = UPlus -- {*{\tt +} unary plus*}
@@ -237,11 +237,8 @@
types "term" = "(expr+stmt,var,expr list) sum3"
translations
- "sig" <= (type) "mname \<times> ty list"
- "var" <= (type) "Term.var"
- "expr" <= (type) "Term.expr"
- "stmt" <= (type) "Term.stmt"
- "term" <= (type) "(expr+stmt,var,expr list) sum3"
+ (type) "sig" <= (type) "mname \<times> ty list"
+ (type) "term" <= (type) "(expr+stmt,var,expr list) sum3"
abbreviation this :: expr
where "this == Acc (LVar This)"
--- a/src/HOL/Bali/Type.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Bali/Type.thy Wed Mar 03 10:40:40 2010 -0800
@@ -30,11 +30,6 @@
= PrimT prim_ty --{* primitive type *}
| RefT ref_ty --{* reference type *}
-translations
- "prim_ty" <= (type) "Type.prim_ty"
- "ref_ty" <= (type) "Type.ref_ty"
- "ty" <= (type) "Type.ty"
-
abbreviation "NT == RefT NullT"
abbreviation "Iface I == RefT (IfaceT I)"
abbreviation "Class C == RefT (ClassT C)"
--- a/src/HOL/Bali/Value.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Bali/Value.thy Wed Mar 03 10:40:40 2010 -0800
@@ -17,9 +17,6 @@
| Addr loc --{* addresses, i.e. locations of objects *}
-translations "val" <= (type) "Term.val"
- "loc" <= (type) "Term.loc"
-
consts the_Bool :: "val \<Rightarrow> bool"
primrec "the_Bool (Bool b) = b"
consts the_Intg :: "val \<Rightarrow> int"
--- a/src/HOL/Bali/WellType.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Bali/WellType.thy Wed Mar 03 10:40:40 2010 -0800
@@ -37,10 +37,10 @@
lcl:: "lenv" --{* local environment *}
translations
- "lenv" <= (type) "(lname, ty) table"
- "lenv" <= (type) "lname \<Rightarrow> ty option"
- "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv\<rparr>"
- "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>"
+ (type) "lenv" <= (type) "(lname, ty) table"
+ (type) "lenv" <= (type) "lname \<Rightarrow> ty option"
+ (type) "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv\<rparr>"
+ (type) "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>"
abbreviation
@@ -238,9 +238,9 @@
section "Typing for terms"
-types tys = "ty + ty list"
+types tys = "ty + ty list"
translations
- "tys" <= (type) "ty + ty list"
+ (type) "tys" <= (type) "ty + ty list"
inductive
--- a/src/HOL/IMPP/Hoare.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/IMPP/Hoare.thy Wed Mar 03 10:40:40 2010 -0800
@@ -18,7 +18,7 @@
types 'a assn = "'a => state => bool"
translations
- "a assn" <= (type)"a => state => bool"
+ (type) "'a assn" <= (type) "'a => state => bool"
definition
state_not_singleton :: bool where
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Wed Mar 03 10:40:40 2010 -0800
@@ -286,14 +286,14 @@
by auto
lemma graph_implies_dom:
- "mrec_graph x y \<Longrightarrow> mrec_dom x"
+ "mrec_graph x y \<Longrightarrow> mrec_dom x"
apply (induct rule:mrec_graph.induct)
apply (rule accpI)
apply (erule mrec_rel.cases)
by simp
lemma f_default: "\<not> mrec_dom (f, g, x, h) \<Longrightarrow> mrec f g x h = (Inr Exn, undefined)"
- unfolding mrec_def
+ unfolding mrec_def
by (rule fundef_default_value[OF mrec_sumC_def graph_implies_dom, of _ _ "(f, g, x, h)", simplified])
lemma f_di_reverse:
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Wed Mar 03 10:40:40 2010 -0800
@@ -27,8 +27,8 @@
[simp del]: "make_llist [] = return Empty"
| "make_llist (x#xs) = do tl \<leftarrow> make_llist xs;
next \<leftarrow> Ref.new tl;
- return (Node x next)
- done"
+ return (Node x next)
+ done"
text {* define traverse using the MREC combinator *}
--- a/src/HOL/IsaMakefile Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/IsaMakefile Wed Mar 03 10:40:40 2010 -0800
@@ -47,6 +47,7 @@
HOL-MicroJava \
HOL-Mirabelle \
HOL-Modelcheck \
+ HOL-Mutabelle \
HOL-NanoJava \
HOL-Nitpick_Examples \
HOL-Nominal-Examples \
--- a/src/HOL/Library/Numeral_Type.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Library/Numeral_Type.thy Wed Mar 03 10:40:40 2010 -0800
@@ -32,7 +32,7 @@
syntax "_type_card" :: "type => nat" ("(1CARD/(1'(_')))")
-translations "CARD(t)" => "CONST card (CONST UNIV \<Colon> t set)"
+translations "CARD('t)" => "CONST card (CONST UNIV \<Colon> 't set)"
typed_print_translation {*
let
--- a/src/HOL/Library/RBT.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Library/RBT.thy Wed Mar 03 10:40:40 2010 -0800
@@ -11,135 +11,151 @@
begin
datatype color = R | B
-datatype ('a,'b)"rbt" = Empty | Tr color "('a,'b)rbt" 'a 'b "('a,'b)rbt"
+datatype ('a, 'b) rbt = Empty | Branch color "('a, 'b) rbt" 'a 'b "('a, 'b) rbt"
+
+lemma rbt_cases:
+ obtains (Empty) "t = Empty"
+ | (Red) l k v r where "t = Branch R l k v r"
+ | (Black) l k v r where "t = Branch B l k v r"
+proof (cases t)
+ case Empty with that show thesis by blast
+next
+ case (Branch c) with that show thesis by (cases c) blast+
+qed
+
+text {* Content of a tree *}
+
+primrec entries
+where
+ "entries Empty = []"
+| "entries (Branch _ l k v r) = entries l @ (k,v) # entries r"
text {* Search tree properties *}
-primrec
- pin_tree :: "'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> bool"
+primrec entry_in_tree :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"
where
- "pin_tree k v Empty = False"
-| "pin_tree k v (Tr c l x y r) = (k = x \<and> v = y \<or> pin_tree k v l \<or> pin_tree k v r)"
+ "entry_in_tree k v Empty = False"
+| "entry_in_tree k v (Branch c l x y r) \<longleftrightarrow> k = x \<and> v = y \<or> entry_in_tree k v l \<or> entry_in_tree k v r"
-primrec
- keys :: "('k,'v) rbt \<Rightarrow> 'k set"
+primrec keys :: "('k, 'v) rbt \<Rightarrow> 'k set"
where
"keys Empty = {}"
-| "keys (Tr _ l k _ r) = { k } \<union> keys l \<union> keys r"
+| "keys (Branch _ l k _ r) = { k } \<union> keys l \<union> keys r"
-lemma pint_keys: "pin_tree k v t \<Longrightarrow> k \<in> keys t" by (induct t) auto
+lemma entry_in_tree_keys:
+ "entry_in_tree k v t \<Longrightarrow> k \<in> keys t"
+ by (induct t) auto
-primrec tlt :: "'a\<Colon>order \<Rightarrow> ('a,'b) rbt \<Rightarrow> bool"
+definition tree_less :: "'a\<Colon>order \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool"
where
- "tlt k Empty = True"
-| "tlt k (Tr c lt kt v rt) = (kt < k \<and> tlt k lt \<and> tlt k rt)"
+ tree_less_prop: "tree_less k t \<longleftrightarrow> (\<forall>x\<in>keys t. x < k)"
+
+abbreviation tree_less_symbol (infix "|\<guillemotleft>" 50)
+where "t |\<guillemotleft> x \<equiv> tree_less x t"
-abbreviation tllt (infix "|\<guillemotleft>" 50)
-where "t |\<guillemotleft> x == tlt x t"
+definition tree_greater :: "'a\<Colon>order \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool" (infix "\<guillemotleft>|" 50)
+where
+ tree_greater_prop: "tree_greater k t = (\<forall>x\<in>keys t. k < x)"
-primrec tgt :: "'a\<Colon>order \<Rightarrow> ('a,'b) rbt \<Rightarrow> bool" (infix "\<guillemotleft>|" 50)
-where
- "tgt k Empty = True"
-| "tgt k (Tr c lt kt v rt) = (k < kt \<and> tgt k lt \<and> tgt k rt)"
+lemma tree_less_simps [simp]:
+ "tree_less k Empty = True"
+ "tree_less k (Branch c lt kt v rt) \<longleftrightarrow> kt < k \<and> tree_less k lt \<and> tree_less k rt"
+ by (auto simp add: tree_less_prop)
-lemma tlt_prop: "(t |\<guillemotleft> k) = (\<forall>x\<in>keys t. x < k)" by (induct t) auto
-lemma tgt_prop: "(k \<guillemotleft>| t) = (\<forall>x\<in>keys t. k < x)" by (induct t) auto
-lemmas tlgt_props = tlt_prop tgt_prop
+lemma tree_greater_simps [simp]:
+ "tree_greater k Empty = True"
+ "tree_greater k (Branch c lt kt v rt) \<longleftrightarrow> k < kt \<and> tree_greater k lt \<and> tree_greater k rt"
+ by (auto simp add: tree_greater_prop)
-lemmas tgt_nit = tgt_prop pint_keys
-lemmas tlt_nit = tlt_prop pint_keys
+lemmas tree_ord_props = tree_less_prop tree_greater_prop
-lemma tlt_trans: "\<lbrakk> t |\<guillemotleft> x; x < y \<rbrakk> \<Longrightarrow> t |\<guillemotleft> y"
- and tgt_trans: "\<lbrakk> x < y; y \<guillemotleft>| t\<rbrakk> \<Longrightarrow> x \<guillemotleft>| t"
-by (auto simp: tlgt_props)
-
+lemmas tree_greater_nit = tree_greater_prop entry_in_tree_keys
+lemmas tree_less_nit = tree_less_prop entry_in_tree_keys
-primrec st :: "('a::linorder, 'b) rbt \<Rightarrow> bool"
-where
- "st Empty = True"
-| "st (Tr c l k v r) = (l |\<guillemotleft> k \<and> k \<guillemotleft>| r \<and> st l \<and> st r)"
+lemma tree_less_trans: "t |\<guillemotleft> x \<Longrightarrow> x < y \<Longrightarrow> t |\<guillemotleft> y"
+ and tree_greater_trans: "x < y \<Longrightarrow> y \<guillemotleft>| t \<Longrightarrow> x \<guillemotleft>| t"
+by (auto simp: tree_ord_props)
-primrec map_of :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b"
+primrec sorted :: "('a::linorder, 'b) rbt \<Rightarrow> bool"
where
- "map_of Empty k = None"
-| "map_of (Tr _ l x y r) k = (if k < x then map_of l k else if x < k then map_of r k else Some y)"
+ "sorted Empty = True"
+| "sorted (Branch c l k v r) = (l |\<guillemotleft> k \<and> k \<guillemotleft>| r \<and> sorted l \<and> sorted r)"
-lemma map_of_tlt[simp]: "t |\<guillemotleft> k \<Longrightarrow> map_of t k = None"
+primrec lookup :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b"
+where
+ "lookup Empty k = None"
+| "lookup (Branch _ l x y r) k = (if k < x then lookup l k else if x < k then lookup r k else Some y)"
+
+lemma lookup_tree_less[simp]: "t |\<guillemotleft> k \<Longrightarrow> lookup t k = None"
by (induct t) auto
-lemma map_of_tgt[simp]: "k \<guillemotleft>| t \<Longrightarrow> map_of t k = None"
+lemma lookup_tree_greater[simp]: "k \<guillemotleft>| t \<Longrightarrow> lookup t k = None"
by (induct t) auto
-lemma mapof_keys: "st t \<Longrightarrow> dom (map_of t) = keys t"
-by (induct t) (auto simp: dom_def tgt_prop tlt_prop)
+lemma lookup_keys: "sorted t \<Longrightarrow> dom (lookup t) = keys t"
+by (induct t) (auto simp: dom_def tree_greater_prop tree_less_prop)
-lemma mapof_pit: "st t \<Longrightarrow> (map_of t k = Some v) = pin_tree k v t"
-by (induct t) (auto simp: tlt_prop tgt_prop pint_keys)
+lemma lookup_pit: "sorted t \<Longrightarrow> (lookup t k = Some v) = entry_in_tree k v t"
+by (induct t) (auto simp: tree_less_prop tree_greater_prop entry_in_tree_keys)
-lemma map_of_Empty: "map_of Empty = empty"
+lemma lookup_Empty: "lookup Empty = empty"
by (rule ext) simp
(* a kind of extensionality *)
-lemma mapof_from_pit:
- assumes st: "st t1" "st t2"
- and eq: "\<And>v. pin_tree (k\<Colon>'a\<Colon>linorder) v t1 = pin_tree k v t2"
- shows "map_of t1 k = map_of t2 k"
-proof (cases "map_of t1 k")
+lemma lookup_from_pit:
+ assumes sorted: "sorted t1" "sorted t2"
+ and eq: "\<And>v. entry_in_tree (k\<Colon>'a\<Colon>linorder) v t1 = entry_in_tree k v t2"
+ shows "lookup t1 k = lookup t2 k"
+proof (cases "lookup t1 k")
case None
- then have "\<And>v. \<not> pin_tree k v t1"
- by (simp add: mapof_pit[symmetric] st)
+ then have "\<And>v. \<not> entry_in_tree k v t1"
+ by (simp add: lookup_pit[symmetric] sorted)
with None show ?thesis
- by (cases "map_of t2 k") (auto simp: mapof_pit st eq)
+ by (cases "lookup t2 k") (auto simp: lookup_pit sorted eq)
next
case (Some a)
then show ?thesis
- apply (cases "map_of t2 k")
- apply (auto simp: mapof_pit st eq)
- by (auto simp add: mapof_pit[symmetric] st Some)
+ apply (cases "lookup t2 k")
+ apply (auto simp: lookup_pit sorted eq)
+ by (auto simp add: lookup_pit[symmetric] sorted Some)
qed
subsection {* Red-black properties *}
-primrec treec :: "('a,'b) rbt \<Rightarrow> color"
+primrec color_of :: "('a, 'b) rbt \<Rightarrow> color"
where
- "treec Empty = B"
-| "treec (Tr c _ _ _ _) = c"
+ "color_of Empty = B"
+| "color_of (Branch c _ _ _ _) = c"
-primrec inv1 :: "('a,'b) rbt \<Rightarrow> bool"
+primrec bheight :: "('a,'b) rbt \<Rightarrow> nat"
+where
+ "bheight Empty = 0"
+| "bheight (Branch c lt k v rt) = (if c = B then Suc (bheight lt) else bheight lt)"
+
+primrec inv1 :: "('a, 'b) rbt \<Rightarrow> bool"
where
"inv1 Empty = True"
-| "inv1 (Tr c lt k v rt) = (inv1 lt \<and> inv1 rt \<and> (c = B \<or> treec lt = B \<and> treec rt = B))"
+| "inv1 (Branch c lt k v rt) \<longleftrightarrow> inv1 lt \<and> inv1 rt \<and> (c = B \<or> color_of lt = B \<and> color_of rt = B)"
-(* Weaker version *)
-primrec inv1l :: "('a,'b) rbt \<Rightarrow> bool"
+primrec inv1l :: "('a, 'b) rbt \<Rightarrow> bool" -- {* Weaker version *}
where
"inv1l Empty = True"
-| "inv1l (Tr c l k v r) = (inv1 l \<and> inv1 r)"
+| "inv1l (Branch c l k v r) = (inv1 l \<and> inv1 r)"
lemma [simp]: "inv1 t \<Longrightarrow> inv1l t" by (cases t) simp+
-primrec bh :: "('a,'b) rbt \<Rightarrow> nat"
-where
- "bh Empty = 0"
-| "bh (Tr c lt k v rt) = (if c = B then Suc (bh lt) else bh lt)"
-
-primrec inv2 :: "('a,'b) rbt \<Rightarrow> bool"
+primrec inv2 :: "('a, 'b) rbt \<Rightarrow> bool"
where
"inv2 Empty = True"
-| "inv2 (Tr c lt k v rt) = (inv2 lt \<and> inv2 rt \<and> bh lt = bh rt)"
+| "inv2 (Branch c lt k v rt) = (inv2 lt \<and> inv2 rt \<and> bheight lt = bheight rt)"
-definition
- "isrbt t = (inv1 t \<and> inv2 t \<and> treec t = B \<and> st t)"
-
-lemma isrbt_st[simp]: "isrbt t \<Longrightarrow> st t" by (simp add: isrbt_def)
+definition is_rbt :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> bool" where
+ "is_rbt t \<longleftrightarrow> inv1 t \<and> inv2 t \<and> color_of t = B \<and> sorted t"
-lemma rbt_cases:
- obtains (Empty) "t = Empty"
- | (Red) l k v r where "t = Tr R l k v r"
- | (Black) l k v r where "t = Tr B l k v r"
-by (cases t, simp) (case_tac "color", auto)
+lemma is_rbt_sorted [simp]:
+ "is_rbt t \<Longrightarrow> sorted t" by (simp add: is_rbt_def)
-theorem Empty_isrbt[simp]: "isrbt Empty"
-unfolding isrbt_def by simp
+theorem Empty_is_rbt [simp]:
+ "is_rbt Empty" by (simp add: is_rbt_def)
subsection {* Insertion *}
@@ -147,80 +163,80 @@
fun (* slow, due to massive case splitting *)
balance :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
where
- "balance (Tr R a w x b) s t (Tr R c y z d) = Tr R (Tr B a w x b) s t (Tr B c y z d)" |
- "balance (Tr R (Tr R a w x b) s t c) y z d = Tr R (Tr B a w x b) s t (Tr B c y z d)" |
- "balance (Tr R a w x (Tr R b s t c)) y z d = Tr R (Tr B a w x b) s t (Tr B c y z d)" |
- "balance a w x (Tr R b s t (Tr R c y z d)) = Tr R (Tr B a w x b) s t (Tr B c y z d)" |
- "balance a w x (Tr R (Tr R b s t c) y z d) = Tr R (Tr B a w x b) s t (Tr B c y z d)" |
- "balance a s t b = Tr B a s t b"
+ "balance (Branch R a w x b) s t (Branch R c y z d) = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
+ "balance (Branch R (Branch R a w x b) s t c) y z d = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
+ "balance (Branch R a w x (Branch R b s t c)) y z d = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
+ "balance a w x (Branch R b s t (Branch R c y z d)) = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
+ "balance a w x (Branch R (Branch R b s t c) y z d) = Branch R (Branch B a w x b) s t (Branch B c y z d)" |
+ "balance a s t b = Branch B a s t b"
lemma balance_inv1: "\<lbrakk>inv1l l; inv1l r\<rbrakk> \<Longrightarrow> inv1 (balance l k v r)"
by (induct l k v r rule: balance.induct) auto
-lemma balance_bh: "bh l = bh r \<Longrightarrow> bh (balance l k v r) = Suc (bh l)"
+lemma balance_bheight: "bheight l = bheight r \<Longrightarrow> bheight (balance l k v r) = Suc (bheight l)"
by (induct l k v r rule: balance.induct) auto
lemma balance_inv2:
- assumes "inv2 l" "inv2 r" "bh l = bh r"
+ assumes "inv2 l" "inv2 r" "bheight l = bheight r"
shows "inv2 (balance l k v r)"
using assms
by (induct l k v r rule: balance.induct) auto
-lemma balance_tgt[simp]: "(v \<guillemotleft>| balance a k x b) = (v \<guillemotleft>| a \<and> v \<guillemotleft>| b \<and> v < k)"
+lemma balance_tree_greater[simp]: "(v \<guillemotleft>| balance a k x b) = (v \<guillemotleft>| a \<and> v \<guillemotleft>| b \<and> v < k)"
by (induct a k x b rule: balance.induct) auto
-lemma balance_tlt[simp]: "(balance a k x b |\<guillemotleft> v) = (a |\<guillemotleft> v \<and> b |\<guillemotleft> v \<and> k < v)"
+lemma balance_tree_less[simp]: "(balance a k x b |\<guillemotleft> v) = (a |\<guillemotleft> v \<and> b |\<guillemotleft> v \<and> k < v)"
by (induct a k x b rule: balance.induct) auto
-lemma balance_st:
+lemma balance_sorted:
fixes k :: "'a::linorder"
- assumes "st l" "st r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
- shows "st (balance l k v r)"
+ assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
+ shows "sorted (balance l k v r)"
using assms proof (induct l k v r rule: balance.induct)
case ("2_2" a x w b y t c z s va vb vd vc)
- hence "y < z \<and> z \<guillemotleft>| Tr B va vb vd vc"
- by (auto simp add: tlgt_props)
- hence "tgt y (Tr B va vb vd vc)" by (blast dest: tgt_trans)
+ hence "y < z \<and> z \<guillemotleft>| Branch B va vb vd vc"
+ by (auto simp add: tree_ord_props)
+ hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
with "2_2" show ?case by simp
next
case ("3_2" va vb vd vc x w b y s c z)
- from "3_2" have "x < y \<and> tlt x (Tr B va vb vd vc)"
- by (simp add: tlt.simps tgt.simps)
- hence "tlt y (Tr B va vb vd vc)" by (blast dest: tlt_trans)
+ from "3_2" have "x < y \<and> tree_less x (Branch B va vb vd vc)"
+ by simp
+ hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
with "3_2" show ?case by simp
next
case ("3_3" x w b y s c z t va vb vd vc)
- from "3_3" have "y < z \<and> tgt z (Tr B va vb vd vc)" by simp
- hence "tgt y (Tr B va vb vd vc)" by (blast dest: tgt_trans)
+ from "3_3" have "y < z \<and> tree_greater z (Branch B va vb vd vc)" by simp
+ hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
with "3_3" show ?case by simp
next
case ("3_4" vd ve vg vf x w b y s c z t va vb vii vc)
- hence "x < y \<and> tlt x (Tr B vd ve vg vf)" by simp
- hence 1: "tlt y (Tr B vd ve vg vf)" by (blast dest: tlt_trans)
- from "3_4" have "y < z \<and> tgt z (Tr B va vb vii vc)" by simp
- hence "tgt y (Tr B va vb vii vc)" by (blast dest: tgt_trans)
+ hence "x < y \<and> tree_less x (Branch B vd ve vg vf)" by simp
+ hence 1: "tree_less y (Branch B vd ve vg vf)" by (blast dest: tree_less_trans)
+ from "3_4" have "y < z \<and> tree_greater z (Branch B va vb vii vc)" by simp
+ hence "tree_greater y (Branch B va vb vii vc)" by (blast dest: tree_greater_trans)
with 1 "3_4" show ?case by simp
next
case ("4_2" va vb vd vc x w b y s c z t dd)
- hence "x < y \<and> tlt x (Tr B va vb vd vc)" by simp
- hence "tlt y (Tr B va vb vd vc)" by (blast dest: tlt_trans)
+ hence "x < y \<and> tree_less x (Branch B va vb vd vc)" by simp
+ hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
with "4_2" show ?case by simp
next
case ("5_2" x w b y s c z t va vb vd vc)
- hence "y < z \<and> tgt z (Tr B va vb vd vc)" by simp
- hence "tgt y (Tr B va vb vd vc)" by (blast dest: tgt_trans)
+ hence "y < z \<and> tree_greater z (Branch B va vb vd vc)" by simp
+ hence "tree_greater y (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
with "5_2" show ?case by simp
next
case ("5_3" va vb vd vc x w b y s c z t)
- hence "x < y \<and> tlt x (Tr B va vb vd vc)" by simp
- hence "tlt y (Tr B va vb vd vc)" by (blast dest: tlt_trans)
+ hence "x < y \<and> tree_less x (Branch B va vb vd vc)" by simp
+ hence "tree_less y (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
with "5_3" show ?case by simp
next
case ("5_4" va vb vg vc x w b y s c z t vd ve vii vf)
- hence "x < y \<and> tlt x (Tr B va vb vg vc)" by simp
- hence 1: "tlt y (Tr B va vb vg vc)" by (blast dest: tlt_trans)
- from "5_4" have "y < z \<and> tgt z (Tr B vd ve vii vf)" by simp
- hence "tgt y (Tr B vd ve vii vf)" by (blast dest: tgt_trans)
+ hence "x < y \<and> tree_less x (Branch B va vb vg vc)" by simp
+ hence 1: "tree_less y (Branch B va vb vg vc)" by (blast dest: tree_less_trans)
+ from "5_4" have "y < z \<and> tree_greater z (Branch B vd ve vii vf)" by simp
+ hence "tree_greater y (Branch B vd ve vii vf)" by (blast dest: tree_greater_trans)
with 1 "5_4" show ?case by simp
qed simp+
@@ -229,62 +245,62 @@
by (induct l k v r rule: balance.induct) auto
lemma balance_pit:
- "pin_tree k x (balance l v y r) = (pin_tree k x l \<or> k = v \<and> x = y \<or> pin_tree k x r)"
+ "entry_in_tree k x (balance l v y r) = (entry_in_tree k x l \<or> k = v \<and> x = y \<or> entry_in_tree k x r)"
by (induct l v y r rule: balance.induct) auto
-lemma map_of_balance[simp]:
+lemma lookup_balance[simp]:
fixes k :: "'a::linorder"
-assumes "st l" "st r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
-shows "map_of (balance l k v r) x = map_of (Tr B l k v r) x"
-by (rule mapof_from_pit) (auto simp:assms balance_pit balance_st)
+assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
+shows "lookup (balance l k v r) x = lookup (Branch B l k v r) x"
+by (rule lookup_from_pit) (auto simp:assms balance_pit balance_sorted)
primrec paint :: "color \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
where
"paint c Empty = Empty"
-| "paint c (Tr _ l k v r) = Tr c l k v r"
+| "paint c (Branch _ l k v r) = Branch c l k v r"
lemma paint_inv1l[simp]: "inv1l t \<Longrightarrow> inv1l (paint c t)" by (cases t) auto
lemma paint_inv1[simp]: "inv1l t \<Longrightarrow> inv1 (paint B t)" by (cases t) auto
lemma paint_inv2[simp]: "inv2 t \<Longrightarrow> inv2 (paint c t)" by (cases t) auto
-lemma paint_treec[simp]: "treec (paint B t) = B" by (cases t) auto
-lemma paint_st[simp]: "st t \<Longrightarrow> st (paint c t)" by (cases t) auto
-lemma paint_pit[simp]: "pin_tree k x (paint c t) = pin_tree k x t" by (cases t) auto
-lemma paint_mapof[simp]: "map_of (paint c t) = map_of t" by (rule ext) (cases t, auto)
-lemma paint_tgt[simp]: "(v \<guillemotleft>| paint c t) = (v \<guillemotleft>| t)" by (cases t) auto
-lemma paint_tlt[simp]: "(paint c t |\<guillemotleft> v) = (t |\<guillemotleft> v)" by (cases t) auto
+lemma paint_color_of[simp]: "color_of (paint B t) = B" by (cases t) auto
+lemma paint_sorted[simp]: "sorted t \<Longrightarrow> sorted (paint c t)" by (cases t) auto
+lemma paint_pit[simp]: "entry_in_tree k x (paint c t) = entry_in_tree k x t" by (cases t) auto
+lemma paint_lookup[simp]: "lookup (paint c t) = lookup t" by (rule ext) (cases t, auto)
+lemma paint_tree_greater[simp]: "(v \<guillemotleft>| paint c t) = (v \<guillemotleft>| t)" by (cases t) auto
+lemma paint_tree_less[simp]: "(paint c t |\<guillemotleft> v) = (t |\<guillemotleft> v)" by (cases t) auto
fun
ins :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
where
- "ins f k v Empty = Tr R Empty k v Empty" |
- "ins f k v (Tr B l x y r) = (if k < x then balance (ins f k v l) x y r
+ "ins f k v Empty = Branch R Empty k v Empty" |
+ "ins f k v (Branch B l x y r) = (if k < x then balance (ins f k v l) x y r
else if k > x then balance l x y (ins f k v r)
- else Tr B l x (f k y v) r)" |
- "ins f k v (Tr R l x y r) = (if k < x then Tr R (ins f k v l) x y r
- else if k > x then Tr R l x y (ins f k v r)
- else Tr R l x (f k y v) r)"
+ else Branch B l x (f k y v) r)" |
+ "ins f k v (Branch R l x y r) = (if k < x then Branch R (ins f k v l) x y r
+ else if k > x then Branch R l x y (ins f k v r)
+ else Branch R l x (f k y v) r)"
lemma ins_inv1_inv2:
assumes "inv1 t" "inv2 t"
- shows "inv2 (ins f k x t)" "bh (ins f k x t) = bh t"
- "treec t = B \<Longrightarrow> inv1 (ins f k x t)" "inv1l (ins f k x t)"
+ shows "inv2 (ins f k x t)" "bheight (ins f k x t) = bheight t"
+ "color_of t = B \<Longrightarrow> inv1 (ins f k x t)" "inv1l (ins f k x t)"
using assms
- by (induct f k x t rule: ins.induct) (auto simp: balance_inv1 balance_inv2 balance_bh)
+ by (induct f k x t rule: ins.induct) (auto simp: balance_inv1 balance_inv2 balance_bheight)
-lemma ins_tgt[simp]: "(v \<guillemotleft>| ins f k x t) = (v \<guillemotleft>| t \<and> k > v)"
+lemma ins_tree_greater[simp]: "(v \<guillemotleft>| ins f k x t) = (v \<guillemotleft>| t \<and> k > v)"
by (induct f k x t rule: ins.induct) auto
-lemma ins_tlt[simp]: "(ins f k x t |\<guillemotleft> v) = (t |\<guillemotleft> v \<and> k < v)"
+lemma ins_tree_less[simp]: "(ins f k x t |\<guillemotleft> v) = (t |\<guillemotleft> v \<and> k < v)"
by (induct f k x t rule: ins.induct) auto
-lemma ins_st[simp]: "st t \<Longrightarrow> st (ins f k x t)"
- by (induct f k x t rule: ins.induct) (auto simp: balance_st)
+lemma ins_sorted[simp]: "sorted t \<Longrightarrow> sorted (ins f k x t)"
+ by (induct f k x t rule: ins.induct) (auto simp: balance_sorted)
lemma keys_ins: "keys (ins f k v t) = { k } \<union> keys t"
by (induct f k v t rule: ins.induct) auto
-lemma map_of_ins:
+lemma lookup_ins:
fixes k :: "'a::linorder"
- assumes "st t"
- shows "map_of (ins f k v t) x = ((map_of t)(k |-> case map_of t k of None \<Rightarrow> v
+ assumes "sorted t"
+ shows "lookup (ins f k v t) x = ((lookup t)(k |-> case lookup t k of None \<Rightarrow> v
| Some w \<Rightarrow> f k w v)) x"
using assms by (induct f k v t rule: ins.induct) auto
@@ -293,98 +309,97 @@
where
"insertwithkey f k v t = paint B (ins f k v t)"
-lemma insertwk_st: "st t \<Longrightarrow> st (insertwithkey f k x t)"
+lemma insertwk_sorted: "sorted t \<Longrightarrow> sorted (insertwithkey f k x t)"
by (auto simp: insertwithkey_def)
-theorem insertwk_isrbt:
- assumes inv: "isrbt t"
- shows "isrbt (insertwithkey f k x t)"
+theorem insertwk_is_rbt:
+ assumes inv: "is_rbt t"
+ shows "is_rbt (insertwithkey f k x t)"
using assms
-unfolding insertwithkey_def isrbt_def
+unfolding insertwithkey_def is_rbt_def
by (auto simp: ins_inv1_inv2)
-lemma map_of_insertwk:
- assumes "st t"
- shows "map_of (insertwithkey f k v t) x = ((map_of t)(k |-> case map_of t k of None \<Rightarrow> v
+lemma lookup_insertwk:
+ assumes "sorted t"
+ shows "lookup (insertwithkey f k v t) x = ((lookup t)(k |-> case lookup t k of None \<Rightarrow> v
| Some w \<Rightarrow> f k w v)) x"
unfolding insertwithkey_def using assms
-by (simp add:map_of_ins)
+by (simp add:lookup_ins)
definition
insertw_def: "insertwith f = insertwithkey (\<lambda>_. f)"
-lemma insertw_st: "st t \<Longrightarrow> st (insertwith f k v t)" by (simp add: insertwk_st insertw_def)
-theorem insertw_isrbt: "isrbt t \<Longrightarrow> isrbt (insertwith f k v t)" by (simp add: insertwk_isrbt insertw_def)
+lemma insertw_sorted: "sorted t \<Longrightarrow> sorted (insertwith f k v t)" by (simp add: insertwk_sorted insertw_def)
+theorem insertw_is_rbt: "is_rbt t \<Longrightarrow> is_rbt (insertwith f k v t)" by (simp add: insertwk_is_rbt insertw_def)
-lemma map_of_insertw:
- assumes "isrbt t"
- shows "map_of (insertwith f k v t) = (map_of t)(k \<mapsto> (if k:dom (map_of t) then f (the (map_of t k)) v else v))"
+lemma lookup_insertw:
+ assumes "is_rbt t"
+ shows "lookup (insertwith f k v t) = (lookup t)(k \<mapsto> (if k:dom (lookup t) then f (the (lookup t k)) v else v))"
using assms
unfolding insertw_def
-by (rule_tac ext) (cases "map_of t k", auto simp:map_of_insertwk dom_def)
-
+by (rule_tac ext) (cases "lookup t k", auto simp:lookup_insertwk dom_def)
-definition
- "insrt k v t = insertwithkey (\<lambda>_ _ nv. nv) k v t"
+definition insert :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
+ "insert k v t = insertwithkey (\<lambda>_ _ nv. nv) k v t"
-lemma insrt_st: "st t \<Longrightarrow> st (insrt k v t)" by (simp add: insertwk_st insrt_def)
-theorem insrt_isrbt: "isrbt t \<Longrightarrow> isrbt (insrt k v t)" by (simp add: insertwk_isrbt insrt_def)
+lemma insert_sorted: "sorted t \<Longrightarrow> sorted (insert k v t)" by (simp add: insertwk_sorted insert_def)
+theorem insert_is_rbt: "is_rbt t \<Longrightarrow> is_rbt (insert k v t)" by (simp add: insertwk_is_rbt insert_def)
-lemma map_of_insert:
- assumes "isrbt t"
- shows "map_of (insrt k v t) = (map_of t)(k\<mapsto>v)"
-unfolding insrt_def
+lemma lookup_insert:
+ assumes "is_rbt t"
+ shows "lookup (insert k v t) = (lookup t)(k\<mapsto>v)"
+unfolding insert_def
using assms
-by (rule_tac ext) (simp add: map_of_insertwk split:option.split)
+by (rule_tac ext) (simp add: lookup_insertwk split:option.split)
subsection {* Deletion *}
-lemma bh_paintR'[simp]: "treec t = B \<Longrightarrow> bh (paint R t) = bh t - 1"
+lemma bheight_paintR'[simp]: "color_of t = B \<Longrightarrow> bheight (paint R t) = bheight t - 1"
by (cases t rule: rbt_cases) auto
fun
balleft :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
where
- "balleft (Tr R a k x b) s y c = Tr R (Tr B a k x b) s y c" |
- "balleft bl k x (Tr B a s y b) = balance bl k x (Tr R a s y b)" |
- "balleft bl k x (Tr R (Tr B a s y b) t z c) = Tr R (Tr B bl k x a) s y (balance b t z (paint R c))" |
+ "balleft (Branch R a k x b) s y c = Branch R (Branch B a k x b) s y c" |
+ "balleft bl k x (Branch B a s y b) = balance bl k x (Branch R a s y b)" |
+ "balleft bl k x (Branch R (Branch B a s y b) t z c) = Branch R (Branch B bl k x a) s y (balance b t z (paint R c))" |
"balleft t k x s = Empty"
lemma balleft_inv2_with_inv1:
- assumes "inv2 lt" "inv2 rt" "bh lt + 1 = bh rt" "inv1 rt"
- shows "bh (balleft lt k v rt) = bh lt + 1"
+ assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "inv1 rt"
+ shows "bheight (balleft lt k v rt) = bheight lt + 1"
and "inv2 (balleft lt k v rt)"
using assms
-by (induct lt k v rt rule: balleft.induct) (auto simp: balance_inv2 balance_bh)
+by (induct lt k v rt rule: balleft.induct) (auto simp: balance_inv2 balance_bheight)
lemma balleft_inv2_app:
- assumes "inv2 lt" "inv2 rt" "bh lt + 1 = bh rt" "treec rt = B"
+ assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "color_of rt = B"
shows "inv2 (balleft lt k v rt)"
- "bh (balleft lt k v rt) = bh rt"
+ "bheight (balleft lt k v rt) = bheight rt"
using assms
-by (induct lt k v rt rule: balleft.induct) (auto simp add: balance_inv2 balance_bh)+
+by (induct lt k v rt rule: balleft.induct) (auto simp add: balance_inv2 balance_bheight)+
-lemma balleft_inv1: "\<lbrakk>inv1l a; inv1 b; treec b = B\<rbrakk> \<Longrightarrow> inv1 (balleft a k x b)"
+lemma balleft_inv1: "\<lbrakk>inv1l a; inv1 b; color_of b = B\<rbrakk> \<Longrightarrow> inv1 (balleft a k x b)"
by (induct a k x b rule: balleft.induct) (simp add: balance_inv1)+
lemma balleft_inv1l: "\<lbrakk> inv1l lt; inv1 rt \<rbrakk> \<Longrightarrow> inv1l (balleft lt k x rt)"
by (induct lt k x rt rule: balleft.induct) (auto simp: balance_inv1)
-lemma balleft_st: "\<lbrakk> st l; st r; tlt k l; tgt k r \<rbrakk> \<Longrightarrow> st (balleft l k v r)"
+lemma balleft_sorted: "\<lbrakk> sorted l; sorted r; tree_less k l; tree_greater k r \<rbrakk> \<Longrightarrow> sorted (balleft l k v r)"
apply (induct l k v r rule: balleft.induct)
-apply (auto simp: balance_st)
-apply (unfold tgt_prop tlt_prop)
+apply (auto simp: balance_sorted)
+apply (unfold tree_greater_prop tree_less_prop)
by force+
-lemma balleft_tgt:
+lemma balleft_tree_greater:
fixes k :: "'a::order"
assumes "k \<guillemotleft>| a" "k \<guillemotleft>| b" "k < x"
shows "k \<guillemotleft>| balleft a x t b"
using assms
by (induct a x t b rule: balleft.induct) auto
-lemma balleft_tlt:
+lemma balleft_tree_less:
fixes k :: "'a::order"
assumes "a |\<guillemotleft> k" "b |\<guillemotleft> k" "x < k"
shows "balleft a x t b |\<guillemotleft> k"
@@ -392,52 +407,52 @@
by (induct a x t b rule: balleft.induct) auto
lemma balleft_pit:
- assumes "inv1l l" "inv1 r" "bh l + 1 = bh r"
- shows "pin_tree k v (balleft l a b r) = (pin_tree k v l \<or> k = a \<and> v = b \<or> pin_tree k v r)"
+ assumes "inv1l l" "inv1 r" "bheight l + 1 = bheight r"
+ shows "entry_in_tree k v (balleft l a b r) = (entry_in_tree k v l \<or> k = a \<and> v = b \<or> entry_in_tree k v r)"
using assms
by (induct l k v r rule: balleft.induct) (auto simp: balance_pit)
fun
balright :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
where
- "balright a k x (Tr R b s y c) = Tr R a k x (Tr B b s y c)" |
- "balright (Tr B a k x b) s y bl = balance (Tr R a k x b) s y bl" |
- "balright (Tr R a k x (Tr B b s y c)) t z bl = Tr R (balance (paint R a) k x b) s y (Tr B c t z bl)" |
+ "balright a k x (Branch R b s y c) = Branch R a k x (Branch B b s y c)" |
+ "balright (Branch B a k x b) s y bl = balance (Branch R a k x b) s y bl" |
+ "balright (Branch R a k x (Branch B b s y c)) t z bl = Branch R (balance (paint R a) k x b) s y (Branch B c t z bl)" |
"balright t k x s = Empty"
lemma balright_inv2_with_inv1:
- assumes "inv2 lt" "inv2 rt" "bh lt = bh rt + 1" "inv1 lt"
- shows "inv2 (balright lt k v rt) \<and> bh (balright lt k v rt) = bh lt"
+ assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt + 1" "inv1 lt"
+ shows "inv2 (balright lt k v rt) \<and> bheight (balright lt k v rt) = bheight lt"
using assms
-by (induct lt k v rt rule: balright.induct) (auto simp: balance_inv2 balance_bh)
+by (induct lt k v rt rule: balright.induct) (auto simp: balance_inv2 balance_bheight)
-lemma balright_inv1: "\<lbrakk>inv1 a; inv1l b; treec a = B\<rbrakk> \<Longrightarrow> inv1 (balright a k x b)"
+lemma balright_inv1: "\<lbrakk>inv1 a; inv1l b; color_of a = B\<rbrakk> \<Longrightarrow> inv1 (balright a k x b)"
by (induct a k x b rule: balright.induct) (simp add: balance_inv1)+
lemma balright_inv1l: "\<lbrakk> inv1 lt; inv1l rt \<rbrakk> \<Longrightarrow>inv1l (balright lt k x rt)"
by (induct lt k x rt rule: balright.induct) (auto simp: balance_inv1)
-lemma balright_st: "\<lbrakk> st l; st r; tlt k l; tgt k r \<rbrakk> \<Longrightarrow> st (balright l k v r)"
+lemma balright_sorted: "\<lbrakk> sorted l; sorted r; tree_less k l; tree_greater k r \<rbrakk> \<Longrightarrow> sorted (balright l k v r)"
apply (induct l k v r rule: balright.induct)
-apply (auto simp:balance_st)
-apply (unfold tlt_prop tgt_prop)
+apply (auto simp:balance_sorted)
+apply (unfold tree_less_prop tree_greater_prop)
by force+
-lemma balright_tgt:
+lemma balright_tree_greater:
fixes k :: "'a::order"
assumes "k \<guillemotleft>| a" "k \<guillemotleft>| b" "k < x"
shows "k \<guillemotleft>| balright a x t b"
using assms by (induct a x t b rule: balright.induct) auto
-lemma balright_tlt:
+lemma balright_tree_less:
fixes k :: "'a::order"
assumes "a |\<guillemotleft> k" "b |\<guillemotleft> k" "x < k"
shows "balright a x t b |\<guillemotleft> k"
using assms by (induct a x t b rule: balright.induct) auto
lemma balright_pit:
- assumes "inv1 l" "inv1l r" "bh l = bh r + 1" "inv2 l" "inv2 r"
- shows "pin_tree x y (balright l k v r) = (pin_tree x y l \<or> x = k \<and> y = v \<or> pin_tree x y r)"
+ assumes "inv1 l" "inv1l r" "bheight l = bheight r + 1" "inv2 l" "inv2 r"
+ shows "entry_in_tree x y (balright l k v r) = (entry_in_tree x y l \<or> x = k \<and> y = v \<or> entry_in_tree x y r)"
using assms by (induct l k v r rule: balright.induct) (auto simp: balance_pit)
@@ -448,50 +463,50 @@
where
"app Empty x = x"
| "app x Empty = x"
-| "app (Tr R a k x b) (Tr R c s y d) = (case (app b c) of
- Tr R b2 t z c2 \<Rightarrow> (Tr R (Tr R a k x b2) t z (Tr R c2 s y d)) |
- bc \<Rightarrow> Tr R a k x (Tr R bc s y d))"
-| "app (Tr B a k x b) (Tr B c s y d) = (case (app b c) of
- Tr R b2 t z c2 \<Rightarrow> Tr R (Tr B a k x b2) t z (Tr B c2 s y d) |
- bc \<Rightarrow> balleft a k x (Tr B bc s y d))"
-| "app a (Tr R b k x c) = Tr R (app a b) k x c"
-| "app (Tr R a k x b) c = Tr R a k x (app b c)"
+| "app (Branch R a k x b) (Branch R c s y d) = (case (app b c) of
+ Branch R b2 t z c2 \<Rightarrow> (Branch R (Branch R a k x b2) t z (Branch R c2 s y d)) |
+ bc \<Rightarrow> Branch R a k x (Branch R bc s y d))"
+| "app (Branch B a k x b) (Branch B c s y d) = (case (app b c) of
+ Branch R b2 t z c2 \<Rightarrow> Branch R (Branch B a k x b2) t z (Branch B c2 s y d) |
+ bc \<Rightarrow> balleft a k x (Branch B bc s y d))"
+| "app a (Branch R b k x c) = Branch R (app a b) k x c"
+| "app (Branch R a k x b) c = Branch R a k x (app b c)"
lemma app_inv2:
- assumes "inv2 lt" "inv2 rt" "bh lt = bh rt"
- shows "bh (app lt rt) = bh lt" "inv2 (app lt rt)"
+ assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt"
+ shows "bheight (app lt rt) = bheight lt" "inv2 (app lt rt)"
using assms
by (induct lt rt rule: app.induct)
(auto simp: balleft_inv2_app split: rbt.splits color.splits)
lemma app_inv1:
assumes "inv1 lt" "inv1 rt"
- shows "treec lt = B \<Longrightarrow> treec rt = B \<Longrightarrow> inv1 (app lt rt)"
+ shows "color_of lt = B \<Longrightarrow> color_of rt = B \<Longrightarrow> inv1 (app lt rt)"
"inv1l (app lt rt)"
using assms
by (induct lt rt rule: app.induct)
(auto simp: balleft_inv1 split: rbt.splits color.splits)
-lemma app_tgt[simp]:
+lemma app_tree_greater[simp]:
fixes k :: "'a::linorder"
assumes "k \<guillemotleft>| l" "k \<guillemotleft>| r"
shows "k \<guillemotleft>| app l r"
using assms
by (induct l r rule: app.induct)
- (auto simp: balleft_tgt split:rbt.splits color.splits)
+ (auto simp: balleft_tree_greater split:rbt.splits color.splits)
-lemma app_tlt[simp]:
+lemma app_tree_less[simp]:
fixes k :: "'a::linorder"
assumes "l |\<guillemotleft> k" "r |\<guillemotleft> k"
shows "app l r |\<guillemotleft> k"
using assms
by (induct l r rule: app.induct)
- (auto simp: balleft_tlt split:rbt.splits color.splits)
+ (auto simp: balleft_tree_less split:rbt.splits color.splits)
-lemma app_st:
+lemma app_sorted:
fixes k :: "'a::linorder"
- assumes "st l" "st r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
- shows "st (app l r)"
+ assumes "sorted l" "sorted r" "l |\<guillemotleft> k" "k \<guillemotleft>| r"
+ shows "sorted (app l r)"
using assms proof (induct l r rule: app.induct)
case (3 a x v b c y w d)
hence ineqs: "a |\<guillemotleft> x" "x \<guillemotleft>| b" "b |\<guillemotleft> k" "k \<guillemotleft>| c" "c |\<guillemotleft> y" "y \<guillemotleft>| d"
@@ -500,55 +515,55 @@
show ?case
apply (cases "app b c" rule: rbt_cases)
apply auto
- by (metis app_tgt app_tlt ineqs ineqs tlt.simps(2) tgt.simps(2) tgt_trans tlt_trans)+
+ by (metis app_tree_greater app_tree_less ineqs ineqs tree_less_simps(2) tree_greater_simps(2) tree_greater_trans tree_less_trans)+
next
case (4 a x v b c y w d)
- hence "x < k \<and> tgt k c" by simp
- hence "tgt x c" by (blast dest: tgt_trans)
- with 4 have 2: "tgt x (app b c)" by (simp add: app_tgt)
- from 4 have "k < y \<and> tlt k b" by simp
- hence "tlt y b" by (blast dest: tlt_trans)
- with 4 have 3: "tlt y (app b c)" by (simp add: app_tlt)
+ hence "x < k \<and> tree_greater k c" by simp
+ hence "tree_greater x c" by (blast dest: tree_greater_trans)
+ with 4 have 2: "tree_greater x (app b c)" by (simp add: app_tree_greater)
+ from 4 have "k < y \<and> tree_less k b" by simp
+ hence "tree_less y b" by (blast dest: tree_less_trans)
+ with 4 have 3: "tree_less y (app b c)" by (simp add: app_tree_less)
show ?case
proof (cases "app b c" rule: rbt_cases)
case Empty
- from 4 have "x < y \<and> tgt y d" by auto
- hence "tgt x d" by (blast dest: tgt_trans)
- with 4 Empty have "st a" and "st (Tr B Empty y w d)" and "tlt x a" and "tgt x (Tr B Empty y w d)" by auto
- with Empty show ?thesis by (simp add: balleft_st)
+ from 4 have "x < y \<and> tree_greater y d" by auto
+ hence "tree_greater x d" by (blast dest: tree_greater_trans)
+ with 4 Empty have "sorted a" and "sorted (Branch B Empty y w d)" and "tree_less x a" and "tree_greater x (Branch B Empty y w d)" by auto
+ with Empty show ?thesis by (simp add: balleft_sorted)
next
case (Red lta va ka rta)
- with 2 4 have "x < va \<and> tlt x a" by simp
- hence 5: "tlt va a" by (blast dest: tlt_trans)
- from Red 3 4 have "va < y \<and> tgt y d" by simp
- hence "tgt va d" by (blast dest: tgt_trans)
+ with 2 4 have "x < va \<and> tree_less x a" by simp
+ hence 5: "tree_less va a" by (blast dest: tree_less_trans)
+ from Red 3 4 have "va < y \<and> tree_greater y d" by simp
+ hence "tree_greater va d" by (blast dest: tree_greater_trans)
with Red 2 3 4 5 show ?thesis by simp
next
case (Black lta va ka rta)
- from 4 have "x < y \<and> tgt y d" by auto
- hence "tgt x d" by (blast dest: tgt_trans)
- with Black 2 3 4 have "st a" and "st (Tr B (app b c) y w d)" and "tlt x a" and "tgt x (Tr B (app b c) y w d)" by auto
- with Black show ?thesis by (simp add: balleft_st)
+ from 4 have "x < y \<and> tree_greater y d" by auto
+ hence "tree_greater x d" by (blast dest: tree_greater_trans)
+ with Black 2 3 4 have "sorted a" and "sorted (Branch B (app b c) y w d)" and "tree_less x a" and "tree_greater x (Branch B (app b c) y w d)" by auto
+ with Black show ?thesis by (simp add: balleft_sorted)
qed
next
case (5 va vb vd vc b x w c)
- hence "k < x \<and> tlt k (Tr B va vb vd vc)" by simp
- hence "tlt x (Tr B va vb vd vc)" by (blast dest: tlt_trans)
- with 5 show ?case by (simp add: app_tlt)
+ hence "k < x \<and> tree_less k (Branch B va vb vd vc)" by simp
+ hence "tree_less x (Branch B va vb vd vc)" by (blast dest: tree_less_trans)
+ with 5 show ?case by (simp add: app_tree_less)
next
case (6 a x v b va vb vd vc)
- hence "x < k \<and> tgt k (Tr B va vb vd vc)" by simp
- hence "tgt x (Tr B va vb vd vc)" by (blast dest: tgt_trans)
- with 6 show ?case by (simp add: app_tgt)
+ hence "x < k \<and> tree_greater k (Branch B va vb vd vc)" by simp
+ hence "tree_greater x (Branch B va vb vd vc)" by (blast dest: tree_greater_trans)
+ with 6 show ?case by (simp add: app_tree_greater)
qed simp+
lemma app_pit:
- assumes "inv2 l" "inv2 r" "bh l = bh r" "inv1 l" "inv1 r"
- shows "pin_tree k v (app l r) = (pin_tree k v l \<or> pin_tree k v r)"
+ assumes "inv2 l" "inv2 r" "bheight l = bheight r" "inv1 l" "inv1 r"
+ shows "entry_in_tree k v (app l r) = (entry_in_tree k v l \<or> entry_in_tree k v r)"
using assms
proof (induct l r rule: app.induct)
case (4 _ _ _ b c)
- hence a: "bh (app b c) = bh b" by (simp add: app_inv2)
+ hence a: "bheight (app b c) = bheight b" by (simp add: app_inv2)
from 4 have b: "inv1l (app b c)" by (simp add: app_inv1)
show ?case
@@ -570,21 +585,21 @@
del :: "('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
where
"del x Empty = Empty" |
- "del x (Tr c a y s b) = (if x < y then delformLeft x a y s b else (if x > y then delformRight x a y s b else app a b))" |
- "delformLeft x (Tr B lt z v rt) y s b = balleft (del x (Tr B lt z v rt)) y s b" |
- "delformLeft x a y s b = Tr R (del x a) y s b" |
- "delformRight x a y s (Tr B lt z v rt) = balright a y s (del x (Tr B lt z v rt))" |
- "delformRight x a y s b = Tr R a y s (del x b)"
+ "del x (Branch c a y s b) = (if x < y then delformLeft x a y s b else (if x > y then delformRight x a y s b else app a b))" |
+ "delformLeft x (Branch B lt z v rt) y s b = balleft (del x (Branch B lt z v rt)) y s b" |
+ "delformLeft x a y s b = Branch R (del x a) y s b" |
+ "delformRight x a y s (Branch B lt z v rt) = balright a y s (del x (Branch B lt z v rt))" |
+ "delformRight x a y s b = Branch R a y s (del x b)"
lemma
assumes "inv2 lt" "inv1 lt"
shows
- "\<lbrakk>inv2 rt; bh lt = bh rt; inv1 rt\<rbrakk> \<Longrightarrow>
- inv2 (delformLeft x lt k v rt) \<and> bh (delformLeft x lt k v rt) = bh lt \<and> (treec lt = B \<and> treec rt = B \<and> inv1 (delformLeft x lt k v rt) \<or> (treec lt \<noteq> B \<or> treec rt \<noteq> B) \<and> inv1l (delformLeft x lt k v rt))"
- and "\<lbrakk>inv2 rt; bh lt = bh rt; inv1 rt\<rbrakk> \<Longrightarrow>
- inv2 (delformRight x lt k v rt) \<and> bh (delformRight x lt k v rt) = bh lt \<and> (treec lt = B \<and> treec rt = B \<and> inv1 (delformRight x lt k v rt) \<or> (treec lt \<noteq> B \<or> treec rt \<noteq> B) \<and> inv1l (delformRight x lt k v rt))"
- and del_inv1_inv2: "inv2 (del x lt) \<and> (treec lt = R \<and> bh (del x lt) = bh lt \<and> inv1 (del x lt)
- \<or> treec lt = B \<and> bh (del x lt) = bh lt - 1 \<and> inv1l (del x lt))"
+ "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
+ inv2 (delformLeft x lt k v rt) \<and> bheight (delformLeft x lt k v rt) = bheight lt \<and> (color_of lt = B \<and> color_of rt = B \<and> inv1 (delformLeft x lt k v rt) \<or> (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (delformLeft x lt k v rt))"
+ and "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
+ inv2 (delformRight x lt k v rt) \<and> bheight (delformRight x lt k v rt) = bheight lt \<and> (color_of lt = B \<and> color_of rt = B \<and> inv1 (delformRight x lt k v rt) \<or> (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (delformRight x lt k v rt))"
+ and del_inv1_inv2: "inv2 (del x lt) \<and> (color_of lt = R \<and> bheight (del x lt) = bheight lt \<and> inv1 (del x lt)
+ \<or> color_of lt = B \<and> bheight (del x lt) = bheight lt - 1 \<and> inv1l (del x lt))"
using assms
proof (induct x lt k v rt and x lt k v rt and x lt rule: delformLeft_delformRight_del.induct)
case (2 y c _ y')
@@ -601,55 +616,55 @@
qed
next
case (3 y lt z v rta y' ss bb)
- thus ?case by (cases "treec (Tr B lt z v rta) = B \<and> treec bb = B") (simp add: balleft_inv2_with_inv1 balleft_inv1 balleft_inv1l)+
+ thus ?case by (cases "color_of (Branch B lt z v rta) = B \<and> color_of bb = B") (simp add: balleft_inv2_with_inv1 balleft_inv1 balleft_inv1l)+
next
case (5 y a y' ss lt z v rta)
- thus ?case by (cases "treec a = B \<and> treec (Tr B lt z v rta) = B") (simp add: balright_inv2_with_inv1 balright_inv1 balright_inv1l)+
+ thus ?case by (cases "color_of a = B \<and> color_of (Branch B lt z v rta) = B") (simp add: balright_inv2_with_inv1 balright_inv1 balright_inv1l)+
next
- case ("6_1" y a y' ss) thus ?case by (cases "treec a = B \<and> treec Empty = B") simp+
+ case ("6_1" y a y' ss) thus ?case by (cases "color_of a = B \<and> color_of Empty = B") simp+
qed auto
lemma
- delformLeft_tlt: "\<lbrakk>tlt v lt; tlt v rt; k < v\<rbrakk> \<Longrightarrow> tlt v (delformLeft x lt k y rt)"
- and delformRight_tlt: "\<lbrakk>tlt v lt; tlt v rt; k < v\<rbrakk> \<Longrightarrow> tlt v (delformRight x lt k y rt)"
- and del_tlt: "tlt v lt \<Longrightarrow> tlt v (del x lt)"
+ delformLeft_tree_less: "\<lbrakk>tree_less v lt; tree_less v rt; k < v\<rbrakk> \<Longrightarrow> tree_less v (delformLeft x lt k y rt)"
+ and delformRight_tree_less: "\<lbrakk>tree_less v lt; tree_less v rt; k < v\<rbrakk> \<Longrightarrow> tree_less v (delformRight x lt k y rt)"
+ and del_tree_less: "tree_less v lt \<Longrightarrow> tree_less v (del x lt)"
by (induct x lt k y rt and x lt k y rt and x lt rule: delformLeft_delformRight_del.induct)
- (auto simp: balleft_tlt balright_tlt)
+ (auto simp: balleft_tree_less balright_tree_less)
-lemma delformLeft_tgt: "\<lbrakk>tgt v lt; tgt v rt; k > v\<rbrakk> \<Longrightarrow> tgt v (delformLeft x lt k y rt)"
- and delformRight_tgt: "\<lbrakk>tgt v lt; tgt v rt; k > v\<rbrakk> \<Longrightarrow> tgt v (delformRight x lt k y rt)"
- and del_tgt: "tgt v lt \<Longrightarrow> tgt v (del x lt)"
+lemma delformLeft_tree_greater: "\<lbrakk>tree_greater v lt; tree_greater v rt; k > v\<rbrakk> \<Longrightarrow> tree_greater v (delformLeft x lt k y rt)"
+ and delformRight_tree_greater: "\<lbrakk>tree_greater v lt; tree_greater v rt; k > v\<rbrakk> \<Longrightarrow> tree_greater v (delformRight x lt k y rt)"
+ and del_tree_greater: "tree_greater v lt \<Longrightarrow> tree_greater v (del x lt)"
by (induct x lt k y rt and x lt k y rt and x lt rule: delformLeft_delformRight_del.induct)
- (auto simp: balleft_tgt balright_tgt)
+ (auto simp: balleft_tree_greater balright_tree_greater)
-lemma "\<lbrakk>st lt; st rt; tlt k lt; tgt k rt\<rbrakk> \<Longrightarrow> st (delformLeft x lt k y rt)"
- and "\<lbrakk>st lt; st rt; tlt k lt; tgt k rt\<rbrakk> \<Longrightarrow> st (delformRight x lt k y rt)"
- and del_st: "st lt \<Longrightarrow> st (del x lt)"
+lemma "\<lbrakk>sorted lt; sorted rt; tree_less k lt; tree_greater k rt\<rbrakk> \<Longrightarrow> sorted (delformLeft x lt k y rt)"
+ and "\<lbrakk>sorted lt; sorted rt; tree_less k lt; tree_greater k rt\<rbrakk> \<Longrightarrow> sorted (delformRight x lt k y rt)"
+ and del_sorted: "sorted lt \<Longrightarrow> sorted (del x lt)"
proof (induct x lt k y rt and x lt k y rt and x lt rule: delformLeft_delformRight_del.induct)
case (3 x lta zz v rta yy ss bb)
- from 3 have "tlt yy (Tr B lta zz v rta)" by simp
- hence "tlt yy (del x (Tr B lta zz v rta))" by (rule del_tlt)
- with 3 show ?case by (simp add: balleft_st)
+ from 3 have "tree_less yy (Branch B lta zz v rta)" by simp
+ hence "tree_less yy (del x (Branch B lta zz v rta))" by (rule del_tree_less)
+ with 3 show ?case by (simp add: balleft_sorted)
next
case ("4_2" x vaa vbb vdd vc yy ss bb)
- hence "tlt yy (Tr R vaa vbb vdd vc)" by simp
- hence "tlt yy (del x (Tr R vaa vbb vdd vc))" by (rule del_tlt)
+ hence "tree_less yy (Branch R vaa vbb vdd vc)" by simp
+ hence "tree_less yy (del x (Branch R vaa vbb vdd vc))" by (rule del_tree_less)
with "4_2" show ?case by simp
next
case (5 x aa yy ss lta zz v rta)
- hence "tgt yy (Tr B lta zz v rta)" by simp
- hence "tgt yy (del x (Tr B lta zz v rta))" by (rule del_tgt)
- with 5 show ?case by (simp add: balright_st)
+ hence "tree_greater yy (Branch B lta zz v rta)" by simp
+ hence "tree_greater yy (del x (Branch B lta zz v rta))" by (rule del_tree_greater)
+ with 5 show ?case by (simp add: balright_sorted)
next
case ("6_2" x aa yy ss vaa vbb vdd vc)
- hence "tgt yy (Tr R vaa vbb vdd vc)" by simp
- hence "tgt yy (del x (Tr R vaa vbb vdd vc))" by (rule del_tgt)
+ hence "tree_greater yy (Branch R vaa vbb vdd vc)" by simp
+ hence "tree_greater yy (del x (Branch R vaa vbb vdd vc))" by (rule del_tree_greater)
with "6_2" show ?case by simp
-qed (auto simp: app_st)
+qed (auto simp: app_sorted)
-lemma "\<lbrakk>st lt; st rt; tlt kt lt; tgt kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bh lt = bh rt; x < kt\<rbrakk> \<Longrightarrow> pin_tree k v (delformLeft x lt kt y rt) = (False \<or> (x \<noteq> k \<and> pin_tree k v (Tr c lt kt y rt)))"
- and "\<lbrakk>st lt; st rt; tlt kt lt; tgt kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bh lt = bh rt; x > kt\<rbrakk> \<Longrightarrow> pin_tree k v (delformRight x lt kt y rt) = (False \<or> (x \<noteq> k \<and> pin_tree k v (Tr c lt kt y rt)))"
- and del_pit: "\<lbrakk>st t; inv1 t; inv2 t\<rbrakk> \<Longrightarrow> pin_tree k v (del x t) = (False \<or> (x \<noteq> k \<and> pin_tree k v t))"
+lemma "\<lbrakk>sorted lt; sorted rt; tree_less kt lt; tree_greater kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bheight lt = bheight rt; x < kt\<rbrakk> \<Longrightarrow> entry_in_tree k v (delformLeft x lt kt y rt) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v (Branch c lt kt y rt)))"
+ and "\<lbrakk>sorted lt; sorted rt; tree_less kt lt; tree_greater kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bheight lt = bheight rt; x > kt\<rbrakk> \<Longrightarrow> entry_in_tree k v (delformRight x lt kt y rt) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v (Branch c lt kt y rt)))"
+ and del_pit: "\<lbrakk>sorted t; inv1 t; inv2 t\<rbrakk> \<Longrightarrow> entry_in_tree k v (del x t) = (False \<or> (x \<noteq> k \<and> entry_in_tree k v t))"
proof (induct x lt kt y rt and x lt kt y rt and x t rule: delformLeft_delformRight_del.induct)
case (2 xx c aa yy ss bb)
have "xx = yy \<or> xx < yy \<or> xx > yy" by auto
@@ -657,68 +672,68 @@
assume "xx = yy"
with 2 show ?thesis proof (cases "xx = k")
case True
- from 2 `xx = yy` `xx = k` have "st (Tr c aa yy ss bb) \<and> k = yy" by simp
- hence "\<not> pin_tree k v aa" "\<not> pin_tree k v bb" by (auto simp: tlt_nit tgt_prop)
+ from 2 `xx = yy` `xx = k` have "sorted (Branch c aa yy ss bb) \<and> k = yy" by simp
+ hence "\<not> entry_in_tree k v aa" "\<not> entry_in_tree k v bb" by (auto simp: tree_less_nit tree_greater_prop)
with `xx = yy` 2 `xx = k` show ?thesis by (simp add: app_pit)
qed (simp add: app_pit)
qed simp+
next
case (3 xx lta zz vv rta yy ss bb)
- def mt[simp]: mt == "Tr B lta zz vv rta"
+ def mt[simp]: mt == "Branch B lta zz vv rta"
from 3 have "inv2 mt \<and> inv1 mt" by simp
- hence "inv2 (del xx mt) \<and> (treec mt = R \<and> bh (del xx mt) = bh mt \<and> inv1 (del xx mt) \<or> treec mt = B \<and> bh (del xx mt) = bh mt - 1 \<and> inv1l (del xx mt))" by (blast dest: del_inv1_inv2)
- with 3 have 4: "pin_tree k v (delformLeft xx mt yy ss bb) = (False \<or> xx \<noteq> k \<and> pin_tree k v mt \<or> (k = yy \<and> v = ss) \<or> pin_tree k v bb)" by (simp add: balleft_pit)
+ hence "inv2 (del xx mt) \<and> (color_of mt = R \<and> bheight (del xx mt) = bheight mt \<and> inv1 (del xx mt) \<or> color_of mt = B \<and> bheight (del xx mt) = bheight mt - 1 \<and> inv1l (del xx mt))" by (blast dest: del_inv1_inv2)
+ with 3 have 4: "entry_in_tree k v (delformLeft xx mt yy ss bb) = (False \<or> xx \<noteq> k \<and> entry_in_tree k v mt \<or> (k = yy \<and> v = ss) \<or> entry_in_tree k v bb)" by (simp add: balleft_pit)
thus ?case proof (cases "xx = k")
case True
- from 3 True have "tgt yy bb \<and> yy > k" by simp
- hence "tgt k bb" by (blast dest: tgt_trans)
- with 3 4 True show ?thesis by (auto simp: tgt_nit)
+ from 3 True have "tree_greater yy bb \<and> yy > k" by simp
+ hence "tree_greater k bb" by (blast dest: tree_greater_trans)
+ with 3 4 True show ?thesis by (auto simp: tree_greater_nit)
qed auto
next
case ("4_1" xx yy ss bb)
show ?case proof (cases "xx = k")
case True
- with "4_1" have "tgt yy bb \<and> k < yy" by simp
- hence "tgt k bb" by (blast dest: tgt_trans)
+ with "4_1" have "tree_greater yy bb \<and> k < yy" by simp
+ hence "tree_greater k bb" by (blast dest: tree_greater_trans)
with "4_1" `xx = k`
- have "pin_tree k v (Tr R Empty yy ss bb) = pin_tree k v Empty" by (auto simp: tgt_nit)
+ have "entry_in_tree k v (Branch R Empty yy ss bb) = entry_in_tree k v Empty" by (auto simp: tree_greater_nit)
thus ?thesis by auto
qed simp+
next
case ("4_2" xx vaa vbb vdd vc yy ss bb)
thus ?case proof (cases "xx = k")
case True
- with "4_2" have "k < yy \<and> tgt yy bb" by simp
- hence "tgt k bb" by (blast dest: tgt_trans)
- with True "4_2" show ?thesis by (auto simp: tgt_nit)
+ with "4_2" have "k < yy \<and> tree_greater yy bb" by simp
+ hence "tree_greater k bb" by (blast dest: tree_greater_trans)
+ with True "4_2" show ?thesis by (auto simp: tree_greater_nit)
qed simp
next
case (5 xx aa yy ss lta zz vv rta)
- def mt[simp]: mt == "Tr B lta zz vv rta"
+ def mt[simp]: mt == "Branch B lta zz vv rta"
from 5 have "inv2 mt \<and> inv1 mt" by simp
- hence "inv2 (del xx mt) \<and> (treec mt = R \<and> bh (del xx mt) = bh mt \<and> inv1 (del xx mt) \<or> treec mt = B \<and> bh (del xx mt) = bh mt - 1 \<and> inv1l (del xx mt))" by (blast dest: del_inv1_inv2)
- with 5 have 3: "pin_tree k v (delformRight xx aa yy ss mt) = (pin_tree k v aa \<or> (k = yy \<and> v = ss) \<or> False \<or> xx \<noteq> k \<and> pin_tree k v mt)" by (simp add: balright_pit)
+ hence "inv2 (del xx mt) \<and> (color_of mt = R \<and> bheight (del xx mt) = bheight mt \<and> inv1 (del xx mt) \<or> color_of mt = B \<and> bheight (del xx mt) = bheight mt - 1 \<and> inv1l (del xx mt))" by (blast dest: del_inv1_inv2)
+ with 5 have 3: "entry_in_tree k v (delformRight xx aa yy ss mt) = (entry_in_tree k v aa \<or> (k = yy \<and> v = ss) \<or> False \<or> xx \<noteq> k \<and> entry_in_tree k v mt)" by (simp add: balright_pit)
thus ?case proof (cases "xx = k")
case True
- from 5 True have "tlt yy aa \<and> yy < k" by simp
- hence "tlt k aa" by (blast dest: tlt_trans)
- with 3 5 True show ?thesis by (auto simp: tlt_nit)
+ from 5 True have "tree_less yy aa \<and> yy < k" by simp
+ hence "tree_less k aa" by (blast dest: tree_less_trans)
+ with 3 5 True show ?thesis by (auto simp: tree_less_nit)
qed auto
next
case ("6_1" xx aa yy ss)
show ?case proof (cases "xx = k")
case True
- with "6_1" have "tlt yy aa \<and> k > yy" by simp
- hence "tlt k aa" by (blast dest: tlt_trans)
- with "6_1" `xx = k` show ?thesis by (auto simp: tlt_nit)
+ with "6_1" have "tree_less yy aa \<and> k > yy" by simp
+ hence "tree_less k aa" by (blast dest: tree_less_trans)
+ with "6_1" `xx = k` show ?thesis by (auto simp: tree_less_nit)
qed simp
next
case ("6_2" xx aa yy ss vaa vbb vdd vc)
thus ?case proof (cases "xx = k")
case True
- with "6_2" have "k > yy \<and> tlt yy aa" by simp
- hence "tlt k aa" by (blast dest: tlt_trans)
- with True "6_2" show ?thesis by (auto simp: tlt_nit)
+ with "6_2" have "k > yy \<and> tree_less yy aa" by simp
+ hence "tree_less k aa" by (blast dest: tree_less_trans)
+ with True "6_2" show ?thesis by (auto simp: tree_less_nit)
qed simp
qed simp
@@ -726,36 +741,36 @@
definition delete where
delete_def: "delete k t = paint B (del k t)"
-theorem delete_isrbt[simp]: assumes "isrbt t" shows "isrbt (delete k t)"
+theorem delete_is_rbt[simp]: assumes "is_rbt t" shows "is_rbt (delete k t)"
proof -
- from assms have "inv2 t" and "inv1 t" unfolding isrbt_def by auto
- hence "inv2 (del k t) \<and> (treec t = R \<and> bh (del k t) = bh t \<and> inv1 (del k t) \<or> treec t = B \<and> bh (del k t) = bh t - 1 \<and> inv1l (del k t))" by (rule del_inv1_inv2)
- hence "inv2 (del k t) \<and> inv1l (del k t)" by (cases "treec t") auto
+ from assms have "inv2 t" and "inv1 t" unfolding is_rbt_def by auto
+ hence "inv2 (del k t) \<and> (color_of t = R \<and> bheight (del k t) = bheight t \<and> inv1 (del k t) \<or> color_of t = B \<and> bheight (del k t) = bheight t - 1 \<and> inv1l (del k t))" by (rule del_inv1_inv2)
+ hence "inv2 (del k t) \<and> inv1l (del k t)" by (cases "color_of t") auto
with assms show ?thesis
- unfolding isrbt_def delete_def
- by (auto intro: paint_st del_st)
+ unfolding is_rbt_def delete_def
+ by (auto intro: paint_sorted del_sorted)
qed
lemma delete_pit:
- assumes "isrbt t"
- shows "pin_tree k v (delete x t) = (x \<noteq> k \<and> pin_tree k v t)"
- using assms unfolding isrbt_def delete_def
+ assumes "is_rbt t"
+ shows "entry_in_tree k v (delete x t) = (x \<noteq> k \<and> entry_in_tree k v t)"
+ using assms unfolding is_rbt_def delete_def
by (auto simp: del_pit)
-lemma map_of_delete:
- assumes isrbt: "isrbt t"
- shows "map_of (delete k t) = (map_of t)|`(-{k})"
+lemma lookup_delete:
+ assumes is_rbt: "is_rbt t"
+ shows "lookup (delete k t) = (lookup t)|`(-{k})"
proof
fix x
- show "map_of (delete k t) x = (map_of t |` (-{k})) x"
+ show "lookup (delete k t) x = (lookup t |` (-{k})) x"
proof (cases "x = k")
assume "x = k"
- with isrbt show ?thesis
- by (cases "map_of (delete k t) k") (auto simp: mapof_pit delete_pit)
+ with is_rbt show ?thesis
+ by (cases "lookup (delete k t) k") (auto simp: lookup_pit delete_pit)
next
assume "x \<noteq> k"
thus ?thesis
- by auto (metis isrbt delete_isrbt delete_pit isrbt_st mapof_from_pit)
+ by auto (metis is_rbt delete_is_rbt delete_pit is_rbt_sorted lookup_from_pit)
qed
qed
@@ -765,43 +780,43 @@
unionwithkey :: "('a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
where
"unionwithkey f t Empty = t"
-| "unionwithkey f t (Tr c lt k v rt) = unionwithkey f (unionwithkey f (insertwithkey f k v t) lt) rt"
+| "unionwithkey f t (Branch c lt k v rt) = unionwithkey f (unionwithkey f (insertwithkey f k v t) lt) rt"
-lemma unionwk_st: "st lt \<Longrightarrow> st (unionwithkey f lt rt)"
- by (induct rt arbitrary: lt) (auto simp: insertwk_st)
-theorem unionwk_isrbt[simp]: "isrbt lt \<Longrightarrow> isrbt (unionwithkey f lt rt)"
- by (induct rt arbitrary: lt) (simp add: insertwk_isrbt)+
+lemma unionwk_sorted: "sorted lt \<Longrightarrow> sorted (unionwithkey f lt rt)"
+ by (induct rt arbitrary: lt) (auto simp: insertwk_sorted)
+theorem unionwk_is_rbt[simp]: "is_rbt lt \<Longrightarrow> is_rbt (unionwithkey f lt rt)"
+ by (induct rt arbitrary: lt) (simp add: insertwk_is_rbt)+
definition
unionwith where
"unionwith f = unionwithkey (\<lambda>_. f)"
-theorem unionw_isrbt: "isrbt lt \<Longrightarrow> isrbt (unionwith f lt rt)" unfolding unionwith_def by simp
+theorem unionw_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (unionwith f lt rt)" unfolding unionwith_def by simp
definition union where
"union = unionwithkey (%_ _ rv. rv)"
-theorem union_isrbt: "isrbt lt \<Longrightarrow> isrbt (union lt rt)" unfolding union_def by simp
+theorem union_is_rbt: "is_rbt lt \<Longrightarrow> is_rbt (union lt rt)" unfolding union_def by simp
-lemma union_Tr[simp]:
- "union t (Tr c lt k v rt) = union (union (insrt k v t) lt) rt"
- unfolding union_def insrt_def
+lemma union_Branch[simp]:
+ "union t (Branch c lt k v rt) = union (union (insert k v t) lt) rt"
+ unfolding union_def insert_def
by simp
-lemma map_of_union:
- assumes "isrbt s" "st t"
- shows "map_of (union s t) = map_of s ++ map_of t"
+lemma lookup_union:
+ assumes "is_rbt s" "sorted t"
+ shows "lookup (union s t) = lookup s ++ lookup t"
using assms
proof (induct t arbitrary: s)
case Empty thus ?case by (auto simp: union_def)
next
- case (Tr c l k v r s)
- hence strl: "st r" "st l" "l |\<guillemotleft> k" "k \<guillemotleft>| r" by auto
+ case (Branch c l k v r s)
+ hence sortedrl: "sorted r" "sorted l" "l |\<guillemotleft> k" "k \<guillemotleft>| r" by auto
- have meq: "map_of s(k \<mapsto> v) ++ map_of l ++ map_of r =
- map_of s ++
- (\<lambda>a. if a < k then map_of l a
- else if k < a then map_of r a else Some v)" (is "?m1 = ?m2")
+ have meq: "lookup s(k \<mapsto> v) ++ lookup l ++ lookup r =
+ lookup s ++
+ (\<lambda>a. if a < k then lookup l a
+ else if k < a then lookup r a else Some v)" (is "?m1 = ?m2")
proof (rule ext)
fix a
@@ -809,7 +824,7 @@
thus "?m1 a = ?m2 a"
proof (elim disjE)
assume "k < a"
- with `l |\<guillemotleft> k` have "l |\<guillemotleft> a" by (rule tlt_trans)
+ with `l |\<guillemotleft> k` have "l |\<guillemotleft> a" by (rule tree_less_trans)
with `k < a` show ?thesis
by (auto simp: map_add_def split: option.splits)
next
@@ -818,20 +833,20 @@
show ?thesis by (auto simp: map_add_def)
next
assume "a < k"
- from this `k \<guillemotleft>| r` have "a \<guillemotleft>| r" by (rule tgt_trans)
+ from this `k \<guillemotleft>| r` have "a \<guillemotleft>| r" by (rule tree_greater_trans)
with `a < k` show ?thesis
by (auto simp: map_add_def split: option.splits)
qed
qed
- from Tr
+ from Branch
have IHs:
- "map_of (union (union (insrt k v s) l) r) = map_of (union (insrt k v s) l) ++ map_of r"
- "map_of (union (insrt k v s) l) = map_of (insrt k v s) ++ map_of l"
- by (auto intro: union_isrbt insrt_isrbt)
+ "lookup (union (union (insert k v s) l) r) = lookup (union (insert k v s) l) ++ lookup r"
+ "lookup (union (insert k v s) l) = lookup (insert k v s) ++ lookup l"
+ by (auto intro: union_is_rbt insert_is_rbt)
with meq show ?case
- by (auto simp: map_of_insert[OF Tr(3)])
+ by (auto simp: lookup_insert[OF Branch(3)])
qed
subsection {* Adjust *}
@@ -840,33 +855,33 @@
adjustwithkey :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
where
"adjustwithkey f k Empty = Empty"
-| "adjustwithkey f k (Tr c lt x v rt) = (if k < x then (Tr c (adjustwithkey f k lt) x v rt) else if k > x then (Tr c lt x v (adjustwithkey f k rt)) else (Tr c lt x (f x v) rt))"
+| "adjustwithkey f k (Branch c lt x v rt) = (if k < x then (Branch c (adjustwithkey f k lt) x v rt) else if k > x then (Branch c lt x v (adjustwithkey f k rt)) else (Branch c lt x (f x v) rt))"
-lemma adjustwk_treec: "treec (adjustwithkey f k t) = treec t" by (induct t) simp+
-lemma adjustwk_inv1: "inv1 (adjustwithkey f k t) = inv1 t" by (induct t) (simp add: adjustwk_treec)+
-lemma adjustwk_inv2: "inv2 (adjustwithkey f k t) = inv2 t" "bh (adjustwithkey f k t) = bh t" by (induct t) simp+
-lemma adjustwk_tgt: "tgt k (adjustwithkey f kk t) = tgt k t" by (induct t) simp+
-lemma adjustwk_tlt: "tlt k (adjustwithkey f kk t) = tlt k t" by (induct t) simp+
-lemma adjustwk_st: "st (adjustwithkey f k t) = st t" by (induct t) (simp add: adjustwk_tlt adjustwk_tgt)+
+lemma adjustwk_color_of: "color_of (adjustwithkey f k t) = color_of t" by (induct t) simp+
+lemma adjustwk_inv1: "inv1 (adjustwithkey f k t) = inv1 t" by (induct t) (simp add: adjustwk_color_of)+
+lemma adjustwk_inv2: "inv2 (adjustwithkey f k t) = inv2 t" "bheight (adjustwithkey f k t) = bheight t" by (induct t) simp+
+lemma adjustwk_tree_greater: "tree_greater k (adjustwithkey f kk t) = tree_greater k t" by (induct t) simp+
+lemma adjustwk_tree_less: "tree_less k (adjustwithkey f kk t) = tree_less k t" by (induct t) simp+
+lemma adjustwk_sorted: "sorted (adjustwithkey f k t) = sorted t" by (induct t) (simp add: adjustwk_tree_less adjustwk_tree_greater)+
-theorem adjustwk_isrbt[simp]: "isrbt (adjustwithkey f k t) = isrbt t"
-unfolding isrbt_def by (simp add: adjustwk_inv2 adjustwk_treec adjustwk_st adjustwk_inv1 )
+theorem adjustwk_is_rbt[simp]: "is_rbt (adjustwithkey f k t) = is_rbt t"
+unfolding is_rbt_def by (simp add: adjustwk_inv2 adjustwk_color_of adjustwk_sorted adjustwk_inv1 )
theorem adjustwithkey_map[simp]:
- "map_of (adjustwithkey f k t) x =
- (if x = k then case map_of t x of None \<Rightarrow> None | Some y \<Rightarrow> Some (f k y)
- else map_of t x)"
+ "lookup (adjustwithkey f k t) x =
+ (if x = k then case lookup t x of None \<Rightarrow> None | Some y \<Rightarrow> Some (f k y)
+ else lookup t x)"
by (induct t arbitrary: x) (auto split:option.splits)
definition adjust where
"adjust f = adjustwithkey (\<lambda>_. f)"
-theorem adjust_isrbt[simp]: "isrbt (adjust f k t) = isrbt t" unfolding adjust_def by simp
+theorem adjust_is_rbt[simp]: "is_rbt (adjust f k t) = is_rbt t" unfolding adjust_def by simp
theorem adjust_map[simp]:
- "map_of (adjust f k t) x =
- (if x = k then case map_of t x of None \<Rightarrow> None | Some y \<Rightarrow> Some (f y)
- else map_of t x)"
+ "lookup (adjust f k t) x =
+ (if x = k then case lookup t x of None \<Rightarrow> None | Some y \<Rightarrow> Some (f y)
+ else lookup t x)"
unfolding adjust_def by simp
subsection {* Map *}
@@ -875,27 +890,27 @@
mapwithkey :: "('a::linorder \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'c) rbt"
where
"mapwithkey f Empty = Empty"
-| "mapwithkey f (Tr c lt k v rt) = Tr c (mapwithkey f lt) k (f k v) (mapwithkey f rt)"
+| "mapwithkey f (Branch c lt k v rt) = Branch c (mapwithkey f lt) k (f k v) (mapwithkey f rt)"
theorem mapwk_keys[simp]: "keys (mapwithkey f t) = keys t" by (induct t) auto
-lemma mapwk_tgt: "tgt k (mapwithkey f t) = tgt k t" by (induct t) simp+
-lemma mapwk_tlt: "tlt k (mapwithkey f t) = tlt k t" by (induct t) simp+
-lemma mapwk_st: "st (mapwithkey f t) = st t" by (induct t) (simp add: mapwk_tlt mapwk_tgt)+
-lemma mapwk_treec: "treec (mapwithkey f t) = treec t" by (induct t) simp+
-lemma mapwk_inv1: "inv1 (mapwithkey f t) = inv1 t" by (induct t) (simp add: mapwk_treec)+
-lemma mapwk_inv2: "inv2 (mapwithkey f t) = inv2 t" "bh (mapwithkey f t) = bh t" by (induct t) simp+
-theorem mapwk_isrbt[simp]: "isrbt (mapwithkey f t) = isrbt t"
-unfolding isrbt_def by (simp add: mapwk_inv1 mapwk_inv2 mapwk_st mapwk_treec)
+lemma mapwk_tree_greater: "tree_greater k (mapwithkey f t) = tree_greater k t" by (induct t) simp+
+lemma mapwk_tree_less: "tree_less k (mapwithkey f t) = tree_less k t" by (induct t) simp+
+lemma mapwk_sorted: "sorted (mapwithkey f t) = sorted t" by (induct t) (simp add: mapwk_tree_less mapwk_tree_greater)+
+lemma mapwk_color_of: "color_of (mapwithkey f t) = color_of t" by (induct t) simp+
+lemma mapwk_inv1: "inv1 (mapwithkey f t) = inv1 t" by (induct t) (simp add: mapwk_color_of)+
+lemma mapwk_inv2: "inv2 (mapwithkey f t) = inv2 t" "bheight (mapwithkey f t) = bheight t" by (induct t) simp+
+theorem mapwk_is_rbt[simp]: "is_rbt (mapwithkey f t) = is_rbt t"
+unfolding is_rbt_def by (simp add: mapwk_inv1 mapwk_inv2 mapwk_sorted mapwk_color_of)
-theorem map_of_mapwk[simp]: "map_of (mapwithkey f t) x = Option.map (f x) (map_of t x)"
+theorem lookup_mapwk[simp]: "lookup (mapwithkey f t) x = Option.map (f x) (lookup t x)"
by (induct t) auto
definition map
where map_def: "map f == mapwithkey (\<lambda>_. f)"
theorem map_keys[simp]: "keys (map f t) = keys t" unfolding map_def by simp
-theorem map_isrbt[simp]: "isrbt (map f t) = isrbt t" unfolding map_def by simp
-theorem map_of_map[simp]: "map_of (map f t) = Option.map f o map_of t"
+theorem map_is_rbt[simp]: "is_rbt (map f t) = is_rbt t" unfolding map_def by simp
+theorem lookup_map[simp]: "lookup (map f t) = Option.map f o lookup t"
by (rule ext) (simp add:map_def)
subsection {* Fold *}
@@ -906,62 +921,57 @@
foldwithkey :: "('a::linorder \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a,'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"
where
"foldwithkey f Empty v = v"
-| "foldwithkey f (Tr c lt k x rt) v = foldwithkey f rt (f k x (foldwithkey f lt v))"
+| "foldwithkey f (Branch c lt k x rt) v = foldwithkey f rt (f k x (foldwithkey f lt v))"
-primrec alist_of
-where
- "alist_of Empty = []"
-| "alist_of (Tr _ l k v r) = alist_of l @ (k,v) # alist_of r"
-
-lemma map_of_alist_of_aux: "st (Tr c t1 k v t2) \<Longrightarrow> RBT.map_of (Tr c t1 k v t2) = RBT.map_of t2 ++ [k\<mapsto>v] ++ RBT.map_of t1"
+lemma lookup_entries_aux: "sorted (Branch c t1 k v t2) \<Longrightarrow> RBT.lookup (Branch c t1 k v t2) = RBT.lookup t2 ++ [k\<mapsto>v] ++ RBT.lookup t1"
proof (rule ext)
fix x
- assume ST: "st (Tr c t1 k v t2)"
- let ?thesis = "RBT.map_of (Tr c t1 k v t2) x = (RBT.map_of t2 ++ [k \<mapsto> v] ++ RBT.map_of t1) x"
+ assume SORTED: "sorted (Branch c t1 k v t2)"
+ let ?thesis = "RBT.lookup (Branch c t1 k v t2) x = (RBT.lookup t2 ++ [k \<mapsto> v] ++ RBT.lookup t1) x"
- have DOM_T1: "!!k'. k'\<in>dom (RBT.map_of t1) \<Longrightarrow> k>k'"
+ have DOM_T1: "!!k'. k'\<in>dom (RBT.lookup t1) \<Longrightarrow> k>k'"
proof -
fix k'
- from ST have "t1 |\<guillemotleft> k" by simp
- with tlt_prop have "\<forall>k'\<in>keys t1. k>k'" by auto
- moreover assume "k'\<in>dom (RBT.map_of t1)"
- ultimately show "k>k'" using RBT.mapof_keys ST by auto
+ from SORTED have "t1 |\<guillemotleft> k" by simp
+ with tree_less_prop have "\<forall>k'\<in>keys t1. k>k'" by auto
+ moreover assume "k'\<in>dom (RBT.lookup t1)"
+ ultimately show "k>k'" using RBT.lookup_keys SORTED by auto
qed
- have DOM_T2: "!!k'. k'\<in>dom (RBT.map_of t2) \<Longrightarrow> k<k'"
+ have DOM_T2: "!!k'. k'\<in>dom (RBT.lookup t2) \<Longrightarrow> k<k'"
proof -
fix k'
- from ST have "k \<guillemotleft>| t2" by simp
- with tgt_prop have "\<forall>k'\<in>keys t2. k<k'" by auto
- moreover assume "k'\<in>dom (RBT.map_of t2)"
- ultimately show "k<k'" using RBT.mapof_keys ST by auto
+ from SORTED have "k \<guillemotleft>| t2" by simp
+ with tree_greater_prop have "\<forall>k'\<in>keys t2. k<k'" by auto
+ moreover assume "k'\<in>dom (RBT.lookup t2)"
+ ultimately show "k<k'" using RBT.lookup_keys SORTED by auto
qed
{
assume C: "x<k"
- hence "RBT.map_of (Tr c t1 k v t2) x = RBT.map_of t1 x" by simp
+ hence "RBT.lookup (Branch c t1 k v t2) x = RBT.lookup t1 x" by simp
moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
- moreover have "x\<notin>dom (RBT.map_of t2)" proof
- assume "x\<in>dom (RBT.map_of t2)"
+ moreover have "x\<notin>dom (RBT.lookup t2)" proof
+ assume "x\<in>dom (RBT.lookup t2)"
with DOM_T2 have "k<x" by blast
with C show False by simp
qed
ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
} moreover {
assume [simp]: "x=k"
- hence "RBT.map_of (Tr c t1 k v t2) x = [k \<mapsto> v] x" by simp
- moreover have "x\<notin>dom (RBT.map_of t1)" proof
- assume "x\<in>dom (RBT.map_of t1)"
+ hence "RBT.lookup (Branch c t1 k v t2) x = [k \<mapsto> v] x" by simp
+ moreover have "x\<notin>dom (RBT.lookup t1)" proof
+ assume "x\<in>dom (RBT.lookup t1)"
with DOM_T1 have "k>x" by blast
thus False by simp
qed
ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps)
} moreover {
assume C: "x>k"
- hence "RBT.map_of (Tr c t1 k v t2) x = RBT.map_of t2 x" by (simp add: less_not_sym[of k x])
+ hence "RBT.lookup (Branch c t1 k v t2) x = RBT.lookup t2 x" by (simp add: less_not_sym[of k x])
moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp
- moreover have "x\<notin>dom (RBT.map_of t1)" proof
- assume "x\<in>dom (RBT.map_of t1)"
+ moreover have "x\<notin>dom (RBT.lookup t1)" proof
+ assume "x\<in>dom (RBT.lookup t1)"
with DOM_T1 have "k>x" by simp
with C show False by simp
qed
@@ -969,35 +979,38 @@
} ultimately show ?thesis using less_linear by blast
qed
-lemma map_of_alist_of:
- shows "st t \<Longrightarrow> Map.map_of (alist_of t) = map_of t"
+lemma map_of_entries:
+ shows "sorted t \<Longrightarrow> map_of (entries t) = lookup t"
proof (induct t)
- case Empty thus ?case by (simp add: RBT.map_of_Empty)
+ case Empty thus ?case by (simp add: RBT.lookup_Empty)
next
- case (Tr c t1 k v t2)
- hence "Map.map_of (alist_of (Tr c t1 k v t2)) = RBT.map_of t2 ++ [k \<mapsto> v] ++ RBT.map_of t1" by simp
- also note map_of_alist_of_aux[OF Tr.prems,symmetric]
+ case (Branch c t1 k v t2)
+ hence "map_of (entries (Branch c t1 k v t2)) = RBT.lookup t2 ++ [k \<mapsto> v] ++ RBT.lookup t1" by simp
+ also note lookup_entries_aux [OF Branch.prems,symmetric]
finally show ?case .
qed
-lemma fold_alist_fold:
- "foldwithkey f t x = foldl (\<lambda>x (k,v). f k v x) x (alist_of t)"
+lemma fold_entries_fold:
+ "foldwithkey f t x = foldl (\<lambda>x (k,v). f k v x) x (entries t)"
by (induct t arbitrary: x) auto
-lemma alist_pit[simp]: "(k, v) \<in> set (alist_of t) = pin_tree k v t"
+lemma entries_pit[simp]: "(k, v) \<in> set (entries t) = entry_in_tree k v t"
by (induct t) auto
-lemma sorted_alist:
- "st t \<Longrightarrow> sorted (List.map fst (alist_of t))"
+lemma sorted_entries:
+ "sorted t \<Longrightarrow> List.sorted (List.map fst (entries t))"
by (induct t)
- (force simp: sorted_append sorted_Cons tlgt_props
- dest!:pint_keys)+
+ (force simp: sorted_append sorted_Cons tree_ord_props
+ dest!: entry_in_tree_keys)+
-lemma distinct_alist:
- "st t \<Longrightarrow> distinct (List.map fst (alist_of t))"
+lemma distinct_entries:
+ "sorted t \<Longrightarrow> distinct (List.map fst (entries t))"
by (induct t)
- (force simp: sorted_append sorted_Cons tlgt_props
- dest!:pint_keys)+
+ (force simp: sorted_append sorted_Cons tree_ord_props
+ dest!: entry_in_tree_keys)+
+
+hide (open) const Empty insert delete entries lookup map fold union adjust sorted
+
(*>*)
text {*
@@ -1010,20 +1023,20 @@
text {*
The type @{typ "('k, 'v) rbt"} denotes red-black trees with keys of
type @{typ "'k"} and values of type @{typ "'v"}. To function
- properly, the key type must belong to the @{text "linorder"} class.
+ properly, the key type musorted belong to the @{text "linorder"} class.
A value @{term t} of this type is a valid red-black tree if it
- satisfies the invariant @{text "isrbt t"}.
+ satisfies the invariant @{text "is_rbt t"}.
This theory provides lemmas to prove that the invariant is
satisfied throughout the computation.
- The interpretation function @{const "map_of"} returns the partial
+ The interpretation function @{const "RBT.lookup"} returns the partial
map represented by a red-black tree:
- @{term_type[display] "map_of"}
+ @{term_type[display] "RBT.lookup"}
This function should be used for reasoning about the semantics of the RBT
operations. Furthermore, it implements the lookup functionality for
- the data structure: It is executable and the lookup is performed in
+ the data sortedructure: It is executable and the lookup is performed in
$O(\log n)$.
*}
@@ -1032,19 +1045,19 @@
text {*
Currently, the following operations are supported:
- @{term_type[display] "Empty"}
+ @{term_type[display] "RBT.Empty"}
Returns the empty tree. $O(1)$
- @{term_type[display] "insrt"}
+ @{term_type[display] "RBT.insert"}
Updates the map at a given position. $O(\log n)$
- @{term_type[display] "delete"}
+ @{term_type[display] "RBT.delete"}
Deletes a map entry at a given position. $O(\log n)$
- @{term_type[display] "union"}
+ @{term_type[display] "RBT.union"}
Forms the union of two trees, preferring entries from the first one.
- @{term_type[display] "map"}
+ @{term_type[display] "RBT.map"}
Maps a function over the values of a map. $O(n)$
*}
@@ -1053,47 +1066,47 @@
text {*
\noindent
- @{thm Empty_isrbt}\hfill(@{text "Empty_isrbt"})
+ @{thm Empty_is_rbt}\hfill(@{text "Empty_is_rbt"})
\noindent
- @{thm insrt_isrbt}\hfill(@{text "insrt_isrbt"})
+ @{thm insert_is_rbt}\hfill(@{text "insert_is_rbt"})
\noindent
- @{thm delete_isrbt}\hfill(@{text "delete_isrbt"})
+ @{thm delete_is_rbt}\hfill(@{text "delete_is_rbt"})
\noindent
- @{thm union_isrbt}\hfill(@{text "union_isrbt"})
+ @{thm union_is_rbt}\hfill(@{text "union_is_rbt"})
\noindent
- @{thm map_isrbt}\hfill(@{text "map_isrbt"})
+ @{thm map_is_rbt}\hfill(@{text "map_is_rbt"})
*}
subsection {* Map Semantics *}
text {*
\noindent
- \underline{@{text "map_of_Empty"}}
- @{thm[display] map_of_Empty}
+ \underline{@{text "lookup_Empty"}}
+ @{thm[display] lookup_Empty}
\vspace{1ex}
\noindent
- \underline{@{text "map_of_insert"}}
- @{thm[display] map_of_insert}
+ \underline{@{text "lookup_insert"}}
+ @{thm[display] lookup_insert}
\vspace{1ex}
\noindent
- \underline{@{text "map_of_delete"}}
- @{thm[display] map_of_delete}
+ \underline{@{text "lookup_delete"}}
+ @{thm[display] lookup_delete}
\vspace{1ex}
\noindent
- \underline{@{text "map_of_union"}}
- @{thm[display] map_of_union}
+ \underline{@{text "lookup_union"}}
+ @{thm[display] lookup_union}
\vspace{1ex}
\noindent
- \underline{@{text "map_of_map"}}
- @{thm[display] map_of_map}
+ \underline{@{text "lookup_map"}}
+ @{thm[display] lookup_map}
\vspace{1ex}
*}
--- a/src/HOL/Library/Transitive_Closure_Table.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Library/Transitive_Closure_Table.thy Wed Mar 03 10:40:40 2010 -0800
@@ -107,25 +107,25 @@
proof (cases as)
case Nil
with xxs have x: "x = a" and xs: "xs = bs @ a # cs"
- by auto
+ by auto
from x xs `rtrancl_path r x xs y` have cs: "rtrancl_path r x cs y"
- by (auto elim: rtrancl_path_appendE)
+ by (auto elim: rtrancl_path_appendE)
from xs have "length cs < length xs" by simp
then show ?thesis
- by (rule less(1)) (iprover intro: cs less(2))+
+ by (rule less(1)) (iprover intro: cs less(2))+
next
case (Cons d ds)
with xxs have xs: "xs = ds @ a # (bs @ [a] @ cs)"
- by auto
+ by auto
with `rtrancl_path r x xs y` obtain xa: "rtrancl_path r x (ds @ [a]) a"
and ay: "rtrancl_path r a (bs @ a # cs) y"
- by (auto elim: rtrancl_path_appendE)
+ by (auto elim: rtrancl_path_appendE)
from ay have "rtrancl_path r a cs y" by (auto elim: rtrancl_path_appendE)
with xa have xy: "rtrancl_path r x ((ds @ [a]) @ cs) y"
- by (rule rtrancl_path_trans)
+ by (rule rtrancl_path_trans)
from xs have "length ((ds @ [a]) @ cs) < length xs" by simp
then show ?thesis
- by (rule less(1)) (iprover intro: xy less(2))+
+ by (rule less(1)) (iprover intro: xy less(2))+
qed
qed
qed
--- a/src/HOL/Map.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Map.thy Wed Mar 03 10:40:40 2010 -0800
@@ -12,10 +12,10 @@
begin
types ('a,'b) "~=>" = "'a => 'b option" (infixr "~=>" 0)
-translations (type) "a ~=> b " <= (type) "a => b option"
+translations (type) "'a ~=> 'b" <= (type) "'a => 'b option"
-syntax (xsymbols)
- "~=>" :: "[type, type] => type" (infixr "\<rightharpoonup>" 0)
+type_notation (xsymbols)
+ "~=>" (infixr "\<rightharpoonup>" 0)
abbreviation
empty :: "'a ~=> 'b" where
--- a/src/HOL/MicroJava/J/Decl.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/MicroJava/J/Decl.thy Wed Mar 03 10:40:40 2010 -0800
@@ -23,12 +23,12 @@
translations
- "fdecl" <= (type) "vname \<times> ty"
- "sig" <= (type) "mname \<times> ty list"
- "mdecl c" <= (type) "sig \<times> ty \<times> c"
- "class c" <= (type) "cname \<times> fdecl list \<times> (c mdecl) list"
- "cdecl c" <= (type) "cname \<times> (c class)"
- "prog c" <= (type) "(c cdecl) list"
+ (type) "fdecl" <= (type) "vname \<times> ty"
+ (type) "sig" <= (type) "mname \<times> ty list"
+ (type) "'c mdecl" <= (type) "sig \<times> ty \<times> 'c"
+ (type) "'c class" <= (type) "cname \<times> fdecl list \<times> ('c mdecl) list"
+ (type) "'c cdecl" <= (type) "cname \<times> ('c class)"
+ (type) "'c prog" <= (type) "('c cdecl) list"
definition "class" :: "'c prog => (cname \<rightharpoonup> 'c class)" where
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed Mar 03 10:40:40 2010 -0800
@@ -15,8 +15,6 @@
declare vector_add_ldistrib[simp] vector_ssub_ldistrib[simp] vector_smult_assoc[simp] vector_smult_rneg[simp]
declare vector_sadd_rdistrib[simp] vector_sub_rdistrib[simp]
-declare dot_ladd[simp] dot_radd[simp] dot_lsub[simp] dot_rsub[simp]
-declare dot_lmult[simp] dot_rmult[simp] dot_lneg[simp] dot_rneg[simp]
declare UNIV_1[simp]
(*lemma dim1in[intro]:"Suc 0 \<in> {1::nat .. CARD(1)}" by auto*)
@@ -1717,7 +1715,7 @@
using norm_basis and dimindex_ge_1 by auto
thus ?thesis apply(rule_tac x="basis a" in exI, rule_tac x=1 in exI) using True by auto
next case False thus ?thesis using False using separating_hyperplane_closed_point[OF assms]
- apply - apply(erule exE)+ unfolding dot_rzero apply(rule_tac x=a in exI, rule_tac x=b in exI) by auto qed
+ apply - apply(erule exE)+ unfolding inner.zero_right apply(rule_tac x=a in exI, rule_tac x=b in exI) by auto qed
subsection {* Now set-to-set for closed/compact sets. *}
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Wed Mar 03 10:40:40 2010 -0800
@@ -12,6 +12,9 @@
(* Because I do not want to type this all the time *)
lemmas linear_linear = linear_conv_bounded_linear[THEN sym]
+(** move this **)
+declare norm_vec1[simp]
+
subsection {* Derivatives *}
text {* The definition is slightly tricky since we make it work over
@@ -612,7 +615,7 @@
finally have "\<bar>(f (x + c *\<^sub>R basis j) - f x - D *v (c *\<^sub>R basis j)) $ k\<bar> \<le> \<bar>D $ k $ j\<bar> / 2 * \<bar>c\<bar>" by simp
hence "\<bar>f (x + c *\<^sub>R basis j) $ k - f x $ k - c * D $ k $ j\<bar> \<le> \<bar>D $ k $ j\<bar> / 2 * \<bar>c\<bar>"
unfolding vector_component_simps matrix_vector_mul_component unfolding smult_conv_scaleR[symmetric]
- unfolding dot_rmult dot_basis unfolding smult_conv_scaleR by simp } note * = this
+ unfolding inner_simps dot_basis smult_conv_scaleR by simp } note * = this
have "x + d *\<^sub>R basis j \<in> ball x e" "x - d *\<^sub>R basis j \<in> ball x e"
unfolding mem_ball vector_dist_norm using norm_basis[of j] d by auto
hence **:"((f (x - d *\<^sub>R basis j))$k \<le> (f x)$k \<and> (f (x + d *\<^sub>R basis j))$k \<le> (f x)$k) \<or>
@@ -702,20 +705,17 @@
subsection {* A nice generalization (see Havin's proof of 5.19 from Rudin's book). *}
-lemma inner_eq_dot: fixes a::"real^'n"
- shows "a \<bullet> b = inner a b" unfolding inner_vector_def dot_def by auto
-
lemma mvt_general: fixes f::"real\<Rightarrow>real^'n"
assumes "a<b" "continuous_on {a..b} f" "\<forall>x\<in>{a<..<b}. (f has_derivative f'(x)) (at x)"
shows "\<exists>x\<in>{a<..<b}. norm(f b - f a) \<le> norm(f'(x) (b - a))" proof-
have "\<exists>x\<in>{a<..<b}. (op \<bullet> (f b - f a) \<circ> f) b - (op \<bullet> (f b - f a) \<circ> f) a = (f b - f a) \<bullet> f' x (b - a)"
- apply(rule mvt) apply(rule assms(1))unfolding inner_eq_dot apply(rule continuous_on_inner continuous_on_intros assms(2))+
+ apply(rule mvt) apply(rule assms(1)) apply(rule continuous_on_inner continuous_on_intros assms(2))+
unfolding o_def apply(rule,rule has_derivative_lift_dot) using assms(3) by auto
then guess x .. note x=this
show ?thesis proof(cases "f a = f b")
case False have "norm (f b - f a) * norm (f b - f a) = norm (f b - f a)^2" by(simp add:class_semiring.semiring_rules)
- also have "\<dots> = (f b - f a) \<bullet> (f b - f a)" unfolding norm_pow_2 ..
- also have "\<dots> = (f b - f a) \<bullet> f' x (b - a)" using x by auto
+ also have "\<dots> = (f b - f a) \<bullet> (f b - f a)" unfolding power2_norm_eq_inner ..
+ also have "\<dots> = (f b - f a) \<bullet> f' x (b - a)" using x unfolding inner_simps by auto
also have "\<dots> \<le> norm (f b - f a) * norm (f' x (b - a))" by(rule norm_cauchy_schwarz)
finally show ?thesis using False x(1) by(auto simp add: real_mult_left_cancel) next
case True thus ?thesis using assms(1) apply(rule_tac x="(a + b) /2" in bexI) by auto qed qed
@@ -751,9 +751,6 @@
also have "\<dots> \<le> B * norm(y - x)" apply(rule **) using * and u by auto
finally show ?thesis by(auto simp add:norm_minus_commute) qed
-(** move this **)
-declare norm_vec1[simp]
-
lemma onorm_vec1: fixes f::"real \<Rightarrow> real"
shows "onorm (\<lambda>x. vec1 (f (dest_vec1 x))) = onorm f" proof-
have "\<forall>x::real^1. norm x = 1 \<longleftrightarrow> x\<in>{vec1 -1, vec1 (1::real)}" unfolding forall_vec1 by(auto simp add:Cart_eq)
--- a/src/HOL/Multivariate_Analysis/Determinants.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy Wed Mar 03 10:40:40 2010 -0800
@@ -837,7 +837,7 @@
unfolding orthogonal_transformation_def
apply auto
apply (erule_tac x=v in allE)+
- apply (simp add: real_vector_norm_def)
+ apply (simp add: norm_eq_sqrt_inner)
by (simp add: dot_norm linear_add[symmetric])
definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow> transpose Q ** Q = mat 1 \<and> Q ** transpose Q = mat 1"
@@ -879,7 +879,7 @@
by simp_all
from fd[rule_format, of "basis i" "basis j", unfolded matrix_works[OF lf, symmetric] dot_matrix_vector_mul]
have "?A$i$j = ?m1 $ i $ j"
- by (simp add: dot_def matrix_matrix_mult_def columnvector_def rowvector_def basis_def th0 setsum_delta[OF fU] mat_def)}
+ by (simp add: inner_vector_def matrix_matrix_mult_def columnvector_def rowvector_def basis_def th0 setsum_delta[OF fU] mat_def)}
hence "orthogonal_matrix ?mf" unfolding orthogonal_matrix by vector
with lf have ?rhs by blast}
moreover
@@ -929,8 +929,7 @@
unfolding dot_norm_neg dist_norm[symmetric]
unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)}
note fc = this
- show ?thesis unfolding linear_def vector_eq
- by (simp add: dot_lmult dot_ladd dot_rmult dot_radd fc ring_simps)
+ show ?thesis unfolding linear_def vector_eq smult_conv_scaleR by (simp add: inner_simps fc ring_simps)
qed
lemma isometry_linear:
@@ -972,7 +971,7 @@
"x' = norm x *s x0'" "y' = norm y *s y0'"
"norm x0 = 1" "norm x0' = 1" "norm y0 = 1" "norm y0' = 1"
"norm(x0' - y0') = norm(x0 - y0)"
-
+ hence *:"x0 \<bullet> y0 = x0' \<bullet> y0' + y0' \<bullet> x0' - y0 \<bullet> x0 " by(simp add: norm_eq norm_eq_1 inner_simps)
have "norm(x' - y') = norm(x - y)"
apply (subst H(1))
apply (subst H(2))
@@ -980,9 +979,8 @@
apply (subst H(4))
using H(5-9)
apply (simp add: norm_eq norm_eq_1)
- apply (simp add: dot_lsub dot_rsub dot_lmult dot_rmult)
- apply (simp add: ring_simps)
- by (simp only: right_distrib[symmetric])}
+ apply (simp add: inner_simps smult_conv_scaleR) unfolding *
+ by (simp add: ring_simps) }
note th0 = this
let ?g = "\<lambda>x. if x = 0 then 0 else norm x *s f (inverse (norm x) *s x)"
{fix x:: "real ^'n" assume nx: "norm x = 1"
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Mar 03 10:40:40 2010 -0800
@@ -100,6 +100,12 @@
instance ..
end
+instantiation cart :: (scaleR, finite) scaleR
+begin
+ definition vector_scaleR_def: "scaleR = (\<lambda> r x. (\<chi> i. scaleR r (x$i)))"
+ instance ..
+end
+
instantiation cart :: (ord,finite) ord
begin
definition vector_le_def:
@@ -108,12 +114,31 @@
instance by (intro_classes)
end
-instantiation cart :: (scaleR, finite) scaleR
+text{* The ordering on real^1 is linear. *}
+
+class cart_one = assumes UNIV_one: "card (UNIV \<Colon> 'a set) = Suc 0"
begin
- definition vector_scaleR_def: "scaleR = (\<lambda> r x. (\<chi> i. scaleR r (x$i)))"
- instance ..
+ subclass finite
+ proof from UNIV_one show "finite (UNIV :: 'a set)"
+ by (auto intro!: card_ge_0_finite) qed
end
+instantiation num1 :: cart_one begin
+instance proof
+ show "CARD(1) = Suc 0" by auto
+qed end
+
+instantiation cart :: (linorder,cart_one) linorder begin
+instance proof
+ guess a B using UNIV_one[where 'a='b] unfolding card_Suc_eq apply- by(erule exE)+
+ hence *:"UNIV = {a}" by auto
+ have "\<And>P. (\<forall>i\<in>UNIV. P i) \<longleftrightarrow> P a" unfolding * by auto hence all:"\<And>P. (\<forall>i. P i) \<longleftrightarrow> P a" by auto
+ fix x y z::"'a^'b::cart_one" note * = vector_le_def vector_less_def all Cart_eq
+ show "x\<le>x" "(x < y) = (x \<le> y \<and> \<not> y \<le> x)" "x\<le>y \<or> y\<le>x" unfolding * by(auto simp only:field_simps)
+ { assume "x\<le>y" "y\<le>z" thus "x\<le>z" unfolding * by(auto simp only:field_simps) }
+ { assume "x\<le>y" "y\<le>x" thus "x=y" unfolding * by(auto simp only:field_simps) }
+qed end
+
text{* Also the scalar-vector multiplication. *}
definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a ^ 'n" (infixl "*s" 70)
@@ -123,25 +148,11 @@
definition "vec x = (\<chi> i. x)"
-text{* Dot products. *}
-
-definition dot :: "'a::{comm_monoid_add, times} ^ 'n \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a" (infix "\<bullet>" 70) where
- "x \<bullet> y = setsum (\<lambda>i. x$i * y$i) UNIV"
-
-lemma dot_1[simp]: "(x::'a::{comm_monoid_add, times}^1) \<bullet> y = (x$1) * (y$1)"
- by (simp add: dot_def setsum_1)
-
-lemma dot_2[simp]: "(x::'a::{comm_monoid_add, times}^2) \<bullet> y = (x$1) * (y$1) + (x$2) * (y$2)"
- by (simp add: dot_def setsum_2)
-
-lemma dot_3[simp]: "(x::'a::{comm_monoid_add, times}^3) \<bullet> y = (x$1) * (y$1) + (x$2) * (y$2) + (x$3) * (y$3)"
- by (simp add: dot_def setsum_3)
-
subsection {* A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space. *}
method_setup vector = {*
let
- val ss1 = HOL_basic_ss addsimps [@{thm dot_def}, @{thm setsum_addf} RS sym,
+ val ss1 = HOL_basic_ss addsimps [@{thm setsum_addf} RS sym,
@{thm setsum_subtractf} RS sym, @{thm setsum_right_distrib},
@{thm setsum_left_distrib}, @{thm setsum_negf} RS sym]
val ss2 = @{simpset} addsimps
@@ -165,8 +176,6 @@
lemma vec_0[simp]: "vec 0 = 0" by (vector vector_zero_def)
lemma vec_1[simp]: "vec 1 = 1" by (vector vector_one_def)
-
-
text{* Obvious "component-pushing". *}
lemma vec_component [simp]: "vec x $ i = x"
@@ -791,6 +800,8 @@
subsection {* Inner products *}
+abbreviation inner_bullet (infix "\<bullet>" 70) where "x \<bullet> y \<equiv> inner x y"
+
instantiation cart :: (real_inner, finite) real_inner
begin
@@ -821,27 +832,6 @@
end
-subsection{* Properties of the dot product. *}
-
-lemma dot_sym: "(x::'a:: {comm_monoid_add, ab_semigroup_mult} ^ 'n) \<bullet> y = y \<bullet> x"
- by (vector mult_commute)
-lemma dot_ladd: "((x::'a::ring ^ 'n) + y) \<bullet> z = (x \<bullet> z) + (y \<bullet> z)"
- by (vector ring_simps)
-lemma dot_radd: "x \<bullet> (y + (z::'a::ring ^ 'n)) = (x \<bullet> y) + (x \<bullet> z)"
- by (vector ring_simps)
-lemma dot_lsub: "((x::'a::ring ^ 'n) - y) \<bullet> z = (x \<bullet> z) - (y \<bullet> z)"
- by (vector ring_simps)
-lemma dot_rsub: "(x::'a::ring ^ 'n) \<bullet> (y - z) = (x \<bullet> y) - (x \<bullet> z)"
- by (vector ring_simps)
-lemma dot_lmult: "(c *s x) \<bullet> y = (c::'a::ring) * (x \<bullet> y)" by (vector ring_simps)
-lemma dot_rmult: "x \<bullet> (c *s y) = (c::'a::comm_ring) * (x \<bullet> y)" by (vector ring_simps)
-lemma dot_lneg: "(-x) \<bullet> (y::'a::ring ^ 'n) = -(x \<bullet> y)" by vector
-lemma dot_rneg: "(x::'a::ring ^ 'n) \<bullet> (-y) = -(x \<bullet> y)" by vector
-lemma dot_lzero[simp]: "0 \<bullet> x = (0::'a::{comm_monoid_add, mult_zero})" by vector
-lemma dot_rzero[simp]: "x \<bullet> 0 = (0::'a::{comm_monoid_add, mult_zero})" by vector
-lemma dot_pos_le[simp]: "(0::'a\<Colon>linordered_ring_strict) <= x \<bullet> x"
- by (simp add: dot_def setsum_nonneg)
-
lemma setsum_squares_eq_0_iff: assumes fS: "finite F" and fp: "\<forall>x \<in> F. f x \<ge> (0 ::'a::ordered_ab_group_add)" shows "setsum f F = 0 \<longleftrightarrow> (ALL x:F. f x = 0)"
using fS fp setsum_nonneg[OF fp]
proof (induct set: finite)
@@ -855,12 +845,6 @@
show ?case by (simp add: h)
qed
-lemma dot_eq_0: "x \<bullet> x = 0 \<longleftrightarrow> (x::'a::{linordered_ring_strict,ring_no_zero_divisors} ^ 'n) = 0"
- by (simp add: dot_def setsum_squares_eq_0_iff Cart_eq)
-
-lemma dot_pos_lt[simp]: "(0 < x \<bullet> x) \<longleftrightarrow> (x::'a::{linordered_ring_strict,ring_no_zero_divisors} ^ 'n) \<noteq> 0" using dot_eq_0[of x] dot_pos_le[of x]
- by (auto simp add: le_less)
-
subsection{* The collapse of the general concepts to dimension one. *}
lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"
@@ -994,12 +978,8 @@
lemma norm_mul[simp]: "norm(a *s x) = abs(a) * norm x"
by (simp add: norm_vector_def vector_component setL2_right_distrib
abs_mult cong: strong_setL2_cong)
-lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (x \<bullet> x = (0::real))"
- by (simp add: norm_vector_def dot_def setL2_def power2_eq_square)
-lemma real_vector_norm_def: "norm x = sqrt (x \<bullet> x)"
- by (simp add: norm_vector_def setL2_def dot_def power2_eq_square)
-lemma norm_pow_2: "norm x ^ 2 = x \<bullet> x"
- by (simp add: real_vector_norm_def)
+lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (inner x x = (0::real))"
+ by (simp add: norm_vector_def setL2_def power2_eq_square)
lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero)
lemma vector_mul_eq_0[simp]: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0"
by vector
@@ -1011,34 +991,17 @@
by (metis vector_mul_lcancel)
lemma vector_mul_rcancel_imp: "x \<noteq> 0 \<Longrightarrow> (a::real) *s x = b *s x ==> a = b"
by (metis vector_mul_rcancel)
+
lemma norm_cauchy_schwarz:
fixes x y :: "real ^ 'n"
- shows "x \<bullet> y <= norm x * norm y"
-proof-
- {assume "norm x = 0"
- hence ?thesis by (simp add: dot_lzero dot_rzero)}
- moreover
- {assume "norm y = 0"
- hence ?thesis by (simp add: dot_lzero dot_rzero)}
- moreover
- {assume h: "norm x \<noteq> 0" "norm y \<noteq> 0"
- let ?z = "norm y *s x - norm x *s y"
- from h have p: "norm x * norm y > 0" by (metis norm_ge_zero le_less zero_compare_simps)
- from dot_pos_le[of ?z]
- have "(norm x * norm y) * (x \<bullet> y) \<le> norm x ^2 * norm y ^2"
- apply (simp add: dot_rsub dot_lsub dot_lmult dot_rmult ring_simps)
- by (simp add: norm_pow_2[symmetric] power2_eq_square dot_sym)
- hence "x\<bullet>y \<le> (norm x ^2 * norm y ^2) / (norm x * norm y)" using p
- by (simp add: field_simps)
- hence ?thesis using h by (simp add: power2_eq_square)}
- ultimately show ?thesis by metis
-qed
+ shows "inner x y <= norm x * norm y"
+ using Cauchy_Schwarz_ineq2[of x y] by auto
lemma norm_cauchy_schwarz_abs:
fixes x y :: "real ^ 'n"
- shows "\<bar>x \<bullet> y\<bar> \<le> norm x * norm y"
+ shows "\<bar>inner x y\<bar> \<le> norm x * norm y"
using norm_cauchy_schwarz[of x y] norm_cauchy_schwarz[of x "-y"]
- by (simp add: real_abs_def dot_rneg)
+ by (simp add: real_abs_def)
lemma norm_triangle_sub:
fixes x y :: "'a::real_normed_vector"
@@ -1064,21 +1027,21 @@
lemma real_abs_sub_norm: "\<bar>norm (x::real ^ 'n) - norm y\<bar> <= norm(x - y)"
by (rule norm_triangle_ineq3)
lemma norm_le: "norm(x::real ^ 'n) <= norm(y) \<longleftrightarrow> x \<bullet> x <= y \<bullet> y"
- by (simp add: real_vector_norm_def)
+ by (simp add: norm_eq_sqrt_inner)
lemma norm_lt: "norm(x::real ^ 'n) < norm(y) \<longleftrightarrow> x \<bullet> x < y \<bullet> y"
- by (simp add: real_vector_norm_def)
-lemma norm_eq: "norm(x::real ^ 'n) = norm y \<longleftrightarrow> x \<bullet> x = y \<bullet> y"
- by (simp add: order_eq_iff norm_le)
+ by (simp add: norm_eq_sqrt_inner)
+lemma norm_eq: "norm(x::real ^ 'n) = norm (y::real ^ 'n) \<longleftrightarrow> x \<bullet> x = y \<bullet> y"
+ apply(subst order_eq_iff) unfolding norm_le by auto
lemma norm_eq_1: "norm(x::real ^ 'n) = 1 \<longleftrightarrow> x \<bullet> x = 1"
- by (simp add: real_vector_norm_def)
+ unfolding norm_eq_sqrt_inner by auto
text{* Squaring equations and inequalities involving norms. *}
lemma dot_square_norm: "x \<bullet> x = norm(x)^2"
- by (simp add: real_vector_norm_def)
+ by (simp add: norm_eq_sqrt_inner)
lemma norm_eq_square: "norm(x) = a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x = a^2"
- by (auto simp add: real_vector_norm_def)
+ by (auto simp add: norm_eq_sqrt_inner)
lemma real_abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> (x::real)^2 \<le> y^2"
proof-
@@ -1106,12 +1069,14 @@
text{* Dot product in terms of the norm rather than conversely. *}
+lemmas inner_simps = inner.add_left inner.add_right inner.diff_right inner.diff_left
+inner.scaleR_left inner.scaleR_right
+
lemma dot_norm: "x \<bullet> y = (norm(x + y) ^2 - norm x ^ 2 - norm y ^ 2) / 2"
- by (simp add: norm_pow_2 dot_ladd dot_radd dot_sym)
+ unfolding power2_norm_eq_inner inner_simps inner_commute by auto
lemma dot_norm_neg: "x \<bullet> y = ((norm x ^ 2 + norm y ^ 2) - norm(x - y) ^ 2) / 2"
- by (simp add: norm_pow_2 dot_ladd dot_radd dot_lsub dot_rsub dot_sym)
-
+ unfolding power2_norm_eq_inner inner_simps inner_commute by(auto simp add:group_simps)
text{* Equality of vectors in terms of @{term "op \<bullet>"} products. *}
@@ -1120,14 +1085,12 @@
assume "?lhs" then show ?rhs by simp
next
assume ?rhs
- then have "x \<bullet> x - x \<bullet> y = 0 \<and> x \<bullet> y - y\<bullet> y = 0" by simp
- hence "x \<bullet> (x - y) = 0 \<and> y \<bullet> (x - y) = 0"
- by (simp add: dot_rsub dot_lsub dot_sym)
- then have "(x - y) \<bullet> (x - y) = 0" by (simp add: ring_simps dot_lsub dot_rsub)
- then show "x = y" by (simp add: dot_eq_0)
+ then have "x \<bullet> x - x \<bullet> y = 0 \<and> x \<bullet> y - y \<bullet> y = 0" by simp
+ hence "x \<bullet> (x - y) = 0 \<and> y \<bullet> (x - y) = 0" by (simp add: inner_simps inner_commute)
+ then have "(x - y) \<bullet> (x - y) = 0" by (simp add: ring_simps inner_simps inner_commute)
+ then show "x = y" by (simp)
qed
-
subsection{* General linear decision procedure for normed spaces. *}
lemma norm_cmul_rule_thm:
@@ -1456,15 +1419,14 @@
finally show ?thesis .
qed
-lemma dot_lsum: "finite S \<Longrightarrow> setsum f S \<bullet> (y::'a::{comm_ring}^'n) = setsum (\<lambda>x. f x \<bullet> y) S "
- by (induct rule: finite_induct, auto simp add: dot_lzero dot_ladd dot_radd)
-
-lemma dot_rsum: "finite S \<Longrightarrow> (y::'a::{comm_ring}^'n) \<bullet> setsum f S = setsum (\<lambda>x. y \<bullet> f x) S "
- by (induct rule: finite_induct, auto simp add: dot_rzero dot_radd)
+lemma dot_lsum: "finite S \<Longrightarrow> setsum f S \<bullet> (y::'a::{real_inner}^'n) = setsum (\<lambda>x. f x \<bullet> y) S "
+ apply(induct rule: finite_induct) by(auto simp add: inner_simps)
+
+lemma dot_rsum: "finite S \<Longrightarrow> (y::'a::{real_inner}^'n) \<bullet> setsum f S = setsum (\<lambda>x. y \<bullet> f x) S "
+ apply(induct rule: finite_induct) by(auto simp add: inner_simps)
subsection{* Basis vectors in coordinate directions. *}
-
definition "basis k = (\<chi> i. if i = k then 1 else 0)"
lemma basis_component [simp]: "basis k $ i = (if k=i then 1 else 0)"
@@ -1475,11 +1437,9 @@
lemma norm_basis:
shows "norm (basis k :: real ^'n) = 1"
- apply (simp add: basis_def real_vector_norm_def dot_def)
+ apply (simp add: basis_def norm_eq_sqrt_inner) unfolding inner_vector_def
apply (vector delta_mult_idempotent)
- using setsum_delta[of "UNIV :: 'n set" "k" "\<lambda>k. 1::real"]
- apply auto
- done
+ using setsum_delta[of "UNIV :: 'n set" "k" "\<lambda>k. 1::real"] by auto
lemma norm_basis_1: "norm(basis 1 :: real ^'n::{finite,one}) = 1"
by (rule norm_basis)
@@ -1515,8 +1475,8 @@
by auto
lemma dot_basis:
- shows "basis i \<bullet> x = x$i" "x \<bullet> (basis i :: 'a^'n) = (x$i :: 'a::semiring_1)"
- by (auto simp add: dot_def basis_def cond_application_beta cond_value_iff setsum_delta cong del: if_weak_cong)
+ shows "basis i \<bullet> x = x$i" "x \<bullet> (basis i) = (x$i)"
+ unfolding inner_vector_def by (auto simp add: basis_def cond_application_beta cond_value_iff setsum_delta cong del: if_weak_cong)
lemma inner_basis:
fixes x :: "'a::{real_inner, real_algebra_1} ^ 'n"
@@ -1532,7 +1492,7 @@
shows "basis k \<noteq> (0:: 'a::semiring_1 ^'n)"
by (simp add: basis_eq_0)
-lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = (z::'a::semiring_1^'n)"
+lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = (z::real^'n)"
apply (auto simp add: Cart_eq dot_basis)
apply (erule_tac x="basis i" in allE)
apply (simp add: dot_basis)
@@ -1541,7 +1501,7 @@
apply (simp add: Cart_eq)
done
-lemma vector_eq_rdot: "(\<forall>z. x \<bullet> z = y \<bullet> z) \<longleftrightarrow> x = (y::'a::semiring_1^'n)"
+lemma vector_eq_rdot: "(\<forall>z. x \<bullet> z = y \<bullet> z) \<longleftrightarrow> x = (y::real^'n)"
apply (auto simp add: Cart_eq dot_basis)
apply (erule_tac x="basis i" in allE)
apply (simp add: dot_basis)
@@ -1555,31 +1515,29 @@
definition "orthogonal x y \<longleftrightarrow> (x \<bullet> y = 0)"
lemma orthogonal_basis:
- shows "orthogonal (basis i :: 'a^'n) x \<longleftrightarrow> x$i = (0::'a::ring_1)"
- by (auto simp add: orthogonal_def dot_def basis_def cond_value_iff cond_application_beta setsum_delta cong del: if_weak_cong)
+ shows "orthogonal (basis i) x \<longleftrightarrow> x$i = (0::real)"
+ by (auto simp add: orthogonal_def inner_vector_def basis_def cond_value_iff cond_application_beta setsum_delta cong del: if_weak_cong)
lemma orthogonal_basis_basis:
- shows "orthogonal (basis i :: 'a::ring_1^'n) (basis j) \<longleftrightarrow> i \<noteq> j"
+ shows "orthogonal (basis i :: real^'n) (basis j) \<longleftrightarrow> i \<noteq> j"
unfolding orthogonal_basis[of i] basis_component[of j] by simp
(* FIXME : Maybe some of these require less than comm_ring, but not all*)
lemma orthogonal_clauses:
- "orthogonal a (0::'a::comm_ring ^'n)"
- "orthogonal a x ==> orthogonal a (c *s x)"
+ "orthogonal a (0::real ^'n)"
+ "orthogonal a x ==> orthogonal a (c *\<^sub>R x)"
"orthogonal a x ==> orthogonal a (-x)"
"orthogonal a x \<Longrightarrow> orthogonal a y ==> orthogonal a (x + y)"
"orthogonal a x \<Longrightarrow> orthogonal a y ==> orthogonal a (x - y)"
"orthogonal 0 a"
- "orthogonal x a ==> orthogonal (c *s x) a"
+ "orthogonal x a ==> orthogonal (c *\<^sub>R x) a"
"orthogonal x a ==> orthogonal (-x) a"
"orthogonal x a \<Longrightarrow> orthogonal y a ==> orthogonal (x + y) a"
"orthogonal x a \<Longrightarrow> orthogonal y a ==> orthogonal (x - y) a"
- unfolding orthogonal_def dot_rneg dot_rmult dot_radd dot_rsub
- dot_lzero dot_rzero dot_lneg dot_lmult dot_ladd dot_lsub
- by simp_all
-
-lemma orthogonal_commute: "orthogonal (x::'a::{ab_semigroup_mult,comm_monoid_add} ^'n)y \<longleftrightarrow> orthogonal y x"
- by (simp add: orthogonal_def dot_sym)
+ unfolding orthogonal_def inner_simps by auto
+
+lemma orthogonal_commute: "orthogonal (x::real ^'n)y \<longleftrightarrow> orthogonal y x"
+ by (simp add: orthogonal_def inner_commute)
subsection{* Explicit vector construction from lists. *}
@@ -1969,7 +1927,7 @@
lemma choice_iff: "(\<forall>x. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x. P x (f x))" by metis
lemma adjoint_works_lemma:
- fixes f:: "'a::ring_1 ^'n \<Rightarrow> 'a ^'m"
+ fixes f:: "real ^'n \<Rightarrow> real ^'m"
assumes lf: "linear f"
shows "\<forall>x y. f x \<bullet> y = x \<bullet> adjoint f y"
proof-
@@ -1977,8 +1935,8 @@
let ?M = "UNIV :: 'm set"
have fN: "finite ?N" by simp
have fM: "finite ?M" by simp
- {fix y:: "'a ^ 'm"
- let ?w = "(\<chi> i. (f (basis i) \<bullet> y)) :: 'a ^ 'n"
+ {fix y:: "real ^ 'm"
+ let ?w = "(\<chi> i. (f (basis i) \<bullet> y)) :: real ^ 'n"
{fix x
have "f x \<bullet> y = f (setsum (\<lambda>i. (x$i) *s basis i) ?N) \<bullet> y"
by (simp only: basis_expansion)
@@ -1987,7 +1945,7 @@
by (simp add: linear_cmul[OF lf])
finally have "f x \<bullet> y = x \<bullet> ?w"
apply (simp only: )
- apply (simp add: dot_def setsum_left_distrib setsum_right_distrib setsum_commute[of _ ?M ?N] ring_simps)
+ apply (simp add: inner_vector_def setsum_left_distrib setsum_right_distrib setsum_commute[of _ ?M ?N] ring_simps)
done}
}
then show ?thesis unfolding adjoint_def
@@ -1997,34 +1955,34 @@
qed
lemma adjoint_works:
- fixes f:: "'a::ring_1 ^'n \<Rightarrow> 'a ^'m"
+ fixes f:: "real ^'n \<Rightarrow> real ^'m"
assumes lf: "linear f"
shows "x \<bullet> adjoint f y = f x \<bullet> y"
using adjoint_works_lemma[OF lf] by metis
-
lemma adjoint_linear:
- fixes f :: "'a::comm_ring_1 ^'n \<Rightarrow> 'a ^'m"
+ fixes f:: "real ^'n \<Rightarrow> real ^'m"
assumes lf: "linear f"
shows "linear (adjoint f)"
- by (simp add: linear_def vector_eq_ldot[symmetric] dot_radd dot_rmult adjoint_works[OF lf])
+ unfolding linear_def vector_eq_ldot[symmetric] apply safe
+ unfolding inner_simps smult_conv_scaleR adjoint_works[OF lf] by auto
lemma adjoint_clauses:
- fixes f:: "'a::comm_ring_1 ^'n \<Rightarrow> 'a ^'m"
+ fixes f:: "real ^'n \<Rightarrow> real ^'m"
assumes lf: "linear f"
shows "x \<bullet> adjoint f y = f x \<bullet> y"
and "adjoint f y \<bullet> x = y \<bullet> f x"
- by (simp_all add: adjoint_works[OF lf] dot_sym )
+ by (simp_all add: adjoint_works[OF lf] inner_commute)
lemma adjoint_adjoint:
- fixes f:: "'a::comm_ring_1 ^ 'n \<Rightarrow> 'a ^'m"
+ fixes f:: "real ^'n \<Rightarrow> real ^'m"
assumes lf: "linear f"
shows "adjoint (adjoint f) = f"
apply (rule ext)
by (simp add: vector_eq_ldot[symmetric] adjoint_clauses[OF adjoint_linear[OF lf]] adjoint_clauses[OF lf])
lemma adjoint_unique:
- fixes f:: "'a::comm_ring_1 ^ 'n \<Rightarrow> 'a ^'m"
+ fixes f:: "real ^'n \<Rightarrow> real ^'m"
assumes lf: "linear f" and u: "\<forall>x y. f' x \<bullet> y = x \<bullet> f y"
shows "f' = adjoint f"
apply (rule ext)
@@ -2101,11 +2059,11 @@
by (auto simp add: basis_def cond_value_iff cond_application_beta setsum_delta[OF finite] cong del: if_weak_cong)
lemma matrix_vector_mul_component:
- shows "((A::'a::semiring_1^_^_) *v x)$k = (A$k) \<bullet> x"
- by (simp add: matrix_vector_mult_def dot_def)
-
-lemma dot_lmul_matrix: "((x::'a::comm_semiring_1 ^_) v* A) \<bullet> y = x \<bullet> (A *v y)"
- apply (simp add: dot_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib mult_ac)
+ shows "((A::real^_^_) *v x)$k = (A$k) \<bullet> x"
+ by (simp add: matrix_vector_mult_def inner_vector_def)
+
+lemma dot_lmul_matrix: "((x::real ^_) v* A) \<bullet> y = x \<bullet> (A *v y)"
+ apply (simp add: inner_vector_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib mult_ac)
apply (subst setsum_commute)
by simp
@@ -2133,7 +2091,7 @@
text{* Two sometimes fruitful ways of looking at matrix-vector multiplication. *}
lemma matrix_mult_dot: "A *v x = (\<chi> i. A$i \<bullet> x)"
- by (simp add: matrix_vector_mult_def dot_def)
+ by (simp add: matrix_vector_mult_def inner_vector_def)
lemma matrix_mult_vsum: "(A::'a::comm_semiring_1^'n^'m) *v x = setsum (\<lambda>i. (x$i) *s column i A) (UNIV:: 'n set)"
by (simp add: matrix_vector_mult_def Cart_eq column_def mult_commute)
@@ -2194,15 +2152,15 @@
lemma matrix_vector_column:"(A::'a::comm_semiring_1^'n^_) *v x = setsum (\<lambda>i. (x$i) *s ((transpose A)$i)) (UNIV:: 'n set)"
by (simp add: matrix_vector_mult_def transpose_def Cart_eq mult_commute)
-lemma adjoint_matrix: "adjoint(\<lambda>x. (A::'a::comm_ring_1^'n^'m) *v x) = (\<lambda>x. transpose A *v x)"
+lemma adjoint_matrix: "adjoint(\<lambda>x. (A::real^'n^'m) *v x) = (\<lambda>x. transpose A *v x)"
apply (rule adjoint_unique[symmetric])
apply (rule matrix_vector_mul_linear)
- apply (simp add: transpose_def dot_def matrix_vector_mult_def setsum_left_distrib setsum_right_distrib)
+ apply (simp add: transpose_def inner_vector_def matrix_vector_mult_def setsum_left_distrib setsum_right_distrib)
apply (subst setsum_commute)
apply (auto simp add: mult_ac)
done
-lemma matrix_adjoint: assumes lf: "linear (f :: 'a::comm_ring_1^'n \<Rightarrow> 'a ^'m)"
+lemma matrix_adjoint: assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'m)"
shows "matrix(adjoint f) = transpose(matrix f)"
apply (subst matrix_vector_mul[OF lf])
unfolding adjoint_matrix matrix_of_matrix_vector_mul ..
@@ -2514,11 +2472,11 @@
apply (auto simp add: Cart_eq matrix_vector_mult_def column_def mult_commute UNIV_1)
done
-lemma linear_to_scalars: assumes lf: "linear (f::'a::comm_ring_1 ^'n \<Rightarrow> 'a^1)"
+lemma linear_to_scalars: assumes lf: "linear (f::real ^'n \<Rightarrow> real^1)"
shows "f = (\<lambda>x. vec1(row 1 (matrix f) \<bullet> x))"
apply (rule ext)
apply (subst matrix_works[OF lf, symmetric])
- apply (simp add: Cart_eq matrix_vector_mult_def row_def dot_def mult_commute forall_1)
+ apply (simp add: Cart_eq matrix_vector_mult_def row_def inner_vector_def mult_commute forall_1)
done
lemma dest_vec1_eq_0: "dest_vec1 x = 0 \<longleftrightarrow> x = 0"
@@ -2624,11 +2582,11 @@
have th0: "norm x = norm (pastecart (fstcart x) (sndcart x))"
by (simp add: pastecart_fst_snd)
have th1: "fstcart x \<bullet> fstcart x \<le> pastecart (fstcart x) (sndcart x) \<bullet> pastecart (fstcart x) (sndcart x)"
- by (simp add: dot_def setsum_UNIV_sum pastecart_def setsum_nonneg)
+ by (simp add: inner_vector_def setsum_UNIV_sum pastecart_def setsum_nonneg)
then show ?thesis
unfolding th0
- unfolding real_vector_norm_def real_sqrt_le_iff id_def
- by (simp add: dot_def)
+ unfolding norm_eq_sqrt_inner real_sqrt_le_iff id_def
+ by (simp add: inner_vector_def)
qed
lemma dist_fstcart: "dist(fstcart (x::real^_)) (fstcart y) <= dist x y"
@@ -2639,18 +2597,18 @@
have th0: "norm x = norm (pastecart (fstcart x) (sndcart x))"
by (simp add: pastecart_fst_snd)
have th1: "sndcart x \<bullet> sndcart x \<le> pastecart (fstcart x) (sndcart x) \<bullet> pastecart (fstcart x) (sndcart x)"
- by (simp add: dot_def setsum_UNIV_sum pastecart_def setsum_nonneg)
+ by (simp add: inner_vector_def setsum_UNIV_sum pastecart_def setsum_nonneg)
then show ?thesis
unfolding th0
- unfolding real_vector_norm_def real_sqrt_le_iff id_def
- by (simp add: dot_def)
+ unfolding norm_eq_sqrt_inner real_sqrt_le_iff id_def
+ by (simp add: inner_vector_def)
qed
lemma dist_sndcart: "dist(sndcart (x::real^_)) (sndcart y) <= dist x y"
unfolding dist_norm by (metis sndcart_sub[symmetric] norm_sndcart)
-lemma dot_pastecart: "(pastecart (x1::'a::{times,comm_monoid_add}^'n) (x2::'a::{times,comm_monoid_add}^'m)) \<bullet> (pastecart y1 y2) = x1 \<bullet> y1 + x2 \<bullet> y2"
- by (simp add: dot_def setsum_UNIV_sum pastecart_def)
+lemma dot_pastecart: "(pastecart (x1::real^'n) (x2::real^'m)) \<bullet> (pastecart y1 y2) = x1 \<bullet> y1 + x2 \<bullet> y2"
+ by (simp add: inner_vector_def setsum_UNIV_sum pastecart_def)
text {* TODO: move to NthRoot *}
lemma sqrt_add_le_add_sqrt:
@@ -3586,8 +3544,8 @@
{fix x assume xs: "x \<in> s"
have t: "t \<subseteq> (insert b (insert a (t -{b})))" using b by auto
from b(1) have "b \<in> span t" by (simp add: span_superset)
- have bs: "b \<in> span (insert a (t - {b}))"
- by (metis in_span_delete a sp mem_def subset_eq)
+ have bs: "b \<in> span (insert a (t - {b}))" apply(rule in_span_delete)
+ using a sp unfolding subset_eq by auto
from xs sp have "x \<in> span t" by blast
with span_mono[OF t]
have x: "x \<in> span (insert b (insert a (t - {b})))" ..
@@ -3842,11 +3800,8 @@
(* FIXME : Move to some general theory ?*)
definition "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y\<in> S. x\<noteq>y \<longrightarrow> R x y)"
-lemma vector_sub_project_orthogonal: "(b::'a::linordered_field^'n) \<bullet> (x - ((b \<bullet> x) / (b\<bullet>b)) *s b) = 0"
- apply (cases "b = 0", simp)
- apply (simp add: dot_rsub dot_rmult)
- unfolding times_divide_eq_right[symmetric]
- by (simp add: field_simps dot_eq_0)
+lemma vector_sub_project_orthogonal: "(b::real^'n) \<bullet> (x - ((b \<bullet> x) / (b \<bullet> b)) *s b) = 0"
+ unfolding inner_simps smult_conv_scaleR by auto
lemma basis_orthogonal:
fixes B :: "(real ^'n) set"
@@ -3861,7 +3816,7 @@
from `\<exists>C. finite C \<and> card C \<le> card B \<and> span C = span B \<and> pairwise orthogonal C`
obtain C where C: "finite C" "card C \<le> card B"
"span C = span B" "pairwise orthogonal C" by blast
- let ?a = "a - setsum (\<lambda>x. (x\<bullet>a / (x\<bullet>x)) *s x) C"
+ let ?a = "a - setsum (\<lambda>x. (x \<bullet> a / (x \<bullet> x)) *s x) C"
let ?C = "insert ?a C"
from C(1) have fC: "finite ?C" by simp
from fB aB C(1,2) have cC: "card ?C \<le> card (insert a B)" by (simp add: card_insert_if)
@@ -3887,13 +3842,12 @@
have fth: "finite (C - {y})" using C by simp
have "orthogonal x y"
using xa ya
- unfolding orthogonal_def xa dot_lsub dot_rsub diff_eq_0_iff_eq
+ unfolding orthogonal_def xa inner_simps diff_eq_0_iff_eq
apply simp
apply (subst Cy)
using C(1) fth
- apply (simp only: setsum_clauses)
- thm dot_ladd
- apply (auto simp add: dot_ladd dot_radd dot_lmult dot_rmult dot_eq_0 dot_sym[of y a] dot_lsum[OF fth])
+ apply (simp only: setsum_clauses) unfolding smult_conv_scaleR
+ apply (auto simp add: inner_simps inner_eq_zero_iff inner_commute[of y a] dot_lsum[OF fth])
apply (rule setsum_0')
apply clarsimp
apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
@@ -3904,13 +3858,13 @@
have fth: "finite (C - {x})" using C by simp
have "orthogonal x y"
using xa ya
- unfolding orthogonal_def ya dot_rsub dot_lsub diff_eq_0_iff_eq
+ unfolding orthogonal_def ya inner_simps diff_eq_0_iff_eq
apply simp
apply (subst Cx)
using C(1) fth
- apply (simp only: setsum_clauses)
- apply (subst dot_sym[of x])
- apply (auto simp add: dot_radd dot_rmult dot_eq_0 dot_sym[of x a] dot_rsum[OF fth])
+ apply (simp only: setsum_clauses) unfolding smult_conv_scaleR
+ apply (subst inner_commute[of x])
+ apply (auto simp add: inner_simps inner_eq_zero_iff inner_commute[of x a] dot_rsum[OF fth])
apply (rule setsum_0')
apply clarsimp
apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
@@ -3945,7 +3899,8 @@
qed
lemma span_eq: "span S = span T \<longleftrightarrow> S \<subseteq> span T \<and> T \<subseteq> span S"
- by (metis set_eq_subset span_mono span_span span_inc) (* FIXME: slow *)
+ using span_inc[unfolded subset_eq] using span_mono[of T "span S"] span_mono[of S "span T"]
+ by(auto simp add: span_span)
(* ------------------------------------------------------------------------- *)
(* Low-dimensional subset is in a hyperplane (weak orthogonal complement). *)
@@ -3962,8 +3917,8 @@
from B have fB: "finite B" "card B = dim S" using independent_bound by auto
from span_mono[OF B(2)] span_mono[OF B(3)]
have sSB: "span S = span B" by (simp add: span_span)
- let ?a = "a - setsum (\<lambda>b. (a\<bullet>b / (b\<bullet>b)) *s b) B"
- have "setsum (\<lambda>b. (a\<bullet>b / (b\<bullet>b)) *s b) B \<in> span S"
+ let ?a = "a - setsum (\<lambda>b. (a \<bullet> b / (b \<bullet> b)) *s b) B"
+ have "setsum (\<lambda>b. (a \<bullet> b / (b \<bullet> b)) *s b) B \<in> span S"
unfolding sSB
apply (rule span_setsum[OF fB(1)])
apply clarsimp
@@ -3972,20 +3927,20 @@
with a have a0:"?a \<noteq> 0" by auto
have "\<forall>x\<in>span B. ?a \<bullet> x = 0"
proof(rule span_induct')
- show "subspace (\<lambda>x. ?a \<bullet> x = 0)"
- by (auto simp add: subspace_def mem_def dot_radd dot_rmult)
- next
+ show "subspace (\<lambda>x. ?a \<bullet> x = 0)" by (auto simp add: subspace_def mem_def inner_simps smult_conv_scaleR)
+
+next
{fix x assume x: "x \<in> B"
from x have B': "B = insert x (B - {x})" by blast
have fth: "finite (B - {x})" using fB by simp
have "?a \<bullet> x = 0"
apply (subst B') using fB fth
unfolding setsum_clauses(2)[OF fth]
- apply simp
- apply (clarsimp simp add: dot_lsub dot_ladd dot_lmult dot_lsum dot_eq_0)
+ apply simp unfolding inner_simps smult_conv_scaleR
+ apply (clarsimp simp add: inner_simps inner_eq_zero_iff smult_conv_scaleR dot_lsum)
apply (rule setsum_0', rule ballI)
- unfolding dot_sym
- by (auto simp add: x field_simps dot_eq_0 intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])}
+ unfolding inner_commute
+ by (auto simp add: x field_simps inner_eq_zero_iff intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])}
then show "\<forall>x \<in> B. ?a \<bullet> x = 0" by blast
qed
with a0 show ?thesis unfolding sSB by (auto intro: exI[where x="?a"])
@@ -4754,8 +4709,8 @@
"columnvector (A *v v) = A ** columnvector v"
by (vector columnvector_def matrix_matrix_mult_def matrix_vector_mult_def)
-lemma dot_matrix_product: "(x::'a::semiring_1^'n) \<bullet> y = (((rowvector x ::'a^'n^1) ** (columnvector y :: 'a^1^'n))$1)$1"
- by (vector matrix_matrix_mult_def rowvector_def columnvector_def dot_def)
+lemma dot_matrix_product: "(x::real^'n) \<bullet> y = (((rowvector x ::real^'n^1) ** (columnvector y :: real^1^'n))$1)$1"
+ by (vector matrix_matrix_mult_def rowvector_def columnvector_def inner_vector_def)
lemma dot_matrix_vector_mul:
fixes A B :: "real ^'n ^'n" and x y :: "real ^'n"
@@ -4911,20 +4866,18 @@
by (auto intro: real_sqrt_pow2)
have th: "sqrt (real ?d) * infnorm x \<ge> 0"
by (simp add: zero_le_mult_iff real_sqrt_ge_0_iff infnorm_pos_le)
- have th1: "x\<bullet>x \<le> (sqrt (real ?d) * infnorm x)^2"
+ have th1: "x \<bullet> x \<le> (sqrt (real ?d) * infnorm x)^2"
unfolding power_mult_distrib d2
+ unfolding real_of_nat_def inner_vector_def
+ apply (subst power2_abs[symmetric])
+ apply (rule setsum_bounded)
+ apply(auto simp add: power2_eq_square[symmetric])
apply (subst power2_abs[symmetric])
- unfolding real_of_nat_def dot_def power2_eq_square[symmetric]
- apply (subst power2_abs[symmetric])
- apply (rule setsum_bounded)
apply (rule power_mono)
- unfolding abs_of_nonneg[OF infnorm_pos_le]
unfolding infnorm_def Sup_finite_ge_iff[OF infnorm_set_lemma]
- unfolding infnorm_set_image bex_simps
- apply blast
- by (rule abs_ge_zero)
- from real_le_lsqrt[OF dot_pos_le th th1]
- show ?thesis unfolding real_vector_norm_def id_def .
+ unfolding infnorm_set_image bex_simps apply(rule_tac x=i in exI) by auto
+ from real_le_lsqrt[OF inner_ge_zero th th1]
+ show ?thesis unfolding norm_eq_sqrt_inner id_def .
qed
(* Equality in Cauchy-Schwarz and triangle inequalities. *)
@@ -4938,16 +4891,14 @@
hence ?thesis by simp}
moreover
{assume x: "x \<noteq> 0" and y: "y \<noteq> 0"
- from dot_eq_0[of "norm y *s x - norm x *s y"]
+ from inner_eq_zero_iff[of "norm y *s x - norm x *s y"]
have "?rhs \<longleftrightarrow> (norm y * (norm y * norm x * norm x - norm x * (x \<bullet> y)) - norm x * (norm y * (y \<bullet> x) - norm x * norm y * norm y) = 0)"
using x y
- unfolding dot_rsub dot_lsub dot_lmult dot_rmult
- unfolding norm_pow_2[symmetric] power2_eq_square diff_eq_0_iff_eq apply (simp add: dot_sym)
- apply (simp add: ring_simps)
- apply metis
- done
+ unfolding inner_simps smult_conv_scaleR
+ unfolding power2_norm_eq_inner[symmetric] power2_eq_square diff_eq_0_iff_eq apply (simp add: inner_commute)
+ apply (simp add: ring_simps) by metis
also have "\<dots> \<longleftrightarrow> (2 * norm x * norm y * (norm x * norm y - x \<bullet> y) = 0)" using x y
- by (simp add: ring_simps dot_sym)
+ by (simp add: ring_simps inner_commute)
also have "\<dots> \<longleftrightarrow> ?lhs" using x y
apply simp
by metis
@@ -4969,8 +4920,7 @@
unfolding norm_minus_cancel
norm_mul by blast
also have "\<dots> \<longleftrightarrow> ?lhs"
- unfolding th[OF mult_nonneg_nonneg, OF norm_ge_zero[of x] norm_ge_zero[of y]] dot_lneg
- by arith
+ unfolding th[OF mult_nonneg_nonneg, OF norm_ge_zero[of x] norm_ge_zero[of y]] inner_simps by auto
finally show ?thesis ..
qed
@@ -4993,8 +4943,8 @@
by arith
also have "\<dots> \<longleftrightarrow> norm x *s y = norm y *s x"
unfolding norm_cauchy_schwarz_eq[symmetric]
- unfolding norm_pow_2 dot_ladd dot_radd
- by (simp add: norm_pow_2[symmetric] power2_eq_square dot_sym ring_simps)
+ unfolding power2_norm_eq_inner inner_simps
+ by (simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute ring_simps)
finally have ?thesis .}
ultimately show ?thesis by blast
qed
@@ -5089,3 +5039,4 @@
done
end
+
\ No newline at end of file
--- a/src/HOL/Multivariate_Analysis/Integration.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Wed Mar 03 10:40:40 2010 -0800
@@ -1310,9 +1310,12 @@
lemma integral_empty[simp]: shows "integral {} f = 0"
apply(rule integral_unique) using has_integral_empty .
-lemma has_integral_refl[intro]: shows "(f has_integral 0) {a..a}"
- apply(rule has_integral_null) unfolding content_eq_0_interior
- unfolding interior_closed_interval using interval_sing by auto
+lemma has_integral_refl[intro]: shows "(f has_integral 0) {a..a}" "(f has_integral 0) {a}"
+proof- have *:"{a} = {a..a}" apply(rule set_ext) unfolding mem_interval singleton_iff Cart_eq
+ apply safe prefer 3 apply(erule_tac x=i in allE) by(auto simp add: field_simps)
+ show "(f has_integral 0) {a..a}" "(f has_integral 0) {a}" unfolding *
+ apply(rule_tac[!] has_integral_null) unfolding content_eq_0_interior
+ unfolding interior_closed_interval using interval_sing by auto qed
lemma integrable_on_refl[intro]: shows "f integrable_on {a..a}" unfolding integrable_on_def by auto
@@ -2811,6 +2814,9 @@
subsection {* Special case of additivity we need for the FCT. *}
+lemma interval_bound_sing[simp]: "interval_upperbound {a} = a" "interval_lowerbound {a} = a"
+ unfolding interval_upperbound_def interval_lowerbound_def unfolding Cart_eq by auto
+
lemma additive_tagged_division_1: fixes f::"real^1 \<Rightarrow> 'a::real_normed_vector"
assumes "dest_vec1 a \<le> dest_vec1 b" "p tagged_division_of {a..b}"
shows "setsum (\<lambda>(x,k). f(interval_upperbound k) - f(interval_lowerbound k)) p = f b - f a"
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Wed Mar 03 10:40:40 2010 -0800
@@ -54,7 +54,7 @@
(* quickcheck options *)
(*val quickcheck_generator = "SML"*)
-val iterations = 100
+val iterations = 10
val size = 5
exception RANDOM;
--- a/src/HOL/NanoJava/AxSem.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/NanoJava/AxSem.thy Wed Mar 03 10:40:40 2010 -0800
@@ -13,10 +13,10 @@
triple = "assn \<times> stmt \<times> assn"
etriple = "assn \<times> expr \<times> vassn"
translations
- "assn" \<leftharpoondown> (type)"state => bool"
- "vassn" \<leftharpoondown> (type)"val => assn"
- "triple" \<leftharpoondown> (type)"assn \<times> stmt \<times> assn"
- "etriple" \<leftharpoondown> (type)"assn \<times> expr \<times> vassn"
+ (type) "assn" \<leftharpoondown> (type) "state => bool"
+ (type) "vassn" \<leftharpoondown> (type) "val => assn"
+ (type) "triple" \<leftharpoondown> (type) "assn \<times> stmt \<times> assn"
+ (type) "etriple" \<leftharpoondown> (type) "assn \<times> expr \<times> vassn"
subsection "Hoare Logic Rules"
--- a/src/HOL/NanoJava/Decl.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/NanoJava/Decl.thy Wed Mar 03 10:40:40 2010 -0800
@@ -38,11 +38,11 @@
= "cdecl list"
translations
- "fdecl" \<leftharpoondown> (type)"fname \<times> ty"
- "mdecl" \<leftharpoondown> (type)"mname \<times> ty \<times> ty \<times> stmt"
- "class" \<leftharpoondown> (type)"cname \<times> fdecl list \<times> mdecl list"
- "cdecl" \<leftharpoondown> (type)"cname \<times> class"
- "prog " \<leftharpoondown> (type)"cdecl list"
+ (type) "fdecl" \<leftharpoondown> (type) "fname \<times> ty"
+ (type) "mdecl" \<leftharpoondown> (type) "mname \<times> ty \<times> ty \<times> stmt"
+ (type) "class" \<leftharpoondown> (type) "cname \<times> fdecl list \<times> mdecl list"
+ (type) "cdecl" \<leftharpoondown> (type) "cname \<times> class"
+ (type) "prog " \<leftharpoondown> (type) "cdecl list"
consts
--- a/src/HOL/NanoJava/State.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/NanoJava/State.thy Wed Mar 03 10:40:40 2010 -0800
@@ -23,9 +23,8 @@
obj = "cname \<times> fields"
translations
-
- "fields" \<leftharpoondown> (type)"fname => val option"
- "obj" \<leftharpoondown> (type)"cname \<times> fields"
+ (type) "fields" \<leftharpoondown> (type) "fname => val option"
+ (type) "obj" \<leftharpoondown> (type) "cname \<times> fields"
definition init_vars :: "('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> val)" where
"init_vars m == Option.map (\<lambda>T. Null) o m"
@@ -40,10 +39,9 @@
locals :: locals
translations
-
- "heap" \<leftharpoondown> (type)"loc => obj option"
- "locals" \<leftharpoondown> (type)"vname => val option"
- "state" \<leftharpoondown> (type)"(|heap :: heap, locals :: locals|)"
+ (type) "heap" \<leftharpoondown> (type) "loc => obj option"
+ (type) "locals" \<leftharpoondown> (type) "vname => val option"
+ (type) "state" \<leftharpoondown> (type) "(|heap :: heap, locals :: locals|)"
definition del_locs :: "state => state" where
"del_locs s \<equiv> s (| locals := empty |)"
--- a/src/HOL/Old_Number_Theory/Euler.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Old_Number_Theory/Euler.thy Wed Mar 03 10:40:40 2010 -0800
@@ -162,8 +162,11 @@
lemma aux2: "[| (a::int) < c; b < c |] ==> (a \<le> b | b \<le> a)"
by auto
+lemma d22set_induct_old: "(\<And>a::int. 1 < a \<longrightarrow> P (a - 1) \<Longrightarrow> P a) \<Longrightarrow> P x"
+using d22set.induct by blast
+
lemma SRStar_d22set_prop: "2 < p \<Longrightarrow> (SRStar p) = {1} \<union> (d22set (p - 1))"
- apply (induct p rule: d22set.induct)
+ apply (induct p rule: d22set_induct_old)
apply auto
apply (simp add: SRStar_def d22set.simps)
apply (simp add: SRStar_def d22set.simps, clarify)
--- a/src/HOL/Product_Type.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Product_Type.thy Wed Mar 03 10:40:40 2010 -0800
@@ -142,10 +142,10 @@
by rule+
qed
-syntax (xsymbols)
- "*" :: "[type, type] => type" ("(_ \<times>/ _)" [21, 20] 20)
-syntax (HTML output)
- "*" :: "[type, type] => type" ("(_ \<times>/ _)" [21, 20] 20)
+type_notation (xsymbols)
+ "*" ("(_ \<times>/ _)" [21, 20] 20)
+type_notation (HTML output)
+ "*" ("(_ \<times>/ _)" [21, 20] 20)
consts
Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b"
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Mar 03 10:40:40 2010 -0800
@@ -10,12 +10,10 @@
val test_ref :
((unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) option) Unsynchronized.ref
val tracing : bool Unsynchronized.ref;
- val quickcheck_compile_term : bool -> bool ->
+ val quickcheck_compile_term : bool -> bool -> int ->
Proof.context -> bool -> term -> int -> term list option * (bool list * bool);
(* val test_term : Proof.context -> bool -> int -> int -> int -> int -> term -> *)
- val quiet : bool Unsynchronized.ref;
val nrandom : int Unsynchronized.ref;
- val depth : int Unsynchronized.ref;
val debug : bool Unsynchronized.ref;
val function_flattening : bool Unsynchronized.ref;
val no_higher_order_predicate : string list Unsynchronized.ref;
@@ -31,19 +29,17 @@
val tracing = Unsynchronized.ref false;
-val target = "Quickcheck"
+val quiet = Unsynchronized.ref true;
-val quiet = Unsynchronized.ref false;
+val target = "Quickcheck"
val nrandom = Unsynchronized.ref 2;
-val depth = Unsynchronized.ref 8;
+val debug = Unsynchronized.ref false;
-val debug = Unsynchronized.ref false;
val function_flattening = Unsynchronized.ref true;
-
-val no_higher_order_predicate = Unsynchronized.ref [];
+val no_higher_order_predicate = Unsynchronized.ref ([] : string list);
val options = Options {
expected_modes = NONE,
@@ -231,21 +227,21 @@
(* quickcheck interface functions *)
-fun compile_term' options ctxt report t =
+fun compile_term' options depth ctxt report t =
let
val c = compile_term options ctxt t
val dummy_report = ([], false)
in
- fn size => (try_upto (!quiet) (c size (!nrandom)) (!depth), dummy_report)
+ fn size => (try_upto (!quiet) (c size (!nrandom)) depth, dummy_report)
end
-fun quickcheck_compile_term function_flattening fail_safe_function_flattening ctxt t =
+fun quickcheck_compile_term function_flattening fail_safe_function_flattening depth =
let
val options =
set_fail_safe_function_flattening fail_safe_function_flattening
(set_function_flattening function_flattening (get_options ()))
in
- compile_term' options ctxt t
+ compile_term' options depth
end
end;
--- a/src/HOL/Tools/numeral_syntax.ML Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Tools/numeral_syntax.ML Wed Mar 03 10:40:40 2010 -0800
@@ -69,7 +69,7 @@
in
-fun numeral_tr' show_sorts (*"number_of"*) (Type (@{type_syntax fun}, [_, T])) (t :: ts) =
+fun numeral_tr' show_sorts (*"number_of"*) (Type (@{type_name fun}, [_, T])) (t :: ts) =
let val t' =
if not (! show_types) andalso can Term.dest_Type T then syntax_numeral t
else Syntax.const Syntax.constrainC $ syntax_numeral t $ Syntax.term_of_typ show_sorts T
--- a/src/HOL/Tools/record.ML Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Tools/record.ML Wed Mar 03 10:40:40 2010 -0800
@@ -697,10 +697,8 @@
let
fun get_sort env xi =
the_default (Sign.defaultS thy) (AList.lookup (op =) env (xi: indexname));
- val map_sort = Sign.intern_sort thy;
in
- Syntax.typ_of_term (get_sort (Syntax.term_sorts map_sort t)) map_sort t
- |> Sign.intern_tycons thy
+ Syntax.typ_of_term (get_sort (Syntax.term_sorts t)) t
end;
@@ -752,8 +750,8 @@
val more' = mk_ext rest;
in
- (* FIXME authentic syntax *)
- list_comb (Syntax.const (suffix ext_typeN ext), alphas' @ [more'])
+ list_comb
+ (Syntax.const (Syntax.mark_type (suffix ext_typeN ext)), alphas' @ [more'])
end
| NONE => err ("no fields defined for " ^ ext))
| NONE => err (name ^ " is no proper field"))
@@ -857,7 +855,7 @@
val T = decode_type thy t;
val varifyT = varifyT (Term.maxidx_of_typ T);
- val term_of_type = Syntax.term_of_typ (! Syntax.show_sorts) o Sign.extern_typ thy;
+ val term_of_type = Syntax.term_of_typ (! Syntax.show_sorts);
fun strip_fields T =
(case T of
@@ -922,8 +920,7 @@
fun mk_type_abbr subst name alphas =
let val abbrT = Type (name, map (fn a => varifyT (TFree (a, Sign.defaultS thy))) alphas) in
- Syntax.term_of_typ (! Syntax.show_sorts)
- (Sign.extern_typ thy (Envir.norm_type subst abbrT))
+ Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT)
end;
fun match rT T = Sign.typ_match thy (varifyT rT, T) Vartab.empty;
@@ -946,14 +943,14 @@
fun record_ext_type_tr' name =
let
- val ext_type_name = suffix ext_typeN name;
+ val ext_type_name = Syntax.mark_type (suffix ext_typeN name);
fun tr' ctxt ts =
record_type_tr' ctxt (list_comb (Syntax.const ext_type_name, ts));
in (ext_type_name, tr') end;
fun record_ext_type_abbr_tr' abbr alphas zeta last_ext schemeT name =
let
- val ext_type_name = suffix ext_typeN name;
+ val ext_type_name = Syntax.mark_type (suffix ext_typeN name);
fun tr' ctxt ts =
record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt
(list_comb (Syntax.const ext_type_name, ts));
@@ -1949,8 +1946,7 @@
val (args', more) = chop_last args;
fun mk_ext' ((name, T), args) more = mk_ext (name, T) (args @ [more]);
fun build Ts =
- fold_rev mk_ext' (drop n ((extension_names ~~ Ts) ~~ chunks parent_chunks args'))
- more;
+ fold_rev mk_ext' (drop n ((extension_names ~~ Ts) ~~ chunks parent_chunks args')) more;
in
if more = HOLogic.unit
then build (map_range recT (parent_len + 1))
@@ -1960,27 +1956,25 @@
val r_rec0 = mk_rec all_vars_more 0;
val r_rec_unit0 = mk_rec (all_vars @ [HOLogic.unit]) 0;
- fun r n = Free (rN, rec_schemeT n)
+ fun r n = Free (rN, rec_schemeT n);
val r0 = r 0;
- fun r_unit n = Free (rN, recT n)
+ fun r_unit n = Free (rN, recT n);
val r_unit0 = r_unit 0;
- val w = Free (wN, rec_schemeT 0)
+ val w = Free (wN, rec_schemeT 0);
(* print translations *)
- val external_names = Name_Space.external_names (Sign.naming_of ext_thy);
-
val record_ext_type_abbr_tr's =
let
- val trnames = external_names (hd extension_names);
+ val trname = hd extension_names;
val last_ext = unsuffix ext_typeN (fst extension);
- in map (record_ext_type_abbr_tr' name alphas zeta last_ext rec_schemeT0) trnames end;
+ in [record_ext_type_abbr_tr' name alphas zeta last_ext rec_schemeT0 trname] end;
val record_ext_type_tr's =
let
(*avoid conflict with record_type_abbr_tr's*)
- val trnames = if parent_len > 0 then external_names extension_name else [];
+ val trnames = if parent_len > 0 then [extension_name] else [];
in map record_ext_type_tr' trnames end;
val advanced_print_translation =
--- a/src/HOL/Tools/typedef.ML Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Tools/typedef.ML Wed Mar 03 10:40:40 2010 -0800
@@ -118,7 +118,7 @@
fun add_def theory =
if def then
theory
- |> Sign.add_consts_i [(name, setT', NoSyn)] (* FIXME authentic syntax *)
+ |> Sign.add_consts_i [(name, setT', NoSyn)]
|> PureThy.add_defs false [((Thm.def_binding name, Logic.mk_equals (setC, set)), [])]
|-> (fn [th] => pair (SOME th))
else (NONE, theory);
--- a/src/HOL/Typerep.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/Typerep.thy Wed Mar 03 10:40:40 2010 -0800
@@ -33,7 +33,7 @@
typed_print_translation {*
let
fun typerep_tr' show_sorts (*"typerep"*)
- (Type (@{type_syntax fun}, [Type (@{type_syntax itself}, [T]), _]))
+ (Type (@{type_name fun}, [Type (@{type_name itself}, [T]), _]))
(Const (@{const_syntax TYPE}, _) :: ts) =
Term.list_comb
(Syntax.const @{syntax_const "_TYPEREP"} $ Syntax.term_of_typ show_sorts T, ts)
--- a/src/HOL/UNITY/Union.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/UNITY/Union.thy Wed Mar 03 10:40:40 2010 -0800
@@ -35,21 +35,22 @@
safety_prop :: "'a program set => bool"
"safety_prop X == SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
+notation (xsymbols)
+ SKIP ("\<bottom>") and
+ Join (infixl "\<squnion>" 65)
+
syntax
"_JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3JN _./ _)" 10)
"_JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3JN _:_./ _)" 10)
+syntax (xsymbols)
+ "_JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\<Squnion> _./ _)" 10)
+ "_JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\<Squnion> _\<in>_./ _)" 10)
translations
"JN x: A. B" == "CONST JOIN A (%x. B)"
"JN x y. B" == "JN x. JN y. B"
"JN x. B" == "CONST JOIN (CONST UNIV) (%x. B)"
-syntax (xsymbols)
- SKIP :: "'a program" ("\<bottom>")
- Join :: "['a program, 'a program] => 'a program" (infixl "\<squnion>" 65)
- "_JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\<Squnion> _./ _)" 10)
- "_JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\<Squnion> _\<in>_./ _)" 10)
-
subsection{*SKIP*}
--- a/src/HOL/ex/Numeral.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/ex/Numeral.thy Wed Mar 03 10:40:40 2010 -0800
@@ -327,7 +327,7 @@
val k = int_of_num' n;
val t' = Syntax.const @{syntax_const "_Numerals"} $ Syntax.free ("#" ^ string_of_int k);
in case T
- of Type (@{type_syntax fun}, [_, T']) =>
+ of Type (@{type_name fun}, [_, T']) =>
if not (! show_types) andalso can Term.dest_Type T' then t'
else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T'
| T' => if T' = dummyT then t' else raise Match
--- a/src/HOL/ex/Predicate_Compile_Quickcheck.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOL/ex/Predicate_Compile_Quickcheck.thy Wed Mar 03 10:40:40 2010 -0800
@@ -7,9 +7,9 @@
uses "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
begin
-setup {* Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term false true) *}
-setup {* Quickcheck.add_generator ("predicate_compile_ff_fs", Predicate_Compile_Quickcheck.quickcheck_compile_term true true) *}
-setup {* Quickcheck.add_generator ("predicate_compile_ff_nofs", Predicate_Compile_Quickcheck.quickcheck_compile_term true false) *}
+setup {* Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term false true 8) *}
+setup {* Quickcheck.add_generator ("predicate_compile_ff_fs", Predicate_Compile_Quickcheck.quickcheck_compile_term true true 8) *}
+setup {* Quickcheck.add_generator ("predicate_compile_ff_nofs", Predicate_Compile_Quickcheck.quickcheck_compile_term true false 8) *}
(*
datatype alphabet = a | b
--- a/src/HOLCF/One.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOLCF/One.thy Wed Mar 03 10:40:40 2010 -0800
@@ -10,7 +10,7 @@
types one = "unit lift"
translations
- "one" <= (type) "unit lift"
+ (type) "one" <= (type) "unit lift"
definition
ONE :: "one"
--- a/src/HOLCF/Representable.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOLCF/Representable.thy Wed Mar 03 10:40:40 2010 -0800
@@ -50,7 +50,7 @@
text "A TypeRep is an algebraic deflation over the universe of values."
types TypeRep = "udom alg_defl"
-translations "TypeRep" \<leftharpoondown> (type) "udom alg_defl"
+translations (type) "TypeRep" \<leftharpoondown> (type) "udom alg_defl"
definition
Rep_of :: "'a::rep itself \<Rightarrow> TypeRep"
@@ -60,7 +60,7 @@
(emb oo (approx i :: 'a \<rightarrow> 'a) oo prj)))"
syntax "_REP" :: "type \<Rightarrow> TypeRep" ("(1REP/(1'(_')))")
-translations "REP(t)" \<rightleftharpoons> "CONST Rep_of TYPE(t)"
+translations "REP('t)" \<rightleftharpoons> "CONST Rep_of TYPE('t)"
lemma cast_REP:
"cast\<cdot>REP('a::rep) = (emb::'a \<rightarrow> udom) oo (prj::udom \<rightarrow> 'a)"
--- a/src/HOLCF/Sprod.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOLCF/Sprod.thy Wed Mar 03 10:40:40 2010 -0800
@@ -22,10 +22,10 @@
instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
by (rule typedef_chfin [OF type_definition_Sprod below_Sprod_def])
-syntax (xsymbols)
- sprod :: "[type, type] => type" ("(_ \<otimes>/ _)" [21,20] 20)
-syntax (HTML output)
- sprod :: "[type, type] => type" ("(_ \<otimes>/ _)" [21,20] 20)
+type_notation (xsymbols)
+ sprod ("(_ \<otimes>/ _)" [21,20] 20)
+type_notation (HTML output)
+ sprod ("(_ \<otimes>/ _)" [21,20] 20)
lemma spair_lemma:
"(strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a) \<in> Sprod"
--- a/src/HOLCF/Ssum.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOLCF/Ssum.thy Wed Mar 03 10:40:40 2010 -0800
@@ -24,10 +24,11 @@
instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
by (rule typedef_chfin [OF type_definition_Ssum below_Ssum_def])
-syntax (xsymbols)
- ssum :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20)
-syntax (HTML output)
- ssum :: "[type, type] => type" ("(_ \<oplus>/ _)" [21, 20] 20)
+type_notation (xsymbols)
+ ssum ("(_ \<oplus>/ _)" [21, 20] 20)
+type_notation (HTML output)
+ ssum ("(_ \<oplus>/ _)" [21, 20] 20)
+
subsection {* Definitions of constructors *}
--- a/src/HOLCF/Tr.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOLCF/Tr.thy Wed Mar 03 10:40:40 2010 -0800
@@ -14,7 +14,7 @@
tr = "bool lift"
translations
- "tr" <= (type) "bool lift"
+ (type) "tr" <= (type) "bool lift"
definition
TT :: "tr" where
--- a/src/HOLCF/Up.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOLCF/Up.thy Wed Mar 03 10:40:40 2010 -0800
@@ -14,8 +14,8 @@
datatype 'a u = Ibottom | Iup 'a
-syntax (xsymbols)
- "u" :: "type \<Rightarrow> type" ("(_\<^sub>\<bottom>)" [1000] 999)
+type_notation (xsymbols)
+ u ("(_\<^sub>\<bottom>)" [1000] 999)
primrec Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b" where
"Ifup f Ibottom = \<bottom>"
--- a/src/HOLCF/ex/Strict_Fun.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOLCF/ex/Strict_Fun.thy Wed Mar 03 10:40:40 2010 -0800
@@ -12,8 +12,8 @@
= "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}"
by simp_all
-syntax (xsymbols)
- sfun :: "type \<Rightarrow> type \<Rightarrow> type" (infixr "\<rightarrow>!" 0)
+type_notation (xsymbols)
+ sfun (infixr "\<rightarrow>!" 0)
text {* TODO: Define nice syntax for abstraction, application. *}
--- a/src/HOLCF/holcf_logic.ML Wed Mar 03 08:49:11 2010 -0800
+++ b/src/HOLCF/holcf_logic.ML Wed Mar 03 10:40:40 2010 -0800
@@ -31,21 +31,14 @@
(* basic types *)
-fun mk_btyp t (S,T) = Type (t,[S,T]);
-
-local
- val intern_type = Sign.intern_type @{theory};
- val u = intern_type "u";
-in
+fun mk_btyp t (S, T) = Type (t, [S, T]);
-val cfun_arrow = intern_type "->";
+val cfun_arrow = @{type_name "cfun"};
val op ->> = mk_btyp cfun_arrow;
-val mk_ssumT = mk_btyp (intern_type "++");
-val mk_sprodT = mk_btyp (intern_type "**");
-fun mk_uT T = Type (u, [T]);
-val trT = Type (intern_type "tr" , []);
-val oneT = Type (intern_type "one", []);
+val mk_ssumT = mk_btyp (@{type_name "ssum"});
+val mk_sprodT = mk_btyp (@{type_name "sprod"});
+fun mk_uT T = Type (@{type_name u}, [T]);
+val trT = @{typ tr};
+val oneT = @{typ one};
end;
-
-end;
--- a/src/Pure/General/name_space.ML Wed Mar 03 08:49:11 2010 -0800
+++ b/src/Pure/General/name_space.ML Wed Mar 03 10:40:40 2010 -0800
@@ -46,7 +46,6 @@
val qualified_path: bool -> binding -> naming -> naming
val transform_binding: naming -> binding -> binding
val full_name: naming -> binding -> string
- val external_names: naming -> string -> string list
val declare: bool -> naming -> binding -> T -> string * T
type 'a table = T * 'a Symtab.table
val define: bool -> naming -> binding * 'a -> 'a table -> string * 'a table
@@ -309,8 +308,6 @@
val pfxs = mandatory_prefixes spec;
in pairself (map Long_Name.implode) (sfxs @ pfxs, sfxs) end;
-fun external_names naming = #2 o accesses naming o Binding.qualified_name;
-
(* declaration *)
--- a/src/Pure/Isar/local_syntax.ML Wed Mar 03 08:49:11 2010 -0800
+++ b/src/Pure/Isar/local_syntax.ML Wed Mar 03 10:40:40 2010 -0800
@@ -4,13 +4,11 @@
Local syntax depending on theory syntax.
*)
-val show_structs = Unsynchronized.ref false;
-
signature LOCAL_SYNTAX =
sig
type T
val syn_of: T -> Syntax.syntax
- val structs_of: T -> string list
+ val idents_of: T -> {structs: string list, fixes: string list}
val init: theory -> T
val rebuild: theory -> T -> T
datatype kind = Type | Const | Fixed
@@ -19,7 +17,6 @@
val restore_mode: T -> T -> T
val update_modesyntax: theory -> bool -> Syntax.mode ->
(kind * (string * typ * mixfix)) list -> T -> T
- val extern_term: T -> term -> term
end;
structure Local_Syntax: LOCAL_SYNTAX =
@@ -49,8 +46,7 @@
Syntax.eq_syntax (Sign.syn_of thy, thy_syntax);
fun syn_of (Syntax {local_syntax, ...}) = local_syntax;
-fun idents_of (Syntax {idents, ...}) = idents;
-val structs_of = #1 o idents_of;
+fun idents_of (Syntax {idents = (structs, fixes), ...}) = {structs = structs, fixes = fixes};
(* build syntax *)
@@ -125,21 +121,4 @@
fun update_modesyntax thy add mode args syntax =
syntax |> set_mode mode |> update_syntax add thy args |> restore_mode syntax;
-
-(* extern_term *)
-
-fun extern_term syntax =
- let
- val (structs, fixes) = idents_of syntax;
- fun map_free (t as Free (x, T)) =
- let val i = find_index (fn s => s = x) structs + 1 in
- if i = 0 andalso member (op =) fixes x then
- Term.Const (Syntax.mark_fixed x, T)
- else if i = 1 andalso not (! show_structs) then
- Syntax.const "_struct" $ Syntax.const "_indexdefault"
- else t
- end
- | map_free t = t;
- in Term.map_aterms map_free end;
-
end;
--- a/src/Pure/Isar/proof_context.ML Wed Mar 03 08:49:11 2010 -0800
+++ b/src/Pure/Isar/proof_context.ML Wed Mar 03 10:40:40 2010 -0800
@@ -363,15 +363,11 @@
(Pretty.str (setmp_CRITICAL show_question_marks true Term.string_of_vname (x', i))))
| NONE => Pretty.mark Markup.var (Pretty.str s));
-fun class_markup _ c = (* FIXME authentic syntax *)
- Pretty.mark (Markup.tclassN, []) (Pretty.str c);
-
fun plain_markup m _ s = Pretty.mark m (Pretty.str s);
val token_trans =
Syntax.tokentrans_mode ""
- [("class", class_markup),
- ("tfree", plain_markup Markup.tfree),
+ [("tfree", plain_markup Markup.tfree),
("tvar", plain_markup Markup.tvar),
("free", free_or_skolem),
("bound", plain_markup Markup.bound),
@@ -601,14 +597,12 @@
{get_sort = get_sort thy (Variable.def_sort ctxt),
map_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a)))
handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)),
- map_free = intern_skolem ctxt (Variable.def_type ctxt false),
- map_type = Sign.intern_tycons thy,
- map_sort = Sign.intern_sort thy}
+ map_free = intern_skolem ctxt (Variable.def_type ctxt false)}
end;
fun decode_term ctxt =
- let val {get_sort, map_const, map_free, map_type, map_sort} = term_context ctxt
- in Syntax.decode_term get_sort map_const map_free map_type map_sort end;
+ let val {get_sort, map_const, map_free} = term_context ctxt
+ in Syntax.decode_term get_sort map_const map_free end;
end;
@@ -677,26 +671,23 @@
fun parse_sort ctxt text =
let
val (syms, pos) = Syntax.parse_token Markup.sort text;
- val S = Syntax.standard_parse_sort ctxt (syn_of ctxt)
- (Sign.intern_sort (theory_of ctxt)) (syms, pos)
+ val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (syms, pos)
handle ERROR msg => cat_error msg ("Failed to parse sort" ^ Position.str_of pos)
in S end;
fun parse_typ ctxt text =
let
- val thy = ProofContext.theory_of ctxt;
+ val thy = theory_of ctxt;
val get_sort = get_sort thy (Variable.def_sort ctxt);
-
val (syms, pos) = Syntax.parse_token Markup.typ text;
- val T = Sign.intern_tycons thy
- (Syntax.standard_parse_typ ctxt (syn_of ctxt) get_sort (Sign.intern_sort thy) (syms, pos))
- handle ERROR msg => cat_error msg ("Failed to parse type" ^ Position.str_of pos);
+ val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) get_sort (syms, pos)
+ handle ERROR msg => cat_error msg ("Failed to parse type" ^ Position.str_of pos);
in T end;
fun parse_term T ctxt text =
let
val thy = theory_of ctxt;
- val {get_sort, map_const, map_free, map_type, map_sort} = term_context ctxt;
+ val {get_sort, map_const, map_free} = term_context ctxt;
val (T', _) = TypeInfer.paramify_dummies T 0;
val (markup, kind) = if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
@@ -704,29 +695,35 @@
fun check t = (Syntax.check_term ctxt (TypeInfer.constrain T' t); NONE)
handle ERROR msg => SOME msg;
- val t = Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free
- map_type map_sort ctxt (Sign.is_logtype thy) (syn_of ctxt) T' (syms, pos)
+ val t =
+ Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free
+ ctxt (Sign.is_logtype thy) (syn_of ctxt) T' (syms, pos)
handle ERROR msg => cat_error msg ("Failed to parse " ^ kind ^ Position.str_of pos);
in t end;
-fun unparse_sort ctxt S =
- Syntax.standard_unparse_sort ctxt (syn_of ctxt) (Sign.extern_sort (theory_of ctxt) S);
+fun unparse_sort ctxt =
+ Syntax.standard_unparse_sort {extern_class = Sign.extern_class (theory_of ctxt)}
+ ctxt (syn_of ctxt);
-fun unparse_typ ctxt T =
- Syntax.standard_unparse_typ ctxt (syn_of ctxt) (Sign.extern_typ (theory_of ctxt) T);
+fun unparse_typ ctxt =
+ let
+ val thy = theory_of ctxt;
+ val extern = {extern_class = Sign.extern_class thy, extern_type = Sign.extern_type thy};
+ in Syntax.standard_unparse_typ extern ctxt (syn_of ctxt) end;
-fun unparse_term ctxt t =
+fun unparse_term ctxt =
let
val thy = theory_of ctxt;
val syntax = syntax_of ctxt;
val consts = consts_of ctxt;
+ val extern =
+ {extern_class = Sign.extern_class thy,
+ extern_type = Sign.extern_type thy,
+ extern_const = Consts.extern consts};
in
- t
- |> Sign.extern_term thy
- |> Local_Syntax.extern_term syntax
- |> Syntax.standard_unparse_term (Consts.extern consts) ctxt
- (Local_Syntax.syn_of syntax) (not (PureThy.old_appl_syntax thy))
+ Syntax.standard_unparse_term (Local_Syntax.idents_of syntax) extern ctxt
+ (Local_Syntax.syn_of syntax) (not (PureThy.old_appl_syntax thy))
end;
in
@@ -1010,18 +1007,20 @@
in Syntax.Constant d end
| const_ast_tr _ _ asts = raise Syntax.AST ("const_ast_tr", asts);
+val typ = Simple_Syntax.read_typ;
+
in
val _ = Context.>> (Context.map_theory
- (Sign.add_syntax
- [("_context_const", "id => logic", Delimfix "CONST _"),
- ("_context_const", "id => aprop", Delimfix "CONST _"),
- ("_context_const", "longid => logic", Delimfix "CONST _"),
- ("_context_const", "longid => aprop", Delimfix "CONST _"),
- ("_context_xconst", "id => logic", Delimfix "XCONST _"),
- ("_context_xconst", "id => aprop", Delimfix "XCONST _"),
- ("_context_xconst", "longid => logic", Delimfix "XCONST _"),
- ("_context_xconst", "longid => aprop", Delimfix "XCONST _")] #>
+ (Sign.add_syntax_i
+ [("_context_const", typ "id => logic", Delimfix "CONST _"),
+ ("_context_const", typ "id => aprop", Delimfix "CONST _"),
+ ("_context_const", typ "longid => logic", Delimfix "CONST _"),
+ ("_context_const", typ "longid => aprop", Delimfix "CONST _"),
+ ("_context_xconst", typ "id => logic", Delimfix "XCONST _"),
+ ("_context_xconst", typ "id => aprop", Delimfix "XCONST _"),
+ ("_context_xconst", typ "longid => logic", Delimfix "XCONST _"),
+ ("_context_xconst", typ "longid => aprop", Delimfix "XCONST _")] #>
Sign.add_advanced_trfuns
([("_context_const", const_ast_tr true), ("_context_xconst", const_ast_tr false)], [], [], [])));
@@ -1032,8 +1031,8 @@
local
-fun type_syntax (Type (c, args), mx) = (* FIXME authentic syntax *)
- SOME (Local_Syntax.Type, (Long_Name.base_name c, Syntax.make_type (length args), mx))
+fun type_syntax (Type (c, args), mx) =
+ SOME (Local_Syntax.Type, (Syntax.mark_type c, Syntax.make_type (length args), mx))
| type_syntax _ = NONE;
fun const_syntax _ (Free (x, T), mx) = SOME (Local_Syntax.Fixed, (x, T, mx))
@@ -1345,7 +1344,7 @@
val prt_term = Syntax.pretty_term ctxt;
(*structures*)
- val structs = Local_Syntax.structs_of (syntax_of ctxt);
+ val {structs, ...} = Local_Syntax.idents_of (syntax_of ctxt);
val prt_structs =
if null structs then []
else [Pretty.block (Pretty.str "structures:" :: Pretty.brk 1 ::
@@ -1415,3 +1414,4 @@
end;
end;
+
--- a/src/Pure/ML/ml_antiquote.ML Wed Mar 03 08:49:11 2010 -0800
+++ b/src/Pure/ML/ml_antiquote.ML Wed Mar 03 10:40:40 2010 -0800
@@ -104,7 +104,7 @@
fun class syn = Args.theory -- Scan.lift Args.name_source >> (fn (thy, s) =>
Sign.read_class thy s
- |> syn ? Long_Name.base_name (* FIXME authentic syntax *)
+ |> syn ? Syntax.mark_class
|> ML_Syntax.print_string);
val _ = inline "class" (class false);
@@ -130,7 +130,7 @@
val _ = inline "type_name" (type_name "logical type" (fn (c, Type.LogicalType _) => c));
val _ = inline "type_abbrev" (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c));
val _ = inline "nonterminal" (type_name "nonterminal" (fn (c, Type.Nonterminal) => c));
-val _ = inline "type_syntax" (type_name "type" (fn (c, _) => Long_Name.base_name c)); (* FIXME authentic syntax *)
+val _ = inline "type_syntax" (type_name "type" (fn (c, _) => Syntax.mark_type c));
(* constants *)
--- a/src/Pure/Proof/extraction.ML Wed Mar 03 08:49:11 2010 -0800
+++ b/src/Pure/Proof/extraction.ML Wed Mar 03 10:40:40 2010 -0800
@@ -207,9 +207,11 @@
let val thy' = add_syntax thy
in fn s =>
let val t = Logic.varify (Syntax.read_prop_global thy' s)
- in (map Logic.dest_equals (Logic.strip_imp_prems t),
- Logic.dest_equals (Logic.strip_imp_concl t))
- end handle TERM _ => error ("Not a (conditional) meta equality:\n" ^ s)
+ in
+ (map Logic.dest_equals (Logic.strip_imp_prems t),
+ Logic.dest_equals (Logic.strip_imp_concl t))
+ handle TERM _ => error ("Not a (conditional) meta equality:\n" ^ s)
+ end
end;
(** preprocessor **)
--- a/src/Pure/Syntax/lexicon.ML Wed Mar 03 08:49:11 2010 -0800
+++ b/src/Pure/Syntax/lexicon.ML Wed Mar 03 10:40:40 2010 -0800
@@ -30,12 +30,17 @@
val read_int: string -> int option
val read_xnum: string -> {radix: int, leading_zeros: int, value: int}
val read_float: string -> {mant: int, exp: int}
- val fixedN: string
- val mark_fixed: string -> string
- val unmark_fixed: string -> string
- val constN: string
- val mark_const: string -> string
- val unmark_const: string -> string
+ val mark_class: string -> string val unmark_class: string -> string
+ val mark_type: string -> string val unmark_type: string -> string
+ val mark_const: string -> string val unmark_const: string -> string
+ val mark_fixed: string -> string val unmark_fixed: string -> string
+ val unmark:
+ {case_class: string -> 'a,
+ case_type: string -> 'a,
+ case_const: string -> 'a,
+ case_fixed: string -> 'a,
+ case_default: string -> 'a} -> string -> 'a
+ val is_marked: string -> bool
end;
signature LEXICON =
@@ -333,15 +338,32 @@
in Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none)) end;
-(* specific identifiers *)
+(* logical entities *)
+
+fun marker s = (prefix s, unprefix s);
+
+val (mark_class, unmark_class) = marker "\\<^class>";
+val (mark_type, unmark_type) = marker "\\<^type>";
+val (mark_const, unmark_const) = marker "\\<^const>";
+val (mark_fixed, unmark_fixed) = marker "\\<^fixed>";
-val fixedN = "\\<^fixed>";
-val mark_fixed = prefix fixedN;
-val unmark_fixed = unprefix fixedN;
+fun unmark {case_class, case_type, case_const, case_fixed, case_default} s =
+ (case try unmark_class s of
+ SOME c => case_class c
+ | NONE =>
+ (case try unmark_type s of
+ SOME c => case_type c
+ | NONE =>
+ (case try unmark_const s of
+ SOME c => case_const c
+ | NONE =>
+ (case try unmark_fixed s of
+ SOME c => case_fixed c
+ | NONE => case_default s))));
-val constN = "\\<^const>";
-val mark_const = prefix constN;
-val unmark_const = unprefix constN;
+val is_marked =
+ unmark {case_class = K true, case_type = K true, case_const = K true,
+ case_fixed = K true, case_default = K false};
(* read numbers *)
@@ -371,7 +393,7 @@
val ten = ord "0" + 10;
val a = ord "a";
val A = ord "A";
-val _ = a > A orelse sys_error "Bad ASCII";
+val _ = a > A orelse raise Fail "Bad ASCII";
fun remap_hex c =
let val x = ord c in
--- a/src/Pure/Syntax/printer.ML Wed Mar 03 08:49:11 2010 -0800
+++ b/src/Pure/Syntax/printer.ML Wed Mar 03 10:40:40 2010 -0800
@@ -11,29 +11,32 @@
val show_types: bool Unsynchronized.ref
val show_no_free_types: bool Unsynchronized.ref
val show_all_types: bool Unsynchronized.ref
+ val show_structs: bool Unsynchronized.ref
val pp_show_brackets: Pretty.pp -> Pretty.pp
end;
signature PRINTER =
sig
include PRINTER0
- val term_to_ast: Proof.context ->
- (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> term -> Ast.ast
+ val sort_to_ast: Proof.context ->
+ (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> sort -> Ast.ast
val typ_to_ast: Proof.context ->
(string -> (Proof.context -> bool -> typ -> term list -> term) list) -> typ -> Ast.ast
- val sort_to_ast: Proof.context ->
- (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> sort -> Ast.ast
+ val term_to_ast: {structs: string list, fixes: string list} -> string list -> Proof.context ->
+ (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> term -> Ast.ast
type prtabs
val empty_prtabs: prtabs
val update_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
val remove_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
val merge_prtabs: prtabs -> prtabs -> prtabs
- val pretty_term_ast: (string -> xstring) -> Proof.context -> bool -> prtabs
- -> (string -> (Proof.context -> Ast.ast list -> Ast.ast) list)
- -> (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list
- val pretty_typ_ast: Proof.context -> bool -> prtabs
- -> (string -> (Proof.context -> Ast.ast list -> Ast.ast) list)
- -> (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list
+ val pretty_term_ast: {extern_class: string -> xstring, extern_type: string -> xstring,
+ extern_const: string -> xstring} -> Proof.context -> bool -> prtabs ->
+ (string -> (Proof.context -> Ast.ast list -> Ast.ast) list) ->
+ (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list
+ val pretty_typ_ast: {extern_class: string -> xstring, extern_type: string -> xstring} ->
+ Proof.context -> bool -> prtabs ->
+ (string -> (Proof.context -> Ast.ast list -> Ast.ast) list) ->
+ (string -> (Proof.context -> string -> Pretty.T) option) -> Ast.ast -> Pretty.T list
end;
structure Printer: PRINTER =
@@ -47,6 +50,7 @@
val show_brackets = Unsynchronized.ref false;
val show_no_free_types = Unsynchronized.ref false;
val show_all_types = Unsynchronized.ref false;
+val show_structs = Unsynchronized.ref false;
fun pp_show_brackets pp = Pretty.pp (setmp_CRITICAL show_brackets true (Pretty.term pp),
Pretty.typ pp, Pretty.sort pp, Pretty.classrel pp, Pretty.arity pp);
@@ -84,8 +88,7 @@
fun ast_of_termT ctxt trf tm =
let
- fun ast_of (t as Const ("_class", _) $ Free _) = simple_ast_of t
- | ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of t
+ fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of t
| ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of t
| ast_of (Const (a, _)) = trans a []
| ast_of (t as _ $ _) =
@@ -105,19 +108,32 @@
(** term_to_ast **)
-fun mark_freevars ((t as Const (c, _)) $ u) =
- if member (op =) SynExt.standard_token_markers c then (t $ u)
- else t $ mark_freevars u
- | mark_freevars (t $ u) = mark_freevars t $ mark_freevars u
- | mark_freevars (Abs (x, T, t)) = Abs (x, T, mark_freevars t)
- | mark_freevars (t as Free _) = Lexicon.const "_free" $ t
- | mark_freevars (t as Var (xi, T)) =
- if xi = SynExt.dddot_indexname then Const ("_DDDOT", T)
- else Lexicon.const "_var" $ t
- | mark_freevars a = a;
+fun ast_of_term idents consts ctxt trf
+ show_all_types no_freeTs show_types show_sorts show_structs tm =
+ let
+ val {structs, fixes} = idents;
-fun ast_of_term ctxt trf show_all_types no_freeTs show_types show_sorts tm =
- let
+ fun mark_atoms ((t as Const (c, T)) $ u) =
+ if member (op =) SynExt.standard_token_markers c
+ then t $ u else mark_atoms t $ mark_atoms u
+ | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
+ | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
+ | mark_atoms (t as Const (c, T)) =
+ if member (op =) consts c then t
+ else Const (Lexicon.mark_const c, T)
+ | mark_atoms (t as Free (x, T)) =
+ let val i = find_index (fn s => s = x) structs + 1 in
+ if i = 0 andalso member (op =) fixes x then
+ Const (Lexicon.mark_fixed x, T)
+ else if i = 1 andalso not show_structs then
+ Lexicon.const "_struct" $ Lexicon.const "_indexdefault"
+ else Lexicon.const "_free" $ t
+ end
+ | mark_atoms (t as Var (xi, T)) =
+ if xi = SynExt.dddot_indexname then Const ("_DDDOT", T)
+ else Lexicon.const "_var" $ t
+ | mark_atoms a = a;
+
fun prune_typs (t_seen as (Const _, _)) = t_seen
| prune_typs (t as Free (x, ty), seen) =
if ty = dummyT then (t, seen)
@@ -148,9 +164,9 @@
Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
| (Const ("_idtdummy", T), ts) =>
Ast.mk_appl (constrain (Lexicon.const "_idtdummy") T) (map ast_of ts)
- | (c' as Const (c, T), ts) =>
+ | (const as Const (c, T), ts) =>
if show_all_types
- then Ast.mk_appl (constrain c' T) (map ast_of ts)
+ then Ast.mk_appl (constrain const T) (map ast_of ts)
else trans c T ts
| (t, ts) => Ast.mk_appl (simple_ast_of t) (map ast_of ts))
@@ -162,18 +178,18 @@
if show_types andalso T <> dummyT then
Ast.Appl [Ast.Constant SynExt.constrainC, simple_ast_of t,
ast_of_termT ctxt trf (TypeExt.term_of_typ show_sorts T)]
- else simple_ast_of t
+ else simple_ast_of t;
in
tm
|> SynTrans.prop_tr'
- |> (if show_types then #1 o prune_typs o rpair [] else I)
- |> mark_freevars
+ |> show_types ? (#1 o prune_typs o rpair [])
+ |> mark_atoms
|> ast_of
end;
-fun term_to_ast ctxt trf tm =
- ast_of_term ctxt trf (! show_all_types) (! show_no_free_types)
- (! show_types orelse ! show_sorts orelse ! show_all_types) (! show_sorts) tm;
+fun term_to_ast idents consts ctxt trf tm =
+ ast_of_term idents consts ctxt trf (! show_all_types) (! show_no_free_types)
+ (! show_types orelse ! show_sorts orelse ! show_all_types) (! show_sorts) (! show_structs) tm;
@@ -267,8 +283,10 @@
| is_chain [Arg _] = true
| is_chain _ = false;
-fun pretty extern_const ctxt tabs trf tokentrf type_mode curried ast0 p0 =
+fun pretty extern ctxt tabs trf tokentrf type_mode curried ast0 p0 =
let
+ val {extern_class, extern_type, extern_const} = extern;
+
fun token_trans a x =
(case tokentrf a of
NONE =>
@@ -291,7 +309,7 @@
val (Ts, args') = synT markup (symbs, args);
in
if type_mode then (astT (t, p) @ Ts, args')
- else (pretty I ctxt tabs trf tokentrf true curried t p @ Ts, args')
+ else (pretty extern ctxt tabs trf tokentrf true curried t p @ Ts, args')
end
| synT markup (String s :: symbs, args) =
let val (Ts, args') = synT markup (symbs, args);
@@ -312,7 +330,6 @@
val (Ts, args') = synT markup (symbs, args);
val T = if i < 0 then Pretty.fbrk else Pretty.brk i;
in (T :: Ts, args') end
- | synT _ (_ :: _, []) = sys_error "synT"
and parT markup (pr, args, p, p': int) = #1 (synT markup
(if p > p' orelse
@@ -320,13 +337,12 @@
then [Block (1, Space "(" :: pr @ [Space ")"])]
else pr, args))
- and atomT a =
- (case try Lexicon.unmark_const a of
- SOME c => Pretty.mark (Markup.const c) (Pretty.str (extern_const c))
- | NONE =>
- (case try Lexicon.unmark_fixed a of
- SOME x => the (token_trans "_free" x)
- | NONE => Pretty.str a))
+ and atomT a = a |> Lexicon.unmark
+ {case_class = fn c => Pretty.mark (Markup.tclass c) (Pretty.str (extern_class c)),
+ case_type = fn c => Pretty.mark (Markup.tycon c) (Pretty.str (extern_type c)),
+ case_const = fn c => Pretty.mark (Markup.const c) (Pretty.str (extern_const c)),
+ case_fixed = fn x => the (token_trans "_free" x),
+ case_default = Pretty.str}
and prefixT (_, a, [], _) = [atomT a]
| prefixT (c, _, args, p) = astT (appT (c, args), p)
@@ -334,15 +350,16 @@
and splitT 0 ([x], ys) = (x, ys)
| splitT 0 (rev_xs, ys) = (Ast.Appl (rev rev_xs), ys)
| splitT n (rev_xs, y :: ys) = splitT (n - 1) (y :: rev_xs, ys)
- | splitT _ _ = sys_error "splitT"
and combT (tup as (c, a, args, p)) =
let
val nargs = length args;
- val markup = Pretty.mark
- (Markup.const (Lexicon.unmark_const a) handle Fail _ =>
- (Markup.fixed (Lexicon.unmark_fixed a)))
- handle Fail _ => I;
+ val markup = a |> Lexicon.unmark
+ {case_class = Pretty.mark o Markup.tclass,
+ case_type = Pretty.mark o Markup.tycon,
+ case_const = Pretty.mark o Markup.const,
+ case_fixed = Pretty.mark o Markup.fixed,
+ case_default = K I};
(*find matching table entry, or print as prefix / postfix*)
fun prnt ([], []) = prefixT tup
@@ -371,15 +388,16 @@
(* pretty_term_ast *)
-fun pretty_term_ast extern_const ctxt curried prtabs trf tokentrf ast =
- pretty extern_const ctxt (mode_tabs prtabs (print_mode_value ()))
+fun pretty_term_ast extern ctxt curried prtabs trf tokentrf ast =
+ pretty extern ctxt (mode_tabs prtabs (print_mode_value ()))
trf tokentrf false curried ast 0;
(* pretty_typ_ast *)
-fun pretty_typ_ast ctxt _ prtabs trf tokentrf ast =
- pretty I ctxt (mode_tabs prtabs (print_mode_value ()))
+fun pretty_typ_ast {extern_class, extern_type} ctxt _ prtabs trf tokentrf ast =
+ pretty {extern_class = extern_class, extern_type = extern_type, extern_const = I}
+ ctxt (mode_tabs prtabs (print_mode_value ()))
trf tokentrf true false ast 0;
end;
--- a/src/Pure/Syntax/syn_ext.ML Wed Mar 03 08:49:11 2010 -0800
+++ b/src/Pure/Syntax/syn_ext.ML Wed Mar 03 10:40:40 2010 -0800
@@ -282,7 +282,8 @@
if not (exists is_index args) then (const, typ, [])
else
let
- val indexed_const = if const <> "" then "_indexed_" ^ const
+ val indexed_const =
+ if const <> "" then const ^ "_indexed"
else err_in_mfix "Missing constant name for indexed syntax" mfix;
val rangeT = Term.range_type typ handle Match =>
err_in_mfix "Missing structure argument for indexed syntax" mfix;
@@ -387,7 +388,7 @@
fun tokentrans_mode m trs = map (fn (s, f) => (m, s, f)) trs;
val standard_token_classes =
- ["class", "tfree", "tvar", "free", "bound", "var", "numeral", "inner_string"];
+ ["tfree", "tvar", "free", "bound", "var", "numeral", "inner_string"];
val standard_token_markers = map (fn s => "_" ^ s) standard_token_classes;
--- a/src/Pure/Syntax/syn_trans.ML Wed Mar 03 08:49:11 2010 -0800
+++ b/src/Pure/Syntax/syn_trans.ML Wed Mar 03 10:40:40 2010 -0800
@@ -34,16 +34,16 @@
val non_typed_tr'': ('a -> term list -> term) -> 'a -> bool -> typ -> term list -> term
val constrainAbsC: string
val pure_trfuns:
- (string * (Ast.ast list -> Ast.ast)) list *
- (string * (term list -> term)) list *
- (string * (term list -> term)) list *
- (string * (Ast.ast list -> Ast.ast)) list
+ (string * (Ast.ast list -> Ast.ast)) list *
+ (string * (term list -> term)) list *
+ (string * (term list -> term)) list *
+ (string * (Ast.ast list -> Ast.ast)) list
val pure_trfunsT: (string * (bool -> typ -> term list -> term)) list
val struct_trfuns: string list ->
- (string * (Ast.ast list -> Ast.ast)) list *
- (string * (term list -> term)) list *
- (string * (bool -> typ -> term list -> term)) list *
- (string * (Ast.ast list -> Ast.ast)) list
+ (string * (Ast.ast list -> Ast.ast)) list *
+ (string * (term list -> term)) list *
+ (string * (bool -> typ -> term list -> term)) list *
+ (string * (Ast.ast list -> Ast.ast)) list
end;
signature SYN_TRANS =
@@ -131,7 +131,7 @@
fun mk_type ty =
Lexicon.const "_constrain" $
- Lexicon.const "\\<^const>TYPE" $ (Lexicon.const "itself" $ ty);
+ Lexicon.const "\\<^const>TYPE" $ (Lexicon.const "\\<^type>itself" $ ty);
fun ofclass_tr (*"_ofclass"*) [ty, cls] = cls $ mk_type ty
| ofclass_tr (*"_ofclass"*) ts = raise TERM ("ofclass_tr", ts);
@@ -143,7 +143,7 @@
(* meta propositions *)
-fun aprop_tr (*"_aprop"*) [t] = Lexicon.const "_constrain" $ t $ Lexicon.const "prop"
+fun aprop_tr (*"_aprop"*) [t] = Lexicon.const "_constrain" $ t $ Lexicon.const "\\<^type>prop"
| aprop_tr (*"_aprop"*) ts = raise TERM ("aprop_tr", ts);
@@ -195,7 +195,8 @@
fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts)
| update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix "_update" x, T), ts)
| update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
- list_comb (c $ update_name_tr [t] $ (Lexicon.const "fun" $ ty $ Lexicon.const "dummy"), ts)
+ list_comb (c $ update_name_tr [t] $
+ (Lexicon.const "\\<^type>fun" $ ty $ Lexicon.const "\\<^type>dummy"), ts)
| update_name_tr ts = raise TERM ("update_name_tr", ts);
@@ -368,7 +369,7 @@
fun is_prop Ts t =
fastype_of1 (Ts, t) = propT handle TERM _ => false;
- fun is_term (Const ("\\<^const>Pure.term", _) $ _) = true
+ fun is_term (Const ("Pure.term", _) $ _) = true
| is_term _ = false;
fun tr' _ (t as Const _) = t
@@ -381,7 +382,7 @@
| tr' Ts (t as Bound _) =
if is_prop Ts t then aprop t else t
| tr' Ts (Abs (x, T, t)) = Abs (x, T, tr' (T :: Ts) t)
- | tr' Ts (t as t1 $ (t2 as Const ("\\<^const>TYPE", Type ("itself", [T])))) =
+ | tr' Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ tr' Ts t1
else tr' Ts t1 $ tr' Ts t2
| tr' Ts (t as t1 $ t2) =
@@ -568,7 +569,7 @@
val free_fixed = Term.map_aterms
(fn t as Const (c, T) =>
- (case try (unprefix Lexicon.fixedN) c of
+ (case try Lexicon.unmark_fixed c of
NONE => t
| SOME x => Free (x, T))
| t => t);
--- a/src/Pure/Syntax/syntax.ML Wed Mar 03 08:49:11 2010 -0800
+++ b/src/Pure/Syntax/syntax.ML Wed Mar 03 10:40:40 2010 -0800
@@ -29,7 +29,10 @@
val mode_default: mode
val mode_input: mode
val merge_syntaxes: syntax -> syntax -> syntax
- val basic_syn: syntax
+ val empty_syntax: syntax
+ val basic_syntax:
+ {read_class: theory -> xstring -> string,
+ read_type: theory -> xstring -> string} -> syntax
val basic_nonterms: string list
val print_gram: syntax -> unit
val print_trans: syntax -> unit
@@ -41,25 +44,24 @@
val ambiguity_limit: int Unsynchronized.ref
val standard_parse_term: Pretty.pp -> (term -> string option) ->
(((string * int) * sort) list -> string * int -> Term.sort) ->
- (string -> bool * string) -> (string -> string option) ->
- (typ -> typ) -> (sort -> sort) -> Proof.context ->
+ (string -> bool * string) -> (string -> string option) -> Proof.context ->
(string -> bool) -> syntax -> typ -> Symbol_Pos.T list * Position.T -> term
val standard_parse_typ: Proof.context -> syntax ->
- ((indexname * sort) list -> indexname -> sort) -> (sort -> sort) ->
- Symbol_Pos.T list * Position.T -> typ
- val standard_parse_sort: Proof.context -> syntax -> (sort -> sort) ->
- Symbol_Pos.T list * Position.T -> sort
+ ((indexname * sort) list -> indexname -> sort) -> Symbol_Pos.T list * Position.T -> typ
+ val standard_parse_sort: Proof.context -> syntax -> Symbol_Pos.T list * Position.T -> sort
datatype 'a trrule =
ParseRule of 'a * 'a |
PrintRule of 'a * 'a |
ParsePrintRule of 'a * 'a
val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
val is_const: syntax -> string -> bool
- val standard_unparse_term: (string -> xstring) ->
- Proof.context -> syntax -> bool -> term -> Pretty.T
- val standard_unparse_typ: Proof.context -> syntax -> typ -> Pretty.T
- val standard_unparse_sort: Proof.context -> syntax -> sort -> Pretty.T
- val update_consts: string list -> syntax -> syntax
+ val standard_unparse_term: {structs: string list, fixes: string list} ->
+ {extern_class: string -> xstring, extern_type: string -> xstring,
+ extern_const: string -> xstring} -> Proof.context -> syntax -> bool -> term -> Pretty.T
+ val standard_unparse_typ: {extern_class: string -> xstring, extern_type: string -> xstring} ->
+ Proof.context -> syntax -> typ -> Pretty.T
+ val standard_unparse_sort: {extern_class: string -> xstring} ->
+ Proof.context -> syntax -> sort -> Pretty.T
val update_trfuns:
(string * ((ast list -> ast) * stamp)) list *
(string * ((term list -> term) * stamp)) list *
@@ -300,7 +302,7 @@
lexicon =
if changed then fold Scan.extend_lexicon (SynExt.delims_of xprods) lexicon else lexicon,
gram = if changed then Parser.extend_gram gram xprods else gram,
- consts = Library.merge (op =) (consts1, filter_out (can Lexicon.unmark_const) consts2),
+ consts = Library.merge (op =) (consts1, filter_out Lexicon.is_marked consts2),
prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),
parse_ast_trtab =
update_trtab "parse ast translation" (if_inout parse_ast_translation) parse_ast_trtab,
@@ -381,9 +383,9 @@
(* basic syntax *)
-val basic_syn =
+fun basic_syntax read =
empty_syntax
- |> update_syntax mode_default TypeExt.type_ext
+ |> update_syntax mode_default (TypeExt.type_ext read)
|> update_syntax mode_default SynExt.pure_ext;
val basic_nonterms =
@@ -547,26 +549,25 @@
map (Pretty.string_of_term pp) (take limit results)))
end;
-fun standard_parse_term pp check get_sort map_const map_free map_type map_sort
- ctxt is_logtype syn ty (syms, pos) =
+fun standard_parse_term pp check get_sort map_const map_free ctxt is_logtype syn ty (syms, pos) =
read ctxt is_logtype syn ty (syms, pos)
- |> map (TypeExt.decode_term get_sort map_const map_free map_type map_sort)
+ |> map (TypeExt.decode_term get_sort map_const map_free)
|> disambig (Printer.pp_show_brackets pp) check;
(* read types *)
-fun standard_parse_typ ctxt syn get_sort map_sort (syms, pos) =
+fun standard_parse_typ ctxt syn get_sort (syms, pos) =
(case read ctxt (K false) syn SynExt.typeT (syms, pos) of
- [t] => TypeExt.typ_of_term (get_sort (TypeExt.term_sorts map_sort t)) map_sort t
+ [t] => TypeExt.typ_of_term (get_sort (TypeExt.term_sorts t)) t
| _ => error (ambiguity_msg pos));
(* read sorts *)
-fun standard_parse_sort ctxt syn map_sort (syms, pos) =
+fun standard_parse_sort ctxt syn (syms, pos) =
(case read ctxt (K false) syn TypeExt.sortT (syms, pos) of
- [t] => TypeExt.sort_of_term map_sort t
+ [t] => TypeExt.sort_of_term t
| _ => error (ambiguity_msg pos));
@@ -640,8 +641,8 @@
fun unparse_t t_to_ast prt_t markup ctxt (Syntax (tabs, _)) curried t =
let
- val {print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs;
- val ast = t_to_ast ctxt (lookup_tr' print_trtab) t;
+ val {consts, print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs;
+ val ast = t_to_ast consts ctxt (lookup_tr' print_trtab) t;
in
Pretty.markup markup (prt_t ctxt curried prtabs (lookup_tr' print_ast_trtab)
(lookup_tokentr tokentrtab (print_mode_value ()))
@@ -650,14 +651,16 @@
in
-fun standard_unparse_term extern =
- unparse_t Printer.term_to_ast (Printer.pretty_term_ast extern) Markup.term;
+fun standard_unparse_term idents extern =
+ unparse_t (Printer.term_to_ast idents) (Printer.pretty_term_ast extern) Markup.term;
-fun standard_unparse_typ ctxt syn =
- unparse_t Printer.typ_to_ast Printer.pretty_typ_ast Markup.typ ctxt syn false;
+fun standard_unparse_typ extern ctxt syn =
+ unparse_t (K Printer.typ_to_ast) (Printer.pretty_typ_ast extern) Markup.typ ctxt syn false;
-fun standard_unparse_sort ctxt syn =
- unparse_t Printer.sort_to_ast Printer.pretty_typ_ast Markup.sort ctxt syn false;
+fun standard_unparse_sort {extern_class} ctxt syn =
+ unparse_t (K Printer.sort_to_ast)
+ (Printer.pretty_typ_ast {extern_class = extern_class, extern_type = I})
+ Markup.sort ctxt syn false;
end;
@@ -667,7 +670,6 @@
fun ext_syntax f decls = update_syntax mode_default (f decls);
-val update_consts = ext_syntax SynExt.syn_ext_const_names;
val update_trfuns = ext_syntax SynExt.syn_ext_trfuns;
val update_advanced_trfuns = ext_syntax SynExt.syn_ext_advanced_trfuns;
val extend_tokentrfuns = ext_syntax SynExt.syn_ext_tokentrfuns;
--- a/src/Pure/Syntax/type_ext.ML Wed Mar 03 08:49:11 2010 -0800
+++ b/src/Pure/Syntax/type_ext.ML Wed Mar 03 10:40:40 2010 -0800
@@ -1,19 +1,17 @@
(* Title: Pure/Syntax/type_ext.ML
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
-Utilities for input and output of types. Also the concrete syntax of
-types, which is required to bootstrap Pure.
+Utilities for input and output of types. The concrete syntax of types.
*)
signature TYPE_EXT0 =
sig
- val sort_of_term: (sort -> sort) -> term -> sort
- val term_sorts: (sort -> sort) -> term -> (indexname * sort) list
- val typ_of_term: (indexname -> sort) -> (sort -> sort) -> term -> typ
+ val sort_of_term: term -> sort
+ val term_sorts: term -> (indexname * sort) list
+ val typ_of_term: (indexname -> sort) -> term -> typ
val type_constraint: typ -> term -> term
val decode_term: (((string * int) * sort) list -> string * int -> sort) ->
- (string -> bool * string) -> (string -> string option) ->
- (typ -> typ) -> (sort -> sort) -> term -> term
+ (string -> bool * string) -> (string -> string option) -> term -> term
val term_of_typ: bool -> typ -> term
val no_brackets: unit -> bool
val no_type_brackets: unit -> bool
@@ -25,7 +23,9 @@
val term_of_sort: sort -> term
val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
val sortT: typ
- val type_ext: SynExt.syn_ext
+ val type_ext:
+ {read_class: theory -> string -> string,
+ read_type: theory -> string -> string} -> SynExt.syn_ext
end;
structure TypeExt: TYPE_EXT =
@@ -35,30 +35,28 @@
(* sort_of_term *)
-fun sort_of_term (map_sort: sort -> sort) tm =
+fun sort_of_term tm =
let
- fun classes (Const (c, _)) = [c]
- | classes (Free (c, _)) = [c]
- | classes (Const ("_class", _) $ Free (c, _)) = [c]
- | classes (Const ("_classes", _) $ Const (c, _) $ cs) = c :: classes cs
- | classes (Const ("_classes", _) $ Free (c, _) $ cs) = c :: classes cs
- | classes (Const ("_classes", _) $ (Const ("_class", _) $ Free (c, _)) $ cs) = c :: classes cs
- | classes tm = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
+ fun err () = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
+
+ fun class s = Lexicon.unmark_class s handle Fail _ => err ();
+
+ fun classes (Const (s, _)) = [class s]
+ | classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs
+ | classes _ = err ();
fun sort (Const ("_topsort", _)) = []
- | sort (Const (c, _)) = [c]
- | sort (Free (c, _)) = [c]
- | sort (Const ("_class", _) $ Free (c, _)) = [c]
+ | sort (Const (s, _)) = [class s]
| sort (Const ("_sort", _) $ cs) = classes cs
- | sort tm = raise TERM ("sort_of_term: bad encoding of sort", [tm]);
- in map_sort (sort tm) end;
+ | sort _ = err ();
+ in sort tm end;
(* term_sorts *)
-fun term_sorts map_sort tm =
+fun term_sorts tm =
let
- val sort_of = sort_of_term map_sort;
+ val sort_of = sort_of_term;
fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) =
insert (op =) ((x, ~1), sort_of cs)
@@ -76,11 +74,11 @@
(* typ_of_term *)
-fun typ_of_term get_sort map_sort t =
+fun typ_of_term get_sort tm =
let
- fun typ_of (Free (x, _)) =
- if Lexicon.is_tid x then TFree (x, get_sort (x, ~1))
- else Type (x, [])
+ fun err () = raise TERM ("typ_of_term: bad encoding of type", [tm]);
+
+ fun typ_of (Free (x, _)) = TFree (x, get_sort (x, ~1))
| typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
| typ_of (Const ("_tfree",_) $ (t as Free _)) = typ_of t
| typ_of (Const ("_tvar",_) $ (t as Var _)) = typ_of t
@@ -90,17 +88,16 @@
| typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) = TVar (xi, get_sort xi)
| typ_of (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ _) =
TVar (xi, get_sort xi)
- | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", sort_of_term map_sort t)
- | typ_of tm =
+ | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", sort_of_term t)
+ | typ_of t =
let
- val (t, ts) = Term.strip_comb tm;
+ val (head, args) = Term.strip_comb t;
val a =
- (case t of
- Const (x, _) => x
- | Free (x, _) => x
- | _ => raise TERM ("typ_of_term: bad encoding of type", [tm]));
- in Type (a, map typ_of ts) end;
- in typ_of t end;
+ (case head of
+ Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ())
+ | _ => err ());
+ in Type (a, map typ_of args) end;
+ in typ_of tm end;
(* decode_term -- transform parse tree into raw term *)
@@ -109,30 +106,30 @@
if T = dummyT then t
else Const ("_type_constraint_", T --> T) $ t;
-fun decode_term get_sort map_const map_free map_type map_sort tm =
+fun decode_term get_sort map_const map_free tm =
let
- val sort_env = term_sorts map_sort tm;
- val decodeT = map_type o typ_of_term (get_sort sort_env) map_sort;
+ val sort_env = term_sorts tm;
+ val decodeT = typ_of_term (get_sort sort_env);
fun decode (Const ("_constrain", _) $ t $ typ) =
type_constraint (decodeT typ) (decode t)
| decode (Const ("_constrainAbs", _) $ (Abs (x, T, t)) $ typ) =
if T = dummyT then Abs (x, decodeT typ, decode t)
- else type_constraint (decodeT typ --> dummyT) (Abs (x, map_type T, decode t))
- | decode (Abs (x, T, t)) = Abs (x, map_type T, decode t)
+ else type_constraint (decodeT typ --> dummyT) (Abs (x, T, decode t))
+ | decode (Abs (x, T, t)) = Abs (x, T, decode t)
| decode (t $ u) = decode t $ decode u
| decode (Const (a, T)) =
let val c =
(case try Lexicon.unmark_const a of
SOME c => c
| NONE => snd (map_const a))
- in Const (c, map_type T) end
+ in Const (c, T) end
| decode (Free (a, T)) =
(case (map_free a, map_const a) of
- (SOME x, _) => Free (x, map_type T)
- | (_, (true, c)) => Const (c, map_type T)
- | (_, (false, c)) => (if Long_Name.is_qualified c then Const else Free) (c, map_type T))
- | decode (Var (xi, T)) = Var (xi, map_type T)
+ (SOME x, _) => Free (x, T)
+ | (_, (true, c)) => Const (c, T)
+ | (_, (false, c)) => (if Long_Name.is_qualified c then Const else Free) (c, T))
+ | decode (Var (xi, T)) = Var (xi, T)
| decode (t as Bound _) = t;
in decode tm end;
@@ -144,10 +141,9 @@
fun term_of_sort S =
let
- fun class c = Lexicon.const "_class" $ Lexicon.free c;
+ val class = Lexicon.const o Lexicon.mark_class;
- fun classes [] = sys_error "term_of_sort"
- | classes [c] = class c
+ fun classes [c] = class c
| classes (c :: cs) = Lexicon.const "_classes" $ class c $ classes cs;
in
(case S of
@@ -165,7 +161,8 @@
if show_sorts then Lexicon.const "_ofsort" $ t $ term_of_sort S
else t;
- fun term_of (Type (a, Ts)) = Term.list_comb (Lexicon.const a, map term_of Ts)
+ fun term_of (Type (a, Ts)) =
+ Term.list_comb (Lexicon.const (Lexicon.mark_type a), map term_of Ts)
| term_of (TFree (x, S)) = of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
| term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
in term_of ty end;
@@ -193,15 +190,29 @@
(* parse ast translations *)
-fun tapp_ast_tr (*"_tapp"*) [ty, f] = Ast.Appl [f, ty]
- | tapp_ast_tr (*"_tapp"*) asts = raise Ast.AST ("tapp_ast_tr", asts);
+val class_ast = Ast.Constant o Lexicon.mark_class;
+val type_ast = Ast.Constant o Lexicon.mark_type;
+
+fun class_name_tr read_class (*"_class_name"*) [Ast.Variable c] = class_ast (read_class c)
+ | class_name_tr _ (*"_class_name"*) asts = raise Ast.AST ("class_name_tr", asts);
+
+fun classes_tr read_class (*"_classes"*) [Ast.Variable c, ast] =
+ Ast.mk_appl (Ast.Constant "_classes") [class_ast (read_class c), ast]
+ | classes_tr _ (*"_classes"*) asts = raise Ast.AST ("classes_tr", asts);
-fun tappl_ast_tr (*"_tappl"*) [ty, tys, f] =
- Ast.Appl (f :: ty :: Ast.unfold_ast "_types" tys)
- | tappl_ast_tr (*"_tappl"*) asts = raise Ast.AST ("tappl_ast_tr", asts);
+fun type_name_tr read_type (*"_type_name"*) [Ast.Variable c] = type_ast (read_type c)
+ | type_name_tr _ (*"_type_name"*) asts = raise Ast.AST ("type_name_tr", asts);
+
+fun tapp_ast_tr read_type (*"_tapp"*) [ty, Ast.Variable c] =
+ Ast.Appl [type_ast (read_type c), ty]
+ | tapp_ast_tr _ (*"_tapp"*) asts = raise Ast.AST ("tapp_ast_tr", asts);
+
+fun tappl_ast_tr read_type (*"_tappl"*) [ty, tys, Ast.Variable c] =
+ Ast.Appl (type_ast (read_type c) :: ty :: Ast.unfold_ast "_types" tys)
+ | tappl_ast_tr _ (*"_tappl"*) asts = raise Ast.AST ("tappl_ast_tr", asts);
fun bracket_ast_tr (*"_bracket"*) [dom, cod] =
- Ast.fold_ast_p "fun" (Ast.unfold_ast "_types" dom, cod)
+ Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
| bracket_ast_tr (*"_bracket"*) asts = raise Ast.AST ("bracket_ast_tr", asts);
@@ -212,10 +223,10 @@
| tappl_ast_tr' (f, ty :: tys) =
Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f];
-fun fun_ast_tr' (*"fun"*) asts =
+fun fun_ast_tr' (*"\\<^type>fun"*) asts =
if no_brackets () orelse no_type_brackets () then raise Match
else
- (case Ast.unfold_ast_p "fun" (Ast.Appl (Ast.Constant "fun" :: asts)) of
+ (case Ast.unfold_ast_p "\\<^type>fun" (Ast.Appl (Ast.Constant "\\<^type>fun" :: asts)) of
(dom as _ :: _ :: _, cod)
=> Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod]
| _ => raise Match);
@@ -229,20 +240,20 @@
local open Lexicon SynExt in
-val type_ext = syn_ext' false (K false)
+fun type_ext {read_class, read_type} = syn_ext' false (K false)
[Mfix ("_", tidT --> typeT, "", [], max_pri),
Mfix ("_", tvarT --> typeT, "", [], max_pri),
- Mfix ("_", idT --> typeT, "", [], max_pri),
- Mfix ("_", longidT --> typeT, "", [], max_pri),
+ Mfix ("_", idT --> typeT, "_type_name", [], max_pri),
+ Mfix ("_", longidT --> typeT, "_type_name", [], max_pri),
Mfix ("_::_", [tidT, sortT] ---> typeT, "_ofsort", [max_pri, 0], max_pri),
Mfix ("_::_", [tvarT, sortT] ---> typeT, "_ofsort", [max_pri, 0], max_pri),
Mfix ("'_()::_", sortT --> typeT, "_dummy_ofsort", [0], max_pri),
- Mfix ("_", idT --> sortT, "", [], max_pri),
- Mfix ("_", longidT --> sortT, "", [], max_pri),
+ Mfix ("_", idT --> sortT, "_class_name", [], max_pri),
+ Mfix ("_", longidT --> sortT, "_class_name", [], max_pri),
Mfix ("{}", sortT, "_topsort", [], max_pri),
Mfix ("{_}", classesT --> sortT, "_sort", [], max_pri),
- Mfix ("_", idT --> classesT, "", [], max_pri),
- Mfix ("_", longidT --> classesT, "", [], max_pri),
+ Mfix ("_", idT --> classesT, "_class_name", [], max_pri),
+ Mfix ("_", longidT --> classesT, "_class_name", [], max_pri),
Mfix ("_,_", [idT, classesT] ---> classesT, "_classes", [], max_pri),
Mfix ("_,_", [longidT, classesT] ---> classesT, "_classes", [], max_pri),
Mfix ("_ _", [typeT, idT] ---> typeT, "_tapp", [max_pri, 0], max_pri),
@@ -251,16 +262,21 @@
Mfix ("((1'(_,/ _')) _)", [typeT, typesT, longidT] ---> typeT, "_tappl", [], max_pri),
Mfix ("_", typeT --> typesT, "", [], max_pri),
Mfix ("_,/ _", [typeT, typesT] ---> typesT, "_types", [], max_pri),
- Mfix ("(_/ => _)", [typeT, typeT] ---> typeT, "fun", [1, 0], 0),
+ Mfix ("(_/ => _)", [typeT, typeT] ---> typeT, "\\<^type>fun", [1, 0], 0),
Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT, "_bracket", [0, 0], 0),
Mfix ("'(_')", typeT --> typeT, "", [0], max_pri),
- Mfix ("'_", typeT, "dummy", [], max_pri)]
- []
+ Mfix ("'_", typeT, "\\<^type>dummy", [], max_pri)]
+ ["_type_prop"]
(map SynExt.mk_trfun
- [("_tapp", K tapp_ast_tr), ("_tappl", K tappl_ast_tr), ("_bracket", K bracket_ast_tr)],
+ [("_class_name", class_name_tr o read_class o ProofContext.theory_of),
+ ("_classes", classes_tr o read_class o ProofContext.theory_of),
+ ("_type_name", type_name_tr o read_type o ProofContext.theory_of),
+ ("_tapp", tapp_ast_tr o read_type o ProofContext.theory_of),
+ ("_tappl", tappl_ast_tr o read_type o ProofContext.theory_of),
+ ("_bracket", K bracket_ast_tr)],
[],
[],
- map SynExt.mk_trfun [("fun", K fun_ast_tr')])
+ map SynExt.mk_trfun [("\\<^type>fun", K fun_ast_tr')])
[]
([], []);
--- a/src/Pure/pure_thy.ML Wed Mar 03 08:49:11 2010 -0800
+++ b/src/Pure/pure_thy.ML Wed Mar 03 10:40:40 2010 -0800
@@ -225,6 +225,8 @@
val typ = Simple_Syntax.read_typ;
val prop = Simple_Syntax.read_prop;
+
+val tycon = Syntax.mark_type;
val const = Syntax.mark_const;
val typeT = Syntax.typeT;
@@ -318,21 +320,21 @@
(const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]
#> Sign.add_syntax_i applC_syntax
#> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
- [("fun", typ "type => type => type", Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
- ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
- ("_ofsort", typ "tid => sort => type", Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
- ("_constrain", typ "logic => type => logic", Mixfix ("_\\<Colon>_", [4, 0], 3)),
- ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\\<Colon>_", [4, 0], 3)),
- ("_idtyp", typ "id => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
- ("_idtypdummy", typ "type => idt", Mixfix ("'_()\\<Colon>_", [], 0)),
- ("_type_constraint_", typ "'a", NoSyn),
- ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
- (const "==", typ "'a => 'a => prop", Infixr ("\\<equiv>", 2)),
- (const "all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
- (const "==>", typ "prop => prop => prop", Infixr ("\\<Longrightarrow>", 1)),
- ("_DDDOT", typ "aprop", Delimfix "\\<dots>"),
- ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
- ("_DDDOT", typ "logic", Delimfix "\\<dots>")]
+ [(tycon "fun", typ "type => type => type", Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
+ ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
+ ("_ofsort", typ "tid => sort => type", Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
+ ("_constrain", typ "logic => type => logic", Mixfix ("_\\<Colon>_", [4, 0], 3)),
+ ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\\<Colon>_", [4, 0], 3)),
+ ("_idtyp", typ "id => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
+ ("_idtypdummy", typ "type => idt", Mixfix ("'_()\\<Colon>_", [], 0)),
+ ("_type_constraint_", typ "'a", NoSyn),
+ ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
+ (const "==", typ "'a => 'a => prop", Infixr ("\\<equiv>", 2)),
+ (const "all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
+ (const "==>", typ "prop => prop => prop", Infixr ("\\<Longrightarrow>", 1)),
+ ("_DDDOT", typ "aprop", Delimfix "\\<dots>"),
+ ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
+ ("_DDDOT", typ "logic", Delimfix "\\<dots>")]
#> Sign.add_modesyntax_i ("", false)
[(const "prop", typ "prop => prop", Mixfix ("_", [0], 0))]
#> Sign.add_modesyntax_i ("HTML", false)
--- a/src/Pure/sign.ML Wed Mar 03 08:49:11 2010 -0800
+++ b/src/Pure/sign.ML Wed Mar 03 10:40:40 2010 -0800
@@ -56,10 +56,7 @@
val intern_sort: theory -> sort -> sort
val extern_sort: theory -> sort -> sort
val intern_typ: theory -> typ -> typ
- val extern_typ: theory -> typ -> typ
val intern_term: theory -> term -> term
- val extern_term: theory -> term -> term
- val intern_tycons: theory -> typ -> typ
val the_type_decl: theory -> string -> Type.decl
val arity_number: theory -> string -> int
val arity_sorts: theory -> string -> sort -> sort list
@@ -157,7 +154,7 @@
make_sign (Name_Space.default_naming, syn, tsig, consts);
val empty =
- make_sign (Name_Space.default_naming, Syntax.basic_syn, Type.empty_tsig, Consts.empty);
+ make_sign (Name_Space.default_naming, Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
fun merge pp (sign1, sign2) =
let
@@ -266,41 +263,10 @@
| map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t)
| map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
-val add_classesT = Term.fold_atyps
- (fn TFree (_, S) => fold (insert (op =)) S
- | TVar (_, S) => fold (insert (op =)) S
- | _ => I);
-
-fun add_tyconsT (Type (c, Ts)) = insert (op =) c #> fold add_tyconsT Ts
- | add_tyconsT _ = I;
-
-val add_consts = Term.fold_aterms (fn Const (c, _) => insert (op =) c | _ => I);
-
-fun mapping add_names f t =
- let
- fun f' (x: string) = let val y = f x in if x = y then NONE else SOME (x, y) end;
- val tab = map_filter f' (add_names t []);
- fun get x = the_default x (AList.lookup (op =) tab x);
- in get end;
-
-fun typ_mapping f g thy T =
- T |> map_typ
- (mapping add_classesT (f thy) T)
- (mapping add_tyconsT (g thy) T);
-
-fun term_mapping f g h thy t =
- t |> map_term
- (mapping (Term.fold_types add_classesT) (f thy) t)
- (mapping (Term.fold_types add_tyconsT) (g thy) t)
- (mapping add_consts (h thy) t);
-
in
-val intern_typ = typ_mapping intern_class intern_type;
-val extern_typ = typ_mapping extern_class extern_type;
-val intern_term = term_mapping intern_class intern_type intern_const;
-val extern_term = term_mapping extern_class extern_type (K Syntax.mark_const);
-val intern_tycons = typ_mapping (K I) intern_type;
+fun intern_typ thy = map_typ (intern_class thy) (intern_type thy);
+fun intern_term thy = map_term (intern_class thy) (intern_type thy) (intern_const thy);
end;
@@ -424,6 +390,27 @@
val cert_arity = prep_arity (K I) certify_sort;
+(* type syntax entities *)
+
+local
+
+fun read_type thy text =
+ let
+ val (syms, pos) = Syntax.read_token text;
+ val c = intern_type thy (Symbol_Pos.content syms);
+ val _ = the_type_decl thy c;
+ val _ = Position.report (Markup.tycon c) pos;
+ in c end;
+
+in
+
+val _ = Context.>>
+ (Context.map_theory
+ (map_syn (K (Syntax.basic_syntax {read_class = read_class, read_type = read_type}))));
+
+end;
+
+
(** signature extension functions **) (*exception ERROR/TYPE*)
@@ -438,11 +425,13 @@
(* add type constructors *)
+val type_syntax = Syntax.mark_type oo full_name;
+
fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
let
val syn' =
Syntax.update_type_gram true Syntax.mode_default
- (map (fn (a, n, mx) => (Name.of_binding a, Syntax.make_type n, mx)) types) syn;
+ (map (fn (a, n, mx) => (type_syntax thy a, Syntax.make_type n, mx)) types) syn;
val decls = map (fn (a, n, _) => (a, n)) types;
val tsig' = fold (Type.add_type naming) decls tsig;
in (naming, syn', tsig', consts) end);
@@ -452,9 +441,8 @@
fun add_nonterminals ns thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
let
- val syn' = Syntax.update_consts (map Name.of_binding ns) syn;
val tsig' = fold (Type.add_nonterminal naming) ns tsig;
- in (naming, syn', tsig', consts) end);
+ in (naming, syn, tsig', consts) end);
(* add type abbreviations *)
@@ -465,7 +453,7 @@
val ctxt = ProofContext.init thy;
val syn' =
Syntax.update_type_gram true Syntax.mode_default
- [(Name.of_binding b, Syntax.make_type (length vs), mx)] syn;
+ [(type_syntax thy b, Syntax.make_type (length vs), mx)] syn;
val abbr = (b, vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
val tsig' = Type.add_abbrev naming abbr tsig;
@@ -495,8 +483,8 @@
fun type_notation add mode args =
let
- fun type_syntax (Type (c, args), mx) = (* FIXME authentic syntax *)
- SOME (Long_Name.base_name c, Syntax.make_type (length args), mx)
+ fun type_syntax (Type (c, args), mx) =
+ SOME (Syntax.mark_type c, Syntax.make_type (length args), mx)
| type_syntax _ = NONE;
in map_syn (Syntax.update_type_gram add mode (map_filter type_syntax args)) end;
@@ -579,9 +567,8 @@
fun primitive_class (bclass, classes) thy =
thy |> map_sign (fn (naming, syn, tsig, consts) =>
let
- val syn' = Syntax.update_consts [Name.of_binding bclass] syn;
val tsig' = Type.add_class (Syntax.pp_global thy) naming (bclass, classes) tsig;
- in (naming, syn', tsig', consts) end)
+ in (naming, syn, tsig', consts) end)
|> add_consts_i [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (Syntax.pp_global thy) arg);
--- a/src/Sequents/Sequents.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/Sequents/Sequents.thy Wed Mar 03 10:40:40 2010 -0800
@@ -65,7 +65,7 @@
(* parse translation for sequences *)
-fun abs_seq' t = Abs ("s", Type (@{type_syntax seq'}, []), t);
+fun abs_seq' t = Abs ("s", Type (@{type_name seq'}, []), t);
fun seqobj_tr (Const (@{syntax_const "_SeqO"}, _) $ f) =
Const (@{const_syntax SeqO'}, dummyT) $ f
--- a/src/ZF/Induct/Comb.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/ZF/Induct/Comb.thy Wed Mar 03 10:40:40 2010 -0800
@@ -23,6 +23,9 @@
| S
| app ("p \<in> comb", "q \<in> comb") (infixl "@@" 90)
+notation (xsymbols)
+ app (infixl "\<bullet>" 90)
+
text {*
Inductive definition of contractions, @{text "-1->"} and
(multi-step) reductions, @{text "--->"}.
@@ -39,9 +42,6 @@
contract_multi :: "[i,i] => o" (infixl "--->" 50)
where "p ---> q == <p,q> \<in> contract^*"
-syntax (xsymbols)
- "comb.app" :: "[i, i] => i" (infixl "\<bullet>" 90)
-
inductive
domains "contract" \<subseteq> "comb \<times> comb"
intros
--- a/src/ZF/List_ZF.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/ZF/List_ZF.thy Wed Mar 03 10:40:40 2010 -0800
@@ -15,8 +15,8 @@
syntax
- "[]" :: i ("[]")
- "_List" :: "is => i" ("[(_)]")
+ "_Nil" :: i ("[]")
+ "_List" :: "is => i" ("[(_)]")
translations
"[x, xs]" == "CONST Cons(x, [xs])"
--- a/src/ZF/UNITY/Union.thy Wed Mar 03 08:49:11 2010 -0800
+++ b/src/ZF/UNITY/Union.thy Wed Mar 03 10:40:40 2010 -0800
@@ -40,23 +40,22 @@
"safety_prop(X) == X\<subseteq>program &
SKIP \<in> X & (\<forall>G \<in> program. Acts(G) \<subseteq> (\<Union>F \<in> X. Acts(F)) --> G \<in> X)"
+notation (xsymbols)
+ SKIP ("\<bottom>") and
+ Join (infixl "\<squnion>" 65)
+
syntax
"_JOIN1" :: "[pttrns, i] => i" ("(3JN _./ _)" 10)
"_JOIN" :: "[pttrn, i, i] => i" ("(3JN _:_./ _)" 10)
+syntax (xsymbols)
+ "_JOIN1" :: "[pttrns, i] => i" ("(3\<Squnion> _./ _)" 10)
+ "_JOIN" :: "[pttrn, i, i] => i" ("(3\<Squnion> _ \<in> _./ _)" 10)
translations
"JN x:A. B" == "CONST JOIN(A, (%x. B))"
"JN x y. B" == "JN x. JN y. B"
"JN x. B" == "CONST JOIN(CONST state,(%x. B))"
-notation (xsymbols)
- SKIP ("\<bottom>") and
- Join (infixl "\<squnion>" 65)
-
-syntax (xsymbols)
- "_JOIN1" :: "[pttrns, i] => i" ("(3\<Squnion> _./ _)" 10)
- "_JOIN" :: "[pttrn, i, i] => i" ("(3\<Squnion> _ \<in> _./ _)" 10)
-
subsection{*SKIP*}