# HG changeset patch # User nipkow # Date 1446745088 -3600 # Node ID 1d2907d0ed73dff4718af177572b959ee8e48c6b # Parent c3974cd2d381dd317f2bd9a3a671816393e09e54 tuned diff -r c3974cd2d381 -r 1d2907d0ed73 src/HOL/Data_Structures/AVL_Set.thy --- a/src/HOL/Data_Structures/AVL_Set.thy Thu Nov 05 11:59:45 2015 +0100 +++ b/src/HOL/Data_Structures/AVL_Set.thy Thu Nov 05 18:38:08 2015 +0100 @@ -119,7 +119,7 @@ interpretation Set_by_Ordered where empty = Leaf and isin = isin and insert = insert and delete = delete -and inorder = inorder and wf = "\_. True" +and inorder = inorder and inv = "\_. True" proof (standard, goal_cases) case 1 show ?case by simp next diff -r c3974cd2d381 -r 1d2907d0ed73 src/HOL/Data_Structures/RBT_Set.thy --- a/src/HOL/Data_Structures/RBT_Set.thy Thu Nov 05 11:59:45 2015 +0100 +++ b/src/HOL/Data_Structures/RBT_Set.thy Thu Nov 05 18:38:08 2015 +0100 @@ -73,7 +73,7 @@ interpretation Set_by_Ordered where empty = Leaf and isin = isin and insert = insert and delete = delete -and inorder = inorder and wf = "\_. True" +and inorder = inorder and inv = "\_. True" proof (standard, goal_cases) case 1 show ?case by simp next diff -r c3974cd2d381 -r 1d2907d0ed73 src/HOL/Data_Structures/Set_by_Ordered.thy --- a/src/HOL/Data_Structures/Set_by_Ordered.thy Thu Nov 05 11:59:45 2015 +0100 +++ b/src/HOL/Data_Structures/Set_by_Ordered.thy Thu Nov 05 18:38:08 2015 +0100 @@ -27,21 +27,21 @@ fixes delete :: "'a \ 't \ 't" fixes isin :: "'t \ 'a \ bool" fixes inorder :: "'t \ 'a list" -fixes wf :: "'t \ bool" +fixes inv :: "'t \ bool" assumes empty: "inorder empty = []" -assumes isin: "wf t \ sorted(inorder t) \ +assumes isin: "inv t \ sorted(inorder t) \ isin t x = (x \ elems (inorder t))" -assumes insert: "wf t \ sorted(inorder t) \ +assumes insert: "inv t \ sorted(inorder t) \ inorder(insert x t) = ins_list x (inorder t)" -assumes delete: "wf t \ sorted(inorder t) \ +assumes delete: "inv t \ sorted(inorder t) \ inorder(delete x t) = del_list x (inorder t)" -assumes wf_empty: "wf empty" -assumes wf_insert: "wf t \ sorted(inorder t) \ wf(insert x t)" -assumes wf_delete: "wf t \ sorted(inorder t) \ wf(delete x t)" +assumes inv_empty: "inv empty" +assumes inv_insert: "inv t \ sorted(inorder t) \ inv(insert x t)" +assumes inv_delete: "inv t \ sorted(inorder t) \ inv(delete x t)" begin sublocale Set - empty insert delete isin "elems o inorder" "\t. wf t \ sorted(inorder t)" + empty insert delete isin "elems o inorder" "\t. inv t \ sorted(inorder t)" proof(standard, goal_cases) case 1 show ?case by (auto simp: empty) next @@ -52,11 +52,11 @@ case (4 s x) show ?case using delete[OF 4, of x] 4 by (auto simp: distinct_if_sorted) next - case 5 thus ?case by(simp add: empty wf_empty) + case 5 thus ?case by(simp add: empty inv_empty) next - case 6 thus ?case by(simp add: insert wf_insert sorted_ins_list) + case 6 thus ?case by(simp add: insert inv_insert sorted_ins_list) next - case 7 thus ?case by (auto simp: delete wf_delete sorted_del_list) + case 7 thus ?case by (auto simp: delete inv_delete sorted_del_list) qed end diff -r c3974cd2d381 -r 1d2907d0ed73 src/HOL/Data_Structures/Splay_Set.thy --- a/src/HOL/Data_Structures/Splay_Set.thy Thu Nov 05 11:59:45 2015 +0100 +++ b/src/HOL/Data_Structures/Splay_Set.thy Thu Nov 05 18:38:08 2015 +0100 @@ -198,7 +198,7 @@ interpretation Set_by_Ordered where empty = Leaf and isin = isin and insert = insert -and delete = delete and inorder = inorder and wf = "\_. True" +and delete = delete and inorder = inorder and inv = "\_. True" proof (standard, goal_cases) case 2 thus ?case by(simp add: isin_set) next diff -r c3974cd2d381 -r 1d2907d0ed73 src/HOL/Data_Structures/Tree234_Set.thy --- a/src/HOL/Data_Structures/Tree234_Set.thy Thu Nov 05 11:59:45 2015 +0100 +++ b/src/HOL/Data_Structures/Tree234_Set.thy Thu Nov 05 18:38:08 2015 +0100 @@ -497,7 +497,7 @@ interpretation Set_by_Ordered where empty = Leaf and isin = isin and insert = insert and delete = delete -and inorder = inorder and wf = bal +and inorder = inorder and inv = bal proof (standard, goal_cases) case 2 thus ?case by(simp add: isin_set) next diff -r c3974cd2d381 -r 1d2907d0ed73 src/HOL/Data_Structures/Tree23_Set.thy --- a/src/HOL/Data_Structures/Tree23_Set.thy Thu Nov 05 11:59:45 2015 +0100 +++ b/src/HOL/Data_Structures/Tree23_Set.thy Thu Nov 05 18:38:08 2015 +0100 @@ -356,7 +356,7 @@ interpretation Set_by_Ordered where empty = Leaf and isin = isin and insert = insert and delete = delete -and inorder = inorder and wf = bal +and inorder = inorder and inv = bal proof (standard, goal_cases) case 2 thus ?case by(simp add: isin_set) next diff -r c3974cd2d381 -r 1d2907d0ed73 src/HOL/Data_Structures/Tree_Set.thy --- a/src/HOL/Data_Structures/Tree_Set.thy Thu Nov 05 11:59:45 2015 +0100 +++ b/src/HOL/Data_Structures/Tree_Set.thy Thu Nov 05 18:38:08 2015 +0100 @@ -61,7 +61,7 @@ interpretation Set_by_Ordered where empty = Leaf and isin = isin and insert = insert and delete = delete -and inorder = inorder and wf = "\_. True" +and inorder = inorder and inv = "\_. True" proof (standard, goal_cases) case 1 show ?case by simp next