Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/HOL/Proofs/Lambda/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 11 kB

Quelle StrongNorm.thy Sprache: Isabelle

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

section \<open>Strong normalization for simply-typed lambda calculus\<close>

theory StrongNorm imports LambdaType InductTermi begin

text \<open>
Formalization by Stefan Berghofer. Partly based on a paper proof by
Felix Joachimski and Ralph Matthes \<^cite>\<open>"Matthes-Joachimski-AML"\<close>.
\<close>

subsection \<open>Properties of \<open>IT\<close>\<close>

lemma lift_IT [intro!]: "IT t \ IT (lift t i)"
  apply (induct arbitrary: i set: IT)
    apply (simp (no_asm))
    apply (rule conjI)
     apply
      (rule impI,
       rule IT.Var,
       erule listsp.induct,
       simp (no_asm),
       simp (no_asm),
       rule listsp.Cons,
       blast,
       assumption)+
     apply auto
   done

lemma lifts_IT: "listsp IT ts \ listsp IT (map (\t. lift t 0) ts)"
  by (induct ts) auto

lemma subst_Var_IT: "IT r \ IT (r[Var i/j])"
  apply (induct arbitrary: i j set: IT)
    txt \<open>Case \<^term>\<open>Var\<close>:\<close>
    apply (simp (no_asm) add: subst_Var)
    apply
    ((rule conjI impI)+,
      rule IT.Var,
      erule listsp.induct,
      simp (no_asm),
      simp (no_asm),
      rule listsp.Cons,
      fast,
      assumption)+
   txt \<open>Case \<^term>\<open>Lambda\<close>:\<close>
   apply atomize
   apply simp
   apply (rule IT.Lambda)
   apply fast
  txt \<open>Case \<^term>\<open>Beta\<close>:\<close>
  apply atomize
  apply (simp (no_asm_use) add: subst_subst [symmetric])
  apply (rule IT.Beta)
   apply auto
  done

lemma Var_IT: "IT (Var n)"
  apply (subgoal_tac "IT (Var n \\ [])")
   apply simp
  apply (rule IT.Var)
  apply (rule listsp.Nil)
  done

lemma app_Var_IT: "IT t \ IT (t \ Var i)"
  apply (induct set: IT)
    apply (subst app_last)
    apply (rule IT.Var)
    apply simp
    apply (rule listsp.Cons)
     apply (rule Var_IT)
    apply (rule listsp.Nil)
   apply (rule IT.Beta [where ?ss = "[]", unfolded foldl_Nil [THEN eq_reflection]])
    apply (erule subst_Var_IT)
   apply (rule Var_IT)
  apply (subst app_last)
  apply (rule IT.Beta)
   apply (subst app_last [symmetric])
   apply assumption
  apply assumption
  done

subsection \<open>Well-typed substitution preserves termination\<close>

lemma subst_type_IT:
  "\t e T u i. IT t \ e\i:U\ \ t : T \
    IT u \<Longrightarrow> e \<turnstile> u : U \<Longrightarrow> IT (t[u/i])"
  (is "PROP ?P U" is "\t e T u i. _ \ PROP ?Q t e T u i U")
proof (induct U)
  fix T t
  assume MI1: "\T1 T2. T = T1 \ T2 \ PROP ?P T1"
  assume MI2: "\T1 T2. T = T1 \ T2 \ PROP ?P T2"
  assume "IT t"
  thus "\e T' u i. PROP ?Q t e T' u i T"
  proof induct
    fix e T' u i
    assume uIT: "IT u"
    assume uT: "e \ u : T"
    {
      case (Var rs n e1 T'1 u1 i1)
      assume nT: "e\i:T\ \ Var n \\ rs : T'"
      let ?ty = "\t. \T'. e\i:T\ \ t : T'"
      let ?R = "\t. \e T' u i.
        e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow> IT u \<longrightarrow> e \<turnstile> u : T \<longrightarrow> IT (t[u/i])"
      show "IT ((Var n \\ rs)[u/i])"
      proof (cases "n = i")
        case True
        show ?thesis
        proof (cases rs)
          case Nil
          with uIT True show ?thesis by simp
        next
          case (Cons a as)
          with nT have "e\i:T\ \ Var n \ a \\ as : T'" by simp
          then obtain Ts
              where headT: "e\i:T\ \ Var n \ a : Ts \ T'"
              and argsT: "e\i:T\ \ as : Ts"
            by (rule list_app_typeE)
          from headT obtain T''
              where varT: "e\i:T\ \ Var n : T'' \ Ts \ T'"
              and argT: "e\i:T\ \ a : T''"
            by cases simp_all
          from varT True have T: "T = T'' \ Ts \ T'"
            by cases auto
          with uT have uT': "e \ u : T'' \ Ts \ T'" by simp
          from T have "IT ((Var 0 \\ map (\t. lift t 0)
            (map (\<lambda>t. t[u/i]) as))[(u \<degree> a[u/i])/0])"
          proof (rule MI2)
            from T have "IT ((lift u 0 \ Var 0)[a[u/i]/0])"
            proof (rule MI1)
              have "IT (lift u 0)" by (rule lift_IT [OF uIT])
              thus "IT (lift u 0 \ Var 0)" by (rule app_Var_IT)
              show "e\0:T''\ \ lift u 0 \ Var 0 : Ts \ T'"
              proof (rule typing.App)
                show "e\0:T''\ \ lift u 0 : T'' \ Ts \ T'"
                  by (rule lift_type) (rule uT')
                show "e\0:T''\ \ Var 0 : T''"
                  by (rule typing.Var) simp
              qed
              from Var have "?R a" by cases (simp_all add: Cons)
              with argT uIT uT show "IT (a[u/i])" by simp
              from argT uT show "e \ a[u/i] : T''"
                by (rule subst_lemma) simp
            qed
            thus "IT (u \ a[u/i])" by simp
            from Var have "listsp ?R as"
              by cases (simp_all add: Cons)
            moreover from argsT have "listsp ?ty as"
              by (rule lists_typings)
            ultimately have "listsp (\t. ?R t \ ?ty t) as"
              by simp
            hence "listsp IT (map (\t. lift t 0) (map (\t. t[u/i]) as))"
              (is "listsp IT (?ls as)")
            proof induct
              case Nil
              show ?case by fastforce
            next
              case (Cons b bs)
              hence I: "?R b" by simp
              from Cons obtain U where "e\i:T\ \ b : U" by fast
              with uT uIT I have "IT (b[u/i])" by simp
              hence "IT (lift (b[u/i]) 0)" by (rule lift_IT)
              hence "listsp IT (lift (b[u/i]) 0 # ?ls bs)"
                by (rule listsp.Cons) (rule Cons)
              thus ?case by simp
            qed
            thus "IT (Var 0 \\ ?ls as)" by (rule IT.Var)
            have "e\0:Ts \ T'\ \ Var 0 : Ts \ T'"
              by (rule typing.Var) simp
            moreover from uT argsT have "e \ map (\t. t[u/i]) as : Ts"
              by (rule substs_lemma)
            hence "e\0:Ts \ T'\ \ ?ls as : Ts"
              by (rule lift_types)
            ultimately show "e\0:Ts \ T'\ \ Var 0 \\ ?ls as : T'"
              by (rule list_app_typeI)
            from argT uT have "e \ a[u/i] : T''"
              by (rule subst_lemma) (rule refl)
            with uT' show "e \ u \ a[u/i] : Ts \ T'"
              by (rule typing.App)
          qed
          with Cons True show ?thesis
            by (simp add: comp_def)
        qed
      next
        case False
        from Var have "listsp ?R rs" by simp
        moreover from nT obtain Ts where "e\i:T\ \ rs : Ts"
          by (rule list_app_typeE)
        hence "listsp ?ty rs" by (rule lists_typings)
        ultimately have "listsp (\t. ?R t \ ?ty t) rs"
          by simp
        hence "listsp IT (map (\x. x[u/i]) rs)"
        proof induct
          case Nil
          show ?case by fastforce
        next
          case (Cons a as)
          hence I: "?R a" by simp
          from Cons obtain U where "e\i:T\ \ a : U" by fast
          with uT uIT I have "IT (a[u/i])" by simp
          hence "listsp IT (a[u/i] # map (\t. t[u/i]) as)"
            by (rule listsp.Cons) (rule Cons)
          thus ?case by simp
        qed
        with False show ?thesis by (auto simp add: subst_Var)
      qed
    next
      case (Lambda r e1 T'1 u1 i1)
      assume "e\i:T\ \ Abs r : T'"
        and "\e T' u i. PROP ?Q r e T' u i T"
      with uIT uT show "IT (Abs r[u/i])"
        by fastforce
    next
      case (Beta r a as e1 T'1 u1 i1)
      assume T: "e\i:T\ \ Abs r \ a \\ as : T'"
      assume SI1: "\e T' u i. PROP ?Q (r[a/0] \\ as) e T' u i T"
      assume SI2: "\e T' u i. PROP ?Q a e T' u i T"
      have "IT (Abs (r[lift u 0/Suc i]) \ a[u/i] \\ map (\t. t[u/i]) as)"
      proof (rule IT.Beta)
        have "Abs r \ a \\ as \\<^sub>\ r[a/0] \\ as"
          by (rule apps_preserves_beta) (rule beta.beta)
        with T have "e\i:T\ \ r[a/0] \\ as : T'"
          by (rule subject_reduction)
        hence "IT ((r[a/0] \\ as)[u/i])"
          using uIT uT by (rule SI1)
        thus "IT (r[lift u 0/Suc i][a[u/i]/0] \\ map (\t. t[u/i]) as)"
          by (simp del: subst_map add: subst_subst subst_map [symmetric])
        from T obtain U where "e\i:T\ \ Abs r \ a : U"
          by (rule list_app_typeE) fast
        then obtain T'' where "e\i:T\ \ a : T''" by cases simp_all
        thus "IT (a[u/i])" using uIT uT by (rule SI2)
      qed
      thus "IT ((Abs r \ a \\ as)[u/i])" by simp
    }
  qed
qed

subsection \<open>Well-typed terms are strongly normalizing\<close>

lemma type_implies_IT:
  assumes "e \ t : T"
  shows "IT t"
  using assms
proof induct
  case Var
  show ?case by (rule Var_IT)
next
  case Abs
  show ?case by (rule IT.Lambda) (rule Abs)
next
  case (App e s T U t)
  have "IT ((Var 0 \ lift t 0)[s/0])"
  proof (rule subst_type_IT)
    have "IT (lift t 0)" using \<open>IT t\<close> by (rule lift_IT)
    hence "listsp IT [lift t 0]" by (rule listsp.Cons) (rule listsp.Nil)
    hence "IT (Var 0 \\ [lift t 0])" by (rule IT.Var)
    also have "Var 0 \\ [lift t 0] = Var 0 \ lift t 0" by simp
    finally show "IT \" .
    have "e\0:T \ U\ \ Var 0 : T \ U"
      by (rule typing.Var) simp
    moreover have "e\0:T \ U\ \ lift t 0 : T"
      by (rule lift_type) (rule App.hyps)
    ultimately show "e\0:T \ U\ \ Var 0 \ lift t 0 : U"
      by (rule typing.App)
    show "IT s" by fact
    show "e \ s : T \ U" by fact
  qed
  thus ?case by simp
qed

theorem type_implies_termi: "e \ t : T \ termip beta t"
proof -
  assume "e \ t : T"
  hence "IT t" by (rule type_implies_IT)
  thus ?thesis by (rule IT_implies_termi)
qed

end

quality100%

¤ Dauer der Verarbeitung: 0.15 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.