Using new "Times" infix
authorpaulson
Thu Apr 04 11:45:01 1996 +0200 (1996-04-04)
changeset 164221db0cf9a1a4
parent 1641 46d2d4a249ca
child 1643 3f83b629f2e3
Using new "Times" infix
src/HOL/Integ/Equiv.ML
src/HOL/Integ/Equiv.thy
src/HOL/Prod.ML
src/HOL/Relation.ML
src/HOL/Sexp.ML
src/HOL/Trancl.ML
src/HOL/Trancl.thy
src/HOL/Univ.ML
src/HOL/WF.ML
src/HOL/ex/Acc.ML
src/HOL/ex/LList.ML
src/HOL/ex/Mutil.ML
     1.1 --- a/src/HOL/Integ/Equiv.ML	Thu Apr 04 11:43:25 1996 +0200
     1.2 +++ b/src/HOL/Integ/Equiv.ML	Thu Apr 04 11:45:01 1996 +0200
     1.3 @@ -82,7 +82,7 @@
     1.4  qed "equiv_class_nondisjoint";
     1.5  
     1.6  val [major] = goalw Equiv.thy [equiv_def,refl_def]
     1.7 -    "equiv A r ==> r <= Sigma A (%x.A)";
     1.8 +    "equiv A r ==> r <= A Times A";
     1.9  by (rtac (major RS conjunct1 RS conjunct1) 1);
    1.10  qed "equiv_type";
    1.11  
     2.1 --- a/src/HOL/Integ/Equiv.thy	Thu Apr 04 11:43:25 1996 +0200
     2.2 +++ b/src/HOL/Integ/Equiv.thy	Thu Apr 04 11:45:01 1996 +0200
     2.3 @@ -18,7 +18,7 @@
     2.4      congruent2  ::      "[('a*'a) set,['a,'a]=>'b]=>bool"
     2.5  
     2.6  defs
     2.7 -    refl_def      "refl A r == r <= Sigma A (%x.A) & (ALL x: A. (x,x) : r)"
     2.8 +    refl_def      "refl A r == r <= A Times A & (ALL x: A. (x,x) : r)"
     2.9      sym_def       "sym(r)    == ALL x y. (x,y): r --> (y,x): r"
    2.10      equiv_def     "equiv A r == refl A r & sym(r) & trans(r)"
    2.11      quotient_def  "A/r == UN x:A. {r^^{x}}"  
     3.1 --- a/src/HOL/Prod.ML	Thu Apr 04 11:43:25 1996 +0200
     3.2 +++ b/src/HOL/Prod.ML	Thu Apr 04 11:45:01 1996 +0200
     3.3 @@ -225,7 +225,7 @@
     3.4      (rtac (major RS SigmaD2) 1) ]);
     3.5  
     3.6  val prems = goal Prod.thy
     3.7 -    "[| A<=C;  !!x. x:A ==> B<=D |] ==> Sigma A (%x.B) <= Sigma C (%x.D)";
     3.8 +    "[| A<=C;  !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D";
     3.9  by (cut_facts_tac prems 1);
    3.10  by (fast_tac (set_cs addIs (prems RL [subsetD]) 
    3.11                       addSIs [SigmaI] 
    3.12 @@ -235,7 +235,7 @@
    3.13  qed_goal "Sigma_empty1" Prod.thy "Sigma {} B = {}"
    3.14   (fn _ => [ (fast_tac (eq_cs addSEs [SigmaE]) 1) ]);
    3.15  
    3.16 -qed_goal "Sigma_empty2" Prod.thy "Sigma A (%x.{}) = {}"
    3.17 +qed_goal "Sigma_empty2" Prod.thy "A Times {} = {}"
    3.18   (fn _ => [ (fast_tac (eq_cs addSEs [SigmaE]) 1) ]);
    3.19  
    3.20  Addsimps [Sigma_empty1,Sigma_empty2]; 
     4.1 --- a/src/HOL/Relation.ML	Thu Apr 04 11:43:25 1996 +0200
     4.2 +++ b/src/HOL/Relation.ML	Thu Apr 04 11:45:01 1996 +0200
     4.3 @@ -62,8 +62,8 @@
     4.4  qed "comp_mono";
     4.5  
     4.6  goal Relation.thy
     4.7 -    "!!r s. [| s <= Sigma A (%x.B);  r <= Sigma B (%x.C) |] ==> \
     4.8 -\           (r O s) <= Sigma A (%x.C)";
     4.9 +    "!!r s. [| s <= A Times B;  r <= B Times C |] ==> \
    4.10 +\           (r O s) <= A Times C";
    4.11  by (fast_tac comp_cs 1);
    4.12  qed "comp_subset_Sigma";
    4.13  
    4.14 @@ -161,7 +161,7 @@
    4.15      (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]);
    4.16  
    4.17  qed_goal "Image_subset" Relation.thy
    4.18 -    "!!A B r. r <= Sigma A (%x.B) ==> r^^C <= B"
    4.19 +    "!!A B r. r <= A Times B ==> r^^C <= B"
    4.20   (fn _ =>
    4.21    [ (rtac subsetI 1),
    4.22      (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ]);
     5.1 --- a/src/HOL/Sexp.ML	Thu Apr 04 11:43:25 1996 +0200
     5.2 +++ b/src/HOL/Sexp.ML	Thu Apr 04 11:45:01 1996 +0200
     5.3 @@ -59,7 +59,7 @@
     5.4  
     5.5  (** Introduction rules for 'pred_sexp' **)
     5.6  
     5.7 -goalw Sexp.thy [pred_sexp_def] "pred_sexp <= Sigma sexp (%u.sexp)";
     5.8 +goalw Sexp.thy [pred_sexp_def] "pred_sexp <= sexp Times sexp";
     5.9  by (fast_tac sexp_cs 1);
    5.10  qed "pred_sexp_subset_Sigma";
    5.11  
     6.1 --- a/src/HOL/Trancl.ML	Thu Apr 04 11:43:25 1996 +0200
     6.2 +++ b/src/HOL/Trancl.ML	Thu Apr 04 11:45:01 1996 +0200
     6.3 @@ -69,10 +69,14 @@
     6.4  qed "rtrancl_induct";
     6.5  
     6.6  (*transitivity of transitive closure!! -- by induction.*)
     6.7 -goal Trancl.thy "!!r. [| (a,b):r^*; (b,c):r^* |] ==> (a,c):r^*";
     6.8 -by (eres_inst_tac [("b","c")] rtrancl_induct 1);
     6.9 +goalw Trancl.thy [trans_def] "trans(r^*)";
    6.10 +by (safe_tac HOL_cs);
    6.11 +by (eres_inst_tac [("b","z")] rtrancl_induct 1);
    6.12  by (ALLGOALS(fast_tac (HOL_cs addIs [rtrancl_into_rtrancl])));
    6.13 -qed "rtrancl_trans";
    6.14 +qed "trans_rtrancl";
    6.15 +
    6.16 +bind_thm ("rtrancl_trans", trans_rtrancl RS transD);
    6.17 +
    6.18  
    6.19  (*elimination of rtrancl -- by induction on a special formula*)
    6.20  val major::prems = goal Trancl.thy
    6.21 @@ -86,15 +90,66 @@
    6.22  by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
    6.23  qed "rtranclE";
    6.24  
    6.25 -goal Trancl.thy "!!R. (y,z):R^* ==> !x. (x,y):R --> (x,z):R^*";
    6.26 +bind_thm ("rtrancl_into_rtrancl2", r_into_rtrancl RS rtrancl_trans);
    6.27 +
    6.28 +
    6.29 +(*** More r^* equations and inclusions ***)
    6.30 +
    6.31 +goal Trancl.thy "(r^*)^* = r^*";
    6.32 +by (rtac set_ext 1);
    6.33 +by (res_inst_tac [("p","x")] PairE 1);
    6.34 +by (hyp_subst_tac 1);
    6.35 +by (rtac iffI 1);
    6.36  by (etac rtrancl_induct 1);
    6.37 -by (fast_tac (HOL_cs addIs [r_into_rtrancl]) 1);
    6.38 -by (fast_tac (HOL_cs addEs [rtrancl_into_rtrancl]) 1);
    6.39 -val lemma = result();
    6.40 +by (rtac rtrancl_refl 1);
    6.41 +by (fast_tac (HOL_cs addEs [rtrancl_trans]) 1);
    6.42 +by (etac r_into_rtrancl 1);
    6.43 +qed "rtrancl_idemp";
    6.44 +Addsimps [rtrancl_idemp];
    6.45 +
    6.46 +goal Trancl.thy "!!r s. r <= s^* ==> r^* <= s^*";
    6.47 +bd rtrancl_mono 1;
    6.48 +by (Asm_full_simp_tac 1);
    6.49 +qed "rtrancl_subset_rtrancl";
    6.50 +
    6.51 +goal Trancl.thy "!!R. [| R <= S; S <= R^* |] ==> S^* = R^*";
    6.52 +by (dtac rtrancl_mono 1);
    6.53 +by (dtac rtrancl_mono 1);
    6.54 +by (Asm_full_simp_tac 1);
    6.55 +by (fast_tac eq_cs 1);
    6.56 +qed "rtrancl_subset";
    6.57 +
    6.58 +goal Trancl.thy "!!R. (R^* Un S^*)^* = (R Un S)^*";
    6.59 +by (best_tac (set_cs addIs [rtrancl_subset,r_into_rtrancl,
    6.60 +                           rtrancl_mono RS subsetD]) 1);
    6.61 +qed "rtrancl_Un_rtrancl";
    6.62  
    6.63 -goal Trancl.thy  "!!R. [| (x,y) : R;  (y,z) : R^* |] ==> (x,z) : R^*";
    6.64 -by (fast_tac (HOL_cs addDs [lemma]) 1);
    6.65 -qed "rtrancl_into_rtrancl2";
    6.66 +goal Trancl.thy "(R^=)^* = R^*";
    6.67 +by (fast_tac (rel_cs addIs [rtrancl_refl,rtrancl_subset,r_into_rtrancl]) 1);
    6.68 +qed "rtrancl_reflcl";
    6.69 +Addsimps [rtrancl_reflcl];
    6.70 +
    6.71 +goal Trancl.thy "!!r. (x,y) : (converse r)^* ==> (x,y) : converse(r^*)";
    6.72 +by (rtac converseI 1);
    6.73 +by (etac rtrancl_induct 1);
    6.74 +by (rtac rtrancl_refl 1);
    6.75 +by (fast_tac (rel_cs addIs [r_into_rtrancl,rtrancl_trans]) 1);
    6.76 +qed "rtrancl_converseD";
    6.77 +
    6.78 +goal Trancl.thy "!!r. (x,y) : converse(r^*) ==> (x,y) : (converse r)^*";
    6.79 +by (dtac converseD 1);
    6.80 +by (etac rtrancl_induct 1);
    6.81 +by (rtac rtrancl_refl 1);
    6.82 +by (fast_tac (rel_cs addIs [r_into_rtrancl,rtrancl_trans]) 1);
    6.83 +qed "rtrancl_converseI";
    6.84 +
    6.85 +goal Trancl.thy "(converse r)^* = converse(r^*)";
    6.86 +by (safe_tac (rel_eq_cs addSIs [rtrancl_converseI]));
    6.87 +by (res_inst_tac [("p","x")] PairE 1);
    6.88 +by (hyp_subst_tac 1);
    6.89 +by (etac rtrancl_converseD 1);
    6.90 +qed "rtrancl_converse";
    6.91 +
    6.92  
    6.93  
    6.94  (**** The relation trancl ****)
    6.95 @@ -129,6 +184,21 @@
    6.96  by (REPEAT (ares_tac (prems@[r_into_rtrancl]) 1));
    6.97  qed "rtrancl_into_trancl2";
    6.98  
    6.99 +(*Nice induction rule for trancl*)
   6.100 +val major::prems = goal Trancl.thy
   6.101 +  "[| (a,b) : r^+;                                      \
   6.102 +\     !!y.  [| (a,y) : r |] ==> P(y);                   \
   6.103 +\     !!y z.[| (a,y) : r^+;  (y,z) : r;  P(y) |] ==> P(z)       \
   6.104 +\  |] ==> P(b)";
   6.105 +by (rtac (rewrite_rule [trancl_def] major  RS  compEpair) 1);
   6.106 +(*by induction on this formula*)
   6.107 +by (subgoal_tac "ALL z. (y,z) : r --> P(z)" 1);
   6.108 +(*now solve first subgoal: this formula is sufficient*)
   6.109 +by (fast_tac HOL_cs 1);
   6.110 +by (etac rtrancl_induct 1);
   6.111 +by (ALLGOALS (fast_tac (set_cs addIs (rtrancl_into_trancl1::prems))));
   6.112 +qed "trancl_induct";
   6.113 +
   6.114  (*elimination of r^+ -- NOT an induction rule*)
   6.115  val major::prems = goal Trancl.thy
   6.116      "[| (a::'a,b) : r^+;  \
   6.117 @@ -152,6 +222,8 @@
   6.118  by (REPEAT (assume_tac 1));
   6.119  qed "trans_trancl";
   6.120  
   6.121 +bind_thm ("trancl_trans", trans_trancl RS transD);
   6.122 +
   6.123  val prems = goal Trancl.thy
   6.124      "[| (a,b) : r;  (b,c) : r^+ |]   ==>  (a,c) : r^+";
   6.125  by (rtac (r_into_trancl RS (trans_trancl RS transD)) 1);
   6.126 @@ -159,71 +231,21 @@
   6.127  by (resolve_tac prems 1);
   6.128  qed "trancl_into_trancl2";
   6.129  
   6.130 -(** More about r^* **)
   6.131 -
   6.132 -goal Trancl.thy "(r^*)^* = r^*";
   6.133 -by (rtac set_ext 1);
   6.134 -by (res_inst_tac [("p","x")] PairE 1);
   6.135 -by (hyp_subst_tac 1);
   6.136 -by (rtac iffI 1);
   6.137 -by (etac rtrancl_induct 1);
   6.138 -by (rtac rtrancl_refl 1);
   6.139 -by (fast_tac (HOL_cs addEs [rtrancl_trans]) 1);
   6.140 -by (etac r_into_rtrancl 1);
   6.141 -qed "rtrancl_idemp";
   6.142 -Addsimps [rtrancl_idemp];
   6.143 -
   6.144 -goal Trancl.thy "!!R. [| R <= S; S <= R^* |] ==> S^* = R^*";
   6.145 -by (dtac rtrancl_mono 1);
   6.146 -by (dtac rtrancl_mono 1);
   6.147 -by (Asm_full_simp_tac 1);
   6.148 -by (fast_tac eq_cs 1);
   6.149 -qed "rtrancl_subset";
   6.150 -
   6.151 -goal Trancl.thy "!!R. (R^* Un S^*)^* = (R Un S)^*";
   6.152 -by (best_tac (set_cs addIs [rtrancl_subset,r_into_rtrancl,
   6.153 -                           rtrancl_mono RS subsetD]) 1);
   6.154 -qed "trancl_Un_trancl";
   6.155 -
   6.156 -goal Trancl.thy "(R^=)^* = R^*";
   6.157 -by (fast_tac (rel_cs addIs [rtrancl_refl,rtrancl_subset,r_into_rtrancl]) 1);
   6.158 -qed "rtrancl_reflcl";
   6.159 -Addsimps [rtrancl_reflcl];
   6.160 -
   6.161 -goal Trancl.thy "!!r. (x,y) : (converse r)^* ==> (x,y) : converse(r^*)";
   6.162 -by (rtac converseI 1);
   6.163 -by (etac rtrancl_induct 1);
   6.164 -by (rtac rtrancl_refl 1);
   6.165 -by (fast_tac (rel_cs addIs [r_into_rtrancl,rtrancl_trans]) 1);
   6.166 -qed "rtrancl_converseD";
   6.167 -
   6.168 -goal Trancl.thy "!!r. (x,y) : converse(r^*) ==> (x,y) : (converse r)^*";
   6.169 -by (dtac converseD 1);
   6.170 -by (etac rtrancl_induct 1);
   6.171 -by (rtac rtrancl_refl 1);
   6.172 -by (fast_tac (rel_cs addIs [r_into_rtrancl,rtrancl_trans]) 1);
   6.173 -qed "rtrancl_converseI";
   6.174 -
   6.175 -goal Trancl.thy "(converse r)^* = converse(r^*)";
   6.176 -by (safe_tac (rel_eq_cs addSIs [rtrancl_converseI]));
   6.177 -by (res_inst_tac [("p","x")] PairE 1);
   6.178 -by (hyp_subst_tac 1);
   6.179 -by (etac rtrancl_converseD 1);
   6.180 -qed "rtrancl_converse";
   6.181 -
   6.182  
   6.183  val major::prems = goal Trancl.thy
   6.184 -    "[| (a,b) : r^*;  r <= Sigma A (%x.A) |] ==> a=b | a:A";
   6.185 +    "[| (a,b) : r^*;  r <= A Times A |] ==> a=b | a:A";
   6.186  by (cut_facts_tac prems 1);
   6.187  by (rtac (major RS rtrancl_induct) 1);
   6.188  by (rtac (refl RS disjI1) 1);
   6.189  by (fast_tac (rel_cs addSEs [SigmaE2]) 1);
   6.190 -qed "trancl_subset_Sigma_lemma";
   6.191 +val lemma = result();
   6.192  
   6.193  goalw Trancl.thy [trancl_def]
   6.194 -    "!!r. r <= Sigma A (%x.A) ==> trancl(r) <= Sigma A (%x.A)";
   6.195 -by (fast_tac (rel_cs addSDs [trancl_subset_Sigma_lemma]) 1);
   6.196 +    "!!r. r <= A Times A ==> r^+ <= A Times A";
   6.197 +by (fast_tac (rel_cs addSDs [lemma]) 1);
   6.198  qed "trancl_subset_Sigma";
   6.199  
   6.200  (* Don't add r_into_rtrancl: it messes up the proofs in Lambda *)
   6.201  val trancl_cs = rel_cs addIs [rtrancl_refl];
   6.202 +
   6.203 +
     7.1 --- a/src/HOL/Trancl.thy	Thu Apr 04 11:43:25 1996 +0200
     7.2 +++ b/src/HOL/Trancl.thy	Thu Apr 04 11:45:01 1996 +0200
     7.3 @@ -5,9 +5,9 @@
     7.4  
     7.5  Relfexive and Transitive closure of a relation
     7.6  
     7.7 -rtrancl is refl&transitive closure;
     7.8 -trancl is transitive closure
     7.9 -reflcl is reflexive closure
    7.10 +rtrancl is reflexive/transitive closure;
    7.11 +trancl  is transitive closure
    7.12 +reflcl  is reflexive closure
    7.13  *)
    7.14  
    7.15  Trancl = Lfp + Relation + 
     8.1 --- a/src/HOL/Univ.ML	Thu Apr 04 11:43:25 1996 +0200
     8.2 +++ b/src/HOL/Univ.ML	Thu Apr 04 11:45:01 1996 +0200
     8.3 @@ -525,11 +525,11 @@
     8.4  
     8.5  (*** Bounding theorems ***)
     8.6  
     8.7 -goal Univ.thy "diag(A) <= Sigma A (%x.A)";
     8.8 +goal Univ.thy "diag(A) <= A Times A";
     8.9  by (fast_tac univ_cs 1);
    8.10  qed "diag_subset_Sigma";
    8.11  
    8.12 -goal Univ.thy "(Sigma A (%x.B) <**> Sigma C (%x.D)) <= Sigma (A<*>C) (%z. B<*>D)";
    8.13 +goal Univ.thy "((A Times B) <**> (C Times D)) <= (A<*>C) Times (B<*>D)";
    8.14  by (fast_tac univ_cs 1);
    8.15  qed "dprod_Sigma";
    8.16  
    8.17 @@ -543,7 +543,7 @@
    8.18  by (fast_tac univ_cs 1);
    8.19  qed "dprod_subset_Sigma2";
    8.20  
    8.21 -goal Univ.thy "(Sigma A (%x.B) <++> Sigma C (%x.D)) <= Sigma (A<+>C) (%z. B<+>D)";
    8.22 +goal Univ.thy "(A Times B <++> C Times D) <= (A<+>C) Times (B<+>D)";
    8.23  by (fast_tac univ_cs 1);
    8.24  qed "dsum_Sigma";
    8.25  
     9.1 --- a/src/HOL/WF.ML	Thu Apr 04 11:43:25 1996 +0200
     9.2 +++ b/src/HOL/WF.ML	Thu Apr 04 11:45:01 1996 +0200
     9.3 @@ -13,7 +13,7 @@
     9.4  
     9.5  (*Restriction to domain A.  If r is well-founded over A then wf(r)*)
     9.6  val [prem1,prem2] = goalw WF.thy [wf_def]
     9.7 - "[| r <= Sigma A (%u.A);  \
     9.8 + "[| r <= A Times A;  \
     9.9  \    !!x P. [| ! x. (! y. (y,x) : r --> P(y)) --> P(x);  x:A |] ==> P(x) |]  \
    9.10  \ ==>  wf(r)";
    9.11  by (strip_tac 1);
    10.1 --- a/src/HOL/ex/Acc.ML	Thu Apr 04 11:43:25 1996 +0200
    10.2 +++ b/src/HOL/ex/Acc.ML	Thu Apr 04 11:45:01 1996 +0200
    10.3 @@ -37,7 +37,7 @@
    10.4  qed "acc_induct";
    10.5  
    10.6  
    10.7 -val [major] = goal Acc.thy "r <= Sigma (acc r) (%u. acc(r)) ==> wf(r)";
    10.8 +val [major] = goal Acc.thy "r <= (acc r) Times (acc r) ==> wf(r)";
    10.9  by (rtac (major RS wfI) 1);
   10.10  by (etac acc.induct 1);
   10.11  by (rewtac pred_def);
   10.12 @@ -51,13 +51,13 @@
   10.13  by (fast_tac set_cs 1);
   10.14  qed "acc_wfD_lemma";
   10.15  
   10.16 -val [major] = goal Acc.thy "wf(r) ==> r <= Sigma (acc r) (%u. acc(r))";
   10.17 +val [major] = goal Acc.thy "wf(r) ==> r <= (acc r) Times (acc r)";
   10.18  by (rtac subsetI 1);
   10.19  by (res_inst_tac [("p", "x")] PairE 1);
   10.20  by (fast_tac (set_cs addSIs [SigmaI,
   10.21                               major RS acc_wfD_lemma RS spec RS mp]) 1);
   10.22  qed "acc_wfD";
   10.23  
   10.24 -goal Acc.thy "wf(r)  =  (r <= Sigma (acc r) (%u. acc(r)))";
   10.25 +goal Acc.thy "wf(r)  =  (r <= (acc r) Times (acc r))";
   10.26  by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]);
   10.27  qed "wf_acc_iff";
    11.1 --- a/src/HOL/ex/LList.ML	Thu Apr 04 11:43:25 1996 +0200
    11.2 +++ b/src/HOL/ex/LList.ML	Thu Apr 04 11:45:01 1996 +0200
    11.3 @@ -133,7 +133,7 @@
    11.4  (*Lemma for the proof of llist_corec*)
    11.5  goal LList.thy
    11.6     "LList_corec a (%z.sum_case Inl (split(%v w.Inr((Leaf(v),w)))) (f z)) : \
    11.7 -\   llist(range(Leaf))";
    11.8 +\   llist(range Leaf)";
    11.9  by (res_inst_tac [("X", "range(%x.LList_corec x ?g)")] llist_coinduct 1);
   11.10  by (rtac rangeI 1);
   11.11  by (safe_tac set_cs);
   11.12 @@ -350,7 +350,7 @@
   11.13  by (rtac Rep_llist_inverse 1);
   11.14  qed "inj_Rep_llist";
   11.15  
   11.16 -goal LList.thy "inj_onto Abs_llist (llist(range(Leaf)))";
   11.17 +goal LList.thy "inj_onto Abs_llist (llist(range Leaf))";
   11.18  by (rtac inj_onto_inverseI 1);
   11.19  by (etac Abs_llist_inverse 1);
   11.20  qed "inj_onto_Abs_llist";
   11.21 @@ -605,8 +605,8 @@
   11.22  (*** Deriving llist_equalityI -- llist equality is a bisimulation ***)
   11.23  
   11.24  goalw LList.thy [LListD_Fun_def]
   11.25 -    "!!r A. r <= Sigma (llist A) (%x.llist(A)) ==> \
   11.26 -\           LListD_Fun (diag A) r <= Sigma (llist A) (%x.llist(A))";
   11.27 +    "!!r A. r <= (llist A) Times (llist A) ==> \
   11.28 +\           LListD_Fun (diag A) r <= (llist A) Times (llist A)";
   11.29  by (stac llist_unfold 1);
   11.30  by (simp_tac (!simpset addsimps [NIL_def, CONS_def]) 1);
   11.31  by (fast_tac univ_cs 1);
   11.32 @@ -614,12 +614,12 @@
   11.33  
   11.34  goal LList.thy
   11.35      "prod_fun Rep_llist Rep_llist `` r <= \
   11.36 -\    Sigma (llist(range(Leaf))) (%x.llist(range(Leaf)))";
   11.37 +\    (llist(range Leaf)) Times (llist(range Leaf))";
   11.38  by (fast_tac (prod_cs addIs [Rep_llist]) 1);
   11.39  qed "subset_Sigma_llist";
   11.40  
   11.41  val [prem] = goal LList.thy
   11.42 -    "r <= Sigma (llist(range Leaf)) (%x.llist(range Leaf)) ==> \
   11.43 +    "r <= (llist(range Leaf)) Times (llist(range Leaf)) ==> \
   11.44  \    prod_fun (Rep_llist o Abs_llist) (Rep_llist o Abs_llist) `` r <= r";
   11.45  by (safe_tac prod_cs);
   11.46  by (rtac (prem RS subsetD RS SigmaE2) 1);
   11.47 @@ -629,7 +629,7 @@
   11.48  
   11.49  goal LList.thy
   11.50      "prod_fun Rep_llist  Rep_llist `` range(%x. (x, x)) = \
   11.51 -\    diag(llist(range(Leaf)))";
   11.52 +\    diag(llist(range Leaf))";
   11.53  by (rtac equalityI 1);
   11.54  by (fast_tac (univ_cs addIs [Rep_llist]) 1);
   11.55  by (fast_tac (univ_cs addSEs [Abs_llist_inverse RS subst]) 1);
    12.1 --- a/src/HOL/ex/Mutil.ML	Thu Apr 04 11:43:25 1996 +0200
    12.2 +++ b/src/HOL/ex/Mutil.ML	Thu Apr 04 11:45:01 1996 +0200
    12.3 @@ -112,26 +112,24 @@
    12.4  by (fast_tac set_cs 1);
    12.5  qed "below_less_iff";
    12.6  
    12.7 -goal thy
    12.8 -    "Sigma (below (Suc A)) B = (Sigma {A} (%x. B(A))) Un Sigma (below A) B";
    12.9 +goal thy "(below (Suc n)) Times B = ({n} Times B) Un ((below n) Times B)";
   12.10  by (simp_tac (!simpset addsimps [below_Suc]) 1);
   12.11  by (fast_tac (prod_cs addIs [equalityI]) 1);
   12.12  qed "Sigma_Suc1";
   12.13  
   12.14 -goal thy
   12.15 -    "Sigma A (%x. below (Suc B)) = Sigma A (%x.{B}) Un Sigma A (%x.below B)";
   12.16 +goal thy "A Times (below (Suc n)) = (A Times {n}) Un (A Times (below n))";
   12.17  by (simp_tac (!simpset addsimps [below_Suc]) 1);
   12.18  by (fast_tac (prod_cs addIs [equalityI]) 1);
   12.19  qed "Sigma_Suc2";
   12.20  
   12.21 -goal thy "Sigma {i} (%x. below (n + n)) : tiling domino";
   12.22 +goal thy "{i} Times (below (n + n)) : tiling domino";
   12.23  by (nat_ind_tac "n" 1);
   12.24  by (simp_tac (!simpset addsimps tiling.intrs) 1);
   12.25  by (asm_simp_tac (!simpset addsimps [Un_assoc RS sym, Sigma_Suc2]) 1);
   12.26  by (resolve_tac tiling.intrs 1);
   12.27  by (assume_tac 2);
   12.28  by (subgoal_tac    (*seems the easiest way of turning one to the other*)
   12.29 -    "Sigma {i} (%x. {Suc(n1+n1)}) Un Sigma {i} (%x. {n1+n1}) = \
   12.30 +    "({i} Times {Suc(n1+n1)}) Un ({i} Times {n1+n1}) = \
   12.31  \    {(i, n1+n1), (i, Suc(n1+n1))}" 1);
   12.32  by (fast_tac (prod_cs addIs [equalityI]) 2);
   12.33  by (asm_simp_tac (!simpset addsimps [domino.horiz]) 1);
   12.34 @@ -139,7 +137,7 @@
   12.35                        addDs [below_less_iff RS iffD1]) 1);
   12.36  qed "dominoes_tile_row";
   12.37  
   12.38 -goal thy "Sigma (below m) (%x. below (n + n)) : tiling domino";
   12.39 +goal thy "(below m) Times (below (n + n)) : tiling domino";
   12.40  by (nat_ind_tac "m" 1);
   12.41  by (simp_tac (!simpset addsimps (below_0::tiling.intrs)) 1);
   12.42  by (asm_simp_tac (!simpset addsimps [Sigma_Suc1]) 1);
   12.43 @@ -148,8 +146,8 @@
   12.44  qed "dominoes_tile_matrix";
   12.45  
   12.46  
   12.47 -goal thy "!!m n. [| t = Sigma (below (Suc m + Suc m))\
   12.48 -\                             (%x. below (Suc n + Suc n));          \
   12.49 +goal thy "!!m n. [| t = (below (Suc m + Suc m))  Times              \
   12.50 +\                       (below (Suc n + Suc n));                    \
   12.51  \                   t' = t - {(0,0)} - {(Suc(m+m), Suc(n+n))}       \
   12.52  \                |] ==> t' ~: tiling domino";
   12.53  by (rtac notI 1);