Email Gateway (Aug 18 2022 at 11:48): Email Gateway (Aug 18 2022 at 11:48):From: "jwang whu.edu.cn (jwang)" <jwang@whu.edu.cn>
Hi:
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?
sincerely
Jean
Email Gateway (Aug 18 2022 at 11:48):From: Lawrence Paulson <lp15@cam.ac.uk>
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
Last updated: May 03 2024 at 04:19 UTC