more concise Isar output
authorblanchet
Fri Jan 31 18:43:16 2014 +0100 (2014-01-31)
changeset 5521677953325d5f1
parent 55215 b6c926e67350
child 55217 70035950e19b
more concise Isar output
src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 16:58:58 2014 +0000
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 18:43:16 2014 +0100
     1.3 @@ -160,7 +160,7 @@
     1.4  
     1.5      val register_fixes = map Free #> fold Variable.auto_fixes
     1.6  
     1.7 -    fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt)
     1.8 +    fun add_str s' = apfst (suffix s')
     1.9  
    1.10      fun of_indent ind = replicate_string (ind * indent_size) " "
    1.11      fun of_moreover ind = of_indent ind ^ "moreover\n"
    1.12 @@ -215,14 +215,6 @@
    1.13        | of_method ls ss Meson_Method = using_facts ls [] ^ by_facts "meson" [] ss
    1.14        | of_method ls ss meth = using_facts ls ss ^ by_method meth
    1.15  
    1.16 -    fun of_byline ind (ls, ss) meth =
    1.17 -      let
    1.18 -        val ls = ls |> sort_distinct label_ord
    1.19 -        val ss = ss |> sort_distinct string_ord
    1.20 -      in
    1.21 -        "\n" ^ of_indent (ind + 1) ^ of_method ls ss meth
    1.22 -      end
    1.23 -
    1.24      fun of_free (s, T) =
    1.25        maybe_quote s ^ " :: " ^
    1.26        maybe_quote (simplify_spaces (with_vanilla_print_mode (Syntax.string_of_typ ctxt) T))
    1.27 @@ -232,21 +224,22 @@
    1.28  
    1.29      fun add_fix _ [] = I
    1.30        | add_fix ind xs =
    1.31 -        add_suffix (of_indent ind ^ "fix ")
    1.32 +        add_str (of_indent ind ^ "fix ")
    1.33          #> add_frees xs
    1.34 -        #> add_suffix "\n"
    1.35 +        #> add_str "\n"
    1.36  
    1.37      fun add_assm ind (l, t) =
    1.38 -      add_suffix (of_indent ind ^ "assume " ^ of_label l)
    1.39 +      add_str (of_indent ind ^ "assume " ^ of_label l)
    1.40        #> add_term t
    1.41 -      #> add_suffix "\n"
    1.42 +      #> add_str "\n"
    1.43  
    1.44      fun add_assms ind assms = fold (add_assm ind) assms
    1.45  
    1.46 -    fun add_step_post ind l t facts meth =
    1.47 -      add_suffix (of_label l)
    1.48 +    fun add_step_post ind l t (ls, ss) meth =
    1.49 +      add_str (of_label l)
    1.50        #> add_term t
    1.51 -      #> add_suffix (of_byline ind facts meth ^ "\n")
    1.52 +      #> add_str (" " ^
    1.53 +           of_method (sort_distinct label_ord ls) (sort_distinct string_ord ss) meth ^ "\n")
    1.54  
    1.55      fun of_subproof ind ctxt proof =
    1.56        let
    1.57 @@ -266,19 +259,15 @@
    1.58      and add_step_pre ind qs subproofs (s, ctxt) =
    1.59        (s ^ of_subproofs ind ctxt qs subproofs ^ of_indent ind, ctxt)
    1.60      and add_step ind (Let (t1, t2)) =
    1.61 -        add_suffix (of_indent ind ^ "let ")
    1.62 -        #> add_term t1
    1.63 -        #> add_suffix " = "
    1.64 -        #> add_term t2
    1.65 -        #> add_suffix "\n"
    1.66 +        add_str (of_indent ind ^ "let ")
    1.67 +        #> add_term t1 #> add_str " = " #> add_term t2
    1.68 +        #> add_str "\n"
    1.69        | add_step ind (Prove (qs, xs, l, t, subproofs, (facts, (meth :: _) :: _))) =
    1.70          add_step_pre ind qs subproofs
    1.71          #> (case xs of
    1.72 -            [] => add_suffix (of_have qs (length subproofs) ^ " ")
    1.73 -          | _ =>
    1.74 -            add_suffix (of_obtain qs (length subproofs) ^ " ")
    1.75 -            #> add_frees xs
    1.76 -            #> add_suffix " where ")
    1.77 +             [] => add_str (of_have qs (length subproofs) ^ " ")
    1.78 +           | _ =>
    1.79 +             add_str (of_obtain qs (length subproofs) ^ " ") #> add_frees xs #> add_str " where ")
    1.80          #> add_step_post ind l t facts meth
    1.81      and add_steps ind = fold (add_step ind)
    1.82      and of_proof ind ctxt (Proof (xs, assms, steps)) =