summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--backends/hol4/divDefLib.sml9
-rw-r--r--backends/hol4/divDefLibTestTheory.sig116
2 files changed, 65 insertions, 60 deletions
diff --git a/backends/hol4/divDefLib.sml b/backends/hol4/divDefLib.sml
index 80f47f65..f53ef6f8 100644
--- a/backends/hol4/divDefLib.sml
+++ b/backends/hol4/divDefLib.sml
@@ -896,9 +896,14 @@ fun DefineDiv (def_qt : term quotation) =
(* Prove the final equations *)
val def_eqs = prove_def_eqs body_is_valid def_tms raw_defs
- (* Save the definitions *)
+ (* Save the final equations as definitions.
+
+ Note that because we use the same names, doing this overrides the "raw"
+ definitions, which are then forgotten, which means we don't need to
+ manually delete them.
+ *)
val thm_names = map (fn x => x ^ "_def") fnames
- val _ = map save_thm (zip thm_names def_eqs)
+ val _ = map store_definition (zip thm_names def_eqs)
in
def_eqs
end
diff --git a/backends/hol4/divDefLibTestTheory.sig b/backends/hol4/divDefLibTestTheory.sig
index 8da736ab..526f74a6 100644
--- a/backends/hol4/divDefLibTestTheory.sig
+++ b/backends/hol4/divDefLibTestTheory.sig
@@ -5,14 +5,20 @@ sig
(* Definitions *)
val btree_TY_DEF : thm
val btree_case_def : thm
+ val btree_height_def : thm
val btree_size_def : thm
+ val even_def : thm
val list_t_TY_DEF : thm
val list_t_case_def : thm
val list_t_size_def : thm
val node_TY_DEF : thm
val node_case_def : thm
+ val nth_def : thm
+ val odd_def : thm
val tree_TY_DEF : thm
val tree_case_def : thm
+ val tree_height_def : thm
+ val tree_nodes_height_def : thm
val tree_size_def : thm
(* Theorems *)
@@ -21,13 +27,11 @@ sig
val btree_case_cong : thm
val btree_case_eq : thm
val btree_distinct : thm
- val btree_height_def : thm
val btree_induction : thm
val btree_nchotomy : thm
val datatype_btree : thm
val datatype_list_t : thm
val datatype_tree : thm
- val even_def : thm
val list_t_11 : thm
val list_t_Axiom : thm
val list_t_case_cong : thm
@@ -41,17 +45,13 @@ sig
val node_case_eq : thm
val node_induction : thm
val node_nchotomy : thm
- val nth_def : thm
- val odd_def : thm
val tree_11 : thm
val tree_Axiom : thm
val tree_case_cong : thm
val tree_case_eq : thm
val tree_distinct : thm
- val tree_height_def : thm
val tree_induction : thm
val tree_nchotomy : thm
- val tree_nodes_height_def : thm
val tree_size_eq : thm
val divDefLibTest_grammars : type_grammar.grammar * term_grammar.grammar
@@ -83,6 +83,19 @@ sig
⊢ (∀a f f1. btree_CASE (BLeaf a) f f1 = f a) ∧
∀a0 a1 f f1. btree_CASE (BNode a0 a1) f f1 = f1 a0 a1
+ [btree_height_def] Definition
+
+ ⊢ ∀tree.
+ btree_height tree =
+ case tree of
+ BLeaf v => Return 1
+ | BNode l r =>
+ do
+ hl <- btree_height l;
+ hr <- btree_height r;
+ Return (hl + hr)
+ od
+
[btree_size_def] Definition
⊢ (∀f a. btree_size f (BLeaf a) = 1 + f a) ∧
@@ -90,6 +103,10 @@ sig
btree_size f (BNode a0 a1) =
1 + (btree_size f a0 + btree_size f a1)
+ [even_def] Definition
+
+ ⊢ ∀i. even i = if i = 0 then Return T else odd (i − 1)
+
[list_t_TY_DEF] Definition
⊢ ∃rep.
@@ -163,6 +180,20 @@ sig
⊢ ∀a f. node_CASE (Node a) f = f a
+ [nth_def] Definition
+
+ ⊢ ∀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
+
+ [odd_def] Definition
+
+ ⊢ ∀i. odd i = if i = 0 then Return F else even (i − 1)
+
[tree_TY_DEF] Definition
⊢ ∃rep.
@@ -208,6 +239,27 @@ sig
⊢ (∀a f f1. tree_CASE (TLeaf a) f f1 = f a) ∧
∀a f f1. tree_CASE (TNode a) f f1 = f1 a
+ [tree_height_def] Definition
+
+ ⊢ ∀tree.
+ tree_height tree =
+ case tree of
+ TLeaf v => Return 1
+ | TNode (Node ls) => tree_nodes_height ls
+
+ [tree_nodes_height_def] Definition
+
+ ⊢ ∀ls.
+ tree_nodes_height ls =
+ case ls of
+ [] => Return 0
+ | t::tl =>
+ do
+ h1 <- tree_height t;
+ h2 <- tree_nodes_height tl;
+ Return (h1 + h2)
+ od
+
[tree_size_def] Definition
⊢ (∀f a. tree_size f (TLeaf a) = 1 + f a) ∧
@@ -244,19 +296,6 @@ sig
⊢ ∀a1 a0 a. BLeaf a ≠ BNode a0 a1
- [btree_height_def] Theorem
-
- ⊢ ∀tree.
- btree_height tree =
- case tree of
- BLeaf v => Return 1
- | BNode l r =>
- do
- hl <- btree_height l;
- hr <- btree_height r;
- Return (hl + hr)
- od
-
[btree_induction] Theorem
⊢ ∀P. (∀a. P (BLeaf a)) ∧ (∀b b0. P b ∧ P b0 ⇒ P (BNode b b0)) ⇒
@@ -278,10 +317,6 @@ sig
⊢ DATATYPE (tree TLeaf TNode ∧ node Node)
- [even_def] Theorem
-
- ⊢ ∀i. even i = if i = 0 then Return T else odd (i − 1)
-
[list_t_11] Theorem
⊢ ∀a0 a1 a0' a1'.
@@ -350,20 +385,6 @@ sig
⊢ ∀nn. ∃l. nn = Node l
- [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
-
- [odd_def] Theorem
-
- ⊢ ∀i. odd i = if i = 0 then Return F else even (i − 1)
-
[tree_11] Theorem
⊢ (∀a a'. TLeaf a = TLeaf a' ⇔ a = a') ∧
@@ -392,14 +413,6 @@ sig
⊢ ∀a' a. TLeaf a ≠ TNode a'
- [tree_height_def] Theorem
-
- ⊢ ∀tree.
- tree_height tree =
- case tree of
- TLeaf v => Return 1
- | TNode (Node ls) => tree_nodes_height ls
-
[tree_induction] Theorem
⊢ ∀P0 P1 P2.
@@ -412,19 +425,6 @@ sig
⊢ ∀tt. (∃a. tt = TLeaf a) ∨ ∃n. tt = TNode n
- [tree_nodes_height_def] Theorem
-
- ⊢ ∀ls.
- tree_nodes_height ls =
- case ls of
- [] => Return 0
- | t::tl =>
- do
- h1 <- tree_height t;
- h2 <- tree_nodes_height tl;
- Return (h1 + h2)
- od
-
[tree_size_eq] Theorem
⊢ tree1_size f = list_size (tree_size f)