Re: [isabelle] Structured induction with custom tactics



Hi Palle,

I am afraid I cannot give an answer to all your questions.

Palle Raabjerg writes:
 > 
 > But in short, what I want to do is automate/manipulate Isar style
 > structured proofs in ML.
 > 
 > Since the last mail I have been looking around to find out more. The
 > Isabelle Programming Tutorial has a section intended for the subject of
 > structured proofs in ML. But that section is marked TBD, and there is
 > only a very short example on a single page.

Sorry. Writing tutorials takes time and it is usually
a thankless task (in terms of paper-counts etc). What
I thought I will describe in this section is how to 
deal with manipulations of contexts. If I understood 
your original question correctly, this will not be of
much help to you.

 > Using 'Proof.theorem_i' as follows:
 > Proof.theorem_i NONE (K I) [[(@{prop "A ==> A"}, [])]] @{context}
 > seems to yield a state with a stack of 3 nodes, the _second_ node
 > including the goal "A ==> A", the other two empty. Puzzling. Maybe
 > theorem_i is not what I am looking for.

Usually, if you want to set up a goal to be proved, then you
need to use the function Goal.prove. For this you need a tactic 
that completely solves the goal. Not sure whether this is what
you want.

 > What is the intention of Proof.theorem/theorem_i?

The function theorem is for "outer layers" where the terms
are given as strings. Theorem_i is the "internal" interface
where parsing has been already done and terms are given
as "real" terms. Having said that, forget this convention 
quickly, as it is already obsolete. I think today, functions
for "outer layers" are called foo_cmd, while the internal
functions are just called foo.

To give more help, maybe it would be helpful if you describe 
exactly what you like to do. In your last email you described 
your problem in abstract terms. Judging from the absence of
replies, it seems nobody was able to give an appropriate
answer. Maybe a concrete example or even a small theory
file would be more helpful....though no promises ;o)

Best wishes,
Christian





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.