Hi Developer,
my interest is to guess list operation and surface operation in many valued
logic
however, there is no result when search artificial intelligence to guess
list operation.
then i found that Isabelle can derive list operation with Lemma,
I have created 3 valued logic, however, i
I believe Florian's proposal is good. On a proof-engineering level, the
only "inconvinience" is mainly that the property
gcd a b * lcm a b = a * b
does not hold as such but generally I suspect in the form
gcd a b * lcm a b = normalize(a * b) -- The normalize in GCD.thy perhaps
has the property
Florian has already hinted at it, but I will say it again explicitly:
Mathematically, gcd and lcm are not operations on the elements of a
ring, but on the equivalence classes w.r.t. associatedness (i.e. mutual
divisibility). In fact, these equivalence classes form a complete
lattice w.r.t.
Very good! This is very convenient.
On 01/06/16 21:42, Makarius wrote:
*** ML ***
* Structure Rat for rational numbers is now an integral part of
Isabelle/ML, with special notation @int/nat or @int for numerals (an
abbreviation for antiquotation @{Pure.rat argument}) and ML pretty
printing.