# HG changeset patch # User wenzelm # Date 1028625725 -7200 # Node ID 56610e2ba220d62841e1f2f0de8ba71e2d885d61 # Parent f93f7d76689542be54566f2a5b3e2a026709ea84 sane interface for simprocs; diff -r f93f7d766895 -r 56610e2ba220 src/FOL/simpdata.ML --- 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 ***) diff -r f93f7d766895 -r 56610e2ba220 src/HOL/Bali/Basis.thy --- 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] diff -r f93f7d766895 -r 56610e2ba220 src/HOL/Bali/Eval.thy --- 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" "\v. w=In1 v \ G\s \t-\v \ s'" @@ -989,7 +989,7 @@ (Const ("Pair", _) $ x $ _) $ _ ) $ _)) = is_None x in val eval_no_abrupt_proc = - make_simproc "eval_no_abrupt" "G\(x,s) \e\\ (w,Norm s')" pred + cond_simproc "eval_no_abrupt" "G\(x,s) \e\\ (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\(Some xc,s) \e\\ (w,s')" pred (thm "eval_abrupt") end; Addsimprocs [eval_abrupt_proc] diff -r f93f7d766895 -r 56610e2ba220 src/HOL/Bali/Evaln.thy --- 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" "\v. w=In1 v \ G\s \t-\v \n\ s'"; @@ -350,7 +350,7 @@ (Const ("Pair", _) $ _ $ x)))) $ _ ) = is_Some x in val evaln_abrupt_proc = - make_simproc "evaln_abrupt" "G\(Some xc,s) \e\\n\ (w,s')" pred (thm "evaln_abrupt") + cond_simproc "evaln_abrupt" "G\(Some xc,s) \e\\n\ (w,s')" pred (thm "evaln_abrupt") end; Addsimprocs [evaln_abrupt_proc] *} diff -r f93f7d766895 -r 56610e2ba220 src/HOL/Bali/WellType.thy --- 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" "\T. U=Inl T \ E,dt\t\-T" diff -r f93f7d766895 -r 56610e2ba220 src/HOL/Fun.ML --- 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]; diff -r f93f7d766895 -r 56610e2ba220 src/HOL/Hyperreal/HyperArith0.ML --- 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 < 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 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 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 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 ((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 (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 ((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 (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]; - - diff -r f93f7d766895 -r 56610e2ba220 src/HOL/Hyperreal/HyperBin.ML --- 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"; diff -r f93f7d766895 -r 56610e2ba220 src/HOL/Hyperreal/NSA.ML --- 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 EX r: Reals. x ((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 [ 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 ==> [] - hypreal_of_real x|: Infinitesimal + |X(n) - x| < 1/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"; diff -r f93f7d766895 -r 56610e2ba220 src/HOL/Hyperreal/hypreal_arith0.ML --- 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} => diff -r f93f7d766895 -r 56610e2ba220 src/HOL/Integ/Bin.ML --- 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; diff -r f93f7d766895 -r 56610e2ba220 src/HOL/Integ/int_arith1.ML --- 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 a+c <= b+d"; diff -r f93f7d766895 -r 56610e2ba220 src/HOL/Integ/int_factor_simprocs.ML --- 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 (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)"; *) diff -r f93f7d766895 -r 56610e2ba220 src/HOL/Integ/nat_bin.ML --- 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; diff -r f93f7d766895 -r 56610e2ba220 src/HOL/Integ/nat_simprocs.ML --- 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 (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 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, diff -r f93f7d766895 -r 56610e2ba220 src/HOL/List.thy --- 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 = diff -r f93f7d766895 -r 56610e2ba220 src/HOL/Modelcheck/EindhovenSyn.ML --- 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]; diff -r f93f7d766895 -r 56610e2ba220 src/HOL/Modelcheck/MuckeSyn.ML --- 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]; diff -r f93f7d766895 -r 56610e2ba220 src/HOL/Product_Type.thy --- 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]; diff -r f93f7d766895 -r 56610e2ba220 src/HOL/Real/RealArith0.ML --- 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 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 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 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 ((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 (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 ((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 (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]; diff -r f93f7d766895 -r 56610e2ba220 src/HOL/Real/RealBin.ML --- 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 [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"; diff -r f93f7d766895 -r 56610e2ba220 src/HOL/Real/real_arith0.ML --- 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} => diff -r f93f7d766895 -r 56610e2ba220 src/HOL/Set.thy --- 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]; *} diff -r f93f7d766895 -r 56610e2ba220 src/HOL/Tools/datatype_package.ML --- 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]; diff -r f93f7d766895 -r 56610e2ba220 src/HOL/Tools/record_package.ML --- 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)); diff -r f93f7d766895 -r 56610e2ba220 src/HOL/arith_data.ML --- 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 diff -r f93f7d766895 -r 56610e2ba220 src/HOL/simpdata.ML --- 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 ***) diff -r f93f7d766895 -r 56610e2ba220 src/Provers/Arith/abel_cancel.ML --- 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; diff -r f93f7d766895 -r 56610e2ba220 src/Provers/Arith/assoc_fold.ML --- 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; diff -r f93f7d766895 -r 56610e2ba220 src/Provers/simplifier.ML --- 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; diff -r f93f7d766895 -r 56610e2ba220 src/ZF/Datatype.ML --- 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; diff -r f93f7d766895 -r 56610e2ba220 src/ZF/Integ/int_arith.ML --- 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; diff -r f93f7d766895 -r 56610e2ba220 src/ZF/OrdQuant.thy --- 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 diff -r f93f7d766895 -r 56610e2ba220 src/ZF/arith_data.ML --- 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; diff -r f93f7d766895 -r 56610e2ba220 src/ZF/simpdata.ML --- 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();