On Fri, 13 Sep 2013, Alexander Krauss wrote:
This refers to Isabelle f557a4645f61:
* New command "fun_cases" derives ad-hoc elimination rules for
function equations as simplified instances of f.elims, analogous to
inductive_cases. See HOL/ex/Fundefs.thy for some examples.
Thanks. I see that you have already provided canonical entries for NEWS
and CONTRIBUTORS, as appropriate for the relase.
Doing some other routine maintenance elsewhere, I've come across the
sources of HOL/Tools/Function/fun_cases.ML and
HOL/Tools/Function/function_elims.ML today and got stuck there -- that
also needs to be consolidated in the remaining weeks before the relase.
The main thing still missing in Isabelle/5ccee1cb245a is a regular ML
interface Fun_Cases.fun_cases.
Manuel is one of many people who have picked up the wrong terminology of
"the ML level of Isabelle" elsewhere, and fell into a corresponding trap
like so many other people did for the first time writing their own tools
in Isabelle/ML. (This is not a problem, if lessons are learned from it.)
Since most Isabelle users use Isar syntax most of the time, one might get
the idea that everything is Isar syntax. This is not the case. On the
contrary, Isabelle/Isar consists mainly of Isabelle/ML interfaces with a
thin layer of concrete syntax on top. Whatever tool is built, it requires
first and foremost a proper ML interface, such that it can be re-used
routinely to build further tools. Concrete syntax is merely a convenient
add-on, which is usually provided as well, but not abolutely mandatory.
Since we've had some interesting discussions about Isabelle in the mid
1990-ies on isabelle-users recently, and there is also the new high-end
(co)datatype package becoming mainstream in Isabelle2013-1, it might be
interesting to look at the 1995 version of HOL/datatype here:
http://isabelle.in.tum.de/repos/Old_HOL/file/9b403e123c1b/datatype.ML#l435
This is how some add-on tool struggles with string-only "interfaces". It
pastes together strings for concrete syntax parsers for types, consts,
axioms, and hopes for the best. (In current Isabelle one could always use
YXML to force terms down the throat of tools without proper ML interfaces,
but this should be the last resort.)
Anyway, looking briefly what is missing for the regular ML version of
Fun_Cases.fun_cases, I fell over another stumbling block: the use of
Proof_Context.read_term_pattern and pat_to_term.
Manuel, can you say what is the idea and purpose behind it?
From the existing inductive_cases and inductive_simps, it looks like plain
Syntax.read_props together with Variable.auto_fixes would do the job, as
is done in the analogous Inductive.mk_cases and Inductive.mk_simp_eq.
(These things are non-trivial, and I always need to look myself carefully
how things really work.)
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
