Re: [isabelle] Parametric theories
On Wed, 18 Apr 2012, Daniel Schoepe wrote:
I could construct a type_synonym that needs to be applied to some
parameters, but then I'd still have to write "('a, 'b, 'c, 'd)
Yes, that's the normal way. Moreover, you can often suppress type
information in the input, say you write some of the type arguments as "_"
and let type inference take care of the rest. Or you don't write types at
BTW, most names in Isabelle are normally just lower case like "foo_bar",
including type names. Capitalization like Foo_Bar is always used for
theory names, datatype constructors, and sometimes for special operators.
Camel-case is generally out of fashion.
A related issue I'm curious about: What was the rationale for
introducing typedecl without a straight-forward way to instantiate it?
Being able to define something that has only been declared earlier seems
rather natural to me.
The classic canon for axiomatic specifications consists of typedecl,
consts, axioms. You can do whatever you want here, but there are no
sanity checks. For example you can first "declare" some types, and then
"define" them -- all axiomatically. Here is an old example from HOL/Bali
Historically, Isabelle theories were always axiomatic like that. Later
the vacous axiomatization of 'consts' followed by a definitional
axiomatization of 'defs' (i.e. 'axioms' with some checks) were called
Much later, an actual definitional concept was made the main principle of
the local theory infrastructure that is commonplace today. It performs
the usual simultaneous declaration-definition of entities seen in most
other provers and in mathematics. There are also technical and conceptual
reasons for it -- definitions that depend on local contexts work out
better if the RHS is explicitly given.
The surface syntax wraps up these truly definitional primitives as
'definition', 'function', 'induction' etc. For types, this is still a bit
limited, though. (Back to start of thread.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and