*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Questions about Isabelle*From*: Tambet <qtvali at gmail.com>*Date*: Mon, 19 Jul 2010 06:03:32 +0300*In-reply-to*: <AANLkTimT50DJGFi55a18dkuTTRPt7sGCPopRX9TEFH-0@mail.gmail.com>*References*: <AANLkTimT50DJGFi55a18dkuTTRPt7sGCPopRX9TEFH-0@mail.gmail.com>

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)

**Follow-Ups**:**Re: [isabelle] Questions about Isabelle***From:*Lawrence Paulson

**Re: [isabelle] Questions about Isabelle***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Finding the instantiation of a variable
- Next by Date: Re: [isabelle] Conflicting locales with a common signature
- Previous by Thread: Re: [isabelle] Conflicting locales with a common signature
- Next by Thread: Re: [isabelle] Questions about Isabelle
- 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