--- a/src/HOL/Bit_Operations.thy Wed Nov 29 19:45:54 2023 +0100
+++ b/src/HOL/Bit_Operations.thy Wed Nov 29 21:29:00 2023 +0100
@@ -652,43 +652,6 @@
\<open>possible_bit TYPE(int) n\<close>
by (simp add: possible_bit_def)
-lemma bit_not_int_iff':
- \<open>bit (- k - 1) n \<longleftrightarrow> \<not> bit k n\<close> for k :: int
-proof (induction n arbitrary: k)
- case 0
- show ?case
- by (simp add: bit_0)
-next
- case (Suc n)
- have \<open>- k - 1 = - (k + 2) + 1\<close>
- by simp
- also have \<open>(- (k + 2) + 1) div 2 = - (k div 2) - 1\<close>
- proof (cases \<open>even k\<close>)
- case True
- then have \<open>- k div 2 = - (k div 2)\<close>
- by rule (simp flip: mult_minus_right)
- with True show ?thesis
- by simp
- next
- case False
- have \<open>4 = 2 * (2::int)\<close>
- by simp
- also have \<open>2 * 2 div 2 = (2::int)\<close>
- by (simp only: nonzero_mult_div_cancel_left)
- finally have *: \<open>4 div 2 = (2::int)\<close> .
- from False obtain l where k: \<open>k = 2 * l + 1\<close> ..
- then have \<open>- k - 2 = 2 * - (l + 2) + 1\<close>
- by simp
- then have \<open>(- k - 2) div 2 + 1 = - (k div 2) - 1\<close>
- by (simp flip: mult_minus_right add: *) (simp add: k)
- with False show ?thesis
- by simp
- qed
- finally have \<open>(- k - 1) div 2 = - (k div 2) - 1\<close> .
- with Suc show ?case
- by (simp add: bit_Suc)
-qed
-
lemma bit_nat_iff [bit_simps]:
\<open>bit (nat k) n \<longleftrightarrow> k \<ge> 0 \<and> bit k n\<close>
proof (cases \<open>k \<ge> 0\<close>)
@@ -1353,8 +1316,7 @@
class ring_bit_operations = semiring_bit_operations + ring_parity +
fixes not :: \<open>'a \<Rightarrow> 'a\<close> (\<open>NOT\<close>)
- assumes not_rec: \<open>NOT a = of_bool (even a) + 2 * NOT (a div 2)\<close>
- assumes minus_eq_not_minus_1: \<open>- a = NOT (a - 1)\<close>
+ assumes not_eq_complement: \<open>NOT a = - a - 1\<close>
begin
text \<open>
@@ -1368,17 +1330,21 @@
\<open>(- 1) mod 2 = 1\<close>
by (simp add: mod_2_eq_odd)
-lemma not_eq_complement:
- \<open>NOT a = - a - 1\<close>
- using minus_eq_not_minus_1 [of \<open>a + 1\<close>] by simp
-
lemma minus_eq_not_plus_1:
\<open>- a = NOT a + 1\<close>
using not_eq_complement [of a] by simp
+lemma minus_eq_not_minus_1:
+ \<open>- a = NOT (a - 1)\<close>
+ using not_eq_complement [of \<open>a - 1\<close>] by simp (simp add: algebra_simps)
+
+lemma not_rec:
+ \<open>NOT a = of_bool (even a) + 2 * NOT (a div 2)\<close>
+ by (simp add: not_eq_complement algebra_simps mod_2_eq_odd flip: minus_mod_eq_mult_div)
+
lemma even_not_iff [simp]:
\<open>even (NOT a) \<longleftrightarrow> odd a\<close>
- by (simp add: not_rec [of a])
+ by (simp add: not_eq_complement)
lemma bit_not_iff [bit_simps]:
\<open>bit (NOT a) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> \<not> bit a n\<close>
@@ -1822,17 +1788,24 @@
definition flip_bit_int :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close>
where \<open>flip_bit n k = k XOR push_bit n 1\<close> for k :: int
+lemma not_int_div_2:
+ \<open>NOT k div 2 = NOT (k div 2)\<close> for k :: int
+ by (simp add: not_int_def)
+
lemma bit_not_int_iff:
- \<open>bit (NOT k) n \<longleftrightarrow> \<not> bit k n\<close>
- for k :: int
- by (simp add: bit_not_int_iff' not_int_def)
+ \<open>bit (NOT k) n \<longleftrightarrow> \<not> bit k n\<close> for k :: int
+proof (rule sym, induction n arbitrary: k)
+ case 0
+ then show ?case
+ by (simp add: bit_0 not_int_def)
+next
+ case (Suc n)
+ then show ?case
+ by (simp add: bit_Suc not_int_div_2)
+qed
instance proof
fix k l :: int and m n :: nat
- show \<open>- k = NOT (k - 1)\<close>
- by (simp add: not_int_def)
- show \<open>NOT k = of_bool (even k) + 2 * NOT (k div 2)\<close>
- by (auto simp add: not_int_def elim: oddE)
show \<open>unset_bit 0 k = 2 * (k div 2)\<close>
by (rule bit_eqI)
(auto simp add: unset_bit_int_def push_bit_int_def and_int.bit_iff bit_not_int_iff bit_simps simp flip: bit_Suc)
@@ -1840,7 +1813,7 @@
by (rule bit_eqI)
(auto simp add: unset_bit_int_def push_bit_int_def and_int.bit_iff bit_not_int_iff bit_simps mod_2_eq_odd even_bit_succ_iff bit_0 simp flip: bit_Suc)
qed (fact and_int.rec or_int.rec xor_int.rec mask_int_def set_bit_int_def flip_bit_int_def
- push_bit_int_def drop_bit_int_def take_bit_int_def)+
+ push_bit_int_def drop_bit_int_def take_bit_int_def not_int_def)+
end
@@ -1929,10 +1902,6 @@
end
-lemma not_int_div_2:
- \<open>NOT k div 2 = NOT (k div 2)\<close> for k :: int
- by (simp add: not_int_def)
-
lemma take_bit_int_less_exp [simp]:
\<open>take_bit n k < 2 ^ n\<close> for k :: int
by (simp add: take_bit_eq_mod)
@@ -3850,6 +3819,10 @@
\<open>bit (push_bit m k) n \<longleftrightarrow> m \<le> n \<and> bit k (n - m)\<close> for k :: int
by (fact bit_push_bit_iff')
+lemma bit_not_int_iff':
+ \<open>bit (- k - 1) n \<longleftrightarrow> \<not> bit k n\<close> for k :: int
+ by (simp flip: not_eq_complement add: bit_simps)
+
no_notation
not (\<open>NOT\<close>)
and "and" (infixr \<open>AND\<close> 64)
--- a/src/HOL/Code_Numeral.thy Wed Nov 29 19:45:54 2023 +0100
+++ b/src/HOL/Code_Numeral.thy Wed Nov 29 21:29:00 2023 +0100
@@ -352,8 +352,8 @@
bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq
even_mask_div_iff even_mult_exp_div_exp_iff
- and_rec or_rec xor_rec mask_eq_exp_minus_1 not_rec
- set_bit_def unset_bit_0 unset_bit_Suc flip_bit_def not_rec minus_eq_not_minus_1)+
+ and_rec or_rec xor_rec mask_eq_exp_minus_1
+ set_bit_def unset_bit_0 unset_bit_Suc flip_bit_def not_eq_complement)+
end
--- a/src/HOL/Library/Word.thy Wed Nov 29 19:45:54 2023 +0100
+++ b/src/HOL/Library/Word.thy Wed Nov 29 21:29:00 2023 +0100
@@ -997,15 +997,8 @@
instance proof
fix v w :: \<open>'a word\<close> and n m :: nat
- show \<open>NOT v = of_bool (even v) + 2 * NOT (v div 2)\<close>
- apply transfer
- apply (rule bit_eqI)
- apply (auto simp add: even_bit_succ_iff bit_simps bit_0 simp flip: bit_Suc)
- apply (metis Suc_pred bit_0 not_gr_zero)
- using odd_bit_iff_bit_pred apply blast
- done
- show \<open>- v = NOT (v - 1)\<close>
- by transfer (simp add: minus_eq_not_minus_1)
+ show \<open>NOT v = - v - 1\<close>
+ by transfer (simp add: not_eq_complement)
show \<open>v AND w = of_bool (odd v \<and> odd w) + 2 * (v div 2 AND w div 2)\<close>
apply transfer
apply (rule bit_eqI)
--- a/src/HOL/Library/Z2.thy Wed Nov 29 19:45:54 2023 +0100
+++ b/src/HOL/Library/Z2.thy Wed Nov 29 21:29:00 2023 +0100
@@ -155,9 +155,8 @@
instance
apply standard
- apply simp_all
- apply (simp only: Z2.bit_eq_iff even_add)
- apply simp
+ apply simp_all
+ apply (simp only: Z2.bit_eq_iff even_add even_zero refl)
done
end
@@ -169,10 +168,8 @@
where [simp]: \<open>bit_bit b n \<longleftrightarrow> odd b \<and> n = 0\<close>
instance
- apply standard
- apply auto
- apply (metis bit.exhaust of_bool_eq(2))
- done
+ by standard
+ (auto intro: Abs_bit_induct simp add: Abs_bit_eq_of_bool)
end
@@ -219,10 +216,7 @@
end
instance
- apply standard
- apply auto
- apply (simp only: Z2.bit_eq_iff even_add even_zero)
- done
+ by standard auto
end
--- a/src/Pure/Tools/build_schedule.scala Wed Nov 29 19:45:54 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala Wed Nov 29 21:29:00 2023 +0100
@@ -386,7 +386,23 @@
/* schedule generation */
- case class State(build_state: Build_Process.State, current_time: Time) {
+ object Schedule {
+ case class Node(job_name: String, node_info: Node_Info, start: Date, duration: Time) {
+ def end: Date = Date(start.time + duration)
+ }
+
+ type Graph = isabelle.Graph[String, Node]
+ }
+
+ case class Schedule(start: Date, graph: Schedule.Graph) {
+ def end: Date =
+ if (graph.is_empty) start
+ else graph.maximals.map(graph.get_node).map(_.end).maxBy(_.unix_epoch)
+
+ def duration: Time = end.time - start.time
+ }
+
+ case class State(build_state: Build_Process.State, current_time: Time, finished: Schedule) {
def start(config: Config): State =
copy(build_state =
build_state.copy(running = build_state.running +
@@ -405,16 +421,25 @@
if (remaining.isEmpty) error("Schedule step without running sessions")
else {
val (job, elapsed) = remaining.minBy(_._2.ms)
- State(build_state.remove_running(job.name).remove_pending(job.name), current_time + elapsed)
+ val now = current_time + elapsed
+ val node = Schedule.Node(job.name, job.node_info, job.start_date, now - job.start_date.time)
+
+ val preds =
+ build_state.sessions.graph.imm_preds(job.name).filter(finished.graph.defined)
+ val graph =
+ preds.foldLeft(finished.graph.new_node(job.name, node))(_.add_edge(_, job.name))
+
+ val build_state1 = build_state.remove_running(job.name).remove_pending(job.name)
+ State(build_state1, now, finished.copy(graph = graph))
}
}
- def finished: Boolean = build_state.pending.isEmpty && build_state.running.isEmpty
+ def is_finished: Boolean = build_state.pending.isEmpty && build_state.running.isEmpty
}
trait Scheduler {
def next(state: Build_Process.State): List[Config]
- def build_duration(build_state: Build_Process.State): Time
+ def build_schedule(build_state: Build_Process.State): Schedule
}
abstract class Heuristic(timing_data: Timing_Data, max_threads_limit: Int) extends Scheduler {
@@ -428,29 +453,32 @@
timing_data.estimate(job_name, host.info.hostname, threads)
}
- def build_duration(build_state: Build_Process.State): Time = {
+ def build_schedule(build_state: Build_Process.State): Schedule = {
@tailrec
def simulate(state: State): State =
- if (state.finished) state
+ if (state.is_finished) state
else {
val state1 = next(state.build_state).foldLeft(state)(_.start(_)).step(timing_data)
simulate(state1)
}
- val start = Time.now()
- simulate(State(build_state, start)).current_time - start
+ val start = Date.now()
+ val end_state = simulate(State(build_state, start.time, Schedule(start, Graph.empty)))
+
+ end_state.finished
}
}
class Meta_Heuristic(heuristics: List[Heuristic]) extends Scheduler {
require(heuristics.nonEmpty)
- def best_result(state: Build_Process.State): (Heuristic, Time) =
- heuristics.map(heuristic => heuristic -> heuristic.build_duration(state)).minBy(_._2.ms)
+ def best_result(state: Build_Process.State): (Heuristic, Schedule) =
+ heuristics.map(heuristic =>
+ heuristic -> heuristic.build_schedule(state)).minBy(_._2.duration.ms)
def next(state: Build_Process.State): List[Config] = best_result(state)._1.next(state)
- def build_duration(state: Build_Process.State): Time = best_result(state)._2
+ def build_schedule(state: Build_Process.State): Schedule = best_result(state)._2
}
@@ -732,7 +760,7 @@
else {
val start = Time.now()
val next = scheduler.next(state)
- val estimate = Date(Time.now() + scheduler.build_duration(state))
+ val estimate = Date(Time.now() + scheduler.build_schedule(state).duration)
val elapsed = Time.now() - start
val timing_msg = if (elapsed.is_relevant) " (took " + elapsed.message + ")" else ""