IRC log for #isabelle, 2017-02-19

All times shown according to UTC.

Time Nick Message
05:40 IRCFrEAK joined #isabelle
05:40 IRCFrEAK left #isabelle
06:25 kini joined #isabelle
11:18 silver joined #isabelle
18:08 chindy IS there some function like zipwith in Isabelle?
18:09 chindy i could only find zip but that just transforms the inputs to a list of pairs
18:14 pruvisto chindy: Not in the distribution, but you can use this one from my private collection: http://downthetypehole.de/paste/XpoCWYFt
18:15 chindy if i am gonna use this in a thesis... how would one zite/reference this ?
18:18 pruvisto Don't bother; it's nothing.
18:18 pruvisto You can add a comment saying "Contributed by Manuel Eberl" or something
18:18 pruvisto I should move this to the distribution at some point anyway
18:19 pruvisto If you really think you need to do a proper citation, I guess "Manuel Eberl, personal communication" would do
18:32 chindy pruvisto: btw in the second to last lemma u add map_upt_Suc to simp, but its unknown.  And adding map_Suc_upt instead, which im not sure is the same does not finish the goals
18:48 pruvisto chindy: what Isabelle version are you on?
18:49 pruvisto ah never mind
18:49 pruvisto lemma map_upt_Suc: "map f [0 ..< Suc n] = f 0 # map (λ i. f (Suc i)) [0 ..< n]" by (induct n arbitrary: f, auto)
20:14 throwaway-irc joined #isabelle
20:20 throwaway-irc hey guys - I'm trying to prove a property for all natural numbers n, but I'd like to split it into the following cases: n=0, n=1, n=2, n>2. how can I do this, preferably in an isar-style environment?
20:28 JCaesar Hm, I think you only have annoying alternatives. Might be best to just do something like let ?x = yourgoalhere; have 0: "n = 0 ==> ?x" …; have 1: "n = 1 ==> ?x" …; have 2: "n = 2 ==> ?x" …; have 3: "3 <= n ==> ?x" …; from 0 1 2 3 have ?x …;
20:28 JCaesar And the last thing is probably by some automated tools…
20:34 JCaesar if the goals with the equalities are easy you could also do something like apply (cases "n ∈ {0,1,2}") and then use apply safe to split it into three subgoals.
20:34 JCaesar I don't know what you're aiming for. If you want to do it really properly, use 3 case distinctions.
20:36 chindy so this is not an equation, http://pastebin.com/hdMyTU8V, because of the \and s ... but how would i define something like thos over lists
20:37 JCaesar use parenthesis.
20:37 JCaesar = binds stronger than &
20:38 juls joined #isabelle
20:38 chindy ahh:P
20:39 JCaesar (there's also == which you can use to avoid parenthesis in definitions, but it doesn't work anywhere else, I think.)
20:48 throwaway-irc thanks JCaesar, your first suggestion looks just fine to me!
20:49 JCaesar (if it works… replace the other … with sorry and try the last step first.)
20:56 int-e joined #isabelle
20:56 pruvisto throwaway-irc: the canonical pattern is this: http://downthetypehole.de/paste/AWjyR5e6
20:57 throwaway-irc joined #isabelle
20:57 throwaway-irc (oops, exited by mistake - thanks pruvisto!)
21:07 JCaesar consider. the heck.
21:15 pruvisto JCaesar: was introduced about a year or two ago, I think
21:15 pruvisto in order to avoid "big bang integration" proofs
21:15 JCaesar I feel old. :(
21:15 pruvisto tell me about it
21:15 pruvisto My first contact with Isabelle was through Isabelle/TTY
21:15 JCaesar chuchuco1ny: Do we still have bitmagic proofs that would benefit from this?
21:15 int-e "consider" is great.
21:16 pruvisto And "'a set" was still a synonym for "'a ⇒ bool"
21:16 pruvisto But, seriously, Isabelle is older than me.
22:15 ammbauer joined #isabelle