79 typedecl bool |
79 typedecl bool |
80 |
80 |
81 judgment Trueprop :: "bool \<Rightarrow> prop" ("(_)" 5) |
81 judgment Trueprop :: "bool \<Rightarrow> prop" ("(_)" 5) |
82 |
82 |
83 axiomatization implies :: "[bool, bool] \<Rightarrow> bool" (infixr "\<longrightarrow>" 25) |
83 axiomatization implies :: "[bool, bool] \<Rightarrow> bool" (infixr "\<longrightarrow>" 25) |
84 and eq :: "['a, 'a] \<Rightarrow> bool" (infixl "=" 50) |
84 and eq :: "['a, 'a] \<Rightarrow> bool" |
85 and The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" |
85 and The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" |
86 |
86 |
|
87 notation (input) |
|
88 eq (infixl "=" 50) |
|
89 notation (output) |
|
90 eq (infix "=" 50) |
|
91 |
|
92 text \<open>The input syntax for \<open>eq\<close> is more permissive than the output syntax |
|
93 because of the large amount of material that relies on infixl.\<close> |
87 |
94 |
88 subsubsection \<open>Defined connectives and quantifiers\<close> |
95 subsubsection \<open>Defined connectives and quantifiers\<close> |
89 |
96 |
90 definition True :: bool |
97 definition True :: bool |
91 where "True \<equiv> ((\<lambda>x::bool. x) = (\<lambda>x. x))" |
98 where "True \<equiv> ((\<lambda>x::bool. x) = (\<lambda>x. x))" |
132 translations |
139 translations |
133 "\<nexists>x. P" \<rightleftharpoons> "\<not> (\<exists>x. P)" |
140 "\<nexists>x. P" \<rightleftharpoons> "\<not> (\<exists>x. P)" |
134 "\<nexists>!x. P" \<rightleftharpoons> "\<not> (\<exists>!x. P)" |
141 "\<nexists>!x. P" \<rightleftharpoons> "\<not> (\<exists>!x. P)" |
135 |
142 |
136 |
143 |
137 abbreviation not_equal :: "['a, 'a] \<Rightarrow> bool" (infixl "\<noteq>" 50) |
144 abbreviation not_equal :: "['a, 'a] \<Rightarrow> bool" (infix "\<noteq>" 50) |
138 where "x \<noteq> y \<equiv> \<not> (x = y)" |
145 where "x \<noteq> y \<equiv> \<not> (x = y)" |
139 |
|
140 notation (output) |
|
141 eq (infix "=" 50) and |
|
142 not_equal (infix "\<noteq>" 50) |
|
143 |
|
144 notation (ASCII output) |
|
145 not_equal (infix "~=" 50) |
|
146 |
146 |
147 notation (ASCII) |
147 notation (ASCII) |
148 Not ("~ _" [40] 40) and |
148 Not ("~ _" [40] 40) and |
149 conj (infixr "&" 35) and |
149 conj (infixr "&" 35) and |
150 disj (infixr "|" 30) and |
150 disj (infixr "|" 30) and |
151 implies (infixr "-->" 25) and |
151 implies (infixr "-->" 25) and |
152 not_equal (infixl "~=" 50) |
152 not_equal (infix "~=" 50) |
153 |
153 |
154 abbreviation (iff) |
154 abbreviation (iff) |
155 iff :: "[bool, bool] \<Rightarrow> bool" (infixr "\<longleftrightarrow>" 25) |
155 iff :: "[bool, bool] \<Rightarrow> bool" (infixr "\<longleftrightarrow>" 25) |
156 where "A \<longleftrightarrow> B \<equiv> A = B" |
156 where "A \<longleftrightarrow> B \<equiv> A = B" |
157 |
157 |