100 |
100 |
101 syntax (xsymbols output) |
101 syntax (xsymbols output) |
102 "_not_equal" :: "['a, 'a] => bool" (infix "\<noteq>" 50) |
102 "_not_equal" :: "['a, 'a] => bool" (infix "\<noteq>" 50) |
103 |
103 |
104 syntax (HTML output) |
104 syntax (HTML output) |
|
105 "_not_equal" :: "['a, 'a] => bool" (infix "\<noteq>" 50) |
105 Not :: "bool => bool" ("\<not> _" [40] 40) |
106 Not :: "bool => bool" ("\<not> _" [40] 40) |
|
107 "op &" :: "[bool, bool] => bool" (infixr "\<and>" 35) |
|
108 "op |" :: "[bool, bool] => bool" (infixr "\<or>" 30) |
|
109 "_not_equal" :: "['a, 'a] => bool" (infix "\<noteq>" 50) |
|
110 "ALL " :: "[idts, bool] => bool" ("(3\<forall>_./ _)" [0, 10] 10) |
|
111 "EX " :: "[idts, bool] => bool" ("(3\<exists>_./ _)" [0, 10] 10) |
|
112 "EX! " :: "[idts, bool] => bool" ("(3\<exists>!_./ _)" [0, 10] 10) |
106 |
113 |
107 syntax (HOL) |
114 syntax (HOL) |
108 "ALL " :: "[idts, bool] => bool" ("(3! _./ _)" [0, 10] 10) |
115 "ALL " :: "[idts, bool] => bool" ("(3! _./ _)" [0, 10] 10) |
109 "EX " :: "[idts, bool] => bool" ("(3? _./ _)" [0, 10] 10) |
116 "EX " :: "[idts, bool] => bool" ("(3? _./ _)" [0, 10] 10) |
110 "EX! " :: "[idts, bool] => bool" ("(3?! _./ _)" [0, 10] 10) |
117 "EX! " :: "[idts, bool] => bool" ("(3?! _./ _)" [0, 10] 10) |
637 |
644 |
638 syntax (xsymbols) |
645 syntax (xsymbols) |
639 "op <=" :: "['a::ord, 'a] => bool" ("op \<le>") |
646 "op <=" :: "['a::ord, 'a] => bool" ("op \<le>") |
640 "op <=" :: "['a::ord, 'a] => bool" ("(_/ \<le> _)" [50, 51] 50) |
647 "op <=" :: "['a::ord, 'a] => bool" ("(_/ \<le> _)" [50, 51] 50) |
641 |
648 |
|
649 syntax (HTML output) |
|
650 "op <=" :: "['a::ord, 'a] => bool" ("op \<le>") |
|
651 "op <=" :: "['a::ord, 'a] => bool" ("(_/ \<le> _)" [50, 51] 50) |
|
652 |
642 |
653 |
643 lemma Not_eq_iff: "((~P) = (~Q)) = (P = Q)" |
654 lemma Not_eq_iff: "((~P) = (~Q)) = (P = Q)" |
644 by blast |
655 by blast |
645 |
656 |
646 subsubsection {* Monotonicity *} |
657 subsubsection {* Monotonicity *} |
1054 "_lessAll" :: "[idt, 'a, bool] => bool" ("(3! _<_./ _)" [0, 0, 10] 10) |
1065 "_lessAll" :: "[idt, 'a, bool] => bool" ("(3! _<_./ _)" [0, 0, 10] 10) |
1055 "_lessEx" :: "[idt, 'a, bool] => bool" ("(3? _<_./ _)" [0, 0, 10] 10) |
1066 "_lessEx" :: "[idt, 'a, bool] => bool" ("(3? _<_./ _)" [0, 0, 10] 10) |
1056 "_leAll" :: "[idt, 'a, bool] => bool" ("(3! _<=_./ _)" [0, 0, 10] 10) |
1067 "_leAll" :: "[idt, 'a, bool] => bool" ("(3! _<=_./ _)" [0, 0, 10] 10) |
1057 "_leEx" :: "[idt, 'a, bool] => bool" ("(3? _<=_./ _)" [0, 0, 10] 10) |
1068 "_leEx" :: "[idt, 'a, bool] => bool" ("(3? _<=_./ _)" [0, 0, 10] 10) |
1058 |
1069 |
|
1070 syntax (HTML output) |
|
1071 "_lessAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_<_./ _)" [0, 0, 10] 10) |
|
1072 "_lessEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_<_./ _)" [0, 0, 10] 10) |
|
1073 "_leAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10) |
|
1074 "_leEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10) |
|
1075 |
1059 translations |
1076 translations |
1060 "ALL x<y. P" => "ALL x. x < y --> P" |
1077 "ALL x<y. P" => "ALL x. x < y --> P" |
1061 "EX x<y. P" => "EX x. x < y & P" |
1078 "EX x<y. P" => "EX x. x < y & P" |
1062 "ALL x<=y. P" => "ALL x. x <= y --> P" |
1079 "ALL x<=y. P" => "ALL x. x <= y --> P" |
1063 "EX x<=y. P" => "EX x. x <= y & P" |
1080 "EX x<=y. P" => "EX x. x <= y & P" |