35 lemma eqvt_valid[eqvt]: |
35 lemma eqvt_valid[eqvt]: |
36 fixes pi:: "name prm" |
36 fixes pi:: "name prm" |
37 assumes a: "valid \<Gamma>" |
37 assumes a: "valid \<Gamma>" |
38 shows "valid (pi\<bullet>\<Gamma>)" |
38 shows "valid (pi\<bullet>\<Gamma>)" |
39 using a |
39 using a |
40 by (induct) |
40 by (induct) (auto simp add: fresh_bij) |
41 (auto simp add: fresh_bij) |
|
42 |
|
43 thm eqvt |
|
44 |
41 |
45 text{* typing judgements *} |
42 text{* typing judgements *} |
46 inductive2 |
43 inductive2 |
47 typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80) |
44 typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80) |
48 where |
45 where |
49 t_Var[intro]: "\<lbrakk>valid \<Gamma>; (a,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var a : \<tau>" |
46 t_Var[intro]: "\<lbrakk>valid \<Gamma>; (a,T)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var a : T" |
50 | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>" |
47 | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1\<rightarrow>T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2" |
51 | t_Lam[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>" |
48 | t_Lam[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,T1)#\<Gamma>) \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : T1\<rightarrow>T2" |
52 |
49 |
53 lemma eqvt_typing[eqvt]: |
50 lemma eqvt_typing[eqvt]: |
54 fixes pi:: "name prm" |
51 fixes pi:: "name prm" |
55 assumes a: "\<Gamma> \<turnstile> t : \<tau>" |
52 assumes a: "\<Gamma> \<turnstile> t : T" |
56 shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>t) : (pi\<bullet>\<tau>)" |
53 shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>t) : (pi\<bullet>T)" |
57 using a |
54 using a |
58 proof (induct) |
55 proof (induct) |
59 case (t_Var \<Gamma> a \<tau>) |
56 case (t_Var \<Gamma> a T) |
60 have "valid (pi\<bullet>\<Gamma>)" by (rule eqvt_valid) |
57 have "valid (pi\<bullet>\<Gamma>)" by (rule eqvt_valid) |
61 moreover |
58 moreover |
62 have "(pi\<bullet>(a,\<tau>))\<in>(pi\<bullet>set \<Gamma>)" by (rule pt_set_bij2[OF pt_name_inst, OF at_name_inst]) |
59 have "(pi\<bullet>(a,T))\<in>(pi\<bullet>set \<Gamma>)" by (rule pt_set_bij2[OF pt_name_inst, OF at_name_inst]) |
63 ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Var a) : (pi\<bullet>\<tau>)" |
60 ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Var a) : (pi\<bullet>T)" |
64 using typing.intros by (force simp add: pt_list_set_pi[OF pt_name_inst, symmetric]) |
61 using typing.intros by (force simp add: set_eqvt) |
65 next |
62 next |
66 case (t_Lam a \<Gamma> \<tau> t \<sigma>) |
63 case (t_Lam a \<Gamma> T1 t T2) |
67 moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_bij) |
64 moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_bij) |
68 ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) :(pi\<bullet>\<tau>\<rightarrow>\<sigma>)" by force |
65 ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) :(pi\<bullet>T1\<rightarrow>T2)" by force |
69 qed (auto) |
66 qed (auto) |
70 |
67 |
71 text {* the strong induction principle needs to be derived manually *} |
68 text {* the strong induction principle needs to be derived manually *} |
72 |
69 |
73 lemma typing_induct[consumes 1, case_names t_Var t_App t_Lam]: |
70 lemma typing_induct[consumes 1, case_names t_Var t_App t_Lam]: |
74 fixes P :: "'a::fs_name\<Rightarrow>(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow>bool" |
71 fixes P :: "'a::fs_name\<Rightarrow>(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow>bool" |
75 and \<Gamma> :: "(name\<times>ty) list" |
72 and \<Gamma> :: "(name\<times>ty) list" |
76 and t :: "lam" |
73 and t :: "lam" |
77 and \<tau> :: "ty" |
74 and T :: "ty" |
78 and x :: "'a::fs_name" |
75 and x :: "'a::fs_name" |
79 assumes a: "\<Gamma> \<turnstile> t : \<tau>" |
76 assumes a: "\<Gamma> \<turnstile> t : T" |
80 and a1: "\<And>\<Gamma> a \<tau> x. \<lbrakk>valid \<Gamma>; (a,\<tau>) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> P x \<Gamma> (Var a) \<tau>" |
77 and a1: "\<And>\<Gamma> a T x. \<lbrakk>valid \<Gamma>; (a,T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> P x \<Gamma> (Var a) T" |
81 and a2: "\<And>\<Gamma> \<tau> \<sigma> t1 t2 x. \<lbrakk>\<And>z. P z \<Gamma> t1 (\<tau>\<rightarrow>\<sigma>); \<And>z. P z \<Gamma> t2 \<tau>\<rbrakk> |
78 and a2: "\<And>\<Gamma> T1 T2 t1 t2 x. \<lbrakk>\<And>z. P z \<Gamma> t1 (T1\<rightarrow>T2); \<And>z. P z \<Gamma> t2 T1\<rbrakk> |
82 \<Longrightarrow> P x \<Gamma> (App t1 t2) \<sigma>" |
79 \<Longrightarrow> P x \<Gamma> (App t1 t2) T2" |
83 and a3: "\<And>a \<Gamma> \<tau> \<sigma> t x. \<lbrakk>a\<sharp>x; a\<sharp>\<Gamma>; \<And>z. P z ((a,\<tau>)#\<Gamma>) t \<sigma>\<rbrakk> |
80 and a3: "\<And>a \<Gamma> T1 T2 t x. \<lbrakk>a\<sharp>x; a\<sharp>\<Gamma>; \<And>z. P z ((a,T1)#\<Gamma>) t T2\<rbrakk> |
84 \<Longrightarrow> P x \<Gamma> (Lam [a].t) (\<tau>\<rightarrow>\<sigma>)" |
81 \<Longrightarrow> P x \<Gamma> (Lam [a].t) (T1\<rightarrow>T2)" |
85 shows "P x \<Gamma> t \<tau>" |
82 shows "P x \<Gamma> t T" |
86 proof - |
83 proof - |
87 from a have "\<And>(pi::name prm) x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>t) (pi\<bullet>\<tau>)" |
84 from a have "\<And>(pi::name prm) x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>t) (pi\<bullet>T)" |
88 proof (induct) |
85 proof (induct) |
89 case (t_Var \<Gamma> a \<tau>) |
86 case (t_Var \<Gamma> a T) |
90 have "valid \<Gamma>" by fact |
87 have "valid \<Gamma>" by fact |
91 then have "valid (pi\<bullet>\<Gamma>)" by (rule eqvt) |
88 then have "valid (pi\<bullet>\<Gamma>)" by (rule eqvt) |
92 moreover |
89 moreover |
93 have "(a,\<tau>)\<in>set \<Gamma>" by fact |
90 have "(a,T)\<in>set \<Gamma>" by fact |
94 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]) |
91 then have "pi\<bullet>(a,T)\<in>pi\<bullet>(set \<Gamma>)" by (simp only: pt_set_bij[OF pt_name_inst, OF at_name_inst]) |
95 then have "(pi\<bullet>a,\<tau>)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: pt_list_set_pi[OF pt_name_inst]) |
92 then have "(pi\<bullet>a,T)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: set_eqvt) |
96 ultimately show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Var a)) (pi\<bullet>\<tau>)" using a1 by simp |
93 ultimately show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Var a)) (pi\<bullet>T)" using a1 by simp |
97 next |
94 next |
98 case (t_App \<Gamma> t1 \<tau> \<sigma> t2) |
95 case (t_App \<Gamma> t1 T1 T2 t2) |
99 thus "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(App t1 t2)) (pi\<bullet>\<sigma>)" using a2 |
96 thus "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(App t1 t2)) (pi\<bullet>T2)" using a2 |
100 by (simp only: eqvt) (blast) |
97 by (simp only: eqvt) (blast) |
101 next |
98 next |
102 case (t_Lam a \<Gamma> \<tau> t \<sigma>) |
99 case (t_Lam a \<Gamma> T1 t T2) |
103 obtain c::"name" where fs: "c\<sharp>(pi\<bullet>a,pi\<bullet>t,pi\<bullet>\<Gamma>,x)" by (rule exists_fresh[OF fs_name1]) |
100 obtain c::"name" where fs: "c\<sharp>(pi\<bullet>a,pi\<bullet>t,pi\<bullet>\<Gamma>,x)" by (rule exists_fresh[OF fs_name1]) |
104 let ?sw="[(pi\<bullet>a,c)]" |
101 let ?sw="[(pi\<bullet>a,c)]" |
105 let ?pi'="?sw@pi" |
102 let ?pi'="?sw@pi" |
106 have f1: "a\<sharp>\<Gamma>" by fact |
103 have f1: "a\<sharp>\<Gamma>" by fact |
107 have f2: "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" using f1 by (simp add: fresh_bij) |
104 have f2: "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" using f1 by (simp add: fresh_bij) |
108 have f3: "c\<sharp>?pi'\<bullet>\<Gamma>" using f1 by (auto simp add: pt_name2 fresh_left calc_atm perm_pi_simp) |
105 have f3: "c\<sharp>?pi'\<bullet>\<Gamma>" using f1 by (auto simp add: pt_name2 fresh_left calc_atm perm_pi_simp) |
109 have ih1: "\<And>x. P x (?pi'\<bullet>((a,\<tau>)#\<Gamma>)) (?pi'\<bullet>t) (?pi'\<bullet>\<sigma>)" by fact |
106 have ih1: "\<And>x. P x (?pi'\<bullet>((a,T1)#\<Gamma>)) (?pi'\<bullet>t) (?pi'\<bullet>T2)" by fact |
110 then have "\<And>x. P x ((c,\<tau>)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>t) (?pi'\<bullet>\<sigma>)" by (simp add: calc_atm) |
107 then have "\<And>x. P x ((c,T1)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>t) (?pi'\<bullet>T2)" by (simp add: calc_atm) |
111 then have "P x (?pi'\<bullet>\<Gamma>) (Lam [c].(?pi'\<bullet>t)) (\<tau>\<rightarrow>\<sigma>)" using a3 f3 fs by simp |
108 then have "P x (?pi'\<bullet>\<Gamma>) (Lam [c].(?pi'\<bullet>t)) (T1\<rightarrow>T2)" using a3 f3 fs by simp |
112 then have "P x (?sw\<bullet>pi\<bullet>\<Gamma>) (?sw\<bullet>(Lam [(pi\<bullet>a)].(pi\<bullet>t))) (\<tau>\<rightarrow>\<sigma>)" |
109 then have "P x (?sw\<bullet>pi\<bullet>\<Gamma>) (?sw\<bullet>(Lam [(pi\<bullet>a)].(pi\<bullet>t))) (T1\<rightarrow>T2)" |
113 by (simp del: append_Cons add: calc_atm pt_name2) |
110 by (simp del: append_Cons add: calc_atm pt_name2) |
114 moreover have "(?sw\<bullet>(pi\<bullet>\<Gamma>)) = (pi\<bullet>\<Gamma>)" |
111 moreover have "(?sw\<bullet>(pi\<bullet>\<Gamma>)) = (pi\<bullet>\<Gamma>)" |
115 by (rule perm_fresh_fresh) (simp_all add: fs f2) |
112 by (rule perm_fresh_fresh) (simp_all add: fs f2) |
116 moreover have "(?sw\<bullet>(Lam [(pi\<bullet>a)].(pi\<bullet>t))) = Lam [(pi\<bullet>a)].(pi\<bullet>t)" |
113 moreover have "(?sw\<bullet>(Lam [(pi\<bullet>a)].(pi\<bullet>t))) = Lam [(pi\<bullet>a)].(pi\<bullet>t)" |
117 by (rule perm_fresh_fresh) (simp_all add: fs f2 abs_fresh) |
114 by (rule perm_fresh_fresh) (simp_all add: fs f2 abs_fresh) |
118 ultimately show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Lam [a].t)) (pi\<bullet>\<tau>\<rightarrow>\<sigma>)" by (simp) |
115 ultimately show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Lam [a].t)) (pi\<bullet>T1\<rightarrow>T2)" by (simp) |
119 qed |
116 qed |
120 hence "P x (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>t) (([]::name prm)\<bullet>\<tau>)" by blast |
117 hence "P x (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>t) (([]::name prm)\<bullet>T)" by blast |
121 thus "P x \<Gamma> t \<tau>" by simp |
118 thus "P x \<Gamma> t T" by simp |
122 qed |
119 qed |
123 |
120 |
124 text {* definition of a subcontext *} |
121 text {* definition of a subcontext *} |
125 |
122 |
126 abbreviation |
123 abbreviation |
128 "\<Gamma>1 \<lless> \<Gamma>2 \<equiv> \<forall>a \<sigma>. (a,\<sigma>)\<in>set \<Gamma>1 \<longrightarrow> (a,\<sigma>)\<in>set \<Gamma>2" |
125 "\<Gamma>1 \<lless> \<Gamma>2 \<equiv> \<forall>a \<sigma>. (a,\<sigma>)\<in>set \<Gamma>1 \<longrightarrow> (a,\<sigma>)\<in>set \<Gamma>2" |
129 |
126 |
130 text {* now it comes: The Weakening Lemma *} |
127 text {* now it comes: The Weakening Lemma *} |
131 |
128 |
132 lemma weakening_version1: |
129 lemma weakening_version1: |
133 assumes a: "\<Gamma>1 \<turnstile> t : \<sigma>" |
130 assumes a: "\<Gamma>1 \<turnstile> t : T" |
134 and b: "valid \<Gamma>2" |
131 and b: "valid \<Gamma>2" |
135 and c: "\<Gamma>1 \<lless> \<Gamma>2" |
132 and c: "\<Gamma>1 \<lless> \<Gamma>2" |
136 shows "\<Gamma>2 \<turnstile> t:\<sigma>" |
133 shows "\<Gamma>2 \<turnstile> t : T" |
137 using a b c |
134 using a b c |
138 apply(nominal_induct \<Gamma>1 t \<sigma> avoiding: \<Gamma>2 rule: typing_induct) |
135 by (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing_induct) |
139 apply(auto | atomize)+ |
136 (auto | atomize)+ |
140 (* FIXME: meta-quantifiers seem to be not as "automatic" as object-quantifiers *) |
137 (* FIXME: meta-quantifiers seem to be not as "automatic" as object-quantifiers *) |
141 done |
|
142 |
138 |
143 lemma weakening_version2: |
139 lemma weakening_version2: |
144 fixes \<Gamma>1::"(name\<times>ty) list" |
140 fixes \<Gamma>1::"(name\<times>ty) list" |
145 and t ::"lam" |
141 and t ::"lam" |
146 and \<tau> ::"ty" |
142 and \<tau> ::"ty" |
147 assumes a: "\<Gamma>1 \<turnstile> t:\<sigma>" |
143 assumes a: "\<Gamma>1 \<turnstile> t:T" |
148 and b: "valid \<Gamma>2" |
144 and b: "valid \<Gamma>2" |
149 and c: "\<Gamma>1 \<lless> \<Gamma>2" |
145 and c: "\<Gamma>1 \<lless> \<Gamma>2" |
150 shows "\<Gamma>2 \<turnstile> t:\<sigma>" |
146 shows "\<Gamma>2 \<turnstile> t:T" |
151 using a b c |
147 using a b c |
152 proof (nominal_induct \<Gamma>1 t \<sigma> avoiding: \<Gamma>2 rule: typing_induct) |
148 proof (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing_induct) |
153 case (t_Var \<Gamma>1 a \<tau>) (* variable case *) |
149 case (t_Var \<Gamma>1 a T) (* variable case *) |
154 have "\<Gamma>1 \<lless> \<Gamma>2" by fact |
150 have "\<Gamma>1 \<lless> \<Gamma>2" by fact |
155 moreover |
151 moreover |
156 have "valid \<Gamma>2" by fact |
152 have "valid \<Gamma>2" by fact |
157 moreover |
153 moreover |
158 have "(a,\<tau>)\<in> set \<Gamma>1" by fact |
154 have "(a,T)\<in> set \<Gamma>1" by fact |
159 ultimately show "\<Gamma>2 \<turnstile> Var a : \<tau>" by auto |
155 ultimately show "\<Gamma>2 \<turnstile> Var a : T" by auto |
160 next |
156 next |
161 case (t_Lam a \<Gamma>1 \<tau> \<sigma> t) (* lambda case *) |
157 case (t_Lam a \<Gamma>1 T1 T2 t) (* lambda case *) |
162 have vc: "a\<sharp>\<Gamma>2" by fact (* variable convention *) |
158 have vc: "a\<sharp>\<Gamma>2" by fact (* variable convention *) |
163 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 |
159 have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; ((a,T1)#\<Gamma>1) \<lless> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t:T2" by fact |
164 have "\<Gamma>1 \<lless> \<Gamma>2" by fact |
160 have "\<Gamma>1 \<lless> \<Gamma>2" by fact |
165 then have "((a,\<tau>)#\<Gamma>1) \<lless> ((a,\<tau>)#\<Gamma>2)" by simp |
161 then have "((a,T1)#\<Gamma>1) \<lless> ((a,T1)#\<Gamma>2)" by simp |
166 moreover |
162 moreover |
167 have "valid \<Gamma>2" by fact |
163 have "valid \<Gamma>2" by fact |
168 then have "valid ((a,\<tau>)#\<Gamma>2)" using vc by (simp add: v2) |
164 then have "valid ((a,T1)#\<Gamma>2)" using vc by (simp add: v2) |
169 ultimately have "((a,\<tau>)#\<Gamma>2) \<turnstile> t:\<sigma>" using ih by simp |
165 ultimately have "((a,T1)#\<Gamma>2) \<turnstile> t:T2" using ih by simp |
170 with vc show "\<Gamma>2 \<turnstile> (Lam [a].t) : \<tau> \<rightarrow> \<sigma>" by auto |
166 with vc show "\<Gamma>2 \<turnstile> (Lam [a].t) : T1\<rightarrow>T2" by auto |
171 qed (auto) (* app case *) |
167 qed (auto) (* app case *) |
172 |
168 |
173 lemma weakening_version3: |
169 lemma weakening_version3: |
174 assumes a: "\<Gamma>1 \<turnstile> t:\<sigma>" |
170 assumes a: "\<Gamma>1 \<turnstile> t : T" |
175 and b: "valid \<Gamma>2" |
171 and b: "valid \<Gamma>2" |
176 and c: "\<Gamma>1 \<lless> \<Gamma>2" |
172 and c: "\<Gamma>1 \<lless> \<Gamma>2" |
177 shows "\<Gamma>2 \<turnstile> t:\<sigma>" |
173 shows "\<Gamma>2 \<turnstile> t : T" |
178 using a b c |
174 using a b c |
179 proof (nominal_induct \<Gamma>1 t \<sigma> avoiding: \<Gamma>2 rule: typing_induct) |
175 proof (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing_induct) |
180 case (t_Lam a \<Gamma>1 \<tau> \<sigma> t) (* lambda case *) |
176 case (t_Lam a \<Gamma>1 T1 T2 t) (* lambda case *) |
181 have vc: "a\<sharp>\<Gamma>2" by fact (* variable convention *) |
177 have vc: "a\<sharp>\<Gamma>2" by fact (* variable convention *) |
182 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 |
178 have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; ((a,T1)#\<Gamma>1) \<lless> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t : T2" by fact |
183 have "\<Gamma>1 \<lless> \<Gamma>2" by fact |
179 have "\<Gamma>1 \<lless> \<Gamma>2" by fact |
184 then have "((a,\<tau>)#\<Gamma>1) \<lless> ((a,\<tau>)#\<Gamma>2)" by simp |
180 then have "((a,T1)#\<Gamma>1) \<lless> ((a,T1)#\<Gamma>2)" by simp |
185 moreover |
181 moreover |
186 have "valid \<Gamma>2" by fact |
182 have "valid \<Gamma>2" by fact |
187 then have "valid ((a,\<tau>)#\<Gamma>2)" using vc by (simp add: v2) |
183 then have "valid ((a,T1)#\<Gamma>2)" using vc by (simp add: v2) |
188 ultimately have "((a,\<tau>)#\<Gamma>2) \<turnstile> t:\<sigma>" using ih by simp |
184 ultimately have "((a,T1)#\<Gamma>2) \<turnstile> t : T2" using ih by simp |
189 with vc show "\<Gamma>2 \<turnstile> (Lam [a].t) : \<tau> \<rightarrow> \<sigma>" by auto |
185 with vc show "\<Gamma>2 \<turnstile> (Lam [a].t) : T1 \<rightarrow> T2" by auto |
190 qed (auto) (* app and var case *) |
186 qed (auto) (* app and var case *) |
191 |
187 |
192 text{* The original induction principle for the typing relation |
188 text{* The original induction principle for the typing relation |
193 is not strong enough - even this simple lemma fails: *} |
189 is not strong enough - even this simple lemma fails: *} |
194 lemma weakening_too_weak: |
190 lemma weakening_too_weak: |
195 assumes a: "\<Gamma>1 \<turnstile> t:\<sigma>" |
191 assumes a: "\<Gamma>1 \<turnstile> t : T" |
196 and b: "valid \<Gamma>2" |
192 and b: "valid \<Gamma>2" |
197 and c: "\<Gamma>1 \<lless> \<Gamma>2" |
193 and c: "\<Gamma>1 \<lless> \<Gamma>2" |
198 shows "\<Gamma>2 \<turnstile> t:\<sigma>" |
194 shows "\<Gamma>2 \<turnstile> t : T" |
199 using a b c |
195 using a b c |
200 proof (induct arbitrary: \<Gamma>2) |
196 proof (induct arbitrary: \<Gamma>2) |
201 case (t_Var \<Gamma>1 a \<tau>) (* variable case *) |
197 case (t_Var \<Gamma>1 a T) (* variable case *) |
202 have "\<Gamma>1 \<lless> \<Gamma>2" by fact |
198 have "\<Gamma>1 \<lless> \<Gamma>2" by fact |
203 moreover |
199 moreover |
204 have "valid \<Gamma>2" by fact |
200 have "valid \<Gamma>2" by fact |
205 moreover |
201 moreover |
206 have "(a,\<tau>) \<in> (set \<Gamma>1)" by fact |
202 have "(a,T) \<in> (set \<Gamma>1)" by fact |
207 ultimately show "\<Gamma>2 \<turnstile> Var a : \<tau>" by auto |
203 ultimately show "\<Gamma>2 \<turnstile> Var a : T" by auto |
208 next |
204 next |
209 case (t_Lam a \<Gamma>1 \<tau> t \<sigma>) (* lambda case *) |
205 case (t_Lam a \<Gamma>1 T1 t T2) (* lambda case *) |
210 (* all assumptions available in this case*) |
206 (* all assumptions available in this case*) |
211 have a0: "a\<sharp>\<Gamma>1" by fact |
207 have a0: "a\<sharp>\<Gamma>1" by fact |
212 have a1: "((a,\<tau>)#\<Gamma>1) \<turnstile> t : \<sigma>" by fact |
208 have a1: "((a,T1)#\<Gamma>1) \<turnstile> t : T2" by fact |
213 have a2: "\<Gamma>1 \<lless> \<Gamma>2" by fact |
209 have a2: "\<Gamma>1 \<lless> \<Gamma>2" by fact |
214 have a3: "valid \<Gamma>2" by fact |
210 have a3: "valid \<Gamma>2" by fact |
215 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 |
211 have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; ((a,T1)#\<Gamma>1) \<lless> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t : T2" by fact |
216 have "((a,\<tau>)#\<Gamma>1) \<lless> ((a,\<tau>)#\<Gamma>2)" using a2 by simp |
212 have "((a,T1)#\<Gamma>1) \<lless> ((a,T1)#\<Gamma>2)" using a2 by simp |
217 moreover |
213 moreover |
218 have "valid ((a,\<tau>)#\<Gamma>2)" using v2 (* fails *) |
214 have "valid ((a,T1)#\<Gamma>2)" using v2 (* fails *) |
219 oops |
215 oops |
220 |
216 |
221 end |
217 end |