[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Tue, 2 Jan 2024 18:12:08 +0100*References*: <e946a3f1-5422-4ee1-b598-a98e57c2275an@googlegroups.com>

Hi Ugur, Isabelle uses the definition of R, simplifies the resulting arithmetic expressions, and the proof then no longer matches the rule you wish to apply. So you need to hide the definition of R before applying rule DownwardNatInduction. The following works: THEOREM UpwardNatInduction == ASSUME NEW P(_), NEW m \in Nat, P(0), \A n \in 1 .. m : P(n-1) => P(n) PROVE P(m) <1> DEFINE R(i) == P(m-i) <1>1. R(m) OBVIOUS <1>2. \A n \in 1 .. m : R(n) => R(n-1) OBVIOUS <1>3. R(0) <2>. HIDE DEF R <2>. QED BY <1>1, <1>2, DownwardNatInduction <1> QED BY <1>3 Stephan
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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/9CD5F21B-50FB-4577-85B6-1C321A3303BE%40gmail.com. |

**References**:**[tlaplus] Using DownwardNatInduction from NaturalsInduction***From:*Ugur Y. Yavuz

- Prev by Date:
**[tlaplus] Using DownwardNatInduction from NaturalsInduction** - Next by Date:
**[tlaplus] Draft of New TLA Book** - Previous by thread:
**[tlaplus] Using DownwardNatInduction from NaturalsInduction** - Next by thread:
**[tlaplus] Draft of New TLA Book** - Index(es):