src/HOL/UNITY/LessThan.ML
changeset 6825 30e09714eef5
parent 6707 3b07e62a718c
child 7521 a18adacbdbd2
equal deleted inserted replaced
6824:8f7bfd81a4c6 6825:30e09714eef5
    26 
    26 
    27 Goalw [lessThan_def, atMost_def] "lessThan (Suc k) = atMost k";
    27 Goalw [lessThan_def, atMost_def] "lessThan (Suc k) = atMost k";
    28 by (simp_tac (simpset() addsimps [less_Suc_eq_le]) 1);
    28 by (simp_tac (simpset() addsimps [less_Suc_eq_le]) 1);
    29 qed "lessThan_Suc_atMost";
    29 qed "lessThan_Suc_atMost";
    30 
    30 
       
    31 Goal "finite (lessThan k)";
       
    32 by (induct_tac "k" 1);
       
    33 by (simp_tac (simpset() addsimps [lessThan_Suc]) 2);
       
    34 by Auto_tac;
       
    35 qed "finite_lessThan";
       
    36 
    31 Goal "(UN m. lessThan m) = UNIV";
    37 Goal "(UN m. lessThan m) = UNIV";
    32 by (Blast_tac 1);
    38 by (Blast_tac 1);
    33 qed "UN_lessThan_UNIV";
    39 qed "UN_lessThan_UNIV";
    34 
    40 
    35 Goalw [lessThan_def, atLeast_def, le_def]
    41 Goalw [lessThan_def, atLeast_def, le_def]
   122 Goalw [atMost_def] "atMost (Suc k) = insert (Suc k) (atMost k)";
   128 Goalw [atMost_def] "atMost (Suc k) = insert (Suc k) (atMost k)";
   123 by (simp_tac (simpset() addsimps [less_Suc_eq, order_le_less]) 1);
   129 by (simp_tac (simpset() addsimps [less_Suc_eq, order_le_less]) 1);
   124 by (Blast_tac 1);
   130 by (Blast_tac 1);
   125 qed "atMost_Suc";
   131 qed "atMost_Suc";
   126 
   132 
       
   133 Goal "finite (atMost k)";
       
   134 by (induct_tac "k" 1);
       
   135 by (simp_tac (simpset() addsimps [atMost_Suc]) 2);
       
   136 by Auto_tac;
       
   137 qed "finite_atMost";
       
   138 
   127 Goal "(UN m. atMost m) = UNIV";
   139 Goal "(UN m. atMost m) = UNIV";
   128 by (Blast_tac 1);
   140 by (Blast_tac 1);
   129 qed "UN_atMost_UNIV";
   141 qed "UN_atMost_UNIV";
   130 
   142 
   131 Goalw [atMost_def, le_def]
   143 Goalw [atMost_def, le_def]