1 theory Lambda

     2 imports "../Nominal2" 

     3 begin

     4 

     5 section {* The Weakening property in the simply-typed lambda-calculus *}

     6 

     7 atom_decl name

     8 

     9 nominal_datatype lam =

    10   Var "name"

    11 | App "lam" "lam"

    12 | Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100,100] 100)

    13 

    14 text {* Typing *}

    15 

    16 nominal_datatype ty =

    17   TVar string

    18 | TFun ty ty ("_ \<rightarrow> _" [100,100] 100) 

    19 

    20 lemma fresh_ty:

    21   fixes x::"name"

    22   and   T::"ty"

    23   shows "atom x \<sharp> T"

    24   by (nominal_induct T rule: ty.strong_induct)

    25      (simp_all add: ty.fresh pure_fresh)

    26 

    27 text {* Valid typing contexts *}

    28 

    29 inductive

    30   valid :: "(name \<times> ty) list \<Rightarrow> bool"

    31 where

    32   v_Nil[intro]: "valid []"

    33 | v_Cons[intro]: "\<lbrakk>atom x \<sharp> Gamma; valid Gamma\<rbrakk> \<Longrightarrow> valid ((x, T) # Gamma)"

    34 

    35 equivariance valid

    36 

    37 text {* Typing judgements *}

    38 

    39 inductive

    40   typing :: "(name \<times> ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 

    41 where

    42     t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"

    43   | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"

    44   | t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x]. t : T1 \<rightarrow> T2"

    45 

    46 equivariance typing

    47 

    48 text {* Strong induction principle for typing judgements *}

    49 

    50 nominal_inductive typing

    51   avoids t_Lam: "x"

    52   by (simp_all add: fresh_star_def fresh_ty lam.fresh)

    53 

    54 

    55 abbreviation

    56   "sub_context" :: "(name \<times> ty) list \<Rightarrow> (name \<times> ty) list \<Rightarrow> bool" (infixr "\<subseteq>" 60) 

    57 where

    58   "\<Gamma>1 \<subseteq> \<Gamma>2 \<equiv> \<forall>x T. (x, T) \<in> set \<Gamma>1 \<longrightarrow> (x, T) \<in> set \<Gamma>2"

    59 

    60 

    61 text {* The proof *}

    62 

    63 lemma weakening_version1: 

    64   fixes \<Gamma>1 \<Gamma>2::"(name \<times> ty) list"

    65   and   t ::"lam"

    66   and   \<tau> ::"ty"

    67   assumes a: "\<Gamma>1 \<turnstile> t : T"

    68   and     b: "valid \<Gamma>2" 

    69   and     c: "\<Gamma>1 \<subseteq> \<Gamma>2"

    70   shows "\<Gamma>2 \<turnstile> t : T"

    71 using a b c

    72 proof (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct)

    73   case (t_Var \<Gamma>1 x T)  (* variable case *)

    74   have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact 

    75   moreover  

    76   have "valid \<Gamma>2" by fact 

    77   moreover 

    78   have "(x, T) \<in> set \<Gamma>1" by fact

    79   ultimately show "\<Gamma>2 \<turnstile> Var x : T" by auto

    80 next

    81   case (t_Lam x \<Gamma>1 T1 t T2) (* lambda case *)

    82   have vc: "atom x \<sharp> \<Gamma>2" by fact   (* variable convention *)

    83   have ih: "\<lbrakk>valid ((x, T1) # \<Gamma>2); (x, T1) # \<Gamma>1 \<subseteq> (x, T1) # \<Gamma>2\<rbrakk> \<Longrightarrow> (x, T1) # \<Gamma>2 \<turnstile> t : T2" by fact

    84   have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact

    85   then have "(x, T1) # \<Gamma>1 \<subseteq> (x, T1) # \<Gamma>2" by simp

    86   moreover

    87   have "valid \<Gamma>2" by fact

    88   then have "valid ((x, T1) # \<Gamma>2)" using vc by auto

    89   ultimately have "(x, T1) # \<Gamma>2 \<turnstile> t : T2" using ih by simp

    90   with vc show "\<Gamma>2 \<turnstile> Lam [x]. t : T1 \<rightarrow> T2" by auto

    91 qed (auto) (* app case *)

    92 

    93 lemma weakening_version2: 

    94   fixes \<Gamma>1 \<Gamma>2::"(name \<times> ty) list"

    95   assumes a: "\<Gamma>1 \<turnstile> t : T" 

    96   and     b: "valid \<Gamma>2" 

    97   and     c: "\<Gamma>1 \<subseteq> \<Gamma>2"

    98   shows "\<Gamma>2 \<turnstile> t : T"

    99 using a b c

   100 by (nominal_induct \<Gamma>1 t T avoiding: \<Gamma>2 rule: typing.strong_induct)

   101    (auto | atomize)+

   102 

   103 

   104 text {* A version with finite sets as typing contexts *}

   105 

   106 inductive

   107   valid2 :: "(name \<times> ty) fset \<Rightarrow> bool"

   108 where

   109   v2_Empty[intro]: "valid2 {||}"

   110 | v2_Insert[intro]: "\<lbrakk>(x, T) |\<notin>| Gamma; valid2 Gamma\<rbrakk> \<Longrightarrow> valid2 (insert_fset (x, T) Gamma)"

   111 

   112 equivariance valid2

   113 

   114 inductive

   115   typing2 :: "(name \<times> ty) fset \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ 2\<turnstile> _ : _" [60,60,60] 60) 

   116 where

   117     t2_Var[intro]: "\<lbrakk>valid2 \<Gamma>; (x, T) |\<in>| \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> 2\<turnstile> Var x : T"

   118   | t2_App[intro]: "\<lbrakk>\<Gamma> 2\<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> 2\<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> 2\<turnstile> App t1 t2 : T2"

   119   | t2_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; insert_fset (x, T1) \<Gamma> 2\<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> 2\<turnstile> Lam [x]. t : T1 \<rightarrow> T2"

   120 

   121 equivariance typing2

   122 

   123 nominal_inductive typing2

   124   avoids t2_Lam: "x"

   125   by (simp_all add: fresh_star_def fresh_ty lam.fresh)

   126 

   127 lemma weakening_version3: 

   128   fixes \<Gamma>::"(name \<times> ty) fset"

   129   assumes a: "\<Gamma> 2\<turnstile> t : T" 

   130   and     b: "(x, T') |\<notin>| \<Gamma>"

   131   shows "{|(x, T')|} |\<union>| \<Gamma> 2\<turnstile> t : T"

   132 using a b

   133 apply(nominal_induct \<Gamma> t T avoiding: x rule: typing2.strong_induct)

   134 apply(auto)[2]

   135 apply(rule t2_Lam)

   136 apply(simp add: fresh_insert_fset fresh_Pair fresh_ty)

   137 apply(simp)

   138 apply(drule_tac x="xa" in meta_spec)

   139 apply(drule meta_mp)

   140 apply(simp add: fresh_at_base)

   141 apply(simp add: insert_fset_left_comm)

   142 done

   143 

   144 lemma weakening_version4: 

   145   fixes \<Gamma>::"(name \<times> ty) fset"

   146   assumes a: "\<Gamma> 2\<turnstile> t : T" 

   147   and     b: "(x, T') |\<notin>| \<Gamma>"

   148   shows "{|(x, T')|} |\<union>| \<Gamma> 2\<turnstile> t : T"

   149 using a b

   150 apply(induct \<Gamma> t T arbitrary: x)

   151 apply(auto)[2]

   152 apply(rule t2_Lam)

   153 oops

   154 

   155 end

   156 

   157 

   158