--- a/src/HOL/Data_Structures/AVL_Set.thy Tue Aug 20 19:56:31 2019 +0200
+++ b/src/HOL/Data_Structures/AVL_Set.thy Tue Aug 20 20:23:21 2019 +0200
@@ -134,7 +134,7 @@
declare Let_def [simp]
lemma ht_height[simp]: "avl t \<Longrightarrow> ht t = height t"
-by (induct t) simp_all
+by (cases t) simp_all
lemma height_balL:
"\<lbrakk> height l = height r + 2; avl l; avl r \<rbrakk> \<Longrightarrow>
--- a/src/HOL/Data_Structures/Leftist_Heap.thy Tue Aug 20 19:56:31 2019 +0200
+++ b/src/HOL/Data_Structures/Leftist_Heap.thy Tue Aug 20 20:23:21 2019 +0200
@@ -29,13 +29,16 @@
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_mset(mset_tree l + mset_tree r). m \<le> x))"
+ (heap l \<and> heap r \<and> (\<forall>x \<in> set_tree l \<union> set_tree r. m \<le> x))"
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)"
+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
@@ -48,12 +51,15 @@
unbundle pattern_aliases
fun merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
-"merge Leaf t2 = t2" |
-"merge t1 Leaf = t1" |
+"merge Leaf t = t" |
+"merge t Leaf = t" |
"merge (Node l1 a1 n1 r1 =: t1) (Node l2 a2 n2 r2 =: t2) =
(if a1 \<le> a2 then node l1 a1 (merge r1 t2)
else node l2 a2 (merge t1 r2))"
+text \<open>Termination of @{const merge}: by sum or lexicographic product of the sizes
+of the two arguments. Isabelle uses a lexicographic product.\<close>
+
lemma merge_code: "merge t1 t2 = (case (t1,t2) of
(Leaf, _) \<Rightarrow> t2 |
(_, Leaf) \<Rightarrow> t1 |
@@ -83,9 +89,11 @@
by(auto simp add: node_def)
lemma heap_node: "heap (node l a r) \<longleftrightarrow>
- heap l \<and> heap r \<and> (\<forall>x \<in> set_mset(mset_tree l + mset_tree r). a \<le> x)"
+ heap l \<and> heap r \<and> (\<forall>x \<in> set_tree l \<union> set_tree r. a \<le> x)"
by(auto simp add: node_def)
+lemma set_tree_mset: "set_tree t = set_mset(mset_tree t)"
+by(induction t) auto
subsection "Functional Correctness"
@@ -95,7 +103,7 @@
lemma mset_insert: "mset_tree (insert x t) = mset_tree t + {#x#}"
by (auto simp add: insert_def mset_merge)
-lemma get_min: "\<lbrakk> heap h; h \<noteq> Leaf \<rbrakk> \<Longrightarrow> get_min h = Min_mset (mset_tree h)"
+lemma get_min: "\<lbrakk> heap h; h \<noteq> Leaf \<rbrakk> \<Longrightarrow> get_min h = Min(set_tree h)"
by (induction h) (auto simp add: eq_Min_iff)
lemma mset_del_min: "mset_tree (del_min h) = mset_tree h - {# get_min h #}"
@@ -120,7 +128,7 @@
lemma heap_merge: "\<lbrakk> heap l; heap r \<rbrakk> \<Longrightarrow> heap (merge l r)"
proof(induction l r rule: merge.induct)
- case 3 thus ?case by(auto simp: heap_node mset_merge ball_Un)
+ case 3 thus ?case by(auto simp: heap_node mset_merge ball_Un set_tree_mset)
qed simp_all
lemma ltree_insert: "ltree t \<Longrightarrow> ltree(insert x t)"
@@ -139,12 +147,12 @@
to show that leftist heaps satisfy the specification of priority queues with merge.\<close>
interpretation lheap: Priority_Queue_Merge
-where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
+where empty = empty and is_empty = "\<lambda>h. h = Leaf"
and insert = insert and del_min = del_min
and get_min = get_min and merge = merge
and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
proof(standard, goal_cases)
- case 1 show ?case by simp
+ case 1 show ?case by (simp add: empty_def)
next
case (2 q) show ?case by (cases q) auto
next
@@ -152,9 +160,9 @@
next
case 4 show ?case by(rule mset_del_min)
next
- case 5 thus ?case by(simp add: get_min mset_tree_empty)
+ case 5 thus ?case by(simp add: get_min mset_tree_empty set_tree_mset)
next
- case 6 thus ?case by(simp)
+ case 6 thus ?case by(simp add: empty_def)
next
case 7 thus ?case by(simp add: heap_insert ltree_insert)
next
@@ -186,8 +194,8 @@
text\<open>Explicit termination argument: sum of sizes\<close>
fun t_merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> nat" where
-"t_merge Leaf t2 = 1" |
-"t_merge t2 Leaf = 1" |
+"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)"
--- a/src/HOL/Data_Structures/Set2_Join_RBT.thy Tue Aug 20 19:56:31 2019 +0200
+++ b/src/HOL/Data_Structures/Set2_Join_RBT.thy Tue Aug 20 20:23:21 2019 +0200
@@ -32,7 +32,7 @@
B l' x' r' \<Rightarrow> baliR l' x' (joinR r' x r) |
R l' x' r' \<Rightarrow> R l' x' (joinR r' x r))"
-fun join :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
+definition join :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
"join l x r =
(if bheight l > bheight r
then paint Black (joinR l x r)
@@ -102,7 +102,7 @@
(* unused *)
lemma rbt_join: "\<lbrakk> invc l; invh l; invc r; invh r \<rbrakk> \<Longrightarrow> rbt(join l x r)"
by(simp add: invc2_joinL invc2_joinR invc_paint_Black invh_joinL invh_joinR invh_paint rbt_def
- color_paint_Black)
+ color_paint_Black join_def)
text \<open>To make sure the the black height is not increased unnecessarily:\<close>
@@ -112,7 +112,7 @@
lemma "\<lbrakk> rbt l; rbt r \<rbrakk> \<Longrightarrow> bheight(join l x r) \<le> max (bheight l) (bheight r) + 1"
using bheight_paint_Black[of "joinL l x r"] bheight_paint_Black[of "joinR l x r"]
bheight_joinL[of l r x] bheight_joinR[of l r x]
-by(auto simp: max_def rbt_def)
+by(auto simp: max_def rbt_def join_def)
subsubsection "Inorder properties"
@@ -133,7 +133,8 @@
qed
lemma "inorder(join l x r) = inorder l @ x # inorder r"
-by(auto simp: inorder_joinL inorder_joinR inorder_paint split!: tree.splits color.splits if_splits
+by(auto simp: inorder_joinL inorder_joinR inorder_paint join_def
+ split!: tree.splits color.splits if_splits
dest!: arg_cong[where f = inorder])
@@ -165,7 +166,7 @@
by (cases t) auto
lemma set_join: "set_tree (join l x r) = set_tree l \<union> {x} \<union> set_tree r"
-by(simp add: set_joinL set_joinR set_paint)
+by(simp add: set_joinL set_joinR set_paint join_def)
lemma bst_baliL:
"\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < a; \<forall>x\<in>set_tree r. a < x\<rbrakk>
@@ -202,10 +203,10 @@
lemma bst_join:
"bst (Node l a n r) \<Longrightarrow> bst (join l a r)"
-by(auto simp: bst_paint bst_joinL bst_joinR)
+by(auto simp: bst_paint bst_joinL bst_joinR join_def)
lemma inv_join: "\<lbrakk> invc l; invh l; invc r; invh r \<rbrakk> \<Longrightarrow> invc(join l x r) \<and> invh(join l x r)"
-by (simp add: invc2_joinL invc2_joinR invc_paint_Black invh_joinL invh_joinR invh_paint)
+by (simp add: invc2_joinL invc2_joinR invc_paint_Black invh_joinL invh_joinR invh_paint join_def)
subsubsection "Interpretation of \<^locale>\<open>Set2_Join\<close> with Red-Black Tree"
@@ -216,11 +217,11 @@
proof (standard, goal_cases)
case 1 show ?case by (rule set_join)
next
- case 2 thus ?case by (simp add: bst_join del: join.simps)
+ case 2 thus ?case by (simp add: bst_join)
next
case 3 show ?case by simp
next
- case 4 thus ?case by (simp add: inv_join del: join.simps)
+ case 4 thus ?case by (simp add: inv_join)
next
case 5 thus ?case by simp
qed
--- a/src/HOL/Data_Structures/Set_Specs.thy Tue Aug 20 19:56:31 2019 +0200
+++ b/src/HOL/Data_Structures/Set_Specs.thy Tue Aug 20 20:23:21 2019 +0200
@@ -17,7 +17,7 @@
fixes invar :: "'s \<Rightarrow> bool"
assumes set_empty: "set empty = {}"
assumes set_isin: "invar s \<Longrightarrow> isin s x = (x \<in> set s)"
-assumes set_insert: "invar s \<Longrightarrow> set(insert x s) = Set.insert x (set s)"
+assumes set_insert: "invar s \<Longrightarrow> set(insert x s) = set s \<union> {x}"
assumes set_delete: "invar s \<Longrightarrow> set(delete x s) = set s - {x}"
assumes invar_empty: "invar empty"
assumes invar_insert: "invar s \<Longrightarrow> invar(insert x s)"