Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Inductive proof by joining rules into one mutu...

Email Gateway (Aug 23 2022 at 09:14):

From: Mark Wassell <mpwassell@gmail.com>
Hello

I am trying to prove that a mutually recursive predicate holds based on two
non-mutually recursive predicates using 'joined' induction on the two
non-mutual predicates. I get the message "Failed to join given rules into
one mutual rule".

What conditions have to hold for this to work? I can see the code for this
in Pure/Isar/rule_cases.ML but cannot interpret the code.

A small example is the following:

inductive rel1 :: "nat => bool" where
"rel1 0"
| "rel1 n ⟹ rel1 (n+2)"

inductive rel2 :: "nat ⇒ bool" where
"rel2 1"
| "rel2 n ⟹ rel2 (n+2)"

inductive odd :: "nat ⇒ bool" and
even :: "nat ⇒ bool" where

"odd 1"
| "even n ⟹ odd (n+1)"
| "even 0 "
| "odd n ⟹ even (n+1)"

lemma
"rel1 m ⟹ even m" and
"rel2 n ⟹ odd n"
proof(induct rule: rel1.inducts rel2.inducts)

Cheers

Mark

Last updated: Apr 19 2024 at 04:17 UTC