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) SomeSynonym".

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 all.

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 http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2011-1/src/HOL/Bali/Example.thy#l66

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 definitions.


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.)


	Makarius





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