author | nipkow |
Wed, 28 Jan 2009 16:29:16 +0100 | |
changeset 29667 | 53103fc8ffa3 |
parent 26966 | 071f40487734 |
child 41589 | bbd861837ebc |
permissions | -rw-r--r-- |
18269 | 1 |
(* $Id$ *) |
18106 | 2 |
|
18882
454d09651d1a
- renamed some lemmas (some had names coming from ancient
urbanc
parents:
18773
diff
changeset
|
3 |
theory CR |
21138 | 4 |
imports Lam_Funs |
18106 | 5 |
begin |
6 |
||
18269 | 7 |
text {* The Church-Rosser proof from Barendregt's book *} |
8 |
||
18312
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
9 |
lemma forget: |
20955
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
10 |
assumes asm: "x\<sharp>L" |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
11 |
shows "L[x::=P] = L" |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
12 |
using asm |
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
25996
diff
changeset
|
13 |
proof (nominal_induct L avoiding: x P rule: lam.strong_induct) |
20955
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
14 |
case (Var z) |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
15 |
have "x\<sharp>Var z" by fact |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
16 |
thus "(Var z)[x::=P] = (Var z)" by (simp add: fresh_atm) |
18106 | 17 |
next |
20955
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
18 |
case (App M1 M2) |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
19 |
have "x\<sharp>App M1 M2" by fact |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
20 |
moreover |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
21 |
have ih1: "x\<sharp>M1 \<Longrightarrow> M1[x::=P] = M1" by fact |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
22 |
moreover |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
23 |
have ih1: "x\<sharp>M2 \<Longrightarrow> M2[x::=P] = M2" by fact |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
24 |
ultimately show "(App M1 M2)[x::=P] = (App M1 M2)" by simp |
18106 | 25 |
next |
20955
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
26 |
case (Lam z M) |
23393 | 27 |
have vc: "z\<sharp>x" "z\<sharp>P" by fact+ |
20955
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
28 |
have ih: "x\<sharp>M \<Longrightarrow> M[x::=P] = M" by fact |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
29 |
have asm: "x\<sharp>Lam [z].M" by fact |
21101 | 30 |
then have "x\<sharp>M" using vc by (simp add: fresh_atm abs_fresh) |
31 |
then have "M[x::=P] = M" using ih by simp |
|
32 |
then show "(Lam [z].M)[x::=P] = Lam [z].M" using vc by simp |
|
18106 | 33 |
qed |
34 |
||
18378 | 35 |
lemma forget_automatic: |
20955
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
36 |
assumes asm: "x\<sharp>L" |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
37 |
shows "L[x::=P] = L" |
21101 | 38 |
using asm |
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
25996
diff
changeset
|
39 |
by (nominal_induct L avoiding: x P rule: lam.strong_induct) |
21101 | 40 |
(auto simp add: abs_fresh fresh_atm) |
18106 | 41 |
|
18312
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
42 |
lemma fresh_fact: |
20955
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
43 |
fixes z::"name" |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
44 |
assumes asms: "z\<sharp>N" "z\<sharp>L" |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
45 |
shows "z\<sharp>(N[y::=L])" |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
46 |
using asms |
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
25996
diff
changeset
|
47 |
proof (nominal_induct N avoiding: z y L rule: lam.strong_induct) |
20955
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
48 |
case (Var u) |
23393 | 49 |
have "z\<sharp>(Var u)" "z\<sharp>L" by fact+ |
20955
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
50 |
thus "z\<sharp>((Var u)[y::=L])" by simp |
18312
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
51 |
next |
20955
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
52 |
case (App N1 N2) |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
53 |
have ih1: "\<lbrakk>z\<sharp>N1; z\<sharp>L\<rbrakk> \<Longrightarrow> z\<sharp>N1[y::=L]" by fact |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
54 |
moreover |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
55 |
have ih2: "\<lbrakk>z\<sharp>N2; z\<sharp>L\<rbrakk> \<Longrightarrow> z\<sharp>N2[y::=L]" by fact |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
56 |
moreover |
23393 | 57 |
have "z\<sharp>App N1 N2" "z\<sharp>L" by fact+ |
20955
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
58 |
ultimately show "z\<sharp>((App N1 N2)[y::=L])" by simp |
18312
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
59 |
next |
20955
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
60 |
case (Lam u N1) |
23393 | 61 |
have vc: "u\<sharp>z" "u\<sharp>y" "u\<sharp>L" by fact+ |
20955
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
62 |
have "z\<sharp>Lam [u].N1" by fact |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
63 |
hence "z\<sharp>N1" using vc by (simp add: abs_fresh fresh_atm) |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
64 |
moreover |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
65 |
have ih: "\<lbrakk>z\<sharp>N1; z\<sharp>L\<rbrakk> \<Longrightarrow> z\<sharp>(N1[y::=L])" by fact |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
66 |
moreover |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
67 |
have "z\<sharp>L" by fact |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
68 |
ultimately show "z\<sharp>(Lam [u].N1)[y::=L]" using vc by (simp add: abs_fresh) |
18312
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
69 |
qed |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
70 |
|
18378 | 71 |
lemma fresh_fact_automatic: |
20955
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
72 |
fixes z::"name" |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
73 |
assumes asms: "z\<sharp>N" "z\<sharp>L" |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
74 |
shows "z\<sharp>(N[y::=L])" |
21101 | 75 |
using asms |
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
25996
diff
changeset
|
76 |
by (nominal_induct N avoiding: z y L rule: lam.strong_induct) |
21101 | 77 |
(auto simp add: abs_fresh fresh_atm) |
18106 | 78 |
|
22540 | 79 |
lemma fresh_fact': |
80 |
fixes a::"name" |
|
81 |
assumes a: "a\<sharp>t2" |
|
82 |
shows "a\<sharp>t1[a::=t2]" |
|
83 |
using a |
|
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
25996
diff
changeset
|
84 |
by (nominal_induct t1 avoiding: a t2 rule: lam.strong_induct) |
22540 | 85 |
(auto simp add: abs_fresh fresh_atm) |
86 |
||
20955
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
87 |
lemma substitution_lemma: |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
88 |
assumes a: "x\<noteq>y" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
89 |
and b: "x\<sharp>L" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
90 |
shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
91 |
using a b |
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
25996
diff
changeset
|
92 |
proof (nominal_induct M avoiding: x y N L rule: lam.strong_induct) |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
93 |
case (Var z) (* case 1: Variables*) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
94 |
have "x\<noteq>y" by fact |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
95 |
have "x\<sharp>L" by fact |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
96 |
show "Var z[x::=N][y::=L] = Var z[y::=L][x::=N[y::=L]]" (is "?LHS = ?RHS") |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
97 |
proof - |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
98 |
{ (*Case 1.1*) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
99 |
assume "z=x" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
100 |
have "(1)": "?LHS = N[y::=L]" using `z=x` by simp |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
101 |
have "(2)": "?RHS = N[y::=L]" using `z=x` `x\<noteq>y` by simp |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
102 |
from "(1)" "(2)" have "?LHS = ?RHS" by simp |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
103 |
} |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
104 |
moreover |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
105 |
{ (*Case 1.2*) |
20955
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
106 |
assume "z=y" and "z\<noteq>x" |
25996 | 107 |
have "(1)": "?LHS = L" using `z\<noteq>x` `z=y` by simp |
108 |
have "(2)": "?RHS = L[x::=N[y::=L]]" using `z=y` by simp |
|
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
109 |
have "(3)": "L[x::=N[y::=L]] = L" using `x\<sharp>L` by (simp add: forget) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
110 |
from "(1)" "(2)" "(3)" have "?LHS = ?RHS" by simp |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
111 |
} |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
112 |
moreover |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
113 |
{ (*Case 1.3*) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
114 |
assume "z\<noteq>x" and "z\<noteq>y" |
25996 | 115 |
have "(1)": "?LHS = Var z" using `z\<noteq>x` `z\<noteq>y` by simp |
116 |
have "(2)": "?RHS = Var z" using `z\<noteq>x` `z\<noteq>y` by simp |
|
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
117 |
from "(1)" "(2)" have "?LHS = ?RHS" by simp |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
118 |
} |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
119 |
ultimately show "?LHS = ?RHS" by blast |
18106 | 120 |
qed |
121 |
next |
|
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
122 |
case (Lam z M1) (* case 2: lambdas *) |
20955
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
123 |
have ih: "\<lbrakk>x\<noteq>y; x\<sharp>L\<rbrakk> \<Longrightarrow> M1[x::=N][y::=L] = M1[y::=L][x::=N[y::=L]]" by fact |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
124 |
have "x\<noteq>y" by fact |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
125 |
have "x\<sharp>L" by fact |
23393 | 126 |
have fs: "z\<sharp>x" "z\<sharp>y" "z\<sharp>N" "z\<sharp>L" by fact+ |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
127 |
hence "z\<sharp>N[y::=L]" by (simp add: fresh_fact) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
128 |
show "(Lam [z].M1)[x::=N][y::=L] = (Lam [z].M1)[y::=L][x::=N[y::=L]]" (is "?LHS=?RHS") |
20955
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
129 |
proof - |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
130 |
have "?LHS = Lam [z].(M1[x::=N][y::=L])" using `z\<sharp>x` `z\<sharp>y` `z\<sharp>N` `z\<sharp>L` by simp |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
131 |
also from ih have "\<dots> = Lam [z].(M1[y::=L][x::=N[y::=L]])" using `x\<noteq>y` `x\<sharp>L` by simp |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
132 |
also have "\<dots> = (Lam [z].(M1[y::=L]))[x::=N[y::=L]]" using `z\<sharp>x` `z\<sharp>N[y::=L]` by simp |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
133 |
also have "\<dots> = ?RHS" using `z\<sharp>y` `z\<sharp>L` by simp |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
134 |
finally show "?LHS = ?RHS" . |
18106 | 135 |
qed |
136 |
next |
|
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
137 |
case (App M1 M2) (* case 3: applications *) |
21101 | 138 |
thus "(App M1 M2)[x::=N][y::=L] = (App M1 M2)[y::=L][x::=N[y::=L]]" by simp |
18106 | 139 |
qed |
140 |
||
20955
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
141 |
lemma substitution_lemma_automatic: |
19172
ad36a9b42cf3
made some small changes to generate nicer latex-output
urbanc
parents:
18882
diff
changeset
|
142 |
assumes asm: "x\<noteq>y" "x\<sharp>L" |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
143 |
shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]" |
21101 | 144 |
using asm |
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
25996
diff
changeset
|
145 |
by (nominal_induct M avoiding: x y N L rule: lam.strong_induct) |
21101 | 146 |
(auto simp add: fresh_fact forget) |
18106 | 147 |
|
148 |
section {* Beta Reduction *} |
|
149 |
||
23760 | 150 |
inductive |
21101 | 151 |
"Beta" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80) |
21366 | 152 |
where |
153 |
b1[intro]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App s1 t)\<longrightarrow>\<^isub>\<beta>(App s2 t)" |
|
154 |
| b2[intro]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App t s1)\<longrightarrow>\<^isub>\<beta>(App t s2)" |
|
155 |
| b3[intro]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>\<beta> (Lam [a].s2)" |
|
22540 | 156 |
| b4[intro]: "a\<sharp>s2 \<Longrightarrow> (App (Lam [a].s1) s2)\<longrightarrow>\<^isub>\<beta>(s1[a::=s2])" |
157 |
||
22730
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22542
diff
changeset
|
158 |
equivariance Beta |
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22542
diff
changeset
|
159 |
|
22540 | 160 |
nominal_inductive Beta |
161 |
by (simp_all add: abs_fresh fresh_fact') |
|
18106 | 162 |
|
23760 | 163 |
inductive |
21101 | 164 |
"Beta_star" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80) |
21366 | 165 |
where |
166 |
bs1[intro, simp]: "M \<longrightarrow>\<^isub>\<beta>\<^sup>* M" |
|
167 |
| bs2[intro]: "\<lbrakk>M1\<longrightarrow>\<^isub>\<beta>\<^sup>* M2; M2 \<longrightarrow>\<^isub>\<beta> M3\<rbrakk> \<Longrightarrow> M1 \<longrightarrow>\<^isub>\<beta>\<^sup>* M3" |
|
21101 | 168 |
|
22540 | 169 |
equivariance Beta_star |
170 |
||
21101 | 171 |
lemma beta_star_trans: |
172 |
assumes a1: "M1\<longrightarrow>\<^isub>\<beta>\<^sup>* M2" |
|
173 |
and a2: "M2\<longrightarrow>\<^isub>\<beta>\<^sup>* M3" |
|
174 |
shows "M1 \<longrightarrow>\<^isub>\<beta>\<^sup>* M3" |
|
175 |
using a2 a1 |
|
176 |
by (induct) (auto) |
|
177 |
||
18106 | 178 |
section {* One-Reduction *} |
179 |
||
23760 | 180 |
inductive |
21101 | 181 |
One :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>1 _" [80,80] 80) |
21366 | 182 |
where |
183 |
o1[intro!]: "M\<longrightarrow>\<^isub>1M" |
|
184 |
| o2[simp,intro!]: "\<lbrakk>t1\<longrightarrow>\<^isub>1t2;s1\<longrightarrow>\<^isub>1s2\<rbrakk> \<Longrightarrow> (App t1 s1)\<longrightarrow>\<^isub>1(App t2 s2)" |
|
185 |
| o3[simp,intro!]: "s1\<longrightarrow>\<^isub>1s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>1(Lam [a].s2)" |
|
22540 | 186 |
| o4[simp,intro!]: "\<lbrakk>a\<sharp>(s1,s2); s1\<longrightarrow>\<^isub>1s2;t1\<longrightarrow>\<^isub>1t2\<rbrakk> \<Longrightarrow> (App (Lam [a].t1) s1)\<longrightarrow>\<^isub>1(t2[a::=s2])" |
187 |
||
22730
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22542
diff
changeset
|
188 |
equivariance One |
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22542
diff
changeset
|
189 |
|
22540 | 190 |
nominal_inductive One |
191 |
by (simp_all add: abs_fresh fresh_fact') |
|
18106 | 192 |
|
23760 | 193 |
inductive |
21101 | 194 |
"One_star" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>1\<^sup>* _" [80,80] 80) |
21366 | 195 |
where |
196 |
os1[intro, simp]: "M \<longrightarrow>\<^isub>1\<^sup>* M" |
|
197 |
| os2[intro]: "\<lbrakk>M1\<longrightarrow>\<^isub>1\<^sup>* M2; M2 \<longrightarrow>\<^isub>1 M3\<rbrakk> \<Longrightarrow> M1 \<longrightarrow>\<^isub>1\<^sup>* M3" |
|
21101 | 198 |
|
22540 | 199 |
equivariance One_star |
18106 | 200 |
|
21101 | 201 |
lemma one_star_trans: |
202 |
assumes a1: "M1\<longrightarrow>\<^isub>1\<^sup>* M2" |
|
203 |
and a2: "M2\<longrightarrow>\<^isub>1\<^sup>* M3" |
|
204 |
shows "M1\<longrightarrow>\<^isub>1\<^sup>* M3" |
|
205 |
using a2 a1 |
|
206 |
by (induct) (auto) |
|
207 |
||
18312
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
208 |
lemma one_fresh_preserv: |
18378 | 209 |
fixes a :: "name" |
18106 | 210 |
assumes a: "t\<longrightarrow>\<^isub>1s" |
18312
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
211 |
and b: "a\<sharp>t" |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
212 |
shows "a\<sharp>s" |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
213 |
using a b |
18106 | 214 |
proof (induct) |
18312
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
215 |
case o1 thus ?case by simp |
18106 | 216 |
next |
18312
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
217 |
case o2 thus ?case by simp |
18106 | 218 |
next |
21101 | 219 |
case (o3 s1 s2 c) |
18312
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
220 |
have ih: "a\<sharp>s1 \<Longrightarrow> a\<sharp>s2" by fact |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
221 |
have c: "a\<sharp>Lam [c].s1" by fact |
18106 | 222 |
show ?case |
18312
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
223 |
proof (cases "a=c") |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
224 |
assume "a=c" thus "a\<sharp>Lam [c].s2" by (simp add: abs_fresh) |
18106 | 225 |
next |
18312
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
226 |
assume d: "a\<noteq>c" |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
227 |
with c have "a\<sharp>s1" by (simp add: abs_fresh) |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
228 |
hence "a\<sharp>s2" using ih by simp |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
229 |
thus "a\<sharp>Lam [c].s2" using d by (simp add: abs_fresh) |
18106 | 230 |
qed |
231 |
next |
|
22540 | 232 |
case (o4 c t1 t2 s1 s2) |
18312
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
233 |
have i1: "a\<sharp>t1 \<Longrightarrow> a\<sharp>t2" by fact |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
234 |
have i2: "a\<sharp>s1 \<Longrightarrow> a\<sharp>s2" by fact |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
235 |
have as: "a\<sharp>App (Lam [c].s1) t1" by fact |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
236 |
hence c1: "a\<sharp>Lam [c].s1" and c2: "a\<sharp>t1" by (simp add: fresh_prod)+ |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
237 |
from c2 i1 have c3: "a\<sharp>t2" by simp |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
238 |
show "a\<sharp>s2[c::=t2]" |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
239 |
proof (cases "a=c") |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
240 |
assume "a=c" |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
241 |
thus "a\<sharp>s2[c::=t2]" using c3 by (simp add: fresh_fact') |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
242 |
next |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
243 |
assume d1: "a\<noteq>c" |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
244 |
from c1 d1 have "a\<sharp>s1" by (simp add: abs_fresh) |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
245 |
hence "a\<sharp>s2" using i2 by simp |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
246 |
thus "a\<sharp>s2[c::=t2]" using c3 by (simp add: fresh_fact) |
18106 | 247 |
qed |
248 |
qed |
|
249 |
||
22823
fa9ff469247f
tuned some proofs in CR and properly included CR_Takahashi
urbanc
parents:
22730
diff
changeset
|
250 |
lemma one_fresh_preserv_automatic: |
fa9ff469247f
tuned some proofs in CR and properly included CR_Takahashi
urbanc
parents:
22730
diff
changeset
|
251 |
fixes a :: "name" |
fa9ff469247f
tuned some proofs in CR and properly included CR_Takahashi
urbanc
parents:
22730
diff
changeset
|
252 |
assumes a: "t\<longrightarrow>\<^isub>1s" |
fa9ff469247f
tuned some proofs in CR and properly included CR_Takahashi
urbanc
parents:
22730
diff
changeset
|
253 |
and b: "a\<sharp>t" |
fa9ff469247f
tuned some proofs in CR and properly included CR_Takahashi
urbanc
parents:
22730
diff
changeset
|
254 |
shows "a\<sharp>s" |
fa9ff469247f
tuned some proofs in CR and properly included CR_Takahashi
urbanc
parents:
22730
diff
changeset
|
255 |
using a b |
fa9ff469247f
tuned some proofs in CR and properly included CR_Takahashi
urbanc
parents:
22730
diff
changeset
|
256 |
apply(nominal_induct avoiding: a rule: One.strong_induct) |
fa9ff469247f
tuned some proofs in CR and properly included CR_Takahashi
urbanc
parents:
22730
diff
changeset
|
257 |
apply(auto simp add: abs_fresh fresh_atm fresh_fact) |
fa9ff469247f
tuned some proofs in CR and properly included CR_Takahashi
urbanc
parents:
22730
diff
changeset
|
258 |
done |
fa9ff469247f
tuned some proofs in CR and properly included CR_Takahashi
urbanc
parents:
22730
diff
changeset
|
259 |
|
22540 | 260 |
lemma subst_rename: |
261 |
assumes a: "c\<sharp>t1" |
|
262 |
shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]" |
|
263 |
using a |
|
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
25996
diff
changeset
|
264 |
by (nominal_induct t1 avoiding: a c t2 rule: lam.strong_induct) |
22540 | 265 |
(auto simp add: calc_atm fresh_atm abs_fresh) |
266 |
||
18106 | 267 |
lemma one_abs: |
25831 | 268 |
assumes a: "Lam [a].t\<longrightarrow>\<^isub>1t'" |
21101 | 269 |
shows "\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>1t''" |
25831 | 270 |
proof - |
271 |
have "a\<sharp>Lam [a].t" by (simp add: abs_fresh) |
|
272 |
with a have "a\<sharp>t'" by (simp add: one_fresh_preserv) |
|
273 |
with a show ?thesis |
|
274 |
by (cases rule: One.strong_cases[where a="a" and aa="a"]) |
|
275 |
(auto simp add: lam.inject abs_fresh alpha) |
|
276 |
qed |
|
18106 | 277 |
|
278 |
lemma one_app: |
|
21101 | 279 |
assumes a: "App t1 t2 \<longrightarrow>\<^isub>1 t'" |
280 |
shows "(\<exists>s1 s2. t' = App s1 s2 \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2) \<or> |
|
25831 | 281 |
(\<exists>a s s1 s2. t1 = Lam [a].s \<and> t' = s1[a::=s2] \<and> s \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2 \<and> a\<sharp>(t2,s2))" |
282 |
using a by (erule_tac One.cases) (auto simp add: lam.inject) |
|
18106 | 283 |
|
284 |
lemma one_red: |
|
25831 | 285 |
assumes a: "App (Lam [a].t1) t2 \<longrightarrow>\<^isub>1 M" "a\<sharp>(t2,M)" |
21101 | 286 |
shows "(\<exists>s1 s2. M = App (Lam [a].s1) s2 \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2) \<or> |
287 |
(\<exists>s1 s2. M = s1[a::=s2] \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2)" |
|
25831 | 288 |
using a |
289 |
by (cases rule: One.strong_cases [where a="a" and aa="a"]) |
|
290 |
(auto dest: one_abs simp add: lam.inject abs_fresh alpha fresh_prod) |
|
18106 | 291 |
|
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
292 |
text {* first case in Lemma 3.2.4*} |
18106 | 293 |
|
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
294 |
lemma one_subst_aux: |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
295 |
assumes a: "N\<longrightarrow>\<^isub>1N'" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
296 |
shows "M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
297 |
using a |
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
25996
diff
changeset
|
298 |
proof (nominal_induct M avoiding: x N N' rule: lam.strong_induct) |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
299 |
case (Var y) |
23393 | 300 |
thus "Var y[x::=N] \<longrightarrow>\<^isub>1 Var y[x::=N']" by (cases "x=y") auto |
18106 | 301 |
next |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
302 |
case (App P Q) (* application case - third line *) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
303 |
thus "(App P Q)[x::=N] \<longrightarrow>\<^isub>1 (App P Q)[x::=N']" using o2 by simp |
18106 | 304 |
next |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
305 |
case (Lam y P) (* abstraction case - fourth line *) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
306 |
thus "(Lam [y].P)[x::=N] \<longrightarrow>\<^isub>1 (Lam [y].P)[x::=N']" using o3 by simp |
18106 | 307 |
qed |
308 |
||
18378 | 309 |
lemma one_subst_aux_automatic: |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
310 |
assumes a: "N\<longrightarrow>\<^isub>1N'" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
311 |
shows "M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
312 |
using a |
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
25996
diff
changeset
|
313 |
by (nominal_induct M avoiding: x N N' rule: lam.strong_induct) |
25831 | 314 |
(auto simp add: fresh_prod fresh_atm) |
18106 | 315 |
|
18312
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
316 |
lemma one_subst: |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
317 |
assumes a: "M\<longrightarrow>\<^isub>1M'" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
318 |
and b: "N\<longrightarrow>\<^isub>1N'" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
319 |
shows "M[x::=N]\<longrightarrow>\<^isub>1M'[x::=N']" |
18773
0eabf66582d0
the additional freshness-condition in the one-induction
urbanc
parents:
18659
diff
changeset
|
320 |
using a b |
22540 | 321 |
proof (nominal_induct M M' avoiding: N N' x rule: One.strong_induct) |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
322 |
case (o1 M) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
323 |
thus ?case by (simp add: one_subst_aux) |
18106 | 324 |
next |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
325 |
case (o2 M1 M2 N1 N2) |
18106 | 326 |
thus ?case by simp |
327 |
next |
|
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
328 |
case (o3 a M1 M2) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
329 |
thus ?case by simp |
18106 | 330 |
next |
22540 | 331 |
case (o4 a N1 N2 M1 M2 N N' x) |
23393 | 332 |
have vc: "a\<sharp>N" "a\<sharp>N'" "a\<sharp>x" "a\<sharp>N1" "a\<sharp>N2" by fact+ |
22540 | 333 |
have asm: "N\<longrightarrow>\<^isub>1N'" by fact |
18106 | 334 |
show ?case |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
335 |
proof - |
22540 | 336 |
have "(App (Lam [a].M1) N1)[x::=N] = App (Lam [a].(M1[x::=N])) (N1[x::=N])" using vc by simp |
21143
56695d1f45cf
changed a misplaced "also" to a "moreover" (caused a loop somehow)
urbanc
parents:
21138
diff
changeset
|
337 |
moreover have "App (Lam [a].(M1[x::=N])) (N1[x::=N]) \<longrightarrow>\<^isub>1 M2[x::=N'][a::=N2[x::=N']]" |
22540 | 338 |
using o4 asm by (simp add: fresh_fact) |
21143
56695d1f45cf
changed a misplaced "also" to a "moreover" (caused a loop somehow)
urbanc
parents:
21138
diff
changeset
|
339 |
moreover have "M2[x::=N'][a::=N2[x::=N']] = M2[a::=N2][x::=N']" |
22540 | 340 |
using vc by (simp add: substitution_lemma fresh_atm) |
18106 | 341 |
ultimately show "(App (Lam [a].M1) N1)[x::=N] \<longrightarrow>\<^isub>1 M2[a::=N2][x::=N']" by simp |
342 |
qed |
|
343 |
qed |
|
344 |
||
18378 | 345 |
lemma one_subst_automatic: |
18106 | 346 |
assumes a: "M\<longrightarrow>\<^isub>1M'" |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
347 |
and b: "N\<longrightarrow>\<^isub>1N'" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
348 |
shows "M[x::=N]\<longrightarrow>\<^isub>1M'[x::=N']" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
349 |
using a b |
25831 | 350 |
by (nominal_induct M M' avoiding: N N' x rule: One.strong_induct) |
351 |
(auto simp add: one_subst_aux substitution_lemma fresh_atm fresh_fact) |
|
18106 | 352 |
|
353 |
lemma diamond[rule_format]: |
|
354 |
fixes M :: "lam" |
|
355 |
and M1:: "lam" |
|
356 |
assumes a: "M\<longrightarrow>\<^isub>1M1" |
|
18344 | 357 |
and b: "M\<longrightarrow>\<^isub>1M2" |
358 |
shows "\<exists>M3. M1\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" |
|
359 |
using a b |
|
22540 | 360 |
proof (nominal_induct avoiding: M1 M2 rule: One.strong_induct) |
18106 | 361 |
case (o1 M) (* case 1 --- M1 = M *) |
18344 | 362 |
thus "\<exists>M3. M\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" by blast |
18106 | 363 |
next |
22540 | 364 |
case (o4 x Q Q' P P') (* case 2 --- a beta-reduction occurs*) |
25831 | 365 |
have vc: "x\<sharp>Q" "x\<sharp>Q'" "x\<sharp>M2" by fact+ |
18344 | 366 |
have i1: "\<And>M2. Q \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact |
367 |
have i2: "\<And>M2. P \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact |
|
368 |
have "App (Lam [x].P) Q \<longrightarrow>\<^isub>1 M2" by fact |
|
369 |
hence "(\<exists>P' Q'. M2 = App (Lam [x].P') Q' \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q') \<or> |
|
25831 | 370 |
(\<exists>P' Q'. M2 = P'[x::=Q'] \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q')" using vc by (simp add: one_red) |
18344 | 371 |
moreover (* subcase 2.1 *) |
372 |
{ assume "\<exists>P' Q'. M2 = App (Lam [x].P') Q' \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q'" |
|
373 |
then obtain P'' and Q'' where |
|
374 |
b1: "M2=App (Lam [x].P'') Q''" and b2: "P\<longrightarrow>\<^isub>1P''" and b3: "Q\<longrightarrow>\<^isub>1Q''" by blast |
|
375 |
from b2 i2 have "(\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> P''\<longrightarrow>\<^isub>1M3)" by simp |
|
376 |
then obtain P''' where |
|
377 |
c1: "P'\<longrightarrow>\<^isub>1P'''" and c2: "P''\<longrightarrow>\<^isub>1P'''" by force |
|
378 |
from b3 i1 have "(\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> Q''\<longrightarrow>\<^isub>1M3)" by simp |
|
379 |
then obtain Q''' where |
|
380 |
d1: "Q'\<longrightarrow>\<^isub>1Q'''" and d2: "Q''\<longrightarrow>\<^isub>1Q'''" by force |
|
381 |
from c1 c2 d1 d2 |
|
382 |
have "P'[x::=Q']\<longrightarrow>\<^isub>1P'''[x::=Q'''] \<and> App (Lam [x].P'') Q'' \<longrightarrow>\<^isub>1 P'''[x::=Q''']" |
|
22540 | 383 |
using vc b3 by (auto simp add: one_subst one_fresh_preserv) |
18344 | 384 |
hence "\<exists>M3. P'[x::=Q']\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 by blast |
385 |
} |
|
386 |
moreover (* subcase 2.2 *) |
|
387 |
{ assume "\<exists>P' Q'. M2 = P'[x::=Q'] \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q'" |
|
388 |
then obtain P'' Q'' where |
|
389 |
b1: "M2=P''[x::=Q'']" and b2: "P\<longrightarrow>\<^isub>1P''" and b3: "Q\<longrightarrow>\<^isub>1Q''" by blast |
|
390 |
from b2 i2 have "(\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> P''\<longrightarrow>\<^isub>1M3)" by simp |
|
391 |
then obtain P''' where |
|
392 |
c1: "P'\<longrightarrow>\<^isub>1P'''" and c2: "P''\<longrightarrow>\<^isub>1P'''" by blast |
|
393 |
from b3 i1 have "(\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> Q''\<longrightarrow>\<^isub>1M3)" by simp |
|
394 |
then obtain Q''' where |
|
395 |
d1: "Q'\<longrightarrow>\<^isub>1Q'''" and d2: "Q''\<longrightarrow>\<^isub>1Q'''" by blast |
|
396 |
from c1 c2 d1 d2 |
|
397 |
have "P'[x::=Q']\<longrightarrow>\<^isub>1P'''[x::=Q'''] \<and> P''[x::=Q'']\<longrightarrow>\<^isub>1P'''[x::=Q''']" |
|
398 |
by (force simp add: one_subst) |
|
399 |
hence "\<exists>M3. P'[x::=Q']\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 by blast |
|
400 |
} |
|
401 |
ultimately show "\<exists>M3. P'[x::=Q']\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" by blast |
|
18106 | 402 |
next |
21101 | 403 |
case (o2 P P' Q Q') (* case 3 *) |
18344 | 404 |
have i0: "P\<longrightarrow>\<^isub>1P'" by fact |
22540 | 405 |
have i0': "Q\<longrightarrow>\<^isub>1Q'" by fact |
18344 | 406 |
have i1: "\<And>M2. Q \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact |
407 |
have i2: "\<And>M2. P \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact |
|
408 |
assume "App P Q \<longrightarrow>\<^isub>1 M2" |
|
409 |
hence "(\<exists>P'' Q''. M2 = App P'' Q'' \<and> P\<longrightarrow>\<^isub>1P'' \<and> Q\<longrightarrow>\<^isub>1Q'') \<or> |
|
25831 | 410 |
(\<exists>x P' P'' Q'. P = Lam [x].P' \<and> M2 = P''[x::=Q'] \<and> P'\<longrightarrow>\<^isub>1 P'' \<and> Q\<longrightarrow>\<^isub>1Q' \<and> x\<sharp>(Q,Q'))" |
18344 | 411 |
by (simp add: one_app[simplified]) |
412 |
moreover (* subcase 3.1 *) |
|
413 |
{ assume "\<exists>P'' Q''. M2 = App P'' Q'' \<and> P\<longrightarrow>\<^isub>1P'' \<and> Q\<longrightarrow>\<^isub>1Q''" |
|
414 |
then obtain P'' and Q'' where |
|
415 |
b1: "M2=App P'' Q''" and b2: "P\<longrightarrow>\<^isub>1P''" and b3: "Q\<longrightarrow>\<^isub>1Q''" by blast |
|
416 |
from b2 i2 have "(\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> P''\<longrightarrow>\<^isub>1M3)" by simp |
|
417 |
then obtain P''' where |
|
418 |
c1: "P'\<longrightarrow>\<^isub>1P'''" and c2: "P''\<longrightarrow>\<^isub>1P'''" by blast |
|
419 |
from b3 i1 have "\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> Q''\<longrightarrow>\<^isub>1M3" by simp |
|
420 |
then obtain Q''' where |
|
421 |
d1: "Q'\<longrightarrow>\<^isub>1Q'''" and d2: "Q''\<longrightarrow>\<^isub>1Q'''" by blast |
|
422 |
from c1 c2 d1 d2 |
|
423 |
have "App P' Q'\<longrightarrow>\<^isub>1App P''' Q''' \<and> App P'' Q'' \<longrightarrow>\<^isub>1 App P''' Q'''" by blast |
|
424 |
hence "\<exists>M3. App P' Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 by blast |
|
425 |
} |
|
426 |
moreover (* subcase 3.2 *) |
|
25831 | 427 |
{ assume "\<exists>x P1 P'' Q''. P = Lam [x].P1 \<and> M2 = P''[x::=Q''] \<and> P1\<longrightarrow>\<^isub>1 P'' \<and> Q\<longrightarrow>\<^isub>1Q'' \<and> x\<sharp>(Q,Q'')" |
18344 | 428 |
then obtain x P1 P1'' Q'' where |
22540 | 429 |
b0: "P = Lam [x].P1" and b1: "M2 = P1''[x::=Q'']" and |
430 |
b2: "P1\<longrightarrow>\<^isub>1P1''" and b3: "Q\<longrightarrow>\<^isub>1Q''" and vc: "x\<sharp>(Q,Q'')" by blast |
|
25831 | 431 |
from b0 i0 have "\<exists>P1'. P'=Lam [x].P1' \<and> P1\<longrightarrow>\<^isub>1P1'" by (simp add: one_abs) |
18344 | 432 |
then obtain P1' where g1: "P'=Lam [x].P1'" and g2: "P1\<longrightarrow>\<^isub>1P1'" by blast |
433 |
from g1 b0 b2 i2 have "(\<exists>M3. (Lam [x].P1')\<longrightarrow>\<^isub>1M3 \<and> (Lam [x].P1'')\<longrightarrow>\<^isub>1M3)" by simp |
|
434 |
then obtain P1''' where |
|
435 |
c1: "(Lam [x].P1')\<longrightarrow>\<^isub>1P1'''" and c2: "(Lam [x].P1'')\<longrightarrow>\<^isub>1P1'''" by blast |
|
436 |
from c1 have "\<exists>R1. P1'''=Lam [x].R1 \<and> P1'\<longrightarrow>\<^isub>1R1" by (simp add: one_abs) |
|
437 |
then obtain R1 where r1: "P1'''=Lam [x].R1" and r2: "P1'\<longrightarrow>\<^isub>1R1" by blast |
|
438 |
from c2 have "\<exists>R2. P1'''=Lam [x].R2 \<and> P1''\<longrightarrow>\<^isub>1R2" by (simp add: one_abs) |
|
439 |
then obtain R2 where r3: "P1'''=Lam [x].R2" and r4: "P1''\<longrightarrow>\<^isub>1R2" by blast |
|
440 |
from r1 r3 have r5: "R1=R2" by (simp add: lam.inject alpha) |
|
441 |
from b3 i1 have "(\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> Q''\<longrightarrow>\<^isub>1M3)" by simp |
|
442 |
then obtain Q''' where |
|
443 |
d1: "Q'\<longrightarrow>\<^isub>1Q'''" and d2: "Q''\<longrightarrow>\<^isub>1Q'''" by blast |
|
444 |
from g1 r2 d1 r4 r5 d2 |
|
22540 | 445 |
have "App P' Q'\<longrightarrow>\<^isub>1R1[x::=Q'''] \<and> P1''[x::=Q'']\<longrightarrow>\<^isub>1R1[x::=Q''']" |
446 |
using vc i0' by (simp add: one_subst one_fresh_preserv) |
|
18344 | 447 |
hence "\<exists>M3. App P' Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 by blast |
448 |
} |
|
449 |
ultimately show "\<exists>M3. App P' Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" by blast |
|
18106 | 450 |
next |
21101 | 451 |
case (o3 P P' x) (* case 4 *) |
18344 | 452 |
have i1: "P\<longrightarrow>\<^isub>1P'" by fact |
453 |
have i2: "\<And>M2. P \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact |
|
454 |
have "(Lam [x].P)\<longrightarrow>\<^isub>1 M2" by fact |
|
455 |
hence "\<exists>P''. M2=Lam [x].P'' \<and> P\<longrightarrow>\<^isub>1P''" by (simp add: one_abs) |
|
456 |
then obtain P'' where b1: "M2=Lam [x].P''" and b2: "P\<longrightarrow>\<^isub>1P''" by blast |
|
457 |
from i2 b1 b2 have "\<exists>M3. (Lam [x].P')\<longrightarrow>\<^isub>1M3 \<and> (Lam [x].P'')\<longrightarrow>\<^isub>1M3" by blast |
|
458 |
then obtain M3 where c1: "(Lam [x].P')\<longrightarrow>\<^isub>1M3" and c2: "(Lam [x].P'')\<longrightarrow>\<^isub>1M3" by blast |
|
459 |
from c1 have "\<exists>R1. M3=Lam [x].R1 \<and> P'\<longrightarrow>\<^isub>1R1" by (simp add: one_abs) |
|
460 |
then obtain R1 where r1: "M3=Lam [x].R1" and r2: "P'\<longrightarrow>\<^isub>1R1" by blast |
|
461 |
from c2 have "\<exists>R2. M3=Lam [x].R2 \<and> P''\<longrightarrow>\<^isub>1R2" by (simp add: one_abs) |
|
462 |
then obtain R2 where r3: "M3=Lam [x].R2" and r4: "P''\<longrightarrow>\<^isub>1R2" by blast |
|
463 |
from r1 r3 have r5: "R1=R2" by (simp add: lam.inject alpha) |
|
464 |
from r2 r4 have "(Lam [x].P')\<longrightarrow>\<^isub>1(Lam [x].R1) \<and> (Lam [x].P'')\<longrightarrow>\<^isub>1(Lam [x].R2)" |
|
465 |
by (simp add: one_subst) |
|
466 |
thus "\<exists>M3. (Lam [x].P')\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 r5 by blast |
|
18106 | 467 |
qed |
468 |
||
18882
454d09651d1a
- renamed some lemmas (some had names coming from ancient
urbanc
parents:
18773
diff
changeset
|
469 |
lemma one_lam_cong: |
18106 | 470 |
assumes a: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" |
471 |
shows "(Lam [a].t1)\<longrightarrow>\<^isub>\<beta>\<^sup>*(Lam [a].t2)" |
|
472 |
using a |
|
473 |
proof induct |
|
21101 | 474 |
case bs1 thus ?case by simp |
18106 | 475 |
next |
21101 | 476 |
case (bs2 y z) |
477 |
thus ?case by (blast dest: b3) |
|
18106 | 478 |
qed |
479 |
||
18378 | 480 |
lemma one_app_congL: |
18106 | 481 |
assumes a: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" |
482 |
shows "App t1 s\<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s" |
|
483 |
using a |
|
484 |
proof induct |
|
21101 | 485 |
case bs1 thus ?case by simp |
18106 | 486 |
next |
21101 | 487 |
case bs2 thus ?case by (blast dest: b1) |
18106 | 488 |
qed |
489 |
||
18378 | 490 |
lemma one_app_congR: |
18106 | 491 |
assumes a: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" |
492 |
shows "App s t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App s t2" |
|
493 |
using a |
|
494 |
proof induct |
|
21101 | 495 |
case bs1 thus ?case by simp |
18106 | 496 |
next |
21101 | 497 |
case bs2 thus ?case by (blast dest: b2) |
18106 | 498 |
qed |
499 |
||
18378 | 500 |
lemma one_app_cong: |
18106 | 501 |
assumes a1: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" |
21101 | 502 |
and a2: "s1\<longrightarrow>\<^isub>\<beta>\<^sup>*s2" |
18106 | 503 |
shows "App t1 s1\<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s2" |
504 |
proof - |
|
18378 | 505 |
have "App t1 s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s1" using a1 by (rule one_app_congL) |
506 |
moreover |
|
507 |
have "App t2 s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s2" using a2 by (rule one_app_congR) |
|
21101 | 508 |
ultimately show ?thesis by (rule beta_star_trans) |
18106 | 509 |
qed |
510 |
||
511 |
lemma one_beta_star: |
|
512 |
assumes a: "(t1\<longrightarrow>\<^isub>1t2)" |
|
513 |
shows "(t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2)" |
|
514 |
using a |
|
22540 | 515 |
proof(nominal_induct rule: One.strong_induct) |
18378 | 516 |
case o1 thus ?case by simp |
18106 | 517 |
next |
18378 | 518 |
case o2 thus ?case by (blast intro!: one_app_cong) |
18106 | 519 |
next |
18882
454d09651d1a
- renamed some lemmas (some had names coming from ancient
urbanc
parents:
18773
diff
changeset
|
520 |
case o3 thus ?case by (blast intro!: one_lam_cong) |
18106 | 521 |
next |
22540 | 522 |
case (o4 a s1 s2 t1 t2) |
23393 | 523 |
have vc: "a\<sharp>s1" "a\<sharp>s2" by fact+ |
524 |
have a1: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" and a2: "s1\<longrightarrow>\<^isub>\<beta>\<^sup>*s2" by fact+ |
|
22540 | 525 |
have c1: "(App (Lam [a].t2) s2) \<longrightarrow>\<^isub>\<beta> (t2 [a::= s2])" using vc by (simp add: b4) |
18106 | 526 |
from a1 a2 have c2: "App (Lam [a].t1 ) s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App (Lam [a].t2 ) s2" |
18882
454d09651d1a
- renamed some lemmas (some had names coming from ancient
urbanc
parents:
18773
diff
changeset
|
527 |
by (blast intro!: one_app_cong one_lam_cong) |
21101 | 528 |
show ?case using c2 c1 by (blast intro: beta_star_trans) |
18106 | 529 |
qed |
530 |
||
18882
454d09651d1a
- renamed some lemmas (some had names coming from ancient
urbanc
parents:
18773
diff
changeset
|
531 |
lemma one_star_lam_cong: |
18106 | 532 |
assumes a: "t1\<longrightarrow>\<^isub>1\<^sup>*t2" |
533 |
shows "(Lam [a].t1)\<longrightarrow>\<^isub>1\<^sup>* (Lam [a].t2)" |
|
534 |
using a |
|
535 |
proof induct |
|
21101 | 536 |
case os1 thus ?case by simp |
18106 | 537 |
next |
21101 | 538 |
case os2 thus ?case by (blast intro: one_star_trans) |
18106 | 539 |
qed |
540 |
||
18882
454d09651d1a
- renamed some lemmas (some had names coming from ancient
urbanc
parents:
18773
diff
changeset
|
541 |
lemma one_star_app_congL: |
18106 | 542 |
assumes a: "t1\<longrightarrow>\<^isub>1\<^sup>*t2" |
543 |
shows "App t1 s\<longrightarrow>\<^isub>1\<^sup>* App t2 s" |
|
544 |
using a |
|
545 |
proof induct |
|
21101 | 546 |
case os1 thus ?case by simp |
18106 | 547 |
next |
21101 | 548 |
case os2 thus ?case by (blast intro: one_star_trans) |
18106 | 549 |
qed |
550 |
||
18882
454d09651d1a
- renamed some lemmas (some had names coming from ancient
urbanc
parents:
18773
diff
changeset
|
551 |
lemma one_star_app_congR: |
18106 | 552 |
assumes a: "t1\<longrightarrow>\<^isub>1\<^sup>*t2" |
553 |
shows "App s t1 \<longrightarrow>\<^isub>1\<^sup>* App s t2" |
|
554 |
using a |
|
555 |
proof induct |
|
21101 | 556 |
case os1 thus ?case by simp |
18106 | 557 |
next |
21101 | 558 |
case os2 thus ?case by (blast intro: one_star_trans) |
18106 | 559 |
qed |
560 |
||
561 |
lemma beta_one_star: |
|
562 |
assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2" |
|
563 |
shows "t1\<longrightarrow>\<^isub>1\<^sup>*t2" |
|
564 |
using a |
|
22540 | 565 |
proof(induct) |
18882
454d09651d1a
- renamed some lemmas (some had names coming from ancient
urbanc
parents:
18773
diff
changeset
|
566 |
case b1 thus ?case by (blast intro!: one_star_app_congL) |
18106 | 567 |
next |
18882
454d09651d1a
- renamed some lemmas (some had names coming from ancient
urbanc
parents:
18773
diff
changeset
|
568 |
case b2 thus ?case by (blast intro!: one_star_app_congR) |
18106 | 569 |
next |
18882
454d09651d1a
- renamed some lemmas (some had names coming from ancient
urbanc
parents:
18773
diff
changeset
|
570 |
case b3 thus ?case by (blast intro!: one_star_lam_cong) |
18106 | 571 |
next |
22540 | 572 |
case b4 thus ?case by auto |
18106 | 573 |
qed |
574 |
||
575 |
lemma trans_closure: |
|
21101 | 576 |
shows "(M1\<longrightarrow>\<^isub>1\<^sup>*M2) = (M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M2)" |
18106 | 577 |
proof |
21101 | 578 |
assume "M1 \<longrightarrow>\<^isub>1\<^sup>* M2" |
579 |
then show "M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M2" |
|
18106 | 580 |
proof induct |
21101 | 581 |
case (os1 M1) thus "M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M1" by simp |
18106 | 582 |
next |
21101 | 583 |
case (os2 M1 M2 M3) |
584 |
have "M2\<longrightarrow>\<^isub>1M3" by fact |
|
585 |
then have "M2\<longrightarrow>\<^isub>\<beta>\<^sup>*M3" by (rule one_beta_star) |
|
586 |
moreover have "M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M2" by fact |
|
587 |
ultimately show "M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M3" by (auto intro: beta_star_trans) |
|
18106 | 588 |
qed |
589 |
next |
|
21101 | 590 |
assume "M1 \<longrightarrow>\<^isub>\<beta>\<^sup>* M2" |
591 |
then show "M1\<longrightarrow>\<^isub>1\<^sup>*M2" |
|
18106 | 592 |
proof induct |
21101 | 593 |
case (bs1 M1) thus "M1\<longrightarrow>\<^isub>1\<^sup>*M1" by simp |
18106 | 594 |
next |
21101 | 595 |
case (bs2 M1 M2 M3) |
596 |
have "M2\<longrightarrow>\<^isub>\<beta>M3" by fact |
|
597 |
then have "M2\<longrightarrow>\<^isub>1\<^sup>*M3" by (rule beta_one_star) |
|
598 |
moreover have "M1\<longrightarrow>\<^isub>1\<^sup>*M2" by fact |
|
599 |
ultimately show "M1\<longrightarrow>\<^isub>1\<^sup>*M3" by (auto intro: one_star_trans) |
|
18106 | 600 |
qed |
601 |
qed |
|
602 |
||
603 |
lemma cr_one: |
|
604 |
assumes a: "t\<longrightarrow>\<^isub>1\<^sup>*t1" |
|
18344 | 605 |
and b: "t\<longrightarrow>\<^isub>1t2" |
18106 | 606 |
shows "\<exists>t3. t1\<longrightarrow>\<^isub>1t3 \<and> t2\<longrightarrow>\<^isub>1\<^sup>*t3" |
18344 | 607 |
using a b |
20503 | 608 |
proof (induct arbitrary: t2) |
21101 | 609 |
case os1 thus ?case by force |
18344 | 610 |
next |
21101 | 611 |
case (os2 t s1 s2 t2) |
18344 | 612 |
have b: "s1 \<longrightarrow>\<^isub>1 s2" by fact |
613 |
have h: "\<And>t2. t \<longrightarrow>\<^isub>1 t2 \<Longrightarrow> (\<exists>t3. s1 \<longrightarrow>\<^isub>1 t3 \<and> t2 \<longrightarrow>\<^isub>1\<^sup>* t3)" by fact |
|
614 |
have c: "t \<longrightarrow>\<^isub>1 t2" by fact |
|
18378 | 615 |
show "\<exists>t3. s2 \<longrightarrow>\<^isub>1 t3 \<and> t2 \<longrightarrow>\<^isub>1\<^sup>* t3" |
18344 | 616 |
proof - |
18378 | 617 |
from c h have "\<exists>t3. s1 \<longrightarrow>\<^isub>1 t3 \<and> t2 \<longrightarrow>\<^isub>1\<^sup>* t3" by blast |
618 |
then obtain t3 where c1: "s1 \<longrightarrow>\<^isub>1 t3" and c2: "t2 \<longrightarrow>\<^isub>1\<^sup>* t3" by blast |
|
619 |
have "\<exists>t4. s2 \<longrightarrow>\<^isub>1 t4 \<and> t3 \<longrightarrow>\<^isub>1 t4" using b c1 by (blast intro: diamond) |
|
21101 | 620 |
thus ?thesis using c2 by (blast intro: one_star_trans) |
18106 | 621 |
qed |
622 |
qed |
|
623 |
||
624 |
lemma cr_one_star: |
|
625 |
assumes a: "t\<longrightarrow>\<^isub>1\<^sup>*t2" |
|
626 |
and b: "t\<longrightarrow>\<^isub>1\<^sup>*t1" |
|
18378 | 627 |
shows "\<exists>t3. t1\<longrightarrow>\<^isub>1\<^sup>*t3\<and>t2\<longrightarrow>\<^isub>1\<^sup>*t3" |
21101 | 628 |
using a b |
629 |
proof (induct arbitrary: t1) |
|
630 |
case (os1 t) then show ?case by force |
|
18106 | 631 |
next |
21101 | 632 |
case (os2 t s1 s2 t1) |
633 |
have c: "t \<longrightarrow>\<^isub>1\<^sup>* s1" by fact |
|
634 |
have c': "t \<longrightarrow>\<^isub>1\<^sup>* t1" by fact |
|
18882
454d09651d1a
- renamed some lemmas (some had names coming from ancient
urbanc
parents:
18773
diff
changeset
|
635 |
have d: "s1 \<longrightarrow>\<^isub>1 s2" by fact |
21101 | 636 |
have "t \<longrightarrow>\<^isub>1\<^sup>* t1 \<Longrightarrow> (\<exists>t3. t1 \<longrightarrow>\<^isub>1\<^sup>* t3 \<and> s1 \<longrightarrow>\<^isub>1\<^sup>* t3)" by fact |
18106 | 637 |
then obtain t3 where f1: "t1 \<longrightarrow>\<^isub>1\<^sup>* t3" |
21101 | 638 |
and f2: "s1 \<longrightarrow>\<^isub>1\<^sup>* t3" using c' by blast |
18378 | 639 |
from cr_one d f2 have "\<exists>t4. t3\<longrightarrow>\<^isub>1t4 \<and> s2\<longrightarrow>\<^isub>1\<^sup>*t4" by blast |
18106 | 640 |
then obtain t4 where g1: "t3\<longrightarrow>\<^isub>1t4" |
18378 | 641 |
and g2: "s2\<longrightarrow>\<^isub>1\<^sup>*t4" by blast |
21101 | 642 |
have "t1\<longrightarrow>\<^isub>1\<^sup>*t4" using f1 g1 by (blast intro: one_star_trans) |
18378 | 643 |
thus ?case using g2 by blast |
18106 | 644 |
qed |
645 |
||
646 |
lemma cr_beta_star: |
|
647 |
assumes a1: "t\<longrightarrow>\<^isub>\<beta>\<^sup>*t1" |
|
18882
454d09651d1a
- renamed some lemmas (some had names coming from ancient
urbanc
parents:
18773
diff
changeset
|
648 |
and a2: "t\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" |
18378 | 649 |
shows "\<exists>t3. t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t3\<and>t2\<longrightarrow>\<^isub>\<beta>\<^sup>*t3" |
18106 | 650 |
proof - |
18882
454d09651d1a
- renamed some lemmas (some had names coming from ancient
urbanc
parents:
18773
diff
changeset
|
651 |
from a1 have "t\<longrightarrow>\<^isub>1\<^sup>*t1" by (simp only: trans_closure) |
18378 | 652 |
moreover |
18882
454d09651d1a
- renamed some lemmas (some had names coming from ancient
urbanc
parents:
18773
diff
changeset
|
653 |
from a2 have "t\<longrightarrow>\<^isub>1\<^sup>*t2" by (simp only: trans_closure) |
454d09651d1a
- renamed some lemmas (some had names coming from ancient
urbanc
parents:
18773
diff
changeset
|
654 |
ultimately have "\<exists>t3. t1\<longrightarrow>\<^isub>1\<^sup>*t3 \<and> t2\<longrightarrow>\<^isub>1\<^sup>*t3" by (blast intro: cr_one_star) |
454d09651d1a
- renamed some lemmas (some had names coming from ancient
urbanc
parents:
18773
diff
changeset
|
655 |
then obtain t3 where "t1\<longrightarrow>\<^isub>1\<^sup>*t3" and "t2\<longrightarrow>\<^isub>1\<^sup>*t3" by blast |
454d09651d1a
- renamed some lemmas (some had names coming from ancient
urbanc
parents:
18773
diff
changeset
|
656 |
hence "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t3" and "t2\<longrightarrow>\<^isub>\<beta>\<^sup>*t3" by (simp_all only: trans_closure) |
454d09651d1a
- renamed some lemmas (some had names coming from ancient
urbanc
parents:
18773
diff
changeset
|
657 |
then show "\<exists>t3. t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t3\<and>t2\<longrightarrow>\<^isub>\<beta>\<^sup>*t3" by blast |
18106 | 658 |
qed |
659 |
||
660 |
end |
|
661 |