TFL/post.sml
changeset 3302 404fe31fd8d2
parent 3271 b873969b05d3
child 3331 c81c7f8ad333
equal deleted inserted replaced
3301:cdcc4d5602b6 3302:404fe31fd8d2
       
     1 (*  Title:      TFL/post
       
     2     ID:         $Id$
       
     3     Author:     Konrad Slind, Cambridge University Computer Laboratory
       
     4     Copyright   1997  University of Cambridge
       
     5 
       
     6 Postprocessing of TFL definitions
       
     7 *)
       
     8 
     1 (*-------------------------------------------------------------------------
     9 (*-------------------------------------------------------------------------
     2 there are 3 postprocessors that get applied to the definition:
    10 Three postprocessors are applied to the definition:
     3 
       
     4     - a wellfoundedness prover (WF_TAC)
    11     - a wellfoundedness prover (WF_TAC)
     5     - a simplifier (tries to eliminate the language of termination expressions)
    12     - a simplifier (tries to eliminate the language of termination expressions)
     6     - a termination prover
    13     - a termination prover
     7 *-------------------------------------------------------------------------*)
    14 *-------------------------------------------------------------------------*)
     8 
    15 
    73                   THEN TRY(best_tac
    80                   THEN TRY(best_tac
    74                            (!claset addSDs [not0_implies_Suc]
    81                            (!claset addSDs [not0_implies_Suc]
    75                                     addss (!simpset)) 1);
    82                                     addss (!simpset)) 1);
    76 
    83 
    77  val simpls = [less_eq RS eq_reflection,
    84  val simpls = [less_eq RS eq_reflection,
    78                lex_prod_def, rprod_def, measure_def, inv_image_def];
    85                lex_prod_def, measure_def, inv_image_def];
    79 
    86 
    80  (*---------------------------------------------------------------------------
    87  (*---------------------------------------------------------------------------
    81   * Does some standard things with the termination conditions of a definition:
    88   * Does some standard things with the termination conditions of a definition:
    82   * attempts to prove wellfoundedness of the given relation; simplifies the
    89   * attempts to prove wellfoundedness of the given relation; simplifies the
    83   * non-proven termination conditions; and finally attempts to prove the 
    90   * non-proven termination conditions; and finally attempts to prove the 
   189           end
   196           end
   190   end handle (e as Utils.ERR _) => Utils.Raise e
   197   end handle (e as Utils.ERR _) => Utils.Raise e
   191           |   e                 => print_exn e;
   198           |   e                 => print_exn e;
   192 
   199 
   193 
   200 
   194 (*lcp: uncurry the predicate of the induction rule*)
   201 (*lcp: curry the predicate of the induction rule*)
   195 fun uncurry_rule rl = Prod_Syntax.split_rule_var
   202 fun curry_rule rl = Prod_Syntax.split_rule_var
   196                         (head_of (HOLogic.dest_Trueprop (concl_of rl)), 
   203                         (head_of (HOLogic.dest_Trueprop (concl_of rl)), 
   197 			 rl);
   204 			 rl);
   198 
   205 
   199 (*lcp: put a theorem into Isabelle form, using meta-level connectives*)
   206 (*lcp: put a theorem into Isabelle form, using meta-level connectives*)
   200 val meta_outer = 
   207 val meta_outer = 
   201     uncurry_rule o standard o 
   208     curry_rule o standard o 
   202     rule_by_tactic (REPEAT_FIRST (resolve_tac [allI, impI, conjI]
   209     rule_by_tactic (REPEAT_FIRST (resolve_tac [allI, impI, conjI]
   203 				  ORELSE' etac conjE));
   210 				  ORELSE' etac conjE));
   204 
   211 
   205 (*Strip off the outer !P*)
   212 (*Strip off the outer !P*)
   206 val spec'= read_instantiate [("x","P::?'b=>bool")] spec;
   213 val spec'= read_instantiate [("x","P::?'b=>bool")] spec;