120 |
120 |
121 equivariance typing2 |
121 equivariance typing2 |
122 |
122 |
123 nominal_inductive typing2 |
123 nominal_inductive typing2 |
124 avoids t2_Lam: "x" |
124 avoids t2_Lam: "x" |
125 by (simp_all add: fresh_star_def fresh_ty) |
125 by (simp_all add: fresh_star_def fresh_ty lam.fresh) |
126 |
126 |
127 lemma weakening_version3: |
127 lemma weakening_version3: |
128 fixes \<Gamma>::"(name \<times> ty) fset" |
128 fixes \<Gamma>::"(name \<times> ty) fset" |
129 assumes a: "\<Gamma> 2\<turnstile> t : T" |
129 assumes a: "\<Gamma> 2\<turnstile> t : T" |
130 and b: "(x, T') |\<notin>| \<Gamma>" |
130 and b: "(x, T') |\<notin>| \<Gamma>" |
131 shows "{|(x, T')|} |\<union>| \<Gamma> 2\<turnstile> t : T" |
131 shows "{|(x, T')|} |\<union>| \<Gamma> 2\<turnstile> t : T" |
132 using a b |
132 using a b |
133 apply(nominal_induct \<Gamma> t T avoiding: x rule: typing2.strong_induct) |
133 apply(nominal_induct \<Gamma> t T avoiding: x rule: typing2.strong_induct) |
134 apply(auto)[2] |
134 apply(auto)[2] |
135 apply(rule t2_Lam) |
135 apply(rule t2_Lam) |
136 apply(simp add: fresh_insert_fset fresh_ty) |
136 apply(simp add: fresh_insert_fset fresh_Pair fresh_ty) |
137 apply(simp) |
137 apply(simp) |
138 apply(drule_tac x="xa" in meta_spec) |
138 apply(drule_tac x="xa" in meta_spec) |
139 apply(drule meta_mp) |
139 apply(drule meta_mp) |
140 apply(simp add: fresh_at_base) |
140 apply(simp add: fresh_at_base) |
141 apply(simp add: insert_fset_left_comm) |
141 apply(simp add: insert_fset_left_comm) |
142 done |
142 done |
143 |
143 |
144 lemma weakening_version4: |
|
145 fixes \<Gamma>::"(name \<times> ty) fset" |
|
146 assumes a: "\<Gamma> 2\<turnstile> t : T" |
|
147 and b: "(x, T') |\<notin>| \<Gamma>" |
|
148 shows "{|(x, T')|} |\<union>| \<Gamma> 2\<turnstile> t : T" |
|
149 using a b |
|
150 apply(induct \<Gamma> t T arbitrary: x T') |
|
151 apply(auto)[2] |
|
152 apply(blast) |
|
153 apply(simp) |
|
154 apply(rule_tac ?'a="name" and x="(x, xa, t, T', \<Gamma>)" in obtain_fresh) |
|
155 apply(rule_tac t= "Lam [x]. t" and s="Lam [a]. ((a \<leftrightarrow> x) \<bullet> t)" in subst) |
|
156 defer |
|
157 apply(rule t2_Lam) |
|
158 apply(simp add: fresh_insert_fset) |
|
159 oops |
|
160 |
|
161 |
|
162 |
144 |
163 end |
145 end |
164 |
146 |
165 |
147 |
166 |
148 |