handle special constants correctly in Isar proof reconstruction code, especially type predicates
authorblanchet
Sun May 01 18:37:24 2011 +0200 (2011-05-01)
changeset 42549b9754f26c7bc
parent 42548 ea2a28b1938f
child 42550 3031d342d514
handle special constants correctly in Isar proof reconstruction code, especially type predicates
src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
     1.3 @@ -356,29 +356,33 @@
     1.4                list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
     1.5            end
     1.6          | SOME b =>
     1.7 -          if b = boolify_base then
     1.8 -            aux (SOME @{typ bool}) [] (hd us)
     1.9 -          else if b = explicit_app_base then
    1.10 -            aux opt_T (nth us 1 :: extra_us) (hd us)
    1.11 -          else
    1.12 -            let
    1.13 -              val (c, mangled_us) = b |> unmangled_const |>> invert_const
    1.14 -              val num_ty_args = num_atp_type_args thy type_sys c
    1.15 -              val (type_us, term_us) = chop num_ty_args us |>> append mangled_us
    1.16 -              (* Extra args from "hAPP" come after any arguments given directly
    1.17 -                 to the constant. *)
    1.18 -              val term_ts = map (aux NONE []) term_us
    1.19 -              val extra_ts = map (aux NONE []) extra_us
    1.20 -              val T =
    1.21 -                case opt_T of
    1.22 -                  SOME T => map fastype_of term_ts ---> T
    1.23 -                | NONE =>
    1.24 -                  if num_type_args thy c = length type_us then
    1.25 -                    Sign.const_instance thy (c,
    1.26 -                        map (type_from_fo_term tfrees) type_us)
    1.27 -                  else
    1.28 -                    HOLogic.typeT
    1.29 -            in list_comb (Const (c, T), term_ts @ extra_ts) end
    1.30 +          let val (b, mangled_us) = b |> unmangled_const |>> invert_const in
    1.31 +            if b = boolify_base then
    1.32 +              aux (SOME @{typ bool}) [] (hd us)
    1.33 +            else if b = explicit_app_base then
    1.34 +              aux opt_T (nth us 1 :: extra_us) (hd us)
    1.35 +            else if b = type_pred_base then
    1.36 +              @{const True}
    1.37 +            else
    1.38 +              let
    1.39 +                val num_ty_args = num_atp_type_args thy type_sys b
    1.40 +                val (type_us, term_us) =
    1.41 +                  chop num_ty_args us |>> append mangled_us
    1.42 +                (* Extra args from "hAPP" come after any arguments given
    1.43 +                   directly to the constant. *)
    1.44 +                val term_ts = map (aux NONE []) term_us
    1.45 +                val extra_ts = map (aux NONE []) extra_us
    1.46 +                val T =
    1.47 +                  case opt_T of
    1.48 +                    SOME T => map fastype_of term_ts ---> T
    1.49 +                  | NONE =>
    1.50 +                    if num_type_args thy b = length type_us then
    1.51 +                      Sign.const_instance thy
    1.52 +                          (b, map (type_from_fo_term tfrees) type_us)
    1.53 +                    else
    1.54 +                      HOLogic.typeT
    1.55 +              in list_comb (Const (b, T), term_ts @ extra_ts) end
    1.56 +          end
    1.57          | NONE => (* a free or schematic variable *)
    1.58            let
    1.59              val ts = map (aux NONE []) (us @ extra_us)
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
     2.3 @@ -23,6 +23,7 @@
     2.4    val conjecture_prefix : string
     2.5    val boolify_base : string
     2.6    val explicit_app_base : string
     2.7 +  val type_pred_base : string
     2.8    val is_type_system_sound : type_system -> bool
     2.9    val type_system_types_dangerous_types : type_system -> bool
    2.10    val num_atp_type_args : theory -> type_system -> string -> int
    2.11 @@ -514,8 +515,8 @@
    2.12    | _ => raise Fail "expected two-argument type constructor"
    2.13  
    2.14  fun type_pred_combatom type_sys ty tm =
    2.15 -  CombApp (CombConst ((const_prefix ^ type_pred_base, type_pred_base),
    2.16 -                      pred_combtyp ty, [ty]), tm)
    2.17 +  CombApp (CombConst (`make_fixed_const type_pred_base, pred_combtyp ty, [ty]),
    2.18 +           tm)
    2.19    |> repair_combterm_consts type_sys
    2.20    |> AAtom
    2.21