src/HOL/Data_Structures/Set2_Join.thy
 changeset 68413 b56ed5010e69 parent 68261 035c78bb0a66 child 68484 59793df7f853
```     1.1 --- a/src/HOL/Data_Structures/Set2_Join.thy	Mon Jun 11 08:15:43 2018 +0200
1.2 +++ b/src/HOL/Data_Structures/Set2_Join.thy	Mon Jun 11 16:29:27 2018 +0200
1.3 @@ -28,7 +28,7 @@
1.4    \<Longrightarrow> bst (join l a r)"
1.5  assumes inv_Leaf: "inv \<langle>\<rangle>"
1.6  assumes inv_join: "\<lbrakk> inv l; inv r \<rbrakk> \<Longrightarrow> inv (join l k r)"
1.7 -assumes inv_Node: "\<lbrakk> inv (Node h l x r) \<rbrakk> \<Longrightarrow> inv l \<and> inv r"
1.8 +assumes inv_Node: "\<lbrakk> inv (Node l x h r) \<rbrakk> \<Longrightarrow> inv l \<and> inv r"
1.9  begin
1.10
1.11  declare set_join [simp]
1.12 @@ -36,7 +36,7 @@
1.13  subsection "\<open>split_min\<close>"
1.14
1.15  fun split_min :: "('a,'b) tree \<Rightarrow> 'a \<times> ('a,'b) tree" where
1.16 -"split_min (Node _ l x r) =
1.17 +"split_min (Node l x _ r) =
1.18    (if l = Leaf then (x,r) else let (m,l') = split_min l in (m, join l' x r))"
1.19
1.20  lemma split_min_set:
1.21 @@ -84,7 +84,7 @@
1.22
1.23  fun split :: "('a,'b)tree \<Rightarrow> 'a \<Rightarrow> ('a,'b)tree \<times> bool \<times> ('a,'b)tree" where
1.24  "split Leaf k = (Leaf, False, Leaf)" |
1.25 -"split (Node _ l a r) k =
1.26 +"split (Node l a _ r) k =
1.27    (if k < a then let (l1,b,l2) = split l k in (l1, b, join l2 a r) else
1.28     if a < k then let (r1,b,r2) = split r k in (join l a r1, b, r2)
1.29     else (l, True, r))"
1.30 @@ -145,7 +145,7 @@
1.31  "union t1 t2 =
1.32    (if t1 = Leaf then t2 else
1.33     if t2 = Leaf then t1 else
1.34 -   case t1 of Node _ l1 k r1 \<Rightarrow>
1.35 +   case t1 of Node l1 k _ r1 \<Rightarrow>
1.36     let (l2,_ ,r2) = split t2 k;
1.37         l' = union l1 l2; r' = union r1 r2
1.38     in join l' k r')"
1.39 @@ -181,7 +181,7 @@
1.40  "inter t1 t2 =
1.41    (if t1 = Leaf then Leaf else
1.42     if t2 = Leaf then Leaf else
1.43 -   case t1 of Node _ l1 k r1 \<Rightarrow>
1.44 +   case t1 of Node l1 k _ r1 \<Rightarrow>
1.45     let (l2,kin,r2) = split t2 k;
1.46         l' = inter l1 l2; r' = inter r1 r2
1.47     in if kin then join l' k r' else join2 l' r')"
1.48 @@ -196,7 +196,7 @@
1.49    proof (cases t1)
1.50      case Leaf thus ?thesis by (simp add: inter.simps)
1.51    next
1.52 -    case [simp]: (Node _ l1 k r1)
1.53 +    case [simp]: (Node l1 k _ r1)
1.54      show ?thesis
1.55      proof (cases "t2 = Leaf")
1.56        case True thus ?thesis by (simp add: inter.simps)
1.57 @@ -246,7 +246,7 @@
1.58  "diff t1 t2 =
1.59    (if t1 = Leaf then Leaf else
1.60     if t2 = Leaf then t1 else
1.61 -   case t2 of Node _ l2 k r2 \<Rightarrow>
1.62 +   case t2 of Node l2 k _ r2 \<Rightarrow>
1.63     let (l1,_,r1) = split t1 k;
1.64         l' = diff l1 l2; r' = diff r1 r2
1.65     in join2 l' r')"
1.66 @@ -261,7 +261,7 @@
1.67    proof (cases t2)
1.68      case Leaf thus ?thesis by (simp add: diff.simps)
1.69    next
1.70 -    case [simp]: (Node _ l2 k r2)
1.71 +    case [simp]: (Node l2 k _ r2)
1.72      show ?thesis
1.73      proof (cases "t1 = Leaf")
1.74        case True thus ?thesis by (simp add: diff.simps)
1.75 @@ -341,7 +341,7 @@
1.76  end
1.77
1.78  interpretation unbal: Set2_Join
1.79 -where join = "\<lambda>l x r. Node () l x r" and inv = "\<lambda>t. True"
1.80 +where join = "\<lambda>l x r. Node l x () r" and inv = "\<lambda>t. True"
1.81  proof (standard, goal_cases)
1.82    case 1 show ?case by simp
1.83  next
```