Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] programmatically adding a class relation

Email Gateway (Aug 18 2022 at 10:45):

From: Michael Norrish <michael.norrish@nicta.com.au>
The following code

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?

Michael.

Email Gateway (Aug 18 2022 at 10:46):

From: Makarius <makarius@sketis.net>
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

Email Gateway (Aug 18 2022 at 10:46):

From: Michael Norrish <michael.norrish@nicta.com.au>
Makarius wrote:

Thanks. Indeed, I should have been using prove_classrel all along.

Michael.

Last updated: May 03 2024 at 04:19 UTC