Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: SOS.thy Sprache: Isabelle

Original von: Isabelle^©

(*                                                        *)
(* Formalisation of some typical SOS-proofs.              *)
(*                                                        *)
(* This work was inspired by challenge suggested by Adam  *)
(* Chlipala on the POPLmark mailing list.                 *)
(*                                                        *)
(* We thank Nick Benton for helping us with the           *)
(* termination-proof for evaluation.                      *)
(*                                                        *)
(* The formalisation was done by Julien Narboux and       *)
(* Christian Urban.                                       *)

theory SOS
  imports "HOL-Nominal.Nominal"
begin

atom_decl name

text \<open>types and terms\<close>
nominal_datatype ty =
    TVar "nat"
  | Arrow "ty" "ty" ("_\_" [100,100] 100)

nominal_datatype trm =
    Var "name"
  | Lam "\name\trm" ("Lam [_]._" [100,100] 100)
  | App "trm" "trm"

lemma fresh_ty:
  fixes x::"name"
  and   T::"ty"
  shows "x\T"
by (induct T rule: ty.induct)
   (auto simp add: fresh_nat)

text \<open>Parallel and single substitution.\<close>
fun
  lookup :: "(name\trm) list \ name \ trm"
where
  "lookup [] x = Var x"
| "lookup ((y,e)#\) x = (if x=y then e else lookup \ x)"

lemma lookup_eqvt[eqvt]:
  fixes pi::"name prm"
  shows "pi\(lookup \ X) = lookup (pi\\) (pi\X)"
by (induct \<theta>) (auto simp add: eqvts)

lemma lookup_fresh:
  fixes z::"name"
  assumes a: "z\\" and b: "z\x"
  shows "z \lookup \ x"
using a b
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)

(* parallel substitution *)

nominal_primrec
  psubst :: "(name\trm) list \ trm \ trm" ("_<_>" [95,95] 105)
where
  "\<(Var x)> = (lookup \ x)"
| "\<(App e\<^sub>1 e\<^sub>2)> = App (\1>) (\2>)"
| "x\\ \ \<(Lam [x].e)> = Lam [x].(\)"
apply(finite_guess)+
apply(rule TrueI)+
apply(simp add: abs_fresh)+
apply(fresh_guess)+
done

lemma psubst_eqvt[eqvt]:
  fixes pi::"name prm"
  and   t::"trm"
  shows "pi\(\) = (pi\\)<(pi\t)>"
by (nominal_induct t avoiding: \<theta> rule: trm.strong_induct)
   (perm_simp add: fresh_bij lookup_eqvt)+

lemma fresh_psubst:
  fixes z::"name"
  and   t::"trm"
  assumes "z\t" and "z\\"
  shows "z\(\)"
using assms
by (nominal_induct t avoiding: z \<theta> t rule: trm.strong_induct)
   (auto simp add: abs_fresh lookup_fresh)

lemma psubst_empty[simp]:
  shows "[] = t"
  by (nominal_induct t rule: trm.strong_induct)
     (auto simp add: fresh_list_nil)

text \<open>Single substitution\<close>
abbreviation
  subst :: "trm \ name \ trm \ trm" ("_[_::=_]" [100,100,100] 100)
where
  "t[x::=t'] \ ([(x,t')])"

lemma subst[simp]:
  shows "(Var x)[y::=t'] = (if x=y then t' else (Var x))"
  and   "(App t\<^sub>1 t\<^sub>2)[y::=t'] = App (t\<^sub>1[y::=t']) (t\<^sub>2[y::=t'])"
  and   "x\(y,t') \ (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])"
by (simp_all add: fresh_list_cons fresh_list_nil)

lemma fresh_subst:
  fixes z::"name"
  shows "\z\s; (z=y \ z\t)\ \ z\t[y::=s]"
by (nominal_induct t avoiding: z y s rule: trm.strong_induct)
   (auto simp add: abs_fresh fresh_prod fresh_atm)

lemma forget:
  assumes a: "x\e"
  shows "e[x::=e'] = e"
using a
by (nominal_induct e avoiding: x e' rule: trm.strong_induct)
   (auto simp add: fresh_atm abs_fresh)

lemma psubst_subst_psubst:
  assumes h: "x\\"
  shows "\[x::=e'] = ((x,e')#\)"
  using h
by (nominal_induct e avoiding: \<theta> x e' rule: trm.strong_induct)
   (auto simp add: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh')

text \<open>Typing Judgements\<close>

inductive
  valid :: "(name\ty) list \ bool"
where
  v_nil[intro]:  "valid []"
| v_cons[intro]: "\valid \;x\\\ \ valid ((x,T)#\)"

equivariance valid

inductive_cases
  valid_elim[elim]: "valid ((x,T)#\)"

lemma valid_insert:
  assumes a: "valid (\@[(x,T)]@\)"
  shows "valid (\ @ \)"
using a
by (induct \<Delta>)
   (auto simp add:  fresh_list_append fresh_list_cons elim!: valid_elim)

lemma fresh_set:
  shows "y\xs = (\x\set xs. y\x)"
by (induct xs) (simp_all add: fresh_list_nil fresh_list_cons)

lemma context_unique:
  assumes a1: "valid \"
  and     a2: "(x,T) \ set \"
  and     a3: "(x,U) \ set \"
  shows "T = U"
using a1 a2 a3
by (induct) (auto simp add: fresh_set fresh_prod fresh_atm)

text \<open>Typing Relation\<close>

inductive
  typing :: "(name\ty) list\trm\ty\bool" ("_ \ _ : _" [60,60,60] 60)
where
  t_Var[intro]:   "\valid \; (x,T)\set \\ \ \ \ Var x : T"
| t_App[intro]:   "\\ \ e\<^sub>1 : T\<^sub>1\T\<^sub>2; \ \ e\<^sub>2 : T\<^sub>1\ \ \ \ App e\<^sub>1 e\<^sub>2 : T\<^sub>2"
| t_Lam[intro]:   "\x\\; (x,T\<^sub>1)#\ \ e : T\<^sub>2\ \ \ \ Lam [x].e : T\<^sub>1\T\<^sub>2"

equivariance typing

nominal_inductive typing
  by (simp_all add: abs_fresh fresh_ty)

lemma typing_implies_valid:
  assumes a: "\ \ t : T"
  shows "valid \"
using a by (induct) (auto)

lemma t_App_elim:
  assumes a: "\ \ App t1 t2 : T"
  obtains T' where "\ \ t1 : T' \ T" and "\ \ t2 : T'"
using a
by (cases) (auto simp add: trm.inject)

lemma t_Lam_elim:
  assumes a: "\ \ Lam [x].t : T" "x\\"
  obtains T\<^sub>1 and T\<^sub>2 where "(x,T\<^sub>1)#\<Gamma> \<turnstile> t : T\<^sub>2" and "T=T\<^sub>1\<rightarrow>T\<^sub>2"
using a
by (cases rule: typing.strong_cases [where x="x"])
   (auto simp add: abs_fresh fresh_ty alpha trm.inject)

abbreviation
  "sub_context" :: "(name\ty) list \ (name\ty) list \ bool" ("_ \ _" [55,55] 55)
where
  "\\<^sub>1 \ \\<^sub>2 \ \x T. (x,T)\set \\<^sub>1 \ (x,T)\set \\<^sub>2"

lemma weakening:
  fixes \<Gamma>\<^sub>1 \<Gamma>\<^sub>2::"(name\<times>ty) list"
  assumes "\\<^sub>1 \ e: T" and "valid \\<^sub>2" and "\\<^sub>1 \ \\<^sub>2"
  shows "\\<^sub>2 \ e: T"
  using assms
proof(nominal_induct \<Gamma>\<^sub>1 e T avoiding: \<Gamma>\<^sub>2 rule: typing.strong_induct)
  case (t_Lam x \<Gamma>\<^sub>1 T\<^sub>1 t T\<^sub>2 \<Gamma>\<^sub>2)
  have vc: "x\\\<^sub>2" by fact
  have ih: "\valid ((x,T\<^sub>1)#\\<^sub>2); (x,T\<^sub>1)#\\<^sub>1 \ (x,T\<^sub>1)#\\<^sub>2\ \ (x,T\<^sub>1)#\\<^sub>2 \ t : T\<^sub>2" by fact
  have "valid \\<^sub>2" by fact
  then have "valid ((x,T\<^sub>1)#\\<^sub>2)" using vc by auto
  moreover
  have "\\<^sub>1 \ \\<^sub>2" by fact
  then have "(x,T\<^sub>1)#\\<^sub>1 \ (x,T\<^sub>1)#\\<^sub>2" by simp
  ultimately have "(x,T\<^sub>1)#\\<^sub>2 \ t : T\<^sub>2" using ih by simp
  with vc show "\\<^sub>2 \ Lam [x].t : T\<^sub>1\T\<^sub>2" by auto
qed (auto)

lemma type_substitutivity_aux:
  assumes a: "(\@[(x,T')]@\) \ e : T"
  and     b: "\ \ e' : T'"
  shows "(\@\) \ e[x::=e'] : T"
using a b
proof (nominal_induct \<Gamma>\<equiv>"\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: e' \<Delta> rule: typing.strong_induct)
  case (t_Var y T e' \)
  then have a1: "valid (\@[(x,T')]@\)"
       and  a2: "(y,T) \ set (\@[(x,T')]@\)"
       and  a3: "\ \ e' : T'" .
  from a1 have a4: "valid (\@\)" by (rule valid_insert)
  { assume eq: "x=y"
    from a1 a2 have "T=T'" using eq by (auto intro: context_unique)
    with a3 have "\@\ \ Var y[x::=e'] : T" using eq a4 by (auto intro: weakening)
  }
  moreover
  { assume ineq: "x\y"
    from a2 have "(y,T) \ set (\@\)" using ineq by simp
    then have "\@\ \ Var y[x::=e'] : T" using ineq a4 by auto
  }
  ultimately show "\@\ \ Var y[x::=e'] : T" by blast
qed (force simp add: fresh_list_append fresh_list_cons)+

corollary type_substitutivity:
  assumes a: "(x,T')#\ \ e : T"
  and     b: "\ \ e' : T'"
  shows "\ \ e[x::=e'] : T"
using a b type_substitutivity_aux[where \<Delta>="[]"]
by (auto)

text \<open>Values\<close>
inductive
  val :: "trm\bool"
where
  v_Lam[intro]:   "val (Lam [x].e)"

equivariance val

lemma not_val_App[simp]:
  shows
  "\ val (App e\<^sub>1 e\<^sub>2)"
  "\ val (Var x)"
  by (auto elim: val.cases)

text \<open>Big-Step Evaluation\<close>

inductive
  big :: "trm\trm\bool" ("_ \ _" [80,80] 80)
where
  b_Lam[intro]:   "Lam [x].e \ Lam [x].e"
| b_App[intro]:   "\x\(e\<^sub>1,e\<^sub>2,e'); e\<^sub>1\Lam [x].e; e\<^sub>2\e\<^sub>2'; e[x::=e\<^sub>2']\e'\ \ App e\<^sub>1 e\<^sub>2 \ e'"

equivariance big

nominal_inductive big
  by (simp_all add: abs_fresh)

lemma big_preserves_fresh:
  fixes x::"name"
  assumes a: "e \ e'" "x\e"
  shows "x\e'"
  using a by (induct) (auto simp add: abs_fresh fresh_subst)

lemma b_App_elim:
  assumes a: "App e\<^sub>1 e\<^sub>2 \ e'" "x\(e\<^sub>1,e\<^sub>2,e')"
  obtains f\<^sub>1 and f\<^sub>2 where "e\<^sub>1 \<Down> Lam [x]. f\<^sub>1" "e\<^sub>2 \<Down> f\<^sub>2" "f\<^sub>1[x::=f\<^sub>2] \<Down> e'"
  using a
by (cases rule: big.strong_cases[where x="x" and xa="x"])
   (auto simp add: trm.inject)

lemma subject_reduction:
  assumes a: "e \ e'" and b: "\ \ e : T"
  shows "\ \ e' : T"
  using a b
proof (nominal_induct avoiding: \<Gamma> arbitrary: T rule: big.strong_induct)
  case (b_App x e\<^sub>1 e\<^sub>2 e' e e\<^sub>2' \<Gamma> T)
  have vc: "x\\" by fact
  have "\ \ App e\<^sub>1 e\<^sub>2 : T" by fact
  then obtain T' where a1: "\ \ e\<^sub>1 : T'\T" and a2: "\ \ e\<^sub>2 : T'"
    by (cases) (auto simp add: trm.inject)
  have ih1: "\ \ e\<^sub>1 : T' \ T \ \ \ Lam [x].e : T' \ T" by fact
  have ih2: "\ \ e\<^sub>2 : T' \ \ \ e\<^sub>2' : T'" by fact
  have ih3: "\ \ e[x::=e\<^sub>2'] : T \ \ \ e' : T" by fact
  have "\ \ Lam [x].e : T'\T" using ih1 a1 by simp
  then have "((x,T')#\) \ e : T" using vc
    by (auto elim: t_Lam_elim simp add: ty.inject)
  moreover
  have "\ \ e\<^sub>2': T'" using ih2 a2 by simp
  ultimately have "\ \ e[x::=e\<^sub>2'] : T" by (simp add: type_substitutivity)
  thus "\ \ e' : T" using ih3 by simp
qed (blast)

lemma subject_reduction2:
  assumes a: "e \ e'" and b: "\ \ e : T"
  shows "\ \ e' : T"
  using a b
by (nominal_induct avoiding: \<Gamma> T rule: big.strong_induct)
   (force elim: t_App_elim t_Lam_elim simp add: ty.inject type_substitutivity)+

lemma unicity_of_evaluation:
  assumes a: "e \ e\<^sub>1"
  and     b: "e \ e\<^sub>2"
  shows "e\<^sub>1 = e\<^sub>2"
  using a b
proof (nominal_induct e e\<^sub>1 avoiding: e\<^sub>2 rule: big.strong_induct)
  case (b_Lam x e t\<^sub>2)
  have "Lam [x].e \ t\<^sub>2" by fact
  thus "Lam [x].e = t\<^sub>2" by cases (simp_all add: trm.inject)
next
  case (b_App x e\<^sub>1 e\<^sub>2 e' e\<^sub>1' e\<^sub>2' t\<^sub>2)
  have ih1: "\t. e\<^sub>1 \ t \ Lam [x].e\<^sub>1' = t" by fact
  have ih2:"\t. e\<^sub>2 \ t \ e\<^sub>2' = t" by fact
  have ih3: "\t. e\<^sub>1'[x::=e\<^sub>2'] \ t \ e' = t" by fact
  have app: "App e\<^sub>1 e\<^sub>2 \ t\<^sub>2" by fact
  have vc: "x\e\<^sub>1" "x\e\<^sub>2" "x\t\<^sub>2" by fact+
  then have "x\App e\<^sub>1 e\<^sub>2" by auto
  from app vc obtain f\<^sub>1 f\<^sub>2 where x1: "e\<^sub>1 \<Down> Lam [x]. f\<^sub>1" and x2: "e\<^sub>2 \<Down> f\<^sub>2" and x3: "f\<^sub>1[x::=f\<^sub>2] \<Down> t\<^sub>2"
    by (auto elim!: b_App_elim)
  then have "Lam [x]. f\<^sub>1 = Lam [x]. e\<^sub>1'" using ih1 by simp
  then
  have "f\<^sub>1 = e\<^sub>1'" by (auto simp add: trm.inject alpha)
  moreover
  have "f\<^sub>2 = e\<^sub>2'" using x2 ih2 by simp
  ultimately have "e\<^sub>1'[x::=e\<^sub>2'] \ t\<^sub>2" using x3 by simp
  thus "e' = t\<^sub>2" using ih3 by simp
qed

lemma reduces_evaluates_to_values:
  assumes h: "t \ t'"
  shows "val t'"
using h by (induct) (auto)

(* Valuation *)

nominal_primrec
  V :: "ty \ trm set"
where
  "V (TVar x) = {e. val e}"
| "V (T\<^sub>1 \ T\<^sub>2) = {Lam [x].e | x e. \ v \ (V T\<^sub>1). \ v'. e[x::=v] \ v' \ v' \ V T\<^sub>2}"
  by (rule TrueI)+

lemma V_eqvt:
  fixes pi::"name prm"
  assumes a: "x\V T"
  shows "(pi\x)\V T"
using a
apply(nominal_induct T arbitrary: pi x rule: ty.strong_induct)
apply(auto simp add: trm.inject)
apply(simp add: eqvts)
apply(rule_tac x="pi\xa" in exI)
apply(rule_tac x="pi\e" in exI)
apply(simp)
apply(auto)
apply(drule_tac x="(rev pi)\v" in bspec)
apply(force)
apply(auto)
apply(rule_tac x="pi\v'" in exI)
apply(auto)
apply(drule_tac pi="pi" in big.eqvt)
apply(perm_simp add: eqvts)
done

lemma V_arrow_elim_weak:
  assumes h:"u \ V (T\<^sub>1 \ T\<^sub>2)"
  obtains a t where "u = Lam [a].t" and "\ v \ (V T\<^sub>1). \ v'. t[a::=v] \ v' \ v' \ V T\<^sub>2"
using h by (auto)

lemma V_arrow_elim_strong:
  fixes c::"'a::fs_name"
  assumes h: "u \ V (T\<^sub>1 \ T\<^sub>2)"
  obtains a t where "a\c" "u = Lam [a].t" "\v \ (V T\<^sub>1). \ v'. t[a::=v] \ v' \ v' \ V T\<^sub>2"
using h
apply -
apply(erule V_arrow_elim_weak)
apply(subgoal_tac "\a'::name. a'\(a,t,c)") (*A*)
apply(erule exE)
apply(drule_tac x="a'" in meta_spec)
apply(drule_tac x="[(a,a')]\t" in meta_spec)
apply(drule meta_mp)
apply(simp)
apply(drule meta_mp)
apply(simp add: trm.inject alpha fresh_left fresh_prod calc_atm fresh_atm)
apply(perm_simp)
apply(force)
apply(drule meta_mp)
apply(rule ballI)
apply(drule_tac x="[(a,a')]\v" in bspec)
apply(simp add: V_eqvt)
apply(auto)
apply(rule_tac x="[(a,a')]\v'" in exI)
apply(auto)
apply(drule_tac pi="[(a,a')]" in big.eqvt)
apply(perm_simp add: eqvts calc_atm)
apply(simp add: V_eqvt)
(*A*)
apply(rule exists_fresh')
apply(simp add: fin_supp)
done

lemma Vs_are_values:
  assumes a: "e \ V T"
  shows "val e"
using a by (nominal_induct T arbitrary: e rule: ty.strong_induct) (auto)

lemma values_reduce_to_themselves:
  assumes a: "val v"
  shows "v \ v"
using a by (induct) (auto)

lemma Vs_reduce_to_themselves:
  assumes a: "v \ V T"
  shows "v \ v"
using a by (simp add: values_reduce_to_themselves Vs_are_values)

text \<open>'\<theta> maps x to e' asserts that \<theta> substitutes x with e\<close>
abbreviation
  mapsto :: "(name\trm) list \ name \ trm \ bool" ("_ maps _ to _" [55,55,55] 55)
where
"\ maps x to e \ (lookup \ x) = e"

abbreviation
  v_closes :: "(name\trm) list \ (name\ty) list \ bool" ("_ Vcloses _" [55,55] 55)
where
  "\ Vcloses \ \ \x T. (x,T) \ set \ \ (\v. \ maps x to v \ v \ V T)"

lemma case_distinction_on_context:
  fixes \<Gamma>::"(name\<times>ty) list"
  assumes asm1: "valid ((m,t)#\)"
  and     asm2: "(n,U) \ set ((m,T)#\)"
  shows "(n,U) = (m,T) \ ((n,U) \ set \ \ n \ m)"
proof -
  from asm2 have "(n,U) \ set [(m,T)] \ (n,U) \ set \" by auto
  moreover
  { assume eq: "m=n"
    assume "(n,U) \ set \"
    then have "\ n\\"
      by (induct \<Gamma>) (auto simp add: fresh_list_cons fresh_prod fresh_atm)
    moreover have "m\\" using asm1 by auto
    ultimately have False using eq by auto
  }
  ultimately show ?thesis by auto
qed

lemma monotonicity:
  fixes m::"name"
  fixes \<theta>::"(name \<times> trm) list"
  assumes h1: "\ Vcloses \"
  and     h2: "e \ V T"
  and     h3: "valid ((x,T)#\)"
  shows "(x,e)#\ Vcloses (x,T)#\"
proof(intro strip)
  fix x' T'
  assume "(x',T') \ set ((x,T)#\)"
  then have "((x',T')=(x,T)) \ ((x',T')\set \ \ x'\x)" using h3
    by (rule_tac case_distinction_on_context)
  moreover
  { (* first case *)
    assume "(x',T') = (x,T)"
    then have "\e'. ((x,e)#\) maps x to e' \ e' \ V T'" using h2 by auto
  }
  moreover
  { (* second case *)
    assume "(x',T') \ set \" and neq:"x' \ x"
      then have "\e'. \ maps x' to e' \ e' \ V T'" using h1 by auto
      then have "\e'. ((x,e)#\) maps x' to e' \ e' \ V T'" using neq by auto
  }
  ultimately show "\e'. ((x,e)#\) maps x' to e' \ e' \ V T'" by blast
qed

lemma termination_aux:
  assumes h1: "\ \ e : T"
  and     h2: "\ Vcloses \"
  shows "\v. \ \ v \ v \ V T"
using h2 h1
proof(nominal_induct e avoiding: \<Gamma> \<theta> arbitrary: T rule: trm.strong_induct)
  case (App e\<^sub>1 e\<^sub>2 \<Gamma> \<theta> T)
  have ih\<^sub>1: "\<And>\<theta> \<Gamma> T. \<lbrakk>\<theta> Vcloses \<Gamma>; \<Gamma> \<turnstile> e\<^sub>1 : T\<rbrakk> \<Longrightarrow> \<exists>v. \<theta><e\<^sub>1> \<Down> v \<and> v \<in> V T" by fact
  have ih\<^sub>2: "\<And>\<theta> \<Gamma> T. \<lbrakk>\<theta> Vcloses \<Gamma>; \<Gamma> \<turnstile> e\<^sub>2 : T\<rbrakk> \<Longrightarrow> \<exists>v. \<theta><e\<^sub>2> \<Down> v \<and> v \<in> V T" by fact
  have as\<^sub>1: "\<theta> Vcloses \<Gamma>" by fact
  have as\<^sub>2: "\<Gamma> \<turnstile> App e\<^sub>1 e\<^sub>2 : T" by fact
  then obtain T' where "\ \ e\<^sub>1 : T' \ T" and "\ \ e\<^sub>2 : T'" by (auto elim: t_App_elim)
  then obtain v\<^sub>1 v\<^sub>2 where "(i)": "\<theta><e\<^sub>1> \<Down> v\<^sub>1" "v\<^sub>1 \<in> V (T' \<rightarrow> T)"
                      and "(ii)": "\2> \ v\<^sub>2" "v\<^sub>2 \ V T'" using ih\<^sub>1 ih\<^sub>2 as\<^sub>1 by blast
  from "(i)" obtain x e'
            where "v\<^sub>1 = Lam [x].e'"
            and "(iii)": "(\v \ (V T').\ v'. e'[x::=v] \ v' \ v' \ V T)"
            and "(iv)":  "\1> \ Lam [x].e'"
            and fr: "x\(\,e\<^sub>1,e\<^sub>2)" by (blast elim: V_arrow_elim_strong)
  from fr have fr\<^sub>1: "x\<sharp>\<theta><e\<^sub>1>" and fr\<^sub>2: "x\<sharp>\<theta><e\<^sub>2>" by (simp_all add: fresh_psubst)
  from "(ii)" "(iii)" obtain v\<^sub>3 where "(v)": "e'[x::=v\<^sub>2] \<Down> v\<^sub>3" "v\<^sub>3 \<in> V T" by auto
  from fr\<^sub>2 "(ii)" have "x\<sharp>v\<^sub>2" by (simp add: big_preserves_fresh)
  then have "x\e'[x::=v\<^sub>2]" by (simp add: fresh_subst)
  then have fr\<^sub>3: "x\<sharp>v\<^sub>3" using "(v)" by (simp add: big_preserves_fresh)
  from fr\<^sub>1 fr\<^sub>2 fr\<^sub>3 have "x\<sharp>(\<theta><e\<^sub>1>,\<theta><e\<^sub>2>,v\<^sub>3)" by simp
  with "(iv)" "(ii)" "(v)" have "App (\1>) (\2>) \ v\<^sub>3" by auto
  then show "\v. \1 e\<^sub>2> \ v \ v \ V T" using "(v)" by auto
next
  case (Lam x e \<Gamma> \<theta> T)
  have ih:"\\ \ T. \\ Vcloses \; \ \ e : T\ \ \v. \ \ v \ v \ V T" by fact
  have as\<^sub>1: "\<theta> Vcloses \<Gamma>" by fact
  have as\<^sub>2: "\<Gamma> \<turnstile> Lam [x].e : T" by fact
  have fs: "x\\" "x\\" by fact+
  from as\<^sub>2 fs obtain T\<^sub>1 T\<^sub>2
    where "(i)": "(x,T\<^sub>1)#\ \ e:T\<^sub>2" and "(ii)": "T = T\<^sub>1 \ T\<^sub>2" using fs
    by (auto elim: t_Lam_elim)
  from "(i)" have "(iii)": "valid ((x,T\<^sub>1)#\)" by (simp add: typing_implies_valid)
  have "\v \ (V T\<^sub>1). \v'. (\)[x::=v] \ v' \ v' \ V T\<^sub>2"
  proof
    fix v
    assume "v \ (V T\<^sub>1)"
    with "(iii)" as\<^sub>1 have "(x,v)#\<theta> Vcloses (x,T\<^sub>1)#\<Gamma>" using monotonicity by auto
    with ih "(i)" obtain v' where "((x,v)#\) \ v' \ v' \ V T\<^sub>2" by blast
    then have "\[x::=v] \ v' \ v' \ V T\<^sub>2" using fs by (simp add: psubst_subst_psubst)
    then show "\v'. \[x::=v] \ v' \ v' \ V T\<^sub>2" by auto
  qed
  then have "Lam[x].\ \ V (T\<^sub>1 \ T\<^sub>2)" by auto
  then have "\ \ Lam [x].\ \ Lam [x].\ \ V (T\<^sub>1\T\<^sub>2)" using fs by auto
  thus "\v. \ \ v \ v \ V T" using "(ii)" by auto
next
  case (Var x \<Gamma> \<theta> T)
  have "\ \ (Var x) : T" by fact
  then have "(x,T)\set \" by (cases) (auto simp add: trm.inject)
  with Var have "\ \ \ \ \\ V T"
    by (auto intro!: Vs_reduce_to_themselves)
  then show "\v. \ \ v \ v \ V T" by auto
qed

theorem termination_of_evaluation:
  assumes a: "[] \ e : T"
  shows "\v. e \ v \ val v"
proof -
  from a have "\v. [] \ v \ v \ V T" by (rule termination_aux) (auto)
  thus "\v. e \ v \ val v" using Vs_are_values by auto
qed

end

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