Theory Misc

section ‹General purpose definitions and lemmas›

theory Misc imports 
  Main
begin

text ‹A handy abbreviation when working with maps›
abbreviation make_map :: "'a set ⇒ 'b ⇒ ('a ⇀ 'b)" ("[ _ |=> _ ]")
where
  "[ks |=> v] ≡ λk. if k ∈ ks then Some v else None"

text ‹Projecting the components of a triple›
definition "fst3 ≡ fst"
definition "snd3 ≡ fst ∘ snd"
definition "thd3 ≡ snd ∘ snd"

lemma fst3_simp [simp]: "fst3 (a,b,c) = a" by (simp add: fst3_def)
lemma snd3_simp [simp]: "snd3 (a,b,c) = b" by (simp add: snd3_def)
lemma thd3_simp [simp]: "thd3 (a,b,c) = c" by (simp add: thd3_def)

end