src/HOL/Library/old_recdef.ML

 
 end;
 
 
 
-(*** notable theorems ***)
-
-structure Thms =
-struct
-  val WFREC_COROLLARY = @{thm tfl_wfrec};
-  val WF_INDUCTION_THM = @{thm tfl_wf_induct};
-  val CUT_DEF = @{thm tfl_cut_def};
-  val eqT = @{thm tfl_eq_True};
-  val rev_eq_mp = @{thm tfl_rev_eq_mp};
-  val simp_thm = @{thm tfl_simp_thm};
-  val P_imp_P_iff_True = @{thm tfl_P_imp_P_iff_True};
-  val imp_trans = @{thm tfl_imp_trans};
-  val disj_assoc = @{thm tfl_disj_assoc};
-  val tfl_disjE = @{thm tfl_disjE};
-  val choose_thm = @{thm tfl_exE};
-end;
-
-
-
 (*** emulation of HOL inference rules for TFL ***)
 
 structure Rules: RULES =
 struct
 

    handle Utils.ERR _ => raise RULES_ERR "UNDISCH" ""
      | THM _ => raise RULES_ERR "UNDISCH" "";
 
 fun PROVE_HYP ath bth = MP (DISCH (cconcl ath) bth) ath;
 
-fun IMP_TRANS th1 th2 = th2 RS (th1 RS Thms.imp_trans)
+fun IMP_TRANS th1 th2 = th2 RS (th1 RS @{thm tfl_imp_trans})
   handle THM (msg, _, _) => raise RULES_ERR "IMP_TRANS" msg;
 
 
 (*----------------------------------------------------------------------------
  *        Conjunction

     val c = Dcterm.drop_prop (cconcl th1);
     val (disj1, disj2) = Dcterm.dest_disj c;
     val th2' = DISCH disj1 th2;
     val th3' = DISCH disj2 th3;
   in
-    th3' RS (th2' RS (th1 RS Thms.tfl_disjE))
+    th3' RS (th2' RS (th1 RS @{thm tfl_disjE}))
       handle THM (msg, _, _) => raise RULES_ERR "DISJ_CASES" msg
   end;
 
 
 (*-----------------------------------------------------------------------------

     val lam = #2 (Dcterm.dest_comb (Dcterm.drop_prop (cconcl exth)))
     val redex = Dcterm.capply lam fvar
     val t$u = Thm.term_of redex
     val residue = Thm.cterm_of ctxt (Term.betapply (t, u))
   in
-    GEN ctxt fvar (DISCH residue fact) RS (exth RS Thms.choose_thm)
+    GEN ctxt fvar (DISCH residue fact) RS (exth RS @{thm tfl_exE})
       handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg
   end;
 
 local
   val prop = Thm.prop_of exI

 
 fun simpl_conv ctxt thl ctm =
  rew_conv (ctxt addsimps thl) ctm RS meta_eq_to_obj_eq;
 
 
-fun RIGHT_ASSOC ctxt = rewrite_rule ctxt [Thms.disj_assoc];
+fun RIGHT_ASSOC ctxt = rewrite_rule ctxt @{thms tfl_disj_assoc};
 
 
 
 (*---------------------------------------------------------------------------
  *                  TERMINATION CONDITION EXTRACTION

   | poly_tvars (TFree (a,sort)) = TVar (("?" ^ a, 0), sort)
   | poly_tvars (TVar ((a,i),sort)) = TVar (("?" ^ a, i+1), sort);
 
 local
   val f_eq_wfrec_R_M =
-    #ant(USyntax.dest_imp(#2(USyntax.strip_forall (concl Thms.WFREC_COROLLARY))))
+    #ant(USyntax.dest_imp(#2(USyntax.strip_forall (concl @{thm tfl_wfrec}))))
   val {lhs=f, rhs} = USyntax.dest_eq f_eq_wfrec_R_M
   val _ = dest_Free f
   val (wfrec,_) = USyntax.strip_comb rhs
 in
 

 
 fun post_definition ctxt meta_tflCongs (def, pats) =
  let val thy = Proof_Context.theory_of ctxt
      val tych = Thry.typecheck thy
      val f = #lhs(USyntax.dest_eq(concl def))
-     val corollary = Rules.MATCH_MP Thms.WFREC_COROLLARY def
+     val corollary = Rules.MATCH_MP @{thm tfl_wfrec} def
      val pats' = filter given pats
      val given_pats = map pat_of pats'
      val rows = map row_of_pat pats'
      val WFR = #ant(USyntax.dest_imp(concl corollary))
      val R = #Rand(USyntax.dest_comb WFR)

               (Symtab.dest (BNF_LFP_Compat.get_all thy [BNF_LFP_Compat.Keep_Nesting]))
      val corollaries' = map (Simplifier.simplify case_simpset) corollaries
      val extract =
       Rules.CONTEXT_REWRITE_RULE ctxt (f, [R], @{thm cut_apply}, meta_tflCongs @ context_congs)
      val (rules, TCs) = ListPair.unzip (map extract corollaries')
-     val rules0 = map (rewrite_rule ctxt [Thms.CUT_DEF]) rules
+     val rules0 = map (rewrite_rule ctxt @{thms tfl_cut_def}) rules
      val mk_cond_rule = Rules.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
      val rules1 = Rules.LIST_CONJ(map mk_cond_rule rules0)
  in
  {rules = rules1,
   rows = rows,

                                       quote fid ^ " but found one of " ^
                                       quote x)
                  else ()
      val (case_rewrites,context_congs) = extraction_thms thy
      val tych = Thry.typecheck thy
-     val WFREC_THM0 = Rules.ISPEC (tych functional) Thms.WFREC_COROLLARY
+     val WFREC_THM0 = Rules.ISPEC (tych functional) @{thm tfl_wfrec}
      val Const(@{const_name All},_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
      val R = Free (singleton (Name.variant_list (List.foldr Misc_Legacy.add_term_names [] eqns)) Rname,
                    Rtype)
      val WFREC_THM = Rules.ISPECL [tych R, tych g] WFREC_THM0
      val ([proto_def, WFR],_) = USyntax.strip_imp(concl WFREC_THM)

 
 
 (*----------------------------------------------------------------------------
  * Input : f, R,  and  [(pat1,TCs1),..., (patn,TCsn)]
  *
- * Instantiates WF_INDUCTION_THM, getting Sinduct and then tries to prove
+ * Instantiates tfl_wf_induct, getting Sinduct and then tries to prove
  * recursion induction (Rinduct) by proving the antecedent of Sinduct from
  * the antecedent of Rinduct.
  *---------------------------------------------------------------------------*)
 fun mk_induction thy {fconst, R, SV, pat_TCs_list} =
 let val ctxt = Proof_Context.init_global thy
     val tych = Thry.typecheck thy
-    val Sinduction = Rules.UNDISCH (Rules.ISPEC (tych R) Thms.WF_INDUCTION_THM)
+    val Sinduction = Rules.UNDISCH (Rules.ISPEC (tych R) @{thm tfl_wf_induct})
     val (pats,TCsl) = ListPair.unzip pat_TCs_list
     val case_thm = complete_cases thy pats
     val domain = (type_of o hd) pats
     val Pname = singleton (Name.variant_list (List.foldr (Library.foldr Misc_Legacy.add_term_names)
                               [] (pats::TCsl))) "P"

       fun loop [] = ind
         | loop (asm::rst) =
           if (can (Thry.match_term thy asm) tc)
           then Rules.UNDISCH
                  (Rules.MATCH_MP
-                     (Rules.MATCH_MP Thms.simp_thm (Rules.DISCH (tych asm) ind))
+                     (Rules.MATCH_MP @{thm tfl_simp_thm} (Rules.DISCH (tych asm) ind))
                      hth)
          else loop rst
   in loop asl
 end;
 

 
    (*----------------------------------------------------------------------
     * The termination condition (tc) is simplified to |- tc = tc' (there
     * might not be a change!) and then 3 attempts are made:
     *
-    *   1. if |- tc = T, then eliminate it with eqT; otherwise,
+    *   1. if |- tc = T, then eliminate it with tfl_eq_True; otherwise,
     *   2. apply the terminator to tc'. If |- tc' = T then eliminate; else
     *   3. replace tc by tc' in both the rules and the induction theorem.
     *---------------------------------------------------------------------*)
 
    fun simplify_tc tc (r,ind) =
        let val tc1 = tych tc
            val _ = trace_cterm ctxt "TC before simplification: " tc1
            val tc_eq = simplifier tc1
            val _ = trace_thms ctxt "result: " [tc_eq]
        in
-       elim_tc (Rules.MATCH_MP Thms.eqT tc_eq) (r,ind)
+       elim_tc (Rules.MATCH_MP @{thm tfl_eq_True} tc_eq) (r,ind)
        handle Utils.ERR _ =>
-        (elim_tc (Rules.MATCH_MP(Rules.MATCH_MP Thms.rev_eq_mp tc_eq)
+        (elim_tc (Rules.MATCH_MP(Rules.MATCH_MP @{thm tfl_rev_eq_mp} tc_eq)
                   (Rules.prove ctxt strict (HOLogic.mk_Trueprop(USyntax.rhs(concl tc_eq)),
                            terminator)))
                  (r,ind)
          handle Utils.ERR _ =>
-          (Rules.UNDISCH(Rules.MATCH_MP (Rules.MATCH_MP Thms.simp_thm r) tc_eq),
+          (Rules.UNDISCH(Rules.MATCH_MP (Rules.MATCH_MP @{thm tfl_simp_thm} r) tc_eq),
            simplify_induction thy tc_eq ind))
        end
 
    (*----------------------------------------------------------------------
     * Nested termination conditions are harder to get at, since they are

     *---------------------------------------------------------------------*)
    fun simplify_nested_tc tc =
       let val tc_eq = simplifier (tych (#2 (USyntax.strip_forall tc)))
       in
       Rules.GEN_ALL ctxt
-       (Rules.MATCH_MP Thms.eqT tc_eq
+       (Rules.MATCH_MP @{thm tfl_eq_True} tc_eq
         handle Utils.ERR _ =>
-          (Rules.MATCH_MP(Rules.MATCH_MP Thms.rev_eq_mp tc_eq)
+          (Rules.MATCH_MP(Rules.MATCH_MP @{thm tfl_rev_eq_mp} tc_eq)
                       (Rules.prove ctxt strict (HOLogic.mk_Trueprop (USyntax.rhs(concl tc_eq)),
                                terminator))
             handle Utils.ERR _ => tc_eq))
       end