# [isabelle] exception THM 0 raised (line 737 of "thm.ML")

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

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