Time 
Nick 
Message 
02:39 
chindy 
am i just to stupid/tired to see an obvious counter example or why cant i show that the set is non empty http://downthetypehole.de/paste/AQOcbrUC? 
02:39 
chindy 
http://downthetypehole.de/paste/FWL3uRoK 
09:34 
inte 
total_on probably doesn't mean what you want: it asserts that if x ~= y then x R y or y R x. 
09:35 
inte 
(with x and y restricted to the specified set) 
09:35 
ammbauer 
why is the isabelle definition different from the wikipedia definition https://en.wikipedia.org/wiki/Total_relation 
09:36 
inte 
chindy: in any case, rel = UNIV x (UNIV  {{}}) would be a counterexample. 
09:36 
inte 
it's probably designed to work with both partial and strict partial orders, making them nonpartial (hence, total) 
09:39 
inte 
lemma assumes "total r" "refl r" shows "∀x. ({y. (x, y) ∈ r} ≠ {})" using assms unfolding total_on_def refl_on_def by blast 
09:39 
inte 
that's one way of fixing this 
09:42 
inte 
ammbauer: And I don't know, there may even be textbooks doing it that way. 
10:01 
pruvisto 
yes, that's precisely the reason 
10:02 
pruvisto 
you may have something like "<" 
10:02 
pruvisto 
which is not reflexive, but still total in the Isabelle sense 
11:04 

aneas joined #isabelle 
11:11 
aneas 
i'm proving some properties A and B over a recursive datatype (think of a list, for example). the proof of A, however, requires B in its inductive case, and vice versa. i handle this by proving the lemma "constraints => A /\ B", which requires me to do both proofs in one go. this is ok for 2 properties A and B, but in one case i have 8 of those, and the current proof is 280 lines long... is there a way to prove seperate lemmas "cons 
11:11 
aneas 
traints /\ B ==> A" and "constraints /\ A ==> B" and combining those to "constraints ==> A /\ B"? 
11:13 
aneas 
btw, you guys have been a huge help for me, thanks everyone! 
11:48 
inte 
aneas: I'm not sure there's much you can do about the length of the proof, but there's an obscure way of proving several goals by induction using subcases: http://downthetypehole.de/paste/v0IZLRBc ... so this may help you make the proof more structured. 
11:50 
larsrh 
aneas: what inte said ... if you need to do simultaneous induction you can't really split that up 
11:50 
inte 
By "obscure" I mean I'm not sure where this is documented at all... there's an example in HOL/Induct/Common_Patterns.thy 
11:51 
larsrh 
one thing that I found helps a lot is to try to rephrase your properties in a nested instead of mutual fashion 
11:52 
larsrh 
e.g. if you need to state something over two lists instead of doing a manual recursion through both, just use list_all2 
11:59 
pruvisto 
In these cases, I often found out that I could actually pull out one of the properties into its own proof 
11:59 
pruvisto 
after I looked at it for a long time 
11:59 

silver joined #isabelle 
11:59 
pruvisto 
another thing you can do is wrap all of those n properties into an auxiliary definition or even a locale 
11:59 
pruvisto 
and perhaps prove some auxiliary lemmas about that 
11:59 
pruvisto 
conceptually, the induction proof will still be the same, but it might be more modular 
12:14 
aneas 
interesting. i thought there must be a clever induction rule to handle such cases. if there is no simple way to break of the proof into several ones, i guess i have to do some reading into how to keep such long proofs readable and maintainable. working on this proof has become very tedious because of the long runtime... 
12:15 
aneas 
inte: i'll try using subcases, thanks! 
12:28 
pruvisto 
I can't rule it out 
12:29 
pruvisto 
there might be a better way to do this 
15:44 
chindy 
inte: to be clear total_on works with strict partial orders while total only with partial orders? 
16:12 
chindy 
So that means that if i define a relation >= that is complete in the sense that \forall x y . x >= y \or y >= x (implying that both might be the case) then i need to use (total rel) \and (refl rel) because total is defined so that this would also work : \forall x y . x >= y XOR y >= x 
16:37 
inte 
chindy: no, "total" is an abbreviation meaning "total_on UNIV". the "fix" was adding a refl[_on] assumption 
16:40 
inte 
(noting that reflexivity of R is equivalent to x R y or y R x for x = y) 
16:43 
chindy 
yea but total_on and therefore total from Relations.thy specifically excludes x=y from the definition 
16:43 
chindy 
inte: 
16:44 
chindy 
so if i want to include it to my relation rel i need to specify total rel \and refl rel 
16:50 
inte 
yes. 
16:50 
chindy 
thanks ;) 
17:19 

aneas joined #isabelle 
18:11 

ertesx joined #isabelle 