src/HOL/Datatype_Examples/Derivation_Trees/Prelim.thy
author wenzelm
Sun Nov 02 18:21:45 2014 +0100 (2014-11-02)
changeset 58889 5b7a9633cfa8
parent 58309 a09ec6daaa19
child 62390 842917225d56
permissions -rw-r--r--
modernized header uniformly as section;
     1 (*  Title:      HOL/Datatype_Examples/Derivation_Trees/Prelim.thy
     2     Author:     Andrei Popescu, TU Muenchen
     3     Copyright   2012
     4 
     5 Preliminaries.
     6 *)
     7 
     8 section {* Preliminaries *}
     9 
    10 theory Prelim
    11 imports "~~/src/HOL/Library/FSet"
    12 begin
    13 
    14 notation BNF_Def.convol ("\<langle>(_,/ _)\<rangle>")
    15 
    16 declare fset_to_fset[simp]
    17 
    18 lemma fst_snd_convol_o[simp]: "\<langle>fst o s, snd o s\<rangle> = s"
    19 apply(rule ext) by (simp add: convol_def)
    20 
    21 abbreviation sm_abbrev (infix "\<oplus>" 60)
    22 where "f \<oplus> g \<equiv> Sum_Type.map_sum f g"
    23 
    24 lemma map_sum_InlD: "(f \<oplus> g) z = Inl x \<Longrightarrow> \<exists>y. z = Inl y \<and> f y = x"
    25 by (cases z) auto
    26 
    27 lemma map_sum_InrD: "(f \<oplus> g) z = Inr x \<Longrightarrow> \<exists>y. z = Inr y \<and> g y = x"
    28 by (cases z) auto
    29 
    30 abbreviation case_sum_abbrev ("[[_,_]]" 800)
    31 where "[[f,g]] \<equiv> Sum_Type.case_sum f g"
    32 
    33 lemma Inl_oplus_elim:
    34 assumes "Inl tr \<in> (id \<oplus> f) ` tns"
    35 shows "Inl tr \<in> tns"
    36 using assms apply clarify by (case_tac x, auto)
    37 
    38 lemma Inl_oplus_iff[simp]: "Inl tr \<in> (id \<oplus> f) ` tns \<longleftrightarrow> Inl tr \<in> tns"
    39 using Inl_oplus_elim
    40 by (metis id_def image_iff map_sum.simps(1))
    41 
    42 lemma Inl_m_oplus[simp]: "Inl -` (id \<oplus> f) ` tns = Inl -` tns"
    43 using Inl_oplus_iff unfolding vimage_def by auto
    44 
    45 lemma Inr_oplus_elim:
    46 assumes "Inr tr \<in> (id \<oplus> f) ` tns"
    47 shows "\<exists> n. Inr n \<in> tns \<and> f n = tr"
    48 using assms apply clarify by (case_tac x, auto)
    49 
    50 lemma Inr_oplus_iff[simp]:
    51 "Inr tr \<in> (id \<oplus> f) ` tns \<longleftrightarrow> (\<exists> n. Inr n \<in> tns \<and> f n = tr)"
    52 apply (rule iffI)
    53  apply (metis Inr_oplus_elim)
    54 by (metis image_iff map_sum.simps(2))
    55 
    56 lemma Inr_m_oplus[simp]: "Inr -` (id \<oplus> f) ` tns = f ` (Inr -` tns)"
    57 using Inr_oplus_iff unfolding vimage_def by auto
    58 
    59 lemma Inl_Inr_image_cong:
    60 assumes "Inl -` A = Inl -` B" and "Inr -` A = Inr -` B"
    61 shows "A = B"
    62 apply safe using assms apply(case_tac x, auto) by(case_tac x, auto)
    63 
    64 end