src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML

tuned: cleaned up data structure

(*  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 (* local & global facts *)

  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 |
  (* for |fix|>0, this is an obtain step; step may contain subproofs *)
  Prove of isar_qualifier list * fix * label * term * isar_proof list * byline
  and byline =
    By_Metis of facts

  val no_label : label
  val no_facts : facts

  val string_of_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 subproofs_of_step : isar_step -> isar_proof list option
  val byline_of_step : isar_step -> byline option

  val fold_isar_step : (isar_step -> 'a -> 'a) -> isar_step -> 'a -> 'a
  val fold_isar_steps :
    (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a

  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 (* local & global facts *)

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 |
  (* for |fix|>0, this is an obtain step; step may contain subproofs *)
  Prove of isar_qualifier list * fix * label * term * isar_proof list * byline
and byline =
  By_Metis of facts

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

fun string_of_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 label_of_step (Prove (_, _, l, _, _, _)) = SOME l
  | label_of_step _ = NONE

fun subproofs_of_step (Prove (_, _, _, _, subproofs, _)) = SOME subproofs
  | subproofs_of_step _ = NONE

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

fun fold_isar_step f step s =
  fold (steps_of_proof #> fold (fold_isar_step f))
    (the_default [] (subproofs_of_step step)) s
    |> f step

fun fold_isar_steps f = fold (fold_isar_step f)

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

val add_metis_steps =
  fold_isar_steps
    (byline_of_step #> (fn SOME (By_Metis _) => Integer.add 1 | _ => I))
end