Невозможно определить правило индукции для взаимно рекурсивных предикатов - PullRequest
Новая
       7

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

0 голосов
/ 25 декабря 2018

Можете ли вы предложить, как применить правило индукции к следующей лемме? 

datatype 'a expr =
  Literal "'a literal_expr"
| Var "string"
and 'a literal_expr =
  NullLiteral
| CollectionLiteral "'a collection_literal_part_expr list"
and 'a collection_literal_part_expr =
  CollectionItem "'a expr"

datatype 'a type = OclVoid | Set "'a type"

inductive typing and collection_parts_typing where
  "typing Γ (Literal NullLiteral) OclVoid"
| "collection_parts_typing Γ prts τ ⟹
   typing Γ (Literal (CollectionLiteral prts)) (Set τ)"
| "collection_parts_typing Γ [] OclVoid"
| "⟦typing Γ a τ; collection_parts_typing Γ xs σ⟧ ⟹
   collection_parts_typing Γ (CollectionItem a # xs) σ"

lemma
  "typing Γ1 expr τ1 ⟹ typing Γ1 expr σ1 ⟹ τ1 = σ1" and
  "collection_parts_typing Γ2 prts τ2 ⟹
   collection_parts_typing Γ2 prts σ2 ⟹ τ2 = σ2"
  apply (induct expr and prts)
  apply (induct rule: typing_collection_parts_typing.inducts)

Следующие вопросы содержат очень простые примеры:

Но мой примерсложнее.И я не могу понять, что не так с моими типами данных, предикатами или леммами.Эта точная теория может быть переформулирована без взаимной рекурсии.Но это всего лишь небольшой фрагмент моей настоящей теории.

1 Ответ

0 голосов
/ 25 декабря 2018

Существует правдоподобное решение, аналогичное предложенному в принятом ответе на ваш предыдущий вопрос .Обратите внимание, что я изменил некоторые из названий некоторых элементов в ваших определениях, и что я очень полагался на sledgehammer, чтобы привести доказательство к выводу. 

datatype 'a expr =
  Literal "'a literal_expr"
| Var "string"
and 'a literal_expr =
  NL
| CL "'a clpe list"
and 'a clpe = CI "'a expr"

datatype 'a type = OclVoid | Set "'a type"

inductive typing and cpt where
  "typing Γ (Literal NL) OclVoid"
| "cpt Γ prts τ ⟹ typing Γ (Literal (CL prts)) (Set τ)"
| "cpt Γ [] OclVoid"
| "⟦typing Γ a τ; cpt Γ xs σ⟧ ⟹ cpt Γ (CI a # xs) σ"

lemma
  fixes Γ1 Γ2 :: 'a
    and expr :: "'b expr"
    and prts :: "'b clpe list"
    and σ1 τ1 σ2 τ2 :: "'c type"
  shows 
    "typing Γ1 expr τ1 ⟹ typing Γ1 expr σ1 ⟹ τ1 = σ1" and
    "cpt Γ2 prts τ2 ⟹ cpt Γ2 prts σ2 ⟹ τ2 = σ2"
  apply(
      induction Γ1 expr τ1 and Γ2 prts τ2 
      arbitrary: σ1 and σ2 
      rule: typing_cpt.inducts
      )
  subgoal by (blast dest: typing.cases)
  subgoal 
    by (metis 
        expr.inject(1) 
        literal_expr.distinct(1) 
        literal_expr.inject 
        typing.cases)
  subgoal by (blast dest: cpt.cases)
  subgoal by (metis cpt.cases list.discI list.sel(3))
  done
...