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