Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] structured induction proofs using customized i...

view this post on Zulip Email Gateway (Aug 18 2022 at 14:32):

From: Bianca Lutz <bianca.lutz@gmx.net>
Hello,
I have some problems concerning customized induction schemes in
conjunction with structured induction proofs using the induct method.

Consider the following two datatypes:
term = T1 term | T2 term | ...
var = string

a primrec function op :: [term, var] => term

and an inductively defined relation
R :: [term, term] => bool
where
R1: [[ ALL x. Q x --> R (op t1 x) (op t2 x) ]] ==> R (T1 t1) (T1 t2)
| R2: [[ ALL x. Q x --> R (op t1 x) (op t2 x) ]] ==> R (T2 t1) (T2 t2)
| ...

whereas Q is a rather long statement concerning elements of type var.

The induction scheme R.induct has the following shape:
[[ R t1 t2;
/\t1 t2. [[ALL x. Q x --> R (op t1 x) (op t2 x) & ?P (op t1 x) (op t2 x)]]
==> ?P (T1 t1) (T1 t2);
/\t1 t2. [[ALL x. Q x --> R (op t1 x) (op t2 x) & ?P (op t1 x) (op t2 x)]]
==> ?P (T2 t1) (T2 t2);
...
]] ==> ?P t1 t2

Usually there is some predicate P2 t1 t2 following from
ALL x. Q x --> R (op t1 x) (op t2 x) & P (op t1 x) (op t2 x)
that solves both R1 and R2.

Therefore, I proved the following customized induction scheme
lemma R_induct:
[[ R t1 t2;
/\t1 t2. [[?P2 t1 t2]] ==> ?P1 (T1 t1) (T1 t2);
/\t1 t2. [[?P2 t1 t2]] ==> ?P1 (T2 t1) (T2 t2);
/\t1 t2. [[ALL x. Q x --> R (op t1 x) (op t2 x) & ?P1 (op t1 x) (op t2 x)]]
==> ?P2 t1 t2;
...
]] ==> ?P1 t1 t2

Unfortunately, when I use this as shown below Isabelle fails at the last line:
*** Illegal schematic variable(s) in case "2"
*** at command "case"

although there is no schematic variable in case "2" (at least
according to Isabelle->Show me...->cases), since I instantiated ?P2
with some appropriate predicate beforehand ...

lemma
assumes "R t1 t2"
shows "P1 t1 t2"
proof (induct rule: R_induct[of t1 t2 P2 P1])
case 1 thus ?case by (simp add: assms) (* R t1 t2 *)
next
case 2

I have no idea how to avoid this. Any suggestions?

Thanks,
Bianca.

view this post on Zulip Email Gateway (Aug 18 2022 at 14:42):

From: Johannes Hölzl <hoelzl@in.tum.de>
Hi Bianca,

Am Dienstag, den 26.01.2010, 16:35 +0100 schrieb Bianca Lutz:
[..]

The induction scheme R.induct has the following shape:
[[ R t1 t2;
/\t1 t2. [[ALL x. Q x --> R (op t1 x) (op t2 x) & ?P (op t1 x) (op t2 x)]]
==> ?P (T1 t1) (T1 t2);
/\t1 t2. [[ALL x. Q x --> R (op t1 x) (op t2 x) & ?P (op t1 x) (op t2 x)]]
==> ?P (T2 t1) (T2 t2);
...
]] ==> ?P t1 t2

Here ?P is an quantified variable which can be arbitrary instantiated
when R.induct is used.

Usually there is some predicate P2 t1 t2 following from
ALL x. Q x --> R (op t1 x) (op t2 x) & P (op t1 x) (op t2 x)
that solves both R1 and R2.

Therefore, I proved the following customized induction scheme
lemma R_induct:
[[ R t1 t2;
/\t1 t2. [[?P2 t1 t2]] ==> ?P1 (T1 t1) (T1 t2);
/\t1 t2. [[?P2 t1 t2]] ==> ?P1 (T2 t1) (T2 t2);
/\t1 t2. [[ALL x. Q x --> R (op t1 x) (op t2 x) & ?P1 (op t1 x) (op t2 x)]]
==> ?P2 t1 t2;
...
]] ==> ?P1 t1 t2

When Isabelle reads variables with question marks in theorems they are
interpreted as existentially quantified variables. Just don't write them
with question marks, Isabelle interprets each identifier which is not
defined as constant as all quantified variable.

So write:

lemma R_induct:
"[[ R t1 t2;
/\t1 t2. [[P2 t1 t2]] ==> P1 (T1 t1) (T1 t2);
/\t1 t2. [[P2 t1 t2]] ==> P1 (T2 t1) (T2 t2);
/\t1 t2. [[ALL x. Q x --> R (op t1 x) (op t2 x) & ?P1 (op t1 x) (op t2 x)]]
==> P2 t1 t2;
...
]] ==> P1 t1 t2"

unfortunately when Isabelle writes theorems (like "thm R_induct") the
all quantified variables are shown with question marks.

By the way you can provide names to the cases with:

lemma R_induct[case_names Name1 Name2 Name3]:
....

Unfortunately, when I use this as shown below Isabelle fails at the last line:
*** Illegal schematic variable(s) in case "2"
*** at command "case"

I hope this solves your problem,

Johannes

view this post on Zulip Email Gateway (Aug 18 2022 at 14:48):

From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi Bianca,

unfortunately, I am not able to reproduce your error, but here are some
more hints on using the induct method:

  1. The generated induction rules for inductive predicates "consume" the
    premise for the inductive predicate. By passing this fact to the induct
    method, it normally selects the right induction rule automatically.
    Moreover, you do not have to show the inductive predicate goal any more.
    If you want the same effect for your custom induction rule, use the
    attribute "consumes n" where n is the number of facts to consume, usually 1.

In your example:
lemma R_induct[consumes 1]: ...

lemma R_lc:
fixes t1 t2
assumes "R t1 t2"
shows "lc t1 & lc t2"
using assms
proof (induct rule: R_induct)

If you combine this with the case_names attribute, use consumes first.
Consumed assumptions are not counted when providing names.

In your example:
lemma R_induct[consumes 1, case_names P1_T1 P1_T2 ...]

  1. Usually, you do not have to instantiate the parameters that appear in
    the conclusion. In particular, ?P1 in R_induct is automatically unified
    with "%t1 t2. lc t1 & lc t2" in your example. If induct has trouble to
    figure out the right instantiation, you can provide the arguments to P1
    explicitly:

...
using assms
proof (induct t1 t2 rule: R_induct)

  1. Your induction rule R_induct involves the free variable P2 that does
    not occur in the conclusion nor in the consumed facts. This is usually
    the cause for your error message "unbound schematic variable(s) in case 2".
    Rather than manually instantiating P2 in the induction rule, the induct
    method provides the "taking" specification:

...
using assms
proof (induct t1 t2
taking: "%t1 t2. (ALL x. Q x --> lc (op t1 x) & lc (op t2 x))"
rule: R_induct)

You can find more documentation on the induct method in the
Isabelle/Isar Reference Manual, Sec. 6.6.

I hope this helps.

Regards,
Andreas

Last updated: Nov 21 2024 at 12:39 UTC