equal
deleted
inserted
replaced
125 assumes ty: "\<Gamma> \<turnstile> Lam [x].t : T" |
125 assumes ty: "\<Gamma> \<turnstile> Lam [x].t : T" |
126 and fc: "atom x \<sharp> \<Gamma>" |
126 and fc: "atom x \<sharp> \<Gamma>" |
127 obtains T1 T2 where "T = T1 \<rightarrow> T2" "(x, T1) # \<Gamma> \<turnstile> t : T2" |
127 obtains T1 T2 where "T = T1 \<rightarrow> T2" "(x, T1) # \<Gamma> \<turnstile> t : T2" |
128 using ty fc |
128 using ty fc |
129 apply(cases) |
129 apply(cases) |
|
130 using [[simproc del: alpha_lst]] |
130 apply(auto simp add: lam.eq_iff lam.distinct ty.eq_iff) |
131 apply(auto simp add: lam.eq_iff lam.distinct ty.eq_iff) |
131 apply(auto simp add: Abs1_eq_iff) |
132 apply(auto simp add: Abs1_eq_iff) |
132 apply(rotate_tac 3) |
133 apply(rotate_tac 3) |
133 apply(drule_tac p="(x \<leftrightarrow> xa)" in permute_boolI) |
134 apply(drule_tac p="(x \<leftrightarrow> xa)" in permute_boolI) |
134 apply(perm_simp) |
135 apply(perm_simp) |
135 apply(auto simp add: flip_def swap_fresh_fresh ty_fresh) |
136 apply(auto simp add: flip_fresh_fresh ty_fresh) |
136 done |
137 done |
137 |
138 |
138 |
139 |
139 section {* EXERCISE 17 *} |
140 section {* EXERCISE 17 *} |
140 |
141 |