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 
inte: 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 
inte 
pruvisto: thanks, that's actually what I ended up doing 
16:58 
inte 
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 
inte 
To be fair, I have no use case for it. And there's if_splits anyway. 
17:05 
inte 
oh, but for simplification that wouldn't work well anyway, because arguments of "if" would be duplicated. 
17:44 

hazyPurple joined #isabelle 