How to use different code lemmas for different modes of inductive predicate?

Question

(The question is related to How to define an inductive predicate on fset? but a more concrete)

Here is a simple theory with 2 kinds of values and a casting predicate:

theory FSetIndTest
  imports Main "~~/src/HOL/Library/FSet"
begin

datatype val1 = A | B
datatype val2 = C | D

inductive cast_val :: "val1 ⇒ val2 ⇒ bool" where
  "cast_val A C"
| "cast_val B D"

code_pred [show_modes] cast_val .

fun cast_val_fun :: "val1 ⇒ val2" where
  "cast_val_fun A = C"
| "cast_val_fun B = D"

fun cast_val_fun_inv :: "val2 ⇒ val1" where
  "cast_val_fun_inv C = A"
| "cast_val_fun_inv D = B"

I'm trying to define a cast predicate for fsets. It works fine in i ⇒ o ⇒ bool mode, but doesn't support o ⇒ i ⇒ bool mode:

inductive cast_fset1 :: "val1 fset ⇒ val2 fset ⇒ bool" where
  "cast_fset1 {||} {||}"
| "cast_val x y ⟹ cast_fset1 xs ys ⟹
   cast_fset1 (finsert x xs) (finsert y ys)"

lemma cast_fset1_left [code_pred_intro]:
  "fimage cast_val_fun xs = ys ⟹ cast_fset1 xs ys"
  apply (induct xs arbitrary: ys)
  apply (simp add: cast_fset1.intros(1))
  by (metis (full_types) cast_fset1.intros(2) cast_val.intros(1) cast_val.intros(2) cast_val_fun.simps(1) cast_val_fun.simps(2) fimage_finsert val1.exhaust)

lemma cast_fset1_left_inv:
  "cast_fset1 xs ys ⟹
   fimage cast_val_fun xs = ys"
  apply (induct rule: cast_fset1.induct)
  apply simp
  using cast_val.simps by auto

code_pred [show_modes] cast_fset1
  by (simp add: cast_fset1_left_inv)

values "{x. cast_fset1 {|A, B|} x}"

So I try to define a code lemma for both arguments. And as result only i ⇒ i ⇒ bool mode is supported:

inductive cast_fset2 :: "val1 fset ⇒ val2 fset ⇒ bool" where
  "cast_fset2 {||} {||}"
| "cast_val x y ⟹ cast_fset2 xs ys ⟹
   cast_fset2 (finsert x xs) (finsert y ys)"

lemma cast_fset2_code [code_pred_intro]:
  "fimage cast_val_fun xs = ys ⟹ cast_fset2 xs ys"
  "fimage cast_val_fun_inv ys = xs ⟹ cast_fset2 xs ys"
  apply (auto)
  apply (induct xs arbitrary: ys)
  apply (simp add: cast_fset2.intros(1))
  apply (metis (full_types) cast_fset2.intros(2) cast_val.intros(1) cast_val.intros(2) cast_val_fun.simps(1) cast_val_fun.simps(2) fimage_finsert val1.exhaust)
  apply (induct ys arbitrary: xs)
  apply (simp add: cast_fset2.intros(1))
  by (smt cast_fset2.intros(2) cast_val.intros(1) cast_val.intros(2) cast_val_fun_inv.elims cast_val_fun_inv.simps(1) fimage_finsert)

lemma cast_fset2_code_inv:
  "cast_fset2 xs ys ⟹ fimage cast_val_fun xs = ys"
  "cast_fset2 xs ys ⟹ fimage cast_val_fun_inv ys = xs"
  apply (induct rule: cast_fset2.induct)
  apply simp
  apply simp
  using cast_val.simps cast_val_fun.simps(1) apply auto[1]
  using cast_val.simps by auto

code_pred [show_modes] cast_fset2
  by (simp add: cast_fset2_code_inv(1))

I'm trying to use [code] annotation instead of [code_pred_intro]:

inductive cast_fset3 :: "val1 fset ⇒ val2 fset ⇒ bool" where
  "cast_fset3 {||} {||}"
| "cast_val x y ⟹ cast_fset3 xs ys ⟹
   cast_fset3 (finsert x xs) (finsert y ys)"

lemma cast_fset3_left:
  "fimage cast_val_fun xs = ys ⟹ cast_fset3 xs ys"
  apply (induct xs arbitrary: ys)
  apply (simp add: cast_fset3.intros(1))
  by (metis (full_types) cast_fset3.intros(2) cast_val.intros(1) cast_val.intros(2) cast_val_fun.simps(1) cast_val_fun.simps(2) fimage_finsert val1.exhaust)

lemma cast_fset3_left_inv:
  "cast_fset3 xs ys ⟹
   fimage cast_val_fun xs = ys"
  apply (induct rule: cast_fset3.induct)
  apply simp
  using cast_val.simps by auto

lemma cast_fset3_left_code [code]:
  "fimage cast_val_fun xs = ys ⟷
   cast_fset3 xs ys"
  using cast_fset3_left cast_fset3_left_inv by blast

But I get the following warning and the lemma is ignored at all:

Partially applied constant "FSetIndTest.cast_val_fun" on left hand side of equation, in theorem:
cast_val_fun |`| ?xs = ?ys ≡ cast_fset3 ?xs ?ys

Is it possible to use different code lemmas for different modes (i ⇒ o ⇒ bool, o ⇒ i ⇒ bool) of an inductive predicate? How to fix last lemma? Why I get this warning?

Florian Haftmann Florian Haftmann · Accepted Answer · 2018-10-21T15:41:06

Code generation for an inductive predicate always operates on the same set of introduction rules; however you are always free to introduce a copy of an existing inductive predicate and equip that with a different set of introduction rules.

The attribute [code] is just for equations, not for introduction rules.

How to use different code lemmas for different modes of inductive predicate?

1 Answers