*To*: Tambet <qtvali at gmail.com>*Subject*: Re: [isabelle] Questions about Isabelle*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Mon, 19 Jul 2010 17:33:29 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <AANLkTil5bK5t6Dd2Pd0ySPNTGM_cqL8ykpazodV6ooeA@mail.gmail.com>*References*: <AANLkTimT50DJGFi55a18dkuTTRPt7sGCPopRX9TEFH-0@mail.gmail.com> <AANLkTil5bK5t6Dd2Pd0ySPNTGM_cqL8ykpazodV6ooeA@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.24 (Macintosh/20100228)

If you do not need negative numbers, I suggest to use nat instead of int. Tobias Tambet schrieb: > Sorry for reposting, but I had a few errors (whole day played with Isabelle, > now a bit blurry). This is the same message with errors fixed (hope that > moderator catches the previous one). > > Hello! > > > I would like to ask a few questions about Isabelle, because in a day of > reading manuals and testing things, I have some questions needed to do > anything at all left unanswered. > > I did, in previous few days, study about Coq, but found out that Isabelle > language use is much more intuitive to me and it has some tools built-in, > which Coq lacks. > > > However, now I have a number of problems: > > - Loading built-in libraries is extremely slow. Is there any kind of > caching, compilation or preloading technique to make it faster? > - Built-in heuristics tool does not solve things and I think that this is > related to some bias in my understanding of semantics, because things are > really trivial. > - Search of patterns is extremely slow - is Isabelle meant only for > supercomputers and clusters? > > > Next thing that I quite much do not understand the Class semantics. I am > used to programming languages, mostly imperative, but with many plays with > others, but it's a first try I try to use prover. I am actually completely > lost with that. > > > I give concrete examples about what I want to do to get on track: > > I want to prove several things about Collatz sequences. For that, I tried > (taking fibonaccy series and primes theories as examples) to just formulate > a class, which contains all positive naturals. I did write fixes clause with > 'a => bool and definition that it's over zero. After that I tried to prove > with heuristics, that even integers of that class are bigger than one - this > failed. I tried to unfold the definition from class, but wasn't able to do > that. Now I think that maybe this class does not provide me that check at > all? It's basically copy of similar class from primes with definitions for > naturals removed as I thought that maybe it does not have enough rules for > naturals. > > > Also, as I'm not even conscious about what exactly to ask, is this possible > to just give me random important hints about good strategies and common > biases related to proving similar things: > > > I would like to define the following properties to numbers: > > Collatz itself, is this OK: > > fun > collatzNext :: "int \<Rightarrow> int" > where > "collatzNext n = > (if (n \<in> even) then (n div (2::int)) else > (if (n \<in> odd) then ((3::int) * n) + (1::int) else > 1))" > > I am somewhat worried about this last else clause - it should not be "1", > but undefined. Such output is not possible as I'm considering only the > typical version of Collatz with naturals. I would like to do in one step: > create class that collatz(i) or smth. is positive natural so that I could > use it in definitions (instead of writing everywhere the clause >0) and > prove that thus, it's output is also positive natural (I imagine that this > proof will be automatically asked from me when defining such function?) I > wasn't able to prove this trivial thing - actually I wasn't able to even > prove that things belonging to my class of positive naturals are always > bigger than zero. Thus, maybe the class was totally wrong? I haven't done > classes with Haskell, I am only tried Haskell for a few days as my > girlfriend learns it (sometimes) and I do not want to take the fun away by > knowing better. Anyway, I am now stuck with Isabelle classes - or do I need > a class at all? > > Second, I would like to define such things: > "follows a b" for a comes after b in series. > "nextto a b" for b is right after a. > I would better like to use something like a \<before> b and a \<rightbefore> > b. > > I would like to have everything after a available as sequence for this class > of rules: > head (collatzSequence a) \<in> even. > first (collatzSequence a) \<in> even. - how to argument about concrete > position, for example that third element is first even element and thus, > second element is last odd element in this series? > > > I would also like to (check and) prove the following lemmas: > > > I am playing with Coq and Isabelle now :) Formalizing the following: > > fun p(a) = if (p(a) % 2 = 0) then (p(a div 2)) else (a). > The greatest divisor of a, which is power of two = p(a). > > I want to show that the number of multiplication-addition series always > equals p(a+1) and gives odd result for odd, even result for even and follows > the formula (((3/2)**(p(a+1)))*a+1)-1. > This should be trivial by binary analysis - how to use that and mix with > other parts? > > I want to show that because of this even-odd differentiation, 3n+1 series is > never called more than twice in a row. This follows from upper. > > I want to show that for any even number, all following even numbers will > have p(n) >= a(n) and that when looked from the position of n/2, that will > come back to even if n/2 it started with was odd and vice versa, because > div2 can't possibly change oddity of any upper level. > > Thus, starting from even it leads to odd (next number) and starting from odd > it leads to even (smaller number). Modulus is built in such way that p(n) > for each even number is p(n)+1 related to it's division by two and this p(n) > is how many times it will be divided by two, thus p(n) for any following > even is big enough to lead to smaller number (n/2+1 for next one, as numbers > grow, also this p(n) grows and thus, even leads to following(n)<=n+1). > > I want, thus, to show that the sequence always eventually leads to smaller > number than it started from or 1. > > Which classes and other stuff I should use for all that? > > Tambet > > > > Brute-force (python) check for those lemmas follows: > > # -*- coding: utf-8 -*- > > def iterCollatz(number, included=False): > if number == 0: > return > if included: > yield number > while number != 4: > while number % 2 == 0: > number /= 2 > yield number > number *= 3 > number += 1 > if number != 4: > yield number > else: > return > > def pow(number, p): > # For integers > if p == 0: > return 1 > r = 1 > for a in range(0,p): > r *= number > return r > > def maxp2(number): > # Count the zeros at end of number > a = number > p = 0 > while a % 2 == 0 and a > 1: > a /= 2 > p += 1 > return p > > def nextp2(number): > b = 1 > while b < number: > b *= 2 > return b > > def simulate(number): > times = maxp2(number+1) > result = pow(3, times) * (number + 1) / pow(2, times) - 1 > # print "Guess: " + str(result) > for b in iterCollatz(number): > if b == result: > # print "Guess correct" > return > print "Guess wrong" > > def pattern(start, length, highlight=-1): > s = "" > for a in range(start, start+length): > if a < 0: > n = "-" > elif maxp2(a) == 0: > n = "o" > elif maxp2(a) > 9: > n = "+" > else: > n = "%1d" % maxp2(a) > if a == highlight: > n = "*%s" % n > elif highlight != -1: > n = " %s" % n > s += n > return s > > def patternDiff(start, start2, length, highlight=-1): > s = "" > for a in range(0, length): > d = maxp2(a+start) - maxp2(a+start2) > if a+start < 0 or a+start2 < 0: > n = "-" > if d == 0: > n = "o" > if d == -1: > n = "A" > if d == -2: > n = "B" > if d == -3: > n = "C" > elif d < 0: > n = "!" > elif d > 9: > n = "+" > else: > n = "%1d" % (maxp2(a+start) - maxp2(a+start2)) > if a+start == highlight: > n = "*%s" % n > elif highlight != -1: > n = " %s" % n > s += n > return s > > def patternShiftSeq(start, length, count): > print "Init: %8d %s" % (start, pattern(start, length)) > for i in range(0, count): > print "Diff: %8d %s %d" % (start + length*i, patternDiff(start + > length*i, start, length), start) > print "Self: %8d %s" % (start + length*i, pattern(start + length*i, > length)) > > def patternMulSeq(number, length, count): > print "Init: %8d %s" % (number, pattern(number, length)) > for i in range(0, count): > print "Diff: %8d %s %d" % (number * pow(2, i), patternDiff(number * > pow(2, i), number, length), number) > print "Self: %8d %s" % (number * pow(2, i), pattern(number * pow(2, i), > length)) > > def patternMul3Seq(start, length, count, shift, difp=-1): > if shift % 2 == 0: > print "Error: there is no 3n for even value" > for i in range(1 + shift, count * length + shift, length): > print "Diff: %8d %s %d" % (((start + i)*3+1)/2, patternDiff(((start + > i)*3+1)/2, start + i, length), start + i) > print "Prev: %8d %s" % (start + i, pattern(start, length)) > if difp != -1: > print "Dif+: %8d %s %d" % (((start + i)*3+1)/2, patternDiff(((start + > i)*3+1)/2, start + difp, length), start + difp) > print "Pre+: %8d %s" % (start + difp, pattern(start + difp, length)) > print "Next: %8d %s" % (((start + i)*3+1)/2, pattern(((start + > i)*3+1)/2, length)) > > def collatzPattern(number): > for b in iterCollatz(number): > print "%4d %s" % (b, pattern(b-25, 25, b)) > > def Series(a): > s = "" > d = [] > while a != 1: > a = a + 1 > p = 0 > while a % 2 == 0: > #s += " " > d += [1] > a = a / 2 > p += 1 > s += str(p) > return s > > def Collatz1(a): > t = 0 > b = a / pow(2, maxp2(a)) > c = a / pow(2, maxp2(a)) > for a in iterCollatz(a): > if a % 2 == 1: > if t == 0: > c = a > if t > 1 and b % 2 == 0: > print "Error" > if t > 1 and c+1 < a == 0: > c = a > if t > 1 and b < a: > print "Error" > #print t, b > a > #print "%10d %30s" % (a, Series(a)), b > t = 0 > b = a > else: > t += 1 > > for a in range(1, 100000): > Collatz1(a)

**References**:**[isabelle] Questions about Isabelle***From:*Tambet

- Previous by Date: Re: [isabelle] Questions about Isabelle
- Next by Date: Re: [isabelle] Conflicting locales with a common signature
- Previous by Thread: Re: [isabelle] Questions about Isabelle
- Next by Thread: [isabelle] Questions about speed and CPU usage
- Cl-isabelle-users July 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list