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/Nominal/Examples/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 24 kB

Quelle SOS.thy Sprache: 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" (\<open>_\<rightarrow>_\<close> [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].(\)"
  by (finite_guess | simp add: abs_fresh | fresh_guess)+

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 "x \ V T"
  shows "(pi\x) \ V T"
using assms
proof (nominal_induct T arbitrary: pi x rule: ty.strong_induct)
  case (TVar nat)
  then show ?case
    by (simp add: val.eqvt)
next
  case (Arrow T\<^sub>1 T\<^sub>2 pi x)
  obtain a e where ae: "x = Lam [a]. e" "\v\V T\<^sub>1. \v'. e[a::=v] \ v' \ v' \ V T\<^sub>2"
    using Arrow.prems by auto
  have "\v'. (pi \ e)[(pi \ a)::=v] \ v' \ v' \ V T\<^sub>2" if v: "v \ V T\<^sub>1" for v
  proof -
    have "rev pi \ v \ V T\<^sub>1"
      by (simp add: Arrow.hyps(1) v)
    then obtain v' where "e[a::=(rev pi \ v)] \ v'" "v' \ V T\<^sub>2"
      using ae(2) by blast
    then have "(pi \ e)[(pi \ a)::=v] \ pi \ v'"
      by (metis (no_types, lifting) big.eqvt cons_eqvt nil_eqvt perm_pi_simp(1) perm_prod.simps psubst_eqvt)
    then show ?thesis
      using Arrow.hyps \<open>v' \<in> V T\<^sub>2\<close> by blast
  qed
  with ae show ?case by force
qed

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"
proof -
  obtain a t where "u = Lam [a].t"
    and at: "\v. v \ (V T\<^sub>1) \ \ v'. t[a::=v] \ v' \ v' \ V T\<^sub>2"
    using V_arrow_elim_weak [OF assms] by metis
  obtain a'::name where a': "a'\(a,t,c)"
    by (meson exists_fresh fs_name_class.axioms)
  then have "u = Lam [a'].([(a, a')] \ t)"
    unfolding \<open>u = Lam [a].t\<close>
    by (smt (verit) alpha fresh_atm fresh_prod perm_swap trm.inject(2))
  moreover
  have "\ v'. ([(a, a')] \ t)[a'::=v] \ v' \ v' \ V T\<^sub>2" if "v \ (V T\<^sub>1)" for v
  proof -
    obtain v' where v': "t[a::=([(a, a')] \ v)] \ v' \ v' \ V T\<^sub>2"
      using V_eqvt \<open>v \<in> V T\<^sub>1\<close> at by blast
    then have "([(a, a')] \ t[a::=([(a, a')] \ v)]) \ [(a, a')] \ v'"
      by (simp add: big.eqvt)
    then show ?thesis
      by (smt (verit) V_eqvt cons_eqvt nil_eqvt perm_prod.simps perm_swap(1) psubst_eqvt swap_simps(1) v')
  qed
  ultimately show thesis
    by (metis fresh_prod that a')
qed

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

quality95%

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