src/HOL/ex/nbe.thy
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 19238 a2a4e6838bfc
child 19794 100ba10eee64
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
nipkow@19148
     1
(*  ID:         $Id$
nipkow@19148
     2
nipkow@19148
     3
Temporary test of nbe module.
nipkow@19148
     4
*)
nipkow@19148
     5
nipkow@19148
     6
theory nbe
nipkow@19148
     7
imports Main
nipkow@19148
     8
begin
haftmann@19202
     9
webertj@19237
    10
ML "reset quick_and_dirty"
nipkow@19148
    11
nipkow@19180
    12
declare disj_assoc[code]
nipkow@19180
    13
nipkow@19180
    14
norm_by_eval "(P | Q) | R"
nipkow@19180
    15
haftmann@19202
    16
(*lemma[code]: "(P \<longrightarrow> P) = True" by blast
nipkow@19180
    17
norm_by_eval "P \<longrightarrow> P"
haftmann@19202
    18
norm_by_eval "True \<longrightarrow> P"*)
nipkow@19180
    19
nipkow@19180
    20
nipkow@19180
    21
datatype n = Z | S n
nipkow@19180
    22
consts
nipkow@19180
    23
 add :: "n \<Rightarrow> n \<Rightarrow> n"
nipkow@19180
    24
 add2 :: "n \<Rightarrow> n \<Rightarrow> n"
nipkow@19180
    25
 mul :: "n \<Rightarrow> n \<Rightarrow> n"
nipkow@19180
    26
 mul2 :: "n \<Rightarrow> n \<Rightarrow> n"
nipkow@19180
    27
 exp :: "n \<Rightarrow> n \<Rightarrow> n"
nipkow@19180
    28
primrec
nipkow@19180
    29
"add Z = id"
nipkow@19180
    30
"add (S m) = S o add m"
nipkow@19180
    31
primrec
nipkow@19180
    32
"add2 Z n = n"
nipkow@19180
    33
"add2 (S m) n = S(add2 m n)"
nipkow@19180
    34
nipkow@19180
    35
lemma [code]: "add2 (add2 n m) k = add2 n (add2 m k)"
nipkow@19180
    36
by(induct n, auto)
nipkow@19180
    37
lemma [code]: "add2 n (S m) =  S(add2 n m)"
nipkow@19180
    38
by(induct n, auto)
nipkow@19180
    39
lemma [code]: "add2 n Z = n"
nipkow@19180
    40
by(induct n, auto)
nipkow@19180
    41
 
nipkow@19180
    42
norm_by_eval "add2 (add2 n m) k"
nipkow@19180
    43
norm_by_eval "add2 (add2 (S n) (S m)) (S k)"
nipkow@19180
    44
norm_by_eval "add2 (add2 (S n)(add2 (S m) Z)) (S k)"
nipkow@19180
    45
nipkow@19180
    46
primrec
nipkow@19180
    47
"mul Z = (%n. Z)"
nipkow@19180
    48
"mul (S m) = (%n. add (mul m n) n)"
nipkow@19180
    49
primrec
nipkow@19180
    50
"mul2 Z n = Z"
nipkow@19180
    51
"mul2 (S m) n = add2 n (mul2 m n)"
nipkow@19180
    52
primrec
nipkow@19180
    53
"exp m Z = S Z"
nipkow@19180
    54
"exp m (S n) = mul (exp m n) m"
nipkow@19180
    55
nipkow@19180
    56
norm_by_eval "mul2 (S(S(S(S(S(S(S Z))))))) (S(S(S(S(S Z)))))"
nipkow@19180
    57
norm_by_eval "mul (S(S(S(S(S(S(S Z))))))) (S(S(S(S(S Z)))))"
nipkow@19180
    58
norm_by_eval "exp (S(S(S(S(S(S(S Z))))))) (S(S(S(S(S Z)))))"
nipkow@19180
    59
nipkow@19180
    60
norm_by_eval "[] @ []"
nipkow@19180
    61
norm_by_eval "[] @ xs"
nipkow@19180
    62
norm_by_eval "[a,b,c] @ xs"
nipkow@19180
    63
norm_by_eval "[%a. a, %b. b, c] @ xs"
nipkow@19180
    64
norm_by_eval "[%a. a, %b. b, c] @ [u,v]"
nipkow@19180
    65
norm_by_eval "map f [x,y,z]"
nipkow@19180
    66
norm_by_eval "map (%f. f True) [id,g,Not]"
nipkow@19180
    67
norm_by_eval "map (%f. f True) ([id,g,Not] @ fs)"
nipkow@19180
    68
norm_by_eval "rev[a,b,c]"
nipkow@19180
    69
norm_by_eval "rev(a#b#cs)"
nipkow@19180
    70
norm_by_eval "map map [f,g,h]"
nipkow@19180
    71
norm_by_eval "map (%F. F [a,b,c]) (map map [f,g,h])"
nipkow@19180
    72
norm_by_eval "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))"
nipkow@19180
    73
norm_by_eval "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])"
nipkow@19180
    74
norm_by_eval "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()]"
nipkow@19180
    75
norm_by_eval "case xs of [] \<Rightarrow> True | x#xs \<Rightarrow> False"
nipkow@19180
    76
norm_by_eval "case Z of Z \<Rightarrow> True | S x \<Rightarrow> False"
nipkow@19180
    77
norm_by_eval "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) xs"
nipkow@19180
    78
norm_by_eval "let x = y in [x,x]"
nipkow@19180
    79
norm_by_eval "Let y (%x. [x,x])"
nipkow@19180
    80
norm_by_eval "case n of Z \<Rightarrow> True | S x \<Rightarrow> False"
nipkow@19180
    81
norm_by_eval "(%(x,y). add x y) (S z,S z)"
nipkow@19180
    82
norm_by_eval "filter (%x. x) ([True,False,x]@xs)"
nipkow@19180
    83
norm_by_eval "filter Not ([True,False,x]@xs)"
nipkow@19180
    84
haftmann@19167
    85
norm_by_eval "0 + (n::nat)"
haftmann@19167
    86
norm_by_eval "0 + Suc(n)"
haftmann@19167
    87
norm_by_eval "Suc(n) + Suc m"
haftmann@19167
    88
norm_by_eval "[] @ xs"
haftmann@19167
    89
norm_by_eval "(x#xs) @ ys"
haftmann@19167
    90
norm_by_eval "[x,y,z] @ [a,b,c]"
haftmann@19167
    91
norm_by_eval "%(xs, ys). xs @ ys"
haftmann@19167
    92
norm_by_eval "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f])"
haftmann@19167
    93
norm_by_eval "%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True"
haftmann@19167
    94
norm_by_eval "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()]"
haftmann@19177
    95
norm_by_eval "rev [a, b, c]"
nipkow@19148
    96
nipkow@19180
    97
norm_by_eval "case n of None \<Rightarrow> True | Some((x,y),(u,v)) \<Rightarrow> False"
nipkow@19180
    98
norm_by_eval "let ((x,y),(u,v)) = ((Z,Z),(Z,Z)) in add (add x y) (add u v)"
nipkow@19180
    99
norm_by_eval "(%((x,y),(u,v)). add (add x y) (add u v)) ((Z,Z),(Z,Z))"
nipkow@19180
   100
norm_by_eval "last[a,b,c]"
haftmann@19202
   101
webertj@19237
   102
(*
haftmann@19202
   103
  won't work since it relies on 
haftmann@19202
   104
  polymorphically used ad-hoc overloaded function:
haftmann@19202
   105
  norm_by_eval "max 0 (0::nat)"
haftmann@19235
   106
*)
nipkow@19180
   107
webertj@19238
   108
text {*
haftmann@19202
   109
  Numerals still take their time\<dots>
webertj@19238
   110
*}
haftmann@19202
   111
haftmann@19202
   112
end