Univ.ML

--- a/Univ.ML	Thu Aug 18 12:13:26 1994 +0200
+++ b/Univ.ML	Thu Aug 18 12:23:52 1994 +0200
@@ -263,7 +263,7 @@
 by (etac less_zeroE 1);
 val ndepth_K0 = result();
 
-goal Univ.thy "k < Suc(LEAST x. f(x)=0) --> nat_case(k, Suc(i), f) ~= 0";
+goal Univ.thy "k < Suc(LEAST x. f(x)=0) --> nat_case(Suc(i), f, k) ~= 0";
 by (nat_ind_tac "k" 1);
 by (ALLGOALS (simp_tac nat_ss));
 by (rtac impI 1);
@@ -457,16 +457,16 @@
 
 (*** Split and Case ***)
 
-goalw Univ.thy [Split_def] "Split(M$N, c) = c(M,N)";
+goalw Univ.thy [Split_def] "Split(c, M$N) = c(M,N)";
 by (fast_tac (set_cs addIs [select_equality] addEs [Scons_inject]) 1);
 val Split = result();
 
-goalw Univ.thy [Case_def] "Case(In0(M), c, d) = c(M)";
+goalw Univ.thy [Case_def] "Case(c, d, In0(M)) = c(M)";
 by (fast_tac (set_cs addIs [select_equality] 
 		     addEs [make_elim In0_inject, In0_neq_In1]) 1);
 val Case_In0 = result();
 
-goalw Univ.thy [Case_def] "Case(In1(N), c, d) = d(N)";
+goalw Univ.thy [Case_def] "Case(c, d, In1(N)) = d(N)";
 by (fast_tac (set_cs addIs [select_equality] 
 		     addEs [make_elim In1_inject, In1_neq_In0]) 1);
 val Case_In1 = result();
@@ -511,15 +511,9 @@
 
 (*** Equality for Cartesian Product ***)
 
-goal Univ.thy
- "split(<M,M'>, %x x'. split(<N,N'>, %y y'. {<x$y,x'$y'>})) = {<M$N, M'$N'>}";
-by (simp_tac univ_ss 1);
-val dprod_lemma = result();
-
 goalw Univ.thy [dprod_def]
     "!!r s. [| <M,M'>:r;  <N,N'>:s |] ==> <M$N, M'$N'> : r<**>s";
-by (REPEAT (ares_tac [UN_I] 1));
-by (rtac (singletonI RS (dprod_lemma RS equalityD2 RS subsetD)) 1);
+by (fast_tac prod_cs 1);
 val dprodI = result();
 
 (*The general elimination rule*)
@@ -528,23 +522,19 @@
 \       !!x y x' y'. [| <x,x'> : r;  <y,y'> : s;  c = <x$y,x'$y'> |] ==> P \
 \    |] ==> P";
 by (cut_facts_tac [major] 1);
-by (REPEAT (eresolve_tac [asm_rl,singletonE,UN_E] 1));
-by (res_inst_tac [("p","u")] PairE 1);
-by (res_inst_tac [("p","v")] PairE 1);
-by (safe_tac HOL_cs);
-by (REPEAT (ares_tac prems 1));
-by (safe_tac (set_cs addSDs [dprod_lemma RS equalityD1 RS subsetD]));
+by (REPEAT_FIRST (eresolve_tac [asm_rl, UN_E, mem_splitE, singletonE]));
+by (REPEAT (ares_tac prems 1 ORELSE hyp_subst_tac 1));
 val dprodE = result();
 
 
 (*** Equality for Disjoint Sum ***)
 
 goalw Univ.thy [dsum_def]  "!!r. <M,M'>:r ==> <In0(M), In0(M')> : r<++>s";
-by (fast_tac (set_cs addSIs [split RS equalityD2 RS subsetD]) 1);
+by (fast_tac prod_cs 1);
 val dsum_In0I = result();
 
 goalw Univ.thy [dsum_def]  "!!r. <N,N'>:s ==> <In1(N), In1(N')> : r<++>s";
-by (fast_tac (set_cs addSIs [split RS equalityD2 RS subsetD]) 1);
+by (fast_tac prod_cs 1);
 val dsum_In1I = result();
 
 val major::prems = goalw Univ.thy [dsum_def]
@@ -552,78 +542,72 @@
 \       !!x x'. [| <x,x'> : r;  w = <In0(x), In0(x')> |] ==> P; \
 \       !!y y'. [| <y,y'> : s;  w = <In1(y), In1(y')> |] ==> P \
 \    |] ==> P";
-by (rtac (major RS UnE) 1);
-by (safe_tac set_cs);
-by (res_inst_tac [("p","u")] PairE 1);
-by (res_inst_tac [("p","v")] PairE 2);
-by (safe_tac (set_cs addSEs prems 
-                     addSDs [split RS equalityD1 RS subsetD]));
+by (cut_facts_tac [major] 1);
+by (REPEAT_FIRST (eresolve_tac [asm_rl, UN_E, UnE, mem_splitE, singletonE]));
+by (DEPTH_SOLVE (ares_tac prems 1 ORELSE hyp_subst_tac 1));
 val dsumE = result();
 
 
+val univ_cs =
+    prod_cs addSIs [diagI, uprodI, dprodI]
+            addIs  [usum_In0I, usum_In1I, dsum_In0I, dsum_In1I]
+            addSEs [diagE, uprodE, dprodE, usumE, dsumE];
+
+
 (*** Monotonicity ***)
 
-goalw Univ.thy [dprod_def] "!!r s. [| r<=r';  s<=s' |] ==> r<**>s <= r'<**>s'";
-by (fast_tac set_cs 1);
+goal Univ.thy "!!r s. [| r<=r';  s<=s' |] ==> r<**>s <= r'<**>s'";
+by (fast_tac univ_cs 1);
 val dprod_mono = result();
 
-goalw Univ.thy [dsum_def] "!!r s. [| r<=r';  s<=s' |] ==> r<++>s <= r'<++>s'";
-by (fast_tac set_cs 1);
+goal Univ.thy "!!r s. [| r<=r';  s<=s' |] ==> r<++>s <= r'<++>s'";
+by (fast_tac univ_cs 1);
 val dsum_mono = result();
 
 
 (*** Bounding theorems ***)
 
 goal Univ.thy "diag(A) <= Sigma(A,%x.A)";
-by (fast_tac (set_cs addIs [SigmaI] addSEs [diagE]) 1);
+by (fast_tac univ_cs 1);
 val diag_subset_Sigma = result();
 
-val prems = goal Univ.thy
-    "[| r <= Sigma(A,%x.B);  s <= Sigma(C,%x.D) |] ==> \
-\    (r<**>s) <= Sigma(A<*>C, %z. B<*>D)";
-by (cut_facts_tac prems 1);
-by (fast_tac (set_cs addSIs [SigmaI,uprodI]
-                     addSEs [dprodE,SigmaE2]) 1);
-val dprod_subset_Sigma = result();
+goal Univ.thy "(Sigma(A,%x.B) <**> Sigma(C,%x.D)) <= Sigma(A<*>C, %z. B<*>D)";
+by (fast_tac univ_cs 1);
+val dprod_Sigma = result();
+
+val dprod_subset_Sigma = [dprod_mono, dprod_Sigma] MRS subset_trans |>standard;
 
+(*Dependent version*)
 goal Univ.thy
-    "!!r s. [| r <= Sigma(A,B);  s <= Sigma(C,D) |] ==> \
-\           (r<**>s) <= Sigma(A<*>C, %z. Split(z, %x y. B(x)<*>D(y)))";
-by (safe_tac (set_cs addSIs [SigmaI,uprodI] addSEs [dprodE]));
-by (stac Split 3);
-by (ALLGOALS (fast_tac (set_cs addSIs [uprodI] addSEs [SigmaE2])));
+    "(Sigma(A,B) <**> Sigma(C,D)) <= Sigma(A<*>C, Split(%x y. B(x)<*>D(y)))";
+by (safe_tac univ_cs);
+by (stac Split 1);
+by (fast_tac univ_cs 1);
 val dprod_subset_Sigma2 = result();
 
-goal Univ.thy
-    "!!r s. [| r <= Sigma(A,%x.B);  s <= Sigma(C,%x.D) |] ==> \
-\           (r<++>s) <= Sigma(A<+>C, %z. B<+>D)";
-by (fast_tac (set_cs addSIs [SigmaI,usum_In0I,usum_In1I]
-                     addSEs [dsumE,SigmaE2]) 1);
-val dsum_subset_Sigma = result();
+goal Univ.thy "(Sigma(A,%x.B) <++> Sigma(C,%x.D)) <= Sigma(A<+>C, %z. B<+>D)";
+by (fast_tac univ_cs 1);
+val dsum_Sigma = result();
+
+val dsum_subset_Sigma = [dsum_mono, dsum_Sigma] MRS subset_trans |> standard;
 
 
 (*** Domain ***)
 
 goal Univ.thy "fst `` diag(A) = A";
-by (fast_tac (set_cs addIs [equalityI, fst_imageI, diagI]
-                     addSEs [fst_imageE, Pair_inject, diagE]) 1);
+by (fast_tac (prod_cs addIs [equalityI, diagI] addSEs [diagE]) 1);
 val fst_image_diag = result();
 
 goal Univ.thy "fst `` (r<**>s) = (fst``r) <*> (fst``s)";
-by (fast_tac (set_cs addIs [equalityI, fst_imageI, uprodI, dprodI]
-                     addSEs [fst_imageE, Pair_inject, uprodE, dprodE]) 1);
+by (fast_tac (prod_cs addIs [equalityI, uprodI, dprodI]
+                     addSEs [uprodE, dprodE]) 1);
 val fst_image_dprod = result();
 
 goal Univ.thy "fst `` (r<++>s) = (fst``r) <+> (fst``s)";
-by (fast_tac (set_cs addIs [equalityI, fst_imageI, usum_In0I, usum_In1I, 
+by (fast_tac (prod_cs addIs [equalityI, usum_In0I, usum_In1I, 
 			     dsum_In0I, dsum_In1I]
-                     addSEs [fst_imageE, Pair_inject, usumE, dsumE]) 1);
+                     addSEs [usumE, dsumE]) 1);
 val fst_image_dsum = result();
 
 val fst_image_simps = [fst_image_diag, fst_image_dprod, fst_image_dsum];
 val fst_image_ss = univ_ss addsimps fst_image_simps;
-
-val univ_cs =
-    set_cs addSIs [SigmaI,uprodI,dprodI]
-           addIs [usum_In0I,usum_In1I,dsum_In0I,dsum_In1I]
-           addSEs [diagE,uprodE,dprodE,usumE,dsumE,SigmaE2,Pair_inject];