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