Isabelle : 유도 술어의 사용

Question

u에서 v까지의 단어 인 경우 word u w v이 보유하는 조건부 단어를 정의해야합니다.

는 좀 (고화질)

type_synonym ('q,'l) lts = "'q ⇒ 'l ⇒ 'q ⇒ bool" 

inductive word:: "('q,'l) lts ⇒ 'q ⇒ 'l list ⇒ 'q ⇒ bool" for δ where.... 

을 가지고 있고 나는 그것을 이해하지 않습니다.

왜 type_synomym을 사용합니까뿐 아니라

inductive word:: " 'q ⇒ 'l list ⇒ 'q ⇒ bool" for δ where.... 

내 두 번째 질문은 유도가 언급 될 수 무엇 δ가 약자 및 방법에 대한 것이다. 어쩌면 하나 이상의 예를 들어 귀납적이라고 설명하는 자습서가 있습니까?

Answer 1

lts은 레이블이있는 전이 시스템을 의미한다고 가정합니다. word 정의는 전환 시스템의 특정 선택에 달려 있습니다.

당신이 제안하는 단순화 된 형태의 서명이 충분하지 않은 다음 propositoin word u w v이가있는 단어 인 전환 시스템을 지정하지 않고 이해되지 않는다