src/Pure/Isar/auto_bind.ML
author wenzelm
Mon Oct 30 18:25:38 2000 +0100 (2000-10-30)
changeset 10359 445e3b87f28b
parent 9464 e290583864e4
child 10377 6b595f9ae37e
permissions -rw-r--r--
improved statement bindings for props;
tuned;
wenzelm@6783
     1
(*  Title:      Pure/Isar/auto_bind.ML
wenzelm@6783
     2
    ID:         $Id$
wenzelm@6783
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@8807
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@6783
     5
wenzelm@10359
     6
Logic specific patterns and automatic term bindings.
wenzelm@7675
     7
wenzelm@8227
     8
Note: the current implementation is not quite 'generic', but works
wenzelm@10359
     9
fine with common object-logics (HOL, FOL, ZF etc.).
wenzelm@6783
    10
*)
wenzelm@6783
    11
wenzelm@6783
    12
signature AUTO_BIND =
wenzelm@6783
    13
sig
wenzelm@10359
    14
  val is_judgment: term -> bool
wenzelm@10359
    15
  val add_judgment: bstring * string * mixfix -> theory -> theory
wenzelm@10359
    16
  val add_judgment_i: bstring * typ * mixfix -> theory -> theory
wenzelm@7599
    17
  val goal: term -> (indexname * term option) list
wenzelm@7599
    18
  val facts: string -> term list -> (indexname * term option) list
wenzelm@9296
    19
  val thesisN: string
wenzelm@6783
    20
end;
wenzelm@6783
    21
wenzelm@6783
    22
structure AutoBind: AUTO_BIND =
wenzelm@6783
    23
struct
wenzelm@6783
    24
wenzelm@9464
    25
wenzelm@9464
    26
(** judgments **)
wenzelm@7675
    27
wenzelm@10359
    28
fun strip_judgment prop =
wenzelm@10359
    29
  (case (Logic.strip_assums_concl prop) of
wenzelm@10359
    30
    Const ("Trueprop", _) $ t => t
wenzelm@10359
    31
  | t => t);
wenzelm@10359
    32
wenzelm@9464
    33
fun is_judgment (Const ("Trueprop", _) $ _) = true
wenzelm@9464
    34
  | is_judgment _ = false;
wenzelm@8227
    35
wenzelm@8227
    36
wenzelm@9464
    37
fun gen_add_judgment add (name, T, syn) thy =
wenzelm@9464
    38
  if name = "Trueprop" then
wenzelm@9464
    39
    thy |> PureThy.global_path |> add [(name, T, syn)] |> PureThy.local_path
wenzelm@9464
    40
  else error "Judgment name has to be \"Trueprop\"";
wenzelm@8227
    41
wenzelm@8227
    42
val add_judgment = gen_add_judgment Theory.add_consts;
wenzelm@8227
    43
val add_judgment_i = gen_add_judgment Theory.add_consts_i;
wenzelm@8227
    44
wenzelm@6796
    45
wenzelm@10359
    46
wenzelm@10359
    47
(** bindings **)
wenzelm@10359
    48
wenzelm@10359
    49
val thesisN = "thesis";
wenzelm@10359
    50
val thisN = "this";
wenzelm@10359
    51
wenzelm@10359
    52
fun list_abs parms tm = foldr (fn ((x, T), t) => Abs (x, T, t)) (parms, tm);
wenzelm@10359
    53
wenzelm@10359
    54
fun statement_binds name prop =
wenzelm@10359
    55
  [((name, 0), Some (list_abs (Logic.strip_params prop) (strip_judgment prop)))];
wenzelm@10359
    56
wenzelm@10359
    57
wenzelm@10359
    58
(* goal *)
wenzelm@10359
    59
wenzelm@10359
    60
fun goal prop = statement_binds thesisN prop;
wenzelm@10359
    61
wenzelm@10359
    62
wenzelm@10359
    63
(* facts *)
wenzelm@10359
    64
wenzelm@10359
    65
fun get_arg prop =
wenzelm@10359
    66
  (case strip_judgment prop of
wenzelm@10359
    67
    _ $ t => Some (list_abs (Logic.strip_params prop) t)
wenzelm@10359
    68
  | _ => None);
wenzelm@10359
    69
wenzelm@10359
    70
fun facts _ [] = []
wenzelm@10359
    71
  | facts name props =
wenzelm@10359
    72
      let val prop = Library.last_elem props
wenzelm@10359
    73
      in [(Syntax.dddot_indexname, get_arg prop)] @ statement_binds thisN prop end;
wenzelm@10359
    74
wenzelm@6783
    75
end;