# HG changeset patch
# User nipkow
# Date 1449602519 -3600
# Node ID 81d34cf268d8e599ebc99e6b3ac9ac5f3af891d0
# Parent  fc1556774cfe1f8c2a358d082142abae9839fd88
tightened invariant

diff -r fc1556774cfe -r 81d34cf268d8 src/HOL/Data_Structures/Brother12_Map.thy
--- a/src/HOL/Data_Structures/Brother12_Map.thy	Mon Dec 07 20:19:59 2015 +0100
+++ b/src/HOL/Data_Structures/Brother12_Map.thy	Tue Dec 08 20:21:59 2015 +0100
@@ -108,8 +108,8 @@
 done
 
 lemma update_type:
-  "t \<in> T h \<Longrightarrow> update x y t \<in> T h \<union> T (Suc h)"
-unfolding update_def by (metis Un_iff upd_type tree_type1 tree_type2)
+  "t \<in> B h \<Longrightarrow> update x y t \<in> B h \<union> B (Suc h)"
+unfolding update_def by (metis upd_type tree_type)
 
 end
 
@@ -186,9 +186,9 @@
 qed auto
 
 lemma delete_type:
-  "t \<in> T h \<Longrightarrow> delete x t \<in> T h \<union> T(h-1)"
+  "t \<in> B h \<Longrightarrow> delete x t \<in> B h \<union> B(h-1)"
 unfolding delete_def
-by (cases h) (simp, metis del_type tree_type Un_iff Suc_eq_plus1 diff_Suc_1)
+by (cases h) (simp, metis del_type(1) tree_type Suc_eq_plus1 diff_Suc_1)
 
 end
 
@@ -196,7 +196,7 @@
 
 interpretation Map_by_Ordered
 where empty = N0 and lookup = lookup and update = update.update
-and delete = delete.delete and inorder = inorder and inv = "\<lambda>t. \<exists>h. t \<in> T h"
+and delete = delete.delete and inorder = inorder and inv = "\<lambda>t. \<exists>h. t \<in> B h"
 proof (standard, goal_cases)
   case 2 thus ?case by(auto intro!: lookup_map_of)
 next
diff -r fc1556774cfe -r 81d34cf268d8 src/HOL/Data_Structures/Brother12_Set.thy
--- a/src/HOL/Data_Structures/Brother12_Set.thy	Mon Dec 07 20:19:59 2015 +0100
+++ b/src/HOL/Data_Structures/Brother12_Set.thy	Tue Dec 08 20:21:59 2015 +0100
@@ -219,12 +219,9 @@
 context insert
 begin
 
-lemma tree_type1: "t \<in> Bp h \<Longrightarrow> tree t \<in> B h \<union> B (Suc h)"
+lemma tree_type: "t \<in> Bp h \<Longrightarrow> tree t \<in> B h \<union> B (Suc h)"
 by(cases h rule: Bp.cases) auto
 
-lemma tree_type2: "t \<in> T h \<Longrightarrow> tree t \<in> T h"
-by(cases h) auto
-
 lemma n2_type:
   "(t1 \<in> Bp h \<and> t2 \<in> T h \<longrightarrow> n2 t1 a t2 \<in> Bp (Suc h)) \<and>
    (t1 \<in> T h \<and> t2 \<in> Bp h \<longrightarrow> n2 t1 a t2 \<in> Bp (Suc h))"
@@ -297,8 +294,8 @@
 qed
 
 lemma insert_type:
-  "t \<in> T h \<Longrightarrow> insert x t \<in> T h \<union> T (Suc h)"
-unfolding insert_def by (metis Un_iff ins_type tree_type1 tree_type2)
+  "t \<in> B h \<Longrightarrow> insert x t \<in> B h \<union> B (Suc h)"
+unfolding insert_def by (metis ins_type(1) tree_type)
 
 end
 
@@ -459,15 +456,12 @@
   { case 2 with Suc.IH(1) show ?case by auto }
 qed auto
 
-lemma tree_type:
-  "t \<in> Um (Suc h) \<Longrightarrow> tree t : T h"
-  "t \<in> T (Suc h) \<Longrightarrow> tree t : T h \<union> T(h+1)"
+lemma tree_type: "t \<in> T (h+1) \<Longrightarrow> tree t : B (h+1) \<union> B h"
 by(auto)
 
-lemma delete_type:
-  "t \<in> T h \<Longrightarrow> delete x t \<in> T h \<union> T(h-1)"
+lemma delete_type: "t \<in> B h \<Longrightarrow> delete x t \<in> B h \<union> B(h-1)"
 unfolding delete_def
-by (cases h) (simp, metis del_type tree_type Un_iff Suc_eq_plus1 diff_Suc_1)
+by (cases h) (simp, metis del_type(1) tree_type Suc_eq_plus1 diff_Suc_1)
 
 end
 
@@ -476,7 +470,7 @@
 
 interpretation Set_by_Ordered
 where empty = N0 and isin = isin and insert = insert.insert
-and delete = delete.delete and inorder = inorder and inv = "\<lambda>t. \<exists>h. t \<in> T h"
+and delete = delete.delete and inorder = inorder and inv = "\<lambda>t. \<exists>h. t \<in> B h"
 proof (standard, goal_cases)
   case 2 thus ?case by(auto intro!: isin_set)
 next