# HG changeset patch # User haftmann # Date 1502024574 -7200 # Node ID 882abe912da90969a000e7631f4fdbd59756e004 # Parent 455ca98d9de3e7391d68c6ce3cb69242deb2c2f9 do not fall back on nbe if plain evaluation fails diff -r 455ca98d9de3 -r 882abe912da9 NEWS --- a/NEWS Sat Aug 05 22:12:41 2017 +0200 +++ b/NEWS Sun Aug 06 15:02:54 2017 +0200 @@ -116,6 +116,11 @@ *** HOL *** +* Command and antiquotation "value" with modified default strategy: +terms without free variables are always evaluated using plain evaluation +only, with no fallback on normalization by evaluation. +Minor INCOMPATIBILITY. + * Notions of squarefreeness, n-th powers, and prime powers in HOL-Computational_Algebra and HOL-Number_Theory. diff -r 455ca98d9de3 -r 882abe912da9 src/HOL/Tools/value_command.ML --- a/src/HOL/Tools/value_command.ML Sat Aug 05 22:12:41 2017 +0200 +++ b/src/HOL/Tools/value_command.ML Sun Aug 06 15:02:54 2017 +0200 @@ -17,9 +17,7 @@ fun default_value ctxt t = if null (Term.add_frees t []) - then case try (Code_Evaluation.dynamic_value_strict ctxt) t of - SOME t' => t' - | NONE => Nbe.dynamic_value ctxt t + then Code_Evaluation.dynamic_value_strict ctxt t else Nbe.dynamic_value ctxt t; structure Evaluator = Theory_Data diff -r 455ca98d9de3 -r 882abe912da9 src/HOL/ex/Adhoc_Overloading_Examples.thy --- a/src/HOL/ex/Adhoc_Overloading_Examples.thy Sat Aug 05 22:12:41 2017 +0200 +++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy Sun Aug 06 15:02:54 2017 +0200 @@ -38,7 +38,7 @@ adhoc_overloading vars term_vars -value "vars (Fun ''f'' [Var 0, Var 1])" +value [nbe] "vars (Fun ''f'' [Var 0, Var 1])" fun rule_vars :: "('a, 'b) term \ ('a, 'b) term \ 'b set" where "rule_vars (l, r) = vars l \ vars r" @@ -46,7 +46,7 @@ adhoc_overloading vars rule_vars -value "vars (Var 1, Var 0)" +value [nbe] "vars (Var 1, Var 0)" definition trs_vars :: "(('a, 'b) term \ ('a, 'b) term) set \ 'b set" where "trs_vars R = \(rule_vars ` R)" @@ -54,7 +54,7 @@ adhoc_overloading vars trs_vars -value "vars {(Var 1, Var 0)}" +value [nbe] "vars {(Var 1, Var 0)}" text \Sometimes it is necessary to add explicit type constraints before a variant can be determined.\ diff -r 455ca98d9de3 -r 882abe912da9 src/HOL/ex/Normalization_by_Evaluation.thy --- a/src/HOL/ex/Normalization_by_Evaluation.thy Sat Aug 05 22:12:41 2017 +0200 +++ b/src/HOL/ex/Normalization_by_Evaluation.thy Sun Aug 06 15:02:54 2017 +0200 @@ -68,20 +68,20 @@ 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 "rev (a#b#cs) = rev cs @ [b, a]" -value "map (%F. F [a,b,c::'x]) (map map [f,g,h])" -value "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))" -value "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])" +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 "case xs of [] \ True | x#xs \ False" -value "map (%x. case x of None \ False | Some y \ True) xs = P" +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 "case n of Z \ True | S x \ False" +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 "filter (%x. x) ([True,False,x]@xs)" -value "filter Not ([True,False,x]@xs)" +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 @@ -106,7 +106,7 @@ 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 "Suc 0 \ set ms" +value [nbe] "Suc 0 \ set ms" (* non-left-linear patterns, equality by extensionality *) @@ -115,13 +115,13 @@ 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 "(\x. x)" +value [nbe] "(\x. x)" (* Church numerals: *) -value "(%m n f x. m f (n f x)) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))" -value "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))" -value "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))" +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 *) diff -r 455ca98d9de3 -r 882abe912da9 src/HOL/ex/Transitive_Closure_Table_Ex.thy --- a/src/HOL/ex/Transitive_Closure_Table_Ex.thy Sat Aug 05 22:12:41 2017 +0200 +++ b/src/HOL/ex/Transitive_Closure_Table_Ex.thy Sun Aug 06 15:02:54 2017 +0200 @@ -24,7 +24,7 @@ values "{x. test\<^sup>*\<^sup>* A x}" values "{x. test\<^sup>*\<^sup>* x C}" -value "test\<^sup>*\<^sup>* A C" -value "test\<^sup>*\<^sup>* C A" +value [nbe] "test\<^sup>*\<^sup>* A C" +value [nbe] "test\<^sup>*\<^sup>* C A" end