isabelle: src/HOL/Data_Structures/Lookup2.thy@c64d778a593a (annotated)

61232 c46faf9762f7 added AVL and lookup function nipkow parents: diff changeset	1	(* Author: Tobias Nipkow *)
c46faf9762f7 added AVL and lookup function nipkow parents: diff changeset	2
c46faf9762f7 added AVL and lookup function nipkow parents: diff changeset	3	section \<open>Function \textit{lookup} for Tree2\<close>
c46faf9762f7 added AVL and lookup function nipkow parents: diff changeset	4
c46faf9762f7 added AVL and lookup function nipkow parents: diff changeset	5	theory Lookup2
c46faf9762f7 added AVL and lookup function nipkow parents: diff changeset	6	imports
c46faf9762f7 added AVL and lookup function nipkow parents: diff changeset	7	Tree2
61693 f6b9f528c89c converted lookup to cmp nipkow parents: 61232 diff changeset	8	Cmp
61232 c46faf9762f7 added AVL and lookup function nipkow parents: diff changeset	9	Map_by_Ordered
c46faf9762f7 added AVL and lookup function nipkow parents: diff changeset	10	begin
c46faf9762f7 added AVL and lookup function nipkow parents: diff changeset	11
63411 e051eea34990 got rid of class cmp; added height-size proofs by Daniel Stuewe nipkow parents: 62390 diff changeset	12	fun lookup :: "('a::linorder * 'b, 'c) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where
61232 c46faf9762f7 added AVL and lookup function nipkow parents: diff changeset	13	"lookup Leaf x = None" \|
c46faf9762f7 added AVL and lookup function nipkow parents: diff changeset	14	"lookup (Node _ l (a,b) r) x =
61693 f6b9f528c89c converted lookup to cmp nipkow parents: 61232 diff changeset	15	(case cmp x a of LT \<Rightarrow> lookup l x \| GT \<Rightarrow> lookup r x \| EQ \<Rightarrow> Some b)"
61232 c46faf9762f7 added AVL and lookup function nipkow parents: diff changeset	16
61790 0494964bb226 avoid name clashes nipkow parents: 61693 diff changeset	17	lemma lookup_map_of:
0494964bb226 avoid name clashes nipkow parents: 61693 diff changeset	18	"sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
61232 c46faf9762f7 added AVL and lookup function nipkow parents: diff changeset	19	by(induction t) (auto simp: map_of_simps split: option.split)
c46faf9762f7 added AVL and lookup function nipkow parents: diff changeset	20
62390 842917225d56 more canonical names nipkow parents: 61790 diff changeset	21	end

author	paulson <lp15@cam.ac.uk>
	Tue, 28 Feb 2017 15:17:57 +0000
changeset 65066	c64d778a593a
parent 63411	e051eea34990
child 67965	aaa31cd0caef
permissions	-rw-r--r--