1(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML 2 Author: Jasmin Blanchette, TU Muenchen 3 Author: Steffen Juilf Smolka, TU Muenchen 4 5Basic data structures for representing and basic methods 6for dealing with Isar proof texts. 7*) 8 9signature SLEDGEHAMMER_ISAR_PROOF = 10sig 11 type proof_method = Sledgehammer_Proof_Methods.proof_method 12 13 type label = string * int 14 type facts = label list * string list (* local and global facts *) 15 16 datatype isar_qualifier = Show | Then 17 18 datatype isar_proof = 19 Proof of (string * typ) list * (label * term) list * isar_step list 20 and isar_step = 21 Let of term * term | 22 Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list 23 * facts * proof_method list * string 24 25 val no_label : label 26 27 val label_ord : label ord 28 val string_of_label : label -> string 29 val sort_facts : facts -> facts 30 31 val steps_of_isar_proof : isar_proof -> isar_step list 32 val label_of_isar_step : isar_step -> label option 33 val facts_of_isar_step : isar_step -> facts 34 val proof_methods_of_isar_step : isar_step -> proof_method list 35 36 val fold_isar_steps : (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a 37 val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof 38 val add_isar_steps : isar_step list -> int -> int 39 40 structure Canonical_Label_Tab : TABLE 41 42 val canonical_label_ord : label ord 43 44 val comment_isar_proof : (label -> proof_method list -> string) -> isar_proof -> isar_proof 45 val chain_isar_proof : isar_proof -> isar_proof 46 val kill_useless_labels_in_isar_proof : isar_proof -> isar_proof 47 val relabel_isar_proof_canonically : isar_proof -> isar_proof 48 val relabel_isar_proof_nicely : isar_proof -> isar_proof 49 val rationalize_obtains_in_isar_proofs : Proof.context -> isar_proof -> isar_proof 50 51 val string_of_isar_proof : Proof.context -> int -> int -> isar_proof -> string 52end; 53 54structure Sledgehammer_Isar_Proof : SLEDGEHAMMER_ISAR_PROOF = 55struct 56 57open ATP_Util 58open ATP_Proof 59open ATP_Problem_Generate 60open ATP_Proof_Reconstruct 61open Sledgehammer_Util 62open Sledgehammer_Proof_Methods 63open Sledgehammer_Isar_Annotate 64 65type label = string * int 66type facts = label list * string list (* local and global facts *) 67 68datatype isar_qualifier = Show | Then 69 70datatype isar_proof = 71 Proof of (string * typ) list * (label * term) list * isar_step list 72and isar_step = 73 Let of term * term | 74 Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list 75 * facts * proof_method list * string 76 77val no_label = ("", ~1) 78 79(* cf. "label_ord" below *) 80val assume_prefix = "a" 81val have_prefix = "f" 82 83fun label_ord ((s1, i1), (s2, i2)) = 84 (case int_ord (apply2 String.size (s1, s2)) of 85 EQUAL => 86 (case string_ord (s1, s2) of 87 EQUAL => int_ord (i1, i2) 88 | ord => ord (* "assume" before "have" *)) 89 | ord => ord) 90 91fun string_of_label (s, num) = s ^ string_of_int num 92 93(* Put the nearest local label first, since it's the most likely to be replaced by a "hence". 94 (Some preplaying proof methods, e.g. "blast", react poorly to fact reorderings.) *) 95fun sort_facts (lfs, gfs) = (sort (label_ord o swap) lfs, sort string_ord gfs) 96 97fun steps_of_isar_proof (Proof (_, _, steps)) = steps 98 99fun label_of_isar_step (Prove (_, _, l, _, _, _, _, _)) = SOME l 100 | label_of_isar_step _ = NONE 101 102fun subproofs_of_isar_step (Prove (_, _, _, _, subs, _, _, _)) = subs 103 | subproofs_of_isar_step _ = [] 104 105fun facts_of_isar_step (Prove (_, _, _, _, _, facts, _, _)) = facts 106 | facts_of_isar_step _ = ([], []) 107 108fun proof_methods_of_isar_step (Prove (_, _, _, _, _, _, meths, _)) = meths 109 | proof_methods_of_isar_step _ = [] 110 111fun fold_isar_step f step = 112 fold (steps_of_isar_proof #> fold_isar_steps f) (subproofs_of_isar_step step) #> f step 113and fold_isar_steps f = fold (fold_isar_step f) 114 115fun map_isar_steps f = 116 let 117 fun map_proof (Proof (fix, assms, steps)) = Proof (fix, assms, map map_step steps) 118 and map_step (step as Let _) = f step 119 | map_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) = 120 f (Prove (qs, xs, l, t, map map_proof subs, facts, meths, comment)) 121 in map_proof end 122 123val add_isar_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I) 124 125(* canonical proof labels: 1, 2, 3, ... in post traversal order *) 126fun canonical_label_ord (((_, i1), (_, i2)) : label * label) = int_ord (i1, i2) 127 128structure Canonical_Label_Tab = Table( 129 type key = label 130 val ord = canonical_label_ord) 131 132fun comment_isar_step comment_of (Prove (qs, xs, l, t, subs, facts, meths, _)) = 133 Prove (qs, xs, l, t, subs, facts, meths, comment_of l meths) 134 | comment_isar_step _ step = step 135fun comment_isar_proof comment_of = map_isar_steps (comment_isar_step comment_of) 136 137fun chain_qs_lfs NONE lfs = ([], lfs) 138 | chain_qs_lfs (SOME l0) lfs = 139 if member (op =) lfs l0 then ([Then], remove (op =) l0 lfs) else ([], lfs) 140 141fun chain_isar_step lbl (Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment)) = 142 let val (qs', lfs) = chain_qs_lfs lbl lfs in 143 Prove (qs' @ qs, xs, l, t, map chain_isar_proof subs, (lfs, gfs), meths, comment) 144 end 145 | chain_isar_step _ step = step 146and chain_isar_steps _ [] = [] 147 | chain_isar_steps prev (i :: is) = 148 chain_isar_step prev i :: chain_isar_steps (label_of_isar_step i) is 149and chain_isar_proof (Proof (fix, assms, steps)) = 150 Proof (fix, assms, chain_isar_steps (try (List.last #> fst) assms) steps) 151 152fun kill_useless_labels_in_isar_proof proof = 153 let 154 val used_ls = 155 fold_isar_steps (facts_of_isar_step #> fst #> union (op =)) (steps_of_isar_proof proof) [] 156 157 fun kill_label l = if member (op =) used_ls l then l else no_label 158 159 fun kill_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) = 160 Prove (qs, xs, kill_label l, t, map kill_proof subs, facts, meths, comment) 161 | kill_step step = step 162 and kill_proof (Proof (fix, assms, steps)) = 163 Proof (fix, map (apfst kill_label) assms, map kill_step steps) 164 in 165 kill_proof proof 166 end 167 168fun relabel_isar_proof_canonically proof = 169 let 170 fun next_label l (next, subst) = 171 let val l' = ("", next) in (l', (next + 1, (l, l') :: subst)) end 172 173 fun relabel_step (Prove (qs, fix, l, t, subs, (lfs, gfs), meths, comment)) 174 (accum as (_, subst)) = 175 let 176 val lfs' = maps (the_list o AList.lookup (op =) subst) lfs 177 val ((subs', l'), accum') = accum 178 |> fold_map relabel_proof subs 179 ||>> next_label l 180 in 181 (Prove (qs, fix, l', t, subs', (lfs', gfs), meths, comment), accum') 182 end 183 | relabel_step step accum = (step, accum) 184 and relabel_proof (Proof (fix, assms, steps)) = 185 fold_map (fn (l, t) => next_label l #> apfst (rpair t)) assms 186 ##>> fold_map relabel_step steps 187 #>> (fn (assms, steps) => Proof (fix, assms, steps)) 188 in 189 fst (relabel_proof proof (0, [])) 190 end 191 192val relabel_isar_proof_nicely = 193 let 194 fun next_label depth prefix l (accum as (next, subst)) = 195 if l = no_label then 196 (l, accum) 197 else 198 let val l' = (replicate_string (depth + 1) prefix, next) in 199 (l', (next + 1, (l, l') :: subst)) 200 end 201 202 fun relabel_step depth (Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment)) 203 (accum as (_, subst)) = 204 let 205 val lfs' = maps (the_list o AList.lookup (op =) subst) lfs 206 val (l', accum' as (_, subst')) = next_label depth have_prefix l accum 207 val subs' = map (relabel_proof subst' (depth + 1)) subs 208 in 209 (Prove (qs, xs, l', t, subs', (lfs', gfs), meths, comment), accum') 210 end 211 | relabel_step _ step accum = (step, accum) 212 and relabel_proof subst depth (Proof (fix, assms, steps)) = 213 (1, subst) 214 |> fold_map (fn (l, t) => next_label depth assume_prefix l #> apfst (rpair t)) assms 215 ||>> fold_map (relabel_step depth) steps 216 |> (fn ((assms, steps), _) => Proof (fix, assms, steps)) 217 in 218 relabel_proof [] 0 219 end 220 221fun stutter_single_letter s = String.extract (s, 0, SOME 1) ^ s 222 223fun rationalize_obtains_in_isar_proofs ctxt = 224 let 225 fun rename_obtains xs (subst, ctxt) = 226 let 227 val Ts = map snd xs 228 val new_names0 = map (stutter_single_letter o var_name_of_typ o body_type) Ts 229 val (new_names, ctxt') = Variable.variant_fixes new_names0 ctxt 230 val ys = map2 pair new_names Ts 231 in 232 (ys, ((map Free xs ~~ map Free ys) @ subst, ctxt')) 233 end 234 235 fun rationalize_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) subst_ctxt = 236 let 237 val (xs', subst_ctxt' as (subst', _)) = rename_obtains xs subst_ctxt 238 val t' = subst_atomic subst' t 239 val subs' = map (rationalize_proof false subst_ctxt') subs 240 in 241 (Prove (qs, xs', l, t', subs', facts, meths, comment), subst_ctxt') 242 end 243 and rationalize_proof outer (subst_ctxt as (subst, ctxt)) (Proof (fix, assms, steps)) = 244 let 245 val (fix', subst_ctxt' as (subst', _)) = 246 if outer then 247 (* last call: eliminate any remaining skolem names (from SMT proofs) *) 248 (fix, (subst @ map (fn x => (Free (apfst Name.skolem x), Free x)) fix, ctxt)) 249 else 250 rename_obtains fix subst_ctxt 251 in 252 Proof (fix', map (apsnd (subst_atomic subst')) assms, 253 fst (fold_map rationalize_step steps subst_ctxt')) 254 end 255 in 256 rationalize_proof true ([], ctxt) 257 end 258 259val thesis_var = ((Auto_Bind.thesisN, 0), HOLogic.boolT) 260 261fun is_thesis ctxt t = 262 (case Vartab.lookup (Variable.binds_of ctxt) (fst thesis_var) of 263 SOME (_, t') => HOLogic.mk_Trueprop t' aconv t 264 | NONE => false) 265 266val indent_size = 2 267 268fun string_of_isar_proof ctxt0 i n proof = 269 let 270 val keywords = Thy_Header.get_keywords' ctxt0 271 272 (* Make sure only type constraints inserted by the type annotation code are printed. *) 273 val ctxt = ctxt0 274 |> Config.put show_markup false 275 |> Config.put Printer.show_type_emphasis false 276 |> Config.put show_types false 277 |> Config.put show_sorts false 278 |> Config.put show_consts false 279 280 fun add_str s' = apfst (suffix s') 281 282 fun of_indent ind = replicate_string (ind * indent_size) " " 283 fun of_moreover ind = of_indent ind ^ "moreover\n" 284 fun of_label l = if l = no_label then "" else string_of_label l ^ ": " 285 286 fun of_obtain qs nr = 287 (if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately " 288 else if nr = 1 orelse member (op =) qs Then then "then " 289 else "") ^ "obtain" 290 291 fun of_show_have qs = if member (op =) qs Show then "show" else "have" 292 fun of_thus_hence qs = if member (op =) qs Show then "then show" else "then have" 293 294 fun of_have qs nr = 295 if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately " ^ of_show_have qs 296 else if nr = 1 orelse member (op =) qs Then then of_thus_hence qs 297 else of_show_have qs 298 299 fun add_term term (s, ctxt) = 300 (s ^ (term 301 |> singleton (Syntax.uncheck_terms ctxt) 302 |> annotate_types_in_term ctxt 303 |> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of) 304 |> simplify_spaces 305 |> maybe_quote keywords), 306 ctxt |> perhaps (try (Proof_Context.augment term))) 307 308 fun using_facts [] [] = "" 309 | using_facts ls ss = enclose "using " " " (space_implode " " (map string_of_label ls @ ss)) 310 311 (* Local facts are always passed via "using", which affects "meson" and "metis". This is 312 arguably stylistically superior, because it emphasises the structure of the proof. It is also 313 more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "then" 314 is introduced. See also "tac_of_method" in "Sledgehammer_Isar_Preplay". *) 315 fun of_method ls ss meth = 316 let val direct = is_proof_method_direct meth in 317 using_facts ls (if direct then [] else ss) ^ 318 "by " ^ string_of_proof_method ctxt (if direct then ss else []) meth 319 end 320 321 fun of_free (s, T) = 322 maybe_quote keywords s ^ " :: " ^ 323 maybe_quote keywords (simplify_spaces (Print_Mode.setmp [] (Syntax.string_of_typ ctxt) T)) 324 325 fun add_frees xs (s, ctxt) = 326 (s ^ space_implode " and " (map of_free xs), ctxt |> fold Proof_Context.augment (map Free xs)) 327 328 fun add_fix _ [] = I 329 | add_fix ind xs = add_str (of_indent ind ^ "fix ") #> add_frees xs #> add_str "\n" 330 331 fun add_assm ind (l, t) = 332 add_str (of_indent ind ^ "assume " ^ of_label l) #> add_term t #> add_str "\n" 333 334 fun of_subproof ind ctxt proof = 335 let 336 val ind = ind + 1 337 val s = of_proof ind ctxt proof 338 val prefix = "{ " 339 val suffix = " }" 340 in 341 replicate_string (ind * indent_size - size prefix) " " ^ prefix ^ 342 String.extract (s, ind * indent_size, SOME (size s - ind * indent_size - 1)) ^ 343 suffix ^ "\n" 344 end 345 and of_subproofs _ _ _ [] = "" 346 | of_subproofs ind ctxt qs subs = 347 (if member (op =) qs Then then of_moreover ind else "") ^ 348 space_implode (of_moreover ind) (map (of_subproof ind ctxt) subs) 349 and add_step_pre ind qs subs (s, ctxt) = 350 (s ^ of_subproofs ind ctxt qs subs ^ of_indent ind, ctxt) 351 and add_step ind (Let (t1, t2)) = 352 add_str (of_indent ind ^ "let ") #> add_term t1 #> add_str " = " #> add_term t2 353 #> add_str "\n" 354 | add_step ind (Prove (qs, xs, l, t, subs, (ls, ss), meth :: _, comment)) = 355 add_step_pre ind qs subs 356 #> (case xs of 357 [] => add_str (of_have qs (length subs) ^ " ") 358 | _ => 359 add_str (of_obtain qs (length subs) ^ " ") 360 #> add_frees xs 361 #> add_str (" where\n" ^ of_indent (ind + 1))) 362 #> add_str (of_label l) 363 #> add_term (if is_thesis ctxt t then HOLogic.mk_Trueprop (Var thesis_var) else t) 364 #> add_str ("\n" ^ of_indent (ind + 1) ^ of_method ls ss meth ^ 365 (if comment = "" then "" else " (* " ^ comment ^ " *)") ^ "\n") 366 and add_steps ind = fold (add_step ind) 367 and of_proof ind ctxt (Proof (xs, assms, steps)) = 368 ("", ctxt) 369 |> add_fix ind xs 370 |> fold (add_assm ind) assms 371 |> add_steps ind steps 372 |> fst 373 in 374 (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ 375 of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^ 376 of_indent 0 ^ (if n = 1 then "qed" else "next") 377 end 378 379end; 380