author nipkow Thu Nov 05 18:38:08 2015 +0100 (2015-11-05) changeset 61588 1d2907d0ed73 parent 61587 c3974cd2d381 child 61589 d07d0d5a572b
tuned
```     1.1 --- a/src/HOL/Data_Structures/AVL_Set.thy	Thu Nov 05 11:59:45 2015 +0100
1.2 +++ b/src/HOL/Data_Structures/AVL_Set.thy	Thu Nov 05 18:38:08 2015 +0100
1.3 @@ -119,7 +119,7 @@
1.4
1.5  interpretation Set_by_Ordered
1.6  where empty = Leaf and isin = isin and insert = insert and delete = delete
1.7 -and inorder = inorder and wf = "\<lambda>_. True"
1.8 +and inorder = inorder and inv = "\<lambda>_. True"
1.9  proof (standard, goal_cases)
1.10    case 1 show ?case by simp
1.11  next
```
```     2.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Thu Nov 05 11:59:45 2015 +0100
2.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Thu Nov 05 18:38:08 2015 +0100
2.3 @@ -73,7 +73,7 @@
2.4
2.5  interpretation Set_by_Ordered
2.6  where empty = Leaf and isin = isin and insert = insert and delete = delete
2.7 -and inorder = inorder and wf = "\<lambda>_. True"
2.8 +and inorder = inorder and inv = "\<lambda>_. True"
2.9  proof (standard, goal_cases)
2.10    case 1 show ?case by simp
2.11  next
```
```     3.1 --- a/src/HOL/Data_Structures/Set_by_Ordered.thy	Thu Nov 05 11:59:45 2015 +0100
3.2 +++ b/src/HOL/Data_Structures/Set_by_Ordered.thy	Thu Nov 05 18:38:08 2015 +0100
3.3 @@ -27,21 +27,21 @@
3.4  fixes delete :: "'a \<Rightarrow> 't \<Rightarrow> 't"
3.5  fixes isin :: "'t \<Rightarrow> 'a \<Rightarrow> bool"
3.6  fixes inorder :: "'t \<Rightarrow> 'a list"
3.7 -fixes wf :: "'t \<Rightarrow> bool"
3.8 +fixes inv :: "'t \<Rightarrow> bool"
3.9  assumes empty: "inorder empty = []"
3.10 -assumes isin: "wf t \<and> sorted(inorder t) \<Longrightarrow>
3.11 +assumes isin: "inv t \<and> sorted(inorder t) \<Longrightarrow>
3.12    isin t x = (x \<in> elems (inorder t))"
3.13 -assumes insert: "wf t \<and> sorted(inorder t) \<Longrightarrow>
3.14 +assumes insert: "inv t \<and> sorted(inorder t) \<Longrightarrow>
3.15    inorder(insert x t) = ins_list x (inorder t)"
3.16 -assumes delete: "wf t \<and> sorted(inorder t) \<Longrightarrow>
3.17 +assumes delete: "inv t \<and> sorted(inorder t) \<Longrightarrow>
3.18    inorder(delete x t) = del_list x (inorder t)"
3.19 -assumes wf_empty:  "wf empty"
3.20 -assumes wf_insert: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(insert x t)"
3.21 -assumes wf_delete: "wf t \<and> sorted(inorder t) \<Longrightarrow> wf(delete x t)"
3.22 +assumes inv_empty:  "inv empty"
3.23 +assumes inv_insert: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(insert x t)"
3.24 +assumes inv_delete: "inv t \<and> sorted(inorder t) \<Longrightarrow> inv(delete x t)"
3.25  begin
3.26
3.27  sublocale Set
3.28 -  empty insert delete isin "elems o inorder" "\<lambda>t. wf t \<and> sorted(inorder t)"
3.29 +  empty insert delete isin "elems o inorder" "\<lambda>t. inv t \<and> sorted(inorder t)"
3.30  proof(standard, goal_cases)
3.31    case 1 show ?case by (auto simp: empty)
3.32  next
3.33 @@ -52,11 +52,11 @@
3.34    case (4 s x) show ?case
3.35      using delete[OF 4, of x] 4 by (auto simp: distinct_if_sorted)
3.36  next
3.37 -  case 5 thus ?case by(simp add: empty wf_empty)
3.38 +  case 5 thus ?case by(simp add: empty inv_empty)
3.39  next
3.40 -  case 6 thus ?case by(simp add: insert wf_insert sorted_ins_list)
3.41 +  case 6 thus ?case by(simp add: insert inv_insert sorted_ins_list)
3.42  next
3.43 -  case 7 thus ?case by (auto simp: delete wf_delete sorted_del_list)
3.44 +  case 7 thus ?case by (auto simp: delete inv_delete sorted_del_list)
3.45  qed
3.46
3.47  end
```
```     4.1 --- a/src/HOL/Data_Structures/Splay_Set.thy	Thu Nov 05 11:59:45 2015 +0100
4.2 +++ b/src/HOL/Data_Structures/Splay_Set.thy	Thu Nov 05 18:38:08 2015 +0100
4.3 @@ -198,7 +198,7 @@
4.4
4.5  interpretation Set_by_Ordered
4.6  where empty = Leaf and isin = isin and insert = insert
4.7 -and delete = delete and inorder = inorder and wf = "\<lambda>_. True"
4.8 +and delete = delete and inorder = inorder and inv = "\<lambda>_. True"
4.9  proof (standard, goal_cases)
4.10    case 2 thus ?case by(simp add: isin_set)
4.11  next
```
```     5.1 --- a/src/HOL/Data_Structures/Tree234_Set.thy	Thu Nov 05 11:59:45 2015 +0100
5.2 +++ b/src/HOL/Data_Structures/Tree234_Set.thy	Thu Nov 05 18:38:08 2015 +0100
5.3 @@ -497,7 +497,7 @@
5.4
5.5  interpretation Set_by_Ordered
5.6  where empty = Leaf and isin = isin and insert = insert and delete = delete
5.7 -and inorder = inorder and wf = bal
5.8 +and inorder = inorder and inv = bal
5.9  proof (standard, goal_cases)
5.10    case 2 thus ?case by(simp add: isin_set)
5.11  next
```
```     6.1 --- a/src/HOL/Data_Structures/Tree23_Set.thy	Thu Nov 05 11:59:45 2015 +0100
6.2 +++ b/src/HOL/Data_Structures/Tree23_Set.thy	Thu Nov 05 18:38:08 2015 +0100
6.3 @@ -356,7 +356,7 @@
6.4
6.5  interpretation Set_by_Ordered
6.6  where empty = Leaf and isin = isin and insert = insert and delete = delete
6.7 -and inorder = inorder and wf = bal
6.8 +and inorder = inorder and inv = bal
6.9  proof (standard, goal_cases)
6.10    case 2 thus ?case by(simp add: isin_set)
6.11  next
```
```     7.1 --- a/src/HOL/Data_Structures/Tree_Set.thy	Thu Nov 05 11:59:45 2015 +0100
7.2 +++ b/src/HOL/Data_Structures/Tree_Set.thy	Thu Nov 05 18:38:08 2015 +0100
7.3 @@ -61,7 +61,7 @@
7.4
7.5  interpretation Set_by_Ordered
7.6  where empty = Leaf and isin = isin and insert = insert and delete = delete
7.7 -and inorder = inorder and wf = "\<lambda>_. True"
7.8 +and inorder = inorder and inv = "\<lambda>_. True"
7.9  proof (standard, goal_cases)
7.10    case 1 show ?case by simp
7.11  next
```