src/HOL/ex/Higher_Order_Logic.thy
changeset 21404 eb85850d3eb7
parent 20523 36a59e5d0039
child 23373 ead82c82da9e
     1.1 --- a/src/HOL/ex/Higher_Order_Logic.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/ex/Higher_Order_Logic.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -80,21 +80,31 @@
     1.4  subsubsection {* Derived connectives *}
     1.5  
     1.6  definition
     1.7 -  false :: o    ("\<bottom>")
     1.8 +  false :: o  ("\<bottom>") where
     1.9    "\<bottom> \<equiv> \<forall>A. A"
    1.10 -  true :: o    ("\<top>")
    1.11 +
    1.12 +definition
    1.13 +  true :: o  ("\<top>") where
    1.14    "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
    1.15 -  not :: "o \<Rightarrow> o"     ("\<not> _" [40] 40)
    1.16 +
    1.17 +definition
    1.18 +  not :: "o \<Rightarrow> o"  ("\<not> _" [40] 40) where
    1.19    "not \<equiv> \<lambda>A. A \<longrightarrow> \<bottom>"
    1.20 -  conj :: "o \<Rightarrow> o \<Rightarrow> o"    (infixr "\<and>" 35)
    1.21 +
    1.22 +definition
    1.23 +  conj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<and>" 35) where
    1.24    "conj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> C"
    1.25 -  disj :: "o \<Rightarrow> o \<Rightarrow> o"    (infixr "\<or>" 30)
    1.26 +
    1.27 +definition
    1.28 +  disj :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<or>" 30) where
    1.29    "disj \<equiv> \<lambda>A B. \<forall>C. (A \<longrightarrow> C) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> C"
    1.30 -  Ex :: "('a \<Rightarrow> o) \<Rightarrow> o"    (binder "\<exists>" 10)
    1.31 +
    1.32 +definition
    1.33 +  Ex :: "('a \<Rightarrow> o) \<Rightarrow> o"  (binder "\<exists>" 10) where
    1.34    "Ex \<equiv> \<lambda>P. \<forall>C. (\<forall>x. P x \<longrightarrow> C) \<longrightarrow> C"
    1.35  
    1.36  abbreviation
    1.37 -  not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"    (infixl "\<noteq>" 50)
    1.38 +  not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> o"  (infixl "\<noteq>" 50) where
    1.39    "x \<noteq> y \<equiv> \<not> (x = y)"
    1.40  
    1.41  theorem falseE [elim]: "\<bottom> \<Longrightarrow> A"