Experimental pgip_isar.xml file
authoraspinall
Mon Aug 16 17:56:07 2004 +0200 (2004-08-16)
changeset 1513387c074aad007
parent 15132 df2b7976d1e7
child 15134 d3fa5e1d6e4d
Experimental pgip_isar.xml file
lib/ProofGeneral/pgip_isar.xml
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/lib/ProofGeneral/pgip_isar.xml	Mon Aug 16 17:56:07 2004 +0200
     1.3 @@ -0,0 +1,147 @@
     1.4 +<!-- Title:      Pure/pgip_isar.xml
     1.5 +     ID:         $Id$
     1.6 +     Author:     David Aspinall, University of Edinburgh
     1.7 +		 Christoph Lüth, University of Bremen
     1.8 +
     1.9 +This file contains the configuration messages which configure 
    1.10 +PGIP interfaces for Isabelle/Isar, in particular, explaining
    1.11 +internal types of objects and operations available on them.
    1.12 +
    1.13 +See http://proofgeneral.inf.ed.ac.uk/kit for more details.
    1.14 +
    1.15 +This file is a contributed part of the Isabelle Distribution.
    1.16 +
    1.17 +STATUS: incomplete and experimental.
    1.18 +-->
    1.19 +
    1.20 +<guiconfig>
    1.21 +  <!-- objtypes -->
    1.22 +  <objtype name="toplevel" descr="top-level context (PGIP internal)">
    1.23 +  <contains objtype="theory"/>
    1.24 +  </objtype>
    1.25 +  <objtype name="theory" descr="Isabelle theory">
    1.26 +  <contains objtype="theorem"/>
    1.27 +  <contains objtype="theory"/>
    1.28 +  </objtype>
    1.29 +  <objtype name="theorem" descr="Isabelle theorem">
    1.30 +  <hasprefs prefcategory="Theorem attributes">
    1.31 +   <haspref name="thm-kind" descr="Theorem kind">
    1.32 +    <pgipchoice>
    1.33 +     <pgipchoiceitem>theorem</pgipchoiceitem>
    1.34 +     <pgipchoiceitem>lemma</pgipchoiceitem>
    1.35 +     <pgipchoiceitem>corollary</pgipchoiceitem>
    1.36 +    </pgipchoice>
    1.37 +   </haspref>
    1.38 +   <haspref name="thm-simp" descr="Include in simplifier set">
    1.39 +    <pgipbool/>
    1.40 +   </haspref>
    1.41 +   <haspref name="thm-intro" descr="Flag as introduction rule">
    1.42 +    <pgipbool/>
    1.43 +   </haspref>
    1.44 +   <haspref name="thm-elim" descr="Flag as elimination rule">
    1.45 +    <pgipbool/>
    1.46 +   </haspref>
    1.47 +   <haspref name="thm-dest" descr="Flag as destruction rule">
    1.48 +    <pgipbool/>
    1.49 +   </haspref>
    1.50 +  </hasprefs>
    1.51 +  </objtype>
    1.52 +  <objtype name="term"      descr="Isabelle term">
    1.53 +    <icon>
    1.54 +      R0lGODlhJgAgAIQAAP////r6+uDg4Nra2tnZ2fn5+WFhYUJCQkFBQWBgYMnO
    1.55 +      91xq6K208wsg3XiD7OTm+0FR5CY54Pb29t3d3dfX119fX/T09NbW1tjY2AAA
    1.56 +      AAAAAAAAAAAAAAAAAAAAAAAAACH+FUNyZWF0ZWQgd2l0aCBUaGUgR0lNUAAh
    1.57 +      +QQBCgAfACwAAAAAJgAgAAAFnCAgjmRpnqgYCAPhvnAsz7BQAIJxIHzv/8Cg
    1.58 +      LyHA6YTI5I8IWLVo0Gjtlqpar9istqRYLBTbMIDRaDDEW7IZrVWf2VYGw1F2
    1.59 +      yBkP+KnM77/1Jm6AcWV/gyeChyiJioGFjYiPkCWMkyKVlpiTmpBqEJYlEWUR
    1.60 +      XgugDBCjDnmgrZMSExQUUrQ0NgADFUq7SUy5vMBATBYDFxi1yFMAIQA7
    1.61 +    </icon>
    1.62 +  </objtype>
    1.63 +  <objtype name="type"      descr="Isabelle type">
    1.64 +    <icon>
    1.65 +      R0lGODlhJgAgAIQAAP////r6+uDg4Nra2tnZ2fn5+WFhYUJCQkFBQWBgYOTm
    1.66 +      +62080FR5Asg3SY54Fxq6MnO95Kc73iD7Pb29t3d3dfX119fX/T09NbW1tjY
    1.67 +      2AAAAAAAAAAAAAAAAAAAAAAAACH+FUNyZWF0ZWQgd2l0aCBUaGUgR0lNUAAh
    1.68 +      +QQBCgAfACwAAAAAJgAgAAAFsyAgjmRpnqgYCAPhvnAsz7BQAIJxIHzv/8Cg
    1.69 +      LyHA6YTI5I8IWLVo0Gjtlqpar9istqRYeL9exbaqYDTOaPRijFI40vDGmm16
    1.70 +      NB74NwOPh9C5DWIidn9VERIkb4UpEYIiZ4tZkJFWEA0MlFYLd5lVmw+dKZ8k
    1.71 +      fqEim4GnoKYAlndiDIisAG9ppawSaauzALkNsrzBwsPEIxMUFRVSyzQ2AAMW
    1.72 +      StJJTNDT10BMFwMYGczfUwAhADs=
    1.73 +    </icon>
    1.74 +  </objtype>
    1.75 +  <objtype name="thmset"    descr="Set of Isabelle theorems">
    1.76 +    <contains objtype="theorem"/>
    1.77 +  </objtype>
    1.78 +<!-- possible objtypes not yet supported:
    1.79 +  <objtype name="oopsgoal"  descr="Abandoned proof"></objtype>
    1.80 +  <objtype name="sorrygoal" descr="Postponed proof"></objtype>
    1.81 +  <objtype name="proof"	    descr="Completed proof"></objtype>
    1.82 +  <objtype name="method"    descr="Isar method or proof step"></objtype>
    1.83 +-->
    1.84 +
    1.85 +  <!-- object operations -->
    1.86 +
    1.87 +  <opn name="add to simpset">
    1.88 +    <opsrc>theorem</opsrc>
    1.89 +    <optrg></optrg>
    1.90 +    <opcmd>declare %1 [simp]</opcmd>
    1.91 +  </opn>
    1.92 +
    1.93 +  <opn name="remove from simpset">
    1.94 +    <opsrc>theorem</opsrc>
    1.95 +    <optrg></optrg>
    1.96 +    <opcmd>declare %1 [simp del]</opcmd>
    1.97 +  </opn>
    1.98 +
    1.99 +  <opn name="instantiatevar">
   1.100 +    <opsrc>theorem term</opsrc>
   1.101 +    <optrg>theorem</optrg>
   1.102 +    <opcmd>%1 [OF %2]</opcmd>
   1.103 +  </opn>
   1.104 +
   1.105 +  <!-- interactive operations -->
   1.106 +  <!-- da: this isn't really a good example.  
   1.107 +       Isar doesn't have cterms, the "term" command just checks & prints
   1.108 +       a term in the current context. -->
   1.109 +  <opn name="checkterm">
   1.110 +    <inputform>
   1.111 +      <field name="term"><pgipstring/><prompt>Input a term:</prompt></field>
   1.112 +    </inputform>
   1.113 +    <opsrc></opsrc>
   1.114 +    <optrg>term</optrg>
   1.115 +    <opcmd>term %term</opcmd>
   1.116 +  </opn>
   1.117 +
   1.118 +  <!-- proof operations -->
   1.119 +  <opn name="applyrule">
   1.120 +    <opsrc>ruleset</opsrc>
   1.121 +    <opcmd>apply (rule %1)</opcmd>
   1.122 +  </opn>
   1.123 +  <opn name="applyerule">
   1.124 +    <opsrc>ruleset</opsrc>
   1.125 +    <opcmd>apply (erule %1)</opcmd>
   1.126 +  </opn>
   1.127 +  <opn name="applydrule">
   1.128 +    <opsrc>ruleset</opsrc>
   1.129 +    <opcmd>apply (drule %1)</opcmd>
   1.130 +  </opn>
   1.131 +
   1.132 +  <!-- introduce new goal -->
   1.133 +  <!-- [FIXME: ideally need to generalise substitution for options? in pgipchoice -->
   1.134 +  <opn name="openlemma">
   1.135 +    <inputform>
   1.136 +      <field name="name"><pgipstring/><prompt>Input a name:</prompt></field>
   1.137 +      <field name="term"><pgipstring/><prompt>Input a term:</prompt></field>
   1.138 +      <field name="attributes">
   1.139 +	<pgipchoice>
   1.140 +	<pgipchoiceitem name="none"></pgipchoiceitem>
   1.141 +	<pgipchoiceitem name="use in global simplifier context">[simp]</pgipchoiceitem>
   1.142 +	</pgipchoice>
   1.143 +	<prompt>Attributes:</prompt></field>
   1.144 +    </inputform>
   1.145 +    <opsrc></opsrc>
   1.146 +    <opcmd>lemma %attributes %name : "%term"</opcmd>
   1.147 +  </opn>
   1.148 +
   1.149 +</guiconfig>
   1.150 +