*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Document preparation question*From*: Joachim Breitner <breitner at kit.edu>*Date*: Thu, 17 Jan 2013 17:23:45 +0100*In-reply-to*: <50F7CC8C.2060308@informatik.tu-muenchen.de>*References*: <1358414370.4392.23.camel@kirk> <50F7CC8C.2060308@informatik.tu-muenchen.de>

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**

**References**:**[isabelle] Document preparation question***From:*Joachim Breitner

**Re: [isabelle] Document preparation question***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] Zorn's Lemma
- Next by Date: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error
- Previous by Thread: Re: [isabelle] Document preparation question
- Next by Thread: Re: [isabelle] Document preparation question
- Cl-isabelle-users January 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list