author | urbanc |
Thu, 23 Nov 2006 14:11:49 +0100 | |
changeset 21487 | 45f9163d79e7 |
parent 21405 | 26b51f724fe6 |
child 21488 | e1b260d204a0 |
permissions | -rw-r--r-- |
18269 | 1 |
(* $Id$ *) |
18105 | 2 |
|
19496 | 3 |
theory Weakening |
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
4 |
imports "Nominal" |
18105 | 5 |
begin |
6 |
||
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
7 |
section {* Weakening Example for the Simply-Typed Lambda-Calculus *} |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
8 |
(*================================================================*) |
18105 | 9 |
|
10 |
atom_decl name |
|
11 |
||
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
12 |
nominal_datatype lam = |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
13 |
Var "name" |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
14 |
| App "lam" "lam" |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
15 |
| Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) |
18105 | 16 |
|
18352 | 17 |
nominal_datatype ty = |
18 |
TVar "nat" |
|
18105 | 19 |
| TArr "ty" "ty" (infix "\<rightarrow>" 200) |
20 |
||
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
21 |
lemma [simp]: |
18105 | 22 |
fixes pi ::"name prm" |
23 |
and \<tau> ::"ty" |
|
24 |
shows "pi\<bullet>\<tau> = \<tau>" |
|
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
25 |
by (induct \<tau> rule: ty.induct_weak) |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
26 |
(simp_all add: perm_nat_def) |
18105 | 27 |
|
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
28 |
text {* valid contexts *} |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
29 |
inductive2 |
18105 | 30 |
valid :: "(name\<times>ty) list \<Rightarrow> bool" |
21364 | 31 |
where |
32 |
v1[intro]: "valid []" |
|
33 |
| v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)" |
|
18105 | 34 |
|
35 |
lemma eqvt_valid: |
|
36 |
fixes pi:: "name prm" |
|
37 |
assumes a: "valid \<Gamma>" |
|
38 |
shows "valid (pi\<bullet>\<Gamma>)" |
|
39 |
using a |
|
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
40 |
by (induct) |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
41 |
(auto simp add: fresh_bij) |
18105 | 42 |
|
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
43 |
text{* typing judgements *} |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
44 |
inductive2 |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
45 |
typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80) |
21364 | 46 |
where |
47 |
t_Var[intro]: "\<lbrakk>valid \<Gamma>; (a,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var a : \<tau>" |
|
48 |
| t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>" |
|
49 |
| t_Lam[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>" |
|
18105 | 50 |
|
51 |
lemma eqvt_typing: |
|
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
52 |
fixes pi:: "name prm" |
18105 | 53 |
assumes a: "\<Gamma> \<turnstile> t : \<tau>" |
54 |
shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>t) : \<tau>" |
|
55 |
using a |
|
56 |
proof (induct) |
|
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
57 |
case (t_Var \<Gamma> a \<tau>) |
18105 | 58 |
have "valid (pi\<bullet>\<Gamma>)" by (rule eqvt_valid) |
59 |
moreover |
|
60 |
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]) |
|
61 |
ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> ((pi::name prm)\<bullet>Var a) : \<tau>" |
|
62 |
using typing.intros by (force simp add: pt_list_set_pi[OF pt_name_inst, symmetric]) |
|
63 |
next |
|
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
64 |
case (t_Lam a \<Gamma> \<tau> t \<sigma>) |
19972
89c5afe4139a
added more infrastructure for the recursion combinator
urbanc
parents:
19496
diff
changeset
|
65 |
moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_bij) |
18105 | 66 |
ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) :\<tau>\<rightarrow>\<sigma>" by force |
67 |
qed (auto) |
|
68 |
||
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
69 |
text {* the strong induction principle needs to be derived manually *} |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
70 |
|
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
71 |
lemma typing_induct[consumes 1, case_names t_Var t_App t_Lam]: |
18296 | 72 |
fixes P :: "'a::fs_name\<Rightarrow>(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow>bool" |
18105 | 73 |
and \<Gamma> :: "(name\<times>ty) list" |
74 |
and t :: "lam" |
|
75 |
and \<tau> :: "ty" |
|
76 |
and x :: "'a::fs_name" |
|
77 |
assumes a: "\<Gamma> \<turnstile> t : \<tau>" |
|
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
78 |
and a1: "\<And>\<Gamma> a \<tau> x. \<lbrakk>valid \<Gamma>; (a,\<tau>) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> P x \<Gamma> (Var a) \<tau>" |
18296 | 79 |
and a2: "\<And>\<Gamma> \<tau> \<sigma> t1 t2 x. |
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
80 |
\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; (\<And>z. P z \<Gamma> t1 (\<tau>\<rightarrow>\<sigma>)); \<Gamma> \<turnstile> t2 : \<tau>; (\<And>z. P z \<Gamma> t2 \<tau>)\<rbrakk> |
18296 | 81 |
\<Longrightarrow> P x \<Gamma> (App t1 t2) \<sigma>" |
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
82 |
and a3: "\<And>a \<Gamma> \<tau> \<sigma> t x. \<lbrakk>a\<sharp>x; a\<sharp>\<Gamma>; ((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>; (\<And>z. P z ((a,\<tau>)#\<Gamma>) t \<sigma>)\<rbrakk> |
18296 | 83 |
\<Longrightarrow> P x \<Gamma> (Lam [a].t) (\<tau>\<rightarrow>\<sigma>)" |
84 |
shows "P x \<Gamma> t \<tau>" |
|
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
85 |
proof - |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
86 |
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
|
87 |
proof (induct) |
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
88 |
case (t_Var \<Gamma> a \<tau>) |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
89 |
have "valid \<Gamma>" by fact |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
90 |
then have "valid (pi\<bullet>\<Gamma>)" by (rule eqvt_valid) |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
91 |
moreover |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
92 |
have "(a,\<tau>)\<in>set \<Gamma>" by fact |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
93 |
then have "pi\<bullet>(a,\<tau>)\<in>pi\<bullet>(set \<Gamma>)" by (simp only: pt_set_bij[OF pt_name_inst, OF at_name_inst]) |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
94 |
then have "(pi\<bullet>a,\<tau>)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: pt_list_set_pi[OF pt_name_inst]) |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
95 |
ultimately show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Var a)) \<tau>" using a1 by simp |
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
96 |
next |
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
97 |
case (t_App \<Gamma> t1 \<tau> \<sigma> t2) |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
98 |
thus "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(App t1 t2)) \<sigma>" using a2 by (simp, blast intro: eqvt_typing) |
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
99 |
next |
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
100 |
case (t_Lam a \<Gamma> \<tau> t \<sigma>) |
21487 | 101 |
obtain c::"name" where fs: "c\<sharp>(pi\<bullet>a,pi\<bullet>t,pi\<bullet>\<Gamma>,x)" by (rule exists_fresh[OF fs_name1]) |
102 |
let ?sw="[(pi\<bullet>a,c)]" |
|
103 |
let ?pi'="?sw@pi" |
|
104 |
have f1: "a\<sharp>\<Gamma>" by fact |
|
105 |
have f2: "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" using f1 by (simp add: fresh_bij) |
|
106 |
have f3: "c\<sharp>?pi'\<bullet>\<Gamma>" using f1 by (auto simp add: pt_name2 fresh_left calc_atm perm_pi_simp) |
|
107 |
have pr1: "((a,\<tau>)#\<Gamma>)\<turnstile>t:\<sigma>" by fact |
|
108 |
then have "(?pi'\<bullet>((a,\<tau>)#\<Gamma>)) \<turnstile> (?pi'\<bullet>t) : \<sigma>" by (rule eqvt_typing) |
|
109 |
then have "((c,\<tau>)#(?pi'\<bullet>\<Gamma>)) \<turnstile> (?pi'\<bullet>t) : \<sigma>" by (simp add: calc_atm) |
|
110 |
moreover |
|
111 |
have ih1: "\<And>x. P x (?pi'\<bullet>((a,\<tau>)#\<Gamma>)) (?pi'\<bullet>t) \<sigma>" by fact |
|
112 |
then have "\<And>x. P x ((c,\<tau>)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>t) \<sigma>" by (simp add: calc_atm) |
|
113 |
ultimately have "P x (?pi'\<bullet>\<Gamma>) (Lam [c].(?pi'\<bullet>t)) (\<tau> \<rightarrow> \<sigma>)" using a3 f3 fs by simp |
|
114 |
then have "P x (?sw\<bullet>pi\<bullet>\<Gamma>) (?sw\<bullet>(Lam [(pi\<bullet>a)].(pi\<bullet>t))) (\<tau> \<rightarrow> \<sigma>)" |
|
115 |
by (simp del: append_Cons add: calc_atm pt_name2) |
|
116 |
moreover have "(?sw\<bullet>(pi\<bullet>\<Gamma>)) = (pi\<bullet>\<Gamma>)" |
|
117 |
by (rule perm_fresh_fresh) (simp_all add: fs f2) |
|
118 |
moreover have "(?sw\<bullet>(Lam [(pi\<bullet>a)].(pi\<bullet>t))) = Lam [(pi\<bullet>a)].(pi\<bullet>t)" |
|
119 |
by (rule perm_fresh_fresh) (simp_all add: fs f2 abs_fresh) |
|
120 |
ultimately show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Lam [a].t)) (\<tau> \<rightarrow> \<sigma>)" by (simp only: , simp) |
|
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
121 |
qed |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
122 |
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
|
123 |
thus "P x \<Gamma> t \<tau>" by simp |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
124 |
qed |
18105 | 125 |
|
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
126 |
text {* definition of a subcontext *} |
18105 | 127 |
|
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
128 |
abbreviation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21377
diff
changeset
|
129 |
"sub" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" (" _ \<lless> _ " [80,80] 80) where |
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
130 |
"\<Gamma>1 \<lless> \<Gamma>2 \<equiv> \<forall>a \<sigma>. (a,\<sigma>)\<in>set \<Gamma>1 \<longrightarrow> (a,\<sigma>)\<in>set \<Gamma>2" |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
131 |
|
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
132 |
text {* Now it comes: The Weakening Lemma *} |
18105 | 133 |
|
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
134 |
lemma weakening_version1: |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
135 |
assumes a: "\<Gamma>1 \<turnstile> t : \<sigma>" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
136 |
and b: "valid \<Gamma>2" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
137 |
and c: "\<Gamma>1 \<lless> \<Gamma>2" |
18296 | 138 |
shows "\<Gamma>2 \<turnstile> t:\<sigma>" |
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
139 |
using a b c |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
140 |
apply(nominal_induct \<Gamma>1 t \<sigma> avoiding: \<Gamma>2 rule: typing_induct) |
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
141 |
apply(auto | atomize)+ |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
142 |
(* FIXME: meta-quantifiers seem to not ba as "automatic" as object-quantifiers *) |
18105 | 143 |
done |
144 |
||
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
145 |
lemma weakening_version2: |
18105 | 146 |
fixes \<Gamma>1::"(name\<times>ty) list" |
147 |
and t ::"lam" |
|
148 |
and \<tau> ::"ty" |
|
149 |
assumes a: "\<Gamma>1 \<turnstile> t:\<sigma>" |
|
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
150 |
and b: "valid \<Gamma>2" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
151 |
and c: "\<Gamma>1 \<lless> \<Gamma>2" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
152 |
shows "\<Gamma>2 \<turnstile> t:\<sigma>" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
153 |
using a b c |
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
154 |
proof (nominal_induct \<Gamma>1 t \<sigma> avoiding: \<Gamma>2 rule: typing_induct) |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
155 |
case (t_Var \<Gamma>1 a \<tau>) (* variable case *) |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
156 |
have "\<Gamma>1 \<lless> \<Gamma>2" by fact |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
157 |
moreover |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
158 |
have "valid \<Gamma>2" by fact |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
159 |
moreover |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
160 |
have "(a,\<tau>)\<in> set \<Gamma>1" by fact |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
161 |
ultimately show "\<Gamma>2 \<turnstile> Var a : \<tau>" by auto |
18105 | 162 |
next |
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
163 |
case (t_Lam a \<Gamma>1 \<tau> \<sigma> t) (* lambda case *) |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
164 |
have vc: "a\<sharp>\<Gamma>2" by fact (* variable convention *) |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
165 |
have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; ((a,\<tau>)#\<Gamma>1) \<lless> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t:\<sigma>" by fact |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
166 |
have "\<Gamma>1 \<lless> \<Gamma>2" by fact |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
167 |
then have "((a,\<tau>)#\<Gamma>1) \<lless> ((a,\<tau>)#\<Gamma>2)" by simp |
18105 | 168 |
moreover |
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
169 |
have "valid \<Gamma>2" by fact |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
170 |
then have "valid ((a,\<tau>)#\<Gamma>2)" using vc v2 by simp |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
171 |
ultimately have "((a,\<tau>)#\<Gamma>2) \<turnstile> t:\<sigma>" using ih by simp |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
172 |
with vc show "\<Gamma>2 \<turnstile> (Lam [a].t) : \<tau> \<rightarrow> \<sigma>" by auto |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
173 |
qed (auto) |
18105 | 174 |
|
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
175 |
lemma weakening_version3: |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
176 |
assumes a: "\<Gamma>1 \<turnstile> t:\<sigma>" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
177 |
and b: "valid \<Gamma>2" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
178 |
and c: "\<Gamma>1 \<lless> \<Gamma>2" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
179 |
shows "\<Gamma>2 \<turnstile> t:\<sigma>" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
180 |
using a b c |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
181 |
proof (nominal_induct \<Gamma>1 t \<sigma> avoiding: \<Gamma>2 rule: typing_induct) |
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
182 |
case (t_Lam a \<Gamma>1 \<tau> \<sigma> t) (* lambda case *) |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
183 |
have vc: "a\<sharp>\<Gamma>2" by fact (* variable convention *) |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
184 |
have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; ((a,\<tau>)#\<Gamma>1) \<lless> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t:\<sigma>" by fact |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
185 |
have "\<Gamma>1 \<lless> \<Gamma>2" by fact |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
186 |
then have "((a,\<tau>)#\<Gamma>1) \<lless> ((a,\<tau>)#\<Gamma>2)" by simp |
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
187 |
moreover |
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
188 |
have "valid \<Gamma>2" by fact |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
189 |
then have "valid ((a,\<tau>)#\<Gamma>2)" using vc v2 by simp |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
190 |
ultimately have "((a,\<tau>)#\<Gamma>2) \<turnstile> t:\<sigma>" using ih by simp |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
191 |
with vc show "\<Gamma>2 \<turnstile> (Lam [a].t) : \<tau> \<rightarrow> \<sigma>" by auto |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
192 |
qed (auto) (* app and var case *) |
18105 | 193 |
|
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
194 |
text{* The original induction principle for the typing relation |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
195 |
is not strong enough - even this simple lemma fails *} |
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
196 |
lemma weakening_too_weak: |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
197 |
assumes a: "\<Gamma>1 \<turnstile> t:\<sigma>" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
198 |
and b: "valid \<Gamma>2" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
199 |
and c: "\<Gamma>1 \<lless> \<Gamma>2" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
200 |
shows "\<Gamma>2 \<turnstile> t:\<sigma>" |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
201 |
using a b c |
20503 | 202 |
proof (induct arbitrary: \<Gamma>2) |
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
203 |
case (t_Var \<Gamma>1 a \<tau>) (* variable case *) |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
204 |
have "\<Gamma>1 \<lless> \<Gamma>2" by fact |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
205 |
moreover |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
206 |
have "valid \<Gamma>2" by fact |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
207 |
moreover |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
208 |
have "(a,\<tau>) \<in> (set \<Gamma>1)" by fact |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
209 |
ultimately show "\<Gamma>2 \<turnstile> Var a : \<tau>" by auto |
18105 | 210 |
next |
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
211 |
case (t_Lam a \<Gamma>1 \<tau> t \<sigma>) (* lambda case *) |
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
212 |
(* all assumption in this case*) |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
213 |
have a0: "a\<sharp>\<Gamma>1" by fact |
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
214 |
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
|
215 |
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
|
216 |
have a3: "valid \<Gamma>2" by fact |
21052
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
217 |
have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; ((a,\<tau>)#\<Gamma>1) \<lless> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t:\<sigma>" by fact |
ec5531061ed6
adapted to Stefan's new inductive package and cleaning up
urbanc
parents:
20955
diff
changeset
|
218 |
have "((a,\<tau>)#\<Gamma>1) \<lless> ((a,\<tau>)#\<Gamma>2)" using a2 by simp |
18105 | 219 |
moreover |
18311
b83b00cbaecf
changed "fresh:" to "avoiding:" and cleaned up the weakening example
urbanc
parents:
18296
diff
changeset
|
220 |
have "valid ((a,\<tau>)#\<Gamma>2)" using v2 (* fails *) |
19496 | 221 |
oops |
18105 | 222 |
|
19496 | 223 |
end |