# IRC log for #isabelle, 2016-05-21

All times shown according to UTC.

Time Nick Message
00:57 fracting joined #isabelle
03:03 fracting joined #isabelle
03:05 fracting joined #isabelle
04:02 fracting joined #isabelle
04:39 fracting joined #isabelle
04:41 fracting joined #isabelle
05:10 fracting joined #isabelle
05:12 fracting joined #isabelle
05:15 fracting joined #isabelle
09:23 fracting joined #isabelle
12:05 JCaesar Hm, say, I'd have a function uncurry, canonically defined. I'd like to make a split rule for it, e.g. P (uncurry f a) = (∀x y. a = (x, y) → P (f x y))
12:05 JCaesar I can prove that split rule, but I can't apply it, so I guess it's in the wrong format…
12:05 JCaesar how would I have to do it?
12:42 fracting joined #isabelle
13:23 ThreeOfEight JCaesar: no idea what you mean
13:23 ThreeOfEight http://downthetypehole.de/paste/9jyViKPZ
13:23 ThreeOfEight this works fine.
13:37 JCaesar ThreeOfEight: Maybe I didn't understand split rules, then…
13:37 JCaesar "y = uncurry (op +) x ==> False"
13:37 JCaesar Doesn't split for me…
13:40 JCaesar It does split if I unfold uncurry_def and use prod.splits, so… I don't get it.
14:00 ThreeOfEight JCaesar: for that you need a split_asm rule
14:00 ThreeOfEight prod.splits consists of two rules, prod.split and prod.split_asm
14:01 JCaesar Uh, so the format of the right side of the split rule is important…
14:02 ThreeOfEight lemma uncurry_split_asm: "P (uncurry f a) ⟷ ¬(∃x y. a = (x, y) ∧ ¬P (f x y))" by (auto simp: uncurry_def split: prod.splits)
14:02 ThreeOfEight does the trick
14:05 ThreeOfEight JCaesar: I don't really know where the splitter is documented
14:05 ThreeOfEight (if anywhere)
14:06 ThreeOfEight But the Isar reference manual mentions that there is split_tac and split_asm_tac
14:06 ThreeOfEight and the splitter decides which of them to use by analysing the split rule
14:08 ThreeOfEight looks like everything of the Form "_ = ¬ _" is an assumption split rule and everything else is a normal split rule
14:08 ThreeOfEight don't ask me why; may just be a convention
14:09 ThreeOfEight apart from that, there seems to be no restriction on the rhs of a split rule
14:14 JCaesar A little strange, I'll remember it.
15:22 ThreeOfEight I've not written a split rule in my entire life
19:29 fracting joined #isabelle
19:32 fracting joined #isabelle
20:30 ammbauer joined #isabelle
21:26 fracting joined #isabelle