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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Sat, 30 May 2020 11:16:06 +0200*References*: <49d1f151-10fe-449d-9fd9-fa7abbf2a4e5@googlegroups.com>

Hello, the proof works if you write ` <1>3. QED `
A little explanation: Isabelle is the only backend useful for proving schematic goals, i.e. those involving some predicate parameters such as Prop and P in your example. The default proof method "auto" combines rewriting and standard logic reasoning, and it so happens that the rewriting it performs is counter-productive here. The "blast" method omits the rewriting and can trivially solve the obligation. Note that since SeqProduct is defined as a recursive function (which introduces a CHOOSE), you will need to prove that it satisfies the expected equation, i.e. you want to prove LEMMA ASSUME NEW s \in Seq(Nat) PROVE SeqProduct(s) = IF s = << >> THEN 1 ELSE Head(s) * SeqProduct(Tail(s)) in order to be able to prove steps <1>1 and <1>2 of your lemma. The theorem TailInductiveDef (in module SequenceOpTheorems) is designed to prove exactly that, and the theorem TailInductiveDefType may also be useful. You may also want to look at some of the proofs of the library theorems (in modules SequenceTheorems_proofs and SequenceOpTheorems_proofs) if you get stuck in your proofs. Hope this helps, 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/F30C5582-E77D-4405-A68A-5214D9FA50CA%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] Proof by induction invoking the SequencesInductionTail theorem***From:*JosEdu Solsona

**References**:**[tlaplus] Proof by induction invoking the SequencesInductionTail theorem***From:*JosEdu Solsona

- Prev by Date:
**[tlaplus] Proof by induction invoking the SequencesInductionTail theorem** - Next by Date:
**[tlaplus] how to input an array constant in TLA+ toolbox?** - Previous by thread:
**[tlaplus] Proof by induction invoking the SequencesInductionTail theorem** - Next by thread:
**Re: [tlaplus] Proof by induction invoking the SequencesInductionTail theorem** - Index(es):