# HG changeset patch # User blanchet # Date 1387130466 -3600 # Node ID 4960647932ece34cafadfdd8481450b464b6b3e0 # Parent dd0f4d265730d1766f199c274bf90cd62b3a175d use 'prop' rather than 'bool' systematically in Isar reconstruction code diff -r dd0f4d265730 -r 4960647932ec src/HOL/Library/refute.ML --- a/src/HOL/Library/refute.ML Sun Dec 15 18:54:26 2013 +0100 +++ b/src/HOL/Library/refute.ML Sun Dec 15 19:01:06 2013 +0100 @@ -393,21 +393,7 @@ (* ------------------------------------------------------------------------- *) val typ_of_dtyp = Nitpick_Util.typ_of_dtyp - -(* ------------------------------------------------------------------------- *) -(* close_form: universal closure over schematic variables in 't' *) -(* ------------------------------------------------------------------------- *) - -(* Term.term -> Term.term *) - -fun close_form t = - let - val vars = sort_wrt (fst o fst) (Term.add_vars t []) - in - fold (fn ((x, i), T) => fn t' => - Logic.all_const T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t - end; - +val close_form = ATP_Util.close_form val monomorphic_term = ATP_Util.monomorphic_term val specialize_type = ATP_Util.specialize_type diff -r dd0f4d265730 -r 4960647932ec src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Sun Dec 15 18:54:26 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Sun Dec 15 19:01:06 2013 +0100 @@ -1332,10 +1332,6 @@ | formula => SOME formula end -fun s_not_prop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t - | s_not_prop (@{const "==>"} $ t $ @{prop False}) = t - | s_not_prop t = @{const "==>"} $ t $ @{prop False} - fun make_conjecture ctxt format type_enc = map (fn ((name, stature), (role, t)) => let diff -r dd0f4d265730 -r 4960647932ec src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sun Dec 15 18:54:26 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sun Dec 15 19:01:06 2013 +0100 @@ -504,6 +504,7 @@ |> uncombine_term thy |> unlift_term lifted |> infer_formula_types ctxt + |> HOLogic.mk_Trueprop in (name, role, t, rule, deps) end diff -r dd0f4d265730 -r 4960647932ec src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML Sun Dec 15 18:54:26 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_util.ML Sun Dec 15 19:01:06 2013 +0100 @@ -36,6 +36,7 @@ val s_disj : term * term -> term val s_imp : term * term -> term val s_iff : term * term -> term + val s_not_prop : term -> term val close_form : term -> term val hol_close_form_prefix : string val hol_close_form : term -> term @@ -292,22 +293,27 @@ | s_disj (@{const True}, _) = @{const True} | s_disj (_, @{const True}) = @{const True} | s_disj (t1, t2) = if t1 aconv t2 then t1 else HOLogic.mk_disj (t1, t2) + fun s_imp (@{const True}, t2) = t2 | s_imp (t1, @{const False}) = s_not t1 | s_imp (@{const False}, _) = @{const True} | s_imp (_, @{const True}) = @{const True} | s_imp p = HOLogic.mk_imp p + fun s_iff (@{const True}, t2) = t2 | s_iff (t1, @{const True}) = t1 | s_iff (@{const False}, t2) = s_not t2 | s_iff (t1, @{const False}) = s_not t1 | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2 -(* cf. "close_form" in "refute.ML" *) +fun s_not_prop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t + | s_not_prop (@{const "==>"} $ t $ @{prop False}) = t + | s_not_prop t = @{const "==>"} $ t $ @{prop False} + fun close_form t = fold (fn ((s, i), T) => fn t' => - Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t'))) - (Term.add_vars t []) t + Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t'))) + (Term.add_vars t []) t val hol_close_form_prefix = "ATP.close_form." diff -r dd0f4d265730 -r 4960647932ec src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sun Dec 15 18:54:26 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sun Dec 15 19:01:06 2013 +0100 @@ -47,9 +47,6 @@ open String_Redirect -fun maybe_mk_Trueprop t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop -val maybe_dest_Trueprop = perhaps (try HOLogic.dest_Trueprop) - val e_skolemize_rule = "skolemize" val vampire_skolemisation_rule = "skolemisation" (* TODO: Use "Z3_Proof.string_of_rule" once it is moved to Isabelle *) @@ -81,7 +78,7 @@ fun inline_z3_defs _ [] = [] | inline_z3_defs defs ((line as (name, role, t, rule, deps)) :: lines) = if rule = z3_intro_def_rule then - let val def = t |> maybe_dest_Trueprop |> HOLogic.dest_eq |> swap in + let val def = t |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> swap in inline_z3_defs (insert (op =) def defs) (map (replace_dependencies_in_line (name, [])) lines) end @@ -286,7 +283,7 @@ else if is_arith_rule rule then ([], ArithM) else ([], AutoM) in - Prove ([], skos, l, maybe_mk_Trueprop t, [], (([], []), meth)) + Prove ([], skos, l, t, [], (([], []), meth)) end) val bot = atp_proof |> List.last |> #1 @@ -306,7 +303,7 @@ |> fold (fn (name as (s, _), role, t, rule, _) => Symtab.update_new (s, (rule, t |> (if is_clause_tainted [name] then - role <> Conjecture ? (maybe_dest_Trueprop #> s_not) + role <> Conjecture ? s_not_prop #> fold exists_of (map Var (Term.add_vars t [])) else I)))) @@ -314,14 +311,11 @@ val rule_of_clause_id = fst o the o Symtab.lookup steps o fst - (* The assumptions and conjecture are "prop"s; the other formulas are "bool"s (for ATPs) or - "prop"s (for Z3). TODO: Always use "prop". *) - fun prop_of_clause [(num, _)] = - Symtab.lookup steps num |> the |> snd |> maybe_mk_Trueprop |> close_form + fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> close_form | prop_of_clause names = let val lits = - map (maybe_dest_Trueprop o snd) (map_filter (Symtab.lookup steps o fst) names) + map (HOLogic.dest_Trueprop o snd) (map_filter (Symtab.lookup steps o fst) names) in (case List.partition (can HOLogic.dest_not) lits of (negs as _ :: _, pos as _ :: _) =>