Theory Prelim

(*  Title:      HOL/Datatype_Examples/Derivation_Trees/Prelim.thy
    Author:     Andrei Popescu, TU Muenchen
    Copyright   2012

Preliminaries.
*)

section ‹Preliminaries›

theory Prelim
imports "HOL-Library.FSet"
begin

notation BNF_Def.convol ("⟨(_,/ _)⟩")

declare fset_to_fset[simp]

lemma fst_snd_convol_o[simp]: "⟨fst o s, snd o s⟩ = s"
apply(rule ext) by (simp add: convol_def)

abbreviation sm_abbrev (infix "⊕" 60)
where "f ⊕ g ≡ Sum_Type.map_sum f g"

lemma map_sum_InlD: "(f ⊕ g) z = Inl x ⟹ ∃y. z = Inl y ∧ f y = x"
by (cases z) auto

lemma map_sum_InrD: "(f ⊕ g) z = Inr x ⟹ ∃y. z = Inr y ∧ g y = x"
by (cases z) auto

abbreviation case_sum_abbrev ("[[_,_]]" 800)
where "[[f,g]] ≡ Sum_Type.case_sum f g"

lemma Inl_oplus_elim:
assumes "Inl tr ∈ (id ⊕ f) ` tns"
shows "Inl tr ∈ tns"
using assms apply clarify by (case_tac x, auto)

lemma Inl_oplus_iff[simp]: "Inl tr ∈ (id ⊕ f) ` tns ⟷ Inl tr ∈ tns"
using Inl_oplus_elim
by (metis id_def image_iff map_sum.simps(1))

lemma Inl_m_oplus[simp]: "Inl -` (id ⊕ f) ` tns = Inl -` tns"
using Inl_oplus_iff unfolding vimage_def by auto

lemma Inr_oplus_elim:
assumes "Inr tr ∈ (id ⊕ f) ` tns"
shows "∃ n. Inr n ∈ tns ∧ f n = tr"
using assms apply clarify by (case_tac x, auto)

lemma Inr_oplus_iff[simp]:
"Inr tr ∈ (id ⊕ f) ` tns ⟷ (∃ n. Inr n ∈ tns ∧ f n = tr)"
apply (rule iffI)
 apply (metis Inr_oplus_elim)
by (metis image_iff map_sum.simps(2))

lemma Inr_m_oplus[simp]: "Inr -` (id ⊕ f) ` tns = f ` (Inr -` tns)"
using Inr_oplus_iff unfolding vimage_def by auto

lemma Inl_Inr_image_cong:
assumes "Inl -` A = Inl -` B" and "Inr -` A = Inr -` B"
shows "A = B"
apply safe using assms apply(case_tac x, auto) by(case_tac x, auto)

end