# HG changeset patch
# User lcp
# Date 777205432 -7200
# Node ID 361521bc7c47c763ffabb973f10b4e25ae82d96f
# Parent  7c6476c53a6c4359fc1fd2553026969ea9f04a58
HOL/Univ: swapped args of split and simplified
HOL/Univ: simplified many proofs involving dprod, dsum.
HOL/Univ: updated to new nat_case
HOL/Univ/univ_cs: added to it and used it more

diff -r 7c6476c53a6c -r 361521bc7c47 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];
diff -r 7c6476c53a6c -r 361521bc7c47 Univ.thy
--- a/Univ.thy	Thu Aug 18 12:13:26 1994 +0200
+++ b/Univ.thy	Thu Aug 18 12:23:52 1994 +0200
@@ -11,7 +11,7 @@
 Could <*> be generalized to a general summation (Sigma)?
 *)
 
-Univ = Arith +
+Univ = Arith + Sum + 
 
 types
   'a node
@@ -42,8 +42,8 @@
   "<*>"  :: "['a node set set, 'a node set set]=> 'a node set set" (infixr 80)
   "<+>"  :: "['a node set set, 'a node set set]=> 'a node set set" (infixr 70)
 
-  Split	 :: "['a node set, ['a node set, 'a node set]=>'b] => 'b"
-  Case   :: "['a node set, ['a node set]=>'b, ['a node set]=>'b] => 'b"
+  Split	 :: "[['a node set, 'a node set]=>'b, 'a node set] => 'b"
+  Case   :: "[['a node set]=>'b, ['a node set]=>'b, 'a node set] => 'b"
 
   diag   :: "'a set => ('a * 'a)set"
   "<**>" :: "[('a node set * 'a node set)set, ('a node set * 'a node set)set] \
@@ -65,8 +65,8 @@
   Push_Node_def    "Push_Node == (%n x. Abs_Node (apfst(Push(n),Rep_Node(x))))"
 
   (*crude "lists" of nats -- needed for the constructions*)
-  apfst_def  "apfst == (%f p.split(p, %x y. <f(x),y>))"
-  Push_def   "Push == (%b h n. nat_case(n,Suc(b),h))"
+  apfst_def  "apfst == (%f. split(%x y. <f(x),y>))"
+  Push_def   "Push == (%b h. nat_case(Suc(b),h))"
 
   (** operations on S-expressions -- sets of nodes **)
 
@@ -83,7 +83,7 @@
   In1_def    "In1(M) == Numb(Suc(0)) $ M"
 
   (*the set of nodes with depth less than k*)
-  ndepth_def "ndepth(n) == split(Rep_Node(n), %f x. LEAST k. f(k)=0)"
+  ndepth_def "ndepth(n) == split(%f x. LEAST k. f(k)=0, Rep_Node(n))"
   ntrunc_def "ntrunc(k,N) == {n. n:N & ndepth(n)<k}"
 
   (*products and sums for the "universe"*)
@@ -91,9 +91,9 @@
   usum_def   "A<+>B == In0``A Un In1``B"
 
   (*the corresponding eliminators*)
-  Split_def  "Split(M,c) == @u. ? x y. M = x$y & u = c(x,y)"
+  Split_def  "Split(c,M) == @u. ? x y. M = x$y & u = c(x,y)"
 
-  Case_def   "Case(M,c,d) == @u.  (? x . M = In0(x) & u = c(x))	\
+  Case_def   "Case(c,d,M) == @u.  (? x . M = In0(x) & u = c(x))	\
 \	   	                | (? y . M = In1(y) & u = d(y))"
 
 
@@ -101,10 +101,10 @@
 
   diag_def   "diag(A) == UN x:A. {<x,x>}"
 
-  dprod_def  "r<**>s == UN u:r. UN v:s. \
-\                       split(u, %x x'. split(v, %y y'. {<x$y,x'$y'>}))"
+  dprod_def  "r<**>s == UN u:r. split(%x x'. \
+\                       UN v:s. split(%y y'. {<x$y,x'$y'>}, v), u)"
 
-  dsum_def   "r<++>s == (UN u:r. split(u, %x x'. {<In0(x),In0(x')>})) Un \
-\                       (UN v:s. split(v, %y y'. {<In1(y),In1(y')>}))"
+  dsum_def   "r<++>s == (UN u:r. split(%x x'. {<In0(x),In0(x')>}, u)) Un \
+\                       (UN v:s. split(%y y'. {<In1(y),In1(y')>}, v))"
 
 end