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