src/Pure/Isar/auto_bind.ML
author skalberg
Sun Feb 13 17:15:14 2005 +0100 (2005-02-13)
changeset 15531 08c8dad8e399
parent 14981 e73f8140af78
child 17349 03fafcdfdfa7
permissions -rw-r--r--
Deleted Library.option type.
wenzelm@6783
     1
(*  Title:      Pure/Isar/auto_bind.ML
wenzelm@6783
     2
    ID:         $Id$
wenzelm@6783
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6783
     4
wenzelm@10359
     5
Logic specific patterns and automatic term bindings.
wenzelm@6783
     6
*)
wenzelm@6783
     7
wenzelm@6783
     8
signature AUTO_BIND =
wenzelm@6783
     9
sig
wenzelm@12140
    10
  val goal: Sign.sg -> term list -> (indexname * term option) list
wenzelm@12140
    11
  val facts: Sign.sg -> term list -> (indexname * term option) list
wenzelm@9296
    12
  val thesisN: string
wenzelm@6783
    13
end;
wenzelm@6783
    14
wenzelm@6783
    15
structure AutoBind: AUTO_BIND =
wenzelm@6783
    16
struct
wenzelm@6783
    17
wenzelm@10359
    18
(** bindings **)
wenzelm@10359
    19
wenzelm@10359
    20
val thesisN = "thesis";
wenzelm@10359
    21
val thisN = "this";
wenzelm@10359
    22
wenzelm@11764
    23
fun strip_judgment sg = ObjectLogic.drop_judgment sg o Logic.strip_assums_concl;
wenzelm@11764
    24
wenzelm@11764
    25
fun statement_binds sg name prop =
skalberg@15531
    26
  [((name, 0), SOME (Term.list_abs (Logic.strip_params prop, strip_judgment sg prop)))];
wenzelm@10359
    27
wenzelm@10359
    28
wenzelm@10359
    29
(* goal *)
wenzelm@10359
    30
wenzelm@12241
    31
fun goal sg [prop] = statement_binds sg thesisN prop
skalberg@15531
    32
  | goal _ _ = [((thesisN, 0), NONE)];
wenzelm@10359
    33
wenzelm@10359
    34
wenzelm@10359
    35
(* facts *)
wenzelm@10359
    36
wenzelm@11764
    37
fun get_arg sg prop =
wenzelm@11764
    38
  (case strip_judgment sg prop of
skalberg@15531
    39
    _ $ t => SOME (Term.list_abs (Logic.strip_params prop, t))
skalberg@15531
    40
  | _ => NONE);
wenzelm@10359
    41
wenzelm@12140
    42
fun facts _ [] = []
wenzelm@12140
    43
  | facts sg props =
wenzelm@10359
    44
      let val prop = Library.last_elem props
wenzelm@11764
    45
      in [(Syntax.dddot_indexname, get_arg sg prop)] @ statement_binds sg thisN prop end;
wenzelm@10359
    46
wenzelm@10808
    47
wenzelm@6783
    48
end;