summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2023-06-02 11:24:10 +0200
committerSon HO2023-06-04 21:54:38 +0200
commit61566b9739ca01bee87daf508a3afc2a4c0c21c6 (patch)
tree82a8a8661e13c86523e0ea5d2d32b1f73532b436
parenta4864b30da15b2b011d7fd768d51f81c326edd58 (diff)
Remove some obsolete files from the HOL4 backend
Diffstat (limited to '')
-rw-r--r--backends/hol4/testHashmapScript.sml416
-rw-r--r--backends/hol4/testHashmapTheory.sig305
-rw-r--r--backends/hol4/testScript.sml1747
-rw-r--r--backends/hol4/testTheory.sig834
4 files changed, 0 insertions, 3302 deletions
diff --git a/backends/hol4/testHashmapScript.sml b/backends/hol4/testHashmapScript.sml
deleted file mode 100644
index c3f04cca..00000000
--- a/backends/hol4/testHashmapScript.sml
+++ /dev/null
@@ -1,416 +0,0 @@
-open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
-
-open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory
-open primitivesLib
-
-val _ = new_theory "testHashmap"
-
-(*
- * Examples of proofs
- *)
-
-Datatype:
- list_t =
- ListCons 't list_t
- | ListNil
-End
-
-val nth_mut_fwd_def = Define ‘
- nth_mut_fwd (ls : 't list_t) (i : u32) : 't result =
- case ls of
- | ListCons x tl =>
- if u32_to_int i = (0:int)
- then Return x
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- nth_mut_fwd tl i0
- od
- | ListNil =>
- Fail Failure
-’
-
-(*** Examples of proofs on [nth] *)
-val list_t_v_def = Define ‘
- list_t_v ListNil = [] /\
- list_t_v (ListCons x tl) = x :: list_t_v tl
-’
-
-Theorem nth_mut_fwd_spec:
- !(ls : 't list_t) (i : u32).
- u32_to_int i < len (list_t_v ls) ==>
- case nth_mut_fwd ls i of
- | Return x => x = index (u32_to_int i) (list_t_v ls)
- | Fail _ => F
- | Diverge => F
-Proof
- Induct_on ‘ls’ >> rw [list_t_v_def, len_def] >~ [‘ListNil’]
- >-(massage >> int_tac) >>
- pure_once_rewrite_tac [nth_mut_fwd_def] >> rw [] >>
- fs [index_eq] >>
- progress >> progress
-QED
-
-val _ = save_spec_thm "nth_mut_fwd_spec"
-
-val _ = new_constant ("insert", “: u32 -> 't -> (u32 # 't) list_t -> (u32 # 't) list_t result”)
-val insert_def = new_axiom ("insert_def", “
- insert (key : u32) (value : 't) (ls : (u32 # 't) list_t) : (u32 # 't) list_t result =
- case ls of
- | ListCons (ckey, cvalue) tl =>
- if ckey = key
- then Return (ListCons (ckey, value) tl)
- else
- do
- tl0 <- insert key value tl;
- Return (ListCons (ckey, cvalue) tl0)
- od
- | ListNil => Return (ListCons (key, value) ListNil)
- ”)
-
-(* Property that keys are pairwise distinct *)
-val distinct_keys_def = Define ‘
- distinct_keys (ls : (u32 # 't) list) =
- !i j.
- 0 ≤ i ⇒ i < j ⇒ j < len ls ⇒
- FST (index i ls) ≠ FST (index j ls)
-’
-
-val lookup_raw_def = Define ‘
- lookup_raw key [] = NONE /\
- lookup_raw key ((k, v) :: ls) =
- if k = key then SOME v else lookup_raw key ls
-’
-
-val lookup_def = Define ‘
- lookup key ls = lookup_raw key (list_t_v ls)
-’
-
-(* Lemma about ‘insert’, without the invariant *)
-Theorem insert_lem_aux:
- !ls key value.
- (* The keys are pairwise distinct *)
- case insert key value ls of
- | Return ls1 =>
- (* We updated the binding *)
- lookup key ls1 = SOME value /\
- (* The other bindings are left unchanged *)
- (!k. k <> key ==> lookup k ls = lookup k ls1)
- | Fail _ => F
- | Diverge => F
-Proof
- Induct_on ‘ls’ >> rw [list_t_v_def] >~ [‘ListNil’] >>
- pure_once_rewrite_tac [insert_def] >> rw []
- >- (rw [lookup_def, lookup_raw_def, list_t_v_def])
- >- (rw [lookup_def, lookup_raw_def, list_t_v_def]) >>
- case_tac >> rw []
- >- (rw [lookup_def, lookup_raw_def, list_t_v_def])
- >- (rw [lookup_def, lookup_raw_def, list_t_v_def]) >>
- progress >>
- fs [lookup_def, lookup_raw_def, list_t_v_def]
-QED
-
-(*
- * Invariant proof 1
- *)
-
-Theorem distinct_keys_cons:
- ∀ k v ls.
- (∀ i. 0 ≤ i ⇒ i < len ls ⇒ FST (index i ls) ≠ k) ⇒
- distinct_keys ls ⇒
- distinct_keys ((k,v) :: ls)
-Proof
- rw [] >>
- rw [distinct_keys_def] >>
- Cases_on ‘i = 0’ >> fs []
- >-(
- (* Use the first hypothesis *)
- fs [index_eq] >>
- last_x_assum (qspecl_assume [‘j - 1’]) >>
- sg ‘0 ≤ j - 1’ >- int_tac >>
- fs [len_def] >>
- sg ‘j - 1 < len ls’ >- int_tac >>
- fs []
- ) >>
- (* Use the second hypothesis *)
- sg ‘0 < i’ >- int_tac >>
- sg ‘0 < j’ >- int_tac >>
- fs [distinct_keys_def, index_eq, len_def] >>
- first_x_assum (qspecl_assume [‘i - 1’, ‘j - 1’]) >>
- sg ‘0 ≤ i - 1 ∧ i - 1 < j - 1 ∧ j - 1 < len ls’ >- int_tac >>
- fs []
-QED
-
-Theorem distinct_keys_tail:
- ∀ k v ls.
- distinct_keys ((k,v) :: ls) ⇒
- distinct_keys ls
-Proof
- rw [distinct_keys_def] >>
- last_x_assum (qspecl_assume [‘i + 1’, ‘j + 1’]) >>
- fs [len_def] >>
- sg ‘0 ≤ i + 1 ∧ i + 1 < j + 1 ∧ j + 1 < 1 + len ls’ >- int_tac >> fs [] >>
- sg ‘0 < i + 1 ∧ 0 < j + 1’ >- int_tac >> fs [index_eq] >>
- sg ‘i + 1 - 1 = i ∧ j + 1 - 1 = j’ >- int_tac >> fs []
-QED
-
-Theorem insert_index_neq:
- ∀ q k v ls0 ls1 i.
- (∀ j. 0 ≤ j ∧ j < len (list_t_v ls0) ⇒ q ≠ FST (index j (list_t_v ls0))) ⇒
- q ≠ k ⇒
- insert k v ls0 = Return ls1 ⇒
- 0 ≤ i ⇒
- i < len (list_t_v ls1) ⇒
- FST (index i (list_t_v ls1)) ≠ q
-Proof
- ntac 3 strip_tac >>
- Induct_on ‘ls0’ >> rw [] >~ [‘ListNil’]
- >-(
- fs [insert_def] >>
- sg ‘ls1 = ListCons (k,v) ListNil’ >- fs [] >> fs [list_t_v_def, len_def] >>
- sg ‘i = 0’ >- int_tac >> fs [index_eq]) >>
- Cases_on ‘t’ >>
- Cases_on ‘i = 0’ >> fs []
- >-(
- qpat_x_assum ‘insert _ _ _ = _’ mp_tac >>
- simp [MK_BOUNDED insert_def 1, bind_def] >>
- Cases_on ‘q' = k’ >> rw []
- >- (fs [list_t_v_def, index_eq]) >>
- Cases_on ‘insert k v ls0’ >> fs [] >>
- gvs [list_t_v_def, index_eq] >>
- first_x_assum (qspec_assume ‘0’) >>
- fs [len_def] >>
- strip_tac >>
- qspec_assume ‘list_t_v ls0’ len_pos >>
- sg ‘0 < 1 + len (list_t_v ls0)’ >- int_tac >>
- fs []) >>
- qpat_x_assum ‘insert _ _ _ = _’ mp_tac >>
- simp [MK_BOUNDED insert_def 1, bind_def] >>
- Cases_on ‘q' = k’ >> rw []
- >-(
- fs [list_t_v_def, index_eq, len_def] >>
- first_x_assum (qspec_assume ‘i’) >> rfs []) >>
- Cases_on ‘insert k v ls0’ >> fs [] >>
- gvs [list_t_v_def, index_eq] >>
- last_x_assum (qspec_assume ‘i - 1’) >>
- fs [len_def] >>
- sg ‘0 ≤ i - 1 ∧ i - 1 < len (list_t_v a)’ >- int_tac >> fs [] >>
- first_x_assum irule >>
- rw [] >>
- last_x_assum (qspec_assume ‘j + 1’) >>
- rfs [] >>
- sg ‘j + 1 < 1 + len (list_t_v ls0) ∧ j + 1 − 1 = j ∧ j + 1 ≠ 0’ >- int_tac >> fs []
-QED
-
-Theorem distinct_keys_insert_index_neq:
- ∀ k v q r ls0 ls1 i.
- distinct_keys ((q,r)::list_t_v ls0) ⇒
- q ≠ k ⇒
- insert k v ls0 = Return ls1 ⇒
- 0 ≤ i ⇒
- i < len (list_t_v ls1) ⇒
- FST (index i (list_t_v ls1)) ≠ q
-Proof
- rw [] >>
- (* Use the first assumption to prove the following assertion *)
- sg ‘∀ j. 0 ≤ j ∧ j < len (list_t_v ls0) ⇒ q ≠ FST (index j (list_t_v ls0))’
- >-(
- strip_tac >>
- fs [distinct_keys_def] >>
- last_x_assum (qspecl_assume [‘0’, ‘j + 1’]) >>
- fs [index_eq] >>
- sg ‘j + 1 - 1 = j’ >- int_tac >> fs [len_def] >>
- rw []>>
- first_x_assum irule >> int_tac) >>
- qspecl_assume [‘q’, ‘k’, ‘v’, ‘ls0’, ‘ls1’, ‘i’] insert_index_neq >>
- fs []
-QED
-
-Theorem distinct_keys_insert:
- ∀ k v ls0 ls1.
- distinct_keys (list_t_v ls0) ⇒
- insert k v ls0 = Return ls1 ⇒
- distinct_keys (list_t_v ls1)
-Proof
- Induct_on ‘ls0’ >~ [‘ListNil’]
- >-(
- rw [distinct_keys_def, list_t_v_def, insert_def] >>
- fs [list_t_v_def, len_def] >>
- int_tac) >>
- Cases >>
- pure_once_rewrite_tac [insert_def] >> fs[] >>
- rw [] >> fs []
- >-(
- (* k = q *)
- last_x_assum ignore_tac >>
- fs [distinct_keys_def] >>
- rw [] >>
- last_x_assum (qspecl_assume [‘i’, ‘j’]) >>
- rfs [list_t_v_def, len_def] >>
- sg ‘0 < j’ >- int_tac >>
- Cases_on ‘i = 0’ >> gvs [index_eq]) >>
- (* k ≠ q: recursion *)
- Cases_on ‘insert k v ls0’ >> fs [bind_def] >>
- last_x_assum (qspecl_assume [‘k’, ‘v’, ‘a’]) >>
- gvs [list_t_v_def] >>
- imp_res_tac distinct_keys_tail >> fs [] >>
- irule distinct_keys_cons >> rw [] >>
- metis_tac [distinct_keys_insert_index_neq]
-QED
-
-Theorem insert_lem:
- !ls key value.
- (* The keys are pairwise distinct *)
- distinct_keys (list_t_v ls) ==>
- case insert key value ls of
- | Return ls1 =>
- (* We updated the binding *)
- lookup key ls1 = SOME value /\
- (* The other bindings are left unchanged *)
- (!k. k <> key ==> lookup k ls = lookup k ls1) ∧
- (* The keys are still pairwise disjoint *)
- distinct_keys (list_t_v ls1)
- | Fail _ => F
- | Diverge => F
-Proof
- rw [] >>
- qspecl_assume [‘ls’, ‘key’, ‘value’] insert_lem_aux >>
- case_tac >> fs [] >>
- metis_tac [distinct_keys_insert]
-QED
-
-(*
- * Invariant proof 2: functional version of the invariant
- *)
-val for_all_def = Define ‘
- for_all p [] = T ∧
- for_all p (x :: ls) = (p x ∧ for_all p ls)
-’
-
-val pairwise_rel_def = Define ‘
- pairwise_rel p [] = T ∧
- pairwise_rel p (x :: ls) = (for_all (p x) ls ∧ pairwise_rel p ls)
-’
-
-val distinct_keys_f_def = Define ‘
- distinct_keys_f (ls : (u32 # 't) list) =
- pairwise_rel (\x y. FST x ≠ FST y) ls
-’
-
-Theorem distinct_keys_f_insert_for_all:
- ∀k v k1 ls0 ls1.
- k1 ≠ k ⇒
- for_all (λy. k1 ≠ FST y) (list_t_v ls0) ⇒
- pairwise_rel (λx y. FST x ≠ FST y) (list_t_v ls0) ⇒
- insert k v ls0 = Return ls1 ⇒
- for_all (λy. k1 ≠ FST y) (list_t_v ls1)
-Proof
- Induct_on ‘ls0’ >> rw [pairwise_rel_def] >~ [‘ListNil’] >>
- gvs [list_t_v_def, pairwise_rel_def, for_all_def]
- >-(gvs [MK_BOUNDED insert_def 1, bind_def, list_t_v_def, for_all_def]) >>
- pat_undisch_tac ‘insert _ _ _ = _’ >>
- simp [MK_BOUNDED insert_def 1, bind_def] >>
- Cases_on ‘t’ >> rw [] >> gvs [list_t_v_def, pairwise_rel_def, for_all_def] >>
- Cases_on ‘insert k v ls0’ >>
- gvs [distinct_keys_f_def, list_t_v_def, pairwise_rel_def, for_all_def] >>
- metis_tac []
-QED
-
-Theorem distinct_keys_f_insert:
- ∀ k v ls0 ls1.
- distinct_keys_f (list_t_v ls0) ⇒
- insert k v ls0 = Return ls1 ⇒
- distinct_keys_f (list_t_v ls1)
-Proof
- Induct_on ‘ls0’ >> rw [distinct_keys_f_def] >~ [‘ListNil’]
- >-(
- fs [list_t_v_def, insert_def] >>
- gvs [list_t_v_def, pairwise_rel_def, for_all_def]) >>
- last_x_assum (qspecl_assume [‘k’, ‘v’]) >>
- pat_undisch_tac ‘insert _ _ _ = _’ >>
- simp [MK_BOUNDED insert_def 1, bind_def] >>
- (* TODO: improve case_tac *)
- Cases_on ‘t’ >> rw [] >> gvs [list_t_v_def, pairwise_rel_def, for_all_def] >>
- Cases_on ‘insert k v ls0’ >>
- gvs [distinct_keys_f_def, list_t_v_def, pairwise_rel_def, for_all_def] >>
- metis_tac [distinct_keys_f_insert_for_all]
-QED
-
-(*
- * Proving equivalence between the two version - exercise.
- *)
-Theorem for_all_quant:
- ∀p ls. for_all p ls ⇔ ∀i. 0 ≤ i ⇒ i < len ls ⇒ p (index i ls)
-Proof
- strip_tac >> Induct_on ‘ls’
- >-(rw [for_all_def, len_def] >> int_tac) >>
- rw [for_all_def, len_def, index_eq] >>
- equiv_tac
- >-(
- rw [] >>
- Cases_on ‘i = 0’ >> fs [] >>
- first_x_assum irule >>
- int_tac) >>
- rw []
- >-(
- first_x_assum (qspec_assume ‘0’) >> fs [] >>
- first_x_assum irule >>
- qspec_assume ‘ls’ len_pos >>
- int_tac) >>
- first_x_assum (qspec_assume ‘i + 1’) >>
- fs [] >>
- sg ‘i + 1 ≠ 0 ∧ i + 1 - 1 = i’ >- int_tac >> fs [] >>
- first_x_assum irule >> int_tac
-QED
-
-Theorem pairwise_rel_quant:
- ∀p ls. pairwise_rel p ls ⇔
- (∀i j. 0 ≤ i ⇒ i < j ⇒ j < len ls ⇒ p (index i ls) (index j ls))
-Proof
- strip_tac >> Induct_on ‘ls’
- >-(rw [pairwise_rel_def, len_def] >> int_tac) >>
- rw [pairwise_rel_def, len_def] >>
- equiv_tac
- >-(
- (* ==> *)
- rw [] >>
- sg ‘0 < j’ >- int_tac >>
- Cases_on ‘i = 0’
- >-(
- simp [index_eq] >>
- qspecl_assume [‘p h’, ‘ls’] (iffLR for_all_quant) >>
- first_x_assum irule >> fs [] >> int_tac
- ) >>
- rw [index_eq] >>
- first_x_assum irule >> int_tac
- ) >>
- (* <== *)
- rw []
- >-(
- rw [for_all_quant] >>
- first_x_assum (qspecl_assume [‘0’, ‘i + 1’]) >>
- sg ‘0 < i + 1 ∧ i + 1 - 1 = i’ >- int_tac >>
- fs [index_eq] >>
- first_x_assum irule >> int_tac
- ) >>
- sg ‘pairwise_rel p ls’
- >-(
- rw [pairwise_rel_def] >>
- first_x_assum (qspecl_assume [‘i' + 1’, ‘j' + 1’]) >>
- sg ‘0 < i' + 1 ∧ 0 < j' + 1’ >- int_tac >>
- fs [index_eq, int_add_minus_same_eq] >>
- first_x_assum irule >> int_tac
- ) >>
- fs []
-QED
-
-Theorem distinct_keys_f_eq_distinct_keys:
- ∀ ls.
- distinct_keys_f ls ⇔ distinct_keys ls
-Proof
- rw [distinct_keys_def, distinct_keys_f_def] >>
- qspecl_assume [‘(λx y. FST x ≠ FST y)’, ‘ls’] pairwise_rel_quant >>
- fs []
-QED
-
-val _ = export_theory ()
diff --git a/backends/hol4/testHashmapTheory.sig b/backends/hol4/testHashmapTheory.sig
deleted file mode 100644
index 1d304723..00000000
--- a/backends/hol4/testHashmapTheory.sig
+++ /dev/null
@@ -1,305 +0,0 @@
-signature testHashmapTheory =
-sig
- type thm = Thm.thm
-
- (* Axioms *)
- val insert_def : thm
-
- (* Definitions *)
- val distinct_keys_def : thm
- val distinct_keys_f_def : thm
- val for_all_def : thm
- val list_t_TY_DEF : thm
- val list_t_case_def : thm
- val list_t_size_def : thm
- val list_t_v_def : thm
- val lookup_def : thm
- val pairwise_rel_def : thm
-
- (* Theorems *)
- val datatype_list_t : thm
- val distinct_keys_cons : thm
- val distinct_keys_f_eq_distinct_keys : thm
- val distinct_keys_f_insert : thm
- val distinct_keys_f_insert_for_all : thm
- val distinct_keys_insert : thm
- val distinct_keys_insert_index_neq : thm
- val distinct_keys_tail : thm
- val for_all_quant : thm
- val insert_index_neq : thm
- val insert_lem : thm
- val insert_lem_aux : thm
- val list_t_11 : thm
- val list_t_Axiom : thm
- val list_t_case_cong : thm
- val list_t_case_eq : thm
- val list_t_distinct : thm
- val list_t_induction : thm
- val list_t_nchotomy : thm
- val lookup_raw_def : thm
- val lookup_raw_ind : thm
- val nth_mut_fwd_def : thm
- val nth_mut_fwd_ind : thm
- val nth_mut_fwd_spec : thm
- val pairwise_rel_quant : thm
-
- val testHashmap_grammars : type_grammar.grammar * term_grammar.grammar
-(*
- [primitives] Parent theory of "testHashmap"
-
- [insert_def] Axiom
-
- [oracles: ] [axioms: insert_def] []
- ⊢ insert key value ls =
- case ls of
- ListCons (ckey,cvalue) tl =>
- if ckey = key then Return (ListCons (ckey,value) tl)
- else
- do
- tl0 <- insert key value tl;
- Return (ListCons (ckey,cvalue) tl0)
- od
- | ListNil => Return (ListCons (key,value) ListNil)
-
- [distinct_keys_def] Definition
-
- ⊢ ∀ls.
- distinct_keys ls ⇔
- ∀i j.
- 0 ≤ i ⇒
- i < j ⇒
- j < len ls ⇒
- FST (index i ls) ≠ FST (index j ls)
-
- [distinct_keys_f_def] Definition
-
- ⊢ ∀ls. distinct_keys_f ls ⇔ pairwise_rel (λx y. FST x ≠ FST y) ls
-
- [for_all_def] Definition
-
- ⊢ (∀p. for_all p [] ⇔ T) ∧
- ∀p x ls. for_all p (x::ls) ⇔ p x ∧ for_all p ls
-
- [list_t_TY_DEF] Definition
-
- ⊢ ∃rep.
- TYPE_DEFINITION
- (λa0'.
- ∀ $var$('list_t').
- (∀a0'.
- (∃a0 a1.
- a0' =
- (λa0 a1.
- ind_type$CONSTR 0 a0
- (ind_type$FCONS a1 (λn. ind_type$BOTTOM)))
- a0 a1 ∧ $var$('list_t') a1) ∨
- a0' =
- ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ⇒
- $var$('list_t') a0') ⇒
- $var$('list_t') a0') rep
-
- [list_t_case_def] Definition
-
- ⊢ (∀a0 a1 f v. list_t_CASE (ListCons a0 a1) f v = f a0 a1) ∧
- ∀f v. list_t_CASE ListNil f v = v
-
- [list_t_size_def] Definition
-
- ⊢ (∀f a0 a1.
- list_t_size f (ListCons a0 a1) = 1 + (f a0 + list_t_size f a1)) ∧
- ∀f. list_t_size f ListNil = 0
-
- [list_t_v_def] Definition
-
- ⊢ list_t_v ListNil = [] ∧
- ∀x tl. list_t_v (ListCons x tl) = x::list_t_v tl
-
- [lookup_def] Definition
-
- ⊢ ∀key ls. lookup key ls = lookup_raw key (list_t_v ls)
-
- [pairwise_rel_def] Definition
-
- ⊢ (∀p. pairwise_rel p [] ⇔ T) ∧
- ∀p x ls.
- pairwise_rel p (x::ls) ⇔ for_all (p x) ls ∧ pairwise_rel p ls
-
- [datatype_list_t] Theorem
-
- ⊢ DATATYPE (list_t ListCons ListNil)
-
- [distinct_keys_cons] Theorem
-
- ⊢ ∀k v ls.
- (∀i. 0 ≤ i ⇒ i < len ls ⇒ FST (index i ls) ≠ k) ⇒
- distinct_keys ls ⇒
- distinct_keys ((k,v)::ls)
-
- [distinct_keys_f_eq_distinct_keys] Theorem
-
- ⊢ ∀ls. distinct_keys_f ls ⇔ distinct_keys ls
-
- [distinct_keys_f_insert] Theorem
-
- [oracles: DISK_THM] [axioms: insert_def] []
- ⊢ ∀k v ls0 ls1.
- distinct_keys_f (list_t_v ls0) ⇒
- insert k v ls0 = Return ls1 ⇒
- distinct_keys_f (list_t_v ls1)
-
- [distinct_keys_f_insert_for_all] Theorem
-
- [oracles: DISK_THM] [axioms: insert_def] []
- ⊢ ∀k v k1 ls0 ls1.
- k1 ≠ k ⇒
- for_all (λy. k1 ≠ FST y) (list_t_v ls0) ⇒
- pairwise_rel (λx y. FST x ≠ FST y) (list_t_v ls0) ⇒
- insert k v ls0 = Return ls1 ⇒
- for_all (λy. k1 ≠ FST y) (list_t_v ls1)
-
- [distinct_keys_insert] Theorem
-
- [oracles: DISK_THM] [axioms: insert_def] []
- ⊢ ∀k v ls0 ls1.
- distinct_keys (list_t_v ls0) ⇒
- insert k v ls0 = Return ls1 ⇒
- distinct_keys (list_t_v ls1)
-
- [distinct_keys_insert_index_neq] Theorem
-
- [oracles: DISK_THM] [axioms: insert_def] []
- ⊢ ∀k v q r ls0 ls1 i.
- distinct_keys ((q,r)::list_t_v ls0) ⇒
- q ≠ k ⇒
- insert k v ls0 = Return ls1 ⇒
- 0 ≤ i ⇒
- i < len (list_t_v ls1) ⇒
- FST (index i (list_t_v ls1)) ≠ q
-
- [distinct_keys_tail] Theorem
-
- ⊢ ∀k v ls. distinct_keys ((k,v)::ls) ⇒ distinct_keys ls
-
- [for_all_quant] Theorem
-
- ⊢ ∀p ls. for_all p ls ⇔ ∀i. 0 ≤ i ⇒ i < len ls ⇒ p (index i ls)
-
- [insert_index_neq] Theorem
-
- [oracles: DISK_THM] [axioms: insert_def] []
- ⊢ ∀q k v ls0 ls1 i.
- (∀j. 0 ≤ j ∧ j < len (list_t_v ls0) ⇒
- q ≠ FST (index j (list_t_v ls0))) ⇒
- q ≠ k ⇒
- insert k v ls0 = Return ls1 ⇒
- 0 ≤ i ⇒
- i < len (list_t_v ls1) ⇒
- FST (index i (list_t_v ls1)) ≠ q
-
- [insert_lem] Theorem
-
- [oracles: DISK_THM] [axioms: insert_def] []
- ⊢ ∀ls key value.
- distinct_keys (list_t_v ls) ⇒
- case insert key value ls of
- Return ls1 =>
- lookup key ls1 = SOME value ∧
- (∀k. k ≠ key ⇒ lookup k ls = lookup k ls1) ∧
- distinct_keys (list_t_v ls1)
- | Fail v1 => F
- | Diverge => F
-
- [insert_lem_aux] Theorem
-
- [oracles: DISK_THM] [axioms: insert_def] []
- ⊢ ∀ls key value.
- case insert key value ls of
- Return ls1 =>
- lookup key ls1 = SOME value ∧
- ∀k. k ≠ key ⇒ lookup k ls = lookup k ls1
- | Fail v1 => F
- | Diverge => F
-
- [list_t_11] Theorem
-
- ⊢ ∀a0 a1 a0' a1'.
- ListCons a0 a1 = ListCons a0' a1' ⇔ a0 = a0' ∧ a1 = a1'
-
- [list_t_Axiom] Theorem
-
- ⊢ ∀f0 f1. ∃fn.
- (∀a0 a1. fn (ListCons a0 a1) = f0 a0 a1 (fn a1)) ∧
- fn ListNil = f1
-
- [list_t_case_cong] Theorem
-
- ⊢ ∀M M' f v.
- M = M' ∧ (∀a0 a1. M' = ListCons a0 a1 ⇒ f a0 a1 = f' a0 a1) ∧
- (M' = ListNil ⇒ v = v') ⇒
- list_t_CASE M f v = list_t_CASE M' f' v'
-
- [list_t_case_eq] Theorem
-
- ⊢ list_t_CASE x f v = v' ⇔
- (∃t l. x = ListCons t l ∧ f t l = v') ∨ x = ListNil ∧ v = v'
-
- [list_t_distinct] Theorem
-
- ⊢ ∀a1 a0. ListCons a0 a1 ≠ ListNil
-
- [list_t_induction] Theorem
-
- ⊢ ∀P. (∀l. P l ⇒ ∀t. P (ListCons t l)) ∧ P ListNil ⇒ ∀l. P l
-
- [list_t_nchotomy] Theorem
-
- ⊢ ∀ll. (∃t l. ll = ListCons t l) ∨ ll = ListNil
-
- [lookup_raw_def] Theorem
-
- ⊢ (∀key. lookup_raw key [] = NONE) ∧
- ∀v ls key k.
- lookup_raw key ((k,v)::ls) =
- if k = key then SOME v else lookup_raw key ls
-
- [lookup_raw_ind] Theorem
-
- ⊢ ∀P. (∀key. P key []) ∧
- (∀key k v ls. (k ≠ key ⇒ P key ls) ⇒ P key ((k,v)::ls)) ⇒
- ∀v v1. P v v1
-
- [nth_mut_fwd_def] Theorem
-
- ⊢ ∀ls i.
- nth_mut_fwd ls i =
- case ls of
- ListCons x tl =>
- if u32_to_int i = 0 then Return x
- else do i0 <- u32_sub i (int_to_u32 1); nth_mut_fwd tl i0 od
- | ListNil => Fail Failure
-
- [nth_mut_fwd_ind] Theorem
-
- ⊢ ∀P. (∀ls i.
- (∀x tl i0. ls = ListCons x tl ∧ u32_to_int i ≠ 0 ⇒ P tl i0) ⇒
- P ls i) ⇒
- ∀v v1. P v v1
-
- [nth_mut_fwd_spec] Theorem
-
- ⊢ ∀ls i.
- u32_to_int i < len (list_t_v ls) ⇒
- case nth_mut_fwd ls i of
- Return x => x = index (u32_to_int i) (list_t_v ls)
- | Fail v1 => F
- | Diverge => F
-
- [pairwise_rel_quant] Theorem
-
- ⊢ ∀p ls.
- pairwise_rel p ls ⇔
- ∀i j. 0 ≤ i ⇒ i < j ⇒ j < len ls ⇒ p (index i ls) (index j ls)
-
-
-*)
-end
diff --git a/backends/hol4/testScript.sml b/backends/hol4/testScript.sml
deleted file mode 100644
index 8b4d523c..00000000
--- a/backends/hol4/testScript.sml
+++ /dev/null
@@ -1,1747 +0,0 @@
-open HolKernel boolLib bossLib Parse
-
-val primitives_theory_name = "test"
-val _ = new_theory primitives_theory_name
-
-open boolTheory integerTheory wordsTheory stringTheory
-
-Datatype:
- error = Failure
-End
-
-Datatype:
- result = Return 'a | Fail error | Loop
-End
-
-Type M = ``: 'a result``
-
-(* TODO: rename *)
-val st_ex_bind_def = Define `
- (st_ex_bind : 'a M -> ('a -> 'b M) -> 'b M) x f =
- case x of
- Return y => f y
- | Fail e => Fail e
- | Loop => Loop`;
-
-val bind_name = fst (dest_const “st_ex_bind”)
-
-val st_ex_return_def = Define `
- (st_ex_return : 'a -> 'a M) x =
- Return x`;
-
-Overload monad_bind[local] = ``st_ex_bind``
-Overload monad_unitbind[local] = ``\x y. st_ex_bind x (\z. y)``
-Overload monad_ignore_bind[local] = ``\x y. st_ex_bind x (\z. y)``
-(*Overload ex_bind[local] = ``st_ex_bind`` *)
-(* Overload ex_return[local] = ``st_ex_return`` *)
-(*Overload failwith = ``raise_Fail``*)
-
-(* Temporarily allow the monadic syntax *)
-val _ = monadsyntax.temp_add_monadsyntax ()
-
-val test1_def = Define `
- test1 (x : bool) = Return x`
-
-val is_true_def = Define ‘
- is_true (x : bool) = if x then Return () else Fail Failure’
-
-val test1_def = Define ‘
- test1 (x : bool) = Return x’
-
-val test_monad_def = Define `
- test_monad v =
- do
- x <- Return v;
- Return x
- od`
-
-val test_monad2_def = Define `
- test_monad2 =
- do
- x <- Return T;
- Return x
- od`
-
-val test_monad3_def = Define `
- test_monad3 x =
- do
- is_true x;
- Return x
- od`
-
-(**
- * Arithmetic
- *)
-
-open intLib
-
-val test_int1 = Define ‘int1 = 32’
-val test_int2 = Define ‘int2 = -32’
-
-Theorem INT_THM1:
- !(x y : int). x > 0 ==> y > 0 ==> x + y > 0
-Proof
- ARITH_TAC
-QED
-
-Theorem INT_THM2:
- !(x : int). T
-Proof
- rw[]
-QED
-
-val _ = prefer_int ()
-
-val x = “-36217863217862718”
-
-(* Deactivate notations for int *)
-val _ = deprecate_int ()
-open arithmeticTheory
-
-
-val m = Hol_pp.print_apropos
-val f = Hol_pp.print_find
-
-(* Display types on/off: M-h C-t *)
-(* Move back: M-h b *)
-
-val _ = numLib.deprecate_num ()
-val _ = numLib.prefer_num ()
-
-Theorem NAT_THM1:
- !(n : num). n < n + 1
-Proof
- Induct_on ‘n’ >> DECIDE_TAC
-QED
-
-Theorem NAT_THM2:
- !(n : num). n < n + (1 : num)
-Proof
- gen_tac >>
- Induct_on ‘n’ >- (
- PURE_REWRITE_TAC [ADD, NUMERAL_DEF, BIT1, ALT_ZERO] >>
- PURE_REWRITE_TAC [prim_recTheory.LESS_0_0]) >>
- PURE_REWRITE_TAC [ADD] >>
- irule prim_recTheory.LESS_MONO >>
- asm_rewrite_tac []
-QED
-
-
-val x = “1278361286371286:num”
-
-
-(********************** PRIMITIVES *)
-val _ = prefer_int ()
-
-val _ = new_type ("u32", 0)
-val _ = new_type ("i32", 0)
-
-(*val u32_min_def = Define ‘u32_min = (0:int)’*)
-val u32_max_def = Define ‘u32_max = (4294967295:int)’
-
-(* TODO: change that *)
-val usize_max_def = Define ‘usize_max = (4294967295:int)’
-
-val i32_min_def = Define ‘i32_min = (-2147483648:int)’
-val i32_max_def = Define ‘i32_max = (2147483647:int)’
-
-val _ = new_constant ("u32_to_int", “:u32 -> int”)
-val _ = new_constant ("i32_to_int", “:i32 -> int”)
-
-val _ = new_constant ("int_to_u32", “:int -> u32”)
-val _ = new_constant ("int_to_i32", “:int -> i32”)
-
-
-(* TODO: change to "...of..." *)
-val u32_to_int_bounds =
- new_axiom (
- "u32_to_int_bounds",
- “!n. 0 <= u32_to_int n /\ u32_to_int n <= u32_max”)
-
-val i32_to_int_bounds =
- new_axiom (
- "i32_to_int_bounds",
- “!n. i32_min <= i32_to_int n /\ i32_to_int n <= i32_max”)
-
-val int_to_u32_id = new_axiom ("int_to_u32_id",
- “!n. 0 <= n /\ n <= u32_max ==> u32_to_int (int_to_u32 n) = n”)
-
-val int_to_i32_id =
- new_axiom (
- "int_to_i32_id",
- “!n. i32_min <= n /\ n <= i32_max ==>
- i32_to_int (int_to_i32 n) = n”)
-
-val mk_u32_def = Define
- ‘mk_u32 n =
- if 0 <= n /\ n <= u32_max then Return (int_to_u32 n)
- else Fail Failure’
-
-val u32_add_def = Define ‘u32_add x y = mk_u32 ((u32_to_int x) + (u32_to_int y))’
-
-Theorem MK_U32_SUCCESS:
- !n. 0 <= n /\ n <= u32_max ==>
- mk_u32 n = Return (int_to_u32 n)
-Proof
- rw[mk_u32_def]
-QED
-
-Theorem U32_ADD_EQ:
- !x y.
- u32_to_int x + u32_to_int y <= u32_max ==>
- ?z. u32_add x y = Return z /\ u32_to_int z = u32_to_int x + u32_to_int y
-Proof
- rpt gen_tac >>
- rpt DISCH_TAC >>
- exists_tac “int_to_u32 (u32_to_int x + u32_to_int y)” >>
- imp_res_tac MK_U32_SUCCESS >>
- (* There is probably a better way of doing this *)
- sg ‘0 <= u32_to_int x’ >- (rw[u32_to_int_bounds]) >>
- sg ‘0 <= u32_to_int y’ >- (rw[u32_to_int_bounds]) >>
- fs [u32_add_def] >>
- irule int_to_u32_id >>
- fs[]
-QED
-
-val u32_sub_def = Define ‘u32_sub x y = mk_u32 ((u32_to_int x) - (u32_to_int y))’
-
-Theorem U32_SUB_EQ:
- !x y.
- 0 <= u32_to_int x - u32_to_int y ==>
- ?z. u32_sub x y = Return z /\ u32_to_int z = u32_to_int x - u32_to_int y
-Proof
- rpt gen_tac >>
- rpt DISCH_TAC >>
- exists_tac “int_to_u32 (u32_to_int x - u32_to_int y)” >>
- imp_res_tac MK_U32_SUCCESS >>
- (* There is probably a better way of doing this *)
- sg ‘u32_to_int x − u32_to_int y ≤ u32_max’ >-(
- sg ‘u32_to_int x <= u32_max’ >- (rw[u32_to_int_bounds]) >>
- sg ‘0 <= u32_to_int y’ >- (rw[u32_to_int_bounds]) >>
- COOPER_TAC
- ) >>
- fs [u32_sub_def] >>
- irule int_to_u32_id >>
- fs[]
-QED
-
-val mk_i32_def = Define
- ‘mk_i32 n =
- if i32_min <= n /\ n <= i32_max then Return (int_to_i32 n)
- else Fail Failure’
-
-val i32_add_def = Define ‘i32_add x y = mk_i32 ((i32_to_int x) + (i32_to_int y))’
-
-Theorem MK_I32_SUCCESS:
- !n. i32_min <= n /\ n <= i32_max ==>
- mk_i32 n = Return (int_to_i32 n)
-Proof
- rw[mk_i32_def]
-QED
-
-Theorem I32_ADD_EQ:
- !x y.
- i32_min <= i32_to_int x + i32_to_int y ==>
- i32_to_int x + i32_to_int y <= i32_max ==>
- ?z. i32_add x y = Return z /\ i32_to_int z = i32_to_int x + i32_to_int y
-Proof
- rpt gen_tac >>
- rpt DISCH_TAC >>
- exists_tac “int_to_i32 (i32_to_int x + i32_to_int y)” >>
- imp_res_tac MK_I32_SUCCESS >>
- fs [i32_min_def, i32_add_def] >>
- irule int_to_i32_id >>
- fs[i32_min_def]
-QED
-
-open listTheory
-
-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)))’
-
-(*
-(* Useless *)
-Theorem VEC_LEN_BOUNDS:
- !v. u32_min <= u32_to_int (vec_len v) /\ u32_to_int (vec_len v) <= u32_max
-Proof
- gen_tac >>
- qspec_then ‘v’ assume_tac VEC_TO_LIST_INT_BOUNDS >>
- fs[VEC_LEN_DEF] >>
- IMP_RES_TAC int_to_u32_id >>
- fs[]
-QED
-*)
-
-(* The type parameters are ordered in alphabetical order *)
-Datatype:
- test = Variant1 'b | Variant2 'a
-End
-
-Datatype:
- test2 = Variant1_1 'T2 | Variant2_1 'T1
-End
-
-Datatype:
- test2 = Variant1_2 'T1 | Variant2_2 'T2
-End
-
-(*
-“Variant1_1 3”
-“Variant1_2 3”
-
-type_of “CONS 3”
-*)
-
-(* TODO: argument order, we must also omit arguments in new type *)
-Datatype:
- list_t =
- ListCons 't list_t
- | ListNil
-End
-
-val list_nth_mut_loop_loop_fwd_def = Define ‘
- list_nth_mut_loop_loop_fwd (ls : 't list_t) (i : u32) : 't result =
- case ls of
- | ListCons x tl =>
- if u32_to_int i = (0:int)
- then Return x
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- list_nth_mut_loop_loop_fwd tl i0
- od
- | ListNil =>
- Fail Failure
-’
-
-(*
-CoInductive coind:
- !x y. coind x /\ coind y ==> coind (x + y)
-End
-*)
-
-(*
-(* This generates inconsistent theorems *)
-CoInductive loop:
- !x. loop x = if x then loop x else 0
-End
-
-CoInductive loop:
- !(x : int). loop x = if x > 0 then loop (x - 1) else 0
-End
-*)
-
-(* This terminates *)
-val list_nth_mut_loop_loop_fwd_def = Define ‘
- list_nth_mut_loop_loop_fwd (ls : 't list_t) (i : u32) : 't result =
- case ls of
- | ListCons x tl =>
- if u32_to_int i = (0:int)
- then Return x
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- list_nth_mut_loop_loop_fwd tl i0
- od
- | ListNil =>
- Fail Failure
-’
-
-(* This is sort of a coinductive definition.
-
- This can be justified:
- - we first define a version [nth_fuel] which uses fuel (and is thus terminating)
- - we define the predicate P:
- P ls i n = case nth_fuel n ls i of Return _ => T | _ => F
- - we then use [LEAST] (least upper bound for natural numbers) to define nth as:
- “nth ls i = if (?n. P n) then nth_fuel (LEAST (P ls i)) ls i else Fail Loop ”
- - we finally prove that nth satisfies the proper equation.
-
- We would need the following intermediate lemma:
- !n.
- n < LEAST (P ls i) ==> nth_fuel n ls i = Fail _ /\
- n >= LEAST (P ls i) ==> nth_fuel n ls i = nth_fuel (LEAST P ls i) ls i
-
- *)
-val _ = new_constant ("nth", “:'t list_t -> u32 -> 't result”)
-val nth_def = new_axiom ("nth_def", “
- nth (ls : 't list_t) (i : u32) : 't result =
- case ls of
- | ListCons x tl =>
- if u32_to_int i = (0:int)
- then Return x
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- nth tl i0
- od
- | ListNil =>
- Fail Failure
- ”)
-
-
-(*** Examples of proofs on [nth] *)
-val list_t_v_def = Define ‘
- list_t_v ListNil = [] /\
- list_t_v (ListCons x tl) = x :: list_t_v tl
-’
-
-(* TODO: move *)
-open dep_rewrite
-open integerTheory
-
-(* Ignore a theorem.
-
- To be used in conjunction with {!pop_assum} for instance.
- *)
-fun IGNORE_TAC (_ : thm) : tactic = ALL_TAC
-
-
-Theorem INT_OF_NUM_INJ:
- !n m. &n = &m ==> n = m
-Proof
- rpt strip_tac >>
- fs [Num]
-QED
-
-Theorem NUM_SUB_EQ:
- !(x y z : int). x = y - z ==> 0 <= x ==> 0 <= z ==> Num y = Num z + Num x
-Proof
- rpt strip_tac >>
- sg ‘0 <= y’ >- COOPER_TAC >>
- rfs [] >>
- (* Convert to integers *)
- irule INT_OF_NUM_INJ >>
- imp_res_tac (GSYM INT_OF_NUM) >>
- (* Associativity of & *)
- PURE_REWRITE_TAC [GSYM INT_ADD] >>
- fs []
-QED
-
-Theorem NUM_SUB_1_EQ:
- !(x y : int). x = y - 1 ==> 0 <= x ==> Num y = SUC (Num x)
-Proof
- rpt strip_tac >>
- (* Get rid of the SUC *)
- sg ‘SUC (Num x) = 1 + Num x’ >-(rw [ADD]) >> rw [] >>
- (* Massage a bit the goal *)
- qsuff_tac ‘Num y = Num (y − 1) + Num 1’ >- COOPER_TAC >>
- (* Apply the general theorem *)
- irule NUM_SUB_EQ >>
- COOPER_TAC
-QED
-
-(* TODO: remove *)
-Theorem NUM_SUB_1_EQ1:
- !i. 0 <= i - 1 ==> Num i = SUC (Num (i-1))
-Proof
- rpt strip_tac >>
- (* 0 <= i *)
- sg ‘0 <= i’ >- COOPER_TAC >>
- (* Get rid of the SUC *)
- sg ‘SUC (Num (i - 1)) = 1 + Num (i - 1)’ >-(rw [ADD]) >>
- rw [] >>
- (* Convert to integers*)
- irule INT_OF_NUM_INJ >>
- imp_res_tac (GSYM INT_OF_NUM) >>
- (* Associativity of & *)
- PURE_REWRITE_TAC [GSYM INT_ADD] >>
- fs []
-QED
-
-(* TODO:
- - list all the integer variables, and insert bounds in the assumptions
- - replace u32_min by 0?
- - i - 1
- - auto lookup of spec lemmas
-*)
-
-(* Add a list of theorems in the assumptions - TODO: move *)
-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
-
-(* The map from integer type to bounds lemmas *)
-val integer_bounds_lemmas =
- Redblackmap.fromList String.compare
- [
- ("u32", u32_to_int_bounds),
- ("i32", i32_to_int_bounds)
- ]
-
-(* The map from integer type to conversion lemmas *)
-val integer_conversion_lemmas =
- Redblackmap.fromList String.compare
- [
- ("u32", int_to_u32_id),
- ("i32", int_to_i32_id)
- ]
-
-val integer_conversion_lemmas_list =
- map snd (Redblackmap.listItems integer_conversion_lemmas)
-
-(* Not sure how term nets work, nor how we are supposed to convert Term.term
- to mlibTerm.term.
-
- TODO: it seems we need to explore the term and convert everything to strings.
- *)
-fun term_to_mlib_term (t : term) : mlibTerm.term =
- mlibTerm.string_to_term (term_to_string t)
-
-(*
-(* The lhs of the conclusion of the integer conversion lemmas - we use this for
- pattern matching *)
-val integer_conversion_lhs_concls =
- let
- val thms = map snd (Redblackmap.listItems integer_conversion_lemmas);
- val concls = map (lhs o concl o UNDISCH_ALL o SPEC_ALL) thms;
- in concls end
-*)
-
-(*
-val integer_conversion_concls_net =
- let
- val maplets = map (fn x => fst (dest_eq x) |-> ()) integer_conversion_concls;
-
- val maplets = map (fn x => fst (mlibTerm.dest_eq x) |-> ()) integer_conversion_concls;
- val maplets = map (fn x => fst (mlibThm.dest_unit_eq x) |-> ()) integer_conversion_concls;
- val parameters = { fifo=false };
- in mlibTermnet.from_maplets parameters maplets end
-
-mlibTerm.string_to_term (term_to_string “u32_to_int (int_to_u32 n) = n”)
-term_to_quote
-
-SIMP_CONV
-mlibThm.dest_thm u32_to_int_bounds
-mlibThm.dest_unit u32_to_int_bounds
-*)
-
-(* The integer types *)
-val integer_types_names =
- Redblackset.fromList String.compare
- (map fst (Redblackmap.listItems integer_bounds_lemmas))
-
-val all_integer_bounds = [
- u32_max_def,
- i32_min_def,
- i32_max_def
-]
-
-(* Small utility: compute the set of assumptions in the context.
-
- We isolate this code in a utility in order to be able to improve it:
- for now we simply put all the assumptions in a set, but in the future
- we might want to split the assumptions which are conjunctions in order
- to be more precise.
- *)
-fun compute_asms_set ((asms,g) : goal) : term Redblackset.set =
- Redblackset.fromList Term.compare asms
-
-(* See {!assume_bounds_for_all_int_vars}.
-
- This tactic is in charge of adding assumptions for one variable.
- *)
-
-fun assume_bounds_for_int_var
- (asms_set: term Redblackset.set) (var : string) (ty : string) :
- tactic =
- let
- (* Lookup the lemma to apply *)
- val lemma = Redblackmap.find (integer_bounds_lemmas, ty);
- (* Instantiate the lemma *)
- val ty_t = mk_type (ty, []);
- val var_t = mk_var (var, ty_t);
- val lemma = SPEC var_t lemma;
- (* Split the theorem into a list of conjuncts.
-
- The bounds are typically a conjunction:
- {[
- ⊢ 0 ≤ u32_to_int x ∧ u32_to_int x ≤ u32_max: thm
- ]}
- *)
- val lemmas = CONJUNCTS lemma;
- (* Filter the conjuncts: some of them might already be in the context,
- we don't want to introduce them again, as it would pollute it.
- *)
- val lemmas = filter (fn lem => not (Redblackset.member (asms_set, concl lem))) lemmas;
- in
- (* Introduce the assumptions in the context *)
- ASSUME_TACL lemmas
- end
-
-(* Destruct if possible a term of the shape: [x y],
- where [x] is not a comb.
-
- Returns [(x, y)]
- *)
-fun dest_single_comb (t : term) : (term * term) option =
- case strip_comb t of
- (x, [y]) => SOME (x, y)
- | _ => NONE
-
-(** Destruct if possible a term of the shape: [x (y z)].
- Returns [(x, y, z)]
- *)
-fun dest_single_comb_twice (t : term) : (term * term * term) option =
- case dest_single_comb t of
- NONE => NONE
- | SOME (x, y) =>
- case dest_single_comb y of
- NONE => NONE
- | SOME (y, z) => SOME (x, y, z)
-
-(* A utility map to lookup integer conversion lemmas *)
-val integer_conversion_pat_map =
- let
- val thms = map snd (Redblackmap.listItems integer_conversion_lemmas);
- val tl = map (lhs o concl o UNDISCH_ALL o SPEC_ALL) thms;
- val tl = map (valOf o dest_single_comb_twice) tl;
- val tl = map (fn (x, y, _) => (x, y)) tl;
- val m = Redblackmap.fromList Term.compare tl
- in m end
-
-(* Introduce bound assumptions for all the machine integers in the context.
-
- Exemple:
- ========
- If there is “x : u32” in the input set, then we introduce:
- {[
- 0 <= u32_to_int x
- u32_to_int x <= u32_max
- ]}
- *)
-fun assume_bounds_for_all_int_vars (asms, g) =
- let
- (* Compute the set of integer variables in the context *)
- val vars = free_varsl (g :: asms);
- (* Compute the set of assumptions already present in the context *)
- val asms_set = compute_asms_set (asms, g);
- (* Filter the variables to keep only the ones with type machine integer,
- decompose the types at the same time *)
- fun decompose_var (v : term) : (string * string) =
- let
- val (v, ty) = dest_var v;
- val {Args=args, Thy=thy, Tyop=ty} = dest_thy_type ty;
- val _ = assert null args;
- val _ = assert (fn thy => thy = primitives_theory_name) thy;
- val _ = assert (fn ty => Redblackset.member (integer_types_names, ty)) ty;
- in (v, ty) end;
- val vars = mapfilter decompose_var vars;
- (* Add assumptions for one variable *)
- fun add_var_asm (v, ty) : tactic =
- assume_bounds_for_int_var asms_set v ty;
- (* Add assumptions for all the variables *)
- (* TODO: use MAP_EVERY *)
- fun add_vars_asm vl : tactic =
- case vl of
- [] => ALL_TAC
- | v :: vl =>
- add_var_asm v >> add_vars_asm vl;
- in
- add_vars_asm vars (asms, g)
- end
-
-(*
-dest_thy_type “:u32”
-val massage : tactic = assume_bounds_for_all_int_vars
-val vl = vars
-val (v::vl) = vl
-*)
-
-(*
-val (asms, g) = top_goal ()
-fun bounds_for_ints_in_list (vars : (string * hol_type) list) : tactic =
- foldl
- FAIL_TAC ""
-val var = "x"
-val ty = "u32"
-
-val asms_set = Redblackset.fromList Term.compare asms;
-
-val x = “1: int”
-val ty = "u32"
-
-val thm = lemma
-*)
-
-(* 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
-
-(* 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.
- *)
-fun inst_match_concl_in_terms (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;
- in
- (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 of the goal.
- *)
-fun apply_dep_rewrites_match_concl_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_concl_in_terms th (g :: asms);
- val thms = map thm_to_conj_implies thms;
- in
- (* Apply each theorem *)
- MAP_EVERY (prove_premise_then prove_premise then_tac) thms (asms, g)
- 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.
- *)
-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
- prove_premise_then prove_premise then_tac th
- end;
- in
- (* Apply each theorem *)
- MAP_EVERY apply_tac thms (asms, g)
- end
-
-(* See {!rewrite_all_int_conversion_ids}.
-
- Small utility which takes care of one rewriting.
-
- TODO: we actually don't use it. REMOVE?
- *)
-fun rewrite_int_conversion_id
- (asms_set: term Redblackset.set) (x : term) (ty : string) :
- tactic =
- let
- (* Lookup the theorem *)
- val lemma = Redblackmap.find (integer_conversion_lemmas, ty);
- (* Instantiate *)
- val lemma = SPEC x lemma;
- (* Rewrite the lemma. The lemma typically has the shape:
- ⊢ u32_min <= x /\ x <= u32_max ==> u32_to_int (int_to_u32 x) = x
-
- Make sure the lemma has the proper shape, attempt to prove the premise,
- then use the conclusion if it succeeds.
- *)
- val lemma = thm_to_conj_implies lemma;
- (* Retrieve the conclusion of the lemma - we do this to check if it is not
- already in the assumptions *)
- val c = concl (UNDISCH_ALL lemma);
- val already_in_asms = Redblackset.member (asms_set, c);
- (* Small utility: the tactic to prove the premise *)
- val prove_premise =
- (* We might need to unfold the bound definitions, in particular if the
- term is a constant (e.g., “3:int”) *)
- FULL_SIMP_TAC simpLib.empty_ss all_integer_bounds >>
- COOPER_TAC;
- (* Rewrite with a lemma, then assume it *)
- fun rewrite_then_assum (thm : thm) : tactic =
- FULL_SIMP_TAC simpLib.empty_ss [thm] >> assume_tac thm;
- in
- (* If the conclusion is not already in the assumptions, prove it, use
- it to rewrite the goal and add it in the assumptions, otherwise do nothing *)
- if already_in_asms then ALL_TAC
- else prove_premise_then prove_premise rewrite_then_assum lemma
- end
-
-(* Look for conversions from integers to machine integers and back.
- {[
- u32_to_int (int_to_u32 x)
- ]}
-
- Attempts to prove and apply equalities of the form:
- {[
- u32_to_int (int_to_u32 x) = x
- ]}
-
- **REMARK**: this function can fail, if it doesn't manage to prove the
- premises of the theorem to apply.
-
- TODO: update
- *)
-val rewrite_with_dep_int_lemmas : tactic =
- (* We're not trying to be smart: we just try to rewrite with each theorem at
- a time *)
- let
- val prove_premise = FULL_SIMP_TAC simpLib.empty_ss all_integer_bounds >> COOPER_TAC;
- val then_tac1 = (fn th => FULL_SIMP_TAC simpLib.empty_ss [th]);
- val rewr_tac1 = apply_dep_rewrites_match_concl_tac prove_premise then_tac1;
- val then_tac2 = (fn th => FULL_SIMP_TAC simpLib.empty_ss [th]);
- val rewr_tac2 = apply_dep_rewrites_match_first_premise_tac prove_premise then_tac2;
- in
- MAP_EVERY rewr_tac1 integer_conversion_lemmas_list >>
- MAP_EVERY rewr_tac2 [NUM_SUB_1_EQ]
- end
-
-(*
-apply_dep_rewrites_match_first_premise_tac prove_premise then_tac NUM_SUB_1_EQ
-
-sg ‘u32_to_int z = u32_to_int i − 1 /\ 0 ≤ u32_to_int z’ >- prove_premise
-
-prove_premise_then prove_premise
-
-val thm = thm_to_conj_implies (SPECL [“u32_to_int z”, “u32_to_int i”] NUM_SUB_1_EQ)
-
-val h = “u32_to_int z = u32_to_int i − 1 ∧ 0 ≤ u32_to_int z”
-*)
-
-(* Massage a bit the goal, for instance by introducing integer bounds in the
- assumptions.
-*)
-val massage : tactic =
- assume_bounds_for_all_int_vars >>
- rewrite_with_dep_int_lemmas
-
-(* Lexicographic order over pairs *)
-fun pair_compare (comp1 : 'a * 'a -> order) (comp2 : 'b * 'b -> order)
- ((p1, p2) : (('a * 'b) * ('a * 'b))) : order =
- let
- val (x1, y1) = p1;
- val (x2, y2) = p2;
- in
- case comp1 (x1, x2) of
- LESS => LESS
- | GREATER => GREATER
- | EQUAL => comp2 (y1, y2)
- end
-
-(* A constant name (theory, constant name) *)
-type const_name = string * string
-
-val const_name_compare = pair_compare String.compare String.compare
-
-(* The registered spec theorems, that {!progress} will automatically apply.
-
- The keys are the function names (it is a pair, because constant names
- are made of the theory name and the name of the constant itself).
-
- Also note that we can store several specs per definition (in practice, when
- looking up specs, we will try them all one by one, in a LIFO order).
-
- We store theorems where all the premises are in the goal, with implications
- (i.e.: [⊢ H0 ==> ... ==> Hn ==> H], not [H0, ..., Hn ⊢ H]).
-
- We do this because, when doing proofs by induction, {!progress} might have to
- handle *unregistered* theorems coming the current goal assumptions and of the shape
- (the conclusion of the theorem is an assumption, and we want to ignore this assumption):
- {[
- [∀i. u32_to_int i < &LENGTH (list_t_v ls) ⇒
- case nth ls i of
- Return x => ...
- | ... => ...]
- ⊢ ∀i. u32_to_int i < &LENGTH (list_t_v ls) ⇒
- case nth ls i of
- Return x => ...
- | ... => ...
- ]}
- *)
-val reg_spec_thms: (const_name, thm) Redblackmap.dict ref =
- ref (Redblackmap.mkDict const_name_compare)
-
-(* Retrieve the specified application in a spec theorem.
-
- A spec theorem for a function [f] typically has the shape:
- {[
- !x0 ... xn.
- H0 ==> ... Hm ==>
- (exists ...
- (exists ... . f y0 ... yp = ... /\ ...) \/
- (exists ... . f y0 ... yp = ... /\ ...) \/
- ...
- ]}
-
- Or:
- {[
- !x0 ... xn.
- H0 ==> ... Hm ==>
- case f y0 ... yp of
- ... => ...
- | ... => ...
- ]}
-
- We return: [f y0 ... yp]
-*)
-fun get_spec_app (t : term) : term =
- let
- (* Remove the universally quantified variables, the premises and
- the existentially quantified variables *)
- val t = (snd o strip_exists o snd o strip_imp o snd o strip_forall) t;
- (* Remove the exists, take the first disjunct *)
- val t = (hd o strip_disj o snd o strip_exists) t;
- (* Split the conjunctions and take the first conjunct *)
- val t = (hd o strip_conj) t;
- (* Remove the case if there is, otherwise destruct the equality *)
- val t =
- if TypeBase.is_case t then let val (_, t, _) = TypeBase.dest_case t in t end
- else (fst o dest_eq) t;
- in t end
-
-(* Given a function call [f y0 ... yn] return the name of the function *)
-fun get_fun_name_from_app (t : term) : const_name =
- let
- val f = (fst o strip_comb) t;
- val {Name=name, Thy=thy, Ty=_} = dest_thy_const f;
- val cn = (thy, name);
- in cn end
-
-(* Register a spec theorem in the spec database.
-
- For the shape of spec theorems, see {!get_spec_thm_app}.
- *)
-fun register_spec_thm (th: thm) : unit =
- let
- (* Transform the theroem a bit before storing it *)
- val th = SPEC_ALL th;
- (* Retrieve the app ([f x0 ... xn]) *)
- val f = get_spec_app (concl th);
- (* Retrieve the function name *)
- val cn = get_fun_name_from_app f;
- in
- (* Store *)
- reg_spec_thms := Redblackmap.insert (!reg_spec_thms, cn, th)
- end
-
-(* TODO: I32_SUB_EQ *)
-val _ = app register_spec_thm [U32_ADD_EQ, U32_SUB_EQ, I32_ADD_EQ]
-
-(*
-app register_spec_thm [U32_ADD_EQ, U32_SUB_EQ, I32_ADD_EQ]
-Redblackmap.listItems (!reg_spec_thms)
-*)
-
-(*
-(* TODO: remove? *)
-datatype monadic_app_kind =
- Call | Bind | Case
-*)
-
-(* Repeatedly destruct cases and return the last scrutinee we get *)
-fun strip_all_cases_get_scrutinee (t : term) : term =
- if TypeBase.is_case t
- then (strip_all_cases_get_scrutinee o fst o TypeBase.strip_case) t
- else t
-
-(*
-TypeBase.dest_case “case ls of [] => T | _ => F”
-TypeBase.strip_case “case ls of [] => T | _ => F”
-TypeBase.strip_case “case (if b then [] else [0, 1]) of [] => T | _ => F”
-TypeBase.strip_case “3”
-TypeBase.dest_case “3”
-
-strip_all_cases_get_scrutinee “case ls of [] => T | _ => F”
-strip_all_cases_get_scrutinee “case (if b then [] else [0, 1]) of [] => T | _ => F”
-strip_all_cases_get_scrutinee “3”
-*)
-
-
-(* Provided the goal contains a call to a monadic function, return this function call.
-
- The goal should be of the shape:
- 1.
- {[
- case (* potentially expanded function body *) of
- ... => ...
- | ... => ...
- ]}
-
- 2. Or:
- {[
- exists ... .
- ... (* potentially expanded function body *) = Return ... /\
- ... (* Various properties *)
- ]}
-
- 3. Or a disjunction of cases like the one above, below existential binders
- (actually: note sure this last case exists in practice):
- {[
- exists ... .
- (exists ... . (* body *) = Return ... /\ ...) \/
- ...
- ]}
-
- The function body should be of the shape:
- {[
- x <- f y0 ... yn;
- ...
- ]}
-
- Or (typically if we expanded the monadic binds):
- {[
- case f y0 ... yn of
- ...
- ]}
-
- Or simply (typically if we reached the end of the function we're analyzing):
- {[
- f y0 ... yn
- ]}
-
- For all the above cases we would return [f y0 ... yn].
- *)
-fun get_monadic_app_call (t : term) : term =
- (* We do something slightly imprecise but hopefully general and robut *)
- let
- (* Case 3.: strip the existential binders, and take the first disjuntion *)
- val t = (hd o strip_disj o snd o strip_exists) t;
- (* Case 2.: strip the existential binders, and take the first conjunction *)
- val t = (hd o strip_conj o snd o strip_exists) t;
- (* If it is an equality, take the lhs *)
- val t = if is_eq t then lhs t else t;
- (* Expand the binders to transform them to cases *)
- val t =
- (rhs o concl) (REWRITE_CONV [st_ex_bind_def] t)
- handle UNCHANGED => t;
- (* Strip all the cases *)
- val t = strip_all_cases_get_scrutinee t;
- in t end
-
-(* Use the given theorem to progress by one step (we use this when
- analyzing a function body: this goes forward by one call to a monadic function).
-
- We transform the goal by:
- - pushing the theorem premises to a subgoal
- - adding the theorem conclusion in the assumptions in another goal, and
- getting rid of the monadic call
-
- Then [then_tac] receives as paramter the monadic call on which we applied
- the lemma. This can be useful, for instance, to make a case disjunction.
-
- This function is the most primitive of the [progress...] functions.
- *)
-fun pure_progress_with (premise_tac : tactic)
- (then_tac : term -> thm_tactic) (th : thm) : tactic =
- fn (asms,g) =>
- let
- (* Remove all the universally quantified variables from the theorem *)
- val th = SPEC_ALL th;
- (* Retrieve the monadic call from the goal *)
- val fgoal = get_monadic_app_call g;
- (* Retrieve the app call from the theroem *)
- val gth = get_spec_app (concl th);
- (* Match and instantiate *)
- val (var_s, ty_s) = match_term gth fgoal;
- (* Instantiate the theorem *)
- val th = INST var_s (INST_TYPE ty_s th);
- (* Retrieve the premises of the theorem *)
- val th = PURE_REWRITE_RULE [GSYM satTheory.AND_IMP] th;
- in
- (* Apply the theorem *)
- sg_premise_then premise_tac (then_tac fgoal) th (asms, g)
- end
-
-(*
-val (asms, g) = top_goal ()
-val t = g
-
-val th = U32_SUB_EQ
-
-val premise_tac = massage >> TRY COOPER_TAC
-fun then_tac fgoal =
- fn thm => ASSUME_TAC thm >> Cases_on ‘^fgoal’ >>
- rw [] >> fs [st_ex_bind_def] >> massage >> fs []
-
-pure_progress_with premise_tac then_tac th
-*)
-
-fun progress_with (th : thm) : tactic =
- let
- val premise_tac = massage >> fs [] >> rw [] >> TRY COOPER_TAC;
- fun then_tac fgoal thm =
- ASSUME_TAC thm >> Cases_on ‘^fgoal’ >>
- rw [] >> fs [st_ex_bind_def] >> massage >> fs [];
- in
- pure_progress_with premise_tac then_tac th
- end
-
-(*
-progress_with U32_SUB_EQ
-*)
-
-(* This function lookups the theorem to use to make progress *)
-val progress : tactic =
- fn (asms, g) =>
- let
- (* Retrieve the monadic call from the goal *)
- val fgoal = get_monadic_app_call g;
- val fname = get_fun_name_from_app fgoal;
- (* Lookup the theorem: first look in the assumptions (we might want to
- use the inductive hypothesis for instance) *)
- fun asm_to_spec asm =
- let
- (* Fail if there are no universal quantifiers *)
- val _ =
- if is_forall asm then asm
- else assert is_forall ((snd o strip_imp) asm);
- val asm_fname = (get_fun_name_from_app o get_spec_app) asm;
- (* Fail if the name is not the one we're looking for *)
- val _ = assert (fn n => fname = n) asm_fname;
- in
- ASSUME asm
- end
- val asms_thl = mapfilter asm_to_spec asms;
- (* Lookup a spec in the database *)
- val thl =
- case Redblackmap.peek (!reg_spec_thms, fname) of
- NONE => asms_thl
- | SOME spec => spec :: asms_thl;
- val _ =
- if null thl then
- raise (failwith "progress: could not find a suitable theorem to apply")
- else ();
- in
- (* Attempt to use the theorems one by one *)
- MAP_FIRST progress_with thl (asms, g)
- end
-
-(*
-val (asms, g) = top_goal ()
-*)
-
-(* TODO: no exfalso tactic?? *)
-val EX_FALSO : tactic =
- SUBGOAL_THEN “F” (fn th => ASSUME_TAC th >> fs[])
-
-Theorem nth_lem:
- !(ls : 't list_t) (i : u32).
- u32_to_int i < int_of_num (LENGTH (list_t_v ls)) ==>
- case nth ls i of
- | Return x => x = EL (Num (u32_to_int i)) (list_t_v ls)
- | Fail _ => F
- | Loop => F
-Proof
- Induct_on ‘ls’ >> rw [list_t_v_def] >~ [‘ListNil’]
- >-(massage >> EX_FALSO >> COOPER_TAC) >>
- PURE_ONCE_REWRITE_TAC [nth_def] >> rw [] >>
- progress >> progress
-QED
-
-(* Example from the hashmap *)
-val _ = new_constant ("insert", “: u32 -> 't -> (u32 # 't) list_t -> (u32 # 't) list_t result”)
-val insert_def = new_axiom ("insert_def", “
- insert (key : u32) (value : 't) (ls : (u32 # 't) list_t) : (u32 # 't) list_t result =
- case ls of
- | ListCons (ckey, cvalue) tl =>
- if ckey = key
- then Return (ListCons (ckey, value) tl)
- else
- do
- tl0 <- insert key value tl;
- Return (ListCons (ckey, cvalue) tl0)
- od
- | ListNil => Return (ListCons (key, value) ListNil)
- ”)
-
-(* Property that keys are pairwise distinct *)
-val distinct_keys_def = Define ‘
- distinct_keys (ls : (u32 # 't) list) =
- !i j.
- i < LENGTH ls ==>
- j < LENGTH ls ==>
- FST (EL i ls) = FST (EL j ls) ==>
- i = j
-’
-
-val lookup_raw_def = Define ‘
- lookup_raw key [] = NONE /\
- lookup_raw key ((k, v) :: ls) =
- if k = key then SOME v else lookup_raw key ls
-’
-
-val lookup_def = Define ‘
- lookup key ls = lookup_raw key (list_t_v ls)
-’
-
-Theorem insert_lem:
- !ls key value.
- (* The keys are pairwise distinct *)
- distinct_keys (list_t_v ls) ==>
- case insert key value ls of
- | Return ls1 =>
- (* We updated the binding *)
- lookup key ls1 = SOME value /\
- (* The other bindings are left unchanged *)
- (!k. k <> key ==> lookup k ls = lookup k ls1)
- | Fail _ => F
- | Loop => F
-Proof
- Induct_on ‘ls’ >> rw [list_t_v_def] >~ [‘ListNil’] >>
- PURE_ONCE_REWRITE_TAC [insert_def] >> rw []
- >- (rw [lookup_def, lookup_raw_def, list_t_v_def])
- >- (rw [lookup_def, lookup_raw_def, list_t_v_def]) >>
- CASE_TAC >> rw []
- >- (rw [lookup_def, lookup_raw_def, list_t_v_def])
- >- (rw [lookup_def, lookup_raw_def, list_t_v_def]) >>
- progress
- >- (
- fs [distinct_keys_def] >>
- rpt strip_tac >>
- first_assum (qspecl_then [‘SUC i’, ‘SUC j’] ASSUME_TAC) >>
- fs []
- (* Alternative: *)
- (*
- PURE_ONCE_REWRITE_TAC [GSYM prim_recTheory.INV_SUC_EQ] >>
- first_assum irule >> fs []
- *)) >>
- fs [lookup_def, lookup_raw_def, list_t_v_def]
-QED
-
-(***
- * Example of how to get rid of the fuel in practice
- *)
-val nth_fuel_def = Define ‘
- nth_fuel (n : num) (ls : 't list_t) (i : u32) : 't result =
- case n of
- | 0 => Loop
- | SUC n =>
- do case ls of
- | ListCons x tl =>
- if u32_to_int i = (0:int)
- then Return x
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- nth_fuel n tl i0
- od
- | ListNil =>
- Fail Failure
- od
- ’
-
-val is_loop_def = Define ‘is_loop r = case r of Loop => T | _ => F’
-
-val nth_fuel_P_def = Define ‘
- nth_fuel_P ls i n = ~is_loop (nth_fuel n ls i)
-’
-
-(* TODO: this is not the theorem we want: we want the one below *)
-Theorem nth_fuel_mono:
- !n m ls i.
- n <= m ==>
- if is_loop (nth_fuel n ls i) then T
- else nth_fuel n ls i = nth_fuel m ls i
-Proof
- Induct_on ‘n’ >- (
- rpt gen_tac >>
- DISCH_TAC >>
- PURE_ONCE_REWRITE_TAC [nth_fuel_def] >>
- rw[is_loop_def]
- ) >>
- (* Interesting case *)
- rpt gen_tac >>
- DISCH_TAC >>
- CASE_TAC >>
- Cases_on ‘m’ >- (
- (* Contradiction: SUC n < 0 *)
- sg ‘SUC n = 0’ >- decide_tac >>
- fs [is_loop_def]
- ) >>
- fs [is_loop_def] >>
- pop_assum mp_tac >>
- PURE_ONCE_REWRITE_TAC [nth_fuel_def] >>
- fs [] >>
- DISCH_TAC >>
- (* We just have to explore all the paths: we can have dedicated tactics for that
- (we need to do case analysis) *)
- Cases_on ‘ls’ >> fs [] >>
- Cases_on ‘u32_to_int (i :u32) = (0 :int)’ >> fs [] >>
- fs [st_ex_bind_def] >>
- Cases_on ‘u32_sub (i :u32) (int_to_u32 (1 :int))’ >> fs [] >>
- (* Apply the induction hypothesis *)
- first_x_assum (qspecl_then [‘n'’, ‘l’, ‘a’] assume_tac) >>
- first_x_assum imp_res_tac >>
- pop_assum mp_tac >>
- CASE_TAC
-QED
-
-Theorem nth_fuel_P_mono:
- !n m ls i.
- n <= m ==>
- nth_fuel_P ls i n ==>
- nth_fuel n ls i = nth_fuel m ls i
-Proof
- rpt gen_tac >> rpt DISCH_TAC >>
- fs [nth_fuel_P_def] >>
- imp_res_tac nth_fuel_mono >>
- pop_assum (qspecl_then [‘ls’, ‘i’] assume_tac) >>
- pop_assum mp_tac >> CASE_TAC >> fs []
-QED
-
-(*Theorem nth_fuel_least_fail_mono:
- !n ls i.
- n < $LEAST (nth_fuel_P ls i) ==>
- nth_fuel n ls i = Loop
-Proof
- rpt gen_tac >>
- disch_tac >>
- imp_res_tac whileTheory.LESS_LEAST >>
- fs [nth_fuel_P_def, is_loop_def] >>
- pop_assum mp_tac >>
- CASE_TAC
-QED*)
-
-Theorem nth_fuel_least_success_mono:
- !n ls i.
- $LEAST (nth_fuel_P ls i) <= n ==>
- nth_fuel n ls i = nth_fuel ($LEAST (nth_fuel_P ls i)) ls i
-Proof
- rpt gen_tac >>
- disch_tac >>
- (* Case disjunction on whether there exists a fuel such that it terminates *)
- Cases_on ‘?m. nth_fuel_P ls i m’ >- (
- (* Terminates *)
- irule EQ_SYM >>
- irule nth_fuel_P_mono >> fs [] >>
- (* Prove that calling with the least upper bound of fuel succeeds *)
- qspec_then ‘nth_fuel_P (ls :α list_t) (i :u32)’ imp_res_tac whileTheory.LEAST_EXISTS_IMP
- ) >>
- (* Doesn't terminate *)
- fs [] >>
- sg ‘~(nth_fuel_P ls i n)’ >- fs [] >>
- sg ‘~(nth_fuel_P ls i ($LEAST (nth_fuel_P ls i)))’ >- fs [] >>
- fs [nth_fuel_P_def, is_loop_def] >>
- pop_assum mp_tac >> CASE_TAC >>
- pop_assum mp_tac >>
- pop_assum mp_tac >> CASE_TAC
-QED
-
-val nth_def_raw = Define ‘
- nth ls i =
- if (?n. nth_fuel_P ls i n) then nth_fuel ($LEAST (nth_fuel_P ls i)) ls i
- else Loop
-’
-
-(* This makes the proofs easier, in that it helps us control the context *)
-val nth_expand_def = Define ‘
- nth_expand nth ls i =
- case ls of
- | ListCons x tl =>
- if u32_to_int i = (0:int)
- then Return x
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- nth tl i0
- od
- | ListNil =>
- Fail Failure
-’
-
-(* Prove the important theorems: termination case *)
-Theorem nth_def_terminates:
- !ls i.
- (?n. nth_fuel_P ls i n) ==>
- nth ls i =
- nth_expand nth ls i
-Proof
- rpt strip_tac >>
- fs [nth_expand_def] >>
- PURE_ONCE_REWRITE_TAC [nth_def_raw] >>
- (* Prove that the least upper bound is <= n *)
- sg ‘$LEAST (nth_fuel_P ls i) <= n’ >-(
- qspec_then ‘nth_fuel_P (ls :α list_t) (i :u32)’ imp_res_tac whileTheory.LEAST_EXISTS_IMP >>
- spose_not_then assume_tac >> fs []
- ) >>
- (* Use the monotonicity theorem - TODO: ? *)
- imp_res_tac nth_fuel_least_success_mono >>
- (* Rewrite only on the left - TODO: easy way ?? *)
- qspecl_then [‘$LEAST (nth_fuel_P ls i)’, ‘ls’, ‘i’] assume_tac nth_fuel_def >>
- (* TODO: how to discard assumptions?? *)
- fs [] >> pop_assum (fn _ => fs []) >>
- (* Cases on the least upper bound *)
- Cases_on ‘$LEAST (nth_fuel_P ls i)’ >> rw [] >- (
- (* The bound is equal to 0: contradiction *)
- sg ‘nth_fuel 0 ls i = Loop’ >- (PURE_ONCE_REWRITE_TAC [nth_fuel_def] >> rw []) >>
- fs [nth_fuel_P_def, is_loop_def]
- ) >>
- (* Bound not equal to 0 *)
- fs [nth_fuel_P_def, is_loop_def] >>
- (* Explore all the paths *)
- fs [st_ex_bind_def] >>
- Cases_on ‘ls’ >> rw [] >> fs [] >>
- Cases_on ‘u32_sub i (int_to_u32 1)’ >> rw [] >> fs [] >>
- (* Recursive call: use monotonicity - we have an assumption which eliminates the Loop case *)
- Cases_on ‘nth_fuel n' l a’ >> rw [] >> fs [] >>
- (sg ‘nth_fuel_P l a n'’ >- fs [nth_fuel_P_def, is_loop_def]) >>
- (sg ‘$LEAST (nth_fuel_P l a) <= n'’ >-(
- qspec_then ‘nth_fuel_P l a’ imp_res_tac whileTheory.LEAST_EXISTS_IMP >>
- spose_not_then assume_tac >> fs [])) >>
- imp_res_tac nth_fuel_least_success_mono >> fs []
-QED
-
-(* Prove the important theorems: divergence case *)
-Theorem nth_def_loop:
- !ls i.
- (!n. ~nth_fuel_P ls i n) ==>
- nth ls i =
- nth_expand nth ls i
-Proof
- rpt gen_tac >>
- PURE_ONCE_REWRITE_TAC [nth_def_raw] >>
- strip_tac >> rw[] >>
- (* Non-terminating case *)
- sg ‘∀n. ¬nth_fuel_P ls i (SUC n)’ >- rw [] >>
- fs [nth_fuel_P_def, is_loop_def] >>
- pop_assum mp_tac >>
- PURE_ONCE_REWRITE_TAC [nth_fuel_def] >>
- rw [] >>
- fs [nth_expand_def] >>
- (* Evaluate all the paths *)
- fs [st_ex_bind_def] >>
- Cases_on ‘ls’ >> rw [] >> fs [] >>
- Cases_on ‘u32_sub i (int_to_u32 1)’ >> rw [] >> fs [] >>
- (* Use the definition of nth *)
- rw [nth_def_raw] >>
- first_x_assum (qspec_then ‘$LEAST (nth_fuel_P l a)’ assume_tac) >>
- Cases_on ‘nth_fuel ($LEAST (nth_fuel_P l a)) l a’ >> fs []
-QED
-
-(* The final theorem *)
-Theorem nth_def:
- !ls i.
- nth ls i =
- case ls of
- | ListCons x tl =>
- if u32_to_int i = (0:int)
- then Return x
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- nth tl i0
- od
- | ListNil =>
- Fail Failure
-Proof
- rpt strip_tac >>
- Cases_on ‘?n. nth_fuel_P ls i n’ >-(
- assume_tac nth_def_terminates >>
- fs [nth_expand_def] >>
- pop_assum irule >>
- metis_tac []) >>
- fs [] >> imp_res_tac nth_def_loop >> fs [nth_expand_def]
-QED
-
-(*
-
-Je viens de finir ma petite expérimentation avec le fuel : ça marche bien. Par exemple, si je pose les définitions suivantes :
-Datatype:
- result = Return 'a | Fail error | Loop
-End
-
-(* Omitting some definitions like the bind *)
-
-val _ = Define ‘
- nth_fuel (n : num) (ls : 't list_t) (i : u32) : 't result =
- case n of
- | 0 => Loop
- | SUC n =>
- do case ls of
- | ListCons x tl =>
- if u32_to_int i = (0:int)
- then Return x
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- nth_fuel n tl i0
- od
- | ListNil =>
- Fail Failure
- od
- ’
-
-val _ = Define 'is_loop r = case r of Loop => T | _ => F'
-
-val _ = Define 'nth_fuel_P ls i n = ~is_loop (nth_fuel n ls i)'
-
-(* $LEAST returns the least upper bound for a predicate (if it exists - otherwise it returns an arbitrary number) *)
-val _ = Define ‘
- nth ls i =
- if (?n. nth_fuel_P ls i n) then nth_fuel ($LEAST (nth_fuel_P ls i)) ls i
- else Loop
-’
-J'arrive à montrer (c'est un chouïa technique) :
-Theorem nth_def:
- !ls i.
- nth ls i =
- case ls of
- | ListCons x tl =>
- if u32_to_int i = (0:int)
- then Return x
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- nth tl i0
- od
- | ListNil =>
- Fail Failure
-
-*)
-
-val _ = export_theory ()
diff --git a/backends/hol4/testTheory.sig b/backends/hol4/testTheory.sig
deleted file mode 100644
index 21b74a39..00000000
--- a/backends/hol4/testTheory.sig
+++ /dev/null
@@ -1,834 +0,0 @@
-signature testTheory =
-sig
- type thm = Thm.thm
-
- (* Axioms *)
- val VEC_TO_LIST_BOUNDS : thm
- val i32_to_int_bounds : thm
- val insert_def : thm
- val int_to_i32_id : thm
- val int_to_u32_id : thm
- val u32_to_int_bounds : thm
-
- (* Definitions *)
- val distinct_keys_def : thm
- val error_BIJ : thm
- val error_CASE : thm
- val error_TY_DEF : thm
- val error_size_def : thm
- val i32_add_def : thm
- val i32_max_def : thm
- val i32_min_def : thm
- val int1_def : thm
- val int2_def : thm
- val is_loop_def : thm
- val is_true_def : thm
- val list_t_TY_DEF : thm
- val list_t_case_def : thm
- val list_t_size_def : thm
- val list_t_v_def : thm
- val lookup_def : thm
- val mk_i32_def : thm
- val mk_u32_def : thm
- val nth_expand_def : thm
- val nth_fuel_P_def : thm
- val result_TY_DEF : thm
- val result_case_def : thm
- val result_size_def : thm
- val st_ex_bind_def : thm
- val st_ex_return_def : thm
- val test1_def : thm
- val test2_TY_DEF : thm
- val test2_case_def : thm
- val test2_size_def : thm
- val test_TY_DEF : thm
- val test_case_def : thm
- val test_monad2_def : thm
- val test_monad3_def : thm
- val test_monad_def : thm
- val test_size_def : thm
- val u32_add_def : thm
- val u32_max_def : thm
- val u32_sub_def : thm
- val usize_max_def : thm
- val vec_len_def : thm
-
- (* Theorems *)
- val I32_ADD_EQ : thm
- val INT_OF_NUM_INJ : thm
- val INT_THM1 : thm
- val INT_THM2 : thm
- val MK_I32_SUCCESS : thm
- val MK_U32_SUCCESS : thm
- val NAT_THM1 : thm
- val NAT_THM2 : thm
- val NUM_SUB_1_EQ : thm
- val NUM_SUB_1_EQ1 : thm
- val NUM_SUB_EQ : thm
- val U32_ADD_EQ : thm
- val U32_SUB_EQ : thm
- val VEC_TO_LIST_INT_BOUNDS : thm
- val datatype_error : thm
- val datatype_list_t : thm
- val datatype_result : thm
- val datatype_test : thm
- val datatype_test2 : thm
- val error2num_11 : thm
- val error2num_ONTO : thm
- val error2num_num2error : thm
- val error2num_thm : thm
- val error_Axiom : thm
- val error_EQ_error : thm
- val error_case_cong : thm
- val error_case_def : thm
- val error_case_eq : thm
- val error_induction : thm
- val error_nchotomy : thm
- val insert_lem : thm
- val list_nth_mut_loop_loop_fwd_def : thm
- val list_nth_mut_loop_loop_fwd_ind : thm
- val list_t_11 : thm
- val list_t_Axiom : thm
- val list_t_case_cong : thm
- val list_t_case_eq : thm
- val list_t_distinct : thm
- val list_t_induction : thm
- val list_t_nchotomy : thm
- val lookup_raw_def : thm
- val lookup_raw_ind : thm
- val nth_def : thm
- val nth_def_loop : thm
- val nth_def_terminates : thm
- val nth_fuel_P_mono : thm
- val nth_fuel_def : thm
- val nth_fuel_ind : thm
- val nth_fuel_least_success_mono : thm
- val nth_fuel_mono : thm
- val num2error_11 : thm
- val num2error_ONTO : thm
- val num2error_error2num : thm
- val num2error_thm : thm
- val result_11 : thm
- val result_Axiom : thm
- val result_case_cong : thm
- val result_case_eq : thm
- val result_distinct : thm
- val result_induction : thm
- val result_nchotomy : thm
- val test2_11 : thm
- val test2_Axiom : thm
- val test2_case_cong : thm
- val test2_case_eq : thm
- val test2_distinct : thm
- val test2_induction : thm
- val test2_nchotomy : thm
- val test_11 : thm
- val test_Axiom : thm
- val test_case_cong : thm
- val test_case_eq : thm
- val test_distinct : thm
- val test_induction : thm
- val test_nchotomy : thm
-
- val test_grammars : type_grammar.grammar * term_grammar.grammar
-(*
- [Omega] Parent theory of "test"
-
- [int_arith] Parent theory of "test"
-
- [words] Parent theory of "test"
-
- [insert_def] Axiom
-
- [oracles: ] [axioms: insert_def] []
- ⊢ insert key value ls =
- case ls of
- ListCons (ckey,cvalue) tl =>
- if ckey = key then Return (ListCons (ckey,value) tl)
- else
- do
- tl0 <- insert key value tl;
- Return (ListCons (ckey,cvalue) tl0)
- od
- | ListNil => Return (ListCons (key,value) ListNil)
-
- [u32_to_int_bounds] Axiom
-
- [oracles: ] [axioms: u32_to_int_bounds] []
- ⊢ ∀n. 0 ≤ u32_to_int n ∧ u32_to_int n ≤ u32_max
-
- [i32_to_int_bounds] Axiom
-
- [oracles: ] [axioms: i32_to_int_bounds] []
- ⊢ ∀n. i32_min ≤ i32_to_int n ∧ i32_to_int n ≤ i32_max
-
- [int_to_u32_id] Axiom
-
- [oracles: ] [axioms: int_to_u32_id] []
- ⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ u32_to_int (int_to_u32 n) = n
-
- [int_to_i32_id] Axiom
-
- [oracles: ] [axioms: int_to_i32_id] []
- ⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ i32_to_int (int_to_i32 n) = n
-
- [VEC_TO_LIST_BOUNDS] Axiom
-
- [oracles: ] [axioms: VEC_TO_LIST_BOUNDS] []
- ⊢ ∀v. (let l = LENGTH (vec_to_list v) in 0 ≤ l ∧ l ≤ 4294967295)
-
- [distinct_keys_def] Definition
-
- ⊢ ∀ls.
- distinct_keys ls ⇔
- ∀i j.
- i < LENGTH ls ⇒
- j < LENGTH ls ⇒
- FST (EL i ls) = FST (EL j ls) ⇒
- i = j
-
- [error_BIJ] Definition
-
- ⊢ (∀a. num2error (error2num a) = a) ∧
- ∀r. (λn. n < 1) r ⇔ error2num (num2error r) = r
-
- [error_CASE] Definition
-
- ⊢ ∀x v0. (case x of Failure => v0) = (λm. v0) (error2num x)
-
- [error_TY_DEF] Definition
-
- ⊢ ∃rep. TYPE_DEFINITION (λn. n < 1) rep
-
- [error_size_def] Definition
-
- ⊢ ∀x. error_size x = 0
-
- [i32_add_def] Definition
-
- ⊢ ∀x y. i32_add x y = mk_i32 (i32_to_int x + i32_to_int y)
-
- [i32_max_def] Definition
-
- ⊢ i32_max = 2147483647
-
- [i32_min_def] Definition
-
- ⊢ i32_min = -2147483648
-
- [int1_def] Definition
-
- ⊢ int1 = 32
-
- [int2_def] Definition
-
- ⊢ int2 = -32
-
- [is_loop_def] Definition
-
- ⊢ ∀r. is_loop r ⇔ case r of Return v2 => F | Fail v3 => F | Loop => T
-
- [is_true_def] Definition
-
- ⊢ ∀x. is_true x = if x then Return () else Fail Failure
-
- [list_t_TY_DEF] Definition
-
- ⊢ ∃rep.
- TYPE_DEFINITION
- (λa0'.
- ∀ $var$('list_t').
- (∀a0'.
- (∃a0 a1.
- a0' =
- (λa0 a1.
- ind_type$CONSTR 0 a0
- (ind_type$FCONS a1 (λn. ind_type$BOTTOM)))
- a0 a1 ∧ $var$('list_t') a1) ∨
- a0' =
- ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ⇒
- $var$('list_t') a0') ⇒
- $var$('list_t') a0') rep
-
- [list_t_case_def] Definition
-
- ⊢ (∀a0 a1 f v. list_t_CASE (ListCons a0 a1) f v = f a0 a1) ∧
- ∀f v. list_t_CASE ListNil f v = v
-
- [list_t_size_def] Definition
-
- ⊢ (∀f a0 a1.
- list_t_size f (ListCons a0 a1) = 1 + (f a0 + list_t_size f a1)) ∧
- ∀f. list_t_size f ListNil = 0
-
- [list_t_v_def] Definition
-
- ⊢ list_t_v ListNil = [] ∧
- ∀x tl. list_t_v (ListCons x tl) = x::list_t_v tl
-
- [lookup_def] Definition
-
- ⊢ ∀key ls. lookup key ls = lookup_raw key (list_t_v ls)
-
- [mk_i32_def] Definition
-
- ⊢ ∀n. mk_i32 n =
- if i32_min ≤ n ∧ n ≤ i32_max then Return (int_to_i32 n)
- else Fail Failure
-
- [mk_u32_def] Definition
-
- ⊢ ∀n. mk_u32 n =
- if 0 ≤ n ∧ n ≤ u32_max then Return (int_to_u32 n)
- else Fail Failure
-
- [nth_expand_def] Definition
-
- ⊢ ∀nth ls i.
- nth_expand nth ls i =
- case ls of
- ListCons x tl =>
- if u32_to_int i = 0 then Return x
- else do i0 <- u32_sub i (int_to_u32 1); nth tl i0 od
- | ListNil => Fail Failure
-
- [nth_fuel_P_def] Definition
-
- ⊢ ∀ls i n. nth_fuel_P ls i n ⇔ ¬is_loop (nth_fuel n ls i)
-
- [result_TY_DEF] Definition
-
- ⊢ ∃rep.
- TYPE_DEFINITION
- (λa0.
- ∀ $var$('result').
- (∀a0.
- (∃a. a0 =
- (λa.
- ind_type$CONSTR 0 (a,ARB)
- (λn. ind_type$BOTTOM)) a) ∨
- (∃a. a0 =
- (λa.
- ind_type$CONSTR (SUC 0) (ARB,a)
- (λn. ind_type$BOTTOM)) a) ∨
- a0 =
- ind_type$CONSTR (SUC (SUC 0)) (ARB,ARB)
- (λn. ind_type$BOTTOM) ⇒
- $var$('result') a0) ⇒
- $var$('result') a0) rep
-
- [result_case_def] Definition
-
- ⊢ (∀a f f1 v. result_CASE (Return a) f f1 v = f a) ∧
- (∀a f f1 v. result_CASE (Fail a) f f1 v = f1 a) ∧
- ∀f f1 v. result_CASE Loop f f1 v = v
-
- [result_size_def] Definition
-
- ⊢ (∀f a. result_size f (Return a) = 1 + f a) ∧
- (∀f a. result_size f (Fail a) = 1 + error_size a) ∧
- ∀f. result_size f Loop = 0
-
- [st_ex_bind_def] Definition
-
- ⊢ ∀x f.
- monad_bind x f =
- case x of Return y => f y | Fail e => Fail e | Loop => Loop
-
- [st_ex_return_def] Definition
-
- ⊢ ∀x. st_ex_return x = Return x
-
- [test1_def] Definition
-
- ⊢ ∀x. test1 x = Return x
-
- [test2_TY_DEF] Definition
-
- ⊢ ∃rep.
- TYPE_DEFINITION
- (λa0.
- ∀ $var$('test2').
- (∀a0.
- (∃a. a0 =
- (λa.
- ind_type$CONSTR 0 (a,ARB)
- (λn. ind_type$BOTTOM)) a) ∨
- (∃a. a0 =
- (λa.
- ind_type$CONSTR (SUC 0) (ARB,a)
- (λn. ind_type$BOTTOM)) a) ⇒
- $var$('test2') a0) ⇒
- $var$('test2') a0) rep
-
- [test2_case_def] Definition
-
- ⊢ (∀a f f1. test2_CASE (Variant1_2 a) f f1 = f a) ∧
- ∀a f f1. test2_CASE (Variant2_2 a) f f1 = f1 a
-
- [test2_size_def] Definition
-
- ⊢ (∀f f1 a. test2_size f f1 (Variant1_2 a) = 1 + f a) ∧
- ∀f f1 a. test2_size f f1 (Variant2_2 a) = 1 + f1 a
-
- [test_TY_DEF] Definition
-
- ⊢ ∃rep.
- TYPE_DEFINITION
- (λa0.
- ∀ $var$('test').
- (∀a0.
- (∃a. a0 =
- (λa.
- ind_type$CONSTR 0 (a,ARB)
- (λn. ind_type$BOTTOM)) a) ∨
- (∃a. a0 =
- (λa.
- ind_type$CONSTR (SUC 0) (ARB,a)
- (λn. ind_type$BOTTOM)) a) ⇒
- $var$('test') a0) ⇒
- $var$('test') a0) rep
-
- [test_case_def] Definition
-
- ⊢ (∀a f f1. test_CASE (Variant1 a) f f1 = f a) ∧
- ∀a f f1. test_CASE (Variant2 a) f f1 = f1 a
-
- [test_monad2_def] Definition
-
- ⊢ test_monad2 = do x <- Return T; Return x od
-
- [test_monad3_def] Definition
-
- ⊢ ∀x. test_monad3 x = monad_ignore_bind (is_true x) (Return x)
-
- [test_monad_def] Definition
-
- ⊢ ∀v. test_monad v = do x <- Return v; Return x od
-
- [test_size_def] Definition
-
- ⊢ (∀f f1 a. test_size f f1 (Variant1 a) = 1 + f1 a) ∧
- ∀f f1 a. test_size f f1 (Variant2 a) = 1 + f a
-
- [u32_add_def] Definition
-
- ⊢ ∀x y. u32_add x y = mk_u32 (u32_to_int x + u32_to_int y)
-
- [u32_max_def] Definition
-
- ⊢ u32_max = 4294967295
-
- [u32_sub_def] Definition
-
- ⊢ ∀x y. u32_sub x y = mk_u32 (u32_to_int x − u32_to_int y)
-
- [usize_max_def] Definition
-
- ⊢ usize_max = 4294967295
-
- [vec_len_def] Definition
-
- ⊢ ∀v. vec_len v = int_to_u32 (&LENGTH (vec_to_list v))
-
- [I32_ADD_EQ] Theorem
-
- [oracles: DISK_THM] [axioms: int_to_i32_id] []
- ⊢ ∀x y.
- i32_min ≤ i32_to_int x + i32_to_int y ⇒
- i32_to_int x + i32_to_int y ≤ i32_max ⇒
- ∃z. i32_add x y = Return z ∧
- i32_to_int z = i32_to_int x + i32_to_int y
-
- [INT_OF_NUM_INJ] Theorem
-
- ⊢ ∀n m. &n = &m ⇒ n = m
-
- [INT_THM1] Theorem
-
- ⊢ ∀x y. x > 0 ⇒ y > 0 ⇒ x + y > 0
-
- [INT_THM2] Theorem
-
- ⊢ ∀x. T
-
- [MK_I32_SUCCESS] Theorem
-
- ⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ mk_i32 n = Return (int_to_i32 n)
-
- [MK_U32_SUCCESS] Theorem
-
- ⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ mk_u32 n = Return (int_to_u32 n)
-
- [NAT_THM1] Theorem
-
- ⊢ ∀n. n < n + 1
-
- [NAT_THM2] Theorem
-
- ⊢ ∀n. n < n + 1
-
- [NUM_SUB_1_EQ] Theorem
-
- ⊢ ∀x y. x = y − 1 ⇒ 0 ≤ x ⇒ Num y = SUC (Num x)
-
- [NUM_SUB_1_EQ1] Theorem
-
- ⊢ ∀i. 0 ≤ i − 1 ⇒ Num i = SUC (Num (i − 1))
-
- [NUM_SUB_EQ] Theorem
-
- ⊢ ∀x y z. x = y − z ⇒ 0 ≤ x ⇒ 0 ≤ z ⇒ Num y = Num z + Num x
-
- [U32_ADD_EQ] Theorem
-
- [oracles: DISK_THM] [axioms: int_to_u32_id, u32_to_int_bounds] []
- ⊢ ∀x y.
- u32_to_int x + u32_to_int y ≤ u32_max ⇒
- ∃z. u32_add x y = Return z ∧
- u32_to_int z = u32_to_int x + u32_to_int y
-
- [U32_SUB_EQ] Theorem
-
- [oracles: DISK_THM] [axioms: int_to_u32_id, u32_to_int_bounds] []
- ⊢ ∀x y.
- 0 ≤ u32_to_int x − u32_to_int y ⇒
- ∃z. u32_sub x y = Return z ∧
- u32_to_int z = u32_to_int x − u32_to_int y
-
- [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)
-
- [datatype_error] Theorem
-
- ⊢ DATATYPE (error Failure)
-
- [datatype_list_t] Theorem
-
- ⊢ DATATYPE (list_t ListCons ListNil)
-
- [datatype_result] Theorem
-
- ⊢ DATATYPE (result Return Fail Loop)
-
- [datatype_test] Theorem
-
- ⊢ DATATYPE (test Variant1 Variant2)
-
- [datatype_test2] Theorem
-
- ⊢ DATATYPE (test2 Variant1_2 Variant2_2)
-
- [error2num_11] Theorem
-
- ⊢ ∀a a'. error2num a = error2num a' ⇔ a = a'
-
- [error2num_ONTO] Theorem
-
- ⊢ ∀r. r < 1 ⇔ ∃a. r = error2num a
-
- [error2num_num2error] Theorem
-
- ⊢ ∀r. r < 1 ⇔ error2num (num2error r) = r
-
- [error2num_thm] Theorem
-
- ⊢ error2num Failure = 0
-
- [error_Axiom] Theorem
-
- ⊢ ∀x0. ∃f. f Failure = x0
-
- [error_EQ_error] Theorem
-
- ⊢ ∀a a'. a = a' ⇔ error2num a = error2num a'
-
- [error_case_cong] Theorem
-
- ⊢ ∀M M' v0.
- M = M' ∧ (M' = Failure ⇒ v0 = v0') ⇒
- (case M of Failure => v0) = case M' of Failure => v0'
-
- [error_case_def] Theorem
-
- ⊢ ∀v0. (case Failure of Failure => v0) = v0
-
- [error_case_eq] Theorem
-
- ⊢ (case x of Failure => v0) = v ⇔ x = Failure ∧ v0 = v
-
- [error_induction] Theorem
-
- ⊢ ∀P. P Failure ⇒ ∀a. P a
-
- [error_nchotomy] Theorem
-
- ⊢ ∀a. a = Failure
-
- [insert_lem] Theorem
-
- [oracles: DISK_THM] [axioms: u32_to_int_bounds, insert_def] []
- ⊢ ∀ls key value.
- distinct_keys (list_t_v ls) ⇒
- case insert key value ls of
- Return ls1 =>
- lookup key ls1 = SOME value ∧
- ∀k. k ≠ key ⇒ lookup k ls = lookup k ls1
- | Fail v1 => F
- | Loop => F
-
- [list_nth_mut_loop_loop_fwd_def] Theorem
-
- ⊢ ∀ls i.
- list_nth_mut_loop_loop_fwd ls i =
- case ls of
- ListCons x tl =>
- if u32_to_int i = 0 then Return x
- else
- do
- i0 <- u32_sub i (int_to_u32 1);
- list_nth_mut_loop_loop_fwd tl i0
- od
- | ListNil => Fail Failure
-
- [list_nth_mut_loop_loop_fwd_ind] Theorem
-
- ⊢ ∀P. (∀ls i.
- (∀x tl i0. ls = ListCons x tl ∧ u32_to_int i ≠ 0 ⇒ P tl i0) ⇒
- P ls i) ⇒
- ∀v v1. P v v1
-
- [list_t_11] Theorem
-
- ⊢ ∀a0 a1 a0' a1'.
- ListCons a0 a1 = ListCons a0' a1' ⇔ a0 = a0' ∧ a1 = a1'
-
- [list_t_Axiom] Theorem
-
- ⊢ ∀f0 f1. ∃fn.
- (∀a0 a1. fn (ListCons a0 a1) = f0 a0 a1 (fn a1)) ∧
- fn ListNil = f1
-
- [list_t_case_cong] Theorem
-
- ⊢ ∀M M' f v.
- M = M' ∧ (∀a0 a1. M' = ListCons a0 a1 ⇒ f a0 a1 = f' a0 a1) ∧
- (M' = ListNil ⇒ v = v') ⇒
- list_t_CASE M f v = list_t_CASE M' f' v'
-
- [list_t_case_eq] Theorem
-
- ⊢ list_t_CASE x f v = v' ⇔
- (∃t l. x = ListCons t l ∧ f t l = v') ∨ x = ListNil ∧ v = v'
-
- [list_t_distinct] Theorem
-
- ⊢ ∀a1 a0. ListCons a0 a1 ≠ ListNil
-
- [list_t_induction] Theorem
-
- ⊢ ∀P. (∀l. P l ⇒ ∀t. P (ListCons t l)) ∧ P ListNil ⇒ ∀l. P l
-
- [list_t_nchotomy] Theorem
-
- ⊢ ∀ll. (∃t l. ll = ListCons t l) ∨ ll = ListNil
-
- [lookup_raw_def] Theorem
-
- ⊢ (∀key. lookup_raw key [] = NONE) ∧
- ∀v ls key k.
- lookup_raw key ((k,v)::ls) =
- if k = key then SOME v else lookup_raw key ls
-
- [lookup_raw_ind] Theorem
-
- ⊢ ∀P. (∀key. P key []) ∧
- (∀key k v ls. (k ≠ key ⇒ P key ls) ⇒ P key ((k,v)::ls)) ⇒
- ∀v v1. P v v1
-
- [nth_def] Theorem
-
- ⊢ ∀ls i.
- nth ls i =
- case ls of
- ListCons x tl =>
- if u32_to_int i = 0 then Return x
- else do i0 <- u32_sub i (int_to_u32 1); nth tl i0 od
- | ListNil => Fail Failure
-
- [nth_def_loop] Theorem
-
- ⊢ ∀ls i. (∀n. ¬nth_fuel_P ls i n) ⇒ nth ls i = nth_expand nth ls i
-
- [nth_def_terminates] Theorem
-
- ⊢ ∀ls i. (∃n. nth_fuel_P ls i n) ⇒ nth ls i = nth_expand nth ls i
-
- [nth_fuel_P_mono] Theorem
-
- ⊢ ∀n m ls i.
- n ≤ m ⇒ nth_fuel_P ls i n ⇒ nth_fuel n ls i = nth_fuel m ls i
-
- [nth_fuel_def] Theorem
-
- ⊢ ∀n ls i.
- nth_fuel n ls i =
- case n of
- 0 => Loop
- | SUC n' =>
- case ls of
- ListCons x tl =>
- if u32_to_int i = 0 then Return x
- else
- do i0 <- u32_sub i (int_to_u32 1); nth_fuel n' tl i0 od
- | ListNil => Fail Failure
-
- [nth_fuel_ind] Theorem
-
- ⊢ ∀P. (∀n ls i.
- (∀n' x tl i0.
- n = SUC n' ∧ ls = ListCons x tl ∧ u32_to_int i ≠ 0 ⇒
- P n' tl i0) ⇒
- P n ls i) ⇒
- ∀v v1 v2. P v v1 v2
-
- [nth_fuel_least_success_mono] Theorem
-
- ⊢ ∀n ls i.
- $LEAST (nth_fuel_P ls i) ≤ n ⇒
- nth_fuel n ls i = nth_fuel ($LEAST (nth_fuel_P ls i)) ls i
-
- [nth_fuel_mono] Theorem
-
- ⊢ ∀n m ls i.
- n ≤ m ⇒
- if is_loop (nth_fuel n ls i) then T
- else nth_fuel n ls i = nth_fuel m ls i
-
- [num2error_11] Theorem
-
- ⊢ ∀r r'. r < 1 ⇒ r' < 1 ⇒ (num2error r = num2error r' ⇔ r = r')
-
- [num2error_ONTO] Theorem
-
- ⊢ ∀a. ∃r. a = num2error r ∧ r < 1
-
- [num2error_error2num] Theorem
-
- ⊢ ∀a. num2error (error2num a) = a
-
- [num2error_thm] Theorem
-
- ⊢ num2error 0 = Failure
-
- [result_11] Theorem
-
- ⊢ (∀a a'. Return a = Return a' ⇔ a = a') ∧
- ∀a a'. Fail a = Fail a' ⇔ a = a'
-
- [result_Axiom] Theorem
-
- ⊢ ∀f0 f1 f2. ∃fn.
- (∀a. fn (Return a) = f0 a) ∧ (∀a. fn (Fail a) = f1 a) ∧
- fn Loop = f2
-
- [result_case_cong] Theorem
-
- ⊢ ∀M M' f f1 v.
- M = M' ∧ (∀a. M' = Return a ⇒ f a = f' a) ∧
- (∀a. M' = Fail a ⇒ f1 a = f1' a) ∧ (M' = Loop ⇒ v = v') ⇒
- result_CASE M f f1 v = result_CASE M' f' f1' v'
-
- [result_case_eq] Theorem
-
- ⊢ result_CASE x f f1 v = v' ⇔
- (∃a. x = Return a ∧ f a = v') ∨ (∃e. x = Fail e ∧ f1 e = v') ∨
- x = Loop ∧ v = v'
-
- [result_distinct] Theorem
-
- ⊢ (∀a' a. Return a ≠ Fail a') ∧ (∀a. Return a ≠ Loop) ∧
- ∀a. Fail a ≠ Loop
-
- [result_induction] Theorem
-
- ⊢ ∀P. (∀a. P (Return a)) ∧ (∀e. P (Fail e)) ∧ P Loop ⇒ ∀r. P r
-
- [result_nchotomy] Theorem
-
- ⊢ ∀rr. (∃a. rr = Return a) ∨ (∃e. rr = Fail e) ∨ rr = Loop
-
- [test2_11] Theorem
-
- ⊢ (∀a a'. Variant1_2 a = Variant1_2 a' ⇔ a = a') ∧
- ∀a a'. Variant2_2 a = Variant2_2 a' ⇔ a = a'
-
- [test2_Axiom] Theorem
-
- ⊢ ∀f0 f1. ∃fn.
- (∀a. fn (Variant1_2 a) = f0 a) ∧ ∀a. fn (Variant2_2 a) = f1 a
-
- [test2_case_cong] Theorem
-
- ⊢ ∀M M' f f1.
- M = M' ∧ (∀a. M' = Variant1_2 a ⇒ f a = f' a) ∧
- (∀a. M' = Variant2_2 a ⇒ f1 a = f1' a) ⇒
- test2_CASE M f f1 = test2_CASE M' f' f1'
-
- [test2_case_eq] Theorem
-
- ⊢ test2_CASE x f f1 = v ⇔
- (∃T'. x = Variant1_2 T' ∧ f T' = v) ∨
- ∃T'. x = Variant2_2 T' ∧ f1 T' = v
-
- [test2_distinct] Theorem
-
- ⊢ ∀a' a. Variant1_2 a ≠ Variant2_2 a'
-
- [test2_induction] Theorem
-
- ⊢ ∀P. (∀T. P (Variant1_2 T)) ∧ (∀T. P (Variant2_2 T)) ⇒ ∀t. P t
-
- [test2_nchotomy] Theorem
-
- ⊢ ∀tt. (∃T. tt = Variant1_2 T) ∨ ∃T. tt = Variant2_2 T
-
- [test_11] Theorem
-
- ⊢ (∀a a'. Variant1 a = Variant1 a' ⇔ a = a') ∧
- ∀a a'. Variant2 a = Variant2 a' ⇔ a = a'
-
- [test_Axiom] Theorem
-
- ⊢ ∀f0 f1. ∃fn.
- (∀a. fn (Variant1 a) = f0 a) ∧ ∀a. fn (Variant2 a) = f1 a
-
- [test_case_cong] Theorem
-
- ⊢ ∀M M' f f1.
- M = M' ∧ (∀a. M' = Variant1 a ⇒ f a = f' a) ∧
- (∀a. M' = Variant2 a ⇒ f1 a = f1' a) ⇒
- test_CASE M f f1 = test_CASE M' f' f1'
-
- [test_case_eq] Theorem
-
- ⊢ test_CASE x f f1 = v ⇔
- (∃b. x = Variant1 b ∧ f b = v) ∨ ∃a. x = Variant2 a ∧ f1 a = v
-
- [test_distinct] Theorem
-
- ⊢ ∀a' a. Variant1 a ≠ Variant2 a'
-
- [test_induction] Theorem
-
- ⊢ ∀P. (∀b. P (Variant1 b)) ∧ (∀a. P (Variant2 a)) ⇒ ∀t. P t
-
- [test_nchotomy] Theorem
-
- ⊢ ∀tt. (∃b. tt = Variant1 b) ∨ ∃a. tt = Variant2 a
-
-
-*)
-end