Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] How to guide Isabelle to a proof?

view this post on Zulip Email Gateway (Aug 18 2022 at 12:35):

From: Eng Siong Ng <eng@nps.edu>
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.

Last updated: May 03 2024 at 12:27 UTC