CollectE;
authorwenzelm
Wed Sep 29 16:45:04 1999 +0200 (1999-09-29)
changeset 76582d3445be4e91
parent 7657 dbbf7721126e
child 7659 c89ba43d9df0
CollectE;
AddXIs [subsetD, rev_subsetD, psubsetI];
src/HOL/Set.ML
     1.1 --- a/src/HOL/Set.ML	Wed Sep 29 16:44:18 1999 +0200
     1.2 +++ b/src/HOL/Set.ML	Wed Sep 29 16:45:04 1999 +0200
     1.3 @@ -19,6 +19,8 @@
     1.4  by (Asm_full_simp_tac 1);
     1.5  qed "CollectD";
     1.6  
     1.7 +bind_thm ("CollectE", make_elim CollectD);
     1.8 +
     1.9  val [prem] = Goal "[| !!x. (x:A) = (x:B) |] ==> A = B";
    1.10  by (rtac (prem RS ext RS arg_cong RS box_equals) 1);
    1.11  by (rtac Collect_mem_eq 1);
    1.12 @@ -139,11 +141,13 @@
    1.13  Goalw [subset_def] "[| A <= B;  c:A |] ==> c:B";
    1.14  by (Blast_tac 1);
    1.15  qed "subsetD";
    1.16 +AddXIs [subsetD];
    1.17  
    1.18  (*The same, with reversed premises for use with etac -- cf rev_mp*)
    1.19  Goal "[| c:A;  A <= B |] ==> c:B";
    1.20  by (REPEAT (ares_tac [subsetD] 1)) ;
    1.21  qed "rev_subsetD";
    1.22 +AddXIs [rev_subsetD];
    1.23  
    1.24  (*Converts A<=B to x:A ==> x:B*)
    1.25  fun impOfSubs th = th RSN (2, rev_subsetD);
    1.26 @@ -724,6 +728,7 @@
    1.27  Goalw [psubset_def] "!!A::'a set. [| A <= B; A ~= B |] ==> A<B";
    1.28  by (Blast_tac 1);
    1.29  qed "psubsetI";
    1.30 +AddXIs [psubsetI];
    1.31  
    1.32  Goalw [psubset_def] "A < insert x B ==> (x ~: A) & A<=B | x:A & A-{x}<B";
    1.33  by Auto_tac;