ASSUME NEW CONSTANT m \in Nat \ {0},NEW CONSTANT n \in Nat \ {0},n > mPROVE \A i \in Int :(\E q \in Int : m = i * q) /\ (\E q \in Int : n = i * q)<=> (\E q \in Int : m = i * q) /\ (\E q \in Int : n - m = i * q)
Btw, why this module defines Divides and DivisorOf over all Int instead of a subset like in https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/Hierarchical_proofs.html? What is the best approach in this case?
Informativa PrivacyQuesta email ha per destinatari dei contatti presenti negli archivi di Qualitade S.r.l.. Tutte le informazioni vengono trattate e tutelate nel rispetto della normativa vigente sulla protezione dei dati personali (Reg. EU 2016/679). Per richiedere informazioni e/o variazioni e/o la cancellazione dei vostri dati presenti nei nostri archivi potete inviare una email a qual...@legalmail.itAvviso di RiservatezzaIl contenuto di questa e-mail e degli eventuali allegati, è strettamente confidenziale e destinato alla/e persona/e a cui è indirizzato. Se avete ricevuto per errore questa e-mail, vi preghiamo di segnalarcelo immediatamente e di cancellarla dal vostro computer. E' fatto divieto di copiare e divulgare il contenuto di questa e-mail. Ogni utilizzo abusivo delle informazioni qui contenute da parte di persone terze o comunque non indicate nella presente e-mail, potrà essere perseguito ai sensi di legge.--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7e0fc5aa-f0c0-4f74-807b-bf0d5a114261%40googlegroups.com.
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/0cdf0ab6-f6a5-49dd-8292-ca15db5a01d8%40googlegroups.com.
THEOREM Div == \A m \in Nat \ {0}, n \in Nat \ {0}, d \in Int :
Divides(d, m) /\ Divides(d, n) <=> Divides(d, m) /\ Divides(d, n-m)
<1> SUFFICES ASSUME NEW m \in Nat \ {0}, NEW n \in Nat \ {0}, NEW d \in Int
PROVE /\ Divides(d, m) /\ Divides(d, n) => Divides(d, n-m)
/\ Divides(d, m) /\ Divides(d, n-m) => Divides(d, n)
OBVIOUS
<1>1. Divides(d, m) /\ Divides(d, n) => Divides(d, n-m)
<2>1. SUFFICES ASSUME NEW g \in Int, m = d*g,
NEW q \in Int, n = d*q
PROVE \E y \in Int : n-m = d*y
BY DEF Divides
<2>2. n-m = d*(q-g)
BY <2>1
<2>3. QED
BY <2>2
<1>2. Divides(d, m) /\ Divides(d, n-m) => Divides(d, n)
<2>1. SUFFICES ASSUME NEW g \in Int, m = d*g,
NEW q \in Int, n-m = d*q
PROVE \E y \in Int : n = d*y
BY DEF Divides
<2>2. n = d*(q+g)
BY <2>1
<2>3. QED
BY <2>2
<1>3. QED
BY <1>1, <1>2
THEOREM GCD3 == \A m, n \in Nat \ {0} :
(n > m) => (GCD(m, n) = GCD(m, n-m))
<1> SUFFICES ASSUME NEW m \in Nat \ {0}, NEW n \in Nat \ {0}, n > m
PROVE GCD(m, n) = GCD(m, n-m)
OBVIOUS
<1>1. \A i \in Int : Divides(i, m) /\ Divides(i, n) <=> Divides(i, m) /\ Divides(i, n-m)
BY Div
<1>2. QED
BY <1>1 DEF GCD, SetMax, DivisorsOf
While I don't profess that it's the most elegant approach, it is sufficiently fine-grained, minimising the size of each 'leap' and the number of theorems employed by each step. This makes it more resilient towards subtle regressions in Isabelle which have tripped me up in the past.