--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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.
--- 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}}
--- 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: "\<not> 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 `\<not> 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 \<le> 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 \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float"
@@ -865,7 +868,7 @@
m = fst X mod snd X
in normfloat (Float (d + (if m = 0 \<or> 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 \<noteq> 0"
show ?thesis
@@ -876,7 +879,7 @@
moreover have "real x * 2 powr real l = real x'"
by (simp add: powr_realpow[symmetric] `0 \<le> 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 \<le> l` `y \<noteq> 0`
l_def[symmetric, THEN meta_eq_to_obj_eq]
by transfer
@@ -890,7 +893,7 @@
using `\<not> 0 \<le> 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] `\<not> 0 \<le> l` `y' \<noteq> 0` `y \<noteq> 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 \<bar>m\<bar> - 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]:
--- 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) =>
--- 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': "\<lbrakk>Rel (op \<longrightarrow>) P Q; P\<rbrakk> \<Longrightarrow> Q"
unfolding Rel_def by simp
+lemma correspondence_start: "\<lbrakk>x = x'; Rel R x' y\<rbrakk> \<Longrightarrow> Rel R x y"
+ by simp
+
lemma Rel_eq_refl: "Rel (op =) x x"
unfolding Rel_def ..
--- 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
+ }
+ }
+ */
+ }
}
}
}
--- 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
--- 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 =>
--- 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}