From dc46dbb9a01329c39673fedc195006745c365030 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 2 Jun 2023 17:23:29 +0200 Subject: Update the HOL4 proofs for the last *release* version of HOL4 --- backends/hol4/divDefLibTestTheory.sig | 5 - backends/hol4/divDefNoFixLibTestTheory.sig | 51 +++---- backends/hol4/primitivesTheory.sig | 226 ++++++++++++++--------------- 3 files changed, 137 insertions(+), 145 deletions(-) (limited to 'backends') diff --git a/backends/hol4/divDefLibTestTheory.sig b/backends/hol4/divDefLibTestTheory.sig index d8cc4ab5..2df28a2f 100644 --- a/backends/hol4/divDefLibTestTheory.sig +++ b/backends/hol4/divDefLibTestTheory.sig @@ -53,7 +53,6 @@ sig val tree_distinct : thm val tree_induction : thm val tree_nchotomy : thm - val tree_size_eq : thm val divDefLibTest_grammars : type_grammar.grammar * term_grammar.grammar (* @@ -434,10 +433,6 @@ sig ⊢ ∀tt. (∃a. tt = TLeaf a) ∨ ∃n. tt = TNode n - [tree_size_eq] Theorem - - ⊢ tree1_size f = list_size (tree_size f) - *) end diff --git a/backends/hol4/divDefNoFixLibTestTheory.sig b/backends/hol4/divDefNoFixLibTestTheory.sig index 999cf543..6c8f373c 100644 --- a/backends/hol4/divDefNoFixLibTestTheory.sig +++ b/backends/hol4/divDefNoFixLibTestTheory.sig @@ -5,12 +5,12 @@ sig (* Definitions *) val even___E_def : thm val even___P_def : thm - val even___fuel0_def_UNION_extract0 : thm - val even___fuel0_def_UNION_extract1 : thm - val even___fuel0_def_UNION_primitive : thm - val even___fuel_def_UNION_extract0 : thm - val even___fuel_def_UNION_extract1 : thm - val even___fuel_def_UNION_primitive : thm + val even___fuel0_UNION_extract0_def : thm + val even___fuel0_UNION_extract1_def : thm + val even___fuel0_UNION_primitive_def : thm + val even___fuel_UNION_extract0_def : thm + val even___fuel_UNION_extract1_def : thm + val even___fuel_UNION_primitive_def : thm val even_def : thm val list_t_TY_DEF : thm val list_t_case_def : thm @@ -56,17 +56,17 @@ sig ⊢ ∀i $var$($n). even___P i $var$($n) ⇔ ¬is_diverge (even___fuel0 $var$($n) i) - [even___fuel0_def_UNION_extract0] Definition + [even___fuel0_UNION_extract0_def] Definition - ⊢ ∀x x0. even___fuel0 x x0 = even___fuel0_def_UNION (INL (x,x0)) + ⊢ ∀x x0. even___fuel0 x x0 = even___fuel0_UNION (INL (x,x0)) - [even___fuel0_def_UNION_extract1] Definition + [even___fuel0_UNION_extract1_def] Definition - ⊢ ∀x x0. odd___fuel0 x x0 = even___fuel0_def_UNION (INR (x,x0)) + ⊢ ∀x x0. odd___fuel0 x x0 = even___fuel0_UNION (INR (x,x0)) - [even___fuel0_def_UNION_primitive] Definition + [even___fuel0_UNION_primitive_def] Definition - ⊢ even___fuel0_def_UNION = + ⊢ even___fuel0_UNION = WFREC (@R. WF R ∧ (∀i $var$($n) $var$($m). @@ -75,7 +75,7 @@ sig ∀i $var$($n) $var$($m). $var$($n) = SUC $var$($m) ∧ i ≠ 0 ⇒ R (INL ($var$($m),i − 1)) (INR ($var$($n),i))) - (λeven___fuel0_def_UNION a. + (λeven___fuel0_UNION a. case a of INL ($var$($n),i) => I @@ -85,9 +85,7 @@ sig if i = 0 then do b <- Return T; Return b od else do - b <- - even___fuel0_def_UNION - (INR ($var$($m),i − 1)); + b <- even___fuel0_UNION (INR ($var$($m),i − 1)); Return b od) | INR ($var$($n'),i') => @@ -98,22 +96,21 @@ sig if i' = 0 then do b <- Return F; Return b od else do - b <- - even___fuel0_def_UNION (INL ($var$($m),i' − 1)); + b <- even___fuel0_UNION (INL ($var$($m),i' − 1)); Return b od)) - [even___fuel_def_UNION_extract0] Definition + [even___fuel_UNION_extract0_def] Definition - ⊢ ∀x x0. even___fuel x x0 = even___fuel_def_UNION (INL (x,x0)) + ⊢ ∀x x0. even___fuel x x0 = even___fuel_UNION (INL (x,x0)) - [even___fuel_def_UNION_extract1] Definition + [even___fuel_UNION_extract1_def] Definition - ⊢ ∀x x0. odd___fuel x x0 = even___fuel_def_UNION (INR (x,x0)) + ⊢ ∀x x0. odd___fuel x x0 = even___fuel_UNION (INR (x,x0)) - [even___fuel_def_UNION_primitive] Definition + [even___fuel_UNION_primitive_def] Definition - ⊢ even___fuel_def_UNION = + ⊢ even___fuel_UNION = WFREC (@R. WF R ∧ (∀i $var$($n) $var$($m). @@ -122,7 +119,7 @@ sig ∀i $var$($n) $var$($m). $var$($n) = SUC $var$($m) ∧ i ≠ 0 ⇒ R (INL ($var$($m),i − 1)) (INR ($var$($n),i))) - (λeven___fuel_def_UNION a. + (λeven___fuel_UNION a. case a of INL ($var$($n),i) => I @@ -130,14 +127,14 @@ sig 0 => Diverge | SUC $var$($m) => if i = 0 then Return T - else even___fuel_def_UNION (INR ($var$($m),i − 1))) + else even___fuel_UNION (INR ($var$($m),i − 1))) | INR ($var$($n'),i') => I (case $var$($n') of 0 => Diverge | SUC $var$($m) => if i' = 0 then Return F - else even___fuel_def_UNION (INL ($var$($m),i' − 1)))) + else even___fuel_UNION (INL ($var$($m),i' − 1)))) [even_def] Definition diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig index ae7f083d..6660b02d 100644 --- a/backends/hol4/primitivesTheory.sig +++ b/backends/hol4/primitivesTheory.sig @@ -359,195 +359,200 @@ sig [string] Parent theory of "primitives" - [isize_bounds] Axiom - - [oracles: ] [axioms: isize_bounds] [] - ⊢ isize_min ≤ i16_min ∧ i16_max ≤ isize_max - - [usize_bounds] Axiom - - [oracles: ] [axioms: usize_bounds] [] ⊢ u16_max ≤ usize_max - - [isize_to_int_bounds] Axiom + [i128_to_int_bounds] Axiom - [oracles: ] [axioms: isize_to_int_bounds] [] - ⊢ ∀n. isize_min ≤ isize_to_int n ∧ isize_to_int n ≤ isize_max + [oracles: ] [axioms: i128_to_int_bounds] [] + ⊢ ∀n. i128_min ≤ i128_to_int n ∧ i128_to_int n ≤ i128_max - [i8_to_int_bounds] Axiom + [i128_to_int_int_to_i128] Axiom - [oracles: ] [axioms: i8_to_int_bounds] [] - ⊢ ∀n. i8_min ≤ i8_to_int n ∧ i8_to_int n ≤ i8_max + [oracles: ] [axioms: i128_to_int_int_to_i128] [] + ⊢ ∀n. i128_min ≤ n ∧ n ≤ i128_max ⇒ i128_to_int (int_to_i128 n) = n [i16_to_int_bounds] Axiom [oracles: ] [axioms: i16_to_int_bounds] [] ⊢ ∀n. i16_min ≤ i16_to_int n ∧ i16_to_int n ≤ i16_max + [i16_to_int_int_to_i16] Axiom + + [oracles: ] [axioms: i16_to_int_int_to_i16] [] + ⊢ ∀n. i16_min ≤ n ∧ n ≤ i16_max ⇒ i16_to_int (int_to_i16 n) = n + [i32_to_int_bounds] Axiom [oracles: ] [axioms: i32_to_int_bounds] [] ⊢ ∀n. i32_min ≤ i32_to_int n ∧ i32_to_int n ≤ i32_max + [i32_to_int_int_to_i32] Axiom + + [oracles: ] [axioms: i32_to_int_int_to_i32] [] + ⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ i32_to_int (int_to_i32 n) = n + [i64_to_int_bounds] Axiom [oracles: ] [axioms: i64_to_int_bounds] [] ⊢ ∀n. i64_min ≤ i64_to_int n ∧ i64_to_int n ≤ i64_max - [i128_to_int_bounds] Axiom + [i64_to_int_int_to_i64] Axiom - [oracles: ] [axioms: i128_to_int_bounds] [] - ⊢ ∀n. i128_min ≤ i128_to_int n ∧ i128_to_int n ≤ i128_max + [oracles: ] [axioms: i64_to_int_int_to_i64] [] + ⊢ ∀n. i64_min ≤ n ∧ n ≤ i64_max ⇒ i64_to_int (int_to_i64 n) = n - [usize_to_int_bounds] Axiom + [i8_to_int_bounds] Axiom - [oracles: ] [axioms: usize_to_int_bounds] [] - ⊢ ∀n. 0 ≤ usize_to_int n ∧ usize_to_int n ≤ usize_max + [oracles: ] [axioms: i8_to_int_bounds] [] + ⊢ ∀n. i8_min ≤ i8_to_int n ∧ i8_to_int n ≤ i8_max - [u8_to_int_bounds] Axiom + [i8_to_int_int_to_i8] Axiom - [oracles: ] [axioms: u8_to_int_bounds] [] - ⊢ ∀n. 0 ≤ u8_to_int n ∧ u8_to_int n ≤ u8_max + [oracles: ] [axioms: i8_to_int_int_to_i8] [] + ⊢ ∀n. i8_min ≤ n ∧ n ≤ i8_max ⇒ i8_to_int (int_to_i8 n) = n - [u16_to_int_bounds] Axiom + [int_to_i128_i128_to_int] Axiom - [oracles: ] [axioms: u16_to_int_bounds] [] - ⊢ ∀n. 0 ≤ u16_to_int n ∧ u16_to_int n ≤ u16_max + [oracles: ] [axioms: int_to_i128_i128_to_int] [] + ⊢ ∀i. int_to_i128 (i128_to_int i) = i - [u32_to_int_bounds] Axiom + [int_to_i16_i16_to_int] Axiom - [oracles: ] [axioms: u32_to_int_bounds] [] - ⊢ ∀n. 0 ≤ u32_to_int n ∧ u32_to_int n ≤ u32_max + [oracles: ] [axioms: int_to_i16_i16_to_int] [] + ⊢ ∀i. int_to_i16 (i16_to_int i) = i - [u64_to_int_bounds] Axiom + [int_to_i32_i32_to_int] Axiom - [oracles: ] [axioms: u64_to_int_bounds] [] - ⊢ ∀n. 0 ≤ u64_to_int n ∧ u64_to_int n ≤ u64_max + [oracles: ] [axioms: int_to_i32_i32_to_int] [] + ⊢ ∀i. int_to_i32 (i32_to_int i) = i - [u128_to_int_bounds] Axiom + [int_to_i64_i64_to_int] Axiom - [oracles: ] [axioms: u128_to_int_bounds] [] - ⊢ ∀n. 0 ≤ u128_to_int n ∧ u128_to_int n ≤ u128_max + [oracles: ] [axioms: int_to_i64_i64_to_int] [] + ⊢ ∀i. int_to_i64 (i64_to_int i) = i - [isize_to_int_int_to_isize] Axiom + [int_to_i8_i8_to_int] Axiom - [oracles: ] [axioms: isize_to_int_int_to_isize] [] - ⊢ ∀n. isize_min ≤ n ∧ n ≤ isize_max ⇒ - isize_to_int (int_to_isize n) = n + [oracles: ] [axioms: int_to_i8_i8_to_int] [] + ⊢ ∀i. int_to_i8 (i8_to_int i) = i - [i8_to_int_int_to_i8] Axiom + [int_to_isize_isize_to_int] Axiom - [oracles: ] [axioms: i8_to_int_int_to_i8] [] - ⊢ ∀n. i8_min ≤ n ∧ n ≤ i8_max ⇒ i8_to_int (int_to_i8 n) = n + [oracles: ] [axioms: int_to_isize_isize_to_int] [] + ⊢ ∀i. int_to_isize (isize_to_int i) = i - [i16_to_int_int_to_i16] Axiom + [int_to_u128_u128_to_int] Axiom - [oracles: ] [axioms: i16_to_int_int_to_i16] [] - ⊢ ∀n. i16_min ≤ n ∧ n ≤ i16_max ⇒ i16_to_int (int_to_i16 n) = n + [oracles: ] [axioms: int_to_u128_u128_to_int] [] + ⊢ ∀i. int_to_u128 (u128_to_int i) = i - [i32_to_int_int_to_i32] Axiom + [int_to_u16_u16_to_int] Axiom - [oracles: ] [axioms: i32_to_int_int_to_i32] [] - ⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ i32_to_int (int_to_i32 n) = n + [oracles: ] [axioms: int_to_u16_u16_to_int] [] + ⊢ ∀i. int_to_u16 (u16_to_int i) = i - [i64_to_int_int_to_i64] Axiom + [int_to_u32_u32_to_int] Axiom - [oracles: ] [axioms: i64_to_int_int_to_i64] [] - ⊢ ∀n. i64_min ≤ n ∧ n ≤ i64_max ⇒ i64_to_int (int_to_i64 n) = n + [oracles: ] [axioms: int_to_u32_u32_to_int] [] + ⊢ ∀i. int_to_u32 (u32_to_int i) = i - [i128_to_int_int_to_i128] Axiom + [int_to_u64_u64_to_int] Axiom - [oracles: ] [axioms: i128_to_int_int_to_i128] [] - ⊢ ∀n. i128_min ≤ n ∧ n ≤ i128_max ⇒ i128_to_int (int_to_i128 n) = n + [oracles: ] [axioms: int_to_u64_u64_to_int] [] + ⊢ ∀i. int_to_u64 (u64_to_int i) = i - [usize_to_int_int_to_usize] Axiom + [int_to_u8_u8_to_int] Axiom - [oracles: ] [axioms: usize_to_int_int_to_usize] [] - ⊢ ∀n. 0 ≤ n ∧ n ≤ usize_max ⇒ usize_to_int (int_to_usize n) = n + [oracles: ] [axioms: int_to_u8_u8_to_int] [] + ⊢ ∀i. int_to_u8 (u8_to_int i) = i - [u8_to_int_int_to_u8] Axiom + [int_to_usize_usize_to_int] Axiom - [oracles: ] [axioms: u8_to_int_int_to_u8] [] - ⊢ ∀n. 0 ≤ n ∧ n ≤ u8_max ⇒ u8_to_int (int_to_u8 n) = n + [oracles: ] [axioms: int_to_usize_usize_to_int] [] + ⊢ ∀i. int_to_usize (usize_to_int i) = i - [u16_to_int_int_to_u16] Axiom + [isize_bounds] Axiom - [oracles: ] [axioms: u16_to_int_int_to_u16] [] - ⊢ ∀n. 0 ≤ n ∧ n ≤ u16_max ⇒ u16_to_int (int_to_u16 n) = n + [oracles: ] [axioms: isize_bounds] [] + ⊢ isize_min ≤ i16_min ∧ i16_max ≤ isize_max - [u32_to_int_int_to_u32] Axiom + [isize_to_int_bounds] Axiom - [oracles: ] [axioms: u32_to_int_int_to_u32] [] - ⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ u32_to_int (int_to_u32 n) = n + [oracles: ] [axioms: isize_to_int_bounds] [] + ⊢ ∀n. isize_min ≤ isize_to_int n ∧ isize_to_int n ≤ isize_max - [u64_to_int_int_to_u64] Axiom + [isize_to_int_int_to_isize] Axiom - [oracles: ] [axioms: u64_to_int_int_to_u64] [] - ⊢ ∀n. 0 ≤ n ∧ n ≤ u64_max ⇒ u64_to_int (int_to_u64 n) = n + [oracles: ] [axioms: isize_to_int_int_to_isize] [] + ⊢ ∀n. isize_min ≤ n ∧ n ≤ isize_max ⇒ + isize_to_int (int_to_isize n) = n + + [mk_vec_axiom] Axiom + + [oracles: ] [axioms: mk_vec_axiom] [] + ⊢ ∀l. len l ≤ usize_max ⇒ vec_to_list (mk_vec l) = l + + [u128_to_int_bounds] Axiom + + [oracles: ] [axioms: u128_to_int_bounds] [] + ⊢ ∀n. 0 ≤ u128_to_int n ∧ u128_to_int n ≤ u128_max [u128_to_int_int_to_u128] Axiom [oracles: ] [axioms: u128_to_int_int_to_u128] [] ⊢ ∀n. 0 ≤ n ∧ n ≤ u128_max ⇒ u128_to_int (int_to_u128 n) = n - [int_to_i8_i8_to_int] Axiom - - [oracles: ] [axioms: int_to_i8_i8_to_int] [] - ⊢ ∀i. int_to_i8 (i8_to_int i) = i - - [int_to_i16_i16_to_int] Axiom + [u16_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_i16_i16_to_int] [] - ⊢ ∀i. int_to_i16 (i16_to_int i) = i + [oracles: ] [axioms: u16_to_int_bounds] [] + ⊢ ∀n. 0 ≤ u16_to_int n ∧ u16_to_int n ≤ u16_max - [int_to_i32_i32_to_int] Axiom + [u16_to_int_int_to_u16] Axiom - [oracles: ] [axioms: int_to_i32_i32_to_int] [] - ⊢ ∀i. int_to_i32 (i32_to_int i) = i + [oracles: ] [axioms: u16_to_int_int_to_u16] [] + ⊢ ∀n. 0 ≤ n ∧ n ≤ u16_max ⇒ u16_to_int (int_to_u16 n) = n - [int_to_i64_i64_to_int] Axiom + [u32_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_i64_i64_to_int] [] - ⊢ ∀i. int_to_i64 (i64_to_int i) = i + [oracles: ] [axioms: u32_to_int_bounds] [] + ⊢ ∀n. 0 ≤ u32_to_int n ∧ u32_to_int n ≤ u32_max - [int_to_i128_i128_to_int] Axiom + [u32_to_int_int_to_u32] Axiom - [oracles: ] [axioms: int_to_i128_i128_to_int] [] - ⊢ ∀i. int_to_i128 (i128_to_int i) = i + [oracles: ] [axioms: u32_to_int_int_to_u32] [] + ⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ u32_to_int (int_to_u32 n) = n - [int_to_isize_isize_to_int] Axiom + [u64_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_isize_isize_to_int] [] - ⊢ ∀i. int_to_isize (isize_to_int i) = i + [oracles: ] [axioms: u64_to_int_bounds] [] + ⊢ ∀n. 0 ≤ u64_to_int n ∧ u64_to_int n ≤ u64_max - [int_to_u8_u8_to_int] Axiom + [u64_to_int_int_to_u64] Axiom - [oracles: ] [axioms: int_to_u8_u8_to_int] [] - ⊢ ∀i. int_to_u8 (u8_to_int i) = i + [oracles: ] [axioms: u64_to_int_int_to_u64] [] + ⊢ ∀n. 0 ≤ n ∧ n ≤ u64_max ⇒ u64_to_int (int_to_u64 n) = n - [int_to_u16_u16_to_int] Axiom + [u8_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_u16_u16_to_int] [] - ⊢ ∀i. int_to_u16 (u16_to_int i) = i + [oracles: ] [axioms: u8_to_int_bounds] [] + ⊢ ∀n. 0 ≤ u8_to_int n ∧ u8_to_int n ≤ u8_max - [int_to_u32_u32_to_int] Axiom + [u8_to_int_int_to_u8] Axiom - [oracles: ] [axioms: int_to_u32_u32_to_int] [] - ⊢ ∀i. int_to_u32 (u32_to_int i) = i + [oracles: ] [axioms: u8_to_int_int_to_u8] [] + ⊢ ∀n. 0 ≤ n ∧ n ≤ u8_max ⇒ u8_to_int (int_to_u8 n) = n - [int_to_u64_u64_to_int] Axiom + [usize_bounds] Axiom - [oracles: ] [axioms: int_to_u64_u64_to_int] [] - ⊢ ∀i. int_to_u64 (u64_to_int i) = i + [oracles: ] [axioms: usize_bounds] [] ⊢ u16_max ≤ usize_max - [int_to_u128_u128_to_int] Axiom + [usize_to_int_bounds] Axiom - [oracles: ] [axioms: int_to_u128_u128_to_int] [] - ⊢ ∀i. int_to_u128 (u128_to_int i) = i + [oracles: ] [axioms: usize_to_int_bounds] [] + ⊢ ∀n. 0 ≤ usize_to_int n ∧ usize_to_int n ≤ usize_max - [int_to_usize_usize_to_int] Axiom + [usize_to_int_int_to_usize] Axiom - [oracles: ] [axioms: int_to_usize_usize_to_int] [] - ⊢ ∀i. int_to_usize (usize_to_int i) = i + [oracles: ] [axioms: usize_to_int_int_to_usize] [] + ⊢ ∀n. 0 ≤ n ∧ n ≤ usize_max ⇒ usize_to_int (int_to_usize n) = n [vec_to_list_num_bounds] Axiom @@ -555,11 +560,6 @@ sig ⊢ ∀v. 0 ≤ LENGTH (vec_to_list v) ∧ LENGTH (vec_to_list v) ≤ Num usize_max - [mk_vec_axiom] Axiom - - [oracles: ] [axioms: mk_vec_axiom] [] - ⊢ ∀l. len l ≤ usize_max ⇒ vec_to_list (mk_vec l) = l - [bind_def] Definition ⊢ ∀x f. -- cgit v1.2.3