1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Sat Dec 05 14:26:56 2015 +0100
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Sat Dec 05 16:09:41 2015 +0100
1.3 @@ -26,9 +26,9 @@
1.4
1.5 val label_ord : label * label -> order
1.6 val string_of_label : label -> string
1.7 + val sort_facts : facts -> facts
1.8
1.9 val steps_of_isar_proof : isar_proof -> isar_step list
1.10 -
1.11 val label_of_isar_step : isar_step -> label option
1.12 val facts_of_isar_step : isar_step -> facts
1.13 val proof_methods_of_isar_step : isar_step -> proof_method list
1.14 @@ -46,6 +46,7 @@
1.15 val kill_useless_labels_in_isar_proof : isar_proof -> isar_proof
1.16 val relabel_isar_proof_canonically : isar_proof -> isar_proof
1.17 val relabel_isar_proof_nicely : isar_proof -> isar_proof
1.18 + val rationalize_obtains_in_isar_proofs : Proof.context -> isar_proof -> isar_proof
1.19
1.20 val string_of_isar_proof : Proof.context -> int -> int -> isar_proof -> string
1.21 end;
1.22 @@ -75,10 +76,24 @@
1.23
1.24 val no_label = ("", ~1)
1.25
1.26 -val label_ord = pairself swap #> prod_ord int_ord fast_string_ord
1.27 +(* cf. "label_ord" below *)
1.28 +val assume_prefix = "a"
1.29 +val have_prefix = "f"
1.30 +
1.31 +fun label_ord ((s1, i1), (s2, i2)) =
1.32 + (case int_ord (apply2 String.size (s1, s2)) of
1.33 + EQUAL =>
1.34 + (case string_ord (s1, s2) of
1.35 + EQUAL => int_ord (i1, i2)
1.36 + | ord => ord (* "assume" before "have" *))
1.37 + | ord => ord)
1.38
1.39 fun string_of_label (s, num) = s ^ string_of_int num
1.40
1.41 +(* Put the nearest local label first, since it's the most likely to be replaced by a "hence".
1.42 + (Some preplaying proof methods, e.g. "blast", react poorly to fact reorderings.) *)
1.43 +fun sort_facts (lfs, gfs) = (sort (label_ord o swap) lfs, sort string_ord gfs)
1.44 +
1.45 fun steps_of_isar_proof (Proof (_, _, steps)) = steps
1.46
1.47 fun label_of_isar_step (Prove (_, _, l, _, _, _, _, _)) = SOME l
1.48 @@ -174,9 +189,6 @@
1.49 fst (relabel_proof proof (0, []))
1.50 end
1.51
1.52 -val assume_prefix = "a"
1.53 -val have_prefix = "f"
1.54 -
1.55 val relabel_isar_proof_nicely =
1.56 let
1.57 fun next_label depth prefix l (accum as (next, subst)) =
1.58 @@ -206,10 +218,57 @@
1.59 relabel_proof [] 0
1.60 end
1.61
1.62 +fun stutter_single_letter s = String.extract (s, 0, SOME 1) ^ s
1.63 +
1.64 +fun rationalize_obtains_in_isar_proofs ctxt =
1.65 + let
1.66 + fun rename_obtains xs (subst, ctxt) =
1.67 + let
1.68 + val Ts = map snd xs
1.69 + val new_names0 = map (stutter_single_letter o var_name_of_typ o body_type) Ts
1.70 + val (new_names, ctxt') = Variable.variant_fixes new_names0 ctxt
1.71 + val ys = map2 pair new_names Ts
1.72 + in
1.73 + (ys, ((map Free xs ~~ map Free ys) @ subst, ctxt'))
1.74 + end
1.75 +
1.76 + fun rationalize_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) subst_ctxt =
1.77 + let
1.78 + val (xs', subst_ctxt' as (subst', _)) = rename_obtains xs subst_ctxt
1.79 + val t' = subst_atomic subst' t
1.80 + val subs' = map (rationalize_proof false subst_ctxt') subs
1.81 + in
1.82 + (Prove (qs, xs', l, t', subs', facts, meths, comment), subst_ctxt')
1.83 + end
1.84 + and rationalize_proof outer (subst_ctxt as (subst, ctxt)) (Proof (fix, assms, steps)) =
1.85 + let
1.86 + val (fix', subst_ctxt' as (subst', _)) =
1.87 + if outer then
1.88 + (* last call: eliminate any remaining skolem names (from SMT proofs) *)
1.89 + (fix, (subst @ map (fn x => (Free (apfst Name.skolem x), Free x)) fix, ctxt))
1.90 + else
1.91 + rename_obtains fix subst_ctxt
1.92 + in
1.93 + Proof (fix', map (apsnd (subst_atomic subst')) assms,
1.94 + fst (fold_map rationalize_step steps subst_ctxt'))
1.95 + end
1.96 + in
1.97 + rationalize_proof true ([], ctxt)
1.98 + end
1.99 +
1.100 +val thesis_var = ((Auto_Bind.thesisN, 0), HOLogic.boolT)
1.101 +
1.102 +fun is_thesis ctxt t =
1.103 + (case Vartab.lookup (Variable.binds_of ctxt) (fst thesis_var) of
1.104 + SOME (_, t') => HOLogic.mk_Trueprop t' aconv t
1.105 + | NONE => false)
1.106 +
1.107 val indent_size = 2
1.108
1.109 fun string_of_isar_proof ctxt0 i n proof =
1.110 let
1.111 + val keywords = Thy_Header.get_keywords' ctxt0
1.112 +
1.113 (* Make sure only type constraints inserted by the type annotation code are printed. *)
1.114 val ctxt = ctxt0
1.115 |> Config.put show_markup false
1.116 @@ -243,7 +302,7 @@
1.117 |> annotate_types_in_term ctxt
1.118 |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of)
1.119 |> simplify_spaces
1.120 - |> maybe_quote),
1.121 + |> maybe_quote keywords),
1.122 ctxt |> perhaps (try (Variable.auto_fixes term)))
1.123
1.124 fun using_facts [] [] = ""
1.125 @@ -260,8 +319,8 @@
1.126 end
1.127
1.128 fun of_free (s, T) =
1.129 - maybe_quote s ^ " :: " ^
1.130 - maybe_quote (simplify_spaces (with_vanilla_print_mode (Syntax.string_of_typ ctxt) T))
1.131 + maybe_quote keywords s ^ " :: " ^
1.132 + maybe_quote keywords (simplify_spaces (with_vanilla_print_mode (Syntax.string_of_typ ctxt) T))
1.133
1.134 fun add_frees xs (s, ctxt) =
1.135 (s ^ space_implode " and " (map of_free xs), ctxt |> fold Variable.auto_fixes (map Free xs))
1.136 @@ -290,18 +349,20 @@
1.137 and add_step_pre ind qs subs (s, ctxt) =
1.138 (s ^ of_subproofs ind ctxt qs subs ^ of_indent ind, ctxt)
1.139 and add_step ind (Let (t1, t2)) =
1.140 - add_str (of_indent ind ^ "let ")
1.141 - #> add_term t1 #> add_str " = " #> add_term t2 #> add_str "\n"
1.142 + add_str (of_indent ind ^ "let ") #> add_term t1 #> add_str " = " #> add_term t2
1.143 + #> add_str "\n"
1.144 | add_step ind (Prove (qs, xs, l, t, subs, (ls, ss), meth :: _, comment)) =
1.145 add_step_pre ind qs subs
1.146 #> (case xs of
1.147 - [] => add_str (of_have qs (length subs) ^ " ")
1.148 - | _ => add_str (of_obtain qs (length subs) ^ " ") #> add_frees xs #> add_str " where ")
1.149 + [] => add_str (of_have qs (length subs) ^ " ")
1.150 + | _ =>
1.151 + add_str (of_obtain qs (length subs) ^ " ")
1.152 + #> add_frees xs
1.153 + #> add_str (" where\n" ^ of_indent (ind + 1)))
1.154 #> add_str (of_label l)
1.155 - #> add_term t
1.156 - #> add_str (" " ^
1.157 - of_method (sort_distinct label_ord ls) (sort_distinct string_ord ss) meth ^
1.158 - (if comment = "" then "" else " (* " ^ comment ^ " *)") ^ "\n")
1.159 + #> add_term (if is_thesis ctxt t then HOLogic.mk_Trueprop (Var thesis_var) else t)
1.160 + #> add_str ("\n" ^ of_indent (ind + 1) ^ of_method ls ss meth ^
1.161 + (if comment = "" then "" else " (* " ^ comment ^ " *)") ^ "\n")
1.162 and add_steps ind = fold (add_step ind)
1.163 and of_proof ind ctxt (Proof (xs, assms, steps)) =
1.164 ("", ctxt)