src/HOL/UNITY/Comp.ML

 by (Blast_tac 2);
 by Auto_tac;
 by (etac order_trans 1);
 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";