# HG changeset patch # User nipkow # Date 1334911624 -7200 # Node ID 148d0b3db78d32ccd08b994220988444c5767d36 # Parent 1568dadd598aede7991345781bfd7cf9e92612ac# Parent 0d3e95375bb72408e5bade135f99041b654ce265 merged diff -r 0d3e95375bb7 -r 148d0b3db78d Admin/isatest/settings/at-poly --- a/Admin/isatest/settings/at-poly Fri Apr 20 10:46:55 2012 +0200 +++ b/Admin/isatest/settings/at-poly Fri Apr 20 10:47:04 2012 +0200 @@ -24,5 +24,6 @@ ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -t true" +init_component "$HOME/contrib_devel/jdk-7u3_x86-linux" init_component "$HOME/contrib_devel/kodkodi-1.2.16" diff -r 0d3e95375bb7 -r 148d0b3db78d Admin/isatest/settings/at-poly-e --- a/Admin/isatest/settings/at-poly-e Fri Apr 20 10:46:55 2012 +0200 +++ b/Admin/isatest/settings/at-poly-e Fri Apr 20 10:47:04 2012 +0200 @@ -24,4 +24,5 @@ ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -t true" +init_component "$HOME/contrib_devel/jdk-7u3_x86-linux" init_component "$HOME/contrib_devel/kodkodi-1.2.16" diff -r 0d3e95375bb7 -r 148d0b3db78d Admin/isatest/settings/at-poly-test --- a/Admin/isatest/settings/at-poly-test Fri Apr 20 10:46:55 2012 +0200 +++ b/Admin/isatest/settings/at-poly-test Fri Apr 20 10:47:04 2012 +0200 @@ -28,4 +28,5 @@ ISABELLE_OCAML="/home/isabelle/contrib_devel/ocaml/x86-linux/ocaml" ISABELLE_SWIPL="/home/isabelle/contrib_devel/swipl/bin/swipl" +init_component "$HOME/contrib_devel/jdk-7u3_x86-linux" init_component "$HOME/contrib_devel/kodkodi-1.2.16" diff -r 0d3e95375bb7 -r 148d0b3db78d Admin/isatest/settings/at64-poly --- a/Admin/isatest/settings/at64-poly Fri Apr 20 10:46:55 2012 +0200 +++ b/Admin/isatest/settings/at64-poly Fri Apr 20 10:47:04 2012 +0200 @@ -24,4 +24,5 @@ ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true" +init_component "$HOME/contrib_devel/jdk-7u3_x86_64-linux" init_component "$HOME/contrib_devel/kodkodi-1.2.16" diff -r 0d3e95375bb7 -r 148d0b3db78d Admin/isatest/settings/cygwin-poly-e --- a/Admin/isatest/settings/cygwin-poly-e Fri Apr 20 10:46:55 2012 +0200 +++ b/Admin/isatest/settings/cygwin-poly-e Fri Apr 20 10:47:04 2012 +0200 @@ -24,4 +24,5 @@ ISABELLE_USEDIR_OPTIONS="-M 1 -i false -d false" +init_component "$HOME/contrib_devel/jdk-7u3_x86-linux" init_component "$HOME/contrib/kodkodi-1.2.16" diff -r 0d3e95375bb7 -r 148d0b3db78d NEWS --- a/NEWS Fri Apr 20 10:46:55 2012 +0200 +++ b/NEWS Fri Apr 20 10:47:04 2012 +0200 @@ -8,6 +8,8 @@ * Prover IDE (PIDE) improvements: + - more robust Sledgehammer integration (as before the sledgehammer + command line needs to be typed into the source buffer) - markup for bound variables - markup for types of term variables (e.g. displayed as tooltips) - support for user-defined Isar commands within the running session @@ -475,6 +477,15 @@ unionwk_is_rbt -> rbt_unionwk_is_rbt unionwk_sorted -> rbt_unionwk_rbt_sorted +* Theory HOL/Library/Float: Floating point numbers are now defined as a +subset of the real numbers. All operations are defined using the +lifing-framework and most proofs use the transfer method. +INCOMPATIBILITY. + + Changed Operations: + scale ~> exponent + pow2 x ~> use "2 powr (real x)" + * Session HOL-Word: Discontinued many redundant theorems specific to type 'a word. INCOMPATIBILITY, use the corresponding generic theorems instead. diff -r 0d3e95375bb7 -r 148d0b3db78d doc-src/IsarRef/style.sty --- a/doc-src/IsarRef/style.sty Fri Apr 20 10:46:55 2012 +0200 +++ b/doc-src/IsarRef/style.sty Fri Apr 20 10:47:04 2012 +0200 @@ -13,16 +13,18 @@ \newcommand{\figref}[1]{figure~\ref{#1}} \newcommand{\Figref}[1]{Figure~\ref{#1}} +%% Isar +\newcommand{\isasymBBAR}{{\,\newdimen{\tmpheight}\settoheight\tmpheight{\isacharbar}\rule{1pt}{\tmpheight}\,}} +\isafoldtag{noproof}\def\isafoldnoproof{~\isafold{proof}} +\newcommand{\isadigitreset}{\def\isadigit##1{##1}} +\renewcommand{\isacommand}[1]{\isakeyword{\isadigitreset#1}} + %% ML \newenvironment{mldecls}{\par\noindent\begingroup\def\isanewline{\\}\begin{tabular}{ll}}{\end{tabular}\medskip\endgroup} -\renewcommand{\isatagML}{\begingroup\isabellestyle{default}\isastyle\def\isadigit##1{##1}} +\renewcommand{\isatagML}{\begingroup\isabellestyle{default}\isastyle\isadigitreset} \renewcommand{\endisatagML}{\endgroup} -%% Isar -\newcommand{\isasymBBAR}{{\,\newdimen{\tmpheight}\settoheight\tmpheight{\isacharbar}\rule{1pt}{\tmpheight}\,}} -\isafoldtag{noproof}\def\isafoldnoproof{~\isafold{proof}} - %% math \newcommand{\isasymstrut}{\isamath{\mathstrut}} \newcommand{\isasymvartheta}{\isamath{\,\theta}} diff -r 0d3e95375bb7 -r 148d0b3db78d src/HOL/Library/Float.thy --- a/src/HOL/Library/Float.thy Fri Apr 20 10:46:55 2012 +0200 +++ b/src/HOL/Library/Float.thy Fri Apr 20 10:47:04 2012 +0200 @@ -1,3 +1,8 @@ +(* Title: HOL/Library/Float.thy + Author: Johannes Hölzl, Fabian Immler + Copyright 2012 TU München +*) + header {* Floating-Point Numbers *} theory Float @@ -614,7 +619,7 @@ show ?thesis proof cases assume "2^nat (-(p + e)) dvd m" - with `p + e < 0` twopow_rewrite show ?thesis unfolding Let_def + with `p + e < 0` twopow_rewrite show ?thesis by transfer (auto simp: ac_simps round_up_def floor_divide_eq_div dvd_eq_mod_eq_0) next assume ndvd: "\ 2 ^ nat (- (p + e)) dvd m" @@ -626,7 +631,6 @@ using ndvd unfolding powr_rewrite one_div by (subst ceil_divide_floor_conv) (auto simp: field_simps) thus ?thesis using `p + e < 0` twopow_rewrite - unfolding Let_def by transfer (auto simp: ac_simps round_up_def floor_divide_eq_div[symmetric]) qed next @@ -636,7 +640,6 @@ by (auto simp add: ac_simps powr_add[symmetric] r1 powr_realpow intro: exI[where x="m*2^nat (e+p)"]) then show ?thesis using `\ p + e < 0` - unfolding Let_def by transfer (simp add: round_up_def floor_divide_eq_div field_simps powr_add powr_minus inverse_eq_divide) qed @@ -846,9 +849,9 @@ l = rat_precision prec x y; d = if 0 \ l then x * 2^nat l div y else x div 2^nat (- l) div y in normfloat (Float d (- l)))" - unfolding div_mult_twopow_eq Let_def normfloat_def + unfolding div_mult_twopow_eq normfloat_def by transfer - (simp add: round_down_def powr_int real_div_nat_eq_floor_of_divide field_simps + (simp add: round_down_def powr_int real_div_nat_eq_floor_of_divide field_simps Let_def del: two_powr_minus_int_float) lift_definition rapprox_posrat :: "nat \ nat \ nat \ float" @@ -865,7 +868,7 @@ m = fst X mod snd X in normfloat (Float (d + (if m = 0 \ y = 0 then 0 else 1)) (- l)))" proof (cases "y = 0") - assume "y = 0" thus ?thesis unfolding Let_def normfloat_def by transfer simp + assume "y = 0" thus ?thesis unfolding normfloat_def by transfer simp next assume "y \ 0" show ?thesis @@ -876,7 +879,7 @@ moreover have "real x * 2 powr real l = real x'" by (simp add: powr_realpow[symmetric] `0 \ l` x'_def) ultimately show ?thesis - unfolding Let_def normfloat_def + unfolding normfloat_def using ceil_divide_floor_conv[of y x'] powr_realpow[of 2 "nat l"] `0 \ l` `y \ 0` l_def[symmetric, THEN meta_eq_to_obj_eq] by transfer @@ -890,7 +893,7 @@ using `\ 0 \ l` by (simp add: powr_realpow[symmetric] powr_minus y'_def field_simps inverse_eq_divide) ultimately show ?thesis - unfolding Let_def normfloat_def + unfolding normfloat_def using ceil_divide_floor_conv[of y' x] `\ 0 \ l` `y' \ 0` `y \ 0` l_def[symmetric, THEN meta_eq_to_obj_eq] by transfer @@ -1206,7 +1209,6 @@ if 0 < d then let P = 2^nat d ; n = m div P in Float n (e + d) else Float m e)" using compute_float_down[of "prec - bitlen \m\ - e" m e, symmetric] - unfolding Let_def by transfer (simp add: field_simps abs_mult log_mult bitlen_def cong del: if_weak_cong) lemma compute_float_round_up[code]: diff -r 0d3e95375bb7 -r 148d0b3db78d src/HOL/Tools/transfer.ML --- a/src/HOL/Tools/transfer.ML Fri Apr 20 10:46:55 2012 +0200 +++ b/src/HOL/Tools/transfer.ML Fri Apr 20 10:47:04 2012 +0200 @@ -86,8 +86,7 @@ Conv.implies_conv Conv.all_conv (correspond_conv ctxt) else_conv Trueprop_conv - (Conv.combination_conv - (Conv.combination_conv Rel_conv (fo_conv ctxt)) (fo_conv ctxt)) + (Conv.combination_conv (Conv.fun_conv Rel_conv) (fo_conv ctxt)) else_conv Conv.all_conv) ct @@ -156,8 +155,11 @@ in EVERY [CONVERSION (correspond_conv ctxt) i, + rtac @{thm correspondence_start} i, REPEAT_ALL_NEW - (resolve_tac rules ORELSE' atac ORELSE' eq_tac ctxt) i] + (resolve_tac rules ORELSE' atac ORELSE' eq_tac ctxt) (i+1), + rewrite_goal_tac @{thms App_def Abs_def} i, + rtac @{thm refl} i] end val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) => diff -r 0d3e95375bb7 -r 148d0b3db78d src/HOL/Transfer.thy --- a/src/HOL/Transfer.thy Fri Apr 20 10:46:55 2012 +0200 +++ b/src/HOL/Transfer.thy Fri Apr 20 10:47:04 2012 +0200 @@ -81,6 +81,9 @@ lemma transfer_start': "\Rel (op \) P Q; P\ \ Q" unfolding Rel_def by simp +lemma correspondence_start: "\x = x'; Rel R x' y\ \ Rel R x y" + by simp + lemma Rel_eq_refl: "Rel (op =) x x" unfolding Rel_def .. diff -r 0d3e95375bb7 -r 148d0b3db78d src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Fri Apr 20 10:46:55 2012 +0200 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Fri Apr 20 10:47:04 2012 +0200 @@ -13,13 +13,15 @@ import scala.collection.Set import scala.collection.immutable.TreeSet +import java.awt.Component import javax.swing.tree.DefaultMutableTreeNode import javax.swing.text.Position -import javax.swing.Icon +import javax.swing.{Icon, DefaultListCellRenderer, ListCellRenderer, JList} import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View} import errorlist.DefaultErrorSource -import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset} +import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, + SideKickCompletionPopup, IAsset} object Isabelle_Sidekick @@ -101,8 +103,27 @@ cs.map(Symbol.decode(_)).sorted else cs).filter(_ != word) if (ds.isEmpty) null - else new SideKickCompletion( - pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { } + else + new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { + /* FIXME Java 7 only + override def getRenderer() = + new ListCellRenderer[Any] { + val default_renderer = + (new DefaultListCellRenderer).asInstanceOf[ListCellRenderer[Any]] + + override def getListCellRendererComponent( + list: JList[_ <: Any], value: Any, index: Int, + selected: Boolean, focus: Boolean): Component = + { + val renderer: Component = + default_renderer.getListCellRendererComponent( + list, value, index, selected, focus) + renderer.setFont(pane.getTextArea.getPainter.getFont) + renderer + } + } + */ + } } } } diff -r 0d3e95375bb7 -r 148d0b3db78d src/Tools/jEdit/src/jEdit.props --- a/src/Tools/jEdit/src/jEdit.props Fri Apr 20 10:46:55 2012 +0200 +++ b/src/Tools/jEdit/src/jEdit.props Fri Apr 20 10:47:04 2012 +0200 @@ -191,8 +191,12 @@ restore.remote=false restore=false sidekick-tree.dock-position=right +sidekick.auto-complete-popup-get-focus=true sidekick.buffer-save-parse=true sidekick.complete-delay=300 +sidekick.complete-instant.toggle=false +sidekick.complete-popup.accept-characters=\\n\\t +sidekick.complete-popup.insert-characters= sidekick.splitter.location=721 tip.show=false twoStageSave=false diff -r 0d3e95375bb7 -r 148d0b3db78d src/Tools/jEdit/src/output_dockable.scala --- a/src/Tools/jEdit/src/output_dockable.scala Fri Apr 20 10:46:55 2012 +0200 +++ b/src/Tools/jEdit/src/output_dockable.scala Fri Apr 20 10:47:04 2012 +0200 @@ -44,10 +44,12 @@ snapshot.node.command_start(cmd) match { case Some(start) if !snapshot.is_outdated => val text = Pretty.string_of(sendback) - buffer.beginCompoundEdit() - buffer.remove(start, cmd.proper_range.length) - buffer.insert(start, text) - buffer.endCompoundEdit() + try { + buffer.beginCompoundEdit() + buffer.remove(start, cmd.proper_range.length) + buffer.insert(start, text) + } + finally { buffer.endCompoundEdit() } case _ => } case None => diff -r 0d3e95375bb7 -r 148d0b3db78d src/Tools/jEdit/src/session_dockable.scala --- a/src/Tools/jEdit/src/session_dockable.scala Fri Apr 20 10:46:55 2012 +0200 +++ b/src/Tools/jEdit/src/session_dockable.scala Fri Apr 20 10:47:04 2012 +0200 @@ -16,7 +16,7 @@ import java.lang.System import java.awt.{BorderLayout, Graphics2D, Insets} -import javax.swing.{JList, DefaultListCellRenderer, BorderFactory} +import javax.swing.{JList, BorderFactory} import javax.swing.border.{BevelBorder, SoftBevelBorder} import org.gjt.sp.jedit.{View, jEdit}