Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Datatypes questions with use case

Email Gateway (Aug 18 2022 at 15:42):

From: Tambet <qtvali@gmail.com>
I am still stuck with datatypes.

I need a set function, which is able to do the following:

- Have topological connection between several things, showing that they
have equivalent behavior - for (in example here) projecting the natural
numbers sequence to itself (to show that some properties have some
irrelevance to how small or big the numbers are).

- Actually explain it, what I do - not just by defining two functions,
which are provably similar, but showing that if one exits, then another must
finish with a smaller number.

- Have the sequence, which allows to use >-kind operator to check if some
number follows another (the question is not about operator, but about having
the functionality - it currently tries to start with proving that the set is
monotone, but this is where this thing must lead and this has not been
proven yet, thus I can't start defining thing needed to prove that it is
from some fast-automatic-check checking if it is, but I need another way for
that).

Also, I would be happy for a few simple proofs about math, which do not use
assign-type syntax, but the kind of syntax described in short Isar manual -
I really like that syntax, because I can understand that and I think that I
might slowly learn to use that other, too (because it's clearly sometimes
convenient), but much more I would like to be able to read the proofs
afterwards. Thus, examples using that syntax would be very good thing to
have (with natural numbers and preferably some about binary numbers, too).

Below is mostly everything I need to show as starting point, also there is
Python file containing the configurable code, which generated that:

Legend:
pp1(n) = how many times the number minus 1 (n-1) divides by 2
pm3d2(n) = how many times (3n+1)/2 divides by 2
pm3(n) = how many times (3n+1) divides by 2.
subc(n)* = (n-1)/2; notice the sub-collatzes in regards to pp1(n).

• For subc, there are approximations, because the exact divisibility and
  rounding is actually synchronized to exact numbers and done in several
  steps,
  which take into consideration the divisibility of previous number. Anyway,
  this formula is useful in understanding the Collatz function. This is
  showable
  from fractal, that subc*0.75 actually rounds up (as all other calls also do,
  which
  is not visible from number circle ) - because number spiral
  is loosing some intermediate positions between numbers, which are divisable
  by bigger numbers.

Explanation:
pp1(n) = how many times to do n=n*1.5.
pm3(n) = how many times to do n/2 afterwards.
subc(n) = how many times the Collatz plays that it's Collatz with smaller
numbers, before zooming out to equivalent position.

Notice the fractal pattern [0102010301020104...] and it's variations!

Numbers make up a nice structure (only a
few members of Collatz series are here - those, which are
involved in pattern); only odd numbers are presented as Collatz
normalizes each number to odd as a first thing:

pp1(n+1)= 2 /\ n= 3 /\ pm3d2(n)= 0 /\ pm3(n)= 1 /\ Seq(n) = [3, 5, 8, 4,
2, 1]
[010*010301020104010201030102010501020103010201040102010301020106]
pp1(n+1)= 1 /\ n= 5 /\ pm3d2(n)= 3 /\ pm3(n)= 4 /\ Seq(n) = [5, 8, 4, 2,
1]
[01020*0301020104010201030102010501020103010201040102010301020106]
pp1(n+1)= 3 /\ n= 7 /\ pm3d2(n)= 0 /\ pm3(n)= 1 /\ Seq(n) = [7, 11, 17,
26, 13, 20, 10, 5, 8..]
[0102010*01020104010201030102010501020103010201040102010301020106]
pp1(n+1)= 1 /\ n= 9 /\ pm3d2(n)= 1 /\ pm3(n)= 2 /\ Seq(n) = [9, 14, 7,
11, 17, 26, 13, 20, 10..]
[010201030*020104010201030102010501020103010201040102010301020106]
pp1(n+1)= 2 /\ n= 11 /\ pm3d2(n)= 0 /\ pm3(n)= 1 /\ Seq(n) = [11, 17, 26,
13, 20, 10, 5, 8, 4..]
[01020103010*0104010201030102010501020103010201040102010301020106]
pp1(n+1)= 1 /\ n= 13 /\ pm3d2(n)= 2 /\ pm3(n)= 3 /\ Seq(n) = [13, 20, 10,
5, 8, 4, 2, 1]
[0102010301020*04010201030102010501020103010201040102010301020106]
pp1(n+1)= 4 /\ n= 15 /\ pm3d2(n)= 0 /\ pm3(n)= 1 /\ Seq(n) = [15, 23, 35,
53, 80, 40, 20, 10, 5..]
[010201030102010*010201030102010501020103010201040102010301020106]
pp1(n+1)= 1 /\ n= 17 /\ pm3d2(n)= 1 /\ pm3(n)= 2 /\ Seq(n) = [17, 26, 13,
20, 10, 5, 8, 4, 2..]
[01020103010201040*0201030102010501020103010201040102010301020106]
pp1(n+1)= 2 /\ n= 19 /\ pm3d2(n)= 0 /\ pm3(n)= 1 /\ Seq(n) = [19, 29, 44,
22, 11, 17, 26, 13, 20..]
[0102010301020104010*01030102010501020103010201040102010301020106]
pp1(n+1)= 1 /\ n= 21 /\ pm3d2(n)= 5 /\ pm3(n)= 6 /\ Seq(n) = [21, 32, 16,
8, 4, 2, 1]
[010201030102010401020*030102010501020103010201040102010301020106]
pp1(n+1)= 3 /\ n= 23 /\ pm3d2(n)= 0 /\ pm3(n)= 1 /\ Seq(n) = [23, 35, 53,
80, 40, 20, 10, 5, 8..]
[01020103010201040102010*0102010501020103010201040102010301020106]
pp1(n+1)= 1 /\ n= 25 /\ pm3d2(n)= 1 /\ pm3(n)= 2 /\ Seq(n) = [25, 38, 19,
29, 44, 22, 11, 17, 26..]
[0102010301020104010201030*02010501020103010201040102010301020106]
pp1(n+1)= 2 /\ n= 27 /\ pm3d2(n)= 0 /\ pm3(n)= 1 /\ Seq(n) = [27, 41, 62,
31, 47, 71, 107, 161, 242..]
[010201030102010401020103010*010501020103010201040102010301020106]
pp1(n+1)= 1 /\ n= 29 /\ pm3d2(n)= 2 /\ pm3(n)= 3 /\ Seq(n) = [29, 44, 22,
11, 17, 26, 13, 20, 10..]
[01020103010201040102010301020*0501020103010201040102010301020106]
pp1(n+1)= 5 /\ n= 31 /\ pm3d2(n)= 0 /\ pm3(n)= 1 /\ Seq(n) = [31, 47, 71,
107, 161, 242, 121, 182, 91..]
[0102010301020104010201030102010*01020103010201040102010301020106]
pp1(n+1)= 1 /\ n= 33 /\ pm3d2(n)= 1 /\ pm3(n)= 2 /\ Seq(n) = [33, 50, 25,
38, 19, 29, 44, 22, 11..]
[010201030102010401020103010201050*020103010201040102010301020106]
pp1(n+1)= 2 /\ n= 35 /\ pm3d2(n)= 0 /\ pm3(n)= 1 /\ Seq(n) = [35, 53, 80,
40, 20, 10, 5, 8, 4..]
[01020103010201040102010301020105010*0103010201040102010301020106]
pp1(n+1)= 1 /\ n= 37 /\ pm3d2(n)= 3 /\ pm3(n)= 4 /\ Seq(n) = [37, 56, 28,
14, 7, 11, 17, 26, 13..]
[0102010301020104010201030102010501020*03010201040102010301020106]
pp1(n+1)= 3 /\ n= 39 /\ pm3d2(n)= 0 /\ pm3(n)= 1 /\ Seq(n) = [39, 59, 89,
134, 67, 101, 152, 76, 38..]
[010201030102010401020103010201050102010*010201040102010301020106]
pp1(n+1)= 1 /\ n= 41 /\ pm3d2(n)= 1 /\ pm3(n)= 2 /\ Seq(n) = [41, 62, 31,
47, 71, 107, 161, 242, 121..]
[01020103010201040102010301020105010201030*0201040102010301020106]
pp1(n+1)= 2 /\ n= 43 /\ pm3d2(n)= 0 /\ pm3(n)= 1 /\ Seq(n) = [43, 65, 98,
49, 74, 37, 56, 28, 14..]
[0102010301020104010201030102010501020103010*01040102010301020106]
pp1(n+1)= 1 /\ n= 45 /\ pm3d2(n)= 2 /\ pm3(n)= 3 /\ Seq(n) = [45, 68, 34,
17, 26, 13, 20, 10, 5..]
[010201030102010401020103010201050102010301020*040102010301020106]
pp1(n+1)= 4 /\ n= 47 /\ pm3d2(n)= 0 /\ pm3(n)= 1 /\ Seq(n) = [47, 71,
107, 161, 242, 121, 182, 91, 137..]
[01020103010201040102010301020105010201030102010*0102010301020106]
pp1(n+1)= 1 /\ n= 49 /\ pm3d2(n)= 1 /\ pm3(n)= 2 /\ Seq(n) = [49, 74, 37,
56, 28, 14, 7, 11, 17..]
pp1(n+1)= 2 /\ n= 51 /\ pm3d2(n)= 0 /\ pm3(n)= 1 /\ Seq(n) = [51, 77,
116, 58, 29, 44, 22, 11, 17..]
pp1(n+1)= 1 /\ n= 53 /\ pm3d2(n)= 4 /\ pm3(n)= 5 /\ Seq(n) = [53, 80, 40,
20, 10, 5, 8, 4, 2..]
pp1(n+1)= 3 /\ n= 55 /\ pm3d2(n)= 0 /\ pm3(n)= 1 /\ Seq(n) = [55, 83,
125, 188, 94, 47, 71, 107, 161..]
pp1(n+1)= 1 /\ n= 57 /\ pm3d2(n)= 1 /\ pm3(n)= 2 /\ Seq(n) = [57, 86, 43,
65, 98, 49, 74, 37, 56..]
pp1(n+1)= 2 /\ n= 59 /\ pm3d2(n)= 0 /\ pm3(n)= 1 /\ Seq(n) = [59, 89,
134, 67, 101, 152, 76, 38, 19..]
pp1(n+1)= 1 /\ n= 61 /\ pm3d2(n)= 2 /\ pm3(n)= 3 /\ Seq(n) = [61, 92, 46,
23, 35, 53, 80, 40, 20..]
pp1(n+1)= 6 /\ n= 63 /\ pm3d2(n)= 0 /\ pm3(n)= 1 /\ Seq(n) = [63, 95,
143, 215, 323, 485, 728, 364, 182..]
pp1(n+1)= 1 /\ n= 65 /\ pm3d2(n)= 1 /\ pm3(n)= 2 /\ Seq(n) = [65, 98, 49,
74, 37, 56, 28, 14, 7..]
pp1(n+1)= 2 /\ n= 67 /\ pm3d2(n)= 0 /\ pm3(n)= 1 /\ Seq(n) = [67, 101,
152, 76, 38, 19, 29, 44, 22..]
pp1(n+1)= 1 /\ n= 69 /\ pm3d2(n)= 3 /\ pm3(n)= 4 /\ Seq(n) = [69, 104,
52, 26, 13, 20, 10, 5, 8..]
pp1(n+1)= 3 /\ n= 71 /\ pm3d2(n)= 0 /\ pm3(n)= 1 /\ Seq(n) = [71, 107,
161, 242, 121, 182, 91, 137, 206..]
pp1(n+1)= 1 /\ n= 73 /\ pm3d2(n)= 1 /\ pm3(n)= 2 /\ Seq(n) = [73, 110,
55, 83, 125, 188, 94, 47, 71..]
pp1(n+1)= 2 /\ n= 75 /\ pm3d2(n)= 0 /\ pm3(n)= 1 /\ Seq(n) = [75, 113,
170, 85, 128, 64, 32, 16, 8..]
pp1(n+1)= 1 /\ n= 77 /\ pm3d2(n)= 2 /\ pm3(n)= 3 /\ Seq(n) = [77, 116,
58, 29, 44, 22, 11, 17, 26..]
pp1(n+1)= 4 /\ n= 79 /\ pm3d2(n)= 0 /\ pm3(n)= 1 /\ Seq(n) = [79, 119,
179, 269, 404, 202, 101, 152, 76..]
pp1(n+1)= 1 /\ n= 81 /\ pm3d2(n)= 1 /\ pm3(n)= 2 /\ Seq(n) = [81, 122,
61, 92, 46, 23, 35, 53, 80..]

Here, the pattern of divisions (things between counting to 1 and after two
of them) need a little explanation.

Look at this sequence of divisibility:
[0102010301020104010201030102010501020103010201040102010301020106]

For understanding the sequence each time Collatz reaches a point,
imagine the point being adjusted so that if biggest number right
before the number is 4, then take the position from first 4 and
adjust it so that it's the same in regards to first 2:

Patterns for 5:
[0102*10301020104010201030102010501020103010201040102010301020106]
5 [0102*10301020104010201030102010501020103010201040102010301020106]
8* [0102010*01020104010201030102010501020103010201040102010301020106]
4 [010*010301020104010201030102010501020103010201040102010301020106]
2 [0*02010301020104010201030102010501020103010201040102010301020106]
1 [*102010301020104010201030102010501020103010201040102010301020106]

Here it's visible, how Collatz changes. It will actually
use a formula 'pow(3, times) * (number + 1) / pow(2, times) - 1' to decide,
how many times to do 3n+1. Times = maxp2(number+1), which is maximum power
of two, by which the number can be divided. We see that it's like reverse
operation to division by two. This means - it uses the next po
[message truncated]

Last updated: Nov 21 2024 at 12:39 UTC