Theory JHelper

Up to index of Isabelle/HOL/ribbonproofs

theory JHelper
imports Main
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