src/HOL/NumberTheory/Factorization.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 9944 2a705d1af4dc
child 11049 7eef34adb852
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9944
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     1
(*  Title:      HOL/ex/Factorization.thy
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     2
    ID:         $Id$
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     3
    Author:     Thomas Marthedal Rasmussen
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     4
    Copyright   2000  University of Cambridge
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     5
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     6
Fundamental Theorem of Arithmetic (unique factorization into primes)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     7
*)
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     8
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
     9
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    10
Factorization = Primes + Perm +
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    11
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    12
consts
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    13
  primel  :: nat list => bool 
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    14
  nondec  :: nat list => bool 
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    15
  prod    :: nat list => nat
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    16
  oinsert :: [nat, nat list] => nat list
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    17
  sort    :: nat list => nat list
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    18
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    19
defs
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    20
  primel_def "primel xs == set xs <= prime"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    21
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    22
primrec
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    23
  "nondec []     = True"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    24
  "nondec (x#xs) = (case xs of [] => True | y#ys => x<=y & nondec xs)"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    25
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    26
primrec
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    27
  "prod []     = 1"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    28
  "prod (x#xs) = x * prod xs"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    29
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    30
primrec
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    31
  "oinsert x []     = [x]"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    32
  "oinsert x (y#ys) = (if x<=y then x#y#ys else y#oinsert x ys)"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    33
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    34
primrec
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    35
  "sort []     = []"
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    36
  "sort (x#xs) = oinsert x (sort xs)"  
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    37
2a705d1af4dc moved Primes, Fib, Factorization from HOL/ex
paulson
parents:
diff changeset
    38
end