Email Gateway (Aug 18 2022 at 11:44): Email Gateway (Aug 18 2022 at 11:44):From: "jwang whu.edu.cn (jwang)" <jwang@whu.edu.cn>
hello,
I'm studying the proof process of NS_Public_Bad.thy in
Isabelle.The content of file( see the attached file)is the
simplification rules used by auto method which is used to proving the
following lemma.I get the simplification rules by
"Isabele--setting--trace simplifier".
lemma Spy_analz_priEK[simp]:
"evs \<in>ns_public\<Longrightarrow>(Key
(invkey(priEK A) \<in>analz(spies evs))=(A\<in>bad)"
by auto
The simplification rules is verbose and very hard to
uderstand.Could anyone interpret the above simplification rules and
simplification process ?
Thanks
Jean
ns_bad.thy
Email Gateway (Aug 18 2022 at 11:44):From: Jens Doll <jd@cococo.de>
Greetings;
which viewer am I supposed use, if I wanted to read a *.thy file on a win
machine?
JD
Email Gateway (Aug 18 2022 at 11:44):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear Jens,
which viewer am I supposed use, if I wanted to read a *.thy file on a win
machine?
The answer is simple: (X)Emacs/ProofGeneral. The (X)Emacs coming with
the Cygwin emulation layer is suitable to run ProofGeneral. Details are
available from the Isabelle FAQ http://isabelle.in.tum.de/faq.html and
the installation instructions http://isabelle.in.tum.de/installation.html.
Hope this helps
Florian
signature.asc
Last updated: May 03 2024 at 08:18 UTC