src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
changeset 36555 8ff45c2076da
parent 36551 cc42df660808
child 36556 81dc2c20f052
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Apr 29 01:11:06 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Apr 29 01:17:14 2010 +0200
     1.3 @@ -392,6 +392,21 @@
     1.4    fold forall_of (Term.add_consts t []
     1.5                   |> filter (is_skolem_const_name o fst) |> map Const) t
     1.6  
     1.7 +val combinator_table =
     1.8 +  [(@{const_name COMBI}, @{thm COMBI_def_raw}),
     1.9 +   (@{const_name COMBK}, @{thm COMBK_def_raw}),
    1.10 +   (@{const_name COMBB}, @{thm COMBB_def_raw}),
    1.11 +   (@{const_name COMBC}, @{thm COMBC_def_raw}),
    1.12 +   (@{const_name COMBS}, @{thm COMBS_def_raw})]
    1.13 +
    1.14 +fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2))
    1.15 +  | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t')
    1.16 +  | uncombine_term (t as Const (x as (s, _))) =
    1.17 +    (case AList.lookup (op =) combinator_table s of
    1.18 +       SOME thm => thm |> prop_of |> specialize_type @{theory} x |> Logic.dest_equals |> snd
    1.19 +     | NONE => t)
    1.20 +  | uncombine_term t = t
    1.21 +
    1.22  (* Interpret a list of syntax trees as a clause, given by "real" literals and
    1.23     sort constraints. "vt" holds the initial sort constraints, from the
    1.24     conjecture clauses. *)
    1.25 @@ -435,15 +450,16 @@
    1.26        val t2 = clause_of_nodes ctxt vt us
    1.27        val (t1, t2) =
    1.28          HOLogic.eq_const HOLogic.typeT $ t1 $ t2
    1.29 -        |> unvarify_args |> check_clause ctxt |> HOLogic.dest_eq
    1.30 +        |> unvarify_args |> uncombine_term |> check_clause ctxt
    1.31 +        |> HOLogic.dest_eq
    1.32      in
    1.33        (Definition (num, t1, t2),
    1.34         fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
    1.35      end
    1.36    | decode_line vt (Inference (num, us, deps)) ctxt =
    1.37      let
    1.38 -      val t = us |> clause_of_nodes ctxt vt |> unskolemize_term
    1.39 -                 |> check_clause ctxt
    1.40 +      val t = us |> clause_of_nodes ctxt vt
    1.41 +                 |> unskolemize_term |> uncombine_term |> check_clause ctxt
    1.42      in
    1.43        (Inference (num, t, deps),
    1.44         fold Variable.declare_term (OldTerm.term_frees t) ctxt)