Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Receiver.thy Sprache: Isabelle

Original von: Isabelle^©

theory SN
imports Lam_Funs
begin

text \<open>Strong Normalisation proof from the Proofs and Types book\<close>

section \<open>Beta Reduction\<close>

lemma subst_rename:
  assumes a: "c\t1"
  shows "t1[a::=t2] = ([(c,a)]\t1)[c::=t2]"
using a
by (nominal_induct t1 avoiding: a c t2 rule: lam.strong_induct)
   (auto simp add: calc_atm fresh_atm abs_fresh)

lemma forget:
  assumes a: "a\t1"
  shows "t1[a::=t2] = t1"
  using a
by (nominal_induct t1 avoiding: a t2 rule: lam.strong_induct)
   (auto simp add: abs_fresh fresh_atm)

lemma fresh_fact:
  fixes a::"name"
  assumes a: "a\t1" "a\t2"
  shows "a\t1[b::=t2]"
using a
by (nominal_induct t1 avoiding: a b t2 rule: lam.strong_induct)
   (auto simp add: abs_fresh fresh_atm)

lemma fresh_fact':
  fixes a::"name"
  assumes a: "a\t2"
  shows "a\t1[a::=t2]"
using a
by (nominal_induct t1 avoiding: a t2 rule: lam.strong_induct)
   (auto simp add: abs_fresh fresh_atm)

lemma subst_lemma:
  assumes a: "x\y"
  and     b: "x\L"
  shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
using a b
by (nominal_induct M avoiding: x y N L rule: lam.strong_induct)
   (auto simp add: fresh_fact forget)

lemma id_subs:
  shows "t[x::=Var x] = t"
  by (nominal_induct t avoiding: x rule: lam.strong_induct)
     (simp_all add: fresh_atm)

lemma lookup_fresh:
  fixes z::"name"
  assumes "z\\" "z\x"
  shows "z\ lookup \ x"
using assms
by (induct rule: lookup.induct) (auto simp add: fresh_list_cons)

lemma lookup_fresh':
  assumes "z\\"
  shows "lookup \ z = Var z"
using assms
by (induct rule: lookup.induct)
   (auto simp add: fresh_list_cons fresh_prod fresh_atm)

lemma psubst_subst:
  assumes h:"c\\"
  shows "(\)[c::=s] = ((c,s)#\)"
  using h
by (nominal_induct t avoiding: \<theta> c s rule: lam.strong_induct)
   (auto simp add: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh')

inductive
  Beta :: "lam\lam\bool" (" _ \\<^sub>\ _" [80,80] 80)
where
  b1[intro!]: "s1 \\<^sub>\ s2 \ App s1 t \\<^sub>\ App s2 t"
| b2[intro!]: "s1\\<^sub>\s2 \ App t s1 \\<^sub>\ App t s2"
| b3[intro!]: "s1\\<^sub>\s2 \ Lam [a].s1 \\<^sub>\ Lam [a].s2"
| b4[intro!]: "a\s2 \ App (Lam [a].s1) s2\\<^sub>\ (s1[a::=s2])"

equivariance Beta

nominal_inductive Beta
  by (simp_all add: abs_fresh fresh_fact')

lemma beta_preserves_fresh:
  fixes a::"name"
  assumes a: "t\\<^sub>\ s"
  shows "a\t \ a\s"
using a
apply(nominal_induct t s avoiding: a rule: Beta.strong_induct)
apply(auto simp add: abs_fresh fresh_fact fresh_atm)
done

lemma beta_abs:
  assumes a: "Lam [a].t\\<^sub>\ t'"
  shows "\t''. t'=Lam [a].t'' \ t\\<^sub>\ t''"
proof -
  have "a\Lam [a].t" by (simp add: abs_fresh)
  with a have "a\t'" by (simp add: beta_preserves_fresh)
  with a show ?thesis
    by (cases rule: Beta.strong_cases[where a="a" and aa="a"])
       (auto simp add: lam.inject abs_fresh alpha)
qed

lemma beta_subst:
  assumes a: "M \\<^sub>\ M'"
  shows "M[x::=N]\\<^sub>\ M'[x::=N]"
using a
by (nominal_induct M M' avoiding: x N rule: Beta.strong_induct)
   (auto simp add: fresh_atm subst_lemma fresh_fact)

section \<open>types\<close>

nominal_datatype ty =
    TVar "nat"
  | TArr "ty" "ty" (infix "\" 200)

lemma fresh_ty:
  fixes a ::"name"
  and   \<tau>  ::"ty"
  shows "a\\"
by (nominal_induct \<tau> rule: ty.strong_induct)
   (auto simp add: fresh_nat)

(* valid contexts *)

inductive
  valid :: "(name\ty) list \ bool"
where
  v1[intro]: "valid []"
| v2[intro]: "\valid \;a\\\\ valid ((a,\)#\)"

equivariance valid

(* typing judgements *)

lemma fresh_context:
  fixes  \<Gamma> :: "(name\<times>ty)list"
  and    a :: "name"
  assumes a: "a\\"
  shows "\(\\::ty. (a,\)\set \)"
using a
by (induct \<Gamma>)
   (auto simp add: fresh_prod fresh_list_cons fresh_atm)

inductive
  typing :: "(name\ty) list\lam\ty\bool" ("_ \ _ : _" [60,60,60] 60)
where
  t1[intro]: "\valid \; (a,\)\set \\ \ \ \ Var a : \"
| t2[intro]: "\\ \ t1 : \\\; \ \ t2 : \\ \ \ \ App t1 t2 : \"
| t3[intro]: "\a\\;((a,\)#\) \ t : \\ \ \ \ Lam [a].t : \\\"

equivariance typing

nominal_inductive typing
  by (simp_all add: abs_fresh fresh_ty)

subsection \<open>a fact about beta\<close>

definition "NORMAL" :: "lam \ bool" where
  "NORMAL t \ \(\t'. t\\<^sub>\ t')"

lemma NORMAL_Var:
  shows "NORMAL (Var a)"
proof -
  { assume "\t'. (Var a) \\<^sub>\ t'"
    then obtain t' where "(Var a) \\<^sub>\ t'" by blast
    hence False by (cases) (auto)
  }
  thus "NORMAL (Var a)" by (auto simp add: NORMAL_def)
qed

text \<open>Inductive version of Strong Normalisation\<close>
inductive
  SN :: "lam \ bool"
where
  SN_intro: "(\t'. t \\<^sub>\ t' \ SN t') \ SN t"

lemma SN_preserved:
  assumes a: "SN t1" "t1\\<^sub>\ t2"
  shows "SN t2"
using a
by (cases) (auto)

lemma double_SN_aux:
  assumes a: "SN a"
  and b: "SN b"
  and hyp: "\x z.
    \<lbrakk>\<And>y. x \<longrightarrow>\<^sub>\<beta> y \<Longrightarrow> SN y; \<And>y. x \<longrightarrow>\<^sub>\<beta> y \<Longrightarrow> P y z;
     \<And>u. z \<longrightarrow>\<^sub>\<beta> u \<Longrightarrow> SN u; \<And>u. z \<longrightarrow>\<^sub>\<beta> u \<Longrightarrow> P x u\<rbrakk> \<Longrightarrow> P x z"
  shows "P a b"
proof -
  from a
  have r: "\b. SN b \ P a b"
  proof (induct a rule: SN.SN.induct)
    case (SN_intro x)
    note SNI' = SN_intro
    have "SN b" by fact
    thus ?case
    proof (induct b rule: SN.SN.induct)
      case (SN_intro y)
      show ?case
        apply (rule hyp)
        apply (erule SNI')
        apply (erule SNI')
        apply (rule SN.SN_intro)
        apply (erule SN_intro)+
        done
    qed
  qed
  from b show ?thesis by (rule r)
qed

lemma double_SN[consumes 2]:
  assumes a: "SN a"
  and     b: "SN b"
  and     c: "\x z. \\y. x \\<^sub>\ y \ P y z; \u. z \\<^sub>\ u \ P x u\ \ P x z"
  shows "P a b"
using a b c
apply(rule_tac double_SN_aux)
apply(assumption)+
apply(blast)
done

section \<open>Candidates\<close>

nominal_primrec
  RED :: "ty \ lam set"
where
  "RED (TVar X) = {t. SN(t)}"
| "RED (\\\) = {t. \u. (u\RED \ \ (App t u)\RED \)}"
by (rule TrueI)+

text \<open>neutral terms\<close>
definition NEUT :: "lam \ bool" where
  "NEUT t \ (\a. t = Var a) \ (\t1 t2. t = App t1 t2)"

(* a slight hack to get the first element of applications *)
(* this is needed to get (SN t) from SN (App t s)         *)
inductive
  FST :: "lam\lam\bool" (" _ \ _" [80,80] 80)
where
  fst[intro!]:  "(App t s) \ t"

nominal_primrec
  fst_app_aux::"lam\lam option"
where
  "fst_app_aux (Var a) = None"
| "fst_app_aux (App t1 t2) = Some t1"
| "fst_app_aux (Lam [x].t) = None"
apply(finite_guess)+
apply(rule TrueI)+
apply(simp add: fresh_none)
apply(fresh_guess)+
done

definition
  fst_app_def[simp]: "fst_app t = the (fst_app_aux t)"

lemma SN_of_FST_of_App:
  assumes a: "SN (App t s)"
  shows "SN (fst_app (App t s))"
using a
proof -
  from a have "\z. (App t s \ z) \ SN z"
    by (induct rule: SN.SN.induct)
       (blast elim: FST.cases intro: SN_intro)
  then have "SN t" by blast
  then show "SN (fst_app (App t s))" by simp
qed

section \<open>Candidates\<close>

definition "CR1" :: "ty \ bool" where
  "CR1 \ \ \t. (t\RED \ \ SN t)"

definition "CR2" :: "ty \ bool" where
  "CR2 \ \ \t t'. (t\RED \ \ t \\<^sub>\ t') \ t'\RED \"

definition "CR3_RED" :: "lam \ ty \ bool" where
  "CR3_RED t \ \ \t'. t\\<^sub>\ t' \ t'\RED \"

definition "CR3" :: "ty \ bool" where
  "CR3 \ \ \t. (NEUT t \ CR3_RED t \) \ t\RED \"

definition "CR4" :: "ty \ bool" where
  "CR4 \ \ \t. (NEUT t \ NORMAL t) \t\RED \"

lemma CR3_implies_CR4:
  assumes a: "CR3 \"
  shows "CR4 \"
using a by (auto simp add: CR3_def CR3_RED_def CR4_def NORMAL_def)

(* sub_induction in the arrow-type case for the next proof *)
lemma sub_induction:
  assumes a: "SN(u)"
  and     b: "u\RED \"
  and     c1: "NEUT t"
  and     c2: "CR2 \"
  and     c3: "CR3 \"
  and     c4: "CR3_RED t (\\\)"
  shows "(App t u)\RED \"
using a b
proof (induct)
  fix u
  assume as: "u\RED \"
  assume ih: " \u'. \u \\<^sub>\ u'; u' \ RED \\ \ App t u' \ RED \"
  have "NEUT (App t u)" using c1 by (auto simp add: NEUT_def)
  moreover
  have "CR3_RED (App t u) \" unfolding CR3_RED_def
  proof (intro strip)
    fix r
    assume red: "App t u \\<^sub>\ r"
    moreover
    { assume "\t'. t \\<^sub>\ t' \ r = App t' u"
      then obtain t' where a1: "t \\<^sub>\ t'" and a2: "r = App t' u" by blast
      have "t'\RED (\\\)" using c4 a1 by (simp add: CR3_RED_def)
      then have "App t' u\RED \" using as by simp
      then have "r\RED \" using a2 by simp
    }
    moreover
    { assume "\u'. u \\<^sub>\ u' \ r = App t u'"
      then obtain u' where b1: "u \\<^sub>\ u'" and b2: "r = App t u'" by blast
      have "u'\RED \" using as b1 c2 by (auto simp add: CR2_def)
      with ih have "App t u' \ RED \" using b1 by simp
      then have "r\RED \" using b2 by simp
    }
    moreover
    { assume "\x t'. t = Lam [x].t'"
      then obtain x t' where "t = Lam [x].t'" by blast
      then have "NEUT (Lam [x].t')" using c1 by simp
      then have "False" by (simp add: NEUT_def)
      then have "r\RED \" by simp
    }
    ultimately show "r \ RED \" by (cases) (auto simp add: lam.inject)
  qed
  ultimately show "App t u \ RED \" using c3 by (simp add: CR3_def)
qed

text \<open>properties of the candiadates\<close>
lemma RED_props:
  shows "CR1 \" and "CR2 \" and "CR3 \"
proof (nominal_induct \<tau> rule: ty.strong_induct)
  case (TVar a)
  { case 1 show "CR1 (TVar a)" by (simp add: CR1_def)
  next
    case 2 show "CR2 (TVar a)" by (auto intro: SN_preserved simp add: CR2_def)
  next
    case 3 show "CR3 (TVar a)" by (auto intro: SN_intro simp add: CR3_def CR3_RED_def)
  }
next
  case (TArr \<tau>1 \<tau>2)
  { case 1
    have ih_CR3_\<tau>1: "CR3 \<tau>1" by fact
    have ih_CR1_\<tau>2: "CR1 \<tau>2" by fact
    have "\t. t \ RED (\1 \ \2) \ SN t"
    proof -
      fix t
      assume "t \ RED (\1 \ \2)"
      then have a: "\u. u \ RED \1 \ App t u \ RED \2" by simp
      from ih_CR3_\<tau>1 have "CR4 \<tau>1" by (simp add: CR3_implies_CR4)
      moreover
      fix a have "NEUT (Var a)" by (force simp add: NEUT_def)
      moreover
      have "NORMAL (Var a)" by (rule NORMAL_Var)
      ultimately have "(Var a)\ RED \1" by (simp add: CR4_def)
      with a have "App t (Var a) \ RED \2" by simp
      hence "SN (App t (Var a))" using ih_CR1_\<tau>2 by (simp add: CR1_def)
      thus "SN t" by (auto dest: SN_of_FST_of_App)
    qed
    then show "CR1 (\1 \ \2)" unfolding CR1_def by simp
  next
    case 2
    have ih_CR2_\<tau>2: "CR2 \<tau>2" by fact
    then show "CR2 (\1 \ \2)" unfolding CR2_def by auto
  next
    case 3
    have ih_CR1_\<tau>1: "CR1 \<tau>1" by fact
    have ih_CR2_\<tau>1: "CR2 \<tau>1" by fact
    have ih_CR3_\<tau>2: "CR3 \<tau>2" by fact
    show "CR3 (\1 \ \2)" unfolding CR3_def
    proof (simp, intro strip)
      fix t u
      assume a1: "u \ RED \1"
      assume a2: "NEUT t \ CR3_RED t (\1 \ \2)"
      have "SN(u)" using a1 ih_CR1_\<tau>1 by (simp add: CR1_def)
      then show "(App t u)\RED \2" using ih_CR2_\1 ih_CR3_\2 a1 a2 by (blast intro: sub_induction)
    qed
  }
qed

text \<open>
  the next lemma not as simple as on paper, probably because of
  the stronger double_SN induction
\<close>
lemma abs_RED:
  assumes asm: "\s\RED \. t[x::=s]\RED \"
  shows "Lam [x].t\RED (\\\)"
proof -
  have b1: "SN t"
  proof -
    have "Var x\RED \"
    proof -
      have "CR4 \" by (simp add: RED_props CR3_implies_CR4)
      moreover
      have "NEUT (Var x)" by (auto simp add: NEUT_def)
      moreover
      have "NORMAL (Var x)" by (auto elim: Beta.cases simp add: NORMAL_def)
      ultimately show "Var x\RED \" by (simp add: CR4_def)
    qed
    then have "t[x::=Var x]\RED \" using asm by simp
    then have "t\RED \" by (simp add: id_subs)
    moreover
    have "CR1 \" by (simp add: RED_props)
    ultimately show "SN t" by (simp add: CR1_def)
  qed
  show "Lam [x].t\RED (\\\)"
  proof (simp, intro strip)
    fix u
    assume b2: "u\RED \"
    then have b3: "SN u" using RED_props by (auto simp add: CR1_def)
    show "App (Lam [x].t) u \ RED \" using b1 b3 b2 asm
    proof(induct t u rule: double_SN)
      fix t u
      assume ih1: "\t'. \t \\<^sub>\ t'; u\RED \; \s\RED \. t'[x::=s]\RED \\ \ App (Lam [x].t') u \ RED \"
      assume ih2: "\u'. \u \\<^sub>\ u'; u'\RED \; \s\RED \. t[x::=s]\RED \\ \ App (Lam [x].t) u' \ RED \"
      assume as1: "u \ RED \"
      assume as2: "\s\RED \. t[x::=s]\RED \"
      have "CR3_RED (App (Lam [x].t) u) \" unfolding CR3_RED_def
      proof(intro strip)
        fix r
        assume red: "App (Lam [x].t) u \\<^sub>\ r"
        moreover
        { assume "\t'. t \\<^sub>\ t' \ r = App (Lam [x].t') u"
          then obtain t' where a1: "t \\<^sub>\ t'" and a2: "r = App (Lam [x].t') u" by blast
          have "App (Lam [x].t') u\RED \" using ih1 a1 as1 as2
            apply(auto)
            apply(drule_tac x="t'" in meta_spec)
            apply(simp)
            apply(drule meta_mp)
            prefer 2
            apply(auto)[1]
            apply(rule ballI)
            apply(drule_tac x="s" in bspec)
            apply(simp)
            apply(subgoal_tac "CR2 \")(*A*)
            apply(unfold CR2_def)[1]
            apply(drule_tac x="t[x::=s]" in spec)
            apply(drule_tac x="t'[x::=s]" in spec)
            apply(simp add: beta_subst)
            (*A*)
            apply(simp add: RED_props)
            done
          then have "r\RED \" using a2 by simp
        }
        moreover
        { assume "\u'. u \\<^sub>\ u' \ r = App (Lam [x].t) u'"
          then obtain u' where b1: "u \\<^sub>\ u'" and b2: "r = App (Lam [x].t) u'" by blast
          have "App (Lam [x].t) u'\RED \" using ih2 b1 as1 as2
            apply(auto)
            apply(drule_tac x="u'" in meta_spec)
            apply(simp)
            apply(drule meta_mp)
            apply(subgoal_tac "CR2 \")
            apply(unfold CR2_def)[1]
            apply(drule_tac x="u" in spec)
            apply(drule_tac x="u'" in spec)
            apply(simp)
            apply(simp add: RED_props)
            apply(simp)
            done
          then have "r\RED \" using b2 by simp
        }
        moreover
        { assume "r = t[x::=u]"
          then have "r\RED \" using as1 as2 by auto
        }
        ultimately show "r \ RED \"
          (* one wants to use the strong elimination principle; for this one
             has to know that x\<sharp>u *)
        apply(cases)
        apply(auto simp add: lam.inject)
        apply(drule beta_abs)
        apply(auto)[1]
        apply(auto simp add: alpha subst_rename)
        done
    qed
    moreover
    have "NEUT (App (Lam [x].t) u)" unfolding NEUT_def by (auto)
    ultimately show "App (Lam [x].t) u \ RED \" using RED_props by (simp add: CR3_def)
  qed
qed
qed

abbreviation
mapsto :: "(name\lam) list \ name \ lam \ bool" ("_ maps _ to _" [55,55,55] 55)
where
"\ maps x to e \ (lookup \ x) = e"

abbreviation
  closes :: "(name\lam) list \ (name\ty) list \ bool" ("_ closes _" [55,55] 55)
where
  "\ closes \ \ \x T. ((x,T) \ set \ \ (\t. \ maps x to t \ t \ RED T))"

lemma all_RED:
  assumes a: "\ \ t : \"
  and     b: "\ closes \"
  shows "\ \ RED \"
using a b
proof(nominal_induct  avoiding: \<theta> rule: typing.strong_induct)
  case (t3 a \<Gamma> \<sigma> t \<tau> \<theta>) \<comment> \<open>lambda case\<close>
  have ih: "\\. \ closes ((a,\)#\) \ \ \ RED \" by fact
  have \<theta>_cond: "\<theta> closes \<Gamma>" by fact
  have fresh: "a\\" "a\\" by fact+
  from ih have "\s\RED \. ((a,s)#\) \ RED \" using fresh \_cond fresh_context by simp
  then have "\s\RED \. \[a::=s] \ RED \" using fresh by (simp add: psubst_subst)
  then have "Lam [a].(\) \ RED (\ \ \)" by (simp only: abs_RED)
  then show "\<(Lam [a].t)> \ RED (\ \ \)" using fresh by simp
qed auto

section \<open>identity substitution generated from a context \<Gamma>\<close>
fun
  "id" :: "(name\ty) list \ (name\lam) list"
where
  "id [] = []"
| "id ((x,\)#\) = (x,Var x)#(id \)"

lemma id_maps:
  shows "(id \) maps a to (Var a)"
by (induct \<Gamma>) (auto)

lemma id_fresh:
  fixes a::"name"
  assumes a: "a\\"
  shows "a\(id \)"
using a
by (induct \<Gamma>)
   (auto simp add: fresh_list_nil fresh_list_cons)

lemma id_apply:
  shows "(id \) = t"
by (nominal_induct t avoiding: \<Gamma> rule: lam.strong_induct)
   (auto simp add: id_maps id_fresh)

lemma id_closes:
  shows "(id \) closes \"
apply(auto)
apply(simp add: id_maps)
apply(subgoal_tac "CR3 T") \<comment> \<open>A\<close>
apply(drule CR3_implies_CR4)
apply(simp add: CR4_def)
apply(drule_tac x="Var x" in spec)
apply(force simp add: NEUT_def NORMAL_Var)
\<comment> \<open>A\<close>
apply(rule RED_props)
done

lemma typing_implies_RED:
  assumes a: "\ \ t : \"
  shows "t \ RED \"
proof -
  have "(id \)\RED \"
  proof -
    have "(id \) closes \" by (rule id_closes)
    with a show ?thesis by (rule all_RED)
  qed
  thus"t \ RED \" by (simp add: id_apply)
qed

lemma typing_implies_SN:
  assumes a: "\ \ t : \"
  shows "SN(t)"
proof -
  from a have "t \ RED \" by (rule typing_implies_RED)
  moreover
  have "CR1 \" by (rule RED_props)
  ultimately show "SN(t)" by (simp add: CR1_def)
qed

end

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