Email Gateway (Aug 18 2022 at 11:42): Email Gateway (Aug 18 2022 at 11:42):From: c fe <zehfee@googlemail.com>
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
Email Gateway (Aug 18 2022 at 11:42):From: Amine Chaieb <chaieb@in.tum.de>
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:
Email Gateway (Aug 18 2022 at 11:42):From: Peter Lammich <peter.lammich@uni-muenster.de>
Amine Chaieb wrote:
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.Moreover, it seems that you have to drop the quotes (") around the
variable name, i.e. ?c2.0="2" instead of "?c2.0"="2".
Last updated: Nov 21 2024 at 12:39 UTC