IRC log for #isabelle, 2017-07-18

All times shown according to UTC.

Time Nick Message
02:07 mal``` joined #isabelle
02:28 dmiles joined #isabelle
08:27 larsrh pruvisto: does anybody actually require the Landau_Symbols session?
08:28 larsrh Why not rename Landau_Analysis to Landau_Symbols?
08:42 pruvisto larsrh: well, Landau symbols are pretty useful for real analysis, too
08:42 pruvisto and you can do quite a bit of that without HOL-Analysis
08:43 pruvisto e.g. the limit-proving stuff I'm currently working on doesn't need it at all
08:43 pruvisto but it does need Landau Symbols
08:43 pruvisto in fact, there's even been some talk about moving the Landau Symbols to the distribution entirely
10:02 larsrh I see.
10:02 larsrh anyway, I just strongly dislike duplicate sessions
10:02 larsrh You have 10 seconds to comply :p
12:46 chindy is there a separate definition of strict convexity ?
13:25 chindy pruvisto: shouldn't this be easily solvable? given that i assume that x is a solution: http://downthetypehole.de/paste/duiTudft
15:01 pruvisto ~chwell, it is
15:01 pruvisto chindy: well, it is
15:01 pruvisto using assms by (auto simp: arg_max_set_def is_arg_max_def)
15:02 chindy pruvisto: yea i realised that i probably have not understood locales quite yet, as this lemmas was quite easy to prove outside of a locale that I have but quite difficult inside... :/
16:14 isabelle-bot joined #isabelle
16:19 larsrh !value 3::nat
16:19 isabelle-bot larsrh: Suc (Suc (Suc 0))
16:20 larsrh now on a new server
17:17 ammbauer larsrh++
17:19 ammbauer !prove "even (x::nat) ==> x > 2 ==> ∃p q. prime p ∧ prime q ∧ p + q = x"
17:19 ammbauer and now we wait…
17:45 isabelle-bot joined #isabelle
18:46 silver joined #isabelle
19:10 deep-book-gk_ joined #isabelle
19:12 deep-book-gk_ left #isabelle
19:26 erisco joined #isabelle
19:26 erisco where can I find a syntax reference?
19:32 larsrh erisco: for logical operations or for Isar theory text?
19:32 larsrh former: https://isabelle.in.tum.de/dist/Isabelle2016-1/doc/main.pdf
19:33 erisco larsrh, thanks, for the Isar theory text
19:33 larsrh latter: https://isabelle.in.tum.de/dist/Isabelle2016-1/doc/isar-ref.pdf
19:34 erisco ah okay, it is just later in the document... I see
19:34 erisco is there no way to have an empty imports list?
19:34 larsrh no, that's impossible
19:35 larsrh you need to import at least Pure
19:35 larsrh theory imports form a DAG with only one start node (which is Pure)
19:41 erisco so I am reading "prog-prove" which has zero occurrences of the keyword "notepad", but this is the first keyword isar-ref mentions ... what is "notepad" ?
20:26 erisco I see this "by simp" occurring frequently... what if I want to refer to something specific? like what if I want to specifically say "by the reflexivity of equality" ?
20:33 pruvisto erisco: notepad is just for opening an empty proof state
20:33 pruvisto where you can play around with Isar proofs
20:34 pruvisto and goal manipulation (including solving goals) is done with tactics
20:34 pruvisto "simp" is one of them
20:34 int-e hmm, lemma "x = x" by (rule refl)
20:34 pruvisto there are others like "rule" (resolution with a single rule)
20:34 int-e so "rule" is another
20:34 pruvisto or "subst" (substitution with a single equation)
20:35 pruvisto I think prog-prove tries to teach people how to "get stuff done" fast
20:35 pruvisto you can do a lot of things initially just with "induction" and "auto"
20:36 erisco I want to work up from the nuts and bolts rather than down from the sophisticated tactics (or whatever you call them)
20:37 erisco where can I find a list or ideally document on these basics?
20:38 erisco like "rule", "refl", "subst", and so on?
20:39 int-e I guess section 9.4 of the isar reference manual is the place where this is documented, but it's a reference, not a tutorial.
20:41 int-e . o O ( funny, I do not recall ever seeing "slowsimp", "bestsimp" or "deepen" )
20:42 int-e and actually I'm wrong, section 9.4 is just the automatic stuff. Section 9.2 are the basic tactics.
20:42 aindilis joined #isabelle
20:45 erisco hm, yeah that is not enough description to tell me what they are
20:47 erisco I'll ignore the proof methods for now... so this is where I am at http://lpaste.net/357017
20:48 erisco now I need to justify that "add Z Z = Z" using the definition "add Z n = n"
20:48 pruvisto int-e: yeah nobody uses those
20:49 pruvisto erisco: you can do "simp only: …" or "subst"
20:50 erisco I know simp works, though subst doesn't seem to... "Failed to apply initial proof method"
20:50 erisco I understand that simp is a menagerie of stuff, so I am wondering what the exact thing I need is
20:52 int-e maybe the ~~/src/HOL/Isar_Examples/Basic_Logic.thy  theory is to your liking (the best way to get there, I think, is to open the Drinker.thy example in the documenation panel; then File -> Open will already be in the right directory.)
20:53 pruvisto erisco: if it's an assumption that you want to rewrite, you have to do "subst (asm)"
20:53 pruvisto anyway, I have to go to bed
20:53 erisco thanks for your help
20:54 pruvisto you're welcome
20:54 pruvisto I can offer more help tomorrow ^
20:54 pruvisto *^^
23:56 dave24 joined #isabelle