--- 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 ***
--- 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 (\<lambda>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:
"\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>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:
- "\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
- \<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
-by (simp add: algebra_simps)
-
lemma DERIV_inverse_lemma:
"\<lbrakk>a \<noteq> 0; b \<noteq> (0::'a::real_normed_field)\<rbrakk>
\<Longrightarrow> (inverse a - inverse b) / h
--- 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)
--- 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
--- 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
--- 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
--- 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)
--- 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
--- 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
--- 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 =
--- 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)
--- 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
--- 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
--- 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
--- 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 \<Rightarrow> bool) \<Rightarrow> bool"
- assumes True: "net (\<lambda>x. True)"
- assumes conj: "net (\<lambda>x. P x) \<Longrightarrow> net (\<lambda>x. Q x) \<Longrightarrow> net (\<lambda>x. P x \<and> Q x)"
- assumes mono: "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> net (\<lambda>x. P x) \<Longrightarrow> net (\<lambda>x. Q x)"
+ fixes F :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
+ assumes True: "F (\<lambda>x. True)"
+ assumes conj: "F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x) \<Longrightarrow> F (\<lambda>x. P x \<and> Q x)"
+ assumes mono: "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x)"
-typedef (open) 'a net =
- "{net :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter net}"
+typedef (open) 'a filter = "{F :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter F}"
proof
- show "(\<lambda>x. True) \<in> ?net" by (auto intro: is_filter.intro)
+ show "(\<lambda>x. True) \<in> ?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 \<Rightarrow> bool) \<Rightarrow> 'a net \<Rightarrow> bool" where
- "eventually P net \<longleftrightarrow> Rep_net net P"
+definition eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool"
+ where "eventually P A \<longleftrightarrow> 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' \<longleftrightarrow> (\<forall>P. eventually P net = eventually P net')"
-unfolding Rep_net_inject [symmetric] fun_eq_iff eventually_def ..
+lemma filter_eq_iff:
+ shows "A = B \<longleftrightarrow> (\<forall>P. eventually P A = eventually P B)"
+ unfolding Rep_filter_inject [symmetric] fun_eq_iff eventually_def ..
-lemma eventually_True [simp]: "eventually (\<lambda>x. True) net"
-unfolding eventually_def
-by (rule is_filter.True [OF is_filter_Rep_net])
+lemma eventually_True [simp]: "eventually (\<lambda>x. True) A"
+ unfolding eventually_def
+ by (rule is_filter.True [OF is_filter_Rep_filter])
-lemma always_eventually: "\<forall>x. P x \<Longrightarrow> eventually P net"
+lemma always_eventually: "\<forall>x. P x \<Longrightarrow> eventually P A"
proof -
assume "\<forall>x. P x" hence "P = (\<lambda>x. True)" by (simp add: ext)
- thus "eventually P net" by simp
+ thus "eventually P A" by simp
qed
lemma eventually_mono:
- "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P net \<Longrightarrow> eventually Q net"
-unfolding eventually_def
-by (rule is_filter.mono [OF is_filter_Rep_net])
+ "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P A \<Longrightarrow> eventually Q A"
+ unfolding eventually_def
+ by (rule is_filter.mono [OF is_filter_Rep_filter])
lemma eventually_conj:
- assumes P: "eventually (\<lambda>x. P x) net"
- assumes Q: "eventually (\<lambda>x. Q x) net"
- shows "eventually (\<lambda>x. P x \<and> Q x) net"
-using assms unfolding eventually_def
-by (rule is_filter.conj [OF is_filter_Rep_net])
+ assumes P: "eventually (\<lambda>x. P x) A"
+ assumes Q: "eventually (\<lambda>x. Q x) A"
+ shows "eventually (\<lambda>x. P x \<and> Q x) A"
+ using assms unfolding eventually_def
+ by (rule is_filter.conj [OF is_filter_Rep_filter])
lemma eventually_mp:
- assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) net"
- assumes "eventually (\<lambda>x. P x) net"
- shows "eventually (\<lambda>x. Q x) net"
+ assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) A"
+ assumes "eventually (\<lambda>x. P x) A"
+ shows "eventually (\<lambda>x. Q x) A"
proof (rule eventually_mono)
show "\<forall>x. (P x \<longrightarrow> Q x) \<and> P x \<longrightarrow> Q x" by simp
- show "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) net"
+ show "eventually (\<lambda>x. (P x \<longrightarrow> Q x) \<and> P x) A"
using assms by (rule eventually_conj)
qed
lemma eventually_rev_mp:
- assumes "eventually (\<lambda>x. P x) net"
- assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) net"
- shows "eventually (\<lambda>x. Q x) net"
+ assumes "eventually (\<lambda>x. P x) A"
+ assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) A"
+ shows "eventually (\<lambda>x. Q x) A"
using assms(2) assms(1) by (rule eventually_mp)
lemma eventually_conj_iff:
- "eventually (\<lambda>x. P x \<and> Q x) net \<longleftrightarrow> eventually P net \<and> eventually Q net"
-by (auto intro: eventually_conj elim: eventually_rev_mp)
+ "eventually (\<lambda>x. P x \<and> Q x) A \<longleftrightarrow> eventually P A \<and> eventually Q A"
+ by (auto intro: eventually_conj elim: eventually_rev_mp)
lemma eventually_elim1:
- assumes "eventually (\<lambda>i. P i) net"
+ assumes "eventually (\<lambda>i. P i) A"
assumes "\<And>i. P i \<Longrightarrow> Q i"
- shows "eventually (\<lambda>i. Q i) net"
-using assms by (auto elim!: eventually_rev_mp)
+ shows "eventually (\<lambda>i. Q i) A"
+ using assms by (auto elim!: eventually_rev_mp)
lemma eventually_elim2:
- assumes "eventually (\<lambda>i. P i) net"
- assumes "eventually (\<lambda>i. Q i) net"
+ assumes "eventually (\<lambda>i. P i) A"
+ assumes "eventually (\<lambda>i. Q i) A"
assumes "\<And>i. P i \<Longrightarrow> Q i \<Longrightarrow> R i"
- shows "eventually (\<lambda>i. R i) net"
-using assms by (auto elim!: eventually_rev_mp)
+ shows "eventually (\<lambda>i. R i) A"
+ using assms by (auto elim!: eventually_rev_mp)
subsection {* Finer-than relation *}
-text {* @{term "net \<le> net'"} means that @{term net} is finer than
-@{term net'}. *}
+text {* @{term "A \<le> 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 \<le> net' \<longleftrightarrow> (\<forall>P. eventually P net' \<longrightarrow> eventually P net)"
+definition le_filter_def:
+ "A \<le> B \<longleftrightarrow> (\<forall>P. eventually P B \<longrightarrow> eventually P A)"
definition
- less_net_def: "(net :: 'a net) < net' \<longleftrightarrow> net \<le> net' \<and> \<not> net' \<le> net"
+ "(A :: 'a filter) < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> A"
definition
- top_net_def: "top = Abs_net (\<lambda>P. \<forall>x. P x)"
+ "top = Abs_filter (\<lambda>P. \<forall>x. P x)"
definition
- bot_net_def: "bot = Abs_net (\<lambda>P. True)"
+ "bot = Abs_filter (\<lambda>P. True)"
definition
- sup_net_def: "sup net net' = Abs_net (\<lambda>P. eventually P net \<and> eventually P net')"
+ "sup A B = Abs_filter (\<lambda>P. eventually P A \<and> eventually P B)"
definition
- inf_net_def: "inf a b = Abs_net
- (\<lambda>P. \<exists>Q R. eventually Q a \<and> eventually R b \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
+ "inf A B = Abs_filter
+ (\<lambda>P. \<exists>Q R. eventually Q A \<and> eventually R B \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x))"
definition
- Sup_net_def: "Sup A = Abs_net (\<lambda>P. \<forall>net\<in>A. eventually P net)"
+ "Sup S = Abs_filter (\<lambda>P. \<forall>A\<in>S. eventually P A)"
definition
- Inf_net_def: "Inf A = Sup {x::'a net. \<forall>y\<in>A. x \<le> y}"
+ "Inf S = Sup {A::'a filter. \<forall>B\<in>S. A \<le> B}"
lemma eventually_top [simp]: "eventually P top \<longleftrightarrow> (\<forall>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') \<longleftrightarrow> eventually P net \<and> 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) \<longleftrightarrow> eventually P A \<and> 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) \<longleftrightarrow>
- (\<exists>Q R. eventually Q a \<and> eventually R b \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> 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) \<longleftrightarrow>
+ (\<exists>Q R. eventually Q A \<and> eventually R B \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> 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) \<longleftrightarrow> (\<forall>net\<in>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) \<longleftrightarrow> (\<forall>A\<in>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 \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
- by (rule less_net_def)
+ fix A B :: "'a filter" show "A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> A"
+ by (rule less_filter_def)
next
- fix x :: "'a net" show "x \<le> x"
- unfolding le_net_def by simp
+ fix A :: "'a filter" show "A \<le> A"
+ unfolding le_filter_def by simp
next
- fix x y z :: "'a net" assume "x \<le> y" and "y \<le> z" thus "x \<le> z"
- unfolding le_net_def by simp
+ fix A B C :: "'a filter" assume "A \<le> B" and "B \<le> C" thus "A \<le> C"
+ unfolding le_filter_def by simp
next
- fix x y :: "'a net" assume "x \<le> y" and "y \<le> x" thus "x = y"
- unfolding le_net_def expand_net_eq by fast
+ fix A B :: "'a filter" assume "A \<le> B" and "B \<le> A" thus "A = B"
+ unfolding le_filter_def filter_eq_iff by fast
next
- fix x :: "'a net" show "x \<le> top"
- unfolding le_net_def eventually_top by (simp add: always_eventually)
+ fix A :: "'a filter" show "A \<le> top"
+ unfolding le_filter_def eventually_top by (simp add: always_eventually)
next
- fix x :: "'a net" show "bot \<le> x"
- unfolding le_net_def by simp
+ fix A :: "'a filter" show "bot \<le> A"
+ unfolding le_filter_def by simp
next
- fix x y :: "'a net" show "x \<le> sup x y" and "y \<le> sup x y"
- unfolding le_net_def eventually_sup by simp_all
+ fix A B :: "'a filter" show "A \<le> sup A B" and "B \<le> sup A B"
+ unfolding le_filter_def eventually_sup by simp_all
next
- fix x y z :: "'a net" assume "x \<le> z" and "y \<le> z" thus "sup x y \<le> z"
- unfolding le_net_def eventually_sup by simp
+ fix A B C :: "'a filter" assume "A \<le> C" and "B \<le> C" thus "sup A B \<le> C"
+ unfolding le_filter_def eventually_sup by simp
next
- fix x y :: "'a net" show "inf x y \<le> x" and "inf x y \<le> y"
- unfolding le_net_def eventually_inf by (auto intro: eventually_True)
+ fix A B :: "'a filter" show "inf A B \<le> A" and "inf A B \<le> B"
+ unfolding le_filter_def eventually_inf by (auto intro: eventually_True)
next
- fix x y z :: "'a net" assume "x \<le> y" and "x \<le> z" thus "x \<le> inf y z"
- unfolding le_net_def eventually_inf
+ fix A B C :: "'a filter" assume "A \<le> B" and "A \<le> C" thus "A \<le> 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 \<in> A" thus "x \<le> Sup A"
- unfolding le_net_def eventually_Sup by simp
+ fix A :: "'a filter" and S assume "A \<in> S" thus "A \<le> Sup S"
+ unfolding le_filter_def eventually_Sup by simp
next
- fix A and y :: "'a net" assume "\<And>x. x \<in> A \<Longrightarrow> x \<le> y" thus "Sup A \<le> y"
- unfolding le_net_def eventually_Sup by simp
+ fix S and B :: "'a filter" assume "\<And>A. A \<in> S \<Longrightarrow> A \<le> B" thus "Sup S \<le> B"
+ unfolding le_filter_def eventually_Sup by simp
next
- fix z :: "'a net" and A assume "z \<in> A" thus "Inf A \<le> z"
- unfolding le_net_def Inf_net_def eventually_Sup Ball_def by simp
+ fix C :: "'a filter" and S assume "C \<in> S" thus "Inf S \<le> C"
+ unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp
next
- fix A and x :: "'a net" assume "\<And>y. y \<in> A \<Longrightarrow> x \<le> y" thus "x \<le> Inf A"
- unfolding le_net_def Inf_net_def eventually_Sup Ball_def by simp
+ fix S and A :: "'a filter" assume "\<And>B. B \<in> S \<Longrightarrow> A \<le> B" thus "A \<le> Inf S"
+ unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp
qed
end
-lemma net_leD:
- "net \<le> net' \<Longrightarrow> eventually P net' \<Longrightarrow> eventually P net"
-unfolding le_net_def by simp
+lemma filter_leD:
+ "A \<le> B \<Longrightarrow> eventually P B \<Longrightarrow> eventually P A"
+ unfolding le_filter_def by simp
-lemma net_leI:
- "(\<And>P. eventually P net' \<Longrightarrow> eventually P net) \<Longrightarrow> net \<le> net'"
-unfolding le_net_def by simp
+lemma filter_leI:
+ "(\<And>P. eventually P B \<Longrightarrow> eventually P A) \<Longrightarrow> A \<le> B"
+ unfolding le_filter_def by simp
lemma eventually_False:
- "eventually (\<lambda>x. False) net \<longleftrightarrow> net = bot"
-unfolding expand_net_eq by (auto elim: eventually_rev_mp)
+ "eventually (\<lambda>x. False) A \<longleftrightarrow> 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 \<Rightarrow> 'b) \<Rightarrow> 'a net \<Rightarrow> 'b net" where
- "netmap f net = Abs_net (\<lambda>P. eventually (\<lambda>x. P (f x)) net)"
+definition filtermap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter"
+ where "filtermap f A = Abs_filter (\<lambda>P. eventually (\<lambda>x. P (f x)) A)"
-lemma eventually_netmap:
- "eventually P (netmap f net) = eventually (\<lambda>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 (\<lambda>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 (\<lambda>x. x) net = net"
-by (simp add: expand_net_eq eventually_netmap)
-
-lemma netmap_netmap: "netmap f (netmap g net) = netmap (\<lambda>x. f (g x)) net"
-by (simp add: expand_net_eq eventually_netmap)
+lemma filtermap_ident: "filtermap (\<lambda>x. x) A = A"
+ by (simp add: filter_eq_iff eventually_filtermap)
-lemma netmap_mono: "net \<le> net' \<Longrightarrow> netmap f net \<le> netmap f net'"
-unfolding le_net_def eventually_netmap by simp
+lemma filtermap_filtermap:
+ "filtermap f (filtermap g A) = filtermap (\<lambda>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 \<le> B \<Longrightarrow> filtermap f A \<le> 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 (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)"
+definition sequentially :: "nat filter"
+ where "sequentially = Abs_filter (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)"
lemma eventually_sequentially:
"eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>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 \<Rightarrow> bool"
assume "\<exists>i. \<forall>n\<ge>i. P n" and "\<exists>j. \<forall>n\<ge>j. Q n"
then obtain i j where "\<forall>n\<ge>i. P n" and "\<forall>n\<ge>j. Q n" by auto
@@ -273,49 +272,48 @@
qed auto
lemma sequentially_bot [simp]: "sequentially \<noteq> bot"
-unfolding expand_net_eq eventually_sequentially by auto
+ unfolding filter_eq_iff eventually_sequentially by auto
lemma eventually_False_sequentially [simp]:
"\<not> eventually (\<lambda>n. False) sequentially"
-by (simp add: eventually_False)
+ by (simp add: eventually_False)
lemma le_sequentially:
- "net \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) net)"
-unfolding le_net_def eventually_sequentially
-by (safe, fast, drule_tac x=N in spec, auto elim: eventually_rev_mp)
+ "A \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> 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 \<Rightarrow> bool" where
- "trivial_limit net \<longleftrightarrow> eventually (\<lambda>x. False) net"
+definition trivial_limit :: "'a filter \<Rightarrow> bool"
+ where "trivial_limit A \<longleftrightarrow> eventually (\<lambda>x. False) A"
-lemma trivial_limit_sequentially[intro]: "\<not> trivial_limit sequentially"
+lemma trivial_limit_sequentially [intro]: "\<not> trivial_limit sequentially"
by (auto simp add: trivial_limit_def eventually_sequentially)
-subsection {* Standard Nets *}
+subsection {* Standard filters *}
-definition within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70) where
- "net within S = Abs_net (\<lambda>P. eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) net)"
+definition within :: "'a filter \<Rightarrow> 'a set \<Rightarrow> 'a filter" (infixr "within" 70)
+ where "A within S = Abs_filter (\<lambda>P. eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) A)"
-definition nhds :: "'a::topological_space \<Rightarrow> 'a net" where
- "nhds a = Abs_net (\<lambda>P. \<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
+definition nhds :: "'a::topological_space \<Rightarrow> 'a filter"
+ where "nhds a = Abs_filter (\<lambda>P. \<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
-definition at :: "'a::topological_space \<Rightarrow> 'a net" where
- "at a = nhds a within - {a}"
+definition at :: "'a::topological_space \<Rightarrow> 'a filter"
+ where "at a = nhds a within - {a}"
lemma eventually_within:
- "eventually P (net within S) = eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) net"
-unfolding within_def
-by (rule eventually_Abs_net, rule is_filter.intro)
- (auto elim!: eventually_rev_mp)
+ "eventually P (A within S) = eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) A"
+ unfolding within_def
+ by (rule eventually_Abs_filter, rule is_filter.intro)
+ (auto elim!: eventually_rev_mp)
-lemma within_UNIV: "net within UNIV = net"
- unfolding expand_net_eq eventually_within by simp
+lemma within_UNIV: "A within UNIV = A"
+ unfolding filter_eq_iff eventually_within by simp
lemma eventually_nhds:
"eventually P (nhds a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
unfolding nhds_def
-proof (rule eventually_Abs_net, rule is_filter.intro)
+proof (rule eventually_Abs_filter, rule is_filter.intro)
have "open UNIV \<and> a \<in> UNIV \<and> (\<forall>x\<in>UNIV. True)" by simp
thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. True)" by - rule
next
@@ -354,52 +352,52 @@
subsection {* Boundedness *}
-definition Bfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" where
- "Bfun f net = (\<exists>K>0. eventually (\<lambda>x. norm (f x) \<le> K) net)"
+definition Bfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool"
+ where "Bfun f A = (\<exists>K>0. eventually (\<lambda>x. norm (f x) \<le> K) A)"
lemma BfunI:
- assumes K: "eventually (\<lambda>x. norm (f x) \<le> K) net" shows "Bfun f net"
+ assumes K: "eventually (\<lambda>x. norm (f x) \<le> K) A" shows "Bfun f A"
unfolding Bfun_def
proof (intro exI conjI allI)
show "0 < max K 1" by simp
next
- show "eventually (\<lambda>x. norm (f x) \<le> max K 1) net"
+ show "eventually (\<lambda>x. norm (f x) \<le> max K 1) A"
using K by (rule eventually_elim1, simp)
qed
lemma BfunE:
- assumes "Bfun f net"
- obtains B where "0 < B" and "eventually (\<lambda>x. norm (f x) \<le> B) net"
+ assumes "Bfun f A"
+ obtains B where "0 < B" and "eventually (\<lambda>x. norm (f x) \<le> B) A"
using assms unfolding Bfun_def by fast
subsection {* Convergence to Zero *}
-definition Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" where
- "Zfun f net = (\<forall>r>0. eventually (\<lambda>x. norm (f x) < r) net)"
+definition Zfun :: "('a \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool"
+ where "Zfun f A = (\<forall>r>0. eventually (\<lambda>x. norm (f x) < r) A)"
lemma ZfunI:
- "(\<And>r. 0 < r \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) net) \<Longrightarrow> Zfun f net"
-unfolding Zfun_def by simp
+ "(\<And>r. 0 < r \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) A) \<Longrightarrow> Zfun f A"
+ unfolding Zfun_def by simp
lemma ZfunD:
- "\<lbrakk>Zfun f net; 0 < r\<rbrakk> \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) net"
-unfolding Zfun_def by simp
+ "\<lbrakk>Zfun f A; 0 < r\<rbrakk> \<Longrightarrow> eventually (\<lambda>x. norm (f x) < r) A"
+ unfolding Zfun_def by simp
lemma Zfun_ssubst:
- "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> Zfun g net \<Longrightarrow> Zfun f net"
-unfolding Zfun_def by (auto elim!: eventually_rev_mp)
+ "eventually (\<lambda>x. f x = g x) A \<Longrightarrow> Zfun g A \<Longrightarrow> Zfun f A"
+ unfolding Zfun_def by (auto elim!: eventually_rev_mp)
-lemma Zfun_zero: "Zfun (\<lambda>x. 0) net"
-unfolding Zfun_def by simp
+lemma Zfun_zero: "Zfun (\<lambda>x. 0) A"
+ unfolding Zfun_def by simp
-lemma Zfun_norm_iff: "Zfun (\<lambda>x. norm (f x)) net = Zfun (\<lambda>x. f x) net"
-unfolding Zfun_def by simp
+lemma Zfun_norm_iff: "Zfun (\<lambda>x. norm (f x)) A = Zfun (\<lambda>x. f x) A"
+ unfolding Zfun_def by simp
lemma Zfun_imp_Zfun:
- assumes f: "Zfun f net"
- assumes g: "eventually (\<lambda>x. norm (g x) \<le> norm (f x) * K) net"
- shows "Zfun (\<lambda>x. g x) net"
+ assumes f: "Zfun f A"
+ assumes g: "eventually (\<lambda>x. norm (g x) \<le> norm (f x) * K) A"
+ shows "Zfun (\<lambda>x. g x) A"
proof (cases)
assume K: "0 < K"
show ?thesis
@@ -407,9 +405,9 @@
fix r::real assume "0 < r"
hence "0 < r / K"
using K by (rule divide_pos_pos)
- then have "eventually (\<lambda>x. norm (f x) < r / K) net"
+ then have "eventually (\<lambda>x. norm (f x) < r / K) A"
using ZfunD [OF f] by fast
- with g show "eventually (\<lambda>x. norm (g x) < r) net"
+ with g show "eventually (\<lambda>x. norm (g x) < r) A"
proof (rule eventually_elim2)
fix x
assume *: "norm (g x) \<le> norm (f x) * K"
@@ -427,7 +425,7 @@
proof (rule ZfunI)
fix r :: real
assume "0 < r"
- from g show "eventually (\<lambda>x. norm (g x) < r) net"
+ from g show "eventually (\<lambda>x. norm (g x) < r) A"
proof (rule eventually_elim1)
fix x
assume "norm (g x) \<le> norm (f x) * K"
@@ -439,22 +437,22 @@
qed
qed
-lemma Zfun_le: "\<lbrakk>Zfun g net; \<forall>x. norm (f x) \<le> norm (g x)\<rbrakk> \<Longrightarrow> Zfun f net"
-by (erule_tac K="1" in Zfun_imp_Zfun, simp)
+lemma Zfun_le: "\<lbrakk>Zfun g A; \<forall>x. norm (f x) \<le> norm (g x)\<rbrakk> \<Longrightarrow> Zfun f A"
+ by (erule_tac K="1" in Zfun_imp_Zfun, simp)
lemma Zfun_add:
- assumes f: "Zfun f net" and g: "Zfun g net"
- shows "Zfun (\<lambda>x. f x + g x) net"
+ assumes f: "Zfun f A" and g: "Zfun g A"
+ shows "Zfun (\<lambda>x. f x + g x) A"
proof (rule ZfunI)
fix r::real assume "0 < r"
hence r: "0 < r / 2" by simp
- have "eventually (\<lambda>x. norm (f x) < r/2) net"
+ have "eventually (\<lambda>x. norm (f x) < r/2) A"
using f r by (rule ZfunD)
moreover
- have "eventually (\<lambda>x. norm (g x) < r/2) net"
+ have "eventually (\<lambda>x. norm (g x) < r/2) A"
using g r by (rule ZfunD)
ultimately
- show "eventually (\<lambda>x. norm (f x + g x) < r) net"
+ show "eventually (\<lambda>x. norm (f x + g x) < r) A"
proof (rule eventually_elim2)
fix x
assume *: "norm (f x) < r/2" "norm (g x) < r/2"
@@ -467,28 +465,28 @@
qed
qed
-lemma Zfun_minus: "Zfun f net \<Longrightarrow> Zfun (\<lambda>x. - f x) net"
-unfolding Zfun_def by simp
+lemma Zfun_minus: "Zfun f A \<Longrightarrow> Zfun (\<lambda>x. - f x) A"
+ unfolding Zfun_def by simp
-lemma Zfun_diff: "\<lbrakk>Zfun f net; Zfun g net\<rbrakk> \<Longrightarrow> Zfun (\<lambda>x. f x - g x) net"
-by (simp only: diff_minus Zfun_add Zfun_minus)
+lemma Zfun_diff: "\<lbrakk>Zfun f A; Zfun g A\<rbrakk> \<Longrightarrow> Zfun (\<lambda>x. f x - g x) A"
+ by (simp only: diff_minus Zfun_add Zfun_minus)
lemma (in bounded_linear) Zfun:
- assumes g: "Zfun g net"
- shows "Zfun (\<lambda>x. f (g x)) net"
+ assumes g: "Zfun g A"
+ shows "Zfun (\<lambda>x. f (g x)) A"
proof -
obtain K where "\<And>x. norm (f x) \<le> norm x * K"
using bounded by fast
- then have "eventually (\<lambda>x. norm (f (g x)) \<le> norm (g x) * K) net"
+ then have "eventually (\<lambda>x. norm (f (g x)) \<le> norm (g x) * K) A"
by simp
with g show ?thesis
by (rule Zfun_imp_Zfun)
qed
lemma (in bounded_bilinear) Zfun:
- assumes f: "Zfun f net"
- assumes g: "Zfun g net"
- shows "Zfun (\<lambda>x. f x ** g x) net"
+ assumes f: "Zfun f A"
+ assumes g: "Zfun g A"
+ shows "Zfun (\<lambda>x. f x ** g x) A"
proof (rule ZfunI)
fix r::real assume r: "0 < r"
obtain K where K: "0 < K"
@@ -496,13 +494,13 @@
using pos_bounded by fast
from K have K': "0 < inverse K"
by (rule positive_imp_inverse_positive)
- have "eventually (\<lambda>x. norm (f x) < r) net"
+ have "eventually (\<lambda>x. norm (f x) < r) A"
using f r by (rule ZfunD)
moreover
- have "eventually (\<lambda>x. norm (g x) < inverse K) net"
+ have "eventually (\<lambda>x. norm (g x) < inverse K) A"
using g K' by (rule ZfunD)
ultimately
- show "eventually (\<lambda>x. norm (f x ** g x) < r) net"
+ show "eventually (\<lambda>x. norm (f x ** g x) < r) A"
proof (rule eventually_elim2)
fix x
assume *: "norm (f x) < r" "norm (g x) < inverse K"
@@ -517,12 +515,12 @@
qed
lemma (in bounded_bilinear) Zfun_left:
- "Zfun f net \<Longrightarrow> Zfun (\<lambda>x. f x ** a) net"
-by (rule bounded_linear_left [THEN bounded_linear.Zfun])
+ "Zfun f A \<Longrightarrow> Zfun (\<lambda>x. f x ** a) A"
+ by (rule bounded_linear_left [THEN bounded_linear.Zfun])
lemma (in bounded_bilinear) Zfun_right:
- "Zfun f net \<Longrightarrow> Zfun (\<lambda>x. a ** f x) net"
-by (rule bounded_linear_right [THEN bounded_linear.Zfun])
+ "Zfun f A \<Longrightarrow> Zfun (\<lambda>x. a ** f x) A"
+ by (rule bounded_linear_right [THEN bounded_linear.Zfun])
lemmas Zfun_mult = mult.Zfun
lemmas Zfun_mult_right = mult.Zfun_right
@@ -531,9 +529,9 @@
subsection {* Limits *}
-definition tendsto :: "('a \<Rightarrow> 'b::topological_space) \<Rightarrow> 'b \<Rightarrow> 'a net \<Rightarrow> bool"
+definition tendsto :: "('a \<Rightarrow> 'b::topological_space) \<Rightarrow> 'b \<Rightarrow> 'a filter \<Rightarrow> bool"
(infixr "--->" 55) where
- "(f ---> l) net \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
+ "(f ---> l) A \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) A)"
ML {*
structure Tendsto_Intros = Named_Thms
@@ -545,74 +543,74 @@
setup Tendsto_Intros.setup
-lemma tendsto_mono: "net \<le> net' \<Longrightarrow> (f ---> l) net' \<Longrightarrow> (f ---> l) net"
-unfolding tendsto_def le_net_def by fast
+lemma tendsto_mono: "A \<le> A' \<Longrightarrow> (f ---> l) A' \<Longrightarrow> (f ---> l) A"
+ unfolding tendsto_def le_filter_def by fast
lemma topological_tendstoI:
- "(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net)
- \<Longrightarrow> (f ---> l) net"
+ "(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) A)
+ \<Longrightarrow> (f ---> l) A"
unfolding tendsto_def by auto
lemma topological_tendstoD:
- "(f ---> l) net \<Longrightarrow> open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) net"
+ "(f ---> l) A \<Longrightarrow> open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) A"
unfolding tendsto_def by auto
lemma tendstoI:
- assumes "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net"
- shows "(f ---> l) net"
-apply (rule topological_tendstoI)
-apply (simp add: open_dist)
-apply (drule (1) bspec, clarify)
-apply (drule assms)
-apply (erule eventually_elim1, simp)
-done
+ assumes "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) A"
+ shows "(f ---> l) A"
+ apply (rule topological_tendstoI)
+ apply (simp add: open_dist)
+ apply (drule (1) bspec, clarify)
+ apply (drule assms)
+ apply (erule eventually_elim1, simp)
+ done
lemma tendstoD:
- "(f ---> l) net \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) net"
-apply (drule_tac S="{x. dist x l < e}" in topological_tendstoD)
-apply (clarsimp simp add: open_dist)
-apply (rule_tac x="e - dist x l" in exI, clarsimp)
-apply (simp only: less_diff_eq)
-apply (erule le_less_trans [OF dist_triangle])
-apply simp
-apply simp
-done
+ "(f ---> l) A \<Longrightarrow> 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) A"
+ apply (drule_tac S="{x. dist x l < e}" in topological_tendstoD)
+ apply (clarsimp simp add: open_dist)
+ apply (rule_tac x="e - dist x l" in exI, clarsimp)
+ apply (simp only: less_diff_eq)
+ apply (erule le_less_trans [OF dist_triangle])
+ apply simp
+ apply simp
+ done
lemma tendsto_iff:
- "(f ---> l) net \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
-using tendstoI tendstoD by fast
+ "(f ---> l) A \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) A)"
+ using tendstoI tendstoD by fast
-lemma tendsto_Zfun_iff: "(f ---> a) net = Zfun (\<lambda>x. f x - a) net"
-by (simp only: tendsto_iff Zfun_def dist_norm)
+lemma tendsto_Zfun_iff: "(f ---> a) A = Zfun (\<lambda>x. f x - a) A"
+ by (simp only: tendsto_iff Zfun_def dist_norm)
lemma tendsto_ident_at [tendsto_intros]: "((\<lambda>x. x) ---> a) (at a)"
-unfolding tendsto_def eventually_at_topological by auto
+ unfolding tendsto_def eventually_at_topological by auto
lemma tendsto_ident_at_within [tendsto_intros]:
"((\<lambda>x. x) ---> a) (at a within S)"
-unfolding tendsto_def eventually_within eventually_at_topological by auto
+ unfolding tendsto_def eventually_within eventually_at_topological by auto
-lemma tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) net"
-by (simp add: tendsto_def)
+lemma tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) A"
+ by (simp add: tendsto_def)
lemma tendsto_const_iff:
fixes k l :: "'a::metric_space"
- assumes "net \<noteq> bot" shows "((\<lambda>n. k) ---> l) net \<longleftrightarrow> k = l"
-apply (safe intro!: tendsto_const)
-apply (rule ccontr)
-apply (drule_tac e="dist k l" in tendstoD)
-apply (simp add: zero_less_dist_iff)
-apply (simp add: eventually_False assms)
-done
+ assumes "A \<noteq> bot" shows "((\<lambda>n. k) ---> l) A \<longleftrightarrow> k = l"
+ apply (safe intro!: tendsto_const)
+ apply (rule ccontr)
+ apply (drule_tac e="dist k l" in tendstoD)
+ apply (simp add: zero_less_dist_iff)
+ apply (simp add: eventually_False assms)
+ done
lemma tendsto_dist [tendsto_intros]:
- assumes f: "(f ---> l) net" and g: "(g ---> m) net"
- shows "((\<lambda>x. dist (f x) (g x)) ---> dist l m) net"
+ assumes f: "(f ---> l) A" and g: "(g ---> m) A"
+ shows "((\<lambda>x. dist (f x) (g x)) ---> dist l m) A"
proof (rule tendstoI)
fix e :: real assume "0 < e"
hence e2: "0 < e/2" by simp
from tendstoD [OF f e2] tendstoD [OF g e2]
- show "eventually (\<lambda>x. dist (dist (f x) (g x)) (dist l m) < e) net"
+ show "eventually (\<lambda>x. dist (dist (f x) (g x)) (dist l m) < e) A"
proof (rule eventually_elim2)
fix x assume "dist (f x) l < e/2" "dist (g x) m < e/2"
then show "dist (dist (f x) (g x)) (dist l m) < e"
@@ -626,58 +624,48 @@
qed
lemma norm_conv_dist: "norm x = dist x 0"
-unfolding dist_norm by simp
+ unfolding dist_norm by simp
lemma tendsto_norm [tendsto_intros]:
- "(f ---> a) net \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> norm a) net"
-unfolding norm_conv_dist by (intro tendsto_intros)
+ "(f ---> a) A \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> norm a) A"
+ unfolding norm_conv_dist by (intro tendsto_intros)
lemma tendsto_norm_zero:
- "(f ---> 0) net \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> 0) net"
-by (drule tendsto_norm, simp)
+ "(f ---> 0) A \<Longrightarrow> ((\<lambda>x. norm (f x)) ---> 0) A"
+ by (drule tendsto_norm, simp)
lemma tendsto_norm_zero_cancel:
- "((\<lambda>x. norm (f x)) ---> 0) net \<Longrightarrow> (f ---> 0) net"
-unfolding tendsto_iff dist_norm by simp
+ "((\<lambda>x. norm (f x)) ---> 0) A \<Longrightarrow> (f ---> 0) A"
+ unfolding tendsto_iff dist_norm by simp
lemma tendsto_norm_zero_iff:
- "((\<lambda>x. norm (f x)) ---> 0) net \<longleftrightarrow> (f ---> 0) net"
-unfolding tendsto_iff dist_norm by simp
-
-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 minus_diff_minus:
- fixes a b :: "'a::ab_group_add"
- shows "(- a) - (- b) = - (a - b)"
-by simp
+ "((\<lambda>x. norm (f x)) ---> 0) A \<longleftrightarrow> (f ---> 0) A"
+ unfolding tendsto_iff dist_norm by simp
lemma tendsto_add [tendsto_intros]:
fixes a b :: "'a::real_normed_vector"
- shows "\<lbrakk>(f ---> a) net; (g ---> b) net\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) ---> a + b) net"
-by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add)
+ shows "\<lbrakk>(f ---> a) A; (g ---> b) A\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) ---> a + b) A"
+ by (simp only: tendsto_Zfun_iff add_diff_add Zfun_add)
lemma tendsto_minus [tendsto_intros]:
fixes a :: "'a::real_normed_vector"
- shows "(f ---> a) net \<Longrightarrow> ((\<lambda>x. - f x) ---> - a) net"
-by (simp only: tendsto_Zfun_iff minus_diff_minus Zfun_minus)
+ shows "(f ---> a) A \<Longrightarrow> ((\<lambda>x. - f x) ---> - a) A"
+ by (simp only: tendsto_Zfun_iff minus_diff_minus Zfun_minus)
lemma tendsto_minus_cancel:
fixes a :: "'a::real_normed_vector"
- shows "((\<lambda>x. - f x) ---> - a) net \<Longrightarrow> (f ---> a) net"
-by (drule tendsto_minus, simp)
+ shows "((\<lambda>x. - f x) ---> - a) A \<Longrightarrow> (f ---> a) A"
+ by (drule tendsto_minus, simp)
lemma tendsto_diff [tendsto_intros]:
fixes a b :: "'a::real_normed_vector"
- shows "\<lbrakk>(f ---> a) net; (g ---> b) net\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x - g x) ---> a - b) net"
-by (simp add: diff_minus tendsto_add tendsto_minus)
+ shows "\<lbrakk>(f ---> a) A; (g ---> b) A\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x - g x) ---> a - b) A"
+ by (simp add: diff_minus tendsto_add tendsto_minus)
lemma tendsto_setsum [tendsto_intros]:
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_vector"
- assumes "\<And>i. i \<in> S \<Longrightarrow> (f i ---> a i) net"
- shows "((\<lambda>x. \<Sum>i\<in>S. f i x) ---> (\<Sum>i\<in>S. a i)) net"
+ assumes "\<And>i. i \<in> S \<Longrightarrow> (f i ---> a i) A"
+ shows "((\<lambda>x. \<Sum>i\<in>S. f i x) ---> (\<Sum>i\<in>S. a i)) A"
proof (cases "finite S")
assume "finite S" thus ?thesis using assms
proof (induct set: finite)
@@ -693,29 +681,29 @@
qed
lemma (in bounded_linear) tendsto [tendsto_intros]:
- "(g ---> a) net \<Longrightarrow> ((\<lambda>x. f (g x)) ---> f a) net"
-by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun)
+ "(g ---> a) A \<Longrightarrow> ((\<lambda>x. f (g x)) ---> f a) A"
+ by (simp only: tendsto_Zfun_iff diff [symmetric] Zfun)
lemma (in bounded_bilinear) tendsto [tendsto_intros]:
- "\<lbrakk>(f ---> a) net; (g ---> b) net\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ** g x) ---> a ** b) net"
-by (simp only: tendsto_Zfun_iff prod_diff_prod
- Zfun_add Zfun Zfun_left Zfun_right)
+ "\<lbrakk>(f ---> a) A; (g ---> b) A\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x ** g x) ---> a ** b) A"
+ by (simp only: tendsto_Zfun_iff prod_diff_prod
+ Zfun_add Zfun Zfun_left Zfun_right)
subsection {* Continuity of Inverse *}
lemma (in bounded_bilinear) Zfun_prod_Bfun:
- assumes f: "Zfun f net"
- assumes g: "Bfun g net"
- shows "Zfun (\<lambda>x. f x ** g x) net"
+ assumes f: "Zfun f A"
+ assumes g: "Bfun g A"
+ shows "Zfun (\<lambda>x. f x ** g x) A"
proof -
obtain K where K: "0 \<le> K"
and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
using nonneg_bounded by fast
obtain B where B: "0 < B"
- and norm_g: "eventually (\<lambda>x. norm (g x) \<le> B) net"
+ and norm_g: "eventually (\<lambda>x. norm (g x) \<le> B) A"
using g by (rule BfunE)
- have "eventually (\<lambda>x. norm (f x ** g x) \<le> norm (f x) * (B * K)) net"
+ have "eventually (\<lambda>x. norm (f x ** g x) \<le> norm (f x) * (B * K)) A"
using norm_g proof (rule eventually_elim1)
fix x
assume *: "norm (g x) \<le> B"
@@ -734,44 +722,39 @@
lemma (in bounded_bilinear) flip:
"bounded_bilinear (\<lambda>x y. y ** x)"
-apply default
-apply (rule add_right)
-apply (rule add_left)
-apply (rule scaleR_right)
-apply (rule scaleR_left)
-apply (subst mult_commute)
-using bounded by fast
+ apply default
+ apply (rule add_right)
+ apply (rule add_left)
+ apply (rule scaleR_right)
+ apply (rule scaleR_left)
+ apply (subst mult_commute)
+ using bounded by fast
lemma (in bounded_bilinear) Bfun_prod_Zfun:
- assumes f: "Bfun f net"
- assumes g: "Zfun g net"
- shows "Zfun (\<lambda>x. f x ** g x) net"
-using flip g f by (rule bounded_bilinear.Zfun_prod_Bfun)
-
-lemma inverse_diff_inverse:
- "\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
- \<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
-by (simp add: algebra_simps)
+ assumes f: "Bfun f A"
+ assumes g: "Zfun g A"
+ shows "Zfun (\<lambda>x. f x ** g x) A"
+ using flip g f by (rule bounded_bilinear.Zfun_prod_Bfun)
lemma Bfun_inverse_lemma:
fixes x :: "'a::real_normed_div_algebra"
shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r"
-apply (subst nonzero_norm_inverse, clarsimp)
-apply (erule (1) le_imp_inverse_le)
-done
+ apply (subst nonzero_norm_inverse, clarsimp)
+ apply (erule (1) le_imp_inverse_le)
+ done
lemma Bfun_inverse:
fixes a :: "'a::real_normed_div_algebra"
- assumes f: "(f ---> a) net"
+ assumes f: "(f ---> a) A"
assumes a: "a \<noteq> 0"
- shows "Bfun (\<lambda>x. inverse (f x)) net"
+ shows "Bfun (\<lambda>x. inverse (f x)) A"
proof -
from a have "0 < norm a" by simp
hence "\<exists>r>0. r < norm a" by (rule dense)
then obtain r where r1: "0 < r" and r2: "r < norm a" by fast
- have "eventually (\<lambda>x. dist (f x) a < r) net"
+ have "eventually (\<lambda>x. dist (f x) a < r) A"
using tendstoD [OF f r1] by fast
- hence "eventually (\<lambda>x. norm (inverse (f x)) \<le> inverse (norm a - r)) net"
+ hence "eventually (\<lambda>x. norm (inverse (f x)) \<le> inverse (norm a - r)) A"
proof (rule eventually_elim1)
fix x
assume "dist (f x) a < r"
@@ -798,29 +781,29 @@
lemma tendsto_inverse_lemma:
fixes a :: "'a::real_normed_div_algebra"
- shows "\<lbrakk>(f ---> a) net; a \<noteq> 0; eventually (\<lambda>x. f x \<noteq> 0) net\<rbrakk>
- \<Longrightarrow> ((\<lambda>x. inverse (f x)) ---> inverse a) net"
-apply (subst tendsto_Zfun_iff)
-apply (rule Zfun_ssubst)
-apply (erule eventually_elim1)
-apply (erule (1) inverse_diff_inverse)
-apply (rule Zfun_minus)
-apply (rule Zfun_mult_left)
-apply (rule mult.Bfun_prod_Zfun)
-apply (erule (1) Bfun_inverse)
-apply (simp add: tendsto_Zfun_iff)
-done
+ shows "\<lbrakk>(f ---> a) A; a \<noteq> 0; eventually (\<lambda>x. f x \<noteq> 0) A\<rbrakk>
+ \<Longrightarrow> ((\<lambda>x. inverse (f x)) ---> inverse a) A"
+ apply (subst tendsto_Zfun_iff)
+ apply (rule Zfun_ssubst)
+ apply (erule eventually_elim1)
+ apply (erule (1) inverse_diff_inverse)
+ apply (rule Zfun_minus)
+ apply (rule Zfun_mult_left)
+ apply (rule mult.Bfun_prod_Zfun)
+ apply (erule (1) Bfun_inverse)
+ apply (simp add: tendsto_Zfun_iff)
+ done
lemma tendsto_inverse [tendsto_intros]:
fixes a :: "'a::real_normed_div_algebra"
- assumes f: "(f ---> a) net"
+ assumes f: "(f ---> a) A"
assumes a: "a \<noteq> 0"
- shows "((\<lambda>x. inverse (f x)) ---> inverse a) net"
+ shows "((\<lambda>x. inverse (f x)) ---> inverse a) A"
proof -
from a have "0 < norm a" by simp
- with f have "eventually (\<lambda>x. dist (f x) a < norm a) net"
+ with f have "eventually (\<lambda>x. dist (f x) a < norm a) A"
by (rule tendstoD)
- then have "eventually (\<lambda>x. f x \<noteq> 0) net"
+ then have "eventually (\<lambda>x. f x \<noteq> 0) A"
unfolding dist_norm by (auto elim!: eventually_elim1)
with f a show ?thesis
by (rule tendsto_inverse_lemma)
@@ -828,32 +811,32 @@
lemma tendsto_divide [tendsto_intros]:
fixes a b :: "'a::real_normed_field"
- shows "\<lbrakk>(f ---> a) net; (g ---> b) net; b \<noteq> 0\<rbrakk>
- \<Longrightarrow> ((\<lambda>x. f x / g x) ---> a / b) net"
-by (simp add: mult.tendsto tendsto_inverse divide_inverse)
+ shows "\<lbrakk>(f ---> a) A; (g ---> b) A; b \<noteq> 0\<rbrakk>
+ \<Longrightarrow> ((\<lambda>x. f x / g x) ---> a / b) A"
+ by (simp add: mult.tendsto tendsto_inverse divide_inverse)
lemma tendsto_unique:
fixes f :: "'a \<Rightarrow> 'b::t2_space"
- assumes "\<not> trivial_limit net" "(f ---> l) net" "(f ---> l') net"
+ assumes "\<not> trivial_limit A" "(f ---> l) A" "(f ---> l') A"
shows "l = l'"
proof (rule ccontr)
assume "l \<noteq> l'"
obtain U V where "open U" "open V" "l \<in> U" "l' \<in> V" "U \<inter> V = {}"
using hausdorff [OF `l \<noteq> l'`] by fast
- have "eventually (\<lambda>x. f x \<in> U) net"
- using `(f ---> l) net` `open U` `l \<in> U` by (rule topological_tendstoD)
+ have "eventually (\<lambda>x. f x \<in> U) A"
+ using `(f ---> l) A` `open U` `l \<in> U` by (rule topological_tendstoD)
moreover
- have "eventually (\<lambda>x. f x \<in> V) net"
- using `(f ---> l') net` `open V` `l' \<in> V` by (rule topological_tendstoD)
+ have "eventually (\<lambda>x. f x \<in> V) A"
+ using `(f ---> l') A` `open V` `l' \<in> V` by (rule topological_tendstoD)
ultimately
- have "eventually (\<lambda>x. False) net"
+ have "eventually (\<lambda>x. False) A"
proof (rule eventually_elim2)
fix x
assume "f x \<in> U" "f x \<in> V"
hence "f x \<in> U \<inter> V" by simp
with `U \<inter> V = {}` show "False" by simp
qed
- with `\<not> trivial_limit net` show "False"
+ with `\<not> trivial_limit A` show "False"
by (simp add: trivial_limit_def)
qed
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Mon Aug 08 22:33:36 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Tue Aug 09 07:44:17 2011 +0200
@@ -1310,25 +1310,19 @@
instance cart :: (perfect_space, finite) perfect_space
proof
fix x :: "'a ^ 'b"
- {
- fix e :: real assume "0 < e"
- def a \<equiv> "x $ undefined"
- have "a islimpt UNIV" by (rule islimpt_UNIV)
- with `0 < e` obtain b where "b \<noteq> a" and "dist b a < e"
- unfolding islimpt_approachable by auto
- def y \<equiv> "Cart_lambda ((Cart_nth x)(undefined := b))"
- from `b \<noteq> a` have "y \<noteq> x"
- unfolding a_def y_def by (simp add: Cart_eq)
- from `dist b a < e` have "dist y x < e"
- unfolding dist_vector_def a_def y_def
- apply simp
- apply (rule le_less_trans [OF setL2_le_setsum [OF zero_le_dist]])
- apply (subst setsum_diff1' [where a=undefined], simp, simp, simp)
- done
- from `y \<noteq> x` and `dist y x < e`
- have "\<exists>y\<in>UNIV. y \<noteq> x \<and> dist y x < e" by auto
- }
- then show "x islimpt UNIV" unfolding islimpt_approachable by blast
+ show "x islimpt UNIV"
+ apply (rule islimptI)
+ apply (unfold open_vector_def)
+ apply (drule (1) bspec)
+ apply clarsimp
+ apply (subgoal_tac "\<forall>i\<in>UNIV. \<exists>y. y \<in> A i \<and> y \<noteq> x $ i")
+ apply (drule finite_choice [OF finite_UNIV], erule exE)
+ apply (rule_tac x="Cart_lambda f" in exI)
+ apply (simp add: Cart_eq)
+ apply (rule ballI, drule_tac x=i in spec, clarify)
+ apply (cut_tac x="x $ i" in islimpt_UNIV)
+ apply (simp add: islimpt_def)
+ done
qed
lemma closed_positive_orthant: "closed {x::real^'n. \<forall>i. 0 \<le>x$i}"
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Mon Aug 08 22:33:36 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Aug 09 07:44:17 2011 +0200
@@ -18,7 +18,7 @@
nets of a particular form. This lets us prove theorems generally and use
"at a" or "at a within s" for restriction to a set (1-sided on R etc.) *}
-definition has_derivative :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a net \<Rightarrow> bool)"
+definition has_derivative :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a filter \<Rightarrow> bool)"
(infixl "(has'_derivative)" 12) where
"(f has_derivative f') net \<equiv> bounded_linear f' \<and> ((\<lambda>y. (1 / (norm (y - netlimit net))) *\<^sub>R
(f y - (f (netlimit net) + f'(y - netlimit net)))) ---> 0) net"
@@ -291,7 +291,7 @@
no_notation Deriv.differentiable (infixl "differentiable" 60)
-definition differentiable :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" (infixr "differentiable" 30) where
+definition differentiable :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool" (infixr "differentiable" 30) where
"f differentiable net \<equiv> (\<exists>f'. (f has_derivative f') net)"
definition differentiable_on :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "differentiable'_on" 30) where
@@ -469,25 +469,25 @@
subsection {* Composition rules stated just for differentiability. *}
-lemma differentiable_const[intro]: "(\<lambda>z. c) differentiable (net::'a::real_normed_vector net)"
+lemma differentiable_const[intro]: "(\<lambda>z. c) differentiable (net::'a::real_normed_vector filter)"
unfolding differentiable_def using has_derivative_const by auto
-lemma differentiable_id[intro]: "(\<lambda>z. z) differentiable (net::'a::real_normed_vector net)"
+lemma differentiable_id[intro]: "(\<lambda>z. z) differentiable (net::'a::real_normed_vector filter)"
unfolding differentiable_def using has_derivative_id by auto
-lemma differentiable_cmul[intro]: "f differentiable net \<Longrightarrow> (\<lambda>x. c *\<^sub>R f(x)) differentiable (net::'a::real_normed_vector net)"
+lemma differentiable_cmul[intro]: "f differentiable net \<Longrightarrow> (\<lambda>x. c *\<^sub>R f(x)) differentiable (net::'a::real_normed_vector filter)"
unfolding differentiable_def apply(erule exE, drule has_derivative_cmul) by auto
-lemma differentiable_neg[intro]: "f differentiable net \<Longrightarrow> (\<lambda>z. -(f z)) differentiable (net::'a::real_normed_vector net)"
+lemma differentiable_neg[intro]: "f differentiable net \<Longrightarrow> (\<lambda>z. -(f z)) differentiable (net::'a::real_normed_vector filter)"
unfolding differentiable_def apply(erule exE, drule has_derivative_neg) by auto
lemma differentiable_add: "f differentiable net \<Longrightarrow> g differentiable net
- \<Longrightarrow> (\<lambda>z. f z + g z) differentiable (net::'a::real_normed_vector net)"
+ \<Longrightarrow> (\<lambda>z. f z + g z) differentiable (net::'a::real_normed_vector filter)"
unfolding differentiable_def apply(erule exE)+ apply(rule_tac x="\<lambda>z. f' z + f'a z" in exI)
apply(rule has_derivative_add) by auto
lemma differentiable_sub: "f differentiable net \<Longrightarrow> g differentiable net
- \<Longrightarrow> (\<lambda>z. f z - g z) differentiable (net::'a::real_normed_vector net)"
+ \<Longrightarrow> (\<lambda>z. f z - g z) differentiable (net::'a::real_normed_vector filter)"
unfolding differentiable_def apply(erule exE)+ apply(rule_tac x="\<lambda>z. f' z - f'a z" in exI)
apply(rule has_derivative_sub) by auto
@@ -1259,7 +1259,7 @@
subsection {* Considering derivative @{typ "real \<Rightarrow> 'b\<Colon>real_normed_vector"} as a vector. *}
-definition has_vector_derivative :: "(real \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'b \<Rightarrow> (real net \<Rightarrow> bool)"
+definition has_vector_derivative :: "(real \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'b \<Rightarrow> (real filter \<Rightarrow> bool)"
(infixl "has'_vector'_derivative" 12) where
"(f has_vector_derivative f') net \<equiv> (f has_derivative (\<lambda>x. x *\<^sub>R f')) net"
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Aug 08 22:33:36 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Aug 09 07:44:17 2011 +0200
@@ -1,6 +1,7 @@
(* title: HOL/Library/Topology_Euclidian_Space.thy
Author: Amine Chaieb, University of Cambridge
Author: Robert Himmelmann, TU Muenchen
+ Author: Brian Huffman, Portland State University
*)
header {* Elementary topology in Euclidean space. *}
@@ -464,11 +465,10 @@
by metis
class perfect_space =
- (* FIXME: perfect_space should inherit from topological_space *)
- assumes islimpt_UNIV [simp, intro]: "(x::'a::metric_space) islimpt UNIV"
+ assumes islimpt_UNIV [simp, intro]: "(x::'a::topological_space) islimpt UNIV"
lemma perfect_choose_dist:
- fixes x :: "'a::perfect_space"
+ fixes x :: "'a::{perfect_space, metric_space}"
shows "0 < r \<Longrightarrow> \<exists>a. a \<noteq> x \<and> dist a x < r"
using islimpt_UNIV [of x]
by (simp add: islimpt_approachable)
@@ -599,22 +599,12 @@
lemma interior_limit_point [intro]:
fixes x :: "'a::perfect_space"
assumes x: "x \<in> interior S" shows "x islimpt S"
-proof-
- from x obtain e where e: "e>0" "\<forall>x'. dist x x' < e \<longrightarrow> x' \<in> S"
- unfolding mem_interior subset_eq Ball_def mem_ball by blast
- {
- fix d::real assume d: "d>0"
- let ?m = "min d e"
- have mde2: "0 < ?m" using e(1) d(1) by simp
- from perfect_choose_dist [OF mde2, of x]
- obtain y where "y \<noteq> x" and "dist y x < ?m" by blast
- then have "dist y x < e" "dist y x < d" by simp_all
- from `dist y x < e` e(2) have "y \<in> S" by (simp add: dist_commute)
- have "\<exists>x'\<in>S. x'\<noteq> x \<and> dist x' x < d"
- using `y \<in> S` `y \<noteq> x` `dist y x < d` by fast
- }
- then show ?thesis unfolding islimpt_approachable by blast
-qed
+ using x islimpt_UNIV [of x]
+ unfolding interior_def islimpt_def
+ apply (clarsimp, rename_tac T T')
+ apply (drule_tac x="T \<inter> T'" in spec)
+ apply (auto simp add: open_Int)
+ done
lemma interior_closed_Un_empty_interior:
assumes cS: "closed S" and iT: "interior T = {}"
@@ -892,24 +882,25 @@
using frontier_complement frontier_subset_eq[of "- S"]
unfolding open_closed by auto
-subsection {* Nets and the ``eventually true'' quantifier *}
-
-text {* Common nets and The "within" modifier for nets. *}
+subsection {* Filters and the ``eventually true'' quantifier *}
+
+text {* Common filters and The "within" modifier for filters. *}
definition
- at_infinity :: "'a::real_normed_vector net" where
- "at_infinity = Abs_net (\<lambda>P. \<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x)"
+ at_infinity :: "'a::real_normed_vector filter" where
+ "at_infinity = Abs_filter (\<lambda>P. \<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x)"
definition
- indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a net" (infixr "indirection" 70) where
+ indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a filter"
+ (infixr "indirection" 70) where
"a indirection v = (at a) within {b. \<exists>c\<ge>0. b - a = scaleR c v}"
-text{* Prove That They are all nets. *}
+text{* Prove That They are all filters. *}
lemma eventually_at_infinity:
"eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. norm x >= b \<longrightarrow> P x)"
unfolding at_infinity_def
-proof (rule eventually_Abs_net, rule is_filter.intro)
+proof (rule eventually_Abs_filter, rule is_filter.intro)
fix P Q :: "'a \<Rightarrow> bool"
assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x" and "\<exists>s. \<forall>x. s \<le> norm x \<longrightarrow> Q x"
then obtain r s where
@@ -954,12 +945,13 @@
by (simp add: trivial_limit_at_iff)
lemma trivial_limit_at_infinity:
- "\<not> trivial_limit (at_infinity :: ('a::{real_normed_vector,zero_neq_one}) net)"
- (* FIXME: find a more appropriate type class *)
+ "\<not> trivial_limit (at_infinity :: ('a::{real_normed_vector,perfect_space}) filter)"
unfolding trivial_limit_def eventually_at_infinity
apply clarsimp
- apply (rule_tac x="scaleR b (sgn 1)" in exI)
- apply (simp add: norm_sgn)
+ apply (subgoal_tac "\<exists>x::'a. x \<noteq> 0", clarify)
+ apply (rule_tac x="scaleR (b / norm x) x" in exI, simp)
+ apply (cut_tac islimpt_UNIV [of "0::'a", unfolded islimpt_def])
+ apply (drule_tac x=UNIV in spec, simp)
done
text {* Some property holds "sufficiently close" to the limit point. *}
@@ -981,12 +973,6 @@
unfolding trivial_limit_def
by (auto elim: eventually_rev_mp)
-lemma always_eventually: "(\<forall>x. P x) ==> eventually P net"
-proof -
- assume "\<forall>x. P x" hence "P = (\<lambda>x. True)" by (simp add: ext)
- thus "eventually P net" by simp
-qed
-
lemma trivial_limit_eventually: "trivial_limit net \<Longrightarrow> eventually P net"
unfolding trivial_limit_def by (auto elim: eventually_rev_mp)
@@ -1021,10 +1007,10 @@
subsection {* Limits *}
- text{* Notation Lim to avoid collition with lim defined in analysis *}
-definition
- Lim :: "'a net \<Rightarrow> ('a \<Rightarrow> 'b::t2_space) \<Rightarrow> 'b" where
- "Lim net f = (THE l. (f ---> l) net)"
+text{* Notation Lim to avoid collition with lim defined in analysis *}
+
+definition Lim :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b::t2_space) \<Rightarrow> 'b"
+ where "Lim A f = (THE l. (f ---> l) A)"
lemma Lim:
"(f ---> l) net \<longleftrightarrow>
@@ -1290,9 +1276,9 @@
using assms by (rule scaleR.tendsto)
lemma Lim_inv:
- fixes f :: "'a \<Rightarrow> real"
- assumes "(f ---> l) (net::'a net)" "l \<noteq> 0"
- shows "((inverse o f) ---> inverse l) net"
+ fixes f :: "'a \<Rightarrow> real" and A :: "'a filter"
+ assumes "(f ---> l) A" and "l \<noteq> 0"
+ shows "((inverse o f) ---> inverse l) A"
unfolding o_def using assms by (rule tendsto_inverse)
lemma Lim_vmul:
@@ -1494,10 +1480,10 @@
thus "?lhs" by (rule topological_tendstoI)
qed
-text{* It's also sometimes useful to extract the limit point from the net. *}
+text{* It's also sometimes useful to extract the limit point from the filter. *}
definition
- netlimit :: "'a::t2_space net \<Rightarrow> 'a" where
+ netlimit :: "'a::t2_space filter \<Rightarrow> 'a" where
"netlimit net = (SOME a. ((\<lambda>x. x) ---> a) net)"
lemma netlimit_within:
@@ -1513,7 +1499,7 @@
done
lemma netlimit_at:
- fixes a :: "'a::perfect_space"
+ fixes a :: "'a::{perfect_space,t2_space}"
shows "netlimit (at a) = a"
apply (subst within_UNIV[symmetric])
using netlimit_within[of a UNIV]
@@ -1911,7 +1897,7 @@
lemma cball_empty: "e < 0 ==> cball x e = {}" by (simp add: cball_eq_empty)
lemma cball_eq_sing:
- fixes x :: "'a::perfect_space"
+ fixes x :: "'a::{metric_space,perfect_space}"
shows "(cball x e = {x}) \<longleftrightarrow> e = 0"
proof (rule linorder_cases)
assume e: "0 < e"
@@ -1952,14 +1938,14 @@
lemma at_within_interior:
"x \<in> interior S \<Longrightarrow> at x within S = at x"
- by (simp add: expand_net_eq eventually_within_interior)
+ by (simp add: filter_eq_iff eventually_within_interior)
lemma lim_within_interior:
"x \<in> interior S \<Longrightarrow> (f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x)"
by (simp add: at_within_interior)
lemma netlimit_within_interior:
- fixes x :: "'a::perfect_space"
+ fixes x :: "'a::{t2_space,perfect_space}"
assumes "x \<in> interior S"
shows "netlimit (at x within S) = x"
using assms by (simp add: at_within_interior netlimit_at)
@@ -2181,6 +2167,16 @@
(\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow>
(\<exists>l\<in>S. \<exists>r. subseq r \<and> ((f o r) ---> l) sequentially))"
+lemma compactI:
+ assumes "\<And>f. \<forall>n. f n \<in> S \<Longrightarrow> \<exists>l\<in>S. \<exists>r. subseq r \<and> ((f o r) ---> l) sequentially"
+ shows "compact S"
+ unfolding compact_def using assms by fast
+
+lemma compactE:
+ assumes "compact S" "\<forall>n. f n \<in> S"
+ obtains l r where "l \<in> S" "subseq r" "((f \<circ> r) ---> l) sequentially"
+ using assms unfolding compact_def by fast
+
text {*
A metric space (or topological vector space) is said to have the
Heine-Borel property if every closed and bounded subset is compact.
@@ -2714,6 +2710,139 @@
subsubsection {* Complete the chain of compactness variants *}
+lemma islimpt_range_imp_convergent_subsequence:
+ fixes f :: "nat \<Rightarrow> 'a::metric_space"
+ assumes "l islimpt (range f)"
+ shows "\<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
+proof (intro exI conjI)
+ have *: "\<And>e. 0 < e \<Longrightarrow> \<exists>n. 0 < dist (f n) l \<and> dist (f n) l < e"
+ using assms unfolding islimpt_def
+ by (drule_tac x="ball l e" in spec)
+ (auto simp add: zero_less_dist_iff dist_commute)
+
+ def t \<equiv> "\<lambda>e. LEAST n. 0 < dist (f n) l \<and> dist (f n) l < e"
+ have f_t_neq: "\<And>e. 0 < e \<Longrightarrow> 0 < dist (f (t e)) l"
+ unfolding t_def by (rule LeastI2_ex [OF * conjunct1])
+ have f_t_closer: "\<And>e. 0 < e \<Longrightarrow> dist (f (t e)) l < e"
+ unfolding t_def by (rule LeastI2_ex [OF * conjunct2])
+ have t_le: "\<And>n e. 0 < dist (f n) l \<Longrightarrow> dist (f n) l < e \<Longrightarrow> t e \<le> n"
+ unfolding t_def by (simp add: Least_le)
+ have less_tD: "\<And>n e. n < t e \<Longrightarrow> 0 < dist (f n) l \<Longrightarrow> e \<le> dist (f n) l"
+ unfolding t_def by (drule not_less_Least) simp
+ have t_antimono: "\<And>e e'. 0 < e \<Longrightarrow> e \<le> e' \<Longrightarrow> t e' \<le> t e"
+ apply (rule t_le)
+ apply (erule f_t_neq)
+ apply (erule (1) less_le_trans [OF f_t_closer])
+ done
+ have t_dist_f_neq: "\<And>n. 0 < dist (f n) l \<Longrightarrow> t (dist (f n) l) \<noteq> n"
+ by (drule f_t_closer) auto
+ have t_less: "\<And>e. 0 < e \<Longrightarrow> t e < t (dist (f (t e)) l)"
+ apply (subst less_le)
+ apply (rule conjI)
+ apply (rule t_antimono)
+ apply (erule f_t_neq)
+ apply (erule f_t_closer [THEN less_imp_le])
+ apply (rule t_dist_f_neq [symmetric])
+ apply (erule f_t_neq)
+ done
+ have dist_f_t_less':
+ "\<And>e e'. 0 < e \<Longrightarrow> 0 < e' \<Longrightarrow> t e \<le> t e' \<Longrightarrow> dist (f (t e')) l < e"
+ apply (simp add: le_less)
+ apply (erule disjE)
+ apply (rule less_trans)
+ apply (erule f_t_closer)
+ apply (rule le_less_trans)
+ apply (erule less_tD)
+ apply (erule f_t_neq)
+ apply (erule f_t_closer)
+ apply (erule subst)
+ apply (erule f_t_closer)
+ done
+
+ def r \<equiv> "nat_rec (t 1) (\<lambda>_ x. t (dist (f x) l))"
+ have r_simps: "r 0 = t 1" "\<And>n. r (Suc n) = t (dist (f (r n)) l)"
+ unfolding r_def by simp_all
+ have f_r_neq: "\<And>n. 0 < dist (f (r n)) l"
+ by (induct_tac n) (simp_all add: r_simps f_t_neq)
+
+ show "subseq r"
+ unfolding subseq_Suc_iff
+ apply (rule allI)
+ apply (case_tac n)
+ apply (simp_all add: r_simps)
+ apply (rule t_less, rule zero_less_one)
+ apply (rule t_less, rule f_r_neq)
+ done
+ show "((f \<circ> r) ---> l) sequentially"
+ unfolding Lim_sequentially o_def
+ apply (clarify, rule_tac x="t e" in exI, clarify)
+ apply (drule le_trans, rule seq_suble [OF `subseq r`])
+ apply (case_tac n, simp_all add: r_simps dist_f_t_less' f_r_neq)
+ done
+qed
+
+lemma finite_range_imp_infinite_repeats:
+ fixes f :: "nat \<Rightarrow> 'a"
+ assumes "finite (range f)"
+ shows "\<exists>k. infinite {n. f n = k}"
+proof -
+ { fix A :: "'a set" assume "finite A"
+ hence "\<And>f. infinite {n. f n \<in> A} \<Longrightarrow> \<exists>k. infinite {n. f n = k}"
+ proof (induct)
+ case empty thus ?case by simp
+ next
+ case (insert x A)
+ show ?case
+ proof (cases "finite {n. f n = x}")
+ case True
+ with `infinite {n. f n \<in> insert x A}`
+ have "infinite {n. f n \<in> A}" by simp
+ thus "\<exists>k. infinite {n. f n = k}" by (rule insert)
+ next
+ case False thus "\<exists>k. infinite {n. f n = k}" ..
+ qed
+ qed
+ } note H = this
+ from assms show "\<exists>k. infinite {n. f n = k}"
+ by (rule H) simp
+qed
+
+lemma bolzano_weierstrass_imp_compact:
+ fixes s :: "'a::metric_space set"
+ assumes "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t)"
+ shows "compact s"
+proof -
+ { fix f :: "nat \<Rightarrow> 'a" assume f: "\<forall>n. f n \<in> s"
+ have "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
+ proof (cases "finite (range f)")
+ case True
+ hence "\<exists>l. infinite {n. f n = l}"
+ by (rule finite_range_imp_infinite_repeats)
+ then obtain l where "infinite {n. f n = l}" ..
+ hence "\<exists>r. subseq r \<and> (\<forall>n. r n \<in> {n. f n = l})"
+ by (rule infinite_enumerate)
+ then obtain r where "subseq r" and fr: "\<forall>n. f (r n) = l" by auto
+ hence "subseq r \<and> ((f \<circ> r) ---> l) sequentially"
+ unfolding o_def by (simp add: fr Lim_const)
+ hence "\<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
+ by - (rule exI)
+ from f have "\<forall>n. f (r n) \<in> s" by simp
+ hence "l \<in> s" by (simp add: fr)
+ thus "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
+ by (rule rev_bexI) fact
+ next
+ case False
+ with f assms have "\<exists>x\<in>s. x islimpt (range f)" by auto
+ then obtain l where "l \<in> s" "l islimpt (range f)" ..
+ have "\<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
+ using `l islimpt (range f)`
+ by (rule islimpt_range_imp_convergent_subsequence)
+ with `l \<in> s` show "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially" ..
+ qed
+ }
+ thus ?thesis unfolding compact_def by auto
+qed
+
primrec helper_2::"(real \<Rightarrow> 'a::metric_space) \<Rightarrow> nat \<Rightarrow> 'a" where
"helper_2 beyond 0 = beyond 0" |
"helper_2 beyond (Suc n) = beyond (dist undefined (helper_2 beyond n) + 1 )"
@@ -2779,36 +2908,83 @@
qed
lemma sequence_infinite_lemma:
- fixes l :: "'a::metric_space" (* TODO: generalize *)
- assumes "\<forall>n::nat. (f n \<noteq> l)" "(f ---> l) sequentially"
+ fixes f :: "nat \<Rightarrow> 'a::t1_space"
+ assumes "\<forall>n. f n \<noteq> l" and "(f ---> l) sequentially"
shows "infinite (range f)"
proof
- let ?A = "(\<lambda>x. dist x l) ` range f"
assume "finite (range f)"
- hence **:"finite ?A" "?A \<noteq> {}" by auto
- obtain k where k:"dist (f k) l = Min ?A" using Min_in[OF **] by auto
- have "0 < Min ?A" using assms(1) unfolding dist_nz unfolding Min_gr_iff[OF **] by auto
- then obtain N where "dist (f N) l < Min ?A" using assms(2)[unfolded Lim_sequentially, THEN spec[where x="Min ?A"]] by auto
- moreover have "dist (f N) l \<in> ?A" by auto
- ultimately show False using Min_le[OF **(1), of "dist (f N) l"] by auto
-qed
-
+ hence "closed (range f)" by (rule finite_imp_closed)
+ hence "open (- range f)" by (rule open_Compl)
+ from assms(1) have "l \<in> - range f" by auto
+ from assms(2) have "eventually (\<lambda>n. f n \<in> - range f) sequentially"
+ using `open (- range f)` `l \<in> - range f` by (rule topological_tendstoD)
+ thus False unfolding eventually_sequentially by auto
+qed
+
+lemma closure_insert:
+ fixes x :: "'a::t1_space"
+ shows "closure (insert x s) = insert x (closure s)"
+apply (rule closure_unique)
+apply (rule conjI [OF insert_mono [OF closure_subset]])
+apply (rule conjI [OF closed_insert [OF closed_closure]])
+apply (simp add: closure_minimal)
+done
+
+lemma islimpt_insert:
+ fixes x :: "'a::t1_space"
+ shows "x islimpt (insert a s) \<longleftrightarrow> x islimpt s"
+proof
+ assume *: "x islimpt (insert a s)"
+ show "x islimpt s"
+ proof (rule islimptI)
+ fix t assume t: "x \<in> t" "open t"
+ show "\<exists>y\<in>s. y \<in> t \<and> y \<noteq> x"
+ proof (cases "x = a")
+ case True
+ obtain y where "y \<in> insert a s" "y \<in> t" "y \<noteq> x"
+ using * t by (rule islimptE)
+ with `x = a` show ?thesis by auto
+ next
+ case False
+ with t have t': "x \<in> t - {a}" "open (t - {a})"
+ by (simp_all add: open_Diff)
+ obtain y where "y \<in> insert a s" "y \<in> t - {a}" "y \<noteq> x"
+ using * t' by (rule islimptE)
+ thus ?thesis by auto
+ qed
+ qed
+next
+ assume "x islimpt s" thus "x islimpt (insert a s)"
+ by (rule islimpt_subset) auto
+qed
+
+lemma islimpt_union_finite:
+ fixes x :: "'a::t1_space"
+ shows "finite s \<Longrightarrow> x islimpt (s \<union> t) \<longleftrightarrow> x islimpt t"
+by (induct set: finite, simp_all add: islimpt_insert)
+
lemma sequence_unique_limpt:
- fixes l :: "'a::metric_space" (* TODO: generalize *)
- assumes "\<forall>n::nat. (f n \<noteq> l)" "(f ---> l) sequentially" "l' islimpt (range f)"
+ fixes f :: "nat \<Rightarrow> 'a::t2_space"
+ assumes "(f ---> l) sequentially" and "l' islimpt (range f)"
shows "l' = l"
-proof(rule ccontr)
- def e \<equiv> "dist l' l"
- assume "l' \<noteq> l" hence "e>0" unfolding dist_nz e_def by auto
- then obtain N::nat where N:"\<forall>n\<ge>N. dist (f n) l < e / 2"
- using assms(2)[unfolded Lim_sequentially, THEN spec[where x="e/2"]] by auto
- def d \<equiv> "Min (insert (e/2) ((\<lambda>n. if dist (f n) l' = 0 then e/2 else dist (f n) l') ` {0 .. N}))"
- have "d>0" using `e>0` unfolding d_def e_def using zero_le_dist[of _ l', unfolded order_le_less] by auto
- obtain k where k:"f k \<noteq> l'" "dist (f k) l' < d" using `d>0` and assms(3)[unfolded islimpt_approachable, THEN spec[where x="d"]] by auto
- have "k\<ge>N" using k(1)[unfolded dist_nz] using k(2)[unfolded d_def]
- by (force simp del: Min.insert_idem)
- hence "dist l' l < e" using N[THEN spec[where x=k]] using k(2)[unfolded d_def] and dist_triangle_half_r[of "f k" l' e l] by (auto simp del: Min.insert_idem)
- thus False unfolding e_def by auto
+proof (rule ccontr)
+ assume "l' \<noteq> l"
+ obtain s t where "open s" "open t" "l' \<in> s" "l \<in> t" "s \<inter> t = {}"
+ using hausdorff [OF `l' \<noteq> l`] by auto
+ have "eventually (\<lambda>n. f n \<in> t) sequentially"
+ using assms(1) `open t` `l \<in> t` by (rule topological_tendstoD)
+ then obtain N where "\<forall>n\<ge>N. f n \<in> t"
+ unfolding eventually_sequentially by auto
+
+ have "UNIV = {..<N} \<union> {N..}" by auto
+ hence "l' islimpt (f ` ({..<N} \<union> {N..}))" using assms(2) by simp
+ hence "l' islimpt (f ` {..<N} \<union> f ` {N..})" by (simp add: image_Un)
+ hence "l' islimpt (f ` {N..})" by (simp add: islimpt_union_finite)
+ then obtain y where "y \<in> f ` {N..}" "y \<in> s" "y \<noteq> l'"
+ using `l' \<in> s` `open s` by (rule islimptE)
+ then obtain n where "N \<le> n" "f n \<in> s" "f n \<noteq> l'" by auto
+ with `\<forall>n\<ge>N. f n \<in> t` have "f n \<in> s \<inter> t" by simp
+ with `s \<inter> t = {}` show False by simp
qed
lemma bolzano_weierstrass_imp_closed:
@@ -2832,26 +3008,26 @@
text{* Hence express everything as an equivalence. *}
lemma compact_eq_heine_borel:
- fixes s :: "'a::heine_borel set"
+ fixes s :: "'a::metric_space set"
shows "compact s \<longleftrightarrow>
(\<forall>f. (\<forall>t \<in> f. open t) \<and> s \<subseteq> (\<Union> f)
--> (\<exists>f'. f' \<subseteq> f \<and> finite f' \<and> s \<subseteq> (\<Union> f')))" (is "?lhs = ?rhs")
proof
- assume ?lhs thus ?rhs using compact_imp_heine_borel[of s] by blast
+ assume ?lhs thus ?rhs by (rule compact_imp_heine_borel)
next
assume ?rhs
hence "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. x islimpt t)"
by (blast intro: heine_borel_imp_bolzano_weierstrass[of s])
- thus ?lhs using bolzano_weierstrass_imp_bounded[of s] bolzano_weierstrass_imp_closed[of s] bounded_closed_imp_compact[of s] by blast
+ thus ?lhs by (rule bolzano_weierstrass_imp_compact)
qed
lemma compact_eq_bolzano_weierstrass:
- fixes s :: "'a::heine_borel set"
+ fixes s :: "'a::metric_space set"
shows "compact s \<longleftrightarrow> (\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t))" (is "?lhs = ?rhs")
proof
assume ?lhs thus ?rhs unfolding compact_eq_heine_borel using heine_borel_imp_bolzano_weierstrass[of s] by auto
next
- assume ?rhs thus ?lhs using bolzano_weierstrass_imp_bounded bolzano_weierstrass_imp_closed bounded_closed_imp_compact by auto
+ assume ?rhs thus ?lhs by (rule bolzano_weierstrass_imp_compact)
qed
lemma compact_eq_bounded_closed:
@@ -2896,56 +3072,82 @@
unfolding compact_def
by simp
-(* TODO: can any of the next 3 lemmas be generalized to metric spaces? *)
-
- (* FIXME : Rename *)
-lemma compact_union[intro]:
- fixes s t :: "'a::heine_borel set"
- shows "compact s \<Longrightarrow> compact t ==> compact (s \<union> t)"
- unfolding compact_eq_bounded_closed
- using bounded_Un[of s t]
- using closed_Un[of s t]
- by simp
-
-lemma compact_inter[intro]:
- fixes s t :: "'a::heine_borel set"
- shows "compact s \<Longrightarrow> compact t ==> compact (s \<inter> t)"
- unfolding compact_eq_bounded_closed
- using bounded_Int[of s t]
- using closed_Int[of s t]
- by simp
-
-lemma compact_inter_closed[intro]:
- fixes s t :: "'a::heine_borel set"
- shows "compact s \<Longrightarrow> closed t ==> compact (s \<inter> t)"
- unfolding compact_eq_bounded_closed
- using closed_Int[of s t]
- using bounded_subset[of "s \<inter> t" s]
- by blast
-
-lemma closed_inter_compact[intro]:
- fixes s t :: "'a::heine_borel set"
- shows "closed s \<Longrightarrow> compact t ==> compact (s \<inter> t)"
-proof-
- assume "closed s" "compact t"
+lemma subseq_o: "subseq r \<Longrightarrow> subseq s \<Longrightarrow> subseq (r \<circ> s)"
+ unfolding subseq_def by simp (* TODO: move somewhere else *)
+
+lemma compact_union [intro]:
+ assumes "compact s" and "compact t"
+ shows "compact (s \<union> t)"
+proof (rule compactI)
+ fix f :: "nat \<Rightarrow> 'a"
+ assume "\<forall>n. f n \<in> s \<union> t"
+ hence "infinite {n. f n \<in> s \<union> t}" by simp
+ hence "infinite {n. f n \<in> s} \<or> infinite {n. f n \<in> t}" by simp
+ thus "\<exists>l\<in>s \<union> t. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
+ proof
+ assume "infinite {n. f n \<in> s}"
+ from infinite_enumerate [OF this]
+ obtain q where "subseq q" "\<forall>n. (f \<circ> q) n \<in> s" by auto
+ obtain r l where "l \<in> s" "subseq r" "((f \<circ> q \<circ> r) ---> l) sequentially"
+ using `compact s` `\<forall>n. (f \<circ> q) n \<in> s` by (rule compactE)
+ hence "l \<in> s \<union> t" "subseq (q \<circ> r)" "((f \<circ> (q \<circ> r)) ---> l) sequentially"
+ using `subseq q` by (simp_all add: subseq_o o_assoc)
+ thus ?thesis by auto
+ next
+ assume "infinite {n. f n \<in> t}"
+ from infinite_enumerate [OF this]
+ obtain q where "subseq q" "\<forall>n. (f \<circ> q) n \<in> t" by auto
+ obtain r l where "l \<in> t" "subseq r" "((f \<circ> q \<circ> r) ---> l) sequentially"
+ using `compact t` `\<forall>n. (f \<circ> q) n \<in> t` by (rule compactE)
+ hence "l \<in> s \<union> t" "subseq (q \<circ> r)" "((f \<circ> (q \<circ> r)) ---> l) sequentially"
+ using `subseq q` by (simp_all add: subseq_o o_assoc)
+ thus ?thesis by auto
+ qed
+qed
+
+lemma compact_inter_closed [intro]:
+ assumes "compact s" and "closed t"
+ shows "compact (s \<inter> t)"
+proof (rule compactI)
+ fix f :: "nat \<Rightarrow> 'a"
+ assume "\<forall>n. f n \<in> s \<inter> t"
+ hence "\<forall>n. f n \<in> s" and "\<forall>n. f n \<in> t" by simp_all
+ obtain l r where "l \<in> s" "subseq r" "((f \<circ> r) ---> l) sequentially"
+ using `compact s` `\<forall>n. f n \<in> s` by (rule compactE)
moreover
- have "s \<inter> t = t \<inter> s" by auto ultimately
- show ?thesis
- using compact_inter_closed[of t s]
+ from `closed t` `\<forall>n. f n \<in> t` `((f \<circ> r) ---> l) sequentially` have "l \<in> t"
+ unfolding closed_sequential_limits o_def by fast
+ ultimately show "\<exists>l\<in>s \<inter> t. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
by auto
qed
-lemma finite_imp_compact:
- fixes s :: "'a::heine_borel set"
- shows "finite s ==> compact s"
- unfolding compact_eq_bounded_closed
- using finite_imp_closed finite_imp_bounded
- by blast
+lemma closed_inter_compact [intro]:
+ assumes "closed s" and "compact t"
+ shows "compact (s \<inter> t)"
+ using compact_inter_closed [of t s] assms
+ by (simp add: Int_commute)
+
+lemma compact_inter [intro]:
+ assumes "compact s" and "compact t"
+ shows "compact (s \<inter> t)"
+ using assms by (intro compact_inter_closed compact_imp_closed)
lemma compact_sing [simp]: "compact {a}"
unfolding compact_def o_def subseq_def
by (auto simp add: tendsto_const)
+lemma compact_insert [simp]:
+ assumes "compact s" shows "compact (insert x s)"
+proof -
+ have "compact ({x} \<union> s)"
+ using compact_sing assms by (rule compact_union)
+ thus ?thesis by simp
+qed
+
+lemma finite_imp_compact:
+ shows "finite s \<Longrightarrow> compact s"
+ by (induct set: finite) simp_all
+
lemma compact_cball[simp]:
fixes x :: "'a::heine_borel"
shows "compact(cball x e)"
@@ -2979,7 +3181,6 @@
text{* Finite intersection property. I could make it an equivalence in fact. *}
lemma compact_imp_fip:
- fixes s :: "'a::heine_borel set"
assumes "compact s" "\<forall>t \<in> f. closed t"
"\<forall>f'. finite f' \<and> f' \<subseteq> f --> (s \<inter> (\<Inter> f') \<noteq> {})"
shows "s \<inter> (\<Inter> f) \<noteq> {}"
@@ -3132,8 +3333,8 @@
text {* Define continuity over a net to take in restrictions of the set. *}
definition
- continuous :: "'a::t2_space net \<Rightarrow> ('a \<Rightarrow> 'b::topological_space) \<Rightarrow> bool" where
- "continuous net f \<longleftrightarrow> (f ---> f(netlimit net)) net"
+ continuous :: "'a::t2_space filter \<Rightarrow> ('a \<Rightarrow> 'b::topological_space) \<Rightarrow> bool"
+ where "continuous net f \<longleftrightarrow> (f ---> f(netlimit net)) net"
lemma continuous_trivial_limit:
"trivial_limit net ==> continuous net f"
--- a/src/HOL/Orderings.thy Mon Aug 08 22:33:36 2011 +0200
+++ b/src/HOL/Orderings.thy Tue Aug 09 07:44:17 2011 +0200
@@ -531,7 +531,7 @@
setup {*
let
-fun prp t thm = (#prop (rep_thm thm) = t);
+fun prp t thm = Thm.prop_of thm = t; (* FIXME aconv!? *)
fun prove_antisym_le sg ss ((le as Const(_,T)) $ r $ s) =
let val prems = Simplifier.prems_of ss;
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Mon Aug 08 22:33:36 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Tue Aug 09 07:44:17 2011 +0200
@@ -46,7 +46,7 @@
val recTs = Datatype_Aux.get_rec_types descr' sorts;
val newTs = take (length (hd descr)) recTs;
- val {maxidx, ...} = rep_thm induct;
+ val maxidx = Thm.maxidx_of induct;
val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
fun prove_casedist_thm (i, (T, t)) =
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Mon Aug 08 22:33:36 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Tue Aug 09 07:44:17 2011 +0200
@@ -20,9 +20,6 @@
in map (fn ks => i::ks) is @ is end
else [[]];
-fun prf_of thm =
- Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
-
fun is_unit t = body_type (fastype_of t) = HOLogic.unitT;
fun tname_of (Type (s, _)) = s
@@ -141,7 +138,8 @@
end
| _ => AbsP ("H", SOME p, prf)))
(rec_fns ~~ prems_of thm)
- (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0))));
+ (Proofterm.proof_combP
+ (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
val r' =
if null is then r
@@ -201,9 +199,10 @@
Proofterm.forall_intr_proof' (Logic.varify_global r)
(AbsP ("H", SOME (Logic.varify_global p), prf)))
(prems ~~ rs)
- (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0))));
+ (Proofterm.proof_combP
+ (Reconstruct.proof_of thm', map PBound (length prems - 1 downto 0))));
val prf' = Extraction.abs_corr_shyps thy' exhaust []
- (map Var (Term.add_vars (prop_of exhaust) [])) (prf_of exhaust);
+ (map Var (Term.add_vars (prop_of exhaust) [])) (Reconstruct.proof_of exhaust);
val r' = Logic.varify_global (Abs ("y", T,
list_abs (map dest_Free rs, list_comb (r,
map Bound ((length rs - 1 downto 0) @ [length rs])))));
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Mon Aug 08 22:33:36 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Tue Aug 09 07:44:17 2011 +0200
@@ -270,7 +270,7 @@
fun lemma thm ct =
let
val cu = Z3_Proof_Literals.negate (Thm.dest_arg ct)
- val hyps = map_filter (try HOLogic.dest_Trueprop) (#hyps (Thm.rep_thm thm))
+ val hyps = map_filter (try HOLogic.dest_Trueprop) (Thm.hyps_of thm)
val th = Z3_Proof_Tools.under_assumption (intro hyps thm) cu
in Thm (Z3_Proof_Tools.compose ccontr th) end
end
--- a/src/HOL/Tools/TFL/rules.ML Mon Aug 08 22:33:36 2011 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Tue Aug 09 07:44:17 2011 +0200
@@ -245,9 +245,7 @@
fun DISJ_CASESL disjth thl =
let val c = cconcl disjth
- fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t
- aconv term_of atm)
- (#hyps(rep_thm th))
+ fun eq th atm = exists (fn t => HOLogic.dest_Trueprop t aconv term_of atm) (Thm.hyps_of th)
val tml = Dcterm.strip_disj c
fun DL th [] = raise RULES_ERR "DISJ_CASESL" "no cases"
| DL th [th1] = PROVE_HYP th th1
--- a/src/HOL/Tools/inductive_codegen.ML Mon Aug 08 22:33:36 2011 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Tue Aug 09 07:44:17 2011 +0200
@@ -581,7 +581,7 @@
(ks @ [SOME k]))) arities));
fun prep_intrs intrs =
- map (Codegen.rename_term o #prop o rep_thm o Drule.export_without_context) intrs;
+ map (Codegen.rename_term o Thm.prop_of o Drule.export_without_context) intrs;
fun constrain cs [] = []
| constrain cs ((s, xs) :: ys) =
--- a/src/HOL/Tools/inductive_realizer.ML Mon Aug 08 22:33:36 2011 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Tue Aug 09 07:44:17 2011 +0200
@@ -22,10 +22,8 @@
| _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm));
fun prf_of thm =
- let
- val thy = Thm.theory_of_thm thm;
- val thm' = Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm);
- in Reconstruct.expand_proof thy [("", NONE)] thm' end; (* FIXME *)
+ Reconstruct.proof_of thm
+ |> Reconstruct.expand_proof (Thm.theory_of_thm thm) [("", NONE)]; (* FIXME *)
fun subsets [] = [[]]
| subsets (x::xs) =
--- a/src/HOL/Tools/sat_funcs.ML Mon Aug 08 22:33:36 2011 +0200
+++ b/src/HOL/Tools/sat_funcs.ML Tue Aug 09 07:44:17 2011 +0200
@@ -153,11 +153,13 @@
fun resolution (c1, hyps1) (c2, hyps2) =
let
val _ =
- if ! trace_sat then
+ if ! trace_sat then (* FIXME !? *)
tracing ("Resolving clause: " ^ Display.string_of_thm_without_context c1 ^
- " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c1)) (#hyps (rep_thm c1))
+ " (hyps: " ^ ML_Syntax.print_list
+ (Syntax.string_of_term_global (theory_of_thm c1)) (Thm.hyps_of c1)
^ ")\nwith clause: " ^ Display.string_of_thm_without_context c2 ^
- " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")")
+ " (hyps: " ^ ML_Syntax.print_list
+ (Syntax.string_of_term_global (theory_of_thm c2)) (Thm.hyps_of c2) ^ ")")
else ()
(* the two literals used for resolution *)
@@ -189,7 +191,7 @@
if !trace_sat then
tracing ("Resulting clause: " ^ Display.string_of_thm_without_context c_new ^
" (hyps: " ^ ML_Syntax.print_list
- (Syntax.string_of_term_global (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")")
+ (Syntax.string_of_term_global (theory_of_thm c_new)) (Thm.hyps_of c_new) ^ ")")
else ()
val _ = Unsynchronized.inc counter
in
--- a/src/Provers/hypsubst.ML Mon Aug 08 22:33:36 2011 +0200
+++ b/src/Provers/hypsubst.ML Tue Aug 09 07:44:17 2011 +0200
@@ -116,8 +116,7 @@
(*For the simpset. Adds ALL suitable equalities, even if not first!
No vars are allowed here, as simpsets are built from meta-assumptions*)
fun mk_eqs bnd th =
- [ if inspect_pair bnd false (Data.dest_eq
- (Data.dest_Trueprop (#prop (rep_thm th))))
+ [ if inspect_pair bnd false (Data.dest_eq (Data.dest_Trueprop (Thm.prop_of th)))
then th RS Data.eq_reflection
else Thm.symmetric(th RS Data.eq_reflection) (*reorient*) ]
handle TERM _ => [] | Match => [];
--- a/src/Pure/IsaMakefile Mon Aug 08 22:33:36 2011 +0200
+++ b/src/Pure/IsaMakefile Tue Aug 09 07:44:17 2011 +0200
@@ -158,9 +158,9 @@
PIDE/document.ML \
PIDE/isar_document.ML \
Proof/extraction.ML \
+ Proof/proof_checker.ML \
Proof/proof_rewrite_rules.ML \
Proof/proof_syntax.ML \
- Proof/proofchecker.ML \
Proof/reconstruct.ML \
ProofGeneral/pgip.ML \
ProofGeneral/pgip_input.ML \
--- a/src/Pure/Isar/element.ML Mon Aug 08 22:33:36 2011 +0200
+++ b/src/Pure/Isar/element.ML Tue Aug 09 07:44:17 2011 +0200
@@ -266,7 +266,7 @@
val mark_witness = Logic.protect;
fun witness_prop (Witness (t, _)) = t;
-fun witness_hyps (Witness (_, th)) = #hyps (Thm.rep_thm th);
+fun witness_hyps (Witness (_, th)) = Thm.hyps_of th;
fun map_witness f (Witness witn) = Witness (f witn);
fun morph_witness phi = map_witness (fn (t, th) => (Morphism.term phi t, Morphism.thm phi th));
--- a/src/Pure/Isar/rule_insts.ML Mon Aug 08 22:33:36 2011 +0200
+++ b/src/Pure/Isar/rule_insts.ML Tue Aug 09 07:44:17 2011 +0200
@@ -312,7 +312,7 @@
(fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
(xis ~~ ts));
(* Lift and instantiate rule *)
- val {maxidx, ...} = rep_thm st;
+ val maxidx = Thm.maxidx_of st;
val paramTs = map #2 params
and inc = maxidx+1
fun liftvar (Var ((a,j), T)) =
--- a/src/Pure/Proof/extraction.ML Mon Aug 08 22:33:36 2011 +0200
+++ b/src/Pure/Proof/extraction.ML Tue Aug 09 07:44:17 2011 +0200
@@ -795,7 +795,7 @@
|> Global_Theory.store_thm (Binding.qualified_name (corr_name s vs),
Thm.varifyT_global (funpow (length (vars_of corr_prop))
(Thm.forall_elim_var 0) (Thm.forall_intr_frees
- (ProofChecker.thm_of_proof thy'
+ (Proof_Checker.thm_of_proof thy'
(fst (Proofterm.freeze_thaw_prf prf))))))
|> snd
|> fold Code.add_default_eqn def_thms
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Proof/proof_checker.ML Tue Aug 09 07:44:17 2011 +0200
@@ -0,0 +1,145 @@
+(* Title: Pure/Proof/proofchecker.ML
+ Author: Stefan Berghofer, TU Muenchen
+
+Simple proof checker based only on the core inference rules
+of Isabelle/Pure.
+*)
+
+signature PROOF_CHECKER =
+sig
+ val thm_of_proof : theory -> Proofterm.proof -> thm
+end;
+
+structure Proof_Checker : PROOF_CHECKER =
+struct
+
+(***** construct a theorem out of a proof term *****)
+
+fun lookup_thm thy =
+ let val tab = fold_rev Symtab.update (Global_Theory.all_thms_of thy) Symtab.empty in
+ fn s =>
+ (case Symtab.lookup tab s of
+ NONE => error ("Unknown theorem " ^ quote s)
+ | SOME thm => thm)
+ end;
+
+val beta_eta_convert =
+ Conv.fconv_rule Drule.beta_eta_conversion;
+
+(* equality modulo renaming of type variables *)
+fun is_equal t t' =
+ let
+ val atoms = fold_types (fold_atyps (insert (op =))) t [];
+ val atoms' = fold_types (fold_atyps (insert (op =))) t' []
+ in
+ length atoms = length atoms' andalso
+ map_types (map_atyps (the o AList.lookup (op =) (atoms ~~ atoms'))) t aconv t'
+ end;
+
+fun pretty_prf thy vs Hs prf =
+ let val prf' = prf |> Proofterm.prf_subst_bounds (map Free vs) |>
+ Proofterm.prf_subst_pbounds (map (Hyp o prop_of) Hs)
+ in
+ (Proof_Syntax.pretty_proof (Syntax.init_pretty_global thy) prf',
+ Syntax.pretty_term_global thy (Reconstruct.prop_of prf'))
+ end;
+
+fun pretty_term thy vs _ t =
+ let val t' = subst_bounds (map Free vs, t)
+ in
+ (Syntax.pretty_term_global thy t',
+ Syntax.pretty_typ_global thy (fastype_of t'))
+ end;
+
+fun appl_error thy prt vs Hs s f a =
+ let
+ val (pp_f, pp_fT) = pretty_prf thy vs Hs f;
+ val (pp_a, pp_aT) = prt thy vs Hs a
+ in
+ error (cat_lines
+ [s,
+ "",
+ Pretty.string_of (Pretty.block
+ [Pretty.str "Operator:", Pretty.brk 2, pp_f,
+ Pretty.str " ::", Pretty.brk 1, pp_fT]),
+ Pretty.string_of (Pretty.block
+ [Pretty.str "Operand:", Pretty.brk 3, pp_a,
+ Pretty.str " ::", Pretty.brk 1, pp_aT]),
+ ""])
+ end;
+
+fun thm_of_proof thy =
+ let val lookup = lookup_thm thy in
+ fn prf =>
+ let
+ val prf_names = Proofterm.fold_proof_terms Term.declare_term_frees (K I) prf Name.context;
+
+ fun thm_of_atom thm Ts =
+ let
+ val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev;
+ val (fmap, thm') = Thm.varifyT_global' [] thm;
+ val ctye = map (pairself (Thm.ctyp_of thy))
+ (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
+ in
+ Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm'))
+ end;
+
+ fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) =
+ let
+ val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));
+ val prop = Thm.prop_of thm;
+ val _ =
+ if is_equal prop prop' then ()
+ else
+ error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
+ Syntax.string_of_term_global thy prop ^ "\n\n" ^
+ Syntax.string_of_term_global thy prop');
+ in thm_of_atom thm Ts end
+
+ | thm_of _ _ (PAxm (name, _, SOME Ts)) =
+ thm_of_atom (Thm.axiom thy name) Ts
+
+ | thm_of _ Hs (PBound i) = nth Hs i
+
+ | thm_of (vs, names) Hs (Abst (s, SOME T, prf)) =
+ let
+ val (x, names') = Name.variant s names;
+ val thm = thm_of ((x, T) :: vs, names') Hs prf
+ in
+ Thm.forall_intr (Thm.cterm_of thy (Free (x, T))) thm
+ end
+
+ | thm_of (vs, names) Hs (prf % SOME t) =
+ let
+ val thm = thm_of (vs, names) Hs prf;
+ val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
+ in
+ Thm.forall_elim ct thm
+ handle THM (s, _, _) => appl_error thy pretty_term vs Hs s prf t
+ end
+
+ | thm_of (vs, names) Hs (AbsP (s, SOME t, prf)) =
+ let
+ val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
+ val thm = thm_of (vs, names) (Thm.assume ct :: Hs) prf;
+ in
+ Thm.implies_intr ct thm
+ end
+
+ | thm_of vars Hs (prf %% prf') =
+ let
+ val thm = beta_eta_convert (thm_of vars Hs prf);
+ val thm' = beta_eta_convert (thm_of vars Hs prf');
+ in
+ Thm.implies_elim thm thm'
+ handle THM (s, _, _) => appl_error thy pretty_prf (fst vars) Hs s prf prf'
+ end
+
+ | thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of thy t)
+
+ | thm_of _ _ _ = error "thm_of_proof: partial proof term";
+
+ in beta_eta_convert (thm_of ([], prf_names) [] prf) end
+ end;
+
+end;
--- a/src/Pure/Proof/proofchecker.ML Mon Aug 08 22:33:36 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,141 +0,0 @@
-(* Title: Pure/Proof/proofchecker.ML
- Author: Stefan Berghofer, TU Muenchen
-
-Simple proof checker based only on the core inference rules
-of Isabelle/Pure.
-*)
-
-signature PROOF_CHECKER =
-sig
- val thm_of_proof : theory -> Proofterm.proof -> thm
-end;
-
-structure ProofChecker : PROOF_CHECKER =
-struct
-
-(***** construct a theorem out of a proof term *****)
-
-fun lookup_thm thy =
- let val tab = fold_rev Symtab.update (Global_Theory.all_thms_of thy) Symtab.empty
- in
- (fn s => case Symtab.lookup tab s of
- NONE => error ("Unknown theorem " ^ quote s)
- | SOME thm => thm)
- end;
-
-val beta_eta_convert =
- Conv.fconv_rule Drule.beta_eta_conversion;
-
-(* equality modulo renaming of type variables *)
-fun is_equal t t' =
- let
- val atoms = fold_types (fold_atyps (insert (op =))) t [];
- val atoms' = fold_types (fold_atyps (insert (op =))) t' []
- in
- length atoms = length atoms' andalso
- map_types (map_atyps (the o AList.lookup (op =) (atoms ~~ atoms'))) t aconv t'
- end;
-
-fun pretty_prf thy vs Hs prf =
- let val prf' = prf |> Proofterm.prf_subst_bounds (map Free vs) |>
- Proofterm.prf_subst_pbounds (map (Hyp o prop_of) Hs)
- in
- (Proof_Syntax.pretty_proof (Syntax.init_pretty_global thy) prf',
- Syntax.pretty_term_global thy (Reconstruct.prop_of prf'))
- end;
-
-fun pretty_term thy vs _ t =
- let val t' = subst_bounds (map Free vs, t)
- in
- (Syntax.pretty_term_global thy t',
- Syntax.pretty_typ_global thy (fastype_of t'))
- end;
-
-fun appl_error thy prt vs Hs s f a =
- let
- val (pp_f, pp_fT) = pretty_prf thy vs Hs f;
- val (pp_a, pp_aT) = prt thy vs Hs a
- in
- error (cat_lines
- [s,
- "",
- Pretty.string_of (Pretty.block
- [Pretty.str "Operator:", Pretty.brk 2, pp_f,
- Pretty.str " ::", Pretty.brk 1, pp_fT]),
- Pretty.string_of (Pretty.block
- [Pretty.str "Operand:", Pretty.brk 3, pp_a,
- Pretty.str " ::", Pretty.brk 1, pp_aT]),
- ""])
- end;
-
-fun thm_of_proof thy prf =
- let
- val prf_names = Proofterm.fold_proof_terms Term.declare_term_frees (K I) prf Name.context;
- val lookup = lookup_thm thy;
-
- fun thm_of_atom thm Ts =
- let
- val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev;
- val (fmap, thm') = Thm.varifyT_global' [] thm;
- val ctye = map (pairself (Thm.ctyp_of thy))
- (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
- in
- Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm'))
- end;
-
- fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) =
- let
- val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));
- val {prop, ...} = rep_thm thm;
- val _ = if is_equal prop prop' then () else
- error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
- Syntax.string_of_term_global thy prop ^ "\n\n" ^
- Syntax.string_of_term_global thy prop');
- in thm_of_atom thm Ts end
-
- | thm_of _ _ (PAxm (name, _, SOME Ts)) =
- thm_of_atom (Thm.axiom thy name) Ts
-
- | thm_of _ Hs (PBound i) = nth Hs i
-
- | thm_of (vs, names) Hs (Abst (s, SOME T, prf)) =
- let
- val (x, names') = Name.variant s names;
- val thm = thm_of ((x, T) :: vs, names') Hs prf
- in
- Thm.forall_intr (Thm.cterm_of thy (Free (x, T))) thm
- end
-
- | thm_of (vs, names) Hs (prf % SOME t) =
- let
- val thm = thm_of (vs, names) Hs prf;
- val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
- in
- Thm.forall_elim ct thm
- handle THM (s, _, _) => appl_error thy pretty_term vs Hs s prf t
- end
-
- | thm_of (vs, names) Hs (AbsP (s, SOME t, prf)) =
- let
- val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
- val thm = thm_of (vs, names) (Thm.assume ct :: Hs) prf;
- in
- Thm.implies_intr ct thm
- end
-
- | thm_of vars Hs (prf %% prf') =
- let
- val thm = beta_eta_convert (thm_of vars Hs prf);
- val thm' = beta_eta_convert (thm_of vars Hs prf');
- in
- Thm.implies_elim thm thm'
- handle THM (s, _, _) => appl_error thy pretty_prf (fst vars) Hs s prf prf'
- end
-
- | thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of thy t)
-
- | thm_of _ _ _ = error "thm_of_proof: partial proof term";
-
- in beta_eta_convert (thm_of ([], prf_names) [] prf) end;
-
-end;
--- a/src/Pure/Proof/reconstruct.ML Mon Aug 08 22:33:36 2011 +0200
+++ b/src/Pure/Proof/reconstruct.ML Tue Aug 09 07:44:17 2011 +0200
@@ -10,6 +10,7 @@
val reconstruct_proof : theory -> term -> Proofterm.proof -> Proofterm.proof
val prop_of' : term list -> Proofterm.proof -> term
val prop_of : Proofterm.proof -> term
+ val proof_of : thm -> Proofterm.proof
val expand_proof : theory -> (string * term option) list ->
Proofterm.proof -> Proofterm.proof
end;
@@ -323,6 +324,10 @@
val prop_of' = Envir.beta_eta_contract oo prop_of0;
val prop_of = prop_of' [];
+fun proof_of thm =
+ reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
+
+
(**** expand and reconstruct subproofs ****)
@@ -352,8 +357,9 @@
(case AList.lookup (op =) prfs (a, prop) of
NONE =>
let
- val _ = message ("Reconstructing proof of " ^ a);
- val _ = message (Syntax.string_of_term_global thy prop);
+ val _ =
+ message ("Reconstructing proof of " ^ a ^ "\n" ^
+ Syntax.string_of_term_global thy prop);
val prf' = forall_intr_vfs_prf prop
(reconstruct_proof thy prop (Proofterm.join_proof body));
val (maxidx', prfs', prf) = expand
--- a/src/Pure/ROOT.ML Mon Aug 08 22:33:36 2011 +0200
+++ b/src/Pure/ROOT.ML Tue Aug 09 07:44:17 2011 +0200
@@ -175,7 +175,7 @@
use "Proof/reconstruct.ML";
use "Proof/proof_syntax.ML";
use "Proof/proof_rewrite_rules.ML";
-use "Proof/proofchecker.ML";
+use "Proof/proof_checker.ML";
(*outer syntax*)
use "Isar/token.ML";
--- a/src/Pure/raw_simplifier.ML Mon Aug 08 22:33:36 2011 +0200
+++ b/src/Pure/raw_simplifier.ML Tue Aug 09 07:44:17 2011 +0200
@@ -1197,7 +1197,7 @@
val prem' = Thm.rhs_of eqn;
val tprems = map term_of prems;
val i = 1 + fold Integer.max (map (fn p =>
- find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn))) ~1;
+ find_index (fn q => q aconv p) tprems) (Thm.hyps_of eqn)) ~1;
val (rrs', asm') = rules_of_prem ss prem'
in mut_impc prems concl rrss asms (prem' :: prems')
(rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true)
--- a/src/Pure/simplifier.ML Mon Aug 08 22:33:36 2011 +0200
+++ b/src/Pure/simplifier.ML Tue Aug 09 07:44:17 2011 +0200
@@ -410,7 +410,7 @@
if can Logic.dest_equals (Thm.concl_of thm) then [thm]
else [thm RS reflect] handle THM _ => [];
- fun mksimps thm = mk_eq (Thm.forall_elim_vars (#maxidx (Thm.rep_thm thm) + 1) thm);
+ fun mksimps thm = mk_eq (Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm);
in
empty_ss setsubgoaler asm_simp_tac
setSSolver safe_solver
--- a/src/Tools/jEdit/src/text_area_painter.scala Mon Aug 08 22:33:36 2011 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala Tue Aug 09 07:44:17 2011 +0200
@@ -204,6 +204,10 @@
val chunk_font = chunk.style.getFont
val chunk_color = chunk.style.getForegroundColor
+ def string_width(s: String): Float =
+ if (s.isEmpty) 0.0f
+ else chunk_font.getStringBounds(s, font_context).getWidth.toFloat
+
val caret_range =
if (text_area.hasFocus) doc_view.caret_range()
else Text.Range(-1)
@@ -230,17 +234,27 @@
range.try_restrict(caret_range) match {
case Some(r) if !r.is_singularity =>
- val astr = new AttributedString(str)
val i = r.start - range.start
val j = r.stop - range.start
+ val s1 = str.substring(0, i)
+ val s2 = str.substring(i, j)
+ val s3 = str.substring(j)
+
+ if (!s1.isEmpty) gfx.drawString(s1, x1, y)
+
+ val astr = new AttributedString(s2)
astr.addAttribute(TextAttribute.FONT, chunk_font)
- astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor, i, j)
- astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON, i, j)
- gfx.drawString(astr.getIterator, x1, y)
+ astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor)
+ astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
+ gfx.drawString(astr.getIterator, x1 + string_width(s1), y)
+
+ if (!s3.isEmpty)
+ gfx.drawString(s3, x1 + string_width(str.substring(0, j)), y)
+
case _ =>
gfx.drawString(str, x1, y)
}
- x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
+ x1 += string_width(str)
}
}
w += chunk.width
--- a/src/ZF/Tools/datatype_package.ML Mon Aug 08 22:33:36 2011 +0200
+++ b/src/ZF/Tools/datatype_package.ML Tue Aug 09 07:44:17 2011 +0200
@@ -339,7 +339,7 @@
end
val constructors =
- map (head_of o #1 o Logic.dest_equals o #prop o rep_thm) (tl con_defs);
+ map (head_of o #1 o Logic.dest_equals o Thm.prop_of) (tl con_defs);
val free_SEs = map Drule.export_without_context (Ind_Syntax.mk_free_SEs free_iffs);
--- a/src/ZF/Tools/induct_tacs.ML Mon Aug 08 22:33:36 2011 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Tue Aug 09 07:44:17 2011 +0200
@@ -123,8 +123,7 @@
Syntax.string_of_term_global thy eqn);
val constructors =
- map (head_of o const_of o FOLogic.dest_Trueprop o
- #prop o rep_thm) case_eqns;
+ map (head_of o const_of o FOLogic.dest_Trueprop o Thm.prop_of) case_eqns;
val Const (@{const_name mem}, _) $ _ $ data =
FOLogic.dest_Trueprop (hd (prems_of elim));
--- a/src/ZF/arith_data.ML Mon Aug 08 22:33:36 2011 +0200
+++ b/src/ZF/arith_data.ML Tue Aug 09 07:44:17 2011 +0200
@@ -61,7 +61,7 @@
(*We remove equality assumptions because they confuse the simplifier and
because only type-checking assumptions are necessary.*)
fun is_eq_thm th =
- can FOLogic.dest_eq (FOLogic.dest_Trueprop (#prop (rep_thm th)));
+ can FOLogic.dest_eq (FOLogic.dest_Trueprop (Thm.prop_of th));
fun add_chyps chyps ct = Drule.list_implies (map cprop_of chyps, ct);
@@ -69,7 +69,7 @@
if t aconv u then NONE
else
let val prems' = filter_out is_eq_thm prems
- val goal = Logic.list_implies (map (#prop o Thm.rep_thm) prems',
+ val goal = Logic.list_implies (map Thm.prop_of prems',
FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
in SOME (prems' MRS Goal.prove ctxt [] [] goal (K (EVERY tacs)))
handle ERROR msg =>