Ограничить домен отношения в Изабель
У меня есть отношение, которое не является обоснованным, называем это r1. Он определяется (неявно) как функция:
r1: a' => a' => bool
Тем не менее, я отмечаю, что если я ограничу тип:
r2: b' => b' => bool
где b'определяется как тип a' с дополнительным ограничением, зависящим от r, это отношение на самом деле хорошо обосновано, и я могу использовать это хорошее свойство с теоремами стандартной библиотеки.
Мой пример
Чтобы быть более точным, я использую предикат finite_runs r s заявить это от государства s Я могу иметь только конечное число переходов (то есть отношений, которые начинаются в s заканчиваются). Конечно, если взять множество всех состояний, из того факта, finite_runs r s Я не могу вывести это для всех государств s' я имею finite_runs r s', Тем не менее, мне нужно это последнее свойство, чтобы утверждать, что отношение r обоснован во множестве всех государств.
Но потом я понимаю, что r действительно обоснованно, если я ограничу его набором состояний, которые связаны с s в каком-то количестве штатов. Это легко показать, потому что индуктивное определение finite_runs является
inductive finite_runs for r where
"(⋀ s'. r s s' ⟹ finite_runs r s') ⟹ finite_runs r s"
Итак, в некоторых доказательствах я хочу использовать информацию о том, что обоснованность r по набору {s'. r** s s'} дает мне. Тем не менее, нет никакой теории в обоснованности, которая могла бы мне помочь. Я хотел бы для этого случая, чтобы иметь возможность сказать, что тип b' выше тип a' с дополнительным ограничением, которое {s'. r** s s'} а затем создать теоремы в обоснованности для этого отношения.
Как я могу ограничить домен функции, как в случае выше?