1 

     2 theory Tutorial2s

     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

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

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

    34   case (Var y)

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

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

    37 next    

    38   case (App t1 t2)

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

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

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

    42 next

    43   case (Lam y t1)

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

    45   moreover

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

    47   ultimately 

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

    49 qed

    50 

    51 

    52 section {* Types and the Weakening Lemma *}

    53 

    54 nominal_datatype ty =

    55   tVar "string"

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

    57 

    58 

    59 text {* 

    60   Having defined them as nominal datatypes gives us additional

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

    62  

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

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

    65   variables) and the typing judgement.

    66 *}

    67 

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

    69 

    70 inductive

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

    72 where

    73   v1[intro]: "valid []"

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

    75 

    76 

    77 inductive

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

    79 where

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

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

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

    83 

    84 

    85 text {*

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

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

    88   For example we have:

    89 *}

    90 

    91 lemma

    92   fixes x::"name"

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

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

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

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

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

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

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

   100 

   101 text {* 

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

   103 *}

   104 

   105 lemma ty_fresh:

   106   fixes x::"name"

   107   and   T::"ty"

   108   shows "atom x \<sharp> T"

   109 by (induct T rule: ty.induct)

   110    (simp_all add: ty.fresh pure_fresh)

   111 

   112 text {* 

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

   114   using the following abbreviation. Abbreviations behave like 

   115   definitions, except that they are always automatically folded 

   116   and unfolded.

   117 *}

   118 

   119 abbreviation

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

   121 where

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

   123 

   124 

   125 subsection {* EXERCISE 8 *}

   126 

   127 text {*

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

   129 *}

   130 

   131 lemma 

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

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

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

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

   136 using a b c

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

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

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

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

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

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

   143 

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

   145 next

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

   147   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

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

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

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

   151 

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

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

   154 

   155 

   156 text {* 

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

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

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

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

   161 *}

   162 

   163 equivariance valid

   164 equivariance typing

   165 

   166 lemma weakening_NOT_TO_BE_TRIED_AT_HOME: 

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

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

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

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

   171 using a b c

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

   173   -- {* lambda case *}

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

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

   176   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

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

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

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

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

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

   182   moreover

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

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

   185   proof - 

   186     -- {* we need to establish *} 

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

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

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

   190     proof -

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

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

   193         by (perm_simp) (simp add: flip_fresh_fresh)

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

   195     qed

   196     moreover 

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

   198     proof -

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

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

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

   202     qed

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

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

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

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

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

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

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

   210   qed

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

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

   213 

   214 

   215 text {* 

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

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

   218   following command derives this induction principle for the typing

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

   220 *}

   221 

   222 nominal_inductive typing

   223   avoids t_Lam: "x"

   224   unfolding fresh_star_def

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

   226 

   227 text {* Compare the two induction principles *}

   228 

   229 thm typing.induct

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

   231 

   232 text {* 

   233   We can use the stronger induction principle by replacing

   234   the line

   235 

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

   237 

   238   with 

   239   

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

   241 

   242   Try now the proof.

   243 *}

   244  

   245 subsection {* EXERCISE 9 *} 

   246 

   247 lemma weakening: 

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

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

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

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

   252 using a b c

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

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

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

   256   moreover  

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

   258   moreover 

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

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

   261 next

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

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

   264   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

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

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

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

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

   269   moreover

   270   have "(x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # \<Gamma>2" using a2 by auto

   271   ultimately 

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

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

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

   275 

   276 

   277 

   278 section {* Unbind and an Inconsistency Example *}

   279 

   280 text {*

   281   You might wonder why we had to discharge some proof

   282   obligations in order to obtain the stronger induction

   283   principle for the typing relation. (Remember for

   284   lambda terms this stronger induction principle is

   285   derived automatically.)

   286   

   287   This proof obligation is really needed, because if we 

   288   assume universally a stronger induction principle, then 

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

   290 *}

   291 

   292 

   293 inductive

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

   295 where

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

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

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

   299 

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

   301 

   302 lemma unbind_simple:

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

   304   by auto

   305 

   306 text {*

   307   Now lets derive the strong induction principle for unbind.

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

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

   310 *}

   311 

   312 equivariance unbind

   313 nominal_inductive unbind

   314   avoids u_Lam: "x"

   315   sorry

   316 

   317 text {*

   318   Using the stronger induction principle, we can establish

   319   th follwoing bogus property.

   320 *}

   321 

   322 lemma unbind_fake:

   323   fixes y::"name"

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

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

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

   327 using a b

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

   329   case (u_Lam t t' x y)

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

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

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

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

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

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

   336 qed

   337 

   338 text {*

   339   And from this follows the inconsitency:

   340 *}

   341 

   342 lemma

   343   shows "False"

   344 proof -

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

   346   moreover 

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

   348   ultimately 

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

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

   351   then show "False" by simp

   352 qed

   353 

   354 end