<1>3. QED
BY <1>1, <1>2, SequencesInductionTail, IsaM("blast")
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
Hello all,
I have a theorem which depends on some lemmas. One of this lemmas is the fact that "the product of two sequence products is the sequence product of their concatenation". That is:
\A s1, s2 \in Seq(Nat) : SeqProduct[s1] * SeqProduct[s2] = SeqProduct[s1 \o s2]
where
SeqProduct[s \in Seq(Nat)] ==
IF s = <<>>
THEN 1
ELSE LET x == Head(s)
xs == Tail(s)
IN x * SeqProduct[xs]
For this one, im planning to reason inductively using the SequencesInductionTail theorem available on module SequenceTheorems (not saying this alone will suffice).
Now, having the following structure:
LEMMA SomeLemma == \A s1, s2 \in Seq(Nat) : SeqProduct[s1] * SeqProduct[s2] = SeqProduct[s1 \o s2]
<1> DEFINE Prop(s) == \A s2 \in Seq(Nat) : SeqProduct[s] * SeqProduct[s2] = SeqProduct[s \o s2]
<1> SUFFICES \A s1 \in Seq(Nat) : Prop(s1) OBVIOUS
<1>1. Prop(<<>>) PROOF OMITTED
<1>2. \A s \in Seq(Nat) : (s # << >>) /\ Prop(Tail(s)) => Prop(s) PROOF OMITTED
<1> HIDE DEF Prop
<1>3. QED
BY <1>1, <1>2, SequencesInductionTail
Ignoring now <1>1 and <1>2, for the high level part i was expecting TLAPS to prove the final step <1>3 and it couldn't.
The proof obligation generated is:
ASSUME Prop(<<>>) ,
\A s \in Seq(Nat) : s # <<>> /\ Prop(Tail(s)) => Prop(s) ,
ASSUME NEW CONSTANT S,
NEW CONSTANT P(_),
P(<<>>) ,
\A s \in Seq(S) : s # <<>> /\ P(Tail(s)) => P(s)
PROVE \A s \in Seq(S) : P(s)
PROVE \A s1 \in Seq(Nat) : Prop(s1)
which looks reasonable to me. Also tried the ASSUME ... PROVE form, but the result is the same.
Im missing something here to correctly invoke SequencesInductionTail ?
Thanks.
--
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/49d1f151-10fe-449d-9fd9-fa7abbf2a4e5%40googlegroups.com.