Hi Frédéric, I see, thanks a lot – in fact, the inability to prove step <4>3 in this context appears to come from an unintended interaction with the set product in the argument to Seq(_) that we'll have to investigate further. Here are two possible fixes in the meanwhile. The first workaround uses lemma SeqDef (the very first lemma in module SequenceTheorems, of which your proposed lemma is an immediate consequence). The step is then proved by Isabelle. <4>1. J \in Nat <4>2. seq \in [ 1 .. J -> ( 0 .. 9 ) \X ( 0 .. 9 ) \X ( ( 0 .. 9 ) \X ( 0 .. 9 ) ) ] <4>3. seq \in Seq(( 0 .. 9 ) \X ( 0 .. 9 ) \X ( ( 0 .. 9 ) \X ( 0 .. 9 ) )) BY <4>1, <4>2, SeqDef The second workaround consists in hiding the product construction: this is a general recipe for handling "complex" expressions that are irrelevant for a given step. Here, the step is proved by SMT using its built-in knowledge of sequences. <4>1. J \in Nat <4>. DEFINE S == ( 0 .. 9 ) \X ( 0 .. 9 ) \X ( ( 0 .. 9 ) \X ( 0 .. 9 ) ) <4>2. seq \in [ 1 .. J -> S] <4>. HIDE DEF S <4>3. seq \in Seq(S) BY <4>1, <4>2 If you need the definition of S further down in the proof, you may prefer the variant <4>1. J \in Nat <4>. DEFINE S == ( 0 .. 9 ) \X ( 0 .. 9 ) \X ( ( 0 .. 9 ) \X ( 0 .. 9 ) ) <4>2. seq \in [ 1 .. J -> S] <4>3. seq \in Seq(S) <5>. HIDE DEF S <5>. QED BY <4>1, <4>2 Best regards, Stephan P.S.: Using the default settings on my platform, I use cvc3 as the default SMT solver, although any solver should be able to handle this proof. -s
|