diff options
Diffstat (limited to 'backends/hol4/primitivesScript.sml')
| -rw-r--r-- | backends/hol4/primitivesScript.sml | 181 |
1 files changed, 3 insertions, 178 deletions
diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml index b7bc978f..5dba408e 100644 --- a/backends/hol4/primitivesScript.sml +++ b/backends/hol4/primitivesScript.sml @@ -1173,183 +1173,6 @@ val vec_to_list_num_bounds = new_axiom ("vec_to_list_num_bounds", “!v. (0:num) <= LENGTH (vec_to_list v) /\ LENGTH (vec_to_list v) <= Num usize_max”) -(* -Theorem vec_to_list_int_bounds: - !v. 0 <= int_of_num (LENGTH (vec_to_list v)) /\ int_of_num (LENGTH (vec_to_list v)) <= usize_max -Proof - gen_tac >> - assume_tac vec_to_list_num_bounds >> - pop_assum (qspec_assume ‘v’) >> - pop_assum mp_tac >> - pure_once_rewrite_tac [GSYM INT_LE] >> - sg ‘0 ≤ usize_max’ >- (assume_tac usize_bounds >> fs [u16_max_def] >> cooper_tac) >> - metis_tac [INT_OF_NUM] -QED - -val vec_len_def = Define ‘vec_len v = int_to_usize (int_of_num (LENGTH (vec_to_list v)))’ -Theorem vec_len_spec: - ∀v. - vec_len v = int_to_usize (&(LENGTH (vec_to_list v))) ∧ - 0 ≤ &(LENGTH (vec_to_list v)) ∧ &(LENGTH (vec_to_list v)) ≤ usize_max -Proof - gen_tac >> rw [vec_len_def] >> - qspec_assume ‘v’ vec_to_list_int_bounds >> - fs [] -QED - -val mk_vec_spec = new_axiom ("mk_vec_spec", - “∀l. &(LENGTH l) ≤ usize_max ⇒ ∃v. mk_vec l = Return v ∧ vec_to_list v = l”) - -val vec_new_def = Define ‘vec_new = case mk_vec [] of Return v => v’ -Theorem vec_new_spec: - vec_to_list vec_new = [] -Proof - rw [vec_new_def] >> - qabbrev_tac ‘l = []’ >> - qspec_assume ‘l’ mk_vec_spec >> - Cases_on ‘mk_vec l’ >> - rfs [markerTheory.Abbrev_def, not_le_eq_gt] >> fs [] >> - assume_tac usize_bounds >> fs[u16_max_def] >> try_tac (exfalso >> cooper_tac) >> - sg ‘0 ≤ usize_max’ >- cooper_tac >> - fs [] -QED - -val vec_push_def = Define ‘vec_push_back v x = mk_vec (vec_to_list v ++ [x])’ -Theorem vec_push_spec: - ∀v x. usize_to_int (vec_len v) < usize_max ⇒ - ∃vx. vec_push_back v x = Return vx ∧ - vec_to_list vx = vec_to_list v ++ [x] -Proof - rpt strip_tac >> fs [vec_push_def] >> - qspec_assume ‘v’ vec_len_spec >> rw [] >> - qspec_assume ‘vec_to_list v ++ [x]’ mk_vec_spec >> - fs [vec_len_def] >> rw [] >> - pop_assum irule >> - pop_last_assum mp_tac >> - dep_rewrite.DEP_PURE_ONCE_REWRITE_TAC all_conversion_id_lemmas >> fs [] >> - cooper_tac -QED - -val update_def = Define ‘ - update ([] : 'a list) (i : num) (y : 'a) : 'a list = [] ∧ - update (_ :: ls) (0: num) y = y :: ls ∧ - update (x :: ls) (SUC i) y = x :: update ls i y -’ - -Theorem update_length: - ∀ls i y. LENGTH (update ls i y) = LENGTH ls -Proof - Induct_on ‘ls’ >> Cases_on ‘i’ >> rw [update_def] -QED - -Theorem update_spec: - ∀ls i y. i < LENGTH ls ==> - LENGTH (update ls i y) = LENGTH ls ∧ - EL i (update ls i y) = y ∧ - ∀j. j < LENGTH ls ⇒ j ≠ i ⇒ EL j (update ls i y) = EL j ls -Proof - Induct_on ‘ls’ >> Cases_on ‘i’ >> rw [update_def] >> - Cases_on ‘j’ >> fs [] -QED -*) - -(* -(* TODO: this is the base definition for index. Shall we remove the ‘return’ type? *) -val vec_index_def = Define ‘ - vec_index i v = - if usize_to_int i ≤ usize_to_int (vec_len v) - then Return (EL (Num (usize_to_int i)) (vec_to_list v)) - else Fail Failure’ -*) - -(* TODO: shortcut for qspec_then ... ASSUME_TAC *) -(* TODO: use cooper_tac everywhere *) -(* TODO: use pure_once_rewrite_tac everywhere *) - -(* -Theorem usize_to_int_inj: - ∀i j. usize_to_int i = usize_to_int j ⇔ i = j -Proof - metis_tac [int_to_usize_usize_to_int] -QED - -Theorem usize_to_int_neq_inj: - ∀i j. i <> j ==> usize_to_int i <> usize_to_int j -Proof - metis_tac [usize_to_int_inj] -QED -*) - -Theorem int_of_num_neq_inj: - ∀n m. &n ≠ &m ⇒ n ≠ m -Proof - metis_tac [int_of_num_inj] -QED - -(* TODO: automate: take assumption, intro first premise as subgoal *) - -(* TODO: I think we should express as much as we could in terms of integers (not machine integers). - - For instance: - - theorem below: ‘j <> i’ ~~> ‘usize_to_int j <> usize_to_int i’ - - we should prove theorems like: ‘usize_eq i j <=> usize_to_int i = usize_to_int j’ - (that we would automatically apply) -*) - -(* - &(SUC n) = 1 + &n - n < m - &n < &m -*) - -(* -val vec_insert_back_def = Define ‘ - vec_insert_back (v : 'a vec) (i : usize) (x : 'a) = mk_vec (update (vec_to_list v) (Num (usize_to_int i)) x)’ - -Theorem vec_insert_back_spec: - ∀v i x. - usize_to_int i < usize_to_int (vec_len v) ⇒ - ∃nv. vec_insert_back v i x = Return nv ∧ - vec_len v = vec_len nv ∧ - vec_index i nv = Return x ∧ - (* TODO: usize_to_int j ≠ usize_to_int i ? *) - (∀j. usize_to_int j < usize_to_int (vec_len nv) ⇒ j ≠ i ⇒ vec_index j nv = vec_index j v) -Proof - rpt strip_tac >> fs [vec_insert_back_def] >> - qspec_assume ‘update (vec_to_list v) (Num (usize_to_int i)) x’ mk_vec_spec >> - qspecl_assume [‘vec_to_list v’, ‘Num (usize_to_int i)’, ‘x’] update_length >> - fs [] >> - qspec_assume ‘v’ vec_len_spec >> - rw [] >> gvs [] >> - fs [vec_len_def, vec_index_def] >> - sg ‘usize_to_int (int_to_usize (&LENGTH (vec_to_list v))) = &LENGTH (vec_to_list v)’ - >-(irule usize_to_int_int_to_usize >> cooper_tac) >> - fs [] >> - qspecl_assume [‘vec_to_list v’, ‘Num (usize_to_int i)’, ‘x’] update_spec >> rfs [] >> - sg ‘Num (usize_to_int i) < LENGTH (vec_to_list v)’ >-( - (* TODO: automate *) - pure_once_rewrite_tac [gsym INT_LT] >> - dep_pure_once_rewrite_tac [int_of_num_id] >> - qspec_assume ‘i’ usize_to_int_bounds >> fs [] - ) >> - fs [] >> - (* Case: !j. j <> i ==> ... *) - rpt strip_tac >> - first_x_assum irule >> - rw [] >-( - (* TODO: automate *) - irule int_of_num_neq_inj >> - dep_pure_rewrite_tac [int_of_num_id] >> - rw [usize_to_int_bounds] >> - metis_tac [int_to_usize_usize_to_int] - ) >> - (* TODO: automate *) - pure_once_rewrite_tac [gsym INT_LT] >> - dep_pure_once_rewrite_tac [int_of_num_id] >> - qspec_assume ‘j’ usize_to_int_bounds >> fs [] -QED -*) - Theorem update_len: ∀ls i y. len (update ls i y) = len ls Proof @@ -1440,7 +1263,9 @@ Theorem vec_insert_back_spec: ∃nv. vec_insert_back v i x = Return nv ∧ vec_len v = vec_len nv ∧ vec_index i nv = Return x ∧ - (∀j. usize_to_int j < usize_to_int (vec_len nv) ⇒ usize_to_int j ≠ usize_to_int i ⇒ vec_index j nv = vec_index j v) + (∀j. usize_to_int j < usize_to_int (vec_len nv) ⇒ + usize_to_int j ≠ usize_to_int i ⇒ + vec_index j nv = vec_index j v) Proof rpt strip_tac >> fs [vec_insert_back_def] >> (* TODO: improve this? *) |