src/HOL/Data_Structures/Brother12_Set.thy
changeset 68431 b294e095f64c
parent 68020 6aade817bee5
     1.1 --- a/src/HOL/Data_Structures/Brother12_Set.thy	Tue Jun 12 07:18:18 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/Brother12_Set.thy	Tue Jun 12 17:18:40 2018 +0200
     1.3 @@ -19,6 +19,9 @@
     1.4    L2 'a |
     1.5    N3 "'a bro" 'a "'a bro" 'a "'a bro"
     1.6  
     1.7 +definition empty :: "'a bro" where
     1.8 +"empty = N0"
     1.9 +
    1.10  fun inorder :: "'a bro \<Rightarrow> 'a list" where
    1.11  "inorder N0 = []" |
    1.12  "inorder (N1 t) = inorder t" |
    1.13 @@ -465,7 +468,7 @@
    1.14  subsection "Overall correctness"
    1.15  
    1.16  interpretation Set_by_Ordered
    1.17 -where empty = N0 and isin = isin and insert = insert.insert
    1.18 +where empty = empty and isin = isin and insert = insert.insert
    1.19  and delete = delete.delete and inorder = inorder and inv = "\<lambda>t. \<exists>h. t \<in> B h"
    1.20  proof (standard, goal_cases)
    1.21    case 2 thus ?case by(auto intro!: isin_set)
    1.22 @@ -477,7 +480,7 @@
    1.23    case 6 thus ?case using insert.insert_type by blast
    1.24  next
    1.25    case 7 thus ?case using delete.delete_type by blast
    1.26 -qed auto
    1.27 +qed (auto simp: empty_def)
    1.28  
    1.29  
    1.30  subsection \<open>Height-Size Relation\<close>