src/Pure/Isar/auto_bind.ML
author wenzelm
Wed Sep 29 13:49:07 1999 +0200 (1999-09-29)
changeset 7632 25a0d2ba3a87
parent 7599 40b7f7f51208
child 7675 c859160e78b0
permissions -rw-r--r--
removed extra shyps error;
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@7599
    10
  val goal: term -> (indexname * term option) list
wenzelm@7599
    11
  val facts: string -> term list -> (indexname * term option) 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@7331
    22
    val concl = Logic.strip_assums_concl prop;
wenzelm@7331
    23
    val parms = Logic.strip_params prop;
wenzelm@7331
    24
    fun list_abs tm = foldr (fn ((x, T), t) => Abs (x, T, t)) (parms, tm);
wenzelm@7331
    25
wenzelm@7599
    26
    val env = [(name ^ "_prop", Some prop), (name ^ "_concl", Some (list_abs concl)),
wenzelm@7599
    27
      (name, case concl of Const ("Trueprop", _) $ t => Some (list_abs t) | _ => None)];
wenzelm@7474
    28
  in map (fn (s, t) => ((s, 0), t)) env end;
wenzelm@6783
    29
wenzelm@6796
    30
fun goal prop = statement_binds ("thesis", prop);
wenzelm@6783
    31
wenzelm@6783
    32
wenzelm@6796
    33
(* facts *)
wenzelm@6796
    34
wenzelm@6796
    35
fun dddot_bind prop =
wenzelm@7599
    36
  [(Syntax.dddot_indexname,
wenzelm@7599
    37
      case Logic.strip_imp_concl prop of Const ("Trueprop", _) $ (_ $ t) => Some t | _ => None)];
wenzelm@6796
    38
wenzelm@6796
    39
fun facts _ [] = []
wenzelm@7452
    40
  | facts name props =
wenzelm@7452
    41
      let val prop = Library.last_elem props
wenzelm@7452
    42
      in dddot_bind prop @ statement_binds ("this", prop) end;
wenzelm@6796
    43
      
wenzelm@6796
    44
wenzelm@6783
    45
end;