src/Pure/Isar/auto_bind.ML
author wenzelm
Sun Mar 07 12:19:47 2010 +0100 (2010-03-07)
changeset 35625 9c818cab0dd0
parent 33386 ff29d1549aca
child 41489 8e2b8649507d
permissions -rw-r--r--
modernized structure Object_Logic;
wenzelm@6783
     1
(*  Title:      Pure/Isar/auto_bind.ML
wenzelm@6783
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6783
     3
wenzelm@17349
     4
Automatic bindings of Isar text elements.
wenzelm@6783
     5
*)
wenzelm@6783
     6
wenzelm@6783
     7
signature AUTO_BIND =
wenzelm@6783
     8
sig
wenzelm@9296
     9
  val thesisN: string
wenzelm@17349
    10
  val thisN: string
wenzelm@21448
    11
  val assmsN: string
wenzelm@17349
    12
  val goal: theory -> term list -> (indexname * term option) list
wenzelm@17349
    13
  val facts: theory -> term list -> (indexname * term option) list
wenzelm@17852
    14
  val no_facts: (indexname * term option) list
wenzelm@6783
    15
end;
wenzelm@6783
    16
wenzelm@33386
    17
structure Auto_Bind: AUTO_BIND =
wenzelm@6783
    18
struct
wenzelm@6783
    19
wenzelm@10359
    20
(** bindings **)
wenzelm@10359
    21
wenzelm@10359
    22
val thesisN = "thesis";
wenzelm@10359
    23
val thisN = "this";
wenzelm@21448
    24
val assmsN = "assms";
wenzelm@10359
    25
wenzelm@35625
    26
fun strip_judgment thy = Object_Logic.drop_judgment thy o Logic.strip_assums_concl;
wenzelm@11764
    27
wenzelm@17349
    28
fun statement_binds thy name prop =
wenzelm@17349
    29
  [((name, 0), SOME (Term.list_abs (Logic.strip_params prop, strip_judgment thy prop)))];
wenzelm@10359
    30
wenzelm@10359
    31
wenzelm@10359
    32
(* goal *)
wenzelm@10359
    33
wenzelm@17349
    34
fun goal thy [prop] = statement_binds thy thesisN prop
skalberg@15531
    35
  | goal _ _ = [((thesisN, 0), NONE)];
wenzelm@10359
    36
wenzelm@10359
    37
wenzelm@10359
    38
(* facts *)
wenzelm@10359
    39
wenzelm@17349
    40
fun get_arg thy prop =
wenzelm@17349
    41
  (case strip_judgment thy prop of
skalberg@15531
    42
    _ $ t => SOME (Term.list_abs (Logic.strip_params prop, t))
skalberg@15531
    43
  | _ => NONE);
wenzelm@10359
    44
wenzelm@12140
    45
fun facts _ [] = []
wenzelm@17349
    46
  | facts thy props =
wenzelm@10359
    47
      let val prop = Library.last_elem props
wenzelm@17349
    48
      in [(Syntax.dddot_indexname, get_arg thy prop)] @ statement_binds thy thisN prop end;
wenzelm@10359
    49
wenzelm@17852
    50
val no_facts = [(Syntax.dddot_indexname, NONE), ((thisN, 0), NONE)];
wenzelm@10808
    51
wenzelm@6783
    52
end;