summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Tue, 31 Oct 2006 09:29:08 +0100 | |

changeset 21117 | e8657a20a52f |

parent 21116 | be58cded79da |

child 21118 | d9789a87825d |

*** empty log message ***

src/HOL/ex/CodeEval.thy | file | annotate | diff | comparison | revisions | |

src/HOL/ex/NormalForm.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/ex/CodeEval.thy Tue Oct 31 09:29:06 2006 +0100 +++ b/src/HOL/ex/CodeEval.thy Tue Oct 31 09:29:08 2006 +0100 @@ -180,8 +180,8 @@ subsection {* Small examples *} +ML {* Eval.term "(Suc 2 + Suc 0) * Suc 3" *} ML {* Eval.term "[]::nat list" *} -ML {* Eval.term "(Suc 2 + Suc 0) * Suc 3" *} ML {* Eval.term "fst ([]::nat list, Suc 0) = []" *} text {* a fancy datatype *}

--- a/src/HOL/ex/NormalForm.thy Tue Oct 31 09:29:06 2006 +0100 +++ b/src/HOL/ex/NormalForm.thy Tue Oct 31 09:29:08 2006 +0100 @@ -8,6 +8,8 @@ imports Main begin +lemma "True" by normalization +lemma "x = x" by normalization lemma "p \<longrightarrow> True" by normalization declare disj_assoc [code func] lemma "((P | Q) | R) = (P | (Q | R))" by normalization @@ -64,15 +66,17 @@ lemma "[] @ [] = []" by normalization lemma "[] @ xs = xs" by normalization -lemma "[a \<Colon> 'd, b, c] @ xs = a # b # c # xs" by normalization +lemma "[a, b, c] @ xs = a # b # c # xs" by normalization lemma "[%a::'x. a, %b. b, c] @ xs = (%x. x) # (%x. x) # c # xs" by normalization -lemma "[%a::'x. a, %b. b, c] @ [u,v] = [%x. x, %x. x, c, u, v]" by normalization +lemma "[%a::'x. a, %b. b, c] @ [u, v] = [%x. x, %x. x, c, u, v]" by normalization lemma "map f [x,y,z::'x] = [f x, f y, f z]" by normalization -normal_form "map (%f. f True) [id,g,Not]" -normal_form "map (%f. f True) ([id,g,Not] @ fs)" -lemma "rev[a,b,c] = [c, b, a]" by normalization -normal_form "rev(a#b#cs)" -lemma "map map [f,g,h] = [map f, map g, map h]" 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 +lemma "rev [a, b, c] = [c, b, a]" by normalization +(*normal_form "rev (a#b#cs)" +normal_form "rev cs @ [b, a]"*) +(*lemma "rev (a#b#cs) = rev cs @ [b, a]" by normalization*) +lemma "map map [f, g, h] = [map f, map g, map h]" by normalization normal_form "map (%F. F [a,b,c::'x]) (map map [f,g,h])" normal_form "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))" normal_form "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])" @@ -87,10 +91,11 @@ normal_form "filter Not ([True,False,x]@xs)" lemma "[x,y,z] @ [a,b,c] = [x, y, z, a, b ,c]" by normalization -normal_form "%(xs, ys). xs @ ys" -normal_form "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f])" +lemma "(%(xs, ys). xs @ ys) = split op @" by normalization +lemma "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f]" by normalization normal_form "%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True" -normal_form "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()]" +lemma "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()] = [False, True]" + by normalization lemma "last [a, b, c] = c" by normalization