src/HOL/Nominal/Examples/SN.thy
author urbanc
Wed Mar 08 18:00:00 2006 +0100 (2006-03-08)
changeset 19218 47b05ebe106b
parent 18659 2ff0ae57431d
child 19496 79dbe35c6cba
permissions -rw-r--r--
deleted some proofs "on comment"
     1 (* $Id$ *)
     2 
     3 theory sn
     4 imports lam_substs  Accessible_Part
     5 begin
     6 
     7 text {* Strong Normalisation proof from the Proofs and Types book *}
     8 
     9 section {* Beta Reduction *}
    10 
    11 lemma subst_rename[rule_format]: 
    12   shows "c\<sharp>t1 \<longrightarrow> (t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2])"
    13 apply(nominal_induct t1 avoiding: a c t2 rule: lam.induct)
    14 apply(auto simp add: calc_atm fresh_atm abs_fresh)
    15 done
    16 
    17 lemma forget: 
    18   assumes a: "a\<sharp>t1"
    19   shows "t1[a::=t2] = t1"
    20   using a
    21 apply (nominal_induct t1 avoiding: a t2 rule: lam.induct)
    22 apply(auto simp add: abs_fresh fresh_atm)
    23 done
    24 
    25 lemma fresh_fact: 
    26   fixes a::"name"
    27   assumes a: "a\<sharp>t1"
    28   and     b: "a\<sharp>t2"
    29   shows "a\<sharp>(t1[b::=t2])"
    30 using a b
    31 apply(nominal_induct t1 avoiding: a b t2 rule: lam.induct)
    32 apply(auto simp add: abs_fresh fresh_atm)
    33 done
    34 
    35 lemma subst_lemma:  
    36   assumes a: "x\<noteq>y"
    37   and     b: "x\<sharp>L"
    38   shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
    39 using a b
    40 by (nominal_induct M avoiding: x y N L rule: lam.induct)
    41    (auto simp add: fresh_fact forget)
    42 
    43 lemma id_subs: "t[x::=Var x] = t"
    44 apply(nominal_induct t avoiding: x rule: lam.induct)
    45 apply(simp_all add: fresh_atm)
    46 done
    47 
    48 consts
    49   Beta :: "(lam\<times>lam) set"
    50 syntax 
    51   "_Beta"       :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
    52   "_Beta_star"  :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80)
    53 translations 
    54   "t1 \<longrightarrow>\<^isub>\<beta> t2" \<rightleftharpoons> "(t1,t2) \<in> Beta"
    55   "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" \<rightleftharpoons> "(t1,t2) \<in> Beta\<^sup>*"
    56 inductive Beta
    57   intros
    58   b1[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App s1 t)\<longrightarrow>\<^isub>\<beta>(App s2 t)"
    59   b2[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App t s1)\<longrightarrow>\<^isub>\<beta>(App t s2)"
    60   b3[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>\<beta> (Lam [(a::name)].s2)"
    61   b4[intro!]: "(App (Lam [(a::name)].s1) s2)\<longrightarrow>\<^isub>\<beta>(s1[a::=s2])"
    62 
    63 lemma eqvt_beta: 
    64   fixes pi :: "name prm"
    65   and   t  :: "lam"
    66   and   s  :: "lam"
    67   assumes a: "t\<longrightarrow>\<^isub>\<beta>s"
    68   shows "(pi\<bullet>t)\<longrightarrow>\<^isub>\<beta>(pi\<bullet>s)"
    69   using a by (induct, auto)
    70 
    71 lemma beta_induct[consumes 1, case_names b1 b2 b3 b4]:
    72   fixes  P :: "'a::fs_name\<Rightarrow>lam \<Rightarrow> lam \<Rightarrow>bool"
    73   and    t :: "lam"
    74   and    s :: "lam"
    75   and    x :: "'a::fs_name"
    76   assumes a: "t\<longrightarrow>\<^isub>\<beta>s"
    77   and a1:    "\<And>t s1 s2 x. s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<And>z. P z s1 s2) \<Longrightarrow> P x (App s1 t) (App s2 t)"
    78   and a2:    "\<And>t s1 s2 x. s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<And>z. P z s1 s2) \<Longrightarrow> P x (App t s1) (App t s2)"
    79   and a3:    "\<And>a s1 s2 x. a\<sharp>x \<Longrightarrow> s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<And>z. P z s1 s2) \<Longrightarrow> P x (Lam [a].s1) (Lam [a].s2)"
    80   and a4:    "\<And>a t1 s1 x. a\<sharp>x \<Longrightarrow> P x (App (Lam [a].t1) s1) (t1[a::=s1])"
    81   shows "P x t s"
    82 proof -
    83   from a have "\<And>(pi::name prm) x. P x (pi\<bullet>t) (pi\<bullet>s)"
    84   proof (induct)
    85     case b1 thus ?case using a1 by (simp, blast intro: eqvt_beta)
    86   next
    87     case b2 thus ?case using a2 by (simp, blast intro: eqvt_beta)
    88   next
    89     case (b3 a s1 s2)
    90     have j1: "s1 \<longrightarrow>\<^isub>\<beta> s2" by fact
    91     have j2: "\<And>x (pi::name prm). P x (pi\<bullet>s1) (pi\<bullet>s2)" by fact
    92     show ?case 
    93     proof (simp)
    94       have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
    95 	by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
    96       then obtain c::"name" 
    97 	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)"
    98 	by (force simp add: fresh_prod fresh_atm)
    99       have x: "P x (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s1)) (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s2))"
   100 	using a3 f2 j1 j2 by (simp, blast intro: eqvt_beta)
   101       have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s1))" using f1 f3
   102 	by (simp add: lam.inject alpha)
   103       have alpha2: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s2))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s2))" using f1 f3
   104 	by (simp add: lam.inject alpha)
   105       show " P x (Lam [(pi\<bullet>a)].(pi\<bullet>s1)) (Lam [(pi\<bullet>a)].(pi\<bullet>s2))"
   106 	using x alpha1 alpha2 by (simp only: pt_name2)
   107     qed
   108   next
   109     case (b4 a s1 s2)
   110     show ?case
   111     proof (simp add: subst_eqvt)
   112       have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
   113 	by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
   114       then obtain c::"name" 
   115 	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)"
   116 	by (force simp add: fresh_prod fresh_atm)
   117       have x: "P x (App (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s1)) (pi\<bullet>s2)) ((([(c,pi\<bullet>a)]@pi)\<bullet>s1)[c::=(pi\<bullet>s2)])"
   118 	using a4 f2 by (blast intro!: eqvt_beta)
   119       have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s1))" using f1 f3
   120 	by (simp add: lam.inject alpha)
   121       have alpha2: "(([(c,pi\<bullet>a)]@pi)\<bullet>s1)[c::=(pi\<bullet>s2)] = (pi\<bullet>s1)[(pi\<bullet>a)::=(pi\<bullet>s2)]"
   122 	using f3 by (simp only: subst_rename[symmetric] pt_name2)
   123       show "P x (App (Lam [(pi\<bullet>a)].(pi\<bullet>s1)) (pi\<bullet>s2)) ((pi\<bullet>s1)[(pi\<bullet>a)::=(pi\<bullet>s2)])"
   124 	using x alpha1 alpha2 by (simp only: pt_name2)
   125     qed
   126   qed
   127   hence "P x (([]::name prm)\<bullet>t) (([]::name prm)\<bullet>s)" by blast 
   128   thus ?thesis by simp
   129 qed
   130 
   131 lemma supp_beta: 
   132   assumes a: "t\<longrightarrow>\<^isub>\<beta> s"
   133   shows "(supp s)\<subseteq>((supp t)::name set)"
   134 using a
   135 by (induct)
   136    (auto intro!: simp add: abs_supp lam.supp subst_supp)
   137 
   138 
   139 lemma beta_abs: "Lam [a].t\<longrightarrow>\<^isub>\<beta> t'\<Longrightarrow>\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>\<beta> t''"
   140 apply(ind_cases "Lam [a].t  \<longrightarrow>\<^isub>\<beta> t'")
   141 apply(auto simp add: lam.distinct lam.inject)
   142 apply(auto simp add: alpha)
   143 apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)
   144 apply(rule conjI)
   145 apply(rule sym)
   146 apply(rule pt_bij2[OF pt_name_inst, OF at_name_inst])
   147 apply(simp)
   148 apply(rule pt_name3)
   149 apply(simp add: at_ds5[OF at_name_inst])
   150 apply(rule conjI)
   151 apply(simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst] calc_atm)
   152 apply(force dest!: supp_beta simp add: fresh_def)
   153 apply(force intro!: eqvt_beta)
   154 done
   155 
   156 lemma beta_subst: 
   157   assumes a: "M \<longrightarrow>\<^isub>\<beta> M'"
   158   shows "M[x::=N]\<longrightarrow>\<^isub>\<beta> M'[x::=N]" 
   159 using a
   160 apply(nominal_induct M M' avoiding: x N rule: beta_induct)
   161 apply(auto simp add: fresh_atm subst_lemma)
   162 done
   163 
   164 section {* types *}
   165 
   166 datatype ty =
   167     TVar "string"
   168   | TArr "ty" "ty" (infix "\<rightarrow>" 200)
   169 
   170 primrec
   171  "pi\<bullet>(TVar s) = TVar s"
   172  "pi\<bullet>(\<tau> \<rightarrow> \<sigma>) = (\<tau> \<rightarrow> \<sigma>)"
   173 
   174 lemma perm_ty[simp]:
   175   fixes pi ::"name prm"
   176   and   \<tau>  ::"ty"
   177   shows "pi\<bullet>\<tau> = \<tau>"
   178   by (cases \<tau>, simp_all)
   179 
   180 lemma fresh_ty:
   181   fixes a ::"name"
   182   and   \<tau>  ::"ty"
   183   shows "a\<sharp>\<tau>"
   184   by (simp add: fresh_def supp_def)
   185 
   186 instance ty :: pt_name
   187 apply(intro_classes)   
   188 apply(simp_all)
   189 done
   190 
   191 instance ty :: fs_name
   192 apply(intro_classes)
   193 apply(simp add: supp_def)
   194 done
   195 
   196 (* valid contexts *)
   197 
   198 consts
   199   "dom_ty" :: "(name\<times>ty) list \<Rightarrow> (name list)"
   200 primrec
   201   "dom_ty []    = []"
   202   "dom_ty (x#\<Gamma>) = (fst x)#(dom_ty \<Gamma>)" 
   203 
   204 consts
   205   ctxts :: "((name\<times>ty) list) set" 
   206   valid :: "(name\<times>ty) list \<Rightarrow> bool"
   207 translations
   208   "valid \<Gamma>" \<rightleftharpoons> "\<Gamma> \<in> ctxts"  
   209 inductive ctxts
   210 intros
   211 v1[intro]: "valid []"
   212 v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)"
   213 
   214 lemma valid_eqvt:
   215   fixes   pi:: "name prm"
   216   assumes a: "valid \<Gamma>"
   217   shows   "valid (pi\<bullet>\<Gamma>)"
   218 using a
   219 apply(induct)
   220 apply(auto simp add: fresh_eqvt)
   221 done
   222 
   223 (* typing judgements *)
   224 
   225 lemma fresh_context[rule_format]: 
   226   fixes  \<Gamma> :: "(name\<times>ty)list"
   227   and    a :: "name"
   228   assumes a: "a\<sharp>\<Gamma>"
   229   shows "\<not>(\<exists>\<tau>::ty. (a,\<tau>)\<in>set \<Gamma>)"
   230 using a
   231 apply(induct \<Gamma>)
   232 apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
   233 done
   234 
   235 lemma valid_elim: 
   236   fixes  \<Gamma> :: "(name\<times>ty)list"
   237   and    pi:: "name prm"
   238   and    a :: "name"
   239   and    \<tau> :: "ty"
   240   shows "valid ((a,\<tau>)#\<Gamma>) \<Longrightarrow> valid \<Gamma> \<and> a\<sharp>\<Gamma>"
   241 apply(ind_cases "valid ((a,\<tau>)#\<Gamma>)", simp)
   242 done
   243 
   244 lemma valid_unicity[rule_format]: 
   245   assumes a: "valid \<Gamma>"
   246   and     b: "(c,\<sigma>)\<in>set \<Gamma>"
   247   and     c: "(c,\<tau>)\<in>set \<Gamma>"
   248   shows "\<sigma>=\<tau>" 
   249 using a b c
   250 apply(induct \<Gamma>)
   251 apply(auto dest!: valid_elim fresh_context)
   252 done
   253 
   254 consts
   255   typing :: "(((name\<times>ty) list)\<times>lam\<times>ty) set" 
   256 syntax
   257   "_typing_judge" :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80) 
   258 translations
   259   "\<Gamma> \<turnstile> t : \<tau>" \<rightleftharpoons> "(\<Gamma>,t,\<tau>) \<in> typing"  
   260 
   261 inductive typing
   262 intros
   263 t1[intro]: "\<lbrakk>valid \<Gamma>; (a,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var a : \<tau>"
   264 t2[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>"
   265 t3[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>"
   266 
   267 lemma eqvt_typing: 
   268   fixes  \<Gamma> :: "(name\<times>ty) list"
   269   and    t :: "lam"
   270   and    \<tau> :: "ty"
   271   and    pi:: "name prm"
   272   assumes a: "\<Gamma> \<turnstile> t : \<tau>"
   273   shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>t) : \<tau>"
   274 using a
   275 proof (induct)
   276   case (t1 \<Gamma> \<tau> a)
   277   have "valid (pi\<bullet>\<Gamma>)" by (rule valid_eqvt)
   278   moreover
   279   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])
   280   ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> ((pi::name prm)\<bullet>Var a) : \<tau>"
   281     using typing.t1 by (force simp add: pt_list_set_pi[OF pt_name_inst, symmetric])
   282 next 
   283   case (t3 \<Gamma> \<sigma> \<tau> a t)
   284   moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_eqvt)
   285   ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) :\<tau>\<rightarrow>\<sigma>" by force 
   286 qed (auto)
   287 
   288 lemma typing_induct[consumes 1, case_names t1 t2 t3]:
   289   fixes  P :: "'a::fs_name\<Rightarrow>(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow>bool"
   290   and    \<Gamma> :: "(name\<times>ty) list"
   291   and    t :: "lam"
   292   and    \<tau> :: "ty"
   293   and    x :: "'a::fs_name"
   294   assumes a: "\<Gamma> \<turnstile> t : \<tau>"
   295   and a1:    "\<And>\<Gamma> (a::name) \<tau> x. valid \<Gamma> \<Longrightarrow> (a,\<tau>) \<in> set \<Gamma> \<Longrightarrow> P x \<Gamma> (Var a) \<tau>"
   296   and a2:    "\<And>\<Gamma> \<tau> \<sigma> t1 t2 x. 
   297               \<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma> \<Longrightarrow> (\<And>z. P z \<Gamma> t1 (\<tau>\<rightarrow>\<sigma>)) \<Longrightarrow> \<Gamma> \<turnstile> t2 : \<tau> \<Longrightarrow> (\<And>z. P z \<Gamma> t2 \<tau>)
   298               \<Longrightarrow> P x \<Gamma> (App t1 t2) \<sigma>"
   299   and a3:    "\<And>a \<Gamma> \<tau> \<sigma> t x. a\<sharp>x \<Longrightarrow> a\<sharp>\<Gamma> \<Longrightarrow> ((a,\<tau>) # \<Gamma>) \<turnstile> t : \<sigma> \<Longrightarrow> (\<And>z. P z ((a,\<tau>)#\<Gamma>) t \<sigma>)
   300               \<Longrightarrow> P x \<Gamma> (Lam [a].t) (\<tau>\<rightarrow>\<sigma>)"
   301   shows "P x \<Gamma> t \<tau>"
   302 proof -
   303   from a have "\<And>(pi::name prm) x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>t) \<tau>"
   304   proof (induct)
   305     case (t1 \<Gamma> \<tau> a)
   306     have j1: "valid \<Gamma>" by fact
   307     have j2: "(a,\<tau>)\<in>set \<Gamma>" by fact
   308     from j1 have j3: "valid (pi\<bullet>\<Gamma>)" by (rule valid_eqvt)
   309     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])  
   310     hence j4: "(pi\<bullet>a,\<tau>)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: pt_list_set_pi[OF pt_name_inst])
   311     show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Var a)) \<tau>" using a1 j3 j4 by simp
   312   next
   313     case (t2 \<Gamma> \<sigma> \<tau> t1 t2)
   314     thus ?case using a2 by (simp, blast intro: eqvt_typing)
   315   next
   316     case (t3 \<Gamma> \<sigma> \<tau> a t)
   317     have k1: "a\<sharp>\<Gamma>" by fact
   318     have k2: "((a,\<tau>)#\<Gamma>)\<turnstile>t:\<sigma>" by fact
   319     have k3: "\<And>(pi::name prm) (x::'a::fs_name). P x (pi \<bullet>((a,\<tau>)#\<Gamma>)) (pi\<bullet>t) \<sigma>" by fact
   320     have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t,pi\<bullet>\<Gamma>,x)"
   321       by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
   322     then obtain c::"name" 
   323       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>)"
   324       by (force simp add: fresh_prod at_fresh[OF at_name_inst])
   325     from k1 have k1a: "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" 
   326       by (simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst] 
   327                     pt_rev_pi[OF pt_name_inst, OF at_name_inst])
   328     have l1: "(([(c,pi\<bullet>a)]@pi)\<bullet>\<Gamma>) = (pi\<bullet>\<Gamma>)" using f4 k1a 
   329       by (simp only: pt2[OF pt_name_inst], rule pt_fresh_fresh[OF pt_name_inst, OF at_name_inst])
   330     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
   331     hence l2: "\<And>x. P x ((c, \<tau>)#(pi\<bullet>\<Gamma>)) (([(c,pi\<bullet>a)]@pi)\<bullet>t) \<sigma>" using f1 l1
   332       by (force simp add: pt2[OF pt_name_inst]  at_calc[OF at_name_inst])
   333     have "(([(c,pi\<bullet>a)]@pi)\<bullet>((a,\<tau>)#\<Gamma>)) \<turnstile> (([(c,pi\<bullet>a)]@pi)\<bullet>t) : \<sigma>" using k2 by (rule eqvt_typing)
   334     hence l3: "((c, \<tau>)#(pi\<bullet>\<Gamma>)) \<turnstile> (([(c,pi\<bullet>a)]@pi)\<bullet>t) : \<sigma>" using l1 f1 
   335       by (force simp add: pt2[OF pt_name_inst]  at_calc[OF at_name_inst])
   336     have l4: "P x (pi\<bullet>\<Gamma>) (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>t)) (\<tau> \<rightarrow> \<sigma>)" using f2 f4 l2 l3 a3 by auto
   337     have alpha: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t))) = (Lam [(pi\<bullet>a)].(pi\<bullet>t))" using f1 f3
   338       by (simp add: lam.inject alpha)
   339     show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Lam [a].t)) (\<tau> \<rightarrow> \<sigma>)" using l4 alpha 
   340       by (simp only: pt2[OF pt_name_inst], simp)
   341   qed
   342   hence "P x (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>t) \<tau>" by blast
   343   thus "P x \<Gamma> t \<tau>" by simp
   344 qed
   345 
   346 constdefs
   347   "sub" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" (" _ \<lless> _ " [80,80] 80)
   348   "\<Gamma>1 \<lless> \<Gamma>2 \<equiv> \<forall>a \<sigma>. (a,\<sigma>)\<in>set \<Gamma>1 \<longrightarrow>  (a,\<sigma>)\<in>set \<Gamma>2"
   349 
   350 lemma weakening: 
   351   assumes a: "\<Gamma>1 \<turnstile> t : \<sigma>" 
   352   and     b: "valid \<Gamma>2" 
   353   and     c: "\<Gamma>1 \<lless> \<Gamma>2"
   354   shows "\<Gamma>2 \<turnstile> t:\<sigma>"
   355 using a b c
   356 apply(nominal_induct \<Gamma>1 t \<sigma> avoiding: \<Gamma>2 rule: typing_induct)
   357 apply(auto simp add: sub_def)
   358 (* FIXME: before using meta-connectives and the new induction *)
   359 (* method, this was completely automatic *)
   360 apply(atomize)
   361 apply(auto)
   362 done
   363 
   364 lemma in_ctxt: 
   365   assumes a: "(a,\<tau>)\<in>set \<Gamma>"
   366   shows "a\<in>set(dom_ty \<Gamma>)"
   367 using a
   368 apply(induct \<Gamma>, auto)
   369 done
   370 
   371 lemma free_vars: 
   372   assumes a: "\<Gamma> \<turnstile> t : \<tau>"
   373   shows " (supp t)\<subseteq>set(dom_ty \<Gamma>)"
   374 using a
   375 apply(nominal_induct \<Gamma> t \<tau> rule: typing_induct)
   376 apply(auto simp add: lam.supp abs_supp supp_atm in_ctxt)
   377 done
   378 
   379 lemma t1_elim: "\<Gamma> \<turnstile> Var a : \<tau> \<Longrightarrow> valid \<Gamma> \<and> (a,\<tau>) \<in> set \<Gamma>"
   380 apply(ind_cases "\<Gamma> \<turnstile> Var a : \<tau>")
   381 apply(auto simp add: lam.inject lam.distinct)
   382 done
   383 
   384 lemma t2_elim: "\<Gamma> \<turnstile> App t1 t2 : \<sigma> \<Longrightarrow> \<exists>\<tau>. (\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma> \<and> \<Gamma> \<turnstile> t2 : \<tau>)"
   385 apply(ind_cases "\<Gamma> \<turnstile> App t1 t2 : \<sigma>")
   386 apply(auto simp add: lam.inject lam.distinct)
   387 done
   388 
   389 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>'"
   390 apply(ind_cases "\<Gamma> \<turnstile> Lam [a].t : \<sigma>")
   391 apply(auto simp add: lam.distinct lam.inject alpha) 
   392 apply(drule_tac pi="[(a,aa)]::name prm" in eqvt_typing)
   393 apply(simp)
   394 apply(subgoal_tac "([(a,aa)]::name prm)\<bullet>\<Gamma> = \<Gamma>")(*A*)
   395 apply(force simp add: calc_atm)
   396 (*A*)
   397 apply(force intro!: pt_fresh_fresh[OF pt_name_inst, OF at_name_inst])
   398 done
   399 
   400 lemma typing_valid: 
   401   assumes a: "\<Gamma> \<turnstile> t : \<tau>" 
   402   shows "valid \<Gamma>"
   403 using a by (induct, auto dest!: valid_elim)
   404 
   405 lemma ty_subs:
   406   assumes a: "((c,\<sigma>)#\<Gamma>) \<turnstile> t1:\<tau>"
   407   and     b: "\<Gamma>\<turnstile> t2:\<sigma>"
   408   shows  "\<Gamma> \<turnstile> t1[c::=t2]:\<tau>"
   409 using a b
   410 proof(nominal_induct t1 avoiding: \<Gamma> \<sigma> \<tau> c t2 rule: lam.induct)
   411   case (Var a) 
   412   have a1: "\<Gamma> \<turnstile>t2:\<sigma>" by fact
   413   have a2: "((c,\<sigma>)#\<Gamma>) \<turnstile> Var a:\<tau>" by fact
   414   hence a21: "(a,\<tau>)\<in>set((c,\<sigma>)#\<Gamma>)" and a22: "valid((c,\<sigma>)#\<Gamma>)" by (auto dest: t1_elim)
   415   from a22 have a23: "valid \<Gamma>" and a24: "c\<sharp>\<Gamma>" by (auto dest: valid_elim) 
   416   from a24 have a25: "\<not>(\<exists>\<tau>. (c,\<tau>)\<in>set \<Gamma>)" by (rule fresh_context)
   417   show "\<Gamma>\<turnstile>(Var a)[c::=t2] : \<tau>"
   418   proof (cases "a=c", simp_all)
   419     assume case1: "a=c"
   420     show "\<Gamma> \<turnstile> t2:\<tau>" using a1
   421     proof (cases "\<sigma>=\<tau>")
   422       assume "\<sigma>=\<tau>" thus ?thesis using a1 by simp 
   423     next
   424       assume a3: "\<sigma>\<noteq>\<tau>"
   425       show ?thesis
   426       proof (rule ccontr)
   427 	from a3 a21 have "(a,\<tau>)\<in>set \<Gamma>" by force
   428 	with case1 a25 show False by force 
   429       qed
   430     qed
   431   next
   432     assume case2: "a\<noteq>c"
   433     with a21 have a26: "(a,\<tau>)\<in>set \<Gamma>" by force 
   434     from a23 a26 show "\<Gamma> \<turnstile> Var a:\<tau>" by force
   435   qed
   436 next
   437   case (App s1 s2)
   438   have ih_s1: "\<And>c \<sigma> \<tau> t2 \<Gamma>. ((c,\<sigma>)#\<Gamma>) \<turnstile> s1:\<tau> \<Longrightarrow> \<Gamma>\<turnstile> t2: \<sigma> \<Longrightarrow> \<Gamma> \<turnstile> s1[c::=t2]:\<tau>" by fact
   439   have ih_s2: "\<And>c \<sigma> \<tau> t2 \<Gamma>. ((c,\<sigma>)#\<Gamma>) \<turnstile> s2:\<tau> \<Longrightarrow> \<Gamma>\<turnstile> t2: \<sigma> \<Longrightarrow> \<Gamma> \<turnstile> s2[c::=t2]:\<tau>" by fact
   440   have "((c,\<sigma>)#\<Gamma>)\<turnstile>App s1 s2 : \<tau>" by fact
   441   hence "\<exists>\<tau>'. ((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau> \<and> ((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>'" by (rule t2_elim) 
   442   then obtain \<tau>' where "((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau>" and "((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>'" by blast
   443   moreover
   444   have "\<Gamma> \<turnstile>t2:\<sigma>" by fact
   445   ultimately show "\<Gamma> \<turnstile>  (App s1 s2)[c::=t2] : \<tau>" using ih_s1 ih_s2 by (simp, blast)
   446 next
   447   case (Lam a s)
   448   have "a\<sharp>\<Gamma>" "a\<sharp>\<sigma>" "a\<sharp>\<tau>" "a\<sharp>c" "a\<sharp>t2" by fact 
   449   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>)"
   450     by (auto simp add: fresh_atm fresh_prod fresh_list_cons)
   451   have c1: "((c,\<sigma>)#\<Gamma>)\<turnstile>Lam [a].s : \<tau>" by fact
   452   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) 
   453   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
   454   from c12 have "valid ((a,\<tau>1)#(c,\<sigma>)#\<Gamma>)" by (rule typing_valid)
   455   hence ca: "valid \<Gamma>" and cb: "a\<sharp>\<Gamma>" and cc: "c\<sharp>\<Gamma>" 
   456     by (auto dest: valid_elim simp add: fresh_list_cons) 
   457   from c12 have c14: "((c,\<sigma>)#(a,\<tau>1)#\<Gamma>) \<turnstile> s : \<tau>2"
   458   proof -
   459     have c2: "((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<lless> ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)" by (force simp add: sub_def)
   460     have c3: "valid ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)"
   461       by (rule v2, rule v2, auto simp add: fresh_list_cons fresh_prod ca cb cc f2' fresh_ty)
   462     from c12 c2 c3 show ?thesis by (force intro: weakening)
   463   qed
   464   assume c8: "\<Gamma> \<turnstile> t2 : \<sigma>"
   465   have c81: "((a,\<tau>1)#\<Gamma>)\<turnstile>t2 :\<sigma>"
   466   proof -
   467     have c82: "\<Gamma> \<lless> ((a,\<tau>1)#\<Gamma>)" by (force simp add: sub_def)
   468     have c83: "valid ((a,\<tau>1)#\<Gamma>)" using f1 ca by force
   469     with c8 c82 c83 show ?thesis by (force intro: weakening)
   470   qed
   471   show "\<Gamma> \<turnstile> (Lam [a].s)[c::=t2] : \<tau>"
   472     using c11 prems c14 c81 f1 by force
   473 qed
   474 
   475 lemma subject: 
   476   assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2"
   477   and     b: "\<Gamma> \<turnstile> t1:\<tau>"
   478   shows "\<Gamma> \<turnstile> t2:\<tau>"
   479 using a b
   480 proof (nominal_induct t1 t2 avoiding: \<Gamma> \<tau> rule: beta_induct)
   481   case (b1 t s1 s2) --"App-case left"
   482   have ih: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1:\<tau> \<Longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact
   483   have "\<Gamma> \<turnstile> App s1 t : \<tau>" by fact 
   484   hence "\<exists>\<sigma>. \<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> t : \<sigma>" by (rule t2_elim)
   485   then obtain \<sigma> where "\<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau>" and "\<Gamma> \<turnstile> t : \<sigma>" by blast
   486   with ih show "\<Gamma> \<turnstile> App s2 t : \<tau>" by blast
   487 next
   488   case (b2 t s1 s2) --"App-case right"
   489   have ih: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact 
   490   have "\<Gamma> \<turnstile> App t s1 : \<tau>" by fact
   491   hence "\<exists>\<sigma>. \<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> s1 : \<sigma>" by (rule t2_elim)
   492   then obtain \<sigma> where "\<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau>" and "\<Gamma> \<turnstile> s1 : \<sigma>" by blast
   493   with ih show "\<Gamma> \<turnstile> App t s2 : \<tau>" by blast
   494 next
   495   case (b3 a s1 s2) --"Lam-case"
   496   have fr: "a\<sharp>\<Gamma>" "a\<sharp>\<tau>" by fact
   497   have ih: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact
   498   have "\<Gamma> \<turnstile> Lam [a].s1 : \<tau>" by fact
   499   with fr have "\<exists>\<tau>1 \<tau>2. \<tau>=\<tau>1\<rightarrow>\<tau>2 \<and> ((a,\<tau>1)#\<Gamma>) \<turnstile> s1 : \<tau>2" by (simp add: t3_elim)
   500   then obtain \<tau>1 \<tau>2 where "\<tau>=\<tau>1\<rightarrow>\<tau>2" and "((a,\<tau>1)#\<Gamma>) \<turnstile> s1 : \<tau>2" by blast
   501   with ih show "\<Gamma> \<turnstile> Lam [a].s2 : \<tau>" using fr by blast
   502 next
   503   case (b4 a s1 s2) --"Beta-redex"
   504   have fr: "a\<sharp>\<Gamma>" by fact
   505   have "\<Gamma> \<turnstile> App (Lam [a].s1) s2 : \<tau>" by fact
   506   hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> (Lam [a].s1) : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> s2 : \<sigma>)" by (simp add: t2_elim)
   507   then obtain \<sigma> where a1: "\<Gamma> \<turnstile> (Lam [a].s1) : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> s2 : \<sigma>" by blast
   508   from a1 have "((a,\<sigma>)#\<Gamma>) \<turnstile> s1 : \<tau>" using fr by (blast dest!: t3_elim)
   509   with a2 show "\<Gamma> \<turnstile> s1[a::=s2] : \<tau>" by (simp add: ty_subs)
   510 qed
   511 
   512 lemma subject_automatic: 
   513   assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2"
   514   and     b: "\<Gamma> \<turnstile> t1:\<tau>"
   515   shows "\<Gamma> \<turnstile> t2:\<tau>"
   516 using a b
   517 apply(nominal_induct t1 t2 avoiding: \<Gamma> \<tau> rule: beta_induct)
   518 apply(auto dest!: t2_elim t3_elim intro: ty_subs)
   519 done
   520 
   521 subsection {* some facts about beta *}
   522 
   523 constdefs
   524   "NORMAL" :: "lam \<Rightarrow> bool"
   525   "NORMAL t \<equiv> \<not>(\<exists>t'. t\<longrightarrow>\<^isub>\<beta> t')"
   526 
   527 lemma NORMAL_Var:
   528   shows "NORMAL (Var a)"
   529 proof -
   530   { assume "\<exists>t'. (Var a) \<longrightarrow>\<^isub>\<beta> t'"
   531     then obtain t' where "(Var a) \<longrightarrow>\<^isub>\<beta> t'" by blast
   532     hence False by (cases, auto) 
   533   }
   534   thus "NORMAL (Var a)" by (force simp add: NORMAL_def)
   535 qed
   536 
   537 constdefs
   538   "SN" :: "lam \<Rightarrow> bool"
   539   "SN t \<equiv> t\<in>termi Beta"
   540 
   541 lemma SN_preserved: "\<lbrakk>SN(t1);t1\<longrightarrow>\<^isub>\<beta> t2\<rbrakk>\<Longrightarrow>SN(t2)"
   542 apply(simp add: SN_def)
   543 apply(drule_tac a="t2" in acc_downward)
   544 apply(auto)
   545 done
   546 
   547 lemma SN_intro: "(\<forall>t2. t1\<longrightarrow>\<^isub>\<beta>t2 \<longrightarrow> SN(t2))\<Longrightarrow>SN(t1)"
   548 apply(simp add: SN_def)
   549 apply(rule accI)
   550 apply(auto)
   551 done
   552 
   553 section {* Candidates *}
   554 
   555 consts
   556   RED :: "ty \<Rightarrow> lam set"
   557 primrec
   558  "RED (TVar X) = {t. SN(t)}"
   559  "RED (\<tau>\<rightarrow>\<sigma>) =   {t. \<forall>u. (u\<in>RED \<tau> \<longrightarrow> (App t u)\<in>RED \<sigma>)}"
   560 
   561 constdefs
   562   NEUT :: "lam \<Rightarrow> bool"
   563   "NEUT t \<equiv> (\<exists>a. t=Var a)\<or>(\<exists>t1 t2. t=App t1 t2)" 
   564 
   565 (* a slight hack to get the first element of applications *)
   566 consts
   567   FST :: "(lam\<times>lam) set"
   568 syntax 
   569   "FST_judge"   :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<guillemotright> _" [80,80] 80)
   570 translations 
   571   "t1 \<guillemotright> t2" \<rightleftharpoons> "(t1,t2) \<in> FST"
   572 inductive FST
   573   intros
   574 fst[intro!]:  "(App t s) \<guillemotright> t"
   575 
   576 lemma fst_elim[elim!]: 
   577   shows "(App t s) \<guillemotright> t' \<Longrightarrow> t=t'"
   578 apply(ind_cases "App t s \<guillemotright> t'")
   579 apply(simp add: lam.inject)
   580 done
   581 
   582 lemma qq3: "SN(App t s)\<Longrightarrow>SN(t)"
   583 apply(simp add: SN_def)
   584 apply(subgoal_tac "\<forall>z. (App t s \<guillemotright> z) \<longrightarrow> z\<in>termi Beta")(*A*)
   585 apply(force)
   586 (*A*)
   587 apply(erule acc_induct)
   588 apply(clarify)
   589 apply(ind_cases "x \<guillemotright> z")
   590 apply(clarify)
   591 apply(rule accI)
   592 apply(auto intro: b1)
   593 done
   594 
   595 section {* Candidates *}
   596 
   597 constdefs
   598   "CR1" :: "ty \<Rightarrow> bool"
   599   "CR1 \<tau> \<equiv> \<forall> t. (t\<in>RED \<tau> \<longrightarrow> SN(t))"
   600 
   601   "CR2" :: "ty \<Rightarrow> bool"
   602   "CR2 \<tau> \<equiv> \<forall>t t'. (t\<in>RED \<tau> \<and> t \<longrightarrow>\<^isub>\<beta> t') \<longrightarrow> t'\<in>RED \<tau>"
   603 
   604   "CR3_RED" :: "lam \<Rightarrow> ty \<Rightarrow> bool"
   605   "CR3_RED t \<tau> \<equiv> \<forall>t'. t\<longrightarrow>\<^isub>\<beta> t' \<longrightarrow>  t'\<in>RED \<tau>" 
   606 
   607   "CR3" :: "ty \<Rightarrow> bool"
   608   "CR3 \<tau> \<equiv> \<forall>t. (NEUT t \<and> CR3_RED t \<tau>) \<longrightarrow> t\<in>RED \<tau>"
   609    
   610   "CR4" :: "ty \<Rightarrow> bool"
   611   "CR4 \<tau> \<equiv> \<forall>t. (NEUT t \<and> NORMAL t) \<longrightarrow>t\<in>RED \<tau>"
   612 
   613 lemma CR3_CR4: "CR3 \<tau> \<Longrightarrow> CR4 \<tau>"
   614 apply(simp (no_asm_use) add: CR3_def CR3_RED_def CR4_def NORMAL_def)
   615 apply(blast)
   616 done
   617 
   618 lemma sub_ind: 
   619   "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>))"
   620 apply(simp add: SN_def)
   621 apply(erule acc_induct)
   622 apply(auto)
   623 apply(simp add: CR3_def)
   624 apply(rotate_tac 5)
   625 apply(drule_tac x="App t x" in spec)
   626 apply(drule mp)
   627 apply(rule conjI)
   628 apply(force simp only: NEUT_def)
   629 apply(simp (no_asm) add: CR3_RED_def)
   630 apply(clarify)
   631 apply(ind_cases "App t x \<longrightarrow>\<^isub>\<beta> t'")
   632 apply(simp_all add: lam.inject)
   633 apply(simp only:  CR3_RED_def)
   634 apply(drule_tac x="s2" in spec)
   635 apply(simp)
   636 apply(drule_tac x="s2" in spec)
   637 apply(simp)
   638 apply(drule mp)
   639 apply(simp (no_asm_use) add: CR2_def)
   640 apply(blast)
   641 apply(drule_tac x="ta" in spec)
   642 apply(force)
   643 apply(auto simp only: NEUT_def lam.inject lam.distinct)
   644 done
   645 
   646 lemma RED_props: 
   647   shows "CR1 \<tau>" and "CR2 \<tau>" and "CR3 \<tau>"
   648 proof (induct \<tau>)
   649   case (TVar a)
   650   { case 1 show "CR1 (TVar a)" by (simp add: CR1_def)
   651   next
   652     case 2 show "CR2 (TVar a)" by (force intro: SN_preserved simp add: CR2_def)
   653   next
   654     case 3 show "CR3 (TVar a)" by (force intro: SN_intro simp add: CR3_def CR3_RED_def)
   655   }
   656 next
   657   case (TArr \<tau>1 \<tau>2)
   658   { case 1
   659     have ih_CR3_\<tau>1: "CR3 \<tau>1" by fact
   660     have ih_CR1_\<tau>2: "CR1 \<tau>2" by fact
   661     show "CR1 (\<tau>1 \<rightarrow> \<tau>2)"
   662     proof (simp add: CR1_def, intro strip)
   663       fix t
   664       assume a: "\<forall>u. u \<in> RED \<tau>1 \<longrightarrow> App t u \<in> RED \<tau>2"
   665       from ih_CR3_\<tau>1 have "CR4 \<tau>1" by (simp add: CR3_CR4) 
   666       moreover
   667       have "NEUT (Var a)" by (force simp add: NEUT_def)
   668       moreover
   669       have "NORMAL (Var a)" by (rule NORMAL_Var)
   670       ultimately have "(Var a)\<in> RED \<tau>1" by (simp add: CR4_def)
   671       with a have "App t (Var a) \<in> RED \<tau>2" by simp
   672       hence "SN (App t (Var a))" using ih_CR1_\<tau>2 by (simp add: CR1_def)
   673       thus "SN(t)" by (rule qq3)
   674     qed
   675   next
   676     case 2
   677     have ih_CR1_\<tau>1: "CR1 \<tau>1" by fact
   678     have ih_CR2_\<tau>2: "CR2 \<tau>2" by fact
   679     show "CR2 (\<tau>1 \<rightarrow> \<tau>2)"
   680     proof (simp add: CR2_def, intro strip)
   681       fix t1 t2 u
   682       assume "(\<forall>u. u \<in> RED \<tau>1 \<longrightarrow> App t1 u \<in> RED \<tau>2) \<and>  t1 \<longrightarrow>\<^isub>\<beta> t2" 
   683 	and  "u \<in> RED \<tau>1"
   684       hence "t1 \<longrightarrow>\<^isub>\<beta> t2" and "App t1 u \<in> RED \<tau>2" by simp_all
   685       thus "App t2 u \<in> RED \<tau>2" using ih_CR2_\<tau>2 by (force simp add: CR2_def)
   686     qed
   687   next
   688     case 3
   689     have ih_CR1_\<tau>1: "CR1 \<tau>1" by fact
   690     have ih_CR2_\<tau>1: "CR2 \<tau>1" by fact
   691     have ih_CR3_\<tau>2: "CR3 \<tau>2" by fact
   692     show "CR3 (\<tau>1 \<rightarrow> \<tau>2)"
   693     proof (simp add: CR3_def, intro strip)
   694       fix t u
   695       assume a1: "u \<in> RED \<tau>1"
   696       assume a2: "NEUT t \<and> CR3_RED t (\<tau>1 \<rightarrow> \<tau>2)"
   697       from a1 have "SN(u)" using ih_CR1_\<tau>1 by (simp add: CR1_def)
   698       hence "u\<in>RED \<tau>1\<longrightarrow>(\<forall>t. (NEUT t\<and>CR2 \<tau>1\<and>CR3 \<tau>2\<and>CR3_RED t (\<tau>1\<rightarrow>\<tau>2))\<longrightarrow>(App t u)\<in>RED \<tau>2)" 
   699 	by (rule sub_ind)
   700       with a1 a2 show "(App t u)\<in>RED \<tau>2" using ih_CR2_\<tau>1 ih_CR3_\<tau>2 by simp
   701     qed
   702   }
   703 qed
   704     
   705 lemma double_acc_aux:
   706   assumes a_acc: "a \<in> acc r"
   707   and b_acc: "b \<in> acc r"
   708   and hyp: "\<And>x z.
   709     (\<And>y. (y, x) \<in> r \<Longrightarrow> y \<in> acc r) \<Longrightarrow>
   710     (\<And>y. (y, x) \<in> r \<Longrightarrow> P y z) \<Longrightarrow>
   711     (\<And>u. (u, z) \<in> r \<Longrightarrow> u \<in> acc r) \<Longrightarrow>
   712     (\<And>u. (u, z) \<in> r \<Longrightarrow> P x u) \<Longrightarrow> P x z"
   713   shows "P a b"
   714 proof -
   715   from a_acc
   716   have r: "\<And>b. b \<in> acc r \<Longrightarrow> P a b"
   717   proof (induct a rule: acc.induct)
   718     case (accI x)
   719     note accI' = accI
   720     have "b \<in> acc r" .
   721     thus ?case
   722     proof (induct b rule: acc.induct)
   723       case (accI y)
   724       show ?case
   725 	apply (rule hyp)
   726 	apply (erule accI')
   727 	apply (erule accI')
   728 	apply (rule acc.accI)
   729 	apply (erule accI)
   730 	apply (erule accI)
   731 	apply (erule accI)
   732 	done
   733     qed
   734   qed
   735   from b_acc show ?thesis by (rule r)
   736 qed
   737 
   738 lemma double_acc:
   739   "\<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"
   740 apply(rule_tac r="r" in double_acc_aux)
   741 apply(assumption)+
   742 apply(blast)
   743 done
   744 
   745 lemma abs_RED: "(\<forall>s\<in>RED \<tau>. t[x::=s]\<in>RED \<sigma>)\<longrightarrow>Lam [x].t\<in>RED (\<tau>\<rightarrow>\<sigma>)"
   746 apply(simp)
   747 apply(clarify)
   748 apply(subgoal_tac "t\<in>termi Beta")(*1*)
   749 apply(erule rev_mp)
   750 apply(subgoal_tac "u \<in> RED \<tau>")(*A*)
   751 apply(erule rev_mp)
   752 apply(rule_tac a="t" and b="u" in double_acc)
   753 apply(assumption)
   754 apply(subgoal_tac "CR1 \<tau>")(*A*)
   755 apply(simp add: CR1_def SN_def)
   756 (*A*)
   757 apply(force simp add: RED_props)
   758 apply(simp)
   759 apply(clarify)
   760 apply(subgoal_tac "CR3 \<sigma>")(*B*)
   761 apply(simp add: CR3_def)
   762 apply(rotate_tac 6)
   763 apply(drule_tac x="App(Lam[x].xa ) z" in spec)
   764 apply(drule mp)
   765 apply(rule conjI)
   766 apply(force simp add: NEUT_def)
   767 apply(simp add: CR3_RED_def)
   768 apply(clarify)
   769 apply(ind_cases "App(Lam[x].xa) z \<longrightarrow>\<^isub>\<beta> t'")
   770 apply(auto simp add: lam.inject lam.distinct)
   771 apply(drule beta_abs)
   772 apply(auto)
   773 apply(drule_tac x="t''" in spec)
   774 apply(simp)
   775 apply(drule mp)
   776 apply(clarify)
   777 apply(drule_tac x="s" in bspec)
   778 apply(assumption)
   779 apply(subgoal_tac "xa [ x ::= s ] \<longrightarrow>\<^isub>\<beta>  t'' [ x ::= s ]")(*B*)
   780 apply(subgoal_tac "CR2 \<sigma>")(*C*)
   781 apply(simp (no_asm_use) add: CR2_def)
   782 apply(blast)
   783 (*C*)
   784 apply(force simp add: RED_props)
   785 (*B*)
   786 apply(force intro!: beta_subst)
   787 apply(assumption)
   788 apply(rotate_tac 3)
   789 apply(drule_tac x="s2" in spec)
   790 apply(subgoal_tac "s2\<in>RED \<tau>")(*D*)
   791 apply(simp)
   792 (*D*)
   793 apply(subgoal_tac "CR2 \<tau>")(*E*)
   794 apply(simp (no_asm_use) add: CR2_def)
   795 apply(blast)
   796 (*E*)
   797 apply(force simp add: RED_props)
   798 apply(simp add: alpha)
   799 apply(erule disjE)
   800 apply(force)
   801 apply(auto)
   802 apply(simp add: subst_rename)
   803 apply(drule_tac x="z" in bspec)
   804 apply(assumption)
   805 (*B*)
   806 apply(force simp add: RED_props)
   807 (*1*)
   808 apply(drule_tac x="Var x" in bspec)
   809 apply(subgoal_tac "CR3 \<tau>")(*2*) 
   810 apply(drule CR3_CR4)
   811 apply(simp add: CR4_def)
   812 apply(drule_tac x="Var x" in spec)
   813 apply(drule mp)
   814 apply(rule conjI)
   815 apply(force simp add: NEUT_def)
   816 apply(simp add: NORMAL_def)
   817 apply(clarify)
   818 apply(ind_cases "Var x \<longrightarrow>\<^isub>\<beta> t'")
   819 apply(auto simp add: lam.inject lam.distinct)
   820 apply(force simp add: RED_props)
   821 apply(simp add: id_subs)
   822 apply(subgoal_tac "CR1 \<sigma>")(*3*)
   823 apply(simp add: CR1_def SN_def)
   824 (*3*)
   825 apply(force simp add: RED_props)
   826 done
   827 
   828 lemma fresh_domain: 
   829   assumes a: "a\<sharp>\<theta>"
   830   shows "a\<notin>set(domain \<theta>)"
   831 using a
   832 apply(induct \<theta>)
   833 apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
   834 done
   835 
   836 lemma fresh_at: 
   837   assumes a: "a\<in>set(domain \<theta>)" 
   838   and     b: "c\<sharp>\<theta>" 
   839   shows "c\<sharp>(\<theta><a>)"
   840 using a b
   841 apply(induct \<theta>)   
   842 apply(auto simp add: fresh_prod fresh_list_cons)
   843 done
   844 
   845 lemma psubst_subst: 
   846   assumes a: "c\<sharp>\<theta>"
   847   shows "(t[<\<theta>>])[c::=s] = t[<((c,s)#\<theta>)>]"
   848 using a
   849 apply(nominal_induct t avoiding: \<theta> c s rule: lam.induct)
   850 apply(auto dest: fresh_domain)
   851 apply(drule fresh_at)
   852 apply(assumption)
   853 apply(rule forget)
   854 apply(assumption)
   855 apply(subgoal_tac "name\<sharp>((c,s)#\<theta>)")(*A*)
   856 apply(simp)
   857 (*A*)
   858 apply(simp add: fresh_list_cons fresh_prod)
   859 done
   860 lemma all_RED: 
   861   assumes a: "\<Gamma>\<turnstile>t:\<tau>"
   862   and     b: "\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>) \<longrightarrow> (a\<in>set(domain \<theta>)\<and>\<theta><a>\<in>RED \<sigma>)" 
   863   shows "t[<\<theta>>]\<in>RED \<tau>"
   864 using a b
   865 proof(nominal_induct t avoiding: \<Gamma> \<tau> \<theta> rule: lam.induct)
   866   case (Lam a t) --"lambda case"
   867   have ih: "\<And>\<Gamma> \<tau> \<theta>. \<Gamma> \<turnstile> t:\<tau> \<Longrightarrow> 
   868                     (\<forall>c \<sigma>. (c,\<sigma>)\<in>set \<Gamma> \<longrightarrow> c\<in>set (domain \<theta>) \<and>  \<theta><c>\<in>RED \<sigma>) 
   869                     \<Longrightarrow> t[<\<theta>>]\<in>RED \<tau>" 
   870   and  \<theta>_cond: "\<forall>c \<sigma>. (c,\<sigma>)\<in>set \<Gamma> \<longrightarrow> c\<in>set (domain \<theta>) \<and>  \<theta><c>\<in>RED \<sigma>" 
   871   and fresh: "a\<sharp>\<Gamma>" "a\<sharp>\<theta>" 
   872   and "\<Gamma> \<turnstile> Lam [a].t:\<tau>" by fact
   873   hence "\<exists>\<tau>1 \<tau>2. \<tau>=\<tau>1\<rightarrow>\<tau>2 \<and> ((a,\<tau>1)#\<Gamma>)\<turnstile>t:\<tau>2" using t3_elim fresh by simp
   874   then obtain \<tau>1 \<tau>2 where \<tau>_inst: "\<tau>=\<tau>1\<rightarrow>\<tau>2" and typing: "((a,\<tau>1)#\<Gamma>)\<turnstile>t:\<tau>2" by blast
   875   from ih have "\<forall>s\<in>RED \<tau>1. t[<\<theta>>][a::=s] \<in> RED \<tau>2" using fresh typing \<theta>_cond
   876     by (force dest: fresh_context simp add: psubst_subst)
   877   hence "(Lam [a].(t[<\<theta>>])) \<in> RED (\<tau>1 \<rightarrow> \<tau>2)" by (simp only: abs_RED)
   878   thus "(Lam [a].t)[<\<theta>>] \<in> RED \<tau>" using fresh \<tau>_inst by simp
   879 qed (force dest!: t1_elim t2_elim)+
   880 
   881 
   882 lemma all_RED: 
   883   assumes a: "\<Gamma>\<turnstile>t:\<tau>"
   884   and     b: "\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>) \<longrightarrow> (a\<in>set(domain \<theta>)\<and>\<theta><a>\<in>RED \<sigma>)" 
   885   shows "t[<\<theta>>]\<in>RED \<tau>"
   886 using a b
   887 proof(nominal_induct t avoiding: \<Gamma> \<tau> \<theta> rule: lam.induct)
   888   case (Lam a t) --"lambda case"
   889   have ih: "\<And>\<Gamma> \<tau> \<theta>. \<lbrakk>\<Gamma> \<turnstile> t:\<tau>; \<forall>c \<sigma>. (c,\<sigma>)\<in>set \<Gamma> \<longrightarrow> c\<in>set (domain \<theta>) \<and>  \<theta><c>\<in>RED \<sigma>\<rbrakk> 
   890                     \<Longrightarrow> t[<\<theta>>]\<in>RED \<tau>" 
   891   and  \<theta>_cond: "\<forall>c \<sigma>. (c,\<sigma>)\<in>set \<Gamma> \<longrightarrow> c\<in>set (domain \<theta>) \<and>  \<theta><c>\<in>RED \<sigma>" 
   892   and fresh: "a\<sharp>\<Gamma>" "a\<sharp>\<theta>" 
   893   and "\<Gamma> \<turnstile> Lam [a].t:\<tau>" by fact
   894   hence "\<exists>\<tau>1 \<tau>2. \<tau>=\<tau>1\<rightarrow>\<tau>2 \<and> ((a,\<tau>1)#\<Gamma>)\<turnstile>t:\<tau>2" using t3_elim fresh by simp
   895   then obtain \<tau>1 \<tau>2 where \<tau>_inst: "\<tau>=\<tau>1\<rightarrow>\<tau>2" and typing: "((a,\<tau>1)#\<Gamma>)\<turnstile>t:\<tau>2" by blast
   896   from ih have "\<forall>s\<in>RED \<tau>1. t[<\<theta>>][a::=s] \<in> RED \<tau>2" using fresh typing \<theta>_cond
   897     by (force dest: fresh_context simp add: psubst_subst)
   898   hence "(Lam [a].(t[<\<theta>>])) \<in> RED (\<tau>1 \<rightarrow> \<tau>2)" by (simp only: abs_RED)
   899   thus "(Lam [a].t)[<\<theta>>] \<in> RED \<tau>" using fresh \<tau>_inst by simp
   900 qed (force dest!: t1_elim t2_elim)+
   901 
   902 (* identity substitution generated from a context \<Gamma> *)
   903 consts
   904   "id" :: "(name\<times>ty) list \<Rightarrow> (name\<times>lam) list"
   905 primrec
   906   "id []    = []"
   907   "id (x#\<Gamma>) = ((fst x),Var (fst x))#(id \<Gamma>)"
   908 
   909 lemma id_var:
   910   assumes a: "a \<in> set (domain (id \<Gamma>))"
   911   shows "(id \<Gamma>)<a> = Var a"
   912 using a
   913 apply(induct \<Gamma>, auto)
   914 done
   915 
   916 lemma id_fresh:
   917   fixes a::"name"
   918   assumes a: "a\<sharp>\<Gamma>"
   919   shows "a\<sharp>(id \<Gamma>)"
   920 using a
   921 apply(induct \<Gamma>)
   922 apply(auto simp add: fresh_list_nil fresh_list_cons fresh_prod)
   923 done
   924 
   925 lemma id_apply:  
   926   shows "t[<(id \<Gamma>)>] = t"
   927 apply(nominal_induct t avoiding: \<Gamma> rule: lam.induct)
   928 apply(auto)
   929 apply(simp add: id_var)
   930 apply(drule id_fresh)+
   931 apply(simp)
   932 done
   933 
   934 lemma id_mem:
   935   assumes a: "(a,\<tau>)\<in>set \<Gamma>"
   936   shows "a \<in> set (domain (id \<Gamma>))"
   937 using a
   938 apply(induct \<Gamma>, auto)
   939 done
   940 
   941 lemma id_prop:
   942   shows "\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>) \<longrightarrow> (a\<in>set(domain (id \<Gamma>))\<and>(id \<Gamma>)<a>\<in>RED \<sigma>)"
   943 apply(auto)
   944 apply(simp add: id_mem)
   945 apply(frule id_mem)
   946 apply(simp add: id_var)
   947 apply(subgoal_tac "CR3 \<sigma>")(*A*)
   948 apply(drule CR3_CR4)
   949 apply(simp add: CR4_def)
   950 apply(drule_tac x="Var a" in spec)
   951 apply(force simp add: NEUT_def NORMAL_Var)
   952 (*A*)
   953 apply(rule RED_props)
   954 done
   955 
   956 lemma typing_implies_RED:  
   957   assumes a: "\<Gamma>\<turnstile>t:\<tau>"
   958   shows "t \<in> RED \<tau>"
   959 proof -
   960   have "t[<id \<Gamma>>]\<in>RED \<tau>" 
   961   proof -
   962     have "\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>) \<longrightarrow> (a\<in>set(domain (id \<Gamma>))\<and>(id \<Gamma>)<a>\<in>RED \<sigma>)" by (rule id_prop)
   963     with a show ?thesis by (rule all_RED)
   964   qed
   965   thus"t \<in> RED \<tau>" by (simp add: id_apply)
   966 qed
   967 
   968 lemma typing_implies_SN: 
   969   assumes a: "\<Gamma>\<turnstile>t:\<tau>"
   970   shows "SN(t)"
   971 proof -
   972   from a have "t \<in> RED \<tau>" by (rule typing_implies_RED)
   973   moreover
   974   have "CR1 \<tau>" by (rule RED_props)
   975   ultimately show "SN(t)" by (simp add: CR1_def)
   976 qed
   977 
   978 end