Quelle  Standardization.thy

(*  Title:      HOL/Proofs/Lambda/Standardization.thy
  Author: Stefan Berghofer
  Copyright 2005 TU Muenchen
*)

section ‹Standardization›

theory Standardization
imports NormalForm
begin

text ‹
 Based on lecture notes by Ralph Matthes 🍋‹"Matthes-ESSLLI2000"›,
 original proof idea due to Ralph Loader 🍋‹Loader1998›.
 ›


subsection ‹Standard reduction relation›

declare listrel_mono [mono_set]

inductive
  sred :: "dB ==> dB ==> bool"  (infixl ‹→🪙s› 50)
  and sredlist :: "dB list ==> dB list ==> bool"  (infixl ‹[→🪙s]› 50)
where
  "s [→🪙s] t ≡ listrelp (→🪙s) s t"
| Var: "rs [→🪙s] rs' ==> Var x 🍋🍋 rs →🪙s Var x 🍋🍋 rs'"
| Abs: "r →🪙s r' ==> ss [→🪙s] ss' ==> Abs r 🍋🍋 ss →🪙s Abs r' 🍋🍋 ss'"
| Beta: "r[s/0] 🍋🍋 ss →🪙s t ==> Abs r 🍋 s 🍋🍋 ss →🪙s t"

lemma refl_listrelp: "∀x∈set xs. R x x ==> listrelp R xs xs"
  by (induct xs) (auto intro: listrelp.intros)

lemma refl_sred: "t →🪙s t"
  by (induct t rule: Apps_dB_induct) (auto intro: refl_listrelp sred.intros)

lemma refl_sreds: "ts [→🪙s] ts"
  by (simp add: refl_sred refl_listrelp)

lemma listrelp_conj1: "listrelp (λx y. R x y ∧ S x y) x y ==> listrelp R x y"
  by (erule listrelp.induct) (auto intro: listrelp.intros)

lemma listrelp_conj2: "listrelp (λx y. R x y ∧ S x y) x y ==> listrelp S x y"
  by (erule listrelp.induct) (auto intro: listrelp.intros)

lemma listrelp_app:
  assumes xsys: "listrelp R xs ys"
  shows "listrelp R xs' ys' ==> listrelp R (xs @ xs') (ys @ ys')" using xsys
  by (induct arbitrary: xs' ys') (auto intro: listrelp.intros)

lemma lemma1:
  assumes r: "r →🪙s r'" and s: "s →🪙s s'"
  shows "r 🍋 s →🪙s r' 🍋 s'" using r
proof induct
  case (Var rs rs' x)
  then have "rs [→🪙s] rs'" by (rule listrelp_conj1)
  moreover have "[s] [→🪙s] [s']" by (iprover intro: s listrelp.intros)
  ultimately have "rs @ [s] [→🪙s] rs' @ [s']" by (rule listrelp_app)
  hence "Var x 🍋🍋 (rs @ [s]) →🪙s Var x 🍋🍋 (rs' @ [s'])" by (rule sred.Var)
  thus ?case by (simp only: app_last)
next
  case (Abs r r' ss ss')
  from Abs(3) have "ss [→🪙s] ss'" by (rule listrelp_conj1)
  moreover have "[s] [→🪙s] [s']" by (iprover intro: s listrelp.intros)
  ultimately have "ss @ [s] [→🪙s] ss' @ [s']" by (rule listrelp_app)
  with ‹r →🪙s r'› have "Abs r 🍋🍋 (ss @ [s]) →🪙s Abs r' 🍋🍋 (ss' @ [s'])"
    by (rule sred.Abs)
  thus ?case by (simp only: app_last)
next
  case (Beta r u ss t)
  hence "r[u/0] 🍋🍋 (ss @ [s]) →🪙s t 🍋 s'" by (simp only: app_last)
  hence "Abs r 🍋 u 🍋🍋 (ss @ [s]) →🪙s t 🍋 s'" by (rule sred.Beta)
  thus ?case by (simp only: app_last)
qed

lemma lemma1':
  assumes ts: "ts [→🪙s] ts'"
  shows "r →🪙s r' ==> r 🍋🍋 ts →🪙s r' 🍋🍋 ts'" using ts
  by (induct arbitrary: r r') (auto intro: lemma1)

lemma lemma2_1:
  assumes beta: "t →🪙β u"
  shows "t →🪙s u" using beta
proof induct
  case (beta s t)
  have "Abs s 🍋 t 🍋🍋 [] →🪙s s[t/0] 🍋🍋 []" by (iprover intro: sred.Beta refl_sred)
  thus ?case by simp
next
  case (appL s t u)
  thus ?case by (iprover intro: lemma1 refl_sred)
next
  case (appR s t u)
  thus ?case by (iprover intro: lemma1 refl_sred)
next
  case (abs s t)
  hence "Abs s 🍋🍋 [] →🪙s Abs t 🍋🍋 []" by (iprover intro: sred.Abs listrelp.Nil)
  thus ?case by simp
qed

lemma listrelp_betas:
  assumes ts: "listrelp (→🪙β🪙*) ts ts'"
  shows "∧t t'. t →🪙β🪙* t' ==> t 🍋🍋 ts →🪙β🪙* t' 🍋🍋 ts'" using ts
  by induct auto

lemma lemma2_2:
  assumes t: "t →🪙s u"
  shows "t →🪙β🪙* u" using t
  by induct (auto dest: listrelp_conj2
    intro: listrelp_betas apps_preserves_beta converse_rtranclp_into_rtranclp)

lemma sred_lift:
  assumes s: "s →🪙s t"
  shows "lift s i →🪙s lift t i" using s
proof (induct arbitrary: i)
  case (Var rs rs' x)
  hence "map (λt. lift t i) rs [→🪙s] map (λt. lift t i) rs'"
    by induct (auto intro: listrelp.intros)
  thus ?case by (cases "x < i") (auto intro: sred.Var)
next
  case (Abs r r' ss ss')
  from Abs(3) have "map (λt. lift t i) ss [→🪙s] map (λt. lift t i) ss'"
    by induct (auto intro: listrelp.intros)
  thus ?case by (auto intro: sred.Abs Abs)
next
  case (Beta r s ss t)
  thus ?case by (auto intro: sred.Beta)
qed

lemma lemma3:
  assumes r: "r →🪙s r'"
  shows "s →🪙s s' ==> r[s/x] →🪙s r'[s'/x]" using r
proof (induct arbitrary: s s' x)
  case (Var rs rs' y)
  hence "map (λt. t[s/x]) rs [→🪙s] map (λt. t[s'/x]) rs'"
    by induct (auto intro: listrelp.intros Var)
  moreover have "Var y[s/x] →🪙s Var y[s'/x]"
  proof (cases "y < x")
    case True thus ?thesis by simp (rule refl_sred)
  next
    case False
    thus ?thesis
      by (cases "y = x") (auto simp add: Var intro: refl_sred)
  qed
  ultimately show ?case by simp (rule lemma1')
next
  case (Abs r r' ss ss')
  from Abs(4) have "lift s 0 →🪙s lift s' 0" by (rule sred_lift)
  hence "r[lift s 0/Suc x] →🪙s r'[lift s' 0/Suc x]" by (fast intro: Abs.hyps)
  moreover from Abs(3) have "map (λt. t[s/x]) ss [→🪙s] map (λt. t[s'/x]) ss'"
    by induct (auto intro: listrelp.intros Abs)
  ultimately show ?case by simp (rule sred.Abs)
next
  case (Beta r u ss t)
  thus ?case by (auto simp add: subst_subst intro: sred.Beta)
qed

lemma lemma4_aux:
  assumes rs: "listrelp (λt u. t →🪙s u ∧ (∀r. u →🪙β r ⟶ t →🪙s r)) rs rs'"
  shows "rs' => ss ==> rs [→🪙s] ss" using rs
proof (induct arbitrary: ss)
  case Nil
  thus ?case by cases (auto intro: listrelp.Nil)
next
  case (Cons x y xs ys)
  note Cons' = Cons
  show ?case
  proof (cases ss)
    case Nil with Cons show ?thesis by simp
  next
    case (Cons y' ys')
    hence ss: "ss = y' # ys'" by simp
    from Cons Cons' have "y →🪙β y' ∧ ys' = ys ∨ y' = y ∧ ys => ys'" by simp
    hence "x # xs [→🪙s] y' # ys'"
    proof
      assume H: "y →🪙β y' ∧ ys' = ys"
      with Cons' have "x →🪙s y'" by blast
      moreover from Cons' have "xs [→🪙s] ys" by (iprover dest: listrelp_conj1)
      ultimately have "x # xs [→🪙s] y' # ys" by (rule listrelp.Cons)
      with H show ?thesis by simp
    next
      assume H: "y' = y ∧ ys => ys'"
      with Cons' have "x →🪙s y'" by blast
      moreover from H have "xs [→🪙s] ys'" by (blast intro: Cons')
      ultimately show ?thesis by (rule listrelp.Cons)
    qed
    with ss show ?thesis by simp
  qed
qed

lemma lemma4:
  assumes r: "r →🪙s r'"
  shows "r' →🪙β r'' ==> r →🪙s r''" using r
proof (induct arbitrary: r'')
  case (Var rs rs' x)
  then obtain ss where rs: "rs' => ss" and r'': "r'' = Var x 🍋🍋 ss"
    by (blast dest: head_Var_reduction)
  from Var(1) rs have "rs [→🪙s] ss" by (rule lemma4_aux)
  hence "Var x 🍋🍋 rs →🪙s Var x 🍋🍋 ss" by (rule sred.Var)
  with r'' show ?case by simp
next
  case (Abs r r' ss ss')
  from ‹Abs r' 🍋🍋 ss' →🪙β r''› show ?case
  proof
    fix s
    assume r'': "r'' = s 🍋🍋 ss'"
    assume "Abs r' →🪙β s"
    then obtain r''' where s: "s = Abs r'''" and r''': "r' →🪙β r'''" by cases auto
    from r''' have "r →🪙s r'''" by (blast intro: Abs)
    moreover from Abs have "ss [→🪙s] ss'" by (iprover dest: listrelp_conj1)
    ultimately have "Abs r 🍋🍋 ss →🪙s Abs r''' 🍋🍋 ss'" by (rule sred.Abs)
    with r'' s show "Abs r 🍋🍋 ss →🪙s r''" by simp
  next
    fix rs'
    assume "ss' => rs'"
    with Abs(3) have "ss [→🪙s] rs'" by (rule lemma4_aux)
    with ‹r →🪙s r'› have "Abs r 🍋🍋 ss →🪙s Abs r' 🍋🍋 rs'" by (rule sred.Abs)
    moreover assume "r'' = Abs r' 🍋🍋 rs'"
    ultimately show "Abs r 🍋🍋 ss →🪙s r''" by simp
  next
    fix t u' us'
    assume "ss' = u' # us'"
    with Abs(3) obtain u us where
      ss: "ss = u # us" and u: "u →🪙s u'" and us: "us [→🪙s] us'"
      by cases (auto dest!: listrelp_conj1)
    have "r[u/0] →🪙s r'[u'/0]" using Abs(1) and u by (rule lemma3)
    with us have "r[u/0] 🍋🍋 us →🪙s r'[u'/0] 🍋🍋 us'" by (rule lemma1')
    hence "Abs r 🍋 u 🍋🍋 us →🪙s r'[u'/0] 🍋🍋 us'" by (rule sred.Beta)
    moreover assume "Abs r' = Abs t" and "r'' = t[u'/0] 🍋🍋 us'"
    ultimately show "Abs r 🍋🍋 ss →🪙s r''" using ss by simp
  qed
next
  case (Beta r s ss t)
  show ?case
    by (rule sred.Beta) (rule Beta)+
qed

lemma rtrancl_beta_sred:
  assumes r: "r →🪙β🪙* r'"
  shows "r →🪙s r'" using r
  by induct (iprover intro: refl_sred lemma4)+


subsection ‹Leftmost reduction and weakly normalizing terms›

inductive
  lred :: "dB ==> dB ==> bool"  (infixl ‹→🪙l› 50)
  and lredlist :: "dB list ==> dB list ==> bool"  (infixl ‹[→🪙l]› 50)
where
  "s [→🪙l] t ≡ listrelp (→🪙l) s t"
| Var: "rs [→🪙l] rs' ==> Var x 🍋🍋 rs →🪙l Var x 🍋🍋 rs'"
| Abs: "r →🪙l r' ==> Abs r →🪙l Abs r'"
| Beta: "r[s/0] 🍋🍋 ss →🪙l t ==> Abs r 🍋 s 🍋🍋 ss →🪙l t"

lemma lred_imp_sred:
  assumes lred: "s →🪙l t"
  shows "s →🪙s t" using lred
proof induct
  case (Var rs rs' x)
  then have "rs [→🪙s] rs'"
    by induct (iprover intro: listrelp.intros)+
  then show ?case by (rule sred.Var)
next
  case (Abs r r')
  from ‹r →🪙s r'›
  have "Abs r 🍋🍋 [] →🪙s Abs r' 🍋🍋 []" using listrelp.Nil
    by (rule sred.Abs)
  then show ?case by simp
next
  case (Beta r s ss t)
  from ‹r[s/0] 🍋🍋 ss →🪙s t›
  show ?case by (rule sred.Beta)
qed

inductive WN :: "dB => bool"
  where
    Var: "listsp WN rs ==> WN (Var n 🍋🍋 rs)"
  | Lambda: "WN r ==> WN (Abs r)"
  | Beta: "WN ((r[s/0]) 🍋🍋 ss) ==> WN ((Abs r 🍋 s) 🍋🍋 ss)"

lemma listrelp_imp_listsp1:
  assumes H: "listrelp (λx y. P x) xs ys"
  shows "listsp P xs" using H
  by induct auto

lemma listrelp_imp_listsp2:
  assumes H: "listrelp (λx y. P y) xs ys"
  shows "listsp P ys" using H
  by induct auto

lemma lemma5:
  assumes lred: "r →🪙l r'"
  shows "WN r" and "NF r'" using lred
  by induct
    (iprover dest: listrelp_conj1 listrelp_conj2
     listrelp_imp_listsp1 listrelp_imp_listsp2 intro: WN.intros
     NF.intros [simplified listall_listsp_eq])+

lemma lemma6:
  assumes wn: "WN r"
  shows "∃r'. r →🪙l r'" using wn
proof induct
  case (Var rs n)
  then have "∃rs'. rs [→🪙l] rs'"
    by induct (iprover intro: listrelp.intros)+
  then show ?case by (iprover intro: lred.Var)
qed (iprover intro: lred.intros)+

lemma lemma7:
  assumes r: "r →🪙s r'"
  shows "NF r' ==> r →🪙l r'" using r
proof induct
  case (Var rs rs' x)
  from ‹NF (Var x 🍋🍋 rs')› have "listall NF rs'"
    by cases simp_all
  with Var(1) have "rs [→🪙l] rs'"
  proof induct
    case Nil
    show ?case by (rule listrelp.Nil)
  next
    case (Cons x y xs ys)
    hence "x →🪙l y" and "xs [→🪙l] ys" by simp_all
    thus ?case by (rule listrelp.Cons)
  qed
  thus ?case by (rule lred.Var)
next
  case (Abs r r' ss ss')
  from ‹NF (Abs r' 🍋🍋 ss')›
  have ss': "ss' = []" by (rule Abs_NF)
  from Abs(3) have ss: "ss = []" using ss'
    by cases simp_all
  from ss' Abs have "NF (Abs r')" by simp
  hence "NF r'" by cases simp_all
  with Abs have "r →🪙l r'" by simp
  hence "Abs r →🪙l Abs r'" by (rule lred.Abs)
  with ss ss' show ?case by simp
next
  case (Beta r s ss t)
  hence "r[s/0] 🍋🍋 ss →🪙l t" by simp
  thus ?case by (rule lred.Beta)
qed

lemma WN_eq: "WN t = (∃t'. t →🪙β🪙* t' ∧ NF t')"
proof
  assume "WN t"
  then have "∃t'. t →🪙l t'" by (rule lemma6)
  then obtain t' where t': "t →🪙l t'" ..
  then have NF: "NF t'" by (rule lemma5)
  from t' have "t →🪙s t'" by (rule lred_imp_sred)
  then have "t →🪙β🪙* t'" by (rule lemma2_2)
  with NF show "∃t'. t →🪙β🪙* t' ∧ NF t'" by iprover
next
  assume "∃t'. t →🪙β🪙* t' ∧ NF t'"
  then obtain t' where t': "t →🪙β🪙* t'" and NF: "NF t'"
    by iprover
  from t' have "t →🪙s t'" by (rule rtrancl_beta_sred)
  then have "t →🪙l t'" using NF by (rule lemma7)
  then show "WN t" by (rule lemma5)
qed

end