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