author urbanc Tue, 19 Feb 2008 12:25:56 +0100 changeset 26095 04ee0a14a9f6 parent 26094 c6bd3185abb8 child 26096 783f957dcb01
slightly tuned
```--- 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```