src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML
author blanchet
Wed Dec 12 21:48:29 2012 +0100 (2012-12-12 ago)
changeset 50510 7e4f2f8d9b50
parent 50269 20a01c3e8072
child 50672 ab5b8b5c9cbe
permissions -rw-r--r--
export a pair of ML functions
smolkas@50264
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_proof.ML
smolkas@50263
     2
    Author:     Jasmin Blanchette, TU Muenchen
smolkas@50263
     3
    Author:     Steffen Juilf Smolka, TU Muenchen
smolkas@50263
     4
smolkas@50263
     5
Basic data structures for representing and basic methods
smolkas@50263
     6
for dealing with Isar proof texts.
smolkas@50263
     7
*)
smolkas@50263
     8
smolkas@50268
     9
signature SLEDGEHAMMER_PROOF =
smolkas@50259
    10
sig
smolkas@50268
    11
	type label = string * int
smolkas@50268
    12
  type facts = label list * string list
smolkas@50268
    13
smolkas@50268
    14
  datatype isar_qualifier = Show | Then | Ultimately
smolkas@50268
    15
smolkas@50268
    16
  datatype isar_step =
smolkas@50268
    17
    Fix of (string * typ) list |
smolkas@50268
    18
    Let of term * term |
smolkas@50268
    19
    Assume of label * term |
smolkas@50268
    20
    Prove of isar_qualifier list * label * term * byline
smolkas@50268
    21
  and byline =
smolkas@50268
    22
    By_Metis of facts |
smolkas@50268
    23
    Case_Split of isar_step list list * facts
smolkas@50268
    24
smolkas@50268
    25
  val string_for_label : label -> string
smolkas@50268
    26
  val metis_steps_top_level : isar_step list -> int
smolkas@50269
    27
  val metis_steps_total : isar_step list -> int
smolkas@50259
    28
end
smolkas@50259
    29
smolkas@50268
    30
structure Sledgehammer_Proof : SLEDGEHAMMER_PROOF = 
smolkas@50259
    31
struct
smolkas@50259
    32
smolkas@50259
    33
type label = string * int
smolkas@50259
    34
type facts = label list * string list
smolkas@50259
    35
smolkas@50260
    36
datatype isar_qualifier = Show | Then | Ultimately
smolkas@50259
    37
smolkas@50259
    38
datatype isar_step =
smolkas@50259
    39
  Fix of (string * typ) list |
smolkas@50259
    40
  Let of term * term |
smolkas@50259
    41
  Assume of label * term |
smolkas@50259
    42
  Prove of isar_qualifier list * label * term * byline
smolkas@50259
    43
and byline =
smolkas@50259
    44
  By_Metis of facts |
smolkas@50259
    45
  Case_Split of isar_step list list * facts
smolkas@50259
    46
smolkas@50259
    47
fun string_for_label (s, num) = s ^ string_of_int num
smolkas@50259
    48
smolkas@50259
    49
val inc = curry op+
smolkas@50259
    50
fun metis_steps_top_level proof = fold (fn Prove _ => inc 1 | _ => I) proof 0
smolkas@50269
    51
fun metis_steps_total proof = 
smolkas@50259
    52
  fold (fn Prove (_,_,_, By_Metis _) => inc 1
smolkas@50259
    53
         | Prove (_,_,_, Case_Split (cases, _)) => 
smolkas@50269
    54
           inc (fold (inc o metis_steps_total) cases 1)
smolkas@50259
    55
         | _ => I) proof 0
smolkas@50259
    56
smolkas@50260
    57
end