tidied
authorpaulson
Thu Nov 11 10:25:29 1999 +0100 (1999-11-11)
changeset 8006299127ded09d
parent 8005 b64d86018785
child 8007 c29e27ee4933
tidied
src/HOL/Algebra/abstract/NatSum.ML
src/HOL/Algebra/poly/Degree.ML
src/HOL/Algebra/poly/LongDiv.ML
src/HOL/Algebra/poly/UnivPoly.ML
src/HOL/UNITY/WFair.thy
     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"