# HG changeset patch # User paulson # Date 828611101 -7200 # Node ID 21db0cf9a1a41791acc744a69d4e97bbef457151 # Parent 46d2d4a249caab3eda61e06c169272e5866a7dc5 Using new "Times" infix diff -r 46d2d4a249ca -r 21db0cf9a1a4 src/HOL/Integ/Equiv.ML --- 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"; diff -r 46d2d4a249ca -r 21db0cf9a1a4 src/HOL/Integ/Equiv.thy --- 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}}" diff -r 46d2d4a249ca -r 21db0cf9a1a4 src/HOL/Prod.ML --- 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]; diff -r 46d2d4a249ca -r 21db0cf9a1a4 src/HOL/Relation.ML --- 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)) ]); diff -r 46d2d4a249ca -r 21db0cf9a1a4 src/HOL/Sexp.ML --- 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"; diff -r 46d2d4a249ca -r 21db0cf9a1a4 src/HOL/Trancl.ML --- 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]; + + diff -r 46d2d4a249ca -r 21db0cf9a1a4 src/HOL/Trancl.thy --- 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 + diff -r 46d2d4a249ca -r 21db0cf9a1a4 src/HOL/Univ.ML --- 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"; diff -r 46d2d4a249ca -r 21db0cf9a1a4 src/HOL/WF.ML --- 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); diff -r 46d2d4a249ca -r 21db0cf9a1a4 src/HOL/ex/Acc.ML --- 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"; diff -r 46d2d4a249ca -r 21db0cf9a1a4 src/HOL/ex/LList.ML --- 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); diff -r 46d2d4a249ca -r 21db0cf9a1a4 src/HOL/ex/Mutil.ML --- 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);