src/Pure/Isar/auto_bind.ML
author wenzelm
Sun Nov 11 21:32:12 2001 +0100 (2001-11-11 ago)
changeset 12140 a987beab002d
parent 11764 fd780dd6e0b4
child 12241 c4a2a0686238
permissions -rw-r--r--
facts: multiple args;
wenzelm@6783
     1
(*  Title:      Pure/Isar/auto_bind.ML
wenzelm@6783
     2
    ID:         $Id$
wenzelm@6783
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@8807
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@6783
     5
wenzelm@10359
     6
Logic specific patterns and automatic term bindings.
wenzelm@7675
     7
wenzelm@8227
     8
Note: the current implementation is not quite 'generic', but works
wenzelm@10359
     9
fine with common object-logics (HOL, FOL, ZF etc.).
wenzelm@6783
    10
*)
wenzelm@6783
    11
wenzelm@6783
    12
signature AUTO_BIND =
wenzelm@6783
    13
sig
wenzelm@12140
    14
  val goal: Sign.sg -> term list -> (indexname * term option) list
wenzelm@12140
    15
  val facts: Sign.sg -> term list -> (indexname * term option) list
wenzelm@9296
    16
  val thesisN: string
wenzelm@6783
    17
end;
wenzelm@6783
    18
wenzelm@6783
    19
structure AutoBind: AUTO_BIND =
wenzelm@6783
    20
struct
wenzelm@6783
    21
wenzelm@10359
    22
(** bindings **)
wenzelm@10359
    23
wenzelm@10359
    24
val thesisN = "thesis";
wenzelm@10359
    25
val thisN = "this";
wenzelm@10359
    26
wenzelm@11764
    27
fun strip_judgment sg = ObjectLogic.drop_judgment sg o Logic.strip_assums_concl;
wenzelm@11764
    28
wenzelm@11764
    29
fun statement_binds sg name prop =
wenzelm@11764
    30
  [((name, 0), Some (Term.list_abs (Logic.strip_params prop, strip_judgment sg prop)))];
wenzelm@10359
    31
wenzelm@10359
    32
wenzelm@10359
    33
(* goal *)
wenzelm@10359
    34
wenzelm@12140
    35
fun goal sg props = statement_binds sg thesisN (Library.last_elem props);
wenzelm@10359
    36
wenzelm@10359
    37
wenzelm@10359
    38
(* facts *)
wenzelm@10359
    39
wenzelm@11764
    40
fun get_arg sg prop =
wenzelm@11764
    41
  (case strip_judgment sg prop of
wenzelm@10808
    42
    _ $ t => Some (Term.list_abs (Logic.strip_params prop, t))
wenzelm@10359
    43
  | _ => None);
wenzelm@10359
    44
wenzelm@12140
    45
fun facts _ [] = []
wenzelm@12140
    46
  | facts sg props =
wenzelm@10359
    47
      let val prop = Library.last_elem props
wenzelm@11764
    48
      in [(Syntax.dddot_indexname, get_arg sg prop)] @ statement_binds sg thisN prop end;
wenzelm@10359
    49
wenzelm@10808
    50
wenzelm@6783
    51
end;