Как исправить «Незаконная схематическая переменная (ы)» в индукции взаимного рекурсивного правила?

Question

В Изабель я пытаюсь сделать индукцию правила по взаимно рекурсивным индуктивным определениям. Вот самый простой пример, который я был в состоянии создать:

theory complex_exprs 
imports Main 
begin 

datatype A = NumA int 
      | AB B 
and B = NumB int 
     | BA A 

inductive eval_a :: "A ⇒ int ⇒ bool" and eval_b :: "B ⇒ int ⇒ bool" where 
eval_num_a: "eval_a (NumA i) i" | 
eval_a_b: "eval_b b i ⟹ eval_a (AB b) i" | 
eval_num_b: "eval_b (NumB i) i" | 
eval_b_a: "eval_a a i ⟹ eval_b (BA a) i" 

lemma foo: 
    assumes "eval_a a result" 
    shows "True" 
using assms 
proof (induction a) 
    case (NumA x) 
    show ?case by auto 
    case (AB x) 

На данный момент, Изабель останавливается с "Illegal схематическом переменной (ы) в случае, если„АБ“. Действительно, текущая цель ⋀x. ?P2.2 x ⟹ eval_a (AB x) result ⟹ True которая содержит предположение ?P2.2 x. Это «схематическая переменная», о которой говорит Изабель? Откуда он исходит, и как я могу избавиться от него?

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

proof (induction) 
    case (eval_num_a i) 
    show ?case by auto 
    case (eval_a_b b i) 

Опять же, цель ⋀b i. eval_b b i ⟹ ?P2.0 b i ⟹ True с неизвестным ?P2.0 b i, и я не могу продолжать.

Как связанный с этим вопрос: я пытался сделать индукцию с помощью

proof (induction rule: eval_a_eval_b.induct) 

но Изабель не принимает это, говоря: "Не удалось применить первоначальный метод доказательства.

Как я могу сделать эту индукцию? (В моем фактическом применении мне действительно нужна индукция, потому что цель сложнее, чем True.)

Answer 1

Доказательства взаимно-рекурсивных определений, будь то типы данных, функции или индуктивные предикаты, должны быть взаимно рекурсивные. Однако в вашей лемме вы указываете только индуктивное свойство для eval_a, но не для eval_b. В случае для AB вы, очевидно, хотите использовать гипотезу индукции для eval_b, но поскольку в лемме не указано индуктивное свойство для eval_b, Изабель не знает, что это такое. Таким образом, он оставляет его в виде условной переменной ?P2.0.

Таким образом, вы должны заявить две цели, скажем

lemma 
    shows "eval_a a result ==> True" 
    and "eval_b b result ==> True" 

Затем метод induction a b будет выяснить, что первое утверждение соответствует A, а второе B.

Правило индукции для индуктивных предикатов выходит из строя, потому что это правило исключает индуктивный предикат (индукция по типам данных только «исключает» информацию типа, но это не формула HOL) и не может найти предположение для второго индуктивного предиката ,

Дополнительные примеры индукции по взаимно рекурсивным объектам можно найти в src/HOL/Induct/Common_Patterns.thy.