--- a/TFL/README Thu May 15 11:35:26 1997 +0200
+++ b/TFL/README Thu May 15 12:29:59 1997 +0200
@@ -2,5 +2,5 @@
1. Invoke the current version of Isabelle-HOL.
2. use "sys.sml";
-3. cd examples/Subst
-4. use "ROOT.ML";
+3. cd "examples/Subst"; or 3. cd "examples";
+4. use "ROOT.ML"; 4. use"test.sml";
--- a/TFL/ROOT.ML Thu May 15 11:35:26 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-(* Title: TFL/ROOT.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-
-Builds and tests Slind's TFL package.
-Should be executed in the subdirectory HOL.
-*)
-
-use"sys.sml";
-cd"examples/Subst";
-use"ROOT.ML";
--- a/TFL/WF1.ML Thu May 15 11:35:26 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,232 +0,0 @@
-(* Title: HOL/WF.ML
- ID: $Id$
- Author: Konrad Slind
- Copyright 1996 TU Munich
-
-For WF1.thy.
-*)
-
-open WF1;
-
-(* TFL variants *)
-goal WF.thy
- "!R. wf R --> (!P. (!x. (!y. (y,x):R --> P y) --> P x) --> (!x. P x))";
-by (strip_tac 1);
-by (res_inst_tac [("r","R"),("P","P"), ("a","x")] wf_induct 1);
-by (assume_tac 1);
-by (fast_tac HOL_cs 1);
-qed"tfl_wf_induct";
-
-goal WF.thy "!f R. (x,a):R --> (cut f R a)(x) = f(x)";
-by (strip_tac 1);
-by (rtac cut_apply 1);
-by (assume_tac 1);
-qed"tfl_cut_apply";
-
-goal WF.thy "!M R f. (f=wfrec R M) --> wf R --> (!x. f x = M (cut f R x) x)";
-by (strip_tac 1);
-by (res_inst_tac [("r","R"), ("H","M"),
- ("a","x"), ("f","f")] (eq_reflection RS def_wfrec) 1);
-by (assume_tac 1);
-by (assume_tac 1);
-qed "tfl_wfrec";
-
-(*----------------------------------------------------------------------------
- * Proof that the inverse image into a wellfounded relation is wellfounded.
- * The proof is relatively sloppy - I map to another version of
- * wellfoundedness (every n.e. set has an R-minimal element) and transport
- * the proof for that formulation over. I also didn't remember the existence
- * of "set_cs" so no doubt the proof can be dramatically shortened!
- *---------------------------------------------------------------------------*)
-goal HOL.thy "(~(!x. P x)) = (? x. ~(P x))";
-by (fast_tac HOL_cs 1);
-val th1 = result();
-
-goal HOL.thy "(~(? x. P x)) = (!x. ~(P x))";
-by (fast_tac HOL_cs 1);
-val th2 = result();
-
-goal HOL.thy "(~(x-->y)) = (x & (~ y))";
-by (fast_tac HOL_cs 1);
-val th3 = result();
-
-goal HOL.thy "((~ x) | y) = (x --> y)";
-by (fast_tac HOL_cs 1);
-val th4 = result();
-
-goal HOL.thy "(~(x & y)) = ((~ x) | (~ y))";
-by (fast_tac HOL_cs 1);
-val th5 = result();
-
-goal HOL.thy "(~(x | y)) = ((~ x) & (~ y))";
-by (fast_tac HOL_cs 1);
-val th6 = result();
-
-goal HOL.thy "(~(~x)) = x";
-by (fast_tac HOL_cs 1);
-val th7 = result();
-
-(* Using [th1,th2,th3,th4,th5,th6,th7] as rewrites drives negation inwards. *)
-val NNF_rews = map (fn th => th RS eq_reflection)[th1,th2,th3,th4,th5,th6,th7];
-
-(* The name "contrapos" is already taken. *)
-goal HOL.thy "(P --> Q) = ((~ Q) --> (~ P))";
-by (fast_tac HOL_cs 1);
-val ol_contrapos = result();
-
-(* Maps to another version of wellfoundedness *)
-val [p1] = goalw WF.thy [wf_def]
-"wf(R) ==> (!Q. (? x. Q x) --> (? min. Q min & (!b. (b,min):R --> (~ Q b))))";
-by (rtac allI 1);
-by (rtac (ol_contrapos RS ssubst) 1);
-by (rewrite_tac NNF_rews);
-by (rtac impI 1);
-by (rtac ((p1 RS spec) RS mp) 1);
-by (fast_tac HOL_cs 1);
-val wf_minimal = result();
-
-goalw WF.thy [wf_def]
-"(!Q. (? x. Q x) --> (? min. Q min & (!b. (b,min):R --> (~ Q b)))) --> wf R";
-by (rtac impI 1);
-by (rtac allI 1);
-by (rtac (ol_contrapos RS ssubst) 1);
-by (rewrite_tac NNF_rews);
-by (rtac impI 1);
-by (etac allE 1);
-by (dtac mp 1);
-by (assume_tac 1);
-by (fast_tac HOL_cs 1);
-val minimal_wf = result();
-
-val wf_eq_minimal =
- standard ((wf_minimal COMP ((minimal_wf RS mp) COMP iffI)) RS sym);
-
-goalw WF1.thy [inv_image_def,wf_eq_minimal RS eq_reflection]
-"wf(R) --> wf(inv_image R (f::'a=>'b))";
-by (strip_tac 1);
-by (etac exE 1);
-by (subgoal_tac "? (w::'b). ? (x::'a). Q x & (f x = w)" 1);
-by (rtac exI 2);
-by (rtac exI 2);
-by (rtac conjI 2);
-by (assume_tac 2);
-by (rtac refl 2);
-
-by (etac allE 1);
-by (dtac mp 1);
-by (assume_tac 1);
-by (eres_inst_tac [("P","? min. (? x. Q x & f x = min) & \
- \ (! b. (b, min) : R --> ~ (? x. Q x & f x = b))")] rev_mp 1);
-by (etac thin_rl 1);
-by (etac thin_rl 1);
-by (rewrite_tac NNF_rews);
-by (rtac impI 1);
-by (etac exE 1);
-by (etac conjE 1);
-by (etac exE 1);
-by (rtac exI 1);
-by (etac conjE 1);
-by (rtac conjI 1);
-by (assume_tac 1);
-by (hyp_subst_tac 1);
-by (rtac allI 1);
-by (rtac impI 1);
-by (etac CollectE 1);
-by (etac allE 1);
-by (dtac mp 1);
-by (rewrite_tac[fst_conv RS eq_reflection,snd_conv RS eq_reflection]);
-by (assume_tac 1);
-by (fast_tac HOL_cs 1);
-val wf_inv_image = result() RS mp;
-
-(* from Nat.ML *)
-goalw WF1.thy [wf_def] "wf(pred_nat)";
-by (strip_tac 1);
-by (nat_ind_tac "x" 1);
-by (fast_tac (HOL_cs addSEs [mp, pred_natE, Pair_inject,
- make_elim Suc_inject]) 2);
-by (fast_tac (HOL_cs addSEs [mp, pred_natE, Pair_inject, Zero_neq_Suc]) 1);
-val wf_pred_nat = result();
-
-goalw WF1.thy [wf_def,pred_list_def] "wf(pred_list)";
-by (strip_tac 1);
-by (List.list.induct_tac "x" 1);
-by (etac allE 1);
-by (etac impE 1);
-by (assume_tac 2);
-by (strip_tac 1);
-by (etac CollectE 1);
-by (asm_full_simp_tac (!simpset) 1);
-
-by (etac allE 1);
-by (etac impE 1);
-by (assume_tac 2);
-by (strip_tac 1);
-by (etac CollectE 1);
-by (etac exE 1);
-by (asm_full_simp_tac (!simpset) 1);
-by (etac conjE 1);
-by (hyp_subst_tac 1);
-by (assume_tac 1);
-qed "wf_pred_list";
-
-(*----------------------------------------------------------------------------
- * All measures are wellfounded.
- *---------------------------------------------------------------------------*)
-
-goalw WF1.thy [measure_def] "wf (measure f)";
-by (rtac wf_inv_image 1);
-by (rtac wf_trancl 1);
-by (rtac wf_pred_nat 1);
-qed "wf_measure";
-
-(*----------------------------------------------------------------------------
- * Wellfoundedness of lexicographic combinations
- *---------------------------------------------------------------------------*)
-
-val prems = goal Prod.thy "!a b. P((a,b)) ==> !p. P(p)";
-by (cut_facts_tac prems 1);
-by (rtac allI 1);
-by (rtac (surjective_pairing RS ssubst) 1);
-by (fast_tac HOL_cs 1);
-qed "split_all_pair";
-
-val [wfa,wfb] = goalw WF1.thy [wf_def,lex_prod_def]
- "[| wf(ra); wf(rb) |] ==> wf(ra**rb)";
-by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]);
-by (rtac (wfa RS spec RS mp) 1);
-by (EVERY1 [rtac allI,rtac impI]);
-by (rtac (wfb RS spec RS mp) 1);
-by (fast_tac (set_cs addSEs [Pair_inject]) 1);
-qed "wf_lex_prod";
-
-(*----------------------------------------------------------------------------
- * Wellfoundedness of relational product
- *---------------------------------------------------------------------------*)
-val [wfa,wfb] = goalw WF1.thy [wf_def,rprod_def]
- "[| wf(ra); wf(rb) |] ==> wf(rprod ra rb)";
-by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]);
-by (rtac (wfa RS spec RS mp) 1);
-by (EVERY1 [rtac allI,rtac impI]);
-by (rtac (wfb RS spec RS mp) 1);
-by (fast_tac (set_cs addSEs [Pair_inject]) 1);
-qed "wf_rel_prod";
-
-
-(*---------------------------------------------------------------------------
- * Wellfoundedness of subsets
- *---------------------------------------------------------------------------*)
-
-goalw WF1.thy [wf_eq_minimal RS eq_reflection]
- "wf(r) --> (!x y. (x,y):p --> (x,y):r) --> wf(p)";
-by (fast_tac set_cs 1);
-qed "wf_subset";
-
-(*---------------------------------------------------------------------------
- * Wellfoundedness of the empty relation.
- *---------------------------------------------------------------------------*)
-
-goalw WF1.thy [wf_eq_minimal RS eq_reflection,emptyr_def]
- "wf(emptyr)";
-by (fast_tac set_cs 1);
-qed "wf_emptyr";
--- a/TFL/WF1.thy Thu May 15 11:35:26 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-(* Derived wellfounded relations, plus customized-for-TFL theorems from WF *)
-
-WF1 = List +
-consts
- inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"
- measure :: "('a => nat) => ('a * 'a)set"
- "**" :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70)
- rprod :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
- emptyr :: "('a * 'b) set"
- pred_list :: "('a list * 'a list) set"
-
-defs
- inv_image_def "inv_image R f == {p. (f(fst p), f(snd p)) : R}"
-
- measure_def "measure == inv_image (trancl pred_nat)"
-
- lex_prod_def "ra**rb == {p. ? a a' b b'.
- p = ((a,b),(a',b')) &
- ((a,a') : ra | a=a' & (b,b') : rb)}"
-
- rprod_def "rprod ra rb == {p. ? a a' b b'.
- p = ((a,b),(a',b')) &
- ((a,a') : ra & (b,b') : rb)}"
-
- emptyr_def "emptyr == {}"
- pred_list_def "pred_list == {p. ? h. snd p = h#(fst p)}"
-end
--- a/TFL/post.sml Thu May 15 11:35:26 1997 +0200
+++ b/TFL/post.sml Thu May 15 12:29:59 1997 +0200
@@ -1,9 +1,9 @@
-structure Tfl
- :sig
+signature TFL =
+ sig
structure Prim : TFL_sig
- val tgoalw : theory -> thm list -> thm -> thm list
- val tgoal: theory -> thm -> thm list
+ val tgoalw : theory -> thm list -> thm list -> thm list
+ val tgoal: theory -> thm list -> thm list
val WF_TAC : thm list -> tactic
@@ -12,27 +12,41 @@
-> {induction:thm, rules:thm, TCs:term list list}
-> {induction:thm, rules:thm, nested_tcs:thm list}
- val rfunction : theory
- -> (thm list -> thm -> thm)
- -> term -> term
- -> {induction:thm, rules:thm,
- tcs:term list, theory:theory}
+ val define_i : theory -> term -> term -> theory * (thm * Prim.pattern list)
+ val define : theory -> string -> string list -> theory * Prim.pattern list
- val Rfunction : theory -> term -> term
- -> {induction:thm, rules:thm,
- theory:theory, tcs:term list}
+ val simplify_defn : theory * (string * Prim.pattern list)
+ -> {rules:thm list, induct:thm, tcs:term list}
- val function : theory -> term -> {theory:theory, eq_ind : thm}
- val lazyR_def : theory -> term -> {theory:theory, eqns : thm}
+ (*-------------------------------------------------------------------------
+ val function : theory -> term -> {theory:theory, eq_ind : thm}
+ val lazyR_def: theory -> term -> {theory:theory, eqns : thm}
+ *-------------------------------------------------------------------------*)
val tflcongs : theory -> thm list
- end =
+ end;
+
+
+structure Tfl: TFL =
struct
structure Prim = Prim
+ structure S = Prim.USyntax
- fun tgoalw thy defs thm =
- let val L = Prim.termination_goals thm
+(*---------------------------------------------------------------------------
+ * Extract termination goals so that they can be put it into a goalstack, or
+ * have a tactic directly applied to them.
+ *--------------------------------------------------------------------------*)
+fun termination_goals rules =
+ map (Logic.freeze_vars o S.drop_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) (mk_prop(list_mk_conj L))
in goalw_cterm defs g
@@ -40,6 +54,9 @@
val tgoal = Utils.C tgoalw [];
+ (*---------------------------------------------------------------------------
+ * 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_pred_nat, wf_pred_list, wf_trancl];
@@ -49,38 +66,62 @@
mem_Collect_eq,lessI]) 1
THEN TRY(fast_tac set_cs 1);
+val length_Cons = prove_goal List.thy "length(h#t) = Suc(length t)"
+ (fn _ => [Simp_tac 1]);
+
val simpls = [less_eq RS eq_reflection,
lex_prod_def, measure_def, inv_image_def,
fst_conv RS eq_reflection, snd_conv RS eq_reflection,
- mem_Collect_eq RS eq_reflection(*, length_Cons RS eq_reflection*)];
+ mem_Collect_eq RS eq_reflection, length_Cons RS eq_reflection];
+ (*---------------------------------------------------------------------------
+ * 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 = Prim.Rules.simpl_conv simpls};
val simplifier = rewrite_rule (simpls @ #simps(rep_ss HOL_ss) @
[pred_nat_def,pred_list_def]);
+
fun tflcongs thy = Prim.Context.read() @ (#case_congs(Thry.extract_info thy));
-local structure S = Prim.USyntax
-in
-fun func_of_cond_eqn tm =
- #1(S.strip_comb(#lhs(S.dest_eq(#2(S.strip_forall(#2(S.strip_imp tm)))))))
-end;
-
-
val concl = #2 o Prim.Rules.dest_thm;
(*---------------------------------------------------------------------------
- * Defining a function with an associated termination relation. Lots of
- * postprocessing takes place.
+ * Defining a function with an associated termination relation.
+ *---------------------------------------------------------------------------*)
+fun define_i thy 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 R functional
+ in (thry,(thm,pats))
+ end;
+
+(*lcp's version: takes strings; doesn't return "thm"
+ (whose signature is a draft and therefore useless) *)
+fun define thy R eqs =
+ let fun read thy = readtm (sign_of thy) (TVar(("DUMMY",0),[]))
+ val (thy',(_,pats)) =
+ define_i thy (read thy R)
+ (fold_bal (app Ind_Syntax.conj) (map (read thy) eqs))
+ in (thy',pats) end
+ handle Utils.ERR {mesg,...} => error mesg;
+
+(*---------------------------------------------------------------------------
+ * Postprocess a definition made by "define". This is a separate stage of
+ * processing from the definition stage.
*---------------------------------------------------------------------------*)
local
-structure S = Prim.USyntax
structure R = Prim.Rules
structure U = Utils
+(* The rest of these local definitions are for the tricky nested case *)
val solved = not o U.can S.dest_eq o #2 o S.strip_forall o concl
fun id_thm th =
@@ -96,6 +137,7 @@
| _$(Const("op =",_)$_$_) => r RS eq_reflection
| _ => r RS P_imp_P_eq_True
fun rewrite L = rewrite_rule (map mk_meta_eq (Utils.filter(not o id_thm) L))
+fun reducer thl = rewrite (map standard thl @ #simps(rep_ss HOL_ss))
fun join_assums th =
let val {sign,...} = rep_thm th
@@ -105,30 +147,28 @@
val cntxtr = (#1 o S.strip_imp) rhs (* but union is solider *)
val cntxt = U.union S.aconv cntxtl cntxtr
in
- R.GEN_ALL
- (R.DISCH_ALL
- (rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th)))
+ R.GEN_ALL
+ (R.DISCH_ALL
+ (rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th)))
end
val gen_all = S.gen_all
in
-fun rfunction theory reducer R eqs =
- let val _ = prs "Making definition.. "
- val {rules,theory, full_pats_TCs,
- TCs,...} = Prim.gen_wfrec_definition theory {R=R,eqs=eqs}
- val f = func_of_cond_eqn(concl(R.CONJUNCT1 rules handle _ => rules))
- val _ = prs "Definition made.\n"
- val _ = prs "Proving induction theorem.. "
- val ind = Prim.mk_induction theory f R full_pats_TCs
- val _ = prs "Proved induction theorem.\n"
- val pp = std_postprocessor theory
- val _ = prs "Postprocessing.. "
- val {rules,induction,nested_tcs} = pp{rules=rules,induction=ind,TCs=TCs}
- val normal_tcs = Prim.termination_goals rules
- in
- case nested_tcs
- of [] => (prs "Postprocessing done.\n";
- {theory=theory, induction=induction, rules=rules,tcs=normal_tcs})
- | L => let val _ = prs "Simplifying nested TCs.. "
+(*---------------------------------------------------------------------------
+ * The "reducer" argument is
+ * (fn thl => rewrite (map standard thl @ #simps(rep_ss HOL_ss)));
+ *---------------------------------------------------------------------------*)
+fun proof_stage theory reducer {f, R, rules, full_pats_TCs, TCs} =
+ let val dummy = output(std_out, "Proving induction theorem.. ")
+ val ind = Prim.mk_induction theory f R full_pats_TCs
+ val dummy = output(std_out, "Proved induction theorem.\n")
+ val pp = std_postprocessor theory
+ val dummy = output(std_out, "Postprocessing.. ")
+ val {rules,induction,nested_tcs} = pp{rules=rules,induction=ind,TCs=TCs}
+ in
+ case nested_tcs
+ of [] => (output(std_out, "Postprocessing done.\n");
+ {induction=induction, rules=rules,tcs=[]})
+ | L => let val dummy = output(std_out, "Simplifying nested TCs.. ")
val (solved,simplified,stubborn) =
U.itlist (fn th => fn (So,Si,St) =>
if (id_thm th) then (So, Si, th::St) else
@@ -137,38 +177,65 @@
val simplified' = map join_assums simplified
val induction' = reducer (solved@simplified') induction
val rules' = reducer (solved@simplified') rules
- val _ = prs "Postprocessing done.\n"
+ val dummy = output(std_out, "Postprocessing done.\n")
in
{induction = induction',
rules = rules',
- tcs = normal_tcs @
- map (gen_all o S.rhs o #2 o S.strip_forall o concl)
- (simplified@stubborn),
- theory = theory}
+ tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl)
+ (simplified@stubborn)}
end
- end
- handle (e as Utils.ERR _) => Utils.Raise e
- | e => print_exn e
+ end handle (e as Utils.ERR _) => Utils.Raise e
+ | e => print_exn e;
+
+
+(*lcp: put a theorem into Isabelle form, using meta-level connectives*)
+val meta_outer =
+ standard o rule_by_tactic (REPEAT_FIRST (resolve_tac [allI, impI, conjI]));
+
+
+(*Strip off the outer !P*)
+val spec'= read_instantiate [("x","P::?'b=>bool")] spec;
-fun Rfunction thry =
- rfunction thry
- (fn thl => rewrite (map standard thl @ #simps(rep_ss HOL_ss)));
-
-
+fun simplify_defn (thy,(id,pats)) =
+ let val def = freezeT(get_def thy id RS meta_eq_to_obj_eq)
+ val {theory,rules,TCs,full_pats_TCs,patterns} =
+ Prim.post_definition (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
+ {f = f, R = R, rules = rules,
+ full_pats_TCs = full_pats_TCs,
+ TCs = TCs}
+ val rules' = map (standard o normalize_thm [RSmp]) (R.CONJUNCTS rules)
+ in {induct = meta_outer
+ (normalize_thm [RSspec,RSmp] (induction RS spec')),
+ rules = rules',
+ tcs = (termination_goals rules') @ tcs}
+ end
+ handle Utils.ERR {mesg,...} => error mesg
end;
+(*---------------------------------------------------------------------------
+ *
+ * Definitions with synthesized termination relation temporarily
+ * deleted -- it's not clear how to integrate this facility with
+ * the Isabelle theory file scheme, which restricts
+ * inference at theory-construction time.
+ *
-local structure R = Prim.Rules
+local fun floutput s = (output(std_out,s); flush_out std_out)
+ structure R = Prim.Rules
in
fun function theory eqs =
- let val _ = prs "Making definition.. "
+ let val dummy = floutput "Making definition.. "
val {rules,R,theory,full_pats_TCs,...} = Prim.lazyR_def theory eqs
val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules))
- val _ = prs "Definition made.\n"
- val _ = prs "Proving induction theorem.. "
+ val dummy = floutput "Definition made.\n"
+ val dummy = floutput "Proving induction theorem.. "
val induction = Prim.mk_induction theory f R full_pats_TCs
- val _ = prs "Induction theorem proved.\n"
+ val dummy = floutput "Induction theorem proved.\n"
in {theory = theory,
eq_ind = standard (induction RS (rules RS conjI))}
end
@@ -183,8 +250,17 @@
end
handle (e as Utils.ERR _) => Utils.Raise e
| e => print_exn e;
+ *
+ *
+ *---------------------------------------------------------------------------*)
+
+
- val () = Prim.Context.write[Thms.LET_CONG, Thms.COND_CONG];
+(*---------------------------------------------------------------------------
+ * Install the basic context notions. Others (for nat and list and prod)
+ * have already been added in thry.sml
+ *---------------------------------------------------------------------------*)
+val () = Prim.Context.write[Thms.LET_CONG, Thms.COND_CONG];
end;
--- a/TFL/rules.new.sml Thu May 15 11:35:26 1997 +0200
+++ b/TFL/rules.new.sml Thu May 15 12:29:59 1997 +0200
@@ -542,7 +542,7 @@
val thm_ref = ref [] : thm list ref;
val tracing = ref false;
-fun say s = if !tracing then prs s else ();
+fun say s = if !tracing then (output(std_out,s); flush_out std_out) else ();
fun print_thms s L =
(say s;
--- a/TFL/sys.sml Thu May 15 11:35:26 1997 +0200
+++ b/TFL/sys.sml Thu May 15 12:29:59 1997 +0200
@@ -29,8 +29,7 @@
* Supply implementations
*---------------------------------------------------------------------------*)
-val _ = use_thy"WF1"; (* Wellfoundedness theory *)
-
+(* Ignore "Time" exception raised at end of building theory. *)
use "usyntax.sml";
use "thms.sml";
use"dcterm.sml"; use"rules.new.sml";
@@ -45,4 +44,3 @@
structure Thry = Thry);
use"post.sml";
-
--- a/TFL/test.sml Thu May 15 11:35:26 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,301 +0,0 @@
-fun cread thy s = read_cterm (sign_of thy) (s, (TVar(("DUMMY",0),[])));
-fun read thy = term_of o cread thy;
-fun Term s = read WF1.thy s;
-
-fun Rfunc thy R eqs =
- let val {induction,rules,theory,tcs} =
- timeit(fn () => Tfl.Rfunction thy (read thy R) (read thy eqs))
- in {induction=induction, rules=rules, theory=theory,
- tcs = map (cterm_of (sign_of theory)) tcs}
- end;
-
-val Rfunction = Rfunc WF1.thy;
-
-fun function tm = timeit (fn () => Tfl.function WF1.thy (Term tm));
-
-
-(*---------------------------------------------------------------------------
- * Factorial. Notice how functions without pattern matching are often harder
- * to deal with than those with! Unfortunately, not all functions can be
- * described purely by pattern matching, e.g., "variant" as below.
- *---------------------------------------------------------------------------*)
-function "fact x = (if (x = 0) then Suc 0 else x * fact (x - Suc 0))";
-
-Rfunction"pred_nat"
- "fact x = (if (x = 0) then Suc 0 else x * fact (x - Suc 0))";
-
-function "(Fact 0 = (Suc 0)) & \
- \ (Fact (Suc x) = (Fact x * Suc x))";
-
-Rfunction "pred_nat"
- "(Fact 0 = (Suc 0)) & \
- \ (Fact (Suc x) = (Fact x * Suc x))";
-
-(*---------------------------------------------------------------------------
- * Fibonacci.
- *---------------------------------------------------------------------------*)
-function "(Fib 0 = (Suc 0)) & \
- \ (Fib (Suc 0) = (Suc 0)) & \
- \ (Fib (Suc(Suc x)) = (Fib x + Fib (Suc x)))";
-
-(* "<" doesn't currently work smoothly *)
-Rfunction"{p::(nat*nat). fst p < snd p}"
- "(Fib 0 = (Suc 0)) & \
- \ (Fib (Suc 0) = (Suc 0)) & \
- \ (Fib (Suc(Suc x)) = (Fib x + Fib (Suc x)))";
-
-
-(* "trancl pred" means "<" and works better *)
-Rfunction"trancl pred_nat"
- "(Fib 0 = (Suc 0)) & \
- \ (Fib (Suc 0) = (Suc 0)) & \
- \ (Fib (Suc(Suc x)) = (Fib x + Fib (Suc x)))";
-
-(*---------------------------------------------------------------------------
- * Ackermann.
- *---------------------------------------------------------------------------*)
-Rfunction"pred_nat ** pred_nat"
- "(Ack (0,n) = (n + Suc 0)) & \
- \ (Ack (Suc m,0) = (Ack (m, Suc 0))) & \
- \ (Ack (Suc m, Suc n) = Ack (m, Ack (Suc m, n)))";
-
-(*---------------------------------------------------------------------------
- * Almost primitive recursion.
- *---------------------------------------------------------------------------*)
-function"(map2(f, [], L) = []) & \
- \ (map2(f, h#t, []) = []) & \
- \ (map2(f, h1#t1, h2#t2) = f h1 h2 # map2 (f, t1, t2))";
-
-(* Swap arguments *)
-function"(map2(([],L), f) = []) & \
- \ (map2((h#t, []), f) = []) & \
- \ (map2((h1#t1, h2#t2), f) = f h1 h2 # map2((t1,t2),f))";
-
-Rfunction
- "measure((length o fst o snd)::('a=>'b=>'c)*'a list*'b list => nat)"
- "(map2((f::'a=>'b=>'c), ([]::'a list), (L::'b list)) = []) & \
-\ (map2(f, h#t, []) = []) & \
-\ (map2(f, h1#t1, h2#t2) = f h1 h2 # map2 (f, t1, t2))";
-
-(*---------------------------------------------------------------------------
- * Relation "R" holds stepwise in a list
- *---------------------------------------------------------------------------*)
-function"(finiteRchain ((R::'a=>'a=>bool), ([]::'a list)) = True) & \
- \ (finiteRchain (R, [x]) = True) & \
- \ (finiteRchain (R, x#y#rst) = (R x y & finiteRchain(R, y#rst)))";
-
-
-Rfunction"measure ((length o snd)::('a=>'a=>bool) * 'a list => nat)"
- "(finiteRchain((R::'a=>'a=>bool), ([]::'a list)) = True) & \
- \ (finiteRchain(R, [x]) = True) & \
- \ (finiteRchain(R, x#y#rst) = (R x y & finiteRchain(R, y#rst)))";
-
-(*---------------------------------------------------------------------------
- * Quicksort.
- *---------------------------------------------------------------------------*)
-function"(qsort(ord, []) = []) & \
- \ (qsort(ord, x#rst) = \
- \ qsort(ord,filter(not o ord x) rst) \
- \ @[x]@ \
- \ qsort(ord,filter(ord x) rst))";
-
-Rfunction"measure ((length o snd)::('a=>'a=>bool) * 'a list => nat)"
- "(qsort((ord::'a=>'a=>bool), ([]::'a list)) = []) & \
- \ (qsort(ord, x#rst) = \
- \ qsort(ord,filter(not o ord x) rst) \
- \ @[x]@ \
- \ qsort(ord,filter(ord x) rst))";
-
-(*---------------------------------------------------------------------------
- * Variant.
- *---------------------------------------------------------------------------*)
-function"variant(x, L) = (if (x mem L) then variant(Suc x, L) else x)";
-
-Rfunction
- "measure(%(p::nat*nat list). length(filter(%y. fst(p) <= y) (snd p)))"
- "variant(x, L) = (if (x mem L) then variant(Suc x, L) else x)";
-
-(*---------------------------------------------------------------------------
- * Euclid's algorithm
- *---------------------------------------------------------------------------*)
-function"(gcd ((0::nat),(y::nat)) = y) & \
- \ (gcd (Suc x, 0) = Suc x) & \
- \ (gcd (Suc x, Suc y) = \
- \ (if (y <= x) then gcd(x - y, Suc y) \
- \ else gcd(Suc x, y - x)))";
-
-
-(*---------------------------------------------------------------------------
- * Wrong answer because Isabelle rewriter (going bottom-up) attempts to
- * apply congruence rule for split to "split" but can't because split is only
- * partly applied. It then fails, instead of just not doing the rewrite.
- * Tobias has said he'll fix it.
- *
- * ... July 96 ... seems to have been fixed.
- *---------------------------------------------------------------------------*)
-
-Rfunction"measure (split (op+) ::nat*nat=>nat)"
- "(gcd ((0::nat),(y::nat)) = y) & \
- \ (gcd (Suc x, 0) = Suc x) & \
- \ (gcd (Suc x, Suc y) = \
- \ (if (y <= x) then gcd(x - y, Suc y) \
- \ else gcd(Suc x, y - x)))";
-
-(*---------------------------------------------------------------------------
- * A simple nested function.
- *---------------------------------------------------------------------------*)
-Rfunction"trancl pred_nat"
- "(g 0 = 0) & \
- \ (g(Suc x) = g(g x))";
-
-(*---------------------------------------------------------------------------
- * A clever division algorithm. Primitive recursive.
- *---------------------------------------------------------------------------*)
-function"(Div(0,x) = (0,0)) & \
- \ (Div(Suc x, y) = \
- \ (let (q,r) = Div(x,y) \
- \ in if (y <= Suc r) then (Suc q,0) else (q, Suc r)))";
-
-Rfunction"inv_image pred_nat (fst::nat*nat=>nat)"
- "(Div(0,x) = (0,0)) & \
- \ (Div(Suc x, y) = \
- \ (let q = fst(Div(x,y)); \
- \ r = snd(Div(x,y)) \
- \ in \
- \ if (y <= Suc r) then (Suc q,0) else (q, Suc r)))";
-
-(*---------------------------------------------------------------------------
- * Testing nested contexts.
- *---------------------------------------------------------------------------*)
-function"(f(0,x) = (0,0)) & \
- \ (f(Suc x, y) = \
- \ (let z = x \
- \ in \
- \ if (0<y) then (0,0) else f(z,y)))";
-
-
-function"(f(0,x) = (0,0)) & \
- \ (f(Suc x, y) = \
- \ (if y = x \
- \ then (if (0<y) then (0,0) else f(x,y)) \
- \ else (x,y)))";
-
-
-(*---------------------------------------------------------------------------
- * Naming trickery in lets.
- *---------------------------------------------------------------------------*)
-
-(* No trick *)
-function "(test(x, []) = x) & \
- \ (test(x,h#t) = (let y = Suc x in test(y,t)))";
-
-(* Trick *)
-function"(test(x, []) = x) & \
- \ (test(x,h#t) = \
- \ (let x = Suc x \
- \ in \
- \ test(x,t)))";
-
-(* Tricky naming, plus nested contexts *)
-function "vary(x, L) = \
- \ (if (x mem L) \
- \ then (let x = Suc x \
- \ in vary(x,L)) \
- \ else x)";
-
-
-(*---------------------------------------------------------------------------
- * Handling paired lets of various kinds
- *---------------------------------------------------------------------------*)
-function
- "(Fib(0) = Suc 0) & \
- \ (Fib (Suc 0) = Suc 0) & \
- \ (Fib (Suc (Suc n)) = \
- \ (let (x,y) = (Fib (Suc n), Fib n) in x+y))";
-
-
-function
- "(qsort((ord::'a=>'a=>bool), ([]::'a list)) = []) & \
- \ (qsort(ord, x#rst) = \
- \ (let (L1,L2) = (filter(not o ord x) rst, \
- \ filter (ord x) rst) \
- \ in \
- \ qsort(ord,L1)@[x]@qsort(ord,L2)))";
-
-function"(qsort((ord::'a=>'a=>bool), ([]::'a list)) = []) & \
- \ (qsort(ord, x#rst) = \
- \ (let (L1,L2,P) = (filter(not o ord x) rst, \
- \ filter (ord x) rst, x) \
- \ in \
- \ qsort(ord,L1)@[x]@qsort(ord,L2)))";
-
-function"(qsort((ord::'a=>'a=>bool), ([]::'a list)) = []) & \
- \ (qsort(ord, x#rst) = \
- \ (let (L1,L2) = (filter(not o ord x) rst, \
- \ filter (ord x) rst); \
- \ (p,q) = (x,rst) \
- \ in \
- \ qsort(ord,L1)@[x]@qsort(ord,L2)))";
-
-
-(*---------------------------------------------------------------------------
- * A biggish function
- *---------------------------------------------------------------------------*)
-
-function"(acc1(A,[],s,xss,zs,xs) = \
-\ (if xs=[] then (xss, zs) \
-\ else acc1(A, zs,s,(xss @ [xs]),[],[]))) & \
-\ (acc1(A,(y#ys), s, xss, zs, xs) = \
-\ (let s' = s; \
-\ zs' = (if fst A s' then [] else zs@[y]); \
-\ xs' = (if fst A s' then xs@zs@[y] else xs) \
-\ in \
-\ acc1(A, ys, s', xss, zs', xs')))";
-
-
-(*---------------------------------------------------------------------------
- * Nested, with context.
- *---------------------------------------------------------------------------*)
-Rfunction"pred_nat"
- "(k 0 = 0) & \
-\ (k (Suc n) = (let x = k (Suc 0) \
-\ in if (0=Suc 0) then k (Suc(Suc 0)) else n))";
-
-
-(*---------------------------------------------------------------------------
- * A function that partitions a list into two around a predicate "P".
- *---------------------------------------------------------------------------*)
-val {theory,induction,rules,tcs} =
- Rfunction
- "inv_image pred_list \
- \ ((fst o snd)::('a=>bool)*'a list*'a list*'a list => 'a list)"
-
- "(part(P::'a=>bool, [], l1,l2) = (l1,l2)) & \
-\ (part(P, h#rst, l1,l2) = \
-\ (if P h then part(P,rst, h#l1, l2) \
-\ else part(P,rst, l1, h#l2)))";
-
-
-(*---------------------------------------------------------------------------
- * Another quicksort.
- *---------------------------------------------------------------------------*)
-Rfunc theory "measure ((length o snd)::('a=>'a=>bool) * 'a list => nat)"
- "(fqsort(ord,[]) = []) & \
-\ (fqsort(ord, x#rst) = \
- \ (let less = fst(part((%y. ord y x), rst,([],[]))); \
- \ more = snd(part((%y. ord y x), rst,([],[]))) \
- \ in \
- \ fqsort(ord,less)@[x]@fqsort(ord,more)))";
-
-Rfunc theory "measure ((length o snd)::('a=>'a=>bool) * 'a list => nat)"
- "(fqsort(ord,[]) = []) & \
-\ (fqsort(ord, x#rst) = \
- \ (let (less,more) = part((%y. ord y x), rst,([],[])) \
- \ in \
- \ fqsort(ord,less)@[x]@fqsort(ord,more)))";
-
-
-(* Should fail on repeated variables. *)
-function"(And(x,[]) = x) & \
- \ (And(y, y#t) = And(y, t))";
-
--- a/TFL/test1.sml Thu May 15 11:35:26 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,83 +0,0 @@
-(*---------------------------------------------------------------------------
- * Pattern matching extensions.
- *---------------------------------------------------------------------------*)
-
-fun cread thy s = read_cterm (sign_of thy) (s, (TVar(("DUMMY",0),[])));
-fun read thy = term_of o cread thy;
-fun Term s = read WF1.thy s;
-
-fun Rfunc thy R eqs =
- let val {induction,rules,theory,tcs} =
- timeit(fn () => Tfl.Rfunction thy (read thy R) (read thy eqs))
- in {induction=induction, rules=rules, theory=theory,
- tcs = map (cterm_of (sign_of theory)) tcs}
- end;
-
-fun def tm = timeit (fn () => Tfl.function WF1.thy (Term tm));
-
-
-
-
-(*---------------------------------------------------------------------------
- * Normal patterns
- *---------------------------------------------------------------------------*)
-def "(f(x,y) = x+y)";
-
-def "(f1 0 = 1) & (f1 (Suc n) = 2)";
-
-(*---------------------------------------------------------------------------
- * Omitted patterns
- *---------------------------------------------------------------------------*)
-def "(f2 0 = 1)";
-
-def "(f3 (h#t) = h)";
-
-def "(f4 [a,b] = a) & (f4 [b] = b)";
-
-def "(f5 (0,0) = 0)";
-
-def "(f6 (0,0) = 0) & (f6 (0,Suc x) = x) & (f6 (Suc x, y) = y+x)";
-
-def "(f7 (Suc 0, h#t) = 1) & (f7 (Suc(Suc n),h1#h2#t) = h1)";
-
-def "(f8 (Suc(Suc n),h1#h2#t) = h1)";
-
-
-(*---------------------------------------------------------------------------
- * Overlapping patterns
- *---------------------------------------------------------------------------*)
-def "(f9 (h1#h2#t) = t) & (f9 x = x)";
-
-def "(g (x,0) = 1) & (g (0,x) = 2)";
-
-def "(g1 (0,x) = x) & (g1 (x,0) = x)";
-
-def "(g2 ([], a#b#x) = 1) & (g2 (a#b#x, y) = 2) & (g2 (z, a#y) = a)";
-
-def "(g3 (x,y,0) = 1) & (g3 (x,0,y) = 2) & (g3 (0,x,y) = x)";
-
-def "(g4 (0,y,z) = 1) & (g4 (x,0,z) = 2) & (g4 (x,y,0) = x)";
-
-def "(g5(0,x,y,z) = 1) & (g5(w,0,y,z) = 2) & (g5(w,x,0,z) = z) & \
- \ (g5(w,x,y,0) = y)";
-
-def "(g6 (0,w,x,y,z) = 1) & (g6 (v,0,x,y,z) = 2) & (g6 (v,w,0,y,z) = z) & \
- \ (g6 (v,w,x,0,z) = z) & (g6 (v,w,x,y,0) = 0)";
-
-def "(g7 [x, 0] = x) & (g7 [Suc v] = 1) & (g7 z = 2)";
-
-def "(g8 (h1#h2#h3#h4#h5#h6) = [h1,h2,h3,h4,h5]# g8 h6) & (g8 x = [x])";
-
-(* Normal *)
-def "(g9 (Suc(Suc x)) = 1) & (g9 (Suc x) = 2) & (g9 0 = 0)";
-
-(*---------------------------------------------------------------------------
- * Inaccessible patterns
- *---------------------------------------------------------------------------*)
-def "(h x = 1) & (h x = 2)";
-
-def "(h1 (x,0) = 1) & (h1 (x,Suc y) = 2) & \
- \ (h1 (x,y) = x) & (h1 (x,y) = y)";
-
-def "(h2 (x,0) = 1) & (h2 (0,x) = 2) & \
- \ (h2 (0,0) = 0) & (h2 (x,y) = x)";
--- a/TFL/tfl.sig Thu May 15 11:35:26 1997 +0200
+++ b/TFL/tfl.sig Thu May 15 12:29:59 1997 +0200
@@ -18,9 +18,15 @@
-> {functional:Preterm,
pats: pattern list}
- val prim_wfrec_definition : Thry
- -> {R:Preterm, functional:Preterm}
- -> {def:Thm, corollary:Thm, theory:Thry}
+ val wfrec_definition0 : Thry -> Preterm -> Preterm -> Thm * Thry
+
+ val post_definition : Thry * (Thm * pattern list)
+ -> {theory : Thry,
+ rules : Thm,
+ TCs : Preterm list list,
+ full_pats_TCs : (Preterm * Preterm list) list,
+ patterns : pattern list}
+
val wfrec_eqns : Thry -> Preterm
-> {WFR : Preterm,
@@ -29,14 +35,6 @@
pats : pattern list}
- val gen_wfrec_definition : Thry
- -> {R:Preterm, eqs:Preterm}
- -> {theory:Thry,
- rules :Thm,
- TCs : Preterm list list,
- full_pats_TCs :(Preterm * Preterm list) list,
- patterns : pattern list}
-
val lazyR_def : Thry
-> Preterm
-> {theory:Thry,
@@ -55,8 +53,6 @@
-> {rules:Thm, induction:Thm, TCs:Preterm list list}
-> {rules:Thm, induction:Thm, nested_tcs:Thm list}
- val termination_goals : Thm -> Preterm list
-
structure Context
: sig
val read : unit -> Thm list
--- a/TFL/tfl.sml Thu May 15 11:35:26 1997 +0200
+++ b/TFL/tfl.sml Thu May 15 12:29:59 1997 +0200
@@ -306,14 +306,17 @@
local fun paired1{lhs,rhs} = (lhs,rhs)
and paired2{Rator,Rand} = (Rator,Rand)
fun mk_functional_err s = raise TFL_ERR{func = "mk_functional", mesg=s}
+ fun single [f] = f
+ | single fs = mk_functional_err (Int.toString (length fs) ^
+ " distinct function names!")
in
fun mk_functional thy eqs =
let val clauses = S.strip_conj eqs
val (L,R) = U.unzip (map (paired1 o S.dest_eq o U.snd o S.strip_forall)
clauses)
val (funcs,pats) = U.unzip(map (paired2 o S.dest_comb) L)
- val [f] = U.mk_set (S.aconv) funcs
- handle _ => mk_functional_err "function name not unique"
+ val f = single (U.mk_set (S.aconv) funcs)
+ val fvar = if (S.is_var f) then f else S.mk_var(S.dest_const f)
val _ = map (no_repeat_vars thy) pats
val rows = U.zip (map (fn x => ([],[x])) pats) (map GIVEN (enumerate R))
val fvs = S.free_varsl R
@@ -334,7 +337,8 @@
of [] => ()
| L => mk_functional_err("The following rows (counting from zero)\
\ are inaccessible: "^stringize L)
- in {functional = S.list_mk_abs ([f,a], case_tm),
+ val case_tm' = S.subst [f |-> fvar] case_tm
+ in {functional = S.list_mk_abs ([fvar,a], case_tm'),
pats = patts2}
end end;
@@ -346,39 +350,28 @@
*---------------------------------------------------------------------------*)
-(*----------------------------------------------------------------------------
- * This basic principle of definition takes a functional M and a relation R
- * and specializes the following theorem
- *
- * |- !M R f. (f = WFREC R M) ==> WF R ==> !x. f x = M (f%R,x) x
- *
- * to them (getting "th1", say). Then we make the definition "f = WFREC R M"
- * and instantiate "th1" to the constant "f" (getting th2). Then we use the
- * definition to delete the first antecedent to th2. Hence the result in
- * the "corollary" field is
- *
- * |- WF R ==> !x. f x = M (f%R,x) x
- *
+(*---------------------------------------------------------------------------
+ * 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
+ val fname = #Name(S.dest_var f)
+ val (wfrec,_) = S.strip_comb rhs
+in
+fun wfrec_definition0 thy R functional =
+ let val {Bvar,...} = S.dest_abs functional
+ val {Name, Ty} = S.dest_var Bvar
+ val def_name = U.concat Name "_def"
+ val (_,ty_theta) = Thry.match_term thy f (S.mk_var{Name=fname,Ty=Ty})
+ val wfrec' = S.inst ty_theta wfrec
+ val wfrec_R_M' = S.list_mk_comb(wfrec',[R,functional])
+ val def_term = S.mk_eq{lhs=Bvar, rhs=wfrec_R_M'}
+ in
+ Thry.make_definition thy def_name def_term
+ end
+end;
-fun prim_wfrec_definition thy {R, functional} =
- let val tych = Thry.typecheck thy
- val {Bvar,...} = S.dest_abs functional
- val {Name,...} = S.dest_var Bvar (* Intended name of definition *)
- val cor1 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
- val cor2 = R.ISPEC (tych R) cor1
- val f_eq_WFREC_R_M = (#ant o S.dest_imp o #Body
- o S.dest_forall o concl) cor2
- val {lhs,rhs} = S.dest_eq f_eq_WFREC_R_M
- val {Ty, ...} = S.dest_var lhs
- val def_term = S.mk_eq{lhs = S.mk_var{Name=Name,Ty=Ty}, rhs=rhs}
- val (def_thm,thy1) = Thry.make_definition thy
- (U.concat Name "_def") def_term
- val (_,[f,_]) = (S.strip_comb o concl) def_thm
- val cor3 = R.ISPEC (Thry.typecheck thy1 f) cor2
- in
- {theory = thy1, def=def_thm, corollary=R.MP cor3 def_thm}
- end;
(*---------------------------------------------------------------------------
@@ -422,26 +415,16 @@
val givens = U.mapfilter not_omitted;
-(*--------------------------------------------------------------------------
- * This is a wrapper for "prim_wfrec_definition": it builds a functional,
- * calls "prim_wfrec_definition", then specializes the result. This gives a
- * list of rewrite rules where the right hand sides are quite ugly, so we
- * simplify to get rid of the case statements. In essence, this function
- * performs pre- and post-processing for patterns. As well, after
- * simplification, termination conditions are extracted.
- *-------------------------------------------------------------------------*)
-
-fun gen_wfrec_definition thy {R, eqs} =
- let val {functional,pats} = mk_functional thy eqs
+fun post_definition (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
val given_pats = givens pats
- val {def,corollary,theory} = prim_wfrec_definition thy
- {R=R, functional=functional}
- val tych = Thry.typecheck theory
- val {lhs=f,...} = S.dest_eq(concl def)
val WFR = #ant(S.dest_imp(concl corollary))
+ val R = #Rand(S.dest_comb WFR)
val corollary' = R.UNDISCH corollary (* put WF R on assums *)
val corollaries = map (U.C R.SPEC corollary' o tych) given_pats
- val (case_rewrites,context_congs) = extraction_thms thy
+ 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)
{thms = [(R.ISPECL o map tych)[f,R] Thms.CUT_LEMMA],
@@ -459,7 +442,6 @@
patterns = pats}
end;
-
(*---------------------------------------------------------------------------
* Perform the extraction without making the definition. Definition and
* extraction commute for the non-nested case. For hol90 users, this
@@ -521,7 +503,7 @@
def
val body_th = R.LIST_CONJ (map (R.ASSUME o tych) full_rqt)
val bar = R.MP (R.BETA_RULE(R.ISPECL[tych R'abs, tych R1] Thms.SELECT_AX))
- body_th
+ body_th
in {theory = theory, R=R1,
rules = U.rev_itlist (U.C R.MP) (R.CONJUNCTS bar) def',
full_pats_TCs = merge (map pat_of pats) (U.zip (givens pats) TCl),
@@ -905,18 +887,4 @@
end;
-(*---------------------------------------------------------------------------
- * Extract termination goals so that they can be put it into a goalstack, or
- * have a tactic directly applied to them.
- *--------------------------------------------------------------------------*)
-local exception IS_NEG
- fun strip_imp tm = if S.is_neg tm then raise IS_NEG else S.strip_imp tm
-in
-fun termination_goals rules =
- U.itlist (fn th => fn A =>
- let val tcl = (#1 o S.strip_imp o #2 o S.strip_forall o concl) th
- in tcl@A
- end handle _ => A) (R.CONJUNCTS rules) (hyp rules)
-end;
-
end; (* TFL *)
--- a/TFL/thms.sml Thu May 15 11:35:26 1997 +0200
+++ b/TFL/thms.sml Thu May 15 12:29:59 1997 +0200
@@ -2,9 +2,9 @@
struct
type Thm = Thm.thm
- val WFREC_COROLLARY = get_thm WF1.thy "tfl_wfrec"
- val WF_INDUCTION_THM = get_thm WF1.thy "tfl_wf_induct"
- val CUT_LEMMA = get_thm WF1.thy "tfl_cut_apply"
+ val WFREC_COROLLARY = get_thm WF_Rel.thy "tfl_wfrec"
+ val WF_INDUCTION_THM = get_thm WF_Rel.thy "tfl_wf_induct"
+ val CUT_LEMMA = get_thm WF_Rel.thy "tfl_cut_apply"
val CUT_DEF = cut_def
local val _ = goal HOL.thy "!P x. P x --> P (Eps P)"
--- a/TFL/thry.sml Thu May 15 11:35:26 1997 +0200
+++ b/TFL/thry.sml Thu May 15 12:29:59 1997 +0200
@@ -49,6 +49,14 @@
* 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 = #2 (S.strip_type ty)
@@ -59,17 +67,14 @@
val lhs1 = S.mk_const{Name = Name, Ty = Ty}
val eeq1 = S.mk_const{Name = eeq_name, Ty = Ty --> Ty --> prop}
val dtm = S.list_mk_comb(eeq1,[lhs1,rhs]) (* Rename "=" to "==" *)
- val thry1 = add_consts_i [(Name,Ty,NoSyn)] parent
- val thry2 = add_defs_i [(s,dtm)] thry1
- val parent_names = map ! (stamps_of_thy parent)
- val newthy_name = variant parent_names (hd parent_names)
- val new_thy = add_thyname newthy_name thry2
+ 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
- ((get_axiom new_thy s) RS meta_eq_to_obj_eq, new_thy)
- end
+ (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
--- a/TFL/utils.sml Thu May 15 11:35:26 1997 +0200
+++ b/TFL/utils.sml Thu May 15 12:29:59 1997 +0200
@@ -19,7 +19,7 @@
val MESG_string = info_string "Message"
end;
-fun Raise (e as ERR sss) = (prs (ERR_string sss); raise e)
+fun Raise (e as ERR sss) = (output(std_out, ERR_string sss); raise e)
| Raise e = raise e;