src/Pure/Isar/auto_bind.ML
author wenzelm
Sat Jan 07 12:26:29 2006 +0100 (2006-01-07)
changeset 18605 b971e113dee7
parent 18472 255eaf0a2119
child 19075 12833c7e0fa6
permissions -rw-r--r--
RuleCases.make_simple;
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@17852
    16
  val no_facts: (indexname * term option) list
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@17349
    24
val rule_contextN = "rule_context";
wenzelm@10359
    25
val thesisN = "thesis";
wenzelm@10359
    26
val thisN = "this";
wenzelm@10359
    27
wenzelm@17349
    28
fun strip_judgment thy = ObjectLogic.drop_judgment thy o Logic.strip_assums_concl;
wenzelm@11764
    29
wenzelm@17349
    30
fun statement_binds thy name prop =
wenzelm@17349
    31
  [((name, 0), SOME (Term.list_abs (Logic.strip_params prop, strip_judgment thy prop)))];
wenzelm@10359
    32
wenzelm@10359
    33
wenzelm@10359
    34
(* goal *)
wenzelm@10359
    35
wenzelm@17349
    36
fun goal thy [prop] = statement_binds thy thesisN prop
skalberg@15531
    37
  | goal _ _ = [((thesisN, 0), NONE)];
wenzelm@10359
    38
wenzelm@18605
    39
fun cases thy [prop] = RuleCases.make_simple true (thy, prop) rule_contextN
wenzelm@18605
    40
  | cases _ _ = [(rule_contextN, NONE)];
wenzelm@17349
    41
wenzelm@10359
    42
wenzelm@10359
    43
(* facts *)
wenzelm@10359
    44
wenzelm@17349
    45
fun get_arg thy prop =
wenzelm@17349
    46
  (case strip_judgment thy prop of
skalberg@15531
    47
    _ $ t => SOME (Term.list_abs (Logic.strip_params prop, t))
skalberg@15531
    48
  | _ => NONE);
wenzelm@10359
    49
wenzelm@12140
    50
fun facts _ [] = []
wenzelm@17349
    51
  | facts thy props =
wenzelm@10359
    52
      let val prop = Library.last_elem props
wenzelm@17349
    53
      in [(Syntax.dddot_indexname, get_arg thy prop)] @ statement_binds thy thisN prop end;
wenzelm@10359
    54
wenzelm@17852
    55
val no_facts = [(Syntax.dddot_indexname, NONE), ((thisN, 0), NONE)];
wenzelm@10808
    56
wenzelm@6783
    57
end;