--- a/src/HOL/HOLCF/Tools/Domain/domain.ML Mon Aug 08 16:57:37 2011 -0700
+++ b/src/HOL/HOLCF/Tools/Domain/domain.ML Mon Aug 08 18:36:32 2011 -0700
@@ -35,7 +35,6 @@
fun first (x,_,_) = x
fun second (_,x,_) = x
-fun third (_,_,x) = x
(* ----- calls for building new thy and thms -------------------------------- *)
@@ -78,16 +77,16 @@
(binding * (bool * binding option * 'b) list * mixfix) list list =
map (fn (_,_,_,cons) => cons) raw_specs
val dtnvs' : (string * typ list) list =
- map (fn (dbind, vs, mx) => (Sign.full_name thy dbind, vs)) dtnvs
+ map (fn (dbind, vs, _) => (Sign.full_name thy dbind, vs)) dtnvs
val all_cons = map (Binding.name_of o first) (flat raw_rhss)
- val test_dupl_cons =
+ val _ =
case duplicates (op =) all_cons of
[] => false | dups => error ("Duplicate constructors: "
^ commas_quote dups)
val all_sels =
(map Binding.name_of o map_filter second o maps second) (flat raw_rhss)
- val test_dupl_sels =
+ val _ =
case duplicates (op =) all_sels of
[] => false | dups => error("Duplicate selectors: "^commas_quote dups)
@@ -95,7 +94,7 @@
case duplicates (op =) (map(fst o dest_TFree)s) of
[] => false | dups => error("Duplicate type arguments: "
^commas_quote dups)
- val test_dupl_tvars' = exists test_dupl_tvars (map snd dtnvs')
+ val _ = exists test_dupl_tvars (map snd dtnvs')
val sorts : (string * sort) list =
let val all_sorts = map (map dest_TFree o snd) dtnvs'
@@ -119,7 +118,7 @@
non-pcpo-types and invalid use of recursive type
replace sorts in type variables on rhs *)
val rec_tab = Domain_Take_Proofs.get_rec_tab thy
- fun check_rec no_rec (T as TFree (v,_)) =
+ fun check_rec _ (T as TFree (v,_)) =
if AList.defined (op =) sorts v then T
else error ("Free type variable " ^ quote v ^ " on rhs.")
| check_rec no_rec (T as Type (s, Ts)) =
@@ -141,7 +140,7 @@
error ("Illegal indirect recursion of type " ^
quote (Syntax.string_of_typ_global tmp_thy T) ^
" under type constructor " ^ quote c)))
- | check_rec no_rec (TVar _) = error "extender:check_rec"
+ | check_rec _ (TVar _) = error "extender:check_rec"
fun prep_arg (lazy, sel, raw_T) =
let
@@ -154,8 +153,8 @@
val rhss : (binding * (bool * binding option * typ) list * mixfix) list list =
map prep_rhs raw_rhss
- fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_upT T else T
- fun mk_con_typ (bind, args, mx) =
+ fun mk_arg_typ (lazy, _, T) = if lazy then mk_upT T else T
+ fun mk_con_typ (_, args, _) =
if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args)
fun mk_rhs_typ cons = foldr1 mk_ssumT (map mk_con_typ cons)
@@ -174,7 +173,7 @@
Domain_Constructors.add_domain_constructors dbind cons info)
(dbinds ~~ rhss ~~ iso_infos)
- val (take_rews, thy) =
+ val (_, thy) =
Domain_Induction.comp_theorems
dbinds take_info constr_infos thy
in
@@ -184,7 +183,7 @@
fun define_isos (spec : (binding * mixfix * (typ * typ)) list) =
let
fun prep (dbind, mx, (lhsT, rhsT)) =
- let val (dname, vs) = dest_Type lhsT
+ let val (_, vs) = dest_Type lhsT
in (map (fst o dest_TFree) vs, dbind, mx, rhsT, NONE) end
in
Domain_Isomorphism.domain_isomorphism (map prep spec)
--- a/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML Mon Aug 08 16:57:37 2011 -0700
+++ b/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML Mon Aug 08 18:36:32 2011 -0700
@@ -127,7 +127,7 @@
(dbinds ~~ iso_infos) take_info lub_take_thms thy
(* define map functions *)
- val (map_info, thy) =
+ val (_, thy) =
Domain_Isomorphism.define_map_functions
(dbinds ~~ iso_infos) thy
--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Mon Aug 08 16:57:37 2011 -0700
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Mon Aug 08 18:36:32 2011 -0700
@@ -80,9 +80,9 @@
fun mk_decl (b, t, mx) = (b, fastype_of t, mx)
val decls = map mk_decl specs
val thy = Cont_Consts.add_consts decls thy
- fun mk_const (b, T, mx) = Const (Sign.full_name thy b, T)
+ fun mk_const (b, T, _) = Const (Sign.full_name thy b, T)
val consts = map mk_const decls
- fun mk_def c (b, t, mx) =
+ fun mk_def c (b, t, _) =
(Binding.suffix_name "_def" b, Logic.mk_equals (c, t))
val defs = map2 mk_def consts specs
val (def_thms, thy) =
@@ -159,7 +159,7 @@
val abs_strict = iso_locale RS @{thm iso.abs_strict}
(* get types of type isomorphism *)
- val (rhsT, lhsT) = dest_cfunT (fastype_of abs_const)
+ val (_, lhsT) = dest_cfunT (fastype_of abs_const)
fun vars_of args =
let
@@ -172,7 +172,7 @@
(* define constructor functions *)
val ((con_consts, con_defs), thy) =
let
- fun one_arg (lazy, T) var = if lazy then mk_up var else var
+ fun one_arg (lazy, _) var = if lazy then mk_up var else var
fun one_con (_,args,_) = mk_stuple (map2 one_arg args (vars_of args))
fun mk_abs t = abs_const ` t
val rhss = map mk_abs (mk_sinjects (map one_con spec))
@@ -187,13 +187,13 @@
(* replace bindings with terms in constructor spec *)
val spec' : (term * (bool * typ) list) list =
- let fun one_con con (b, args, mx) = (con, args)
+ let fun one_con con (_, args, _) = (con, args)
in map2 one_con con_consts spec end
(* prove exhaustiveness of constructors *)
local
- fun arg2typ n (true, T) = (n+1, mk_upT (TVar (("'a", n), @{sort cpo})))
- | arg2typ n (false, T) = (n+1, TVar (("'a", n), @{sort pcpo}))
+ fun arg2typ n (true, _) = (n+1, mk_upT (TVar (("'a", n), @{sort cpo})))
+ | arg2typ n (false, _) = (n+1, TVar (("'a", n), @{sort pcpo}))
fun args2typ n [] = (n, oneT)
| args2typ n [arg] = arg2typ n arg
| args2typ n (arg::args) =
@@ -332,14 +332,14 @@
| prime t = t
fun iff_disj (t, []) = mk_not t
| iff_disj (t, ts) = mk_eq (t, foldr1 mk_disj ts)
- fun iff_disj2 (t, [], us) = mk_not t
- | iff_disj2 (t, ts, []) = mk_not t
+ fun iff_disj2 (t, [], _) = mk_not t
+ | iff_disj2 (t, _, []) = mk_not t
| iff_disj2 (t, ts, us) =
mk_eq (t, mk_conj (foldr1 mk_disj ts, foldr1 mk_disj us))
fun dist_le (con1, args1) (con2, args2) =
let
val (vs1, zs1) = get_vars args1
- val (vs2, zs2) = get_vars args2 |> pairself (map prime)
+ val (vs2, _) = get_vars args2 |> pairself (map prime)
val lhs = mk_below (list_ccomb (con1, vs1), list_ccomb (con2, vs2))
val rhss = map mk_undef zs1
val goal = mk_trp (iff_disj (lhs, rhss))
@@ -390,7 +390,6 @@
(lhsT : typ)
(dbind : binding)
(con_betas : thm list)
- (exhaust : thm)
(iso_locale : thm)
(rep_const : term)
(thy : theory)
@@ -429,7 +428,7 @@
| mk_sscases ts = foldr1 mk_sscase ts
val body = mk_sscases (map2 one_con fs spec)
val rhs = big_lambdas fs (mk_cfcomp (body, rep_const))
- val ((case_consts, case_defs), thy) =
+ val ((_, case_defs), thy) =
define_consts [(case_bind, rhs, NoSyn)] thy
val case_name = Sign.full_name thy case_bind
in
@@ -457,7 +456,7 @@
Library.foldl capp (c_ast authentic con, argvars n args)
fun case1 authentic (n, c) =
app "_case1" (Ast.strip_positions (con1 authentic n c), expvar n)
- fun arg1 (n, (con,args)) = List.foldr cabs (expvar n) (argvars n args)
+ fun arg1 (n, (_, args)) = List.foldr cabs (expvar n) (argvars n args)
fun when1 n (m, c) = if n = m then arg1 (n, c) else Ast.Constant @{const_syntax bottom}
val case_constant = Ast.Constant (syntax (case_const dummyT))
fun case_trans authentic =
@@ -541,16 +540,16 @@
fun mk_ssnd s = mk_cfcomp (ssnd_const (dest_sprodT (rangeT s)), s)
fun mk_down s = mk_cfcomp (from_up (dest_upT (rangeT s)), s)
- fun sels_of_arg s (lazy, NONE, T) = []
- | sels_of_arg s (lazy, SOME b, T) =
+ fun sels_of_arg _ (_, NONE, _) = []
+ | sels_of_arg s (lazy, SOME b, _) =
[(b, if lazy then mk_down s else s, NoSyn)]
- fun sels_of_args s [] = []
+ fun sels_of_args _ [] = []
| sels_of_args s (v :: []) = sels_of_arg s v
| sels_of_args s (v :: vs) =
sels_of_arg (mk_sfst s) v @ sels_of_args (mk_ssnd s) vs
- fun sels_of_cons s [] = []
- | sels_of_cons s ((con, args) :: []) = sels_of_args s args
- | sels_of_cons s ((con, args) :: cs) =
+ fun sels_of_cons _ [] = []
+ | sels_of_cons s ((_, args) :: []) = sels_of_args s args
+ | sels_of_cons s ((_, args) :: cs) =
sels_of_args (mk_outl s) args @ sels_of_cons (mk_outr s) cs
val sel_eqns : (binding * term * mixfix) list =
sels_of_cons rep_const spec
@@ -598,7 +597,7 @@
val vs : term list = map Free (ns ~~ Ts)
val con_app : term = list_ccomb (con, vs)
val vs' : (bool * term) list = map #1 args ~~ vs
- fun one_same (n, sel, T) =
+ fun one_same (n, sel, _) =
let
val xs = map snd (filter_out fst (nth_drop n vs'))
val assms = map (mk_trp o mk_defined) xs
@@ -607,7 +606,7 @@
in
prove thy defs goal (K tacs)
end
- fun one_diff (n, sel, T) =
+ fun one_diff (_, sel, T) =
let
val goal = mk_trp (mk_eq (sel ` con_app, mk_bottom T))
in
@@ -615,8 +614,8 @@
end
fun one_con (j, (_, args')) : thm list =
let
- fun prep (i, (lazy, NONE, T)) = NONE
- | prep (i, (lazy, SOME sel, T)) = SOME (i, sel, T)
+ fun prep (_, (_, NONE, _)) = NONE
+ | prep (i, (_, SOME sel, T)) = SOME (i, sel, T)
val sels : (int * term * typ) list =
map_filter prep (map_index I args')
in
@@ -646,12 +645,12 @@
in
prove thy sel_defs goal (K tacs)
end
- fun one_arg (false, SOME sel, T) = SOME (sel_defin sel)
+ fun one_arg (false, SOME sel, _) = SOME (sel_defin sel)
| one_arg _ = NONE
in
case spec2 of
- [(con, args)] => map_filter one_arg args
- | _ => []
+ [(_, args)] => map_filter one_arg args
+ | _ => []
end
in
@@ -672,19 +671,11 @@
(thy : theory) =
let
- fun vars_of args =
- let
- val Ts = map snd args
- val ns = Datatype_Prop.make_tnames Ts
- in
- map Free (ns ~~ Ts)
- end
-
(* define discriminator functions *)
local
- fun dis_fun i (j, (con, args)) =
+ fun dis_fun i (j, (_, args)) =
let
- val (vs, nonlazy) = get_vars args
+ val (vs, _) = get_vars args
val tr = if i = j then @{term TT} else @{term FF}
in
big_lambdas vs tr
@@ -758,7 +749,6 @@
(bindings : binding list)
(spec : (term * (bool * typ) list) list)
(lhsT : typ)
- (exhaust : thm)
(case_const : typ -> term)
(case_rews : thm list)
(thy : theory) =
@@ -776,13 +766,13 @@
val x = Free ("x", lhsT)
fun k args = Free ("k", map snd args -->> mk_matchT resultT)
val fail = mk_fail resultT
- fun mat_fun i (j, (con, args)) =
+ fun mat_fun i (j, (_, args)) =
let
- val (vs, nonlazy) = get_vars_avoiding ["x","k"] args
+ val (vs, _) = get_vars_avoiding ["x","k"] args
in
if i = j then k args else big_lambdas vs fail
end
- fun mat_eqn (i, (bind, (con, args))) : binding * term * mixfix =
+ fun mat_eqn (i, (bind, (_, args))) : binding * term * mixfix =
let
val mat_bind = Binding.prefix_name "match_" bind
val funs = map_index (mat_fun i) spec
@@ -866,7 +856,6 @@
val rep_strict = iso_locale RS @{thm iso.rep_strict}
val abs_strict = iso_locale RS @{thm iso.abs_strict}
val rep_bottom_iff = iso_locale RS @{thm iso.rep_bottom_iff}
- val abs_bottom_iff = iso_locale RS @{thm iso.abs_bottom_iff}
val iso_rews = [abs_iso_thm, rep_iso_thm, abs_strict, rep_strict]
(* qualify constants and theorems with domain name *)
@@ -875,7 +864,7 @@
(* define constructor functions *)
val (con_result, thy) =
let
- fun prep_arg (lazy, sel, T) = (lazy, T)
+ fun prep_arg (lazy, _, T) = (lazy, T)
fun prep_con (b, args, mx) = (b, map prep_arg args, mx)
val con_spec = map prep_con spec
in
@@ -887,8 +876,8 @@
(* prepare constructor spec *)
val con_specs : (term * (bool * typ) list) list =
let
- fun prep_arg (lazy, sel, T) = (lazy, T)
- fun prep_con c (b, args, mx) = (c, map prep_arg args)
+ fun prep_arg (lazy, _, T) = (lazy, T)
+ fun prep_con c (_, args, _) = (c, map prep_arg args)
in
map2 prep_con con_consts spec
end
@@ -896,13 +885,13 @@
(* define case combinator *)
val ((case_const : typ -> term, cases : thm list), thy) =
add_case_combinator con_specs lhsT dbind
- con_betas exhaust iso_locale rep_const thy
+ con_betas iso_locale rep_const thy
(* define and prove theorems for selector functions *)
val (sel_thms : thm list, thy : theory) =
let
val sel_spec : (term * (bool * binding option * typ) list) list =
- map2 (fn con => fn (b, args, mx) => (con, args)) con_consts spec
+ map2 (fn con => fn (_, args, _) => (con, args)) con_consts spec
in
add_selectors sel_spec rep_const
abs_iso_thm rep_strict rep_bottom_iff con_betas thy
@@ -916,7 +905,7 @@
(* define and prove theorems for match combinators *)
val (match_thms : thm list, thy : theory) =
add_match_combinators bindings con_specs lhsT
- exhaust case_const cases thy
+ case_const cases thy
(* restore original signature path *)
val thy = Sign.parent_path thy
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Mon Aug 08 16:57:37 2011 -0700
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Mon Aug 08 18:36:32 2011 -0700
@@ -221,7 +221,7 @@
if length dnames = 1 then ["bottom"] else
map (fn s => "bottom_" ^ Long_Name.base_name s) dnames
fun one_eq bot (constr_info : Domain_Constructors.constr_info) =
- let fun name_of (c, args) = Long_Name.base_name (fst (dest_Const c))
+ let fun name_of (c, _) = Long_Name.base_name (fst (dest_Const c))
in bot :: map name_of (#con_specs constr_info) end
in adms @ flat (map2 one_eq bottoms constr_infos) end
@@ -344,7 +344,7 @@
val assm1 = mk_trp (list_comb (bisim_const, Rs))
val assm2 = mk_trp (R $ x $ y)
val goal = mk_trp (mk_eq (x, y))
- fun tacf {prems, context} =
+ fun tacf {prems, context = _} =
let
val rule = hd prems RS coind_lemma
in
@@ -420,7 +420,7 @@
val (take_rewss, thy) =
take_theorems dbinds take_info constr_infos thy
-val {take_lemma_thms, take_0_thms, take_strict_thms, ...} = take_info
+val {take_0_thms, take_strict_thms, ...} = take_info
val take_rews = take_0_thms @ take_strict_thms @ flat take_rewss
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Aug 08 16:57:37 2011 -0700
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Aug 08 18:36:32 2011 -0700
@@ -86,15 +86,6 @@
fun mk_u_defl t = mk_capply (@{const "u_defl"}, t)
-fun mk_u_map t =
- let
- val (T, U) = dest_cfunT (fastype_of t)
- val u_map_type = (T ->> U) ->> (mk_upT T ->> mk_upT U)
- val u_map_const = Const (@{const_name u_map}, u_map_type)
- in
- mk_capply (u_map_const, t)
- end
-
fun emb_const T = Const (@{const_name emb}, T ->> udomT)
fun prj_const T = Const (@{const_name prj}, udomT ->> T)
fun coerce_const (T, U) = mk_cfcomp (prj_const U, emb_const T)
@@ -130,7 +121,7 @@
(*************** fixed-point definitions and unfolding theorems ***************)
(******************************************************************************)
-fun mk_projs [] t = []
+fun mk_projs [] _ = []
| mk_projs (x::[]) t = [(x, t)]
| mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t)
@@ -187,7 +178,7 @@
(@{thm def_cont_fix_eq} OF [tuple_fixdef_thm, cont_thm])
|> Local_Defs.unfold (Proof_Context.init_global thy) @{thms split_conv}
- fun mk_unfold_thms [] thm = []
+ fun mk_unfold_thms [] _ = []
| mk_unfold_thms (n::[]) thm = [(n, thm)]
| mk_unfold_thms (n::ns) thm = let
val thmL = thm RS @{thm Pair_eqD1}
@@ -271,7 +262,7 @@
| mapT T = T ->> T
(* declare map functions *)
- fun declare_map_const (tbind, (lhsT, rhsT)) thy =
+ fun declare_map_const (tbind, (lhsT, _)) thy =
let
val map_type = mapT lhsT
val map_bind = Binding.suffix_name "_map" tbind
@@ -290,7 +281,7 @@
val tab1 = map map_lhs (map_consts ~~ map fst dom_eqns)
val Ts = (snd o dest_Type o fst o hd) dom_eqns
val tab = (Ts ~~ map mapvar Ts) @ tab1
- fun mk_map_spec (((rep_const, abs_const), map_const), (lhsT, rhsT)) =
+ fun mk_map_spec (((rep_const, abs_const), _), (lhsT, rhsT)) =
let
val lhs = Domain_Take_Proofs.map_of_typ thy tab lhsT
val body = Domain_Take_Proofs.map_of_typ thy tab rhsT
@@ -313,7 +304,7 @@
fun unprime a = Library.unprefix "'" a
fun mk_f T = Free (unprime (fst (dest_TFree T)), T ->> T)
fun mk_assm T = mk_trp (mk_deflation (mk_f T))
- fun mk_goal (map_const, (lhsT, rhsT)) =
+ fun mk_goal (map_const, (lhsT, _)) =
let
val (_, Ts) = dest_Type lhsT
val map_term = list_ccomb (map_const, map mk_f (filter (is_cpo thy) Ts))
@@ -343,7 +334,7 @@
REPEAT (etac @{thm conjE} 1),
REPEAT (resolve_tac (deflation_rules @ prems) 1 ORELSE atac 1)])
end
- fun conjuncts [] thm = []
+ fun conjuncts [] _ = []
| conjuncts (n::[]) thm = [(n, thm)]
| conjuncts (n::ns) thm = let
val thmL = thm RS @{thm conjunct1}
@@ -360,7 +351,6 @@
fun register_map (dname, args) =
Domain_Take_Proofs.add_rec_type (dname, args)
val dnames = map (fst o dest_Type o fst) dom_eqns
- val map_names = map (fst o dest_Const) map_consts
fun args (T, _) = case T of Type (_, Ts) => map (is_cpo thy) Ts | _ => []
val argss = map args dom_eqns
in
@@ -417,7 +407,7 @@
(* this theory is used just for parsing *)
val tmp_thy = thy |>
Theory.copy |>
- Sign.add_types_global (map (fn (tvs, tbind, mx, _, morphs) =>
+ Sign.add_types_global (map (fn (tvs, tbind, mx, _, _) =>
(tbind, length tvs, mx)) doms_raw)
fun prep_dom thy (vs, t, mx, typ_raw, morphs) sorts =
@@ -434,28 +424,28 @@
(* declare arities in temporary theory *)
val tmp_thy =
let
- fun arity (vs, tbind, mx, _, _) =
+ fun arity (vs, tbind, _, _, _) =
(Sign.full_name thy tbind, map the_sort vs, @{sort "domain"})
in
fold AxClass.axiomatize_arity (map arity doms) tmp_thy
end
(* check bifiniteness of right-hand sides *)
- fun check_rhs (vs, tbind, mx, rhs, morphs) =
+ fun check_rhs (_, _, _, rhs, _) =
if Sign.of_sort tmp_thy (rhs, @{sort "domain"}) then ()
else error ("Type not of sort domain: " ^
quote (Syntax.string_of_typ_global tmp_thy rhs))
val _ = map check_rhs doms
(* domain equations *)
- fun mk_dom_eqn (vs, tbind, mx, rhs, morphs) =
+ fun mk_dom_eqn (vs, tbind, _, rhs, _) =
let fun arg v = TFree (v, the_sort v)
in (Type (Sign.full_name tmp_thy tbind, map arg vs), rhs) end
val dom_eqns = map mk_dom_eqn doms
(* check for valid type parameters *)
val (tyvars, _, _, _, _) = hd doms
- val new_doms = map (fn (tvs, tname, mx, _, _) =>
+ val _ = map (fn (tvs, tname, _, _, _) =>
let val full_tname = Sign.full_name tmp_thy tname
in
(case duplicates (op =) tvs of
@@ -528,7 +518,7 @@
fun make_repdef ((vs, tbind, mx, _, _), defl) thy =
let
val spec = (tbind, map (rpair dummyS) vs, mx)
- val ((_, _, _, {DEFL, liftemb_def, liftprj_def, ...}), thy) =
+ val ((_, _, _, {DEFL, ...}), thy) =
Domaindef.add_domaindef false NONE spec defl NONE thy
(* declare domain_defl_simps rules *)
val thy = Context.theory_map (RepData.add_thm DEFL) thy
@@ -557,7 +547,7 @@
(DEFL_eq_binds ~~ DEFL_eq_thms)
(* define rep/abs functions *)
- fun mk_rep_abs ((tbind, morphs), (lhsT, rhsT)) thy =
+ fun mk_rep_abs ((tbind, _), (lhsT, rhsT)) thy =
let
val rep_bind = Binding.suffix_name "_rep" tbind
val abs_bind = Binding.suffix_name "_abs" tbind
@@ -611,8 +601,7 @@
(* definitions and proofs related to map functions *)
val (map_info, thy) =
define_map_functions (dbinds ~~ iso_infos) thy
- val { map_consts, map_apply_thms, map_unfold_thms,
- map_cont_thm, deflation_map_thms } = map_info
+ val { map_consts, map_apply_thms, map_cont_thm, ...} = map_info
(* prove isodefl rules for map functions *)
val isodefl_thm =
@@ -627,7 +616,7 @@
| NONE =>
let val T = dest_DEFL t
in mk_trp (isodefl_const T $ mk_f T $ mk_d T) end
- fun mk_goal (map_const, (T, rhsT)) =
+ fun mk_goal (map_const, (T, _)) =
let
val (_, Ts) = dest_Type T
val map_term = list_ccomb (map_const, map mk_f (filter (is_cpo thy) Ts))
@@ -662,7 +651,7 @@
REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)])
end
val isodefl_binds = map (Binding.prefix_name "isodefl_") dbinds
- fun conjuncts [] thm = []
+ fun conjuncts [] _ = []
| conjuncts (n::[]) thm = [(n, thm)]
| conjuncts (n::ns) thm = let
val thmL = thm RS @{thm conjunct1}
@@ -709,7 +698,7 @@
let
val lhs = mk_tuple (map mk_lub take_consts)
fun is_cpo T = Sign.of_sort thy (T, @{sort cpo})
- fun mk_map_ID (map_const, (lhsT, rhsT)) =
+ fun mk_map_ID (map_const, (lhsT, _)) =
list_ccomb (map_const, map mk_ID (filter is_cpo (snd (dest_Type lhsT))))
val rhs = mk_tuple (map mk_map_ID (map_consts ~~ dom_eqns))
val goal = mk_trp (mk_eq (lhs, rhs))
@@ -736,7 +725,7 @@
end
(* prove lub of take equals ID *)
- fun prove_lub_take (((dbind, take_const), map_ID_thm), (lhsT, rhsT)) thy =
+ fun prove_lub_take (((dbind, take_const), map_ID_thm), (lhsT, _)) thy =
let
val n = Free ("n", natT)
val goal = mk_eqs (mk_lub (lambda n (take_const $ n)), mk_ID lhsT)
--- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Mon Aug 08 16:57:37 2011 -0700
+++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Mon Aug 08 18:36:32 2011 -0700
@@ -159,10 +159,6 @@
infix -->>
infix 9 `
-fun mapT (T as Type (_, Ts)) =
- (map (fn T => T ->> T) Ts) -->> (T ->> T)
- | mapT T = T ->> T
-
fun mk_deflation t =
Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t
@@ -227,7 +223,7 @@
val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos
val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos
- fun mk_projs [] t = []
+ fun mk_projs [] _ = []
| mk_projs (x::[]) t = [(x, t)]
| mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t)
@@ -239,7 +235,7 @@
val copy_arg_type = mk_tupleT (map (fn T => T ->> T) newTs)
val copy_arg = Free ("f", copy_arg_type)
val copy_args = map snd (mk_projs dbinds copy_arg)
- fun one_copy_rhs (rep_abs, (lhsT, rhsT)) =
+ fun one_copy_rhs (rep_abs, (_, rhsT)) =
let
val body = map_of_typ thy (newTs ~~ copy_args) rhsT
in
@@ -257,7 +253,7 @@
end
(* define take constants *)
- fun define_take_const ((dbind, take_rhs), (lhsT, rhsT)) thy =
+ fun define_take_const ((dbind, take_rhs), (lhsT, _)) thy =
let
val take_type = HOLogic.natT --> lhsT ->> lhsT
val take_bind = Binding.suffix_name "_take" dbind
@@ -285,7 +281,7 @@
fold_map prove_chain_take (take_consts ~~ dbinds) thy
(* prove take_0 lemmas *)
- fun prove_take_0 ((take_const, dbind), (lhsT, rhsT)) thy =
+ fun prove_take_0 ((take_const, dbind), (lhsT, _)) thy =
let
val lhs = take_const $ @{term "0::nat"}
val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT))
@@ -302,7 +298,7 @@
val n = Free ("n", natT)
val take_is = map (fn t => t $ n) take_consts
fun prove_take_Suc
- (((take_const, rep_abs), dbind), (lhsT, rhsT)) thy =
+ (((take_const, rep_abs), dbind), (_, rhsT)) thy =
let
val lhs = take_const $ (@{term Suc} $ n)
val body = map_of_typ thy (newTs ~~ take_is) rhsT
@@ -326,9 +322,6 @@
val n = Free ("n", natT)
fun mk_goal take_const = mk_deflation (take_const $ n)
val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts))
- val adm_rules =
- @{thms adm_conj adm_subst [OF _ adm_deflation]
- cont2cont_fst cont2cont_snd cont_id}
val bottom_rules =
take_0_thms @ @{thms deflation_bottom simp_thms}
val deflation_rules =
@@ -345,7 +338,7 @@
ORELSE resolve_tac deflation_rules 1
ORELSE atac 1)])
end
- fun conjuncts [] thm = []
+ fun conjuncts [] _ = []
| conjuncts (n::[]) thm = [(n, thm)]
| conjuncts (n::ns) thm = let
val thmL = thm RS @{thm conjunct1}
@@ -378,7 +371,7 @@
in
add_qualified_thm "take_take" (dbind, take_take_thm) thy
end
- val (take_take_thms, thy) =
+ val (_, thy) =
fold_map prove_take_take
(chain_take_thms ~~ deflation_take_thms ~~ dbinds) thy
@@ -391,12 +384,12 @@
in
add_qualified_thm "take_below" (dbind, take_below_thm) thy
end
- val (take_below_thms, thy) =
+ val (_, thy) =
fold_map prove_take_below
(deflation_take_thms ~~ dbinds) thy
(* define finiteness predicates *)
- fun define_finite_const ((dbind, take_const), (lhsT, rhsT)) thy =
+ fun define_finite_const ((dbind, take_const), (lhsT, _)) thy =
let
val finite_type = lhsT --> boolT
val finite_bind = Binding.suffix_name "_finite" dbind
@@ -517,8 +510,7 @@
val iso_infos = map snd spec
val absTs = map #absT iso_infos
val repTs = map #repT iso_infos
- val {take_consts, take_0_thms, take_Suc_thms, ...} = take_info
- val {chain_take_thms, deflation_take_thms, ...} = take_info
+ val {chain_take_thms, ...} = take_info
(* prove take lemmas *)
fun prove_take_lemma ((chain_take, lub_take), dbind) thy =
@@ -553,12 +545,12 @@
and finite' d (Type (c, Ts)) =
let val d' = d andalso member (op =) types c
in forall (finite d') Ts end
- | finite' d _ = true
+ | finite' _ _ = true
in
val is_finite = forall (finite true) repTs
end
- val ((finite_thms, take_induct_thms), thy) =
+ val ((_, take_induct_thms), thy) =
if is_finite
then
let
--- a/src/HOL/HOLCF/Tools/cont_proc.ML Mon Aug 08 16:57:37 2011 -0700
+++ b/src/HOL/HOLCF/Tools/cont_proc.ML Mon Aug 08 18:36:32 2011 -0700
@@ -102,7 +102,7 @@
fun new_cont_tac f' i =
case all_cont_thms f' of
[] => no_tac
- | (c::cs) => rtac c i
+ | (c::_) => rtac c i
fun cont_tac_of_term (Const (@{const_name cont}, _) $ f) =
let
--- a/src/HOL/HOLCF/Tools/cpodef.ML Mon Aug 08 16:57:37 2011 -0700
+++ b/src/HOL/HOLCF/Tools/cpodef.ML Mon Aug 08 18:36:32 2011 -0700
@@ -154,10 +154,7 @@
(* prepare_cpodef *)
-fun declare_type_name a =
- Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)))
-
-fun prepare prep_term name (tname, raw_args, mx) raw_set opt_morphs thy =
+fun prepare prep_term name (tname, raw_args, _) raw_set opt_morphs thy =
let
val _ = Theory.requires thy "Cpodef" "cpodefs"
@@ -186,7 +183,7 @@
fun add_podef def opt_name typ set opt_morphs tac thy =
let
val name = the_default (#1 typ) opt_name
- val ((full_tname, info as ({Rep_name, ...}, {type_definition, set_def, ...})), thy) = thy
+ val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) = thy
|> Typedef.add_typedef_global def opt_name typ set opt_morphs tac
val oldT = #rep_type (#1 info)
val newT = #abs_type (#1 info)
@@ -216,7 +213,7 @@
(thy: theory)
: term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info) * theory) =
let
- val (newT, oldT, set, morphs as (Rep_name, Abs_name)) =
+ val (newT, oldT, set, morphs) =
prepare prep_term name typ raw_set opt_morphs thy
val goal_nonempty =
@@ -249,7 +246,7 @@
(thy: theory)
: term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory) =
let
- val (newT, oldT, set, morphs as (Rep_name, Abs_name)) =
+ val (newT, oldT, set, morphs) =
prepare prep_term name typ raw_set opt_morphs thy
val goal_bottom_mem =
--- a/src/HOL/HOLCF/Tools/domaindef.ML Mon Aug 08 16:57:37 2011 -0700
+++ b/src/HOL/HOLCF/Tools/domaindef.ML Mon Aug 08 18:36:32 2011 -0700
@@ -76,14 +76,11 @@
(* proving class instances *)
-fun declare_type_name a =
- Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)))
-
fun gen_add_domaindef
(prep_term: Proof.context -> 'a -> term)
(def: bool)
(name: binding)
- (typ as (tname, raw_args, mx) : binding * (string * sort) list * mixfix)
+ (typ as (tname, raw_args, _) : binding * (string * sort) list * mixfix)
(raw_defl: 'a)
(opt_morphs: (binding * binding) option)
(thy: theory)
@@ -104,7 +101,6 @@
(*lhs*)
val lhs_tfrees = map (Proof_Context.check_tfree tmp_ctxt) raw_args
- val lhs_sorts = map snd lhs_tfrees
val full_tname = Sign.full_name thy tname
val newT = Type (full_tname, map TFree lhs_tfrees)
--- a/src/HOL/HOLCF/Tools/fixrec.ML Mon Aug 08 16:57:37 2011 -0700
+++ b/src/HOL/HOLCF/Tools/fixrec.ML Mon Aug 08 18:36:32 2011 -0700
@@ -28,8 +28,6 @@
val def_cont_fix_ind = @{thm def_cont_fix_ind}
fun fixrec_err s = error ("fixrec definition error:\n" ^ s)
-fun fixrec_eq_err thy s eq =
- fixrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq))
(*************************************************************************)
(***************************** building types ****************************)
@@ -41,13 +39,10 @@
| binder_cfun (Type(@{type_name "fun"},[T, U])) = T :: binder_cfun U
| binder_cfun _ = []
-fun body_cfun (Type(@{type_name cfun},[T, U])) = body_cfun U
- | body_cfun (Type(@{type_name "fun"},[T, U])) = body_cfun U
+fun body_cfun (Type(@{type_name cfun},[_, U])) = body_cfun U
+ | body_cfun (Type(@{type_name "fun"},[_, U])) = body_cfun U
| body_cfun T = T
-fun strip_cfun T : typ list * typ =
- (binder_cfun T, body_cfun T)
-
in
fun matcherT (T, U) =
@@ -65,10 +60,9 @@
fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t)
(* similar to Thm.head_of, but for continuous application *)
-fun chead_of (Const(@{const_name Rep_cfun},_)$f$t) = chead_of f
+fun chead_of (Const(@{const_name Rep_cfun},_)$f$_) = chead_of f
| chead_of u = u
-infix 0 == val (op ==) = Logic.mk_equals
infix 1 === val (op ===) = HOLogic.mk_eq
fun mk_mplus (t, u) =
@@ -102,8 +96,8 @@
local
-fun name_of (Const (n, T)) = n
- | name_of (Free (n, T)) = n
+fun name_of (Const (n, _)) = n
+ | name_of (Free (n, _)) = n
| name_of t = raise TERM ("Fixrec.add_unfold: lhs not a constant", [t])
val lhs_name =
@@ -145,7 +139,7 @@
Goal.prove lthy [] [] prop (K tac)
end
- fun one_def (l as Free(n,_)) r =
+ fun one_def (Free(n,_)) r =
let val b = Long_Name.base_name n
in ((Binding.name (b^"_def"), []), r) end
| one_def _ _ = fixrec_err "fixdefs: lhs not of correct form"
@@ -164,7 +158,7 @@
|> Local_Defs.unfold lthy @{thms split_paired_all split_conv split_strict}
val tuple_unfold_thm = (def_cont_fix_eq OF [tuple_fixdef_thm, cont_thm])
|> Local_Defs.unfold lthy @{thms split_conv}
- fun unfolds [] thm = []
+ fun unfolds [] _ = []
| unfolds (n::[]) thm = [(n, thm)]
| unfolds (n::ns) thm = let
val thmL = thm RS @{thm Pair_eqD1}
@@ -184,7 +178,7 @@
in
((thm_name, [src]), [thm])
end
- val (thmss, lthy) = lthy
+ val (_, lthy) = lthy
|> fold_map Local_Theory.note (induct_note :: map unfold_note unfold_thms)
in
(lthy, names, fixdef_thms, map snd unfold_thms)
@@ -303,7 +297,7 @@
else HOLogic.dest_Trueprop (Logic.strip_imp_concl t)
fun tac (t, i) =
let
- val (c, T) =
+ val (c, _) =
(dest_Const o head_of o chead_of o fst o HOLogic.dest_eq o concl) t
val unfold_thm = the (Symtab.lookup tab c)
val rule = unfold_thm RS @{thm ssubst_lhs}
@@ -346,7 +340,7 @@
val chead_of_spec =
chead_of o fst o dest_eqs o Logic.strip_imp_concl o strip_alls o snd
fun name_of (Free (n, _)) = n
- | name_of t = fixrec_err ("unknown term")
+ | name_of _ = fixrec_err ("unknown term")
val all_names = map (name_of o chead_of_spec) spec
val names = distinct (op =) all_names
fun block_of_name n =
@@ -362,7 +356,7 @@
val matches = map (compile_eqs match_name) (map (map (snd o fst)) blocks)
val spec' = map (pair Attrib.empty_binding) matches
- val (lthy, cnames, fixdef_thms, unfold_thms) =
+ val (lthy, _, _, unfold_thms) =
add_fixdefs fixes spec' lthy
val blocks' = map (map fst o filter_out snd) blocks
--- a/src/HOL/HOLCF/Tools/holcf_library.ML Mon Aug 08 16:57:37 2011 -0700
+++ b/src/HOL/HOLCF/Tools/holcf_library.ML Mon Aug 08 18:36:32 2011 -0700
@@ -244,7 +244,7 @@
(T ->> V) ->> (U ->> V) ->> mk_ssumT (T, U) ->> V)
fun mk_sscase (t, u) =
- let val (T, V) = dest_cfunT (fastype_of t)
+ let val (T, _) = dest_cfunT (fastype_of t)
val (U, V) = dest_cfunT (fastype_of u)
in sscase_const (T, U, V) ` t ` u end