Re: [isabelle] Simple problem with variable instantiation



Hi,

The variable must be exactly the same as it appears in the theorem, i.e.
 ?c2.0 and not
  c2.0
All these theorems can be proved automatically by eg. arith.

Best,
Amine.

c fe wrote:
Hallo,

I stumbled upon a problem with Isabelle 2007 that didn't occur in
Isabelle 2003 (IIRC). I made a small (not very meaningful) example:

lemma test:
"c1 + (c2::nat) < a ==> c1 < a"
apply simp
done

lemma test':
"a + (b::nat) < c ==> a < c"
apply simp
done

lemma test2:
"7 < (a::nat) ==> 5 < a"
(* Now use either [1] or [2] *)
[1] apply (rule_tac "c2.0"="2" in test)
[2] apply (rule_tac b=2 in test')
apply simp
done

If I want to use test to proof test2 I can't instantiate c2.
That isn't a big problem as I can just make lemmas like test' but if
there is a simple solution to this I'd be interested to hear about it.

Thanks,
Christoph Feller





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