src/HOL/Nominal/Examples/Weakening.thy

 
 theory Weakening 
   imports "../Nominal" 
 begin
 
-section {* Weakening Example for the Simply-Typed Lambda-Calculus *}
+section {* Weakening Property in the Simply-Typed Lambda-Calculus *}
 
 atom_decl name 
 
-text {* Terms and types *}
+text {* Terms and Types *}
 nominal_datatype lam = 
     Var "name"
   | App "lam" "lam"
   | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
 

   | t_Lam[intro]: "\<lbrakk>x\<sharp>\<Gamma>;(x,T1)#\<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T1\<rightarrow>T2"
 
 text {* 
   We derive the strong induction principle for the typing 
   relation (this induction principle has the variable convention 
-  already built in). 
+  already built-in). 
   *}
 equivariance typing
 nominal_inductive typing
   by (simp_all add: abs_fresh ty_fresh)
 

   moreover
   have "valid ((x,T1)#\<Gamma>2)" using v2 (* fails *) 
     oops
   
 text{* The complete proof without using the variable convention. *}
+
 lemma weakening_with_explicit_renaming: 
   fixes \<Gamma>1 \<Gamma>2::"(name\<times>ty) list"
   assumes a: "\<Gamma>1 \<turnstile> t : T"
   and     b: "valid \<Gamma>2" 
   and     c: "\<Gamma>1 \<subseteq> \<Gamma>2"

   qed
   ultimately show "\<Gamma>2 \<turnstile> Lam [x].t : T1 \<rightarrow> T2" by simp
 qed (auto)
 
 text {*
-  Compare the proof with explicit renamings to version1 and version2,
-  and imagine you are proving something more substantial than the
-  weakening lemma. 
+  Moral: compare the proof with explicit renamings to version1 and version2,
+  and imagine you are proving something more substantial than the weakening 
+  lemma. 
   *}
 
 end