TFL/post.sml
changeset 3331 c81c7f8ad333
parent 3302 404fe31fd8d2
child 3391 5e45dd3b64e9
equal deleted inserted replaced
3330:ab7161e593c8 3331:c81c7f8ad333
    25    val simplifier : thm -> thm
    25    val simplifier : thm -> thm
    26    val std_postprocessor : theory 
    26    val std_postprocessor : theory 
    27                            -> {induction:thm, rules:thm, TCs:term list list} 
    27                            -> {induction:thm, rules:thm, TCs:term list list} 
    28                            -> {induction:thm, rules:thm, nested_tcs:thm list}
    28                            -> {induction:thm, rules:thm, nested_tcs:thm list}
    29 
    29 
    30    val define_i : theory -> term -> term -> theory * (thm * Prim.pattern list)
    30    val define_i : theory -> string -> term -> term 
    31    val define   : theory -> string -> string list -> theory * Prim.pattern list
    31                   -> theory * (thm * Prim.pattern list)
       
    32 
       
    33    val define   : theory -> string -> string -> string list 
       
    34                   -> theory * Prim.pattern list
    32 
    35 
    33    val simplify_defn : theory * (string * Prim.pattern list)
    36    val simplify_defn : theory * (string * Prim.pattern list)
    34                         -> {rules:thm list, induct:thm, tcs:term list}
    37                         -> {rules:thm list, induct:thm, tcs:term list}
    35 
    38 
    36   (*-------------------------------------------------------------------------
    39   (*-------------------------------------------------------------------------
    72  (*---------------------------------------------------------------------------
    75  (*---------------------------------------------------------------------------
    73   * Simple wellfoundedness prover.
    76   * Simple wellfoundedness prover.
    74   *--------------------------------------------------------------------------*)
    77   *--------------------------------------------------------------------------*)
    75  fun WF_TAC thms = REPEAT(FIRST1(map rtac thms))
    78  fun WF_TAC thms = REPEAT(FIRST1(map rtac thms))
    76  val WFtac = WF_TAC[wf_measure, wf_inv_image, wf_lex_prod, wf_less_than, 
    79  val WFtac = WF_TAC[wf_measure, wf_inv_image, wf_lex_prod, wf_less_than, 
    77                     wf_pred_list, wf_trancl];
    80                     wf_trancl];
    78 
    81 
    79  val terminator = simp_tac(!simpset addsimps [less_Suc_eq, pred_list_def]) 1
    82  val terminator = simp_tac(!simpset addsimps [less_Suc_eq]) 1
    80                   THEN TRY(best_tac
    83                   THEN TRY(best_tac
    81                            (!claset addSDs [not0_implies_Suc]
    84                            (!claset addSDs [not0_implies_Suc]
    82                                     addss (!simpset)) 1);
    85                                     addss (!simpset)) 1);
    83 
    86 
    84  val simpls = [less_eq RS eq_reflection,
    87  val simpls = [less_eq RS eq_reflection,
   103 val concl = #2 o Prim.Rules.dest_thm;
   106 val concl = #2 o Prim.Rules.dest_thm;
   104 
   107 
   105 (*---------------------------------------------------------------------------
   108 (*---------------------------------------------------------------------------
   106  * Defining a function with an associated termination relation. 
   109  * Defining a function with an associated termination relation. 
   107  *---------------------------------------------------------------------------*)
   110  *---------------------------------------------------------------------------*)
   108 fun define_i thy R eqs = 
   111 fun define_i thy fid R eqs = 
   109   let val dummy = require_thy thy "WF_Rel" "recursive function definitions";
   112   let val dummy = require_thy thy "WF_Rel" "recursive function definitions"
   110       
       
   111       val {functional,pats} = Prim.mk_functional thy eqs
   113       val {functional,pats} = Prim.mk_functional thy eqs
   112       val (thm,thry) = Prim.wfrec_definition0 thy  R functional
   114       val (thm,thry) = Prim.wfrec_definition0 thy fid R functional
   113   in (thry,(thm,pats))
   115   in (thry,(thm,pats))
   114   end;
   116   end;
   115 
   117 
   116 (*lcp's version: takes strings; doesn't return "thm" 
   118 (*lcp's version: takes strings; doesn't return "thm" 
   117         (whose signature is a draft and therefore useless) *)
   119         (whose signature is a draft and therefore useless) *)
   118 fun define thy R eqs = 
   120 fun define thy fid R eqs = 
   119   let fun read thy = readtm (sign_of thy) (TVar(("DUMMY",0),[])) 
   121   let fun read thy = readtm (sign_of thy) (TVar(("DUMMY",0),[])) 
   120       val (thy',(_,pats)) =
   122       val (thy',(_,pats)) =
   121              define_i thy (read thy R) 
   123              define_i thy fid (read thy R) 
   122                       (fold_bal (app Ind_Syntax.conj) (map (read thy) eqs))
   124                       (fold_bal (app Ind_Syntax.conj) (map (read thy) eqs))
   123   in  (thy',pats)  end
   125   in  (thy',pats)  end
   124   handle Utils.ERR {mesg,...} => error mesg;
   126   handle Utils.ERR {mesg,...} => error mesg;
   125 
   127 
   126 (*---------------------------------------------------------------------------
   128 (*---------------------------------------------------------------------------