From a84e0f331053c0860ce80c5a541ff32c857e46c6 Mon Sep 17 00:00:00 2001 From: John Harrison Date: Sun, 6 Jan 2019 19:51:19 -0800 Subject: [PATCH] Added a complete replacement, from Andrea Gabrielli and Marco Maggesi, of the previous arrangements for the definition of finite types of specified size. In place of the former case-by-case approach via "define_finite_type", there is now a pair of type constructors "tybit0" and "tybit1" allowing finite types to be represented schematically in binary, keeping the old scheme only for the base type `:1` defined in "trivia.ml". The parser and printer are modified so that this representation is parsed and printed as before (e.g. what is written `:6` is actually `:(1 tybit1) tybit0`). A conversion "DIMINDEX_CONV", rule "HAS_SIZE_DIMINDEX_RULE" and corresponding tactic "DIMINDEX_TAC" are also provided to compute the `dimindex` function for such types, while syntax constructors and destructors "mk_finty" and "dest_finty" convert between such types and nums. The old "define_finite_type" has been deleted, since it could just be confusing. The same final theorem (without the side-effects) from the call "define_finite_type k" can be obtained using the new setup by "HAS_SIZE_DIMINDEX_RULE(mk_finty(Num.num_of_int k))". In addition, a useful conversion "BITS_ELIM_CONV" is provided for eliminating some stray instances of numeral-constructing constants. Also added two trivial theorems MOD_LT_EQ and MOD_LT_EQ_LT, a new conversional BINOP2_CONV, and missing documentation files for EXPAND_NSUM_CONV and EXPAND_SUM_CONV. Overall new theorems: DIMINDEX_CLAUSES DIMINDEX_TYBIT0 DIMINDEX_TYBIT1 FINITE_1 FINITE_CLAUSES FINITE_TYBIT0 FINITE_TYBIT1 HAS_SIZE_TYBIT0 HAS_SIZE_TYBIT1 MOD_LT_EQ MOD_LT_EQ_LT UNIV_HAS_SIZE_DIMINDEX tybit0_INDUCT tybit0_RECURSION tybit1_INDUCT tybit1_RECURSION --- CHANGES | 102 ++++++++++----- Formal_ineqs/taylor/m_taylor.hl | 8 +- Help/BINOP2_CONV.doc | 33 +++++ Help/BINOP_CONV.doc | 14 +- Help/BITS_ELIM_CONV.doc | 35 +++++ Help/COMB2_CONV.doc | 6 +- Help/COMB_CONV.doc | 4 +- Help/DIMINDEX_CONV.doc | 32 +++++ Help/DIMINDEX_TAC.doc | 33 +++++ Help/EXPAND_CASES_CONV.doc | 8 +- Help/EXPAND_NSUM_CONV.doc | 34 +++++ Help/EXPAND_SUM_CONV.doc | 34 +++++ Help/HAS_SIZE_DIMINDEX_RULE.doc | 29 +++++ Help/NUMSEG_CONV.doc | 2 +- Help/define_finite_type.doc | 43 ------- Help/dest_finty.doc | 26 ++++ Help/mk_finty.doc | 25 ++++ Multivariate/complex_database.ml | 20 +++ Multivariate/multivariate_database.ml | 20 +++ arith.ml | 43 +++++++ basics.ml | 21 +++ cart.ml | 177 +++++++++++++++++++++----- database.ml | 20 +++ equal.ml | 29 +++-- parser.ml | 13 +- printer.ml | 2 + 26 files changed, 673 insertions(+), 140 deletions(-) create mode 100644 Help/BINOP2_CONV.doc create mode 100644 Help/BITS_ELIM_CONV.doc create mode 100644 Help/DIMINDEX_CONV.doc create mode 100644 Help/DIMINDEX_TAC.doc create mode 100644 Help/EXPAND_NSUM_CONV.doc create mode 100644 Help/EXPAND_SUM_CONV.doc create mode 100644 Help/HAS_SIZE_DIMINDEX_RULE.doc delete mode 100644 Help/define_finite_type.doc create mode 100644 Help/dest_finty.doc create mode 100644 Help/mk_finty.doc diff --git a/CHANGES b/CHANGES index 33ed00e8..6cb79817 100644 --- a/CHANGES +++ b/CHANGES @@ -8,6 +8,44 @@ * page: https://github.com/jrh13/hol-light/commits/master * * ***************************************************************** +Sat 5th Jan 2019 arith.ml, basics.ml, cart.ml, parser.ml, printer.ml, Formal_ineqs/taylor/m_taylor.hl, Help/BITS_ELIM_CONV.doc [new file], Help/DIMINDEX_CONV.doc [new file], Help/DIMINDEX_TAC.doc [new file], Help/HAS_SIZE_DIMINDEX_RULE.doc [new file], Help/dest_finty.doc [new file], Help/mk_finty.doc [new file] + +Added a complete replacement, from Andrea Gabrielli and Marco Maggesi, of the +previous arrangements for the definition of finite types of specified size. In +place of the former case-by-case approach via "define_finite_type", there is +now a pair of type constructors "tybit0" and "tybit1" allowing finite types to +be represented schematically in binary, keeping the old scheme only for the +base type `:1` defined in "trivia.ml". The parser and printer are modified so +that this representation is parsed and printed as before (e.g. what is written +`:6` is actually `:(1 tybit1) tybit0`). + +A conversion "DIMINDEX_CONV", rule "HAS_SIZE_DIMINDEX_RULE" and corresponding +tactic "DIMINDEX_TAC" are also provided to compute the `dimindex` function for +such types, while syntax constructors and destructors "mk_finty" and +"dest_finty" convert between such types and nums. + +The old "define_finite_type" has been deleted, since it could just be +confusing. The same final theorem (without the side-effects) from the call +"define_finite_type k" can be obtained using the new setup by +"HAS_SIZE_DIMINDEX_RULE(mk_finty(Num.num_of_int k))". + +In addition, a useful conversion "BITS_ELIM_CONV" is provided for eliminating +some stray instances of numeral-constructing constants. + +Thu 3rd Jan 2019 equal.ml, Help/BINOP2_CONV.doc [new file] + +Added a simple new conversional BINOP2_CONV, which is similar to BINOP_CONV +but with different conversions for the left and right. + +Thu 3rd Jan 2019 arith.ml + +Added a couple of trivial results that are easy via DIVISION / LE_1 but +seemed worth having as simple equivalences: + + MOD_LT_EQ = |- !m n. m MOD n < n <=> ~(n = 0) + + MOD_LT_EQ_LT = |- !m n. m MOD n < n <=> 0 < n + Fri 21st Dec 2018 Library/grouptheory.ml Added a number of theorems about group theory, mainly natural interrelations @@ -17,31 +55,31 @@ among various concepts: |- !G h k. cartesian_product k h normal_subgroup_of product_group k G <=> (!i. i IN k ==> h i normal_subgroup_of G i) - + CROSS_NORMAL_SUBGROUP_OF_PROD_GROUP = |- !G1 G2 h1 h2. h1 CROSS h2 normal_subgroup_of prod_group G1 G2 <=> h1 normal_subgroup_of G1 /\ h2 normal_subgroup_of G2 - + GROUP_ELEMENT_ORDER_EQ_2 = |- !G x. x IN group_carrier G ==> (group_element_order G x = 2 <=> ~(x = group_id G) /\ group_pow G x 2 = group_id G) - + GROUP_ELEMENT_ORDER_MUL_SYM = |- !G x y. x IN group_carrier G /\ y IN group_carrier G ==> group_element_order G (group_mul G x y) = group_element_order G (group_mul G y x) - + GROUP_ELEMENT_ORDER_UNIQUE_ALT = |- !G x n. x IN group_carrier G /\ ~(n = 0) ==> (group_element_order G x = n <=> group_pow G x n = group_id G /\ (!m. 0 < m /\ m < n ==> ~(group_pow G x m = group_id G))) - + GROUP_ISOMORPHISM_PRODUCT_QUOTIENT_GROUP = |- !G n k. (!i. i IN k ==> n i normal_subgroup_of G i) @@ -49,7 +87,7 @@ among various concepts: (product_group k (\i. quotient_group (G i) (n i)), quotient_group (product_group k G) (cartesian_product k n)) (cartesian_product k) - + GROUP_ISOMORPHISM_PROD_QUOTIENT_GROUP = |- !G1 G2 n1 n2. n1 normal_subgroup_of G1 /\ n2 normal_subgroup_of G2 @@ -57,117 +95,117 @@ among various concepts: (prod_group (quotient_group G1 n1) (quotient_group G2 n2), quotient_group (prod_group G1 G2) (n1 CROSS n2)) (\(s,t). s CROSS t) - + GROUP_POW_MUL_EQ_ID_SYM = |- !G n x y. x IN group_carrier G /\ y IN group_carrier G ==> (group_pow G (group_mul G x y) n = group_id G <=> group_pow G (group_mul G y x) n = group_id G) - + GROUP_SETINV_SUBGROUP_GENERATED = |- !G h. group_setinv (subgroup_generated G h) = group_setinv G - + GROUP_SETMUL_PRODUCT_GROUP = |- !G k s t. group_setmul (product_group k G) (cartesian_product k s) (cartesian_product k t) = cartesian_product k (\i. group_setmul (G i) (s i) (t i)) - + GROUP_SETMUL_PROD_GROUP = |- !G1 G2 s1 s2 t1 t2. group_setmul (prod_group G1 G2) (s1 CROSS s2) (t1 CROSS t2) = group_setmul G1 s1 t1 CROSS group_setmul G2 s2 t2 - + GROUP_SETMUL_SUBGROUP_GENERATED = |- !G h. group_setmul (subgroup_generated G h) = group_setmul G - + ISOMORPHIC_QUOTIENT_PRODUCT_GROUP = |- !G n k. (!i. i IN k ==> n i normal_subgroup_of G i) - ==> quotient_group (product_group k G) (cartesian_product k n) + ==> quotient_group (product_group k G) (cartesian_product k n) isomorphic_group product_group k (\i. quotient_group (G i) (n i)) - + ISOMORPHIC_QUOTIENT_PROD_GROUP = |- !G1 G2 n1 n2. n1 normal_subgroup_of G1 /\ n2 normal_subgroup_of G2 ==> quotient_group (prod_group G1 G2) (n1 CROSS n2) isomorphic_group prod_group (quotient_group G1 n1) (quotient_group G2 n2) - + LEFT_COSET_PRODUCT_GROUP = |- !G h x k. left_coset (product_group k G) x (cartesian_product k h) = cartesian_product k (\i. left_coset (G i) (x i) (h i)) - + LEFT_COSET_PROD_GROUP = |- !G1 G2 h1 h2 x1 x2. left_coset (prod_group G1 G2) (x1,x2) (h1 CROSS h2) = left_coset G1 x1 h1 CROSS left_coset G2 x2 h2 - + LEFT_COSET_SUBGROUP_GENERATED = |- !G h k x. left_coset (subgroup_generated G h) x k = left_coset G x k - + NORMAL_SUBGROUP_OF_SUBGROUP_GENERATED = |- !G s h. h normal_subgroup_of G /\ h SUBSET s ==> h normal_subgroup_of subgroup_generated G s - + NORMAL_SUBGROUP_OF_SUBGROUP_GENERATED_GEN = |- !G s h. h normal_subgroup_of G /\ h SUBSET group_carrier (subgroup_generated G s) ==> h normal_subgroup_of subgroup_generated G s - + OPPOSITE_PRODUCT_GROUP = |- !G k. opposite_group (product_group k G) = product_group k (\i. opposite_group (G i)) - + OPPOSITE_PROD_GROUP = |- !G1 G2. opposite_group (prod_group G1 G2) = prod_group (opposite_group G1) (opposite_group G2) - + QUOTIENT_GROUP_SUBGROUP_GENERATED = |- !G h n. n normal_subgroup_of G /\ h subgroup_of G /\ n SUBSET h ==> quotient_group (subgroup_generated G h) n = subgroup_generated (quotient_group G n) {right_coset G n x | x IN h} - + RIGHT_COSET_PRODUCT_GROUP = |- !G h x k. right_coset (product_group k G) (cartesian_product k h) x = cartesian_product k (\i. right_coset (G i) (h i) (x i)) - + RIGHT_COSET_PROD_GROUP = |- !G1 G2 h1 h2 x1 x2. right_coset (prod_group G1 G2) (h1 CROSS h2) (x1,x2) = right_coset G1 h1 x1 CROSS right_coset G2 h2 x2 - + RIGHT_COSET_SUBGROUP_GENERATED = |- !G h k x. right_coset (subgroup_generated G h) k x = right_coset G k x - + SUBGROUP_GENERATED_REFL = |- !G s. group_carrier G SUBSET s ==> subgroup_generated G s = G - + SUBGROUP_OF_EPIMORPHIC_PREIMAGE = |- !G H f h. group_epimorphism (G,H) f /\ h subgroup_of H ==> {x | x IN group_carrier G /\ f x IN h} subgroup_of G /\ IMAGE f {x | x IN group_carrier G /\ f x IN h} = h - + SUBGROUP_OF_HOMOMORPHIC_PREIMAGE = |- !G H f h. group_homomorphism (G,H) f /\ h subgroup_of H ==> {x | x IN group_carrier G /\ f x IN h} subgroup_of G - + SUBGROUP_OF_QUOTIENT_GROUP = |- !G n h. n normal_subgroup_of G ==> (h subgroup_of quotient_group G n <=> (?k. k subgroup_of G /\ {right_coset G n x | x IN k} = h)) - + SUBGROUP_OF_QUOTIENT_GROUP_ALT = |- !G n h. n normal_subgroup_of G @@ -175,7 +213,7 @@ among various concepts: (?k. k subgroup_of G /\ n SUBSET k /\ {right_coset G n x | x IN k} = h)) - + SUBGROUP_OF_QUOTIENT_GROUP_GENERATED_BY = |- !G n h. n normal_subgroup_of G /\ h subgroup_of quotient_group G n @@ -183,7 +221,7 @@ among various concepts: n SUBSET k /\ quotient_group (subgroup_generated G k) n = subgroup_generated (quotient_group G n) h) - + SUM_GROUP_EQ_PRODUCT_GROUP = |- !k G. FINITE k ==> sum_group k G = product_group k G diff --git a/Formal_ineqs/taylor/m_taylor.hl b/Formal_ineqs/taylor/m_taylor.hl index 5b6be032..1fe5d544 100644 --- a/Formal_ineqs/taylor/m_taylor.hl +++ b/Formal_ineqs/taylor/m_taylor.hl @@ -59,7 +59,7 @@ let has_size_array = Array.init (max_dim + 1) (fun i -> match i with | 0 -> TRUTH | 1 -> HAS_SIZE_1 - | _ -> define_finite_type i);; + | _ -> HAS_SIZE_DIMINDEX_RULE(mk_finty(Int i)));; let dimindex_array = Array.init (max_dim + 1) (fun i -> if i < 1 then TRUTH else MATCH_MP DIMINDEX_UNIQUE has_size_array.(i));; @@ -306,7 +306,7 @@ let dest_m_cell_domain domain_tm = (**************************************************) (* Given a variable of the type `:real^N`, returns the number N *) -let get_dim = int_of_string o fst o dest_type o hd o tl o snd o dest_type o type_of;; +let get_dim = Num.int_of_num o dest_finty o hd o tl o snd o dest_type o type_of;; (**********************) @@ -385,7 +385,7 @@ let diff2c_domain_tm = `diff2c_domain domain`;; let rec gen_diff2c_domain_poly poly_tm = let x_var, expr = dest_abs poly_tm in - let n = (int_of_string o fst o dest_type o hd o tl o snd o dest_type o type_of) x_var in + let n = get_dim x_var in let diff2c_tm = mk_icomb (diff2c_domain_tm, poly_tm) in if frees expr = [] then (* const *) @@ -452,7 +452,7 @@ let gen_partial_poly = let i_tm = mk_small_numeral i in let rec gen_rec poly_tm = let x_var, expr = dest_abs poly_tm in - let n = (int_of_string o fst o dest_type o hd o tl o snd o dest_type o type_of) x_var in + let n = get_dim x_var in if frees expr = [] then (* const *) (SPECL [i_tm; expr] o inst_first_type_var (n_type_array.(n))) partial_const diff --git a/Help/BINOP2_CONV.doc b/Help/BINOP2_CONV.doc new file mode 100644 index 00000000..162db253 --- /dev/null +++ b/Help/BINOP2_CONV.doc @@ -0,0 +1,33 @@ +\DOC BINOP2_CONV + +\TYPE {BINOP2_CONV : conv -> conv -> conv} + +\SYNOPSIS +Applies conversions to the two arguments of a binary operator. + +\DESCRIBE +If {c1} is a conversion where {c1 `l`} returns {|- l = l'} and {c2} is a +conversion where {c2 `r`} returns {|- r = r'}, then +{BINOP2_CONV c1 c2 `op l r`} returns {|- op l r = op l' r'}. The +term {op} is arbitrary, but is often a constant such as addition or +conjunction. + +\FAILURE +Never fails when applied to the conversion. But may fail when applied to the +term if one of the core conversions fails or returns an inappropriate theorem +on the subterms. + +\EXAMPLE +{ + # BINOP2_CONV NUM_ADD_CONV NUM_SUB_CONV `(3 + 3) * (10 - 3)`;; + val it : thm = |- (3 + 3) * (10 - 3) = 6 * 7 +} + +\COMMENTS +The special case when the two conversions are the same is more briefly achieved +using {BINOP_CONV}. + +\SEEALSO +ABS_CONV, BINOP_CONV, COMB_CONV, COMB2_CONV, RAND_CONV, RATOR_CONV. + +\ENDDOC diff --git a/Help/BINOP_CONV.doc b/Help/BINOP_CONV.doc index 9769794d..1e7c0569 100644 --- a/Help/BINOP_CONV.doc +++ b/Help/BINOP_CONV.doc @@ -1,19 +1,19 @@ \DOC BINOP_CONV -\TYPE {BINOP_CONV : (term -> thm) -> term -> thm} +\TYPE {BINOP_CONV : conv -> conv} \SYNOPSIS Applies a conversion to both arguments of a binary operator. \DESCRIBE -If {c} is a conversion where {c `l`} returns {|- l = l'} and {c `r`} returns -{|- r = r'}, then {BINOP_CONV `op l r`} returns {|- op l r = op l' r'}. The -term {op} is arbitrary, but is often a constant such as addition or +If {c} is a conversion where {c `l`} returns {|- l = l'} and {c `r`} returns +{|- r = r'}, then {BINOP_CONV c `op l r`} returns {|- op l r = op l' r'}. The +term {op} is arbitrary, but is often a constant such as addition or conjunction. \FAILURE -Never fails when applied to the conversion. But may fail when applied to the -term if one of the core conversions fails or returns an inappropriate theorem +Never fails when applied to the conversion. But may fail when applied to the +term if one of the core conversions fails or returns an inappropriate theorem on the subterms. \EXAMPLE @@ -23,6 +23,6 @@ on the subterms. } \SEEALSO -ABS_CONV, COMB_CONV, COMB2_CONV, RAND_CONV, RATOR_CONV. +ABS_CONV, BINOP2_CONV, COMB_CONV, COMB2_CONV, RAND_CONV, RATOR_CONV. \ENDDOC diff --git a/Help/BITS_ELIM_CONV.doc b/Help/BITS_ELIM_CONV.doc new file mode 100644 index 00000000..c59b852b --- /dev/null +++ b/Help/BITS_ELIM_CONV.doc @@ -0,0 +1,35 @@ +\DOC BITS_ELIM_CONV + +\TYPE {BITS_ELIM_CONV : conv} + +\SYNOPSIS +Removes stray instances of special constants used in numeral representation + +\DESCRIBE +The HOL Light representation of numeral constants like {`6`} uses a +number of special constants {`NUMERAL`}, {`BIT0`}, {`BIT1`} and {`_0`}, +essentially to represent those numbers in binary. The conversion +{BITS_ELIM_CONV} eliminates any uses of these constants within the given term +not used as part of a standard numeral. + +\FAILURE +Never fails + +\EXAMPLE +{ + # BITS_ELIM_CONV `BIT0(BIT1(BIT1 _0)) = 6`;; + val it : thm = + |- BIT0 (BIT1 (BIT1 _0)) = 6 <=> 2 * (2 * (2 * 0 + 1) + 1) = 6 + + # (BITS_ELIM_CONV THENC NUM_REDUCE_CONV) `BIT0(BIT1(BIT1 _0)) = 6`;; + val it : thm = |- BIT0 (BIT1 (BIT1 _0)) = 6 <=> T +} + +\USES +Mainly intended for internal use in functions doing sophisticated things with +numerals. + +\SEEALSO +ARITH_RULE, ARITH_TAC, NUM_RING. + +\ENDDOC diff --git a/Help/COMB2_CONV.doc b/Help/COMB2_CONV.doc index 577d29aa..8e5adccd 100644 --- a/Help/COMB2_CONV.doc +++ b/Help/COMB2_CONV.doc @@ -16,7 +16,11 @@ Never fails when applied to the initial conversions. On application to the term, it fails if either {c1} or {c2} does, or if either returns a theorem that is of the wrong form. +\COMMENTS +The special case when the two conversions are the same is more briefly achieved +using {COMB_CONV}. + \SEEALSO -BINOP_CONV, COMB_CONV, LAND_CONV, RAND_CONV, RATOR_CONV +BINOP_CONV, BINOP2_CONV, COMB_CONV, LAND_CONV, RAND_CONV, RATOR_CONV \ENDDOC diff --git a/Help/COMB_CONV.doc b/Help/COMB_CONV.doc index 628131f1..cccab4f6 100644 --- a/Help/COMB_CONV.doc +++ b/Help/COMB_CONV.doc @@ -12,11 +12,11 @@ If {c} is a conversion such that {c `f`} returns {|- f = f'} and immediate subterms. \FAILURE -Never fails when applied to the initial conversion. On application to the term, +Never fails when applied to the initial conversion. On application to the term, it fails if conversion given as the argument does, or if the theorem returned by it is inappropriate. \SEEALSO -BINOP_CONV, COMB2_CONV, LAND_CONV, RAND_CONV, RATOR_CONV +BINOP_CONV, BINOP2_CONV, COMB2_CONV, LAND_CONV, RAND_CONV, RATOR_CONV \ENDDOC diff --git a/Help/DIMINDEX_CONV.doc b/Help/DIMINDEX_CONV.doc new file mode 100644 index 00000000..024bbdf4 --- /dev/null +++ b/Help/DIMINDEX_CONV.doc @@ -0,0 +1,32 @@ +\DOC DIMINDEX_CONV + +\TYPE {DIMINDEX_CONV : conv} + +\SYNOPSIS +Computes the {dimindex} for a standard finite type. + +\DESCRIBE +Finite types parsed and printed as numerals are provided, and this conversion +when applied to a term of the form {`dimindex (:n)`} returns the theorem +{|- dimindex(:n) = n} where the {n} on the right is a numeral term. + +\FAILURE +Fails if the term is not of the form {`dimindex (:n)`} for a standard finite +type. + +\EXAMPLE +Here we use a 32-element type, perhaps useful for indexing the bits of a +word: +{ + # DIMINDEX_CONV `dimindex(:32)`;; + val it : thm = |- dimindex (:32) = 32 +} + +\USES +In conjunction with Cartesian powers such as {real^3}, where only the size of +the indexing type is relevant and the simple name {n} is intuitive. + +\SEEALSO +dest_finty, DIMINDEX_TAC, HAS_SIZE_DIMINDEX_RULE, mk_finty. + +\ENDDOC diff --git a/Help/DIMINDEX_TAC.doc b/Help/DIMINDEX_TAC.doc new file mode 100644 index 00000000..f2cbdbb7 --- /dev/null +++ b/Help/DIMINDEX_TAC.doc @@ -0,0 +1,33 @@ +\DOC DIMINDEX_TAC + +\TYPE {DIMINDEX_TAC : tactic} + +\SYNOPSIS +Solves subterms of a goal by computing the {dimindex} for standard finite types. + +\DESCRIBE +Finite types parsed and printed as numerals are provided, and this tactic +simplfies subterms of a goal of the form {`dimindex (:n)`} to a simple numeral +{`n`}. + +\FAILURE +Never fails + +\EXAMPLE +We set up the following goal: +{ + # g `dimindex(:64) = 2 * dimindex(:32)`;; +} +and simplify it by +{ +# e DIMINDEX_TAC;; +val it : goalstack = 1 subgoal (1 total) + +`64 = 2 * 32` +} +after which simply {ARITH_TAC} would finish the goal. + +\SEEALSO +dest_finty, DIMINDEX_CONV, HAS_SIZE_DIMINDEX_RULE, mk_finty. + +\ENDDOC diff --git a/Help/EXPAND_CASES_CONV.doc b/Help/EXPAND_CASES_CONV.doc index 8b9feece..8e7a071a 100644 --- a/Help/EXPAND_CASES_CONV.doc +++ b/Help/EXPAND_CASES_CONV.doc @@ -6,8 +6,8 @@ Expand a numerical range {`!i. i < n ==> P[i]`}. \DESCRIBE -When applied to a term of the form {`!i. i < n ==> P[i]`} for some {P[i]} and a -numeral {n}, the conversion {EXPAND_CASES_CONV} returns +When applied to a term of the form {`!i. i < n ==> P[i]`} for some {P[i]} and a +numeral {n}, the conversion {EXPAND_CASES_CONV} returns { |- (!i. i < n ==> P[i]) <=> P[0] /\ ... /\ P[n-1] } @@ -26,11 +26,11 @@ Fails if applied to a term that is not of the right form. (~(4 = 0) ==> 12 MOD 4 = 0) # (EXPAND_CASES_CONV THENC NUM_REDUCE_CONV) - `(!n. n < 5 ==> ~(n = 0) ==> 12 MOD n = 0)`;; + `(!n. n < 5 ==> ~(n = 0) ==> 12 MOD n = 0)`;; val it : thm = |- (!n. n < 5 ==> ~(n = 0) ==> 12 MOD n = 0) <=> T } \SEEALSO -NUM_REDUCE_CONV. +EXPAND_SUM_CONV, EXPAND_NSUM_CONV, NUMSEG_CONV, NUM_REDUCE_CONV. \ENDDOC diff --git a/Help/EXPAND_NSUM_CONV.doc b/Help/EXPAND_NSUM_CONV.doc new file mode 100644 index 00000000..1a75c214 --- /dev/null +++ b/Help/EXPAND_NSUM_CONV.doc @@ -0,0 +1,34 @@ +\DOC EXPAND_NSUM_CONV + +\TYPE {EXPAND_NSUM_CONV : conv} + +\SYNOPSIS +Expands a natural number sum over an explicit interval of numerals + +\DESCRIBE +The conversion {EXPAND_NSUM_CONV} applied to a term of the form +{`nsum (m..n) f`} where {m} and {n} are explicit numerals (the double-dot being +an infix set construction for a range), returns an expansion theorem +{|- nsum (m..n) f = f(m) + ... + f(n)}. In the common case where {f} is a +lambda-term, each application {f(i)} will be beta-reduced at the top level. + +\FAILURE +{EXPAND_NSUM_CONV tm} fails if {tm} is not a sum of the specified form. + +\EXAMPLE +The following is a typical use of the conversion: +{ + # EXPAND_NSUM_CONV `nsum (1..5) (\n. n * n)`;; + val it : thm = + |- nsum (1..5) (\n. n * n) = 1 * 1 + 2 * 2 + 3 * 3 + 4 * 4 + 5 * 5 +} + +\COMMENTS +As well as the real-number version {EXPAND_SUM_CONV} in the core HOL Light, the +library file {Library/isum.ml} contains a corresponding form for integer sums +{EXPAND_ISUM_CONV}. + +\SEEALSO +EXPAND_CASES_CONV, EXPAND_SUM_CONV, NUMSEG_CONV. + +\ENDDOC diff --git a/Help/EXPAND_SUM_CONV.doc b/Help/EXPAND_SUM_CONV.doc new file mode 100644 index 00000000..a078b8b8 --- /dev/null +++ b/Help/EXPAND_SUM_CONV.doc @@ -0,0 +1,34 @@ +\DOC EXPAND_SUM_CONV + +\TYPE {EXPAND_SUM_CONV : conv} + +\SYNOPSIS +Expands a real number sum over an explicit interval of numerals + +\DESCRIBE +The conversion {EXPAND_SUM_CONV} applied to a term of the form +{`sum (m..n) f`} where {m} and {n} are explicit numerals (the double-dot being +an infix set construction for a range), returns an expansion theorem +{|- sum (m..n) f = f(m) + ... + f(n)}. In the common case where {f} is a +lambda-term, each application {f(i)} will be beta-reduced at the top level. + +\FAILURE +{EXPAND_SUM_CONV tm} fails if {tm} is not a sum of the specified form. + +\EXAMPLE +The following is a typical use of the conversion: +{ + # EXPAND_SUM_CONV `sum(1..8) f`;; + val it : thm = + |- sum (1..8) f = f 1 + f 2 + f 3 + f 4 + f 5 + f 6 + f 7 + f 8 +} + +\COMMENTS +As well as the natural-number version {EXPAND_NSUM_CONV} in the core HOL Light, +the library file {Library/isum.ml} contains a corresponding form for integer +sums {EXPAND_ISUM_CONV}. + +\SEEALSO +EXPAND_CASES_CONV, EXPAND_NSUM_CONV, NUMSEG_CONV. + +\ENDDOC diff --git a/Help/HAS_SIZE_DIMINDEX_RULE.doc b/Help/HAS_SIZE_DIMINDEX_RULE.doc new file mode 100644 index 00000000..cd030643 --- /dev/null +++ b/Help/HAS_SIZE_DIMINDEX_RULE.doc @@ -0,0 +1,29 @@ +\DOC HAS_SIZE_DIMINDEX_RULE + +\TYPE {HAS_SIZE_DIMINDEX_RULE : hol_type -> thm} + +\SYNOPSIS +Computes the {dimindex} for a standard finite type. + +\DESCRIBE +Finite types parsed and printed as numerals are provided, and this conversion +when applied to such a type of the form {`:n`} returns the theorem +{|- (:n) HAS_SIZE n} where the {(:n)} is the customary HOL Light printing of +the universe set {UNIV:n->bool}, the second {n} is a numeral term and +{HAS_SIZE} is the usual cardinality relation. + +\FAILURE +Fails if the type provided is not a standard finite type. + +\EXAMPLE +Here we use a 64-element type, perhaps useful for indexing the bits of a +word: +{ + # HAS_SIZE_DIMINDEX_RULE `:64`;; + val it : thm = |- (:64) HAS_SIZE 64 +} + +\SEEALSO +dest_finty, DIMINDEX_CONV, DIMINDEX_TAC, mk_finty. + +\ENDDOC diff --git a/Help/NUMSEG_CONV.doc b/Help/NUMSEG_CONV.doc index beeaa04d..1e5fe0b2 100644 --- a/Help/NUMSEG_CONV.doc +++ b/Help/NUMSEG_CONV.doc @@ -25,6 +25,6 @@ Fails unless applied to a term of the form {m..n} for specific numerals {m} and } \SEEALSO -SET_RULE, SET_TAC. +EXPAND_CASES_CONV, EXPAND_NSUM_CONV, EXPAND_SUM_CONV, SET_RULE, SET_TAC. \ENDDOC diff --git a/Help/define_finite_type.doc b/Help/define_finite_type.doc deleted file mode 100644 index f17e8c7e..00000000 --- a/Help/define_finite_type.doc +++ /dev/null @@ -1,43 +0,0 @@ -\DOC define_finite_type - -\TYPE {define_finite_type : int -> thm} - -\SYNOPSIS -Defines a new type of a specified finite size. - -\DESCRIBE -The call {define_finite_type n} where {n} is a positive integer defines a new -type also called simply `{n}', and returns a theorem asserting that its -universe has size {n}, in the form: -{ - |- (:n) HAS_SIZE n -} -\noindent where {(:n)} is the customary HOL Light printing of the universe set -{UNIV:n->bool}. - -\FAILURE -Fails if {n} is zero or negative, or if there is a type of the same name -(unless it was also defined by the same call for {define_finite_type}, which is -perfectly permissible), or if the names of the type constructor and destructor -functions are already in use: -{ - mk_auto_define_finite_type_n:num->n - dest_auto_define_finite_type_n:32->num -} - -\EXAMPLE -Here we define a 32-element type, perhaps useful for indexing the bits of a -word: -{ - # define_finite_type 32;; - val it : thm = |- (:32) HAS_SIZE 32 -} - -\USES -In conjunction with Cartesian powers such as {real^3}, where only the size of -the indexing type is relevant and the simple name {n} is intuitive. - -\SEEALSO -define_type, new_type_definition. - -\ENDDOC diff --git a/Help/dest_finty.doc b/Help/dest_finty.doc new file mode 100644 index 00000000..db78049d --- /dev/null +++ b/Help/dest_finty.doc @@ -0,0 +1,26 @@ +\DOC dest_finty + +\TYPE {dest_finty : hol_type -> num} + +\SYNOPSIS +Converts a standard finite type to corresponding integer. + +\DESCRIBE +Finite types parsed and printed as numerals are provided, and this operation +when applied to such a type gives the corresponding number. + +\FAILURE +Fails if the type is not a standard finite type. + +\EXAMPLE +Here we use a 32-element type, perhaps useful for indexing the bits of a +word: +{ + # dest_finty `:32`;; + val it : num = 32 +} + +\SEEALSO +dest_type, DIMINDEX_CONV, DIMINDEX_TAC, HAS_SIZE_DIMINDEX_RULE, mk_finty. + +\ENDDOC diff --git a/Help/mk_finty.doc b/Help/mk_finty.doc new file mode 100644 index 00000000..7868b7cf --- /dev/null +++ b/Help/mk_finty.doc @@ -0,0 +1,25 @@ +\DOC mk_finty + +\TYPE {mk_finty :num -> hol_type} + +\SYNOPSIS +Converts an integer to a standard finite type. + +\DESCRIBE +Finite types parsed and printed as numerals are provided, and this operation +when applied to a number gives a type of that size. + +\FAILURE +Fails if the number is not a strictly positive integer. + +\EXAMPLE +Here we use a 6-element type: +{ + # mk_finty (Int 6);; + val it : hol_type = `:6` +} + +\SEEALSO +dest_finty, DIMINDEX_CONV, DIMINDEX_TAC, HAS_SIZE_DIMINDEX_RULE, mk_type. + +\ENDDOC diff --git a/Multivariate/complex_database.ml b/Multivariate/complex_database.ml index 9ed96d8f..051beb8e 100644 --- a/Multivariate/complex_database.ml +++ b/Multivariate/complex_database.ml @@ -4996,6 +4996,7 @@ theorems := "DIMINDEX_2",DIMINDEX_2; "DIMINDEX_3",DIMINDEX_3; "DIMINDEX_4",DIMINDEX_4; +"DIMINDEX_CLAUSES",DIMINDEX_CLAUSES; "DIMINDEX_FINITE_DIFF",DIMINDEX_FINITE_DIFF; "DIMINDEX_FINITE_IMAGE",DIMINDEX_FINITE_IMAGE; "DIMINDEX_FINITE_PROD",DIMINDEX_FINITE_PROD; @@ -5006,6 +5007,8 @@ theorems := "DIMINDEX_HAS_SIZE_FINITE_SUM",DIMINDEX_HAS_SIZE_FINITE_SUM; "DIMINDEX_MULTIVECTOR",DIMINDEX_MULTIVECTOR; "DIMINDEX_NONZERO",DIMINDEX_NONZERO; +"DIMINDEX_TYBIT0",DIMINDEX_TYBIT0; +"DIMINDEX_TYBIT1",DIMINDEX_TYBIT1; "DIMINDEX_UNIQUE",DIMINDEX_UNIQUE; "DIMINDEX_UNIV",DIMINDEX_UNIV; "DIM_BASIS_IMAGE",DIM_BASIS_IMAGE; @@ -5908,6 +5911,7 @@ theorems := "FINE_UNION",FINE_UNION; "FINE_UNIONS",FINE_UNIONS; "FINITELY_GENERATED_CONIC_POLYHEDRON",FINITELY_GENERATED_CONIC_POLYHEDRON; +"FINITE_1",FINITE_1; "FINITE_ANR_COMPLEMENT_COMPONENTS_CONCENTRIC",FINITE_ANR_COMPLEMENT_COMPONENTS_CONCENTRIC; "FINITE_ANR_COMPONENTS",FINITE_ANR_COMPONENTS; "FINITE_BALL",FINITE_BALL; @@ -5924,6 +5928,7 @@ theorems := "FINITE_CASES",FINITE_CASES; "FINITE_CBALL",FINITE_CBALL; "FINITE_CIRCLE_INTERSECTION",FINITE_CIRCLE_INTERSECTION; +"FINITE_CLAUSES",FINITE_CLAUSES; "FINITE_COLUMNS",FINITE_COLUMNS; "FINITE_COMPLEMENT_ANR_COMPONENTS",FINITE_COMPLEMENT_ANR_COMPONENTS; "FINITE_COMPLEMENT_ENR_COMPONENTS",FINITE_COMPLEMENT_ENR_COMPONENTS; @@ -6068,6 +6073,8 @@ theorems := "FINITE_T1_SPACE_IMP_DISCRETE_TOPOLOGY",FINITE_T1_SPACE_IMP_DISCRETE_TOPOLOGY; "FINITE_TOPSPACE_IMP_DISCRETE_TOPOLOGY",FINITE_TOPSPACE_IMP_DISCRETE_TOPOLOGY; "FINITE_TRANSITIVITY_CHAIN",FINITE_TRANSITIVITY_CHAIN; +"FINITE_TYBIT0",FINITE_TYBIT0; +"FINITE_TYBIT1",FINITE_TYBIT1; "FINITE_UNION",FINITE_UNION; "FINITE_UNIONS",FINITE_UNIONS; "FINITE_UNION_IMP",FINITE_UNION_IMP; @@ -7641,6 +7648,8 @@ theorems := "HAS_SIZE_SPHERE_2",HAS_SIZE_SPHERE_2; "HAS_SIZE_STDBASIS",HAS_SIZE_STDBASIS; "HAS_SIZE_SUC",HAS_SIZE_SUC; +"HAS_SIZE_TYBIT0",HAS_SIZE_TYBIT0; +"HAS_SIZE_TYBIT1",HAS_SIZE_TYBIT1; "HAS_SIZE_UNBOUNDED_COMPONENTS_COMPLEMENT",HAS_SIZE_UNBOUNDED_COMPONENTS_COMPLEMENT; "HAS_SIZE_UNBOUNDED_COMPONENTS_COMPLEMENT_1",HAS_SIZE_UNBOUNDED_COMPONENTS_COMPLEMENT_1; "HAS_SIZE_UNION",HAS_SIZE_UNION; @@ -8470,6 +8479,10 @@ theorems := "HYPERPLANE_FACET_OF_HALFSPACE_LE",HYPERPLANE_FACET_OF_HALFSPACE_LE; "HYPERPLANE_FACE_OF_HALFSPACE_GE",HYPERPLANE_FACE_OF_HALFSPACE_GE; "HYPERPLANE_FACE_OF_HALFSPACE_LE",HYPERPLANE_FACE_OF_HALFSPACE_LE; +"Hashek.hashek_def",Hashek.hashek_def; +"Hashek.hashek_eq",Hashek.hashek_eq; +"Hashek.hashek_prop",Hashek.hashek_prop; +"Hashek.hashek_thm",Hashek.hashek_thm; "IDEMPOTENT_IMP_RETRACTION",IDEMPOTENT_IMP_RETRACTION; "IDEMPOTENT_MATRIX_MUL_LINV",IDEMPOTENT_MATRIX_MUL_LINV; "IDEMPOTENT_MATRIX_MUL_RINV",IDEMPOTENT_MATRIX_MUL_RINV; @@ -11710,6 +11723,8 @@ theorems := "MOD_LE",MOD_LE; "MOD_LE_TWICE",MOD_LE_TWICE; "MOD_LT",MOD_LT; +"MOD_LT_EQ",MOD_LT_EQ; +"MOD_LT_EQ_LT",MOD_LT_EQ_LT; "MOD_MOD",MOD_MOD; "MOD_MOD_EXP_MIN",MOD_MOD_EXP_MIN; "MOD_MOD_LE",MOD_MOD_LE; @@ -17567,6 +17582,7 @@ theorems := "UNIV",UNIV; "UNIVERSAL_COVERING_SPACE",UNIVERSAL_COVERING_SPACE; "UNIV_GSPEC",UNIV_GSPEC; +"UNIV_HAS_SIZE_DIMINDEX",UNIV_HAS_SIZE_DIMINDEX; "UNIV_NOT_EMPTY",UNIV_NOT_EMPTY; "UNIV_PCROSS_UNIV",UNIV_PCROSS_UNIV; "UNIV_SECOND_COUNTABLE",UNIV_SECOND_COUNTABLE; @@ -18741,6 +18757,10 @@ theorems := "trivial_group",trivial_group; "trivial_homomorphism",trivial_homomorphism; "trivial_limit",trivial_limit; +"tybit0_INDUCT",tybit0_INDUCT; +"tybit0_RECURSION",tybit0_RECURSION; +"tybit1_INDUCT",tybit1_INDUCT; +"tybit1_RECURSION",tybit1_RECURSION; "unicoherent",unicoherent; "uniformly_continuous_map",uniformly_continuous_map; "uniformly_continuous_on",uniformly_continuous_on; diff --git a/Multivariate/multivariate_database.ml b/Multivariate/multivariate_database.ml index 88bf721d..51f38d04 100644 --- a/Multivariate/multivariate_database.ml +++ b/Multivariate/multivariate_database.ml @@ -4032,6 +4032,7 @@ theorems := "DIMINDEX_2",DIMINDEX_2; "DIMINDEX_3",DIMINDEX_3; "DIMINDEX_4",DIMINDEX_4; +"DIMINDEX_CLAUSES",DIMINDEX_CLAUSES; "DIMINDEX_FINITE_DIFF",DIMINDEX_FINITE_DIFF; "DIMINDEX_FINITE_IMAGE",DIMINDEX_FINITE_IMAGE; "DIMINDEX_FINITE_PROD",DIMINDEX_FINITE_PROD; @@ -4042,6 +4043,8 @@ theorems := "DIMINDEX_HAS_SIZE_FINITE_SUM",DIMINDEX_HAS_SIZE_FINITE_SUM; "DIMINDEX_MULTIVECTOR",DIMINDEX_MULTIVECTOR; "DIMINDEX_NONZERO",DIMINDEX_NONZERO; +"DIMINDEX_TYBIT0",DIMINDEX_TYBIT0; +"DIMINDEX_TYBIT1",DIMINDEX_TYBIT1; "DIMINDEX_UNIQUE",DIMINDEX_UNIQUE; "DIMINDEX_UNIV",DIMINDEX_UNIV; "DIM_BASIS_IMAGE",DIM_BASIS_IMAGE; @@ -4912,6 +4915,7 @@ theorems := "FINE_UNION",FINE_UNION; "FINE_UNIONS",FINE_UNIONS; "FINITELY_GENERATED_CONIC_POLYHEDRON",FINITELY_GENERATED_CONIC_POLYHEDRON; +"FINITE_1",FINITE_1; "FINITE_ANR_COMPLEMENT_COMPONENTS_CONCENTRIC",FINITE_ANR_COMPLEMENT_COMPONENTS_CONCENTRIC; "FINITE_ANR_COMPONENTS",FINITE_ANR_COMPONENTS; "FINITE_BALL",FINITE_BALL; @@ -4926,6 +4930,7 @@ theorems := "FINITE_CASES",FINITE_CASES; "FINITE_CBALL",FINITE_CBALL; "FINITE_CIRCLE_INTERSECTION",FINITE_CIRCLE_INTERSECTION; +"FINITE_CLAUSES",FINITE_CLAUSES; "FINITE_COLUMNS",FINITE_COLUMNS; "FINITE_COMPLEMENT_ANR_COMPONENTS",FINITE_COMPLEMENT_ANR_COMPONENTS; "FINITE_COMPLEMENT_ENR_COMPONENTS",FINITE_COMPLEMENT_ENR_COMPONENTS; @@ -5067,6 +5072,8 @@ theorems := "FINITE_T1_SPACE_IMP_DISCRETE_TOPOLOGY",FINITE_T1_SPACE_IMP_DISCRETE_TOPOLOGY; "FINITE_TOPSPACE_IMP_DISCRETE_TOPOLOGY",FINITE_TOPSPACE_IMP_DISCRETE_TOPOLOGY; "FINITE_TRANSITIVITY_CHAIN",FINITE_TRANSITIVITY_CHAIN; +"FINITE_TYBIT0",FINITE_TYBIT0; +"FINITE_TYBIT1",FINITE_TYBIT1; "FINITE_UNION",FINITE_UNION; "FINITE_UNIONS",FINITE_UNIONS; "FINITE_UNION_IMP",FINITE_UNION_IMP; @@ -6268,6 +6275,8 @@ theorems := "HAS_SIZE_SPHERE_2",HAS_SIZE_SPHERE_2; "HAS_SIZE_STDBASIS",HAS_SIZE_STDBASIS; "HAS_SIZE_SUC",HAS_SIZE_SUC; +"HAS_SIZE_TYBIT0",HAS_SIZE_TYBIT0; +"HAS_SIZE_TYBIT1",HAS_SIZE_TYBIT1; "HAS_SIZE_UNBOUNDED_COMPONENTS_COMPLEMENT",HAS_SIZE_UNBOUNDED_COMPONENTS_COMPLEMENT; "HAS_SIZE_UNBOUNDED_COMPONENTS_COMPLEMENT_1",HAS_SIZE_UNBOUNDED_COMPONENTS_COMPLEMENT_1; "HAS_SIZE_UNION",HAS_SIZE_UNION; @@ -6953,6 +6962,10 @@ theorems := "HYPERPLANE_FACET_OF_HALFSPACE_LE",HYPERPLANE_FACET_OF_HALFSPACE_LE; "HYPERPLANE_FACE_OF_HALFSPACE_GE",HYPERPLANE_FACE_OF_HALFSPACE_GE; "HYPERPLANE_FACE_OF_HALFSPACE_LE",HYPERPLANE_FACE_OF_HALFSPACE_LE; +"Hashek.hashek_def",Hashek.hashek_def; +"Hashek.hashek_eq",Hashek.hashek_eq; +"Hashek.hashek_prop",Hashek.hashek_prop; +"Hashek.hashek_thm",Hashek.hashek_thm; "IDEMPOTENT_IMP_RETRACTION",IDEMPOTENT_IMP_RETRACTION; "IDEMPOTENT_MATRIX_MUL_LINV",IDEMPOTENT_MATRIX_MUL_LINV; "IDEMPOTENT_MATRIX_MUL_RINV",IDEMPOTENT_MATRIX_MUL_RINV; @@ -9920,6 +9933,8 @@ theorems := "MOD_LE",MOD_LE; "MOD_LE_TWICE",MOD_LE_TWICE; "MOD_LT",MOD_LT; +"MOD_LT_EQ",MOD_LT_EQ; +"MOD_LT_EQ_LT",MOD_LT_EQ_LT; "MOD_MOD",MOD_MOD; "MOD_MOD_EXP_MIN",MOD_MOD_EXP_MIN; "MOD_MOD_LE",MOD_MOD_LE; @@ -14327,6 +14342,7 @@ theorems := "UNIV",UNIV; "UNIVERSAL_COVERING_SPACE",UNIVERSAL_COVERING_SPACE; "UNIV_GSPEC",UNIV_GSPEC; +"UNIV_HAS_SIZE_DIMINDEX",UNIV_HAS_SIZE_DIMINDEX; "UNIV_NOT_EMPTY",UNIV_NOT_EMPTY; "UNIV_PCROSS_UNIV",UNIV_PCROSS_UNIV; "UNIV_SECOND_COUNTABLE",UNIV_SECOND_COUNTABLE; @@ -15299,6 +15315,10 @@ theorems := "trivial_group",trivial_group; "trivial_homomorphism",trivial_homomorphism; "trivial_limit",trivial_limit; +"tybit0_INDUCT",tybit0_INDUCT; +"tybit0_RECURSION",tybit0_RECURSION; +"tybit1_INDUCT",tybit1_INDUCT; +"tybit1_RECURSION",tybit1_RECURSION; "uniformly_continuous_map",uniformly_continuous_map; "uniformly_continuous_on",uniformly_continuous_on; "vec",vec; diff --git a/arith.ml b/arith.ml index 30c4ecff..a8f28b31 100644 --- a/arith.ml +++ b/arith.ml @@ -6,6 +6,7 @@ (* (c) Copyright, University of Cambridge 1998 *) (* (c) Copyright, John Harrison 1998-2007 *) (* (c) Copyright, Marco Maggesi 2015 *) +(* (c) Copyright, Andrea Gabrielli, Marco Maggesi 2017-2018 *) (* ========================================================================= *) needs "recursion.ml";; @@ -1104,6 +1105,14 @@ let DIVISION_SIMP = prove ASM_SIMP_TAC[DIV_ZERO; MOD_ZERO; MULT_CLAUSES; ADD_CLAUSES] THEN ASM_MESON_TAC[DIVISION; MULT_SYM]);; +let MOD_LT_EQ = prove + (`!m n. m MOD n < n <=> ~(n = 0)`, + MESON_TAC[DIVISION; LE_1; CONJUNCT1 LT]);; + +let MOD_LT_EQ_LT = prove + (`!m n. m MOD n < n <=> 0 < n`, + MESON_TAC[DIVISION; LE_1; CONJUNCT1 LT]);; + let DIVMOD_UNIQ_LEMMA = prove (`!m n q1 r1 q2 r2. ((m = q1 * n + r1) /\ r1 < n) /\ ((m = q2 * n + r2) /\ r2 < n) @@ -1709,3 +1718,37 @@ let DEPENDENT_CHOICE = prove (?a. P 0 a) /\ (!n x. P n x ==> ?y. P (SUC n) y /\ R n x y) ==> ?f. (!n. P n (f n)) /\ (!n. R n (f n) (f(SUC n)))`, MESON_TAC[DEPENDENT_CHOICE_FIXED]);; + +(* ------------------------------------------------------------------------- *) +(* Conversion that elimimates every occurrence of `NUMERAL`, `BIT0`, *) +(* `BIT1`, `_0` that is not part of a well-formed numeral. *) +(* ------------------------------------------------------------------------- *) + +let BITS_ELIM_CONV : conv = + let NUMERAL_pth = prove(`m = n <=> NUMERAL m = n`,REWRITE_TAC[NUMERAL]) + and ZERO_pth = GSYM (REWRITE_CONV[NUMERAL] `0`) + and BIT0_pth,BIT1_pth = CONJ_PAIR + (prove(`(m = n <=> BIT0 m = 2 * n) /\ + (m = n <=> BIT1 m = 2 * n + 1)`, + CONJ_TAC THEN GEN_REWRITE_TAC (RAND_CONV o LAND_CONV) [BIT0; BIT1] THEN + REWRITE_TAC[ADD1; EQ_ADD_RCANCEL; GSYM MULT_2] THEN + REWRITE_TAC[EQ_MULT_LCANCEL] THEN + REWRITE_TAC[TWO; NOT_SUC])) + and mvar,nvar = `m:num`,`n:num` in + let rec BITS_ELIM_CONV : conv = + fun tm -> match tm with + Const("_0",_) -> ZERO_pth + | Var _ | Const _ -> REFL tm + | Comb(Const("NUMERAL",_),mtm) -> + if is_numeral tm then REFL tm else + let th = BITS_ELIM_CONV mtm in + EQ_MP (INST[mtm,mvar;rand(concl th),nvar] NUMERAL_pth) th + | Comb(Const("BIT0",_),mtm) -> + let th = BITS_ELIM_CONV mtm in + EQ_MP (INST [mtm,mvar;rand(concl th),nvar] BIT0_pth) th + | Comb(Const("BIT1",_),mtm) -> + let th = BITS_ELIM_CONV mtm in + EQ_MP (INST [mtm,mvar;rand(concl th),nvar] BIT1_pth) th + | Comb _ -> COMB_CONV BITS_ELIM_CONV tm + | Abs _ -> ABS_CONV BITS_ELIM_CONV tm in + BITS_ELIM_CONV;; diff --git a/basics.ml b/basics.ml index a7d716ca..3e13f6d9 100644 --- a/basics.ml +++ b/basics.ml @@ -5,6 +5,7 @@ (* *) (* (c) Copyright, University of Cambridge 1998 *) (* (c) Copyright, John Harrison 1998-2007 *) +(* (c) Copyright, Andrea Gabrielli, Marco Maggesi 2017-2018 *) (* ========================================================================= *) needs "fusion.ml";; @@ -390,6 +391,26 @@ let mk_let(assigs,bod) = let ltm = mk_const("LET",[ty1,aty; ty2,bty]) in list_mk_comb(ltm,lbod::rights);; +(* ------------------------------------------------------------------------- *) +(* Constructors and destructors for finite types. *) +(* ------------------------------------------------------------------------- *) + +let mk_finty:num->hol_type = + let rec finty n = + if n =/ num_1 then mk_type("1",[]) else + mk_type((if Num.mod_num n num_2 =/ num_0 then "tybit0" else "tybit1"), + [finty(Num.quo_num n num_2)]) in + fun n -> + if not(is_integer_num n) || n num = + function + Tyapp("1",_) -> num_1 + | Tyapp("tybit0",[ty]) -> dest_finty ty */ num_2 + | Tyapp("tybit1",[ty]) -> succ_num (dest_finty ty */ num_2) + | _ -> failwith "dest_finty";; + (* ------------------------------------------------------------------------- *) (* Useful function to create stylized arguments using numbers. *) (* ------------------------------------------------------------------------- *) diff --git a/cart.ml b/cart.ml index 3473fd8c..3689ef46 100644 --- a/cart.ml +++ b/cart.ml @@ -2,6 +2,7 @@ (* Definition of finite Cartesian product types. *) (* *) (* (c) Copyright, John Harrison 1998-2007 *) +(* (c) Copyright, Andrea Gabrielli, Marco Maggesi 2017-2018 *) (* ========================================================================= *) needs "iterate.ml";; @@ -30,6 +31,18 @@ let DIMINDEX_UNIQUE = prove (`(:A) HAS_SIZE n ==> dimindex(:A) = n`, MESON_TAC[dimindex; HAS_SIZE]);; +let UNIV_HAS_SIZE_DIMINDEX = prove + (`(:N) HAS_SIZE dimindex (:N) <=> FINITE(:N)`, + MESON_TAC[HAS_SIZE; dimindex]);; + +let HAS_SIZE_1 = prove + (`(:1) HAS_SIZE 1`, + SUBGOAL_THEN `(:1) = {one}` SUBST1_TAC THENL + [REWRITE_TAC[EXTENSION; IN_UNIV; IN_SING] THEN MESON_TAC[one]; + SIMP_TAC[NOT_IN_EMPTY; HAS_SIZE; FINITE_RULES; CARD_CLAUSES; ARITH]]);; + +let DIMINDEX_1 = MATCH_MP DIMINDEX_UNIQUE HAS_SIZE_1;; + (* ------------------------------------------------------------------------- *) (* An indexing type with that size, parametrized by base type. *) (* ------------------------------------------------------------------------- *) @@ -295,50 +308,146 @@ let DIMINDEX_FINITE_PROD = prove REWRITE_TAC[REWRITE_RULE[HAS_SIZE] DIMINDEX_HAS_SIZE_FINITE_PROD]);; (* ------------------------------------------------------------------------- *) -(* Automatically define a type of size n. *) +(* Type constructors for setting up finite types indexed by binary numbers. *) (* ------------------------------------------------------------------------- *) -let define_finite_type = - let lemma_pre = prove - (`~(n = 0) ==> ?x. x IN 1..n`, - DISCH_TAC THEN EXISTS_TAC `1` THEN REWRITE_TAC[IN_NUMSEG] THEN - POP_ASSUM MP_TAC THEN ARITH_TAC) - and lemma_post = prove - (`(!a:A. mk(dest a) = a) /\ (!r. r IN 1..n <=> dest(mk r) = r) - ==> (:A) HAS_SIZE n`, - REPEAT STRIP_TAC THEN - SUBGOAL_THEN `(:A) = IMAGE mk (1..n)` SUBST1_TAC THENL - [REWRITE_TAC[EXTENSION; IN_IMAGE; IN_UNIV]; - MATCH_MP_TAC HAS_SIZE_IMAGE_INJ] THEN - ASM_MESON_TAC[HAS_SIZE_NUMSEG_1]) in - let POST_RULE = MATCH_MP lemma_post and n_tm = `n:num` in - fun n -> - let ns = string_of_int n in - let ns' = "auto_define_finite_type_"^ns in - let th0 = INST [mk_small_numeral n,n_tm] lemma_pre in - let th1 = MP th0 (EQF_ELIM(NUM_EQ_CONV(rand(lhand(concl th0))))) in - POST_RULE(new_type_definition ns ("mk_"^ns',"dest_"^ns') th1);; +let tybit0_INDUCT,tybit0_RECURSION = define_type + "tybit0 = mktybit0((A,A)finite_sum)";; + +let tybit1_INDUCT,tybit1_RECURSION = define_type + "tybit1 = mktybit1(((A,A)finite_sum,1)finite_sum)";; + +let HAS_SIZE_TYBIT0 = prove + (`(:(A)tybit0) HAS_SIZE 2 * dimindex(:A)`, + SUBGOAL_THEN + `(:(A)tybit0) = IMAGE mktybit0 (:(A,A)finite_sum)` + SUBST1_TAC THENL + [CONV_TAC SYM_CONV THEN MATCH_MP_TAC SURJECTIVE_IMAGE_EQ THEN + REWRITE_TAC[IN_UNIV] THEN MESON_TAC[cases "tybit0"]; + MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN + REWRITE_TAC[IN_UNIV; injectivity "tybit0"] THEN + W(MP_TAC o PART_MATCH lhand + DIMINDEX_HAS_SIZE_FINITE_SUM o lhand o snd) THEN + REWRITE_TAC[DIMINDEX_FINITE_SUM; GSYM MULT_2]]);; + +let HAS_SIZE_TYBIT1 = prove + (`(:(A)tybit1) HAS_SIZE 2 * dimindex(:A) + 1`, + SUBGOAL_THEN + `(:(A)tybit1) = IMAGE mktybit1 (:((A,A)finite_sum,1)finite_sum)` + SUBST1_TAC THENL + [CONV_TAC SYM_CONV THEN MATCH_MP_TAC SURJECTIVE_IMAGE_EQ THEN + REWRITE_TAC[IN_UNIV] THEN MESON_TAC[cases "tybit1"]; + MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN + REWRITE_TAC[IN_UNIV; injectivity "tybit1"] THEN + W(MP_TAC o PART_MATCH lhand + DIMINDEX_HAS_SIZE_FINITE_SUM o lhand o snd) THEN + REWRITE_TAC[DIMINDEX_FINITE_SUM; DIMINDEX_1; GSYM MULT_2]]);; + +let DIMINDEX_TYBIT0 = prove + (`dimindex(:(A)tybit0) = 2 * dimindex(:A)`, + MATCH_MP_TAC DIMINDEX_UNIQUE THEN MATCH_ACCEPT_TAC HAS_SIZE_TYBIT0);; + +let DIMINDEX_TYBIT1 = prove + (`dimindex(:(A)tybit1) = 2 * dimindex(:A) + 1`, + MATCH_MP_TAC DIMINDEX_UNIQUE THEN MATCH_ACCEPT_TAC HAS_SIZE_TYBIT1);; + +let DIMINDEX_CLAUSES = prove + (`dimindex(:1) = 1 /\ + dimindex(:(A)tybit0) = 2 * dimindex(:A) /\ + dimindex(:(A)tybit1) = 2 * dimindex(:A) + 1`, + REWRITE_TAC[DIMINDEX_1] THEN CONJ_TAC THEN + MATCH_MP_TAC DIMINDEX_UNIQUE THEN + REWRITE_TAC[ HAS_SIZE_TYBIT0; HAS_SIZE_TYBIT1]);; + +let FINITE_1 = prove + (`FINITE (:1)`, + MESON_TAC[HAS_SIZE_1; HAS_SIZE]);; + +let FINITE_TYBIT0 = prove + (`FINITE (:A tybit0)`, + MESON_TAC[HAS_SIZE_TYBIT0; HAS_SIZE]);; + +let FINITE_TYBIT1 = prove + (`FINITE (:A tybit1)`, + MESON_TAC[HAS_SIZE_TYBIT1; HAS_SIZE]);; + +let FINITE_CLAUSES = prove + (`FINITE(:1) /\ FINITE(:A tybit0) /\ FINITE(:A tybit1)`, + REWRITE_TAC[FINITE_1; FINITE_TYBIT0; FINITE_TYBIT1]);; (* ------------------------------------------------------------------------- *) -(* Predefine the cases 2, 3 and 4, which are especially useful for real^N. *) +(* Computing dimindex of fintypes. *) (* ------------------------------------------------------------------------- *) -let HAS_SIZE_1 = prove - (`(:1) HAS_SIZE 1`, - SUBGOAL_THEN `(:1) = {one}` SUBST1_TAC THENL - [REWRITE_TAC[EXTENSION; IN_UNIV; IN_SING] THEN MESON_TAC[one]; - SIMP_TAC[NOT_IN_EMPTY; HAS_SIZE; FINITE_RULES; CARD_CLAUSES; ARITH]]);; +let DIMINDEX_CONV : conv = + let [pth_num;pth0;pth1;pth_one] = (CONJUNCTS o prove) + (`(dimindex(:A) = n <=> dimindex(s:A->bool) = NUMERAL n) /\ + (dimindex(:A) = n <=> dimindex(:A tybit0) = BIT0 n) /\ + (dimindex(:A) = n <=> dimindex(:A tybit1) = BIT1 n) /\ + dimindex(:1) = BIT1 _0`, + CONJ_TAC THENL [REWRITE_TAC[NUMERAL; dimindex]; ALL_TAC] THEN + REWRITE_TAC[DIMINDEX_CLAUSES] THEN CONV_TAC BITS_ELIM_CONV THEN + ARITH_TAC) in + let nvar = `n:num` in + let rec calc_dimindex ty = + match ty with + Tyapp("1",_) -> pth_one + | Tyapp("tybit0",ty'::_) -> + let th = calc_dimindex ty' in + let n = rand(concl th) in + EQ_MP (INST [n,nvar] (INST_TYPE [ty',aty] pth0)) th + | Tyapp("tybit1",ty'::_) -> + let th = calc_dimindex ty' in + let n = rand(concl th) in + EQ_MP (INST [n,nvar] (INST_TYPE [ty',aty] pth1)) th + | _ -> fail() in + function + Comb(Const("dimindex",_),tm) -> + let uty = type_of tm in + let _,(sty::_) = dest_type uty in + let th = calc_dimindex sty in + let svar = mk_var("s",uty) + and ntm = rand(concl th) in + let pth = INST [tm,svar;ntm,nvar] (INST_TYPE [sty,aty] pth_num) in + EQ_MP pth th + | _ -> failwith "DIMINDEX_CONV";; + +let HAS_SIZE_DIMINDEX_RULE = + let pth = prove + (`(:A) HAS_SIZE n <=> FINITE(:A) /\ dimindex(:A) = n`, + MESON_TAC[UNIV_HAS_SIZE_DIMINDEX; HAS_SIZE]) in + let htm = `(HAS_SIZE) (:A)` + and conv = GEN_REWRITE_CONV I [pth] + and rule = EQT_ELIM o GEN_REWRITE_CONV I [FINITE_CLAUSES] in + fun nty -> + let tm = mk_comb(inst[nty,aty] htm,mk_numeral (dest_finty nty)) in + let th1 = conv tm in + EQ_MP (SYM th1) + (CONJ (rule (lhand(rand(concl th1)))) + (DIMINDEX_CONV (lhand(rand(rand(concl th1))))));; + +let DIMINDEX_TAC : tactic = + CONV_TAC (ONCE_DEPTH_CONV DIMINDEX_CONV);; -let HAS_SIZE_2 = define_finite_type 2;; +(* ------------------------------------------------------------------------- *) +(* Remember cases 2, 3 and 4, which are especially useful for real^N. *) +(* ------------------------------------------------------------------------- *) -let HAS_SIZE_3 = define_finite_type 3;; +let DIMINDEX_2 = prove + (`dimindex (:2) = 2`, + DIMINDEX_TAC THEN REFL_TAC);; -let HAS_SIZE_4 = define_finite_type 4;; +let DIMINDEX_3 = prove + (`dimindex (:3) = 3`, + DIMINDEX_TAC THEN REFL_TAC);; -let DIMINDEX_1 = MATCH_MP DIMINDEX_UNIQUE HAS_SIZE_1;; -let DIMINDEX_2 = MATCH_MP DIMINDEX_UNIQUE HAS_SIZE_2;; -let DIMINDEX_3 = MATCH_MP DIMINDEX_UNIQUE HAS_SIZE_3;; -let DIMINDEX_4 = MATCH_MP DIMINDEX_UNIQUE HAS_SIZE_4;; +let DIMINDEX_4 = prove + (`dimindex (:4) = 4`, + DIMINDEX_TAC THEN REFL_TAC);; + +let HAS_SIZE_2 = HAS_SIZE_DIMINDEX_RULE `:2`;; +let HAS_SIZE_3 = HAS_SIZE_DIMINDEX_RULE `:3`;; +let HAS_SIZE_4 = HAS_SIZE_DIMINDEX_RULE `:4`;; (* ------------------------------------------------------------------------- *) (* Finiteness lemma. *) diff --git a/database.ml b/database.ml index 3a91b85f..173a583d 100644 --- a/database.ml +++ b/database.ml @@ -258,6 +258,7 @@ theorems := "DIMINDEX_2",DIMINDEX_2; "DIMINDEX_3",DIMINDEX_3; "DIMINDEX_4",DIMINDEX_4; +"DIMINDEX_CLAUSES",DIMINDEX_CLAUSES; "DIMINDEX_FINITE_DIFF",DIMINDEX_FINITE_DIFF; "DIMINDEX_FINITE_IMAGE",DIMINDEX_FINITE_IMAGE; "DIMINDEX_FINITE_PROD",DIMINDEX_FINITE_PROD; @@ -267,6 +268,8 @@ theorems := "DIMINDEX_HAS_SIZE_FINITE_PROD",DIMINDEX_HAS_SIZE_FINITE_PROD; "DIMINDEX_HAS_SIZE_FINITE_SUM",DIMINDEX_HAS_SIZE_FINITE_SUM; "DIMINDEX_NONZERO",DIMINDEX_NONZERO; +"DIMINDEX_TYBIT0",DIMINDEX_TYBIT0; +"DIMINDEX_TYBIT1",DIMINDEX_TYBIT1; "DIMINDEX_UNIQUE",DIMINDEX_UNIQUE; "DIMINDEX_UNIV",DIMINDEX_UNIV; "DISJOINT",DISJOINT; @@ -456,10 +459,12 @@ theorems := "FILTER",FILTER; "FILTER_APPEND",FILTER_APPEND; "FILTER_MAP",FILTER_MAP; +"FINITE_1",FINITE_1; "FINITE_BOOL",FINITE_BOOL; "FINITE_CART",FINITE_CART; "FINITE_CART_UNIV",FINITE_CART_UNIV; "FINITE_CASES",FINITE_CASES; +"FINITE_CLAUSES",FINITE_CLAUSES; "FINITE_CROSS",FINITE_CROSS; "FINITE_CROSS_EQ",FINITE_CROSS_EQ; "FINITE_DELETE",FINITE_DELETE; @@ -531,6 +536,8 @@ theorems := "FINITE_SUPPORT",FINITE_SUPPORT; "FINITE_SUPPORT_DELTA",FINITE_SUPPORT_DELTA; "FINITE_TRANSITIVITY_CHAIN",FINITE_TRANSITIVITY_CHAIN; +"FINITE_TYBIT0",FINITE_TYBIT0; +"FINITE_TYBIT1",FINITE_TYBIT1; "FINITE_UNION",FINITE_UNION; "FINITE_UNIONS",FINITE_UNIONS; "FINITE_UNION_IMP",FINITE_UNION_IMP; @@ -639,6 +646,8 @@ theorems := "HAS_SIZE_PRODUCT_DEPENDENT",HAS_SIZE_PRODUCT_DEPENDENT; "HAS_SIZE_SET_OF_LIST",HAS_SIZE_SET_OF_LIST; "HAS_SIZE_SUC",HAS_SIZE_SUC; +"HAS_SIZE_TYBIT0",HAS_SIZE_TYBIT0; +"HAS_SIZE_TYBIT1",HAS_SIZE_TYBIT1; "HAS_SIZE_UNION",HAS_SIZE_UNION; "HAS_SIZE_UNIONS",HAS_SIZE_UNIONS; "HAS_SUP",HAS_SUP; @@ -683,6 +692,10 @@ theorems := "HREAL_OF_NUM_EQ",HREAL_OF_NUM_EQ; "HREAL_OF_NUM_LE",HREAL_OF_NUM_LE; "HREAL_OF_NUM_MUL",HREAL_OF_NUM_MUL; +"Hashek.hashek_def",Hashek.hashek_def; +"Hashek.hashek_eq",Hashek.hashek_eq; +"Hashek.hashek_prop",Hashek.hashek_prop; +"Hashek.hashek_thm",Hashek.hashek_thm; "IMAGE",IMAGE; "IMAGE_CLAUSES",IMAGE_CLAUSES; "IMAGE_CONST",IMAGE_CONST; @@ -1369,6 +1382,8 @@ theorems := "MOD_LE",MOD_LE; "MOD_LE_TWICE",MOD_LE_TWICE; "MOD_LT",MOD_LT; +"MOD_LT_EQ",MOD_LT_EQ; +"MOD_LT_EQ_LT",MOD_LT_EQ_LT; "MOD_MOD",MOD_MOD; "MOD_MOD_EXP_MIN",MOD_MOD_EXP_MIN; "MOD_MOD_LE",MOD_MOD_LE; @@ -2468,6 +2483,7 @@ theorems := "UNIQUE_SKOLEM_THM",UNIQUE_SKOLEM_THM; "UNIV",UNIV; "UNIV_GSPEC",UNIV_GSPEC; +"UNIV_HAS_SIZE_DIMINDEX",UNIV_HAS_SIZE_DIMINDEX; "UNIV_NOT_EMPTY",UNIV_NOT_EMPTY; "UNIV_PCROSS_UNIV",UNIV_PCROSS_UNIV; "UNIV_SUBSET",UNIV_SUBSET; @@ -2700,5 +2716,9 @@ theorems := "treal_mul",treal_mul; "treal_neg",treal_neg; "treal_of_num",treal_of_num; +"tybit0_INDUCT",tybit0_INDUCT; +"tybit0_RECURSION",tybit0_RECURSION; +"tybit1_INDUCT",tybit1_INDUCT; +"tybit1_RECURSION",tybit1_RECURSION; "vector",vector ];; diff --git a/equal.ml b/equal.ml index 311a667e..7db9f47a 100644 --- a/equal.ml +++ b/equal.ml @@ -82,7 +82,7 @@ let GEN_ALPHA_CONV v tm = let b,abs = dest_comb tm in AP_TERM b (ALPHA_CONV v abs);; -let MK_BINOP op = +let MK_BINOP op = let afn = AP_TERM op in fun (lth,rth) -> MK_COMB(afn lth,rth);; @@ -138,15 +138,15 @@ let (RATOR_CONV:conv->conv) = let (RAND_CONV:conv->conv) = fun conv tm -> - match tm with - Comb(l,r) -> MK_COMB(REFL l,conv r) + match tm with + Comb(l,r) -> MK_COMB(REFL l,conv r) | _ -> failwith "RAND_CONV: Not a combination";; let LAND_CONV = RATOR_CONV o RAND_CONV;; let (COMB2_CONV: conv->conv->conv) = - fun lconv rconv tm -> - match tm with + fun lconv rconv tm -> + match tm with Comb(l,r) -> MK_COMB(lconv l,rconv r) | _ -> failwith "COMB2_CONV: Not a combination";; @@ -176,10 +176,17 @@ let SUB_CONV conv tm = | Abs(_,_) -> ABS_CONV conv tm | _ -> REFL tm;; -let BINOP_CONV conv tm = - let lop,r = dest_comb tm in - let op,l = dest_comb lop in - MK_COMB(AP_TERM op (conv l),conv r);; +let (BINOP_CONV:conv->conv) = + fun conv tm -> + let lop,r = dest_comb tm in + let op,l = dest_comb lop in + MK_COMB(AP_TERM op (conv l),conv r);; + +let (BINOP2_CONV:conv->conv->conv) = + fun conv1 conv2 tm -> + let lop,r = dest_comb tm in + let op,l = dest_comb lop in + MK_COMB(AP_TERM op (conv1 l),conv2 r);; (* ------------------------------------------------------------------------- *) (* Depth conversions; internal use of a failure-propagating `Boultonized' *) @@ -202,11 +209,11 @@ let (ONCE_DEPTH_CONV: conv->conv), with Failure _ -> th1 and COMB_QCONV conv tm = match tm with - Comb(l,r) -> + Comb(l,r) -> (try let th1 = conv l in try let th2 = conv r in MK_COMB(th1,th2) with Failure _ -> AP_THM th1 r - with Failure _ -> AP_TERM l (conv r)) + with Failure _ -> AP_TERM l (conv r)) | _ -> failwith "COMB_QCONV: Not a combination" in let rec REPEATQC conv tm = THENCQC conv (REPEATQC conv) tm in let SUB_QCONV conv tm = diff --git a/parser.ml b/parser.ml index d74f0e9c..4836fb46 100644 --- a/parser.ml +++ b/parser.ml @@ -5,6 +5,7 @@ (* *) (* (c) Copyright, University of Cambridge 1998 *) (* (c) Copyright, John Harrison 1998-2007 *) +(* (c) Copyright, Andrea Gabrielli, Marco Maggesi 2017-2018 *) (* ========================================================================= *) needs "preterm.ml";; @@ -178,6 +179,14 @@ let lex = (* ------------------------------------------------------------------------- *) let parse_pretype = + let mk_prefinty:num->pretype = + let rec prefinty n = + if n =/ num_1 then Ptycon("1",[]) else + let c = if Num.mod_num n num_2 =/ num_0 then "tybit0" else "tybit1" in + Ptycon(c,[prefinty(Num.quo_num n num_2)]) in + fun n -> + if not(is_integer_num n) || n (try pretype_of_type(assoc s (type_abbrevs())) with Failure _ -> + try mk_prefinty (num_of_string s) with Failure _ -> if try get_type_arity s = 0 with Failure _ -> false then Ptycon(s,[]) else Utv(s)),rest | _ -> raise Noparse @@ -196,7 +206,8 @@ let parse_pretype = (Ident s)::rest -> if try get_type_arity s > 0 with Failure _ -> false then s,rest else raise Noparse | _ -> raise Noparse in - let rec pretype i = rightbin sumtype (a (Resword "->")) (btyop "fun") "type" i + let rec pretype i = + rightbin sumtype (a (Resword "->")) (btyop "fun") "type" i and sumtype i = rightbin prodtype (a (Ident "+")) (btyop "sum") "type" i and prodtype i = rightbin carttype (a (Ident "#")) (btyop "prod") "type" i and carttype i = leftbin apptype (a (Ident "^")) (btyop "cart") "type" i diff --git a/printer.ml b/printer.ml index b51c54f4..9d6fb44a 100644 --- a/printer.ml +++ b/printer.ml @@ -6,6 +6,7 @@ (* (c) Copyright, University of Cambridge 1998 *) (* (c) Copyright, John Harrison 1998-2007 *) (* (c) Copyright, Marco Maggesi 2017 *) +(* (c) Copyright, Andrea Gabrielli, Marco Maggesi 2017-2018 *) (* ========================================================================= *) needs "nets.ml";; @@ -163,6 +164,7 @@ let pp_print_type,pp_print_qtype = if flag then "("^s^")" else s in let rec sot pr ty = try dest_vartype ty with Failure _ -> + try string_of_num(dest_finty ty) with Failure _ -> match dest_type ty with con,[] -> con | "fun",[ty1;ty2] -> soc "->" (pr > 0) [sot 1 ty1; sot 0 ty2]