565 

   661 

   700 section {* Types *}

   701 

   702 nominal_datatype ty =

   703   tVar "string"

   704 | tArr "ty" "ty" ("_ \<rightarrow> _" [100, 100] 100)

   705 

   706 

   707 text {* 

   708   Having defined them as nominal datatypes gives us additional

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

   710  

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

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

   713   variables) and the typing judgement.

   714 

   715 *}

   716 

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

   718 

   719 

   720 inductive

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

   722 where

   723   v1[intro]: "valid []"

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

   725 

   726 

   727 inductive

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

   729 where

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

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

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

   733 

   734 

   735 text {*

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

   737   Nominal Isabelle. Freshness is defined for lambda-terms, products, 

   738   lists etc. For example we have:

   739   *}

   740 

   741 lemma

   742   fixes x::"name"

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

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

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

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

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

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

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

   750 

   751 text {* 

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

   753 *}

   754 

   755 lemma ty_fresh:

   756   fixes x::"name"

   757   and   T::"ty"

   758   shows "atom x \<sharp> T"

   759 by (induct T rule: ty.induct)

   760    (simp_all add: ty.fresh pure_fresh)

   761 

   762 text {* 

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

   764   using the following abbreviation. Abbreviations behave like 

   765   definitions, except that they are always automatically folded 

   766   and unfolded.

   767 *}

   768 

   769 abbreviation

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

   771 where

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

   773 

   774 

   775 subsection {* EXERCISE 4 *}

   776 

   777 text {*

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

   779 *}

   780 

   781 lemma 

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

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

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

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

   786 using a b c

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

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

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

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

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

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

   793 

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

   795 next

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

   797   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

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

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

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

   801 

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

   803 qed (auto) -- {* the application case *}

   804 

   805 

   806 text {* 

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

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

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

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

   811 *}

   812 

   813 equivariance valid

   814 equivariance typing

   815 

   816 lemma weakening_NOT_TO_BE_TRIED_AT_HOME: 

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

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

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

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

   821 using a b c

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

   823   -- {* lambda case *}

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

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

   826   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

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

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

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

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

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

   832   moreover

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

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

   835   proof - 

   836     -- {* we need to establish 

   837            *   (x, T1) # \<Gamma>1 \<sqsubseteq> (x, T1) # ((c \<leftrightarrow> x) \<bullet> \<Gamma>2) and 

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

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

   840     proof -

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

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

   843         by (perm_simp) (simp add: flip_fresh_fresh)

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

   845     qed

   846     moreover 

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

   848     proof -

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

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

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

   852     qed

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

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

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

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

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

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

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

   860   qed

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

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

   863 

   864 

   865 text {* 

   866   The remedy is to use a stronger induction principle that

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

   868   following command derives this induction principle for us.

   869   (We shall explain what happens here later.)

   870 *}

   871 

   872 nominal_inductive typing

   873   avoids t_Lam: "x"

   874   unfolding fresh_star_def

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

   876 

   877 text {* Compare the two induction principles *}

   878 

   879 thm typing.induct

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

   881 

   882 text {* 

   883   We can use the stronger induction principle by replacing

   884   the line

   885 

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

   887 

   888   with 

   889   

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

   891 

   892   Try now the proof.

   893 *}

   894   

   895 

   896 lemma weakening: 

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

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

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

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

   901 using a b c

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

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

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

   905   moreover  

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

   907   moreover 

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

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

   910 next

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

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

   913   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

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

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

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

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

   918   moreover

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

   920   ultimately 

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

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

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

  1117   fixes z::"name"