54 order_less_le "x < y = (x <= y & x ~= y)" |
54 order_less_le "x < y = (x <= y & x ~= y)" |
55 |
55 |
56 axclass linorder < order |
56 axclass linorder < order |
57 linorder_linear "x <= y | y <= x" |
57 linorder_linear "x <= y | y <= x" |
58 |
58 |
59 (*bounded quantifiers*) |
59 |
|
60 (* bounded quantifiers *) |
|
61 |
60 syntax |
62 syntax |
61 "@lessAll" :: [idt, 'a, bool] => bool ("(3! _<_./ _)" [0, 0, 10] 10) |
63 "_lessAll" :: [idt, 'a, bool] => bool ("(3ALL _<_./ _)" [0, 0, 10] 10) |
62 "@lessEx" :: [idt, 'a, bool] => bool ("(3? _<_./ _)" [0, 0, 10] 10) |
64 "_lessEx" :: [idt, 'a, bool] => bool ("(3EX _<_./ _)" [0, 0, 10] 10) |
63 "@leAll" :: [idt, 'a, bool] => bool ("(3! _<=_./ _)" [0, 0, 10] 10) |
65 "_leAll" :: [idt, 'a, bool] => bool ("(3ALL _<=_./ _)" [0, 0, 10] 10) |
64 "@leEx" :: [idt, 'a, bool] => bool ("(3? _<=_./ _)" [0, 0, 10] 10) |
66 "_leEx" :: [idt, 'a, bool] => bool ("(3EX _<=_./ _)" [0, 0, 10] 10) |
|
67 |
|
68 syntax (symbols) |
|
69 "_lessAll" :: [idt, 'a, bool] => bool ("(3\\<forall>_<_./ _)" [0, 0, 10] 10) |
|
70 "_lessEx" :: [idt, 'a, bool] => bool ("(3\\<exists>_<_./ _)" [0, 0, 10] 10) |
|
71 "_leAll" :: [idt, 'a, bool] => bool ("(3\\<forall>_<=_./ _)" [0, 0, 10] 10) |
|
72 "_leEx" :: [idt, 'a, bool] => bool ("(3\\<exists>_<=_./ _)" [0, 0, 10] 10) |
|
73 |
|
74 syntax (HOL) |
|
75 "_lessAll" :: [idt, 'a, bool] => bool ("(3! _<_./ _)" [0, 0, 10] 10) |
|
76 "_lessEx" :: [idt, 'a, bool] => bool ("(3? _<_./ _)" [0, 0, 10] 10) |
|
77 "_leAll" :: [idt, 'a, bool] => bool ("(3! _<=_./ _)" [0, 0, 10] 10) |
|
78 "_leEx" :: [idt, 'a, bool] => bool ("(3? _<=_./ _)" [0, 0, 10] 10) |
|
79 |
65 translations |
80 translations |
66 "! x<y. P" => "! x. x < y --> P" |
81 "ALL x<y. P" => "ALL x. x < y --> P" |
67 "! x<=y. P" => "! x. x <= y --> P" |
82 "EX x<y. P" => "EX x. x < y & P" |
68 "? x<y. P" => "? x. x < y & P" |
83 "ALL x<=y. P" => "ALL x. x <= y --> P" |
69 "? x<=y. P" => "? x. x <= y & P" |
84 "EX x<=y. P" => "EX x. x <= y & P" |
|
85 |
70 |
86 |
71 end |
87 end |