src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
changeset 42449 494e4ac5b0f8
parent 42361 23f352990944
child 42451 a75fcd103cbb
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Thu Apr 21 21:14:06 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Thu Apr 21 22:18:28 2011 +0200
     1.3 @@ -8,11 +8,12 @@
     1.4  
     1.5  signature SLEDGEHAMMER_ATP_RECONSTRUCT =
     1.6  sig
     1.7 +  type 'a proof = 'a ATP_Proof.proof
     1.8    type locality = Sledgehammer_Filter.locality
     1.9    type type_system = Sledgehammer_ATP_Translate.type_system
    1.10    type minimize_command = string list -> string
    1.11    type metis_params =
    1.12 -    string * type_system * minimize_command * string
    1.13 +    string * type_system * minimize_command * string proof
    1.14      * (string * locality) list vector * thm * int
    1.15    type isar_params =
    1.16      string Symtab.table * bool * int * Proof.context * int list list
    1.17 @@ -21,6 +22,8 @@
    1.18    val repair_conjecture_shape_and_fact_names :
    1.19      string -> int list list -> (string * locality) list vector
    1.20      -> int list list * (string * locality) list vector
    1.21 +  val is_unsound_proof :
    1.22 +    int list list -> (string * locality) list vector -> string proof -> bool
    1.23    val apply_on_subgoal : string -> int -> int -> string
    1.24    val command_call : string -> string list -> string
    1.25    val try_command_line : string -> string -> string
    1.26 @@ -45,7 +48,7 @@
    1.27  
    1.28  type minimize_command = string list -> string
    1.29  type metis_params =
    1.30 -  string * type_system * minimize_command * string
    1.31 +  string * type_system * minimize_command * string proof
    1.32    * (string * locality) list vector * thm * int
    1.33  type isar_params =
    1.34    string Symtab.table * bool * int * Proof.context * int list list
    1.35 @@ -115,39 +118,6 @@
    1.36    else
    1.37      (conjecture_shape, fact_names)
    1.38  
    1.39 -
    1.40 -(** Soft-core proof reconstruction: Metis one-liner **)
    1.41 -
    1.42 -fun string_for_label (s, num) = s ^ string_of_int num
    1.43 -
    1.44 -fun set_settings "" = ""
    1.45 -  | set_settings settings = "using [[" ^ settings ^ "]] "
    1.46 -fun apply_on_subgoal settings _ 1 = set_settings settings ^ "by "
    1.47 -  | apply_on_subgoal settings 1 _ = set_settings settings ^ "apply "
    1.48 -  | apply_on_subgoal settings i n =
    1.49 -    "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal settings 1 n
    1.50 -fun command_call name [] = name
    1.51 -  | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
    1.52 -fun try_command_line banner command =
    1.53 -  banner ^ ": " ^ Markup.markup Markup.sendback command ^ "."
    1.54 -fun using_labels [] = ""
    1.55 -  | using_labels ls =
    1.56 -    "using " ^ space_implode " " (map string_for_label ls) ^ " "
    1.57 -fun metis_name type_sys =
    1.58 -  if types_dangerous_types type_sys then "metisFT" else "metis"
    1.59 -fun metis_call type_sys ss = command_call (metis_name type_sys) ss
    1.60 -fun metis_command type_sys i n (ls, ss) =
    1.61 -  using_labels ls ^ apply_on_subgoal "" i n ^ metis_call type_sys ss
    1.62 -fun metis_line banner type_sys i n ss =
    1.63 -  try_command_line banner (metis_command type_sys i n ([], ss))
    1.64 -fun minimize_line _ [] = ""
    1.65 -  | minimize_line minimize_command ss =
    1.66 -    case minimize_command ss of
    1.67 -      "" => ""
    1.68 -    | command =>
    1.69 -      "\nTo minimize the number of lemmas, try this: " ^
    1.70 -      Markup.markup Markup.sendback command ^ "."
    1.71 -
    1.72  val vampire_step_prefix = "f" (* grrr... *)
    1.73  
    1.74  fun resolve_fact fact_names ((_, SOME s)) =
    1.75 @@ -168,27 +138,77 @@
    1.76          []
    1.77      | NONE => []
    1.78  
    1.79 +fun resolve_conjecture conjecture_shape (num, s_opt) =
    1.80 +  let
    1.81 +    val k = case try (unprefix conjecture_prefix) (the_default "" s_opt) of
    1.82 +              SOME s => Int.fromString s |> the_default ~1
    1.83 +            | NONE => case Int.fromString num of
    1.84 +                        SOME j => find_index (exists (curry (op =) j))
    1.85 +                                             conjecture_shape
    1.86 +                      | NONE => ~1
    1.87 +  in if k >= 0 then [k] else [] end
    1.88 +
    1.89 +fun is_fact conjecture_shape = not o null o resolve_fact conjecture_shape
    1.90 +fun is_conjecture conjecture_shape =
    1.91 +  not o null o resolve_conjecture conjecture_shape
    1.92 +
    1.93  fun add_fact fact_names (Inference (name, _, [])) =
    1.94      append (resolve_fact fact_names name)
    1.95    | add_fact _ _ = I
    1.96  
    1.97 -fun used_facts_in_tstplike_proof fact_names tstplike_proof =
    1.98 -  if tstplike_proof = "" then
    1.99 -    Vector.foldl (op @) [] fact_names
   1.100 -  else
   1.101 -    tstplike_proof
   1.102 -    |> atp_proof_from_tstplike_string false
   1.103 -    |> rpair [] |-> fold (add_fact fact_names)
   1.104 +fun used_facts_in_atp_proof fact_names atp_proof =
   1.105 +  if null atp_proof then Vector.foldl (op @) [] fact_names
   1.106 +  else fold (add_fact fact_names) atp_proof []
   1.107 +
   1.108 +fun is_conjecture_referred_to_in_proof conjecture_shape =
   1.109 +  exists (fn Inference (name, _, []) => is_conjecture conjecture_shape name
   1.110 +           | _ => false)
   1.111 +
   1.112 +fun is_unsound_proof conjecture_shape fact_names =
   1.113 +  (not o is_conjecture_referred_to_in_proof conjecture_shape) andf
   1.114 +  forall (is_global_locality o snd) o used_facts_in_atp_proof fact_names
   1.115 +
   1.116 +(** Soft-core proof reconstruction: Metis one-liner **)
   1.117 +
   1.118 +fun string_for_label (s, num) = s ^ string_of_int num
   1.119 +
   1.120 +fun set_settings "" = ""
   1.121 +  | set_settings settings = "using [[" ^ settings ^ "]] "
   1.122 +fun apply_on_subgoal settings _ 1 = set_settings settings ^ "by "
   1.123 +  | apply_on_subgoal settings 1 _ = set_settings settings ^ "apply "
   1.124 +  | apply_on_subgoal settings i n =
   1.125 +    "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal settings 1 n
   1.126 +fun command_call name [] = name
   1.127 +  | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
   1.128 +fun try_command_line banner command =
   1.129 +  banner ^ ": " ^ Markup.markup Markup.sendback command ^ "."
   1.130 +fun using_labels [] = ""
   1.131 +  | using_labels ls =
   1.132 +    "using " ^ space_implode " " (map string_for_label ls) ^ " "
   1.133 +fun metis_name type_sys =
   1.134 +  if type_system_types_dangerous_types type_sys then "metisFT" else "metis"
   1.135 +fun metis_call type_sys ss = command_call (metis_name type_sys) ss
   1.136 +fun metis_command type_sys i n (ls, ss) =
   1.137 +  using_labels ls ^ apply_on_subgoal "" i n ^ metis_call type_sys ss
   1.138 +fun metis_line banner type_sys i n ss =
   1.139 +  try_command_line banner (metis_command type_sys i n ([], ss))
   1.140 +fun minimize_line _ [] = ""
   1.141 +  | minimize_line minimize_command ss =
   1.142 +    case minimize_command ss of
   1.143 +      "" => ""
   1.144 +    | command =>
   1.145 +      "\nTo minimize the number of lemmas, try this: " ^
   1.146 +      Markup.markup Markup.sendback command ^ "."
   1.147  
   1.148  val split_used_facts =
   1.149    List.partition (curry (op =) Chained o snd)
   1.150    #> pairself (sort_distinct (string_ord o pairself fst))
   1.151  
   1.152 -fun metis_proof_text (banner, type_sys, minimize_command, tstplike_proof,
   1.153 -                      fact_names, goal, i) =
   1.154 +fun metis_proof_text (banner, type_sys, minimize_command, atp_proof, fact_names,
   1.155 +                      goal, i) =
   1.156    let
   1.157      val (chained_lemmas, other_lemmas) =
   1.158 -      split_used_facts (used_facts_in_tstplike_proof fact_names tstplike_proof)
   1.159 +      split_used_facts (used_facts_in_atp_proof fact_names atp_proof)
   1.160      val n = Logic.count_prems (prop_of goal)
   1.161    in
   1.162      (metis_line banner type_sys i n (map fst other_lemmas) ^
   1.163 @@ -196,7 +216,6 @@
   1.164       other_lemmas @ chained_lemmas)
   1.165    end
   1.166  
   1.167 -
   1.168  (** Hard-core proof reconstruction: structured Isar proofs **)
   1.169  
   1.170  (* Simple simplifications to ensure that sort annotations don't leave a trail of
   1.171 @@ -241,19 +260,6 @@
   1.172  val assum_prefix = "A"
   1.173  val have_prefix = "F"
   1.174  
   1.175 -fun resolve_conjecture conjecture_shape (num, s_opt) =
   1.176 -  let
   1.177 -    val k = case try (unprefix conjecture_prefix) (the_default "" s_opt) of
   1.178 -              SOME s => Int.fromString s |> the_default ~1
   1.179 -            | NONE => case Int.fromString num of
   1.180 -                        SOME j => find_index (exists (curry (op =) j))
   1.181 -                                             conjecture_shape
   1.182 -                      | NONE => ~1
   1.183 -  in if k >= 0 then [k] else [] end
   1.184 -
   1.185 -fun is_fact conjecture_shape = not o null o resolve_fact conjecture_shape
   1.186 -fun is_conjecture conjecture_shape = not o null o resolve_conjecture conjecture_shape
   1.187 -
   1.188  fun raw_label_for_name conjecture_shape name =
   1.189    case resolve_conjecture conjecture_shape name of
   1.190      [j] => (conjecture_prefix, j)
   1.191 @@ -621,12 +627,11 @@
   1.192      else
   1.193        s
   1.194  
   1.195 -fun isar_proof_from_tstplike_proof pool ctxt type_sys tfrees isar_shrink_factor
   1.196 -        tstplike_proof conjecture_shape fact_names params frees =
   1.197 +fun isar_proof_from_atp_proof pool ctxt type_sys tfrees isar_shrink_factor
   1.198 +        atp_proof conjecture_shape fact_names params frees =
   1.199    let
   1.200      val lines =
   1.201 -      tstplike_proof
   1.202 -      |> atp_proof_from_tstplike_string true
   1.203 +      atp_proof
   1.204        |> nasty_atp_proof pool
   1.205        |> map_term_names_in_atp_proof repair_name
   1.206        |> decode_lines ctxt type_sys tfrees
   1.207 @@ -929,8 +934,7 @@
   1.208    in do_proof end
   1.209  
   1.210  fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   1.211 -                    (metis_params as (_, type_sys, _, tstplike_proof,
   1.212 -                                      fact_names, goal, i)) =
   1.213 +        (metis_params as (_, type_sys, _, atp_proof, fact_names, goal, i)) =
   1.214    let
   1.215      val (params, hyp_ts, concl_t) = strip_subgoal goal i
   1.216      val frees = fold Term.add_frees (concl_t :: hyp_ts) []
   1.217 @@ -938,9 +942,9 @@
   1.218      val n = Logic.count_prems (prop_of goal)
   1.219      val (one_line_proof, lemma_names) = metis_proof_text metis_params
   1.220      fun isar_proof_for () =
   1.221 -      case isar_proof_from_tstplike_proof pool ctxt type_sys tfrees
   1.222 -               isar_shrink_factor tstplike_proof conjecture_shape fact_names
   1.223 -               params frees
   1.224 +      case isar_proof_from_atp_proof pool ctxt type_sys tfrees
   1.225 +               isar_shrink_factor atp_proof conjecture_shape fact_names params
   1.226 +               frees
   1.227             |> redirect_proof hyp_ts concl_t
   1.228             |> kill_duplicate_assumptions_in_proof
   1.229             |> then_chain_proof