1.1 --- a/src/HOL/Algebra/abstract/NatSum.ML Thu Nov 11 10:25:17 1999 +0100
1.2 +++ b/src/HOL/Algebra/abstract/NatSum.ML Thu Nov 11 10:25:29 1999 +0100
1.3 @@ -4,8 +4,6 @@
1.4 Author: Clemens Ballarin, started 12 December 1996
1.5 *)
1.6
1.7 -open NatSum;
1.8 -
1.9 section "Basic Properties";
1.10
1.11 Goalw [SUM_def] "SUM 0 f = (f 0::'a::ring)";
1.12 @@ -164,12 +162,12 @@
1.13 \ SUM n (%i. if i = x then f i else <0>) = (if x <= n then f x else <0>)";
1.14 by (nat_ind_tac "n" 1);
1.15 (* Base case *)
1.16 -by (simp_tac (simpset() setloop (split_tac [expand_if])) 1);
1.17 +by (Simp_tac 1);
1.18 (* Induction step *)
1.19 -by (asm_simp_tac (simpset() setloop (split_tac [expand_if])) 1);
1.20 +by (Asm_simp_tac 1);
1.21 by (Clarify_tac 1);
1.22 by (res_inst_tac [("f", "f")] arg_cong 1);
1.23 -by (fast_arith_tac 1);
1.24 +by (arith_tac 1);
1.25 qed "SUM_if_singleton";
1.26
1.27 Goal
2.1 --- a/src/HOL/Algebra/poly/Degree.ML Thu Nov 11 10:25:17 1999 +0100
2.2 +++ b/src/HOL/Algebra/poly/Degree.ML Thu Nov 11 10:25:29 1999 +0100
2.3 @@ -285,7 +285,7 @@
2.4 by (simp_tac (simpset() addsimps [SUM_if_singleton]) 1);
2.5 by (auto_tac
2.6 (claset() addDs [not_leE],
2.7 - simpset() setloop (split_tac [expand_if])));
2.8 + simpset()));
2.9 qed "bound_SUM_if";
2.10
2.11 Goal
2.12 @@ -297,8 +297,7 @@
2.13 by (full_simp_tac (simpset() addsimps [deg_above_is_bound, coeff_def]) 2);
2.14 by (rtac SUM_cong 1);
2.15 by (rtac refl 1);
2.16 -by (asm_simp_tac
2.17 - (simpset() setloop (split_tac [expand_if])) 1);
2.18 +by (Asm_simp_tac 1);
2.19 qed "up_repr";
2.20
2.21 Goal
3.1 --- a/src/HOL/Algebra/poly/LongDiv.ML Thu Nov 11 10:25:17 1999 +0100
3.2 +++ b/src/HOL/Algebra/poly/LongDiv.ML Thu Nov 11 10:25:29 1999 +0100
3.3 @@ -4,29 +4,6 @@
3.4 Author: Clemens Ballarin, started 23 June 1999
3.5 *)
3.6
3.7 -open LongDiv;
3.8 -
3.9 -(*
3.10 -Goalw [lcoeff_def]
3.11 - "!!p::('a::ring up). \
3.12 -\ [| deg p = deg q; lcoeff p = - (lcoeff q); deg q ~= 0 |] ==> \
3.13 -\ deg (p + q) < deg q";
3.14 -by (res_inst_tac [("j", "deg q - 1")] le_less_trans 1);
3.15 -by (rtac deg_aboveI 1);
3.16 -by (strip_tac 1);
3.17 -by (dtac pred_less_imp_le 1);
3.18 -by (case_tac "deg q = m" 1);
3.19 -by (Clarify_tac 1);
3.20 -by (Asm_full_simp_tac 1);
3.21 -(* case "deg q ~= m" *)
3.22 -by (dtac le_neq_implies_less 1);
3.23 -by (assume_tac 1);
3.24 -by (asm_simp_tac (simpset() addsimps [deg_aboveD]) 1);
3.25 -(* end case *)
3.26 -by (asm_full_simp_tac (simpset() addsimps [le_pred_eq]) 1);
3.27 -qed "deg_lcoeff_cancel";
3.28 -*)
3.29 -
3.30 Goal
3.31 "!!p::('a::ring up). \
3.32 \ [| deg p <= deg r; deg q <= deg r; \
3.33 @@ -86,20 +63,20 @@
3.34 (* case "x ~= <0> *)
3.35 by (rotate_tac ~1 1);
3.36 by (asm_full_simp_tac (simpset() addsimps [eucl_size_def]) 1);
3.37 -by (simp_tac (simpset() addsplits [expand_if]) 1);
3.38 +by (Simp_tac 1);
3.39 by (rtac impI 1);
3.40 by (rtac deg_lcoeff_cancel2 1);
3.41 (* replace by linear arithmetic??? *)
3.42 by (rtac le_trans 1);
3.43 by (rtac deg_smult_ring 1);
3.44 - by (simp_tac (simpset() addsplits [expand_if]) 1);
3.45 + by (Simp_tac 1);
3.46 by (Simp_tac 1);
3.47 by (rtac le_trans 1);
3.48 by (rtac deg_mult_ring 1);
3.49 by (rtac le_trans 1);
3.50 by (rtac add_le_mono1 1);
3.51 by (rtac deg_smult_ring 1);
3.52 - by (asm_simp_tac (simpset() addsimps [leI] addsplits [expand_if]) 1);
3.53 + by (asm_simp_tac (simpset() addsimps [leI]) 1);
3.54 by (SELECT_GOAL Auto_tac 1);
3.55 by (Simp_tac 1);
3.56 by (res_inst_tac [("m", "deg x - deg g"), ("n", "deg x")] SUM_extend 1);
3.57 @@ -155,7 +132,7 @@
3.58 by (rtac disjI2 1);
3.59 by (rtac le_less_trans 1);
3.60 by (rtac deg_smult_ring 1);
3.61 -by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
3.62 +by (Asm_simp_tac 1);
3.63 qed "long_div_unit";
3.64
3.65 Goal
4.1 --- a/src/HOL/Algebra/poly/UnivPoly.ML Thu Nov 11 10:25:17 1999 +0100
4.2 +++ b/src/HOL/Algebra/poly/UnivPoly.ML Thu Nov 11 10:25:29 1999 +0100
4.3 @@ -212,13 +212,13 @@
4.4
4.5 Goal "!! a::'a::ring. const (a + b) = const a + const b";
4.6 by (rtac up_eqI 1);
4.7 -by (simp_tac (simpset() setloop (split_tac [expand_if])) 1);
4.8 +by (Simp_tac 1);
4.9 qed "const_add";
4.10
4.11 Goal "!! a::'a::ring. const (a * b) = const a * const b";
4.12 by (simp_tac (simpset() addsimps [const_mult_is_smult]) 1);
4.13 by (rtac up_eqI 1);
4.14 -by (simp_tac (simpset() setloop (split_tac [expand_if])) 1);
4.15 +by (Simp_tac 1);
4.16 qed "const_mult";
4.17
4.18 Goal "const (<1>::'a::ring) = <1>";
4.19 @@ -228,7 +228,7 @@
4.20
4.21 Goal "const (<0>::'a::ring) = <0>";
4.22 by (rtac up_eqI 1);
4.23 -by (simp_tac (simpset() setloop (split_tac [expand_if])) 1);
4.24 +by (Simp_tac 1);
4.25 qed "const_zero";
4.26
4.27 Addsimps [const_add, const_mult, const_one, const_zero];
5.1 --- a/src/HOL/UNITY/WFair.thy Thu Nov 11 10:25:17 1999 +0100
5.2 +++ b/src/HOL/UNITY/WFair.thy Thu Nov 11 10:25:29 1999 +0100
5.3 @@ -17,17 +17,15 @@
5.4 transient :: "'a set => 'a program set"
5.5 "transient A == {F. EX act: Acts F. A <= Domain act & act^^A <= -A}"
5.6
5.7 + ensures :: "['a set, 'a set] => 'a program set" (infixl 60)
5.8 + "A ensures B == (A-B co A Un B) Int transient (A-B)"
5.9 +
5.10
5.11 consts
5.12
5.13 - ensures :: "['a set, 'a set] => 'a program set" (infixl 60)
5.14 -
5.15 (*LEADS-TO constant for the inductive definition*)
5.16 leads :: "'a program => ('a set * 'a set) set"
5.17
5.18 - (*visible version of the LEADS-TO relation*)
5.19 - leadsTo :: "['a set, 'a set] => 'a program set" (infixl 60)
5.20 -
5.21
5.22 inductive "leads F"
5.23 intrs
5.24 @@ -44,13 +42,11 @@
5.25 monos Pow_mono
5.26
5.27
5.28 -
5.29 -defs
5.30 - ensures_def "A ensures B == (A-B co A Un B) Int transient (A-B)"
5.31 +constdefs
5.32
5.33 - leadsTo_def "A leadsTo B == {F. (A,B) : leads F}"
5.34 -
5.35 -constdefs
5.36 + (*visible version of the LEADS-TO relation*)
5.37 + leadsTo :: "['a set, 'a set] => 'a program set" (infixl 60)
5.38 + "A leadsTo B == {F. (A,B) : leads F}"
5.39
5.40 (*wlt F B is the largest set that leads to B*)
5.41 wlt :: "['a program, 'a set] => 'a set"