Quelle Standardization.thy Sprache: Isabelle

(*  Title:      HOL/Nominal/Examples/Standardization.thy
    Author:     Stefan Berghofer and Tobias Nipkow
    Copyright   2005, 2008 TU Muenchen
*)

section \<open>Standardization\<close>

theory Standardization
imports "HOL-Nominal.Nominal"
begin

text \<open>
The proof of the standardization theorem, as well as most of the theorems about
lambda calculus in the following sections, are taken from \<open>HOL/Lambda\<close>.
\<close>

subsection \<open>Lambda terms\<close>

atom_decl name

nominal_datatype lam =
  Var "name"
| App "lam" "lam" (infixl \<open>\<degree>\<close> 200)
| Lam "\name\lam" (\Lam [_]._\ [0, 10] 10)

instantiation lam :: size
begin

nominal_primrec size_lam
where
  "size (Var n) = 0"
| "size (t \ u) = size t + size u + 1"
| "size (Lam [x].t) = size t + 1"
  by (finite_guess | simp add: fresh_nat | fresh_guess)+

instance ..

end

nominal_primrec
  subst :: "lam \ name \ lam \ lam" (\_[_::=_]\ [300, 0, 0] 300)
where
  subst_Var: "(Var x)[y::=s] = (if x=y then s else (Var x))"
| subst_App: "(t\<^sub>1 \ t\<^sub>2)[y::=s] = t\<^sub>1[y::=s] \ t\<^sub>2[y::=s]"
| subst_Lam: "x \ (y, s) \ (Lam [x].t)[y::=s] = (Lam [x].(t[y::=s]))"
  by (finite_guess | simp add: abs_fresh | fresh_guess)+

lemma subst_eqvt [eqvt]:
  "(pi::name prm) \ (t[x::=u]) = (pi \ t)[(pi \ x)::=(pi \ u)]"
  by (nominal_induct t avoiding: x u rule: lam.strong_induct)
     (perm_simp add: fresh_bij)+

lemma subst_rename:
  "y \ t \ ([(y, x)] \ t)[y::=u] = t[x::=u]"
  by (nominal_induct t avoiding: x y u rule: lam.strong_induct)
     (simp_all add: fresh_atm calc_atm abs_fresh)

lemma fresh_subst:
  "(x::name) \ t \ x \ u \ x \ t[y::=u]"
  by (nominal_induct t avoiding: x y u rule: lam.strong_induct)
     (auto simp add: abs_fresh fresh_atm)

lemma fresh_subst':
  "(x::name) \ u \ x \ t[x::=u]"
  by (nominal_induct t avoiding: x u rule: lam.strong_induct)
     (auto simp add: abs_fresh fresh_atm)

lemma subst_forget: "(x::name) \ t \ t[x::=u] = t"
  by (nominal_induct t avoiding: x u rule: lam.strong_induct)
     (auto simp add: abs_fresh fresh_atm)

lemma subst_subst:
  "x \ y \ x \ v \ t[y::=v][x::=u[y::=v]] = t[x::=u][y::=v]"
  by (nominal_induct t avoiding: x y u v rule: lam.strong_induct)
     (auto simp add: fresh_subst subst_forget)

declare subst_Var [simp del]

lemma subst_eq [simp]: "(Var x)[x::=u] = u"
  by (simp add: subst_Var)

lemma subst_neq [simp]: "x \ y \ (Var x)[y::=u] = Var x"
  by (simp add: subst_Var)

inductive beta :: "lam \ lam \ bool" (infixl \\\<^sub>\\ 50)
  where
    beta: "x \ t \ (Lam [x].s) \ t \\<^sub>\ s[x::=t]"
  | appL [simp, intro!]: "s \\<^sub>\ t \ s \ u \\<^sub>\ t \ u"
  | appR [simp, intro!]: "s \\<^sub>\ t \ u \ s \\<^sub>\ u \ t"
  | abs [simp, intro!]: "s \\<^sub>\ t \ (Lam [x].s) \\<^sub>\ (Lam [x].t)"

equivariance beta
nominal_inductive beta
  by (simp_all add: abs_fresh fresh_subst')

lemma better_beta [simp, intro!]: "(Lam [x].s) \ t \\<^sub>\ s[x::=t]"
proof -
  obtain y::name where y: "y \ (x, s, t)"
    by (rule exists_fresh) (rule fin_supp)
  then have "y \ t" by simp
  then have "(Lam [y]. [(y, x)] \ s) \ t \\<^sub>\ ([(y, x)] \ s)[y::=t]"
    by (rule beta)
  moreover from y have "(Lam [x].s) = (Lam [y]. [(y, x)] \ s)"
    by (auto simp add: lam.inject alpha' fresh_prod fresh_atm)
  ultimately show ?thesis using y by (simp add: subst_rename)
qed

abbreviation
  beta_reds :: "lam \ lam \ bool" (infixl \\\<^sub>\\<^sup>*\ 50) where
  "s \\<^sub>\\<^sup>* t \ beta\<^sup>*\<^sup>* s t"

subsection \<open>Application of a term to a list of terms\<close>

abbreviation
  list_application :: "lam \ lam list \ lam" (infixl \\\\ 150) where
  "t \\ ts \ foldl (\) t ts"

lemma apps_eq_tail_conv [iff]: "(r \\ ts = s \\ ts) = (r = s)"
  by (induct ts rule: rev_induct) (auto simp add: lam.inject)

lemma Var_eq_apps_conv [iff]: "(Var m = s \\ ss) = (Var m = s \ ss = [])"
  by (induct ss arbitrary: s) auto

lemma Var_apps_eq_Var_apps_conv [iff]:
    "(Var m \\ rs = Var n \\ ss) = (m = n \ rs = ss)"
proof (induct rs arbitrary: ss rule: rev_induct)
  case Nil then show ?case by (auto simp add: lam.inject)
next
  case (snoc x xs) then show ?case
  by (induct ss rule: rev_induct) (auto simp add: lam.inject)
qed

lemma App_eq_foldl_conv:
  "(r \ s = t \\ ts) =
    (if ts = [] then r \<degree> s = t
    else (\<exists>ss. ts = ss @ [s] \<and> r = t \<degree>\<degree> ss))"
  by (rule rev_exhaust [of ts]) (auto simp: lam.inject)

lemma Abs_eq_apps_conv [iff]:
    "((Lam [x].r) = s \\ ss) = ((Lam [x].r) = s \ ss = [])"
  by (induct ss rule: rev_induct) auto

lemma apps_eq_Abs_conv [iff]: "(s \\ ss = (Lam [x].r)) = (s = (Lam [x].r) \ ss = [])"
  by (induct ss rule: rev_induct) auto

lemma Abs_App_neq_Var_apps [iff]:
    "(Lam [x].s) \ t \ Var n \\ ss"
  by (induct ss arbitrary: s t rule: rev_induct) (auto simp add: lam.inject)

lemma Var_apps_neq_Abs_apps [iff]:
    "Var n \\ ts \ (Lam [x].r) \\ ss"
proof (induct ss arbitrary: ts rule: rev_induct)
  case Nil then show ?case by simp
next
  case (snoc x xs) then show ?case
  by (induct ts rule: rev_induct) (auto simp add: lam.inject)
qed

lemma ex_head_tail:
  "\ts h. t = h \\ ts \ ((\n. h = Var n) \ (\x u. h = (Lam [x].u)))"
proof (induct t rule: lam.induct)
  case (App lam1 lam2)
  then show ?case
    by (metis foldl_Cons foldl_Nil foldl_append)
qed auto

lemma size_apps [simp]:
  "size (r \\ rs) = size r + foldl (+) 0 (map size rs) + length rs"
  by (induct rs rule: rev_induct) auto

lemma lem0: "(0::nat) < k \ m \ n \ m < n + k"
  by simp

lemma subst_map [simp]:
    "(t \\ ts)[x::=u] = t[x::=u] \\ map (\t. t[x::=u]) ts"
  by (induct ts arbitrary: t) simp_all

lemma app_last: "(t \\ ts) \ u = t \\ (ts @ [u])"
  by simp

lemma perm_apps [eqvt]:
  "(pi::name prm) \ (t \\ ts) = ((pi \ t) \\ (pi \ ts))"
  by (induct ts rule: rev_induct) (auto simp add: append_eqvt)

lemma fresh_apps [simp]: "(x::name) \ (t \\ ts) = (x \ t \ x \ ts)"
  by (induct ts rule: rev_induct)
    (auto simp add: fresh_list_append fresh_list_nil fresh_list_cons)

text \<open>A customized induction schema for \<open>\<degree>\<degree>\<close>.\<close>

lemma Apps_lam_induct_aux:
  assumes "\n ts (z::'a::fs_name). (\z. \t \ set ts. P z t) \ P z (Var n \\ ts)"
    and "\x u ts z. x \ z \ (\z. P z u) \ (\z. \t \ set ts. P z t) \ P z ((Lam [x].u) \\ ts)"
  shows "size t = n \ P z t"
proof (induct n arbitrary: t z rule: less_induct)
  case (less n)
  obtain ts h where t: "t = h \\ ts" and D: "(\a. h = Var a) \ (\x u. h = (Lam [x].u))"
    using ex_head_tail [of t] by metis
  show ?case
    using D
  proof (elim exE disjE)
    fix a :: name
    assume h: "h = Var a"
    have "P z t" if "t \ set ts" for z t
    proof -
      have "size t < length ts + fold (+) (map size ts) 0"
        using that
        by (fastforce simp add: sum_list_map_remove1 fold_plus_sum_list_rev)
      then have "size t < size (Var a \\ ts)"
        by simp (simp add: add.commute foldl_conv_fold)
      then show ?thesis
        using h less.hyps less.prems t by blast
    qed
    then show "P z t"
      unfolding t h by (blast intro: assms)
  next
    fix x u
    assume h: "h = (Lam [x].u)"
    obtain y::name where y: "y \ (x, u, z)"
      by (metis exists_fresh' fin_supp)
    then have eq: "(Lam [x].u) = (Lam [y].([(y, x)] \ u))"
      by (metis alpha' fresh_prod lam.inject(3) perm_fresh_fresh)
    show "P z t"
      unfolding t h eq
    proof (intro assms strip)
      show "y \ z"
        by (simp add: y)
      have "size ([(y, x)] \ u) < size ((Lam [x].u) \\ ts)"
        by (simp add: eq)
      then show "P z ([(y, x)] \ u)" for z
        using h less.hyps less.prems t by blast
      show "P z t" if "t\set ts" for z t
      proof -
        have 2: "size t < size ((Lam [x].u) \\ ts)"
          using that
          apply (simp add: eq)
          apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev)
          apply (fastforce simp add: sum_list_map_remove1)
          done
        then show ?thesis
          using h less.hyps less.prems t by blast
      qed
    qed
  qed
qed

theorem Apps_lam_induct:
  assumes "\n ts (z::'a::fs_name). (\z. \t \ set ts. P z t) \ P z (Var n \\ ts)"
    and "\x u ts z. x \ z \ (\z. P z u) \ (\z. \t \ set ts. P z t) \ P z ((Lam [x].u) \\ ts)"
  shows "P z t"
  using Apps_lam_induct_aux [of P] assms by blast

subsection \<open>Congruence rules\<close>

lemma apps_preserves_beta [simp]:
    "r \\<^sub>\ s \ r \\ ss \\<^sub>\ s \\ ss"
  by (induct ss rule: rev_induct) auto

lemma rtrancl_beta_Abs [intro!]:
    "s \\<^sub>\\<^sup>* s' \ (Lam [x].s) \\<^sub>\\<^sup>* (Lam [x].s')"
  by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

lemma rtrancl_beta_AppL:
    "s \\<^sub>\\<^sup>* s' \ s \ t \\<^sub>\\<^sup>* s' \ t"
  by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

lemma rtrancl_beta_AppR:
    "t \\<^sub>\\<^sup>* t' \ s \ t \\<^sub>\\<^sup>* s \ t'"
  by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

lemma rtrancl_beta_App [intro]:
    "s \\<^sub>\\<^sup>* s' \ t \\<^sub>\\<^sup>* t' \ s \ t \\<^sub>\\<^sup>* s' \ t'"
  by (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR intro: rtranclp_trans)

subsection \<open>Lifting an order to lists of elements\<close>

definition
  step1 :: "('a \ 'a \ bool) \ 'a list \ 'a list \ bool" where
  "step1 r \
    (\<lambda>ys xs. \<exists>us z z' vs. xs = us @ z # vs \<and> r z' z \<and> ys =
      us @ z' # vs)"

lemma not_Nil_step1 [iff]: "\ step1 r [] xs"
  by (simp add: step1_def)

lemma not_step1_Nil [iff]: "\ step1 r xs []"
  by (simp add: step1_def)

lemma Cons_step1_Cons [iff]:
    "step1 r (y # ys) (x # xs) \ r y x \ xs = ys \ x = y \ step1 r ys xs"
  apply (rule )
   apply (smt (verit, ccfv_SIG) append_eq_Cons_conv list.inject step1_def)
  by (metis append_Cons append_Nil step1_def)

lemma Cons_step1E [elim!]:
  assumes "step1 r ys (x # xs)"
    and "\y. ys = y # xs \ r y x \ R"
    and "\zs. ys = x # zs \ step1 r zs xs \ R"
  shows R
  by (metis Cons_step1_Cons assms list.exhaust not_Nil_step1)

lemma append_step1I:
  "step1 r ys xs \ vs = us \ ys = xs \ step1 r vs us
    \<Longrightarrow> step1 r (ys @ vs) (xs @ us)"
  by (smt (verit) append_Cons append_assoc step1_def)

lemma Snoc_step1_SnocD:
  assumes "step1 r (ys @ [y]) (xs @ [x])"
  shows "(step1 r ys xs \ y = x \ ys = xs \ r y x)"
  using assms
    apply (clarsimp simp: step1_def)
  by (metis butlast.simps(2) butlast_append butlast_snoc last.simps last_appendR list.simps(3))

subsection \<open>Lifting beta-reduction to lists\<close>

abbreviation
  list_beta :: "lam list \ lam list \ bool" (infixl \[\\<^sub>\]\<^sub>1\ 50) where
  "rs [\\<^sub>\]\<^sub>1 ss \ step1 beta rs ss"

lemma head_Var_reduction:
  "Var n \\ rs \\<^sub>\ v \ \ss. rs [\\<^sub>\]\<^sub>1 ss \ v = Var n \\ ss"
proof (induct u \<equiv> "Var n \<degree>\<degree> rs" v arbitrary: rs set: beta)
  case (appL s t u)
  then show ?case
    by (smt (verit, best) App_eq_foldl_conv app_last append_step1I lam.distinct(1))
next
  case (appR s t u)
  then show ?case
    by (smt (verit, ccfv_SIG) App_eq_foldl_conv Cons_step1_Cons app_last append_step1I lam.distinct(1))
qed auto

lemma apps_betasE [case_names appL appR beta, consumes 1]:
  assumes major: "r \\ rs \\<^sub>\ s"
    and cases: "\r'. r \\<^sub>\ r' \ s = r' \\ rs \ R"
      "\rs'. rs [\\<^sub>\]\<^sub>1 rs' \ s = r \\ rs' \ R"
      "\t u us. (x \ r \ r = (Lam [x].t) \ rs = u # us \ s = t[x::=u] \\ us) \ R"
  shows R
proof -
  note [[simproc del: defined_all]]
  from major have
   "(\r'. r \\<^sub>\ r' \ s = r' \\ rs) \
    (\<exists>rs'. rs [\<rightarrow>\<^sub>\<beta>]\<^sub>1 rs' \<and> s = r \<degree>\<degree> rs') \<or>
    (\<exists>t u us. x \<sharp> r \<longrightarrow> r = (Lam [x].t) \<and> rs = u # us \<and> s = t[x::=u] \<degree>\<degree> us)"
  proof (nominal_induct u \<equiv> "r \<degree>\<degree> rs" s avoiding: x r rs rule: beta.strong_induct)
    case (beta y t s)
    then show ?case
      apply (simp add: App_eq_foldl_conv split: if_split_asm)
       apply blast
      by (metis (no_types, lifting) abs_fresh(1) alpha' lam.fresh(3) lam.inject(3) subst_rename)
  next
    case (appL s t u)
    then show ?case
      apply (simp add: App_eq_foldl_conv split: if_split_asm)
      apply blast
      by (smt (verit) append_Cons append_step1I snoc_eq_iff_butlast)
  next
    case (appR s t u)
    then show ?case
      apply (simp add: App_eq_foldl_conv step1_def split: if_split_asm)
      apply force
      by (metis snoc_eq_iff_butlast)
  next
    case (abs s t x)
    then show ?case
      by blast
  qed
  with cases show ?thesis by blast
qed

lemma apps_preserves_betas [simp]:
    "rs [\\<^sub>\]\<^sub>1 ss \ r \\ rs \\<^sub>\ r \\ ss"
proof (induct rs arbitrary: ss rule: rev_induct)
  case Nil
  then show ?case by simp
next
  case (snoc x ts)
  then show ?case
    apply (simp add: step1_def)
    by (smt (verit) appR app_last apps_preserves_beta foldl_Cons foldl_append)
qed

subsection \<open>Standard reduction relation\<close>

text \<open>
Based on lecture notes by Ralph Matthes,
original proof idea due to Ralph Loader.
\<close>

declare listrel_mono [mono_set]

lemma listrelp_eqvt [eqvt]:
  fixes f :: "'a::pt_name \ 'b::pt_name \ bool"
  assumes xy: "listrelp f (x::'a::pt_name list) y"
  shows "listrelp ((pi::name prm) \ f) (pi \ x) (pi \ y)" using xy
  by induct (simp_all add: listrelp.intros perm_app [symmetric])

inductive
  sred :: "lam \ lam \ bool" (infixl \\\<^sub>s\ 50)
  and sredlist :: "lam list \ lam list \ bool" (infixl \[\\<^sub>s]\ 50)
where
  "s [\\<^sub>s] t \ listrelp (\\<^sub>s) s t"
| Var: "rs [\\<^sub>s] rs' \ Var x \\ rs \\<^sub>s Var x \\ rs'"
| Abs: "x \ (ss, ss') \ r \\<^sub>s r' \ ss [\\<^sub>s] ss' \ (Lam [x].r) \\ ss \\<^sub>s (Lam [x].r') \\ ss'"
| Beta: "x \ (s, ss, t) \ r[x::=s] \\ ss \\<^sub>s t \ (Lam [x].r) \ s \\ ss \\<^sub>s t"

equivariance sred
nominal_inductive sred
  by (simp add: abs_fresh)+

lemma better_sred_Abs:
  assumes H1: "r \\<^sub>s r'"
  and H2: "ss [\\<^sub>s] ss'"
  shows "(Lam [x].r) \\ ss \\<^sub>s (Lam [x].r') \\ ss'"
proof -
  obtain y::name where y: "y \ (x, r, r', ss, ss')"
    by (rule exists_fresh) (rule fin_supp)
  then have "y \ (ss, ss')" by simp
  moreover from H1 have "[(y, x)] \ (r \\<^sub>s r')" by (rule perm_boolI)
  then have "([(y, x)] \ r) \\<^sub>s ([(y, x)] \ r')" by (simp add: eqvts)
  ultimately have "(Lam [y]. [(y, x)] \ r) \\ ss \\<^sub>s (Lam [y]. [(y, x)] \ r') \\ ss'" using H2
    by (rule sred.Abs)
  moreover from y have "(Lam [x].r) = (Lam [y]. [(y, x)] \ r)"
    by (auto simp add: lam.inject alpha' fresh_prod fresh_atm)
  moreover from y have "(Lam [x].r') = (Lam [y]. [(y, x)] \ r')"
    by (auto simp add: lam.inject alpha' fresh_prod fresh_atm)
  ultimately show ?thesis by simp
qed

lemma better_sred_Beta:
  assumes H: "r[x::=s] \\ ss \\<^sub>s t"
  shows "(Lam [x].r) \ s \\ ss \\<^sub>s t"
proof -
  obtain y::name where y: "y \ (x, r, s, ss, t)"
    by (rule exists_fresh) (rule fin_supp)
  then have "y \ (s, ss, t)" by simp
  moreover from y H have "([(y, x)] \ r)[y::=s] \\ ss \\<^sub>s t"
    by (simp add: subst_rename)
  ultimately have "(Lam [y].[(y, x)] \ r) \ s \\ ss \\<^sub>s t"
    by (rule sred.Beta)
  moreover from y have "(Lam [x].r) = (Lam [y]. [(y, x)] \ r)"
    by (auto simp add: lam.inject alpha' fresh_prod fresh_atm)
  ultimately show ?thesis by simp
qed

lemmas better_sred_intros = sred.Var better_sred_Abs better_sred_Beta

lemma refl_listrelp: "\x\set xs. R x x \ listrelp R xs xs"
  by (induct xs) (auto intro: listrelp.intros)

lemma refl_sred: "t \\<^sub>s t"
  by (nominal_induct t rule: Apps_lam_induct) (auto intro: refl_listrelp better_sred_intros)

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 \\<^sub>s r'" and s: "s \\<^sub>s s'"
  shows "r \ s \\<^sub>s r' \ s'" using r
proof induct
  case (Var rs rs' x)
  then have "rs [\\<^sub>s] rs'" by (rule listrelp_conj1)
  moreover have "[s] [\\<^sub>s] [s']" by (iprover intro: s listrelp.intros)
  ultimately have "rs @ [s] [\\<^sub>s] rs' @ [s']" by (rule listrelp_app)
  hence "Var x \\ (rs @ [s]) \\<^sub>s Var x \\ (rs' @ [s'])" by (rule sred.Var)
  thus ?case by (simp only: app_last)
next
  case (Abs x ss ss' r r')
  from Abs(4) have "ss [\\<^sub>s] ss'" by (rule listrelp_conj1)
  moreover have "[s] [\\<^sub>s] [s']" by (iprover intro: s listrelp.intros)
  ultimately have "ss @ [s] [\\<^sub>s] ss' @ [s']" by (rule listrelp_app)
  with \<open>r \<rightarrow>\<^sub>s r'\<close> have "(Lam [x].r) \<degree>\<degree> (ss @ [s]) \<rightarrow>\<^sub>s (Lam [x].r') \<degree>\<degree> (ss' @ [s'])"
    by (rule better_sred_Abs)
  thus ?case by (simp only: app_last)
next
  case (Beta x u ss t r)
  hence "r[x::=u] \\ (ss @ [s]) \\<^sub>s t \ s'" by (simp only: app_last)
  hence "(Lam [x].r) \ u \\ (ss @ [s]) \\<^sub>s t \ s'" by (rule better_sred_Beta)
  thus ?case by (simp only: app_last)
qed

lemma lemma1':
  assumes ts: "ts [\\<^sub>s] ts'"
  shows "r \\<^sub>s r' \ r \\ ts \\<^sub>s r' \\ ts'" using ts
  by (induct arbitrary: r r') (auto intro: lemma1)

lemma listrelp_betas:
  assumes ts: "listrelp (\\<^sub>\\<^sup>*) ts ts'"
  shows "\t t'. t \\<^sub>\\<^sup>* t' \ t \\ ts \\<^sub>\\<^sup>* t' \\ ts'" using ts
  by induct auto

lemma lemma2:
  assumes t: "t \\<^sub>s u"
  shows "t \\<^sub>\\<^sup>* u" using t
  by induct (auto dest: listrelp_conj2
    intro: listrelp_betas apps_preserves_beta converse_rtranclp_into_rtranclp)

lemma lemma3:
  assumes r: "r \\<^sub>s r'"
  shows "s \\<^sub>s s' \ r[x::=s] \\<^sub>s r'[x::=s']" using r
proof (nominal_induct avoiding: x s s' rule: sred.strong_induct)
  case (Var rs rs' y)
  hence "map (\t. t[x::=s]) rs [\\<^sub>s] map (\t. t[x::=s']) rs'"
    by induct (auto intro: listrelp.intros Var)
  moreover have "Var y[x::=s] \\<^sub>s Var y[x::=s']"
    by (cases "y = x") (auto simp add: Var intro: refl_sred)
  ultimately show ?case by simp (rule lemma1')
next
  case (Abs y ss ss' r r')
  then have "r[x::=s] \\<^sub>s r'[x::=s']" by fast
  moreover from Abs(8) \<open>s \<rightarrow>\<^sub>s s'\<close> have "map (\<lambda>t. t[x::=s]) ss [\<rightarrow>\<^sub>s] map (\<lambda>t. t[x::=s']) ss'"
    by induct (auto intro: listrelp.intros Abs)
  ultimately show ?case using Abs(6) \<open>y \<sharp> x\<close> \<open>y \<sharp> s\<close> \<open>y \<sharp> s'\<close>
    by simp (rule better_sred_Abs)
next
  case (Beta y u ss t r)
  thus ?case by (auto simp add: subst_subst fresh_atm intro: better_sred_Beta)
qed

lemma lemma4_aux:
  assumes rs: "listrelp (\t u. t \\<^sub>s u \ (\r. u \\<^sub>\ r \ t \\<^sub>s r)) rs rs'"
  shows "rs' [\\<^sub>\]\<^sub>1 ss \ rs [\\<^sub>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 \\<^sub>\ y' \ ys' = ys \ y' = y \ ys [\\<^sub>\]\<^sub>1 ys'" by simp
    hence "x # xs [\\<^sub>s] y' # ys'"
    proof
      assume H: "y \\<^sub>\ y' \ ys' = ys"
      with Cons' have "x \\<^sub>s y'" by blast
      moreover from Cons' have "xs [\\<^sub>s] ys" by (iprover dest: listrelp_conj1)
      ultimately have "x # xs [\\<^sub>s] y' # ys" by (rule listrelp.Cons)
      with H show ?thesis by simp
    next
      assume H: "y' = y \ ys [\\<^sub>\]\<^sub>1 ys'"
      with Cons' have "x \\<^sub>s y'" by blast
      moreover from H have "xs [\\<^sub>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 \\<^sub>s r'"
  shows "r' \\<^sub>\ r'' \ r \\<^sub>s r''" using r
proof (nominal_induct avoiding: r'' rule: sred.strong_induct)
  case (Var rs rs' x)
  then obtain ss where rs: "rs' [\\<^sub>\]\<^sub>1 ss" and r'': "r'' = Var x \\ ss"
    by (blast dest: head_Var_reduction)
  from Var(1) [simplified] rs have "rs [\\<^sub>s] ss" by (rule lemma4_aux)
  hence "Var x \\ rs \\<^sub>s Var x \\ ss" by (rule sred.Var)
  with r'' show ?case by simp
next
  case (Abs x ss ss' r r')
  from \<open>(Lam [x].r') \<degree>\<degree> ss' \<rightarrow>\<^sub>\<beta> r''\<close> show ?case
  proof (cases rule: apps_betasE [where x=x])
    case (appL s)
    then obtain r''' where s: "s = (Lam [x].r''')" and r''': "r' \\<^sub>\ r'''" using \x \ r''\
      by (cases rule: beta.strong_cases) (auto simp add: abs_fresh lam.inject alpha)
    from r''' have "r \\<^sub>s r'''" by (blast intro: Abs)
    moreover from Abs have "ss [\\<^sub>s] ss'" by (iprover dest: listrelp_conj1)
    ultimately have "(Lam [x].r) \\ ss \\<^sub>s (Lam [x].r''') \\ ss'" by (rule better_sred_Abs)
    with appL s show "(Lam [x].r) \\ ss \\<^sub>s r''" by simp
  next
    case (appR rs')
    from Abs(6) [simplified] \<open>ss' [\<rightarrow>\<^sub>\<beta>]\<^sub>1 rs'\<close>
    have "ss [\\<^sub>s] rs'" by (rule lemma4_aux)
    with \<open>r \<rightarrow>\<^sub>s r'\<close> have "(Lam [x].r) \<degree>\<degree> ss \<rightarrow>\<^sub>s (Lam [x].r') \<degree>\<degree> rs'" by (rule better_sred_Abs)
    with appR show "(Lam [x].r) \\ ss \\<^sub>s r''" by simp
  next
    case (beta t u' us')
    then have Lam_eq: "(Lam [x].r') = (Lam [x].t)" and ss': "ss' = u' # us'"
      and r'': "r'' = t[x::=u'] \\ us'"
      by (simp_all add: abs_fresh)
    from Abs(6) ss' obtain u us where
      ss: "ss = u # us" and u: "u \\<^sub>s u'" and us: "us [\\<^sub>s] us'"
      by cases (auto dest!: listrelp_conj1)
    have "r[x::=u] \\<^sub>s r'[x::=u']" using \r \\<^sub>s r'\ and u by (rule lemma3)
    with us have "r[x::=u] \\ us \\<^sub>s r'[x::=u'] \\ us'" by (rule lemma1')
    hence "(Lam [x].r) \ u \\ us \\<^sub>s r'[x::=u'] \\ us'" by (rule better_sred_Beta)
    with ss r'' Lam_eq show "(Lam [x].r) \\ ss \\<^sub>s r''" by (simp add: lam.inject alpha)
  qed
next
  case (Beta x s ss t r)
  show ?case
    by (rule better_sred_Beta) (rule Beta)+
qed

lemma rtrancl_beta_sred:
  assumes r: "r \\<^sub>\\<^sup>* r'"
  shows "r \\<^sub>s r'" using r
  by induct (iprover intro: refl_sred lemma4)+

subsection \<open>Terms in normal form\<close>

lemma listsp_eqvt [eqvt]:
  assumes xs: "listsp p (xs::'a::pt_name list)"
  shows "listsp ((pi::name prm) \ p) (pi \ xs)" using xs
by induction (use perm_app in force)+

inductive NF :: "lam \ bool"
where
  App: "listsp NF ts \ NF (Var x \\ ts)"
| Abs: "NF t \ NF (Lam [x].t)"

equivariance NF
nominal_inductive NF
  by (simp add: abs_fresh)

lemma Abs_NF:
  assumes NF: "NF ((Lam [x].t) \\ ts)"
  shows "ts = []" using NF
  by (metis Abs_eq_apps_conv NF.cases Var_apps_neq_Abs_apps)

text \<open>
\<^term>\<open>NF\<close> characterizes exactly the terms that are in normal form.
\<close>

lemma NF_eq: "NF t = (\t'. \ t \\<^sub>\ t')"
proof
  assume H: "NF t"
  show "\t'. \ t \\<^sub>\ t'"
  proof
    fix t'
    from H show "\ t \\<^sub>\ t'"
    proof (nominal_induct avoiding: t' rule: NF.strong_induct)
      case (App ts t)
      show ?case
      proof
        assume "Var t \\ ts \\<^sub>\ t'"
        then obtain rs where "ts [\\<^sub>\]\<^sub>1 rs"
          by (iprover dest: head_Var_reduction)
        with App show False
          by (induct rs arbitrary: ts) (auto del: in_listspD)
      qed
    next
      case (Abs t x)
      show ?case
      proof
        assume "(Lam [x].t) \\<^sub>\ t'"
        then show False using Abs
          by (cases rule: beta.strong_cases) (auto simp add: abs_fresh lam.inject alpha)
      qed
    qed
  qed
next
  assume H: "\t'. \ t \\<^sub>\ t'"
  then show "NF t"
  proof (nominal_induct t rule: Apps_lam_induct)
    case (1 n ts)
    then have "\ts'. \ ts [\\<^sub>\]\<^sub>1 ts'"
      by (iprover intro: apps_preserves_betas)
    with 1(1) have "listsp NF ts"
      by (induct ts) (auto simp add: in_listsp_conv_set)
    then show ?case by (rule NF.App)
  next
    case (2 x u ts)
    show ?case
    proof (cases ts)
      case Nil thus ?thesis by (metis 2 NF.Abs abs foldl_Nil)
    next
      case (Cons r rs)
      have "(Lam [x].u) \ r \\<^sub>\ u[x::=r]" ..
      then have "(Lam [x].u) \ r \\ rs \\<^sub>\ u[x::=r] \\ rs"
        by (rule apps_preserves_beta)
      with Cons have "(Lam [x].u) \\ ts \\<^sub>\ u[x::=r] \\ rs"
        by simp
      with 2 show ?thesis by iprover
    qed
  qed
qed

subsection \<open>Leftmost reduction and weakly normalizing terms\<close>

inductive
  lred :: "lam \ lam \ bool" (infixl \\\<^sub>l\ 50)
  and lredlist :: "lam list \ lam list \ bool" (infixl \[\\<^sub>l]\ 50)
where
  "s [\\<^sub>l] t \ listrelp (\\<^sub>l) s t"
| Var: "rs [\\<^sub>l] rs' \ Var x \\ rs \\<^sub>l Var x \\ rs'"
| Abs: "r \\<^sub>l r' \ (Lam [x].r) \\<^sub>l (Lam [x].r')"
| Beta: "r[x::=s] \\ ss \\<^sub>l t \ (Lam [x].r) \ s \\ ss \\<^sub>l t"

lemma lred_imp_sred:
  assumes lred: "s \\<^sub>l t"
  shows "s \\<^sub>s t" using lred
proof induct
  case (Var rs rs' x)
  then have "rs [\\<^sub>s] rs'"
    by induct (iprover intro: listrelp.intros)+
  then show ?case by (rule sred.Var)
next
  case (Abs r r' x)
  from \<open>r \<rightarrow>\<^sub>s r'\<close>
  have "(Lam [x].r) \\ [] \\<^sub>s (Lam [x].r') \\ []" using listrelp.Nil
    by (rule better_sred_Abs)
  then show ?case by simp
next
  case (Beta r x s ss t)
  from \<open>r[x::=s] \<degree>\<degree> ss \<rightarrow>\<^sub>s t\<close>
  show ?case by (rule better_sred_Beta)
qed

inductive WN :: "lam \ bool"
  where
    Var: "listsp WN rs \ WN (Var n \\ rs)"
  | Lambda: "WN r \ WN (Lam [x].r)"
  | Beta: "WN ((r[x::=s]) \\ ss) \ WN (((Lam [x].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 \\<^sub>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)+

lemma lemma6:
  assumes wn: "WN r"
  shows "\r'. r \\<^sub>l r'" using wn
proof induct
  case (Var rs n)
  then have "\rs'. rs [\\<^sub>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 \\<^sub>s r'"
  shows "NF r' \ r \\<^sub>l r'" using r
proof induct
  case (Var rs rs' x)
  from \<open>NF (Var x \<degree>\<degree> rs')\<close> have "listsp NF rs'"
    by cases simp_all
  with Var(1) have "rs [\\<^sub>l] rs'"
  proof induct
    case Nil
    show ?case by (rule listrelp.Nil)
  next
    case (Cons x y xs ys)
    hence "x \\<^sub>l y" and "xs [\\<^sub>l] ys" by (auto del: in_listspD)
    thus ?case by (rule listrelp.Cons)
  qed
  thus ?case by (rule lred.Var)
next
  case (Abs x ss ss' r r')
  from \<open>NF ((Lam [x].r') \<degree>\<degree> ss')\<close>
  have ss': "ss' = []" by (rule Abs_NF)
  from Abs(4) have ss: "ss = []" using ss'
    by cases simp_all
  from ss' Abs have "NF (Lam [x].r')" by simp
  hence "NF r'" by (cases rule: NF.strong_cases) (auto simp add: abs_fresh lam.inject alpha)
  with Abs have "r \\<^sub>l r'" by simp
  hence "(Lam [x].r) \\<^sub>l (Lam [x].r')" by (rule lred.Abs)
  with ss ss' show ?case by simp
next
  case (Beta x s ss t r)
  hence "r[x::=s] \\ ss \\<^sub>l t" by simp
  thus ?case by (rule lred.Beta)
qed

lemma WN_eq: "WN t = (\t'. t \\<^sub>\\<^sup>* t' \ NF t')"
proof
  assume "WN t"
  then have "\t'. t \\<^sub>l t'" by (rule lemma6)
  then obtain t' where t': "t \\<^sub>l t'" ..
  then have NF: "NF t'" by (rule lemma5)
  from t' have "t \\<^sub>s t'" by (rule lred_imp_sred)
  then have "t \\<^sub>\\<^sup>* t'" by (rule lemma2)
  with NF show "\t'. t \\<^sub>\\<^sup>* t' \ NF t'" by iprover
next
  assume "\t'. t \\<^sub>\\<^sup>* t' \ NF t'"
  then obtain t' where t': "t \\<^sub>\\<^sup>* t'" and NF: "NF t'"
    by iprover
  from t' have "t \\<^sub>s t'" by (rule rtrancl_beta_sred)
  then have "t \\<^sub>l t'" using NF by (rule lemma7)
  then show "WN t" by (rule lemma5)
qed

end

quality100%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.