How to deal with "exception Match raised" while computing relation operators in Isabelle?

user_4196578 0
Viewed 89

I couldn't get the right usage for the relation operator refl in Isabelle (2020)'s Main. I assume refl on a relation returns true if it's reflexive, same as the refl_on example above. But I am still learning these notations.

More specifically:

value "refl_on {True,False} {(True,True),(False,False)}"

gives True as expected. I thought the refl is the same, but the following:

value "refl {(True,True),(False,False)}"

gives an error:

exception Match raised (line 39 of "generated code")

Other operators such as sym seems to be fine:

value "sym {(True,True)}"

What is the correct way to use refl here?

-- Update --

There seems to be a similar error with total:

value "total {(True,True),(False,False)}"

, which gives:

exception Match raised (line 39 of "generated code")
isabelle
1 Answers

You should not expect to be able to evaluate everything with value. The value command is a diagnostic command that is fun to play around with and it can occasionally be useful, but Isabelle/HOL is not a programming language and most HOL terms that you write down cannot be evaluated without additional setup.

The machinery that makes evaluation possible at all is the code generator, which translates HOL definitions into executable ML code and then runs that code and converts the result back into HOL terms.

In this case, there is of course no a priori reason why you shouldn't be able to evaluate that term. When things fail, you can either use export_code to look at what code is actually generated for your term:

definition foo where "foo = refl {(True,True),(False,False)}"

export_code foo in SML

Of you can look at the ‘code equations’ used by the code generator

definition foo where "foo = refl {(True,True),(False,False)}"

code_thms foo

It might be a bit difficult to read, but basically the problem is that sets are, by default, implemented through lists, either as set xs (all the elements of the list xs) or as List.coset xs (all the elements not int he list xs) and UNIV has the code equation UNIV = List.coset []. (Note that refl is just an abbreviation for refl_on UNIV).

Unfortunately, the implementation for Ball (the ‘for all elements x of the set x, P(x) holds’ operator) does not know what to do with List.coset.

A quick workaround here is to add (UNIV :: bool set) = {True, False} as a code_unfold rule so that the code generator uses that instead. And with that, it works!

lemma UNIV_bool [code_unfold]: "UNIV = {True, False}"
  by auto
user_21442270
Related