Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
authorpaulson
Mon Jun 30 18:15:51 2003 +0200 (2003-06-30)
changeset 14084ccb48f3239f7
parent 14083 aed5d25c4a0c
child 14085 8dc3e532959a
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
Conversion of UNITY/State to Isar format.;
src/ZF/IsaMakefile
src/ZF/UNITY/AllocBase.thy
src/ZF/UNITY/ClientImpl.thy
src/ZF/UNITY/State.ML
src/ZF/UNITY/State.thy
src/ZF/UNITY/UNITYMisc.ML
src/ZF/UNITY/UNITYMisc.thy
src/ZF/UNITY/WFair.ML
src/ZF/equalities.thy
     1.1 --- a/src/ZF/IsaMakefile	Mon Jun 30 12:23:00 2003 +0200
     1.2 +++ b/src/ZF/IsaMakefile	Mon Jun 30 18:15:51 2003 +0200
     1.3 @@ -117,9 +117,9 @@
     1.4  $(LOG)/ZF-UNITY.gz: $(OUT)/ZF UNITY/ROOT.ML \
     1.5    UNITY/Comp.ML UNITY/Comp.thy UNITY/Constrains.ML UNITY/Constrains.thy \
     1.6    UNITY/FP.ML UNITY/FP.thy UNITY/Guar.ML UNITY/Guar.thy \
     1.7 -  UNITY/Mutex.ML UNITY/Mutex.thy UNITY/State.ML UNITY/State.thy \
     1.8 +  UNITY/Mutex.ML UNITY/Mutex.thy UNITY/State.thy \
     1.9    UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.thy \
    1.10 -  UNITY/UNITYMisc.ML UNITY/UNITYMisc.thy UNITY/Union.ML UNITY/Union.thy \
    1.11 +  UNITY/Union.ML UNITY/Union.thy \
    1.12    UNITY/AllocBase.thy UNITY/AllocImpl.thy\
    1.13    UNITY/ClientImpl.thy UNITY/Distributor.thy\
    1.14    UNITY/Follows.ML UNITY/Follows.thy\
     2.1 --- a/src/ZF/UNITY/AllocBase.thy	Mon Jun 30 12:23:00 2003 +0200
     2.2 +++ b/src/ZF/UNITY/AllocBase.thy	Mon Jun 30 18:15:51 2003 +0200
     2.3 @@ -187,8 +187,11 @@
     2.4  
     2.5  lemma mem_Int_imp_lt_length:
     2.6       "[|xs \<in> list(A); k \<in> C \<inter> length(xs)|] ==> k < length(xs)"
     2.7 -apply (simp add: ltI)
     2.8 -done
     2.9 +by (simp add: ltI)
    2.10 +
    2.11 +lemma Int_succ_right:
    2.12 +     "A Int succ(k) = (if k : A then cons(k, A Int k) else A Int k)"
    2.13 +by auto
    2.14  
    2.15  
    2.16  lemma bag_of_sublist_lemma:
    2.17 @@ -349,18 +352,6 @@
    2.18  apply (rule var_infinite_lemma)
    2.19  done
    2.20  
    2.21 -(*Surely a simpler proof uses lepoll_Finite and the following lemma:*)
    2.22 -
    2.23 -    (*????Cardinal*)
    2.24 -    lemma nat_not_Finite: "~Finite(nat)"
    2.25 -    apply (unfold Finite_def, clarify) 
    2.26 -    apply (drule eqpoll_imp_lepoll [THEN lepoll_cardinal_le], simp) 
    2.27 -    apply (insert Card_nat) 
    2.28 -    apply (simp add: Card_def)
    2.29 -    apply (drule le_imp_subset)
    2.30 -    apply (blast elim: mem_irrefl)
    2.31 -    done
    2.32 -
    2.33  lemma var_not_Finite: "~Finite(var)"
    2.34  apply (insert nat_not_Finite) 
    2.35  apply (blast intro: lepoll_Finite [OF 	nat_lepoll_var]) 
     3.1 --- a/src/ZF/UNITY/ClientImpl.thy	Mon Jun 30 12:23:00 2003 +0200
     3.2 +++ b/src/ZF/UNITY/ClientImpl.thy	Mon Jun 30 18:15:51 2003 +0200
     3.3 @@ -9,7 +9,7 @@
     3.4  
     3.5  theory ClientImpl = AllocBase + Guar:
     3.6  
     3.7 -(*????MOVE UP*)
     3.8 +(*move to Constrains.thy when the latter is converted to Isar format*)
     3.9  method_setup constrains = {*
    3.10      Method.ctxt_args (fn ctxt =>
    3.11          Method.METHOD (fn facts =>
    3.12 @@ -17,13 +17,6 @@
    3.13                                 Simplifier.get_local_simpset ctxt) 1)) *}
    3.14      "for proving safety properties"
    3.15  
    3.16 -(*For using "disjunction" (union over an index set) to eliminate a variable.
    3.17 -  ????move way up*)
    3.18 -lemma UN_conj_eq: "\<forall>s\<in>state. f(s) \<in> A
    3.19 -      ==> (\<Union>k\<in>A. {s\<in>state. P(s) & f(s) = k}) = {s\<in>state. P(s)}"
    3.20 -by blast
    3.21 -
    3.22 -
    3.23  consts
    3.24    ask :: i (* input history:  tokens requested *)
    3.25    giv :: i (* output history: tokens granted *)
     4.1 --- a/src/ZF/UNITY/State.ML	Mon Jun 30 12:23:00 2003 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,114 +0,0 @@
     4.4 -(*  Title:      HOL/UNITY/State.ML
     4.5 -    ID:         $Id$
     4.6 -    Author:     Sidi O Ehmety, Computer Laboratory
     4.7 -    Copyright   2001  University of Cambridge
     4.8 -
     4.9 -Formalizes UNITY-program states.
    4.10 -*)
    4.11 -Goalw [state_def, st0_def] "st0:state";
    4.12 -by Auto_tac;
    4.13 -qed "st0_in_state";
    4.14 -Addsimps [st0_in_state];
    4.15 -AddTCs [st0_in_state];
    4.16 -
    4.17 -Goalw [st_set_def] "st_set({x:state. P(x)})";
    4.18 -by Auto_tac;
    4.19 -qed "st_set_Collect";
    4.20 -AddIffs [st_set_Collect];
    4.21 -
    4.22 -Goalw [st_set_def] "st_set(0)";
    4.23 -by (Simp_tac 1);
    4.24 -qed "st_set_0";
    4.25 -AddIffs [st_set_0];
    4.26 -
    4.27 -Goalw [st_set_def] "st_set(state)";
    4.28 -by (Simp_tac 1);
    4.29 -qed "st_set_state";
    4.30 -AddIffs [st_set_state];
    4.31 -
    4.32 -(* Union *)
    4.33 -
    4.34 -Goalw [st_set_def] 
    4.35 -"st_set(A Un B) <-> st_set(A) & st_set(B)";
    4.36 -by Auto_tac;
    4.37 -qed "st_set_Un_iff";
    4.38 -AddIffs [st_set_Un_iff];
    4.39 -
    4.40 -Goalw [st_set_def] 
    4.41 -"st_set(Union(S)) <-> (ALL A:S. st_set(A))";
    4.42 -by Auto_tac;
    4.43 -qed "st_set_Union_iff";
    4.44 -AddIffs [st_set_Union_iff];
    4.45 -
    4.46 -(* Intersection *)
    4.47 -
    4.48 -Goalw [st_set_def] 
    4.49 -"st_set(A) | st_set(B) ==> st_set(A Int B)";
    4.50 -by Auto_tac;
    4.51 -qed "st_set_Int";
    4.52 -AddSIs [st_set_Int];
    4.53 -
    4.54 -Goalw [st_set_def, Inter_def]
    4.55 -   "(S=0) | (EX A:S. st_set(A)) ==> st_set(Inter(S))";
    4.56 -by Auto_tac;
    4.57 -qed "st_set_Inter";
    4.58 -AddSIs [st_set_Inter];
    4.59 -
    4.60 -(* Diff *)
    4.61 -Goalw [st_set_def]
    4.62 -"st_set(A) ==> st_set(A - B)";
    4.63 -by Auto_tac;
    4.64 -qed "st_set_DiffI";
    4.65 -AddSIs [st_set_DiffI];
    4.66 -
    4.67 -Goal "{s:state. P(s)} Int state = {s:state. P(s)}";
    4.68 -by Auto_tac;
    4.69 -qed "Collect_Int_state";
    4.70 -
    4.71 -Goal "state Int {s:state. P(s)} = {s:state. P(s)}";
    4.72 -by Auto_tac;
    4.73 -qed "state_Int_Collect";
    4.74 -AddIffs [Collect_Int_state, state_Int_Collect];
    4.75 -
    4.76 -(* Introduction and destruction rules for st_set *)
    4.77 -
    4.78 -Goalw [st_set_def]
    4.79 - "A <= state ==> st_set(A)";
    4.80 -by (assume_tac 1);
    4.81 -qed "st_setI";
    4.82 -
    4.83 -Goalw [st_set_def]
    4.84 - "st_set(A) ==> A<=state";
    4.85 -by (assume_tac 1);
    4.86 -qed "st_setD";
    4.87 -
    4.88 -Goalw [st_set_def]
    4.89 -"[| st_set(A); B<=A |] ==> st_set(B)";
    4.90 -by Auto_tac;
    4.91 -qed "st_set_subset";
    4.92 -
    4.93 -
    4.94 -Goalw [state_def]
    4.95 -"[| s:state; x:var; y:type_of(x) |] ==> s(x:=y):state";
    4.96 -by (blast_tac (claset() addIs [update_type]) 1);
    4.97 -qed "state_update_type";
    4.98 -
    4.99 -Goalw [st_compl_def] "st_set(st_compl(A))";
   4.100 -by Auto_tac;
   4.101 -qed "st_set_compl";
   4.102 -Addsimps [st_set_compl];
   4.103 -
   4.104 -Goalw [st_compl_def] "x:st_compl(A) <-> x:state & x ~:A";
   4.105 -by Auto_tac;
   4.106 -qed "st_compl_iff";
   4.107 -Addsimps [st_compl_iff];
   4.108 -
   4.109 -Goalw [st_compl_def] "st_compl({s:state. P(s)}) = {s:state. ~P(s)}";
   4.110 -by Auto_tac;
   4.111 -qed "st_compl_Collect";
   4.112 -Addsimps [st_compl_Collect];
   4.113 -
   4.114 -
   4.115 -
   4.116 -
   4.117 -
     5.1 --- a/src/ZF/UNITY/State.thy	Mon Jun 30 12:23:00 2003 +0200
     5.2 +++ b/src/ZF/UNITY/State.thy	Mon Jun 30 18:15:51 2003 +0200
     5.3 @@ -9,27 +9,132 @@
     5.4   - variables can be quantified over.
     5.5  *)
     5.6  
     5.7 -State = UNITYMisc +
     5.8 +header{*UNITY Program States*}
     5.9 +
    5.10 +theory State = Main:
    5.11  
    5.12 -consts var::i
    5.13 -datatype var = Var("i:list(nat)")
    5.14 -         type_intrs "[list_nat_into_univ]"
    5.15 +consts var :: i
    5.16 +datatype var = Var("i \<in> list(nat)")
    5.17 +  type_intros  nat_subset_univ [THEN list_subset_univ, THEN subsetD]
    5.18 +
    5.19  consts
    5.20 -  type_of :: i=>i
    5.21 -  default_val :: i=>i
    5.22 +  type_of :: "i=>i"
    5.23 +  default_val :: "i=>i"
    5.24  
    5.25  constdefs
    5.26    state   :: i
    5.27 -  "state == PROD x:var. cons(default_val(x), type_of(x))"
    5.28 +   "state == \<Pi>x \<in> var. cons(default_val(x), type_of(x))"
    5.29 +
    5.30    st0     :: i
    5.31 -  "st0 == lam x:var. default_val(x)"
    5.32 +   "st0 == \<lambda>x \<in> var. default_val(x)"
    5.33    
    5.34 -  st_set  :: i =>o
    5.35 +  st_set  :: "i=>o"
    5.36  (* To prevent typing conditions like `A<=state' from
    5.37     being used in combination with the rules `constrains_weaken', etc. *)
    5.38    "st_set(A) == A<=state"
    5.39  
    5.40 -  st_compl :: i=>i
    5.41 +  st_compl :: "i=>i"
    5.42    "st_compl(A) == state-A"
    5.43 -  
    5.44 -end
    5.45 \ No newline at end of file
    5.46 +
    5.47 +
    5.48 +lemma st0_in_state [simp,TC]: "st0 \<in> state"
    5.49 +by (simp add: state_def st0_def)
    5.50 +
    5.51 +lemma st_set_Collect [iff]: "st_set({x \<in> state. P(x)})"
    5.52 +by (simp add: st_set_def, auto)
    5.53 +
    5.54 +lemma st_set_0 [iff]: "st_set(0)"
    5.55 +by (simp add: st_set_def)
    5.56 +
    5.57 +lemma st_set_state [iff]: "st_set(state)"
    5.58 +by (simp add: st_set_def)
    5.59 +
    5.60 +(* Union *)
    5.61 +
    5.62 +lemma st_set_Un_iff [iff]: "st_set(A Un B) <-> st_set(A) & st_set(B)"
    5.63 +by (simp add: st_set_def, auto)
    5.64 +
    5.65 +lemma st_set_Union_iff [iff]: "st_set(Union(S)) <-> (\<forall>A \<in> S. st_set(A))"
    5.66 +by (simp add: st_set_def, auto)
    5.67 +
    5.68 +(* Intersection *)
    5.69 +
    5.70 +lemma st_set_Int [intro!]: "st_set(A) | st_set(B) ==> st_set(A Int B)"
    5.71 +by (simp add: st_set_def, auto)
    5.72 +
    5.73 +lemma st_set_Inter [intro!]: 
    5.74 +   "(S=0) | (\<exists>A \<in> S. st_set(A)) ==> st_set(Inter(S))"
    5.75 +apply (simp add: st_set_def Inter_def, auto)
    5.76 +done
    5.77 +
    5.78 +(* Diff *)
    5.79 +lemma st_set_DiffI [intro!]: "st_set(A) ==> st_set(A - B)"
    5.80 +by (simp add: st_set_def, auto)
    5.81 +
    5.82 +lemma Collect_Int_state [simp]: "Collect(state,P) Int state = Collect(state,P)"
    5.83 +by auto
    5.84 +
    5.85 +lemma state_Int_Collect [simp]: "state Int Collect(state,P) = Collect(state,P)"
    5.86 +by auto
    5.87 +
    5.88 +
    5.89 +(* Introduction and destruction rules for st_set *)
    5.90 +
    5.91 +lemma st_setI: "A <= state ==> st_set(A)"
    5.92 +by (simp add: st_set_def)
    5.93 +
    5.94 +lemma st_setD: "st_set(A) ==> A<=state"
    5.95 +by (simp add: st_set_def)
    5.96 +
    5.97 +lemma st_set_subset: "[| st_set(A); B<=A |] ==> st_set(B)"
    5.98 +by (simp add: st_set_def, auto)
    5.99 +
   5.100 +
   5.101 +lemma state_update_type: 
   5.102 +     "[| s \<in> state; x \<in> var; y \<in> type_of(x) |] ==> s(x:=y):state"
   5.103 +apply (simp add: state_def)
   5.104 +apply (blast intro: update_type)
   5.105 +done
   5.106 +
   5.107 +lemma st_set_compl [simp]: "st_set(st_compl(A))"
   5.108 +by (simp add: st_compl_def, auto)
   5.109 +
   5.110 +lemma st_compl_iff [simp]: "x \<in> st_compl(A) <-> x \<in> state & x \<notin> A"
   5.111 +by (simp add: st_compl_def)
   5.112 +
   5.113 +lemma st_compl_Collect [simp]:
   5.114 +     "st_compl({s \<in> state. P(s)}) = {s \<in> state. ~P(s)}"
   5.115 +by (simp add: st_compl_def, auto)
   5.116 +
   5.117 +(*For using "disjunction" (union over an index set) to eliminate a variable.*)
   5.118 +lemma UN_conj_eq:
   5.119 +     "\<forall>d\<in>D. f(d) \<in> A ==> (\<Union>k\<in>A. {d\<in>D. P(d) & f(d) = k}) = {d\<in>D. P(d)}"
   5.120 +by blast
   5.121 +
   5.122 +
   5.123 +ML
   5.124 +{*
   5.125 +val st_set_def = thm "st_set_def";
   5.126 +val state_def = thm "state_def";
   5.127 +
   5.128 +val st0_in_state = thm "st0_in_state";
   5.129 +val st_set_Collect = thm "st_set_Collect";
   5.130 +val st_set_0 = thm "st_set_0";
   5.131 +val st_set_state = thm "st_set_state";
   5.132 +val st_set_Un_iff = thm "st_set_Un_iff";
   5.133 +val st_set_Union_iff = thm "st_set_Union_iff";
   5.134 +val st_set_Int = thm "st_set_Int";
   5.135 +val st_set_Inter = thm "st_set_Inter";
   5.136 +val st_set_DiffI = thm "st_set_DiffI";
   5.137 +val Collect_Int_state = thm "Collect_Int_state";
   5.138 +val state_Int_Collect = thm "state_Int_Collect";
   5.139 +val st_setI = thm "st_setI";
   5.140 +val st_setD = thm "st_setD";
   5.141 +val st_set_subset = thm "st_set_subset";
   5.142 +val state_update_type = thm "state_update_type";
   5.143 +val st_set_compl = thm "st_set_compl";
   5.144 +val st_compl_iff = thm "st_compl_iff";
   5.145 +val st_compl_Collect = thm "st_compl_Collect";
   5.146 +*}
   5.147 +
   5.148 +end
     6.1 --- a/src/ZF/UNITY/UNITYMisc.ML	Mon Jun 30 12:23:00 2003 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,57 +0,0 @@
     6.4 -(*  Title:      HOL/UNITY/UNITYMisc.ML
     6.5 -    ID:         $Id$
     6.6 -    Author:     Sidi O Ehmety, Computer Laboratory
     6.7 -    Copyright   2001  University of Cambridge
     6.8 -
     6.9 -Some miscellaneous and add-hoc set theory concepts.
    6.10 -
    6.11 -*)
    6.12 -
    6.13 -(** Ad-hoc set-theory rules **)
    6.14 -
    6.15 -Goal "Union(B) Int A = (UN b:B. b Int A)";
    6.16 -by Auto_tac;
    6.17 -qed "Int_Union_Union";
    6.18 -
    6.19 -Goal "A Int Union(B) = (UN b:B. A Int b)";
    6.20 -by Auto_tac;
    6.21 -qed "Int_Union_Union2";
    6.22 -
    6.23 -
    6.24 -(** Needed in State theory for the current definition of variables 
    6.25 -where they are indexed by lists  **)
    6.26 -
    6.27 -Goal "i:list(nat) ==> i:univ(0)";
    6.28 -by (dres_inst_tac [("B", "0")] list_into_univ 1);
    6.29 -by (blast_tac (claset() addIs [nat_into_univ]) 1);
    6.30 -by (assume_tac 1);
    6.31 -qed "list_nat_into_univ";
    6.32 -
    6.33 -
    6.34 -(** Simplication rules for Collect **)
    6.35 -
    6.36 -(*Currently unused*)
    6.37 -Goal "{x:A. P(x)} Int B = {x : A Int B. P(x)}";
    6.38 -by Auto_tac;
    6.39 -qed "Collect_Int_left";
    6.40 -
    6.41 -(*Currently unused*)
    6.42 -Goal "A Int {x:B. P(x)} = {x : A Int B. P(x)}";
    6.43 -by Auto_tac;
    6.44 -qed "Collect_Int_right";
    6.45 -
    6.46 -Goal "{x:A. P(x) | Q(x)} = Collect(A, P) Un Collect(A, Q)";
    6.47 -by Auto_tac;
    6.48 -qed "Collect_disj_eq";
    6.49 -
    6.50 -Goal "{x:A. P(x) & Q(x)} = Collect(A, P) Int Collect(A, Q)";
    6.51 -by Auto_tac;
    6.52 -qed "Collect_conj_eq";
    6.53 -
    6.54 -Goal "Union(B) Int A = (UN C:B. C Int A)"; 
    6.55 -by (Blast_tac 1);
    6.56 -qed "Int_Union2";
    6.57 -
    6.58 -Goal "A Int succ(k) = (if k : A then cons(k, A Int k) else A Int k)";
    6.59 -by Auto_tac;
    6.60 -qed "Int_succ_right";
     7.1 --- a/src/ZF/UNITY/UNITYMisc.thy	Mon Jun 30 12:23:00 2003 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,11 +0,0 @@
     7.4 -(*  Title:      HOL/UNITY/UNITYMisc.thy
     7.5 -    ID:         $Id$
     7.6 -    Author:     Sidi O Ehmety, Computer Laboratory
     7.7 -    Copyright   2001  University of Cambridge
     7.8 -
     7.9 -Some miscellaneous and add-hoc set theory concepts.
    7.10 -*)
    7.11 -
    7.12 -
    7.13 -
    7.14 -UNITYMisc = Main
    7.15 \ No newline at end of file
     8.1 --- a/src/ZF/UNITY/WFair.ML	Mon Jun 30 12:23:00 2003 +0200
     8.2 +++ b/src/ZF/UNITY/WFair.ML	Mon Jun 30 18:15:51 2003 +0200
     8.3 @@ -8,6 +8,16 @@
     8.4  From Misra, "A Logic for Concurrent Programming", 1994
     8.5  *)
     8.6  
     8.7 +(** Ad-hoc set-theory rules **)
     8.8 +
     8.9 +Goal "Union(B) Int A = (UN b:B. b Int A)";
    8.10 +by Auto_tac;
    8.11 +qed "Int_Union_Union";
    8.12 +
    8.13 +Goal "A Int Union(B) = (UN b:B. A Int b)";
    8.14 +by Auto_tac;
    8.15 +qed "Int_Union_Union2";
    8.16 +
    8.17  (*** transient ***)
    8.18  
    8.19  Goalw [transient_def] "transient(A)<=program";
     9.1 --- a/src/ZF/equalities.thy	Mon Jun 30 12:23:00 2003 +0200
     9.2 +++ b/src/ZF/equalities.thy	Mon Jun 30 18:15:51 2003 +0200
     9.3 @@ -12,41 +12,9 @@
     9.4  text{*These cover union, intersection, converse, domain, range, etc.  Philippe
     9.5  de Groote proved many of the inclusions.*}
     9.6  
     9.7 -(*FIXME: move to ZF.thy or even to FOL.thy??*)
     9.8 -lemma [simp]: "((P-->Q) <-> (P-->R)) <-> (P --> (Q<->R))"
     9.9 -by blast
    9.10 -
    9.11 -(*FIXME: move to ZF.thy or even to FOL.thy??*)
    9.12 -lemma not_disj_iff_imp: "~P | Q <-> (P-->Q)"
    9.13 -by blast
    9.14 -
    9.15 -(** Monotonicity of implications -- some could go to FOL **)
    9.16 -
    9.17  lemma in_mono: "A<=B ==> x:A --> x:B"
    9.18  by blast
    9.19  
    9.20 -lemma conj_mono: "[| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)"
    9.21 -by fast (*or (IntPr.fast_tac 1)*)
    9.22 -
    9.23 -lemma disj_mono: "[| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)"
    9.24 -by fast (*or (IntPr.fast_tac 1)*)
    9.25 -
    9.26 -lemma imp_mono: "[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)"
    9.27 -by fast (*or (IntPr.fast_tac 1)*)
    9.28 -
    9.29 -lemma imp_refl: "P-->P"
    9.30 -by (rule impI, assumption)
    9.31 -
    9.32 -(*The quantifier monotonicity rules are also intuitionistically valid*)
    9.33 -lemma ex_mono:
    9.34 -    "[| !!x. P(x) --> Q(x) |] ==> (EX x. P(x)) --> (EX x. Q(x))"
    9.35 -by blast
    9.36 -
    9.37 -lemma all_mono:
    9.38 -    "[| !!x. P(x) --> Q(x) |] ==> (ALL x. P(x)) --> (ALL x. Q(x))"
    9.39 -by blast
    9.40 -
    9.41 -
    9.42  lemma the_eq_0 [simp]: "(THE x. False) = 0"
    9.43  by (blast intro: the_0)
    9.44  
    9.45 @@ -404,6 +372,9 @@
    9.46  lemma Union_empty_iff: "Union(A) = 0 <-> (\<forall>B\<in>A. B=0)"
    9.47  by blast
    9.48  
    9.49 +lemma Int_Union2: "Union(B) Int A = (UN C:B. C Int A)"
    9.50 +by blast
    9.51 +
    9.52  (** Big Intersection is the greatest lower bound of a nonempty set **)
    9.53  
    9.54  lemma Inter_subset_iff: "a: A  ==>  C <= Inter(A) <-> (\<forall>x\<in>A. C <= x)"
    9.55 @@ -978,6 +949,18 @@
    9.56       "Collect(\<Union>x\<in>A. B(x), P) = (\<Union>x\<in>A. Collect(B(x), P))"
    9.57  by blast
    9.58  
    9.59 +lemma Collect_Int_left: "{x:A. P(x)} Int B = {x : A Int B. P(x)}"
    9.60 +by blast
    9.61 +
    9.62 +lemma Collect_Int_right: "A Int {x:B. P(x)} = {x : A Int B. P(x)}"
    9.63 +by blast
    9.64 +
    9.65 +lemma Collect_disj_eq: "{x:A. P(x) | Q(x)} = Collect(A, P) Un Collect(A, Q)"
    9.66 +by blast
    9.67 +
    9.68 +lemma Collect_conj_eq: "{x:A. P(x) & Q(x)} = Collect(A, P) Int Collect(A, Q)"
    9.69 +by blast
    9.70 +
    9.71  lemmas subset_SIs = subset_refl cons_subsetI subset_consI 
    9.72                      Union_least UN_least Un_least 
    9.73                      Inter_greatest Int_greatest RepFun_subset
    9.74 @@ -1139,6 +1122,7 @@
    9.75  val Union_Int_subset = thm "Union_Int_subset";
    9.76  val Union_disjoint = thm "Union_disjoint";
    9.77  val Union_empty_iff = thm "Union_empty_iff";
    9.78 +val Int_Union2 = thm "Int_Union2";
    9.79  val Inter_0 = thm "Inter_0";
    9.80  val Inter_Un_subset = thm "Inter_Un_subset";
    9.81  val Inter_Un_distrib = thm "Inter_Un_distrib";
    9.82 @@ -1246,6 +1230,8 @@
    9.83  val Int_Collect_self_eq = thm "Int_Collect_self_eq";
    9.84  val Collect_Collect_eq = thm "Collect_Collect_eq";
    9.85  val Collect_Int_Collect_eq = thm "Collect_Int_Collect_eq";
    9.86 +val Collect_disj_eq = thm "Collect_disj_eq";
    9.87 +val Collect_conj_eq = thm "Collect_conj_eq";
    9.88  
    9.89  val Int_ac = thms "Int_ac";
    9.90  val Un_ac = thms "Un_ac";