--- a/Admin/components/index.php Thu Nov 05 19:09:02 2020 +0000
+++ b/Admin/components/index.php Thu Nov 05 19:09:11 2020 +0000
@@ -1,11 +1,11 @@
<html>
<body>
-<h2>Components:</h2>
+<h2>Isabelle Components</h2>
<table>
<tr>
-<th> Name </th>
-<th> </th>
-<th> Size</th>
+<td><b>Name</b></td>
+<td> </td>
+<td><b>Size</b></td>
</tr>
<?php
$component_pattern="/^.+\.tar\.gz$/";
@@ -14,7 +14,7 @@
if (preg_match($component_pattern, $file)
&& is_file($file)
&& is_readable($file)) {
- print "<tr><td><a href=\"$file\">$file</a></td><td></td><td>".filesize($file)."</td></tr>\n";
+ print "<tr><td><a href=\"$file\"><code>$file</code></a></td><td></td><td>".filesize($file)."</td></tr>\n";
}
}
?>
--- a/NEWS Thu Nov 05 19:09:02 2020 +0000
+++ b/NEWS Thu Nov 05 19:09:11 2020 +0000
@@ -147,8 +147,9 @@
INCOMPATIBILITY.
* Former session "HOL-Word": Operations lsb, msb and set_bit are
-separated into theories Misc_lsb, Misc_msb and Misc_set_bit respectively
-in session Word_Lib in the AFP. INCOMPATIBILITY.
+separated into theories Least_significant_bit, Most_significant_bit and
+Generic_set_bit respectively in session Word_Lib in the AFP.
+INCOMPATIBILITY.
* Former session "HOL-Word": Ancient int numeral representation has been
factored out in separate theory "Ancient_Numeral" in session Word_Lib
--- a/etc/settings Thu Nov 05 19:09:02 2020 +0000
+++ b/etc/settings Thu Nov 05 19:09:11 2020 +0000
@@ -73,7 +73,7 @@
isabelle_directory '$ISABELLE_HOME_USER'
isabelle_directory '~~'
-ISABELLE_COMPONENT_REPOSITORY="https://isabelle.sketis.net/components"
+ISABELLE_COMPONENT_REPOSITORY="https://isabelle.in.tum.de/components"
ISABELLE_COMPONENTS_BASE="$USER_HOME/.isabelle/contrib"
# The place for user configuration, heap files, etc.
--- a/src/HOL/Data_Structures/Leftist_Heap.thy Thu Nov 05 19:09:02 2020 +0000
+++ b/src/HOL/Data_Structures/Leftist_Heap.thy Thu Nov 05 19:09:11 2020 +0000
@@ -16,32 +16,28 @@
type_synonym 'a lheap = "('a*nat)tree"
-fun rank :: "'a lheap \<Rightarrow> nat" where
-"rank Leaf = 0" |
-"rank (Node _ _ r) = rank r + 1"
-
-fun rk :: "'a lheap \<Rightarrow> nat" where
-"rk Leaf = 0" |
-"rk (Node _ (_, n) _) = n"
+fun mht :: "'a lheap \<Rightarrow> nat" where
+"mht Leaf = 0" |
+"mht (Node _ (_, n) _) = n"
text\<open>The invariants:\<close>
fun (in linorder) heap :: "('a*'b) tree \<Rightarrow> bool" where
"heap Leaf = True" |
"heap (Node l (m, _) r) =
- (heap l \<and> heap r \<and> (\<forall>x \<in> set_tree l \<union> set_tree r. m \<le> x))"
+ ((\<forall>x \<in> set_tree l \<union> set_tree r. m \<le> x) \<and> heap l \<and> heap r)"
fun ltree :: "'a lheap \<Rightarrow> bool" where
"ltree Leaf = True" |
"ltree (Node l (a, n) r) =
- (n = rank r + 1 \<and> rank l \<ge> rank r \<and> ltree l & ltree r)"
+ (min_height l \<ge> min_height r \<and> n = min_height r + 1 \<and> ltree l & ltree r)"
definition empty :: "'a lheap" where
"empty = Leaf"
definition node :: "'a lheap \<Rightarrow> 'a \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
"node l a r =
- (let rl = rk l; rr = rk r
+ (let rl = mht l; rr = mht r
in if rl \<ge> rr then Node l (a,rr+1) r else Node r (a,rl+1) l)"
fun get_min :: "'a lheap \<Rightarrow> 'a" where
@@ -82,11 +78,11 @@
lemma mset_tree_empty: "mset_tree t = {#} \<longleftrightarrow> t = Leaf"
by(cases t) auto
-lemma rk_eq_rank[simp]: "ltree t \<Longrightarrow> rk t = rank t"
+lemma mht_eq_min_height: "ltree t \<Longrightarrow> mht t = min_height t"
by(cases t) auto
lemma ltree_node: "ltree (node l a r) \<longleftrightarrow> ltree l \<and> ltree r"
-by(auto simp add: node_def)
+by(auto simp add: node_def mht_eq_min_height)
lemma heap_node: "heap (node l a r) \<longleftrightarrow>
heap l \<and> heap r \<and> (\<forall>x \<in> set_tree l \<union> set_tree r. a \<le> x)"
@@ -162,51 +158,36 @@
subsection "Complexity"
-lemma pow2_rank_size1: "ltree t \<Longrightarrow> 2 ^ rank t \<le> size1 t"
-proof(induction t rule: tree2_induct)
- case Leaf show ?case by simp
-next
- case (Node l a n r)
- hence "rank r \<le> rank l" by simp
- hence *: "(2::nat) ^ rank r \<le> 2 ^ rank l" by simp
- have "(2::nat) ^ rank \<langle>l, (a, n), r\<rangle> = 2 ^ rank r + 2 ^ rank r"
- by(simp add: mult_2)
- also have "\<dots> \<le> size1 l + size1 r"
- using Node * by (simp del: power_increasing_iff)
- also have "\<dots> = size1 \<langle>l, (a, n), r\<rangle>" by simp
- finally show ?case .
-qed
-
text\<open>Explicit termination argument: sum of sizes\<close>
-fun t_merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> nat" where
-"t_merge Leaf t = 1" |
-"t_merge t Leaf = 1" |
-"t_merge (Node l1 (a1, n1) r1 =: t1) (Node l2 (a2, n2) r2 =: t2) =
- (if a1 \<le> a2 then 1 + t_merge r1 t2
- else 1 + t_merge t1 r2)"
+fun T_merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> nat" where
+"T_merge Leaf t = 1" |
+"T_merge t Leaf = 1" |
+"T_merge (Node l1 (a1, n1) r1 =: t1) (Node l2 (a2, n2) r2 =: t2) =
+ (if a1 \<le> a2 then T_merge r1 t2
+ else T_merge t1 r2) + 1"
-definition t_insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> nat" where
-"t_insert x t = t_merge (Node Leaf (x, 1) Leaf) t"
+definition T_insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> nat" where
+"T_insert x t = T_merge (Node Leaf (x, 1) Leaf) t + 1"
-fun t_del_min :: "'a::ord lheap \<Rightarrow> nat" where
-"t_del_min Leaf = 1" |
-"t_del_min (Node l _ r) = t_merge l r"
+fun T_del_min :: "'a::ord lheap \<Rightarrow> nat" where
+"T_del_min Leaf = 1" |
+"T_del_min (Node l _ r) = T_merge l r + 1"
-lemma t_merge_rank: "t_merge l r \<le> rank l + rank r + 1"
+lemma T_merge_min_height: "ltree l \<Longrightarrow> ltree r \<Longrightarrow> T_merge l r \<le> min_height l + min_height r + 1"
proof(induction l r rule: merge.induct)
- case 3 thus ?case by(simp)
+ case 3 thus ?case by(auto)
qed simp_all
-corollary t_merge_log: assumes "ltree l" "ltree r"
- shows "t_merge l r \<le> log 2 (size1 l) + log 2 (size1 r) + 1"
-using le_log2_of_power[OF pow2_rank_size1[OF assms(1)]]
- le_log2_of_power[OF pow2_rank_size1[OF assms(2)]] t_merge_rank[of l r]
+corollary T_merge_log: assumes "ltree l" "ltree r"
+ shows "T_merge l r \<le> log 2 (size1 l) + log 2 (size1 r) + 1"
+using le_log2_of_power[OF min_height_size1[of l]]
+ le_log2_of_power[OF min_height_size1[of r]] T_merge_min_height[of l r] assms
by linarith
-corollary t_insert_log: "ltree t \<Longrightarrow> t_insert x t \<le> log 2 (size1 t) + 2"
-using t_merge_log[of "Node Leaf (x, 1) Leaf" t]
-by(simp add: t_insert_def split: tree.split)
+corollary T_insert_log: "ltree t \<Longrightarrow> T_insert x t \<le> log 2 (size1 t) + 3"
+using T_merge_log[of "Node Leaf (x, 1) Leaf" t]
+by(simp add: T_insert_def split: tree.split)
(* FIXME mv ? *)
lemma ld_ld_1_less:
@@ -221,17 +202,17 @@
finally show ?thesis by simp
qed
-corollary t_del_min_log: assumes "ltree t"
- shows "t_del_min t \<le> 2 * log 2 (size1 t) + 1"
+corollary T_del_min_log: assumes "ltree t"
+ shows "T_del_min t \<le> 2 * log 2 (size1 t) + 1"
proof(cases t rule: tree2_cases)
case Leaf thus ?thesis using assms by simp
next
- case [simp]: (Node t1 _ _ t2)
- have "t_del_min t = t_merge t1 t2" by simp
- also have "\<dots> \<le> log 2 (size1 t1) + log 2 (size1 t2) + 1"
- using \<open>ltree t\<close> by (auto simp: t_merge_log simp del: t_merge.simps)
+ case [simp]: (Node l _ _ r)
+ have "T_del_min t = T_merge l r + 1" by simp
+ also have "\<dots> \<le> log 2 (size1 l) + log 2 (size1 r) + 2"
+ using \<open>ltree t\<close> T_merge_log[of l r] by (auto simp del: T_merge.simps)
also have "\<dots> \<le> 2 * log 2 (size1 t) + 1"
- using ld_ld_1_less[of "size1 t1" "size1 t2"] by (simp)
+ using ld_ld_1_less[of "size1 l" "size1 r"] by (simp)
finally show ?thesis .
qed
--- a/src/HOL/Data_Structures/Queue_2Lists.thy Thu Nov 05 19:09:02 2020 +0000
+++ b/src/HOL/Data_Structures/Queue_2Lists.thy Thu Nov 05 19:09:11 2020 +0000
@@ -57,30 +57,30 @@
text \<open>Running times:\<close>
-fun t_norm :: "'a queue \<Rightarrow> nat" where
-"t_norm (fs,rs) = (if fs = [] then length rs else 0) + 1"
+fun T_norm :: "'a queue \<Rightarrow> nat" where
+"T_norm (fs,rs) = (if fs = [] then length rs else 0) + 1"
-fun t_enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> nat" where
-"t_enq a (fs,rs) = t_norm(fs, a # rs)"
+fun T_enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> nat" where
+"T_enq a (fs,rs) = T_norm(fs, a # rs) + 1"
-fun t_deq :: "'a queue \<Rightarrow> nat" where
-"t_deq (fs,rs) = (if fs = [] then 0 else t_norm(tl fs,rs)) + 1"
+fun T_deq :: "'a queue \<Rightarrow> nat" where
+"T_deq (fs,rs) = (if fs = [] then 0 else T_norm(tl fs,rs)) + 1"
-fun t_first :: "'a queue \<Rightarrow> nat" where
-"t_first (a # fs,rs) = 1"
+fun T_first :: "'a queue \<Rightarrow> nat" where
+"T_first (a # fs,rs) = 1"
-fun t_is_empty :: "'a queue \<Rightarrow> nat" where
-"t_is_empty (fs,rs) = 1"
+fun T_is_empty :: "'a queue \<Rightarrow> nat" where
+"T_is_empty (fs,rs) = 1"
text \<open>Amortized running times:\<close>
fun \<Phi> :: "'a queue \<Rightarrow> nat" where
"\<Phi>(fs,rs) = length rs"
-lemma a_enq: "t_enq a (fs,rs) + \<Phi>(enq a (fs,rs)) - \<Phi>(fs,rs) \<le> 2"
+lemma a_enq: "T_enq a (fs,rs) + \<Phi>(enq a (fs,rs)) - \<Phi>(fs,rs) \<le> 3"
by(auto)
-lemma a_deq: "t_deq (fs,rs) + \<Phi>(deq (fs,rs)) - \<Phi>(fs,rs) \<le> 2"
+lemma a_deq: "T_deq (fs,rs) + \<Phi>(deq (fs,rs)) - \<Phi>(fs,rs) \<le> 2"
by(auto)
end
--- a/src/HOL/Data_Structures/Sorting.thy Thu Nov 05 19:09:02 2020 +0000
+++ b/src/HOL/Data_Structures/Sorting.thy Thu Nov 05 19:09:11 2020 +0000
@@ -27,7 +27,7 @@
subsubsection "Functional Correctness"
-lemma mset_insort: "mset (insort x xs) = add_mset x (mset xs)"
+lemma mset_insort: "mset (insort x xs) = {#x#} + mset xs"
apply(induction xs)
apply auto
done
@@ -39,7 +39,7 @@
done
lemma set_insort: "set (insort x xs) = insert x (set xs)"
-by (metis mset_insort set_mset_add_mset_insert set_mset_mset)
+by(simp add: mset_insort flip: set_mset_mset)
lemma sorted_insort: "sorted (insort a xs) = sorted xs"
apply(induction xs)
@@ -386,7 +386,7 @@
subsubsection "Standard functional correctness"
-lemma mset_insort_key: "mset (insort_key f x xs) = add_mset x (mset xs)"
+lemma mset_insort_key: "mset (insort_key f x xs) = {#x#} + mset xs"
by(induction xs) simp_all
lemma mset_isort_key: "mset (isort_key f xs) = mset xs"
--- a/src/HOL/Data_Structures/Tree23_of_List.thy Thu Nov 05 19:09:02 2020 +0000
+++ b/src/HOL/Data_Structures/Tree23_of_List.thy Thu Nov 05 19:09:11 2020 +0000
@@ -116,50 +116,53 @@
subsection "Linear running time"
-fun t_join_adj :: "'a tree23s \<Rightarrow> nat" where
-"t_join_adj (TTs t1 a (T t2)) = 1" |
-"t_join_adj (TTs t1 a (TTs t2 b (T t3))) = 1" |
-"t_join_adj (TTs t1 a (TTs t2 b ts)) = t_join_adj ts + 1"
+fun T_join_adj :: "'a tree23s \<Rightarrow> nat" where
+"T_join_adj (TTs t1 a (T t2)) = 1" |
+"T_join_adj (TTs t1 a (TTs t2 b (T t3))) = 1" |
+"T_join_adj (TTs t1 a (TTs t2 b ts)) = T_join_adj ts + 1"
-fun t_join_all :: "'a tree23s \<Rightarrow> nat" where
-"t_join_all (T t) = 1" |
-"t_join_all ts = t_join_adj ts + t_join_all (join_adj ts)"
+fun T_join_all :: "'a tree23s \<Rightarrow> nat" where
+"T_join_all (T t) = 1" |
+"T_join_all ts = T_join_adj ts + T_join_all (join_adj ts) + 1"
-fun t_leaves :: "'a list \<Rightarrow> nat" where
-"t_leaves [] = 1" |
-"t_leaves (a # as) = t_leaves as + 1"
+fun T_leaves :: "'a list \<Rightarrow> nat" where
+"T_leaves [] = 1" |
+"T_leaves (a # as) = T_leaves as + 1"
+
+definition T_tree23_of_list :: "'a list \<Rightarrow> nat" where
+"T_tree23_of_list as = T_leaves as + T_join_all(leaves as) + 1"
-definition t_tree23_of_list :: "'a list \<Rightarrow> nat" where
-"t_tree23_of_list as = t_leaves as + t_join_all(leaves as)"
+lemma T_join_adj: "not_T ts \<Longrightarrow> T_join_adj ts \<le> len ts div 2"
+by(induction ts rule: T_join_adj.induct) auto
-lemma t_join_adj: "not_T ts \<Longrightarrow> t_join_adj ts \<le> len ts div 2"
-by(induction ts rule: t_join_adj.induct) auto
+lemma len_ge_1: "len ts \<ge> 1"
+by(cases ts) auto
-lemma t_join_all: "t_join_all ts \<le> len ts"
+lemma T_join_all: "T_join_all ts \<le> 2 * len ts"
proof(induction ts rule: join_all.induct)
case 1 thus ?case by simp
next
case (2 t a ts)
let ?ts = "TTs t a ts"
- have "t_join_all ?ts = t_join_adj ?ts + t_join_all (join_adj ?ts)"
+ have "T_join_all ?ts = T_join_adj ?ts + T_join_all (join_adj ?ts) + 1"
by simp
- also have "\<dots> \<le> len ?ts div 2 + t_join_all (join_adj ?ts)"
- using t_join_adj[of ?ts] by simp
- also have "\<dots> \<le> len ?ts div 2 + len (join_adj ?ts)"
+ also have "\<dots> \<le> len ?ts div 2 + T_join_all (join_adj ?ts) + 1"
+ using T_join_adj[of ?ts] by simp
+ also have "\<dots> \<le> len ?ts div 2 + 2 * len (join_adj ?ts) + 1"
using "2.IH" by simp
- also have "\<dots> \<le> len ?ts div 2 + len ?ts div 2"
+ also have "\<dots> \<le> len ?ts div 2 + 2 * (len ?ts div 2) + 1"
using len_join_adj_div2[of ?ts] by simp
- also have "\<dots> \<le> len ?ts" by linarith
+ also have "\<dots> \<le> 2 * len ?ts" using len_ge_1[of ?ts] by linarith
finally show ?case .
qed
-lemma t_leaves: "t_leaves as = length as + 1"
+lemma T_leaves: "T_leaves as = length as + 1"
by(induction as) auto
lemma len_leaves: "len(leaves as) = length as + 1"
by(induction as) auto
-lemma t_tree23_of_list: "t_tree23_of_list as \<le> 2*(length as + 1)"
-using t_join_all[of "leaves as"] by(simp add: t_tree23_of_list_def t_leaves len_leaves)
+lemma T_tree23_of_list: "T_tree23_of_list as \<le> 3*(length as) + 4"
+using T_join_all[of "leaves as"] by(simp add: T_tree23_of_list_def T_leaves len_leaves)
end
--- a/src/HOL/Groups_List.thy Thu Nov 05 19:09:02 2020 +0000
+++ b/src/HOL/Groups_List.thy Thu Nov 05 19:09:11 2020 +0000
@@ -301,6 +301,10 @@
finally show ?thesis by(simp add:sum_list_map_eq_sum_count)
qed
+lemma sum_list_replicate: "sum_list (replicate n c) = of_nat n * c"
+by(induction n)(auto simp add: distrib_right)
+
+
lemma sum_list_nonneg:
"(\<And>x. x \<in> set xs \<Longrightarrow> (x :: 'a :: ordered_comm_monoid_add) \<ge> 0) \<Longrightarrow> sum_list xs \<ge> 0"
by (induction xs) simp_all