src/Pure/Isar/auto_bind.ML
author wenzelm
Tue Sep 13 22:19:33 2005 +0200 (2005-09-13 ago)
changeset 17349 03fafcdfdfa7
parent 15531 08c8dad8e399
child 17852 a06b185a26d7
permissions -rw-r--r--
added cases, rule_contextN;
eliminated obsolete Sign.sg;
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@17349
     5
Automatic bindings of Isar text elements.
wenzelm@6783
     6
*)
wenzelm@6783
     7
wenzelm@6783
     8
signature AUTO_BIND =
wenzelm@6783
     9
sig
wenzelm@17349
    10
  val rule_contextN: string
wenzelm@9296
    11
  val thesisN: string
wenzelm@17349
    12
  val thisN: string
wenzelm@17349
    13
  val goal: theory -> term list -> (indexname * term option) list
wenzelm@17349
    14
  val cases: theory -> term list -> (string * RuleCases.T option) list
wenzelm@17349
    15
  val facts: theory -> term list -> (indexname * term option) list
wenzelm@6783
    16
end;
wenzelm@6783
    17
wenzelm@6783
    18
structure AutoBind: AUTO_BIND =
wenzelm@6783
    19
struct
wenzelm@6783
    20
wenzelm@10359
    21
(** bindings **)
wenzelm@10359
    22
wenzelm@17349
    23
val rule_contextN = "rule_context";
wenzelm@10359
    24
val thesisN = "thesis";
wenzelm@10359
    25
val thisN = "this";
wenzelm@10359
    26
wenzelm@17349
    27
fun strip_judgment thy = ObjectLogic.drop_judgment thy o Logic.strip_assums_concl;
wenzelm@11764
    28
wenzelm@17349
    29
fun statement_binds thy name prop =
wenzelm@17349
    30
  [((name, 0), SOME (Term.list_abs (Logic.strip_params prop, strip_judgment thy prop)))];
wenzelm@10359
    31
wenzelm@10359
    32
wenzelm@10359
    33
(* goal *)
wenzelm@10359
    34
wenzelm@17349
    35
fun goal thy [prop] = statement_binds thy thesisN prop
skalberg@15531
    36
  | goal _ _ = [((thesisN, 0), NONE)];
wenzelm@10359
    37
wenzelm@17349
    38
fun cases thy [prop] = [RuleCases.simple true (thy, prop) rule_contextN]
wenzelm@17349
    39
  | cases _ _ = [(rule_contextN, NONE)];
wenzelm@17349
    40
wenzelm@10359
    41
wenzelm@10359
    42
(* facts *)
wenzelm@10359
    43
wenzelm@17349
    44
fun get_arg thy prop =
wenzelm@17349
    45
  (case strip_judgment thy prop of
skalberg@15531
    46
    _ $ t => SOME (Term.list_abs (Logic.strip_params prop, t))
skalberg@15531
    47
  | _ => NONE);
wenzelm@10359
    48
wenzelm@12140
    49
fun facts _ [] = []
wenzelm@17349
    50
  | facts thy props =
wenzelm@10359
    51
      let val prop = Library.last_elem props
wenzelm@17349
    52
      in [(Syntax.dddot_indexname, get_arg thy prop)] @ statement_binds thy thisN prop end;
wenzelm@10359
    53
wenzelm@10808
    54
wenzelm@6783
    55
end;