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
>
> Jeremy

Hi Jeremy,

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 
square-bracket syntax:
 apply (induct_tac [1] "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, 
rule_tac, etc.

Usually you won't need to specify a number, and it will default to the first 
subgoal:
 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.

- Brian





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