Time 
Nick 
Message 
01:48 

ilbot3 joined #isabelle 
01:48 

Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html  Now with logging: http://irclog.perlgeek.de/isabelle/ 
09:02 

dave24 joined #isabelle 
09:35 
dave24 
must inductive definitions always have a return type of bool? 
09:35 
larsrh 
you can also have an "inductive set" (command inductive_set) which "returns" a set of things 
09:36 
larsrh 
instead of writing "Q ==> R x" you write "Q ==> x : R" 
09:37 
dave24 
ah I see, thanks 
09:54 

silver joined #isabelle 
11:32 
chindy 
is \exist x > 0 . P x the same as \exist x . x > 0 > P x ?= 
11:58 
pruvisto 
no 
11:59 
pruvisto 
its the same as \exist x . x > 0 & P x 
11:59 
pruvisto 
just ctrlclick it and it will take you to the definition 
12:00 

stoopkid joined #isabelle 
12:09 
chindy 
pruvisto: and \forall x > 0 . P x ? 
12:12 
pruvisto 
that is indeed \forall x . x > 0 > P x 
12:13 
pruvisto 
both correspond to the intuitive meaning of these quantifiers 
12:13 
chindy 
pruvisto: yea.... thats what i thought 
14:24 
dave24 
definition nbo_of_nat :: "nat => 8 word list" where "nbo_of_nat n = word_rsplit (of_nat n)" 
14:25 
dave24 
is this the correct way of getting big endian word list of a number? 
15:28 

stoopkid joined #isabelle 
16:35 
dave24 
what is the "itself" type constructor? 
17:04 
pruvisto 
dave24: that's essentially a way to convert an type parameter to an explicit value parameter 
17:05 
pruvisto 
e.g. if you want to know the cardinality of a type, you can use the CARD function which has type 'a itself => nat 
17:05 
pruvisto 
the "'a itself" is sort of a dummy parameter 
17:05 
pruvisto 
it only has one value 
17:05 
pruvisto 
but without it, there would be nothing to indicate /what/ type's cardinality you mean 
17:09 
dave24 
right, Thanks! 
17:16 
pruvisto 
these "'a itself" parameters sometimes get added to definitions automatically 
17:17 
pruvisto 
e.g. if you have a definition like "P = (ALL x. x > 0)" 
17:17 
pruvisto 
then P is clearly a Boolean, but the value of P depends on the type of the bound variable x in there 
17:17 
pruvisto 
Isabelle solves this problem by defining P with the type "'a itself => bool" 
17:25 
dave24 
yes, thats how I came across it, thanks! 
18:12 

ertesx joined #isabelle 
18:40 
JCaesar 
Say, can I get isabelle to insert things like <a name="blubbs_def" /> into the generated html documents? so I can link https://liftm.de/Magic.thy#blubbs_def, or so. 
18:57 
pruvisto 
JCaesar: well there is the @{url antiquutation 
18:57 
pruvisto 
no idea what that actually does 
18:58 
JCaesar 
to clarify: I don't want to link from my document, I want to link a specific line in my document with an anchor. 
18:59 
pruvisto 
no idea then 
18:59 
pruvisto 
sorry, I only halfread your message 
19:48 
JCaesar 
nvm. (I'm not very good at making my point…) 
19:52 
JCaesar 
I've got a question that's less technical… so i've got a function f k 0 = 2*k, f k (Suc n) = f (f k n) n. How would I go on about finding a closed form, or at least an upper bound for this function? How would I prove that in Isabelle? 
20:07 
larsrh 
JCaesar: could probably be hacked together with libisabelle 
20:26 
pruvisto 
JCaesar: you'd have to use "function" 
20:26 
pruvisto 
and you wouldn't be able to prove induction right away 
20:27 
pruvisto 
you'd first have to prove some properties with the pinduct rule (partial induction) 
20:27 
pruvisto 
and then prove full termination 
20:27 
pruvisto 
it'd be ugly; I've done it before 
20:27 
pruvisto 
as for closed form, I don't think there's a fixed "algorithm" for solving such things 
20:27 
JCaesar 
Me too… but I think I've misled you. The above definition is primitive recursive. 
20:28 
pruvisto 
you can try out some values and make an educated guess 
20:28 
JCaesar 
(unfortunately, I'm not educated for such guesses.) 
20:28 
pruvisto 
huh? 
20:28 
pruvisto 
there's a nested recursion in there 
20:28 
pruvisto 
doesn't look very primitive to me 
20:29 
JCaesar 
The second argument is strictly decreasing, one per call. 
20:29 
JCaesar 
I'm not sure if that's actually enough for primitive recursive, but it's enough for primrec… 
20:29 
pruvisto 
hm 
20:30 
pruvisto 
okay that may be true 
20:30 
pruvisto 
that does make things easier 
20:30 
pruvisto 
okay yes, termination at least is obvious here 
20:30 
pruvisto 
now that I look at it 
20:30 
pruvisto 
still don't know about closed form though 
20:31 
pruvisto 
I might look at it tomorrw 
20:32 
pruvisto 
anyway, I suggest using "fun" to define it 
20:32 
pruvisto 
then you can probably use the induction rule "fun" gives you to prove stuff about it 
20:34 
pruvisto 
that will probably be much more convenient than doing using nat.induct 
20:35 
JCaesar 
Shouldn't that just be the same as induction over nat? or do I actually get something different? 
20:35 
JCaesar 
oho! 
20:36 
pruvisto 
fun gives you an induct rule with one case per function equation 
20:36 
pruvisto 
and each case has one induction hypothesis for each recursive call in that equation 
20:36 
pruvisto 
that rule is often weaker than nat.induct, but that's good 
20:36 
pruvisto 
because it helps automation, and sometimes also you 
20:37 
pruvisto 
it's a more "focused" rule 
20:46 
pruvisto 
got it 
20:46 
pruvisto 
JCaesar: do you want to hear the solution or just some hints? 
20:46 
JCaesar 
wow. 
20:47 
JCaesar 
I mean, I want the solution, but it sounds like a bit of fun to find it, if I can. So… some hints. 
20:47 
pruvisto 
Okay, try evaluating the function for a fixed k while varying the n 
20:47 
pruvisto 
and the other way round 
20:47 
pruvisto 
and see if you can find a simple law w.r.t. how it changes when you do that 
20:48 
pruvisto 
that helps a lot 
20:48 
pruvisto 
(it's also important to note that the "k" doesn't influence the "structure" of the recursion at all) 
20:49 
pruvisto 
(so it's a very "simple" parameter, so one could reasonably expect there to be some simple law about what happens when you vary the k) 
20:50 
JCaesar 
O_O. 
20:50 
JCaesar 
I didn't expect k to have so little influence… 
20:52 
pruvisto 
once I understood the structure of your recursion, I thought it probably wouldn't change very much 
20:52 
pruvisto 
but it was actually easier than I expected 
20:53 
pruvisto 
these recursions can get pretty funky 
20:53 
pruvisto 
anyway, I'm going to bed now 
20:53 
JCaesar 
Good night, and thank you. 
20:53 
pruvisto 
you'll probably figure it out by yourself now 
20:53 
pruvisto 
but this would be my general advice for such problems 
20:53 
pruvisto 
plug in some values and see if you can spot some interesting behaviour 
20:53 
pruvisto 
then make an educated guess and prove it 
20:59 
inte 
phew sledgehammer could do the induction step 
20:59 
inte 
proving obvious arithmetic identities is hard, sometimes. 
21:01 
JCaesar 
I'd need a pow function that isn't weird… ^^ isn't what I want, right? 
21:03 
inte 
Oh, I restricted k to nat in my proof. Not sure what the minimal structure for that argument is... a ring should suffice. 
21:04 
JCaesar 
nat does suffice for me… I'm counting depths of Sequent Calculus derivations… 
21:06 
inte 
well, ring_1, hmm 
21:07 
inte 
shouldn't there be a function "int => _ :: ring_1" 
21:12 
pruvisto 
it's called of_int 
21:12 
pruvisto 
monoid_mult should suffice 
21:13 
JCaesar 
apply(auto3 sleep: sheep(1)) 
21:13 
JCaesar 
:) 
21:14 
inte 
pruvisto: thanks. any idea why "find constants" with "int => _ :: ring_1"  "_ => _ => _" doesn't find of_int? 
21:15 
inte 
maybe lift_definition doesn't register it properly? hmm hmm. out of my comfort zone. 
21:17 
inte 
Ah, it does turn up concrete instances though, so I should have found it anyway. 