src/Pure/Isar/auto_bind.ML
author wenzelm
Mon Jun 07 22:16:56 1999 +0200 (1999-06-07)
changeset 6796 c2e5cb8cd50d
parent 6783 9cf9c17d9e35
child 7048 3535eec33c50
permissions -rw-r--r--
facts: bind named props (from proof.ML/let_thms);
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@6783
     6
*)
wenzelm@6783
     7
wenzelm@6783
     8
signature AUTO_BIND =
wenzelm@6783
     9
sig
wenzelm@6783
    10
  val goal: term -> (indexname * term) list
wenzelm@6796
    11
  val facts: string -> term list -> (indexname * term) list
wenzelm@6783
    12
end;
wenzelm@6783
    13
wenzelm@6783
    14
structure AutoBind: AUTO_BIND =
wenzelm@6783
    15
struct
wenzelm@6783
    16
wenzelm@6796
    17
wenzelm@6796
    18
(* goals *)
wenzelm@6783
    19
wenzelm@6796
    20
fun statement_binds (name, prop) =
wenzelm@6796
    21
  let
wenzelm@6796
    22
    val concl = Logic.strip_imp_concl prop;
wenzelm@6796
    23
    val env = [(name ^ "_prop", prop), (name ^ "_concl", concl)] @
wenzelm@6796
    24
      (case concl of Const ("Trueprop", _) $ t => [(name, t)] | _ => []);
wenzelm@6796
    25
  in map (fn (s, t) => ((Syntax.binding s, 0), t)) env end;
wenzelm@6783
    26
wenzelm@6796
    27
fun goal prop = statement_binds ("thesis", prop);
wenzelm@6783
    28
wenzelm@6783
    29
wenzelm@6796
    30
(* facts *)
wenzelm@6796
    31
wenzelm@6796
    32
fun dddot_bind prop =
wenzelm@6796
    33
  (case Logic.strip_imp_concl prop of
wenzelm@6796
    34
    Const ("Trueprop", _) $ (_ $ t) => [(Syntax.dddot_indexname, t)]
wenzelm@6796
    35
  | _ => []);
wenzelm@6796
    36
wenzelm@6796
    37
fun facts _ [] = []
wenzelm@6796
    38
  | facts name [prop] = statement_binds (name, prop) @ dddot_bind prop
wenzelm@6796
    39
  | facts name props =
wenzelm@6796
    40
      flat (map statement_binds
wenzelm@6796
    41
        (map2 (fn (i, t) => (name ^ string_of_int i, t)) (1 upto length props, props))) @
wenzelm@6796
    42
      dddot_bind (Library.last_elem props);
wenzelm@6796
    43
      
wenzelm@6796
    44
wenzelm@6783
    45
end;