Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Standardization.thy Sprache: Isabelle

Original von: 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 "\" 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"
  apply finite_guess+
  apply (rule TrueI)+
  apply (simp add: fresh_nat)
  apply fresh_guess+
  done

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]))"
  apply(finite_guess)+
  apply(rule TrueI)+
  apply(simp add: abs_fresh)
  apply(fresh_guess)+
  done

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)"
  apply (induct rs arbitrary: ss rule: rev_induct)
   apply (simp add: lam.inject)
   apply blast
  apply (induct_tac ss rule: rev_induct)
   apply (auto simp add: lam.inject)
  done

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))"
  apply (rule_tac xs = ts in rev_exhaust)
   apply (auto simp add: lam.inject)
  done

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"
  apply (induct ss arbitrary: ts rule: rev_induct)
   apply simp
  apply (induct_tac ts rule: rev_induct)
   apply (auto simp add: lam.inject)
  done

lemma ex_head_tail:
  "\ts h. t = h \\ ts \ ((\n. h = Var n) \ (\x u. h = (Lam [x].u)))"
  apply (induct t rule: lam.induct)
    apply (metis foldl_Nil)
   apply (metis foldl_Cons foldl_Nil foldl_append)
  apply (metis foldl_Nil)
  done

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 lem:
  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"
  apply (induct n arbitrary: t z rule: nat_less_induct)
  apply (cut_tac t = t in ex_head_tail)
  apply clarify
  apply (erule disjE)
   apply clarify
   apply (rule assms)
   apply clarify
   apply (erule allE, erule impE)
    prefer 2
    apply (erule allE, erule impE, rule refl, erule spec)
    apply simp
    apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev)
    apply (fastforce simp add: sum_list_map_remove1)
  apply clarify
  apply (subgoal_tac "\y::name. y \ (x, u, z)")
   prefer 2
   apply (blast intro: exists_fresh' fin_supp)
  apply (erule exE)
  apply (subgoal_tac "(Lam [x].u) = (Lam [y].([(y, x)] \ u))")
  prefer 2
  apply (auto simp add: lam.inject alpha' fresh_prod fresh_atm)[]
  apply (simp (no_asm_simp))
  apply (rule assms)
  apply (simp add: fresh_prod)
   apply (erule allE, erule impE)
    prefer 2
    apply (erule allE, erule impE, rule refl, erule spec)
   apply simp
  apply clarify
  apply (erule allE, erule impE)
   prefer 2
   apply blast
  apply simp
  apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev)
  apply (fastforce simp add: sum_list_map_remove1)
  done

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"
  apply (rule_tac t = t and z = z in lem)
    prefer 3
    apply (rule refl)
    using assms apply blast+
  done

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"
  apply (unfold step1_def)
  apply blast
  done

lemma not_step1_Nil [iff]: "\ step1 r xs []"
  apply (unfold step1_def)
  apply blast
  done

lemma Cons_step1_Cons [iff]:
    "(step1 r (y # ys) (x # xs)) =
      (r y x \<and> xs = ys \<or> x = y \<and> step1 r ys xs)"
  apply (unfold step1_def)
  apply (rule iffI)
   apply (erule exE)
   apply (rename_tac ts)
   apply (case_tac ts)
    apply fastforce
   apply force
  apply (erule disjE)
   apply blast
  apply (blast intro: Cons_eq_appendI)
  done

lemma append_step1I:
  "step1 r ys xs \ vs = us \ ys = xs \ step1 r vs us
    \<Longrightarrow> step1 r (ys @ vs) (xs @ us)"
  apply (unfold step1_def)
  apply auto
   apply blast
  apply (blast intro: append_eq_appendI)
  done

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
  using assms
  apply (cases ys)
   apply (simp add: step1_def)
  apply blast
  done

lemma Snoc_step1_SnocD:
  "step1 r (ys @ [y]) (xs @ [x])
    \<Longrightarrow> (step1 r ys xs \<and> y = x \<or> ys = xs \<and> r y x)"
  apply (unfold step1_def)
  apply (clarify del: disjCI)
  apply (rename_tac vs)
  apply (rule_tac xs = vs in rev_exhaust)
   apply force
  apply simp
  apply blast
  done

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"
  apply (induct u \<equiv> "Var n \<degree>\<degree> rs" v arbitrary: rs set: beta)
     apply simp
    apply (rule_tac xs = rs in rev_exhaust)
     apply simp
    apply (atomize, force intro: append_step1I iff: lam.inject)
   apply (rule_tac xs = rs in rev_exhaust)
    apply simp
    apply (auto 0 3 intro: disjI2 [THEN append_step1I] simp add: lam.inject)
  done

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 -
  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)"
    supply [[simproc del: defined_all]]
    apply (nominal_induct u \<equiv> "r \<degree>\<degree> rs" s avoiding: x r rs rule: beta.strong_induct)
    apply (simp add: App_eq_foldl_conv)
    apply (split if_split_asm)
    apply simp
    apply blast
    apply simp
    apply (rule impI)+
    apply (rule disjI2)
    apply (rule disjI2)
    apply (subgoal_tac "r = [(xa, x)] \ (Lam [x].s)")
    prefer 2
    apply (simp add: perm_fresh_fresh)
    apply (drule conjunct1)
    apply (subgoal_tac "r = (Lam [xa]. [(xa, x)] \ s)")
    prefer 2
    apply (simp add: calc_atm)
    apply (thin_tac "r = _")
    apply simp
    apply (rule exI)
    apply (rule conjI)
    apply (rule refl)
    apply (simp add: abs_fresh fresh_atm fresh_left calc_atm subst_rename)
      apply (drule App_eq_foldl_conv [THEN iffD1])
      apply (split if_split_asm)
       apply simp
       apply blast
      apply (force intro!: disjI1 [THEN append_step1I] simp add: fresh_list_append)
     apply (drule App_eq_foldl_conv [THEN iffD1])
     apply (split if_split_asm)
      apply simp
      apply blast
     apply (clarify, auto 0 3 intro!: exI intro: append_step1I)
    done
  with cases show ?thesis by blast
qed

lemma apps_preserves_betas [simp]:
    "rs [\\<^sub>\]\<^sub>1 ss \ r \\ rs \\<^sub>\ r \\ ss"
  apply (induct rs arbitrary: ss rule: rev_induct)
   apply simp
  apply simp
  apply (rule_tac xs = ss in rev_exhaust)
   apply simp
  apply simp
  apply (drule Snoc_step1_SnocD)
  apply blast
  done

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
  apply induct
  apply simp
  apply simp
  apply (rule listsp.intros)
  apply (drule_tac pi=pi in perm_boolI)
  apply perm_simp
  apply assumption
  done

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
proof cases
  case (App us i)
  thus ?thesis by (simp add: Var_apps_neq_Abs_apps [THEN not_sym])
next
  case (Abs u)
  thus ?thesis by simp
qed

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

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.