Deleted some useless things and made proofs of
authorlcp
Thu Apr 13 15:06:25 1995 +0200 (1995-04-13)
changeset 10450cdf86973c49
parent 1044 5bf29088250e
child 1046 9d2261a3e682
Deleted some useless things and made proofs of
refl_comp_subset and comp_equivI more like the versions in ZF/EquivClass.ML
src/HOL/Integ/Equiv.ML
     1.1 --- a/src/HOL/Integ/Equiv.ML	Thu Apr 13 15:03:07 1995 +0200
     1.2 +++ b/src/HOL/Integ/Equiv.ML	Thu Apr 13 15:06:25 1995 +0200
     1.3 @@ -19,39 +19,9 @@
     1.4  by (fast_tac (comp_cs addSEs [converseD]) 1);
     1.5  qed "sym_trans_comp_subset";
     1.6  
     1.7 -val [major,minor]=goal Equiv.thy "[|(x,y):r; z=(x,y)|] ==>  z:r";
     1.8 -by (simp_tac (prod_ss addsimps [minor]) 1);
     1.9 -by (rtac major 1);
    1.10 -qed "BreakPair";
    1.11 -
    1.12 -val [major]=goal Equiv.thy "[|? x y. (x,y):r & z=(x,y)|] ==>  z:r";
    1.13 -by (resolve_tac [major RS exE] 1);
    1.14 -by (etac exE 1);
    1.15 -by (etac conjE 1);
    1.16 -by (asm_simp_tac (prod_ss addsimps [minor]) 1);
    1.17 -qed "BreakPair1";
    1.18 -
    1.19 -val [major,minor]=goal Equiv.thy "[|z:r; z=(x,y)|] ==> (x,y):r";
    1.20 -by (simp_tac (prod_ss addsimps [minor RS sym]) 1);
    1.21 -by (rtac major 1);
    1.22 -qed "BuildPair";
    1.23 -
    1.24 -val [major]=goal Equiv.thy "[|? z:r. (x,y)=z|] ==> (x,y):r";
    1.25 -by (resolve_tac [major RS bexE] 1);
    1.26 -by (asm_simp_tac (prod_ss addsimps []) 1);
    1.27 -qed "BuildPair1";
    1.28 -
    1.29 -val rel_pair_cs = rel_cs addIs [BuildPair1] 
    1.30 -                         addEs [BreakPair1];
    1.31 -
    1.32 -goalw Equiv.thy [refl_def,converse_def]
    1.33 +goalw Equiv.thy [refl_def]
    1.34      "!!A r. refl A r ==> r <= converse(r) O r";
    1.35 -by (step_tac comp_cs 1);
    1.36 -by (dtac subsetD 1);
    1.37 -by (assume_tac 1);
    1.38 -by (etac SigmaE 1);
    1.39 -by (rtac BreakPair1 1);
    1.40 -by (fast_tac comp_cs 1);
    1.41 +by (fast_tac (rel_cs addIs [compI]) 1);
    1.42  qed "refl_comp_subset";
    1.43  
    1.44  goalw Equiv.thy [equiv_def]
    1.45 @@ -68,16 +38,7 @@
    1.46  by (subgoal_tac "ALL x y. (x,y) : r --> (y,x) : r" 1);
    1.47  by (safe_tac set_cs);
    1.48  by (fast_tac (set_cs addSIs [converseI] addIs [compI]) 3);
    1.49 -by (fast_tac (set_cs addSIs [converseI] addIs [compI] addSEs [DomainE]) 2);
    1.50 -by (fast_tac (rel_pair_cs addSEs [SigmaE] addSIs [SigmaI]) 1);
    1.51 -by (dtac subsetD 1);
    1.52 -by (dtac subsetD 1);
    1.53 -by (fast_tac rel_cs 1);
    1.54 -by (fast_tac rel_cs 1);
    1.55 -by flexflex_tac;
    1.56 -by (dtac subsetD 1);
    1.57 -by (fast_tac converse_cs 2);
    1.58 -by (fast_tac converse_cs 1);
    1.59 +by (ALLGOALS (fast_tac (rel_cs addIs [compI] addSEs [compE])));
    1.60  qed "comp_equivI";
    1.61  
    1.62  (** Equivalence classes **)