Skip to content

Commit

Permalink
Added a complete replacement, from Andrea Gabrielli and Marco Maggesi,
Browse files Browse the repository at this point in the history 
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
  • Loading branch information
@jrh13
jrh13 committed Jan 7, 2019
1 parent 5f7cab7 commit a84e0f3
Show file tree
Hide file tree
Showing 26 changed files with 673 additions and 140 deletions.
102 changes: 70 additions & 32 deletions CHANGES
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -17,173 +55,173 @@ 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)
==> group_isomorphism
(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
==> group_isomorphism
(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
==> (h subgroup_of quotient_group G n <=>
(?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
==> (?k. k subgroup_of G /\
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

Expand Down
8 changes: 4 additions & 4 deletions Formal_ineqs/taylor/m_taylor.hl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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));;
Expand Down Expand Up @@ -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;;


(**********************)
Expand Down Expand Up @@ -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 *)
Expand Down Expand Up @@ -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
Expand Down
33 changes: 33 additions & 0 deletions Help/BINOP2_CONV.doc
View file
Original file line number Diff line number Diff line change
@@ -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
14 changes: 7 additions & 7 deletions Help/BINOP_CONV.doc
View file
Original file line number Diff line number Diff line change
@@ -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
Expand All @@ -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
35 changes: 35 additions & 0 deletions Help/BITS_ELIM_CONV.doc
View file
Original file line number Diff line number Diff line change
@@ -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
Loading

0 comments on commit a84e0f3

Please sign in to comment.