Camelia, the Perl 6 bug

IRC log for #isabelle, 2011-06-05

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | plain, newest first | summary

All times shown according to UTC.

Time S Nick Message
02:53 lispy joined #isabelle
09:34 stbuehler joined #isabelle
09:42 stbuehler hi! i have a small problem with isabelle; i think the lemma i want to use should match my assumptions + subgoal, but it somehow doesn't use it
09:45 stbuehler using this: "0 \<le> 2 * k \<and> 0 \<le> 2 * k + 3" goal (1 subgoal): 1. "fib (gcd (2 * k) (2 * k + 3)) = gcd (fib (2 * k)) (fib (2 * k + 3))"
09:45 stbuehler should match lemma fib_gcd_int: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow> fib (gcd (m::int) n) = gcd (fib m) (fib n)"
14:00 lispy stbuehler: hmm
14:00 lispy stbuehler: I'm not very good with Isabelle, but is it failing to match because the inequalities are turned around?
14:11 stbuehler i'm not sure what it actually was, but i got it working somehow
14:12 stbuehler adding [where ?m = ... and ?n = ... ] looked important
14:29 copumpkin joined #isabelle
14:29 copumpkin left #isabelle
14:29 copumpkin joined #isabelle
14:35 copumpkin left #isabelle
14:41 copumpkin joined #isabelle
14:46 copumpkin left #isabelle
14:47 stbuehler it would be really nice to see why it couldn't apply a rule -.-
15:39 lispy oh, yeah, naming them may help
16:45 copumpkin joined #isabelle
16:45 copumpkin left #isabelle
16:45 copumpkin joined #isabelle
16:47 pumpkin joined #isabelle
16:50 copumpkin left #isabelle
16:52 haifeng joined #isabelle
16:53 haifeng left #isabelle
16:59 stbuehler aargs
17:00 stbuehler i can proof 'have ?thesis', but i can't show it.. 'local statement will fail to refine any pending goal' -.-
17:01 stbuehler i guess it has something to do with me using "assume"...

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | plain, newest first | summary