header {* \isaheader{Hashable Interface} *}
theory Intf_Hash
imports
Main
"../../Lib/HashCode"
"../../../Automatic_Refinement/Automatic_Refinement"
begin
type_synonym 'a eq = "'a => 'a => bool"
type_synonym 'k bhc = "nat => 'k => nat"
subsection {* Abstract and concrete hash functions *}
definition is_bounded_hashcode :: "('c×'a) set => 'c eq => 'c bhc => bool"
where "is_bounded_hashcode R eq bhc ≡
((eq,op =) ∈ R -> R -> bool_rel) ∧
(∀n x y. eq x y --> bhc n x = bhc n y) ∧
(∀n x. 1 < n --> bhc n x < n)"
definition abstract_bounded_hashcode :: "('c×'a) set => 'c bhc => 'a bhc"
where "abstract_bounded_hashcode Rk bhc n x' ≡
if x' ∈ Range Rk
then THE c. ∃x. (x,x') ∈ Rk ∧ bhc n x = c
else 0"
lemma is_bounded_hashcodeI[intro]:
"((eq,op =) ∈ R -> R -> bool_rel) ==>
(!!x y n. eq x y ==> bhc n x = bhc n y) ==>
(!!x n. 1 < n ==> bhc n x < n) ==> is_bounded_hashcode R eq bhc"
unfolding is_bounded_hashcode_def by force
lemma is_bounded_hashcodeD[dest]:
assumes "is_bounded_hashcode R eq bhc"
shows "(eq,op =) ∈ R -> R -> bool_rel" and
"!!n x y. eq x y ==> bhc n x = bhc n y" and
"!!n x. 1 < n ==> bhc n x < n"
using assms unfolding is_bounded_hashcode_def by simp_all
lemma bounded_hashcode_welldefined:
assumes BHC: "is_bounded_hashcode Rk eq bhc" and
R1: "(x1,x') ∈ Rk" and R2: "(x2,x') ∈ Rk"
shows "bhc n x1 = bhc n x2"
proof-
from is_bounded_hashcodeD[OF BHC] have "(eq,op =) ∈ Rk -> Rk -> bool_rel" by simp
with R1 R2 have "eq x1 x2" by (force dest: fun_relD)
thus ?thesis using BHC by blast
qed
lemma abstract_bhc_correct[intro]:
assumes "is_bounded_hashcode Rk eq bhc"
shows "(bhc, abstract_bounded_hashcode Rk bhc) ∈
nat_rel -> Rk -> nat_rel" (is "(bhc, ?bhc') ∈ _")
proof (intro fun_relI)
fix n n' x x'
assume A: "(n,n') ∈ nat_rel" and B: "(x,x') ∈ Rk"
hence C: "n = n'" and D: "x' ∈ Range Rk" by auto
have "?bhc' n' x' = bhc n x"
unfolding abstract_bounded_hashcode_def
apply (simp add: C D, rule)
apply (intro exI conjI, fact B, rule refl)
apply (elim exE conjE, hypsubst,
erule bounded_hashcode_welldefined[OF assms _ B])
done
thus "(bhc n x, ?bhc' n' x') ∈ nat_rel" by simp
qed
lemma abstract_bhc_is_bhc[intro]:
fixes Rk :: "('c×'a) set"
assumes bhc: "is_bounded_hashcode Rk eq bhc"
shows "is_bounded_hashcode Id op= (abstract_bounded_hashcode Rk bhc)"
(is "is_bounded_hashcode _ op= ?bhc'")
proof
fix x'::'a and y'::'a and n'::nat assume "x' = y'"
thus "?bhc' n' x' = ?bhc' n' y'" by simp
next
fix x'::'a and n'::nat assume "1 < n'"
from abstract_bhc_correct[OF bhc] show "?bhc' n' x' < n'"
proof (cases "x' ∈ Range Rk")
case False
with `1 < n'` show ?thesis
unfolding abstract_bounded_hashcode_def by simp
next
case True
then obtain x where "(x,x') ∈ Rk" ..
have "(n',n') ∈ nat_rel" ..
from abstract_bhc_correct[OF assms] have "?bhc' n' x' = bhc n' x"
apply -
apply (drule fun_relD[OF _ `(n',n') ∈ nat_rel`],
drule fun_relD[OF _ `(x,x') ∈ Rk`], simp)
done
also from `1 < n'` and bhc have "... < n'" by blast
finally show "?bhc' n' x' < n'" .
qed
qed simp
lemma hashable_bhc_is_bhc[autoref_ga_rules]:
"[|STRUCT_EQ_tag eq op=; REL_FORCE_ID R|] ==> is_bounded_hashcode R eq bounded_hashcode_nat"
unfolding is_bounded_hashcode_def
by (simp add: bounded_hashcode_nat_bounds)
subsection {* Default hash map size *}
definition is_valid_def_hm_size :: "'k itself => nat => bool"
where "is_valid_def_hm_size type n ≡ n > 1"
lemma hashable_def_size_is_def_size[autoref_ga_rules]:
shows "is_valid_def_hm_size TYPE('k::hashable) (def_hashmap_size TYPE('k))"
unfolding is_valid_def_hm_size_def by (fact def_hashmap_size)
end