--- a/src/HOL/Data_Structures/Balance.thy Tue Nov 10 23:21:04 2020 +0000
+++ b/src/HOL/Data_Structures/Balance.thy Wed Nov 11 11:27:44 2020 +0000
@@ -1,6 +1,6 @@
(* Author: Tobias Nipkow *)
-section \<open>Creating Balanced Trees\<close>
+section \<open>Creating Almost Complete Trees\<close>
theory Balance
imports
@@ -169,9 +169,9 @@
qed
qed
-lemma balanced_bal:
- assumes "n \<le> length xs" "bal n xs = (t,ys)" shows "balanced t"
-unfolding balanced_def
+lemma acomplete_bal:
+ assumes "n \<le> length xs" "bal n xs = (t,ys)" shows "acomplete t"
+unfolding acomplete_def
using height_bal[OF assms] min_height_bal[OF assms]
by linarith
@@ -192,16 +192,16 @@
"height (balance_tree t) = nat\<lceil>log 2 (size t + 1)\<rceil>"
by (simp add: bal_tree_def balance_tree_def height_bal_list)
-corollary balanced_bal_list[simp]: "n \<le> length xs \<Longrightarrow> balanced (bal_list n xs)"
-unfolding bal_list_def by (metis balanced_bal prod.collapse)
+corollary acomplete_bal_list[simp]: "n \<le> length xs \<Longrightarrow> acomplete (bal_list n xs)"
+unfolding bal_list_def by (metis acomplete_bal prod.collapse)
-corollary balanced_balance_list[simp]: "balanced (balance_list xs)"
+corollary acomplete_balance_list[simp]: "acomplete (balance_list xs)"
by (simp add: balance_list_def)
-corollary balanced_bal_tree[simp]: "n \<le> size t \<Longrightarrow> balanced (bal_tree n t)"
+corollary acomplete_bal_tree[simp]: "n \<le> size t \<Longrightarrow> acomplete (bal_tree n t)"
by (simp add: bal_tree_def)
-corollary balanced_balance_tree[simp]: "balanced (balance_tree t)"
+corollary acomplete_balance_tree[simp]: "acomplete (balance_tree t)"
by (simp add: balance_tree_def)
lemma wbalanced_bal: "\<lbrakk> n \<le> length xs; bal n xs = (t,ys) \<rbrakk> \<Longrightarrow> wbalanced t"
@@ -226,9 +226,9 @@
qed
qed
-text\<open>An alternative proof via @{thm balanced_if_wbalanced}:\<close>
-lemma "\<lbrakk> n \<le> length xs; bal n xs = (t,ys) \<rbrakk> \<Longrightarrow> balanced t"
-by(rule balanced_if_wbalanced[OF wbalanced_bal])
+text\<open>An alternative proof via @{thm acomplete_if_wbalanced}:\<close>
+lemma "\<lbrakk> n \<le> length xs; bal n xs = (t,ys) \<rbrakk> \<Longrightarrow> acomplete t"
+by(rule acomplete_if_wbalanced[OF wbalanced_bal])
lemma wbalanced_bal_list[simp]: "n \<le> length xs \<Longrightarrow> wbalanced (bal_list n xs)"
by(simp add: bal_list_def) (metis prod.collapse wbalanced_bal)
--- a/src/HOL/Data_Structures/Braun_Tree.thy Tue Nov 10 23:21:04 2020 +0000
+++ b/src/HOL/Data_Structures/Braun_Tree.thy Wed Nov 11 11:27:44 2020 +0000
@@ -30,13 +30,13 @@
thus ?case using Node.prems(1,2) Node.IH by auto
qed
-text \<open>Braun trees are balanced:\<close>
+text \<open>Braun trees are almost complete:\<close>
-lemma balanced_if_braun: "braun t \<Longrightarrow> balanced t"
+lemma acomplete_if_braun: "braun t \<Longrightarrow> acomplete t"
proof(induction t)
- case Leaf show ?case by (simp add: balanced_def)
+ case Leaf show ?case by (simp add: acomplete_def)
next
- case (Node l x r) thus ?case using balanced_Node_if_wbal2 by force
+ case (Node l x r) thus ?case using acomplete_Node_if_wbal2 by force
qed
subsection \<open>Numbering Nodes\<close>
--- a/src/HOL/Data_Structures/Sorting.thy Tue Nov 10 23:21:04 2020 +0000
+++ b/src/HOL/Data_Structures/Sorting.thy Wed Nov 11 11:27:44 2020 +0000
@@ -38,7 +38,7 @@
apply (simp add: mset_insort)
done
-lemma set_insort: "set (insort x xs) = insert x (set xs)"
+lemma set_insort: "set (insort x xs) = {x} \<union> set xs"
by(simp add: mset_insort flip: set_mset_mset)
lemma sorted_insort: "sorted (insort a xs) = sorted xs"
--- a/src/HOL/Data_Structures/Tree23.thy Tue Nov 10 23:21:04 2020 +0000
+++ b/src/HOL/Data_Structures/Tree23.thy Wed Nov 11 11:27:44 2020 +0000
@@ -32,7 +32,7 @@
end
-text \<open>Balanced:\<close>
+text \<open>Completeness:\<close>
fun complete :: "'a tree23 \<Rightarrow> bool" where
"complete Leaf = True" |
--- a/src/HOL/Data_Structures/Tree23_Set.thy Tue Nov 10 23:21:04 2020 +0000
+++ b/src/HOL/Data_Structures/Tree23_Set.thy Wed Nov 11 11:27:44 2020 +0000
@@ -114,7 +114,7 @@
"split_min (Node3 l a m b r) = (let (x,l') = split_min l in (x, node31 l' a m b r))"
text \<open>In the base cases of \<open>split_min\<close> and \<open>del\<close> it is enough to check if one subtree is a \<open>Leaf\<close>,
-in which case balancedness implies that so are the others. Exercise.\<close>
+in which case completeness implies that so are the others. Exercise.\<close>
fun del :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a upD" where
"del x Leaf = TD Leaf" |
@@ -203,7 +203,7 @@
by(simp add: delete_def inorder_del)
-subsection \<open>Balancedness\<close>
+subsection \<open>Completeness\<close>
subsubsection "Proofs for insert"
@@ -225,7 +225,7 @@
by (induct t) (auto split!: if_split upI.split) (* 15 secs in 2015 *)
text\<open>Now an alternative proof (by Brian Huffman) that runs faster because
-two properties (balance and height) are combined in one predicate.\<close>
+two properties (completeness and height) are combined in one predicate.\<close>
inductive full :: "nat \<Rightarrow> 'a tree23 \<Rightarrow> bool" where
"full 0 Leaf" |
--- a/src/HOL/Library/Tree.thy Tue Nov 10 23:21:04 2020 +0000
+++ b/src/HOL/Library/Tree.thy Wed Nov 11 11:27:44 2020 +0000
@@ -1,5 +1,5 @@
(* Author: Tobias Nipkow *)
-(* Todo: minimal ipl of balanced trees *)
+(* Todo: minimal ipl of almost complete trees *)
section \<open>Binary Tree\<close>
@@ -55,8 +55,9 @@
"complete Leaf = True" |
"complete (Node l x r) = (complete l \<and> complete r \<and> height l = height r)"
-definition balanced :: "'a tree \<Rightarrow> bool" where
-"balanced t = (height t - min_height t \<le> 1)"
+text \<open>Almost complete:\<close>
+definition acomplete :: "'a tree \<Rightarrow> bool" where
+"acomplete t = (height t - min_height t \<le> 1)"
text \<open>Weight balanced:\<close>
fun wbalanced :: "'a tree \<Rightarrow> bool" where
@@ -290,24 +291,24 @@
using complete_if_size1_height size1_if_complete by blast
-subsection \<open>\<^const>\<open>balanced\<close>\<close>
+subsection \<open>\<^const>\<open>acomplete\<close>\<close>
-lemma balanced_subtreeL: "balanced (Node l x r) \<Longrightarrow> balanced l"
-by(simp add: balanced_def)
+lemma acomplete_subtreeL: "acomplete (Node l x r) \<Longrightarrow> acomplete l"
+by(simp add: acomplete_def)
-lemma balanced_subtreeR: "balanced (Node l x r) \<Longrightarrow> balanced r"
-by(simp add: balanced_def)
+lemma acomplete_subtreeR: "acomplete (Node l x r) \<Longrightarrow> acomplete r"
+by(simp add: acomplete_def)
-lemma balanced_subtrees: "\<lbrakk> balanced t; s \<in> subtrees t \<rbrakk> \<Longrightarrow> balanced s"
+lemma acomplete_subtrees: "\<lbrakk> acomplete t; s \<in> subtrees t \<rbrakk> \<Longrightarrow> acomplete s"
using [[simp_depth_limit=1]]
by(induction t arbitrary: s)
- (auto simp add: balanced_subtreeL balanced_subtreeR)
+ (auto simp add: acomplete_subtreeL acomplete_subtreeR)
text\<open>Balanced trees have optimal height:\<close>
-lemma balanced_optimal:
+lemma acomplete_optimal:
fixes t :: "'a tree" and t' :: "'b tree"
-assumes "balanced t" "size t \<le> size t'" shows "height t \<le> height t'"
+assumes "acomplete t" "size t \<le> size t'" shows "height t \<le> height t'"
proof (cases "complete t")
case True
have "(2::nat) ^ height t \<le> 2 ^ height t'"
@@ -333,7 +334,7 @@
hence *: "min_height t < height t'" by simp
have "min_height t + 1 = height t"
using min_height_le_height[of t] assms(1) False
- by (simp add: complete_iff_height balanced_def)
+ by (simp add: complete_iff_height acomplete_def)
with * show ?thesis by arith
qed
--- a/src/HOL/Library/Tree_Real.thy Tue Nov 10 23:21:04 2020 +0000
+++ b/src/HOL/Library/Tree_Real.thy Wed Nov 11 11:27:44 2020 +0000
@@ -26,7 +26,7 @@
by (simp add: less_log2_of_power min_height_size1_if_incomplete)
-lemma min_height_balanced: assumes "balanced t"
+lemma min_height_acomplete: assumes "acomplete t"
shows "min_height t = nat(floor(log 2 (size1 t)))"
proof cases
assume *: "complete t"
@@ -37,12 +37,12 @@
assume *: "\<not> complete t"
hence "height t = min_height t + 1"
using assms min_height_le_height[of t]
- by(auto simp: balanced_def complete_iff_height)
+ by(auto simp: acomplete_def complete_iff_height)
hence "size1 t < 2 ^ (min_height t + 1)" by (metis * size1_height_if_incomplete)
from floor_log_nat_eq_if[OF min_height_size1 this] show ?thesis by simp
qed
-lemma height_balanced: assumes "balanced t"
+lemma height_acomplete: assumes "acomplete t"
shows "height t = nat(ceiling(log 2 (size1 t)))"
proof cases
assume *: "complete t"
@@ -52,41 +52,41 @@
assume *: "\<not> complete t"
hence **: "height t = min_height t + 1"
using assms min_height_le_height[of t]
- by(auto simp add: balanced_def complete_iff_height)
+ by(auto simp add: acomplete_def complete_iff_height)
hence "size1 t \<le> 2 ^ (min_height t + 1)" by (metis size1_height)
from log2_of_power_le[OF this size1_ge0] min_height_size1_log_if_incomplete[OF *] **
show ?thesis by linarith
qed
-lemma balanced_Node_if_wbal1:
-assumes "balanced l" "balanced r" "size l = size r + 1"
-shows "balanced \<langle>l, x, r\<rangle>"
+lemma acomplete_Node_if_wbal1:
+assumes "acomplete l" "acomplete r" "size l = size r + 1"
+shows "acomplete \<langle>l, x, r\<rangle>"
proof -
from assms(3) have [simp]: "size1 l = size1 r + 1" by(simp add: size1_size)
have "nat \<lceil>log 2 (1 + size1 r)\<rceil> \<ge> nat \<lceil>log 2 (size1 r)\<rceil>"
by(rule nat_mono[OF ceiling_mono]) simp
hence 1: "height(Node l x r) = nat \<lceil>log 2 (1 + size1 r)\<rceil> + 1"
- using height_balanced[OF assms(1)] height_balanced[OF assms(2)]
+ using height_acomplete[OF assms(1)] height_acomplete[OF assms(2)]
by (simp del: nat_ceiling_le_eq add: max_def)
have "nat \<lfloor>log 2 (1 + size1 r)\<rfloor> \<ge> nat \<lfloor>log 2 (size1 r)\<rfloor>"
by(rule nat_mono[OF floor_mono]) simp
hence 2: "min_height(Node l x r) = nat \<lfloor>log 2 (size1 r)\<rfloor> + 1"
- using min_height_balanced[OF assms(1)] min_height_balanced[OF assms(2)]
+ using min_height_acomplete[OF assms(1)] min_height_acomplete[OF assms(2)]
by (simp)
have "size1 r \<ge> 1" by(simp add: size1_size)
then obtain i where i: "2 ^ i \<le> size1 r" "size1 r < 2 ^ (i + 1)"
using ex_power_ivl1[of 2 "size1 r"] by auto
hence i1: "2 ^ i < size1 r + 1" "size1 r + 1 \<le> 2 ^ (i + 1)" by auto
from 1 2 floor_log_nat_eq_if[OF i] ceiling_log_nat_eq_if[OF i1]
- show ?thesis by(simp add:balanced_def)
+ show ?thesis by(simp add:acomplete_def)
qed
-lemma balanced_sym: "balanced \<langle>l, x, r\<rangle> \<Longrightarrow> balanced \<langle>r, y, l\<rangle>"
-by(auto simp: balanced_def)
+lemma acomplete_sym: "acomplete \<langle>l, x, r\<rangle> \<Longrightarrow> acomplete \<langle>r, y, l\<rangle>"
+by(auto simp: acomplete_def)
-lemma balanced_Node_if_wbal2:
-assumes "balanced l" "balanced r" "abs(int(size l) - int(size r)) \<le> 1"
-shows "balanced \<langle>l, x, r\<rangle>"
+lemma acomplete_Node_if_wbal2:
+assumes "acomplete l" "acomplete r" "abs(int(size l) - int(size r)) \<le> 1"
+shows "acomplete \<langle>l, x, r\<rangle>"
proof -
have "size l = size r \<or> (size l = size r + 1 \<or> size r = size l + 1)" (is "?A \<or> ?B")
using assms(3) by linarith
@@ -94,21 +94,21 @@
proof
assume "?A"
thus ?thesis using assms(1,2)
- apply(simp add: balanced_def min_def max_def)
- by (metis assms(1,2) balanced_optimal le_antisym le_less)
+ apply(simp add: acomplete_def min_def max_def)
+ by (metis assms(1,2) acomplete_optimal le_antisym le_less)
next
assume "?B"
thus ?thesis
- by (meson assms(1,2) balanced_sym balanced_Node_if_wbal1)
+ by (meson assms(1,2) acomplete_sym acomplete_Node_if_wbal1)
qed
qed
-lemma balanced_if_wbalanced: "wbalanced t \<Longrightarrow> balanced t"
+lemma acomplete_if_wbalanced: "wbalanced t \<Longrightarrow> acomplete t"
proof(induction t)
- case Leaf show ?case by (simp add: balanced_def)
+ case Leaf show ?case by (simp add: acomplete_def)
next
case (Node l x r)
- thus ?case by(simp add: balanced_Node_if_wbal2)
+ thus ?case by(simp add: acomplete_Node_if_wbal2)
qed
end
--- a/src/HOL/ex/Tree23.thy Tue Nov 10 23:21:04 2020 +0000
+++ b/src/HOL/ex/Tree23.thy Wed Nov 11 11:27:44 2020 +0000
@@ -12,9 +12,6 @@
in the Isabelle source code. That source is due to Makarius Wenzel and Stefan
Berghofer.
-So far this file contains only data types and functions, but no proofs. Feel
-free to have a go at the latter!
-
Note that because of complicated patterns and mutual recursion, these
function definitions take a few minutes and can also be seen as stress tests
for the function definition facility.\<close>
--- a/src/Pure/General/mailman.scala Tue Nov 10 23:21:04 2020 +0000
+++ b/src/Pure/General/mailman.scala Wed Nov 11 11:27:44 2020 +0000
@@ -20,18 +20,18 @@
val hrefs = """href="([^"]+\.txt(?:\.gz)?)"""".r.findAllMatchIn(text).map(_.group(1)).toList
val title =
"""<title>The ([^</>]*) Archives</title>""".r.findFirstMatchIn(text).map(_.group(1))
+ val list_url =
+ Url(Library.take_suffix[Char](_ == '/', Url.trim_index(url).toString.toList)._1.mkString + "/")
val list_name =
(proper_string(name) orElse title).getOrElse(error("Failed to determine mailing list name"))
- new Archive(Url.trim_index(url), list_name, hrefs)
+ new Archive(list_url, list_name, hrefs)
}
class Archive private[Mailman](val list_url: URL, val list_name: String, hrefs: List[String])
{
override def toString: String = list_name
- def download(
- target_dir: Path = Path.current,
- progress: Progress = new Progress): List[Path] =
+ def download(target_dir: Path, progress: Progress = new Progress): List[Path] =
{
val dir = target_dir + Path.basic(list_name)
Isabelle_System.make_directory(dir)
--- a/src/Pure/Thy/present.scala Tue Nov 10 23:21:04 2020 +0000
+++ b/src/Pure/Thy/present.scala Wed Nov 11 11:27:44 2020 +0000
@@ -193,6 +193,17 @@
+ /** make document source **/
+
+ def write_tex_index(dir: Path, names: List[Document.Node.Name])
+ {
+ val path = dir + Path.explode("session.tex")
+ val text = names.map(name => "\\input{" + name.theory_base_name + ".tex}\n\n").mkString
+ File.write(path, text)
+ }
+
+
+
/** build document **/
val document_format = "pdf"
--- a/src/Pure/Thy/sessions.scala Tue Nov 10 23:21:04 2020 +0000
+++ b/src/Pure/Thy/sessions.scala Wed Nov 11 11:27:44 2020 +0000
@@ -167,10 +167,7 @@
val overall_syntax = dependencies.overall_syntax
val session_theories =
- for {
- name <- dependencies.theories
- if deps_base.theory_qualifier(name) == info.name
- } yield name
+ dependencies.theories.filter(name => deps_base.theory_qualifier(name) == session_name)
val theory_files = dependencies.theories.map(_.path)
@@ -240,9 +237,6 @@
val known_loaded_files = deps_base.known_loaded_files ++ loaded_files
- val used_theories_session =
- dependencies.theories.filter(name => deps_base.theory_qualifier(name) == session_name)
-
val import_errors =
{
val known_sessions =
@@ -260,7 +254,7 @@
val ok = info.dirs.map(_.canonical_file).toSet
val bad =
(for {
- name <- used_theories_session.iterator
+ name <- session_theories.iterator
path = name.master_dir_path
if !ok(path.canonical_file)
path1 = File.relative_path(info.dir.canonical, path).getOrElse(path)
@@ -276,7 +270,7 @@
val errs3 = for (p <- info.dirs if !p.is_dir) yield "No such directory: " + p
val errs4 =
(for {
- name <- used_theories_session.iterator
+ name <- session_theories.iterator
name1 <- resources.find_theory_node(name.theory)
if name.node != name1.node
} yield "Incoherent theory file import:\n " + name.path + " vs. \n " + name1.path)
--- a/src/Pure/Tools/build.scala Tue Nov 10 23:21:04 2020 +0000
+++ b/src/Pure/Tools/build.scala Wed Nov 11 11:27:44 2020 +0000
@@ -415,9 +415,7 @@
for (document_output <- proper_string(options.string("document_output"))) {
val document_output_dir =
Isabelle_System.make_directory(info.dir + Path.explode(document_output))
- val base = deps(session_name)
- File.write(document_output_dir + Path.explode("session.tex"),
- base.session_theories.map(name => "\\input{" + name.theory_base_name + ".tex}\n\n").mkString)
+ Present.write_tex_index(document_output_dir, deps(session_name).session_theories)
}
Present.finish(progress, store.browser_info, graph_file, info, session_name)
}