author | wenzelm |
Sun, 02 Nov 2014 18:21:45 +0100 | |
changeset 58889 | 5b7a9633cfa8 |
parent 58309 | a09ec6daaa19 |
child 63167 | 0909deb8059b |
permissions | -rw-r--r-- |
58309
a09ec6daaa19
renamed 'BNF_Examples' to 'Datatype_Examples' (cf. 'datatypes.pdf')
blanchet
parents:
55943
diff
changeset
|
1 |
(* Title: HOL/Datatype_Examples/Derivation_Trees/Parallel.thy |
49463 | 2 |
Author: Andrei Popescu, TU Muenchen |
3 |
Copyright 2012 |
|
4 |
||
5 |
Parallel composition. |
|
6 |
*) |
|
7 |
||
58889 | 8 |
section {* Parallel Composition *} |
49463 | 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) |
49879 | 15 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
16 |
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
|
17 |
|
49514 | 18 |
axiomatization where |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
19 |
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
|
20 |
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
|
21 |
|
49882 | 22 |
subsection{* Corecursive Definition of Parallel Composition *} |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
23 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
24 |
fun par_r where "par_r (tr1,tr2) = root tr1 + root tr2" |
49514 | 25 |
fun par_c where |
26 |
"par_c (tr1,tr2) = |
|
27 |
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
|
28 |
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
|
29 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
30 |
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
|
31 |
|
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
32 |
definition par :: "dtree \<times> dtree \<Rightarrow> dtree" where |
49508 | 33 |
"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
|
34 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
35 |
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
|
36 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
37 |
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
|
38 |
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
|
39 |
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
|
40 |
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
|
41 |
using finite_cont by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
42 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
43 |
lemma root_par: "root (tr1 \<parallel> tr2) = root tr1 + root tr2" |
49508 | 44 |
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
|
45 |
|
49514 | 46 |
lemma cont_par: |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
47 |
"cont (tr1 \<parallel> tr2) = (id \<oplus> par) ` par_c (tr1,tr2)" |
49508 | 48 |
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
|
49 |
unfolding par_def .. |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
50 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
51 |
lemma Inl_cont_par[simp]: |
49514 | 52 |
"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
|
53 |
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
|
54 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
55 |
lemma Inr_cont_par[simp]: |
49514 | 56 |
"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
|
57 |
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
|
58 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
59 |
lemma Inl_in_cont_par: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
60 |
"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
|
61 |
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
|
62 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
63 |
lemma Inr_in_cont_par: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
64 |
"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
|
65 |
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
|
66 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
67 |
|
49882 | 68 |
subsection{* Structural Coinduction Proofs *} |
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
69 |
|
55943 | 70 |
lemma rel_set_rel_sum_eq[simp]: |
71 |
"rel_set (rel_sum (op =) \<phi>) A1 A2 \<longleftrightarrow> |
|
55938 | 72 |
Inl -` A1 = Inl -` A2 \<and> rel_set \<phi> (Inr -` A1) (Inr -` A2)" |
55943 | 73 |
unfolding rel_set_rel_sum rel_set_eq .. |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
74 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
75 |
(* 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
|
76 |
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
|
77 |
proof- |
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
78 |
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
|
79 |
{fix trA trB |
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
80 |
assume "?\<theta> trA trB" hence "trA = trB" |
49879 | 81 |
apply (induct rule: dtree_coinduct) |
55943 | 82 |
unfolding rel_set_rel_sum rel_set_eq unfolding rel_set_def proof safe |
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
83 |
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
|
84 |
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
|
85 |
next |
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
86 |
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
|
87 |
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
|
88 |
next |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
89 |
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
|
90 |
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
|
91 |
next |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
92 |
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
|
93 |
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
|
94 |
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
|
95 |
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
|
96 |
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
|
97 |
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
|
98 |
next |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
99 |
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
|
100 |
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
|
101 |
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
|
102 |
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
|
103 |
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
|
104 |
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
|
105 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
106 |
} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
107 |
thus ?thesis by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
108 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
109 |
|
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
110 |
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
|
111 |
proof- |
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
112 |
let ?\<theta> = |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
113 |
"\<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
|
114 |
{fix trA trB |
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
115 |
assume "?\<theta> trA trB" hence "trA = trB" |
49879 | 116 |
apply (induct rule: dtree_coinduct) |
55943 | 117 |
unfolding rel_set_rel_sum rel_set_eq unfolding rel_set_def proof safe |
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
118 |
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
|
119 |
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
|
120 |
next |
49879 | 121 |
fix n tr1 tr2 tr3 assume "Inl n \<in> (cont ((tr1 \<parallel> tr2) \<parallel> tr3))" |
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
122 |
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
|
123 |
next |
49879 | 124 |
fix n tr1 tr2 tr3 assume "Inl n \<in> (cont (tr1 \<parallel> tr2 \<parallel> tr3))" |
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
125 |
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
|
126 |
next |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
127 |
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
|
128 |
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
|
129 |
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
|
130 |
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
|
131 |
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
|
132 |
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
|
133 |
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
|
134 |
next |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
135 |
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
|
136 |
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
|
137 |
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
|
138 |
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
|
139 |
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
|
140 |
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
|
141 |
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
|
142 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
143 |
} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
144 |
thus ?thesis by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
145 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
146 |
|
54538
ba7392b52a7c
factor 'List_Prefix' out of 'Sublist' and move to 'Main' (needed for codatatypes)
blanchet
parents:
49882
diff
changeset
|
147 |
end |