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