Re: [isabelle] Simple problem with variable instantiation
Amine Chaieb wrote:
Moreover, it seems that you have to drop the quotes (") around the
variable name, i.e. ?c2.0="2" instead of "?c2.0"="2".
The variable must be exactly the same as it appears in the theorem, i.e.
?c2.0 and not
All these theorems can be proved automatically by eg. arith.
c fe wrote:
I stumbled upon a problem with Isabelle 2007 that didn't occur in
Isabelle 2003 (IIRC). I made a small (not very meaningful) example:
"c1 + (c2::nat) < a ==> c1 < a"
"a + (b::nat) < c ==> a < c"
"7 < (a::nat) ==> 5 < a"
(* Now use either  or  *)
 apply (rule_tac "c2.0"="2" in test)
 apply (rule_tac b=2 in test')
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and