1465

1 
(* Title: HOL/subset

923

2 
ID: $Id$

1465

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

923

4 
Copyright 1991 University of Cambridge


5 


6 
Derived rules involving subsets


7 
Union and Intersection as lattice operations


8 
*)


9 


10 
(*** insert ***)


11 

7007

12 
Goal "B <= insert a B";


13 
by (rtac subsetI 1);


14 
by (etac insertI2 1) ;


15 
qed "subset_insertI";

923

16 

5316

17 
Goal "x ~: A ==> (A <= insert x B) = (A <= B)";

2893

18 
by (Blast_tac 1);

1531

19 
qed "subset_insert";


20 

923

21 
(*** Big Union  least upper bound of a set ***)


22 

5316

23 
Goal "B:A ==> B <= Union(A)";


24 
by (REPEAT (ares_tac [subsetI,UnionI] 1));

923

25 
qed "Union_upper";


26 

5316

27 
val [prem] = Goal "[ !!X. X:A ==> X<=C ] ==> Union(A) <= C";

1465

28 
by (rtac subsetI 1);

923

29 
by (REPEAT (eresolve_tac [asm_rl, UnionE, prem RS subsetD] 1));


30 
qed "Union_least";


31 


32 
(** General union **)


33 

5316

34 
Goal "a:A ==> B(a) <= (UN x:A. B(x))";


35 
by (Blast_tac 1);

923

36 
qed "UN_upper";


37 

5316

38 
val [prem] = Goal "[ !!x. x:A ==> B(x)<=C ] ==> (UN x:A. B(x)) <= C";

1465

39 
by (rtac subsetI 1);

923

40 
by (REPEAT (eresolve_tac [asm_rl, UN_E, prem RS subsetD] 1));


41 
qed "UN_least";


42 


43 


44 
(*** Big Intersection  greatest lower bound of a set ***)


45 

5316

46 
Goal "B:A ==> Inter(A) <= B";

2893

47 
by (Blast_tac 1);

923

48 
qed "Inter_lower";


49 

5316

50 
val [prem] = Goal "[ !!X. X:A ==> C<=X ] ==> C <= Inter(A)";

1465

51 
by (rtac (InterI RS subsetI) 1);

923

52 
by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1));


53 
qed "Inter_greatest";


54 

5316

55 
Goal "a:A ==> (INT x:A. B(x)) <= B(a)";


56 
by (Blast_tac 1);

923

57 
qed "INT_lower";


58 

5316

59 
val [prem] = Goal "[ !!x. x:A ==> C<=B(x) ] ==> C <= (INT x:A. B(x))";

1465

60 
by (rtac (INT_I RS subsetI) 1);

923

61 
by (REPEAT (eresolve_tac [asm_rl, prem RS subsetD] 1));


62 
qed "INT_greatest";


63 


64 
(*** Finite Union  the least upper bound of 2 sets ***)


65 

5316

66 
Goal "A <= A Un B";

2893

67 
by (Blast_tac 1);

923

68 
qed "Un_upper1";


69 

5316

70 
Goal "B <= A Un B";

2893

71 
by (Blast_tac 1);

923

72 
qed "Un_upper2";


73 

5316

74 
Goal "[ A<=C; B<=C ] ==> A Un B <= C";

2893

75 
by (Blast_tac 1);

923

76 
qed "Un_least";


77 


78 
(*** Finite Intersection  the greatest lower bound of 2 sets *)


79 

5316

80 
Goal "A Int B <= A";

2893

81 
by (Blast_tac 1);

923

82 
qed "Int_lower1";


83 

5316

84 
Goal "A Int B <= B";

2893

85 
by (Blast_tac 1);

923

86 
qed "Int_lower2";


87 

5316

88 
Goal "[ C<=A; C<=B ] ==> C <= A Int B";

2893

89 
by (Blast_tac 1);

923

90 
qed "Int_greatest";


91 


92 
(*** Set difference ***)


93 

7007

94 
Goal "AB <= (A::'a set)";


95 
by (Blast_tac 1) ;


96 
qed "Diff_subset";

923

97 


98 
(*** Monotonicity ***)


99 

5316

100 
Goal "mono(f) ==> f(A) Un f(B) <= f(A Un B)";

923

101 
by (rtac Un_least 1);

5316

102 
by (etac (Un_upper1 RSN (2,monoD)) 1);


103 
by (etac (Un_upper2 RSN (2,monoD)) 1);

923

104 
qed "mono_Un";


105 

5316

106 
Goal "mono(f) ==> f(A Int B) <= f(A) Int f(B)";

923

107 
by (rtac Int_greatest 1);

5316

108 
by (etac (Int_lower1 RSN (2,monoD)) 1);


109 
by (etac (Int_lower2 RSN (2,monoD)) 1);

923

110 
qed "mono_Int";
