isabelle: src/HOL/Data_Structures/Lookup2.thy@dc85b5b3a532 (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
67965 aaa31cd0caef more name tuning nipkow parents: 63411 diff changeset	9	Map_Specs
61232 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" \|
68413 b56ed5010e69 tuned order of arguments nipkow parents: 67965 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, 22 Jan 2019 12:00:16 +0000
changeset 69712	dc85b5b3a532
parent 68413	b56ed5010e69
child 70755	3fb16bed5d6c
permissions	-rw-r--r--