src/HOL/HOL.thy
 changeset 62151 dc4c9748a86e parent 61955 e96292f32c3c child 62390 842917225d56
```     1.1 --- a/src/HOL/HOL.thy	Tue Jan 12 11:48:43 2016 +0100
1.2 +++ b/src/HOL/HOL.thy	Tue Jan 12 11:49:35 2016 +0100
1.3 @@ -69,25 +69,38 @@
1.4
1.5  typedecl bool
1.6
1.7 -judgment
1.8 -  Trueprop      :: "bool \<Rightarrow> prop"                   ("(_)" 5)
1.9 +judgment Trueprop :: "bool \<Rightarrow> prop"  ("(_)" 5)
1.10 +
1.11 +axiomatization implies :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<longrightarrow>" 25)
1.12 +  and eq :: "['a, 'a] \<Rightarrow> bool"  (infixl "=" 50)
1.13 +  and The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
1.14 +
1.15
1.16 -axiomatization
1.17 -  implies       :: "[bool, bool] \<Rightarrow> bool"           (infixr "\<longrightarrow>" 25)  and
1.18 -  eq            :: "['a, 'a] \<Rightarrow> bool"               (infixl "=" 50)  and
1.19 -  The           :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
1.20 +subsubsection \<open>Defined connectives and quantifiers\<close>
1.21 +
1.22 +definition True :: bool
1.23 +  where "True \<equiv> ((\<lambda>x::bool. x) = (\<lambda>x. x))"
1.24 +
1.25 +definition All :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<forall>" 10)
1.26 +  where "All P \<equiv> (P = (\<lambda>x. True))"
1.27
1.28 -consts
1.29 -  True          :: bool
1.30 -  False         :: bool
1.31 -  Not           :: "bool \<Rightarrow> bool"                   ("\<not> _" [40] 40)
1.32 +definition Ex :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<exists>" 10)
1.33 +  where "Ex P \<equiv> \<forall>Q. (\<forall>x. P x \<longrightarrow> Q) \<longrightarrow> Q"
1.34 +
1.35 +definition False :: bool
1.36 +  where "False \<equiv> (\<forall>P. P)"
1.37 +
1.38 +definition Not :: "bool \<Rightarrow> bool"  ("\<not> _" [40] 40)
1.39 +  where not_def: "\<not> P \<equiv> P \<longrightarrow> False"
1.40
1.41 -  conj          :: "[bool, bool] \<Rightarrow> bool"           (infixr "\<and>" 35)
1.42 -  disj          :: "[bool, bool] \<Rightarrow> bool"           (infixr "\<or>" 30)
1.43 +definition conj :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<and>" 35)
1.44 +  where and_def: "P \<and> Q \<equiv> \<forall>R. (P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> R"
1.45
1.46 -  All           :: "('a \<Rightarrow> bool) \<Rightarrow> bool"           (binder "\<forall>" 10)
1.47 -  Ex            :: "('a \<Rightarrow> bool) \<Rightarrow> bool"           (binder "\<exists>" 10)
1.48 -  Ex1           :: "('a \<Rightarrow> bool) \<Rightarrow> bool"           (binder "\<exists>!" 10)
1.49 +definition disj :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<or>" 30)
1.50 +  where or_def: "P \<or> Q \<equiv> \<forall>R. (P \<longrightarrow> R) \<longrightarrow> (Q \<longrightarrow> R) \<longrightarrow> R"
1.51 +
1.52 +definition Ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<exists>!" 10)
1.53 +  where "Ex1 P \<equiv> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x)"
1.54
1.55
1.57 @@ -167,16 +180,6 @@
1.58    iff: "(P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P) \<longrightarrow> (P = Q)" and
1.59    True_or_False: "(P = True) \<or> (P = False)"
1.60
1.61 -defs
1.62 -  True_def:     "True      \<equiv> ((\<lambda>x::bool. x) = (\<lambda>x. x))"
1.63 -  All_def:      "All P     \<equiv> (P = (\<lambda>x. True))"
1.64 -  Ex_def:       "Ex P      \<equiv> \<forall>Q. (\<forall>x. P x \<longrightarrow> Q) \<longrightarrow> Q"
1.65 -  False_def:    "False     \<equiv> (\<forall>P. P)"
1.66 -  not_def:      "\<not> P       \<equiv> P \<longrightarrow> False"
1.67 -  and_def:      "P \<and> Q     \<equiv> \<forall>R. (P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> R"
1.68 -  or_def:       "P \<or> Q     \<equiv> \<forall>R. (P \<longrightarrow> R) \<longrightarrow> (Q \<longrightarrow> R) \<longrightarrow> R"
1.69 -  Ex1_def:      "Ex1 P     \<equiv> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x)"
1.70 -
1.71  definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10)
1.72    where "If P x y \<equiv> (THE z::'a. (P = True \<longrightarrow> z = x) \<and> (P = False \<longrightarrow> z = y))"
1.73
```