# IRC log for #isabelle, 2017-04-10

All times shown according to UTC.

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 ctrl-click 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
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 int-e phew sledgehammer could do the induction step
20:59 int-e 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 int-e 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 int-e well, ring_1, hmm
21:07 int-e 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 int-e pruvisto: thanks. any idea why "find constants" with "int => _ :: ring_1"  - "_ => _ => _"  doesn't find of_int?
21:15 int-e maybe lift_definition doesn't register it properly? hmm hmm. out of my comfort zone.
21:17 int-e Ah, it does turn up concrete instances though, so I should have found it anyway.