Quelle  SN.thy   Sprache: Isabelle

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\t1"
  shows "t1[a::=t2] = ([(c,a)]\t1)[c::=t2]"
using a
by (nominal_induct t1 avoiding: a c t2 rule: lam.strong_induct)
   (auto simp add: calc_atm fresh_atm abs_fresh)

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

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

lemma fresh_fact':
  fixes a::"name"
  assumes a: "a\t2"
  shows "a\t1[a::=t2]"
using a 
by (nominal_induct t1 avoiding: a t2 rule: lam.strong_induct)
   (auto simp add: abs_fresh fresh_atm)

lemma subst_lemma:  
  assumes a: "x\y"
  and     b: "x\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.strong_induct)
   (auto simp add: fresh_fact forget)

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

lemma lookup_fresh:
  fixes z::"name"
  assumes "z\\" "z\x"
  shows "z\ lookup \ x"
using assms 
by (induct rule: lookup.induct) (auto simp add: fresh_list_cons)

lemma lookup_fresh':
  assumes "z\\"
  shows "lookup \ z = Var z"
using assms 
by (induct rule: lookup.induct)
   (auto simp add: fresh_list_cons fresh_prod fresh_atm)

lemma psubst_subst:
  assumes h:"c\\"
  shows "(\)[c::=s] = ((c,s)#\)"
  using h
by (nominal_induct t avoiding: θ c s rule: lam.strong_induct)
   (auto simp add: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh')
 
inductive 
  Beta :: "lam\lam\bool" (‹ _ ⟶🚫β _› [80,80] 80)
where
  b1[intro!]: "s1 \\<^sub>\ s2 \ App s1 t \\<^sub>\ App s2 t"
| b2[intro!]: "s1\\<^sub>\s2 \ App t s1 \\<^sub>\ App t s2"
| b3[intro!]: "s1\\<^sub>\s2 \ Lam [a].s1 \\<^sub>\ Lam [a].s2"
| b4[intro!]: "a\s2 \ App (Lam [a].s1) s2\\<^sub>\ (s1[a::=s2])"

equivariance Beta

nominal_inductive Beta
  by (simp_all add: abs_fresh fresh_fact')

lemma beta_preserves_fresh: 
  fixes a::"name"
  assumes a: "t\\<^sub>\ s"
  shows "a\t \ a\s"
using a
  by (nominal_induct t s avoiding: a rule: Beta.strong_induct)
     (auto simp add: abs_fresh fresh_fact fresh_atm)

lemma beta_abs: 
  assumes a: "Lam [a].t\\<^sub>\ t'" 
  shows "\t''. t'=Lam [a].t'' \ t\\<^sub>\ t''"
proof -
  have "a\Lam [a].t" by (simp add: abs_fresh)
  with a have "a\t'" by (simp add: beta_preserves_fresh)
  with a show ?thesis
    by (cases rule: Beta.strong_cases[where a="a" and aa="a"])
       (auto simp add: lam.inject abs_fresh alpha)
qed

lemma beta_subst: 
  assumes a: "M \\<^sub>\ M'"
  shows "M[x::=N]\\<^sub>\ M'[x::=N]" 
using a
by (nominal_induct M M' avoiding: x N rule: Beta.strong_induct)
   (auto simp add: fresh_atm subst_lemma fresh_fact)

section ‹types›

nominal_datatype ty =
    TVar "nat"
  | TArr "ty" "ty" (infix ‹→› 200)

lemma fresh_ty:
  fixes a ::"name"
  and   τ  ::"ty"
  shows "a\\"
by (nominal_induct τ rule: ty.strong_induct)
   (auto simp add: fresh_nat)

(* valid contexts *)

inductive 
  valid :: "(name\ty) list \ bool"
where
  v1[intro]: "valid []"
| v2[intro]: "\valid \;a\\\\ valid ((a,\)#\)"

equivariance valid 

(* typing judgements *)

lemma fresh_context: 
  fixes  Γ :: "(name\ty)list"
  and    a :: "name"
  assumes a: "a\\"
  shows "\(\\::ty. (a,\)\set \)"
using a
by (induct Γ)
   (auto simp add: fresh_prod fresh_list_cons fresh_atm)

inductive 
  typing :: "(name\ty) list\lam\ty\bool" (‹_ ⊨ _ : _› [60,60,60] 60)
where
  t1[intro]: "\valid \; (a,\)\set \\ \ \ \ Var a : \"
| t2[intro]: "\\ \ t1 : \\\; \ \ t2 : \\ \ \ \ App t1 t2 : \"
| t3[intro]: "\a\\;((a,\)#\) \ t : \\ \ \ \ Lam [a].t : \\\"

equivariance typing

nominal_inductive typing
  by (simp_all add: abs_fresh fresh_ty)

subsection ‹a fact about beta›

definition "NORMAL" :: "lam \ bool" where
  "NORMAL t \ \(\t'. t\\<^sub>\ t')"

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

text ‹Inductive version of Strong Normalisation›
inductive 
  SN :: "lam \ bool"
where
  SN_intro: "(\t'. t \\<^sub>\ t' \ SN t') \ SN t"

lemma SN_preserved: 
  assumes a: "SN t1" "t1\\<^sub>\ t2"
  shows "SN t2"
using a 
by (cases) (auto)

lemma double_SN_aux:
  assumes a: "SN a"
  and b: "SN b"
  and hyp: "\x z.
    [∧y. x ⟶🚫β y ==> SN y; ∧y. x ⟶🚫β y ==> P y z;
     ∧u. z ⟶🚫β u ==> SN u; ∧u. z ⟶🚫β u ==> P x u] ==> P x z"
  shows "P a b"
proof -
  from a
  have r: "\b. SN b \ P a b"
  proof (induct a rule: SN.SN.induct)
    case (SN_intro x)
    note SNI' = SN_intro
    have "SN b" by fact
    thus ?case
    proof (induct b rule: SN.SN.induct)
      case (SN_intro y)
      with SNI' show ?case
        by (metis SN.simps hyp)
    qed
  qed
  from b show ?thesis by (rule r)
qed

lemma double_SN[consumes 2]:
  assumes a: "SN a"
  and     b: "SN b" 
  and     c: "\x z. \\y. x \\<^sub>\ y \ P y z; \u. z \\<^sub>\ u \ P x u\ \ P x z"
  shows "P a b"
using a b c
  by (smt (verit, best) double_SN_aux)

section ‹Candidates›

nominal_primrec
  RED :: "ty \ lam set"
where
  "RED (TVar X) = {t. SN(t)}"
| "RED (\\\) = {t. \u. (u\RED \ \ (App t u)\RED \)}"
by (rule TrueI)+

text ‹neutral terms›
definition NEUT :: "lam \ bool" where
  "NEUT t \ (\a. t = Var a) \ (\t1 t2. t = App t1 t2)" 

(* a slight hack to get the first element of applications *)
(* this is needed to get (SN t) from SN (App t s)         *) 
inductive 
  FST :: "lam\lam\bool" (‹ _ ¬ _› [80,80] 80)
where
  fst[intro!]:  "(App t s) \ t"

nominal_primrec
  fst_app_aux::"lam\lam option"
where
  "fst_app_aux (Var a) = None"
| "fst_app_aux (App t1 t2) = Some t1"
| "fst_app_aux (Lam [x].t) = None"
by (finite_guess | simp add: fresh_none | fresh_guess)+

definition
  fst_app_def[simp]: "fst_app t = the (fst_app_aux t)"

lemma SN_of_FST_of_App: 
  assumes a: "SN (App t s)"
  shows "SN (fst_app (App t s))"
using a
proof - 
  from a have "\z. (App t s \ z) \ SN z"
    by (induct rule: SN.SN.induct)
       (blast elim: FST.cases intro: SN_intro)
  then have "SN t" by blast
  then show "SN (fst_app (App t s))" by simp
qed

section ‹Candidates›

definition "CR1" :: "ty \ bool" where
  "CR1 \ \ \t. (t\RED \ \ SN t)"

definition "CR2" :: "ty \ bool" where
  "CR2 \ \ \t t'. (t\RED \ \ t \\<^sub>\ t') \ t'\RED \"

definition "CR3_RED" :: "lam \ ty \ bool" where
  "CR3_RED t \ \ \t'. t\\<^sub>\ t' \ t'\RED \" 

definition "CR3" :: "ty \ bool" where
  "CR3 \ \ \t. (NEUT t \ CR3_RED t \) \ t\RED \"
   
definition "CR4" :: "ty \ bool" where
  "CR4 \ \ \t. (NEUT t \ NORMAL t) \t\RED \"

lemma CR3_implies_CR4: 
  assumes a: "CR3 \" 
  shows "CR4 \"
using a by (auto simp add: CR3_def CR3_RED_def CR4_def NORMAL_def)

(* sub_induction in the arrow-type case for the next proof *) 
lemma sub_induction: 
  assumes a: "SN(u)"
  and     b: "u\RED \"
  and     c1: "NEUT t"
  and     c2: "CR2 \"
  and     c3: "CR3 \"
  and     c4: "CR3_RED t (\\\)"
  shows "(App t u)\RED \"
using a b
proof (induct)
  fix u
  assume as: "u\RED \"
  assume ih: " \u'. \u \\<^sub>\ u'; u' \ RED \\ \ App t u' \ RED \"
  have "NEUT (App t u)" using c1 by (auto simp add: NEUT_def)
  moreover
  have "CR3_RED (App t u) \" unfolding CR3_RED_def
  proof (intro strip)
    fix r
    assume red: "App t u \\<^sub>\ r"
    moreover
    { assume "\t'. t \\<^sub>\ t' \ r = App t' u"
      then obtain t' where a1: "t \\<^sub>\ t'" and a2: "r = App t' u" by blast
      have "t'\RED (\\\)" using c4 a1 by (simp add: CR3_RED_def)
      then have "App t' u\RED \" using as by simp
      then have "r\RED \" using a2 by simp
    }
    moreover
    { assume "\u'. u \\<^sub>\ u' \ r = App t u'"
      then obtain u' where b1: "u \\<^sub>\ u'" and b2: "r = App t u'" by blast
      have "u'\RED \" using as b1 c2 by (auto simp add: CR2_def)
      with ih have "App t u' \ RED \" using b1 by simp
      then have "r\RED \" using b2 by simp
    }
    moreover
    { assume "\x t'. t = Lam [x].t'"
      then obtain x t' where "t = Lam [x].t'" by blast
      then have "NEUT (Lam [x].t')" using c1 by simp
      then have "False" by (simp add: NEUT_def)
      then have "r\RED \" by simp
    }
    ultimately show "r \ RED \" by (cases) (auto simp add: lam.inject)
  qed
  ultimately show "App t u \ RED \" using c3 by (simp add: CR3_def)
qed 

text ‹properties of the candiadates›
lemma RED_props: 
  shows "CR1 \" and "CR2 \" and "CR3 \"
proof (nominal_induct τ rule: ty.strong_induct)
  case (TVar a)
  { case 1 show "CR1 (TVar a)" by (simp add: CR1_def)
  next
    case 2 show "CR2 (TVar a)" by (auto intro: SN_preserved simp add: CR2_def)
  next
    case 3 show "CR3 (TVar a)" by (auto intro: SN_intro simp add: CR3_def CR3_RED_def)
  }
next
  case (TArr τ1 τ2)
  { case 1
    have ih_CR3_τ1: "CR3 \1" by fact
    have ih_CR1_τ2: "CR1 \2" by fact
    have "\t. t \ RED (\1 \ \2) \ SN t" 
    proof - 
      fix t
      assume "t \ RED (\1 \ \2)"
      then have a: "\u. u \ RED \1 \ App t u \ RED \2" by simp
      from ih_CR3_τ1 have "CR4 \1" by (simp add: CR3_implies_CR4) 
      moreover
      fix a have "NEUT (Var a)" by (force simp add: NEUT_def)
      moreover
      have "NORMAL (Var a)" by (rule NORMAL_Var)
      ultimately have "(Var a)\ RED \1" by (simp add: CR4_def)
      with a have "App t (Var a) \ RED \2" by simp
      hence "SN (App t (Var a))" using ih_CR1_τ2 by (simp add: CR1_def)
      thus "SN t" by (auto dest: SN_of_FST_of_App)
    qed
    then show "CR1 (\1 \ \2)" unfolding CR1_def by simp
  next
    case 2
    have ih_CR2_τ2: "CR2 \2" by fact
    then show "CR2 (\1 \ \2)" unfolding CR2_def by auto 
  next
    case 3
    have ih_CR1_τ1: "CR1 \1" by fact
    have ih_CR2_τ1: "CR2 \1" by fact
    have ih_CR3_τ2: "CR3 \2" by fact
    show "CR3 (\1 \ \2)" unfolding CR3_def
    proof (simp, intro strip)
      fix t u
      assume a1: "u \ RED \1"
      assume a2: "NEUT t \ CR3_RED t (\1 \ \2)"
      have "SN(u)" using a1 ih_CR1_τ1 by (simp add: CR1_def)
      then show "(App t u)\RED \2" using ih_CR2_τ1 ih_CR3_τ2 a1 a2 by (blast intro: sub_induction)
    qed
  }
qed
   
text ‹
  the next lemma not as simple as on paper, probably because of 
  the stronger double_SN induction 
› 
lemma abs_RED: 
  assumes asm: "\s\RED \. t[x::=s]\RED \"
  shows "Lam [x].t\RED (\\\)"
proof -
  have b1: "SN t" 
  proof -
    have "Var x\RED \"
    proof -
      have "CR4 \" by (simp add: RED_props CR3_implies_CR4)
      moreover
      have "NEUT (Var x)" by (auto simp add: NEUT_def)
      moreover
      have "NORMAL (Var x)" by (auto elim: Beta.cases simp add: NORMAL_def)
      ultimately show "Var x\RED \" by (simp add: CR4_def)
    qed
    then have "t[x::=Var x]\RED \" using asm by simp
    then have "t\RED \" by (simp add: id_subs)
    moreover 
    have "CR1 \" by (simp add: RED_props)
    ultimately show "SN t" by (simp add: CR1_def)
  qed
  show "Lam [x].t\RED (\\\)"
  proof (simp, intro strip)
    fix u
    assume b2: "u\RED \"
    then have b3: "SN u" using RED_props by (auto simp add: CR1_def)
    show "App (Lam [x].t) u \ RED \" using b1 b3 b2 asm
    proof(induct t u rule: double_SN)
      fix t u
      assume ih1: "\t'. \t \\<^sub>\ t'; u\RED \; \s\RED \. t'[x::=s]\RED \\ \ App (Lam [x].t') u \ RED \" 
      assume ih2: "\u'. \u \\<^sub>\ u'; u'\RED \; \s\RED \. t[x::=s]\RED \\ \ App (Lam [x].t) u' \ RED \"
      assume u: "u \ RED \"
      assume t: "\s\RED \. t[x::=s]\RED \"
      have "CR3_RED (App (Lam [x].t) u) \" unfolding CR3_RED_def
      proof(intro strip)
        fix r
        assume red: "App (Lam [x].t) u \\<^sub>\ r"
        moreover
        { assume "\t'. t \\<^sub>\ t' \ r = App (Lam [x].t') u"
          then obtain t' where "t \\<^sub>\ t'" and t': "r = App (Lam [x].t') u"
            by blast
          then have "\s\RED \. t'[x::=s] \ RED \"
            using CR2_def RED_props(2) t beta_subst by blast
          then have "App (Lam [x].t') u\RED \"
            using ‹t ⟶🚫β t'\ u ih1 by blast
          then have "r\RED \" using t' by simp
        }
        moreover
        { assume "\u'. u \\<^sub>\ u' \ r = App (Lam [x].t) u'"
          then obtain u' where "u \\<^sub>\ u'" and u': "r = App (Lam [x].t) u'" by blast
          have "CR2 \"
            by (simp add: RED_props(2))
          then
          have "App (Lam [x].t) u'\RED \"
            using CR2_def ih2 ‹u ⟶🚫β u'\ t u by blast
          then have "r\RED \" using u' by simp
        }
        moreover
        { assume "r = t[x::=u]"
          then have "r\RED \" using u t by auto
        }
        ultimately show "r \ RED \"
          by cases (auto simp: alpha subst_rename lam.inject dest: beta_abs)
          (* one wants to use the strong elimination principle; for this one 
             has to know that x\<sharp>u *)
    qed
    moreover 
    have "NEUT (App (Lam [x].t) u)" unfolding NEUT_def by (auto)
    ultimately show "App (Lam [x].t) u \ RED \"  using RED_props by (simp add: CR3_def)
  qed
qed
qed

abbreviation 
 mapsto :: "(name\lam) list \ name \ lam \ bool" (‹_ maps _ to _› [55,55,55] 55) 
where
 "\ maps x to e \ (lookup \ x) = e"

abbreviation 
  closes :: "(name\lam) list \ (name\ty) list \ bool" (‹_ closes _› [55,55] 55) 
where
  "\ closes \ \ \x T. ((x,T) \ set \ \ (\t. \ maps x to t \ t \ RED T))"

lemma all_RED: 
  assumes a: "\ \ t : \"
  and     b: "\ closes \"
  shows "\ \ RED \"
using a b
proof(nominal_induct  avoiding: θ rule: typing.strong_induct)
  case (t3 a Γ σ t τ θ) 🍋 ‹lambda case›
  have ih: "\\. \ closes ((a,\)#\) \ \ \ RED \" by fact
  have θ_cond: "\ closes \" by fact
  have fresh: "a\\" "a\\" by fact+
  from ih have "\s\RED \. ((a,s)#\) \ RED \" using fresh θ_cond fresh_context by simp
  then have "\s\RED \. \[a::=s] \ RED \" using fresh by (simp add: psubst_subst)
  then have "Lam [a].(\) \ RED (\ \ \)" by (simp only: abs_RED)
  then show "\<(Lam [a].t)> \ RED (\ \ \)" using fresh by simp
qed auto

section ‹identity substitution generated from a context Γ›
fun
  "id" :: "(name\ty) list \ (name\lam) list"
where
  "id [] = []"
| "id ((x,\)#\) = (x,Var x)#(id \)"

lemma id_maps:
  shows "(id \) maps a to (Var a)"
by (induct Γ) (auto)

lemma id_fresh:
  fixes a::"name"
  assumes a: "a\\"
  shows "a\(id \)"
using a
by (induct Γ)
   (auto simp add: fresh_list_nil fresh_list_cons)

lemma id_apply:  
  shows "(id \) = t"
by (nominal_induct t avoiding: Γ rule: lam.strong_induct)
   (auto simp add: id_maps id_fresh)

lemma id_closes:
  shows "(id \) closes \"
  by (metis CR3_implies_CR4 CR4_def NEUT_def NORMAL_Var RED_props(3) id_maps)

lemma typing_implies_RED:
  assumes a: "\ \ t : \"
  shows "t \ RED \"
proof -
  have "(id \)\RED \" 
  proof -
    have "(id \) closes \" by (rule id_closes)
    with a show ?thesis by (rule all_RED)
  qed
  thus"t \ RED \" by (simp add: id_apply)
qed

lemma typing_implies_SN: 
  assumes a: "\ \ t : \"
  shows "SN(t)"
proof -
  from a have "t \ RED \" by (rule typing_implies_RED)
  moreover
  have "CR1 \" by (rule RED_props)
  ultimately show "SN(t)" by (simp add: CR1_def)
qed

end