src/Pure/Isar/auto_bind.ML

isar: no_pos flag;

(*  Title:      Pure/Isar/auto_bind.ML
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen

Automatic term bindings -- logic specific patterns.
*)

signature AUTO_BIND =
sig
  val goal: term -> (indexname * term) list
  val facts: string -> term list -> (indexname * term) list
end;

structure AutoBind: AUTO_BIND =
struct


(* goals *)

fun statement_binds (name, prop) =
  let
    val concl = Logic.strip_assums_concl prop;
    val parms = Logic.strip_params prop;
    fun list_abs tm = foldr (fn ((x, T), t) => Abs (x, T, t)) (parms, tm);

    val env = [(name ^ "_prop", prop), (name ^ "_concl", list_abs concl)] @
      (case concl of Const ("Trueprop", _) $ t => [(name, list_abs t)] | _ => []);
  in map (fn (s, t) => ((Syntax.binding s, 0), t)) env end;

fun goal prop = statement_binds ("thesis", prop);


(* facts *)

fun dddot_bind prop =
  (case Logic.strip_imp_concl prop of
    Const ("Trueprop", _) $ (_ $ t) => [(Syntax.dddot_indexname, t)]
  | _ => []);

fun facts _ [] = []
  | facts name [prop] = dddot_bind prop
  | facts name props =  dddot_bind (Library.last_elem props);
      

end;