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