218 | aux (Var ((s, i), T)) = |
218 | aux (Var ((s, i), T)) = |
219 Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T) |
219 Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T) |
220 | aux t = t |
220 | aux t = t |
221 in t |> exists_subterm is_Var t ? aux end |
221 in t |> exists_subterm is_Var t ? aux end |
222 |
222 |
223 (* "Object_Logic.atomize_term" isn't as powerful as it could be; for example, |
|
224 it leaves metaequalities over "prop"s alone. *) |
|
225 val atomize_term = |
|
226 let |
|
227 fun aux (@{const Trueprop} $ t1) = t1 |
|
228 | aux (Const (@{const_name all}, _) $ Abs (s, T, t')) = |
|
229 HOLogic.all_const T $ Abs (s, T, aux t') |
|
230 | aux (@{const "==>"} $ t1 $ t2) = HOLogic.mk_imp (pairself aux (t1, t2)) |
|
231 | aux (Const (@{const_name "=="}, Type (_, [@{typ prop}, _])) $ t1 $ t2) = |
|
232 HOLogic.eq_const HOLogic.boolT $ aux t1 $ aux t2 |
|
233 | aux (Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2) = |
|
234 HOLogic.eq_const T $ t1 $ t2 |
|
235 | aux _ = raise Fail "aux" |
|
236 in perhaps (try aux) end |
|
237 |
|
238 (* making fact and conjecture formulas *) |
223 (* making fact and conjecture formulas *) |
239 fun make_formula ctxt eq_as_iff presimp name kind t = |
224 fun make_formula ctxt eq_as_iff presimp name kind t = |
240 let |
225 let |
241 val thy = ProofContext.theory_of ctxt |
226 val thy = ProofContext.theory_of ctxt |
242 val t = t |> Envir.beta_eta_contract |
227 val t = t |> Envir.beta_eta_contract |