src/Pure/Isar/auto_bind.ML
changeset 7675 c859160e78b0
parent 7599 40b7f7f51208
child 8227 d67db92897df
     1.1 --- a/src/Pure/Isar/auto_bind.ML	Fri Oct 01 20:36:53 1999 +0200
     1.2 +++ b/src/Pure/Isar/auto_bind.ML	Fri Oct 01 20:37:38 1999 +0200
     1.3 @@ -3,19 +3,26 @@
     1.4      Author:     Markus Wenzel, TU Muenchen
     1.5  
     1.6  Automatic term bindings -- logic specific patterns.
     1.7 +
     1.8 +The implementation below works fine with the more common
     1.9 +object-logics, such as HOL, ZF.
    1.10  *)
    1.11  
    1.12  signature AUTO_BIND =
    1.13  sig
    1.14    val goal: term -> (indexname * term option) list
    1.15    val facts: string -> term list -> (indexname * term option) list
    1.16 +  val atomic_thesis: term -> (string * term) * term
    1.17  end;
    1.18  
    1.19  structure AutoBind: AUTO_BIND =
    1.20  struct
    1.21  
    1.22 +val thesisN = "thesis";
    1.23 +val thisN = "this";
    1.24  
    1.25 -(* goals *)
    1.26 +
    1.27 +(* goal *)
    1.28  
    1.29  fun statement_binds (name, prop) =
    1.30    let
    1.31 @@ -27,7 +34,7 @@
    1.32        (name, case concl of Const ("Trueprop", _) $ t => Some (list_abs t) | _ => None)];
    1.33    in map (fn (s, t) => ((s, 0), t)) env end;
    1.34  
    1.35 -fun goal prop = statement_binds ("thesis", prop);
    1.36 +fun goal prop = statement_binds (thesisN, prop);
    1.37  
    1.38  
    1.39  (* facts *)
    1.40 @@ -39,7 +46,15 @@
    1.41  fun facts _ [] = []
    1.42    | facts name props =
    1.43        let val prop = Library.last_elem props
    1.44 -      in dddot_bind prop @ statement_binds ("this", prop) end;
    1.45 +      in dddot_bind prop @ statement_binds (thisN, prop) end;
    1.46 +
    1.47 +
    1.48 +(* atomic_thesis *)
    1.49 +
    1.50 +fun mk_free t = Free (thesisN, Term.fastype_of t);
    1.51 +
    1.52 +fun atomic_thesis ((c as Const ("Trueprop", _)) $ t) = ((thesisN, t), c $ mk_free t)
    1.53 +  | atomic_thesis t = ((thesisN, t), mk_free t);
    1.54        
    1.55  
    1.56  end;