added evaluation examples
authorhaftmann
Thu Aug 16 11:45:05 2007 +0200 (2007-08-16)
changeset 2429226ac9fe0e80e
parent 24291 fa72aab966dc
child 24293 7e67b9706211
added evaluation examples
src/HOL/ex/Eval_Examples.thy
src/Tools/nbe.ML
     1.1 --- a/src/HOL/ex/Eval_Examples.thy	Wed Aug 15 22:21:13 2007 +0200
     1.2 +++ b/src/HOL/ex/Eval_Examples.thy	Thu Aug 16 11:45:05 2007 +0200
     1.3 @@ -8,12 +8,21 @@
     1.4  imports Eval
     1.5  begin
     1.6  
     1.7 +text {* SML evaluation oracle *}
     1.8 +
     1.9 +lemma "True \<or> False" by evaluation
    1.10 +lemma "\<not> (Suc 0 = Suc 1)" by evaluation
    1.11 +lemma "[] = ([]\<Colon> int list)" by evaluation
    1.12 +lemma "[()] = [()]" by evaluation
    1.13 +lemma "fst ([]::nat list, Suc 0) = []" by evaluation
    1.14 +
    1.15  text {* evaluation oracle *}
    1.16  
    1.17  lemma "True \<or> False" by eval
    1.18  lemma "\<not> (Suc 0 = Suc 1)" by eval
    1.19  lemma "[] = ([]\<Colon> int list)" by eval
    1.20  lemma "[()] = [()]" by eval
    1.21 +lemma "fst ([]::nat list, Suc 0) = []" by eval
    1.22  
    1.23  text {* term evaluation *}
    1.24  
    1.25 @@ -24,7 +33,6 @@
    1.26  value (overloaded) "(10\<Colon>int) \<le> 12"
    1.27  value (overloaded) "[(nat 100, ())]"
    1.28  value (overloaded) "[]::nat list"
    1.29 -value (overloaded) "fst ([]::nat list, Suc 0) = []"
    1.30  
    1.31  text {* a fancy datatype *}
    1.32  
     2.1 --- a/src/Tools/nbe.ML	Wed Aug 15 22:21:13 2007 +0200
     2.2 +++ b/src/Tools/nbe.ML	Thu Aug 16 11:45:05 2007 +0200
     2.3 @@ -346,7 +346,7 @@
     2.4    Logic.mk_equals (t, eval thy code t t' deps);
     2.5  
     2.6  fun normalization_invoke thy code t t' deps =
     2.7 -  Thm.invoke_oracle_i thy "Code_Setup.normalization" (thy, Normalization (code, t, t', deps));
     2.8 +  Thm.invoke_oracle_i thy "HOL.normalization" (thy, Normalization (code, t, t', deps));
     2.9    (*FIXME get rid of hardwired theory name*)
    2.10  
    2.11  fun normalization_conv ct =