# HG changeset patch # User paulson # Date 934994660 -7200 # Node ID a05dc63ca29bdf4f08175708c8c67af5fcfeb55a # Parent a141985d660bdef9b03e79e021d207876dab7e59 from Konrad: support for schematic definitions diff -r a141985d660b -r a05dc63ca29b TFL/post.sml --- 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; diff -r a141985d660b -r a05dc63ca29b TFL/rules.sig --- 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 diff -r a141985d660b -r a05dc63ca29b TFL/rules.sml --- 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 diff -r a141985d660b -r a05dc63ca29b TFL/tfl.sml --- 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 diff -r a141985d660b -r a05dc63ca29b src/HOL/Tools/recdef_package.ML --- 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