--- a/src/HOL/Import/replay.ML Wed Dec 15 17:14:44 2010 +0100
+++ b/src/HOL/Import/replay.ML Wed Dec 15 17:43:22 2010 +0100
@@ -2,11 +2,9 @@
Author: Sebastian Skalberg (TU Muenchen)
*)
-structure Replay =
+structure Replay = (* FIXME proper signature *)
struct
-structure P = ProofKernel
-
open ProofKernel
open ImportRecorder
@@ -17,12 +15,12 @@
fun replay_proof int_thms thyname thmname prf thy =
let
val _ = ImportRecorder.start_replay_proof thyname thmname
- fun rp (PRefl tm) thy = P.REFL tm thy
+ fun rp (PRefl tm) thy = ProofKernel.REFL tm thy
| rp (PInstT(p,lambda)) thy =
let
val (thy',th) = rp' p thy
in
- P.INST_TYPE lambda th thy'
+ ProofKernel.INST_TYPE lambda th thy'
end
| rp (PSubst(prfs,ctxt,prf)) thy =
let
@@ -34,52 +32,52 @@
end) prfs (thy,[])
val (thy'',th) = rp' prf thy'
in
- P.SUBST ths ctxt th thy''
+ ProofKernel.SUBST ths ctxt th thy''
end
| rp (PAbs(prf,v)) thy =
let
val (thy',th) = rp' prf thy
in
- P.ABS v th thy'
+ ProofKernel.ABS v th thy'
end
| rp (PDisch(prf,tm)) thy =
let
val (thy',th) = rp' prf thy
in
- P.DISCH tm th thy'
+ ProofKernel.DISCH tm th thy'
end
| rp (PMp(prf1,prf2)) thy =
let
val (thy1,th1) = rp' prf1 thy
val (thy2,th2) = rp' prf2 thy1
in
- P.MP th1 th2 thy2
+ ProofKernel.MP th1 th2 thy2
end
- | rp (PHyp tm) thy = P.ASSUME tm thy
+ | rp (PHyp tm) thy = ProofKernel.ASSUME tm thy
| rp (PDef(seg,name,rhs)) thy =
- (case P.get_def seg name rhs thy of
+ (case ProofKernel.get_def seg name rhs thy of
(thy',SOME res) => (thy',res)
| (thy',NONE) =>
if seg = thyname
- then P.new_definition seg name rhs thy'
+ then ProofKernel.new_definition seg name rhs thy'
else raise ERR "replay_proof" ("Too late for term definition: "^seg^" != "^thyname))
- | rp (POracle(tg,asl,c)) thy = (*P.mk_oracle_thm tg (map be_contract asl,c)*) NY "ORACLE"
+ | rp (POracle(tg,asl,c)) thy = (*ProofKernel.mk_oracle_thm tg (map be_contract asl,c)*) NY "ORACLE"
| rp (PSpec(prf,tm)) thy =
let
val (thy',th) = rp' prf thy
in
- P.SPEC tm th thy'
+ ProofKernel.SPEC tm th thy'
end
| rp (PInst(prf,theta)) thy =
let
val (thy',th) = rp' prf thy
in
- P.INST theta th thy'
+ ProofKernel.INST theta th thy'
end
| rp (PGen(prf,v)) thy =
let
val (thy',th) = rp' prf thy
- val p = P.GEN v th thy'
+ val p = ProofKernel.GEN v th thy'
in
p
end
@@ -87,91 +85,91 @@
let
val (thy',th) = rp' prf thy
in
- P.GEN_ABS opt vl th thy'
+ ProofKernel.GEN_ABS opt vl th thy'
end
| rp (PImpAS(prf1,prf2)) thy =
let
val (thy1,th1) = rp' prf1 thy
val (thy2,th2) = rp' prf2 thy1
in
- P.IMP_ANTISYM th1 th2 thy2
+ ProofKernel.IMP_ANTISYM th1 th2 thy2
end
| rp (PSym prf) thy =
let
val (thy1,th) = rp' prf thy
in
- P.SYM th thy1
+ ProofKernel.SYM th thy1
end
| rp (PTrans(prf1,prf2)) thy =
let
val (thy1,th1) = rp' prf1 thy
val (thy2,th2) = rp' prf2 thy1
in
- P.TRANS th1 th2 thy2
+ ProofKernel.TRANS th1 th2 thy2
end
| rp (PComb(prf1,prf2)) thy =
let
val (thy1,th1) = rp' prf1 thy
val (thy2,th2) = rp' prf2 thy1
in
- P.COMB th1 th2 thy2
+ ProofKernel.COMB th1 th2 thy2
end
| rp (PEqMp(prf1,prf2)) thy =
let
val (thy1,th1) = rp' prf1 thy
val (thy2,th2) = rp' prf2 thy1
in
- P.EQ_MP th1 th2 thy2
+ ProofKernel.EQ_MP th1 th2 thy2
end
| rp (PEqImp prf) thy =
let
val (thy',th) = rp' prf thy
in
- P.EQ_IMP_RULE th thy'
+ ProofKernel.EQ_IMP_RULE th thy'
end
| rp (PExists(prf,ex,wit)) thy =
let
val (thy',th) = rp' prf thy
in
- P.EXISTS ex wit th thy'
+ ProofKernel.EXISTS ex wit th thy'
end
| rp (PChoose(v,prf1,prf2)) thy =
let
val (thy1,th1) = rp' prf1 thy
val (thy2,th2) = rp' prf2 thy1
in
- P.CHOOSE v th1 th2 thy2
+ ProofKernel.CHOOSE v th1 th2 thy2
end
| rp (PConj(prf1,prf2)) thy =
let
val (thy1,th1) = rp' prf1 thy
val (thy2,th2) = rp' prf2 thy1
in
- P.CONJ th1 th2 thy2
+ ProofKernel.CONJ th1 th2 thy2
end
| rp (PConjunct1 prf) thy =
let
val (thy',th) = rp' prf thy
in
- P.CONJUNCT1 th thy'
+ ProofKernel.CONJUNCT1 th thy'
end
| rp (PConjunct2 prf) thy =
let
val (thy',th) = rp' prf thy
in
- P.CONJUNCT2 th thy'
+ ProofKernel.CONJUNCT2 th thy'
end
| rp (PDisj1(prf,tm)) thy =
let
val (thy',th) = rp' prf thy
in
- P.DISJ1 th tm thy'
+ ProofKernel.DISJ1 th tm thy'
end
| rp (PDisj2(prf,tm)) thy =
let
val (thy',th) = rp' prf thy
in
- P.DISJ2 tm th thy'
+ ProofKernel.DISJ2 tm th thy'
end
| rp (PDisjCases(prf,prf1,prf2)) thy =
let
@@ -179,25 +177,25 @@
val (thy1,th1) = rp' prf1 thy'
val (thy2,th2) = rp' prf2 thy1
in
- P.DISJ_CASES th th1 th2 thy2
+ ProofKernel.DISJ_CASES th th1 th2 thy2
end
| rp (PNotI prf) thy =
let
val (thy',th) = rp' prf thy
in
- P.NOT_INTRO th thy'
+ ProofKernel.NOT_INTRO th thy'
end
| rp (PNotE prf) thy =
let
val (thy',th) = rp' prf thy
in
- P.NOT_ELIM th thy'
+ ProofKernel.NOT_ELIM th thy'
end
| rp (PContr(prf,tm)) thy =
let
val (thy',th) = rp' prf thy
in
- P.CCONTR tm th thy'
+ ProofKernel.CCONTR tm th thy'
end
| rp (PTmSpec _) _ = raise ERR "rp" "Shouldn't reach here (PTmSpec)"
| rp (PTyDef _) _ = raise ERR "rp" "Shouldn't reach here (PTyDef)"
@@ -226,7 +224,7 @@
| SOME th => (thy,th))
else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")
| NONE =>
- (case P.get_thm thyname' thmname thy of
+ (case ProofKernel.get_thm thyname' thmname thy of
(thy',SOME res) => (thy',res)
| (thy',NONE) =>
if thyname' = thyname
@@ -242,31 +240,31 @@
PTmSpec _ => (thy',th)
| PTyDef _ => (thy',th)
| PTyIntro _ => (thy',th)
- | _ => P.store_thm thyname' thmname th thy'
+ | _ => ProofKernel.store_thm thyname' thmname th thy'
end
else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")))
| NONE => raise ERR "rp'.PDisk" "Not enough information")
| PAxm(name,c) =>
- (case P.get_axiom thyname name thy of
+ (case ProofKernel.get_axiom thyname name thy of
(thy',SOME res) => (thy',res)
- | (thy',NONE) => P.new_axiom name c thy')
+ | (thy',NONE) => ProofKernel.new_axiom name c thy')
| PTmSpec(seg,names,prf') =>
let
val (thy',th) = rp' prf' thy
in
- P.new_specification seg thmname names th thy'
+ ProofKernel.new_specification seg thmname names th thy'
end
| PTyDef(seg,name,prf') =>
let
val (thy',th) = rp' prf' thy
in
- P.new_type_definition seg thmname name th thy'
+ ProofKernel.new_type_definition seg thmname name th thy'
end
| PTyIntro(seg,name,abs_name,rep_name,P,t,prf') =>
let
val (thy',th) = rp' prf' thy
in
- P.type_introduction seg thmname name abs_name rep_name (P,t) th thy'
+ ProofKernel.type_introduction seg thmname name abs_name rep_name (P,t) th thy'
end
| _ => rp pc thy
end
@@ -282,7 +280,7 @@
fun setup_int_thms thyname thy =
let
val fname =
- case P.get_proof_dir thyname thy of
+ case ProofKernel.get_proof_dir thyname thy of
SOME p => OS.Path.joinDirFile {dir=p,file=OS.Path.joinBaseExt{base = "facts",ext=SOME "lst"}}
| NONE => error "Cannot find proof files"
val is = TextIO.openIn fname
@@ -291,7 +289,7 @@
fun get_facts facts =
case TextIO.inputLine is of
NONE => (case facts of
- i::facts => (the (Int.fromString i),map P.protect_factname (rev facts))
+ i::facts => (the (Int.fromString i),map ProofKernel.protect_factname (rev facts))
| _ => raise ERR "replay_thm" "Bad facts.lst file")
| SOME fact => get_facts ((String.substring(fact,0,String.size fact -1 ))::facts)
in
@@ -349,9 +347,9 @@
| delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =
add_hol4_type_mapping thyname tycname true fulltyname thy
| delta (Indexed_theorem (i, th)) thy =
- (Array.update (int_thms,i-1,SOME (P.to_hol_thm (th_of thy th))); thy)
- | delta (Protect_varname (s,t)) thy = (P.replay_protect_varname s t; thy)
- | delta (Dump s) thy = P.replay_add_dump s thy
+ (Array.update (int_thms,i-1,SOME (ProofKernel.to_hol_thm (th_of thy th))); thy)
+ | delta (Protect_varname (s,t)) thy = (ProofKernel.replay_protect_varname s t; thy)
+ | delta (Dump s) thy = ProofKernel.replay_add_dump s thy
in
rps
end
--- a/src/HOL/Nominal/nominal_atoms.ML Wed Dec 15 17:14:44 2010 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML Wed Dec 15 17:43:22 2010 +0100
@@ -1004,7 +1004,6 @@
(* syntax und parsing *)
-structure P = Parse and K = Keyword;
val _ =
Outer_Syntax.command "atom_decl" "declare new kinds of atoms" Keyword.thy_decl
--- a/src/HOL/Tools/TFL/dcterm.ML Wed Dec 15 17:14:44 2010 +0100
+++ b/src/HOL/Tools/TFL/dcterm.ML Wed Dec 15 17:43:22 2010 +0100
@@ -49,9 +49,7 @@
structure Dcterm: DCTERM =
struct
-structure U = Utils;
-
-fun ERR func mesg = U.ERR {module = "Dcterm", func = func, mesg = mesg};
+fun ERR func mesg = Utils.ERR {module = "Dcterm", func = func, mesg = mesg};
fun dest_comb t = Thm.dest_comb t
@@ -110,19 +108,19 @@
fun dest_monop expected tm =
let
fun err () = raise ERR "dest_monop" ("Not a(n) " ^ quote expected);
- val (c, N) = dest_comb tm handle U.ERR _ => err ();
- val name = #Name (dest_const c handle U.ERR _ => err ());
+ val (c, N) = dest_comb tm handle Utils.ERR _ => err ();
+ val name = #Name (dest_const c handle Utils.ERR _ => err ());
in if name = expected then N else err () end;
fun dest_binop expected tm =
let
fun err () = raise ERR "dest_binop" ("Not a(n) " ^ quote expected);
- val (M, N) = dest_comb tm handle U.ERR _ => err ()
- in (dest_monop expected M, N) handle U.ERR _ => err () end;
+ val (M, N) = dest_comb tm handle Utils.ERR _ => err ()
+ in (dest_monop expected M, N) handle Utils.ERR _ => err () end;
fun dest_binder expected tm =
dest_abs NONE (dest_monop expected tm)
- handle U.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected);
+ handle Utils.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected);
val dest_neg = dest_monop @{const_name Not}
@@ -151,7 +149,7 @@
(*---------------------------------------------------------------------------
* Iterated creation.
*---------------------------------------------------------------------------*)
-val list_mk_disj = U.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.)
@@ -160,7 +158,7 @@
let fun dest (p as (ctm,accum)) =
let val (M,N) = break ctm
in dest (N, M::accum)
- end handle U.ERR _ => p
+ end handle Utils.ERR _ => p
in dest (tm,[])
end;
@@ -190,7 +188,7 @@
handle TYPE (msg, _, _) => raise ERR "mk_prop" msg
| TERM (msg, _) => raise ERR "mk_prop" msg;
-fun drop_prop ctm = dest_monop @{const_name Trueprop} ctm handle U.ERR _ => ctm;
+fun drop_prop ctm = dest_monop @{const_name Trueprop} ctm handle Utils.ERR _ => ctm;
end;
--- a/src/HOL/Tools/TFL/post.ML Wed Dec 15 17:14:44 2010 +0100
+++ b/src/HOL/Tools/TFL/post.ML Wed Dec 15 17:43:22 2010 +0100
@@ -18,8 +18,6 @@
structure Tfl: TFL =
struct
-structure S = USyntax
-
(* misc *)
(*---------------------------------------------------------------------------
@@ -53,16 +51,14 @@
* processing from the definition stage.
*---------------------------------------------------------------------------*)
local
-structure R = Rules
-structure U = Utils
(* The rest of these local definitions are for the tricky nested case *)
-val solved = not o can S.dest_eq o #2 o S.strip_forall o concl
+val solved = not o can USyntax.dest_eq o #2 o USyntax.strip_forall o concl
fun id_thm th =
- let val {lhs,rhs} = S.dest_eq (#2 (S.strip_forall (#2 (R.dest_thm th))));
+ let val {lhs,rhs} = USyntax.dest_eq (#2 (USyntax.strip_forall (#2 (Rules.dest_thm th))));
in lhs aconv rhs end
- handle U.ERR _ => false;
+ handle Utils.ERR _ => false;
val P_imp_P_eq_True = @{thm eqTrueI} RS eq_reflection;
fun mk_meta_eq r = case concl_of r of
@@ -76,16 +72,16 @@
fun join_assums th =
let val thy = Thm.theory_of_thm th
val tych = cterm_of thy
- val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th)))
- val cntxtl = (#1 o S.strip_imp) lhs (* cntxtl should = cntxtr *)
- val cntxtr = (#1 o S.strip_imp) rhs (* but union is solider *)
+ val {lhs,rhs} = USyntax.dest_eq(#2 (USyntax.strip_forall (concl th)))
+ val cntxtl = (#1 o USyntax.strip_imp) lhs (* cntxtl should = cntxtr *)
+ val cntxtr = (#1 o USyntax.strip_imp) rhs (* but union is solider *)
val cntxt = union (op aconv) cntxtl cntxtr
in
- R.GEN_ALL
- (R.DISCH_ALL
- (rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th)))
+ Rules.GEN_ALL
+ (Rules.DISCH_ALL
+ (rewrite (map (Rules.ASSUME o tych) cntxt) (Rules.SPEC_ALL th)))
end
- val gen_all = S.gen_all
+ val gen_all = USyntax.gen_all
in
fun proof_stage strict cs ss wfs theory {f, R, rules, full_pats_TCs, TCs} =
let
@@ -117,7 +113,7 @@
in
{induction = induction',
rules = rules',
- tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl)
+ tcs = map (gen_all o USyntax.rhs o #2 o USyntax.strip_forall o concl)
(simplified@stubborn)}
end
end;
@@ -144,8 +140,8 @@
val def = Thm.unvarify_global def0 RS meta_eq_to_obj_eq
val {rules,rows,TCs,full_pats_TCs} =
Prim.post_definition congs (thy, (def,pats))
- val {lhs=f,rhs} = S.dest_eq (concl def)
- val (_,[R,_]) = S.strip_comb rhs
+ val {lhs=f,rhs} = USyntax.dest_eq (concl def)
+ val (_,[R,_]) = USyntax.strip_comb rhs
val dummy = Prim.trace_thms "congs =" congs
(*the next step has caused simplifier looping in some cases*)
val {induction, rules, tcs} =
@@ -154,12 +150,12 @@
full_pats_TCs = full_pats_TCs,
TCs = TCs}
val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm)
- (R.CONJUNCTS rules)
+ (Rules.CONJUNCTS rules)
in {induct = meta_outer ctxt (Object_Logic.rulify_no_asm (induction RS spec')),
rules = ListPair.zip(rules', rows),
tcs = (termination_goals rules') @ tcs}
end
- handle U.ERR {mesg,func,module} =>
+ handle Utils.ERR {mesg,func,module} =>
error (mesg ^
"\n (In TFL function " ^ module ^ "." ^ func ^ ")");
@@ -217,7 +213,7 @@
fun define strict thy cs ss congs wfs fid R seqs =
define_i strict thy cs ss congs wfs fid
(Syntax.read_term_global thy R) (map (Syntax.read_term_global thy) seqs)
- handle U.ERR {mesg,...} => error mesg;
+ handle Utils.ERR {mesg,...} => error mesg;
(*---------------------------------------------------------------------------
@@ -227,11 +223,11 @@
*---------------------------------------------------------------------------*)
fun func_of_cond_eqn tm =
- #1 (S.strip_comb (#lhs (S.dest_eq (#2 (S.strip_forall (#2 (S.strip_imp tm)))))));
+ #1 (USyntax.strip_comb (#lhs (USyntax.dest_eq (#2 (USyntax.strip_forall (#2 (USyntax.strip_imp tm)))))));
fun defer_i thy congs fid eqs =
let val {rules,R,theory,full_pats_TCs,SV,...} = Prim.lazyR_def thy fid congs eqs
- val f = func_of_cond_eqn (concl (R.CONJUNCT1 rules handle U.ERR _ => rules));
+ val f = func_of_cond_eqn (concl (Rules.CONJUNCT1 rules handle Utils.ERR _ => rules));
val dummy = writeln "Proving induction theorem ...";
val induction = Prim.mk_induction theory
{fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs}
@@ -243,7 +239,7 @@
fun defer thy congs fid seqs =
defer_i thy congs fid (map (Syntax.read_term_global thy) seqs)
- handle U.ERR {mesg,...} => error mesg;
+ handle Utils.ERR {mesg,...} => error mesg;
end;
end;
--- a/src/HOL/Tools/TFL/rules.ML Wed Dec 15 17:14:44 2010 +0100
+++ b/src/HOL/Tools/TFL/rules.ML Wed Dec 15 17:43:22 2010 +0100
@@ -57,16 +57,11 @@
structure Rules: RULES =
struct
-structure S = USyntax;
-structure U = Utils;
-structure D = Dcterm;
+fun RULES_ERR func mesg = Utils.ERR {module = "Rules", func = func, mesg = mesg};
-fun RULES_ERR func mesg = U.ERR {module = "Rules", func = func, mesg = mesg};
-
-
-fun cconcl thm = D.drop_prop (#prop (Thm.crep_thm thm));
-fun chyps thm = map D.drop_prop (#hyps (Thm.crep_thm thm));
+fun cconcl thm = Dcterm.drop_prop (#prop (Thm.crep_thm thm));
+fun chyps thm = map Dcterm.drop_prop (#hyps (Thm.crep_thm thm));
fun dest_thm thm =
let val {prop,hyps,...} = Thm.rep_thm thm
@@ -95,7 +90,7 @@
handle THM (msg, _, _) => raise RULES_ERR "ALPHA" msg;
fun rbeta th =
- (case D.strip_comb (cconcl th) of
+ (case Dcterm.strip_comb (cconcl th) of
(_, [l, r]) => Thm.transitive th (Thm.beta_conversion false r)
| _ => raise RULES_ERR "rbeta" "");
@@ -108,7 +103,7 @@
* "B" results in something that looks like "A --> B".
*---------------------------------------------------------------------------*)
-fun ASSUME ctm = Thm.assume (D.mk_prop ctm);
+fun ASSUME ctm = Thm.assume (Dcterm.mk_prop ctm);
(*---------------------------------------------------------------------------
@@ -119,7 +114,7 @@
handle THM (msg, _, _) => raise RULES_ERR "MP" msg;
(*forces the first argument to be a proposition if necessary*)
-fun DISCH tm thm = Thm.implies_intr (D.mk_prop tm) thm COMP impI
+fun DISCH tm thm = Thm.implies_intr (Dcterm.mk_prop tm) thm COMP impI
handle THM (msg, _, _) => raise RULES_ERR "DISCH" msg;
fun DISCH_ALL thm = fold_rev DISCH (#hyps (Thm.crep_thm thm)) thm;
@@ -131,9 +126,9 @@
end;
fun UNDISCH thm =
- let val tm = D.mk_prop (#1 (D.dest_imp (cconcl thm)))
+ let val tm = Dcterm.mk_prop (#1 (Dcterm.dest_imp (cconcl thm)))
in Thm.implies_elim (thm RS mp) (ASSUME tm) end
- handle U.ERR _ => raise RULES_ERR "UNDISCH" ""
+ handle Utils.ERR _ => raise RULES_ERR "UNDISCH" ""
| THM _ => raise RULES_ERR "UNDISCH" "";
fun PROVE_HYP ath bth = MP (DISCH (cconcl ath) bth) ath;
@@ -152,7 +147,7 @@
fun CONJUNCT2 thm = thm RS conjunct2
handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT2" msg;
-fun CONJUNCTS th = CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th) handle U.ERR _ => [th];
+fun CONJUNCTS th = CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th) handle Utils.ERR _ => [th];
fun LIST_CONJ [] = raise RULES_ERR "LIST_CONJ" "empty list"
| LIST_CONJ [th] = th
@@ -168,7 +163,7 @@
val [P,Q] = OldTerm.term_vars prop
val disj1 = Thm.forall_intr (Thm.cterm_of thy Q) disjI1
in
-fun DISJ1 thm tm = thm RS (Thm.forall_elim (D.drop_prop tm) disj1)
+fun DISJ1 thm tm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj1)
handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg;
end;
@@ -177,7 +172,7 @@
val [P,Q] = OldTerm.term_vars prop
val disj2 = Thm.forall_intr (Thm.cterm_of thy P) disjI2
in
-fun DISJ2 tm thm = thm RS (Thm.forall_elim (D.drop_prop tm) disj2)
+fun DISJ2 tm thm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj2)
handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg;
end;
@@ -195,10 +190,10 @@
let fun blue ldisjs [] _ = []
| blue ldisjs (th::rst) rdisjs =
let val tail = tl rdisjs
- val rdisj_tl = D.list_mk_disj tail
+ val rdisj_tl = Dcterm.list_mk_disj tail
in fold_rev DISJ2 ldisjs (DISJ1 th rdisj_tl)
:: blue (ldisjs @ [cconcl th]) rst tail
- end handle U.ERR _ => [fold_rev DISJ2 ldisjs th]
+ end handle Utils.ERR _ => [fold_rev DISJ2 ldisjs th]
in blue [] thms (map cconcl thms) end;
@@ -212,8 +207,8 @@
fun DISJ_CASES th1 th2 th3 =
let
- val c = D.drop_prop (cconcl th1);
- val (disj1, disj2) = D.dest_disj c;
+ val c = Dcterm.drop_prop (cconcl th1);
+ val (disj1, disj2) = Dcterm.dest_disj c;
val th2' = DISCH disj1 th2;
val th3' = DISCH disj2 th3;
in
@@ -253,12 +248,12 @@
fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t
aconv term_of atm)
(#hyps(rep_thm th))
- val tml = D.strip_disj c
+ val tml = Dcterm.strip_disj c
fun DL th [] = raise RULES_ERR "DISJ_CASESL" "no cases"
| DL th [th1] = PROVE_HYP th th1
| DL th [th1,th2] = DISJ_CASES th th1 th2
| DL th (th1::rst) =
- let val tm = #2(D.dest_disj(D.drop_prop(cconcl th)))
+ let val tm = #2 (Dcterm.dest_disj (Dcterm.drop_prop(cconcl th)))
in DISJ_CASES th th1 (DL (ASSUME tm) rst) end
in DL disjth (organize eq tml thl)
end;
@@ -279,7 +274,7 @@
in thm RS (Thm.forall_elim tm gspec') end
end;
-fun SPEC_ALL thm = fold SPEC (#1(D.strip_forall(cconcl thm))) thm;
+fun SPEC_ALL thm = fold SPEC (#1 (Dcterm.strip_forall(cconcl thm))) thm;
val ISPEC = SPEC
val ISPECL = fold ISPEC;
@@ -323,7 +318,7 @@
fun MATCH_MP th1 th2 =
- if (D.is_forall (D.drop_prop(cconcl th1)))
+ if (Dcterm.is_forall (Dcterm.drop_prop(cconcl th1)))
then MATCH_MP (th1 RS spec) th2
else MP th1 th2;
@@ -345,8 +340,8 @@
fun CHOOSE (fvar, exth) fact =
let
- val lam = #2 (D.dest_comb (D.drop_prop (cconcl exth)))
- val redex = D.capply lam fvar
+ val lam = #2 (Dcterm.dest_comb (Dcterm.drop_prop (cconcl exth)))
+ val redex = Dcterm.capply lam fvar
val thy = Thm.theory_of_cterm redex
val t$u = Thm.term_of redex
val residue = Thm.cterm_of thy (Term.betapply (t, u))
@@ -364,7 +359,7 @@
val prop = Thm.prop_of thm
val P' = cterm_of thy P
val x' = cterm_of thy x
- val abstr = #2 (D.dest_comb template)
+ val abstr = #2 (Dcterm.dest_comb template)
in
thm RS (cterm_instantiate[(P',abstr), (x',witness)] exI)
handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg
@@ -380,7 +375,7 @@
*---------------------------------------------------------------------------*)
fun EXISTL vlist th =
- fold_rev (fn v => fn thm => EXISTS(D.mk_exists(v,cconcl thm), v) thm)
+ fold_rev (fn v => fn thm => EXISTS(Dcterm.mk_exists(v,cconcl thm), v) thm)
vlist th;
@@ -397,7 +392,7 @@
let val thy = Thm.theory_of_thm th
val tych = cterm_of thy
val blist' = map (pairself Thm.term_of) blist
- fun ex v M = cterm_of thy (S.mk_exists{Bvar=v,Body = M})
+ fun ex v M = cterm_of thy (USyntax.mk_exists{Bvar=v,Body = M})
in
fold_rev (fn (b as (r1,r2)) => fn thm =>
@@ -443,7 +438,7 @@
(* Object language quantifier, i.e., "!" *)
-fun Forall v M = S.mk_forall{Bvar=v, Body=M};
+fun Forall v M = USyntax.mk_forall{Bvar=v, Body=M};
(* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *)
@@ -458,11 +453,11 @@
(Const (@{const_name Trueprop},_) $ lhs)
$ (Const (@{const_name Trueprop},_) $ rhs)) = {lhs=lhs, rhs=rhs}
| dest_equal(Const ("==",_) $ lhs $ rhs) = {lhs=lhs, rhs=rhs}
- | dest_equal tm = S.dest_eq tm;
+ | dest_equal tm = USyntax.dest_eq tm;
fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm));
-fun dest_all used (Const("all",_) $ (a as Abs _)) = S.dest_abs used a
+fun dest_all used (Const("all",_) $ (a as Abs _)) = USyntax.dest_abs used a
| dest_all _ _ = raise RULES_ERR "dest_all" "not a !!";
val is_all = can (dest_all []);
@@ -505,13 +500,13 @@
of ([],_) => get (rst, n+1,L)
| (vlist,body) =>
let val eq = Logic.strip_imp_concl body
- val (f,args) = S.strip_comb (get_lhs eq)
- val (vstrl,_) = S.strip_abs f
+ val (f,args) = USyntax.strip_comb (get_lhs eq)
+ val (vstrl,_) = USyntax.strip_abs f
val names =
Name.variant_list (OldTerm.add_term_names(body, [])) (map (#1 o dest_Free) vstrl)
in get (rst, n+1, (names,n)::L) end
handle TERM _ => get (rst, n+1, L)
- | U.ERR _ => get (rst, n+1, L);
+ | Utils.ERR _ => get (rst, n+1, L);
(* Note: Thm.rename_params_rule counts from 1, not 0 *)
fun rename thm =
@@ -529,7 +524,7 @@
*---------------------------------------------------------------------------*)
fun list_beta_conv tm =
- let fun rbeta th = Thm.transitive th (Thm.beta_conversion false (#2(D.dest_eq(cconcl th))))
+ let fun rbeta th = Thm.transitive th (Thm.beta_conversion false (#2(Dcterm.dest_eq(cconcl th))))
fun iter [] = Thm.reflexive tm
| iter (v::rst) = rbeta (Thm.combination(iter rst) (Thm.reflexive v))
in iter end;
@@ -553,28 +548,28 @@
* General abstraction handlers, should probably go in USyntax.
*---------------------------------------------------------------------------*)
fun mk_aabs (vstr, body) =
- S.mk_abs {Bvar = vstr, Body = body}
- handle U.ERR _ => S.mk_pabs {varstruct = vstr, body = body};
+ USyntax.mk_abs {Bvar = vstr, Body = body}
+ handle Utils.ERR _ => USyntax.mk_pabs {varstruct = vstr, body = body};
fun list_mk_aabs (vstrl,tm) =
fold_rev (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm;
fun dest_aabs used tm =
- let val ({Bvar,Body}, used') = S.dest_abs used tm
+ let val ({Bvar,Body}, used') = USyntax.dest_abs used tm
in (Bvar, Body, used') end
- handle U.ERR _ =>
- let val {varstruct, body, used} = S.dest_pabs used tm
+ handle Utils.ERR _ =>
+ let val {varstruct, body, used} = USyntax.dest_pabs used tm
in (varstruct, body, used) end;
fun strip_aabs used tm =
let val (vstr, body, used') = dest_aabs used tm
val (bvs, core, used'') = strip_aabs used' body
in (vstr::bvs, core, used'') end
- handle U.ERR _ => ([], tm, used);
+ handle Utils.ERR _ => ([], tm, used);
fun dest_combn tm 0 = (tm,[])
| dest_combn tm n =
- let val {Rator,Rand} = S.dest_comb tm
+ let val {Rator,Rand} = USyntax.dest_comb tm
val (f,rands) = dest_combn Rator (n-1)
in (f,Rand::rands)
end;
@@ -582,7 +577,7 @@
-local fun dest_pair M = let val {fst,snd} = S.dest_pair M in (fst,snd) end
+local fun dest_pair M = let val {fst,snd} = USyntax.dest_pair M in (fst,snd) end
fun mk_fst tm =
let val ty as Type(@{type_name Product_Type.prod}, [fty,sty]) = type_of tm
in Const ("Product_Type.fst", ty --> fty) $ tm end
@@ -610,7 +605,7 @@
*---------------------------------------------------------------------------*)
fun VSTRUCT_ELIM tych a vstr th =
- let val L = S.free_vars_lr vstr
+ let val L = USyntax.free_vars_lr vstr
val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr)))
val thm1 = Thm.implies_intr bind1 (SUBS [SYM(Thm.assume bind1)] th)
val thm2 = forall_intr_list (map tych L) thm1
@@ -641,7 +636,7 @@
in (strip_aabs used f,args)
end;
-fun pbeta_redex M n = can (U.C (dest_pbeta_redex []) n) M;
+fun pbeta_redex M n = can (Utils.C (dest_pbeta_redex []) n) M;
fun dest_impl tm =
let val ants = Logic.strip_imp_prems tm
@@ -649,7 +644,7 @@
in (ants,get_lhs eq)
end;
-fun restricted t = is_some (S.find_term
+fun restricted t = is_some (USyntax.find_term
(fn (Const(@{const_name Recdef.cut},_)) =>true | _ => false)
t)
@@ -675,7 +670,7 @@
val lhs = tych(get_lhs eq)
val ss' = Simplifier.add_prems (map ASSUME ants) ss
val lhs_eq_lhs1 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used) ss' lhs
- handle U.ERR _ => Thm.reflexive lhs
+ handle Utils.ERR _ => Thm.reflexive lhs
val dummy = print_thms "proven:" [lhs_eq_lhs1]
val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq
@@ -693,10 +688,10 @@
val eq1 = Logic.strip_imp_concl imp_body1
val Q = get_lhs eq1
val QeqQ1 = pbeta_reduce (tych Q)
- val Q1 = #2(D.dest_eq(cconcl QeqQ1))
+ val Q1 = #2(Dcterm.dest_eq(cconcl QeqQ1))
val ss' = Simplifier.add_prems (map ASSUME ants1) ss
val Q1eeqQ2 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used') ss' Q1
- handle U.ERR _ => Thm.reflexive Q1
+ handle Utils.ERR _ => Thm.reflexive Q1
val Q2 = #2 (Logic.dest_equals (Thm.prop_of Q1eeqQ2))
val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
val Q2eeqQ3 = Thm.symmetric(pbeta_reduce Q3 RS eq_reflection)
@@ -708,7 +703,7 @@
val impth = implies_intr_list ants1 QeeqQ3
val impth1 = impth RS meta_eq_to_obj_eq
(* Need to abstract *)
- val ant_th = U.itlist2 (PGEN tych) args vstrl impth1
+ val ant_th = Utils.itlist2 (PGEN tych) args vstrl impth1
in ant_th COMP thm
end
fun q_eliminate (thm,imp,thy) =
@@ -722,7 +717,7 @@
val ss' = MetaSimplifier.add_prems (map ASSUME ants1) ss
val Q_eeq_Q1 = MetaSimplifier.rewrite_cterm
(false,true,false) (prover used') ss' (tych Q)
- handle U.ERR _ => Thm.reflexive (tych Q)
+ handle Utils.ERR _ => Thm.reflexive (tych Q)
val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq
val ant_th = forall_intr_list(map tych vlist)lhs_eq_lhs2
@@ -740,7 +735,7 @@
(* Assume that the leading constant is ==, *)
| _ => thm (* if it is not a ==> *)
in SOME(eliminate (rename thm)) end
- handle U.ERR _ => NONE (* FIXME handle THM as well?? *)
+ handle Utils.ERR _ => NONE (* FIXME handle THM as well?? *)
fun restrict_prover ss thm =
let val dummy = say "restrict_prover:"
@@ -765,12 +760,12 @@
val rcontext = rev cntxt
val cncl = HOLogic.dest_Trueprop o Thm.prop_of
val antl = case rcontext of [] => []
- | _ => [S.list_mk_conj(map cncl rcontext)]
- val TC = genl(S.list_mk_imp(antl, A))
+ | _ => [USyntax.list_mk_conj(map cncl rcontext)]
+ val TC = genl(USyntax.list_mk_imp(antl, A))
val dummy = print_cterm "func:" (cterm_of thy func)
val dummy = print_cterm "TC:" (cterm_of thy (HOLogic.mk_Trueprop TC))
val dummy = tc_list := (TC :: !tc_list)
- val nestedp = is_some (S.find_term is_func TC)
+ val nestedp = is_some (USyntax.find_term is_func TC)
val dummy = if nestedp then say "nested" else say "not_nested"
val th' = if nestedp then raise RULES_ERR "solver" "nested function"
else let val cTC = cterm_of thy
@@ -782,7 +777,7 @@
end
val th'' = th' RS thm
in SOME (th'')
- end handle U.ERR _ => NONE (* FIXME handle THM as well?? *)
+ end handle Utils.ERR _ => NONE (* FIXME handle THM as well?? *)
in
(if (is_cong thm) then cong_prover else restrict_prover) ss thm
end
--- a/src/HOL/Tools/TFL/tfl.ML Wed Dec 15 17:14:44 2010 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML Wed Dec 15 17:43:22 2010 +0100
@@ -42,17 +42,13 @@
val trace = Unsynchronized.ref false;
-structure R = Rules;
-structure S = USyntax;
-structure U = Utils;
+fun TFL_ERR func mesg = Utils.ERR {module = "Tfl", func = func, mesg = mesg};
-fun TFL_ERR func mesg = U.ERR {module = "Tfl", func = func, mesg = mesg};
+val concl = #2 o Rules.dest_thm;
+val hyp = #1 o Rules.dest_thm;
-val concl = #2 o R.dest_thm;
-val hyp = #1 o R.dest_thm;
-
-val list_mk_type = U.end_itlist (curry (op -->));
+val list_mk_type = Utils.end_itlist (curry (op -->));
fun front_last [] = raise TFL_ERR "front_last" "empty list"
| front_last [x] = ([],x)
@@ -99,12 +95,12 @@
val (in_group, not_in_group) =
fold_rev (fn (row as (p::rst, rhs)) =>
fn (in_group,not_in_group) =>
- let val (pc,args) = S.strip_comb p
+ let val (pc,args) = USyntax.strip_comb p
in if (#1(dest_Const pc) = c)
then ((args@rst, rhs)::in_group, not_in_group)
else (in_group, row::not_in_group)
end) rows ([],[])
- val col_types = U.take type_of (length L, #1(hd in_group))
+ val col_types = Utils.take type_of (length L, #1(hd in_group))
in
part{constrs = crst, rows = not_in_group,
A = {constructor = c,
@@ -142,8 +138,8 @@
val L = binder_types Ty
and ty = body_type Ty
val ty_theta = ty_match ty colty
- val c' = S.inst ty_theta c
- val gvars = map (S.inst ty_theta o gv) L
+ val c' = USyntax.inst ty_theta c
+ val gvars = map (USyntax.inst ty_theta o gv) L
in (c', gvars)
end;
@@ -155,7 +151,7 @@
fun mk_group name rows =
fold_rev (fn (row as ((prfx, p::rst), rhs)) =>
fn (in_group,not_in_group) =>
- let val (pc,args) = S.strip_comb p
+ let val (pc,args) = USyntax.strip_comb p
in if ((#1 (Term.dest_Const pc) = name) handle TERM _ => false)
then (((prfx,args@rst), rhs)::in_group, not_in_group)
else (in_group, row::not_in_group) end)
@@ -174,7 +170,7 @@
val (in_group, not_in_group) = mk_group (#1 (dest_Const c')) rows
val in_group' =
if (null in_group) (* Constructor not given *)
- then [((prfx, #2(fresh c)), (S.ARB res_ty, (~1,false)))]
+ then [((prfx, #2(fresh c)), (USyntax.ARB res_ty, (~1,false)))]
else in_group
in
part{constrs = crst,
@@ -264,7 +260,7 @@
(ListPair.zip (new_formals, groups))
val rec_calls = map mk news
val (pat_rect,dtrees) = ListPair.unzip rec_calls
- val case_functions = map S.list_mk_abs
+ val case_functions = map USyntax.list_mk_abs
(ListPair.zip (new_formals, dtrees))
val types = map type_of (case_functions@[u]) @ [range_ty]
val case_const' = Const(case_const_name, list_mk_type types)
@@ -279,11 +275,11 @@
(* Repeated variable occurrences in a pattern are not allowed. *)
fun FV_multiset tm =
- case (S.dest_term tm)
- of S.VAR{Name = c, Ty = T} => [Free(c, T)]
- | S.CONST _ => []
- | S.COMB{Rator, Rand} => FV_multiset Rator @ FV_multiset Rand
- | S.LAMB _ => raise TFL_ERR "FV_multiset" "lambda";
+ case (USyntax.dest_term tm)
+ of USyntax.VAR{Name = c, Ty = T} => [Free(c, T)]
+ | USyntax.CONST _ => []
+ | USyntax.COMB{Rator, Rand} => FV_multiset Rator @ FV_multiset Rand
+ | USyntax.LAMB _ => raise TFL_ERR "FV_multiset" "lambda";
fun no_repeat_vars thy pat =
let fun check [] = true
@@ -370,10 +366,10 @@
| poly_tvars (TVar ((a,i),sort)) = TVar (("?" ^ a, i+1), sort);
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
+ #ant(USyntax.dest_imp(#2(USyntax.strip_forall (concl Thms.WFREC_COROLLARY))))
+ val {lhs=f, rhs} = USyntax.dest_eq f_eq_wfrec_R_M
val (fname,_) = dest_Free f
- val (wfrec,_) = S.strip_comb rhs
+ val (wfrec,_) = USyntax.strip_comb rhs
in
fun wfrec_definition0 thy fid R (functional as Abs(x, Ty, _)) =
let val def_name = Long_Name.base_name fid ^ "_def"
@@ -422,15 +418,15 @@
fun post_definition meta_tflCongs (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 f = #lhs(USyntax.dest_eq(concl def))
+ val corollary = Rules.MATCH_MP Thms.WFREC_COROLLARY def
val pats' = filter given pats
val given_pats = map pat_of pats'
val rows = map row_of_pat pats'
- 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 (fn pat => R.SPEC (tych pat) corollary')
+ val WFR = #ant(USyntax.dest_imp(concl corollary))
+ val R = #Rand(USyntax.dest_comb WFR)
+ val corollary' = Rules.UNDISCH corollary (* put WF R on assums *)
+ val corollaries = map (fn pat => Rules.SPEC (tych pat) corollary')
given_pats
val (case_rewrites,context_congs) = extraction_thms theory
(*case_ss causes minimal simplification: bodies of case expressions are
@@ -440,12 +436,12 @@
(HOL_basic_ss addcongs
(map (#weak_case_cong o snd) o Symtab.dest o Datatype.get_all) theory addsimps case_rewrites)
val corollaries' = map (Simplifier.simplify case_ss) corollaries
- val extract = R.CONTEXT_REWRITE_RULE
+ val extract = Rules.CONTEXT_REWRITE_RULE
(f, [R], @{thm cut_apply}, meta_tflCongs@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)
+ val mk_cond_rule = Rules.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
+ val rules1 = Rules.LIST_CONJ(map mk_cond_rule rules0)
in
{rules = rules1,
rows = rows,
@@ -463,8 +459,8 @@
*---------------------------------------------------------------------------*)
fun wfrec_eqns thy fid tflCongs eqns =
- let val {lhs,rhs} = S.dest_eq (hd eqns)
- val (f,args) = S.strip_comb lhs
+ let val {lhs,rhs} = USyntax.dest_eq (hd eqns)
+ val (f,args) = USyntax.strip_comb lhs
val (fname,fty) = dest_atom f
val (SV,a) = front_last args (* SV = schematic variables *)
val g = list_comb(f,SV)
@@ -482,22 +478,22 @@
else ()
val (case_rewrites,context_congs) = extraction_thms thy
val tych = Thry.typecheck thy
- val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
+ val WFREC_THM0 = Rules.ISPEC (tych functional) Thms.WFREC_COROLLARY
val Const(@{const_name All},_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
val R = Free (Name.variant (List.foldr OldTerm.add_term_names [] eqns) Rname,
Rtype)
- val WFREC_THM = R.ISPECL [tych R, tych g] WFREC_THM0
- val ([proto_def, WFR],_) = S.strip_imp(concl WFREC_THM)
+ val WFREC_THM = Rules.ISPECL [tych R, tych g] WFREC_THM0
+ val ([proto_def, WFR],_) = USyntax.strip_imp(concl WFREC_THM)
val dummy =
if !trace then
writeln ("ORIGINAL PROTO_DEF: " ^
Syntax.string_of_term_global thy proto_def)
else ()
- val R1 = S.rand WFR
- val corollary' = R.UNDISCH(R.UNDISCH WFREC_THM)
- val corollaries = map (fn pat => R.SPEC (tych pat) corollary') given_pats
+ val R1 = USyntax.rand WFR
+ val corollary' = Rules.UNDISCH (Rules.UNDISCH WFREC_THM)
+ val corollaries = map (fn pat => Rules.SPEC (tych pat) corollary') given_pats
val corollaries' = map (rewrite_rule case_rewrites) corollaries
- fun extract X = R.CONTEXT_REWRITE_RULE
+ fun extract X = Rules.CONTEXT_REWRITE_RULE
(f, R1::SV, @{thm cut_apply}, tflCongs@context_congs) X
in {proto_def = proto_def,
SV=SV,
@@ -517,8 +513,8 @@
fun lazyR_def thy fid tflCongs eqns =
let val {proto_def,WFR,pats,extracta,SV} =
wfrec_eqns thy fid tflCongs eqns
- val R1 = S.rand WFR
- val f = #lhs(S.dest_eq proto_def)
+ val R1 = USyntax.rand WFR
+ val f = #lhs(USyntax.dest_eq proto_def)
val (extractants,TCl) = ListPair.unzip extracta
val dummy = if !trace
then writeln (cat_lines ("Extractants =" ::
@@ -526,17 +522,17 @@
else ()
val TCs = fold_rev (union (op aconv)) TCl []
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 R' = USyntax.mk_select{Bvar=R1, Body=USyntax.list_mk_conj full_rqt}
+ val R'abs = USyntax.rand R'
val proto_def' = subst_free[(R1,R')] proto_def
val dummy = if !trace then writeln ("proto_def' = " ^
Syntax.string_of_term_global
thy proto_def')
else ()
- val {lhs,rhs} = S.dest_eq proto_def'
- val (c,args) = S.strip_comb lhs
+ val {lhs,rhs} = USyntax.dest_eq proto_def'
+ val (c,args) = USyntax.strip_comb lhs
val (name,Ty) = dest_atom c
- val defn = const_def thy (name, Ty, S.list_mk_abs (args,rhs))
+ val defn = const_def thy (name, Ty, USyntax.list_mk_abs (args,rhs))
val ([def0], theory) =
thy
|> Global_Theory.add_defs false
@@ -545,31 +541,31 @@
val dummy =
if !trace then writeln ("DEF = " ^ Display.string_of_thm_global theory def)
else ()
- (* val fconst = #lhs(S.dest_eq(concl def)) *)
+ (* val fconst = #lhs(USyntax.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*)
- val baz = R.DISCH_ALL
- (fold_rev R.DISCH full_rqt_prop
- (R.LIST_CONJ extractants))
+ val baz = Rules.DISCH_ALL
+ (fold_rev Rules.DISCH full_rqt_prop
+ (Rules.LIST_CONJ extractants))
val dum = if !trace then writeln ("baz = " ^ Display.string_of_thm_global theory baz)
else ()
val f_free = Free (fid, fastype_of f) (*'cos f is a Const*)
val SV' = map tych SV;
val SVrefls = map Thm.reflexive SV'
- val def0 = (fold (fn x => fn th => R.rbeta(Thm.combination th x))
+ val def0 = (fold (fn x => fn th => Rules.rbeta(Thm.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 def' = Rules.MP (Rules.SPEC (tych R') (Rules.GEN (tych R1) baz)) def0
+ val body_th = Rules.LIST_CONJ (map Rules.ASSUME full_rqt_prop)
val SELECT_AX = (*in this way we hope to avoid a STATIC dependence upon
theory Hilbert_Choice*)
ML_Context.thm "Hilbert_Choice.tfl_some"
handle ERROR msg => cat_error msg
"defer_recdef requires theory Main or at least Hilbert_Choice as parent"
- val bar = R.MP (R.ISPECL[tych R'abs, tych R1] SELECT_AX) body_th
+ val bar = Rules.MP (Rules.ISPECL[tych R'abs, tych R1] SELECT_AX) body_th
in {theory = theory, R=R1, SV=SV,
- rules = fold (U.C R.MP) (R.CONJUNCTS bar) def',
+ rules = fold (Utils.C Rules.MP) (Rules.CONJUNCTS bar) def',
full_pats_TCs = merge (map pat_of pats) (ListPair.zip (givens pats, TCl)),
patterns = pats}
end;
@@ -603,8 +599,8 @@
*---------------------------------------------------------------------------*)
fun alpha_ex_unroll (xlist, tm) =
- let val (qvars,body) = S.strip_exists tm
- val vlist = #2(S.strip_comb (S.rhs body))
+ let val (qvars,body) = USyntax.strip_exists tm
+ val vlist = #2 (USyntax.strip_comb (USyntax.rhs body))
val plist = ListPair.zip (vlist, xlist)
val args = map (the o AList.lookup (op aconv) plist) qvars
handle Option => raise Fail "TFL.alpha_ex_unroll: no correspondence"
@@ -634,7 +630,7 @@
fun fail s = raise TFL_ERR "mk_case" s
fun mk{rows=[],...} = fail"no rows"
| mk{path=[], rows = [([], (thm, bindings))]} =
- R.IT_EXISTS (map tych_binding bindings) thm
+ Rules.IT_EXISTS (map tych_binding bindings) thm
| mk{path = u::rstp, rows as (p::_, _)::_} =
let val (pat_rectangle,rights) = ListPair.unzip rows
val col0 = map hd pat_rectangle
@@ -651,8 +647,8 @@
case (ty_info ty_name)
of NONE => fail("Not a known datatype: "^ty_name)
| SOME{constructors,nchotomy} =>
- let val thm' = R.ISPEC (tych u) nchotomy
- val disjuncts = S.strip_disj (concl thm')
+ let val thm' = Rules.ISPEC (tych u) nchotomy
+ val disjuncts = USyntax.strip_disj (concl thm')
val subproblems = divide(constructors, rows)
val groups = map #group subproblems
and new_formals = map #new_formals subproblems
@@ -660,17 +656,17 @@
(new_formals, disjuncts)
val constraints = map #1 existentials
val vexl = map #2 existentials
- fun expnd tm (pats,(th,b)) = (pats,(R.SUBS[R.ASSUME(tych tm)]th,b))
+ fun expnd tm (pats,(th,b)) = (pats, (Rules.SUBS [Rules.ASSUME (tych tm)] th, b))
val news = map (fn (nf,rows,c) => {path = nf@rstp,
rows = map (expnd c) rows})
- (U.zip3 new_formals groups constraints)
+ (Utils.zip3 new_formals groups constraints)
val recursive_thms = map mk news
val build_exists = Library.foldr
(fn((x,t), th) =>
- R.CHOOSE (tych x, R.ASSUME (tych t)) th)
+ Rules.CHOOSE (tych x, Rules.ASSUME (tych t)) th)
val thms' = ListPair.map build_exists (vexl, recursive_thms)
- val same_concls = R.EVEN_ORS thms'
- in R.DISJ_CASESL thm' same_concls
+ val same_concls = Rules.EVEN_ORS thms'
+ in Rules.DISJ_CASESL thm' same_concls
end
end end
in mk
@@ -688,14 +684,14 @@
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))
- val th0 = R.ASSUME (tych a_eq_v)
+ val ex_th0 = Rules.EXISTS (tych (USyntax.mk_exists{Bvar=v,Body=a_eq_v}), tych a)
+ (Rules.REFL (tych a))
+ val th0 = Rules.ASSUME (tych a_eq_v)
val rows = map (fn x => ([x], (th0,[]))) pats
in
- R.GEN (tych a)
- (R.RIGHT_ASSOC
- (R.CHOOSE(tych v, ex_th0)
+ Rules.GEN (tych a)
+ (Rules.RIGHT_ASSOC
+ (Rules.CHOOSE(tych v, ex_th0)
(mk_case ty_info (vname::aname::names)
thy {path=[v], rows=rows})))
end end;
@@ -712,57 +708,57 @@
*---------------------------------------------------------------------------*)
(*
local infix 5 ==>
- fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2}
+ fun (tm1 ==> tm2) = USyntax.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 = is_some (S.find_term (curry (op aconv) f) tm)
+ let val globals = USyntax.free_vars_lr pat
+ fun nested tm = is_some (USyntax.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
+ let val (cntxt,R_y_pat) = USyntax.strip_imp(#2(USyntax.strip_forall tm))
+ val (R,y,_) = USyntax.dest_relation R_y_pat
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 (curry (op aconv) P) lvs) handle U.ERR _ => lvs
- in (S.list_mk_forall(locals,imp), (tm,locals)) end
+ val imp = USyntax.list_mk_conj cntxt ==> P_y
+ val lvs = gen_rems (op aconv) (USyntax.free_vars_lr imp, globals)
+ val locals = #2(Utils.pluck (curry (op aconv) P) lvs) handle Utils.ERR _ => lvs
+ in (USyntax.list_mk_forall(locals,imp), (tm,locals)) end
end
in case TCs
- of [] => (S.list_mk_forall(globals, P$pat), [])
+ of [] => (USyntax.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
- in (S.list_mk_forall(globals,ind_clause), TCs_locals)
+ val ind_clause = USyntax.list_mk_conj ihs ==> P$pat
+ in (USyntax.list_mk_forall(globals,ind_clause), TCs_locals)
end
end
end;
*)
local infix 5 ==>
- fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2}
+ fun (tm1 ==> tm2) = USyntax.mk_imp{ant = tm1, conseq = tm2}
in
fun build_ih f (P,SV) (pat,TCs) =
- let val pat_vars = S.free_vars_lr pat
+ let val pat_vars = USyntax.free_vars_lr pat
val globals = pat_vars@SV
- fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
+ fun nested tm = is_some (USyntax.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
+ let val (cntxt,R_y_pat) = USyntax.strip_imp(#2(USyntax.strip_forall tm))
+ val (R,y,_) = USyntax.dest_relation R_y_pat
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 = subtract (op aconv) globals (S.free_vars_lr imp)
- val locals = #2(U.pluck (curry (op aconv) P) lvs) handle U.ERR _ => lvs
- in (S.list_mk_forall(locals,imp), (tm,locals)) end
+ val imp = USyntax.list_mk_conj cntxt ==> P_y
+ val lvs = subtract (op aconv) globals (USyntax.free_vars_lr imp)
+ val locals = #2(Utils.pluck (curry (op aconv) P) lvs) handle Utils.ERR _ => lvs
+ in (USyntax.list_mk_forall(locals,imp), (tm,locals)) end
end
in case TCs
- of [] => (S.list_mk_forall(pat_vars, P$pat), [])
+ of [] => (USyntax.list_mk_forall(pat_vars, P$pat), [])
| _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs)
- val ind_clause = S.list_mk_conj ihs ==> P$pat
- in (S.list_mk_forall(pat_vars,ind_clause), TCs_locals)
+ val ind_clause = USyntax.list_mk_conj ihs ==> P$pat
+ in (USyntax.list_mk_forall(pat_vars,ind_clause), TCs_locals)
end
end
end;
@@ -776,29 +772,29 @@
*---------------------------------------------------------------------------*)
fun prove_case f thy (tm,TCs_locals,thm) =
let val tych = Thry.typecheck thy
- val antc = tych(#ant(S.dest_imp tm))
- val thm' = R.SPEC_ALL thm
- 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)))))
+ val antc = tych(#ant(USyntax.dest_imp tm))
+ val thm' = Rules.SPEC_ALL thm
+ fun nested tm = is_some (USyntax.find_term (curry (op aconv) f) tm)
+ fun get_cntxt TC = tych(#ant(USyntax.dest_imp(#2(USyntax.strip_forall(concl TC)))))
fun mk_ih ((TC,locals),th2,nested) =
- R.GENL (map tych locals)
- (if nested then R.DISCH (get_cntxt TC) th2 handle U.ERR _ => th2
- else if S.is_imp (concl TC) then R.IMP_TRANS TC th2
- else R.MP th2 TC)
+ Rules.GENL (map tych locals)
+ (if nested then Rules.DISCH (get_cntxt TC) th2 handle Utils.ERR _ => th2
+ else if USyntax.is_imp (concl TC) then Rules.IMP_TRANS TC th2
+ else Rules.MP th2 TC)
in
- R.DISCH antc
- (if S.is_imp(concl thm') (* recursive calls in this clause *)
- then let val th1 = R.ASSUME antc
+ Rules.DISCH antc
+ (if USyntax.is_imp(concl thm') (* recursive calls in this clause *)
+ then let val th1 = Rules.ASSUME antc
val TCs = map #1 TCs_locals
- val ylist = map (#2 o S.dest_relation o #2 o S.strip_imp o
- #2 o S.strip_forall) TCs
- val TClist = map (fn(TC,lvs) => (R.SPEC_ALL(R.ASSUME(tych TC)),lvs))
+ val ylist = map (#2 o USyntax.dest_relation o #2 o USyntax.strip_imp o
+ #2 o USyntax.strip_forall) TCs
+ val TClist = map (fn(TC,lvs) => (Rules.SPEC_ALL(Rules.ASSUME(tych TC)),lvs))
TCs_locals
- val th2list = map (U.C R.SPEC th1 o tych) ylist
+ val th2list = map (Utils.C Rules.SPEC th1 o tych) ylist
val nlist = map nested TCs
- val triples = U.zip3 TClist th2list nlist
+ val triples = Utils.zip3 TClist th2list nlist
val Pylist = map mk_ih triples
- in R.MP thm' (R.LIST_CONJ Pylist) end
+ in Rules.MP thm' (Rules.LIST_CONJ Pylist) end
else thm')
end;
@@ -812,12 +808,12 @@
*---------------------------------------------------------------------------*)
fun LEFT_ABS_VSTRUCT tych thm =
let fun CHOOSER v (tm,thm) =
- let val ex_tm = S.mk_exists{Bvar=v,Body=tm}
- in (ex_tm, R.CHOOSE(tych v, R.ASSUME (tych ex_tm)) thm)
+ let val ex_tm = USyntax.mk_exists{Bvar=v,Body=tm}
+ in (ex_tm, Rules.CHOOSE(tych v, Rules.ASSUME (tych ex_tm)) thm)
end
- val [veq] = filter (can S.dest_eq) (#1 (R.dest_thm thm))
- val {lhs,rhs} = S.dest_eq veq
- val L = S.free_vars_lr rhs
+ val [veq] = filter (can USyntax.dest_eq) (#1 (Rules.dest_thm thm))
+ val {lhs,rhs} = USyntax.dest_eq veq
+ val L = USyntax.free_vars_lr rhs
in #2 (fold_rev CHOOSER L (veq,thm)) end;
@@ -830,39 +826,39 @@
*---------------------------------------------------------------------------*)
fun mk_induction thy {fconst, R, SV, pat_TCs_list} =
let val tych = Thry.typecheck thy
- val Sinduction = R.UNDISCH (R.ISPEC (tych R) Thms.WF_INDUCTION_THM)
+ val Sinduction = Rules.UNDISCH (Rules.ISPEC (tych R) Thms.WF_INDUCTION_THM)
val (pats,TCsl) = ListPair.unzip pat_TCs_list
val case_thm = complete_cases thy pats
val domain = (type_of o hd) pats
val Pname = Name.variant (List.foldr (Library.foldr OldTerm.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 Sinduct = Rules.SPEC (tych P) Sinduction
+ val Sinduct_assumf = USyntax.rand ((#ant o USyntax.dest_imp o concl) Sinduct)
val Rassums_TCl' = map (build_ih fconst (P,SV)) pat_TCs_list
val (Rassums,TCl') = ListPair.unzip Rassums_TCl'
- val Rinduct_assum = R.ASSUME (tych (S.list_mk_conj Rassums))
+ val Rinduct_assum = Rules.ASSUME (tych (USyntax.list_mk_conj Rassums))
val cases = map (fn pat => Term.betapply (Sinduct_assumf, pat)) pats
- val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum)
+ val tasks = Utils.zip3 cases TCl' (Rules.CONJUNCTS Rinduct_assum)
val proved_cases = map (prove_case fconst thy) tasks
val v = Free (Name.variant (List.foldr OldTerm.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')
+ val substs = map (Rules.SYM o Rules.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
+ val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS[th]th')
(substs, proved_cases)
val abs_cases = map (LEFT_ABS_VSTRUCT tych) proved_cases1
- 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[Pname]) (S.strip_prod_type Parg_ty)
- val dc' = fold_rev (R.GEN o tych) vars
- (R.SPEC (tych(S.mk_vstruct Parg_ty vars)) dc)
+ val dant = Rules.GEN vtyped (Rules.DISJ_CASESL (Rules.ISPEC vtyped case_thm) abs_cases)
+ val dc = Rules.MP Sinduct dant
+ val Parg_ty = type_of(#Bvar(USyntax.dest_forall(concl dc)))
+ val vars = map (gvvariant[Pname]) (USyntax.strip_prod_type Parg_ty)
+ val dc' = fold_rev (Rules.GEN o tych) vars
+ (Rules.SPEC (tych(USyntax.mk_vstruct Parg_ty vars)) dc)
in
- R.GEN (tych P) (R.DISCH (tych(concl Rinduct_assum)) dc')
+ Rules.GEN (tych P) (Rules.DISCH (tych(concl Rinduct_assum)) dc')
end
-handle U.ERR _ => raise TFL_ERR "mk_induction" "failed derivation";
+handle Utils.ERR _ => raise TFL_ERR "mk_induction" "failed derivation";
@@ -876,15 +872,15 @@
fun simplify_induction thy hth ind =
let val tych = Thry.typecheck thy
- val (asl,_) = R.dest_thm ind
- val (_,tc_eq_tc') = R.dest_thm hth
- val tc = S.lhs tc_eq_tc'
+ val (asl,_) = Rules.dest_thm ind
+ val (_,tc_eq_tc') = Rules.dest_thm hth
+ val tc = USyntax.lhs tc_eq_tc'
fun loop [] = ind
| loop (asm::rst) =
if (can (Thry.match_term thy asm) tc)
- then R.UNDISCH
- (R.MATCH_MP
- (R.MATCH_MP Thms.simp_thm (R.DISCH (tych asm) ind))
+ then Rules.UNDISCH
+ (Rules.MATCH_MP
+ (Rules.MATCH_MP Thms.simp_thm (Rules.DISCH (tych asm) ind))
hth)
else loop rst
in loop asl
@@ -896,7 +892,7 @@
* assumption to the theorem.
*---------------------------------------------------------------------------*)
fun elim_tc tcthm (rule,induction) =
- (R.MP rule tcthm, R.PROVE_HYP tcthm induction)
+ (Rules.MP rule tcthm, Rules.PROVE_HYP tcthm induction)
fun trace_thms s L =
@@ -911,17 +907,17 @@
fun postprocess strict {wf_tac, terminator, simplifier} theory {rules,induction,TCs} =
let val tych = Thry.typecheck theory
- val prove = R.prove strict;
+ val prove = Rules.prove strict;
(*---------------------------------------------------------------------
* Attempt to eliminate WF condition. It's the only assumption of rules
*---------------------------------------------------------------------*)
val (rules1,induction1) =
let val thm = prove(tych(HOLogic.mk_Trueprop
- (hd(#1(R.dest_thm rules)))),
+ (hd(#1(Rules.dest_thm rules)))),
wf_tac)
- in (R.PROVE_HYP thm rules, R.PROVE_HYP thm induction)
- end handle U.ERR _ => (rules,induction);
+ in (Rules.PROVE_HYP thm rules, Rules.PROVE_HYP thm induction)
+ end handle Utils.ERR _ => (rules,induction);
(*----------------------------------------------------------------------
* The termination condition (tc) is simplified to |- tc = tc' (there
@@ -938,14 +934,14 @@
val tc_eq = simplifier tc1
val _ = trace_thms "result: " [tc_eq]
in
- elim_tc (R.MATCH_MP Thms.eqT tc_eq) (r,ind)
- handle U.ERR _ =>
- (elim_tc (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
- (prove(tych(HOLogic.mk_Trueprop(S.rhs(concl tc_eq))),
+ elim_tc (Rules.MATCH_MP Thms.eqT tc_eq) (r,ind)
+ handle Utils.ERR _ =>
+ (elim_tc (Rules.MATCH_MP(Rules.MATCH_MP Thms.rev_eq_mp tc_eq)
+ (prove(tych(HOLogic.mk_Trueprop(USyntax.rhs(concl tc_eq))),
terminator)))
(r,ind)
- handle U.ERR _ =>
- (R.UNDISCH(R.MATCH_MP (R.MATCH_MP Thms.simp_thm r) tc_eq),
+ handle Utils.ERR _ =>
+ (Rules.UNDISCH(Rules.MATCH_MP (Rules.MATCH_MP Thms.simp_thm r) tc_eq),
simplify_induction theory tc_eq ind))
end
@@ -963,35 +959,35 @@
* 3. return |- tc = tc'
*---------------------------------------------------------------------*)
fun simplify_nested_tc tc =
- let val tc_eq = simplifier (tych (#2 (S.strip_forall tc)))
+ let val tc_eq = simplifier (tych (#2 (USyntax.strip_forall tc)))
in
- R.GEN_ALL
- (R.MATCH_MP Thms.eqT tc_eq
- handle U.ERR _ =>
- (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
- (prove(tych(HOLogic.mk_Trueprop (S.rhs(concl tc_eq))),
+ Rules.GEN_ALL
+ (Rules.MATCH_MP Thms.eqT tc_eq
+ handle Utils.ERR _ =>
+ (Rules.MATCH_MP(Rules.MATCH_MP Thms.rev_eq_mp tc_eq)
+ (prove(tych(HOLogic.mk_Trueprop (USyntax.rhs(concl tc_eq))),
terminator))
- handle U.ERR _ => tc_eq))
+ handle Utils.ERR _ => tc_eq))
end
(*-------------------------------------------------------------------
* Attempt to simplify the termination conditions in each rule and
* in the induction theorem.
*-------------------------------------------------------------------*)
- fun strip_imp tm = if S.is_neg tm then ([],tm) else S.strip_imp tm
+ fun strip_imp tm = if USyntax.is_neg tm then ([],tm) else USyntax.strip_imp tm
fun loop ([],extras,R,ind) = (rev R, ind, extras)
| loop ((r,ftcs)::rst, nthms, R, ind) =
let val tcs = #1(strip_imp (concl r))
val extra_tcs = subtract (op aconv) tcs ftcs
val extra_tc_thms = map simplify_nested_tc extra_tcs
val (r1,ind1) = fold simplify_tc tcs (r,ind)
- val r2 = R.FILTER_DISCH_ALL(not o S.is_WFR) r1
+ val r2 = Rules.FILTER_DISCH_ALL(not o USyntax.is_WFR) r1
in loop(rst, nthms@extra_tc_thms, r2::R, ind1)
end
- val rules_tcs = ListPair.zip (R.CONJUNCTS rules1, TCs)
+ val rules_tcs = ListPair.zip (Rules.CONJUNCTS rules1, TCs)
val (rules2,ind2,extras) = loop(rules_tcs,[],[],induction1)
in
- {induction = ind2, rules = R.LIST_CONJ rules2, nested_tcs = extras}
+ {induction = ind2, rules = Rules.LIST_CONJ rules2, nested_tcs = extras}
end;
--- a/src/Tools/eqsubst.ML Wed Dec 15 17:14:44 2010 +0100
+++ b/src/Tools/eqsubst.ML Wed Dec 15 17:43:22 2010 +0100
@@ -119,11 +119,8 @@
end;
-structure EqSubst
-: EQSUBST
-= struct
-
-structure Z = Zipper;
+structure EqSubst: EQSUBST =
+struct
(* changes object "=" to meta "==" which prepares a given rewrite rule *)
fun prep_meta_eq ctxt =
@@ -196,11 +193,11 @@
abstracted out) for use in rewriting with RWInst.rw *)
fun prep_zipper_match z =
let
- val t = Z.trm z
- val c = Z.ctxt z
- val Ts = Z.C.nty_ctxt c
+ val t = Zipper.trm z
+ val c = Zipper.ctxt z
+ val Ts = Zipper.C.nty_ctxt c
val (FakeTs', Ts', t') = fakefree_badbounds Ts t
- val absterm = mk_foo_match (Z.C.apply c) Ts' t'
+ val absterm = mk_foo_match (Zipper.C.apply c) Ts' t'
in
(t', (FakeTs', Ts', absterm))
end;
@@ -291,7 +288,7 @@
(* Avoid considering replacing terms which have a var at the head as
they always succeed trivially, and uninterestingly. *)
fun valid_match_start z =
- (case bot_left_leaf_of (Z.trm z) of
+ (case bot_left_leaf_of (Zipper.trm z) of
Var _ => false
| _ => true);
@@ -302,33 +299,33 @@
fun search_lr_valid validf =
let
fun sf_valid_td_lr z =
- let val here = if validf z then [Z.Here z] else [] in
- case Z.trm z
- of _ $ _ => [Z.LookIn (Z.move_down_left z)]
+ let val here = if validf z then [Zipper.Here z] else [] in
+ case Zipper.trm z
+ of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z)]
@ here
- @ [Z.LookIn (Z.move_down_right z)]
- | Abs _ => here @ [Z.LookIn (Z.move_down_abs z)]
+ @ [Zipper.LookIn (Zipper.move_down_right z)]
+ | Abs _ => here @ [Zipper.LookIn (Zipper.move_down_abs z)]
| _ => here
end;
- in Z.lzy_search sf_valid_td_lr end;
+ in Zipper.lzy_search sf_valid_td_lr end;
(* search from bottom to top, left to right *)
fun search_bt_valid validf =
let
fun sf_valid_td_lr z =
- let val here = if validf z then [Z.Here z] else [] in
- case Z.trm z
- of _ $ _ => [Z.LookIn (Z.move_down_left z),
- Z.LookIn (Z.move_down_right z)] @ here
- | Abs _ => [Z.LookIn (Z.move_down_abs z)] @ here
+ let val here = if validf z then [Zipper.Here z] else [] in
+ case Zipper.trm z
+ of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z),
+ Zipper.LookIn (Zipper.move_down_right z)] @ here
+ | Abs _ => [Zipper.LookIn (Zipper.move_down_abs z)] @ here
| _ => here
end;
- in Z.lzy_search sf_valid_td_lr end;
+ in Zipper.lzy_search sf_valid_td_lr end;
fun searchf_unify_gen f (sgn, maxidx, z) lhs =
Seq.map (clean_unify_z sgn maxidx lhs)
- (Z.limit_apply f z);
+ (Zipper.limit_apply f z);
(* search all unifications *)
val searchf_lr_unify_all =
@@ -369,9 +366,9 @@
val conclterm = Logic.strip_imp_concl fixedbody;
val conclthm = trivify conclterm;
val maxidx = Thm.maxidx_of th;
- val ft = ((Z.move_down_right (* ==> *)
- o Z.move_down_left (* Trueprop *)
- o Z.mktop
+ val ft = ((Zipper.move_down_right (* ==> *)
+ o Zipper.move_down_left (* Trueprop *)
+ o Zipper.mktop
o Thm.prop_of) conclthm)
in
((cfvs, conclthm), (sgn, maxidx, ft))
@@ -487,8 +484,8 @@
val pth = trivify asmt;
val maxidx = Thm.maxidx_of th;
- val ft = ((Z.move_down_right (* trueprop *)
- o Z.mktop
+ val ft = ((Zipper.move_down_right (* trueprop *)
+ o Zipper.mktop
o Thm.prop_of) pth)
in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;