1107 "_lessAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<_./ _)" [0, 0, 10] 10) |
1107 "_lessAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<_./ _)" [0, 0, 10] 10) |
1108 "_lessEx" :: "[idt, 'a, bool] => bool" ("(3EX _<_./ _)" [0, 0, 10] 10) |
1108 "_lessEx" :: "[idt, 'a, bool] => bool" ("(3EX _<_./ _)" [0, 0, 10] 10) |
1109 "_leAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<=_./ _)" [0, 0, 10] 10) |
1109 "_leAll" :: "[idt, 'a, bool] => bool" ("(3ALL _<=_./ _)" [0, 0, 10] 10) |
1110 "_leEx" :: "[idt, 'a, bool] => bool" ("(3EX _<=_./ _)" [0, 0, 10] 10) |
1110 "_leEx" :: "[idt, 'a, bool] => bool" ("(3EX _<=_./ _)" [0, 0, 10] 10) |
1111 |
1111 |
|
1112 "_gtAll" :: "[idt, 'a, bool] => bool" ("(3ALL _>_./ _)" [0, 0, 10] 10) |
|
1113 "_gtEx" :: "[idt, 'a, bool] => bool" ("(3EX _>_./ _)" [0, 0, 10] 10) |
|
1114 "_geAll" :: "[idt, 'a, bool] => bool" ("(3ALL _>=_./ _)" [0, 0, 10] 10) |
|
1115 "_geEx" :: "[idt, 'a, bool] => bool" ("(3EX _>=_./ _)" [0, 0, 10] 10) |
|
1116 |
1112 syntax (xsymbols) |
1117 syntax (xsymbols) |
1113 "_lessAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_<_./ _)" [0, 0, 10] 10) |
1118 "_lessAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_<_./ _)" [0, 0, 10] 10) |
1114 "_lessEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_<_./ _)" [0, 0, 10] 10) |
1119 "_lessEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_<_./ _)" [0, 0, 10] 10) |
1115 "_leAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10) |
1120 "_leAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10) |
1116 "_leEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10) |
1121 "_leEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10) |
1117 |
1122 |
|
1123 "_gtAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_>_./ _)" [0, 0, 10] 10) |
|
1124 "_gtEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_>_./ _)" [0, 0, 10] 10) |
|
1125 "_geAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10) |
|
1126 "_geEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10) |
|
1127 |
1118 syntax (HOL) |
1128 syntax (HOL) |
1119 "_lessAll" :: "[idt, 'a, bool] => bool" ("(3! _<_./ _)" [0, 0, 10] 10) |
1129 "_lessAll" :: "[idt, 'a, bool] => bool" ("(3! _<_./ _)" [0, 0, 10] 10) |
1120 "_lessEx" :: "[idt, 'a, bool] => bool" ("(3? _<_./ _)" [0, 0, 10] 10) |
1130 "_lessEx" :: "[idt, 'a, bool] => bool" ("(3? _<_./ _)" [0, 0, 10] 10) |
1121 "_leAll" :: "[idt, 'a, bool] => bool" ("(3! _<=_./ _)" [0, 0, 10] 10) |
1131 "_leAll" :: "[idt, 'a, bool] => bool" ("(3! _<=_./ _)" [0, 0, 10] 10) |
1122 "_leEx" :: "[idt, 'a, bool] => bool" ("(3? _<=_./ _)" [0, 0, 10] 10) |
1132 "_leEx" :: "[idt, 'a, bool] => bool" ("(3? _<=_./ _)" [0, 0, 10] 10) |
1125 "_lessAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_<_./ _)" [0, 0, 10] 10) |
1135 "_lessAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_<_./ _)" [0, 0, 10] 10) |
1126 "_lessEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_<_./ _)" [0, 0, 10] 10) |
1136 "_lessEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_<_./ _)" [0, 0, 10] 10) |
1127 "_leAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10) |
1137 "_leAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10) |
1128 "_leEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10) |
1138 "_leEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10) |
1129 |
1139 |
|
1140 "_gtAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_>_./ _)" [0, 0, 10] 10) |
|
1141 "_gtEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_>_./ _)" [0, 0, 10] 10) |
|
1142 "_geAll" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10) |
|
1143 "_geEx" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10) |
|
1144 |
1130 translations |
1145 translations |
1131 "ALL x<y. P" => "ALL x. x < y --> P" |
1146 "ALL x<y. P" => "ALL x. x < y --> P" |
1132 "EX x<y. P" => "EX x. x < y & P" |
1147 "EX x<y. P" => "EX x. x < y & P" |
1133 "ALL x<=y. P" => "ALL x. x <= y --> P" |
1148 "ALL x<=y. P" => "ALL x. x <= y --> P" |
1134 "EX x<=y. P" => "EX x. x <= y & P" |
1149 "EX x<=y. P" => "EX x. x <= y & P" |
|
1150 "ALL x>y. P" => "ALL x. x > y --> P" |
|
1151 "EX x>y. P" => "EX x. x > y & P" |
|
1152 "ALL x>=y. P" => "ALL x. x >= y --> P" |
|
1153 "EX x>=y. P" => "EX x. x >= y & P" |
1135 |
1154 |
1136 print_translation {* |
1155 print_translation {* |
1137 let |
1156 let |
1138 fun all_tr' [Const ("_bound",_) $ Free (v,_), |
1157 fun all_tr' [Const ("_bound",_) $ Free (v,_), |
1139 Const("op -->",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = |
1158 Const("op -->",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = |