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.
On 28 Apr 2008, at 08:19, jwang whu.edu.cn (jwang) wrote:
Now,I'm studing the proof process of Ns_Bublic_Bad.thy in the
"src/HOl/Auth/Ns_Punlic_Bad.thy".I run the Ns_Bublic_Bad.thy in
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