src/Pure/Isar/auto_bind.ML
author wenzelm
Tue Dec 05 22:14:42 2006 +0100 (2006-12-05)
changeset 21658 5e31241e1e3c
parent 21448 09c953c07008
child 26686 9f3f5429bac6
permissions -rw-r--r--
Attrib.internal: morphism;
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@19075
    13
  val premsN: string
wenzelm@21448
    14
  val assmsN: string
wenzelm@17349
    15
  val goal: theory -> term list -> (indexname * term option) list
wenzelm@17349
    16
  val cases: theory -> term list -> (string * RuleCases.T option) list
wenzelm@17349
    17
  val facts: theory -> term list -> (indexname * term option) list
wenzelm@17852
    18
  val no_facts: (indexname * term option) list
wenzelm@6783
    19
end;
wenzelm@6783
    20
wenzelm@6783
    21
structure AutoBind: AUTO_BIND =
wenzelm@6783
    22
struct
wenzelm@6783
    23
wenzelm@10359
    24
(** bindings **)
wenzelm@10359
    25
wenzelm@17349
    26
val rule_contextN = "rule_context";
wenzelm@10359
    27
val thesisN = "thesis";
wenzelm@10359
    28
val thisN = "this";
wenzelm@19075
    29
val premsN = "prems";
wenzelm@21448
    30
val assmsN = "assms";
wenzelm@10359
    31
wenzelm@17349
    32
fun strip_judgment thy = ObjectLogic.drop_judgment thy o Logic.strip_assums_concl;
wenzelm@11764
    33
wenzelm@17349
    34
fun statement_binds thy name prop =
wenzelm@17349
    35
  [((name, 0), SOME (Term.list_abs (Logic.strip_params prop, strip_judgment thy prop)))];
wenzelm@10359
    36
wenzelm@10359
    37
wenzelm@10359
    38
(* goal *)
wenzelm@10359
    39
wenzelm@17349
    40
fun goal thy [prop] = statement_binds thy thesisN prop
skalberg@15531
    41
  | goal _ _ = [((thesisN, 0), NONE)];
wenzelm@10359
    42
wenzelm@18605
    43
fun cases thy [prop] = RuleCases.make_simple true (thy, prop) rule_contextN
wenzelm@18605
    44
  | cases _ _ = [(rule_contextN, NONE)];
wenzelm@17349
    45
wenzelm@10359
    46
wenzelm@10359
    47
(* facts *)
wenzelm@10359
    48
wenzelm@17349
    49
fun get_arg thy prop =
wenzelm@17349
    50
  (case strip_judgment thy prop of
skalberg@15531
    51
    _ $ t => SOME (Term.list_abs (Logic.strip_params prop, t))
skalberg@15531
    52
  | _ => NONE);
wenzelm@10359
    53
wenzelm@12140
    54
fun facts _ [] = []
wenzelm@17349
    55
  | facts thy props =
wenzelm@10359
    56
      let val prop = Library.last_elem props
wenzelm@17349
    57
      in [(Syntax.dddot_indexname, get_arg thy prop)] @ statement_binds thy thisN prop end;
wenzelm@10359
    58
wenzelm@17852
    59
val no_facts = [(Syntax.dddot_indexname, NONE), ((thisN, 0), NONE)];
wenzelm@10808
    60
wenzelm@6783
    61
end;