header {* 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 o snd"

definition thd3 :: "'a × 'b × 'c => 'c"

where "thd3 ≡ snd o 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