summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | berghofe |

Tue, 19 Feb 2008 10:21:09 +0100 | |

changeset 26094 | c6bd3185abb8 |

parent 26093 | 51e8d37b4e7b |

child 26095 | 04ee0a14a9f6 |

Yet another proof of False, this time using the strong case analysis rule.

--- 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.