author | popescua |
Tue, 16 Oct 2012 17:08:20 +0200 | |
changeset 49877 | b75555ec30a4 |
parent 49871 | 41ee3bfccb4d |
child 49879 | 5e323695f26e |
permissions | -rw-r--r-- |
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
1 |
(* Title: HOL/BNF/Examples/Derivation_Trees/Parallel.thy |
49463 | 2 |
Author: Andrei Popescu, TU Muenchen |
3 |
Copyright 2012 |
|
4 |
||
5 |
Parallel composition. |
|
6 |
*) |
|
7 |
||
8 |
header {* Parallel Composition *} |
|
9 |
||
49514 | 10 |
theory Parallel |
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
11 |
imports DTree |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
12 |
begin |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
13 |
|
49839 | 14 |
no_notation plus_class.plus (infixl "+" 65) |
15 |
no_notation Sublist.parallel (infixl "\<parallel>" 50) |
|
16 |
||
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
17 |
consts Nplus :: "N \<Rightarrow> N \<Rightarrow> N" (infixl "+" 60) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
18 |
|
49514 | 19 |
axiomatization where |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
20 |
Nplus_comm: "(a::N) + b = b + (a::N)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
21 |
and Nplus_assoc: "((a::N) + b) + c = a + (b + c)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
22 |
|
49514 | 23 |
section{* Parallel composition *} |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
24 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
25 |
fun par_r where "par_r (tr1,tr2) = root tr1 + root tr2" |
49514 | 26 |
fun par_c where |
27 |
"par_c (tr1,tr2) = |
|
28 |
Inl ` (Inl -` (cont tr1 \<union> cont tr2)) \<union> |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
29 |
Inr ` (Inr -` cont tr1 \<times> Inr -` cont tr2)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
30 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
31 |
declare par_r.simps[simp del] declare par_c.simps[simp del] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
32 |
|
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
33 |
(* Corecursive definition of parallel composition: *) |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
34 |
definition par :: "dtree \<times> dtree \<Rightarrow> dtree" where |
49508 | 35 |
"par \<equiv> unfold par_r par_c" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
36 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
37 |
abbreviation par_abbr (infixr "\<parallel>" 80) where "tr1 \<parallel> tr2 \<equiv> par (tr1, tr2)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
38 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
39 |
lemma finite_par_c: "finite (par_c (tr1, tr2))" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
40 |
unfolding par_c.simps apply(rule finite_UnI) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
41 |
apply (metis finite_Un finite_cont finite_imageI finite_vimageI inj_Inl) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
42 |
apply(intro finite_imageI finite_cartesian_product finite_vimageI) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
43 |
using finite_cont by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
44 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
45 |
lemma root_par: "root (tr1 \<parallel> tr2) = root tr1 + root tr2" |
49508 | 46 |
using unfold(1)[of par_r par_c "(tr1,tr2)"] unfolding par_def par_r.simps by simp |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
47 |
|
49514 | 48 |
lemma cont_par: |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
49 |
"cont (tr1 \<parallel> tr2) = (id \<oplus> par) ` par_c (tr1,tr2)" |
49508 | 50 |
using unfold(2)[of par_c "(tr1,tr2)" par_r, OF finite_par_c] |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
51 |
unfolding par_def .. |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
52 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
53 |
lemma Inl_cont_par[simp]: |
49514 | 54 |
"Inl -` (cont (tr1 \<parallel> tr2)) = Inl -` (cont tr1 \<union> cont tr2)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
55 |
unfolding cont_par par_c.simps by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
56 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
57 |
lemma Inr_cont_par[simp]: |
49514 | 58 |
"Inr -` (cont (tr1 \<parallel> tr2)) = par ` (Inr -` cont tr1 \<times> Inr -` cont tr2)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
59 |
unfolding cont_par par_c.simps by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
60 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
61 |
lemma Inl_in_cont_par: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
62 |
"Inl t \<in> cont (tr1 \<parallel> tr2) \<longleftrightarrow> (Inl t \<in> cont tr1 \<or> Inl t \<in> cont tr2)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
63 |
using Inl_cont_par[of tr1 tr2] unfolding vimage_def by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
64 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
65 |
lemma Inr_in_cont_par: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
66 |
"Inr t \<in> cont (tr1 \<parallel> tr2) \<longleftrightarrow> (t \<in> par ` (Inr -` cont tr1 \<times> Inr -` cont tr2))" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
67 |
using Inr_cont_par[of tr1 tr2] unfolding vimage_def by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
68 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
69 |
|
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
70 |
section{* Structural coinductive proofs *} |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
71 |
|
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
72 |
lemma set_rel_sum_rel_eq[simp]: |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
73 |
"set_rel (sum_rel (op =) \<phi>) A1 A2 \<longleftrightarrow> |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
74 |
Inl -` A1 = Inl -` A2 \<and> set_rel \<phi> (Inr -` A1) (Inr -` A2)" |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
75 |
unfolding set_rel_sum_rel set_rel_eq .. |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
76 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
77 |
(* Detailed proofs of commutativity and associativity: *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
78 |
theorem par_com: "tr1 \<parallel> tr2 = tr2 \<parallel> tr1" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
79 |
proof- |
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
80 |
let ?\<theta> = "\<lambda> trA trB. \<exists> tr1 tr2. trA = tr1 \<parallel> tr2 \<and> trB = tr2 \<parallel> tr1" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
81 |
{fix trA trB |
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
82 |
assume "?\<theta> trA trB" hence "trA = trB" |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
83 |
apply (induct rule: dtree_coinduct) |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
84 |
unfolding set_rel_sum_rel set_rel_eq unfolding set_rel_def proof safe |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
85 |
fix tr1 tr2 show "root (tr1 \<parallel> tr2) = root (tr2 \<parallel> tr1)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
86 |
unfolding root_par by (rule Nplus_comm) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
87 |
next |
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
88 |
fix n tr1 tr2 assume "Inl n \<in> cont (tr1 \<parallel> tr2)" thus "n \<in> Inl -` (cont (tr2 \<parallel> tr1))" |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
89 |
unfolding Inl_in_cont_par by auto |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
90 |
next |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
91 |
fix n tr1 tr2 assume "Inl n \<in> cont (tr2 \<parallel> tr1)" thus "n \<in> Inl -` (cont (tr1 \<parallel> tr2))" |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
92 |
unfolding Inl_in_cont_par by auto |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
93 |
next |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
94 |
fix tr1 tr2 trA' assume "Inr trA' \<in> cont (tr1 \<parallel> tr2)" |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
95 |
then obtain tr1' tr2' where "trA' = tr1' \<parallel> tr2'" |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
96 |
and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2" |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
97 |
unfolding Inr_in_cont_par by auto |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
98 |
thus "\<exists> trB' \<in> Inr -` (cont (tr2 \<parallel> tr1)). ?\<theta> trA' trB'" |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
99 |
apply(intro bexI[of _ "tr2' \<parallel> tr1'"]) unfolding Inr_in_cont_par by auto |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
100 |
next |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
101 |
fix tr1 tr2 trB' assume "Inr trB' \<in> cont (tr2 \<parallel> tr1)" |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
102 |
then obtain tr1' tr2' where "trB' = tr2' \<parallel> tr1'" |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
103 |
and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2" |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
104 |
unfolding Inr_in_cont_par by auto |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
105 |
thus "\<exists> trA' \<in> Inr -` (cont (tr1 \<parallel> tr2)). ?\<theta> trA' trB'" |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
106 |
apply(intro bexI[of _ "tr1' \<parallel> tr2'"]) unfolding Inr_in_cont_par by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
107 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
108 |
} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
109 |
thus ?thesis by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
110 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
111 |
|
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
112 |
lemma par_assoc: "(tr1 \<parallel> tr2) \<parallel> tr3 = tr1 \<parallel> (tr2 \<parallel> tr3)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
113 |
proof- |
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
114 |
let ?\<theta> = |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
115 |
"\<lambda> trA trB. \<exists> tr1 tr2 tr3. trA = (tr1 \<parallel> tr2) \<parallel> tr3 \<and> trB = tr1 \<parallel> (tr2 \<parallel> tr3)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
116 |
{fix trA trB |
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
117 |
assume "?\<theta> trA trB" hence "trA = trB" |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
118 |
apply (induct rule: dtree_coinduct) |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
119 |
unfolding set_rel_sum_rel set_rel_eq unfolding set_rel_def proof safe |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
120 |
fix tr1 tr2 tr3 show "root ((tr1 \<parallel> tr2) \<parallel> tr3) = root (tr1 \<parallel> (tr2 \<parallel> tr3))" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
121 |
unfolding root_par by (rule Nplus_assoc) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
122 |
next |
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
123 |
fix n tr1 tr2 tr3 assume "Inl n \<in> (cont ((tr1 \<parallel> tr2) \<parallel> tr3))" |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
124 |
thus "n \<in> Inl -` (cont (tr1 \<parallel> tr2 \<parallel> tr3))" unfolding Inl_in_cont_par by simp |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
125 |
next |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
126 |
fix n tr1 tr2 tr3 assume "Inl n \<in> (cont (tr1 \<parallel> tr2 \<parallel> tr3))" |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
127 |
thus "n \<in> Inl -` (cont ((tr1 \<parallel> tr2) \<parallel> tr3))" unfolding Inl_in_cont_par by simp |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
128 |
next |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
129 |
fix trA' tr1 tr2 tr3 assume "Inr trA' \<in> cont ((tr1 \<parallel> tr2) \<parallel> tr3)" |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
130 |
then obtain tr1' tr2' tr3' where "trA' = (tr1' \<parallel> tr2') \<parallel> tr3'" |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
131 |
and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2" |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
132 |
and "Inr tr3' \<in> cont tr3" unfolding Inr_in_cont_par by auto |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
133 |
thus "\<exists> trB' \<in> Inr -` (cont (tr1 \<parallel> tr2 \<parallel> tr3)). ?\<theta> trA' trB'" |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
134 |
apply(intro bexI[of _ "tr1' \<parallel> tr2' \<parallel> tr3'"]) |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
135 |
unfolding Inr_in_cont_par by auto |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
136 |
next |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
137 |
fix trB' tr1 tr2 tr3 assume "Inr trB' \<in> cont (tr1 \<parallel> tr2 \<parallel> tr3)" |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
138 |
then obtain tr1' tr2' tr3' where "trB' = tr1' \<parallel> (tr2' \<parallel> tr3')" |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
139 |
and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2" |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
140 |
and "Inr tr3' \<in> cont tr3" unfolding Inr_in_cont_par by auto |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
141 |
thus "\<exists> trA' \<in> Inr -` cont ((tr1 \<parallel> tr2) \<parallel> tr3). ?\<theta> trA' trB'" |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
142 |
apply(intro bexI[of _ "(tr1' \<parallel> tr2') \<parallel> tr3'"]) |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
143 |
unfolding Inr_in_cont_par by auto |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
144 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
145 |
} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
146 |
thus ?thesis by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
147 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
148 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
149 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
150 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
151 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
152 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
153 |
end |