[isabelle-dev] Nested "case" statements and "show" getting stuck

[Simon Meier]

Hi all,

(Apologies in advance, if I should have sent this mail to the
Isabelle users list. However, the problems are Isabelle
implementation specific.)

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,
Simon

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,
www.infsec.ethz.ch
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: nsl_cert_auto.thy
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20091210/18a86107/attachment.ksh>