[isabelle] How to guide Isabelle to a proof?



Hi,

 

I am a beginner in formal method. I have problem proving the following
sub-goal:

 

goal (1 subgoal):

 1. !!n. [| snd (evaluate n);

            fst (snd (fst (snd (snd (snd (fst (evaluate n))))) !

                      snd (snd (snd (snd (fst (evaluate n))))))) =

            WriteLow;

            snd (snd (snd (snd (fst (evaluate n)))))

            < length (fst (snd (snd (snd (fst (evaluate n)))))) |]

         ==> case List__find

                   (%i. ~ fst i <

                          fst (snd (snd (fst

    (snd (snd (snd (fst (evaluate n))))) !

   snd (snd (snd (snd (fst (evaluate n)))))))) &

                        (~ fst i <

                           fst (snd (snd

(fst (snd (snd (snd (fst (evaluate n))))) !

 snd (snd (snd (snd (fst (evaluate n)))))))) -->

                         ~ fst (snd (snd

(fst (snd (snd (snd (fst (evaluate n))))) !

 snd (snd (snd (snd (fst (evaluate n)))))))) <

                           fst i))

                   (fst (fst (evaluate n))) of

             None => True

             | Some var =>

                 (thirdl var = Low --> True) & (thirdl var ~= Low --> False)

 

Please help to advice on how I should go about proving this sub-goal.

 

Marcus.

 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.