Re: [isabelle] I want to print axiomatization info



Larry,

Thanks for fix. It makes sense now that a binary operator needs an associativity rule. I was trying to finish making my table of HOL operator priorities, so I would have lots of examples, and then try to dig through section "7.2 Mixfix annotations" of isar-ref.pdf. But now, I can put off looking at the mixfix documentation.

(For anyone interested, I've attached iS.thy. Load it into jEdit, have sidekick open to see the section tree, and in section 1 there's all the symbols from etc/symbols. In section 2 there's a table showing the mixfix operator priorites from HOL.thy, and in section 3 there's the source from src/Pure/pure_thy.ML, which contains the mixfix operator priorities for the Pure logic.)

If I had print commands, like thm, find_theorems, find_consts, etc., but for axiomatizations and defs, I might could figure out some of your logic in HOL.thy. Makarius showed me how to print explicit use of Trueprop and prop, so with explicit types, explicit parentheses, explicit names, explicit Trueprop, and explicit prop, I might could eventually figure out the reasoning behind your defs in HOL.thy, like for these:

LINE: 178 of src/HOL/HOL.thy
defs
  True_def:     "True      == ((%x::bool. x) = (%x. x))"
  All_def:      "All(P)    == (P = (%x. True))"
  Ex_def:       "Ex(P)     == !Q. (!x. P x --> Q) --> Q"
  False_def:    "False     == (!P. P)"
  not_def:      "~ P       == P-->False"
  and_def:      "P & Q     == !R. (P-->Q-->R) --> R"
  or_def:       "P | Q     == !R. (P-->R) --> (Q-->R) --> R"
  Ex1_def:      "Ex1(P)    == ? x. P(x) & (! y. P(y) --> y=x)"

I'm thinking that parts of your "Interactive Proof with Cambridge LCF" and your "The Foundation of a Generic Theorem Prover" will eventually help me out, that you directly implement into HOL.thy some of the logic definitions in your LCF book. It'll take time for me to find that out.

But, with the right print info for definitions and axiomatizations, it would help me when I occasionally look at definitions such as the above.

Thanks,
GB



On 7/8/2012 2:46 AM, Lawrence Paulson wrote:
On 8 Jul 2012, at 02:18, Gottfried Barrow wrote:

2) I got lots of warnings like: "Ambiguous input produces 4 parse trees... Fortunately, only one parse tree is type correct..."
This message indicates that your syntax is ambiguous. The way to eliminate such a message is by disambiguating your syntax, which in most cases means tightening up the precedences of operators. And indeed, your operator “in" gives no precedence information for its operands. I wonder why you don't use something akin to (ignoring fancy symbols)

	(infixl "IN" 55)

where you have

	("_ IN_ " 55) .

Larry Paulson






(*DOC*)theory iS(*DOC*)
imports Main
begin
section{* FROM: Isabelle2012/etc/symbols *}
subsection{* NOTE: Use a backslash before the "<" in each command. *}
--"However, in jEdit, if you simply start typing what's between '<' and '>',
   the command completion will kick in."
--"Set the SideKick option 'After popup trigger keystroke, wait (seconds)' to
   determine how fast the popup windowd pops up."
subsection{* 0-9 *}
text{*
...\<zero>......<zero>
...\<one>......<one>
...\<two>......<two>
...\<three>......<three>
...\<four>......<four>
...\<five>......<five>
...\<six>......<six>
...\<seven>......<seven>
...\<eight>......<eight>
...\<nine>......<nine>
*}
subsection{* mathcal *}
text{*
...\<A>......<A>
...\<B>......<B>
...\<C>......<C>
...\<D>......<D>
...\<E>......<E>
...\<F>......<F>
...\<G>......<G>
...\<H>......<H>
...\<I>......<I>
...\<J>......<J>
...\<K>......<K>
...\<L>......<L>
...\<M>.....<M>
...\<N>......<N>
...\<O>......<O>
...\<P>......<P>
...\<Q>......<Q>
...\<R>......<R>
...\<S>......<S>
...\<T>......<T>
...\<U>......<U>
...\<V>......<V>
...\<W>.....<W>
...\<X>......<X>
...\<Y>......<Y>
...\<Z>......<Z>
...\<a>......<a>
...\<b>......<b>
...\<c>......<c>
...\<d>......<d>
...\<e>......<e>
...\<f>.......<f>
...\<g>......<g>
...\<h>......<h>
...\<i>.......<i>
...\<j>.......<j>
...\<k>......<k>
...\<l>.......<l>
...\<m>......<m>
...\<n>......<n>
...\<o>......<o>
...\<p>......<p>
...\<q>......<q>
...\<r>......<r>
...\<s>......<s>
...\<t>......<t>
...\<u>......<u>
...\<v>......<v>
...\<w>......<w>
...\<x>......<x>
...\<y>......<y>
...\<z>......<z>
*}
subsection{* mathfrak *}
text{*
...\<AA>......<AA>
...\<BB>.....<BB>
...\<CC>......<CC>
...\<DD>......<DD>
...\<EE>......<EE>
...\<FF>......<FF>
...\<GG>......<GG>
...\<HH>......<HH>
...\<JJ>......<JJ>
...\<KK>......<KK>
...\<LL>......<LL>
...\<MM>.....<MM>
...\<NN>......<NN>
...\<OO>......<OO>
...\<PP>......<PP>
...\<QQ>......<QQ>
...\<SS>......<SS>
...\<TT>......<TT>
...\<UU>......<UU>
...\<VV>......<VV>
...\<WW>.....<WW>
...\<XX>......<XX>
...\<YY>......<YY>
...\<ZZ>......<ZZ>
...\<aa>......<aa>
...\<bb>......<bb>
...\<cc>......<cc>
...\<dd>......<dd>
...\<ee>......<ee>
...\<ff>......<ff>
...\<gg>......<gg>
...\<hh>......<hh>
...\<ii>.......<ii>
...\<jj>.......<jj>
...\<kk>......<kk>
...\<ll>.......<ll>
...\<mm>......<mm>
...\<nn>......<nn>
...\<oo>......<oo>
...\<pp>......<pp>
...\<qq>......<qq>
...\<rr>......<rr>
...\<ss>......<ss>
...\<tt>......<tt>
...\<uu>......<uu>
...\<vv>......<vv>
...\<ww>......<ww>
...\<xx>......<xx>
...\<yy>......<yy>
...\<zz>......<zz>
*}
subsection{* Greek *}
text{*
...\<alpha>......<alpha>
...\<beta>......<beta>
...\<gamma>......<gamma>
...\<delta>......<delta>
...\<epsilon>......<epsilon>
...\<zeta>......<zeta>
...\<eta>......<eta>
...\<theta>......<theta>
...\<iota>......<iota>
...\<kappa>......<kappa>
...\<lambda>......<lambda>               abbrev: %
...\<mu>......<mu>
...\<nu>......<nu>
...\<xi>......<xi>
...\<pi>......<pi>
...\<rho>......<rho>
...\<sigma>......<sigma>
...\<tau>......<tau>
...\<upsilon>......<upsilon>
...\<phi>......<phi>
...\<chi>......<chi>
...\<psi>......<psi>
...\<omega>......<omega>
...\<Gamma>......<Gamma>
...\<Delta>......<Delta>
...\<Theta>......<Theta>
...\<Lambda>......<Lambda>
...\<Xi>......<Xi>
...\<Pi>......<Pi>
...\<Sigma>......<Sigma>
...\<Upsilon>......<Upsilon>
...\<Phi>......<Phi>
...\<Psi>......<Psi>
...\<Omega>......<Omega>
*}
subsection{* Blackboard Bold *}
text{*
...\<bool>......<bool>
...\<complex>......<complex>
...\<nat>......<nat>
...\<rat>......<rat>
...\<real>......<real>
...\<int>......<int>
*}
subsection{* Arrows, Etc. *}
text{*
...\<leftarrow>.....<leftarrow>
...\<longleftarrow>....<longleftarrow>
...\<rightarrow>.....<rightarrow>           abbrev: ->
...\<longrightarrow>....<longrightarrow>       abbrev: -->
...\<Leftarrow>.....<Leftarrow>
...\<Longleftarrow>....<Longleftarrow>
...\<Rightarrow>.....<Rightarrow>           abbrev: =>
...\<Longrightarrow>....<Longrightarrow>       abbrev: ==>
...\<leftrightarrow>.....<leftrightarrow>
...\<longleftrightarrow>....<longleftrightarrow>   abbrev: <->
...\<Leftrightarrow>.....<Leftrightarrow>
...\<Longleftrightarrow>....<Longleftrightarrow>   abbrev: <=>
...\<mapsto>.....<mapsto>               abbrev: |->
...\<longmapsto>....<longmapsto>           abbrev: |-->
...\<midarrow>......<midarrow>
...\<Midarrow>......<Midarrow>
...\<hookleftarrow>.....<hookleftarrow>
...\<hookrightarrow>.....<hookrightarrow>
...\<leftharpoondown>.....<leftharpoondown>
...\<rightharpoondown>.....<rightharpoondown>
...\<leftharpoonup>.....<leftharpoonup>
...\<rightharpoonup>.....<rightharpoonup>
...\<rightleftharpoons>.....<rightleftharpoons>
...\<leadsto>.....<leadsto>              abbrev: ~>
...\<downharpoonleft>......<downharpoonleft>
...\<downharpoonright>......<downharpoonright>
...\<upharpoonleft>......<upharpoonleft>
...\<restriction>......<restriction>
...\<Colon>......<Colon>
...\<up>......<up>
...\<Up>......<Up>
...\<down>......<down>
...\<Down>......<Down>
...\<updown>......<updown>
...\<Updown>......<Updown>
*}
subsection{* Delimiters *}
text{*
...\<langle>......<langle>               abbrev: <.
...\<rangle>......<rangle>               abbrev: .>
...\<lceil>......<lceil>
...\<rceil>......<rceil>
...\<lfloor>......<lfloor>
...\<rfloor>......<rfloor>
...\<lparr>......<lparr>                abbrev: (|
...\<rparr>......<rparr>                abbrev: |)
...\<lbrakk>......<lbrakk>               abbrev: [|
...\<rbrakk>......<rbrakk>               abbrev: |]
...\<lbrace>......<lbrace>               abbrev: {.
...\<rbrace>......<rbrace>               abbrev: .}
...\<guillemotleft>......<guillemotleft>        abbrev: <<
...\<guillemotright>......<guillemotright>       abbrev: >>
*}
subsection{* Logic, Etc. *}
text{*
...\<bottom>......<bottom>
...\<top>......<top>
...\<and>......<and>                  abbrev: /\, &
...\<And>......<And>                  abbrev: !!
...\<or>......<or>                   abbrev: \/, |
...\<Or>.....<Or>                    abbrev: ??
...\<forall>......<forall>               abbrev: !, ALL
...\<exists>......<exists>               abbrev: ?, EX
...\<nexists>......<nexists>              abbrev: ~?
...\<not>......<not>                  abbrev: ~
...\<box>......<box>
...\<diamond>......<diamond>
...\<turnstile>......<turnstile>            abbrev: |-
...\<Turnstile>.....<Turnstile>             abbrev: |=
...\<tturnstile>......<tturnstile>           abbrev: ||-
...\<TTurnstile>.....<TTurnstile>           abbrev: ||=
...\<stileturn>......<stileturn>            abbrev: -|
*}
subsection{* Relations, Etc. *}
text{*
...\<surd>......<surd>
...\<le>......<le>                   abbrev: <=
...\<ge>......<ge>                   abbrev: >=
...\<lless>.....<lless>
...\<ggreater>.....<ggreater>
...\<lesssim>......<lesssim>
...\<greatersim>......<greatersim>
...\<lessapprox>......<lessapprox>
...\<greaterapprox>......<greaterapprox>
*}
subsection{* Sets *}
text{*
...\<in>......<in>                   abbrev: :
...\<notin>......<notin>                abbrev: ~:
...\<subset>......<subset>
...\<supset>......<supset>
...\<subseteq>......<subseteq>             abbrev: (=
...\<supseteq>......<supseteq>             abbrev: =)
...\<sqsubset>......<sqsubset>
...\<sqsupset>......<sqsupset>
...\<sqsubseteq>......<sqsubseteq>           abbrev: [=
...\<sqsupseteq>......<sqsupseteq>           abbrev: =]
...\<inter>......<inter>                abbrev: Int
...\<Inter>......<Inter>                abbrev: Inter
...\<union>......<union>                abbrev: Un
...\<Union>......<Union>                abbrev: Union
...\<squnion>......<squnion>
...\<Squnion>......<Squnion>
...\<sqinter>......<sqinter>
...\<Sqinter>......<Sqinter>
...\<setminus>......<setminus>
...\<propto>......<propto>
...\<uplus>......<uplus>
...\<Uplus>......<Uplus>
*}
subsection{* Relations, Etc. *}
text{*
...\<noteq>......<noteq>                abbrev: ~=
...\<sim>......<sim>
...\<doteq>......<doteq>
...\<simeq>......<simeq>
...\<approx>......<approx>
...\<asymp>......<asymp>
...\<cong>......<cong>
...\<smile>......<smile>
...\<equiv>......<equiv>                abbrev: ==
...\<frown>.....<frown>
...\<Join>......<Join>
...\<bowtie>......<bowtie>
...\<prec>......<prec>
...\<succ>......<succ>
...\<preceq>......<preceq>
...\<succeq>......<succeq>
...\<parallel>......<parallel>             abbrev: ||
*}
subsection{* Operators, Etc. *}
text{*
...\<bar>......<bar>
...\<plusminus>......<plusminus>
...\<minusplus>......<minusplus>
...\<times>......<times>
...\<div>......<div>
...\<cdot>......<cdot>
...\<star>......<star>
...\<bullet>......<bullet>
...\<circ>......<circ>
...\<dagger>......<dagger>
...\<ddagger>......<ddagger>
...\<lhd>......<lhd>
...\<rhd>......<rhd>
...\<unlhd>......<unlhd>
...\<unrhd>......<unrhd>
...\<triangleleft>......<triangleleft>
...\<triangleright>......<triangleright>
...\<triangle>......<triangle>
...\<triangleq>......<triangleq>
...\<oplus>......<oplus>                abbrev: +o
...\<Oplus>.....<Oplus>                abbrev: +O
...\<otimes>......<otimes>               abbrev: *o
...\<Otimes>.....<Otimes>               abbrev: *O
...\<odot>......<odot>                 abbrev: .o
...\<Odot>.....<Odot>                 abbrev: .O
...\<ominus>......<ominus>               abbrev: -o
...\<oslash>......<oslash>               abbrev: /o
...\<dots>.....<dots>                 abbrev: ...
...\<cdots>.....<cdots>
...\<Sum>.....<Sum>                  abbrev: SUM
...\<Prod>.....<Prod>                 abbrev: PROD
...\<Coprod>.....<Coprod>
...\<infinity>.....<infinity>
...\<integral>......<integral>
...\<ointegral>......<ointegral>
...\<clubsuit>......<clubsuit>
...\<diamondsuit>......<diamondsuit>
...\<heartsuit>......<heartsuit>
...\<spadesuit>......<spadesuit>
...\<aleph>......<aleph>
...\<emptyset>......<emptyset>
...\<nabla>......<nabla>
...\<partial>......<partial>
...\<Re>......<Re>
...\<Im>......<Im>
*}
subsection{* Symbols, Etc. *}
text{*
...\<flat>......<flat>
...\<natural>......<natural>
...\<sharp>......<sharp>
...\<angle>......<angle>
...\<copyright>......<copyright>
...\<registered>......<registered>
...\<hyphen>......<hyphen>
...\<inverse>......<inverse>
...\<onesuperior>......<onesuperior>
...\<onequarter>......<onequarter>
...\<twosuperior>......<twosuperior>
...\<onehalf>......<onehalf>
...\<threesuperior>......<threesuperior>
...\<threequarters>......<threequarters>
...\<ordfeminine>......<ordfeminine>
...\<ordmasculine>......<ordmasculine>
...\<section>......<section>
...\<paragraph>......<paragraph>
...\<exclamdown>......<exclamdown>
...\<questiondown>......<questiondown>
...\<euro>......<euro>
...\<pounds>......<pounds>
...\<yen>......<yen>
...\<cent>......<cent>
...\<currency>......<currency>
...\<degree>......<degree>
...\<amalg>......<amalg>
...\<mho>......<mho>
...\<lozenge>......<lozenge>
...\<wp>......<wp>
...\<wrong>.......<wrong>
...\<struct>......<struct>
...\<acute>......<acute>
...\<index>......<index>
...\<dieresis>......<dieresis>
...\<cedilla>......<cedilla>
...\<hungarumlaut>......<hungarumlaut>
...\<some>......<some>
*}
subsection{* Subscripts & Superscripts *}
text{*
...\<^sub>.......<^sub>                 abbrev: =_
...\<^sup>.......<^sup>                 abbrev: =^
...\<^isub>.......<^isub>                abbrev: -_
...\<^isup>.......<^isup>                abbrev: -^
...\<^bsub>......<^bsub>                abbrev: =_(
...\<^esub>......<^esub>                abbrev: =_)
...\<^bsup>......<^bsup>                abbrev: =^(
...\<^esup>......<^esup>                abbrev: =^)
...\<^bold>.......<^bold>                abbrev: -.
*}

section{* OPERATOR PRIORITY: 2012 HOL *}
--{*                                                                   02ho = src/HOL.thy                           *}
--{*       PRIORITY                                                    FILE-LINE                       WHY INTRODUCED
           __01__                                             *}--{*-----------------------------------
=simp=...................[prop, prop] => prop..........................02ho 1843 (infixr "=simp=>" 1)  definition
           __05__                                             *}--{*-----------------------------------
Trueprop.................bool => prop..................................02ho 0067 ("(_)" 5)             judgment
If.......................bool => 'a => 'a => 'a........................02ho 0189 ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10)   definition
           __10__                                             *}--{*-----------------------------------
_bind....................[pttrn, 'a] => letbind........................02ho 0129 ("(2_ =/ _)" 10)      syntax
_case_syntax.............['a, cases_syn] => 'b.........................02ho 0136 ("(case _ of/ _)" 10) syntax
_case1...................['a, 'b] => case_syn..........................02ho 0137 ("(2_ =>/ _)" 10)     syntax
                                                                       02ho 0141 ("(2_ \<Rightarrow>/ _)" 10)     xsymbols
_Let.....................[letbinds, 'a] => 'a..........................02ho 0132 ("(let (_)/ in (_))" [0, 10] 10)   syntax
_The.....................[pttrn, bool] => 'a...........................02ho 0119 ("(3THE _./ _)" [0, 10] 10)        syntax
All......................('a => bool) => bool..........................02ho 0082 (binder "ALL " 10)    consts
                                                                       02ho 0144 (binder "\<forall>" 10)       xsymbols
                                                                       02ho 0149 (binder "\<forall>" 10)       HTML
                                                                       02ho 0154 (binder "! " 10)      HOL
Ex.......................('a => bool) => bool..........................02ho 0083 (binder "EX " 10)     consts
                                                                       02ho 0145 (binder "\<exists>" 10)       xsymbols
                                                                       02ho 0150 (binder "\<exists>" 10)       HTML
                                                                       02ho 0155 (binder "? " 10)      HOL
Ex1......................('a => bool) => bool..........................02ho 0084 (binder "EX! " 10)    consts
                                                                       02ho 0146 (binder "\<exists>!" 10)      xsymbols
                                                                       02ho 0151 (binder "\<exists>!" 10)      HTML
                                                                       02ho 0156 (binder "?! " 10)     HOL
           __25__                                             *}--{*-----------------------------------
implies..................[bool, bool] => bool..........................02ho 0070 (infixr "-->" 25)     axiomatization
                                                                       02ho 0103 (infixr "\<longrightarrow>" 25)     xsymbols
iff......................[bool, bool] => bool..........................02ho 0113 (infixr "<->" 25)     abbreviation
                                                                       02ho 0117 (infixr "\<longleftrightarrow>" 25)     xsymbols
           __30__                                             *}--{*-----------------------------------
disj.....................[bool, bool] => bool..........................02ho 0080 (infixr "|" 30)      consts
                                                                       02ho 0102 (infixr "\<or>" 30)      xsymbols
                                                                       02ho 0109 (infixr "\<or>" 30)      HTML
           __35__                                             *}--{*-----------------------------------
conj.....................[bool, bool] => bool..........................02ho 0079 (infixr "&" 35)      consts
                                                                       02ho 0101 (infixr "\<and>" 35)      xsymbols
                                                                       02ho 0108 (infixr "\<and>" 35)      HTML
           __40__                                             *}--{*-----------------------------------
Not......................bool => bool..................................02ho 0077 ("~ _" [40] 40)      consts
                                                                       02ho 0100 ("\<not> _" [40] 40)      xsymbols
                                                                       02ho 0107 ("\<not> _" [40] 40)      HTML
           __50__                                             *}--{*-----------------------------------
eq.......................['a, 'a] => bool..............................02ho 0071 (infixl "=" 50)      axiomatization
                                                                       02ho 0090 (infix "=" 50)       output
not_equal................['a, 'a] => bool..............................02ho 0093 (infixl "~=" 50)     abbreviation
                                                                       02ho 0097 (infix "~=" 50)      output
                                                                       02ho 0104 (infix "\<noteq>" 50)       xsymbols
                                                                       02ho 0110 (infix "\<noteq>" 50)       HTML
*}

section{* PRIORITY: 2012 PURE *}
text{* From ~~/src/Pure/pure_thy.ML

(*  Title:      Pure/pure_thy.ML
    Author:     Markus Wenzel, TU Muenchen

Pure theory syntax and further logical content.
*)

signature PURE_THY =
sig
  val old_appl_syntax: theory -> bool
  val old_appl_syntax_setup: theory -> theory
end;

structure Pure_Thy: PURE_THY =
struct

val typ = Simple_Syntax.read_typ;
val prop = Simple_Syntax.read_prop;

val tycon = Lexicon.mark_type;
val const = Lexicon.mark_const;


(* application syntax variants *)

val appl_syntax =
 [("_appl", typ "('b => 'a) => args => logic", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000)),
  ("_appl", typ "('b => 'a) => args => aprop", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000))];

val applC_syntax =
 [("",       typ "'a => cargs",                  Delimfix "_"),
  ("_cargs", typ "'a => cargs => cargs",         Mixfix ("_/ _", [1000, 1000], 1000)),
  ("_applC", typ "('b => 'a) => cargs => logic", Mixfix ("(1_/ _)", [1000, 1000], 999)),
  ("_applC", typ "('b => 'a) => cargs => aprop", Mixfix ("(1_/ _)", [1000, 1000], 999))];

structure Old_Appl_Syntax = Theory_Data
(
  type T = bool;
  val empty = false;
  val extend = I;
  fun merge (b1, b2) : T =
    if b1 = b2 then b1
    else error "Cannot merge theories with different application syntax";
);

val old_appl_syntax = Old_Appl_Syntax.get;

val old_appl_syntax_setup =
  Old_Appl_Syntax.put true #>
  Sign.del_modesyntax_i Syntax.mode_default applC_syntax #>
  Sign.add_syntax_i appl_syntax;


(* main content *)

val _ = Context.>> (Context.map_theory
  (Sign.map_naming (Name_Space.set_theory_name Context.PureN) #>
   Old_Appl_Syntax.put false #>
   Sign.add_types_global
   [(Binding.name "fun", 2, NoSyn),
    (Binding.name "prop", 0, NoSyn),
    (Binding.name "itself", 1, NoSyn),
    (Binding.name "dummy", 0, NoSyn)]
  #> Sign.add_nonterminals_global (map Binding.name Syntax.basic_nonterms)
  #> Sign.add_syntax_i (map (fn x => (x, typ "'a", NoSyn)) Syntax.token_markers)
  #> Sign.add_syntax_i
   [("",            typ "prop' => prop",               Delimfix "_"),
    ("",            typ "logic => any",                Delimfix "_"),
    ("",            typ "prop' => any",                Delimfix "_"),
    ("",            typ "logic => logic",              Delimfix "'(_')"),
    ("",            typ "prop' => prop'",              Delimfix "'(_')"),
    ("_constrain",  typ "logic => type => logic",      Mixfix ("_::_", [4, 0], 3)),
    ("_constrain",  typ "prop' => type => prop'",      Mixfix ("_::_", [4, 0], 3)),
    ("",            typ "tid => type",                 Delimfix "_"),
    ("",            typ "tvar => type",                Delimfix "_"),
    ("",            typ "type_name => type",           Delimfix "_"),
    ("_type_name",  typ "id => type_name",             Delimfix "_"),
    ("_type_name",  typ "longid => type_name",         Delimfix "_"),
    ("_ofsort",     typ "tid => sort => type",         Mixfix ("_::_", [1000, 0], 1000)),
    ("_ofsort",     typ "tvar => sort => type",        Mixfix ("_::_", [1000, 0], 1000)),
    ("_dummy_ofsort", typ "sort => type",              Mixfix ("'_()::_", [0], 1000)),
    ("",            typ "class_name => sort",          Delimfix "_"),
    ("_class_name", typ "id => class_name",            Delimfix "_"),
    ("_class_name", typ "longid => class_name",        Delimfix "_"),
    ("_topsort",    typ "sort",                        Delimfix "{}"),
    ("_sort",       typ "classes => sort",             Delimfix "{_}"),
    ("",            typ "class_name => classes",       Delimfix "_"),
    ("_classes",    typ "class_name => classes => classes", Delimfix "_,_"),
    ("_tapp",       typ "type => type_name => type",   Mixfix ("_ _", [1000, 0], 1000)),
    ("_tappl",      typ "type => types => type_name => type", Delimfix "((1'(_,/ _')) _)"),
    ("",            typ "type => types",               Delimfix "_"),
    ("_types",      typ "type => types => types",      Delimfix "_,/ _"),
    ("\\<^type>fun", typ "type => type => type",       Mixfix ("(_/ => _)", [1, 0], 0)),
    ("_bracket",    typ "types => type => type",       Mixfix ("([_]/ => _)", [0, 0], 0)),
    ("",            typ "type => type",                Delimfix "'(_')"),
    ("\\<^type>dummy", typ "type",                     Delimfix "'_"),
    ("_type_prop",  typ "'a",                          NoSyn),
    ("_lambda",     typ "pttrns => 'a => logic",       Mixfix ("(3%_./ _)", [0, 3], 3)),
    ("_abs",        typ "'a",                          NoSyn),
    ("",            typ "'a => args",                  Delimfix "_"),
    ("_args",       typ "'a => args => args",          Delimfix "_,/ _"),
    ("",            typ "id_position => idt",          Delimfix "_"),
    ("_idtdummy",   typ "idt",                         Delimfix "'_"),
    ("_idtyp",      typ "id_position => type => idt",  Mixfix ("_::_", [], 0)),
    ("_idtypdummy", typ "type => idt",                 Mixfix ("'_()::_", [], 0)),
    ("",            typ "idt => idt",                  Delimfix "'(_')"),
    ("",            typ "idt => idts",                 Delimfix "_"),
    ("_idts",       typ "idt => idts => idts",         Mixfix ("_/ _", [1, 0], 0)),
    ("",            typ "idt => pttrn",                Delimfix "_"),
    ("",            typ "pttrn => pttrns",             Delimfix "_"),
    ("_pttrns",     typ "pttrn => pttrns => pttrns",   Mixfix ("_/ _", [1, 0], 0)),
    ("",            typ "aprop => aprop",              Delimfix "'(_')"),
    ("",            typ "id_position => aprop",        Delimfix "_"),
    ("",            typ "longid_position => aprop",    Delimfix "_"),
    ("",            typ "var => aprop",                Delimfix "_"),
    ("_DDDOT",      typ "aprop",                       Delimfix "..."),
    ("_aprop",      typ "aprop => prop",               Delimfix "PROP _"),
    ("_asm",        typ "prop => asms",                Delimfix "_"),
    ("_asms",       typ "prop => asms => asms",        Delimfix "_;/ _"),
    ("_bigimpl",    typ "asms => prop => prop",        Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
    ("_ofclass",    typ "type => logic => prop",       Delimfix "(1OFCLASS/(1'(_,/ _')))"),
    ("_mk_ofclass", typ "dummy",                       NoSyn),
    ("_TYPE",       typ "type => logic",               Delimfix "(1TYPE/(1'(_')))"),
    ("",            typ "id_position => logic",        Delimfix "_"),
    ("",            typ "longid_position => logic",    Delimfix "_"),
    ("",            typ "var => logic",                Delimfix "_"),
    ("_DDDOT",      typ "logic",                       Delimfix "..."),
    ("_strip_positions", typ "'a", NoSyn),
    ("_position",   typ "num_token => num_position",   Delimfix "_"),
    ("_position",   typ "float_token => float_position", Delimfix "_"),
    ("_position",   typ "xnum_token => xnum_position", Delimfix "_"),
    ("_constify",   typ "num_position => num_const",   Delimfix "_"),
    ("_constify",   typ "float_position => float_const", Delimfix "_"),
    ("_constify",   typ "xnum_position => xnum_const", Delimfix "_"),
    ("_index",      typ "logic => index",              Delimfix "(00\\<^bsub>_\\<^esub>)"),
    ("_indexdefault", typ "index",                     Delimfix ""),
    ("_indexvar",   typ "index",                       Delimfix "'\\<index>"),
    ("_struct",     typ "index => logic",              Mixfix ("\\<struct>_", [1000], 1000)),
    ("_update_name", typ "idt",                        NoSyn),
    ("_constrainAbs", typ "'a",                        NoSyn),
    ("_position",   typ "id => id_position",           Delimfix "_"),
    ("_position",   typ "longid => longid_position",   Delimfix "_"),
    ("_position",   typ "str_token => str_position",   Delimfix "_"),
    ("_type_constraint_", typ "'a",                    NoSyn),
    ("_context_const", typ "id_position => logic",     Delimfix "CONST _"),
    ("_context_const", typ "id_position => aprop",     Delimfix "CONST _"),
    ("_context_const", typ "longid_position => logic", Delimfix "CONST _"),
    ("_context_const", typ "longid_position => aprop", Delimfix "CONST _"),
    ("_context_xconst", typ "id_position => logic",    Delimfix "XCONST _"),
    ("_context_xconst", typ "id_position => aprop",    Delimfix "XCONST _"),
    ("_context_xconst", typ "longid_position => logic", Delimfix "XCONST _"),
    ("_context_xconst", typ "longid_position => aprop", Delimfix "XCONST _"),
    (const "==>",   typ "prop => prop => prop",        Delimfix "op ==>"),
    (const Term.dummy_patternN, typ "aprop",           Delimfix "'_"),
    ("_sort_constraint", typ "type => prop",           Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
    (const "Pure.term", typ "logic => prop",           Delimfix "TERM _"),
    (const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]
  #> Sign.add_syntax_i applC_syntax
  #> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
   [(tycon "fun",         typ "type => type => type",   Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
    ("_bracket",          typ "types => type => type",  Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
    ("_ofsort",           typ "tid => sort => type",    Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
    ("_constrain",        typ "logic => type => logic", Mixfix ("_\\<Colon>_", [4, 0], 3)),
    ("_constrain",        typ "prop' => type => prop'", Mixfix ("_\\<Colon>_", [4, 0], 3)),
    ("_idtyp",            typ "id_position => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
    ("_idtypdummy",       typ "type => idt",            Mixfix ("'_()\\<Colon>_", [], 0)),
    ("_lambda",           typ "pttrns => 'a => logic",  Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
    (const "==",          typ "'a => 'a => prop",       Infixr ("\\<equiv>", 2)),
    (const "all_binder",  typ "idts => prop => prop",   Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),
    (const "==>",         typ "prop => prop => prop",   Infixr ("\\<Longrightarrow>", 1)),
    ("_DDDOT",            typ "aprop",                  Delimfix "\\<dots>"),
    ("_bigimpl",          typ "asms => prop => prop",   Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
    ("_DDDOT",            typ "logic",                  Delimfix "\\<dots>")]
  #> Sign.add_modesyntax_i ("", false)
   [(const "prop", typ "prop => prop", Mixfix ("_", [0], 0))]
  #> Sign.add_modesyntax_i ("HTML", false)
   [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
  #> Sign.add_consts_i
   [(Binding.name "==", typ "'a => 'a => prop", Infixr ("==", 2)),
    (Binding.name "==>", typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
    (Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)),
    (Binding.name "prop", typ "prop => prop", NoSyn),
    (Binding.name "TYPE", typ "'a itself", NoSyn),
    (Binding.name Term.dummy_patternN, typ "'a", Delimfix "'_")]
  #> Theory.add_deps_global "==" ("==", typ "'a => 'a => prop") []
  #> Theory.add_deps_global "==>" ("==>", typ "prop => prop => prop") []
  #> Theory.add_deps_global "all" ("all", typ "('a => prop) => prop") []
  #> Theory.add_deps_global "TYPE" ("TYPE", typ "'a itself") []
  #> Theory.add_deps_global Term.dummy_patternN (Term.dummy_patternN, typ "'a") []
  #> Sign.add_trfuns Syntax_Trans.pure_trfuns
  #> Sign.local_path
  #> Sign.add_consts_i
   [(Binding.name "term", typ "'a => prop", NoSyn),
    (Binding.name "sort_constraint", typ "'a itself => prop", NoSyn),
    (Binding.name "conjunction", typ "prop => prop => prop", NoSyn)]
  #> (Global_Theory.add_defs false o map Thm.no_attributes)
   [(Binding.name "prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"),
    (Binding.name "term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
    (Binding.name "sort_constraint_def",
      prop "(CONST Pure.sort_constraint :: 'a itself => prop) (CONST TYPE :: 'a itself) ==\
      \ (CONST Pure.term :: 'a itself => prop) (CONST TYPE :: 'a itself)"),
    (Binding.name "conjunction_def", prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
  #> Sign.hide_const false "Pure.term"
  #> Sign.hide_const false "Pure.sort_constraint"
  #> Sign.hide_const false "Pure.conjunction"
  #> Global_Theory.add_thmss [((Binding.name "nothing", []), [])] #> snd
  #> fold (fn (a, prop) =>
      snd o Thm.add_axiom_global (Binding.name a, prop)) Proofterm.equality_axms));

end;

*}

end


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