--- a/src/HOL/Int.thy Fri May 08 08:06:43 2009 +0200
+++ b/src/HOL/Int.thy Fri May 08 08:07:05 2009 +0200
@@ -15,6 +15,9 @@
"~~/src/Provers/Arith/assoc_fold.ML"
"~~/src/Provers/Arith/cancel_numerals.ML"
"~~/src/Provers/Arith/combine_numerals.ML"
+ "~~/src/Provers/Arith/cancel_numeral_factor.ML"
+ "~~/src/Provers/Arith/extract_common_term.ML"
+ ("Tools/int_factor_simprocs.ML")
("Tools/int_arith.ML")
begin
@@ -1517,10 +1520,11 @@
use "Tools/int_arith.ML"
declaration {* K Int_Arith.setup *}
+use "Tools/int_factor_simprocs.ML"
setup {*
ReorientProc.add
- (fn Const(@{const_name number_of}, _) $ _ => true | _ => false)
+ (fn Const (@{const_name number_of}, _) $ _ => true | _ => false)
*}
simproc_setup reorient_numeral ("number_of w = x") = ReorientProc.proc
--- a/src/HOL/IntDiv.thy Fri May 08 08:06:43 2009 +0200
+++ b/src/HOL/IntDiv.thy Fri May 08 08:07:05 2009 +0200
@@ -8,10 +8,6 @@
theory IntDiv
imports Int Divides FunDef
-uses
- "~~/src/Provers/Arith/cancel_numeral_factor.ML"
- "~~/src/Provers/Arith/extract_common_term.ML"
- ("Tools/int_factor_simprocs.ML")
begin
definition divmod_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" where
@@ -724,7 +720,6 @@
apply (auto simp add: divmod_rel_def)
apply (auto simp add: algebra_simps)
apply (auto simp add: zero_less_mult_iff zero_le_mult_iff mult_le_0_iff)
- apply (simp_all add: mult_less_cancel_left_disj mult_commute [of _ a])
done
moreover with `c \<noteq> 0` divmod_rel_div_mod have "divmod_rel b c (b div c, b mod c)" by auto
ultimately have "divmod_rel (a * b) (a * c) (b div c, a * (b mod c))" .
@@ -1078,8 +1073,6 @@
prefer 2
apply (blast intro: order_less_trans)
apply (simp add: zero_less_mult_iff)
- apply (subgoal_tac "n * k < n * 1")
- apply (drule mult_less_cancel_left [THEN iffD1], auto)
done
lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"
@@ -1334,11 +1327,6 @@
qed
-subsection {* Simproc setup *}
-
-use "Tools/int_factor_simprocs.ML"
-
-
subsection {* Code generation *}
definition pdivmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
--- a/src/HOL/IsaMakefile Fri May 08 08:06:43 2009 +0200
+++ b/src/HOL/IsaMakefile Fri May 08 08:07:05 2009 +0200
@@ -342,6 +342,7 @@
Library/Random.thy Library/Quickcheck.thy \
Library/Poly_Deriv.thy \
Library/Polynomial.thy \
+ Library/Preorder.thy \
Library/Product_plus.thy \
Library/Product_Vector.thy \
Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML \
--- a/src/HOL/Library/Library.thy Fri May 08 08:06:43 2009 +0200
+++ b/src/HOL/Library/Library.thy Fri May 08 08:07:05 2009 +0200
@@ -42,6 +42,7 @@
Pocklington
Poly_Deriv
Polynomial
+ Preorder
Primes
Product_Vector
Quickcheck
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Preorder.thy Fri May 08 08:07:05 2009 +0200
@@ -0,0 +1,65 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Preorders with explicit equivalence relation *}
+
+theory Preorder
+imports Orderings
+begin
+
+class preorder_equiv = preorder
+begin
+
+definition equiv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
+ "equiv x y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
+
+notation
+ equiv ("op ~~") and
+ equiv ("(_/ ~~ _)" [51, 51] 50)
+
+notation (xsymbols)
+ equiv ("op \<approx>") and
+ equiv ("(_/ \<approx> _)" [51, 51] 50)
+
+notation (HTML output)
+ equiv ("op \<approx>") and
+ equiv ("(_/ \<approx> _)" [51, 51] 50)
+
+lemma refl [iff]:
+ "x \<approx> x"
+ unfolding equiv_def by simp
+
+lemma trans:
+ "x \<approx> y \<Longrightarrow> y \<approx> z \<Longrightarrow> x \<approx> z"
+ unfolding equiv_def by (auto intro: order_trans)
+
+lemma antisym:
+ "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x \<approx> y"
+ unfolding equiv_def ..
+
+lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> x \<approx> y"
+ by (auto simp add: equiv_def less_le_not_le)
+
+lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x \<approx> y"
+ by (auto simp add: equiv_def less_le)
+
+lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x \<approx> y"
+ by (simp add: less_le)
+
+lemma less_imp_not_eq: "x < y \<Longrightarrow> x \<approx> y \<longleftrightarrow> False"
+ by (simp add: less_le)
+
+lemma less_imp_not_eq2: "x < y \<Longrightarrow> y \<approx> x \<longleftrightarrow> False"
+ by (simp add: equiv_def less_le)
+
+lemma neq_le_trans: "\<not> a \<approx> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b"
+ by (simp add: less_le)
+
+lemma le_neq_trans: "a \<le> b \<Longrightarrow> \<not> a \<approx> b \<Longrightarrow> a < b"
+ by (simp add: less_le)
+
+lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x \<approx> y"
+ by (simp add: equiv_def)
+
+end
+
+end
--- a/src/HOL/Tools/int_factor_simprocs.ML Fri May 08 08:06:43 2009 +0200
+++ b/src/HOL/Tools/int_factor_simprocs.ML Fri May 08 08:07:05 2009 +0200
@@ -222,7 +222,7 @@
simplify_one ss (([th, cancel_th]) MRS trans);
local
- val Tp_Eq = Thm.reflexive(Thm.cterm_of (@{theory HOL}) HOLogic.Trueprop)
+ val Tp_Eq = Thm.reflexive (Thm.cterm_of @{theory HOL} HOLogic.Trueprop)
fun Eq_True_elim Eq =
Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI}
in
@@ -297,7 +297,7 @@
(open CancelFactorCommon
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_binop @{const_name Divides.mod}
- val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} HOLogic.intT
+ val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} Term.dummyT
val simp_conv = K (K (SOME @{thm mod_mult_mult1}))
);
--- a/src/HOL/ex/Arith_Examples.thy Fri May 08 08:06:43 2009 +0200
+++ b/src/HOL/ex/Arith_Examples.thy Fri May 08 08:07:05 2009 +0200
@@ -4,7 +4,9 @@
header {* Arithmetic *}
-theory Arith_Examples imports Main begin
+theory Arith_Examples
+imports Main
+begin
text {*
The @{text arith} method is used frequently throughout the Isabelle
@@ -35,87 +37,87 @@
@{term Divides.div} *}
lemma "(i::nat) <= max i j"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "(i::int) <= max i j"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "min i j <= (i::nat)"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "min i j <= (i::int)"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "min (i::nat) j <= max i j"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "min (i::int) j <= max i j"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "min (i::nat) j + max i j = i + j"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "min (i::int) j + max i j = i + j"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "(i::nat) < j ==> min i j < max i j"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "(i::int) < j ==> min i j < max i j"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "(0::int) <= abs i"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "(i::int) <= abs i"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "abs (abs (i::int)) = abs i"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
text {* Also testing subgoals with bound variables. *}
lemma "!!x. (x::nat) <= y ==> x - y = 0"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "!!x. (x::nat) - y = 0 ==> x <= y"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "!!x. ((x::nat) <= y) = (x - y = 0)"
- by (tactic {* linear_arith_tac @{context} 1 *})
+ by linarith
lemma "[| (x::nat) < y; d < 1 |] ==> x - y = d"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "[| (x::nat) < y; d < 1 |] ==> x - y - x = d - x"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "(x::int) < y ==> x - y < 0"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "nat (i + j) <= nat i + nat j"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "i < j ==> nat (i - j) = 0"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "(i::nat) mod 0 = i"
(* FIXME: need to replace 0 by its numeral representation *)
apply (subst nat_numeral_0_eq_0 [symmetric])
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "(i::nat) mod 1 = 0"
(* FIXME: need to replace 1 by its numeral representation *)
apply (subst nat_numeral_1_eq_1 [symmetric])
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "(i::nat) mod 42 <= 41"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "(i::int) mod 0 = i"
(* FIXME: need to replace 0 by its numeral representation *)
apply (subst numeral_0_eq_0 [symmetric])
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "(i::int) mod 1 = 0"
(* FIXME: need to replace 1 by its numeral representation *)
@@ -130,70 +132,70 @@
oops
lemma "-(i::int) * 1 = 0 ==> i = 0"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "[| (0::int) < abs i; abs i * 1 < abs i * j |] ==> 1 < abs i * j"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
subsection {* Meta-Logic *}
lemma "x < Suc y == x <= y"
- by (tactic {* linear_arith_tac @{context} 1 *})
+ by linarith
lemma "((x::nat) == z ==> x ~= y) ==> x ~= y | z ~= y"
- by (tactic {* linear_arith_tac @{context} 1 *})
+ by linarith
subsection {* Various Other Examples *}
lemma "(x < Suc y) = (x <= y)"
- by (tactic {* linear_arith_tac @{context} 1 *})
+ by linarith
lemma "[| (x::nat) < y; y < z |] ==> x < z"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "(x::nat) < y & y < z ==> x < z"
- by (tactic {* linear_arith_tac @{context} 1 *})
+ by linarith
text {* This example involves no arithmetic at all, but is solved by
preprocessing (i.e. NNF normalization) alone. *}
lemma "(P::bool) = Q ==> Q = P"
- by (tactic {* linear_arith_tac @{context} 1 *})
+ by linarith
lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> min (x::nat) y = 0"
- by (tactic {* linear_arith_tac @{context} 1 *})
+ by linarith
lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> max (x::nat) y = x + y"
- by (tactic {* linear_arith_tac @{context} 1 *})
+ by linarith
lemma "[| (x::nat) ~= y; a + 2 = b; a < y; y < b; a < x; x < b |] ==> False"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "[| (x::nat) > y; y > z; z > x |] ==> False"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "(x::nat) - 5 > y ==> y < x"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "(x::nat) ~= 0 ==> 0 < x"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "[| (x::nat) ~= y; x <= y |] ==> x < y"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "[| (x::nat) < y; P (x - y) |] ==> P 0"
- by (tactic {* linear_arith_tac @{context} 1 *})
+ by linarith
lemma "(x - y) - (x::nat) = (x - x) - y"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "[| (a::nat) < b; c < d |] ==> (a - b) = (c - d)"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "((a::nat) - (b - (c - (d - e)))) = (a - (b - (c - (d - e))))"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "(n < m & m < n') | (n < m & m = n') | (n < n' & n' < m) |
(n = n' & n' < m) | (n = m & m < n') |
@@ -218,28 +220,28 @@
text {* Constants. *}
lemma "(0::nat) < 1"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "(0::int) < 1"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "(47::nat) + 11 < 08 * 15"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
lemma "(47::int) + 11 < 08 * 15"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
text {* Splitting of inequalities of different type. *}
lemma "[| (a::nat) ~= b; (i::int) ~= j; a < 2; b < 2 |] ==>
a + b <= nat (max (abs i) (abs j))"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
text {* Again, but different order. *}
lemma "[| (i::int) ~= j; (a::nat) ~= b; a < 2; b < 2 |] ==>
a + b <= nat (max (abs i) (abs j))"
- by (tactic {* fast_arith_tac @{context} 1 *})
+ by linarith
(*
ML {* reset trace_arith; *}
--- a/src/HOL/ex/BinEx.thy Fri May 08 08:06:43 2009 +0200
+++ b/src/HOL/ex/BinEx.thy Fri May 08 08:07:05 2009 +0200
@@ -712,38 +712,38 @@
by arith
lemma "!!a::real. a \<le> b ==> c \<le> d ==> x + y < z ==> a + c \<le> b + d"
-by (tactic "fast_arith_tac @{context} 1")
+by linarith
lemma "!!a::real. a < b ==> c < d ==> a - d \<le> b + (-c)"
-by (tactic "fast_arith_tac @{context} 1")
+by linarith
lemma "!!a::real. a \<le> b ==> b + b \<le> c ==> a + a \<le> c"
-by (tactic "fast_arith_tac @{context} 1")
+by linarith
lemma "!!a::real. a + b \<le> i + j ==> a \<le> b ==> i \<le> j ==> a + a \<le> j + j"
-by (tactic "fast_arith_tac @{context} 1")
+by linarith
lemma "!!a::real. a + b < i + j ==> a < b ==> i < j ==> a + a < j + j"
-by (tactic "fast_arith_tac @{context} 1")
+by linarith
lemma "!!a::real. a + b + c \<le> i + j + k \<and> a \<le> b \<and> b \<le> c \<and> i \<le> j \<and> j \<le> k --> a + a + a \<le> k + k + k"
by arith
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a \<le> l"
-by (tactic "fast_arith_tac @{context} 1")
+by linarith
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a \<le> l + l + l + l"
-by (tactic "fast_arith_tac @{context} 1")
+by linarith
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a \<le> l + l + l + l + i"
-by (tactic "fast_arith_tac @{context} 1")
+by linarith
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a + a \<le> l + l + l + l + i + l"
-by (tactic "fast_arith_tac @{context} 1")
+by linarith
subsection{*Complex Arithmetic*}
--- a/src/HOL/ex/NormalForm.thy Fri May 08 08:06:43 2009 +0200
+++ b/src/HOL/ex/NormalForm.thy Fri May 08 08:07:05 2009 +0200
@@ -10,7 +10,6 @@
lemma "p \<longrightarrow> True" by normalization
declare disj_assoc [code nbe]
lemma "((P | Q) | R) = (P | (Q | R))" by normalization
-declare disj_assoc [code del]
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
--- a/src/Tools/code/code_ml.ML Fri May 08 08:06:43 2009 +0200
+++ b/src/Tools/code/code_ml.ML Fri May 08 08:07:05 2009 +0200
@@ -958,10 +958,7 @@
fun eval some_target reff postproc thy t args =
let
val ctxt = ProofContext.init thy;
- val _ = if null (Term.add_frees t []) then () else error ("Term "
- ^ quote (Syntax.string_of_term_global thy t)
- ^ " to be evaluated contains free variables");
- fun evaluator naming program (((_, (_, ty)), _), t) deps =
+ fun evaluator naming program ((_, (_, ty)), t) deps =
let
val _ = if Code_Thingol.contains_dictvar t then
error "Term to be evaluated contains free dictionaries" else ();
--- a/src/Tools/code/code_thingol.ML Fri May 08 08:06:43 2009 +0200
+++ b/src/Tools/code/code_thingol.ML Fri May 08 08:07:05 2009 +0200
@@ -85,10 +85,10 @@
val consts_program: theory -> string list -> string list * (naming * program)
val cached_program: theory -> naming * program
val eval_conv: theory -> (sort -> sort)
- -> (naming -> program -> (((string * sort) list * typscheme) * (string * itype) list) * iterm -> string list -> cterm -> thm)
+ -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> cterm -> thm)
-> cterm -> thm
val eval: theory -> (sort -> sort) -> ((term -> term) -> 'a -> 'a)
- -> (naming -> program -> (((string * sort) list * typscheme) * (string * itype) list) * iterm -> string list -> 'a)
+ -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
-> term -> 'a
end;
@@ -755,7 +755,7 @@
(* value evaluation *)
-fun ensure_value thy algbr funcgr (fs, t) =
+fun ensure_value thy algbr funcgr t =
let
val ty = fastype_of t;
val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
@@ -766,7 +766,7 @@
##>> translate_term thy algbr funcgr NONE t
#>> (fn ((vs, ty), t) => Fun
(Term.dummy_patternN, ((vs, ty), [(([], t), (Drule.dummy_thm, true))])));
- fun term_value fs (dep, (naming, program1)) =
+ fun term_value (dep, (naming, program1)) =
let
val Fun (_, (vs_ty, [(([], t), _)])) =
Graph.get_node program1 Term.dummy_patternN;
@@ -774,22 +774,19 @@
val program2 = Graph.del_nodes [Term.dummy_patternN] program1;
val deps_all = Graph.all_succs program2 deps;
val program3 = Graph.subgraph (member (op =) deps_all) program2;
- in (((naming, program3), (((vs_ty, fs), t), deps)), (dep, (naming, program2))) end;
+ in (((naming, program3), ((vs_ty, t), deps)), (dep, (naming, program2))) end;
in
ensure_stmt ((K o K) NONE) pair stmt_value Term.dummy_patternN
#> snd
- #> fold_map (fn (v, ty) => translate_typ thy algbr funcgr ty
- #-> (fn ty' => pair (v, ty'))) fs
- #-> (fn fs' => term_value fs')
+ #> term_value
end;
fun base_evaluator thy evaluator algebra funcgr vs t =
let
- val fs = Term.add_frees t [];
- val (((naming, program), ((((vs', ty'), fs'), t'), deps)), _) =
- invoke_generation thy (algebra, funcgr) ensure_value (fs, t);
+ val (((naming, program), (((vs', ty'), t'), deps)), _) =
+ invoke_generation thy (algebra, funcgr) ensure_value t;
val vs'' = map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v)) vs';
- in evaluator naming program (((vs'', (vs', ty')), fs'), t') deps end;
+ in evaluator naming program ((vs'', (vs', ty')), t') deps end;
fun eval_conv thy prep_sort = Code_Wellsorted.eval_conv thy prep_sort o base_evaluator thy;
fun eval thy prep_sort postproc = Code_Wellsorted.eval thy prep_sort postproc o base_evaluator thy;
--- a/src/Tools/code/code_wellsorted.ML Fri May 08 08:06:43 2009 +0200
+++ b/src/Tools/code/code_wellsorted.ML Fri May 08 08:07:05 2009 +0200
@@ -293,19 +293,22 @@
fun obtain thy cs ts = apsnd snd
(Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts));
-fun prepare_sorts prep_sort (Const (c, ty)) = Const (c, map_type_tfree
- (fn (v, sort) => TFree (v, prep_sort sort)) ty)
+fun prepare_sorts_typ prep_sort
+ = map_type_tfree (fn (v, sort) => TFree (v, prep_sort sort));
+
+fun prepare_sorts prep_sort (Const (c, ty)) =
+ Const (c, prepare_sorts_typ prep_sort ty)
| prepare_sorts prep_sort (t1 $ t2) =
prepare_sorts prep_sort t1 $ prepare_sorts prep_sort t2
| prepare_sorts prep_sort (Abs (v, ty, t)) =
- Abs (v, Type.strip_sorts ty, prepare_sorts prep_sort t)
- | prepare_sorts _ (Term.Free (v, ty)) = Term.Free (v, Type.strip_sorts ty)
+ Abs (v, prepare_sorts_typ prep_sort ty, prepare_sorts prep_sort t)
| prepare_sorts _ (t as Bound _) = t;
fun gen_eval thy cterm_of conclude_evaluation prep_sort evaluator proto_ct =
let
+ val pp = Syntax.pp_global thy;
val ct = cterm_of proto_ct;
- val _ = (Term.map_types Type.no_tvars o Sign.no_vars (Syntax.pp_global thy))
+ val _ = (Sign.no_frees pp o map_types (K dummyT) o Sign.no_vars pp)
(Thm.term_of ct);
val thm = Code.preprocess_conv thy ct;
val ct' = Thm.rhs_of thm;
@@ -313,6 +316,7 @@
val vs = Term.add_tfrees t' [];
val consts = fold_aterms
(fn Const (c, _) => insert (op =) c | _ => I) t' [];
+
val t'' = prepare_sorts prep_sort t';
val (algebra', eqngr') = obtain thy consts [t''];
in conclude_evaluation (evaluator algebra' eqngr' vs t'' ct') thm end;
--- a/src/Tools/nbe.ML Fri May 08 08:06:43 2009 +0200
+++ b/src/Tools/nbe.ML Fri May 08 08:07:05 2009 +0200
@@ -11,7 +11,6 @@
datatype Univ =
Const of int * Univ list (*named (uninterpreted) constants*)
- | Free of string * Univ list (*free (uninterpreted) variables*)
| DFree of string * int (*free (uninterpreted) dictionary parameters*)
| BVar of int * Univ list
| Abs of (int * (Univ list -> Univ)) * Univ list
@@ -57,14 +56,12 @@
datatype Univ =
Const of int * Univ list (*named (uninterpreted) constants*)
- | Free of string * Univ list (*free variables*)
| DFree of string * int (*free (uninterpreted) dictionary parameters*)
| BVar of int * Univ list (*bound variables, named*)
| Abs of (int * (Univ list -> Univ)) * Univ list
(*abstractions as closures*);
fun same (Const (k, xs)) (Const (l, ys)) = k = l andalso sames xs ys
- | same (Free (s, xs)) (Free (t, ys)) = s = t andalso sames xs ys
| same (DFree (s, k)) (DFree (t, l)) = s = t andalso k = l
| same (BVar (k, xs)) (BVar (l, ys)) = k = l andalso sames xs ys
| same _ _ = false
@@ -80,7 +77,6 @@
| GREATER => Abs ((k, f), ys @ xs) (*note: reverse convention also for apps!*)
end
| apps (Const (name, xs)) ys = Const (name, ys @ xs)
- | apps (Free (name, xs)) ys = Free (name, ys @ xs)
| apps (BVar (n, xs)) ys = BVar (n, ys @ xs);
@@ -352,14 +348,12 @@
fun eval_term ctxt gr deps (vs : (string * sort) list, t) =
let
- val frees = Code_Thingol.fold_unbound_varnames (insert (op =)) t []
- val frees' = map (fn v => Free (v, [])) frees;
val dict_frees = maps (fn (v, sort) => map_index (curry DFree v o fst) sort) vs;
in
- ("", (vs, [(map IVar frees, t)]))
+ ("", (vs, [([], t)]))
|> singleton (compile_eqnss ctxt gr deps)
|> snd
- |> (fn t => apps t (rev (dict_frees @ frees')))
+ |> (fn t => apps t (rev dict_frees))
end;
(* reification *)
@@ -399,8 +393,6 @@
val T' = map_type_tfree (fn (v, _) => TypeInfer.param typidx (v, [])) T;
val typidx' = typidx + 1;
in of_apps bounds (Term.Const (c, T'), ts') typidx' end
- | of_univ bounds (Free (name, ts)) typidx =
- of_apps bounds (Term.Free (name, dummyT), ts) typidx
| of_univ bounds (BVar (n, ts)) typidx =
of_apps bounds (Bound (bounds - n - 1), ts) typidx
| of_univ bounds (t as Abs _) typidx =
@@ -440,15 +432,12 @@
(* evaluation with type reconstruction *)
-fun normalize thy naming program (((vs0, (vs, ty)), fs), t) deps =
+fun normalize thy naming program ((vs0, (vs, ty)), t) deps =
let
fun subst_const f = map_aterms (fn t as Term.Const (c, ty) => Term.Const (f c, ty)
| t => t);
val resubst_triv_consts = subst_const (Code_Unit.resubst_alias thy);
val ty' = typ_of_itype program vs0 ty;
- val fs' = (map o apsnd) (typ_of_itype program vs0) fs;
- val type_frees = Term.map_aterms (fn (t as Term.Free (s, _)) =>
- Term.Free (s, (the o AList.lookup (op =) fs') s) | t => t);
fun type_infer t =
singleton (TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
(try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0)
@@ -461,8 +450,6 @@
compile_eval thy naming program (vs, t) deps
|> tracing (fn t => "Normalized:\n" ^ string_of_term t)
|> resubst_triv_consts
- |> type_frees
- |> tracing (fn t => "Vars typed:\n" ^ string_of_term t)
|> type_infer
|> tracing (fn t => "Types inferred:\n" ^ string_of_term t)
|> check_tvars
@@ -482,18 +469,41 @@
in Thm.mk_binop eq lhs rhs end;
val (_, raw_norm_oracle) = Context.>>> (Context.map_theory_result
- (Thm.add_oracle (Binding.name "norm", fn (thy, naming, program, vsp_ty_fs_t, deps, ct) =>
- mk_equals thy ct (normalize thy naming program vsp_ty_fs_t deps))));
+ (Thm.add_oracle (Binding.name "norm", fn (thy, naming, program, vsp_ty_t, deps, ct) =>
+ mk_equals thy ct (normalize thy naming program vsp_ty_t deps))));
+
+fun norm_oracle thy naming program vsp_ty_t deps ct =
+ raw_norm_oracle (thy, naming, program, vsp_ty_t, deps, ct);
-fun norm_oracle thy naming program vsp_ty_fs_t deps ct =
- raw_norm_oracle (thy, naming, program, vsp_ty_fs_t, deps, ct);
+fun no_frees_conv conv ct =
+ let
+ val frees = Thm.add_cterm_frees ct [];
+ fun apply_beta free thm = Thm.combination thm (Thm.reflexive free)
+ |> Conv.fconv_rule (Conv.arg_conv (Conv.try_conv (Thm.beta_conversion false)))
+ |> Conv.fconv_rule (Conv.arg1_conv (Thm.beta_conversion false));
+ in
+ ct
+ |> fold_rev Thm.cabs frees
+ |> conv
+ |> fold apply_beta frees
+ end;
-fun norm_conv ct =
+fun no_frees_rew rew t =
+ let
+ val frees = map Free (Term.add_frees t []);
+ in
+ t
+ |> fold_rev lambda frees
+ |> rew
+ |> (fn t' => Term.betapplys (t', frees))
+ end;
+
+val norm_conv = no_frees_conv (fn ct =>
let
val thy = Thm.theory_of_cterm ct;
- in Code_Thingol.eval_conv thy (add_triv_classes thy) (norm_oracle thy) ct end;
+ in Code_Thingol.eval_conv thy (add_triv_classes thy) (norm_oracle thy) ct end);
-fun norm thy = Code_Thingol.eval thy (add_triv_classes thy) I (normalize thy);
+fun norm thy = no_frees_rew (Code_Thingol.eval thy (add_triv_classes thy) I (normalize thy));
(* evaluation command *)