CODEWITHSUNDEEP
isabelle
Denis
Denis

Reputation: 1271

How to define an inductive predicate inside locale?

Here is an example of a simple locale:

locale test =
  fixes test_less_eq :: "'a ⇒ 'a ⇒ bool"
begin

inductive test_eq where
  "test_less_eq x y ⟹ test_less_eq y x ⟹ test_eq x y"

end

It defines inductive test_eq. It can be defined using definition, but I need it to be an inductive predicate.

Then I define a trivial interpretation of the locale and try to use it:

interpretation interp: test "op <" .

inductive some_pred where
  "interp.test_eq x y ⟹
   some_pred x y"

code_pred [show_modes] some_pred .

The problem is that I get the following error for code_pred:

Type mismatch of predicate test.test_eq (trying to match ?'a
                   ⇒ ?'a ⇒ bool and ('a ⇒ 'a ⇒ bool)
                                      ⇒ 'a ⇒ 'a ⇒ bool) in ?x1 < ?y1 ⟹
          ?y1 < ?x1 ⟹ interp.test_eq ?x1 ?y1

What is a cause of the error and how to fix it?

Upvotes: 0

Views: 84

Answers (1)

Andreas Lochbihler
Andreas Lochbihler

Reputation: 5058

The predicate compiler has never been localized, i.e., it cannot directly deal with predicates that are defined inside a locale. There are two ways to make this work nevertheless.

Either, use global_interpretation with a defines clause to introduce a new constant for the predicate (plain interpretation only introduces an abbreviation). Then, you also have to re-declare the introduction rules to code_pred and prove the corresponding elimination rule.

global_interpretation interp: test "op <" 
  defines interp_test_eq = interp.test_eq .

declare interp.test_eq.intros[code_pred_intro]

code_pred interp_test_eq by(rule interp.test_eq.cases)

Or, leave the interpretation as is and re-declare the introduction rules of the internal constant to which the definition in the locale is mapped. This is <locale_name>.<predicate_name>, i.e., test.test_eq in your case. This works only if your locale has no assumption.

declare test.test_eq.intros[code_pred_intro]

code_pred test.test_eq by(rule test.test_eq.cases)

Upvotes: 1

Related Questions