I'm still trying to get my head around equality relations and how to define one in Isabelle. Luckily there is a chapter about this in the isar reference manual 2.3.1 p38f.
I tried to rebuild the given example. To avoid any overlaps with the established syntax i renamed everything. Also i added some quotationmarks, since they seem to be missing in the example.
theory playground
imports Main
begin
typedecl i_play
typedecl u_play
The next step is the judgment i don't really understand, but hey what can go wrong:
judgment
Trueprop :: "u_play => prop" ("_play" 5)
error: Attempt to redeclare object-logic judgment
even renaming Trueprop doesn't yield another result.
Can't i somehow use bool here instead of defining my own object proposition? Or do i need to introduce u_play somewhere else?
But let's go further. The next step is the equality relation, also copied and and renamed.
axiomatization
equal :: "i_play => i_play => u_play" (infix "EQ" 50)
where
refl [intro]: "x EQ x" and
subst [elim]: "x EQ y ⟹ B x ⟹ B y"
This gives an Type unification failed: Clash of types "u_play" and "bool" error. When i replace u_play with bool all is fine and i can even use EQ in something trivial like lemma t : "x EQ x", but the substitutionrule doesn't seem to work, which leads me to the question what are the two B's there. I've seen the same construct in HOL.thy with P's instead and a bit further down the isar rm they are omitted. Just stating impD [dest]: (A --> B) ==> A ==> B
What needs to be done to get the substitution to work?
