--- a/src/FOL/simpdata.ML Tue Aug 06 11:20:47 2002 +0200
+++ b/src/FOL/simpdata.ML Tue Aug 06 11:22:05 2002 +0200
@@ -266,20 +266,13 @@
end;
-local
-
-val ex_pattern =
- read_cterm (Theory.sign_of (the_context ())) ("EX x. P(x)", FOLogic.oT)
+val defEX_regroup =
+ Simplifier.simproc (Theory.sign_of (the_context ()))
+ "defined EX" ["EX x. P(x)"] Quantifier1.rearrange_ex;
-val all_pattern =
- read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x)", FOLogic.oT)
-
-in
-val defEX_regroup =
- mk_simproc "defined EX" [ex_pattern] Quantifier1.rearrange_ex;
val defALL_regroup =
- mk_simproc "defined ALL" [all_pattern] Quantifier1.rearrange_all;
-end;
+ Simplifier.simproc (Theory.sign_of (the_context ()))
+ "defined ALL" ["ALL x. P(x)"] Quantifier1.rearrange_all;
(*** Case splitting ***)
--- a/src/HOL/Bali/Basis.thy Tue Aug 06 11:20:47 2002 +0200
+++ b/src/HOL/Bali/Basis.thy Tue Aug 06 11:22:05 2002 +0200
@@ -19,11 +19,9 @@
declare same_fstI [intro!] (*### TO HOL/Wellfounded_Relations *)
-(* ###TO HOL/???.ML?? *)
ML {*
-fun make_simproc name pat pred thm = Simplifier.mk_simproc name
- [Thm.read_cterm (Thm.sign_of_thm thm) (pat, HOLogic.typeT)]
- (K (K (fn s => if pred s then None else Some (standard (mk_meta_eq thm)))))
+fun cond_simproc name pat pred thm = Simplifier.simproc (Thm.sign_of_thm thm) name [pat]
+ (fn _ => fn _ => fn t => if pred t then None else Some (mk_meta_eq thm));
*}
declare split_if_asm [split] option.split [split] option.split_asm [split]
--- a/src/HOL/Bali/Eval.thy Tue Aug 06 11:20:47 2002 +0200
+++ b/src/HOL/Bali/Eval.thy Tue Aug 06 11:22:05 2002 +0200
@@ -894,7 +894,7 @@
fun pred (_ $ (Const ("Pair",_) $ _ $
(Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ ))) $ _ ) = is_Inj x
in
- make_simproc name lhs pred (thm name)
+ cond_simproc name lhs pred (thm name)
end
val eval_expr_proc =eval_fun "expr" "In1l" "\<exists>v. w=In1 v \<and> G\<turnstile>s \<midarrow>t-\<succ>v \<rightarrow> s'"
@@ -989,7 +989,7 @@
(Const ("Pair", _) $ x $ _) $ _ ) $ _)) = is_None x
in
val eval_no_abrupt_proc =
- make_simproc "eval_no_abrupt" "G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')" pred
+ cond_simproc "eval_no_abrupt" "G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')" pred
(thm "eval_no_abrupt")
end;
Addsimprocs [eval_no_abrupt_proc]
@@ -1017,7 +1017,7 @@
x))) $ _ ) = is_Some x
in
val eval_abrupt_proc =
- make_simproc "eval_abrupt"
+ cond_simproc "eval_abrupt"
"G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')" pred (thm "eval_abrupt")
end;
Addsimprocs [eval_abrupt_proc]
--- a/src/HOL/Bali/Evaln.thy Tue Aug 06 11:20:47 2002 +0200
+++ b/src/HOL/Bali/Evaln.thy Tue Aug 06 11:22:05 2002 +0200
@@ -260,7 +260,7 @@
fun pred (_ $ (Const ("Pair",_) $ _ $ (Const ("Pair", _) $ _ $
(Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ )))) $ _ ) = is_Inj x
in
- make_simproc name lhs pred (thm name)
+ cond_simproc name lhs pred (thm name)
end;
val evaln_expr_proc = enf "expr" "In1l" "\<exists>v. w=In1 v \<and> G\<turnstile>s \<midarrow>t-\<succ>v \<midarrow>n\<rightarrow> s'";
@@ -350,7 +350,7 @@
(Const ("Pair", _) $ _ $ x)))) $ _ ) = is_Some x
in
val evaln_abrupt_proc =
- make_simproc "evaln_abrupt" "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')" pred (thm "evaln_abrupt")
+ cond_simproc "evaln_abrupt" "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')" pred (thm "evaln_abrupt")
end;
Addsimprocs [evaln_abrupt_proc]
*}
--- a/src/HOL/Bali/WellType.thy Tue Aug 06 11:20:47 2002 +0200
+++ b/src/HOL/Bali/WellType.thy Tue Aug 06 11:22:05 2002 +0200
@@ -620,7 +620,7 @@
_ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
x))) $ _ )) = is_Inj x
in
- make_simproc name lhs pred (thm name)
+ cond_simproc name lhs pred (thm name)
end
val wt_expr_proc = wt_fun "wt_expr_eq" "In1l" "\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>-T"
--- a/src/HOL/Fun.ML Tue Aug 06 11:20:47 2002 +0200
+++ b/src/HOL/Fun.ML Tue Aug 06 11:22:05 2002 +0200
@@ -372,10 +372,10 @@
simp_tac ss 1]
fun mk_eq_cterm sg T l r = Thm.cterm_of sg (equals T $ l $ r)
in
- val fun_upd2_simproc = Simplifier.mk_simproc "fun_upd2"
- [HOLogic.read_cterm (sign_of (the_context ())) "f(v := w, x := y)"]
- (fn sg => (K (fn t => case find_double t of (T,None)=> None | (T,Some rhs)=>
- Some (prove_goalw_cterm [] (mk_eq_cterm sg T t rhs) fun_upd_prover))))
+ val fun_upd2_simproc =
+ Simplifier.simproc (Theory.sign_of (the_context ())) "fun_upd2" ["f(v := w, x := y)"]
+ (fn sg => fn _ => fn t => case find_double t of (T, None) => None | (T, Some rhs) =>
+ Some (prove_goalw_cterm [] (mk_eq_cterm sg T t rhs) fun_upd_prover));
end;
Addsimprocs[fun_upd2_simproc];
--- a/src/HOL/Hyperreal/HyperArith0.ML Tue Aug 06 11:20:47 2002 +0200
+++ b/src/HOL/Hyperreal/HyperArith0.ML Tue Aug 06 11:22:05 2002 +0200
@@ -9,59 +9,59 @@
*)
Goal "x - - y = x + (y::hypreal)";
-by (Simp_tac 1);
+by (Simp_tac 1);
qed "hypreal_diff_minus_eq";
Addsimps [hypreal_diff_minus_eq];
Goal "((x * y = 0) = (x = 0 | y = (0::hypreal)))";
-by Auto_tac;
+by Auto_tac;
by (cut_inst_tac [("x","x"),("y","y")] hypreal_mult_zero_disj 1);
-by Auto_tac;
+by Auto_tac;
qed "hypreal_mult_is_0";
AddIffs [hypreal_mult_is_0];
(** Division and inverse **)
Goal "0/x = (0::hypreal)";
-by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1);
+by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1);
qed "hypreal_0_divide";
Addsimps [hypreal_0_divide];
Goal "((0::hypreal) < inverse x) = (0 < x)";
by (case_tac "x=0" 1);
-by (asm_simp_tac (HOL_ss addsimps [HYPREAL_INVERSE_ZERO]) 1);
-by (auto_tac (claset() addDs [hypreal_inverse_less_0],
- simpset() addsimps [linorder_neq_iff,
- hypreal_inverse_gt_0]));
+by (asm_simp_tac (HOL_ss addsimps [HYPREAL_INVERSE_ZERO]) 1);
+by (auto_tac (claset() addDs [hypreal_inverse_less_0],
+ simpset() addsimps [linorder_neq_iff,
+ hypreal_inverse_gt_0]));
qed "hypreal_0_less_inverse_iff";
Addsimps [hypreal_0_less_inverse_iff];
Goal "(inverse x < (0::hypreal)) = (x < 0)";
by (case_tac "x=0" 1);
-by (asm_simp_tac (HOL_ss addsimps [HYPREAL_INVERSE_ZERO]) 1);
-by (auto_tac (claset() addDs [hypreal_inverse_less_0],
- simpset() addsimps [linorder_neq_iff,
- hypreal_inverse_gt_0]));
+by (asm_simp_tac (HOL_ss addsimps [HYPREAL_INVERSE_ZERO]) 1);
+by (auto_tac (claset() addDs [hypreal_inverse_less_0],
+ simpset() addsimps [linorder_neq_iff,
+ hypreal_inverse_gt_0]));
qed "hypreal_inverse_less_0_iff";
Addsimps [hypreal_inverse_less_0_iff];
Goal "((0::hypreal) <= inverse x) = (0 <= x)";
-by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
+by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
qed "hypreal_0_le_inverse_iff";
Addsimps [hypreal_0_le_inverse_iff];
Goal "(inverse x <= (0::hypreal)) = (x <= 0)";
-by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
+by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
qed "hypreal_inverse_le_0_iff";
Addsimps [hypreal_inverse_le_0_iff];
Goalw [hypreal_divide_def] "x/(0::hypreal) = 0";
-by (stac (HYPREAL_INVERSE_ZERO) 1);
-by (Simp_tac 1);
+by (stac (HYPREAL_INVERSE_ZERO) 1);
+by (Simp_tac 1);
qed "HYPREAL_DIVIDE_ZERO";
Goal "inverse (x::hypreal) = 1/x";
-by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1);
+by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1);
qed "hypreal_inverse_eq_divide";
Goal "((0::hypreal) < x/y) = (0 < x & 0 < y | x < 0 & y < 0)";
@@ -76,34 +76,34 @@
Goal "((0::hypreal) <= x/y) = ((x <= 0 | 0 <= y) & (0 <= x | y <= 0))";
by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_0_le_mult_iff]) 1);
-by Auto_tac;
+by Auto_tac;
qed "hypreal_0_le_divide_iff";
Addsimps [inst "x" "number_of ?w" hypreal_0_le_divide_iff];
Goal "(x/y <= (0::hypreal)) = ((x <= 0 | y <= 0) & (0 <= x | 0 <= y))";
-by (simp_tac (simpset() addsimps [hypreal_divide_def,
+by (simp_tac (simpset() addsimps [hypreal_divide_def,
hypreal_mult_le_0_iff]) 1);
-by Auto_tac;
+by Auto_tac;
qed "hypreal_divide_le_0_iff";
Addsimps [inst "x" "number_of ?w" hypreal_divide_le_0_iff];
Goal "(inverse(x::hypreal) = 0) = (x = 0)";
-by (auto_tac (claset(),
- simpset() addsimps [HYPREAL_INVERSE_ZERO]));
-by (rtac ccontr 1);
-by (blast_tac (claset() addDs [hypreal_inverse_not_zero]) 1);
+by (auto_tac (claset(),
+ simpset() addsimps [HYPREAL_INVERSE_ZERO]));
+by (rtac ccontr 1);
+by (blast_tac (claset() addDs [hypreal_inverse_not_zero]) 1);
qed "hypreal_inverse_zero_iff";
Addsimps [hypreal_inverse_zero_iff];
Goal "(x/y = 0) = (x=0 | y=(0::hypreal))";
-by (auto_tac (claset(), simpset() addsimps [hypreal_divide_def]));
+by (auto_tac (claset(), simpset() addsimps [hypreal_divide_def]));
qed "hypreal_divide_eq_0_iff";
Addsimps [hypreal_divide_eq_0_iff];
Goal "h ~= (0::hypreal) ==> h/h = 1";
-by (asm_simp_tac
+by (asm_simp_tac
(simpset() addsimps [hypreal_divide_def, hypreal_mult_inverse_left]) 1);
-qed "hypreal_divide_self_eq";
+qed "hypreal_divide_self_eq";
Addsimps [hypreal_divide_self_eq];
@@ -121,23 +121,23 @@
Goal "[| i<j; k < (0::hypreal) |] ==> j*k < i*k";
by (rtac (hypreal_minus_less_minus RS iffD1) 1);
-by (auto_tac (claset(),
+by (auto_tac (claset(),
simpset() delsimps [hypreal_minus_mult_eq2 RS sym]
addsimps [hypreal_minus_mult_eq2,
- hypreal_mult_less_mono1]));
+ hypreal_mult_less_mono1]));
qed "hypreal_mult_less_mono1_neg";
Goal "[| i<j; k < (0::hypreal) |] ==> k*j < k*i";
by (rtac (hypreal_minus_less_minus RS iffD1) 1);
-by (auto_tac (claset(),
+by (auto_tac (claset(),
simpset() delsimps [hypreal_minus_mult_eq1 RS sym]
addsimps [hypreal_minus_mult_eq1,
hypreal_mult_less_mono2]));
qed "hypreal_mult_less_mono2_neg";
Goal "[| i <= j; k <= (0::hypreal) |] ==> j*k <= i*k";
-by (auto_tac (claset(),
- simpset() addsimps [order_le_less, hypreal_mult_less_mono1_neg]));
+by (auto_tac (claset(),
+ simpset() addsimps [order_le_less, hypreal_mult_less_mono1_neg]));
qed "hypreal_mult_le_mono1_neg";
Goal "[| i <= j; k <= (0::hypreal) |] ==> k*j <= k*i";
@@ -147,56 +147,56 @@
Goal "(m*k < n*k) = (((0::hypreal) < k & m<n) | (k < 0 & n<m))";
by (case_tac "k = (0::hypreal)" 1);
-by (auto_tac (claset(),
- simpset() addsimps [linorder_neq_iff,
- hypreal_mult_less_mono1, hypreal_mult_less_mono1_neg]));
-by (auto_tac (claset(),
+by (auto_tac (claset(),
+ simpset() addsimps [linorder_neq_iff,
+ hypreal_mult_less_mono1, hypreal_mult_less_mono1_neg]));
+by (auto_tac (claset(),
simpset() addsimps [linorder_not_less,
- inst "y1" "m*k" (linorder_not_le RS sym),
+ inst "y1" "m*k" (linorder_not_le RS sym),
inst "y1" "m" (linorder_not_le RS sym)]));
by (TRYALL (etac notE));
-by (auto_tac (claset(),
+by (auto_tac (claset(),
simpset() addsimps [order_less_imp_le, hypreal_mult_le_mono1,
- hypreal_mult_le_mono1_neg]));
+ hypreal_mult_le_mono1_neg]));
qed "hypreal_mult_less_cancel2";
Goal "(m*k <= n*k) = (((0::hypreal) < k --> m<=n) & (k < 0 --> n<=m))";
-by (simp_tac (simpset() addsimps [linorder_not_less RS sym,
+by (simp_tac (simpset() addsimps [linorder_not_less RS sym,
hypreal_mult_less_cancel2]) 1);
qed "hypreal_mult_le_cancel2";
Goal "(k*m < k*n) = (((0::hypreal) < k & m<n) | (k < 0 & n<m))";
-by (simp_tac (simpset() addsimps [inst "z" "k" hypreal_mult_commute,
+by (simp_tac (simpset() addsimps [inst "z" "k" hypreal_mult_commute,
hypreal_mult_less_cancel2]) 1);
qed "hypreal_mult_less_cancel1";
Goal "!!k::hypreal. (k*m <= k*n) = ((0 < k --> m<=n) & (k < 0 --> n<=m))";
-by (simp_tac (simpset() addsimps [linorder_not_less RS sym,
+by (simp_tac (simpset() addsimps [linorder_not_less RS sym,
hypreal_mult_less_cancel1]) 1);
qed "hypreal_mult_le_cancel1";
Goal "!!k::hypreal. (k*m = k*n) = (k = 0 | m=n)";
by (case_tac "k=0" 1);
-by (auto_tac (claset(), simpset() addsimps [hypreal_mult_left_cancel]));
+by (auto_tac (claset(), simpset() addsimps [hypreal_mult_left_cancel]));
qed "hypreal_mult_eq_cancel1";
Goal "!!k::hypreal. (m*k = n*k) = (k = 0 | m=n)";
by (case_tac "k=0" 1);
-by (auto_tac (claset(), simpset() addsimps [hypreal_mult_right_cancel]));
+by (auto_tac (claset(), simpset() addsimps [hypreal_mult_right_cancel]));
qed "hypreal_mult_eq_cancel2";
Goal "!!k::hypreal. k~=0 ==> (k*m) / (k*n) = (m/n)";
by (asm_simp_tac
- (simpset() addsimps [hypreal_divide_def, hypreal_inverse_distrib]) 1);
+ (simpset() addsimps [hypreal_divide_def, hypreal_inverse_distrib]) 1);
by (subgoal_tac "k * m * (inverse k * inverse n) = \
\ (k * inverse k) * (m * inverse n)" 1);
-by (asm_full_simp_tac (simpset() addsimps []) 1);
-by (asm_full_simp_tac (HOL_ss addsimps hypreal_mult_ac) 1);
+by (asm_full_simp_tac (simpset() addsimps []) 1);
+by (asm_full_simp_tac (HOL_ss addsimps hypreal_mult_ac) 1);
qed "hypreal_mult_div_cancel1";
(*For ExtractCommonTerm*)
Goal "(k*m) / (k*n) = (if k = (0::hypreal) then 0 else m/n)";
-by (simp_tac (simpset() addsimps [hypreal_mult_div_cancel1]) 1);
+by (simp_tac (simpset() addsimps [hypreal_mult_div_cancel1]) 1);
qed "hypreal_mult_div_cancel_disj";
@@ -204,19 +204,19 @@
open Hyperreal_Numeral_Simprocs
in
-val rel_hypreal_number_of = [eq_hypreal_number_of, less_hypreal_number_of,
+val rel_hypreal_number_of = [eq_hypreal_number_of, less_hypreal_number_of,
le_hypreal_number_of_eq_not_less];
structure CancelNumeralFactorCommon =
struct
- val mk_coeff = mk_coeff
- val dest_coeff = dest_coeff 1
+ val mk_coeff = mk_coeff
+ val dest_coeff = dest_coeff 1
val trans_tac = Real_Numeral_Simprocs.trans_tac
- val norm_tac =
+ val norm_tac =
ALLGOALS (simp_tac (HOL_ss addsimps hypreal_minus_from_mult_simps @ mult_1s))
THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hypreal_mult_minus_simps))
THEN ALLGOALS (simp_tac (HOL_ss addsimps hypreal_mult_ac))
- val numeral_simp_tac =
+ val numeral_simp_tac =
ALLGOALS (simp_tac (HOL_ss addsimps rel_hypreal_number_of@bin_simps))
val simplify_meta_eq = simplify_meta_eq
end
@@ -261,26 +261,26 @@
val neg_exchanges = true
)
-val hypreal_cancel_numeral_factors_relations =
+val hypreal_cancel_numeral_factors_relations =
map prep_simproc
[("hyprealeq_cancel_numeral_factor",
- prep_pats ["(l::hypreal) * m = n", "(l::hypreal) = m * n"],
+ ["(l::hypreal) * m = n", "(l::hypreal) = m * n"],
EqCancelNumeralFactor.proc),
- ("hyprealless_cancel_numeral_factor",
- prep_pats ["(l::hypreal) * m < n", "(l::hypreal) < m * n"],
+ ("hyprealless_cancel_numeral_factor",
+ ["(l::hypreal) * m < n", "(l::hypreal) < m * n"],
LessCancelNumeralFactor.proc),
- ("hyprealle_cancel_numeral_factor",
- prep_pats ["(l::hypreal) * m <= n", "(l::hypreal) <= m * n"],
+ ("hyprealle_cancel_numeral_factor",
+ ["(l::hypreal) * m <= n", "(l::hypreal) <= m * n"],
LeCancelNumeralFactor.proc)];
val hypreal_cancel_numeral_factors_divide = prep_simproc
- ("hyprealdiv_cancel_numeral_factor",
- prep_pats ["((l::hypreal) * m) / n", "(l::hypreal) / (m * n)",
- "((number_of v)::hypreal) / (number_of w)"],
- DivCancelNumeralFactor.proc);
+ ("hyprealdiv_cancel_numeral_factor",
+ ["((l::hypreal) * m) / n", "(l::hypreal) / (m * n)",
+ "((number_of v)::hypreal) / (number_of w)"],
+ DivCancelNumeralFactor.proc);
-val hypreal_cancel_numeral_factors =
- hypreal_cancel_numeral_factors_relations @
+val hypreal_cancel_numeral_factors =
+ hypreal_cancel_numeral_factors_relations @
[hypreal_cancel_numeral_factors_divide];
end;
@@ -292,7 +292,7 @@
print_depth 22;
set timing;
set trace_simp;
-fun test s = (Goal s; by (Simp_tac 1));
+fun test s = (Goal s; by (Simp_tac 1));
test "0 <= (y::hypreal) * -2";
test "9*x = 12 * (y::hypreal)";
@@ -333,11 +333,11 @@
structure CancelFactorCommon =
struct
- val mk_sum = long_mk_prod
- val dest_sum = dest_prod
- val mk_coeff = mk_coeff
- val dest_coeff = dest_coeff
- val find_first = find_first []
+ val mk_sum = long_mk_prod
+ val dest_sum = dest_prod
+ val mk_coeff = mk_coeff
+ val dest_coeff = dest_coeff
+ val find_first = find_first []
val trans_tac = Real_Numeral_Simprocs.trans_tac
val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@hypreal_mult_ac))
end;
@@ -361,13 +361,11 @@
val simplify_meta_eq = cancel_simplify_meta_eq hypreal_mult_div_cancel_disj
);
-val hypreal_cancel_factor =
+val hypreal_cancel_factor =
map prep_simproc
- [("hypreal_eq_cancel_factor",
- prep_pats ["(l::hypreal) * m = n", "(l::hypreal) = m * n"],
+ [("hypreal_eq_cancel_factor", ["(l::hypreal) * m = n", "(l::hypreal) = m * n"],
EqCancelFactor.proc),
- ("hypreal_divide_cancel_factor",
- prep_pats ["((l::hypreal) * m) / n", "(l::hypreal) / (m * n)"],
+ ("hypreal_divide_cancel_factor", ["((l::hypreal) * m) / n", "(l::hypreal) / (m * n)"],
DivideCancelFactor.proc)];
end;
@@ -379,16 +377,16 @@
print_depth 22;
set timing;
set trace_simp;
-fun test s = (Goal s; by (Asm_simp_tac 1));
+fun test s = (Goal s; by (Asm_simp_tac 1));
test "x*k = k*(y::hypreal)";
-test "k = k*(y::hypreal)";
+test "k = k*(y::hypreal)";
test "a*(b*c) = (b::hypreal)";
test "a*(b*c) = d*(b::hypreal)*(x*a)";
test "(x*k) / (k*(y::hypreal)) = (uu::hypreal)";
-test "(k) / (k*(y::hypreal)) = (uu::hypreal)";
+test "(k) / (k*(y::hypreal)) = (uu::hypreal)";
test "(a*(b*c)) / ((b::hypreal)) = (uu::hypreal)";
test "(a*(b*c)) / (d*(b::hypreal)*(x*a)) = (uu::hypreal)";
@@ -401,106 +399,106 @@
Goal "0<z ==> ((x::hypreal) <= y/z) = (x*z <= y)";
by (subgoal_tac "(x*z <= y) = (x*z <= (y/z)*z)" 1);
-by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
+by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
by (etac ssubst 1);
-by (stac hypreal_mult_le_cancel2 1);
-by (Asm_simp_tac 1);
+by (stac hypreal_mult_le_cancel2 1);
+by (Asm_simp_tac 1);
qed "pos_hypreal_le_divide_eq";
Addsimps [inst "z" "number_of ?w" pos_hypreal_le_divide_eq];
Goal "z<0 ==> ((x::hypreal) <= y/z) = (y <= x*z)";
by (subgoal_tac "(y <= x*z) = ((y/z)*z <= x*z)" 1);
-by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
+by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
by (etac ssubst 1);
-by (stac hypreal_mult_le_cancel2 1);
-by (Asm_simp_tac 1);
+by (stac hypreal_mult_le_cancel2 1);
+by (Asm_simp_tac 1);
qed "neg_hypreal_le_divide_eq";
Addsimps [inst "z" "number_of ?w" neg_hypreal_le_divide_eq];
Goal "0<z ==> (y/z <= (x::hypreal)) = (y <= x*z)";
by (subgoal_tac "(y <= x*z) = ((y/z)*z <= x*z)" 1);
-by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
+by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
by (etac ssubst 1);
-by (stac hypreal_mult_le_cancel2 1);
-by (Asm_simp_tac 1);
+by (stac hypreal_mult_le_cancel2 1);
+by (Asm_simp_tac 1);
qed "pos_hypreal_divide_le_eq";
Addsimps [inst "z" "number_of ?w" pos_hypreal_divide_le_eq];
Goal "z<0 ==> (y/z <= (x::hypreal)) = (x*z <= y)";
by (subgoal_tac "(x*z <= y) = (x*z <= (y/z)*z)" 1);
-by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
+by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
by (etac ssubst 1);
-by (stac hypreal_mult_le_cancel2 1);
-by (Asm_simp_tac 1);
+by (stac hypreal_mult_le_cancel2 1);
+by (Asm_simp_tac 1);
qed "neg_hypreal_divide_le_eq";
Addsimps [inst "z" "number_of ?w" neg_hypreal_divide_le_eq];
Goal "0<z ==> ((x::hypreal) < y/z) = (x*z < y)";
by (subgoal_tac "(x*z < y) = (x*z < (y/z)*z)" 1);
-by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
+by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
by (etac ssubst 1);
-by (stac hypreal_mult_less_cancel2 1);
-by (Asm_simp_tac 1);
+by (stac hypreal_mult_less_cancel2 1);
+by (Asm_simp_tac 1);
qed "pos_hypreal_less_divide_eq";
Addsimps [inst "z" "number_of ?w" pos_hypreal_less_divide_eq];
Goal "z<0 ==> ((x::hypreal) < y/z) = (y < x*z)";
by (subgoal_tac "(y < x*z) = ((y/z)*z < x*z)" 1);
-by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
+by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
by (etac ssubst 1);
-by (stac hypreal_mult_less_cancel2 1);
-by (Asm_simp_tac 1);
+by (stac hypreal_mult_less_cancel2 1);
+by (Asm_simp_tac 1);
qed "neg_hypreal_less_divide_eq";
Addsimps [inst "z" "number_of ?w" neg_hypreal_less_divide_eq];
Goal "0<z ==> (y/z < (x::hypreal)) = (y < x*z)";
by (subgoal_tac "(y < x*z) = ((y/z)*z < x*z)" 1);
-by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
+by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
by (etac ssubst 1);
-by (stac hypreal_mult_less_cancel2 1);
-by (Asm_simp_tac 1);
+by (stac hypreal_mult_less_cancel2 1);
+by (Asm_simp_tac 1);
qed "pos_hypreal_divide_less_eq";
Addsimps [inst "z" "number_of ?w" pos_hypreal_divide_less_eq];
Goal "z<0 ==> (y/z < (x::hypreal)) = (x*z < y)";
by (subgoal_tac "(x*z < y) = (x*z < (y/z)*z)" 1);
-by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
+by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
by (etac ssubst 1);
-by (stac hypreal_mult_less_cancel2 1);
-by (Asm_simp_tac 1);
+by (stac hypreal_mult_less_cancel2 1);
+by (Asm_simp_tac 1);
qed "neg_hypreal_divide_less_eq";
Addsimps [inst "z" "number_of ?w" neg_hypreal_divide_less_eq];
Goal "z~=0 ==> ((x::hypreal) = y/z) = (x*z = y)";
by (subgoal_tac "(x*z = y) = (x*z = (y/z)*z)" 1);
-by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
+by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
by (etac ssubst 1);
-by (stac hypreal_mult_eq_cancel2 1);
-by (Asm_simp_tac 1);
+by (stac hypreal_mult_eq_cancel2 1);
+by (Asm_simp_tac 1);
qed "hypreal_eq_divide_eq";
Addsimps [inst "z" "number_of ?w" hypreal_eq_divide_eq];
Goal "z~=0 ==> (y/z = (x::hypreal)) = (y = x*z)";
by (subgoal_tac "(y = x*z) = ((y/z)*z = x*z)" 1);
-by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
+by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2);
by (etac ssubst 1);
-by (stac hypreal_mult_eq_cancel2 1);
-by (Asm_simp_tac 1);
+by (stac hypreal_mult_eq_cancel2 1);
+by (Asm_simp_tac 1);
qed "hypreal_divide_eq_eq";
Addsimps [inst "z" "number_of ?w" hypreal_divide_eq_eq];
Goal "(m/k = n/k) = (k = 0 | m = (n::hypreal))";
by (case_tac "k=0" 1);
-by (asm_simp_tac (simpset() addsimps [HYPREAL_DIVIDE_ZERO]) 1);
-by (asm_simp_tac (simpset() addsimps [hypreal_divide_eq_eq, hypreal_eq_divide_eq,
- hypreal_mult_eq_cancel2]) 1);
+by (asm_simp_tac (simpset() addsimps [HYPREAL_DIVIDE_ZERO]) 1);
+by (asm_simp_tac (simpset() addsimps [hypreal_divide_eq_eq, hypreal_eq_divide_eq,
+ hypreal_mult_eq_cancel2]) 1);
qed "hypreal_divide_eq_cancel2";
Goal "(k/m = k/n) = (k = 0 | m = (n::hypreal))";
by (case_tac "m=0 | n = 0" 1);
-by (auto_tac (claset(),
- simpset() addsimps [HYPREAL_DIVIDE_ZERO, hypreal_divide_eq_eq,
- hypreal_eq_divide_eq, hypreal_mult_eq_cancel1]));
+by (auto_tac (claset(),
+ simpset() addsimps [HYPREAL_DIVIDE_ZERO, hypreal_divide_eq_eq,
+ hypreal_eq_divide_eq, hypreal_mult_eq_cancel1]));
qed "hypreal_divide_eq_cancel1";
Goal "[| 0 < r; 0 < x|] ==> (inverse x < inverse (r::hypreal)) = (r < x)";
@@ -508,35 +506,35 @@
by (res_inst_tac [("t","r")] (hypreal_inverse_inverse RS subst) 1);
by (res_inst_tac [("t","x")] (hypreal_inverse_inverse RS subst) 1);
by (auto_tac (claset() addIs [hypreal_inverse_less_swap],
- simpset() delsimps [hypreal_inverse_inverse]
- addsimps [hypreal_inverse_gt_0]));
+ simpset() delsimps [hypreal_inverse_inverse]
+ addsimps [hypreal_inverse_gt_0]));
qed "hypreal_inverse_less_iff";
Goal "[| 0 < r; 0 < x|] ==> (inverse x <= inverse r) = (r <= (x::hypreal))";
-by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
- hypreal_inverse_less_iff]) 1);
+by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
+ hypreal_inverse_less_iff]) 1);
qed "hypreal_inverse_le_iff";
(** Division by 1, -1 **)
Goal "(x::hypreal)/1 = x";
-by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1);
+by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1);
qed "hypreal_divide_1";
Addsimps [hypreal_divide_1];
Goal "x/-1 = -(x::hypreal)";
-by (Simp_tac 1);
+by (Simp_tac 1);
qed "hypreal_divide_minus1";
Addsimps [hypreal_divide_minus1];
Goal "-1/(x::hypreal) = - (1/x)";
-by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_minus_inverse]) 1);
+by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_minus_inverse]) 1);
qed "hypreal_minus1_divide";
Addsimps [hypreal_minus1_divide];
Goal "[| (0::hypreal) < d1; 0 < d2 |] ==> EX e. 0 < e & e < d1 & e < d2";
-by (res_inst_tac [("x","(min d1 d2)/2")] exI 1);
-by (asm_simp_tac (simpset() addsimps [min_def]) 1);
+by (res_inst_tac [("x","(min d1 d2)/2")] exI 1);
+by (asm_simp_tac (simpset() addsimps [min_def]) 1);
qed "hypreal_lbound_gt_zero";
@@ -545,20 +543,20 @@
(** The next several equations can make the simplifier loop! **)
Goal "(x < - y) = (y < - (x::hypreal))";
-by Auto_tac;
-qed "hypreal_less_minus";
+by Auto_tac;
+qed "hypreal_less_minus";
Goal "(- x < y) = (- y < (x::hypreal))";
-by Auto_tac;
-qed "hypreal_minus_less";
+by Auto_tac;
+qed "hypreal_minus_less";
Goal "(x <= - y) = (y <= - (x::hypreal))";
-by Auto_tac;
-qed "hypreal_le_minus";
+by Auto_tac;
+qed "hypreal_le_minus";
Goal "(- x <= y) = (- y <= (x::hypreal))";
-by Auto_tac;
-qed "hypreal_minus_le";
+by Auto_tac;
+qed "hypreal_minus_le";
Goal "(x = - y) = (y = - (x::hypreal))";
by Auto_tac;
@@ -579,51 +577,51 @@
Addsimps [hypreal_minus_eq_cancel];
Goal "(-s <= -r) = ((r::hypreal) <= s)";
-by (stac hypreal_minus_le 1);
-by (Simp_tac 1);
+by (stac hypreal_minus_le 1);
+by (Simp_tac 1);
qed "hypreal_le_minus_iff";
-Addsimps [hypreal_le_minus_iff];
+Addsimps [hypreal_le_minus_iff];
(*Distributive laws for literals*)
Addsimps (map (inst "w" "number_of ?v")
- [hypreal_add_mult_distrib, hypreal_add_mult_distrib2,
- hypreal_diff_mult_distrib, hypreal_diff_mult_distrib2]);
+ [hypreal_add_mult_distrib, hypreal_add_mult_distrib2,
+ hypreal_diff_mult_distrib, hypreal_diff_mult_distrib2]);
-Addsimps (map (inst "x" "number_of ?v")
- [hypreal_less_minus, hypreal_le_minus, hypreal_equation_minus]);
-Addsimps (map (inst "y" "number_of ?v")
- [hypreal_minus_less, hypreal_minus_le, hypreal_minus_equation]);
+Addsimps (map (inst "x" "number_of ?v")
+ [hypreal_less_minus, hypreal_le_minus, hypreal_equation_minus]);
+Addsimps (map (inst "y" "number_of ?v")
+ [hypreal_minus_less, hypreal_minus_le, hypreal_minus_equation]);
-Addsimps (map (simplify (simpset()) o inst "x" "1")
- [hypreal_less_minus, hypreal_le_minus, hypreal_equation_minus]);
-Addsimps (map (simplify (simpset()) o inst "y" "1")
- [hypreal_minus_less, hypreal_minus_le, hypreal_minus_equation]);
+Addsimps (map (simplify (simpset()) o inst "x" "1")
+ [hypreal_less_minus, hypreal_le_minus, hypreal_equation_minus]);
+Addsimps (map (simplify (simpset()) o inst "y" "1")
+ [hypreal_minus_less, hypreal_minus_le, hypreal_minus_equation]);
(*** Simprules combining x+y and 0 ***)
Goal "(x+y = (0::hypreal)) = (y = -x)";
-by Auto_tac;
+by Auto_tac;
qed "hypreal_add_eq_0_iff";
AddIffs [hypreal_add_eq_0_iff];
Goal "(x+y < (0::hypreal)) = (y < -x)";
-by Auto_tac;
+by Auto_tac;
qed "hypreal_add_less_0_iff";
AddIffs [hypreal_add_less_0_iff];
Goal "((0::hypreal) < x+y) = (-x < y)";
-by Auto_tac;
+by Auto_tac;
qed "hypreal_0_less_add_iff";
AddIffs [hypreal_0_less_add_iff];
Goal "(x+y <= (0::hypreal)) = (y <= -x)";
-by Auto_tac;
+by Auto_tac;
qed "hypreal_add_le_0_iff";
AddIffs [hypreal_add_le_0_iff];
Goal "((0::hypreal) <= x+y) = (-x <= y)";
-by Auto_tac;
+by Auto_tac;
qed "hypreal_0_le_add_iff";
AddIffs [hypreal_0_le_add_iff];
@@ -633,12 +631,12 @@
**)
Goal "((0::hypreal) < x-y) = (y < x)";
-by Auto_tac;
+by Auto_tac;
qed "hypreal_0_less_diff_iff";
AddIffs [hypreal_0_less_diff_iff];
Goal "((0::hypreal) <= x-y) = (y <= x)";
-by Auto_tac;
+by Auto_tac;
qed "hypreal_0_le_diff_iff";
AddIffs [hypreal_0_le_diff_iff];
@@ -671,5 +669,3 @@
(*Replaces "inverse #nn" by 1/#nn *)
Addsimps [inst "x" "number_of ?w" hypreal_inverse_eq_divide];
-
-
--- a/src/HOL/Hyperreal/HyperBin.ML Tue Aug 06 11:20:47 2002 +0200
+++ b/src/HOL/Hyperreal/HyperBin.ML Tue Aug 06 11:22:05 2002 +0200
@@ -13,7 +13,7 @@
qed "hypreal_number_of";
Addsimps [hypreal_number_of];
-Goalw [hypreal_number_of_def] "Numeral0 = (0::hypreal)";
+Goalw [hypreal_number_of_def] "Numeral0 = (0::hypreal)";
by (Simp_tac 1);
qed "hypreal_numeral_0_eq_0";
@@ -25,7 +25,7 @@
Goal "(number_of v :: hypreal) + number_of v' = number_of (bin_add v v')";
by (simp_tac
- (HOL_ss addsimps [hypreal_number_of_def,
+ (HOL_ss addsimps [hypreal_number_of_def,
hypreal_of_real_add RS sym, add_real_number_of]) 1);
qed "add_hypreal_number_of";
Addsimps [add_hypreal_number_of];
@@ -43,7 +43,7 @@
Goalw [hypreal_number_of_def, hypreal_diff_def]
"(number_of v :: hypreal) - number_of w = \
\ number_of (bin_add v (bin_minus w))";
-by (Simp_tac 1);
+by (Simp_tac 1);
qed "diff_hypreal_number_of";
Addsimps [diff_hypreal_number_of];
@@ -52,8 +52,8 @@
Goal "(number_of v :: hypreal) * number_of v' = number_of (bin_mult v v')";
by (simp_tac
- (HOL_ss addsimps [hypreal_number_of_def,
- hypreal_of_real_mult RS sym, mult_real_number_of]) 1);
+ (HOL_ss addsimps [hypreal_number_of_def,
+ hypreal_of_real_mult RS sym, mult_real_number_of]) 1);
qed "mult_hypreal_number_of";
Addsimps [mult_hypreal_number_of];
@@ -64,8 +64,8 @@
(*For specialist use: NOT as default simprules*)
Goal "2 * z = (z+z::hypreal)";
by (simp_tac (simpset ()
- addsimps [lemma, hypreal_add_mult_distrib,
- hypreal_numeral_1_eq_1]) 1);
+ addsimps [lemma, hypreal_add_mult_distrib,
+ hypreal_numeral_1_eq_1]) 1);
qed "hypreal_mult_2";
Goal "z * 2 = (z+z::hypreal)";
@@ -80,8 +80,8 @@
Goal "((number_of v :: hypreal) = number_of v') = \
\ iszero (number_of (bin_add v (bin_minus v')))";
by (simp_tac
- (HOL_ss addsimps [hypreal_number_of_def,
- hypreal_of_real_eq_iff, eq_real_number_of]) 1);
+ (HOL_ss addsimps [hypreal_number_of_def,
+ hypreal_of_real_eq_iff, eq_real_number_of]) 1);
qed "eq_hypreal_number_of";
Addsimps [eq_hypreal_number_of];
@@ -91,8 +91,8 @@
Goal "((number_of v :: hypreal) < number_of v') = \
\ neg (number_of (bin_add v (bin_minus v')))";
by (simp_tac
- (HOL_ss addsimps [hypreal_number_of_def, hypreal_of_real_less_iff,
- less_real_number_of]) 1);
+ (HOL_ss addsimps [hypreal_number_of_def, hypreal_of_real_less_iff,
+ less_real_number_of]) 1);
qed "less_hypreal_number_of";
Addsimps [less_hypreal_number_of];
@@ -102,7 +102,7 @@
Goal "(number_of x <= (number_of y::hypreal)) = \
\ (~ number_of y < (number_of x::hypreal))";
by (rtac (linorder_not_less RS sym) 1);
-qed "le_hypreal_number_of_eq_not_less";
+qed "le_hypreal_number_of_eq_not_less";
Addsimps [le_hypreal_number_of_eq_not_less];
(*** New versions of existing theorems involving 0, 1 ***)
@@ -112,19 +112,19 @@
qed "hypreal_minus_1_eq_m1";
(*Maps 0 to Numeral0 and 1 to Numeral1 and -(Numeral1) to -1*)
-val hypreal_numeral_ss =
- real_numeral_ss addsimps [hypreal_numeral_0_eq_0 RS sym,
- hypreal_numeral_1_eq_1 RS sym,
- hypreal_minus_1_eq_m1];
+val hypreal_numeral_ss =
+ real_numeral_ss addsimps [hypreal_numeral_0_eq_0 RS sym,
+ hypreal_numeral_1_eq_1 RS sym,
+ hypreal_minus_1_eq_m1];
-fun rename_numerals th =
+fun rename_numerals th =
asm_full_simplify hypreal_numeral_ss (Thm.transfer (the_context ()) th);
(** Simplification of arithmetic when nested to the right **)
Goal "number_of v + (number_of w + z) = (number_of(bin_add v w) + z::hypreal)";
-by Auto_tac;
+by Auto_tac;
qed "hypreal_add_number_of_left";
Goal "number_of v *(number_of w * z) = (number_of(bin_mult v w) * z::hypreal)";
@@ -143,7 +143,7 @@
qed "hypreal_add_number_of_diff2";
Addsimps [hypreal_add_number_of_left, hypreal_mult_number_of_left,
- hypreal_add_number_of_diff1, hypreal_add_number_of_diff2];
+ hypreal_add_number_of_diff1, hypreal_add_number_of_diff2];
(**** Simprocs for numeric literals ****)
@@ -151,15 +151,15 @@
(** Combining of literal coefficients in sums of products **)
Goal "(x < y) = (x-y < (0::hypreal))";
-by (simp_tac (simpset() addsimps [hypreal_diff_less_eq]) 1);
+by (simp_tac (simpset() addsimps [hypreal_diff_less_eq]) 1);
qed "hypreal_less_iff_diff_less_0";
Goal "(x = y) = (x-y = (0::hypreal))";
-by (simp_tac (simpset() addsimps [hypreal_diff_eq_eq]) 1);
+by (simp_tac (simpset() addsimps [hypreal_diff_eq_eq]) 1);
qed "hypreal_eq_iff_diff_eq_0";
Goal "(x <= y) = (x-y <= (0::hypreal))";
-by (simp_tac (simpset() addsimps [hypreal_diff_le_eq]) 1);
+by (simp_tac (simpset() addsimps [hypreal_diff_le_eq]) 1);
qed "hypreal_le_iff_diff_le_0";
@@ -172,12 +172,12 @@
(** For cancel_numerals **)
-val rel_iff_rel_0_rls =
+val rel_iff_rel_0_rls =
map (inst "y" "?u+?v")
- [hypreal_less_iff_diff_less_0, hypreal_eq_iff_diff_eq_0,
+ [hypreal_less_iff_diff_less_0, hypreal_eq_iff_diff_eq_0,
hypreal_le_iff_diff_le_0] @
map (inst "y" "n")
- [hypreal_less_iff_diff_less_0, hypreal_eq_iff_diff_eq_0,
+ [hypreal_less_iff_diff_less_0, hypreal_eq_iff_diff_eq_0,
hypreal_le_iff_diff_le_0];
Goal "!!i::hypreal. (i*u + m = j*u + n) = ((i-j)*u + m = n)";
@@ -217,7 +217,7 @@
qed "hypreal_le_add_iff2";
Goal "-1 * (z::hypreal) = -z";
-by (simp_tac (simpset() addsimps [hypreal_minus_1_eq_m1 RS sym,
+by (simp_tac (simpset() addsimps [hypreal_minus_1_eq_m1 RS sym,
hypreal_mult_minus_1]) 1);
qed "hypreal_mult_minus1";
Addsimps [hypreal_mult_minus1];
@@ -236,7 +236,7 @@
(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic in simprocs
isn't complicated by the abstract 0 and 1.*)
-val numeral_syms = [hypreal_numeral_0_eq_0 RS sym,
+val numeral_syms = [hypreal_numeral_0_eq_0 RS sym,
hypreal_numeral_1_eq_1 RS sym];
(*Utilities*)
@@ -271,7 +271,7 @@
| dest_summing (pos, Const ("op -", _) $ t $ u, ts) =
dest_summing (pos, t, dest_summing (not pos, u, ts))
| dest_summing (pos, t, ts) =
- if pos then t::ts else uminus_const$t :: ts;
+ if pos then t::ts else uminus_const$t :: ts;
fun dest_sum t = dest_summing (true, t, []);
@@ -289,29 +289,29 @@
val dest_times = HOLogic.dest_bin "op *" hyprealT;
fun dest_prod t =
- let val (t,u) = dest_times t
+ let val (t,u) = dest_times t
in dest_prod t @ dest_prod u end
handle TERM _ => [t];
-(*DON'T do the obvious simplifications; that would create special cases*)
+(*DON'T do the obvious simplifications; that would create special cases*)
fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts);
(*Express t as a product of (possibly) a numeral with other sorted terms*)
fun dest_coeff sign (Const ("uminus", _) $ t) = dest_coeff (~sign) t
| dest_coeff sign t =
let val ts = sort Term.term_ord (dest_prod t)
- val (n, ts') = find_first_numeral [] ts
+ val (n, ts') = find_first_numeral [] ts
handle TERM _ => (1, ts)
in (sign*n, mk_prod ts') end;
(*Find first coefficient-term THAT MATCHES u*)
-fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
+fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
| find_first_coeff past u (t::terms) =
- let val (n,u') = dest_coeff 1 t
- in if u aconv u' then (n, rev past @ terms)
- else find_first_coeff (t::past) u terms
- end
- handle TERM _ => find_first_coeff (t::past) u terms;
+ let val (n,u') = dest_coeff 1 t
+ in if u aconv u' then (n, rev past @ terms)
+ else find_first_coeff (t::past) u terms
+ end
+ handle TERM _ => find_first_coeff (t::past) u terms;
(*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1*)
@@ -323,29 +323,29 @@
(*To perform binary arithmetic*)
val bin_simps =
[hypreal_numeral_0_eq_0 RS sym, hypreal_numeral_1_eq_1 RS sym,
- add_hypreal_number_of, hypreal_add_number_of_left,
- minus_hypreal_number_of,
- diff_hypreal_number_of, mult_hypreal_number_of,
+ add_hypreal_number_of, hypreal_add_number_of_left,
+ minus_hypreal_number_of,
+ diff_hypreal_number_of, mult_hypreal_number_of,
hypreal_mult_number_of_left] @ bin_arith_simps @ bin_rel_simps;
(*To evaluate binary negations of coefficients*)
val hypreal_minus_simps = NCons_simps @
- [hypreal_minus_1_eq_m1, minus_hypreal_number_of,
- bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
- bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
+ [hypreal_minus_1_eq_m1, minus_hypreal_number_of,
+ bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
+ bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
(*To let us treat subtraction as addition*)
-val diff_simps = [hypreal_diff_def, hypreal_minus_add_distrib,
+val diff_simps = [hypreal_diff_def, hypreal_minus_add_distrib,
hypreal_minus_minus];
(*push the unary minus down: - x * y = x * - y *)
-val hypreal_minus_mult_eq_1_to_2 =
- [hypreal_minus_mult_eq1 RS sym, hypreal_minus_mult_eq2] MRS trans
+val hypreal_minus_mult_eq_1_to_2 =
+ [hypreal_minus_mult_eq1 RS sym, hypreal_minus_mult_eq2] MRS trans
|> standard;
(*to extract again any uncancelled minuses*)
-val hypreal_minus_from_mult_simps =
- [hypreal_minus_minus, hypreal_minus_mult_eq1 RS sym,
+val hypreal_minus_from_mult_simps =
+ [hypreal_minus_minus, hypreal_minus_mult_eq1 RS sym,
hypreal_minus_mult_eq2 RS sym];
(*combine unary minus with numeric literals, however nested within a product*)
@@ -353,31 +353,30 @@
[hypreal_mult_assoc, hypreal_minus_mult_eq1, hypreal_minus_mult_eq_1_to_2];
(*Final simplification: cancel + and * *)
-val simplify_meta_eq =
+val simplify_meta_eq =
Int_Numeral_Simprocs.simplify_meta_eq
[hypreal_add_zero_left, hypreal_add_zero_right,
- hypreal_mult_0, hypreal_mult_0_right, hypreal_mult_1,
+ hypreal_mult_0, hypreal_mult_0_right, hypreal_mult_1,
hypreal_mult_1_right];
val prep_simproc = Real_Numeral_Simprocs.prep_simproc;
-val prep_pats = map Real_Numeral_Simprocs.prep_pat;
structure CancelNumeralsCommon =
struct
- val mk_sum = mk_sum
- val dest_sum = dest_sum
- val mk_coeff = mk_coeff
- val dest_coeff = dest_coeff 1
- val find_first_coeff = find_first_coeff []
+ val mk_sum = mk_sum
+ val dest_sum = dest_sum
+ val mk_coeff = mk_coeff
+ val dest_coeff = dest_coeff 1
+ val find_first_coeff = find_first_coeff []
val trans_tac = Real_Numeral_Simprocs.trans_tac
- val norm_tac =
+ val norm_tac =
ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
hypreal_minus_simps@hypreal_add_ac))
THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hypreal_mult_minus_simps))
THEN ALLGOALS
(simp_tac (HOL_ss addsimps hypreal_minus_from_mult_simps@
hypreal_add_ac@hypreal_mult_ac))
- val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
+ val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
val simplify_meta_eq = simplify_meta_eq
end;
@@ -409,53 +408,52 @@
val bal_add2 = hypreal_le_add_iff2 RS trans
);
-val cancel_numerals =
+val cancel_numerals =
map prep_simproc
[("hyprealeq_cancel_numerals",
- prep_pats ["(l::hypreal) + m = n", "(l::hypreal) = m + n",
- "(l::hypreal) - m = n", "(l::hypreal) = m - n",
- "(l::hypreal) * m = n", "(l::hypreal) = m * n"],
+ ["(l::hypreal) + m = n", "(l::hypreal) = m + n",
+ "(l::hypreal) - m = n", "(l::hypreal) = m - n",
+ "(l::hypreal) * m = n", "(l::hypreal) = m * n"],
EqCancelNumerals.proc),
- ("hyprealless_cancel_numerals",
- prep_pats ["(l::hypreal) + m < n", "(l::hypreal) < m + n",
- "(l::hypreal) - m < n", "(l::hypreal) < m - n",
- "(l::hypreal) * m < n", "(l::hypreal) < m * n"],
+ ("hyprealless_cancel_numerals",
+ ["(l::hypreal) + m < n", "(l::hypreal) < m + n",
+ "(l::hypreal) - m < n", "(l::hypreal) < m - n",
+ "(l::hypreal) * m < n", "(l::hypreal) < m * n"],
LessCancelNumerals.proc),
- ("hyprealle_cancel_numerals",
- prep_pats ["(l::hypreal) + m <= n", "(l::hypreal) <= m + n",
- "(l::hypreal) - m <= n", "(l::hypreal) <= m - n",
- "(l::hypreal) * m <= n", "(l::hypreal) <= m * n"],
+ ("hyprealle_cancel_numerals",
+ ["(l::hypreal) + m <= n", "(l::hypreal) <= m + n",
+ "(l::hypreal) - m <= n", "(l::hypreal) <= m - n",
+ "(l::hypreal) * m <= n", "(l::hypreal) <= m * n"],
LeCancelNumerals.proc)];
structure CombineNumeralsData =
struct
- val add = op + : int*int -> int
- val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *)
- val dest_sum = dest_sum
- val mk_coeff = mk_coeff
- val dest_coeff = dest_coeff 1
- val left_distrib = left_hypreal_add_mult_distrib RS trans
+ val add = op + : int*int -> int
+ val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *)
+ val dest_sum = dest_sum
+ val mk_coeff = mk_coeff
+ val dest_coeff = dest_coeff 1
+ val left_distrib = left_hypreal_add_mult_distrib RS trans
val prove_conv = Real_Numeral_Simprocs.prove_conv_nohyps
"hypreal_combine_numerals"
val trans_tac = Real_Numeral_Simprocs.trans_tac
- val norm_tac =
+ val norm_tac =
ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
hypreal_minus_simps@hypreal_add_ac))
THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hypreal_mult_minus_simps))
THEN ALLGOALS (simp_tac (HOL_ss addsimps hypreal_minus_from_mult_simps@
hypreal_add_ac@hypreal_mult_ac))
- val numeral_simp_tac = ALLGOALS
+ val numeral_simp_tac = ALLGOALS
(simp_tac (HOL_ss addsimps add_0s@bin_simps))
val simplify_meta_eq = simplify_meta_eq
end;
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
-
-val combine_numerals =
- prep_simproc ("hypreal_combine_numerals",
- prep_pats ["(i::hypreal) + j", "(i::hypreal) - j"],
- CombineNumerals.proc);
+
+val combine_numerals =
+ prep_simproc
+ ("hypreal_combine_numerals", ["(i::hypreal) + j", "(i::hypreal) - j"], CombineNumerals.proc);
(** Declarations for ExtractCommonTerm **)
@@ -465,16 +463,16 @@
| long_mk_prod (t :: ts) = mk_times (t, mk_prod ts);
(*Find first term that matches u*)
-fun find_first past u [] = raise TERM("find_first", [])
+fun find_first past u [] = raise TERM("find_first", [])
| find_first past u (t::terms) =
- if u aconv t then (rev past @ terms)
+ if u aconv t then (rev past @ terms)
else find_first (t::past) u terms
- handle TERM _ => find_first (t::past) u terms;
+ handle TERM _ => find_first (t::past) u terms;
(*Final simplification: cancel + and * *)
-fun cancel_simplify_meta_eq cancel_th th =
- Int_Numeral_Simprocs.simplify_meta_eq
- [hypreal_mult_1, hypreal_mult_1_right]
+fun cancel_simplify_meta_eq cancel_th th =
+ Int_Numeral_Simprocs.simplify_meta_eq
+ [hypreal_mult_1, hypreal_mult_1_right]
(([th, cancel_th]) MRS trans);
(*** Making constant folding work for 0 and 1 too ***)
@@ -488,36 +486,33 @@
val prove_conv = Real_Numeral_Simprocs.prove_conv_nohyps
"hypreal_abstract_numerals"
fun norm_tac simps = ALLGOALS (simp_tac (HOL_ss addsimps simps))
- val simplify_meta_eq = Bin_Simprocs.simplify_meta_eq
+ val simplify_meta_eq = Bin_Simprocs.simplify_meta_eq
end
-structure HyperrealAbstractNumerals =
+structure HyperrealAbstractNumerals =
AbstractNumeralsFun (HyperrealAbstractNumeralsData)
(*For addition, we already have rules for the operand 0.
- Multiplication is omitted because there are already special rules for
+ Multiplication is omitted because there are already special rules for
both 0 and 1 as operands. Unary minus is trivial, just have - 1 = -1.
For the others, having three patterns is a compromise between just having
one (many spurious calls) and having nine (just too many!) *)
-val eval_numerals =
+val eval_numerals =
map prep_simproc
[("hypreal_add_eval_numerals",
- prep_pats ["(m::hypreal) + 1", "(m::hypreal) + number_of v"],
+ ["(m::hypreal) + 1", "(m::hypreal) + number_of v"],
HyperrealAbstractNumerals.proc add_hypreal_number_of),
("hypreal_diff_eval_numerals",
- prep_pats ["(m::hypreal) - 1", "(m::hypreal) - number_of v"],
+ ["(m::hypreal) - 1", "(m::hypreal) - number_of v"],
HyperrealAbstractNumerals.proc diff_hypreal_number_of),
("hypreal_eq_eval_numerals",
- prep_pats ["(m::hypreal) = 0", "(m::hypreal) = 1",
- "(m::hypreal) = number_of v"],
+ ["(m::hypreal) = 0", "(m::hypreal) = 1", "(m::hypreal) = number_of v"],
HyperrealAbstractNumerals.proc eq_hypreal_number_of),
("hypreal_less_eval_numerals",
- prep_pats ["(m::hypreal) < 0", "(m::hypreal) < 1",
- "(m::hypreal) < number_of v"],
+ ["(m::hypreal) < 0", "(m::hypreal) < 1", "(m::hypreal) < number_of v"],
HyperrealAbstractNumerals.proc less_hypreal_number_of),
("hypreal_le_eval_numerals",
- prep_pats ["(m::hypreal) <= 0", "(m::hypreal) <= 1",
- "(m::hypreal) <= number_of v"],
+ ["(m::hypreal) <= 0", "(m::hypreal) <= 1", "(m::hypreal) <= number_of v"],
HyperrealAbstractNumerals.proc le_hypreal_number_of_eq_not_less)]
end;
@@ -533,7 +528,7 @@
print_depth 22;
set timing;
set trace_simp;
-fun test s = (Goal s, by (Simp_tac 1));
+fun test s = (Goal s, by (Simp_tac 1));
test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::hypreal)";
test "2*u = (u::hypreal)";
@@ -574,10 +569,10 @@
structure Hyperreal_Times_Assoc_Data : ASSOC_FOLD_DATA =
struct
- val ss = HOL_ss
- val eq_reflection = eq_reflection
+ val ss = HOL_ss
+ val eq_reflection = eq_reflection
val sg_ref = Sign.self_ref (Theory.sign_of (the_context ()))
- val T = Hyperreal_Numeral_Simprocs.hyprealT
+ val T = Hyperreal_Numeral_Simprocs.hyprealT
val plus = Const ("op *", [T,T] ---> T)
val add_ac = hypreal_mult_ac
end;
@@ -595,32 +590,32 @@
(** number_of related to hypreal_of_real **)
Goal "(number_of w < hypreal_of_real z) = (number_of w < z)";
-by (stac (hypreal_of_real_less_iff RS sym) 1);
-by (Simp_tac 1);
+by (stac (hypreal_of_real_less_iff RS sym) 1);
+by (Simp_tac 1);
qed "number_of_less_hypreal_of_real_iff";
Addsimps [number_of_less_hypreal_of_real_iff];
Goal "(number_of w <= hypreal_of_real z) = (number_of w <= z)";
-by (stac (hypreal_of_real_le_iff RS sym) 1);
-by (Simp_tac 1);
+by (stac (hypreal_of_real_le_iff RS sym) 1);
+by (Simp_tac 1);
qed "number_of_le_hypreal_of_real_iff";
Addsimps [number_of_le_hypreal_of_real_iff];
Goal "(hypreal_of_real z = number_of w) = (z = number_of w)";
-by (stac (hypreal_of_real_eq_iff RS sym) 1);
-by (Simp_tac 1);
+by (stac (hypreal_of_real_eq_iff RS sym) 1);
+by (Simp_tac 1);
qed "hypreal_of_real_eq_number_of_iff";
Addsimps [hypreal_of_real_eq_number_of_iff];
Goal "(hypreal_of_real z < number_of w) = (z < number_of w)";
-by (stac (hypreal_of_real_less_iff RS sym) 1);
-by (Simp_tac 1);
+by (stac (hypreal_of_real_less_iff RS sym) 1);
+by (Simp_tac 1);
qed "hypreal_of_real_less_number_of_iff";
Addsimps [hypreal_of_real_less_number_of_iff];
Goal "(hypreal_of_real z <= number_of w) = (z <= number_of w)";
-by (stac (hypreal_of_real_le_iff RS sym) 1);
-by (Simp_tac 1);
+by (stac (hypreal_of_real_le_iff RS sym) 1);
+by (Simp_tac 1);
qed "hypreal_of_real_le_number_of_iff";
Addsimps [hypreal_of_real_le_number_of_iff];
@@ -641,8 +636,8 @@
(** <= monotonicity results: needed for arithmetic **)
Goal "[| i <= j; (0::hypreal) <= k |] ==> i*k <= j*k";
-by (auto_tac (claset(),
- simpset() addsimps [order_le_less, hypreal_mult_less_mono1]));
+by (auto_tac (claset(),
+ simpset() addsimps [order_le_less, hypreal_mult_less_mono1]));
qed "hypreal_mult_le_mono1";
Goal "[| i <= j; (0::hypreal) <= k |] ==> k*i <= k*j";
--- a/src/HOL/Hyperreal/NSA.ML Tue Aug 06 11:20:47 2002 +0200
+++ b/src/HOL/Hyperreal/NSA.ML Tue Aug 06 11:22:05 2002 +0200
@@ -3,7 +3,7 @@
Copyright : 1998 University of Cambridge
Description : Infinite numbers, Infinitesimals,
infinitely close relation etc.
-*)
+*)
fun CLAIM_SIMP str thms =
prove_goal (the_context()) str
@@ -28,31 +28,31 @@
qed "SReal_mult";
Goalw [SReal_def] "(x::hypreal): Reals ==> inverse x : Reals";
-by (blast_tac (claset() addIs [hypreal_of_real_inverse RS sym]) 1);
+by (blast_tac (claset() addIs [hypreal_of_real_inverse RS sym]) 1);
qed "SReal_inverse";
Goal "[| (x::hypreal): Reals; y: Reals |] ==> x/y: Reals";
by (asm_simp_tac (simpset() addsimps [SReal_mult,SReal_inverse,
- hypreal_divide_def]) 1);
+ hypreal_divide_def]) 1);
qed "SReal_divide";
Goalw [SReal_def] "(x::hypreal): Reals ==> -x : Reals";
-by (blast_tac (claset() addIs [hypreal_of_real_minus RS sym]) 1);
+by (blast_tac (claset() addIs [hypreal_of_real_minus RS sym]) 1);
qed "SReal_minus";
Goal "(-x : Reals) = ((x::hypreal): Reals)";
-by Auto_tac;
-by (etac SReal_minus 2);
-by (dtac SReal_minus 1);
-by Auto_tac;
+by Auto_tac;
+by (etac SReal_minus 2);
+by (dtac SReal_minus 1);
+by Auto_tac;
qed "SReal_minus_iff";
-Addsimps [SReal_minus_iff];
+Addsimps [SReal_minus_iff];
Goal "[| (x::hypreal) + y : Reals; y: Reals |] ==> x: Reals";
by (dres_inst_tac [("x","y")] SReal_minus 1);
by (dtac SReal_add 1);
-by (assume_tac 1);
-by Auto_tac;
+by (assume_tac 1);
+by Auto_tac;
qed "SReal_add_cancel";
Goalw [SReal_def] "(x::hypreal): Reals ==> abs x : Reals";
@@ -73,18 +73,18 @@
Goal "(0::hypreal) : Reals";
by (stac (hypreal_numeral_0_eq_0 RS sym) 1);
-by (rtac SReal_number_of 1);
+by (rtac SReal_number_of 1);
qed "Reals_0";
Addsimps [Reals_0];
Goal "(1::hypreal) : Reals";
by (stac (hypreal_numeral_1_eq_1 RS sym) 1);
-by (rtac SReal_number_of 1);
+by (rtac SReal_number_of 1);
qed "Reals_1";
Addsimps [Reals_1];
Goalw [hypreal_divide_def] "r : Reals ==> r/(number_of w::hypreal) : Reals";
-by (blast_tac (claset() addSIs [SReal_number_of, SReal_mult,
+by (blast_tac (claset() addSIs [SReal_number_of, SReal_mult,
SReal_inverse]) 1);
qed "SReal_divide_number_of";
@@ -118,9 +118,9 @@
by (Blast_tac 1);
qed "inv_hypreal_of_real_image";
-Goalw [SReal_def]
+Goalw [SReal_def]
"[| EX x. x: P; P <= Reals |] ==> EX Q. P = hypreal_of_real ` Q";
-by (Best_tac 1);
+by (Best_tac 1);
qed "SReal_hypreal_of_real_image";
Goal "[| (x::hypreal): Reals; y: Reals; x<y |] ==> EX r: Reals. x<r & r<y";
@@ -133,7 +133,7 @@
(*------------------------------------------------------------------
Completeness of Reals
------------------------------------------------------------------*)
-Goal "P <= Reals ==> ((EX x:P. y < x) = \
+Goal "P <= Reals ==> ((EX x:P. y < x) = \
\ (EX X. hypreal_of_real X : P & y < hypreal_of_real X))";
by (blast_tac (claset() addSDs [SReal_iff RS iffD1]) 1);
by (flexflex_tac );
@@ -153,20 +153,20 @@
(*------------------------------------------------------
lifting of ub and property of lub
-------------------------------------------------------*)
-Goalw [isUb_def,setle_def]
+Goalw [isUb_def,setle_def]
"(isUb (Reals) (hypreal_of_real ` Q) (hypreal_of_real Y)) = \
\ (isUb (UNIV :: real set) Q Y)";
by Auto_tac;
qed "hypreal_of_real_isUb_iff";
-Goalw [isLub_def,leastP_def]
+Goalw [isLub_def,leastP_def]
"isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y) \
\ ==> isLub (UNIV :: real set) Q Y";
by (auto_tac (claset() addIs [hypreal_of_real_isUb_iff RS iffD2],
simpset() addsimps [hypreal_of_real_isUb_iff, setge_def]));
qed "hypreal_of_real_isLub1";
-Goalw [isLub_def,leastP_def]
+Goalw [isLub_def,leastP_def]
"isLub (UNIV :: real set) Q Y \
\ ==> isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)";
by (auto_tac (claset(),
@@ -184,17 +184,17 @@
qed "hypreal_of_real_isLub_iff";
(* lemmas *)
-Goalw [isUb_def]
+Goalw [isUb_def]
"isUb Reals P Y ==> EX Yo. isUb Reals P (hypreal_of_real Yo)";
by (auto_tac (claset(), simpset() addsimps [SReal_iff]));
qed "lemma_isUb_hypreal_of_real";
-Goalw [isLub_def,leastP_def,isUb_def]
+Goalw [isLub_def,leastP_def,isUb_def]
"isLub Reals P Y ==> EX Yo. isLub Reals P (hypreal_of_real Yo)";
by (auto_tac (claset(), simpset() addsimps [SReal_iff]));
qed "lemma_isLub_hypreal_of_real";
-Goalw [isLub_def,leastP_def,isUb_def]
+Goalw [isLub_def,leastP_def,isUb_def]
"EX Yo. isLub Reals P (hypreal_of_real Yo) ==> EX Y. isLub Reals P Y";
by Auto_tac;
qed "lemma_isLub_hypreal_of_real2";
@@ -203,7 +203,7 @@
\ ==> EX t::hypreal. isLub Reals P t";
by (ftac SReal_hypreal_of_real_image 1);
by (Auto_tac THEN dtac lemma_isUb_hypreal_of_real 1);
-by (auto_tac (claset() addSIs [reals_complete, lemma_isLub_hypreal_of_real2],
+by (auto_tac (claset() addSIs [reals_complete, lemma_isLub_hypreal_of_real2],
simpset() addsimps [hypreal_of_real_isLub_iff,hypreal_of_real_isUb_iff]));
qed "SReal_complete";
@@ -215,7 +215,7 @@
qed "HFinite_add";
Goalw [HFinite_def] "[|x : HFinite; y : HFinite|] ==> x*y : HFinite";
-by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
by (blast_tac (claset() addSIs [SReal_mult,hrabs_mult_less]) 1);
qed "HFinite_mult";
@@ -256,13 +256,13 @@
Goal "0 : HFinite";
by (stac (hypreal_numeral_0_eq_0 RS sym) 1);
-by (rtac HFinite_number_of 1);
+by (rtac HFinite_number_of 1);
qed "HFinite_0";
Addsimps [HFinite_0];
Goal "1 : HFinite";
by (stac (hypreal_numeral_1_eq_1 RS sym) 1);
-by (rtac HFinite_number_of 1);
+by (rtac HFinite_number_of 1);
qed "HFinite_1";
Addsimps [HFinite_1];
@@ -273,10 +273,10 @@
by (auto_tac (claset() addSDs [not_hypreal_leE], simpset()));
by (auto_tac (claset() addSIs [bexI] addIs [order_le_less_trans],
simpset() addsimps [hrabs_eqI1,hrabs_eqI2,hrabs_minus_eqI1,HFinite_def]));
-qed "HFinite_bounded";
+qed "HFinite_bounded";
(*------------------------------------------------------------------
- Set of infinitesimals is a subring of the hyperreals
+ Set of infinitesimals is a subring of the hyperreals
------------------------------------------------------------------*)
Goalw [Infinitesimal_def]
"x : Infinitesimal ==> ALL r: Reals. 0 < r --> abs x < r";
@@ -289,20 +289,20 @@
AddIffs [Infinitesimal_zero];
Goal "x/(2::hypreal) + x/(2::hypreal) = x";
-by Auto_tac;
+by Auto_tac;
qed "hypreal_sum_of_halves";
Goal "0 < r ==> 0 < r/(2::hypreal)";
-by Auto_tac;
+by Auto_tac;
qed "hypreal_half_gt_zero";
-Goalw [Infinitesimal_def]
+Goalw [Infinitesimal_def]
"[| x : Infinitesimal; y : Infinitesimal |] ==> (x+y) : Infinitesimal";
by Auto_tac;
by (rtac (hypreal_sum_of_halves RS subst) 1);
by (dtac hypreal_half_gt_zero 1);
-by (blast_tac (claset() addIs [hrabs_add_less, hrabs_add_less,
- SReal_divide_number_of]) 1);
+by (blast_tac (claset() addIs [hrabs_add_less, hrabs_add_less,
+ SReal_divide_number_of]) 1);
qed "Infinitesimal_add";
Goalw [Infinitesimal_def] "(-x:Infinitesimal) = (x:Infinitesimal)";
@@ -315,11 +315,11 @@
(simpset() addsimps [hypreal_diff_def, Infinitesimal_add]) 1);
qed "Infinitesimal_diff";
-Goalw [Infinitesimal_def]
+Goalw [Infinitesimal_def]
"[| x : Infinitesimal; y : Infinitesimal |] ==> (x * y) : Infinitesimal";
by Auto_tac;
by (case_tac "y=0" 1);
-by (cut_inst_tac [("u","abs x"),("v","1"),("x","abs y"),("y","r")]
+by (cut_inst_tac [("u","abs x"),("v","1"),("x","abs y"),("y","r")]
hypreal_mult_less_mono 2);
by Auto_tac;
qed "Infinitesimal_mult";
@@ -328,13 +328,13 @@
by (auto_tac (claset() addSDs [HFiniteD],
simpset() addsimps [Infinitesimal_def]));
by (ftac hrabs_less_gt_zero 1);
-by (dres_inst_tac [("x","r/t")] bspec 1);
+by (dres_inst_tac [("x","r/t")] bspec 1);
by (blast_tac (claset() addIs [SReal_divide]) 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_0_less_divide_iff]) 1);
+by (asm_full_simp_tac (simpset() addsimps [hypreal_0_less_divide_iff]) 1);
by (case_tac "x=0 | y=0" 1);
-by (cut_inst_tac [("u","abs x"),("v","r/t"),("x","abs y")]
+by (cut_inst_tac [("u","abs x"),("v","r/t"),("x","abs y")]
hypreal_mult_less_mono 2);
-by (auto_tac (claset(), simpset() addsimps [hypreal_0_less_divide_iff]));
+by (auto_tac (claset(), simpset() addsimps [hypreal_0_less_divide_iff]));
qed "Infinitesimal_HFinite_mult";
Goal "[| x : Infinitesimal; y : HFinite |] ==> (y * x) : Infinitesimal";
@@ -343,17 +343,17 @@
qed "Infinitesimal_HFinite_mult2";
(*** rather long proof ***)
-Goalw [HInfinite_def,Infinitesimal_def]
+Goalw [HInfinite_def,Infinitesimal_def]
"x: HInfinite ==> inverse x: Infinitesimal";
by Auto_tac;
by (eres_inst_tac [("x","inverse r")] ballE 1);
by (stac hrabs_inverse 1);
-by (forw_inst_tac [("x1","r"),("z","abs x")]
+by (forw_inst_tac [("x1","r"),("z","abs x")]
(hypreal_inverse_gt_0 RS order_less_trans) 1);
by (assume_tac 1);
by (dtac ((hypreal_inverse_inverse RS sym) RS subst) 1);
by (rtac (hypreal_inverse_less_iff RS iffD1) 1);
-by (auto_tac (claset(), simpset() addsimps [SReal_inverse]));
+by (auto_tac (claset(), simpset() addsimps [SReal_inverse]));
qed "HInfinite_inverse_Infinitesimal";
@@ -362,13 +362,13 @@
by Auto_tac;
by (eres_inst_tac [("x","1")] ballE 1);
by (eres_inst_tac [("x","r")] ballE 1);
-by (case_tac "y=0" 1);
+by (case_tac "y=0" 1);
by (cut_inst_tac [("x","1"),("y","abs x"),
("u","r"),("v","abs y")] hypreal_mult_less_mono 2);
-by (auto_tac (claset(), simpset() addsimps hypreal_mult_ac));
+by (auto_tac (claset(), simpset() addsimps hypreal_mult_ac));
qed "HInfinite_mult";
-Goalw [HInfinite_def]
+Goalw [HInfinite_def]
"[|x: HInfinite; 0 <= y; 0 <= x|] ==> (x + y): HInfinite";
by (auto_tac (claset() addSIs [hypreal_add_zero_less_le_mono],
simpset() addsimps [hrabs_eqI1, hypreal_add_commute,
@@ -401,7 +401,7 @@
order_less_imp_le]) 1);
qed "HInfinite_add_lt_zero";
-Goal "[|a: HFinite; b: HFinite; c: HFinite|] \
+Goal "[|a: HFinite; b: HFinite; c: HFinite|] \
\ ==> a*a + b*b + c*c : HFinite";
by (auto_tac (claset() addIs [HFinite_mult,HFinite_add], simpset()));
qed "HFinite_sum_squares";
@@ -423,7 +423,7 @@
by (Blast_tac 1);
qed "HFinite_diff_Infinitesimal_hrabs";
-Goalw [Infinitesimal_def]
+Goalw [Infinitesimal_def]
"[| e : Infinitesimal; abs x < e |] ==> x : Infinitesimal";
by (auto_tac (claset() addSDs [bspec], simpset()));
by (dres_inst_tac [("x","e")] (hrabs_ge_self RS order_le_less_trans) 1);
@@ -431,11 +431,11 @@
qed "hrabs_less_Infinitesimal";
Goal "[| e : Infinitesimal; abs x <= e |] ==> x : Infinitesimal";
-by (blast_tac (claset() addDs [order_le_imp_less_or_eq]
+by (blast_tac (claset() addDs [order_le_imp_less_or_eq]
addIs [hrabs_less_Infinitesimal]) 1);
qed "hrabs_le_Infinitesimal";
-Goalw [Infinitesimal_def]
+Goalw [Infinitesimal_def]
"[| e : Infinitesimal; \
\ e' : Infinitesimal; \
\ e' < x ; x < e |] ==> x : Infinitesimal";
@@ -451,16 +451,16 @@
simpset() addsimps [hypreal_le_eq_less_or_eq]));
qed "Infinitesimal_interval2";
-Goalw [Infinitesimal_def]
+Goalw [Infinitesimal_def]
"[| x ~: Infinitesimal; y ~: Infinitesimal|] ==> (x*y) ~:Infinitesimal";
by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [linorder_not_less]) 1);
+by (asm_full_simp_tac (simpset() addsimps [linorder_not_less]) 1);
by (eres_inst_tac [("x","r*ra")] ballE 1);
by (fast_tac (claset() addIs [SReal_mult]) 2);
by (auto_tac (claset(), simpset() addsimps [hypreal_0_less_mult_iff]));
by (cut_inst_tac [("x","ra"),("y","abs y"),
("u","r"),("v","abs x")] hypreal_mult_le_mono 1);
-by Auto_tac;
+by Auto_tac;
qed "not_Infinitesimal_mult";
Goal "x*y : Infinitesimal ==> x : Infinitesimal | y : Infinitesimal";
@@ -480,20 +480,20 @@
by (blast_tac (claset() addDs [HFinite_mult,not_Infinitesimal_mult]) 1);
qed "HFinite_Infinitesimal_diff_mult";
-Goalw [Infinitesimal_def,HFinite_def]
+Goalw [Infinitesimal_def,HFinite_def]
"Infinitesimal <= HFinite";
-by Auto_tac;
-by (res_inst_tac [("x","1")] bexI 1);
-by Auto_tac;
+by Auto_tac;
+by (res_inst_tac [("x","1")] bexI 1);
+by Auto_tac;
qed "Infinitesimal_subset_HFinite";
Goal "x: Infinitesimal ==> x * hypreal_of_real r : Infinitesimal";
-by (etac (HFinite_hypreal_of_real RSN
+by (etac (HFinite_hypreal_of_real RSN
(2,Infinitesimal_HFinite_mult)) 1);
qed "Infinitesimal_hypreal_of_real_mult";
Goal "x: Infinitesimal ==> hypreal_of_real r * x: Infinitesimal";
-by (etac (HFinite_hypreal_of_real RSN
+by (etac (HFinite_hypreal_of_real RSN
(2,Infinitesimal_HFinite_mult2)) 1);
qed "Infinitesimal_hypreal_of_real_mult2";
@@ -501,7 +501,7 @@
Infinitely close relation @=
----------------------------------------------------------------------*)
-Goalw [Infinitesimal_def,approx_def]
+Goalw [Infinitesimal_def,approx_def]
"(x:Infinitesimal) = (x @= 0)";
by (Simp_tac 1);
qed "mem_infmal_iff";
@@ -525,33 +525,33 @@
qed "approx_sym";
Goalw [approx_def] "[| x @= y; y @= z |] ==> x @= z";
-by (dtac Infinitesimal_add 1);
-by (assume_tac 1);
-by Auto_tac;
+by (dtac Infinitesimal_add 1);
+by (assume_tac 1);
+by Auto_tac;
qed "approx_trans";
Goal "[| r @= x; s @= x |] ==> r @= s";
-by (blast_tac (claset() addIs [approx_sym, approx_trans]) 1);
+by (blast_tac (claset() addIs [approx_sym, approx_trans]) 1);
qed "approx_trans2";
Goal "[| x @= r; x @= s|] ==> r @= s";
-by (blast_tac (claset() addIs [approx_sym, approx_trans]) 1);
+by (blast_tac (claset() addIs [approx_sym, approx_trans]) 1);
qed "approx_trans3";
-Goal "(number_of w @= x) = (x @= number_of w)";
-by (blast_tac (claset() addIs [approx_sym]) 1);
+Goal "(number_of w @= x) = (x @= number_of w)";
+by (blast_tac (claset() addIs [approx_sym]) 1);
qed "number_of_approx_reorient";
-Goal "(0 @= x) = (x @= 0)";
-by (blast_tac (claset() addIs [approx_sym]) 1);
+Goal "(0 @= x) = (x @= 0)";
+by (blast_tac (claset() addIs [approx_sym]) 1);
qed "zero_approx_reorient";
-Goal "(1 @= x) = (x @= 1)";
-by (blast_tac (claset() addIs [approx_sym]) 1);
+Goal "(1 @= x) = (x @= 1)";
+by (blast_tac (claset() addIs [approx_sym]) 1);
qed "one_approx_reorient";
-(*** re-orientation, following HOL/Integ/Bin.ML
+(*** re-orientation, following HOL/Integ/Bin.ML
We re-orient x @=y where x is 0, 1 or a numeral, unless y is as well!
***)
@@ -560,7 +560,7 @@
val meta_one_approx_reorient = one_approx_reorient RS eq_reflection;
val meta_number_of_approx_reorient = number_of_approx_reorient RS eq_reflection;
-(*reorientation simplification procedure: reorients (polymorphic)
+(*reorientation simplification procedure: reorients (polymorphic)
0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
fun reorient_proc sg _ (_ $ t $ u) =
case u of
@@ -568,15 +568,14 @@
| Const("1", _) => None
| Const("Numeral.number_of", _) $ _ => None
| _ => Some (case t of
- Const("0", _) => meta_zero_approx_reorient
- | Const("1", _) => meta_one_approx_reorient
- | Const("Numeral.number_of", _) $ _ =>
+ Const("0", _) => meta_zero_approx_reorient
+ | Const("1", _) => meta_one_approx_reorient
+ | Const("Numeral.number_of", _) $ _ =>
meta_number_of_approx_reorient);
-val approx_reorient_simproc =
- Bin_Simprocs.prep_simproc ("reorient_simproc",
- Bin_Simprocs.prep_pats ["0@=x", "1@=x", "number_of w @= x"],
- reorient_proc);
+val approx_reorient_simproc =
+ Bin_Simprocs.prep_simproc
+ ("reorient_simproc", ["0@=x", "1@=x", "number_of w @= x"], reorient_proc);
Addsimprocs [approx_reorient_simproc];
@@ -588,17 +587,17 @@
qed "Infinitesimal_approx_minus";
Goalw [monad_def] "(x @= y) = (monad(x)=monad(y))";
-by (auto_tac (claset() addDs [approx_sym]
+by (auto_tac (claset() addDs [approx_sym]
addSEs [approx_trans,equalityCE],
simpset()));
qed "approx_monad_iff";
Goal "[| x: Infinitesimal; y: Infinitesimal |] ==> x @= y";
by (asm_full_simp_tac (simpset() addsimps [mem_infmal_iff]) 1);
-by (blast_tac (claset() addIs [approx_trans, approx_sym]) 1);
+by (blast_tac (claset() addIs [approx_trans, approx_sym]) 1);
qed "Infinitesimal_approx";
-val prem1::prem2::rest =
+val prem1::prem2::rest =
goalw thy [approx_def] "[| a @= b; c @= d |] ==> a+c @= b+d";
by (stac hypreal_minus_add_distrib 1);
by (stac hypreal_add_assoc 1);
@@ -627,13 +626,13 @@
by (blast_tac (claset() addSIs [approx_add,approx_minus]) 1);
qed "approx_add_minus";
-Goalw [approx_def] "[| a @= b; c: HFinite|] ==> a*c @= b*c";
+Goalw [approx_def] "[| a @= b; c: HFinite|] ==> a*c @= b*c";
by (asm_full_simp_tac (simpset() addsimps [Infinitesimal_HFinite_mult,
- hypreal_minus_mult_eq1,hypreal_add_mult_distrib RS sym]
+ hypreal_minus_mult_eq1,hypreal_add_mult_distrib RS sym]
delsimps [hypreal_minus_mult_eq1 RS sym]) 1);
qed "approx_mult1";
-Goal "[|a @= b; c: HFinite|] ==> c*a @= c*b";
+Goal "[|a @= b; c: HFinite|] ==> c*a @= c*b";
by (asm_simp_tac (simpset() addsimps [approx_mult1,hypreal_mult_commute]) 1);
qed "approx_mult2";
@@ -653,7 +652,7 @@
by (Asm_simp_tac 1);
qed "approx_eq_imp";
-Goal "x: Infinitesimal ==> -x @= x";
+Goal "x: Infinitesimal ==> -x @= x";
by (fast_tac (HOL_cs addIs [Infinitesimal_minus_iff RS iffD2,
mem_infmal_iff RS iffD1,approx_trans2]) 1);
qed "Infinitesimal_minus_approx";
@@ -706,26 +705,26 @@
Goal "d + b @= d + c ==> b @= c";
by (dtac (approx_minus_iff RS iffD1) 1);
-by (asm_full_simp_tac (simpset() addsimps
- [hypreal_minus_add_distrib,approx_minus_iff RS sym]
+by (asm_full_simp_tac (simpset() addsimps
+ [hypreal_minus_add_distrib,approx_minus_iff RS sym]
@ hypreal_add_ac) 1);
qed "approx_add_left_cancel";
Goal "b + d @= c + d ==> b @= c";
by (rtac approx_add_left_cancel 1);
-by (asm_full_simp_tac (simpset() addsimps
+by (asm_full_simp_tac (simpset() addsimps
[hypreal_add_commute]) 1);
qed "approx_add_right_cancel";
Goal "b @= c ==> d + b @= d + c";
by (rtac (approx_minus_iff RS iffD2) 1);
-by (asm_full_simp_tac (simpset() addsimps
- [hypreal_minus_add_distrib,approx_minus_iff RS sym]
+by (asm_full_simp_tac (simpset() addsimps
+ [hypreal_minus_add_distrib,approx_minus_iff RS sym]
@ hypreal_add_ac) 1);
qed "approx_add_mono1";
Goal "b @= c ==> b + a @= c + a";
-by (asm_simp_tac (simpset() addsimps
+by (asm_simp_tac (simpset() addsimps
[hypreal_add_commute,approx_add_mono1]) 1);
qed "approx_add_mono2";
@@ -745,7 +744,7 @@
Goal "[| x: HFinite; x @= y |] ==> y: HFinite";
by (dtac (bex_Infinitesimal_iff2 RS iffD2) 1);
by (Step_tac 1);
-by (dtac (Infinitesimal_subset_HFinite RS subsetD
+by (dtac (Infinitesimal_subset_HFinite RS subsetD
RS (HFinite_minus_iff RS iffD2)) 1);
by (dtac HFinite_add 1);
by (auto_tac (claset(), simpset() addsimps [hypreal_add_assoc]));
@@ -757,11 +756,11 @@
qed "approx_hypreal_of_real_HFinite";
Goal "[|a @= b; c @= d; b: HFinite; d: HFinite|] ==> a*c @= b*d";
-by (rtac approx_trans 1);
-by (rtac approx_mult2 2);
+by (rtac approx_trans 1);
+by (rtac approx_mult2 2);
by (rtac approx_mult1 1);
-by (blast_tac (claset() addIs [approx_HFinite, approx_sym]) 2);
-by Auto_tac;
+by (blast_tac (claset() addIs [approx_HFinite, approx_sym]) 2);
+by Auto_tac;
qed "approx_mult_HFinite";
Goal "[|a @= hypreal_of_real b; c @= hypreal_of_real d |] \
@@ -800,44 +799,44 @@
qed "approx_SReal_mult_cancel";
Goal "[| a: Reals; a ~= 0|] ==> (a* w @= a*z) = (w @= z)";
-by (auto_tac (claset() addSIs [approx_mult2,SReal_subset_HFinite RS subsetD]
+by (auto_tac (claset() addSIs [approx_mult2,SReal_subset_HFinite RS subsetD]
addIs [approx_SReal_mult_cancel], simpset()));
qed "approx_SReal_mult_cancel_iff1";
Addsimps [approx_SReal_mult_cancel_iff1];
Goal "[| z <= f; f @= g; g <= z |] ==> f @= z";
-by (asm_full_simp_tac (simpset() addsimps [bex_Infinitesimal_iff2 RS sym]) 1);
-by Auto_tac;
+by (asm_full_simp_tac (simpset() addsimps [bex_Infinitesimal_iff2 RS sym]) 1);
+by Auto_tac;
by (res_inst_tac [("x","g+y-z")] bexI 1);
-by (Simp_tac 1);
-by (rtac Infinitesimal_interval2 1);
-by (rtac Infinitesimal_zero 2);
-by Auto_tac;
+by (Simp_tac 1);
+by (rtac Infinitesimal_interval2 1);
+by (rtac Infinitesimal_zero 2);
+by Auto_tac;
qed "approx_le_bound";
(*-----------------------------------------------------------------
Zero is the only infinitesimal that is also a real
-----------------------------------------------------------------*)
-Goalw [Infinitesimal_def]
+Goalw [Infinitesimal_def]
"[| x: Reals; y: Infinitesimal; 0 < x |] ==> y < x";
by (rtac (hrabs_ge_self RS order_le_less_trans) 1);
-by Auto_tac;
+by Auto_tac;
qed "Infinitesimal_less_SReal";
Goal "y: Infinitesimal ==> ALL r: Reals. 0 < r --> y < r";
by (blast_tac (claset() addIs [Infinitesimal_less_SReal]) 1);
qed "Infinitesimal_less_SReal2";
-Goalw [Infinitesimal_def]
+Goalw [Infinitesimal_def]
"[| 0 < y; y: Reals|] ==> y ~: Infinitesimal";
by (auto_tac (claset(), simpset() addsimps [hrabs_def]));
qed "SReal_not_Infinitesimal";
Goal "[| y < 0; y : Reals |] ==> y ~: Infinitesimal";
-by (stac (Infinitesimal_minus_iff RS sym) 1);
-by (rtac SReal_not_Infinitesimal 1);
-by Auto_tac;
+by (stac (Infinitesimal_minus_iff RS sym) 1);
+by (rtac SReal_not_Infinitesimal 1);
+by Auto_tac;
qed "SReal_minus_not_Infinitesimal";
Goal "Reals Int Infinitesimal = {0}";
@@ -854,7 +853,7 @@
Goal "[| x : Reals; x ~= 0 |] ==> x : HFinite - Infinitesimal";
by (auto_tac (claset() addDs [SReal_Infinitesimal_zero,
- SReal_subset_HFinite RS subsetD],
+ SReal_subset_HFinite RS subsetD],
simpset()));
qed "SReal_HFinite_diff_Infinitesimal";
@@ -864,9 +863,9 @@
qed "hypreal_of_real_HFinite_diff_Infinitesimal";
Goal "(hypreal_of_real x : Infinitesimal) = (x=0)";
-by Auto_tac;
-by (rtac ccontr 1);
-by (rtac (hypreal_of_real_HFinite_diff_Infinitesimal RS DiffD2) 1);
+by Auto_tac;
+by (rtac ccontr 1);
+by (rtac (hypreal_of_real_HFinite_diff_Infinitesimal RS DiffD2) 1);
by Auto_tac;
qed "hypreal_of_real_Infinitesimal_iff_0";
AddIffs [hypreal_of_real_Infinitesimal_iff_0];
@@ -879,17 +878,17 @@
(*again: 1 is a special case, but not 0 this time*)
Goal "1 ~: Infinitesimal";
by (stac (hypreal_numeral_1_eq_1 RS sym) 1);
-by (rtac number_of_not_Infinitesimal 1);
-by (Simp_tac 1);
+by (rtac number_of_not_Infinitesimal 1);
+by (Simp_tac 1);
qed "one_not_Infinitesimal";
Addsimps [one_not_Infinitesimal];
Goal "[| y: Reals; x @= y; y~= 0 |] ==> x ~= 0";
by (cut_inst_tac [("x","y")] hypreal_trichotomy 1);
-by (Asm_full_simp_tac 1);
-by (blast_tac (claset() addDs
- [approx_sym RS (mem_infmal_iff RS iffD2),
- SReal_not_Infinitesimal, SReal_minus_not_Infinitesimal]) 1);
+by (Asm_full_simp_tac 1);
+by (blast_tac (claset() addDs
+ [approx_sym RS (mem_infmal_iff RS iffD2),
+ SReal_not_Infinitesimal, SReal_minus_not_Infinitesimal]) 1);
qed "approx_SReal_not_zero";
Goal "[| x @= y; y : HFinite - Infinitesimal |] \
@@ -900,24 +899,24 @@
by (blast_tac (claset() addDs [approx_sym]) 1);
qed "HFinite_diff_Infinitesimal_approx";
-(*The premise y~=0 is essential; otherwise x/y =0 and we lose the
+(*The premise y~=0 is essential; otherwise x/y =0 and we lose the
HFinite premise.*)
Goal "[| y ~= 0; y: Infinitesimal; x/y : HFinite |] ==> x : Infinitesimal";
by (dtac Infinitesimal_HFinite_mult2 1);
by (assume_tac 1);
-by (asm_full_simp_tac
+by (asm_full_simp_tac
(simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 1);
qed "Infinitesimal_ratio";
(*------------------------------------------------------------------
- Standard Part Theorem: Every finite x: R* is infinitely
+ Standard Part Theorem: Every finite x: R* is infinitely
close to a unique real number (i.e a member of Reals)
------------------------------------------------------------------*)
(*------------------------------------------------------------------
Uniqueness: Two infinitely close reals are equal
------------------------------------------------------------------*)
-Goal "[|x: Reals; y: Reals|] ==> (x @= y) = (x = y)";
+Goal "[|x: Reals; y: Reals|] ==> (x @= y) = (x = y)";
by Auto_tac;
by (rewtac approx_def);
by (dres_inst_tac [("x","y")] SReal_minus 1);
@@ -928,50 +927,50 @@
qed "SReal_approx_iff";
Goal "(number_of v @= number_of w) = (number_of v = (number_of w :: hypreal))";
-by (rtac SReal_approx_iff 1);
-by Auto_tac;
+by (rtac SReal_approx_iff 1);
+by Auto_tac;
qed "number_of_approx_iff";
Addsimps [number_of_approx_iff];
(*And also for 0 @= #nn and 1 @= #nn, #nn @= 0 and #nn @= 1.*)
Addsimps
(map (simplify (simpset()))
- [inst "v" "Pls" number_of_approx_iff,
+ [inst "v" "Pls" number_of_approx_iff,
inst "v" "Pls BIT True" number_of_approx_iff,
- inst "w" "Pls" number_of_approx_iff,
+ inst "w" "Pls" number_of_approx_iff,
inst "w" "Pls BIT True" number_of_approx_iff]);
Goal "~ (0 @= 1)";
-by (stac SReal_approx_iff 1);
-by Auto_tac;
+by (stac SReal_approx_iff 1);
+by Auto_tac;
qed "not_0_approx_1";
Addsimps [not_0_approx_1];
Goal "~ (1 @= 0)";
-by (stac SReal_approx_iff 1);
-by Auto_tac;
+by (stac SReal_approx_iff 1);
+by Auto_tac;
qed "not_1_approx_0";
Addsimps [not_1_approx_0];
Goal "(hypreal_of_real k @= hypreal_of_real m) = (k = m)";
-by Auto_tac;
-by (rtac (inj_hypreal_of_real RS injD) 1);
-by (rtac (SReal_approx_iff RS iffD1) 1);
-by Auto_tac;
+by Auto_tac;
+by (rtac (inj_hypreal_of_real RS injD) 1);
+by (rtac (SReal_approx_iff RS iffD1) 1);
+by Auto_tac;
qed "hypreal_of_real_approx_iff";
Addsimps [hypreal_of_real_approx_iff];
Goal "(hypreal_of_real k @= number_of w) = (k = number_of w)";
-by (stac (hypreal_of_real_approx_iff RS sym) 1);
-by Auto_tac;
+by (stac (hypreal_of_real_approx_iff RS sym) 1);
+by Auto_tac;
qed "hypreal_of_real_approx_number_of_iff";
Addsimps [hypreal_of_real_approx_number_of_iff];
(*And also for 0 and 1.*)
Addsimps
(map (simplify (simpset()))
- [inst "w" "Pls" hypreal_of_real_approx_number_of_iff,
+ [inst "w" "Pls" hypreal_of_real_approx_number_of_iff,
inst "w" "Pls BIT True" hypreal_of_real_approx_number_of_iff]);
Goal "[| r: Reals; s: Reals; r @= x; s @= x|] ==> r = s";
@@ -1000,7 +999,7 @@
Goal "x: HFinite ==> EX y. y: {s. s: Reals & s < x}";
by (dtac HFiniteD 1 THEN Step_tac 1);
by (dtac SReal_minus 1);
-by (res_inst_tac [("x","-t")] exI 1);
+by (res_inst_tac [("x","-t")] exI 1);
by (auto_tac (claset(), simpset() addsimps [hrabs_interval_iff]));
qed "lemma_st_part_nonempty";
@@ -1026,7 +1025,7 @@
by (rtac ccontr 1 THEN dtac (linorder_not_le RS iffD2) 1);
by (dres_inst_tac [("x","t")] SReal_add 1 THEN assume_tac 1);
by (dres_inst_tac [("y","t + r")] (isLubD1 RS setleD) 1);
-by Auto_tac;
+by Auto_tac;
qed "lemma_st_part_le1";
Goalw [setle_def] "!!x::hypreal. [| S *<= x; x < y |] ==> S *<= y";
@@ -1035,7 +1034,7 @@
simpset()));
qed "hypreal_setle_less_trans";
-Goalw [isUb_def]
+Goalw [isUb_def]
"!!x::hypreal. [| isUb R S x; x < y; y: R |] ==> isUb R S y";
by (blast_tac (claset() addIs [hypreal_setle_less_trans]) 1);
qed "hypreal_gt_isUb";
@@ -1057,7 +1056,7 @@
\ ==> t + -r <= x";
by (ftac isLubD1a 1);
by (rtac ccontr 1 THEN dtac not_hypreal_leE 1);
-by (dtac SReal_minus 1 THEN dres_inst_tac [("x","t")]
+by (dtac SReal_minus 1 THEN dres_inst_tac [("x","t")]
SReal_add 1 THEN assume_tac 1);
by (dtac lemma_st_part_gt_ub 1 THEN REPEAT(assume_tac 1));
by (dtac isLub_le_isUb 1 THEN assume_tac 1);
@@ -1066,7 +1065,7 @@
qed "lemma_st_part_le2";
Goal "((x::hypreal) <= t + r) = (x + -t <= r)";
-by Auto_tac;
+by Auto_tac;
qed "lemma_hypreal_le_swap";
Goal "[| x: HFinite; \
@@ -1078,7 +1077,7 @@
qed "lemma_st_part1a";
Goal "(t + -r <= x) = (-(x + -t) <= (r::hypreal))";
-by Auto_tac;
+by Auto_tac;
qed "lemma_hypreal_le_swap2";
Goal "[| x: HFinite; \
@@ -1157,10 +1156,10 @@
by (blast_tac (claset() addDs [lemma_st_part_major2]) 1);
qed "lemma_st_part_Ex";
-Goalw [approx_def,Infinitesimal_def]
+Goalw [approx_def,Infinitesimal_def]
"x:HFinite ==> EX t: Reals. x @= t";
by (dtac lemma_st_part_Ex 1);
-by Auto_tac;
+by Auto_tac;
qed "st_part_Ex";
(*--------------------------------
@@ -1168,7 +1167,7 @@
-------------------------------*)
Goal "x:HFinite ==> EX! t. t: Reals & x @= t";
by (dtac st_part_Ex 1 THEN Step_tac 1);
-by (dtac approx_sym 2 THEN dtac approx_sym 2
+by (dtac approx_sym 2 THEN dtac approx_sym 2
THEN dtac approx_sym 2);
by (auto_tac (claset() addSIs [approx_unique_real], simpset()));
qed "st_part_Ex1";
@@ -1189,9 +1188,9 @@
qed "HFinite_not_HInfinite";
Goalw [HInfinite_def, HFinite_def] "x~: HFinite ==> x: HInfinite";
-by Auto_tac;
+by Auto_tac;
by (dres_inst_tac [("x","r + 1")] bspec 1);
-by (auto_tac (claset(), simpset() addsimps [SReal_add]));
+by (auto_tac (claset(), simpset() addsimps [SReal_add]));
qed "not_HFinite_HInfinite";
Goal "x : HInfinite | x : HFinite";
@@ -1237,7 +1236,7 @@
by (dtac Infinitesimal_HFinite_mult2 1);
by (assume_tac 1);
by (asm_full_simp_tac
- (simpset() addsimps [not_Infinitesimal_not_zero, hypreal_mult_inverse]) 1);
+ (simpset() addsimps [not_Infinitesimal_not_zero, hypreal_mult_inverse]) 1);
qed "HFinite_not_Infinitesimal_inverse";
Goal "[| x @= y; y : HFinite - Infinitesimal |] \
@@ -1249,7 +1248,7 @@
by (REPEAT(dtac HFinite_inverse2 1));
by (dtac approx_mult2 1 THEN assume_tac 1);
by Auto_tac;
-by (dres_inst_tac [("c","inverse x")] approx_mult1 1
+by (dres_inst_tac [("c","inverse x")] approx_mult1 1
THEN assume_tac 1);
by (auto_tac (claset() addIs [approx_sym],
simpset() addsimps [hypreal_mult_assoc]));
@@ -1261,8 +1260,8 @@
Goal "[| x: HFinite - Infinitesimal; \
\ h : Infinitesimal |] ==> inverse(x + h) @= inverse x";
-by (auto_tac (claset() addIs [approx_inverse, approx_sym,
- Infinitesimal_add_approx_self],
+by (auto_tac (claset() addIs [approx_inverse, approx_sym,
+ Infinitesimal_add_approx_self],
simpset()));
qed "inverse_add_Infinitesimal_approx";
@@ -1273,7 +1272,7 @@
qed "inverse_add_Infinitesimal_approx2";
Goal "[| x : HFinite - Infinitesimal; \
-\ h : Infinitesimal |] ==> inverse(x + h) + -inverse x @= h";
+\ h : Infinitesimal |] ==> inverse(x + h) + -inverse x @= h";
by (rtac approx_trans2 1);
by (auto_tac (claset() addIs [inverse_add_Infinitesimal_approx],
simpset() addsimps [mem_infmal_iff,
@@ -1297,7 +1296,7 @@
Addsimps [HFinite_square_iff];
Goal "(x*x : HInfinite) = (x : HInfinite)";
-by (auto_tac (claset(), simpset() addsimps
+by (auto_tac (claset(), simpset() addsimps
[HInfinite_HFinite_iff]));
qed "HInfinite_square_iff";
Addsimps [HInfinite_square_iff];
@@ -1366,7 +1365,7 @@
------------------------------------------------------------------*)
Goal "x @= y ==> {x,y}<=monad x";
by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps
+by (asm_full_simp_tac (simpset() addsimps
[approx_monad_iff]) 1);
qed "approx_subset_monad";
@@ -1393,15 +1392,15 @@
qed "approx_mem_monad_zero";
Goal "[| x @= y; x: Infinitesimal |] ==> abs x @= abs y";
-by (dtac (Infinitesimal_monad_zero_iff RS iffD1) 1);
-by (blast_tac (claset() addIs [approx_mem_monad_zero,
+by (dtac (Infinitesimal_monad_zero_iff RS iffD1) 1);
+by (blast_tac (claset() addIs [approx_mem_monad_zero,
monad_zero_hrabs_iff RS iffD1, mem_monad_approx, approx_trans3]) 1);
qed "Infinitesimal_approx_hrabs";
Goal "[| 0 < x; x ~:Infinitesimal; e :Infinitesimal |] ==> e < x";
by (rtac ccontr 1);
by (auto_tac (claset()
- addIs [Infinitesimal_zero RSN (2, Infinitesimal_interval)]
+ addIs [Infinitesimal_zero RSN (2, Infinitesimal_interval)]
addSDs [hypreal_leI, order_le_imp_less_or_eq],
simpset()));
qed "less_Infinitesimal_less";
@@ -1410,14 +1409,14 @@
by (dtac (mem_monad_approx RS approx_sym) 1);
by (etac (bex_Infinitesimal_iff2 RS iffD2 RS bexE) 1);
by (dres_inst_tac [("e","-xa")] less_Infinitesimal_less 1);
-by Auto_tac;
+by Auto_tac;
qed "Ball_mem_monad_gt_zero";
Goal "[| x < 0; x ~: Infinitesimal; u: monad x |] ==> u < 0";
by (dtac (mem_monad_approx RS approx_sym) 1);
by (etac (bex_Infinitesimal_iff RS iffD2 RS bexE) 1);
by (cut_inst_tac [("x","-x"),("e","xa")] less_Infinitesimal_less 1);
-by Auto_tac;
+by Auto_tac;
qed "Ball_mem_monad_less_zero";
Goal "[|0 < x; x ~: Infinitesimal; x @= y|] ==> 0 < y";
@@ -1480,25 +1479,25 @@
by (auto_tac (claset() addIs [approx_trans2], simpset()));
qed "hrabs_add_minus_Infinitesimal_cancel";
-(* interesting slightly counterintuitive theorem: necessary
- for proving that an open interval is an NS open set
+(* interesting slightly counterintuitive theorem: necessary
+ for proving that an open interval is an NS open set
*)
-Goalw [Infinitesimal_def]
+Goalw [Infinitesimal_def]
"[| x < y; u: Infinitesimal |] \
\ ==> hypreal_of_real x + u < hypreal_of_real y";
-by (dtac (hypreal_of_real_less_iff RS iffD2) 1);
+by (dtac (hypreal_of_real_less_iff RS iffD2) 1);
by (dtac (hypreal_less_minus_iff RS iffD1) 1 THEN Step_tac 1);
by (rtac (hypreal_less_minus_iff RS iffD2) 1);
by (dres_inst_tac [("x","hypreal_of_real y + -hypreal_of_real x")] bspec 1);
by (auto_tac (claset(),
- simpset() addsimps [hypreal_add_commute,
+ simpset() addsimps [hypreal_add_commute,
hrabs_interval_iff,
SReal_add, SReal_minus]));
qed "Infinitesimal_add_hypreal_of_real_less";
Goal "[| x: Infinitesimal; abs(hypreal_of_real r) < hypreal_of_real y |] \
\ ==> abs (hypreal_of_real r + x) < hypreal_of_real y";
-by (dres_inst_tac [("x","hypreal_of_real r")]
+by (dres_inst_tac [("x","hypreal_of_real r")]
approx_hrabs_add_Infinitesimal 1);
by (dtac (approx_sym RS (bex_Infinitesimal_iff2 RS iffD2)) 1);
by (auto_tac (claset() addSIs [Infinitesimal_add_hypreal_of_real_less],
@@ -1517,11 +1516,11 @@
\ ==> hypreal_of_real x <= hypreal_of_real y";
by (EVERY1 [rtac notI, rtac contrapos_np, assume_tac]);
by (res_inst_tac [("C","-u")] hypreal_less_add_right_cancel 1);
-by (Asm_full_simp_tac 1);
-by (dtac (Infinitesimal_minus_iff RS iffD2) 1);
-by (dtac Infinitesimal_add_hypreal_of_real_less 1);
-by (assume_tac 1);
-by Auto_tac;
+by (Asm_full_simp_tac 1);
+by (dtac (Infinitesimal_minus_iff RS iffD2) 1);
+by (dtac Infinitesimal_add_hypreal_of_real_less 1);
+by (assume_tac 1);
+by Auto_tac;
qed "Infinitesimal_add_cancel_hypreal_of_real_le";
Goal "[| u: Infinitesimal; hypreal_of_real x + u <= hypreal_of_real y |] \
@@ -1533,10 +1532,10 @@
Goal "[| u: Infinitesimal; v: Infinitesimal; \
\ hypreal_of_real x + u <= hypreal_of_real y + v |] \
\ ==> hypreal_of_real x <= hypreal_of_real y";
-by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
-by Auto_tac;
+by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
+by Auto_tac;
by (dres_inst_tac [("u","v-u")] Infinitesimal_add_hypreal_of_real_less 1);
-by (auto_tac (claset(), simpset() addsimps [Infinitesimal_diff]));
+by (auto_tac (claset(), simpset() addsimps [Infinitesimal_diff]));
qed "hypreal_of_real_le_add_Infininitesimal_cancel";
Goal "[| u: Infinitesimal; v: Infinitesimal; \
@@ -1555,22 +1554,22 @@
(*used once, in NSDERIV_inverse*)
Goal "[| h: Infinitesimal; x ~= 0 |] ==> hypreal_of_real x + h ~= 0";
-by Auto_tac;
+by Auto_tac;
qed "Infinitesimal_add_not_zero";
Goal "x*x + y*y : Infinitesimal ==> x*x : Infinitesimal";
-by (rtac Infinitesimal_interval2 1);
-by (rtac hypreal_le_square 3);
-by (rtac hypreal_self_le_add_pos 3);
-by Auto_tac;
+by (rtac Infinitesimal_interval2 1);
+by (rtac hypreal_le_square 3);
+by (rtac hypreal_self_le_add_pos 3);
+by Auto_tac;
qed "Infinitesimal_square_cancel";
Addsimps [Infinitesimal_square_cancel];
Goal "x*x + y*y : HFinite ==> x*x : HFinite";
-by (rtac HFinite_bounded 1);
-by (rtac hypreal_self_le_add_pos 2);
-by (rtac (hypreal_le_square) 2);
-by (assume_tac 1);
+by (rtac HFinite_bounded 1);
+by (rtac hypreal_self_le_add_pos 2);
+by (rtac (hypreal_le_square) 2);
+by (assume_tac 1);
qed "HFinite_square_cancel";
Addsimps [HFinite_square_cancel];
@@ -1595,9 +1594,9 @@
Addsimps [Infinitesimal_sum_square_cancel];
Goal "x*x + y*y + z*z : HFinite ==> x*x : HFinite";
-by (blast_tac (claset() addIs [hypreal_self_le_add_pos2, HFinite_bounded,
+by (blast_tac (claset() addIs [hypreal_self_le_add_pos2, HFinite_bounded,
hypreal_le_square,
- HFinite_number_of]) 1);
+ HFinite_number_of]) 1);
qed "HFinite_sum_square_cancel";
Addsimps [HFinite_sum_square_cancel];
@@ -1635,9 +1634,9 @@
Goal "x: monad (hypreal_of_real a) ==> x: HFinite";
by (dtac (mem_monad_approx RS approx_sym) 1);
by (dtac (bex_Infinitesimal_iff2 RS iffD2) 1);
-by (step_tac (claset() addSDs
+by (step_tac (claset() addSDs
[Infinitesimal_subset_HFinite RS subsetD]) 1);
-by (etac (SReal_hypreal_of_real RS (SReal_subset_HFinite
+by (etac (SReal_hypreal_of_real RS (SReal_subset_HFinite
RS subsetD) RS HFinite_add) 1);
qed "mem_monad_SReal_HFinite";
@@ -1673,7 +1672,7 @@
qed "st_hypreal_of_real";
Goal "[| x: HFinite; y: HFinite; st x = st y |] ==> x @= y";
-by (auto_tac (claset() addSDs [st_approx_self]
+by (auto_tac (claset() addSDs [st_approx_self]
addSEs [approx_trans3], simpset()));
qed "st_eq_approx";
@@ -1699,7 +1698,7 @@
by (dtac st_SReal_eq 1);
by (rtac approx_st_eq 1);
by (auto_tac (claset() addIs [HFinite_add],
- simpset() addsimps [Infinitesimal_add_approx_self
+ simpset() addsimps [Infinitesimal_add_approx_self
RS approx_sym]));
qed "st_Infinitesimal_add_SReal";
@@ -1711,7 +1710,7 @@
Goal "x: HFinite ==> \
\ EX e: Infinitesimal. x = st(x) + e";
-by (blast_tac (claset() addSDs [(st_approx_self RS
+by (blast_tac (claset() addSDs [(st_approx_self RS
approx_sym),bex_Infinitesimal_iff2 RS iffD2]) 1);
qed "HFinite_st_Infinitesimal_add";
@@ -1744,7 +1743,7 @@
by (forward_tac [HFinite_minus_iff RS iffD2] 1);
by (rtac hypreal_add_minus_eq_minus 1);
by (dtac (st_add RS sym) 1 THEN assume_tac 1);
-by Auto_tac;
+by Auto_tac;
qed "st_minus";
Goalw [hypreal_diff_def]
@@ -1776,7 +1775,7 @@
by (Asm_full_simp_tac 2);
by (thin_tac "x = st x + e" 1);
by (thin_tac "y = st y + ea" 1);
-by (asm_full_simp_tac (simpset() addsimps
+by (asm_full_simp_tac (simpset() addsimps
[hypreal_add_mult_distrib,hypreal_add_mult_distrib2]) 1);
by (REPEAT(dtac st_SReal 1));
by (full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
@@ -1788,7 +1787,7 @@
qed "st_mult";
Goal "x: Infinitesimal ==> st x = 0";
-by (stac (hypreal_numeral_0_eq_0 RS sym) 1);
+by (stac (hypreal_numeral_0_eq_0 RS sym) 1);
by (rtac (st_number_of RS subst) 1);
by (rtac approx_st_eq 1);
by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD],
@@ -1805,14 +1804,14 @@
by (auto_tac (claset(),
simpset() addsimps [st_mult RS sym, st_not_Infinitesimal,
HFinite_inverse]));
-by (stac hypreal_mult_inverse 1);
-by Auto_tac;
+by (stac hypreal_mult_inverse 1);
+by Auto_tac;
qed "st_inverse";
Goal "[| x: HFinite; y: HFinite; st y ~= 0 |] \
\ ==> st(x/y) = (st x) / (st y)";
by (auto_tac (claset(),
- simpset() addsimps [hypreal_divide_def, st_mult, st_not_Infinitesimal,
+ simpset() addsimps [hypreal_divide_def, st_mult, st_not_Infinitesimal,
HFinite_inverse, st_inverse]));
qed "st_divide";
Addsimps [st_divide];
@@ -1846,23 +1845,23 @@
by (ftac HFinite_st_Infinitesimal_add 1);
by (Step_tac 1);
by (rtac Infinitesimal_add_st_le_cancel 1);
-by (res_inst_tac [("x","ea"),("y","e")]
+by (res_inst_tac [("x","ea"),("y","e")]
Infinitesimal_diff 3);
by (auto_tac (claset(), simpset() addsimps [hypreal_add_assoc RS sym]));
qed "st_le";
Goal "[| 0 <= x; x: HFinite |] ==> 0 <= st x";
-by (stac (hypreal_numeral_0_eq_0 RS sym) 1);
+by (stac (hypreal_numeral_0_eq_0 RS sym) 1);
by (rtac (st_number_of RS subst) 1);
-by (rtac st_le 1);
-by Auto_tac;
+by (rtac st_le 1);
+by Auto_tac;
qed "st_zero_le";
Goal "[| x <= 0; x: HFinite |] ==> st x <= 0";
-by (stac (hypreal_numeral_0_eq_0 RS sym) 1);
+by (stac (hypreal_numeral_0_eq_0 RS sym) 1);
by (rtac (st_number_of RS subst) 1);
-by (rtac st_le 1);
-by Auto_tac;
+by (rtac st_le 1);
+by Auto_tac;
qed "st_zero_ge";
Goal "x: HFinite ==> abs(st x) = st(abs x)";
@@ -1891,12 +1890,12 @@
by Auto_tac;
qed "lemma_free2";
-Goalw [HFinite_def]
+Goalw [HFinite_def]
"x : HFinite ==> EX X: Rep_hypreal x. \
\ EX u. {n. abs (X n) < u}: FreeUltrafilterNat";
-by (auto_tac (claset(), simpset() addsimps
+by (auto_tac (claset(), simpset() addsimps
[hrabs_interval_iff]));
-by (auto_tac (claset(), simpset() addsimps
+by (auto_tac (claset(), simpset() addsimps
[hypreal_less_def,SReal_iff,hypreal_minus,
hypreal_of_real_def]));
by (dtac FreeUltrafilterNat_Rep_hypreal 1 THEN assume_tac 1);
@@ -1905,14 +1904,14 @@
by (Ultra_tac 1 THEN arith_tac 1);
qed "HFinite_FreeUltrafilterNat";
-Goalw [HFinite_def]
+Goalw [HFinite_def]
"EX X: Rep_hypreal x. \
\ EX u. {n. abs (X n) < u}: FreeUltrafilterNat\
\ ==> x : HFinite";
-by (auto_tac (claset(), simpset() addsimps
+by (auto_tac (claset(), simpset() addsimps
[hrabs_interval_iff]));
by (res_inst_tac [("x","hypreal_of_real u")] bexI 1);
-by (auto_tac (claset() addSIs [exI], simpset() addsimps
+by (auto_tac (claset() addSIs [exI], simpset() addsimps
[hypreal_less_def,SReal_iff,hypreal_minus,
hypreal_of_real_def]));
by (ALLGOALS(Ultra_tac THEN' arith_tac));
@@ -1945,7 +1944,7 @@
qed "lemma_FreeUltrafilterNat_one";
(*-------------------------------------
- Exclude this type of sets from free
+ Exclude this type of sets from free
ultrafilter for Infinite numbers!
-------------------------------------*)
Goal "[| xa: Rep_hypreal x; \
@@ -1961,11 +1960,11 @@
\ ALL u. {n. u < abs (X n)}: FreeUltrafilterNat";
by (cut_facts_tac [(prem RS (HInfinite_HFinite_iff RS iffD1))] 1);
by (cut_inst_tac [("x","x")] Rep_hypreal_nonempty 1);
-by (auto_tac (claset(), simpset() delsimps [Rep_hypreal_nonempty]
+by (auto_tac (claset(), simpset() delsimps [Rep_hypreal_nonempty]
addsimps [HFinite_FreeUltrafilterNat_iff,Bex_def]));
by (REPEAT(dtac spec 1));
by Auto_tac;
-by (dres_inst_tac [("x","u")] spec 1 THEN
+by (dres_inst_tac [("x","u")] spec 1 THEN
REPEAT(dtac FreeUltrafilterNat_Compl_mem 1));
by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
@@ -2019,7 +2018,7 @@
by Auto_tac;
qed "lemma_free5";
-Goalw [Infinitesimal_def]
+Goalw [Infinitesimal_def]
"x : Infinitesimal ==> EX X: Rep_hypreal x. \
\ ALL u. 0 < u --> {n. abs (X n) < u}: FreeUltrafilterNat";
by (auto_tac (claset(), simpset() addsimps [hrabs_interval_iff]));
@@ -2028,13 +2027,13 @@
by (dtac (hypreal_of_real_less_iff RS iffD2) 1);
by (dres_inst_tac [("x","hypreal_of_real u")] bspec 1);
by Auto_tac;
-by (auto_tac (claset(),
+by (auto_tac (claset(),
simpset() addsimps [hypreal_less_def, hypreal_minus,
hypreal_of_real_def]));
by (Ultra_tac 1 THEN arith_tac 1);
qed "Infinitesimal_FreeUltrafilterNat";
-Goalw [Infinitesimal_def]
+Goalw [Infinitesimal_def]
"EX X: Rep_hypreal x. \
\ ALL u. 0 < u --> {n. abs (X n) < u} : FreeUltrafilterNat \
\ ==> x : Infinitesimal";
@@ -2042,7 +2041,7 @@
simpset() addsimps [hrabs_interval_iff,abs_interval_iff]));
by (auto_tac (claset(),
simpset() addsimps [SReal_iff]));
-by (auto_tac (claset() addSIs [exI]
+by (auto_tac (claset() addSIs [exI]
addIs [FreeUltrafilterNat_subset],
simpset() addsimps [hypreal_less_def, hypreal_minus,hypreal_of_real_def]));
qed "FreeUltrafilterNat_Infinitesimal";
@@ -2059,37 +2058,37 @@
Goal "(ALL r. 0 < r --> x < r) = (ALL n. x < inverse(real (Suc n)))";
by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc_gt_zero]));
-by (blast_tac (claset() addSDs [reals_Archimedean]
+by (blast_tac (claset() addSDs [reals_Archimedean]
addIs [order_less_trans]) 1);
qed "lemma_Infinitesimal";
Goal "(ALL r: Reals. 0 < r --> x < r) = \
\ (ALL n. x < inverse(hypreal_of_nat (Suc n)))";
by (Step_tac 1);
-by (dres_inst_tac [("x","inverse (hypreal_of_real(real (Suc n)))")]
+by (dres_inst_tac [("x","inverse (hypreal_of_real(real (Suc n)))")]
bspec 1);
-by (full_simp_tac (simpset() addsimps [SReal_inverse]) 1);
-by (rtac (real_of_nat_Suc_gt_zero RS real_inverse_gt_0 RS
+by (full_simp_tac (simpset() addsimps [SReal_inverse]) 1);
+by (rtac (real_of_nat_Suc_gt_zero RS real_inverse_gt_0 RS
(hypreal_of_real_less_iff RS iffD2) RSN(2,impE)) 1);
by (assume_tac 2);
-by (asm_full_simp_tac (simpset() addsimps
+by (asm_full_simp_tac (simpset() addsimps
[real_of_nat_Suc_gt_zero, hypreal_of_nat_def]) 1);
by (auto_tac (claset() addSDs [reals_Archimedean],
simpset() addsimps [SReal_iff]));
by (dtac (hypreal_of_real_less_iff RS iffD2) 1);
-by (asm_full_simp_tac (simpset() addsimps
+by (asm_full_simp_tac (simpset() addsimps
[real_of_nat_Suc_gt_zero, hypreal_of_nat_def])1);
by (blast_tac (claset() addIs [order_less_trans]) 1);
qed "lemma_Infinitesimal2";
-Goalw [Infinitesimal_def]
+Goalw [Infinitesimal_def]
"Infinitesimal = {x. ALL n. abs x < inverse (hypreal_of_nat (Suc n))}";
by (auto_tac (claset(), simpset() addsimps [lemma_Infinitesimal2]));
qed "Infinitesimal_hypreal_of_nat_iff";
(*-------------------------------------------------------------------------
- Proof that omega is an infinite number and
+ Proof that omega is an infinite number and
hence that epsilon is an infinitesimal number.
-------------------------------------------------------------------------*)
Goal "{n. n < Suc m} = {n. n < m} Un {n. n = m}";
@@ -2097,7 +2096,7 @@
qed "Suc_Un_eq";
(*-------------------------------------------
- Prove that any segment is finite and
+ Prove that any segment is finite and
hence cannot belong to FreeUltrafilterNat
-------------------------------------------*)
Goal "finite {n::nat. n < m}";
@@ -2122,8 +2121,8 @@
qed "lemma_real_le_Un_eq";
Goal "finite {n::nat. real n <= u}";
-by (auto_tac (claset(),
- simpset() addsimps [lemma_real_le_Un_eq,lemma_finite_omega_set,
+by (auto_tac (claset(),
+ simpset() addsimps [lemma_real_le_Un_eq,lemma_finite_omega_set,
finite_real_of_nat_less_real]));
qed "finite_real_of_nat_le_real";
@@ -2140,14 +2139,14 @@
Goal "{n. u < real n} : FreeUltrafilterNat";
by (rtac ccontr 1 THEN dtac FreeUltrafilterNat_Compl_mem 1);
by (subgoal_tac "- {n::nat. u < real n} = {n. real n <= u}" 1);
-by (Force_tac 2);
+by (Force_tac 2);
by (asm_full_simp_tac (simpset() addsimps
- [finite_real_of_nat_le_real RS FreeUltrafilterNat_finite]) 1);
+ [finite_real_of_nat_le_real RS FreeUltrafilterNat_finite]) 1);
qed "FreeUltrafilterNat_nat_gt_real";
(*--------------------------------------------------------------
- The complement of {n. abs(real n) <= u} =
- {n. u < abs (real n)} is in FreeUltrafilterNat
+ The complement of {n. abs(real n) <= u} =
+ {n. u < abs (real n)} is in FreeUltrafilterNat
by property of (free) ultrafilters
--------------------------------------------------------------*)
Goal "- {n::nat. real n <= u} = {n. u < real n}";
@@ -2170,13 +2169,13 @@
qed "FreeUltrafilterNat_omega";
Goalw [omega_def] "omega: HInfinite";
-by (auto_tac (claset() addSIs [FreeUltrafilterNat_HInfinite],
+by (auto_tac (claset() addSIs [FreeUltrafilterNat_HInfinite],
simpset()));
-by (rtac bexI 1);
-by (rtac lemma_hyprel_refl 2);
-by Auto_tac;
-by (simp_tac (simpset() addsimps [real_of_nat_Suc, real_diff_less_eq RS sym,
- FreeUltrafilterNat_omega]) 1);
+by (rtac bexI 1);
+by (rtac lemma_hyprel_refl 2);
+by Auto_tac;
+by (simp_tac (simpset() addsimps [real_of_nat_Suc, real_diff_less_eq RS sym,
+ FreeUltrafilterNat_omega]) 1);
qed "HInfinite_omega";
(*-----------------------------------------------
@@ -2201,24 +2200,24 @@
Addsimps [epsilon_approx_zero];
(*------------------------------------------------------------------------
- Needed for proof that we define a hyperreal [<X(n)] @= hypreal_of_real a given
+ Needed for proof that we define a hyperreal [<X(n)] @= hypreal_of_real a given
that ALL n. |X n - a| < 1/n. Used in proof of NSLIM => LIM.
-----------------------------------------------------------------------*)
Goal "0 < u ==> \
\ (u < inverse (real(Suc n))) = (real(Suc n) < inverse u)";
by (asm_full_simp_tac (simpset() addsimps [real_inverse_eq_divide]) 1);
-by (stac pos_real_less_divide_eq 1);
-by (assume_tac 1);
-by (stac pos_real_less_divide_eq 1);
-by (simp_tac (simpset() addsimps [real_mult_commute]) 2);
-by (simp_tac (simpset() addsimps [real_of_nat_Suc_gt_zero]) 1);
+by (stac pos_real_less_divide_eq 1);
+by (assume_tac 1);
+by (stac pos_real_less_divide_eq 1);
+by (simp_tac (simpset() addsimps [real_mult_commute]) 2);
+by (simp_tac (simpset() addsimps [real_of_nat_Suc_gt_zero]) 1);
qed "real_of_nat_less_inverse_iff";
Goal "0 < u ==> finite {n. u < inverse(real(Suc n))}";
by (asm_simp_tac (simpset() addsimps [real_of_nat_less_inverse_iff]) 1);
-by (asm_simp_tac (simpset() addsimps [real_of_nat_Suc,
- real_less_diff_eq RS sym]) 1);
+by (asm_simp_tac (simpset() addsimps [real_of_nat_Suc,
+ real_less_diff_eq RS sym]) 1);
by (rtac finite_real_of_nat_less_real 1);
qed "finite_inverse_real_of_posnat_gt_real";
@@ -2229,28 +2228,28 @@
qed "lemma_real_le_Un_eq2";
Goal "(inverse (real(Suc n)) <= r) = (1 <= r * real(Suc n))";
-by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
+by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
by (simp_tac (simpset() addsimps [real_inverse_eq_divide]) 1);
-by (stac pos_real_less_divide_eq 1);
-by (simp_tac (simpset() addsimps [real_of_nat_Suc_gt_zero]) 1);
-by (simp_tac (simpset() addsimps [real_mult_commute]) 1);
+by (stac pos_real_less_divide_eq 1);
+by (simp_tac (simpset() addsimps [real_of_nat_Suc_gt_zero]) 1);
+by (simp_tac (simpset() addsimps [real_mult_commute]) 1);
qed "real_of_nat_inverse_le_iff";
Goal "(u = inverse (real(Suc n))) = (real(Suc n) = inverse u)";
by (auto_tac (claset(),
- simpset() addsimps [real_inverse_inverse, real_of_nat_Suc_gt_zero,
- real_not_refl2 RS not_sym]));
+ simpset() addsimps [real_inverse_inverse, real_of_nat_Suc_gt_zero,
+ real_not_refl2 RS not_sym]));
qed "real_of_nat_inverse_eq_iff";
Goal "finite {n::nat. u = inverse(real(Suc n))}";
by (asm_simp_tac (simpset() addsimps [real_of_nat_inverse_eq_iff]) 1);
by (cut_inst_tac [("x","inverse u - 1")] lemma_finite_omega_set 1);
-by (asm_full_simp_tac (simpset() addsimps [real_of_nat_Suc,
- real_diff_eq_eq RS sym, eq_commute]) 1);
+by (asm_full_simp_tac (simpset() addsimps [real_of_nat_Suc,
+ real_diff_eq_eq RS sym, eq_commute]) 1);
qed "lemma_finite_omega_set2";
Goal "0 < u ==> finite {n. u <= inverse(real(Suc n))}";
-by (auto_tac (claset(),
+by (auto_tac (claset(),
simpset() addsimps [lemma_real_le_Un_eq2,lemma_finite_omega_set2,
finite_inverse_real_of_posnat_gt_real]));
qed "finite_inverse_real_of_posnat_ge_real";
@@ -2263,7 +2262,7 @@
(*--------------------------------------------------------------
The complement of {n. u <= inverse(real(Suc n))} =
- {n. inverse(real(Suc n)) < u} is in FreeUltrafilterNat
+ {n. inverse(real(Suc n)) < u} is in FreeUltrafilterNat
by property of (free) ultrafilters
--------------------------------------------------------------*)
Goal "- {n. u <= inverse(real(Suc n))} = \
@@ -2284,44 +2283,44 @@
for which a particular property holds. The theorem is
used in proofs about equivalence of nonstandard and
standard neighbourhoods. Also used for equivalence of
- nonstandard ans standard definitions of pointwise
+ nonstandard ans standard definitions of pointwise
limit (the theorem was previously in REALTOPOS.thy).
-------------------------------------------------------------*)
(*-----------------------------------------------------
- |X(n) - x| < 1/n ==> [<X n>] - hypreal_of_real x|: Infinitesimal
+ |X(n) - x| < 1/n ==> [<X n>] - hypreal_of_real x|: Infinitesimal
-----------------------------------------------------*)
-Goal "ALL n. abs(X n + -x) < inverse(real(Suc n)) \
+Goal "ALL n. abs(X n + -x) < inverse(real(Suc n)) \
\ ==> Abs_hypreal(hyprel``{X}) + -hypreal_of_real x : Infinitesimal";
-by (auto_tac (claset() addSIs [bexI]
+by (auto_tac (claset() addSIs [bexI]
addDs [FreeUltrafilterNat_inverse_real_of_posnat,
- FreeUltrafilterNat_all,FreeUltrafilterNat_Int]
+ FreeUltrafilterNat_all,FreeUltrafilterNat_Int]
addIs [order_less_trans, FreeUltrafilterNat_subset],
- simpset() addsimps [hypreal_minus,
+ simpset() addsimps [hypreal_minus,
hypreal_of_real_def,hypreal_add,
Infinitesimal_FreeUltrafilterNat_iff,hypreal_inverse]));
qed "real_seq_to_hypreal_Infinitesimal";
-Goal "ALL n. abs(X n + -x) < inverse(real(Suc n)) \
+Goal "ALL n. abs(X n + -x) < inverse(real(Suc n)) \
\ ==> Abs_hypreal(hyprel``{X}) @= hypreal_of_real x";
by (stac approx_minus_iff 1);
by (rtac (mem_infmal_iff RS subst) 1);
by (etac real_seq_to_hypreal_Infinitesimal 1);
qed "real_seq_to_hypreal_approx";
-Goal "ALL n. abs(x + -X n) < inverse(real(Suc n)) \
+Goal "ALL n. abs(x + -X n) < inverse(real(Suc n)) \
\ ==> Abs_hypreal(hyprel``{X}) @= hypreal_of_real x";
by (asm_full_simp_tac (simpset() addsimps [abs_minus_add_cancel,
real_seq_to_hypreal_approx]) 1);
qed "real_seq_to_hypreal_approx2";
-Goal "ALL n. abs(X n + -Y n) < inverse(real(Suc n)) \
+Goal "ALL n. abs(X n + -Y n) < inverse(real(Suc n)) \
\ ==> Abs_hypreal(hyprel``{X}) + \
\ -Abs_hypreal(hyprel``{Y}) : Infinitesimal";
-by (auto_tac (claset() addSIs [bexI]
+by (auto_tac (claset() addSIs [bexI]
addDs [FreeUltrafilterNat_inverse_real_of_posnat,
- FreeUltrafilterNat_all,FreeUltrafilterNat_Int]
+ FreeUltrafilterNat_all,FreeUltrafilterNat_Int]
addIs [order_less_trans, FreeUltrafilterNat_subset],
- simpset() addsimps
- [Infinitesimal_FreeUltrafilterNat_iff,hypreal_minus,hypreal_add,
+ simpset() addsimps
+ [Infinitesimal_FreeUltrafilterNat_iff,hypreal_minus,hypreal_add,
hypreal_inverse]));
qed "real_seq_to_hypreal_Infinitesimal2";
--- a/src/HOL/Hyperreal/hypreal_arith0.ML Tue Aug 06 11:20:47 2002 +0200
+++ b/src/HOL/Hyperreal/hypreal_arith0.ML Tue Aug 06 11:22:05 2002 +0200
@@ -44,11 +44,6 @@
"(i <= j) & (k < l) ==> i + k < j + (l::hypreal)",
"(i < j) & (k < l) ==> i + k < j + (l::hypreal)"];
-val hypreal_arith_simproc_pats =
- map (fn s => Thm.read_cterm (Theory.sign_of (the_context ()))
- (s, HOLogic.boolT))
- ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"];
-
fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var;
val hypreal_mult_mono_thms =
@@ -59,8 +54,10 @@
in
-val fast_hypreal_arith_simproc = mk_simproc
- "fast_hypreal_arith" hypreal_arith_simproc_pats Fast_Arith.lin_arith_prover;
+val fast_hypreal_arith_simproc =
+ Simplifier.simproc (Theory.sign_of (the_context ()))
+ "fast_hypreal_arith" ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
+ Fast_Arith.lin_arith_prover;
val hypreal_arith_setup =
[Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
--- a/src/HOL/Integ/Bin.ML Tue Aug 06 11:20:47 2002 +0200
+++ b/src/HOL/Integ/Bin.ML Tue Aug 06 11:22:05 2002 +0200
@@ -348,9 +348,8 @@
(*version without the hyps argument*)
fun prove_conv_nohyps name tacs sg = prove_conv name tacs sg []
- fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc
- fun prep_pat s = HOLogic.read_cterm (Theory.sign_of (the_context())) s
- val prep_pats = map prep_pat
+ fun prep_simproc (name, pats, proc) =
+ Simplifier.simproc (Theory.sign_of (the_context())) name pats proc;
fun is_numeral (Const("Numeral.number_of", _) $ w) = true
| is_numeral _ = false
@@ -380,19 +379,19 @@
val eval_numerals =
map prep_simproc
[("int_add_eval_numerals",
- prep_pats ["(m::int) + 1", "(m::int) + number_of v"],
+ ["(m::int) + 1", "(m::int) + number_of v"],
IntAbstractNumerals.proc (number_of_add RS sym)),
("int_diff_eval_numerals",
- prep_pats ["(m::int) - 1", "(m::int) - number_of v"],
+ ["(m::int) - 1", "(m::int) - number_of v"],
IntAbstractNumerals.proc diff_number_of_eq),
("int_eq_eval_numerals",
- prep_pats ["(m::int) = 0", "(m::int) = 1", "(m::int) = number_of v"],
+ ["(m::int) = 0", "(m::int) = 1", "(m::int) = number_of v"],
IntAbstractNumerals.proc eq_number_of_eq),
("int_less_eval_numerals",
- prep_pats ["(m::int) < 0", "(m::int) < 1", "(m::int) < number_of v"],
+ ["(m::int) < 0", "(m::int) < 1", "(m::int) < number_of v"],
IntAbstractNumerals.proc less_number_of_eq_neg),
("int_le_eval_numerals",
- prep_pats ["(m::int) <= 0", "(m::int) <= 1", "(m::int) <= number_of v"],
+ ["(m::int) <= 0", "(m::int) <= 1", "(m::int) <= number_of v"],
IntAbstractNumerals.proc le_number_of_eq_not_less)]
(*reorientation simprules using ==, for the following simproc*)
@@ -413,9 +412,7 @@
| Const("Numeral.number_of", _) $ _ => meta_number_of_reorient)
val reorient_simproc =
- prep_simproc ("reorient_simproc",
- prep_pats ["0=x", "1=x", "number_of w = x"],
- reorient_proc)
+ prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc)
end;
--- a/src/HOL/Integ/int_arith1.ML Tue Aug 06 11:20:47 2002 +0200
+++ b/src/HOL/Integ/int_arith1.ML Tue Aug 06 11:22:05 2002 +0200
@@ -34,15 +34,15 @@
(** For cancel_numerals **)
val rel_iff_rel_0_rls = map (inst "y" "?u+?v")
- [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
- zle_iff_zdiff_zle_0] @
- map (inst "y" "n")
- [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
- zle_iff_zdiff_zle_0];
+ [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
+ zle_iff_zdiff_zle_0] @
+ map (inst "y" "n")
+ [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
+ zle_iff_zdiff_zle_0];
Goal "!!i::int. (i*u + m = j*u + n) = ((i-j)*u + m = n)";
by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
- zadd_ac@rel_iff_rel_0_rls) 1);
+ zadd_ac@rel_iff_rel_0_rls) 1);
qed "eq_add_iff1";
Goal "!!i::int. (i*u + m = j*u + n) = (m = (j-i)*u + n)";
@@ -79,7 +79,7 @@
val numeral_syms = [int_numeral_0_eq_0 RS sym, int_numeral_1_eq_1 RS sym];
val numeral_sym_ss = HOL_ss addsimps numeral_syms;
-fun rename_numerals th =
+fun rename_numerals th =
simplify numeral_sym_ss (Thm.transfer (the_context ()) th);
(*Utilities*)
@@ -89,14 +89,14 @@
(*Decodes a binary INTEGER*)
fun dest_numeral (Const("0", _)) = 0
| dest_numeral (Const("1", _)) = 1
- | dest_numeral (Const("Numeral.number_of", _) $ w) =
+ | dest_numeral (Const("Numeral.number_of", _) $ w) =
(HOLogic.dest_binum w
handle TERM _ => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
| dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
fun find_first_numeral past (t::terms) =
- ((dest_numeral t, rev past @ terms)
- handle TERM _ => find_first_numeral (t::past) terms)
+ ((dest_numeral t, rev past @ terms)
+ handle TERM _ => find_first_numeral (t::past) terms)
| find_first_numeral past [] = raise TERM("find_first_numeral", []);
val zero = mk_numeral 0;
@@ -121,7 +121,7 @@
| dest_summing (pos, Const ("op -", _) $ t $ u, ts) =
dest_summing (pos, t, dest_summing (not pos, u, ts))
| dest_summing (pos, t, ts) =
- if pos then t::ts else uminus_const$t :: ts;
+ if pos then t::ts else uminus_const$t :: ts;
fun dest_sum t = dest_summing (true, t, []);
@@ -139,29 +139,29 @@
val dest_times = HOLogic.dest_bin "op *" HOLogic.intT;
fun dest_prod t =
- let val (t,u) = dest_times t
+ let val (t,u) = dest_times t
in dest_prod t @ dest_prod u end
handle TERM _ => [t];
-(*DON'T do the obvious simplifications; that would create special cases*)
+(*DON'T do the obvious simplifications; that would create special cases*)
fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts);
(*Express t as a product of (possibly) a numeral with other sorted terms*)
fun dest_coeff sign (Const ("uminus", _) $ t) = dest_coeff (~sign) t
| dest_coeff sign t =
let val ts = sort Term.term_ord (dest_prod t)
- val (n, ts') = find_first_numeral [] ts
+ val (n, ts') = find_first_numeral [] ts
handle TERM _ => (1, ts)
in (sign*n, mk_prod ts') end;
(*Find first coefficient-term THAT MATCHES u*)
-fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
+fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
| find_first_coeff past u (t::terms) =
- let val (n,u') = dest_coeff 1 t
- in if u aconv u' then (n, rev past @ terms)
- else find_first_coeff (t::past) u terms
- end
- handle TERM _ => find_first_coeff (t::past) u terms;
+ let val (n,u') = dest_coeff 1 t
+ in if u aconv u' then (n, rev past @ terms)
+ else find_first_coeff (t::past) u terms
+ end
+ handle TERM _ => find_first_coeff (t::past) u terms;
(*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1*)
@@ -172,24 +172,24 @@
(*To perform binary arithmetic. The "left" rewriting handles patterns
created by the simprocs, such as 3 * (5 * x). *)
val bin_simps = [int_numeral_0_eq_0 RS sym, int_numeral_1_eq_1 RS sym,
- add_number_of_left, mult_number_of_left] @
+ add_number_of_left, mult_number_of_left] @
bin_arith_simps @ bin_rel_simps;
(*To evaluate binary negations of coefficients*)
val zminus_simps = NCons_simps @
- [zminus_1_eq_m1, number_of_minus RS sym,
- bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
- bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
+ [zminus_1_eq_m1, number_of_minus RS sym,
+ bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
+ bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
(*To let us treat subtraction as addition*)
val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus];
(*push the unary minus down: - x * y = x * - y *)
-val int_minus_mult_eq_1_to_2 =
+val int_minus_mult_eq_1_to_2 =
[zmult_zminus, zmult_zminus_right RS sym] MRS trans |> standard;
(*to extract again any uncancelled minuses*)
-val int_minus_from_mult_simps =
+val int_minus_from_mult_simps =
[zminus_zminus, zmult_zminus, zmult_zminus_right];
(*combine unary minus with numeric literals, however nested within a product*)
@@ -206,19 +206,19 @@
structure CancelNumeralsCommon =
struct
- val mk_sum = mk_sum
- val dest_sum = dest_sum
- val mk_coeff = mk_coeff
- val dest_coeff = dest_coeff 1
- val find_first_coeff = find_first_coeff []
+ val mk_sum = mk_sum
+ val dest_sum = dest_sum
+ val mk_coeff = mk_coeff
+ val dest_coeff = dest_coeff 1
+ val find_first_coeff = find_first_coeff []
val trans_tac = trans_tac
- val norm_tac =
+ val norm_tac =
ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
diff_simps@zminus_simps@zadd_ac))
THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps))
THEN ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@
zadd_ac@zmult_ac))
- val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
+ val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s)
end;
@@ -250,55 +250,51 @@
val bal_add2 = le_add_iff2 RS trans
);
-val cancel_numerals =
+val cancel_numerals =
map Bin_Simprocs.prep_simproc
[("inteq_cancel_numerals",
- Bin_Simprocs.prep_pats
- ["(l::int) + m = n", "(l::int) = m + n",
- "(l::int) - m = n", "(l::int) = m - n",
- "(l::int) * m = n", "(l::int) = m * n"],
+ ["(l::int) + m = n", "(l::int) = m + n",
+ "(l::int) - m = n", "(l::int) = m - n",
+ "(l::int) * m = n", "(l::int) = m * n"],
EqCancelNumerals.proc),
- ("intless_cancel_numerals",
- Bin_Simprocs.prep_pats
- ["(l::int) + m < n", "(l::int) < m + n",
- "(l::int) - m < n", "(l::int) < m - n",
- "(l::int) * m < n", "(l::int) < m * n"],
+ ("intless_cancel_numerals",
+ ["(l::int) + m < n", "(l::int) < m + n",
+ "(l::int) - m < n", "(l::int) < m - n",
+ "(l::int) * m < n", "(l::int) < m * n"],
LessCancelNumerals.proc),
- ("intle_cancel_numerals",
- Bin_Simprocs.prep_pats
- ["(l::int) + m <= n", "(l::int) <= m + n",
- "(l::int) - m <= n", "(l::int) <= m - n",
- "(l::int) * m <= n", "(l::int) <= m * n"],
+ ("intle_cancel_numerals",
+ ["(l::int) + m <= n", "(l::int) <= m + n",
+ "(l::int) - m <= n", "(l::int) <= m - n",
+ "(l::int) * m <= n", "(l::int) <= m * n"],
LeCancelNumerals.proc)];
structure CombineNumeralsData =
struct
- val add = op + : int*int -> int
- val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *)
- val dest_sum = dest_sum
- val mk_coeff = mk_coeff
- val dest_coeff = dest_coeff 1
- val left_distrib = left_zadd_zmult_distrib RS trans
+ val add = op + : int*int -> int
+ val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *)
+ val dest_sum = dest_sum
+ val mk_coeff = mk_coeff
+ val dest_coeff = dest_coeff 1
+ val left_distrib = left_zadd_zmult_distrib RS trans
val prove_conv = Bin_Simprocs.prove_conv_nohyps "int_combine_numerals"
val trans_tac = trans_tac
- val norm_tac =
+ val norm_tac =
ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
diff_simps@zminus_simps@zadd_ac))
THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps))
THEN ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@
zadd_ac@zmult_ac))
- val numeral_simp_tac = ALLGOALS
+ val numeral_simp_tac = ALLGOALS
(simp_tac (HOL_ss addsimps add_0s@bin_simps))
val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s)
end;
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
-
-val combine_numerals = Bin_Simprocs.prep_simproc
- ("int_combine_numerals",
- Bin_Simprocs.prep_pats ["(i::int) + j", "(i::int) - j"],
- CombineNumerals.proc);
+
+val combine_numerals =
+ Bin_Simprocs.prep_simproc
+ ("int_combine_numerals", ["(i::int) + j", "(i::int) - j"], CombineNumerals.proc);
end;
@@ -312,7 +308,7 @@
print_depth 22;
set timing;
set trace_simp;
-fun test s = (Goal s, by (Simp_tac 1));
+fun test s = (Goal s, by (Simp_tac 1));
test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)";
@@ -355,10 +351,10 @@
structure Int_Times_Assoc_Data : ASSOC_FOLD_DATA =
struct
- val ss = HOL_ss
- val eq_reflection = eq_reflection
+ val ss = HOL_ss
+ val eq_reflection = eq_reflection
val sg_ref = Sign.self_ref (Theory.sign_of (the_context ()))
- val T = HOLogic.intT
+ val T = HOLogic.intT
val plus = Const ("op *", [HOLogic.intT,HOLogic.intT] ---> HOLogic.intT);
val add_ac = zmult_ac
end;
@@ -372,10 +368,10 @@
structure Nat_Times_Assoc_Data : ASSOC_FOLD_DATA =
struct
- val ss = HOL_ss
- val eq_reflection = eq_reflection
+ val ss = HOL_ss
+ val eq_reflection = eq_reflection
val sg_ref = Sign.self_ref (Theory.sign_of (the_context ()))
- val T = HOLogic.natT
+ val T = HOLogic.natT
val plus = Const ("op *", [HOLogic.natT,HOLogic.natT] ---> HOLogic.natT);
val add_ac = mult_ac
end;
@@ -399,19 +395,19 @@
local
(* reduce contradictory <= to False *)
-val add_rules =
- simp_thms @ bin_arith_simps @ bin_rel_simps @
+val add_rules =
+ simp_thms @ bin_arith_simps @ bin_rel_simps @
[int_numeral_0_eq_0, int_numeral_1_eq_1,
zminus_0, zadd_0, zadd_0_right, zdiff_def,
- zadd_zminus_inverse, zadd_zminus_inverse2,
- zmult_0, zmult_0_right,
+ zadd_zminus_inverse, zadd_zminus_inverse2,
+ zmult_0, zmult_0_right,
zmult_1, zmult_1_right,
zmult_zminus, zmult_zminus_right,
zminus_zadd_distrib, zminus_zminus, zmult_assoc,
int_0, int_1, zadd_int RS sym, int_Suc];
val simprocs = [Int_Times_Assoc.conv, Int_Numeral_Simprocs.combine_numerals]@
- Int_Numeral_Simprocs.cancel_numerals @
+ Int_Numeral_Simprocs.cancel_numerals @
Bin_Simprocs.eval_numerals;
val add_mono_thms_int =
@@ -440,16 +436,12 @@
end;
-let
-val int_arith_simproc_pats =
- map (fn s => Thm.read_cterm (Theory.sign_of (the_context())) (s, HOLogic.boolT))
- ["(m::int) < n","(m::int) <= n", "(m::int) = n"];
+val fast_int_arith_simproc =
+ Simplifier.simproc (Theory.sign_of (the_context()))
+ "fast_int_arith" ["(m::int) < n","(m::int) <= n", "(m::int) = n"] Fast_Arith.lin_arith_prover;
-val fast_int_arith_simproc = mk_simproc
- "fast_int_arith" int_arith_simproc_pats Fast_Arith.lin_arith_prover;
-in
Addsimprocs [fast_int_arith_simproc]
-end;
+
(* Some test data
Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
--- a/src/HOL/Integ/int_factor_simprocs.ML Tue Aug 06 11:20:47 2002 +0200
+++ b/src/HOL/Integ/int_factor_simprocs.ML Tue Aug 06 11:22:05 2002 +0200
@@ -12,26 +12,26 @@
Goal "!!k::int. (k*m <= k*n) = ((0 < k --> m<=n) & (k < 0 --> n<=m))";
by (stac zmult_zle_cancel1 1);
-by Auto_tac;
+by Auto_tac;
qed "int_mult_le_cancel1";
Goal "!!k::int. (k*m < k*n) = ((0 < k & m<n) | (k < 0 & n<m))";
by (stac zmult_zless_cancel1 1);
-by Auto_tac;
+by Auto_tac;
qed "int_mult_less_cancel1";
Goal "!!k::int. (k*m = k*n) = (k = 0 | m=n)";
-by Auto_tac;
+by Auto_tac;
qed "int_mult_eq_cancel1";
Goal "!!k::int. k~=0 ==> (k*m) div (k*n) = (m div n)";
-by (stac zdiv_zmult_zmult1 1);
-by Auto_tac;
+by (stac zdiv_zmult_zmult1 1);
+by Auto_tac;
qed "int_mult_div_cancel1";
(*For ExtractCommonTermFun, cancelling common factors*)
Goal "(k*m) div (k*n) = (if k = (0::int) then 0 else m div n)";
-by (simp_tac (simpset() addsimps [int_mult_div_cancel1]) 1);
+by (simp_tac (simpset() addsimps [int_mult_div_cancel1]) 1);
qed "int_mult_div_cancel_disj";
local
@@ -40,15 +40,15 @@
structure CancelNumeralFactorCommon =
struct
- val mk_coeff = mk_coeff
- val dest_coeff = dest_coeff 1
+ val mk_coeff = mk_coeff
+ val dest_coeff = dest_coeff 1
val trans_tac = trans_tac
- val norm_tac =
+ val norm_tac =
ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@mult_1s))
THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps))
THEN ALLGOALS
(simp_tac (HOL_ss addsimps zmult_ac))
- val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
+ val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
val simplify_meta_eq = simplify_meta_eq mult_1s
end
@@ -88,19 +88,15 @@
val neg_exchanges = true
)
-val int_cancel_numeral_factors =
+val int_cancel_numeral_factors =
map Bin_Simprocs.prep_simproc
- [("inteq_cancel_numeral_factors",
- Bin_Simprocs.prep_pats ["(l::int) * m = n", "(l::int) = m * n"],
+ [("inteq_cancel_numeral_factors", ["(l::int) * m = n", "(l::int) = m * n"],
EqCancelNumeralFactor.proc),
- ("intless_cancel_numeral_factors",
- Bin_Simprocs.prep_pats ["(l::int) * m < n", "(l::int) < m * n"],
+ ("intless_cancel_numeral_factors", ["(l::int) * m < n", "(l::int) < m * n"],
LessCancelNumeralFactor.proc),
- ("intle_cancel_numeral_factors",
- Bin_Simprocs.prep_pats ["(l::int) * m <= n", "(l::int) <= m * n"],
+ ("intle_cancel_numeral_factors", ["(l::int) * m <= n", "(l::int) <= m * n"],
LeCancelNumeralFactor.proc),
- ("intdiv_cancel_numeral_factors",
- Bin_Simprocs.prep_pats ["((l::int) * m) div n", "(l::int) div (m * n)"],
+ ("intdiv_cancel_numeral_factors", ["((l::int) * m) div n", "(l::int) div (m * n)"],
DivCancelNumeralFactor.proc)];
end;
@@ -112,7 +108,7 @@
print_depth 22;
set timing;
set trace_simp;
-fun test s = (Goal s; by (Simp_tac 1));
+fun test s = (Goal s; by (Simp_tac 1));
test "9*x = 12 * (y::int)";
test "(9*x) div (12 * (y::int)) = z";
@@ -156,25 +152,25 @@
| long_mk_prod (t :: ts) = mk_times (t, mk_prod ts);
(*Find first term that matches u*)
-fun find_first past u [] = raise TERM("find_first", [])
+fun find_first past u [] = raise TERM("find_first", [])
| find_first past u (t::terms) =
- if u aconv t then (rev past @ terms)
+ if u aconv t then (rev past @ terms)
else find_first (t::past) u terms
- handle TERM _ => find_first (t::past) u terms;
+ handle TERM _ => find_first (t::past) u terms;
(*Final simplification: cancel + and * *)
-fun cancel_simplify_meta_eq cancel_th th =
- Int_Numeral_Simprocs.simplify_meta_eq
- [zmult_1, zmult_1_right]
+fun cancel_simplify_meta_eq cancel_th th =
+ Int_Numeral_Simprocs.simplify_meta_eq
+ [zmult_1, zmult_1_right]
(([th, cancel_th]) MRS trans);
structure CancelFactorCommon =
struct
- val mk_sum = long_mk_prod
- val dest_sum = dest_prod
- val mk_coeff = mk_coeff
- val dest_coeff = dest_coeff
- val find_first = find_first []
+ val mk_sum = long_mk_prod
+ val dest_sum = dest_prod
+ val mk_coeff = mk_coeff
+ val dest_coeff = dest_coeff
+ val find_first = find_first []
val trans_tac = trans_tac
val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@zmult_ac))
end;
@@ -195,13 +191,10 @@
val simplify_meta_eq = cancel_simplify_meta_eq int_mult_div_cancel_disj
);
-val int_cancel_factor =
+val int_cancel_factor =
map Bin_Simprocs.prep_simproc
- [("int_eq_cancel_factor",
- Bin_Simprocs.prep_pats ["(l::int) * m = n", "(l::int) = m * n"],
- EqCancelFactor.proc),
- ("int_divide_cancel_factor",
- Bin_Simprocs.prep_pats ["((l::int) * m) div n", "(l::int) div (m * n)"],
+ [("int_eq_cancel_factor", ["(l::int) * m = n", "(l::int) = m * n"], EqCancelFactor.proc),
+ ("int_divide_cancel_factor", ["((l::int) * m) div n", "(l::int) div (m * n)"],
DivideCancelFactor.proc)];
end;
@@ -213,15 +206,15 @@
print_depth 22;
set timing;
set trace_simp;
-fun test s = (Goal s; by (Asm_simp_tac 1));
+fun test s = (Goal s; by (Asm_simp_tac 1));
test "x*k = k*(y::int)";
-test "k = k*(y::int)";
+test "k = k*(y::int)";
test "a*(b*c) = (b::int)";
test "a*(b*c) = d*(b::int)*(x*a)";
test "(x*k) div (k*(y::int)) = (uu::int)";
-test "(k) div (k*(y::int)) = (uu::int)";
+test "(k) div (k*(y::int)) = (uu::int)";
test "(a*(b*c)) div ((b::int)) = (uu::int)";
test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)";
*)
--- a/src/HOL/Integ/nat_bin.ML Tue Aug 06 11:20:47 2002 +0200
+++ b/src/HOL/Integ/nat_bin.ML Tue Aug 06 11:22:05 2002 +0200
@@ -238,12 +238,8 @@
val nat_eval_numerals =
map Bin_Simprocs.prep_simproc
- [("nat_div_eval_numerals",
- Bin_Simprocs.prep_pats ["(Suc 0) div m"],
- NatAbstractNumerals.proc div_nat_number_of),
- ("nat_mod_eval_numerals",
- Bin_Simprocs.prep_pats ["(Suc 0) mod m"],
- NatAbstractNumerals.proc mod_nat_number_of)];
+ [("nat_div_eval_numerals", ["(Suc 0) div m"], NatAbstractNumerals.proc div_nat_number_of),
+ ("nat_mod_eval_numerals", ["(Suc 0) mod m"], NatAbstractNumerals.proc mod_nat_number_of)];
Addsimprocs nat_eval_numerals;
--- a/src/HOL/Integ/nat_simprocs.ML Tue Aug 06 11:20:47 2002 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML Tue Aug 06 11:22:05 2002 +0200
@@ -67,38 +67,38 @@
(** For cancel_numeral_factors **)
Goal "(0::nat) < k ==> (k*m <= k*n) = (m<=n)";
-by Auto_tac;
+by Auto_tac;
qed "nat_mult_le_cancel1";
Goal "(0::nat) < k ==> (k*m < k*n) = (m<n)";
-by Auto_tac;
+by Auto_tac;
qed "nat_mult_less_cancel1";
Goal "(0::nat) < k ==> (k*m = k*n) = (m=n)";
-by Auto_tac;
+by Auto_tac;
qed "nat_mult_eq_cancel1";
Goal "(0::nat) < k ==> (k*m) div (k*n) = (m div n)";
-by Auto_tac;
+by Auto_tac;
qed "nat_mult_div_cancel1";
(** For cancel_factor **)
Goal "(k*m <= k*n) = ((0::nat) < k --> m<=n)";
-by Auto_tac;
+by Auto_tac;
qed "nat_mult_le_cancel_disj";
Goal "(k*m < k*n) = ((0::nat) < k & m<n)";
-by Auto_tac;
+by Auto_tac;
qed "nat_mult_less_cancel_disj";
Goal "(k*m = k*n) = (k = (0::nat) | m=n)";
-by Auto_tac;
+by Auto_tac;
qed "nat_mult_eq_cancel_disj";
Goal "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)";
-by (simp_tac (simpset() addsimps [nat_mult_div_cancel1]) 1);
+by (simp_tac (simpset() addsimps [nat_mult_div_cancel1]) 1);
qed "nat_mult_div_cancel_disj";
@@ -110,7 +110,7 @@
[numeral_0_eq_0 RS sym, numeral_1_eq_1 RS sym, numeral_2_eq_2 RS sym];
val numeral_sym_ss = HOL_ss addsimps numeral_syms;
-fun rename_numerals th =
+fun rename_numerals th =
simplify numeral_sym_ss (Thm.transfer (the_context ()) th);
(*Utilities*)
@@ -164,13 +164,12 @@
val bin_simps = [numeral_0_eq_0 RS sym, numeral_1_eq_1 RS sym,
add_nat_number_of, nat_number_of_add_left,
diff_nat_number_of, le_nat_number_of_eq_not_less,
- less_nat_number_of, mult_nat_number_of,
+ less_nat_number_of, mult_nat_number_of,
thm "Let_number_of", nat_number_of] @
bin_arith_simps @ bin_rel_simps;
-fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
-fun prep_pat s = HOLogic.read_cterm (Theory.sign_of (the_context ())) s;
-val prep_pats = map prep_pat;
+fun prep_simproc (name, pats, proc) =
+ Simplifier.simproc (Theory.sign_of (the_context ())) name pats proc;
(*** CancelNumerals simprocs ***)
@@ -218,7 +217,7 @@
(*And these help the simproc return False when appropriate, which helps
the arith prover.*)
-val contra_rules = [add_Suc, add_Suc_right, Zero_not_Suc, Suc_not_Zero,
+val contra_rules = [add_Suc, add_Suc_right, Zero_not_Suc, Suc_not_Zero,
le_0_eq];
val simplify_meta_eq =
@@ -240,7 +239,7 @@
fun prod_has_numeral t = exists is_numeral (dest_prod t);
-fun restricted_dest_Sucs_sum t =
+fun restricted_dest_Sucs_sum t =
if exists prod_has_numeral (dest_sum (ignore_Sucs t))
then dest_Sucs_sum t
else raise TERM("Nat_Numeral_Simprocs.restricted_dest_Sucs_sum", [t]);
@@ -307,24 +306,24 @@
val cancel_numerals =
map prep_simproc
[("nateq_cancel_numerals",
- prep_pats ["(l::nat) + m = n", "(l::nat) = m + n",
- "(l::nat) * m = n", "(l::nat) = m * n",
- "Suc m = n", "m = Suc n"],
+ ["(l::nat) + m = n", "(l::nat) = m + n",
+ "(l::nat) * m = n", "(l::nat) = m * n",
+ "Suc m = n", "m = Suc n"],
EqCancelNumerals.proc),
("natless_cancel_numerals",
- prep_pats ["(l::nat) + m < n", "(l::nat) < m + n",
- "(l::nat) * m < n", "(l::nat) < m * n",
- "Suc m < n", "m < Suc n"],
+ ["(l::nat) + m < n", "(l::nat) < m + n",
+ "(l::nat) * m < n", "(l::nat) < m * n",
+ "Suc m < n", "m < Suc n"],
LessCancelNumerals.proc),
("natle_cancel_numerals",
- prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n",
- "(l::nat) * m <= n", "(l::nat) <= m * n",
- "Suc m <= n", "m <= Suc n"],
+ ["(l::nat) + m <= n", "(l::nat) <= m + n",
+ "(l::nat) * m <= n", "(l::nat) <= m * n",
+ "Suc m <= n", "m <= Suc n"],
LeCancelNumerals.proc),
("natdiff_cancel_numerals",
- prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)",
- "(l::nat) * m - n", "(l::nat) - m * n",
- "Suc m - n", "m - Suc n"],
+ ["((l::nat) + m) - n", "(l::nat) - (m + n)",
+ "(l::nat) * m - n", "(l::nat) - m * n",
+ "Suc m - n", "m - Suc n"],
DiffCancelNumerals.proc)];
@@ -332,13 +331,13 @@
structure CombineNumeralsData =
struct
- val add = op + : int*int -> int
+ val add = op + : int*int -> int
val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *)
val dest_sum = restricted_dest_Sucs_sum
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
val left_distrib = left_add_mult_distrib RS trans
- val prove_conv = Bin_Simprocs.prove_conv_nohyps "nat_combine_numerals"
+ val prove_conv = Bin_Simprocs.prove_conv_nohyps "nat_combine_numerals"
val trans_tac = trans_tac
val norm_tac = ALLGOALS
(simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
@@ -353,22 +352,20 @@
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
val combine_numerals =
- prep_simproc ("nat_combine_numerals",
- prep_pats ["(i::nat) + j", "Suc (i + j)"],
- CombineNumerals.proc);
+ prep_simproc ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], CombineNumerals.proc);
(*** Applying CancelNumeralFactorFun ***)
structure CancelNumeralFactorCommon =
struct
- val mk_coeff = mk_coeff
- val dest_coeff = dest_coeff
+ val mk_coeff = mk_coeff
+ val dest_coeff = dest_coeff
val trans_tac = trans_tac
- val norm_tac = ALLGOALS
+ val norm_tac = ALLGOALS
(simp_tac (HOL_ss addsimps [Suc_eq_add_numeral_1]@mult_1s))
THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@mult_ac))
- val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
+ val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
val simplify_meta_eq = simplify_meta_eq
end
@@ -408,19 +405,19 @@
val neg_exchanges = true
)
-val cancel_numeral_factors =
+val cancel_numeral_factors =
map prep_simproc
[("nateq_cancel_numeral_factors",
- prep_pats ["(l::nat) * m = n", "(l::nat) = m * n"],
+ ["(l::nat) * m = n", "(l::nat) = m * n"],
EqCancelNumeralFactor.proc),
- ("natless_cancel_numeral_factors",
- prep_pats ["(l::nat) * m < n", "(l::nat) < m * n"],
+ ("natless_cancel_numeral_factors",
+ ["(l::nat) * m < n", "(l::nat) < m * n"],
LessCancelNumeralFactor.proc),
- ("natle_cancel_numeral_factors",
- prep_pats ["(l::nat) * m <= n", "(l::nat) <= m * n"],
+ ("natle_cancel_numeral_factors",
+ ["(l::nat) * m <= n", "(l::nat) <= m * n"],
LeCancelNumeralFactor.proc),
- ("natdiv_cancel_numeral_factors",
- prep_pats ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
+ ("natdiv_cancel_numeral_factors",
+ ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
DivCancelNumeralFactor.proc)];
@@ -432,24 +429,24 @@
| long_mk_prod (t :: ts) = mk_times (t, mk_prod ts);
(*Find first term that matches u*)
-fun find_first past u [] = raise TERM("find_first", [])
+fun find_first past u [] = raise TERM("find_first", [])
| find_first past u (t::terms) =
- if u aconv t then (rev past @ terms)
+ if u aconv t then (rev past @ terms)
else find_first (t::past) u terms
- handle TERM _ => find_first (t::past) u terms;
+ handle TERM _ => find_first (t::past) u terms;
(*Final simplification: cancel + and * *)
-fun cancel_simplify_meta_eq cancel_th th =
- Int_Numeral_Simprocs.simplify_meta_eq [zmult_1, zmult_1_right]
+fun cancel_simplify_meta_eq cancel_th th =
+ Int_Numeral_Simprocs.simplify_meta_eq [zmult_1, zmult_1_right]
(([th, cancel_th]) MRS trans);
structure CancelFactorCommon =
struct
- val mk_sum = long_mk_prod
- val dest_sum = dest_prod
- val mk_coeff = mk_coeff
- val dest_coeff = dest_coeff
- val find_first = find_first []
+ val mk_sum = long_mk_prod
+ val dest_sum = dest_prod
+ val mk_coeff = mk_coeff
+ val dest_coeff = dest_coeff
+ val find_first = find_first []
val trans_tac = trans_tac
val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@mult_ac))
end;
@@ -486,19 +483,19 @@
val simplify_meta_eq = cancel_simplify_meta_eq nat_mult_div_cancel_disj
);
-val cancel_factor =
+val cancel_factor =
map prep_simproc
[("nat_eq_cancel_factor",
- prep_pats ["(l::nat) * m = n", "(l::nat) = m * n"],
+ ["(l::nat) * m = n", "(l::nat) = m * n"],
EqCancelFactor.proc),
("nat_less_cancel_factor",
- prep_pats ["(l::nat) * m < n", "(l::nat) < m * n"],
+ ["(l::nat) * m < n", "(l::nat) < m * n"],
LessCancelFactor.proc),
("nat_le_cancel_factor",
- prep_pats ["(l::nat) * m <= n", "(l::nat) <= m * n"],
+ ["(l::nat) * m <= n", "(l::nat) <= m * n"],
LeCancelFactor.proc),
- ("nat_divide_cancel_factor",
- prep_pats ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
+ ("nat_divide_cancel_factor",
+ ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
DivideCancelFactor.proc)];
end;
@@ -576,22 +573,22 @@
(*cancel_factor*)
test "x*k = k*(y::nat)";
-test "k = k*(y::nat)";
+test "k = k*(y::nat)";
test "a*(b*c) = (b::nat)";
test "a*(b*c) = d*(b::nat)*(x*a)";
test "x*k < k*(y::nat)";
-test "k < k*(y::nat)";
+test "k < k*(y::nat)";
test "a*(b*c) < (b::nat)";
test "a*(b*c) < d*(b::nat)*(x*a)";
test "x*k <= k*(y::nat)";
-test "k <= k*(y::nat)";
+test "k <= k*(y::nat)";
test "a*(b*c) <= (b::nat)";
test "a*(b*c) <= d*(b::nat)*(x*a)";
test "(x*k) div (k*(y::nat)) = (uu::nat)";
-test "(k) div (k*(y::nat)) = (uu::nat)";
+test "(k) div (k*(y::nat)) = (uu::nat)";
test "(a*(b*c)) div ((b::nat)) = (uu::nat)";
test "(a*(b*c)) div (d*(b::nat)*(x*a)) = (uu::nat)";
*)
@@ -603,7 +600,7 @@
(* reduce contradictory <= to False *)
val add_rules =
- [thm "Let_number_of", thm "Let_0", thm "Let_1", nat_0, nat_1,
+ [thm "Let_number_of", thm "Let_0", thm "Let_1", nat_0, nat_1,
add_nat_number_of, diff_nat_number_of, mult_nat_number_of,
eq_nat_number_of, less_nat_number_of, le_nat_number_of_eq_not_less,
le_Suc_number_of,le_number_of_Suc,
--- a/src/HOL/List.thy Tue Aug 06 11:20:47 2002 +0200
+++ b/src/HOL/List.thy Tue Aug 06 11:22:05 2002 +0200
@@ -1,7 +1,7 @@
-(* Title:HOL/List.thy
- ID: $Id$
- Author: Tobias Nipkow
- Copyright 1994 TU Muenchen
+(* Title: HOL/List.thy
+ ID: $Id$
+ Author: Tobias Nipkow
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
header {* The datatype of finite lists *}
@@ -367,50 +367,50 @@
val append1_eq_conv = thm "append1_eq_conv";
val append_same_eq = thm "append_same_eq";
-val list_eq_pattern =
-Thm.read_cterm (Theory.sign_of (the_context ())) ("(xs::'a list) = ys",HOLogic.boolT)
-
fun last (cons as Const("List.list.Cons",_) $ _ $ xs) =
-(case xs of Const("List.list.Nil",_) => cons | _ => last xs)
-| last (Const("List.op @",_) $ _ $ ys) = last ys
-| last t = t
+ (case xs of Const("List.list.Nil",_) => cons | _ => last xs)
+ | last (Const("List.op @",_) $ _ $ ys) = last ys
+ | last t = t;
fun list1 (Const("List.list.Cons",_) $ _ $ Const("List.list.Nil",_)) = true
-| list1 _ = false
+ | list1 _ = false;
fun butlast ((cons as Const("List.list.Cons",_) $ x) $ xs) =
-(case xs of Const("List.list.Nil",_) => xs | _ => cons $ butlast xs)
-| butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
-| butlast xs = Const("List.list.Nil",fastype_of xs)
+ (case xs of Const("List.list.Nil",_) => xs | _ => cons $ butlast xs)
+ | butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
+ | butlast xs = Const("List.list.Nil",fastype_of xs);
val rearr_tac =
-simp_tac (HOL_basic_ss addsimps [append_assoc,append_Nil,append_Cons])
+ simp_tac (HOL_basic_ss addsimps [append_assoc, append_Nil, append_Cons]);
fun list_eq sg _ (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
-let
-val lastl = last lhs and lastr = last rhs
-fun rearr conv =
-let val lhs1 = butlast lhs and rhs1 = butlast rhs
-val Type(_,listT::_) = eqT
-val appT = [listT,listT] ---> listT
-val app = Const("List.op @",appT)
-val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
-val ct = cterm_of sg (HOLogic.mk_Trueprop(HOLogic.mk_eq(F,F2)))
-val thm = prove_goalw_cterm [] ct (K [rearr_tac 1])
-handle ERROR =>
-error("The error(s) above occurred while trying to prove " ^
-string_of_cterm ct)
-in Some((conv RS (thm RS trans)) RS eq_reflection) end
+ let
+ val lastl = last lhs and lastr = last rhs;
+ fun rearr conv =
+ let
+ val lhs1 = butlast lhs and rhs1 = butlast rhs;
+ val Type(_,listT::_) = eqT
+ val appT = [listT,listT] ---> listT
+ val app = Const("List.op @",appT)
+ val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
+ val ct = cterm_of sg (HOLogic.mk_Trueprop(HOLogic.mk_eq(F,F2)))
+ val thm = prove_goalw_cterm [] ct (K [rearr_tac 1])
+ handle ERROR =>
+ error("The error(s) above occurred while trying to prove " ^
+ string_of_cterm ct);
+ in Some ((conv RS (thm RS trans)) RS eq_reflection) end;
-in if list1 lastl andalso list1 lastr
- then rearr append1_eq_conv
- else
- if lastl aconv lastr
- then rearr append_same_eq
- else None
-end
+ in
+ if list1 lastl andalso list1 lastr then rearr append1_eq_conv
+ else if lastl aconv lastr then rearr append_same_eq
+ else None
+ end;
+
in
-val list_eq_simproc = mk_simproc "list_eq" [list_eq_pattern] list_eq
+
+val list_eq_simproc =
+ Simplifier.simproc (Theory.sign_of (the_context ())) "list_eq" ["(xs::'a list) = ys"] list_eq;
+
end;
Addsimprocs [list_eq_simproc];
@@ -1364,6 +1364,7 @@
drop_Cons'[of "number_of v",standard]
nth_Cons'[of _ _ "number_of v",standard]
+
subsection {* Characters and strings *}
datatype nibble =
--- a/src/HOL/Modelcheck/EindhovenSyn.ML Tue Aug 06 11:20:47 2002 +0200
+++ b/src/HOL/Modelcheck/EindhovenSyn.ML Tue Aug 06 11:22:05 2002 +0200
@@ -24,16 +24,9 @@
by (rtac refl 1);
qed "pair_eta_expand";
-local
- val lhss = [read_cterm (sign_of thy) ("f::'a*'b=>'c", TVar (("'a", 0), []))];
- val rew = mk_meta_eq pair_eta_expand;
-
- fun proc _ _ (Abs _) = Some rew
- | proc _ _ _ = None;
-in
- val pair_eta_expand_proc = Simplifier.mk_simproc "pair_eta_expand" lhss proc;
-end;
-
+val pair_eta_expand_proc =
+ Simplifier.simproc (Theory.sign_of (the_context ())) "pair_eta_expand" ["f::'a*'b=>'c"]
+ (fn _ => fn _ => fn t => case t of Abs _ => Some (mk_meta_eq pair_eta_expand) | _ => None);
val Eindhoven_ss =
simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
--- a/src/HOL/Modelcheck/MuckeSyn.ML Tue Aug 06 11:20:47 2002 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.ML Tue Aug 06 11:22:05 2002 +0200
@@ -153,16 +153,9 @@
by (rtac refl 1);
qed "pair_eta_expand";
-local
- val lhss = [read_cterm (sign_of thy) ("f::'a*'b=>'c", TVar (("'a", 0), []))];
- val rew = mk_meta_eq pair_eta_expand;
-
- fun proc _ _ (Abs _) = Some rew
- | proc _ _ _ = None;
-in
- val pair_eta_expand_proc = Simplifier.mk_simproc "pair_eta_expand" lhss proc;
-end;
-
+val pair_eta_expand_proc =
+ Simplifier.simproc (Theory.sign_of (the_context ())) "pair_eta_expand" ["f::'a*'b=>'c"]
+ (fn _ => fn _ => fn t => case t of Abs _ => Some (mk_meta_eq pair_eta_expand) | _ => None);
val Mucke_ss = simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
--- a/src/HOL/Product_Type.thy Tue Aug 06 11:20:47 2002 +0200
+++ b/src/HOL/Product_Type.thy Tue Aug 06 11:22:05 2002 +0200
@@ -29,13 +29,11 @@
*}
ML_setup {*
- local
- val unit_pat = Thm.cterm_of (Theory.sign_of (the_context ())) (Free ("x", HOLogic.unitT));
- val unit_meta_eq = standard (mk_meta_eq (thm "unit_eq"));
- fun proc _ _ t =
- if HOLogic.is_unit t then None
- else Some unit_meta_eq
- in val unit_eq_proc = Simplifier.mk_simproc "unit_eq" [unit_pat] proc end;
+ val unit_eq_proc =
+ let val unit_meta_eq = mk_meta_eq (thm "unit_eq") in
+ Simplifier.simproc (Theory.sign_of (the_context ())) "unit_eq" ["x::unit"]
+ (fn _ => fn _ => fn t => if HOLogic.is_unit t then None else Some unit_meta_eq)
+ end;
Addsimprocs [unit_eq_proc];
*}
@@ -341,12 +339,7 @@
fun metaeq sg lhs rhs = mk_meta_eq (prove_goalw_cterm []
(cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs))))
(K [simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1]));
- val sign = sign_of (the_context ());
- fun simproc name patstr =
- Simplifier.mk_simproc name [HOLogic.read_cterm sign patstr];
- val beta_patstr = "split f z";
- val eta_patstr = "split f";
fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t
| beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse
(beta_term_pat k i t andalso beta_term_pat k i u)
@@ -368,8 +361,10 @@
| None => None)
| eta_proc _ _ _ = None;
in
- val split_beta_proc = simproc "split_beta" beta_patstr beta_proc;
- val split_eta_proc = simproc "split_eta" eta_patstr eta_proc;
+ val split_beta_proc = Simplifier.simproc (Theory.sign_of (the_context ()))
+ "split_beta" ["split f z"] beta_proc;
+ val split_eta_proc = Simplifier.simproc (Theory.sign_of (the_context ()))
+ "split_eta" ["split f"] eta_proc;
end;
Addsimprocs [split_beta_proc, split_eta_proc];
--- a/src/HOL/Real/RealArith0.ML Tue Aug 06 11:20:47 2002 +0200
+++ b/src/HOL/Real/RealArith0.ML Tue Aug 06 11:22:05 2002 +0200
@@ -9,50 +9,50 @@
*)
Goal "x - - y = x + (y::real)";
-by (Simp_tac 1);
+by (Simp_tac 1);
qed "real_diff_minus_eq";
Addsimps [real_diff_minus_eq];
(** Division and inverse **)
Goal "0/x = (0::real)";
-by (simp_tac (simpset() addsimps [real_divide_def]) 1);
+by (simp_tac (simpset() addsimps [real_divide_def]) 1);
qed "real_0_divide";
Addsimps [real_0_divide];
Goal "((0::real) < inverse x) = (0 < x)";
by (case_tac "x=0" 1);
-by (asm_simp_tac (HOL_ss addsimps [INVERSE_ZERO]) 1);
-by (auto_tac (claset() addDs [real_inverse_less_0],
- simpset() addsimps [linorder_neq_iff, real_inverse_gt_0]));
+by (asm_simp_tac (HOL_ss addsimps [INVERSE_ZERO]) 1);
+by (auto_tac (claset() addDs [real_inverse_less_0],
+ simpset() addsimps [linorder_neq_iff, real_inverse_gt_0]));
qed "real_0_less_inverse_iff";
Addsimps [real_0_less_inverse_iff];
Goal "(inverse x < (0::real)) = (x < 0)";
by (case_tac "x=0" 1);
-by (asm_simp_tac (HOL_ss addsimps [INVERSE_ZERO]) 1);
-by (auto_tac (claset() addDs [real_inverse_less_0],
- simpset() addsimps [linorder_neq_iff, real_inverse_gt_0]));
+by (asm_simp_tac (HOL_ss addsimps [INVERSE_ZERO]) 1);
+by (auto_tac (claset() addDs [real_inverse_less_0],
+ simpset() addsimps [linorder_neq_iff, real_inverse_gt_0]));
qed "real_inverse_less_0_iff";
Addsimps [real_inverse_less_0_iff];
Goal "((0::real) <= inverse x) = (0 <= x)";
-by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
+by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
qed "real_0_le_inverse_iff";
Addsimps [real_0_le_inverse_iff];
Goal "(inverse x <= (0::real)) = (x <= 0)";
-by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
+by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
qed "real_inverse_le_0_iff";
Addsimps [real_inverse_le_0_iff];
Goalw [real_divide_def] "x/(0::real) = 0";
-by (stac INVERSE_ZERO 1);
-by (Simp_tac 1);
+by (stac INVERSE_ZERO 1);
+by (Simp_tac 1);
qed "REAL_DIVIDE_ZERO";
Goal "inverse (x::real) = 1/x";
-by (simp_tac (simpset() addsimps [real_divide_def]) 1);
+by (simp_tac (simpset() addsimps [real_divide_def]) 1);
qed "real_inverse_eq_divide";
Goal "((0::real) < x/y) = (0 < x & 0 < y | x < 0 & y < 0)";
@@ -67,31 +67,31 @@
Goal "((0::real) <= x/y) = ((x <= 0 | 0 <= y) & (0 <= x | y <= 0))";
by (simp_tac (simpset() addsimps [real_divide_def, real_0_le_mult_iff]) 1);
-by Auto_tac;
+by Auto_tac;
qed "real_0_le_divide_iff";
Addsimps [inst "x" "number_of ?w" real_0_le_divide_iff];
Goal "(x/y <= (0::real)) = ((x <= 0 | y <= 0) & (0 <= x | 0 <= y))";
by (simp_tac (simpset() addsimps [real_divide_def, real_mult_le_0_iff]) 1);
-by Auto_tac;
+by Auto_tac;
qed "real_divide_le_0_iff";
Addsimps [inst "x" "number_of ?w" real_divide_le_0_iff];
Goal "(inverse(x::real) = 0) = (x = 0)";
-by (auto_tac (claset(), simpset() addsimps [INVERSE_ZERO]));
-by (rtac ccontr 1);
-by (blast_tac (claset() addDs [real_inverse_not_zero]) 1);
+by (auto_tac (claset(), simpset() addsimps [INVERSE_ZERO]));
+by (rtac ccontr 1);
+by (blast_tac (claset() addDs [real_inverse_not_zero]) 1);
qed "real_inverse_zero_iff";
Addsimps [real_inverse_zero_iff];
Goal "(x/y = 0) = (x=0 | y=(0::real))";
-by (auto_tac (claset(), simpset() addsimps [real_divide_def]));
+by (auto_tac (claset(), simpset() addsimps [real_divide_def]));
qed "real_divide_eq_0_iff";
Addsimps [real_divide_eq_0_iff];
Goal "h ~= (0::real) ==> h/h = 1";
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_inv_left]) 1);
-qed "real_divide_self_eq";
+qed "real_divide_self_eq";
Addsimps [real_divide_self_eq];
@@ -110,19 +110,19 @@
by (rtac (real_minus_less_minus RS iffD1) 1);
by (auto_tac (claset(),
simpset() delsimps [real_mult_minus_eq2]
- addsimps [real_minus_mult_eq2]));
+ addsimps [real_minus_mult_eq2]));
qed "real_mult_less_mono1_neg";
Goal "[| i<j; k < (0::real) |] ==> k*j < k*i";
by (rtac (real_minus_less_minus RS iffD1) 1);
-by (auto_tac (claset(),
+by (auto_tac (claset(),
simpset() delsimps [real_mult_minus_eq1]
- addsimps [real_minus_mult_eq1]));
+ addsimps [real_minus_mult_eq1]));
qed "real_mult_less_mono2_neg";
Goal "[| i <= j; k <= (0::real) |] ==> j*k <= i*k";
-by (auto_tac (claset(),
- simpset() addsimps [order_le_less, real_mult_less_mono1_neg]));
+by (auto_tac (claset(),
+ simpset() addsimps [order_le_less, real_mult_less_mono1_neg]));
qed "real_mult_le_mono1_neg";
Goal "[| i <= j; k <= (0::real) |] ==> k*j <= k*i";
@@ -132,56 +132,56 @@
Goal "(m*k < n*k) = (((0::real) < k & m<n) | (k < 0 & n<m))";
by (case_tac "k = (0::real)" 1);
-by (auto_tac (claset(),
- simpset() addsimps [linorder_neq_iff,
- real_mult_less_mono1, real_mult_less_mono1_neg]));
-by (auto_tac (claset(),
+by (auto_tac (claset(),
+ simpset() addsimps [linorder_neq_iff,
+ real_mult_less_mono1, real_mult_less_mono1_neg]));
+by (auto_tac (claset(),
simpset() addsimps [linorder_not_less,
- inst "y1" "m*k" (linorder_not_le RS sym),
+ inst "y1" "m*k" (linorder_not_le RS sym),
inst "y1" "m" (linorder_not_le RS sym)]));
by (TRYALL (etac notE));
-by (auto_tac (claset(),
+by (auto_tac (claset(),
simpset() addsimps [order_less_imp_le, real_mult_le_mono1,
- real_mult_le_mono1_neg]));
+ real_mult_le_mono1_neg]));
qed "real_mult_less_cancel2";
Goal "(m*k <= n*k) = (((0::real) < k --> m<=n) & (k < 0 --> n<=m))";
-by (simp_tac (simpset() addsimps [linorder_not_less RS sym,
+by (simp_tac (simpset() addsimps [linorder_not_less RS sym,
real_mult_less_cancel2]) 1);
qed "real_mult_le_cancel2";
Goal "(k*m < k*n) = (((0::real) < k & m<n) | (k < 0 & n<m))";
-by (simp_tac (simpset() addsimps [inst "z" "k" real_mult_commute,
+by (simp_tac (simpset() addsimps [inst "z" "k" real_mult_commute,
real_mult_less_cancel2]) 1);
qed "real_mult_less_cancel1";
Goal "!!k::real. (k*m <= k*n) = ((0 < k --> m<=n) & (k < 0 --> n<=m))";
-by (simp_tac (simpset() addsimps [linorder_not_less RS sym,
+by (simp_tac (simpset() addsimps [linorder_not_less RS sym,
real_mult_less_cancel1]) 1);
qed "real_mult_le_cancel1";
Goal "!!k::real. (k*m = k*n) = (k = 0 | m=n)";
by (case_tac "k=0" 1);
-by (auto_tac (claset(), simpset() addsimps [real_mult_left_cancel]));
+by (auto_tac (claset(), simpset() addsimps [real_mult_left_cancel]));
qed "real_mult_eq_cancel1";
Goal "!!k::real. (m*k = n*k) = (k = 0 | m=n)";
by (case_tac "k=0" 1);
-by (auto_tac (claset(), simpset() addsimps [real_mult_right_cancel]));
+by (auto_tac (claset(), simpset() addsimps [real_mult_right_cancel]));
qed "real_mult_eq_cancel2";
Goal "!!k::real. k~=0 ==> (k*m) / (k*n) = (m/n)";
by (asm_simp_tac
- (simpset() addsimps [real_divide_def, real_inverse_distrib]) 1);
+ (simpset() addsimps [real_divide_def, real_inverse_distrib]) 1);
by (subgoal_tac "k * m * (inverse k * inverse n) = \
\ (k * inverse k) * (m * inverse n)" 1);
-by (asm_full_simp_tac (simpset() addsimps []) 1);
-by (asm_full_simp_tac (HOL_ss addsimps real_mult_ac) 1);
+by (asm_full_simp_tac (simpset() addsimps []) 1);
+by (asm_full_simp_tac (HOL_ss addsimps real_mult_ac) 1);
qed "real_mult_div_cancel1";
(*For ExtractCommonTerm*)
Goal "(k*m) / (k*n) = (if k = (0::real) then 0 else m/n)";
-by (simp_tac (simpset() addsimps [real_mult_div_cancel1]) 1);
+by (simp_tac (simpset() addsimps [real_mult_div_cancel1]) 1);
qed "real_mult_div_cancel_disj";
@@ -189,19 +189,19 @@
open Real_Numeral_Simprocs
in
-val rel_real_number_of = [eq_real_number_of, less_real_number_of,
+val rel_real_number_of = [eq_real_number_of, less_real_number_of,
le_real_number_of_eq_not_less]
structure CancelNumeralFactorCommon =
struct
- val mk_coeff = mk_coeff
- val dest_coeff = dest_coeff 1
+ val mk_coeff = mk_coeff
+ val dest_coeff = dest_coeff 1
val trans_tac = trans_tac
- val norm_tac =
+ val norm_tac =
ALLGOALS (simp_tac (HOL_ss addsimps real_minus_from_mult_simps @ mult_1s))
THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@real_mult_minus_simps))
THEN ALLGOALS (simp_tac (HOL_ss addsimps real_mult_ac))
- val numeral_simp_tac =
+ val numeral_simp_tac =
ALLGOALS (simp_tac (HOL_ss addsimps rel_real_number_of@bin_simps))
val simplify_meta_eq = simplify_meta_eq
end
@@ -242,26 +242,26 @@
val neg_exchanges = true
)
-val real_cancel_numeral_factors_relations =
+val real_cancel_numeral_factors_relations =
map prep_simproc
[("realeq_cancel_numeral_factor",
- prep_pats ["(l::real) * m = n", "(l::real) = m * n"],
+ ["(l::real) * m = n", "(l::real) = m * n"],
EqCancelNumeralFactor.proc),
- ("realless_cancel_numeral_factor",
- prep_pats ["(l::real) * m < n", "(l::real) < m * n"],
+ ("realless_cancel_numeral_factor",
+ ["(l::real) * m < n", "(l::real) < m * n"],
LessCancelNumeralFactor.proc),
- ("realle_cancel_numeral_factor",
- prep_pats ["(l::real) * m <= n", "(l::real) <= m * n"],
+ ("realle_cancel_numeral_factor",
+ ["(l::real) * m <= n", "(l::real) <= m * n"],
LeCancelNumeralFactor.proc)]
val real_cancel_numeral_factors_divide = prep_simproc
- ("realdiv_cancel_numeral_factor",
- prep_pats ["((l::real) * m) / n", "(l::real) / (m * n)",
- "((number_of v)::real) / (number_of w)"],
- DivCancelNumeralFactor.proc)
+ ("realdiv_cancel_numeral_factor",
+ ["((l::real) * m) / n", "(l::real) / (m * n)",
+ "((number_of v)::real) / (number_of w)"],
+ DivCancelNumeralFactor.proc)
-val real_cancel_numeral_factors =
- real_cancel_numeral_factors_relations @
+val real_cancel_numeral_factors =
+ real_cancel_numeral_factors_relations @
[real_cancel_numeral_factors_divide]
end;
@@ -273,7 +273,7 @@
print_depth 22;
set timing;
set trace_simp;
-fun test s = (Goal s; by (Simp_tac 1));
+fun test s = (Goal s; by (Simp_tac 1));
test "0 <= (y::real) * -2";
test "9*x = 12 * (y::real)";
@@ -315,11 +315,11 @@
structure CancelFactorCommon =
struct
- val mk_sum = long_mk_prod
- val dest_sum = dest_prod
- val mk_coeff = mk_coeff
- val dest_coeff = dest_coeff
- val find_first = find_first []
+ val mk_sum = long_mk_prod
+ val dest_sum = dest_prod
+ val mk_coeff = mk_coeff
+ val dest_coeff = dest_coeff
+ val find_first = find_first []
val trans_tac = trans_tac
val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@real_mult_ac))
end;
@@ -341,13 +341,10 @@
val simplify_meta_eq = cancel_simplify_meta_eq real_mult_div_cancel_disj
);
-val real_cancel_factor =
+val real_cancel_factor =
map prep_simproc
- [("real_eq_cancel_factor",
- prep_pats ["(l::real) * m = n", "(l::real) = m * n"],
- EqCancelFactor.proc),
- ("real_divide_cancel_factor",
- prep_pats ["((l::real) * m) / n", "(l::real) / (m * n)"],
+ [("real_eq_cancel_factor", ["(l::real) * m = n", "(l::real) = m * n"], EqCancelFactor.proc),
+ ("real_divide_cancel_factor", ["((l::real) * m) / n", "(l::real) / (m * n)"],
DivideCancelFactor.proc)];
end;
@@ -359,16 +356,16 @@
print_depth 22;
set timing;
set trace_simp;
-fun test s = (Goal s; by (Asm_simp_tac 1));
+fun test s = (Goal s; by (Asm_simp_tac 1));
test "x*k = k*(y::real)";
-test "k = k*(y::real)";
+test "k = k*(y::real)";
test "a*(b*c) = (b::real)";
test "a*(b*c) = d*(b::real)*(x*a)";
test "(x*k) / (k*(y::real)) = (uu::real)";
-test "(k) / (k*(y::real)) = (uu::real)";
+test "(k) / (k*(y::real)) = (uu::real)";
test "(a*(b*c)) / ((b::real)) = (uu::real)";
test "(a*(b*c)) / (d*(b::real)*(x*a)) = (uu::real)";
@@ -381,106 +378,106 @@
Goal "0<z ==> ((x::real) <= y/z) = (x*z <= y)";
by (subgoal_tac "(x*z <= y) = (x*z <= (y/z)*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
+by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
by (etac ssubst 1);
-by (stac real_mult_le_cancel2 1);
-by (Asm_simp_tac 1);
+by (stac real_mult_le_cancel2 1);
+by (Asm_simp_tac 1);
qed "pos_real_le_divide_eq";
Addsimps [inst "z" "number_of ?w" pos_real_le_divide_eq];
Goal "z<0 ==> ((x::real) <= y/z) = (y <= x*z)";
by (subgoal_tac "(y <= x*z) = ((y/z)*z <= x*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
+by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
by (etac ssubst 1);
-by (stac real_mult_le_cancel2 1);
-by (Asm_simp_tac 1);
+by (stac real_mult_le_cancel2 1);
+by (Asm_simp_tac 1);
qed "neg_real_le_divide_eq";
Addsimps [inst "z" "number_of ?w" neg_real_le_divide_eq];
Goal "0<z ==> (y/z <= (x::real)) = (y <= x*z)";
by (subgoal_tac "(y <= x*z) = ((y/z)*z <= x*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
+by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
by (etac ssubst 1);
-by (stac real_mult_le_cancel2 1);
-by (Asm_simp_tac 1);
+by (stac real_mult_le_cancel2 1);
+by (Asm_simp_tac 1);
qed "pos_real_divide_le_eq";
Addsimps [inst "z" "number_of ?w" pos_real_divide_le_eq];
Goal "z<0 ==> (y/z <= (x::real)) = (x*z <= y)";
by (subgoal_tac "(x*z <= y) = (x*z <= (y/z)*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
+by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
by (etac ssubst 1);
-by (stac real_mult_le_cancel2 1);
-by (Asm_simp_tac 1);
+by (stac real_mult_le_cancel2 1);
+by (Asm_simp_tac 1);
qed "neg_real_divide_le_eq";
Addsimps [inst "z" "number_of ?w" neg_real_divide_le_eq];
Goal "0<z ==> ((x::real) < y/z) = (x*z < y)";
by (subgoal_tac "(x*z < y) = (x*z < (y/z)*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
+by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
by (etac ssubst 1);
-by (stac real_mult_less_cancel2 1);
-by (Asm_simp_tac 1);
+by (stac real_mult_less_cancel2 1);
+by (Asm_simp_tac 1);
qed "pos_real_less_divide_eq";
Addsimps [inst "z" "number_of ?w" pos_real_less_divide_eq];
Goal "z<0 ==> ((x::real) < y/z) = (y < x*z)";
by (subgoal_tac "(y < x*z) = ((y/z)*z < x*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
+by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
by (etac ssubst 1);
-by (stac real_mult_less_cancel2 1);
-by (Asm_simp_tac 1);
+by (stac real_mult_less_cancel2 1);
+by (Asm_simp_tac 1);
qed "neg_real_less_divide_eq";
Addsimps [inst "z" "number_of ?w" neg_real_less_divide_eq];
Goal "0<z ==> (y/z < (x::real)) = (y < x*z)";
by (subgoal_tac "(y < x*z) = ((y/z)*z < x*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
+by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
by (etac ssubst 1);
-by (stac real_mult_less_cancel2 1);
-by (Asm_simp_tac 1);
+by (stac real_mult_less_cancel2 1);
+by (Asm_simp_tac 1);
qed "pos_real_divide_less_eq";
Addsimps [inst "z" "number_of ?w" pos_real_divide_less_eq];
Goal "z<0 ==> (y/z < (x::real)) = (x*z < y)";
by (subgoal_tac "(x*z < y) = (x*z < (y/z)*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
+by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
by (etac ssubst 1);
-by (stac real_mult_less_cancel2 1);
-by (Asm_simp_tac 1);
+by (stac real_mult_less_cancel2 1);
+by (Asm_simp_tac 1);
qed "neg_real_divide_less_eq";
Addsimps [inst "z" "number_of ?w" neg_real_divide_less_eq];
Goal "z~=0 ==> ((x::real) = y/z) = (x*z = y)";
by (subgoal_tac "(x*z = y) = (x*z = (y/z)*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
+by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
by (etac ssubst 1);
-by (stac real_mult_eq_cancel2 1);
-by (Asm_simp_tac 1);
+by (stac real_mult_eq_cancel2 1);
+by (Asm_simp_tac 1);
qed "real_eq_divide_eq";
Addsimps [inst "z" "number_of ?w" real_eq_divide_eq];
Goal "z~=0 ==> (y/z = (x::real)) = (y = x*z)";
by (subgoal_tac "(y = x*z) = ((y/z)*z = x*z)" 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
+by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2);
by (etac ssubst 1);
-by (stac real_mult_eq_cancel2 1);
-by (Asm_simp_tac 1);
+by (stac real_mult_eq_cancel2 1);
+by (Asm_simp_tac 1);
qed "real_divide_eq_eq";
Addsimps [inst "z" "number_of ?w" real_divide_eq_eq];
Goal "(m/k = n/k) = (k = 0 | m = (n::real))";
by (case_tac "k=0" 1);
-by (asm_simp_tac (simpset() addsimps [REAL_DIVIDE_ZERO]) 1);
-by (asm_simp_tac (simpset() addsimps [real_divide_eq_eq, real_eq_divide_eq,
- real_mult_eq_cancel2]) 1);
+by (asm_simp_tac (simpset() addsimps [REAL_DIVIDE_ZERO]) 1);
+by (asm_simp_tac (simpset() addsimps [real_divide_eq_eq, real_eq_divide_eq,
+ real_mult_eq_cancel2]) 1);
qed "real_divide_eq_cancel2";
Goal "(k/m = k/n) = (k = 0 | m = (n::real))";
by (case_tac "m=0 | n = 0" 1);
-by (auto_tac (claset(),
- simpset() addsimps [REAL_DIVIDE_ZERO, real_divide_eq_eq,
- real_eq_divide_eq, real_mult_eq_cancel1]));
+by (auto_tac (claset(),
+ simpset() addsimps [REAL_DIVIDE_ZERO, real_divide_eq_eq,
+ real_eq_divide_eq, real_mult_eq_cancel1]));
qed "real_divide_eq_cancel1";
(*Moved from RealOrd.ML to use 0 *)
@@ -489,53 +486,53 @@
by (res_inst_tac [("t","r")] (real_inverse_inverse RS subst) 1);
by (res_inst_tac [("t","x")] (real_inverse_inverse RS subst) 1);
by (auto_tac (claset() addIs [real_inverse_less_swap],
- simpset() delsimps [real_inverse_inverse]
- addsimps [real_inverse_gt_0]));
+ simpset() delsimps [real_inverse_inverse]
+ addsimps [real_inverse_gt_0]));
qed "real_inverse_less_iff";
Goal "[| 0 < r; 0 < x|] ==> (inverse x <= inverse r) = (r <= (x::real))";
-by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
- real_inverse_less_iff]) 1);
+by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
+ real_inverse_less_iff]) 1);
qed "real_inverse_le_iff";
(** Division by 1, -1 **)
Goal "(x::real)/1 = x";
-by (simp_tac (simpset() addsimps [real_divide_def]) 1);
+by (simp_tac (simpset() addsimps [real_divide_def]) 1);
qed "real_divide_1";
Addsimps [real_divide_1];
Goal "x/-1 = -(x::real)";
-by (Simp_tac 1);
+by (Simp_tac 1);
qed "real_divide_minus1";
Addsimps [real_divide_minus1];
Goal "-1/(x::real) = - (1/x)";
-by (simp_tac (simpset() addsimps [real_divide_def, real_minus_inverse]) 1);
+by (simp_tac (simpset() addsimps [real_divide_def, real_minus_inverse]) 1);
qed "real_minus1_divide";
Addsimps [real_minus1_divide];
Goal "[| (0::real) < d1; 0 < d2 |] ==> EX e. 0 < e & e < d1 & e < d2";
-by (res_inst_tac [("x","(min d1 d2)/2")] exI 1);
-by (asm_simp_tac (simpset() addsimps [min_def]) 1);
+by (res_inst_tac [("x","(min d1 d2)/2")] exI 1);
+by (asm_simp_tac (simpset() addsimps [min_def]) 1);
qed "real_lbound_gt_zero";
Goal "(inverse x = inverse y) = (x = (y::real))";
by (case_tac "x=0 | y=0" 1);
-by (auto_tac (claset(),
- simpset() addsimps [real_inverse_eq_divide,
- DIVISION_BY_ZERO]));
-by (dres_inst_tac [("f","%u. x*y*u")] arg_cong 1);
-by (Asm_full_simp_tac 1);
+by (auto_tac (claset(),
+ simpset() addsimps [real_inverse_eq_divide,
+ DIVISION_BY_ZERO]));
+by (dres_inst_tac [("f","%u. x*y*u")] arg_cong 1);
+by (Asm_full_simp_tac 1);
qed "real_inverse_eq_iff";
Addsimps [real_inverse_eq_iff];
Goal "(z/x = z/y) = (z = 0 | x = (y::real))";
by (case_tac "x=0 | y=0" 1);
-by (auto_tac (claset(),
- simpset() addsimps [DIVISION_BY_ZERO]));
+by (auto_tac (claset(),
+ simpset() addsimps [DIVISION_BY_ZERO]));
by (dres_inst_tac [("f","%u. x*y*u")] arg_cong 1);
-by Auto_tac;
+by Auto_tac;
qed "real_divide_eq_iff";
Addsimps [real_divide_eq_iff];
@@ -545,20 +542,20 @@
(** The next several equations can make the simplifier loop! **)
Goal "(x < - y) = (y < - (x::real))";
-by Auto_tac;
-qed "real_less_minus";
+by Auto_tac;
+qed "real_less_minus";
Goal "(- x < y) = (- y < (x::real))";
-by Auto_tac;
-qed "real_minus_less";
+by Auto_tac;
+qed "real_minus_less";
Goal "(x <= - y) = (y <= - (x::real))";
-by Auto_tac;
-qed "real_le_minus";
+by Auto_tac;
+qed "real_le_minus";
Goal "(- x <= y) = (- y <= (x::real))";
-by Auto_tac;
-qed "real_minus_le";
+by Auto_tac;
+qed "real_minus_le";
Goal "(x = - y) = (y = - (x::real))";
by Auto_tac;
@@ -582,44 +579,44 @@
(*Distributive laws for literals*)
Addsimps (map (inst "w" "number_of ?v")
- [real_add_mult_distrib, real_add_mult_distrib2,
- real_diff_mult_distrib, real_diff_mult_distrib2]);
+ [real_add_mult_distrib, real_add_mult_distrib2,
+ real_diff_mult_distrib, real_diff_mult_distrib2]);
-Addsimps (map (inst "x" "number_of ?v")
- [real_less_minus, real_le_minus, real_equation_minus]);
-Addsimps (map (inst "y" "number_of ?v")
- [real_minus_less, real_minus_le, real_minus_equation]);
+Addsimps (map (inst "x" "number_of ?v")
+ [real_less_minus, real_le_minus, real_equation_minus]);
+Addsimps (map (inst "y" "number_of ?v")
+ [real_minus_less, real_minus_le, real_minus_equation]);
(*Equations and inequations involving 1*)
-Addsimps (map (simplify (simpset()) o inst "x" "1")
- [real_less_minus, real_le_minus, real_equation_minus]);
-Addsimps (map (simplify (simpset()) o inst "y" "1")
- [real_minus_less, real_minus_le, real_minus_equation]);
+Addsimps (map (simplify (simpset()) o inst "x" "1")
+ [real_less_minus, real_le_minus, real_equation_minus]);
+Addsimps (map (simplify (simpset()) o inst "y" "1")
+ [real_minus_less, real_minus_le, real_minus_equation]);
(*** Simprules combining x+y and 0 ***)
Goal "(x+y = (0::real)) = (y = -x)";
-by Auto_tac;
+by Auto_tac;
qed "real_add_eq_0_iff";
AddIffs [real_add_eq_0_iff];
Goal "(x+y < (0::real)) = (y < -x)";
-by Auto_tac;
+by Auto_tac;
qed "real_add_less_0_iff";
AddIffs [real_add_less_0_iff];
Goal "((0::real) < x+y) = (-x < y)";
-by Auto_tac;
+by Auto_tac;
qed "real_0_less_add_iff";
AddIffs [real_0_less_add_iff];
Goal "(x+y <= (0::real)) = (y <= -x)";
-by Auto_tac;
+by Auto_tac;
qed "real_add_le_0_iff";
AddIffs [real_add_le_0_iff];
Goal "((0::real) <= x+y) = (-x <= y)";
-by Auto_tac;
+by Auto_tac;
qed "real_0_le_add_iff";
AddIffs [real_0_le_add_iff];
@@ -629,12 +626,12 @@
**)
Goal "((0::real) < x-y) = (y < x)";
-by Auto_tac;
+by Auto_tac;
qed "real_0_less_diff_iff";
AddIffs [real_0_less_diff_iff];
Goal "((0::real) <= x-y) = (y <= x)";
-by Auto_tac;
+by Auto_tac;
qed "real_0_le_diff_iff";
AddIffs [real_0_le_diff_iff];
--- a/src/HOL/Real/RealBin.ML Tue Aug 06 11:20:47 2002 +0200
+++ b/src/HOL/Real/RealBin.ML Tue Aug 06 11:22:05 2002 +0200
@@ -18,16 +18,16 @@
qed "real_numeral_0_eq_0";
Goalw [real_number_of_def] "Numeral1 = (1::real)";
-by (stac (real_of_one RS sym) 1);
-by (Simp_tac 1);
+by (stac (real_of_one RS sym) 1);
+by (Simp_tac 1);
qed "real_numeral_1_eq_1";
(** Addition **)
Goal "(number_of v :: real) + number_of v' = number_of (bin_add v v')";
by (simp_tac
- (HOL_ss addsimps [real_number_of_def,
- real_of_int_add, number_of_add]) 1);
+ (HOL_ss addsimps [real_number_of_def,
+ real_of_int_add, number_of_add]) 1);
qed "add_real_number_of";
Addsimps [add_real_number_of];
@@ -53,7 +53,7 @@
Goal "(number_of v :: real) * number_of v' = number_of (bin_mult v v')";
by (simp_tac
- (HOL_ss addsimps [real_number_of_def, real_of_int_mult,
+ (HOL_ss addsimps [real_number_of_def, real_of_int_mult,
number_of_mult]) 1);
qed "mult_real_number_of";
@@ -80,8 +80,8 @@
Goal "((number_of v :: real) = number_of v') = \
\ iszero (number_of (bin_add v (bin_minus v')))";
by (simp_tac
- (HOL_ss addsimps [real_number_of_def,
- real_of_int_inject, eq_number_of_eq]) 1);
+ (HOL_ss addsimps [real_number_of_def,
+ real_of_int_inject, eq_number_of_eq]) 1);
qed "eq_real_number_of";
Addsimps [eq_real_number_of];
@@ -92,8 +92,8 @@
Goal "((number_of v :: real) < number_of v') = \
\ neg (number_of (bin_add v (bin_minus v')))";
by (simp_tac
- (HOL_ss addsimps [real_number_of_def, real_of_int_less_iff,
- less_number_of_eq_neg]) 1);
+ (HOL_ss addsimps [real_number_of_def, real_of_int_less_iff,
+ less_number_of_eq_neg]) 1);
qed "less_real_number_of";
Addsimps [less_real_number_of];
@@ -104,7 +104,7 @@
Goal "(number_of x <= (number_of y::real)) = \
\ (~ number_of y < (number_of x::real))";
by (rtac (linorder_not_less RS sym) 1);
-qed "le_real_number_of_eq_not_less";
+qed "le_real_number_of_eq_not_less";
Addsimps [le_real_number_of_eq_not_less];
@@ -115,7 +115,7 @@
qed "real_minus_1_eq_m1";
Goal "-1 * z = -(z::real)";
-by (simp_tac (simpset() addsimps [real_minus_1_eq_m1 RS sym,
+by (simp_tac (simpset() addsimps [real_minus_1_eq_m1 RS sym,
real_mult_minus_1]) 1);
qed "real_mult_minus1";
@@ -127,24 +127,24 @@
(*Maps 0 to Numeral0 and 1 to Numeral1 and -(Numeral1) to -1*)
-val real_numeral_ss =
- HOL_ss addsimps [real_numeral_0_eq_0 RS sym, real_numeral_1_eq_1 RS sym,
- real_minus_1_eq_m1];
+val real_numeral_ss =
+ HOL_ss addsimps [real_numeral_0_eq_0 RS sym, real_numeral_1_eq_1 RS sym,
+ real_minus_1_eq_m1];
-fun rename_numerals th =
+fun rename_numerals th =
asm_full_simplify real_numeral_ss (Thm.transfer (the_context ()) th);
(** real from type "nat" **)
Goal "(0 < real (n::nat)) = (0<n)";
-by (simp_tac (HOL_ss addsimps [real_of_nat_less_iff,
+by (simp_tac (HOL_ss addsimps [real_of_nat_less_iff,
real_of_nat_zero RS sym]) 1);
qed "zero_less_real_of_nat_iff";
AddIffs [zero_less_real_of_nat_iff];
Goal "(0 <= real (n::nat)) = (0<=n)";
-by (simp_tac (HOL_ss addsimps [real_of_nat_le_iff,
+by (simp_tac (HOL_ss addsimps [real_of_nat_le_iff,
real_of_nat_zero RS sym]) 1);
qed "zero_le_real_of_nat_iff";
AddIffs [zero_le_real_of_nat_iff];
@@ -156,7 +156,7 @@
(** Simplification of arithmetic when nested to the right **)
Goal "number_of v + (number_of w + z) = (number_of(bin_add v w) + z::real)";
-by Auto_tac;
+by Auto_tac;
qed "real_add_number_of_left";
Goal "number_of v * (number_of w * z) = (number_of(bin_mult v w) * z::real)";
@@ -175,7 +175,7 @@
qed "real_add_number_of_diff2";
Addsimps [real_add_number_of_left, real_mult_number_of_left,
- real_add_number_of_diff1, real_add_number_of_diff2];
+ real_add_number_of_diff1, real_add_number_of_diff2];
(*"neg" is used in rewrite rules for binary comparisons*)
@@ -195,15 +195,15 @@
(** Combining of literal coefficients in sums of products **)
Goal "(x < y) = (x-y < (0::real))";
-by (simp_tac (simpset() addsimps [real_diff_less_eq]) 1);
+by (simp_tac (simpset() addsimps [real_diff_less_eq]) 1);
qed "real_less_iff_diff_less_0";
Goal "(x = y) = (x-y = (0::real))";
-by (simp_tac (simpset() addsimps [real_diff_eq_eq]) 1);
+by (simp_tac (simpset() addsimps [real_diff_eq_eq]) 1);
qed "real_eq_iff_diff_eq_0";
Goal "(x <= y) = (x-y <= (0::real))";
-by (simp_tac (simpset() addsimps [real_diff_le_eq]) 1);
+by (simp_tac (simpset() addsimps [real_diff_le_eq]) 1);
qed "real_le_iff_diff_le_0";
@@ -217,15 +217,15 @@
(** For cancel_numerals **)
val rel_iff_rel_0_rls = map (inst "y" "?u+?v")
- [real_less_iff_diff_less_0, real_eq_iff_diff_eq_0,
- real_le_iff_diff_le_0] @
- map (inst "y" "n")
- [real_less_iff_diff_less_0, real_eq_iff_diff_eq_0,
- real_le_iff_diff_le_0];
+ [real_less_iff_diff_less_0, real_eq_iff_diff_eq_0,
+ real_le_iff_diff_le_0] @
+ map (inst "y" "n")
+ [real_less_iff_diff_less_0, real_eq_iff_diff_eq_0,
+ real_le_iff_diff_le_0];
Goal "!!i::real. (i*u + m = j*u + n) = ((i-j)*u + m = n)";
by (asm_simp_tac (simpset() addsimps [real_diff_def, real_add_mult_distrib]@
- real_add_ac@rel_iff_rel_0_rls) 1);
+ real_add_ac@rel_iff_rel_0_rls) 1);
qed "real_eq_add_iff1";
Goal "!!i::real. (i*u + m = j*u + n) = (m = (j-i)*u + n)";
@@ -294,7 +294,7 @@
| dest_summing (pos, Const ("op -", _) $ t $ u, ts) =
dest_summing (pos, t, dest_summing (not pos, u, ts))
| dest_summing (pos, t, ts) =
- if pos then t::ts else uminus_const$t :: ts;
+ if pos then t::ts else uminus_const$t :: ts;
fun dest_sum t = dest_summing (true, t, []);
@@ -312,29 +312,29 @@
val dest_times = HOLogic.dest_bin "op *" HOLogic.realT;
fun dest_prod t =
- let val (t,u) = dest_times t
+ let val (t,u) = dest_times t
in dest_prod t @ dest_prod u end
handle TERM _ => [t];
-(*DON'T do the obvious simplifications; that would create special cases*)
+(*DON'T do the obvious simplifications; that would create special cases*)
fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts);
(*Express t as a product of (possibly) a numeral with other sorted terms*)
fun dest_coeff sign (Const ("uminus", _) $ t) = dest_coeff (~sign) t
| dest_coeff sign t =
let val ts = sort Term.term_ord (dest_prod t)
- val (n, ts') = find_first_numeral [] ts
+ val (n, ts') = find_first_numeral [] ts
handle TERM _ => (1, ts)
in (sign*n, mk_prod ts') end;
(*Find first coefficient-term THAT MATCHES u*)
-fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
+fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
| find_first_coeff past u (t::terms) =
- let val (n,u') = dest_coeff 1 t
- in if u aconv u' then (n, rev past @ terms)
- else find_first_coeff (t::past) u terms
- end
- handle TERM _ => find_first_coeff (t::past) u terms;
+ let val (n,u') = dest_coeff 1 t
+ in if u aconv u' then (n, rev past @ terms)
+ else find_first_coeff (t::past) u terms
+ end
+ handle TERM _ => find_first_coeff (t::past) u terms;
(*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1*)
@@ -345,27 +345,27 @@
(*To perform binary arithmetic*)
val bin_simps =
[real_numeral_0_eq_0 RS sym, real_numeral_1_eq_1 RS sym,
- add_real_number_of, real_add_number_of_left, minus_real_number_of,
- diff_real_number_of, mult_real_number_of, real_mult_number_of_left] @
+ add_real_number_of, real_add_number_of_left, minus_real_number_of,
+ diff_real_number_of, mult_real_number_of, real_mult_number_of_left] @
bin_arith_simps @ bin_rel_simps;
(*To evaluate binary negations of coefficients*)
val real_minus_simps = NCons_simps @
- [real_minus_1_eq_m1, minus_real_number_of,
- bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
- bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
+ [real_minus_1_eq_m1, minus_real_number_of,
+ bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
+ bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
(*To let us treat subtraction as addition*)
val diff_simps = [real_diff_def, real_minus_add_distrib, real_minus_minus];
(*push the unary minus down: - x * y = x * - y
-val real_minus_mult_eq_1_to_2 =
+val real_minus_mult_eq_1_to_2 =
[real_minus_mult_eq1 RS sym, real_minus_mult_eq2] MRS trans |> standard;
same as real_minus_mult_commute
*)
(*to extract again any uncancelled minuses*)
-val real_minus_from_mult_simps =
+val real_minus_from_mult_simps =
[real_minus_minus, real_mult_minus_eq1, real_mult_minus_eq2];
(*combine unary minus with numeric literals, however nested within a product*)
@@ -382,40 +382,39 @@
let val ct = cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)))
in Some
(prove_goalw_cterm [] ct (K tacs)
- handle ERROR => error
- ("The error(s) above occurred while trying to prove " ^
- string_of_cterm ct ^ "\nInternal failure of simproc " ^ name))
+ handle ERROR => error
+ ("The error(s) above occurred while trying to prove " ^
+ string_of_cterm ct ^ "\nInternal failure of simproc " ^ name))
end;
(*version without the hyps argument*)
fun prove_conv_nohyps name tacs sg = prove_conv name tacs sg [];
(*Final simplification: cancel + and * *)
-val simplify_meta_eq =
+val simplify_meta_eq =
Int_Numeral_Simprocs.simplify_meta_eq
[real_add_zero_left, real_add_zero_right,
- real_mult_0, real_mult_0_right, real_mult_1, real_mult_1_right];
+ real_mult_0, real_mult_0_right, real_mult_1, real_mult_1_right];
-fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
-fun prep_pat s = HOLogic.read_cterm (Theory.sign_of (the_context ())) s;
-val prep_pats = map prep_pat;
+fun prep_simproc (name, pats, proc) =
+ Simplifier.simproc (Theory.sign_of (the_context ())) name pats proc;
structure CancelNumeralsCommon =
struct
- val mk_sum = mk_sum
- val dest_sum = dest_sum
- val mk_coeff = mk_coeff
- val dest_coeff = dest_coeff 1
- val find_first_coeff = find_first_coeff []
+ val mk_sum = mk_sum
+ val dest_sum = dest_sum
+ val mk_coeff = mk_coeff
+ val dest_coeff = dest_coeff 1
+ val find_first_coeff = find_first_coeff []
val trans_tac = trans_tac
- val norm_tac =
+ val norm_tac =
ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
real_minus_simps@real_add_ac))
THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@real_mult_minus_simps))
THEN ALLGOALS
(simp_tac (HOL_ss addsimps real_minus_from_mult_simps@
real_add_ac@real_mult_ac))
- val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
+ val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
val simplify_meta_eq = simplify_meta_eq
end;
@@ -447,53 +446,51 @@
val bal_add2 = real_le_add_iff2 RS trans
);
-val cancel_numerals =
+val cancel_numerals =
map prep_simproc
[("realeq_cancel_numerals",
- prep_pats ["(l::real) + m = n", "(l::real) = m + n",
- "(l::real) - m = n", "(l::real) = m - n",
- "(l::real) * m = n", "(l::real) = m * n"],
+ ["(l::real) + m = n", "(l::real) = m + n",
+ "(l::real) - m = n", "(l::real) = m - n",
+ "(l::real) * m = n", "(l::real) = m * n"],
EqCancelNumerals.proc),
- ("realless_cancel_numerals",
- prep_pats ["(l::real) + m < n", "(l::real) < m + n",
- "(l::real) - m < n", "(l::real) < m - n",
- "(l::real) * m < n", "(l::real) < m * n"],
+ ("realless_cancel_numerals",
+ ["(l::real) + m < n", "(l::real) < m + n",
+ "(l::real) - m < n", "(l::real) < m - n",
+ "(l::real) * m < n", "(l::real) < m * n"],
LessCancelNumerals.proc),
- ("realle_cancel_numerals",
- prep_pats ["(l::real) + m <= n", "(l::real) <= m + n",
- "(l::real) - m <= n", "(l::real) <= m - n",
- "(l::real) * m <= n", "(l::real) <= m * n"],
+ ("realle_cancel_numerals",
+ ["(l::real) + m <= n", "(l::real) <= m + n",
+ "(l::real) - m <= n", "(l::real) <= m - n",
+ "(l::real) * m <= n", "(l::real) <= m * n"],
LeCancelNumerals.proc)];
structure CombineNumeralsData =
struct
- val add = op + : int*int -> int
- val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *)
- val dest_sum = dest_sum
- val mk_coeff = mk_coeff
- val dest_coeff = dest_coeff 1
- val left_distrib = left_real_add_mult_distrib RS trans
- val prove_conv = prove_conv_nohyps "real_combine_numerals"
+ val add = op + : int*int -> int
+ val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *)
+ val dest_sum = dest_sum
+ val mk_coeff = mk_coeff
+ val dest_coeff = dest_coeff 1
+ val left_distrib = left_real_add_mult_distrib RS trans
+ val prove_conv = prove_conv_nohyps "real_combine_numerals"
val trans_tac = trans_tac
- val norm_tac =
+ val norm_tac =
ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
diff_simps@real_minus_simps@real_add_ac))
THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@real_mult_minus_simps))
THEN ALLGOALS (simp_tac (HOL_ss addsimps real_minus_from_mult_simps@
real_add_ac@real_mult_ac))
- val numeral_simp_tac = ALLGOALS
+ val numeral_simp_tac = ALLGOALS
(simp_tac (HOL_ss addsimps add_0s@bin_simps))
- val simplify_meta_eq =
- Int_Numeral_Simprocs.simplify_meta_eq (add_0s@mult_1s)
+ val simplify_meta_eq =
+ Int_Numeral_Simprocs.simplify_meta_eq (add_0s@mult_1s)
end;
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
-
-val combine_numerals =
- prep_simproc ("real_combine_numerals",
- prep_pats ["(i::real) + j", "(i::real) - j"],
- CombineNumerals.proc);
+
+val combine_numerals =
+ prep_simproc ("real_combine_numerals", ["(i::real) + j", "(i::real) - j"], CombineNumerals.proc);
(** Declarations for ExtractCommonTerm **)
@@ -503,16 +500,16 @@
| long_mk_prod (t :: ts) = mk_times (t, mk_prod ts);
(*Find first term that matches u*)
-fun find_first past u [] = raise TERM("find_first", [])
+fun find_first past u [] = raise TERM("find_first", [])
| find_first past u (t::terms) =
- if u aconv t then (rev past @ terms)
+ if u aconv t then (rev past @ terms)
else find_first (t::past) u terms
- handle TERM _ => find_first (t::past) u terms;
+ handle TERM _ => find_first (t::past) u terms;
(*Final simplification: cancel + and * *)
-fun cancel_simplify_meta_eq cancel_th th =
- Int_Numeral_Simprocs.simplify_meta_eq
- [real_mult_1, real_mult_1_right]
+fun cancel_simplify_meta_eq cancel_th th =
+ Int_Numeral_Simprocs.simplify_meta_eq
+ [real_mult_1, real_mult_1_right]
(([th, cancel_th]) MRS trans);
(*** Making constant folding work for 0 and 1 too ***)
@@ -525,32 +522,32 @@
val numeral_1_eq_1 = real_numeral_1_eq_1
val prove_conv = prove_conv_nohyps "real_abstract_numerals"
fun norm_tac simps = ALLGOALS (simp_tac (HOL_ss addsimps simps))
- val simplify_meta_eq = Bin_Simprocs.simplify_meta_eq
+ val simplify_meta_eq = Bin_Simprocs.simplify_meta_eq
end
structure RealAbstractNumerals = AbstractNumeralsFun (RealAbstractNumeralsData)
(*For addition, we already have rules for the operand 0.
- Multiplication is omitted because there are already special rules for
+ Multiplication is omitted because there are already special rules for
both 0 and 1 as operands. Unary minus is trivial, just have - 1 = -1.
For the others, having three patterns is a compromise between just having
one (many spurious calls) and having nine (just too many!) *)
-val eval_numerals =
+val eval_numerals =
map prep_simproc
[("real_add_eval_numerals",
- prep_pats ["(m::real) + 1", "(m::real) + number_of v"],
+ ["(m::real) + 1", "(m::real) + number_of v"],
RealAbstractNumerals.proc add_real_number_of),
("real_diff_eval_numerals",
- prep_pats ["(m::real) - 1", "(m::real) - number_of v"],
+ ["(m::real) - 1", "(m::real) - number_of v"],
RealAbstractNumerals.proc diff_real_number_of),
("real_eq_eval_numerals",
- prep_pats ["(m::real) = 0", "(m::real) = 1", "(m::real) = number_of v"],
+ ["(m::real) = 0", "(m::real) = 1", "(m::real) = number_of v"],
RealAbstractNumerals.proc eq_real_number_of),
("real_less_eval_numerals",
- prep_pats ["(m::real) < 0", "(m::real) < 1", "(m::real) < number_of v"],
+ ["(m::real) < 0", "(m::real) < 1", "(m::real) < number_of v"],
RealAbstractNumerals.proc less_real_number_of),
("real_le_eval_numerals",
- prep_pats ["(m::real) <= 0", "(m::real) <= 1", "(m::real) <= number_of v"],
+ ["(m::real) <= 0", "(m::real) <= 1", "(m::real) <= number_of v"],
RealAbstractNumerals.proc le_real_number_of_eq_not_less)]
end;
@@ -567,7 +564,7 @@
print_depth 22;
set timing;
set trace_simp;
-fun test s = (Goal s; by (Simp_tac 1));
+fun test s = (Goal s; by (Simp_tac 1));
test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::real)";
@@ -609,10 +606,10 @@
structure Real_Times_Assoc_Data : ASSOC_FOLD_DATA =
struct
- val ss = HOL_ss
- val eq_reflection = eq_reflection
+ val ss = HOL_ss
+ val eq_reflection = eq_reflection
val sg_ref = Sign.self_ref (Theory.sign_of (the_context ()))
- val T = HOLogic.realT
+ val T = HOLogic.realT
val plus = Const ("op *", [HOLogic.realT,HOLogic.realT] ---> HOLogic.realT)
val add_ac = real_mult_ac
end;
@@ -629,8 +626,8 @@
(** <= monotonicity results: needed for arithmetic **)
Goal "[| i <= j; (0::real) <= k |] ==> i*k <= j*k";
-by (auto_tac (claset(),
- simpset() addsimps [order_le_less, real_mult_less_mono1]));
+by (auto_tac (claset(),
+ simpset() addsimps [order_le_less, real_mult_less_mono1]));
qed "real_mult_le_mono1";
Goal "[| i <= j; (0::real) <= k |] ==> k*i <= k*j";
--- a/src/HOL/Real/real_arith0.ML Tue Aug 06 11:20:47 2002 +0200
+++ b/src/HOL/Real/real_arith0.ML Tue Aug 06 11:22:05 2002 +0200
@@ -43,10 +43,6 @@
"(i <= j) & (k < l) ==> i + k < j + (l::real)",
"(i < j) & (k < l) ==> i + k < j + (l::real)"];
-val real_arith_simproc_pats =
- map (fn s => Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.boolT))
- ["(m::real) < n","(m::real) <= n", "(m::real) = n"];
-
fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var;
val real_mult_mono_thms =
@@ -57,8 +53,9 @@
in
-val fast_real_arith_simproc = mk_simproc
- "fast_real_arith" real_arith_simproc_pats Fast_Arith.lin_arith_prover;
+val fast_real_arith_simproc = Simplifier.simproc (Theory.sign_of (the_context ()))
+ "fast_real_arith" ["(m::real) < n","(m::real) <= n", "(m::real) = n"]
+ Fast_Arith.lin_arith_prover;
val real_arith_setup =
[Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
--- a/src/HOL/Set.thy Tue Aug 06 11:20:47 2002 +0200
+++ b/src/HOL/Set.thy Tue Aug 06 11:22:05 2002 +0200
@@ -297,29 +297,25 @@
by blast
ML_setup {*
- let
+ local
val Ball_def = thm "Ball_def";
val Bex_def = thm "Bex_def";
- val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
- ("EX x:A. P x & Q x", HOLogic.boolT);
-
val prove_bex_tac =
rewrite_goals_tac [Bex_def] THEN Quantifier1.prove_one_point_ex_tac;
val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
- val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
- ("ALL x:A. P x --> Q x", HOLogic.boolT);
-
val prove_ball_tac =
rewrite_goals_tac [Ball_def] THEN Quantifier1.prove_one_point_all_tac;
val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
-
- val defBEX_regroup = mk_simproc "defined BEX" [ex_pattern] rearrange_bex;
- val defBALL_regroup = mk_simproc "defined BALL" [all_pattern] rearrange_ball;
in
- Addsimprocs [defBALL_regroup, defBEX_regroup]
+ val defBEX_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
+ "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex;
+ val defBALL_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
+ "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball;
end;
+
+ Addsimprocs [defBALL_regroup, defBEX_regroup];
*}
--- a/src/HOL/Tools/datatype_package.ML Tue Aug 06 11:20:47 2002 +0200
+++ b/src/HOL/Tools/datatype_package.ML Tue Aug 06 11:22:05 2002 +0200
@@ -367,8 +367,8 @@
| _ => None)
| distinct_proc sg _ _ = None;
-val distinct_pats = [HOLogic.read_cterm (Theory.sign_of HOL.thy) "s = t"];
-val distinct_simproc = mk_simproc distinctN distinct_pats distinct_proc;
+val distinct_simproc =
+ Simplifier.simproc (Theory.sign_of HOL.thy) distinctN ["s = t"] distinct_proc;
val dist_ss = HOL_ss addsimprocs [distinct_simproc];
--- a/src/HOL/Tools/record_package.ML Tue Aug 06 11:20:47 2002 +0200
+++ b/src/HOL/Tools/record_package.ML Tue Aug 06 11:22:05 2002 +0200
@@ -499,34 +499,26 @@
(** record simproc **)
-local
-
-val sel_upd_pat = [HOLogic.read_cterm (Theory.sign_of HOL.thy) "s (u k r)"];
-
-fun proc sg _ t =
- (case t of (sel as Const (s, _)) $ ((upd as Const (u, _)) $ k $ r) =>
- (case get_selectors sg s of Some () =>
- (case get_updates sg u of Some u_name =>
- let
- fun mk_free x t = Free (x, fastype_of t);
- val k' = mk_free "k" k;
- val r' = mk_free "r" r;
- val t' = sel $ (upd $ k' $ r');
- fun prove prop =
- Tactic.prove sg ["k", "r"] [] prop (K (simp_all_tac (get_simpset sg) []));
- in
- if u_name = s then Some (prove (Logic.mk_equals (t', k')))
- else Some (prove (Logic.mk_equals (t', sel $ r')))
- end
- | None => None)
- | None => None)
- | _ => None);
-
-in
-
-val record_simproc = Simplifier.mk_simproc "record_simp" sel_upd_pat proc;
-
-end;
+val record_simproc =
+ Simplifier.simproc (Theory.sign_of HOL.thy) "record_simp" ["s (u k r)"]
+ (fn sg => fn _ => fn t =>
+ (case t of (sel as Const (s, _)) $ ((upd as Const (u, _)) $ k $ r) =>
+ (case get_selectors sg s of Some () =>
+ (case get_updates sg u of Some u_name =>
+ let
+ fun mk_free x t = Free (x, fastype_of t);
+ val k' = mk_free "k" k;
+ val r' = mk_free "r" r;
+ val t' = sel $ (upd $ k' $ r');
+ fun prove prop =
+ Tactic.prove sg ["k", "r"] [] prop (K (simp_all_tac (get_simpset sg) []));
+ in
+ if u_name = s then Some (prove (Logic.mk_equals (t', k')))
+ else Some (prove (Logic.mk_equals (t', sel $ r')))
+ end
+ | None => None)
+ | None => None)
+ | _ => None));
--- a/src/HOL/arith_data.ML Tue Aug 06 11:20:47 2002 +0200
+++ b/src/HOL/arith_data.ML Tue Aug 06 11:22:05 2002 +0200
@@ -138,28 +138,20 @@
(** prepare nat_cancel simprocs **)
-fun prep_pat s = HOLogic.read_cterm (Theory.sign_of (the_context ())) s;
-val prep_pats = map prep_pat;
-
-fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
-
-val eq_pats = prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n",
- "m = Suc n"];
-val less_pats = prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n",
- "m < Suc n"];
-val le_pats = prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n",
- "Suc m <= n", "m <= Suc n"];
-val diff_pats = prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)",
- "Suc m - n", "m - Suc n"];
+fun prep_simproc (name, pats, proc) =
+ Simplifier.simproc (Theory.sign_of (the_context ())) name pats proc;
val nat_cancel_sums_add = map prep_simproc
- [("nateq_cancel_sums", eq_pats, EqCancelSums.proc),
- ("natless_cancel_sums", less_pats, LessCancelSums.proc),
- ("natle_cancel_sums", le_pats, LeCancelSums.proc)];
+ [("nateq_cancel_sums",
+ ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"], EqCancelSums.proc),
+ ("natless_cancel_sums",
+ ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"], LessCancelSums.proc),
+ ("natle_cancel_sums",
+ ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"], LeCancelSums.proc)];
val nat_cancel_sums = nat_cancel_sums_add @
- [prep_simproc("natdiff_cancel_sums", diff_pats, DiffCancelSums.proc)];
-
+ [prep_simproc ("natdiff_cancel_sums",
+ ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"], DiffCancelSums.proc)];
end;
@@ -393,15 +385,10 @@
end;
+val fast_nat_arith_simproc =
+ Simplifier.simproc (Theory.sign_of (the_context ())) "fast_nat_arith"
+ ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] Fast_Arith.lin_arith_prover;
-local
-val nat_arith_simproc_pats =
- map (fn s => Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.boolT))
- ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"];
-in
-val fast_nat_arith_simproc = mk_simproc
- "fast_nat_arith" nat_arith_simproc_pats Fast_Arith.lin_arith_prover;
-end;
(* Because of fast_nat_arith_simproc, the arithmetic solver is really only
useful to detect inconsistencies among the premises for subgoals which are
--- a/src/HOL/simpdata.ML Tue Aug 06 11:20:47 2002 +0200
+++ b/src/HOL/simpdata.ML Tue Aug 06 11:22:05 2002 +0200
@@ -123,17 +123,13 @@
end;
-local
-val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
- ("EX x. P(x)",HOLogic.boolT)
-val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
- ("ALL x. P(x)",HOLogic.boolT)
-in
-val defEX_regroup = mk_simproc "defined EX" [ex_pattern]
- Quantifier1.rearrange_ex
-val defALL_regroup = mk_simproc "defined ALL" [all_pattern]
- Quantifier1.rearrange_all
-end;
+val defEX_regroup =
+ Simplifier.simproc (Theory.sign_of (the_context ()))
+ "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex;
+
+val defALL_regroup =
+ Simplifier.simproc (Theory.sign_of (the_context ()))
+ "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all;
(*** Case splitting ***)
--- a/src/Provers/Arith/abel_cancel.ML Tue Aug 06 11:20:47 2002 +0200
+++ b/src/Provers/Arith/abel_cancel.ML Tue Aug 06 11:22:05 2002 +0200
@@ -5,41 +5,41 @@
Simplification procedures for abelian groups (e.g. integers, reals)
-- Cancel complementary terms in sums
+- Cancel complementary terms in sums
- Cancel like terms on opposite sides of relations
*)
signature ABEL_CANCEL =
sig
- val ss : simpset (*basic simpset of object-logtic*)
- val eq_reflection : thm (*object-equality to meta-equality*)
+ val ss : simpset (*basic simpset of object-logtic*)
+ val eq_reflection : thm (*object-equality to meta-equality*)
- val sg_ref : Sign.sg_ref (*signature of the theory of the group*)
- val T : typ (*the type of group elements*)
+ val sg_ref : Sign.sg_ref (*signature of the theory of the group*)
+ val T : typ (*the type of group elements*)
- val zero : term
+ val zero : term
val restrict_to_left : thm
- val add_cancel_21 : thm
- val add_cancel_end : thm
- val add_left_cancel : thm
- val add_assoc : thm
- val add_commute : thm
- val add_left_commute : thm
- val add_0 : thm
- val add_0_right : thm
+ val add_cancel_21 : thm
+ val add_cancel_end : thm
+ val add_left_cancel : thm
+ val add_assoc : thm
+ val add_commute : thm
+ val add_left_commute : thm
+ val add_0 : thm
+ val add_0_right : thm
- val eq_diff_eq : thm
- val eqI_rules : thm list
- val dest_eqI : thm -> term
+ val eq_diff_eq : thm
+ val eqI_rules : thm list
+ val dest_eqI : thm -> term
- val diff_def : thm
- val minus_add_distrib : thm
- val minus_minus : thm
- val minus_0 : thm
+ val diff_def : thm
+ val minus_add_distrib : thm
+ val minus_minus : thm
+ val minus_0 : thm
- val add_inverses : thm list
- val cancel_simps : thm list
+ val add_inverses : thm list
+ val cancel_simps : thm list
end;
@@ -48,9 +48,9 @@
open Data;
- val prepare_ss = Data.ss addsimps [add_assoc, diff_def,
- minus_add_distrib, minus_minus,
- minus_0, add_0, add_0_right];
+ val prepare_ss = Data.ss addsimps [add_assoc, diff_def,
+ minus_add_distrib, minus_minus,
+ minus_0, add_0, add_0_right];
(*prove while suppressing timing information*)
fun prove ct = setmp Library.timing false (prove_goalw_cterm [] ct);
@@ -60,8 +60,8 @@
(*Cancel corresponding terms on the two sides of the equation, NOT on
the same side!*)
- val cancel_ss =
- Data.ss addsimps [add_cancel_21, add_cancel_end, minus_minus] @
+ val cancel_ss =
+ Data.ss addsimps [add_cancel_21, add_cancel_end, minus_minus] @
(map (fn th => th RS restrict_to_left) Data.cancel_simps);
val inverse_ss = Data.ss addsimps Data.add_inverses @ Data.cancel_simps;
@@ -77,13 +77,13 @@
(*Flatten a formula built from +, binary - and unary -.
No need to check types PROVIDED they are checked upon entry!*)
fun add_terms neg (Const ("op +", _) $ x $ y, ts) =
- add_terms neg (x, add_terms neg (y, ts))
+ add_terms neg (x, add_terms neg (y, ts))
| add_terms neg (Const ("op -", _) $ x $ y, ts) =
- add_terms neg (x, add_terms (not neg) (y, ts))
- | add_terms neg (Const ("uminus", _) $ x, ts) =
- add_terms (not neg) (x, ts)
- | add_terms neg (x, ts) =
- (if neg then negate x else x) :: ts;
+ add_terms neg (x, add_terms (not neg) (y, ts))
+ | add_terms neg (Const ("uminus", _) $ x, ts) =
+ add_terms (not neg) (x, ts)
+ | add_terms neg (x, ts) =
+ (if neg then negate x else x) :: ts;
fun terms fml = add_terms false (fml, []);
@@ -98,39 +98,39 @@
(*Make a simproc to cancel complementary terms in sums. Examples:
x-x = 0 x+(y-x) = y -x+(y+(x+z)) = y+z
- It will unfold the definition of diff and associate to the right if
+ It will unfold the definition of diff and associate to the right if
necessary. Rewriting is faster if the formula is already
in that form.
*)
fun sum_proc sg _ lhs =
- let val _ = if !trace then tracing ("cancel_sums: LHS = " ^
- string_of_cterm (cterm_of sg lhs))
- else ()
+ let val _ = if !trace then tracing ("cancel_sums: LHS = " ^
+ string_of_cterm (cterm_of sg lhs))
+ else ()
val (head::tail) = terms lhs
val head' = negate head
val rhs = mk_sum (cancelled (head',tail))
and chead' = Thm.cterm_of sg head'
- val _ = if !trace then
- tracing ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
- else ()
+ val _ = if !trace then
+ tracing ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
+ else ()
val ct = Thm.cterm_of sg (Logic.mk_equals (lhs, rhs))
- val thm = prove ct
- (fn _ => [rtac eq_reflection 1,
- simp_tac prepare_ss 1,
- IF_UNSOLVED (simp_tac cancel_ss 1),
- IF_UNSOLVED (simp_tac inverse_ss 1)])
- handle ERROR =>
- error("cancel_sums simproc:\nfailed to prove " ^
- string_of_cterm ct)
+ val thm = prove ct
+ (fn _ => [rtac eq_reflection 1,
+ simp_tac prepare_ss 1,
+ IF_UNSOLVED (simp_tac cancel_ss 1),
+ IF_UNSOLVED (simp_tac inverse_ss 1)])
+ handle ERROR =>
+ error("cancel_sums simproc:\nfailed to prove " ^
+ string_of_cterm ct)
in Some thm end
handle Cancel => None;
- val sum_conv =
+ val sum_conv =
Simplifier.mk_simproc "cancel_sums"
(map (Thm.read_cterm (Sign.deref sg_ref))
- [("x + y", Data.T), ("x - y", Data.T)])
+ [("x + y", Data.T), ("x - y", Data.T)]) (* FIXME depends on concrete syntax !???!!??! *)
sum_proc;
@@ -144,24 +144,24 @@
calls to the simproc will be needed.*)
fun cancel1 ([], u) = raise Match (*impossible: it's a common term*)
| cancel1 (t::ts, u) = if t aconv u then ts
- else t :: cancel1 (ts,u);
+ else t :: cancel1 (ts,u);
val sum_cancel_ss = Data.ss addsimprocs [sum_conv]
- addsimps [add_0, add_0_right];
+ addsimps [add_0, add_0_right];
val add_ac_ss = Data.ss addsimps [add_assoc,add_commute,add_left_commute];
fun rel_proc sg _ (lhs as (rel$lt$rt)) =
- let val _ = if !trace then tracing ("cancel_relations: LHS = " ^
- string_of_cterm (cterm_of sg lhs))
- else ()
+ let val _ = if !trace then tracing ("cancel_relations: LHS = " ^
+ string_of_cterm (cterm_of sg lhs))
+ else ()
val ltms = terms lt
and rtms = terms rt
val common = (*inter_term miscounts repetitions, so squash them*)
- gen_distinct (op aconv) (inter_term (ltms, rtms))
+ gen_distinct (op aconv) (inter_term (ltms, rtms))
val _ = if null common then raise Cancel (*nothing to do*)
- else ()
+ else ()
fun cancelled tms = mk_sum (foldl cancel1 (tms, common))
@@ -169,26 +169,25 @@
and rt' = cancelled rtms
val rhs = rel$lt'$rt'
- val _ = if !trace then
- tracing ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
- else ()
+ val _ = if !trace then
+ tracing ("RHS = " ^ string_of_cterm (Thm.cterm_of sg rhs))
+ else ()
val ct = Thm.cterm_of sg (Logic.mk_equals (lhs,rhs))
- val thm = prove ct
- (fn _ => [rtac eq_reflection 1,
- resolve_tac eqI_rules 1,
- simp_tac prepare_ss 1,
- simp_tac sum_cancel_ss 1,
- IF_UNSOLVED (simp_tac add_ac_ss 1)])
- handle ERROR =>
- error("cancel_relations simproc:\nfailed to prove " ^
- string_of_cterm ct)
+ val thm = prove ct
+ (fn _ => [rtac eq_reflection 1,
+ resolve_tac eqI_rules 1,
+ simp_tac prepare_ss 1,
+ simp_tac sum_cancel_ss 1,
+ IF_UNSOLVED (simp_tac add_ac_ss 1)])
+ handle ERROR =>
+ error("cancel_relations simproc:\nfailed to prove " ^
+ string_of_cterm ct)
in Some thm end
handle Cancel => None;
- val rel_conv =
- Simplifier.mk_simproc "cancel_relations"
- (map (Thm.cterm_of (Sign.deref sg_ref) o Data.dest_eqI) eqI_rules)
- rel_proc;
+ val rel_conv =
+ Simplifier.simproc_i (Sign.deref sg_ref) "cancel_relations"
+ (map Data.dest_eqI eqI_rules) rel_proc;
end;
--- a/src/Provers/Arith/assoc_fold.ML Tue Aug 06 11:20:47 2002 +0200
+++ b/src/Provers/Arith/assoc_fold.ML Tue Aug 06 11:22:05 2002 +0200
@@ -11,12 +11,12 @@
signature ASSOC_FOLD_DATA =
sig
- val ss : simpset (*basic simpset of object-logtic*)
- val eq_reflection : thm (*object-equality to meta-equality*)
- val sg_ref : Sign.sg_ref (*the operator's signature*)
- val T : typ (*the operator's numeric type*)
- val plus : term (*the operator being folded*)
- val add_ac : thm list (*AC-rewrites for plus*)
+ val ss : simpset (*basic simpset of object-logtic*)
+ val eq_reflection : thm (*object-equality to meta-equality*)
+ val sg_ref : Sign.sg_ref (*the operator's signature*)
+ val T : typ (*the operator's numeric type*)
+ val plus : term (*the operator being folded*)
+ val add_ac : thm list (*AC-rewrites for plus*)
end;
@@ -26,11 +26,11 @@
val assoc_ss = Data.ss addsimps Data.add_ac;
(*prove while suppressing timing information*)
- fun prove name ct tacf =
+ fun prove name ct tacf =
setmp Library.timing false (prove_goalw_cterm [] ct) tacf
handle ERROR =>
- error(name ^ " simproc:\nfailed to prove " ^ string_of_cterm ct);
-
+ error(name ^ " simproc:\nfailed to prove " ^ string_of_cterm ct);
+
exception Assoc_fail;
fun mk_sum [] = raise Assoc_fail
@@ -39,13 +39,13 @@
(*Separate the literals from the other terms being combined*)
fun sift_terms (t, (lits,others)) =
case t of
- Const("Numeral.number_of", _) $ _ =>
- (t::lits, others) (*new literal*)
- | (f as Const _) $ x $ y =>
- if f = Data.plus
+ Const("Numeral.number_of", _) $ _ =>
+ (t::lits, others) (*new literal*)
+ | (f as Const _) $ x $ y =>
+ if f = Data.plus
then sift_terms (x, sift_terms (y, (lits,others)))
- else (lits, t::others) (*arbitrary summand*)
- | _ => (lits, t::others);
+ else (lits, t::others) (*arbitrary summand*)
+ | _ => (lits, t::others);
val trace = ref false;
@@ -53,25 +53,23 @@
fun proc sg _ lhs =
let fun show t = string_of_cterm (Thm.cterm_of sg t)
val _ = if !trace then tracing ("assoc_fold simproc: LHS = " ^ show lhs)
- else ()
+ else ()
val (lits,others) = sift_terms (lhs, ([],[]))
val _ = if length lits < 2
then raise Assoc_fail (*we can't reduce the number of terms*)
- else ()
+ else ()
val rhs = Data.plus $ mk_sum lits $ mk_sum others
val _ = if !trace then tracing ("RHS = " ^ show rhs) else ()
- val th = prove "assoc_fold"
- (Thm.cterm_of sg (Logic.mk_equals (lhs, rhs)))
- (fn _ => [rtac Data.eq_reflection 1,
- simp_tac assoc_ss 1])
+ val th = prove "assoc_fold"
+ (Thm.cterm_of sg (Logic.mk_equals (lhs, rhs)))
+ (fn _ => [rtac Data.eq_reflection 1,
+ simp_tac assoc_ss 1])
in Some th end
handle Assoc_fail => None;
-
- val conv =
- Simplifier.mk_simproc "assoc_fold"
- [Thm.cterm_of (Sign.deref Data.sg_ref)
- (Data.plus $ Free("x",Data.T) $ Free("y",Data.T))]
- proc;
+
+ val conv =
+ Simplifier.simproc_i (Sign.deref Data.sg_ref) "assoc_fold"
+ [Data.plus $ Free ("x", Data.T) $ Free ("y",Data.T)] proc;
end;
--- a/src/Provers/simplifier.ML Tue Aug 06 11:20:47 2002 +0200
+++ b/src/Provers/simplifier.ML Tue Aug 06 11:22:05 2002 +0200
@@ -16,6 +16,10 @@
type simproc
val mk_simproc: string -> cterm list
-> (Sign.sg -> thm list -> term -> thm option) -> simproc
+ val simproc: Sign.sg -> string -> string list
+ -> (Sign.sg -> thm list -> term -> thm option) -> simproc
+ val simproc_i: Sign.sg -> string -> term list
+ -> (Sign.sg -> thm list -> term -> thm option) -> simproc
type solver
val mk_solver: string -> (thm list -> int -> tactic) -> solver
type simpset
@@ -126,6 +130,10 @@
fun mk_simproc name lhss proc =
Simproc (name, map (Thm.cterm_fun Logic.varify) lhss, proc, stamp ());
+fun simproc sg name ss =
+ mk_simproc name (map (fn s => Thm.read_cterm sg (s, TypeInfer.logicT)) ss);
+fun simproc_i sg name = mk_simproc name o map (Thm.cterm_of sg);
+
fun rep_simproc (Simproc args) = args;
--- a/src/ZF/Datatype.ML Tue Aug 06 11:20:47 2002 +0200
+++ b/src/ZF/Datatype.ML Tue Aug 06 11:22:05 2002 +0200
@@ -97,9 +97,7 @@
val conv =
- Simplifier.mk_simproc "data_free"
- [Thm.read_cterm (sign_of ZF.thy) ("(x::i) = y", FOLogic.oT)]
- proc;
+ Simplifier.simproc (Theory.sign_of ZF.thy) "data_free" ["(x::i) = y"] proc;
end;
--- a/src/ZF/Integ/int_arith.ML Tue Aug 06 11:20:47 2002 +0200
+++ b/src/ZF/Integ/int_arith.ML Tue Aug 06 11:22:05 2002 +0200
@@ -49,11 +49,11 @@
(** For cancel_numerals **)
val rel_iff_rel_0_rls = map (inst "y" "?u$+?v")
- [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
- zle_iff_zdiff_zle_0] @
- map (inst "y" "n")
- [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
- zle_iff_zdiff_zle_0];
+ [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
+ zle_iff_zdiff_zle_0] @
+ map (inst "y" "n")
+ [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
+ zle_iff_zdiff_zle_0];
Goal "(i$*u $+ m = j$*u $+ n) <-> ((i$-j)$*u $+ m = intify(n))";
by (simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
@@ -100,14 +100,14 @@
fun mk_numeral n = integ_of_const $ NumeralSyntax.mk_bin n;
(*Decodes a binary INTEGER*)
-fun dest_numeral (Const("Bin.integ_of", _) $ w) =
+fun dest_numeral (Const("Bin.integ_of", _) $ w) =
(NumeralSyntax.dest_bin w
handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
| dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
fun find_first_numeral past (t::terms) =
- ((dest_numeral t, rev past @ terms)
- handle TERM _ => find_first_numeral (t::past) terms)
+ ((dest_numeral t, rev past @ terms)
+ handle TERM _ => find_first_numeral (t::past) terms)
| find_first_numeral past [] = raise TERM("find_first_numeral", []);
val zero = mk_numeral 0;
@@ -134,7 +134,7 @@
| dest_summing (pos, Const ("Int.zdiff", _) $ t $ u, ts) =
dest_summing (pos, t, dest_summing (not pos, u, ts))
| dest_summing (pos, t, ts) =
- if pos then t::ts else zminus_const$t :: ts;
+ if pos then t::ts else zminus_const$t :: ts;
fun dest_sum t = dest_summing (true, t, []);
@@ -152,38 +152,38 @@
val dest_times = FOLogic.dest_bin "Int.zmult" iT;
fun dest_prod t =
- let val (t,u) = dest_times t
+ let val (t,u) = dest_times t
in dest_prod t @ dest_prod u end
handle TERM _ => [t];
-(*DON'T do the obvious simplifications; that would create special cases*)
+(*DON'T do the obvious simplifications; that would create special cases*)
fun mk_coeff (k, t) = mk_times (mk_numeral k, t);
(*Express t as a product of (possibly) a numeral with other sorted terms*)
fun dest_coeff sign (Const ("Int.zminus", _) $ t) = dest_coeff (~sign) t
| dest_coeff sign t =
let val ts = sort Term.term_ord (dest_prod t)
- val (n, ts') = find_first_numeral [] ts
+ val (n, ts') = find_first_numeral [] ts
handle TERM _ => (1, ts)
in (sign*n, mk_prod ts') end;
(*Find first coefficient-term THAT MATCHES u*)
-fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
+fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
| find_first_coeff past u (t::terms) =
- let val (n,u') = dest_coeff 1 t
- in if u aconv u' then (n, rev past @ terms)
- else find_first_coeff (t::past) u terms
- end
- handle TERM _ => find_first_coeff (t::past) u terms;
+ let val (n,u') = dest_coeff 1 t
+ in if u aconv u' then (n, rev past @ terms)
+ else find_first_coeff (t::past) u terms
+ end
+ handle TERM _ => find_first_coeff (t::past) u terms;
(*Simplify #1*n and n*#1 to n*)
val add_0s = [zadd_0_intify, zadd_0_right_intify];
-val mult_1s = [zmult_1_intify, zmult_1_right_intify,
+val mult_1s = [zmult_1_intify, zmult_1_right_intify,
zmult_minus1, zmult_minus1_right];
-val tc_rules = [integ_of_type, intify_in_int,
+val tc_rules = [integ_of_type, intify_in_int,
int_of_type, zadd_type, zdiff_type, zmult_type] @ bin.intrs;
val intifys = [intify_ident, zadd_intify1, zadd_intify2,
zdiff_intify1, zdiff_intify2, zmult_intify1, zmult_intify2,
@@ -194,47 +194,45 @@
(*To evaluate binary negations of coefficients*)
val zminus_simps = NCons_simps @
- [integ_of_minus RS sym,
- bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
- bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
+ [integ_of_minus RS sym,
+ bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
+ bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
(*To let us treat subtraction as addition*)
val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus];
(*push the unary minus down: - x * y = x * - y *)
-val int_minus_mult_eq_1_to_2 =
+val int_minus_mult_eq_1_to_2 =
[zmult_zminus, zmult_zminus_right RS sym] MRS trans |> standard;
(*to extract again any uncancelled minuses*)
-val int_minus_from_mult_simps =
+val int_minus_from_mult_simps =
[zminus_zminus, zmult_zminus, zmult_zminus_right];
(*combine unary minus with numeric literals, however nested within a product*)
val int_mult_minus_simps =
[zmult_assoc, zmult_zminus RS sym, int_minus_mult_eq_1_to_2];
-fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
-fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ()))
- (s, TypeInfer.anyT ["logic"]);
-val prep_pats = map prep_pat;
+fun prep_simproc (name, pats, proc) =
+ Simplifier.simproc (Theory.sign_of (the_context ())) name pats proc;
structure CancelNumeralsCommon =
struct
- val mk_sum = mk_sum
- val dest_sum = dest_sum
- val mk_coeff = mk_coeff
- val dest_coeff = dest_coeff 1
- val find_first_coeff = find_first_coeff []
- val trans_tac = ArithData.gen_trans_tac iff_trans
+ val mk_sum = mk_sum
+ val dest_sum = dest_sum
+ val mk_coeff = mk_coeff
+ val dest_coeff = dest_coeff 1
+ val find_first_coeff = find_first_coeff []
+ val trans_tac = ArithData.gen_trans_tac iff_trans
val norm_tac_ss1 = ZF_ss addsimps add_0s@mult_1s@diff_simps@
zminus_simps@zadd_ac
val norm_tac_ss2 = ZF_ss addsimps bin_simps@int_mult_minus_simps@intifys
val norm_tac_ss3 = ZF_ss addsimps int_minus_from_mult_simps@
zadd_ac@zmult_ac@tc_rules@intifys
- val norm_tac = ALLGOALS (asm_simp_tac norm_tac_ss1)
- THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
- THEN ALLGOALS (asm_simp_tac norm_tac_ss3)
- val numeral_simp_tac =
+ val norm_tac = ALLGOALS (asm_simp_tac norm_tac_ss1)
+ THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
+ THEN ALLGOALS (asm_simp_tac norm_tac_ss3)
+ val numeral_simp_tac =
ALLGOALS (simp_tac (ZF_ss addsimps add_0s@bin_simps@tc_rules@intifys))
THEN ALLGOALS Asm_simp_tac
val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s@mult_1s)
@@ -268,22 +266,22 @@
val bal_add2 = le_add_iff2 RS iff_trans
);
-val cancel_numerals =
+val cancel_numerals =
map prep_simproc
[("inteq_cancel_numerals",
- prep_pats ["l $+ m = n", "l = m $+ n",
- "l $- m = n", "l = m $- n",
- "l $* m = n", "l = m $* n"],
+ ["l $+ m = n", "l = m $+ n",
+ "l $- m = n", "l = m $- n",
+ "l $* m = n", "l = m $* n"],
EqCancelNumerals.proc),
- ("intless_cancel_numerals",
- prep_pats ["l $+ m $< n", "l $< m $+ n",
- "l $- m $< n", "l $< m $- n",
- "l $* m $< n", "l $< m $* n"],
+ ("intless_cancel_numerals",
+ ["l $+ m $< n", "l $< m $+ n",
+ "l $- m $< n", "l $< m $- n",
+ "l $* m $< n", "l $< m $* n"],
LessCancelNumerals.proc),
- ("intle_cancel_numerals",
- prep_pats ["l $+ m $<= n", "l $<= m $+ n",
- "l $- m $<= n", "l $<= m $- n",
- "l $* m $<= n", "l $<= m $* n"],
+ ("intle_cancel_numerals",
+ ["l $+ m $<= n", "l $<= m $+ n",
+ "l $- m $<= n", "l $<= m $- n",
+ "l $* m $<= n", "l $<= m $* n"],
LeCancelNumerals.proc)];
@@ -292,12 +290,12 @@
structure CombineNumeralsData =
struct
- val add = op + : int*int -> int
- val mk_sum = long_mk_sum (*to work for e.g. #2*x $+ #3*x *)
- val dest_sum = dest_sum
- val mk_coeff = mk_coeff
- val dest_coeff = dest_coeff 1
- val left_distrib = left_zadd_zmult_distrib RS trans
+ val add = op + : int*int -> int
+ val mk_sum = long_mk_sum (*to work for e.g. #2*x $+ #3*x *)
+ val dest_sum = dest_sum
+ val mk_coeff = mk_coeff
+ val dest_coeff = dest_coeff 1
+ val left_distrib = left_zadd_zmult_distrib RS trans
val prove_conv = prove_conv_nohyps "int_combine_numerals"
val trans_tac = ArithData.gen_trans_tac trans
val norm_tac_ss1 = ZF_ss addsimps add_0s@mult_1s@diff_simps@
@@ -305,20 +303,18 @@
val norm_tac_ss2 = ZF_ss addsimps bin_simps@int_mult_minus_simps@intifys
val norm_tac_ss3 = ZF_ss addsimps int_minus_from_mult_simps@
zadd_ac@zmult_ac@tc_rules@intifys
- val norm_tac = ALLGOALS (asm_simp_tac norm_tac_ss1)
- THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
- THEN ALLGOALS (asm_simp_tac norm_tac_ss3)
- val numeral_simp_tac =
+ val norm_tac = ALLGOALS (asm_simp_tac norm_tac_ss1)
+ THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
+ THEN ALLGOALS (asm_simp_tac norm_tac_ss3)
+ val numeral_simp_tac =
ALLGOALS (simp_tac (ZF_ss addsimps add_0s@bin_simps@tc_rules@intifys))
val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s@mult_1s)
end;
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
-
-val combine_numerals =
- prep_simproc ("int_combine_numerals",
- prep_pats ["i $+ j", "i $- j"],
- CombineNumerals.proc);
+
+val combine_numerals =
+ prep_simproc ("int_combine_numerals", ["i $+ j", "i $- j"], CombineNumerals.proc);
@@ -330,39 +326,37 @@
structure CombineNumeralsProdData =
struct
- val add = op * : int*int -> int
- val mk_sum = mk_prod
- val dest_sum = dest_prod
- fun mk_coeff(k,t) = if t=one then mk_numeral k
+ val add = op * : int*int -> int
+ val mk_sum = mk_prod
+ val dest_sum = dest_prod
+ fun mk_coeff(k,t) = if t=one then mk_numeral k
else raise TERM("mk_coeff", [])
fun dest_coeff t = (dest_numeral t, one) (*We ONLY want pure numerals.*)
- val left_distrib = zmult_assoc RS sym RS trans
+ val left_distrib = zmult_assoc RS sym RS trans
val prove_conv = prove_conv_nohyps "int_combine_numerals_prod"
val trans_tac = ArithData.gen_trans_tac trans
val norm_tac_ss1 = ZF_ss addsimps mult_1s@diff_simps@zminus_simps
val norm_tac_ss2 = ZF_ss addsimps [zmult_zminus_right RS sym]@
bin_simps@zmult_ac@tc_rules@intifys
- val norm_tac = ALLGOALS (asm_simp_tac norm_tac_ss1)
- THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
- val numeral_simp_tac =
+ val norm_tac = ALLGOALS (asm_simp_tac norm_tac_ss1)
+ THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
+ val numeral_simp_tac =
ALLGOALS (simp_tac (ZF_ss addsimps bin_simps@tc_rules@intifys))
val simplify_meta_eq = ArithData.simplify_meta_eq (mult_1s)
end;
structure CombineNumeralsProd = CombineNumeralsFun(CombineNumeralsProdData);
-
-val combine_numerals_prod =
- prep_simproc ("int_combine_numerals_prod",
- prep_pats ["i $* j"],
- CombineNumeralsProd.proc);
+
+val combine_numerals_prod =
+ prep_simproc ("int_combine_numerals_prod", ["i $* j"], CombineNumeralsProd.proc);
end;
Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
Addsimprocs [Int_Numeral_Simprocs.combine_numerals,
- Int_Numeral_Simprocs.combine_numerals_prod];
+ Int_Numeral_Simprocs.combine_numerals_prod];
(*examples:*)
@@ -370,7 +364,7 @@
print_depth 22;
set timing;
set trace_simp;
-fun test s = (Goal s; by (Asm_simp_tac 1));
+fun test s = (Goal s; by (Asm_simp_tac 1));
val sg = #sign (rep_thm (topthm()));
val t = FOLogic.dest_Trueprop (Logic.strip_assums_concl(getgoal 1));
val (t,_) = FOLogic.dest_eq t;
--- a/src/ZF/OrdQuant.thy Tue Aug 06 11:20:47 2002 +0200
+++ b/src/ZF/OrdQuant.thy Tue Aug 06 11:22:05 2002 +0200
@@ -388,34 +388,27 @@
simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
*}
-text{*Setting up the one-point-rule simproc*}
-ML
-{*
+text {* Setting up the one-point-rule simproc *}
-let
-val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
- ("EX x[M]. P(x) & Q(x)", FOLogic.oT)
+ML_setup {*
+local
-val prove_rex_tac = rewtac rex_def THEN
- Quantifier1.prove_one_point_ex_tac;
-
+val prove_rex_tac = rewtac rex_def THEN Quantifier1.prove_one_point_ex_tac;
val rearrange_bex = Quantifier1.rearrange_bex prove_rex_tac;
-val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
- ("ALL x[M]. P(x) --> Q(x)", FOLogic.oT)
-
-val prove_rall_tac = rewtac rall_def THEN
- Quantifier1.prove_one_point_all_tac;
-
+val prove_rall_tac = rewtac rall_def THEN Quantifier1.prove_one_point_all_tac;
val rearrange_ball = Quantifier1.rearrange_ball prove_rall_tac;
-val defREX_regroup = mk_simproc "defined REX" [ex_pattern] rearrange_bex;
-val defRALL_regroup = mk_simproc "defined RALL" [all_pattern] rearrange_ball;
in
-Addsimprocs [defRALL_regroup,defREX_regroup]
+val defREX_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
+ "defined REX" ["EX x[M]. P(x) & Q(x)"] rearrange_bex;
+val defRALL_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
+ "defined RALL" ["ALL x[M]. P(x) --> Q(x)"] rearrange_ball;
end;
+
+Addsimprocs [defRALL_regroup,defREX_regroup];
*}
end
--- a/src/ZF/arith_data.ML Tue Aug 06 11:20:47 2002 +0200
+++ b/src/ZF/arith_data.ML Tue Aug 06 11:22:05 2002 +0200
@@ -12,7 +12,7 @@
val nat_cancel: simproc list
(*tools for use in similar applications*)
val gen_trans_tac: thm -> thm option -> tactic
- val prove_conv: string -> tactic list -> Sign.sg ->
+ val prove_conv: string -> tactic list -> Sign.sg ->
thm list -> term * term -> thm option
val simplify_meta_eq: thm list -> thm -> thm
(*debugging*)
@@ -63,7 +63,7 @@
(*We remove equality assumptions because they confuse the simplifier and
because only type-checking assumptions are necessary.*)
-fun is_eq_thm th =
+fun is_eq_thm th =
can FOLogic.dest_eq (FOLogic.dest_Trueprop (#prop (rep_thm th)));
fun add_chyps chyps ct = Drule.list_implies (map cprop_of chyps, ct);
@@ -75,17 +75,15 @@
val goal = Logic.list_implies (map (#prop o Thm.rep_thm) hyps',
FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
in Some (hyps' MRS Tactic.prove sg [] [] goal (K (EVERY tacs)))
- handle ERROR_MESSAGE msg =>
- (warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); None)
+ handle ERROR_MESSAGE msg =>
+ (warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); None)
end;
-fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
-fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ()))
- (s, TypeInfer.anyT ["logic"]);
-val prep_pats = map prep_pat;
+fun prep_simproc (name, pats, proc) =
+ Simplifier.simproc (Theory.sign_of (the_context ())) name pats proc;
-(*** Use CancelNumerals simproc without binary numerals,
+(*** Use CancelNumerals simproc without binary numerals,
just for cancellation ***)
val mk_times = FOLogic.mk_binop "Arith.mult";
@@ -132,9 +130,9 @@
(*Final simplification: cancel + and **)
fun simplify_meta_eq rules =
mk_meta_eq o
- simplify (FOL_ss addeqcongs[eq_cong2,iff_cong2]
+ simplify (FOL_ss addeqcongs[eq_cong2,iff_cong2]
delsimps iff_simps (*these could erase the whole rule!*)
- addsimps rules);
+ addsimps rules);
val final_rules = add_0s @ mult_1s @ [mult_0, mult_0_right];
@@ -158,7 +156,7 @@
(** The functor argumnets are declared as separate structures
so that they can be exported to ease debugging. **)
-structure EqCancelNumeralsData =
+structure EqCancelNumeralsData =
struct
open CancelNumeralsCommon
val prove_conv = prove_conv "nateq_cancel_numerals"
@@ -171,7 +169,7 @@
structure EqCancelNumerals = CancelNumeralsFun(EqCancelNumeralsData);
-structure LessCancelNumeralsData =
+structure LessCancelNumeralsData =
struct
open CancelNumeralsCommon
val prove_conv = prove_conv "natless_cancel_numerals"
@@ -184,7 +182,7 @@
structure LessCancelNumerals = CancelNumeralsFun(LessCancelNumeralsData);
-structure DiffCancelNumeralsData =
+structure DiffCancelNumeralsData =
struct
open CancelNumeralsCommon
val prove_conv = prove_conv "natdiff_cancel_numerals"
@@ -199,26 +197,25 @@
val nat_cancel =
- map prep_simproc
- [("nateq_cancel_numerals",
- prep_pats ["l #+ m = n", "l = m #+ n",
- "l #* m = n", "l = m #* n",
- "succ(m) = n", "m = succ(n)"],
- EqCancelNumerals.proc),
- ("natless_cancel_numerals",
- prep_pats ["l #+ m < n", "l < m #+ n",
- "l #* m < n", "l < m #* n",
- "succ(m) < n", "m < succ(n)"],
- LessCancelNumerals.proc),
- ("natdiff_cancel_numerals",
- prep_pats ["(l #+ m) #- n", "l #- (m #+ n)",
- "(l #* m) #- n", "l #- (m #* n)",
- "succ(m) #- n", "m #- succ(n)"],
- DiffCancelNumerals.proc)];
+ map prep_simproc
+ [("nateq_cancel_numerals",
+ ["l #+ m = n", "l = m #+ n",
+ "l #* m = n", "l = m #* n",
+ "succ(m) = n", "m = succ(n)"],
+ EqCancelNumerals.proc),
+ ("natless_cancel_numerals",
+ ["l #+ m < n", "l < m #+ n",
+ "l #* m < n", "l < m #* n",
+ "succ(m) < n", "m < succ(n)"],
+ LessCancelNumerals.proc),
+ ("natdiff_cancel_numerals",
+ ["(l #+ m) #- n", "l #- (m #+ n)",
+ "(l #* m) #- n", "l #- (m #* n)",
+ "succ(m) #- n", "m #- succ(n)"],
+ DiffCancelNumerals.proc)];
end;
-(*Install the simprocs!*)
Addsimprocs ArithData.nat_cancel;
--- a/src/ZF/simpdata.ML Tue Aug 06 11:20:47 2002 +0200
+++ b/src/ZF/simpdata.ML Tue Aug 06 11:22:05 2002 +0200
@@ -11,17 +11,17 @@
(*Should False yield False<->True, or should it solve goals some other way?*)
(*Analyse a theorem to atomic rewrite rules*)
-fun atomize (conn_pairs, mem_pairs) th =
+fun atomize (conn_pairs, mem_pairs) th =
let fun tryrules pairs t =
case head_of t of
- Const(a,_) =>
+ Const(a,_) =>
(case assoc(pairs,a) of
Some rls => flat (map (atomize (conn_pairs, mem_pairs))
([th] RL rls))
| None => [th])
| _ => [th]
- in case concl_of th of
- Const("Trueprop",_) $ P =>
+ in case concl_of th of
+ Const("Trueprop",_) $ P =>
(case P of
Const("op :",_) $ a $ b => tryrules mem_pairs b
| Const("True",_) => []
@@ -32,13 +32,13 @@
(*Analyse a rigid formula*)
val ZF_conn_pairs =
- [("Ball", [bspec]),
+ [("Ball", [bspec]),
("All", [spec]),
("op -->", [mp]),
("op &", [conjunct1,conjunct2])];
(*Analyse a:b, where b is rigid*)
-val ZF_mem_pairs =
+val ZF_mem_pairs =
[("Collect", [CollectD1,CollectD2]),
("op -", [DiffD1,DiffD2]),
("op Int", [IntD1,IntD2])];
@@ -55,8 +55,8 @@
(** Splitting IFs in the assumptions **)
Goal "P(if Q then x else y) <-> (~((Q & ~P(x)) | (~Q & ~P(y))))";
-by (Simp_tac 1);
-qed "split_if_asm";
+by (Simp_tac 1);
+qed "split_if_asm";
bind_thms ("if_splits", [split_if, split_if_asm]);
@@ -65,8 +65,8 @@
local
(*For proving rewrite rules*)
- fun prover s = (print s;prove_goalw (the_context ()) [Inter_def] s
- (fn _ => [Simp_tac 1,
+ fun prover s = (print s;prove_goalw (the_context ()) [Inter_def] s
+ (fn _ => [Simp_tac 1,
ALLGOALS (blast_tac (claset() addSIs[equalityI]))]));
in
@@ -86,7 +86,7 @@
"(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))",
"(~(ALL x:A. P(x))) <-> (EX x:A. ~P(x))"];
-val ball_conj_distrib =
+val ball_conj_distrib =
prover "(ALL x:A. P(x) & Q(x)) <-> ((ALL x:A. P(x)) & (ALL x:A. Q(x)))";
val bex_simps = map prover
@@ -104,14 +104,14 @@
"(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))",
"(~(EX x:A. P(x))) <-> (ALL x:A. ~P(x))"];
-val bex_disj_distrib =
+val bex_disj_distrib =
prover "(EX x:A. P(x) | Q(x)) <-> ((EX x:A. P(x)) | (EX x:A. Q(x)))";
val Rep_simps = map prover
- ["{x. y:0, R(x,y)} = 0", (*Replace*)
- "{x:0. P(x)} = 0", (*Collect*)
+ ["{x. y:0, R(x,y)} = 0", (*Replace*)
+ "{x:0. P(x)} = 0", (*Collect*)
"{x:A. P} = (if P then A else 0)",
- "RepFun(0,f) = 0", (*RepFun*)
+ "RepFun(0,f) = 0", (*RepFun*)
"RepFun(succ(i),f) = cons(f(i), RepFun(i,f))",
"RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"]
@@ -124,7 +124,7 @@
"Inter({b}) = b"]
-val UN_simps = map prover
+val UN_simps = map prover
["(UN x:C. cons(a, B(x))) = (if C=0 then 0 else cons(a, UN x:C. B(x)))",
"(UN x:C. A(x) Un B) = (if C=0 then 0 else (UN x:C. A(x)) Un B)",
"(UN x:C. A Un B(x)) = (if C=0 then 0 else A Un (UN x:C. B(x)))",
@@ -145,10 +145,10 @@
"(INT x:C. A(x) Un B) = (if C=0 then 0 else (INT x:C. A(x)) Un B)",
"(INT x:C. A Un B(x)) = (if C=0 then 0 else A Un (INT x:C. B(x)))"];
-(** The _extend_simps rules are oriented in the opposite direction, to
+(** The _extend_simps rules are oriented in the opposite direction, to
pull UN and INT outwards. **)
-val UN_extend_simps = map prover
+val UN_extend_simps = map prover
["cons(a, UN x:C. B(x)) = (if C=0 then {a} else (UN x:C. cons(a, B(x))))",
"(UN x:C. A(x)) Un B = (if C=0 then B else (UN x:C. A(x) Un B))",
"A Un (UN x:C. B(x)) = (if C=0 then A else (UN x:C. A Un B(x)))",
@@ -220,30 +220,25 @@
ball_one_point1,ball_one_point2];
-let
-val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
- ("EX x:A. P(x) & Q(x)",FOLogic.oT)
+local
-val prove_bex_tac = rewtac Bex_def THEN
- Quantifier1.prove_one_point_ex_tac;
-
+val prove_bex_tac = rewtac Bex_def THEN Quantifier1.prove_one_point_ex_tac;
val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
-val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ()))
- ("ALL x:A. P(x) --> Q(x)",FOLogic.oT)
-
-val prove_ball_tac = rewtac Ball_def THEN
- Quantifier1.prove_one_point_all_tac;
-
+val prove_ball_tac = rewtac Ball_def THEN Quantifier1.prove_one_point_all_tac;
val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
-val defBEX_regroup = mk_simproc "defined BEX" [ex_pattern] rearrange_bex;
-val defBALL_regroup = mk_simproc "defined BALL" [all_pattern] rearrange_ball;
in
-Addsimprocs [defBALL_regroup,defBEX_regroup]
+val defBEX_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
+ "defined BEX" ["EX x:A. P(x) & Q(x)"] rearrange_bex;
+
+val defBALL_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
+ "defined BALL" ["ALL x:A. P(x) --> Q(x)"] rearrange_ball;
end;
+Addsimprocs [defBALL_regroup, defBEX_regroup];
+
val ZF_ss = simpset();