Re: [isabelle] programmatically adding a class relation
On Thu, 23 Aug 2007, Michael Norrish wrote:
> val thy = let
> val subrel_t =
> Logic.mk_classrel (nclass,
> val subrel_th =
> Goal.prove_raw  (cterm_of thy subrel_t) (tac thy )
> AxClass.add_classrel subrel_th thy before
> writeln("Proved " ^ nclass ^ " < fourthousand_count")
> produces the following error:
> ("add_classrel: malformed class relation",
> ["OFCLASS('a, fourthousand_count_class)"]) raised
> The theorem is proved, but then add_classrel complains. What should I
> do differently?
AxClass.add_classrel refers to Logic.dest_classrel internally, which
expectes results in canonical form, with generalized variables. In
contrast Logic.mk_classrel produces a fixed form, because this is what you
need during the proof.
Normally the system converts between fixed and arbitrary variables
transparently, but this requires use of higher-level goal interfaces
rather than Goal.prove_raw. See AxClass.prove_classrel (in
src/Pure/axclass.ML) of how to do something like that.
This archive was generated by a fusion of
Pipermail (Mailman edition) and