src/HOL/ex/NormalForm.thy
 changeset 30946 585c3f2622ea parent 28952 15a4b2cf8c34 child 31062 878e00798148
equal inserted replaced
30945:0418e9bffbba 30946:585c3f2622ea
`     1 (*  Authors:    Klaus Aehlig, Tobias Nipkow`
`     1 (*  Authors:  Klaus Aehlig, Tobias Nipkow *)`
`     2 *)`
`       `
`     3 `
`     2 `
`     4 header {* Test of normalization function *}`
`     3 header {* Testing implementation of normalization by evaluation *}`
`     5 `
`     4 `
`     6 theory NormalForm`
`     5 theory NormalForm`
`     7 imports Main Rational`
`     6 imports Main Rational`
`     8 begin`
`     7 begin`
`     9 `
`     8 `
`    17 lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization`
`    16 lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization`
`    18 lemma "~((0::nat) < (0::nat))" by normalization`
`    17 lemma "~((0::nat) < (0::nat))" by normalization`
`    19 `
`    18 `
`    20 datatype n = Z | S n`
`    19 datatype n = Z | S n`
`    21 `
`    20 `
`    22 consts`
`    21 primrec add :: "n \<Rightarrow> n \<Rightarrow> n" where`
`    23   add :: "n \<Rightarrow> n \<Rightarrow> n"`
`    22    "add Z = id"`
`    24   add2 :: "n \<Rightarrow> n \<Rightarrow> n"`
`    23  | "add (S m) = S o add m"`
`    25   mul :: "n \<Rightarrow> n \<Rightarrow> n"`
`    24 `
`    26   mul2 :: "n \<Rightarrow> n \<Rightarrow> n"`
`    25 primrec add2 :: "n \<Rightarrow> n \<Rightarrow> n" where`
`    27   exp :: "n \<Rightarrow> n \<Rightarrow> n"`
`    26    "add2 Z n = n"`
`    28 primrec`
`    27  | "add2 (S m) n = S(add2 m n)"`
`    29   "add Z = id"`
`       `
`    30   "add (S m) = S o add m"`
`       `
`    31 primrec`
`       `
`    32   "add2 Z n = n"`
`       `
`    33   "add2 (S m) n = S(add2 m n)"`
`       `
`    34 `
`    28 `
`    35 declare add2.simps [code]`
`    29 declare add2.simps [code]`
`    36 lemma [code nbe]: "add2 (add2 n m) k = add2 n (add2 m k)"`
`    30 lemma [code nbe]: "add2 (add2 n m) k = add2 n (add2 m k)"`
`    37   by (induct n) auto`
`    31   by (induct n) auto`
`    38 lemma [code]: "add2 n (S m) =  S (add2 n m)"`
`    32 lemma [code]: "add2 n (S m) =  S (add2 n m)"`
`    42 `
`    36 `
`    43 lemma "add2 (add2 n m) k = add2 n (add2 m k)" by normalization`
`    37 lemma "add2 (add2 n m) k = add2 n (add2 m k)" by normalization`
`    44 lemma "add2 (add2 (S n) (S m)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization`
`    38 lemma "add2 (add2 (S n) (S m)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization`
`    45 lemma "add2 (add2 (S n) (add2 (S m) Z)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization`
`    39 lemma "add2 (add2 (S n) (add2 (S m) Z)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization`
`    46 `
`    40 `
`    47 primrec`
`    41 primrec mul :: "n \<Rightarrow> n \<Rightarrow> n" where`
`    48   "mul Z = (%n. Z)"`
`    42    "mul Z = (%n. Z)"`
`    49   "mul (S m) = (%n. add (mul m n) n)"`
`    43  | "mul (S m) = (%n. add (mul m n) n)"`
`    50 primrec`
`    44 `
`    51   "mul2 Z n = Z"`
`    45 primrec mul2 :: "n \<Rightarrow> n \<Rightarrow> n" where`
`    52   "mul2 (S m) n = add2 n (mul2 m n)"`
`    46    "mul2 Z n = Z"`
`    53 primrec`
`    47  | "mul2 (S m) n = add2 n (mul2 m n)"`
`    54   "exp m Z = S Z"`
`    48 `
`    55   "exp m (S n) = mul (exp m n) m"`
`    49 primrec exp :: "n \<Rightarrow> n \<Rightarrow> n" where`
`       `
`    50    "exp m Z = S Z"`
`       `
`    51  | "exp m (S n) = mul (exp m n) m"`
`    56 `
`    52 `
`    57 lemma "mul2 (S(S(S(S(S Z))))) (S(S(S Z))) = S(S(S(S(S(S(S(S(S(S(S(S(S(S(S Z))))))))))))))" by normalization`
`    53 lemma "mul2 (S(S(S(S(S Z))))) (S(S(S Z))) = S(S(S(S(S(S(S(S(S(S(S(S(S(S(S Z))))))))))))))" by normalization`
`    58 lemma "mul (S(S(S(S(S Z))))) (S(S(S Z))) = S(S(S(S(S(S(S(S(S(S(S(S(S(S(S Z))))))))))))))" by normalization`
`    54 lemma "mul (S(S(S(S(S Z))))) (S(S(S Z))) = S(S(S(S(S(S(S(S(S(S(S(S(S(S(S Z))))))))))))))" by normalization`
`    59 lemma "exp (S(S Z)) (S(S(S(S Z)))) = exp (S(S(S(S Z)))) (S(S Z))" by normalization`
`    55 lemma "exp (S(S Z)) (S(S(S(S Z)))) = exp (S(S(S(S Z)))) (S(S Z))" by normalization`
`    60 `
`    56 `