# IRC log for #isabelle, 2017-04-26

All times shown according to UTC.

Time Nick Message
01:01 wagle joined #isabelle
01:48 ilbot3 joined #isabelle
01:48 Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html || Now with logging: http://irclog.perlgeek.de/isabelle/
04:53 fracting joined #isabelle
04:55 hazyPurple joined #isabelle
05:55 hazyPurple joined #isabelle
07:54 dave24 joined #isabelle
15:21 chindy is there som dest rule that lets me show > by showing neither = nor < ?
15:25 JCaesar "dest rule" "show"… are you sure you're not looking for an intro rule?
16:36 pruvisto int-e: you can also do "cong: if_cong"
16:49 chindy lemma "∀i ∈ S . (f i) ≥ (g i) ⟹ ∃i ∈ S . (f i) > (g i) ⟹ (∑i∈S . f i) >  (∑i∈S . g i)" quickcheck tellms me a counter example is when f and g are undefined given an input i, how can i rule out f and g being undefined for input i
16:50 pruvisto "undefined" just means "some arbitrary (but fixed) value"
16:50 pruvisto so you can't rule that out
16:51 pruvisto you should probably restrict "S" to be finite though
16:51 pruvisto otherwise, both sums are zero
16:51 pruvisto (by definition)
16:51 pruvisto and f and g must have a sensible type, e.g. _ => real
16:51 pruvisto so do make sure that's the case
16:52 pruvisto in fact, the lemma you're looking for is simply sum_strict_mono_ex1
16:54 int-e pruvisto: thanks, that's actually what I ended up doing
16:58 int-e hmm, there's no if_strong_cong though. (which I imagine could be  "(b ==> c ==> x = u) ==> (b ==> ~c ==> x = v) ==> (~b ==> c ==> y = u) ==> (~b ==> ~c ==> y = v) ==> (if b then x else y) = (if c then u else v)")
16:59 int-e To be fair, I have no use case for it. And there's if_splits anyway.
17:05 int-e oh, but for simplification that wouldn't work well anyway, because arguments of "if" would be duplicated.
17:44 hazyPurple joined #isabelle