--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Fri Sep 07 14:15:46 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Fri Sep 07 15:28:48 2012 +0200
@@ -57,23 +57,39 @@
text{* The ordering on one-dimensional vectors is linear. *}
-class cart_one = assumes UNIV_one: "card (UNIV \<Colon> 'a set) = Suc 0"
+class cart_one =
+ assumes UNIV_one: "card (UNIV \<Colon> 'a set) = Suc 0"
begin
- subclass finite
- proof from UNIV_one show "finite (UNIV :: 'a set)"
- by (auto intro!: card_ge_0_finite) qed
+
+subclass finite
+proof
+ from UNIV_one show "finite (UNIV :: 'a set)"
+ by (auto intro!: card_ge_0_finite)
+qed
+
end
-instantiation vec :: (linorder,cart_one) linorder begin
-instance proof
- guess a B using UNIV_one[where 'a='b] unfolding card_Suc_eq apply- by(erule exE)+
- hence *:"UNIV = {a}" by auto
- have "\<And>P. (\<forall>i\<in>UNIV. P i) \<longleftrightarrow> P a" unfolding * by auto hence all:"\<And>P. (\<forall>i. P i) \<longleftrightarrow> P a" by auto
- fix x y z::"'a^'b::cart_one" note * = less_eq_vec_def less_vec_def all vec_eq_iff
- show "x\<le>x" "(x < y) = (x \<le> y \<and> \<not> y \<le> x)" "x\<le>y \<or> y\<le>x" unfolding * by(auto simp only:field_simps)
- { assume "x\<le>y" "y\<le>z" thus "x\<le>z" unfolding * by(auto simp only:field_simps) }
- { assume "x\<le>y" "y\<le>x" thus "x=y" unfolding * by(auto simp only:field_simps) }
-qed end
+instantiation vec :: (linorder, cart_one) linorder
+begin
+
+instance
+proof
+ obtain a :: 'b where all: "\<And>P. (\<forall>i. P i) \<longleftrightarrow> P a"
+ proof -
+ have "card (UNIV :: 'b set) = Suc 0" by (rule UNIV_one)
+ then obtain b :: 'b where "UNIV = {b}" by (auto iff: card_Suc_eq)
+ then have "\<And>P. (\<forall>i\<in>UNIV. P i) \<longleftrightarrow> P b" by auto
+ then show thesis by (auto intro: that)
+ qed
+
+ note [simp] = less_eq_vec_def less_vec_def all vec_eq_iff field_simps
+ fix x y z :: "'a^'b::cart_one"
+ show "x \<le> x" "(x < y) = (x \<le> y \<and> \<not> y \<le> x)" "x \<le> y \<or> y \<le> x" by auto
+ { assume "x\<le>y" "y\<le>z" then show "x\<le>z" by auto }
+ { assume "x\<le>y" "y\<le>x" then show "x=y" by auto }
+qed
+
+end
text{* Constant Vectors *}
@@ -1986,12 +2002,21 @@
unfolding simps unfolding *(1)[of "\<lambda>i x. b$i - x"] *(1)[of "\<lambda>i x. x - a$i"] *(2) by(auto)
qed*)
-lemma has_integral_vec1: assumes "(f has_integral k) {a..b}"
+lemma has_integral_vec1:
+ assumes "(f has_integral k) {a..b}"
shows "((\<lambda>x. vec1 (f x)) has_integral (vec1 k)) {a..b}"
-proof- have *:"\<And>p. (\<Sum>(x, k)\<in>p. content k *\<^sub>R vec1 (f x)) - vec1 k = vec1 ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k)"
- unfolding vec_sub vec_eq_iff by(auto simp add: split_beta)
- show ?thesis using assms unfolding has_integral apply safe
- apply(erule_tac x=e in allE,safe) apply(rule_tac x=d in exI,safe)
- apply(erule_tac x=p in allE,safe) unfolding * norm_vector_1 by auto qed
+proof -
+ have *: "\<And>p. (\<Sum>(x, k)\<in>p. content k *\<^sub>R vec1 (f x)) - vec1 k = vec1 ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k)"
+ unfolding vec_sub vec_eq_iff by (auto simp add: split_beta)
+ show ?thesis
+ using assms unfolding has_integral
+ apply safe
+ apply(erule_tac x=e in allE,safe)
+ apply(rule_tac x=d in exI,safe)
+ apply(erule_tac x=p in allE,safe)
+ unfolding * norm_vector_1
+ apply auto
+ done
+qed
end
--- a/src/HOL/Multivariate_Analysis/Integration.thy Fri Sep 07 14:15:46 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Fri Sep 07 15:28:48 2012 +0200
@@ -1771,31 +1771,33 @@
lemma forall_option: "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>x. P(Some x))"
by (metis option.nchotomy)
-lemma exists_option:
- "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P(Some x))"
+lemma exists_option: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P(Some x))"
by (metis option.nchotomy)
-fun lifted where
- "lifted (opp::'a\<Rightarrow>'a\<Rightarrow>'b) (Some x) (Some y) = Some(opp x y)" |
- "lifted opp None _ = (None::'b option)" |
- "lifted opp _ None = None"
+fun lifted
+where
+ "lifted (opp::'a\<Rightarrow>'a\<Rightarrow>'b) (Some x) (Some y) = Some (opp x y)"
+| "lifted opp None _ = (None::'b option)"
+| "lifted opp _ None = None"
lemma lifted_simp_1[simp]: "lifted opp v None = None"
- apply(induct v) by auto
+ by (induct v) auto
definition "monoidal opp \<equiv> (\<forall>x y. opp x y = opp y x) \<and>
(\<forall>x y z. opp x (opp y z) = opp (opp x y) z) \<and>
(\<forall>x. opp (neutral opp) x = x)"
-lemma monoidalI: assumes "\<And>x y. opp x y = opp y x"
+lemma monoidalI:
+ assumes "\<And>x y. opp x y = opp y x"
"\<And>x y z. opp x (opp y z) = opp (opp x y) z"
"\<And>x. opp (neutral opp) x = x" shows "monoidal opp"
unfolding monoidal_def using assms by fastforce
-lemma monoidal_ac: assumes "monoidal opp"
+lemma monoidal_ac:
+ assumes "monoidal opp"
shows "opp (neutral opp) a = a" "opp a (neutral opp) = a" "opp a b = opp b a"
"opp (opp a b) c = opp a (opp b c)" "opp a (opp b c) = opp b (opp a c)"
- using assms unfolding monoidal_def apply- by metis+
+ using assms unfolding monoidal_def by metis+
lemma monoidal_simps[simp]: assumes "monoidal opp"
shows "opp (neutral opp) a = a" "opp a (neutral opp) = a"
@@ -1804,10 +1806,14 @@
lemma neutral_lifted[cong]: assumes "monoidal opp"
shows "neutral (lifted opp) = Some(neutral opp)"
apply(subst neutral_def) apply(rule some_equality) apply(rule,induct_tac y) prefer 3
-proof- fix x assume "\<forall>y. lifted opp x y = y \<and> lifted opp y x = y"
- thus "x = Some (neutral opp)" apply(induct x) defer
+proof -
+ fix x assume "\<forall>y. lifted opp x y = y \<and> lifted opp y x = y"
+ thus "x = Some (neutral opp)"
+ apply(induct x) defer
apply rule apply(subst neutral_def) apply(subst eq_commute,rule some_equality)
- apply(rule,erule_tac x="Some y" in allE) defer apply(erule_tac x="Some x" in allE) by auto
+ apply(rule,erule_tac x="Some y" in allE) defer apply(erule_tac x="Some x" in allE)
+ apply auto
+ done
qed(auto simp add:monoidal_ac[OF assms])
lemma monoidal_lifted[intro]: assumes "monoidal opp" shows "monoidal(lifted opp)"
@@ -1825,7 +1831,8 @@
lemma support_clauses:
"\<And>f g s. support opp f {} = {}"
- "\<And>f g s. support opp f (insert x s) = (if f(x) = neutral opp then support opp f s else insert x (support opp f s))"
+ "\<And>f g s. support opp f (insert x s) =
+ (if f(x) = neutral opp then support opp f s else insert x (support opp f s))"
"\<And>f g s. support opp f (s - {x}) = (support opp f s) - {x}"
"\<And>f g s. support opp f (s \<union> t) = (support opp f s) \<union> (support opp f t)"
"\<And>f g s. support opp f (s \<inter> t) = (support opp f s) \<inter> (support opp f t)"
@@ -3989,7 +3996,7 @@
lemma has_integral_spike_set_eq: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
assumes "negligible((s - t) \<union> (t - s))" shows "((f has_integral y) s \<longleftrightarrow> (f has_integral y) t)"
- unfolding has_integral_restrict_univ[THEN sym,of f] apply(rule has_integral_spike_eq[OF assms]) by (safe, auto split: split_if_asm)
+ unfolding has_integral_restrict_univ[THEN sym,of f] apply(rule has_integral_spike_eq[OF assms]) by (auto split: split_if_asm)
lemma has_integral_spike_set[dest]: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
assumes "negligible((s - t) \<union> (t - s))" "(f has_integral y) s"
--- a/src/Pure/System/session.scala Fri Sep 07 14:15:46 2012 +0200
+++ b/src/Pure/System/session.scala Fri Sep 07 15:28:48 2012 +0200
@@ -24,6 +24,7 @@
//{{{
case object Global_Settings
case object Caret_Focus
+ case class Raw_Edits(edits: List[Document.Edit_Text])
case class Commands_Changed(
assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
@@ -61,6 +62,7 @@
val global_settings = new Event_Bus[Session.Global_Settings.type]
val caret_focus = new Event_Bus[Session.Caret_Focus.type]
+ val raw_edits = new Event_Bus[Session.Raw_Edits]
val commands_changed = new Event_Bus[Session.Commands_Changed]
val phase_changed = new Event_Bus[Session.Phase]
val syslog_messages = new Event_Bus[Isabelle_Process.Output]
@@ -168,7 +170,6 @@
private case class Start(args: List[String])
private case object Cancel_Execution
- private case class Edit(edits: List[Document.Edit_Text])
private case class Change(
doc_edits: List[Document.Edit_Command],
previous: Document.Version,
@@ -391,12 +392,13 @@
case Cancel_Execution if prover.isDefined =>
prover.get.cancel_execution()
- case Edit(edits) if prover.isDefined =>
+ case raw @ Session.Raw_Edits(edits) if prover.isDefined =>
prover.get.discontinue_execution()
val previous = global_state().history.tip.version
val version = Future.promise[Document.Version]
val change = global_state >>> (_.continue_history(previous, edits, version))
+ raw_edits.event(raw)
change_parser ! Text_Edits(previous, edits, version)
reply(())
@@ -435,7 +437,7 @@
def cancel_execution() { session_actor ! Cancel_Execution }
def edit(edits: List[Document.Edit_Text])
- { session_actor !? Edit(edits) }
+ { session_actor !? Session.Raw_Edits(edits) }
def init_node(name: Document.Node.Name,
header: Document.Node.Header, perspective: Text.Perspective, text: String)
--- a/src/Pure/System/swing_thread.scala Fri Sep 07 14:15:46 2012 +0200
+++ b/src/Pure/System/swing_thread.scala Fri Sep 07 15:28:48 2012 +0200
@@ -47,19 +47,47 @@
/* delayed actions */
- private def delayed_action(first: Boolean)(time: Time)(action: => Unit): Boolean => Unit =
+ abstract class Delay extends
{
- val listener = new ActionListener {
- override def actionPerformed(e: ActionEvent) { Swing_Thread.assert(); action }
+ def invoke(): Unit
+ def revoke(): Unit
+ def postpone(time: Time): Unit
+ }
+
+ private def delayed_action(first: Boolean)(time: Time)(action: => Unit): Delay =
+ new Delay {
+ private val timer = new Timer(time.ms.toInt, null)
+ timer.setRepeats(false)
+ timer.addActionListener(new ActionListener {
+ override def actionPerformed(e: ActionEvent) {
+ assert()
+ timer.setDelay(time.ms.toInt)
+ action
+ }
+ })
+
+ def invoke()
+ {
+ require()
+ if (first) timer.start() else timer.restart()
+ }
+
+ def revoke()
+ {
+ require()
+ timer.stop()
+ timer.setDelay(time.ms.toInt)
+ }
+
+ def postpone(alt_time: Time)
+ {
+ require()
+ if (timer.isRunning) {
+ timer.setDelay(timer.getDelay max alt_time.ms.toInt)
+ timer.restart()
+ }
+ }
}
- val timer = new Timer(time.ms.toInt, listener)
- timer.setRepeats(false)
-
- def invoke() { later { if (first) timer.start() else timer.restart() } }
- def revoke() { timer.stop() }
-
- (active: Boolean) => if (active) invoke() else revoke()
- }
// delayed action after first invocation
def delay_first = delayed_action(true) _
--- a/src/Tools/jEdit/src/document_model.scala Fri Sep 07 14:15:46 2012 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Fri Sep 07 15:28:48 2012 +0200
@@ -121,12 +121,12 @@
{
Swing_Thread.require()
pending += edit
- delay_flush(true)
+ delay_flush.invoke()
}
def update_perspective()
{
- delay_flush(true)
+ delay_flush.invoke()
}
def init()
@@ -137,7 +137,7 @@
def exit()
{
- delay_flush(false)
+ delay_flush.revoke()
flush()
}
}
--- a/src/Tools/jEdit/src/document_view.scala Fri Sep 07 14:15:46 2012 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Fri Sep 07 15:28:48 2012 +0200
@@ -346,7 +346,7 @@
}
private val caret_listener = new CaretListener {
- override def caretUpdate(e: CaretEvent) { delay_caret_update(true) }
+ override def caretUpdate(e: CaretEvent) { delay_caret_update.invoke() }
}
@@ -364,6 +364,11 @@
private val main_actor = actor {
loop {
react {
+ case _: Session.Raw_Edits =>
+ Swing_Thread.later {
+ overview.delay_repaint.postpone(Isabelle.session.input_delay)
+ }
+
case changed: Session.Commands_Changed =>
val buffer = model.buffer
Swing_Thread.later {
@@ -374,7 +379,7 @@
if (changed.assignment ||
(changed.nodes.contains(model.name) &&
changed.commands.exists(snapshot.node.commands.contains)))
- overview.delay_repaint(true)
+ Swing_Thread.later { overview.delay_repaint.invoke() }
visible_range() match {
case Some(visible) =>
@@ -422,6 +427,7 @@
painter.addMouseMotionListener(mouse_motion_listener)
text_area.addCaretListener(caret_listener)
text_area.addLeftOfScrollBar(overview)
+ session.raw_edits += main_actor
session.commands_changed += main_actor
session.global_settings += main_actor
}
@@ -429,14 +435,15 @@
private def deactivate()
{
val painter = text_area.getPainter
+ session.raw_edits -= main_actor
session.commands_changed -= main_actor
session.global_settings -= main_actor
text_area.removeFocusListener(focus_listener)
text_area.getView.removeWindowListener(window_listener)
painter.removeMouseMotionListener(mouse_motion_listener)
painter.removeMouseListener(mouse_listener)
- text_area.removeCaretListener(caret_listener); delay_caret_update(false)
- text_area.removeLeftOfScrollBar(overview); overview.delay_repaint(false)
+ text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
+ text_area.removeLeftOfScrollBar(overview); overview.delay_repaint.revoke()
text_area.getGutter.removeExtension(gutter_painter)
text_area_painter.deactivate()
painter.removeExtension(tooltip_painter)
--- a/src/Tools/jEdit/src/output_dockable.scala Fri Sep 07 14:15:46 2012 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Fri Sep 07 15:28:48 2012 +0200
@@ -141,7 +141,7 @@
Isabelle.session.global_settings -= main_actor
Isabelle.session.commands_changed -= main_actor
Isabelle.session.caret_focus -= main_actor
- delay_resize(false)
+ delay_resize.revoke()
}
@@ -151,7 +151,7 @@
Swing_Thread.delay_first(Isabelle.session.update_delay) { handle_resize() }
addComponentListener(new ComponentAdapter {
- override def componentResized(e: ComponentEvent) { delay_resize(true) }
+ override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
})
--- a/src/Tools/jEdit/src/plugin.scala Fri Sep 07 14:15:46 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Fri Sep 07 15:28:48 2012 +0200
@@ -416,11 +416,11 @@
case Session.Ready =>
Isabelle.jedit_buffers.foreach(Isabelle.init_model)
- delay_load(true)
+ Swing_Thread.later { delay_load.invoke() }
case Session.Shutdown =>
Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
- delay_load(false)
+ Swing_Thread.later { delay_load.revoke() }
case _ =>
}
@@ -458,7 +458,7 @@
if (Isabelle.session.is_ready) {
val buffer = msg.getBuffer
if (buffer != null && !buffer.isLoading) Isabelle.init_model(buffer)
- delay_load(true)
+ Swing_Thread.later { delay_load.invoke() }
}
case msg: EditPaneUpdate