author urbanc Sun, 21 Oct 2007 19:12:05 +0200 changeset 25138 e453c480d599 parent 25137 0835ac64834a child 25139 ffc5054a7274
```--- 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```