# Theory JHelper

Up to index of Isabelle/HOL/ribbonproofs

theory JHelper
imports Main
`header {* General purpose definitions and lemmas *}theory JHelper imports  Mainbeginlemma Collect_iff:   "a ∈ {x . P x} ≡ P a"by autolemma diff_diff_eq:  assumes "C ⊆ B"  shows "(A - C) - (B - C) = A - B"using assms by autolemma nth_in_set:  "[| i < length xs ; xs ! i = x |] ==> x ∈ set xs" by autolemma disjI [intro]:  assumes "¬ P ==> Q"  shows "P ∨ Q"using assms by autolemma empty_eq_Plus_conv:   "({} = A <+> B) = (A = {} ∧ B = {})"by autosubsection {* 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`