blob: 3b157b873c9853423bc6ccb8df151ac4b5c5c757 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
|
signature primitivesArithTheory =
sig
type thm = Thm.thm
(* Theorems *)
val GE_EQ_LE : thm
val GT_EQ_LT : thm
val INT_OF_NUM_INJ : thm
val LE_EQ_GE : thm
val LT_EQ_GT : thm
val NOT_GE_EQ_LT : thm
val NOT_GT_EQ_LE : thm
val NOT_LE_EQ_GT : thm
val NOT_LT_EQ_GE : thm
val NUM_SUB_1_EQ : thm
val NUM_SUB_EQ : thm
val POS_DIV_POS_IS_POS : thm
val POS_DIV_POS_LE : thm
val POS_DIV_POS_LE_INIT : thm
val POS_MOD_POS_IS_POS : thm
val POS_MOD_POS_LE_INIT : thm
val POS_MUL_POS_IS_POS : thm
val primitivesArith_grammars : type_grammar.grammar * term_grammar.grammar
(*
[Omega] Parent theory of "primitivesArith"
[int_arith] Parent theory of "primitivesArith"
[GE_EQ_LE] Theorem
⊢ ∀x y. x ≥ y ⇔ y ≤ x
[GT_EQ_LT] Theorem
⊢ ∀x y. x > y ⇔ y < x
[INT_OF_NUM_INJ] Theorem
⊢ ∀n m. &n = &m ⇒ n = m
[LE_EQ_GE] Theorem
⊢ ∀x y. x ≤ y ⇔ y ≥ x
[LT_EQ_GT] Theorem
⊢ ∀x y. x < y ⇔ y > x
[NOT_GE_EQ_LT] Theorem
⊢ ∀x y. ¬(x ≥ y) ⇔ x < y
[NOT_GT_EQ_LE] Theorem
⊢ ∀x y. ¬(x > y) ⇔ x ≤ y
[NOT_LE_EQ_GT] Theorem
⊢ ∀x y. ¬(x ≤ y) ⇔ x > y
[NOT_LT_EQ_GE] Theorem
⊢ ∀x y. ¬(x < y) ⇔ x ≥ y
[NUM_SUB_1_EQ] Theorem
⊢ ∀x y. x = y − 1 ⇒ 0 ≤ x ⇒ Num y = SUC (Num x)
[NUM_SUB_EQ] Theorem
⊢ ∀x y z. x = y − z ⇒ 0 ≤ x ⇒ 0 ≤ z ⇒ Num y = Num z + Num x
[POS_DIV_POS_IS_POS] Theorem
⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ x / y
[POS_DIV_POS_LE] Theorem
⊢ ∀x y d. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 < d ⇒ x ≤ y ⇒ x / d ≤ y / d
[POS_DIV_POS_LE_INIT] Theorem
⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x / y ≤ x
[POS_MOD_POS_IS_POS] Theorem
⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ x % y
[POS_MOD_POS_LE_INIT] Theorem
⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x % y ≤ x
[POS_MUL_POS_IS_POS] Theorem
⊢ ∀x y. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 ≤ x * y
*)
end
|
