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