Как определить индуктивный предикат по fset? - PullRequest
Новая
       18

Как определить индуктивный предикат по fset?

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

Я определил 2 вида значений и функцию приведения: 

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"

Также я определил функцию приведения для списка значений: 

inductive cast_list :: "val1 list ⇒ val2 list ⇒ bool" where
  "cast_list [] []"
| "cast_val x y ⟹ cast_list xs ys ⟹ cast_list (x#xs) (y#ys)"

code_pred [show_modes] cast_list .

values "{x. cast_list [A, B] x}"
values "{x. cast_list x [C, D]}"

Мне нужно определить аналогичныйфункция для fset.

Вот 1-я попытка.Кажется, что сгенерированная реализация не заканчивается: 

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

code_pred [show_modes] cast_fset1 .

(*values "{x. cast_fset1 {|A, B|} x}"*)

Вот еще одна попытка.Он не позволяет вычислить второй аргумент с учетом 1-го аргумента: 

inductive cast_fset2 :: "val1 fset ⇒ val2 fset ⇒ bool" where
  "⋀x y. x |∈| xs ⟹ y |∈| ys ⟹ cast_val x y ⟹
   cast_fset2 xs ys"

code_pred [show_modes] cast_fset2 .

Следующая версия работает нормально, но она использует функционал cast_val_fun вместо индуктивного cast_val.И также это работает только в одном направлении: 

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

inductive cast_fset3 :: "val1 fset ⇒ val2 fset ⇒ bool" where
  "cast_fset3 x (fimage cast_val_fun x)"

code_pred [show_modes] cast_fset3 .

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

Вот еще одна не прекращающаяся реализация: 

inductive cast_fset4 :: "val1 fset ⇒ val2 fset ⇒ bool" where
  "cast_list xs ys ⟹
   cast_fset4 (fset_of_list xs) (fset_of_list ys)"

code_pred [show_modes] cast_fset4 .

(*values "{x. cast_fset4 {|A, B|} x}"*)

Не могли бы вы предложить, как определить индуктивную версию функции приведения дляfsets с завершающей реализацией?

ОБНОВЛЕНИЕ:

Следующий код генерируется для cast_fset1: 

  cast_fset1_o_o =
  sup (Predicate.bind (Predicate.single ()) (λx. case x of () ⇒ Predicate.single ({||}, {||})))
   (Predicate.bind (Predicate.single ())
     (λx. case x of
          () ⇒
            Predicate.bind cast_fset1_o_o
             (λx. case x of
                  (xs_, ys_) ⇒
                    Predicate.bind cast_val_o_o
                     (λxa. case xa of
                           (x_, y_) ⇒ Predicate.single (finsert x_ xs_, finsert y_ ys_)))))

  cast_fset1_i_o ?xa =
  sup (Predicate.bind (Predicate.single ?xa)
        (λx. if x = {||} then Predicate.single {||} else bot))
   (Predicate.bind (Predicate.single ?xa)
     (λx. Predicate.bind cast_fset1_o_o
           (λxa. case xa of
                 (xs_, ys_) ⇒
                   Predicate.bind cast_val_o_o
                    (λxb. case xb of
                          (xa_, y_) ⇒
                            if x = finsert xa_ xs_ then Predicate.single (finsert y_ ys_)
                            else bot))))

cast_fset1_i_o вызывает cast_fset1_o_o.Последний не прекращается.Я думаю, это потому что fset не имеет конструкторов.Но я не понимаю, как это исправить.Как создать код для типов данных без конструкторов?

ОБНОВЛЕНИЕ 2:

То же поведение для мультимножеств: 

code_pred [show_modes] rel_mset' .

values 2 "{x. (rel_mset' cast_val) {#A, B#} x}"

возвращает {mset [D, C], mset [C, D]} ∪ ...

mset [D, C] и mset [C, D] равны.Abs_fset {D, C} и Abs_fset {C, D}, возвращаемые следующим выражением, также равны: 

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

Как определить индуктивный предикат для fset, multiset, ... чтобы он вычислял множества с некоторым каноническимпредставление списка и не возвращает повторяющиеся значения?

...