I'm trying to define a function that takes a set and a relation and returns a bool telling if the relation is reflexive on the set. I tried to define it like this:
definition refl::"'a set⇒('a×'a) set⇒bool" where
"refl A R = (∀x. x∈A⟹(x,x)∈R)"
but Isabelle gives me the following error:
Type unification failed: Clash of types "prop" and "bool"
Type error in application: incompatible operand type
Operator: (=) (refl A R) :: bool ⇒ bool
Operand: ∀x. x ∈ A ⟹ (x, x) ∈ R :: prop
I can't seem to find any function to force a "prop" into a "bool". I also tried changing the definition to set the RHS = True, but I get the same error. What is the correct way to define my function?
You can't go from prop to bool. But you don't have to: just use the object level connectives (⟶ and ∀) instead of the meta-logical ones (⟹ and ⋀). They are logically equivalent, so this is not a problem.
The meta-logical connectives should (and usually can) only be used on the ‘outermost level’ of a proposition.
Note however that when you can use the mega-logical ones, it is usually more convenient to use them because the object-level ones are opaque to Isabelle and the Isar proof language (i.e. they are functions just like any other function) whereas Isar ‘knows’ what ⟹ and ⋀ mean. For instance, if you have a fact stated with ⟹ and ⋀, you can immediately instantiate variables and discharge assumptions in it using the of/OF attributes.