prevent schematic variable clash in combinator-introduction code, when invoked from Sledgehammer (another consequence of the CNF -> FOF transition)
1.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon Jul 26 22:35:25 2010 +0200
1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon Jul 26 23:54:40 2010 +0200
1.3 @@ -187,8 +187,9 @@
1.4 subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
1.5 (0 upto length Ts - 1 ~~ Ts))
1.6
1.7 -fun introduce_combinators_in_term thy t =
1.8 +fun introduce_combinators_in_term ctxt kind t =
1.9 let
1.10 + val thy = ProofContext.theory_of ctxt
1.11 fun aux Ts t =
1.12 case t of
1.13 @{const Not} $ t1 => @{const Not} $ aux Ts t1
1.14 @@ -205,37 +206,44 @@
1.15 | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
1.16 t
1.17 else
1.18 - t |> conceal_bounds Ts
1.19 - |> Envir.eta_contract
1.20 - |> cterm_of thy
1.21 - |> Clausifier.introduce_combinators_in_cterm
1.22 - |> prop_of |> Logic.dest_equals |> snd
1.23 - |> reveal_bounds Ts
1.24 - handle THM (msg, _, _) =>
1.25 - (* A type variable of sort "{}" will make abstraction
1.26 - fail. *)
1.27 - t
1.28 + let
1.29 + val t = t |> conceal_bounds Ts
1.30 + |> Envir.eta_contract
1.31 + val ([t], ctxt') = Variable.import_terms true [t] ctxt
1.32 + in
1.33 + t |> cterm_of thy
1.34 + |> Clausifier.introduce_combinators_in_cterm
1.35 + |> singleton (Variable.export ctxt' ctxt)
1.36 + |> prop_of |> Logic.dest_equals |> snd
1.37 + |> reveal_bounds Ts
1.38 + end
1.39 in t |> not (Meson.is_fol_term thy t) ? aux [] end
1.40 + handle THM _ =>
1.41 + (* A type variable of sort "{}" will make abstraction fail. *)
1.42 + case kind of
1.43 + Axiom => HOLogic.true_const
1.44 + | Conjecture => HOLogic.false_const
1.45
1.46 (* making axiom and conjecture clauses *)
1.47 -fun make_clause thy (formula_name, kind, t) =
1.48 +fun make_clause ctxt (formula_name, kind, t) =
1.49 let
1.50 + val thy = ProofContext.theory_of ctxt
1.51 (* ### FIXME: perform other transformations previously done by
1.52 "Clausifier.to_nnf", e.g. "HOL.If" *)
1.53 val t = t |> transform_elim_term
1.54 |> Object_Logic.atomize_term thy
1.55 |> extensionalize_term
1.56 - |> introduce_combinators_in_term thy
1.57 + |> introduce_combinators_in_term ctxt kind
1.58 val (combformula, ctypes_sorts) = combformula_for_prop thy t []
1.59 in
1.60 FOLFormula {formula_name = formula_name, combformula = combformula,
1.61 kind = kind, ctypes_sorts = ctypes_sorts}
1.62 end
1.63
1.64 -fun make_axiom_clause thy (name, th) =
1.65 - (name, make_clause thy (name, Axiom, prop_of th))
1.66 -fun make_conjecture_clauses thy ts =
1.67 - map2 (fn j => fn t => make_clause thy (Int.toString j, Conjecture, t))
1.68 +fun make_axiom_clause ctxt (name, th) =
1.69 + (name, make_clause ctxt (name, Axiom, prop_of th))
1.70 +fun make_conjecture_clauses ctxt ts =
1.71 + map2 (fn j => fn t => make_clause ctxt (Int.toString j, Conjecture, t))
1.72 (0 upto length ts - 1) ts
1.73
1.74 (** Helper clauses **)
1.75 @@ -263,7 +271,7 @@
1.76 Symtab.make (maps (maps (map (rpair 0) o fst))
1.77 [optional_helpers, optional_typed_helpers])
1.78
1.79 -fun get_helper_clauses thy is_FO full_types conjectures axclauses =
1.80 +fun get_helper_clauses ctxt is_FO full_types conjectures axclauses =
1.81 let
1.82 val ct = fold (fold count_fol_formula) [conjectures, axclauses]
1.83 init_counters
1.84 @@ -275,31 +283,35 @@
1.85 if exists is_needed ss then map (`Thm.get_name_hint) ths
1.86 else [])) @
1.87 (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)
1.88 - in map (snd o make_axiom_clause thy) cnfs end
1.89 + in map (snd o make_axiom_clause ctxt) cnfs end
1.90
1.91 fun s_not (@{const Not} $ t) = t
1.92 | s_not t = @{const Not} $ t
1.93
1.94 (* prepare for passing to writer,
1.95 create additional clauses based on the information from extra_cls *)
1.96 -fun prepare_clauses full_types hyp_ts concl_t axcls extra_cls thy =
1.97 +fun prepare_clauses ctxt full_types hyp_ts concl_t axcls extra_cls =
1.98 let
1.99 + val thy = ProofContext.theory_of ctxt
1.100 val goal_t = Logic.list_implies (hyp_ts, concl_t)
1.101 val is_FO = Meson.is_fol_term thy goal_t
1.102 - val _ = trace_msg (fn _ => Syntax.string_of_term_global thy goal_t)
1.103 + val _ = trace_msg (fn _ => Syntax.string_of_term ctxt goal_t)
1.104 val axtms = map (prop_of o snd) extra_cls
1.105 val subs = tfree_classes_of_terms [goal_t]
1.106 val supers = tvar_classes_of_terms axtms
1.107 val tycons = type_consts_of_terms thy (goal_t :: axtms)
1.108 (* TFrees in conjecture clauses; TVars in axiom clauses *)
1.109 - val conjectures = make_conjecture_clauses thy (map s_not hyp_ts @ [concl_t])
1.110 - val extra_clauses = map (snd o make_axiom_clause thy) extra_cls
1.111 + val conjectures =
1.112 + map (s_not o HOLogic.dest_Trueprop) hyp_ts @
1.113 + [HOLogic.dest_Trueprop concl_t]
1.114 + |> make_conjecture_clauses ctxt
1.115 + val extra_clauses = map (snd o make_axiom_clause ctxt) extra_cls
1.116 val (clnames, axiom_clauses) =
1.117 - ListPair.unzip (map (make_axiom_clause thy) axcls)
1.118 + ListPair.unzip (map (make_axiom_clause ctxt) axcls)
1.119 (* FIXME: Should it read "extra_clauses" or "axiom_clauses" in the
1.120 "get_helper_clauses" call? *)
1.121 val helper_clauses =
1.122 - get_helper_clauses thy is_FO full_types conjectures extra_clauses
1.123 + get_helper_clauses ctxt is_FO full_types conjectures extra_clauses
1.124 val (supers', arity_clauses) = make_arity_clauses thy tycons supers
1.125 val class_rel_clauses = make_class_rel_clauses thy subs supers'
1.126 in
1.127 @@ -367,7 +379,7 @@
1.128 let
1.129 (* get clauses and prepare them for writing *)
1.130 val (ctxt, (_, th)) = goal;
1.131 - val thy = ProofContext.theory_of ctxt;
1.132 + val thy = ProofContext.theory_of ctxt
1.133 (* ### FIXME: (1) preprocessing for "if" etc. *)
1.134 val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
1.135 val the_filtered_clauses =
1.136 @@ -379,8 +391,8 @@
1.137 relevance_override goal hyp_ts concl_t
1.138 val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses
1.139 val (internal_thm_names, clauses) =
1.140 - prepare_clauses full_types hyp_ts concl_t the_axiom_clauses
1.141 - the_filtered_clauses thy
1.142 + prepare_clauses ctxt full_types hyp_ts concl_t the_axiom_clauses
1.143 + the_filtered_clauses
1.144
1.145 (* path to unique problem file *)
1.146 val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
2.1 --- a/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Jul 26 22:35:25 2010 +0200
2.2 +++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Jul 26 23:54:40 2010 +0200
2.3 @@ -109,8 +109,11 @@
2.4 val thy = theory_of_cterm ct
2.5 val Abs(x,_,body) = term_of ct
2.6 val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct)
2.7 - val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT
2.8 - fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K}
2.9 + val cxT = ctyp_of thy xT
2.10 + val cbodyT = ctyp_of thy bodyT
2.11 + fun makeK () =
2.12 + instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)]
2.13 + @{thm abs_K}
2.14 in
2.15 case body of
2.16 Const _ => makeK()
3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Mon Jul 26 22:35:25 2010 +0200
3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Mon Jul 26 23:54:40 2010 +0200
3.3 @@ -77,6 +77,8 @@
3.4 fun string_for_formula (AQuant (q, xs, phi)) =
3.5 string_for_quantifier q ^ "[" ^ commas xs ^ "]: " ^
3.6 string_for_formula phi
3.7 + | string_for_formula (AConn (ANot, [APred (ATerm ("equal", ts))])) =
3.8 + space_implode " != " (map string_for_term ts)
3.9 | string_for_formula (AConn (c, [phi])) =
3.10 string_for_connective c ^ " " ^ string_for_formula phi
3.11 | string_for_formula (AConn (c, phis)) =