src/HOL/SetInterval.ML
author nipkow
Mon Sep 30 15:44:21 2002 +0200 (2002-09-30)
changeset 13596 ee5f79b210c1
parent 9310 ab706fdb0842
child 13735 7de9342aca7a
permissions -rw-r--r--
modified induct method
     1 (*  Title:      HOL/SetInterval.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   2000  TU Muenchen
     5 
     6 Set Intervals: lessThan, greaterThan, atLeast, atMost
     7 *)
     8 
     9 
    10 (*** lessThan ***)
    11 
    12 Goalw [lessThan_def] "(i: lessThan k) = (i<k)";
    13 by (Blast_tac 1);
    14 qed "lessThan_iff";
    15 AddIffs [lessThan_iff];
    16 
    17 Goalw [lessThan_def] "lessThan (0::nat) = {}";
    18 by (Simp_tac 1);
    19 qed "lessThan_0";
    20 Addsimps [lessThan_0];
    21 
    22 Goalw [lessThan_def] "lessThan (Suc k) = insert k (lessThan k)";
    23 by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
    24 by (Blast_tac 1);
    25 qed "lessThan_Suc";
    26 
    27 Goalw [lessThan_def, atMost_def] "lessThan (Suc k) = atMost k";
    28 by (simp_tac (simpset() addsimps [less_Suc_eq_le]) 1);
    29 qed "lessThan_Suc_atMost";
    30 
    31 Goal "(UN m::nat. lessThan m) = UNIV";
    32 by (Blast_tac 1);
    33 qed "UN_lessThan_UNIV";
    34 
    35 Goalw [lessThan_def, atLeast_def]
    36     "!!k:: 'a::linorder. -lessThan k = atLeast k";
    37 by Auto_tac;
    38 by (blast_tac (claset() addIs [linorder_not_less RS iffD1]) 1);
    39 by (blast_tac (claset() addDs [order_le_less_trans]) 1);
    40 qed "Compl_lessThan";
    41 
    42 Goal "!!k:: 'a::order. {k} - lessThan k = {k}";
    43 by Auto_tac;
    44 qed "single_Diff_lessThan";
    45 Addsimps [single_Diff_lessThan];
    46 
    47 (*** greaterThan ***)
    48 
    49 Goalw [greaterThan_def] "(i: greaterThan k) = (k<i)";
    50 by (Blast_tac 1);
    51 qed "greaterThan_iff";
    52 AddIffs [greaterThan_iff];
    53 
    54 Goalw [greaterThan_def] "greaterThan 0 = range Suc";
    55 by (blast_tac (claset() addDs [gr0_conv_Suc RS iffD1]) 1);
    56 qed "greaterThan_0";
    57 Addsimps [greaterThan_0];
    58 
    59 Goalw [greaterThan_def] "greaterThan (Suc k) = greaterThan k - {Suc k}";
    60 by (auto_tac (claset() addEs [linorder_neqE], simpset()));
    61 qed "greaterThan_Suc";
    62 
    63 Goal "(INT m::nat. greaterThan m) = {}";
    64 by (Blast_tac 1);
    65 qed "INT_greaterThan_UNIV";
    66 
    67 Goalw [greaterThan_def, atMost_def, le_def]
    68     "!!k:: 'a::linorder. -greaterThan k = atMost k";
    69 by Auto_tac;
    70 by (blast_tac (claset() addIs [linorder_not_less RS iffD1]) 1);
    71 by (blast_tac (claset() addDs [order_le_less_trans]) 1);
    72 qed "Compl_greaterThan";
    73 
    74 Goal "!!k:: 'a::linorder. -atMost k = greaterThan k";
    75 by (simp_tac (simpset() addsimps [Compl_greaterThan RS sym]) 1);
    76 qed "Compl_atMost";
    77 
    78 Addsimps [Compl_greaterThan, Compl_atMost];
    79 
    80 (*** atLeast ***)
    81 
    82 Goalw [atLeast_def] "(i: atLeast k) = (k<=i)";
    83 by (Blast_tac 1);
    84 qed "atLeast_iff";
    85 AddIffs [atLeast_iff];
    86 
    87 Goalw [atLeast_def, UNIV_def] "atLeast (0::nat) = UNIV";
    88 by (Simp_tac 1);
    89 qed "atLeast_0";
    90 Addsimps [atLeast_0];
    91 
    92 Goalw [atLeast_def] "atLeast (Suc k) = atLeast k - {k}";
    93 by (simp_tac (simpset() addsimps [Suc_le_eq]) 1);
    94 by (simp_tac (simpset() addsimps [order_le_less]) 1);
    95 by (Blast_tac 1);
    96 qed "atLeast_Suc";
    97 
    98 Goal "(UN m::nat. atLeast m) = UNIV";
    99 by (Blast_tac 1);
   100 qed "UN_atLeast_UNIV";
   101 
   102 Goalw [lessThan_def, atLeast_def, le_def]
   103     "!!k:: 'a::linorder. -atLeast k = lessThan k";
   104 by Auto_tac;
   105 by (blast_tac (claset() addIs [linorder_not_less RS iffD1]) 1);
   106 by (blast_tac (claset() addDs [order_le_less_trans]) 1);
   107 qed "Compl_atLeast";
   108 
   109 Addsimps [Compl_lessThan, Compl_atLeast];
   110 
   111 (*** atMost ***)
   112 
   113 Goalw [atMost_def] "(i: atMost k) = (i<=k)";
   114 by (Blast_tac 1);
   115 qed "atMost_iff";
   116 AddIffs [atMost_iff];
   117 
   118 Goalw [atMost_def] "atMost (0::nat) = {0}";
   119 by (Simp_tac 1);
   120 qed "atMost_0";
   121 Addsimps [atMost_0];
   122 
   123 Goalw [atMost_def] "atMost (Suc k) = insert (Suc k) (atMost k)";
   124 by (simp_tac (simpset() addsimps [less_Suc_eq, order_le_less]) 1);
   125 by (Blast_tac 1);
   126 qed "atMost_Suc";
   127 
   128 Goal "(UN m::nat. atMost m) = UNIV";
   129 by (Blast_tac 1);
   130 qed "UN_atMost_UNIV";
   131 
   132 
   133 (*** Combined properties ***)
   134 
   135 Goal "!!n:: 'a::order. atMost n Int atLeast n = {n}";
   136 by (blast_tac (claset() addIs [order_antisym]) 1);
   137 qed "atMost_Int_atLeast";