src/Pure/Isar/auto_bind.ML
changeset 6783 9cf9c17d9e35
child 6796 c2e5cb8cd50d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Isar/auto_bind.ML	Sat Jun 05 20:27:53 1999 +0200
     1.3 @@ -0,0 +1,36 @@
     1.4 +(*  Title:      Pure/Isar/auto_bind.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +
     1.8 +Automatic term bindings -- logic specific patterns.
     1.9 +
    1.10 +TODO:
    1.11 +  - logic specific theory data instead of hardwired operations (!!);
    1.12 +*)
    1.13 +
    1.14 +signature AUTO_BIND =
    1.15 +sig
    1.16 +  val goal: term -> (indexname * term) list
    1.17 +  val facts: term list -> (indexname * term) list
    1.18 +end;
    1.19 +
    1.20 +structure AutoBind: AUTO_BIND =
    1.21 +struct
    1.22 +
    1.23 +val thesisN = "thesis";
    1.24 +fun thesis_name sfx = (Syntax.binding (thesisN ^ sfx), 0);
    1.25 +
    1.26 +fun goal prop =
    1.27 +  let val concl = Logic.strip_imp_concl prop in
    1.28 +    [(thesis_name "_prop", prop), (thesis_name "_concl", concl)] @
    1.29 +      (case concl of Const ("Trueprop", _) $ t => [(thesis_name "", t)] | _ => [])
    1.30 +  end;
    1.31 +
    1.32 +fun facts [] = []
    1.33 +  | facts props =
    1.34 +      (case Logic.strip_imp_concl (Library.last_elem props) of
    1.35 +        Const ("Trueprop", _) $ (_ $ t) => [(Syntax.dddot_indexname, t)]
    1.36 +      | _ => []);
    1.37 +
    1.38 +
    1.39 +end;