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 HOLAnalysis 
08:43 
pruvisto 
e.g. the limitproving 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 

isabellebot joined #isabelle 
16:19 
larsrh 
!value 3::nat 
16:19 
isabellebot 
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 

isabellebot joined #isabelle 
18:46 

silver joined #isabelle 
19:10 

deepbookgk_ joined #isabelle 
19:12 

deepbookgk_ 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/Isabelle20161/doc/main.pdf 
19:33 
erisco 
larsrh, thanks, for the Isar theory text 
19:33 
larsrh 
latter: https://isabelle.in.tum.de/dist/Isabelle20161/doc/isarref.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 "progprove" which has zero occurrences of the keyword "notepad", but this is the first keyword isarref 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 
inte 
hmm, lemma "x = x" by (rule refl) 
20:34 
pruvisto 
there are others like "rule" (resolution with a single rule) 
20:34 
inte 
so "rule" is another 
20:34 
pruvisto 
or "subst" (substitution with a single equation) 
20:35 
pruvisto 
I think progprove 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 
inte 
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 
inte 
. o O ( funny, I do not recall ever seeing "slowsimp", "bestsimp" or "deepen" ) 
20:42 
inte 
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 
inte: 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 
inte 
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 