# HG changeset patch # User haftmann # Date 1312868657 -7200 # Node ID c0847967a25a77f914148f7905aa6ab3cd111235 # Parent 730f7cced3a6ab5b0270f29f6f2419c3c3fdcd8c# Parent a65e26f1427bffff0a58b852603a78a144276aed merged diff -r a65e26f1427b -r c0847967a25a NEWS --- a/NEWS Mon Aug 08 22:33:36 2011 +0200 +++ b/NEWS Tue Aug 09 07:44:17 2011 +0200 @@ -172,6 +172,9 @@ Every theorem name containing "inat", "Fin", "Infty", or "iSuc" has been renamed accordingly. +* Limits.thy: Type "'a net" has been renamed to "'a filter", in +accordance with standard mathematical terminology. INCOMPATIBILITY. + *** Document preparation *** diff -r a65e26f1427b -r c0847967a25a src/HOL/Deriv.thy --- a/src/HOL/Deriv.thy Mon Aug 08 22:33:36 2011 +0200 +++ b/src/HOL/Deriv.thy Tue Aug 09 07:44:17 2011 +0200 @@ -42,11 +42,6 @@ lemma DERIV_ident [simp]: "DERIV (\x. x) x :> 1" by (simp add: deriv_def cong: LIM_cong) -lemma add_diff_add: - fixes a b c d :: "'a::ab_group_add" - shows "(a + c) - (b + d) = (a - b) + (c - d)" -by simp - lemma DERIV_add: "\DERIV f x :> D; DERIV g x :> E\ \ DERIV (\x. f x + g x) x :> D + E" by (simp only: deriv_def add_diff_add add_divide_distrib LIM_add) @@ -141,11 +136,6 @@ lemma DERIV_iff2: "(DERIV f x :> D) = ((%z. (f(z) - f(x)) / (z-x)) -- x --> D)" by (simp add: deriv_def diff_minus [symmetric] DERIV_LIM_iff) -lemma inverse_diff_inverse: - "\(a::'a::division_ring) \ 0; b \ 0\ - \ inverse a - inverse b = - (inverse a * (a - b) * inverse b)" -by (simp add: algebra_simps) - lemma DERIV_inverse_lemma: "\a \ 0; b \ (0::'a::real_normed_field)\ \ (inverse a - inverse b) / h diff -r a65e26f1427b -r c0847967a25a src/HOL/HOLCF/Tools/Domain/domain.ML --- a/src/HOL/HOLCF/Tools/Domain/domain.ML Mon Aug 08 22:33:36 2011 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain.ML Tue Aug 09 07:44:17 2011 +0200 @@ -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) diff -r a65e26f1427b -r c0847967a25a src/HOL/HOLCF/Tools/Domain/domain_axioms.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML Mon Aug 08 22:33:36 2011 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML Tue Aug 09 07:44:17 2011 +0200 @@ -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 diff -r a65e26f1427b -r c0847967a25a src/HOL/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Mon Aug 08 22:33:36 2011 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Tue Aug 09 07:44:17 2011 +0200 @@ -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 diff -r a65e26f1427b -r c0847967a25a src/HOL/HOLCF/Tools/Domain/domain_induction.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Mon Aug 08 22:33:36 2011 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Tue Aug 09 07:44:17 2011 +0200 @@ -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 diff -r a65e26f1427b -r c0847967a25a src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Mon Aug 08 22:33:36 2011 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Aug 09 07:44:17 2011 +0200 @@ -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) diff -r a65e26f1427b -r c0847967a25a src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Mon Aug 08 22:33:36 2011 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Tue Aug 09 07:44:17 2011 +0200 @@ -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 diff -r a65e26f1427b -r c0847967a25a src/HOL/HOLCF/Tools/cont_proc.ML --- a/src/HOL/HOLCF/Tools/cont_proc.ML Mon Aug 08 22:33:36 2011 +0200 +++ b/src/HOL/HOLCF/Tools/cont_proc.ML Tue Aug 09 07:44:17 2011 +0200 @@ -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 diff -r a65e26f1427b -r c0847967a25a src/HOL/HOLCF/Tools/cpodef.ML --- a/src/HOL/HOLCF/Tools/cpodef.ML Mon Aug 08 22:33:36 2011 +0200 +++ b/src/HOL/HOLCF/Tools/cpodef.ML Tue Aug 09 07:44:17 2011 +0200 @@ -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 = diff -r a65e26f1427b -r c0847967a25a src/HOL/HOLCF/Tools/domaindef.ML --- a/src/HOL/HOLCF/Tools/domaindef.ML Mon Aug 08 22:33:36 2011 +0200 +++ b/src/HOL/HOLCF/Tools/domaindef.ML Tue Aug 09 07:44:17 2011 +0200 @@ -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) diff -r a65e26f1427b -r c0847967a25a src/HOL/HOLCF/Tools/fixrec.ML --- a/src/HOL/HOLCF/Tools/fixrec.ML Mon Aug 08 22:33:36 2011 +0200 +++ b/src/HOL/HOLCF/Tools/fixrec.ML Tue Aug 09 07:44:17 2011 +0200 @@ -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 diff -r a65e26f1427b -r c0847967a25a src/HOL/HOLCF/Tools/holcf_library.ML --- a/src/HOL/HOLCF/Tools/holcf_library.ML Mon Aug 08 22:33:36 2011 +0200 +++ b/src/HOL/HOLCF/Tools/holcf_library.ML Tue Aug 09 07:44:17 2011 +0200 @@ -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 diff -r a65e26f1427b -r c0847967a25a src/HOL/Library/positivstellensatz.ML --- a/src/HOL/Library/positivstellensatz.ML Mon Aug 08 22:33:36 2011 +0200 +++ b/src/HOL/Library/positivstellensatz.ML Tue Aug 09 07:44:17 2011 +0200 @@ -170,8 +170,8 @@ Thm.equal_intr (Thm.implies_intr (cprop_of thb) tha) (Thm.implies_intr (cprop_of tha) thb); -fun prove_hyp tha thb = - if exists (curry op aconv (concl_of tha)) (#hyps (rep_thm thb)) +fun prove_hyp tha thb = + if exists (curry op aconv (concl_of tha)) (Thm.hyps_of thb) (* FIXME !? *) then Thm.equal_elim (Thm.symmetric (deduct_antisym_rule tha thb)) tha else thb; val pth = @{lemma "(((x::real) < y) == (y - x > 0))" and "((x <= y) == (y - x >= 0))" and diff -r a65e26f1427b -r c0847967a25a src/HOL/Limits.thy --- a/src/HOL/Limits.thy Mon Aug 08 22:33:36 2011 +0200 +++ b/src/HOL/Limits.thy Tue Aug 09 07:44:17 2011 +0200 @@ -8,263 +8,262 @@ imports RealVector begin -subsection {* Nets *} +subsection {* Filters *} text {* - A net is now defined simply as a filter on a set. - The definition also allows non-proper filters. + This definition also allows non-proper filters. *} locale is_filter = - fixes net :: "('a \ bool) \ bool" - assumes True: "net (\x. True)" - assumes conj: "net (\x. P x) \ net (\x. Q x) \ net (\x. P x \ Q x)" - assumes mono: "\x. P x \ Q x \ net (\x. P x) \ net (\x. Q x)" + fixes F :: "('a \ bool) \ bool" + assumes True: "F (\x. True)" + assumes conj: "F (\x. P x) \ F (\x. Q x) \ F (\x. P x \ Q x)" + assumes mono: "\x. P x \ Q x \ F (\x. P x) \ F (\x. Q x)" -typedef (open) 'a net = - "{net :: ('a \ bool) \ bool. is_filter net}" +typedef (open) 'a filter = "{F :: ('a \ bool) \ bool. is_filter F}" proof - show "(\x. True) \ ?net" by (auto intro: is_filter.intro) + show "(\x. True) \ ?filter" by (auto intro: is_filter.intro) qed -lemma is_filter_Rep_net: "is_filter (Rep_net net)" -using Rep_net [of net] by simp +lemma is_filter_Rep_filter: "is_filter (Rep_filter A)" + using Rep_filter [of A] by simp -lemma Abs_net_inverse': - assumes "is_filter net" shows "Rep_net (Abs_net net) = net" -using assms by (simp add: Abs_net_inverse) +lemma Abs_filter_inverse': + assumes "is_filter F" shows "Rep_filter (Abs_filter F) = F" + using assms by (simp add: Abs_filter_inverse) subsection {* Eventually *} -definition eventually :: "('a \ bool) \ 'a net \ bool" where - "eventually P net \ Rep_net net P" +definition eventually :: "('a \ bool) \ 'a filter \ bool" + where "eventually P A \ Rep_filter A P" -lemma eventually_Abs_net: - assumes "is_filter net" shows "eventually P (Abs_net net) = net P" -unfolding eventually_def using assms by (simp add: Abs_net_inverse) +lemma eventually_Abs_filter: + assumes "is_filter F" shows "eventually P (Abs_filter F) = F P" + unfolding eventually_def using assms by (simp add: Abs_filter_inverse) -lemma expand_net_eq: - shows "net = net' \ (\P. eventually P net = eventually P net')" -unfolding Rep_net_inject [symmetric] fun_eq_iff eventually_def .. +lemma filter_eq_iff: + shows "A = B \ (\P. eventually P A = eventually P B)" + unfolding Rep_filter_inject [symmetric] fun_eq_iff eventually_def .. -lemma eventually_True [simp]: "eventually (\x. True) net" -unfolding eventually_def -by (rule is_filter.True [OF is_filter_Rep_net]) +lemma eventually_True [simp]: "eventually (\x. True) A" + unfolding eventually_def + by (rule is_filter.True [OF is_filter_Rep_filter]) -lemma always_eventually: "\x. P x \ eventually P net" +lemma always_eventually: "\x. P x \ eventually P A" proof - assume "\x. P x" hence "P = (\x. True)" by (simp add: ext) - thus "eventually P net" by simp + thus "eventually P A" by simp qed lemma eventually_mono: - "(\x. P x \ Q x) \ eventually P net \ eventually Q net" -unfolding eventually_def -by (rule is_filter.mono [OF is_filter_Rep_net]) + "(\x. P x \ Q x) \ eventually P A \ eventually Q A" + unfolding eventually_def + by (rule is_filter.mono [OF is_filter_Rep_filter]) lemma eventually_conj: - assumes P: "eventually (\x. P x) net" - assumes Q: "eventually (\x. Q x) net" - shows "eventually (\x. P x \ Q x) net" -using assms unfolding eventually_def -by (rule is_filter.conj [OF is_filter_Rep_net]) + assumes P: "eventually (\x. P x) A" + assumes Q: "eventually (\x. Q x) A" + shows "eventually (\x. P x \ Q x) A" + using assms unfolding eventually_def + by (rule is_filter.conj [OF is_filter_Rep_filter]) lemma eventually_mp: - assumes "eventually (\x. P x \ Q x) net" - assumes "eventually (\x. P x) net" - shows "eventually (\x. Q x) net" + assumes "eventually (\x. P x \ Q x) A" + assumes "eventually (\x. P x) A" + shows "eventually (\x. Q x) A" proof (rule eventually_mono) show "\x. (P x \ Q x) \ P x \ Q x" by simp - show "eventually (\x. (P x \ Q x) \ P x) net" + show "eventually (\x. (P x \ Q x) \ P x) A" using assms by (rule eventually_conj) qed lemma eventually_rev_mp: - assumes "eventually (\x. P x) net" - assumes "eventually (\x. P x \ Q x) net" - shows "eventually (\x. Q x) net" + assumes "eventually (\x. P x) A" + assumes "eventually (\x. P x \ Q x) A" + shows "eventually (\x. Q x) A" using assms(2) assms(1) by (rule eventually_mp) lemma eventually_conj_iff: - "eventually (\x. P x \ Q x) net \ eventually P net \ eventually Q net" -by (auto intro: eventually_conj elim: eventually_rev_mp) + "eventually (\x. P x \ Q x) A \ eventually P A \ eventually Q A" + by (auto intro: eventually_conj elim: eventually_rev_mp) lemma eventually_elim1: - assumes "eventually (\i. P i) net" + assumes "eventually (\i. P i) A" assumes "\i. P i \ Q i" - shows "eventually (\i. Q i) net" -using assms by (auto elim!: eventually_rev_mp) + shows "eventually (\i. Q i) A" + using assms by (auto elim!: eventually_rev_mp) lemma eventually_elim2: - assumes "eventually (\i. P i) net" - assumes "eventually (\i. Q i) net" + assumes "eventually (\i. P i) A" + assumes "eventually (\i. Q i) A" assumes "\i. P i \ Q i \ R i" - shows "eventually (\i. R i) net" -using assms by (auto elim!: eventually_rev_mp) + shows "eventually (\i. R i) A" + using assms by (auto elim!: eventually_rev_mp) subsection {* Finer-than relation *} -text {* @{term "net \ net'"} means that @{term net} is finer than -@{term net'}. *} +text {* @{term "A \ B"} means that filter @{term A} is finer than +filter @{term B}. *} -instantiation net :: (type) complete_lattice +instantiation filter :: (type) complete_lattice begin -definition - le_net_def: "net \ net' \ (\P. eventually P net' \ eventually P net)" +definition le_filter_def: + "A \ B \ (\P. eventually P B \ eventually P A)" definition - less_net_def: "(net :: 'a net) < net' \ net \ net' \ \ net' \ net" + "(A :: 'a filter) < B \ A \ B \ \ B \ A" definition - top_net_def: "top = Abs_net (\P. \x. P x)" + "top = Abs_filter (\P. \x. P x)" definition - bot_net_def: "bot = Abs_net (\P. True)" + "bot = Abs_filter (\P. True)" definition - sup_net_def: "sup net net' = Abs_net (\P. eventually P net \ eventually P net')" + "sup A B = Abs_filter (\P. eventually P A \ eventually P B)" definition - inf_net_def: "inf a b = Abs_net - (\P. \Q R. eventually Q a \ eventually R b \ (\x. Q x \ R x \ P x))" + "inf A B = Abs_filter + (\P. \Q R. eventually Q A \ eventually R B \ (\x. Q x \ R x \ P x))" definition - Sup_net_def: "Sup A = Abs_net (\P. \net\A. eventually P net)" + "Sup S = Abs_filter (\P. \A\S. eventually P A)" definition - Inf_net_def: "Inf A = Sup {x::'a net. \y\A. x \ y}" + "Inf S = Sup {A::'a filter. \B\S. A \ B}" lemma eventually_top [simp]: "eventually P top \ (\x. P x)" -unfolding top_net_def -by (rule eventually_Abs_net, rule is_filter.intro, auto) + unfolding top_filter_def + by (rule eventually_Abs_filter, rule is_filter.intro, auto) lemma eventually_bot [simp]: "eventually P bot" -unfolding bot_net_def -by (subst eventually_Abs_net, rule is_filter.intro, auto) + unfolding bot_filter_def + by (subst eventually_Abs_filter, rule is_filter.intro, auto) lemma eventually_sup: - "eventually P (sup net net') \ eventually P net \ eventually P net'" -unfolding sup_net_def -by (rule eventually_Abs_net, rule is_filter.intro) - (auto elim!: eventually_rev_mp) + "eventually P (sup A B) \ eventually P A \ eventually P B" + unfolding sup_filter_def + by (rule eventually_Abs_filter, rule is_filter.intro) + (auto elim!: eventually_rev_mp) lemma eventually_inf: - "eventually P (inf a b) \ - (\Q R. eventually Q a \ eventually R b \ (\x. Q x \ R x \ P x))" -unfolding inf_net_def -apply (rule eventually_Abs_net, rule is_filter.intro) -apply (fast intro: eventually_True) -apply clarify -apply (intro exI conjI) -apply (erule (1) eventually_conj) -apply (erule (1) eventually_conj) -apply simp -apply auto -done + "eventually P (inf A B) \ + (\Q R. eventually Q A \ eventually R B \ (\x. Q x \ R x \ P x))" + unfolding inf_filter_def + apply (rule eventually_Abs_filter, rule is_filter.intro) + apply (fast intro: eventually_True) + apply clarify + apply (intro exI conjI) + apply (erule (1) eventually_conj) + apply (erule (1) eventually_conj) + apply simp + apply auto + done lemma eventually_Sup: - "eventually P (Sup A) \ (\net\A. eventually P net)" -unfolding Sup_net_def -apply (rule eventually_Abs_net, rule is_filter.intro) -apply (auto intro: eventually_conj elim!: eventually_rev_mp) -done + "eventually P (Sup S) \ (\A\S. eventually P A)" + unfolding Sup_filter_def + apply (rule eventually_Abs_filter, rule is_filter.intro) + apply (auto intro: eventually_conj elim!: eventually_rev_mp) + done instance proof - fix x y :: "'a net" show "x < y \ x \ y \ \ y \ x" - by (rule less_net_def) + fix A B :: "'a filter" show "A < B \ A \ B \ \ B \ A" + by (rule less_filter_def) next - fix x :: "'a net" show "x \ x" - unfolding le_net_def by simp + fix A :: "'a filter" show "A \ A" + unfolding le_filter_def by simp next - fix x y z :: "'a net" assume "x \ y" and "y \ z" thus "x \ z" - unfolding le_net_def by simp + fix A B C :: "'a filter" assume "A \ B" and "B \ C" thus "A \ C" + unfolding le_filter_def by simp next - fix x y :: "'a net" assume "x \ y" and "y \ x" thus "x = y" - unfolding le_net_def expand_net_eq by fast + fix A B :: "'a filter" assume "A \ B" and "B \ A" thus "A = B" + unfolding le_filter_def filter_eq_iff by fast next - fix x :: "'a net" show "x \ top" - unfolding le_net_def eventually_top by (simp add: always_eventually) + fix A :: "'a filter" show "A \ top" + unfolding le_filter_def eventually_top by (simp add: always_eventually) next - fix x :: "'a net" show "bot \ x" - unfolding le_net_def by simp + fix A :: "'a filter" show "bot \ A" + unfolding le_filter_def by simp next - fix x y :: "'a net" show "x \ sup x y" and "y \ sup x y" - unfolding le_net_def eventually_sup by simp_all + fix A B :: "'a filter" show "A \ sup A B" and "B \ sup A B" + unfolding le_filter_def eventually_sup by simp_all next - fix x y z :: "'a net" assume "x \ z" and "y \ z" thus "sup x y \ z" - unfolding le_net_def eventually_sup by simp + fix A B C :: "'a filter" assume "A \ C" and "B \ C" thus "sup A B \ C" + unfolding le_filter_def eventually_sup by simp next - fix x y :: "'a net" show "inf x y \ x" and "inf x y \ y" - unfolding le_net_def eventually_inf by (auto intro: eventually_True) + fix A B :: "'a filter" show "inf A B \ A" and "inf A B \ B" + unfolding le_filter_def eventually_inf by (auto intro: eventually_True) next - fix x y z :: "'a net" assume "x \ y" and "x \ z" thus "x \ inf y z" - unfolding le_net_def eventually_inf + fix A B C :: "'a filter" assume "A \ B" and "A \ C" thus "A \ inf B C" + unfolding le_filter_def eventually_inf by (auto elim!: eventually_mono intro: eventually_conj) next - fix x :: "'a net" and A assume "x \ A" thus "x \ Sup A" - unfolding le_net_def eventually_Sup by simp + fix A :: "'a filter" and S assume "A \ S" thus "A \ Sup S" + unfolding le_filter_def eventually_Sup by simp next - fix A and y :: "'a net" assume "\x. x \ A \ x \ y" thus "Sup A \ y" - unfolding le_net_def eventually_Sup by simp + fix S and B :: "'a filter" assume "\A. A \ S \ A \ B" thus "Sup S \ B" + unfolding le_filter_def eventually_Sup by simp next - fix z :: "'a net" and A assume "z \ A" thus "Inf A \ z" - unfolding le_net_def Inf_net_def eventually_Sup Ball_def by simp + fix C :: "'a filter" and S assume "C \ S" thus "Inf S \ C" + unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp next - fix A and x :: "'a net" assume "\y. y \ A \ x \ y" thus "x \ Inf A" - unfolding le_net_def Inf_net_def eventually_Sup Ball_def by simp + fix S and A :: "'a filter" assume "\B. B \ S \ A \ B" thus "A \ Inf S" + unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp qed end -lemma net_leD: - "net \ net' \ eventually P net' \ eventually P net" -unfolding le_net_def by simp +lemma filter_leD: + "A \ B \ eventually P B \ eventually P A" + unfolding le_filter_def by simp -lemma net_leI: - "(\P. eventually P net' \ eventually P net) \ net \ net'" -unfolding le_net_def by simp +lemma filter_leI: + "(\P. eventually P B \ eventually P A) \ A \ B" + unfolding le_filter_def by simp lemma eventually_False: - "eventually (\x. False) net \ net = bot" -unfolding expand_net_eq by (auto elim: eventually_rev_mp) + "eventually (\x. False) A \ A = bot" + unfolding filter_eq_iff by (auto elim: eventually_rev_mp) -subsection {* Map function for nets *} +subsection {* Map function for filters *} -definition netmap :: "('a \ 'b) \ 'a net \ 'b net" where - "netmap f net = Abs_net (\P. eventually (\x. P (f x)) net)" +definition filtermap :: "('a \ 'b) \ 'a filter \ 'b filter" + where "filtermap f A = Abs_filter (\P. eventually (\x. P (f x)) A)" -lemma eventually_netmap: - "eventually P (netmap f net) = eventually (\x. P (f x)) net" -unfolding netmap_def -apply (rule eventually_Abs_net) -apply (rule is_filter.intro) -apply (auto elim!: eventually_rev_mp) -done +lemma eventually_filtermap: + "eventually P (filtermap f A) = eventually (\x. P (f x)) A" + unfolding filtermap_def + apply (rule eventually_Abs_filter) + apply (rule is_filter.intro) + apply (auto elim!: eventually_rev_mp) + done -lemma netmap_ident: "netmap (\x. x) net = net" -by (simp add: expand_net_eq eventually_netmap) - -lemma netmap_netmap: "netmap f (netmap g net) = netmap (\x. f (g x)) net" -by (simp add: expand_net_eq eventually_netmap) +lemma filtermap_ident: "filtermap (\x. x) A = A" + by (simp add: filter_eq_iff eventually_filtermap) -lemma netmap_mono: "net \ net' \ netmap f net \ netmap f net'" -unfolding le_net_def eventually_netmap by simp +lemma filtermap_filtermap: + "filtermap f (filtermap g A) = filtermap (\x. f (g x)) A" + by (simp add: filter_eq_iff eventually_filtermap) -lemma netmap_bot [simp]: "netmap f bot = bot" -by (simp add: expand_net_eq eventually_netmap) +lemma filtermap_mono: "A \ B \ filtermap f A \ filtermap f B" + unfolding le_filter_def eventually_filtermap by simp + +lemma filtermap_bot [simp]: "filtermap f bot = bot" + by (simp add: filter_eq_iff eventually_filtermap) subsection {* Sequentially *} -definition sequentially :: "nat net" where - "sequentially = Abs_net (\P. \k. \n\k. P n)" +definition sequentially :: "nat filter" + where "sequentially = Abs_filter (\P. \k. \n\k. P n)" lemma eventually_sequentially: "eventually P sequentially \ (\N. \n\N. P n)" unfolding sequentially_def -proof (rule eventually_Abs_net, rule is_filter.intro) +proof (rule eventually_Abs_filter, rule is_filter.intro) fix P Q :: "nat \ bool" assume "\i. \n\i. P n" and "\j. \n\j. Q n" then obtain i j where "\n\i. P n" and "\n\j. Q n" by auto @@ -273,49 +272,48 @@ qed auto lemma sequentially_bot [simp]: "sequentially \ bot" -unfolding expand_net_eq eventually_sequentially by auto + unfolding filter_eq_iff eventually_sequentially by auto lemma eventually_False_sequentially [simp]: "\ eventually (\n. False) sequentially" -by (simp add: eventually_False) + by (simp add: eventually_False) lemma le_sequentially: - "net \ sequentially \ (\N. eventually (\n. N \ n) net)" -unfolding le_net_def eventually_sequentially -by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp) + "A \ sequentially \ (\N. eventually (\n. N \ n) A)" + unfolding le_filter_def eventually_sequentially + by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp) -definition - trivial_limit :: "'a net \ bool" where - "trivial_limit net \ eventually (\x. False) net" +definition trivial_limit :: "'a filter \ bool" + where "trivial_limit A \ eventually (\x. False) A" -lemma trivial_limit_sequentially[intro]: "\ trivial_limit sequentially" +lemma trivial_limit_sequentially [intro]: "\ trivial_limit sequentially" by (auto simp add: trivial_limit_def eventually_sequentially) -subsection {* Standard Nets *} +subsection {* Standard filters *} -definition within :: "'a net \ 'a set \ 'a net" (infixr "within" 70) where - "net within S = Abs_net (\P. eventually (\x. x \ S \ P x) net)" +definition within :: "'a filter \ 'a set \ 'a filter" (infixr "within" 70) + where "A within S = Abs_filter (\P. eventually (\x. x \ S \ P x) A)" -definition nhds :: "'a::topological_space \ 'a net" where - "nhds a = Abs_net (\P. \S. open S \ a \ S \ (\x\S. P x))" +definition nhds :: "'a::topological_space \ 'a filter" + where "nhds a = Abs_filter (\P. \