[isabelle-dev] Nested "case" statements and "show" getting stuck
simon.meier at inf.ethz.ch
Thu Dec 10 21:01:45 CET 2009
(Apologies in advance, if I should have sent this mail to the
Isabelle users list. However, the problems are Isabelle
I'm working on automatically generating Isabelle/ISAR proofs of
secrecy and authentication properties of security protocols. These
proofs are based on a set of inference rules derived from a deep
embedding of an operational security protocol semantics.
In order to allow for a "natural" representation of these proofs, I
have extended the ISAR proof language. Among these extensions is a
new proof method "sources", which allows for case splits about the
origin of a message known to the intruder. This proof method works
by instantiating a general theorem, converting its conclusion into
disjunctive normal form represented in elimination form (I hope this
is the right term for rules like 'disjE' and 'exE'), and attaching
appropriate case name information.
As you can see from the attached NSL example the resulting proofs
use several nested applications of the "sources" proof method. This
leads to problems, I have trouble dealing with:
1. It seems that case environments are global instead of local to
subproofs. Hence, reusing case names in a subproof is impossible.
2. Sometimes in a more deeoply nested position (like four calls of
the "sources" proof method) the "show" command gets stuck while
checking if the proven goal solves an open subgoal.
I think I can develop a workaround for problem (1). Or perhaps I'm
just using the infrastructure the wrong way round.
However, I'm stuck on problem (2). Possibly useful information about
my implementation of the "sources" proof method is:
2.a Facts are getting accumulated as it would be the case for nested
applications of the "induct" proof method. I'm doing this such
that the user doesn't need to name and gather them by himself.
Furthermore, all facts are needed for the
"qed ((clarsimp, order?)+)?"
finishers to work. However, I'm not sure if these facts inserted
into the proof goal are the same ones that the user is getting
as local assumptions.
2.b Some cases do not have a new fixed variables in the corresonding
premise of the derived rule used for the case distinction. In
order, to allow for uniform output, I add an additional dummy
abstraction to the terms used for the assumption part of the
named case. This way an additional argument for a named fixed
variable is allowed in every case.
However, I'm not doing the same dummy abstraction in the derived
rule. Perhaps this makes the checking loop.
2.c I'm using Isabelle2009-1 on an Ubuntu 9.10 Linux machine.
All in all, the Isabelle codebase is really nice to work with. I
could gather a lot of information from it. However, I have trouble
understanding the rule_cases.ml file. It would be great, if I could
be given some good pointers for understanding it.
many thanks in advance and best regards,
PS: I can make the theories available if this is any help.
ETH Zurich, Simon Meier, Department of Computer Science
IFW C 43.1, Haldeneggsteig 4 / Weinbergstrasse, 8092 Zurich, SWITZERLAND
Tel +41 44 632 83 84, Fax +41 44 632 11 72,
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
More information about the isabelle-dev