backends/hol4/primitivesArithTheory.sig


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
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115

signature primitivesArithTheory =
sig
  type thm = Thm.thm
  
  (*  Theorems  *)
    val ge_eq_le : thm
    val gt_eq_lt : thm
    val int_add : thm
    val int_induction : thm
    val int_of_num : 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_add]  Theorem
      
      ⊢ ∀m n. &(m + n) = &m + &n
   
   [int_induction]  Theorem
      
      ⊢ ∀P. P 0 ∧ (∀i. 0 ≤ i ∧ P i ⇒ P (i + 1)) ⇒ ∀i. 0 ≤ i ⇒ P i
   
   [int_of_num]  Theorem
      
      ⊢ ∀i. 0 ≤ i ⇒ &Num i = i
   
   [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