Theory JHelper

section ‹General purpose definitions and lemmas›

theory JHelper imports
  Main
begin

lemma Collect_iff: 
  "a ∈ {x . P x} ≡ P a"
by auto

lemma diff_diff_eq:
  assumes "C ⊆ B"
  shows "(A - C) - (B - C) = A - B"
using assms by auto

lemma nth_in_set:
  "⟦ i < length xs ; xs ! i = x ⟧ ⟹ x ∈ set xs" by auto

lemma disjI [intro]:
  assumes "¬ P ⟹ Q"
  shows "P ∨ Q"
using assms by auto

lemma empty_eq_Plus_conv: 
  "({} = A <+> B) = (A = {} ∧ B = {})"
by auto

subsection ‹Projection functions on triples›

definition fst3 :: "'a × 'b × 'c ⇒ 'a"
where "fst3 ≡ fst"

definition snd3 :: "'a × 'b × 'c ⇒ 'b"
where "snd3 ≡ fst ∘ snd"

definition thd3 :: "'a × 'b × 'c ⇒ 'c"
where "thd3 ≡ snd ∘ snd"

lemma fst3_simp: 
  "⋀a b c. fst3 (a,b,c) = a" 
by (auto simp add: fst3_def)

lemma snd3_simp: 
  "⋀a b c. snd3 (a,b,c) = b" 
by (auto simp add: snd3_def)

lemma thd3_simp: 
  "⋀a b c. thd3 (a,b,c) = c" 
by (auto simp add: thd3_def)

lemma tripleI:
  fixes T U
  assumes "fst3 T = fst3 U" 
      and "snd3 T = snd3 U" 
      and "thd3 T = thd3 U" 
  shows "T = U" 
by (metis assms fst3_def snd3_def thd3_def o_def surjective_pairing)

end