expand combinators in Isar proofs constructed by Sledgehammer;
authorblanchet
Thu Apr 29 01:17:14 2010 +0200 (2010-04-29)
changeset 365558ff45c2076da
parent 36554 2673979cb54d
child 36556 81dc2c20f052
expand combinators in Isar proofs constructed by Sledgehammer;
this requires shuffling around a couple of functions previously defined in Refute
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
src/HOL/Tools/Nitpick/nitpick_util.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
src/HOL/Tools/refute.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Apr 29 01:11:06 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Apr 29 01:17:14 2010 +0200
     1.3 @@ -1260,15 +1260,15 @@
     1.4    | t1 $ _ => term_under_def t1
     1.5    | _ => t
     1.6  
     1.7 -(* Here we crucially rely on "Refute.specialize_type" performing a preorder
     1.8 -   traversal of the term, without which the wrong occurrence of a constant could
     1.9 -   be matched in the face of overloading. *)
    1.10 +(* Here we crucially rely on "specialize_type" performing a preorder traversal
    1.11 +   of the term, without which the wrong occurrence of a constant could be
    1.12 +   matched in the face of overloading. *)
    1.13  fun def_props_for_const thy stds fast_descrs table (x as (s, _)) =
    1.14    if is_built_in_const thy stds fast_descrs x then
    1.15      []
    1.16    else
    1.17      these (Symtab.lookup table s)
    1.18 -    |> map_filter (try (Refute.specialize_type thy x))
    1.19 +    |> map_filter (try (specialize_type thy x))
    1.20      |> filter (curry (op =) (Const x) o term_under_def)
    1.21  
    1.22  fun normalized_rhs_of t =
    1.23 @@ -1381,8 +1381,8 @@
    1.24      SOME t' => is_constr_pattern_lhs thy t'
    1.25    | NONE => false
    1.26  
    1.27 -(* Similar to "Refute.specialize_type" but returns all matches rather than only
    1.28 -   the first (preorder) match. *)
    1.29 +(* Similar to "specialize_type" but returns all matches rather than only the
    1.30 +   first (preorder) match. *)
    1.31  fun multi_specialize_type thy slack (s, T) t =
    1.32    let
    1.33      fun aux (Const (s', T')) ys =
    1.34 @@ -1390,8 +1390,8 @@
    1.35            ys |> (if AList.defined (op =) ys T' then
    1.36                     I
    1.37                   else
    1.38 -                   cons (T', Refute.monomorphic_term
    1.39 -                                 (Sign.typ_match thy (T', T) Vartab.empty) t)
    1.40 +                   cons (T', monomorphic_term (Sign.typ_match thy (T', T)
    1.41 +                                                              Vartab.empty) t)
    1.42                     handle Type.TYPE_MATCH => I
    1.43                          | Refute.REFUTE _ =>
    1.44                            if slack then
    1.45 @@ -1682,7 +1682,7 @@
    1.46    let val abs_T = domain_type T in
    1.47      typedef_info thy (fst (dest_Type abs_T)) |> the
    1.48      |> pairf #Abs_inverse #Rep_inverse
    1.49 -    |> pairself (Refute.specialize_type thy x o prop_of o the)
    1.50 +    |> pairself (specialize_type thy x o prop_of o the)
    1.51      ||> single |> op ::
    1.52    end
    1.53  fun optimized_typedef_axioms thy (abs_z as (abs_s, _)) =
    1.54 @@ -1697,7 +1697,7 @@
    1.55          val set_t = Const (set_name, rep_T --> bool_T)
    1.56          val set_t' =
    1.57            prop_of_Rep |> HOLogic.dest_Trueprop
    1.58 -                      |> Refute.specialize_type thy (dest_Const rep_t)
    1.59 +                      |> specialize_type thy (dest_Const rep_t)
    1.60                        |> HOLogic.dest_mem |> snd
    1.61        in
    1.62          [HOLogic.all_const abs_T
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Apr 29 01:11:06 2010 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Apr 29 01:17:14 2010 +0200
     2.3 @@ -914,8 +914,8 @@
     2.4                   val class = Logic.class_of_const s
     2.5                   val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]),
     2.6                                                     class)
     2.7 -                 val ax1 = try (Refute.specialize_type thy x) of_class
     2.8 -                 val ax2 = Option.map (Refute.specialize_type thy x o snd)
     2.9 +                 val ax1 = try (specialize_type thy x) of_class
    2.10 +                 val ax2 = Option.map (specialize_type thy x o snd)
    2.11                                        (Refute.get_classdef thy class)
    2.12                 in
    2.13                   fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
    2.14 @@ -997,7 +997,7 @@
    2.15            map (fn t => case Term.add_tvars t [] of
    2.16                           [] => t
    2.17                         | [(x, S)] =>
    2.18 -                         Refute.monomorphic_term (Vartab.make [(x, (S, T))]) t
    2.19 +                         monomorphic_term (Vartab.make [(x, (S, T))]) t
    2.20                         | _ => raise TERM ("Nitpick_Preproc.axioms_for_term.\
    2.21                                            \add_axioms_for_sort", [t]))
    2.22                class_axioms
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Thu Apr 29 01:11:06 2010 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Thu Apr 29 01:17:14 2010 +0200
     3.3 @@ -57,6 +57,8 @@
     3.4    val bool_T : typ
     3.5    val nat_T : typ
     3.6    val int_T : typ
     3.7 +  val monomorphic_term : Type.tyenv -> term -> term
     3.8 +  val specialize_type : theory -> (string * typ) -> term -> term
     3.9    val nat_subscript : int -> string
    3.10    val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
    3.11    val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
    3.12 @@ -227,6 +229,9 @@
    3.13  val nat_T = @{typ nat}
    3.14  val int_T = @{typ int}
    3.15  
    3.16 +val monomorphic_term = Sledgehammer_Util.monomorphic_term
    3.17 +val specialize_type = Sledgehammer_Util.specialize_type
    3.18 +
    3.19  val subscript = implode o map (prefix "\<^isub>") o explode
    3.20  fun nat_subscript n =
    3.21    (* cheap trick to ensure proper alphanumeric ordering for one- and two-digit
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Apr 29 01:11:06 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Apr 29 01:17:14 2010 +0200
     4.3 @@ -392,6 +392,21 @@
     4.4    fold forall_of (Term.add_consts t []
     4.5                   |> filter (is_skolem_const_name o fst) |> map Const) t
     4.6  
     4.7 +val combinator_table =
     4.8 +  [(@{const_name COMBI}, @{thm COMBI_def_raw}),
     4.9 +   (@{const_name COMBK}, @{thm COMBK_def_raw}),
    4.10 +   (@{const_name COMBB}, @{thm COMBB_def_raw}),
    4.11 +   (@{const_name COMBC}, @{thm COMBC_def_raw}),
    4.12 +   (@{const_name COMBS}, @{thm COMBS_def_raw})]
    4.13 +
    4.14 +fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2))
    4.15 +  | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t')
    4.16 +  | uncombine_term (t as Const (x as (s, _))) =
    4.17 +    (case AList.lookup (op =) combinator_table s of
    4.18 +       SOME thm => thm |> prop_of |> specialize_type @{theory} x |> Logic.dest_equals |> snd
    4.19 +     | NONE => t)
    4.20 +  | uncombine_term t = t
    4.21 +
    4.22  (* Interpret a list of syntax trees as a clause, given by "real" literals and
    4.23     sort constraints. "vt" holds the initial sort constraints, from the
    4.24     conjecture clauses. *)
    4.25 @@ -435,15 +450,16 @@
    4.26        val t2 = clause_of_nodes ctxt vt us
    4.27        val (t1, t2) =
    4.28          HOLogic.eq_const HOLogic.typeT $ t1 $ t2
    4.29 -        |> unvarify_args |> check_clause ctxt |> HOLogic.dest_eq
    4.30 +        |> unvarify_args |> uncombine_term |> check_clause ctxt
    4.31 +        |> HOLogic.dest_eq
    4.32      in
    4.33        (Definition (num, t1, t2),
    4.34         fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
    4.35      end
    4.36    | decode_line vt (Inference (num, us, deps)) ctxt =
    4.37      let
    4.38 -      val t = us |> clause_of_nodes ctxt vt |> unskolemize_term
    4.39 -                 |> check_clause ctxt
    4.40 +      val t = us |> clause_of_nodes ctxt vt
    4.41 +                 |> unskolemize_term |> uncombine_term |> check_clause ctxt
    4.42      in
    4.43        (Inference (num, t, deps),
    4.44         fold Variable.declare_term (OldTerm.term_frees t) ctxt)
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Apr 29 01:11:06 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Apr 29 01:17:14 2010 +0200
     5.3 @@ -18,6 +18,8 @@
     5.4    val nat_subscript : int -> string
     5.5    val unyxml : string -> string
     5.6    val maybe_quote : string -> string
     5.7 +  val monomorphic_term : Type.tyenv -> term -> term
     5.8 +  val specialize_type : theory -> (string * typ) -> term -> term
     5.9  end;
    5.10   
    5.11  structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
    5.12 @@ -103,4 +105,30 @@
    5.13             OuterKeyword.is_keyword s) ? quote
    5.14    end
    5.15  
    5.16 +fun monomorphic_term subst t =
    5.17 +  map_types (map_type_tvar (fn v =>
    5.18 +      case Type.lookup subst v of
    5.19 +        SOME typ => typ
    5.20 +      | NONE => raise TERM ("monomorphic_term: uninstanitated schematic type \
    5.21 +                            \variable", [t]))) t
    5.22 +
    5.23 +fun specialize_type thy (s, T) t =
    5.24 +  let
    5.25 +    fun subst_for (Const (s', T')) =
    5.26 +      if s = s' then
    5.27 +        SOME (Sign.typ_match thy (T', T) Vartab.empty)
    5.28 +        handle Type.TYPE_MATCH => NONE
    5.29 +      else
    5.30 +        NONE
    5.31 +    | subst_for (t1 $ t2) =
    5.32 +      (case subst_for t1 of SOME x => SOME x | NONE => subst_for t2)
    5.33 +    | subst_for (Abs (_, _, t')) = subst_for t'
    5.34 +    | subst_for _ = NONE
    5.35 +  in
    5.36 +    case subst_for t of
    5.37 +      SOME subst => monomorphic_term subst t
    5.38 +    | NONE => raise Type.TYPE_MATCH
    5.39 +  end
    5.40 +
    5.41 +
    5.42  end;
     6.1 --- a/src/HOL/Tools/refute.ML	Thu Apr 29 01:11:06 2010 +0200
     6.2 +++ b/src/HOL/Tools/refute.ML	Thu Apr 29 01:17:14 2010 +0200
     6.3 @@ -70,8 +70,6 @@
     6.4    val is_IDT_constructor : theory -> string * typ -> bool
     6.5    val is_IDT_recursor : theory -> string * typ -> bool
     6.6    val is_const_of_class: theory -> string * typ -> bool
     6.7 -  val monomorphic_term : Type.tyenv -> term -> term
     6.8 -  val specialize_type : theory -> (string * typ) -> term -> term
     6.9    val string_of_typ : typ -> string
    6.10    val typ_of_dtyp : Datatype.descr -> (Datatype.dtyp * typ) list -> Datatype.dtyp -> typ
    6.11  end;  (* signature REFUTE *)
    6.12 @@ -449,57 +447,8 @@
    6.13        Term.all T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t
    6.14    end;
    6.15  
    6.16 -(* ------------------------------------------------------------------------- *)
    6.17 -(* monomorphic_term: applies a type substitution 'typeSubs' for all type     *)
    6.18 -(*                   variables in a term 't'                                 *)
    6.19 -(* ------------------------------------------------------------------------- *)
    6.20 -
    6.21 -  (* Type.tyenv -> Term.term -> Term.term *)
    6.22 -
    6.23 -  fun monomorphic_term typeSubs t =
    6.24 -    map_types (map_type_tvar
    6.25 -      (fn v =>
    6.26 -        case Type.lookup typeSubs v of
    6.27 -          NONE =>
    6.28 -          (* schematic type variable not instantiated *)
    6.29 -          raise REFUTE ("monomorphic_term",
    6.30 -            "no substitution for type variable " ^ fst (fst v) ^
    6.31 -            " in term " ^ Syntax.string_of_term_global Pure.thy t)
    6.32 -        | SOME typ =>
    6.33 -          typ)) t;
    6.34 -
    6.35 -(* ------------------------------------------------------------------------- *)
    6.36 -(* specialize_type: given a constant 's' of type 'T', which is a subterm of  *)
    6.37 -(*                  't', where 't' has a (possibly) more general type, the   *)
    6.38 -(*                  schematic type variables in 't' are instantiated to      *)
    6.39 -(*                  match the type 'T' (may raise Type.TYPE_MATCH)           *)
    6.40 -(* ------------------------------------------------------------------------- *)
    6.41 -
    6.42 -  (* theory -> (string * Term.typ) -> Term.term -> Term.term *)
    6.43 -
    6.44 -  fun specialize_type thy (s, T) t =
    6.45 -  let
    6.46 -    fun find_typeSubs (Const (s', T')) =
    6.47 -      if s=s' then
    6.48 -        SOME (Sign.typ_match thy (T', T) Vartab.empty)
    6.49 -          handle Type.TYPE_MATCH => NONE
    6.50 -      else
    6.51 -        NONE
    6.52 -      | find_typeSubs (Free _)           = NONE
    6.53 -      | find_typeSubs (Var _)            = NONE
    6.54 -      | find_typeSubs (Bound _)          = NONE
    6.55 -      | find_typeSubs (Abs (_, _, body)) = find_typeSubs body
    6.56 -      | find_typeSubs (t1 $ t2)          =
    6.57 -      (case find_typeSubs t1 of SOME x => SOME x
    6.58 -                              | NONE   => find_typeSubs t2)
    6.59 -  in
    6.60 -    case find_typeSubs t of
    6.61 -      SOME typeSubs =>
    6.62 -      monomorphic_term typeSubs t
    6.63 -    | NONE =>
    6.64 -      (* no match found - perhaps due to sort constraints *)
    6.65 -      raise Type.TYPE_MATCH
    6.66 -  end;
    6.67 +val monomorphic_term = Sledgehammer_Util.monomorphic_term
    6.68 +val specialize_type = Sledgehammer_Util.specialize_type
    6.69  
    6.70  (* ------------------------------------------------------------------------- *)
    6.71  (* is_const_of_class: returns 'true' iff 'Const (s, T)' is a constant that   *)