1 

     2 theory Tutorial2

     3 imports Lambda

     4 begin

     5 

     6 section {* Height of a Lambda-Term *}

     7 

     8 text {*

     9   The theory Lambda defines the notions of capture-avoiding

    10   substitution and the height of lambda terms. 

    11 *}

    12 

    13 thm height.simps

    14 thm subst.simps

    15 

    16 subsection {* EXERCISE 7 *}

    17 

    18 text {* 

    19   Lets prove a property about the height of substitutions.

    20 

    21   Assume that the height of a lambda-term is always greater 

    22   or equal to 1.

    23 *}

    24 

    25 lemma height_ge_one: 

    26   shows "1 \<le> height t"

    27 by (induct t rule: lam.induct) (auto)

    28 

    29 text {* Remove the sorries *}

    30 

    31 theorem height_subst:

    32   shows "height (t[x ::= t']) \<le> height t - 1 + height t'"

    33 proof (induct t rule: lam.induct)

    34   case (Var y)

    35   show "height (Var y[x ::= t']) \<le> height (Var y) - 1 + height t'" sorry

    36 next    

    37   case (App t1 t2)

    38   have ih1: "height (t1[x::=t']) \<le> (height t1) - 1 + height t'" by fact

    39   have ih2: "height (t2[x::=t']) \<le> (height t2) - 1 + height t'" by fact

    40   

    41   show "height ((App t1 t2)[x ::= t']) \<le> height (App t1 t2) - 1 + height t'" sorry  

    42 next

    43   case (Lam y t1)

    44   have ih: "height (t1[x::=t']) \<le> height t1 - 1 + height t'" by fact

    45   -- {* the definition of capture-avoiding substitution *}

    46   thm subst.simps

    47 

    48   show "height ((Lam [y].t1)[x ::= t']) \<le> height (Lam [y].t1) - 1 + height t'" sorry

    49 qed

    50 

    51 

    52 text {*

    53   The point is that substitutions can only be moved under a binder

    54   provided certain freshness conditions are satisfied. The structural

    55   induction above does not say anything about such freshness conditions.

    56 

    57   Fortunately, Nominal derives automatically some stronger induction

    58   principle for lambda terms which has the usual variable convention

    59   build in.

    60 

    61   In the proof below, we use this stronger induction principle. The

    62   variable and application case are as before.

    63 *}

    64 

    65 

    66 theorem

    67   shows "height (t[x ::= t']) \<le> height t - 1 + height t'"

    68 proof (nominal_induct t avoiding: x t' rule: lam.strong_induct)

    69   case (Var y)

    70   have "1 \<le> height t'" using height_ge_one by simp

    71   then show "height (Var y[x ::= t']) \<le> height (Var y) - 1 + height t'" by simp

    72 next    

    73   case (App t1 t2)

    74   have ih1: "height (t1[x::=t']) \<le> (height t1) - 1 + height t'" 

    75   and  ih2: "height (t2[x::=t']) \<le> (height t2) - 1 + height t'" by fact+

    76   then show "height ((App t1 t2)[x ::= t']) \<le> height (App t1 t2) - 1 + height t'" by simp  

    77 next

    78   case (Lam y t1)

    79   have ih: "height (t1[x::=t']) \<le> height t1 - 1 + height t'" by fact

    80   have vc: "atom y \<sharp> x" "atom y \<sharp> t'" by fact+ -- {* usual variable convention *}

    81   

    82   show "height ((Lam [y].t1)[x ::= t']) \<le> height (Lam [y].t1) - 1 + height t'" sorry

    83 qed

    84 

    85 

    86 section {* Types and the Weakening Lemma *}

    87 

    88 nominal_datatype ty =

    89   tVar "string"

    90 | tArr "ty" "ty" (infixr "\<rightarrow>" 100)

    91 

    92 

    93 text {* 

    94   Having defined them as nominal datatypes gives us additional

    95   definitions and theorems that come with types (see below).

    96  

    97   We next define the type of typing contexts, a predicate that

    98   defines valid contexts (i.e. lists that contain only unique

    99   variables) and the typing judgement.

   100 *}

   101 

   102 type_synonym ty_ctx = "(name \<times> ty) list"

   103 

   104 inductive

   105   valid :: "ty_ctx \<Rightarrow> bool"

   106 where

   107   v1[intro]: "valid []"

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

   109 

   110 

   111 inductive

   112   typing :: "ty_ctx \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60, 60, 60] 60) 

   113 where

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

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

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

   117 

   118 

   119 text {*

   120   The predicate atom x \<sharp> \<Gamma>, read as x fresh for \<Gamma>, is defined by 

   121   Nominal Isabelle. It is defined for lambda-terms, products, lists etc. 

   122   For example we have:

   123 *}

   124 

   125 lemma

   126   fixes x::"name"

   127   shows "atom x \<sharp> Lam [x].t"

   128   and   "atom x \<sharp> (t1, t2) \<Longrightarrow> atom x \<sharp> App t1 t2"

   129   and   "atom x \<sharp> Var y \<Longrightarrow> atom x \<sharp> y" 

   130   and   "\<lbrakk>atom x \<sharp> t1; atom x \<sharp> t2\<rbrakk> \<Longrightarrow> atom x \<sharp> (t1, t2)"

   131   and   "\<lbrakk>atom x \<sharp> l1; atom x \<sharp> l2\<rbrakk> \<Longrightarrow> atom x \<sharp> (l1 @ l2)"

   132   and   "atom x \<sharp> y \<Longrightarrow> x \<noteq> y"

   133   by (simp_all add: lam.fresh fresh_append fresh_at_base) 

   134 

   135 text {* 

   136   We can also prove that every variable is fresh for a type. 

   137 *}

   138 

   139 lemma ty_fresh:

   140   fixes x::"name"

   141   and   T::"ty"

   142   shows "atom x \<sharp> T"

   143 by (induct T rule: ty.induct)

   144    (simp_all add: ty.fresh pure_fresh)

   145 

   146 text {* 

   147   In order to state the weakening lemma in a convenient form, we 

   148   using the following abbreviation. Abbreviations behave like 

   149   definitions, except that they are always automatically folded 

   150   and unfolded.

   151 *}

   152 

   153 abbreviation

   154   "sub_ty_ctx" :: "ty_ctx \<Rightarrow> ty_ctx \<Rightarrow> bool" ("_ \<sqsubseteq> _" [60, 60] 60) 

   155 where

   156   "\<Gamma>1 \<sqsubseteq> \<Gamma>2 \<equiv> \<forall>x. x \<in> set \<Gamma>1 \<longrightarrow> x \<in> set \<Gamma>2"

   157 

   158 

   159 subsection {* EXERCISE 8 *}

   160 

   161 text {*

   162   Fill in the details and give a proof of the weakening lemma. 

   163 *}

   164 

   165 lemma 

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

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

   168   and     c: "\<Gamma>1 \<sqsubseteq> \<Gamma>2"

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

   170 using a b c

   171 proof (induct arbitrary: \<Gamma>2)

   172   case (t_Var \<Gamma>1 x T)

   173   have a1: "valid \<Gamma>1" by fact

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

   175   have a3: "valid \<Gamma>2" by fact

   176   have a4: "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact

   177 

   178   show "\<Gamma>2 \<turnstile> Var x : T" sorry

   179 next

   180   case (t_Lam x \<Gamma>1 T1 t T2) 

   181   have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; (x, T1) # \<Gamma>1 \<sqsubseteq> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t : T2" by fact

   182   have a0: "atom x \<sharp> \<Gamma>1" by fact

   183   have a1: "valid \<Gamma>2" by fact

   184   have a2: "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact

   185 

   186   show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" sorry

   187 qed (auto) -- {* the application case is automatic*}

   188 

   189 

   190 text {* 

   191   Despite the frequent claim that the weakening lemma is trivial,

   192   routine or obvious, the proof in the lambda-case does not go 

   193   through smoothly. Painful variable renamings seem to be necessary. 

   194   But the proof using renamings is horribly complicated (see below). 

   195 *}

   196 

   197 equivariance valid

   198 equivariance typing

   199 

   200 lemma weakening_NOT_TO_BE_TRIED_AT_HOME: 

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

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

   203   and     c: "\<Gamma>1 \<sqsubseteq> \<Gamma>2"

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

   205 using a b c

   206 proof (induct arbitrary: \<Gamma>2)

   207   -- {* lambda case *}

   208   case (t_Lam x \<Gamma>1 T1 t T2) 

   209   have fc0: "atom x \<sharp> \<Gamma>1" by fact

   210   have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; (x, T1) # \<Gamma>1 \<sqsubseteq> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t : T2" by fact

   211   -- {* we choose a fresh variable *}

   212   obtain c::"name" where fc1: "atom c \<sharp> (x, t, \<Gamma>1, \<Gamma>2)" by (rule obtain_fresh)

   213   -- {* we alpha-rename the abstraction *}

   214   have "Lam [c].((c \<leftrightarrow> x) \<bullet> t) = Lam [x].t" using fc1

   215     by (auto simp add: lam.eq_iff Abs1_eq_iff flip_def)

   216   moreover

   217   -- {* we can then alpha rename the goal *}

   218   have "\<Gamma>2 \<turnstile> Lam [c].((c \<leftrightarrow> x) \<bullet> t) : T1 \<rightarrow> T2" 

   219   proof - 

   220     -- {* we need to establish *} 

   221     -- {* (1)   (x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2) *}

   222     -- {* (2)   valid ((x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2)) *}

   223     have "(1)": "(x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2)" 

   224     proof -

   225       have "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact

   226       then have "(c \<leftrightarrow> x) \<bullet> ((x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2))" using fc0 fc1

   227         by (perm_simp) (simp add: flip_fresh_fresh)

   228       then show "(x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2)" by (rule permute_boolE)

   229     qed

   230     moreover 

   231     have "(2)": "valid ((x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2))" 

   232     proof -

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

   234       then show "valid ((x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2))" using fc1

   235         by (auto simp add: fresh_permute_left atom_eqvt valid.eqvt)	

   236     qed

   237     -- {* these two facts give us by induction hypothesis the following *}

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

   239     -- {* we now apply renamings to get to our goal *}

   240     then have "(c \<leftrightarrow> x) \<bullet> ((x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2) \<turnstile> t : T2)" by (rule permute_boolI)

   241     then have "(c, T1) # \<Gamma>2 \<turnstile> ((c \<leftrightarrow> x) \<bullet> t) : T2" using fc1

   242       by (perm_simp) (simp add: flip_fresh_fresh ty_fresh)

   243     then show "\<Gamma>2 \<turnstile> Lam [c].((c \<leftrightarrow> x) \<bullet> t) : T1 \<rightarrow> T2" using fc1 by auto

   244   qed

   245   ultimately show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" by (simp only:)

   246 qed (auto) -- {* var and app cases, luckily, are automatic *}

   247 

   248 

   249 text {* 

   250   The remedy is to use again a stronger induction principle that

   251   has the usual "variable convention" already build in. The

   252   following command derives this induction principle for the typing

   253   relation. (We shall explain what happens here later.)

   254 *}

   255 

   256 nominal_inductive typing

   257   avoids t_Lam: "x"

   258   unfolding fresh_star_def

   259   by (simp_all add: fresh_Pair lam.fresh ty_fresh)

   260 

   261 text {* Compare the two induction principles *}

   262 

   263 thm typing.induct

   264 thm typing.strong_induct -- {* note the additional assumption {atom x} \<sharp> c *}

   265 

   266 text {* 

   267   We can use the stronger induction principle by replacing

   268   the line

   269 

   270       proof (induct arbitrary: \<Gamma>2)

   271 

   272   with 

   273   

   274       proof (nominal_induct avoiding: \<Gamma>2 rule: typing.strong_induct)

   275 

   276   Try now the proof.

   277 *}

   278  

   279 subsection {* EXERCISE 9 *} 

   280 

   281 lemma weakening: 

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

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

   284   and     c: "\<Gamma>1 \<sqsubseteq> \<Gamma>2"

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

   286 using a b c

   287 proof (nominal_induct avoiding: \<Gamma>2 rule: typing.strong_induct)

   288   case (t_Var \<Gamma>1 x T)  -- {* again the variable case is as before *}

   289   have "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact 

   290   moreover  

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

   292   moreover 

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

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

   295 next

   296   case (t_Lam x \<Gamma>1 T1 t T2) 

   297   have vc: "atom x \<sharp> \<Gamma>2" by fact  -- {* additional fact afforded by the strong induction *}

   298   have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; (x, T1) # \<Gamma>1 \<sqsubseteq> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t : T2" by fact

   299   have a0: "atom x \<sharp> \<Gamma>1" by fact

   300   have a1: "valid \<Gamma>2" by fact

   301   have a2: "\<Gamma>1 \<sqsubseteq> \<Gamma>2" by fact

   302   

   303   show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" sorry

   304 qed (auto) -- {* app case *}

   305 

   306 

   307 

   308 section {* Unbind and an Inconsistency Example *}

   309 

   310 text {*

   311   You might wonder why we had to discharge some proof

   312   obligations in order to obtain the stronger induction

   313   principle for the typing relation. (Remember for

   314   lambda terms this stronger induction principle is

   315   derived automatically.)

   316   

   317   This proof obligation is really needed, because if we 

   318   assume universally a stronger induction principle, then 

   319   in some cases we can derive false. This is "shown" below.

   320 *}

   321 

   322 

   323 inductive

   324   unbind :: "lam \<Rightarrow> lam \<Rightarrow> bool" (infixr "\<mapsto>" 60)

   325 where

   326   u_Var[intro]: "Var x \<mapsto> Var x"

   327 | u_App[intro]: "App t1 t2 \<mapsto> App t1 t2"

   328 | u_Lam[intro]: "t \<mapsto> t' \<Longrightarrow> Lam [x].t \<mapsto> t'"

   329 

   330 text {* It is clear that the following judgement holds. *}

   331 

   332 lemma unbind_simple:

   333   shows "Lam [x].Var x \<mapsto> Var x"

   334   by auto

   335 

   336 text {*

   337   Now lets derive the strong induction principle for unbind.

   338   The point is that we cannot establish the proof obligations,

   339   therefore we force Isabelle to accept them by using "sorry".

   340 *}

   341 

   342 equivariance unbind

   343 nominal_inductive unbind

   344   avoids u_Lam: "x"

   345   sorry

   346 

   347 text {*

   348   Using the stronger induction principle, we can establish

   349   th follwoing bogus property.

   350 *}

   351 

   352 lemma unbind_fake:

   353   fixes y::"name"

   354   assumes a: "t \<mapsto> t'"

   355   and     b: "atom y \<sharp> t"

   356   shows "atom y \<sharp> t'"

   357 using a b

   358 proof (nominal_induct avoiding: y rule: unbind.strong_induct)

   359   case (u_Lam t t' x y)

   360   have ih: "atom y \<sharp> t \<Longrightarrow> atom y \<sharp> t'" by fact

   361   have asm: "atom y \<sharp> Lam [x]. t" by fact

   362   have fc: "atom x \<sharp> y" by fact

   363   then have in_eq: "x \<noteq> y" by (simp add: fresh_at_base)

   364   then have "atom y \<sharp> t" using asm by (simp add: lam.fresh)

   365   then show "atom y \<sharp> t'" using ih by simp

   366 qed

   367 

   368 text {*

   369   And from this follows the inconsitency:

   370 *}

   371 

   372 lemma

   373   shows "False"

   374 proof -

   375   have "atom x \<sharp> Lam [x]. Var x" by (simp add: lam.fresh)

   376   moreover 

   377   have "Lam [x]. Var x \<mapsto> Var x" using unbind_simple by auto

   378   ultimately 

   379   have "atom x \<sharp> Var x" using unbind_fake by auto

   380   then have "x \<noteq> x" by (simp add: lam.fresh fresh_at_base)

   381   then show "False" by simp

   382 qed

   383 

   384 end