author | urbanc |
Thu, 01 Dec 2005 04:46:17 +0100 | |
changeset 18311 | b83b00cbaecf |
parent 18296 | 3dcc34f18bfa |
child 18346 | c9be8266325f |
permissions | -rw-r--r-- |
18269 | 1 |
(* $Id$ *) |
18105 | 2 |
|
18269 | 3 |
theory weakening |
18105 | 4 |
imports "../nominal" |
5 |
begin |
|
6 |
||
7 |
(* WEAKENING EXAMPLE*) |
|
8 |
||
9 |
section {* Simply-Typed Lambda-Calculus *} |
|
10 |
(*======================================*) |
|
11 |
||
12 |
atom_decl name |
|
13 |
||
14 |
nominal_datatype lam = Var "name" |
|
15 |
| App "lam" "lam" |
|
16 |
| Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) |
|
17 |
||
18 |
datatype ty = |
|
19 |
TVar "string" |
|
20 |
| TArr "ty" "ty" (infix "\<rightarrow>" 200) |
|
21 |
||
22 |
primrec |
|
23 |
"pi\<bullet>(TVar s) = TVar s" |
|
24 |
"pi\<bullet>(\<tau> \<rightarrow> \<sigma>) = (\<tau> \<rightarrow> \<sigma>)" |
|
25 |
||
26 |
lemma perm_ty[simp]: |
|
27 |
fixes pi ::"name prm" |
|
28 |
and \<tau> ::"ty" |
|
29 |
shows "pi\<bullet>\<tau> = \<tau>" |
|
30 |
by (cases \<tau>, simp_all) |
|
31 |
||
32 |
instance ty :: pt_name |
|
33 |
apply(intro_classes) |
|
34 |
apply(simp_all) |
|
35 |
done |
|
36 |
||
37 |
instance ty :: fs_name |
|
38 |
apply(intro_classes) |
|
39 |
apply(simp add: supp_def) |
|
40 |
done |
|
41 |
||
42 |
(* valid contexts *) |
|
43 |
consts |
|
44 |
ctxts :: "((name\<times>ty) list) set" |
|
45 |
valid :: "(name\<times>ty) list \<Rightarrow> bool" |
|
46 |
translations |
|
47 |
"valid \<Gamma>" \<rightleftharpoons> "\<Gamma> \<in> ctxts" |
|
48 |
inductive ctxts |
|
49 |
intros |
|
50 |
v1[intro]: "valid []" |
|
51 |
v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)" |
|
52 |
||
53 |
lemma eqvt_valid: |
|
54 |
fixes pi:: "name prm" |
|
55 |
assumes a: "valid \<Gamma>" |
|
56 |
shows "valid (pi\<bullet>\<Gamma>)" |
|
57 |
using a |
|
58 |
apply(induct) |
|
59 |
apply(auto simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst]) |
|
60 |
done |
|
61 |
||
62 |
(* typing judgements *) |
|
63 |
consts |
|
64 |
typing :: "(((name\<times>ty) list)\<times>lam\<times>ty) set" |
|
65 |
syntax |
|
66 |
"_typing_judge" :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80) |
|
67 |
translations |
|
68 |
"\<Gamma> \<turnstile> t : \<tau>" \<rightleftharpoons> "(\<Gamma>,t,\<tau>) \<in> typing" |
|
69 |
||
70 |
inductive typing |
|
71 |
intros |
|
72 |
t1[intro]: "\<lbrakk>valid \<Gamma>; (a,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var a : \<tau>" |
|
73 |
t2[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>" |
|
74 |
t3[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>" |
|
75 |
||
76 |
lemma eqvt_typing: |
|
77 |
fixes \<Gamma> :: "(name\<times>ty) list" |
|
78 |
and t :: "lam" |
|
79 |
and \<tau> :: "ty" |
|
80 |
and pi:: "name prm" |
|
81 |
assumes a: "\<Gamma> \<turnstile> t : \<tau>" |
|
82 |
shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>t) : \<tau>" |
|
83 |
using a |
|
84 |
proof (induct) |
|
85 |
case (t1 \<Gamma> \<tau> a) |
|
86 |
have "valid (pi\<bullet>\<Gamma>)" by (rule eqvt_valid) |
|
87 |
moreover |
|
88 |
have "(pi\<bullet>(a,\<tau>))\<in>((pi::name prm)\<bullet>set \<Gamma>)" by (rule pt_set_bij2[OF pt_name_inst, OF at_name_inst]) |
|
89 |
ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> ((pi::name prm)\<bullet>Var a) : \<tau>" |
|
90 |
using typing.intros by (force simp add: pt_list_set_pi[OF pt_name_inst, symmetric]) |
|
91 |
next |
|
92 |
case (t3 \<Gamma> \<sigma> \<tau> a t) |
|
93 |
moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (rule pt_fresh_bij1[OF pt_name_inst, OF at_name_inst]) |
|
94 |
ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) :\<tau>\<rightarrow>\<sigma>" by force |
|
95 |
qed (auto) |
|
96 |
||
18296 | 97 |
lemma typing_induct[consumes 1, case_names t1 t2 t3]: |
98 |
fixes P :: "'a::fs_name\<Rightarrow>(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow>bool" |
|
18105 | 99 |
and \<Gamma> :: "(name\<times>ty) list" |
100 |
and t :: "lam" |
|
101 |
and \<tau> :: "ty" |
|
102 |
and x :: "'a::fs_name" |
|
103 |
assumes a: "\<Gamma> \<turnstile> t : \<tau>" |
|
18296 | 104 |
and a1: "\<And>\<Gamma> (a::name) \<tau> x. valid \<Gamma> \<Longrightarrow> (a,\<tau>) \<in> set \<Gamma> \<Longrightarrow> P x \<Gamma> (Var a) \<tau>" |
105 |
and a2: "\<And>\<Gamma> \<tau> \<sigma> t1 t2 x. |
|
106 |
\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma> \<Longrightarrow> (\<And>z. P z \<Gamma> t1 (\<tau>\<rightarrow>\<sigma>)) \<Longrightarrow> \<Gamma> \<turnstile> t2 : \<tau> \<Longrightarrow> (\<And>z. P z \<Gamma> t2 \<tau>) |
|
107 |
\<Longrightarrow> P x \<Gamma> (App t1 t2) \<sigma>" |
|
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
108 |
and a3: "\<And>a \<Gamma> \<tau> \<sigma> t x. a\<sharp>x \<Longrightarrow> a\<sharp>\<Gamma> \<Longrightarrow> ((a,\<tau>) # \<Gamma>) \<turnstile> t : \<sigma> \<Longrightarrow> (\<And>z. P z ((a,\<tau>)#\<Gamma>) t \<sigma>) |
18296 | 109 |
\<Longrightarrow> P x \<Gamma> (Lam [a].t) (\<tau>\<rightarrow>\<sigma>)" |
110 |
shows "P x \<Gamma> t \<tau>" |
|
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
111 |
proof - |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
112 |
from a have "\<And>(pi::name prm) x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>t) \<tau>" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
113 |
proof (induct) |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
114 |
case (t1 \<Gamma> \<tau> a) |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
115 |
have j1: "valid \<Gamma>" by fact |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
116 |
have j2: "(a,\<tau>)\<in>set \<Gamma>" by fact |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
117 |
from j1 have j3: "valid (pi\<bullet>\<Gamma>)" by (rule eqvt_valid) |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
118 |
from j2 have "pi\<bullet>(a,\<tau>)\<in>pi\<bullet>(set \<Gamma>)" by (simp only: pt_set_bij[OF pt_name_inst, OF at_name_inst]) |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
119 |
hence j4: "(pi\<bullet>a,\<tau>)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: pt_list_set_pi[OF pt_name_inst]) |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
120 |
show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Var a)) \<tau>" using a1 j3 j4 by simp |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
121 |
next |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
122 |
case (t2 \<Gamma> \<sigma> \<tau> t1 t2) |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
123 |
thus ?case using a2 by (simp, blast intro: eqvt_typing) |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
124 |
next |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
125 |
case (t3 \<Gamma> \<sigma> \<tau> a t) |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
126 |
have k1: "a\<sharp>\<Gamma>" by fact |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
127 |
have k2: "((a,\<tau>)#\<Gamma>)\<turnstile>t:\<sigma>" by fact |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
128 |
have k3: "\<And>(pi::name prm) (x::'a::fs_name). P x (pi \<bullet>((a,\<tau>)#\<Gamma>)) (pi\<bullet>t) \<sigma>" by fact |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
129 |
have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t,pi\<bullet>\<Gamma>,x)" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
130 |
by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1) |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
131 |
then obtain c::"name" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
132 |
where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>t)" and f4: "c\<sharp>(pi\<bullet>\<Gamma>)" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
133 |
by (force simp add: fresh_prod at_fresh[OF at_name_inst]) |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
134 |
from k1 have k1a: "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
135 |
by (simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst] |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
136 |
pt_rev_pi[OF pt_name_inst, OF at_name_inst]) |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
137 |
have l1: "(([(c,pi\<bullet>a)]@pi)\<bullet>\<Gamma>) = (pi\<bullet>\<Gamma>)" using f4 k1a |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
138 |
by (simp only: pt2[OF pt_name_inst], rule pt_fresh_fresh[OF pt_name_inst, OF at_name_inst]) |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
139 |
have "\<And>x. P x (([(c,pi\<bullet>a)]@pi)\<bullet>((a,\<tau>)#\<Gamma>)) (([(c,pi\<bullet>a)]@pi)\<bullet>t) \<sigma>" using k3 by force |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
140 |
hence l2: "\<And>x. P x ((c, \<tau>)#(pi\<bullet>\<Gamma>)) (([(c,pi\<bullet>a)]@pi)\<bullet>t) \<sigma>" using f1 l1 |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
141 |
by (force simp add: pt2[OF pt_name_inst] at_calc[OF at_name_inst]) |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
142 |
have "(([(c,pi\<bullet>a)]@pi)\<bullet>((a,\<tau>)#\<Gamma>)) \<turnstile> (([(c,pi\<bullet>a)]@pi)\<bullet>t) : \<sigma>" using k2 by (rule eqvt_typing) |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
143 |
hence l3: "((c, \<tau>)#(pi\<bullet>\<Gamma>)) \<turnstile> (([(c,pi\<bullet>a)]@pi)\<bullet>t) : \<sigma>" using l1 f1 |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
144 |
by (force simp add: pt2[OF pt_name_inst] at_calc[OF at_name_inst]) |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
145 |
have l4: "P x (pi\<bullet>\<Gamma>) (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>t)) (\<tau> \<rightarrow> \<sigma>)" using f2 f4 l2 l3 a3 by auto |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
146 |
have alpha: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t))) = (Lam [(pi\<bullet>a)].(pi\<bullet>t))" using f1 f3 |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
147 |
by (simp add: lam.inject alpha) |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
148 |
show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Lam [a].t)) (\<tau> \<rightarrow> \<sigma>)" using l4 alpha |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
149 |
by (simp only: pt2[OF pt_name_inst], simp) |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
150 |
qed |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
151 |
hence "P x (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>t) \<tau>" by blast |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
152 |
thus "P x \<Gamma> t \<tau>" by simp |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
153 |
qed |
18105 | 154 |
|
155 |
(* Now it comes: The Weakening Lemma *) |
|
156 |
||
157 |
constdefs |
|
158 |
"sub" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" (" _ \<lless> _ " [80,80] 80) |
|
159 |
"\<Gamma>1 \<lless> \<Gamma>2 \<equiv> \<forall>a \<sigma>. (a,\<sigma>)\<in>set \<Gamma>1 \<longrightarrow> (a,\<sigma>)\<in>set \<Gamma>2" |
|
160 |
||
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
161 |
lemma weakening_version1: |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
162 |
assumes a: "\<Gamma>1 \<turnstile> t : \<sigma>" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
163 |
and b: "valid \<Gamma>2" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
164 |
and c: "\<Gamma>1 \<lless> \<Gamma>2" |
18296 | 165 |
shows "\<Gamma>2 \<turnstile> t:\<sigma>" |
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
166 |
using a b c |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
167 |
apply(nominal_induct \<Gamma>1 t \<sigma> avoiding: \<Gamma>2 rule: typing_induct) |
18105 | 168 |
apply(auto simp add: sub_def) |
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
169 |
(* FIXME: before using meta-connectives and the new induction *) |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
170 |
(* method, this was completely automatic *) |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
171 |
apply(atomize) |
18296 | 172 |
apply(auto) |
18105 | 173 |
done |
174 |
||
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
175 |
lemma weakening_version2: |
18105 | 176 |
fixes \<Gamma>1::"(name\<times>ty) list" |
177 |
and t ::"lam" |
|
178 |
and \<tau> ::"ty" |
|
179 |
assumes a: "\<Gamma>1 \<turnstile> t:\<sigma>" |
|
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
180 |
and b: "valid \<Gamma>2" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
181 |
and c: "\<Gamma>1 \<lless> \<Gamma>2" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
182 |
shows "\<Gamma>2 \<turnstile> t:\<sigma>" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
183 |
using a b c |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
184 |
proof (nominal_induct \<Gamma>1 t \<sigma> avoiding: \<Gamma>2 rule: typing_induct, auto) |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
185 |
case (t1 \<Gamma>1 a \<tau>) (* variable case *) |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
186 |
have "\<Gamma>1 \<lless> \<Gamma>2" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
187 |
and "valid \<Gamma>2" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
188 |
and "(a,\<tau>)\<in> set \<Gamma>1" by fact+ |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
189 |
thus "\<Gamma>2 \<turnstile> Var a : \<tau>" by (force simp add: sub_def) |
18105 | 190 |
next |
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
191 |
case (t3 a \<Gamma>1 \<tau> \<sigma> t) (* lambda case *) |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
192 |
have a1: "\<Gamma>1 \<lless> \<Gamma>2" by fact |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
193 |
have a2: "valid \<Gamma>2" by fact |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
194 |
have a3: "a\<sharp>\<Gamma>2" by fact |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
195 |
have ih: "\<And>\<Gamma>3. valid \<Gamma>3 \<Longrightarrow> ((a,\<tau>)#\<Gamma>1) \<lless> \<Gamma>3 \<Longrightarrow> \<Gamma>3 \<turnstile> t:\<sigma>" by fact |
18105 | 196 |
have "((a,\<tau>)#\<Gamma>1) \<lless> ((a,\<tau>)#\<Gamma>2)" using a1 by (simp add: sub_def) |
197 |
moreover |
|
198 |
have "valid ((a,\<tau>)#\<Gamma>2)" using a2 a3 v2 by force |
|
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
199 |
ultimately have "((a,\<tau>)#\<Gamma>2) \<turnstile> t:\<sigma>" using ih by force |
18105 | 200 |
with a3 show "\<Gamma>2 \<turnstile> (Lam [a].t) : \<tau> \<rightarrow> \<sigma>" by force |
201 |
qed |
|
202 |
||
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
203 |
lemma weakening_version3: |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
204 |
assumes a: "\<Gamma>1 \<turnstile> t:\<sigma>" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
205 |
and b: "valid \<Gamma>2" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
206 |
and c: "\<Gamma>1 \<lless> \<Gamma>2" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
207 |
shows "\<Gamma>2 \<turnstile> t:\<sigma>" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
208 |
using a b c |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
209 |
proof (nominal_induct \<Gamma>1 t \<sigma> avoiding: \<Gamma>2 rule: typing_induct) |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
210 |
case (t3 a \<Gamma>1 \<tau> \<sigma> t) (* lambda case *) |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
211 |
have fc: "a\<sharp>\<Gamma>2" by fact |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
212 |
have ih: "\<And>\<Gamma>3. valid \<Gamma>3 \<Longrightarrow> ((a,\<tau>)#\<Gamma>1) \<lless> \<Gamma>3 \<Longrightarrow> \<Gamma>3 \<turnstile> t:\<sigma>" by fact |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
213 |
have a1: "\<Gamma>1 \<lless> \<Gamma>2" by fact |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
214 |
have a2: "valid \<Gamma>2" by fact |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
215 |
have "((a,\<tau>)#\<Gamma>1) \<lless> ((a,\<tau>)#\<Gamma>2)" using a1 sub_def by simp |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
216 |
moreover |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
217 |
have "valid ((a,\<tau>)#\<Gamma>2)" using a2 fc by force |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
218 |
ultimately have "((a,\<tau>)#\<Gamma>2) \<turnstile> t:\<sigma>" using ih by force |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
219 |
with fc show "\<Gamma>2 \<turnstile> (Lam [a].t) : \<tau> \<rightarrow> \<sigma>" by force |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
220 |
qed (auto simp add: sub_def) (* app and var case *) |
18105 | 221 |
|
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
222 |
text{* The original induction principle for typing |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
223 |
is not strong enough - so the simple proof fails *} |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
224 |
lemma weakening_too_weak: |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
225 |
assumes a: "\<Gamma>1 \<turnstile> t:\<sigma>" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
226 |
and b: "valid \<Gamma>2" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
227 |
and c: "\<Gamma>1 \<lless> \<Gamma>2" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
228 |
shows "\<Gamma>2 \<turnstile> t:\<sigma>" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
229 |
using a b c |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
230 |
proof (induct fixing: \<Gamma>2) |
18296 | 231 |
case (t1 \<Gamma>1 \<tau> a) (* variable case *) |
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
232 |
have "\<Gamma>1 \<lless> \<Gamma>2" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
233 |
and "valid \<Gamma>2" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
234 |
and "(a,\<tau>) \<in> (set \<Gamma>1)" by fact+ |
18105 | 235 |
thus "\<Gamma>2 \<turnstile> Var a : \<tau>" by (force simp add: sub_def) |
236 |
next |
|
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
237 |
case (t3 \<Gamma>1 \<sigma> \<tau> a t) (* lambda case *) |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
238 |
(* all assumption in this case*) |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
239 |
have a0: "a\<sharp>\<Gamma>1" by fact |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
240 |
have a1: "((a,\<tau>)#\<Gamma>1) \<turnstile> t : \<sigma>" by fact |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
241 |
have a2: "\<Gamma>1 \<lless> \<Gamma>2" by fact |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
242 |
have a3: "valid \<Gamma>2" by fact |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
243 |
have ih: "\<And>\<Gamma>3. valid \<Gamma>3 \<Longrightarrow> ((a,\<tau>)#\<Gamma>1) \<lless> \<Gamma>3 \<Longrightarrow> \<Gamma>3 \<turnstile> t:\<sigma>" by fact |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
244 |
have "((a,\<tau>)#\<Gamma>1) \<lless> ((a,\<tau>)#\<Gamma>2)" using a2 by (simp add: sub_def) |
18105 | 245 |
moreover |
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
246 |
have "valid ((a,\<tau>)#\<Gamma>2)" using v2 (* fails *) |
18105 | 247 |
|
248 |
||
249 |