src/HOL/Nominal/Examples/SN.thy
changeset 18106 836135c8acb2
child 18263 7f75925498da
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Nominal/Examples/SN.thy	Mon Nov 07 15:19:03 2005 +0100
     1.3 @@ -0,0 +1,902 @@
     1.4 +
     1.5 +theory sn
     1.6 +imports lam_substs  Accessible_Part
     1.7 +begin
     1.8 +
     1.9 +(* Strong normalisation according to the P&T book by Girard et al *)
    1.10 +
    1.11 +section {* Beta Reduction *}
    1.12 +
    1.13 +lemma subst_rename[rule_format]: 
    1.14 +  fixes  c  :: "name"
    1.15 +  and    a  :: "name"
    1.16 +  and    t1 :: "lam"
    1.17 +  and    t2 :: "lam"
    1.18 +  shows "c\<sharp>t1 \<longrightarrow> (t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2])"
    1.19 +apply(nominal_induct t1 rule: lam_induct)
    1.20 +apply(auto simp add: calc_atm fresh_atm fresh_prod abs_fresh)
    1.21 +done
    1.22 +
    1.23 +lemma forget[rule_format]: 
    1.24 +  shows "a\<sharp>t1 \<longrightarrow> t1[a::=t2] = t1"
    1.25 +apply (nominal_induct t1 rule: lam_induct)
    1.26 +apply(auto simp add: abs_fresh fresh_atm fresh_prod)
    1.27 +done
    1.28 +
    1.29 +lemma fresh_fact[rule_format]: 
    1.30 +  fixes   b :: "name"
    1.31 +  and    a  :: "name"
    1.32 +  and    t1 :: "lam"
    1.33 +  and    t2 :: "lam" 
    1.34 +  shows "a\<sharp>t1\<longrightarrow>a\<sharp>t2\<longrightarrow>a\<sharp>(t1[b::=t2])"
    1.35 +apply(nominal_induct t1 rule: lam_induct)
    1.36 +apply(auto simp add: abs_fresh fresh_prod fresh_atm)
    1.37 +done
    1.38 +
    1.39 +lemma subs_lemma:  
    1.40 +  fixes x::"name"
    1.41 +  and   y::"name"
    1.42 +  and   L::"lam"
    1.43 +  and   M::"lam"
    1.44 +  and   N::"lam"
    1.45 +  shows "x\<noteq>y\<longrightarrow>x\<sharp>L\<longrightarrow>M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
    1.46 +apply(nominal_induct M rule: lam_induct)
    1.47 +apply(auto simp add: fresh_fact forget fresh_prod fresh_atm)
    1.48 +done
    1.49 +
    1.50 +lemma id_subs: "t[x::=Var x] = t"
    1.51 +apply(nominal_induct t rule: lam_induct)
    1.52 +apply(simp_all add: fresh_atm)
    1.53 +done
    1.54 +
    1.55 +consts
    1.56 +  Beta :: "(lam\<times>lam) set"
    1.57 +syntax 
    1.58 +  "_Beta"       :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
    1.59 +  "_Beta_star"  :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80)
    1.60 +translations 
    1.61 +  "t1 \<longrightarrow>\<^isub>\<beta> t2" \<rightleftharpoons> "(t1,t2) \<in> Beta"
    1.62 +  "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" \<rightleftharpoons> "(t1,t2) \<in> Beta\<^sup>*"
    1.63 +inductive Beta
    1.64 +  intros
    1.65 +  b1[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App s1 t)\<longrightarrow>\<^isub>\<beta>(App s2 t)"
    1.66 +  b2[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App t s1)\<longrightarrow>\<^isub>\<beta>(App t s2)"
    1.67 +  b3[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>\<beta> (Lam [(a::name)].s2)"
    1.68 +  b4[intro!]: "(App (Lam [(a::name)].s1) s2)\<longrightarrow>\<^isub>\<beta>(s1[a::=s2])"
    1.69 +
    1.70 +lemma eqvt_beta: 
    1.71 +  fixes pi :: "name prm"
    1.72 +  and   t  :: "lam"
    1.73 +  and   s  :: "lam"
    1.74 +  shows "t\<longrightarrow>\<^isub>\<beta>s \<Longrightarrow> (pi\<bullet>t)\<longrightarrow>\<^isub>\<beta>(pi\<bullet>s)"
    1.75 +  apply(erule Beta.induct)
    1.76 +  apply(auto)
    1.77 +  done
    1.78 +
    1.79 +lemma beta_induct_aux[rule_format]:
    1.80 +  fixes  P :: "lam \<Rightarrow> lam \<Rightarrow>'a::fs_name\<Rightarrow>bool"
    1.81 +  and    t :: "lam"
    1.82 +  and    s :: "lam"
    1.83 +  assumes a: "t\<longrightarrow>\<^isub>\<beta>s"
    1.84 +  and a1:    "\<And>x t s1 s2. 
    1.85 +              s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (App s1 t) (App s2 t) x"
    1.86 +  and a2:    "\<And>x t s1 s2. 
    1.87 +              s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (App t s1) (App t s2) x"
    1.88 +  and a3:    "\<And>x (a::name) s1 s2. 
    1.89 +              a\<sharp>x \<Longrightarrow> s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (Lam [a].s1) (Lam [a].s2) x"
    1.90 +  and a4:    "\<And>x (a::name) t1 s1. a\<sharp>(s1,x) \<Longrightarrow> P (App (Lam [a].t1) s1) (t1[a::=s1]) x"
    1.91 +  shows "\<forall>x (pi::name prm). P (pi\<bullet>t) (pi\<bullet>s) x"
    1.92 +using a
    1.93 +proof (induct)
    1.94 +  case b1 thus ?case using a1 by (simp, blast intro: eqvt_beta)
    1.95 +next
    1.96 +  case b2 thus ?case using a2 by (simp, blast intro: eqvt_beta)
    1.97 +next
    1.98 +  case (b3 a s1 s2)
    1.99 +  assume j1: "s1 \<longrightarrow>\<^isub>\<beta> s2"
   1.100 +  assume j2: "\<forall>x (pi::name prm). P (pi\<bullet>s1) (pi\<bullet>s2) x"
   1.101 +  show ?case 
   1.102 +  proof (simp, intro strip)
   1.103 +    fix pi::"name prm" and x::"'a::fs_name"
   1.104 +     have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
   1.105 +      by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
   1.106 +    then obtain c::"name" 
   1.107 +      where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>s1)" and f4: "c\<sharp>(pi\<bullet>s2)"
   1.108 +      by (force simp add: fresh_prod fresh_atm)
   1.109 +    have x: "P (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s1)) (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s2)) x"
   1.110 +      using a3 f2 j1 j2 by (simp, blast intro: eqvt_beta)
   1.111 +    have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s1))" using f1 f3
   1.112 +      by (simp add: lam.inject alpha)
   1.113 +    have alpha2: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s2))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s2))" using f1 f3
   1.114 +      by (simp add: lam.inject alpha)
   1.115 +    show " P (Lam [(pi\<bullet>a)].(pi\<bullet>s1)) (Lam [(pi\<bullet>a)].(pi\<bullet>s2)) x"
   1.116 +      using x alpha1 alpha2 by (simp only: pt_name2)
   1.117 +  qed
   1.118 +next
   1.119 +  case (b4 a s1 s2)
   1.120 +  show ?case
   1.121 +  proof (simp add: subst_eqvt, intro strip)
   1.122 +    fix pi::"name prm" and x::"'a::fs_name" 
   1.123 +    have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
   1.124 +      by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
   1.125 +    then obtain c::"name" 
   1.126 +      where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>(pi\<bullet>s2,x)" and f3: "c\<sharp>(pi\<bullet>s1)" and f4: "c\<sharp>(pi\<bullet>s2)"
   1.127 +      by (force simp add: fresh_prod fresh_atm)
   1.128 +    have x: "P (App (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s1)) (pi\<bullet>s2)) ((([(c,pi\<bullet>a)]@pi)\<bullet>s1)[c::=(pi\<bullet>s2)]) x"
   1.129 +      using a4 f2 by (blast intro!: eqvt_beta)
   1.130 +    have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s1))" using f1 f3
   1.131 +      by (simp add: lam.inject alpha)
   1.132 +    have alpha2: "(([(c,pi\<bullet>a)]@pi)\<bullet>s1)[c::=(pi\<bullet>s2)] = (pi\<bullet>s1)[(pi\<bullet>a)::=(pi\<bullet>s2)]"
   1.133 +      using f3 by (simp only: subst_rename[symmetric] pt_name2)
   1.134 +    show "P (App (Lam [(pi\<bullet>a)].(pi\<bullet>s1)) (pi\<bullet>s2)) ((pi\<bullet>s1)[(pi\<bullet>a)::=(pi\<bullet>s2)]) x"
   1.135 +      using x alpha1 alpha2 by (simp only: pt_name2)
   1.136 +  qed
   1.137 +qed
   1.138 +
   1.139 +lemma beta_induct[case_names b1 b2 b3 b4]:
   1.140 +  fixes  P :: "lam \<Rightarrow> lam \<Rightarrow>'a::fs_name\<Rightarrow>bool"
   1.141 +  and    t :: "lam"
   1.142 +  and    s :: "lam"
   1.143 +  and    x :: "'a::fs_name"
   1.144 +  assumes a: "t\<longrightarrow>\<^isub>\<beta>s"
   1.145 +  and a1:    "\<And>x t s1 s2. 
   1.146 +              s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (App s1 t) (App s2 t) x"
   1.147 +  and a2:    "\<And>x t s1 s2. 
   1.148 +              s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (App t s1) (App t s2) x"
   1.149 +  and a3:    "\<And>x (a::name) s1 s2. 
   1.150 +              a\<sharp>x \<Longrightarrow> s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (Lam [a].s1) (Lam [a].s2) x"
   1.151 +  and a4:    "\<And>x (a::name) t1 s1. 
   1.152 +              a\<sharp>(s1,x) \<Longrightarrow> P (App (Lam [a].t1) s1) (t1[a::=s1]) x"
   1.153 +  shows "P t s x"
   1.154 +using a a1 a2 a3 a4
   1.155 +by (auto intro!: beta_induct_aux[of "t" "s" "P" "[]" "x", simplified])
   1.156 +
   1.157 +lemma supp_beta: "t\<longrightarrow>\<^isub>\<beta> s\<Longrightarrow>(supp s)\<subseteq>((supp t)::name set)"
   1.158 +apply(erule Beta.induct)
   1.159 +apply(auto intro!: simp add: abs_supp lam.supp subst_supp)
   1.160 +done
   1.161 +lemma beta_abs: "Lam [a].t\<longrightarrow>\<^isub>\<beta> t'\<Longrightarrow>\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>\<beta> t''"
   1.162 +apply(ind_cases "Lam [a].t  \<longrightarrow>\<^isub>\<beta> t'")
   1.163 +apply(auto simp add: lam.distinct lam.inject)
   1.164 +apply(auto simp add: alpha)
   1.165 +apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)
   1.166 +apply(rule conjI)
   1.167 +apply(rule sym)
   1.168 +apply(rule pt_bij2[OF pt_name_inst, OF at_name_inst])
   1.169 +apply(simp)
   1.170 +apply(rule pt_name3)
   1.171 +apply(simp add: at_ds5[OF at_name_inst])
   1.172 +apply(rule conjI)
   1.173 +apply(simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst] calc_atm)
   1.174 +apply(force dest!: supp_beta simp add: fresh_def)
   1.175 +apply(force intro!: eqvt_beta)
   1.176 +done
   1.177 +
   1.178 +lemma beta_subst[rule_format]: 
   1.179 +  assumes a: "M \<longrightarrow>\<^isub>\<beta> M'"
   1.180 +  shows "M[x::=N]\<longrightarrow>\<^isub>\<beta> M'[x::=N]" 
   1.181 +using a
   1.182 +apply(nominal_induct M M' rule: beta_induct)
   1.183 +apply(auto simp add: fresh_prod fresh_atm subs_lemma)
   1.184 +done
   1.185 +
   1.186 +instance nat :: fs_name
   1.187 +apply(intro_classes)   
   1.188 +apply(simp_all add: supp_def perm_nat_def)
   1.189 +done
   1.190 +
   1.191 +datatype ty =
   1.192 +    TVar "string"
   1.193 +  | TArr "ty" "ty" (infix "\<rightarrow>" 200)
   1.194 +
   1.195 +primrec
   1.196 + "pi\<bullet>(TVar s) = TVar s"
   1.197 + "pi\<bullet>(\<tau> \<rightarrow> \<sigma>) = (\<tau> \<rightarrow> \<sigma>)"
   1.198 +
   1.199 +lemma perm_ty[simp]:
   1.200 +  fixes pi ::"name prm"
   1.201 +  and   \<tau>  ::"ty"
   1.202 +  shows "pi\<bullet>\<tau> = \<tau>"
   1.203 +  by (cases \<tau>, simp_all)
   1.204 +
   1.205 +lemma fresh_ty:
   1.206 +  fixes a ::"name"
   1.207 +  and   \<tau>  ::"ty"
   1.208 +  shows "a\<sharp>\<tau>"
   1.209 +  by (simp add: fresh_def supp_def)
   1.210 +
   1.211 +instance ty :: pt_name
   1.212 +apply(intro_classes)   
   1.213 +apply(simp_all)
   1.214 +done
   1.215 +
   1.216 +instance ty :: fs_name
   1.217 +apply(intro_classes)
   1.218 +apply(simp add: supp_def)
   1.219 +done
   1.220 +
   1.221 +(* valid contexts *)
   1.222 +
   1.223 +consts
   1.224 +  "dom_ty" :: "(name\<times>ty) list \<Rightarrow> (name list)"
   1.225 +primrec
   1.226 +  "dom_ty []    = []"
   1.227 +  "dom_ty (x#\<Gamma>) = (fst x)#(dom_ty \<Gamma>)" 
   1.228 +
   1.229 +consts
   1.230 +  ctxts :: "((name\<times>ty) list) set" 
   1.231 +  valid :: "(name\<times>ty) list \<Rightarrow> bool"
   1.232 +translations
   1.233 +  "valid \<Gamma>" \<rightleftharpoons> "\<Gamma> \<in> ctxts"  
   1.234 +inductive ctxts
   1.235 +intros
   1.236 +v1[intro]: "valid []"
   1.237 +v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)"
   1.238 +
   1.239 +lemma valid_eqvt:
   1.240 +  fixes   pi:: "name prm"
   1.241 +  assumes a: "valid \<Gamma>"
   1.242 +  shows   "valid (pi\<bullet>\<Gamma>)"
   1.243 +using a
   1.244 +apply(induct)
   1.245 +apply(auto simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst])
   1.246 +done
   1.247 +
   1.248 +(* typing judgements *)
   1.249 +
   1.250 +lemma fresh_context[rule_format]: 
   1.251 +  fixes  \<Gamma> :: "(name\<times>ty)list"
   1.252 +  and    a :: "name"
   1.253 +  shows "a\<sharp>\<Gamma>\<longrightarrow>\<not>(\<exists>\<tau>::ty. (a,\<tau>)\<in>set \<Gamma>)"
   1.254 +apply(induct_tac \<Gamma>)
   1.255 +apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
   1.256 +done
   1.257 +
   1.258 +lemma valid_elim: 
   1.259 +  fixes  \<Gamma> :: "(name\<times>ty)list"
   1.260 +  and    pi:: "name prm"
   1.261 +  and    a :: "name"
   1.262 +  and    \<tau> :: "ty"
   1.263 +  shows "valid ((a,\<tau>)#\<Gamma>) \<Longrightarrow> valid \<Gamma> \<and> a\<sharp>\<Gamma>"
   1.264 +apply(ind_cases "valid ((a,\<tau>)#\<Gamma>)", simp)
   1.265 +done
   1.266 +
   1.267 +lemma valid_unicity[rule_format]: 
   1.268 +  shows "valid \<Gamma>\<longrightarrow>(c,\<sigma>)\<in>set \<Gamma>\<longrightarrow>(c,\<tau>)\<in>set \<Gamma>\<longrightarrow>\<sigma>=\<tau>" 
   1.269 +apply(induct_tac \<Gamma>)
   1.270 +apply(auto dest!: valid_elim fresh_context)
   1.271 +done
   1.272 +
   1.273 +consts
   1.274 +  typing :: "(((name\<times>ty) list)\<times>lam\<times>ty) set" 
   1.275 +syntax
   1.276 +  "_typing_judge" :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80) 
   1.277 +translations
   1.278 +  "\<Gamma> \<turnstile> t : \<tau>" \<rightleftharpoons> "(\<Gamma>,t,\<tau>) \<in> typing"  
   1.279 +
   1.280 +inductive typing
   1.281 +intros
   1.282 +t1[intro]: "\<lbrakk>valid \<Gamma>; (a,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var a : \<tau>"
   1.283 +t2[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>"
   1.284 +t3[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>"
   1.285 +
   1.286 +lemma typing_eqvt: 
   1.287 +  fixes  \<Gamma> :: "(name\<times>ty) list"
   1.288 +  and    t :: "lam"
   1.289 +  and    \<tau> :: "ty"
   1.290 +  and    pi:: "name prm"
   1.291 +  assumes a: "\<Gamma> \<turnstile> t : \<tau>"
   1.292 +  shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>t) : \<tau>"
   1.293 +using a
   1.294 +proof (induct)
   1.295 +  case (t1 \<Gamma> \<tau> a)
   1.296 +  have "valid (pi\<bullet>\<Gamma>)" by (rule valid_eqvt)
   1.297 +  moreover
   1.298 +  have "(pi\<bullet>(a,\<tau>))\<in>((pi::name prm)\<bullet>set \<Gamma>)" by (rule pt_set_bij2[OF pt_name_inst, OF at_name_inst])
   1.299 +  ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Var a) : \<tau>"
   1.300 +    using typing.intros by (auto simp add: pt_list_set_pi[OF pt_name_inst])
   1.301 +next 
   1.302 +  case (t3 \<Gamma> \<sigma> \<tau> a t)
   1.303 +  moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (rule pt_fresh_bij1[OF pt_name_inst, OF at_name_inst])
   1.304 +  ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) : \<tau>\<rightarrow>\<sigma>" 
   1.305 +    using typing.intros by (force)
   1.306 +qed (auto)
   1.307 +
   1.308 +lemma typing_induct_aux[rule_format]:
   1.309 +  fixes  P :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow>'a::fs_name\<Rightarrow>bool"
   1.310 +  and    \<Gamma> :: "(name\<times>ty) list"
   1.311 +  and    t :: "lam"
   1.312 +  and    \<tau> :: "ty"
   1.313 +  assumes a: "\<Gamma> \<turnstile> t : \<tau>"
   1.314 +  and a1:    "\<And>x \<Gamma> (a::name) \<tau>. valid \<Gamma> \<Longrightarrow> (a,\<tau>) \<in> set \<Gamma> \<Longrightarrow> P \<Gamma> (Var a) \<tau> x"
   1.315 +  and a2:    "\<And>x \<Gamma> \<tau> \<sigma> t1 t2. 
   1.316 +              \<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma> \<Longrightarrow> (\<And>z. P \<Gamma> t1 (\<tau>\<rightarrow>\<sigma>) z) \<Longrightarrow> \<Gamma> \<turnstile> t2 : \<tau> \<Longrightarrow> (\<And>z. P \<Gamma> t2 \<tau> z)
   1.317 +              \<Longrightarrow> P \<Gamma> (App t1 t2) \<sigma> x"
   1.318 +  and a3:    "\<And>x (a::name) \<Gamma> \<tau> \<sigma> t. 
   1.319 +              a\<sharp>x \<Longrightarrow> a\<sharp>\<Gamma> \<Longrightarrow> ((a,\<tau>) # \<Gamma>) \<turnstile> t : \<sigma> \<Longrightarrow> (\<forall>z. P ((a,\<tau>)#\<Gamma>) t \<sigma> z)
   1.320 +              \<Longrightarrow> P \<Gamma> (Lam [a].t) (\<tau>\<rightarrow>\<sigma>) x"
   1.321 +  shows "\<forall>(pi::name prm) (x::'a::fs_name). P (pi\<bullet>\<Gamma>) (pi\<bullet>t) \<tau> x"
   1.322 +using a
   1.323 +proof (induct)
   1.324 +  case (t1 \<Gamma> \<tau> a)
   1.325 +  assume j1: "valid \<Gamma>"
   1.326 +  assume j2: "(a,\<tau>)\<in>set \<Gamma>"
   1.327 +  show ?case
   1.328 +  proof (intro strip, simp)
   1.329 +    fix pi::"name prm" and x::"'a::fs_name"
   1.330 +    from j1 have j3: "valid (pi\<bullet>\<Gamma>)" by (rule valid_eqvt)
   1.331 +    from j2 have "pi\<bullet>(a,\<tau>)\<in>pi\<bullet>(set \<Gamma>)" by (simp only: pt_set_bij[OF pt_name_inst, OF at_name_inst])  
   1.332 +    hence j4: "(pi\<bullet>a,\<tau>)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: pt_list_set_pi[OF pt_name_inst])
   1.333 +    show "P (pi\<bullet>\<Gamma>) (Var (pi\<bullet>a)) \<tau> x" using a1 j3 j4 by force
   1.334 +  qed
   1.335 +next
   1.336 +  case (t2 \<Gamma> \<sigma> \<tau> t1 t2)
   1.337 +  thus ?case using a2 by (simp, blast intro: typing_eqvt)
   1.338 +next
   1.339 +  case (t3 \<Gamma> \<sigma> \<tau> a t)
   1.340 +  have k1: "a\<sharp>\<Gamma>" by fact
   1.341 +  have k2: "((a,\<tau>)#\<Gamma>)\<turnstile>t:\<sigma>" by fact
   1.342 +  have k3: "\<forall>(pi::name prm) (x::'a::fs_name). P (pi \<bullet> ((a,\<tau>)#\<Gamma>)) (pi\<bullet>t) \<sigma> x" by fact
   1.343 +  show ?case
   1.344 +  proof (intro strip, simp)
   1.345 +    fix pi::"name prm" and x::"'a::fs_name"
   1.346 +    have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t,pi\<bullet>\<Gamma>,x)"
   1.347 +      by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
   1.348 +    then obtain c::"name" 
   1.349 +      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>)"
   1.350 +      by (force simp add: fresh_prod fresh_atm)
   1.351 +    from k1 have k1a: "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" 
   1.352 +      by (simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst] 
   1.353 +                    pt_rev_pi[OF pt_name_inst, OF at_name_inst])
   1.354 +    have l1: "(([(c,pi\<bullet>a)]@pi)\<bullet>\<Gamma>) = (pi\<bullet>\<Gamma>)" using f4 k1a 
   1.355 +      by (simp only: pt_name2, rule pt_fresh_fresh[OF pt_name_inst, OF at_name_inst])
   1.356 +    have "\<forall>x. P (([(c,pi\<bullet>a)]@pi)\<bullet>((a,\<tau>)#\<Gamma>)) (([(c,pi\<bullet>a)]@pi)\<bullet>t) \<sigma> x" using k3 by force
   1.357 +    hence l2: "\<forall>x. P ((c, \<tau>)#(pi\<bullet>\<Gamma>)) (([(c,pi\<bullet>a)]@pi)\<bullet>t) \<sigma> x" using f1 l1
   1.358 +      by (force simp add: pt_name2  calc_atm split: if_splits)
   1.359 +    have "(([(c,pi\<bullet>a)]@pi)\<bullet>((a,\<tau>)#\<Gamma>)) \<turnstile> (([(c,pi\<bullet>a)]@pi)\<bullet>t) : \<sigma>" using k2 by (rule typing_eqvt)
   1.360 +    hence l3: "((c, \<tau>)#(pi\<bullet>\<Gamma>)) \<turnstile> (([(c,pi\<bullet>a)]@pi)\<bullet>t) : \<sigma>" using l1 f1 
   1.361 +      by (force simp add: pt_name2 calc_atm split: if_splits)
   1.362 +    have l4: "P (pi\<bullet>\<Gamma>) (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>t)) (\<tau> \<rightarrow> \<sigma>) x" using f2 f4 l2 l3 a3 by auto
   1.363 +    have alpha: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t))) = (Lam [(pi\<bullet>a)].(pi\<bullet>t))" using f1 f3
   1.364 +      by (simp add: lam.inject alpha)
   1.365 +    show "P (pi\<bullet>\<Gamma>) (Lam [(pi\<bullet>a)].(pi\<bullet>t)) (\<tau> \<rightarrow> \<sigma>) x" using l4 alpha 
   1.366 +      by (simp only: pt_name2)
   1.367 +  qed
   1.368 +qed
   1.369 +
   1.370 +lemma typing_induct[case_names t1 t2 t3]:
   1.371 +  fixes  P :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow>'a::fs_name\<Rightarrow>bool"
   1.372 +  and    \<Gamma> :: "(name\<times>ty) list"
   1.373 +  and    t :: "lam"
   1.374 +  and    \<tau> :: "ty"
   1.375 +  and    x :: "'a::fs_name"
   1.376 +  assumes a: "\<Gamma> \<turnstile> t : \<tau>"
   1.377 +  and a1:    "\<And>x \<Gamma> (a::name) \<tau>. valid \<Gamma> \<Longrightarrow> (a,\<tau>) \<in> set \<Gamma> \<Longrightarrow> P \<Gamma> (Var a) \<tau> x"
   1.378 +  and a2:    "\<And>x \<Gamma> \<tau> \<sigma> t1 t2. 
   1.379 +              \<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma> \<Longrightarrow> (\<forall>z. P \<Gamma> t1 (\<tau>\<rightarrow>\<sigma>) z) \<Longrightarrow> \<Gamma> \<turnstile> t2 : \<tau> \<Longrightarrow> (\<forall>z. P \<Gamma> t2 \<tau> z)
   1.380 +              \<Longrightarrow> P \<Gamma> (App t1 t2) \<sigma> x"
   1.381 +  and a3:    "\<And>x (a::name) \<Gamma> \<tau> \<sigma> t. 
   1.382 +              a\<sharp>x \<Longrightarrow> a\<sharp>\<Gamma> \<Longrightarrow> ((a,\<tau>) # \<Gamma>) \<turnstile> t : \<sigma> \<Longrightarrow> (\<forall>z. P ((a,\<tau>)#\<Gamma>) t \<sigma> z)
   1.383 +              \<Longrightarrow> P \<Gamma> (Lam [a].t) (\<tau>\<rightarrow>\<sigma>) x"
   1.384 +  shows "P \<Gamma> t \<tau> x"
   1.385 +using a a1 a2 a3 typing_induct_aux[of "\<Gamma>" "t" "\<tau>" "P" "[]" "x", simplified] by force
   1.386 +
   1.387 +constdefs
   1.388 +  "sub" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" (" _ \<lless> _ " [80,80] 80)
   1.389 +  "\<Gamma>1 \<lless> \<Gamma>2 \<equiv> \<forall>a \<sigma>. (a,\<sigma>)\<in>set \<Gamma>1 \<longrightarrow>  (a,\<sigma>)\<in>set \<Gamma>2"
   1.390 +
   1.391 +lemma weakening[rule_format]: 
   1.392 +  assumes a: "\<Gamma>1 \<turnstile> t : \<sigma>"
   1.393 +  shows "valid \<Gamma>2 \<longrightarrow> \<Gamma>1 \<lless> \<Gamma>2 \<longrightarrow> \<Gamma>2 \<turnstile> t:\<sigma>"
   1.394 +using a
   1.395 +apply(nominal_induct \<Gamma>1 t \<sigma> rule: typing_induct)
   1.396 +apply(auto simp add: sub_def)
   1.397 +done
   1.398 +
   1.399 +lemma in_ctxt[rule_format]: "(a,\<tau>)\<in>set \<Gamma> \<longrightarrow> (a\<in>set(dom_ty \<Gamma>))"
   1.400 +apply(induct_tac \<Gamma>)
   1.401 +apply(auto)
   1.402 +done
   1.403 +
   1.404 +lemma free_vars: 
   1.405 +  assumes a: "\<Gamma> \<turnstile> t : \<tau>"
   1.406 +  shows " (supp t)\<subseteq>set(dom_ty \<Gamma>)"
   1.407 +using a
   1.408 +apply(nominal_induct \<Gamma> t \<tau> rule: typing_induct)
   1.409 +apply(auto simp add: lam.supp abs_supp supp_atm in_ctxt)
   1.410 +done
   1.411 +
   1.412 +lemma t1_elim: "\<Gamma> \<turnstile> Var a : \<tau> \<Longrightarrow> valid \<Gamma> \<and> (a,\<tau>) \<in> set \<Gamma>"
   1.413 +apply(ind_cases "\<Gamma> \<turnstile> Var a : \<tau>")
   1.414 +apply(auto simp add: lam.inject lam.distinct)
   1.415 +done
   1.416 +
   1.417 +lemma t2_elim: "\<Gamma> \<turnstile> App t1 t2 : \<sigma> \<Longrightarrow> \<exists>\<tau>. (\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma> \<and> \<Gamma> \<turnstile> t2 : \<tau>)"
   1.418 +apply(ind_cases "\<Gamma> \<turnstile> App t1 t2 : \<sigma>")
   1.419 +apply(auto simp add: lam.inject lam.distinct)
   1.420 +done
   1.421 +
   1.422 +lemma t3_elim: "\<lbrakk>\<Gamma> \<turnstile> Lam [a].t : \<sigma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> \<exists>\<tau> \<tau>'. \<sigma>=\<tau>\<rightarrow>\<tau>' \<and> ((a,\<tau>)#\<Gamma>) \<turnstile> t : \<tau>'"
   1.423 +apply(ind_cases "\<Gamma> \<turnstile> Lam [a].t : \<sigma>")
   1.424 +apply(auto simp add: lam.distinct lam.inject alpha) 
   1.425 +apply(drule_tac pi="[(a,aa)]::name prm" in typing_eqvt)
   1.426 +apply(simp)
   1.427 +apply(subgoal_tac "([(a,aa)]::name prm)\<bullet>\<Gamma> = \<Gamma>")(*A*)
   1.428 +apply(force simp add: calc_atm)
   1.429 +(*A*)
   1.430 +apply(force intro!: pt_fresh_fresh[OF pt_name_inst, OF at_name_inst])
   1.431 +done
   1.432 +
   1.433 +lemma typing_valid: 
   1.434 +  assumes a: "\<Gamma> \<turnstile> t : \<tau>" 
   1.435 +  shows "valid \<Gamma>"
   1.436 +using a by (induct, auto dest!: valid_elim)
   1.437 +
   1.438 +lemma ty_subs[rule_format]:
   1.439 +  fixes \<Gamma> ::"(name\<times>ty) list"
   1.440 +  and   t1 ::"lam"
   1.441 +  and   t2 ::"lam"
   1.442 +  and   \<tau>  ::"ty"
   1.443 +  and   \<sigma>  ::"ty" 
   1.444 +  and   c  ::"name"
   1.445 +  shows  "((c,\<sigma>)#\<Gamma>) \<turnstile> t1:\<tau>\<longrightarrow> \<Gamma>\<turnstile> t2:\<sigma>\<longrightarrow> \<Gamma> \<turnstile> t1[c::=t2]:\<tau>"
   1.446 +proof(nominal_induct t1 rule: lam_induct)
   1.447 +  case (Var \<Gamma> \<sigma> \<tau> c t2 a)
   1.448 +  show ?case
   1.449 +  proof(intro strip)
   1.450 +    assume a1: "\<Gamma> \<turnstile>t2:\<sigma>"
   1.451 +    assume a2: "((c,\<sigma>)#\<Gamma>) \<turnstile> Var a:\<tau>"
   1.452 +    hence a21: "(a,\<tau>)\<in>set((c,\<sigma>)#\<Gamma>)" and a22: "valid((c,\<sigma>)#\<Gamma>)" by (auto dest: t1_elim)
   1.453 +    from a22 have a23: "valid \<Gamma>" and a24: "c\<sharp>\<Gamma>" by (auto dest: valid_elim) 
   1.454 +    from a24 have a25: "\<not>(\<exists>\<tau>. (c,\<tau>)\<in>set \<Gamma>)" by (rule fresh_context)
   1.455 +    show "\<Gamma>\<turnstile>(Var a)[c::=t2] : \<tau>"
   1.456 +    proof (cases "a=c", simp_all)
   1.457 +      assume case1: "a=c"
   1.458 +      show "\<Gamma> \<turnstile> t2:\<tau>" using a1
   1.459 +      proof (cases "\<sigma>=\<tau>")
   1.460 +	assume "\<sigma>=\<tau>" thus ?thesis using a1 by simp 
   1.461 +      next
   1.462 +	assume a3: "\<sigma>\<noteq>\<tau>"
   1.463 +	show ?thesis
   1.464 +	proof (rule ccontr)
   1.465 +	  from a3 a21 have "(a,\<tau>)\<in>set \<Gamma>" by force
   1.466 +	  with case1 a25 show False by force 
   1.467 +	qed
   1.468 +      qed
   1.469 +    next
   1.470 +      assume case2: "a\<noteq>c"
   1.471 +      with a21 have a26: "(a,\<tau>)\<in>set \<Gamma>" by force 
   1.472 +      from a23 a26 show "\<Gamma> \<turnstile> Var a:\<tau>" by force
   1.473 +    qed
   1.474 +  qed
   1.475 +next
   1.476 +  case (App \<Gamma> \<sigma> \<tau> c t2 s1 s2)
   1.477 +  show ?case
   1.478 +  proof (intro strip, simp)
   1.479 +    assume b1: "\<Gamma> \<turnstile>t2:\<sigma>" 
   1.480 +    assume b2: " ((c,\<sigma>)#\<Gamma>)\<turnstile>App s1 s2 : \<tau>"
   1.481 +    hence "\<exists>\<tau>'. (((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau> \<and> ((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>')" by (rule t2_elim) 
   1.482 +    then obtain \<tau>' where b3a: "((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau>" and b3b: "((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>'" by force
   1.483 +    show "\<Gamma> \<turnstile>  App (s1[c::=t2]) (s2[c::=t2]) : \<tau>" 
   1.484 +      using b1 b3a b3b App by (rule_tac \<tau>="\<tau>'" in t2, auto)
   1.485 +  qed
   1.486 +next
   1.487 +  case (Lam \<Gamma> \<sigma> \<tau> c t2 a s)
   1.488 +  assume "a\<sharp>(\<Gamma>,\<sigma>,\<tau>,c,t2)" 
   1.489 +  hence f1: "a\<sharp>\<Gamma>" and f2: "a\<noteq>c" and f2': "c\<sharp>a" and f3: "a\<sharp>t2" and f4: "a\<sharp>((c,\<sigma>)#\<Gamma>)"
   1.490 +    by (auto simp add: fresh_atm fresh_prod fresh_list_cons)
   1.491 +  show ?case using f2 f3
   1.492 +  proof(intro strip, simp)
   1.493 +    assume c1: "((c,\<sigma>)#\<Gamma>)\<turnstile>Lam [a].s : \<tau>"
   1.494 +    hence "\<exists>\<tau>1 \<tau>2. \<tau>=\<tau>1\<rightarrow>\<tau>2 \<and> ((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<turnstile> s : \<tau>2" using f4 by (auto dest: t3_elim) 
   1.495 +    then obtain \<tau>1 \<tau>2 where c11: "\<tau>=\<tau>1\<rightarrow>\<tau>2" and c12: "((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<turnstile> s : \<tau>2" by force
   1.496 +    from c12 have "valid ((a,\<tau>1)#(c,\<sigma>)#\<Gamma>)" by (rule typing_valid)
   1.497 +    hence ca: "valid \<Gamma>" and cb: "a\<sharp>\<Gamma>" and cc: "c\<sharp>\<Gamma>" 
   1.498 +      by (auto dest: valid_elim simp add: fresh_list_cons) 
   1.499 +    from c12 have c14: "((c,\<sigma>)#(a,\<tau>1)#\<Gamma>) \<turnstile> s : \<tau>2"
   1.500 +    proof -
   1.501 +      have c2: "((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<lless> ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)" by (force simp add: sub_def)
   1.502 +      have c3: "valid ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)"
   1.503 +	by (rule v2, rule v2, auto simp add: fresh_list_cons fresh_prod ca cb cc f2' fresh_ty)
   1.504 +      from c12 c2 c3 show ?thesis by (force intro: weakening)
   1.505 +    qed
   1.506 +    assume c8: "\<Gamma> \<turnstile> t2 : \<sigma>"
   1.507 +    have c81: "((a,\<tau>1)#\<Gamma>)\<turnstile>t2 :\<sigma>"
   1.508 +    proof -
   1.509 +      have c82: "\<Gamma> \<lless> ((a,\<tau>1)#\<Gamma>)" by (force simp add: sub_def)
   1.510 +      have c83: "valid ((a,\<tau>1)#\<Gamma>)" using f1 ca by force
   1.511 +      with c8 c82 c83 show ?thesis by (force intro: weakening)
   1.512 +    qed
   1.513 +    show "\<Gamma> \<turnstile> Lam [a].(s[c::=t2]) : \<tau>"
   1.514 +      using c11 Lam c14 c81 f1 by force
   1.515 +  qed
   1.516 +qed
   1.517 +
   1.518 +lemma subject[rule_format]: 
   1.519 +  fixes \<Gamma>  ::"(name\<times>ty) list"
   1.520 +  and   t1 ::"lam"
   1.521 +  and   t2 ::"lam"
   1.522 +  and   \<tau>  ::"ty"
   1.523 +  assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2"
   1.524 +  shows "(\<Gamma> \<turnstile> t1:\<tau>) \<longrightarrow> (\<Gamma> \<turnstile> t2:\<tau>)"
   1.525 +using a
   1.526 +proof (nominal_induct t1 t2 rule: beta_induct, auto)
   1.527 +  case (b1 \<Gamma> \<tau> t s1 s2)
   1.528 +  assume i: "\<forall>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" 
   1.529 +  assume "\<Gamma> \<turnstile> App s1 t : \<tau>"
   1.530 +  hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> t : \<sigma>)" by (rule t2_elim)
   1.531 +  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> t : \<sigma>" by force
   1.532 +  thus "\<Gamma> \<turnstile> App s2 t : \<tau>" using i by force
   1.533 +next
   1.534 +  case (b2 \<Gamma> \<tau> t s1 s2)
   1.535 +  assume i: "\<forall>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" 
   1.536 +  assume "\<Gamma> \<turnstile> App t s1 : \<tau>"
   1.537 +  hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> s1 : \<sigma>)" by (rule t2_elim)
   1.538 +  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> s1 : \<sigma>" by force
   1.539 +  thus "\<Gamma> \<turnstile> App t s2 : \<tau>" using i by force
   1.540 +next
   1.541 +  case (b3 \<Gamma> \<tau> a s1 s2)
   1.542 +  assume "a\<sharp>(\<Gamma>,\<tau>)"
   1.543 +  hence f: "a\<sharp>\<Gamma>" by (simp add: fresh_prod)
   1.544 +  assume i: "\<forall>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" 
   1.545 +  assume "\<Gamma> \<turnstile> Lam [a].s1 : \<tau>"
   1.546 +  with f have "\<exists>\<tau>1 \<tau>2. \<tau>=\<tau>1\<rightarrow>\<tau>2 \<and> ((a,\<tau>1)#\<Gamma>) \<turnstile> s1 : \<tau>2" by (force dest: t3_elim)
   1.547 +  then obtain \<tau>1 \<tau>2 where a1: "\<tau>=\<tau>1\<rightarrow>\<tau>2" and a2: "((a,\<tau>1)#\<Gamma>) \<turnstile> s1 : \<tau>2" by force
   1.548 +  thus "\<Gamma> \<turnstile> Lam [a].s2 : \<tau>" using f i by force 
   1.549 +next
   1.550 +  case (b4 \<Gamma> \<tau> a s1 s2)
   1.551 +  have "a\<sharp>(s2,\<Gamma>,\<tau>)" by fact
   1.552 +  hence f: "a\<sharp>\<Gamma>" by (simp add: fresh_prod)
   1.553 +  assume "\<Gamma> \<turnstile> App (Lam [a].s1) s2 : \<tau>"
   1.554 +  hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> (Lam [a].s1) : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> s2 : \<sigma>)" by (rule t2_elim)
   1.555 +  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> (Lam [(a::name)].s1) : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> s2 : \<sigma>" by force
   1.556 +  have  "((a,\<sigma>)#\<Gamma>) \<turnstile> s1 : \<tau>" using a1 f by (auto dest!: t3_elim)
   1.557 +  with a2 show "\<Gamma> \<turnstile>  s1[a::=s2] : \<tau>" by (force intro: ty_subs)
   1.558 +qed
   1.559 +
   1.560 +
   1.561 +lemma subject[rule_format]: 
   1.562 +  fixes \<Gamma>  ::"(name\<times>ty) list"
   1.563 +  and   t1 ::"lam"
   1.564 +  and   t2 ::"lam"
   1.565 +  and   \<tau>  ::"ty"
   1.566 +  assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2"
   1.567 +  shows "\<Gamma> \<turnstile> t1:\<tau> \<longrightarrow> \<Gamma> \<turnstile> t2:\<tau>"
   1.568 +using a
   1.569 +apply(nominal_induct t1 t2 rule: beta_induct)
   1.570 +apply(auto dest!: t2_elim t3_elim intro: ty_subs simp add: fresh_prod)
   1.571 +done
   1.572 +
   1.573 +
   1.574 +
   1.575 +subsection {* some facts about beta *}
   1.576 +
   1.577 +constdefs
   1.578 +  "NORMAL" :: "lam \<Rightarrow> bool"
   1.579 +  "NORMAL t \<equiv> \<not>(\<exists>t'. t\<longrightarrow>\<^isub>\<beta> t')"
   1.580 +
   1.581 +constdefs
   1.582 +  "SN" :: "lam \<Rightarrow> bool"
   1.583 +  "SN t \<equiv> t\<in>termi Beta"
   1.584 +
   1.585 +lemma qq1: "\<lbrakk>SN(t1);t1\<longrightarrow>\<^isub>\<beta> t2\<rbrakk>\<Longrightarrow>SN(t2)"
   1.586 +apply(simp add: SN_def)
   1.587 +apply(drule_tac a="t2" in acc_downward)
   1.588 +apply(auto)
   1.589 +done
   1.590 +
   1.591 +lemma qq2: "(\<forall>t2. t1\<longrightarrow>\<^isub>\<beta>t2 \<longrightarrow> SN(t2))\<Longrightarrow>SN(t1)"
   1.592 +apply(simp add: SN_def)
   1.593 +apply(rule accI)
   1.594 +apply(auto)
   1.595 +done
   1.596 +
   1.597 +
   1.598 +section {* Candidates *}
   1.599 +
   1.600 +consts
   1.601 +  RED :: "ty \<Rightarrow> lam set"
   1.602 +primrec
   1.603 + "RED (TVar X) = {t. SN(t)}"
   1.604 + "RED (\<tau>\<rightarrow>\<sigma>) =   {t. \<forall>u. (u\<in>RED \<tau> \<longrightarrow> (App t u)\<in>RED \<sigma>)}"
   1.605 +
   1.606 +constdefs
   1.607 +  NEUT :: "lam \<Rightarrow> bool"
   1.608 +  "NEUT t \<equiv> (\<exists>a. t=Var a)\<or>(\<exists>t1 t2. t=App t1 t2)" 
   1.609 +
   1.610 +(* a slight hack to get the first element of applications *)
   1.611 +consts
   1.612 +  FST :: "(lam\<times>lam) set"
   1.613 +syntax 
   1.614 +  "FST_judge"   :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<guillemotright> _" [80,80] 80)
   1.615 +translations 
   1.616 +  "t1 \<guillemotright> t2" \<rightleftharpoons> "(t1,t2) \<in> FST"
   1.617 +inductive FST
   1.618 +intros
   1.619 +fst[intro!]:  "(App t s) \<guillemotright> t"
   1.620 +
   1.621 +lemma fst_elim[elim!]: "(App t s) \<guillemotright> t' \<Longrightarrow> t=t'"
   1.622 +apply(ind_cases "App t s \<guillemotright> t'")
   1.623 +apply(simp add: lam.inject)
   1.624 +done
   1.625 +
   1.626 +lemma qq3: "SN(App t s)\<Longrightarrow>SN(t)"
   1.627 +apply(simp add: SN_def)
   1.628 +apply(subgoal_tac "\<forall>z. (App t s \<guillemotright> z) \<longrightarrow> z\<in>termi Beta")(*A*)
   1.629 +apply(force)
   1.630 +(*A*)
   1.631 +apply(erule acc_induct)
   1.632 +apply(clarify)
   1.633 +apply(ind_cases "x \<guillemotright> z")
   1.634 +apply(clarify)
   1.635 +apply(rule accI)
   1.636 +apply(auto intro: b1)
   1.637 +done
   1.638 +
   1.639 +constdefs
   1.640 +   "CR1" :: "ty \<Rightarrow> bool"
   1.641 +   "CR1 \<tau> \<equiv> \<forall> t. (t\<in>RED \<tau> \<longrightarrow> SN(t))"
   1.642 +
   1.643 +   "CR2" :: "ty \<Rightarrow> bool"
   1.644 +   "CR2 \<tau> \<equiv> \<forall>t t'. ((t\<in>RED \<tau> \<and> t \<longrightarrow>\<^isub>\<beta> t') \<longrightarrow> t'\<in>RED \<tau>)"
   1.645 +
   1.646 +   "CR3_RED" :: "lam \<Rightarrow> ty \<Rightarrow> bool"
   1.647 +   "CR3_RED t \<tau> \<equiv> \<forall>t'. (t\<longrightarrow>\<^isub>\<beta> t' \<longrightarrow>  t'\<in>RED \<tau>)" 
   1.648 +
   1.649 +   "CR3" :: "ty \<Rightarrow> bool"
   1.650 +   "CR3 \<tau> \<equiv> \<forall>t. (NEUT t \<and> CR3_RED t \<tau>) \<longrightarrow> t\<in>RED \<tau>"
   1.651 +   
   1.652 +   "CR4" :: "ty \<Rightarrow> bool"
   1.653 +   "CR4 \<tau> \<equiv> \<forall>t. (NEUT t \<and> NORMAL t) \<longrightarrow>t\<in>RED \<tau>"
   1.654 +
   1.655 +lemma CR3_CR4: "CR3 \<tau> \<Longrightarrow> CR4 \<tau>"
   1.656 +apply(simp (no_asm_use) add: CR3_def CR3_RED_def CR4_def NORMAL_def)
   1.657 +apply(blast)
   1.658 +done
   1.659 +
   1.660 +lemma sub_ind: 
   1.661 +  "SN(u)\<Longrightarrow>(u\<in>RED \<tau>\<longrightarrow>(\<forall>t. (NEUT t\<and>CR2 \<tau>\<and>CR3 \<sigma>\<and>CR3_RED t (\<tau>\<rightarrow>\<sigma>))\<longrightarrow>(App t u)\<in>RED \<sigma>))"
   1.662 +apply(simp add: SN_def)
   1.663 +apply(erule acc_induct)
   1.664 +apply(auto)
   1.665 +apply(simp add: CR3_def)
   1.666 +apply(rotate_tac 5)
   1.667 +apply(drule_tac x="App t x" in spec)
   1.668 +apply(drule mp)
   1.669 +apply(rule conjI)
   1.670 +apply(force simp only: NEUT_def)
   1.671 +apply(simp (no_asm) add: CR3_RED_def)
   1.672 +apply(clarify)
   1.673 +apply(ind_cases "App t x \<longrightarrow>\<^isub>\<beta> t'")
   1.674 +apply(simp_all add: lam.inject)
   1.675 +apply(simp only:  CR3_RED_def)
   1.676 +apply(drule_tac x="s2" in spec)
   1.677 +apply(simp)
   1.678 +apply(drule_tac x="s2" in spec)
   1.679 +apply(simp)
   1.680 +apply(drule mp)
   1.681 +apply(simp (no_asm_use) add: CR2_def)
   1.682 +apply(blast)
   1.683 +apply(drule_tac x="ta" in spec)
   1.684 +apply(force)
   1.685 +apply(auto simp only: NEUT_def lam.inject lam.distinct)
   1.686 +done
   1.687 +
   1.688 +lemma RED_props: "CR1 \<tau> \<and> CR2 \<tau> \<and> CR3 \<tau>"
   1.689 +apply(induct_tac \<tau>)
   1.690 +apply(auto)
   1.691 +(* atom types *)
   1.692 +(* C1 *)
   1.693 +apply(simp add: CR1_def)
   1.694 +(* C2 *)
   1.695 +apply(simp add: CR2_def)
   1.696 +apply(clarify)
   1.697 +apply(drule_tac ?t2.0="t'" in  qq1)
   1.698 +apply(assumption)+
   1.699 +(* C3 *)
   1.700 +apply(simp add: CR3_def CR3_RED_def)
   1.701 +apply(clarify)
   1.702 +apply(rule qq2)
   1.703 +apply(assumption)
   1.704 +(* arrow types *)
   1.705 +(* C1 *)
   1.706 +apply(simp (no_asm) add: CR1_def)
   1.707 +apply(clarify)
   1.708 +apply(subgoal_tac "NEUT (Var a)")(*A*)
   1.709 +apply(subgoal_tac "(Var a)\<in>RED ty1")(*C*)
   1.710 +apply(drule_tac x="Var a" in spec)
   1.711 +apply(simp)
   1.712 +apply(simp add: CR1_def)
   1.713 +apply(rotate_tac 1)
   1.714 +apply(drule_tac x="App t (Var a)" in spec)
   1.715 +apply(simp)
   1.716 +apply(drule qq3) 
   1.717 +apply(assumption)
   1.718 +(*C*)
   1.719 +apply(simp (no_asm_use) add: CR3_def CR3_RED_def)
   1.720 +apply(drule_tac x="Var a" in spec)
   1.721 +apply(drule mp)
   1.722 +apply(clarify)
   1.723 +apply(ind_cases " Var a \<longrightarrow>\<^isub>\<beta> t'")
   1.724 +apply(simp (no_asm_use) add: lam.distinct)+ 
   1.725 +(*A*)
   1.726 +apply(simp (no_asm) only: NEUT_def)
   1.727 +apply(rule disjCI)
   1.728 +apply(rule_tac x="a" in exI)
   1.729 +apply(simp (no_asm))
   1.730 +(* C2 *)
   1.731 +apply(simp (no_asm) add: CR2_def)
   1.732 +apply(clarify)
   1.733 +apply(drule_tac x="u" in spec)
   1.734 +apply(simp)
   1.735 +apply(subgoal_tac "App t u \<longrightarrow>\<^isub>\<beta> App t' u")(*X*)
   1.736 +apply(simp (no_asm_use) only: CR2_def)
   1.737 +apply(blast)
   1.738 +(*X*)
   1.739 +apply(force intro!: b1)
   1.740 +(* C3 *)
   1.741 +apply(unfold CR3_def)
   1.742 +apply(rule allI)
   1.743 +apply(rule impI)
   1.744 +apply(erule conjE)
   1.745 +apply(simp (no_asm))
   1.746 +apply(rule allI)
   1.747 +apply(rule impI)
   1.748 +apply(subgoal_tac "SN(u)")(*Z*)
   1.749 +apply(fold CR3_def)
   1.750 +apply(drule_tac \<tau>="ty1" and \<sigma>="ty2" in sub_ind)
   1.751 +apply(simp)
   1.752 +(*Z*)
   1.753 +apply(simp add: CR1_def)
   1.754 +done
   1.755 +
   1.756 +lemma double_acc_aux:
   1.757 +  assumes a_acc: "a \<in> acc r"
   1.758 +  and b_acc: "b \<in> acc r"
   1.759 +  and hyp: "\<And>x z.
   1.760 +    (\<And>y. (y, x) \<in> r \<Longrightarrow> y \<in> acc r) \<Longrightarrow>
   1.761 +    (\<And>y. (y, x) \<in> r \<Longrightarrow> P y z) \<Longrightarrow>
   1.762 +    (\<And>u. (u, z) \<in> r \<Longrightarrow> u \<in> acc r) \<Longrightarrow>
   1.763 +    (\<And>u. (u, z) \<in> r \<Longrightarrow> P x u) \<Longrightarrow> P x z"
   1.764 +  shows "P a b"
   1.765 +proof -
   1.766 +  from a_acc
   1.767 +  have r: "\<And>b. b \<in> acc r \<Longrightarrow> P a b"
   1.768 +  proof (induct a rule: acc.induct)
   1.769 +    case (accI x)
   1.770 +    note accI' = accI
   1.771 +    have "b \<in> acc r" .
   1.772 +    thus ?case
   1.773 +    proof (induct b rule: acc.induct)
   1.774 +      case (accI y)
   1.775 +      show ?case
   1.776 +	apply (rule hyp)
   1.777 +	apply (erule accI')
   1.778 +	apply (erule accI')
   1.779 +	apply (rule acc.accI)
   1.780 +	apply (erule accI)
   1.781 +	apply (erule accI)
   1.782 +	apply (erule accI)
   1.783 +	done
   1.784 +    qed
   1.785 +  qed
   1.786 +  from b_acc show ?thesis by (rule r)
   1.787 +qed
   1.788 +
   1.789 +lemma double_acc:
   1.790 +  "\<lbrakk>a \<in> acc r; b \<in> acc r; \<forall>x z. ((\<forall>y. (y, x)\<in>r\<longrightarrow>P y z)\<and>(\<forall>u. (u, z)\<in>r\<longrightarrow>P x u))\<longrightarrow>P x z\<rbrakk>\<Longrightarrow>P a b"
   1.791 +apply(rule_tac r="r" in double_acc_aux)
   1.792 +apply(assumption)+
   1.793 +apply(blast)
   1.794 +done
   1.795 +
   1.796 +lemma abs_RED[rule_format]: "(\<forall>s\<in>RED \<tau>. t[x::=s]\<in>RED \<sigma>)\<longrightarrow>Lam [x].t\<in>RED (\<tau>\<rightarrow>\<sigma>)"
   1.797 +apply(simp)
   1.798 +apply(clarify)
   1.799 +apply(subgoal_tac "t\<in>termi Beta")(*1*)
   1.800 +apply(erule rev_mp)
   1.801 +apply(subgoal_tac "u \<in> RED \<tau>")(*A*)
   1.802 +apply(erule rev_mp)
   1.803 +apply(rule_tac a="t" and b="u" in double_acc)
   1.804 +apply(assumption)
   1.805 +apply(subgoal_tac "CR1 \<tau>")(*A*)
   1.806 +apply(simp add: CR1_def SN_def)
   1.807 +(*A*)
   1.808 +apply(force simp add: RED_props)
   1.809 +apply(simp)
   1.810 +apply(clarify)
   1.811 +apply(subgoal_tac "CR3 \<sigma>")(*B*)
   1.812 +apply(simp add: CR3_def)
   1.813 +apply(rotate_tac 6)
   1.814 +apply(drule_tac x="App(Lam[x].xa ) z" in spec)
   1.815 +apply(drule mp)
   1.816 +apply(rule conjI)
   1.817 +apply(force simp add: NEUT_def)
   1.818 +apply(simp add: CR3_RED_def)
   1.819 +apply(clarify)
   1.820 +apply(ind_cases "App(Lam[x].xa) z \<longrightarrow>\<^isub>\<beta> t'")
   1.821 +apply(auto simp add: lam.inject lam.distinct)
   1.822 +apply(drule beta_abs)
   1.823 +apply(auto)
   1.824 +apply(drule_tac x="t''" in spec)
   1.825 +apply(simp)
   1.826 +apply(drule mp)
   1.827 +apply(clarify)
   1.828 +apply(drule_tac x="s" in bspec)
   1.829 +apply(assumption)
   1.830 +apply(subgoal_tac "xa [ x ::= s ] \<longrightarrow>\<^isub>\<beta>  t'' [ x ::= s ]")(*B*)
   1.831 +apply(subgoal_tac "CR2 \<sigma>")(*C*)
   1.832 +apply(simp (no_asm_use) add: CR2_def)
   1.833 +apply(blast)
   1.834 +(*C*)
   1.835 +apply(force simp add: RED_props)
   1.836 +(*B*)
   1.837 +apply(force intro!: beta_subst)
   1.838 +apply(assumption)
   1.839 +apply(rotate_tac 3)
   1.840 +apply(drule_tac x="s2" in spec)
   1.841 +apply(subgoal_tac "s2\<in>RED \<tau>")(*D*)
   1.842 +apply(simp)
   1.843 +(*D*)
   1.844 +apply(subgoal_tac "CR2 \<tau>")(*E*)
   1.845 +apply(simp (no_asm_use) add: CR2_def)
   1.846 +apply(blast)
   1.847 +(*E*)
   1.848 +apply(force simp add: RED_props)
   1.849 +apply(simp add: alpha)
   1.850 +apply(erule disjE)
   1.851 +apply(force)
   1.852 +apply(auto)
   1.853 +apply(simp add: subst_rename)
   1.854 +apply(drule_tac x="z" in bspec)
   1.855 +apply(assumption)
   1.856 +(*B*)
   1.857 +apply(force simp add: RED_props)
   1.858 +(*1*)
   1.859 +apply(drule_tac x="Var x" in bspec)
   1.860 +apply(subgoal_tac "CR3 \<tau>")(*2*) 
   1.861 +apply(drule CR3_CR4)
   1.862 +apply(simp add: CR4_def)
   1.863 +apply(drule_tac x="Var x" in spec)
   1.864 +apply(drule mp)
   1.865 +apply(rule conjI)
   1.866 +apply(force simp add: NEUT_def)
   1.867 +apply(simp add: NORMAL_def)
   1.868 +apply(clarify)
   1.869 +apply(ind_cases "Var x \<longrightarrow>\<^isub>\<beta> t'")
   1.870 +apply(auto simp add: lam.inject lam.distinct)
   1.871 +apply(force simp add: RED_props)
   1.872 +apply(simp add: id_subs)
   1.873 +apply(subgoal_tac "CR1 \<sigma>")(*3*)
   1.874 +apply(simp add: CR1_def SN_def)
   1.875 +(*3*)
   1.876 +apply(force simp add: RED_props)
   1.877 +done
   1.878 +
   1.879 +lemma all_RED: 
   1.880 + "((\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>)\<longrightarrow>(a\<in>set(dom_sss \<theta>)\<and>\<theta><a>\<in>RED \<sigma>))\<and>\<Gamma>\<turnstile>t:\<tau>) \<longrightarrow> (t[<\<theta>>]\<in>RED \<tau>)"
   1.881 +apply(nominal_induct t rule: lam_induct)
   1.882 +(* Variables *)
   1.883 +apply(force dest: t1_elim)
   1.884 +(* Applications *)
   1.885 +apply(auto dest!: t2_elim)
   1.886 +apply(drule_tac x="a" in spec)
   1.887 +apply(drule_tac x="a" in spec)
   1.888 +apply(drule_tac x="\<tau>\<rightarrow>aa" in spec)
   1.889 +apply(drule_tac x="\<tau>" in spec)
   1.890 +apply(drule_tac x="b" in spec)
   1.891 +apply(drule_tac x="b" in spec)
   1.892 +apply(force)
   1.893 +(* Abstractions *)
   1.894 +apply(drule t3_elim)
   1.895 +apply(simp add: fresh_prod)
   1.896 +apply(auto)
   1.897 +apply(drule_tac x="((ab,\<tau>)#a)" in spec)
   1.898 +apply(drule_tac x="\<tau>'" in spec)
   1.899 +apply(drule_tac x="b" in spec)
   1.900 +apply(simp)
   1.901 +(* HERE *)
   1.902 +
   1.903 +
   1.904 +done
   1.905 +