src/HOL/UNITY/LessThan.ML
changeset 4776 1f9362e769c1
child 5069 3ea049f7979d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/UNITY/LessThan.ML	Fri Apr 03 12:34:33 1998 +0200
     1.3 @@ -0,0 +1,146 @@
     1.4 +(*  Title:      HOL/LessThan/LessThan
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1998  University of Cambridge
     1.8 +
     1.9 +lessThan, greaterThan, atLeast, atMost
    1.10 +*)
    1.11 +
    1.12 +
    1.13 +open LessThan;
    1.14 +
    1.15 +
    1.16 +(*** lessThan ***)
    1.17 +
    1.18 +goalw thy [lessThan_def] "(i: lessThan k) = (i<k)";
    1.19 +by (Blast_tac 1);
    1.20 +qed "lessThan_iff";
    1.21 +AddIffs [lessThan_iff];
    1.22 +
    1.23 +goalw thy [lessThan_def] "lessThan 0 = {}";
    1.24 +by (Simp_tac 1);
    1.25 +qed "lessThan_0";
    1.26 +Addsimps [lessThan_0];
    1.27 +
    1.28 +goalw thy [lessThan_def] "lessThan (Suc k) = insert k (lessThan k)";
    1.29 +by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
    1.30 +by (Blast_tac 1);
    1.31 +qed "lessThan_Suc";
    1.32 +
    1.33 +goal thy "(UN m. lessThan m) = UNIV";
    1.34 +by (Blast_tac 1);
    1.35 +qed "UN_lessThan_UNIV";
    1.36 +
    1.37 +goalw thy [lessThan_def, atLeast_def, le_def]
    1.38 +    "Compl(lessThan k) = atLeast k";
    1.39 +by (Blast_tac 1);
    1.40 +qed "Compl_lessThan";
    1.41 +
    1.42 +
    1.43 +(*** greaterThan ***)
    1.44 +
    1.45 +goalw thy [greaterThan_def] "(i: greaterThan k) = (k<i)";
    1.46 +by (Blast_tac 1);
    1.47 +qed "greaterThan_iff";
    1.48 +AddIffs [greaterThan_iff];
    1.49 +
    1.50 +goalw thy [greaterThan_def] "greaterThan 0 = range Suc";
    1.51 +by (blast_tac (claset() addIs [Suc_pred RS sym]) 1);
    1.52 +qed "greaterThan_0";
    1.53 +Addsimps [greaterThan_0];
    1.54 +
    1.55 +goalw thy [greaterThan_def] "greaterThan (Suc k) = greaterThan k - {Suc k}";
    1.56 +by Safe_tac;
    1.57 +by (blast_tac (claset() addIs [less_trans]) 1);
    1.58 +by (asm_simp_tac (simpset() addsimps [le_Suc_eq, not_le_iff_less RS sym]) 1);
    1.59 +by (asm_simp_tac (simpset() addsimps [not_le_iff_less]) 1);
    1.60 +qed "greaterThan_Suc";
    1.61 +
    1.62 +goal thy "(INT m. greaterThan m) = {}";
    1.63 +by (Blast_tac 1);
    1.64 +qed "INT_greaterThan_UNIV";
    1.65 +
    1.66 +goalw thy [greaterThan_def, atMost_def, le_def]
    1.67 +    "Compl(greaterThan k) = atMost k";
    1.68 +by (Blast_tac 1);
    1.69 +qed "Compl_greaterThan";
    1.70 +
    1.71 +goalw thy [greaterThan_def, atMost_def, le_def]
    1.72 +    "Compl(atMost k) = greaterThan k";
    1.73 +by (Blast_tac 1);
    1.74 +qed "Compl_atMost";
    1.75 +
    1.76 +goal thy "less_than ^^ {k} = greaterThan k";
    1.77 +by (Blast_tac 1);
    1.78 +qed "Image_less_than";
    1.79 +
    1.80 +Addsimps [Compl_greaterThan, Compl_atMost, Image_less_than];
    1.81 +
    1.82 +(*** atLeast ***)
    1.83 +
    1.84 +goalw thy [atLeast_def] "(i: atLeast k) = (k<=i)";
    1.85 +by (Blast_tac 1);
    1.86 +qed "atLeast_iff";
    1.87 +AddIffs [atLeast_iff];
    1.88 +
    1.89 +goalw thy [atLeast_def, UNIV_def] "atLeast 0 = UNIV";
    1.90 +by (Simp_tac 1);
    1.91 +qed "atLeast_0";
    1.92 +Addsimps [atLeast_0];
    1.93 +
    1.94 +goalw thy [atLeast_def] "atLeast (Suc k) = atLeast k - {k}";
    1.95 +by (simp_tac (simpset() addsimps [Suc_le_eq]) 1);
    1.96 +by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
    1.97 +by (Blast_tac 1);
    1.98 +qed "atLeast_Suc";
    1.99 +
   1.100 +goal thy "(UN m. atLeast m) = UNIV";
   1.101 +by (Blast_tac 1);
   1.102 +qed "UN_atLeast_UNIV";
   1.103 +
   1.104 +goalw thy [lessThan_def, atLeast_def, le_def]
   1.105 +    "Compl(atLeast k) = lessThan k";
   1.106 +by (Blast_tac 1);
   1.107 +qed "Compl_atLeast";
   1.108 +
   1.109 +goal thy "less_than^-1 ^^ {k} = lessThan k";
   1.110 +by (Blast_tac 1);
   1.111 +qed "Image_inverse_less_than";
   1.112 +
   1.113 +Addsimps [Compl_lessThan, Compl_atLeast, Image_inverse_less_than];
   1.114 +
   1.115 +(*** atMost ***)
   1.116 +
   1.117 +goalw thy [atMost_def] "(i: atMost k) = (i<=k)";
   1.118 +by (Blast_tac 1);
   1.119 +qed "atMost_iff";
   1.120 +AddIffs [atMost_iff];
   1.121 +
   1.122 +goalw thy [atMost_def] "atMost 0 = {0}";
   1.123 +by (Simp_tac 1);
   1.124 +qed "atMost_0";
   1.125 +Addsimps [atMost_0];
   1.126 +
   1.127 +goalw thy [atMost_def] "atMost (Suc k) = insert (Suc k) (atMost k)";
   1.128 +by (simp_tac (simpset() addsimps [less_Suc_eq, le_eq_less_or_eq]) 1);
   1.129 +by (Blast_tac 1);
   1.130 +qed "atMost_Suc";
   1.131 +
   1.132 +goal thy "(UN m. atMost m) = UNIV";
   1.133 +by (Blast_tac 1);
   1.134 +qed "UN_atMost_UNIV";
   1.135 +
   1.136 +goalw thy [atMost_def, le_def]
   1.137 +    "Compl(atMost k) = greaterThan k";
   1.138 +by (Blast_tac 1);
   1.139 +qed "Compl_atMost";
   1.140 +Addsimps [Compl_atMost];
   1.141 +
   1.142 +
   1.143 +(*** Combined properties ***)
   1.144 +
   1.145 +goal thy "atMost n Int atLeast n = {n}";
   1.146 +by (blast_tac (claset() addIs [le_anti_sym]) 1);
   1.147 +qed "atMost_Int_atLeast";
   1.148 +
   1.149 +