CODEWITHSUNDEEP
typesbooleanpredicatedefinitionisabelle
Jonathan Julian
Jonathan Julian

Reputation: 125

How to do an inductive definition over "booleans" in Isabelle

In Isabelle, I want to define operators that take predicates 'a => bool and modify them based on the "inductive structure of predicates". For example, one might want to compute the Disjunctive Normal Form (DNF) on these predicates, e.g. D (λ x. P x --> Q x) = (λ x. ¬ P x \/ Q x).

The problem here is that bool is not an inductive datatype. I have thought of two possible solutions:

  1. Create an inductive datatype that allows me to define my operators on them. Give predicate (P::'a => bool) semantics for this datatype and then use it to prove the lemmas I want to check.
  2. Prove the theorems for each one of the possible inductive cases. Then show a general case that uses all of the previous rules.

As a third option, I am (wishfully) hoping that a more experienced Isabelle user might enlighten my approach with a secret function/typedef that circumvents this "inductive issue". So the questions here are:

Are there any other simpler options? If yes, which ones? If not, do any of my approaches seem flawed or doomed?

WARNING: I gave as an example, the DNF, however, the general case where the operator does not necessarily preserve the truth value of the predicate is of more interest to me, e.g. D could do this: D (λ x. P x /\ Q x) = (λ x. P x \/ Q x).

Upvotes: 1

Views: 456

Answers (1)

Andreas Lochbihler
Andreas Lochbihler

Reputation: 5108

HOL functions cannot look into the syntactic representation of their arguments. The reason is the substitution axiom, i.e., logically equal terms may be replaced in any context. Otherwise, one could define a function D satisfying D (λ x. P x) = True and D (λ x. P x & True) = False, which leads to a proof of False.

For a function like conversion to DNF, whose semantics in HOL does not depend on the syntax of the argument, one can still define such a transformation. For the DNF conversion, the semantic operation is the identity, i.e.,

definition DNF :: "('a => bool) => ('a => bool)" where "D = id"

Then, you can derive rewriting rules that actually perform the conversion. For example,

lemma DNF_imp: "DNF (λx. P x --> Q x) = DNF (λx. ~ P x | Q x)"

If you call Isabelle's simplifier with such a dedicated set of rules, you effectively get a conversion into DNF (although you will never ever be able to formally express in HOL that your set of rules works in all cases).

Very often, rules like DNF_imp are not enough to implement such a function. In that case, you can write a simproc in Isabelle/ML which triggers on DNF _ terms and performs the transformation. Since you are stepping out of the logic, the simproc can look at the HOL syntax of the argument and behave differently for logically equal terms.

Conversely, if you do want to express and reason about the conversion function D within the logic, there is no way around to introduce syntax to work on, as you have suggested with a datatype.

Upvotes: 3

Related Questions