isabelle: src/HOL/Data_Structures/Lookup2.thy@8348bba699e6 (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
70755 3fb16bed5d6c replaced new type ('a,'b) tree by old type ('a'b) tree. nipkow* parents: 68413 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" \|
70755 3fb16bed5d6c replaced new type ('a,'b) tree by old type ('a'b) tree. nipkow* parents: 68413 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"
70755 3fb16bed5d6c replaced new type ('a,'b) tree by old type ('a'b) tree. nipkow* parents: 68413 diff changeset	19	by(induction t rule: tree2_induct) (auto simp: map_of_simps split: option.split)
61232 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>
	Fri, 31 Jul 2020 12:54:46 +0100
changeset 72089	8348bba699e6
parent 70755	3fb16bed5d6c
permissions	-rw-r--r--