Email Gateway (Aug 22 2022 at 12:54): Email Gateway (Aug 22 2022 at 12:54):From: Daniel Stüwe <stuewe@in.tum.de>
Hi all,
in my bachelor's thesis I was working with functions calling themselves
in a set comprehension.
But while using induction and Isar with the induction rules for these
functions I got an unexpected exception in the case of the induction
step. I guess some unnecessary fixed variables in the rule are causing
this.
I created a minimal example showing the exception at last:
theory Super
imports Main
begin
fun super where
"super 0 = {}" |
"super (Suc n) = { x | x . x ∈ super n}"
lemma "x ∈ super n ⟹ P x"
by (induction n rule: super.induct) auto
lemma "x ∈ super n ⟹ P x"
proof (induction n)
case 0
thus ?case by simp
next
case (Suc n)
thus ?case by auto
qed
thm super.induct nat.induct
(*
⟦?P 0; ⋀n. (⋀x xa. ?P n) ⟹ ?P (Suc n)⟧ ⟹ ?P ?a0.0
⟦?P 0; ⋀nat. ?P nat ⟹ ?P (Suc nat)⟧ ⟹ ?P ?nat
*)
lemma "x ∈ super n ⟹ P x"
proof (induction n rule: super.induct)
print_cases
case 1
thus ?case by simp
next
case 2
(* exception THM 0 raised (line 661 of "thm.ML") - Isabelle 2015 *)
(* exception THM 0 raised (line 737 of "thm.ML") - Isabelle 2016 *)
oops
end
Greetings,
Daniel
Email Gateway (Aug 22 2022 at 12:54):From: Thomas Sewell <thomas.sewell@nicta.com.au>
OK, here are some bits of information, none of which are a satisfactory
answer.
1) It's clear the problem comes from the extra meta-quantified "x" and
"xa" in super.induct.
2) You can use super.induct[simplified] as an induction rule. That gets
rid of the pointless quantification and essentially gives you
nat.induct. Then the cases can be proven.
3) If you turn ML's debugging trace on, you get this explanation:
Here's the full trace:
Exception trace - exception THM 0 raised (line 737 of "thm.ML"): assume:
variables
Assumption.assume_hyps(2)
Basics.fold_map(3)()
Assumption.add_assms(3)
Proof.gen_assume(8)(1)
Proof.gen_assume(8)
Proof.gen_case(5)
Library.oo(1)(1)(1)
Toplevel.gen_proofs'(2)(1)(1)(1)
exception THM 0 raised (line 737 of "thm.ML"): assume: variables
So, the problem is, the "case" mechanism is trying to depend on an
assumption involving more variables. I'm guessing those variables were
invented by the "fun" package to handle the two binders of "x" created
by the syntax "{x | x . x : super n}". I think the package is then
getting confused, because these variables don't actually get involved in
the induction principle.
I would suspect that for more involved recursive functions, the
variables involved will be connected to the induction principle for it
to be useful. But you might have to fiddle a bit to get that to be true.
Cheers,
Thomas.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Last updated: Nov 21 2024 at 12:39 UTC