# HG changeset patch # User lcp # Date 797778385 -7200 # Node ID 0cdf86973c49e994e686437ae7bddea9555a326e # Parent 5bf29088250e68faa52263f9743c193731026be5 Deleted some useless things and made proofs of refl_comp_subset and comp_equivI more like the versions in ZF/EquivClass.ML diff -r 5bf29088250e -r 0cdf86973c49 src/HOL/Integ/Equiv.ML --- a/src/HOL/Integ/Equiv.ML Thu Apr 13 15:03:07 1995 +0200 +++ b/src/HOL/Integ/Equiv.ML Thu Apr 13 15:06:25 1995 +0200 @@ -19,39 +19,9 @@ by (fast_tac (comp_cs addSEs [converseD]) 1); qed "sym_trans_comp_subset"; -val [major,minor]=goal Equiv.thy "[|(x,y):r; z=(x,y)|] ==> z:r"; -by (simp_tac (prod_ss addsimps [minor]) 1); -by (rtac major 1); -qed "BreakPair"; - -val [major]=goal Equiv.thy "[|? x y. (x,y):r & z=(x,y)|] ==> z:r"; -by (resolve_tac [major RS exE] 1); -by (etac exE 1); -by (etac conjE 1); -by (asm_simp_tac (prod_ss addsimps [minor]) 1); -qed "BreakPair1"; - -val [major,minor]=goal Equiv.thy "[|z:r; z=(x,y)|] ==> (x,y):r"; -by (simp_tac (prod_ss addsimps [minor RS sym]) 1); -by (rtac major 1); -qed "BuildPair"; - -val [major]=goal Equiv.thy "[|? z:r. (x,y)=z|] ==> (x,y):r"; -by (resolve_tac [major RS bexE] 1); -by (asm_simp_tac (prod_ss addsimps []) 1); -qed "BuildPair1"; - -val rel_pair_cs = rel_cs addIs [BuildPair1] - addEs [BreakPair1]; - -goalw Equiv.thy [refl_def,converse_def] +goalw Equiv.thy [refl_def] "!!A r. refl A r ==> r <= converse(r) O r"; -by (step_tac comp_cs 1); -by (dtac subsetD 1); -by (assume_tac 1); -by (etac SigmaE 1); -by (rtac BreakPair1 1); -by (fast_tac comp_cs 1); +by (fast_tac (rel_cs addIs [compI]) 1); qed "refl_comp_subset"; goalw Equiv.thy [equiv_def] @@ -68,16 +38,7 @@ by (subgoal_tac "ALL x y. (x,y) : r --> (y,x) : r" 1); by (safe_tac set_cs); by (fast_tac (set_cs addSIs [converseI] addIs [compI]) 3); -by (fast_tac (set_cs addSIs [converseI] addIs [compI] addSEs [DomainE]) 2); -by (fast_tac (rel_pair_cs addSEs [SigmaE] addSIs [SigmaI]) 1); -by (dtac subsetD 1); -by (dtac subsetD 1); -by (fast_tac rel_cs 1); -by (fast_tac rel_cs 1); -by flexflex_tac; -by (dtac subsetD 1); -by (fast_tac converse_cs 2); -by (fast_tac converse_cs 1); +by (ALLGOALS (fast_tac (rel_cs addIs [compI] addSEs [compE]))); qed "comp_equivI"; (** Equivalence classes **)