merged
authorhuffman
Wed Sep 07 19:24:28 2011 -0700 (2011-09-07)
changeset 448261120cba9bce4
parent 44825 353ddca2e4c0
parent 44820 7798deb6f8fa
child 44827 4d1384a1fc82
child 44839 d19c677eb812
merged
NEWS
     1.1 --- a/ANNOUNCE	Wed Sep 07 17:41:29 2011 -0700
     1.2 +++ b/ANNOUNCE	Wed Sep 07 19:24:28 2011 -0700
     1.3 @@ -1,34 +1,15 @@
     1.4 -Subject: Announcing Isabelle2011
     1.5 +Subject: Announcing Isabelle2011-1
     1.6  To: isabelle-users@cl.cam.ac.uk
     1.7  
     1.8 -Isabelle2011 is now available.
     1.9 -
    1.10 -This version significantly improves upon Isabelle2009-2, see the NEWS
    1.11 -file in the distribution for more details.  Some notable changes are:
    1.12 -
    1.13 -* Experimental Prover IDE based on Isabelle/Scala and jEdit.
    1.14 -
    1.15 -* Coercive subtyping (configured in HOL/Complex_Main).
    1.16 -
    1.17 -* HOL code generation: Scala as another target language.
    1.18 -
    1.19 -* HOL: partial_function definitions.
    1.20 +Isabelle2011-1 is now available.
    1.21  
    1.22 -* HOL: various tool enhancements, including Quickcheck, Nitpick,
    1.23 -  Sledgehammer, SMT integration.
    1.24 -
    1.25 -* HOL: various additions to theory library, including HOL-Algebra,
    1.26 -  Imperative_HOL, Multivariate_Analysis, Probability.
    1.27 +This version improves upon Isabelle2011, see the NEWS file in the
    1.28 +distribution for more details.  Some important changes are:
    1.29  
    1.30 -* HOLCF: reorganization of library and related tools.
    1.31 -
    1.32 -* HOL/SPARK: interactive proof environment for verification conditions
    1.33 -  generated by the SPARK Ada program verifier.
    1.34 -
    1.35 -* Improved Isabelle/Isar implementation manual (covering Isabelle/ML).
    1.36 +* FIXME
    1.37  
    1.38  
    1.39 -You may get Isabelle2011 from the following mirror sites:
    1.40 +You may get Isabelle2011-1 from the following mirror sites:
    1.41  
    1.42    Cambridge (UK)       http://www.cl.cam.ac.uk/research/hvg/Isabelle/
    1.43    Munich (Germany)     http://isabelle.in.tum.de/
     2.1 --- a/Admin/CHECKLIST	Wed Sep 07 17:41:29 2011 -0700
     2.2 +++ b/Admin/CHECKLIST	Wed Sep 07 19:24:28 2011 -0700
     2.3 @@ -3,9 +3,7 @@
     2.4  
     2.5  - test polyml-5.4.0, polyml-5.3.0, polyml-5.2.1, smlnj;
     2.6  
     2.7 -- test Proof General 4.1, 4.0, 3.7.1.1;
     2.8 -
     2.9 -- test Scala wrapper;
    2.10 +- test Proof General 4.1, 3.7.1.1;
    2.11  
    2.12  - check HTML header of library;
    2.13  
     3.1 --- a/Admin/makebundle	Wed Sep 07 17:41:29 2011 -0700
     3.2 +++ b/Admin/makebundle	Wed Sep 07 19:24:28 2011 -0700
     3.3 @@ -75,7 +75,13 @@
     3.4  )
     3.5  
     3.6  case "$PLATFORM" in
     3.7 -  x86-cygwin)
     3.8 +  *-darwin)
     3.9 +    perl -pi -e "s,lookAndFeel=.*,lookAndFeel=com.apple.laf.AquaLookAndFeel,g;" \
    3.10 +      "$TMP/$ISABELLE_NAME/src/Tools/jEdit/dist/properties/jEdit.props"
    3.11 +    ;;
    3.12 +  *-cygwin)
    3.13 +    perl -pi -e "s,lookAndFeel=.*,lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel,g;" \
    3.14 +      "$TMP/$ISABELLE_NAME/src/Tools/jEdit/dist/properties/jEdit.props"
    3.15      rm "$TMP/$ISABELLE_NAME/contrib/ProofGeneral"
    3.16      ln -s ProofGeneral-3.7.1.1 "$TMP/$ISABELLE_NAME/contrib/ProofGeneral"
    3.17      ;;
     4.1 --- a/CONTRIBUTORS	Wed Sep 07 17:41:29 2011 -0700
     4.2 +++ b/CONTRIBUTORS	Wed Sep 07 19:24:28 2011 -0700
     4.3 @@ -3,8 +3,14 @@
     4.4  who is listed as an author in one of the source files of this Isabelle
     4.5  distribution.
     4.6  
     4.7 -Contributions to this Isabelle version
     4.8 ---------------------------------------
     4.9 +Contributions to Isabelle2011-1
    4.10 +-------------------------------
    4.11 +
    4.12 +* September 2011: Peter Gammie
    4.13 +  Theory HOL/Libary/Saturated: numbers with saturated arithmetic.
    4.14 +
    4.15 +* August 2011: Florian Haftmann, Johannes Hölzl and Lars Noschinski, TUM
    4.16 +  Refined theory on complete lattices.
    4.17  
    4.18  
    4.19  Contributions to Isabelle2011
     5.1 --- a/NEWS	Wed Sep 07 17:41:29 2011 -0700
     5.2 +++ b/NEWS	Wed Sep 07 19:24:28 2011 -0700
     5.3 @@ -1,8 +1,8 @@
     5.4  Isabelle NEWS -- history user-relevant changes
     5.5  ==============================================
     5.6  
     5.7 -New in this Isabelle version
     5.8 -----------------------------
     5.9 +New in Isabelle2011-1 (October 2011)
    5.10 +------------------------------------
    5.11  
    5.12  *** General ***
    5.13  
    5.14 @@ -34,6 +34,13 @@
    5.15  See also ~~/src/Tools/jEdit/README.html for further information,
    5.16  including some remaining limitations.
    5.17  
    5.18 +* Theory loader: source files are exclusively located via the master
    5.19 +directory of each theory node (where the .thy file itself resides).
    5.20 +The global load path (such as src/HOL/Library) has been discontinued.
    5.21 +Note that the path element ~~ may be used to reference theories in the
    5.22 +Isabelle home folder -- for instance, "~~/src/HOL/Library/FuncSet".
    5.23 +INCOMPATIBILITY.
    5.24 +
    5.25  * Theory loader: source files are identified by content via SHA1
    5.26  digests.  Discontinued former path/modtime identification and optional
    5.27  ISABELLE_FILE_IDENT plugin scripts.
    5.28 @@ -48,13 +55,6 @@
    5.29  * Discontinued old lib/scripts/polyml-platform, which has been
    5.30  obsolete since Isabelle2009-2.
    5.31  
    5.32 -* Theory loader: source files are exclusively located via the master
    5.33 -directory of each theory node (where the .thy file itself resides).
    5.34 -The global load path (such as src/HOL/Library) has been discontinued.
    5.35 -Note that the path element ~~ may be used to reference theories in the
    5.36 -Isabelle home folder -- for instance, "~~/src/HOL/Library/FuncSet".
    5.37 -INCOMPATIBILITY.
    5.38 -
    5.39  * Various optional external tools are referenced more robustly and
    5.40  uniformly by explicit Isabelle settings as follows:
    5.41  
    5.42 @@ -82,29 +82,38 @@
    5.43  that the result needs to be unique, which means fact specifications
    5.44  may have to be refined after enriching a proof context.
    5.45  
    5.46 +* Attribute "case_names" has been refined: the assumptions in each case
    5.47 +can be named now by following the case name with [name1 name2 ...].
    5.48 +
    5.49  * Isabelle/Isar reference manual provides more formal references in
    5.50  syntax diagrams.
    5.51  
    5.52 -* Attribute case_names has been refined: the assumptions in each case can
    5.53 -be named now by following the case name with [name1 name2 ...].
    5.54 -
    5.55  
    5.56  *** HOL ***
    5.57  
    5.58 -* Classes bot and top require underlying partial order rather than preorder:
    5.59 -uniqueness of bot and top is guaranteed.  INCOMPATIBILITY.
    5.60 +* Theory Library/Saturated provides type of numbers with saturated
    5.61 +arithmetic.
    5.62 +
    5.63 +* Classes bot and top require underlying partial order rather than
    5.64 +preorder: uniqueness of bot and top is guaranteed.  INCOMPATIBILITY.
    5.65  
    5.66  * Class complete_lattice: generalized a couple of lemmas from sets;
    5.67 -generalized theorems INF_cong and SUP_cong.  New type classes for complete
    5.68 -boolean algebras and complete linear orders.  Lemmas Inf_less_iff,
    5.69 -less_Sup_iff, INF_less_iff, less_SUP_iff now reside in class complete_linorder.
    5.70 -Changed proposition of lemmas Inf_bool_def, Sup_bool_def, Inf_fun_def, Sup_fun_def,
    5.71 -Inf_apply, Sup_apply.
    5.72 +generalized theorems INF_cong and SUP_cong.  New type classes for
    5.73 +complete boolean algebras and complete linear orders.  Lemmas
    5.74 +Inf_less_iff, less_Sup_iff, INF_less_iff, less_SUP_iff now reside in
    5.75 +class complete_linorder.
    5.76 +
    5.77 +Changed proposition of lemmas Inf_bool_def, Sup_bool_def, Inf_fun_def,
    5.78 +Sup_fun_def, Inf_apply, Sup_apply.
    5.79 +
    5.80  Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary, Sup_binary,
    5.81  INF_eq, SUP_eq, INF_UNIV_range, SUP_UNIV_range, Int_eq_Inter,
    5.82 -INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union, UNION_eq_Union_image,
    5.83 -Union_def, UN_singleton, UN_eq have been discarded.
    5.84 -More consistent and less misunderstandable names:
    5.85 +INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union,
    5.86 +UNION_eq_Union_image, Union_def, UN_singleton, UN_eq have been
    5.87 +discarded.
    5.88 +
    5.89 +More consistent and comprehensive names:
    5.90 +
    5.91    INFI_def ~> INF_def
    5.92    SUPR_def ~> SUP_def
    5.93    INF_leI ~> INF_lower
    5.94 @@ -122,30 +131,35 @@
    5.95  
    5.96  INCOMPATIBILITY.
    5.97  
    5.98 -* Theorem collections ball_simps and bex_simps do not contain theorems referring
    5.99 -to UNION any longer;  these have been moved to collection UN_ball_bex_simps.
   5.100 -INCOMPATIBILITY.
   5.101 -
   5.102 -* Archimedean_Field.thy:
   5.103 -    floor now is defined as parameter of a separate type class floor_ceiling.
   5.104 - 
   5.105 -* Finite_Set.thy: more coherent development of fold_set locales:
   5.106 +* Theorem collections ball_simps and bex_simps do not contain theorems
   5.107 +referring to UNION any longer; these have been moved to collection
   5.108 +UN_ball_bex_simps.  INCOMPATIBILITY.
   5.109 +
   5.110 +* Theory Archimedean_Field: floor now is defined as parameter of a
   5.111 +separate type class floor_ceiling.
   5.112 +
   5.113 +* Theory Finite_Set: more coherent development of fold_set locales:
   5.114  
   5.115      locale fun_left_comm ~> locale comp_fun_commute
   5.116      locale fun_left_comm_idem ~> locale comp_fun_idem
   5.117 -    
   5.118 -Both use point-free characterisation; interpretation proofs may need adjustment.
   5.119 -INCOMPATIBILITY.
   5.120 +
   5.121 +Both use point-free characterization; interpretation proofs may need
   5.122 +adjustment.  INCOMPATIBILITY.
   5.123  
   5.124  * Code generation:
   5.125 -  - theory Library/Code_Char_ord provides native ordering of characters
   5.126 -    in the target language.
   5.127 -  - commands code_module and code_library are legacy, use export_code instead. 
   5.128 -  - method evaluation is legacy, use method eval instead.
   5.129 -  - legacy evaluator "SML" is deactivated by default. To activate it, add the following
   5.130 -    line in your theory:
   5.131 +
   5.132 +  - Theory Library/Code_Char_ord provides native ordering of
   5.133 +    characters in the target language.
   5.134 +
   5.135 +  - Commands code_module and code_library are legacy, use export_code instead.
   5.136 +
   5.137 +  - Method "evaluation" is legacy, use method "eval" instead.
   5.138 +
   5.139 +  - Legacy evaluator "SML" is deactivated by default.  May be
   5.140 +    reactivated by the following theory command:
   5.141 +
   5.142        setup {* Value.add_evaluator ("SML", Codegen.eval_term) *}
   5.143 - 
   5.144 +
   5.145  * Declare ext [intro] by default.  Rare INCOMPATIBILITY.
   5.146  
   5.147  * Nitpick:
   5.148 @@ -168,51 +182,57 @@
   5.149    - Removed "metisF" -- use "metis" instead. INCOMPATIBILITY.
   5.150    - Obsoleted "metisFT" -- use "metis (full_types)" instead. INCOMPATIBILITY.
   5.151  
   5.152 -* "try":
   5.153 -  - Renamed "try_methods" and added "simp:", "intro:", "dest:", and "elim:"
   5.154 -    options. INCOMPATIBILITY.
   5.155 -  - Introduced "try" that not only runs "try_methods" but also "solve_direct",
   5.156 -    "sledgehammer", "quickcheck", and "nitpick".
   5.157 +* Command 'try':
   5.158 +  - Renamed 'try_methods' and added "simp:", "intro:", "dest:", and
   5.159 +    "elim:" options. INCOMPATIBILITY.
   5.160 +  - Introduced 'tryÄ that not only runs 'try_methods' but also
   5.161 +    'solve_direct', 'sledgehammer', 'quickcheck', and 'nitpick'.
   5.162  
   5.163  * Quickcheck:
   5.164 +
   5.165    - Added "eval" option to evaluate terms for the found counterexample
   5.166 -    (currently only supported by the default (exhaustive) tester)
   5.167 +    (currently only supported by the default (exhaustive) tester).
   5.168 +
   5.169    - Added post-processing of terms to obtain readable counterexamples
   5.170 -    (currently only supported by the default (exhaustive) tester)
   5.171 +    (currently only supported by the default (exhaustive) tester).
   5.172 +
   5.173    - New counterexample generator quickcheck[narrowing] enables
   5.174 -    narrowing-based testing.
   5.175 -    It requires that the Glasgow Haskell compiler is installed and
   5.176 -    its location is known to Isabelle with the environment variable
   5.177 -    ISABELLE_GHC.
   5.178 +    narrowing-based testing.  Requires the Glasgow Haskell compiler
   5.179 +    with its installation location defined in the Isabelle settings
   5.180 +    environment as ISABELLE_GHC.
   5.181 +
   5.182    - Removed quickcheck tester "SML" based on the SML code generator
   5.183 -    from HOL-Library
   5.184 +    (formly in HOL/Library).
   5.185  
   5.186  * Function package: discontinued option "tailrec".
   5.187 -INCOMPATIBILITY. Use partial_function instead.
   5.188 -
   5.189 -* HOL-Probability:
   5.190 +INCOMPATIBILITY. Use 'partial_function' instead.
   5.191 +
   5.192 +* Session HOL-Probability:
   5.193    - Caratheodory's extension lemma is now proved for ring_of_sets.
   5.194    - Infinite products of probability measures are now available.
   5.195 -  - Use extended reals instead of positive extended reals.
   5.196 -    INCOMPATIBILITY.
   5.197 -
   5.198 -* Old recdef package has been moved to Library/Old_Recdef.thy, where it
   5.199 -must be loaded explicitly.  INCOMPATIBILITY.
   5.200 -
   5.201 -* Well-founded recursion combinator "wfrec" has been moved to
   5.202 -Library/Wfrec.thy. INCOMPATIBILITY.
   5.203 -
   5.204 -* Theory Library/Nat_Infinity has been renamed to Library/Extended_Nat.
   5.205 -The names of the following types and constants have changed:
   5.206 -  inat (type) ~> enat
   5.207 +  - Use extended reals instead of positive extended
   5.208 +    reals. INCOMPATIBILITY.
   5.209 +
   5.210 +* Old 'recdef' package has been moved to theory Library/Old_Recdef,
   5.211 +from where it must be imported explicitly.  INCOMPATIBILITY.
   5.212 +
   5.213 +* Well-founded recursion combinator "wfrec" has been moved to theory
   5.214 +Library/Wfrec. INCOMPATIBILITY.
   5.215 +
   5.216 +* Theory Library/Nat_Infinity has been renamed to
   5.217 +Library/Extended_Nat, with name changes of the following types and
   5.218 +constants:
   5.219 +
   5.220 +  type inat   ~> type enat
   5.221    Fin         ~> enat
   5.222    Infty       ~> infinity (overloaded)
   5.223    iSuc        ~> eSuc
   5.224    the_Fin     ~> the_enat
   5.225 +
   5.226  Every theorem name containing "inat", "Fin", "Infty", or "iSuc" has
   5.227  been renamed accordingly.
   5.228  
   5.229 -* Limits.thy: Type "'a net" has been renamed to "'a filter", in
   5.230 +* Theory Limits: Type "'a net" has been renamed to "'a filter", in
   5.231  accordance with standard mathematical terminology. INCOMPATIBILITY.
   5.232  
   5.233  * Session Multivariate_Analysis: Type "('a, 'b) cart" has been renamed
   5.234 @@ -283,10 +303,10 @@
   5.235    real_abs_sub_norm ~> norm_triangle_ineq3
   5.236    norm_cauchy_schwarz_abs ~> Cauchy_Schwarz_ineq2
   5.237  
   5.238 -* Complex_Main: The locale interpretations for the bounded_linear and
   5.239 -bounded_bilinear locales have been removed, in order to reduce the
   5.240 -number of duplicate lemmas. Users must use the original names for
   5.241 -distributivity theorems, potential INCOMPATIBILITY.
   5.242 +* Theory Complex_Main: The locale interpretations for the
   5.243 +bounded_linear and bounded_bilinear locales have been removed, in
   5.244 +order to reduce the number of duplicate lemmas. Users must use the
   5.245 +original names for distributivity theorems, potential INCOMPATIBILITY.
   5.246  
   5.247    divide.add ~> add_divide_distrib
   5.248    divide.diff ~> diff_divide_distrib
   5.249 @@ -296,7 +316,7 @@
   5.250    mult_right.setsum ~> setsum_right_distrib
   5.251    mult_left.diff ~> left_diff_distrib
   5.252  
   5.253 -* Complex_Main: Several redundant theorems have been removed or
   5.254 +* Theory Complex_Main: Several redundant theorems have been removed or
   5.255  replaced by more general versions. INCOMPATIBILITY.
   5.256  
   5.257    real_of_int_real_of_nat ~> real_of_int_of_nat_eq
   5.258 @@ -365,26 +385,30 @@
   5.259  
   5.260  *** Document preparation ***
   5.261  
   5.262 -* Discontinued special treatment of hard tabulators, which are better
   5.263 -avoided in the first place.  Implicit tab-width is 1.
   5.264 -
   5.265 -* Antiquotation @{rail} layouts railroad syntax diagrams, see also
   5.266 -isar-ref manual.
   5.267 -
   5.268 -* Antiquotation @{value} evaluates the given term and presents its result.
   5.269 -
   5.270  * Localized \isabellestyle switch can be used within blocks or groups
   5.271  like this:
   5.272  
   5.273    \isabellestyle{it}  %preferred default
   5.274    {\isabellestylett @{text "typewriter stuff"}}
   5.275  
   5.276 -* New term style "isub" as ad-hoc conversion of variables x1, y23 into
   5.277 -subscripted form x\<^isub>1, y\<^isub>2\<^isub>3.
   5.278 +* Antiquotation @{rail} layouts railroad syntax diagrams, see also
   5.279 +isar-ref manual, both for description and actual application of the
   5.280 +same.
   5.281 +
   5.282 +* Antiquotation @{value} evaluates the given term and presents its
   5.283 +result.
   5.284 +
   5.285 +* Antiquotations: term style "isub" provides ad-hoc conversion of
   5.286 +variables x1, y23 into subscripted form x\<^isub>1,
   5.287 +y\<^isub>2\<^isub>3.
   5.288  
   5.289  * Predefined LaTeX macros for Isabelle symbols \<bind> and \<then>
   5.290  (e.g. see ~~/src/HOL/Library/Monad_Syntax.thy).
   5.291  
   5.292 +* Discontinued special treatment of hard tabulators, which are better
   5.293 +avoided in the first place (no universally agreed standard expansion).
   5.294 +Implicit tab-width is now 1.
   5.295 +
   5.296  
   5.297  *** ML ***
   5.298  
   5.299 @@ -443,12 +467,22 @@
   5.300  INCOMPATIBILITY, classical tactics and derived proof methods require
   5.301  proper Proof.context.
   5.302  
   5.303 +
   5.304 +*** System ***
   5.305 +
   5.306  * Scala layer provides JVM method invocation service for static
   5.307 -methods of type (String)String, see Invoke_Scala.method in ML.
   5.308 -For example:
   5.309 +methods of type (String)String, see Invoke_Scala.method in ML.  For
   5.310 +example:
   5.311  
   5.312    Invoke_Scala.method "java.lang.System.getProperty" "java.home"
   5.313  
   5.314 +Togeter with YXML.string_of_body/parse_body and XML.Encode/Decode this
   5.315 +allows to pass structured values between ML and Scala.
   5.316 +
   5.317 +* The IsabelleText fonts includes some further glyphs to support the
   5.318 +Prover IDE.  Potential INCOMPATIBILITY: users who happen to have
   5.319 +installed a local copy (which is normally *not* required) need to
   5.320 +delete or update it from ~~/lib/fonts/.
   5.321  
   5.322  
   5.323  New in Isabelle2011 (January 2011)
     6.1 --- a/README	Wed Sep 07 17:41:29 2011 -0700
     6.2 +++ b/README	Wed Sep 07 19:24:28 2011 -0700
     6.3 @@ -16,8 +16,8 @@
     6.4       * The Poly/ML compiler and runtime system (version 5.2.1 or later).
     6.5       * The GNU bash shell (version 3.x or 2.x).
     6.6       * Perl (version 5.x).
     6.7 +     * Java 1.6.x from Oracle or Apple -- for Scala and jEdit.
     6.8       * GNU Emacs (version 23) -- for the Proof General 4.x interface.
     6.9 -     * Java 1.6.x from Oracle/Sun or Apple -- for Scala and jEdit.
    6.10       * A complete LaTeX installation -- for document preparation.
    6.11  
    6.12  Installation
    6.13 @@ -31,17 +31,18 @@
    6.14  
    6.15  User interface
    6.16  
    6.17 +   Isabelle/jEdit is an emerging Prover IDE based on advanced
    6.18 +   technology of Isabelle/Scala.  It provides a metaphor of continuous
    6.19 +   proof checking of a versioned collection of theory sources, with
    6.20 +   instantaneous feedback in real-time and rich semantic markup
    6.21 +   associated with the formal text.
    6.22 +
    6.23     The classic Isabelle user interface is Proof General by David
    6.24     Aspinall and others.  It is a generic Emacs interface for proof
    6.25     assistants, including Isabelle.  Its most prominent feature is
    6.26     script management, providing a metaphor of stepwise proof script
    6.27     editing.
    6.28  
    6.29 -   Isabelle/jEdit is an experimental Prover IDE based on advanced
    6.30 -   technology of Isabelle/Scala.  It provides a metaphor of continuous
    6.31 -   proof checking of a versioned collection of theory sources, with
    6.32 -   instantaneous feedback in real-time.
    6.33 -
    6.34  Other sources of information
    6.35  
    6.36    The Isabelle Page
     7.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Wed Sep 07 17:41:29 2011 -0700
     7.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Wed Sep 07 19:24:28 2011 -0700
     7.3 @@ -942,19 +942,29 @@
     7.4  \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
     7.5  \textit{mono\_tags}, and \textit{mono\_simple} are fully
     7.6  typed and sound. For each of these, Sledgehammer also provides a lighter,
     7.7 -virtually sound variant identified by a question mark (`{?}')\ that detects and
     7.8 -erases monotonic types, notably infinite types. (For \textit{mono\_simple}, the
     7.9 -types are not actually erased but rather replaced by a shared uniform type of
    7.10 -individuals.) As argument to the \textit{metis} proof method, the question mark
    7.11 -is replaced by a \hbox{``\textit{\_query}''} suffix. If the \emph{sound} option
    7.12 -is enabled, these encodings are fully sound.
    7.13 +virtually sound variant identified by a question mark (`\hbox{?}')\ that detects
    7.14 +and erases monotonic types, notably infinite types. (For \textit{mono\_simple},
    7.15 +the types are not actually erased but rather replaced by a shared uniform type
    7.16 +of individuals.) As argument to the \textit{metis} proof method, the question
    7.17 +mark is replaced by a \hbox{``\textit{\_query}''} suffix. If the \emph{sound}
    7.18 +option is enabled, these encodings are fully sound.
    7.19  
    7.20  \item[$\bullet$]
    7.21  \textbf{%
    7.22  \textit{poly\_guards}??, \textit{poly\_tags}??, \textit{raw\_mono\_guards}??, \\
    7.23  \textit{raw\_mono\_tags}??, \textit{mono\_guards}??, \textit{mono\_tags}?? \\
    7.24  (quasi-sound):} \\
    7.25 -Even lighter versions of the `{?}' encodings.
    7.26 +Even lighter versions of the `\hbox{?}' encodings. As argument to the
    7.27 +\textit{metis} proof method, the `\hbox{??}' suffix is replaced by
    7.28 +\hbox{``\textit{\_query\_query}''}.
    7.29 +
    7.30 +\item[$\bullet$]
    7.31 +\textbf{%
    7.32 +\textit{poly\_guards}@?, \textit{poly\_tags}@?, \textit{raw\_mono\_guards}@?, \\
    7.33 +\textit{raw\_mono\_tags}@? (quasi-sound):} \\
    7.34 +Alternative versions of the `\hbox{??}' encodings. As argument to the
    7.35 +\textit{metis} proof method, the `\hbox{@?}' suffix is replaced by
    7.36 +\hbox{``\textit{\_at\_query}''}.
    7.37  
    7.38  \item[$\bullet$]
    7.39  \textbf{%
    7.40 @@ -965,9 +975,9 @@
    7.41  \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, \textit{mono\_guards},
    7.42  \textit{mono\_tags}, \textit{mono\_simple}, and \textit{mono\_simple\_higher}
    7.43  also admit a mildly unsound (but very efficient) variant identified by an
    7.44 -exclamation mark (`{!}') that detects and erases erases all types except those
    7.45 -that are clearly finite (e.g., \textit{bool}). (For \textit{mono\_simple} and
    7.46 -\textit{mono\_simple\_higher}, the types are not actually erased but rather
    7.47 +exclamation mark (`\hbox{!}') that detects and erases erases all types except
    7.48 +those that are clearly finite (e.g., \textit{bool}). (For \textit{mono\_simple}
    7.49 +and \textit{mono\_simple\_higher}, the types are not actually erased but rather
    7.50  replaced by a shared uniform type of individuals.) As argument to the
    7.51  \textit{metis} proof method, the exclamation mark is replaced by the suffix
    7.52  \hbox{``\textit{\_bang}''}.
    7.53 @@ -977,7 +987,17 @@
    7.54  \textit{poly\_guards}!!, \textit{poly\_tags}!!, \textit{raw\_mono\_guards}!!, \\
    7.55  \textit{raw\_mono\_tags}!!, \textit{mono\_guards}!!, \textit{mono\_tags}!! \\
    7.56  (mildly unsound):} \\
    7.57 -Even lighter versions of the `{!}' encodings.
    7.58 +Even lighter versions of the `\hbox{!}' encodings. As argument to the
    7.59 +\textit{metis} proof method, the `\hbox{!!}' suffix is replaced by
    7.60 +\hbox{``\textit{\_bang\_bang}''}.
    7.61 +
    7.62 +\item[$\bullet$]
    7.63 +\textbf{%
    7.64 +\textit{poly\_guards}@!, \textit{poly\_tags}@!, \textit{raw\_mono\_guards}@!, \\
    7.65 +\textit{raw\_mono\_tags}@! (mildly unsound):} \\
    7.66 +Alternative versions of the `\hbox{!!}' encodings. As argument to the
    7.67 +\textit{metis} proof method, the `\hbox{@!}' suffix is replaced by
    7.68 +\hbox{``\textit{\_at\_bang}''}.
    7.69  
    7.70  \item[$\bullet$] \textbf{\textit{smart}:} The actual encoding used depends on
    7.71  the ATP and should be the most efficient virtually sound encoding for that ATP.
     8.1 --- a/doc-src/System/Thy/Misc.thy	Wed Sep 07 17:41:29 2011 -0700
     8.2 +++ b/doc-src/System/Thy/Misc.thy	Wed Sep 07 19:24:28 2011 -0700
     8.3 @@ -336,8 +336,8 @@
     8.4    sub-chunks separated by @{text "\<^bold>Y"}.  Markup chunks start
     8.5    with an empty sub-chunk, and a second empty sub-chunk indicates
     8.6    close of an element.  Any other non-empty chunk consists of plain
     8.7 -  text.  For example, see @{file "~~/src/Pure/General/yxml.ML"} or
     8.8 -  @{file "~~/src/Pure/General/yxml.scala"}.
     8.9 +  text.  For example, see @{file "~~/src/Pure/PIDE/yxml.ML"} or
    8.10 +  @{file "~~/src/Pure/PIDE/yxml.scala"}.
    8.11  
    8.12    YXML documents may be detected quickly by checking that the first
    8.13    two characters are @{text "\<^bold>X\<^bold>Y"}.
     9.1 --- a/doc-src/System/Thy/document/Misc.tex	Wed Sep 07 17:41:29 2011 -0700
     9.2 +++ b/doc-src/System/Thy/document/Misc.tex	Wed Sep 07 19:24:28 2011 -0700
     9.3 @@ -376,8 +376,8 @@
     9.4    sub-chunks separated by \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}.  Markup chunks start
     9.5    with an empty sub-chunk, and a second empty sub-chunk indicates
     9.6    close of an element.  Any other non-empty chunk consists of plain
     9.7 -  text.  For example, see \verb|~~/src/Pure/General/yxml.ML| or
     9.8 -  \verb|~~/src/Pure/General/yxml.scala|.
     9.9 +  text.  For example, see \verb|~~/src/Pure/PIDE/yxml.ML| or
    9.10 +  \verb|~~/src/Pure/PIDE/yxml.scala|.
    9.11  
    9.12    YXML documents may be detected quickly by checking that the first
    9.13    two characters are \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}.%
    10.1 --- a/doc/Contents	Wed Sep 07 17:41:29 2011 -0700
    10.2 +++ b/doc/Contents	Wed Sep 07 19:24:28 2011 -0700
    10.3 @@ -1,4 +1,4 @@
    10.4 -Learning and using Isabelle
    10.5 +Miscellaneous tutorials
    10.6    tutorial        Tutorial on Isabelle/HOL
    10.7    main            What's in Main
    10.8    isar-overview   Tutorial on Isar
    11.1 --- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Wed Sep 07 17:41:29 2011 -0700
    11.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Wed Sep 07 19:24:28 2011 -0700
    11.3 @@ -12,8 +12,7 @@
    11.4  begin
    11.5  
    11.6  text {* Formalization of normal form *}
    11.7 -fun
    11.8 -  isnorm :: "('a::{comm_ring}) pol \<Rightarrow> bool"
    11.9 +fun isnorm :: "'a::comm_ring pol \<Rightarrow> bool"
   11.10  where
   11.11      "isnorm (Pc c) \<longleftrightarrow> True"
   11.12    | "isnorm (Pinj i (Pc c)) \<longleftrightarrow> False"
   11.13 @@ -26,35 +25,40 @@
   11.14    | "isnorm (PX P i Q) \<longleftrightarrow> isnorm P \<and> isnorm Q"
   11.15  
   11.16  (* Some helpful lemmas *)
   11.17 -lemma norm_Pinj_0_False:"isnorm (Pinj 0 P) = False"
   11.18 -by(cases P, auto)
   11.19 +lemma norm_Pinj_0_False: "isnorm (Pinj 0 P) = False"
   11.20 +  by (cases P) auto
   11.21  
   11.22 -lemma norm_PX_0_False:"isnorm (PX (Pc 0) i Q) = False"
   11.23 -by(cases i, auto)
   11.24 +lemma norm_PX_0_False: "isnorm (PX (Pc 0) i Q) = False"
   11.25 +  by (cases i) auto
   11.26  
   11.27 -lemma norm_Pinj:"isnorm (Pinj i Q) \<Longrightarrow> isnorm Q"
   11.28 -by(cases i,simp add: norm_Pinj_0_False norm_PX_0_False,cases Q) auto
   11.29 +lemma norm_Pinj: "isnorm (Pinj i Q) \<Longrightarrow> isnorm Q"
   11.30 +  by (cases i) (simp add: norm_Pinj_0_False norm_PX_0_False, cases Q, auto)
   11.31  
   11.32 -lemma norm_PX2:"isnorm (PX P i Q) \<Longrightarrow> isnorm Q"
   11.33 -by(cases i, auto, cases P, auto, case_tac pol2, auto)
   11.34 +lemma norm_PX2: "isnorm (PX P i Q) \<Longrightarrow> isnorm Q"
   11.35 +  by (cases i) (auto, cases P, auto, case_tac pol2, auto)
   11.36 +
   11.37 +lemma norm_PX1: "isnorm (PX P i Q) \<Longrightarrow> isnorm P"
   11.38 +  by (cases i) (auto, cases P, auto, case_tac pol2, auto)
   11.39  
   11.40 -lemma norm_PX1:"isnorm (PX P i Q) \<Longrightarrow> isnorm P"
   11.41 -by(cases i, auto, cases P, auto, case_tac pol2, auto)
   11.42 -
   11.43 -lemma mkPinj_cn:"\<lbrakk>y~=0; isnorm Q\<rbrakk> \<Longrightarrow> isnorm (mkPinj y Q)" 
   11.44 -apply(auto simp add: mkPinj_def norm_Pinj_0_False split: pol.split)
   11.45 -apply(case_tac nat, auto simp add: norm_Pinj_0_False)
   11.46 -by(case_tac pol, auto) (case_tac y, auto)
   11.47 +lemma mkPinj_cn: "y ~= 0 \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (mkPinj y Q)"
   11.48 +  apply (auto simp add: mkPinj_def norm_Pinj_0_False split: pol.split)
   11.49 +  apply (case_tac nat, auto simp add: norm_Pinj_0_False)
   11.50 +  apply (case_tac pol, auto)
   11.51 +  apply (case_tac y, auto)
   11.52 +  done
   11.53  
   11.54  lemma norm_PXtrans: 
   11.55 -  assumes A:"isnorm (PX P x Q)" and "isnorm Q2" 
   11.56 +  assumes A: "isnorm (PX P x Q)" and "isnorm Q2" 
   11.57    shows "isnorm (PX P x Q2)"
   11.58 -proof(cases P)
   11.59 -  case (PX p1 y p2) with assms show ?thesis by(cases x, auto, cases p2, auto)
   11.60 +proof (cases P)
   11.61 +  case (PX p1 y p2)
   11.62 +  with assms show ?thesis by (cases x) (auto, cases p2, auto)
   11.63  next
   11.64 -  case Pc with assms show ?thesis by (cases x) auto
   11.65 +  case Pc
   11.66 +  with assms show ?thesis by (cases x) auto
   11.67  next
   11.68 -  case Pinj with assms show ?thesis by (cases x) auto
   11.69 +  case Pinj
   11.70 +  with assms show ?thesis by (cases x) auto
   11.71  qed
   11.72   
   11.73  lemma norm_PXtrans2:
   11.74 @@ -62,7 +66,7 @@
   11.75    shows "isnorm (PX P (Suc (n+x)) Q2)"
   11.76  proof (cases P)
   11.77    case (PX p1 y p2)
   11.78 -  with assms show ?thesis by (cases x, auto, cases p2, auto)
   11.79 +  with assms show ?thesis by (cases x) (auto, cases p2, auto)
   11.80  next
   11.81    case Pc
   11.82    with assms show ?thesis by (cases x) auto
   11.83 @@ -83,27 +87,33 @@
   11.84    with assms show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def)
   11.85  next
   11.86    case (PX P1 y P2)
   11.87 -  with assms have Y0: "y>0" by (cases y) auto
   11.88 +  with assms have Y0: "y > 0" by (cases y) auto
   11.89    from assms PX have "isnorm P1" "isnorm P2"
   11.90      by (auto simp add: norm_PX1[of P1 y P2] norm_PX2[of P1 y P2])
   11.91    from assms PX Y0 show ?thesis
   11.92 -    by (cases x, auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto)
   11.93 +    by (cases x) (auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto)
   11.94  qed
   11.95  
   11.96  text {* add conserves normalizedness *}
   11.97 -lemma add_cn:"isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<oplus> Q)"
   11.98 -proof(induct P Q rule: add.induct)
   11.99 -  case (2 c i P2) thus ?case by (cases P2, simp_all, cases i, simp_all)
  11.100 +lemma add_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<oplus> Q)"
  11.101 +proof (induct P Q rule: add.induct)
  11.102 +  case (2 c i P2)
  11.103 +  thus ?case by (cases P2) (simp_all, cases i, simp_all)
  11.104  next
  11.105 -  case (3 i P2 c) thus ?case by (cases P2, simp_all, cases i, simp_all)
  11.106 +  case (3 i P2 c)
  11.107 +  thus ?case by (cases P2) (simp_all, cases i, simp_all)
  11.108  next
  11.109    case (4 c P2 i Q2)
  11.110 -  then have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
  11.111 -  with 4 show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto)
  11.112 +  then have "isnorm P2" "isnorm Q2"
  11.113 +    by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
  11.114 +  with 4 show ?case
  11.115 +    by (cases i) (simp, cases P2, auto, case_tac pol2, auto)
  11.116  next
  11.117    case (5 P2 i Q2 c)
  11.118 -  then have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
  11.119 -  with 5 show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto)
  11.120 +  then have "isnorm P2" "isnorm Q2"
  11.121 +    by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
  11.122 +  with 5 show ?case
  11.123 +    by (cases i) (simp, cases P2, auto, case_tac pol2, auto)
  11.124  next
  11.125    case (6 x P2 y Q2)
  11.126    then have Y0: "y>0" by (cases y) (auto simp add: norm_Pinj_0_False)
  11.127 @@ -115,14 +125,17 @@
  11.128      moreover
  11.129      note 6 X0
  11.130      moreover
  11.131 -    from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
  11.132 +    from 6 have "isnorm P2" "isnorm Q2"
  11.133 +      by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
  11.134      moreover
  11.135 -    from 6 `x < y` y have "isnorm (Pinj d Q2)" by (cases d, simp, cases Q2, auto)
  11.136 +    from 6 `x < y` y have "isnorm (Pinj d Q2)"
  11.137 +      by (cases d, simp, cases Q2, auto)
  11.138      ultimately have ?case by (simp add: mkPinj_cn) }
  11.139    moreover
  11.140    { assume "x=y"
  11.141      moreover
  11.142 -    from 6 have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
  11.143 +    from 6 have "isnorm P2" "isnorm Q2"
  11.144 +      by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
  11.145      moreover
  11.146      note 6 Y0
  11.147      moreover
  11.148 @@ -133,30 +146,35 @@
  11.149      moreover
  11.150      note 6 Y0
  11.151      moreover
  11.152 -    from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
  11.153 +    from 6 have "isnorm P2" "isnorm Q2"
  11.154 +      by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
  11.155      moreover
  11.156 -    from 6 `x > y` x have "isnorm (Pinj d P2)" by (cases d, simp, cases P2, auto)
  11.157 -    ultimately have ?case by (simp add: mkPinj_cn)}
  11.158 +    from 6 `x > y` x have "isnorm (Pinj d P2)"
  11.159 +      by (cases d) (simp, cases P2, auto)
  11.160 +    ultimately have ?case by (simp add: mkPinj_cn) }
  11.161    ultimately show ?case by blast
  11.162  next
  11.163    case (7 x P2 Q2 y R)
  11.164 -  have "x=0 \<or> (x = 1) \<or> (x > 1)" by arith
  11.165 +  have "x = 0 \<or> x = 1 \<or> x > 1" by arith
  11.166    moreover
  11.167    { assume "x = 0"
  11.168      with 7 have ?case by (auto simp add: norm_Pinj_0_False) }
  11.169    moreover
  11.170    { assume "x = 1"
  11.171 -    from 7 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
  11.172 +    from 7 have "isnorm R" "isnorm P2"
  11.173 +      by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
  11.174      with 7 `x = 1` have "isnorm (R \<oplus> P2)" by simp
  11.175 -    with 7 `x = 1` have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
  11.176 +    with 7 `x = 1` have ?case
  11.177 +      by (simp add: norm_PXtrans[of Q2 y _]) }
  11.178    moreover
  11.179    { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
  11.180 -    then obtain d where X:"x=Suc (Suc d)" ..
  11.181 +    then obtain d where X: "x=Suc (Suc d)" ..
  11.182      with 7 have NR: "isnorm R" "isnorm P2"
  11.183        by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
  11.184      with 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto
  11.185      with 7 X NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp
  11.186 -    with `isnorm (PX Q2 y R)` X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
  11.187 +    with `isnorm (PX Q2 y R)` X have ?case
  11.188 +      by (simp add: norm_PXtrans[of Q2 y _]) }
  11.189    ultimately show ?case by blast
  11.190  next
  11.191    case (8 Q2 y R x P2)
  11.192 @@ -183,7 +201,7 @@
  11.193    with 9 have X0: "x>0" by (cases x) auto
  11.194    with 9 have NP1: "isnorm P1" and NP2: "isnorm P2"
  11.195      by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2])
  11.196 -  with 9 have NQ1:"isnorm Q1" and NQ2: "isnorm Q2"
  11.197 +  with 9 have NQ1: "isnorm Q1" and NQ2: "isnorm Q2"
  11.198      by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ Q2])
  11.199    have "y < x \<or> x = y \<or> x < y" by arith
  11.200    moreover
  11.201 @@ -194,7 +212,7 @@
  11.202      have "isnorm (PX P1 d (Pc 0))" 
  11.203      proof (cases P1)
  11.204        case (PX p1 y p2)
  11.205 -      with 9 sm1 sm2 show ?thesis by - (cases d, simp, cases p2, auto)
  11.206 +      with 9 sm1 sm2 show ?thesis by (cases d) (simp, cases p2, auto)
  11.207      next
  11.208        case Pc with 9 sm1 sm2 show ?thesis by (cases d) auto
  11.209      next
  11.210 @@ -214,35 +232,37 @@
  11.211      have "isnorm (PX Q1 d (Pc 0))" 
  11.212      proof (cases Q1)
  11.213        case (PX p1 y p2)
  11.214 -      with 9 sm1 sm2 show ?thesis by - (cases d, simp, cases p2, auto)
  11.215 +      with 9 sm1 sm2 show ?thesis by (cases d) (simp, cases p2, auto)
  11.216      next
  11.217        case Pc with 9 sm1 sm2 show ?thesis by (cases d) auto
  11.218      next
  11.219        case Pinj with 9 sm1 sm2 show ?thesis by (cases d) auto
  11.220      qed
  11.221      ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)" by auto
  11.222 -    with X0 sm1 sm2 have ?case by (simp add: mkPX_cn)}
  11.223 +    with X0 sm1 sm2 have ?case by (simp add: mkPX_cn) }
  11.224    ultimately show ?case by blast
  11.225  qed simp
  11.226  
  11.227  text {* mul concerves normalizedness *}
  11.228 -lemma mul_cn :"isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)"
  11.229 -proof(induct P Q rule: mul.induct)
  11.230 +lemma mul_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)"
  11.231 +proof (induct P Q rule: mul.induct)
  11.232    case (2 c i P2) thus ?case 
  11.233 -    by (cases P2, simp_all) (cases "i",simp_all add: mkPinj_cn)
  11.234 +    by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn)
  11.235  next
  11.236    case (3 i P2 c) thus ?case 
  11.237 -    by (cases P2, simp_all) (cases "i",simp_all add: mkPinj_cn)
  11.238 +    by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn)
  11.239  next
  11.240    case (4 c P2 i Q2)
  11.241 -  then have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
  11.242 +  then have "isnorm P2" "isnorm Q2"
  11.243 +    by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
  11.244    with 4 show ?case 
  11.245 -    by - (cases "c = 0", simp_all, cases "i = 0", simp_all add: mkPX_cn)
  11.246 +    by (cases "c = 0") (simp_all, cases "i = 0", simp_all add: mkPX_cn)
  11.247  next
  11.248    case (5 P2 i Q2 c)
  11.249 -  then have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
  11.250 +  then have "isnorm P2" "isnorm Q2"
  11.251 +    by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
  11.252    with 5 show ?case
  11.253 -    by - (cases "c = 0", simp_all, cases "i = 0", simp_all add: mkPX_cn)
  11.254 +    by (cases "c = 0") (simp_all, cases "i = 0", simp_all add: mkPX_cn)
  11.255  next
  11.256    case (6 x P2 y Q2)
  11.257    have "x < y \<or> x = y \<or> x > y" by arith
  11.258 @@ -256,7 +276,7 @@
  11.259      moreover
  11.260      from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
  11.261      moreover
  11.262 -    from 6 `x < y` y have "isnorm (Pinj d Q2)" by - (cases d, simp, cases Q2, auto) 
  11.263 +    from 6 `x < y` y have "isnorm (Pinj d Q2)" by (cases d) (simp, cases Q2, auto) 
  11.264      ultimately have ?case by (simp add: mkPinj_cn) }
  11.265    moreover
  11.266    { assume "x = y"
  11.267 @@ -278,7 +298,7 @@
  11.268      moreover
  11.269      from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
  11.270      moreover
  11.271 -    from 6 `x > y` x have "isnorm (Pinj d P2)" by - (cases d, simp, cases P2, auto)
  11.272 +    from 6 `x > y` x have "isnorm (Pinj d P2)" by (cases d) (simp, cases P2, auto)
  11.273      ultimately have ?case by (simp add: mkPinj_cn) }
  11.274    ultimately show ?case by blast
  11.275  next
  11.276 @@ -356,7 +376,7 @@
  11.277  proof (induct P)
  11.278    case (Pinj i P2)
  11.279    then have "isnorm P2" by (simp add: norm_Pinj[of i P2])
  11.280 -  with Pinj show ?case by - (cases P2, auto, cases i, auto)
  11.281 +  with Pinj show ?case by (cases P2) (auto, cases i, auto)
  11.282  next
  11.283    case (PX P1 x P2) note PX1 = this
  11.284    from PX have "isnorm P2" "isnorm P1"
  11.285 @@ -364,7 +384,7 @@
  11.286    with PX show ?case
  11.287    proof (cases P1)
  11.288      case (PX p1 y p2)
  11.289 -    with PX1 show ?thesis by - (cases x, auto, cases p2, auto)
  11.290 +    with PX1 show ?thesis by (cases x) (auto, cases p2, auto)
  11.291    next
  11.292      case Pinj
  11.293      with PX1 show ?thesis by (cases x) auto
  11.294 @@ -372,15 +392,18 @@
  11.295  qed simp
  11.296  
  11.297  text {* sub conserves normalizedness *}
  11.298 -lemma sub_cn:"isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)"
  11.299 -by (simp add: sub_def add_cn neg_cn)
  11.300 +lemma sub_cn: "isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)"
  11.301 +  by (simp add: sub_def add_cn neg_cn)
  11.302  
  11.303  text {* sqr conserves normalizizedness *}
  11.304 -lemma sqr_cn:"isnorm P \<Longrightarrow> isnorm (sqr P)"
  11.305 +lemma sqr_cn: "isnorm P \<Longrightarrow> isnorm (sqr P)"
  11.306  proof (induct P)
  11.307 +  case Pc
  11.308 +  then show ?case by simp
  11.309 +next
  11.310    case (Pinj i Q)
  11.311    then show ?case
  11.312 -    by - (cases Q, auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn)
  11.313 +    by (cases Q) (auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn)
  11.314  next 
  11.315    case (PX P1 x P2)
  11.316    then have "x + x ~= 0" "isnorm P2" "isnorm P1"
  11.317 @@ -389,20 +412,23 @@
  11.318        and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))"
  11.319      by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
  11.320    then show ?case by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
  11.321 -qed simp
  11.322 +qed
  11.323  
  11.324  text {* pow conserves normalizedness *}
  11.325 -lemma pow_cn:"isnorm P \<Longrightarrow> isnorm (pow n P)"
  11.326 -proof (induct n arbitrary: P rule: nat_less_induct)
  11.327 -  case (1 k)
  11.328 +lemma pow_cn: "isnorm P \<Longrightarrow> isnorm (pow n P)"
  11.329 +proof (induct n arbitrary: P rule: less_induct)
  11.330 +  case (less k)
  11.331    show ?case 
  11.332    proof (cases "k = 0")
  11.333 +    case True
  11.334 +    then show ?thesis by simp
  11.335 +  next
  11.336      case False
  11.337      then have K2: "k div 2 < k" by (cases k) auto
  11.338 -    from 1 have "isnorm (sqr P)" by (simp add: sqr_cn)
  11.339 -    with 1 False K2 show ?thesis
  11.340 -      by - (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn)
  11.341 -  qed simp
  11.342 +    from less have "isnorm (sqr P)" by (simp add: sqr_cn)
  11.343 +    with less False K2 show ?thesis
  11.344 +      by (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn)
  11.345 +  qed
  11.346  qed
  11.347  
  11.348  end
    12.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Wed Sep 07 17:41:29 2011 -0700
    12.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Wed Sep 07 19:24:28 2011 -0700
    12.3 @@ -676,13 +676,13 @@
    12.4    {assume nz: "n = 0" hence ?thesis by (simp add: Let_def simp_num_pair_def)}
    12.5    moreover
    12.6    { assume nnz: "n \<noteq> 0"
    12.7 -    {assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simp_num_pair_def simpnum_ci) }
    12.8 +    {assume "\<not> ?g > 1" hence ?thesis by (simp add: Let_def simp_num_pair_def) }
    12.9      moreover
   12.10      {assume g1:"?g>1" hence g0: "?g > 0" by simp
   12.11        from g1 nnz have gp0: "?g' \<noteq> 0" by simp
   12.12        hence g'p: "?g' > 0" using gcd_ge_0_int[where x="n" and y="numgcd ?t'"] by arith 
   12.13        hence "?g'= 1 \<or> ?g' > 1" by arith
   12.14 -      moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simp_num_pair_def simpnum_ci)}
   12.15 +      moreover {assume "?g'=1" hence ?thesis by (simp add: Let_def simp_num_pair_def)}
   12.16        moreover {assume g'1:"?g'>1"
   12.17          from dvdnumcoeff_aux2[OF g1] have th1:"dvdnumcoeff ?t' ?g" ..
   12.18          let ?tt = "reducecoeffh ?t' ?g'"
   12.19 @@ -800,32 +800,34 @@
   12.20  proof(induct p rule: simpfm.induct)
   12.21    case (6 a) hence nb: "numbound0 a" by simp
   12.22    hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
   12.23 -  thus ?case by (cases "simpnum a", auto simp add: Let_def)
   12.24 +  thus ?case by (cases "simpnum a") (auto simp add: Let_def)
   12.25  next
   12.26    case (7 a) hence nb: "numbound0 a" by simp
   12.27    hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
   12.28 -  thus ?case by (cases "simpnum a", auto simp add: Let_def)
   12.29 +  thus ?case by (cases "simpnum a") (auto simp add: Let_def)
   12.30  next
   12.31    case (8 a) hence nb: "numbound0 a" by simp
   12.32    hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
   12.33 -  thus ?case by (cases "simpnum a", auto simp add: Let_def)
   12.34 +  thus ?case by (cases "simpnum a") (auto simp add: Let_def)
   12.35  next
   12.36    case (9 a) hence nb: "numbound0 a" by simp
   12.37    hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
   12.38 -  thus ?case by (cases "simpnum a", auto simp add: Let_def)
   12.39 +  thus ?case by (cases "simpnum a") (auto simp add: Let_def)
   12.40  next
   12.41    case (10 a) hence nb: "numbound0 a" by simp
   12.42    hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
   12.43 -  thus ?case by (cases "simpnum a", auto simp add: Let_def)
   12.44 +  thus ?case by (cases "simpnum a") (auto simp add: Let_def)
   12.45  next
   12.46    case (11 a) hence nb: "numbound0 a" by simp
   12.47    hence "numbound0 (simpnum a)" by (simp only: simpnum_numbound0[OF nb])
   12.48 -  thus ?case by (cases "simpnum a", auto simp add: Let_def)
   12.49 +  thus ?case by (cases "simpnum a") (auto simp add: Let_def)
   12.50  qed(auto simp add: disj_def imp_def iff_def conj_def not_bn)
   12.51  
   12.52  lemma simpfm_qf: "qfree p \<Longrightarrow> qfree (simpfm p)"
   12.53 -by (induct p rule: simpfm.induct, auto simp add: disj_qf imp_qf iff_qf conj_qf not_qf Let_def)
   12.54 - (case_tac "simpnum a",auto)+
   12.55 +  apply (induct p rule: simpfm.induct)
   12.56 +  apply (auto simp add: Let_def)
   12.57 +  apply (case_tac "simpnum a", auto)+
   12.58 +  done
   12.59  
   12.60  consts prep :: "fm \<Rightarrow> fm"
   12.61  recdef prep "measure fmsize"
   12.62 @@ -854,7 +856,7 @@
   12.63    "prep p = p"
   12.64  (hints simp add: fmsize_pos)
   12.65  lemma prep: "\<And> bs. Ifm bs (prep p) = Ifm bs p"
   12.66 -by (induct p rule: prep.induct, auto)
   12.67 +  by (induct p rule: prep.induct) auto
   12.68  
   12.69    (* Generic quantifier elimination *)
   12.70  function (sequential) qelim :: "fm \<Rightarrow> (fm \<Rightarrow> fm) \<Rightarrow> fm" where
   12.71 @@ -1037,7 +1039,7 @@
   12.72    assumes qfp: "qfree p"
   12.73    shows "(Ifm bs (rlfm p) = Ifm bs p) \<and> isrlfm (rlfm p)"
   12.74    using qfp 
   12.75 -by (induct p rule: rlfm.induct, auto simp add: lt le gt ge eq neq conj disj conj_lin disj_lin)
   12.76 +by (induct p rule: rlfm.induct) (auto simp add: lt le gt ge eq neq conj disj conj_lin disj_lin)
   12.77  
   12.78      (* Operations needed for Ferrante and Rackoff *)
   12.79  lemma rminusinf_inf:
   12.80 @@ -1045,9 +1047,11 @@
   12.81    shows "\<exists> z. \<forall> x < z. Ifm (x#bs) (minusinf p) = Ifm (x#bs) p" (is "\<exists> z. \<forall> x. ?P z x p")
   12.82  using lp
   12.83  proof (induct p rule: minusinf.induct)
   12.84 -  case (1 p q) thus ?case by (auto,rule_tac x= "min z za" in exI) auto 
   12.85 +  case (1 p q)
   12.86 +  thus ?case apply auto apply (rule_tac x= "min z za" in exI) apply auto done
   12.87  next
   12.88 -  case (2 p q) thus ?case by (auto,rule_tac x= "min z za" in exI) auto
   12.89 +  case (2 p q)
   12.90 +  thus ?case apply auto apply (rule_tac x= "min z za" in exI) apply auto done
   12.91  next
   12.92    case (3 c e) 
   12.93    from 3 have nb: "numbound0 e" by simp
    13.1 --- a/src/HOL/HOLCF/Representable.thy	Wed Sep 07 17:41:29 2011 -0700
    13.2 +++ b/src/HOL/HOLCF/Representable.thy	Wed Sep 07 19:24:28 2011 -0700
    13.3 @@ -5,7 +5,7 @@
    13.4  header {* Representable domains *}
    13.5  
    13.6  theory Representable
    13.7 -imports Algebraic Map_Functions Countable
    13.8 +imports Algebraic Map_Functions "~~/src/HOL/Library/Countable"
    13.9  begin
   13.10  
   13.11  default_sort cpo
    14.1 --- a/src/HOL/IsaMakefile	Wed Sep 07 17:41:29 2011 -0700
    14.2 +++ b/src/HOL/IsaMakefile	Wed Sep 07 19:24:28 2011 -0700
    14.3 @@ -463,10 +463,10 @@
    14.4    Library/Quotient_Option.thy Library/Quotient_Product.thy		\
    14.5    Library/Quotient_Sum.thy Library/Quotient_Syntax.thy			\
    14.6    Library/Quotient_Type.thy Library/RBT.thy Library/RBT_Impl.thy	\
    14.7 -  Library/RBT_Mapping.thy Library/README.html Library/Set_Algebras.thy	\
    14.8 -  Library/State_Monad.thy Library/Ramsey.thy Library/Reflection.thy	\
    14.9 -  Library/Sublist_Order.thy Library/Sum_of_Squares.thy			\
   14.10 -  Library/Sum_of_Squares/sos_wrapper.ML					\
   14.11 +  Library/RBT_Mapping.thy Library/README.html Library/Saturated.thy	\
   14.12 +  Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy	\
   14.13 +  Library/Reflection.thy Library/Sublist_Order.thy			\
   14.14 +  Library/Sum_of_Squares.thy Library/Sum_of_Squares/sos_wrapper.ML	\
   14.15    Library/Sum_of_Squares/sum_of_squares.ML				\
   14.16    Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy		\
   14.17    Library/Wfrec.thy Library/While_Combinator.thy Library/Zorn.thy	\
    15.1 --- a/src/HOL/Library/Abstract_Rat.thy	Wed Sep 07 17:41:29 2011 -0700
    15.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Wed Sep 07 19:24:28 2011 -0700
    15.3 @@ -10,64 +10,57 @@
    15.4  
    15.5  type_synonym Num = "int \<times> int"
    15.6  
    15.7 -abbreviation
    15.8 -  Num0_syn :: Num ("0\<^sub>N")
    15.9 -where "0\<^sub>N \<equiv> (0, 0)"
   15.10 +abbreviation Num0_syn :: Num  ("0\<^sub>N")
   15.11 +  where "0\<^sub>N \<equiv> (0, 0)"
   15.12  
   15.13 -abbreviation
   15.14 -  Numi_syn :: "int \<Rightarrow> Num" ("_\<^sub>N")
   15.15 -where "i\<^sub>N \<equiv> (i, 1)"
   15.16 +abbreviation Numi_syn :: "int \<Rightarrow> Num"  ("_\<^sub>N")
   15.17 +  where "i\<^sub>N \<equiv> (i, 1)"
   15.18  
   15.19 -definition
   15.20 -  isnormNum :: "Num \<Rightarrow> bool"
   15.21 -where
   15.22 +definition isnormNum :: "Num \<Rightarrow> bool" where
   15.23    "isnormNum = (\<lambda>(a,b). (if a = 0 then b = 0 else b > 0 \<and> gcd a b = 1))"
   15.24  
   15.25 -definition
   15.26 -  normNum :: "Num \<Rightarrow> Num"
   15.27 -where
   15.28 -  "normNum = (\<lambda>(a,b). (if a=0 \<or> b = 0 then (0,0) else 
   15.29 -  (let g = gcd a b 
   15.30 -   in if b > 0 then (a div g, b div g) else (- (a div g), - (b div g)))))"
   15.31 +definition normNum :: "Num \<Rightarrow> Num" where
   15.32 +  "normNum = (\<lambda>(a,b).
   15.33 +    (if a=0 \<or> b = 0 then (0,0) else
   15.34 +      (let g = gcd a b
   15.35 +       in if b > 0 then (a div g, b div g) else (- (a div g), - (b div g)))))"
   15.36  
   15.37 -declare gcd_dvd1_int[presburger]
   15.38 -declare gcd_dvd2_int[presburger]
   15.39 +declare gcd_dvd1_int[presburger] gcd_dvd2_int[presburger]
   15.40 +
   15.41  lemma normNum_isnormNum [simp]: "isnormNum (normNum x)"
   15.42  proof -
   15.43 -  have " \<exists> a b. x = (a,b)" by auto
   15.44 -  then obtain a b where x[simp]: "x = (a,b)" by blast
   15.45 -  {assume "a=0 \<or> b = 0" hence ?thesis by (simp add: normNum_def isnormNum_def)}  
   15.46 +  obtain a b where x: "x = (a, b)" by (cases x)
   15.47 +  { assume "a=0 \<or> b = 0" hence ?thesis by (simp add: x normNum_def isnormNum_def) }
   15.48    moreover
   15.49 -  {assume anz: "a \<noteq> 0" and bnz: "b \<noteq> 0" 
   15.50 +  { assume anz: "a \<noteq> 0" and bnz: "b \<noteq> 0"
   15.51      let ?g = "gcd a b"
   15.52      let ?a' = "a div ?g"
   15.53      let ?b' = "b div ?g"
   15.54      let ?g' = "gcd ?a' ?b'"
   15.55 -    from anz bnz have "?g \<noteq> 0" by simp  with gcd_ge_0_int[of a b] 
   15.56 +    from anz bnz have "?g \<noteq> 0" by simp  with gcd_ge_0_int[of a b]
   15.57      have gpos: "?g > 0" by arith
   15.58 -    have gdvd: "?g dvd a" "?g dvd b" by arith+ 
   15.59 -    from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)]
   15.60 -    anz bnz
   15.61 -    have nz':"?a' \<noteq> 0" "?b' \<noteq> 0"
   15.62 -      by - (rule notI, simp)+
   15.63 -    from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith 
   15.64 +    have gdvd: "?g dvd a" "?g dvd b" by arith+
   15.65 +    from zdvd_mult_div_cancel[OF gdvd(1)] zdvd_mult_div_cancel[OF gdvd(2)] anz bnz
   15.66 +    have nz': "?a' \<noteq> 0" "?b' \<noteq> 0" by - (rule notI, simp)+
   15.67 +    from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith
   15.68      from div_gcd_coprime_int[OF stupid] have gp1: "?g' = 1" .
   15.69      from bnz have "b < 0 \<or> b > 0" by arith
   15.70      moreover
   15.71 -    {assume b: "b > 0"
   15.72 -      from b have "?b' \<ge> 0" 
   15.73 -        by (presburger add: pos_imp_zdiv_nonneg_iff[OF gpos])  
   15.74 -      with nz' have b': "?b' > 0" by arith 
   15.75 -      from b b' anz bnz nz' gp1 have ?thesis 
   15.76 -        by (simp add: isnormNum_def normNum_def Let_def split_def fst_conv snd_conv)}
   15.77 -    moreover {assume b: "b < 0"
   15.78 -      {assume b': "?b' \<ge> 0" 
   15.79 +    { assume b: "b > 0"
   15.80 +      from b have "?b' \<ge> 0"
   15.81 +        by (presburger add: pos_imp_zdiv_nonneg_iff[OF gpos])
   15.82 +      with nz' have b': "?b' > 0" by arith
   15.83 +      from b b' anz bnz nz' gp1 have ?thesis
   15.84 +        by (simp add: x isnormNum_def normNum_def Let_def split_def) }
   15.85 +    moreover {
   15.86 +      assume b: "b < 0"
   15.87 +      { assume b': "?b' \<ge> 0"
   15.88          from gpos have th: "?g \<ge> 0" by arith
   15.89          from mult_nonneg_nonneg[OF th b'] zdvd_mult_div_cancel[OF gdvd(2)]
   15.90          have False using b by arith }
   15.91 -      hence b': "?b' < 0" by (presburger add: linorder_not_le[symmetric]) 
   15.92 -      from anz bnz nz' b b' gp1 have ?thesis 
   15.93 -        by (simp add: isnormNum_def normNum_def Let_def split_def)}
   15.94 +      hence b': "?b' < 0" by (presburger add: linorder_not_le[symmetric])
   15.95 +      from anz bnz nz' b b' gp1 have ?thesis
   15.96 +        by (simp add: x isnormNum_def normNum_def Let_def split_def) }
   15.97      ultimately have ?thesis by blast
   15.98    }
   15.99    ultimately show ?thesis by blast
  15.100 @@ -75,63 +68,55 @@
  15.101  
  15.102  text {* Arithmetic over Num *}
  15.103  
  15.104 -definition
  15.105 -  Nadd :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "+\<^sub>N" 60)
  15.106 -where
  15.107 -  "Nadd = (\<lambda>(a,b) (a',b'). if a = 0 \<or> b = 0 then normNum(a',b') 
  15.108 -    else if a'=0 \<or> b' = 0 then normNum(a,b) 
  15.109 +definition Nadd :: "Num \<Rightarrow> Num \<Rightarrow> Num"  (infixl "+\<^sub>N" 60) where
  15.110 +  "Nadd = (\<lambda>(a,b) (a',b'). if a = 0 \<or> b = 0 then normNum(a',b')
  15.111 +    else if a'=0 \<or> b' = 0 then normNum(a,b)
  15.112      else normNum(a*b' + b*a', b*b'))"
  15.113  
  15.114 -definition
  15.115 -  Nmul :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "*\<^sub>N" 60)
  15.116 -where
  15.117 -  "Nmul = (\<lambda>(a,b) (a',b'). let g = gcd (a*a') (b*b') 
  15.118 +definition Nmul :: "Num \<Rightarrow> Num \<Rightarrow> Num"  (infixl "*\<^sub>N" 60) where
  15.119 +  "Nmul = (\<lambda>(a,b) (a',b'). let g = gcd (a*a') (b*b')
  15.120      in (a*a' div g, b*b' div g))"
  15.121  
  15.122 -definition
  15.123 -  Nneg :: "Num \<Rightarrow> Num" ("~\<^sub>N")
  15.124 -where
  15.125 -  "Nneg \<equiv> (\<lambda>(a,b). (-a,b))"
  15.126 +definition Nneg :: "Num \<Rightarrow> Num" ("~\<^sub>N")
  15.127 +  where "Nneg \<equiv> (\<lambda>(a,b). (-a,b))"
  15.128  
  15.129 -definition
  15.130 -  Nsub :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "-\<^sub>N" 60)
  15.131 -where
  15.132 -  "Nsub = (\<lambda>a b. a +\<^sub>N ~\<^sub>N b)"
  15.133 +definition Nsub :: "Num \<Rightarrow> Num \<Rightarrow> Num"  (infixl "-\<^sub>N" 60)
  15.134 +  where "Nsub = (\<lambda>a b. a +\<^sub>N ~\<^sub>N b)"
  15.135  
  15.136 -definition
  15.137 -  Ninv :: "Num \<Rightarrow> Num" 
  15.138 -where
  15.139 -  "Ninv \<equiv> \<lambda>(a,b). if a < 0 then (-b, \<bar>a\<bar>) else (b,a)"
  15.140 +definition Ninv :: "Num \<Rightarrow> Num"
  15.141 +  where "Ninv = (\<lambda>(a,b). if a < 0 then (-b, \<bar>a\<bar>) else (b,a))"
  15.142  
  15.143 -definition
  15.144 -  Ndiv :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "\<div>\<^sub>N" 60)
  15.145 -where
  15.146 -  "Ndiv \<equiv> \<lambda>a b. a *\<^sub>N Ninv b"
  15.147 +definition Ndiv :: "Num \<Rightarrow> Num \<Rightarrow> Num"  (infixl "\<div>\<^sub>N" 60)
  15.148 +  where "Ndiv = (\<lambda>a b. a *\<^sub>N Ninv b)"
  15.149  
  15.150  lemma Nneg_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (~\<^sub>N x)"
  15.151 -  by(simp add: isnormNum_def Nneg_def split_def)
  15.152 +  by (simp add: isnormNum_def Nneg_def split_def)
  15.153 +
  15.154  lemma Nadd_normN[simp]: "isnormNum (x +\<^sub>N y)"
  15.155    by (simp add: Nadd_def split_def)
  15.156 +
  15.157  lemma Nsub_normN[simp]: "\<lbrakk> isnormNum y\<rbrakk> \<Longrightarrow> isnormNum (x -\<^sub>N y)"
  15.158    by (simp add: Nsub_def split_def)
  15.159 -lemma Nmul_normN[simp]: assumes xn:"isnormNum x" and yn: "isnormNum y"
  15.160 +
  15.161 +lemma Nmul_normN[simp]:
  15.162 +  assumes xn: "isnormNum x" and yn: "isnormNum y"
  15.163    shows "isnormNum (x *\<^sub>N y)"
  15.164 -proof-
  15.165 -  have "\<exists>a b. x = (a,b)" and "\<exists> a' b'. y = (a',b')" by auto
  15.166 -  then obtain a b a' b' where ab: "x = (a,b)"  and ab': "y = (a',b')" by blast 
  15.167 -  {assume "a = 0"
  15.168 -    hence ?thesis using xn ab ab'
  15.169 -      by (simp add: isnormNum_def Let_def Nmul_def split_def)}
  15.170 +proof -
  15.171 +  obtain a b where x: "x = (a, b)" by (cases x)
  15.172 +  obtain a' b' where y: "y = (a', b')" by (cases y)
  15.173 +  { assume "a = 0"
  15.174 +    hence ?thesis using xn x y
  15.175 +      by (simp add: isnormNum_def Let_def Nmul_def split_def) }
  15.176    moreover
  15.177 -  {assume "a' = 0"
  15.178 -    hence ?thesis using yn ab ab' 
  15.179 -      by (simp add: isnormNum_def Let_def Nmul_def split_def)}
  15.180 +  { assume "a' = 0"
  15.181 +    hence ?thesis using yn x y
  15.182 +      by (simp add: isnormNum_def Let_def Nmul_def split_def) }
  15.183    moreover
  15.184 -  {assume a: "a \<noteq>0" and a': "a'\<noteq>0"
  15.185 -    hence bp: "b > 0" "b' > 0" using xn yn ab ab' by (simp_all add: isnormNum_def)
  15.186 -    from mult_pos_pos[OF bp] have "x *\<^sub>N y = normNum (a*a', b*b')" 
  15.187 -      using ab ab' a a' bp by (simp add: Nmul_def Let_def split_def normNum_def)
  15.188 -    hence ?thesis by simp}
  15.189 +  { assume a: "a \<noteq>0" and a': "a'\<noteq>0"
  15.190 +    hence bp: "b > 0" "b' > 0" using xn yn x y by (simp_all add: isnormNum_def)
  15.191 +    from mult_pos_pos[OF bp] have "x *\<^sub>N y = normNum (a * a', b * b')"
  15.192 +      using x y a a' bp by (simp add: Nmul_def Let_def split_def normNum_def)
  15.193 +    hence ?thesis by simp }
  15.194    ultimately show ?thesis by blast
  15.195  qed
  15.196  
  15.197 @@ -139,89 +124,77 @@
  15.198    by (simp add: Ninv_def isnormNum_def split_def)
  15.199      (cases "fst x = 0", auto simp add: gcd_commute_int)
  15.200  
  15.201 -lemma isnormNum_int[simp]: 
  15.202 +lemma isnormNum_int[simp]:
  15.203    "isnormNum 0\<^sub>N" "isnormNum ((1::int)\<^sub>N)" "i \<noteq> 0 \<Longrightarrow> isnormNum (i\<^sub>N)"
  15.204    by (simp_all add: isnormNum_def)
  15.205  
  15.206  
  15.207  text {* Relations over Num *}
  15.208  
  15.209 -definition
  15.210 -  Nlt0:: "Num \<Rightarrow> bool" ("0>\<^sub>N")
  15.211 -where
  15.212 -  "Nlt0 = (\<lambda>(a,b). a < 0)"
  15.213 +definition Nlt0:: "Num \<Rightarrow> bool"  ("0>\<^sub>N")
  15.214 +  where "Nlt0 = (\<lambda>(a,b). a < 0)"
  15.215  
  15.216 -definition
  15.217 -  Nle0:: "Num \<Rightarrow> bool" ("0\<ge>\<^sub>N")
  15.218 -where
  15.219 -  "Nle0 = (\<lambda>(a,b). a \<le> 0)"
  15.220 +definition Nle0:: "Num \<Rightarrow> bool"  ("0\<ge>\<^sub>N")
  15.221 +  where "Nle0 = (\<lambda>(a,b). a \<le> 0)"
  15.222  
  15.223 -definition
  15.224 -  Ngt0:: "Num \<Rightarrow> bool" ("0<\<^sub>N")
  15.225 -where
  15.226 -  "Ngt0 = (\<lambda>(a,b). a > 0)"
  15.227 +definition Ngt0:: "Num \<Rightarrow> bool"  ("0<\<^sub>N")
  15.228 +  where "Ngt0 = (\<lambda>(a,b). a > 0)"
  15.229  
  15.230 -definition
  15.231 -  Nge0:: "Num \<Rightarrow> bool" ("0\<le>\<^sub>N")
  15.232 -where
  15.233 -  "Nge0 = (\<lambda>(a,b). a \<ge> 0)"
  15.234 +definition Nge0:: "Num \<Rightarrow> bool"  ("0\<le>\<^sub>N")
  15.235 +  where "Nge0 = (\<lambda>(a,b). a \<ge> 0)"
  15.236  
  15.237 -definition
  15.238 -  Nlt :: "Num \<Rightarrow> Num \<Rightarrow> bool" (infix "<\<^sub>N" 55)
  15.239 -where
  15.240 -  "Nlt = (\<lambda>a b. 0>\<^sub>N (a -\<^sub>N b))"
  15.241 +definition Nlt :: "Num \<Rightarrow> Num \<Rightarrow> bool"  (infix "<\<^sub>N" 55)
  15.242 +  where "Nlt = (\<lambda>a b. 0>\<^sub>N (a -\<^sub>N b))"
  15.243  
  15.244 -definition
  15.245 -  Nle :: "Num \<Rightarrow> Num \<Rightarrow> bool" (infix "\<le>\<^sub>N" 55)
  15.246 -where
  15.247 -  "Nle = (\<lambda>a b. 0\<ge>\<^sub>N (a -\<^sub>N b))"
  15.248 +definition Nle :: "Num \<Rightarrow> Num \<Rightarrow> bool"  (infix "\<le>\<^sub>N" 55)
  15.249 +  where "Nle = (\<lambda>a b. 0\<ge>\<^sub>N (a -\<^sub>N b))"
  15.250  
  15.251 -definition
  15.252 -  "INum = (\<lambda>(a,b). of_int a / of_int b)"
  15.253 +definition "INum = (\<lambda>(a,b). of_int a / of_int b)"
  15.254  
  15.255  lemma INum_int [simp]: "INum (i\<^sub>N) = ((of_int i) ::'a::field)" "INum 0\<^sub>N = (0::'a::field)"
  15.256    by (simp_all add: INum_def)
  15.257  
  15.258 -lemma isnormNum_unique[simp]: 
  15.259 -  assumes na: "isnormNum x" and nb: "isnormNum y" 
  15.260 +lemma isnormNum_unique[simp]:
  15.261 +  assumes na: "isnormNum x" and nb: "isnormNum y"
  15.262    shows "((INum x ::'a::{field_char_0, field_inverse_zero}) = INum y) = (x = y)" (is "?lhs = ?rhs")
  15.263  proof
  15.264 -  have "\<exists> a b a' b'. x = (a,b) \<and> y = (a',b')" by auto
  15.265 -  then obtain a b a' b' where xy[simp]: "x = (a,b)" "y=(a',b')" by blast
  15.266 -  assume H: ?lhs 
  15.267 -  {assume "a = 0 \<or> b = 0 \<or> a' = 0 \<or> b' = 0"
  15.268 +  obtain a b where x: "x = (a, b)" by (cases x)
  15.269 +  obtain a' b' where y: "y = (a', b')" by (cases y)
  15.270 +  assume H: ?lhs
  15.271 +  { assume "a = 0 \<or> b = 0 \<or> a' = 0 \<or> b' = 0"
  15.272      hence ?rhs using na nb H
  15.273 -      by (simp add: INum_def split_def isnormNum_def split: split_if_asm)}
  15.274 +      by (simp add: x y INum_def split_def isnormNum_def split: split_if_asm) }
  15.275    moreover
  15.276    { assume az: "a \<noteq> 0" and bz: "b \<noteq> 0" and a'z: "a'\<noteq>0" and b'z: "b'\<noteq>0"
  15.277 -    from az bz a'z b'z na nb have pos: "b > 0" "b' > 0" by (simp_all add: isnormNum_def)
  15.278 -    from H bz b'z have eq:"a * b' = a'*b" 
  15.279 -      by (simp add: INum_def  eq_divide_eq divide_eq_eq of_int_mult[symmetric] del: of_int_mult)
  15.280 -    from az a'z na nb have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1"       
  15.281 -      by (simp_all add: isnormNum_def add: gcd_commute_int)
  15.282 -    from eq have raw_dvd: "a dvd a'*b" "b dvd b'*a" "a' dvd a*b'" "b' dvd b*a'"
  15.283 -      apply - 
  15.284 +    from az bz a'z b'z na nb have pos: "b > 0" "b' > 0" by (simp_all add: x y isnormNum_def)
  15.285 +    from H bz b'z have eq: "a * b' = a'*b"
  15.286 +      by (simp add: x y INum_def eq_divide_eq divide_eq_eq of_int_mult[symmetric] del: of_int_mult)
  15.287 +    from az a'z na nb have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1"
  15.288 +      by (simp_all add: x y isnormNum_def add: gcd_commute_int)
  15.289 +    from eq have raw_dvd: "a dvd a' * b" "b dvd b' * a" "a' dvd a * b'" "b' dvd b * a'"
  15.290 +      apply -
  15.291        apply algebra
  15.292        apply algebra
  15.293        apply simp
  15.294        apply algebra
  15.295        done
  15.296      from zdvd_antisym_abs[OF coprime_dvd_mult_int[OF gcd1(2) raw_dvd(2)]
  15.297 -      coprime_dvd_mult_int[OF gcd1(4) raw_dvd(4)]]
  15.298 +        coprime_dvd_mult_int[OF gcd1(4) raw_dvd(4)]]
  15.299        have eq1: "b = b'" using pos by arith
  15.300        with eq have "a = a'" using pos by simp
  15.301 -      with eq1 have ?rhs by simp}
  15.302 +      with eq1 have ?rhs by (simp add: x y) }
  15.303    ultimately show ?rhs by blast
  15.304  next
  15.305    assume ?rhs thus ?lhs by simp
  15.306  qed
  15.307  
  15.308  
  15.309 -lemma isnormNum0[simp]: "isnormNum x \<Longrightarrow> (INum x = (0::'a::{field_char_0, field_inverse_zero})) = (x = 0\<^sub>N)"
  15.310 +lemma isnormNum0[simp]:
  15.311 +    "isnormNum x \<Longrightarrow> (INum x = (0::'a::{field_char_0, field_inverse_zero})) = (x = 0\<^sub>N)"
  15.312    unfolding INum_int(2)[symmetric]
  15.313 -  by (rule isnormNum_unique, simp_all)
  15.314 +  by (rule isnormNum_unique) simp_all
  15.315  
  15.316 -lemma of_int_div_aux: "d ~= 0 ==> ((of_int x)::'a::field_char_0) / (of_int d) = 
  15.317 +lemma of_int_div_aux: "d ~= 0 ==> ((of_int x)::'a::field_char_0) / (of_int d) =
  15.318      of_int (x div d) + (of_int (x mod d)) / ((of_int d)::'a)"
  15.319  proof -
  15.320    assume "d ~= 0"
  15.321 @@ -231,7 +204,7 @@
  15.322      by auto
  15.323    then have eq: "of_int x = ?t"
  15.324      by (simp only: of_int_mult[symmetric] of_int_add [symmetric])
  15.325 -  then have "of_int x / of_int d = ?t / of_int d" 
  15.326 +  then have "of_int x / of_int d = ?t / of_int d"
  15.327      using cong[OF refl[of ?f] eq] by simp
  15.328    then show ?thesis by (simp add: add_divide_distrib algebra_simps `d ~= 0`)
  15.329  qed
  15.330 @@ -241,25 +214,26 @@
  15.331    apply (frule of_int_div_aux [of d n, where ?'a = 'a])
  15.332    apply simp
  15.333    apply (simp add: dvd_eq_mod_eq_0)
  15.334 -done
  15.335 +  done
  15.336  
  15.337  
  15.338  lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{field_char_0, field_inverse_zero})"
  15.339 -proof-
  15.340 -  have "\<exists> a b. x = (a,b)" by auto
  15.341 -  then obtain a b where x[simp]: "x = (a,b)" by blast
  15.342 -  {assume "a=0 \<or> b = 0" hence ?thesis
  15.343 -      by (simp add: INum_def normNum_def split_def Let_def)}
  15.344 -  moreover 
  15.345 -  {assume a: "a\<noteq>0" and b: "b\<noteq>0"
  15.346 +proof -
  15.347 +  obtain a b where x: "x = (a, b)" by (cases x)
  15.348 +  { assume "a = 0 \<or> b = 0"
  15.349 +    hence ?thesis by (simp add: x INum_def normNum_def split_def Let_def) }
  15.350 +  moreover
  15.351 +  { assume a: "a \<noteq> 0" and b: "b \<noteq> 0"
  15.352      let ?g = "gcd a b"
  15.353      from a b have g: "?g \<noteq> 0"by simp
  15.354      from of_int_div[OF g, where ?'a = 'a]
  15.355 -    have ?thesis by (auto simp add: INum_def normNum_def split_def Let_def)}
  15.356 +    have ?thesis by (auto simp add: x INum_def normNum_def split_def Let_def) }
  15.357    ultimately show ?thesis by blast
  15.358  qed
  15.359  
  15.360 -lemma INum_normNum_iff: "(INum x ::'a::{field_char_0, field_inverse_zero}) = INum y \<longleftrightarrow> normNum x = normNum y" (is "?lhs = ?rhs")
  15.361 +lemma INum_normNum_iff:
  15.362 +  "(INum x ::'a::{field_char_0, field_inverse_zero}) = INum y \<longleftrightarrow> normNum x = normNum y"
  15.363 +  (is "?lhs = ?rhs")
  15.364  proof -
  15.365    have "normNum x = normNum y \<longleftrightarrow> (INum (normNum x) :: 'a) = INum (normNum y)"
  15.366      by (simp del: normNum)
  15.367 @@ -268,139 +242,157 @@
  15.368  qed
  15.369  
  15.370  lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {field_char_0, field_inverse_zero})"
  15.371 -proof-
  15.372 -let ?z = "0:: 'a"
  15.373 -  have " \<exists> a b. x = (a,b)" " \<exists> a' b'. y = (a',b')" by auto
  15.374 -  then obtain a b a' b' where x[simp]: "x = (a,b)" 
  15.375 -    and y[simp]: "y = (a',b')" by blast
  15.376 -  {assume "a=0 \<or> a'= 0 \<or> b =0 \<or> b' = 0" hence ?thesis 
  15.377 -      apply (cases "a=0",simp_all add: Nadd_def)
  15.378 -      apply (cases "b= 0",simp_all add: INum_def)
  15.379 -       apply (cases "a'= 0",simp_all)
  15.380 -       apply (cases "b'= 0",simp_all)
  15.381 +proof -
  15.382 +  let ?z = "0:: 'a"
  15.383 +  obtain a b where x: "x = (a, b)" by (cases x)
  15.384 +  obtain a' b' where y: "y = (a', b')" by (cases y)
  15.385 +  { assume "a=0 \<or> a'= 0 \<or> b =0 \<or> b' = 0"
  15.386 +    hence ?thesis
  15.387 +      apply (cases "a=0", simp_all add: x y Nadd_def)
  15.388 +      apply (cases "b= 0", simp_all add: INum_def)
  15.389 +       apply (cases "a'= 0", simp_all)
  15.390 +       apply (cases "b'= 0", simp_all)
  15.391         done }
  15.392 -  moreover 
  15.393 -  {assume aa':"a \<noteq> 0" "a'\<noteq> 0" and bb': "b \<noteq> 0" "b' \<noteq> 0" 
  15.394 -    {assume z: "a * b' + b * a' = 0"
  15.395 +  moreover
  15.396 +  { assume aa': "a \<noteq> 0" "a'\<noteq> 0" and bb': "b \<noteq> 0" "b' \<noteq> 0"
  15.397 +    { assume z: "a * b' + b * a' = 0"
  15.398        hence "of_int (a*b' + b*a') / (of_int b* of_int b') = ?z" by simp
  15.399 -      hence "of_int b' * of_int a / (of_int b * of_int b') + of_int b * of_int a' / (of_int b * of_int b') = ?z"  by (simp add:add_divide_distrib) 
  15.400 -      hence th: "of_int a / of_int b + of_int a' / of_int b' = ?z" using bb' aa' by simp 
  15.401 -      from z aa' bb' have ?thesis 
  15.402 -        by (simp add: th Nadd_def normNum_def INum_def split_def)}
  15.403 -    moreover {assume z: "a * b' + b * a' \<noteq> 0"
  15.404 +      hence "of_int b' * of_int a / (of_int b * of_int b') +
  15.405 +          of_int b * of_int a' / (of_int b * of_int b') = ?z"
  15.406 +        by (simp add:add_divide_distrib)
  15.407 +      hence th: "of_int a / of_int b + of_int a' / of_int b' = ?z" using bb' aa'
  15.408 +        by simp
  15.409 +      from z aa' bb' have ?thesis
  15.410 +        by (simp add: x y th Nadd_def normNum_def INum_def split_def) }
  15.411 +    moreover {
  15.412 +      assume z: "a * b' + b * a' \<noteq> 0"
  15.413        let ?g = "gcd (a * b' + b * a') (b*b')"
  15.414        have gz: "?g \<noteq> 0" using z by simp
  15.415        have ?thesis using aa' bb' z gz
  15.416 -        of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a * b' + b * a'" and y="b*b'"]]  of_int_div[where ?'a = 'a,
  15.417 -        OF gz gcd_dvd2_int[where x="a * b' + b * a'" and y="b*b'"]]
  15.418 -        by (simp add: Nadd_def INum_def normNum_def Let_def add_divide_distrib)}
  15.419 -    ultimately have ?thesis using aa' bb' 
  15.420 -      by (simp add: Nadd_def INum_def normNum_def Let_def) }
  15.421 +        of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a * b' + b * a'" and y="b*b'"]]
  15.422 +        of_int_div[where ?'a = 'a, OF gz gcd_dvd2_int[where x="a * b' + b * a'" and y="b*b'"]]
  15.423 +        by (simp add: x y Nadd_def INum_def normNum_def Let_def add_divide_distrib) }
  15.424 +    ultimately have ?thesis using aa' bb'
  15.425 +      by (simp add: x y Nadd_def INum_def normNum_def Let_def) }
  15.426    ultimately show ?thesis by blast
  15.427  qed
  15.428  
  15.429 -lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {field_char_0, field_inverse_zero}) "
  15.430 -proof-
  15.431 +lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {field_char_0, field_inverse_zero})"
  15.432 +proof -
  15.433    let ?z = "0::'a"
  15.434 -  have " \<exists> a b. x = (a,b)" " \<exists> a' b'. y = (a',b')" by auto
  15.435 -  then obtain a b a' b' where x: "x = (a,b)" and y: "y = (a',b')" by blast
  15.436 -  {assume "a=0 \<or> a'= 0 \<or> b = 0 \<or> b' = 0" hence ?thesis 
  15.437 -      apply (cases "a=0",simp_all add: x y Nmul_def INum_def Let_def)
  15.438 -      apply (cases "b=0",simp_all)
  15.439 -      apply (cases "a'=0",simp_all) 
  15.440 +  obtain a b where x: "x = (a, b)" by (cases x)
  15.441 +  obtain a' b' where y: "y = (a', b')" by (cases y)
  15.442 +  { assume "a=0 \<or> a'= 0 \<or> b = 0 \<or> b' = 0"
  15.443 +    hence ?thesis
  15.444 +      apply (cases "a=0", simp_all add: x y Nmul_def INum_def Let_def)
  15.445 +      apply (cases "b=0", simp_all)
  15.446 +      apply (cases "a'=0", simp_all)
  15.447        done }
  15.448    moreover
  15.449 -  {assume z: "a \<noteq> 0" "a' \<noteq> 0" "b \<noteq> 0" "b' \<noteq> 0"
  15.450 +  { assume z: "a \<noteq> 0" "a' \<noteq> 0" "b \<noteq> 0" "b' \<noteq> 0"
  15.451      let ?g="gcd (a*a') (b*b')"
  15.452      have gz: "?g \<noteq> 0" using z by simp
  15.453 -    from z of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a*a'" and y="b*b'"]] 
  15.454 -      of_int_div[where ?'a = 'a , OF gz gcd_dvd2_int[where x="a*a'" and y="b*b'"]] 
  15.455 -    have ?thesis by (simp add: Nmul_def x y Let_def INum_def)}
  15.456 +    from z of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a*a'" and y="b*b'"]]
  15.457 +      of_int_div[where ?'a = 'a , OF gz gcd_dvd2_int[where x="a*a'" and y="b*b'"]]
  15.458 +    have ?thesis by (simp add: Nmul_def x y Let_def INum_def) }
  15.459    ultimately show ?thesis by blast
  15.460  qed
  15.461  
  15.462  lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x ::'a:: field)"
  15.463    by (simp add: Nneg_def split_def INum_def)
  15.464  
  15.465 -lemma Nsub[simp]: shows "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {field_char_0, field_inverse_zero})"
  15.466 -by (simp add: Nsub_def split_def)
  15.467 +lemma Nsub[simp]: "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {field_char_0, field_inverse_zero})"
  15.468 +  by (simp add: Nsub_def split_def)
  15.469  
  15.470  lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: field_inverse_zero) / (INum x)"
  15.471    by (simp add: Ninv_def INum_def split_def)
  15.472  
  15.473 -lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0, field_inverse_zero})" by (simp add: Ndiv_def)
  15.474 +lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0, field_inverse_zero})"
  15.475 +  by (simp add: Ndiv_def)
  15.476  
  15.477 -lemma Nlt0_iff[simp]: assumes nx: "isnormNum x" 
  15.478 -  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})< 0) = 0>\<^sub>N x "
  15.479 -proof-
  15.480 -  have " \<exists> a b. x = (a,b)" by simp
  15.481 -  then obtain a b where x[simp]:"x = (a,b)" by blast
  15.482 -  {assume "a = 0" hence ?thesis by (simp add: Nlt0_def INum_def) }
  15.483 +lemma Nlt0_iff[simp]:
  15.484 +  assumes nx: "isnormNum x"
  15.485 +  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})< 0) = 0>\<^sub>N x"
  15.486 +proof -
  15.487 +  obtain a b where x: "x = (a, b)" by (cases x)
  15.488 +  { assume "a = 0" hence ?thesis by (simp add: x Nlt0_def INum_def) }
  15.489    moreover
  15.490 -  {assume a: "a\<noteq>0" hence b: "(of_int b::'a) > 0" using nx by (simp add: isnormNum_def)
  15.491 +  { assume a: "a \<noteq> 0" hence b: "(of_int b::'a) > 0"
  15.492 +      using nx by (simp add: x isnormNum_def)
  15.493      from pos_divide_less_eq[OF b, where b="of_int a" and a="0::'a"]
  15.494 -    have ?thesis by (simp add: Nlt0_def INum_def)}
  15.495 +    have ?thesis by (simp add: x Nlt0_def INum_def) }
  15.496    ultimately show ?thesis by blast
  15.497  qed
  15.498  
  15.499 -lemma Nle0_iff[simp]:assumes nx: "isnormNum x" 
  15.500 +lemma Nle0_iff[simp]:
  15.501 +  assumes nx: "isnormNum x"
  15.502    shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \<le> 0) = 0\<ge>\<^sub>N x"
  15.503 -proof-
  15.504 -  have " \<exists> a b. x = (a,b)" by simp
  15.505 -  then obtain a b where x[simp]:"x = (a,b)" by blast
  15.506 -  {assume "a = 0" hence ?thesis by (simp add: Nle0_def INum_def) }
  15.507 +proof -
  15.508 +  obtain a b where x: "x = (a, b)" by (cases x)
  15.509 +  { assume "a = 0" hence ?thesis by (simp add: x Nle0_def INum_def) }
  15.510    moreover
  15.511 -  {assume a: "a\<noteq>0" hence b: "(of_int b :: 'a) > 0" using nx by (simp add: isnormNum_def)
  15.512 +  { assume a: "a \<noteq> 0" hence b: "(of_int b :: 'a) > 0"
  15.513 +      using nx by (simp add: x isnormNum_def)
  15.514      from pos_divide_le_eq[OF b, where b="of_int a" and a="0::'a"]
  15.515 -    have ?thesis by (simp add: Nle0_def INum_def)}
  15.516 +    have ?thesis by (simp add: x Nle0_def INum_def) }
  15.517    ultimately show ?thesis by blast
  15.518  qed
  15.519  
  15.520 -lemma Ngt0_iff[simp]:assumes nx: "isnormNum x" shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})> 0) = 0<\<^sub>N x"
  15.521 -proof-
  15.522 -  have " \<exists> a b. x = (a,b)" by simp
  15.523 -  then obtain a b where x[simp]:"x = (a,b)" by blast
  15.524 -  {assume "a = 0" hence ?thesis by (simp add: Ngt0_def INum_def) }
  15.525 +lemma Ngt0_iff[simp]:
  15.526 +  assumes nx: "isnormNum x"
  15.527 +  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})> 0) = 0<\<^sub>N x"
  15.528 +proof -
  15.529 +  obtain a b where x: "x = (a, b)" by (cases x)
  15.530 +  { assume "a = 0" hence ?thesis by (simp add: x Ngt0_def INum_def) }
  15.531    moreover
  15.532 -  {assume a: "a\<noteq>0" hence b: "(of_int b::'a) > 0" using nx by (simp add: isnormNum_def)
  15.533 +  { assume a: "a \<noteq> 0" hence b: "(of_int b::'a) > 0" using nx
  15.534 +      by (simp add: x isnormNum_def)
  15.535      from pos_less_divide_eq[OF b, where b="of_int a" and a="0::'a"]
  15.536 -    have ?thesis by (simp add: Ngt0_def INum_def)}
  15.537 -  ultimately show ?thesis by blast
  15.538 -qed
  15.539 -lemma Nge0_iff[simp]:assumes nx: "isnormNum x" 
  15.540 -  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \<ge> 0) = 0\<le>\<^sub>N x"
  15.541 -proof-
  15.542 -  have " \<exists> a b. x = (a,b)" by simp
  15.543 -  then obtain a b where x[simp]:"x = (a,b)" by blast
  15.544 -  {assume "a = 0" hence ?thesis by (simp add: Nge0_def INum_def) }
  15.545 -  moreover
  15.546 -  {assume a: "a\<noteq>0" hence b: "(of_int b::'a) > 0" using nx by (simp add: isnormNum_def)
  15.547 -    from pos_le_divide_eq[OF b, where b="of_int a" and a="0::'a"]
  15.548 -    have ?thesis by (simp add: Nge0_def INum_def)}
  15.549 +    have ?thesis by (simp add: x Ngt0_def INum_def) }
  15.550    ultimately show ?thesis by blast
  15.551  qed
  15.552  
  15.553 -lemma Nlt_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y"
  15.554 +lemma Nge0_iff[simp]:
  15.555 +  assumes nx: "isnormNum x"
  15.556 +  shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \<ge> 0) = 0\<le>\<^sub>N x"
  15.557 +proof -
  15.558 +  obtain a b where x: "x = (a, b)" by (cases x)
  15.559 +  { assume "a = 0" hence ?thesis by (simp add: x Nge0_def INum_def) }
  15.560 +  moreover
  15.561 +  { assume "a \<noteq> 0" hence b: "(of_int b::'a) > 0" using nx
  15.562 +      by (simp add: x isnormNum_def)
  15.563 +    from pos_le_divide_eq[OF b, where b="of_int a" and a="0::'a"]
  15.564 +    have ?thesis by (simp add: x Nge0_def INum_def) }
  15.565 +  ultimately show ?thesis by blast
  15.566 +qed
  15.567 +
  15.568 +lemma Nlt_iff[simp]:
  15.569 +  assumes nx: "isnormNum x" and ny: "isnormNum y"
  15.570    shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) < INum y) = (x <\<^sub>N y)"
  15.571 -proof-
  15.572 +proof -
  15.573    let ?z = "0::'a"
  15.574 -  have "((INum x ::'a) < INum y) = (INum (x -\<^sub>N y) < ?z)" using nx ny by simp
  15.575 -  also have "\<dots> = (0>\<^sub>N (x -\<^sub>N y))" using Nlt0_iff[OF Nsub_normN[OF ny]] by simp
  15.576 +  have "((INum x ::'a) < INum y) = (INum (x -\<^sub>N y) < ?z)"
  15.577 +    using nx ny by simp
  15.578 +  also have "\<dots> = (0>\<^sub>N (x -\<^sub>N y))"
  15.579 +    using Nlt0_iff[OF Nsub_normN[OF ny]] by simp
  15.580    finally show ?thesis by (simp add: Nlt_def)
  15.581  qed
  15.582  
  15.583 -lemma Nle_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y"
  15.584 +lemma Nle_iff[simp]:
  15.585 +  assumes nx: "isnormNum x" and ny: "isnormNum y"
  15.586    shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})\<le> INum y) = (x \<le>\<^sub>N y)"
  15.587 -proof-
  15.588 -  have "((INum x ::'a) \<le> INum y) = (INum (x -\<^sub>N y) \<le> (0::'a))" using nx ny by simp
  15.589 -  also have "\<dots> = (0\<ge>\<^sub>N (x -\<^sub>N y))" using Nle0_iff[OF Nsub_normN[OF ny]] by simp
  15.590 +proof -
  15.591 +  have "((INum x ::'a) \<le> INum y) = (INum (x -\<^sub>N y) \<le> (0::'a))"
  15.592 +    using nx ny by simp
  15.593 +  also have "\<dots> = (0\<ge>\<^sub>N (x -\<^sub>N y))"
  15.594 +    using Nle0_iff[OF Nsub_normN[OF ny]] by simp
  15.595    finally show ?thesis by (simp add: Nle_def)
  15.596  qed
  15.597  
  15.598  lemma Nadd_commute:
  15.599    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  15.600    shows "x +\<^sub>N y = y +\<^sub>N x"
  15.601 -proof-
  15.602 +proof -
  15.603    have n: "isnormNum (x +\<^sub>N y)" "isnormNum (y +\<^sub>N x)" by simp_all
  15.604    have "(INum (x +\<^sub>N y)::'a) = INum (y +\<^sub>N x)" by simp
  15.605    with isnormNum_unique[OF n] show ?thesis by simp
  15.606 @@ -409,7 +401,7 @@
  15.607  lemma [simp]:
  15.608    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  15.609    shows "(0, b) +\<^sub>N y = normNum y"
  15.610 -    and "(a, 0) +\<^sub>N y = normNum y" 
  15.611 +    and "(a, 0) +\<^sub>N y = normNum y"
  15.612      and "x +\<^sub>N (0, b) = normNum x"
  15.613      and "x +\<^sub>N (a, 0) = normNum x"
  15.614    apply (simp add: Nadd_def split_def)
  15.615 @@ -420,14 +412,13 @@
  15.616  
  15.617  lemma normNum_nilpotent_aux[simp]:
  15.618    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  15.619 -  assumes nx: "isnormNum x" 
  15.620 +  assumes nx: "isnormNum x"
  15.621    shows "normNum x = x"
  15.622 -proof-
  15.623 +proof -
  15.624    let ?a = "normNum x"
  15.625    have n: "isnormNum ?a" by simp
  15.626 -  have th:"INum ?a = (INum x ::'a)" by simp
  15.627 -  with isnormNum_unique[OF n nx]  
  15.628 -  show ?thesis by simp
  15.629 +  have th: "INum ?a = (INum x ::'a)" by simp
  15.630 +  with isnormNum_unique[OF n nx] show ?thesis by simp
  15.631  qed
  15.632  
  15.633  lemma normNum_nilpotent[simp]:
  15.634 @@ -445,7 +436,7 @@
  15.635  lemma Nadd_normNum1[simp]:
  15.636    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  15.637    shows "normNum x +\<^sub>N y = x +\<^sub>N y"
  15.638 -proof-
  15.639 +proof -
  15.640    have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" by simp_all
  15.641    have "INum (normNum x +\<^sub>N y) = INum x + (INum y :: 'a)" by simp
  15.642    also have "\<dots> = INum (x +\<^sub>N y)" by simp
  15.643 @@ -455,7 +446,7 @@
  15.644  lemma Nadd_normNum2[simp]:
  15.645    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  15.646    shows "x +\<^sub>N normNum y = x +\<^sub>N y"
  15.647 -proof-
  15.648 +proof -
  15.649    have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" by simp_all
  15.650    have "INum (x +\<^sub>N normNum y) = INum x + (INum y :: 'a)" by simp
  15.651    also have "\<dots> = INum (x +\<^sub>N y)" by simp
  15.652 @@ -465,7 +456,7 @@
  15.653  lemma Nadd_assoc:
  15.654    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  15.655    shows "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)"
  15.656 -proof-
  15.657 +proof -
  15.658    have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))" by simp_all
  15.659    have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp
  15.660    with isnormNum_unique[OF n] show ?thesis by simp
  15.661 @@ -476,10 +467,10 @@
  15.662  
  15.663  lemma Nmul_assoc:
  15.664    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  15.665 -  assumes nx: "isnormNum x" and ny:"isnormNum y" and nz:"isnormNum z"
  15.666 +  assumes nx: "isnormNum x" and ny: "isnormNum y" and nz: "isnormNum z"
  15.667    shows "x *\<^sub>N y *\<^sub>N z = x *\<^sub>N (y *\<^sub>N z)"
  15.668 -proof-
  15.669 -  from nx ny nz have n: "isnormNum (x *\<^sub>N y *\<^sub>N z)" "isnormNum (x *\<^sub>N (y *\<^sub>N z))" 
  15.670 +proof -
  15.671 +  from nx ny nz have n: "isnormNum (x *\<^sub>N y *\<^sub>N z)" "isnormNum (x *\<^sub>N (y *\<^sub>N z))"
  15.672      by simp_all
  15.673    have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp
  15.674    with isnormNum_unique[OF n] show ?thesis by simp
  15.675 @@ -487,14 +478,15 @@
  15.676  
  15.677  lemma Nsub0:
  15.678    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  15.679 -  assumes x: "isnormNum x" and y:"isnormNum y" shows "(x -\<^sub>N y = 0\<^sub>N) = (x = y)"
  15.680 -proof-
  15.681 -  { fix h :: 'a
  15.682 -    from isnormNum_unique[where 'a = 'a, OF Nsub_normN[OF y], where y="0\<^sub>N"] 
  15.683 -    have "(x -\<^sub>N y = 0\<^sub>N) = (INum (x -\<^sub>N y) = (INum 0\<^sub>N :: 'a)) " by simp
  15.684 -    also have "\<dots> = (INum x = (INum y :: 'a))" by simp
  15.685 -    also have "\<dots> = (x = y)" using x y by simp
  15.686 -    finally show ?thesis . }
  15.687 +  assumes x: "isnormNum x" and y: "isnormNum y"
  15.688 +  shows "x -\<^sub>N y = 0\<^sub>N \<longleftrightarrow> x = y"
  15.689 +proof -
  15.690 +  fix h :: 'a
  15.691 +  from isnormNum_unique[where 'a = 'a, OF Nsub_normN[OF y], where y="0\<^sub>N"]
  15.692 +  have "(x -\<^sub>N y = 0\<^sub>N) = (INum (x -\<^sub>N y) = (INum 0\<^sub>N :: 'a)) " by simp
  15.693 +  also have "\<dots> = (INum x = (INum y :: 'a))" by simp
  15.694 +  also have "\<dots> = (x = y)" using x y by simp
  15.695 +  finally show ?thesis .
  15.696  qed
  15.697  
  15.698  lemma Nmul0[simp]: "c *\<^sub>N 0\<^sub>N = 0\<^sub>N" " 0\<^sub>N *\<^sub>N c = 0\<^sub>N"
  15.699 @@ -502,24 +494,26 @@
  15.700  
  15.701  lemma Nmul_eq0[simp]:
  15.702    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  15.703 -  assumes nx:"isnormNum x" and ny: "isnormNum y"
  15.704 -  shows "(x*\<^sub>N y = 0\<^sub>N) = (x = 0\<^sub>N \<or> y = 0\<^sub>N)"
  15.705 -proof-
  15.706 -  { fix h :: 'a
  15.707 -    have " \<exists> a b a' b'. x = (a,b) \<and> y= (a',b')" by auto
  15.708 -    then obtain a b a' b' where xy[simp]: "x = (a,b)" "y = (a',b')" by blast
  15.709 -    have n0: "isnormNum 0\<^sub>N" by simp
  15.710 -    show ?thesis using nx ny 
  15.711 -      apply (simp only: isnormNum_unique[where ?'a = 'a, OF  Nmul_normN[OF nx ny] n0, symmetric] Nmul[where ?'a = 'a])
  15.712 -      by (simp add: INum_def split_def isnormNum_def split: split_if_asm)
  15.713 -  }
  15.714 +  assumes nx: "isnormNum x" and ny: "isnormNum y"
  15.715 +  shows "x*\<^sub>N y = 0\<^sub>N \<longleftrightarrow> x = 0\<^sub>N \<or> y = 0\<^sub>N"
  15.716 +proof -
  15.717 +  fix h :: 'a
  15.718 +  obtain a b where x: "x = (a, b)" by (cases x)
  15.719 +  obtain a' b' where y: "y = (a', b')" by (cases y)
  15.720 +  have n0: "isnormNum 0\<^sub>N" by simp
  15.721 +  show ?thesis using nx ny
  15.722 +    apply (simp only: isnormNum_unique[where ?'a = 'a, OF  Nmul_normN[OF nx ny] n0, symmetric]
  15.723 +      Nmul[where ?'a = 'a])
  15.724 +    apply (simp add: x y INum_def split_def isnormNum_def split: split_if_asm)
  15.725 +    done
  15.726  qed
  15.727 +
  15.728  lemma Nneg_Nneg[simp]: "~\<^sub>N (~\<^sub>N c) = c"
  15.729    by (simp add: Nneg_def split_def)
  15.730  
  15.731 -lemma Nmul1[simp]: 
  15.732 -  "isnormNum c \<Longrightarrow> 1\<^sub>N *\<^sub>N c = c" 
  15.733 -  "isnormNum c \<Longrightarrow> c *\<^sub>N (1\<^sub>N) = c" 
  15.734 +lemma Nmul1[simp]:
  15.735 +    "isnormNum c \<Longrightarrow> 1\<^sub>N *\<^sub>N c = c"
  15.736 +    "isnormNum c \<Longrightarrow> c *\<^sub>N (1\<^sub>N) = c"
  15.737    apply (simp_all add: Nmul_def Let_def split_def isnormNum_def)
  15.738    apply (cases "fst c = 0", simp_all, cases c, simp_all)+
  15.739    done
    16.1 --- a/src/HOL/Library/Library.thy	Wed Sep 07 17:41:29 2011 -0700
    16.2 +++ b/src/HOL/Library/Library.thy	Wed Sep 07 19:24:28 2011 -0700
    16.3 @@ -55,6 +55,7 @@
    16.4    Ramsey
    16.5    Reflection
    16.6    RBT_Mapping
    16.7 +  Saturated
    16.8    Set_Algebras
    16.9    State_Monad
   16.10    Sum_of_Squares
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/src/HOL/Library/Saturated.thy	Wed Sep 07 19:24:28 2011 -0700
    17.3 @@ -0,0 +1,242 @@
    17.4 +(* Author: Brian Huffman *)
    17.5 +(* Author: Peter Gammie *)
    17.6 +(* Author: Florian Haftmann *)
    17.7 +
    17.8 +header {* Saturated arithmetic *}
    17.9 +
   17.10 +theory Saturated
   17.11 +imports Main "~~/src/HOL/Library/Numeral_Type" "~~/src/HOL/Word/Type_Length"
   17.12 +begin
   17.13 +
   17.14 +subsection {* The type of saturated naturals *}
   17.15 +
   17.16 +typedef (open) ('a::len) sat = "{.. len_of TYPE('a)}"
   17.17 +  morphisms nat_of Abs_sat
   17.18 +  by auto
   17.19 +
   17.20 +lemma sat_eqI:
   17.21 +  "nat_of m = nat_of n \<Longrightarrow> m = n"
   17.22 +  by (simp add: nat_of_inject)
   17.23 +
   17.24 +lemma sat_eq_iff:
   17.25 +  "m = n \<longleftrightarrow> nat_of m = nat_of n"
   17.26 +  by (simp add: nat_of_inject)
   17.27 +
   17.28 +lemma Abs_sa_nat_of [code abstype]:
   17.29 +  "Abs_sat (nat_of n) = n"
   17.30 +  by (fact nat_of_inverse)
   17.31 +
   17.32 +definition Sat :: "nat \<Rightarrow> 'a::len sat" where
   17.33 +  "Sat n = Abs_sat (min (len_of TYPE('a)) n)"
   17.34 +
   17.35 +lemma nat_of_Sat [simp]:
   17.36 +  "nat_of (Sat n :: ('a::len) sat) = min (len_of TYPE('a)) n"
   17.37 +  unfolding Sat_def by (rule Abs_sat_inverse) simp
   17.38 +
   17.39 +lemma nat_of_le_len_of [simp]:
   17.40 +  "nat_of (n :: ('a::len) sat) \<le> len_of TYPE('a)"
   17.41 +  using nat_of [where x = n] by simp
   17.42 +
   17.43 +lemma min_len_of_nat_of [simp]:
   17.44 +  "min (len_of TYPE('a)) (nat_of (n::('a::len) sat)) = nat_of n"
   17.45 +  by (rule min_max.inf_absorb2 [OF nat_of_le_len_of])
   17.46 +
   17.47 +lemma min_nat_of_len_of [simp]:
   17.48 +  "min (nat_of (n::('a::len) sat)) (len_of TYPE('a)) = nat_of n"
   17.49 +  by (subst min_max.inf.commute) simp
   17.50 +
   17.51 +lemma Sat_nat_of [simp]:
   17.52 +  "Sat (nat_of n) = n"
   17.53 +  by (simp add: Sat_def nat_of_inverse)
   17.54 +
   17.55 +instantiation sat :: (len) linorder
   17.56 +begin
   17.57 +
   17.58 +definition
   17.59 +  less_eq_sat_def: "x \<le> y \<longleftrightarrow> nat_of x \<le> nat_of y"
   17.60 +
   17.61 +definition
   17.62 +  less_sat_def: "x < y \<longleftrightarrow> nat_of x < nat_of y"
   17.63 +
   17.64 +instance
   17.65 +by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min_max.le_infI1 nat_mult_commute)
   17.66 +
   17.67 +end
   17.68 +
   17.69 +instantiation sat :: (len) "{minus, comm_semiring_0, comm_semiring_1}"
   17.70 +begin
   17.71 +
   17.72 +definition
   17.73 +  "0 = Sat 0"
   17.74 +
   17.75 +definition
   17.76 +  "1 = Sat 1"
   17.77 +
   17.78 +lemma nat_of_zero_sat [simp, code abstract]:
   17.79 +  "nat_of 0 = 0"
   17.80 +  by (simp add: zero_sat_def)
   17.81 +
   17.82 +lemma nat_of_one_sat [simp, code abstract]:
   17.83 +  "nat_of 1 = min 1 (len_of TYPE('a))"
   17.84 +  by (simp add: one_sat_def)
   17.85 +
   17.86 +definition
   17.87 +  "x + y = Sat (nat_of x + nat_of y)"
   17.88 +
   17.89 +lemma nat_of_plus_sat [simp, code abstract]:
   17.90 +  "nat_of (x + y) = min (nat_of x + nat_of y) (len_of TYPE('a))"
   17.91 +  by (simp add: plus_sat_def)
   17.92 +
   17.93 +definition
   17.94 +  "x - y = Sat (nat_of x - nat_of y)"
   17.95 +
   17.96 +lemma nat_of_minus_sat [simp, code abstract]:
   17.97 +  "nat_of (x - y) = nat_of x - nat_of y"
   17.98 +proof -
   17.99 +  from nat_of_le_len_of [of x] have "nat_of x - nat_of y \<le> len_of TYPE('a)" by arith
  17.100 +  then show ?thesis by (simp add: minus_sat_def)
  17.101 +qed
  17.102 +
  17.103 +definition
  17.104 +  "x * y = Sat (nat_of x * nat_of y)"
  17.105 +
  17.106 +lemma nat_of_times_sat [simp, code abstract]:
  17.107 +  "nat_of (x * y) = min (nat_of x * nat_of y) (len_of TYPE('a))"
  17.108 +  by (simp add: times_sat_def)
  17.109 +
  17.110 +instance proof
  17.111 +  fix a b c :: "('a::len) sat"
  17.112 +  show "a * b * c = a * (b * c)"
  17.113 +  proof(cases "a = 0")
  17.114 +    case True thus ?thesis by (simp add: sat_eq_iff)
  17.115 +  next
  17.116 +    case False show ?thesis
  17.117 +    proof(cases "c = 0")
  17.118 +      case True thus ?thesis by (simp add: sat_eq_iff)
  17.119 +    next
  17.120 +      case False with `a \<noteq> 0` show ?thesis
  17.121 +        by (simp add: sat_eq_iff nat_mult_min_left nat_mult_min_right mult_assoc min_max.inf_assoc min_max.inf_absorb2)
  17.122 +    qed
  17.123 +  qed
  17.124 +next
  17.125 +  fix a :: "('a::len) sat"
  17.126 +  show "1 * a = a"
  17.127 +    apply (simp add: sat_eq_iff)
  17.128 +    apply (metis One_nat_def len_gt_0 less_Suc0 less_zeroE linorder_not_less min_max.le_iff_inf min_nat_of_len_of nat_mult_1_right nat_mult_commute)
  17.129 +    done
  17.130 +next
  17.131 +  fix a b c :: "('a::len) sat"
  17.132 +  show "(a + b) * c = a * c + b * c"
  17.133 +  proof(cases "c = 0")
  17.134 +    case True thus ?thesis by (simp add: sat_eq_iff)
  17.135 +  next
  17.136 +    case False thus ?thesis
  17.137 +      by (simp add: sat_eq_iff nat_mult_min_left add_mult_distrib nat_add_min_left nat_add_min_right min_max.inf_assoc min_max.inf_absorb2)
  17.138 +  qed
  17.139 +qed (simp_all add: sat_eq_iff mult.commute)
  17.140 +
  17.141 +end
  17.142 +
  17.143 +instantiation sat :: (len) ordered_comm_semiring
  17.144 +begin
  17.145 +
  17.146 +instance
  17.147 +by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min_max.le_infI1 nat_mult_commute)
  17.148 +
  17.149 +end
  17.150 +
  17.151 +instantiation sat :: (len) number
  17.152 +begin
  17.153 +
  17.154 +definition
  17.155 +  number_of_sat_def [code del]: "number_of = Sat \<circ> nat"
  17.156 +
  17.157 +instance ..
  17.158 +
  17.159 +end
  17.160 +
  17.161 +lemma [code abstract]:
  17.162 +  "nat_of (number_of n :: ('a::len) sat) = min (nat n) (len_of TYPE('a))"
  17.163 +  unfolding number_of_sat_def by simp
  17.164 +
  17.165 +instance sat :: (len) finite
  17.166 +proof
  17.167 +  show "finite (UNIV::'a sat set)"
  17.168 +    unfolding type_definition.univ [OF type_definition_sat]
  17.169 +    using finite by simp
  17.170 +qed
  17.171 +
  17.172 +instantiation sat :: (len) equal
  17.173 +begin
  17.174 +
  17.175 +definition
  17.176 +  "HOL.equal A B \<longleftrightarrow> nat_of A = nat_of B"
  17.177 +
  17.178 +instance proof
  17.179 +qed (simp add: equal_sat_def nat_of_inject)
  17.180 +
  17.181 +end
  17.182 +
  17.183 +instantiation sat :: (len) "{bounded_lattice, distrib_lattice}"
  17.184 +begin
  17.185 +
  17.186 +definition
  17.187 +  "(inf :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = min"
  17.188 +
  17.189 +definition
  17.190 +  "(sup :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = max"
  17.191 +
  17.192 +definition
  17.193 +  "bot = (0 :: 'a sat)"
  17.194 +
  17.195 +definition
  17.196 +  "top = Sat (len_of TYPE('a))"
  17.197 +
  17.198 +instance proof
  17.199 +qed (simp_all add: inf_sat_def sup_sat_def bot_sat_def top_sat_def min_max.sup_inf_distrib1,
  17.200 +  simp_all add: less_eq_sat_def)
  17.201 +
  17.202 +end
  17.203 +
  17.204 +instantiation sat :: (len) complete_lattice
  17.205 +begin
  17.206 +
  17.207 +definition
  17.208 +  "Inf (A :: 'a sat set) = fold min top A"
  17.209 +
  17.210 +definition
  17.211 +  "Sup (A :: 'a sat set) = fold max bot A"
  17.212 +
  17.213 +instance proof
  17.214 +  fix x :: "'a sat"
  17.215 +  fix A :: "'a sat set"
  17.216 +  note finite
  17.217 +  moreover assume "x \<in> A"
  17.218 +  ultimately have "fold min top A \<le> min x top" by (rule min_max.fold_inf_le_inf)
  17.219 +  then show "Inf A \<le> x" by (simp add: Inf_sat_def)
  17.220 +next
  17.221 +  fix z :: "'a sat"
  17.222 +  fix A :: "'a sat set"
  17.223 +  note finite
  17.224 +  moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> z \<le> x"
  17.225 +  ultimately have "min z top \<le> fold min top A" by (blast intro: min_max.inf_le_fold_inf)
  17.226 +  then show "z \<le> Inf A" by (simp add: Inf_sat_def min_def)
  17.227 +next
  17.228 +  fix x :: "'a sat"
  17.229 +  fix A :: "'a sat set"
  17.230 +  note finite
  17.231 +  moreover assume "x \<in> A"
  17.232 +  ultimately have "max x bot \<le> fold max bot A" by (rule min_max.sup_le_fold_sup)
  17.233 +  then show "x \<le> Sup A" by (simp add: Sup_sat_def)
  17.234 +next
  17.235 +  fix z :: "'a sat"
  17.236 +  fix A :: "'a sat set"
  17.237 +  note finite
  17.238 +  moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
  17.239 +  ultimately have "fold max bot A \<le> max z bot" by (blast intro: min_max.fold_sup_le_sup)
  17.240 +  then show "Sup A \<le> z" by (simp add: Sup_sat_def max_def bot_unique)
  17.241 +qed
  17.242 +
  17.243 +end
  17.244 +
  17.245 +end
    18.1 --- a/src/HOL/Metis_Examples/Type_Encodings.thy	Wed Sep 07 17:41:29 2011 -0700
    18.2 +++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Wed Sep 07 19:24:28 2011 -0700
    18.3 @@ -27,24 +27,32 @@
    18.4     "poly_guards",
    18.5     "poly_guards?",
    18.6     "poly_guards??",
    18.7 +   "poly_guards@?",
    18.8     "poly_guards!",
    18.9     "poly_guards!!",
   18.10 +   "poly_guards@!",
   18.11     "poly_tags",
   18.12     "poly_tags?",
   18.13     "poly_tags??",
   18.14 +   "poly_tags@?",
   18.15     "poly_tags!",
   18.16     "poly_tags!!",
   18.17 +   "poly_tags@!",
   18.18     "poly_args",
   18.19     "raw_mono_guards",
   18.20     "raw_mono_guards?",
   18.21     "raw_mono_guards??",
   18.22 +   "raw_mono_guards@?",
   18.23     "raw_mono_guards!",
   18.24     "raw_mono_guards!!",
   18.25 +   "raw_mono_guards@!",
   18.26     "raw_mono_tags",
   18.27     "raw_mono_tags?",
   18.28     "raw_mono_tags??",
   18.29 +   "raw_mono_tags@?",
   18.30     "raw_mono_tags!",
   18.31     "raw_mono_tags!!",
   18.32 +   "raw_mono_tags@!",
   18.33     "raw_mono_args",
   18.34     "mono_guards",
   18.35     "mono_guards?",
    19.1 --- a/src/HOL/Nat.thy	Wed Sep 07 17:41:29 2011 -0700
    19.2 +++ b/src/HOL/Nat.thy	Wed Sep 07 19:24:28 2011 -0700
    19.3 @@ -657,46 +657,6 @@
    19.4  by (cases m) simp_all
    19.5  
    19.6  
    19.7 -subsubsection {* @{term min} and @{term max} *}
    19.8 -
    19.9 -lemma mono_Suc: "mono Suc"
   19.10 -by (rule monoI) simp
   19.11 -
   19.12 -lemma min_0L [simp]: "min 0 n = (0::nat)"
   19.13 -by (rule min_leastL) simp
   19.14 -
   19.15 -lemma min_0R [simp]: "min n 0 = (0::nat)"
   19.16 -by (rule min_leastR) simp
   19.17 -
   19.18 -lemma min_Suc_Suc [simp]: "min (Suc m) (Suc n) = Suc (min m n)"
   19.19 -by (simp add: mono_Suc min_of_mono)
   19.20 -
   19.21 -lemma min_Suc1:
   19.22 -   "min (Suc n) m = (case m of 0 => 0 | Suc m' => Suc(min n m'))"
   19.23 -by (simp split: nat.split)
   19.24 -
   19.25 -lemma min_Suc2:
   19.26 -   "min m (Suc n) = (case m of 0 => 0 | Suc m' => Suc(min m' n))"
   19.27 -by (simp split: nat.split)
   19.28 -
   19.29 -lemma max_0L [simp]: "max 0 n = (n::nat)"
   19.30 -by (rule max_leastL) simp
   19.31 -
   19.32 -lemma max_0R [simp]: "max n 0 = (n::nat)"
   19.33 -by (rule max_leastR) simp
   19.34 -
   19.35 -lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc(max m n)"
   19.36 -by (simp add: mono_Suc max_of_mono)
   19.37 -
   19.38 -lemma max_Suc1:
   19.39 -   "max (Suc n) m = (case m of 0 => Suc n | Suc m' => Suc(max n m'))"
   19.40 -by (simp split: nat.split)
   19.41 -
   19.42 -lemma max_Suc2:
   19.43 -   "max m (Suc n) = (case m of 0 => Suc n | Suc m' => Suc(max m' n))"
   19.44 -by (simp split: nat.split)
   19.45 -
   19.46 -
   19.47  subsubsection {* Monotonicity of Addition *}
   19.48  
   19.49  lemma Suc_pred [simp]: "n>0 ==> Suc (n - Suc 0) = n"
   19.50 @@ -753,11 +713,85 @@
   19.51    fix a::nat and b::nat show "a ~= 0 \<Longrightarrow> b ~= 0 \<Longrightarrow> a * b ~= 0" by auto
   19.52  qed
   19.53  
   19.54 -lemma nat_mult_1: "(1::nat) * n = n"
   19.55 -by simp
   19.56 +
   19.57 +subsubsection {* @{term min} and @{term max} *}
   19.58 +
   19.59 +lemma mono_Suc: "mono Suc"
   19.60 +by (rule monoI) simp
   19.61 +
   19.62 +lemma min_0L [simp]: "min 0 n = (0::nat)"
   19.63 +by (rule min_leastL) simp
   19.64 +
   19.65 +lemma min_0R [simp]: "min n 0 = (0::nat)"
   19.66 +by (rule min_leastR) simp
   19.67 +
   19.68 +lemma min_Suc_Suc [simp]: "min (Suc m) (Suc n) = Suc (min m n)"
   19.69 +by (simp add: mono_Suc min_of_mono)
   19.70 +
   19.71 +lemma min_Suc1:
   19.72 +   "min (Suc n) m = (case m of 0 => 0 | Suc m' => Suc(min n m'))"
   19.73 +by (simp split: nat.split)
   19.74 +
   19.75 +lemma min_Suc2:
   19.76 +   "min m (Suc n) = (case m of 0 => 0 | Suc m' => Suc(min m' n))"
   19.77 +by (simp split: nat.split)
   19.78 +
   19.79 +lemma max_0L [simp]: "max 0 n = (n::nat)"
   19.80 +by (rule max_leastL) simp
   19.81 +
   19.82 +lemma max_0R [simp]: "max n 0 = (n::nat)"
   19.83 +by (rule max_leastR) simp
   19.84 +
   19.85 +lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc(max m n)"
   19.86 +by (simp add: mono_Suc max_of_mono)
   19.87 +
   19.88 +lemma max_Suc1:
   19.89 +   "max (Suc n) m = (case m of 0 => Suc n | Suc m' => Suc(max n m'))"
   19.90 +by (simp split: nat.split)
   19.91 +
   19.92 +lemma max_Suc2:
   19.93 +   "max m (Suc n) = (case m of 0 => Suc n | Suc m' => Suc(max m' n))"
   19.94 +by (simp split: nat.split)
   19.95  
   19.96 -lemma nat_mult_1_right: "n * (1::nat) = n"
   19.97 -by simp
   19.98 +lemma nat_add_min_left:
   19.99 +  fixes m n q :: nat
  19.100 +  shows "min m n + q = min (m + q) (n + q)"
  19.101 +  by (simp add: min_def)
  19.102 +
  19.103 +lemma nat_add_min_right:
  19.104 +  fixes m n q :: nat
  19.105 +  shows "m + min n q = min (m + n) (m + q)"
  19.106 +  by (simp add: min_def)
  19.107 +
  19.108 +lemma nat_mult_min_left:
  19.109 +  fixes m n q :: nat
  19.110 +  shows "min m n * q = min (m * q) (n * q)"
  19.111 +  by (simp add: min_def not_le) (auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans)
  19.112 +
  19.113 +lemma nat_mult_min_right:
  19.114 +  fixes m n q :: nat
  19.115 +  shows "m * min n q = min (m * n) (m * q)"
  19.116 +  by (simp add: min_def not_le) (auto dest: mult_left_le_imp_le mult_left_less_imp_less le_less_trans)
  19.117 +
  19.118 +lemma nat_add_max_left:
  19.119 +  fixes m n q :: nat
  19.120 +  shows "max m n + q = max (m + q) (n + q)"
  19.121 +  by (simp add: max_def)
  19.122 +
  19.123 +lemma nat_add_max_right:
  19.124 +  fixes m n q :: nat
  19.125 +  shows "m + max n q = max (m + n) (m + q)"
  19.126 +  by (simp add: max_def)
  19.127 +
  19.128 +lemma nat_mult_max_left:
  19.129 +  fixes m n q :: nat
  19.130 +  shows "max m n * q = max (m * q) (n * q)"
  19.131 +  by (simp add: max_def not_le) (auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans)
  19.132 +
  19.133 +lemma nat_mult_max_right:
  19.134 +  fixes m n q :: nat
  19.135 +  shows "m * max n q = max (m * n) (m * q)"
  19.136 +  by (simp add: max_def not_le) (auto dest: mult_left_le_imp_le mult_left_less_imp_less le_less_trans)
  19.137  
  19.138  
  19.139  subsubsection {* Additional theorems about @{term "op \<le>"} *}
  19.140 @@ -1700,6 +1734,15 @@
  19.141  by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
  19.142  
  19.143  
  19.144 +subsection {* aliasses *}
  19.145 +
  19.146 +lemma nat_mult_1: "(1::nat) * n = n"
  19.147 +  by simp
  19.148 + 
  19.149 +lemma nat_mult_1_right: "n * (1::nat) = n"
  19.150 +  by simp
  19.151 +
  19.152 +
  19.153  subsection {* size of a datatype value *}
  19.154  
  19.155  class size =
    20.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 17:41:29 2011 -0700
    20.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 19:24:28 2011 -0700
    20.3 @@ -20,11 +20,11 @@
    20.4  
    20.5    datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
    20.6    datatype soundness = Sound_Modulo_Infiniteness | Sound
    20.7 -  datatype heaviness = Heavy | Ann_Light | Arg_Light
    20.8 +  datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
    20.9    datatype type_level =
   20.10      All_Types |
   20.11 -    Noninf_Nonmono_Types of soundness * heaviness |
   20.12 -    Fin_Nonmono_Types of heaviness |
   20.13 +    Noninf_Nonmono_Types of soundness * granularity |
   20.14 +    Fin_Nonmono_Types of granularity |
   20.15      Const_Arg_Types |
   20.16      No_Types
   20.17    type type_enc
   20.18 @@ -530,11 +530,11 @@
   20.19  datatype order = First_Order | Higher_Order
   20.20  datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
   20.21  datatype soundness = Sound_Modulo_Infiniteness | Sound
   20.22 -datatype heaviness = Heavy | Ann_Light | Arg_Light
   20.23 +datatype granularity = All_Vars | Positively_Naked_Vars | Ghost_Type_Arg_Vars
   20.24  datatype type_level =
   20.25    All_Types |
   20.26 -  Noninf_Nonmono_Types of soundness * heaviness |
   20.27 -  Fin_Nonmono_Types of heaviness |
   20.28 +  Noninf_Nonmono_Types of soundness * granularity |
   20.29 +  Fin_Nonmono_Types of granularity |
   20.30    Const_Arg_Types |
   20.31    No_Types
   20.32  
   20.33 @@ -554,9 +554,9 @@
   20.34    | level_of_type_enc (Guards (_, level)) = level
   20.35    | level_of_type_enc (Tags (_, level)) = level
   20.36  
   20.37 -fun heaviness_of_level (Noninf_Nonmono_Types (_, heaviness)) = heaviness
   20.38 -  | heaviness_of_level (Fin_Nonmono_Types heaviness) = heaviness
   20.39 -  | heaviness_of_level _ = Heavy
   20.40 +fun granularity_of_type_level (Noninf_Nonmono_Types (_, grain)) = grain
   20.41 +  | granularity_of_type_level (Fin_Nonmono_Types grain) = grain
   20.42 +  | granularity_of_type_level _ = All_Vars
   20.43  
   20.44  fun is_type_level_quasi_sound All_Types = true
   20.45    | is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true
   20.46 @@ -584,13 +584,17 @@
   20.47    case try_unsuffixes suffixes s of
   20.48      SOME s =>
   20.49      (case try_unsuffixes suffixes s of
   20.50 -       SOME s => (constr Ann_Light, s)
   20.51 +       SOME s => (constr Positively_Naked_Vars, s)
   20.52       | NONE =>
   20.53         case try_unsuffixes ats s of
   20.54 -         SOME s => (constr Arg_Light, s)
   20.55 -       | NONE => (constr Heavy, s))
   20.56 +         SOME s => (constr Ghost_Type_Arg_Vars, s)
   20.57 +       | NONE => (constr All_Vars, s))
   20.58    | NONE => fallback s
   20.59  
   20.60 +fun is_incompatible_type_level poly level =
   20.61 +  poly = Mangled_Monomorphic andalso
   20.62 +  granularity_of_type_level level = Ghost_Type_Arg_Vars
   20.63 +
   20.64  fun type_enc_from_string soundness s =
   20.65    (case try (unprefix "poly_") s of
   20.66       SOME s => (SOME Polymorphic, s)
   20.67 @@ -611,7 +615,7 @@
   20.68                (Polymorphic, All_Types) =>
   20.69                Simple_Types (First_Order, Polymorphic, All_Types)
   20.70              | (Mangled_Monomorphic, _) =>
   20.71 -              if heaviness_of_level level = Heavy then
   20.72 +              if granularity_of_type_level level = All_Vars then
   20.73                  Simple_Types (First_Order, Mangled_Monomorphic, level)
   20.74                else
   20.75                  raise Same.SAME
   20.76 @@ -622,14 +626,17 @@
   20.77                Simple_Types (Higher_Order, Polymorphic, All_Types)
   20.78              | (_, Noninf_Nonmono_Types _) => raise Same.SAME
   20.79              | (Mangled_Monomorphic, _) =>
   20.80 -              if heaviness_of_level level = Heavy then
   20.81 +              if granularity_of_type_level level = All_Vars then
   20.82                  Simple_Types (Higher_Order, Mangled_Monomorphic, level)
   20.83                else
   20.84                  raise Same.SAME
   20.85              | _ => raise Same.SAME)
   20.86 -         | ("guards", (SOME poly, _)) => Guards (poly, level)
   20.87 -         | ("tags", (SOME Polymorphic, _)) => Tags (Polymorphic, level)
   20.88 -         | ("tags", (SOME poly, _)) => Tags (poly, level)
   20.89 +         | ("guards", (SOME poly, _)) =>
   20.90 +           if is_incompatible_type_level poly level then raise Same.SAME
   20.91 +           else Guards (poly, level)
   20.92 +         | ("tags", (SOME poly, _)) =>
   20.93 +           if is_incompatible_type_level poly level then raise Same.SAME
   20.94 +           else Tags (poly, level)
   20.95           | ("args", (SOME poly, All_Types (* naja *))) =>
   20.96             Guards (poly, Const_Arg_Types)
   20.97           | ("erased", (NONE, All_Types (* naja *))) =>
   20.98 @@ -700,10 +707,6 @@
   20.99    Mangled_Type_Args |
  20.100    No_Type_Args
  20.101  
  20.102 -fun should_drop_arg_type_args (Simple_Types _) = false
  20.103 -  | should_drop_arg_type_args type_enc =
  20.104 -    level_of_type_enc type_enc = All_Types
  20.105 -
  20.106  fun type_arg_policy type_enc s =
  20.107    let val mangled = (polymorphism_of_type_enc type_enc = Mangled_Monomorphic) in
  20.108      if s = type_tag_name then
  20.109 @@ -718,7 +721,9 @@
  20.110          else if mangled then
  20.111            Mangled_Type_Args
  20.112          else
  20.113 -          Explicit_Type_Args (should_drop_arg_type_args type_enc)
  20.114 +          Explicit_Type_Args
  20.115 +              (level = All_Types orelse
  20.116 +               granularity_of_type_level level = Ghost_Type_Arg_Vars)
  20.117        end
  20.118    end
  20.119  
  20.120 @@ -1089,28 +1094,31 @@
  20.121        t
  20.122      else
  20.123        let
  20.124 -        fun aux Ts t =
  20.125 +        fun trans Ts t =
  20.126            case t of
  20.127 -            @{const Not} $ t1 => @{const Not} $ aux Ts t1
  20.128 +            @{const Not} $ t1 => @{const Not} $ trans Ts t1
  20.129            | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
  20.130 -            t0 $ Abs (s, T, aux (T :: Ts) t')
  20.131 +            t0 $ Abs (s, T, trans (T :: Ts) t')
  20.132            | (t0 as Const (@{const_name All}, _)) $ t1 =>
  20.133 -            aux Ts (t0 $ eta_expand Ts t1 1)
  20.134 +            trans Ts (t0 $ eta_expand Ts t1 1)
  20.135            | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
  20.136 -            t0 $ Abs (s, T, aux (T :: Ts) t')
  20.137 +            t0 $ Abs (s, T, trans (T :: Ts) t')
  20.138            | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
  20.139 -            aux Ts (t0 $ eta_expand Ts t1 1)
  20.140 -          | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
  20.141 -          | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
  20.142 -          | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
  20.143 +            trans Ts (t0 $ eta_expand Ts t1 1)
  20.144 +          | (t0 as @{const HOL.conj}) $ t1 $ t2 =>
  20.145 +            t0 $ trans Ts t1 $ trans Ts t2
  20.146 +          | (t0 as @{const HOL.disj}) $ t1 $ t2 =>
  20.147 +            t0 $ trans Ts t1 $ trans Ts t2
  20.148 +          | (t0 as @{const HOL.implies}) $ t1 $ t2 =>
  20.149 +            t0 $ trans Ts t1 $ trans Ts t2
  20.150            | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
  20.151                $ t1 $ t2 =>
  20.152 -            t0 $ aux Ts t1 $ aux Ts t2
  20.153 +            t0 $ trans Ts t1 $ trans Ts t2
  20.154            | _ =>
  20.155              if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
  20.156              else t |> Envir.eta_contract |> do_lambdas ctxt Ts
  20.157          val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
  20.158 -      in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
  20.159 +      in t |> trans [] |> singleton (Variable.export_terms ctxt' ctxt) end
  20.160    end
  20.161  
  20.162  fun do_cheaply_conceal_lambdas Ts (t1 $ t2) =
  20.163 @@ -1148,12 +1156,12 @@
  20.164     same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
  20.165  fun freeze_term t =
  20.166    let
  20.167 -    fun aux (t $ u) = aux t $ aux u
  20.168 -      | aux (Abs (s, T, t)) = Abs (s, T, aux t)
  20.169 -      | aux (Var ((s, i), T)) =
  20.170 +    fun freeze (t $ u) = freeze t $ freeze u
  20.171 +      | freeze (Abs (s, T, t)) = Abs (s, T, freeze t)
  20.172 +      | freeze (Var ((s, i), T)) =
  20.173          Free (atp_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
  20.174 -      | aux t = t
  20.175 -  in t |> exists_subterm is_Var t ? aux end
  20.176 +      | freeze t = t
  20.177 +  in t |> exists_subterm is_Var t ? freeze end
  20.178  
  20.179  fun presimp_prop ctxt presimp_consts t =
  20.180    let
  20.181 @@ -1198,6 +1206,30 @@
  20.182  
  20.183  (** Finite and infinite type inference **)
  20.184  
  20.185 +fun tvar_footprint thy s ary =
  20.186 +  (case strip_prefix_and_unascii const_prefix s of
  20.187 +     SOME s =>
  20.188 +     s |> invert_const |> robust_const_type thy |> chop_fun ary |> fst
  20.189 +       |> map (fn T => Term.add_tvarsT T [] |> map fst)
  20.190 +   | NONE => [])
  20.191 +  handle TYPE _ => []
  20.192 +
  20.193 +fun ghost_type_args thy s ary =
  20.194 +  let
  20.195 +    val footprint = tvar_footprint thy s ary
  20.196 +    fun ghosts _ [] = []
  20.197 +      | ghosts seen ((i, tvars) :: args) =
  20.198 +        ghosts (union (op =) seen tvars) args
  20.199 +        |> exists (not o member (op =) seen) tvars ? cons i
  20.200 +  in
  20.201 +    if forall null footprint then
  20.202 +      []
  20.203 +    else
  20.204 +      0 upto length footprint - 1 ~~ footprint
  20.205 +      |> sort (rev_order o list_ord Term_Ord.indexname_ord o pairself snd)
  20.206 +      |> ghosts []
  20.207 +  end
  20.208 +
  20.209  type monotonicity_info =
  20.210    {maybe_finite_Ts : typ list,
  20.211     surely_finite_Ts : typ list,
  20.212 @@ -1221,23 +1253,25 @@
  20.213  fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true
  20.214    | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
  20.215                               maybe_nonmono_Ts, ...}
  20.216 -                       (Noninf_Nonmono_Types (soundness, _)) T =
  20.217 -    exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
  20.218 -    not (exists (type_instance ctxt T) surely_infinite_Ts orelse
  20.219 -         (not (member (type_aconv ctxt) maybe_finite_Ts T) andalso
  20.220 -          is_type_kind_of_surely_infinite ctxt soundness surely_infinite_Ts T))
  20.221 +                       (Noninf_Nonmono_Types (soundness, grain)) T =
  20.222 +    grain = Ghost_Type_Arg_Vars orelse
  20.223 +    (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
  20.224 +     not (exists (type_instance ctxt T) surely_infinite_Ts orelse
  20.225 +          (not (member (type_aconv ctxt) maybe_finite_Ts T) andalso
  20.226 +           is_type_kind_of_surely_infinite ctxt soundness surely_infinite_Ts
  20.227 +                                           T)))
  20.228    | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
  20.229                               maybe_nonmono_Ts, ...}
  20.230 -                       (Fin_Nonmono_Types _) T =
  20.231 -    exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
  20.232 -    (exists (type_generalization ctxt T) surely_finite_Ts orelse
  20.233 -     (not (member (type_aconv ctxt) maybe_infinite_Ts T) andalso
  20.234 -      is_type_surely_finite ctxt T))
  20.235 +                       (Fin_Nonmono_Types grain) T =
  20.236 +    grain = Ghost_Type_Arg_Vars orelse
  20.237 +    (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
  20.238 +     (exists (type_generalization ctxt T) surely_finite_Ts orelse
  20.239 +      (not (member (type_aconv ctxt) maybe_infinite_Ts T) andalso
  20.240 +       is_type_surely_finite ctxt T)))
  20.241    | should_encode_type _ _ _ _ = false
  20.242  
  20.243  fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T =
  20.244 -    (heaviness_of_level level = Heavy orelse should_guard_var ()) andalso
  20.245 -    should_encode_type ctxt mono level T
  20.246 +    should_guard_var () andalso should_encode_type ctxt mono level T
  20.247    | should_guard_type _ _ _ _ _ = false
  20.248  
  20.249  fun is_maybe_universal_var (IConst ((s, _), _, _)) =
  20.250 @@ -1249,15 +1283,21 @@
  20.251  datatype tag_site =
  20.252    Top_Level of bool option |
  20.253    Eq_Arg of bool option |
  20.254 +  Arg of string * int |
  20.255    Elsewhere
  20.256  
  20.257  fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
  20.258    | should_tag_with_type ctxt mono (Tags (_, level)) site u T =
  20.259 -    (if heaviness_of_level level = Heavy then
  20.260 -       should_encode_type ctxt mono level T
  20.261 -     else case (site, is_maybe_universal_var u) of
  20.262 -       (Eq_Arg _, true) => should_encode_type ctxt mono level T
  20.263 -     | _ => false)
  20.264 +    (case granularity_of_type_level level of
  20.265 +       All_Vars => should_encode_type ctxt mono level T
  20.266 +     | grain =>
  20.267 +       case (site, is_maybe_universal_var u) of
  20.268 +         (Eq_Arg _, true) => should_encode_type ctxt mono level T
  20.269 +       | (Arg (s, j), true) =>
  20.270 +         grain = Ghost_Type_Arg_Vars andalso
  20.271 +         member (op =)
  20.272 +                (ghost_type_args (Proof_Context.theory_of ctxt) s (j + 1)) j
  20.273 +       | _ => false)
  20.274    | should_tag_with_type _ _ _ _ _ _ = false
  20.275  
  20.276  fun fused_type ctxt mono level =
  20.277 @@ -1646,13 +1686,36 @@
  20.278      accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
  20.279    | is_var_positively_naked_in_term _ _ _ _ = true
  20.280  
  20.281 -fun should_guard_var_in_formula pos phi (SOME true) name =
  20.282 -    formula_fold pos (is_var_positively_naked_in_term name) phi false
  20.283 -  | should_guard_var_in_formula _ _ _ _ = true
  20.284 +fun is_var_ghost_type_arg_in_term thy name pos tm accum =
  20.285 +  is_var_positively_naked_in_term name pos tm accum orelse
  20.286 +  let
  20.287 +    val var = ATerm (name, [])
  20.288 +    fun is_nasty_in_term (ATerm (_, [])) = false
  20.289 +      | is_nasty_in_term (ATerm ((s, _), tms)) =
  20.290 +        (member (op =) tms var andalso
  20.291 +         let val ary = length tms in
  20.292 +           case ghost_type_args thy s ary of
  20.293 +             [] => false
  20.294 +           | ghosts =>
  20.295 +             exists (fn (j, tm) => tm = var andalso member (op =) ghosts j)
  20.296 +                    (0 upto length tms - 1 ~~ tms)
  20.297 +         end) orelse
  20.298 +        exists is_nasty_in_term tms
  20.299 +      | is_nasty_in_term _ = true
  20.300 +  in is_nasty_in_term tm end
  20.301 +
  20.302 +fun should_guard_var_in_formula thy level pos phi (SOME true) name =
  20.303 +    (case granularity_of_type_level level of
  20.304 +       All_Vars => true
  20.305 +     | Positively_Naked_Vars =>
  20.306 +       formula_fold pos (is_var_positively_naked_in_term name) phi false
  20.307 +     | Ghost_Type_Arg_Vars =>
  20.308 +       formula_fold pos (is_var_ghost_type_arg_in_term thy name) phi false)
  20.309 +  | should_guard_var_in_formula _ _ _ _ _ _ = true
  20.310  
  20.311  fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false
  20.312    | should_generate_tag_bound_decl ctxt mono (Tags (_, level)) _ T =
  20.313 -    heaviness_of_level level <> Heavy andalso
  20.314 +    granularity_of_type_level level <> All_Vars andalso
  20.315      should_encode_type ctxt mono level T
  20.316    | should_generate_tag_bound_decl _ _ _ _ _ = false
  20.317  
  20.318 @@ -1667,27 +1730,29 @@
  20.319         | _ => raise Fail "unexpected lambda-abstraction")
  20.320  and ho_term_from_iterm ctxt format mono type_enc =
  20.321    let
  20.322 -    fun aux site u =
  20.323 +    fun term site u =
  20.324        let
  20.325          val (head, args) = strip_iterm_comb u
  20.326          val pos =
  20.327            case site of
  20.328              Top_Level pos => pos
  20.329            | Eq_Arg pos => pos
  20.330 -          | Elsewhere => NONE
  20.331 +          | _ => NONE
  20.332          val t =
  20.333            case head of
  20.334              IConst (name as (s, _), _, T_args) =>
  20.335              let
  20.336 -              val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere
  20.337 +              fun arg_site j =
  20.338 +                if is_tptp_equal s then Eq_Arg pos else Arg (s, j)
  20.339              in
  20.340 -              mk_aterm format type_enc name T_args (map (aux arg_site) args)
  20.341 +              mk_aterm format type_enc name T_args
  20.342 +                       (map2 (term o arg_site) (0 upto length args - 1) args)
  20.343              end
  20.344            | IVar (name, _) =>
  20.345 -            mk_aterm format type_enc name [] (map (aux Elsewhere) args)
  20.346 +            mk_aterm format type_enc name [] (map (term Elsewhere) args)
  20.347            | IAbs ((name, T), tm) =>
  20.348              AAbs ((name, ho_type_from_typ format type_enc true 0 T),
  20.349 -                  aux Elsewhere tm)
  20.350 +                  term Elsewhere tm)
  20.351            | IApp _ => raise Fail "impossible \"IApp\""
  20.352          val T = ityp_of u
  20.353        in
  20.354 @@ -1696,18 +1761,20 @@
  20.355                else
  20.356                  I)
  20.357        end
  20.358 -  in aux end
  20.359 +  in term end
  20.360  and formula_from_iformula ctxt format mono type_enc should_guard_var =
  20.361    let
  20.362 +    val thy = Proof_Context.theory_of ctxt
  20.363 +    val level = level_of_type_enc type_enc
  20.364      val do_term = ho_term_from_iterm ctxt format mono type_enc o Top_Level
  20.365      val do_bound_type =
  20.366        case type_enc of
  20.367 -        Simple_Types (_, _, level) => fused_type ctxt mono level 0
  20.368 +        Simple_Types _ => fused_type ctxt mono level 0
  20.369          #> ho_type_from_typ format type_enc false 0 #> SOME
  20.370        | _ => K NONE
  20.371      fun do_out_of_bound_type pos phi universal (name, T) =
  20.372        if should_guard_type ctxt mono type_enc
  20.373 -             (fn () => should_guard_var pos phi universal name) T then
  20.374 +             (fn () => should_guard_var thy level pos phi universal name) T then
  20.375          IVar (name, T)
  20.376          |> type_guard_iterm format type_enc T
  20.377          |> do_term pos |> AAtom |> SOME
  20.378 @@ -1958,9 +2025,12 @@
  20.379  fun add_fact_monotonic_types ctxt mono type_enc =
  20.380    add_iformula_monotonic_types ctxt mono type_enc |> fact_lift
  20.381  fun monotonic_types_for_facts ctxt mono type_enc facts =
  20.382 -  [] |> (polymorphism_of_type_enc type_enc = Polymorphic andalso
  20.383 -         is_type_level_monotonicity_based (level_of_type_enc type_enc))
  20.384 -        ? fold (add_fact_monotonic_types ctxt mono type_enc) facts
  20.385 +  let val level = level_of_type_enc type_enc in
  20.386 +    [] |> (polymorphism_of_type_enc type_enc = Polymorphic andalso
  20.387 +           is_type_level_monotonicity_based level andalso
  20.388 +           granularity_of_type_level level <> Ghost_Type_Arg_Vars)
  20.389 +          ? fold (add_fact_monotonic_types ctxt mono type_enc) facts
  20.390 +  end
  20.391  
  20.392  fun formula_line_for_guards_mono_type ctxt format mono type_enc T =
  20.393    Formula (guards_sym_formula_prefix ^
  20.394 @@ -1970,7 +2040,7 @@
  20.395             |> type_guard_iterm format type_enc T
  20.396             |> AAtom
  20.397             |> formula_from_iformula ctxt format mono type_enc
  20.398 -                                    (K (K (K (K true)))) (SOME true)
  20.399 +                                    (K (K (K (K (K (K true)))))) (SOME true)
  20.400             |> bound_tvars type_enc (atyps_of T)
  20.401             |> close_formula_universally type_enc,
  20.402             isabelle_info introN, NONE)
  20.403 @@ -2023,21 +2093,28 @@
  20.404  fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono type_enc n s
  20.405                                       j (s', T_args, T, _, ary, in_conj) =
  20.406    let
  20.407 +    val thy = Proof_Context.theory_of ctxt
  20.408      val (kind, maybe_negate) =
  20.409        if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
  20.410        else (Axiom, I)
  20.411      val (arg_Ts, res_T) = chop_fun ary T
  20.412 -    val num_args = length arg_Ts
  20.413 -    val bound_names =
  20.414 -      1 upto num_args |> map (`I o make_bound_var o string_of_int)
  20.415 +    val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
  20.416      val bounds =
  20.417        bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
  20.418 -    val sym_needs_arg_types = exists (curry (op =) dummyT) T_args
  20.419 -    fun should_keep_arg_type T =
  20.420 -      sym_needs_arg_types andalso
  20.421 -      should_guard_type ctxt mono type_enc (K true) T
  20.422      val bound_Ts =
  20.423 -      arg_Ts |> map (fn T => if should_keep_arg_type T then SOME T else NONE)
  20.424 +      if exists (curry (op =) dummyT) T_args then
  20.425 +        case level_of_type_enc type_enc of
  20.426 +          All_Types => map SOME arg_Ts
  20.427 +        | level =>
  20.428 +          if granularity_of_type_level level = Ghost_Type_Arg_Vars then
  20.429 +            let val ghosts = ghost_type_args thy s ary in
  20.430 +              map2 (fn j => if member (op =) ghosts j then SOME else K NONE)
  20.431 +                   (0 upto ary - 1) arg_Ts
  20.432 +            end
  20.433 +          else
  20.434 +            replicate ary NONE
  20.435 +      else
  20.436 +        replicate ary NONE
  20.437    in
  20.438      Formula (guards_sym_formula_prefix ^ s ^
  20.439               (if n > 1 then "_" ^ string_of_int j else ""), kind,
  20.440 @@ -2046,16 +2123,19 @@
  20.441               |> type_guard_iterm format type_enc res_T
  20.442               |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
  20.443               |> formula_from_iformula ctxt format mono type_enc
  20.444 -                                      (K (K (K (K true)))) (SOME true)
  20.445 +                                      (K (K (K (K (K (K true)))))) (SOME true)
  20.446               |> n > 1 ? bound_tvars type_enc (atyps_of T)
  20.447               |> close_formula_universally type_enc
  20.448               |> maybe_negate,
  20.449               isabelle_info introN, NONE)
  20.450    end
  20.451  
  20.452 -fun formula_lines_for_nonuniform_tags_sym_decl ctxt format conj_sym_kind mono
  20.453 -        type_enc n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =
  20.454 +fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono type_enc n s
  20.455 +        (j, (s', T_args, T, pred_sym, ary, in_conj)) =
  20.456    let
  20.457 +    val thy = Proof_Context.theory_of ctxt
  20.458 +    val level = level_of_type_enc type_enc
  20.459 +    val grain = granularity_of_type_level level
  20.460      val ident_base =
  20.461        tags_sym_formula_prefix ^ s ^
  20.462        (if n > 1 then "_" ^ string_of_int j else "")
  20.463 @@ -2063,19 +2143,28 @@
  20.464        if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
  20.465        else (Axiom, I)
  20.466      val (arg_Ts, res_T) = chop_fun ary T
  20.467 -    val bound_names =
  20.468 -      1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
  20.469 +    val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
  20.470      val bounds = bound_names |> map (fn name => ATerm (name, []))
  20.471      val cst = mk_aterm format type_enc (s, s') T_args
  20.472      val eq = maybe_negate oo eq_formula type_enc (atyps_of T) pred_sym
  20.473 -    val should_encode =
  20.474 -      should_encode_type ctxt mono (level_of_type_enc type_enc)
  20.475 +    val should_encode = should_encode_type ctxt mono level
  20.476      val tag_with = tag_with_type ctxt format mono type_enc NONE
  20.477      val add_formula_for_res =
  20.478        if should_encode res_T then
  20.479 -        cons (Formula (ident_base ^ "_res", kind,
  20.480 -                       eq (tag_with res_T (cst bounds)) (cst bounds),
  20.481 -                       isabelle_info simpN, NONE))
  20.482 +        let
  20.483 +          val tagged_bounds =
  20.484 +            if grain = Ghost_Type_Arg_Vars then
  20.485 +              let val ghosts = ghost_type_args thy s ary in
  20.486 +                map2 (fn (j, arg_T) => member (op =) ghosts j ? tag_with arg_T)
  20.487 +                     (0 upto ary - 1 ~~ arg_Ts) bounds
  20.488 +              end
  20.489 +            else
  20.490 +              bounds
  20.491 +        in
  20.492 +          cons (Formula (ident_base ^ "_res", kind,
  20.493 +                         eq (tag_with res_T (cst bounds)) (cst tagged_bounds),
  20.494 +                         isabelle_info simpN, NONE))
  20.495 +        end
  20.496        else
  20.497          I
  20.498      fun add_formula_for_arg k =
  20.499 @@ -2093,7 +2182,8 @@
  20.500        end
  20.501    in
  20.502      [] |> not pred_sym ? add_formula_for_res
  20.503 -       |> Config.get ctxt type_tag_arguments
  20.504 +       |> (Config.get ctxt type_tag_arguments andalso
  20.505 +           grain = Positively_Naked_Vars)
  20.506            ? fold add_formula_for_arg (ary - 1 downto 0)
  20.507    end
  20.508  
  20.509 @@ -2127,13 +2217,13 @@
  20.510                                                   type_enc n s)
  20.511      end
  20.512    | Tags (_, level) =>
  20.513 -    if heaviness_of_level level = Heavy then
  20.514 +    if granularity_of_type_level level = All_Vars then
  20.515        []
  20.516      else
  20.517        let val n = length decls in
  20.518          (0 upto n - 1 ~~ decls)
  20.519 -        |> maps (formula_lines_for_nonuniform_tags_sym_decl ctxt format
  20.520 -                     conj_sym_kind mono type_enc n s)
  20.521 +        |> maps (formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono
  20.522 +                                                 type_enc n s)
  20.523        end
  20.524  
  20.525  fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono type_enc
  20.526 @@ -2168,13 +2258,22 @@
  20.527  val conjsN = "Conjectures"
  20.528  val free_typesN = "Type variables"
  20.529  
  20.530 -val explicit_apply = NONE (* for experiments *)
  20.531 +val explicit_apply_threshold = 50
  20.532  
  20.533  fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
  20.534          lambda_trans readable_names preproc hyp_ts concl_t facts =
  20.535    let
  20.536      val thy = Proof_Context.theory_of ctxt
  20.537      val type_enc = type_enc |> adjust_type_enc format
  20.538 +    (* Forcing explicit applications is expensive for polymorphic encodings,
  20.539 +       because it takes only one existential variable ranging over "'a => 'b" to
  20.540 +       ruin everything. Hence we do it only if there are few facts. *)
  20.541 +    val explicit_apply =
  20.542 +      if polymorphism_of_type_enc type_enc <> Polymorphic orelse
  20.543 +         length facts <= explicit_apply_threshold then
  20.544 +        NONE
  20.545 +      else
  20.546 +        SOME false
  20.547      val lambda_trans =
  20.548        if lambda_trans = smartN then
  20.549          if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
    21.1 --- a/src/Pure/PIDE/document.ML	Wed Sep 07 17:41:29 2011 -0700
    21.2 +++ b/src/Pure/PIDE/document.ML	Wed Sep 07 19:24:28 2011 -0700
    21.3 @@ -331,7 +331,6 @@
    21.4    let
    21.5      val is_init = Toplevel.is_init tr;
    21.6      val is_proof = Keyword.is_proof (Toplevel.name_of tr);
    21.7 -    val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof);
    21.8  
    21.9      val _ = Multithreading.interrupted ();
   21.10      val _ = Toplevel.status tr Markup.forked;
   21.11 @@ -343,13 +342,18 @@
   21.12    in
   21.13      (case result of
   21.14        NONE =>
   21.15 -       (if null errs then Exn.interrupt () else ();
   21.16 -        Toplevel.status tr Markup.failed;
   21.17 -        (st, no_print))
   21.18 +        let
   21.19 +          val _ = if null errs then Exn.interrupt () else ();
   21.20 +          val _ = Toplevel.status tr Markup.failed;
   21.21 +        in (st, no_print) end
   21.22      | SOME st' =>
   21.23 -       (Toplevel.status tr Markup.finished;
   21.24 -        proof_status tr st';
   21.25 -        (st', if do_print then print_state tr st' else no_print)))
   21.26 +        let
   21.27 +          val _ = Toplevel.status tr Markup.finished;
   21.28 +          val _ = proof_status tr st';
   21.29 +          val do_print =
   21.30 +            not is_init andalso
   21.31 +              (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
   21.32 +        in (st', if do_print then print_state tr st' else no_print) end)
   21.33    end;
   21.34  
   21.35  end;
    22.1 --- a/src/Pure/PIDE/xml.ML	Wed Sep 07 17:41:29 2011 -0700
    22.2 +++ b/src/Pure/PIDE/xml.ML	Wed Sep 07 19:24:28 2011 -0700
    22.3 @@ -47,6 +47,7 @@
    22.4    val parse_element: string list -> tree * string list
    22.5    val parse_document: string list -> tree * string list
    22.6    val parse: string -> tree
    22.7 +  val cache: unit -> tree -> tree
    22.8    exception XML_ATOM of string
    22.9    exception XML_BODY of body
   22.10    structure Encode: XML_DATA_OPS
   22.11 @@ -228,6 +229,48 @@
   22.12  end;
   22.13  
   22.14  
   22.15 +(** cache for substructural sharing **)
   22.16 +
   22.17 +fun tree_ord tu =
   22.18 +  if pointer_eq tu then EQUAL
   22.19 +  else
   22.20 +    (case tu of
   22.21 +      (Text _, Elem _) => LESS
   22.22 +    | (Elem _, Text _) => GREATER
   22.23 +    | (Text s, Text s') => fast_string_ord (s, s')
   22.24 +    | (Elem e, Elem e') =>
   22.25 +        prod_ord
   22.26 +          (prod_ord fast_string_ord (list_ord (prod_ord fast_string_ord fast_string_ord)))
   22.27 +          (list_ord tree_ord) (e, e'));
   22.28 +
   22.29 +structure Treetab = Table(type key = tree val ord = tree_ord);
   22.30 +
   22.31 +fun cache () =
   22.32 +  let
   22.33 +    val strings = Unsynchronized.ref (Symtab.empty: unit Symtab.table);
   22.34 +    val trees = Unsynchronized.ref (Treetab.empty: unit Treetab.table);
   22.35 +
   22.36 +    fun string s =
   22.37 +      if size s <= 1 then s
   22.38 +      else
   22.39 +        (case Symtab.lookup_key (! strings) s of
   22.40 +          SOME (s', ()) => s'
   22.41 +        | NONE => (Unsynchronized.change strings (Symtab.update (s, ())); s));
   22.42 +
   22.43 +    fun tree t =
   22.44 +      (case Treetab.lookup_key (! trees) t of
   22.45 +        SOME (t', ()) => t'
   22.46 +      | NONE =>
   22.47 +          let
   22.48 +            val t' =
   22.49 +              (case t of
   22.50 +                Elem ((a, ps), b) => Elem ((string a, map (pairself string) ps), map tree b)
   22.51 +              | Text s => Text (string s));
   22.52 +            val _ = Unsynchronized.change trees (Treetab.update (t', ()));
   22.53 +          in t' end);
   22.54 +  in tree end;
   22.55 +
   22.56 +
   22.57  
   22.58  (** XML as data representation language **)
   22.59  
    23.1 --- a/src/Pure/PIDE/xml.scala	Wed Sep 07 17:41:29 2011 -0700
    23.2 +++ b/src/Pure/PIDE/xml.scala	Wed Sep 07 19:24:28 2011 -0700
    23.3 @@ -84,7 +84,8 @@
    23.4    def content(body: Body): Iterator[String] = content_stream(body).iterator
    23.5  
    23.6  
    23.7 -  /* pipe-lined cache for partial sharing */
    23.8 +
    23.9 +  /** cache for partial sharing (weak table) **/
   23.10  
   23.11    class Cache(initial_size: Int = 131071, max_string: Int = 100)
   23.12    {
    24.1 --- a/src/Pure/Syntax/syntax.ML	Wed Sep 07 17:41:29 2011 -0700
    24.2 +++ b/src/Pure/Syntax/syntax.ML	Wed Sep 07 19:24:28 2011 -0700
    24.3 @@ -99,6 +99,7 @@
    24.4    val string_of_sort_global: theory -> sort -> string
    24.5    type syntax
    24.6    val eq_syntax: syntax * syntax -> bool
    24.7 +  val join_syntax: syntax -> unit
    24.8    val lookup_const: syntax -> string -> string option
    24.9    val is_keyword: syntax -> string -> bool
   24.10    val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list
   24.11 @@ -508,6 +509,8 @@
   24.12  
   24.13  fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2;
   24.14  
   24.15 +fun join_syntax (Syntax ({gram, ...}, _)) = ignore (Future.join gram);
   24.16 +
   24.17  fun lookup_const (Syntax ({consts, ...}, _)) = Symtab.lookup consts;
   24.18  fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;
   24.19  fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon;
    25.1 --- a/src/Pure/System/session.scala	Wed Sep 07 17:41:29 2011 -0700
    25.2 +++ b/src/Pure/System/session.scala	Wed Sep 07 19:24:28 2011 -0700
    25.3 @@ -22,7 +22,7 @@
    25.4  
    25.5    //{{{
    25.6    case object Global_Settings
    25.7 -  case object Perspective
    25.8 +  case object Caret_Focus
    25.9    case object Assignment
   25.10    case class Commands_Changed(nodes: Set[Document.Node.Name], commands: Set[Command])
   25.11  
   25.12 @@ -52,7 +52,7 @@
   25.13    /* pervasive event buses */
   25.14  
   25.15    val global_settings = new Event_Bus[Session.Global_Settings.type]
   25.16 -  val perspective = new Event_Bus[Session.Perspective.type]
   25.17 +  val caret_focus = new Event_Bus[Session.Caret_Focus.type]
   25.18    val assignments = new Event_Bus[Session.Assignment.type]
   25.19    val commands_changed = new Event_Bus[Session.Commands_Changed]
   25.20    val phase_changed = new Event_Bus[Session.Phase]
    26.1 --- a/src/Pure/theory.ML	Wed Sep 07 17:41:29 2011 -0700
    26.2 +++ b/src/Pure/theory.ML	Wed Sep 07 19:24:28 2011 -0700
    26.3 @@ -147,6 +147,7 @@
    26.4      |> Sign.local_path
    26.5      |> Sign.map_naming (Name_Space.set_theory_name name)
    26.6      |> apply_wrappers wrappers
    26.7 +    |> tap (Syntax.join_syntax o Sign.syn_of)
    26.8    end;
    26.9  
   26.10  fun end_theory thy =
    27.1 --- a/src/Tools/jEdit/README.html	Wed Sep 07 17:41:29 2011 -0700
    27.2 +++ b/src/Tools/jEdit/README.html	Wed Sep 07 19:24:28 2011 -0700
    27.3 @@ -144,6 +144,11 @@
    27.4    <em>Workaround:</em> Force re-parsing of files using such commands
    27.5    via reload menu of jEdit.</li>
    27.6  
    27.7 +  <li>No way to delete document nodes from the overall collection of
    27.8 +  theories.<br/>
    27.9 +  <em>Workaround:</em> Restart whole Isabelle/jEdit session in
   27.10 +  worst-case situation.</li>
   27.11 +
   27.12    <li>No support for non-local markup, e.g. commands reporting on
   27.13    previous commands (proof end on proof head), or markup produced by
   27.14    loading external files.</li>
    28.1 --- a/src/Tools/jEdit/src/document_view.scala	Wed Sep 07 17:41:29 2011 -0700
    28.2 +++ b/src/Tools/jEdit/src/document_view.scala	Wed Sep 07 19:24:28 2011 -0700
    28.3 @@ -362,7 +362,7 @@
    28.4  
    28.5    private val caret_listener = new CaretListener {
    28.6      private val delay = Swing_Thread.delay_last(session.input_delay) {
    28.7 -      session.perspective.event(Session.Perspective)
    28.8 +      session.caret_focus.event(Session.Caret_Focus)
    28.9      }
   28.10      override def caretUpdate(e: CaretEvent) { delay() }
   28.11    }
    29.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Wed Sep 07 17:41:29 2011 -0700
    29.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Wed Sep 07 19:24:28 2011 -0700
    29.3 @@ -106,7 +106,7 @@
    29.4        react {
    29.5          case Session.Global_Settings => handle_resize()
    29.6          case changed: Session.Commands_Changed => handle_update(Some(changed.commands))
    29.7 -        case Session.Perspective => if (follow_caret && handle_perspective()) handle_update()
    29.8 +        case Session.Caret_Focus => if (follow_caret && handle_perspective()) handle_update()
    29.9          case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
   29.10        }
   29.11      }
   29.12 @@ -116,14 +116,14 @@
   29.13    {
   29.14      Isabelle.session.global_settings += main_actor
   29.15      Isabelle.session.commands_changed += main_actor
   29.16 -    Isabelle.session.perspective += main_actor
   29.17 +    Isabelle.session.caret_focus += main_actor
   29.18    }
   29.19  
   29.20    override def exit()
   29.21    {
   29.22      Isabelle.session.global_settings -= main_actor
   29.23      Isabelle.session.commands_changed -= main_actor
   29.24 -    Isabelle.session.perspective -= main_actor
   29.25 +    Isabelle.session.caret_focus -= main_actor
   29.26    }
   29.27  
   29.28