Как использовать разные кодовые леммы для разных режимов индуктивного предиката? - PullRequest
Новая
       5

Как использовать разные кодовые леммы для разных режимов индуктивного предиката?

0 голосов
/ 23 сентября 2018

(Вопрос связан с Как определить индуктивный предикат для fset? , но более конкретно)

Вот простая теория с двумя типами значений и предикатом приведения:

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"

Я пытаюсь определить предикат приведения для fsets.Он отлично работает в режиме i ⇒ o ⇒ bool, но не поддерживает режим o ⇒ i ⇒ bool: 

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}"

Поэтому я пытаюсь определить лемму кода для обоих аргументов.И в результате поддерживается только режим i ⇒ i ⇒ bool: 

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))

Я пытаюсь использовать аннотацию [code] вместо [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

Но я получаю следующеепредупреждение и лемма вообще игнорируется: 

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

Можно ли использовать разные кодовые леммы для разных режимов (i ⇒ o ⇒ bool, o ⇒ i ⇒ bool) индуктивного предиката?Как исправить последнюю лемму?Почему я получаю это предупреждение?

1 Ответ

0 голосов
/ 21 октября 2018

Генерация кода для индуктивного предиката всегда работает по одному и тому же набору правил введения;однако вы всегда можете ввести копию существующего индуктивного предиката и снабдить его другим набором правил введения.

Атрибут [code] простодля уравнений, а не для правил введения.

...