added auxiliary lemma for code generation 2
authorhaftmann
Tue Sep 19 15:22:35 2006 +0200 (2006-09-19)
changeset 206049dba9c7872c9
parent 20603 37dfd7af2746
child 20605 56e4bb01fd99
added auxiliary lemma for code generation 2
src/HOL/Inductive.thy
     1.1 --- a/src/HOL/Inductive.thy	Tue Sep 19 15:22:29 2006 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Tue Sep 19 15:22:35 2006 +0200
     1.3 @@ -70,6 +70,26 @@
     1.4    Ball_def Bex_def
     1.5    induct_rulify_fallback
     1.6  
     1.7 +lemma False_meta_all:
     1.8 +  "Trueprop False \<equiv> (\<And>P\<Colon>bool. P)"
     1.9 +proof
    1.10 +  fix P
    1.11 +  assume False
    1.12 +  then show P ..
    1.13 +next
    1.14 +  assume "\<And>P\<Colon>bool. P"
    1.15 +  then show "False" ..
    1.16 +qed
    1.17 +
    1.18 +lemma not_eq_False:
    1.19 +  assumes not_eq: "x \<noteq> y"
    1.20 +  and eq: "x == y"
    1.21 +  shows False
    1.22 +  using not_eq eq by auto
    1.23 +
    1.24 +lemmas not_eq_quodlibet =
    1.25 +  not_eq_False [simplified False_meta_all]
    1.26 +
    1.27  
    1.28  subsection {* Inductive datatypes and primitive recursion *}
    1.29