Numerous simplifications and removal of HOL-isms
Addition of the "simpset" feature (replacing references to \!simpset)
--- a/TFL/dcterm.sml Thu Jun 05 13:26:09 1997 +0200
+++ b/TFL/dcterm.sml Thu Jun 05 13:27:28 1997 +0200
@@ -35,8 +35,6 @@
val is_let : cterm -> bool
val is_neg : cterm -> bool
val is_pair : cterm -> bool
- val list_mk_abs : cterm list -> cterm -> cterm
- val list_mk_exists : cterm list * cterm -> cterm
val list_mk_disj : cterm list -> cterm
val strip_abs : cterm -> cterm list * cterm
val strip_comb : cterm -> cterm * cterm list
@@ -57,14 +55,6 @@
val can = Utils.can;
fun swap (x,y) = (y,x);
-fun itlist f L base_value =
- let fun it [] = base_value
- | it (a::rst) = f a (it rst)
- in it L
- end;
-
-val end_itlist = Utils.end_itlist;
-
(*---------------------------------------------------------------------------
* Some simple constructor functions.
@@ -164,10 +154,7 @@
(*---------------------------------------------------------------------------
* Iterated creation.
*---------------------------------------------------------------------------*)
-val list_mk_abs = itlist cabs;
-
-fun list_mk_exists(V,t) = itlist(fn v => fn b => mk_exists(v, b)) V t;
-val list_mk_disj = end_itlist(fn d1 => fn tm => mk_disj(d1, tm))
+val list_mk_disj = Utils.end_itlist(fn d1 => fn tm => mk_disj(d1, tm))
(*---------------------------------------------------------------------------
* Iterated destruction. (To the "right" in a term.)
--- a/TFL/post.sml Thu Jun 05 13:26:09 1997 +0200
+++ b/TFL/post.sml Thu Jun 05 13:27:28 1997 +0200
@@ -6,13 +6,6 @@
Postprocessing of TFL definitions
*)
-(*-------------------------------------------------------------------------
-Three postprocessors are applied to the definition:
- - a wellfoundedness prover (WF_TAC)
- - a simplifier (tries to eliminate the language of termination expressions)
- - a termination prover
-*-------------------------------------------------------------------------*)
-
signature TFL =
sig
structure Prim : TFL_sig
@@ -20,20 +13,17 @@
val tgoalw : theory -> thm list -> thm list -> thm list
val tgoal: theory -> thm list -> thm list
- val WF_TAC : thm list -> tactic
-
- val simplifier : thm -> thm
- val std_postprocessor : theory
+ val std_postprocessor : simpset -> theory
-> {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 * (thm * Prim.pattern list)
+ -> theory * Prim.pattern list
val define : theory -> string -> string -> string list
-> theory * Prim.pattern list
- val simplify_defn : theory * (string * Prim.pattern list)
+ val simplify_defn : simpset -> theory * (string * Prim.pattern list)
-> {rules:thm list, induct:thm, tcs:term list}
(*-------------------------------------------------------------------------
@@ -56,51 +46,38 @@
* have a tactic directly applied to them.
*--------------------------------------------------------------------------*)
fun termination_goals rules =
- map (Logic.freeze_vars o HOLogic.dest_Trueprop)
+ map (#1 o Type.freeze_thaw o HOLogic.dest_Trueprop)
(foldr (fn (th,A) => union_term (prems_of th, A)) (rules, []));
- (*---------------------------------------------------------------------------
- * Finds the termination conditions in (highly massaged) definition and
- * puts them into a goalstack.
- *--------------------------------------------------------------------------*)
- fun tgoalw thy defs rules =
- let val L = termination_goals rules
- open USyntax
- val g = cterm_of (sign_of thy) (HOLogic.mk_Trueprop(list_mk_conj L))
- in goalw_cterm defs g
- end;
+(*---------------------------------------------------------------------------
+ * Finds the termination conditions in (highly massaged) definition and
+ * puts them into a goalstack.
+ *--------------------------------------------------------------------------*)
+fun tgoalw thy defs rules =
+ let val L = termination_goals rules
+ open USyntax
+ val g = cterm_of (sign_of thy) (HOLogic.mk_Trueprop(list_mk_conj L))
+ in goalw_cterm defs g
+ end;
- fun tgoal thy = tgoalw thy [];
-
- (*---------------------------------------------------------------------------
- * Simple wellfoundedness prover.
- *--------------------------------------------------------------------------*)
- fun WF_TAC thms = REPEAT(FIRST1(map rtac thms))
- val WFtac = WF_TAC[wf_measure, wf_inv_image, wf_lex_prod, wf_less_than,
- wf_trancl];
+fun tgoal thy = tgoalw thy [];
- val terminator = simp_tac(!simpset addsimps [less_Suc_eq]) 1
- THEN TRY(best_tac
- (!claset addSDs [not0_implies_Suc]
- addss (!simpset)) 1);
-
- val simpls = [less_eq RS eq_reflection,
- lex_prod_def, measure_def, inv_image_def];
+(*---------------------------------------------------------------------------
+* Three postprocessors are applied to the definition. It
+* attempts to prove wellfoundedness of the given relation, simplifies the
+* non-proved termination conditions, and finally attempts to prove the
+* simplified termination conditions.
+*--------------------------------------------------------------------------*)
+fun std_postprocessor ss =
+ Prim.postprocess
+ {WFtac = REPEAT (ares_tac [wf_measure, wf_inv_image, wf_lex_prod,
+ wf_less_than, wf_trancl] 1),
+ terminator = asm_simp_tac ss 1
+ THEN TRY(best_tac
+ (!claset addSDs [not0_implies_Suc] addss ss) 1),
+ simplifier = Rules.simpl_conv ss []};
- (*---------------------------------------------------------------------------
- * Does some standard things with the termination conditions of a definition:
- * attempts to prove wellfoundedness of the given relation; simplifies the
- * non-proven termination conditions; and finally attempts to prove the
- * simplified termination conditions.
- *--------------------------------------------------------------------------*)
- val std_postprocessor = Prim.postprocess{WFtac = WFtac,
- terminator = terminator,
- simplifier = Rules.simpl_conv simpls};
-
- val simplifier = rewrite_rule (simpls @ #simps(rep_ss (!simpset)) @
- [pred_list_def]);
-
- fun tflcongs thy = Prim.Context.read() @ (#case_congs(Thry.extract_info thy));
+fun tflcongs thy = Prim.Context.read() @ (#case_congs(Thry.extract_info thy));
val concl = #2 o Rules.dest_thm;
@@ -111,17 +88,14 @@
fun define_i thy fid R eqs =
let val dummy = require_thy thy "WF_Rel" "recursive function definitions"
val {functional,pats} = Prim.mk_functional thy eqs
- val (thm,thry) = Prim.wfrec_definition0 thy fid R functional
- in (thry,(thm,pats))
+ in (Prim.wfrec_definition0 thy fid R functional, pats)
end;
(*lcp's version: takes strings; doesn't return "thm"
(whose signature is a draft and therefore useless) *)
fun define thy fid R eqs =
let fun read thy = readtm (sign_of thy) (TVar(("DUMMY",0),[]))
- val (thy',(_,pats)) =
- define_i thy fid (read thy R) (map (read thy) eqs)
- in (thy',pats) end
+ in define_i thy fid (read thy R) (map (read thy) eqs) end
handle Utils.ERR {mesg,...} => error mesg;
(*---------------------------------------------------------------------------
@@ -147,8 +121,9 @@
Const("==",_)$_$_ => r
| _$(Const("op =",_)$_$_) => r RS eq_reflection
| _ => r RS P_imp_P_eq_True
+
+(*Is this the best way to invoke the simplifier??*)
fun rewrite L = rewrite_rule (map mk_meta_eq (filter(not o id_thm) L))
-fun reducer thl = rewrite (map standard thl @ #simps(rep_ss (!simpset)))
fun join_assums th =
let val {sign,...} = rep_thm th
@@ -164,17 +139,12 @@
end
val gen_all = S.gen_all
in
-(*---------------------------------------------------------------------------
- * The "reducer" argument is
- * (fn thl => rewrite (map standard thl @ #simps(rep_ss (!simpset))));
- *---------------------------------------------------------------------------*)
-fun proof_stage theory reducer {f, R, rules, full_pats_TCs, TCs} =
+fun proof_stage ss theory {f, R, rules, full_pats_TCs, TCs} =
let val dummy = prs "Proving induction theorem.. "
val ind = Prim.mk_induction theory f R full_pats_TCs
- val dummy = writeln "Proved induction theorem."
- val pp = std_postprocessor theory
- val dummy = prs "Postprocessing.. "
- val {rules,induction,nested_tcs} = pp{rules=rules,induction=ind,TCs=TCs}
+ val dummy = prs "Proved induction theorem.\nPostprocessing.. "
+ val {rules, induction, nested_tcs} =
+ std_postprocessor ss theory {rules=rules, induction=ind, TCs=TCs}
in
case nested_tcs
of [] => (writeln "Postprocessing done.";
@@ -186,8 +156,9 @@
if (solved th) then (th::So, Si, St)
else (So, th::Si, St)) nested_tcs ([],[],[])
val simplified' = map join_assums simplified
- val induction' = reducer (solved@simplified') induction
- val rules' = reducer (solved@simplified') rules
+ val rewr = rewrite (solved @ simplified' @ #simps(rep_ss ss))
+ val induction' = rewr induction
+ and rules' = rewr rules
val dummy = writeln "Postprocessing done."
in
{induction = induction',
@@ -212,18 +183,20 @@
(*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];
-fun simplify_defn (thy,(id,pats)) =
+fun simplify_defn ss (thy,(id,pats)) =
let val dummy = deny (id mem map ! (stamps_of_thy thy))
("Recursive definition " ^ id ^
" would clash with the theory of the same name!")
- val def = freezeT(get_def thy id RS meta_eq_to_obj_eq)
+ val def = freezeT(get_def thy id) RS meta_eq_to_obj_eq
+ val ss' = ss addsimps ((less_Suc_eq RS iffD2) :: wf_rel_defs)
val {theory,rules,TCs,full_pats_TCs,patterns} =
- Prim.post_definition (thy,(def,pats))
+ Prim.post_definition ss' (thy,(def,pats))
val {lhs=f,rhs} = S.dest_eq(concl def)
val (_,[R,_]) = S.strip_comb rhs
val {induction, rules, tcs} =
- proof_stage theory reducer
+ proof_stage ss' theory
{f = f, R = R, rules = rules,
full_pats_TCs = full_pats_TCs,
TCs = TCs}
@@ -235,8 +208,7 @@
end
handle Utils.ERR {mesg,func,module} =>
error (mesg ^
- "\n (In TFL function " ^ module ^ "." ^ func ^ ")")
- | e => print_exn e;
+ "\n (In TFL function " ^ module ^ "." ^ func ^ ")");
end;
(*---------------------------------------------------------------------------
@@ -260,7 +232,6 @@
in {theory = theory,
eq_ind = standard (induction RS (rules RS conjI))}
end
- handle e => print_exn e
end;
--- a/TFL/rules.new.sml Thu Jun 05 13:26:09 1997 +0200
+++ b/TFL/rules.new.sml Thu Jun 05 13:27:28 1997 +0200
@@ -282,19 +282,6 @@
end;
-local fun string_of(s,_) = s
-in
-fun freeze th =
- let val fth = freezeT th
- val {prop,sign,...} = rep_thm fth
- fun mk_inst (Var(v,T)) =
- (cterm_of sign (Var(v,T)),
- cterm_of sign (Free(string_of v, T)))
- val insts = map mk_inst (term_vars prop)
- in instantiate ([],insts) fth
- end
-end;
-
fun MATCH_MP th1 th2 =
if (D.is_forall (D.drop_prop(cconcl th1)))
then MATCH_MP (th1 RS spec) th2
@@ -326,8 +313,8 @@
fun CHOOSE(fvar,exth) fact =
let val lam = #2(dest_comb(D.drop_prop(cconcl exth)))
val redex = capply lam fvar
- val {sign,t,...} = rep_cterm redex
- val residue = cterm_of sign (S.beta_conv t)
+ val {sign, t = t$u,...} = rep_cterm redex
+ val residue = cterm_of sign (betapply(t,u))
in GEN fvar (DISCH residue fact) RS (exth RS choose_thm)
end
end;
@@ -403,12 +390,10 @@
fun SUBS thl =
rewrite_rule (map (fn th => (th RS eq_reflection) handle _ => th) thl);
-val simplify = rewrite_rule;
-
local fun rew_conv mss = rewrite_cterm (true,false) mss (K(K None))
in
-fun simpl_conv thl ctm =
- rew_conv (Thm.mss_of (#simps(rep_ss (!simpset))@thl)) ctm
+fun simpl_conv ss thl ctm =
+ rew_conv (Thm.mss_of (#simps(rep_ss ss)@thl)) ctm
RS meta_eq_to_obj_eq
end;
@@ -449,13 +434,6 @@
fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm));
-fun variants FV vlist =
- rev(#1(U.rev_itlist (fn v => fn (V,W) =>
- let val v' = S.variant W v
- in (v'::V, v'::W) end)
- vlist ([],FV)));
-
-
fun dest_all(Const("all",_) $ (a as Abs _)) = S.dest_abs a
| dest_all _ = raise RULES_ERR{func = "dest_all", mesg = "not a !!"};
@@ -501,8 +479,8 @@
let val eq = Logic.strip_imp_concl body
val (f,args) = S.strip_comb (get_lhs eq)
val (vstrl,_) = S.strip_abs f
- val names = map (#1 o dest_Free)
- (variants (term_frees body) vstrl)
+ val names = variantlist (map (#1 o dest_Free) vstrl,
+ add_term_names(body, []))
in get (rst, n+1, (names,n)::L)
end handle _ => get (rst, n+1, L);
@@ -648,12 +626,13 @@
in (ants,get_lhs eq)
end;
-val pbeta_reduce = simpl_conv [split RS eq_reflection];
-val restricted = U.can(S.find_term
- (U.holds(fn c => (#Name(S.dest_const c)="cut"))))
+fun restricted t = is_some (S.find_term
+ (fn (Const("cut",_)) =>true | _ => false)
+ t)
-fun CONTEXT_REWRITE_RULE(func,R){cut_lemma, congs, th} =
- let val tc_list = ref[]: term list ref
+fun CONTEXT_REWRITE_RULE (ss, func, R, cut_lemma, congs) th =
+ let val pbeta_reduce = simpl_conv ss [split RS eq_reflection];
+ val tc_list = ref[]: term list ref
val dummy = term_ref := []
val dummy = thm_ref := []
val dummy = mss_ref := []
@@ -761,11 +740,9 @@
* term "f v1..vn" which is a pattern that any full application
* of "f" will match.
*-------------------------------------------------------------*)
- val func_name = #1(dest_Const func handle _ => dest_Free func)
- fun is_func tm = (#1(dest_Const tm handle _ => dest_Free tm)
- = func_name)
- handle _ => false
- val nested = U.can(S.find_term is_func)
+ val func_name = #1(dest_Const func)
+ fun is_func (Const (name,_)) = (name = func_name)
+ | is_func _ = false
val rcontext = rev cntxt
val cncl = HOLogic.dest_Trueprop o #prop o rep_thm
val antl = case rcontext of [] => []
@@ -775,7 +752,7 @@
val dummy = print_cterms "TC:\n"
[cterm_of sign (HOLogic.mk_Trueprop TC)]
val dummy = tc_list := (TC :: !tc_list)
- val nestedp = nested TC
+ val nestedp = is_some (S.find_term is_func TC)
val dummy = if nestedp then say"nested\n" else say"not_nested\n"
val dummy = term_ref := ([func,TC]@(!term_ref))
val th' = if nestedp then raise RULES_ERR{func = "solver",
@@ -803,12 +780,8 @@
-fun prove (tm,tac) =
- let val {t,sign,...} = rep_cterm tm
- val ptm = cterm_of sign(HOLogic.mk_Trueprop t)
- in
- freeze(prove_goalw_cterm [] ptm (fn _ => [tac]))
- end;
+fun prove (ptm,tac) =
+ #1 (freeze_thaw (prove_goalw_cterm [] ptm (fn _ => [tac])));
end; (* Rules *)
--- a/TFL/rules.sig Thu Jun 05 13:26:09 1997 +0200
+++ b/TFL/rules.sig Thu Jun 05 13:27:28 1997 +0200
@@ -46,17 +46,15 @@
val DISJ_CASESL : thm -> thm list -> thm
val SUBS : thm list -> thm -> thm
- val simplify : thm list -> thm -> thm
- val simpl_conv : thm list -> cterm -> thm
+ val simpl_conv : simpset -> thm list -> cterm -> thm
(* For debugging my isabelle solver in the conditional rewriter *)
val term_ref : term list ref
val thm_ref : thm list ref
val mss_ref : meta_simpset list ref
val tracing :bool ref
- val CONTEXT_REWRITE_RULE : term * term
- -> {cut_lemma:thm, congs: thm list, th:thm}
- -> thm * term list
+ val CONTEXT_REWRITE_RULE : simpset * term * term * thm * thm list
+ -> thm -> thm * term list
val RIGHT_ASSOC : thm -> thm
val prove : cterm * tactic -> thm
--- a/TFL/tfl.sig Thu Jun 05 13:26:09 1997 +0200
+++ b/TFL/tfl.sig Thu Jun 05 13:27:28 1997 +0200
@@ -15,23 +15,22 @@
-> {functional:term,
pats: pattern list}
- val wfrec_definition0 : theory -> string -> term -> term -> thm * theory
+ val wfrec_definition0 : theory -> string -> term -> term -> theory
- val post_definition : theory * (thm * pattern list)
- -> {theory : theory,
- rules : thm,
- TCs : term list list,
- full_pats_TCs : (term * term list) list,
- patterns : pattern list}
+ val post_definition : simpset -> theory * (thm * pattern list)
+ -> {theory : theory,
+ rules : thm,
+ TCs : term list list,
+ full_pats_TCs : (term * term list) list,
+ patterns : pattern list}
-
+(*CURRENTLY UNUSED
val wfrec_eqns : theory -> term list
-> {WFR : term,
proto_def : term,
extracta :(thm * term list) list,
pats : pattern list}
-
val lazyR_def : theory
-> term list
-> {theory:theory,
@@ -39,11 +38,9 @@
R :term,
full_pats_TCs :(term * term list) list,
patterns: pattern list}
+---------------------*)
- val mk_induction : theory
- -> term -> term
- -> (term * term list) list
- -> thm
+ val mk_induction : theory -> term -> term -> (term * term list) list -> thm
val postprocess: {WFtac:tactic, terminator:tactic, simplifier:cterm -> thm}
-> theory
--- a/TFL/tfl.sml Thu Jun 05 13:26:09 1997 +0200
+++ b/TFL/tfl.sml Thu Jun 05 13:27:28 1997 +0200
@@ -43,12 +43,12 @@
* proof of completeness of cases for the induction theorem.
*
* The curried function "gvvariant" returns a function to generate distinct
- * variables that are guaranteed not to be in vlist. The names of
+ * variables that are guaranteed not to be in names. The names of
* the variables go u, v, ..., z, aa, ..., az, ... The returned
* function contains embedded refs!
*---------------------------------------------------------------------------*)
-fun gvvariant vlist =
- let val slist = ref (map (#1 o dest_Free) vlist)
+fun gvvariant names =
+ let val slist = ref names
val vname = ref "u"
fun new() =
if !vname mem_string (!slist)
@@ -189,10 +189,10 @@
* incomplete set of patterns is given.
*---------------------------------------------------------------------------*)
-fun mk_case ty_info ty_match FV range_ty =
+fun mk_case ty_info ty_match usednames range_ty =
let
fun mk_case_fail s = raise TFL_ERR{func = "mk_case", mesg = s}
- val fresh_var = gvvariant FV
+ val fresh_var = gvvariant usednames
val divide = partition fresh_var ty_match
fun expand constructors ty ((_,[]), _) = mk_case_fail"expand_var_row"
| expand constructors ty (row as ((prefix, p::rst), rhs)) =
@@ -285,19 +285,18 @@
let val (L,R) = ListPair.unzip
(map (fn (Const("op =",_) $ t $ u) => (t,u)) clauses)
val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L)
- val f = single (gen_distinct (op aconv) funcs)
- (**??why change the Const to a Free??????????????**)
- val fvar = if (is_Free f) then f else Free(dest_Const f)
+ val fcon as Const (fname, ftype) = single (gen_distinct (op aconv) funcs)
val dummy = map (no_repeat_vars thy) pats
val rows = ListPair.zip (map (fn x => ([],[x])) pats,
map GIVEN (enumerate R))
- val fvs = S.free_varsl R
- val a = S.variant fvs (Free("a",type_of(hd pats)))
- val FV = a::fvs
+ val names = foldr add_term_names (R,[])
+ val atype = type_of(hd pats)
+ and aname = variant names "a"
+ val a = Free(aname,atype)
val ty_info = Thry.match_info thy
val ty_match = Thry.match_type thy
val range_ty = type_of (hd R)
- val (patts, case_tm) = mk_case ty_info ty_match FV range_ty
+ val (patts, case_tm) = mk_case ty_info ty_match (aname::names) range_ty
{path=[a], rows=rows}
val patts1 = map (fn (_,(tag,i),[pat]) => tag (pat,i)) patts
handle _ => mk_functional_err "error in pattern-match translation"
@@ -308,8 +307,9 @@
of [] => ()
| L => mk_functional_err("The following rows (counting from zero)\
\ are inaccessible: "^stringize L)
- val case_tm' = subst_free [(f,fvar)] case_tm
- in {functional = S.list_mk_abs ([fvar,a], case_tm'),
+ in {functional = Abs(fname, ftype,
+ abstract_over (fcon,
+ absfree(aname,atype, case_tm))),
pats = patts2}
end end;
@@ -326,10 +326,6 @@
| poly_tvars (TFree (a,sort)) = TVar (("?" ^ a, 0), sort)
| poly_tvars (TVar ((a,i),sort)) = TVar (("?" ^ a, i+1), sort);
-
-(*---------------------------------------------------------------------------
- * R is already assumed to be type-copacetic with M
- *---------------------------------------------------------------------------*)
local val f_eq_wfrec_R_M =
#ant(S.dest_imp(#2(S.strip_forall (concl Thms.WFREC_COROLLARY))))
val {lhs=f, rhs} = S.dest_eq f_eq_wfrec_R_M
@@ -348,12 +344,9 @@
$ functional
val (_, def_term, _) =
Sign.infer_types (sign_of thy) (K None) (K None) [] false
- ([HOLogic.mk_eq(Const(Name,Ty), wfrec_R_M)],
- HOLogic.boolT)
-
- in
- Thry.make_definition thy def_name def_term
- end
+ ([Const("==",dummyT) $ Const(Name,Ty) $ wfrec_R_M],
+ propT)
+ in add_defs_i [(def_name, def_term)] thy end
end;
@@ -396,15 +389,11 @@
end;
-(*Replace all TFrees by TVars [CURRENTLY UNUSED]*)
-val tvars_of_tfrees =
- map_term_types (map_type_tfree (fn (a,sort) => TVar ((a, 0), sort)));
-
fun givens [] = []
| givens (GIVEN(tm,_)::pats) = tm :: givens pats
| givens (OMITTED _::pats) = givens pats;
-fun post_definition (theory, (def, pats)) =
+fun post_definition ss (theory, (def, pats)) =
let val tych = Thry.typecheck theory
val f = #lhs(S.dest_eq(concl def))
val corollary = R.MATCH_MP Thms.WFREC_COROLLARY def
@@ -415,14 +404,14 @@
val corollaries = map (fn pat => R.SPEC (tych pat) corollary')
given_pats
val (case_rewrites,context_congs) = extraction_thms theory
- val corollaries' = map(R.simplify case_rewrites) corollaries
- fun xtract th = R.CONTEXT_REWRITE_RULE(f,R)
- {cut_lemma = R.ISPECL (map tych [f,R]) Thms.CUT_LEMMA,
- congs = context_congs,
- th = th}
- val (rules, TCs) = ListPair.unzip (map xtract corollaries')
- val rules0 = map (R.simplify [Thms.CUT_DEF]) rules
- val mk_cond_rule = R.FILTER_DISCH_ALL(not o S.aconv WFR)
+ val corollaries' = map(rewrite_rule case_rewrites) corollaries
+ val extract = R.CONTEXT_REWRITE_RULE
+ (ss, f, R,
+ R.ISPECL (map tych [f,R]) Thms.CUT_LEMMA,
+ context_congs)
+ val (rules, TCs) = ListPair.unzip (map extract corollaries')
+ val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules
+ val mk_cond_rule = R.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
val rules1 = R.LIST_CONJ(map mk_cond_rule rules0)
in
{theory = theory, (* holds def, if it's needed *)
@@ -437,8 +426,8 @@
* Perform the extraction without making the definition. Definition and
* extraction commute for the non-nested case. For hol90 users, this
* function can be invoked without being in draft mode.
- *---------------------------------------------------------------------------*)
-fun wfrec_eqns thy eqns =
+ * CURRENTLY UNUSED
+fun wfrec_eqns ss thy eqns =
let val {functional,pats} = mk_functional thy eqns
val given_pats = givens pats
val {Bvar = f, Body} = S.dest_abs functional
@@ -447,23 +436,25 @@
val (case_rewrites,context_congs) = extraction_thms thy
val tych = Thry.typecheck thy
val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
- val R = S.variant(foldr add_term_frees (eqns,[]))
- (#Bvar(S.dest_forall(concl WFREC_THM0)))
+ 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 ([proto_def, WFR],_) = S.strip_imp(concl WFREC_THM)
val R1 = S.rand WFR
val corollary' = R.UNDISCH(R.UNDISCH WFREC_THM)
- val corollaries = map (U.C R.SPEC corollary' o tych) given_pats
- val corollaries' = map (R.simplify case_rewrites) corollaries
- fun extract th = R.CONTEXT_REWRITE_RULE(f,R1)
- {cut_lemma = R.ISPECL (map tych [f,R1]) Thms.CUT_LEMMA,
- congs = context_congs,
- th = th}
+ val corollaries = map (fn pat => R.SPEC (tych pat) corollary') given_pats
+ val corollaries' = map (rewrite_rule case_rewrites) corollaries
+ val extract = R.CONTEXT_REWRITE_RULE
+ (ss, f, R1,
+ R.ISPECL (map tych [f,R1]) Thms.CUT_LEMMA,
+ context_congs)
in {proto_def=proto_def,
WFR=WFR,
pats=pats,
extracta = map extract corollaries'}
end;
+ *---------------------------------------------------------------------------*)
(*---------------------------------------------------------------------------
@@ -471,9 +462,9 @@
* wellfounded relation used in the definition is computed by using the
* choice operator on the extracted conditions (plus the condition that
* such a relation must be wellfounded).
- *---------------------------------------------------------------------------*)
-fun lazyR_def thy eqns =
- let val {proto_def,WFR,pats,extracta} = wfrec_eqns thy eqns
+ * CURRENTLY UNUSED
+fun lazyR_def ss thy eqns =
+ let val {proto_def,WFR,pats,extracta} = wfrec_eqns ss thy eqns
val R1 = S.rand WFR
val f = S.lhs proto_def
val (Name,_) = dest_Free f
@@ -482,8 +473,9 @@
val full_rqt = WFR::TCs
val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
val R'abs = S.rand R'
- val (def,theory) = Thry.make_definition thy (Name ^ "_def")
- (subst_free[(R1,R')] proto_def)
+ val theory = add_defs_i [(Name ^ "_def", subst_free[(R1,R')] proto_def)]
+ thy
+ val def = freezeT((get_axiom theory (Name ^ "_def")) RS meta_eq_to_obj_eq)
val fconst = #lhs(S.dest_eq(concl def))
val tych = Thry.typecheck theory
val baz = R.DISCH (tych proto_def)
@@ -499,6 +491,7 @@
full_pats_TCs = merge (map pat_of pats) (ListPair.zip (givens pats, TCl)),
patterns = pats}
end;
+ *---------------------------------------------------------------------------*)
@@ -535,10 +528,10 @@
val args = map (fn qv => the (gen_assoc (op aconv) (plist, qv))) qvars
handle OPTION _ => error
"TFL fault [alpha_ex_unroll]: no correspondence"
- fun build ex [] = []
- | build ex (v::rst) =
- let val ex1 = S.beta_conv(S.mk_comb{Rator=S.rand ex, Rand=v})
- in ex1::build ex1 rst
+ fun build ex [] = []
+ | build (_$rex) (v::rst) =
+ let val ex1 = betapply(rex, v)
+ in ex1 :: build ex1 rst
end
val (nex::exl) = rev (tm::build tm args)
in
@@ -553,9 +546,9 @@
*
*---------------------------------------------------------------------------*)
-fun mk_case ty_info FV thy =
+fun mk_case ty_info usednames thy =
let
- val divide = ipartition (gvvariant FV)
+ val divide = ipartition (gvvariant usednames)
val tych = Thry.typecheck thy
fun tych_binding(x,y) = (tych x, tych y)
fun fail s = raise TFL_ERR{func = "mk_case", mesg = s}
@@ -608,11 +601,12 @@
let val tych = Thry.typecheck thy
val ty_info = Thry.induct_info thy
in fn pats =>
- let val FV0 = S.free_varsl pats
+ let val names = foldr add_term_names (pats,[])
val T = type_of (hd pats)
- val a = S.variant FV0 (Free ("a", T))
- val v = S.variant (a::FV0) (Free ("v", T))
- val FV = a::v::FV0
+ val aname = Term.variant names "a"
+ val vname = Term.variant (aname::names) "v"
+ val a = Free (aname, T)
+ val v = Free (vname, T)
val a_eq_v = HOLogic.mk_eq(a,v)
val ex_th0 = R.EXISTS (tych (S.mk_exists{Bvar=v,Body=a_eq_v}), tych a)
(R.REFL (tych a))
@@ -622,7 +616,8 @@
R.GEN (tych a)
(R.RIGHT_ASSOC
(R.CHOOSE(tych v, ex_th0)
- (mk_case ty_info FV thy {path=[v], rows=rows})))
+ (mk_case ty_info (vname::aname::names)
+ thy {path=[v], rows=rows})))
end end;
@@ -636,29 +631,28 @@
* Note. When the context is empty, there can be no local variables.
*---------------------------------------------------------------------------*)
-local nonfix ^ ; infix 9 ^ ; infix 5 ==>
- fun (tm1 ^ tm2) = S.mk_comb{Rator = tm1, Rand = tm2}
+local infix 5 ==>
fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2}
in
fun build_ih f P (pat,TCs) =
let val globals = S.free_vars_lr pat
- fun nested tm = U.can(S.find_term (S.aconv f)) tm handle _ => false
+ fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
fun dest_TC tm =
let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm))
val (R,y,_) = S.dest_relation R_y_pat
- val P_y = if (nested tm) then R_y_pat ==> P^y else P^y
+ val P_y = if (nested tm) then R_y_pat ==> P$y else P$y
in case cntxt
of [] => (P_y, (tm,[]))
| _ => let
val imp = S.list_mk_conj cntxt ==> P_y
val lvs = gen_rems (op aconv) (S.free_vars_lr imp, globals)
- val locals = #2(U.pluck (S.aconv P) lvs) handle _ => lvs
+ val locals = #2(U.pluck (curry (op aconv) P) lvs) handle _ => lvs
in (S.list_mk_forall(locals,imp), (tm,locals)) end
end
in case TCs
- of [] => (S.list_mk_forall(globals, P^pat), [])
+ of [] => (S.list_mk_forall(globals, P$pat), [])
| _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs)
- val ind_clause = S.list_mk_conj ihs ==> P^pat
+ val ind_clause = S.list_mk_conj ihs ==> P$pat
in (S.list_mk_forall(globals,ind_clause), TCs_locals)
end
end
@@ -678,7 +672,7 @@
let val tych = Thry.typecheck thy
val antc = tych(#ant(S.dest_imp tm))
val thm' = R.SPEC_ALL thm
- fun nested tm = U.can(S.find_term (S.aconv f)) tm handle _ => false
+ fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
fun get_cntxt TC = tych(#ant(S.dest_imp(#2(S.strip_forall(concl TC)))))
fun mk_ih ((TC,locals),th2,nested) =
R.GENL (map tych locals)
@@ -723,9 +717,6 @@
in #2 (U.itlist CHOOSER L (veq,thm)) end;
-fun combize M N = S.mk_comb{Rator=M,Rand=N};
-
-
(*----------------------------------------------------------------------------
* Input : f, R, and [(pat1,TCs1),..., (patn,TCsn)]
*
@@ -739,18 +730,20 @@
val (pats,TCsl) = ListPair.unzip pat_TCs_list
val case_thm = complete_cases thy pats
val domain = (type_of o hd) pats
- val P = S.variant (S.all_varsl (pats @ List_.concat TCsl))
- (Free("P",domain --> HOLogic.boolT))
+ val Pname = Term.variant (foldr (foldr add_term_names)
+ (pats::TCsl, [])) "P"
+ val P = Free(Pname, domain --> HOLogic.boolT)
val Sinduct = R.SPEC (tych P) Sinduction
val Sinduct_assumf = S.rand ((#ant o S.dest_imp o concl) Sinduct)
val Rassums_TCl' = map (build_ih f P) pat_TCs_list
val (Rassums,TCl') = ListPair.unzip Rassums_TCl'
val Rinduct_assum = R.ASSUME (tych (S.list_mk_conj Rassums))
- val cases = map (S.beta_conv o combize Sinduct_assumf) pats
+ val cases = map (fn pat => betapply (Sinduct_assumf, pat)) pats
val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum)
val proved_cases = map (prove_case f thy) tasks
- val v = S.variant (S.free_varsl (map concl proved_cases))
- (Free("v",domain))
+ val v = Free (variant (foldr add_term_names (map concl proved_cases, []))
+ "v",
+ domain)
val vtyped = tych v
val substs = map (R.SYM o R.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
val proved_cases1 = ListPair.map (fn (th,th') => R.SUBS[th]th')
@@ -759,7 +752,7 @@
val dant = R.GEN vtyped (R.DISJ_CASESL (R.ISPEC vtyped case_thm) abs_cases)
val dc = R.MP Sinduct dant
val Parg_ty = type_of(#Bvar(S.dest_forall(concl dc)))
- val vars = map (gvvariant[P]) (S.strip_prod_type Parg_ty)
+ val vars = map (gvvariant[Pname]) (S.strip_prod_type Parg_ty)
val dc' = U.itlist (R.GEN o tych) vars
(R.SPEC (tych(S.mk_vstruct Parg_ty vars)) dc)
in
@@ -809,7 +802,9 @@
* Attempt to eliminate WF condition. It's the only assumption of rules
*---------------------------------------------------------------------*)
val (rules1,induction1) =
- let val thm = R.prove(tych(hd(#1(R.dest_thm rules))),WFtac)
+ let val thm = R.prove(tych(HOLogic.mk_Trueprop
+ (hd(#1(R.dest_thm rules)))),
+ WFtac)
in (R.PROVE_HYP thm rules, R.PROVE_HYP thm induction)
end handle _ => (rules,induction)
@@ -827,7 +822,8 @@
elim_tc (R.MATCH_MP Thms.eqT tc_eq) (r,ind)
handle _ =>
(elim_tc (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
- (R.prove(tych(S.rhs(concl tc_eq)),terminator)))
+ (R.prove(tych(HOLogic.mk_Trueprop(S.rhs(concl tc_eq))),
+ terminator)))
(r,ind)
handle _ =>
(R.UNDISCH(R.MATCH_MP (R.MATCH_MP Thms.simp_thm r) tc_eq),
@@ -854,7 +850,8 @@
(R.MATCH_MP Thms.eqT tc_eq
handle _
=> (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
- (R.prove(tych(S.rhs(concl tc_eq)),terminator))
+ (R.prove(tych(HOLogic.mk_Trueprop (S.rhs(concl tc_eq))),
+ terminator))
handle _ => tc_eq))
end
--- a/TFL/thry.sig Thu Jun 05 13:26:09 1997 +0200
+++ b/TFL/thry.sig Thu Jun 05 13:27:28 1997 +0200
@@ -6,7 +6,6 @@
signature Thry_sig =
sig
- structure USyntax : USyntax_sig
val match_term : theory -> term -> term
-> (term*term)list * (typ*typ)list
@@ -14,8 +13,6 @@
val typecheck : theory -> term -> cterm
- val make_definition: theory -> string -> term -> thm * theory
-
(* Datatype facts of various flavours *)
val match_info: theory -> string -> {constructors:term list,
case_const:term} option
--- a/TFL/thry.sml Thu Jun 05 13:26:09 1997 +0200
+++ b/TFL/thry.sml Thu Jun 05 13:27:28 1997 +0200
@@ -7,7 +7,6 @@
structure Thry : Thry_sig (* LThry_sig *) =
struct
-structure USyntax = USyntax;
structure S = USyntax;
fun THRY_ERR{func,mesg} = Utils.ERR{module = "Thry",func=func,mesg=mesg};
@@ -37,55 +36,6 @@
fun typecheck thry = cterm_of (sign_of thry);
-
-(*----------------------------------------------------------------------------
- * Making a definition. The argument "tm" looks like "f = WFREC R M". This
- * entrypoint is specialized for interactive use, since it closes the theory
- * after making the definition. This allows later interactive definitions to
- * refer to previous ones. The name for the new theory is automatically
- * generated from the name of the argument theory.
- *---------------------------------------------------------------------------*)
-
-
-(*---------------------------------------------------------------------------
- * TFL attempts to make definitions where the lhs is a variable. Isabelle
- * wants it to be a constant, so here we map it to a constant. Moreover, the
- * theory should already have the constant, so we refrain from adding the
- * constant to the theory. We just add the axiom and return the theory.
- *---------------------------------------------------------------------------*)
-local val (imp $ tprop $ (eeq $ _ $ _ )) = #prop(rep_thm(eq_reflection))
- val Const(eeq_name, ty) = eeq
- val prop = body_type ty
-in
-fun make_definition parent s tm =
- let val {lhs,rhs} = S.dest_eq tm
- val (_,Ty) = dest_Const lhs
- val eeq1 = Const(eeq_name, Ty --> Ty --> prop)
- val dtm = list_comb(eeq1,[lhs,rhs]) (* Rename "=" to "==" *)
- val (_, tm', _) = Sign.infer_types (sign_of parent)
- (K None) (K None) [] true ([dtm],propT)
- val new_thy = add_defs_i [(s,tm')] parent
- in
- (freezeT((get_axiom new_thy s) RS meta_eq_to_obj_eq), new_thy)
- end;
-end;
-
-(*---------------------------------------------------------------------------
- * Utility routine. Insert into list ordered by the key (a string). If two
- * keys are equal, the new element replaces the old. A more efficient option
- * for the future is needed. In fact, having the list of datatype facts be
- * ordered is useless, since the lookup should never fail!
- *---------------------------------------------------------------------------*)
-fun insert (el as (x:string, _)) =
- let fun canfind[] = [el]
- | canfind(alist as ((y as (k,_))::rst)) =
- if (x<k) then el::alist
- else if (x=k) then el::rst
- else y::canfind rst
- in canfind
- end;
-
-
(*---------------------------------------------------------------------------
* A collection of facts about datatypes
*---------------------------------------------------------------------------*)
--- a/TFL/usyntax.sig Thu Jun 05 13:26:09 1997 +0200
+++ b/TFL/usyntax.sig Thu Jun 05 13:27:28 1997 +0200
@@ -25,21 +25,14 @@
val strip_prod_type : typ -> typ list
(* Terms *)
- val free_varsl : term list -> term list
val free_vars_lr : term -> term list
- val all_vars : term -> term list
- val all_varsl : term list -> term list
- val variant : term list -> term -> term
val type_vars_in_term : term -> typ list
val dest_term : term -> lambda
(* Prelogic *)
- val aconv : term -> term -> bool
val inst : (typ*typ) list -> term -> term
- val beta_conv : term -> term
(* Construction routines *)
- val mk_comb :{Rator : term, Rand : term} -> term
val mk_abs :{Bvar : term, Body : term} -> term
val mk_imp :{ant : term, conseq : term} -> term
@@ -66,14 +59,9 @@
val lhs : term -> term
val rhs : term -> term
- val rator : term -> term
val rand : term -> term
- val bvar : term -> term
- val body : term -> term
-
(* Query routines *)
- val is_eq : term -> bool
val is_imp : term -> bool
val is_forall : term -> bool
val is_exists : term -> bool
@@ -87,7 +75,6 @@
val list_mk_abs : (term list * term) -> term
val list_mk_imp : (term list * term) -> term
val list_mk_forall : (term list * term) -> term
- val list_mk_exists : (term list * term) -> term
val list_mk_conj : term list -> term
val list_mk_disj : term list -> term
@@ -102,8 +89,7 @@
(* Miscellaneous *)
val mk_vstruct : typ -> term list -> term
val gen_all : term -> term
- val find_term : (term -> bool) -> term -> term
- val find_terms : (term -> bool) -> term -> term list
+ val find_term : (term -> bool) -> term -> term option
val dest_relation : term -> term * term * term
val is_WFR : term -> bool
val ARB : typ -> term
--- a/TFL/usyntax.sml Thu Jun 05 13:26:09 1997 +0200
+++ b/TFL/usyntax.sml Thu Jun 05 13:27:28 1997 +0200
@@ -49,9 +49,6 @@
* Terms
*
*---------------------------------------------------------------------------*)
-nonfix aconv;
-val aconv = curry (op aconv);
-
(* Free variables, in order of occurrence, from left to right in the
* syntax tree. *)
@@ -67,52 +64,17 @@
-fun free_varsl L = gen_distinct Term.aconv
- (Utils.rev_itlist (curry op @ o term_frees) L []);
-
val type_vars_in_term = map mk_prim_vartype o term_tvars;
-fun all_vars tm =
- let fun memb x = let fun m[] = false | m(y::rst) = (x=y)orelse m rst in m end
- fun add (t, A) = case t of
- Free _ => if (memb t A) then A else t::A
- | Abs (s,ty,body) => add(body, add(Free(s,ty),A))
- | f$t => add(t, add(f, A))
- | _ => A
- in rev(add(tm,[]))
- end;
-fun all_varsl L = gen_distinct Term.aconv
- (Utils.rev_itlist (curry op @ o all_vars) L []);
(* Prelogic *)
fun dest_tybinding (v,ty) = (#1(dest_vtype v),ty)
fun inst theta = subst_vars (map dest_tybinding theta,[])
-fun beta_conv((t1 as Abs _ ) $ t2) = betapply(t1,t2)
- | beta_conv _ = raise USYN_ERR{func = "beta_conv", mesg = "Not a beta-redex"};
-
(* Construction routines *)
-val string_variant = variant;
-
-local fun var_name(Var((Name,_),_)) = Name
- | var_name(Free(s,_)) = s
- | var_name _ = raise USYN_ERR{func = "variant",
- mesg = "list elem. is not a variable"}
-in
-fun variant [] v = v
- | variant vlist (Var((Name,i),ty)) =
- Var((string_variant (map var_name vlist) Name,i),ty)
- | variant vlist (Free(Name,ty)) =
- Free(string_variant (map var_name vlist) Name,ty)
- | variant _ _ = raise USYN_ERR{func = "variant",
- mesg = "2nd arg. should be a variable"}
-end;
-
-fun mk_comb{Rator,Rand} = Rator $ Rand;
-
fun mk_abs{Bvar as Var((s,_),ty),Body} = Abs(s,ty,abstract_over(Bvar,Body))
| mk_abs{Bvar as Free(s,ty),Body} = Abs(s,ty,abstract_over(Bvar,Body))
| mk_abs _ = raise USYN_ERR{func = "mk_abs", mesg = "Bvar is not a variable"};
@@ -166,8 +128,8 @@
if (is_var varstruct)
then mk_abs{Bvar = varstruct, Body = body}
else let val {fst,snd} = dest_pair varstruct
- in mk_comb{Rator= mk_uncurry(type_of fst,type_of snd,type_of body),
- Rand = mpa(fst,mpa(snd,body))}
+ in mk_uncurry(type_of fst,type_of snd,type_of body) $
+ mpa(fst,mpa(snd,body))
end
in mpa(varstruct,body)
end
@@ -255,16 +217,10 @@
(* Garbage - ought to be dropped *)
val lhs = #lhs o dest_eq
val rhs = #rhs o dest_eq
-val rator = #Rator o dest_comb
val rand = #Rand o dest_comb
-val bvar = #Bvar o dest_abs
-val body = #Body o dest_abs
(* Query routines *)
-val is_comb = can dest_comb
-val is_abs = can dest_abs
-val is_eq = can dest_eq
val is_imp = can dest_imp
val is_forall = can dest_forall
val is_exists = can dest_exists
@@ -281,7 +237,6 @@
(* These others are almost never used *)
fun list_mk_imp(A,c) = itlist(fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c;
-fun list_mk_exists(V,t) = itlist(fn v => fn b => mk_exists{Bvar=v, Body=b})V t;
fun list_mk_forall(V,t) = itlist(fn v => fn b => mk_forall{Bvar=v, Body=b})V t;
val list_mk_conj = end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm})
val list_mk_disj = end_itlist(fn d1 => fn tm => mk_disj{disj1=d1, disj2=tm})
@@ -352,35 +307,14 @@
(* Search a term for a sub-term satisfying the predicate p. *)
fun find_term p =
let fun find tm =
- if (p tm)
- then tm
- else if (is_abs tm)
- then find (#Body(dest_abs tm))
- else let val {Rator,Rand} = dest_comb tm
- in find Rator handle _ => find Rand
- end handle _ => raise USYN_ERR{func = "find_term",mesg = ""}
+ if (p tm) then Some tm
+ else case tm of
+ Abs(_,_,body) => find body
+ | (t$u) => (Some (the (find t)) handle _ => find u)
+ | _ => None
in find
end;
-(*******************************************************************
- * find_terms: (term -> HOLogic.boolT) -> term -> term list
- *
- * Find all subterms in a term that satisfy a given predicate p.
- *
- *******************************************************************)
-fun find_terms p =
- let fun accum tl tm =
- let val tl' = if (p tm) then (tm::tl) else tl
- in if (is_abs tm)
- then accum tl' (#Body(dest_abs tm))
- else let val {Rator,Rand} = dest_comb tm
- in accum (accum tl' Rator) Rand
- end handle _ => tl'
- end
- in accum []
- end;
-
-
fun dest_relation tm =
if (type_of tm = HOLogic.boolT)
then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm
@@ -389,7 +323,8 @@
mesg="unexpected term structure"}
else raise USYN_ERR{func="dest_relation",mesg="not a boolean term"};
-fun is_WFR tm = (#Name(dest_const(rator tm)) = "wf") handle _ => false;
+fun is_WFR (Const("wf",_)$_) = true
+ | is_WFR _ = false;
fun ARB ty = mk_select{Bvar=Free("v",ty),
Body=Const("True",HOLogic.boolT)};