products/sources/formale Sprachen/Cobol/Test-Suite/SQL P/xop/  image not shown  

Quellcode-Bibliothek

Wann und warum man die Qualität sichern sollte

So läuft die Entwicklung rund

Datei: yts753.cob   Sprache: Isabelle

Untersuchung Isabelle©
(*  Title:      HOL/Proofs/Lambda/Lambda.thy
    Author:     Tobias Nipkow
    Copyright   1995 TU Muenchen
*)

section \<open>Basic definitions of Lambda-calculus\<close>

theory Lambda
imports Main
begin

declare [[syntax_ambiguity_warning = false]]


subsection \<open>Lambda-terms in de Bruijn notation and substitution\<close>

datatype dB =
    Var nat
  | App dB dB (infixl "\" 200)
  | Abs dB

primrec
  lift :: "[dB, nat] => dB"
where
    "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
  | "lift (s \ t) k = lift s k \ lift t k"
  | "lift (Abs s) k = Abs (lift s (k + 1))"

primrec
  subst :: "[dB, dB, nat] => dB"  ("_[_'/_]" [300, 0, 0] 300)
where (* FIXME base names *)
    subst_Var: "(Var i)[s/k] =
      (if k < i then Var (i - 1) else if i = k then s else Var i)"
  | subst_App: "(t \ u)[s/k] = t[s/k] \ u[s/k]"
  | subst_Abs: "(Abs t)[s/k] = Abs (t[lift s 0 / k+1])"

declare subst_Var [simp del]

text \<open>Optimized versions of \<^term>\<open>subst\<close> and \<^term>\<open>lift\<close>.\<close>

primrec
  liftn :: "[nat, dB, nat] => dB"
where
    "liftn n (Var i) k = (if i < k then Var i else Var (i + n))"
  | "liftn n (s \ t) k = liftn n s k \ liftn n t k"
  | "liftn n (Abs s) k = Abs (liftn n s (k + 1))"

primrec
  substn :: "[dB, dB, nat] => dB"
where
    "substn (Var i) s k =
      (if k < i then Var (i - 1) else if i = k then liftn k s 0 else Var i)"
  | "substn (t \ u) s k = substn t s k \ substn u s k"
  | "substn (Abs t) s k = Abs (substn t s (k + 1))"


subsection \<open>Beta-reduction\<close>

inductive beta :: "[dB, dB] => bool"  (infixl "\\<^sub>\" 50)
  where
    beta [simp, intro!]: "Abs s \ t \\<^sub>\ s[t/0]"
  | 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 ==> Abs s \\<^sub>\ Abs t"

abbreviation
  beta_reds :: "[dB, dB] => bool"  (infixl "\\<^sub>\\<^sup>*" 50) where
  "s \\<^sub>\\<^sup>* t == beta\<^sup>*\<^sup>* s t"

inductive_cases beta_cases [elim!]:
  "Var i \\<^sub>\ t"
  "Abs r \\<^sub>\ s"
  "s \ t \\<^sub>\ u"

declare if_not_P [simp] not_less_eq [simp]
  \<comment> \<open>don't add \<open>r_into_rtrancl[intro!]\<close>\<close>


subsection \<open>Congruence rules\<close>

lemma rtrancl_beta_Abs [intro!]:
    "s \\<^sub>\\<^sup>* s' ==> Abs s \\<^sub>\\<^sup>* Abs 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>Substitution-lemmas\<close>

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

lemma subst_gt [simp]: "i < j ==> (Var j)[u/i] = Var (j - 1)"
  by (simp add: subst_Var)

lemma subst_lt [simp]: "j < i ==> (Var j)[u/i] = Var j"
  by (simp add: subst_Var)

lemma lift_lift:
    "i < k + 1 \ lift (lift t i) (Suc k) = lift (lift t k) i"
  by (induct t arbitrary: i k) auto

lemma lift_subst [simp]:
    "j < i + 1 \ lift (t[s/j]) i = (lift t (i + 1)) [lift s i / j]"
  by (induct t arbitrary: i j s)
    (simp_all add: diff_Suc subst_Var lift_lift split: nat.split)

lemma lift_subst_lt:
    "i < j + 1 \ lift (t[s/j]) i = (lift t i) [lift s i / j + 1]"
  by (induct t arbitrary: i j s) (simp_all add: subst_Var lift_lift)

lemma subst_lift [simp]:
    "(lift t k)[s/k] = t"
  by (induct t arbitrary: k s) simp_all

lemma subst_subst:
    "i < j + 1 \ t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"
  by (induct t arbitrary: i j u v)
    (simp_all add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt
      split: nat.split)


subsection \<open>Equivalence proof for optimized substitution\<close>

lemma liftn_0 [simp]: "liftn 0 t k = t"
  by (induct t arbitrary: k) (simp_all add: subst_Var)

lemma liftn_lift [simp]: "liftn (Suc n) t k = lift (liftn n t k) k"
  by (induct t arbitrary: k) (simp_all add: subst_Var)

lemma substn_subst_n [simp]: "substn t s n = t[liftn n s 0 / n]"
  by (induct t arbitrary: n) (simp_all add: subst_Var)

theorem substn_subst_0: "substn t s 0 = t[s/0]"
  by simp


subsection \<open>Preservation theorems\<close>

text \<open>Not used in Church-Rosser proof, but in Strong
  Normalization. \medskip\<close>

theorem subst_preserves_beta [simp]:
    "r \\<^sub>\ s ==> r[t/i] \\<^sub>\ s[t/i]"
  by (induct arbitrary: t i set: beta) (simp_all add: subst_subst [symmetric])

theorem subst_preserves_beta': "r \\<^sub>\\<^sup>* s ==> r[t/i] \\<^sub>\\<^sup>* s[t/i]"
  apply (induct set: rtranclp)
   apply (rule rtranclp.rtrancl_refl)
  apply (erule rtranclp.rtrancl_into_rtrancl)
  apply (erule subst_preserves_beta)
  done

theorem lift_preserves_beta [simp]:
    "r \\<^sub>\ s ==> lift r i \\<^sub>\ lift s i"
  by (induct arbitrary: i set: beta) auto

theorem lift_preserves_beta': "r \\<^sub>\\<^sup>* s ==> lift r i \\<^sub>\\<^sup>* lift s i"
  apply (induct set: rtranclp)
   apply (rule rtranclp.rtrancl_refl)
  apply (erule rtranclp.rtrancl_into_rtrancl)
  apply (erule lift_preserves_beta)
  done

theorem subst_preserves_beta2 [simp]: "r \\<^sub>\ s ==> t[r/i] \\<^sub>\\<^sup>* t[s/i]"
  apply (induct t arbitrary: r s i)
    apply (simp add: subst_Var r_into_rtranclp)
   apply (simp add: rtrancl_beta_App)
  apply (simp add: rtrancl_beta_Abs)
  done

theorem subst_preserves_beta2': "r \\<^sub>\\<^sup>* s ==> t[r/i] \\<^sub>\\<^sup>* t[s/i]"
  apply (induct set: rtranclp)
   apply (rule rtranclp.rtrancl_refl)
  apply (erule rtranclp_trans)
  apply (erule subst_preserves_beta2)
  done

end

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.1Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Begriffe der Konzeptbildung
Was zu einem Entwurf gehört
Begriffe der Konzeptbildung
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff