--- a/src/HOL/Integ/Equiv.ML Thu Apr 04 11:43:25 1996 +0200
+++ b/src/HOL/Integ/Equiv.ML Thu Apr 04 11:45:01 1996 +0200
@@ -82,7 +82,7 @@
qed "equiv_class_nondisjoint";
val [major] = goalw Equiv.thy [equiv_def,refl_def]
- "equiv A r ==> r <= Sigma A (%x.A)";
+ "equiv A r ==> r <= A Times A";
by (rtac (major RS conjunct1 RS conjunct1) 1);
qed "equiv_type";
--- a/src/HOL/Integ/Equiv.thy Thu Apr 04 11:43:25 1996 +0200
+++ b/src/HOL/Integ/Equiv.thy Thu Apr 04 11:45:01 1996 +0200
@@ -18,7 +18,7 @@
congruent2 :: "[('a*'a) set,['a,'a]=>'b]=>bool"
defs
- refl_def "refl A r == r <= Sigma A (%x.A) & (ALL x: A. (x,x) : r)"
+ refl_def "refl A r == r <= A Times A & (ALL x: A. (x,x) : r)"
sym_def "sym(r) == ALL x y. (x,y): r --> (y,x): r"
equiv_def "equiv A r == refl A r & sym(r) & trans(r)"
quotient_def "A/r == UN x:A. {r^^{x}}"
--- a/src/HOL/Prod.ML Thu Apr 04 11:43:25 1996 +0200
+++ b/src/HOL/Prod.ML Thu Apr 04 11:45:01 1996 +0200
@@ -225,7 +225,7 @@
(rtac (major RS SigmaD2) 1) ]);
val prems = goal Prod.thy
- "[| A<=C; !!x. x:A ==> B<=D |] ==> Sigma A (%x.B) <= Sigma C (%x.D)";
+ "[| A<=C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D";
by (cut_facts_tac prems 1);
by (fast_tac (set_cs addIs (prems RL [subsetD])
addSIs [SigmaI]
@@ -235,7 +235,7 @@
qed_goal "Sigma_empty1" Prod.thy "Sigma {} B = {}"
(fn _ => [ (fast_tac (eq_cs addSEs [SigmaE]) 1) ]);
-qed_goal "Sigma_empty2" Prod.thy "Sigma A (%x.{}) = {}"
+qed_goal "Sigma_empty2" Prod.thy "A Times {} = {}"
(fn _ => [ (fast_tac (eq_cs addSEs [SigmaE]) 1) ]);
Addsimps [Sigma_empty1,Sigma_empty2];
--- a/src/HOL/Relation.ML Thu Apr 04 11:43:25 1996 +0200
+++ b/src/HOL/Relation.ML Thu Apr 04 11:45:01 1996 +0200
@@ -62,8 +62,8 @@
qed "comp_mono";
goal Relation.thy
- "!!r s. [| s <= Sigma A (%x.B); r <= Sigma B (%x.C) |] ==> \
-\ (r O s) <= Sigma A (%x.C)";
+ "!!r s. [| s <= A Times B; r <= B Times C |] ==> \
+\ (r O s) <= A Times C";
by (fast_tac comp_cs 1);
qed "comp_subset_Sigma";
@@ -161,7 +161,7 @@
(REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]);
qed_goal "Image_subset" Relation.thy
- "!!A B r. r <= Sigma A (%x.B) ==> r^^C <= B"
+ "!!A B r. r <= A Times B ==> r^^C <= B"
(fn _ =>
[ (rtac subsetI 1),
(REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ]);
--- a/src/HOL/Sexp.ML Thu Apr 04 11:43:25 1996 +0200
+++ b/src/HOL/Sexp.ML Thu Apr 04 11:45:01 1996 +0200
@@ -59,7 +59,7 @@
(** Introduction rules for 'pred_sexp' **)
-goalw Sexp.thy [pred_sexp_def] "pred_sexp <= Sigma sexp (%u.sexp)";
+goalw Sexp.thy [pred_sexp_def] "pred_sexp <= sexp Times sexp";
by (fast_tac sexp_cs 1);
qed "pred_sexp_subset_Sigma";
--- a/src/HOL/Trancl.ML Thu Apr 04 11:43:25 1996 +0200
+++ b/src/HOL/Trancl.ML Thu Apr 04 11:45:01 1996 +0200
@@ -69,10 +69,14 @@
qed "rtrancl_induct";
(*transitivity of transitive closure!! -- by induction.*)
-goal Trancl.thy "!!r. [| (a,b):r^*; (b,c):r^* |] ==> (a,c):r^*";
-by (eres_inst_tac [("b","c")] rtrancl_induct 1);
+goalw Trancl.thy [trans_def] "trans(r^*)";
+by (safe_tac HOL_cs);
+by (eres_inst_tac [("b","z")] rtrancl_induct 1);
by (ALLGOALS(fast_tac (HOL_cs addIs [rtrancl_into_rtrancl])));
-qed "rtrancl_trans";
+qed "trans_rtrancl";
+
+bind_thm ("rtrancl_trans", trans_rtrancl RS transD);
+
(*elimination of rtrancl -- by induction on a special formula*)
val major::prems = goal Trancl.thy
@@ -86,15 +90,66 @@
by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
qed "rtranclE";
-goal Trancl.thy "!!R. (y,z):R^* ==> !x. (x,y):R --> (x,z):R^*";
+bind_thm ("rtrancl_into_rtrancl2", r_into_rtrancl RS rtrancl_trans);
+
+
+(*** More r^* equations and inclusions ***)
+
+goal Trancl.thy "(r^*)^* = r^*";
+by (rtac set_ext 1);
+by (res_inst_tac [("p","x")] PairE 1);
+by (hyp_subst_tac 1);
+by (rtac iffI 1);
by (etac rtrancl_induct 1);
-by (fast_tac (HOL_cs addIs [r_into_rtrancl]) 1);
-by (fast_tac (HOL_cs addEs [rtrancl_into_rtrancl]) 1);
-val lemma = result();
+by (rtac rtrancl_refl 1);
+by (fast_tac (HOL_cs addEs [rtrancl_trans]) 1);
+by (etac r_into_rtrancl 1);
+qed "rtrancl_idemp";
+Addsimps [rtrancl_idemp];
+
+goal Trancl.thy "!!r s. r <= s^* ==> r^* <= s^*";
+bd rtrancl_mono 1;
+by (Asm_full_simp_tac 1);
+qed "rtrancl_subset_rtrancl";
+
+goal Trancl.thy "!!R. [| R <= S; S <= R^* |] ==> S^* = R^*";
+by (dtac rtrancl_mono 1);
+by (dtac rtrancl_mono 1);
+by (Asm_full_simp_tac 1);
+by (fast_tac eq_cs 1);
+qed "rtrancl_subset";
+
+goal Trancl.thy "!!R. (R^* Un S^*)^* = (R Un S)^*";
+by (best_tac (set_cs addIs [rtrancl_subset,r_into_rtrancl,
+ rtrancl_mono RS subsetD]) 1);
+qed "rtrancl_Un_rtrancl";
-goal Trancl.thy "!!R. [| (x,y) : R; (y,z) : R^* |] ==> (x,z) : R^*";
-by (fast_tac (HOL_cs addDs [lemma]) 1);
-qed "rtrancl_into_rtrancl2";
+goal Trancl.thy "(R^=)^* = R^*";
+by (fast_tac (rel_cs addIs [rtrancl_refl,rtrancl_subset,r_into_rtrancl]) 1);
+qed "rtrancl_reflcl";
+Addsimps [rtrancl_reflcl];
+
+goal Trancl.thy "!!r. (x,y) : (converse r)^* ==> (x,y) : converse(r^*)";
+by (rtac converseI 1);
+by (etac rtrancl_induct 1);
+by (rtac rtrancl_refl 1);
+by (fast_tac (rel_cs addIs [r_into_rtrancl,rtrancl_trans]) 1);
+qed "rtrancl_converseD";
+
+goal Trancl.thy "!!r. (x,y) : converse(r^*) ==> (x,y) : (converse r)^*";
+by (dtac converseD 1);
+by (etac rtrancl_induct 1);
+by (rtac rtrancl_refl 1);
+by (fast_tac (rel_cs addIs [r_into_rtrancl,rtrancl_trans]) 1);
+qed "rtrancl_converseI";
+
+goal Trancl.thy "(converse r)^* = converse(r^*)";
+by (safe_tac (rel_eq_cs addSIs [rtrancl_converseI]));
+by (res_inst_tac [("p","x")] PairE 1);
+by (hyp_subst_tac 1);
+by (etac rtrancl_converseD 1);
+qed "rtrancl_converse";
+
(**** The relation trancl ****)
@@ -129,6 +184,21 @@
by (REPEAT (ares_tac (prems@[r_into_rtrancl]) 1));
qed "rtrancl_into_trancl2";
+(*Nice induction rule for trancl*)
+val major::prems = goal Trancl.thy
+ "[| (a,b) : r^+; \
+\ !!y. [| (a,y) : r |] ==> P(y); \
+\ !!y z.[| (a,y) : r^+; (y,z) : r; P(y) |] ==> P(z) \
+\ |] ==> P(b)";
+by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1);
+(*by induction on this formula*)
+by (subgoal_tac "ALL z. (y,z) : r --> P(z)" 1);
+(*now solve first subgoal: this formula is sufficient*)
+by (fast_tac HOL_cs 1);
+by (etac rtrancl_induct 1);
+by (ALLGOALS (fast_tac (set_cs addIs (rtrancl_into_trancl1::prems))));
+qed "trancl_induct";
+
(*elimination of r^+ -- NOT an induction rule*)
val major::prems = goal Trancl.thy
"[| (a::'a,b) : r^+; \
@@ -152,6 +222,8 @@
by (REPEAT (assume_tac 1));
qed "trans_trancl";
+bind_thm ("trancl_trans", trans_trancl RS transD);
+
val prems = goal Trancl.thy
"[| (a,b) : r; (b,c) : r^+ |] ==> (a,c) : r^+";
by (rtac (r_into_trancl RS (trans_trancl RS transD)) 1);
@@ -159,71 +231,21 @@
by (resolve_tac prems 1);
qed "trancl_into_trancl2";
-(** More about r^* **)
-
-goal Trancl.thy "(r^*)^* = r^*";
-by (rtac set_ext 1);
-by (res_inst_tac [("p","x")] PairE 1);
-by (hyp_subst_tac 1);
-by (rtac iffI 1);
-by (etac rtrancl_induct 1);
-by (rtac rtrancl_refl 1);
-by (fast_tac (HOL_cs addEs [rtrancl_trans]) 1);
-by (etac r_into_rtrancl 1);
-qed "rtrancl_idemp";
-Addsimps [rtrancl_idemp];
-
-goal Trancl.thy "!!R. [| R <= S; S <= R^* |] ==> S^* = R^*";
-by (dtac rtrancl_mono 1);
-by (dtac rtrancl_mono 1);
-by (Asm_full_simp_tac 1);
-by (fast_tac eq_cs 1);
-qed "rtrancl_subset";
-
-goal Trancl.thy "!!R. (R^* Un S^*)^* = (R Un S)^*";
-by (best_tac (set_cs addIs [rtrancl_subset,r_into_rtrancl,
- rtrancl_mono RS subsetD]) 1);
-qed "trancl_Un_trancl";
-
-goal Trancl.thy "(R^=)^* = R^*";
-by (fast_tac (rel_cs addIs [rtrancl_refl,rtrancl_subset,r_into_rtrancl]) 1);
-qed "rtrancl_reflcl";
-Addsimps [rtrancl_reflcl];
-
-goal Trancl.thy "!!r. (x,y) : (converse r)^* ==> (x,y) : converse(r^*)";
-by (rtac converseI 1);
-by (etac rtrancl_induct 1);
-by (rtac rtrancl_refl 1);
-by (fast_tac (rel_cs addIs [r_into_rtrancl,rtrancl_trans]) 1);
-qed "rtrancl_converseD";
-
-goal Trancl.thy "!!r. (x,y) : converse(r^*) ==> (x,y) : (converse r)^*";
-by (dtac converseD 1);
-by (etac rtrancl_induct 1);
-by (rtac rtrancl_refl 1);
-by (fast_tac (rel_cs addIs [r_into_rtrancl,rtrancl_trans]) 1);
-qed "rtrancl_converseI";
-
-goal Trancl.thy "(converse r)^* = converse(r^*)";
-by (safe_tac (rel_eq_cs addSIs [rtrancl_converseI]));
-by (res_inst_tac [("p","x")] PairE 1);
-by (hyp_subst_tac 1);
-by (etac rtrancl_converseD 1);
-qed "rtrancl_converse";
-
val major::prems = goal Trancl.thy
- "[| (a,b) : r^*; r <= Sigma A (%x.A) |] ==> a=b | a:A";
+ "[| (a,b) : r^*; r <= A Times A |] ==> a=b | a:A";
by (cut_facts_tac prems 1);
by (rtac (major RS rtrancl_induct) 1);
by (rtac (refl RS disjI1) 1);
by (fast_tac (rel_cs addSEs [SigmaE2]) 1);
-qed "trancl_subset_Sigma_lemma";
+val lemma = result();
goalw Trancl.thy [trancl_def]
- "!!r. r <= Sigma A (%x.A) ==> trancl(r) <= Sigma A (%x.A)";
-by (fast_tac (rel_cs addSDs [trancl_subset_Sigma_lemma]) 1);
+ "!!r. r <= A Times A ==> r^+ <= A Times A";
+by (fast_tac (rel_cs addSDs [lemma]) 1);
qed "trancl_subset_Sigma";
(* Don't add r_into_rtrancl: it messes up the proofs in Lambda *)
val trancl_cs = rel_cs addIs [rtrancl_refl];
+
+
--- a/src/HOL/Trancl.thy Thu Apr 04 11:43:25 1996 +0200
+++ b/src/HOL/Trancl.thy Thu Apr 04 11:45:01 1996 +0200
@@ -5,9 +5,9 @@
Relfexive and Transitive closure of a relation
-rtrancl is refl&transitive closure;
-trancl is transitive closure
-reflcl is reflexive closure
+rtrancl is reflexive/transitive closure;
+trancl is transitive closure
+reflcl is reflexive closure
*)
Trancl = Lfp + Relation +
--- a/src/HOL/Univ.ML Thu Apr 04 11:43:25 1996 +0200
+++ b/src/HOL/Univ.ML Thu Apr 04 11:45:01 1996 +0200
@@ -525,11 +525,11 @@
(*** Bounding theorems ***)
-goal Univ.thy "diag(A) <= Sigma A (%x.A)";
+goal Univ.thy "diag(A) <= A Times A";
by (fast_tac univ_cs 1);
qed "diag_subset_Sigma";
-goal Univ.thy "(Sigma A (%x.B) <**> Sigma C (%x.D)) <= Sigma (A<*>C) (%z. B<*>D)";
+goal Univ.thy "((A Times B) <**> (C Times D)) <= (A<*>C) Times (B<*>D)";
by (fast_tac univ_cs 1);
qed "dprod_Sigma";
@@ -543,7 +543,7 @@
by (fast_tac univ_cs 1);
qed "dprod_subset_Sigma2";
-goal Univ.thy "(Sigma A (%x.B) <++> Sigma C (%x.D)) <= Sigma (A<+>C) (%z. B<+>D)";
+goal Univ.thy "(A Times B <++> C Times D) <= (A<+>C) Times (B<+>D)";
by (fast_tac univ_cs 1);
qed "dsum_Sigma";
--- a/src/HOL/WF.ML Thu Apr 04 11:43:25 1996 +0200
+++ b/src/HOL/WF.ML Thu Apr 04 11:45:01 1996 +0200
@@ -13,7 +13,7 @@
(*Restriction to domain A. If r is well-founded over A then wf(r)*)
val [prem1,prem2] = goalw WF.thy [wf_def]
- "[| r <= Sigma A (%u.A); \
+ "[| r <= A Times A; \
\ !!x P. [| ! x. (! y. (y,x) : r --> P(y)) --> P(x); x:A |] ==> P(x) |] \
\ ==> wf(r)";
by (strip_tac 1);
--- a/src/HOL/ex/Acc.ML Thu Apr 04 11:43:25 1996 +0200
+++ b/src/HOL/ex/Acc.ML Thu Apr 04 11:45:01 1996 +0200
@@ -37,7 +37,7 @@
qed "acc_induct";
-val [major] = goal Acc.thy "r <= Sigma (acc r) (%u. acc(r)) ==> wf(r)";
+val [major] = goal Acc.thy "r <= (acc r) Times (acc r) ==> wf(r)";
by (rtac (major RS wfI) 1);
by (etac acc.induct 1);
by (rewtac pred_def);
@@ -51,13 +51,13 @@
by (fast_tac set_cs 1);
qed "acc_wfD_lemma";
-val [major] = goal Acc.thy "wf(r) ==> r <= Sigma (acc r) (%u. acc(r))";
+val [major] = goal Acc.thy "wf(r) ==> r <= (acc r) Times (acc r)";
by (rtac subsetI 1);
by (res_inst_tac [("p", "x")] PairE 1);
by (fast_tac (set_cs addSIs [SigmaI,
major RS acc_wfD_lemma RS spec RS mp]) 1);
qed "acc_wfD";
-goal Acc.thy "wf(r) = (r <= Sigma (acc r) (%u. acc(r)))";
+goal Acc.thy "wf(r) = (r <= (acc r) Times (acc r))";
by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]);
qed "wf_acc_iff";
--- a/src/HOL/ex/LList.ML Thu Apr 04 11:43:25 1996 +0200
+++ b/src/HOL/ex/LList.ML Thu Apr 04 11:45:01 1996 +0200
@@ -133,7 +133,7 @@
(*Lemma for the proof of llist_corec*)
goal LList.thy
"LList_corec a (%z.sum_case Inl (split(%v w.Inr((Leaf(v),w)))) (f z)) : \
-\ llist(range(Leaf))";
+\ llist(range Leaf)";
by (res_inst_tac [("X", "range(%x.LList_corec x ?g)")] llist_coinduct 1);
by (rtac rangeI 1);
by (safe_tac set_cs);
@@ -350,7 +350,7 @@
by (rtac Rep_llist_inverse 1);
qed "inj_Rep_llist";
-goal LList.thy "inj_onto Abs_llist (llist(range(Leaf)))";
+goal LList.thy "inj_onto Abs_llist (llist(range Leaf))";
by (rtac inj_onto_inverseI 1);
by (etac Abs_llist_inverse 1);
qed "inj_onto_Abs_llist";
@@ -605,8 +605,8 @@
(*** Deriving llist_equalityI -- llist equality is a bisimulation ***)
goalw LList.thy [LListD_Fun_def]
- "!!r A. r <= Sigma (llist A) (%x.llist(A)) ==> \
-\ LListD_Fun (diag A) r <= Sigma (llist A) (%x.llist(A))";
+ "!!r A. r <= (llist A) Times (llist A) ==> \
+\ LListD_Fun (diag A) r <= (llist A) Times (llist A)";
by (stac llist_unfold 1);
by (simp_tac (!simpset addsimps [NIL_def, CONS_def]) 1);
by (fast_tac univ_cs 1);
@@ -614,12 +614,12 @@
goal LList.thy
"prod_fun Rep_llist Rep_llist `` r <= \
-\ Sigma (llist(range(Leaf))) (%x.llist(range(Leaf)))";
+\ (llist(range Leaf)) Times (llist(range Leaf))";
by (fast_tac (prod_cs addIs [Rep_llist]) 1);
qed "subset_Sigma_llist";
val [prem] = goal LList.thy
- "r <= Sigma (llist(range Leaf)) (%x.llist(range Leaf)) ==> \
+ "r <= (llist(range Leaf)) Times (llist(range Leaf)) ==> \
\ prod_fun (Rep_llist o Abs_llist) (Rep_llist o Abs_llist) `` r <= r";
by (safe_tac prod_cs);
by (rtac (prem RS subsetD RS SigmaE2) 1);
@@ -629,7 +629,7 @@
goal LList.thy
"prod_fun Rep_llist Rep_llist `` range(%x. (x, x)) = \
-\ diag(llist(range(Leaf)))";
+\ diag(llist(range Leaf))";
by (rtac equalityI 1);
by (fast_tac (univ_cs addIs [Rep_llist]) 1);
by (fast_tac (univ_cs addSEs [Abs_llist_inverse RS subst]) 1);
--- a/src/HOL/ex/Mutil.ML Thu Apr 04 11:43:25 1996 +0200
+++ b/src/HOL/ex/Mutil.ML Thu Apr 04 11:45:01 1996 +0200
@@ -112,26 +112,24 @@
by (fast_tac set_cs 1);
qed "below_less_iff";
-goal thy
- "Sigma (below (Suc A)) B = (Sigma {A} (%x. B(A))) Un Sigma (below A) B";
+goal thy "(below (Suc n)) Times B = ({n} Times B) Un ((below n) Times B)";
by (simp_tac (!simpset addsimps [below_Suc]) 1);
by (fast_tac (prod_cs addIs [equalityI]) 1);
qed "Sigma_Suc1";
-goal thy
- "Sigma A (%x. below (Suc B)) = Sigma A (%x.{B}) Un Sigma A (%x.below B)";
+goal thy "A Times (below (Suc n)) = (A Times {n}) Un (A Times (below n))";
by (simp_tac (!simpset addsimps [below_Suc]) 1);
by (fast_tac (prod_cs addIs [equalityI]) 1);
qed "Sigma_Suc2";
-goal thy "Sigma {i} (%x. below (n + n)) : tiling domino";
+goal thy "{i} Times (below (n + n)) : tiling domino";
by (nat_ind_tac "n" 1);
by (simp_tac (!simpset addsimps tiling.intrs) 1);
by (asm_simp_tac (!simpset addsimps [Un_assoc RS sym, Sigma_Suc2]) 1);
by (resolve_tac tiling.intrs 1);
by (assume_tac 2);
by (subgoal_tac (*seems the easiest way of turning one to the other*)
- "Sigma {i} (%x. {Suc(n1+n1)}) Un Sigma {i} (%x. {n1+n1}) = \
+ "({i} Times {Suc(n1+n1)}) Un ({i} Times {n1+n1}) = \
\ {(i, n1+n1), (i, Suc(n1+n1))}" 1);
by (fast_tac (prod_cs addIs [equalityI]) 2);
by (asm_simp_tac (!simpset addsimps [domino.horiz]) 1);
@@ -139,7 +137,7 @@
addDs [below_less_iff RS iffD1]) 1);
qed "dominoes_tile_row";
-goal thy "Sigma (below m) (%x. below (n + n)) : tiling domino";
+goal thy "(below m) Times (below (n + n)) : tiling domino";
by (nat_ind_tac "m" 1);
by (simp_tac (!simpset addsimps (below_0::tiling.intrs)) 1);
by (asm_simp_tac (!simpset addsimps [Sigma_Suc1]) 1);
@@ -148,8 +146,8 @@
qed "dominoes_tile_matrix";
-goal thy "!!m n. [| t = Sigma (below (Suc m + Suc m))\
-\ (%x. below (Suc n + Suc n)); \
+goal thy "!!m n. [| t = (below (Suc m + Suc m)) Times \
+\ (below (Suc n + Suc n)); \
\ t' = t - {(0,0)} - {(Suc(m+m), Suc(n+n))} \
\ |] ==> t' ~: tiling domino";
by (rtac notI 1);