Quelle Weakening.thy Sprache: Isabelle

theory Weakening
  imports "HOL-Nominal.Nominal"
begin

text \<open>
  A simple proof of the Weakening Property in the simply-typed
  lambda-calculus. The proof is simple, because we can make use
  of the variable convention.\<close>

atom_decl name

text \<open>Terms and Types\<close>

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

nominal_datatype ty =
    TVar "string"
  | TArr "ty" "ty" (\<open>_ \<rightarrow> _\<close> [100,100] 100)

lemma ty_fresh:
  fixes x::"name"
  and   T::"ty"
  shows "x\T"
by (nominal_induct T rule: ty.strong_induct)
   (auto simp add: fresh_string)

text \<open>
  Valid contexts (at the moment we have no type for finite
  sets yet, therefore typing-contexts are lists).\<close>

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

equivariance valid

text\<open>Typing judgements\<close>

inductive
  typing :: "(name\ty) list\lam\ty\bool" (\_ \ _ : _\ [60,60,60] 60)
where
    t_Var[intro]: "\valid \; (x,T)\set \\ \ \ \ Var x : T"
  | t_App[intro]: "\\ \ t1 : T1\T2; \ \ t2 : T1\ \ \ \ App t1 t2 : T2"
  | t_Lam[intro]: "\x\\;(x,T1)#\ \ t : T2\ \ \ \ Lam [x].t : T1\T2"

text \<open>
  We derive the strong induction principle for the typing
  relation (this induction principle has the variable convention
  already built-in).\<close>

equivariance typing
nominal_inductive typing
  by (simp_all add: abs_fresh ty_fresh)

text \<open>Abbreviation for the notion of subcontexts.\<close>

abbreviation
  "sub_context" :: "(name\ty) list \ (name\ty) list \ bool" (\_ \ _\ [60,60] 60)
where
  "\1 \ \2 \ \x T. (x,T)\set \1 \ (x,T)\set \2"

text \<open>Now it comes: The Weakening Lemma\<close>

text \<open>
  The first version is, after setting up the induction,
  completely automatic except for use of atomize.\<close>

lemma weakening_version1:
  fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
  assumes a: "\1 \ t : T"
  and     b: "valid \2"
  and     c: "\1 \ \2"
  shows "\2 \ t : T"
using a b c
by (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct)
   (auto | atomize)+

text \<open>
  The second version gives the details for the variable
  and lambda case.\<close>

lemma weakening_version2:
  fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
  and   t ::"lam"
  and   \<tau> ::"ty"
  assumes a: "\1 \ t : T"
  and     b: "valid \2"
  and     c: "\1 \ \2"
  shows "\2 \ t : T"
using a b c
proof (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct)
  case (t_Var \<Gamma>1 x T)  (* variable case *)
  have "\1 \ \2" by fact
  moreover
  have "valid \2" by fact
  moreover
  have "(x,T)\ set \1" by fact
  ultimately show "\2 \ Var x : T" by auto
next
  case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *)
  have vc: "x\\2" by fact (* variable convention *)
  have ih: "\valid ((x,T1)#\2); (x,T1)#\1 \ (x,T1)#\2\ \ (x,T1)#\2 \ t:T2" by fact
  have "\1 \ \2" by fact
  then have "(x,T1)#\1 \ (x,T1)#\2" by simp
  moreover
  have "valid \2" by fact
  then have "valid ((x,T1)#\2)" using vc by (simp add: v2)
  ultimately have "(x,T1)#\2 \ t : T2" using ih by simp
  with vc show "\2 \ Lam [x].t : T1\T2" by auto
qed (auto) (* app case *)

text\<open>
  The original induction principle for the typing relation
  is not strong enough - even this simple lemma fails to be
  simple ;o)\<close>

lemma weakening_not_straigh_forward:
  fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
  assumes a: "\1 \ t : T"
  and     b: "valid \2"
  and     c: "\1 \ \2"
  shows "\2 \ t : T"
using a b c
proof (induct arbitrary: \<Gamma>2)
  case (t_Var \<Gamma>1 x T) (* variable case still works *)
  have "\1 \ \2" by fact
  moreover
  have "valid \2" by fact
  moreover
  have "(x,T) \ (set \1)" by fact
  ultimately show "\2 \ Var x : T" by auto
next
  case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *)
  (* These are all assumptions available in this case*)
  have a0: "x\\1" by fact
  have a1: "(x,T1)#\1 \ t : T2" by fact
  have a2: "\1 \ \2" by fact
  have a3: "valid \2" by fact
  have ih: "\\3. \valid \3; (x,T1)#\1 \ \3\ \ \3 \ t : T2" by fact
  have "(x,T1)#\1 \ (x,T1)#\2" using a2 by simp
  moreover
  have "valid ((x,T1)#\2)" using v2 (* fails *)
    oops

text\<open>
  To show that the proof with explicit renaming is not simple,
  here is the proof without using the variable convention. It
  crucially depends on the equivariance property of the typing
  relation.

\<close>

lemma weakening_with_explicit_renaming:
  fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
  assumes a: "\1 \ t : T"
  and     b: "valid \2"
  and     c: "\1 \ \2"
  shows "\2 \ t : T"
using a b c
proof (induct arbitrary: \<Gamma>2)
  case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *)
  have fc0: "x\\1" by fact
  have ih: "\\3. \valid \3; (x,T1)#\1 \ \3\ \ \3 \ t : T2" by fact
  obtain c::"name" where fc1: "c\(x,t,\1,\2)" (* we obtain a fresh name *)
    by (rule exists_fresh) (auto simp add: fs_name1)
  have "Lam [c].([(c,x)]\t) = Lam [x].t" using fc1 (* we then alpha-rename the lambda-abstraction *)
    by (auto simp add: lam.inject alpha fresh_prod fresh_atm)
  moreover
  have "\2 \ Lam [c].([(c,x)]\t) : T1 \ T2" (* we can then alpha-rename our original goal *)
  proof -
    (* we establish (x,T1)#\<Gamma>1 \<subseteq> (x,T1)#([(c,x)]\<bullet>\<Gamma>2) and valid ((x,T1)#([(c,x)]\<bullet>\<Gamma>2)) *)
    have "(x,T1)#\1 \ (x,T1)#([(c,x)]\\2)"
    proof -
      have "\1 \ \2" by fact
      then have "[(c,x)]\((x,T1)#\1 \ (x,T1)#([(c,x)]\\2))" using fc0 fc1
        by (perm_simp add: eqvts calc_atm perm_fresh_fresh ty_fresh)
      then show "(x,T1)#\1 \ (x,T1)#([(c,x)]\\2)" by (rule perm_boolE)
    qed
    moreover
    have "valid ((x,T1)#([(c,x)]\\2))"
    proof -
      have "valid \2" by fact
      then show "valid ((x,T1)#([(c,x)]\\2))" using fc1
        by (auto intro!: v2 simp add: fresh_left calc_atm eqvts)
    qed
    (* these two facts give us by induction hypothesis the following *)
    ultimately have "(x,T1)#([(c,x)]\\2) \ t : T2" using ih by simp
    (* we now apply renamings to get to our goal *)
    then have "[(c,x)]\((x,T1)#([(c,x)]\\2) \ t : T2)" by (rule perm_boolI)
    then have "(c,T1)#\2 \ ([(c,x)]\t) : T2" using fc1
      by (perm_simp add: eqvts calc_atm perm_fresh_fresh ty_fresh)
    then show "\2 \ Lam [c].([(c,x)]\t) : T1 \ T2" using fc1 by auto
  qed
  ultimately show "\2 \ Lam [x].t : T1 \ T2" by simp
qed (auto) (* var and app cases *)

text \<open>
  Moral: compare the proof with explicit renamings to weakening_version1
  and weakening_version2, and imagine you are proving something more substantial
  than the weakening lemma.\<close>

end

quality95%

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.