src/Pure/Isar/auto_bind.ML
changeset 6796 c2e5cb8cd50d
parent 6783 9cf9c17d9e35
child 7048 3535eec33c50
     1.1 --- a/src/Pure/Isar/auto_bind.ML	Mon Jun 07 21:22:18 1999 +0200
     1.2 +++ b/src/Pure/Isar/auto_bind.ML	Mon Jun 07 22:16:56 1999 +0200
     1.3 @@ -3,34 +3,43 @@
     1.4      Author:     Markus Wenzel, TU Muenchen
     1.5  
     1.6  Automatic term bindings -- logic specific patterns.
     1.7 -
     1.8 -TODO:
     1.9 -  - logic specific theory data instead of hardwired operations (!!);
    1.10  *)
    1.11  
    1.12  signature AUTO_BIND =
    1.13  sig
    1.14    val goal: term -> (indexname * term) list
    1.15 -  val facts: term list -> (indexname * term) list
    1.16 +  val facts: string -> term list -> (indexname * term) list
    1.17  end;
    1.18  
    1.19  structure AutoBind: AUTO_BIND =
    1.20  struct
    1.21  
    1.22 -val thesisN = "thesis";
    1.23 -fun thesis_name sfx = (Syntax.binding (thesisN ^ sfx), 0);
    1.24 +
    1.25 +(* goals *)
    1.26  
    1.27 -fun goal prop =
    1.28 -  let val concl = Logic.strip_imp_concl prop in
    1.29 -    [(thesis_name "_prop", prop), (thesis_name "_concl", concl)] @
    1.30 -      (case concl of Const ("Trueprop", _) $ t => [(thesis_name "", t)] | _ => [])
    1.31 -  end;
    1.32 +fun statement_binds (name, prop) =
    1.33 +  let
    1.34 +    val concl = Logic.strip_imp_concl prop;
    1.35 +    val env = [(name ^ "_prop", prop), (name ^ "_concl", concl)] @
    1.36 +      (case concl of Const ("Trueprop", _) $ t => [(name, t)] | _ => []);
    1.37 +  in map (fn (s, t) => ((Syntax.binding s, 0), t)) env end;
    1.38  
    1.39 -fun facts [] = []
    1.40 -  | facts props =
    1.41 -      (case Logic.strip_imp_concl (Library.last_elem props) of
    1.42 -        Const ("Trueprop", _) $ (_ $ t) => [(Syntax.dddot_indexname, t)]
    1.43 -      | _ => []);
    1.44 +fun goal prop = statement_binds ("thesis", prop);
    1.45  
    1.46  
    1.47 +(* facts *)
    1.48 +
    1.49 +fun dddot_bind prop =
    1.50 +  (case Logic.strip_imp_concl prop of
    1.51 +    Const ("Trueprop", _) $ (_ $ t) => [(Syntax.dddot_indexname, t)]
    1.52 +  | _ => []);
    1.53 +
    1.54 +fun facts _ [] = []
    1.55 +  | facts name [prop] = statement_binds (name, prop) @ dddot_bind prop
    1.56 +  | facts name props =
    1.57 +      flat (map statement_binds
    1.58 +        (map2 (fn (i, t) => (name ^ string_of_int i, t)) (1 upto length props, props))) @
    1.59 +      dddot_bind (Library.last_elem props);
    1.60 +      
    1.61 +
    1.62  end;