use 'prop' rather than 'bool' systematically in Isar reconstruction code
authorblanchet
Sun Dec 15 19:01:06 2013 +0100 (2013-12-15)
changeset 547574960647932ec
parent 54756 dd0f4d265730
child 54758 ba488d89614a
use 'prop' rather than 'bool' systematically in Isar reconstruction code
src/HOL/Library/refute.ML
src/HOL/Tools/ATP/atp_problem_generate.ML
src/HOL/Tools/ATP/atp_proof_reconstruct.ML
src/HOL/Tools/ATP/atp_util.ML
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
     1.1 --- a/src/HOL/Library/refute.ML	Sun Dec 15 18:54:26 2013 +0100
     1.2 +++ b/src/HOL/Library/refute.ML	Sun Dec 15 19:01:06 2013 +0100
     1.3 @@ -393,21 +393,7 @@
     1.4  (* ------------------------------------------------------------------------- *)
     1.5  
     1.6  val typ_of_dtyp = Nitpick_Util.typ_of_dtyp
     1.7 -
     1.8 -(* ------------------------------------------------------------------------- *)
     1.9 -(* close_form: universal closure over schematic variables in 't'             *)
    1.10 -(* ------------------------------------------------------------------------- *)
    1.11 -
    1.12 -(* Term.term -> Term.term *)
    1.13 -
    1.14 -fun close_form t =
    1.15 -  let
    1.16 -    val vars = sort_wrt (fst o fst) (Term.add_vars t [])
    1.17 -  in
    1.18 -    fold (fn ((x, i), T) => fn t' =>
    1.19 -      Logic.all_const T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t
    1.20 -  end;
    1.21 -
    1.22 +val close_form = ATP_Util.close_form
    1.23  val monomorphic_term = ATP_Util.monomorphic_term
    1.24  val specialize_type = ATP_Util.specialize_type
    1.25  
     2.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Sun Dec 15 18:54:26 2013 +0100
     2.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Sun Dec 15 19:01:06 2013 +0100
     2.3 @@ -1332,10 +1332,6 @@
     2.4      | formula => SOME formula
     2.5    end
     2.6  
     2.7 -fun s_not_prop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
     2.8 -  | s_not_prop (@{const "==>"} $ t $ @{prop False}) = t
     2.9 -  | s_not_prop t = @{const "==>"} $ t $ @{prop False}
    2.10 -
    2.11  fun make_conjecture ctxt format type_enc =
    2.12    map (fn ((name, stature), (role, t)) =>
    2.13            let
     3.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sun Dec 15 18:54:26 2013 +0100
     3.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sun Dec 15 19:01:06 2013 +0100
     3.3 @@ -504,6 +504,7 @@
     3.4        |> uncombine_term thy
     3.5        |> unlift_term lifted
     3.6        |> infer_formula_types ctxt
     3.7 +      |> HOLogic.mk_Trueprop
     3.8    in
     3.9      (name, role, t, rule, deps)
    3.10    end
     4.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Sun Dec 15 18:54:26 2013 +0100
     4.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Sun Dec 15 19:01:06 2013 +0100
     4.3 @@ -36,6 +36,7 @@
     4.4    val s_disj : term * term -> term
     4.5    val s_imp : term * term -> term
     4.6    val s_iff : term * term -> term
     4.7 +  val s_not_prop : term -> term
     4.8    val close_form : term -> term
     4.9    val hol_close_form_prefix : string
    4.10    val hol_close_form : term -> term
    4.11 @@ -292,22 +293,27 @@
    4.12    | s_disj (@{const True}, _) = @{const True}
    4.13    | s_disj (_, @{const True}) = @{const True}
    4.14    | s_disj (t1, t2) = if t1 aconv t2 then t1 else HOLogic.mk_disj (t1, t2)
    4.15 +
    4.16  fun s_imp (@{const True}, t2) = t2
    4.17    | s_imp (t1, @{const False}) = s_not t1
    4.18    | s_imp (@{const False}, _) = @{const True}
    4.19    | s_imp (_, @{const True}) = @{const True}
    4.20    | s_imp p = HOLogic.mk_imp p
    4.21 +
    4.22  fun s_iff (@{const True}, t2) = t2
    4.23    | s_iff (t1, @{const True}) = t1
    4.24    | s_iff (@{const False}, t2) = s_not t2
    4.25    | s_iff (t1, @{const False}) = s_not t1
    4.26    | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
    4.27  
    4.28 -(* cf. "close_form" in "refute.ML" *)
    4.29 +fun s_not_prop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
    4.30 +  | s_not_prop (@{const "==>"} $ t $ @{prop False}) = t
    4.31 +  | s_not_prop t = @{const "==>"} $ t $ @{prop False}
    4.32 +
    4.33  fun close_form t =
    4.34    fold (fn ((s, i), T) => fn t' =>
    4.35 -           Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t')))
    4.36 -       (Term.add_vars t []) t
    4.37 +      Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t')))
    4.38 +    (Term.add_vars t []) t
    4.39  
    4.40  val hol_close_form_prefix = "ATP.close_form."
    4.41  
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sun Dec 15 18:54:26 2013 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sun Dec 15 19:01:06 2013 +0100
     5.3 @@ -47,9 +47,6 @@
     5.4  
     5.5  open String_Redirect
     5.6  
     5.7 -fun maybe_mk_Trueprop t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
     5.8 -val maybe_dest_Trueprop = perhaps (try HOLogic.dest_Trueprop)
     5.9 -
    5.10  val e_skolemize_rule = "skolemize"
    5.11  val vampire_skolemisation_rule = "skolemisation"
    5.12  (* TODO: Use "Z3_Proof.string_of_rule" once it is moved to Isabelle *)
    5.13 @@ -81,7 +78,7 @@
    5.14  fun inline_z3_defs _ [] = []
    5.15    | inline_z3_defs defs ((line as (name, role, t, rule, deps)) :: lines) =
    5.16      if rule = z3_intro_def_rule then
    5.17 -      let val def = t |> maybe_dest_Trueprop |> HOLogic.dest_eq |> swap in
    5.18 +      let val def = t |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> swap in
    5.19          inline_z3_defs (insert (op =) def defs)
    5.20            (map (replace_dependencies_in_line (name, [])) lines)
    5.21        end
    5.22 @@ -286,7 +283,7 @@
    5.23                  else if is_arith_rule rule then ([], ArithM)
    5.24                  else ([], AutoM)
    5.25              in
    5.26 -              Prove ([], skos, l, maybe_mk_Trueprop t, [], (([], []), meth))
    5.27 +              Prove ([], skos, l, t, [], (([], []), meth))
    5.28              end)
    5.29  
    5.30          val bot = atp_proof |> List.last |> #1
    5.31 @@ -306,7 +303,7 @@
    5.32            |> fold (fn (name as (s, _), role, t, rule, _) =>
    5.33                        Symtab.update_new (s, (rule,
    5.34                          t |> (if is_clause_tainted [name] then
    5.35 -                                role <> Conjecture ? (maybe_dest_Trueprop #> s_not)
    5.36 +                                role <> Conjecture ? s_not_prop
    5.37                                  #> fold exists_of (map Var (Term.add_vars t []))
    5.38                                else
    5.39                                  I))))
    5.40 @@ -314,14 +311,11 @@
    5.41  
    5.42          val rule_of_clause_id = fst o the o Symtab.lookup steps o fst
    5.43  
    5.44 -        (* The assumptions and conjecture are "prop"s; the other formulas are "bool"s (for ATPs) or
    5.45 -           "prop"s (for Z3). TODO: Always use "prop". *)
    5.46 -        fun prop_of_clause [(num, _)] =
    5.47 -            Symtab.lookup steps num |> the |> snd |> maybe_mk_Trueprop |> close_form
    5.48 +        fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> close_form
    5.49            | prop_of_clause names =
    5.50              let
    5.51                val lits =
    5.52 -                map (maybe_dest_Trueprop o snd) (map_filter (Symtab.lookup steps o fst) names)
    5.53 +                map (HOLogic.dest_Trueprop o snd) (map_filter (Symtab.lookup steps o fst) names)
    5.54              in
    5.55                (case List.partition (can HOLogic.dest_not) lits of
    5.56                  (negs as _ :: _, pos as _ :: _) =>