Re: [isabelle] odd type error message
On Wednesday 25 April 2007 17:13, Jeremy Dawson wrote:
> Here I have a simple goal and tactic:
> > > Goal "j <= (i :: nat) --> k < j --> i - j + k < i"
> > by (induct_tac "i" 1);
> 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" ;
> > apply (induct_tac "i" 1) ;
> *** 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
In ML style, the following command says to perform induction on the variable
"i" in subgoal 1:
by (induct_tac "i" 1);
If you want to specify a subgoal number in Isar style, you need to use the
apply (induct_tac  "i")
You can also use e.g. [2-4] to specify a range of subgoals, or [!] to specify
all subgoals. The same syntax is used to specify subgoals with case_tac,
Usually you won't need to specify a number, and it will default to the first
apply (induct_tac "i")
When you apply (induct_tac "i" 1) in Isar, I'm not sure exactly how it gets
interpreted; my best guess is that it is parsed as an application of the term
"i" to the term "1", which doesn't type check because "i" is not a function.
This archive was generated by a fusion of
Pipermail (Mailman edition) and