author | urbanc |
Mon, 27 Nov 2006 14:05:43 +0100 | |
changeset 21555 | 229c0158de92 |
parent 21377 | c29146dc14f1 |
child 22540 | e4817fa0f6a1 |
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 |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
13 |
proof (nominal_induct L avoiding: x P rule: lam.induct) |
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) |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
27 |
have vc: "z\<sharp>x" "z\<sharp>P" by fact |
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 |
39 |
by (nominal_induct L avoiding: x P rule: lam.induct) |
|
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 |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
47 |
proof (nominal_induct N avoiding: z y L rule: lam.induct) |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
48 |
case (Var u) |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
49 |
have "z\<sharp>(Var u)" "z\<sharp>L" by fact |
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 |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
57 |
have "z\<sharp>App N1 N2" "z\<sharp>L" by fact |
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) |
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
61 |
have vc: "u\<sharp>z" "u\<sharp>y" "u\<sharp>L" by fact |
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 |
76 |
by (nominal_induct N avoiding: z y L rule: lam.induct) |
|
77 |
(auto simp add: abs_fresh fresh_atm) |
|
18106 | 78 |
|
20955
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
79 |
lemma substitution_lemma: |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
80 |
assumes a: "x\<noteq>y" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
81 |
and b: "x\<sharp>L" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
82 |
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
|
83 |
using a b |
18659
2ff0ae57431d
changes to make use of the new induction principle proved by
urbanc
parents:
18378
diff
changeset
|
84 |
proof (nominal_induct M avoiding: x y N L rule: lam.induct) |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
85 |
case (Var z) (* case 1: Variables*) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
86 |
have "x\<noteq>y" by fact |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
87 |
have "x\<sharp>L" by fact |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
88 |
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
|
89 |
proof - |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
90 |
{ (*Case 1.1*) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
91 |
assume "z=x" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
92 |
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
|
93 |
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
|
94 |
from "(1)" "(2)" have "?LHS = ?RHS" by simp |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
95 |
} |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
96 |
moreover |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
97 |
{ (*Case 1.2*) |
20955
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
98 |
assume "z=y" and "z\<noteq>x" |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
99 |
have "(1)": "?LHS = L" using `z\<noteq>x` `z=y` by force |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
100 |
have "(2)": "?RHS = L[x::=N[y::=L]]" using `z=y` by force |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
101 |
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
|
102 |
from "(1)" "(2)" "(3)" 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.3*) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
106 |
assume "z\<noteq>x" and "z\<noteq>y" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
107 |
have "(1)": "?LHS = Var z" using `z\<noteq>x` `z\<noteq>y` by force |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
108 |
have "(2)": "?RHS = Var z" using `z\<noteq>x` `z\<noteq>y` by force |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
109 |
from "(1)" "(2)" have "?LHS = ?RHS" by simp |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
110 |
} |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
111 |
ultimately show "?LHS = ?RHS" by blast |
18106 | 112 |
qed |
113 |
next |
|
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
114 |
case (Lam z M1) (* case 2: lambdas *) |
20955
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
115 |
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
|
116 |
have "x\<noteq>y" by fact |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
117 |
have "x\<sharp>L" by fact |
19477 | 118 |
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
|
119 |
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
|
120 |
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
|
121 |
proof - |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
122 |
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
|
123 |
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
|
124 |
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
|
125 |
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
|
126 |
finally show "?LHS = ?RHS" . |
18106 | 127 |
qed |
128 |
next |
|
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
129 |
case (App M1 M2) (* case 3: applications *) |
21101 | 130 |
thus "(App M1 M2)[x::=N][y::=L] = (App M1 M2)[y::=L][x::=N[y::=L]]" by simp |
18106 | 131 |
qed |
132 |
||
20955
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
133 |
lemma substitution_lemma_automatic: |
19172
ad36a9b42cf3
made some small changes to generate nicer latex-output
urbanc
parents:
18882
diff
changeset
|
134 |
assumes asm: "x\<noteq>y" "x\<sharp>L" |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
135 |
shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]" |
21101 | 136 |
using asm |
137 |
by (nominal_induct M avoiding: x y N L rule: lam.induct) |
|
138 |
(auto simp add: fresh_fact forget) |
|
18106 | 139 |
|
18344 | 140 |
lemma subst_rename: |
21101 | 141 |
assumes a: "y\<sharp>N" |
142 |
shows "N[x::=L] = ([(y,x)]\<bullet>N)[y::=L]" |
|
18344 | 143 |
using a |
21101 | 144 |
proof (nominal_induct N avoiding: x y L rule: lam.induct) |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
145 |
case (Var b) |
21101 | 146 |
thus "(Var b)[x::=L] = ([(y,x)]\<bullet>(Var b))[y::=L]" by (simp add: calc_atm fresh_atm) |
18106 | 147 |
next |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
148 |
case App thus ?case by force |
18106 | 149 |
next |
21101 | 150 |
case (Lam b N1) |
151 |
have ih: "y\<sharp>N1 \<Longrightarrow> (N1[x::=L] = ([(y,x)]\<bullet>N1)[y::=L])" by fact |
|
21555 | 152 |
have vc: "b\<sharp>y" "b\<sharp>x" "b\<sharp>L" by fact |
21101 | 153 |
have "y\<sharp>Lam [b].N1" by fact |
21555 | 154 |
hence "y\<sharp>N1" using vc by (simp add: abs_fresh fresh_atm) |
21101 | 155 |
hence d: "N1[x::=L] = ([(y,x)]\<bullet>N1)[y::=L]" using ih by simp |
156 |
show "(Lam [b].N1)[x::=L] = ([(y,x)]\<bullet>(Lam [b].N1))[y::=L]" (is "?LHS = ?RHS") |
|
18344 | 157 |
proof - |
21555 | 158 |
have "?LHS = Lam [b].(N1[x::=L])" using vc by simp |
21101 | 159 |
also have "\<dots> = Lam [b].(([(y,x)]\<bullet>N1)[y::=L])" using d by simp |
21555 | 160 |
also have "\<dots> = (Lam [b].([(y,x)]\<bullet>N1))[y::=L]" using vc by simp |
161 |
also have "\<dots> = ?RHS" using vc by (simp add: calc_atm fresh_atm) |
|
18106 | 162 |
finally show "?LHS = ?RHS" by simp |
163 |
qed |
|
164 |
qed |
|
165 |
||
18378 | 166 |
lemma subst_rename_automatic: |
21101 | 167 |
assumes a: "y\<sharp>N" |
168 |
shows "N[x::=L] = ([(y,x)]\<bullet>N)[y::=L]" |
|
169 |
using a |
|
170 |
by (nominal_induct N avoiding: y x L rule: lam.induct) |
|
171 |
(auto simp add: calc_atm fresh_atm abs_fresh) |
|
18106 | 172 |
|
173 |
section {* Beta Reduction *} |
|
174 |
||
21101 | 175 |
inductive2 |
176 |
"Beta" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80) |
|
21366 | 177 |
where |
178 |
b1[intro]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App s1 t)\<longrightarrow>\<^isub>\<beta>(App s2 t)" |
|
179 |
| b2[intro]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App t s1)\<longrightarrow>\<^isub>\<beta>(App t s2)" |
|
180 |
| b3[intro]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>\<beta> (Lam [a].s2)" |
|
181 |
| b4[intro]: "(App (Lam [a].s1) s2)\<longrightarrow>\<^isub>\<beta>(s1[a::=s2])" |
|
18106 | 182 |
|
21101 | 183 |
inductive2 |
184 |
"Beta_star" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80) |
|
21366 | 185 |
where |
186 |
bs1[intro, simp]: "M \<longrightarrow>\<^isub>\<beta>\<^sup>* M" |
|
187 |
| bs2[intro]: "\<lbrakk>M1\<longrightarrow>\<^isub>\<beta>\<^sup>* M2; M2 \<longrightarrow>\<^isub>\<beta> M3\<rbrakk> \<Longrightarrow> M1 \<longrightarrow>\<^isub>\<beta>\<^sup>* M3" |
|
21101 | 188 |
|
189 |
lemma beta_star_trans: |
|
190 |
assumes a1: "M1\<longrightarrow>\<^isub>\<beta>\<^sup>* M2" |
|
191 |
and a2: "M2\<longrightarrow>\<^isub>\<beta>\<^sup>* M3" |
|
192 |
shows "M1 \<longrightarrow>\<^isub>\<beta>\<^sup>* M3" |
|
193 |
using a2 a1 |
|
194 |
by (induct) (auto) |
|
195 |
||
196 |
lemma eqvt_beta: |
|
18106 | 197 |
fixes pi :: "name prm" |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
198 |
assumes a: "t\<longrightarrow>\<^isub>\<beta>s" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
199 |
shows "(pi\<bullet>t)\<longrightarrow>\<^isub>\<beta>(pi\<bullet>s)" |
21101 | 200 |
using a |
201 |
by (induct) (auto) |
|
18106 | 202 |
|
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
203 |
lemma beta_induct[consumes 1, case_names b1 b2 b3 b4]: |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
204 |
fixes P :: "'a::fs_name\<Rightarrow>lam \<Rightarrow> lam \<Rightarrow>bool" |
18106 | 205 |
and t :: "lam" |
206 |
and s :: "lam" |
|
207 |
and x :: "'a::fs_name" |
|
208 |
assumes a: "t\<longrightarrow>\<^isub>\<beta>s" |
|
21101 | 209 |
and a1: "\<And>t s1 s2 x. \<lbrakk>s1\<longrightarrow>\<^isub>\<beta>s2; (\<And>z. P z s1 s2)\<rbrakk> \<Longrightarrow> P x (App s1 t) (App s2 t)" |
210 |
and a2: "\<And>t s1 s2 x. \<lbrakk>s1\<longrightarrow>\<^isub>\<beta>s2; (\<And>z. P z s1 s2)\<rbrakk> \<Longrightarrow> P x (App t s1) (App t s2)" |
|
211 |
and a3: "\<And>a s1 s2 x. \<lbrakk>a\<sharp>x; s1\<longrightarrow>\<^isub>\<beta>s2; (\<And>z. P z s1 s2)\<rbrakk> \<Longrightarrow> P x (Lam [a].s1) (Lam [a].s2)" |
|
18773
0eabf66582d0
the additional freshness-condition in the one-induction
urbanc
parents:
18659
diff
changeset
|
212 |
and a4: "\<And>a t1 s1 x. a\<sharp>x \<Longrightarrow> P x (App (Lam [a].t1) s1) (t1[a::=s1])" |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
213 |
shows "P x t s" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
214 |
proof - |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
215 |
from a have "\<And>(pi::name prm) x. P x (pi\<bullet>t) (pi\<bullet>s)" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
216 |
proof (induct) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
217 |
case b1 thus ?case using a1 by (simp, blast intro: eqvt_beta) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
218 |
next |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
219 |
case b2 thus ?case using a2 by (simp, blast intro: eqvt_beta) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
220 |
next |
21101 | 221 |
case (b3 s1 s2 a) |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
222 |
have j1: "s1 \<longrightarrow>\<^isub>\<beta> s2" by fact |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
223 |
have j2: "\<And>x (pi::name prm). P x (pi\<bullet>s1) (pi\<bullet>s2)" by fact |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
224 |
show ?case |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
225 |
proof (simp) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
226 |
have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)" |
21377
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21366
diff
changeset
|
227 |
by (rule exists_fresh', simp add: fs_name1) |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
228 |
then obtain c::"name" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
229 |
where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>s1)" and f4: "c\<sharp>(pi\<bullet>s2)" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
230 |
by (force simp add: fresh_prod fresh_atm) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
231 |
have x: "P x (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s1)) (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s2))" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
232 |
using a3 f2 j1 j2 by (simp, blast intro: eqvt_beta) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
233 |
have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s1))" using f1 f3 |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
234 |
by (simp add: lam.inject alpha) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
235 |
have alpha2: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s2))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s2))" using f1 f3 |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
236 |
by (simp add: lam.inject alpha) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
237 |
show " P x (Lam [(pi\<bullet>a)].(pi\<bullet>s1)) (Lam [(pi\<bullet>a)].(pi\<bullet>s2))" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
238 |
using x alpha1 alpha2 by (simp only: pt_name2) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
239 |
qed |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
240 |
next |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
241 |
case (b4 a s1 s2) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
242 |
show ?case |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
243 |
proof (simp add: subst_eqvt) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
244 |
have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)" |
21377
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21366
diff
changeset
|
245 |
by (rule exists_fresh', simp add: fs_name1) |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
246 |
then obtain c::"name" |
18773
0eabf66582d0
the additional freshness-condition in the one-induction
urbanc
parents:
18659
diff
changeset
|
247 |
where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>s1)" and f4: "c\<sharp>(pi\<bullet>s2)" |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
248 |
by (force simp add: fresh_prod fresh_atm) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
249 |
have x: "P x (App (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s1)) (pi\<bullet>s2)) ((([(c,pi\<bullet>a)]@pi)\<bullet>s1)[c::=(pi\<bullet>s2)])" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
250 |
using a4 f2 by (blast intro!: eqvt_beta) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
251 |
have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s1))" using f1 f3 |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
252 |
by (simp add: lam.inject alpha) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
253 |
have alpha2: "(([(c,pi\<bullet>a)]@pi)\<bullet>s1)[c::=(pi\<bullet>s2)] = (pi\<bullet>s1)[(pi\<bullet>a)::=(pi\<bullet>s2)]" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
254 |
using f3 by (simp only: subst_rename[symmetric] pt_name2) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
255 |
show "P x (App (Lam [(pi\<bullet>a)].(pi\<bullet>s1)) (pi\<bullet>s2)) ((pi\<bullet>s1)[(pi\<bullet>a)::=(pi\<bullet>s2)])" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
256 |
using x alpha1 alpha2 by (simp only: pt_name2) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
257 |
qed |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
258 |
qed |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
259 |
hence "P x (([]::name prm)\<bullet>t) (([]::name prm)\<bullet>s)" by blast |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
260 |
thus ?thesis by simp |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
261 |
qed |
18106 | 262 |
|
263 |
section {* One-Reduction *} |
|
264 |
||
21101 | 265 |
inductive2 |
266 |
One :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>1 _" [80,80] 80) |
|
21366 | 267 |
where |
268 |
o1[intro!]: "M\<longrightarrow>\<^isub>1M" |
|
269 |
| o2[simp,intro!]: "\<lbrakk>t1\<longrightarrow>\<^isub>1t2;s1\<longrightarrow>\<^isub>1s2\<rbrakk> \<Longrightarrow> (App t1 s1)\<longrightarrow>\<^isub>1(App t2 s2)" |
|
270 |
| o3[simp,intro!]: "s1\<longrightarrow>\<^isub>1s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>1(Lam [a].s2)" |
|
271 |
| o4[simp,intro!]: "\<lbrakk>s1\<longrightarrow>\<^isub>1s2;t1\<longrightarrow>\<^isub>1t2\<rbrakk> \<Longrightarrow> (App (Lam [a].t1) s1)\<longrightarrow>\<^isub>1(t2[a::=s2])" |
|
18106 | 272 |
|
21101 | 273 |
inductive2 |
274 |
"One_star" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>1\<^sup>* _" [80,80] 80) |
|
21366 | 275 |
where |
276 |
os1[intro, simp]: "M \<longrightarrow>\<^isub>1\<^sup>* M" |
|
277 |
| os2[intro]: "\<lbrakk>M1\<longrightarrow>\<^isub>1\<^sup>* M2; M2 \<longrightarrow>\<^isub>1 M3\<rbrakk> \<Longrightarrow> M1 \<longrightarrow>\<^isub>1\<^sup>* M3" |
|
21101 | 278 |
|
18106 | 279 |
lemma eqvt_one: |
280 |
fixes pi :: "name prm" |
|
281 |
and t :: "lam" |
|
282 |
and s :: "lam" |
|
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
283 |
assumes a: "t\<longrightarrow>\<^isub>1s" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
284 |
shows "(pi\<bullet>t)\<longrightarrow>\<^isub>1(pi\<bullet>s)" |
21366 | 285 |
using a by (induct) (auto) |
18106 | 286 |
|
21101 | 287 |
lemma one_star_trans: |
288 |
assumes a1: "M1\<longrightarrow>\<^isub>1\<^sup>* M2" |
|
289 |
and a2: "M2\<longrightarrow>\<^isub>1\<^sup>* M3" |
|
290 |
shows "M1\<longrightarrow>\<^isub>1\<^sup>* M3" |
|
291 |
using a2 a1 |
|
292 |
by (induct) (auto) |
|
293 |
||
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
294 |
lemma one_induct[consumes 1, case_names o1 o2 o3 o4]: |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
295 |
fixes P :: "'a::fs_name\<Rightarrow>lam \<Rightarrow> lam \<Rightarrow>bool" |
18106 | 296 |
and t :: "lam" |
297 |
and s :: "lam" |
|
298 |
and x :: "'a::fs_name" |
|
299 |
assumes a: "t\<longrightarrow>\<^isub>1s" |
|
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
300 |
and a1: "\<And>t x. P x t t" |
21101 | 301 |
and a2: "\<And>t1 t2 s1 s2 x. \<lbrakk>t1\<longrightarrow>\<^isub>1t2; (\<And>z. P z t1 t2); s1\<longrightarrow>\<^isub>1s2; (\<And>z. P z s1 s2)\<rbrakk> \<Longrightarrow> |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
302 |
P x (App t1 s1) (App t2 s2)" |
21101 | 303 |
and a3: "\<And>a s1 s2 x. \<lbrakk>a\<sharp>x; s1\<longrightarrow>\<^isub>1s2; (\<And>z. P z s1 s2)\<rbrakk> \<Longrightarrow> P x (Lam [a].s1) (Lam [a].s2)" |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
304 |
and a4: "\<And>a t1 t2 s1 s2 x. |
21101 | 305 |
\<lbrakk>a\<sharp>x; t1\<longrightarrow>\<^isub>1t2; (\<And>z. P z t1 t2); s1\<longrightarrow>\<^isub>1s2; (\<And>z. P z s1 s2)\<rbrakk> |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
306 |
\<Longrightarrow> P x (App (Lam [a].t1) s1) (t2[a::=s2])" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
307 |
shows "P x t s" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
308 |
proof - |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
309 |
from a have "\<And>(pi::name prm) x. P x (pi\<bullet>t) (pi\<bullet>s)" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
310 |
proof (induct) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
311 |
case o1 show ?case using a1 by force |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
312 |
next |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
313 |
case (o2 s1 s2 t1 t2) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
314 |
thus ?case using a2 by (simp, blast intro: eqvt_one) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
315 |
next |
21101 | 316 |
case (o3 t1 t2 a) |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
317 |
have j1: "t1 \<longrightarrow>\<^isub>1 t2" by fact |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
318 |
have j2: "\<And>(pi::name prm) x. P x (pi\<bullet>t1) (pi\<bullet>t2)" by fact |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
319 |
show ?case |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
320 |
proof (simp) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
321 |
have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t1,pi\<bullet>t2,x)" |
21377
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21366
diff
changeset
|
322 |
by (rule exists_fresh', simp add: fs_name1) |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
323 |
then obtain c::"name" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
324 |
where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>t1)" and f4: "c\<sharp>(pi\<bullet>t2)" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
325 |
by (force simp add: fresh_prod fresh_atm) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
326 |
have x: "P x (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>t1)) (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>t2))" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
327 |
using a3 f2 j1 j2 by (simp, blast intro: eqvt_one) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
328 |
have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>t1))" using f1 f3 |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
329 |
by (simp add: lam.inject alpha) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
330 |
have alpha2: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t2))) = (Lam [(pi\<bullet>a)].(pi\<bullet>t2))" using f1 f3 |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
331 |
by (simp add: lam.inject alpha) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
332 |
show " P x (Lam [(pi\<bullet>a)].(pi\<bullet>t1)) (Lam [(pi\<bullet>a)].(pi\<bullet>t2))" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
333 |
using x alpha1 alpha2 by (simp only: pt_name2) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
334 |
qed |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
335 |
next |
21101 | 336 |
case (o4 s1 s2 t1 t2 a) |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
337 |
have j0: "t1 \<longrightarrow>\<^isub>1 t2" by fact |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
338 |
have j1: "s1 \<longrightarrow>\<^isub>1 s2" by fact |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
339 |
have j2: "\<And>(pi::name prm) x. P x (pi\<bullet>t1) (pi\<bullet>t2)" by fact |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
340 |
have j3: "\<And>(pi::name prm) x. P x (pi\<bullet>s1) (pi\<bullet>s2)" by fact |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
341 |
show ?case |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
342 |
proof (simp) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
343 |
have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t1,pi\<bullet>t2,pi\<bullet>s1,pi\<bullet>s2,x)" |
21377
c29146dc14f1
replaced exists_fresh lemma with a version formulated with obtains;
urbanc
parents:
21366
diff
changeset
|
344 |
by (rule exists_fresh', simp add: fs_name1) |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
345 |
then obtain c::"name" |
18773
0eabf66582d0
the additional freshness-condition in the one-induction
urbanc
parents:
18659
diff
changeset
|
346 |
where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>t1)" and f4: "c\<sharp>(pi\<bullet>t2)" |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
347 |
by (force simp add: fresh_prod at_fresh[OF at_name_inst]) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
348 |
have x: "P x (App (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>t1)) (pi\<bullet>s1)) ((([(c,pi\<bullet>a)]@pi)\<bullet>t2)[c::=(pi\<bullet>s2)])" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
349 |
using a4 f2 j0 j1 j2 j3 by (simp, blast intro!: eqvt_one) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
350 |
have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>t1))" using f1 f3 |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
351 |
by (simp add: lam.inject alpha) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
352 |
have alpha2: "(([(c,pi\<bullet>a)]@pi)\<bullet>t2)[c::=(pi\<bullet>s2)] = (pi\<bullet>t2)[(pi\<bullet>a)::=(pi\<bullet>s2)]" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
353 |
using f4 by (simp only: subst_rename[symmetric] pt_name2) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
354 |
show "P x (App (Lam [(pi\<bullet>a)].(pi\<bullet>t1)) (pi\<bullet>s1)) ((pi\<bullet>t2)[(pi\<bullet>a)::=(pi\<bullet>s2)])" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
355 |
using x alpha1 alpha2 by (simp only: pt_name2) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
356 |
qed |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
357 |
qed |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
358 |
hence "P x (([]::name prm)\<bullet>t) (([]::name prm)\<bullet>s)" by blast |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
359 |
thus ?thesis by simp |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
360 |
qed |
18106 | 361 |
|
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
362 |
lemma fresh_fact': |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
363 |
assumes a: "a\<sharp>t2" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
364 |
shows "a\<sharp>(t1[a::=t2])" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
365 |
using a |
18659
2ff0ae57431d
changes to make use of the new induction principle proved by
urbanc
parents:
18378
diff
changeset
|
366 |
proof (nominal_induct t1 avoiding: a t2 rule: lam.induct) |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
367 |
case (Var b) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
368 |
thus ?case by (simp add: fresh_atm) |
18106 | 369 |
next |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
370 |
case App thus ?case by simp |
18106 | 371 |
next |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
372 |
case (Lam c t) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
373 |
have "a\<sharp>t2" "c\<sharp>a" "c\<sharp>t2" by fact |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
374 |
moreover |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
375 |
have ih: "\<And>a t2. a\<sharp>t2 \<Longrightarrow> a\<sharp>(t[a::=t2])" by fact |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
376 |
ultimately show ?case by (simp add: abs_fresh) |
18106 | 377 |
qed |
378 |
||
18312
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
379 |
lemma one_fresh_preserv: |
18378 | 380 |
fixes a :: "name" |
18106 | 381 |
assumes a: "t\<longrightarrow>\<^isub>1s" |
18312
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
382 |
and b: "a\<sharp>t" |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
383 |
shows "a\<sharp>s" |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
384 |
using a b |
18106 | 385 |
proof (induct) |
18312
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
386 |
case o1 thus ?case by simp |
18106 | 387 |
next |
18312
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
388 |
case o2 thus ?case by simp |
18106 | 389 |
next |
21101 | 390 |
case (o3 s1 s2 c) |
18312
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
391 |
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
|
392 |
have c: "a\<sharp>Lam [c].s1" by fact |
18106 | 393 |
show ?case |
18312
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
394 |
proof (cases "a=c") |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
395 |
assume "a=c" thus "a\<sharp>Lam [c].s2" by (simp add: abs_fresh) |
18106 | 396 |
next |
18312
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
397 |
assume d: "a\<noteq>c" |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
398 |
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
|
399 |
hence "a\<sharp>s2" using ih by simp |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
400 |
thus "a\<sharp>Lam [c].s2" using d by (simp add: abs_fresh) |
18106 | 401 |
qed |
402 |
next |
|
21101 | 403 |
case (o4 t1 t2 s1 s2 c) |
18312
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
404 |
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
|
405 |
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
|
406 |
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
|
407 |
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
|
408 |
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
|
409 |
show "a\<sharp>s2[c::=t2]" |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
410 |
proof (cases "a=c") |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
411 |
assume "a=c" |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
412 |
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
|
413 |
next |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
414 |
assume d1: "a\<noteq>c" |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
415 |
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
|
416 |
hence "a\<sharp>s2" using i2 by simp |
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
417 |
thus "a\<sharp>s2[c::=t2]" using c3 by (simp add: fresh_fact) |
18106 | 418 |
qed |
419 |
qed |
|
420 |
||
421 |
lemma one_abs: |
|
422 |
fixes t :: "lam" |
|
423 |
and t':: "lam" |
|
424 |
and a :: "name" |
|
21101 | 425 |
assumes a: "(Lam [a].t)\<longrightarrow>\<^isub>1t'" |
426 |
shows "\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>1t''" |
|
427 |
using a |
|
428 |
apply - |
|
429 |
apply(ind_cases2 "(Lam [a].t)\<longrightarrow>\<^isub>1t'") |
|
18106 | 430 |
apply(auto simp add: lam.distinct lam.inject alpha) |
431 |
apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI) |
|
432 |
apply(rule conjI) |
|
433 |
apply(rule pt_bij2[OF pt_name_inst, OF at_name_inst, symmetric]) |
|
434 |
apply(simp) |
|
435 |
apply(rule pt_name3) |
|
436 |
apply(rule at_ds5[OF at_name_inst]) |
|
437 |
apply(frule_tac a="a" in one_fresh_preserv) |
|
438 |
apply(assumption) |
|
439 |
apply(rule conjI) |
|
440 |
apply(simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst]) |
|
441 |
apply(simp add: calc_atm) |
|
442 |
apply(force intro!: eqvt_one) |
|
443 |
done |
|
444 |
||
445 |
lemma one_app: |
|
21101 | 446 |
assumes a: "App t1 t2 \<longrightarrow>\<^isub>1 t'" |
447 |
shows "(\<exists>s1 s2. t' = App s1 s2 \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2) \<or> |
|
448 |
(\<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)" |
|
449 |
using a |
|
450 |
apply - |
|
21366 | 451 |
apply(ind_cases2 "App t1 t2 \<longrightarrow>\<^isub>1 t'") |
18106 | 452 |
apply(auto simp add: lam.distinct lam.inject) |
453 |
done |
|
454 |
||
455 |
lemma one_red: |
|
21101 | 456 |
assumes a: "App (Lam [a].t1) t2 \<longrightarrow>\<^isub>1 M" |
457 |
shows "(\<exists>s1 s2. M = App (Lam [a].s1) s2 \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2) \<or> |
|
458 |
(\<exists>s1 s2. M = s1[a::=s2] \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2)" |
|
459 |
using a |
|
460 |
apply - |
|
21366 | 461 |
apply(ind_cases2 "App (Lam [a].t1) t2 \<longrightarrow>\<^isub>1 M") |
18106 | 462 |
apply(simp_all add: lam.inject) |
463 |
apply(force) |
|
464 |
apply(erule conjE) |
|
465 |
apply(drule sym[of "Lam [a].t1"]) |
|
466 |
apply(simp) |
|
467 |
apply(drule one_abs) |
|
468 |
apply(erule exE) |
|
469 |
apply(simp) |
|
470 |
apply(force simp add: alpha) |
|
471 |
apply(erule conjE) |
|
472 |
apply(simp add: lam.inject alpha) |
|
473 |
apply(erule disjE) |
|
474 |
apply(simp) |
|
475 |
apply(force) |
|
476 |
apply(simp) |
|
477 |
apply(rule disjI2) |
|
478 |
apply(rule_tac x="[(a,aa)]\<bullet>t2a" in exI) |
|
479 |
apply(rule_tac x="s2" in exI) |
|
480 |
apply(auto) |
|
481 |
apply(subgoal_tac "a\<sharp>t2a")(*A*) |
|
482 |
apply(simp add: subst_rename) |
|
483 |
(*A*) |
|
484 |
apply(force intro: one_fresh_preserv) |
|
485 |
apply(force intro: eqvt_one) |
|
486 |
done |
|
487 |
||
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
488 |
text {* first case in Lemma 3.2.4*} |
18106 | 489 |
|
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
490 |
lemma one_subst_aux: |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
491 |
assumes a: "N\<longrightarrow>\<^isub>1N'" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
492 |
shows "M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
493 |
using a |
18659
2ff0ae57431d
changes to make use of the new induction principle proved by
urbanc
parents:
18378
diff
changeset
|
494 |
proof (nominal_induct M avoiding: x N N' rule: lam.induct) |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
495 |
case (Var y) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
496 |
show "Var y[x::=N] \<longrightarrow>\<^isub>1 Var y[x::=N']" by (cases "x=y", auto) |
18106 | 497 |
next |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
498 |
case (App P Q) (* application case - third line *) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
499 |
thus "(App P Q)[x::=N] \<longrightarrow>\<^isub>1 (App P Q)[x::=N']" using o2 by simp |
18106 | 500 |
next |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
501 |
case (Lam y P) (* abstraction case - fourth line *) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
502 |
thus "(Lam [y].P)[x::=N] \<longrightarrow>\<^isub>1 (Lam [y].P)[x::=N']" using o3 by simp |
18106 | 503 |
qed |
504 |
||
18378 | 505 |
lemma one_subst_aux_automatic: |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
506 |
assumes a: "N\<longrightarrow>\<^isub>1N'" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
507 |
shows "M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
508 |
using a |
18659
2ff0ae57431d
changes to make use of the new induction principle proved by
urbanc
parents:
18378
diff
changeset
|
509 |
apply(nominal_induct M avoiding: x N N' rule: lam.induct) |
18106 | 510 |
apply(auto simp add: fresh_prod fresh_atm) |
511 |
done |
|
512 |
||
18312
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
513 |
lemma one_subst: |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
514 |
assumes a: "M\<longrightarrow>\<^isub>1M'" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
515 |
and b: "N\<longrightarrow>\<^isub>1N'" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
516 |
shows "M[x::=N]\<longrightarrow>\<^isub>1M'[x::=N']" |
18773
0eabf66582d0
the additional freshness-condition in the one-induction
urbanc
parents:
18659
diff
changeset
|
517 |
using a b |
18312
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
518 |
proof (nominal_induct M M' avoiding: N N' x rule: one_induct) |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
519 |
case (o1 M) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
520 |
thus ?case by (simp add: one_subst_aux) |
18106 | 521 |
next |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
522 |
case (o2 M1 M2 N1 N2) |
18106 | 523 |
thus ?case by simp |
524 |
next |
|
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
525 |
case (o3 a M1 M2) |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
526 |
thus ?case by simp |
18106 | 527 |
next |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
528 |
case (o4 a M1 M2 N1 N2) |
18773
0eabf66582d0
the additional freshness-condition in the one-induction
urbanc
parents:
18659
diff
changeset
|
529 |
have e3: "a\<sharp>N" "a\<sharp>N'" "a\<sharp>x" by fact |
18106 | 530 |
show ?case |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
531 |
proof - |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
532 |
have "(App (Lam [a].M1) N1)[x::=N] = App (Lam [a].(M1[x::=N])) (N1[x::=N])" using e3 by simp |
21143
56695d1f45cf
changed a misplaced "also" to a "moreover" (caused a loop somehow)
urbanc
parents:
21138
diff
changeset
|
533 |
moreover have "App (Lam [a].(M1[x::=N])) (N1[x::=N]) \<longrightarrow>\<^isub>1 M2[x::=N'][a::=N2[x::=N']]" |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
534 |
using o4 b by force |
21143
56695d1f45cf
changed a misplaced "also" to a "moreover" (caused a loop somehow)
urbanc
parents:
21138
diff
changeset
|
535 |
moreover have "M2[x::=N'][a::=N2[x::=N']] = M2[a::=N2][x::=N']" |
20955
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
536 |
using e3 by (simp add: substitution_lemma fresh_atm) |
18106 | 537 |
ultimately show "(App (Lam [a].M1) N1)[x::=N] \<longrightarrow>\<^isub>1 M2[a::=N2][x::=N']" by simp |
538 |
qed |
|
539 |
qed |
|
540 |
||
18378 | 541 |
lemma one_subst_automatic: |
18106 | 542 |
assumes a: "M\<longrightarrow>\<^isub>1M'" |
18303
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
543 |
and b: "N\<longrightarrow>\<^isub>1N'" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
544 |
shows "M[x::=N]\<longrightarrow>\<^isub>1M'[x::=N']" |
b18fabea0fd0
modified almost everything for the new nominal_induct
urbanc
parents:
18269
diff
changeset
|
545 |
using a b |
18312
c68296902ddb
cleaned up further the proofs (diamond still needs work);
urbanc
parents:
18303
diff
changeset
|
546 |
apply(nominal_induct M M' avoiding: N N' x rule: one_induct) |
20955
65a9a30b8ece
made some proof look more like the ones in Barendregt
urbanc
parents:
20503
diff
changeset
|
547 |
apply(auto simp add: one_subst_aux substitution_lemma fresh_atm) |
18106 | 548 |
done |
549 |
||
550 |
lemma diamond[rule_format]: |
|
551 |
fixes M :: "lam" |
|
552 |
and M1:: "lam" |
|
553 |
assumes a: "M\<longrightarrow>\<^isub>1M1" |
|
18344 | 554 |
and b: "M\<longrightarrow>\<^isub>1M2" |
555 |
shows "\<exists>M3. M1\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" |
|
556 |
using a b |
|
20503 | 557 |
proof (induct arbitrary: M2) |
18106 | 558 |
case (o1 M) (* case 1 --- M1 = M *) |
18344 | 559 |
thus "\<exists>M3. M\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" by blast |
18106 | 560 |
next |
21101 | 561 |
case (o4 Q Q' P P' x) (* case 2 --- a beta-reduction occurs*) |
18344 | 562 |
have i1: "\<And>M2. Q \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact |
563 |
have i2: "\<And>M2. P \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact |
|
564 |
have "App (Lam [x].P) Q \<longrightarrow>\<^isub>1 M2" by fact |
|
565 |
hence "(\<exists>P' Q'. M2 = App (Lam [x].P') Q' \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q') \<or> |
|
566 |
(\<exists>P' Q'. M2 = P'[x::=Q'] \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q')" by (simp add: one_red) |
|
567 |
moreover (* subcase 2.1 *) |
|
568 |
{ assume "\<exists>P' Q'. M2 = App (Lam [x].P') Q' \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q'" |
|
569 |
then obtain P'' and Q'' where |
|
570 |
b1: "M2=App (Lam [x].P'') Q''" and b2: "P\<longrightarrow>\<^isub>1P''" and b3: "Q\<longrightarrow>\<^isub>1Q''" by blast |
|
571 |
from b2 i2 have "(\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> P''\<longrightarrow>\<^isub>1M3)" by simp |
|
572 |
then obtain P''' where |
|
573 |
c1: "P'\<longrightarrow>\<^isub>1P'''" and c2: "P''\<longrightarrow>\<^isub>1P'''" by force |
|
574 |
from b3 i1 have "(\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> Q''\<longrightarrow>\<^isub>1M3)" by simp |
|
575 |
then obtain Q''' where |
|
576 |
d1: "Q'\<longrightarrow>\<^isub>1Q'''" and d2: "Q''\<longrightarrow>\<^isub>1Q'''" by force |
|
577 |
from c1 c2 d1 d2 |
|
578 |
have "P'[x::=Q']\<longrightarrow>\<^isub>1P'''[x::=Q'''] \<and> App (Lam [x].P'') Q'' \<longrightarrow>\<^isub>1 P'''[x::=Q''']" |
|
579 |
by (force simp add: one_subst) |
|
580 |
hence "\<exists>M3. P'[x::=Q']\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 by blast |
|
581 |
} |
|
582 |
moreover (* subcase 2.2 *) |
|
583 |
{ assume "\<exists>P' Q'. M2 = P'[x::=Q'] \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q'" |
|
584 |
then obtain P'' Q'' where |
|
585 |
b1: "M2=P''[x::=Q'']" and b2: "P\<longrightarrow>\<^isub>1P''" and b3: "Q\<longrightarrow>\<^isub>1Q''" by blast |
|
586 |
from b2 i2 have "(\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> P''\<longrightarrow>\<^isub>1M3)" by simp |
|
587 |
then obtain P''' where |
|
588 |
c1: "P'\<longrightarrow>\<^isub>1P'''" and c2: "P''\<longrightarrow>\<^isub>1P'''" by blast |
|
589 |
from b3 i1 have "(\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> Q''\<longrightarrow>\<^isub>1M3)" by simp |
|
590 |
then obtain Q''' where |
|
591 |
d1: "Q'\<longrightarrow>\<^isub>1Q'''" and d2: "Q''\<longrightarrow>\<^isub>1Q'''" by blast |
|
592 |
from c1 c2 d1 d2 |
|
593 |
have "P'[x::=Q']\<longrightarrow>\<^isub>1P'''[x::=Q'''] \<and> P''[x::=Q'']\<longrightarrow>\<^isub>1P'''[x::=Q''']" |
|
594 |
by (force simp add: one_subst) |
|
595 |
hence "\<exists>M3. P'[x::=Q']\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 by blast |
|
596 |
} |
|
597 |
ultimately show "\<exists>M3. P'[x::=Q']\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" by blast |
|
18106 | 598 |
next |
21101 | 599 |
case (o2 P P' Q Q') (* case 3 *) |
18344 | 600 |
have i0: "P\<longrightarrow>\<^isub>1P'" by fact |
601 |
have i1: "\<And>M2. Q \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact |
|
602 |
have i2: "\<And>M2. P \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact |
|
603 |
assume "App P Q \<longrightarrow>\<^isub>1 M2" |
|
604 |
hence "(\<exists>P'' Q''. M2 = App P'' Q'' \<and> P\<longrightarrow>\<^isub>1P'' \<and> Q\<longrightarrow>\<^isub>1Q'') \<or> |
|
605 |
(\<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')" |
|
606 |
by (simp add: one_app[simplified]) |
|
607 |
moreover (* subcase 3.1 *) |
|
608 |
{ assume "\<exists>P'' Q''. M2 = App P'' Q'' \<and> P\<longrightarrow>\<^isub>1P'' \<and> Q\<longrightarrow>\<^isub>1Q''" |
|
609 |
then obtain P'' and Q'' where |
|
610 |
b1: "M2=App P'' Q''" and b2: "P\<longrightarrow>\<^isub>1P''" and b3: "Q\<longrightarrow>\<^isub>1Q''" by blast |
|
611 |
from b2 i2 have "(\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> P''\<longrightarrow>\<^isub>1M3)" by simp |
|
612 |
then obtain P''' where |
|
613 |
c1: "P'\<longrightarrow>\<^isub>1P'''" and c2: "P''\<longrightarrow>\<^isub>1P'''" by blast |
|
614 |
from b3 i1 have "\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> Q''\<longrightarrow>\<^isub>1M3" by simp |
|
615 |
then obtain Q''' where |
|
616 |
d1: "Q'\<longrightarrow>\<^isub>1Q'''" and d2: "Q''\<longrightarrow>\<^isub>1Q'''" by blast |
|
617 |
from c1 c2 d1 d2 |
|
618 |
have "App P' Q'\<longrightarrow>\<^isub>1App P''' Q''' \<and> App P'' Q'' \<longrightarrow>\<^isub>1 App P''' Q'''" by blast |
|
619 |
hence "\<exists>M3. App P' Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 by blast |
|
620 |
} |
|
621 |
moreover (* subcase 3.2 *) |
|
622 |
{ 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''" |
|
623 |
then obtain x P1 P1'' Q'' where |
|
624 |
b0: "P=Lam [x].P1" and b1: "M2=P1''[x::=Q'']" and |
|
625 |
b2: "P1\<longrightarrow>\<^isub>1P1''" and b3: "Q\<longrightarrow>\<^isub>1Q''" by blast |
|
626 |
from b0 i0 have "\<exists>P1'. P'=Lam [x].P1' \<and> P1\<longrightarrow>\<^isub>1P1'" by (simp add: one_abs) |
|
627 |
then obtain P1' where g1: "P'=Lam [x].P1'" and g2: "P1\<longrightarrow>\<^isub>1P1'" by blast |
|
628 |
from g1 b0 b2 i2 have "(\<exists>M3. (Lam [x].P1')\<longrightarrow>\<^isub>1M3 \<and> (Lam [x].P1'')\<longrightarrow>\<^isub>1M3)" by simp |
|
629 |
then obtain P1''' where |
|
630 |
c1: "(Lam [x].P1')\<longrightarrow>\<^isub>1P1'''" and c2: "(Lam [x].P1'')\<longrightarrow>\<^isub>1P1'''" by blast |
|
631 |
from c1 have "\<exists>R1. P1'''=Lam [x].R1 \<and> P1'\<longrightarrow>\<^isub>1R1" by (simp add: one_abs) |
|
632 |
then obtain R1 where r1: "P1'''=Lam [x].R1" and r2: "P1'\<longrightarrow>\<^isub>1R1" by blast |
|
633 |
from c2 have "\<exists>R2. P1'''=Lam [x].R2 \<and> P1''\<longrightarrow>\<^isub>1R2" by (simp add: one_abs) |
|
634 |
then obtain R2 where r3: "P1'''=Lam [x].R2" and r4: "P1''\<longrightarrow>\<^isub>1R2" by blast |
|
635 |
from r1 r3 have r5: "R1=R2" by (simp add: lam.inject alpha) |
|
636 |
from b3 i1 have "(\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> Q''\<longrightarrow>\<^isub>1M3)" by simp |
|
637 |
then obtain Q''' where |
|
638 |
d1: "Q'\<longrightarrow>\<^isub>1Q'''" and d2: "Q''\<longrightarrow>\<^isub>1Q'''" by blast |
|
639 |
from g1 r2 d1 r4 r5 d2 |
|
640 |
have "App P' Q'\<longrightarrow>\<^isub>1R1[x::=Q'''] \<and> P1''[x::=Q'']\<longrightarrow>\<^isub>1R1[x::=Q''']" by (simp add: one_subst) |
|
641 |
hence "\<exists>M3. App P' Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 by blast |
|
642 |
} |
|
643 |
ultimately show "\<exists>M3. App P' Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" by blast |
|
18106 | 644 |
next |
21101 | 645 |
case (o3 P P' x) (* case 4 *) |
18344 | 646 |
have i1: "P\<longrightarrow>\<^isub>1P'" by fact |
647 |
have i2: "\<And>M2. P \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact |
|
648 |
have "(Lam [x].P)\<longrightarrow>\<^isub>1 M2" by fact |
|
649 |
hence "\<exists>P''. M2=Lam [x].P'' \<and> P\<longrightarrow>\<^isub>1P''" by (simp add: one_abs) |
|
650 |
then obtain P'' where b1: "M2=Lam [x].P''" and b2: "P\<longrightarrow>\<^isub>1P''" by blast |
|
651 |
from i2 b1 b2 have "\<exists>M3. (Lam [x].P')\<longrightarrow>\<^isub>1M3 \<and> (Lam [x].P'')\<longrightarrow>\<^isub>1M3" by blast |
|
652 |
then obtain M3 where c1: "(Lam [x].P')\<longrightarrow>\<^isub>1M3" and c2: "(Lam [x].P'')\<longrightarrow>\<^isub>1M3" by blast |
|
653 |
from c1 have "\<exists>R1. M3=Lam [x].R1 \<and> P'\<longrightarrow>\<^isub>1R1" by (simp add: one_abs) |
|
654 |
then obtain R1 where r1: "M3=Lam [x].R1" and r2: "P'\<longrightarrow>\<^isub>1R1" by blast |
|
655 |
from c2 have "\<exists>R2. M3=Lam [x].R2 \<and> P''\<longrightarrow>\<^isub>1R2" by (simp add: one_abs) |
|
656 |
then obtain R2 where r3: "M3=Lam [x].R2" and r4: "P''\<longrightarrow>\<^isub>1R2" by blast |
|
657 |
from r1 r3 have r5: "R1=R2" by (simp add: lam.inject alpha) |
|
658 |
from r2 r4 have "(Lam [x].P')\<longrightarrow>\<^isub>1(Lam [x].R1) \<and> (Lam [x].P'')\<longrightarrow>\<^isub>1(Lam [x].R2)" |
|
659 |
by (simp add: one_subst) |
|
660 |
thus "\<exists>M3. (Lam [x].P')\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 r5 by blast |
|
18106 | 661 |
qed |
662 |
||
18882
454d09651d1a
- renamed some lemmas (some had names coming from ancient
urbanc
parents:
18773
diff
changeset
|
663 |
lemma one_lam_cong: |
18106 | 664 |
assumes a: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" |
665 |
shows "(Lam [a].t1)\<longrightarrow>\<^isub>\<beta>\<^sup>*(Lam [a].t2)" |
|
666 |
using a |
|
667 |
proof induct |
|
21101 | 668 |
case bs1 thus ?case by simp |
18106 | 669 |
next |
21101 | 670 |
case (bs2 y z) |
671 |
thus ?case by (blast dest: b3) |
|
18106 | 672 |
qed |
673 |
||
18378 | 674 |
lemma one_app_congL: |
18106 | 675 |
assumes a: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" |
676 |
shows "App t1 s\<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s" |
|
677 |
using a |
|
678 |
proof induct |
|
21101 | 679 |
case bs1 thus ?case by simp |
18106 | 680 |
next |
21101 | 681 |
case bs2 thus ?case by (blast dest: b1) |
18106 | 682 |
qed |
683 |
||
18378 | 684 |
lemma one_app_congR: |
18106 | 685 |
assumes a: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" |
686 |
shows "App s t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App s t2" |
|
687 |
using a |
|
688 |
proof induct |
|
21101 | 689 |
case bs1 thus ?case by simp |
18106 | 690 |
next |
21101 | 691 |
case bs2 thus ?case by (blast dest: b2) |
18106 | 692 |
qed |
693 |
||
18378 | 694 |
lemma one_app_cong: |
18106 | 695 |
assumes a1: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" |
21101 | 696 |
and a2: "s1\<longrightarrow>\<^isub>\<beta>\<^sup>*s2" |
18106 | 697 |
shows "App t1 s1\<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s2" |
698 |
proof - |
|
18378 | 699 |
have "App t1 s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s1" using a1 by (rule one_app_congL) |
700 |
moreover |
|
701 |
have "App t2 s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s2" using a2 by (rule one_app_congR) |
|
21101 | 702 |
ultimately show ?thesis by (rule beta_star_trans) |
18106 | 703 |
qed |
704 |
||
705 |
lemma one_beta_star: |
|
706 |
assumes a: "(t1\<longrightarrow>\<^isub>1t2)" |
|
707 |
shows "(t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2)" |
|
708 |
using a |
|
709 |
proof induct |
|
18378 | 710 |
case o1 thus ?case by simp |
18106 | 711 |
next |
18378 | 712 |
case o2 thus ?case by (blast intro!: one_app_cong) |
18106 | 713 |
next |
18882
454d09651d1a
- renamed some lemmas (some had names coming from ancient
urbanc
parents:
18773
diff
changeset
|
714 |
case o3 thus ?case by (blast intro!: one_lam_cong) |
18106 | 715 |
next |
21101 | 716 |
case (o4 s1 s2 t1 t2 a) |
18378 | 717 |
have a1: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" and a2: "s1\<longrightarrow>\<^isub>\<beta>\<^sup>*s2" by fact |
18106 | 718 |
have c1: "(App (Lam [a].t2) s2) \<longrightarrow>\<^isub>\<beta> (t2 [a::= s2])" by (rule b4) |
719 |
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
|
720 |
by (blast intro!: one_app_cong one_lam_cong) |
21101 | 721 |
show ?case using c2 c1 by (blast intro: beta_star_trans) |
18106 | 722 |
qed |
723 |
||
18882
454d09651d1a
- renamed some lemmas (some had names coming from ancient
urbanc
parents:
18773
diff
changeset
|
724 |
lemma one_star_lam_cong: |
18106 | 725 |
assumes a: "t1\<longrightarrow>\<^isub>1\<^sup>*t2" |
726 |
shows "(Lam [a].t1)\<longrightarrow>\<^isub>1\<^sup>* (Lam [a].t2)" |
|
727 |
using a |
|
728 |
proof induct |
|
21101 | 729 |
case os1 thus ?case by simp |
18106 | 730 |
next |
21101 | 731 |
case os2 thus ?case by (blast intro: one_star_trans) |
18106 | 732 |
qed |
733 |
||
18882
454d09651d1a
- renamed some lemmas (some had names coming from ancient
urbanc
parents:
18773
diff
changeset
|
734 |
lemma one_star_app_congL: |
18106 | 735 |
assumes a: "t1\<longrightarrow>\<^isub>1\<^sup>*t2" |
736 |
shows "App t1 s\<longrightarrow>\<^isub>1\<^sup>* App t2 s" |
|
737 |
using a |
|
738 |
proof induct |
|
21101 | 739 |
case os1 thus ?case by simp |
18106 | 740 |
next |
21101 | 741 |
case os2 thus ?case by (blast intro: one_star_trans) |
18106 | 742 |
qed |
743 |
||
18882
454d09651d1a
- renamed some lemmas (some had names coming from ancient
urbanc
parents:
18773
diff
changeset
|
744 |
lemma one_star_app_congR: |
18106 | 745 |
assumes a: "t1\<longrightarrow>\<^isub>1\<^sup>*t2" |
746 |
shows "App s t1 \<longrightarrow>\<^isub>1\<^sup>* App s t2" |
|
747 |
using a |
|
748 |
proof induct |
|
21101 | 749 |
case os1 thus ?case by simp |
18106 | 750 |
next |
21101 | 751 |
case os2 thus ?case by (blast intro: one_star_trans) |
18106 | 752 |
qed |
753 |
||
754 |
lemma beta_one_star: |
|
755 |
assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2" |
|
756 |
shows "t1\<longrightarrow>\<^isub>1\<^sup>*t2" |
|
757 |
using a |
|
758 |
proof induct |
|
18882
454d09651d1a
- renamed some lemmas (some had names coming from ancient
urbanc
parents:
18773
diff
changeset
|
759 |
case b1 thus ?case by (blast intro!: one_star_app_congL) |
18106 | 760 |
next |
18882
454d09651d1a
- renamed some lemmas (some had names coming from ancient
urbanc
parents:
18773
diff
changeset
|
761 |
case b2 thus ?case by (blast intro!: one_star_app_congR) |
18106 | 762 |
next |
18882
454d09651d1a
- renamed some lemmas (some had names coming from ancient
urbanc
parents:
18773
diff
changeset
|
763 |
case b3 thus ?case by (blast intro!: one_star_lam_cong) |
18106 | 764 |
next |
18378 | 765 |
case b4 thus ?case by blast |
18106 | 766 |
qed |
767 |
||
768 |
lemma trans_closure: |
|
21101 | 769 |
shows "(M1\<longrightarrow>\<^isub>1\<^sup>*M2) = (M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M2)" |
18106 | 770 |
proof |
21101 | 771 |
assume "M1 \<longrightarrow>\<^isub>1\<^sup>* M2" |
772 |
then show "M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M2" |
|
18106 | 773 |
proof induct |
21101 | 774 |
case (os1 M1) thus "M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M1" by simp |
18106 | 775 |
next |
21101 | 776 |
case (os2 M1 M2 M3) |
777 |
have "M2\<longrightarrow>\<^isub>1M3" by fact |
|
778 |
then have "M2\<longrightarrow>\<^isub>\<beta>\<^sup>*M3" by (rule one_beta_star) |
|
779 |
moreover have "M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M2" by fact |
|
780 |
ultimately show "M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M3" by (auto intro: beta_star_trans) |
|
18106 | 781 |
qed |
782 |
next |
|
21101 | 783 |
assume "M1 \<longrightarrow>\<^isub>\<beta>\<^sup>* M2" |
784 |
then show "M1\<longrightarrow>\<^isub>1\<^sup>*M2" |
|
18106 | 785 |
proof induct |
21101 | 786 |
case (bs1 M1) thus "M1\<longrightarrow>\<^isub>1\<^sup>*M1" by simp |
18106 | 787 |
next |
21101 | 788 |
case (bs2 M1 M2 M3) |
789 |
have "M2\<longrightarrow>\<^isub>\<beta>M3" by fact |
|
790 |
then have "M2\<longrightarrow>\<^isub>1\<^sup>*M3" by (rule beta_one_star) |
|
791 |
moreover have "M1\<longrightarrow>\<^isub>1\<^sup>*M2" by fact |
|
792 |
ultimately show "M1\<longrightarrow>\<^isub>1\<^sup>*M3" by (auto intro: one_star_trans) |
|
18106 | 793 |
qed |
794 |
qed |
|
795 |
||
796 |
lemma cr_one: |
|
797 |
assumes a: "t\<longrightarrow>\<^isub>1\<^sup>*t1" |
|
18344 | 798 |
and b: "t\<longrightarrow>\<^isub>1t2" |
18106 | 799 |
shows "\<exists>t3. t1\<longrightarrow>\<^isub>1t3 \<and> t2\<longrightarrow>\<^isub>1\<^sup>*t3" |
18344 | 800 |
using a b |
20503 | 801 |
proof (induct arbitrary: t2) |
21101 | 802 |
case os1 thus ?case by force |
18344 | 803 |
next |
21101 | 804 |
case (os2 t s1 s2 t2) |
18344 | 805 |
have b: "s1 \<longrightarrow>\<^isub>1 s2" by fact |
806 |
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 |
|
807 |
have c: "t \<longrightarrow>\<^isub>1 t2" by fact |
|
18378 | 808 |
show "\<exists>t3. s2 \<longrightarrow>\<^isub>1 t3 \<and> t2 \<longrightarrow>\<^isub>1\<^sup>* t3" |
18344 | 809 |
proof - |
18378 | 810 |
from c h have "\<exists>t3. s1 \<longrightarrow>\<^isub>1 t3 \<and> t2 \<longrightarrow>\<^isub>1\<^sup>* t3" by blast |
811 |
then obtain t3 where c1: "s1 \<longrightarrow>\<^isub>1 t3" and c2: "t2 \<longrightarrow>\<^isub>1\<^sup>* t3" by blast |
|
812 |
have "\<exists>t4. s2 \<longrightarrow>\<^isub>1 t4 \<and> t3 \<longrightarrow>\<^isub>1 t4" using b c1 by (blast intro: diamond) |
|
21101 | 813 |
thus ?thesis using c2 by (blast intro: one_star_trans) |
18106 | 814 |
qed |
815 |
qed |
|
816 |
||
817 |
lemma cr_one_star: |
|
818 |
assumes a: "t\<longrightarrow>\<^isub>1\<^sup>*t2" |
|
819 |
and b: "t\<longrightarrow>\<^isub>1\<^sup>*t1" |
|
18378 | 820 |
shows "\<exists>t3. t1\<longrightarrow>\<^isub>1\<^sup>*t3\<and>t2\<longrightarrow>\<^isub>1\<^sup>*t3" |
21101 | 821 |
using a b |
822 |
proof (induct arbitrary: t1) |
|
823 |
case (os1 t) then show ?case by force |
|
18106 | 824 |
next |
21101 | 825 |
case (os2 t s1 s2 t1) |
826 |
have c: "t \<longrightarrow>\<^isub>1\<^sup>* s1" by fact |
|
827 |
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
|
828 |
have d: "s1 \<longrightarrow>\<^isub>1 s2" by fact |
21101 | 829 |
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 | 830 |
then obtain t3 where f1: "t1 \<longrightarrow>\<^isub>1\<^sup>* t3" |
21101 | 831 |
and f2: "s1 \<longrightarrow>\<^isub>1\<^sup>* t3" using c' by blast |
18378 | 832 |
from cr_one d f2 have "\<exists>t4. t3\<longrightarrow>\<^isub>1t4 \<and> s2\<longrightarrow>\<^isub>1\<^sup>*t4" by blast |
18106 | 833 |
then obtain t4 where g1: "t3\<longrightarrow>\<^isub>1t4" |
18378 | 834 |
and g2: "s2\<longrightarrow>\<^isub>1\<^sup>*t4" by blast |
21101 | 835 |
have "t1\<longrightarrow>\<^isub>1\<^sup>*t4" using f1 g1 by (blast intro: one_star_trans) |
18378 | 836 |
thus ?case using g2 by blast |
18106 | 837 |
qed |
838 |
||
839 |
lemma cr_beta_star: |
|
840 |
assumes a1: "t\<longrightarrow>\<^isub>\<beta>\<^sup>*t1" |
|
18882
454d09651d1a
- renamed some lemmas (some had names coming from ancient
urbanc
parents:
18773
diff
changeset
|
841 |
and a2: "t\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" |
18378 | 842 |
shows "\<exists>t3. t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t3\<and>t2\<longrightarrow>\<^isub>\<beta>\<^sup>*t3" |
18106 | 843 |
proof - |
18882
454d09651d1a
- renamed some lemmas (some had names coming from ancient
urbanc
parents:
18773
diff
changeset
|
844 |
from a1 have "t\<longrightarrow>\<^isub>1\<^sup>*t1" by (simp only: trans_closure) |
18378 | 845 |
moreover |
18882
454d09651d1a
- renamed some lemmas (some had names coming from ancient
urbanc
parents:
18773
diff
changeset
|
846 |
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
|
847 |
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
|
848 |
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
|
849 |
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
|
850 |
then show "\<exists>t3. t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t3\<and>t2\<longrightarrow>\<^isub>\<beta>\<^sup>*t3" by blast |
18106 | 851 |
qed |
852 |
||
853 |
end |
|
854 |