--- a/TFL/post.sml Wed Aug 18 18:10:48 1999 +0200
+++ b/TFL/post.sml Wed Aug 18 18:44:20 1999 +0200
@@ -8,6 +8,9 @@
signature TFL =
sig
+
+ val trace : bool ref
+
structure Prim : TFL_sig
val quiet_mode : bool ref
val message : string -> unit
@@ -19,17 +22,21 @@
-> {induction:thm, rules:thm, TCs:term list list}
-> {induction:thm, rules:thm, nested_tcs:thm list}
- val define_i : theory -> string -> term -> term list
- -> theory * Prim.pattern list
+ val define_i : theory -> xstring -> term
+ -> simpset * thm list (*allows special simplication*)
+ -> term list
+ -> theory * {rules:thm list, induct:thm, tcs:term list}
- val define : theory -> string -> string -> string list
- -> theory * Prim.pattern list
+ val define : theory -> xstring -> string
+ -> simpset * thm list
+ -> string list
+ -> theory * {rules:thm list, induct:thm, tcs:term list}
- val defer_i : theory -> string
+ val defer_i : theory -> xstring
-> thm list (* congruence rules *)
-> term list -> theory * thm
- val defer : theory -> string
+ val defer : theory -> xstring
-> thm list
-> string list -> theory * thm
@@ -45,7 +52,6 @@
structure Prim = Prim
structure S = USyntax
-
(* messages *)
val quiet_mode = ref false;
@@ -94,19 +100,6 @@
val concl = #2 o Rules.dest_thm;
- (*---------------------------------------------------------------------------
- * Defining a function with an associated termination relation.
- *---------------------------------------------------------------------------*)
- fun define_i thy fid R eqs =
- let val {functional,pats} = Prim.mk_functional thy eqs
- in (Prim.wfrec_definition0 thy (Sign.base_name fid) R functional, pats)
- end;
-
- fun define thy fid R eqs =
- let fun read thy = readtm (Theory.sign_of thy) (TVar(("DUMMY",0),[]))
- in define_i thy fid (read thy R) (map (read thy) eqs) end
- handle Utils.ERR {mesg,...} => error mesg;
-
(*---------------------------------------------------------------------------
* Postprocess a definition made by "define". This is a separate stage of
* processing from the definition stage.
@@ -152,7 +145,8 @@
let val dummy = message "Proving induction theorem ..."
val ind = Prim.mk_induction theory
{fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs}
- val dummy = (message "Proved induction theorem."; message "Postprocessing ...");
+ val dummy = (message "Proved induction theorem.";
+ message "Postprocessing ...");
val {rules, induction, nested_tcs} =
std_postprocessor ss theory {rules=rules, induction=ind, TCs=TCs}
in
@@ -194,15 +188,7 @@
(*Strip off the outer !P*)
val spec'= read_instantiate [("x","P::?'b=>bool")] spec;
- val wf_rel_defs = [lex_prod_def, measure_def, inv_image_def];
-
- (*Convert conclusion from = to ==*)
- val eq_reflect_list = map (fn th => (th RS eq_reflection) handle _ => th);
-
- (*---------------------------------------------------------------------------
- * Install the basic context notions. Others (for nat and list and prod)
- * have already been added in thry.sml
- *---------------------------------------------------------------------------*)
+ (*this function could be combined with define_i --lcp*)
fun simplify_defn (ss, tflCongs) (thy,(id,pats)) =
let val dummy = deny (id mem (Sign.stamp_names_of (Theory.sign_of thy)))
("Recursive definition " ^ id ^
@@ -230,6 +216,22 @@
"\n (In TFL function " ^ module ^ "." ^ func ^ ")");
(*---------------------------------------------------------------------------
+ * Defining a function with an associated termination relation.
+ *---------------------------------------------------------------------------*)
+ fun define_i thy fid R ss_congs eqs =
+ let val {functional,pats} = Prim.mk_functional thy eqs
+ val thy = Prim.wfrec_definition0 thy (Sign.base_name fid) R functional
+ in (thy, simplify_defn ss_congs (thy, (fid, pats)))
+ end;
+
+ fun define thy fid R ss_congs seqs =
+ let val _ = writeln ("Recursive function " ^ fid)
+ val read = readtm (Theory.sign_of thy) (TVar(("DUMMY",0),[]))
+ in define_i thy fid (read R) ss_congs (map read seqs) end
+ handle Utils.ERR {mesg,...} => error mesg;
+
+
+(*---------------------------------------------------------------------------
*
* Definitions with synthesized termination relation
*
@@ -245,7 +247,8 @@
let val {rules,R,theory,full_pats_TCs,SV,...} =
Prim.lazyR_def thy (Sign.base_name fid) congs eqs
val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules))
- val dummy = (message "Definition made."; message "Proving induction theorem ...");
+ val dummy = (message "Definition made.";
+ message "Proving induction theorem ...");
val induction = Prim.mk_induction theory
{fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs}
val dummy = message "Induction theorem proved."
@@ -256,10 +259,9 @@
end
fun defer thy fid congs seqs =
- let fun read thy = readtm (Theory.sign_of thy) (TVar(("DUMMY",0),[]))
- in defer_i thy fid congs (map (read thy) seqs) end
+ let val read = readtm (Theory.sign_of thy) (TVar(("DUMMY",0),[]))
+ in defer_i thy fid congs (map read seqs) end
handle Utils.ERR {mesg,...} => error mesg;
-
end;
end;
--- a/TFL/rules.sig Wed Aug 18 18:10:48 1999 +0200
+++ b/TFL/rules.sig Wed Aug 18 18:44:20 1999 +0200
@@ -49,6 +49,7 @@
val SUBS : thm list -> thm -> thm
val simpl_conv : simpset -> thm list -> cterm -> thm
+ val rbeta : thm -> thm
(* For debugging my isabelle solver in the conditional rewriter *)
val term_ref : term list ref
val thm_ref : thm list ref
--- a/TFL/rules.sml Wed Aug 18 18:10:48 1999 +0200
+++ b/TFL/rules.sml Wed Aug 18 18:44:20 1999 +0200
@@ -46,6 +46,10 @@
in equal_elim (transitive ctm2_eq ctm1_eq) thm
end;
+fun rbeta th =
+ case Dcterm.strip_comb (cconcl th)
+ of (eeq,[l,r]) => transitive th (beta_conversion r)
+ | _ => raise RULES_ERR{func="rbeta", mesg =""};
(*----------------------------------------------------------------------------
* typ instantiation
@@ -772,7 +776,8 @@
(if (is_cong thm) then cong_prover else restrict_prover) mss thm
end
val ctm = cprop_of th
- val th1 = Thm.rewrite_cterm(false,true,false) (add_congs(mss_of [cut_lemma'], congs))
+ val th1 = Thm.rewrite_cterm(false,true,false)
+ (add_congs(mss_of [cut_lemma'], congs))
prover ctm
val th2 = equal_elim th1 th
in
--- a/TFL/tfl.sml Wed Aug 18 18:10:48 1999 +0200
+++ b/TFL/tfl.sml Wed Aug 18 18:44:20 1999 +0200
@@ -16,6 +16,8 @@
structure S = USyntax;
structure U = S.Utils;
+fun TFL_ERR{func,mesg} = U.ERR{module = "Tfl", func = func, mesg = mesg};
+
val concl = #2 o R.dest_thm;
val hyp = #1 o R.dest_thm;
@@ -28,8 +30,14 @@
| stringize [i] = Int.toString i
| stringize (h::t) = (Int.toString h^", "^stringize t);
+fun front_last [] = raise TFL_ERR {func="front_last", mesg="empty list"}
+ | front_last [x] = ([],x)
+ | front_last (h::t) =
+ let val (pref,x) = front_last t
+ in
+ (h::pref,x)
+ end;
-fun TFL_ERR{func,mesg} = U.ERR{module = "Tfl", func = func, mesg = mesg};
(*---------------------------------------------------------------------------
@@ -48,7 +56,6 @@
-
(*---------------------------------------------------------------------------
* The next function is common to pattern-match translation and
* proof of completeness of cases for the induction theorem.
@@ -288,13 +295,16 @@
in check (FV_multiset pat)
end;
+fun dest_atom (Free p) = p
+ | dest_atom (Const p) = p
+ | dest_atom _ = raise TFL_ERR {func="dest_atom",
+ mesg="function name not an identifier"};
+
+
local fun mk_functional_err s = raise TFL_ERR{func = "mk_functional", mesg=s}
- fun single [Free(a,_)] =
- mk_functional_err (a ^ " has not been declared as a constant")
- | single [_$_] =
+ fun single [_$_] =
mk_functional_err "recdef does not allow currying"
- | single [Const arg] = arg
- | single [_] = mk_functional_err "recdef: bad function name"
+ | single [f] = f
| single fs = mk_functional_err (Int.toString (length fs) ^
" distinct function names!")
in
@@ -304,9 +314,10 @@
{func = "mk_functional",
mesg = "recursion equations must use the = relation"}
val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L)
- val (fname, ftype) = single (gen_distinct (op aconv) funcs)
+ val atom = single (gen_distinct (op aconv) funcs)
+ val (fname,ftype) = dest_atom atom
val dummy = map (no_repeat_vars thy) pats
- val rows = ListPair.zip (map (fn x => ([],[x])) pats,
+ val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats,
map GIVEN (enumerate R))
val names = foldr add_term_names (R,[])
val atype = type_of(hd pats)
@@ -327,8 +338,8 @@
| L => mk_functional_err("The following rows (counting from zero)\
\ are inaccessible: "^stringize L)
in {functional = Abs(Sign.base_name fname, ftype,
- abstract_over (Const(fname,ftype),
- absfree(aname, atype, case_tm))),
+ abstract_over (atom,
+ absfree(aname,atype, case_tm))),
pats = patts2}
end end;
@@ -439,27 +450,36 @@
(*---------------------------------------------------------------------------
* Perform the extraction without making the definition. Definition and
* extraction commute for the non-nested case. (Deferred recdefs)
+ *
+ * The purpose of wfrec_eqns is merely to instantiate the recursion theorem
+ * and extract termination conditions: no definition is made.
*---------------------------------------------------------------------------*)
+
fun wfrec_eqns thy fid tflCongs eqns =
- let val {functional as Abs(Name, Ty, _), pats} = mk_functional thy eqns
+ let val {lhs,rhs} = S.dest_eq (hd eqns)
+ val (f,args) = S.strip_comb lhs
+ val (fname,fty) = dest_atom f
+ val (SV,a) = front_last args (* SV = schematic variables *)
+ val g = list_comb(f,SV)
+ val h = Free(fname,type_of g)
+ val eqns1 = map (subst_free[(g,h)]) eqns
+ val {functional as Abs(Name, Ty, _), pats} = mk_functional thy eqns1
val given_pats = givens pats
- val f = #1 (S.strip_comb(#lhs(S.dest_eq (hd eqns))))
(* val f = Free(Name,Ty) *)
val Type("fun", [f_dty, f_rty]) = Ty
val dummy = if Name<>fid then
- raise TFL_ERR{func = "lazyR_def",
+ raise TFL_ERR{func = "wfrec_eqns",
mesg = "Expected a definition of " ^
quote fid ^ " but found one of " ^
quote Name}
else ()
- val SV = S.free_vars_lr functional (* schema variables *)
val (case_rewrites,context_congs) = extraction_thms thy
val tych = Thry.typecheck thy
val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
val Const("All",_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
val R = Free (variant (foldr add_term_names (eqns,[])) Rname,
Rtype)
- val WFREC_THM = R.ISPECL [tych R, tych f] WFREC_THM0
+ val WFREC_THM = R.ISPECL [tych R, tych g] WFREC_THM0
val ([proto_def, WFR],_) = S.strip_imp(concl WFREC_THM)
val dummy =
if !trace then
@@ -472,9 +492,11 @@
val corollaries' = map (rewrite_rule case_rewrites) corollaries
fun extract X = R.CONTEXT_REWRITE_RULE
(f, R1::SV, cut_apply, tflCongs@context_congs) X
- in {proto_def = (*Use == rather than = for definitions*)
+ in {proto_def = proto_def,
+ (*LCP: want this??
+ (*Use == rather than = for definitions*)
mk_const_def (Theory.sign_of thy)
- (Name, Ty, S.rhs proto_def),
+ (Name, Ty, S.rhs proto_def), *)
SV=SV,
WFR=WFR,
pats=pats,
@@ -488,11 +510,13 @@
* choice operator on the extracted conditions (plus the condition that
* such a relation must be wellfounded).
*---------------------------------------------------------------------------*)
+
fun lazyR_def thy fid tflCongs eqns =
let val {proto_def,WFR,pats,extracta,SV} =
wfrec_eqns thy fid (congs tflCongs) eqns
val R1 = S.rand WFR
- val f = #1 (Logic.dest_equals proto_def)
+ val f = #lhs(S.dest_eq proto_def)
+(*LCP: want this? val f = #1 (Logic.dest_equals proto_def) *)
val (extractants,TCl) = ListPair.unzip extracta
val dummy = if !trace
then (writeln "Extractants = ";
@@ -508,14 +532,26 @@
Sign.string_of_term
(Theory.sign_of thy) proto_def')
else ()
+ val {lhs,rhs} = S.dest_eq proto_def'
+ val (c,args) = S.strip_comb lhs
+ val (Name,Ty) = dest_atom c
+ val defn = mk_const_def (Theory.sign_of thy)
+ (Name, Ty, S.list_mk_abs (args,rhs))
+ (*LCP: want this??
val theory =
thy
|> PureThy.add_defs_i
[Thm.no_attributes (fid ^ "_def", proto_def')];
val def = get_axiom theory (fid ^ "_def") RS meta_eq_to_obj_eq
+ *)
+ val theory =
+ thy
+ |> PureThy.add_defs_i
+ [Thm.no_attributes (fid ^ "_def", defn)]
+ val def = freezeT (get_axiom theory (fid ^ "_def"))
val dummy = if !trace then writeln ("DEF = " ^ string_of_thm def)
else ()
- val fconst = #lhs(S.dest_eq(concl def))
+ (* val fconst = #lhs(S.dest_eq(concl def)) *)
val tych = Thry.typecheck theory
val full_rqt_prop = map (Dcterm.mk_prop o tych) full_rqt
(*lcp: a lot of object-logic inference to remove*)
@@ -525,10 +561,12 @@
val dum = if !trace then writeln ("baz = " ^ string_of_thm baz)
else ()
val f_free = Free (fid, fastype_of f) (*'cos f is a Const*)
- val def' = R.MP (R.SPEC (tych fconst)
- (R.SPEC (tych R')
- (R.GENL[tych R1, tych f_free] baz)))
- def
+ val SV' = map tych SV;
+ val SVrefls = map reflexive SV'
+ val def0 = (U.rev_itlist (fn x => fn th => R.rbeta(combination th x))
+ SVrefls def)
+ RS meta_eq_to_obj_eq
+ val def' = R.MP (R.SPEC (tych R') (R.GEN (tych R1) baz)) def0
val body_th = R.LIST_CONJ (map R.ASSUME full_rqt_prop)
val bar = R.MP (R.ISPECL[tych R'abs, tych R1] Thms.SELECT_AX)
body_th
@@ -888,13 +926,13 @@
* 3. replace tc by tc' in both the rules and the induction theorem.
*---------------------------------------------------------------------*)
-fun print_thms s L =
- if !trace then writeln (cat_lines (s :: map string_of_thm L))
- else ();
+ fun print_thms s L =
+ if !trace then writeln (cat_lines (s :: map string_of_thm L))
+ else ();
-fun print_cterms s L =
- if !trace then writeln (cat_lines (s :: map string_of_cterm L))
- else ();;
+ fun print_cterms s L =
+ if !trace then writeln (cat_lines (s :: map string_of_cterm L))
+ else ();;
fun simplify_tc tc (r,ind) =
let val tc1 = tych tc
--- a/src/HOL/Tools/recdef_package.ML Wed Aug 18 18:10:48 1999 +0200
+++ b/src/HOL/Tools/recdef_package.ML Wed Aug 18 18:44:20 1999 +0200
@@ -85,8 +85,8 @@
val ss = (case raw_ss of None => Simplifier.simpset_of thy | Some x => prep_ss x);
val (thy1, congs) = thy |> app_thms raw_congs;
- val (thy2, pats) = tfl_fn thy1 name R eqs;
- val (result as {rules, induct, tcs}) = Tfl.simplify_defn (ss, congs) (thy2, (name, pats));
+ val (thy2, result as {rules, induct, tcs}) =
+ tfl_fn thy1 name R (ss, congs) eqs
val thy3 =
thy2
|> Theory.add_path bname