src/HOL/Data_Structures/Set_by_Ordered.thy
 author nipkow Mon Sep 21 14:44:32 2015 +0200 (2015-09-21) changeset 61203 a8a8eca85801 child 61428 5e1938107371 permissions -rw-r--r--
New subdirectory for functional data structures
 nipkow@61203 ` 1` ```(* Author: Tobias Nipkow *) ``` nipkow@61203 ` 2` nipkow@61203 ` 3` ```section {* Implementing Ordered Sets *} ``` nipkow@61203 ` 4` nipkow@61203 ` 5` ```theory Set_by_Ordered ``` nipkow@61203 ` 6` ```imports List_Ins_Del ``` nipkow@61203 ` 7` ```begin ``` nipkow@61203 ` 8` nipkow@61203 ` 9` ```locale Set = ``` nipkow@61203 ` 10` ```fixes empty :: "'s" ``` nipkow@61203 ` 11` ```fixes insert :: "'a \ 's \ 's" ``` nipkow@61203 ` 12` ```fixes delete :: "'a \ 's \ 's" ``` nipkow@61203 ` 13` ```fixes isin :: "'s \ 'a \ bool" ``` nipkow@61203 ` 14` ```fixes set :: "'s \ 'a set" ``` nipkow@61203 ` 15` ```fixes invar :: "'s \ bool" ``` nipkow@61203 ` 16` ```assumes "set empty = {}" ``` nipkow@61203 ` 17` ```assumes "invar s \ isin s a = (a \ set s)" ``` nipkow@61203 ` 18` ```assumes "invar s \ set(insert a s) = Set.insert a (set s)" ``` nipkow@61203 ` 19` ```assumes "invar s \ set(delete a s) = set s - {a}" ``` nipkow@61203 ` 20` ```assumes "invar s \ invar(insert a s)" ``` nipkow@61203 ` 21` ```assumes "invar s \ invar(delete a s)" ``` nipkow@61203 ` 22` nipkow@61203 ` 23` ```locale Set_by_Ordered = ``` nipkow@61203 ` 24` ```fixes empty :: "'t" ``` nipkow@61203 ` 25` ```fixes insert :: "'a::linorder \ 't \ 't" ``` nipkow@61203 ` 26` ```fixes delete :: "'a \ 't \ 't" ``` nipkow@61203 ` 27` ```fixes isin :: "'t \ 'a \ bool" ``` nipkow@61203 ` 28` ```fixes inorder :: "'t \ 'a list" ``` nipkow@61203 ` 29` ```fixes wf :: "'t \ bool" ``` nipkow@61203 ` 30` ```assumes empty: "inorder empty = []" ``` nipkow@61203 ` 31` ```assumes isin: "wf t \ sorted(inorder t) \ ``` nipkow@61203 ` 32` ``` isin t a = (a \ elems (inorder t))" ``` nipkow@61203 ` 33` ```assumes insert: "wf t \ sorted(inorder t) \ ``` nipkow@61203 ` 34` ``` inorder(insert a t) = ins_list a (inorder t)" ``` nipkow@61203 ` 35` ```assumes delete: "wf t \ sorted(inorder t) \ ``` nipkow@61203 ` 36` ``` inorder(delete a t) = del_list a (inorder t)" ``` nipkow@61203 ` 37` ```assumes wf_insert: "wf t \ sorted(inorder t) \ wf(insert a t)" ``` nipkow@61203 ` 38` ```assumes wf_delete: "wf t \ sorted(inorder t) \ wf(delete a t)" ``` nipkow@61203 ` 39` ```begin ``` nipkow@61203 ` 40` nipkow@61203 ` 41` ```sublocale Set ``` nipkow@61203 ` 42` ``` empty insert delete isin "elems o inorder" "\t. wf t \ sorted(inorder t)" ``` nipkow@61203 ` 43` ```proof(standard, goal_cases) ``` nipkow@61203 ` 44` ``` case 1 show ?case by (auto simp: empty) ``` nipkow@61203 ` 45` ```next ``` nipkow@61203 ` 46` ``` case 2 thus ?case by(simp add: isin) ``` nipkow@61203 ` 47` ```next ``` nipkow@61203 ` 48` ``` case 3 thus ?case by(simp add: insert) ``` nipkow@61203 ` 49` ```next ``` nipkow@61203 ` 50` ``` case (4 s a) show ?case ``` nipkow@61203 ` 51` ``` using delete[OF 4, of a] 4 by (auto simp: distinct_if_sorted) ``` nipkow@61203 ` 52` ```next ``` nipkow@61203 ` 53` ``` case 5 thus ?case by(simp add: insert wf_insert sorted_ins_list) ``` nipkow@61203 ` 54` ```next ``` nipkow@61203 ` 55` ``` case 6 thus ?case by (auto simp: delete wf_delete sorted_del_list) ``` nipkow@61203 ` 56` ```qed ``` nipkow@61203 ` 57` nipkow@61203 ` 58` ```end ``` nipkow@61203 ` 59` nipkow@61203 ` 60` ```end ```