99 next |
99 next |
100 case (t_Lam a \<Gamma> \<tau> t \<sigma>) |
100 case (t_Lam a \<Gamma> \<tau> t \<sigma>) |
101 have k1: "a\<sharp>\<Gamma>" by fact |
101 have k1: "a\<sharp>\<Gamma>" by fact |
102 have k2: "((a,\<tau>)#\<Gamma>)\<turnstile>t:\<sigma>" by fact |
102 have k2: "((a,\<tau>)#\<Gamma>)\<turnstile>t:\<sigma>" by fact |
103 have k3: "\<And>(pi::name prm) (x::'a::fs_name). P x (pi \<bullet>((a,\<tau>)#\<Gamma>)) (pi\<bullet>t) \<sigma>" by fact |
103 have k3: "\<And>(pi::name prm) (x::'a::fs_name). P x (pi \<bullet>((a,\<tau>)#\<Gamma>)) (pi\<bullet>t) \<sigma>" by fact |
104 have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t,pi\<bullet>\<Gamma>,x)" |
104 obtain c::"name" where "c\<sharp>(pi\<bullet>a,pi\<bullet>t,pi\<bullet>\<Gamma>,x)" by (erule exists_fresh[OF fs_name1]) |
105 by (rule exists_fresh', simp add: fs_name1) |
105 then have f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>t)" and f4: "c\<sharp>(pi\<bullet>\<Gamma>)" |
106 then obtain c::"name" |
106 by (simp_all add: fresh_atm[symmetric]) |
107 where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>t)" and f4: "c\<sharp>(pi\<bullet>\<Gamma>)" |
|
108 by (force simp add: fresh_prod fresh_atm) |
|
109 from k1 have k1a: "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_bij) |
107 from k1 have k1a: "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_bij) |
110 have l1: "(([(c,pi\<bullet>a)]@pi)\<bullet>\<Gamma>) = (pi\<bullet>\<Gamma>)" using f4 k1a |
108 have l1: "(([(c,pi\<bullet>a)]@pi)\<bullet>\<Gamma>) = (pi\<bullet>\<Gamma>)" using f4 k1a |
111 by (simp only: pt_name2, rule perm_fresh_fresh) |
109 by (simp only: pt_name2, rule perm_fresh_fresh) |
112 have "\<And>x. P x (([(c,pi\<bullet>a)]@pi)\<bullet>((a,\<tau>)#\<Gamma>)) (([(c,pi\<bullet>a)]@pi)\<bullet>t) \<sigma>" using k3 by force |
110 have "\<And>x. P x (([(c,pi\<bullet>a)]@pi)\<bullet>((a,\<tau>)#\<Gamma>)) (([(c,pi\<bullet>a)]@pi)\<bullet>t) \<sigma>" using k3 by force |
113 hence l2: "\<And>x. P x ((c, \<tau>)#(pi\<bullet>\<Gamma>)) (([(c,pi\<bullet>a)]@pi)\<bullet>t) \<sigma>" using f1 l1 |
111 hence l2: "\<And>x. P x ((c, \<tau>)#(pi\<bullet>\<Gamma>)) (([(c,pi\<bullet>a)]@pi)\<bullet>t) \<sigma>" using f1 l1 |
156 case (t_Lam a \<Gamma> \<tau> t \<sigma> pi x) |
154 case (t_Lam a \<Gamma> \<tau> t \<sigma> pi x) |
157 have p1: "((a,\<tau>)#\<Gamma>)\<turnstile>t:\<sigma>" by fact |
155 have p1: "((a,\<tau>)#\<Gamma>)\<turnstile>t:\<sigma>" by fact |
158 have ih1: "\<And>(pi::name prm) x. P x (pi\<bullet>((a,\<tau>)#\<Gamma>)) (pi\<bullet>t) \<sigma>" by fact |
156 have ih1: "\<And>(pi::name prm) x. P x (pi\<bullet>((a,\<tau>)#\<Gamma>)) (pi\<bullet>t) \<sigma>" by fact |
159 have f: "a\<sharp>\<Gamma>" by fact |
157 have f: "a\<sharp>\<Gamma>" by fact |
160 then have f': "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_bij) |
158 then have f': "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_bij) |
161 have "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t,pi\<bullet>\<Gamma>,x)" |
159 obtain c::"name" where "c\<sharp>(pi\<bullet>a,pi\<bullet>t,pi\<bullet>\<Gamma>,x)" by (erule exists_fresh[OF fs_name1]) |
162 by (rule exists_fresh', simp add: fs_name1) |
160 then have fs: "c\<noteq>(pi\<bullet>a)" "c\<sharp>x" "c\<sharp>(pi\<bullet>t)" "c\<sharp>(pi\<bullet>\<Gamma>)" |
163 then obtain c::"name" |
161 by (simp_all add: fresh_atm[symmetric]) |
164 where fs: "c\<noteq>(pi\<bullet>a)" "c\<sharp>x" "c\<sharp>(pi\<bullet>t)" "c\<sharp>(pi\<bullet>\<Gamma>)" |
|
165 by (force simp add: fresh_prod fresh_atm) |
|
166 let ?pi'="[(pi\<bullet>a,c)]@pi" |
162 let ?pi'="[(pi\<bullet>a,c)]@pi" |
167 have eq: "((pi\<bullet>a,c)#pi)\<bullet>a = c" by (simp add: calc_atm) |
163 have eq: "((pi\<bullet>a,c)#pi)\<bullet>a = c" by (simp add: calc_atm) |
168 have p1': "(?pi'\<bullet>((a,\<tau>)#\<Gamma>))\<turnstile>(?pi'\<bullet>t):\<sigma>" using p1 by (simp only: eqvt_typing) |
164 have p1': "(?pi'\<bullet>((a,\<tau>)#\<Gamma>))\<turnstile>(?pi'\<bullet>t):\<sigma>" using p1 by (simp only: eqvt_typing) |
169 have ih1': "\<And>x. P x (?pi'\<bullet>((a,\<tau>)#\<Gamma>)) (?pi'\<bullet>t) \<sigma>" using ih1 by simp |
165 have ih1': "\<And>x. P x (?pi'\<bullet>((a,\<tau>)#\<Gamma>)) (?pi'\<bullet>t) \<sigma>" using ih1 by simp |
170 have "P x (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>(Lam [a].t)) (\<tau>\<rightarrow>\<sigma>)" using f f' fs p1' ih1' eq |
166 have "P x (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>(Lam [a].t)) (\<tau>\<rightarrow>\<sigma>)" using f f' fs p1' ih1' eq |