# HG changeset patch # User blanchet # Date 1272496634 -7200 # Node ID 8ff45c2076da8b52e6db69dba8fd1120678a5fc3 # Parent 2673979cb54da14aaf0d9298be8b357042f1fbd9 expand combinators in Isar proofs constructed by Sledgehammer; this requires shuffling around a couple of functions previously defined in Refute diff -r 2673979cb54d -r 8ff45c2076da src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Apr 29 01:11:06 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Apr 29 01:17:14 2010 +0200 @@ -1260,15 +1260,15 @@ | t1 $ _ => term_under_def t1 | _ => t -(* Here we crucially rely on "Refute.specialize_type" performing a preorder - traversal of the term, without which the wrong occurrence of a constant could - be matched in the face of overloading. *) +(* Here we crucially rely on "specialize_type" performing a preorder traversal + of the term, without which the wrong occurrence of a constant could be + matched in the face of overloading. *) fun def_props_for_const thy stds fast_descrs table (x as (s, _)) = if is_built_in_const thy stds fast_descrs x then [] else these (Symtab.lookup table s) - |> map_filter (try (Refute.specialize_type thy x)) + |> map_filter (try (specialize_type thy x)) |> filter (curry (op =) (Const x) o term_under_def) fun normalized_rhs_of t = @@ -1381,8 +1381,8 @@ SOME t' => is_constr_pattern_lhs thy t' | NONE => false -(* Similar to "Refute.specialize_type" but returns all matches rather than only - the first (preorder) match. *) +(* Similar to "specialize_type" but returns all matches rather than only the + first (preorder) match. *) fun multi_specialize_type thy slack (s, T) t = let fun aux (Const (s', T')) ys = @@ -1390,8 +1390,8 @@ ys |> (if AList.defined (op =) ys T' then I else - cons (T', Refute.monomorphic_term - (Sign.typ_match thy (T', T) Vartab.empty) t) + cons (T', monomorphic_term (Sign.typ_match thy (T', T) + Vartab.empty) t) handle Type.TYPE_MATCH => I | Refute.REFUTE _ => if slack then @@ -1682,7 +1682,7 @@ let val abs_T = domain_type T in typedef_info thy (fst (dest_Type abs_T)) |> the |> pairf #Abs_inverse #Rep_inverse - |> pairself (Refute.specialize_type thy x o prop_of o the) + |> pairself (specialize_type thy x o prop_of o the) ||> single |> op :: end fun optimized_typedef_axioms thy (abs_z as (abs_s, _)) = @@ -1697,7 +1697,7 @@ val set_t = Const (set_name, rep_T --> bool_T) val set_t' = prop_of_Rep |> HOLogic.dest_Trueprop - |> Refute.specialize_type thy (dest_Const rep_t) + |> specialize_type thy (dest_Const rep_t) |> HOLogic.dest_mem |> snd in [HOLogic.all_const abs_T diff -r 2673979cb54d -r 8ff45c2076da src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Apr 29 01:11:06 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Apr 29 01:17:14 2010 +0200 @@ -914,8 +914,8 @@ val class = Logic.class_of_const s val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]), class) - val ax1 = try (Refute.specialize_type thy x) of_class - val ax2 = Option.map (Refute.specialize_type thy x o snd) + val ax1 = try (specialize_type thy x) of_class + val ax2 = Option.map (specialize_type thy x o snd) (Refute.get_classdef thy class) in fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2]) @@ -997,7 +997,7 @@ map (fn t => case Term.add_tvars t [] of [] => t | [(x, S)] => - Refute.monomorphic_term (Vartab.make [(x, (S, T))]) t + monomorphic_term (Vartab.make [(x, (S, T))]) t | _ => raise TERM ("Nitpick_Preproc.axioms_for_term.\ \add_axioms_for_sort", [t])) class_axioms diff -r 2673979cb54d -r 8ff45c2076da src/HOL/Tools/Nitpick/nitpick_util.ML --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Thu Apr 29 01:11:06 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Thu Apr 29 01:17:14 2010 +0200 @@ -57,6 +57,8 @@ val bool_T : typ val nat_T : typ val int_T : typ + val monomorphic_term : Type.tyenv -> term -> term + val specialize_type : theory -> (string * typ) -> term -> term val nat_subscript : int -> string val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b val DETERM_TIMEOUT : Time.time option -> tactic -> tactic @@ -227,6 +229,9 @@ val nat_T = @{typ nat} val int_T = @{typ int} +val monomorphic_term = Sledgehammer_Util.monomorphic_term +val specialize_type = Sledgehammer_Util.specialize_type + val subscript = implode o map (prefix "\<^isub>") o explode fun nat_subscript n = (* cheap trick to ensure proper alphanumeric ordering for one- and two-digit diff -r 2673979cb54d -r 8ff45c2076da src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Apr 29 01:11:06 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Apr 29 01:17:14 2010 +0200 @@ -392,6 +392,21 @@ fold forall_of (Term.add_consts t [] |> filter (is_skolem_const_name o fst) |> map Const) t +val combinator_table = + [(@{const_name COMBI}, @{thm COMBI_def_raw}), + (@{const_name COMBK}, @{thm COMBK_def_raw}), + (@{const_name COMBB}, @{thm COMBB_def_raw}), + (@{const_name COMBC}, @{thm COMBC_def_raw}), + (@{const_name COMBS}, @{thm COMBS_def_raw})] + +fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2)) + | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t') + | uncombine_term (t as Const (x as (s, _))) = + (case AList.lookup (op =) combinator_table s of + SOME thm => thm |> prop_of |> specialize_type @{theory} x |> Logic.dest_equals |> snd + | NONE => t) + | uncombine_term t = t + (* Interpret a list of syntax trees as a clause, given by "real" literals and sort constraints. "vt" holds the initial sort constraints, from the conjecture clauses. *) @@ -435,15 +450,16 @@ val t2 = clause_of_nodes ctxt vt us val (t1, t2) = HOLogic.eq_const HOLogic.typeT $ t1 $ t2 - |> unvarify_args |> check_clause ctxt |> HOLogic.dest_eq + |> unvarify_args |> uncombine_term |> check_clause ctxt + |> HOLogic.dest_eq in (Definition (num, t1, t2), fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt) end | decode_line vt (Inference (num, us, deps)) ctxt = let - val t = us |> clause_of_nodes ctxt vt |> unskolemize_term - |> check_clause ctxt + val t = us |> clause_of_nodes ctxt vt + |> unskolemize_term |> uncombine_term |> check_clause ctxt in (Inference (num, t, deps), fold Variable.declare_term (OldTerm.term_frees t) ctxt) diff -r 2673979cb54d -r 8ff45c2076da src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Apr 29 01:11:06 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Apr 29 01:17:14 2010 +0200 @@ -18,6 +18,8 @@ val nat_subscript : int -> string val unyxml : string -> string val maybe_quote : string -> string + val monomorphic_term : Type.tyenv -> term -> term + val specialize_type : theory -> (string * typ) -> term -> term end; structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = @@ -103,4 +105,30 @@ OuterKeyword.is_keyword s) ? quote end +fun monomorphic_term subst t = + map_types (map_type_tvar (fn v => + case Type.lookup subst v of + SOME typ => typ + | NONE => raise TERM ("monomorphic_term: uninstanitated schematic type \ + \variable", [t]))) t + +fun specialize_type thy (s, T) t = + let + fun subst_for (Const (s', T')) = + if s = s' then + SOME (Sign.typ_match thy (T', T) Vartab.empty) + handle Type.TYPE_MATCH => NONE + else + NONE + | subst_for (t1 $ t2) = + (case subst_for t1 of SOME x => SOME x | NONE => subst_for t2) + | subst_for (Abs (_, _, t')) = subst_for t' + | subst_for _ = NONE + in + case subst_for t of + SOME subst => monomorphic_term subst t + | NONE => raise Type.TYPE_MATCH + end + + end; diff -r 2673979cb54d -r 8ff45c2076da src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Thu Apr 29 01:11:06 2010 +0200 +++ b/src/HOL/Tools/refute.ML Thu Apr 29 01:17:14 2010 +0200 @@ -70,8 +70,6 @@ val is_IDT_constructor : theory -> string * typ -> bool val is_IDT_recursor : theory -> string * typ -> bool val is_const_of_class: theory -> string * typ -> bool - val monomorphic_term : Type.tyenv -> term -> term - val specialize_type : theory -> (string * typ) -> term -> term val string_of_typ : typ -> string val typ_of_dtyp : Datatype.descr -> (Datatype.dtyp * typ) list -> Datatype.dtyp -> typ end; (* signature REFUTE *) @@ -449,57 +447,8 @@ Term.all T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t end; -(* ------------------------------------------------------------------------- *) -(* monomorphic_term: applies a type substitution 'typeSubs' for all type *) -(* variables in a term 't' *) -(* ------------------------------------------------------------------------- *) - - (* Type.tyenv -> Term.term -> Term.term *) - - fun monomorphic_term typeSubs t = - map_types (map_type_tvar - (fn v => - case Type.lookup typeSubs v of - NONE => - (* schematic type variable not instantiated *) - raise REFUTE ("monomorphic_term", - "no substitution for type variable " ^ fst (fst v) ^ - " in term " ^ Syntax.string_of_term_global Pure.thy t) - | SOME typ => - typ)) t; - -(* ------------------------------------------------------------------------- *) -(* specialize_type: given a constant 's' of type 'T', which is a subterm of *) -(* 't', where 't' has a (possibly) more general type, the *) -(* schematic type variables in 't' are instantiated to *) -(* match the type 'T' (may raise Type.TYPE_MATCH) *) -(* ------------------------------------------------------------------------- *) - - (* theory -> (string * Term.typ) -> Term.term -> Term.term *) - - fun specialize_type thy (s, T) t = - let - fun find_typeSubs (Const (s', T')) = - if s=s' then - SOME (Sign.typ_match thy (T', T) Vartab.empty) - handle Type.TYPE_MATCH => NONE - else - NONE - | find_typeSubs (Free _) = NONE - | find_typeSubs (Var _) = NONE - | find_typeSubs (Bound _) = NONE - | find_typeSubs (Abs (_, _, body)) = find_typeSubs body - | find_typeSubs (t1 $ t2) = - (case find_typeSubs t1 of SOME x => SOME x - | NONE => find_typeSubs t2) - in - case find_typeSubs t of - SOME typeSubs => - monomorphic_term typeSubs t - | NONE => - (* no match found - perhaps due to sort constraints *) - raise Type.TYPE_MATCH - end; +val monomorphic_term = Sledgehammer_Util.monomorphic_term +val specialize_type = Sledgehammer_Util.specialize_type (* ------------------------------------------------------------------------- *) (* is_const_of_class: returns 'true' iff 'Const (s, T)' is a constant that *)