1.1 --- a/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Dec 14 23:08:03 2011 +0100
1.2 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Dec 14 23:08:03 2011 +0100
1.3 @@ -669,9 +669,6 @@
1.4
1.5 (** Isar proof construction and manipulation **)
1.6
1.7 -fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
1.8 - (union (op =) ls1 ls2, union (op =) ss1 ss2)
1.9 -
1.10 type label = string * int
1.11 type facts = label list * string list
1.12
1.13 @@ -686,23 +683,12 @@
1.14 By_Metis of facts |
1.15 Case_Split of isar_step list list * facts
1.16
1.17 -fun smart_case_split [] facts = By_Metis facts
1.18 - | smart_case_split proofs facts = Case_Split (proofs, facts)
1.19 -
1.20 fun add_fact_from_dependency fact_names (name as (_, ss)) =
1.21 if is_fact fact_names ss then
1.22 apsnd (union (op =) (map fst (resolve_fact fact_names ss)))
1.23 else
1.24 apfst (insert (op =) (raw_label_for_name name))
1.25
1.26 -fun step_for_line _ _ (Definition (_, t1, t2)) = Let (t1, t2)
1.27 - | step_for_line _ _ (Inference (name, t, _, [])) =
1.28 - Assume (raw_label_for_name name, t)
1.29 - | step_for_line fact_names j (Inference (name, t, _, deps)) =
1.30 - Prove (if j = 1 then [Show] else [], raw_label_for_name name,
1.31 - fold_rev forall_of (map Var (Term.add_vars t [])) t,
1.32 - By_Metis (fold (add_fact_from_dependency fact_names) deps ([], [])))
1.33 -
1.34 fun repair_name "$true" = "c_True"
1.35 | repair_name "$false" = "c_False"
1.36 | repair_name "$$e" = tptp_equal (* seen in Vampire proofs *)
1.37 @@ -714,167 +700,7 @@
1.38 else
1.39 s
1.40
1.41 -fun isar_proof_from_atp_proof pool ctxt isar_shrink_factor fact_names sym_tab
1.42 - params frees atp_proof =
1.43 - let
1.44 - val lines =
1.45 - atp_proof
1.46 - |> clean_up_atp_proof_dependencies
1.47 - |> nasty_atp_proof pool
1.48 - |> map_term_names_in_atp_proof repair_name
1.49 - |> decode_lines ctxt sym_tab
1.50 - |> rpair [] |-> fold_rev (add_line fact_names)
1.51 - |> rpair [] |-> fold_rev add_nontrivial_line
1.52 - |> rpair (0, [])
1.53 - |-> fold_rev (add_desired_line isar_shrink_factor fact_names frees)
1.54 - |> snd
1.55 - in
1.56 - (if null params then [] else [Fix params]) @
1.57 - map2 (step_for_line fact_names) (length lines downto 1) lines
1.58 - end
1.59 -
1.60 -(* When redirecting proofs, we keep information about the labels seen so far in
1.61 - the "backpatches" data structure. The first component indicates which facts
1.62 - should be associated with forthcoming proof steps. The second component is a
1.63 - pair ("assum_ls", "drop_ls"), where "assum_ls" are the labels that should
1.64 - become assumptions and "drop_ls" are the labels that should be dropped in a
1.65 - case split. *)
1.66 -type backpatches = (label * facts) list * (label list * label list)
1.67 -
1.68 -fun used_labels_of_step (Prove (_, _, _, by)) =
1.69 - (case by of
1.70 - By_Metis (ls, _) => ls
1.71 - | Case_Split (proofs, (ls, _)) =>
1.72 - fold (union (op =) o used_labels_of) proofs ls)
1.73 - | used_labels_of_step _ = []
1.74 -and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof []
1.75 -
1.76 -fun new_labels_of_step (Fix _) = []
1.77 - | new_labels_of_step (Let _) = []
1.78 - | new_labels_of_step (Assume (l, _)) = [l]
1.79 - | new_labels_of_step (Prove (_, l, _, _)) = [l]
1.80 -val new_labels_of = maps new_labels_of_step
1.81 -
1.82 -val join_proofs =
1.83 - let
1.84 - fun aux _ [] = NONE
1.85 - | aux proof_tail (proofs as (proof1 :: _)) =
1.86 - if exists null proofs then
1.87 - NONE
1.88 - else if forall (curry (op =) (hd proof1) o hd) (tl proofs) then
1.89 - aux (hd proof1 :: proof_tail) (map tl proofs)
1.90 - else case hd proof1 of
1.91 - Prove ([], l, t, _) => (* FIXME: should we really ignore the "by"? *)
1.92 - if forall (fn Prove ([], l', t', _) :: _ => (l, t) = (l', t')
1.93 - | _ => false) (tl proofs) andalso
1.94 - not (exists (member (op =) (maps new_labels_of proofs))
1.95 - (used_labels_of proof_tail)) then
1.96 - SOME (l, t, map rev proofs, proof_tail)
1.97 - else
1.98 - NONE
1.99 - | _ => NONE
1.100 - in aux [] o map rev end
1.101 -
1.102 -fun case_split_qualifiers proofs =
1.103 - case length proofs of
1.104 - 0 => []
1.105 - | 1 => [Then]
1.106 - | _ => [Ultimately]
1.107 -
1.108 -fun redirect_proof hyp_ts concl_t proof =
1.109 - let
1.110 - (* The first pass outputs those steps that are independent of the negated
1.111 - conjecture. The second pass flips the proof by contradiction to obtain a
1.112 - direct proof, introducing case splits when an inference depends on
1.113 - several facts that depend on the negated conjecture. *)
1.114 - val concl_l = (conjecture_prefix, length hyp_ts)
1.115 - fun first_pass ([], contra) = ([], contra)
1.116 - | first_pass ((step as Fix _) :: proof, contra) =
1.117 - first_pass (proof, contra) |>> cons step
1.118 - | first_pass ((step as Let _) :: proof, contra) =
1.119 - first_pass (proof, contra) |>> cons step
1.120 - | first_pass ((step as Assume (l as (_, j), _)) :: proof, contra) =
1.121 - if l = concl_l then first_pass (proof, contra ||> cons step)
1.122 - else first_pass (proof, contra) |>> cons (Assume (l, nth hyp_ts j))
1.123 - | first_pass (Prove (qs, l, t, By_Metis (ls, ss)) :: proof, contra) =
1.124 - let val step = Prove (qs, l, t, By_Metis (ls, ss)) in
1.125 - if exists (member (op =) (fst contra)) ls then
1.126 - first_pass (proof, contra |>> cons l ||> cons step)
1.127 - else
1.128 - first_pass (proof, contra) |>> cons step
1.129 - end
1.130 - | first_pass _ = raise Fail "malformed proof"
1.131 - val (proof_top, (contra_ls, contra_proof)) =
1.132 - first_pass (proof, ([concl_l], []))
1.133 - val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst
1.134 - fun backpatch_labels patches ls =
1.135 - fold merge_fact_sets (map (backpatch_label patches) ls) ([], [])
1.136 - fun second_pass end_qs ([], assums, patches) =
1.137 - ([Prove (end_qs, no_label, concl_t,
1.138 - By_Metis (backpatch_labels patches (map snd assums)))], patches)
1.139 - | second_pass end_qs (Assume (l, t) :: proof, assums, patches) =
1.140 - second_pass end_qs (proof, (t, l) :: assums, patches)
1.141 - | second_pass end_qs (Prove (qs, l, t, By_Metis (ls, ss)) :: proof, assums,
1.142 - patches) =
1.143 - (if member (op =) (snd (snd patches)) l andalso
1.144 - not (member (op =) (fst (snd patches)) l) andalso
1.145 - not (AList.defined (op =) (fst patches) l) then
1.146 - second_pass end_qs (proof, assums, patches ||> apsnd (append ls))
1.147 - else case List.partition (member (op =) contra_ls) ls of
1.148 - ([contra_l], co_ls) =>
1.149 - if member (op =) qs Show then
1.150 - second_pass end_qs (proof, assums,
1.151 - patches |>> cons (contra_l, (co_ls, ss)))
1.152 - else
1.153 - second_pass end_qs
1.154 - (proof, assums,
1.155 - patches |>> cons (contra_l, (l :: co_ls, ss)))
1.156 - |>> cons (if member (op =) (fst (snd patches)) l then
1.157 - Assume (l, s_not t)
1.158 - else
1.159 - Prove (qs, l, s_not t,
1.160 - By_Metis (backpatch_label patches l)))
1.161 - | (contra_ls as _ :: _, co_ls) =>
1.162 - let
1.163 - val proofs =
1.164 - map_filter
1.165 - (fn l =>
1.166 - if l = concl_l then
1.167 - NONE
1.168 - else
1.169 - let
1.170 - val drop_ls = filter (curry (op <>) l) contra_ls
1.171 - in
1.172 - second_pass []
1.173 - (proof, assums,
1.174 - patches ||> apfst (insert (op =) l)
1.175 - ||> apsnd (union (op =) drop_ls))
1.176 - |> fst |> SOME
1.177 - end) contra_ls
1.178 - val (assumes, facts) =
1.179 - if member (op =) (fst (snd patches)) l then
1.180 - ([Assume (l, s_not t)], (l :: co_ls, ss))
1.181 - else
1.182 - ([], (co_ls, ss))
1.183 - in
1.184 - (case join_proofs proofs of
1.185 - SOME (l, t, proofs, proof_tail) =>
1.186 - Prove (case_split_qualifiers proofs @
1.187 - (if null proof_tail then end_qs else []), l, t,
1.188 - smart_case_split proofs facts) :: proof_tail
1.189 - | NONE =>
1.190 - [Prove (case_split_qualifiers proofs @ end_qs, no_label,
1.191 - concl_t, smart_case_split proofs facts)],
1.192 - patches)
1.193 - |>> append assumes
1.194 - end
1.195 - | _ => raise Fail "malformed proof")
1.196 - | second_pass _ _ = raise Fail "malformed proof"
1.197 - val proof_bottom =
1.198 - second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst
1.199 - in proof_top @ proof_bottom end
1.200 -
1.201 -(* FIXME: Still needed? Probably not. *)
1.202 +(* FIXME: Still needed? Try with SPASS proofs perhaps. *)
1.203 val kill_duplicate_assumptions_in_proof =
1.204 let
1.205 fun relabel_facts subst =
1.206 @@ -895,23 +721,13 @@
1.207 and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev
1.208 in do_proof end
1.209
1.210 -val then_chain_proof =
1.211 - let
1.212 - fun aux _ [] = []
1.213 - | aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof
1.214 - | aux l' (Prove (qs, l, t, by) :: proof) =
1.215 - (case by of
1.216 - By_Metis (ls, ss) =>
1.217 - Prove (if member (op =) ls l' then
1.218 - (Then :: qs, l, t,
1.219 - By_Metis (filter_out (curry (op =) l') ls, ss))
1.220 - else
1.221 - (qs, l, t, By_Metis (ls, ss)))
1.222 - | Case_Split (proofs, facts) =>
1.223 - Prove (qs, l, t, Case_Split (map (aux no_label) proofs, facts))) ::
1.224 - aux l proof
1.225 - | aux _ (step :: proof) = step :: aux no_label proof
1.226 - in aux no_label end
1.227 +fun used_labels_of_step (Prove (_, _, _, by)) =
1.228 + (case by of
1.229 + By_Metis (ls, _) => ls
1.230 + | Case_Split (proofs, (ls, _)) =>
1.231 + fold (union (op =) o used_labels_of) proofs ls)
1.232 + | used_labels_of_step _ = []
1.233 +and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof []
1.234
1.235 fun kill_useless_labels_in_proof proof =
1.236 let
1.237 @@ -1037,104 +853,86 @@
1.238 else partial_typesN
1.239 val lam_trans = lam_trans_from_atp_proof atp_proof metis_default_lam_trans
1.240
1.241 - val atp_proof' = (*###*)
1.242 - atp_proof
1.243 - |> clean_up_atp_proof_dependencies
1.244 - |> nasty_atp_proof pool
1.245 - |> map_term_names_in_atp_proof repair_name
1.246 - |> decode_lines ctxt sym_tab
1.247 - |> rpair [] |-> fold_rev (add_line fact_names)
1.248 - |> rpair [] |-> fold_rev add_nontrivial_line
1.249 - |> rpair (0, [])
1.250 - |-> fold_rev (add_desired_line isar_shrink_factor fact_names frees)
1.251 - |> snd
1.252 -(*
1.253 - |> tap (map (tracing o PolyML.makestring))
1.254 -*)
1.255 -
1.256 - val conj_name = conjecture_prefix ^ string_of_int (length hyp_ts)
1.257 - val conjs =
1.258 - atp_proof'
1.259 - |> map_filter (fn Inference (name as (_, ss), _, _, []) =>
1.260 - if member (op =) ss conj_name then SOME name else NONE
1.261 - | _ => NONE)
1.262 -
1.263 -
1.264 - fun dep_of_step (Definition _) = NONE
1.265 - | dep_of_step (Inference (name, _, _, from)) = SOME (from, name)
1.266 -
1.267 - val ref_graph = atp_proof' |> map_filter dep_of_step |> make_ref_graph
1.268 - val axioms = axioms_of_ref_graph ref_graph conjs
1.269 - val tainted = tainted_atoms_of_ref_graph ref_graph conjs
1.270 -
1.271 - val props =
1.272 - Symtab.empty
1.273 - |> fold (fn Definition _ => I (* FIXME *)
1.274 - | Inference ((s, _), t, _, _) =>
1.275 - Symtab.update_new (s,
1.276 - t |> member (op = o apsnd fst) tainted s ? s_not))
1.277 - atp_proof'
1.278 -
1.279 - val direct_proof =
1.280 - ref_graph |> redirect_graph axioms tainted
1.281 - |> chain_direct_proof
1.282 - |> tap (tracing o string_of_direct_proof) (*###*)
1.283 -
1.284 - fun prop_of_clause c =
1.285 - fold (curry s_disj) (map_filter (Symtab.lookup props o fst) c)
1.286 - @{term False}
1.287 -
1.288 - fun label_of_clause c = (space_implode "___" (map fst c), 0)
1.289 -
1.290 - fun maybe_show outer c =
1.291 - (outer andalso length c = 1 andalso subset (op =) (c, conjs)) ? cons Show
1.292 -
1.293 - fun do_have outer qs (gamma, c) =
1.294 - Prove (maybe_show outer c qs, label_of_clause c, prop_of_clause c,
1.295 - By_Metis (fold (add_fact_from_dependency fact_names o the_single)
1.296 - gamma ([], [])))
1.297 - fun do_inf outer (Have z) = do_have outer [] z
1.298 - | do_inf outer (Hence z) = do_have outer [Then] z
1.299 - | do_inf outer (Cases cases) =
1.300 - let val c = succedent_of_cases cases in
1.301 - Prove (maybe_show outer c [Ultimately], label_of_clause c,
1.302 - prop_of_clause c,
1.303 - Case_Split (map (do_case false) cases, ([], [])))
1.304 - end
1.305 - and do_case outer (c, infs) =
1.306 - Assume (label_of_clause c, prop_of_clause c) :: map (do_inf outer) infs
1.307 -
1.308 - val isar_proof =
1.309 - (if null params then [] else [Fix params]) @
1.310 - (map (do_inf true) direct_proof
1.311 - |> kill_useless_labels_in_proof
1.312 - |> relabel_proof)
1.313 - |> string_for_proof ctxt type_enc lam_trans subgoal subgoal_count
1.314 - |> tap tracing (*###*)
1.315 -
1.316 - fun isar_proof_for () =
1.317 - case atp_proof
1.318 - |> isar_proof_from_atp_proof pool ctxt isar_shrink_factor fact_names
1.319 - sym_tab params frees
1.320 - |> redirect_proof hyp_ts concl_t
1.321 + fun isar_proof_of () =
1.322 + let
1.323 + val atp_proof =
1.324 + atp_proof
1.325 + |> clean_up_atp_proof_dependencies
1.326 + |> nasty_atp_proof pool
1.327 + |> map_term_names_in_atp_proof repair_name
1.328 + |> decode_lines ctxt sym_tab
1.329 + |> rpair [] |-> fold_rev (add_line fact_names)
1.330 + |> rpair [] |-> fold_rev add_nontrivial_line
1.331 + |> rpair (0, [])
1.332 + |-> fold_rev (add_desired_line isar_shrink_factor fact_names frees)
1.333 + |> snd
1.334 + val conj_name = conjecture_prefix ^ string_of_int (length hyp_ts)
1.335 + val conjs =
1.336 + atp_proof
1.337 + |> map_filter (fn Inference (name as (_, ss), _, _, []) =>
1.338 + if member (op =) ss conj_name then SOME name else NONE
1.339 + | _ => NONE)
1.340 + fun dep_of_step (Definition _) = NONE
1.341 + | dep_of_step (Inference (name, _, _, from)) = SOME (from, name)
1.342 + val ref_graph = atp_proof |> map_filter dep_of_step |> make_ref_graph
1.343 + val axioms = axioms_of_ref_graph ref_graph conjs
1.344 + val tainted = tainted_atoms_of_ref_graph ref_graph conjs
1.345 + val props =
1.346 + Symtab.empty
1.347 + |> fold (fn Definition _ => I (* FIXME *)
1.348 + | Inference ((s, _), t, _, _) =>
1.349 + Symtab.update_new (s,
1.350 + t |> member (op = o apsnd fst) tainted s ? s_not))
1.351 + atp_proof
1.352 + (* FIXME: add "fold_rev forall_of (map Var (Term.add_vars t []))"? *)
1.353 + fun prop_of_clause c =
1.354 + fold (curry s_disj) (map_filter (Symtab.lookup props o fst) c)
1.355 + @{term False}
1.356 + fun label_of_clause c = (space_implode "___" (map fst c), 0)
1.357 + fun maybe_show outer c =
1.358 + (outer andalso length c = 1 andalso subset (op =) (c, conjs))
1.359 + ? cons Show
1.360 + fun do_have outer qs (gamma, c) =
1.361 + Prove (maybe_show outer c qs, label_of_clause c, prop_of_clause c,
1.362 + By_Metis (fold (add_fact_from_dependency fact_names
1.363 + o the_single) gamma ([], [])))
1.364 + fun do_inf outer (Have z) = do_have outer [] z
1.365 + | do_inf outer (Hence z) = do_have outer [Then] z
1.366 + | do_inf outer (Cases cases) =
1.367 + let val c = succedent_of_cases cases in
1.368 + Prove (maybe_show outer c [Ultimately], label_of_clause c,
1.369 + prop_of_clause c,
1.370 + Case_Split (map (do_case false) cases, ([], [])))
1.371 + end
1.372 + and do_case outer (c, infs) =
1.373 + Assume (label_of_clause c, prop_of_clause c) ::
1.374 + map (do_inf outer) infs
1.375 + val isar_proof =
1.376 + (if null params then [] else [Fix params]) @
1.377 + (ref_graph
1.378 + |> redirect_graph axioms tainted
1.379 + |> chain_direct_proof
1.380 + |> map (do_inf true)
1.381 |> kill_duplicate_assumptions_in_proof
1.382 - |> then_chain_proof
1.383 |> kill_useless_labels_in_proof
1.384 - |> relabel_proof
1.385 - |> string_for_proof ctxt type_enc lam_trans subgoal subgoal_count of
1.386 - "" =>
1.387 - if isar_proof_requested then
1.388 - "\nNo structured proof available (proof too short)."
1.389 - else
1.390 - ""
1.391 - | proof =>
1.392 - "\n\n" ^ (if isar_proof_requested then "Structured proof"
1.393 - else "Perhaps this will work") ^
1.394 - ":\n" ^ Markup.markup Isabelle_Markup.sendback proof
1.395 + |> relabel_proof)
1.396 + |> string_for_proof ctxt type_enc lam_trans subgoal subgoal_count
1.397 + in
1.398 + case isar_proof of
1.399 + "" =>
1.400 + if isar_proof_requested then
1.401 + "\nNo structured proof available (proof too short)."
1.402 + else
1.403 + ""
1.404 + | _ =>
1.405 + "\n\n" ^ (if isar_proof_requested then "Structured proof"
1.406 + else "Perhaps this will work") ^
1.407 + ":\n" ^ Markup.markup Isabelle_Markup.sendback isar_proof
1.408 + end
1.409 val isar_proof =
1.410 if debug then
1.411 - isar_proof_for ()
1.412 - else case try isar_proof_for () of
1.413 + isar_proof_of ()
1.414 + else case try isar_proof_of () of
1.415 SOME s => s
1.416 | NONE => if isar_proof_requested then
1.417 "\nWarning: The Isar proof construction failed."
2.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML Wed Dec 14 23:08:03 2011 +0100
2.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Wed Dec 14 23:08:03 2011 +0100
2.3 @@ -83,7 +83,7 @@
2.4 if Meson_Clausify.is_quasi_lambda_free (term_of ct) then
2.5 Thm.reflexive ct
2.6 else case term_of ct of
2.7 - t as Abs (_, _, u) =>
2.8 + Abs (_, _, u) =>
2.9 if first then
2.10 case add_vars_and_frees u [] of
2.11 [] =>