135 thm valid.eqvt |
135 thm valid.eqvt |
136 thm typing.eqvt |
136 thm typing.eqvt |
137 thm eqvts |
137 thm eqvts |
138 thm eqvts_raw |
138 thm eqvts_raw |
139 |
139 |
|
140 thm typing.induct[of "\<Gamma>" "t" "T", no_vars] |
|
141 |
|
142 lemma |
|
143 fixes c::"'a::fs" |
|
144 assumes a: "\<Gamma> \<turnstile> t : T" |
|
145 and a1: "\<And>\<Gamma> x T c. \<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> P c \<Gamma> (Var x) T" |
|
146 and a2: "\<And>\<Gamma> t1 T1 T2 t2 c. \<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<And>d. P d \<Gamma> t1 T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1; \<And>d. P d \<Gamma> t2 T1\<rbrakk> |
|
147 \<Longrightarrow> P c \<Gamma> (App t1 t2) T2" |
|
148 and a3: "\<And>x \<Gamma> T1 t T2 c. \<lbrakk>atom x \<sharp> c; atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2; \<And>d. P d ((x, T1) # \<Gamma>) t T2\<rbrakk> |
|
149 \<Longrightarrow> P c \<Gamma> (Lam x t) T1 \<rightarrow> T2" |
|
150 shows "P c \<Gamma> t T" |
|
151 proof - |
|
152 from a have "\<And>p c. P c (p \<bullet> \<Gamma>) (p \<bullet> t) (p \<bullet> T)" |
|
153 proof (induct) |
|
154 case (t_Var \<Gamma> x T p c) |
|
155 then show ?case |
|
156 apply - |
|
157 apply(perm_strict_simp) |
|
158 apply(rule a1) |
|
159 apply(rule_tac p="-p" in permute_boolE) |
|
160 apply(perm_strict_simp add: permute_minus_cancel) |
|
161 apply(assumption) |
|
162 apply(rule_tac p="-p" in permute_boolE) |
|
163 apply(perm_strict_simp add: permute_minus_cancel) |
|
164 apply(assumption) |
|
165 done |
|
166 next |
|
167 case (t_App \<Gamma> t1 T1 T2 t2 p c) |
|
168 then show ?case |
|
169 apply - |
|
170 apply(perm_strict_simp) |
|
171 apply(rule_tac ?T1.0="p \<bullet> T1" in a2) |
|
172 apply(rule_tac p="-p" in permute_boolE) |
|
173 apply(perm_strict_simp add: permute_minus_cancel) |
|
174 apply(assumption) |
|
175 apply(assumption) |
|
176 apply(rule_tac p="-p" in permute_boolE) |
|
177 apply(perm_strict_simp add: permute_minus_cancel) |
|
178 apply(assumption) |
|
179 apply(assumption) |
|
180 done |
|
181 next |
|
182 case (t_Lam x \<Gamma> T1 t T2 p c) |
|
183 then show ?case |
|
184 apply - |
|
185 apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom x}) \<sharp>* c \<and> |
|
186 supp (p \<bullet> \<Gamma>, p \<bullet> Lam x t, p \<bullet> (T1 \<rightarrow> T2)) \<sharp>* q") |
|
187 apply(erule exE) |
|
188 apply(rule_tac t="p \<bullet> \<Gamma>" and s="q \<bullet> p \<bullet> \<Gamma>" in subst) |
|
189 apply(rule supp_perm_eq) |
|
190 apply(simp add: supp_Pair fresh_star_union) |
|
191 apply(rule_tac t="p \<bullet> Lam x t" and s="q \<bullet> p \<bullet> Lam x t" in subst) |
|
192 apply(rule supp_perm_eq) |
|
193 apply(simp add: supp_Pair fresh_star_union) |
|
194 apply(rule_tac t="p \<bullet> (T1 \<rightarrow> T2)" and s="q \<bullet> p \<bullet> (T1 \<rightarrow> T2)" in subst) |
|
195 apply(rule supp_perm_eq) |
|
196 apply(simp add: supp_Pair fresh_star_union) |
|
197 apply(simp add: eqvts) |
|
198 apply(rule a3) |
|
199 apply(simp add: fresh_star_def) |
|
200 apply(rule_tac p="-q" in permute_boolE) |
|
201 apply(perm_strict_simp add: permute_minus_cancel) |
|
202 apply(rule_tac p="-p" in permute_boolE) |
|
203 apply(perm_strict_simp add: permute_minus_cancel) |
|
204 apply(assumption) |
|
205 apply(rule_tac p="-q" in permute_boolE) |
|
206 apply(perm_strict_simp add: permute_minus_cancel) |
|
207 apply(rule_tac p="-p" in permute_boolE) |
|
208 apply(perm_strict_simp add: permute_minus_cancel) |
|
209 apply(assumption) |
|
210 apply(drule_tac x="d" in meta_spec) |
|
211 apply(drule_tac x="q + p" in meta_spec) |
|
212 apply(simp) |
|
213 apply(rule at_set_avoiding2) |
|
214 apply(simp add: finite_supp) |
|
215 apply(simp add: finite_supp) |
|
216 apply(simp add: finite_supp) |
|
217 apply(rule_tac p="-p" in permute_boolE) |
|
218 apply(perm_strict_simp add: permute_minus_cancel) |
|
219 (* supplied by the user *) |
|
220 apply(simp add: fresh_star_prod) |
|
221 apply(simp add: fresh_star_def) |
|
222 |
|
223 |
|
224 done |
|
225 (* HERE *) |
|
226 |
|
227 |
|
228 |
|
229 |
|
230 |
|
231 |
140 |
232 |
141 inductive |
233 inductive |
142 tt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" |
234 tt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" |
143 for r :: "('a \<Rightarrow> 'a \<Rightarrow> bool)" |
235 for r :: "('a \<Rightarrow> 'a \<Rightarrow> bool)" |
144 where |
236 where |