src/Pure/Isar/auto_bind.ML
author wenzelm
Thu Jul 13 11:41:06 2000 +0200 (2000-07-13)
changeset 9296 0d2b31e1ea1b
parent 8807 0046be1769f9
child 9464 e290583864e4
permissions -rw-r--r--
export thesisN separately;
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@6783
     6
Automatic term bindings -- logic specific patterns.
wenzelm@7675
     7
wenzelm@8227
     8
Note: the current implementation is not quite 'generic', but works
wenzelm@8227
     9
fine with the more common object-logics (HOL, FOL, ZF etc.).
wenzelm@6783
    10
*)
wenzelm@6783
    11
wenzelm@6783
    12
signature AUTO_BIND =
wenzelm@6783
    13
sig
wenzelm@7599
    14
  val goal: term -> (indexname * term option) list
wenzelm@7599
    15
  val facts: string -> term list -> (indexname * term option) list
wenzelm@9296
    16
  val thesisN: string
wenzelm@9296
    17
  val atomic_thesis: term -> term * term
wenzelm@8227
    18
  val add_judgment: bstring * string * mixfix -> theory -> theory
wenzelm@8227
    19
  val add_judgment_i: bstring * typ * mixfix -> theory -> theory
wenzelm@6783
    20
end;
wenzelm@6783
    21
wenzelm@6783
    22
structure AutoBind: AUTO_BIND =
wenzelm@6783
    23
struct
wenzelm@6783
    24
wenzelm@7675
    25
val thesisN = "thesis";
wenzelm@7675
    26
val thisN = "this";
wenzelm@6796
    27
wenzelm@7675
    28
wenzelm@8227
    29
(** bindings **)
wenzelm@8227
    30
wenzelm@8612
    31
fun list_abs parms tm = foldr (fn ((x, T), t) => Abs (x, T, t)) (parms, tm);
wenzelm@8612
    32
wenzelm@8612
    33
wenzelm@7675
    34
(* goal *)
wenzelm@6783
    35
wenzelm@6796
    36
fun statement_binds (name, prop) =
wenzelm@6796
    37
  let
wenzelm@7331
    38
    val concl = Logic.strip_assums_concl prop;
wenzelm@7331
    39
    val parms = Logic.strip_params prop;
wenzelm@7331
    40
wenzelm@8612
    41
    val env = [(name ^ "_prop", Some prop), (name ^ "_concl", Some (list_abs parms concl)),
wenzelm@8612
    42
      (name, case concl of Const ("Trueprop", _) $ t => Some (list_abs parms t) | _ => None)];
wenzelm@7474
    43
  in map (fn (s, t) => ((s, 0), t)) env end;
wenzelm@6783
    44
wenzelm@7675
    45
fun goal prop = statement_binds (thesisN, prop);
wenzelm@6783
    46
wenzelm@6783
    47
wenzelm@6796
    48
(* facts *)
wenzelm@6796
    49
wenzelm@8612
    50
fun get_subject prop =
wenzelm@8612
    51
  (case (Logic.strip_assums_concl prop) of
wenzelm@8612
    52
    Const ("Trueprop", _) $ (_ $ t) => Some (list_abs (Logic.strip_params prop) t)
wenzelm@8612
    53
  | _ => None);
wenzelm@6796
    54
wenzelm@6796
    55
fun facts _ [] = []
wenzelm@7452
    56
  | facts name props =
wenzelm@7452
    57
      let val prop = Library.last_elem props
wenzelm@8612
    58
      in [(Syntax.dddot_indexname, get_subject prop)] @ statement_binds (thisN, prop) end;
wenzelm@7675
    59
wenzelm@7675
    60
wenzelm@7675
    61
(* atomic_thesis *)
wenzelm@7675
    62
wenzelm@7675
    63
fun mk_free t = Free (thesisN, Term.fastype_of t);
wenzelm@7675
    64
wenzelm@9296
    65
fun atomic_thesis ((c as Const ("Trueprop", _)) $ t) = (t, c $ mk_free t)
wenzelm@9296
    66
  | atomic_thesis t = (t, mk_free t);
wenzelm@8227
    67
wenzelm@8227
    68
wenzelm@8227
    69
(** judgment **)
wenzelm@8227
    70
wenzelm@8227
    71
fun gen_add_judgment add args = PureThy.local_path o add [args] o PureThy.global_path;
wenzelm@8227
    72
wenzelm@8227
    73
val add_judgment = gen_add_judgment Theory.add_consts;
wenzelm@8227
    74
val add_judgment_i = gen_add_judgment Theory.add_consts_i;
wenzelm@8227
    75
wenzelm@6796
    76
wenzelm@6783
    77
end;