[isabelle] making local definitions programmatically



I have a locale L with some number of fixes, f1, f2 and f3, say.

Using LocalTheory.define, I have defined a number of constants in that
locale with eqns

  C1 == rhs1
  C2 == rhs2

some, none or all of the rhs-es may refer to the fixes.  Say each of
C1 and C2 is of type nat.

Subsequently, in the same locale, I want to define a function of the
form

  select b == if b then C1 else C2

I want to build the right-hand side for this definition in ML.

What do I put into the conditional term in the place of C1 and C2?

It would be nice if I could just write

  Const("C1", nat)

and

  Const("C2", nat)

But I guess this won't work, because C1 probably really has a type
that depends on the fixes that appear in rhs1, and likewise C2.
I.e., at the top level, if I do the Isar command

  term "L.C1"

I may see that it really has type "fixtype1 => nat", and L.C2 may have
type "fixtype1 => fixtype2 => nat".

So, what do I do?

Michael.






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