tuned
authornipkow
Thu Nov 05 18:38:08 2015 +0100 (2015-11-05)
changeset 615881d2907d0ed73
parent 61587 c3974cd2d381
child 61589 d07d0d5a572b
tuned
src/HOL/Data_Structures/AVL_Set.thy
src/HOL/Data_Structures/RBT_Set.thy
src/HOL/Data_Structures/Set_by_Ordered.thy
src/HOL/Data_Structures/Splay_Set.thy
src/HOL/Data_Structures/Tree234_Set.thy
src/HOL/Data_Structures/Tree23_Set.thy
src/HOL/Data_Structures/Tree_Set.thy
     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