<commit_before>(* $Id$ *)

theory SN
imports Lam_Funs
begin

text {* Strong Normalisation proof from the Proofs and Types book *}

section {* Beta Reduction *}

lemma subst_rename: 
  assumes a: "c\<sharp>t1"
  shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]"
using a
by (nominal_induct t1 avoiding: a c t2 rule: lam.induct)
   (auto simp add: calc_atm fresh_atm abs_fresh)

lemma forget: 
  assumes a: "a\<sharp>t1"
  shows "t1[a::=t2] = t1"
  using a
by (nominal_induct t1 avoiding: a t2 rule: lam.induct)
   (auto simp add: abs_fresh fresh_atm)

lemma fresh_fact: 
  fixes a::"name"
  assumes a: "a\<sharp>t1"
  and     b: "a\<sharp>t2"
  shows "a\<sharp>(t1[b::=t2])"
using a b
by (nominal_induct t1 avoiding: a b t2 rule: lam.induct)
   (auto simp add: abs_fresh fresh_atm)

lemma subst_lemma:  
  assumes a: "x\<noteq>y"
  and     b: "x\<sharp>L"
  shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
using a b
by (nominal_induct M avoiding: x y N L rule: lam.induct)
   (auto simp add: fresh_fact forget)

lemma id_subs: 
  shows "t[x::=Var x] = t"
  by (nominal_induct t avoiding: x rule: lam.induct)
     (simp_all add: fresh_atm)

lemma subst_eqvt[eqvt]:
  fixes pi::"name prm" 
  and   t::"lam"
  shows "pi\<bullet>(t[x::=t']) = (pi\<bullet>t)[(pi\<bullet>x)::=(pi\<bullet>t')]"
by (nominal_induct t avoiding: x t' rule: lam.induct)
   (perm_simp add: fresh_bij)+

inductive2 Beta :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
where
  b1[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App s1 t)\<longrightarrow>\<^isub>\<beta>(App s2 t)"
| b2[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App t s1)\<longrightarrow>\<^isub>\<beta>(App t s2)"
| b3[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>\<beta> (Lam [(a::name)].s2)"
| b4[intro!]: "(App (Lam [(a::name)].s1) s2)\<longrightarrow>\<^isub>\<beta>(s1[a::=s2])"

abbreviation "Beta_star"  :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80) where
  "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2 \<equiv> Beta\<^sup>*\<^sup>* t1 t2"

nominal_inductive Beta
 
lemma beta_induct[consumes 1, case_names b1 b2 b3 b4]:
  fixes  P :: "'a::fs_name\<Rightarrow>lam \<Rightarrow> lam \<Rightarrow>bool"
  and    t :: "lam"
  and    s :: "lam"
  and    x :: "'a::fs_name"
  assumes a: "t\<longrightarrow>\<^isub>\<beta>s"
  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)"
  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)"
  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)"
  and a4:    "\<And>a t1 s1 x. a\<sharp>x \<Longrightarrow> P x (App (Lam [a].t1) s1) (t1[a::=s1])"
  shows "P x t s"
proof -
  from a have "\<And>(pi::name prm) x. P x (pi\<bullet>t) (pi\<bullet>s)"
  proof (induct)
    case b1 thus ?case using a1 by (simp, blast intro: eqvt)
  next
    case b2 thus ?case using a2 by (simp, blast intro: eqvt)
  next
    case (b3 s1 s2 a)
    have j1: "s1 \<longrightarrow>\<^isub>\<beta> s2" by fact
    have j2: "\<And>x (pi::name prm). P x (pi\<bullet>s1) (pi\<bullet>s2)" by fact
    show ?case 
    proof (simp)
      have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
	by (rule exists_fresh', simp add: fs_name1)
      then obtain c::"name" 
	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)"
	by (force simp add: fresh_prod fresh_atm)
      have x: "P x (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s1)) (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s2))"
	using a3 f2 j1 j2 by (simp, blast intro: eqvt)
      have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s1))" using f1 f3
	by (simp add: lam.inject alpha)
      have alpha2: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s2))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s2))" using f1 f3
	by (simp add: lam.inject alpha)
      show " P x (Lam [(pi\<bullet>a)].(pi\<bullet>s1)) (Lam [(pi\<bullet>a)].(pi\<bullet>s2))"
	using x alpha1 alpha2 by (simp only: pt_name2)
    qed
  next
    case (b4 a s1 s2)
    show ?case
    proof (simp add: subst_eqvt)
      have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
	by (rule exists_fresh', simp add: fs_name1)
      then obtain c::"name" 
	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)"
	by (force simp add: fresh_prod fresh_atm)
      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)])"
	using a4 f2 by (blast intro!: eqvt)
      have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s1))" using f1 f3
	by (simp add: lam.inject alpha)
      have alpha2: "(([(c,pi\<bullet>a)]@pi)\<bullet>s1)[c::=(pi\<bullet>s2)] = (pi\<bullet>s1)[(pi\<bullet>a)::=(pi\<bullet>s2)]"
	using f3 by (simp only: subst_rename[symmetric] pt_name2)
      show "P x (App (Lam [(pi\<bullet>a)].(pi\<bullet>s1)) (pi\<bullet>s2)) ((pi\<bullet>s1)[(pi\<bullet>a)::=(pi\<bullet>s2)])"
	using x alpha1 alpha2 by (simp only: pt_name2)
    qed
  qed
  hence "P x (([]::name prm)\<bullet>t) (([]::name prm)\<bullet>s)" by blast 
  thus ?thesis by simp
qed

lemma supp_beta: 
  assumes a: "t\<longrightarrow>\<^isub>\<beta> s"
  shows "(supp s)\<subseteq>((supp t)::name set)"
using a
by (induct)
   (auto intro!: simp add: abs_supp lam.supp subst_supp)


lemma beta_abs: "Lam [a].t\<longrightarrow>\<^isub>\<beta> t'\<Longrightarrow>\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>\<beta> t''"
apply(ind_cases2 "Lam [a].t  \<longrightarrow>\<^isub>\<beta> t'")
apply(auto simp add: lam.distinct lam.inject)
apply(auto simp add: alpha)
apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)
apply(rule conjI)
apply(rule sym)
apply(rule pt_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp)
apply(rule pt_name3)
apply(simp add: at_ds5[OF at_name_inst])
apply(rule conjI)
apply(simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst] calc_atm)
apply(force dest!: supp_beta simp add: fresh_def)
apply(force intro!: eqvt)
done

lemma beta_subst: 
  assumes a: "M \<longrightarrow>\<^isub>\<beta> M'"
  shows "M[x::=N]\<longrightarrow>\<^isub>\<beta> M'[x::=N]" 
using a
apply(nominal_induct M M' avoiding: x N rule: beta_induct)
apply(auto simp add: fresh_atm subst_lemma)
done

section {* types *}

nominal_datatype ty =
    TVar "nat"
  | TArr "ty" "ty" (infix "\<rightarrow>" 200)

lemma perm_ty[simp]:
  fixes pi ::"name prm"
  and   \<tau>  ::"ty"
  shows "pi\<bullet>\<tau> = \<tau>"
by (nominal_induct \<tau> rule: ty.induct) 
   (simp_all add: perm_nat_def)

lemma fresh_ty:
  fixes a ::"name"
  and   \<tau>  ::"ty"
  shows "a\<sharp>\<tau>"
  by (simp add: fresh_def supp_def)

(* valid contexts *)

consts
  "dom_ty" :: "(name\<times>ty) list \<Rightarrow> (name list)"
primrec
  "dom_ty []    = []"
  "dom_ty (x#\<Gamma>) = (fst x)#(dom_ty \<Gamma>)" 

inductive2 valid :: "(name\<times>ty) list \<Rightarrow> bool"
where
  v1[intro]: "valid []"
| v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)"

nominal_inductive valid

(* typing judgements *)

lemma fresh_context: 
  fixes  \<Gamma> :: "(name\<times>ty)list"
  and    a :: "name"
  assumes a: "a\<sharp>\<Gamma>"
  shows "\<not>(\<exists>\<tau>::ty. (a,\<tau>)\<in>set \<Gamma>)"
using a
apply(induct \<Gamma>)
apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
done

inductive_cases2 valid_elim[elim]: "valid ((a,\<tau>)#\<Gamma>)"

lemma valid_unicity: 
  assumes a: "valid \<Gamma>"
  and     b: "(c,\<sigma>)\<in>set \<Gamma>"
  and     c: "(c,\<tau>)\<in>set \<Gamma>"
  shows "\<sigma>=\<tau>" 
using a b c
by (induct \<Gamma>) (auto dest!: fresh_context)

inductive2 typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80)
where
  t1[intro]: "\<lbrakk>valid \<Gamma>; (a,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var a : \<tau>"
| t2[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>"
| t3[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>"

lemma eqvt_typing: 
  fixes  \<Gamma> :: "(name\<times>ty) list"
  and    t :: "lam"
  and    \<tau> :: "ty"
  and    pi:: "name prm"
  assumes a: "\<Gamma> \<turnstile> t : \<tau>"
  shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>t) : \<tau>"
using a
proof (induct)
  case (t1 \<Gamma> a \<tau>)
  have "valid (pi\<bullet>\<Gamma>)" by (rule valid_eqvt)
  moreover
  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])
  ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> ((pi::name prm)\<bullet>Var a) : \<tau>"
    using typing.t1 by (force simp add: set_eqvt[symmetric])
next 
  case (t3 a \<Gamma> \<tau> t \<sigma>)
  moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_bij)
  ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) :\<tau>\<rightarrow>\<sigma>" by force 
qed (auto)

lemma typing_induct[consumes 1, case_names t1 t2 t3]:
  fixes  P :: "'a::fs_name\<Rightarrow>(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow>bool"
  and    \<Gamma> :: "(name\<times>ty) list"
  and    t :: "lam"
  and    \<tau> :: "ty"
  and    x :: "'a::fs_name"
  assumes a: "\<Gamma> \<turnstile> t : \<tau>"
  and a1:    "\<And>\<Gamma> (a::name) \<tau> x. valid \<Gamma> \<Longrightarrow> (a,\<tau>) \<in> set \<Gamma> \<Longrightarrow> P x \<Gamma> (Var a) \<tau>"
  and a2:    "\<And>\<Gamma> \<tau> \<sigma> t1 t2 x. 
              \<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>)
              \<Longrightarrow> P x \<Gamma> (App t1 t2) \<sigma>"
  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>)
              \<Longrightarrow> P x \<Gamma> (Lam [a].t) (\<tau>\<rightarrow>\<sigma>)"
  shows "P x \<Gamma> t \<tau>"
proof -
  from a have "\<And>(pi::name prm) x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>t) \<tau>"
  proof (induct)
    case (t1 \<Gamma> a \<tau>)
    have j1: "valid \<Gamma>" by fact
    have j2: "(a,\<tau>)\<in>set \<Gamma>" by fact
    from j1 have j3: "valid (pi\<bullet>\<Gamma>)" by (rule valid_eqvt)
    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])  
    hence j4: "(pi\<bullet>a,\<tau>)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: eqvt)
    show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Var a)) \<tau>" using a1 j3 j4 by simp
  next
    case (t2 \<Gamma> t1 \<tau> \<sigma> t2)
    thus ?case using a2 by (simp, blast intro: eqvt_typing)
  next
    case (t3 a \<Gamma> \<tau> t \<sigma>)
    have k1: "a\<sharp>\<Gamma>" by fact
    have k2: "((a,\<tau>)#\<Gamma>)\<turnstile>t:\<sigma>" by fact
    have k3: "\<And>(pi::name prm) (x::'a::fs_name). P x (pi \<bullet>((a,\<tau>)#\<Gamma>)) (pi\<bullet>t) \<sigma>" by fact
    have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t,pi\<bullet>\<Gamma>,x)"
      by (rule exists_fresh', simp add: fs_name1)
    then obtain c::"name" 
      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>)"
      by (force simp add: fresh_prod at_fresh[OF at_name_inst])
    from k1 have k1a: "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" 
      by (simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst] 
                    pt_rev_pi[OF pt_name_inst, OF at_name_inst])
    have l1: "(([(c,pi\<bullet>a)]@pi)\<bullet>\<Gamma>) = (pi\<bullet>\<Gamma>)" using f4 k1a 
      by (simp only: pt2[OF pt_name_inst], rule pt_fresh_fresh[OF pt_name_inst, OF at_name_inst])
    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
    hence l2: "\<And>x. P x ((c, \<tau>)#(pi\<bullet>\<Gamma>)) (([(c,pi\<bullet>a)]@pi)\<bullet>t) \<sigma>" using f1 l1
      by (force simp add: pt2[OF pt_name_inst]  at_calc[OF at_name_inst])
    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)
    hence l3: "((c, \<tau>)#(pi\<bullet>\<Gamma>)) \<turnstile> (([(c,pi\<bullet>a)]@pi)\<bullet>t) : \<sigma>" using l1 f1 
      by (force simp add: pt2[OF pt_name_inst]  at_calc[OF at_name_inst])
    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
    have alpha: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t))) = (Lam [(pi\<bullet>a)].(pi\<bullet>t))" using f1 f3
      by (simp add: lam.inject alpha)
    show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Lam [a].t)) (\<tau> \<rightarrow> \<sigma>)" using l4 alpha 
      by (simp only: pt2[OF pt_name_inst], simp)
  qed
  hence "P x (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>t) \<tau>" by blast
  thus "P x \<Gamma> t \<tau>" by simp
qed

abbreviation
  "sub" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" (" _ \<lless> _ " [80,80] 80) where
  "\<Gamma>1 \<lless> \<Gamma>2 \<equiv> \<forall>a \<sigma>. (a,\<sigma>)\<in>set \<Gamma>1 \<longrightarrow>  (a,\<sigma>)\<in>set \<Gamma>2"

lemma weakening: 
  assumes a: "\<Gamma>1 \<turnstile> t : \<sigma>" 
  and     b: "valid \<Gamma>2" 
  and     c: "\<Gamma>1 \<lless> \<Gamma>2"
  shows "\<Gamma>2 \<turnstile> t:\<sigma>"
using a b c
apply(nominal_induct \<Gamma>1 t \<sigma> avoiding: \<Gamma>2 rule: typing_induct)
apply(auto | atomize)+
(* FIXME: before using meta-connectives and the new induction *)
(* method, this was completely automatic *)
done

lemma in_ctxt: 
  assumes a: "(a,\<tau>)\<in>set \<Gamma>"
  shows "a\<in>set(dom_ty \<Gamma>)"
using a
by (induct \<Gamma>) (auto)

lemma free_vars: 
  assumes a: "\<Gamma> \<turnstile> t : \<tau>"
  shows " (supp t)\<subseteq>set(dom_ty \<Gamma>)"
using a
by (nominal_induct \<Gamma> t \<tau> rule: typing_induct)
   (auto simp add: lam.supp abs_supp supp_atm in_ctxt)

lemma t1_elim: "\<Gamma> \<turnstile> Var a : \<tau> \<Longrightarrow> valid \<Gamma> \<and> (a,\<tau>) \<in> set \<Gamma>"
apply(ind_cases2 "\<Gamma> \<turnstile> Var a : \<tau>")
apply(auto simp add: lam.inject lam.distinct)
done

lemma t2_elim: "\<Gamma> \<turnstile> App t1 t2 : \<sigma> \<Longrightarrow> \<exists>\<tau>. (\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma> \<and> \<Gamma> \<turnstile> t2 : \<tau>)"
apply(ind_cases2 "\<Gamma> \<turnstile> App t1 t2 : \<sigma>")
apply(auto simp add: lam.inject lam.distinct)
done

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>'"
apply(ind_cases2 "\<Gamma> \<turnstile> Lam [a].t : \<sigma>")
apply(auto simp add: lam.distinct lam.inject alpha) 
apply(drule_tac pi="[(a,aa)]::name prm" in eqvt_typing)
apply(simp)
apply(subgoal_tac "([(a,aa)]::name prm)\<bullet>\<Gamma> = \<Gamma>")(*A*)
apply(force simp add: calc_atm)
(*A*)
apply(force intro!: pt_fresh_fresh[OF pt_name_inst, OF at_name_inst])
done

lemma typing_valid: 
  assumes a: "\<Gamma> \<turnstile> t : \<tau>" 
  shows "valid \<Gamma>"
using a by (induct, auto)

lemma ty_subs:
  assumes a: "((c,\<sigma>)#\<Gamma>) \<turnstile> t1:\<tau>"
  and     b: "\<Gamma>\<turnstile> t2:\<sigma>"
  shows  "\<Gamma> \<turnstile> t1[c::=t2]:\<tau>"
using a b
proof(nominal_induct t1 avoiding: \<Gamma> \<sigma> \<tau> c t2 rule: lam.induct)
  case (Var a) 
  have a1: "\<Gamma> \<turnstile>t2:\<sigma>" by fact
  have a2: "((c,\<sigma>)#\<Gamma>) \<turnstile> Var a:\<tau>" by fact
  hence a21: "(a,\<tau>)\<in>set((c,\<sigma>)#\<Gamma>)" and a22: "valid((c,\<sigma>)#\<Gamma>)" by (auto dest: t1_elim)
  from a22 have a23: "valid \<Gamma>" and a24: "c\<sharp>\<Gamma>" by (auto dest: valid_elim) 
  from a24 have a25: "\<not>(\<exists>\<tau>. (c,\<tau>)\<in>set \<Gamma>)" by (rule fresh_context)
  show "\<Gamma>\<turnstile>(Var a)[c::=t2] : \<tau>"
  proof (cases "a=c", simp_all)
    assume case1: "a=c"
    show "\<Gamma> \<turnstile> t2:\<tau>" using a1
    proof (cases "\<sigma>=\<tau>")
      assume "\<sigma>=\<tau>" thus ?thesis using a1 by simp 
    next
      assume a3: "\<sigma>\<noteq>\<tau>"
      show ?thesis
      proof (rule ccontr)
	from a3 a21 have "(a,\<tau>)\<in>set \<Gamma>" by force
	with case1 a25 show False by force 
      qed
    qed
  next
    assume case2: "a\<noteq>c"
    with a21 have a26: "(a,\<tau>)\<in>set \<Gamma>" by force 
    from a23 a26 show "\<Gamma> \<turnstile> Var a:\<tau>" by force
  qed
next
  case (App s1 s2)
  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
  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
  have "((c,\<sigma>)#\<Gamma>)\<turnstile>App s1 s2 : \<tau>" by fact
  hence "\<exists>\<tau>'. ((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau> \<and> ((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>'" by (rule t2_elim) 
  then obtain \<tau>' where "((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau>" and "((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>'" by blast
  moreover
  have "\<Gamma> \<turnstile>t2:\<sigma>" by fact
  ultimately show "\<Gamma> \<turnstile>  (App s1 s2)[c::=t2] : \<tau>" using ih_s1 ih_s2 by (simp, blast)
next
  case (Lam a s)
  have "a\<sharp>\<Gamma>" "a\<sharp>\<sigma>" "a\<sharp>\<tau>" "a\<sharp>c" "a\<sharp>t2" by fact 
  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>)"
    by (auto simp add: fresh_atm fresh_prod fresh_list_cons)
  have c1: "((c,\<sigma>)#\<Gamma>)\<turnstile>Lam [a].s : \<tau>" by fact
  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) 
  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
  from c12 have "valid ((a,\<tau>1)#(c,\<sigma>)#\<Gamma>)" by (rule typing_valid)
  hence ca: "valid \<Gamma>" and cb: "a\<sharp>\<Gamma>" and cc: "c\<sharp>\<Gamma>" 
    by (auto simp add: fresh_list_cons) 
  from c12 have c14: "((c,\<sigma>)#(a,\<tau>1)#\<Gamma>) \<turnstile> s : \<tau>2"
  proof -
    have c2: "((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<lless> ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)" by force
    have c3: "valid ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)"
      by (rule v2, rule v2, auto simp add: fresh_list_cons fresh_prod ca cb cc f2' fresh_ty)
    from c12 c2 c3 show ?thesis by (force intro: weakening)
  qed
  assume c8: "\<Gamma> \<turnstile> t2 : \<sigma>"
  have c81: "((a,\<tau>1)#\<Gamma>)\<turnstile>t2 :\<sigma>"
  proof -
    have c82: "\<Gamma> \<lless> ((a,\<tau>1)#\<Gamma>)" by force
    have c83: "valid ((a,\<tau>1)#\<Gamma>)" using f1 ca by force
    with c8 c82 c83 show ?thesis by (force intro: weakening)
  qed
  show "\<Gamma> \<turnstile> (Lam [a].s)[c::=t2] : \<tau>"
    using c11 prems c14 c81 f1 by force
qed

lemma subject: 
  assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2"
  and     b: "\<Gamma> \<turnstile> t1:\<tau>"
  shows "\<Gamma> \<turnstile> t2:\<tau>"
using a b
proof (nominal_induct t1 t2 avoiding: \<Gamma> \<tau> rule: beta_induct)
  case (b1 t s1 s2) --"App-case left"
  have ih: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1:\<tau> \<Longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact
  have "\<Gamma> \<turnstile> App s1 t : \<tau>" by fact 
  hence "\<exists>\<sigma>. \<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> t : \<sigma>" by (rule t2_elim)
  then obtain \<sigma> where "\<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau>" and "\<Gamma> \<turnstile> t : \<sigma>" by blast
  with ih show "\<Gamma> \<turnstile> App s2 t : \<tau>" by blast
next
  case (b2 t s1 s2) --"App-case right"
  have ih: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact 
  have "\<Gamma> \<turnstile> App t s1 : \<tau>" by fact
  hence "\<exists>\<sigma>. \<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> s1 : \<sigma>" by (rule t2_elim)
  then obtain \<sigma> where "\<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau>" and "\<Gamma> \<turnstile> s1 : \<sigma>" by blast
  with ih show "\<Gamma> \<turnstile> App t s2 : \<tau>" by blast
next
  case (b3 a s1 s2) --"Lam-case"
  have fr: "a\<sharp>\<Gamma>" "a\<sharp>\<tau>" by fact
  have ih: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact
  have "\<Gamma> \<turnstile> Lam [a].s1 : \<tau>" by fact
  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)
  then obtain \<tau>1 \<tau>2 where "\<tau>=\<tau>1\<rightarrow>\<tau>2" and "((a,\<tau>1)#\<Gamma>) \<turnstile> s1 : \<tau>2" by blast
  with ih show "\<Gamma> \<turnstile> Lam [a].s2 : \<tau>" using fr by blast
next
  case (b4 a s1 s2) --"Beta-redex"
  have fr: "a\<sharp>\<Gamma>" by fact
  have "\<Gamma> \<turnstile> App (Lam [a].s1) s2 : \<tau>" by fact
  hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> (Lam [a].s1) : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> s2 : \<sigma>)" by (simp add: t2_elim)
  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> (Lam [a].s1) : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> s2 : \<sigma>" by blast
  from a1 have "((a,\<sigma>)#\<Gamma>) \<turnstile> s1 : \<tau>" using fr by (auto dest!: t3_elim simp add: ty.inject) 
  with a2 show "\<Gamma> \<turnstile> s1[a::=s2] : \<tau>" by (simp add: ty_subs)
qed

lemma subject_automatic: 
  assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2"
  and     b: "\<Gamma> \<turnstile> t1:\<tau>"
  shows "\<Gamma> \<turnstile> t2:\<tau>"
using a b
apply(nominal_induct t1 t2 avoiding: \<Gamma> \<tau> rule: beta_induct)
apply(auto dest!: t2_elim t3_elim intro: ty_subs simp add: ty.inject)
done

subsection {* some facts about beta *}

constdefs
  "NORMAL" :: "lam \<Rightarrow> bool"
  "NORMAL t \<equiv> \<not>(\<exists>t'. t\<longrightarrow>\<^isub>\<beta> t')"

lemma NORMAL_Var:
  shows "NORMAL (Var a)"
proof -
  { assume "\<exists>t'. (Var a) \<longrightarrow>\<^isub>\<beta> t'"
    then obtain t' where "(Var a) \<longrightarrow>\<^isub>\<beta> t'" by blast
    hence False by (cases, auto) 
  }
  thus "NORMAL (Var a)" by (force simp add: NORMAL_def)
qed

constdefs
  "SN" :: "lam \<Rightarrow> bool"
  "SN t \<equiv> termi Beta t"

lemma SN_preserved: "\<lbrakk>SN(t1);t1\<longrightarrow>\<^isub>\<beta> t2\<rbrakk>\<Longrightarrow>SN(t2)"
apply(simp add: SN_def)
apply(drule_tac a="t2" in acc_downward)
apply(auto)
done

lemma SN_intro: "(\<forall>t2. t1\<longrightarrow>\<^isub>\<beta>t2 \<longrightarrow> SN(t2))\<Longrightarrow>SN(t1)"
apply(simp add: SN_def)
apply(rule accI)
apply(auto)
done

section {* Candidates *}

lemma ty_cases:
  fixes x::ty
  shows "(\<exists>X. x= TVar X) \<or> (\<exists>T1 T2. x=T1\<rightarrow>T2)"
by (induct x rule: ty.induct_weak) (auto)

function
  RED :: "ty \<Rightarrow> lam set"
where
  "RED (TVar X) = {t. SN(t)}"
| "RED (\<tau>\<rightarrow>\<sigma>) =   {t. \<forall>u. (u\<in>RED \<tau> \<longrightarrow> (App t u)\<in>RED \<sigma>)}"
apply(auto simp add: ty.inject)
apply(subgoal_tac "(\<exists>X. x= TVar X) \<or> (\<exists>T1 T2. x=T1\<rightarrow>T2)")
apply(blast)
apply(rule ty_cases)
done

instance ty :: size ..

nominal_primrec
  "size (TVar X) = 1"
  "size (T\<^isub>1\<rightarrow>T\<^isub>2) = size T\<^isub>1 + size T\<^isub>2"
by (rule TrueI)+

lemma ty_size_greater_zero[simp]:
  fixes T::"ty"
  shows "size T > 0"
by (nominal_induct T rule: ty.induct) (simp_all)

termination
apply(relation "measure size") 
apply(auto)
done

constdefs
  NEUT :: "lam \<Rightarrow> bool"
  "NEUT t \<equiv> (\<exists>a. t=Var a)\<or>(\<exists>t1 t2. t=App t1 t2)" 

(* a slight hack to get the first element of applications *)
inductive2 FST :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<guillemotright> _" [80,80] 80)
where
  fst[intro!]:  "(App t s) \<guillemotright> t"<commit_msg>deleted function for defining candidates and used nominal_primrec instead<commit_after>(* $Id$ *)

theory SN
imports Lam_Funs
begin

text {* Strong Normalisation proof from the Proofs and Types book *}

section {* Beta Reduction *}

lemma subst_rename: 
  assumes a: "c\<sharp>t1"
  shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]"
using a
by (nominal_induct t1 avoiding: a c t2 rule: lam.induct)
   (auto simp add: calc_atm fresh_atm abs_fresh)

lemma forget: 
  assumes a: "a\<sharp>t1"
  shows "t1[a::=t2] = t1"
  using a
by (nominal_induct t1 avoiding: a t2 rule: lam.induct)
   (auto simp add: abs_fresh fresh_atm)

lemma fresh_fact: 
  fixes a::"name"
  assumes a: "a\<sharp>t1"
  and     b: "a\<sharp>t2"
  shows "a\<sharp>(t1[b::=t2])"
using a b
by (nominal_induct t1 avoiding: a b t2 rule: lam.induct)
   (auto simp add: abs_fresh fresh_atm)

lemma subst_lemma:  
  assumes a: "x\<noteq>y"
  and     b: "x\<sharp>L"
  shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
using a b
by (nominal_induct M avoiding: x y N L rule: lam.induct)
   (auto simp add: fresh_fact forget)

lemma id_subs: 
  shows "t[x::=Var x] = t"
  by (nominal_induct t avoiding: x rule: lam.induct)
     (simp_all add: fresh_atm)

lemma subst_eqvt[eqvt]:
  fixes pi::"name prm" 
  and   t::"lam"
  shows "pi\<bullet>(t[x::=t']) = (pi\<bullet>t)[(pi\<bullet>x)::=(pi\<bullet>t')]"
by (nominal_induct t avoiding: x t' rule: lam.induct)
   (perm_simp add: fresh_bij)+

inductive2 Beta :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
where
  b1[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App s1 t)\<longrightarrow>\<^isub>\<beta>(App s2 t)"
| b2[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App t s1)\<longrightarrow>\<^isub>\<beta>(App t s2)"
| b3[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>\<beta> (Lam [(a::name)].s2)"
| b4[intro!]: "(App (Lam [(a::name)].s1) s2)\<longrightarrow>\<^isub>\<beta>(s1[a::=s2])"

abbreviation "Beta_star"  :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80) where
  "t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2 \<equiv> Beta\<^sup>*\<^sup>* t1 t2"

nominal_inductive Beta
 
lemma beta_induct[consumes 1, case_names b1 b2 b3 b4]:
  fixes  P :: "'a::fs_name\<Rightarrow>lam \<Rightarrow> lam \<Rightarrow>bool"
  and    t :: "lam"
  and    s :: "lam"
  and    x :: "'a::fs_name"
  assumes a: "t\<longrightarrow>\<^isub>\<beta>s"
  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)"
  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)"
  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)"
  and a4:    "\<And>a t1 s1 x. a\<sharp>x \<Longrightarrow> P x (App (Lam [a].t1) s1) (t1[a::=s1])"
  shows "P x t s"
proof -
  from a have "\<And>(pi::name prm) x. P x (pi\<bullet>t) (pi\<bullet>s)"
  proof (induct)
    case b1 thus ?case using a1 by (simp, blast intro: eqvt)
  next
    case b2 thus ?case using a2 by (simp, blast intro: eqvt)
  next
    case (b3 s1 s2 a)
    have j1: "s1 \<longrightarrow>\<^isub>\<beta> s2" by fact
    have j2: "\<And>x (pi::name prm). P x (pi\<bullet>s1) (pi\<bullet>s2)" by fact
    show ?case 
    proof (simp)
      have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
	by (rule exists_fresh', simp add: fs_name1)
      then obtain c::"name" 
	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)"
	by (force simp add: fresh_prod fresh_atm)
      have x: "P x (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s1)) (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s2))"
	using a3 f2 j1 j2 by (simp, blast intro: eqvt)
      have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s1))" using f1 f3
	by (simp add: lam.inject alpha)
      have alpha2: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s2))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s2))" using f1 f3
	by (simp add: lam.inject alpha)
      show " P x (Lam [(pi\<bullet>a)].(pi\<bullet>s1)) (Lam [(pi\<bullet>a)].(pi\<bullet>s2))"
	using x alpha1 alpha2 by (simp only: pt_name2)
    qed
  next
    case (b4 a s1 s2)
    show ?case
    proof (simp add: subst_eqvt)
      have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
	by (rule exists_fresh', simp add: fs_name1)
      then obtain c::"name" 
	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)"
	by (force simp add: fresh_prod fresh_atm)
      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)])"
	using a4 f2 by (blast intro!: eqvt)
      have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s1))" using f1 f3
	by (simp add: lam.inject alpha)
      have alpha2: "(([(c,pi\<bullet>a)]@pi)\<bullet>s1)[c::=(pi\<bullet>s2)] = (pi\<bullet>s1)[(pi\<bullet>a)::=(pi\<bullet>s2)]"
	using f3 by (simp only: subst_rename[symmetric] pt_name2)
      show "P x (App (Lam [(pi\<bullet>a)].(pi\<bullet>s1)) (pi\<bullet>s2)) ((pi\<bullet>s1)[(pi\<bullet>a)::=(pi\<bullet>s2)])"
	using x alpha1 alpha2 by (simp only: pt_name2)
    qed
  qed
  hence "P x (([]::name prm)\<bullet>t) (([]::name prm)\<bullet>s)" by blast 
  thus ?thesis by simp
qed

lemma supp_beta: 
  assumes a: "t\<longrightarrow>\<^isub>\<beta> s"
  shows "(supp s)\<subseteq>((supp t)::name set)"
using a
by (induct)
   (auto intro!: simp add: abs_supp lam.supp subst_supp)


lemma beta_abs: "Lam [a].t\<longrightarrow>\<^isub>\<beta> t'\<Longrightarrow>\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>\<beta> t''"
apply(ind_cases2 "Lam [a].t  \<longrightarrow>\<^isub>\<beta> t'")
apply(auto simp add: lam.distinct lam.inject)
apply(auto simp add: alpha)
apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)
apply(rule conjI)
apply(rule sym)
apply(rule pt_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp)
apply(rule pt_name3)
apply(simp add: at_ds5[OF at_name_inst])
apply(rule conjI)
apply(simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst] calc_atm)
apply(force dest!: supp_beta simp add: fresh_def)
apply(force intro!: eqvt)
done

lemma beta_subst: 
  assumes a: "M \<longrightarrow>\<^isub>\<beta> M'"
  shows "M[x::=N]\<longrightarrow>\<^isub>\<beta> M'[x::=N]" 
using a
apply(nominal_induct M M' avoiding: x N rule: beta_induct)
apply(auto simp add: fresh_atm subst_lemma)
done

section {* types *}

nominal_datatype ty =
    TVar "nat"
  | TArr "ty" "ty" (infix "\<rightarrow>" 200)

lemma perm_ty[simp]:
  fixes pi ::"name prm"
  and   \<tau>  ::"ty"
  shows "pi\<bullet>\<tau> = \<tau>"
by (nominal_induct \<tau> rule: ty.induct) 
   (simp_all add: perm_nat_def)

lemma fresh_ty:
  fixes a ::"name"
  and   \<tau>  ::"ty"
  shows "a\<sharp>\<tau>"
  by (simp add: fresh_def supp_def)

(* valid contexts *)

consts
  "dom_ty" :: "(name\<times>ty) list \<Rightarrow> (name list)"
primrec
  "dom_ty []    = []"
  "dom_ty (x#\<Gamma>) = (fst x)#(dom_ty \<Gamma>)" 

inductive2 valid :: "(name\<times>ty) list \<Rightarrow> bool"
where
  v1[intro]: "valid []"
| v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)"

nominal_inductive valid

(* typing judgements *)

lemma fresh_context: 
  fixes  \<Gamma> :: "(name\<times>ty)list"
  and    a :: "name"
  assumes a: "a\<sharp>\<Gamma>"
  shows "\<not>(\<exists>\<tau>::ty. (a,\<tau>)\<in>set \<Gamma>)"
using a
apply(induct \<Gamma>)
apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
done

inductive_cases2 valid_elim[elim]: "valid ((a,\<tau>)#\<Gamma>)"

lemma valid_unicity: 
  assumes a: "valid \<Gamma>"
  and     b: "(c,\<sigma>)\<in>set \<Gamma>"
  and     c: "(c,\<tau>)\<in>set \<Gamma>"
  shows "\<sigma>=\<tau>" 
using a b c
by (induct \<Gamma>) (auto dest!: fresh_context)

inductive2 typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80)
where
  t1[intro]: "\<lbrakk>valid \<Gamma>; (a,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var a : \<tau>"
| t2[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>"
| t3[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>"

lemma eqvt_typing: 
  fixes  \<Gamma> :: "(name\<times>ty) list"
  and    t :: "lam"
  and    \<tau> :: "ty"
  and    pi:: "name prm"
  assumes a: "\<Gamma> \<turnstile> t : \<tau>"
  shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>t) : \<tau>"
using a
proof (induct)
  case (t1 \<Gamma> a \<tau>)
  have "valid (pi\<bullet>\<Gamma>)" by (rule valid_eqvt)
  moreover
  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])
  ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> ((pi::name prm)\<bullet>Var a) : \<tau>"
    using typing.t1 by (force simp add: set_eqvt[symmetric])
next 
  case (t3 a \<Gamma> \<tau> t \<sigma>)
  moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_bij)
  ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) :\<tau>\<rightarrow>\<sigma>" by force 
qed (auto)

lemma typing_induct[consumes 1, case_names t1 t2 t3]:
  fixes  P :: "'a::fs_name\<Rightarrow>(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow>bool"
  and    \<Gamma> :: "(name\<times>ty) list"
  and    t :: "lam"
  and    \<tau> :: "ty"
  and    x :: "'a::fs_name"
  assumes a: "\<Gamma> \<turnstile> t : \<tau>"
  and a1:    "\<And>\<Gamma> (a::name) \<tau> x. valid \<Gamma> \<Longrightarrow> (a,\<tau>) \<in> set \<Gamma> \<Longrightarrow> P x \<Gamma> (Var a) \<tau>"
  and a2:    "\<And>\<Gamma> \<tau> \<sigma> t1 t2 x. 
              \<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>)
              \<Longrightarrow> P x \<Gamma> (App t1 t2) \<sigma>"
  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>)
              \<Longrightarrow> P x \<Gamma> (Lam [a].t) (\<tau>\<rightarrow>\<sigma>)"
  shows "P x \<Gamma> t \<tau>"
proof -
  from a have "\<And>(pi::name prm) x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>t) \<tau>"
  proof (induct)
    case (t1 \<Gamma> a \<tau>)
    have j1: "valid \<Gamma>" by fact
    have j2: "(a,\<tau>)\<in>set \<Gamma>" by fact
    from j1 have j3: "valid (pi\<bullet>\<Gamma>)" by (rule valid_eqvt)
    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])  
    hence j4: "(pi\<bullet>a,\<tau>)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: eqvt)
    show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Var a)) \<tau>" using a1 j3 j4 by simp
  next
    case (t2 \<Gamma> t1 \<tau> \<sigma> t2)
    thus ?case using a2 by (simp, blast intro: eqvt_typing)
  next
    case (t3 a \<Gamma> \<tau> t \<sigma>)
    have k1: "a\<sharp>\<Gamma>" by fact
    have k2: "((a,\<tau>)#\<Gamma>)\<turnstile>t:\<sigma>" by fact
    have k3: "\<And>(pi::name prm) (x::'a::fs_name). P x (pi \<bullet>((a,\<tau>)#\<Gamma>)) (pi\<bullet>t) \<sigma>" by fact
    have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t,pi\<bullet>\<Gamma>,x)"
      by (rule exists_fresh', simp add: fs_name1)
    then obtain c::"name" 
      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>)"
      by (force simp add: fresh_prod at_fresh[OF at_name_inst])
    from k1 have k1a: "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" 
      by (simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst] 
                    pt_rev_pi[OF pt_name_inst, OF at_name_inst])
    have l1: "(([(c,pi\<bullet>a)]@pi)\<bullet>\<Gamma>) = (pi\<bullet>\<Gamma>)" using f4 k1a 
      by (simp only: pt2[OF pt_name_inst], rule pt_fresh_fresh[OF pt_name_inst, OF at_name_inst])
    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
    hence l2: "\<And>x. P x ((c, \<tau>)#(pi\<bullet>\<Gamma>)) (([(c,pi\<bullet>a)]@pi)\<bullet>t) \<sigma>" using f1 l1
      by (force simp add: pt2[OF pt_name_inst]  at_calc[OF at_name_inst])
    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)
    hence l3: "((c, \<tau>)#(pi\<bullet>\<Gamma>)) \<turnstile> (([(c,pi\<bullet>a)]@pi)\<bullet>t) : \<sigma>" using l1 f1 
      by (force simp add: pt2[OF pt_name_inst]  at_calc[OF at_name_inst])
    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
    have alpha: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t))) = (Lam [(pi\<bullet>a)].(pi\<bullet>t))" using f1 f3
      by (simp add: lam.inject alpha)
    show "P x (pi\<bullet>\<Gamma>) (pi\<bullet>(Lam [a].t)) (\<tau> \<rightarrow> \<sigma>)" using l4 alpha 
      by (simp only: pt2[OF pt_name_inst], simp)
  qed
  hence "P x (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>t) \<tau>" by blast
  thus "P x \<Gamma> t \<tau>" by simp
qed

abbreviation
  "sub" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" (" _ \<lless> _ " [80,80] 80) where
  "\<Gamma>1 \<lless> \<Gamma>2 \<equiv> \<forall>a \<sigma>. (a,\<sigma>)\<in>set \<Gamma>1 \<longrightarrow>  (a,\<sigma>)\<in>set \<Gamma>2"

lemma weakening: 
  assumes a: "\<Gamma>1 \<turnstile> t : \<sigma>" 
  and     b: "valid \<Gamma>2" 
  and     c: "\<Gamma>1 \<lless> \<Gamma>2"
  shows "\<Gamma>2 \<turnstile> t:\<sigma>"
using a b c
apply(nominal_induct \<Gamma>1 t \<sigma> avoiding: \<Gamma>2 rule: typing_induct)
apply(auto | atomize)+
(* FIXME: before using meta-connectives and the new induction *)
(* method, this was completely automatic *)
done

lemma in_ctxt: 
  assumes a: "(a,\<tau>)\<in>set \<Gamma>"
  shows "a\<in>set(dom_ty \<Gamma>)"
using a
by (induct \<Gamma>) (auto)

lemma free_vars: 
  assumes a: "\<Gamma> \<turnstile> t : \<tau>"
  shows " (supp t)\<subseteq>set(dom_ty \<Gamma>)"
using a
by (nominal_induct \<Gamma> t \<tau> rule: typing_induct)
   (auto simp add: lam.supp abs_supp supp_atm in_ctxt)

lemma t1_elim: "\<Gamma> \<turnstile> Var a : \<tau> \<Longrightarrow> valid \<Gamma> \<and> (a,\<tau>) \<in> set \<Gamma>"
apply(ind_cases2 "\<Gamma> \<turnstile> Var a : \<tau>")
apply(auto simp add: lam.inject lam.distinct)
done

lemma t2_elim: "\<Gamma> \<turnstile> App t1 t2 : \<sigma> \<Longrightarrow> \<exists>\<tau>. (\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma> \<and> \<Gamma> \<turnstile> t2 : \<tau>)"
apply(ind_cases2 "\<Gamma> \<turnstile> App t1 t2 : \<sigma>")
apply(auto simp add: lam.inject lam.distinct)
done

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>'"
apply(ind_cases2 "\<Gamma> \<turnstile> Lam [a].t : \<sigma>")
apply(auto simp add: lam.distinct lam.inject alpha) 
apply(drule_tac pi="[(a,aa)]::name prm" in eqvt_typing)
apply(simp)
apply(subgoal_tac "([(a,aa)]::name prm)\<bullet>\<Gamma> = \<Gamma>")(*A*)
apply(force simp add: calc_atm)
(*A*)
apply(force intro!: pt_fresh_fresh[OF pt_name_inst, OF at_name_inst])
done

lemma typing_valid: 
  assumes a: "\<Gamma> \<turnstile> t : \<tau>" 
  shows "valid \<Gamma>"
using a by (induct, auto)

lemma ty_subs:
  assumes a: "((c,\<sigma>)#\<Gamma>) \<turnstile> t1:\<tau>"
  and     b: "\<Gamma>\<turnstile> t2:\<sigma>"
  shows  "\<Gamma> \<turnstile> t1[c::=t2]:\<tau>"
using a b
proof(nominal_induct t1 avoiding: \<Gamma> \<sigma> \<tau> c t2 rule: lam.induct)
  case (Var a) 
  have a1: "\<Gamma> \<turnstile>t2:\<sigma>" by fact
  have a2: "((c,\<sigma>)#\<Gamma>) \<turnstile> Var a:\<tau>" by fact
  hence a21: "(a,\<tau>)\<in>set((c,\<sigma>)#\<Gamma>)" and a22: "valid((c,\<sigma>)#\<Gamma>)" by (auto dest: t1_elim)
  from a22 have a23: "valid \<Gamma>" and a24: "c\<sharp>\<Gamma>" by (auto dest: valid_elim) 
  from a24 have a25: "\<not>(\<exists>\<tau>. (c,\<tau>)\<in>set \<Gamma>)" by (rule fresh_context)
  show "\<Gamma>\<turnstile>(Var a)[c::=t2] : \<tau>"
  proof (cases "a=c", simp_all)
    assume case1: "a=c"
    show "\<Gamma> \<turnstile> t2:\<tau>" using a1
    proof (cases "\<sigma>=\<tau>")
      assume "\<sigma>=\<tau>" thus ?thesis using a1 by simp 
    next
      assume a3: "\<sigma>\<noteq>\<tau>"
      show ?thesis
      proof (rule ccontr)
	from a3 a21 have "(a,\<tau>)\<in>set \<Gamma>" by force
	with case1 a25 show False by force 
      qed
    qed
  next
    assume case2: "a\<noteq>c"
    with a21 have a26: "(a,\<tau>)\<in>set \<Gamma>" by force 
    from a23 a26 show "\<Gamma> \<turnstile> Var a:\<tau>" by force
  qed
next
  case (App s1 s2)
  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
  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
  have "((c,\<sigma>)#\<Gamma>)\<turnstile>App s1 s2 : \<tau>" by fact
  hence "\<exists>\<tau>'. ((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau> \<and> ((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>'" by (rule t2_elim) 
  then obtain \<tau>' where "((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau>" and "((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>'" by blast
  moreover
  have "\<Gamma> \<turnstile>t2:\<sigma>" by fact
  ultimately show "\<Gamma> \<turnstile>  (App s1 s2)[c::=t2] : \<tau>" using ih_s1 ih_s2 by (simp, blast)
next
  case (Lam a s)
  have "a\<sharp>\<Gamma>" "a\<sharp>\<sigma>" "a\<sharp>\<tau>" "a\<sharp>c" "a\<sharp>t2" by fact 
  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>)"
    by (auto simp add: fresh_atm fresh_prod fresh_list_cons)
  have c1: "((c,\<sigma>)#\<Gamma>)\<turnstile>Lam [a].s : \<tau>" by fact
  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) 
  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
  from c12 have "valid ((a,\<tau>1)#(c,\<sigma>)#\<Gamma>)" by (rule typing_valid)
  hence ca: "valid \<Gamma>" and cb: "a\<sharp>\<Gamma>" and cc: "c\<sharp>\<Gamma>" 
    by (auto simp add: fresh_list_cons) 
  from c12 have c14: "((c,\<sigma>)#(a,\<tau>1)#\<Gamma>) \<turnstile> s : \<tau>2"
  proof -
    have c2: "((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<lless> ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)" by force
    have c3: "valid ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)"
      by (rule v2, rule v2, auto simp add: fresh_list_cons fresh_prod ca cb cc f2' fresh_ty)
    from c12 c2 c3 show ?thesis by (force intro: weakening)
  qed
  assume c8: "\<Gamma> \<turnstile> t2 : \<sigma>"
  have c81: "((a,\<tau>1)#\<Gamma>)\<turnstile>t2 :\<sigma>"
  proof -
    have c82: "\<Gamma> \<lless> ((a,\<tau>1)#\<Gamma>)" by force
    have c83: "valid ((a,\<tau>1)#\<Gamma>)" using f1 ca by force
    with c8 c82 c83 show ?thesis by (force intro: weakening)
  qed
  show "\<Gamma> \<turnstile> (Lam [a].s)[c::=t2] : \<tau>"
    using c11 prems c14 c81 f1 by force
qed

lemma subject: 
  assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2"
  and     b: "\<Gamma> \<turnstile> t1:\<tau>"
  shows "\<Gamma> \<turnstile> t2:\<tau>"
using a b
proof (nominal_induct t1 t2 avoiding: \<Gamma> \<tau> rule: beta_induct)
  case (b1 t s1 s2) --"App-case left"
  have ih: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1:\<tau> \<Longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact
  have "\<Gamma> \<turnstile> App s1 t : \<tau>" by fact 
  hence "\<exists>\<sigma>. \<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> t : \<sigma>" by (rule t2_elim)
  then obtain \<sigma> where "\<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau>" and "\<Gamma> \<turnstile> t : \<sigma>" by blast
  with ih show "\<Gamma> \<turnstile> App s2 t : \<tau>" by blast
next
  case (b2 t s1 s2) --"App-case right"
  have ih: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact 
  have "\<Gamma> \<turnstile> App t s1 : \<tau>" by fact
  hence "\<exists>\<sigma>. \<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> s1 : \<sigma>" by (rule t2_elim)
  then obtain \<sigma> where "\<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau>" and "\<Gamma> \<turnstile> s1 : \<sigma>" by blast
  with ih show "\<Gamma> \<turnstile> App t s2 : \<tau>" by blast
next
  case (b3 a s1 s2) --"Lam-case"
  have fr: "a\<sharp>\<Gamma>" "a\<sharp>\<tau>" by fact
  have ih: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact
  have "\<Gamma> \<turnstile> Lam [a].s1 : \<tau>" by fact
  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)
  then obtain \<tau>1 \<tau>2 where "\<tau>=\<tau>1\<rightarrow>\<tau>2" and "((a,\<tau>1)#\<Gamma>) \<turnstile> s1 : \<tau>2" by blast
  with ih show "\<Gamma> \<turnstile> Lam [a].s2 : \<tau>" using fr by blast
next
  case (b4 a s1 s2) --"Beta-redex"
  have fr: "a\<sharp>\<Gamma>" by fact
  have "\<Gamma> \<turnstile> App (Lam [a].s1) s2 : \<tau>" by fact
  hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> (Lam [a].s1) : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> s2 : \<sigma>)" by (simp add: t2_elim)
  then obtain \<sigma> where a1: "\<Gamma> \<turnstile> (Lam [a].s1) : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> s2 : \<sigma>" by blast
  from a1 have "((a,\<sigma>)#\<Gamma>) \<turnstile> s1 : \<tau>" using fr by (auto dest!: t3_elim simp add: ty.inject) 
  with a2 show "\<Gamma> \<turnstile> s1[a::=s2] : \<tau>" by (simp add: ty_subs)
qed

lemma subject_automatic: 
  assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2"
  and     b: "\<Gamma> \<turnstile> t1:\<tau>"
  shows "\<Gamma> \<turnstile> t2:\<tau>"
using a b
apply(nominal_induct t1 t2 avoiding: \<Gamma> \<tau> rule: beta_induct)
apply(auto dest!: t2_elim t3_elim intro: ty_subs simp add: ty.inject)
done

subsection {* some facts about beta *}

constdefs
  "NORMAL" :: "lam \<Rightarrow> bool"
  "NORMAL t \<equiv> \<not>(\<exists>t'. t\<longrightarrow>\<^isub>\<beta> t')"

lemma NORMAL_Var:
  shows "NORMAL (Var a)"
proof -
  { assume "\<exists>t'. (Var a) \<longrightarrow>\<^isub>\<beta> t'"
    then obtain t' where "(Var a) \<longrightarrow>\<^isub>\<beta> t'" by blast
    hence False by (cases, auto) 
  }
  thus "NORMAL (Var a)" by (force simp add: NORMAL_def)
qed

constdefs
  "SN" :: "lam \<Rightarrow> bool"
  "SN t \<equiv> termi Beta t"

lemma SN_preserved: "\<lbrakk>SN(t1);t1\<longrightarrow>\<^isub>\<beta> t2\<rbrakk>\<Longrightarrow>SN(t2)"
apply(simp add: SN_def)
apply(drule_tac a="t2" in acc_downward)
apply(auto)
done

lemma SN_intro: "(\<forall>t2. t1\<longrightarrow>\<^isub>\<beta>t2 \<longrightarrow> SN(t2))\<Longrightarrow>SN(t1)"
apply(simp add: SN_def)
apply(rule accI)
apply(auto)
done

section {* Candidates *}

consts
  RED :: "ty \<Rightarrow> lam set"

nominal_primrec
  "RED (TVar X) = {t. SN(t)}"
  "RED (\<tau>\<rightarrow>\<sigma>) =   {t. \<forall>u. (u\<in>RED \<tau> \<longrightarrow> (App t u)\<in>RED \<sigma>)}"
apply(rule TrueI)+
done


constdefs
  NEUT :: "lam \<Rightarrow> bool"
  "NEUT t \<equiv> (\<exists>a. t=Var a)\<or>(\<exists>t1 t2. t=App t1 t2)" 

(* a slight hack to get the first element of applications *)
inductive2 FST :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<guillemotright> _" [80,80] 80)
where
  fst[intro!]:  "(App t s) \<guillemotright> t"
{'fraction_non_alphanumeric': 0.23621739045345128, 'fraction_numerical': 0.02141025891931033, 'mean_word_length': 3.9900390625, 'pattern_counts': {'":': 0, '<': 2084, '<?xml version=': 0, '>': 2085, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4869126', 'n_tokens_mistral': 22965, 'n_tokens_neox': 21022, 'n_words': 5335}