Time 
Nick 
Message 
01:16 

ertes joined #isabelle 
01:49 

ilbot3 joined #isabelle 
01:49 

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/ 
03:36 
chindy 
... turns out im a moron, what i wanted is the inverse implication A > B ⟹ P ∙ A > P ∙ B, which in fact is true 
17:17 
chindy 
The AFP submission says that there are not supposed to be usage of smt... hoever there are some theories containing smt solver 
17:17 
chindy 
also is there any more or less "standard" way to transform an smt proof to a proof not using an smt solver? 
17:30 
larsrh 
chindy: there's no strict enforcement of that rule in particular 
17:30 
larsrh 
it's more of a "avoid it if possible" 
17:30 
larsrh 
you can rewrite it by calling sledgehammer with the required facts and switch on Isar mode 
17:33 
chindy 
larsrh: but it does not find an isar proof all the time, is it supposed to ? 
17:43 
larsrh 
no, not all the time 
17:43 
larsrh 
in that case you'll have to do it yourself 
18:11 

ertes joined #isabelle 
18:34 
JCaesar 
Oh, and: SMT is quite smart. Good luck. 
20:04 
chindy 
i've noticed 
23:32 
pruvisto 
I think isar proofs are obly generated when ainglestep proof generation fails 
23:33 
pruvisto 
also, the individual steps in the generated isar proofs can still use smt, i think 
23:37 
chindy 
is there any meaningful difference between corollary/lemma/theorem/proposition 
23:57 
pruvisto 
No. 
23:57 
pruvisto 
None at all. 
23:58 
pruvisto 
the idea is that "lemma" is some auxiliary fact and "theorem" is some important fact (e.g. the main result you want to show) 
23:58 
pruvisto 
and "corollary" is something that follows immediately from some previous fact with little no no further effort 
23:58 
pruvisto 
not sure what "proposition" is 
23:58 
pruvisto 
but in practice, few people really make this distinction in Isabelle 
23:58 
pruvisto 
I sometimes call important stuff "theorem" when I remember to do it 
23:59 
pruvisto 
but that's about it 
23:59 
chindy 
I see :) 