.gitattributes

+*.ml linguist-language=OCaml
+*.hl linguist-language=OCaml
\ No newline at end of file

.gitignore

-*~
+.DS_Store
+*.cmi
+*.cmo
+*.o
+*.cmx
+pa_j.ml
+update_database.ml
\ No newline at end of file

100/cayley_hamilton.ml

@@ -3,9 +3,10 @@
 (* ========================================================================= *)
 
 needs "Multivariate/complexes.ml";;
+needs "Multivariate/msum.ml";;
 
 (* ------------------------------------------------------------------------- *)
-(* Powers of a square matrix (mpow) and sums of matrices (msum).             *)
+(* Powers of a square matrix (mpow).                                         *)
 (* ------------------------------------------------------------------------- *)
 
 parse_as_infix("mpow",(24,"left"));;
@@ -14,118 +15,6 @@ let mpow = define
   `(!A:real^N^N. A mpow 0 = (mat 1 :real^N^N)) /\
    (!A:real^N^N n. A mpow (SUC n) = A ** A mpow n)`;;
 
-let msum = new_definition
- `msum = iterate (matrix_add)`;;
-
-let NEUTRAL_MATRIX_ADD = prove
- (`neutral((+):real^N^M->real^N^M->real^N^M) = mat 0`,
-  REWRITE_TAC[neutral] THEN MATCH_MP_TAC SELECT_UNIQUE THEN
-  MESON_TAC[MATRIX_ADD_RID; MATRIX_ADD_LID]);;
-
-let MONOIDAL_MATRIX_ADD = prove
- (`monoidal((+):real^N^M->real^N^M->real^N^M)`,
-  REWRITE_TAC[monoidal; NEUTRAL_MATRIX_ADD] THEN
-  REWRITE_TAC[MATRIX_ADD_LID; MATRIX_ADD_ASSOC] THEN
-  REWRITE_TAC[MATRIX_ADD_SYM]);;
-
-let MSUM_CLAUSES = prove
- (`(!(f:A->real^N^M). msum {} f = mat 0) /\
-   (!x (f:A->real^N^M) s.
-        FINITE(s)
-        ==> (msum (x INSERT s) f =
-             if x IN s then msum s f else f(x) + msum s f))`,
-  REWRITE_TAC[msum; GSYM NEUTRAL_MATRIX_ADD] THEN
-  ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
-  MATCH_MP_TAC ITERATE_CLAUSES THEN REWRITE_TAC[MONOIDAL_MATRIX_ADD]);;
-
-let MSUM_MATRIX_RMUL = prove
- (`!(f:A->real^N^M) (A:real^P^N) s.
-        FINITE s ==> msum s (\i. f(i) ** A) = msum s f ** A`,
-  GEN_TAC THEN GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
-  SIMP_TAC[MSUM_CLAUSES; MATRIX_MUL_LZERO; MATRIX_ADD_RDISTRIB]);;
-
-let MSUM_MATRIX_LMUL = prove
- (`!(f:A->real^P^N) (A:real^N^M) s.
-        FINITE s ==> msum s (\i. A ** f(i)) = A ** msum s f`,
-  GEN_TAC THEN GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
-  SIMP_TAC[MSUM_CLAUSES; MATRIX_MUL_RZERO; MATRIX_ADD_LDISTRIB]);;
-
-let MSUM_ADD = prove
- (`!f g s. FINITE s ==> (msum s (\x. f(x) + g(x)) = msum s f + msum s g)`,
-  SIMP_TAC[msum; ITERATE_OP; MONOIDAL_MATRIX_ADD]);;
-
-let MSUM_CMUL = prove
- (`!(f:A->real^N^M) c s.
-        FINITE s ==>  msum s (\i. c %% f(i)) = c %% msum s f`,
-  GEN_TAC THEN GEN_TAC THEN MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
-  SIMP_TAC[MSUM_CLAUSES; MATRIX_CMUL_ADD_LDISTRIB; MATRIX_CMUL_RZERO]);;
-
-let MSUM_NEG = prove
- (`!(f:A->real^N^M) s.
-        FINITE s ==>  msum s (\i. --(f(i))) = --(msum s f)`,
-  ONCE_REWRITE_TAC[MATRIX_NEG_MINUS1] THEN
-  REWRITE_TAC[MSUM_CMUL]);;
-
-let MSUM_SUB = prove
- (`!f g s. FINITE s ==> (msum s (\x. f(x) - g(x)) = msum s f - msum s g)`,
-  REWRITE_TAC[MATRIX_SUB; MATRIX_NEG_MINUS1] THEN
-  SIMP_TAC[MSUM_ADD; MSUM_CMUL]);;
-
-let MSUM_CLAUSES_LEFT = prove
- (`!f m n. m <= n ==> msum(m..n) f = f(m) + msum(m+1..n) f`,
-  SIMP_TAC[GSYM NUMSEG_LREC; MSUM_CLAUSES; FINITE_NUMSEG; IN_NUMSEG] THEN
-  ARITH_TAC);;
-
-let MSUM_SUPPORT = prove
- (`!f s. msum (support (+) f s) f = msum s f`,
-  SIMP_TAC[msum; iterate; SUPPORT_SUPPORT]);;
-
-let MSUM_EQ = prove
- (`!f g s. (!x. x IN s ==> (f x = g x)) ==> (msum s f = msum s g)`,
-  REWRITE_TAC[msum] THEN
-  MATCH_MP_TAC ITERATE_EQ THEN REWRITE_TAC[MONOIDAL_MATRIX_ADD]);;
-
-let MSUM_RESTRICT_SET = prove
- (`!P s f. msum {x:A | x IN s /\ P x} f =
-           msum s (\x. if P x then f(x) else mat 0)`,
-  REWRITE_TAC[msum; GSYM NEUTRAL_MATRIX_ADD] THEN
-  MATCH_MP_TAC ITERATE_RESTRICT_SET THEN REWRITE_TAC[MONOIDAL_MATRIX_ADD]);;
-
-let MSUM_SING = prove
- (`!f x. msum {x} f = f(x)`,
-  SIMP_TAC[MSUM_CLAUSES; FINITE_RULES; NOT_IN_EMPTY; MATRIX_ADD_RID]);;
-
-let MSUM_IMAGE = prove
- (`!f g s. (!x y. x IN s /\ y IN s /\ (f x = f y) ==> (x = y))
-           ==> (msum (IMAGE f s) g = msum s (g o f))`,
-  REWRITE_TAC[msum; GSYM NEUTRAL_MATRIX_ADD] THEN
-  MATCH_MP_TAC ITERATE_IMAGE THEN REWRITE_TAC[MONOIDAL_MATRIX_ADD]);;
-
-let MSUM_OFFSET = prove
- (`!p f m n. msum(m+p..n+p) f = msum(m..n) (\i. f(i + p))`,
-  SIMP_TAC[NUMSEG_OFFSET_IMAGE; MSUM_IMAGE; EQ_ADD_RCANCEL; FINITE_NUMSEG] THEN
-  REWRITE_TAC[o_DEF]);;
-
-let MSUM_COMPONENT = prove
- (`!f:A->real^N^M i j s.
-        1 <= i /\ i <= dimindex(:M) /\
-        1 <= j /\ j <= dimindex(:N) /\
-        FINITE s
-        ==> (msum s f)$i$j = sum s (\a. f(a)$i$j)`,
-  REPLICATE_TAC 3 GEN_TAC THEN
-  REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
-  REPEAT DISCH_TAC THEN
-  MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
-  SIMP_TAC[MSUM_CLAUSES; SUM_CLAUSES] THEN
-  ASM_SIMP_TAC[MATRIX_ADD_COMPONENT; MAT_COMPONENT; COND_ID]);;
-
-let MSUM_CLAUSES_NUMSEG = prove
- (`(!m. msum(m..0) f = if m = 0 then f(0) else mat 0) /\
-   (!m n. msum(m..SUC n) f = if m <= SUC n then msum(m..n) f + f(SUC n)
-                             else msum(m..n) f)`,
-  REWRITE_TAC[MATCH_MP ITERATE_CLAUSES_NUMSEG MONOIDAL_MATRIX_ADD;
-              NEUTRAL_MATRIX_ADD; msum]);;
-
 let MPOW_ADD = prove
  (`!A:real^N^N m n. A mpow (m + n) = A mpow m ** A mpow n`,
   GEN_TAC THEN INDUCT_TAC THEN
@@ -415,7 +304,7 @@ let MATRIC_CHARPOLY_DIFFERENCE = prove
       REWRITE_TAC[GSYM MSUM_RESTRICT_SET; IN_NUMSEG] THEN
       REWRITE_TAC[numseg; ARITH_RULE
        `(0 <= i /\ i <= n) /\ i <= n - 1 <=> 0 <= i /\ i <= n - 1`];
-      SIMP_TAC[GSYM MSUM_CMUL; FINITE_NUMSEG; MATRIX_CMUL_ASSOC] THEN
+      SIMP_TAC[GSYM MSUM_LMUL; FINITE_NUMSEG; MATRIX_CMUL_ASSOC] THEN
       REWRITE_TAC[REAL_MUL_SYM]]]);;
 
 let CAYLEY_HAMILTON = prove

Boyer_Moore/README

                             BOYER-MOORE AUTOMATION
 
-(c) Richard Boulton, University of Edinburgh, University of Cambridge, INRIA 1994
+(c) University of Edinburgh, University of Cambridge, INRIA 1994
 (c) Petros Papapanagiotou & Jacques Fleuriot, University of Edinburgh 2007-2017
 
 All code in this directory is distributed under the same license as

Examples/lucas_lehmer.ml

@@ -63,7 +63,7 @@ let LLSEQ_CLOSEDFORM = prove
      [ALL_TAC;
       ASM_SIMP_TAC[ARITH_RULE
        `2 <= x /\ ~(p = 0) /\ ~(p = 1) ==> x + p - 2 = (x - 2) + p`]] THEN
-    FIRST_ASSUM(fun t -> ONCE_REWRITE_TAC[GSYM(MATCH_MP MOD_ADD_MOD t)]) THENL
+    ONCE_REWRITE_TAC[GSYM MOD_ADD_MOD] THENL
      [ASM_MESON_TAC[MOD_EXP_MOD];
       ASM_SIMP_TAC[MOD_REFL; ADD_CLAUSES; MOD_MOD_REFL]];
     ASM_SIMP_TAC[GSYM REAL_OF_NUM_SUB; GSYM REAL_OF_NUM_POW] THEN

Formal_ineqs/arith/arith_num.hl

@@ -538,7 +538,7 @@ let gen_bi_eq_bj =
                        SUBGOAL_THEN `~(b = 0)` ASSUME_TAC THENL [POP_ASSUM MP_TAC THEN ARITH_TAC; ALL_TAC] THEN
                        REWRITE_TAC[CONTRAPOS_THM] THEN
                        DISCH_TAC THEN FIRST_ASSUM (MP_TAC o AP_TERM `\x. x DIV b`) THEN REWRITE_TAC[] THEN
-		       FIRST_ASSUM (MP_TAC o MATCH_MP DIV_MULT_ADD) THEN
+                       FIRST_ASSUM (MP_TAC o MATCH_MP(CONJUNCT1 DIV_MULT_ADD)) THEN
                        DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
                        SUBGOAL_THEN `i DIV b = 0 /\ j DIV b = 0` (fun th -> REWRITE_TAC[th]) THENL
                          [

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

Geometric_Algebra/README

+Formulation of geometric algebra G(P,Q,R) with the multivector structure
+(P,Q,R)multivector, which can formulate positive definite, negative definite
+and zero quadratic forms.
+
+      (c) Copyright, Capital Normal University, China, 2018.
+  Authors: Liming Li, Zhiping Shi, Yong Guan, Guohui Wang, Sha Ma.
+
+     Distributed with HOL Light under the same license terms

Geometric_Algebra/make.ml

+(* ========================================================================= *)
+(* Load geometric algebra theory plus complex/quaternions application        *)
+(*                                                                           *)
+(*        (c) Copyright, Capital Normal University, China, 2018.             *)
+(*     Authors: Liming Li, Zhiping Shi, Yong Guan, Guohui Wang, Sha Ma.      *)
+(* ========================================================================= *)
+
+loadt "Geometric_Algebra/geometricalgebra.ml";;
+loadt "Geometric_Algebra/quaternions.ml";;

Geometric_Algebra/quaternions.ml

+(* ========================================================================= *)
+(* Complex numbers and quaternions in the geometric algebra theory.          *)
+(*                                                                           *)
+(*        (c) Copyright, Capital Normal University, China, 2018.             *)
+(*     Authors: Liming Li, Zhiping Shi, Yong Guan, Guohui Wang, Sha Ma.      *)
+(* ========================================================================= *)
+
+needs "Geometric_Algebra/geometricalgebra.ml";;
+needs "Quaternions/make.ml";;
+
+(* ------------------------------------------------------------------------- *)
+(* Complexes in GA.                                                          *)
+(* ------------------------------------------------------------------------- *)
+
+let DIMINDEX_GA010 = prove
+ (`dimindex(:('0,'1,'0)geomalg) = dimindex(:2)`,
+  REWRITE_TAC[DIMINDEX_2; DIMINDEX_GEOMALG; PDIMINDEX_0; PDIMINDEX_1] THEN ARITH_TAC);;
+
+let COMPLEX_PRODUCT_GA010 = prove
+ (`!x y:real^('0,'1,'0)geomalg.
+     x * y =
+       (x $$ {} * y $$ {} - x $$ {1} * y $$ {1}) % mbasis {} +
+       (x $$ {} * y $$ {1} + x $$ {1} * y $$ {}) % mbasis {1}`,
+  REPEAT GEN_TAC THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[GSYM MVBASIS_EXPANSION] THEN
+  GEN_REWRITE_TAC(LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[GSYM MVBASIS_EXPANSION] THEN
+  REWRITE_TAC[PDIMINDEX_0; PDIMINDEX_1; ADD_0; ADD_SYM; NUMSEG_SING] THEN
+  REWRITE_TAC[prove(`{s | s SUBSET {1}} = {{}, {1}}`, REWRITE_TAC[POWERSET_CLAUSES] THEN SET_TAC[])] THEN
+  SIMP_TAC[VSUM_CLAUSES;FINITE_INSERT; FINITE_SING; IN_INSERT; IN_SING; NOT_EMPTY_INSERT; VSUM_SING] THEN
+  CONV_TAC GEOM_ARITH);;
+
+GEOM_ARITH `mbasis{1}:real^('0,'1,'0)geomalg * mbasis{1} = --mbasis{}`;;
+GEOM_ARITH `mbasis{1,2}:real^('2,'0,'0)geomalg * mbasis{1,2} = --mbasis{}`;;
+
+(* ------------------------------------------------------------------------- *)
+(* Quaternions in GA.                                                        *)
+(* ------------------------------------------------------------------------- *)
+
+let DIMINDEX_GA020 = prove
+ (`dimindex(:('0,'2,'0)geomalg) = dimindex(:4)`,
+  REWRITE_TAC[DIMINDEX_4; DIMINDEX_GEOMALG; PDIMINDEX_0; PDIMINDEX_2] THEN ARITH_TAC);;
+
+let QUAT_PRODUCT_GA020 = prove
+ (`!x y:real^('0,'2,'0)geomalg.
+     x * y =
+       (x $$ {} * y $$ {} - x $$ {1} * y $$ {1} - x $$ {2} * y $$ {2} - x $$ {1,2} * y $$ {1,2}) % mbasis {} +
+       (x $$ {} * y $$ {1} + x $$ {1} * y $$ {} + x $$ {2} * y $$ {1,2} - x $$ {1,2} * y $$ {2}) % mbasis {1} +
+       (x $$ {} * y $$ {2} - x $$ {1} * y $$ {1,2} + x $$ {2} * y $$ {} + x $$ {1,2} * y $$ {1}) % mbasis {2} +
+       (x $$ {} * y $$ {1,2} + x $$ {1} * y $$ {2} - x $$ {2} * y $$ {1} + x $$ {1,2} * y $$ {}) % mbasis {1,2}`,
+  REPEAT GEN_TAC THEN GEN_REWRITE_TAC(LAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)[GSYM MVBASIS_EXPANSION] THEN
+  GEN_REWRITE_TAC(LAND_CONV o RAND_CONV o ONCE_DEPTH_CONV)[GSYM MVBASIS_EXPANSION] THEN
+  REWRITE_TAC[PDIMINDEX_0; PDIMINDEX_2; ADD_0; ADD_SYM] THEN
+  GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[TWO] THEN REWRITE_TAC[NUMSEG_CLAUSES] THEN REWRITE_TAC[ARITH; NUMSEG_SING] THEN
+  REWRITE_TAC[prove(`{s | s SUBSET {2,1}} = {{}, {1}, {2}, {1,2}}`,
+     REWRITE_TAC[POWERSET_CLAUSES] THEN REWRITE_TAC[EXTENSION] THEN
+     GEN_TAC THEN REWRITE_TAC[IN_UNION; IN_IMAGE; IN_INSERT; NOT_IN_EMPTY] THEN REWRITE_TAC[GSYM DISJ_ASSOC] THEN
+     MATCH_MP_TAC (TAUT `p1 = q1 /\ p2 = q2 ==> (p1 \/ p2) = (q1 \/q2)`) THEN CONJ_TAC THENL[SET_TAC[]; ALL_TAC] THEN
+     MATCH_MP_TAC (TAUT `p1 = q1 /\ p2 = q2 ==> (p1 \/ p2) = (q1 \/q2)`) THEN CONJ_TAC THEN
+     EQ_TAC THENL[SET_TAC[]; ALL_TAC; SET_TAC[]; ALL_TAC] THEN STRIP_TAC THENL
+      [EXISTS_TAC `{}:num->bool`; EXISTS_TAC `{}:num->bool`; EXISTS_TAC `{1}:num->bool`] THEN ASM_REWRITE_TAC[] THEN
+     CONJ_TAC THENL[SET_TAC[]; ALL_TAC] THEN DISJ2_TAC THEN EXISTS_TAC `{}:num->bool` THEN ASM_REWRITE_TAC[])] THEN
+  SIMP_TAC[VSUM_CLAUSES; FINITE_INSERT; FINITE_SING; IN_INSERT; IN_SING; NOT_EMPTY_INSERT; VSUM_SING] THEN
+  SIMP_TAC[EXTENSION; IN_INSERT; NOT_IN_EMPTY] THEN
+  REWRITE_TAC[prove(`!a b:num. (!x. (x=a) <=> (x=b)) <=> (a=b)`, MESON_TAC[]);
+              prove(`!a b:num. (!x. (x=a) <=> (x=a) \/ (x=b)) <=> (a=b)`, MESON_TAC[]);
+              DISJ_SYM; ARITH_EQ] THEN
+  CONV_TAC GEOM_ARITH);;
+
+GEOM_ARITH `(mbasis{1}:real^('0,'2,'0)geomalg)* mbasis{1} = --mbasis{}`;;
+GEOM_ARITH `(mbasis{2}:real^('0,'2,'0)geomalg)* mbasis{2} = --mbasis {}`;;
+GEOM_ARITH `(mbasis{1,2}:real^('0,'2,'0)geomalg)* mbasis{1,2} = --mbasis {}`;;
+GEOM_ARITH `(mbasis{1}:real^('0,'2,'0)geomalg)* mbasis{2} = mbasis {1,2}`;;
+GEOM_ARITH `(mbasis{2}:real^('0,'2,'0)geomalg)* mbasis{1,2} = mbasis {1}`;;
+GEOM_ARITH `(mbasis{1,2}:real^('0,'2,'0)geomalg)* mbasis{1} = mbasis {2}`;;
+GEOM_ARITH `(mbasis{1}:real^('0,'2,'0)geomalg)* mbasis{2} = --(mbasis{2} * mbasis{1})`;;
+GEOM_ARITH `(mbasis{2}:real^('0,'2,'0)geomalg)* mbasis{1,2} = --(mbasis{1,2} * mbasis {2})`;;
+GEOM_ARITH `(mbasis{1,2}:real^('0,'2,'0)geomalg)* mbasis{1} = --(mbasis{1} * mbasis{1,2})`;;
+GEOM_ARITH `(mbasis{1}:real^('0,'2,'0)geomalg)* mbasis{2} * mbasis{1,2} = --mbasis{}`;;
+
+let geomalg_300_quat = new_definition
+`geomalg_300_quat (q:quat) =
+  (Re q) % mbasis{} +
+  (Im1 q) % mbasis{2,3} +
+  (Im2 q) % mbasis{1,2} +
+  (Im3 q) % (--(mbasis{1,3}:real^('3,'0,'0)geomalg))`;;
+
+let CNJ_QUAT = prove
+(`!q:quat. conjugation (geomalg_300_quat q) = geomalg_300_quat (cnj q)`,
+  GEN_TAC THEN REWRITE_TAC[conjugation; geomalg_300_quat; quat_cnj; QUAT_COMPONENTS] THEN
+  SIMP_TAC[GEOMALG_BETA; GEOMALG_EQ] THEN
+  REPEAT STRIP_TAC THEN
+  ASM_SIMP_TAC[VECTOR_NEG_MINUS1; GEOMALG_ADD_COMPONENT; GEOMALG_MUL_COMPONENT; MVBASIS_COMPONENT] THEN
+  REWRITE_TAC[REAL_ADD_LDISTRIB] THEN
+  ASM_SIMP_TAC[MVBASIS_COMPONENT] THEN
+  BINOP_TAC THENL
+   [COND_CASES_TAC THEN ASM_REWRITE_TAC[PDIMINDEX_3; PDIMINDEX_0] THEN
+    REWRITE_TAC[ARITH; (NUMSEG_CONV `4..3`); INTER_EMPTY] THEN
+    CONV_TAC REVERSION_CONV THEN REAL_ARITH_TAC; ALL_TAC] THEN
+  BINOP_TAC THENL
+   [COND_CASES_TAC THEN ASM_REWRITE_TAC[PDIMINDEX_3; PDIMINDEX_0] THEN
+    REWRITE_TAC[ARITH; (NUMSEG_CONV `4..3`); INTER_EMPTY] THEN
+    CONV_TAC REVERSION_CONV THEN REAL_ARITH_TAC THEN REAL_ARITH_TAC; ALL_TAC] THEN
+  BINOP_TAC THENL
+   [COND_CASES_TAC THEN ASM_REWRITE_TAC[PDIMINDEX_3; PDIMINDEX_0] THEN
+    REWRITE_TAC[ARITH; (NUMSEG_CONV `4..3`); INTER_EMPTY] THEN
+    CONV_TAC REVERSION_CONV THEN REAL_ARITH_TAC THEN REAL_ARITH_TAC; ALL_TAC] THEN
+  COND_CASES_TAC THEN ASM_REWRITE_TAC[PDIMINDEX_3; PDIMINDEX_0] THEN
+    REWRITE_TAC[ARITH; (NUMSEG_CONV `4..3`); INTER_EMPTY] THEN
+    CONV_TAC REVERSION_CONV THEN REAL_ARITH_TAC THEN REAL_ARITH_TAC);;
+
+GEOM_ARITH `(mbasis{2,3}:real^('3,'0,'0)geomalg)* mbasis{2,3} = --mbasis{}`;;
+GEOM_ARITH `(mbasis{1,2}:real^('3,'0,'0)geomalg)* mbasis{1,2} = --mbasis{}`;;
+GEOM_ARITH `(--mbasis{1,3}:real^('3,'0,'0)geomalg)*(--mbasis{1,3}) = --mbasis{}`;;
+GEOM_ARITH `(mbasis{2,3}:real^('3,'0,'0)geomalg)* mbasis {1,2} = --mbasis{1,3}`;;
+GEOM_ARITH `(mbasis{1,2}:real^('3,'0,'0)geomalg)*(--mbasis{1,3}) = mbasis{2,3}`;;
+GEOM_ARITH `(--mbasis{1,3}:real^('3,'0,'0)geomalg)* mbasis{2,3} = mbasis{1,2}`;;
+GEOM_ARITH `(mbasis{2,3}:real^('3,'0,'0)geomalg)* mbasis{1,2} = --(mbasis{1,2} * mbasis{2,3})`;;
+GEOM_ARITH `(mbasis{1,2}:real^('3,'0,'0)geomalg)*(--mbasis{1,3})= --(--mbasis{1,3} * mbasis{1,2})`;;
+GEOM_ARITH `(--mbasis{1,3}:real^('3,'0,'0)geomalg)* mbasis{2,3} = --(mbasis{2,3} * --mbasis{1,3})`;;
+GEOM_ARITH `(mbasis{2,3}:real^('3,'0,'0)geomalg)* mbasis{1,2} * --mbasis{1,3} = --mbasis{}`;;
+
+(* ------------------------------------------------------------------------- *)
+(* Dual quaternions in GA.                                                   *)
+(* ------------------------------------------------------------------------- *)
+
+GEOM_ARITH `(mbasis{2,3}:real^('3,'0,'1)geomalg)* mbasis{2,3} = --mbasis{}`;;
+GEOM_ARITH `(mbasis{1,2}:real^('3,'0,'1)geomalg)* mbasis{1,2} = --mbasis{}`;;
+GEOM_ARITH `(--mbasis{1,3}:real^('3,'0,'1)geomalg)*(--mbasis{1,3}) = --mbasis{}`;;
+GEOM_ARITH `(mbasis{2,3}:real^('3,'0,'1)geomalg)* mbasis {1,2} = --mbasis{1,3}`;;
+GEOM_ARITH `(mbasis{1,2}:real^('3,'0,'1)geomalg)*(--mbasis{1,3}) = mbasis{2,3}`;;
+GEOM_ARITH `(--mbasis{1,3}:real^('3,'0,'1)geomalg)* mbasis{2,3} = mbasis{1,2}`;;
+GEOM_ARITH `(mbasis{2,3}:real^('3,'0,'1)geomalg)* mbasis{1,2} = --(mbasis{1,2} * mbasis{2,3})`;;
+GEOM_ARITH `(mbasis{1,2}:real^('3,'0,'1)geomalg)*(--mbasis{1,3})= --(--mbasis{1,3} * mbasis{1,2})`;;
+GEOM_ARITH `(--mbasis{1,3}:real^('3,'0,'1)geomalg)* mbasis{2,3} = --(mbasis{2,3} * --mbasis{1,3})`;;
+GEOM_ARITH `(mbasis{2,3}:real^('3,'0,'1)geomalg)* mbasis{1,2} * --mbasis{1,3} = --mbasis{}`;;
+GEOM_ARITH `mbasis{2,3}:real^('3,'0,'1)geomalg * mbasis{1,2,3,4} = mbasis{1,2,3,4} * mbasis{2,3}`;;
+GEOM_ARITH `mbasis{1,2}:real^('3,'0,'1)geomalg * mbasis{1,2,3,4} = mbasis{1,2,3,4} * mbasis{1,2}`;;
+GEOM_ARITH `--mbasis{1,3}:real^('3,'0,'1)geomalg * mbasis{1,2,3,4}= mbasis{1,2,3,4}* --mbasis{1,3}`;;
+GEOM_ARITH `mbasis{1,2,3,4}:real^('3,'0,'1)geomalg * mbasis{1,2,3,4} = vec 0`;;

Help/BINOP2_CONV.doc

+\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

Help/BINOP_CONV.doc

 \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 
+{|- 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.
 
@@ -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

Help/BITS_ELIM_CONV.doc

+\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

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

Help/COMB_CONV.doc

@@ -17,6 +17,6 @@ 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

Help/DIMINDEX_CONV.doc

+\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