Re: [isabelle] Document preparation question



Hi,

Am Donnerstag, den 17.01.2013, 11:03 +0100 schrieb Florian Haftmann:
> > I also miss good ways to automatically print data type definitions. My
> > work around is to show
> >         lemma Terms:
> >           "∃ x assn e'. (e = (Lam [x]. e') ∨ (e = Var x) ∨ (e = App e' x) ∨ (e = Let assn e'))"
> >           by (metis Terms.exp_assn.exhaust(1))
> > and pretty-print this lemma in the text, but a tool that formats an
> > exhaust-lemma in the style of a grammar specification would be slick.
> 
> Maybe also something which can be implemented as term style, e.g.
> expecting an exhaustivness lemma as produced by datatype and rearranging
> it as desired.

I tried to do it using the translation and syntax features, and here is
what I cam up with, based on my very partial understanding of these
features:

abbreviation (Grammar output)
  "grammar_imp"
where
  "grammar_imp ≡ op ⟶"

syntax (Grammar output)
  "_grapats" :: "term \<Rightarrow> term \<Rightarrow> term" ("_ | _")
  "_grafirst" :: "term \<Rightarrow> term \<Rightarrow> term" ("_ ::= _")
  "_grarest" :: "term \<Rightarrow> term \<Rightarrow> term"
  "_firsteq" :: "term \<Rightarrow> term \<Rightarrow> term"
  "_resteq" :: "term \<Rightarrow> term \<Rightarrow> term"

translations
  "_grapats (_firsteq all) (_grarest (CONST grammar_imp rest1 rest2))" <= "CONST grammar_imp all (CONST grammar_imp rest1 rest2)"
  "_grapats (_resteq all) (_grarest (CONST grammar_imp rest1 rest2))" <= "_grarest (CONST grammar_imp all (CONST grammar_imp rest1 rest2))"
  "_resteq all" <= "_grarest (CONST grammar_imp all rest)"
  "_resteq all" <= "_resteq (CONST grammar_imp all rest)"
  "_firsteq all" <= "_firsteq (CONST grammar_imp all rest)"
  "_firsteq imp" <= "_firsteq (ALL x. imp)"
  "_resteq imp" <= "_resteq (ALL x. imp)"
  "_grafirst x t" <= "_firsteq (x = t)"
  "t" <= "_resteq (x = t)"

This does require the lemma to be internalized, e.g.:
        lemma tmp:
        "(∀ var. y = Var var ⟶ P) ⟶
         (∀ exp var. y = App exp var ⟶ P) ⟶
         (∀ assn exp. y = Terms.Let assn exp ⟶ P) ⟶
         (∀ var exp. y = Lam [var].exp ⟶ P) ⟶ P"
          by (metis exp_assn.exhaust(1)) 
but then
        thm (Grammar) tmp[no_vars]
prints
        y ::= Var var | App exp var | Terms.Let assn exp | Lam [var].
        exp 
which is nice.


It seems that translations work independent of the current mode. That is
why I introduced a mode-dependent abbreviation for the outermost symbol
of the theorem (op ⟶), to make sure my translations only affect the
output in this particular mode. The abbreviation command did however not
work with Trueprop or ==> – how can I adjust this setup to work with the
meta logic directives directly?


There might be more eleganter and saner ways to achieve this. If so,
please let me know.

Thanks,
Joachim

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.info.uni-karlsruhe.de/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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