1.1 --- a/src/HOL/Import/replay.ML Wed Dec 15 15:01:34 2010 +0100
1.2 +++ b/src/HOL/Import/replay.ML Wed Dec 15 15:11:56 2010 +0100
1.3 @@ -2,11 +2,9 @@
1.4 Author: Sebastian Skalberg (TU Muenchen)
1.5 *)
1.6
1.7 -structure Replay =
1.8 +structure Replay = (* FIXME proper signature *)
1.9 struct
1.10
1.11 -structure P = ProofKernel
1.12 -
1.13 open ProofKernel
1.14 open ImportRecorder
1.15
1.16 @@ -17,12 +15,12 @@
1.17 fun replay_proof int_thms thyname thmname prf thy =
1.18 let
1.19 val _ = ImportRecorder.start_replay_proof thyname thmname
1.20 - fun rp (PRefl tm) thy = P.REFL tm thy
1.21 + fun rp (PRefl tm) thy = ProofKernel.REFL tm thy
1.22 | rp (PInstT(p,lambda)) thy =
1.23 let
1.24 val (thy',th) = rp' p thy
1.25 in
1.26 - P.INST_TYPE lambda th thy'
1.27 + ProofKernel.INST_TYPE lambda th thy'
1.28 end
1.29 | rp (PSubst(prfs,ctxt,prf)) thy =
1.30 let
1.31 @@ -34,52 +32,52 @@
1.32 end) prfs (thy,[])
1.33 val (thy'',th) = rp' prf thy'
1.34 in
1.35 - P.SUBST ths ctxt th thy''
1.36 + ProofKernel.SUBST ths ctxt th thy''
1.37 end
1.38 | rp (PAbs(prf,v)) thy =
1.39 let
1.40 val (thy',th) = rp' prf thy
1.41 in
1.42 - P.ABS v th thy'
1.43 + ProofKernel.ABS v th thy'
1.44 end
1.45 | rp (PDisch(prf,tm)) thy =
1.46 let
1.47 val (thy',th) = rp' prf thy
1.48 in
1.49 - P.DISCH tm th thy'
1.50 + ProofKernel.DISCH tm th thy'
1.51 end
1.52 | rp (PMp(prf1,prf2)) thy =
1.53 let
1.54 val (thy1,th1) = rp' prf1 thy
1.55 val (thy2,th2) = rp' prf2 thy1
1.56 in
1.57 - P.MP th1 th2 thy2
1.58 + ProofKernel.MP th1 th2 thy2
1.59 end
1.60 - | rp (PHyp tm) thy = P.ASSUME tm thy
1.61 + | rp (PHyp tm) thy = ProofKernel.ASSUME tm thy
1.62 | rp (PDef(seg,name,rhs)) thy =
1.63 - (case P.get_def seg name rhs thy of
1.64 + (case ProofKernel.get_def seg name rhs thy of
1.65 (thy',SOME res) => (thy',res)
1.66 | (thy',NONE) =>
1.67 if seg = thyname
1.68 - then P.new_definition seg name rhs thy'
1.69 + then ProofKernel.new_definition seg name rhs thy'
1.70 else raise ERR "replay_proof" ("Too late for term definition: "^seg^" != "^thyname))
1.71 - | rp (POracle(tg,asl,c)) thy = (*P.mk_oracle_thm tg (map be_contract asl,c)*) NY "ORACLE"
1.72 + | rp (POracle(tg,asl,c)) thy = (*ProofKernel.mk_oracle_thm tg (map be_contract asl,c)*) NY "ORACLE"
1.73 | rp (PSpec(prf,tm)) thy =
1.74 let
1.75 val (thy',th) = rp' prf thy
1.76 in
1.77 - P.SPEC tm th thy'
1.78 + ProofKernel.SPEC tm th thy'
1.79 end
1.80 | rp (PInst(prf,theta)) thy =
1.81 let
1.82 val (thy',th) = rp' prf thy
1.83 in
1.84 - P.INST theta th thy'
1.85 + ProofKernel.INST theta th thy'
1.86 end
1.87 | rp (PGen(prf,v)) thy =
1.88 let
1.89 val (thy',th) = rp' prf thy
1.90 - val p = P.GEN v th thy'
1.91 + val p = ProofKernel.GEN v th thy'
1.92 in
1.93 p
1.94 end
1.95 @@ -87,91 +85,91 @@
1.96 let
1.97 val (thy',th) = rp' prf thy
1.98 in
1.99 - P.GEN_ABS opt vl th thy'
1.100 + ProofKernel.GEN_ABS opt vl th thy'
1.101 end
1.102 | rp (PImpAS(prf1,prf2)) thy =
1.103 let
1.104 val (thy1,th1) = rp' prf1 thy
1.105 val (thy2,th2) = rp' prf2 thy1
1.106 in
1.107 - P.IMP_ANTISYM th1 th2 thy2
1.108 + ProofKernel.IMP_ANTISYM th1 th2 thy2
1.109 end
1.110 | rp (PSym prf) thy =
1.111 let
1.112 val (thy1,th) = rp' prf thy
1.113 in
1.114 - P.SYM th thy1
1.115 + ProofKernel.SYM th thy1
1.116 end
1.117 | rp (PTrans(prf1,prf2)) thy =
1.118 let
1.119 val (thy1,th1) = rp' prf1 thy
1.120 val (thy2,th2) = rp' prf2 thy1
1.121 in
1.122 - P.TRANS th1 th2 thy2
1.123 + ProofKernel.TRANS th1 th2 thy2
1.124 end
1.125 | rp (PComb(prf1,prf2)) thy =
1.126 let
1.127 val (thy1,th1) = rp' prf1 thy
1.128 val (thy2,th2) = rp' prf2 thy1
1.129 in
1.130 - P.COMB th1 th2 thy2
1.131 + ProofKernel.COMB th1 th2 thy2
1.132 end
1.133 | rp (PEqMp(prf1,prf2)) thy =
1.134 let
1.135 val (thy1,th1) = rp' prf1 thy
1.136 val (thy2,th2) = rp' prf2 thy1
1.137 in
1.138 - P.EQ_MP th1 th2 thy2
1.139 + ProofKernel.EQ_MP th1 th2 thy2
1.140 end
1.141 | rp (PEqImp prf) thy =
1.142 let
1.143 val (thy',th) = rp' prf thy
1.144 in
1.145 - P.EQ_IMP_RULE th thy'
1.146 + ProofKernel.EQ_IMP_RULE th thy'
1.147 end
1.148 | rp (PExists(prf,ex,wit)) thy =
1.149 let
1.150 val (thy',th) = rp' prf thy
1.151 in
1.152 - P.EXISTS ex wit th thy'
1.153 + ProofKernel.EXISTS ex wit th thy'
1.154 end
1.155 | rp (PChoose(v,prf1,prf2)) thy =
1.156 let
1.157 val (thy1,th1) = rp' prf1 thy
1.158 val (thy2,th2) = rp' prf2 thy1
1.159 in
1.160 - P.CHOOSE v th1 th2 thy2
1.161 + ProofKernel.CHOOSE v th1 th2 thy2
1.162 end
1.163 | rp (PConj(prf1,prf2)) thy =
1.164 let
1.165 val (thy1,th1) = rp' prf1 thy
1.166 val (thy2,th2) = rp' prf2 thy1
1.167 in
1.168 - P.CONJ th1 th2 thy2
1.169 + ProofKernel.CONJ th1 th2 thy2
1.170 end
1.171 | rp (PConjunct1 prf) thy =
1.172 let
1.173 val (thy',th) = rp' prf thy
1.174 in
1.175 - P.CONJUNCT1 th thy'
1.176 + ProofKernel.CONJUNCT1 th thy'
1.177 end
1.178 | rp (PConjunct2 prf) thy =
1.179 let
1.180 val (thy',th) = rp' prf thy
1.181 in
1.182 - P.CONJUNCT2 th thy'
1.183 + ProofKernel.CONJUNCT2 th thy'
1.184 end
1.185 | rp (PDisj1(prf,tm)) thy =
1.186 let
1.187 val (thy',th) = rp' prf thy
1.188 in
1.189 - P.DISJ1 th tm thy'
1.190 + ProofKernel.DISJ1 th tm thy'
1.191 end
1.192 | rp (PDisj2(prf,tm)) thy =
1.193 let
1.194 val (thy',th) = rp' prf thy
1.195 in
1.196 - P.DISJ2 tm th thy'
1.197 + ProofKernel.DISJ2 tm th thy'
1.198 end
1.199 | rp (PDisjCases(prf,prf1,prf2)) thy =
1.200 let
1.201 @@ -179,25 +177,25 @@
1.202 val (thy1,th1) = rp' prf1 thy'
1.203 val (thy2,th2) = rp' prf2 thy1
1.204 in
1.205 - P.DISJ_CASES th th1 th2 thy2
1.206 + ProofKernel.DISJ_CASES th th1 th2 thy2
1.207 end
1.208 | rp (PNotI prf) thy =
1.209 let
1.210 val (thy',th) = rp' prf thy
1.211 in
1.212 - P.NOT_INTRO th thy'
1.213 + ProofKernel.NOT_INTRO th thy'
1.214 end
1.215 | rp (PNotE prf) thy =
1.216 let
1.217 val (thy',th) = rp' prf thy
1.218 in
1.219 - P.NOT_ELIM th thy'
1.220 + ProofKernel.NOT_ELIM th thy'
1.221 end
1.222 | rp (PContr(prf,tm)) thy =
1.223 let
1.224 val (thy',th) = rp' prf thy
1.225 in
1.226 - P.CCONTR tm th thy'
1.227 + ProofKernel.CCONTR tm th thy'
1.228 end
1.229 | rp (PTmSpec _) _ = raise ERR "rp" "Shouldn't reach here (PTmSpec)"
1.230 | rp (PTyDef _) _ = raise ERR "rp" "Shouldn't reach here (PTyDef)"
1.231 @@ -226,7 +224,7 @@
1.232 | SOME th => (thy,th))
1.233 else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")
1.234 | NONE =>
1.235 - (case P.get_thm thyname' thmname thy of
1.236 + (case ProofKernel.get_thm thyname' thmname thy of
1.237 (thy',SOME res) => (thy',res)
1.238 | (thy',NONE) =>
1.239 if thyname' = thyname
1.240 @@ -242,31 +240,31 @@
1.241 PTmSpec _ => (thy',th)
1.242 | PTyDef _ => (thy',th)
1.243 | PTyIntro _ => (thy',th)
1.244 - | _ => P.store_thm thyname' thmname th thy'
1.245 + | _ => ProofKernel.store_thm thyname' thmname th thy'
1.246 end
1.247 else raise ERR "replay_proof" ("Library " ^ thyname' ^ " should be built before " ^ thyname ^ " (" ^ thmname ^ ")")))
1.248 | NONE => raise ERR "rp'.PDisk" "Not enough information")
1.249 | PAxm(name,c) =>
1.250 - (case P.get_axiom thyname name thy of
1.251 + (case ProofKernel.get_axiom thyname name thy of
1.252 (thy',SOME res) => (thy',res)
1.253 - | (thy',NONE) => P.new_axiom name c thy')
1.254 + | (thy',NONE) => ProofKernel.new_axiom name c thy')
1.255 | PTmSpec(seg,names,prf') =>
1.256 let
1.257 val (thy',th) = rp' prf' thy
1.258 in
1.259 - P.new_specification seg thmname names th thy'
1.260 + ProofKernel.new_specification seg thmname names th thy'
1.261 end
1.262 | PTyDef(seg,name,prf') =>
1.263 let
1.264 val (thy',th) = rp' prf' thy
1.265 in
1.266 - P.new_type_definition seg thmname name th thy'
1.267 + ProofKernel.new_type_definition seg thmname name th thy'
1.268 end
1.269 | PTyIntro(seg,name,abs_name,rep_name,P,t,prf') =>
1.270 let
1.271 val (thy',th) = rp' prf' thy
1.272 in
1.273 - P.type_introduction seg thmname name abs_name rep_name (P,t) th thy'
1.274 + ProofKernel.type_introduction seg thmname name abs_name rep_name (P,t) th thy'
1.275 end
1.276 | _ => rp pc thy
1.277 end
1.278 @@ -282,7 +280,7 @@
1.279 fun setup_int_thms thyname thy =
1.280 let
1.281 val fname =
1.282 - case P.get_proof_dir thyname thy of
1.283 + case ProofKernel.get_proof_dir thyname thy of
1.284 SOME p => OS.Path.joinDirFile {dir=p,file=OS.Path.joinBaseExt{base = "facts",ext=SOME "lst"}}
1.285 | NONE => error "Cannot find proof files"
1.286 val is = TextIO.openIn fname
1.287 @@ -291,7 +289,7 @@
1.288 fun get_facts facts =
1.289 case TextIO.inputLine is of
1.290 NONE => (case facts of
1.291 - i::facts => (the (Int.fromString i),map P.protect_factname (rev facts))
1.292 + i::facts => (the (Int.fromString i),map ProofKernel.protect_factname (rev facts))
1.293 | _ => raise ERR "replay_thm" "Bad facts.lst file")
1.294 | SOME fact => get_facts ((String.substring(fact,0,String.size fact -1 ))::facts)
1.295 in
1.296 @@ -349,9 +347,9 @@
1.297 | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =
1.298 add_hol4_type_mapping thyname tycname true fulltyname thy
1.299 | delta (Indexed_theorem (i, th)) thy =
1.300 - (Array.update (int_thms,i-1,SOME (P.to_hol_thm (th_of thy th))); thy)
1.301 - | delta (Protect_varname (s,t)) thy = (P.replay_protect_varname s t; thy)
1.302 - | delta (Dump s) thy = P.replay_add_dump s thy
1.303 + (Array.update (int_thms,i-1,SOME (ProofKernel.to_hol_thm (th_of thy th))); thy)
1.304 + | delta (Protect_varname (s,t)) thy = (ProofKernel.replay_protect_varname s t; thy)
1.305 + | delta (Dump s) thy = ProofKernel.replay_add_dump s thy
1.306 in
1.307 rps
1.308 end
2.1 --- a/src/HOL/Tools/TFL/dcterm.ML Wed Dec 15 15:01:34 2010 +0100
2.2 +++ b/src/HOL/Tools/TFL/dcterm.ML Wed Dec 15 15:11:56 2010 +0100
2.3 @@ -49,9 +49,7 @@
2.4 structure Dcterm: DCTERM =
2.5 struct
2.6
2.7 -structure U = Utils;
2.8 -
2.9 -fun ERR func mesg = U.ERR {module = "Dcterm", func = func, mesg = mesg};
2.10 +fun ERR func mesg = Utils.ERR {module = "Dcterm", func = func, mesg = mesg};
2.11
2.12
2.13 fun dest_comb t = Thm.dest_comb t
2.14 @@ -110,19 +108,19 @@
2.15 fun dest_monop expected tm =
2.16 let
2.17 fun err () = raise ERR "dest_monop" ("Not a(n) " ^ quote expected);
2.18 - val (c, N) = dest_comb tm handle U.ERR _ => err ();
2.19 - val name = #Name (dest_const c handle U.ERR _ => err ());
2.20 + val (c, N) = dest_comb tm handle Utils.ERR _ => err ();
2.21 + val name = #Name (dest_const c handle Utils.ERR _ => err ());
2.22 in if name = expected then N else err () end;
2.23
2.24 fun dest_binop expected tm =
2.25 let
2.26 fun err () = raise ERR "dest_binop" ("Not a(n) " ^ quote expected);
2.27 - val (M, N) = dest_comb tm handle U.ERR _ => err ()
2.28 - in (dest_monop expected M, N) handle U.ERR _ => err () end;
2.29 + val (M, N) = dest_comb tm handle Utils.ERR _ => err ()
2.30 + in (dest_monop expected M, N) handle Utils.ERR _ => err () end;
2.31
2.32 fun dest_binder expected tm =
2.33 dest_abs NONE (dest_monop expected tm)
2.34 - handle U.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected);
2.35 + handle Utils.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected);
2.36
2.37
2.38 val dest_neg = dest_monop @{const_name Not}
2.39 @@ -151,7 +149,7 @@
2.40 (*---------------------------------------------------------------------------
2.41 * Iterated creation.
2.42 *---------------------------------------------------------------------------*)
2.43 -val list_mk_disj = U.end_itlist (fn d1 => fn tm => mk_disj (d1, tm));
2.44 +val list_mk_disj = Utils.end_itlist (fn d1 => fn tm => mk_disj (d1, tm));
2.45
2.46 (*---------------------------------------------------------------------------
2.47 * Iterated destruction. (To the "right" in a term.)
2.48 @@ -160,7 +158,7 @@
2.49 let fun dest (p as (ctm,accum)) =
2.50 let val (M,N) = break ctm
2.51 in dest (N, M::accum)
2.52 - end handle U.ERR _ => p
2.53 + end handle Utils.ERR _ => p
2.54 in dest (tm,[])
2.55 end;
2.56
2.57 @@ -190,7 +188,7 @@
2.58 handle TYPE (msg, _, _) => raise ERR "mk_prop" msg
2.59 | TERM (msg, _) => raise ERR "mk_prop" msg;
2.60
2.61 -fun drop_prop ctm = dest_monop @{const_name Trueprop} ctm handle U.ERR _ => ctm;
2.62 +fun drop_prop ctm = dest_monop @{const_name Trueprop} ctm handle Utils.ERR _ => ctm;
2.63
2.64
2.65 end;
3.1 --- a/src/HOL/Tools/TFL/post.ML Wed Dec 15 15:01:34 2010 +0100
3.2 +++ b/src/HOL/Tools/TFL/post.ML Wed Dec 15 15:11:56 2010 +0100
3.3 @@ -18,8 +18,6 @@
3.4 structure Tfl: TFL =
3.5 struct
3.6
3.7 -structure S = USyntax
3.8 -
3.9 (* misc *)
3.10
3.11 (*---------------------------------------------------------------------------
3.12 @@ -53,16 +51,14 @@
3.13 * processing from the definition stage.
3.14 *---------------------------------------------------------------------------*)
3.15 local
3.16 -structure R = Rules
3.17 -structure U = Utils
3.18
3.19 (* The rest of these local definitions are for the tricky nested case *)
3.20 -val solved = not o can S.dest_eq o #2 o S.strip_forall o concl
3.21 +val solved = not o can USyntax.dest_eq o #2 o USyntax.strip_forall o concl
3.22
3.23 fun id_thm th =
3.24 - let val {lhs,rhs} = S.dest_eq (#2 (S.strip_forall (#2 (R.dest_thm th))));
3.25 + let val {lhs,rhs} = USyntax.dest_eq (#2 (USyntax.strip_forall (#2 (Rules.dest_thm th))));
3.26 in lhs aconv rhs end
3.27 - handle U.ERR _ => false;
3.28 + handle Utils.ERR _ => false;
3.29
3.30 val P_imp_P_eq_True = @{thm eqTrueI} RS eq_reflection;
3.31 fun mk_meta_eq r = case concl_of r of
3.32 @@ -76,16 +72,16 @@
3.33 fun join_assums th =
3.34 let val thy = Thm.theory_of_thm th
3.35 val tych = cterm_of thy
3.36 - val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th)))
3.37 - val cntxtl = (#1 o S.strip_imp) lhs (* cntxtl should = cntxtr *)
3.38 - val cntxtr = (#1 o S.strip_imp) rhs (* but union is solider *)
3.39 + val {lhs,rhs} = USyntax.dest_eq(#2 (USyntax.strip_forall (concl th)))
3.40 + val cntxtl = (#1 o USyntax.strip_imp) lhs (* cntxtl should = cntxtr *)
3.41 + val cntxtr = (#1 o USyntax.strip_imp) rhs (* but union is solider *)
3.42 val cntxt = union (op aconv) cntxtl cntxtr
3.43 in
3.44 - R.GEN_ALL
3.45 - (R.DISCH_ALL
3.46 - (rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th)))
3.47 + Rules.GEN_ALL
3.48 + (Rules.DISCH_ALL
3.49 + (rewrite (map (Rules.ASSUME o tych) cntxt) (Rules.SPEC_ALL th)))
3.50 end
3.51 - val gen_all = S.gen_all
3.52 + val gen_all = USyntax.gen_all
3.53 in
3.54 fun proof_stage strict cs ss wfs theory {f, R, rules, full_pats_TCs, TCs} =
3.55 let
3.56 @@ -117,7 +113,7 @@
3.57 in
3.58 {induction = induction',
3.59 rules = rules',
3.60 - tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl)
3.61 + tcs = map (gen_all o USyntax.rhs o #2 o USyntax.strip_forall o concl)
3.62 (simplified@stubborn)}
3.63 end
3.64 end;
3.65 @@ -144,8 +140,8 @@
3.66 val def = Thm.unvarify_global def0 RS meta_eq_to_obj_eq
3.67 val {rules,rows,TCs,full_pats_TCs} =
3.68 Prim.post_definition congs (thy, (def,pats))
3.69 - val {lhs=f,rhs} = S.dest_eq (concl def)
3.70 - val (_,[R,_]) = S.strip_comb rhs
3.71 + val {lhs=f,rhs} = USyntax.dest_eq (concl def)
3.72 + val (_,[R,_]) = USyntax.strip_comb rhs
3.73 val dummy = Prim.trace_thms "congs =" congs
3.74 (*the next step has caused simplifier looping in some cases*)
3.75 val {induction, rules, tcs} =
3.76 @@ -154,12 +150,12 @@
3.77 full_pats_TCs = full_pats_TCs,
3.78 TCs = TCs}
3.79 val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm)
3.80 - (R.CONJUNCTS rules)
3.81 + (Rules.CONJUNCTS rules)
3.82 in {induct = meta_outer ctxt (Object_Logic.rulify_no_asm (induction RS spec')),
3.83 rules = ListPair.zip(rules', rows),
3.84 tcs = (termination_goals rules') @ tcs}
3.85 end
3.86 - handle U.ERR {mesg,func,module} =>
3.87 + handle Utils.ERR {mesg,func,module} =>
3.88 error (mesg ^
3.89 "\n (In TFL function " ^ module ^ "." ^ func ^ ")");
3.90
3.91 @@ -217,7 +213,7 @@
3.92 fun define strict thy cs ss congs wfs fid R seqs =
3.93 define_i strict thy cs ss congs wfs fid
3.94 (Syntax.read_term_global thy R) (map (Syntax.read_term_global thy) seqs)
3.95 - handle U.ERR {mesg,...} => error mesg;
3.96 + handle Utils.ERR {mesg,...} => error mesg;
3.97
3.98
3.99 (*---------------------------------------------------------------------------
3.100 @@ -227,11 +223,11 @@
3.101 *---------------------------------------------------------------------------*)
3.102
3.103 fun func_of_cond_eqn tm =
3.104 - #1 (S.strip_comb (#lhs (S.dest_eq (#2 (S.strip_forall (#2 (S.strip_imp tm)))))));
3.105 + #1 (USyntax.strip_comb (#lhs (USyntax.dest_eq (#2 (USyntax.strip_forall (#2 (USyntax.strip_imp tm)))))));
3.106
3.107 fun defer_i thy congs fid eqs =
3.108 let val {rules,R,theory,full_pats_TCs,SV,...} = Prim.lazyR_def thy fid congs eqs
3.109 - val f = func_of_cond_eqn (concl (R.CONJUNCT1 rules handle U.ERR _ => rules));
3.110 + val f = func_of_cond_eqn (concl (Rules.CONJUNCT1 rules handle Utils.ERR _ => rules));
3.111 val dummy = writeln "Proving induction theorem ...";
3.112 val induction = Prim.mk_induction theory
3.113 {fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs}
3.114 @@ -243,7 +239,7 @@
3.115
3.116 fun defer thy congs fid seqs =
3.117 defer_i thy congs fid (map (Syntax.read_term_global thy) seqs)
3.118 - handle U.ERR {mesg,...} => error mesg;
3.119 + handle Utils.ERR {mesg,...} => error mesg;
3.120 end;
3.121
3.122 end;
4.1 --- a/src/HOL/Tools/TFL/rules.ML Wed Dec 15 15:01:34 2010 +0100
4.2 +++ b/src/HOL/Tools/TFL/rules.ML Wed Dec 15 15:11:56 2010 +0100
4.3 @@ -57,16 +57,11 @@
4.4 structure Rules: RULES =
4.5 struct
4.6
4.7 -structure S = USyntax;
4.8 -structure U = Utils;
4.9 -structure D = Dcterm;
4.10 +fun RULES_ERR func mesg = Utils.ERR {module = "Rules", func = func, mesg = mesg};
4.11
4.12
4.13 -fun RULES_ERR func mesg = U.ERR {module = "Rules", func = func, mesg = mesg};
4.14 -
4.15 -
4.16 -fun cconcl thm = D.drop_prop (#prop (Thm.crep_thm thm));
4.17 -fun chyps thm = map D.drop_prop (#hyps (Thm.crep_thm thm));
4.18 +fun cconcl thm = Dcterm.drop_prop (#prop (Thm.crep_thm thm));
4.19 +fun chyps thm = map Dcterm.drop_prop (#hyps (Thm.crep_thm thm));
4.20
4.21 fun dest_thm thm =
4.22 let val {prop,hyps,...} = Thm.rep_thm thm
4.23 @@ -95,7 +90,7 @@
4.24 handle THM (msg, _, _) => raise RULES_ERR "ALPHA" msg;
4.25
4.26 fun rbeta th =
4.27 - (case D.strip_comb (cconcl th) of
4.28 + (case Dcterm.strip_comb (cconcl th) of
4.29 (_, [l, r]) => Thm.transitive th (Thm.beta_conversion false r)
4.30 | _ => raise RULES_ERR "rbeta" "");
4.31
4.32 @@ -108,7 +103,7 @@
4.33 * "B" results in something that looks like "A --> B".
4.34 *---------------------------------------------------------------------------*)
4.35
4.36 -fun ASSUME ctm = Thm.assume (D.mk_prop ctm);
4.37 +fun ASSUME ctm = Thm.assume (Dcterm.mk_prop ctm);
4.38
4.39
4.40 (*---------------------------------------------------------------------------
4.41 @@ -119,7 +114,7 @@
4.42 handle THM (msg, _, _) => raise RULES_ERR "MP" msg;
4.43
4.44 (*forces the first argument to be a proposition if necessary*)
4.45 -fun DISCH tm thm = Thm.implies_intr (D.mk_prop tm) thm COMP impI
4.46 +fun DISCH tm thm = Thm.implies_intr (Dcterm.mk_prop tm) thm COMP impI
4.47 handle THM (msg, _, _) => raise RULES_ERR "DISCH" msg;
4.48
4.49 fun DISCH_ALL thm = fold_rev DISCH (#hyps (Thm.crep_thm thm)) thm;
4.50 @@ -131,9 +126,9 @@
4.51 end;
4.52
4.53 fun UNDISCH thm =
4.54 - let val tm = D.mk_prop (#1 (D.dest_imp (cconcl thm)))
4.55 + let val tm = Dcterm.mk_prop (#1 (Dcterm.dest_imp (cconcl thm)))
4.56 in Thm.implies_elim (thm RS mp) (ASSUME tm) end
4.57 - handle U.ERR _ => raise RULES_ERR "UNDISCH" ""
4.58 + handle Utils.ERR _ => raise RULES_ERR "UNDISCH" ""
4.59 | THM _ => raise RULES_ERR "UNDISCH" "";
4.60
4.61 fun PROVE_HYP ath bth = MP (DISCH (cconcl ath) bth) ath;
4.62 @@ -152,7 +147,7 @@
4.63 fun CONJUNCT2 thm = thm RS conjunct2
4.64 handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT2" msg;
4.65
4.66 -fun CONJUNCTS th = CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th) handle U.ERR _ => [th];
4.67 +fun CONJUNCTS th = CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th) handle Utils.ERR _ => [th];
4.68
4.69 fun LIST_CONJ [] = raise RULES_ERR "LIST_CONJ" "empty list"
4.70 | LIST_CONJ [th] = th
4.71 @@ -168,7 +163,7 @@
4.72 val [P,Q] = OldTerm.term_vars prop
4.73 val disj1 = Thm.forall_intr (Thm.cterm_of thy Q) disjI1
4.74 in
4.75 -fun DISJ1 thm tm = thm RS (Thm.forall_elim (D.drop_prop tm) disj1)
4.76 +fun DISJ1 thm tm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj1)
4.77 handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg;
4.78 end;
4.79
4.80 @@ -177,7 +172,7 @@
4.81 val [P,Q] = OldTerm.term_vars prop
4.82 val disj2 = Thm.forall_intr (Thm.cterm_of thy P) disjI2
4.83 in
4.84 -fun DISJ2 tm thm = thm RS (Thm.forall_elim (D.drop_prop tm) disj2)
4.85 +fun DISJ2 tm thm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj2)
4.86 handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg;
4.87 end;
4.88
4.89 @@ -195,10 +190,10 @@
4.90 let fun blue ldisjs [] _ = []
4.91 | blue ldisjs (th::rst) rdisjs =
4.92 let val tail = tl rdisjs
4.93 - val rdisj_tl = D.list_mk_disj tail
4.94 + val rdisj_tl = Dcterm.list_mk_disj tail
4.95 in fold_rev DISJ2 ldisjs (DISJ1 th rdisj_tl)
4.96 :: blue (ldisjs @ [cconcl th]) rst tail
4.97 - end handle U.ERR _ => [fold_rev DISJ2 ldisjs th]
4.98 + end handle Utils.ERR _ => [fold_rev DISJ2 ldisjs th]
4.99 in blue [] thms (map cconcl thms) end;
4.100
4.101
4.102 @@ -212,8 +207,8 @@
4.103
4.104 fun DISJ_CASES th1 th2 th3 =
4.105 let
4.106 - val c = D.drop_prop (cconcl th1);
4.107 - val (disj1, disj2) = D.dest_disj c;
4.108 + val c = Dcterm.drop_prop (cconcl th1);
4.109 + val (disj1, disj2) = Dcterm.dest_disj c;
4.110 val th2' = DISCH disj1 th2;
4.111 val th3' = DISCH disj2 th3;
4.112 in
4.113 @@ -253,12 +248,12 @@
4.114 fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t
4.115 aconv term_of atm)
4.116 (#hyps(rep_thm th))
4.117 - val tml = D.strip_disj c
4.118 + val tml = Dcterm.strip_disj c
4.119 fun DL th [] = raise RULES_ERR "DISJ_CASESL" "no cases"
4.120 | DL th [th1] = PROVE_HYP th th1
4.121 | DL th [th1,th2] = DISJ_CASES th th1 th2
4.122 | DL th (th1::rst) =
4.123 - let val tm = #2(D.dest_disj(D.drop_prop(cconcl th)))
4.124 + let val tm = #2 (Dcterm.dest_disj (Dcterm.drop_prop(cconcl th)))
4.125 in DISJ_CASES th th1 (DL (ASSUME tm) rst) end
4.126 in DL disjth (organize eq tml thl)
4.127 end;
4.128 @@ -279,7 +274,7 @@
4.129 in thm RS (Thm.forall_elim tm gspec') end
4.130 end;
4.131
4.132 -fun SPEC_ALL thm = fold SPEC (#1(D.strip_forall(cconcl thm))) thm;
4.133 +fun SPEC_ALL thm = fold SPEC (#1 (Dcterm.strip_forall(cconcl thm))) thm;
4.134
4.135 val ISPEC = SPEC
4.136 val ISPECL = fold ISPEC;
4.137 @@ -323,7 +318,7 @@
4.138
4.139
4.140 fun MATCH_MP th1 th2 =
4.141 - if (D.is_forall (D.drop_prop(cconcl th1)))
4.142 + if (Dcterm.is_forall (Dcterm.drop_prop(cconcl th1)))
4.143 then MATCH_MP (th1 RS spec) th2
4.144 else MP th1 th2;
4.145
4.146 @@ -345,8 +340,8 @@
4.147
4.148 fun CHOOSE (fvar, exth) fact =
4.149 let
4.150 - val lam = #2 (D.dest_comb (D.drop_prop (cconcl exth)))
4.151 - val redex = D.capply lam fvar
4.152 + val lam = #2 (Dcterm.dest_comb (Dcterm.drop_prop (cconcl exth)))
4.153 + val redex = Dcterm.capply lam fvar
4.154 val thy = Thm.theory_of_cterm redex
4.155 val t$u = Thm.term_of redex
4.156 val residue = Thm.cterm_of thy (Term.betapply (t, u))
4.157 @@ -364,7 +359,7 @@
4.158 val prop = Thm.prop_of thm
4.159 val P' = cterm_of thy P
4.160 val x' = cterm_of thy x
4.161 - val abstr = #2 (D.dest_comb template)
4.162 + val abstr = #2 (Dcterm.dest_comb template)
4.163 in
4.164 thm RS (cterm_instantiate[(P',abstr), (x',witness)] exI)
4.165 handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg
4.166 @@ -380,7 +375,7 @@
4.167 *---------------------------------------------------------------------------*)
4.168
4.169 fun EXISTL vlist th =
4.170 - fold_rev (fn v => fn thm => EXISTS(D.mk_exists(v,cconcl thm), v) thm)
4.171 + fold_rev (fn v => fn thm => EXISTS(Dcterm.mk_exists(v,cconcl thm), v) thm)
4.172 vlist th;
4.173
4.174
4.175 @@ -397,7 +392,7 @@
4.176 let val thy = Thm.theory_of_thm th
4.177 val tych = cterm_of thy
4.178 val blist' = map (pairself Thm.term_of) blist
4.179 - fun ex v M = cterm_of thy (S.mk_exists{Bvar=v,Body = M})
4.180 + fun ex v M = cterm_of thy (USyntax.mk_exists{Bvar=v,Body = M})
4.181
4.182 in
4.183 fold_rev (fn (b as (r1,r2)) => fn thm =>
4.184 @@ -443,7 +438,7 @@
4.185
4.186
4.187 (* Object language quantifier, i.e., "!" *)
4.188 -fun Forall v M = S.mk_forall{Bvar=v, Body=M};
4.189 +fun Forall v M = USyntax.mk_forall{Bvar=v, Body=M};
4.190
4.191
4.192 (* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *)
4.193 @@ -458,11 +453,11 @@
4.194 (Const (@{const_name Trueprop},_) $ lhs)
4.195 $ (Const (@{const_name Trueprop},_) $ rhs)) = {lhs=lhs, rhs=rhs}
4.196 | dest_equal(Const ("==",_) $ lhs $ rhs) = {lhs=lhs, rhs=rhs}
4.197 - | dest_equal tm = S.dest_eq tm;
4.198 + | dest_equal tm = USyntax.dest_eq tm;
4.199
4.200 fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm));
4.201
4.202 -fun dest_all used (Const("all",_) $ (a as Abs _)) = S.dest_abs used a
4.203 +fun dest_all used (Const("all",_) $ (a as Abs _)) = USyntax.dest_abs used a
4.204 | dest_all _ _ = raise RULES_ERR "dest_all" "not a !!";
4.205
4.206 val is_all = can (dest_all []);
4.207 @@ -505,13 +500,13 @@
4.208 of ([],_) => get (rst, n+1,L)
4.209 | (vlist,body) =>
4.210 let val eq = Logic.strip_imp_concl body
4.211 - val (f,args) = S.strip_comb (get_lhs eq)
4.212 - val (vstrl,_) = S.strip_abs f
4.213 + val (f,args) = USyntax.strip_comb (get_lhs eq)
4.214 + val (vstrl,_) = USyntax.strip_abs f
4.215 val names =
4.216 Name.variant_list (OldTerm.add_term_names(body, [])) (map (#1 o dest_Free) vstrl)
4.217 in get (rst, n+1, (names,n)::L) end
4.218 handle TERM _ => get (rst, n+1, L)
4.219 - | U.ERR _ => get (rst, n+1, L);
4.220 + | Utils.ERR _ => get (rst, n+1, L);
4.221
4.222 (* Note: Thm.rename_params_rule counts from 1, not 0 *)
4.223 fun rename thm =
4.224 @@ -529,7 +524,7 @@
4.225 *---------------------------------------------------------------------------*)
4.226
4.227 fun list_beta_conv tm =
4.228 - let fun rbeta th = Thm.transitive th (Thm.beta_conversion false (#2(D.dest_eq(cconcl th))))
4.229 + let fun rbeta th = Thm.transitive th (Thm.beta_conversion false (#2(Dcterm.dest_eq(cconcl th))))
4.230 fun iter [] = Thm.reflexive tm
4.231 | iter (v::rst) = rbeta (Thm.combination(iter rst) (Thm.reflexive v))
4.232 in iter end;
4.233 @@ -553,28 +548,28 @@
4.234 * General abstraction handlers, should probably go in USyntax.
4.235 *---------------------------------------------------------------------------*)
4.236 fun mk_aabs (vstr, body) =
4.237 - S.mk_abs {Bvar = vstr, Body = body}
4.238 - handle U.ERR _ => S.mk_pabs {varstruct = vstr, body = body};
4.239 + USyntax.mk_abs {Bvar = vstr, Body = body}
4.240 + handle Utils.ERR _ => USyntax.mk_pabs {varstruct = vstr, body = body};
4.241
4.242 fun list_mk_aabs (vstrl,tm) =
4.243 fold_rev (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm;
4.244
4.245 fun dest_aabs used tm =
4.246 - let val ({Bvar,Body}, used') = S.dest_abs used tm
4.247 + let val ({Bvar,Body}, used') = USyntax.dest_abs used tm
4.248 in (Bvar, Body, used') end
4.249 - handle U.ERR _ =>
4.250 - let val {varstruct, body, used} = S.dest_pabs used tm
4.251 + handle Utils.ERR _ =>
4.252 + let val {varstruct, body, used} = USyntax.dest_pabs used tm
4.253 in (varstruct, body, used) end;
4.254
4.255 fun strip_aabs used tm =
4.256 let val (vstr, body, used') = dest_aabs used tm
4.257 val (bvs, core, used'') = strip_aabs used' body
4.258 in (vstr::bvs, core, used'') end
4.259 - handle U.ERR _ => ([], tm, used);
4.260 + handle Utils.ERR _ => ([], tm, used);
4.261
4.262 fun dest_combn tm 0 = (tm,[])
4.263 | dest_combn tm n =
4.264 - let val {Rator,Rand} = S.dest_comb tm
4.265 + let val {Rator,Rand} = USyntax.dest_comb tm
4.266 val (f,rands) = dest_combn Rator (n-1)
4.267 in (f,Rand::rands)
4.268 end;
4.269 @@ -582,7 +577,7 @@
4.270
4.271
4.272
4.273 -local fun dest_pair M = let val {fst,snd} = S.dest_pair M in (fst,snd) end
4.274 +local fun dest_pair M = let val {fst,snd} = USyntax.dest_pair M in (fst,snd) end
4.275 fun mk_fst tm =
4.276 let val ty as Type(@{type_name Product_Type.prod}, [fty,sty]) = type_of tm
4.277 in Const ("Product_Type.fst", ty --> fty) $ tm end
4.278 @@ -610,7 +605,7 @@
4.279 *---------------------------------------------------------------------------*)
4.280
4.281 fun VSTRUCT_ELIM tych a vstr th =
4.282 - let val L = S.free_vars_lr vstr
4.283 + let val L = USyntax.free_vars_lr vstr
4.284 val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr)))
4.285 val thm1 = Thm.implies_intr bind1 (SUBS [SYM(Thm.assume bind1)] th)
4.286 val thm2 = forall_intr_list (map tych L) thm1
4.287 @@ -641,7 +636,7 @@
4.288 in (strip_aabs used f,args)
4.289 end;
4.290
4.291 -fun pbeta_redex M n = can (U.C (dest_pbeta_redex []) n) M;
4.292 +fun pbeta_redex M n = can (Utils.C (dest_pbeta_redex []) n) M;
4.293
4.294 fun dest_impl tm =
4.295 let val ants = Logic.strip_imp_prems tm
4.296 @@ -649,7 +644,7 @@
4.297 in (ants,get_lhs eq)
4.298 end;
4.299
4.300 -fun restricted t = is_some (S.find_term
4.301 +fun restricted t = is_some (USyntax.find_term
4.302 (fn (Const(@{const_name Recdef.cut},_)) =>true | _ => false)
4.303 t)
4.304
4.305 @@ -675,7 +670,7 @@
4.306 val lhs = tych(get_lhs eq)
4.307 val ss' = Simplifier.add_prems (map ASSUME ants) ss
4.308 val lhs_eq_lhs1 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used) ss' lhs
4.309 - handle U.ERR _ => Thm.reflexive lhs
4.310 + handle Utils.ERR _ => Thm.reflexive lhs
4.311 val dummy = print_thms "proven:" [lhs_eq_lhs1]
4.312 val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
4.313 val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq
4.314 @@ -693,10 +688,10 @@
4.315 val eq1 = Logic.strip_imp_concl imp_body1
4.316 val Q = get_lhs eq1
4.317 val QeqQ1 = pbeta_reduce (tych Q)
4.318 - val Q1 = #2(D.dest_eq(cconcl QeqQ1))
4.319 + val Q1 = #2(Dcterm.dest_eq(cconcl QeqQ1))
4.320 val ss' = Simplifier.add_prems (map ASSUME ants1) ss
4.321 val Q1eeqQ2 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used') ss' Q1
4.322 - handle U.ERR _ => Thm.reflexive Q1
4.323 + handle Utils.ERR _ => Thm.reflexive Q1
4.324 val Q2 = #2 (Logic.dest_equals (Thm.prop_of Q1eeqQ2))
4.325 val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
4.326 val Q2eeqQ3 = Thm.symmetric(pbeta_reduce Q3 RS eq_reflection)
4.327 @@ -708,7 +703,7 @@
4.328 val impth = implies_intr_list ants1 QeeqQ3
4.329 val impth1 = impth RS meta_eq_to_obj_eq
4.330 (* Need to abstract *)
4.331 - val ant_th = U.itlist2 (PGEN tych) args vstrl impth1
4.332 + val ant_th = Utils.itlist2 (PGEN tych) args vstrl impth1
4.333 in ant_th COMP thm
4.334 end
4.335 fun q_eliminate (thm,imp,thy) =
4.336 @@ -722,7 +717,7 @@
4.337 val ss' = MetaSimplifier.add_prems (map ASSUME ants1) ss
4.338 val Q_eeq_Q1 = MetaSimplifier.rewrite_cterm
4.339 (false,true,false) (prover used') ss' (tych Q)
4.340 - handle U.ERR _ => Thm.reflexive (tych Q)
4.341 + handle Utils.ERR _ => Thm.reflexive (tych Q)
4.342 val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
4.343 val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq
4.344 val ant_th = forall_intr_list(map tych vlist)lhs_eq_lhs2
4.345 @@ -740,7 +735,7 @@
4.346 (* Assume that the leading constant is ==, *)
4.347 | _ => thm (* if it is not a ==> *)
4.348 in SOME(eliminate (rename thm)) end
4.349 - handle U.ERR _ => NONE (* FIXME handle THM as well?? *)
4.350 + handle Utils.ERR _ => NONE (* FIXME handle THM as well?? *)
4.351
4.352 fun restrict_prover ss thm =
4.353 let val dummy = say "restrict_prover:"
4.354 @@ -765,12 +760,12 @@
4.355 val rcontext = rev cntxt
4.356 val cncl = HOLogic.dest_Trueprop o Thm.prop_of
4.357 val antl = case rcontext of [] => []
4.358 - | _ => [S.list_mk_conj(map cncl rcontext)]
4.359 - val TC = genl(S.list_mk_imp(antl, A))
4.360 + | _ => [USyntax.list_mk_conj(map cncl rcontext)]
4.361 + val TC = genl(USyntax.list_mk_imp(antl, A))
4.362 val dummy = print_cterm "func:" (cterm_of thy func)
4.363 val dummy = print_cterm "TC:" (cterm_of thy (HOLogic.mk_Trueprop TC))
4.364 val dummy = tc_list := (TC :: !tc_list)
4.365 - val nestedp = is_some (S.find_term is_func TC)
4.366 + val nestedp = is_some (USyntax.find_term is_func TC)
4.367 val dummy = if nestedp then say "nested" else say "not_nested"
4.368 val th' = if nestedp then raise RULES_ERR "solver" "nested function"
4.369 else let val cTC = cterm_of thy
4.370 @@ -782,7 +777,7 @@
4.371 end
4.372 val th'' = th' RS thm
4.373 in SOME (th'')
4.374 - end handle U.ERR _ => NONE (* FIXME handle THM as well?? *)
4.375 + end handle Utils.ERR _ => NONE (* FIXME handle THM as well?? *)
4.376 in
4.377 (if (is_cong thm) then cong_prover else restrict_prover) ss thm
4.378 end
5.1 --- a/src/HOL/Tools/TFL/tfl.ML Wed Dec 15 15:01:34 2010 +0100
5.2 +++ b/src/HOL/Tools/TFL/tfl.ML Wed Dec 15 15:11:56 2010 +0100
5.3 @@ -42,17 +42,13 @@
5.4
5.5 val trace = Unsynchronized.ref false;
5.6
5.7 -structure R = Rules;
5.8 -structure S = USyntax;
5.9 -structure U = Utils;
5.10
5.11 +fun TFL_ERR func mesg = Utils.ERR {module = "Tfl", func = func, mesg = mesg};
5.12
5.13 -fun TFL_ERR func mesg = U.ERR {module = "Tfl", func = func, mesg = mesg};
5.14 +val concl = #2 o Rules.dest_thm;
5.15 +val hyp = #1 o Rules.dest_thm;
5.16
5.17 -val concl = #2 o R.dest_thm;
5.18 -val hyp = #1 o R.dest_thm;
5.19 -
5.20 -val list_mk_type = U.end_itlist (curry (op -->));
5.21 +val list_mk_type = Utils.end_itlist (curry (op -->));
5.22
5.23 fun front_last [] = raise TFL_ERR "front_last" "empty list"
5.24 | front_last [x] = ([],x)
5.25 @@ -99,12 +95,12 @@
5.26 val (in_group, not_in_group) =
5.27 fold_rev (fn (row as (p::rst, rhs)) =>
5.28 fn (in_group,not_in_group) =>
5.29 - let val (pc,args) = S.strip_comb p
5.30 + let val (pc,args) = USyntax.strip_comb p
5.31 in if (#1(dest_Const pc) = c)
5.32 then ((args@rst, rhs)::in_group, not_in_group)
5.33 else (in_group, row::not_in_group)
5.34 end) rows ([],[])
5.35 - val col_types = U.take type_of (length L, #1(hd in_group))
5.36 + val col_types = Utils.take type_of (length L, #1(hd in_group))
5.37 in
5.38 part{constrs = crst, rows = not_in_group,
5.39 A = {constructor = c,
5.40 @@ -142,8 +138,8 @@
5.41 val L = binder_types Ty
5.42 and ty = body_type Ty
5.43 val ty_theta = ty_match ty colty
5.44 - val c' = S.inst ty_theta c
5.45 - val gvars = map (S.inst ty_theta o gv) L
5.46 + val c' = USyntax.inst ty_theta c
5.47 + val gvars = map (USyntax.inst ty_theta o gv) L
5.48 in (c', gvars)
5.49 end;
5.50
5.51 @@ -155,7 +151,7 @@
5.52 fun mk_group name rows =
5.53 fold_rev (fn (row as ((prfx, p::rst), rhs)) =>
5.54 fn (in_group,not_in_group) =>
5.55 - let val (pc,args) = S.strip_comb p
5.56 + let val (pc,args) = USyntax.strip_comb p
5.57 in if ((#1 (Term.dest_Const pc) = name) handle TERM _ => false)
5.58 then (((prfx,args@rst), rhs)::in_group, not_in_group)
5.59 else (in_group, row::not_in_group) end)
5.60 @@ -174,7 +170,7 @@
5.61 val (in_group, not_in_group) = mk_group (#1 (dest_Const c')) rows
5.62 val in_group' =
5.63 if (null in_group) (* Constructor not given *)
5.64 - then [((prfx, #2(fresh c)), (S.ARB res_ty, (~1,false)))]
5.65 + then [((prfx, #2(fresh c)), (USyntax.ARB res_ty, (~1,false)))]
5.66 else in_group
5.67 in
5.68 part{constrs = crst,
5.69 @@ -264,7 +260,7 @@
5.70 (ListPair.zip (new_formals, groups))
5.71 val rec_calls = map mk news
5.72 val (pat_rect,dtrees) = ListPair.unzip rec_calls
5.73 - val case_functions = map S.list_mk_abs
5.74 + val case_functions = map USyntax.list_mk_abs
5.75 (ListPair.zip (new_formals, dtrees))
5.76 val types = map type_of (case_functions@[u]) @ [range_ty]
5.77 val case_const' = Const(case_const_name, list_mk_type types)
5.78 @@ -279,11 +275,11 @@
5.79
5.80 (* Repeated variable occurrences in a pattern are not allowed. *)
5.81 fun FV_multiset tm =
5.82 - case (S.dest_term tm)
5.83 - of S.VAR{Name = c, Ty = T} => [Free(c, T)]
5.84 - | S.CONST _ => []
5.85 - | S.COMB{Rator, Rand} => FV_multiset Rator @ FV_multiset Rand
5.86 - | S.LAMB _ => raise TFL_ERR "FV_multiset" "lambda";
5.87 + case (USyntax.dest_term tm)
5.88 + of USyntax.VAR{Name = c, Ty = T} => [Free(c, T)]
5.89 + | USyntax.CONST _ => []
5.90 + | USyntax.COMB{Rator, Rand} => FV_multiset Rator @ FV_multiset Rand
5.91 + | USyntax.LAMB _ => raise TFL_ERR "FV_multiset" "lambda";
5.92
5.93 fun no_repeat_vars thy pat =
5.94 let fun check [] = true
5.95 @@ -370,10 +366,10 @@
5.96 | poly_tvars (TVar ((a,i),sort)) = TVar (("?" ^ a, i+1), sort);
5.97
5.98 local val f_eq_wfrec_R_M =
5.99 - #ant(S.dest_imp(#2(S.strip_forall (concl Thms.WFREC_COROLLARY))))
5.100 - val {lhs=f, rhs} = S.dest_eq f_eq_wfrec_R_M
5.101 + #ant(USyntax.dest_imp(#2(USyntax.strip_forall (concl Thms.WFREC_COROLLARY))))
5.102 + val {lhs=f, rhs} = USyntax.dest_eq f_eq_wfrec_R_M
5.103 val (fname,_) = dest_Free f
5.104 - val (wfrec,_) = S.strip_comb rhs
5.105 + val (wfrec,_) = USyntax.strip_comb rhs
5.106 in
5.107 fun wfrec_definition0 thy fid R (functional as Abs(x, Ty, _)) =
5.108 let val def_name = Long_Name.base_name fid ^ "_def"
5.109 @@ -422,15 +418,15 @@
5.110
5.111 fun post_definition meta_tflCongs (theory, (def, pats)) =
5.112 let val tych = Thry.typecheck theory
5.113 - val f = #lhs(S.dest_eq(concl def))
5.114 - val corollary = R.MATCH_MP Thms.WFREC_COROLLARY def
5.115 + val f = #lhs(USyntax.dest_eq(concl def))
5.116 + val corollary = Rules.MATCH_MP Thms.WFREC_COROLLARY def
5.117 val pats' = filter given pats
5.118 val given_pats = map pat_of pats'
5.119 val rows = map row_of_pat pats'
5.120 - val WFR = #ant(S.dest_imp(concl corollary))
5.121 - val R = #Rand(S.dest_comb WFR)
5.122 - val corollary' = R.UNDISCH corollary (* put WF R on assums *)
5.123 - val corollaries = map (fn pat => R.SPEC (tych pat) corollary')
5.124 + val WFR = #ant(USyntax.dest_imp(concl corollary))
5.125 + val R = #Rand(USyntax.dest_comb WFR)
5.126 + val corollary' = Rules.UNDISCH corollary (* put WF R on assums *)
5.127 + val corollaries = map (fn pat => Rules.SPEC (tych pat) corollary')
5.128 given_pats
5.129 val (case_rewrites,context_congs) = extraction_thms theory
5.130 (*case_ss causes minimal simplification: bodies of case expressions are
5.131 @@ -440,12 +436,12 @@
5.132 (HOL_basic_ss addcongs
5.133 (map (#weak_case_cong o snd) o Symtab.dest o Datatype.get_all) theory addsimps case_rewrites)
5.134 val corollaries' = map (Simplifier.simplify case_ss) corollaries
5.135 - val extract = R.CONTEXT_REWRITE_RULE
5.136 + val extract = Rules.CONTEXT_REWRITE_RULE
5.137 (f, [R], @{thm cut_apply}, meta_tflCongs@context_congs)
5.138 val (rules, TCs) = ListPair.unzip (map extract corollaries')
5.139 val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules
5.140 - val mk_cond_rule = R.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
5.141 - val rules1 = R.LIST_CONJ(map mk_cond_rule rules0)
5.142 + val mk_cond_rule = Rules.FILTER_DISCH_ALL(not o curry (op aconv) WFR)
5.143 + val rules1 = Rules.LIST_CONJ(map mk_cond_rule rules0)
5.144 in
5.145 {rules = rules1,
5.146 rows = rows,
5.147 @@ -463,8 +459,8 @@
5.148 *---------------------------------------------------------------------------*)
5.149
5.150 fun wfrec_eqns thy fid tflCongs eqns =
5.151 - let val {lhs,rhs} = S.dest_eq (hd eqns)
5.152 - val (f,args) = S.strip_comb lhs
5.153 + let val {lhs,rhs} = USyntax.dest_eq (hd eqns)
5.154 + val (f,args) = USyntax.strip_comb lhs
5.155 val (fname,fty) = dest_atom f
5.156 val (SV,a) = front_last args (* SV = schematic variables *)
5.157 val g = list_comb(f,SV)
5.158 @@ -482,22 +478,22 @@
5.159 else ()
5.160 val (case_rewrites,context_congs) = extraction_thms thy
5.161 val tych = Thry.typecheck thy
5.162 - val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
5.163 + val WFREC_THM0 = Rules.ISPEC (tych functional) Thms.WFREC_COROLLARY
5.164 val Const(@{const_name All},_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
5.165 val R = Free (Name.variant (List.foldr OldTerm.add_term_names [] eqns) Rname,
5.166 Rtype)
5.167 - val WFREC_THM = R.ISPECL [tych R, tych g] WFREC_THM0
5.168 - val ([proto_def, WFR],_) = S.strip_imp(concl WFREC_THM)
5.169 + val WFREC_THM = Rules.ISPECL [tych R, tych g] WFREC_THM0
5.170 + val ([proto_def, WFR],_) = USyntax.strip_imp(concl WFREC_THM)
5.171 val dummy =
5.172 if !trace then
5.173 writeln ("ORIGINAL PROTO_DEF: " ^
5.174 Syntax.string_of_term_global thy proto_def)
5.175 else ()
5.176 - val R1 = S.rand WFR
5.177 - val corollary' = R.UNDISCH(R.UNDISCH WFREC_THM)
5.178 - val corollaries = map (fn pat => R.SPEC (tych pat) corollary') given_pats
5.179 + val R1 = USyntax.rand WFR
5.180 + val corollary' = Rules.UNDISCH (Rules.UNDISCH WFREC_THM)
5.181 + val corollaries = map (fn pat => Rules.SPEC (tych pat) corollary') given_pats
5.182 val corollaries' = map (rewrite_rule case_rewrites) corollaries
5.183 - fun extract X = R.CONTEXT_REWRITE_RULE
5.184 + fun extract X = Rules.CONTEXT_REWRITE_RULE
5.185 (f, R1::SV, @{thm cut_apply}, tflCongs@context_congs) X
5.186 in {proto_def = proto_def,
5.187 SV=SV,
5.188 @@ -517,8 +513,8 @@
5.189 fun lazyR_def thy fid tflCongs eqns =
5.190 let val {proto_def,WFR,pats,extracta,SV} =
5.191 wfrec_eqns thy fid tflCongs eqns
5.192 - val R1 = S.rand WFR
5.193 - val f = #lhs(S.dest_eq proto_def)
5.194 + val R1 = USyntax.rand WFR
5.195 + val f = #lhs(USyntax.dest_eq proto_def)
5.196 val (extractants,TCl) = ListPair.unzip extracta
5.197 val dummy = if !trace
5.198 then writeln (cat_lines ("Extractants =" ::
5.199 @@ -526,17 +522,17 @@
5.200 else ()
5.201 val TCs = fold_rev (union (op aconv)) TCl []
5.202 val full_rqt = WFR::TCs
5.203 - val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
5.204 - val R'abs = S.rand R'
5.205 + val R' = USyntax.mk_select{Bvar=R1, Body=USyntax.list_mk_conj full_rqt}
5.206 + val R'abs = USyntax.rand R'
5.207 val proto_def' = subst_free[(R1,R')] proto_def
5.208 val dummy = if !trace then writeln ("proto_def' = " ^
5.209 Syntax.string_of_term_global
5.210 thy proto_def')
5.211 else ()
5.212 - val {lhs,rhs} = S.dest_eq proto_def'
5.213 - val (c,args) = S.strip_comb lhs
5.214 + val {lhs,rhs} = USyntax.dest_eq proto_def'
5.215 + val (c,args) = USyntax.strip_comb lhs
5.216 val (name,Ty) = dest_atom c
5.217 - val defn = const_def thy (name, Ty, S.list_mk_abs (args,rhs))
5.218 + val defn = const_def thy (name, Ty, USyntax.list_mk_abs (args,rhs))
5.219 val ([def0], theory) =
5.220 thy
5.221 |> Global_Theory.add_defs false
5.222 @@ -545,31 +541,31 @@
5.223 val dummy =
5.224 if !trace then writeln ("DEF = " ^ Display.string_of_thm_global theory def)
5.225 else ()
5.226 - (* val fconst = #lhs(S.dest_eq(concl def)) *)
5.227 + (* val fconst = #lhs(USyntax.dest_eq(concl def)) *)
5.228 val tych = Thry.typecheck theory
5.229 val full_rqt_prop = map (Dcterm.mk_prop o tych) full_rqt
5.230 (*lcp: a lot of object-logic inference to remove*)
5.231 - val baz = R.DISCH_ALL
5.232 - (fold_rev R.DISCH full_rqt_prop
5.233 - (R.LIST_CONJ extractants))
5.234 + val baz = Rules.DISCH_ALL
5.235 + (fold_rev Rules.DISCH full_rqt_prop
5.236 + (Rules.LIST_CONJ extractants))
5.237 val dum = if !trace then writeln ("baz = " ^ Display.string_of_thm_global theory baz)
5.238 else ()
5.239 val f_free = Free (fid, fastype_of f) (*'cos f is a Const*)
5.240 val SV' = map tych SV;
5.241 val SVrefls = map Thm.reflexive SV'
5.242 - val def0 = (fold (fn x => fn th => R.rbeta(Thm.combination th x))
5.243 + val def0 = (fold (fn x => fn th => Rules.rbeta(Thm.combination th x))
5.244 SVrefls def)
5.245 RS meta_eq_to_obj_eq
5.246 - val def' = R.MP (R.SPEC (tych R') (R.GEN (tych R1) baz)) def0
5.247 - val body_th = R.LIST_CONJ (map R.ASSUME full_rqt_prop)
5.248 + val def' = Rules.MP (Rules.SPEC (tych R') (Rules.GEN (tych R1) baz)) def0
5.249 + val body_th = Rules.LIST_CONJ (map Rules.ASSUME full_rqt_prop)
5.250 val SELECT_AX = (*in this way we hope to avoid a STATIC dependence upon
5.251 theory Hilbert_Choice*)
5.252 ML_Context.thm "Hilbert_Choice.tfl_some"
5.253 handle ERROR msg => cat_error msg
5.254 "defer_recdef requires theory Main or at least Hilbert_Choice as parent"
5.255 - val bar = R.MP (R.ISPECL[tych R'abs, tych R1] SELECT_AX) body_th
5.256 + val bar = Rules.MP (Rules.ISPECL[tych R'abs, tych R1] SELECT_AX) body_th
5.257 in {theory = theory, R=R1, SV=SV,
5.258 - rules = fold (U.C R.MP) (R.CONJUNCTS bar) def',
5.259 + rules = fold (Utils.C Rules.MP) (Rules.CONJUNCTS bar) def',
5.260 full_pats_TCs = merge (map pat_of pats) (ListPair.zip (givens pats, TCl)),
5.261 patterns = pats}
5.262 end;
5.263 @@ -603,8 +599,8 @@
5.264 *---------------------------------------------------------------------------*)
5.265
5.266 fun alpha_ex_unroll (xlist, tm) =
5.267 - let val (qvars,body) = S.strip_exists tm
5.268 - val vlist = #2(S.strip_comb (S.rhs body))
5.269 + let val (qvars,body) = USyntax.strip_exists tm
5.270 + val vlist = #2 (USyntax.strip_comb (USyntax.rhs body))
5.271 val plist = ListPair.zip (vlist, xlist)
5.272 val args = map (the o AList.lookup (op aconv) plist) qvars
5.273 handle Option => raise Fail "TFL.alpha_ex_unroll: no correspondence"
5.274 @@ -634,7 +630,7 @@
5.275 fun fail s = raise TFL_ERR "mk_case" s
5.276 fun mk{rows=[],...} = fail"no rows"
5.277 | mk{path=[], rows = [([], (thm, bindings))]} =
5.278 - R.IT_EXISTS (map tych_binding bindings) thm
5.279 + Rules.IT_EXISTS (map tych_binding bindings) thm
5.280 | mk{path = u::rstp, rows as (p::_, _)::_} =
5.281 let val (pat_rectangle,rights) = ListPair.unzip rows
5.282 val col0 = map hd pat_rectangle
5.283 @@ -651,8 +647,8 @@
5.284 case (ty_info ty_name)
5.285 of NONE => fail("Not a known datatype: "^ty_name)
5.286 | SOME{constructors,nchotomy} =>
5.287 - let val thm' = R.ISPEC (tych u) nchotomy
5.288 - val disjuncts = S.strip_disj (concl thm')
5.289 + let val thm' = Rules.ISPEC (tych u) nchotomy
5.290 + val disjuncts = USyntax.strip_disj (concl thm')
5.291 val subproblems = divide(constructors, rows)
5.292 val groups = map #group subproblems
5.293 and new_formals = map #new_formals subproblems
5.294 @@ -660,17 +656,17 @@
5.295 (new_formals, disjuncts)
5.296 val constraints = map #1 existentials
5.297 val vexl = map #2 existentials
5.298 - fun expnd tm (pats,(th,b)) = (pats,(R.SUBS[R.ASSUME(tych tm)]th,b))
5.299 + fun expnd tm (pats,(th,b)) = (pats, (Rules.SUBS [Rules.ASSUME (tych tm)] th, b))
5.300 val news = map (fn (nf,rows,c) => {path = nf@rstp,
5.301 rows = map (expnd c) rows})
5.302 - (U.zip3 new_formals groups constraints)
5.303 + (Utils.zip3 new_formals groups constraints)
5.304 val recursive_thms = map mk news
5.305 val build_exists = Library.foldr
5.306 (fn((x,t), th) =>
5.307 - R.CHOOSE (tych x, R.ASSUME (tych t)) th)
5.308 + Rules.CHOOSE (tych x, Rules.ASSUME (tych t)) th)
5.309 val thms' = ListPair.map build_exists (vexl, recursive_thms)
5.310 - val same_concls = R.EVEN_ORS thms'
5.311 - in R.DISJ_CASESL thm' same_concls
5.312 + val same_concls = Rules.EVEN_ORS thms'
5.313 + in Rules.DISJ_CASESL thm' same_concls
5.314 end
5.315 end end
5.316 in mk
5.317 @@ -688,14 +684,14 @@
5.318 val a = Free (aname, T)
5.319 val v = Free (vname, T)
5.320 val a_eq_v = HOLogic.mk_eq(a,v)
5.321 - val ex_th0 = R.EXISTS (tych (S.mk_exists{Bvar=v,Body=a_eq_v}), tych a)
5.322 - (R.REFL (tych a))
5.323 - val th0 = R.ASSUME (tych a_eq_v)
5.324 + val ex_th0 = Rules.EXISTS (tych (USyntax.mk_exists{Bvar=v,Body=a_eq_v}), tych a)
5.325 + (Rules.REFL (tych a))
5.326 + val th0 = Rules.ASSUME (tych a_eq_v)
5.327 val rows = map (fn x => ([x], (th0,[]))) pats
5.328 in
5.329 - R.GEN (tych a)
5.330 - (R.RIGHT_ASSOC
5.331 - (R.CHOOSE(tych v, ex_th0)
5.332 + Rules.GEN (tych a)
5.333 + (Rules.RIGHT_ASSOC
5.334 + (Rules.CHOOSE(tych v, ex_th0)
5.335 (mk_case ty_info (vname::aname::names)
5.336 thy {path=[v], rows=rows})))
5.337 end end;
5.338 @@ -712,57 +708,57 @@
5.339 *---------------------------------------------------------------------------*)
5.340 (*
5.341 local infix 5 ==>
5.342 - fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2}
5.343 + fun (tm1 ==> tm2) = USyntax.mk_imp{ant = tm1, conseq = tm2}
5.344 in
5.345 fun build_ih f P (pat,TCs) =
5.346 - let val globals = S.free_vars_lr pat
5.347 - fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
5.348 + let val globals = USyntax.free_vars_lr pat
5.349 + fun nested tm = is_some (USyntax.find_term (curry (op aconv) f) tm)
5.350 fun dest_TC tm =
5.351 - let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm))
5.352 - val (R,y,_) = S.dest_relation R_y_pat
5.353 + let val (cntxt,R_y_pat) = USyntax.strip_imp(#2(USyntax.strip_forall tm))
5.354 + val (R,y,_) = USyntax.dest_relation R_y_pat
5.355 val P_y = if (nested tm) then R_y_pat ==> P$y else P$y
5.356 in case cntxt
5.357 of [] => (P_y, (tm,[]))
5.358 | _ => let
5.359 - val imp = S.list_mk_conj cntxt ==> P_y
5.360 - val lvs = gen_rems (op aconv) (S.free_vars_lr imp, globals)
5.361 - val locals = #2(U.pluck (curry (op aconv) P) lvs) handle U.ERR _ => lvs
5.362 - in (S.list_mk_forall(locals,imp), (tm,locals)) end
5.363 + val imp = USyntax.list_mk_conj cntxt ==> P_y
5.364 + val lvs = gen_rems (op aconv) (USyntax.free_vars_lr imp, globals)
5.365 + val locals = #2(Utils.pluck (curry (op aconv) P) lvs) handle Utils.ERR _ => lvs
5.366 + in (USyntax.list_mk_forall(locals,imp), (tm,locals)) end
5.367 end
5.368 in case TCs
5.369 - of [] => (S.list_mk_forall(globals, P$pat), [])
5.370 + of [] => (USyntax.list_mk_forall(globals, P$pat), [])
5.371 | _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs)
5.372 - val ind_clause = S.list_mk_conj ihs ==> P$pat
5.373 - in (S.list_mk_forall(globals,ind_clause), TCs_locals)
5.374 + val ind_clause = USyntax.list_mk_conj ihs ==> P$pat
5.375 + in (USyntax.list_mk_forall(globals,ind_clause), TCs_locals)
5.376 end
5.377 end
5.378 end;
5.379 *)
5.380
5.381 local infix 5 ==>
5.382 - fun (tm1 ==> tm2) = S.mk_imp{ant = tm1, conseq = tm2}
5.383 + fun (tm1 ==> tm2) = USyntax.mk_imp{ant = tm1, conseq = tm2}
5.384 in
5.385 fun build_ih f (P,SV) (pat,TCs) =
5.386 - let val pat_vars = S.free_vars_lr pat
5.387 + let val pat_vars = USyntax.free_vars_lr pat
5.388 val globals = pat_vars@SV
5.389 - fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
5.390 + fun nested tm = is_some (USyntax.find_term (curry (op aconv) f) tm)
5.391 fun dest_TC tm =
5.392 - let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm))
5.393 - val (R,y,_) = S.dest_relation R_y_pat
5.394 + let val (cntxt,R_y_pat) = USyntax.strip_imp(#2(USyntax.strip_forall tm))
5.395 + val (R,y,_) = USyntax.dest_relation R_y_pat
5.396 val P_y = if (nested tm) then R_y_pat ==> P$y else P$y
5.397 in case cntxt
5.398 of [] => (P_y, (tm,[]))
5.399 | _ => let
5.400 - val imp = S.list_mk_conj cntxt ==> P_y
5.401 - val lvs = subtract (op aconv) globals (S.free_vars_lr imp)
5.402 - val locals = #2(U.pluck (curry (op aconv) P) lvs) handle U.ERR _ => lvs
5.403 - in (S.list_mk_forall(locals,imp), (tm,locals)) end
5.404 + val imp = USyntax.list_mk_conj cntxt ==> P_y
5.405 + val lvs = subtract (op aconv) globals (USyntax.free_vars_lr imp)
5.406 + val locals = #2(Utils.pluck (curry (op aconv) P) lvs) handle Utils.ERR _ => lvs
5.407 + in (USyntax.list_mk_forall(locals,imp), (tm,locals)) end
5.408 end
5.409 in case TCs
5.410 - of [] => (S.list_mk_forall(pat_vars, P$pat), [])
5.411 + of [] => (USyntax.list_mk_forall(pat_vars, P$pat), [])
5.412 | _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs)
5.413 - val ind_clause = S.list_mk_conj ihs ==> P$pat
5.414 - in (S.list_mk_forall(pat_vars,ind_clause), TCs_locals)
5.415 + val ind_clause = USyntax.list_mk_conj ihs ==> P$pat
5.416 + in (USyntax.list_mk_forall(pat_vars,ind_clause), TCs_locals)
5.417 end
5.418 end
5.419 end;
5.420 @@ -776,29 +772,29 @@
5.421 *---------------------------------------------------------------------------*)
5.422 fun prove_case f thy (tm,TCs_locals,thm) =
5.423 let val tych = Thry.typecheck thy
5.424 - val antc = tych(#ant(S.dest_imp tm))
5.425 - val thm' = R.SPEC_ALL thm
5.426 - fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
5.427 - fun get_cntxt TC = tych(#ant(S.dest_imp(#2(S.strip_forall(concl TC)))))
5.428 + val antc = tych(#ant(USyntax.dest_imp tm))
5.429 + val thm' = Rules.SPEC_ALL thm
5.430 + fun nested tm = is_some (USyntax.find_term (curry (op aconv) f) tm)
5.431 + fun get_cntxt TC = tych(#ant(USyntax.dest_imp(#2(USyntax.strip_forall(concl TC)))))
5.432 fun mk_ih ((TC,locals),th2,nested) =
5.433 - R.GENL (map tych locals)
5.434 - (if nested then R.DISCH (get_cntxt TC) th2 handle U.ERR _ => th2
5.435 - else if S.is_imp (concl TC) then R.IMP_TRANS TC th2
5.436 - else R.MP th2 TC)
5.437 + Rules.GENL (map tych locals)
5.438 + (if nested then Rules.DISCH (get_cntxt TC) th2 handle Utils.ERR _ => th2
5.439 + else if USyntax.is_imp (concl TC) then Rules.IMP_TRANS TC th2
5.440 + else Rules.MP th2 TC)
5.441 in
5.442 - R.DISCH antc
5.443 - (if S.is_imp(concl thm') (* recursive calls in this clause *)
5.444 - then let val th1 = R.ASSUME antc
5.445 + Rules.DISCH antc
5.446 + (if USyntax.is_imp(concl thm') (* recursive calls in this clause *)
5.447 + then let val th1 = Rules.ASSUME antc
5.448 val TCs = map #1 TCs_locals
5.449 - val ylist = map (#2 o S.dest_relation o #2 o S.strip_imp o
5.450 - #2 o S.strip_forall) TCs
5.451 - val TClist = map (fn(TC,lvs) => (R.SPEC_ALL(R.ASSUME(tych TC)),lvs))
5.452 + val ylist = map (#2 o USyntax.dest_relation o #2 o USyntax.strip_imp o
5.453 + #2 o USyntax.strip_forall) TCs
5.454 + val TClist = map (fn(TC,lvs) => (Rules.SPEC_ALL(Rules.ASSUME(tych TC)),lvs))
5.455 TCs_locals
5.456 - val th2list = map (U.C R.SPEC th1 o tych) ylist
5.457 + val th2list = map (Utils.C Rules.SPEC th1 o tych) ylist
5.458 val nlist = map nested TCs
5.459 - val triples = U.zip3 TClist th2list nlist
5.460 + val triples = Utils.zip3 TClist th2list nlist
5.461 val Pylist = map mk_ih triples
5.462 - in R.MP thm' (R.LIST_CONJ Pylist) end
5.463 + in Rules.MP thm' (Rules.LIST_CONJ Pylist) end
5.464 else thm')
5.465 end;
5.466
5.467 @@ -812,12 +808,12 @@
5.468 *---------------------------------------------------------------------------*)
5.469 fun LEFT_ABS_VSTRUCT tych thm =
5.470 let fun CHOOSER v (tm,thm) =
5.471 - let val ex_tm = S.mk_exists{Bvar=v,Body=tm}
5.472 - in (ex_tm, R.CHOOSE(tych v, R.ASSUME (tych ex_tm)) thm)
5.473 + let val ex_tm = USyntax.mk_exists{Bvar=v,Body=tm}
5.474 + in (ex_tm, Rules.CHOOSE(tych v, Rules.ASSUME (tych ex_tm)) thm)
5.475 end
5.476 - val [veq] = filter (can S.dest_eq) (#1 (R.dest_thm thm))
5.477 - val {lhs,rhs} = S.dest_eq veq
5.478 - val L = S.free_vars_lr rhs
5.479 + val [veq] = filter (can USyntax.dest_eq) (#1 (Rules.dest_thm thm))
5.480 + val {lhs,rhs} = USyntax.dest_eq veq
5.481 + val L = USyntax.free_vars_lr rhs
5.482 in #2 (fold_rev CHOOSER L (veq,thm)) end;
5.483
5.484
5.485 @@ -830,39 +826,39 @@
5.486 *---------------------------------------------------------------------------*)
5.487 fun mk_induction thy {fconst, R, SV, pat_TCs_list} =
5.488 let val tych = Thry.typecheck thy
5.489 - val Sinduction = R.UNDISCH (R.ISPEC (tych R) Thms.WF_INDUCTION_THM)
5.490 + val Sinduction = Rules.UNDISCH (Rules.ISPEC (tych R) Thms.WF_INDUCTION_THM)
5.491 val (pats,TCsl) = ListPair.unzip pat_TCs_list
5.492 val case_thm = complete_cases thy pats
5.493 val domain = (type_of o hd) pats
5.494 val Pname = Name.variant (List.foldr (Library.foldr OldTerm.add_term_names)
5.495 [] (pats::TCsl)) "P"
5.496 val P = Free(Pname, domain --> HOLogic.boolT)
5.497 - val Sinduct = R.SPEC (tych P) Sinduction
5.498 - val Sinduct_assumf = S.rand ((#ant o S.dest_imp o concl) Sinduct)
5.499 + val Sinduct = Rules.SPEC (tych P) Sinduction
5.500 + val Sinduct_assumf = USyntax.rand ((#ant o USyntax.dest_imp o concl) Sinduct)
5.501 val Rassums_TCl' = map (build_ih fconst (P,SV)) pat_TCs_list
5.502 val (Rassums,TCl') = ListPair.unzip Rassums_TCl'
5.503 - val Rinduct_assum = R.ASSUME (tych (S.list_mk_conj Rassums))
5.504 + val Rinduct_assum = Rules.ASSUME (tych (USyntax.list_mk_conj Rassums))
5.505 val cases = map (fn pat => Term.betapply (Sinduct_assumf, pat)) pats
5.506 - val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum)
5.507 + val tasks = Utils.zip3 cases TCl' (Rules.CONJUNCTS Rinduct_assum)
5.508 val proved_cases = map (prove_case fconst thy) tasks
5.509 val v = Free (Name.variant (List.foldr OldTerm.add_term_names [] (map concl proved_cases))
5.510 "v",
5.511 domain)
5.512 val vtyped = tych v
5.513 - val substs = map (R.SYM o R.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
5.514 - val proved_cases1 = ListPair.map (fn (th,th') => R.SUBS[th]th')
5.515 + val substs = map (Rules.SYM o Rules.ASSUME o tych o (curry HOLogic.mk_eq v)) pats
5.516 + val proved_cases1 = ListPair.map (fn (th,th') => Rules.SUBS[th]th')
5.517 (substs, proved_cases)
5.518 val abs_cases = map (LEFT_ABS_VSTRUCT tych) proved_cases1
5.519 - val dant = R.GEN vtyped (R.DISJ_CASESL (R.ISPEC vtyped case_thm) abs_cases)
5.520 - val dc = R.MP Sinduct dant
5.521 - val Parg_ty = type_of(#Bvar(S.dest_forall(concl dc)))
5.522 - val vars = map (gvvariant[Pname]) (S.strip_prod_type Parg_ty)
5.523 - val dc' = fold_rev (R.GEN o tych) vars
5.524 - (R.SPEC (tych(S.mk_vstruct Parg_ty vars)) dc)
5.525 + val dant = Rules.GEN vtyped (Rules.DISJ_CASESL (Rules.ISPEC vtyped case_thm) abs_cases)
5.526 + val dc = Rules.MP Sinduct dant
5.527 + val Parg_ty = type_of(#Bvar(USyntax.dest_forall(concl dc)))
5.528 + val vars = map (gvvariant[Pname]) (USyntax.strip_prod_type Parg_ty)
5.529 + val dc' = fold_rev (Rules.GEN o tych) vars
5.530 + (Rules.SPEC (tych(USyntax.mk_vstruct Parg_ty vars)) dc)
5.531 in
5.532 - R.GEN (tych P) (R.DISCH (tych(concl Rinduct_assum)) dc')
5.533 + Rules.GEN (tych P) (Rules.DISCH (tych(concl Rinduct_assum)) dc')
5.534 end
5.535 -handle U.ERR _ => raise TFL_ERR "mk_induction" "failed derivation";
5.536 +handle Utils.ERR _ => raise TFL_ERR "mk_induction" "failed derivation";
5.537
5.538
5.539
5.540 @@ -876,15 +872,15 @@
5.541
5.542 fun simplify_induction thy hth ind =
5.543 let val tych = Thry.typecheck thy
5.544 - val (asl,_) = R.dest_thm ind
5.545 - val (_,tc_eq_tc') = R.dest_thm hth
5.546 - val tc = S.lhs tc_eq_tc'
5.547 + val (asl,_) = Rules.dest_thm ind
5.548 + val (_,tc_eq_tc') = Rules.dest_thm hth
5.549 + val tc = USyntax.lhs tc_eq_tc'
5.550 fun loop [] = ind
5.551 | loop (asm::rst) =
5.552 if (can (Thry.match_term thy asm) tc)
5.553 - then R.UNDISCH
5.554 - (R.MATCH_MP
5.555 - (R.MATCH_MP Thms.simp_thm (R.DISCH (tych asm) ind))
5.556 + then Rules.UNDISCH
5.557 + (Rules.MATCH_MP
5.558 + (Rules.MATCH_MP Thms.simp_thm (Rules.DISCH (tych asm) ind))
5.559 hth)
5.560 else loop rst
5.561 in loop asl
5.562 @@ -896,7 +892,7 @@
5.563 * assumption to the theorem.
5.564 *---------------------------------------------------------------------------*)
5.565 fun elim_tc tcthm (rule,induction) =
5.566 - (R.MP rule tcthm, R.PROVE_HYP tcthm induction)
5.567 + (Rules.MP rule tcthm, Rules.PROVE_HYP tcthm induction)
5.568
5.569
5.570 fun trace_thms s L =
5.571 @@ -911,17 +907,17 @@
5.572
5.573 fun postprocess strict {wf_tac, terminator, simplifier} theory {rules,induction,TCs} =
5.574 let val tych = Thry.typecheck theory
5.575 - val prove = R.prove strict;
5.576 + val prove = Rules.prove strict;
5.577
5.578 (*---------------------------------------------------------------------
5.579 * Attempt to eliminate WF condition. It's the only assumption of rules
5.580 *---------------------------------------------------------------------*)
5.581 val (rules1,induction1) =
5.582 let val thm = prove(tych(HOLogic.mk_Trueprop
5.583 - (hd(#1(R.dest_thm rules)))),
5.584 + (hd(#1(Rules.dest_thm rules)))),
5.585 wf_tac)
5.586 - in (R.PROVE_HYP thm rules, R.PROVE_HYP thm induction)
5.587 - end handle U.ERR _ => (rules,induction);
5.588 + in (Rules.PROVE_HYP thm rules, Rules.PROVE_HYP thm induction)
5.589 + end handle Utils.ERR _ => (rules,induction);
5.590
5.591 (*----------------------------------------------------------------------
5.592 * The termination condition (tc) is simplified to |- tc = tc' (there
5.593 @@ -938,14 +934,14 @@
5.594 val tc_eq = simplifier tc1
5.595 val _ = trace_thms "result: " [tc_eq]
5.596 in
5.597 - elim_tc (R.MATCH_MP Thms.eqT tc_eq) (r,ind)
5.598 - handle U.ERR _ =>
5.599 - (elim_tc (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
5.600 - (prove(tych(HOLogic.mk_Trueprop(S.rhs(concl tc_eq))),
5.601 + elim_tc (Rules.MATCH_MP Thms.eqT tc_eq) (r,ind)
5.602 + handle Utils.ERR _ =>
5.603 + (elim_tc (Rules.MATCH_MP(Rules.MATCH_MP Thms.rev_eq_mp tc_eq)
5.604 + (prove(tych(HOLogic.mk_Trueprop(USyntax.rhs(concl tc_eq))),
5.605 terminator)))
5.606 (r,ind)
5.607 - handle U.ERR _ =>
5.608 - (R.UNDISCH(R.MATCH_MP (R.MATCH_MP Thms.simp_thm r) tc_eq),
5.609 + handle Utils.ERR _ =>
5.610 + (Rules.UNDISCH(Rules.MATCH_MP (Rules.MATCH_MP Thms.simp_thm r) tc_eq),
5.611 simplify_induction theory tc_eq ind))
5.612 end
5.613
5.614 @@ -963,35 +959,35 @@
5.615 * 3. return |- tc = tc'
5.616 *---------------------------------------------------------------------*)
5.617 fun simplify_nested_tc tc =
5.618 - let val tc_eq = simplifier (tych (#2 (S.strip_forall tc)))
5.619 + let val tc_eq = simplifier (tych (#2 (USyntax.strip_forall tc)))
5.620 in
5.621 - R.GEN_ALL
5.622 - (R.MATCH_MP Thms.eqT tc_eq
5.623 - handle U.ERR _ =>
5.624 - (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
5.625 - (prove(tych(HOLogic.mk_Trueprop (S.rhs(concl tc_eq))),
5.626 + Rules.GEN_ALL
5.627 + (Rules.MATCH_MP Thms.eqT tc_eq
5.628 + handle Utils.ERR _ =>
5.629 + (Rules.MATCH_MP(Rules.MATCH_MP Thms.rev_eq_mp tc_eq)
5.630 + (prove(tych(HOLogic.mk_Trueprop (USyntax.rhs(concl tc_eq))),
5.631 terminator))
5.632 - handle U.ERR _ => tc_eq))
5.633 + handle Utils.ERR _ => tc_eq))
5.634 end
5.635
5.636 (*-------------------------------------------------------------------
5.637 * Attempt to simplify the termination conditions in each rule and
5.638 * in the induction theorem.
5.639 *-------------------------------------------------------------------*)
5.640 - fun strip_imp tm = if S.is_neg tm then ([],tm) else S.strip_imp tm
5.641 + fun strip_imp tm = if USyntax.is_neg tm then ([],tm) else USyntax.strip_imp tm
5.642 fun loop ([],extras,R,ind) = (rev R, ind, extras)
5.643 | loop ((r,ftcs)::rst, nthms, R, ind) =
5.644 let val tcs = #1(strip_imp (concl r))
5.645 val extra_tcs = subtract (op aconv) tcs ftcs
5.646 val extra_tc_thms = map simplify_nested_tc extra_tcs
5.647 val (r1,ind1) = fold simplify_tc tcs (r,ind)
5.648 - val r2 = R.FILTER_DISCH_ALL(not o S.is_WFR) r1
5.649 + val r2 = Rules.FILTER_DISCH_ALL(not o USyntax.is_WFR) r1
5.650 in loop(rst, nthms@extra_tc_thms, r2::R, ind1)
5.651 end
5.652 - val rules_tcs = ListPair.zip (R.CONJUNCTS rules1, TCs)
5.653 + val rules_tcs = ListPair.zip (Rules.CONJUNCTS rules1, TCs)
5.654 val (rules2,ind2,extras) = loop(rules_tcs,[],[],induction1)
5.655 in
5.656 - {induction = ind2, rules = R.LIST_CONJ rules2, nested_tcs = extras}
5.657 + {induction = ind2, rules = Rules.LIST_CONJ rules2, nested_tcs = extras}
5.658 end;
5.659
5.660
6.1 --- a/src/Tools/eqsubst.ML Wed Dec 15 15:01:34 2010 +0100
6.2 +++ b/src/Tools/eqsubst.ML Wed Dec 15 15:11:56 2010 +0100
6.3 @@ -119,11 +119,8 @@
6.4
6.5 end;
6.6
6.7 -structure EqSubst
6.8 -: EQSUBST
6.9 -= struct
6.10 -
6.11 -structure Z = Zipper;
6.12 +structure EqSubst: EQSUBST =
6.13 +struct
6.14
6.15 (* changes object "=" to meta "==" which prepares a given rewrite rule *)
6.16 fun prep_meta_eq ctxt =
6.17 @@ -196,11 +193,11 @@
6.18 abstracted out) for use in rewriting with RWInst.rw *)
6.19 fun prep_zipper_match z =
6.20 let
6.21 - val t = Z.trm z
6.22 - val c = Z.ctxt z
6.23 - val Ts = Z.C.nty_ctxt c
6.24 + val t = Zipper.trm z
6.25 + val c = Zipper.ctxt z
6.26 + val Ts = Zipper.C.nty_ctxt c
6.27 val (FakeTs', Ts', t') = fakefree_badbounds Ts t
6.28 - val absterm = mk_foo_match (Z.C.apply c) Ts' t'
6.29 + val absterm = mk_foo_match (Zipper.C.apply c) Ts' t'
6.30 in
6.31 (t', (FakeTs', Ts', absterm))
6.32 end;
6.33 @@ -291,7 +288,7 @@
6.34 (* Avoid considering replacing terms which have a var at the head as
6.35 they always succeed trivially, and uninterestingly. *)
6.36 fun valid_match_start z =
6.37 - (case bot_left_leaf_of (Z.trm z) of
6.38 + (case bot_left_leaf_of (Zipper.trm z) of
6.39 Var _ => false
6.40 | _ => true);
6.41
6.42 @@ -302,33 +299,33 @@
6.43 fun search_lr_valid validf =
6.44 let
6.45 fun sf_valid_td_lr z =
6.46 - let val here = if validf z then [Z.Here z] else [] in
6.47 - case Z.trm z
6.48 - of _ $ _ => [Z.LookIn (Z.move_down_left z)]
6.49 + let val here = if validf z then [Zipper.Here z] else [] in
6.50 + case Zipper.trm z
6.51 + of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z)]
6.52 @ here
6.53 - @ [Z.LookIn (Z.move_down_right z)]
6.54 - | Abs _ => here @ [Z.LookIn (Z.move_down_abs z)]
6.55 + @ [Zipper.LookIn (Zipper.move_down_right z)]
6.56 + | Abs _ => here @ [Zipper.LookIn (Zipper.move_down_abs z)]
6.57 | _ => here
6.58 end;
6.59 - in Z.lzy_search sf_valid_td_lr end;
6.60 + in Zipper.lzy_search sf_valid_td_lr end;
6.61
6.62 (* search from bottom to top, left to right *)
6.63
6.64 fun search_bt_valid validf =
6.65 let
6.66 fun sf_valid_td_lr z =
6.67 - let val here = if validf z then [Z.Here z] else [] in
6.68 - case Z.trm z
6.69 - of _ $ _ => [Z.LookIn (Z.move_down_left z),
6.70 - Z.LookIn (Z.move_down_right z)] @ here
6.71 - | Abs _ => [Z.LookIn (Z.move_down_abs z)] @ here
6.72 + let val here = if validf z then [Zipper.Here z] else [] in
6.73 + case Zipper.trm z
6.74 + of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z),
6.75 + Zipper.LookIn (Zipper.move_down_right z)] @ here
6.76 + | Abs _ => [Zipper.LookIn (Zipper.move_down_abs z)] @ here
6.77 | _ => here
6.78 end;
6.79 - in Z.lzy_search sf_valid_td_lr end;
6.80 + in Zipper.lzy_search sf_valid_td_lr end;
6.81
6.82 fun searchf_unify_gen f (sgn, maxidx, z) lhs =
6.83 Seq.map (clean_unify_z sgn maxidx lhs)
6.84 - (Z.limit_apply f z);
6.85 + (Zipper.limit_apply f z);
6.86
6.87 (* search all unifications *)
6.88 val searchf_lr_unify_all =
6.89 @@ -369,9 +366,9 @@
6.90 val conclterm = Logic.strip_imp_concl fixedbody;
6.91 val conclthm = trivify conclterm;
6.92 val maxidx = Thm.maxidx_of th;
6.93 - val ft = ((Z.move_down_right (* ==> *)
6.94 - o Z.move_down_left (* Trueprop *)
6.95 - o Z.mktop
6.96 + val ft = ((Zipper.move_down_right (* ==> *)
6.97 + o Zipper.move_down_left (* Trueprop *)
6.98 + o Zipper.mktop
6.99 o Thm.prop_of) conclthm)
6.100 in
6.101 ((cfvs, conclthm), (sgn, maxidx, ft))
6.102 @@ -487,8 +484,8 @@
6.103 val pth = trivify asmt;
6.104 val maxidx = Thm.maxidx_of th;
6.105
6.106 - val ft = ((Z.move_down_right (* trueprop *)
6.107 - o Z.mktop
6.108 + val ft = ((Zipper.move_down_right (* trueprop *)
6.109 + o Zipper.mktop
6.110 o Thm.prop_of) pth)
6.111 in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
6.112