Re: [isabelle] about the proof of ns_public_bad protocol

The behaviour you describe is merely an instance of how Isabelle uses logic. In particular, if a rewrite rule contains a conditional expression (that is, if-then-else) then Isabelle will automatically perform a case split on the condition during simplification. Sometimes, both cases will be presented to you; at other times, Isabelle may succeed in proving one of the cases and present you with the other one. That is what you are seeing.

It might help if you went through the examples in the tutorial.
Larry Paulson

On 28 Apr 2008, at 08:19, jwang (jwang) wrote:

Now,I'm studing the proof process of Ns_Bublic_Bad.thy in the path "src/HOl/Auth/Ns_Punlic_Bad.thy".I run the Ns_Bublic_Bad.thy in ISABELLE
and analyse
the proof scripts of Ns_Punlic_Bad protocol.But I could not understand
the proof process of  the theorem   Spy_not_see_NA and
A_trusts_NS2_lemma.Applying erule ns_public.induct,then five subgoals
were given,but how  were the five subgoals  proved?why Ba belong to
"bad"  in evs1,evs3 and Aa belong to "bad 'in  evs2?



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