Как определить полурешетку списков? - PullRequest
Новая
       9

Как определить полурешетку списков?

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

Я пытаюсь определить верхнюю полурешетку: 

A ≺ B
... ≺ C [B,B,B] ≺ C [B,B] ≺ C [B] ≺ B
C [A] ≺ C [B]
C [A,A] ≺ C [A,B] ≺ C [B,B]
C [A,A] ≺ C [B,A] ≺ C [B,B]
C [A,A,A] ≺ C [A,A,B] ≺ C [A,B,B] ≺ C [B,B,B]
C [A,A,A] ≺ C [A,B,A] ≺ C [A,B,B] ≺ C [B,B,B]
C [A,A,A] ≺ C [A,A,B] ≺ C [B,A,B] ≺ C [B,B,B]
C [A,A,A] ≺ C [B,A,A] ≺ C [B,A,B] ≺ C [B,B,B]
C [A,A,A] ≺ C [A,B,A] ≺ C [B,B,A] ≺ C [B,B,B]
C [A,A,A] ≺ C [B,A,A] ≺ C [B,B,A] ≺ C [B,B,B]
and so on...

Мне нужно запретить прямые отношения вида: 

C [A,A] ≺ C [B,B]
C [A,A,B] ≺ C [B,B,B]
and so on...

Только один элемент должен отличаться в предыдущих элементах,Я определю эти косвенные отношения как транзитивное замыкание.

Я попытался определить его следующим образом: 

datatype t = A | B | C "t list"

definition "only_one p xs ys ≡
  let xys = zip xs ys in
  length xs = length ys ∧
  list_all (λ(x, y). x = y ∨ p x y) xys ∧
  length xs =
    length (takeWhile (λ(x, y). x = y) xys) +
    length (takeWhile (λ(x, y). x = y) (rev xys)) + 1"

inductive prec_t ("_ ≺ _" [65, 65] 65) where
  "A ≺ B"
| "C [B] ≺ B"
| "C (xs@[B]) ≺ C xs"
| "only_one (λx y. x ≺ y) xs ys ⟹
   C xs ≺ C ys"

Но я получаю следующую ошибку: 

Proof failed.
 1. ⋀x y xa xb xs ys.
       x (?x47 x y xa xb xs ys) (?x48 x y xa xb xs ys) ⟶
       y (?x47 x y xa xb xs ys) (?x48 x y xa xb xs ys) ⟹
       only_one x xs ys ⟶ only_one y xs ys
The error(s) above occurred for the goal statement⌂:
mono
 (λp x1 x2.
     x1 = A ∧ x2 = B ∨
     x1 = C [B] ∧ x2 = B ∨
     (∃xs. x1 = C (xs @ [B]) ∧ x2 = C xs) ∨ (∃xs ys. x1 = C xs ∧ x2 = C ys ∧ only_one p xs ys))

Не могли бы вы предложить, как это исправить?

ОБНОВЛЕНИЕ

Я переопределил проверку состояния следующим образом.Но это не помогает. 

primrec only_one' :: "bool ⇒ ('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ 'a list ⇒ bool" where
  "only_one' found p xs [] = (case xs of [] ⇒ found | _ ⇒ False)"
| "only_one' found p xs (y # ys) = (case xs of [] ⇒ False | z # zs ⇒
    if z = y then only_one' found p zs ys else
    let found' = p z y in
    if found ∧ found' then False else only_one' found' p zs ys)"

abbreviation "only_one ≡ only_one' False"

ОБНОВЛЕНИЕ 2

Индуктивное определение тоже не помогает: 

inductive only_one :: "bool ⇒ ('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ 'a list ⇒ bool" where
  "only_one True p [] []"
| "x = y ⟹
   only_one found p xs ys ⟹
   only_one found p (x#xs) (y#ys)"
| "p x y ⟹
   found = False ⟹
   only_one True p xs ys ⟹
   only_one found p (x#xs) (y#ys)"

1 Ответ

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

Ваше индуктивное определение не принимается, поскольку Изабель не знает, что only_one является монотонным.

Следовательно, следующий код перед вашим индуктивным определением должен решить вашу проблему. 

lemma only_one_mono: "(⋀ x y. x ∈ set xs ⟹ y ∈ set ys ⟹ p x y ⟶ q x y) ⟹ 
  only_one p xs ys ⟶ only_one q xs ys" sorry

declare only_one_mono[mono]

Бест, Рене

...