src/HOL/Tools/ATP/atp_translate.ML
changeset 44634 2ac4ff398bc3
parent 44626 a40b713232c8
child 44738 1b333e4173a2
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Sep 01 16:16:25 2011 +0900
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Sep 01 13:18:27 2011 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4  
     1.5    datatype order = First_Order | Higher_Order
     1.6    datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
     1.7 -  datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
     1.8 +  datatype soundness = Sound_Modulo_Infiniteness | Sound
     1.9    datatype type_level =
    1.10      All_Types |
    1.11      Noninf_Nonmono_Types of soundness |
    1.12 @@ -536,7 +536,7 @@
    1.13  
    1.14  datatype order = First_Order | Higher_Order
    1.15  datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
    1.16 -datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
    1.17 +datatype soundness = Sound_Modulo_Infiniteness | Sound
    1.18  datatype type_level =
    1.19    All_Types |
    1.20    Noninf_Nonmono_Types of soundness |
    1.21 @@ -1133,11 +1133,10 @@
    1.22  (* These types witness that the type classes they belong to allow infinite
    1.23     models and hence that any types with these type classes is monotonic. *)
    1.24  val known_infinite_types =
    1.25 -  [@{typ nat}, Type ("Int.int", []), @{typ "nat => bool"}]
    1.26 +  [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}]
    1.27  
    1.28  fun is_type_kind_of_surely_infinite ctxt soundness cached_Ts T =
    1.29 -  soundness <> Sound andalso
    1.30 -  is_type_surely_infinite ctxt (soundness <> Unsound) cached_Ts T
    1.31 +  soundness <> Sound andalso is_type_surely_infinite ctxt true cached_Ts T
    1.32  
    1.33  (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
    1.34     dangerous because their "exhaust" properties can easily lead to unsound ATP
    1.35 @@ -1860,11 +1859,14 @@
    1.36    end
    1.37  
    1.38  (* We add "bool" in case the helper "True_or_False" is included later. *)
    1.39 -val default_mono =
    1.40 +fun default_mono level =
    1.41    {maybe_finite_Ts = [@{typ bool}],
    1.42     surely_finite_Ts = [@{typ bool}],
    1.43     maybe_infinite_Ts = known_infinite_types,
    1.44 -   surely_infinite_Ts = known_infinite_types,
    1.45 +   surely_infinite_Ts =
    1.46 +     case level of
    1.47 +       Noninf_Nonmono_Types Sound => []
    1.48 +     | _ => known_infinite_types,
    1.49     maybe_nonmono_Ts = [@{typ bool}]}
    1.50  
    1.51  (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
    1.52 @@ -1919,7 +1921,7 @@
    1.53                 (add_iterm_mononotonicity_info ctxt level) iformula
    1.54  fun mononotonicity_info_for_facts ctxt type_enc facts =
    1.55    let val level = level_of_type_enc type_enc in
    1.56 -    default_mono
    1.57 +    default_mono level
    1.58      |> is_type_level_monotonicity_based level
    1.59         ? fold (add_fact_mononotonicity_info ctxt level) facts
    1.60    end