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,
>                            "ArraysMemInstance.fourthousand_count")
>     val subrel_th =
>         Goal.prove_raw [] (cterm_of thy subrel_t) (tac thy [])
>   in
>     AxClass.add_classrel subrel_th thy before
>     writeln("Proved " ^ nclass ^ " < fourthousand_count")
>   end
> 
> produces the following error:
> 
> Exception-
>    THM
>       ("add_classrel: malformed class relation",
>          0,
>          ["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.


	Makarius





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