--- a/src/HOL/UNITY/Comp.ML Thu Jan 13 17:36:58 2000 +0100
+++ b/src/HOL/UNITY/Comp.ML Fri Jan 14 12:17:53 2000 +0100
@@ -173,74 +173,3 @@
by (Blast_tac 1);
qed "Increasing_preserves_Stable";
-
-(*** givenBy ***)
-
-Goalw [givenBy_def] "givenBy id = UNIV";
-by Auto_tac;
-qed "givenBy_id";
-Addsimps [givenBy_id];
-
-Goalw [givenBy_def] "(givenBy v) = {A. ALL x:A. ALL y. v x = v y --> y: A}";
-by Safe_tac;
-by (res_inst_tac [("x", "v `` ?u")] image_eqI 2);
-by Auto_tac;
-qed "givenBy_eq_all";
-
-Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
-by (simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
-by Safe_tac;
-by (res_inst_tac [("x", "%n. EX s. v s = n & s : ?A")] exI 1);
-by (Blast_tac 1);
-by Auto_tac;
-qed "givenBy_eq_Collect";
-
-val prems =
-Goal "(!!x y. [| x:A; v x = v y |] ==> y: A) ==> A: givenBy v";
-by (stac givenBy_eq_all 1);
-by (blast_tac (claset() addIs prems) 1);
-qed "givenByI";
-
-Goalw [givenBy_def] "[| A: givenBy v; x:A; v x = v y |] ==> y: A";
-by Auto_tac;
-qed "givenByD";
-
-Goal "{} : givenBy v";
-by (blast_tac (claset() addSIs [givenByI]) 1);
-qed "empty_mem_givenBy";
-
-AddIffs [empty_mem_givenBy];
-
-Goal "A: givenBy v ==> EX P. A = {s. P(v s)}";
-by (res_inst_tac [("x", "%n. EX s. v s = n & s : A")] exI 1);
-by (full_simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
-by (Blast_tac 1);
-qed "givenBy_imp_eq_Collect";
-
-Goalw [givenBy_def] "{s. P(v s)} : givenBy v";
-by (Best_tac 1);
-qed "Collect_mem_givenBy";
-
-Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
-by (blast_tac (claset() addIs [Collect_mem_givenBy,
- givenBy_imp_eq_Collect]) 1);
-qed "givenBy_eq_eq_Collect";
-
-(*preserving v preserves properties given by v*)
-Goal "[| F : preserves v; D : givenBy v |] ==> F : stable D";
-by (force_tac (claset(),
- simpset() addsimps [impOfSubs preserves_subset_stable,
- givenBy_eq_Collect]) 1);
-qed "preserves_givenBy_imp_stable";
-
-Goal "givenBy (w o v) <= givenBy v";
-by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
-by (Deepen_tac 0 1);
-qed "givenBy_o_subset";
-
-Goal "[| A : givenBy v; B : givenBy v |] ==> A-B : givenBy v";
-by (full_simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
-by Safe_tac;
-by (res_inst_tac [("x", "%z. ?R z & ~ ?Q z")] exI 1);
-by (deepen_tac (set_cs addSIs [equalityI]) 0 1);
-qed "givenBy_DiffI";