|
1 (* Title: HOL/BNF/Examples/Infinite_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 "../../BNF" |
|
12 begin |
|
13 |
|
14 declare fset_to_fset[simp] |
|
15 |
|
16 lemma fst_snd_convol_o[simp]: "<fst o s, snd o s> = s" |
|
17 apply(rule ext) by (simp add: convol_def) |
|
18 |
|
19 abbreviation sm_abbrev (infix "\<oplus>" 60) |
|
20 where "f \<oplus> g \<equiv> Sum_Type.sum_map f g" |
|
21 |
|
22 lemma sum_map_InlD: "(f \<oplus> g) z = Inl x \<Longrightarrow> \<exists>y. z = Inl y \<and> f y = x" |
|
23 by (cases z) auto |
|
24 |
|
25 lemma sum_map_InrD: "(f \<oplus> g) z = Inr x \<Longrightarrow> \<exists>y. z = Inr y \<and> g y = x" |
|
26 by (cases z) auto |
|
27 |
|
28 abbreviation sum_case_abbrev ("[[_,_]]" 800) |
|
29 where "[[f,g]] \<equiv> Sum_Type.sum_case f g" |
|
30 |
|
31 lemma inj_Inl[simp]: "inj Inl" unfolding inj_on_def by auto |
|
32 lemma inj_Inr[simp]: "inj Inr" unfolding inj_on_def by auto |
|
33 |
|
34 lemma Inl_oplus_elim: |
|
35 assumes "Inl tr \<in> (id \<oplus> f) ` tns" |
|
36 shows "Inl tr \<in> tns" |
|
37 using assms apply clarify by (case_tac x, auto) |
|
38 |
|
39 lemma Inl_oplus_iff[simp]: "Inl tr \<in> (id \<oplus> f) ` tns \<longleftrightarrow> Inl tr \<in> tns" |
|
40 using Inl_oplus_elim |
|
41 by (metis id_def image_iff sum_map.simps(1)) |
|
42 |
|
43 lemma Inl_m_oplus[simp]: "Inl -` (id \<oplus> f) ` tns = Inl -` tns" |
|
44 using Inl_oplus_iff unfolding vimage_def by auto |
|
45 |
|
46 lemma Inr_oplus_elim: |
|
47 assumes "Inr tr \<in> (id \<oplus> f) ` tns" |
|
48 shows "\<exists> n. Inr n \<in> tns \<and> f n = tr" |
|
49 using assms apply clarify by (case_tac x, auto) |
|
50 |
|
51 lemma Inr_oplus_iff[simp]: |
|
52 "Inr tr \<in> (id \<oplus> f) ` tns \<longleftrightarrow> (\<exists> n. Inr n \<in> tns \<and> f n = tr)" |
|
53 apply (rule iffI) |
|
54 apply (metis Inr_oplus_elim) |
|
55 by (metis image_iff sum_map.simps(2)) |
|
56 |
|
57 lemma Inr_m_oplus[simp]: "Inr -` (id \<oplus> f) ` tns = f ` (Inr -` tns)" |
|
58 using Inr_oplus_iff unfolding vimage_def by auto |
|
59 |
|
60 lemma Inl_Inr_image_cong: |
|
61 assumes "Inl -` A = Inl -` B" and "Inr -` A = Inr -` B" |
|
62 shows "A = B" |
|
63 apply safe using assms apply(case_tac x, auto) by(case_tac x, auto) |
|
64 |
|
65 |
|
66 |
|
67 end |