discontinued unused 'defer_recdef';
authorwenzelm
Fri Jun 19 20:14:50 2015 +0200 (2015-06-19)
changeset 60523be2d9f5ddc76
parent 60522 1409b4015671
child 60524 ffc1ee11759c
discontinued unused 'defer_recdef';
NEWS
src/Doc/Isar_Ref/HOL_Specific.thy
src/HOL/Library/Old_Recdef.thy
src/HOL/Library/old_recdef.ML
     1.1 --- a/NEWS	Fri Jun 19 19:45:01 2015 +0200
     1.2 +++ b/NEWS	Fri Jun 19 20:14:50 2015 +0200
     1.3 @@ -129,6 +129,9 @@
     1.4      less_eq_multiset_def
     1.5      INCOMPATIBILITY
     1.6  
     1.7 +* Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef'
     1.8 +command. Minor INCOMPATIBILITY, use 'function' instead.
     1.9 +
    1.10  
    1.11  
    1.12  New in Isabelle2015 (May 2015)
     2.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Jun 19 19:45:01 2015 +0200
     2.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Jun 19 20:14:50 2015 +0200
     2.3 @@ -654,25 +654,20 @@
     2.4  text \<open>
     2.5    \begin{matharray}{rcl}
     2.6      @{command_def (HOL) "recdef"} & : & @{text "theory \<rightarrow> theory)"} \\
     2.7 -    @{command_def (HOL) "recdef_tc"}@{text "\<^sup>*"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
     2.8    \end{matharray}
     2.9  
    2.10 -  The old TFL commands @{command (HOL) "recdef"} and @{command (HOL)
    2.11 -  "recdef_tc"} for defining recursive are mostly obsolete; @{command
    2.12 -  (HOL) "function"} or @{command (HOL) "fun"} should be used instead.
    2.13 +  The old TFL command @{command (HOL) "recdef"} for defining recursive is
    2.14 +  mostly obsolete; @{command (HOL) "function"} or @{command (HOL) "fun"}
    2.15 +  should be used instead.
    2.16  
    2.17    @{rail \<open>
    2.18      @@{command (HOL) recdef} ('(' @'permissive' ')')? \<newline>
    2.19        @{syntax name} @{syntax term} (@{syntax prop} +) hints?
    2.20      ;
    2.21 -    recdeftc @{syntax thmdecl}? tc
    2.22 -    ;
    2.23      hints: '(' @'hints' ( recdefmod * ) ')'
    2.24      ;
    2.25      recdefmod: (('recdef_simp' | 'recdef_cong' | 'recdef_wf')
    2.26        (() | 'add' | 'del') ':' @{syntax thmrefs}) | @{syntax clasimpmod}
    2.27 -    ;
    2.28 -    tc: @{syntax nameref} ('(' @{syntax nat} ')')?
    2.29    \<close>}
    2.30  
    2.31    \begin{description}
    2.32 @@ -688,14 +683,6 @@
    2.33    (cf.\ \secref{sec:simplifier}) and Classical reasoner (cf.\
    2.34    \secref{sec:classical}).
    2.35  
    2.36 -  \item @{command (HOL) "recdef_tc"}~@{text "c (i)"} recommences the
    2.37 -  proof for leftover termination condition number @{text i} (default
    2.38 -  1) as generated by a @{command (HOL) "recdef"} definition of
    2.39 -  constant @{text c}.
    2.40 -
    2.41 -  Note that in most cases, @{command (HOL) "recdef"} is able to finish
    2.42 -  its internal proofs without manual intervention.
    2.43 -
    2.44    \end{description}
    2.45  
    2.46    \medskip Hints for @{command (HOL) "recdef"} may be also declared
     3.1 --- a/src/HOL/Library/Old_Recdef.thy	Fri Jun 19 19:45:01 2015 +0200
     3.2 +++ b/src/HOL/Library/Old_Recdef.thy	Fri Jun 19 20:14:50 2015 +0200
     3.3 @@ -7,8 +7,7 @@
     3.4  theory Old_Recdef
     3.5  imports Main
     3.6  keywords
     3.7 -  "recdef" "defer_recdef" :: thy_decl and
     3.8 -  "recdef_tc" :: thy_goal and
     3.9 +  "recdef" :: thy_decl and
    3.10    "permissive" "congs" "hints"
    3.11  begin
    3.12  
     4.1 --- a/src/HOL/Library/old_recdef.ML	Fri Jun 19 19:45:01 2015 +0200
     4.2 +++ b/src/HOL/Library/old_recdef.ML	Fri Jun 19 20:14:50 2015 +0200
     4.3 @@ -225,13 +225,6 @@
     4.4      proto_def: term,
     4.5      extracta: (thm * term list) list,
     4.6      pats: pattern list}
     4.7 -  val lazyR_def: theory -> xstring -> thm list -> term list ->
     4.8 -   {theory: theory,
     4.9 -    rules: thm,
    4.10 -    R: term,
    4.11 -    SV: term list,
    4.12 -    full_pats_TCs: (term * term list) list,
    4.13 -    patterns : pattern list}
    4.14    val mk_induction: theory ->
    4.15      {fconst: term, R: term, SV: term list, pat_TCs_list: (term * term list) list} -> thm
    4.16    val postprocess: Proof.context -> bool ->
    4.17 @@ -246,8 +239,6 @@
    4.18      {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} * Proof.context
    4.19    val define: bool -> thm list -> thm list -> xstring -> string -> string list -> Proof.context ->
    4.20      {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} * Proof.context
    4.21 -  val defer_i: thm list -> xstring -> term list -> theory -> thm * theory
    4.22 -  val defer: thm list -> xstring -> string list -> theory -> thm * theory
    4.23  end;
    4.24  
    4.25  signature OLD_RECDEF =
    4.26 @@ -266,13 +257,6 @@
    4.27        * {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list}
    4.28    val add_recdef_i: bool -> xstring -> term -> ((binding * term) * attribute list) list ->
    4.29      theory -> theory * {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list}
    4.30 -  val defer_recdef: xstring -> string list -> (Facts.ref * Token.src list) list
    4.31 -    -> theory -> theory * {induct_rules: thm}
    4.32 -  val defer_recdef_i: xstring -> term list -> thm list -> theory -> theory * {induct_rules: thm}
    4.33 -  val recdef_tc: bstring * Token.src list -> xstring -> int option -> bool ->
    4.34 -    local_theory -> Proof.state
    4.35 -  val recdef_tc_i: bstring * Token.src list -> string -> int option -> bool ->
    4.36 -    local_theory -> Proof.state
    4.37  end;
    4.38  
    4.39  structure Old_Recdef: OLD_RECDEF =
    4.40 @@ -2209,74 +2193,6 @@
    4.41   end;
    4.42  
    4.43  
    4.44 -(*---------------------------------------------------------------------------
    4.45 - * Define the constant after extracting the termination conditions. The
    4.46 - * wellfounded relation used in the definition is computed by using the
    4.47 - * choice operator on the extracted conditions (plus the condition that
    4.48 - * such a relation must be wellfounded).
    4.49 - *---------------------------------------------------------------------------*)
    4.50 -
    4.51 -fun lazyR_def thy fid tflCongs eqns =
    4.52 - let val {proto_def,WFR,pats,extracta,SV} =
    4.53 -           wfrec_eqns thy fid tflCongs eqns
    4.54 -     val R1 = USyntax.rand WFR
    4.55 -     val f = #lhs(USyntax.dest_eq proto_def)
    4.56 -     val (extractants,TCl) = ListPair.unzip extracta
    4.57 -     val _ = if !trace
    4.58 -                 then writeln (cat_lines ("Extractants =" ::
    4.59 -                  map (Display.string_of_thm_global thy) extractants))
    4.60 -                 else ()
    4.61 -     val TCs = fold_rev (union (op aconv)) TCl []
    4.62 -     val full_rqt = WFR::TCs
    4.63 -     val R' = USyntax.mk_select{Bvar=R1, Body=USyntax.list_mk_conj full_rqt}
    4.64 -     val R'abs = USyntax.rand R'
    4.65 -     val proto_def' = subst_free[(R1,R')] proto_def
    4.66 -     val _ = if !trace then writeln ("proto_def' = " ^
    4.67 -                                         Syntax.string_of_term_global
    4.68 -                                         thy proto_def')
    4.69 -                           else ()
    4.70 -     val {lhs,rhs} = USyntax.dest_eq proto_def'
    4.71 -     val (c,args) = USyntax.strip_comb lhs
    4.72 -     val (name,Ty) = dest_atom c
    4.73 -     val defn = const_def thy (name, Ty, USyntax.list_mk_abs (args,rhs))
    4.74 -     val ([def0], thy') =
    4.75 -       thy
    4.76 -       |> Global_Theory.add_defs false
    4.77 -            [Thm.no_attributes (Binding.name (Thm.def_name fid), defn)]
    4.78 -     val def = Thm.unvarify_global def0;
    4.79 -     val ctxt' = Syntax.init_pretty_global thy';
    4.80 -     val _ =
    4.81 -       if !trace then writeln ("DEF = " ^ Display.string_of_thm ctxt' def)
    4.82 -       else ()
    4.83 -     (* val fconst = #lhs(USyntax.dest_eq(concl def))  *)
    4.84 -     val tych = Thry.typecheck thy'
    4.85 -     val full_rqt_prop = map (Dcterm.mk_prop o tych) full_rqt
    4.86 -         (*lcp: a lot of object-logic inference to remove*)
    4.87 -     val baz = Rules.DISCH_ALL
    4.88 -                 (fold_rev Rules.DISCH full_rqt_prop
    4.89 -                  (Rules.LIST_CONJ extractants))
    4.90 -     val _ = if !trace then writeln ("baz = " ^ Display.string_of_thm ctxt' baz) else ()
    4.91 -     val SV' = map tych SV;
    4.92 -     val SVrefls = map Thm.reflexive SV'
    4.93 -     val def0 = (fold (fn x => fn th => Rules.rbeta(Thm.combination th x))
    4.94 -                   SVrefls def)
    4.95 -                RS meta_eq_to_obj_eq
    4.96 -     val def' = Rules.MP (Rules.SPEC (tych R') (Rules.GEN ctxt' (tych R1) baz)) def0
    4.97 -     val body_th = Rules.LIST_CONJ (map Rules.ASSUME full_rqt_prop)
    4.98 -     val SELECT_AX = (*in this way we hope to avoid a STATIC dependence upon
    4.99 -                       theory Hilbert_Choice*)
   4.100 -         ML_Context.thm "Hilbert_Choice.tfl_some"
   4.101 -         handle ERROR msg => cat_error msg
   4.102 -    "defer_recdef requires theory Main or at least Hilbert_Choice as parent"
   4.103 -     val bar = Rules.MP (Rules.ISPECL[tych R'abs, tych R1] SELECT_AX) body_th
   4.104 - in {theory = thy', R=R1, SV=SV,
   4.105 -     rules = fold (fn a => fn b => Rules.MP b a) (Rules.CONJUNCTS bar) def',
   4.106 -     full_pats_TCs = merge (map pat_of pats) (ListPair.zip (givens pats, TCl)),
   4.107 -     patterns = pats}
   4.108 - end;
   4.109 -
   4.110 -
   4.111 -
   4.112  (*----------------------------------------------------------------------------
   4.113   *
   4.114   *                           INDUCTION THEOREM
   4.115 @@ -2860,32 +2776,6 @@
   4.116      (Syntax.read_term ctxt R) (map (Syntax.read_term ctxt) seqs) ctxt
   4.117        handle Utils.ERR {mesg,...} => error mesg;
   4.118  
   4.119 -
   4.120 -(*---------------------------------------------------------------------------
   4.121 - *
   4.122 - *     Definitions with synthesized termination relation
   4.123 - *
   4.124 - *---------------------------------------------------------------------------*)
   4.125 -
   4.126 -fun func_of_cond_eqn tm =
   4.127 -  #1 (USyntax.strip_comb (#lhs (USyntax.dest_eq (#2 (USyntax.strip_forall (#2 (USyntax.strip_imp tm)))))));
   4.128 -
   4.129 -fun defer_i congs fid eqs thy =
   4.130 - let
   4.131 -     val {rules,R,theory,full_pats_TCs,SV,...} = Prim.lazyR_def thy fid congs eqs
   4.132 -     val f = func_of_cond_eqn (concl (Rules.CONJUNCT1 rules handle Utils.ERR _ => rules));
   4.133 -     val _ = writeln "Proving induction theorem ...";
   4.134 -     val induction = Prim.mk_induction theory
   4.135 -                        {fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs}
   4.136 - in
   4.137 -   (*return the conjoined induction rule and recursion equations,
   4.138 -     with assumptions remaining to discharge*)
   4.139 -   (Drule.export_without_context (induction RS (rules RS conjI)), theory)
   4.140 - end
   4.141 -
   4.142 -fun defer congs fid seqs thy =
   4.143 -  defer_i congs fid (map (Syntax.read_term_global thy) seqs) thy
   4.144 -    handle Utils.ERR {mesg,...} => error mesg;
   4.145  end;
   4.146  
   4.147  end;
   4.148 @@ -3066,55 +2956,6 @@
   4.149  
   4.150  
   4.151  
   4.152 -(** defer_recdef(_i) **)
   4.153 -
   4.154 -fun gen_defer_recdef tfl_fn eval_thms raw_name eqs raw_congs thy =
   4.155 -  let
   4.156 -    val name = Sign.intern_const thy raw_name;
   4.157 -    val bname = Long_Name.base_name name;
   4.158 -
   4.159 -    val _ = writeln ("Deferred recursive function " ^ quote name ^ " ...");
   4.160 -
   4.161 -    val congs = eval_thms (Proof_Context.init_global thy) raw_congs;
   4.162 -    val (induct_rules, thy2) = tfl_fn congs name eqs thy;
   4.163 -    val ([induct_rules'], thy3) =
   4.164 -      thy2
   4.165 -      |> Sign.add_path bname
   4.166 -      |> Global_Theory.add_thms [((Binding.name "induct_rules", induct_rules), [])]
   4.167 -      ||> Sign.parent_path;
   4.168 -  in (thy3, {induct_rules = induct_rules'}) end;
   4.169 -
   4.170 -val defer_recdef = gen_defer_recdef Tfl.defer Attrib.eval_thms;
   4.171 -val defer_recdef_i = gen_defer_recdef Tfl.defer_i (K I);
   4.172 -
   4.173 -
   4.174 -
   4.175 -(** recdef_tc(_i) **)
   4.176 -
   4.177 -fun gen_recdef_tc prep_att prep_name (bname, raw_atts) raw_name opt_i int lthy =
   4.178 -  let
   4.179 -    val thy = Proof_Context.theory_of lthy;
   4.180 -    val name = prep_name thy raw_name;
   4.181 -    val atts = map (prep_att lthy) raw_atts;
   4.182 -    val tcs =
   4.183 -      (case get_recdef thy name of
   4.184 -        NONE => error ("No recdef definition of constant: " ^ quote name)
   4.185 -      | SOME {tcs, ...} => tcs);
   4.186 -    val i = the_default 1 opt_i;
   4.187 -    val tc = nth tcs (i - 1) handle General.Subscript =>
   4.188 -      error ("No termination condition #" ^ string_of_int i ^
   4.189 -        " in recdef definition of " ^ quote name);
   4.190 -  in
   4.191 -    Specification.theorem "" NONE (K I)
   4.192 -      (Binding.concealed (Binding.name bname), atts) [] []
   4.193 -      (Element.Shows [(Attrib.empty_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy
   4.194 -  end;
   4.195 -
   4.196 -val recdef_tc = gen_recdef_tc Attrib.check_src Sign.intern_const;
   4.197 -val recdef_tc_i = gen_recdef_tc (K I) (K I);
   4.198 -
   4.199 -
   4.200 -
   4.201  (** package setup **)
   4.202  
   4.203  (* setup theory *)
   4.204 @@ -3147,23 +2988,4 @@
   4.205    Outer_Syntax.command @{command_keyword recdef} "define general recursive functions (obsolete TFL)"
   4.206      (recdef_decl >> Toplevel.theory);
   4.207  
   4.208 -
   4.209 -val defer_recdef_decl =
   4.210 -  Parse.name -- Scan.repeat1 Parse.prop --
   4.211 -  Scan.optional
   4.212 -    (@{keyword "("} |-- @{keyword "congs"} |-- Parse.!!! (Parse.xthms1 --| @{keyword ")"})) []
   4.213 -  >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
   4.214 -
   4.215 -val _ =
   4.216 -  Outer_Syntax.command @{command_keyword defer_recdef}
   4.217 -    "defer general recursive functions (obsolete TFL)"
   4.218 -    (defer_recdef_decl >> Toplevel.theory);
   4.219 -
   4.220 -val _ =
   4.221 -  Outer_Syntax.local_theory_to_proof' @{command_keyword recdef_tc}
   4.222 -    "recommence proof of termination condition (obsolete TFL)"
   4.223 -    ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.xname --
   4.224 -        Scan.option (@{keyword "("} |-- Parse.nat --| @{keyword ")"})
   4.225 -      >> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
   4.226 -
   4.227  end;