--- 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];
--- 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