summaryrefslogtreecommitdiff
path: root/backends/hol4
diff options
context:
space:
mode:
Diffstat (limited to 'backends/hol4')
-rw-r--r--backends/hol4/ilistScript.sml14
-rw-r--r--backends/hol4/ilistTheory.sig5
-rw-r--r--backends/hol4/primitivesArithTheory.sig35
-rw-r--r--backends/hol4/primitivesScript.sml29
-rw-r--r--backends/hol4/primitivesTheory.sig24
5 files changed, 98 insertions, 9 deletions
diff --git a/backends/hol4/ilistScript.sml b/backends/hol4/ilistScript.sml
index 2183ef77..fb0c7688 100644
--- a/backends/hol4/ilistScript.sml
+++ b/backends/hol4/ilistScript.sml
@@ -16,6 +16,7 @@ val len_def = Define ‘
len [] : int = 0 /\
len (x :: ls) : int = 1 + len ls
+val _ = BasicProvers.export_rewrites ["len_def"]
(* Return the ith element of a list.
@@ -117,6 +118,7 @@ Theorem len_append:
Proof
rw [len_eq_LENGTH] >> cooper_tac
QED
+val _ = BasicProvers.export_rewrites ["len_append"]
Theorem append_len_eq:
(∀l1 l2 l1' l2'.
@@ -129,6 +131,18 @@ Proof
rw [len_eq_LENGTH] >> fs [APPEND_11_LENGTH]
QED
+Theorem drop_more_than_length:
+ ∀ ls i.
+ len ls ≤ i ⇒
+ drop i ls = []
+Proof
+ Induct_on ‘ls’ >>
+ rw [drop_def] >>
+ qspec_assume ‘ls’ len_pos >> try_tac int_tac >>
+ last_x_assum irule >>
+ int_tac
+QED
+
(* TODO: prove more theorems, and add rewriting theorems *)
val _ = export_theory ()
diff --git a/backends/hol4/ilistTheory.sig b/backends/hol4/ilistTheory.sig
index da7cdbb3..26f455d6 100644
--- a/backends/hol4/ilistTheory.sig
+++ b/backends/hol4/ilistTheory.sig
@@ -11,6 +11,7 @@ sig
(* Theorems *)
val append_len_eq : thm
val drop_eq : thm
+ val drop_more_than_length : thm
val index_eq : thm
val index_eq_EL : thm
val len_append : thm
@@ -62,6 +63,10 @@ sig
drop i (x::ls) =
if 0 < i ∨ 0 ≤ i ∧ i ≠ 0 then drop (i − 1) ls else x::ls
+ [drop_more_than_length] Theorem
+
+ ⊢ ∀ls i. len ls ≤ i ⇒ drop i ls = []
+
[index_eq] Theorem
⊢ (∀x ls. index 0 (x::ls) = x) ∧
diff --git a/backends/hol4/primitivesArithTheory.sig b/backends/hol4/primitivesArithTheory.sig
index 84b9b67a..85a627d2 100644
--- a/backends/hol4/primitivesArithTheory.sig
+++ b/backends/hol4/primitivesArithTheory.sig
@@ -15,13 +15,16 @@ sig
val le_eq_ge : thm
val lt_eq_gt : thm
val mul_pos_left_le : thm
+ val mul_pos_left_lt : thm
val mul_pos_right_le : thm
+ val mul_pos_right_lt : 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_ge : thm
val pos_div_pos_is_pos : thm
val pos_div_pos_le : thm
val pos_div_pos_le_init : thm
@@ -30,9 +33,13 @@ sig
val pos_mod_pos_is_pos : thm
val pos_mod_pos_le_init : thm
val pos_mod_pos_lt : thm
+ val pos_mul_2_div_pos_decompose : thm
val pos_mul_left_pos_le : thm
+ val pos_mul_left_pos_lt : thm
+ val pos_mul_pos_div_pos_decompose : thm
val pos_mul_pos_is_pos : thm
val pos_mul_right_pos_le : thm
+ val pos_mul_right_pos_lt : thm
val primitivesArith_grammars : type_grammar.grammar * term_grammar.grammar
(*
@@ -88,10 +95,18 @@ sig
⊢ ∀a x y. 0 ≤ a ⇒ x ≤ y ⇒ a * x ≤ a * y
+ [mul_pos_left_lt] Theorem
+
+ ⊢ ∀a x y. 0 < a ⇒ x < y ⇒ a * x < a * y
+
[mul_pos_right_le] Theorem
⊢ ∀a x y. 0 ≤ a ⇒ x ≤ y ⇒ x * a ≤ y * a
+ [mul_pos_right_lt] Theorem
+
+ ⊢ ∀a x y. 0 < a ⇒ x < y ⇒ x * a < y * a
+
[not_ge_eq_lt] Theorem
⊢ ∀x y. ¬(x ≥ y) ⇔ x < y
@@ -116,6 +131,10 @@ sig
⊢ ∀x y z. x = y − z ⇒ 0 ≤ x ⇒ 0 ≤ z ⇒ Num y = Num z + Num x
+ [pos_div_pos_ge] Theorem
+
+ ⊢ ∀x y d. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 < d ⇒ x ≥ y ⇒ x / d ≥ y / d
+
[pos_div_pos_is_pos] Theorem
⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ x / y
@@ -148,10 +167,22 @@ sig
⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x % y < y
+ [pos_mul_2_div_pos_decompose] Theorem
+
+ ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x / y + x / y ≤ x * 2 / y
+
[pos_mul_left_pos_le] Theorem
⊢ ∀a x. 0 < a ⇒ 0 ≤ x ⇒ x ≤ a * x
+ [pos_mul_left_pos_lt] Theorem
+
+ ⊢ ∀a x. 1 < a ⇒ 0 < x ⇒ x < a * x
+
+ [pos_mul_pos_div_pos_decompose] Theorem
+
+ ⊢ ∀x y z. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 < z ⇒ x / z + y / z ≤ (x + y) / z
+
[pos_mul_pos_is_pos] Theorem
⊢ ∀x y. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 ≤ x * y
@@ -160,6 +191,10 @@ sig
⊢ ∀a x. 0 < a ⇒ 0 ≤ x ⇒ x ≤ x * a
+ [pos_mul_right_pos_lt] Theorem
+
+ ⊢ ∀a x. 1 < a ⇒ 0 < x ⇒ x < x * a
+
*)
end
diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml
index 4378f9c3..82da4de9 100644
--- a/backends/hol4/primitivesScript.sml
+++ b/backends/hol4/primitivesScript.sml
@@ -1702,16 +1702,16 @@ QED
Theorem update_spec:
∀ls i y.
- 0 <= i ⇒
- i < len ls ⇒
len (update ls i y) = len ls ∧
- index i (update ls i y) = y ∧
- ∀j. j < len ls ⇒ j ≠ i ⇒ index j (update ls i y) = index j ls
+ (0 <= i ⇒
+ i < len ls ⇒
+ index i (update ls i y) = y ∧
+ ∀j. j < len ls ⇒ j ≠ i ⇒ index j (update ls i y) = index j ls)
Proof
Induct_on ‘ls’ >> Cases_on ‘i = 0’ >> rw [update_def, len_def, index_def] >>
try_tac (exfalso >> cooper_tac) >>
try_tac (
- pop_last_assum (qspecl_assume [‘i' - 1’, ‘y’]) >>
+ pop_last_assum (qspecl_assume [‘i' - 1’, ‘y’]) >> fs [] >>
pop_assum sg_premise_tac >- cooper_tac >>
pop_assum sg_premise_tac >- cooper_tac >>
rw [])
@@ -1722,6 +1722,13 @@ Proof
rw [])
QED
+Theorem len_update:
+ ∀ ls i y. len (update ls i y) = len ls
+Proof
+ fs [update_spec]
+QED
+val _ = BasicProvers.export_rewrites ["len_update"]
+
Theorem index_update_same:
∀ls i j y.
0 <= i ⇒
@@ -1832,6 +1839,18 @@ Proof
sg_dep_rewrite_all_tac index_update_same >- cooper_tac >> fs []
QED
+Theorem vec_to_list_vec_update:
+ ∀ v i x. vec_to_list (vec_update v i x) = update (vec_to_list v) (usize_to_int i) x
+Proof
+ rw [vec_update_def] >>
+ qspec_assume ‘v’ vec_len_spec >>
+ qspecl_assume [‘v’, ‘i’, ‘x’] vec_update_eq >> fs [] >>
+ qspecl_assume [‘vec_to_list v’, ‘usize_to_int i’, ‘x’] update_len >>
+ sg_dep_rewrite_all_tac mk_vec_axiom >- fs [] >>
+ fs []
+QED
+val _ = export_rewrites ["vec_to_list_vec_update"]
+
Definition vec_index_fwd_def:
vec_index_fwd v i =
if usize_to_int i ≤ usize_to_int (vec_len v)
diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig
index 7e03987b..ae7f083d 100644
--- a/backends/hol4/primitivesTheory.sig
+++ b/backends/hol4/primitivesTheory.sig
@@ -278,6 +278,7 @@ sig
val isize_sub_eq : thm
val isize_to_int_int_to_isize_i16_bounds : thm
val isize_to_int_int_to_isize_unfold : thm
+ val len_update : thm
val mk_isize_unfold : thm
val mk_usize_unfold : thm
val mk_vec_unfold : thm
@@ -349,6 +350,7 @@ sig
val vec_push_back_unfold : thm
val vec_to_list_int_bounds : thm
val vec_to_list_vec_new : thm
+ val vec_to_list_vec_update : thm
val vec_update_eq : thm
val primitives_grammars : type_grammar.grammar * term_grammar.grammar
@@ -1907,6 +1909,10 @@ sig
if i16_min ≤ n ∧ n ≤ i16_max then n
else isize_to_int (int_to_isize n)
+ [len_update] Theorem
+
+ ⊢ ∀ls i y. len (update ls i y) = len ls
+
[mk_isize_unfold] Theorem
[oracles: DISK_THM] [axioms: isize_bounds] []
@@ -2305,10 +2311,11 @@ sig
[update_spec] Theorem
⊢ ∀ls i y.
- 0 ≤ i ⇒
- i < len ls ⇒
- len (update ls i y) = len ls ∧ index i (update ls i y) = y ∧
- ∀j. j < len ls ⇒ j ≠ i ⇒ index j (update ls i y) = index j ls
+ len (update ls i y) = len ls ∧
+ (0 ≤ i ⇒
+ i < len ls ⇒
+ index i (update ls i y) = y ∧
+ ∀j. j < len ls ⇒ j ≠ i ⇒ index j (update ls i y) = index j ls)
[usize_add_eq] Theorem
@@ -2454,6 +2461,15 @@ sig
[oracles: DISK_THM] [axioms: mk_vec_axiom, usize_bounds] []
⊢ vec_to_list vec_new = []
+ [vec_to_list_vec_update] Theorem
+
+ [oracles: DISK_THM]
+ [axioms: mk_vec_axiom, usize_to_int_bounds,
+ usize_to_int_int_to_usize, usize_bounds, vec_to_list_num_bounds] []
+ ⊢ ∀v i x.
+ vec_to_list (vec_update v i x) =
+ update (vec_to_list v) (usize_to_int i) x
+
[vec_update_eq] Theorem
[oracles: DISK_THM]