diff options
Diffstat (limited to '')
| -rw-r--r-- | backends/hol4/primitivesScript.sml (renamed from backends/hol4/PrimitivesScript.sml) | 144 |
1 files changed, 29 insertions, 115 deletions
diff --git a/backends/hol4/PrimitivesScript.sml b/backends/hol4/primitivesScript.sml index 1f8bb1a5..56a876d4 100644 --- a/backends/hol4/PrimitivesScript.sml +++ b/backends/hol4/primitivesScript.sml @@ -1,7 +1,9 @@ open HolKernel boolLib bossLib Parse open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory -val primitives_theory_name = "Primitives" +open primitivesArithTheory + +val primitives_theory_name = "primitives" val _ = new_theory primitives_theory_name (*** Result *) @@ -502,120 +504,6 @@ val all_rem_defs = [ u128_rem_def ] -(* Ignore a theorem. - - To be used in conjunction with {!pop_assum} for instance. - *) -fun IGNORE_TAC (_ : thm) : tactic = ALL_TAC - -val POP_IGNORE_TAC = POP_ASSUM IGNORE_TAC - -(* TODO: we need a better library of lemmas about arithmetic *) - -(* TODO: add those as rewriting tactics by default *) -val NOT_LE_EQ_GT = store_thm("NOT_LE_EQ_GT", “!(x y: int). ~(x <= y) <=> x > y”, COOPER_TAC) -val NOT_LT_EQ_GE = store_thm("NOT_LT_EQ_GE", “!(x y: int). ~(x < y) <=> x >= y”, COOPER_TAC) -val NOT_GE_EQ_LT = store_thm("NOT_GE_EQ_LT", “!(x y: int). ~(x >= y) <=> x < y”, COOPER_TAC) -val NOT_GT_EQ_LE = store_thm("NOT_GT_EQ_LE", “!(x y: int). ~(x > y) <=> x <= y”, COOPER_TAC) - -Theorem POS_MUL_POS_IS_POS: - !(x y : int). 0 <= x ==> 0 <= y ==> 0 <= x * y -Proof - rpt strip_tac >> - sg ‘0 <= &(Num x) * &(Num y)’ >- (rw [INT_MUL_CALCULATE] >> COOPER_TAC) >> - sg ‘&(Num x) = x’ >- (irule EQ_SYM >> rw [INT_OF_NUM] >> COOPER_TAC) >> - sg ‘&(Num y) = y’ >- (irule EQ_SYM >> rw [INT_OF_NUM] >> COOPER_TAC) >> - metis_tac[] -QED - -val GE_EQ_LE = store_thm("GE_EQ_LE", “!(x y : int). x >= y <=> y <= x”, COOPER_TAC) -val LE_EQ_GE = store_thm("LE_EQ_GE", “!(x y : int). x <= y <=> y >= x”, COOPER_TAC) -val GT_EQ_LT = store_thm("GT_EQ_LT", “!(x y : int). x > y <=> y < x”, COOPER_TAC) -val LT_EQ_GT = store_thm("LT_EQ_GT", “!(x y : int). x < y <=> y > x”, COOPER_TAC) - -Theorem POS_DIV_POS_IS_POS: - !(x y : int). 0 <= x ==> 0 < y ==> 0 <= x / y -Proof - rpt strip_tac >> - rw [LE_EQ_GE] >> - sg ‘y <> 0’ >- COOPER_TAC >> - qspecl_then [‘\x. x >= 0’, ‘x’, ‘y’] ASSUME_TAC INT_DIV_FORALL_P >> - fs [] >> POP_IGNORE_TAC >> rw [] >- COOPER_TAC >> - fs [NOT_LT_EQ_GE] >> - (* Proof by contradiction: assume k < 0 *) - spose_not_then ASSUME_TAC >> - fs [NOT_GE_EQ_LT] >> - sg ‘k * y = (k + 1) * y + - y’ >- (fs [INT_RDISTRIB] >> COOPER_TAC) >> - sg ‘0 <= (-(k + 1)) * y’ >- (irule POS_MUL_POS_IS_POS >> COOPER_TAC) >> - COOPER_TAC -QED - -Theorem POS_DIV_POS_LE: - !(x y d : int). 0 <= x ==> 0 <= y ==> 0 < d ==> x <= y ==> x / d <= y / d -Proof - rpt strip_tac >> - sg ‘d <> 0’ >- COOPER_TAC >> - qspecl_then [‘\k. k = x / d’, ‘x’, ‘d’] ASSUME_TAC INT_DIV_P >> - qspecl_then [‘\k. k = y / d’, ‘y’, ‘d’] ASSUME_TAC INT_DIV_P >> - rfs [NOT_LT_EQ_GE] >> TRY COOPER_TAC >> - sg ‘y = (x / d) * d + (r' + y - x)’ >- COOPER_TAC >> - qspecl_then [‘(x / d) * d’, ‘r' + y - x’, ‘d’] ASSUME_TAC INT_ADD_DIV >> - rfs [] >> - Cases_on ‘x = y’ >- fs [] >> - sg ‘r' + y ≠ x’ >- COOPER_TAC >> fs [] >> - sg ‘((x / d) * d) / d = x / d’ >- (irule INT_DIV_RMUL >> COOPER_TAC) >> - fs [] >> - sg ‘0 <= (r' + y − x) / d’ >- (irule POS_DIV_POS_IS_POS >> COOPER_TAC) >> - metis_tac [INT_LE_ADDR] -QED - -Theorem POS_DIV_POS_LE_INIT: - !(x y : int). 0 <= x ==> 0 < y ==> x / y <= x -Proof - rpt strip_tac >> - sg ‘y <> 0’ >- COOPER_TAC >> - qspecl_then [‘\k. k = x / y’, ‘x’, ‘y’] ASSUME_TAC INT_DIV_P >> - rfs [NOT_LT_EQ_GE] >- COOPER_TAC >> - sg ‘y = (y - 1) + 1’ >- rw [] >> - sg ‘x = x / y + ((x / y) * (y - 1) + r)’ >-( - qspecl_then [‘1’, ‘y-1’, ‘x / y’] ASSUME_TAC INT_LDISTRIB >> - rfs [] >> - COOPER_TAC - ) >> - sg ‘!a b c. 0 <= c ==> a = b + c ==> b <= a’ >- (COOPER_TAC) >> - pop_assum irule >> - exists_tac “x / y * (y − 1) + r” >> - sg ‘0 <= x / y’ >- (irule POS_DIV_POS_IS_POS >> COOPER_TAC) >> - sg ‘0 <= (x / y) * (y - 1)’ >- (irule POS_MUL_POS_IS_POS >> COOPER_TAC) >> - COOPER_TAC -QED - -Theorem POS_MOD_POS_IS_POS: - !(x y : int). 0 <= x ==> 0 < y ==> 0 <= x % y -Proof - rpt strip_tac >> - sg ‘y <> 0’ >- COOPER_TAC >> - imp_res_tac INT_DIVISION >> - first_x_assum (qspec_then ‘x’ assume_tac) >> - first_x_assum (qspec_then ‘x’ assume_tac) >> - sg ‘~(y < 0)’ >- COOPER_TAC >> fs [] -QED - -Theorem POS_MOD_POS_LE_INIT: - !(x y : int). 0 <= x ==> 0 < y ==> x % y <= x -Proof - rpt strip_tac >> - sg ‘y <> 0’ >- COOPER_TAC >> - imp_res_tac INT_DIVISION >> - first_x_assum (qspec_then ‘x’ assume_tac) >> - first_x_assum (qspec_then ‘x’ assume_tac) >> - sg ‘~(y < 0)’ >- COOPER_TAC >> fs [] >> - sg ‘0 <= x % y’ >- (irule POS_MOD_POS_IS_POS >> COOPER_TAC) >> - sg ‘0 <= x / y’ >- (irule POS_DIV_POS_IS_POS >> COOPER_TAC) >> - sg ‘0 <= (x / y) * y’ >- (irule POS_MUL_POS_IS_POS >> COOPER_TAC) >> - COOPER_TAC -QED - (* val (asms,g) = top_goal () *) @@ -1353,4 +1241,30 @@ val all_div_eqs = [ U128_DIV_EQ ] +(*** + * Vectors + *) + +val _ = new_type ("vec", 1) +val _ = new_constant ("vec_to_list", “:'a vec -> 'a list”) + +val VEC_TO_LIST_NUM_BOUNDS = + new_axiom ( + "VEC_TO_LIST_BOUNDS", + “!v. let l = LENGTH (vec_to_list v) in + (0:num) <= l /\ l <= (4294967295:num)”) + +Theorem VEC_TO_LIST_INT_BOUNDS: + !v. let l = int_of_num (LENGTH (vec_to_list v)) in + 0 <= l /\ l <= u32_max +Proof + gen_tac >> + rw [u32_max_def] >> + assume_tac VEC_TO_LIST_NUM_BOUNDS >> + fs[] +QED + +val VEC_LEN_DEF = Define ‘vec_len v = int_to_u32 (int_of_num (LENGTH (vec_to_list v)))’ + + val _ = export_theory () |