1.1 --- a/src/HOL/Tools/ATP/atp_reconstruct.ML Fri Nov 18 06:50:05 2011 +0100
1.2 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Fri Nov 18 11:47:12 2011 +0100
1.3 @@ -26,8 +26,8 @@
1.4 type one_line_params =
1.5 play * string * (string * locality) list * minimize_command * int * int
1.6 type isar_params =
1.7 - bool * bool * int * string Symtab.table * int list list * int
1.8 - * (string * locality) list vector * int Symtab.table * string proof * thm
1.9 + bool * bool * int * string Symtab.table * (string * locality) list vector
1.10 + * int Symtab.table * string proof * thm
1.11
1.12 val metisN : string
1.13 val smtN : string
1.14 @@ -41,12 +41,12 @@
1.15 val full_type_encs : string list
1.16 val partial_type_encs : string list
1.17 val used_facts_in_atp_proof :
1.18 - Proof.context -> int -> (string * locality) list vector -> string proof
1.19 + Proof.context -> (string * locality) list vector -> string proof
1.20 -> (string * locality) list
1.21 val used_facts_in_unsound_atp_proof :
1.22 - Proof.context -> int list list -> int -> (string * locality) list vector
1.23 - -> 'a proof -> string list option
1.24 - val uses_typed_helpers : int list -> 'a proof -> bool
1.25 + Proof.context -> (string * locality) list vector -> 'a proof
1.26 + -> string list option
1.27 + val uses_typed_helpers : 'a proof -> bool
1.28 val unalias_type_enc : string -> string list
1.29 val metis_default_lam_trans : string
1.30 val metis_call : string -> string -> string
1.31 @@ -87,11 +87,8 @@
1.32 type one_line_params =
1.33 play * string * (string * locality) list * minimize_command * int * int
1.34 type isar_params =
1.35 - bool * bool * int * string Symtab.table * int list list * int
1.36 - * (string * locality) list vector * int Symtab.table * string proof * thm
1.37 -
1.38 -val is_typed_helper_name =
1.39 - String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix
1.40 + bool * bool * int * string Symtab.table * (string * locality) list vector
1.41 + * int Symtab.table * string proof * thm
1.42
1.43 fun find_first_in_list_vector vec key =
1.44 Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
1.45 @@ -99,11 +96,6 @@
1.46
1.47 val unprefix_fact_number = space_implode "_" o tl o space_explode "_"
1.48
1.49 -val vampire_step_prefix = "f" (* grrr... *)
1.50 -
1.51 -val extract_step_number =
1.52 - Int.fromString o perhaps (try (unprefix vampire_step_prefix))
1.53 -
1.54 fun resolve_one_named_fact fact_names s =
1.55 case try (unprefix fact_prefix) s of
1.56 SOME s' =>
1.57 @@ -111,43 +103,22 @@
1.58 s' |> find_first_in_list_vector fact_names |> Option.map (pair s')
1.59 end
1.60 | NONE => NONE
1.61 -fun resolve_fact _ fact_names (_, SOME ss) =
1.62 - map_filter (resolve_one_named_fact fact_names) ss
1.63 - | resolve_fact facts_offset fact_names (num, NONE) =
1.64 - (case extract_step_number num of
1.65 - SOME j =>
1.66 - let val j = j - facts_offset in
1.67 - if j > 0 andalso j <= Vector.length fact_names then
1.68 - Vector.sub (fact_names, j - 1)
1.69 - else
1.70 - []
1.71 - end
1.72 - | NONE => [])
1.73 -
1.74 -fun is_fact conjecture_shape = not o null o resolve_fact 0 conjecture_shape
1.75 +fun resolve_fact fact_names (_, ss) =
1.76 + map_filter (resolve_one_named_fact fact_names) ss
1.77 +val is_fact = not o null oo resolve_fact
1.78
1.79 fun resolve_one_named_conjecture s =
1.80 case try (unprefix conjecture_prefix) s of
1.81 SOME s' => Int.fromString s'
1.82 | NONE => NONE
1.83
1.84 -fun resolve_conjecture _ (_, SOME ss) =
1.85 - map_filter resolve_one_named_conjecture ss
1.86 - | resolve_conjecture conjecture_shape (num, NONE) =
1.87 - case extract_step_number num of
1.88 - SOME i => (case find_index (exists (curry (op =) i)) conjecture_shape of
1.89 - ~1 => []
1.90 - | j => [j])
1.91 - | NONE => []
1.92 +fun resolve_conjecture (_, ss) = map_filter resolve_one_named_conjecture ss
1.93 +val is_conjecture = not o null o resolve_conjecture
1.94
1.95 -fun is_conjecture conjecture_shape =
1.96 - not o null o resolve_conjecture conjecture_shape
1.97 -
1.98 -fun is_typed_helper _ (_, SOME ss) = exists is_typed_helper_name ss
1.99 - | is_typed_helper typed_helpers (num, NONE) =
1.100 - (case extract_step_number num of
1.101 - SOME i => member (op =) typed_helpers i
1.102 - | NONE => false)
1.103 +val is_typed_helper_name =
1.104 + String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix
1.105 +fun is_typed_helper (_, ss) = exists is_typed_helper_name ss
1.106 + | is_typed_helper _ = false
1.107
1.108 val leo2_ext = "extcnf_equal_neg"
1.109 val isa_ext = Thm.get_name_hint @{thm ext}
1.110 @@ -160,19 +131,20 @@
1.111 else
1.112 isa_ext
1.113
1.114 -fun add_fact _ facts_offset fact_names (Inference (name, _, _, [])) =
1.115 - union (op =) (resolve_fact facts_offset fact_names name)
1.116 - | add_fact ctxt _ _ (Inference (_, _, rule, _)) =
1.117 +fun add_fact _ fact_names (Inference (name, _, _, [])) =
1.118 + union (op =) (resolve_fact fact_names name)
1.119 + | add_fact ctxt _ (Inference (_, _, rule, _)) =
1.120 if rule = leo2_ext then insert (op =) (ext_name ctxt, General) else I
1.121 - | add_fact _ _ _ _ = I
1.122 + | add_fact _ _ _ = I
1.123
1.124 -fun used_facts_in_atp_proof ctxt facts_offset fact_names atp_proof =
1.125 +fun used_facts_in_atp_proof ctxt fact_names atp_proof =
1.126 if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names
1.127 - else fold (add_fact ctxt facts_offset fact_names) atp_proof []
1.128 + else fold (add_fact ctxt fact_names) atp_proof []
1.129
1.130 -fun is_conjecture_used_in_proof conjecture_shape =
1.131 - exists (fn Inference (name, _, _, []) => is_conjecture conjecture_shape name
1.132 - | _ => false)
1.133 +(* FIXME ### merge with other similar functions *)
1.134 +fun is_conjecture_used_in_proof proof =
1.135 + exists (fn Inference (name, _, _, []) => is_conjecture name | _ => false)
1.136 + proof
1.137
1.138 (* (quasi-)underapproximation of the truth *)
1.139 fun is_locality_global Local = false
1.140 @@ -180,23 +152,21 @@
1.141 | is_locality_global Chained = false
1.142 | is_locality_global _ = true
1.143
1.144 -fun used_facts_in_unsound_atp_proof _ _ _ _ [] = NONE
1.145 - | used_facts_in_unsound_atp_proof ctxt conjecture_shape facts_offset
1.146 - fact_names atp_proof =
1.147 +fun used_facts_in_unsound_atp_proof _ _ [] = NONE
1.148 + | used_facts_in_unsound_atp_proof ctxt fact_names atp_proof =
1.149 let
1.150 - val used_facts =
1.151 - used_facts_in_atp_proof ctxt facts_offset fact_names atp_proof
1.152 + val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
1.153 in
1.154 if forall (is_locality_global o snd) used_facts andalso
1.155 - not (is_conjecture_used_in_proof conjecture_shape atp_proof) then
1.156 + not (is_conjecture_used_in_proof atp_proof) then
1.157 SOME (map fst used_facts)
1.158 else
1.159 NONE
1.160 end
1.161
1.162 -fun uses_typed_helpers typed_helpers =
1.163 - exists (fn Inference (name, _, _, []) => is_typed_helper typed_helpers name
1.164 - | _ => false)
1.165 +fun uses_typed_helpers proof =
1.166 + exists (fn Inference (name, _, _, []) => is_typed_helper name | _ => false)
1.167 + proof
1.168
1.169
1.170 (** Soft-core proof reconstruction: one-liners **)
1.171 @@ -311,8 +281,8 @@
1.172 val assum_prefix = "A"
1.173 val have_prefix = "F"
1.174
1.175 -fun raw_label_for_name conjecture_shape name =
1.176 - case resolve_conjecture conjecture_shape name of
1.177 +fun raw_label_for_name name =
1.178 + case resolve_conjecture name of
1.179 [j] => (conjecture_prefix, j)
1.180 | _ => case Int.fromString (fst name) of
1.181 SOME j => (raw_prefix, j)
1.182 @@ -619,8 +589,8 @@
1.183
1.184 (* Discard facts; consolidate adjacent lines that prove the same formula, since
1.185 they differ only in type information.*)
1.186 -fun add_line _ _ (line as Definition _) lines = line :: lines
1.187 - | add_line conjecture_shape fact_names (Inference (name, t, rule, [])) lines =
1.188 +fun add_line _ (line as Definition _) lines = line :: lines
1.189 + | add_line fact_names (Inference (name, t, rule, [])) lines =
1.190 (* No dependencies: fact, conjecture, or (for Vampire) internal facts or
1.191 definitions. *)
1.192 if is_fact fact_names name then
1.193 @@ -633,11 +603,11 @@
1.194 | (pre, Inference (name', _, _, _) :: post) =>
1.195 pre @ map (replace_dependencies_in_line (name', [name])) post
1.196 | _ => raise Fail "unexpected inference"
1.197 - else if is_conjecture conjecture_shape name then
1.198 + else if is_conjecture name then
1.199 Inference (name, s_not t, rule, []) :: lines
1.200 else
1.201 map (replace_dependencies_in_line (name, [])) lines
1.202 - | add_line _ _ (Inference (name, t, rule, deps)) lines =
1.203 + | add_line _ (Inference (name, t, rule, deps)) lines =
1.204 (* Type information will be deleted later; skip repetition test. *)
1.205 if is_only_type_information t then
1.206 Inference (name, t, rule, deps) :: lines
1.207 @@ -665,13 +635,13 @@
1.208 fun is_bad_free frees (Free x) = not (member (op =) frees x)
1.209 | is_bad_free _ _ = false
1.210
1.211 -fun add_desired_line _ _ _ _ (line as Definition (name, _, _)) (j, lines) =
1.212 +fun add_desired_line _ _ _ (line as Definition (name, _, _)) (j, lines) =
1.213 (j, line :: map (replace_dependencies_in_line (name, [])) lines)
1.214 - | add_desired_line isar_shrink_factor conjecture_shape fact_names frees
1.215 + | add_desired_line isar_shrink_factor fact_names frees
1.216 (Inference (name, t, rule, deps)) (j, lines) =
1.217 (j + 1,
1.218 if is_fact fact_names name orelse
1.219 - is_conjecture conjecture_shape name orelse
1.220 + is_conjecture name orelse
1.221 (* the last line must be kept *)
1.222 j = 0 orelse
1.223 (not (is_only_type_information t) andalso
1.224 @@ -706,23 +676,19 @@
1.225 fun smart_case_split [] facts = ByMetis facts
1.226 | smart_case_split proofs facts = CaseSplit (proofs, facts)
1.227
1.228 -fun add_fact_from_dependency conjecture_shape facts_offset fact_names name =
1.229 +fun add_fact_from_dependency fact_names name =
1.230 if is_fact fact_names name then
1.231 - apsnd (union (op =) (map fst (resolve_fact facts_offset fact_names name)))
1.232 + apsnd (union (op =) (map fst (resolve_fact fact_names name)))
1.233 else
1.234 - apfst (insert (op =) (raw_label_for_name conjecture_shape name))
1.235 + apfst (insert (op =) (raw_label_for_name name))
1.236
1.237 -fun step_for_line _ _ _ _ (Definition (_, t1, t2)) = Let (t1, t2)
1.238 - | step_for_line conjecture_shape _ _ _ (Inference (name, t, _, [])) =
1.239 - Assume (raw_label_for_name conjecture_shape name, t)
1.240 - | step_for_line conjecture_shape facts_offset fact_names j
1.241 - (Inference (name, t, _, deps)) =
1.242 - Have (if j = 1 then [Show] else [],
1.243 - raw_label_for_name conjecture_shape name,
1.244 +fun step_for_line _ _ (Definition (_, t1, t2)) = Let (t1, t2)
1.245 + | step_for_line _ _ (Inference (name, t, _, [])) =
1.246 + Assume (raw_label_for_name name, t)
1.247 + | step_for_line fact_names j (Inference (name, t, _, deps)) =
1.248 + Have (if j = 1 then [Show] else [], raw_label_for_name name,
1.249 fold_rev forall_of (map Var (Term.add_vars t [])) t,
1.250 - ByMetis (fold (add_fact_from_dependency conjecture_shape facts_offset
1.251 - fact_names)
1.252 - deps ([], [])))
1.253 + ByMetis (fold (add_fact_from_dependency fact_names) deps ([], [])))
1.254
1.255 fun repair_name "$true" = "c_True"
1.256 | repair_name "$false" = "c_False"
1.257 @@ -735,8 +701,8 @@
1.258 else
1.259 s
1.260
1.261 -fun isar_proof_from_atp_proof pool ctxt isar_shrink_factor conjecture_shape
1.262 - facts_offset fact_names sym_tab params frees atp_proof =
1.263 +fun isar_proof_from_atp_proof pool ctxt isar_shrink_factor fact_names sym_tab
1.264 + params frees atp_proof =
1.265 let
1.266 val lines =
1.267 atp_proof
1.268 @@ -744,16 +710,14 @@
1.269 |> nasty_atp_proof pool
1.270 |> map_term_names_in_atp_proof repair_name
1.271 |> decode_lines ctxt sym_tab
1.272 - |> rpair [] |-> fold_rev (add_line conjecture_shape fact_names)
1.273 + |> rpair [] |-> fold_rev (add_line fact_names)
1.274 |> rpair [] |-> fold_rev add_nontrivial_line
1.275 |> rpair (0, [])
1.276 - |-> fold_rev (add_desired_line isar_shrink_factor conjecture_shape
1.277 - fact_names frees)
1.278 + |-> fold_rev (add_desired_line isar_shrink_factor fact_names frees)
1.279 |> snd
1.280 in
1.281 (if null params then [] else [Fix params]) @
1.282 - map2 (step_for_line conjecture_shape facts_offset fact_names)
1.283 - (length lines downto 1) lines
1.284 + map2 (step_for_line fact_names) (length lines downto 1) lines
1.285 end
1.286
1.287 (* When redirecting proofs, we keep information about the labels seen so far in
1.288 @@ -1047,8 +1011,8 @@
1.289 in do_proof end
1.290
1.291 fun isar_proof_text ctxt isar_proof_requested
1.292 - (debug, full_types, isar_shrink_factor, pool, conjecture_shape,
1.293 - facts_offset, fact_names, sym_tab, atp_proof, goal)
1.294 + (debug, full_types, isar_shrink_factor, pool, fact_names, sym_tab,
1.295 + atp_proof, goal)
1.296 (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
1.297 let
1.298 val isar_shrink_factor =
1.299 @@ -1058,8 +1022,8 @@
1.300 val one_line_proof = one_line_proof_text one_line_params
1.301 fun isar_proof_for () =
1.302 case atp_proof
1.303 - |> isar_proof_from_atp_proof pool ctxt isar_shrink_factor
1.304 - conjecture_shape facts_offset fact_names sym_tab params frees
1.305 + |> isar_proof_from_atp_proof pool ctxt isar_shrink_factor fact_names
1.306 + sym_tab params frees
1.307 |> redirect_proof hyp_ts concl_t
1.308 |> kill_duplicate_assumptions_in_proof
1.309 |> then_chain_proof