src/HOL/Set.ML
changeset 9088 453996655ac2
parent 9075 e8521ed7f35b
child 9108 9fff97d29837
     1.1 --- a/src/HOL/Set.ML	Tue Jun 20 11:41:25 2000 +0200
     1.2 +++ b/src/HOL/Set.ML	Tue Jun 20 11:42:24 2000 +0200
     1.3 @@ -473,13 +473,9 @@
     1.4  AddSIs [insertCI]; 
     1.5  AddSEs [insertE];
     1.6  
     1.7 -Goal "A <= insert x B ==> A <= B & x ~: A | (EX B'. A = insert x B' & B' <= B)";
     1.8 -by (case_tac "x:A" 1);
     1.9 -by  (Fast_tac 2);
    1.10 -by (rtac disjI2 1);
    1.11 -by (res_inst_tac [("x","A-{x}")] exI 1);
    1.12 -by (Fast_tac 1);
    1.13 -qed "subset_insertD";
    1.14 +Goal "(A <= insert x B) = (if x:A then A-{x} <= B else A<=B)";
    1.15 +by Auto_tac; 
    1.16 +qed "subset_insert_iff";
    1.17  
    1.18  section "Singletons, using insert";
    1.19  
    1.20 @@ -755,9 +751,11 @@
    1.21  qed "psubsetI";
    1.22  AddSIs [psubsetI];
    1.23  
    1.24 -Goalw [psubset_def] "A < insert x B ==> (x ~: A) & A<=B | x:A & A-{x}<B";
    1.25 -by Auto_tac;
    1.26 -qed "psubset_insertD";
    1.27 +Goalw [psubset_def]
    1.28 +  "(A < insert x B) = (if x:B then A<B else if x:A then A-{x} < B else A<=B)";
    1.29 +by (asm_simp_tac (simpset() addsimps [subset_insert_iff]) 1);
    1.30 +by (Blast_tac 1); 
    1.31 +qed "psubset_insert_iff";
    1.32  
    1.33  bind_thm ("psubset_eq", psubset_def RS meta_eq_to_obj_eq);
    1.34