author | urbanc |
Fri, 02 Feb 2007 17:16:16 +0100 | |
changeset 22231 | f76f187c91f9 |
parent 22082 | b1be13d32efd |
child 22418 | 49e2d9744ae1 |
permissions | -rw-r--r-- |
22073 | 1 |
(* "$Id$" *) |
2 |
(* *) |
|
22082 | 3 |
(* Formalisation of the chapter on Logical Relations *) |
4 |
(* and a Case Study in Equivalence Checking *) |
|
5 |
(* by Karl Crary from the book on Advanced Topics in *) |
|
6 |
(* Types and Programming Languages, MIT Press 2005 *) |
|
7 |
||
8 |
(* The formalisation was done by Julien Narboux and *) |
|
9 |
(* Christian Urban *) |
|
22073 | 10 |
|
11 |
theory Crary |
|
12 |
imports "Nominal" |
|
13 |
begin |
|
14 |
||
15 |
atom_decl name |
|
16 |
||
17 |
nominal_datatype ty = TBase |
|
18 |
| TUnit |
|
19 |
| Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100) |
|
20 |
||
21 |
nominal_datatype trm = Unit |
|
22 |
| Var "name" |
|
23 |
| Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100) |
|
24 |
| App "trm" "trm" |
|
25 |
| Const "nat" |
|
26 |
||
22082 | 27 |
(* The next 3 lemmas should be in the nominal library *) |
22073 | 28 |
lemma eq_eqvt: |
29 |
fixes pi::"name prm" |
|
30 |
and x::"'a::pt_name" |
|
31 |
shows "pi\<bullet>(x=y) = (pi\<bullet>x=pi\<bullet>y)" |
|
32 |
apply(simp add: perm_bool perm_bij) |
|
33 |
done |
|
34 |
||
35 |
lemma in_eqvt: |
|
36 |
fixes pi::"name prm" |
|
37 |
and x::"'a::pt_name" |
|
38 |
assumes "x\<in>X" |
|
39 |
shows "pi\<bullet>x \<in> pi\<bullet>X" |
|
40 |
using assms by (perm_simp add: pt_set_bij1a[OF pt_name_inst, OF at_name_inst]) |
|
41 |
||
42 |
lemma set_eqvt: |
|
43 |
fixes pi::"name prm" |
|
44 |
and xs::"('a::pt_name) list" |
|
45 |
shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)" |
|
46 |
by (perm_simp add: pt_list_set_pi[OF pt_name_inst]) |
|
22082 | 47 |
(* end of library *) |
22073 | 48 |
|
49 |
lemma perm_ty[simp]: |
|
50 |
fixes T::"ty" |
|
51 |
and pi::"name prm" |
|
52 |
shows "pi\<bullet>T = T" |
|
53 |
by (induct T rule: ty.induct_weak) (simp_all) |
|
54 |
||
55 |
lemma fresh_ty[simp]: |
|
56 |
fixes x::"name" |
|
57 |
and T::"ty" |
|
58 |
shows "x\<sharp>T" |
|
59 |
by (simp add: fresh_def supp_def) |
|
60 |
||
61 |
lemma ty_cases: |
|
62 |
fixes T::ty |
|
63 |
shows "(\<exists> T1 T2. T=T1\<rightarrow>T2) \<or> T=TUnit \<or> T=TBase" |
|
22082 | 64 |
by (induct T rule:ty.induct_weak) (auto) |
22073 | 65 |
|
66 |
text {* Size Functions *} |
|
67 |
||
68 |
instance ty :: size .. |
|
69 |
||
70 |
nominal_primrec |
|
71 |
"size (TBase) = 1" |
|
72 |
"size (TUnit) = 1" |
|
73 |
"size (T1\<rightarrow>T2) = size T1 + size T2" |
|
74 |
by (rule TrueI)+ |
|
75 |
||
76 |
instance trm :: size .. |
|
77 |
||
78 |
nominal_primrec |
|
79 |
"size (Unit) = 1" |
|
80 |
"size (Var x) = 1" |
|
81 |
"size (Lam [x].t) = size t + 1" |
|
82 |
"size (App t1 t2) = size t1 + size t2" |
|
83 |
"size (Const n) = 1" |
|
84 |
apply(finite_guess add: fs_name1 perm_nat_def)+ |
|
85 |
apply(perm_full_simp add: perm_nat_def) |
|
86 |
apply(simp add: fs_name1) |
|
87 |
apply(rule TrueI)+ |
|
88 |
apply(simp add: fresh_nat)+ |
|
89 |
apply(fresh_guess add: fs_name1 perm_nat_def)+ |
|
90 |
done |
|
91 |
||
92 |
lemma ty_size_greater_zero[simp]: |
|
93 |
fixes T::"ty" |
|
94 |
shows "size T > 0" |
|
95 |
by (nominal_induct rule:ty.induct) (simp_all) |
|
96 |
||
97 |
text {* valid contexts *} |
|
98 |
||
99 |
inductive2 |
|
100 |
valid :: "(name \<times> 'a::pt_name) list \<Rightarrow> bool" |
|
101 |
where |
|
22082 | 102 |
v_nil[intro]: "valid []" |
22073 | 103 |
| v_cons[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)" |
104 |
||
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
105 |
lemma valid_eqvt[eqvt]: |
22073 | 106 |
fixes pi:: "name prm" |
107 |
assumes a: "valid \<Gamma>" |
|
108 |
shows "valid (pi\<bullet>\<Gamma>)" |
|
109 |
using a |
|
110 |
by (induct) (auto simp add: fresh_bij) |
|
111 |
||
112 |
inductive_cases2 |
|
113 |
valid_cons_elim_auto[elim]:"valid ((x,T)#\<Gamma>)" |
|
114 |
||
22082 | 115 |
text {* typing judgements for terms *} |
22073 | 116 |
|
117 |
inductive2 |
|
118 |
typing :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [60,60,60] 60) |
|
119 |
where |
|
120 |
t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var x : T" |
|
121 |
| t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> e1 : T1\<rightarrow>T2; \<Gamma> \<turnstile> e2 : T1\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App e1 e2 : T2" |
|
122 |
| t_Lam[intro]: "\<lbrakk>x\<sharp>\<Gamma>; (x,T1)#\<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T1\<rightarrow>T2" |
|
123 |
| t_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n : TBase" |
|
124 |
| t_Unit[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Unit : TUnit" |
|
125 |
||
126 |
lemma typing_valid: |
|
127 |
assumes "\<Gamma> \<turnstile> t : T" |
|
128 |
shows "valid \<Gamma>" |
|
129 |
using assms |
|
130 |
by (induct) (auto) |
|
131 |
||
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
132 |
lemma typing_eqvt[eqvt]: |
22073 | 133 |
fixes pi::"name prm" |
134 |
assumes "\<Gamma> \<turnstile> t : T" |
|
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
135 |
shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>t) : (pi\<bullet>T)" |
22073 | 136 |
using assms |
137 |
apply(induct) |
|
138 |
apply(auto simp add: fresh_bij set_eqvt valid_eqvt) |
|
139 |
apply(rule t_Var) |
|
140 |
apply(drule valid_eqvt) |
|
141 |
apply(assumption) |
|
142 |
apply(drule in_eqvt) |
|
143 |
apply(simp add: set_eqvt) |
|
144 |
done |
|
145 |
||
146 |
text {* Inversion lemmas for the typing judgment *} |
|
147 |
||
148 |
declare trm.inject [simp add] |
|
149 |
declare ty.inject [simp add] |
|
150 |
||
151 |
inductive_cases2 t_Lam_elim_auto[elim]: "\<Gamma> \<turnstile> Lam [x].t : T" |
|
152 |
inductive_cases2 t_Var_elim_auto[elim]: "\<Gamma> \<turnstile> Var x : T" |
|
153 |
inductive_cases2 t_App_elim_auto[elim]: "\<Gamma> \<turnstile> App x y : T" |
|
154 |
inductive_cases2 t_Const_elim_auto[elim]: "\<Gamma> \<turnstile> Const n : T" |
|
155 |
inductive_cases2 t_Unit_elim_auto[elim]: "\<Gamma> \<turnstile> Unit : TUnit" |
|
156 |
||
157 |
declare trm.inject [simp del] |
|
158 |
declare ty.inject [simp del] |
|
159 |
||
160 |
lemma typing_induct_strong |
|
161 |
[consumes 1, case_names t_Var t_App t_Lam t_Const t_Unit]: |
|
162 |
fixes P::"'a::fs_name \<Rightarrow> (name\<times>ty) list \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow>bool" |
|
163 |
and x :: "'a::fs_name" |
|
164 |
assumes a: "\<Gamma> \<turnstile> e : T" |
|
165 |
and a1: "\<And>\<Gamma> x T c. \<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> P c \<Gamma> (Var x) T" |
|
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
166 |
and a2: "\<And>\<Gamma> e1 T1 T2 e2 c. \<lbrakk>\<And>c. P c \<Gamma> e1 (T1\<rightarrow>T2); \<And>c. P c \<Gamma> e2 T1\<rbrakk> |
22073 | 167 |
\<Longrightarrow> P c \<Gamma> (App e1 e2) T2" |
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
168 |
and a3: "\<And>x \<Gamma> T1 t T2 c.\<lbrakk>x\<sharp>(\<Gamma>,c); \<And>c. P c ((x,T1)#\<Gamma>) t T2\<rbrakk> |
22073 | 169 |
\<Longrightarrow> P c \<Gamma> (Lam [x].t) (T1\<rightarrow>T2)" |
170 |
and a4: "\<And>\<Gamma> n c. valid \<Gamma> \<Longrightarrow> P c \<Gamma> (Const n) TBase" |
|
171 |
and a5: "\<And>\<Gamma> c. valid \<Gamma> \<Longrightarrow> P c \<Gamma> Unit TUnit" |
|
172 |
shows "P c \<Gamma> e T" |
|
173 |
proof - |
|
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
174 |
from a have "\<And>(pi::name prm) c. P c (pi\<bullet>\<Gamma>) (pi\<bullet>e) (pi\<bullet>T)" |
22073 | 175 |
proof (induct) |
176 |
case (t_Var \<Gamma> x T pi c) |
|
177 |
have "valid \<Gamma>" by fact |
|
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
178 |
then have "valid (pi\<bullet>\<Gamma>)" by (simp only: eqvt) |
22073 | 179 |
moreover |
180 |
have "(x,T)\<in>set \<Gamma>" by fact |
|
181 |
then have "pi\<bullet>(x,T)\<in>pi\<bullet>(set \<Gamma>)" by (simp only: pt_set_bij[OF pt_name_inst, OF at_name_inst]) |
|
182 |
then have "(pi\<bullet>x,T)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: set_eqvt) |
|
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
183 |
ultimately show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(Var x)) (pi\<bullet>T)" using a1 by simp |
22073 | 184 |
next |
185 |
case (t_App \<Gamma> e1 T1 T2 e2 pi c) |
|
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
186 |
thus "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(App e1 e2)) (pi\<bullet>T2)" using a2 |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
187 |
by (simp only: eqvt) (blast) |
22073 | 188 |
next |
189 |
case (t_Lam x \<Gamma> T1 t T2 pi c) |
|
190 |
obtain y::"name" where fs: "y\<sharp>(pi\<bullet>x,pi\<bullet>\<Gamma>,pi\<bullet>t,c)" by (erule exists_fresh[OF fs_name1]) |
|
191 |
let ?sw = "[(pi\<bullet>x,y)]" |
|
192 |
let ?pi' = "?sw@pi" |
|
193 |
have f0: "x\<sharp>\<Gamma>" by fact |
|
194 |
have f1: "(pi\<bullet>x)\<sharp>(pi\<bullet>\<Gamma>)" using f0 by (simp add: fresh_bij) |
|
195 |
have f2: "y\<sharp>?pi'\<bullet>\<Gamma>" by (auto simp add: pt_name2 fresh_left calc_atm perm_pi_simp) |
|
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
196 |
have ih1: "\<And>c. P c (?pi'\<bullet>((x,T1)#\<Gamma>)) (?pi'\<bullet>t) (?pi'\<bullet>T2)" by fact |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
197 |
then have "P c (?pi'\<bullet>\<Gamma>) (Lam [y].(?pi'\<bullet>t)) (T1\<rightarrow>T2)" using fs f2 a3 |
22073 | 198 |
by (simp add: calc_atm) |
199 |
then have "P c (?sw\<bullet>pi\<bullet>\<Gamma>) (?sw\<bullet>(Lam [(pi\<bullet>x)].(pi\<bullet>t))) (T1\<rightarrow>T2)" |
|
200 |
by (simp del: append_Cons add: calc_atm pt_name2) |
|
201 |
moreover have "(?sw\<bullet>pi\<bullet>\<Gamma>) = (pi\<bullet>\<Gamma>)" |
|
202 |
by (rule perm_fresh_fresh) (simp_all add: fs f1) |
|
203 |
moreover have "(?sw\<bullet>(Lam [(pi\<bullet>x)].(pi\<bullet>t))) = Lam [(pi\<bullet>x)].(pi\<bullet>t)" |
|
204 |
by (rule perm_fresh_fresh) (simp_all add: fs f1 fresh_atm abs_fresh) |
|
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
205 |
ultimately show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(Lam [x].t)) (pi\<bullet>T1\<rightarrow>T2)" by simp |
22073 | 206 |
next |
207 |
case (t_Const \<Gamma> n pi c) |
|
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
208 |
thus "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(Const n)) (pi\<bullet>TBase)" using a4 by (simp, blast intro: valid_eqvt) |
22073 | 209 |
next |
210 |
case (t_Unit \<Gamma> pi c) |
|
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
211 |
thus "P c (pi\<bullet>\<Gamma>) (pi\<bullet>Unit) (pi\<bullet>TUnit)" using a5 by (simp, blast intro: valid_eqvt) |
22073 | 212 |
qed |
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
213 |
then have "P c (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>e) (([]::name prm)\<bullet>T)" by blast |
22073 | 214 |
then show "P c \<Gamma> e T" by simp |
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
215 |
qed |
22073 | 216 |
|
217 |
text {* capture-avoiding substitution *} |
|
218 |
||
219 |
fun |
|
220 |
lookup :: "(name\<times>trm) list \<Rightarrow> name \<Rightarrow> trm" |
|
221 |
where |
|
222 |
"lookup [] X = Var X" |
|
223 |
"lookup ((Y,T)#\<theta>) X = (if X=Y then T else lookup \<theta> X)" |
|
224 |
||
225 |
lemma lookup_eqvt: |
|
226 |
fixes pi::"name prm" |
|
227 |
and \<theta>::"(name\<times>trm) list" |
|
228 |
and X::"name" |
|
229 |
shows "pi\<bullet>(lookup \<theta> X) = lookup (pi\<bullet>\<theta>) (pi\<bullet>X)" |
|
230 |
by (induct \<theta>) |
|
231 |
(auto simp add: perm_bij) |
|
232 |
||
233 |
lemma lookup_fresh: |
|
234 |
fixes z::"name" |
|
235 |
assumes "z\<sharp>\<theta>" "z\<sharp>x" |
|
236 |
shows "z \<sharp>lookup \<theta> x" |
|
237 |
using assms |
|
238 |
by (induct rule: lookup.induct) (auto simp add: fresh_list_cons) |
|
239 |
||
240 |
lemma lookup_fresh': |
|
241 |
assumes "z\<sharp>\<theta>" |
|
242 |
shows "lookup \<theta> z = Var z" |
|
243 |
using assms |
|
244 |
by (induct rule: lookup.induct) |
|
245 |
(auto simp add: fresh_list_cons fresh_prod fresh_atm) |
|
246 |
||
247 |
consts |
|
248 |
psubst :: "(name\<times>trm) list \<Rightarrow> trm \<Rightarrow> trm" ("_<_>" [60,100] 100) |
|
249 |
||
250 |
nominal_primrec |
|
251 |
"\<theta><(Var x)> = (lookup \<theta> x)" |
|
252 |
"\<theta><(App t1 t2)> = App (\<theta><t1>) (\<theta><t2>)" |
|
253 |
"x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].t)> = Lam [x].(\<theta><t>)" |
|
254 |
"\<theta><(Const n)> = Const n" |
|
255 |
"\<theta><(Unit)> = Unit" |
|
256 |
apply(finite_guess add: fs_name1 lookup_eqvt)+ |
|
257 |
apply(perm_full_simp) |
|
258 |
apply(simp add: fs_name1) |
|
259 |
apply(rule TrueI)+ |
|
260 |
apply(simp add: abs_fresh)+ |
|
261 |
apply(fresh_guess add: fs_name1 lookup_eqvt)+ |
|
262 |
done |
|
263 |
||
264 |
abbreviation |
|
265 |
subst :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_[_::=_]" [100,100,100] 100) |
|
266 |
where |
|
267 |
"t[x::=t'] \<equiv> ([(x,t')])<t>" |
|
268 |
||
269 |
lemma subst[simp]: |
|
270 |
shows "(Var x)[y::=t'] = (if x=y then t' else (Var x))" |
|
271 |
and "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])" |
|
272 |
and "x\<sharp>(y,t') \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])" |
|
273 |
and "Const n[y::=t'] = Const n" |
|
274 |
and "Unit [y::=t'] = Unit" |
|
275 |
by (simp_all add: fresh_list_cons fresh_list_nil) |
|
276 |
||
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
277 |
lemma subst_eqvt[eqvt]: |
22073 | 278 |
fixes pi::"name prm" |
279 |
and t::"trm" |
|
280 |
shows "pi\<bullet>(t[x::=t']) = (pi\<bullet>t)[(pi\<bullet>x)::=(pi\<bullet>t')]" |
|
281 |
by (nominal_induct t avoiding: x t' rule: trm.induct) |
|
282 |
(perm_simp add: fresh_bij)+ |
|
283 |
||
284 |
lemma subst_rename: |
|
285 |
fixes c::"name" |
|
286 |
and t1::"trm" |
|
287 |
assumes a: "c\<sharp>t1" |
|
288 |
shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]" |
|
289 |
using a |
|
290 |
apply(nominal_induct t1 avoiding: a c t2 rule: trm.induct) |
|
291 |
apply(simp add: trm.inject calc_atm fresh_atm abs_fresh perm_nat_def)+ |
|
292 |
done |
|
293 |
||
294 |
lemma fresh_psubst: |
|
295 |
fixes z::"name" |
|
296 |
and t::"trm" |
|
297 |
assumes "z\<sharp>t" "z\<sharp>\<theta>" |
|
298 |
shows "z\<sharp>(\<theta><t>)" |
|
299 |
using assms |
|
300 |
by (nominal_induct t avoiding: z \<theta> t rule: trm.induct) |
|
301 |
(auto simp add: abs_fresh lookup_fresh) |
|
302 |
||
303 |
lemma fresh_subst'': |
|
304 |
fixes z::"name" |
|
305 |
and t1::"trm" |
|
306 |
and t2::"trm" |
|
307 |
assumes "z\<sharp>t2" |
|
308 |
shows "z\<sharp>t1[z::=t2]" |
|
309 |
using assms |
|
310 |
by (nominal_induct t1 avoiding: t2 z rule: trm.induct) |
|
311 |
(auto simp add: abs_fresh fresh_nat fresh_atm) |
|
312 |
||
313 |
lemma fresh_subst': |
|
314 |
fixes z::"name" |
|
315 |
and t1::"trm" |
|
316 |
and t2::"trm" |
|
317 |
assumes "z\<sharp>[y].t1" "z\<sharp>t2" |
|
318 |
shows "z\<sharp>t1[y::=t2]" |
|
319 |
using assms |
|
320 |
by (nominal_induct t1 avoiding: y t2 z rule: trm.induct) |
|
321 |
(auto simp add: abs_fresh fresh_nat fresh_atm) |
|
322 |
||
323 |
lemma fresh_subst: |
|
324 |
fixes z::"name" |
|
325 |
and t1::"trm" |
|
326 |
and t2::"trm" |
|
327 |
assumes "z\<sharp>t1" "z\<sharp>t2" |
|
328 |
shows "z\<sharp>t1[y::=t2]" |
|
329 |
using assms fresh_subst' |
|
330 |
by (auto simp add: abs_fresh) |
|
331 |
||
332 |
lemma fresh_psubst_simpl: |
|
333 |
assumes "x\<sharp>t" |
|
334 |
shows "(x,u)#\<theta><t> = \<theta><t>" |
|
335 |
using assms |
|
336 |
proof (nominal_induct t avoiding: x u \<theta> rule: trm.induct) |
|
337 |
case (Lam y t x u) |
|
338 |
have fs: "y\<sharp>\<theta>" "y\<sharp>x" "y\<sharp>u" by fact |
|
339 |
moreover have "x\<sharp> Lam [y].t" by fact |
|
340 |
ultimately have "x\<sharp>t" by (simp add: abs_fresh fresh_atm) |
|
341 |
moreover have ih:"\<And>n T. n\<sharp>t \<Longrightarrow> ((n,T)#\<theta>)<t> = \<theta><t>" by fact |
|
342 |
ultimately have "(x,u)#\<theta><t> = \<theta><t>" by auto |
|
343 |
moreover have "(x,u)#\<theta><Lam [y].t> = Lam [y]. ((x,u)#\<theta><t>)" using fs |
|
344 |
by (simp add: fresh_list_cons fresh_prod) |
|
345 |
moreover have " \<theta><Lam [y].t> = Lam [y]. (\<theta><t>)" using fs by simp |
|
346 |
ultimately show "(x,u)#\<theta><Lam [y].t> = \<theta><Lam [y].t>" by auto |
|
347 |
qed (auto simp add: fresh_atm abs_fresh) |
|
348 |
||
349 |
text {* Equivalence (defined) *} |
|
350 |
||
351 |
inductive2 |
|
352 |
equiv_def :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ == _ : _" [60,60] 60) |
|
353 |
where |
|
354 |
Q_Refl[intro]: "\<Gamma> \<turnstile> t : T \<Longrightarrow> \<Gamma> \<turnstile> t == t : T" |
|
355 |
| Q_Symm[intro]: "\<Gamma> \<turnstile> t == s : T \<Longrightarrow> \<Gamma> \<turnstile> s == t : T" |
|
356 |
| Q_Trans[intro]: "\<lbrakk>\<Gamma> \<turnstile> s == t : T; \<Gamma> \<turnstile> t == u : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s == u : T" |
|
357 |
| Q_Abs[intro]: "\<lbrakk>x\<sharp>\<Gamma>; (x,T1)#\<Gamma> \<turnstile> s2 == t2 : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x]. s2 == Lam [x]. t2 : T1 \<rightarrow> T2" |
|
358 |
| Q_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> s1 == t1 : T1 \<rightarrow> T2 ; \<Gamma> \<turnstile> s2 == t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App s1 s2 == App t1 t2 : T2" |
|
359 |
| Q_Beta[intro]: "\<lbrakk>x\<sharp>(\<Gamma>,s2,t2); (x,T1)#\<Gamma> \<turnstile> s12 == t12 : T2 ; \<Gamma> \<turnstile> s2 == t2 : T1\<rbrakk> |
|
360 |
\<Longrightarrow> \<Gamma> \<turnstile> App (Lam [x]. s12) s2 == t12[x::=t2] : T2" |
|
361 |
| Q_Ext[intro]: "\<lbrakk>x\<sharp>(\<Gamma>,s,t); (x,T1)#\<Gamma> \<turnstile> App s (Var x) == App t (Var x) : T2\<rbrakk> |
|
362 |
\<Longrightarrow> \<Gamma> \<turnstile> s == t : T1 \<rightarrow> T2" |
|
363 |
||
364 |
lemma equiv_def_valid: |
|
365 |
assumes "\<Gamma> \<turnstile> t == s : T" |
|
366 |
shows "valid \<Gamma>" |
|
367 |
using assms by (induct,auto elim:typing_valid) |
|
368 |
||
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
369 |
lemma equiv_def_eqvt[eqvt]: |
22073 | 370 |
fixes pi::"name prm" |
371 |
assumes a: "\<Gamma> \<turnstile> s == t : T" |
|
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
372 |
shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>s) == (pi\<bullet>t) : (pi\<bullet>T)" |
22073 | 373 |
using a |
374 |
apply(induct) |
|
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
375 |
apply(auto intro: typing_eqvt valid_eqvt simp add: fresh_bij subst_eqvt simp del: perm_ty) |
22073 | 376 |
apply(rule_tac x="pi\<bullet>x" in Q_Ext) |
377 |
apply(simp add: fresh_bij)+ |
|
378 |
done |
|
379 |
||
380 |
lemma equiv_def_strong_induct |
|
381 |
[consumes 1, case_names Q_Refl Q_Symm Q_Trans Q_Abs Q_App Q_Beta Q_Ext]: |
|
382 |
fixes c::"'a::fs_name" |
|
383 |
assumes a0: "\<Gamma> \<turnstile> s == t : T" |
|
384 |
and a1: "\<And>\<Gamma> t T c. \<Gamma> \<turnstile> t : T \<Longrightarrow> P c \<Gamma> t t T" |
|
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
385 |
and a2: "\<And>\<Gamma> t s T c. \<lbrakk>\<And>d. P d \<Gamma> t s T\<rbrakk> \<Longrightarrow> P c \<Gamma> s t T" |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
386 |
and a3: "\<And>\<Gamma> s t T u c. \<lbrakk>\<And>d. P d \<Gamma> s t T; \<And>d. P d \<Gamma> t u T\<rbrakk> |
22073 | 387 |
\<Longrightarrow> P c \<Gamma> s u T" |
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
388 |
and a4: "\<And>x \<Gamma> T1 s2 t2 T2 c. \<lbrakk>x\<sharp>\<Gamma>; x\<sharp>c; \<And>d. P d ((x,T1)#\<Gamma>) s2 t2 T2\<rbrakk> |
22073 | 389 |
\<Longrightarrow> P c \<Gamma> (Lam [x].s2) (Lam [x].t2) (T1\<rightarrow>T2)" |
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
390 |
and a5: "\<And>\<Gamma> s1 t1 T1 T2 s2 t2 c. \<lbrakk>\<And>d. P d \<Gamma> s1 t1 (T1\<rightarrow>T2); \<And>d. P d \<Gamma> s2 t2 T1\<rbrakk> |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
391 |
\<Longrightarrow> P c \<Gamma> (App s1 s2) (App t1 t2) T2" |
22073 | 392 |
and a6: "\<And>x \<Gamma> T1 s12 t12 T2 s2 t2 c. |
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
393 |
\<lbrakk>x\<sharp>(\<Gamma>,s2,t2); x\<sharp>c; \<And>d. P d ((x,T1)#\<Gamma>) s12 t12 T2; \<And>d. P d \<Gamma> s2 t2 T1\<rbrakk> |
22073 | 394 |
\<Longrightarrow> P c \<Gamma> (App (Lam [x].s12) s2) (t12[x::=t2]) T2" |
395 |
and a7: "\<And>x \<Gamma> s t T1 T2 c. |
|
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
396 |
\<lbrakk>x\<sharp>(\<Gamma>,s,t); \<And>d. P d ((x,T1)#\<Gamma>) (App s (Var x)) (App t (Var x)) T2\<rbrakk> |
22073 | 397 |
\<Longrightarrow> P c \<Gamma> s t (T1\<rightarrow>T2)" |
398 |
shows "P c \<Gamma> s t T" |
|
399 |
proof - |
|
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
400 |
from a0 have "\<And>(pi::name prm) c. P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) (pi\<bullet>T)" |
22073 | 401 |
proof(induct) |
402 |
case (Q_Refl \<Gamma> t T pi c) |
|
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
403 |
then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>t) (pi\<bullet>t) (pi\<bullet>T)" using a1 by (simp only: eqvt) |
22073 | 404 |
next |
405 |
case (Q_Symm \<Gamma> t s T pi c) |
|
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
406 |
then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) (pi\<bullet>T)" using a2 by (simp only: equiv_def_eqvt) |
22073 | 407 |
next |
408 |
case (Q_Trans \<Gamma> s t T u pi c) |
|
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
409 |
then show " P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>u) (pi\<bullet>T)" using a3 by (blast intro: equiv_def_eqvt) |
22073 | 410 |
next |
411 |
case (Q_App \<Gamma> s1 t1 T1 T2 s2 t2 pi c) |
|
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
412 |
then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>App s1 s2) (pi\<bullet>App t1 t2) (pi\<bullet>T2)" using a5 |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
413 |
by (simp only: eqvt) (blast) |
22073 | 414 |
next |
415 |
case (Q_Ext x \<Gamma> s t T1 T2 pi c) |
|
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
416 |
then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) (pi\<bullet>T1\<rightarrow>T2)" |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
417 |
by (auto intro!: a7 simp add: fresh_bij) |
22073 | 418 |
next |
419 |
case (Q_Abs x \<Gamma> T1 s2 t2 T2 pi c) |
|
420 |
obtain y::"name" where fs: "y\<sharp>(pi\<bullet>x,pi\<bullet>s2,pi\<bullet>t2,pi\<bullet>\<Gamma>,c)" by (rule exists_fresh[OF fs_name1]) |
|
421 |
let ?sw="[(pi\<bullet>x,y)]" |
|
422 |
let ?pi'="?sw@pi" |
|
423 |
have f1: "x\<sharp>\<Gamma>" by fact |
|
424 |
have f2: "(pi\<bullet>x)\<sharp>(pi\<bullet>\<Gamma>)" using f1 by (simp add: fresh_bij) |
|
425 |
have f3: "y\<sharp>?pi'\<bullet>\<Gamma>" using f1 by (auto simp add: pt_name2 fresh_left calc_atm perm_pi_simp) |
|
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
426 |
have ih1: "\<And>c. P c (?pi'\<bullet>((x,T1)#\<Gamma>)) (?pi'\<bullet>s2) (?pi'\<bullet>t2) (?pi'\<bullet>T2)" by fact |
22073 | 427 |
then have "\<And>c. P c ((y,T1)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>s2) (?pi'\<bullet>t2) T2" by (simp add: calc_atm) |
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
428 |
then have "P c (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>Lam [x].s2) (?pi'\<bullet>Lam [x].t2) (T1\<rightarrow>T2)" using a4 f3 fs |
22073 | 429 |
by (simp add: calc_atm) |
430 |
then have "P c (?sw\<bullet>pi\<bullet>\<Gamma>) (?sw\<bullet>Lam [(pi\<bullet>x)].(pi\<bullet>s2)) (?sw\<bullet>Lam [(pi\<bullet>x)].(pi\<bullet>t2)) (T1\<rightarrow>T2)" |
|
431 |
by (simp del: append_Cons add: calc_atm pt_name2) |
|
432 |
moreover have "(?sw\<bullet>(pi\<bullet>\<Gamma>)) = (pi\<bullet>\<Gamma>)" |
|
433 |
by (rule perm_fresh_fresh) (simp_all add: fs f2) |
|
434 |
moreover have "(?sw\<bullet>(Lam [(pi\<bullet>x)].(pi\<bullet>s2))) = Lam [(pi\<bullet>x)].(pi\<bullet>s2)" |
|
435 |
by (rule perm_fresh_fresh) (simp_all add: fs f2 abs_fresh) |
|
436 |
moreover have "(?sw\<bullet>(Lam [(pi\<bullet>x)].(pi\<bullet>t2))) = Lam [(pi\<bullet>x)].(pi\<bullet>t2)" |
|
437 |
by (rule perm_fresh_fresh) (simp_all add: fs f2 abs_fresh) |
|
438 |
ultimately have "P c (pi\<bullet>\<Gamma>) (Lam [(pi\<bullet>x)].(pi\<bullet>s2)) (Lam [(pi\<bullet>x)].(pi\<bullet>t2)) (T1\<rightarrow>T2)" by simp |
|
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
439 |
then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>Lam [x].s2) (pi\<bullet>Lam [x].t2) (pi\<bullet>T1\<rightarrow>T2)" by simp |
22073 | 440 |
next |
441 |
case (Q_Beta x \<Gamma> s2 t2 T1 s12 t12 T2 pi c) |
|
442 |
obtain y::"name" where fs: "y\<sharp>(pi\<bullet>x,pi\<bullet>s12,pi\<bullet>t12,pi\<bullet>s2,pi\<bullet>t2,pi\<bullet>\<Gamma>,c)" |
|
443 |
by (rule exists_fresh[OF fs_name1]) |
|
444 |
let ?sw="[(pi\<bullet>x,y)]" |
|
445 |
let ?pi'="?sw@pi" |
|
446 |
have f1: "x\<sharp>(\<Gamma>,s2,t2)" by fact |
|
447 |
have f2: "(pi\<bullet>x)\<sharp>(pi\<bullet>(\<Gamma>,s2,t2))" using f1 by (simp add: fresh_bij) |
|
448 |
have f3: "y\<sharp>(?pi'\<bullet>(\<Gamma>,s2,t2))" using f1 |
|
449 |
by (auto simp add: pt_name2 fresh_left calc_atm perm_pi_simp fresh_prod) |
|
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
450 |
have ih1: "\<And>c. P c (?pi'\<bullet>((x,T1)#\<Gamma>)) (?pi'\<bullet>s12) (?pi'\<bullet>t12) (?pi'\<bullet>T2)" by fact |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
451 |
then have "\<And>c. P c ((y,T1)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>s12) (?pi'\<bullet>t12) (?pi'\<bullet>T2)" by (simp add: calc_atm) |
22073 | 452 |
moreover |
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
453 |
have ih2: "\<And>c. P c (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>s2) (?pi'\<bullet>t2) (?pi'\<bullet>T1)" by fact |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
454 |
ultimately have "P c (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>(App (Lam [x].s12) s2)) (?pi'\<bullet>(t12[x::=t2])) (?pi'\<bullet>T2)" |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
455 |
using a6 f3 fs by (force simp add: subst_eqvt calc_atm del: perm_ty) |
22073 | 456 |
then have "P c (?sw\<bullet>pi\<bullet>\<Gamma>) (?sw\<bullet>(App (Lam [(pi\<bullet>x)].(pi\<bullet>s12)) (pi\<bullet>s2))) |
457 |
(?sw\<bullet>((pi\<bullet>t12)[(pi\<bullet>x)::=(pi\<bullet>t2)])) T2" |
|
458 |
by (simp del: append_Cons add: calc_atm pt_name2 subst_eqvt) |
|
459 |
moreover have "(?sw\<bullet>(pi\<bullet>\<Gamma>)) = (pi\<bullet>\<Gamma>)" |
|
460 |
by (rule perm_fresh_fresh) (simp_all add: fs[simplified] f2[simplified]) |
|
461 |
moreover have "(?sw\<bullet>(App (Lam [(pi\<bullet>x)].(pi\<bullet>s12)) (pi\<bullet>s2))) = App (Lam [(pi\<bullet>x)].(pi\<bullet>s12)) (pi\<bullet>s2)" |
|
462 |
by (rule perm_fresh_fresh) (simp_all add: fs[simplified] f2[simplified] abs_fresh) |
|
463 |
moreover have "(?sw\<bullet>((pi\<bullet>t12)[(pi\<bullet>x)::=(pi\<bullet>t2)])) = ((pi\<bullet>t12)[(pi\<bullet>x)::=(pi\<bullet>t2)])" |
|
464 |
by (rule perm_fresh_fresh) |
|
465 |
(simp_all add: fs[simplified] f2[simplified] fresh_subst fresh_subst'') |
|
466 |
ultimately have "P c (pi\<bullet>\<Gamma>) (App (Lam [(pi\<bullet>x)].(pi\<bullet>s12)) (pi\<bullet>s2)) ((pi\<bullet>t12)[(pi\<bullet>x)::=(pi\<bullet>t2)]) T2" |
|
467 |
by simp |
|
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
468 |
then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>App (Lam [x].s12) s2) (pi\<bullet>t12[x::=t2]) (pi\<bullet>T2)" by (simp add: subst_eqvt) |
22073 | 469 |
qed |
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
470 |
then have "P c (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>s) (([]::name prm)\<bullet>t) (([]::name prm)\<bullet>T)" by blast |
22073 | 471 |
then show "P c \<Gamma> s t T" by simp |
472 |
qed |
|
473 |
||
474 |
text {* Weak head reduction *} |
|
475 |
||
476 |
inductive2 |
|
477 |
whr_def :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<leadsto> _" [80,80] 80) |
|
478 |
where |
|
479 |
QAR_Beta[intro]: "App (Lam [x]. t12) t2 \<leadsto> t12[x::=t2]" |
|
480 |
| QAR_App[intro]: "t1 \<leadsto> t1' \<Longrightarrow> App t1 t2 \<leadsto> App t1' t2" |
|
481 |
||
482 |
declare trm.inject [simp add] |
|
483 |
declare ty.inject [simp add] |
|
484 |
||
485 |
inductive_cases2 whr_Gen[elim]: "t \<leadsto> t'" |
|
486 |
inductive_cases2 whr_Lam[elim]: "Lam [x].t \<leadsto> t'" |
|
487 |
inductive_cases2 whr_App_Lam[elim]: "App (Lam [x].t12) t2 \<leadsto> t" |
|
488 |
inductive_cases2 whr_Var[elim]: "Var x \<leadsto> t" |
|
489 |
inductive_cases2 whr_Const[elim]: "Const n \<leadsto> t" |
|
490 |
inductive_cases2 whr_App[elim]: "App p q \<leadsto> t" |
|
491 |
inductive_cases2 whr_Const_Right[elim]: "t \<leadsto> Const n" |
|
492 |
inductive_cases2 whr_Var_Right[elim]: "t \<leadsto> Var x" |
|
493 |
inductive_cases2 whr_App_Right[elim]: "t \<leadsto> App p q" |
|
494 |
||
495 |
declare trm.inject [simp del] |
|
496 |
declare ty.inject [simp del] |
|
497 |
||
498 |
text {* Weak head normalization *} |
|
499 |
||
500 |
abbreviation |
|
501 |
nf :: "trm \<Rightarrow> bool" ("_ \<leadsto>|" [100] 100) |
|
502 |
where |
|
503 |
"t\<leadsto>| \<equiv> \<not>(\<exists> u. t \<leadsto> u)" |
|
504 |
||
505 |
inductive2 |
|
506 |
whn_def :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<Down> _" [80,80] 80) |
|
507 |
where |
|
508 |
QAN_Reduce[intro]: "\<lbrakk>s \<leadsto> t; t \<Down> u\<rbrakk> \<Longrightarrow> s \<Down> u" |
|
509 |
| QAN_Normal[intro]: "t\<leadsto>| \<Longrightarrow> t \<Down> t" |
|
510 |
||
511 |
lemma whr_eqvt: |
|
512 |
fixes pi::"name prm" |
|
513 |
assumes a: "t \<leadsto> t'" |
|
514 |
shows "(pi\<bullet>t) \<leadsto> (pi\<bullet>t')" |
|
22082 | 515 |
using a |
516 |
by (induct) (auto simp add: subst_eqvt fresh_bij) |
|
22073 | 517 |
|
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
518 |
lemma whn_eqvt[eqvt]: |
22073 | 519 |
fixes pi::"name prm" |
520 |
assumes a: "t \<Down> t'" |
|
521 |
shows "(pi\<bullet>t) \<Down> (pi\<bullet>t')" |
|
22082 | 522 |
using a |
523 |
apply(induct) |
|
524 |
apply(rule QAN_Reduce) |
|
525 |
apply(rule whr_eqvt) |
|
526 |
apply(assumption)+ |
|
527 |
apply(rule QAN_Normal) |
|
528 |
apply(auto) |
|
529 |
apply(drule_tac pi="rev pi" in whr_eqvt) |
|
530 |
apply(perm_simp) |
|
531 |
done |
|
22073 | 532 |
|
533 |
text {* Algorithmic term equivalence and algorithmic path equivalence *} |
|
534 |
||
535 |
inductive2 |
|
536 |
alg_equiv :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ <=> _ : _" [60,60] 60) |
|
537 |
and |
|
538 |
alg_path_equiv :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<leftrightarrow> _ : _" [60,60] 60) |
|
539 |
where |
|
540 |
QAT_Base[intro]: "\<lbrakk>s \<Down> p; t \<Down> q; \<Gamma> \<turnstile> p \<leftrightarrow> q : TBase \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s <=> t : TBase" |
|
541 |
| QAT_Arrow[intro]: "\<lbrakk>x\<sharp>\<Gamma>; x\<sharp>s; x\<sharp>t; (x,T1)#\<Gamma> \<turnstile> App s (Var x) <=> App t (Var x) : T2\<rbrakk> |
|
542 |
\<Longrightarrow> \<Gamma> \<turnstile> s <=> t : T1 \<rightarrow> T2" |
|
543 |
| QAT_One[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> s <=> t : TUnit" |
|
544 |
| QAP_Var[intro]: "\<lbrakk>valid \<Gamma>;(x,T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x \<leftrightarrow> Var x : T" |
|
545 |
| QAP_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> p \<leftrightarrow> q : T1 \<rightarrow> T2; \<Gamma> \<turnstile> s <=> t : T1 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App p s \<leftrightarrow> App q t : T2" |
|
546 |
| QAP_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n \<leftrightarrow> Const n : TBase" |
|
547 |
||
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
548 |
lemma alg_equiv_alg_path_equiv_eqvt[eqvt]: |
22073 | 549 |
fixes pi::"name prm" |
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
550 |
shows "\<Gamma> \<turnstile> s <=> t : T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>s) <=> (pi\<bullet>t) : (pi\<bullet>T)" |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
551 |
and "\<Gamma> \<turnstile> p \<leftrightarrow> q : T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>p) \<leftrightarrow> (pi\<bullet>q) : (pi\<bullet>T)" |
22073 | 552 |
apply(induct rule: alg_equiv_alg_path_equiv.inducts) |
553 |
apply(auto intro: whn_eqvt simp add: fresh_bij valid_eqvt) |
|
554 |
apply(rule_tac x="pi\<bullet>x" in QAT_Arrow) |
|
555 |
apply(auto simp add: fresh_bij) |
|
556 |
apply(rule QAP_Var) |
|
557 |
apply(simp add: valid_eqvt) |
|
558 |
apply(simp add: pt_list_set_pi[OF pt_name_inst, symmetric]) |
|
559 |
apply(perm_simp add: pt_set_bij1a[OF pt_name_inst, OF at_name_inst]) |
|
560 |
done |
|
561 |
||
562 |
lemma alg_equiv_alg_path_equiv_strong_induct |
|
563 |
[case_names QAT_Base QAT_Arrow QAT_One QAP_Var QAP_App QAP_Const]: |
|
564 |
fixes c::"'a::fs_name" |
|
565 |
assumes a1: "\<And>s p t q \<Gamma> c. \<lbrakk>s \<Down> p; t \<Down> q; \<Gamma> \<turnstile> p \<leftrightarrow> q : TBase; \<And>d. P2 d \<Gamma> p q TBase\<rbrakk> |
|
566 |
\<Longrightarrow> P1 c \<Gamma> s t TBase" |
|
567 |
and a2: "\<And>x \<Gamma> s t T1 T2 c. |
|
568 |
\<lbrakk>x\<sharp>\<Gamma>; x\<sharp>s; x\<sharp>t; x\<sharp>c; (x,T1)#\<Gamma> \<turnstile> App s (Var x) <=> App t (Var x) : T2; |
|
569 |
\<And>d. P1 d ((x,T1)#\<Gamma>) (App s (Var x)) (App t (Var x)) T2\<rbrakk> |
|
570 |
\<Longrightarrow> P1 c \<Gamma> s t (T1\<rightarrow>T2)" |
|
571 |
and a3: "\<And>\<Gamma> s t c. valid \<Gamma> \<Longrightarrow> P1 c \<Gamma> s t TUnit" |
|
572 |
and a4: "\<And>\<Gamma> x T c. \<lbrakk>valid \<Gamma>; (x,T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> P2 c \<Gamma> (Var x) (Var x) T" |
|
573 |
and a5: "\<And>\<Gamma> p q T1 T2 s t c. |
|
574 |
\<lbrakk>\<Gamma> \<turnstile> p \<leftrightarrow> q : T1\<rightarrow>T2; \<And>d. P2 d \<Gamma> p q (T1\<rightarrow>T2); \<Gamma> \<turnstile> s <=> t : T1; \<And>d. P1 d \<Gamma> s t T1\<rbrakk> |
|
575 |
\<Longrightarrow> P2 c \<Gamma> (App p s) (App q t) T2" |
|
576 |
and a6: "\<And>\<Gamma> n c. valid \<Gamma> \<Longrightarrow> P2 c \<Gamma> (Const n) (Const n) TBase" |
|
577 |
shows "(\<Gamma> \<turnstile> s <=> t : T \<longrightarrow>P1 c \<Gamma> s t T) \<and> (\<Gamma>' \<turnstile> s' \<leftrightarrow> t' : T' \<longrightarrow> P2 c \<Gamma>' s' t' T')" |
|
578 |
proof - |
|
579 |
have "(\<Gamma> \<turnstile> s <=> t : T \<longrightarrow> (\<forall>c (pi::name prm). P1 c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) T)) \<and> |
|
580 |
(\<Gamma>' \<turnstile> s' \<leftrightarrow> t' : T' \<longrightarrow> (\<forall>c (pi::name prm). P2 c (pi\<bullet>\<Gamma>') (pi\<bullet>s') (pi\<bullet>t') T'))" |
|
581 |
proof(induct rule: alg_equiv_alg_path_equiv.induct) |
|
582 |
case (QAT_Base s q t p \<Gamma>) |
|
583 |
then show "\<forall>c (pi::name prm). P1 c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) TBase" |
|
584 |
apply(auto) |
|
585 |
apply(rule_tac p="pi\<bullet>q" and q="pi\<bullet>p" in a1) |
|
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
586 |
apply(simp_all add: whn_eqvt alg_equiv_alg_path_equiv_eqvt[simplified]) |
22073 | 587 |
done |
588 |
next |
|
589 |
case (QAT_Arrow x \<Gamma> s t T1 T2) |
|
590 |
show ?case |
|
591 |
proof (rule allI, rule allI) |
|
592 |
fix c::"'a::fs_name" and pi::"name prm" |
|
593 |
obtain y::"name" where fs: "y\<sharp>(pi\<bullet>s,pi\<bullet>t,pi\<bullet>\<Gamma>,c)" by (rule exists_fresh[OF fs_name1]) |
|
594 |
let ?sw="[(pi\<bullet>x,y)]" |
|
595 |
let ?pi'="?sw@pi" |
|
596 |
have f0: "x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact |
|
597 |
then have f1: "x\<sharp>(\<Gamma>,s,t)" by simp |
|
598 |
have f2: "(pi\<bullet>x)\<sharp>(pi\<bullet>(\<Gamma>,s,t))" using f1 by (simp add: fresh_bij) |
|
599 |
have f3: "y\<sharp>?pi'\<bullet>(\<Gamma>,s,t)" using f1 |
|
600 |
by (simp only: pt_name2 fresh_left, auto simp add: perm_pi_simp calc_atm) |
|
601 |
then have f3': "y\<sharp>?pi'\<bullet>\<Gamma>" "y\<sharp>?pi'\<bullet>s" "y\<sharp>?pi'\<bullet>t" by (auto simp add: fresh_prod) |
|
602 |
have pr1: "(x,T1)#\<Gamma> \<turnstile> App s (Var x) <=> App t (Var x) : T2" by fact |
|
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
603 |
then have "(?pi'\<bullet>((x,T1)#\<Gamma>)) \<turnstile> (?pi'\<bullet>(App s (Var x))) <=> (?pi'\<bullet>(App t (Var x))) : (?pi'\<bullet>T2)" |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
604 |
by (rule alg_equiv_alg_path_equiv_eqvt) |
22073 | 605 |
then have "(y,T1)#(?pi'\<bullet>\<Gamma>) \<turnstile> (App (?pi'\<bullet>s) (Var y)) <=> (App (?pi'\<bullet>t) (Var y)) : T2" |
606 |
by (simp add: calc_atm) |
|
607 |
moreover |
|
608 |
have ih1: "\<forall>c (pi::name prm). P1 c (pi\<bullet>((x,T1)#\<Gamma>)) (pi\<bullet>App s (Var x)) (pi\<bullet>App t (Var x)) T2" |
|
609 |
by fact |
|
610 |
then have "\<And>c. P1 c (?pi'\<bullet>((x,T1)#\<Gamma>)) (?pi'\<bullet>App s (Var x)) (?pi'\<bullet>App t (Var x)) T2" |
|
611 |
by auto |
|
612 |
then have "\<And>c. P1 c ((y,T1)#(?pi'\<bullet>\<Gamma>)) (App (?pi'\<bullet>s) (Var y)) (App (?pi'\<bullet>t) (Var y)) T2" |
|
613 |
by (simp add: calc_atm) |
|
614 |
ultimately have "P1 c (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>s) (?pi'\<bullet>t) (T1\<rightarrow>T2)" using a2 f3' fs by simp |
|
615 |
then have "P1 c (?sw\<bullet>pi\<bullet>\<Gamma>) (?sw\<bullet>pi\<bullet>s) (?sw\<bullet>pi\<bullet>t) (T1\<rightarrow>T2)" |
|
616 |
by (simp del: append_Cons add: calc_atm pt_name2) |
|
617 |
moreover have "(?sw\<bullet>(pi\<bullet>\<Gamma>)) = (pi\<bullet>\<Gamma>)" |
|
618 |
by (rule perm_fresh_fresh) (simp_all add: fs[simplified] f2[simplified]) |
|
619 |
moreover have "(?sw\<bullet>(pi\<bullet>s)) = (pi\<bullet>s)" |
|
620 |
by (rule perm_fresh_fresh) (simp_all add: fs[simplified] f2[simplified]) |
|
621 |
moreover have "(?sw\<bullet>(pi\<bullet>t)) = (pi\<bullet>t)" |
|
622 |
by (rule perm_fresh_fresh) (simp_all add: fs[simplified] f2[simplified]) |
|
623 |
ultimately show "P1 c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) (T1\<rightarrow>T2)" by (simp) |
|
624 |
qed |
|
625 |
next |
|
626 |
case (QAT_One \<Gamma> s t) |
|
627 |
then show "\<forall>c (pi::name prm). P1 c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) TUnit" |
|
628 |
by (auto intro!: a3 simp add: valid_eqvt) |
|
629 |
next |
|
630 |
case (QAP_Var \<Gamma> x T) |
|
631 |
then show "\<forall>c (pi::name prm). P2 c (pi \<bullet> \<Gamma>) (pi \<bullet> Var x) (pi \<bullet> Var x) T" |
|
632 |
apply(auto intro!: a4 simp add: valid_eqvt) |
|
633 |
apply(simp add: pt_list_set_pi[OF pt_name_inst, symmetric]) |
|
634 |
apply(perm_simp add: pt_set_bij1a[OF pt_name_inst, OF at_name_inst]) |
|
635 |
done |
|
636 |
next |
|
637 |
case (QAP_App \<Gamma> p q T1 T2 s t) |
|
638 |
then show "\<forall>c (pi::name prm). P2 c (pi\<bullet>\<Gamma>) (pi\<bullet>App p s) (pi\<bullet>App q t) T2" |
|
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
639 |
by (auto intro!: a5 simp add: alg_equiv_alg_path_equiv_eqvt[simplified]) |
22073 | 640 |
next |
641 |
case (QAP_Const \<Gamma> n) |
|
642 |
then show "\<forall>c (pi::name prm). P2 c (pi\<bullet>\<Gamma>) (pi\<bullet>Const n) (pi\<bullet>Const n) TBase" |
|
643 |
by (auto intro!: a6 simp add: valid_eqvt) |
|
644 |
qed |
|
645 |
then have "(\<Gamma> \<turnstile> s <=> t : T \<longrightarrow> P1 c (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>s) (([]::name prm)\<bullet>t) T) \<and> |
|
646 |
(\<Gamma>' \<turnstile> s' \<leftrightarrow> t' : T' \<longrightarrow> P2 c (([]::name prm)\<bullet>\<Gamma>') (([]::name prm)\<bullet>s') (([]::name prm)\<bullet>t') T')" |
|
647 |
by blast |
|
648 |
then show ?thesis by simp |
|
649 |
qed |
|
650 |
||
22082 | 651 |
(* post-processing of the strong induction principle proved above; *) |
652 |
(* the code extracts the strong_inducts-version from strong_induct *) |
|
22073 | 653 |
setup {* |
654 |
PureThy.add_thmss |
|
655 |
[(("alg_equiv_alg_path_equiv_strong_inducts", |
|
656 |
ProjectRule.projects (ProofContext.init (the_context())) [1,2] |
|
657 |
(thm "alg_equiv_alg_path_equiv_strong_induct")), [])] #> snd |
|
658 |
*} |
|
659 |
||
660 |
declare trm.inject [simp add] |
|
661 |
declare ty.inject [simp add] |
|
662 |
||
663 |
inductive_cases2 whn_inv_auto[elim]: "t \<Down> t'" |
|
664 |
||
665 |
inductive_cases2 alg_equiv_Base_inv_auto[elim]: "\<Gamma> \<turnstile> s<=>t : TBase" |
|
666 |
inductive_cases2 alg_equiv_Arrow_inv_auto[elim]: "\<Gamma> \<turnstile> s<=>t : T1 \<rightarrow> T2" |
|
667 |
||
668 |
inductive_cases2 alg_path_equiv_Base_inv_auto[elim]: "\<Gamma> \<turnstile> s\<leftrightarrow>t : TBase" |
|
669 |
inductive_cases2 alg_path_equiv_Unit_inv_auto[elim]: "\<Gamma> \<turnstile> s\<leftrightarrow>t : TUnit" |
|
670 |
inductive_cases2 alg_path_equiv_Arrow_inv_auto[elim]: "\<Gamma> \<turnstile> s\<leftrightarrow>t : T1 \<rightarrow> T2" |
|
671 |
||
672 |
inductive_cases2 alg_path_equiv_Var_left_inv_auto[elim]: "\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T" |
|
673 |
inductive_cases2 alg_path_equiv_Var_left_inv_auto'[elim]: "\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T'" |
|
674 |
inductive_cases2 alg_path_equiv_Var_right_inv_auto[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T" |
|
675 |
inductive_cases2 alg_path_equiv_Var_right_inv_auto'[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T'" |
|
676 |
inductive_cases2 alg_path_equiv_Const_left_inv_auto[elim]: "\<Gamma> \<turnstile> Const n \<leftrightarrow> t : T" |
|
677 |
inductive_cases2 alg_path_equiv_Const_right_inv_auto[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> Const n : T" |
|
678 |
inductive_cases2 alg_path_equiv_App_left_inv_auto[elim]: "\<Gamma> \<turnstile> App p s \<leftrightarrow> t : T" |
|
679 |
inductive_cases2 alg_path_equiv_App_right_inv_auto[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> App q t : T" |
|
680 |
inductive_cases2 alg_path_equiv_Lam_left_inv_auto[elim]: "\<Gamma> \<turnstile> Lam[x].s \<leftrightarrow> t : T" |
|
681 |
inductive_cases2 alg_path_equiv_Lam_right_inv_auto[elim]: "\<Gamma> \<turnstile> t \<leftrightarrow> Lam[x].s : T" |
|
682 |
||
683 |
declare trm.inject [simp del] |
|
684 |
declare ty.inject [simp del] |
|
685 |
||
686 |
text {* Subcontext. *} |
|
687 |
||
688 |
abbreviation |
|
689 |
"sub" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" (" _ \<lless> _ " [55,55] 55) |
|
690 |
where |
|
691 |
"\<Gamma>1 \<lless> \<Gamma>2 \<equiv> (\<forall>a \<sigma>. (a,\<sigma>)\<in>set \<Gamma>1 \<longrightarrow> (a,\<sigma>)\<in>set \<Gamma>2) \<and> valid \<Gamma>2" |
|
692 |
||
693 |
lemma alg_equiv_valid: |
|
694 |
shows "\<Gamma> \<turnstile> s <=> t : T \<Longrightarrow> valid \<Gamma>" and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> valid \<Gamma>" |
|
695 |
by (induct rule : alg_equiv_alg_path_equiv.inducts, auto) |
|
696 |
||
697 |
lemma algorithmic_monotonicity: |
|
698 |
fixes \<Gamma>':: "(name\<times>ty) list" |
|
699 |
shows "\<Gamma> \<turnstile> s <=> t : T \<Longrightarrow> \<Gamma>\<lless>\<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s <=> t : T" |
|
700 |
and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma>\<lless>\<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<leftrightarrow> t : T" |
|
701 |
proof (nominal_induct \<Gamma> s t T and \<Gamma> s t T avoiding: \<Gamma>' rule: alg_equiv_alg_path_equiv_strong_inducts) |
|
702 |
case (QAT_Arrow x \<Gamma> s t T1 T2 \<Gamma>') |
|
703 |
have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact |
|
704 |
have h2:"\<Gamma>\<lless>\<Gamma>'" by fact |
|
705 |
have ih:"\<And>\<Gamma>'. \<lbrakk>(x,T1)#\<Gamma> \<lless> \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> App s (Var x) <=> App t (Var x) : T2" by fact |
|
706 |
have "x\<sharp>\<Gamma>'" by fact |
|
707 |
then have sub:"(x,T1)#\<Gamma> \<lless> (x,T1)#\<Gamma>'" using h2 by auto |
|
708 |
then have "(x,T1)#\<Gamma>' \<turnstile> App s (Var x) <=> App t (Var x) : T2" using ih by auto |
|
709 |
then show "\<Gamma>' \<turnstile> s <=> t : T1\<rightarrow>T2" using sub fs by auto |
|
710 |
qed (auto) |
|
711 |
||
712 |
text {* Logical equivalence. *} |
|
713 |
||
714 |
function log_equiv :: "((name\<times>ty) list \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool)" |
|
715 |
("_ \<turnstile> _ is _ : _" [60,60,60,60] 60) |
|
716 |
where |
|
717 |
"\<Gamma> \<turnstile> s is t : TUnit = valid \<Gamma>" |
|
718 |
| "\<Gamma> \<turnstile> s is t : TBase = \<Gamma> \<turnstile> s <=> t : TBase" |
|
22082 | 719 |
| "\<Gamma> \<turnstile> s is t : (T1 \<rightarrow> T2) = |
720 |
(valid \<Gamma> \<and> (\<forall>\<Gamma>' s' t'. \<Gamma>\<lless>\<Gamma>' \<longrightarrow> \<Gamma>' \<turnstile> s' is t' : T1 \<longrightarrow> (\<Gamma>' \<turnstile> (App s s') is (App t t') : T2)))" |
|
22073 | 721 |
apply (auto simp add: ty.inject) |
22082 | 722 |
apply (subgoal_tac "(\<exists>T1 T2. b=T1 \<rightarrow> T2) \<or> b=TUnit \<or> b=TBase" ) |
22073 | 723 |
apply (force) |
724 |
apply (rule ty_cases) |
|
725 |
done |
|
726 |
||
727 |
termination |
|
728 |
apply(relation "measure (\<lambda>(_,_,_,T). size T)") |
|
729 |
apply(auto) |
|
730 |
done |
|
731 |
||
732 |
lemma log_equiv_valid: |
|
733 |
assumes "\<Gamma> \<turnstile> s is t : T" |
|
734 |
shows "valid \<Gamma>" |
|
735 |
using assms |
|
736 |
by (induct rule: log_equiv.induct,auto elim: alg_equiv_valid) |
|
737 |
||
738 |
lemma logical_monotonicity : |
|
739 |
fixes T::ty |
|
740 |
assumes "\<Gamma> \<turnstile> s is t : T" "\<Gamma>\<lless>\<Gamma>'" |
|
741 |
shows "\<Gamma>' \<turnstile> s is t : T" |
|
742 |
using assms |
|
743 |
proof (induct arbitrary: \<Gamma>' rule: log_equiv.induct) |
|
744 |
case (2 \<Gamma> s t \<Gamma>') |
|
745 |
then show "\<Gamma>' \<turnstile> s is t : TBase" using algorithmic_monotonicity by auto |
|
746 |
next |
|
747 |
case (3 \<Gamma> s t T1 T2 \<Gamma>') |
|
748 |
have h1:"\<Gamma> \<turnstile> s is t : T1\<rightarrow>T2" by fact |
|
749 |
have h2:"\<Gamma>\<lless>\<Gamma>'" by fact |
|
750 |
{ |
|
751 |
fix \<Gamma>'' s' t' |
|
752 |
assume "\<Gamma>'\<lless>\<Gamma>''" "\<Gamma>'' \<turnstile> s' is t' : T1" |
|
753 |
then have "\<Gamma>'' \<turnstile> (App s s') is (App t t') : T2" using h1 h2 by auto |
|
754 |
} |
|
755 |
then show "\<Gamma>' \<turnstile> s is t : T1\<rightarrow>T2" using h2 by auto |
|
756 |
qed (auto) |
|
757 |
||
758 |
lemma forget: |
|
759 |
fixes x::"name" |
|
760 |
and L::"trm" |
|
761 |
assumes a: "x\<sharp>L" |
|
762 |
shows "L[x::=P] = L" |
|
763 |
using a |
|
22082 | 764 |
by (nominal_induct L avoiding: x P rule: trm.induct) |
765 |
(auto simp add: fresh_atm abs_fresh) |
|
22073 | 766 |
|
767 |
lemma subst_fun_eq: |
|
768 |
fixes u::trm |
|
769 |
assumes h:"[x].t1 = [y].t2" |
|
770 |
shows "t1[x::=u] = t2[y::=u]" |
|
771 |
proof - |
|
772 |
{ |
|
773 |
assume "x=y" and "t1=t2" |
|
774 |
then have ?thesis using h by simp |
|
775 |
} |
|
776 |
moreover |
|
777 |
{ |
|
778 |
assume h1:"x \<noteq> y" and h2:"t1=[(x,y)] \<bullet> t2" and h3:"x \<sharp> t2" |
|
779 |
then have "([(x,y)] \<bullet> t2)[x::=u] = t2[y::=u]" by (simp add: subst_rename) |
|
780 |
then have ?thesis using h2 by simp |
|
781 |
} |
|
782 |
ultimately show ?thesis using alpha h by blast |
|
783 |
qed |
|
784 |
||
785 |
lemma psubst_empty[simp]: |
|
786 |
shows "[]<t> = t" |
|
787 |
by (nominal_induct t rule: trm.induct) (auto simp add: fresh_list_nil) |
|
788 |
||
789 |
lemma psubst_subst_psubst: |
|
790 |
assumes h:"c \<sharp> \<theta>" |
|
791 |
shows "\<theta><t>[c::=s] = (c,s)#\<theta><t>" |
|
792 |
using h |
|
22082 | 793 |
by (nominal_induct t avoiding: \<theta> c s rule: trm.induct) |
794 |
(auto simp add: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh' fresh_psubst) |
|
22073 | 795 |
|
796 |
lemma subst_fresh_simpl: |
|
22082 | 797 |
assumes a: "x\<sharp>\<theta>" |
22073 | 798 |
shows "\<theta><Var x> = Var x" |
22082 | 799 |
using a |
800 |
by (induct \<theta> arbitrary: x, auto simp add:fresh_list_cons fresh_prod fresh_atm) |
|
22073 | 801 |
|
802 |
lemma psubst_subst_propagate: |
|
803 |
assumes "x\<sharp>\<theta>" |
|
804 |
shows "\<theta><t[x::=u]> = \<theta><t>[x::=\<theta><u>]" |
|
805 |
using assms |
|
806 |
proof (nominal_induct t avoiding: x u \<theta> rule: trm.induct) |
|
807 |
case (Var n x u \<theta>) |
|
808 |
{ assume "x=n" |
|
809 |
moreover have "x\<sharp>\<theta>" by fact |
|
810 |
ultimately have "\<theta><Var n[x::=u]> = \<theta><Var n>[x::=\<theta><u>]" using subst_fresh_simpl by auto |
|
811 |
} |
|
812 |
moreover |
|
813 |
{ assume h:"x\<noteq>n" |
|
814 |
then have "x\<sharp>Var n" by (auto simp add: fresh_atm) |
|
815 |
moreover have "x\<sharp>\<theta>" by fact |
|
816 |
ultimately have "x\<sharp>\<theta><Var n>" using fresh_psubst by blast |
|
817 |
then have " \<theta><Var n>[x::=\<theta><u>] = \<theta><Var n>" using forget by auto |
|
818 |
then have "\<theta><Var n[x::=u]> = \<theta><Var n>[x::=\<theta><u>]" using h by auto |
|
819 |
} |
|
820 |
ultimately show ?case by auto |
|
821 |
next |
|
822 |
case (Lam n t x u \<theta>) |
|
823 |
have fs:"n\<sharp>x" "n\<sharp>u" "n\<sharp>\<theta>" "x\<sharp>\<theta>" by fact |
|
824 |
have ih:"\<And> y s \<theta>. y\<sharp>\<theta> \<Longrightarrow> ((\<theta><(t[y::=s])>) = ((\<theta><t>)[y::=(\<theta><s>)]))" by fact |
|
825 |
have "\<theta> <(Lam [n].t)[x::=u]> = \<theta><Lam [n]. (t [x::=u])>" using fs by auto |
|
826 |
then have "\<theta> <(Lam [n].t)[x::=u]> = Lam [n]. \<theta><t [x::=u]>" using fs by auto |
|
827 |
moreover have "\<theta><t[x::=u]> = \<theta><t>[x::=\<theta><u>]" using ih fs by blast |
|
828 |
ultimately have "\<theta> <(Lam [n].t)[x::=u]> = Lam [n].(\<theta><t>[x::=\<theta><u>])" by auto |
|
829 |
moreover have "Lam [n].(\<theta><t>[x::=\<theta><u>]) = (Lam [n].\<theta><t>)[x::=\<theta><u>]" using fs fresh_psubst by auto |
|
830 |
ultimately have "\<theta><(Lam [n].t)[x::=u]> = (Lam [n].\<theta><t>)[x::=\<theta><u>]" using fs by auto |
|
831 |
then show "\<theta><(Lam [n].t)[x::=u]> = \<theta><Lam [n].t>[x::=\<theta><u>]" using fs by auto |
|
832 |
qed (auto) |
|
833 |
||
834 |
lemma fresh_subst_fresh: |
|
835 |
assumes "a\<sharp>e" |
|
836 |
shows "a\<sharp>t[a::=e]" |
|
837 |
using assms |
|
838 |
by (nominal_induct t avoiding: a e rule: trm.induct) |
|
839 |
(auto simp add: fresh_atm abs_fresh fresh_nat) |
|
840 |
||
841 |
lemma path_equiv_implies_nf: |
|
842 |
assumes "\<Gamma> \<turnstile> s \<leftrightarrow> t : T" |
|
843 |
shows "s \<leadsto>|" and "t \<leadsto>|" |
|
844 |
using assms |
|
22082 | 845 |
by (induct rule: alg_equiv_alg_path_equiv.inducts(2)) (simp, auto) |
22073 | 846 |
|
847 |
lemma path_equiv_implies_nf: |
|
848 |
shows "\<Gamma> \<turnstile> s <=> t : T \<Longrightarrow> True" |
|
849 |
and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> s \<leadsto>|" |
|
850 |
"\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> t \<leadsto>|" |
|
22082 | 851 |
by (induct rule: alg_equiv_alg_path_equiv.inducts) (auto) |
22073 | 852 |
|
853 |
lemma main_lemma: |
|
854 |
shows "\<Gamma> \<turnstile> s is t : T \<Longrightarrow> \<Gamma> \<turnstile> s <=> t : T" and "\<Gamma> \<turnstile> p \<leftrightarrow> q : T \<Longrightarrow> \<Gamma> \<turnstile> p is q : T" |
|
855 |
proof (nominal_induct T arbitrary: \<Gamma> s t p q rule:ty.induct) |
|
856 |
case (Arrow T1 T2) |
|
857 |
{ |
|
858 |
case (1 \<Gamma> s t) |
|
859 |
have ih1:"\<And>\<Gamma> s t. \<Gamma> \<turnstile> s is t : T2 \<Longrightarrow> \<Gamma> \<turnstile> s <=> t : T2" by fact |
|
860 |
have ih2:"\<And>\<Gamma> s t. \<Gamma> \<turnstile> s \<leftrightarrow> t : T1 \<Longrightarrow> \<Gamma> \<turnstile> s is t : T1" by fact |
|
861 |
have h:"\<Gamma> \<turnstile> s is t : T1\<rightarrow>T2" by fact |
|
862 |
obtain x::name where fs:"x\<sharp>(\<Gamma>,s,t)" by (erule exists_fresh[OF fs_name1]) |
|
863 |
have "valid \<Gamma>" using h log_equiv_valid by auto |
|
864 |
then have v:"valid ((x,T1)#\<Gamma>)" using fs by auto |
|
865 |
then have "(x,T1)#\<Gamma> \<turnstile> Var x \<leftrightarrow> Var x : T1" by auto |
|
866 |
then have "(x,T1)#\<Gamma> \<turnstile> Var x is Var x : T1" using ih2 by auto |
|
867 |
then have "(x,T1)#\<Gamma> \<turnstile> App s (Var x) is App t (Var x) : T2" using h v by auto |
|
868 |
then have "(x,T1)#\<Gamma> \<turnstile> App s (Var x) <=> App t (Var x) : T2" using ih1 by auto |
|
869 |
then show "\<Gamma> \<turnstile> s <=> t : T1\<rightarrow>T2" using fs by (auto simp add: fresh_prod) |
|
870 |
next |
|
871 |
case (2 \<Gamma> p q) |
|
872 |
have h:"\<Gamma> \<turnstile> p \<leftrightarrow> q : T1\<rightarrow>T2" by fact |
|
873 |
have ih1:"\<And>\<Gamma> s t. \<Gamma> \<turnstile> s \<leftrightarrow> t : T2 \<Longrightarrow> \<Gamma> \<turnstile> s is t : T2" by fact |
|
874 |
have ih2:"\<And>\<Gamma> s t. \<Gamma> \<turnstile> s is t : T1 \<Longrightarrow> \<Gamma> \<turnstile> s <=> t : T1" by fact |
|
875 |
{ |
|
876 |
fix \<Gamma>' s t |
|
877 |
assume "\<Gamma>\<lless>\<Gamma>'" and hl:"\<Gamma>' \<turnstile> s is t : T1" |
|
878 |
then have "\<Gamma>' \<turnstile> p \<leftrightarrow> q : T1 \<rightarrow> T2" using h algorithmic_monotonicity by auto |
|
879 |
moreover have "\<Gamma>' \<turnstile> s <=> t : T1" using ih2 hl by auto |
|
880 |
ultimately have "\<Gamma>' \<turnstile> App p s \<leftrightarrow> App q t : T2" by auto |
|
881 |
then have "\<Gamma>' \<turnstile> App p s is App q t : T2" using ih1 by auto |
|
882 |
} |
|
883 |
moreover have "valid \<Gamma>" using h alg_equiv_valid by auto |
|
884 |
ultimately show "\<Gamma> \<turnstile> p is q : T1\<rightarrow>T2" by auto |
|
885 |
} |
|
886 |
next |
|
887 |
case TBase |
|
888 |
{ case 2 |
|
889 |
have h:"\<Gamma> \<turnstile> s \<leftrightarrow> t : TBase" by fact |
|
890 |
then have "s \<leadsto>|" and "t \<leadsto>|" using path_equiv_implies_nf by auto |
|
891 |
then have "s \<Down> s" and "t \<Down> t" by auto |
|
892 |
then have "\<Gamma> \<turnstile> s <=> t : TBase" using h by auto |
|
893 |
then show "\<Gamma> \<turnstile> s is t : TBase" by auto |
|
894 |
} |
|
895 |
qed (auto elim:alg_equiv_valid) |
|
896 |
||
897 |
corollary corollary_main: |
|
22082 | 898 |
assumes a: "\<Gamma> \<turnstile> s \<leftrightarrow> t : T" |
22073 | 899 |
shows "\<Gamma> \<turnstile> s <=> t : T" |
22082 | 900 |
using a main_lemma by blast |
22073 | 901 |
|
902 |
lemma algorithmic_symmetry_aux: |
|
22082 | 903 |
shows "\<Gamma> \<turnstile> s <=> t : T \<Longrightarrow> \<Gamma> \<turnstile> t <=> s : T" |
904 |
and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<leftrightarrow> s : T" |
|
905 |
by (induct rule: alg_equiv_alg_path_equiv.inducts) (auto) |
|
22073 | 906 |
|
907 |
lemma algorithmic_symmetry: |
|
22082 | 908 |
assumes a: "\<Gamma> \<turnstile> s <=> t : T" |
22073 | 909 |
shows "\<Gamma> \<turnstile> t <=> s : T" |
22082 | 910 |
using a by (simp add: algorithmic_symmetry_aux) |
22073 | 911 |
|
912 |
lemma algorithmic_path_symmetry: |
|
22082 | 913 |
assumes a: "\<Gamma> \<turnstile> s \<leftrightarrow> t : T" |
22073 | 914 |
shows "\<Gamma> \<turnstile> t \<leftrightarrow> s : T" |
22082 | 915 |
using a by (simp add: algorithmic_symmetry_aux) |
22073 | 916 |
|
917 |
lemma red_unicity : |
|
22082 | 918 |
assumes a: "x \<leadsto> a" |
919 |
and b: "x \<leadsto> b" |
|
22073 | 920 |
shows "a=b" |
22082 | 921 |
using a b |
22073 | 922 |
apply (induct arbitrary: b) |
923 |
apply (erule whr_App_Lam) |
|
924 |
apply (clarify) |
|
925 |
apply (rule subst_fun_eq) |
|
22082 | 926 |
apply (simp) |
22073 | 927 |
apply (force) |
928 |
apply (erule whr_App) |
|
929 |
apply (blast)+ |
|
930 |
done |
|
931 |
||
932 |
lemma nf_unicity : |
|
933 |
assumes "x \<Down> a" "x \<Down> b" |
|
934 |
shows "a=b" |
|
935 |
using assms |
|
936 |
proof (induct arbitrary: b) |
|
937 |
case (QAN_Reduce x t a b) |
|
938 |
have h:"x \<leadsto> t" "t \<Down> a" by fact |
|
939 |
have ih:"\<And>b. t \<Down> b \<Longrightarrow> a = b" by fact |
|
940 |
have "x \<Down> b" by fact |
|
941 |
then obtain t' where "x \<leadsto> t'" and hl:"t' \<Down> b" using h by auto |
|
942 |
then have "t=t'" using h red_unicity by auto |
|
943 |
then show "a=b" using ih hl by auto |
|
944 |
qed (auto) |
|
945 |
||
946 |
lemma Q_eqvt : |
|
22082 | 947 |
fixes pi:: "name prm" |
22073 | 948 |
shows "\<Gamma> \<turnstile> s <=> t : T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>s) <=> (pi\<bullet>t) : T" |
949 |
and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>s) \<leftrightarrow> (pi\<bullet>t) : T" |
|
950 |
using assms |
|
951 |
proof (induct rule:alg_equiv_alg_path_equiv.inducts) |
|
952 |
case (QAP_Var \<Gamma> x T) |
|
953 |
then have "pi\<bullet>(x,T) \<in> (pi\<bullet>(set \<Gamma>))" using in_eqvt by blast |
|
954 |
then have "(pi\<bullet>x,T) \<in> (set (pi\<bullet>\<Gamma>))" using set_eqvt perm_ty by auto |
|
955 |
moreover have "valid \<Gamma>" by fact |
|
956 |
ultimately show ?case using valid_eqvt by auto |
|
957 |
next |
|
958 |
case (QAT_Arrow x \<Gamma> s t T1 T2) |
|
959 |
then have h:"((pi\<bullet>x)\<sharp>(pi\<bullet>\<Gamma>))" "((pi\<bullet>x)\<sharp>(pi\<bullet>s))" "((pi\<bullet>x)\<sharp>(pi\<bullet>t))" using fresh_bij by auto |
|
960 |
have "(pi\<bullet>((x,T1)#\<Gamma>)) \<turnstile> pi \<bullet> (App s (Var x)) <=> pi \<bullet> (App t (Var x)) : T2" by fact |
|
961 |
then have "(pi\<bullet>((x,T1)#\<Gamma>)) \<turnstile> (App (pi\<bullet>s) (Var (pi\<bullet>x))) <=> (App (pi\<bullet>t) (Var (pi\<bullet>x))) : T2" by auto |
|
962 |
moreover have "pi\<bullet>((x,T1)#\<Gamma>) = (pi\<bullet>x,pi\<bullet>T1)#(pi\<bullet>\<Gamma>)" by auto |
|
22231
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
963 |
ultimately have "((pi\<bullet>x,T1)#(pi\<bullet>\<Gamma>)) \<turnstile> (App (pi\<bullet>s) (Var (pi\<bullet>x))) <=> (App (pi\<bullet>t) (Var (pi\<bullet>x))) : T2" |
f76f187c91f9
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
urbanc
parents:
22082
diff
changeset
|
964 |
using perm_ty by auto |
22073 | 965 |
then show ?case using h by auto |
966 |
qed (auto elim:whn_eqvt valid_eqvt) |
|
967 |
||
968 |
(* FIXME this lemma should not be here I am reinventing the wheel I guess *) |
|
969 |
||
970 |
lemma perm_basic[simp]: |
|
22082 | 971 |
fixes x y::"name" |
22073 | 972 |
shows "[(x,y)]\<bullet>y = x" |
973 |
using assms using calc_atm by perm_simp |
|
974 |
||
975 |
lemma Q_Arrow_strong_inversion: |
|
976 |
assumes fs:"x\<sharp>\<Gamma>" "x\<sharp>t" "x\<sharp>u" and h:"\<Gamma> \<turnstile> t <=> u : T1\<rightarrow>T2" |
|
977 |
shows "(x,T1)#\<Gamma> \<turnstile> App t (Var x) <=> App u (Var x) : T2" |
|
978 |
proof - |
|
22082 | 979 |
obtain y where fs2:"y\<sharp>\<Gamma>" "y\<sharp>u" "y\<sharp>t" and "(y,T1)#\<Gamma> \<turnstile> App t (Var y) <=> App u (Var y) : T2" |
980 |
using h by auto |
|
981 |
then have "([(x,y)]\<bullet>((y,T1)#\<Gamma>)) \<turnstile> [(x,y)]\<bullet> App t (Var y) <=> [(x,y)]\<bullet> App u (Var y) : T2" |
|
982 |
using Q_eqvt by blast |
|
983 |
then show ?thesis using fs fs2 by (perm_simp) |
|
22073 | 984 |
qed |
985 |
||
22082 | 986 |
lemma fresh_context: |
987 |
fixes \<Gamma> :: "(name\<times>ty) list" |
|
22073 | 988 |
and a :: "name" |
989 |
assumes "a\<sharp>\<Gamma>" |
|
990 |
shows "\<not>(\<exists>\<tau>::ty. (a,\<tau>)\<in>set \<Gamma>)" |
|
991 |
using assms by(induct \<Gamma>, auto simp add: fresh_prod fresh_list_cons fresh_atm) |
|
992 |
||
993 |
lemma type_unicity_in_context: |
|
994 |
fixes \<Gamma> :: "(name\<times>ty)list" |
|
995 |
and pi:: "name prm" |
|
996 |
and a :: "name" |
|
997 |
and \<tau> :: "ty" |
|
998 |
assumes "valid \<Gamma>" and "(x,T1) \<in> set \<Gamma>" and "(x,T2) \<in> set \<Gamma>" |
|
999 |
shows "T1=T2" |
|
1000 |
using assms by (induct \<Gamma>, auto dest!: fresh_context) |
|
1001 |
||
1002 |
(* |
|
1003 |
||
1004 |
Warning: This lemma is false. |
|
1005 |
||
1006 |
lemma algorithmic_type_unicity: |
|
1007 |
shows "\<lbrakk> \<Gamma> \<turnstile> s <=> t : T ; \<Gamma> \<turnstile> s <=> u : T' \<rbrakk> \<Longrightarrow> T = T'" |
|
1008 |
and "\<lbrakk> \<Gamma> \<turnstile> s \<leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'" |
|
1009 |
||
1010 |
Here is the counter example : |
|
1011 |
\<Gamma> \<turnstile> Const n <=> Const n : Tbase and \<Gamma> \<turnstile> Const n <=> Const n : TUnit |
|
1012 |
||
1013 |
*) |
|
1014 |
||
1015 |
lemma algorithmic_path_type_unicity: |
|
1016 |
shows "\<lbrakk> \<Gamma> \<turnstile> s \<leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'" |
|
22082 | 1017 |
proof (induct arbitrary: u T' |
1018 |
rule: alg_equiv_alg_path_equiv.inducts(2) [of _ _ _ _ _ "%a b c d . True" ]) |
|
22073 | 1019 |
case (QAP_Var \<Gamma> x T u T') |
1020 |
have "\<Gamma> \<turnstile> Var x \<leftrightarrow> u : T'" by fact |
|
1021 |
then have "u=Var x" and "(x,T') \<in> set \<Gamma>" by auto |
|
1022 |
moreover have "valid \<Gamma>" "(x,T) \<in> set \<Gamma>" by fact |
|
1023 |
ultimately show "T=T'" using type_unicity_in_context by auto |
|
1024 |
next |
|
1025 |
case (QAP_App \<Gamma> p q T1 T2 s t u T2') |
|
1026 |
have ih:"\<And>u T. \<Gamma> \<turnstile> p \<leftrightarrow> u : T \<Longrightarrow> T1\<rightarrow>T2 = T" by fact |
|
1027 |
have "\<Gamma> \<turnstile> App p s \<leftrightarrow> u : T2'" by fact |
|
1028 |
then obtain r t T1' where "u = App r t" "\<Gamma> \<turnstile> p \<leftrightarrow> r : T1' \<rightarrow> T2'" by auto |
|
1029 |
then have "T1\<rightarrow>T2 = T1' \<rightarrow> T2'" by auto |
|
1030 |
then show "T2=T2'" using ty.inject by auto |
|
1031 |
qed (auto) |
|
1032 |
||
1033 |
lemma algorithmic_transitivity: |
|
1034 |
shows "\<lbrakk> \<Gamma> \<turnstile> s <=> t : T ; \<Gamma> \<turnstile> t <=> u : T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s <=> u : T" |
|
1035 |
and "\<lbrakk> \<Gamma> \<turnstile> s \<leftrightarrow> t : T ; \<Gamma> \<turnstile> t \<leftrightarrow> u : T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<leftrightarrow> u : T" |
|
1036 |
proof (nominal_induct \<Gamma> s t T and \<Gamma> s t T avoiding: u rule: alg_equiv_alg_path_equiv_strong_inducts) |
|
1037 |
case (QAT_Base s p t q \<Gamma> u) |
|
1038 |
have h:"s \<Down> p" "t \<Down> q" by fact |
|
1039 |
have ih:"\<And>u. \<Gamma> \<turnstile> q \<leftrightarrow> u : TBase \<Longrightarrow> \<Gamma> \<turnstile> p \<leftrightarrow> u : TBase" by fact |
|
1040 |
have "\<Gamma> \<turnstile> t <=> u : TBase" by fact |
|
1041 |
then obtain r q' where hl:"t \<Down> q'" "u \<Down> r" "\<Gamma> \<turnstile> q' \<leftrightarrow> r : TBase" by auto |
|
1042 |
moreover have eq:"q=q'" using nf_unicity hl h by auto |
|
1043 |
ultimately have "\<Gamma> \<turnstile> p \<leftrightarrow> r : TBase" using ih by auto |
|
1044 |
then show "\<Gamma> \<turnstile> s <=> u : TBase" using hl h by auto |
|
1045 |
next |
|
1046 |
case (QAT_Arrow x \<Gamma> s t T1 T2 u) |
|
1047 |
have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact |
|
1048 |
moreover have h:"\<Gamma> \<turnstile> t <=> u : T1\<rightarrow>T2" by fact |
|
22082 | 1049 |
moreover then obtain y where "y\<sharp>\<Gamma>" "y\<sharp>t" "y\<sharp>u" and "(y,T1)#\<Gamma> \<turnstile> App t (Var y) <=> App u (Var y) : T2" |
1050 |
by auto |
|
22073 | 1051 |
moreover have fs2:"x\<sharp>u" by fact |
1052 |
ultimately have "(x,T1)#\<Gamma> \<turnstile> App t (Var x) <=> App u (Var x) : T2" using Q_Arrow_strong_inversion by blast |
|
22082 | 1053 |
moreover have ih:"\<And> v. (x,T1)#\<Gamma> \<turnstile> App t (Var x) <=> v : T2 \<Longrightarrow> (x,T1)#\<Gamma> \<turnstile> App s (Var x) <=> v : T2" |
1054 |
by fact |
|
22073 | 1055 |
ultimately have "(x,T1)#\<Gamma> \<turnstile> App s (Var x) <=> App u (Var x) : T2" by auto |
1056 |
then show "\<Gamma> \<turnstile> s <=> u : T1\<rightarrow>T2" using fs fs2 by auto |
|
1057 |
next |
|
1058 |
case (QAP_App \<Gamma> p q T1 T2 s t u) |
|
1059 |
have h1:"\<Gamma> \<turnstile> p \<leftrightarrow> q : T1\<rightarrow>T2" by fact |
|
1060 |
have ih1:"\<And>u. \<Gamma> \<turnstile> q \<leftrightarrow> u : T1\<rightarrow>T2 \<Longrightarrow> \<Gamma> \<turnstile> p \<leftrightarrow> u : T1\<rightarrow>T2" by fact |
|
1061 |
have "\<Gamma> \<turnstile> s <=> t : T1" by fact |
|
1062 |
have ih2:"\<And>u. \<Gamma> \<turnstile> t <=> u : T1 \<Longrightarrow> \<Gamma> \<turnstile> s <=> u : T1" by fact |
|
1063 |
have "\<Gamma> \<turnstile> App q t \<leftrightarrow> u : T2" by fact |
|
22082 | 1064 |
then obtain r T1' v where ha:"\<Gamma> \<turnstile> q \<leftrightarrow> r : T1'\<rightarrow>T2" and hb:"\<Gamma> \<turnstile> t <=> v : T1'" and eq:"u = App r v" |
1065 |
by auto |
|
22073 | 1066 |
moreover have "\<Gamma> \<turnstile> q \<leftrightarrow> p : T1\<rightarrow>T2" using h1 algorithmic_path_symmetry by auto |
1067 |
ultimately have "T1'\<rightarrow>T2 = T1\<rightarrow>T2" using algorithmic_path_type_unicity by auto |
|
1068 |
then have "T1' = T1" using ty.inject by auto |
|
1069 |
then have "\<Gamma> \<turnstile> s <=> v : T1" "\<Gamma> \<turnstile> p \<leftrightarrow> r : T1\<rightarrow>T2" using ih1 ih2 ha hb by auto |
|
1070 |
then show "\<Gamma> \<turnstile> App p s \<leftrightarrow> u : T2" using eq by auto |
|
1071 |
qed (auto) |
|
1072 |
||
1073 |
lemma algorithmic_weak_head_closure: |
|
1074 |
shows "\<lbrakk>\<Gamma> \<turnstile> s <=> t : T ; s' \<leadsto> s; t' \<leadsto> t\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s' <=> t' : T" |
|
1075 |
by (nominal_induct \<Gamma> s t T avoiding: s' t' |
|
1076 |
rule: alg_equiv_alg_path_equiv_strong_inducts(1) [of _ _ _ _ "%a b c d e. True"]) |
|
1077 |
(auto) |
|
1078 |
||
1079 |
lemma logical_symmetry: |
|
22082 | 1080 |
assumes a: "\<Gamma> \<turnstile> s is t : T" |
22073 | 1081 |
shows "\<Gamma> \<turnstile> t is s : T" |
22082 | 1082 |
using a |
1083 |
by (nominal_induct arbitrary: \<Gamma> s t rule:ty.induct) (auto simp add: algorithmic_symmetry) |
|
22073 | 1084 |
|
1085 |
lemma logical_transitivity: |
|
1086 |
assumes "\<Gamma> \<turnstile> s is t : T" "\<Gamma> \<turnstile> t is u : T" |
|
1087 |
shows "\<Gamma> \<turnstile> s is u : T" |
|
1088 |
using assms |
|
1089 |
proof (nominal_induct arbitrary: \<Gamma> s t u rule:ty.induct) |
|
1090 |
case TBase |
|
1091 |
then show "\<Gamma> \<turnstile> s is u : TBase" by (auto elim: algorithmic_transitivity) |
|
1092 |
next |
|
1093 |
case (Arrow T1 T2 \<Gamma> s t u) |
|
1094 |
have h1:"\<Gamma> \<turnstile> s is t : T1 \<rightarrow> T2" by fact |
|
1095 |
have h2:"\<Gamma> \<turnstile> t is u : T1 \<rightarrow> T2" by fact |
|
1096 |
have ih1:"\<And>\<Gamma> s t u. \<lbrakk>\<Gamma> \<turnstile> s is t : T1; \<Gamma> \<turnstile> t is u : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s is u : T1" by fact |
|
1097 |
have ih2:"\<And>\<Gamma> s t u. \<lbrakk>\<Gamma> \<turnstile> s is t : T2; \<Gamma> \<turnstile> t is u : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s is u : T2" by fact |
|
1098 |
{ |
|
1099 |
fix \<Gamma>' s' u' |
|
1100 |
assume hsub:"\<Gamma>\<lless>\<Gamma>'" and hl:"\<Gamma>' \<turnstile> s' is u' : T1" |
|
1101 |
then have "\<Gamma>' \<turnstile> u' is s' : T1" using logical_symmetry by blast |
|
1102 |
then have "\<Gamma>' \<turnstile> u' is u' : T1" using ih1 hl by blast |
|
1103 |
then have "\<Gamma>' \<turnstile> App t u' is App u u' : T2" using h2 hsub by auto |
|
1104 |
moreover have "\<Gamma>' \<turnstile> App s s' is App t u' : T2" using h1 hsub hl by auto |
|
1105 |
ultimately have "\<Gamma>' \<turnstile> App s s' is App u u' : T2" using ih2 by blast |
|
1106 |
} |
|
1107 |
moreover have "valid \<Gamma>" using h1 alg_equiv_valid by auto |
|
1108 |
ultimately show "\<Gamma> \<turnstile> s is u : T1 \<rightarrow> T2" by auto |
|
1109 |
qed (auto) |
|
1110 |
||
1111 |
lemma logical_weak_head_closure: |
|
22082 | 1112 |
assumes a: "\<Gamma> \<turnstile> s is t : T" "s' \<leadsto> s" "t' \<leadsto> t" |
22073 | 1113 |
shows "\<Gamma> \<turnstile> s' is t' : T" |
22082 | 1114 |
using a |
1115 |
apply(nominal_induct arbitrary: \<Gamma> s t s' t' rule:ty.induct) |
|
1116 |
apply(auto simp add: algorithmic_weak_head_closure) |
|
1117 |
apply(blast) |
|
22073 | 1118 |
done |
1119 |
||
1120 |
lemma logical_weak_head_closure': |
|
1121 |
assumes "\<Gamma> \<turnstile> s is t : T" "s' \<leadsto> s" |
|
1122 |
shows "\<Gamma> \<turnstile> s' is t : T" |
|
1123 |
using assms |
|
22082 | 1124 |
proof (nominal_induct arbitrary: \<Gamma> s t s' rule: ty.induct) |
22073 | 1125 |
case (TBase \<Gamma> s t s') |
1126 |
then show ?case by force |
|
1127 |
next |
|
1128 |
case (TUnit \<Gamma> s t s') |
|
1129 |
then show ?case by auto |
|
1130 |
next |
|
1131 |
case (Arrow T1 T2 \<Gamma> s t s') |
|
1132 |
have h1:"s' \<leadsto> s" by fact |
|
1133 |
have ih:"\<And>\<Gamma> s t s'. \<lbrakk>\<Gamma> \<turnstile> s is t : T2; s' \<leadsto> s\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s' is t : T2" by fact |
|
1134 |
have h2:"\<Gamma> \<turnstile> s is t : T1\<rightarrow>T2" by fact |
|
1135 |
then have hb:"\<forall>\<Gamma>' s' t'. \<Gamma>\<lless>\<Gamma>' \<longrightarrow> \<Gamma>' \<turnstile> s' is t' : T1 \<longrightarrow> (\<Gamma>' \<turnstile> (App s s') is (App t t') : T2)" by auto |
|
1136 |
{ |
|
1137 |
fix \<Gamma>' s2 t2 |
|
1138 |
assume "\<Gamma>\<lless>\<Gamma>'" and "\<Gamma>' \<turnstile> s2 is t2 : T1" |
|
1139 |
then have "\<Gamma>' \<turnstile> (App s s2) is (App t t2) : T2" using hb by auto |
|
1140 |
moreover have "(App s' s2) \<leadsto> (App s s2)" using h1 by auto |
|
1141 |
ultimately have "\<Gamma>' \<turnstile> App s' s2 is App t t2 : T2" using ih by auto |
|
1142 |
} |
|
1143 |
moreover have "valid \<Gamma>" using h2 log_equiv_valid by auto |
|
1144 |
ultimately show "\<Gamma> \<turnstile> s' is t : T1\<rightarrow>T2" by auto |
|
1145 |
qed |
|
1146 |
||
1147 |
abbreviation |
|
1148 |
log_equiv_subst :: "(name\<times>ty) list \<Rightarrow> (name\<times>trm) list \<Rightarrow> (name\<times>trm) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" |
|
1149 |
("_ \<turnstile> _ is _ over _" [60,60] 60) |
|
1150 |
where |
|
1151 |
"\<Gamma>' \<turnstile> \<gamma> is \<delta> over \<Gamma> \<equiv> valid \<Gamma>' \<and> (\<forall> x T. (x,T) \<in> set \<Gamma> \<longrightarrow> \<Gamma>' \<turnstile> \<gamma><Var x> is \<delta><Var x> : T)" |
|
1152 |
||
1153 |
lemma logical_pseudo_reflexivity: |
|
1154 |
assumes "\<Gamma>' \<turnstile> t is s over \<Gamma>" |
|
1155 |
shows "\<Gamma>' \<turnstile> s is s over \<Gamma>" |
|
1156 |
proof - |
|
1157 |
have "\<Gamma>' \<turnstile> t is s over \<Gamma>" by fact |
|
1158 |
moreover then have "\<Gamma>' \<turnstile> s is t over \<Gamma>" using logical_symmetry by blast |
|
1159 |
ultimately show "\<Gamma>' \<turnstile> s is s over \<Gamma>" using logical_transitivity by blast |
|
1160 |
qed |
|
1161 |
||
1162 |
lemma logical_subst_monotonicity : |
|
1163 |
fixes \<Gamma>::"(name\<times>ty) list" |
|
1164 |
and \<Gamma>'::"(name\<times>ty) list" |
|
1165 |
and \<Gamma>''::"(name\<times>ty) list" |
|
1166 |
assumes "\<Gamma>' \<turnstile> s is t over \<Gamma>" "\<Gamma>'\<lless>\<Gamma>''" |
|
1167 |
shows "\<Gamma>'' \<turnstile> s is t over \<Gamma>" |
|
1168 |
using assms logical_monotonicity by blast |
|
1169 |
||
1170 |
lemma equiv_subst_ext : |
|
1171 |
assumes h1:"\<Gamma>' \<turnstile> \<gamma> is \<delta> over \<Gamma>" and h2:"\<Gamma>' \<turnstile> s is t : T" and fs:"x\<sharp>\<Gamma>" |
|
1172 |
shows "\<Gamma>' \<turnstile> (x,s)#\<gamma> is (x,t)#\<delta> over (x,T)#\<Gamma>" |
|
1173 |
using assms |
|
1174 |
proof - |
|
1175 |
{ |
|
1176 |
fix y U |
|
1177 |
assume "(y,U) \<in> set ((x,T)#\<Gamma>)" |
|
1178 |
moreover |
|
1179 |
{ |
|
1180 |
assume "(y,U) \<in> set [(x,T)]" |
|
1181 |
then have "\<Gamma>' \<turnstile> (x,s)#\<gamma><Var y> is (x,t)#\<delta><Var y> : U" by auto |
|
1182 |
} |
|
1183 |
moreover |
|
1184 |
{ |
|
1185 |
assume hl:"(y,U) \<in> set \<Gamma>" |
|
1186 |
then have "\<not> y\<sharp>\<Gamma>" by (induct \<Gamma>) (auto simp add: fresh_list_cons fresh_atm fresh_prod) |
|
1187 |
then have hf:"x\<sharp> Var y" using fs by (auto simp add: fresh_atm) |
|
1188 |
then have "(x,s)#\<gamma><Var y> = \<gamma><Var y>" "(x,t)#\<delta><Var y> = \<delta><Var y>" using fresh_psubst_simpl by blast+ |
|
1189 |
moreover have "\<Gamma>' \<turnstile> \<gamma><Var y> is \<delta><Var y> : U" using h1 hl by auto |
|
1190 |
ultimately have "\<Gamma>' \<turnstile> (x,s)#\<gamma><Var y> is (x,t)#\<delta><Var y> : U" by auto |
|
1191 |
} |
|
1192 |
ultimately have "\<Gamma>' \<turnstile> (x,s)#\<gamma><Var y> is (x,t)#\<delta><Var y> : U" by auto |
|
1193 |
} |
|
1194 |
moreover have "valid \<Gamma>'" using h2 log_equiv_valid by blast |
|
1195 |
ultimately show "\<Gamma>' \<turnstile> (x,s)#\<gamma> is (x,t)#\<delta> over (x,T)#\<Gamma>" by auto |
|
1196 |
qed |
|
1197 |
||
1198 |
theorem fundamental_theorem: |
|
1199 |
assumes "\<Gamma> \<turnstile> t : T" "\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" |
|
1200 |
shows "\<Gamma>' \<turnstile> \<gamma><t> is \<theta><t> : T" |
|
1201 |
using assms |
|
1202 |
proof (nominal_induct avoiding:\<Gamma>' \<gamma> \<theta> rule: typing_induct_strong) |
|
1203 |
case (t_Lam x \<Gamma> T1 t2 T2 \<Gamma>' \<gamma> \<theta>) |
|
1204 |
have fs:"x\<sharp>\<gamma>" "x\<sharp>\<theta>" "x\<sharp>\<Gamma>" by fact |
|
1205 |
have h:"\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact |
|
1206 |
have ih:"\<And> \<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over (x,T1)#\<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><t2> is \<theta><t2> : T2" by fact |
|
1207 |
{ |
|
1208 |
fix \<Gamma>'' s' t' |
|
1209 |
assume "\<Gamma>'\<lless>\<Gamma>''" and hl:"\<Gamma>''\<turnstile> s' is t' : T1" |
|
1210 |
then have "\<Gamma>'' \<turnstile> \<gamma> is \<theta> over \<Gamma>" using logical_subst_monotonicity h by blast |
|
1211 |
then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma> is (x,t')#\<theta> over (x,T1)#\<Gamma>" using equiv_subst_ext hl fs by blast |
|
1212 |
then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma><t2> is (x,t')#\<theta><t2> : T2" using ih by auto |
|
1213 |
then have "\<Gamma>''\<turnstile>\<gamma><t2>[x::=s'] is \<theta><t2>[x::=t'] : T2" using psubst_subst_psubst fs by simp |
|
1214 |
moreover have "App (Lam [x].\<gamma><t2>) s' \<leadsto> \<gamma><t2>[x::=s']" by auto |
|
1215 |
moreover have "App (Lam [x].\<theta><t2>) t' \<leadsto> \<theta><t2>[x::=t']" by auto |
|
1216 |
ultimately have "\<Gamma>''\<turnstile> App (Lam [x].\<gamma><t2>) s' is App (Lam [x].\<theta><t2>) t' : T2" |
|
1217 |
using logical_weak_head_closure by auto |
|
1218 |
} |
|
1219 |
moreover have "valid \<Gamma>'" using h by auto |
|
1220 |
ultimately show "\<Gamma>' \<turnstile> \<gamma><Lam [x].t2> is \<theta><Lam [x].t2> : T1\<rightarrow>T2" using fs by auto |
|
1221 |
qed (auto) |
|
1222 |
||
1223 |
theorem fundamental_theorem_2: |
|
1224 |
assumes h1: "\<Gamma> \<turnstile> s == t : T" |
|
1225 |
and h2: "\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" |
|
1226 |
shows "\<Gamma>' \<turnstile> \<gamma><s> is \<theta><t> : T" |
|
1227 |
using h1 h2 |
|
1228 |
proof (nominal_induct \<Gamma> s t T avoiding: \<Gamma>' \<gamma> \<theta> rule: equiv_def_strong_induct) |
|
1229 |
case (Q_Refl \<Gamma> t T \<Gamma>' \<gamma> \<theta>) |
|
1230 |
have "\<Gamma> \<turnstile> t : T" by fact |
|
1231 |
moreover have "\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact |
|
1232 |
ultimately show "\<Gamma>' \<turnstile> \<gamma><t> is \<theta><t> : T" using fundamental_theorem by blast |
|
1233 |
next |
|
1234 |
case (Q_Symm \<Gamma> t s T \<Gamma>' \<gamma> \<theta>) |
|
1235 |
have "\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact |
|
1236 |
moreover have ih:"\<And> \<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><t> is \<theta><s> : T" by fact |
|
1237 |
ultimately show "\<Gamma>' \<turnstile> \<gamma><s> is \<theta><t> : T" using logical_symmetry by blast |
|
1238 |
next |
|
1239 |
case (Q_Trans \<Gamma> s t T u \<Gamma>' \<gamma> \<theta>) |
|
1240 |
have ih1:"\<And> \<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><s> is \<theta><t> : T" by fact |
|
1241 |
have ih2:"\<And> \<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><t> is \<theta><u> : T" by fact |
|
1242 |
have h:"\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact |
|
1243 |
then have "\<Gamma>' \<turnstile> \<theta> is \<theta> over \<Gamma>" using logical_pseudo_reflexivity by auto |
|
1244 |
then have "\<Gamma>' \<turnstile> \<theta><t> is \<theta><u> : T" using ih2 by auto |
|
1245 |
moreover have "\<Gamma>' \<turnstile> \<gamma><s> is \<theta><t> : T" using ih1 h by auto |
|
1246 |
ultimately show "\<Gamma>' \<turnstile> \<gamma><s> is \<theta><u> : T" using logical_transitivity by blast |
|
1247 |
next |
|
1248 |
case (Q_Abs x \<Gamma> T1 s2 t2 T2 \<Gamma>' \<gamma> \<theta>) |
|
1249 |
have fs:"x\<sharp>\<Gamma>" by fact |
|
1250 |
have fs2: "x\<sharp>\<gamma>" "x\<sharp>\<theta>" by fact |
|
1251 |
have h2:"\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact |
|
1252 |
have ih:"\<And>\<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over (x,T1)#\<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><s2> is \<theta><t2> : T2" by fact |
|
1253 |
{ |
|
1254 |
fix \<Gamma>'' s' t' |
|
1255 |
assume "\<Gamma>'\<lless>\<Gamma>''" and hl:"\<Gamma>''\<turnstile> s' is t' : T1" |
|
1256 |
then have "\<Gamma>'' \<turnstile> \<gamma> is \<theta> over \<Gamma>" using h2 logical_subst_monotonicity by blast |
|
1257 |
then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma> is (x,t')#\<theta> over (x,T1)#\<Gamma>" using equiv_subst_ext hl fs by blast |
|
1258 |
then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma><s2> is (x,t')#\<theta><t2> : T2" using ih by blast |
|
1259 |
then have "\<Gamma>''\<turnstile> \<gamma><s2>[x::=s'] is \<theta><t2>[x::=t'] : T2" using fs2 psubst_subst_psubst by auto |
|
1260 |
moreover have "App (Lam [x]. \<gamma><s2>) s' \<leadsto> \<gamma><s2>[x::=s']" |
|
1261 |
and "App (Lam [x].\<theta><t2>) t' \<leadsto> \<theta><t2>[x::=t']" by auto |
|
1262 |
ultimately have "\<Gamma>'' \<turnstile> App (Lam [x]. \<gamma><s2>) s' is App (Lam [x].\<theta><t2>) t' : T2" |
|
1263 |
using logical_weak_head_closure by auto |
|
1264 |
} |
|
1265 |
moreover have "valid \<Gamma>'" using h2 by auto |
|
1266 |
ultimately have "\<Gamma>' \<turnstile> Lam [x].\<gamma><s2> is Lam [x].\<theta><t2> : T1\<rightarrow>T2" by auto |
|
1267 |
then show "\<Gamma>' \<turnstile> \<gamma><Lam [x].s2> is \<theta><Lam [x].t2> : T1\<rightarrow>T2" using fs2 by auto |
|
1268 |
next |
|
1269 |
case (Q_App \<Gamma> s1 t1 T1 T2 s2 t2 \<Gamma>' \<gamma> \<theta>) |
|
1270 |
then show "\<Gamma>' \<turnstile> \<gamma><App s1 s2> is \<theta><App t1 t2> : T2" by auto |
|
1271 |
next |
|
1272 |
case (Q_Beta x \<Gamma> T1 s12 t12 T2 s2 t2 \<Gamma>' \<gamma> \<theta>) |
|
1273 |
have h:"\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact |
|
1274 |
have fs:"x\<sharp>\<Gamma>" by fact |
|
1275 |
have fs2:"x\<sharp>\<gamma>" "x\<sharp>\<theta>" by fact |
|
1276 |
have ih1:"\<And>\<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><s2> is \<theta><t2> : T1" by fact |
|
1277 |
have ih2:"\<And>\<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over (x,T1)#\<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><s12> is \<theta><t12> : T2" by fact |
|
1278 |
have "\<Gamma>' \<turnstile> \<gamma><s2> is \<theta><t2> : T1" using ih1 h by auto |
|
1279 |
then have "\<Gamma>' \<turnstile> (x,\<gamma><s2>)#\<gamma> is (x,\<theta><t2>)#\<theta> over (x,T1)#\<Gamma>" using equiv_subst_ext h fs by blast |
|
1280 |
then have "\<Gamma>' \<turnstile> (x,\<gamma><s2>)#\<gamma><s12> is (x,\<theta><t2>)#\<theta><t12> : T2" using ih2 by auto |
|
1281 |
then have "\<Gamma>' \<turnstile> \<gamma><s12>[x::=\<gamma><s2>] is \<theta><t12>[x::=\<theta><t2>] : T2" using fs2 psubst_subst_psubst by auto |
|
1282 |
then have "\<Gamma>' \<turnstile> \<gamma><s12>[x::=\<gamma><s2>] is \<theta><t12[x::=t2]> : T2" using fs2 psubst_subst_propagate by auto |
|
1283 |
moreover have "App (Lam [x].\<gamma><s12>) (\<gamma><s2>) \<leadsto> \<gamma><s12>[x::=\<gamma><s2>]" by auto |
|
1284 |
ultimately have "\<Gamma>' \<turnstile> App (Lam [x].\<gamma><s12>) (\<gamma><s2>) is \<theta><t12[x::=t2]> : T2" |
|
1285 |
using logical_weak_head_closure' by auto |
|
1286 |
then show "\<Gamma>' \<turnstile> \<gamma><App (Lam [x].s12) s2> is \<theta><t12[x::=t2]> : T2" using fs2 by simp |
|
1287 |
next |
|
1288 |
case (Q_Ext x \<Gamma> s t T1 T2 \<Gamma>' \<gamma> \<theta>) |
|
1289 |
have h2:"\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact |
|
1290 |
have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact |
|
1291 |
have ih:"\<And>\<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over (x,T1)#\<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><App s (Var x)> is \<theta><App t (Var x)> : T2" |
|
1292 |
by fact |
|
1293 |
{ |
|
1294 |
fix \<Gamma>'' s' t' |
|
1295 |
assume hsub:"\<Gamma>'\<lless>\<Gamma>''" and hl:"\<Gamma>''\<turnstile> s' is t' : T1" |
|
1296 |
then have "\<Gamma>'' \<turnstile> \<gamma> is \<theta> over \<Gamma>" using h2 logical_subst_monotonicity by blast |
|
1297 |
then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma> is (x,t')#\<theta> over (x,T1)#\<Gamma>" using equiv_subst_ext hl fs by blast |
|
1298 |
then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma><App s (Var x)> is (x,t')#\<theta><App t (Var x)> : T2" using ih by blast |
|
22082 | 1299 |
then have "\<Gamma>'' \<turnstile> App (((x,s')#\<gamma>)<s>) (((x,s')#\<gamma>)<(Var x)>) is App ((x,t')#\<theta><t>) ((x,t')#\<theta><(Var x)>) : T2" |
1300 |
by auto |
|
22073 | 1301 |
then have "\<Gamma>'' \<turnstile> App ((x,s')#\<gamma><s>) s' is App ((x,t')#\<theta><t>) t' : T2" by auto |
1302 |
then have "\<Gamma>'' \<turnstile> App (\<gamma><s>) s' is App (\<theta><t>) t' : T2" using fs fresh_psubst_simpl by auto |
|
1303 |
} |
|
1304 |
moreover have "valid \<Gamma>'" using h2 by auto |
|
1305 |
ultimately show "\<Gamma>' \<turnstile> \<gamma><s> is \<theta><t> : T1\<rightarrow>T2" by auto |
|
1306 |
qed |
|
1307 |
||
1308 |
theorem completeness: |
|
1309 |
assumes "\<Gamma> \<turnstile> s == t : T" |
|
1310 |
shows "\<Gamma> \<turnstile> s <=> t : T" |
|
1311 |
using assms |
|
1312 |
proof - |
|
1313 |
{ |
|
1314 |
fix x T |
|
1315 |
assume "(x,T) \<in> set \<Gamma>" "valid \<Gamma>" |
|
1316 |
then have "\<Gamma> \<turnstile> Var x is Var x : T" using main_lemma by blast |
|
1317 |
} |
|
1318 |
moreover have "valid \<Gamma>" using equiv_def_valid assms by auto |
|
1319 |
ultimately have "\<Gamma> \<turnstile> [] is [] over \<Gamma>" by auto |
|
1320 |
then have "\<Gamma> \<turnstile> []<s> is []<t> : T" using fundamental_theorem_2 assms by blast |
|
1321 |
then have "\<Gamma> \<turnstile> s is t : T" by simp |
|
1322 |
then show "\<Gamma> \<turnstile> s <=> t : T" using main_lemma by simp |
|
1323 |
qed |
|
1324 |
||
22082 | 1325 |
(* Soundness is left as an exercise - like in the book - for the avid formalist |
22073 | 1326 |
|
1327 |
theorem soundness: |
|
22082 | 1328 |
shows "\<lbrakk>\<Gamma> \<turnstile> s <=> t : T; \<Gamma> \<turnstile> t : T; \<Gamma> \<turnstile> s : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s == t : T" |
1329 |
and "\<lbrakk>\<Gamma> \<turnstile> s \<leftrightarrow> t : T; \<Gamma> \<turnstile> t : T; \<Gamma> \<turnstile> s : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s == t : T" |
|
1330 |
||
22073 | 1331 |
*) |
1332 |
||
1333 |
end |
|
1334 |