Re: [isabelle] "Illegal schematic variable(s) in case" when using an exported induction rule

It's not a bug, in that sense. The theorem you're trying to use isn't the usual shape for an induction rule, and it's reporting that as best it can.

Exporting a theorem out of a context, in general, changes its shape, although typically not much. There's no guarantee that induction-shaped rules are exported to induction-shaped rules, etc. Since you've now left an anonymous context and there's no way to return, or get access to foo.induct by any other name, it might seem confusing that foo.induct is not an induction rule, but it's just a consequence of the steps that have been taken.

You've written a postscript in which you explain your reasoning for using a context, which looks like it boils down to saying that some other approach wasn't working. I suspect you should rewind and try other fixes to your original induction problem.

Good luck with it,

From: cl-isabelle-users-bounces at <cl-isabelle-users-bounces at> on behalf of Isaac at <Isaac at>
Sent: 11 October 2021 06:54
To: isabelle-users at <isabelle-users at>
Subject: [isabelle] "Illegal schematic variable(s) in case" when using an exported induction rule
I seem to have a fund a bug with induction, but I couldn't work out where I should report this;

Bassically, if I put a function inside a context like this:
    context fixes par :: bool begin
        function foo :: ‹bool ⇒ bool› where
            ‹foo True = (∀ j :: bool. par ∧ (par ⟶ foo False))› |
            ‹foo False = True›
            by(auto) termination by(relation ‹measure (λb . if b then 1 else 0)›, auto)
The generated "thm foo.induct" is as expected:
    ((⋀x. ?par ⟹ ?P False) ⟹ ?P True) ⟹ ?P False ⟹ ?P ?a0.0

However if I try and use it with the "induction" method, it breaks:
    lemma assumes ‹par› shows ‹foo par val› proof(induction val rule: foo.induct)

This suggests the proof text:
    case 1
    then show ?case sorry
    case 2
    then show ?case sorry

But that text reports an error on the first "case 1":
    proof (state)
    goal (2 subgoals):
    1. (⋀x. ?par ⟹ foo par False) ⟹ foo par True
    2. foo par False 
    Illegal schematic variable(s) in case "1"⌂

A simple workaround is to use "proof(induction val rule: foo.induct[of par])", and everything works as expected:
    proof (state)
    goal (2 subgoals):
    1. (⋀x. par ⟹ foo par False) ⟹ foo par True
    2. foo par False 

And the proof goes through (after replacing "sorry" with "by (auto)")

As an asside, the reason I have my function in a context to begin with is so that it dosen't put "⋀par" arround each case, which would break my proof, because each step dosn't hold for each "par", but rather the specific one i've assumed to be true!

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.