# HG changeset patch
# User urbanc
# Date 1192986725 -7200
# Node ID e453c480d59953362448211fcf40ed00f0e310b2
# Parent  0835ac64834a93556d7189c7d545fedc2e33a21d
further comments

diff -r 0835ac64834a -r e453c480d599 src/HOL/Nominal/Examples/Weakening.thy
--- a/src/HOL/Nominal/Examples/Weakening.thy	Sun Oct 21 19:04:53 2007 +0200
+++ b/src/HOL/Nominal/Examples/Weakening.thy	Sun Oct 21 19:12:05 2007 +0200
@@ -155,7 +155,7 @@
   have ih: "\<And>\<Gamma>3. \<lbrakk>valid \<Gamma>3; (x,T1)#\<Gamma>1 \<subseteq> \<Gamma>3\<rbrakk> \<Longrightarrow> \<Gamma>3 \<turnstile> t : T2" by fact
   obtain c::"name" where fc1: "c\<sharp>(x,t,\<Gamma>1,\<Gamma>2)"  (* we obtain a fresh name *)
     by (rule exists_fresh) (auto simp add: fs_name1)
-  have "Lam [c].([(c,x)]\<bullet>t) = Lam [x].t" using fc1 (* we alpha-rename the lambda-abstraction *)
+  have "Lam [c].([(c,x)]\<bullet>t) = Lam [x].t" using fc1 (* we then alpha-rename the lambda-abstraction *)
     by (auto simp add: lam.inject alpha fresh_prod fresh_atm)
   moreover
   have "\<Gamma>2 \<turnstile> Lam [c].([(c,x)]\<bullet>t) : T1 \<rightarrow> T2" (* we can then alpha-rename our original goal *)
@@ -177,7 +177,7 @@
     qed
     (* these two facts give us by induction hypothesis the following *)
     ultimately have "(x,T1)#([(c,x)]\<bullet>\<Gamma>2) \<turnstile> t : T2" using ih by simp 
-    (* we now apply renamings to get our goal *)
+    (* we now apply renamings to get to our goal *)
     then have "[(c,x)]\<bullet>((x,T1)#([(c,x)]\<bullet>\<Gamma>2) \<turnstile> t : T2)" by (rule perm_boolI)
     then have "(c,T1)#\<Gamma>2 \<turnstile> ([(c,x)]\<bullet>t) : T2" using fc1 
       by (perm_simp add: eqvts calc_atm perm_fresh_fresh ty_fresh)
@@ -186,4 +186,9 @@
   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. *}
+
 end
\ No newline at end of file