merged
authorhaftmann
Mon Nov 30 08:08:31 2009 +0100 (2009-11-30)
changeset 33966b863967f23ea
parent 33965 f57c11db4ad4
parent 33936 6e77ca6d3a8f
child 33967 e191b400a8e0
merged
src/HOL/Inductive.thy
src/HOL/Tools/inductive.ML
     1.1 --- a/src/HOL/Inductive.thy	Fri Nov 27 08:42:50 2009 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Mon Nov 30 08:08:31 2009 +0100
     1.3 @@ -261,18 +261,13 @@
     1.4  theorems basic_monos =
     1.5    subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
     1.6    Collect_mono in_mono vimage_mono
     1.7 -  imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
     1.8 -  not_all not_ex
     1.9 -  Ball_def Bex_def
    1.10 -  induct_rulify_fallback
    1.11  
    1.12  use "Tools/inductive.ML"
    1.13  setup Inductive.setup
    1.14  
    1.15  theorems [mono] =
    1.16    imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
    1.17 -  imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
    1.18 -  not_all not_ex
    1.19 +  imp_mono not_mono
    1.20    Ball_def Bex_def
    1.21    induct_rulify_fallback
    1.22  
     2.1 --- a/src/HOL/Tools/inductive.ML	Fri Nov 27 08:42:50 2009 +0100
     2.2 +++ b/src/HOL/Tools/inductive.ML	Mon Nov 30 08:08:31 2009 +0100
     2.3 @@ -177,26 +177,22 @@
     2.4  
     2.5  fun mk_mono thm =
     2.6    let
     2.7 -    val concl = concl_of thm;
     2.8 -    fun eq2mono thm' = [thm' RS (thm' RS eq_to_mono)] @
     2.9 -      (case concl of
    2.10 -          (_ $ (_ $ (Const ("Not", _) $ _) $ _)) => []
    2.11 -        | _ => [thm' RS (thm' RS eq_to_mono2)]);
    2.12 +    fun eq2mono thm' = thm' RS (thm' RS eq_to_mono);
    2.13      fun dest_less_concl thm = dest_less_concl (thm RS @{thm le_funD})
    2.14        handle THM _ => thm RS @{thm le_boolD}
    2.15    in
    2.16 -    case concl of
    2.17 +    case concl_of thm of
    2.18        Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
    2.19      | _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm
    2.20      | _ $ (Const (@{const_name HOL.less_eq}, _) $ _ $ _) =>
    2.21 -      [dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
    2.22 -         (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))]
    2.23 -    | _ => [thm]
    2.24 +      dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
    2.25 +        (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))
    2.26 +    | _ => thm
    2.27    end handle THM _ =>
    2.28      error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm_without_context thm);
    2.29  
    2.30 -val mono_add = Thm.declaration_attribute (map_monos o fold Thm.add_thm o mk_mono);
    2.31 -val mono_del = Thm.declaration_attribute (map_monos o fold Thm.del_thm o mk_mono);
    2.32 +val mono_add = Thm.declaration_attribute (map_monos o Thm.add_thm o mk_mono);
    2.33 +val mono_del = Thm.declaration_attribute (map_monos o Thm.del_thm o mk_mono);
    2.34  
    2.35  
    2.36  
    2.37 @@ -338,7 +334,7 @@
    2.38        REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI'}] 1),
    2.39        REPEAT (FIRST
    2.40          [atac 1,
    2.41 -         resolve_tac (maps mk_mono monos @ get_monos ctxt) 1,
    2.42 +         resolve_tac (map mk_mono monos @ get_monos ctxt) 1,
    2.43           etac @{thm le_funE} 1, dtac @{thm le_boolD} 1])]));
    2.44  
    2.45