# HG changeset patch # User wenzelm # Date 1347024528 -7200 # Node ID 38af9102ee753e816f0e1e3029127741d63606fb # Parent 0067d83414c864d8a5f5384df0082cfac070bd23# Parent e5224d887e12b1ec4751a7a693349f4d38e650f1 merged diff -r 0067d83414c8 -r 38af9102ee75 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy --- 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 \ 'a set) = Suc 0" +class cart_one = + assumes UNIV_one: "card (UNIV \ '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 "\P. (\i\UNIV. P i) \ P a" unfolding * by auto hence all:"\P. (\i. P i) \ P a" by auto - fix x y z::"'a^'b::cart_one" note * = less_eq_vec_def less_vec_def all vec_eq_iff - show "x\x" "(x < y) = (x \ y \ \ y \ x)" "x\y \ y\x" unfolding * by(auto simp only:field_simps) - { assume "x\y" "y\z" thus "x\z" unfolding * by(auto simp only:field_simps) } - { assume "x\y" "y\x" thus "x=y" unfolding * by(auto simp only:field_simps) } -qed end +instantiation vec :: (linorder, cart_one) linorder +begin + +instance +proof + obtain a :: 'b where all: "\P. (\i. P i) \ 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 "\P. (\i\UNIV. P i) \ 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 \ x" "(x < y) = (x \ y \ \ y \ x)" "x \ y \ y \ x" by auto + { assume "x\y" "y\z" then show "x\z" by auto } + { assume "x\y" "y\x" then show "x=y" by auto } +qed + +end text{* Constant Vectors *} @@ -1986,12 +2002,21 @@ unfolding simps unfolding *(1)[of "\i x. b$i - x"] *(1)[of "\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 "((\x. vec1 (f x)) has_integral (vec1 k)) {a..b}" -proof- have *:"\p. (\(x, k)\p. content k *\<^sub>R vec1 (f x)) - vec1 k = vec1 ((\(x, k)\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 *: "\p. (\(x, k)\p. content k *\<^sub>R vec1 (f x)) - vec1 k = vec1 ((\(x, k)\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 diff -r 0067d83414c8 -r 38af9102ee75 src/HOL/Multivariate_Analysis/Integration.thy --- 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: "(\x. P x) \ P None \ (\x. P(Some x))" by (metis option.nchotomy) -lemma exists_option: - "(\x. P x) \ P None \ (\x. P(Some x))" +lemma exists_option: "(\x. P x) \ P None \ (\x. P(Some x))" by (metis option.nchotomy) -fun lifted where - "lifted (opp::'a\'a\'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\'a\'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 \ (\x y. opp x y = opp y x) \ (\x y z. opp x (opp y z) = opp (opp x y) z) \ (\x. opp (neutral opp) x = x)" -lemma monoidalI: assumes "\x y. opp x y = opp y x" +lemma monoidalI: + assumes "\x y. opp x y = opp y x" "\x y z. opp x (opp y z) = opp (opp x y) z" "\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 "\y. lifted opp x y = y \ lifted opp y x = y" - thus "x = Some (neutral opp)" apply(induct x) defer +proof - + fix x assume "\y. lifted opp x y = y \ 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: "\f g s. support opp f {} = {}" - "\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))" + "\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))" "\f g s. support opp f (s - {x}) = (support opp f s) - {x}" "\f g s. support opp f (s \ t) = (support opp f s) \ (support opp f t)" "\f g s. support opp f (s \ t) = (support opp f s) \ (support opp f t)" @@ -3989,7 +3996,7 @@ lemma has_integral_spike_set_eq: fixes f::"'n::ordered_euclidean_space \ 'a::banach" assumes "negligible((s - t) \ (t - s))" shows "((f has_integral y) s \ (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 \ 'a::banach" assumes "negligible((s - t) \ (t - s))" "(f has_integral y) s" diff -r 0067d83414c8 -r 38af9102ee75 src/Pure/System/session.scala --- 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) diff -r 0067d83414c8 -r 38af9102ee75 src/Pure/System/swing_thread.scala --- 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) _ diff -r 0067d83414c8 -r 38af9102ee75 src/Tools/jEdit/src/document_model.scala --- 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() } } diff -r 0067d83414c8 -r 38af9102ee75 src/Tools/jEdit/src/document_view.scala --- 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) diff -r 0067d83414c8 -r 38af9102ee75 src/Tools/jEdit/src/output_dockable.scala --- 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() } }) diff -r 0067d83414c8 -r 38af9102ee75 src/Tools/jEdit/src/plugin.scala --- 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