src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML

eliminated hard tabs;

(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_proof.ML
    Author:     Jasmin Blanchette, TU Muenchen
    Author:     Steffen Juilf Smolka, TU Muenchen

Basic data structures for representing and basic methods
for dealing with Isar proof texts.
*)

signature SLEDGEHAMMER_PROOF =
sig
  type label = string * int
  type facts = label list * string list

  datatype isar_qualifier = Show | Then

  datatype fix = Fix of (string * typ) list
  datatype assms = Assume of (label * term) list

  datatype isar_proof = 
    Proof of fix * assms * isar_step list
  and isar_step =
    Let of term * term |
    Prove of isar_qualifier list * label * term * byline |
    Obtain of isar_qualifier list * fix * label * term * byline
  and byline =
    By_Metis of isar_proof list * facts

  val no_label : label
  val no_facts : facts

  val string_for_label : label -> string
  val fix_of_proof : isar_proof -> fix
  val assms_of_proof : isar_proof -> assms
  val steps_of_proof : isar_proof -> isar_step list

  val label_of_step : isar_step -> label option
  val byline_of_step : isar_step -> byline option

  val add_metis_steps_top_level : isar_step list -> int -> int
  val add_metis_steps : isar_step list -> int -> int
end

structure Sledgehammer_Proof : SLEDGEHAMMER_PROOF =
struct

type label = string * int
type facts = label list * string list

datatype isar_qualifier = Show | Then

datatype fix = Fix of (string * typ) list
datatype assms = Assume of (label * term) list

datatype isar_proof = 
  Proof of fix * assms * isar_step list
and isar_step =
  Let of term * term |
  Prove of isar_qualifier list * label * term * byline |
  Obtain of isar_qualifier list * fix * label * term * byline
and byline =
  By_Metis of isar_proof list * facts

val no_label = ("", ~1)
val no_facts = ([],[])

fun string_for_label (s, num) = s ^ string_of_int num

fun fix_of_proof (Proof (fix, _, _)) = fix
fun assms_of_proof (Proof (_, assms, _)) = assms
fun steps_of_proof (Proof (_, _, steps)) = steps
(*fun map_steps_of_proof f (Proof (fix, assms, steps)) =
  Proof(fix, assms, f steps)*)

fun label_of_step (Obtain (_, _, l, _, _)) = SOME l
  | label_of_step (Prove (_, l, _, _)) = SOME l
  | label_of_step _ = NONE

fun byline_of_step (Obtain (_, _, _, _, byline)) = SOME byline
  | byline_of_step (Prove (_, _, _, byline)) = SOME byline
  | byline_of_step _ = NONE

val add_metis_steps_top_level =
  fold (byline_of_step #> (fn SOME (By_Metis _) => Integer.add 1 | _ => I))

fun add_metis_steps steps =
  fold (byline_of_step 
        #> (fn SOME (By_Metis (subproofs, _)) =>
                Integer.add 1 #> add_substeps subproofs
             | _ => I)) steps
and add_substeps subproofs = fold (steps_of_proof #> add_metis_steps) subproofs

end