eliminated old defs;
authorwenzelm
Tue Jan 12 11:49:35 2016 +0100 (2016-01-12)
changeset 62151dc4c9748a86e
parent 62150 33ce5f41a9e1
child 62152 7023a007712e
eliminated old defs;
src/HOL/HOL.thy
     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.56  subsubsection \<open>Additional concrete syntax\<close>
    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