1.1 --- a/src/HOL/HOLCF/Tools/Domain/domain.ML Mon Aug 08 16:57:37 2011 -0700
1.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain.ML Mon Aug 08 18:36:32 2011 -0700
1.3 @@ -35,7 +35,6 @@
1.4
1.5 fun first (x,_,_) = x
1.6 fun second (_,x,_) = x
1.7 -fun third (_,_,x) = x
1.8
1.9 (* ----- calls for building new thy and thms -------------------------------- *)
1.10
1.11 @@ -78,16 +77,16 @@
1.12 (binding * (bool * binding option * 'b) list * mixfix) list list =
1.13 map (fn (_,_,_,cons) => cons) raw_specs
1.14 val dtnvs' : (string * typ list) list =
1.15 - map (fn (dbind, vs, mx) => (Sign.full_name thy dbind, vs)) dtnvs
1.16 + map (fn (dbind, vs, _) => (Sign.full_name thy dbind, vs)) dtnvs
1.17
1.18 val all_cons = map (Binding.name_of o first) (flat raw_rhss)
1.19 - val test_dupl_cons =
1.20 + val _ =
1.21 case duplicates (op =) all_cons of
1.22 [] => false | dups => error ("Duplicate constructors: "
1.23 ^ commas_quote dups)
1.24 val all_sels =
1.25 (map Binding.name_of o map_filter second o maps second) (flat raw_rhss)
1.26 - val test_dupl_sels =
1.27 + val _ =
1.28 case duplicates (op =) all_sels of
1.29 [] => false | dups => error("Duplicate selectors: "^commas_quote dups)
1.30
1.31 @@ -95,7 +94,7 @@
1.32 case duplicates (op =) (map(fst o dest_TFree)s) of
1.33 [] => false | dups => error("Duplicate type arguments: "
1.34 ^commas_quote dups)
1.35 - val test_dupl_tvars' = exists test_dupl_tvars (map snd dtnvs')
1.36 + val _ = exists test_dupl_tvars (map snd dtnvs')
1.37
1.38 val sorts : (string * sort) list =
1.39 let val all_sorts = map (map dest_TFree o snd) dtnvs'
1.40 @@ -119,7 +118,7 @@
1.41 non-pcpo-types and invalid use of recursive type
1.42 replace sorts in type variables on rhs *)
1.43 val rec_tab = Domain_Take_Proofs.get_rec_tab thy
1.44 - fun check_rec no_rec (T as TFree (v,_)) =
1.45 + fun check_rec _ (T as TFree (v,_)) =
1.46 if AList.defined (op =) sorts v then T
1.47 else error ("Free type variable " ^ quote v ^ " on rhs.")
1.48 | check_rec no_rec (T as Type (s, Ts)) =
1.49 @@ -141,7 +140,7 @@
1.50 error ("Illegal indirect recursion of type " ^
1.51 quote (Syntax.string_of_typ_global tmp_thy T) ^
1.52 " under type constructor " ^ quote c)))
1.53 - | check_rec no_rec (TVar _) = error "extender:check_rec"
1.54 + | check_rec _ (TVar _) = error "extender:check_rec"
1.55
1.56 fun prep_arg (lazy, sel, raw_T) =
1.57 let
1.58 @@ -154,8 +153,8 @@
1.59 val rhss : (binding * (bool * binding option * typ) list * mixfix) list list =
1.60 map prep_rhs raw_rhss
1.61
1.62 - fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_upT T else T
1.63 - fun mk_con_typ (bind, args, mx) =
1.64 + fun mk_arg_typ (lazy, _, T) = if lazy then mk_upT T else T
1.65 + fun mk_con_typ (_, args, _) =
1.66 if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args)
1.67 fun mk_rhs_typ cons = foldr1 mk_ssumT (map mk_con_typ cons)
1.68
1.69 @@ -174,7 +173,7 @@
1.70 Domain_Constructors.add_domain_constructors dbind cons info)
1.71 (dbinds ~~ rhss ~~ iso_infos)
1.72
1.73 - val (take_rews, thy) =
1.74 + val (_, thy) =
1.75 Domain_Induction.comp_theorems
1.76 dbinds take_info constr_infos thy
1.77 in
1.78 @@ -184,7 +183,7 @@
1.79 fun define_isos (spec : (binding * mixfix * (typ * typ)) list) =
1.80 let
1.81 fun prep (dbind, mx, (lhsT, rhsT)) =
1.82 - let val (dname, vs) = dest_Type lhsT
1.83 + let val (_, vs) = dest_Type lhsT
1.84 in (map (fst o dest_TFree) vs, dbind, mx, rhsT, NONE) end
1.85 in
1.86 Domain_Isomorphism.domain_isomorphism (map prep spec)
2.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML Mon Aug 08 16:57:37 2011 -0700
2.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML Mon Aug 08 18:36:32 2011 -0700
2.3 @@ -127,7 +127,7 @@
2.4 (dbinds ~~ iso_infos) take_info lub_take_thms thy
2.5
2.6 (* define map functions *)
2.7 - val (map_info, thy) =
2.8 + val (_, thy) =
2.9 Domain_Isomorphism.define_map_functions
2.10 (dbinds ~~ iso_infos) thy
2.11
3.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Mon Aug 08 16:57:37 2011 -0700
3.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Mon Aug 08 18:36:32 2011 -0700
3.3 @@ -80,9 +80,9 @@
3.4 fun mk_decl (b, t, mx) = (b, fastype_of t, mx)
3.5 val decls = map mk_decl specs
3.6 val thy = Cont_Consts.add_consts decls thy
3.7 - fun mk_const (b, T, mx) = Const (Sign.full_name thy b, T)
3.8 + fun mk_const (b, T, _) = Const (Sign.full_name thy b, T)
3.9 val consts = map mk_const decls
3.10 - fun mk_def c (b, t, mx) =
3.11 + fun mk_def c (b, t, _) =
3.12 (Binding.suffix_name "_def" b, Logic.mk_equals (c, t))
3.13 val defs = map2 mk_def consts specs
3.14 val (def_thms, thy) =
3.15 @@ -159,7 +159,7 @@
3.16 val abs_strict = iso_locale RS @{thm iso.abs_strict}
3.17
3.18 (* get types of type isomorphism *)
3.19 - val (rhsT, lhsT) = dest_cfunT (fastype_of abs_const)
3.20 + val (_, lhsT) = dest_cfunT (fastype_of abs_const)
3.21
3.22 fun vars_of args =
3.23 let
3.24 @@ -172,7 +172,7 @@
3.25 (* define constructor functions *)
3.26 val ((con_consts, con_defs), thy) =
3.27 let
3.28 - fun one_arg (lazy, T) var = if lazy then mk_up var else var
3.29 + fun one_arg (lazy, _) var = if lazy then mk_up var else var
3.30 fun one_con (_,args,_) = mk_stuple (map2 one_arg args (vars_of args))
3.31 fun mk_abs t = abs_const ` t
3.32 val rhss = map mk_abs (mk_sinjects (map one_con spec))
3.33 @@ -187,13 +187,13 @@
3.34
3.35 (* replace bindings with terms in constructor spec *)
3.36 val spec' : (term * (bool * typ) list) list =
3.37 - let fun one_con con (b, args, mx) = (con, args)
3.38 + let fun one_con con (_, args, _) = (con, args)
3.39 in map2 one_con con_consts spec end
3.40
3.41 (* prove exhaustiveness of constructors *)
3.42 local
3.43 - fun arg2typ n (true, T) = (n+1, mk_upT (TVar (("'a", n), @{sort cpo})))
3.44 - | arg2typ n (false, T) = (n+1, TVar (("'a", n), @{sort pcpo}))
3.45 + fun arg2typ n (true, _) = (n+1, mk_upT (TVar (("'a", n), @{sort cpo})))
3.46 + | arg2typ n (false, _) = (n+1, TVar (("'a", n), @{sort pcpo}))
3.47 fun args2typ n [] = (n, oneT)
3.48 | args2typ n [arg] = arg2typ n arg
3.49 | args2typ n (arg::args) =
3.50 @@ -332,14 +332,14 @@
3.51 | prime t = t
3.52 fun iff_disj (t, []) = mk_not t
3.53 | iff_disj (t, ts) = mk_eq (t, foldr1 mk_disj ts)
3.54 - fun iff_disj2 (t, [], us) = mk_not t
3.55 - | iff_disj2 (t, ts, []) = mk_not t
3.56 + fun iff_disj2 (t, [], _) = mk_not t
3.57 + | iff_disj2 (t, _, []) = mk_not t
3.58 | iff_disj2 (t, ts, us) =
3.59 mk_eq (t, mk_conj (foldr1 mk_disj ts, foldr1 mk_disj us))
3.60 fun dist_le (con1, args1) (con2, args2) =
3.61 let
3.62 val (vs1, zs1) = get_vars args1
3.63 - val (vs2, zs2) = get_vars args2 |> pairself (map prime)
3.64 + val (vs2, _) = get_vars args2 |> pairself (map prime)
3.65 val lhs = mk_below (list_ccomb (con1, vs1), list_ccomb (con2, vs2))
3.66 val rhss = map mk_undef zs1
3.67 val goal = mk_trp (iff_disj (lhs, rhss))
3.68 @@ -390,7 +390,6 @@
3.69 (lhsT : typ)
3.70 (dbind : binding)
3.71 (con_betas : thm list)
3.72 - (exhaust : thm)
3.73 (iso_locale : thm)
3.74 (rep_const : term)
3.75 (thy : theory)
3.76 @@ -429,7 +428,7 @@
3.77 | mk_sscases ts = foldr1 mk_sscase ts
3.78 val body = mk_sscases (map2 one_con fs spec)
3.79 val rhs = big_lambdas fs (mk_cfcomp (body, rep_const))
3.80 - val ((case_consts, case_defs), thy) =
3.81 + val ((_, case_defs), thy) =
3.82 define_consts [(case_bind, rhs, NoSyn)] thy
3.83 val case_name = Sign.full_name thy case_bind
3.84 in
3.85 @@ -457,7 +456,7 @@
3.86 Library.foldl capp (c_ast authentic con, argvars n args)
3.87 fun case1 authentic (n, c) =
3.88 app "_case1" (Ast.strip_positions (con1 authentic n c), expvar n)
3.89 - fun arg1 (n, (con,args)) = List.foldr cabs (expvar n) (argvars n args)
3.90 + fun arg1 (n, (_, args)) = List.foldr cabs (expvar n) (argvars n args)
3.91 fun when1 n (m, c) = if n = m then arg1 (n, c) else Ast.Constant @{const_syntax bottom}
3.92 val case_constant = Ast.Constant (syntax (case_const dummyT))
3.93 fun case_trans authentic =
3.94 @@ -541,16 +540,16 @@
3.95 fun mk_ssnd s = mk_cfcomp (ssnd_const (dest_sprodT (rangeT s)), s)
3.96 fun mk_down s = mk_cfcomp (from_up (dest_upT (rangeT s)), s)
3.97
3.98 - fun sels_of_arg s (lazy, NONE, T) = []
3.99 - | sels_of_arg s (lazy, SOME b, T) =
3.100 + fun sels_of_arg _ (_, NONE, _) = []
3.101 + | sels_of_arg s (lazy, SOME b, _) =
3.102 [(b, if lazy then mk_down s else s, NoSyn)]
3.103 - fun sels_of_args s [] = []
3.104 + fun sels_of_args _ [] = []
3.105 | sels_of_args s (v :: []) = sels_of_arg s v
3.106 | sels_of_args s (v :: vs) =
3.107 sels_of_arg (mk_sfst s) v @ sels_of_args (mk_ssnd s) vs
3.108 - fun sels_of_cons s [] = []
3.109 - | sels_of_cons s ((con, args) :: []) = sels_of_args s args
3.110 - | sels_of_cons s ((con, args) :: cs) =
3.111 + fun sels_of_cons _ [] = []
3.112 + | sels_of_cons s ((_, args) :: []) = sels_of_args s args
3.113 + | sels_of_cons s ((_, args) :: cs) =
3.114 sels_of_args (mk_outl s) args @ sels_of_cons (mk_outr s) cs
3.115 val sel_eqns : (binding * term * mixfix) list =
3.116 sels_of_cons rep_const spec
3.117 @@ -598,7 +597,7 @@
3.118 val vs : term list = map Free (ns ~~ Ts)
3.119 val con_app : term = list_ccomb (con, vs)
3.120 val vs' : (bool * term) list = map #1 args ~~ vs
3.121 - fun one_same (n, sel, T) =
3.122 + fun one_same (n, sel, _) =
3.123 let
3.124 val xs = map snd (filter_out fst (nth_drop n vs'))
3.125 val assms = map (mk_trp o mk_defined) xs
3.126 @@ -607,7 +606,7 @@
3.127 in
3.128 prove thy defs goal (K tacs)
3.129 end
3.130 - fun one_diff (n, sel, T) =
3.131 + fun one_diff (_, sel, T) =
3.132 let
3.133 val goal = mk_trp (mk_eq (sel ` con_app, mk_bottom T))
3.134 in
3.135 @@ -615,8 +614,8 @@
3.136 end
3.137 fun one_con (j, (_, args')) : thm list =
3.138 let
3.139 - fun prep (i, (lazy, NONE, T)) = NONE
3.140 - | prep (i, (lazy, SOME sel, T)) = SOME (i, sel, T)
3.141 + fun prep (_, (_, NONE, _)) = NONE
3.142 + | prep (i, (_, SOME sel, T)) = SOME (i, sel, T)
3.143 val sels : (int * term * typ) list =
3.144 map_filter prep (map_index I args')
3.145 in
3.146 @@ -646,12 +645,12 @@
3.147 in
3.148 prove thy sel_defs goal (K tacs)
3.149 end
3.150 - fun one_arg (false, SOME sel, T) = SOME (sel_defin sel)
3.151 + fun one_arg (false, SOME sel, _) = SOME (sel_defin sel)
3.152 | one_arg _ = NONE
3.153 in
3.154 case spec2 of
3.155 - [(con, args)] => map_filter one_arg args
3.156 - | _ => []
3.157 + [(_, args)] => map_filter one_arg args
3.158 + | _ => []
3.159 end
3.160
3.161 in
3.162 @@ -672,19 +671,11 @@
3.163 (thy : theory) =
3.164 let
3.165
3.166 - fun vars_of args =
3.167 - let
3.168 - val Ts = map snd args
3.169 - val ns = Datatype_Prop.make_tnames Ts
3.170 - in
3.171 - map Free (ns ~~ Ts)
3.172 - end
3.173 -
3.174 (* define discriminator functions *)
3.175 local
3.176 - fun dis_fun i (j, (con, args)) =
3.177 + fun dis_fun i (j, (_, args)) =
3.178 let
3.179 - val (vs, nonlazy) = get_vars args
3.180 + val (vs, _) = get_vars args
3.181 val tr = if i = j then @{term TT} else @{term FF}
3.182 in
3.183 big_lambdas vs tr
3.184 @@ -758,7 +749,6 @@
3.185 (bindings : binding list)
3.186 (spec : (term * (bool * typ) list) list)
3.187 (lhsT : typ)
3.188 - (exhaust : thm)
3.189 (case_const : typ -> term)
3.190 (case_rews : thm list)
3.191 (thy : theory) =
3.192 @@ -776,13 +766,13 @@
3.193 val x = Free ("x", lhsT)
3.194 fun k args = Free ("k", map snd args -->> mk_matchT resultT)
3.195 val fail = mk_fail resultT
3.196 - fun mat_fun i (j, (con, args)) =
3.197 + fun mat_fun i (j, (_, args)) =
3.198 let
3.199 - val (vs, nonlazy) = get_vars_avoiding ["x","k"] args
3.200 + val (vs, _) = get_vars_avoiding ["x","k"] args
3.201 in
3.202 if i = j then k args else big_lambdas vs fail
3.203 end
3.204 - fun mat_eqn (i, (bind, (con, args))) : binding * term * mixfix =
3.205 + fun mat_eqn (i, (bind, (_, args))) : binding * term * mixfix =
3.206 let
3.207 val mat_bind = Binding.prefix_name "match_" bind
3.208 val funs = map_index (mat_fun i) spec
3.209 @@ -866,7 +856,6 @@
3.210 val rep_strict = iso_locale RS @{thm iso.rep_strict}
3.211 val abs_strict = iso_locale RS @{thm iso.abs_strict}
3.212 val rep_bottom_iff = iso_locale RS @{thm iso.rep_bottom_iff}
3.213 - val abs_bottom_iff = iso_locale RS @{thm iso.abs_bottom_iff}
3.214 val iso_rews = [abs_iso_thm, rep_iso_thm, abs_strict, rep_strict]
3.215
3.216 (* qualify constants and theorems with domain name *)
3.217 @@ -875,7 +864,7 @@
3.218 (* define constructor functions *)
3.219 val (con_result, thy) =
3.220 let
3.221 - fun prep_arg (lazy, sel, T) = (lazy, T)
3.222 + fun prep_arg (lazy, _, T) = (lazy, T)
3.223 fun prep_con (b, args, mx) = (b, map prep_arg args, mx)
3.224 val con_spec = map prep_con spec
3.225 in
3.226 @@ -887,8 +876,8 @@
3.227 (* prepare constructor spec *)
3.228 val con_specs : (term * (bool * typ) list) list =
3.229 let
3.230 - fun prep_arg (lazy, sel, T) = (lazy, T)
3.231 - fun prep_con c (b, args, mx) = (c, map prep_arg args)
3.232 + fun prep_arg (lazy, _, T) = (lazy, T)
3.233 + fun prep_con c (_, args, _) = (c, map prep_arg args)
3.234 in
3.235 map2 prep_con con_consts spec
3.236 end
3.237 @@ -896,13 +885,13 @@
3.238 (* define case combinator *)
3.239 val ((case_const : typ -> term, cases : thm list), thy) =
3.240 add_case_combinator con_specs lhsT dbind
3.241 - con_betas exhaust iso_locale rep_const thy
3.242 + con_betas iso_locale rep_const thy
3.243
3.244 (* define and prove theorems for selector functions *)
3.245 val (sel_thms : thm list, thy : theory) =
3.246 let
3.247 val sel_spec : (term * (bool * binding option * typ) list) list =
3.248 - map2 (fn con => fn (b, args, mx) => (con, args)) con_consts spec
3.249 + map2 (fn con => fn (_, args, _) => (con, args)) con_consts spec
3.250 in
3.251 add_selectors sel_spec rep_const
3.252 abs_iso_thm rep_strict rep_bottom_iff con_betas thy
3.253 @@ -916,7 +905,7 @@
3.254 (* define and prove theorems for match combinators *)
3.255 val (match_thms : thm list, thy : theory) =
3.256 add_match_combinators bindings con_specs lhsT
3.257 - exhaust case_const cases thy
3.258 + case_const cases thy
3.259
3.260 (* restore original signature path *)
3.261 val thy = Sign.parent_path thy
4.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Mon Aug 08 16:57:37 2011 -0700
4.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Mon Aug 08 18:36:32 2011 -0700
4.3 @@ -221,7 +221,7 @@
4.4 if length dnames = 1 then ["bottom"] else
4.5 map (fn s => "bottom_" ^ Long_Name.base_name s) dnames
4.6 fun one_eq bot (constr_info : Domain_Constructors.constr_info) =
4.7 - let fun name_of (c, args) = Long_Name.base_name (fst (dest_Const c))
4.8 + let fun name_of (c, _) = Long_Name.base_name (fst (dest_Const c))
4.9 in bot :: map name_of (#con_specs constr_info) end
4.10 in adms @ flat (map2 one_eq bottoms constr_infos) end
4.11
4.12 @@ -344,7 +344,7 @@
4.13 val assm1 = mk_trp (list_comb (bisim_const, Rs))
4.14 val assm2 = mk_trp (R $ x $ y)
4.15 val goal = mk_trp (mk_eq (x, y))
4.16 - fun tacf {prems, context} =
4.17 + fun tacf {prems, context = _} =
4.18 let
4.19 val rule = hd prems RS coind_lemma
4.20 in
4.21 @@ -420,7 +420,7 @@
4.22 val (take_rewss, thy) =
4.23 take_theorems dbinds take_info constr_infos thy
4.24
4.25 -val {take_lemma_thms, take_0_thms, take_strict_thms, ...} = take_info
4.26 +val {take_0_thms, take_strict_thms, ...} = take_info
4.27
4.28 val take_rews = take_0_thms @ take_strict_thms @ flat take_rewss
4.29
5.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Aug 08 16:57:37 2011 -0700
5.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Aug 08 18:36:32 2011 -0700
5.3 @@ -86,15 +86,6 @@
5.4
5.5 fun mk_u_defl t = mk_capply (@{const "u_defl"}, t)
5.6
5.7 -fun mk_u_map t =
5.8 - let
5.9 - val (T, U) = dest_cfunT (fastype_of t)
5.10 - val u_map_type = (T ->> U) ->> (mk_upT T ->> mk_upT U)
5.11 - val u_map_const = Const (@{const_name u_map}, u_map_type)
5.12 - in
5.13 - mk_capply (u_map_const, t)
5.14 - end
5.15 -
5.16 fun emb_const T = Const (@{const_name emb}, T ->> udomT)
5.17 fun prj_const T = Const (@{const_name prj}, udomT ->> T)
5.18 fun coerce_const (T, U) = mk_cfcomp (prj_const U, emb_const T)
5.19 @@ -130,7 +121,7 @@
5.20 (*************** fixed-point definitions and unfolding theorems ***************)
5.21 (******************************************************************************)
5.22
5.23 -fun mk_projs [] t = []
5.24 +fun mk_projs [] _ = []
5.25 | mk_projs (x::[]) t = [(x, t)]
5.26 | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t)
5.27
5.28 @@ -187,7 +178,7 @@
5.29 (@{thm def_cont_fix_eq} OF [tuple_fixdef_thm, cont_thm])
5.30 |> Local_Defs.unfold (Proof_Context.init_global thy) @{thms split_conv}
5.31
5.32 - fun mk_unfold_thms [] thm = []
5.33 + fun mk_unfold_thms [] _ = []
5.34 | mk_unfold_thms (n::[]) thm = [(n, thm)]
5.35 | mk_unfold_thms (n::ns) thm = let
5.36 val thmL = thm RS @{thm Pair_eqD1}
5.37 @@ -271,7 +262,7 @@
5.38 | mapT T = T ->> T
5.39
5.40 (* declare map functions *)
5.41 - fun declare_map_const (tbind, (lhsT, rhsT)) thy =
5.42 + fun declare_map_const (tbind, (lhsT, _)) thy =
5.43 let
5.44 val map_type = mapT lhsT
5.45 val map_bind = Binding.suffix_name "_map" tbind
5.46 @@ -290,7 +281,7 @@
5.47 val tab1 = map map_lhs (map_consts ~~ map fst dom_eqns)
5.48 val Ts = (snd o dest_Type o fst o hd) dom_eqns
5.49 val tab = (Ts ~~ map mapvar Ts) @ tab1
5.50 - fun mk_map_spec (((rep_const, abs_const), map_const), (lhsT, rhsT)) =
5.51 + fun mk_map_spec (((rep_const, abs_const), _), (lhsT, rhsT)) =
5.52 let
5.53 val lhs = Domain_Take_Proofs.map_of_typ thy tab lhsT
5.54 val body = Domain_Take_Proofs.map_of_typ thy tab rhsT
5.55 @@ -313,7 +304,7 @@
5.56 fun unprime a = Library.unprefix "'" a
5.57 fun mk_f T = Free (unprime (fst (dest_TFree T)), T ->> T)
5.58 fun mk_assm T = mk_trp (mk_deflation (mk_f T))
5.59 - fun mk_goal (map_const, (lhsT, rhsT)) =
5.60 + fun mk_goal (map_const, (lhsT, _)) =
5.61 let
5.62 val (_, Ts) = dest_Type lhsT
5.63 val map_term = list_ccomb (map_const, map mk_f (filter (is_cpo thy) Ts))
5.64 @@ -343,7 +334,7 @@
5.65 REPEAT (etac @{thm conjE} 1),
5.66 REPEAT (resolve_tac (deflation_rules @ prems) 1 ORELSE atac 1)])
5.67 end
5.68 - fun conjuncts [] thm = []
5.69 + fun conjuncts [] _ = []
5.70 | conjuncts (n::[]) thm = [(n, thm)]
5.71 | conjuncts (n::ns) thm = let
5.72 val thmL = thm RS @{thm conjunct1}
5.73 @@ -360,7 +351,6 @@
5.74 fun register_map (dname, args) =
5.75 Domain_Take_Proofs.add_rec_type (dname, args)
5.76 val dnames = map (fst o dest_Type o fst) dom_eqns
5.77 - val map_names = map (fst o dest_Const) map_consts
5.78 fun args (T, _) = case T of Type (_, Ts) => map (is_cpo thy) Ts | _ => []
5.79 val argss = map args dom_eqns
5.80 in
5.81 @@ -417,7 +407,7 @@
5.82 (* this theory is used just for parsing *)
5.83 val tmp_thy = thy |>
5.84 Theory.copy |>
5.85 - Sign.add_types_global (map (fn (tvs, tbind, mx, _, morphs) =>
5.86 + Sign.add_types_global (map (fn (tvs, tbind, mx, _, _) =>
5.87 (tbind, length tvs, mx)) doms_raw)
5.88
5.89 fun prep_dom thy (vs, t, mx, typ_raw, morphs) sorts =
5.90 @@ -434,28 +424,28 @@
5.91 (* declare arities in temporary theory *)
5.92 val tmp_thy =
5.93 let
5.94 - fun arity (vs, tbind, mx, _, _) =
5.95 + fun arity (vs, tbind, _, _, _) =
5.96 (Sign.full_name thy tbind, map the_sort vs, @{sort "domain"})
5.97 in
5.98 fold AxClass.axiomatize_arity (map arity doms) tmp_thy
5.99 end
5.100
5.101 (* check bifiniteness of right-hand sides *)
5.102 - fun check_rhs (vs, tbind, mx, rhs, morphs) =
5.103 + fun check_rhs (_, _, _, rhs, _) =
5.104 if Sign.of_sort tmp_thy (rhs, @{sort "domain"}) then ()
5.105 else error ("Type not of sort domain: " ^
5.106 quote (Syntax.string_of_typ_global tmp_thy rhs))
5.107 val _ = map check_rhs doms
5.108
5.109 (* domain equations *)
5.110 - fun mk_dom_eqn (vs, tbind, mx, rhs, morphs) =
5.111 + fun mk_dom_eqn (vs, tbind, _, rhs, _) =
5.112 let fun arg v = TFree (v, the_sort v)
5.113 in (Type (Sign.full_name tmp_thy tbind, map arg vs), rhs) end
5.114 val dom_eqns = map mk_dom_eqn doms
5.115
5.116 (* check for valid type parameters *)
5.117 val (tyvars, _, _, _, _) = hd doms
5.118 - val new_doms = map (fn (tvs, tname, mx, _, _) =>
5.119 + val _ = map (fn (tvs, tname, _, _, _) =>
5.120 let val full_tname = Sign.full_name tmp_thy tname
5.121 in
5.122 (case duplicates (op =) tvs of
5.123 @@ -528,7 +518,7 @@
5.124 fun make_repdef ((vs, tbind, mx, _, _), defl) thy =
5.125 let
5.126 val spec = (tbind, map (rpair dummyS) vs, mx)
5.127 - val ((_, _, _, {DEFL, liftemb_def, liftprj_def, ...}), thy) =
5.128 + val ((_, _, _, {DEFL, ...}), thy) =
5.129 Domaindef.add_domaindef false NONE spec defl NONE thy
5.130 (* declare domain_defl_simps rules *)
5.131 val thy = Context.theory_map (RepData.add_thm DEFL) thy
5.132 @@ -557,7 +547,7 @@
5.133 (DEFL_eq_binds ~~ DEFL_eq_thms)
5.134
5.135 (* define rep/abs functions *)
5.136 - fun mk_rep_abs ((tbind, morphs), (lhsT, rhsT)) thy =
5.137 + fun mk_rep_abs ((tbind, _), (lhsT, rhsT)) thy =
5.138 let
5.139 val rep_bind = Binding.suffix_name "_rep" tbind
5.140 val abs_bind = Binding.suffix_name "_abs" tbind
5.141 @@ -611,8 +601,7 @@
5.142 (* definitions and proofs related to map functions *)
5.143 val (map_info, thy) =
5.144 define_map_functions (dbinds ~~ iso_infos) thy
5.145 - val { map_consts, map_apply_thms, map_unfold_thms,
5.146 - map_cont_thm, deflation_map_thms } = map_info
5.147 + val { map_consts, map_apply_thms, map_cont_thm, ...} = map_info
5.148
5.149 (* prove isodefl rules for map functions *)
5.150 val isodefl_thm =
5.151 @@ -627,7 +616,7 @@
5.152 | NONE =>
5.153 let val T = dest_DEFL t
5.154 in mk_trp (isodefl_const T $ mk_f T $ mk_d T) end
5.155 - fun mk_goal (map_const, (T, rhsT)) =
5.156 + fun mk_goal (map_const, (T, _)) =
5.157 let
5.158 val (_, Ts) = dest_Type T
5.159 val map_term = list_ccomb (map_const, map mk_f (filter (is_cpo thy) Ts))
5.160 @@ -662,7 +651,7 @@
5.161 REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)])
5.162 end
5.163 val isodefl_binds = map (Binding.prefix_name "isodefl_") dbinds
5.164 - fun conjuncts [] thm = []
5.165 + fun conjuncts [] _ = []
5.166 | conjuncts (n::[]) thm = [(n, thm)]
5.167 | conjuncts (n::ns) thm = let
5.168 val thmL = thm RS @{thm conjunct1}
5.169 @@ -709,7 +698,7 @@
5.170 let
5.171 val lhs = mk_tuple (map mk_lub take_consts)
5.172 fun is_cpo T = Sign.of_sort thy (T, @{sort cpo})
5.173 - fun mk_map_ID (map_const, (lhsT, rhsT)) =
5.174 + fun mk_map_ID (map_const, (lhsT, _)) =
5.175 list_ccomb (map_const, map mk_ID (filter is_cpo (snd (dest_Type lhsT))))
5.176 val rhs = mk_tuple (map mk_map_ID (map_consts ~~ dom_eqns))
5.177 val goal = mk_trp (mk_eq (lhs, rhs))
5.178 @@ -736,7 +725,7 @@
5.179 end
5.180
5.181 (* prove lub of take equals ID *)
5.182 - fun prove_lub_take (((dbind, take_const), map_ID_thm), (lhsT, rhsT)) thy =
5.183 + fun prove_lub_take (((dbind, take_const), map_ID_thm), (lhsT, _)) thy =
5.184 let
5.185 val n = Free ("n", natT)
5.186 val goal = mk_eqs (mk_lub (lambda n (take_const $ n)), mk_ID lhsT)
6.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Mon Aug 08 16:57:37 2011 -0700
6.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Mon Aug 08 18:36:32 2011 -0700
6.3 @@ -159,10 +159,6 @@
6.4 infix -->>
6.5 infix 9 `
6.6
6.7 -fun mapT (T as Type (_, Ts)) =
6.8 - (map (fn T => T ->> T) Ts) -->> (T ->> T)
6.9 - | mapT T = T ->> T
6.10 -
6.11 fun mk_deflation t =
6.12 Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t
6.13
6.14 @@ -227,7 +223,7 @@
6.15 val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos
6.16 val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos
6.17
6.18 - fun mk_projs [] t = []
6.19 + fun mk_projs [] _ = []
6.20 | mk_projs (x::[]) t = [(x, t)]
6.21 | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t)
6.22
6.23 @@ -239,7 +235,7 @@
6.24 val copy_arg_type = mk_tupleT (map (fn T => T ->> T) newTs)
6.25 val copy_arg = Free ("f", copy_arg_type)
6.26 val copy_args = map snd (mk_projs dbinds copy_arg)
6.27 - fun one_copy_rhs (rep_abs, (lhsT, rhsT)) =
6.28 + fun one_copy_rhs (rep_abs, (_, rhsT)) =
6.29 let
6.30 val body = map_of_typ thy (newTs ~~ copy_args) rhsT
6.31 in
6.32 @@ -257,7 +253,7 @@
6.33 end
6.34
6.35 (* define take constants *)
6.36 - fun define_take_const ((dbind, take_rhs), (lhsT, rhsT)) thy =
6.37 + fun define_take_const ((dbind, take_rhs), (lhsT, _)) thy =
6.38 let
6.39 val take_type = HOLogic.natT --> lhsT ->> lhsT
6.40 val take_bind = Binding.suffix_name "_take" dbind
6.41 @@ -285,7 +281,7 @@
6.42 fold_map prove_chain_take (take_consts ~~ dbinds) thy
6.43
6.44 (* prove take_0 lemmas *)
6.45 - fun prove_take_0 ((take_const, dbind), (lhsT, rhsT)) thy =
6.46 + fun prove_take_0 ((take_const, dbind), (lhsT, _)) thy =
6.47 let
6.48 val lhs = take_const $ @{term "0::nat"}
6.49 val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT))
6.50 @@ -302,7 +298,7 @@
6.51 val n = Free ("n", natT)
6.52 val take_is = map (fn t => t $ n) take_consts
6.53 fun prove_take_Suc
6.54 - (((take_const, rep_abs), dbind), (lhsT, rhsT)) thy =
6.55 + (((take_const, rep_abs), dbind), (_, rhsT)) thy =
6.56 let
6.57 val lhs = take_const $ (@{term Suc} $ n)
6.58 val body = map_of_typ thy (newTs ~~ take_is) rhsT
6.59 @@ -326,9 +322,6 @@
6.60 val n = Free ("n", natT)
6.61 fun mk_goal take_const = mk_deflation (take_const $ n)
6.62 val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts))
6.63 - val adm_rules =
6.64 - @{thms adm_conj adm_subst [OF _ adm_deflation]
6.65 - cont2cont_fst cont2cont_snd cont_id}
6.66 val bottom_rules =
6.67 take_0_thms @ @{thms deflation_bottom simp_thms}
6.68 val deflation_rules =
6.69 @@ -345,7 +338,7 @@
6.70 ORELSE resolve_tac deflation_rules 1
6.71 ORELSE atac 1)])
6.72 end
6.73 - fun conjuncts [] thm = []
6.74 + fun conjuncts [] _ = []
6.75 | conjuncts (n::[]) thm = [(n, thm)]
6.76 | conjuncts (n::ns) thm = let
6.77 val thmL = thm RS @{thm conjunct1}
6.78 @@ -378,7 +371,7 @@
6.79 in
6.80 add_qualified_thm "take_take" (dbind, take_take_thm) thy
6.81 end
6.82 - val (take_take_thms, thy) =
6.83 + val (_, thy) =
6.84 fold_map prove_take_take
6.85 (chain_take_thms ~~ deflation_take_thms ~~ dbinds) thy
6.86
6.87 @@ -391,12 +384,12 @@
6.88 in
6.89 add_qualified_thm "take_below" (dbind, take_below_thm) thy
6.90 end
6.91 - val (take_below_thms, thy) =
6.92 + val (_, thy) =
6.93 fold_map prove_take_below
6.94 (deflation_take_thms ~~ dbinds) thy
6.95
6.96 (* define finiteness predicates *)
6.97 - fun define_finite_const ((dbind, take_const), (lhsT, rhsT)) thy =
6.98 + fun define_finite_const ((dbind, take_const), (lhsT, _)) thy =
6.99 let
6.100 val finite_type = lhsT --> boolT
6.101 val finite_bind = Binding.suffix_name "_finite" dbind
6.102 @@ -517,8 +510,7 @@
6.103 val iso_infos = map snd spec
6.104 val absTs = map #absT iso_infos
6.105 val repTs = map #repT iso_infos
6.106 - val {take_consts, take_0_thms, take_Suc_thms, ...} = take_info
6.107 - val {chain_take_thms, deflation_take_thms, ...} = take_info
6.108 + val {chain_take_thms, ...} = take_info
6.109
6.110 (* prove take lemmas *)
6.111 fun prove_take_lemma ((chain_take, lub_take), dbind) thy =
6.112 @@ -553,12 +545,12 @@
6.113 and finite' d (Type (c, Ts)) =
6.114 let val d' = d andalso member (op =) types c
6.115 in forall (finite d') Ts end
6.116 - | finite' d _ = true
6.117 + | finite' _ _ = true
6.118 in
6.119 val is_finite = forall (finite true) repTs
6.120 end
6.121
6.122 - val ((finite_thms, take_induct_thms), thy) =
6.123 + val ((_, take_induct_thms), thy) =
6.124 if is_finite
6.125 then
6.126 let
7.1 --- a/src/HOL/HOLCF/Tools/cont_proc.ML Mon Aug 08 16:57:37 2011 -0700
7.2 +++ b/src/HOL/HOLCF/Tools/cont_proc.ML Mon Aug 08 18:36:32 2011 -0700
7.3 @@ -102,7 +102,7 @@
7.4 fun new_cont_tac f' i =
7.5 case all_cont_thms f' of
7.6 [] => no_tac
7.7 - | (c::cs) => rtac c i
7.8 + | (c::_) => rtac c i
7.9
7.10 fun cont_tac_of_term (Const (@{const_name cont}, _) $ f) =
7.11 let
8.1 --- a/src/HOL/HOLCF/Tools/cpodef.ML Mon Aug 08 16:57:37 2011 -0700
8.2 +++ b/src/HOL/HOLCF/Tools/cpodef.ML Mon Aug 08 18:36:32 2011 -0700
8.3 @@ -154,10 +154,7 @@
8.4
8.5 (* prepare_cpodef *)
8.6
8.7 -fun declare_type_name a =
8.8 - Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)))
8.9 -
8.10 -fun prepare prep_term name (tname, raw_args, mx) raw_set opt_morphs thy =
8.11 +fun prepare prep_term name (tname, raw_args, _) raw_set opt_morphs thy =
8.12 let
8.13 val _ = Theory.requires thy "Cpodef" "cpodefs"
8.14
8.15 @@ -186,7 +183,7 @@
8.16 fun add_podef def opt_name typ set opt_morphs tac thy =
8.17 let
8.18 val name = the_default (#1 typ) opt_name
8.19 - val ((full_tname, info as ({Rep_name, ...}, {type_definition, set_def, ...})), thy) = thy
8.20 + val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) = thy
8.21 |> Typedef.add_typedef_global def opt_name typ set opt_morphs tac
8.22 val oldT = #rep_type (#1 info)
8.23 val newT = #abs_type (#1 info)
8.24 @@ -216,7 +213,7 @@
8.25 (thy: theory)
8.26 : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info) * theory) =
8.27 let
8.28 - val (newT, oldT, set, morphs as (Rep_name, Abs_name)) =
8.29 + val (newT, oldT, set, morphs) =
8.30 prepare prep_term name typ raw_set opt_morphs thy
8.31
8.32 val goal_nonempty =
8.33 @@ -249,7 +246,7 @@
8.34 (thy: theory)
8.35 : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory) =
8.36 let
8.37 - val (newT, oldT, set, morphs as (Rep_name, Abs_name)) =
8.38 + val (newT, oldT, set, morphs) =
8.39 prepare prep_term name typ raw_set opt_morphs thy
8.40
8.41 val goal_bottom_mem =
9.1 --- a/src/HOL/HOLCF/Tools/domaindef.ML Mon Aug 08 16:57:37 2011 -0700
9.2 +++ b/src/HOL/HOLCF/Tools/domaindef.ML Mon Aug 08 18:36:32 2011 -0700
9.3 @@ -76,14 +76,11 @@
9.4
9.5 (* proving class instances *)
9.6
9.7 -fun declare_type_name a =
9.8 - Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)))
9.9 -
9.10 fun gen_add_domaindef
9.11 (prep_term: Proof.context -> 'a -> term)
9.12 (def: bool)
9.13 (name: binding)
9.14 - (typ as (tname, raw_args, mx) : binding * (string * sort) list * mixfix)
9.15 + (typ as (tname, raw_args, _) : binding * (string * sort) list * mixfix)
9.16 (raw_defl: 'a)
9.17 (opt_morphs: (binding * binding) option)
9.18 (thy: theory)
9.19 @@ -104,7 +101,6 @@
9.20
9.21 (*lhs*)
9.22 val lhs_tfrees = map (Proof_Context.check_tfree tmp_ctxt) raw_args
9.23 - val lhs_sorts = map snd lhs_tfrees
9.24 val full_tname = Sign.full_name thy tname
9.25 val newT = Type (full_tname, map TFree lhs_tfrees)
9.26
10.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML Mon Aug 08 16:57:37 2011 -0700
10.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML Mon Aug 08 18:36:32 2011 -0700
10.3 @@ -28,8 +28,6 @@
10.4 val def_cont_fix_ind = @{thm def_cont_fix_ind}
10.5
10.6 fun fixrec_err s = error ("fixrec definition error:\n" ^ s)
10.7 -fun fixrec_eq_err thy s eq =
10.8 - fixrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq))
10.9
10.10 (*************************************************************************)
10.11 (***************************** building types ****************************)
10.12 @@ -41,13 +39,10 @@
10.13 | binder_cfun (Type(@{type_name "fun"},[T, U])) = T :: binder_cfun U
10.14 | binder_cfun _ = []
10.15
10.16 -fun body_cfun (Type(@{type_name cfun},[T, U])) = body_cfun U
10.17 - | body_cfun (Type(@{type_name "fun"},[T, U])) = body_cfun U
10.18 +fun body_cfun (Type(@{type_name cfun},[_, U])) = body_cfun U
10.19 + | body_cfun (Type(@{type_name "fun"},[_, U])) = body_cfun U
10.20 | body_cfun T = T
10.21
10.22 -fun strip_cfun T : typ list * typ =
10.23 - (binder_cfun T, body_cfun T)
10.24 -
10.25 in
10.26
10.27 fun matcherT (T, U) =
10.28 @@ -65,10 +60,9 @@
10.29 fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t)
10.30
10.31 (* similar to Thm.head_of, but for continuous application *)
10.32 -fun chead_of (Const(@{const_name Rep_cfun},_)$f$t) = chead_of f
10.33 +fun chead_of (Const(@{const_name Rep_cfun},_)$f$_) = chead_of f
10.34 | chead_of u = u
10.35
10.36 -infix 0 == val (op ==) = Logic.mk_equals
10.37 infix 1 === val (op ===) = HOLogic.mk_eq
10.38
10.39 fun mk_mplus (t, u) =
10.40 @@ -102,8 +96,8 @@
10.41
10.42 local
10.43
10.44 -fun name_of (Const (n, T)) = n
10.45 - | name_of (Free (n, T)) = n
10.46 +fun name_of (Const (n, _)) = n
10.47 + | name_of (Free (n, _)) = n
10.48 | name_of t = raise TERM ("Fixrec.add_unfold: lhs not a constant", [t])
10.49
10.50 val lhs_name =
10.51 @@ -145,7 +139,7 @@
10.52 Goal.prove lthy [] [] prop (K tac)
10.53 end
10.54
10.55 - fun one_def (l as Free(n,_)) r =
10.56 + fun one_def (Free(n,_)) r =
10.57 let val b = Long_Name.base_name n
10.58 in ((Binding.name (b^"_def"), []), r) end
10.59 | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form"
10.60 @@ -164,7 +158,7 @@
10.61 |> Local_Defs.unfold lthy @{thms split_paired_all split_conv split_strict}
10.62 val tuple_unfold_thm = (def_cont_fix_eq OF [tuple_fixdef_thm, cont_thm])
10.63 |> Local_Defs.unfold lthy @{thms split_conv}
10.64 - fun unfolds [] thm = []
10.65 + fun unfolds [] _ = []
10.66 | unfolds (n::[]) thm = [(n, thm)]
10.67 | unfolds (n::ns) thm = let
10.68 val thmL = thm RS @{thm Pair_eqD1}
10.69 @@ -184,7 +178,7 @@
10.70 in
10.71 ((thm_name, [src]), [thm])
10.72 end
10.73 - val (thmss, lthy) = lthy
10.74 + val (_, lthy) = lthy
10.75 |> fold_map Local_Theory.note (induct_note :: map unfold_note unfold_thms)
10.76 in
10.77 (lthy, names, fixdef_thms, map snd unfold_thms)
10.78 @@ -303,7 +297,7 @@
10.79 else HOLogic.dest_Trueprop (Logic.strip_imp_concl t)
10.80 fun tac (t, i) =
10.81 let
10.82 - val (c, T) =
10.83 + val (c, _) =
10.84 (dest_Const o head_of o chead_of o fst o HOLogic.dest_eq o concl) t
10.85 val unfold_thm = the (Symtab.lookup tab c)
10.86 val rule = unfold_thm RS @{thm ssubst_lhs}
10.87 @@ -346,7 +340,7 @@
10.88 val chead_of_spec =
10.89 chead_of o fst o dest_eqs o Logic.strip_imp_concl o strip_alls o snd
10.90 fun name_of (Free (n, _)) = n
10.91 - | name_of t = fixrec_err ("unknown term")
10.92 + | name_of _ = fixrec_err ("unknown term")
10.93 val all_names = map (name_of o chead_of_spec) spec
10.94 val names = distinct (op =) all_names
10.95 fun block_of_name n =
10.96 @@ -362,7 +356,7 @@
10.97
10.98 val matches = map (compile_eqs match_name) (map (map (snd o fst)) blocks)
10.99 val spec' = map (pair Attrib.empty_binding) matches
10.100 - val (lthy, cnames, fixdef_thms, unfold_thms) =
10.101 + val (lthy, _, _, unfold_thms) =
10.102 add_fixdefs fixes spec' lthy
10.103
10.104 val blocks' = map (map fst o filter_out snd) blocks
11.1 --- a/src/HOL/HOLCF/Tools/holcf_library.ML Mon Aug 08 16:57:37 2011 -0700
11.2 +++ b/src/HOL/HOLCF/Tools/holcf_library.ML Mon Aug 08 18:36:32 2011 -0700
11.3 @@ -244,7 +244,7 @@
11.4 (T ->> V) ->> (U ->> V) ->> mk_ssumT (T, U) ->> V)
11.5
11.6 fun mk_sscase (t, u) =
11.7 - let val (T, V) = dest_cfunT (fastype_of t)
11.8 + let val (T, _) = dest_cfunT (fastype_of t)
11.9 val (U, V) = dest_cfunT (fastype_of u)
11.10 in sscase_const (T, U, V) ` t ` u end
11.11