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);
```     1 (*  Title:      HOL/BNF_Examples/Derivation_Trees/Prelim.thy
```
```     2     Author:     Andrei Popescu, TU Muenchen
```
```     3     Copyright   2012
```
```     4
```
```     5 Preliminaries.
```
```     6 *)
```
```     7
```
```     8 header {* 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`