# HG changeset patch
# User wenzelm
# Date 1566325401 -7200
# Node ID a56b4e59bfd146640f3a1faf2d21276a5d48b305
# Parent  eecade21bc6a8871f368570c413618e7c40a21aa# Parent  a896257a3f07c4993dbe9d8295820d67bfc53293
merged

diff -r a896257a3f07 -r a56b4e59bfd1 src/HOL/Data_Structures/AVL_Set.thy
--- 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>
diff -r a896257a3f07 -r a56b4e59bfd1 src/HOL/Data_Structures/Leftist_Heap.thy
--- 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)"
diff -r a896257a3f07 -r a56b4e59bfd1 src/HOL/Data_Structures/Set2_Join_RBT.thy
--- 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
diff -r a896257a3f07 -r a56b4e59bfd1 src/HOL/Data_Structures/Set_Specs.thy
--- 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)"