author | wenzelm |
Fri, 18 Aug 2017 20:47:47 +0200 | |
changeset 66453 | cc19f7ca2ed6 |
parent 63167 | 0909deb8059b |
child 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
22073 | 1 |
(* *) |
22082 | 2 |
(* Formalisation of the chapter on Logical Relations *) |
3 |
(* and a Case Study in Equivalence Checking *) |
|
4 |
(* by Karl Crary from the book on Advanced Topics in *) |
|
5 |
(* Types and Programming Languages, MIT Press 2005 *) |
|
6 |
||
7 |
(* The formalisation was done by Julien Narboux and *) |
|
22594
33a690455f88
add a few details in the Fst and Snd cases of unicity proof
narboux
parents:
22542
diff
changeset
|
8 |
(* Christian Urban. *) |
22073 | 9 |
|
10 |
theory Crary |
|
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
63167
diff
changeset
|
11 |
imports "HOL-Nominal.Nominal" |
22073 | 12 |
begin |
13 |
||
14 |
atom_decl name |
|
15 |
||
22829
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22730
diff
changeset
|
16 |
nominal_datatype ty = |
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22730
diff
changeset
|
17 |
TBase |
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22730
diff
changeset
|
18 |
| TUnit |
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22730
diff
changeset
|
19 |
| Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100) |
22073 | 20 |
|
22829
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22730
diff
changeset
|
21 |
nominal_datatype trm = |
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22730
diff
changeset
|
22 |
Unit |
24070 | 23 |
| Var "name" ("Var _" [100] 100) |
22829
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22730
diff
changeset
|
24 |
| Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100) |
24070 | 25 |
| App "trm" "trm" ("App _ _" [110,110] 100) |
22829
f1db55c7534d
tuned some proofs and changed variable names in some definitions of Nominal.thy
urbanc
parents:
22730
diff
changeset
|
26 |
| Const "nat" |
22073 | 27 |
|
41798 | 28 |
type_synonym Ctxt = "(name\<times>ty) list" |
29 |
type_synonym Subst = "(name\<times>trm) list" |
|
22494 | 30 |
|
22073 | 31 |
|
32 |
lemma perm_ty[simp]: |
|
33 |
fixes T::"ty" |
|
34 |
and pi::"name prm" |
|
35 |
shows "pi\<bullet>T = T" |
|
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
26677
diff
changeset
|
36 |
by (induct T rule: ty.induct) (simp_all) |
22073 | 37 |
|
38 |
lemma fresh_ty[simp]: |
|
39 |
fixes x::"name" |
|
40 |
and T::"ty" |
|
41 |
shows "x\<sharp>T" |
|
42 |
by (simp add: fresh_def supp_def) |
|
43 |
||
44 |
lemma ty_cases: |
|
45 |
fixes T::ty |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
46 |
shows "(\<exists> T\<^sub>1 T\<^sub>2. T=T\<^sub>1\<rightarrow>T\<^sub>2) \<or> T=TUnit \<or> T=TBase" |
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
26677
diff
changeset
|
47 |
by (induct T rule:ty.induct) (auto) |
22073 | 48 |
|
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
28042
diff
changeset
|
49 |
instantiation ty :: size |
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
28042
diff
changeset
|
50 |
begin |
22073 | 51 |
|
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
28042
diff
changeset
|
52 |
nominal_primrec size_ty |
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
28042
diff
changeset
|
53 |
where |
22073 | 54 |
"size (TBase) = 1" |
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
28042
diff
changeset
|
55 |
| "size (TUnit) = 1" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
56 |
| "size (T\<^sub>1\<rightarrow>T\<^sub>2) = size T\<^sub>1 + size T\<^sub>2" |
22073 | 57 |
by (rule TrueI)+ |
58 |
||
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
28042
diff
changeset
|
59 |
instance .. |
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
28042
diff
changeset
|
60 |
|
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
28042
diff
changeset
|
61 |
end |
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
28042
diff
changeset
|
62 |
|
22073 | 63 |
lemma ty_size_greater_zero[simp]: |
64 |
fixes T::"ty" |
|
65 |
shows "size T > 0" |
|
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
26677
diff
changeset
|
66 |
by (nominal_induct rule: ty.strong_induct) (simp_all) |
22073 | 67 |
|
63167 | 68 |
section \<open>Substitutions\<close> |
22494 | 69 |
|
70 |
fun |
|
71 |
lookup :: "Subst \<Rightarrow> name \<Rightarrow> trm" |
|
72 |
where |
|
73 |
"lookup [] x = Var x" |
|
22501 | 74 |
| "lookup ((y,T)#\<theta>) x = (if x=y then T else lookup \<theta> x)" |
22494 | 75 |
|
76 |
lemma lookup_eqvt[eqvt]: |
|
77 |
fixes pi::"name prm" |
|
78 |
shows "pi\<bullet>(lookup \<theta> x) = lookup (pi\<bullet>\<theta>) (pi\<bullet>x)" |
|
79 |
by (induct \<theta>) (auto simp add: perm_bij) |
|
80 |
||
81 |
lemma lookup_fresh: |
|
82 |
fixes z::"name" |
|
83 |
assumes a: "z\<sharp>\<theta>" "z\<sharp>x" |
|
84 |
shows "z\<sharp> lookup \<theta> x" |
|
85 |
using a |
|
86 |
by (induct rule: lookup.induct) |
|
87 |
(auto simp add: fresh_list_cons) |
|
88 |
||
89 |
lemma lookup_fresh': |
|
90 |
assumes a: "z\<sharp>\<theta>" |
|
91 |
shows "lookup \<theta> z = Var z" |
|
92 |
using a |
|
93 |
by (induct rule: lookup.induct) |
|
94 |
(auto simp add: fresh_list_cons fresh_prod fresh_atm) |
|
95 |
||
96 |
nominal_primrec |
|
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
28042
diff
changeset
|
97 |
psubst :: "Subst \<Rightarrow> trm \<Rightarrow> trm" ("_<_>" [100,100] 130) |
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
28042
diff
changeset
|
98 |
where |
22494 | 99 |
"\<theta><(Var x)> = (lookup \<theta> x)" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
100 |
| "\<theta><(App t\<^sub>1 t\<^sub>2)> = App \<theta><t\<^sub>1> \<theta><t\<^sub>2>" |
29097
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
28042
diff
changeset
|
101 |
| "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].t)> = Lam [x].(\<theta><t>)" |
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
28042
diff
changeset
|
102 |
| "\<theta><(Const n)> = Const n" |
68245155eb58
Modified nominal_primrec to make it work with local theories, unified syntax
berghofe
parents:
28042
diff
changeset
|
103 |
| "\<theta><(Unit)> = Unit" |
22494 | 104 |
apply(finite_guess)+ |
105 |
apply(rule TrueI)+ |
|
106 |
apply(simp add: abs_fresh)+ |
|
107 |
apply(fresh_guess)+ |
|
108 |
done |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
109 |
|
22494 | 110 |
abbreviation |
111 |
subst :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_[_::=_]" [100,100,100] 100) |
|
112 |
where |
|
113 |
"t[x::=t'] \<equiv> ([(x,t')])<t>" |
|
114 |
||
115 |
lemma subst[simp]: |
|
116 |
shows "(Var x)[y::=t'] = (if x=y then t' else (Var x))" |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
117 |
and "(App t\<^sub>1 t\<^sub>2)[y::=t'] = App (t\<^sub>1[y::=t']) (t\<^sub>2[y::=t'])" |
22494 | 118 |
and "x\<sharp>(y,t') \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])" |
119 |
and "Const n[y::=t'] = Const n" |
|
120 |
and "Unit [y::=t'] = Unit" |
|
121 |
by (simp_all add: fresh_list_cons fresh_list_nil) |
|
122 |
||
123 |
lemma subst_eqvt[eqvt]: |
|
124 |
fixes pi::"name prm" |
|
125 |
shows "pi\<bullet>(t[x::=t']) = (pi\<bullet>t)[(pi\<bullet>x)::=(pi\<bullet>t')]" |
|
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
26677
diff
changeset
|
126 |
by (nominal_induct t avoiding: x t' rule: trm.strong_induct) |
22494 | 127 |
(perm_simp add: fresh_bij)+ |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
128 |
|
22494 | 129 |
lemma subst_rename: |
130 |
fixes c::"name" |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
131 |
assumes a: "c\<sharp>t\<^sub>1" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
132 |
shows "t\<^sub>1[a::=t\<^sub>2] = ([(c,a)]\<bullet>t\<^sub>1)[c::=t\<^sub>2]" |
22494 | 133 |
using a |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
134 |
apply(nominal_induct t\<^sub>1 avoiding: a c t\<^sub>2 rule: trm.strong_induct) |
22494 | 135 |
apply(simp add: trm.inject calc_atm fresh_atm abs_fresh perm_nat_def)+ |
136 |
done |
|
137 |
||
138 |
lemma fresh_psubst: |
|
139 |
fixes z::"name" |
|
140 |
assumes a: "z\<sharp>t" "z\<sharp>\<theta>" |
|
141 |
shows "z\<sharp>(\<theta><t>)" |
|
142 |
using a |
|
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
26677
diff
changeset
|
143 |
by (nominal_induct t avoiding: z \<theta> t rule: trm.strong_induct) |
22494 | 144 |
(auto simp add: abs_fresh lookup_fresh) |
145 |
||
146 |
lemma fresh_subst'': |
|
147 |
fixes z::"name" |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
148 |
assumes "z\<sharp>t\<^sub>2" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
149 |
shows "z\<sharp>t\<^sub>1[z::=t\<^sub>2]" |
22494 | 150 |
using assms |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
151 |
by (nominal_induct t\<^sub>1 avoiding: t\<^sub>2 z rule: trm.strong_induct) |
22494 | 152 |
(auto simp add: abs_fresh fresh_nat fresh_atm) |
153 |
||
154 |
lemma fresh_subst': |
|
155 |
fixes z::"name" |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
156 |
assumes "z\<sharp>[y].t\<^sub>1" "z\<sharp>t\<^sub>2" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
157 |
shows "z\<sharp>t\<^sub>1[y::=t\<^sub>2]" |
22494 | 158 |
using assms |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
159 |
by (nominal_induct t\<^sub>1 avoiding: y t\<^sub>2 z rule: trm.strong_induct) |
22494 | 160 |
(auto simp add: abs_fresh fresh_nat fresh_atm) |
22073 | 161 |
|
22494 | 162 |
lemma fresh_subst: |
163 |
fixes z::"name" |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
164 |
assumes a: "z\<sharp>t\<^sub>1" "z\<sharp>t\<^sub>2" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
165 |
shows "z\<sharp>t\<^sub>1[y::=t\<^sub>2]" |
22494 | 166 |
using a |
167 |
by (auto simp add: fresh_subst' abs_fresh) |
|
168 |
||
169 |
lemma fresh_psubst_simp: |
|
170 |
assumes "x\<sharp>t" |
|
24070 | 171 |
shows "((x,u)#\<theta>)<t> = \<theta><t>" |
22494 | 172 |
using assms |
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
26677
diff
changeset
|
173 |
proof (nominal_induct t avoiding: x u \<theta> rule: trm.strong_induct) |
22494 | 174 |
case (Lam y t x u) |
25107 | 175 |
have fs: "y\<sharp>\<theta>" "y\<sharp>x" "y\<sharp>u" by fact+ |
22494 | 176 |
moreover have "x\<sharp> Lam [y].t" by fact |
177 |
ultimately have "x\<sharp>t" by (simp add: abs_fresh fresh_atm) |
|
178 |
moreover have ih:"\<And>n T. n\<sharp>t \<Longrightarrow> ((n,T)#\<theta>)<t> = \<theta><t>" by fact |
|
24070 | 179 |
ultimately have "((x,u)#\<theta>)<t> = \<theta><t>" by auto |
180 |
moreover have "((x,u)#\<theta>)<Lam [y].t> = Lam [y].(((x,u)#\<theta>)<t>)" using fs |
|
22494 | 181 |
by (simp add: fresh_list_cons fresh_prod) |
182 |
moreover have " \<theta><Lam [y].t> = Lam [y]. (\<theta><t>)" using fs by simp |
|
24070 | 183 |
ultimately show "((x,u)#\<theta>)<Lam [y].t> = \<theta><Lam [y].t>" by auto |
22494 | 184 |
qed (auto simp add: fresh_atm abs_fresh) |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
185 |
|
22494 | 186 |
lemma forget: |
187 |
fixes x::"name" |
|
188 |
assumes a: "x\<sharp>t" |
|
189 |
shows "t[x::=t'] = t" |
|
190 |
using a |
|
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
26677
diff
changeset
|
191 |
by (nominal_induct t avoiding: x t' rule: trm.strong_induct) |
22494 | 192 |
(auto simp add: fresh_atm abs_fresh) |
193 |
||
194 |
lemma subst_fun_eq: |
|
195 |
fixes u::trm |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
196 |
assumes h:"[x].t\<^sub>1 = [y].t\<^sub>2" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
197 |
shows "t\<^sub>1[x::=u] = t\<^sub>2[y::=u]" |
22494 | 198 |
proof - |
199 |
{ |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
200 |
assume "x=y" and "t\<^sub>1=t\<^sub>2" |
22494 | 201 |
then have ?thesis using h by simp |
202 |
} |
|
203 |
moreover |
|
204 |
{ |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
205 |
assume h1:"x \<noteq> y" and h2:"t\<^sub>1=[(x,y)] \<bullet> t\<^sub>2" and h3:"x \<sharp> t\<^sub>2" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
206 |
then have "([(x,y)] \<bullet> t\<^sub>2)[x::=u] = t\<^sub>2[y::=u]" by (simp add: subst_rename) |
22494 | 207 |
then have ?thesis using h2 by simp |
208 |
} |
|
209 |
ultimately show ?thesis using alpha h by blast |
|
210 |
qed |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
211 |
|
22494 | 212 |
lemma psubst_empty[simp]: |
213 |
shows "[]<t> = t" |
|
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
26677
diff
changeset
|
214 |
by (nominal_induct t rule: trm.strong_induct) |
22494 | 215 |
(auto simp add: fresh_list_nil) |
216 |
||
217 |
lemma psubst_subst_psubst: |
|
218 |
assumes h:"c\<sharp>\<theta>" |
|
24070 | 219 |
shows "\<theta><t>[c::=s] = ((c,s)#\<theta>)<t>" |
22494 | 220 |
using h |
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
26677
diff
changeset
|
221 |
by (nominal_induct t avoiding: \<theta> c s rule: trm.strong_induct) |
22494 | 222 |
(auto simp add: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh' fresh_psubst) |
223 |
||
224 |
lemma subst_fresh_simp: |
|
225 |
assumes a: "x\<sharp>\<theta>" |
|
226 |
shows "\<theta><Var x> = Var x" |
|
227 |
using a |
|
49171 | 228 |
by (induct \<theta> arbitrary: x) (auto simp add:fresh_list_cons fresh_prod fresh_atm) |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
229 |
|
22494 | 230 |
lemma psubst_subst_propagate: |
231 |
assumes "x\<sharp>\<theta>" |
|
232 |
shows "\<theta><t[x::=u]> = \<theta><t>[x::=\<theta><u>]" |
|
233 |
using assms |
|
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
26677
diff
changeset
|
234 |
proof (nominal_induct t avoiding: x u \<theta> rule: trm.strong_induct) |
22494 | 235 |
case (Var n x u \<theta>) |
236 |
{ assume "x=n" |
|
237 |
moreover have "x\<sharp>\<theta>" by fact |
|
238 |
ultimately have "\<theta><Var n[x::=u]> = \<theta><Var n>[x::=\<theta><u>]" using subst_fresh_simp by auto |
|
239 |
} |
|
240 |
moreover |
|
241 |
{ assume h:"x\<noteq>n" |
|
242 |
then have "x\<sharp>Var n" by (auto simp add: fresh_atm) |
|
243 |
moreover have "x\<sharp>\<theta>" by fact |
|
244 |
ultimately have "x\<sharp>\<theta><Var n>" using fresh_psubst by blast |
|
245 |
then have " \<theta><Var n>[x::=\<theta><u>] = \<theta><Var n>" using forget by auto |
|
246 |
then have "\<theta><Var n[x::=u]> = \<theta><Var n>[x::=\<theta><u>]" using h by auto |
|
247 |
} |
|
248 |
ultimately show ?case by auto |
|
249 |
next |
|
250 |
case (Lam n t x u \<theta>) |
|
25107 | 251 |
have fs:"n\<sharp>x" "n\<sharp>u" "n\<sharp>\<theta>" "x\<sharp>\<theta>" by fact+ |
22494 | 252 |
have ih:"\<And> y s \<theta>. y\<sharp>\<theta> \<Longrightarrow> ((\<theta><(t[y::=s])>) = ((\<theta><t>)[y::=(\<theta><s>)]))" by fact |
253 |
have "\<theta> <(Lam [n].t)[x::=u]> = \<theta><Lam [n]. (t [x::=u])>" using fs by auto |
|
254 |
then have "\<theta> <(Lam [n].t)[x::=u]> = Lam [n]. \<theta><t [x::=u]>" using fs by auto |
|
255 |
moreover have "\<theta><t[x::=u]> = \<theta><t>[x::=\<theta><u>]" using ih fs by blast |
|
256 |
ultimately have "\<theta> <(Lam [n].t)[x::=u]> = Lam [n].(\<theta><t>[x::=\<theta><u>])" by auto |
|
257 |
moreover have "Lam [n].(\<theta><t>[x::=\<theta><u>]) = (Lam [n].\<theta><t>)[x::=\<theta><u>]" using fs fresh_psubst by auto |
|
258 |
ultimately have "\<theta><(Lam [n].t)[x::=u]> = (Lam [n].\<theta><t>)[x::=\<theta><u>]" using fs by auto |
|
259 |
then show "\<theta><(Lam [n].t)[x::=u]> = \<theta><Lam [n].t>[x::=\<theta><u>]" using fs by auto |
|
260 |
qed (auto) |
|
261 |
||
63167 | 262 |
section \<open>Typing\<close> |
22494 | 263 |
|
23760 | 264 |
inductive |
22494 | 265 |
valid :: "Ctxt \<Rightarrow> bool" |
22073 | 266 |
where |
22494 | 267 |
v_nil[intro]: "valid []" |
268 |
| v_cons[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> valid ((a,T)#\<Gamma>)" |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
269 |
|
22538
3ccb92dfb5e9
tuned proofs (taking full advantage of nominal_inductive)
urbanc
parents:
22531
diff
changeset
|
270 |
equivariance valid |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
271 |
|
24070 | 272 |
inductive_cases |
22073 | 273 |
valid_cons_elim_auto[elim]:"valid ((x,T)#\<Gamma>)" |
274 |
||
22494 | 275 |
abbreviation |
22650
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22609
diff
changeset
|
276 |
"sub_context" :: "Ctxt \<Rightarrow> Ctxt \<Rightarrow> bool" (" _ \<subseteq> _ " [55,55] 55) |
22494 | 277 |
where |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
278 |
"\<Gamma>\<^sub>1 \<subseteq> \<Gamma>\<^sub>2 \<equiv> \<forall>a T. (a,T)\<in>set \<Gamma>\<^sub>1 \<longrightarrow> (a,T)\<in>set \<Gamma>\<^sub>2" |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
279 |
|
22494 | 280 |
lemma valid_monotonicity[elim]: |
24231
85fb973a8207
added type constraints to resolve syntax ambiguities;
wenzelm
parents:
24088
diff
changeset
|
281 |
fixes \<Gamma> \<Gamma>' :: Ctxt |
22650
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22609
diff
changeset
|
282 |
assumes a: "\<Gamma> \<subseteq> \<Gamma>'" |
22494 | 283 |
and b: "x\<sharp>\<Gamma>'" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
284 |
shows "(x,T\<^sub>1)#\<Gamma> \<subseteq> (x,T\<^sub>1)#\<Gamma>'" |
22494 | 285 |
using a b by auto |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
286 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
287 |
lemma fresh_context: |
22494 | 288 |
fixes \<Gamma> :: "Ctxt" |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
289 |
and a :: "name" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
290 |
assumes "a\<sharp>\<Gamma>" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
291 |
shows "\<not>(\<exists>\<tau>::ty. (a,\<tau>)\<in>set \<Gamma>)" |
22494 | 292 |
using assms |
293 |
by (induct \<Gamma>) |
|
294 |
(auto simp add: fresh_prod fresh_list_cons fresh_atm) |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
295 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
296 |
lemma type_unicity_in_context: |
22494 | 297 |
assumes a: "valid \<Gamma>" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
298 |
and b: "(x,T\<^sub>1) \<in> set \<Gamma>" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
299 |
and c: "(x,T\<^sub>2) \<in> set \<Gamma>" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
300 |
shows "T\<^sub>1=T\<^sub>2" |
22494 | 301 |
using a b c |
302 |
by (induct \<Gamma>) |
|
303 |
(auto dest!: fresh_context) |
|
22073 | 304 |
|
23760 | 305 |
inductive |
22494 | 306 |
typing :: "Ctxt\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [60,60,60] 60) |
22073 | 307 |
where |
24070 | 308 |
T_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
309 |
| T_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> e\<^sub>1 : T\<^sub>1\<rightarrow>T\<^sub>2; \<Gamma> \<turnstile> e\<^sub>2 : T\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App e\<^sub>1 e\<^sub>2 : T\<^sub>2" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
310 |
| T_Lam[intro]: "\<lbrakk>x\<sharp>\<Gamma>; (x,T\<^sub>1)#\<Gamma> \<turnstile> t : T\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T\<^sub>1\<rightarrow>T\<^sub>2" |
24070 | 311 |
| T_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n : TBase" |
312 |
| T_Unit[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Unit : TUnit" |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
313 |
|
22730
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22650
diff
changeset
|
314 |
equivariance typing |
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22650
diff
changeset
|
315 |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
316 |
nominal_inductive typing |
22531 | 317 |
by (simp_all add: abs_fresh) |
22073 | 318 |
|
22494 | 319 |
lemma typing_implies_valid: |
320 |
assumes a: "\<Gamma> \<turnstile> t : T" |
|
321 |
shows "valid \<Gamma>" |
|
322 |
using a by (induct) (auto) |
|
22073 | 323 |
|
324 |
declare trm.inject [simp add] |
|
325 |
declare ty.inject [simp add] |
|
326 |
||
24088
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
327 |
inductive_cases typing_inv_auto[elim]: |
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
328 |
"\<Gamma> \<turnstile> Lam [x].t : T" |
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
329 |
"\<Gamma> \<turnstile> Var x : T" |
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
330 |
"\<Gamma> \<turnstile> App x y : T" |
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
331 |
"\<Gamma> \<turnstile> Const n : T" |
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
332 |
"\<Gamma> \<turnstile> Unit : TUnit" |
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
333 |
"\<Gamma> \<turnstile> s : TUnit" |
22073 | 334 |
|
335 |
declare trm.inject [simp del] |
|
336 |
declare ty.inject [simp del] |
|
24088
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
337 |
|
22073 | 338 |
|
63167 | 339 |
section \<open>Definitional Equivalence\<close> |
22073 | 340 |
|
23760 | 341 |
inductive |
22494 | 342 |
def_equiv :: "Ctxt\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<equiv> _ : _" [60,60] 60) |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
343 |
where |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
344 |
Q_Refl[intro]: "\<Gamma> \<turnstile> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<equiv> t : T" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
345 |
| Q_Symm[intro]: "\<Gamma> \<turnstile> t \<equiv> s : T \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
346 |
| Q_Trans[intro]: "\<lbrakk>\<Gamma> \<turnstile> s \<equiv> t : T; \<Gamma> \<turnstile> t \<equiv> u : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> u : T" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
347 |
| Q_Abs[intro]: "\<lbrakk>x\<sharp>\<Gamma>; (x,T\<^sub>1)#\<Gamma> \<turnstile> s\<^sub>2 \<equiv> t\<^sub>2 : T\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x]. s\<^sub>2 \<equiv> Lam [x]. t\<^sub>2 : T\<^sub>1 \<rightarrow> T\<^sub>2" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
348 |
| Q_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> s\<^sub>1 \<equiv> t\<^sub>1 : T\<^sub>1 \<rightarrow> T\<^sub>2 ; \<Gamma> \<turnstile> s\<^sub>2 \<equiv> t\<^sub>2 : T\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App s\<^sub>1 s\<^sub>2 \<equiv> App t\<^sub>1 t\<^sub>2 : T\<^sub>2" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
349 |
| Q_Beta[intro]: "\<lbrakk>x\<sharp>(\<Gamma>,s\<^sub>2,t\<^sub>2); (x,T\<^sub>1)#\<Gamma> \<turnstile> s\<^sub>1 \<equiv> t\<^sub>1 : T\<^sub>2 ; \<Gamma> \<turnstile> s\<^sub>2 \<equiv> t\<^sub>2 : T\<^sub>1\<rbrakk> |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
350 |
\<Longrightarrow> \<Gamma> \<turnstile> App (Lam [x]. s\<^sub>1) s\<^sub>2 \<equiv> t\<^sub>1[x::=t\<^sub>2] : T\<^sub>2" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
351 |
| Q_Ext[intro]: "\<lbrakk>x\<sharp>(\<Gamma>,s,t); (x,T\<^sub>1)#\<Gamma> \<turnstile> App s (Var x) \<equiv> App t (Var x) : T\<^sub>2\<rbrakk> |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
352 |
\<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T\<^sub>1 \<rightarrow> T\<^sub>2" |
23370
513a8ee192f1
added the Q_Unit rule (was missing) and adjusted the proof accordingly
urbanc
parents:
22829
diff
changeset
|
353 |
| Q_Unit[intro]: "\<lbrakk>\<Gamma> \<turnstile> s : TUnit; \<Gamma> \<turnstile> t: TUnit\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : TUnit" |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
354 |
|
22730
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22650
diff
changeset
|
355 |
equivariance def_equiv |
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22650
diff
changeset
|
356 |
|
22494 | 357 |
nominal_inductive def_equiv |
22531 | 358 |
by (simp_all add: abs_fresh fresh_subst'') |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
359 |
|
22494 | 360 |
lemma def_equiv_implies_valid: |
361 |
assumes a: "\<Gamma> \<turnstile> t \<equiv> s : T" |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
362 |
shows "valid \<Gamma>" |
22494 | 363 |
using a by (induct) (auto elim: typing_implies_valid) |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
364 |
|
63167 | 365 |
section \<open>Weak Head Reduction\<close> |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
366 |
|
23760 | 367 |
inductive |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
368 |
whr_def :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<leadsto> _" [80,80] 80) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
369 |
where |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
370 |
QAR_Beta[intro]: "App (Lam [x]. t\<^sub>1) t\<^sub>2 \<leadsto> t\<^sub>1[x::=t\<^sub>2]" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
371 |
| QAR_App[intro]: "t\<^sub>1 \<leadsto> t\<^sub>1' \<Longrightarrow> App t\<^sub>1 t\<^sub>2 \<leadsto> App t\<^sub>1' t\<^sub>2" |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
372 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
373 |
declare trm.inject [simp add] |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
374 |
declare ty.inject [simp add] |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
375 |
|
24088
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
376 |
inductive_cases whr_inv_auto[elim]: |
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
377 |
"t \<leadsto> t'" |
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
378 |
"Lam [x].t \<leadsto> t'" |
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
379 |
"App (Lam [x].t12) t2 \<leadsto> t" |
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
380 |
"Var x \<leadsto> t" |
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
381 |
"Const n \<leadsto> t" |
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
382 |
"App p q \<leadsto> t" |
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
383 |
"t \<leadsto> Const n" |
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
384 |
"t \<leadsto> Var x" |
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
385 |
"t \<leadsto> App p q" |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
386 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
387 |
declare trm.inject [simp del] |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
388 |
declare ty.inject [simp del] |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
389 |
|
22531 | 390 |
equivariance whr_def |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
391 |
|
63167 | 392 |
section \<open>Weak Head Normalisation\<close> |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
393 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
394 |
abbreviation |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
395 |
nf :: "trm \<Rightarrow> bool" ("_ \<leadsto>|" [100] 100) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
396 |
where |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
397 |
"t\<leadsto>| \<equiv> \<not>(\<exists> u. t \<leadsto> u)" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
398 |
|
23760 | 399 |
inductive |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
400 |
whn_def :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<Down> _" [80,80] 80) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
401 |
where |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
402 |
QAN_Reduce[intro]: "\<lbrakk>s \<leadsto> t; t \<Down> u\<rbrakk> \<Longrightarrow> s \<Down> u" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
403 |
| QAN_Normal[intro]: "t\<leadsto>| \<Longrightarrow> t \<Down> t" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
404 |
|
22494 | 405 |
declare trm.inject[simp] |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
406 |
|
23760 | 407 |
inductive_cases whn_inv_auto[elim]: "t \<Down> t'" |
22494 | 408 |
|
409 |
declare trm.inject[simp del] |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
410 |
|
32638 | 411 |
equivariance whn_def |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
412 |
|
22494 | 413 |
lemma red_unicity : |
414 |
assumes a: "x \<leadsto> a" |
|
415 |
and b: "x \<leadsto> b" |
|
416 |
shows "a=b" |
|
417 |
using a b |
|
418 |
apply (induct arbitrary: b) |
|
24088
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
419 |
apply (erule whr_inv_auto(3)) |
22494 | 420 |
apply (clarify) |
421 |
apply (rule subst_fun_eq) |
|
422 |
apply (simp) |
|
423 |
apply (force) |
|
24088
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
424 |
apply (erule whr_inv_auto(6)) |
22494 | 425 |
apply (blast)+ |
426 |
done |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
427 |
|
22494 | 428 |
lemma nf_unicity : |
429 |
assumes "x \<Down> a" and "x \<Down> b" |
|
430 |
shows "a=b" |
|
431 |
using assms |
|
432 |
proof (induct arbitrary: b) |
|
433 |
case (QAN_Reduce x t a b) |
|
25107 | 434 |
have h:"x \<leadsto> t" "t \<Down> a" by fact+ |
22494 | 435 |
have ih:"\<And>b. t \<Down> b \<Longrightarrow> a = b" by fact |
436 |
have "x \<Down> b" by fact |
|
437 |
then obtain t' where "x \<leadsto> t'" and hl:"t' \<Down> b" using h by auto |
|
438 |
then have "t=t'" using h red_unicity by auto |
|
439 |
then show "a=b" using ih hl by auto |
|
440 |
qed (auto) |
|
441 |
||
24070 | 442 |
|
63167 | 443 |
section \<open>Algorithmic Term Equivalence and Algorithmic Path Equivalence\<close> |
22494 | 444 |
|
23760 | 445 |
inductive |
22650
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22609
diff
changeset
|
446 |
alg_equiv :: "Ctxt\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<Leftrightarrow> _ : _" [60,60,60,60] 60) |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
447 |
and |
22650
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22609
diff
changeset
|
448 |
alg_path_equiv :: "Ctxt\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<leftrightarrow> _ : _" [60,60,60,60] 60) |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
449 |
where |
22650
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22609
diff
changeset
|
450 |
QAT_Base[intro]: "\<lbrakk>s \<Down> p; t \<Down> q; \<Gamma> \<turnstile> p \<leftrightarrow> q : TBase\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : TBase" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
451 |
| QAT_Arrow[intro]: "\<lbrakk>x\<sharp>(\<Gamma>,s,t); (x,T\<^sub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^sub>2\<rbrakk> |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
452 |
\<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^sub>1 \<rightarrow> T\<^sub>2" |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
453 |
| QAT_One[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : TUnit" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
454 |
| QAP_Var[intro]: "\<lbrakk>valid \<Gamma>;(x,T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x \<leftrightarrow> Var x : T" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
455 |
| QAP_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> p \<leftrightarrow> q : T\<^sub>1 \<rightarrow> T\<^sub>2; \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App p s \<leftrightarrow> App q t : T\<^sub>2" |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
456 |
| QAP_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n \<leftrightarrow> Const n : TBase" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
457 |
|
22730
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22650
diff
changeset
|
458 |
equivariance alg_equiv |
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22650
diff
changeset
|
459 |
|
22531 | 460 |
nominal_inductive alg_equiv |
461 |
avoids QAT_Arrow: x |
|
462 |
by simp_all |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
463 |
|
22494 | 464 |
declare trm.inject [simp add] |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
465 |
declare ty.inject [simp add] |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
466 |
|
24088
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
467 |
inductive_cases alg_equiv_inv_auto[elim]: |
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
468 |
"\<Gamma> \<turnstile> s\<Leftrightarrow>t : TBase" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
469 |
"\<Gamma> \<turnstile> s\<Leftrightarrow>t : T\<^sub>1 \<rightarrow> T\<^sub>2" |
24088
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
470 |
"\<Gamma> \<turnstile> s\<leftrightarrow>t : TBase" |
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
471 |
"\<Gamma> \<turnstile> s\<leftrightarrow>t : TUnit" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
472 |
"\<Gamma> \<turnstile> s\<leftrightarrow>t : T\<^sub>1 \<rightarrow> T\<^sub>2" |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
473 |
|
24088
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
474 |
"\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T" |
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
475 |
"\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T'" |
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
476 |
"\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T" |
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
477 |
"\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T'" |
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
478 |
"\<Gamma> \<turnstile> Const n \<leftrightarrow> t : T" |
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
479 |
"\<Gamma> \<turnstile> s \<leftrightarrow> Const n : T" |
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
480 |
"\<Gamma> \<turnstile> App p s \<leftrightarrow> t : T" |
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
481 |
"\<Gamma> \<turnstile> s \<leftrightarrow> App q t : T" |
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
482 |
"\<Gamma> \<turnstile> Lam[x].s \<leftrightarrow> t : T" |
c2d8270e53a5
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
narboux
parents:
24070
diff
changeset
|
483 |
"\<Gamma> \<turnstile> t \<leftrightarrow> Lam[x].s : T" |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
484 |
|
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
485 |
declare trm.inject [simp del] |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
486 |
declare ty.inject [simp del] |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
487 |
|
22073 | 488 |
lemma Q_Arrow_strong_inversion: |
22494 | 489 |
assumes fs: "x\<sharp>\<Gamma>" "x\<sharp>t" "x\<sharp>u" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
490 |
and h: "\<Gamma> \<turnstile> t \<Leftrightarrow> u : T\<^sub>1\<rightarrow>T\<^sub>2" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
491 |
shows "(x,T\<^sub>1)#\<Gamma> \<turnstile> App t (Var x) \<Leftrightarrow> App u (Var x) : T\<^sub>2" |
22073 | 492 |
proof - |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
493 |
obtain y where fs2: "y\<sharp>(\<Gamma>,t,u)" and "(y,T\<^sub>1)#\<Gamma> \<turnstile> App t (Var y) \<Leftrightarrow> App u (Var y) : T\<^sub>2" |
22082 | 494 |
using h by auto |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
495 |
then have "([(x,y)]\<bullet>((y,T\<^sub>1)#\<Gamma>)) \<turnstile> [(x,y)]\<bullet> App t (Var y) \<Leftrightarrow> [(x,y)]\<bullet> App u (Var y) : T\<^sub>2" |
22542 | 496 |
using alg_equiv.eqvt[simplified] by blast |
22082 | 497 |
then show ?thesis using fs fs2 by (perm_simp) |
22073 | 498 |
qed |
499 |
||
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
500 |
(* |
22594
33a690455f88
add a few details in the Fst and Snd cases of unicity proof
narboux
parents:
22542
diff
changeset
|
501 |
Warning this lemma is false: |
33a690455f88
add a few details in the Fst and Snd cases of unicity proof
narboux
parents:
22542
diff
changeset
|
502 |
|
22073 | 503 |
lemma algorithmic_type_unicity: |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
504 |
shows "\<lbrakk> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<Leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'" |
22073 | 505 |
and "\<lbrakk> \<Gamma> \<turnstile> s \<leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'" |
506 |
||
507 |
Here is the counter example : |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
508 |
\<Gamma> \<turnstile> Const n \<Leftrightarrow> Const n : Tbase and \<Gamma> \<turnstile> Const n \<Leftrightarrow> Const n : TUnit |
22073 | 509 |
*) |
510 |
||
511 |
lemma algorithmic_path_type_unicity: |
|
22494 | 512 |
shows "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> s \<leftrightarrow> u : T' \<Longrightarrow> T = T'" |
22082 | 513 |
proof (induct arbitrary: u T' |
514 |
rule: alg_equiv_alg_path_equiv.inducts(2) [of _ _ _ _ _ "%a b c d . True" ]) |
|
22073 | 515 |
case (QAP_Var \<Gamma> x T u T') |
516 |
have "\<Gamma> \<turnstile> Var x \<leftrightarrow> u : T'" by fact |
|
517 |
then have "u=Var x" and "(x,T') \<in> set \<Gamma>" by auto |
|
25107 | 518 |
moreover have "valid \<Gamma>" "(x,T) \<in> set \<Gamma>" by fact+ |
22073 | 519 |
ultimately show "T=T'" using type_unicity_in_context by auto |
520 |
next |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
521 |
case (QAP_App \<Gamma> p q T\<^sub>1 T\<^sub>2 s t u T\<^sub>2') |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
522 |
have ih:"\<And>u T. \<Gamma> \<turnstile> p \<leftrightarrow> u : T \<Longrightarrow> T\<^sub>1\<rightarrow>T\<^sub>2 = T" by fact |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
523 |
have "\<Gamma> \<turnstile> App p s \<leftrightarrow> u : T\<^sub>2'" by fact |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
524 |
then obtain r t T\<^sub>1' where "u = App r t" "\<Gamma> \<turnstile> p \<leftrightarrow> r : T\<^sub>1' \<rightarrow> T\<^sub>2'" by auto |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
525 |
with ih have "T\<^sub>1\<rightarrow>T\<^sub>2 = T\<^sub>1' \<rightarrow> T\<^sub>2'" by auto |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
526 |
then show "T\<^sub>2=T\<^sub>2'" using ty.inject by auto |
22073 | 527 |
qed (auto) |
528 |
||
22494 | 529 |
lemma alg_path_equiv_implies_valid: |
530 |
shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> valid \<Gamma>" |
|
531 |
and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> valid \<Gamma>" |
|
49171 | 532 |
by (induct rule : alg_equiv_alg_path_equiv.inducts) auto |
22494 | 533 |
|
534 |
lemma algorithmic_symmetry: |
|
535 |
shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<Leftrightarrow> s : T" |
|
536 |
and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<leftrightarrow> s : T" |
|
537 |
by (induct rule: alg_equiv_alg_path_equiv.inducts) |
|
538 |
(auto simp add: fresh_prod) |
|
539 |
||
22073 | 540 |
lemma algorithmic_transitivity: |
22494 | 541 |
shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<Leftrightarrow> u : T \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> u : T" |
542 |
and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<leftrightarrow> u : T \<Longrightarrow> \<Gamma> \<turnstile> s \<leftrightarrow> u : T" |
|
22531 | 543 |
proof (nominal_induct \<Gamma> s t T and \<Gamma> s t T avoiding: u rule: alg_equiv_alg_path_equiv.strong_inducts) |
22073 | 544 |
case (QAT_Base s p t q \<Gamma> u) |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
545 |
have "\<Gamma> \<turnstile> t \<Leftrightarrow> u : TBase" by fact |
22494 | 546 |
then obtain r' q' where b1: "t \<Down> q'" and b2: "u \<Down> r'" and b3: "\<Gamma> \<turnstile> q' \<leftrightarrow> r' : TBase" by auto |
547 |
have ih: "\<Gamma> \<turnstile> q \<leftrightarrow> r' : TBase \<Longrightarrow> \<Gamma> \<turnstile> p \<leftrightarrow> r' : TBase" by fact |
|
548 |
have "t \<Down> q" by fact |
|
549 |
with b1 have eq: "q=q'" by (simp add: nf_unicity) |
|
550 |
with ih b3 have "\<Gamma> \<turnstile> p \<leftrightarrow> r' : TBase" by simp |
|
551 |
moreover |
|
552 |
have "s \<Down> p" by fact |
|
553 |
ultimately show "\<Gamma> \<turnstile> s \<Leftrightarrow> u : TBase" using b2 by auto |
|
22073 | 554 |
next |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
555 |
case (QAT_Arrow x \<Gamma> s t T\<^sub>1 T\<^sub>2 u) |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
556 |
have ih:"(x,T\<^sub>1)#\<Gamma> \<turnstile> App t (Var x) \<Leftrightarrow> App u (Var x) : T\<^sub>2 |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
557 |
\<Longrightarrow> (x,T\<^sub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App u (Var x) : T\<^sub>2" by fact |
25107 | 558 |
have fs: "x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" "x\<sharp>u" by fact+ |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
559 |
have "\<Gamma> \<turnstile> t \<Leftrightarrow> u : T\<^sub>1\<rightarrow>T\<^sub>2" by fact |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
560 |
then have "(x,T\<^sub>1)#\<Gamma> \<turnstile> App t (Var x) \<Leftrightarrow> App u (Var x) : T\<^sub>2" using fs |
22494 | 561 |
by (simp add: Q_Arrow_strong_inversion) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
562 |
with ih have "(x,T\<^sub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App u (Var x) : T\<^sub>2" by simp |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
563 |
then show "\<Gamma> \<turnstile> s \<Leftrightarrow> u : T\<^sub>1\<rightarrow>T\<^sub>2" using fs by (auto simp add: fresh_prod) |
22073 | 564 |
next |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
565 |
case (QAP_App \<Gamma> p q T\<^sub>1 T\<^sub>2 s t u) |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
566 |
have "\<Gamma> \<turnstile> App q t \<leftrightarrow> u : T\<^sub>2" by fact |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
567 |
then obtain r T\<^sub>1' v where ha: "\<Gamma> \<turnstile> q \<leftrightarrow> r : T\<^sub>1'\<rightarrow>T\<^sub>2" and hb: "\<Gamma> \<turnstile> t \<Leftrightarrow> v : T\<^sub>1'" and eq: "u = App r v" |
22082 | 568 |
by auto |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
569 |
have ih1: "\<Gamma> \<turnstile> q \<leftrightarrow> r : T\<^sub>1\<rightarrow>T\<^sub>2 \<Longrightarrow> \<Gamma> \<turnstile> p \<leftrightarrow> r : T\<^sub>1\<rightarrow>T\<^sub>2" by fact |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
570 |
have ih2:"\<Gamma> \<turnstile> t \<Leftrightarrow> v : T\<^sub>1 \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> v : T\<^sub>1" by fact |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
571 |
have "\<Gamma> \<turnstile> p \<leftrightarrow> q : T\<^sub>1\<rightarrow>T\<^sub>2" by fact |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
572 |
then have "\<Gamma> \<turnstile> q \<leftrightarrow> p : T\<^sub>1\<rightarrow>T\<^sub>2" by (simp add: algorithmic_symmetry) |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
573 |
with ha have "T\<^sub>1'\<rightarrow>T\<^sub>2 = T\<^sub>1\<rightarrow>T\<^sub>2" using algorithmic_path_type_unicity by simp |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
574 |
then have "T\<^sub>1' = T\<^sub>1" by (simp add: ty.inject) |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
575 |
then have "\<Gamma> \<turnstile> s \<Leftrightarrow> v : T\<^sub>1" "\<Gamma> \<turnstile> p \<leftrightarrow> r : T\<^sub>1\<rightarrow>T\<^sub>2" using ih1 ih2 ha hb by auto |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
576 |
then show "\<Gamma> \<turnstile> App p s \<leftrightarrow> u : T\<^sub>2" using eq by auto |
22073 | 577 |
qed (auto) |
578 |
||
579 |
lemma algorithmic_weak_head_closure: |
|
22494 | 580 |
shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> s' \<leadsto> s \<Longrightarrow> t' \<leadsto> t \<Longrightarrow> \<Gamma> \<turnstile> s' \<Leftrightarrow> t' : T" |
581 |
apply (nominal_induct \<Gamma> s t T avoiding: s' t' |
|
22531 | 582 |
rule: alg_equiv_alg_path_equiv.strong_inducts(1) [of _ _ _ _ "%a b c d e. True"]) |
22494 | 583 |
apply(auto intro!: QAT_Arrow) |
584 |
done |
|
585 |
||
586 |
lemma algorithmic_monotonicity: |
|
22650
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22609
diff
changeset
|
587 |
shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<subseteq> \<Gamma>' \<Longrightarrow> valid \<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<Leftrightarrow> t : T" |
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22609
diff
changeset
|
588 |
and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<subseteq> \<Gamma>' \<Longrightarrow> valid \<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<leftrightarrow> t : T" |
22531 | 589 |
proof (nominal_induct \<Gamma> s t T and \<Gamma> s t T avoiding: \<Gamma>' rule: alg_equiv_alg_path_equiv.strong_inducts) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
590 |
case (QAT_Arrow x \<Gamma> s t T\<^sub>1 T\<^sub>2 \<Gamma>') |
25107 | 591 |
have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" "x\<sharp>\<Gamma>'" by fact+ |
22650
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22609
diff
changeset
|
592 |
have h2:"\<Gamma> \<subseteq> \<Gamma>'" by fact |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
593 |
have ih:"\<And>\<Gamma>'. \<lbrakk>(x,T\<^sub>1)#\<Gamma> \<subseteq> \<Gamma>'; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^sub>2" by fact |
22494 | 594 |
have "valid \<Gamma>'" by fact |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
595 |
then have "valid ((x,T\<^sub>1)#\<Gamma>')" using fs by auto |
22494 | 596 |
moreover |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
597 |
have sub: "(x,T\<^sub>1)#\<Gamma> \<subseteq> (x,T\<^sub>1)#\<Gamma>'" using h2 by auto |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
598 |
ultimately have "(x,T\<^sub>1)#\<Gamma>' \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^sub>2" using ih by simp |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
599 |
then show "\<Gamma>' \<turnstile> s \<Leftrightarrow> t : T\<^sub>1\<rightarrow>T\<^sub>2" using fs by (auto simp add: fresh_prod) |
22494 | 600 |
qed (auto) |
601 |
||
602 |
lemma path_equiv_implies_nf: |
|
603 |
assumes "\<Gamma> \<turnstile> s \<leftrightarrow> t : T" |
|
604 |
shows "s \<leadsto>|" and "t \<leadsto>|" |
|
605 |
using assms |
|
606 |
by (induct rule: alg_equiv_alg_path_equiv.inducts(2)) (simp, auto) |
|
607 |
||
63167 | 608 |
section \<open>Logical Equivalence\<close> |
22494 | 609 |
|
610 |
function log_equiv :: "(Ctxt \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool)" ("_ \<turnstile> _ is _ : _" [60,60,60,60] 60) |
|
611 |
where |
|
612 |
"\<Gamma> \<turnstile> s is t : TUnit = True" |
|
613 |
| "\<Gamma> \<turnstile> s is t : TBase = \<Gamma> \<turnstile> s \<Leftrightarrow> t : TBase" |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
614 |
| "\<Gamma> \<turnstile> s is t : (T\<^sub>1 \<rightarrow> T\<^sub>2) = |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
615 |
(\<forall>\<Gamma>' s' t'. \<Gamma>\<subseteq>\<Gamma>' \<longrightarrow> valid \<Gamma>' \<longrightarrow> \<Gamma>' \<turnstile> s' is t' : T\<^sub>1 \<longrightarrow> (\<Gamma>' \<turnstile> (App s s') is (App t t') : T\<^sub>2))" |
22494 | 616 |
apply (auto simp add: ty.inject) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
617 |
apply (subgoal_tac "(\<exists>T\<^sub>1 T\<^sub>2. b=T\<^sub>1 \<rightarrow> T\<^sub>2) \<or> b=TUnit \<or> b=TBase" ) |
22494 | 618 |
apply (force) |
619 |
apply (rule ty_cases) |
|
620 |
done |
|
32638 | 621 |
|
28042 | 622 |
termination by lexicographic_order |
22494 | 623 |
|
24231
85fb973a8207
added type constraints to resolve syntax ambiguities;
wenzelm
parents:
24088
diff
changeset
|
624 |
lemma logical_monotonicity: |
85fb973a8207
added type constraints to resolve syntax ambiguities;
wenzelm
parents:
24088
diff
changeset
|
625 |
fixes \<Gamma> \<Gamma>' :: Ctxt |
22494 | 626 |
assumes a1: "\<Gamma> \<turnstile> s is t : T" |
22650
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22609
diff
changeset
|
627 |
and a2: "\<Gamma> \<subseteq> \<Gamma>'" |
22494 | 628 |
and a3: "valid \<Gamma>'" |
629 |
shows "\<Gamma>' \<turnstile> s is t : T" |
|
630 |
using a1 a2 a3 |
|
631 |
proof (induct arbitrary: \<Gamma>' rule: log_equiv.induct) |
|
632 |
case (2 \<Gamma> s t \<Gamma>') |
|
633 |
then show "\<Gamma>' \<turnstile> s is t : TBase" using algorithmic_monotonicity by auto |
|
634 |
next |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
635 |
case (3 \<Gamma> s t T\<^sub>1 T\<^sub>2 \<Gamma>') |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
636 |
have "\<Gamma> \<turnstile> s is t : T\<^sub>1\<rightarrow>T\<^sub>2" |
24070 | 637 |
and "\<Gamma> \<subseteq> \<Gamma>'" |
25107 | 638 |
and "valid \<Gamma>'" by fact+ |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
639 |
then show "\<Gamma>' \<turnstile> s is t : T\<^sub>1\<rightarrow>T\<^sub>2" by simp |
22494 | 640 |
qed (auto) |
641 |
||
642 |
lemma main_lemma: |
|
643 |
shows "\<Gamma> \<turnstile> s is t : T \<Longrightarrow> valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T" |
|
644 |
and "\<Gamma> \<turnstile> p \<leftrightarrow> q : T \<Longrightarrow> \<Gamma> \<turnstile> p is q : T" |
|
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
26677
diff
changeset
|
645 |
proof (nominal_induct T arbitrary: \<Gamma> s t p q rule: ty.strong_induct) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
646 |
case (Arrow T\<^sub>1 T\<^sub>2) |
22494 | 647 |
{ |
648 |
case (1 \<Gamma> s t) |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
649 |
have ih1:"\<And>\<Gamma> s t. \<lbrakk>\<Gamma> \<turnstile> s is t : T\<^sub>2; valid \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^sub>2" by fact |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
650 |
have ih2:"\<And>\<Gamma> s t. \<Gamma> \<turnstile> s \<leftrightarrow> t : T\<^sub>1 \<Longrightarrow> \<Gamma> \<turnstile> s is t : T\<^sub>1" by fact |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
651 |
have h:"\<Gamma> \<turnstile> s is t : T\<^sub>1\<rightarrow>T\<^sub>2" by fact |
22494 | 652 |
obtain x::name where fs:"x\<sharp>(\<Gamma>,s,t)" by (erule exists_fresh[OF fs_name1]) |
653 |
have "valid \<Gamma>" by fact |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
654 |
then have v: "valid ((x,T\<^sub>1)#\<Gamma>)" using fs by auto |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
655 |
then have "(x,T\<^sub>1)#\<Gamma> \<turnstile> Var x \<leftrightarrow> Var x : T\<^sub>1" by auto |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
656 |
then have "(x,T\<^sub>1)#\<Gamma> \<turnstile> Var x is Var x : T\<^sub>1" using ih2 by auto |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
657 |
then have "(x,T\<^sub>1)#\<Gamma> \<turnstile> App s (Var x) is App t (Var x) : T\<^sub>2" using h v by auto |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
658 |
then have "(x,T\<^sub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^sub>2" using ih1 v by auto |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
659 |
then show "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^sub>1\<rightarrow>T\<^sub>2" using fs by (auto simp add: fresh_prod) |
22494 | 660 |
next |
661 |
case (2 \<Gamma> p q) |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
662 |
have h: "\<Gamma> \<turnstile> p \<leftrightarrow> q : T\<^sub>1\<rightarrow>T\<^sub>2" by fact |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
663 |
have ih1:"\<And>\<Gamma> s t. \<Gamma> \<turnstile> s \<leftrightarrow> t : T\<^sub>2 \<Longrightarrow> \<Gamma> \<turnstile> s is t : T\<^sub>2" by fact |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
664 |
have ih2:"\<And>\<Gamma> s t. \<lbrakk>\<Gamma> \<turnstile> s is t : T\<^sub>1; valid \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^sub>1" by fact |
22494 | 665 |
{ |
666 |
fix \<Gamma>' s t |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
667 |
assume "\<Gamma> \<subseteq> \<Gamma>'" and hl:"\<Gamma>' \<turnstile> s is t : T\<^sub>1" and hk: "valid \<Gamma>'" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
668 |
then have "\<Gamma>' \<turnstile> p \<leftrightarrow> q : T\<^sub>1 \<rightarrow> T\<^sub>2" using h algorithmic_monotonicity by auto |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
669 |
moreover have "\<Gamma>' \<turnstile> s \<Leftrightarrow> t : T\<^sub>1" using ih2 hl hk by auto |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
670 |
ultimately have "\<Gamma>' \<turnstile> App p s \<leftrightarrow> App q t : T\<^sub>2" by auto |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
671 |
then have "\<Gamma>' \<turnstile> App p s is App q t : T\<^sub>2" using ih1 by auto |
22494 | 672 |
} |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
673 |
then show "\<Gamma> \<turnstile> p is q : T\<^sub>1\<rightarrow>T\<^sub>2" by simp |
22494 | 674 |
} |
675 |
next |
|
676 |
case TBase |
|
677 |
{ case 2 |
|
678 |
have h:"\<Gamma> \<turnstile> s \<leftrightarrow> t : TBase" by fact |
|
679 |
then have "s \<leadsto>|" and "t \<leadsto>|" using path_equiv_implies_nf by auto |
|
680 |
then have "s \<Down> s" and "t \<Down> t" by auto |
|
681 |
then have "\<Gamma> \<turnstile> s \<Leftrightarrow> t : TBase" using h by auto |
|
682 |
then show "\<Gamma> \<turnstile> s is t : TBase" by auto |
|
683 |
} |
|
684 |
qed (auto elim: alg_path_equiv_implies_valid) |
|
685 |
||
686 |
corollary corollary_main: |
|
687 |
assumes a: "\<Gamma> \<turnstile> s \<leftrightarrow> t : T" |
|
688 |
shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T" |
|
689 |
using a main_lemma alg_path_equiv_implies_valid by blast |
|
22073 | 690 |
|
691 |
lemma logical_symmetry: |
|
22082 | 692 |
assumes a: "\<Gamma> \<turnstile> s is t : T" |
22073 | 693 |
shows "\<Gamma> \<turnstile> t is s : T" |
22082 | 694 |
using a |
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
26677
diff
changeset
|
695 |
by (nominal_induct arbitrary: \<Gamma> s t rule: ty.strong_induct) |
22494 | 696 |
(auto simp add: algorithmic_symmetry) |
22073 | 697 |
|
698 |
lemma logical_transitivity: |
|
699 |
assumes "\<Gamma> \<turnstile> s is t : T" "\<Gamma> \<turnstile> t is u : T" |
|
700 |
shows "\<Gamma> \<turnstile> s is u : T" |
|
701 |
using assms |
|
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
26677
diff
changeset
|
702 |
proof (nominal_induct arbitrary: \<Gamma> s t u rule:ty.strong_induct) |
22073 | 703 |
case TBase |
704 |
then show "\<Gamma> \<turnstile> s is u : TBase" by (auto elim: algorithmic_transitivity) |
|
705 |
next |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
706 |
case (Arrow T\<^sub>1 T\<^sub>2 \<Gamma> s t u) |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
707 |
have h1:"\<Gamma> \<turnstile> s is t : T\<^sub>1 \<rightarrow> T\<^sub>2" by fact |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
708 |
have h2:"\<Gamma> \<turnstile> t is u : T\<^sub>1 \<rightarrow> T\<^sub>2" by fact |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
709 |
have ih1:"\<And>\<Gamma> s t u. \<lbrakk>\<Gamma> \<turnstile> s is t : T\<^sub>1; \<Gamma> \<turnstile> t is u : T\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s is u : T\<^sub>1" by fact |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
710 |
have ih2:"\<And>\<Gamma> s t u. \<lbrakk>\<Gamma> \<turnstile> s is t : T\<^sub>2; \<Gamma> \<turnstile> t is u : T\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s is u : T\<^sub>2" by fact |
22073 | 711 |
{ |
712 |
fix \<Gamma>' s' u' |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
713 |
assume hsub:"\<Gamma> \<subseteq> \<Gamma>'" and hl:"\<Gamma>' \<turnstile> s' is u' : T\<^sub>1" and hk: "valid \<Gamma>'" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
714 |
then have "\<Gamma>' \<turnstile> u' is s' : T\<^sub>1" using logical_symmetry by blast |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
715 |
then have "\<Gamma>' \<turnstile> u' is u' : T\<^sub>1" using ih1 hl by blast |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
716 |
then have "\<Gamma>' \<turnstile> App t u' is App u u' : T\<^sub>2" using h2 hsub hk by auto |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
717 |
moreover have "\<Gamma>' \<turnstile> App s s' is App t u' : T\<^sub>2" using h1 hsub hl hk by auto |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
718 |
ultimately have "\<Gamma>' \<turnstile> App s s' is App u u' : T\<^sub>2" using ih2 by blast |
22073 | 719 |
} |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
720 |
then show "\<Gamma> \<turnstile> s is u : T\<^sub>1 \<rightarrow> T\<^sub>2" by auto |
22073 | 721 |
qed (auto) |
722 |
||
723 |
lemma logical_weak_head_closure: |
|
22494 | 724 |
assumes a: "\<Gamma> \<turnstile> s is t : T" |
725 |
and b: "s' \<leadsto> s" |
|
726 |
and c: "t' \<leadsto> t" |
|
22073 | 727 |
shows "\<Gamma> \<turnstile> s' is t' : T" |
22494 | 728 |
using a b c algorithmic_weak_head_closure |
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
26677
diff
changeset
|
729 |
by (nominal_induct arbitrary: \<Gamma> s t s' t' rule: ty.strong_induct) |
22494 | 730 |
(auto, blast) |
22073 | 731 |
|
732 |
lemma logical_weak_head_closure': |
|
22494 | 733 |
assumes "\<Gamma> \<turnstile> s is t : T" and "s' \<leadsto> s" |
22073 | 734 |
shows "\<Gamma> \<turnstile> s' is t : T" |
735 |
using assms |
|
26966
071f40487734
made the naming of the induction principles consistent: weak_induct is
urbanc
parents:
26677
diff
changeset
|
736 |
proof (nominal_induct arbitrary: \<Gamma> s t s' rule: ty.strong_induct) |
22073 | 737 |
case (TBase \<Gamma> s t s') |
738 |
then show ?case by force |
|
739 |
next |
|
740 |
case (TUnit \<Gamma> s t s') |
|
741 |
then show ?case by auto |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
742 |
next |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
743 |
case (Arrow T\<^sub>1 T\<^sub>2 \<Gamma> s t s') |
22073 | 744 |
have h1:"s' \<leadsto> s" by fact |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
745 |
have ih:"\<And>\<Gamma> s t s'. \<lbrakk>\<Gamma> \<turnstile> s is t : T\<^sub>2; s' \<leadsto> s\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s' is t : T\<^sub>2" by fact |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
746 |
have h2:"\<Gamma> \<turnstile> s is t : T\<^sub>1\<rightarrow>T\<^sub>2" by fact |
22494 | 747 |
then |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
748 |
have hb:"\<forall>\<Gamma>' s' t'. \<Gamma>\<subseteq>\<Gamma>' \<longrightarrow> valid \<Gamma>' \<longrightarrow> \<Gamma>' \<turnstile> s' is t' : T\<^sub>1 \<longrightarrow> (\<Gamma>' \<turnstile> (App s s') is (App t t') : T\<^sub>2)" |
22494 | 749 |
by auto |
22073 | 750 |
{ |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
751 |
fix \<Gamma>' s\<^sub>2 t\<^sub>2 |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
752 |
assume "\<Gamma> \<subseteq> \<Gamma>'" and "\<Gamma>' \<turnstile> s\<^sub>2 is t\<^sub>2 : T\<^sub>1" and "valid \<Gamma>'" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
753 |
then have "\<Gamma>' \<turnstile> (App s s\<^sub>2) is (App t t\<^sub>2) : T\<^sub>2" using hb by auto |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
754 |
moreover have "(App s' s\<^sub>2) \<leadsto> (App s s\<^sub>2)" using h1 by auto |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
755 |
ultimately have "\<Gamma>' \<turnstile> App s' s\<^sub>2 is App t t\<^sub>2 : T\<^sub>2" using ih by auto |
22073 | 756 |
} |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
757 |
then show "\<Gamma> \<turnstile> s' is t : T\<^sub>1\<rightarrow>T\<^sub>2" by auto |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
758 |
qed |
22073 | 759 |
|
760 |
abbreviation |
|
22494 | 761 |
log_equiv_for_psubsts :: "Ctxt \<Rightarrow> Subst \<Rightarrow> Subst \<Rightarrow> Ctxt \<Rightarrow> bool" ("_ \<turnstile> _ is _ over _" [60,60] 60) |
22073 | 762 |
where |
22494 | 763 |
"\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma> \<equiv> \<forall>x T. (x,T) \<in> set \<Gamma> \<longrightarrow> \<Gamma>' \<turnstile> \<theta><Var x> is \<theta>'<Var x> : T" |
22073 | 764 |
|
765 |
lemma logical_pseudo_reflexivity: |
|
766 |
assumes "\<Gamma>' \<turnstile> t is s over \<Gamma>" |
|
767 |
shows "\<Gamma>' \<turnstile> s is s over \<Gamma>" |
|
768 |
proof - |
|
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
53015
diff
changeset
|
769 |
from assms have "\<Gamma>' \<turnstile> s is t over \<Gamma>" using logical_symmetry by blast |
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
53015
diff
changeset
|
770 |
with assms show "\<Gamma>' \<turnstile> s is s over \<Gamma>" using logical_transitivity by blast |
22073 | 771 |
qed |
772 |
||
773 |
lemma logical_subst_monotonicity : |
|
24231
85fb973a8207
added type constraints to resolve syntax ambiguities;
wenzelm
parents:
24088
diff
changeset
|
774 |
fixes \<Gamma> \<Gamma>' \<Gamma>'' :: Ctxt |
24070 | 775 |
assumes a: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" |
22650
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22609
diff
changeset
|
776 |
and b: "\<Gamma>' \<subseteq> \<Gamma>''" |
22494 | 777 |
and c: "valid \<Gamma>''" |
24070 | 778 |
shows "\<Gamma>'' \<turnstile> \<theta> is \<theta>' over \<Gamma>" |
22494 | 779 |
using a b c logical_monotonicity by blast |
22073 | 780 |
|
781 |
lemma equiv_subst_ext : |
|
22494 | 782 |
assumes h1: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" |
783 |
and h2: "\<Gamma>' \<turnstile> s is t : T" |
|
784 |
and fs: "x\<sharp>\<Gamma>" |
|
785 |
shows "\<Gamma>' \<turnstile> (x,s)#\<theta> is (x,t)#\<theta>' over (x,T)#\<Gamma>" |
|
22073 | 786 |
using assms |
787 |
proof - |
|
22494 | 788 |
{ |
789 |
fix y U |
|
790 |
assume "(y,U) \<in> set ((x,T)#\<Gamma>)" |
|
791 |
moreover |
|
792 |
{ |
|
793 |
assume "(y,U) \<in> set [(x,T)]" |
|
25107 | 794 |
with h2 have "\<Gamma>' \<turnstile> ((x,s)#\<theta>)<Var y> is ((x,t)#\<theta>')<Var y> : U" by auto |
22494 | 795 |
} |
796 |
moreover |
|
797 |
{ |
|
798 |
assume hl:"(y,U) \<in> set \<Gamma>" |
|
799 |
then have "\<not> y\<sharp>\<Gamma>" by (induct \<Gamma>) (auto simp add: fresh_list_cons fresh_atm fresh_prod) |
|
800 |
then have hf:"x\<sharp> Var y" using fs by (auto simp add: fresh_atm) |
|
24070 | 801 |
then have "((x,s)#\<theta>)<Var y> = \<theta><Var y>" "((x,t)#\<theta>')<Var y> = \<theta>'<Var y>" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32638
diff
changeset
|
802 |
using fresh_psubst_simp by blast+ |
22494 | 803 |
moreover have "\<Gamma>' \<turnstile> \<theta><Var y> is \<theta>'<Var y> : U" using h1 hl by auto |
24070 | 804 |
ultimately have "\<Gamma>' \<turnstile> ((x,s)#\<theta>)<Var y> is ((x,t)#\<theta>')<Var y> : U" by auto |
22494 | 805 |
} |
24070 | 806 |
ultimately have "\<Gamma>' \<turnstile> ((x,s)#\<theta>)<Var y> is ((x,t)#\<theta>')<Var y> : U" by auto |
22073 | 807 |
} |
22494 | 808 |
then show "\<Gamma>' \<turnstile> (x,s)#\<theta> is (x,t)#\<theta>' over (x,T)#\<Gamma>" by auto |
22073 | 809 |
qed |
810 |
||
22494 | 811 |
theorem fundamental_theorem_1: |
24070 | 812 |
assumes a1: "\<Gamma> \<turnstile> t : T" |
813 |
and a2: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" |
|
814 |
and a3: "valid \<Gamma>'" |
|
22494 | 815 |
shows "\<Gamma>' \<turnstile> \<theta><t> is \<theta>'<t> : T" |
24070 | 816 |
using a1 a2 a3 |
817 |
proof (nominal_induct \<Gamma> t T avoiding: \<theta> \<theta>' arbitrary: \<Gamma>' rule: typing.strong_induct) |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
818 |
case (T_Lam x \<Gamma> T\<^sub>1 t\<^sub>2 T\<^sub>2 \<theta> \<theta>' \<Gamma>') |
25107 | 819 |
have vc: "x\<sharp>\<theta>" "x\<sharp>\<theta>'" "x\<sharp>\<Gamma>" by fact+ |
24070 | 820 |
have asm1: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" by fact |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
821 |
have ih:"\<And>\<theta> \<theta>' \<Gamma>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^sub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><t\<^sub>2> is \<theta>'<t\<^sub>2> : T\<^sub>2" by fact |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
822 |
show "\<Gamma>' \<turnstile> \<theta><Lam [x].t\<^sub>2> is \<theta>'<Lam [x].t\<^sub>2> : T\<^sub>1\<rightarrow>T\<^sub>2" using vc |
24070 | 823 |
proof (simp, intro strip) |
22494 | 824 |
fix \<Gamma>'' s' t' |
24070 | 825 |
assume sub: "\<Gamma>' \<subseteq> \<Gamma>''" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
826 |
and asm2: "\<Gamma>''\<turnstile> s' is t' : T\<^sub>1" |
24070 | 827 |
and val: "valid \<Gamma>''" |
828 |
from asm1 val sub have "\<Gamma>'' \<turnstile> \<theta> is \<theta>' over \<Gamma>" using logical_subst_monotonicity by blast |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
829 |
with asm2 vc have "\<Gamma>'' \<turnstile> (x,s')#\<theta> is (x,t')#\<theta>' over (x,T\<^sub>1)#\<Gamma>" using equiv_subst_ext by blast |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
830 |
with ih val have "\<Gamma>'' \<turnstile> ((x,s')#\<theta>)<t\<^sub>2> is ((x,t')#\<theta>')<t\<^sub>2> : T\<^sub>2" by auto |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
831 |
with vc have "\<Gamma>''\<turnstile>\<theta><t\<^sub>2>[x::=s'] is \<theta>'<t\<^sub>2>[x::=t'] : T\<^sub>2" by (simp add: psubst_subst_psubst) |
24070 | 832 |
moreover |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
833 |
have "App (Lam [x].\<theta><t\<^sub>2>) s' \<leadsto> \<theta><t\<^sub>2>[x::=s']" by auto |
24070 | 834 |
moreover |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
835 |
have "App (Lam [x].\<theta>'<t\<^sub>2>) t' \<leadsto> \<theta>'<t\<^sub>2>[x::=t']" by auto |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
836 |
ultimately show "\<Gamma>''\<turnstile> App (Lam [x].\<theta><t\<^sub>2>) s' is App (Lam [x].\<theta>'<t\<^sub>2>) t' : T\<^sub>2" |
22494 | 837 |
using logical_weak_head_closure by auto |
24070 | 838 |
qed |
22073 | 839 |
qed (auto) |
840 |
||
24070 | 841 |
|
22073 | 842 |
theorem fundamental_theorem_2: |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
843 |
assumes h1: "\<Gamma> \<turnstile> s \<equiv> t : T" |
22494 | 844 |
and h2: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" |
845 |
and h3: "valid \<Gamma>'" |
|
846 |
shows "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T" |
|
847 |
using h1 h2 h3 |
|
22531 | 848 |
proof (nominal_induct \<Gamma> s t T avoiding: \<Gamma>' \<theta> \<theta>' rule: def_equiv.strong_induct) |
22494 | 849 |
case (Q_Refl \<Gamma> t T \<Gamma>' \<theta> \<theta>') |
850 |
have "\<Gamma> \<turnstile> t : T" |
|
25107 | 851 |
and "valid \<Gamma>'" by fact+ |
22494 | 852 |
moreover |
853 |
have "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" by fact |
|
854 |
ultimately show "\<Gamma>' \<turnstile> \<theta><t> is \<theta>'<t> : T" using fundamental_theorem_1 by blast |
|
22073 | 855 |
next |
22494 | 856 |
case (Q_Symm \<Gamma> t s T \<Gamma>' \<theta> \<theta>') |
857 |
have "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" |
|
25107 | 858 |
and "valid \<Gamma>'" by fact+ |
22494 | 859 |
moreover |
860 |
have ih: "\<And> \<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><t> is \<theta>'<s> : T" by fact |
|
861 |
ultimately show "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T" using logical_symmetry by blast |
|
22073 | 862 |
next |
22494 | 863 |
case (Q_Trans \<Gamma> s t T u \<Gamma>' \<theta> \<theta>') |
864 |
have ih1: "\<And> \<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T" by fact |
|
865 |
have ih2: "\<And> \<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><t> is \<theta>'<u> : T" by fact |
|
866 |
have h: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" |
|
25107 | 867 |
and v: "valid \<Gamma>'" by fact+ |
22494 | 868 |
then have "\<Gamma>' \<turnstile> \<theta>' is \<theta>' over \<Gamma>" using logical_pseudo_reflexivity by auto |
869 |
then have "\<Gamma>' \<turnstile> \<theta>'<t> is \<theta>'<u> : T" using ih2 v by auto |
|
870 |
moreover have "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T" using ih1 h v by auto |
|
871 |
ultimately show "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<u> : T" using logical_transitivity by blast |
|
872 |
next |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
873 |
case (Q_Abs x \<Gamma> T\<^sub>1 s\<^sub>2 t\<^sub>2 T\<^sub>2 \<Gamma>' \<theta> \<theta>') |
22073 | 874 |
have fs:"x\<sharp>\<Gamma>" by fact |
25107 | 875 |
have fs2: "x\<sharp>\<theta>" "x\<sharp>\<theta>'" by fact+ |
22494 | 876 |
have h2: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" |
25107 | 877 |
and h3: "valid \<Gamma>'" by fact+ |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
878 |
have ih:"\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^sub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s\<^sub>2> is \<theta>'<t\<^sub>2> : T\<^sub>2" by fact |
22073 | 879 |
{ |
880 |
fix \<Gamma>'' s' t' |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
881 |
assume "\<Gamma>' \<subseteq> \<Gamma>''" and hl:"\<Gamma>''\<turnstile> s' is t' : T\<^sub>1" and hk: "valid \<Gamma>''" |
22494 | 882 |
then have "\<Gamma>'' \<turnstile> \<theta> is \<theta>' over \<Gamma>" using h2 logical_subst_monotonicity by blast |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
883 |
then have "\<Gamma>'' \<turnstile> (x,s')#\<theta> is (x,t')#\<theta>' over (x,T\<^sub>1)#\<Gamma>" using equiv_subst_ext hl fs by blast |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
884 |
then have "\<Gamma>'' \<turnstile> ((x,s')#\<theta>)<s\<^sub>2> is ((x,t')#\<theta>')<t\<^sub>2> : T\<^sub>2" using ih hk by blast |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
885 |
then have "\<Gamma>''\<turnstile> \<theta><s\<^sub>2>[x::=s'] is \<theta>'<t\<^sub>2>[x::=t'] : T\<^sub>2" using fs2 psubst_subst_psubst by auto |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
886 |
moreover have "App (Lam [x]. \<theta><s\<^sub>2>) s' \<leadsto> \<theta><s\<^sub>2>[x::=s']" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
887 |
and "App (Lam [x].\<theta>'<t\<^sub>2>) t' \<leadsto> \<theta>'<t\<^sub>2>[x::=t']" by auto |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
888 |
ultimately have "\<Gamma>'' \<turnstile> App (Lam [x]. \<theta><s\<^sub>2>) s' is App (Lam [x].\<theta>'<t\<^sub>2>) t' : T\<^sub>2" |
22073 | 889 |
using logical_weak_head_closure by auto |
890 |
} |
|
25107 | 891 |
moreover have "valid \<Gamma>'" by fact |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
892 |
ultimately have "\<Gamma>' \<turnstile> Lam [x].\<theta><s\<^sub>2> is Lam [x].\<theta>'<t\<^sub>2> : T\<^sub>1\<rightarrow>T\<^sub>2" by auto |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
893 |
then show "\<Gamma>' \<turnstile> \<theta><Lam [x].s\<^sub>2> is \<theta>'<Lam [x].t\<^sub>2> : T\<^sub>1\<rightarrow>T\<^sub>2" using fs2 by auto |
22073 | 894 |
next |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
895 |
case (Q_App \<Gamma> s\<^sub>1 t\<^sub>1 T\<^sub>1 T\<^sub>2 s\<^sub>2 t\<^sub>2 \<Gamma>' \<theta> \<theta>') |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
896 |
then show "\<Gamma>' \<turnstile> \<theta><App s\<^sub>1 s\<^sub>2> is \<theta>'<App t\<^sub>1 t\<^sub>2> : T\<^sub>2" by auto |
22073 | 897 |
next |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
898 |
case (Q_Beta x \<Gamma> s\<^sub>2 t\<^sub>2 T\<^sub>1 s12 t12 T\<^sub>2 \<Gamma>' \<theta> \<theta>') |
22494 | 899 |
have h: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" |
25107 | 900 |
and h': "valid \<Gamma>'" by fact+ |
22494 | 901 |
have fs: "x\<sharp>\<Gamma>" by fact |
25107 | 902 |
have fs2: " x\<sharp>\<theta>" "x\<sharp>\<theta>'" by fact+ |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
903 |
have ih1: "\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s\<^sub>2> is \<theta>'<t\<^sub>2> : T\<^sub>1" by fact |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
904 |
have ih2: "\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^sub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s12> is \<theta>'<t12> : T\<^sub>2" by fact |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
905 |
have "\<Gamma>' \<turnstile> \<theta><s\<^sub>2> is \<theta>'<t\<^sub>2> : T\<^sub>1" using ih1 h' h by auto |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
906 |
then have "\<Gamma>' \<turnstile> (x,\<theta><s\<^sub>2>)#\<theta> is (x,\<theta>'<t\<^sub>2>)#\<theta>' over (x,T\<^sub>1)#\<Gamma>" using equiv_subst_ext h fs by blast |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
907 |
then have "\<Gamma>' \<turnstile> ((x,\<theta><s\<^sub>2>)#\<theta>)<s12> is ((x,\<theta>'<t\<^sub>2>)#\<theta>')<t12> : T\<^sub>2" using ih2 h' by auto |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
908 |
then have "\<Gamma>' \<turnstile> \<theta><s12>[x::=\<theta><s\<^sub>2>] is \<theta>'<t12>[x::=\<theta>'<t\<^sub>2>] : T\<^sub>2" using fs2 psubst_subst_psubst by auto |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
909 |
then have "\<Gamma>' \<turnstile> \<theta><s12>[x::=\<theta><s\<^sub>2>] is \<theta>'<t12[x::=t\<^sub>2]> : T\<^sub>2" using fs2 psubst_subst_propagate by auto |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
910 |
moreover have "App (Lam [x].\<theta><s12>) (\<theta><s\<^sub>2>) \<leadsto> \<theta><s12>[x::=\<theta><s\<^sub>2>]" by auto |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
911 |
ultimately have "\<Gamma>' \<turnstile> App (Lam [x].\<theta><s12>) (\<theta><s\<^sub>2>) is \<theta>'<t12[x::=t\<^sub>2]> : T\<^sub>2" |
22073 | 912 |
using logical_weak_head_closure' by auto |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
913 |
then show "\<Gamma>' \<turnstile> \<theta><App (Lam [x].s12) s\<^sub>2> is \<theta>'<t12[x::=t\<^sub>2]> : T\<^sub>2" using fs2 by simp |
22073 | 914 |
next |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
915 |
case (Q_Ext x \<Gamma> s t T\<^sub>1 T\<^sub>2 \<Gamma>' \<theta> \<theta>') |
22494 | 916 |
have h2: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" |
25107 | 917 |
and h2': "valid \<Gamma>'" by fact+ |
918 |
have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact+ |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
919 |
have ih:"\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^sub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
920 |
\<Longrightarrow> \<Gamma>' \<turnstile> \<theta><App s (Var x)> is \<theta>'<App t (Var x)> : T\<^sub>2" by fact |
22073 | 921 |
{ |
922 |
fix \<Gamma>'' s' t' |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
923 |
assume hsub: "\<Gamma>' \<subseteq> \<Gamma>''" and hl: "\<Gamma>''\<turnstile> s' is t' : T\<^sub>1" and hk: "valid \<Gamma>''" |
22494 | 924 |
then have "\<Gamma>'' \<turnstile> \<theta> is \<theta>' over \<Gamma>" using h2 logical_subst_monotonicity by blast |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
925 |
then have "\<Gamma>'' \<turnstile> (x,s')#\<theta> is (x,t')#\<theta>' over (x,T\<^sub>1)#\<Gamma>" using equiv_subst_ext hl fs by blast |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
926 |
then have "\<Gamma>'' \<turnstile> ((x,s')#\<theta>)<App s (Var x)> is ((x,t')#\<theta>')<App t (Var x)> : T\<^sub>2" using ih hk by blast |
22494 | 927 |
then |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
928 |
have "\<Gamma>'' \<turnstile> App (((x,s')#\<theta>)<s>) (((x,s')#\<theta>)<(Var x)>) is App (((x,t')#\<theta>')<t>) (((x,t')#\<theta>')<(Var x)>) : T\<^sub>2" |
22082 | 929 |
by auto |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
930 |
then have "\<Gamma>'' \<turnstile> App ((x,s')#\<theta>)<s> s' is App ((x,t')#\<theta>')<t> t' : T\<^sub>2" by auto |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
931 |
then have "\<Gamma>'' \<turnstile> App (\<theta><s>) s' is App (\<theta>'<t>) t' : T\<^sub>2" using fs fresh_psubst_simp by auto |
22073 | 932 |
} |
25107 | 933 |
moreover have "valid \<Gamma>'" by fact |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49171
diff
changeset
|
934 |
ultimately show "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T\<^sub>1\<rightarrow>T\<^sub>2" by auto |
23370
513a8ee192f1
added the Q_Unit rule (was missing) and adjusted the proof accordingly
urbanc
parents:
22829
diff
changeset
|
935 |
next |
513a8ee192f1
added the Q_Unit rule (was missing) and adjusted the proof accordingly
urbanc
parents:
22829
diff
changeset
|
936 |
case (Q_Unit \<Gamma> s t \<Gamma>' \<theta> \<theta>') |
513a8ee192f1
added the Q_Unit rule (was missing) and adjusted the proof accordingly
urbanc
parents:
22829
diff
changeset
|
937 |
then show "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : TUnit" by auto |
22073 | 938 |
qed |
939 |
||
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
940 |
|
22073 | 941 |
theorem completeness: |
22494 | 942 |
assumes asm: "\<Gamma> \<turnstile> s \<equiv> t : T" |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
943 |
shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T" |
22073 | 944 |
proof - |
22494 | 945 |
have val: "valid \<Gamma>" using def_equiv_implies_valid asm by simp |
946 |
moreover |
|
22073 | 947 |
{ |
948 |
fix x T |
|
949 |
assume "(x,T) \<in> set \<Gamma>" "valid \<Gamma>" |
|
22494 | 950 |
then have "\<Gamma> \<turnstile> Var x is Var x : T" using main_lemma(2) by blast |
22073 | 951 |
} |
952 |
ultimately have "\<Gamma> \<turnstile> [] is [] over \<Gamma>" by auto |
|
22494 | 953 |
then have "\<Gamma> \<turnstile> []<s> is []<t> : T" using fundamental_theorem_2 val asm by blast |
22073 | 954 |
then have "\<Gamma> \<turnstile> s is t : T" by simp |
22494 | 955 |
then show "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T" using main_lemma(1) val by simp |
22073 | 956 |
qed |
957 |
||
63167 | 958 |
text \<open>We leave soundness as an exercise - just like Crary in the ATS book :-) \\ |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
959 |
@{prop[mode=IfThen] "\<lbrakk>\<Gamma> \<turnstile> s \<Leftrightarrow> t : T; \<Gamma> \<turnstile> t : T; \<Gamma> \<turnstile> s : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T"} \\ |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22231
diff
changeset
|
960 |
@{prop "\<lbrakk>\<Gamma> \<turnstile> s \<leftrightarrow> t : T; \<Gamma> \<turnstile> t : T; \<Gamma> \<turnstile> s : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T"} |
63167 | 961 |
\<close> |
22073 | 962 |
|
963 |
end |
|
964 |