Updated the files in RichterHilbertAxiomGeometry to match Bill
Richter's current version. Thanks to a reminder from Hendrik Tews
about the debian package, the README file now also has a proper
copyright statement.

Made some updates in the Multivariate theories. Generalized the
notions of "has_bounded_variation_on" and "vector_variation" to
real^1->real^N functions and generalized many of the theorems
to this context. Made a separate generalization of the theorem
ABSOLUTELY_INTEGRABLE_BOUNDED_SETVARIATION so it applies to
integrability on arbitrary sets. Made this the basis of definitions
of "rectifiable_path" and "path_length". Also added a few new
unrelated results like ABSOLUTELY_INTEGRABLE_APPROXIMATE_CONTINUOUS.
Here are the new theorems:

        ABSOLUTELY_INTEGRABLE_APPROXIMATE_CONTINUOUS
        ABSOLUTELY_INTEGRABLE_BOUNDED_SETVARIATION_EQ
        ABSOLUTELY_INTEGRABLE_ON_CONST
        BOUNDED_COMPONENTWISE
        BOUNDED_RECTIFIABLE_PATH_IMAGE
        CONTINUOUS_DISCRETE_RANGE_CONSTANT_EQ
        CONTINUOUS_FINITE_RANGE_CONSTANT
        CONTINUOUS_FINITE_RANGE_CONSTANT_EQ
        CONTINUOUS_IMP_MEASURABLE_ON_LEBESGUE_MEASURABLE_SUBSET
        DECREASING_BOUNDED_VARIATION
        DECREASING_VECTOR_VARIATION
        DIVISION_OF_AFFINITY
        DIVISION_OF_REFLECT
        FORALL_IN_DIVISION_NONEMPTY
        HAS_BOUNDED_REAL_VARIATION_AFFINITY2_EQ
        HAS_BOUNDED_REAL_VARIATION_AFFINITY_EQ
        HAS_BOUNDED_REAL_VARIATION_ON_EQ
        HAS_BOUNDED_REAL_VARIATION_REFLECT2_EQ
        HAS_BOUNDED_REAL_VARIATION_REFLECT_EQ
        HAS_BOUNDED_REAL_VARIATION_REFLECT_EQ_INTERVAL
        HAS_BOUNDED_REAL_VARIATION_TRANSLATION2_EQ
        HAS_BOUNDED_REAL_VARIATION_TRANSLATION_EQ
        HAS_BOUNDED_REAL_VARIATION_TRANSLATION_EQ_INTERVAL
        HAS_BOUNDED_SETVARIATION_ON_0
        HAS_BOUNDED_SETVARIATION_ON_COMPONENTWISE
        HAS_BOUNDED_SETVARIATION_ON_EQ
        HAS_BOUNDED_SETVARIATION_REFLECT2_EQ
        HAS_BOUNDED_SETVARIATION_TRANSLATION2_EQ
        HAS_BOUNDED_VARIATION_ABSOLUTELY_INTEGRABLE_DERIVATIVE
        HAS_BOUNDED_VARIATION_AFFINITY2_EQ
        HAS_BOUNDED_VARIATION_AFFINITY_EQ
        HAS_BOUNDED_VARIATION_COMPOSE_DECREASING
        HAS_BOUNDED_VARIATION_COMPOSE_INCREASING
        HAS_BOUNDED_VARIATION_INTEGRABLE_NORM_DERIVATIVE
        HAS_BOUNDED_VARIATION_ON_COMPONENTWISE
        HAS_BOUNDED_VARIATION_ON_CONST
        HAS_BOUNDED_VARIATION_ON_EQ
        HAS_BOUNDED_VARIATION_ON_ID
        HAS_BOUNDED_VARIATION_ON_LINEAR_IMAGE
        HAS_BOUNDED_VARIATION_ON_REFLECT
        HAS_BOUNDED_VARIATION_ON_REFLECT_INTERVAL
        HAS_BOUNDED_VARIATION_REFLECT2_EQ
        HAS_BOUNDED_VARIATION_REFLECT_EQ
        HAS_BOUNDED_VARIATION_REFLECT_EQ_INTERVAL
        HAS_BOUNDED_VARIATION_TRANSLATION2_EQ
        HAS_BOUNDED_VARIATION_TRANSLATION_EQ
        HAS_BOUNDED_VARIATION_TRANSLATION_EQ_INTERVAL
        IN_REAL_INTERVAL_REFLECT
        LEBESGUE_MEASURABLE_CONVEX
        LEBESGUE_MEASURABLE_JORDAN
        LINEAR_1
        LINEAR_MATRIX_EXISTS
        MEASURABLE_ON_COUNTABLE_UNIONS
        MEASURABLE_ON_DIFF
        MEASURABLE_ON_EMPTY
        MEASURABLE_ON_INTER
        MEASURABLE_ON_TRANSLATION
        MEASURABLE_ON_TRANSLATION_EQ
        MEASURABLE_ON_UNION
        MEASURABLE_ON_UNIONS
        MEASURABLE_ON_VECTOR_DERIVATIVE
        NEGLIGIBLE_IMP_LEBESGUE_MEASURABLE
        NEGLIGIBLE_IMP_MEASURABLE
        NORM_1
        NORM_1_POS
        PATH_LENGTH_REVERSEPATH
        REAL_VARIATION_AFFINITY
        REAL_VARIATION_AFFINITY2
        REAL_VARIATION_REFLECT
        REAL_VARIATION_REFLECT2
        REAL_VARIATION_REFLECT_INTERVAL
        REAL_VARIATION_TRANSLATION
        REAL_VARIATION_TRANSLATION2
        REAL_VARIATION_TRANSLATION_INTERVAL
        RECTIFIABLE_PATH_IMP_PATH
        RECTIFIABLE_PATH_LINEPATH
        RECTIFIABLE_PATH_REVERSEPATH
        RECTIFIABLE_PATH_SUBPATH
        REFLECT_INTERVAL
        REFLECT_REAL_INTERVAL
        SETVARIATION_EQUAL_LEMMA
        SET_VARIATION_0
        SET_VARIATION_REFLECT2
        SET_VARIATION_TRANSLATION2
        VARIATION_EQUAL_LEMMA
        VECTOR_VARIATION_AFFINITY
        VECTOR_VARIATION_AFFINITY2
        VECTOR_VARIATION_CONST
        VECTOR_VARIATION_REFLECT
        VECTOR_VARIATION_REFLECT2
        VECTOR_VARIATION_REFLECT_INTERVAL
        VECTOR_VARIATION_TRANSLATION
        VECTOR_VARIATION_TRANSLATION2
        VECTOR_VARIATION_TRANSLATION_INTERVAL
        path_length
        rectifiable_path



git-svn-id: http://hol-light.googlecode.com/svn@151 1eddc5a6-173b-11df-bff1-5f4ea15f2b7c
Reshuffled a few preliminaries between interface files so that
printer.ml can be loaded before the other two. This is a prelude to
putting in code from Vincent Aravantinos for better error messages
from typechecking.

At the suggestion of Petros Papapanagiotou, made a theorem-tactic form
STRUCT_CASES_THEN of STRUCT_CASES_TAC.

Update IsabelleLight and RichterHilbertAxiomGeometry in line with
newer versions from their authors.

Added a number of basic lemmas about cardinalities of finite universe
sets and a few more about countable sets. In the Multivariate
theories, generalized FUNDAMENTAL_THEOREM_OF_CALCULUS_STRONG from a
finite set of exceptional points to a countable set (using a technical
lemma TAGGED_PARTIAL_DIVISION_COMMON_TAGS), and generalized several
other consequences, as well as adding a few additional results
connected with variation and path length. The complete list of new
theorems is:

        ABSOLUTELY_INTEGRABLE_SET_VARIATION
        CARD_BOOL
        CARD_CART_UNIV
        CARD_FUNSPACE_UNIV
        COUNTABLE_IMAGE_INJ
        COUNTABLE_IMAGE_INJ_EQ
        COUNTABLE_IMAGE_INJ_GENERAL
        DIVISION_COMMON_POINT_BOUND
        FINITE_BOOL
        FINITE_CART_UNIV
        FINITE_FUNSPACE_UNIV
        HAS_SIZE_BOOL
        HAS_SIZE_CART_UNIV
        HAS_SIZE_FUNSPACE_UNIV
        PATH_LENGTH_DIFFERENTIABLE
        PATH_LENGTH_JOIN
        RECTIFIABLE_PATH_DIFFERENTIABLE
        RECTIFIABLE_PATH_JOIN
        RECTIFIABLE_PATH_JOIN_EQ
        RECTIFIABLE_PATH_JOIN_IMP
        SET_VARIATION_EQ
        TAGGED_PARTIAL_DIVISION_COMMON_POINT_BOUND
        TAGGED_PARTIAL_DIVISION_COMMON_TAGS
        UNIV_GSPEC
        VECTOR_VARIATION_EQ
        VECTOR_VARIATION_INTEGRAL_NORM_DERIVATIVE



git-svn-id: http://hol-light.googlecode.com/svn@152 1eddc5a6-173b-11df-bff1-5f4ea15f2b7c
Added a miscellany of theorems, mostly in the Multivariate theories:

        ABS_SQUARE_EQ_1
        BETWEEN_COLLINEAR_DIST_EQ
        BETWEEN_DIST_LE
        BETWEEN_DIST_LT
        BETWEEN_EXISTS_EXTENSION
        BETWEEN_NORM_LE
        BETWEEN_NORM_LT
        BILINEAR_DOT
        CONTINUOUS_AT_LIFT_DOT2
        CONTINUOUS_INJECTIVE_IFF_MONOTONIC
        CONTINUOUS_INJECTIVE_IMAGE_SEGMENT_1
        CONTINUOUS_WITHIN_LIFT_DOT2
        CONVEX_CONTAINS_SEGMENT_EQ
        DEPENDENT_2
        DEPENDENT_3
        DEPENDENT_SING
        INDEPENDENT_SING
        INJECTIVE_ALT
        INJECTIVE_ON_ALT
        INVERTIBLE_MATRIX_MUL
        MIDPOINT_BETWEEN
        MOEBIUS_FUNCTION_SIMPLE
        ORTHOGONAL_LVSUM
        ORTHOGONAL_RVSUM
        PATH_LENGTH_VALID_PATH
        REAL_CONTINUOUS_INJECTIVE_IFF_MONOTONIC
        REAL_LT_LSQRT
        RECTIFIABLE_VALID_PATH
        SPAN_EQ_INSERT
        SUBSET_CONTINUOUS_IMAGE_SEGMENT_1

as well as a few more in Multivariate/flyspeck.ml

        ARG_DIV_EQ_SUBSET_HALFLINE
        ARG_EQ_SUBSET_HALFLINE
        COPLANAR_AZIM_EQ



git-svn-id: http://hol-light.googlecode.com/svn@153 1eddc5a6-173b-11df-bff1-5f4ea15f2b7c
Updated the typechecker with a new version from Vincent Aravantinos
that gives more useful error messages when typechecking fails.

Added four new tactic constructs from Marco Maggesi. HYP is analogous
to ASM but restricting to named (labelled) assumptions. DESTRUCT_TAC,
FIX_TAC and INTRO_TAC give more concise and elegant ways of fixing
variables, performing introduction on a goal or elimination on a
theorem, labelling assumptions in the process.

Extended the regular quotation parser to pass quotations of the form
`;....` to miz3's "parse_qproof". This makes it more convenient to
load files with miz3 proofs in without first setting up the new parser
before the file is loaded.

Added two files showing Tarski's 11 axioms for geometry hold in the
Euclidean plane but all except axiom 10 hold in the Klein model of the
hyperbolic plane. This effectively proves the independence of the
parallel postulate.

Split the file "Multivariate/convex.ml" (which was getting rather
large and unwieldy) into two, introducing a new file named
"Multivariate/paths.ml" for stuff related to paths, homotopy etc.
Generalized existing theorems NORM_LE_PASTECART (avoiding pointless
type over-specialization), RIGID_TRANSFORMATION_BETWEEN_CONGRUENT_SETS
(now uses an arbitrary indexing set instead of a matrix to represent a
set of pairs of points) and NEGLIGIBLE_LIPSCHITZ_IMAGE (proved with a
sharper and more useful alternation of quantifiers). Removed
NEGLIGIBLE_LIPSCHITZ_IMAGE_BOUNDED, which now seems redundant. Added
various new theorems and a couple of new definitions, mainly in the
Multivariate theories:

        BILINEAR_DIFFERENTIABLE_AT_COMPOSE
        BILINEAR_DIFFERENTIABLE_ON_COMPOSE
        BILINEAR_DIFFERENTIABLE_WITHIN_COMPOSE
        BOUNDED_PASTECART_EQ
        CARD_EQ_CLOSED_SETS
        CARD_EQ_OPEN_SETS
        CLOSED_PASTECART_EQ
        CLOSED_UNION_COMPACT_SUBSETS
        COMPACT_PASTECART_EQ
        CONDENSATION_POINT_IMP_LIMPT
        CONDENSATION_POINT_INFINITE_BALL
        CONDENSATION_POINT_INFINITE_CBALL
        CONNECTED_PASTECART_EQ
        CONTINUOUS_MIDPOINT_CONVEX
        CONTINUOUS_WITHIN_OPEN
        CONVEX_LOWER_SEGMENT
        CONVEX_MAX
        CONVEX_NORM
        CONVEX_ON_EPIGRAPH_SLICE_LE
        CONVEX_ON_EPIGRAPH_SLICE_LT
        DIFFERENTIABLE_AT_LIFT_DOT2
        DIFFERENTIABLE_LINEAR
        DIFFERENTIABLE_ON_LIFT_DOT2
        DIFFERENTIABLE_WITHIN_LIFT_DOT2
        DIFF_UNIONS_NONEMPTY
        INFINITE_FROM
        IN_CLOSURE_DELETE
        LEBESGUE_MEASURABLE_CONTINUOUS_IMAGE
        LEBESGUE_MEASURABLE_DIFFERENTIABLE_IMAGE
        LEBESGUE_MEASURABLE_LEBESGUE_MEASURABLE_PREIMAGE_CLOSED
        LEBESGUE_MEASURABLE_LEBESGUE_MEASURABLE_PREIMAGE_OPEN
        LEBESGUE_MEASURABLE_REGULAR_INNER
        LEBESGUE_MEASURABLE_REGULAR_OUTER
        LIMPT_INFINITE_BALL
        LIMPT_INFINITE_CBALL
        LIMPT_INFINITE_OPEN
        LIMPT_OF_CLOSURE
        LIMPT_OF_LIMPTS
        LIMPT_SEQUENTIAL_INJ
        LINEAR_SUBSPACE_GRAPH
        LUZIN
        LUZIN_EQ
        LUZIN_EQ_ALT
        MEASURABLE_COUNTABLE_INTERS_GEN
        MEASURABLE_MEASURABLE_PREIMAGE_CLOSED
        MEASURABLE_MEASURABLE_PREIMAGE_OPEN
        MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_CLOSED
        MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_CLOSED_EQ
        MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_CLOSED_INTERVAL
        MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_OPEN
        MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_OPEN_EQ
        MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_OPEN_HALFSPACE_COMPONENT_GE
        MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_OPEN_HALFSPACE_COMPONENT_GT
        MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_OPEN_HALFSPACE_COMPONENT_LE
        MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_OPEN_HALFSPACE_COMPONENT_LT
        MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_OPEN_INTERVAL
        MEASURABLE_ON_MEASURABLE_PREIMAGE_CLOSED
        MEASURABLE_ON_MEASURABLE_PREIMAGE_CLOSED_EQ
        MEASURABLE_ON_MEASURABLE_PREIMAGE_CLOSED_INTERVAL
        MEASURABLE_ON_MEASURABLE_PREIMAGE_OPEN
        MEASURABLE_ON_MEASURABLE_PREIMAGE_OPEN_EQ
        MEASURABLE_ON_MEASURABLE_PREIMAGE_OPEN_HALFSPACE_COMPONENT_GE
        MEASURABLE_ON_MEASURABLE_PREIMAGE_OPEN_HALFSPACE_COMPONENT_GT
        MEASURABLE_ON_MEASURABLE_PREIMAGE_OPEN_HALFSPACE_COMPONENT_LE
        MEASURABLE_ON_MEASURABLE_PREIMAGE_OPEN_HALFSPACE_COMPONENT_LT
        MEASURABLE_ON_MEASURABLE_PREIMAGE_OPEN_INTERVAL
        MIDPOINT_CONVEX_DYADIC_RATIONALS
        NEGLIGIBLE_DIFFERENTIABLE_IMAGE_LOWDIM
        NEGLIGIBLE_DIFFERENTIABLE_IMAGE_NEGLIGIBLE
        NEGLIGIBLE_IFF_LEBESGUE_MEASURABLE_SUBSETS
        NEGLIGIBLE_IFF_MEASURABLE_SUBSETS
        NEGLIGIBLE_VALID_PATH_IMAGE
        OEP
        ONORM_I
        ONORM_ID
        OPEN_PASTECART_EQ
        PASTECART_INJ
        PRESERVES_LEBESGUE_MEASURABLE_IMP_PRESERVES_NEGLIGIBLE
        RATIONAL_BETWEEN
        RIGID_TRANSFORMATION_BETWEEN_CONGRUENT_SETS_STRONG
        SAME_DISTANCES_TO_AFFINE_HULL
        SUBSET_INTERS
        UNIONS_DIFF
        condensation_point_of
        toset



git-svn-id: http://hol-light.googlecode.com/svn@154 1eddc5a6-173b-11df-bff1-5f4ea15f2b7c
Added an update from Vincent Aravantinos to handle an additional case of
typechecking errors. Fixed a documentation bug for HYP.

Type-generalized the following theorems to a range of type real^N:

  VECTOR_VARIATION_GE_NORM_FUNCTION
  VECTOR_VARIATION_GE_DROP_FUNCTION
  REAL_VARIATION_GE_ABS_FUNCTION
  REAL_VARIATION_GE_FUNCTION

as well as removing an unnecessary hypothesis from REAL_MEASURE_MEASURE
and renaming OPEN_OPEN_PROJECTION to OPEN_OPEN_LEFT_PROJECTION. Added a
miscellany of additional theorems:

        APPEND_SING
        BABY_SARD
        CARD_EQ_CLOSED
        CARD_EQ_COMPACT_SETS
        CARD_EQ_CONDENSATION_POINTS
        CARD_EQ_CONDENSATION_POINTS_IN_SET
        CARD_EQ_NONEMPTY_INTERIOR
        CLOSED_AS_FRONTIER
        CLOSED_AS_FRONTIER_OF_SUBSET
        CLOSED_CONDENSATION_POINTS
        CLOSED_LIMPTS
        CLOSURE_COCOUNTABLE_COORDINATES
        CLOSURE_COSMALL_COORDINATES
        CLOSURE_INTERIOR_IDEMP
        CLOSURE_IRRATIONAL_COORDINATES
        CLOSURE_PASTECART
        COCOUNTABLE_APPROXIMATION
        CONDENSATION_POINTS_EQ_EMPTY
        COSMALL_APPROXIMATION
        COUNTABLE_NON_CONDENSATION_POINTS
        DIAMETER_LE
        DIVIDES_EXP_MINUS1
        DIVIDES_EXP_PLUS1
        DROP_IN_IMAGE_DROP
        EXISTS_DROP_IMAGE
        EXISTS_LIFT_IMAGE
        FORALL_DROP_IMAGE
        FORALL_LIFT_IMAGE
        FRONTIER_FRONTIER_FRONTIER
        FRONTIER_FRONTIER_SUBSET
        IMAGE_LIFT_REAL_SEGMENT
        INTERIOR_CLOSURE_IDEMP
        INTERIOR_FRONTIER
        INTERIOR_FRONTIER_EMPTY
        INTERIOR_MAXIMAL_EQ
        INTERIOR_PASTECART
        IRRATIONAL_APPROXIMATION
        LIMPT_OF_CONDENSATION_POINTS
        LIMPT_PASTECART
        LIM_NORM
        MEASURABLE_INSERT
        MEASURE_BALL_BOUND
        MEASURE_CBALL_BOUND
        MEASURE_INSERT
        MEM_APPEND_DECOMPOSE
        MEM_APPEND_DECOMPOSE_LEFT
        NEGLIGIBLE_IMAGE_BOUNDED_VARIATION_INTERVAL
        NEGLIGIBLE_RECTIBIABLE_PATH_IMAGE
        OPEN_OPEN_RIGHT_PROJECTION
        OPEN_SET_COCOUNTABLE_COORDINATES
        OPEN_SET_COSMALL_COORDINATES
        OPEN_SET_IRRATIONAL_COORDINATES
        PERMUTED_APPEND_SWAP
        PRIME_DIVEXP_EQ
        PRIME_POWER_EXISTS
        PRODUCT_CLAUSES_LEFT
        PRODUCT_CLAUSES_RIGHT
        REAL_NEGLIGIBLE_OUTER
        REAL_NEGLIGIBLE_OUTER_LE
        SUBSET_DROP_IMAGE
        SUBSET_LIFT_IMAGE
        TAGGED_DIVISION_UNION_IMAGE_SND
        UNCOUNTABLE_HAS_CONDENSATION_POINT
        UNCOUNTABLE_NONEMPTY_INTERIOR
        UNCOUNTABLE_OPEN
        UNIONS_MONO
        UNIONS_MONO_IMAGE
        UNION_INTERIOR_SUBSET
        VECTOR_VARIATION_ON_NULL



git-svn-id: http://hol-light.googlecode.com/svn@155 1eddc5a6-173b-11df-bff1-5f4ea15f2b7c