src/CCL/subset.ML
author paulson
Fri Feb 16 17:24:51 1996 +0100 (1996-02-16)
changeset 1511 09354d37a5ab
parent 1459 d12da312eff4
child 1963 a4abf41134e2
permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
clasohm@1459
     1
(*  Title:      CCL/subset
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
clasohm@0
     4
Modified version of
clasohm@1459
     5
    Title:      HOL/subset
clasohm@1459
     6
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     7
    Copyright   1991  University of Cambridge
clasohm@0
     8
clasohm@0
     9
Derived rules involving subsets
clasohm@0
    10
Union and Intersection as lattice operations
clasohm@0
    11
*)
clasohm@0
    12
clasohm@0
    13
(*** Big Union -- least upper bound of a set  ***)
clasohm@0
    14
clasohm@0
    15
val prems = goal Set.thy
clasohm@0
    16
    "B:A ==> B <= Union(A)";
clasohm@0
    17
by (REPEAT (ares_tac (prems@[subsetI,UnionI]) 1));
clasohm@757
    18
qed "Union_upper";
clasohm@0
    19
clasohm@0
    20
val prems = goal Set.thy
clasohm@0
    21
    "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C";
clasohm@0
    22
by (REPEAT (ares_tac [subsetI] 1
clasohm@0
    23
     ORELSE eresolve_tac ([UnionE] @ (prems RL [subsetD])) 1));
clasohm@757
    24
qed "Union_least";
clasohm@0
    25
clasohm@0
    26
clasohm@0
    27
(*** Big Intersection -- greatest lower bound of a set ***)
clasohm@0
    28
clasohm@0
    29
val prems = goal Set.thy
clasohm@0
    30
    "B:A ==> Inter(A) <= B";
clasohm@0
    31
by (REPEAT (resolve_tac (prems@[subsetI]) 1
clasohm@0
    32
     ORELSE etac InterD 1));
clasohm@757
    33
qed "Inter_lower";
clasohm@0
    34
clasohm@0
    35
val prems = goal Set.thy
clasohm@0
    36
    "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)";
clasohm@0
    37
by (REPEAT (ares_tac [subsetI,InterI] 1
clasohm@0
    38
     ORELSE eresolve_tac (prems RL [subsetD]) 1));
clasohm@757
    39
qed "Inter_greatest";
clasohm@0
    40
clasohm@0
    41
(*** Finite Union -- the least upper bound of 2 sets ***)
clasohm@0
    42
clasohm@0
    43
goal Set.thy "A <= A Un B";
clasohm@0
    44
by (REPEAT (ares_tac [subsetI,UnI1] 1));
clasohm@757
    45
qed "Un_upper1";
clasohm@0
    46
clasohm@0
    47
goal Set.thy "B <= A Un B";
clasohm@0
    48
by (REPEAT (ares_tac [subsetI,UnI2] 1));
clasohm@757
    49
qed "Un_upper2";
clasohm@0
    50
clasohm@0
    51
val prems = goal Set.thy "[| A<=C;  B<=C |] ==> A Un B <= C";
clasohm@0
    52
by (cut_facts_tac prems 1);
clasohm@0
    53
by (DEPTH_SOLVE (ares_tac [subsetI] 1 
clasohm@0
    54
          ORELSE eresolve_tac [UnE,subsetD] 1));
clasohm@757
    55
qed "Un_least";
clasohm@0
    56
clasohm@0
    57
(*** Finite Intersection -- the greatest lower bound of 2 sets *)
clasohm@0
    58
clasohm@0
    59
goal Set.thy "A Int B <= A";
clasohm@0
    60
by (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1));
clasohm@757
    61
qed "Int_lower1";
clasohm@0
    62
clasohm@0
    63
goal Set.thy "A Int B <= B";
clasohm@0
    64
by (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1));
clasohm@757
    65
qed "Int_lower2";
clasohm@0
    66
clasohm@0
    67
val prems = goal Set.thy "[| C<=A;  C<=B |] ==> C <= A Int B";
clasohm@0
    68
by (cut_facts_tac prems 1);
clasohm@0
    69
by (REPEAT (ares_tac [subsetI,IntI] 1
clasohm@0
    70
     ORELSE etac subsetD 1));
clasohm@757
    71
qed "Int_greatest";
clasohm@0
    72
clasohm@0
    73
(*** Monotonicity ***)
clasohm@0
    74
clasohm@0
    75
val [prem] = goalw Set.thy [mono_def]
clasohm@0
    76
    "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)";
clasohm@0
    77
by (REPEAT (ares_tac [allI, impI, prem] 1));
clasohm@757
    78
qed "monoI";
clasohm@0
    79
clasohm@0
    80
val [major,minor] = goalw Set.thy [mono_def]
clasohm@0
    81
    "[| mono(f);  A <= B |] ==> f(A) <= f(B)";
clasohm@0
    82
by (rtac (major RS spec RS spec RS mp) 1);
clasohm@0
    83
by (rtac minor 1);
clasohm@757
    84
qed "monoD";
clasohm@0
    85
clasohm@0
    86
val [prem] = goal Set.thy "mono(f) ==> f(A) Un f(B) <= f(A Un B)";
clasohm@0
    87
by (rtac Un_least 1);
clasohm@0
    88
by (rtac (Un_upper1 RS (prem RS monoD)) 1);
clasohm@0
    89
by (rtac (Un_upper2 RS (prem RS monoD)) 1);
clasohm@757
    90
qed "mono_Un";
clasohm@0
    91
clasohm@0
    92
val [prem] = goal Set.thy "mono(f) ==> f(A Int B) <= f(A) Int f(B)";
clasohm@0
    93
by (rtac Int_greatest 1);
clasohm@0
    94
by (rtac (Int_lower1 RS (prem RS monoD)) 1);
clasohm@0
    95
by (rtac (Int_lower2 RS (prem RS monoD)) 1);
clasohm@757
    96
qed "mono_Int";
clasohm@0
    97
clasohm@0
    98
(****)
clasohm@0
    99
clasohm@0
   100
val set_cs = FOL_cs 
clasohm@0
   101
    addSIs [ballI, subsetI, InterI, INT_I, CollectI, 
clasohm@1459
   102
            ComplI, IntI, UnCI, singletonI] 
clasohm@0
   103
    addIs  [bexI, UnionI, UN_I] 
clasohm@0
   104
    addSEs [bexE, UnionE, UN_E,
clasohm@1459
   105
            CollectE, ComplE, IntE, UnE, emptyE, singletonE] 
clasohm@0
   106
    addEs  [ballE, InterD, InterE, INT_D, INT_E, subsetD, subsetCE];
clasohm@0
   107
clasohm@0
   108
fun cfast_tac prems = cut_facts_tac prems THEN' fast_tac set_cs;
clasohm@0
   109
clasohm@0
   110
fun prover s = prove_goal Set.thy s (fn _=>[fast_tac set_cs 1]);
clasohm@0
   111
clasohm@0
   112
val mem_rews = [trivial_set,empty_eq] @ (map prover
clasohm@0
   113
 [ "(a : A Un B)   <->  (a:A | a:B)",
clasohm@0
   114
   "(a : A Int B)  <->  (a:A & a:B)",
clasohm@0
   115
   "(a : Compl(B)) <->  (~a:B)",
clasohm@0
   116
   "(a : {b})      <->  (a=b)",
clasohm@0
   117
   "(a : {})       <->   False",
clasohm@0
   118
   "(a : {x.P(x)}) <->  P(a)" ]);
clasohm@0
   119
lcp@8
   120
val set_congs = [ball_cong, bex_cong, INT_cong, UN_cong];
clasohm@0
   121
lcp@8
   122
val set_ss = FOL_ss addcongs set_congs addsimps mem_rews;