--- a/src/HOL/Library/old_recdef.ML Fri Jun 19 19:13:15 2015 +0200
+++ b/src/HOL/Library/old_recdef.ML Fri Jun 19 19:29:57 2015 +0200
@@ -293,7 +293,7 @@
val ty_str = case ty of
Type(ty_str, _) => ty_str
| TFree(s,_) => error ("Free type: " ^ s)
- | TVar((s,i),_) => error ("Free variable: " ^ s)
+ | TVar((s,_),_) => error ("Free variable: " ^ s)
val {induct, ...} = BNF_LFP_Compat.the_info thy [BNF_LFP_Compat.Keep_Nesting] ty_str
in
cases_thm_of_induct_thm induct
@@ -316,7 +316,7 @@
val (Pv, Dv, type_insts) =
case (Thm.concl_of case_thm) of
- (_ $ (Pv $ (Dv as Var(D, Dty)))) =>
+ (_ $ (Pv $ (Dv as Var(_, Dty)))) =>
(Pv, Dv,
Sign.typ_match thy (Dty, ty) Vartab.empty)
| _ => error "not a valid case thm";
@@ -342,14 +342,14 @@
fun find_term_split (Free v, _ $ _) = SOME v
| find_term_split (Free v, Const _) = SOME v
| find_term_split (Free v, Abs _) = SOME v (* do we really want this case? *)
- | find_term_split (Free v, Var _) = NONE (* keep searching *)
+ | find_term_split (Free _, Var _) = NONE (* keep searching *)
| find_term_split (a $ b, a2 $ b2) =
(case find_term_split (a, a2) of
NONE => find_term_split (b,b2)
| vopt => vopt)
- | find_term_split (Abs(_,ty,t1), Abs(_,ty2,t2)) =
+ | find_term_split (Abs(_,_,t1), Abs(_,_,t2)) =
find_term_split (t1, t2)
- | find_term_split (Const (x,ty), Const(x2,ty2)) =
+ | find_term_split (Const (x,_), Const(x2,_)) =
if x = x2 then NONE else (* keep searching *)
raise find_split_exp (* stop now *)
"Terms are not identical upto a free varaible! (Consts)"
@@ -422,6 +422,7 @@
end;
+
(*** basic utilities ***)
structure Utils: UTILS =
@@ -433,8 +434,8 @@
fun UTILS_ERR func mesg = ERR {module = "Utils", func = func, mesg = mesg};
-fun end_itlist f [] = raise (UTILS_ERR "end_itlist" "list too short")
- | end_itlist f [x] = x
+fun end_itlist _ [] = raise (UTILS_ERR "end_itlist" "list too short")
+ | end_itlist _ [x] = x
| end_itlist f (x :: xs) = f x (end_itlist f xs);
fun itlist2 f L1 L2 base_value =
@@ -451,7 +452,7 @@
end;
fun take f =
- let fun grab(0,L) = []
+ let fun grab(0, _) = []
| grab(n, x::rst) = f x::grab(n-1,rst)
in grab
end;
@@ -464,6 +465,7 @@
end;
+
(*** emulation of HOL's abstract syntax functions ***)
structure USyntax: USYNTAX =
@@ -492,7 +494,6 @@
fun type_varsl L = distinct (op =) (fold (curry op @ o type_vars) L []);
val alpha = mk_vartype "'a"
-val beta = mk_vartype "'b"
val strip_prod_type = HOLogic.flatten_tupleT;
@@ -597,7 +598,7 @@
| LAMB of {Bvar : term, Body : term};
-fun dest_term(Var((s,i),ty)) = VAR{Name = s, Ty = ty}
+fun dest_term(Var((s,_),ty)) = VAR{Name = s, Ty = ty}
| dest_term(Free(s,ty)) = VAR{Name = s, Ty = ty}
| dest_term(Const(s,ty)) = CONST{Name = s, Ty = ty}
| dest_term(M$N) = COMB{Rator=M,Rand=N}
@@ -783,6 +784,7 @@
end;
+
(*** derived cterm destructors ***)
structure Dcterm: DCTERM =
@@ -835,7 +837,7 @@
fun dest_var ctm =
(case Thm.term_of ctm
- of Var((s,i),ty) => {Name=s, Ty=ty}
+ of Var((s,_),ty) => {Name=s, Ty=ty}
| Free(s,ty) => {Name=s, Ty=ty}
| _ => raise ERR "dest_var" "not a variable");
@@ -927,6 +929,7 @@
end;
+
(*** notable theorems ***)
structure Thms =
@@ -945,6 +948,7 @@
end;
+
(*** emulation of HOL inference rules for TFL ***)
structure Rules: RULES =
@@ -984,7 +988,7 @@
fun rbeta th =
(case Dcterm.strip_comb (cconcl th) of
- (_, [l, r]) => Thm.transitive th (Thm.beta_conversion false r)
+ (_, [_, r]) => Thm.transitive th (Thm.beta_conversion false r)
| _ => raise RULES_ERR "rbeta" "");
@@ -1062,7 +1066,7 @@
local
val prop = Thm.prop_of disjI2
- val [P,Q] = Misc_Legacy.term_vars prop
+ val [P,_] = Misc_Legacy.term_vars prop
val disj2 = Thm.forall_intr (Thm.cterm_of @{context} P) disjI2
in
fun DISJ2 tm thm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj2)
@@ -1141,7 +1145,7 @@
fun eq th atm =
exists (fn t => HOLogic.dest_Trueprop t aconv Thm.term_of atm) (Thm.hyps_of th)
val tml = Dcterm.strip_disj c
- fun DL th [] = raise RULES_ERR "DISJ_CASESL" "no cases"
+ fun DL _ [] = 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) =
@@ -1325,7 +1329,7 @@
fun is_cong thm =
case (Thm.prop_of thm) of
(Const(@{const_name Pure.imp},_)$(Const(@{const_name Trueprop},_)$ _) $
- (Const(@{const_name Pure.eq},_) $ (Const (@{const_name Wfrec.cut},_) $ f $ R $ a $ x) $ _)) =>
+ (Const(@{const_name Pure.eq},_) $ (Const (@{const_name Wfrec.cut},_) $ _ $ _ $ a $ x) $ _)) =>
false
| _ => true;
@@ -1379,9 +1383,9 @@
| get (ant::rst,n,L) =
case (list_break_all ant)
of ([],_) => get (rst, n+1,L)
- | (vlist,body) =>
+ | (_,body) =>
let val eq = Logic.strip_imp_concl body
- val (f,args) = USyntax.strip_comb (get_lhs eq)
+ val (f,_) = USyntax.strip_comb (get_lhs eq)
val (vstrl,_) = USyntax.strip_abs f
val names =
Name.variant_list (Misc_Legacy.add_term_names(body, [])) (map (#1 o dest_Free) vstrl)
@@ -1510,7 +1514,7 @@
*---------------------------------------------------------------------------*)
fun dest_pbeta_redex used M n =
let val (f,args) = dest_combn M n
- val dummy = dest_aabs used f
+ val _ = dest_aabs used f
in (strip_aabs used f,args)
end;
@@ -1534,11 +1538,11 @@
val cut_lemma' = cut_lemma RS eq_reflection
fun prover used ctxt thm =
let fun cong_prover ctxt thm =
- let val dummy = say "cong_prover:"
+ let val _ = say "cong_prover:"
val cntxt = Simplifier.prems_of ctxt
- val dummy = print_thms ctxt "cntxt:" cntxt
- val dummy = say "cong rule:"
- val dummy = say (Display.string_of_thm ctxt thm)
+ val _ = print_thms ctxt "cntxt:" cntxt
+ val _ = say "cong rule:"
+ val _ = say (Display.string_of_thm ctxt thm)
(* Unquantified eliminate *)
fun uq_eliminate (thm,imp) =
let val tych = Thm.cterm_of ctxt
@@ -1557,7 +1561,7 @@
end
fun pq_eliminate (thm, vlist, imp_body, lhs_eq) =
let val ((vstrl, _, used'), args) = dest_pbeta_redex used lhs_eq (length vlist)
- val dummy = forall (op aconv) (ListPair.zip (vlist, args))
+ val _ = forall (op aconv) (ListPair.zip (vlist, args))
orelse error "assertion failed in CONTEXT_REWRITE_RULE"
val imp_body1 = subst_free (ListPair.zip (args, vstrl))
imp_body
@@ -1682,6 +1686,7 @@
end;
+
(*** theory operations ***)
structure Thry: THRY =
@@ -1751,6 +1756,7 @@
end;
+
(*** first part of main module ***)
structure Prim: PRIM =
@@ -1762,7 +1768,6 @@
fun TFL_ERR func mesg = Utils.ERR {module = "Tfl", func = func, mesg = mesg};
val concl = #2 o Rules.dest_thm;
-val hyp = #1 o Rules.dest_thm;
val list_mk_type = Utils.end_itlist (curry (op -->));
@@ -1929,7 +1934,7 @@
fun mk_case_fail s = raise TFL_ERR "mk_case" s
val fresh_var = gvvariant usednames
val divide = partition fresh_var ty_match
- fun expand constructors ty ((_,[]), _) = mk_case_fail"expand_var_row"
+ fun expand _ ty ((_,[]), _) = mk_case_fail"expand_var_row"
| expand constructors ty (row as ((prfx, p::rst), rhs)) =
if (is_Free p)
then let val fresh = fresh_constr ty_match ty fresh_var
@@ -2035,7 +2040,7 @@
val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L)
val atom = single (distinct (op aconv) funcs)
val (fname,ftype) = dest_atom atom
- val dummy = map (no_repeat_vars thy) pats
+ val _ = map (no_repeat_vars thy) pats
val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats,
map_index (fn (i, t) => (t,(i,true))) R)
val names = List.foldr Misc_Legacy.add_term_names [] R
@@ -2052,7 +2057,7 @@
val patts2 = Library.sort (Library.int_ord o apply2 row_of_pat) patts1
val finals = map row_of_pat patts2
val originals = map (row_of_pat o #2) rows
- val dummy = case (subtract (op =) finals originals)
+ val _ = case (subtract (op =) finals originals)
of [] => ()
| L => mk_functional_err
("The following clauses are redundant (covered by preceding clauses): " ^
@@ -2084,7 +2089,7 @@
val 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 _ = dest_Free f
val (wfrec,_) = USyntax.strip_comb rhs
in
@@ -2181,8 +2186,8 @@
let val ctxt = Proof_Context.init_global thy
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 (fname,_) = dest_atom f
+ val (SV,_) = front_last args (* SV = schematic variables *)
val g = list_comb(f,SV)
val h = Free(fname,type_of g)
val eqns1 = map (subst_free[(g,h)]) eqns
@@ -2190,7 +2195,7 @@
val given_pats = givens pats
(* val f = Free(x,Ty) *)
val Type("fun", [f_dty, f_rty]) = Ty
- val dummy = if x<>fid then
+ val _ = if x<>fid then
raise TFL_ERR "wfrec_eqns"
("Expected a definition of " ^
quote fid ^ " but found one of " ^
@@ -2204,7 +2209,7 @@
Rtype)
val WFREC_THM = Rules.ISPECL [tych R, tych g] WFREC_THM0
val ([proto_def, WFR],_) = USyntax.strip_imp(concl WFREC_THM)
- val dummy =
+ val _ =
if !trace then
writeln ("ORIGINAL PROTO_DEF: " ^
Syntax.string_of_term_global thy proto_def)
@@ -2236,7 +2241,7 @@
val R1 = USyntax.rand WFR
val f = #lhs(USyntax.dest_eq proto_def)
val (extractants,TCl) = ListPair.unzip extracta
- val dummy = if !trace
+ val _ = if !trace
then writeln (cat_lines ("Extractants =" ::
map (Display.string_of_thm_global thy) extractants))
else ()
@@ -2245,7 +2250,7 @@
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' = " ^
+ val _ = if !trace then writeln ("proto_def' = " ^
Syntax.string_of_term_global
thy proto_def')
else ()
@@ -2259,7 +2264,7 @@
[Thm.no_attributes (Binding.name (Thm.def_name fid), defn)]
val def = Thm.unvarify_global def0;
val ctxt' = Syntax.init_pretty_global thy';
- val dummy =
+ val _ =
if !trace then writeln ("DEF = " ^ Display.string_of_thm ctxt' def)
else ()
(* val fconst = #lhs(USyntax.dest_eq(concl def)) *)
@@ -2269,8 +2274,7 @@
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 ctxt' baz) else ()
- val f_free = Free (fid, fastype_of f) (*'cos f is a Const*)
+ val _ = if !trace then writeln ("baz = " ^ Display.string_of_thm ctxt' baz) else ()
val SV' = map tych SV;
val SVrefls = map Thm.reflexive SV'
val def0 = (fold (fn x => fn th => Rules.rbeta(Thm.combination th x))
@@ -2428,34 +2432,6 @@
*
* Note. When the context is empty, there can be no local variables.
*---------------------------------------------------------------------------*)
-(*
-local infix 5 ==>
- fun (tm1 ==> tm2) = USyntax.mk_imp{ant = tm1, conseq = tm2}
-in
-fun build_ih f P (pat,TCs) =
- 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) = 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 = 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 [] => (USyntax.list_mk_forall(globals, P$pat), [])
- | _ => let val (ihs, TCs_locals) = ListPair.unzip(map dest_TC TCs)
- 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) = USyntax.mk_imp{ant = tm1, conseq = tm2}
@@ -2717,6 +2693,7 @@
end;
+
(*** second part of main module (postprocessing of TFL definitions) ***)
structure Tfl: TFL =
@@ -2800,7 +2777,7 @@
in
case nested_tcs
of [] => {induction=induction, rules=rules,tcs=[]}
- | L => let val dummy = writeln "Simplifying nested TCs ..."
+ | L => let val _ = writeln "Simplifying nested TCs ..."
val (solved,simplified,stubborn) =
fold_rev (fn th => fn (So,Si,St) =>
if (id_thm th) then (So, Si, th::St) else
@@ -2837,16 +2814,13 @@
val spec'=
Rule_Insts.read_instantiate @{context} [((("x", 0), Position.none), "P::'b=>bool")] [] spec;
-fun tracing true _ = ()
- | tracing false msg = writeln msg;
-
fun simplify_defn ctxt strict congs wfs id pats def0 =
let
val def = Thm.unvarify_global def0 RS meta_eq_to_obj_eq
val {rules, rows, TCs, full_pats_TCs} = Prim.post_definition ctxt congs (def, pats)
val {lhs=f,rhs} = USyntax.dest_eq (concl def)
val (_,[R,_]) = USyntax.strip_comb rhs
- val dummy = Prim.trace_thms ctxt "congs =" congs
+ val _ = Prim.trace_thms ctxt "congs =" congs
(*the next step has caused simplifier looping in some cases*)
val {induction, rules, tcs} =
proof_stage ctxt strict wfs
@@ -2870,8 +2844,8 @@
fun get_related_thms i =
map_filter ((fn (r,x) => if x = i then SOME r else NONE));
- fun solve_eq _ (th, [], i) = error "derive_init_eqs: missing rules"
- | solve_eq _ (th, [a], i) = [(a, i)]
+ fun solve_eq _ (_, [], _) = error "derive_init_eqs: missing rules"
+ | solve_eq _ (_, [a], i) = [(a, i)]
| solve_eq ctxt (th, splitths, i) =
(writeln "Proving unsplit equation...";
[((Drule.export_without_context o Object_Logic.rulify_no_asm ctxt)
@@ -2919,7 +2893,7 @@
let
val {rules,R,theory,full_pats_TCs,SV,...} = Prim.lazyR_def thy fid congs eqs
val f = func_of_cond_eqn (concl (Rules.CONJUNCT1 rules handle Utils.ERR _ => rules));
- val dummy = writeln "Proving induction theorem ...";
+ val _ = writeln "Proving induction theorem ...";
val induction = Prim.mk_induction theory
{fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs}
in
@@ -2936,6 +2910,7 @@
end;
+
(*** wrappers for Isar ***)
(** recdef hints **)