Hallo, > The main thing still missing in Isabelle/5ccee1cb245a is a regular ML > interface Fun_Cases.fun_cases. What do you mean by that? There exists an ML function Fun_Cases.mk_fun_cases : Proof.context -> term -> thm -- is that not an ML interface to the Fun_Cases tool? Or do you also want a function that registers the resulting theorem with a given name, as the fun_cases command does?
> 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.) The reason for this was that I wanted to be able to use dummy patterns in the input terms, i.e. write something like "list_to_option xs = Some _". Obviously, it's not hugely important, but it does add a small amount of convenience. I do think that read_props does not support dummy patterns. Cheers, Manuel
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
