Inductive predicates for a fixed tuple parameter

Question

let's assume we have some predicate

definition someP :: "('a × 'a) ⇒ 'a ⇒ 'a ⇒ bool"

and an inductive over it

inductive my_inductive :: "('a × 'a) ⇒ 'a ⇒ bool"
 for "a_b" where
 basecase: "fst a_b = a ⟹ my_inductive a_b a" |
 stepcase: "someP a_b x y ⟹ my_inductive a_b x ⟹ my_inductive a_b y"

The inductive is fixed for the first parameter "a_b". "a_b" is a tuple which leads to somewhat ugly syntax. Unfortunately isabelle does not allow me writing something like for "(a,b)".

How can I create nicer introduction and induction rules for this inductive predicate?

corny corny · Accepted Answer · 2013-04-24T07:30:58

We can define a new set of introduction rules my_inductive_intros with a more beautiful basecase and the default stepcase

lemma my_inductive_intro_1: "my_inductive (a, b) a"
  by (simp add: my_inductive.basecase)
lemmas my_inductive_intros = my_inductive_intro_1 my_inductive.stepcase

We can write our own beautiful induction rule

lemma my_inductive_tuple_induct[consumes 1, case_names "basecase" "stepcase", induct pred: my_inductive]: 
 "my_inductive (a, b) x ⟹ 
 (P a) ⟹ (⋀x y. someP (a, b) x y ⟹ my_inductive (a, b) x ⟹ P x ⟹ P y) ⟹ P x"
 apply(rule my_inductive.induct[of "(a,b)"])
 apply(simp_all)
 done

consumes 1 tells isabelle to consume the first parameter. Let's illustrate this by an example:

lemma "my_inductive (a,b) c ⟹ P a b c"
  proof(induction rule: my_inductive_tuple_induct)

Without [consumes 1] this is the proof state:

my_inductive (?a, ?b) (my_inductive (a, b) c ⟶ P a b c)
?a
⋀x y. someP (?a, ?b) x y ⟹ my_inductive (?a, ?b) x ⟹ x ⟹ y

With [consumes 1], we get the desired proof state:

P a b a
⋀x y. someP (a, b) x y ⟹ my_inductive (a, b) x ⟹ P a b x ⟹ P a b y

case_names sets up the case names for an isar proof. The above proof can thus start with case basecase.

induct pred tells that we are declaring an induction rule. In certain cases, just writing proof(induction) might now be sufficient that isabelle figures out by itself to use our new fancy induction rule.

The following example demonstrates the setup

lemma
  assumes "my_inductive (a,b) c" shows "P a b c"
  using assms
proof (induction)
case basecase thus ?case using my_inductive_intros sorry
case (stepcase x y) thus ?case using my_inductive_intros sorry
qed

Inductive predicates for a fixed tuple parameter

1 Answers