summaryrefslogtreecommitdiff
path: root/backends/hol4
diff options
context:
space:
mode:
Diffstat (limited to 'backends/hol4')
-rw-r--r--backends/hol4/primitivesBaseTacLib.sml399
-rw-r--r--backends/hol4/primitivesScript.sml177
-rw-r--r--backends/hol4/primitivesTheory.sig393
-rw-r--r--backends/hol4/testScript.sml8
4 files changed, 890 insertions, 87 deletions
diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml
index b5d9918e..0368ee9a 100644
--- a/backends/hol4/primitivesBaseTacLib.sml
+++ b/backends/hol4/primitivesBaseTacLib.sml
@@ -13,6 +13,8 @@ fun ignore_tac (_ : thm) : tactic = ALL_TAC
val pop_ignore_tac = pop_assum ignore_tac
+val try_tac = TRY
+
(* TODO: no exfalso tactic?? *)
val ex_falso : tactic =
SUBGOAL_THEN “F” (fn th => ASSUME_TAC th >> fs[])
@@ -22,13 +24,406 @@ fun qspecl_assume xl th = qspecl_then xl assume_tac th
fun first_qspec_assume x = first_assum (qspec_assume x)
fun first_qspecl_assume xl = first_assum (qspecl_assume xl)
-
-
+val all_tac = all_tac
val cooper_tac = COOPER_TAC
+val pure_rewrite_tac = PURE_REWRITE_TAC
val pure_once_rewrite_tac = PURE_ONCE_REWRITE_TAC
(* Dependent rewrites *)
val dep_pure_once_rewrite_tac = dep_rewrite.DEP_PURE_ONCE_REWRITE_TAC
val dep_pure_rewrite_tac = dep_rewrite.DEP_PURE_REWRITE_TAC
+
+(* Add a list of theorems in the assumptions *)
+fun assume_tacl (thms : thm list) : tactic =
+ let
+ (* TODO: use MAP_EVERY *)
+ fun t thms =
+ case thms of
+ [] => all_tac
+ | thm :: thms => assume_tac thm >> t thms
+ in
+ t thms
+ end
+
+(* Given a theorem of the shape:
+ {[
+ A0, ..., An ⊢ B0 ==> ... ==> Bm ==> concl
+ ]}
+
+ Rewrite it so that it has the shape:
+ {[
+ ⊢ (A0 /\ ... /\ An /\ B0 /\ ... /\ Bm) ==> concl
+ ]}
+ *)
+fun thm_to_conj_implies (thm : thm) : thm =
+ let
+ (* Discharge all the assumptions *)
+ val thm = DISCH_ALL thm;
+ (* Rewrite the implications as one conjunction *)
+ val thm = PURE_REWRITE_RULE [GSYM satTheory.AND_IMP] thm;
+ in thm end
+
+(* Like THEN1 and >-, but doesn't fail if the first subgoal is not completely
+ solved.
+
+ TODO: how to get the notation right?
+ *)
+fun op partial_then1 (tac1: tactic) (tac2: tactic) : tactic = tac1 THEN_LT (NTH_GOAL tac2 1)
+
+(* If the current goal is [asms ⊢ g], and given a lemma of the form
+ [⊢ H ==> C], do the following:
+ - introduce [asms ⊢ H] as a subgoal and apply the given tactic on it
+ - also calls the theorem tactic with the theorem [asms ⊢ C]
+
+ If the lemma is not an implication, we directly call the theorem tactic.
+ *)
+fun sg_premise_then (premise_tac: tactic) (then_tac: thm_tactic) (thm : thm) : tactic =
+ let
+ val c = concl thm;
+ (* First case: there is a premise to prove *)
+ fun prove_premise_then (h : term) =
+ partial_then1 (SUBGOAL_THEN h (fn h_thm => then_tac (MP thm h_thm))) premise_tac;
+ (* Second case: no premise to prove *)
+ val no_prove_premise_then = then_tac thm;
+ in
+ if is_imp c then prove_premise_then (fst (dest_imp c)) else no_prove_premise_then
+ end
+
+(* Add the first premise of the theorem as subgoal, and add the theorem without its
+ first premise as an assumption.
+
+ For instance, if we have the goal:
+ asls
+ ====
+ c
+ and the theorem: ⊢ H ==> G
+
+ We generate:
+ asls asls
+ ==== G
+ H ====
+ C
+
+*)
+val sg_premise_tac = sg_premise_then all_tac assume_tac
+
+(* Same as {!sg_premise_then} but fails if the premise_tac fails to prove the premise *)
+fun prove_premise_then (premise_tac: tactic) (then_tac: thm_tactic) (thm : thm) : tactic =
+ sg_premise_then
+ (premise_tac >> FAIL_TAC "prove_premise_then: could not prove premise")
+ then_tac thm
+
+(*
+val thm = th
+*)
+
+(* Call a function on all the subterms of a term *)
+fun dep_apply_in_subterms
+ (f : string Redblackset.set -> term -> unit)
+ (bound_vars : string Redblackset.set)
+ (t : term) : unit =
+ let
+ val dep = dep_apply_in_subterms f;
+ val _ = f bound_vars t;
+ in
+ case dest_term t of
+ VAR (name, ty) => ()
+ | CONST {Name=name, Thy=thy, Ty=ty} => ()
+ | COMB (app, arg) =>
+ let
+ val _ = dep bound_vars app;
+ val _ = dep bound_vars arg;
+ in () end
+ | LAMB (bvar, body) =>
+ let
+ val (varname, ty) = dest_var bvar;
+ val bound_vars = Redblackset.add (bound_vars, varname);
+ val _ = dep bound_vars body;
+ in () end
+ end
+
+(* Return the set of free variables appearing in the residues of a term substitution *)
+fun free_vars_in_subst_residue (s: (term, term) Term.subst) : string Redblackset.set =
+ let
+ val free_vars = free_varsl (map (fn {redex=_, residue=x} => x) s);
+ val free_vars = map (fst o dest_var) free_vars;
+ val free_vars = Redblackset.fromList String.compare free_vars;
+ in free_vars end
+
+(* Attempt to instantiate a rewrite theorem.
+
+ Remark: this theorem should be of the form:
+ H ⊢ x = y
+
+ (without quantified variables).
+
+ **REMARK**: the function raises a HOL_ERR exception if it fails.
+
+ [forbid_vars]: forbid substituting with those vars (typically because
+ we are maching in a subterm under lambdas, and some of those variables
+ are bounds in the outer lambdas).
+*)
+fun inst_match_concl (forbid_vars : string Redblackset.set) (th : thm) (t : term) : thm =
+ let
+ (* Retrieve the lhs of the conclusion of the theorem *)
+ val l = lhs (concl th);
+ (* Match this lhs with the term *)
+ val (var_s, ty_s) = match_term l t;
+ (* Check that we are allowed to perform the substitution *)
+ val free_vars = free_vars_in_subst_residue var_s;
+ val _ = assert Redblackset.isEmpty (Redblackset.intersection (free_vars, forbid_vars));
+ in
+ (* Perform the substitution *)
+ INST var_s (INST_TYPE ty_s th)
+ end
+
+(*
+val forbid_vars = Redblackset.empty String.compare
+val t = “u32_to_int (int_to_u32 x)”
+val t = “u32_to_int (int_to_u32 3)”
+val th = (UNDISCH_ALL o SPEC_ALL) int_to_u32_id
+*)
+
+(* Attempt to instantiate a theorem by matching its first premise.
+
+ Note that we make the hypothesis tha all the free variables which need
+ to be instantiated appear in the first premise, of course (the caller should
+ enforce this).
+
+ Remark: this theorem should be of the form:
+ ⊢ H0 ==> ... ==> Hn ==> H
+
+ (without quantified variables).
+
+ **REMARK**: the function raises a HOL_ERR exception if it fails.
+
+ [forbid_vars]: see [inst_match_concl]
+*)
+fun inst_match_first_premise
+ (forbid_vars : string Redblackset.set) (th : thm) (t : term) : thm =
+ let
+ (* Retrieve the first premise *)
+ val l = (fst o dest_imp o concl) th;
+ (* Match this with the term *)
+ val (var_s, ty_s) = match_term l t;
+ (* Check that we are allowed to perform the substitution *)
+ val free_vars = free_vars_in_subst_residue var_s;
+ val _ = assert Redblackset.isEmpty (Redblackset.intersection (free_vars, forbid_vars));
+ in
+ (* Perform the substitution *)
+ INST var_s (INST_TYPE ty_s th)
+ end
+
+(*
+val forbid_vars = Redblackset.empty String.compare
+val t = “u32_to_int z = u32_to_int i − 1”
+val th = SPEC_ALL NUM_SUB_1_EQ
+*)
+
+(* Call a matching function on all the subterms in the provided list of term.
+ This is a generic function.
+
+ [try_match] should return an instantiated theorem, as well as a term which
+ identifies this theorem (the lhs of the equality, if this is a rewriting
+ theorem for instance - we use this to check for collisions, and discard
+ redundant instantiations).
+ *)
+fun inst_match_in_terms
+ (try_match: string Redblackset.set -> term -> term * thm)
+ (tl : term list) : thm list =
+ let
+ (* We use a map when storing the theorems, to avoid storing the same theorem twice *)
+ val inst_thms: (term, thm) Redblackmap.dict ref = ref (Redblackmap.mkDict Term.compare);
+ fun try_instantiate bvars t =
+ let
+ val (inst_th_tm, inst_th) = try_match bvars t;
+ in
+ inst_thms := Redblackmap.insert (!inst_thms, inst_th_tm, inst_th)
+ end
+ handle HOL_ERR _ => ();
+ (* Explore the term *)
+ val _ = app (dep_apply_in_subterms try_instantiate (Redblackset.empty String.compare)) tl;
+ in
+ map snd (Redblackmap.listItems (!inst_thms))
+ end
+
+(* Given a rewriting theorem [th] which has premises, return all the
+ instantiations of this theorem which make its conclusion match subterms
+ in the provided list of term.
+
+ [ignore]: if the conclusion of a theorem matches a term in this set, ignore it.
+ *)
+fun inst_match_concl_in_terms (ignore : term Redblackset.set) (th : thm) (tl : term list) : thm list =
+ let
+ val th = (UNDISCH_ALL o SPEC_ALL) th;
+ fun try_match bvars t =
+ let
+ val inst_th = inst_match_concl bvars th t;
+ val c = concl inst_th;
+ in
+ (* Check that we mustn't ignore the theorem *)
+ if Redblackset.member (ignore, c) then failwith "inst_match_concl_in_terms: already in the assumptions"
+ else (lhs (concl inst_th), inst_th)
+ end;
+ in
+ inst_match_in_terms try_match tl
+ end
+
+(*
+val t = “!x. u32_to_int (int_to_u32 x) = u32_to_int (int_to_u32 y)”
+val th = int_to_u32_id
+
+val thms = inst_match_concl_in_terms int_to_u32_id [t]
+*)
+
+
+(* Given a theorem [th] which has premises, return all the
+ instantiations of this theorem which make its first premise match subterms
+ in the provided list of term.
+ *)
+fun inst_match_first_premise_in_terms (th : thm) (tl : term list) : thm list =
+ let
+ val th = SPEC_ALL th;
+ fun try_match bvars t =
+ let
+ val inst_th = inst_match_first_premise bvars th t;
+ in
+ ((fst o dest_imp o concl) inst_th, inst_th)
+ end;
+ in
+ inst_match_in_terms try_match tl
+ end
+
+(*
+val t = “x = y - 1 ==> T”
+val th = SPEC_ALL NUM_SUB_1_EQ
+
+val thms = inst_match_first_premise_in_terms th [t]
+*)
+
+
+(* Attempt to apply dependent rewrites with a theorem by matching its
+ conclusion with subterms in the given list of terms.
+
+ Leaves the premises as subgoals if [prove_premise] doesn't prove them.
+ *)
+fun apply_dep_rewrites_match_concl_with_terms_tac
+ (prove_premise : tactic) (then_tac : thm_tactic) (tl : term list) (th : thm) : tactic =
+ let
+ val ignore = Redblackset.fromList Term.compare tl;
+ (* Discharge the assumptions so that the goal is one single term *)
+ val thms = inst_match_concl_in_terms ignore th tl;
+ val thms = map thm_to_conj_implies thms;
+ in
+ (* Apply each theorem *)
+ MAP_EVERY (sg_premise_then prove_premise then_tac) thms
+ end
+
+(* Attempt to apply dependent rewrites with a theorem by matching its
+ conclusion with subterms of the goal (including the assumptions).
+
+ Leaves the premises as subgoals if [prove_premise] doesn't prove them.
+ *)
+fun apply_dep_rewrites_match_concl_with_all_tac
+ (prove_premise : tactic) (then_tac : thm_tactic) (th : thm) : tactic =
+ fn (asms, g) => apply_dep_rewrites_match_concl_with_terms_tac prove_premise then_tac (g :: asms) th (asms, g)
+
+(* Same as {!apply_dep_rewrites_match_concl_with_all_tac} but we only match the
+ conclusion of the goal.
+ *)
+fun apply_dep_rewrites_match_concl_with_goal_tac
+ (prove_premise : tactic) (then_tac : thm_tactic) (th : thm) : tactic =
+ fn (asms, g) => apply_dep_rewrites_match_concl_with_terms_tac prove_premise then_tac [g] th (asms, g)
+
+(* A theorem might be of the shape: [H => A = B /\ C = D], in which
+ case we can split it into:
+ [H => A = B]
+ [H => C = D]
+
+ The theorem mustn't have assumptions.
+ *)
+fun split_rewrite_thm (th : thm) : thm list =
+ let
+ val _ = null (hyp th);
+ val t = concl th;
+ val (vars, t) = strip_forall t;
+ val (impl, t) = strip_imp t;
+ val tl = strip_conj t;
+ fun mk_goal (t : term) = list_mk_forall (vars, (list_mk_imp (impl, t)))
+ val prove_tac =
+ rpt gen_tac >> rpt disch_tac >>
+ qspecl_assume (map (fn a => ‘^a’) vars) th >>
+ fs [];
+ fun mk_th (t : term) = prove (mk_goal t, prove_tac);
+ (* Change the shape of the theorem (one of the conjuncts may have
+ universally quantified variables)
+ *)
+ fun transform_th (th : thm) : thm =
+ (GEN_ALL o thm_to_conj_implies o SPEC_ALL o UNDISCH_ALL o SPEC_ALL) th
+ in
+ map (transform_th o mk_th) tl
+ end
+
+(* A dependent rewrite tactic which introduces the premises in a new goal.
+
+ We try to apply dependent rewrites to the whole goal, including its assumptions.
+
+ TODO: this tactic sometimes introduces several times the same subgoal
+ (because we split theorems...).
+ *)
+fun sg_dep_rewrite_all_tac (th : thm) =
+ let
+ (* Split the theorem *)
+ val thml = split_rewrite_thm th
+ in
+ MAP_EVERY (apply_dep_rewrites_match_concl_with_all_tac all_tac assume_tac) thml
+ end
+
+(* Same as {!sg_dep_rewrite_tac} but this time we apply rewrites only in the conclusion
+ of the goal (not the assumptions).
+ *)
+fun sg_dep_rewrite_goal_tac (th : thm) =
+ let
+ (* Split the theorem *)
+ val thml = split_rewrite_thm th
+ in
+ MAP_EVERY (apply_dep_rewrites_match_concl_with_goal_tac all_tac assume_tac) thml
+ end
+
+(*
+val (asms, g) = ([
+ “u32_to_int z = u32_to_int i − u32_to_int (int_to_u32 1)”,
+ “u32_to_int (int_to_u32 2) = 2”
+], “T”)
+
+apply_dep_rewrites_match_concl_tac
+ (FULL_SIMP_TAC simpLib.empty_ss all_integer_bounds >> COOPER_TAC)
+ (fn th => FULL_SIMP_TAC simpLib.empty_ss [th])
+ int_to_u32_id
+*)
+
+(* Attempt to apply dependent rewrites with a theorem by matching its
+ first premise with subterms of the goal.
+
+ Leaves the premises as subgoals if [prove_premise] doesn't prove them.
+ *)
+fun apply_dep_rewrites_match_first_premise_tac
+ (prove_premise : tactic) (then_tac : thm_tactic) (th : thm) : tactic =
+ fn (asms, g) =>
+ let
+ (* Discharge the assumptions so that the goal is one single term *)
+ val thms = inst_match_first_premise_in_terms th (g :: asms);
+ val thms = map thm_to_conj_implies thms;
+ fun apply_tac th =
+ let
+ val th = thm_to_conj_implies th;
+ in
+ sg_premise_then prove_premise then_tac th
+ end;
+ in
+ (* Apply each theorem *)
+ MAP_EVERY apply_tac thms (asms, g)
+ end
+
end
diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml
index 85efeb61..2df3375a 100644
--- a/backends/hol4/primitivesScript.sml
+++ b/backends/hol4/primitivesScript.sml
@@ -1389,8 +1389,23 @@ 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) ⇒
@@ -1433,4 +1448,166 @@ Proof
qspec_assume ‘j’ usize_to_int_bounds >> fs []
QED
+(* TODO: use lowercase everywhere for the theorem names *)
+
+(* We generate and save an induction theorem for positive integers *)
+Theorem int_induction:
+ !(P : int -> bool). P 0 /\ (!i. 0 <= i /\ P i ==> P (i+1)) ==> !i. 0 <= i ==> P i
+Proof
+ ntac 4 strip_tac >>
+ Induct_on ‘Num i’ >> rpt strip_tac
+ >-(sg ‘i = 0’ >- cooper_tac >> fs []) >>
+ last_assum (qspec_assume ‘i-1’) >>
+ fs [] >> pop_assum irule >>
+ rw [] >> try_tac cooper_tac >>
+ first_assum (qspec_assume ‘i - 1’) >>
+ pop_assum irule >>
+ rw [] >> try_tac cooper_tac
+QED
+
+val _ = TypeBase.update_induction int_induction
+
+(* Small experiment: trying to redefine common functions with integers instead of nums *)
+val index_def = Define ‘
+ index (i : int) (x :: ls) = if i = 0 then x else (if 0 < i then index (i - 1) ls else ARB)
+’
+
+val len_def = Define ‘
+ len [] : int = 0 /\
+ len (x :: ls) : int = 1 + len ls
+’
+
+val update_def = Define ‘
+ update ([] : 'a list) (i : int) (y : 'a) : 'a list = [] ∧
+ update (x :: ls) (i : int) y = if i = 0 then y :: ls else (if 0 < i then x :: update ls (i - 1) y else x :: ls)
+’
+
+Theorem update_len:
+ ∀ls i y. len (update ls i y) = len ls
+Proof
+ Induct_on ‘ls’ >> Cases_on ‘i’ >> rw [update_def, len_def]
+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
+Proof
+ Induct_on ‘ls’ >> Cases_on ‘i = 0’ >> rw [update_def, len_def, index_def] >> try_tac (ex_falso >> cooper_tac) >>
+ try_tac (
+ pop_last_assum (qspecl_assume [‘i' - 1’, ‘y’]) >>
+ pop_assum sg_premise_tac >- cooper_tac >>
+ pop_assum sg_premise_tac >- cooper_tac >>
+ rw [])
+ >> (
+ pop_assum (qspec_assume ‘j - 1’) >>
+ pop_assum sg_premise_tac >- cooper_tac >>
+ pop_assum sg_premise_tac >- cooper_tac >>
+ rw [])
+QED
+
+Theorem index_update_same:
+ ∀ls i j y.
+ 0 <= i ==>
+ i < len ls ==>
+ j < len ls ⇒ j ≠ i ⇒ index j (update ls i y) = index j ls
+Proof
+ rpt strip_tac >>
+ qspecl_assume [‘ls’, ‘i’, ‘y’] update_spec >>
+ rw []
+QED
+
+Theorem index_update_diff:
+ ∀ls i j y.
+ 0 <= i ==>
+ i < len ls ==>
+ index i (update ls i y) = y
+Proof
+ rpt strip_tac >>
+ qspecl_assume [‘ls’, ‘i’, ‘y’] update_spec >>
+ rw []
+QED
+
+Theorem vec_to_list_int_bounds:
+ !v. 0 <= len (vec_to_list v) /\ len (vec_to_list v) <= usize_max
+Proof
+ (* TODO *)
+ cheat
+QED
+
+val vec_len_def = Define ‘vec_len v = int_to_usize (len (vec_to_list v))’
+Theorem vec_len_spec:
+ ∀v.
+ vec_len v = int_to_usize (len (vec_to_list v)) ∧
+ 0 ≤ len (vec_to_list v) ∧ len (vec_to_list v) ≤ usize_max
+Proof
+ gen_tac >> rw [vec_len_def] >>
+ qspec_assume ‘v’ vec_to_list_int_bounds >>
+ fs []
+QED
+
+val vec_index_def = Define ‘
+ vec_index i v = if usize_to_int i ≤ usize_to_int (vec_len v) then Return (index (usize_to_int i) (vec_to_list v)) else Fail Failure’
+
+(* TODO: *)
+val mk_vec_spec = new_axiom ("mk_vec_spec", “∀l. len l ≤ usize_max ⇒ ∃v. mk_vec l = Return v ∧ vec_to_list v = l”)
+
+(* Redefining ‘vec_insert_back’ *)
+val vec_insert_back_def = Define ‘
+ vec_insert_back (v : 'a vec) (i : usize) (x : 'a) = mk_vec (update (vec_to_list v) (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 ∧
+ (∀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? *)
+ qspec_assume ‘update (vec_to_list v) (usize_to_int i) x’ mk_vec_spec >>
+ sg_dep_rewrite_all_tac update_len >> fs [] >>
+ qspec_assume ‘v’ vec_len_spec >>
+ rw [] >> gvs [] >>
+ fs [vec_len_def, vec_index_def] >>
+ qspec_assume ‘i’ usize_to_int_bounds >>
+ sg_dep_rewrite_all_tac int_to_usize_id >- cooper_tac >> fs [] >>
+ sg_dep_rewrite_goal_tac index_update_diff >- cooper_tac >> fs [] >>
+ rw [] >>
+ irule index_update_same >> cooper_tac
+QED
+
+(* TODO: add theorems to the rewriting theorems
+from listSimps.sml:
+
+val LIST_ss = BasicProvers.thy_ssfrag "list"
+val _ = BasicProvers.logged_addfrags {thyname="list"} [LIST_EQ_ss]
+
+val list_rws = computeLib.add_thms
+ [
+ ALL_DISTINCT, APPEND, APPEND_NIL, CONS_11, DROP_compute, EL_restricted,
+ EL_simp_restricted, EVERY_DEF, EXISTS_DEF, FILTER, FIND_def, FLAT, FOLDL,
+ FOLDR, FRONT_DEF, GENLIST_AUX_compute, GENLIST_NUMERALS, HD, INDEX_FIND_def,
+ INDEX_OF_def, LAST_compute, LENGTH, LEN_DEF, LIST_APPLY_def, LIST_BIND_def,
+ LIST_IGNORE_BIND_def, LIST_LIFT2_def, LIST_TO_SET_THM, LLEX_def, LRC_def,
+ LUPDATE_compute, MAP, MAP2, NOT_CONS_NIL, NOT_NIL_CONS, NULL_DEF, oEL_def,
+ oHD_def,
+ PAD_LEFT, PAD_RIGHT, REVERSE_REV, REV_DEF, SHORTLEX_def, SNOC, SUM_ACC_DEF,
+ SUM_SUM_ACC,
+ TAKE_compute, TL, UNZIP, ZIP, computeLib.lazyfy_thm list_case_compute,
+ dropWhile_def, isPREFIX, list_size_def, nub_def, splitAtPki_def
+ ]
+
+fun list_compset () =
+ let
+ val base = reduceLib.num_compset()
+ in
+ list_rws base; base
+ end
+*)
+
val _ = export_theory ()
diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig
index 75098bfe..cc2f3115 100644
--- a/backends/hol4/primitivesTheory.sig
+++ b/backends/hol4/primitivesTheory.sig
@@ -3,26 +3,40 @@ sig
type thm = Thm.thm
(* Axioms *)
+ val MK_VEC_SPEC : thm
val VEC_TO_LIST_BOUNDS : thm
val i128_to_int_bounds : thm
val i16_to_int_bounds : thm
val i32_to_int_bounds : thm
val i64_to_int_bounds : thm
val i8_to_int_bounds : thm
+ val int_to_i128_i128_to_int : thm
val int_to_i128_id : thm
+ val int_to_i16_i16_to_int : thm
val int_to_i16_id : thm
+ val int_to_i32_i32_to_int : thm
val int_to_i32_id : thm
+ val int_to_i64_i64_to_int : thm
val int_to_i64_id : thm
+ val int_to_i8_i8_to_int : thm
val int_to_i8_id : thm
val int_to_isize_id : thm
+ val int_to_isize_isize_to_int : thm
val int_to_u128_id : thm
+ val int_to_u128_u128_to_int : thm
val int_to_u16_id : thm
+ val int_to_u16_u16_to_int : thm
val int_to_u32_id : thm
+ val int_to_u32_u32_to_int : thm
val int_to_u64_id : thm
+ val int_to_u64_u64_to_int : thm
val int_to_u8_id : thm
+ val int_to_u8_u8_to_int : thm
val int_to_usize_id : thm
+ val int_to_usize_usize_to_int : thm
val isize_bounds : thm
val isize_to_int_bounds : thm
+ val mk_vec_spec : thm
val u128_to_int_bounds : thm
val u16_to_int_bounds : thm
val u32_to_int_bounds : thm
@@ -72,12 +86,14 @@ sig
val i8_mul_def : thm
val i8_rem_def : thm
val i8_sub_def : thm
+ val index_def : thm
val int_rem_def : thm
val isize_add_def : thm
val isize_div_def : thm
val isize_mul_def : thm
val isize_rem_def : thm
val isize_sub_def : thm
+ val len_def : thm
val massert_def : thm
val mem_replace_back_def : thm
val mem_replace_fwd_def : thm
@@ -127,12 +143,17 @@ sig
val u8_mul_def : thm
val u8_rem_def : thm
val u8_sub_def : thm
+ val update_def : thm
val usize_add_def : thm
val usize_div_def : thm
val usize_mul_def : thm
val usize_rem_def : thm
val usize_sub_def : thm
+ val vec_index_def : thm
+ val vec_insert_back_def : thm
val vec_len_def : thm
+ val vec_new_def : thm
+ val vec_push_back_def : thm
(* Theorems *)
val I128_ADD_EQ : thm
@@ -159,6 +180,8 @@ sig
val I8_MUL_EQ : thm
val I8_REM_EQ : thm
val I8_SUB_EQ : thm
+ val INT_OF_NUM : thm
+ val INT_OF_NUM_NEQ_INJ : thm
val ISIZE_ADD_EQ : thm
val ISIZE_DIV_EQ : thm
val ISIZE_MUL_EQ : thm
@@ -193,6 +216,9 @@ sig
val USIZE_MUL_EQ : thm
val USIZE_REM_EQ : thm
val USIZE_SUB_EQ : thm
+ val USIZE_TO_INT_INJ : thm
+ val USIZE_TO_INT_NEQ_INJ : thm
+ val VEC_NEW_SPEC : thm
val VEC_TO_LIST_INT_BOUNDS : thm
val datatype_error : thm
val datatype_result : thm
@@ -207,6 +233,9 @@ sig
val error_case_eq : thm
val error_induction : thm
val error_nchotomy : thm
+ val index_update_diff : thm
+ val index_update_same : thm
+ val int_induction : thm
val num2error_11 : thm
val num2error_ONTO : thm
val num2error_error2num : thm
@@ -218,6 +247,12 @@ sig
val result_distinct : thm
val result_induction : thm
val result_nchotomy : thm
+ val update_ind : thm
+ val update_len : thm
+ val update_spec : thm
+ val vec_insert_back_spec : thm
+ val vec_len_spec : thm
+ val vec_to_list_int_bounds : thm
val primitives_grammars : type_grammar.grammar * term_grammar.grammar
(*
@@ -225,61 +260,84 @@ sig
[string] Parent theory of "primitives"
- [int_to_u128_id] Axiom
+ [mk_vec_spec] Axiom
- [oracles: ] [axioms: int_to_u128_id] []
- ⊢ ∀n. 0 ≤ n ∧ n ≤ u128_max ⇒ u128_to_int (int_to_u128 n) = n
+ [oracles: ] [axioms: mk_vec_spec] []
+ ⊢ ∀l. len l ≤ usize_max ⇒ ∃v. mk_vec l = Return v ∧ vec_to_list v = l
- [int_to_u64_id] Axiom
+ [VEC_TO_LIST_BOUNDS] Axiom
- [oracles: ] [axioms: int_to_u64_id] []
- ⊢ ∀n. 0 ≤ n ∧ n ≤ u64_max ⇒ u64_to_int (int_to_u64 n) = n
+ [oracles: ] [axioms: VEC_TO_LIST_BOUNDS] []
+ ⊢ ∀v. (let l = LENGTH (vec_to_list v) in 0 ≤ l ∧ l ≤ Num usize_max)
- [int_to_u32_id] Axiom
+ [isize_bounds] Axiom
- [oracles: ] [axioms: int_to_u32_id] []
- ⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ u32_to_int (int_to_u32 n) = n
+ [oracles: ] [axioms: isize_bounds] []
+ ⊢ isize_min ≤ i16_min ∧ isize_max ≥ i16_max
- [int_to_u16_id] Axiom
+ [usize_bounds] Axiom
- [oracles: ] [axioms: int_to_u16_id] []
- ⊢ ∀n. 0 ≤ n ∧ n ≤ u16_max ⇒ u16_to_int (int_to_u16 n) = n
+ [oracles: ] [axioms: usize_bounds] [] ⊢ usize_max ≥ u16_max
- [int_to_u8_id] Axiom
+ [isize_to_int_bounds] Axiom
- [oracles: ] [axioms: int_to_u8_id] []
- ⊢ ∀n. 0 ≤ n ∧ n ≤ u8_max ⇒ u8_to_int (int_to_u8 n) = n
+ [oracles: ] [axioms: isize_to_int_bounds] []
+ ⊢ ∀n. isize_min ≤ isize_to_int n ∧ isize_to_int n ≤ isize_max
- [int_to_i128_id] Axiom
+ [i8_to_int_bounds] Axiom
- [oracles: ] [axioms: int_to_i128_id] []
- ⊢ ∀n. i128_min ≤ n ∧ n ≤ i128_max ⇒ i128_to_int (int_to_i128 n) = n
+ [oracles: ] [axioms: i8_to_int_bounds] []
+ ⊢ ∀n. i8_min ≤ i8_to_int n ∧ i8_to_int n ≤ i8_max
- [int_to_i64_id] Axiom
+ [i16_to_int_bounds] Axiom
- [oracles: ] [axioms: int_to_i64_id] []
- ⊢ ∀n. i64_min ≤ n ∧ n ≤ i64_max ⇒ i64_to_int (int_to_i64 n) = n
+ [oracles: ] [axioms: i16_to_int_bounds] []
+ ⊢ ∀n. i16_min ≤ i16_to_int n ∧ i16_to_int n ≤ i16_max
- [int_to_i32_id] Axiom
+ [i32_to_int_bounds] Axiom
- [oracles: ] [axioms: int_to_i32_id] []
- ⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ i32_to_int (int_to_i32 n) = n
+ [oracles: ] [axioms: i32_to_int_bounds] []
+ ⊢ ∀n. i32_min ≤ i32_to_int n ∧ i32_to_int n ≤ i32_max
- [int_to_i16_id] Axiom
+ [i64_to_int_bounds] Axiom
- [oracles: ] [axioms: int_to_i16_id] []
- ⊢ ∀n. i16_min ≤ n ∧ n ≤ i16_max ⇒ i16_to_int (int_to_i16 n) = n
+ [oracles: ] [axioms: i64_to_int_bounds] []
+ ⊢ ∀n. i64_min ≤ i64_to_int n ∧ i64_to_int n ≤ i64_max
- [int_to_i8_id] Axiom
+ [i128_to_int_bounds] Axiom
- [oracles: ] [axioms: int_to_i8_id] []
- ⊢ ∀n. i8_min ≤ n ∧ n ≤ i8_max ⇒ i8_to_int (int_to_i8 n) = n
+ [oracles: ] [axioms: i128_to_int_bounds] []
+ ⊢ ∀n. i128_min ≤ i128_to_int n ∧ i128_to_int n ≤ i128_max
- [int_to_usize_id] Axiom
+ [usize_to_int_bounds] Axiom
- [oracles: ] [axioms: int_to_usize_id] []
- ⊢ ∀n. 0 ≤ n ∧ (n ≤ u16_max ∨ n ≤ usize_max) ⇒
- usize_to_int (int_to_usize n) = n
+ [oracles: ] [axioms: usize_to_int_bounds] []
+ ⊢ ∀n. 0 ≤ usize_to_int n ∧ usize_to_int n ≤ usize_max
+
+ [u8_to_int_bounds] Axiom
+
+ [oracles: ] [axioms: u8_to_int_bounds] []
+ ⊢ ∀n. 0 ≤ u8_to_int n ∧ u8_to_int n ≤ u8_max
+
+ [u16_to_int_bounds] Axiom
+
+ [oracles: ] [axioms: u16_to_int_bounds] []
+ ⊢ ∀n. 0 ≤ u16_to_int n ∧ u16_to_int n ≤ u16_max
+
+ [u32_to_int_bounds] Axiom
+
+ [oracles: ] [axioms: u32_to_int_bounds] []
+ ⊢ ∀n. 0 ≤ u32_to_int n ∧ u32_to_int n ≤ u32_max
+
+ [u64_to_int_bounds] Axiom
+
+ [oracles: ] [axioms: u64_to_int_bounds] []
+ ⊢ ∀n. 0 ≤ u64_to_int n ∧ u64_to_int n ≤ u64_max
+
+ [u128_to_int_bounds] Axiom
+
+ [oracles: ] [axioms: u128_to_int_bounds] []
+ ⊢ ∀n. 0 ≤ u128_to_int n ∧ u128_to_int n ≤ u128_max
[int_to_isize_id] Axiom
@@ -287,79 +345,127 @@ sig
⊢ ∀n. (i16_min ≤ n ∨ isize_min ≤ n) ∧ (n ≤ i16_max ∨ n ≤ isize_max) ⇒
isize_to_int (int_to_isize n) = n
- [u128_to_int_bounds] Axiom
+ [int_to_usize_id] Axiom
- [oracles: ] [axioms: u128_to_int_bounds] []
- ⊢ ∀n. 0 ≤ u128_to_int n ∧ u128_to_int n ≤ u128_max
+ [oracles: ] [axioms: int_to_usize_id] []
+ ⊢ ∀n. 0 ≤ n ∧ (n ≤ u16_max ∨ n ≤ usize_max) ⇒
+ usize_to_int (int_to_usize n) = n
- [u64_to_int_bounds] Axiom
+ [int_to_i8_id] Axiom
- [oracles: ] [axioms: u64_to_int_bounds] []
- ⊢ ∀n. 0 ≤ u64_to_int n ∧ u64_to_int n ≤ u64_max
+ [oracles: ] [axioms: int_to_i8_id] []
+ ⊢ ∀n. i8_min ≤ n ∧ n ≤ i8_max ⇒ i8_to_int (int_to_i8 n) = n
- [u32_to_int_bounds] Axiom
+ [int_to_i16_id] Axiom
- [oracles: ] [axioms: u32_to_int_bounds] []
- ⊢ ∀n. 0 ≤ u32_to_int n ∧ u32_to_int n ≤ u32_max
+ [oracles: ] [axioms: int_to_i16_id] []
+ ⊢ ∀n. i16_min ≤ n ∧ n ≤ i16_max ⇒ i16_to_int (int_to_i16 n) = n
- [u16_to_int_bounds] Axiom
+ [int_to_i32_id] Axiom
- [oracles: ] [axioms: u16_to_int_bounds] []
- ⊢ ∀n. 0 ≤ u16_to_int n ∧ u16_to_int n ≤ u16_max
+ [oracles: ] [axioms: int_to_i32_id] []
+ ⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ i32_to_int (int_to_i32 n) = n
- [u8_to_int_bounds] Axiom
+ [int_to_i64_id] Axiom
- [oracles: ] [axioms: u8_to_int_bounds] []
- ⊢ ∀n. 0 ≤ u8_to_int n ∧ u8_to_int n ≤ u8_max
+ [oracles: ] [axioms: int_to_i64_id] []
+ ⊢ ∀n. i64_min ≤ n ∧ n ≤ i64_max ⇒ i64_to_int (int_to_i64 n) = n
- [usize_to_int_bounds] Axiom
+ [int_to_i128_id] Axiom
- [oracles: ] [axioms: usize_to_int_bounds] []
- ⊢ ∀n. 0 ≤ usize_to_int n ∧ usize_to_int n ≤ usize_max
+ [oracles: ] [axioms: int_to_i128_id] []
+ ⊢ ∀n. i128_min ≤ n ∧ n ≤ i128_max ⇒ i128_to_int (int_to_i128 n) = n
- [i128_to_int_bounds] Axiom
+ [int_to_u8_id] Axiom
- [oracles: ] [axioms: i128_to_int_bounds] []
- ⊢ ∀n. i128_min ≤ i128_to_int n ∧ i128_to_int n ≤ i128_max
+ [oracles: ] [axioms: int_to_u8_id] []
+ ⊢ ∀n. 0 ≤ n ∧ n ≤ u8_max ⇒ u8_to_int (int_to_u8 n) = n
- [i64_to_int_bounds] Axiom
+ [int_to_u16_id] Axiom
- [oracles: ] [axioms: i64_to_int_bounds] []
- ⊢ ∀n. i64_min ≤ i64_to_int n ∧ i64_to_int n ≤ i64_max
+ [oracles: ] [axioms: int_to_u16_id] []
+ ⊢ ∀n. 0 ≤ n ∧ n ≤ u16_max ⇒ u16_to_int (int_to_u16 n) = n
- [i32_to_int_bounds] Axiom
+ [int_to_u32_id] Axiom
- [oracles: ] [axioms: i32_to_int_bounds] []
- ⊢ ∀n. i32_min ≤ i32_to_int n ∧ i32_to_int n ≤ i32_max
+ [oracles: ] [axioms: int_to_u32_id] []
+ ⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ u32_to_int (int_to_u32 n) = n
- [i16_to_int_bounds] Axiom
+ [int_to_u64_id] Axiom
- [oracles: ] [axioms: i16_to_int_bounds] []
- ⊢ ∀n. i16_min ≤ i16_to_int n ∧ i16_to_int n ≤ i16_max
+ [oracles: ] [axioms: int_to_u64_id] []
+ ⊢ ∀n. 0 ≤ n ∧ n ≤ u64_max ⇒ u64_to_int (int_to_u64 n) = n
- [i8_to_int_bounds] Axiom
+ [int_to_u128_id] Axiom
- [oracles: ] [axioms: i8_to_int_bounds] []
- ⊢ ∀n. i8_min ≤ i8_to_int n ∧ i8_to_int n ≤ i8_max
+ [oracles: ] [axioms: int_to_u128_id] []
+ ⊢ ∀n. 0 ≤ n ∧ n ≤ u128_max ⇒ u128_to_int (int_to_u128 n) = n
- [isize_to_int_bounds] Axiom
+ [int_to_i8_i8_to_int] Axiom
- [oracles: ] [axioms: isize_to_int_bounds] []
- ⊢ ∀n. isize_min ≤ isize_to_int n ∧ isize_to_int n ≤ isize_max
+ [oracles: ] [axioms: int_to_i8_i8_to_int] []
+ ⊢ ∀i. int_to_i8 (i8_to_int i) = i
- [usize_bounds] Axiom
+ [int_to_i16_i16_to_int] Axiom
- [oracles: ] [axioms: usize_bounds] [] ⊢ usize_max ≥ u16_max
+ [oracles: ] [axioms: int_to_i16_i16_to_int] []
+ ⊢ ∀i. int_to_i16 (i16_to_int i) = i
- [isize_bounds] Axiom
+ [int_to_i32_i32_to_int] Axiom
- [oracles: ] [axioms: isize_bounds] []
- ⊢ isize_min ≤ i16_min ∧ isize_max ≥ i16_max
+ [oracles: ] [axioms: int_to_i32_i32_to_int] []
+ ⊢ ∀i. int_to_i32 (i32_to_int i) = i
- [VEC_TO_LIST_BOUNDS] Axiom
+ [int_to_i64_i64_to_int] Axiom
- [oracles: ] [axioms: VEC_TO_LIST_BOUNDS] []
- ⊢ ∀v. (let l = LENGTH (vec_to_list v) in 0 ≤ l ∧ l ≤ 4294967295)
+ [oracles: ] [axioms: int_to_i64_i64_to_int] []
+ ⊢ ∀i. int_to_i64 (i64_to_int i) = i
+
+ [int_to_i128_i128_to_int] Axiom
+
+ [oracles: ] [axioms: int_to_i128_i128_to_int] []
+ ⊢ ∀i. int_to_i128 (i128_to_int i) = i
+
+ [int_to_isize_isize_to_int] Axiom
+
+ [oracles: ] [axioms: int_to_isize_isize_to_int] []
+ ⊢ ∀i. int_to_isize (isize_to_int i) = i
+
+ [int_to_u8_u8_to_int] Axiom
+
+ [oracles: ] [axioms: int_to_u8_u8_to_int] []
+ ⊢ ∀i. int_to_u8 (u8_to_int i) = i
+
+ [int_to_u16_u16_to_int] Axiom
+
+ [oracles: ] [axioms: int_to_u16_u16_to_int] []
+ ⊢ ∀i. int_to_u16 (u16_to_int i) = i
+
+ [int_to_u32_u32_to_int] Axiom
+
+ [oracles: ] [axioms: int_to_u32_u32_to_int] []
+ ⊢ ∀i. int_to_u32 (u32_to_int i) = i
+
+ [int_to_u64_u64_to_int] Axiom
+
+ [oracles: ] [axioms: int_to_u64_u64_to_int] []
+ ⊢ ∀i. int_to_u64 (u64_to_int i) = i
+
+ [int_to_u128_u128_to_int] Axiom
+
+ [oracles: ] [axioms: int_to_u128_u128_to_int] []
+ ⊢ ∀i. int_to_u128 (u128_to_int i) = i
+
+ [int_to_usize_usize_to_int] Axiom
+
+ [oracles: ] [axioms: int_to_usize_usize_to_int] []
+ ⊢ ∀i. int_to_usize (usize_to_int i) = i
+
+ [MK_VEC_SPEC] Axiom
+
+ [oracles: ] [axioms: MK_VEC_SPEC] []
+ ⊢ ∀l. &LENGTH l ≤ usize_max ⇒
+ ∃v. mk_vec l = Return v ∧ vec_to_list v = l
[bind_def] Definition
@@ -554,6 +660,12 @@ sig
⊢ ∀x y. i8_sub x y = mk_i8 (i8_to_int x − i8_to_int y)
+ [index_def] Definition
+
+ ⊢ ∀i x ls.
+ index i (x::ls) =
+ if i = 0 then x else if 0 < i then index (i − 1) ls else ARB
+
[int_rem_def] Definition
⊢ ∀x y.
@@ -586,6 +698,10 @@ sig
⊢ ∀x y. isize_sub x y = mk_isize (isize_to_int x − isize_to_int y)
+ [len_def] Definition
+
+ ⊢ len [] = 0 ∧ ∀x ls. len (x::ls) = 1 + len ls
+
[massert_def] Definition
⊢ ∀b. massert b = if b then Return () else Fail Failure
@@ -857,6 +973,15 @@ sig
⊢ ∀x y. u8_sub x y = mk_u8 (u8_to_int x − u8_to_int y)
+ [update_def] Definition
+
+ ⊢ (∀i y. update [] i y = []) ∧
+ ∀x ls i y.
+ update (x::ls) i y =
+ if i = 0 then y::ls
+ else if 0 < i then x::update ls (i − 1) y
+ else x::ls
+
[usize_add_def] Definition
⊢ ∀x y. usize_add x y = mk_usize (usize_to_int x + usize_to_int y)
@@ -883,9 +1008,32 @@ sig
⊢ ∀x y. usize_sub x y = mk_usize (usize_to_int x − usize_to_int y)
+ [vec_index_def] Definition
+
+ ⊢ ∀i v.
+ vec_index i v =
+ if usize_to_int i ≤ usize_to_int (vec_len v) then
+ Return (index (usize_to_int i) (vec_to_list v))
+ else Fail Failure
+
+ [vec_insert_back_def] Definition
+
+ ⊢ ∀v i x.
+ vec_insert_back v i x =
+ mk_vec (update (vec_to_list v) (usize_to_int i) x)
+
[vec_len_def] Definition
- ⊢ ∀v. vec_len v = int_to_u32 (&LENGTH (vec_to_list v))
+ ⊢ ∀v. vec_len v = int_to_usize (len (vec_to_list v))
+
+ [vec_new_def] Definition
+
+ ⊢ vec_new =
+ case mk_vec [] of Return v => v | Fail v2 => ARB | Loop => ARB
+
+ [vec_push_back_def] Definition
+
+ ⊢ ∀v x. vec_push_back v x = mk_vec (vec_to_list v ⧺ [x])
[I128_ADD_EQ] Theorem
@@ -1140,6 +1288,14 @@ sig
∃z. i8_sub x y = Return z ∧
i8_to_int z = i8_to_int x − i8_to_int y
+ [INT_OF_NUM] Theorem
+
+ ⊢ ∀i. 0 ≤ i ⇒ &Num i = i
+
+ [INT_OF_NUM_NEQ_INJ] Theorem
+
+ ⊢ ∀n m. &n ≠ &m ⇒ n ≠ m
+
[ISIZE_ADD_EQ] Theorem
[oracles: DISK_THM]
@@ -1495,10 +1651,26 @@ sig
∃z. usize_sub x y = Return z ∧
usize_to_int z = usize_to_int x − usize_to_int y
+ [USIZE_TO_INT_INJ] Theorem
+
+ [oracles: DISK_THM] [axioms: int_to_usize_usize_to_int] []
+ ⊢ ∀i j. usize_to_int i = usize_to_int j ⇔ i = j
+
+ [USIZE_TO_INT_NEQ_INJ] Theorem
+
+ [oracles: DISK_THM] [axioms: int_to_usize_usize_to_int] []
+ ⊢ ∀i j. i ≠ j ⇒ usize_to_int i ≠ usize_to_int j
+
+ [VEC_NEW_SPEC] Theorem
+
+ [oracles: DISK_THM] [axioms: usize_bounds, MK_VEC_SPEC] []
+ ⊢ vec_to_list vec_new = []
+
[VEC_TO_LIST_INT_BOUNDS] Theorem
- [oracles: DISK_THM] [axioms: VEC_TO_LIST_BOUNDS] []
- ⊢ ∀v. (let l = &LENGTH (vec_to_list v) in 0 ≤ l ∧ l ≤ u32_max)
+ [oracles: DISK_THM] [axioms: usize_bounds, VEC_TO_LIST_BOUNDS] []
+ ⊢ ∀v. 0 ≤ &LENGTH (vec_to_list v) ∧
+ &LENGTH (vec_to_list v) ≤ usize_max
[datatype_error] Theorem
@@ -1554,6 +1726,23 @@ sig
⊢ ∀a. a = Failure
+ [index_update_diff] Theorem
+
+ ⊢ ∀ls i j y. 0 ≤ i ⇒ i < len ls ⇒ index i (update ls i y) = y
+
+ [index_update_same] Theorem
+
+ ⊢ ∀ls i j y.
+ 0 ≤ i ⇒
+ i < len ls ⇒
+ j < len ls ⇒
+ j ≠ i ⇒
+ index j (update ls i y) = index j ls
+
+ [int_induction] Theorem
+
+ ⊢ ∀P. P 0 ∧ (∀i. 0 ≤ i ∧ P i ⇒ P (i + 1)) ⇒ ∀i. 0 ≤ i ⇒ P i
+
[num2error_11] Theorem
⊢ ∀r r'. r < 1 ⇒ r' < 1 ⇒ (num2error r = num2error r' ⇔ r = r')
@@ -1607,6 +1796,48 @@ sig
⊢ ∀rr. (∃a. rr = Return a) ∨ (∃e. rr = Fail e) ∨ rr = Loop
+ [update_ind] Theorem
+
+ ⊢ ∀P. (∀i y. P [] i y) ∧ (∀v0 ls y. P (v0::ls) 0 y) ∧
+ (∀x ls i y. P ls i y ⇒ P (x::ls) (SUC i) y) ⇒
+ ∀v v1 v2. P v v1 v2
+
+ [update_len] Theorem
+
+ ⊢ ∀ls i y. len (update ls i y) = len ls
+
+ [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
+
+ [vec_insert_back_spec] Theorem
+
+ [oracles: DISK_THM, cheat]
+ [axioms: usize_to_int_bounds, int_to_usize_id, mk_vec_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 ∧
+ ∀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
+
+ [vec_len_spec] Theorem
+
+ [oracles: DISK_THM, cheat] [axioms: ] []
+ ⊢ ∀v. vec_len v = int_to_usize (len (vec_to_list v)) ∧
+ 0 ≤ len (vec_to_list v) ∧ len (vec_to_list v) ≤ usize_max
+
+ [vec_to_list_int_bounds] Theorem
+
+ [oracles: cheat] [axioms: ] []
+ ⊢ ∀v. 0 ≤ len (vec_to_list v) ∧ len (vec_to_list v) ≤ usize_max
+
*)
end
diff --git a/backends/hol4/testScript.sml b/backends/hol4/testScript.sml
index fe1c1e11..a2d15117 100644
--- a/backends/hol4/testScript.sml
+++ b/backends/hol4/testScript.sml
@@ -722,7 +722,7 @@ fun op PARTIAL_THEN1 (tac1: tactic) (tac2: tactic) : tactic = tac1 THEN_LT (NTH_
If the lemma is not an implication, we directly call the theorem tactic.
*)
-fun intro_premise_then (premise_tac: tactic) (then_tac: thm_tactic) (thm : thm) : tactic =
+fun sg_premise_then (premise_tac: tactic) (then_tac: thm_tactic) (thm : thm) : tactic =
let
val c = concl thm;
(* First case: there is a premise to prove *)
@@ -734,9 +734,9 @@ fun intro_premise_then (premise_tac: tactic) (then_tac: thm_tactic) (thm : thm)
if is_imp c then prove_premise_then (fst (dest_imp c)) else no_prove_premise_then
end
-(* Same as {!intro_premise_then} but fails if the premise_tac fails to prove the premise *)
+(* Same as {!sg_premise_then} but fails if the premise_tac fails to prove the premise *)
fun prove_premise_then (premise_tac: tactic) (then_tac: thm_tactic) (thm : thm) : tactic =
- intro_premise_then
+ sg_premise_then
(premise_tac >> FAIL_TAC "prove_premise_then: could not prove premise")
then_tac thm
@@ -1294,7 +1294,7 @@ fun pure_progress_with (premise_tac : tactic)
val th = PURE_REWRITE_RULE [GSYM satTheory.AND_IMP] th;
in
(* Apply the theorem *)
- intro_premise_then premise_tac (then_tac fgoal) th (asms, g)
+ sg_premise_then premise_tac (then_tac fgoal) th (asms, g)
end
(*