src/CCL/subset.ML
changeset 0 a5a9c433f639
child 8 c3d2c6dcf3f0
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/CCL/subset.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,129 @@
     1.4 +(*  Title: 	CCL/subset
     1.5 +    ID:         $Id$
     1.6 +
     1.7 +Modified version of
     1.8 +    Title: 	HOL/subset
     1.9 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    1.10 +    Copyright   1991  University of Cambridge
    1.11 +
    1.12 +Derived rules involving subsets
    1.13 +Union and Intersection as lattice operations
    1.14 +*)
    1.15 +
    1.16 +(*** Big Union -- least upper bound of a set  ***)
    1.17 +
    1.18 +val prems = goal Set.thy
    1.19 +    "B:A ==> B <= Union(A)";
    1.20 +by (REPEAT (ares_tac (prems@[subsetI,UnionI]) 1));
    1.21 +val Union_upper = result();
    1.22 +
    1.23 +val prems = goal Set.thy
    1.24 +    "[| !!X. X:A ==> X<=C |] ==> Union(A) <= C";
    1.25 +by (REPEAT (ares_tac [subsetI] 1
    1.26 +     ORELSE eresolve_tac ([UnionE] @ (prems RL [subsetD])) 1));
    1.27 +val Union_least = result();
    1.28 +
    1.29 +
    1.30 +(*** Big Intersection -- greatest lower bound of a set ***)
    1.31 +
    1.32 +val prems = goal Set.thy
    1.33 +    "B:A ==> Inter(A) <= B";
    1.34 +by (REPEAT (resolve_tac (prems@[subsetI]) 1
    1.35 +     ORELSE etac InterD 1));
    1.36 +val Inter_lower = result();
    1.37 +
    1.38 +val prems = goal Set.thy
    1.39 +    "[| !!X. X:A ==> C<=X |] ==> C <= Inter(A)";
    1.40 +by (REPEAT (ares_tac [subsetI,InterI] 1
    1.41 +     ORELSE eresolve_tac (prems RL [subsetD]) 1));
    1.42 +val Inter_greatest = result();
    1.43 +
    1.44 +(*** Finite Union -- the least upper bound of 2 sets ***)
    1.45 +
    1.46 +goal Set.thy "A <= A Un B";
    1.47 +by (REPEAT (ares_tac [subsetI,UnI1] 1));
    1.48 +val Un_upper1 = result();
    1.49 +
    1.50 +goal Set.thy "B <= A Un B";
    1.51 +by (REPEAT (ares_tac [subsetI,UnI2] 1));
    1.52 +val Un_upper2 = result();
    1.53 +
    1.54 +val prems = goal Set.thy "[| A<=C;  B<=C |] ==> A Un B <= C";
    1.55 +by (cut_facts_tac prems 1);
    1.56 +by (DEPTH_SOLVE (ares_tac [subsetI] 1 
    1.57 +          ORELSE eresolve_tac [UnE,subsetD] 1));
    1.58 +val Un_least = result();
    1.59 +
    1.60 +(*** Finite Intersection -- the greatest lower bound of 2 sets *)
    1.61 +
    1.62 +goal Set.thy "A Int B <= A";
    1.63 +by (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1));
    1.64 +val Int_lower1 = result();
    1.65 +
    1.66 +goal Set.thy "A Int B <= B";
    1.67 +by (REPEAT (ares_tac [subsetI] 1 ORELSE etac IntE 1));
    1.68 +val Int_lower2 = result();
    1.69 +
    1.70 +val prems = goal Set.thy "[| C<=A;  C<=B |] ==> C <= A Int B";
    1.71 +by (cut_facts_tac prems 1);
    1.72 +by (REPEAT (ares_tac [subsetI,IntI] 1
    1.73 +     ORELSE etac subsetD 1));
    1.74 +val Int_greatest = result();
    1.75 +
    1.76 +(*** Monotonicity ***)
    1.77 +
    1.78 +val [prem] = goalw Set.thy [mono_def]
    1.79 +    "[| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)";
    1.80 +by (REPEAT (ares_tac [allI, impI, prem] 1));
    1.81 +val monoI = result();
    1.82 +
    1.83 +val [major,minor] = goalw Set.thy [mono_def]
    1.84 +    "[| mono(f);  A <= B |] ==> f(A) <= f(B)";
    1.85 +by (rtac (major RS spec RS spec RS mp) 1);
    1.86 +by (rtac minor 1);
    1.87 +val monoD = result();
    1.88 +
    1.89 +val [prem] = goalw Set.thy [mono_def] "(!!x.f(x) = g(x)) ==> mono(f) <-> mono(g)";
    1.90 +by (REPEAT (resolve_tac (iff_refl::FOL_congs @ [prem RS subst]) 1));
    1.91 +val mono_cong = result();
    1.92 +
    1.93 +val [prem] = goal Set.thy "mono(f) ==> f(A) Un f(B) <= f(A Un B)";
    1.94 +by (rtac Un_least 1);
    1.95 +by (rtac (Un_upper1 RS (prem RS monoD)) 1);
    1.96 +by (rtac (Un_upper2 RS (prem RS monoD)) 1);
    1.97 +val mono_Un = result();
    1.98 +
    1.99 +val [prem] = goal Set.thy "mono(f) ==> f(A Int B) <= f(A) Int f(B)";
   1.100 +by (rtac Int_greatest 1);
   1.101 +by (rtac (Int_lower1 RS (prem RS monoD)) 1);
   1.102 +by (rtac (Int_lower2 RS (prem RS monoD)) 1);
   1.103 +val mono_Int = result();
   1.104 +
   1.105 +(****)
   1.106 +
   1.107 +val set_cs = FOL_cs 
   1.108 +    addSIs [ballI, subsetI, InterI, INT_I, CollectI, 
   1.109 +	    ComplI, IntI, UnCI, singletonI] 
   1.110 +    addIs  [bexI, UnionI, UN_I] 
   1.111 +    addSEs [bexE, UnionE, UN_E,
   1.112 +	    CollectE, ComplE, IntE, UnE, emptyE, singletonE] 
   1.113 +    addEs  [ballE, InterD, InterE, INT_D, INT_E, subsetD, subsetCE];
   1.114 +
   1.115 +fun cfast_tac prems = cut_facts_tac prems THEN' fast_tac set_cs;
   1.116 +
   1.117 +fun prover s = prove_goal Set.thy s (fn _=>[fast_tac set_cs 1]);
   1.118 +
   1.119 +val mem_rews = [trivial_set,empty_eq] @ (map prover
   1.120 + [ "(a : A Un B)   <->  (a:A | a:B)",
   1.121 +   "(a : A Int B)  <->  (a:A & a:B)",
   1.122 +   "(a : Compl(B)) <->  (~a:B)",
   1.123 +   "(a : {b})      <->  (a=b)",
   1.124 +   "(a : {})       <->   False",
   1.125 +   "(a : {x.P(x)}) <->  P(a)" ]);
   1.126 +
   1.127 +val set_congs = 
   1.128 +    [Collect_cong, ball_cong, bex_cong, INT_cong, UN_cong, mono_cong] @ 
   1.129 +    mk_congs Set.thy ["Compl", "op Int", "op Un", "Union", "Inter", 
   1.130 +		      "op :", "op <=", "singleton"];
   1.131 +
   1.132 +val set_ss = FOL_ss addcongs set_congs addrews mem_rews;