src/HOL/Data_Structures/Leftist_Heap.thy
changeset 68413 b56ed5010e69
parent 68021 b91a043c0dcb
child 68492 c7e0a7bcacaf
     1.1 --- a/src/HOL/Data_Structures/Leftist_Heap.thy	Mon Jun 11 08:15:43 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/Leftist_Heap.thy	Mon Jun 11 16:29:27 2018 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  
     1.5  fun mset_tree :: "('a,'b) tree \<Rightarrow> 'a multiset" where
     1.6  "mset_tree Leaf = {#}" |
     1.7 -"mset_tree (Node _ l a r) = {#a#} + mset_tree l + mset_tree r"
     1.8 +"mset_tree (Node l a _ r) = {#a#} + mset_tree l + mset_tree r"
     1.9  
    1.10  type_synonym 'a lheap = "('a,nat)tree"
    1.11  
    1.12 @@ -22,27 +22,27 @@
    1.13  
    1.14  fun rk :: "'a lheap \<Rightarrow> nat" where
    1.15  "rk Leaf = 0" |
    1.16 -"rk (Node n _ _ _) = n"
    1.17 +"rk (Node _ _ n _) = n"
    1.18  
    1.19  text\<open>The invariants:\<close>
    1.20  
    1.21  fun (in linorder) heap :: "('a,'b) tree \<Rightarrow> bool" where
    1.22  "heap Leaf = True" |
    1.23 -"heap (Node _ l m r) =
    1.24 +"heap (Node l m _ r) =
    1.25    (heap l \<and> heap r \<and> (\<forall>x \<in> set_mset(mset_tree l + mset_tree r). m \<le> x))"
    1.26  
    1.27  fun ltree :: "'a lheap \<Rightarrow> bool" where
    1.28  "ltree Leaf = True" |
    1.29 -"ltree (Node n l a r) =
    1.30 +"ltree (Node l a n r) =
    1.31   (n = rank r + 1 \<and> rank l \<ge> rank r \<and> ltree l & ltree r)"
    1.32  
    1.33  definition node :: "'a lheap \<Rightarrow> 'a \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
    1.34  "node l a r =
    1.35   (let rl = rk l; rr = rk r
    1.36 -  in if rl \<ge> rr then Node (rr+1) l a r else Node (rl+1) r a l)"
    1.37 +  in if rl \<ge> rr then Node l a (rr+1) r else Node r a (rl+1) l)"
    1.38  
    1.39  fun get_min :: "'a lheap \<Rightarrow> 'a" where
    1.40 -"get_min(Node n l a r) = a"
    1.41 +"get_min(Node l a n r) = a"
    1.42  
    1.43  text \<open>For function \<open>merge\<close>:\<close>
    1.44  unbundle pattern_aliases
    1.45 @@ -51,25 +51,25 @@
    1.46  fun merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
    1.47  "merge Leaf t2 = t2" |
    1.48  "merge t1 Leaf = t1" |
    1.49 -"merge (Node n1 l1 a1 r1 =: t1) (Node n2 l2 a2 r2 =: t2) =
    1.50 +"merge (Node l1 a1 n1 r1 =: t1) (Node l2 a2 n2 r2 =: t2) =
    1.51     (if a1 \<le> a2 then node l1 a1 (merge r1 t2)
    1.52      else node l2 a2 (merge r2 t1))"
    1.53  
    1.54  lemma merge_code: "merge t1 t2 = (case (t1,t2) of
    1.55    (Leaf, _) \<Rightarrow> t2 |
    1.56    (_, Leaf) \<Rightarrow> t1 |
    1.57 -  (Node n1 l1 a1 r1, Node n2 l2 a2 r2) \<Rightarrow>
    1.58 +  (Node l1 a1 n1 r1, Node l2 a2 n2 r2) \<Rightarrow>
    1.59      if a1 \<le> a2 then node l1 a1 (merge r1 t2) else node l2 a2 (merge r2 t1))"
    1.60  by(induction t1 t2 rule: merge.induct) (simp_all split: tree.split)
    1.61  
    1.62  hide_const (open) insert
    1.63  
    1.64  definition insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
    1.65 -"insert x t = merge (Node 1 Leaf x Leaf) t"
    1.66 +"insert x t = merge (Node Leaf x 1 Leaf) t"
    1.67  
    1.68  fun del_min :: "'a::ord lheap \<Rightarrow> 'a lheap" where
    1.69  "del_min Leaf = Leaf" |
    1.70 -"del_min (Node n l x r) = merge l r"
    1.71 +"del_min (Node l x n r) = merge l r"
    1.72  
    1.73  
    1.74  subsection "Lemmas"
    1.75 @@ -104,7 +104,7 @@
    1.76  
    1.77  lemma ltree_merge: "\<lbrakk> ltree l; ltree r \<rbrakk> \<Longrightarrow> ltree (merge l r)"
    1.78  proof(induction l r rule: merge.induct)
    1.79 -  case (3 n1 l1 a1 r1 n2 l2 a2 r2)
    1.80 +  case (3 l1 a1 n1 r1 l2 a2 n2 r2)
    1.81    show ?case (is "ltree(merge ?t1 ?t2)")
    1.82    proof cases
    1.83      assume "a1 \<le> a2"
    1.84 @@ -173,14 +173,14 @@
    1.85  proof(induction t)
    1.86    case Leaf show ?case by simp
    1.87  next
    1.88 -  case (Node n l a r)
    1.89 +  case (Node l a n r)
    1.90    hence "rank r \<le> rank l" by simp
    1.91    hence *: "(2::nat) ^ rank r \<le> 2 ^ rank l" by simp
    1.92 -  have "(2::nat) ^ rank \<langle>n, l, a, r\<rangle> = 2 ^ rank r + 2 ^ rank r"
    1.93 +  have "(2::nat) ^ rank \<langle>l, a, n, r\<rangle> = 2 ^ rank r + 2 ^ rank r"
    1.94      by(simp add: mult_2)
    1.95    also have "\<dots> \<le> size1 l + size1 r"
    1.96      using Node * by (simp del: power_increasing_iff)
    1.97 -  also have "\<dots> = size1 \<langle>n, l, a, r\<rangle>" by simp
    1.98 +  also have "\<dots> = size1 \<langle>l, a, n, r\<rangle>" by simp
    1.99    finally show ?case .
   1.100  qed
   1.101  
   1.102 @@ -189,16 +189,16 @@
   1.103  fun t_merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> nat" where
   1.104  "t_merge Leaf t2 = 1" |
   1.105  "t_merge t2 Leaf = 1" |
   1.106 -"t_merge (Node n1 l1 a1 r1 =: t1) (Node n2 l2 a2 r2 =: t2) =
   1.107 +"t_merge (Node l1 a1 n1 r1 =: t1) (Node l2 a2 n2 r2 =: t2) =
   1.108    (if a1 \<le> a2 then 1 + t_merge r1 t2
   1.109     else 1 + t_merge r2 t1)"
   1.110  
   1.111  definition t_insert :: "'a::ord \<Rightarrow> 'a lheap \<Rightarrow> nat" where
   1.112 -"t_insert x t = t_merge (Node 1 Leaf x Leaf) t"
   1.113 +"t_insert x t = t_merge (Node Leaf x 1 Leaf) t"
   1.114  
   1.115  fun t_del_min :: "'a::ord lheap \<Rightarrow> nat" where
   1.116  "t_del_min Leaf = 1" |
   1.117 -"t_del_min (Node n l a r) = t_merge l r"
   1.118 +"t_del_min (Node l a n r) = t_merge l r"
   1.119  
   1.120  lemma t_merge_rank: "t_merge l r \<le> rank l + rank r + 1"
   1.121  proof(induction l r rule: merge.induct)
   1.122 @@ -213,7 +213,7 @@
   1.123  by linarith
   1.124  
   1.125  corollary t_insert_log: "ltree t \<Longrightarrow> t_insert x t \<le> log 2 (size1 t) + 2"
   1.126 -using t_merge_log[of "Node 1 Leaf x Leaf" t]
   1.127 +using t_merge_log[of "Node Leaf x 1 Leaf" t]
   1.128  by(simp add: t_insert_def split: tree.split)
   1.129  
   1.130  (* FIXME mv ? *)
   1.131 @@ -234,7 +234,7 @@
   1.132  proof(cases t)
   1.133    case Leaf thus ?thesis using assms by simp
   1.134  next
   1.135 -  case [simp]: (Node _ t1 _ t2)
   1.136 +  case [simp]: (Node t1 _ _ t2)
   1.137    have "t_del_min t = t_merge t1 t2" by simp
   1.138    also have "\<dots> \<le> log 2 (size1 t1) + log 2 (size1 t2) + 1"
   1.139      using \<open>ltree t\<close> by (auto simp: t_merge_log simp del: t_merge.simps)