added invar empty
authornipkow
Tue Oct 13 17:06:37 2015 +0200 (2015-10-13)
changeset 614285e1938107371
parent 61427 3c69ea85f8dd
child 61429 63fb7a68a12c
added invar empty
src/HOL/Data_Structures/AVL_Set.thy
src/HOL/Data_Structures/Map_by_Ordered.thy
src/HOL/Data_Structures/RBT_Set.thy
src/HOL/Data_Structures/Set_by_Ordered.thy
src/HOL/Data_Structures/Tree_Set.thy
     1.1 --- a/src/HOL/Data_Structures/AVL_Set.thy	Tue Oct 13 14:49:15 2015 +0100
     1.2 +++ b/src/HOL/Data_Structures/AVL_Set.thy	Tue Oct 13 17:06:37 2015 +0200
     1.3 @@ -130,9 +130,7 @@
     1.4    case 3 thus ?case by(simp add: inorder_insert)
     1.5  next
     1.6    case 4 thus ?case by(simp add: inorder_delete)
     1.7 -next
     1.8 -  case 5 thus ?case ..
     1.9 -qed
    1.10 +qed (rule TrueI)+
    1.11  
    1.12  
    1.13  subsection {* AVL invariants *}
     2.1 --- a/src/HOL/Data_Structures/Map_by_Ordered.thy	Tue Oct 13 14:49:15 2015 +0100
     2.2 +++ b/src/HOL/Data_Structures/Map_by_Ordered.thy	Tue Oct 13 17:06:37 2015 +0200
     2.3 @@ -15,6 +15,7 @@
     2.4  assumes "map_of empty = (\<lambda>_. None)"
     2.5  assumes "invar m \<Longrightarrow> map_of(update a b m) = (map_of m)(a := Some b)"
     2.6  assumes "invar m \<Longrightarrow> map_of(delete a m) = (map_of m)(a := None)"
     2.7 +assumes "invar empty"
     2.8  assumes "invar m \<Longrightarrow> invar(update a b m)"
     2.9  assumes "invar m \<Longrightarrow> invar(delete a m)"
    2.10  
    2.11 @@ -32,6 +33,7 @@
    2.12    inorder(update a b t) = upd_list a b (inorder t)"
    2.13  assumes delete: "wf t \<and> sorted1 (inorder t) \<Longrightarrow>
    2.14    inorder(delete a t) = del_list a (inorder t)"
    2.15 +assumes wf_empty:  "wf empty"
    2.16  assumes wf_insert: "wf t \<and> sorted1 (inorder t) \<Longrightarrow> wf(update a b t)"
    2.17  assumes wf_delete: "wf t \<and> sorted1 (inorder t) \<Longrightarrow> wf(delete a t)"
    2.18  begin
    2.19 @@ -45,9 +47,11 @@
    2.20  next
    2.21    case 3 thus ?case by(simp add: delete map_of_del_list)
    2.22  next
    2.23 -  case 4 thus ?case by(simp add: update wf_insert sorted_upd_list)
    2.24 +  case 4 thus ?case by(simp add: empty wf_empty)
    2.25  next
    2.26 -  case 5 thus ?case by (auto simp: delete wf_delete sorted_del_list)
    2.27 +  case 5 thus ?case by(simp add: update wf_insert sorted_upd_list)
    2.28 +next
    2.29 +  case 6 thus ?case by (auto simp: delete wf_delete sorted_del_list)
    2.30  qed
    2.31  
    2.32  end
     3.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Tue Oct 13 14:49:15 2015 +0100
     3.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Tue Oct 13 17:06:37 2015 +0200
     3.3 @@ -77,8 +77,6 @@
     3.4    case 3 thus ?case by(simp add: inorder_insert)
     3.5  next
     3.6    case 4 thus ?case by(simp add: inorder_delete)
     3.7 -next
     3.8 -  case 5 thus ?case ..
     3.9 -qed
    3.10 +qed (rule TrueI)+
    3.11  
    3.12  end
     4.1 --- a/src/HOL/Data_Structures/Set_by_Ordered.thy	Tue Oct 13 14:49:15 2015 +0100
     4.2 +++ b/src/HOL/Data_Structures/Set_by_Ordered.thy	Tue Oct 13 17:06:37 2015 +0200
     4.3 @@ -17,6 +17,7 @@
     4.4  assumes "invar s \<Longrightarrow> isin s a = (a \<in> set s)"
     4.5  assumes "invar s \<Longrightarrow> set(insert a s) = Set.insert a (set s)"
     4.6  assumes "invar s \<Longrightarrow> set(delete a s) = set s - {a}"
     4.7 +assumes "invar empty"
     4.8  assumes "invar s \<Longrightarrow> invar(insert a s)"
     4.9  assumes "invar s \<Longrightarrow> invar(delete a s)"
    4.10  
    4.11 @@ -34,6 +35,7 @@
    4.12    inorder(insert a t) = ins_list a (inorder t)"
    4.13  assumes delete: "wf t \<and> sorted(inorder t) \<Longrightarrow>
    4.14    inorder(delete a t) = del_list a (inorder t)"
    4.15 +assumes wf_empty:  "wf empty"
    4.16  assumes wf_insert: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(insert a t)"
    4.17  assumes wf_delete: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(delete a t)"
    4.18  begin
    4.19 @@ -50,9 +52,11 @@
    4.20    case (4 s a) show ?case
    4.21      using delete[OF 4, of a] 4 by (auto simp: distinct_if_sorted)
    4.22  next
    4.23 -  case 5 thus ?case by(simp add: insert wf_insert sorted_ins_list)
    4.24 +  case 5 thus ?case by(simp add: empty wf_empty)
    4.25  next
    4.26 -  case 6 thus ?case by (auto simp: delete wf_delete sorted_del_list)
    4.27 +  case 6 thus ?case by(simp add: insert wf_insert sorted_ins_list)
    4.28 +next
    4.29 +  case 7 thus ?case by (auto simp: delete wf_delete sorted_del_list)
    4.30  qed
    4.31  
    4.32  end
     5.1 --- a/src/HOL/Data_Structures/Tree_Set.thy	Tue Oct 13 14:49:15 2015 +0100
     5.2 +++ b/src/HOL/Data_Structures/Tree_Set.thy	Tue Oct 13 17:06:37 2015 +0200
     5.3 @@ -68,8 +68,6 @@
     5.4    case 3 thus ?case by(simp add: inorder_insert)
     5.5  next
     5.6    case 4 thus ?case by(simp add: inorder_delete)
     5.7 -next
     5.8 -  case 5 thus ?case by(simp)
     5.9 -qed
    5.10 +qed (rule TrueI)+
    5.11  
    5.12  end