moved congruence rules UN_cong, INT_cong from UNTIY/Union to Set.ML
authorpaulson
Fri Aug 25 12:15:35 2000 +0200 (2000-08-25)
changeset 9687772ac061bd76
parent 9686 87b460d72e80
child 9688 d1415164b814
moved congruence rules UN_cong, INT_cong from UNTIY/Union to Set.ML
src/HOL/Set.ML
src/HOL/UNITY/Union.ML
     1.1 --- a/src/HOL/Set.ML	Thu Aug 24 12:39:42 2000 +0200
     1.2 +++ b/src/HOL/Set.ML	Fri Aug 25 12:15:35 2000 +0200
     1.3 @@ -19,13 +19,13 @@
     1.4  by (Asm_full_simp_tac 1);
     1.5  qed "CollectD";
     1.6  
     1.7 -val [prem] = Goal "[| !!x. (x:A) = (x:B) |] ==> A = B";
     1.8 +val [prem] = Goal "(!!x. (x:A) = (x:B)) ==> A = B";
     1.9  by (rtac (prem RS ext RS arg_cong RS box_equals) 1);
    1.10  by (rtac Collect_mem_eq 1);
    1.11  by (rtac Collect_mem_eq 1);
    1.12  qed "set_ext";
    1.13  
    1.14 -val [prem] = Goal "[| !!x. P(x)=Q(x) |] ==> {x. P(x)} = {x. Q(x)}";
    1.15 +val [prem] = Goal "(!!x. P(x)=Q(x)) ==> {x. P(x)} = {x. Q(x)}";
    1.16  by (rtac (prem RS ext RS arg_cong) 1);
    1.17  qed "Collect_cong";
    1.18  
    1.19 @@ -557,6 +557,7 @@
    1.20  \    (UN x:A. C(x)) = (UN x:B. D(x))";
    1.21  by (asm_simp_tac (simpset() addsimps prems) 1);
    1.22  qed "UN_cong";
    1.23 +Addcongs [UN_cong];
    1.24  
    1.25  
    1.26  section "Intersections of families -- INTER x:A. B(x) is Inter(B``A)";
    1.27 @@ -591,6 +592,7 @@
    1.28  \    (INT x:A. C(x)) = (INT x:B. D(x))";
    1.29  by (asm_simp_tac (simpset() addsimps prems) 1);
    1.30  qed "INT_cong";
    1.31 +Addcongs [INT_cong];
    1.32  
    1.33  
    1.34  section "Union";
     2.1 --- a/src/HOL/UNITY/Union.ML	Thu Aug 24 12:39:42 2000 +0200
     2.2 +++ b/src/HOL/UNITY/Union.ML	Fri Aug 25 12:15:35 2000 +0200
     2.3 @@ -8,8 +8,6 @@
     2.4  From Misra's Chapter 5: Asynchronous Compositions of Programs
     2.5  *)
     2.6  
     2.7 -Addcongs [UN_cong, INT_cong];
     2.8 -
     2.9  
    2.10  (** SKIP **)
    2.11