# IRC log for #isabelle, 2017-03-25

All times shown according to UTC.

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 int-e 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 int-e (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 int-e chindy: in any case, rel = UNIV x (UNIV - {{}})  would be a counterexample.
09:36 int-e it's probably designed to work with both partial and strict partial orders, making them non-partial (hence, total)
09:39 int-e 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 int-e that's one way of fixing this
09:42 int-e 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 int-e 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 int-e said ... if you need to do simultaneous induction you can't really split that up
11:50 int-e 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 int-e: 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 int-e: 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 int-e chindy: no, "total" is an abbreviation meaning "total_on UNIV". the "fix" was adding a refl[_on] assumption
16:40 int-e (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 int-e:
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 int-e yes.
16:50 chindy thanks ;)
17:19 aneas joined #isabelle
18:11 ertesx joined #isabelle