# HG changeset patch
# User urbanc
# Date 1203420356 -3600
# Node ID 04ee0a14a9f6ee55cd9900056b39bbda44aa3fe5
# Parent  c6bd3185abb8e34430921308864ca67a4e4f865d
slightly tuned

diff -r c6bd3185abb8 -r 04ee0a14a9f6 src/HOL/Nominal/Examples/VC_Condition.thy
--- a/src/HOL/Nominal/Examples/VC_Condition.thy	Tue Feb 19 10:21:09 2008 +0100
+++ b/src/HOL/Nominal/Examples/VC_Condition.thy	Tue Feb 19 12:25:56 2008 +0100
@@ -183,27 +183,30 @@
   then show "False" by (simp add: fresh_atm)
 qed 
 
-text {* A similar effect can be achieved using the strong case analysis rule. *}
-
-lemma false3: "False"
-proof -
-  have "Lam [x].(Var x) \<rightarrow> (Var x)" by (iprover intro: strip.intros)
-  moreover obtain y::name where y: "y \<sharp> x"
-    by (rule exists_fresh) (rule fin_supp)
-  then have "(Lam [x].(Var x)) = (Lam [y].(Var y))"
-    by (simp add: lam.inject alpha calc_atm fresh_atm)
-  ultimately have "Lam [y].(Var y) \<rightarrow> (Var x)" by simp
-  then have "Var y \<rightarrow> Var x" using y
-    by (cases rule: strip.strong_cases [where x=y])
-      (simp_all add: lam.inject alpha abs_fresh)
-  then show "False" using y
-    by cases (simp_all add: lam.inject fresh_atm)
-qed
-
 text {*
   Moral: Who would have thought that the variable convention 
   is in general an unsound reasoning principle.
   *}
 
- 
+
+text 
+  {* BTW: A similar effect can be achieved by using naive (that
+     is strong) inversion rules. *}
+
+lemma false3: 
+  shows "False"
+proof -
+  have "Lam [x].(Var x) \<rightarrow> (Var x)" by (auto intro: strip.intros)
+  moreover obtain y::name where y: "y\<sharp>x"
+    by (rule exists_fresh) (rule fin_supp)
+  then have "Lam [x].(Var x) = Lam [y].(Var y)"
+    by (simp add: lam.inject alpha calc_atm fresh_atm)
+  ultimately have "Lam [y].(Var y) \<rightarrow> (Var x)" by simp
+  then have "Var y \<rightarrow> Var x" using y
+    by (cases rule: strip.strong_cases [where x=y])
+       (simp_all add: lam.inject alpha abs_fresh)
+  then show "False" using y
+    by (cases) (simp_all add: lam.inject fresh_atm)
+qed
+
 end
\ No newline at end of file