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)
```