simon.foster
  • Joined on Dec 06, 2019

simon.foster pushed to master at Isabelle_DOF/Isabelle_DOF

  • 1839afa883 Added proofs that quantities from a real normed vector space

2 years ago

simon.foster pushed to master at Isabelle_DOF/Isabelle_DOF

2 years ago

simon.foster pushed to master at Isabelle_DOF/Isabelle_DOF

  • 4b605faa2d Improved proof support. Added some proofs of the astronomical constants.

2 years ago

simon.foster pushed to master at Isabelle_DOF/Isabelle_DOF

  • 31c0dd56e8 Some renaming, cleaning, and addition of astronomical units

2 years ago

simon.foster pushed to master at Isabelle_DOF/Isabelle_DOF

  • 25f2c76f1b Restructured the document into the ISQ and SI parts

2 years ago

simon.foster pushed to master at Isabelle_DOF/Isabelle_DOF

  • 0c73aa1ce7 Commented on the relationship between units and quantities, and added several supporting definitions and types.

2 years ago

simon.foster pushed to master at Isabelle_DOF/Isabelle_DOF

  • cf10043680 A few more revisions and explanations.

2 years ago

simon.foster pushed to master at Isabelle_DOF/Isabelle_DOF

  • 1e31cbb8a1 Some fixes and improvements for proof support

2 years ago

simon.foster pushed to master at Isabelle_DOF/Isabelle_DOF

  • 6feaeee050 More refactoring. The mechanisation is now split conveniently into a quantity and unit part. Most of the technical foundations

2 years ago

simon.foster pushed to master at Isabelle_DOF/Isabelle_DOF

  • da74d4ecc4 Revision of the narrative in Dimensions and Quantities

2 years ago

simon.foster pushed to master at Isabelle_DOF/Isabelle_DOF

2 years ago

simon.foster pushed to master at Isabelle_DOF/Isabelle_DOF

  • 3fa136ec72 A few additional properties and proofs

2 years ago

simon.foster pushed to master at Isabelle_DOF/Isabelle_DOF

2 years ago

simon.foster pushed to master at Isabelle_DOF/Isabelle_DOF

  • e1d4079c0f Renamed Unit to Dimension. Added several more definitions and results from the standard.

2 years ago

simon.foster pushed to master at Isabelle_DOF/Isabelle_DOF

  • c40088199c Some tidying of the proof strategy and derived properties

2 years ago

simon.foster pushed to master at Isabelle_DOF/Isabelle_DOF

  • 240c10eb58 Factored out definitions, and added several additional units

3 years ago

simon.foster pushed to master at Isabelle_DOF/Isabelle_DOF

  • 583637859a Cleaning up the proof procedure, and additional algebraic laws

3 years ago

simon.foster pushed to master at Isabelle_DOF/Isabelle_DOF

  • b8e347b4c8 Removed the scalar product and associated class instantiations in favour of scaleQ

3 years ago

simon.foster pushed to master at Isabelle_DOF/Isabelle_DOF

  • c104f1e2b2 Added the the scaleQ function that should allow removal of the scalar product operator

3 years ago

simon.foster pushed to master at Isabelle_DOF/Isabelle_DOF

  • 2c63ef07e9 Added core physical constants of the 2019 SI standard, dimensionless units, and various proof facilities for support.

3 years ago