diff --git a/thys/Priority_Queue_Braun/Priority_Queue_Braun.thy b/thys/Priority_Queue_Braun/Priority_Queue_Braun.thy
--- a/thys/Priority_Queue_Braun/Priority_Queue_Braun.thy
+++ b/thys/Priority_Queue_Braun/Priority_Queue_Braun.thy
@@ -1,224 +1,225 @@
 section "Priority Queues Based on Braun Trees"
 
 theory Priority_Queue_Braun
 imports
   "HOL-Library.Tree_Multiset"
   "HOL-Library.Pattern_Aliases"
   "HOL-Data_Structures.Priority_Queue_Specs"
   "HOL-Data_Structures.Braun_Tree"
 begin
 
 subsection "Introduction"
 
 text\<open>Braun, Rem and Hoogerwoord \cite{BraunRem,Hoogerwoord} used
 specific balanced binary trees, often called Braun trees (where in
 each node with subtrees $l$ and $r$, $size(r) \le size(l) \le
 size(r)+1$), to implement flexible arrays. Paulson \cite{Paulson}
 (based on code supplied by Okasaki)
 implemented priority queues via Braun trees. This theory verifies
 Paulsons's implementation, with small simplifications.\<close>
 
 text \<open>Direct proof of logarithmic height. Also follows from the fact that Braun
 trees are balanced (proved in the base theory).\<close>
 
 lemma height_size_braun: "braun t \<Longrightarrow> 2 ^ (height t) \<le> 2 * size t + 1"
 proof(induction t)
   case (Node t1)
   show ?case
   proof (cases "height t1")
     case 0 thus ?thesis using Node by simp
   next
     case (Suc n)
     hence "2 ^ n \<le> size t1" using Node by simp
     thus ?thesis using Suc Node by(auto simp: max_def)
   qed
 qed simp
 
 
 subsection "Get Minimum"
 
-lemma get_min: "\<lbrakk> heap h;  h \<noteq> Leaf \<rbrakk> \<Longrightarrow> value h = Min_mset (mset_tree h)"
+fun get_min :: "'a::linorder tree \<Rightarrow> 'a" where
+"get_min (Node l a r) = a"
+
+lemma get_min: "\<lbrakk> heap t;  t \<noteq> Leaf \<rbrakk> \<Longrightarrow> get_min t = Min_mset (mset_tree t)"
 by (auto simp add: eq_Min_iff neq_Leaf_iff)
 
 subsection \<open>Insertion\<close>
 
 hide_const (open) insert
 
 fun insert :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
 "insert a Leaf = Node Leaf a Leaf" |
 "insert a (Node l x r) =
  (if a < x then Node (insert x r) a l else Node (insert a r) x l)"
 
-value "fold insert [0::int,1,2,3,-55,-5] Leaf"
-
 lemma size_insert[simp]: "size(insert x t) = size t + 1"
 by(induction t arbitrary: x) auto
 
 lemma mset_insert: "mset_tree(insert x t) = {#x#} + mset_tree t"
 by(induction t arbitrary: x) (auto simp: ac_simps)
 
 lemma set_insert[simp]: "set_tree(insert x t) = {x} \<union> (set_tree t)"
 by(simp add: mset_insert flip: set_mset_tree)
 
 lemma braun_insert: "braun t \<Longrightarrow> braun(insert x t)"
 by(induction t arbitrary: x) auto
 
 lemma heap_insert: "heap t \<Longrightarrow> heap(insert x t)"
 by(induction t arbitrary: x) (auto  simp add: ball_Un)
 
 
 subsection \<open>Deletion\<close>
 
 text \<open>Slightly simpler definition of @{text del_left}
 which avoids the need to appeal to the Braun invariant.\<close>
 
 fun del_left :: "'a tree \<Rightarrow> 'a * 'a tree" where
 "del_left (Node Leaf x r) = (x,r)" |
 "del_left (Node l x r) = (let (y,l') = del_left l in (y,Node r x l'))"
 
 lemma del_left_mset_plus:
   "del_left t = (x,t') \<Longrightarrow> t \<noteq> Leaf
   \<Longrightarrow> mset_tree t = {#x#} + mset_tree t'"
   by (induction t arbitrary: x t' rule: del_left.induct;
     auto split: prod.splits)
 
 lemma del_left_mset:
   "del_left t = (x,t') \<Longrightarrow> t \<noteq> Leaf
   \<Longrightarrow> x \<in># mset_tree t \<and> mset_tree t' = mset_tree t - {#x#}"
 by (simp add: del_left_mset_plus)
 
 lemma del_left_set:
   "del_left t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> set_tree t = {x} \<union> set_tree t'"
 by(simp add: del_left_mset_plus flip: set_mset_tree)
 
 lemma del_left_heap:
   "del_left t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> heap t \<Longrightarrow> heap t'"
   by (induction t arbitrary: x t' rule: del_left.induct;
     fastforce split: prod.splits dest: del_left_set[THEN equalityD2])
 
 lemma del_left_size:
   "del_left t = (x,t') \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> size t = size t' + 1"
   by(induction t arbitrary: x t' rule: del_left.induct;
     auto split: prod.splits)
 
 lemma del_left_braun:
   "del_left t = (x,t') \<Longrightarrow> braun t \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> braun t'"
   by(induction t arbitrary: x t' rule: del_left.induct;
     auto split: prod.splits dest: del_left_size)
 
 context includes pattern_aliases
 begin
 
 text \<open>Slightly simpler definition: \<open>_\<close> instead of @{const Leaf} because of Braun invariant.\<close>
 
 function (sequential) sift_down :: "'a::linorder tree \<Rightarrow> 'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
 "sift_down Leaf a _ = Node Leaf a Leaf" |
 "sift_down (Node Leaf x _) a Leaf =
   (if a \<le> x then Node (Node Leaf x Leaf) a Leaf
    else Node (Node Leaf a Leaf) x Leaf)" |
 "sift_down (Node l1 x1 r1 =: t1) a (Node l2 x2 r2 =: t2) =
   (if a \<le> x1 \<and> a \<le> x2
    then Node t1 a t2
    else if x1 \<le> x2 then Node (sift_down l1 a r1) x1 t2
         else Node t1 x2 (sift_down l2 a r2))"
 by pat_completeness auto
 termination
 by (relation "measure (%(l,a,r). size l + size r)") auto
 
 end
 
 lemma size_sift_down:
   "braun(Node l a r) \<Longrightarrow> size(sift_down l a r) = size l + size r + 1"
 by(induction l a r rule: sift_down.induct) (auto simp: Let_def)
 
 lemma braun_sift_down:
   "braun(Node l a r) \<Longrightarrow> braun(sift_down l a r)"
 by(induction l a r rule: sift_down.induct) (auto simp: size_sift_down Let_def)
 
 lemma mset_sift_down:
   "braun(Node l a r) \<Longrightarrow> mset_tree(sift_down l a r) = {#a#} + (mset_tree l + mset_tree r)"
 by(induction l a r rule: sift_down.induct) (auto simp: ac_simps Let_def)
 
 lemma set_sift_down: "braun(Node l a r)
   \<Longrightarrow> set_tree(sift_down l a r) = {a} \<union> (set_tree l \<union> set_tree r)"
 by(drule arg_cong[where f=set_mset, OF mset_sift_down]) (simp)
 
 lemma heap_sift_down:
   "braun(Node l a r) \<Longrightarrow> heap l \<Longrightarrow> heap r \<Longrightarrow> heap(sift_down l a r)"
 by (induction l a r rule: sift_down.induct) (auto simp: set_sift_down ball_Un Let_def)
 
 fun del_min :: "'a::linorder tree \<Rightarrow> 'a tree" where
 "del_min Leaf = Leaf" |
 "del_min (Node Leaf x r) = Leaf" |
 "del_min (Node l x r) = (let (y,l') = del_left l in sift_down r y l')"
 
 lemma braun_del_min: "braun t \<Longrightarrow> braun(del_min t)"
 apply(cases t rule: del_min.cases)
   apply simp
  apply simp
 apply (fastforce split: prod.split intro!: braun_sift_down
   dest: del_left_size del_left_braun)
 done
 
 lemma heap_del_min: "heap t \<Longrightarrow> braun t \<Longrightarrow> heap(del_min t)"
 apply(cases t rule: del_min.cases)
   apply simp
  apply simp
 apply (fastforce split: prod.split intro!: heap_sift_down
   dest: del_left_size del_left_braun del_left_heap)
 done
 
 lemma size_del_min: assumes "braun t" shows "size(del_min t) = size t - 1"
 proof(cases t rule: del_min.cases)
   case [simp]: (3 ll b lr a r)
   { fix y l' assume "del_left (Node ll b lr) = (y,l')"
     hence "size(sift_down r y l') = size t - 1" using assms
     by(subst size_sift_down) (auto dest: del_left_size del_left_braun) }
   thus ?thesis by(auto split: prod.split)
 qed (insert assms, auto)
 
 lemma mset_del_min: assumes "braun t" "t \<noteq> Leaf"
-shows "mset_tree(del_min t) = mset_tree t - {#value t#}"
+shows "mset_tree(del_min t) = mset_tree t - {#get_min t#}"
 proof(cases t rule: del_min.cases)
   case 1 with assms show ?thesis by simp
 next
   case 2 with assms show ?thesis by (simp)
 next
   case [simp]: (3 ll b lr a r)
   have "mset_tree(sift_down r y l') = mset_tree t - {#a#}"
     if del: "del_left (Node ll b lr) = (y,l')" for y l'
     using assms del_left_mset[OF del] del_left_size[OF del]
       del_left_braun[OF del] del_left_mset_plus[OF del]
     apply (subst mset_sift_down)
     apply (auto simp: ac_simps del_left_mset_plus[OF del])
     done
   thus ?thesis by(auto split: prod.split)
 qed
 
 
 text \<open>Last step: prove all axioms of the priority queue specification:\<close>
 
 interpretation braun: Priority_Queue
 where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
 and insert = insert and del_min = del_min
-and get_min = "value" and invar = "\<lambda>h. braun h \<and> heap h"
+and get_min = get_min and invar = "\<lambda>h. braun h \<and> heap h"
 and mset = mset_tree
 proof(standard, goal_cases)
   case 1 show ?case by simp
 next
   case 2 show ?case by simp
 next
   case 3 show ?case by(simp add: mset_insert)
 next
   case 4 thus ?case by(simp add: mset_del_min)
 next
   case 5 thus ?case using get_min mset_tree.simps(1) by blast
 next
   case 6 thus ?case by(simp)
 next
   case 7 thus ?case by(simp add: heap_insert braun_insert)
 next
   case 8 thus ?case by(simp add: heap_del_min braun_del_min)
 qed
 
 end
diff --git a/thys/Priority_Queue_Braun/Priority_Queue_Braun2.thy b/thys/Priority_Queue_Braun/Priority_Queue_Braun2.thy
--- a/thys/Priority_Queue_Braun/Priority_Queue_Braun2.thy
+++ b/thys/Priority_Queue_Braun/Priority_Queue_Braun2.thy
@@ -1,129 +1,129 @@
 section "Priority Queues Based on Braun Trees 2"
 
 theory Priority_Queue_Braun2
 imports Priority_Queue_Braun
 begin
 
 text \<open>This is the version verified by Jean-Christophe Filliâtre with the help of the Why3 system
 \<^url>\<open>http://toccata.lri.fr/gallery/braun_trees.en.html\<close>.
 Only the deletion function (\<open>del_min2\<close> below) differs from Paulson's version.
 But the difference turns out to be minor --- see below.\<close>
 
 
 subsection "Function \<open>del_min2\<close>"
 
 fun le_root :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> bool" where
 "le_root a t = (t = Leaf \<or> a \<le> value t)"
 
 fun replace_min :: "'a::linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
 "replace_min x (Node l _ r) =
   (if le_root x l & le_root x r then Node l x r
    else
      let a = value l in
      if le_root a r then Node (replace_min x l) a r
      else Node l (value r) (replace_min x r))"
 
 fun merge :: "'a::linorder tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
 "merge l Leaf = l" |
 "merge (Node l1 a1 r1) (Node l2 a2 r2) =
    (if a1 \<le> a2 then Node (Node l2 a2 r2) a1 (merge l1 r1)
     else let (x, l') = del_left (Node l1 a1 r1)
          in Node (replace_min x (Node l2 a2 r2)) a2 l')"
 
 fun del_min2 where
 "del_min2 Leaf = Leaf" |
 "del_min2 (Node l x r) = merge l r"
 
 
 subsection "Correctness Proof"
 
 text \<open>It turns out that @{const replace_min} is just @{const sift_down} in disguise:\<close>
 
 lemma replace_min_sift_down: "braun (Node l a r) \<Longrightarrow> replace_min x (Node l a r) = sift_down l x r"
 by(induction l x r rule: sift_down.induct)(auto)
 
 text \<open>This means that @{const del_min2} is merely a slight optimization of @{const del_min}:
 instead of calling @{const del_left} right away, @{const merge} can take advantage of the case
 where the smaller element is at the root of the left heap and can be moved up without complications.
 However, on average this is just the case on the first level.\<close>
 
 text \<open>Function @{const merge}:\<close>
 
 lemma mset_tree_merge:
   "braun (Node l x r) \<Longrightarrow> mset_tree(merge l r) = mset_tree l + mset_tree r"
 by(induction l r rule: merge.induct)
   (auto simp: Let_def tree.set_sel(2) mset_sift_down replace_min_sift_down
         simp del: replace_min.simps dest!: del_left_mset split!: prod.split)
 
 lemma heap_merge:
   "\<lbrakk> braun (Node l x r); heap l; heap r \<rbrakk> \<Longrightarrow> heap(merge l r)"
 proof(induction l r rule: merge.induct)
   case 1 thus ?case by simp
 next
   case (2 l1 a1 r1 l2 a2 r2)
   show ?case
   proof cases
     assume "a1 \<le> a2"
     thus ?thesis using 2 by(auto simp: ball_Un mset_tree_merge simp flip: set_mset_tree)
   next
     assume "\<not> a1 \<le> a2"
     let ?l = "Node l1 a1 r1" let ?r = "Node l2 a2 r2"
     have "braun ?r" using "2.prems"(1) by auto
     obtain x l' where dl: "del_left ?l = (x, l')" by (metis surj_pair)
     from del_left_heap[OF this _ "2.prems"(2)] have "heap l'" by auto
     have hr: "heap(replace_min x ?r)" using \<open>braun ?r\<close> "2.prems"(3)
       by(simp add: heap_sift_down neq_Leaf_iff replace_min_sift_down del: replace_min.simps)
     have 0: "\<forall>x \<in> set_tree ?l. a2 \<le> x" using "2.prems"(2) \<open>\<not> a1 \<le> a2\<close> by (auto simp: ball_Un)
     moreover have "set_tree l' \<subseteq> set_tree ?l" "x \<in> set_tree ?l"
       using del_left_mset[OF dl] by (auto simp flip: set_mset_tree dest:in_diffD simp: union_iff)
     ultimately have 1: "\<forall>x \<in> set_tree l'. a2 \<le> x" by blast
     have "\<forall>x \<in> set_tree ?r. a2 \<le> x" using \<open>heap ?r\<close> by auto
     thus ?thesis
       using \<open>\<not> a1 \<le> a2\<close> dl \<open>heap(replace_min x ?r)\<close> \<open>heap l'\<close> \<open>x \<in> set_tree ?l\<close> 0 1 \<open>braun ?r\<close>
       by(auto simp: mset_sift_down replace_min_sift_down simp flip: set_mset_tree
               simp del: replace_min.simps)
   qed
 next
   case 3 thus ?case by simp
 qed
 
 lemma del_left_braun_size:
   "del_left t = (x,t') \<Longrightarrow> braun t \<Longrightarrow> t \<noteq> Leaf \<Longrightarrow> braun t' \<and> size t = size t' + 1"
 by (simp add: del_left_braun del_left_size)
 
 lemma braun_size_merge:
   "braun (Node l x r) \<Longrightarrow> braun(merge l r) \<and> size(merge l r) = size l + size r"
 apply(induction l r rule: merge.induct)
 apply(auto simp: size_sift_down braun_sift_down replace_min_sift_down
            simp del: replace_min.simps
            dest!: del_left_braun_size split!: prod.split)
 done
 
 
 text \<open>Last step: prove all axioms of the priority queue specification:\<close>
 
 interpretation braun: Priority_Queue
 where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
 and insert = insert and del_min = del_min2
-and get_min = "value" and invar = "\<lambda>h. braun h \<and> heap h"
+and get_min = get_min and invar = "\<lambda>h. braun h \<and> heap h"
 and mset = mset_tree
 proof(standard, goal_cases)
   case 1 show ?case by simp
 next
   case 2 show ?case by simp
 next
   case 3 show ?case by(simp add: mset_insert)
 next
   case 4 thus ?case by(auto simp: mset_tree_merge neq_Leaf_iff)
 next
   case 5 thus ?case using get_min mset_tree.simps(1) by blast
 next
   case 6 thus ?case by(simp)
 next
   case 7 thus ?case by(simp add: heap_insert braun_insert)
 next
   case 8 thus ?case by(auto simp: heap_merge braun_size_merge neq_Leaf_iff)
 qed
 
 
 end