do not fall back on nbe if plain evaluation fails
authorhaftmann
Sun Aug 06 15:02:54 2017 +0200 (21 months ago)
changeset 66345882abe912da9
parent 66344 455ca98d9de3
child 66354 8bf96de50193
do not fall back on nbe if plain evaluation fails
NEWS
src/HOL/Tools/value_command.ML
src/HOL/ex/Adhoc_Overloading_Examples.thy
src/HOL/ex/Normalization_by_Evaluation.thy
src/HOL/ex/Transitive_Closure_Table_Ex.thy
     1.1 --- a/NEWS	Sat Aug 05 22:12:41 2017 +0200
     1.2 +++ b/NEWS	Sun Aug 06 15:02:54 2017 +0200
     1.3 @@ -116,6 +116,11 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Command and antiquotation "value" with modified default strategy:
     1.8 +terms without free variables are always evaluated using plain evaluation
     1.9 +only, with no fallback on normalization by evaluation.
    1.10 +Minor INCOMPATIBILITY.
    1.11 +
    1.12  * Notions of squarefreeness, n-th powers, and prime powers in
    1.13  HOL-Computational_Algebra and HOL-Number_Theory.
    1.14  
     2.1 --- a/src/HOL/Tools/value_command.ML	Sat Aug 05 22:12:41 2017 +0200
     2.2 +++ b/src/HOL/Tools/value_command.ML	Sun Aug 06 15:02:54 2017 +0200
     2.3 @@ -17,9 +17,7 @@
     2.4  
     2.5  fun default_value ctxt t =
     2.6    if null (Term.add_frees t [])
     2.7 -  then case try (Code_Evaluation.dynamic_value_strict ctxt) t of
     2.8 -    SOME t' => t'
     2.9 -  | NONE => Nbe.dynamic_value ctxt t
    2.10 +  then Code_Evaluation.dynamic_value_strict ctxt t
    2.11    else Nbe.dynamic_value ctxt t;
    2.12  
    2.13  structure Evaluator = Theory_Data
     3.1 --- a/src/HOL/ex/Adhoc_Overloading_Examples.thy	Sat Aug 05 22:12:41 2017 +0200
     3.2 +++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy	Sun Aug 06 15:02:54 2017 +0200
     3.3 @@ -38,7 +38,7 @@
     3.4  adhoc_overloading
     3.5    vars term_vars
     3.6  
     3.7 -value "vars (Fun ''f'' [Var 0, Var 1])"
     3.8 +value [nbe] "vars (Fun ''f'' [Var 0, Var 1])"
     3.9  
    3.10  fun rule_vars :: "('a, 'b) term \<times> ('a, 'b) term \<Rightarrow> 'b set" where
    3.11    "rule_vars (l, r) = vars l \<union> vars r"
    3.12 @@ -46,7 +46,7 @@
    3.13  adhoc_overloading
    3.14    vars rule_vars
    3.15  
    3.16 -value "vars (Var 1, Var 0)"
    3.17 +value [nbe] "vars (Var 1, Var 0)"
    3.18  
    3.19  definition trs_vars :: "(('a, 'b) term \<times> ('a, 'b) term) set \<Rightarrow> 'b set" where
    3.20    "trs_vars R = \<Union>(rule_vars ` R)"
    3.21 @@ -54,7 +54,7 @@
    3.22  adhoc_overloading
    3.23    vars trs_vars
    3.24  
    3.25 -value "vars {(Var 1, Var 0)}"
    3.26 +value [nbe] "vars {(Var 1, Var 0)}"
    3.27  
    3.28  text \<open>Sometimes it is necessary to add explicit type constraints
    3.29  before a variant can be determined.\<close>
     4.1 --- a/src/HOL/ex/Normalization_by_Evaluation.thy	Sat Aug 05 22:12:41 2017 +0200
     4.2 +++ b/src/HOL/ex/Normalization_by_Evaluation.thy	Sun Aug 06 15:02:54 2017 +0200
     4.3 @@ -68,20 +68,20 @@
     4.4  lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs"
     4.5    by normalization rule
     4.6  lemma "rev [a, b, c] = [c, b, a]" by normalization
     4.7 -value "rev (a#b#cs) = rev cs @ [b, a]"
     4.8 -value "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
     4.9 -value "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))"
    4.10 -value "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])"
    4.11 +value [nbe] "rev (a#b#cs) = rev cs @ [b, a]"
    4.12 +value [nbe] "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
    4.13 +value [nbe] "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))"
    4.14 +value [nbe] "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])"
    4.15  lemma "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()] = [False, True]" 
    4.16    by normalization
    4.17 -value "case xs of [] \<Rightarrow> True | x#xs \<Rightarrow> False"
    4.18 -value "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) xs = P"
    4.19 +value [nbe] "case xs of [] \<Rightarrow> True | x#xs \<Rightarrow> False"
    4.20 +value [nbe] "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) xs = P"
    4.21  lemma "let x = y in [x, x] = [y, y]" by normalization
    4.22  lemma "Let y (%x. [x,x]) = [y, y]" by normalization
    4.23 -value "case n of Z \<Rightarrow> True | S x \<Rightarrow> False"
    4.24 +value [nbe] "case n of Z \<Rightarrow> True | S x \<Rightarrow> False"
    4.25  lemma "(%(x,y). add x y) (S z,S z) = S (add z (S z))" by normalization
    4.26 -value "filter (%x. x) ([True,False,x]@xs)"
    4.27 -value "filter Not ([True,False,x]@xs)"
    4.28 +value [nbe] "filter (%x. x) ([True,False,x]@xs)"
    4.29 +value [nbe] "filter Not ([True,False,x]@xs)"
    4.30  
    4.31  lemma "[x,y,z] @ [a,b,c] = [x, y, z, a, b, c]" by normalization
    4.32  lemma "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f]" by normalization
    4.33 @@ -106,7 +106,7 @@
    4.34  lemma "[Suc 0, 0] = [Suc 0, 0]" by normalization
    4.35  lemma "max (Suc 0) 0 = Suc 0" by normalization
    4.36  lemma "(42::rat) / 1704 = 1 / 284 + 3 / 142" by normalization
    4.37 -value "Suc 0 \<in> set ms"
    4.38 +value [nbe] "Suc 0 \<in> set ms"
    4.39  
    4.40  (* non-left-linear patterns, equality by extensionality *)
    4.41  
    4.42 @@ -115,13 +115,13 @@
    4.43  lemma "(f o g) x = f (g x)" by normalization
    4.44  lemma "(f o id) x = f x" by normalization
    4.45  lemma "(id :: bool \<Rightarrow> bool) = id" by normalization
    4.46 -value "(\<lambda>x. x)"
    4.47 +value [nbe] "(\<lambda>x. x)"
    4.48  
    4.49  (* Church numerals: *)
    4.50  
    4.51 -value "(%m n f x. m f (n f x)) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
    4.52 -value "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
    4.53 -value "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
    4.54 +value [nbe] "(%m n f x. m f (n f x)) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
    4.55 +value [nbe] "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
    4.56 +value [nbe] "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
    4.57  
    4.58  (* handling of type classes in connection with equality *)
    4.59  
     5.1 --- a/src/HOL/ex/Transitive_Closure_Table_Ex.thy	Sat Aug 05 22:12:41 2017 +0200
     5.2 +++ b/src/HOL/ex/Transitive_Closure_Table_Ex.thy	Sun Aug 06 15:02:54 2017 +0200
     5.3 @@ -24,7 +24,7 @@
     5.4  values "{x. test\<^sup>*\<^sup>* A x}"
     5.5  values "{x. test\<^sup>*\<^sup>* x C}"
     5.6  
     5.7 -value "test\<^sup>*\<^sup>* A C"
     5.8 -value "test\<^sup>*\<^sup>* C A"
     5.9 +value [nbe] "test\<^sup>*\<^sup>* A C"
    5.10 +value [nbe] "test\<^sup>*\<^sup>* C A"
    5.11  
    5.12  end