# HG changeset patch # User huffman # Date 1267641640 28800 # Node ID f5ec817df77f07c2c8430f7a3e001987f513c26f # Parent e27550a842b99fdf92db086b5c42eabeb4e7f5f0# Parent 6d3fa3a378221c9807c6e68da6122c2a66e8ffcc merged diff -r e27550a842b9 -r f5ec817df77f Admin/Mercurial/isabelle-style.diff --- 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 -< #date|age# ago#desc|strip|firstline|escape# {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag} -< -<
-<
-< changeset
-<
-< #author|obfuscate# [#date|rfc822date#] rev #rev#
---- -> #date|age# ago#author|obfuscate# [#date|rfc822date#] rev #rev# {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag} -12a7,9 ->
-> #files# ->
-diff -r gitweb/changeset.tmpl isabelle/changeset.tmpl -19c19 -< #desc|strip|escape|firstline# {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag} ---- -> #desc|strip|escape# {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag} -diff -r gitweb/map isabelle/map -29c29 -< annotateline = '#author|user#@#rev#
#linenumber#
#line|escape#
' ---- -> annotateline = '#author|user#@#rev#
#linenumber#
#line|escape#
' -59,60c59,60 -< shortlogentry = '#date|age# ago#author|person##desc|strip|firstline|escape# {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}changeset | files' -< filelogentry = '#date|age# ago#desc|strip|firstline|escape#file | diff | annotate #rename%filelogrename#' ---- -> shortlogentry = '#date|age# ago#date|shortdate##author|person##desc|strip|escape# {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}changeset | files' -> filelogentry = '#date|age# ago#date|shortdate##author|person##desc|strip|escape#file | diff | annotate #rename%filelogrename#' -diff -r gitweb/summary.tmpl isabelle/summary.tmpl -34d33 -< owner#owner|obfuscate# +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 @@ +
+-{date|age}{desc|strip|firstline|escape|nonempty} {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag} +-
+-
+-
+-changeset
+-
+-{author|obfuscate} [{date|rfc822date}] rev {rev}
++{date|age} ++{author|obfuscate} [{date|rfc822date}] rev {rev} {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag} +
+
+ {desc|strip|escape|addbreaks|nonempty} +
++
++{files} ++
+
+
+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 @@ + + {date|age} + {author|person} ++ {date|shortdate} + + +- {desc|strip|firstline|escape|nonempty} ++ {desc|strip|escape|nonempty} + {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag} + + diff -r e27550a842b9 -r f5ec817df77f NEWS --- 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. diff -r e27550a842b9 -r f5ec817df77f doc-src/Locales/Locales/Examples3.thy --- 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 diff -r e27550a842b9 -r f5ec817df77f doc-src/Locales/Locales/document/Examples3.tex --- 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% diff -r e27550a842b9 -r f5ec817df77f src/HOL/Bali/AxSem.thy --- 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 @@ "\Vals:v. b" == "(\v. b) \ CONST the_In3" --{* relation on result values, state and auxiliary variables *} -types 'a assn = "res \ state \ 'a \ bool" +types 'a assn = "res \ state \ 'a \ bool" translations - "res" <= (type) "AxSem.res" - "a assn" <= (type) "vals \ state \ a \ bool" + (type) "'a assn" <= (type) "vals \ state \ 'a \ bool" definition assn_imp :: "'a assn \ 'a assn \ bool" (infixr "\" 25) where "P \ Q \ \Y s Z. P Y s Z \ Q Y s Z" diff -r e27550a842b9 -r f5ec817df77f src/HOL/Bali/Basis.thy --- 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" diff -r e27550a842b9 -r f5ec817df77f src/HOL/Bali/Decl.thy --- 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) "\access::acc_modi\" - "decl" <= (type) "\access::acc_modi,\::'a\" + (type) "decl" <= (type) "\access::acc_modi\" + (type) "decl" <= (type) "\access::acc_modi,\::'a\" subsection {* Member (field or method)*} record member = decl + static :: stat_modi translations - "member" <= (type) "\access::acc_modi,static::bool\" - "member" <= (type) "\access::acc_modi,static::bool,\::'a\" + (type) "member" <= (type) "\access::acc_modi,static::bool\" + (type) "member" <= (type) "\access::acc_modi,static::bool,\::'a\" subsection {* Field *} record field = member + type :: ty translations - "field" <= (type) "\access::acc_modi, static::bool, type::ty\" - "field" <= (type) "\access::acc_modi, static::bool, type::ty,\::'a\" + (type) "field" <= (type) "\access::acc_modi, static::bool, type::ty\" + (type) "field" <= (type) "\access::acc_modi, static::bool, type::ty,\::'a\" types fdecl (* field declaration, cf. 8.3 *) @@ -174,7 +174,7 @@ translations - "fdecl" <= (type) "vname \ field" + (type) "fdecl" <= (type) "vname \ field" subsection {* Method *} @@ -193,17 +193,17 @@ translations - "mhead" <= (type) "\access::acc_modi, static::bool, + (type) "mhead" <= (type) "\access::acc_modi, static::bool, pars::vname list, resT::ty\" - "mhead" <= (type) "\access::acc_modi, static::bool, + (type) "mhead" <= (type) "\access::acc_modi, static::bool, pars::vname list, resT::ty,\::'a\" - "mbody" <= (type) "\lcls::(vname \ ty) list,stmt::stmt\" - "mbody" <= (type) "\lcls::(vname \ ty) list,stmt::stmt,\::'a\" - "methd" <= (type) "\access::acc_modi, static::bool, + (type) "mbody" <= (type) "\lcls::(vname \ ty) list,stmt::stmt\" + (type) "mbody" <= (type) "\lcls::(vname \ ty) list,stmt::stmt,\::'a\" + (type) "methd" <= (type) "\access::acc_modi, static::bool, pars::vname list, resT::ty,mbody::mbody\" - "methd" <= (type) "\access::acc_modi, static::bool, + (type) "methd" <= (type) "\access::acc_modi, static::bool, pars::vname list, resT::ty,mbody::mbody,\::'a\" - "mdecl" <= (type) "sig \ methd" + (type) "mdecl" <= (type) "sig \ methd" definition mhead :: "methd \ mhead" where @@ -306,13 +306,13 @@ = "qtname \ iface" translations - "ibody" <= (type) "\access::acc_modi,imethods::(sig \ mhead) list\" - "ibody" <= (type) "\access::acc_modi,imethods::(sig \ mhead) list,\::'a\" - "iface" <= (type) "\access::acc_modi,imethods::(sig \ mhead) list, + (type) "ibody" <= (type) "\access::acc_modi,imethods::(sig \ mhead) list\" + (type) "ibody" <= (type) "\access::acc_modi,imethods::(sig \ mhead) list,\::'a\" + (type) "iface" <= (type) "\access::acc_modi,imethods::(sig \ mhead) list, isuperIfs::qtname list\" - "iface" <= (type) "\access::acc_modi,imethods::(sig \ mhead) list, + (type) "iface" <= (type) "\access::acc_modi,imethods::(sig \ mhead) list, isuperIfs::qtname list,\::'a\" - "idecl" <= (type) "qtname \ iface" + (type) "idecl" <= (type) "qtname \ iface" definition ibody :: "iface \ ibody" where "ibody i \ \access=access i,imethods=imethods i\" @@ -337,17 +337,17 @@ = "qtname \ class" translations - "cbody" <= (type) "\access::acc_modi,cfields::fdecl list, + (type) "cbody" <= (type) "\access::acc_modi,cfields::fdecl list, methods::mdecl list,init::stmt\" - "cbody" <= (type) "\access::acc_modi,cfields::fdecl list, + (type) "cbody" <= (type) "\access::acc_modi,cfields::fdecl list, methods::mdecl list,init::stmt,\::'a\" - "class" <= (type) "\access::acc_modi,cfields::fdecl list, + (type) "class" <= (type) "\access::acc_modi,cfields::fdecl list, methods::mdecl list,init::stmt, super::qtname,superIfs::qtname list\" - "class" <= (type) "\access::acc_modi,cfields::fdecl list, + (type) "class" <= (type) "\access::acc_modi,cfields::fdecl list, methods::mdecl list,init::stmt, super::qtname,superIfs::qtname list,\::'a\" - "cdecl" <= (type) "qtname \ class" + (type) "cdecl" <= (type) "qtname \ class" definition cbody :: "class \ cbody" where "cbody c \ \access=access c, cfields=cfields c,methods=methods c,init=init c\" @@ -404,8 +404,8 @@ "classes"::"cdecl list" translations - "prog"<= (type) "\ifaces::idecl list,classes::cdecl list\" - "prog"<= (type) "\ifaces::idecl list,classes::cdecl list,\::'a\" + (type) "prog" <= (type) "\ifaces::idecl list,classes::cdecl list\" + (type) "prog" <= (type) "\ifaces::idecl list,classes::cdecl list,\::'a\" abbreviation iface :: "prog \ (qtname, iface) table" diff -r e27550a842b9 -r f5ec817df77f src/HOL/Bali/DeclConcepts.thy --- 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 \ qtname" translations - "fspec" <= (type) "vname \ qtname" + (type) "fspec" <= (type) "vname \ qtname" definition imethds :: "prog \ qtname \ (sig,qtname \ mhead) tables" where "imethds G I diff -r e27550a842b9 -r f5ec817df77f src/HOL/Bali/Eval.thy --- 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 \ (val \ state \ state)" vals = "(val, vvar, val list) sum3" translations - "vvar" <= (type) "val \ (val \ state \ state)" - "vals" <= (type)"(val, vvar, val list) sum3" + (type) "vvar" <= (type) "val \ (val \ state \ 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 diff -r e27550a842b9 -r f5ec817df77f src/HOL/Bali/Name.thy --- 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) \ q" translations - "mname" <= "Name.mname" - "xname" <= "Name.xname" - "tname" <= "Name.tname" - "ename" <= "Name.ename" - "qtname" <= (type) "\pid::pname,tid::tname\" + (type) "qtname" <= (type) "\pid::pname,tid::tname\" (type) "'a qtname_scheme" <= (type) "\pid::pname,tid::tname,\::'a\" diff -r e27550a842b9 -r f5ec817df77f src/HOL/Bali/State.thy --- 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 \ qtname" - "vn" <= (type) "fspec + int" - "obj" <= (type) "\tag::obj_tag, values::vn \ val option\" - "obj" <= (type) "\tag::obj_tag, values::vn \ val option,\::'a\" + (type) "fspec" <= (type) "vname \ qtname" + (type) "vn" <= (type) "fspec + int" + (type) "obj" <= (type) "\tag::obj_tag, values::vn \ val option\" + (type) "obj" <= (type) "\tag::obj_tag, values::vn \ val option,\::'a\" definition the_Arr :: "obj option \ ty \ int \ (vn, val) table" where "the_Arr obj \ SOME (T,k,t). obj = Some \tag=Arr T k,values=t\" @@ -134,7 +134,7 @@ translations "Heap" => "CONST Inl" "Stat" => "CONST Inr" - "oref" <= (type) "loc + qtname" + (type) "oref" <= (type) "loc + qtname" definition fields_table :: "prog \ qtname \ (fspec \ field \ bool) \ (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 \ st" --{* state including abruption information *} translations - "abopt" <= (type) "State.abrupt option" - "abopt" <= (type) "abrupt option" - "state" <= (type) "abopt \ State.st" - "state" <= (type) "abopt \ st" + (type) "abopt" <= (type) "abrupt option" + (type) "state" <= (type) "abopt \ st" abbreviation Norm :: "st \ state" diff -r e27550a842b9 -r f5ec817df77f src/HOL/Bali/Table.thy --- 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 \ map_of" translations - (type)"'a \ 'b" <= (type)"'a \ 'b Datatype.option" - (type)"('a, 'b) table" <= (type)"'a \ 'b" + (type) "('a, 'b) table" <= (type) "'a \ 'b" (* ### To map *) lemma map_add_find_left[simp]: diff -r e27550a842b9 -r f5ec817df77f src/HOL/Bali/Term.thy --- 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) "\name::mname,parTs::ty list\" - "sig" <= (type) "\name::mname,parTs::ty list,\::'a\" + (type) "sig" <= (type) "\name::mname,parTs::ty list\" + (type) "sig" <= (type) "\name::mname,parTs::ty list,\::'a\" --{* 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 \ 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 \ ty list" + (type) "term" <= (type) "(expr+stmt,var,expr list) sum3" abbreviation this :: expr where "this == Acc (LVar This)" diff -r e27550a842b9 -r f5ec817df77f src/HOL/Bali/Type.thy --- 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)" diff -r e27550a842b9 -r f5ec817df77f src/HOL/Bali/Value.thy --- 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 \ bool" primrec "the_Bool (Bool b) = b" consts the_Intg :: "val \ int" diff -r e27550a842b9 -r f5ec817df77f src/HOL/Bali/WellType.thy --- 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 \ ty option" - "env" <= (type) "\prg::prog,cls::qtname,lcl::lenv\" - "env" <= (type) "\prg::prog,cls::qtname,lcl::lenv,\::'a\" + (type) "lenv" <= (type) "(lname, ty) table" + (type) "lenv" <= (type) "lname \ ty option" + (type) "env" <= (type) "\prg::prog,cls::qtname,lcl::lenv\" + (type) "env" <= (type) "\prg::prog,cls::qtname,lcl::lenv,\::'a\" 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 diff -r e27550a842b9 -r f5ec817df77f src/HOL/IMPP/Hoare.thy --- 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 diff -r e27550a842b9 -r f5ec817df77f src/HOL/Imperative_HOL/Heap_Monad.thy --- 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 \ mrec_dom x" + "mrec_graph x y \ mrec_dom x" apply (induct rule:mrec_graph.induct) apply (rule accpI) apply (erule mrec_rel.cases) by simp lemma f_default: "\ mrec_dom (f, g, x, h) \ 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: diff -r e27550a842b9 -r f5ec817df77f src/HOL/Imperative_HOL/ex/Linked_Lists.thy --- 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 \ make_llist xs; next \ Ref.new tl; - return (Node x next) - done" + return (Node x next) + done" text {* define traverse using the MREC combinator *} diff -r e27550a842b9 -r f5ec817df77f src/HOL/IsaMakefile --- 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 \ diff -r e27550a842b9 -r f5ec817df77f src/HOL/Library/Numeral_Type.thy --- 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 \ t set)" +translations "CARD('t)" => "CONST card (CONST UNIV \ 't set)" typed_print_translation {* let diff -r e27550a842b9 -r f5ec817df77f src/HOL/Library/RBT.thy --- 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 \ 'b \ ('a,'b) rbt \ bool" +primrec entry_in_tree :: "'a \ 'b \ ('a, 'b) rbt \ bool" where - "pin_tree k v Empty = False" -| "pin_tree k v (Tr c l x y r) = (k = x \ v = y \ pin_tree k v l \ pin_tree k v r)" + "entry_in_tree k v Empty = False" +| "entry_in_tree k v (Branch c l x y r) \ k = x \ v = y \ entry_in_tree k v l \ entry_in_tree k v r" -primrec - keys :: "('k,'v) rbt \ 'k set" +primrec keys :: "('k, 'v) rbt \ 'k set" where "keys Empty = {}" -| "keys (Tr _ l k _ r) = { k } \ keys l \ keys r" +| "keys (Branch _ l k _ r) = { k } \ keys l \ keys r" -lemma pint_keys: "pin_tree k v t \ k \ keys t" by (induct t) auto +lemma entry_in_tree_keys: + "entry_in_tree k v t \ k \ keys t" + by (induct t) auto -primrec tlt :: "'a\order \ ('a,'b) rbt \ bool" +definition tree_less :: "'a\order \ ('a, 'b) rbt \ bool" where - "tlt k Empty = True" -| "tlt k (Tr c lt kt v rt) = (kt < k \ tlt k lt \ tlt k rt)" + tree_less_prop: "tree_less k t \ (\x\keys t. x < k)" + +abbreviation tree_less_symbol (infix "|\" 50) +where "t |\ x \ tree_less x t" -abbreviation tllt (infix "|\" 50) -where "t |\ x == tlt x t" +definition tree_greater :: "'a\order \ ('a, 'b) rbt \ bool" (infix "\|" 50) +where + tree_greater_prop: "tree_greater k t = (\x\keys t. k < x)" -primrec tgt :: "'a\order \ ('a,'b) rbt \ bool" (infix "\|" 50) -where - "tgt k Empty = True" -| "tgt k (Tr c lt kt v rt) = (k < kt \ tgt k lt \ tgt k rt)" +lemma tree_less_simps [simp]: + "tree_less k Empty = True" + "tree_less k (Branch c lt kt v rt) \ kt < k \ tree_less k lt \ tree_less k rt" + by (auto simp add: tree_less_prop) -lemma tlt_prop: "(t |\ k) = (\x\keys t. x < k)" by (induct t) auto -lemma tgt_prop: "(k \| t) = (\x\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) \ k < kt \ tree_greater k lt \ 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: "\ t |\ x; x < y \ \ t |\ y" - and tgt_trans: "\ x < y; y \| t\ \ x \| 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 \ bool" -where - "st Empty = True" -| "st (Tr c l k v r) = (l |\ k \ k \| r \ st l \ st r)" +lemma tree_less_trans: "t |\ x \ x < y \ t |\ y" + and tree_greater_trans: "x < y \ y \| t \ x \| t" +by (auto simp: tree_ord_props) -primrec map_of :: "('a\linorder, 'b) rbt \ 'a \ 'b" +primrec sorted :: "('a::linorder, 'b) rbt \ 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 |\ k \ k \| r \ sorted l \ sorted r)" -lemma map_of_tlt[simp]: "t |\ k \ map_of t k = None" +primrec lookup :: "('a\linorder, 'b) rbt \ 'a \ '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 |\ k \ lookup t k = None" by (induct t) auto -lemma map_of_tgt[simp]: "k \| t \ map_of t k = None" +lemma lookup_tree_greater[simp]: "k \| t \ lookup t k = None" by (induct t) auto -lemma mapof_keys: "st t \ dom (map_of t) = keys t" -by (induct t) (auto simp: dom_def tgt_prop tlt_prop) +lemma lookup_keys: "sorted t \ dom (lookup t) = keys t" +by (induct t) (auto simp: dom_def tree_greater_prop tree_less_prop) -lemma mapof_pit: "st t \ (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 \ (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: "\v. pin_tree (k\'a\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: "\v. entry_in_tree (k\'a\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 "\v. \ pin_tree k v t1" - by (simp add: mapof_pit[symmetric] st) + then have "\v. \ 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 \ color" +primrec color_of :: "('a, 'b) rbt \ color" where - "treec Empty = B" -| "treec (Tr c _ _ _ _) = c" + "color_of Empty = B" +| "color_of (Branch c _ _ _ _) = c" -primrec inv1 :: "('a,'b) rbt \ bool" +primrec bheight :: "('a,'b) rbt \ 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 \ bool" where "inv1 Empty = True" -| "inv1 (Tr c lt k v rt) = (inv1 lt \ inv1 rt \ (c = B \ treec lt = B \ treec rt = B))" +| "inv1 (Branch c lt k v rt) \ inv1 lt \ inv1 rt \ (c = B \ color_of lt = B \ color_of rt = B)" -(* Weaker version *) -primrec inv1l :: "('a,'b) rbt \ bool" +primrec inv1l :: "('a, 'b) rbt \ bool" -- {* Weaker version *} where "inv1l Empty = True" -| "inv1l (Tr c l k v r) = (inv1 l \ inv1 r)" +| "inv1l (Branch c l k v r) = (inv1 l \ inv1 r)" lemma [simp]: "inv1 t \ inv1l t" by (cases t) simp+ -primrec bh :: "('a,'b) rbt \ 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 \ bool" +primrec inv2 :: "('a, 'b) rbt \ bool" where "inv2 Empty = True" -| "inv2 (Tr c lt k v rt) = (inv2 lt \ inv2 rt \ bh lt = bh rt)" +| "inv2 (Branch c lt k v rt) = (inv2 lt \ inv2 rt \ bheight lt = bheight rt)" -definition - "isrbt t = (inv1 t \ inv2 t \ treec t = B \ st t)" - -lemma isrbt_st[simp]: "isrbt t \ st t" by (simp add: isrbt_def) +definition is_rbt :: "('a\linorder, 'b) rbt \ bool" where + "is_rbt t \ inv1 t \ inv2 t \ color_of t = B \ 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 \ 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 \ 'a \ 'b \ ('a,'b) rbt \ ('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: "\inv1l l; inv1l r\ \ inv1 (balance l k v r)" by (induct l k v r rule: balance.induct) auto -lemma balance_bh: "bh l = bh r \ bh (balance l k v r) = Suc (bh l)" +lemma balance_bheight: "bheight l = bheight r \ 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 \| balance a k x b) = (v \| a \ v \| b \ v < k)" +lemma balance_tree_greater[simp]: "(v \| balance a k x b) = (v \| a \ v \| b \ v < k)" by (induct a k x b rule: balance.induct) auto -lemma balance_tlt[simp]: "(balance a k x b |\ v) = (a |\ v \ b |\ v \ k < v)" +lemma balance_tree_less[simp]: "(balance a k x b |\ v) = (a |\ v \ b |\ v \ 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 |\ k" "k \| r" - shows "st (balance l k v r)" + assumes "sorted l" "sorted r" "l |\ k" "k \| 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 \ z \| 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 \ z \| 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ k = v \ x = y \ pin_tree k x r)" + "entry_in_tree k x (balance l v y r) = (entry_in_tree k x l \ k = v \ x = y \ 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 |\ k" "k \| 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 |\ k" "k \| 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 \ ('a,'b) rbt \ ('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 \ inv1l (paint c t)" by (cases t) auto lemma paint_inv1[simp]: "inv1l t \ inv1 (paint B t)" by (cases t) auto lemma paint_inv2[simp]: "inv2 t \ 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 \ 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 \| paint c t) = (v \| t)" by (cases t) auto -lemma paint_tlt[simp]: "(paint c t |\ v) = (t |\ 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 \ 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 \| paint c t) = (v \| t)" by (cases t) auto +lemma paint_tree_less[simp]: "(paint c t |\ v) = (t |\ v)" by (cases t) auto fun ins :: "('a\linorder \ 'b \ 'b \ 'b) \ 'a \ 'b \ ('a,'b) rbt \ ('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 \ 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 \ 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 \| ins f k x t) = (v \| t \ k > v)" +lemma ins_tree_greater[simp]: "(v \| ins f k x t) = (v \| t \ k > v)" by (induct f k x t rule: ins.induct) auto -lemma ins_tlt[simp]: "(ins f k x t |\ v) = (t |\ v \ k < v)" +lemma ins_tree_less[simp]: "(ins f k x t |\ v) = (t |\ v \ k < v)" by (induct f k x t rule: ins.induct) auto -lemma ins_st[simp]: "st t \ 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 \ 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 } \ 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 \ v + assumes "sorted t" + shows "lookup (ins f k v t) x = ((lookup t)(k |-> case lookup t k of None \ v | Some w \ 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 \ st (insertwithkey f k x t)" +lemma insertwk_sorted: "sorted t \ 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 \ v +lemma lookup_insertwk: + assumes "sorted t" + shows "lookup (insertwithkey f k v t) x = ((lookup t)(k |-> case lookup t k of None \ v | Some w \ 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 (\_. f)" -lemma insertw_st: "st t \ st (insertwith f k v t)" by (simp add: insertwk_st insertw_def) -theorem insertw_isrbt: "isrbt t \ isrbt (insertwith f k v t)" by (simp add: insertwk_isrbt insertw_def) +lemma insertw_sorted: "sorted t \ sorted (insertwith f k v t)" by (simp add: insertwk_sorted insertw_def) +theorem insertw_is_rbt: "is_rbt t \ 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 \ (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 \ (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 (\_ _ nv. nv) k v t" +definition insert :: "'a\linorder \ 'b \ ('a, 'b) rbt \ ('a, 'b) rbt" where + "insert k v t = insertwithkey (\_ _ nv. nv) k v t" -lemma insrt_st: "st t \ st (insrt k v t)" by (simp add: insertwk_st insrt_def) -theorem insrt_isrbt: "isrbt t \ isrbt (insrt k v t)" by (simp add: insertwk_isrbt insrt_def) +lemma insert_sorted: "sorted t \ sorted (insert k v t)" by (simp add: insertwk_sorted insert_def) +theorem insert_is_rbt: "is_rbt t \ 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\v)" -unfolding insrt_def +lemma lookup_insert: + assumes "is_rbt t" + shows "lookup (insert k v t) = (lookup t)(k\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 \ bh (paint R t) = bh t - 1" +lemma bheight_paintR'[simp]: "color_of t = B \ bheight (paint R t) = bheight t - 1" by (cases t rule: rbt_cases) auto fun balleft :: "('a,'b) rbt \ 'a \ 'b \ ('a,'b) rbt \ ('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: "\inv1l a; inv1 b; treec b = B\ \ inv1 (balleft a k x b)" +lemma balleft_inv1: "\inv1l a; inv1 b; color_of b = B\ \ inv1 (balleft a k x b)" by (induct a k x b rule: balleft.induct) (simp add: balance_inv1)+ lemma balleft_inv1l: "\ inv1l lt; inv1 rt \ \ inv1l (balleft lt k x rt)" by (induct lt k x rt rule: balleft.induct) (auto simp: balance_inv1) -lemma balleft_st: "\ st l; st r; tlt k l; tgt k r \ \ st (balleft l k v r)" +lemma balleft_sorted: "\ sorted l; sorted r; tree_less k l; tree_greater k r \ \ 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 \| a" "k \| b" "k < x" shows "k \| 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 |\ k" "b |\ k" "x < k" shows "balleft a x t b |\ 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 \ k = a \ v = b \ 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 \ k = a \ v = b \ 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 \ 'a \ 'b \ ('a,'b) rbt \ ('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) \ 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) \ 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: "\inv1 a; inv1l b; treec a = B\ \ inv1 (balright a k x b)" +lemma balright_inv1: "\inv1 a; inv1l b; color_of a = B\ \ inv1 (balright a k x b)" by (induct a k x b rule: balright.induct) (simp add: balance_inv1)+ lemma balright_inv1l: "\ inv1 lt; inv1l rt \ \inv1l (balright lt k x rt)" by (induct lt k x rt rule: balright.induct) (auto simp: balance_inv1) -lemma balright_st: "\ st l; st r; tlt k l; tgt k r \ \ st (balright l k v r)" +lemma balright_sorted: "\ sorted l; sorted r; tree_less k l; tree_greater k r \ \ 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 \| a" "k \| b" "k < x" shows "k \| 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 |\ k" "b |\ k" "x < k" shows "balright a x t b |\ 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 \ x = k \ y = v \ 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 \ x = k \ y = v \ 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 \ (Tr R (Tr R a k x b2) t z (Tr R c2 s y d)) | - bc \ 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 \ Tr R (Tr B a k x b2) t z (Tr B c2 s y d) | - bc \ 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 \ (Branch R (Branch R a k x b2) t z (Branch R c2 s y d)) | + bc \ 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 \ Branch R (Branch B a k x b2) t z (Branch B c2 s y d) | + bc \ 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 \ treec rt = B \ inv1 (app lt rt)" + shows "color_of lt = B \ color_of rt = B \ 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 \| l" "k \| r" shows "k \| 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 |\ k" "r |\ k" shows "app l r |\ 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 |\ k" "k \| r" - shows "st (app l r)" + assumes "sorted l" "sorted r" "l |\ k" "k \| 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 |\ x" "x \| b" "b |\ k" "k \| c" "c |\ y" "y \| 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ tlt x a" by simp - hence 5: "tlt va a" by (blast dest: tlt_trans) - from Red 3 4 have "va < y \ tgt y d" by simp - hence "tgt va d" by (blast dest: tgt_trans) + with 2 4 have "x < va \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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\linorder) \ ('a,'b) rbt \ ('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 - "\inv2 rt; bh lt = bh rt; inv1 rt\ \ - inv2 (delformLeft x lt k v rt) \ bh (delformLeft x lt k v rt) = bh lt \ (treec lt = B \ treec rt = B \ inv1 (delformLeft x lt k v rt) \ (treec lt \ B \ treec rt \ B) \ inv1l (delformLeft x lt k v rt))" - and "\inv2 rt; bh lt = bh rt; inv1 rt\ \ - inv2 (delformRight x lt k v rt) \ bh (delformRight x lt k v rt) = bh lt \ (treec lt = B \ treec rt = B \ inv1 (delformRight x lt k v rt) \ (treec lt \ B \ treec rt \ B) \ inv1l (delformRight x lt k v rt))" - and del_inv1_inv2: "inv2 (del x lt) \ (treec lt = R \ bh (del x lt) = bh lt \ inv1 (del x lt) - \ treec lt = B \ bh (del x lt) = bh lt - 1 \ inv1l (del x lt))" + "\inv2 rt; bheight lt = bheight rt; inv1 rt\ \ + inv2 (delformLeft x lt k v rt) \ bheight (delformLeft x lt k v rt) = bheight lt \ (color_of lt = B \ color_of rt = B \ inv1 (delformLeft x lt k v rt) \ (color_of lt \ B \ color_of rt \ B) \ inv1l (delformLeft x lt k v rt))" + and "\inv2 rt; bheight lt = bheight rt; inv1 rt\ \ + inv2 (delformRight x lt k v rt) \ bheight (delformRight x lt k v rt) = bheight lt \ (color_of lt = B \ color_of rt = B \ inv1 (delformRight x lt k v rt) \ (color_of lt \ B \ color_of rt \ B) \ inv1l (delformRight x lt k v rt))" + and del_inv1_inv2: "inv2 (del x lt) \ (color_of lt = R \ bheight (del x lt) = bheight lt \ inv1 (del x lt) + \ color_of lt = B \ bheight (del x lt) = bheight lt - 1 \ 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 \ 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 \ 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 \ 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 \ 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 \ treec Empty = B") simp+ + case ("6_1" y a y' ss) thus ?case by (cases "color_of a = B \ color_of Empty = B") simp+ qed auto lemma - delformLeft_tlt: "\tlt v lt; tlt v rt; k < v\ \ tlt v (delformLeft x lt k y rt)" - and delformRight_tlt: "\tlt v lt; tlt v rt; k < v\ \ tlt v (delformRight x lt k y rt)" - and del_tlt: "tlt v lt \ tlt v (del x lt)" + delformLeft_tree_less: "\tree_less v lt; tree_less v rt; k < v\ \ tree_less v (delformLeft x lt k y rt)" + and delformRight_tree_less: "\tree_less v lt; tree_less v rt; k < v\ \ tree_less v (delformRight x lt k y rt)" + and del_tree_less: "tree_less v lt \ 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: "\tgt v lt; tgt v rt; k > v\ \ tgt v (delformLeft x lt k y rt)" - and delformRight_tgt: "\tgt v lt; tgt v rt; k > v\ \ tgt v (delformRight x lt k y rt)" - and del_tgt: "tgt v lt \ tgt v (del x lt)" +lemma delformLeft_tree_greater: "\tree_greater v lt; tree_greater v rt; k > v\ \ tree_greater v (delformLeft x lt k y rt)" + and delformRight_tree_greater: "\tree_greater v lt; tree_greater v rt; k > v\ \ tree_greater v (delformRight x lt k y rt)" + and del_tree_greater: "tree_greater v lt \ 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 "\st lt; st rt; tlt k lt; tgt k rt\ \ st (delformLeft x lt k y rt)" - and "\st lt; st rt; tlt k lt; tgt k rt\ \ st (delformRight x lt k y rt)" - and del_st: "st lt \ st (del x lt)" +lemma "\sorted lt; sorted rt; tree_less k lt; tree_greater k rt\ \ sorted (delformLeft x lt k y rt)" + and "\sorted lt; sorted rt; tree_less k lt; tree_greater k rt\ \ sorted (delformRight x lt k y rt)" + and del_sorted: "sorted lt \ 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 "\st lt; st rt; tlt kt lt; tgt kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bh lt = bh rt; x < kt\ \ pin_tree k v (delformLeft x lt kt y rt) = (False \ (x \ k \ pin_tree k v (Tr c lt kt y rt)))" - and "\st lt; st rt; tlt kt lt; tgt kt rt; inv1 lt; inv1 rt; inv2 lt; inv2 rt; bh lt = bh rt; x > kt\ \ pin_tree k v (delformRight x lt kt y rt) = (False \ (x \ k \ pin_tree k v (Tr c lt kt y rt)))" - and del_pit: "\st t; inv1 t; inv2 t\ \ pin_tree k v (del x t) = (False \ (x \ k \ pin_tree k v t))" +lemma "\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\ \ entry_in_tree k v (delformLeft x lt kt y rt) = (False \ (x \ k \ entry_in_tree k v (Branch c lt kt y rt)))" + and "\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\ \ entry_in_tree k v (delformRight x lt kt y rt) = (False \ (x \ k \ entry_in_tree k v (Branch c lt kt y rt)))" + and del_pit: "\sorted t; inv1 t; inv2 t\ \ entry_in_tree k v (del x t) = (False \ (x \ k \ 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 \ xx < yy \ 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) \ k = yy" by simp - hence "\ pin_tree k v aa" "\ 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) \ k = yy" by simp + hence "\ entry_in_tree k v aa" "\ 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 \ inv1 mt" by simp - hence "inv2 (del xx mt) \ (treec mt = R \ bh (del xx mt) = bh mt \ inv1 (del xx mt) \ treec mt = B \ bh (del xx mt) = bh mt - 1 \ 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 \ xx \ k \ pin_tree k v mt \ (k = yy \ v = ss) \ pin_tree k v bb)" by (simp add: balleft_pit) + hence "inv2 (del xx mt) \ (color_of mt = R \ bheight (del xx mt) = bheight mt \ inv1 (del xx mt) \ color_of mt = B \ bheight (del xx mt) = bheight mt - 1 \ 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 \ xx \ k \ entry_in_tree k v mt \ (k = yy \ v = ss) \ 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 \ 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 \ 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 \ k < yy" by simp - hence "tgt k bb" by (blast dest: tgt_trans) + with "4_1" have "tree_greater yy bb \ 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 \ 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 \ 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 \ inv1 mt" by simp - hence "inv2 (del xx mt) \ (treec mt = R \ bh (del xx mt) = bh mt \ inv1 (del xx mt) \ treec mt = B \ bh (del xx mt) = bh mt - 1 \ 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 \ (k = yy \ v = ss) \ False \ xx \ k \ pin_tree k v mt)" by (simp add: balright_pit) + hence "inv2 (del xx mt) \ (color_of mt = R \ bheight (del xx mt) = bheight mt \ inv1 (del xx mt) \ color_of mt = B \ bheight (del xx mt) = bheight mt - 1 \ 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 \ (k = yy \ v = ss) \ False \ xx \ k \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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) \ (treec t = R \ bh (del k t) = bh t \ inv1 (del k t) \ treec t = B \ bh (del k t) = bh t - 1 \ inv1l (del k t))" by (rule del_inv1_inv2) - hence "inv2 (del k t) \ 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) \ (color_of t = R \ bheight (del k t) = bheight t \ inv1 (del k t) \ color_of t = B \ bheight (del k t) = bheight t - 1 \ inv1l (del k t))" by (rule del_inv1_inv2) + hence "inv2 (del k t) \ 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 \ k \ 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 \ k \ 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 \ 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\linorder \ 'b \ 'b \ 'b) \ ('a,'b) rbt \ ('a,'b) rbt \ ('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 \ st (unionwithkey f lt rt)" - by (induct rt arbitrary: lt) (auto simp: insertwk_st) -theorem unionwk_isrbt[simp]: "isrbt lt \ isrbt (unionwithkey f lt rt)" - by (induct rt arbitrary: lt) (simp add: insertwk_isrbt)+ +lemma unionwk_sorted: "sorted lt \ sorted (unionwithkey f lt rt)" + by (induct rt arbitrary: lt) (auto simp: insertwk_sorted) +theorem unionwk_is_rbt[simp]: "is_rbt lt \ is_rbt (unionwithkey f lt rt)" + by (induct rt arbitrary: lt) (simp add: insertwk_is_rbt)+ definition unionwith where "unionwith f = unionwithkey (\_. f)" -theorem unionw_isrbt: "isrbt lt \ isrbt (unionwith f lt rt)" unfolding unionwith_def by simp +theorem unionw_is_rbt: "is_rbt lt \ is_rbt (unionwith f lt rt)" unfolding unionwith_def by simp definition union where "union = unionwithkey (%_ _ rv. rv)" -theorem union_isrbt: "isrbt lt \ isrbt (union lt rt)" unfolding union_def by simp +theorem union_is_rbt: "is_rbt lt \ 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 |\ k" "k \| r" by auto + case (Branch c l k v r s) + hence sortedrl: "sorted r" "sorted l" "l |\ k" "k \| r" by auto - have meq: "map_of s(k \ v) ++ map_of l ++ map_of r = - map_of s ++ - (\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 \ v) ++ lookup l ++ lookup r = + lookup s ++ + (\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 |\ k` have "l |\ a" by (rule tlt_trans) + with `l |\ k` have "l |\ 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 \| r` have "a \| r" by (rule tgt_trans) + from this `k \| r` have "a \| 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 \ 'b \ 'b) \ ('a\linorder) \ ('a,'b) rbt \ ('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 \ None | Some y \ 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 \ None | Some y \ Some (f k y) + else lookup t x)" by (induct t arbitrary: x) (auto split:option.splits) definition adjust where "adjust f = adjustwithkey (\_. 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 \ None | Some y \ Some (f y) - else map_of t x)" + "lookup (adjust f k t) x = + (if x = k then case lookup t x of None \ None | Some y \ Some (f y) + else lookup t x)" unfolding adjust_def by simp subsection {* Map *} @@ -875,27 +890,27 @@ mapwithkey :: "('a::linorder \ 'b \ 'c) \ ('a,'b) rbt \ ('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 (\_. 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 \ 'b \ 'c \ 'c) \ ('a,'b) rbt \ 'c \ '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) \ RBT.map_of (Tr c t1 k v t2) = RBT.map_of t2 ++ [k\v] ++ RBT.map_of t1" +lemma lookup_entries_aux: "sorted (Branch c t1 k v t2) \ RBT.lookup (Branch c t1 k v t2) = RBT.lookup t2 ++ [k\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 \ 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 \ v] ++ RBT.lookup t1) x" - have DOM_T1: "!!k'. k'\dom (RBT.map_of t1) \ k>k'" + have DOM_T1: "!!k'. k'\dom (RBT.lookup t1) \ k>k'" proof - fix k' - from ST have "t1 |\ k" by simp - with tlt_prop have "\k'\keys t1. k>k'" by auto - moreover assume "k'\dom (RBT.map_of t1)" - ultimately show "k>k'" using RBT.mapof_keys ST by auto + from SORTED have "t1 |\ k" by simp + with tree_less_prop have "\k'\keys t1. k>k'" by auto + moreover assume "k'\dom (RBT.lookup t1)" + ultimately show "k>k'" using RBT.lookup_keys SORTED by auto qed - have DOM_T2: "!!k'. k'\dom (RBT.map_of t2) \ kdom (RBT.lookup t2) \ k| t2" by simp - with tgt_prop have "\k'\keys t2. kdom (RBT.map_of t2)" - ultimately show "k| t2" by simp + with tree_greater_prop have "\k'\keys t2. kdom (RBT.lookup t2)" + ultimately show "kdom [k\v]" by simp - moreover have "x\dom (RBT.map_of t2)" proof - assume "x\dom (RBT.map_of t2)" + moreover have "x\dom (RBT.lookup t2)" proof + assume "x\dom (RBT.lookup t2)" with DOM_T2 have "k v] x" by simp - moreover have "x\dom (RBT.map_of t1)" proof - assume "x\dom (RBT.map_of t1)" + hence "RBT.lookup (Branch c t1 k v t2) x = [k \ v] x" by simp + moreover have "x\dom (RBT.lookup t1)" proof + assume "x\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\dom [k\v]" by simp - moreover have "x\dom (RBT.map_of t1)" proof - assume "x\dom (RBT.map_of t1)" + moreover have "x\dom (RBT.lookup t1)" proof + assume "x\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 \ Map.map_of (alist_of t) = map_of t" +lemma map_of_entries: + shows "sorted t \ 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 \ 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 \ 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 (\x (k,v). f k v x) x (alist_of t)" +lemma fold_entries_fold: + "foldwithkey f t x = foldl (\x (k,v). f k v x) x (entries t)" by (induct t arbitrary: x) auto -lemma alist_pit[simp]: "(k, v) \ set (alist_of t) = pin_tree k v t" +lemma entries_pit[simp]: "(k, v) \ set (entries t) = entry_in_tree k v t" by (induct t) auto -lemma sorted_alist: - "st t \ sorted (List.map fst (alist_of t))" +lemma sorted_entries: + "sorted t \ 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 \ distinct (List.map fst (alist_of t))" +lemma distinct_entries: + "sorted t \ 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} *} diff -r e27550a842b9 -r f5ec817df77f src/HOL/Library/Transitive_Closure_Table.thy --- 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 diff -r e27550a842b9 -r f5ec817df77f src/HOL/Map.thy --- 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 "\" 0) +type_notation (xsymbols) + "~=>" (infixr "\" 0) abbreviation empty :: "'a ~=> 'b" where diff -r e27550a842b9 -r f5ec817df77f src/HOL/MicroJava/J/Decl.thy --- 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 \ ty" - "sig" <= (type) "mname \ ty list" - "mdecl c" <= (type) "sig \ ty \ c" - "class c" <= (type) "cname \ fdecl list \ (c mdecl) list" - "cdecl c" <= (type) "cname \ (c class)" - "prog c" <= (type) "(c cdecl) list" + (type) "fdecl" <= (type) "vname \ ty" + (type) "sig" <= (type) "mname \ ty list" + (type) "'c mdecl" <= (type) "sig \ ty \ 'c" + (type) "'c class" <= (type) "cname \ fdecl list \ ('c mdecl) list" + (type) "'c cdecl" <= (type) "cname \ ('c class)" + (type) "'c prog" <= (type) "('c cdecl) list" definition "class" :: "'c prog => (cname \ 'c class)" where diff -r e27550a842b9 -r f5ec817df77f src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- 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 \ {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. *} diff -r e27550a842b9 -r f5ec817df77f src/HOL/Multivariate_Analysis/Derivative.thy --- 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 "\(f (x + c *\<^sub>R basis j) - f x - D *v (c *\<^sub>R basis j)) $ k\ \ \D $ k $ j\ / 2 * \c\" by simp hence "\f (x + c *\<^sub>R basis j) $ k - f x $ k - c * D $ k $ j\ \ \D $ k $ j\ / 2 * \c\" 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 \ ball x e" "x - d *\<^sub>R basis j \ 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 \ (f x)$k \ (f (x + d *\<^sub>R basis j))$k \ (f x)$k) \ @@ -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 \ b = inner a b" unfolding inner_vector_def dot_def by auto - lemma mvt_general: fixes f::"real\real^'n" assumes "ax\{a<..x\{a<.. norm(f'(x) (b - a))" proof- have "\x\{a<.. (f b - f a) \ f) b - (op \ (f b - f a) \ f) a = (f b - f a) \ 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 "\ = (f b - f a) \ (f b - f a)" unfolding norm_pow_2 .. - also have "\ = (f b - f a) \ f' x (b - a)" using x by auto + also have "\ = (f b - f a) \ (f b - f a)" unfolding power2_norm_eq_inner .. + also have "\ = (f b - f a) \ f' x (b - a)" using x unfolding inner_simps by auto also have "\ \ 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 "\ \ 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 \ real" shows "onorm (\x. vec1 (f (dest_vec1 x))) = onorm f" proof- have "\x::real^1. norm x = 1 \ x\{vec1 -1, vec1 (1::real)}" unfolding forall_vec1 by(auto simp add:Cart_eq) diff -r e27550a842b9 -r f5ec817df77f src/HOL/Multivariate_Analysis/Determinants.thy --- 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) \ transpose Q ** Q = mat 1 \ 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 \ y0 = x0' \ y0' + y0' \ x0' - y0 \ 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 = "\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" diff -r e27550a842b9 -r f5ec817df77f src/HOL/Multivariate_Analysis/Euclidean_Space.thy --- 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 = (\ r x. (\ 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 \ 'a set) = Suc 0" begin - definition vector_scaleR_def: "scaleR = (\ r x. (\ 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 "\P. (\i\UNIV. P i) \ P a" unfolding * by auto hence all:"\P. (\i. P i) \ P a" by auto + fix x y z::"'a^'b::cart_one" note * = vector_le_def vector_less_def all Cart_eq + show "x\x" "(x < y) = (x \ y \ \ y \ x)" "x\y \ y\x" unfolding * by(auto simp only:field_simps) + { assume "x\y" "y\z" thus "x\z" unfolding * by(auto simp only:field_simps) } + { assume "x\y" "y\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 \ 'a ^ 'n \ 'a ^ 'n" (infixl "*s" 70) @@ -123,25 +148,11 @@ definition "vec x = (\ i. x)" -text{* Dot products. *} - -definition dot :: "'a::{comm_monoid_add, times} ^ 'n \ 'a ^ 'n \ 'a" (infix "\" 70) where - "x \ y = setsum (\i. x$i * y$i) UNIV" - -lemma dot_1[simp]: "(x::'a::{comm_monoid_add, times}^1) \ y = (x$1) * (y$1)" - by (simp add: dot_def setsum_1) - -lemma dot_2[simp]: "(x::'a::{comm_monoid_add, times}^2) \ 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) \ 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 "\" 70) where "x \ y \ 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) \ y = y \ x" - by (vector mult_commute) -lemma dot_ladd: "((x::'a::ring ^ 'n) + y) \ z = (x \ z) + (y \ z)" - by (vector ring_simps) -lemma dot_radd: "x \ (y + (z::'a::ring ^ 'n)) = (x \ y) + (x \ z)" - by (vector ring_simps) -lemma dot_lsub: "((x::'a::ring ^ 'n) - y) \ z = (x \ z) - (y \ z)" - by (vector ring_simps) -lemma dot_rsub: "(x::'a::ring ^ 'n) \ (y - z) = (x \ y) - (x \ z)" - by (vector ring_simps) -lemma dot_lmult: "(c *s x) \ y = (c::'a::ring) * (x \ y)" by (vector ring_simps) -lemma dot_rmult: "x \ (c *s y) = (c::'a::comm_ring) * (x \ y)" by (vector ring_simps) -lemma dot_lneg: "(-x) \ (y::'a::ring ^ 'n) = -(x \ y)" by vector -lemma dot_rneg: "(x::'a::ring ^ 'n) \ (-y) = -(x \ y)" by vector -lemma dot_lzero[simp]: "0 \ x = (0::'a::{comm_monoid_add, mult_zero})" by vector -lemma dot_rzero[simp]: "x \ 0 = (0::'a::{comm_monoid_add, mult_zero})" by vector -lemma dot_pos_le[simp]: "(0::'a\linordered_ring_strict) <= x \ x" - by (simp add: dot_def setsum_nonneg) - lemma setsum_squares_eq_0_iff: assumes fS: "finite F" and fp: "\x \ F. f x \ (0 ::'a::ordered_ab_group_add)" shows "setsum f F = 0 \ (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 \ x = 0 \ (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 \ x) \ (x::'a::{linordered_ring_strict,ring_no_zero_divisors} ^ 'n) \ 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) = (\ 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) \ (x \ 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 \ x)" - by (simp add: norm_vector_def setL2_def dot_def power2_eq_square) -lemma norm_pow_2: "norm x ^ 2 = x \ x" - by (simp add: real_vector_norm_def) +lemma norm_eq_0_dot: "(norm x = 0) \ (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) \ a = (0::'a::idom) \ x = 0" by vector @@ -1011,34 +991,17 @@ by (metis vector_mul_lcancel) lemma vector_mul_rcancel_imp: "x \ 0 \ (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 \ 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 \ 0" "norm y \ 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 \ y) \ 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\y \ (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 "\x \ y\ \ norm x * norm y" + shows "\inner x y\ \ 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: "\norm (x::real ^ 'n) - norm y\ <= norm(x - y)" by (rule norm_triangle_ineq3) lemma norm_le: "norm(x::real ^ 'n) <= norm(y) \ x \ x <= y \ y" - by (simp add: real_vector_norm_def) + by (simp add: norm_eq_sqrt_inner) lemma norm_lt: "norm(x::real ^ 'n) < norm(y) \ x \ x < y \ y" - by (simp add: real_vector_norm_def) -lemma norm_eq: "norm(x::real ^ 'n) = norm y \ x \ x = y \ 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) \ x \ x = y \ y" + apply(subst order_eq_iff) unfolding norm_le by auto lemma norm_eq_1: "norm(x::real ^ 'n) = 1 \ x \ 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 \ 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 \ 0 <= a \ x \ 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: "\x\ \ \y\ \ (x::real)^2 \ 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 \ 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 \ 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 \"} products. *} @@ -1120,14 +1085,12 @@ assume "?lhs" then show ?rhs by simp next assume ?rhs - then have "x \ x - x \ y = 0 \ x \ y - y\ y = 0" by simp - hence "x \ (x - y) = 0 \ y \ (x - y) = 0" - by (simp add: dot_rsub dot_lsub dot_sym) - then have "(x - y) \ (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 \ x - x \ y = 0 \ x \ y - y \ y = 0" by simp + hence "x \ (x - y) = 0 \ y \ (x - y) = 0" by (simp add: inner_simps inner_commute) + then have "(x - y) \ (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 \ setsum f S \ (y::'a::{comm_ring}^'n) = setsum (\x. f x \ y) S " - by (induct rule: finite_induct, auto simp add: dot_lzero dot_ladd dot_radd) - -lemma dot_rsum: "finite S \ (y::'a::{comm_ring}^'n) \ setsum f S = setsum (\x. y \ f x) S " - by (induct rule: finite_induct, auto simp add: dot_rzero dot_radd) +lemma dot_lsum: "finite S \ setsum f S \ (y::'a::{real_inner}^'n) = setsum (\x. f x \ y) S " + apply(induct rule: finite_induct) by(auto simp add: inner_simps) + +lemma dot_rsum: "finite S \ (y::'a::{real_inner}^'n) \ setsum f S = setsum (\x. y \ f x) S " + apply(induct rule: finite_induct) by(auto simp add: inner_simps) subsection{* Basis vectors in coordinate directions. *} - definition "basis k = (\ 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" "\k. 1::real"] - apply auto - done + using setsum_delta[of "UNIV :: 'n set" "k" "\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 \ x = x$i" "x \ (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 \ x = x$i" "x \ (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 \ (0:: 'a::semiring_1 ^'n)" by (simp add: basis_eq_0) -lemma vector_eq_ldot: "(\x. x \ y = x \ z) \ y = (z::'a::semiring_1^'n)" +lemma vector_eq_ldot: "(\x. x \ y = x \ z) \ 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: "(\z. x \ z = y \ z) \ x = (y::'a::semiring_1^'n)" +lemma vector_eq_rdot: "(\z. x \ z = y \ z) \ 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 \ (x \ y = 0)" lemma orthogonal_basis: - shows "orthogonal (basis i :: 'a^'n) x \ 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 \ 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) \ i \ j" + shows "orthogonal (basis i :: real^'n) (basis j) \ i \ 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 \ orthogonal a y ==> orthogonal a (x + y)" "orthogonal a x \ 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 \ orthogonal y a ==> orthogonal (x + y) a" "orthogonal x a \ 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 \ 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 \ orthogonal y x" + by (simp add: orthogonal_def inner_commute) subsection{* Explicit vector construction from lists. *} @@ -1969,7 +1927,7 @@ lemma choice_iff: "(\x. \y. P x y) \ (\f. \x. P x (f x))" by metis lemma adjoint_works_lemma: - fixes f:: "'a::ring_1 ^'n \ 'a ^'m" + fixes f:: "real ^'n \ real ^'m" assumes lf: "linear f" shows "\x y. f x \ y = x \ 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 = "(\ i. (f (basis i) \ y)) :: 'a ^ 'n" + {fix y:: "real ^ 'm" + let ?w = "(\ i. (f (basis i) \ y)) :: real ^ 'n" {fix x have "f x \ y = f (setsum (\i. (x$i) *s basis i) ?N) \ y" by (simp only: basis_expansion) @@ -1987,7 +1945,7 @@ by (simp add: linear_cmul[OF lf]) finally have "f x \ y = x \ ?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 \ 'a ^'m" + fixes f:: "real ^'n \ real ^'m" assumes lf: "linear f" shows "x \ adjoint f y = f x \ y" using adjoint_works_lemma[OF lf] by metis - lemma adjoint_linear: - fixes f :: "'a::comm_ring_1 ^'n \ 'a ^'m" + fixes f:: "real ^'n \ 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 \ 'a ^'m" + fixes f:: "real ^'n \ real ^'m" assumes lf: "linear f" shows "x \ adjoint f y = f x \ y" and "adjoint f y \ x = y \ 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 \ 'a ^'m" + fixes f:: "real ^'n \ 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 \ 'a ^'m" + fixes f:: "real ^'n \ real ^'m" assumes lf: "linear f" and u: "\x y. f' x \ y = x \ 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) \ x" - by (simp add: matrix_vector_mult_def dot_def) - -lemma dot_lmul_matrix: "((x::'a::comm_semiring_1 ^_) v* A) \ y = x \ (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) \ x" + by (simp add: matrix_vector_mult_def inner_vector_def) + +lemma dot_lmul_matrix: "((x::real ^_) v* A) \ y = x \ (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 = (\ i. A$i \ 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 (\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 (\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(\x. (A::'a::comm_ring_1^'n^'m) *v x) = (\x. transpose A *v x)" +lemma adjoint_matrix: "adjoint(\x. (A::real^'n^'m) *v x) = (\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 \ 'a ^'m)" +lemma matrix_adjoint: assumes lf: "linear (f :: real^'n \ 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 \ 'a^1)" +lemma linear_to_scalars: assumes lf: "linear (f::real ^'n \ real^1)" shows "f = (\x. vec1(row 1 (matrix f) \ 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 \ 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 \ fstcart x \ pastecart (fstcart x) (sndcart x) \ 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 \ sndcart x \ pastecart (fstcart x) (sndcart x) \ 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)) \ (pastecart y1 y2) = x1 \ y1 + x2 \ y2" - by (simp add: dot_def setsum_UNIV_sum pastecart_def) +lemma dot_pastecart: "(pastecart (x1::real^'n) (x2::real^'m)) \ (pastecart y1 y2) = x1 \ y1 + x2 \ 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 \ s" have t: "t \ (insert b (insert a (t -{b})))" using b by auto from b(1) have "b \ span t" by (simp add: span_superset) - have bs: "b \ span (insert a (t - {b}))" - by (metis in_span_delete a sp mem_def subset_eq) + have bs: "b \ span (insert a (t - {b}))" apply(rule in_span_delete) + using a sp unfolding subset_eq by auto from xs sp have "x \ span t" by blast with span_mono[OF t] have x: "x \ span (insert b (insert a (t - {b})))" .. @@ -3842,11 +3800,8 @@ (* FIXME : Move to some general theory ?*) definition "pairwise R S \ (\x \ S. \y\ S. x\y \ R x y)" -lemma vector_sub_project_orthogonal: "(b::'a::linordered_field^'n) \ (x - ((b \ x) / (b\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) \ (x - ((b \ x) / (b \ 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 `\C. finite C \ card C \ card B \ span C = span B \ pairwise orthogonal C` obtain C where C: "finite C" "card C \ card B" "span C = span B" "pairwise orthogonal C" by blast - let ?a = "a - setsum (\x. (x\a / (x\x)) *s x) C" + let ?a = "a - setsum (\x. (x \ a / (x \ 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 \ 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 \ S \ span T \ T \ 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 (\b. (a\b / (b\b)) *s b) B" - have "setsum (\b. (a\b / (b\b)) *s b) B \ span S" + let ?a = "a - setsum (\b. (a \ b / (b \ b)) *s b) B" + have "setsum (\b. (a \ b / (b \ b)) *s b) B \ span S" unfolding sSB apply (rule span_setsum[OF fB(1)]) apply clarsimp @@ -3972,20 +3927,20 @@ with a have a0:"?a \ 0" by auto have "\x\span B. ?a \ x = 0" proof(rule span_induct') - show "subspace (\x. ?a \ x = 0)" - by (auto simp add: subspace_def mem_def dot_radd dot_rmult) - next + show "subspace (\x. ?a \ x = 0)" by (auto simp add: subspace_def mem_def inner_simps smult_conv_scaleR) + +next {fix x assume x: "x \ B" from x have B': "B = insert x (B - {x})" by blast have fth: "finite (B - {x})" using fB by simp have "?a \ 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 "\x \ B. ?a \ 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) \ 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) \ 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 \ 0" by (simp add: zero_le_mult_iff real_sqrt_ge_0_iff infnorm_pos_le) - have th1: "x\x \ (sqrt (real ?d) * infnorm x)^2" + have th1: "x \ x \ (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 \ 0" and y: "y \ 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 \ (norm y * (norm y * norm x * norm x - norm x * (x \ y)) - norm x * (norm y * (y \ 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 "\ \ (2 * norm x * norm y * (norm x * norm y - x \ y) = 0)" using x y - by (simp add: ring_simps dot_sym) + by (simp add: ring_simps inner_commute) also have "\ \ ?lhs" using x y apply simp by metis @@ -4969,8 +4920,7 @@ unfolding norm_minus_cancel norm_mul by blast also have "\ \ ?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 "\ \ 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 diff -r e27550a842b9 -r f5ec817df77f src/HOL/Multivariate_Analysis/Integration.thy --- 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 \ 'a::real_normed_vector" assumes "dest_vec1 a \ dest_vec1 b" "p tagged_division_of {a..b}" shows "setsum (\(x,k). f(interval_upperbound k) - f(interval_lowerbound k)) p = f b - f a" diff -r e27550a842b9 -r f5ec817df77f src/HOL/Mutabelle/mutabelle_extra.ML --- 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; diff -r e27550a842b9 -r f5ec817df77f src/HOL/NanoJava/AxSem.thy --- 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 \ stmt \ assn" etriple = "assn \ expr \ vassn" translations - "assn" \ (type)"state => bool" - "vassn" \ (type)"val => assn" - "triple" \ (type)"assn \ stmt \ assn" - "etriple" \ (type)"assn \ expr \ vassn" + (type) "assn" \ (type) "state => bool" + (type) "vassn" \ (type) "val => assn" + (type) "triple" \ (type) "assn \ stmt \ assn" + (type) "etriple" \ (type) "assn \ expr \ vassn" subsection "Hoare Logic Rules" diff -r e27550a842b9 -r f5ec817df77f src/HOL/NanoJava/Decl.thy --- 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" \ (type)"fname \ ty" - "mdecl" \ (type)"mname \ ty \ ty \ stmt" - "class" \ (type)"cname \ fdecl list \ mdecl list" - "cdecl" \ (type)"cname \ class" - "prog " \ (type)"cdecl list" + (type) "fdecl" \ (type) "fname \ ty" + (type) "mdecl" \ (type) "mname \ ty \ ty \ stmt" + (type) "class" \ (type) "cname \ fdecl list \ mdecl list" + (type) "cdecl" \ (type) "cname \ class" + (type) "prog " \ (type) "cdecl list" consts diff -r e27550a842b9 -r f5ec817df77f src/HOL/NanoJava/State.thy --- 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 \ fields" translations - - "fields" \ (type)"fname => val option" - "obj" \ (type)"cname \ fields" + (type) "fields" \ (type) "fname => val option" + (type) "obj" \ (type) "cname \ fields" definition init_vars :: "('a \ 'b) => ('a \ val)" where "init_vars m == Option.map (\T. Null) o m" @@ -40,10 +39,9 @@ locals :: locals translations - - "heap" \ (type)"loc => obj option" - "locals" \ (type)"vname => val option" - "state" \ (type)"(|heap :: heap, locals :: locals|)" + (type) "heap" \ (type) "loc => obj option" + (type) "locals" \ (type) "vname => val option" + (type) "state" \ (type) "(|heap :: heap, locals :: locals|)" definition del_locs :: "state => state" where "del_locs s \ s (| locals := empty |)" diff -r e27550a842b9 -r f5ec817df77f src/HOL/Old_Number_Theory/Euler.thy --- 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 \ b | b \ a)" by auto +lemma d22set_induct_old: "(\a::int. 1 < a \ P (a - 1) \ P a) \ P x" +using d22set.induct by blast + lemma SRStar_d22set_prop: "2 < p \ (SRStar p) = {1} \ (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) diff -r e27550a842b9 -r f5ec817df77f src/HOL/Product_Type.thy --- 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" ("(_ \/ _)" [21, 20] 20) -syntax (HTML output) - "*" :: "[type, type] => type" ("(_ \/ _)" [21, 20] 20) +type_notation (xsymbols) + "*" ("(_ \/ _)" [21, 20] 20) +type_notation (HTML output) + "*" ("(_ \/ _)" [21, 20] 20) consts Pair :: "'a \ 'b \ 'a \ 'b" diff -r e27550a842b9 -r f5ec817df77f src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- 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; diff -r e27550a842b9 -r f5ec817df77f src/HOL/Tools/numeral_syntax.ML --- 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 diff -r e27550a842b9 -r f5ec817df77f src/HOL/Tools/record.ML --- 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 = diff -r e27550a842b9 -r f5ec817df77f src/HOL/Tools/typedef.ML --- 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); diff -r e27550a842b9 -r f5ec817df77f src/HOL/Typerep.thy --- 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) diff -r e27550a842b9 -r f5ec817df77f src/HOL/UNITY/Union.thy --- 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 & (\G. Acts G \ UNION X Acts --> G \ X)" +notation (xsymbols) + SKIP ("\") and + Join (infixl "\" 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\ _./ _)" 10) + "_JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\ _\_./ _)" 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" ("\") - Join :: "['a program, 'a program] => 'a program" (infixl "\" 65) - "_JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\ _./ _)" 10) - "_JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\ _\_./ _)" 10) - subsection{*SKIP*} diff -r e27550a842b9 -r f5ec817df77f src/HOL/ex/Numeral.thy --- 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 diff -r e27550a842b9 -r f5ec817df77f src/HOL/ex/Predicate_Compile_Quickcheck.thy --- 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 diff -r e27550a842b9 -r f5ec817df77f src/HOLCF/Cfun.thy diff -r e27550a842b9 -r f5ec817df77f src/HOLCF/One.thy --- 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" diff -r e27550a842b9 -r f5ec817df77f src/HOLCF/Representable.thy --- 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" \ (type) "udom alg_defl" +translations (type) "TypeRep" \ (type) "udom alg_defl" definition Rep_of :: "'a::rep itself \ TypeRep" @@ -60,7 +60,7 @@ (emb oo (approx i :: 'a \ 'a) oo prj)))" syntax "_REP" :: "type \ TypeRep" ("(1REP/(1'(_')))") -translations "REP(t)" \ "CONST Rep_of TYPE(t)" +translations "REP('t)" \ "CONST Rep_of TYPE('t)" lemma cast_REP: "cast\REP('a::rep) = (emb::'a \ udom) oo (prj::udom \ 'a)" diff -r e27550a842b9 -r f5ec817df77f src/HOLCF/Sprod.thy --- 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" ("(_ \/ _)" [21,20] 20) -syntax (HTML output) - sprod :: "[type, type] => type" ("(_ \/ _)" [21,20] 20) +type_notation (xsymbols) + sprod ("(_ \/ _)" [21,20] 20) +type_notation (HTML output) + sprod ("(_ \/ _)" [21,20] 20) lemma spair_lemma: "(strictify\(\ b. a)\b, strictify\(\ a. b)\a) \ Sprod" diff -r e27550a842b9 -r f5ec817df77f src/HOLCF/Ssum.thy --- 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" ("(_ \/ _)" [21, 20] 20) -syntax (HTML output) - ssum :: "[type, type] => type" ("(_ \/ _)" [21, 20] 20) +type_notation (xsymbols) + ssum ("(_ \/ _)" [21, 20] 20) +type_notation (HTML output) + ssum ("(_ \/ _)" [21, 20] 20) + subsection {* Definitions of constructors *} diff -r e27550a842b9 -r f5ec817df77f src/HOLCF/Tr.thy --- 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 diff -r e27550a842b9 -r f5ec817df77f src/HOLCF/Up.thy --- 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 \ type" ("(_\<^sub>\)" [1000] 999) +type_notation (xsymbols) + u ("(_\<^sub>\)" [1000] 999) primrec Ifup :: "('a \ 'b::pcpo) \ 'a u \ 'b" where "Ifup f Ibottom = \" diff -r e27550a842b9 -r f5ec817df77f src/HOLCF/ex/Strict_Fun.thy --- 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 \ 'b. f\\ = \}" by simp_all -syntax (xsymbols) - sfun :: "type \ type \ type" (infixr "\!" 0) +type_notation (xsymbols) + sfun (infixr "\!" 0) text {* TODO: Define nice syntax for abstraction, application. *} diff -r e27550a842b9 -r f5ec817df77f src/HOLCF/holcf_logic.ML --- 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; diff -r e27550a842b9 -r f5ec817df77f src/Pure/General/name_space.ML --- 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 *) diff -r e27550a842b9 -r f5ec817df77f src/Pure/Isar/local_syntax.ML --- 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; diff -r e27550a842b9 -r f5ec817df77f src/Pure/Isar/proof_context.ML --- 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; + diff -r e27550a842b9 -r f5ec817df77f src/Pure/ML/ml_antiquote.ML --- 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 *) diff -r e27550a842b9 -r f5ec817df77f src/Pure/Proof/extraction.ML --- 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 **) diff -r e27550a842b9 -r f5ec817df77f src/Pure/Syntax/lexicon.ML --- 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 diff -r e27550a842b9 -r f5ec817df77f src/Pure/Syntax/printer.ML --- 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; diff -r e27550a842b9 -r f5ec817df77f src/Pure/Syntax/syn_ext.ML --- 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; diff -r e27550a842b9 -r f5ec817df77f src/Pure/Syntax/syn_trans.ML --- 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); diff -r e27550a842b9 -r f5ec817df77f src/Pure/Syntax/syntax.ML --- 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; diff -r e27550a842b9 -r f5ec817df77f src/Pure/Syntax/type_ext.ML --- 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')]) [] ([], []); diff -r e27550a842b9 -r f5ec817df77f src/Pure/pure_thy.ML --- 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 ("(_/ \\ _)", [1, 0], 0)), - ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\ _)", [0, 0], 0)), - ("_ofsort", typ "tid => sort => type", Mixfix ("_\\_", [1000, 0], 1000)), - ("_constrain", typ "logic => type => logic", Mixfix ("_\\_", [4, 0], 3)), - ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\\_", [4, 0], 3)), - ("_idtyp", typ "id => type => idt", Mixfix ("_\\_", [], 0)), - ("_idtypdummy", typ "type => idt", Mixfix ("'_()\\_", [], 0)), - ("_type_constraint_", typ "'a", NoSyn), - ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\_./ _)", [0, 3], 3)), - (const "==", typ "'a => 'a => prop", Infixr ("\\", 2)), - (const "all_binder", typ "idts => prop => prop", Mixfix ("(3\\_./ _)", [0, 0], 0)), - (const "==>", typ "prop => prop => prop", Infixr ("\\", 1)), - ("_DDDOT", typ "aprop", Delimfix "\\"), - ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\_\\)/ \\ _)", [0, 1], 1)), - ("_DDDOT", typ "logic", Delimfix "\\")] + [(tycon "fun", typ "type => type => type", Mixfix ("(_/ \\ _)", [1, 0], 0)), + ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\ _)", [0, 0], 0)), + ("_ofsort", typ "tid => sort => type", Mixfix ("_\\_", [1000, 0], 1000)), + ("_constrain", typ "logic => type => logic", Mixfix ("_\\_", [4, 0], 3)), + ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\\_", [4, 0], 3)), + ("_idtyp", typ "id => type => idt", Mixfix ("_\\_", [], 0)), + ("_idtypdummy", typ "type => idt", Mixfix ("'_()\\_", [], 0)), + ("_type_constraint_", typ "'a", NoSyn), + ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\_./ _)", [0, 3], 3)), + (const "==", typ "'a => 'a => prop", Infixr ("\\", 2)), + (const "all_binder", typ "idts => prop => prop", Mixfix ("(3\\_./ _)", [0, 0], 0)), + (const "==>", typ "prop => prop => prop", Infixr ("\\", 1)), + ("_DDDOT", typ "aprop", Delimfix "\\"), + ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\_\\)/ \\ _)", [0, 1], 1)), + ("_DDDOT", typ "logic", Delimfix "\\")] #> Sign.add_modesyntax_i ("", false) [(const "prop", typ "prop => prop", Mixfix ("_", [0], 0))] #> Sign.add_modesyntax_i ("HTML", false) diff -r e27550a842b9 -r f5ec817df77f src/Pure/sign.ML --- 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); diff -r e27550a842b9 -r f5ec817df77f src/Sequents/Sequents.thy --- 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 diff -r e27550a842b9 -r f5ec817df77f src/ZF/Induct/Comb.thy --- 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 \ comb", "q \ comb") (infixl "@@" 90) +notation (xsymbols) + app (infixl "\" 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 == \ contract^*" -syntax (xsymbols) - "comb.app" :: "[i, i] => i" (infixl "\" 90) - inductive domains "contract" \ "comb \ comb" intros diff -r e27550a842b9 -r f5ec817df77f src/ZF/List_ZF.thy --- 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])" diff -r e27550a842b9 -r f5ec817df77f src/ZF/UNITY/Union.thy --- 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\program & SKIP \ X & (\G \ program. Acts(G) \ (\F \ X. Acts(F)) --> G \ X)" +notation (xsymbols) + SKIP ("\") and + Join (infixl "\" 65) + syntax "_JOIN1" :: "[pttrns, i] => i" ("(3JN _./ _)" 10) "_JOIN" :: "[pttrn, i, i] => i" ("(3JN _:_./ _)" 10) +syntax (xsymbols) + "_JOIN1" :: "[pttrns, i] => i" ("(3\ _./ _)" 10) + "_JOIN" :: "[pttrn, i, i] => i" ("(3\ _ \ _./ _)" 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 ("\") and - Join (infixl "\" 65) - -syntax (xsymbols) - "_JOIN1" :: "[pttrns, i] => i" ("(3\ _./ _)" 10) - "_JOIN" :: "[pttrn, i, i] => i" ("(3\ _ \ _./ _)" 10) - subsection{*SKIP*}