src/HOL/UNITY/LessThan.ML
author paulson
Fri Apr 03 12:34:33 1998 +0200 (1998-04-03)
changeset 4776 1f9362e769c1
child 5069 3ea049f7979d
permissions -rw-r--r--
New UNITY theory
     1 (*  Title:      HOL/LessThan/LessThan
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 lessThan, greaterThan, atLeast, atMost
     7 *)
     8 
     9 
    10 open LessThan;
    11 
    12 
    13 (*** lessThan ***)
    14 
    15 goalw thy [lessThan_def] "(i: lessThan k) = (i<k)";
    16 by (Blast_tac 1);
    17 qed "lessThan_iff";
    18 AddIffs [lessThan_iff];
    19 
    20 goalw thy [lessThan_def] "lessThan 0 = {}";
    21 by (Simp_tac 1);
    22 qed "lessThan_0";
    23 Addsimps [lessThan_0];
    24 
    25 goalw thy [lessThan_def] "lessThan (Suc k) = insert k (lessThan k)";
    26 by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
    27 by (Blast_tac 1);
    28 qed "lessThan_Suc";
    29 
    30 goal thy "(UN m. lessThan m) = UNIV";
    31 by (Blast_tac 1);
    32 qed "UN_lessThan_UNIV";
    33 
    34 goalw thy [lessThan_def, atLeast_def, le_def]
    35     "Compl(lessThan k) = atLeast k";
    36 by (Blast_tac 1);
    37 qed "Compl_lessThan";
    38 
    39 
    40 (*** greaterThan ***)
    41 
    42 goalw thy [greaterThan_def] "(i: greaterThan k) = (k<i)";
    43 by (Blast_tac 1);
    44 qed "greaterThan_iff";
    45 AddIffs [greaterThan_iff];
    46 
    47 goalw thy [greaterThan_def] "greaterThan 0 = range Suc";
    48 by (blast_tac (claset() addIs [Suc_pred RS sym]) 1);
    49 qed "greaterThan_0";
    50 Addsimps [greaterThan_0];
    51 
    52 goalw thy [greaterThan_def] "greaterThan (Suc k) = greaterThan k - {Suc k}";
    53 by Safe_tac;
    54 by (blast_tac (claset() addIs [less_trans]) 1);
    55 by (asm_simp_tac (simpset() addsimps [le_Suc_eq, not_le_iff_less RS sym]) 1);
    56 by (asm_simp_tac (simpset() addsimps [not_le_iff_less]) 1);
    57 qed "greaterThan_Suc";
    58 
    59 goal thy "(INT m. greaterThan m) = {}";
    60 by (Blast_tac 1);
    61 qed "INT_greaterThan_UNIV";
    62 
    63 goalw thy [greaterThan_def, atMost_def, le_def]
    64     "Compl(greaterThan k) = atMost k";
    65 by (Blast_tac 1);
    66 qed "Compl_greaterThan";
    67 
    68 goalw thy [greaterThan_def, atMost_def, le_def]
    69     "Compl(atMost k) = greaterThan k";
    70 by (Blast_tac 1);
    71 qed "Compl_atMost";
    72 
    73 goal thy "less_than ^^ {k} = greaterThan k";
    74 by (Blast_tac 1);
    75 qed "Image_less_than";
    76 
    77 Addsimps [Compl_greaterThan, Compl_atMost, Image_less_than];
    78 
    79 (*** atLeast ***)
    80 
    81 goalw thy [atLeast_def] "(i: atLeast k) = (k<=i)";
    82 by (Blast_tac 1);
    83 qed "atLeast_iff";
    84 AddIffs [atLeast_iff];
    85 
    86 goalw thy [atLeast_def, UNIV_def] "atLeast 0 = UNIV";
    87 by (Simp_tac 1);
    88 qed "atLeast_0";
    89 Addsimps [atLeast_0];
    90 
    91 goalw thy [atLeast_def] "atLeast (Suc k) = atLeast k - {k}";
    92 by (simp_tac (simpset() addsimps [Suc_le_eq]) 1);
    93 by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
    94 by (Blast_tac 1);
    95 qed "atLeast_Suc";
    96 
    97 goal thy "(UN m. atLeast m) = UNIV";
    98 by (Blast_tac 1);
    99 qed "UN_atLeast_UNIV";
   100 
   101 goalw thy [lessThan_def, atLeast_def, le_def]
   102     "Compl(atLeast k) = lessThan k";
   103 by (Blast_tac 1);
   104 qed "Compl_atLeast";
   105 
   106 goal thy "less_than^-1 ^^ {k} = lessThan k";
   107 by (Blast_tac 1);
   108 qed "Image_inverse_less_than";
   109 
   110 Addsimps [Compl_lessThan, Compl_atLeast, Image_inverse_less_than];
   111 
   112 (*** atMost ***)
   113 
   114 goalw thy [atMost_def] "(i: atMost k) = (i<=k)";
   115 by (Blast_tac 1);
   116 qed "atMost_iff";
   117 AddIffs [atMost_iff];
   118 
   119 goalw thy [atMost_def] "atMost 0 = {0}";
   120 by (Simp_tac 1);
   121 qed "atMost_0";
   122 Addsimps [atMost_0];
   123 
   124 goalw thy [atMost_def] "atMost (Suc k) = insert (Suc k) (atMost k)";
   125 by (simp_tac (simpset() addsimps [less_Suc_eq, le_eq_less_or_eq]) 1);
   126 by (Blast_tac 1);
   127 qed "atMost_Suc";
   128 
   129 goal thy "(UN m. atMost m) = UNIV";
   130 by (Blast_tac 1);
   131 qed "UN_atMost_UNIV";
   132 
   133 goalw thy [atMost_def, le_def]
   134     "Compl(atMost k) = greaterThan k";
   135 by (Blast_tac 1);
   136 qed "Compl_atMost";
   137 Addsimps [Compl_atMost];
   138 
   139 
   140 (*** Combined properties ***)
   141 
   142 goal thy "atMost n Int atLeast n = {n}";
   143 by (blast_tac (claset() addIs [le_anti_sym]) 1);
   144 qed "atMost_Int_atLeast";
   145 
   146