[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.