src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy
author wenzelm
Thu Jul 24 11:54:15 2014 +0200 (2014-07-24)
changeset 57641 dc59f147b27d
parent 55931 62156e694f3d
permissions -rw-r--r--
more robust notation BNF_Def.convol, which is private to main HOL, but may cause syntax ambiguities nonetheless (e.g. List.thy);
blanchet@55075
     1
(*  Title:      HOL/BNF_Examples/Derivation_Trees/Prelim.thy
blanchet@48975
     2
    Author:     Andrei Popescu, TU Muenchen
blanchet@48975
     3
    Copyright   2012
blanchet@48975
     4
blanchet@49463
     5
Preliminaries.
blanchet@48975
     6
*)
blanchet@48975
     7
blanchet@49463
     8
header {* Preliminaries *}
blanchet@48975
     9
blanchet@48975
    10
theory Prelim
blanchet@55129
    11
imports "~~/src/HOL/Library/FSet"
blanchet@48975
    12
begin
blanchet@48975
    13
wenzelm@57641
    14
notation BNF_Def.convol ("\<langle>(_,/ _)\<rangle>")
blanchet@55091
    15
blanchet@48975
    16
declare fset_to_fset[simp]
blanchet@48975
    17
wenzelm@57641
    18
lemma fst_snd_convol_o[simp]: "\<langle>fst o s, snd o s\<rangle> = s"
blanchet@48975
    19
apply(rule ext) by (simp add: convol_def)
blanchet@48975
    20
blanchet@49514
    21
abbreviation sm_abbrev (infix "\<oplus>" 60)
blanchet@55931
    22
where "f \<oplus> g \<equiv> Sum_Type.map_sum f g"
blanchet@48975
    23
blanchet@55931
    24
lemma map_sum_InlD: "(f \<oplus> g) z = Inl x \<Longrightarrow> \<exists>y. z = Inl y \<and> f y = x"
blanchet@48975
    25
by (cases z) auto
blanchet@48975
    26
blanchet@55931
    27
lemma map_sum_InrD: "(f \<oplus> g) z = Inr x \<Longrightarrow> \<exists>y. z = Inr y \<and> g y = x"
blanchet@48975
    28
by (cases z) auto
blanchet@48975
    29
blanchet@55414
    30
abbreviation case_sum_abbrev ("[[_,_]]" 800)
blanchet@55414
    31
where "[[f,g]] \<equiv> Sum_Type.case_sum f g"
blanchet@48975
    32
blanchet@48975
    33
lemma Inl_oplus_elim:
blanchet@48975
    34
assumes "Inl tr \<in> (id \<oplus> f) ` tns"
blanchet@48975
    35
shows "Inl tr \<in> tns"
blanchet@48975
    36
using assms apply clarify by (case_tac x, auto)
blanchet@48975
    37
blanchet@48975
    38
lemma Inl_oplus_iff[simp]: "Inl tr \<in> (id \<oplus> f) ` tns \<longleftrightarrow> Inl tr \<in> tns"
blanchet@48975
    39
using Inl_oplus_elim
blanchet@55931
    40
by (metis id_def image_iff map_sum.simps(1))
blanchet@48975
    41
blanchet@48975
    42
lemma Inl_m_oplus[simp]: "Inl -` (id \<oplus> f) ` tns = Inl -` tns"
blanchet@48975
    43
using Inl_oplus_iff unfolding vimage_def by auto
blanchet@48975
    44
blanchet@48975
    45
lemma Inr_oplus_elim:
blanchet@48975
    46
assumes "Inr tr \<in> (id \<oplus> f) ` tns"
blanchet@48975
    47
shows "\<exists> n. Inr n \<in> tns \<and> f n = tr"
blanchet@48975
    48
using assms apply clarify by (case_tac x, auto)
blanchet@48975
    49
blanchet@49514
    50
lemma Inr_oplus_iff[simp]:
blanchet@48975
    51
"Inr tr \<in> (id \<oplus> f) ` tns \<longleftrightarrow> (\<exists> n. Inr n \<in> tns \<and> f n = tr)"
blanchet@48975
    52
apply (rule iffI)
blanchet@48975
    53
 apply (metis Inr_oplus_elim)
blanchet@55931
    54
by (metis image_iff map_sum.simps(2))
blanchet@48975
    55
blanchet@48975
    56
lemma Inr_m_oplus[simp]: "Inr -` (id \<oplus> f) ` tns = f ` (Inr -` tns)"
blanchet@48975
    57
using Inr_oplus_iff unfolding vimage_def by auto
blanchet@48975
    58
blanchet@48975
    59
lemma Inl_Inr_image_cong:
blanchet@48975
    60
assumes "Inl -` A = Inl -` B" and "Inr -` A = Inr -` B"
blanchet@48975
    61
shows "A = B"
blanchet@48975
    62
apply safe using assms apply(case_tac x, auto) by(case_tac x, auto)
blanchet@48975
    63
blanchet@48975
    64
end