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

Question

У меня есть тип данных и индуктивный предикат над ней (который на самом деле является малым шагом семантика некоторой переходной системы):

datatype dtype = E | A | B dtype 

inductive dsem :: "dtype ⇒ dtype ⇒ bool" where 
    "dsem A E" 
| "dsem (B E) E" 
| "dsem d d' ⟹ dsem (B d) (B d')" 

, а также функция, которая вычисляется путем случае различия:

fun f :: "dtype ⇒ nat" where 
    "f E = 0" 
| "f A = 1" 
| "f (B _) = 2" 

Я пытаюсь доказать некоторое свойство об индуктивном предикате, а предположения также включают вычисление значения f, которое не участвует в индукции.

lemma 
    assumes d: "dsem s s'" 
    and h: "h s v" 
    and v: "v = f s" 
    shows "P v" 
using d h 
proof (induct rule: dsem.induct) 

Для правила 3-семантикой Isabelle вычисляет подцель

⋀d d'. dsem d d' ⟹ (h d v ⟹ P v) ⟹ h (B d) v ⟹ P v 

где значение s теряется, так что невозможно вычислить значение v. я не могу ни включать в себя v в индукционных предположения, потому что тогда Изабель генерирует подцель

⋀d d'. dsem d d' ⟹ (h d v ⟹ v = f d ⟹ P v) ⟹ h (B d) v ⟹ v = f (B d) ⟹ P v 

, где по предположению индукции говорит v = f d что неверно, так как v = f (B d) в этом случае. Я также не могу поставить v в arbitrary: ..., потому что значение v должно быть исправлено на протяжении всего доказательства.

Было бы хорошо иметь явное привязку s = B d в сгенерированном подцеле; к сожалению, правило dsem.induct не предусматривает его.

Кто-нибудь знает обходное решение для вычисления значения v в этом случае?

Answer 1

Мне кажется странным, что v должен быть в то же время зафиксирован и рассчитан с s, и это то, что chris говорится в комментариях.

Если решение Brian дает в комментариях, что вы хотите, это может дублировать выражение f s, которое может быть большим (и использовать s несколько раз) и, возможно, точка предположения v = f s, чтобы избежать этого.

Первый обходной путь (это было возможно, что Brian неявно предлагается), чтобы сделать Isabelle сделать unfolding:

lemma 
    assumes d: "dsem s s'" 
    and h: "h s v" 
    and v: "v = big_f s s" 
    shows "P v" 
using d h 
unfolding v -- {* <<<< *} 
proof (induct rule: dsem.induct) 

Второй обходной путь может быть сокращайте big_f вместо big_f s s:

lemma 
    assumes d: "dsem s s'" 
    and h: "h s (f s)" 
    and v: "f = (λs. big_f s s)" -- {* <<<< *} 
    shows "P (f s)" 
using d h 
proof (induct rule: dsem.induct)