types - saving a datatype before fixing additional variable in Isabelle/HOL

Question

I'm fairly new to Isabelle and I'm having some trouble with typing: I would like to have two separate, but overlapping types, let's say 'a and 'b. Thinking of them as sets, I would like to have 'b = 'a cup {tau} for a specific tau that doesn't appear in 'a. As I understand it, you can expand a type using "fixes tau :: 'a" in Isabelle, but it seems like then the original type 'a (without tau) gets lost: Current Isabelle code using fixes

I need both types for my later formulation, so is there a way to "save" the state of 'a before fixing tau to it?

Any help would be greatly appreciated!

question from:https://stackoverflow.com/questions/65903299/saving-a-datatype-before-fixing-additional-variable-in-isabelle-hol

Answer 1

You are misunderstanding locales. Fixes introduces constants of a certain type. Remember what a locale means:

locale t =
   fixes x
   assumes "P x"
begin

lemma b: Q 
  sorry

means that "!!x. P x ==> Q". You are not extending types.

About the actual question: you cannot extend types directly or express that directly in HOL. It is impossible to do so. There are two solutions to extend types in practice:

• a datatype datatype 'a myunion = Either1 'a | Tau. In that case, it is actually isomorphic to 'a option.
• union types (see here for another SO question on the topic)