[isabelle] odd type error message



Here I have a simple goal and tactic:

> > Goal   "j <= (i :: nat) --> k < j --> i - j + k < i"
# ;
### Obsolete goal command encountered
Level 0 (1 subgoal)
j <= i --> k < j --> i - j + k < i
 1. j <= i --> k < j --> i - j + k < i
val it = [] : Thm.thm list
> by (induct_tac "i" 1);
Level 1 (2 subgoals)
j <= i --> k < j --> i - j + k < i
 1. j <= 0 --> k < j --> 0 - j + k < 0
 2. !!n. j <= n --> k < j --> n - j + k < n
         ==> j <= Suc n --> k < j --> Suc n - j + k < Suc n
val it = () : unit

but trying to convert the same proof into Isar I get

lemma mpl_lem [rule_format] : "j <= (i :: nat) --> k < j --> i - j + k < i" ;
proof (prove): step 0

goal (1 subgoal):
 1. j <= i --> k < j --> i - j + k < i
variables:
  i, j, k :: nat
>   apply (induct_tac "i" 1) ;
proof (prove): step 0

goal (1 subgoal):
 1. j <= i --> k < j --> i - j + k < i
variables:
  i, j, k :: nat
*** Type unification failed: Clash of types "nat" and "fun"
***
*** Cannot meet type constraint:
***
*** Term:  (i::nat) :: nat
*** Type:  nat => bool
***
*** At command "apply" (line 428 of stdin).

Does anyone have any ideas about what might be happening here?

Thanks for any help

Jeremy





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