# HG changeset patch
# User berghofe
# Date 1203412869 -3600
# Node ID c6bd3185abb8e34430921308864ca67a4e4f865d
# Parent  51e8d37b4e7bb4b49cc984f322c7503326873d60
Yet another proof of False, this time using the strong case analysis rule.

diff -r 51e8d37b4e7b -r c6bd3185abb8 src/HOL/Nominal/Examples/VC_Condition.thy
--- a/src/HOL/Nominal/Examples/VC_Condition.thy	Mon Feb 18 22:56:53 2008 +0100
+++ b/src/HOL/Nominal/Examples/VC_Condition.thy	Tue Feb 19 10:21:09 2008 +0100
@@ -183,6 +183,23 @@
   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.