Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Normalization_by_Evaluation.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Authors:  Klaus Aehlig, Tobias Nipkow *)

section \<open>Testing implementation of normalization by evaluation\<close>

theory Normalization_by_Evaluation
imports Complex_Main
begin

lemma "True" by normalization
lemma "p \ True" by normalization
declare disj_assoc [code nbe]
lemma "((P | Q) | R) = (P | (Q | R))" by normalization
lemma "0 + (n::nat) = n" by normalization
lemma "0 + Suc n = Suc n" by normalization
lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization
lemma "~((0::nat) < (0::nat))" by normalization

datatype n = Z | S n

primrec add :: "n \ n \ n" where
   "add Z = id"
| "add (S m) = S o add m"

primrec add2 :: "n \ n \ n" where
   "add2 Z n = n"
| "add2 (S m) n = S(add2 m n)"

declare add2.simps [code]
lemma [code nbe]: "add2 (add2 n m) k = add2 n (add2 m k)"
  by (induct n) auto
lemma [code]: "add2 n (S m) = S (add2 n m)"
  by(induct n) auto
lemma [code]: "add2 n Z = n"
  by(induct n) auto

lemma "add2 (add2 n m) k = add2 n (add2 m k)" by normalization
lemma "add2 (add2 (S n) (S m)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization
lemma "add2 (add2 (S n) (add2 (S m) Z)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization

primrec mul :: "n \ n \ n" where
   "mul Z = (%n. Z)"
| "mul (S m) = (%n. add (mul m n) n)"

primrec mul2 :: "n \ n \ n" where
   "mul2 Z n = Z"
| "mul2 (S m) n = add2 n (mul2 m n)"

primrec exp :: "n \ n \ n" where
   "exp m Z = S Z"
| "exp m (S n) = mul (exp m n) m"

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
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
lemma "exp (S(S Z)) (S(S(S(S Z)))) = exp (S(S(S(S Z)))) (S(S Z))" by normalization

lemma "(let ((x,y),(u,v)) = ((Z,Z),(Z,Z)) in add (add x y) (add u v)) = Z" by normalization
lemma "case_prod (%x y. x) (a, b) = a" by normalization
lemma "(%((x,y),(u,v)). add (add x y) (add u v)) ((Z,Z),(Z,Z)) = Z" by normalization

lemma "case Z of Z \ True | S x \ False" by normalization

lemma "[] @ [] = []" by normalization
lemma "map f [x,y,z::'x] = [f x, f y, f z]" by normalization
lemma "[a, b, c] @ xs = a # b # c # xs" by normalization
lemma "[] @ xs = xs" by normalization
lemma "map (%f. f True) [id, g, Not] = [True, g True, False]" by normalization

lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs"
  by normalization rule
lemma "rev [a, b, c] = [c, b, a]" by normalization
value [nbe] "rev (a#b#cs) = rev cs @ [b, a]"
value [nbe] "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
value [nbe] "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))"
value [nbe] "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])"
lemma "map (%x. case x of None \ False | Some y \ True) [None, Some ()] = [False, True]"
  by normalization
value [nbe] "case xs of [] \ True | x#xs \ False"
value [nbe] "map (%x. case x of None \ False | Some y \ True) xs = P"
lemma "let x = y in [x, x] = [y, y]" by normalization
lemma "Let y (%x. [x,x]) = [y, y]" by normalization
value [nbe] "case n of Z \ True | S x \ False"
lemma "(%(x,y). add x y) (S z,S z) = S (add z (S z))" by normalization
value [nbe] "filter (%x. x) ([True,False,x]@xs)"
value [nbe] "filter Not ([True,False,x]@xs)"

lemma "[x,y,z] @ [a,b,c] = [x, y, z, a, b, c]" by normalization
lemma "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f]" by normalization
lemma "map (%x. case x of None \ False | Some y \ True) [None, Some ()] = [False, True]" by normalization

lemma "last [a, b, c] = c" by normalization
lemma "last ([a, b, c] @ xs) = last (c # xs)" by normalization

lemma "(2::int) + 3 - 1 + (- k) * 2 = 4 + - k * 2" by normalization
lemma "(-4::int) * 2 = -8" by normalization
lemma "\(-4::int) + 2 * 1\ = 2" by normalization
lemma "(2::int) + 3 = 5" by normalization
lemma "(2::int) + 3 * (- 4) * (- 1) = 14" by normalization
lemma "(2::int) + 3 * (- 4) * 1 + 0 = -10" by normalization
lemma "(2::int) < 3" by normalization
lemma "(2::int) <= 3" by normalization
lemma "\(-4::int) + 2 * 1\ = 2" by normalization
lemma "4 - 42 * \3 + (-7::int)\ = -164" by normalization
lemma "(if (0::nat) \ (x::nat) then 0::nat else x) = 0" by normalization
lemma "4 = Suc (Suc (Suc (Suc 0)))" by normalization
lemma "nat 4 = Suc (Suc (Suc (Suc 0)))" by normalization
lemma "[Suc 0, 0] = [Suc 0, 0]" by normalization
lemma "max (Suc 0) 0 = Suc 0" by normalization
lemma "(42::rat) / 1704 = 1 / 284 + 3 / 142" by normalization
value [nbe] "Suc 0 \ set ms"

(* non-left-linear patterns, equality by extensionality *)

lemma "f = f" by normalization
lemma "f x = f x" by normalization
lemma "(f o g) x = f (g x)" by normalization
lemma "(f o id) x = f x" by normalization
lemma "(id :: bool \ bool) = id" by normalization
value [nbe] "(\x. x)"

(* Church numerals: *)

value [nbe] "(%m n f x. m f (n f x)) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
value [nbe] "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
value [nbe] "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"

(* handling of type classes in connection with equality *)

lemma "map f [x, y] = [f x, f y]" by normalization
lemma "(map f [x, y], w) = ([f x, f y], w)" by normalization
lemma "map f [x, y] = [f x :: 'a::semigroup_add, f y]" by normalization
lemma "map f [x :: 'a::semigroup_add, y] = [f x, f y]" by normalization
lemma "(map f [x :: 'a::semigroup_add, y], w :: 'b::finite) = ([f x, f y], w)" by normalization

end

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.