--- a/src/Doc/Datatypes/Datatypes.thy Wed Sep 25 12:43:20 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Wed Sep 25 13:39:34 2013 +0200
@@ -164,7 +164,7 @@
in.\allowbreak tum.\allowbreak de}}
The commands @{command datatype_new} and @{command primrec_new} are expected to
-displace \keyw{datatype} and \keyw{primrec} in a future release. Authors of new
+replace \keyw{datatype} and \keyw{primrec} in a future release. Authors of new
theories are encouraged to use the new commands, and maintainers of older
theories may want to consider upgrading.
@@ -175,7 +175,7 @@
\begin{framed}
\noindent
\textbf{Warning:}\enskip This tutorial and the package it describes are under
-construction. Please apologise for their appearance. Should you have suggestions
+construction. Please forgive their appearance. Should you have suggestions
or comments regarding either, please let the authors know.
\end{framed}
*}
@@ -242,6 +242,12 @@
datatype_new ('a, 'b, 'c) triple\<^sub>u = Triple\<^sub>u "'a * 'b * 'c"
+text {*
+\noindent
+Occurrences of nonatomic types on the right-hand side of the equal sign must be
+enclosed in double quotes, as is customary in Isabelle.
+*}
+
subsubsection {* Simple Recursion
\label{sssec:datatype-simple-recursion} *}
@@ -259,12 +265,6 @@
datatype_new (*<*)(in early) (*>*)('a, 'b) tlist = TNil 'b | TCons 'a "('a, 'b) tlist"
-text {*
-\noindent
-Occurrences of nonatomic types on the right-hand side of the equal sign must be
-enclosed in double quotes, as is customary in Isabelle.
-*}
-
subsubsection {* Mutual Recursion
\label{sssec:datatype-mutual-recursion} *}
@@ -402,8 +402,8 @@
characteristic theorems can lead Isabelle's automation to switch between the
constructor and the destructor view in surprising ways.
-The usual mixfix syntaxes are available for both types and constructors. For
-example:
+The usual mixfix syntax annotations are available for both types and
+constructors. For example:
*}
(*<*)
@@ -419,7 +419,7 @@
text {*
\noindent
-Incidentally, this is how the traditional syntaxes can be set up:
+Incidentally, this is how the traditional syntax can be set up:
*}
syntax "_list" :: "args \<Rightarrow> 'a list" ("[(_)]")
@@ -450,7 +450,7 @@
@{syntax_def dt_options}: '(' (('no_discs_sels' | 'rep_compat') + ',') ')'
"}
-The syntactic quantity \synt{target} can be used to specify a local
+The syntactic entity \synt{target} can be used to specify a local
context---e.g., @{text "(in linorder)"}. It is documented in the Isar reference
manual \cite{isabelle-isar-ref}.
%
@@ -482,7 +482,7 @@
"}
\noindent
-The syntactic quantity \synt{name} denotes an identifier, \synt{typefree}
+The syntactic entity \synt{name} denotes an identifier, \synt{typefree}
denotes fixed type variable (@{typ 'a}, @{typ 'b}, \ldots), and \synt{mixfix}
denotes the usual parenthesized mixfix notation. They are documented in the Isar
reference manual \cite{isabelle-isar-ref}.
@@ -500,7 +500,7 @@
\medskip
\noindent
-The main constituents of a constructor specification is the name of the
+The main constituents of a constructor specification are the name of the
constructor and the list of its argument types. An optional discriminator name
can be supplied at the front to override the default name
(@{text t.is_C\<^sub>j}).
@@ -528,7 +528,7 @@
@{text "un_D \<Colon> \<sigma> \<Rightarrow> \<tau>"}
associated with other constructors. The specified default value must be of type
@{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<sigma>\<^sub>p \<Rightarrow> \<tau>"}
-(i.e., it may depends on @{text C}'s arguments).
+(i.e., it may depend on @{text C}'s arguments).
*}
@@ -560,7 +560,7 @@
\end{itemize}
\noindent
-New-style datatypes can in most case be registered as old-style datatypes using
+New-style datatypes can in most cases be registered as old-style datatypes using
@{command datatype_new_compat}. The \textit{names} argument is a space-separated
list of type names that are mutually recursive. For example:
*}
@@ -687,7 +687,7 @@
(*>*)
text {*
-The first subgroup of properties are concerned with the constructors.
+The first subgroup of properties is concerned with the constructors.
They are listed below for @{typ "'a list"}:
\begin{indentblock}
@@ -895,7 +895,7 @@
Section~\ref{sssec:primrec-nested-as-mutual-recursion}, if the recursion is via
new-style datatypes.
-\item \emph{The internal constructions are completely different.} Proofs texts
+\item \emph{The internal constructions are completely different.} Proof texts
that unfold the definition of constants introduced by \keyw{datatype} will be
difficult to port.
@@ -1343,8 +1343,8 @@
\label{sssec:codatatype-simple-corecursion} *}
text {*
-Noncorecursive codatatypes coincide with the corresponding datatypes, so
-they have no practical uses. \emph{Corecursive codatatypes} have the same syntax
+Noncorecursive codatatypes coincide with the corresponding datatypes, so they
+are useless in practice. \emph{Corecursive codatatypes} have the same syntax
as recursive datatypes, except for the command name. For example, here is the
definition of lazy lists:
*}
@@ -1671,11 +1671,10 @@
@{text "[x, f x, f (f x), \<dots>]"}. Productivity guarantees that prefixes
@{text "[x, f x, f (f x), \<dots>, (f ^^ k) x]"} of arbitrary finite length
@{text k} can be computed by unfolding the code equation a finite number of
-times. The period (\keyw{.}) at the end of the commands discharge the zero proof
-obligations.
+times.
Corecursive functions construct codatatype values, but nothing prevents them
-from also consuming such values. The following function drops ever second
+from also consuming such values. The following function drops every second
element in a stream:
*}
@@ -2185,9 +2184,9 @@
@{rail "
@@{command wrap_free_constructors} target? @{syntax dt_options} \\
- term_list name @{syntax fc_discs_sels}?
+ term_list name @{syntax wfc_discs_sels}?
;
- @{syntax_def fc_discs_sels}: name_list (name_list_list name_term_list_list? )?
+ @{syntax_def wfc_discs_sels}: name_list (name_list_list name_term_list_list? )?
;
@{syntax_def name_term}: (name ':' term)
"}
@@ -2273,17 +2272,17 @@
*)
-section {* Acknowledgments
- \label{sec:acknowledgments} *}
-
text {*
+\section*{Acknowledgment}
+
Tobias Nipkow and Makarius Wenzel encouraged us to implement the new
(co)datatype package. Andreas Lochbihler provided lots of comments on earlier
versions of the package, especially for the coinductive part. Brian Huffman
suggested major simplifications to the internal constructions, much of which has
yet to be implemented. Florian Haftmann and Christian Urban provided general
advice on Isabelle and package writing. Stefan Milius and Lutz Schr\"oder
-suggested an elegant proof to eliminate one of the BNF assumptions.
+found an elegant proof to eliminate one of the BNF assumptions. Christian
+Sternagel suggested many textual improvements to this tutorial.
*}
end
--- a/src/HOL/BNF/BNF_FP_Base.thy Wed Sep 25 12:43:20 2013 +0200
+++ b/src/HOL/BNF/BNF_FP_Base.thy Wed Sep 25 13:39:34 2013 +0200
@@ -172,15 +172,6 @@
(if b then f y else if b' then x' else f y')"
by simp
-lemma if_then_else_True_False:
- "(if p then False else r) \<longleftrightarrow> \<not> p \<and> r"
- "(if p then True else r) \<longleftrightarrow> p \<or> r"
- "(if p then q else False) \<longleftrightarrow> p \<and> q"
- "(if p then q else True) \<longleftrightarrow> \<not> p \<or> q"
-by simp_all
-
-lemmas bool_if_simps = bool_simps(7,8,15-17,19,21-24,29-32) if_then_else_True_False
-
ML_file "Tools/bnf_fp_util.ML"
ML_file "Tools/bnf_fp_def_sugar_tactics.ML"
ML_file "Tools/bnf_fp_def_sugar.ML"
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Wed Sep 25 12:43:20 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Wed Sep 25 13:39:34 2013 +0200
@@ -30,6 +30,7 @@
case_conv_ifs: thm list};
val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar
+ val ctr_sugar_of: Proof.context -> string -> ctr_sugar option
val rep_compat_prefix: string
@@ -37,10 +38,11 @@
val join_halves: int -> 'a list list -> 'a list list -> 'a list * 'a list list list
val mk_ctr: typ list -> term -> term
+ val mk_case: typ list -> typ -> term -> term
val mk_disc_or_sel: typ list -> term -> term
-
val name_of_ctr: term -> string
val name_of_disc: term -> string
+ val dest_case: Proof.context -> string -> typ list -> term -> (term list * term list) option
val wrap_free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list ->
(((bool * bool) * term list) * binding) *
@@ -102,6 +104,27 @@
expands = map (Morphism.thm phi) expands,
case_conv_ifs = map (Morphism.thm phi) case_conv_ifs};
+fun eq_ctr_sugar ({ctrs = ctrs1, casex = case1, discs = discs1, selss = selss1, ...} : ctr_sugar,
+ {ctrs = ctrs2, casex = case2, discs = discs2, selss = selss2, ...} : ctr_sugar) =
+ ctrs1 = ctrs2 andalso case1 = case2 andalso discs1 = discs2 andalso selss1 = selss2;
+
+structure Data = Generic_Data
+(
+ type T = ctr_sugar Symtab.table;
+ val empty = Symtab.empty;
+ val extend = I;
+ val merge = Symtab.merge eq_ctr_sugar;
+);
+
+fun ctr_sugar_of ctxt =
+ Symtab.lookup (Data.get (Context.Proof ctxt))
+ #> Option.map (morph_ctr_sugar
+ (Morphism.thm_morphism (Thm.transfer (Proof_Context.theory_of ctxt))));
+
+fun register_ctr_sugar key ctr_sugar =
+ Local_Theory.declaration {syntax = false, pervasive = true}
+ (fn phi => Data.map (Symtab.default (key, morph_ctr_sugar phi ctr_sugar)));
+
val rep_compat_prefix = "new";
val isN = "is_";
@@ -160,14 +183,14 @@
Term.subst_atomic_types (Ts0 ~~ Ts) t
end;
-fun mk_disc_or_sel Ts t =
- Term.subst_atomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t;
-
fun mk_case Ts T t =
let val (Type (_, Ts0), body) = strip_type (fastype_of t) |>> List.last in
Term.subst_atomic_types ((body, T) :: (Ts0 ~~ Ts)) t
end;
+fun mk_disc_or_sel Ts t =
+ Term.subst_atomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t;
+
fun name_of_const what t =
(case head_of t of
Const (s, _) => s
@@ -192,6 +215,28 @@
val base_name_of_ctr = Long_Name.base_name o name_of_ctr;
+fun dest_case ctxt s Ts t =
+ (case Term.strip_comb t of
+ (Const (c, _), args as _ :: _) =>
+ (case ctr_sugar_of ctxt s of
+ SOME {casex = Const (case_name, _), discs = discs0, selss = selss0, ...} =>
+ if case_name = c then
+ let
+ val n = length discs0;
+ val (branches, obj :: leftovers) = chop n args;
+ val discs = map (mk_disc_or_sel Ts) discs0;
+ val selss = map (map (mk_disc_or_sel Ts)) selss0;
+ val conds = map (rapp obj) discs;
+ val branch_argss = map (fn sels => map (rapp obj) sels @ leftovers) selss;
+ val branches' = map2 (curry Term.betapplys) branches branch_argss;
+ in
+ SOME (conds, branches')
+ end
+ else
+ NONE
+ | _ => NONE)
+ | _ => NONE);
+
fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
fun prepare_wrap_free_constructors prep_term ((((no_discs_sels, rep_compat), raw_ctrs),
@@ -786,19 +831,23 @@
val notes' =
[(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)]
|> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
+
+ val ctr_sugar =
+ {ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
+ nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
+ case_thms = case_thms, case_cong = case_cong_thm, weak_case_cong = weak_case_cong_thm,
+ split = split_thm, split_asm = split_asm_thm, disc_thmss = disc_thmss,
+ discIs = discI_thms, sel_thmss = sel_thmss, disc_exhausts = disc_exhaust_thms,
+ collapses = all_collapse_thms, expands = expand_thms, case_conv_ifs = case_conv_if_thms};
in
- ({ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
- nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
- case_thms = case_thms, case_cong = case_cong_thm, weak_case_cong = weak_case_cong_thm,
- split = split_thm, split_asm = split_asm_thm, disc_thmss = disc_thmss,
- discIs = discI_thms, sel_thmss = sel_thmss, disc_exhausts = disc_exhaust_thms,
- collapses = all_collapse_thms, expands = expand_thms, case_conv_ifs = case_conv_if_thms},
+ (ctr_sugar,
lthy
|> not rep_compat ?
(Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi => Case_Translation.register
(Morphism.term phi casex) (map (Morphism.term phi) ctrs)))
- |> Local_Theory.notes (notes' @ notes) |> snd)
+ |> Local_Theory.notes (notes' @ notes) |> snd
+ |> register_ctr_sugar dataT_name ctr_sugar)
end;
in
(goalss, after_qed, lthy')
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Wed Sep 25 12:43:20 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Wed Sep 25 13:39:34 2013 +0200
@@ -51,11 +51,6 @@
val abs_tuple = HOLogic.tupled_lambda o HOLogic.mk_tuple;
fun drop_All t = subst_bounds (strip_qnt_vars @{const_name all} t |> map Free |> rev,
strip_qnt_body @{const_name all} t)
-fun s_not @{const True} = @{const False}
- | s_not @{const False} = @{const True}
- | s_not (@{const Not} $ t) = t
- | s_not (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
- | s_not t = HOLogic.mk_not t
val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True};
val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default @{const False};
fun invert_prems [t] = map s_not (HOLogic.disjuncts t)
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Wed Sep 25 12:43:20 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Wed Sep 25 13:39:34 2013 +0200
@@ -85,10 +85,10 @@
EVERY (map2 (mk_primcorec_code_of_ctr_case_tac ctxt eq_caseIs) ms ctr_thms);
fun mk_primcorec_code_tac eq_caseIs disc_excludes raw collapses =
- HEADGOAL (rtac (raw RS trans) THEN'
- REPEAT o (resolve_tac (maps (fn thm => [thm, thm RS sym]) (@{thm eq_ifI} :: eq_caseIs)) ORELSE'
- rtac refl ORELSE' (etac notE THEN' atac) ORELSE'
- (dresolve_tac disc_excludes THEN' etac notE THEN' atac) ORELSE'
- eresolve_tac (maps (fn thm => [thm, thm RS sym]) collapses)));
+ HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN' REPEAT o
+ (resolve_tac (maps (fn thm => [thm, thm RS sym]) (@{thm eq_ifI} :: eq_caseIs)) ORELSE'
+ rtac refl ORELSE' etac notE THEN' atac ORELSE'
+ dresolve_tac disc_excludes THEN' etac notE THEN' atac ORELSE'
+ eresolve_tac (maps (fn thm => [thm, thm RS sym]) collapses)));
end;
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Wed Sep 25 12:43:20 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Wed Sep 25 13:39:34 2013 +0200
@@ -51,6 +51,7 @@
nested_map_comps: thm list,
ctr_specs: corec_ctr_spec list}
+ val s_not: term -> term
val massage_indirect_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
typ list -> term -> term -> term -> term
val massage_direct_corec_call: Proof.context -> (term -> bool) -> (term -> term) -> typ list ->
@@ -60,8 +61,8 @@
val expand_corec_code_rhs: Proof.context -> (term -> bool) -> typ list -> term -> term
val massage_corec_code_rhs: Proof.context -> (term -> term list -> term) -> typ list -> typ ->
term -> term
- val fold_rev_corec_code_rhs: (term -> term list -> 'a -> 'a) -> term -> 'a -> 'a
- val simplify_bool_ifs: theory -> term -> term list
+ val fold_rev_corec_code_rhs: Proof.context -> (term list -> term -> term list -> 'a -> 'a) ->
+ typ list -> term -> 'a -> 'a
val rec_specs_of: binding list -> typ list -> typ list -> (term -> int list) ->
((term * term list list) list) list -> local_theory ->
(bool * rec_spec list * typ list * thm * thm list) * local_theory
@@ -138,6 +139,12 @@
fun unexpected_corec_call ctxt t =
error ("Unexpected corecursive call: " ^ quote (Syntax.string_of_term ctxt t));
+fun s_not @{const True} = @{const False}
+ | s_not @{const False} = @{const True}
+ | s_not (@{const Not} $ t) = t
+ | s_not (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
+ | s_not t = HOLogic.mk_not t
+
fun factor_out_types ctxt massage destU U T =
(case try destU U of
SOME (U1, U2) => if U1 = T then massage T U2 else invalid_map ctxt
@@ -174,7 +181,7 @@
val map' = mk_map (length fs) Us ran_Ts map0;
val fs' = map_flattened_map_args ctxt s (map3 massage_map_or_map_arg Us Ts) fs;
in
- list_comb (map', fs')
+ Term.list_comb (map', fs')
end
| NONE => raise AINT_NO_MAP t)
| massage_map _ _ t = raise AINT_NO_MAP t
@@ -196,7 +203,33 @@
massage_call
end;
-fun massage_let_if ctxt has_call massage_leaf bound_Ts U =
+fun fold_rev_let_if_case ctxt f bound_Ts =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+
+ fun fld conds t =
+ (case Term.strip_comb t of
+ (Const (@{const_name Let}, _), [arg1, arg2]) => fld conds (betapply (arg2, arg1))
+ | (Const (@{const_name If}, _), [cond, then_branch, else_branch]) =>
+ fld (cond :: conds) then_branch o fld (s_not cond :: conds) else_branch
+ | (Const (c, _), args as _ :: _) =>
+ let val n = num_binder_types (Sign.the_const_type thy c) in
+ (case fastype_of1 (bound_Ts, nth args (n - 1)) of
+ Type (s, Ts) =>
+ (case dest_case ctxt s Ts t of
+ NONE => f conds t
+ | SOME (conds', branches) =>
+ fold_rev (uncurry fld) (map (fn cond => cond :: conds) conds' ~~ branches))
+ | _ => f conds t)
+ end
+ | _ => f conds t)
+ in
+ fld []
+ end;
+
+fun case_of ctxt = ctr_sugar_of ctxt #> Option.map (fst o dest_Const o #casex);
+
+fun massage_let_if_case ctxt has_call massage_leaf bound_Ts U =
let
val typof = curry fastype_of1 bound_Ts;
val check_obj = ((not o has_call) orf unexpected_corec_call ctxt);
@@ -205,35 +238,28 @@
(case Term.strip_comb t of
(Const (@{const_name Let}, _), [arg1, arg2]) => massage_rec (betapply (arg2, arg1))
| (Const (@{const_name If}, _), obj :: branches) =>
- list_comb (If_const U $ tap check_obj obj, map massage_rec branches)
- | (Const (@{const_name nat_case}, _), args) =>
- (* Proof of concept -- should be extensible to all case-like constructs *)
- let
- val (branches, obj) = split_last args;
- val branches' = map massage_rec branches
- (* FIXME: bound_Ts *)
- val casex' = Const (@{const_name nat_case}, map typof branches' ---> typof obj);
- in
- list_comb (casex', branches') $ tap check_obj obj
+ Term.list_comb (If_const U $ tap check_obj obj, map massage_rec branches)
+ | (Const (c, _), args as _ :: _) =>
+ let val (branches, obj) = split_last args in
+ (case fastype_of1 (bound_Ts, obj) of
+ Type (T_name, _) =>
+ if case_of ctxt T_name = SOME c then
+ let
+ val branches' = map massage_rec branches;
+ val casex' = Const (c, map typof branches' ---> typof obj);
+ in
+ Term.list_comb (casex', branches') $ tap check_obj obj
+ end
+ else
+ massage_leaf t
+ | _ => massage_leaf t)
end
| _ => massage_leaf t)
in
massage_rec
end;
-fun fold_rev_let_if f =
- let
- fun fld t =
- (case Term.strip_comb t of
- (Const (@{const_name Let}, _), [arg1, arg2]) => fld (betapply (arg2, arg1))
- | (Const (@{const_name If}, _), _ :: branches) => fold_rev fld branches
- | (Const (@{const_name nat_case}, _), args) => fold_rev fld (fst (split_last args))
- | _ => f t)
- in
- fld
- end;
-
-val massage_direct_corec_call = massage_let_if;
+val massage_direct_corec_call = massage_let_if_case;
fun massage_indirect_corec_call ctxt has_call raw_massage_call bound_Ts U t =
let
@@ -257,7 +283,7 @@
val map' = mk_map (length fs) dom_Ts Us map0;
val fs' = map_flattened_map_args ctxt s (map3 massage_map_or_map_arg Us Ts) fs;
in
- list_comb (map', fs')
+ Term.list_comb (map', fs')
end
| NONE => raise AINT_NO_MAP t)
| massage_map _ _ t = raise AINT_NO_MAP t
@@ -269,14 +295,15 @@
handle AINT_NO_MAP _ => massage_direct_fun U T t;
fun massage_call U T =
- massage_let_if ctxt has_call (fn t =>
+ massage_let_if_case ctxt has_call (fn t =>
if has_call t then
(case U of
Type (s, Us) =>
(case try (dest_ctr ctxt s) t of
SOME (f, args) =>
let val f' = mk_ctr Us f in
- list_comb (f', map3 massage_call (binder_types (typof f')) (map typof args) args)
+ Term.list_comb (f',
+ map3 massage_call (binder_types (typof f')) (map typof args) args)
end
| NONE =>
(case t of
@@ -296,45 +323,26 @@
end;
fun expand_ctr_term ctxt s Ts t =
- (case fp_sugar_of ctxt s of
- SOME fp_sugar =>
- let
- val T = Type (s, Ts);
- val x = Bound 0;
- val {ctrs = ctrs0, discs = discs0, selss = selss0, ...} = of_fp_sugar #ctr_sugars fp_sugar;
- val ctrs = map (mk_ctr Ts) ctrs0;
- val discs = map (mk_disc_or_sel Ts) discs0;
- val selss = map (map (mk_disc_or_sel Ts)) selss0;
- val xdiscs = map (rapp x) discs;
- val xselss = map (map (rapp x)) selss;
- val xsel_ctrs = map2 (curry Term.list_comb) ctrs xselss;
- val xif = mk_IfN T xdiscs xsel_ctrs;
- in
- Const (@{const_name Let}, T --> (T --> T) --> T) $ t $ Abs (Name.uu, T, xif)
- end
+ (case ctr_sugar_of ctxt s of
+ SOME {ctrs, casex, ...} =>
+ Term.list_comb (mk_case Ts (Type (s, Ts)) casex, map (mk_ctr Ts) ctrs) $ t
| NONE => raise Fail "expand_ctr_term");
fun expand_corec_code_rhs ctxt has_call bound_Ts t =
(case fastype_of1 (bound_Ts, t) of
T as Type (s, Ts) =>
- massage_let_if ctxt has_call (fn t =>
- if can (dest_ctr ctxt s) t then t
- else massage_let_if ctxt has_call I bound_Ts T (expand_ctr_term ctxt s Ts t)) bound_Ts T t
+ massage_let_if_case ctxt has_call (fn t =>
+ if can (dest_ctr ctxt s) t then
+ t
+ else
+ massage_let_if_case ctxt has_call I bound_Ts T (expand_ctr_term ctxt s Ts t)) bound_Ts T t
| _ => raise Fail "expand_corec_code_rhs");
fun massage_corec_code_rhs ctxt massage_ctr =
- massage_let_if ctxt (K false) (uncurry massage_ctr o Term.strip_comb);
-
-fun fold_rev_corec_code_rhs f = fold_rev_let_if (uncurry f o Term.strip_comb);
+ massage_let_if_case ctxt (K false) (uncurry massage_ctr o Term.strip_comb);
-fun add_conjuncts (Const (@{const_name conj}, _) $ t $ t') = add_conjuncts t o add_conjuncts t'
- | add_conjuncts t = cons t;
-
-fun conjuncts t = add_conjuncts t [];
-
-fun simplify_bool_ifs thy =
- Raw_Simplifier.rewrite_term thy @{thms bool_if_simps[THEN eq_reflection]} []
- #> conjuncts #> (fn [@{term True}] => [] | ts => ts);
+fun fold_rev_corec_code_rhs ctxt f =
+ fold_rev_let_if_case ctxt (fn conds => uncurry (f conds) o Term.strip_comb);
fun indexed xs h = let val h' = h + length xs in (h upto h' - 1, h') end;
fun indexedd xss = fold_map indexed xss;
--- a/src/HOL/IMP/Compiler.thy Wed Sep 25 12:43:20 2013 +0200
+++ b/src/HOL/IMP/Compiler.thy Wed Sep 25 13:39:34 2013 +0200
@@ -21,16 +21,16 @@
where @{term i} is an @{typ int}.
*}
fun inth :: "'a list \<Rightarrow> int \<Rightarrow> 'a" (infixl "!!" 100) where
-"(x # xs) !! n = (if n = 0 then x else xs !! (n - 1))"
+"(x # xs) !! i = (if i = 0 then x else xs !! (i - 1))"
text {*
The only additional lemma we need about this function
is indexing over append:
*}
lemma inth_append [simp]:
- "0 \<le> n \<Longrightarrow>
- (xs @ ys) !! n = (if n < size xs then xs !! n else ys !! (n - size xs))"
-by (induction xs arbitrary: n) (auto simp: algebra_simps)
+ "0 \<le> i \<Longrightarrow>
+ (xs @ ys) !! i = (if i < size xs then xs !! i else ys !! (i - size xs))"
+by (induction xs arbitrary: i) (auto simp: algebra_simps)
subsection "Instructions and Stack Machine"
--- a/src/HOL/Library/Extended_Real.thy Wed Sep 25 12:43:20 2013 +0200
+++ b/src/HOL/Library/Extended_Real.thy Wed Sep 25 13:39:34 2013 +0200
@@ -24,23 +24,29 @@
instantiation ereal :: uminus
begin
- fun uminus_ereal where
- "- (ereal r) = ereal (- r)"
- | "- PInfty = MInfty"
- | "- MInfty = PInfty"
- instance ..
+
+fun uminus_ereal where
+ "- (ereal r) = ereal (- r)"
+| "- PInfty = MInfty"
+| "- MInfty = PInfty"
+
+instance ..
+
end
instantiation ereal :: infinity
begin
- definition "(\<infinity>::ereal) = PInfty"
- instance ..
+
+definition "(\<infinity>::ereal) = PInfty"
+instance ..
+
end
declare [[coercion "ereal :: real \<Rightarrow> ereal"]]
lemma ereal_uminus_uminus[simp]:
- fixes a :: ereal shows "- (- a) = a"
+ fixes a :: ereal
+ shows "- (- a) = a"
by (cases a) simp_all
lemma
@@ -59,7 +65,7 @@
lemma [code_unfold]:
"\<infinity> = PInfty"
- "-PInfty = MInfty"
+ "- PInfty = MInfty"
by simp_all
lemma inj_ereal[simp]: "inj_on ereal A"
@@ -76,77 +82,97 @@
lemmas ereal3_cases = ereal2_cases[case_product ereal_cases]
lemma ereal_uminus_eq_iff[simp]:
- fixes a b :: ereal shows "-a = -b \<longleftrightarrow> a = b"
+ fixes a b :: ereal
+ shows "-a = -b \<longleftrightarrow> a = b"
by (cases rule: ereal2_cases[of a b]) simp_all
function of_ereal :: "ereal \<Rightarrow> real" where
-"of_ereal (ereal r) = r" |
-"of_ereal \<infinity> = 0" |
-"of_ereal (-\<infinity>) = 0"
+ "of_ereal (ereal r) = r"
+| "of_ereal \<infinity> = 0"
+| "of_ereal (-\<infinity>) = 0"
by (auto intro: ereal_cases)
-termination proof qed (rule wf_empty)
+termination by default (rule wf_empty)
defs (overloaded)
real_of_ereal_def [code_unfold]: "real \<equiv> of_ereal"
lemma real_of_ereal[simp]:
- "real (- x :: ereal) = - (real x)"
- "real (ereal r) = r"
- "real (\<infinity>::ereal) = 0"
+ "real (- x :: ereal) = - (real x)"
+ "real (ereal r) = r"
+ "real (\<infinity>::ereal) = 0"
by (cases x) (simp_all add: real_of_ereal_def)
lemma range_ereal[simp]: "range ereal = UNIV - {\<infinity>, -\<infinity>}"
proof safe
- fix x assume "x \<notin> range ereal" "x \<noteq> \<infinity>"
- then show "x = -\<infinity>" by (cases x) auto
+ fix x
+ assume "x \<notin> range ereal" "x \<noteq> \<infinity>"
+ then show "x = -\<infinity>"
+ by (cases x) auto
qed auto
lemma ereal_range_uminus[simp]: "range uminus = (UNIV::ereal set)"
proof safe
- fix x :: ereal show "x \<in> range uminus" by (intro image_eqI[of _ _ "-x"]) auto
+ fix x :: ereal
+ show "x \<in> range uminus"
+ by (intro image_eqI[of _ _ "-x"]) auto
qed auto
instantiation ereal :: abs
begin
- function abs_ereal where
- "\<bar>ereal r\<bar> = ereal \<bar>r\<bar>"
- | "\<bar>-\<infinity>\<bar> = (\<infinity>::ereal)"
- | "\<bar>\<infinity>\<bar> = (\<infinity>::ereal)"
- by (auto intro: ereal_cases)
- termination proof qed (rule wf_empty)
- instance ..
+
+function abs_ereal where
+ "\<bar>ereal r\<bar> = ereal \<bar>r\<bar>"
+| "\<bar>-\<infinity>\<bar> = (\<infinity>::ereal)"
+| "\<bar>\<infinity>\<bar> = (\<infinity>::ereal)"
+by (auto intro: ereal_cases)
+termination proof qed (rule wf_empty)
+
+instance ..
+
end
-lemma abs_eq_infinity_cases[elim!]: "\<lbrakk> \<bar>x :: ereal\<bar> = \<infinity> ; x = \<infinity> \<Longrightarrow> P ; x = -\<infinity> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
- by (cases x) auto
+lemma abs_eq_infinity_cases[elim!]:
+ fixes x :: ereal
+ assumes "\<bar>x\<bar> = \<infinity>"
+ obtains "x = \<infinity>" | "x = -\<infinity>"
+ using assms by (cases x) auto
-lemma abs_neq_infinity_cases[elim!]: "\<lbrakk> \<bar>x :: ereal\<bar> \<noteq> \<infinity> ; \<And>r. x = ereal r \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
+lemma abs_neq_infinity_cases[elim!]:
+ fixes x :: ereal
+ assumes "\<bar>x\<bar> \<noteq> \<infinity>"
+ obtains r where "x = ereal r"
+ using assms by (cases x) auto
+
+lemma abs_ereal_uminus[simp]:
+ fixes x :: ereal
+ shows "\<bar>- x\<bar> = \<bar>x\<bar>"
by (cases x) auto
-lemma abs_ereal_uminus[simp]: "\<bar>- x\<bar> = \<bar>x::ereal\<bar>"
- by (cases x) auto
+lemma ereal_infinity_cases:
+ fixes a :: ereal
+ shows "a \<noteq> \<infinity> \<Longrightarrow> a \<noteq> -\<infinity> \<Longrightarrow> \<bar>a\<bar> \<noteq> \<infinity>"
+ by auto
-lemma ereal_infinity_cases: "(a::ereal) \<noteq> \<infinity> \<Longrightarrow> a \<noteq> -\<infinity> \<Longrightarrow> \<bar>a\<bar> \<noteq> \<infinity>"
- by auto
subsubsection "Addition"
-instantiation ereal :: "{one, comm_monoid_add}"
+instantiation ereal :: "{one,comm_monoid_add}"
begin
definition "0 = ereal 0"
definition "1 = ereal 1"
function plus_ereal where
-"ereal r + ereal p = ereal (r + p)" |
-"\<infinity> + a = (\<infinity>::ereal)" |
-"a + \<infinity> = (\<infinity>::ereal)" |
-"ereal r + -\<infinity> = - \<infinity>" |
-"-\<infinity> + ereal p = -(\<infinity>::ereal)" |
-"-\<infinity> + -\<infinity> = -(\<infinity>::ereal)"
+ "ereal r + ereal p = ereal (r + p)"
+| "\<infinity> + a = (\<infinity>::ereal)"
+| "a + \<infinity> = (\<infinity>::ereal)"
+| "ereal r + -\<infinity> = - \<infinity>"
+| "-\<infinity> + ereal p = -(\<infinity>::ereal)"
+| "-\<infinity> + -\<infinity> = -(\<infinity>::ereal)"
proof -
case (goal1 P x)
- then obtain a b where "x = (a, b)" by (cases x) auto
+ then obtain a b where "x = (a, b)"
+ by (cases x) auto
with goal1 show P
by (cases rule: ereal2_cases[of a b]) auto
qed auto
@@ -172,6 +198,7 @@
show "a + b + c = a + (b + c)"
by (cases rule: ereal3_cases[of a b c]) simp_all
qed
+
end
instance ereal :: numeral ..
@@ -182,35 +209,37 @@
lemma abs_ereal_zero[simp]: "\<bar>0\<bar> = (0::ereal)"
unfolding zero_ereal_def abs_ereal.simps by simp
-lemma ereal_uminus_zero[simp]:
- "- 0 = (0::ereal)"
+lemma ereal_uminus_zero[simp]: "- 0 = (0::ereal)"
by (simp add: zero_ereal_def)
lemma ereal_uminus_zero_iff[simp]:
- fixes a :: ereal shows "-a = 0 \<longleftrightarrow> a = 0"
+ fixes a :: ereal
+ shows "-a = 0 \<longleftrightarrow> a = 0"
by (cases a) simp_all
lemma ereal_plus_eq_PInfty[simp]:
- fixes a b :: ereal shows "a + b = \<infinity> \<longleftrightarrow> a = \<infinity> \<or> b = \<infinity>"
+ fixes a b :: ereal
+ shows "a + b = \<infinity> \<longleftrightarrow> a = \<infinity> \<or> b = \<infinity>"
by (cases rule: ereal2_cases[of a b]) auto
lemma ereal_plus_eq_MInfty[simp]:
- fixes a b :: ereal shows "a + b = -\<infinity> \<longleftrightarrow>
- (a = -\<infinity> \<or> b = -\<infinity>) \<and> a \<noteq> \<infinity> \<and> b \<noteq> \<infinity>"
+ fixes a b :: ereal
+ shows "a + b = -\<infinity> \<longleftrightarrow> (a = -\<infinity> \<or> b = -\<infinity>) \<and> a \<noteq> \<infinity> \<and> b \<noteq> \<infinity>"
by (cases rule: ereal2_cases[of a b]) auto
lemma ereal_add_cancel_left:
- fixes a b :: ereal assumes "a \<noteq> -\<infinity>"
- shows "a + b = a + c \<longleftrightarrow> (a = \<infinity> \<or> b = c)"
+ fixes a b :: ereal
+ assumes "a \<noteq> -\<infinity>"
+ shows "a + b = a + c \<longleftrightarrow> a = \<infinity> \<or> b = c"
using assms by (cases rule: ereal3_cases[of a b c]) auto
lemma ereal_add_cancel_right:
- fixes a b :: ereal assumes "a \<noteq> -\<infinity>"
- shows "b + a = c + a \<longleftrightarrow> (a = \<infinity> \<or> b = c)"
+ fixes a b :: ereal
+ assumes "a \<noteq> -\<infinity>"
+ shows "b + a = c + a \<longleftrightarrow> a = \<infinity> \<or> b = c"
using assms by (cases rule: ereal3_cases[of a b c]) auto
-lemma ereal_real:
- "ereal (real x) = (if \<bar>x\<bar> = \<infinity> then 0 else x)"
+lemma ereal_real: "ereal (real x) = (if \<bar>x\<bar> = \<infinity> then 0 else x)"
by (cases x) simp_all
lemma real_of_ereal_add:
@@ -219,6 +248,7 @@
(if (\<bar>a\<bar> = \<infinity>) \<and> (\<bar>b\<bar> = \<infinity>) \<or> (\<bar>a\<bar> \<noteq> \<infinity>) \<and> (\<bar>b\<bar> \<noteq> \<infinity>) then real a + real b else 0)"
by (cases rule: ereal2_cases[of a b]) auto
+
subsubsection "Linear order on @{typ ereal}"
instantiation ereal :: linorder
@@ -250,7 +280,7 @@
lemma ereal_infty_less_eq[simp]:
fixes x :: ereal
shows "\<infinity> \<le> x \<longleftrightarrow> x = \<infinity>"
- "x \<le> -\<infinity> \<longleftrightarrow> x = -\<infinity>"
+ and "x \<le> -\<infinity> \<longleftrightarrow> x = -\<infinity>"
by (auto simp add: less_eq_ereal_def)
lemma ereal_less[simp]:
@@ -282,10 +312,16 @@
by (cases rule: ereal2_cases[of x y]) auto
show "x \<le> y \<or> y \<le> x "
by (cases rule: ereal2_cases[of x y]) auto
- { assume "x \<le> y" "y \<le> x" then show "x = y"
- by (cases rule: ereal2_cases[of x y]) auto }
- { assume "x \<le> y" "y \<le> z" then show "x \<le> z"
- by (cases rule: ereal3_cases[of x y z]) auto }
+ {
+ assume "x \<le> y" "y \<le> x"
+ then show "x = y"
+ by (cases rule: ereal2_cases[of x y]) auto
+ }
+ {
+ assume "x \<le> y" "y \<le> z"
+ then show "x \<le> z"
+ by (cases rule: ereal3_cases[of x y z]) auto
+ }
qed
end
@@ -298,20 +334,25 @@
instance ereal :: ordered_ab_semigroup_add
proof
- fix a b c :: ereal assume "a \<le> b" then show "c + a \<le> c + b"
+ fix a b c :: ereal
+ assume "a \<le> b"
+ then show "c + a \<le> c + b"
by (cases rule: ereal3_cases[of a b c]) auto
qed
lemma real_of_ereal_positive_mono:
- fixes x y :: ereal shows "\<lbrakk>0 \<le> x; x \<le> y; y \<noteq> \<infinity>\<rbrakk> \<Longrightarrow> real x \<le> real y"
+ fixes x y :: ereal
+ shows "0 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<noteq> \<infinity> \<Longrightarrow> real x \<le> real y"
by (cases rule: ereal2_cases[of x y]) auto
lemma ereal_MInfty_lessI[intro, simp]:
- fixes a :: ereal shows "a \<noteq> -\<infinity> \<Longrightarrow> -\<infinity> < a"
+ fixes a :: ereal
+ shows "a \<noteq> -\<infinity> \<Longrightarrow> -\<infinity> < a"
by (cases a) auto
lemma ereal_less_PInfty[intro, simp]:
- fixes a :: ereal shows "a \<noteq> \<infinity> \<Longrightarrow> a < \<infinity>"
+ fixes a :: ereal
+ shows "a \<noteq> \<infinity> \<Longrightarrow> a < \<infinity>"
by (cases a) auto
lemma ereal_less_ereal_Ex:
@@ -321,12 +362,16 @@
lemma less_PInf_Ex_of_nat: "x \<noteq> \<infinity> \<longleftrightarrow> (\<exists>n::nat. x < ereal (real n))"
proof (cases x)
- case (real r) then show ?thesis
+ case (real r)
+ then show ?thesis
using reals_Archimedean2[of r] by simp
qed simp_all
lemma ereal_add_mono:
- fixes a b c d :: ereal assumes "a \<le> b" "c \<le> d" shows "a + c \<le> b + d"
+ fixes a b c d :: ereal
+ assumes "a \<le> b"
+ and "c \<le> d"
+ shows "a + c \<le> b + d"
using assms
apply (cases a)
apply (cases rule: ereal3_cases[of b c d], auto)
@@ -334,31 +379,34 @@
done
lemma ereal_minus_le_minus[simp]:
- fixes a b :: ereal shows "- a \<le> - b \<longleftrightarrow> b \<le> a"
+ fixes a b :: ereal
+ shows "- a \<le> - b \<longleftrightarrow> b \<le> a"
by (cases rule: ereal2_cases[of a b]) auto
lemma ereal_minus_less_minus[simp]:
- fixes a b :: ereal shows "- a < - b \<longleftrightarrow> b < a"
+ fixes a b :: ereal
+ shows "- a < - b \<longleftrightarrow> b < a"
by (cases rule: ereal2_cases[of a b]) auto
lemma ereal_le_real_iff:
- "x \<le> real y \<longleftrightarrow> ((\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> ereal x \<le> y) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> x \<le> 0))"
+ "x \<le> real y \<longleftrightarrow> (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> ereal x \<le> y) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> x \<le> 0)"
by (cases y) auto
lemma real_le_ereal_iff:
- "real y \<le> x \<longleftrightarrow> ((\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y \<le> ereal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 \<le> x))"
+ "real y \<le> x \<longleftrightarrow> (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y \<le> ereal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 \<le> x)"
by (cases y) auto
lemma ereal_less_real_iff:
- "x < real y \<longleftrightarrow> ((\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> ereal x < y) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> x < 0))"
+ "x < real y \<longleftrightarrow> (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> ereal x < y) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> x < 0)"
by (cases y) auto
lemma real_less_ereal_iff:
- "real y < x \<longleftrightarrow> ((\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y < ereal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 < x))"
+ "real y < x \<longleftrightarrow> (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> y < ereal x) \<and> (\<bar>y\<bar> = \<infinity> \<longrightarrow> 0 < x)"
by (cases y) auto
lemma real_of_ereal_pos:
- fixes x :: ereal shows "0 \<le> x \<Longrightarrow> 0 \<le> real x" by (cases x) auto
+ fixes x :: ereal
+ shows "0 \<le> x \<Longrightarrow> 0 \<le> real x" by (cases x) auto
lemmas real_of_ereal_ord_simps =
ereal_le_real_iff real_le_ereal_iff ereal_less_real_iff real_less_ereal_iff
@@ -372,35 +420,44 @@
lemma abs_ereal_pos[simp]: "0 \<le> \<bar>x :: ereal\<bar>"
by (cases x) auto
-lemma real_of_ereal_le_0[simp]: "real (x :: ereal) \<le> 0 \<longleftrightarrow> (x \<le> 0 \<or> x = \<infinity>)"
+lemma real_of_ereal_le_0[simp]: "real (x :: ereal) \<le> 0 \<longleftrightarrow> x \<le> 0 \<or> x = \<infinity>"
by (cases x) auto
lemma abs_real_of_ereal[simp]: "\<bar>real (x :: ereal)\<bar> = real \<bar>x\<bar>"
by (cases x) auto
lemma zero_less_real_of_ereal:
- fixes x :: ereal shows "0 < real x \<longleftrightarrow> (0 < x \<and> x \<noteq> \<infinity>)"
+ fixes x :: ereal
+ shows "0 < real x \<longleftrightarrow> 0 < x \<and> x \<noteq> \<infinity>"
by (cases x) auto
lemma ereal_0_le_uminus_iff[simp]:
- fixes a :: ereal shows "0 \<le> -a \<longleftrightarrow> a \<le> 0"
+ fixes a :: ereal
+ shows "0 \<le> - a \<longleftrightarrow> a \<le> 0"
by (cases rule: ereal2_cases[of a]) auto
lemma ereal_uminus_le_0_iff[simp]:
- fixes a :: ereal shows "-a \<le> 0 \<longleftrightarrow> 0 \<le> a"
+ fixes a :: ereal
+ shows "- a \<le> 0 \<longleftrightarrow> 0 \<le> a"
by (cases rule: ereal2_cases[of a]) auto
lemma ereal_add_strict_mono:
fixes a b c d :: ereal
- assumes "a = b" "0 \<le> a" "a \<noteq> \<infinity>" "c < d"
+ assumes "a = b"
+ and "0 \<le> a"
+ and "a \<noteq> \<infinity>"
+ and "c < d"
shows "a + c < b + d"
- using assms by (cases rule: ereal3_cases[case_product ereal_cases, of a b c d]) auto
+ using assms
+ by (cases rule: ereal3_cases[case_product ereal_cases, of a b c d]) auto
-lemma ereal_less_add:
- fixes a b c :: ereal shows "\<bar>a\<bar> \<noteq> \<infinity> \<Longrightarrow> c < b \<Longrightarrow> a + c < a + b"
+lemma ereal_less_add:
+ fixes a b c :: ereal
+ shows "\<bar>a\<bar> \<noteq> \<infinity> \<Longrightarrow> c < b \<Longrightarrow> a + c < a + b"
by (cases rule: ereal2_cases[of b c]) auto
-lemma ereal_uminus_eq_reorder: "- a = b \<longleftrightarrow> a = (-b::ereal)" by auto
+lemma ereal_uminus_eq_reorder: "- a = b \<longleftrightarrow> a = (-b::ereal)"
+ by auto
lemma ereal_uminus_less_reorder: "- a < b \<longleftrightarrow> -b < (a::ereal)"
by (subst (3) ereal_uminus_uminus[symmetric]) (simp only: ereal_minus_less_minus)
@@ -412,23 +469,39 @@
ereal_uminus_eq_reorder ereal_uminus_less_reorder ereal_uminus_le_reorder
lemma ereal_bot:
- fixes x :: ereal assumes "\<And>B. x \<le> ereal B" shows "x = - \<infinity>"
+ fixes x :: ereal
+ assumes "\<And>B. x \<le> ereal B"
+ shows "x = - \<infinity>"
proof (cases x)
- case (real r) with assms[of "r - 1"] show ?thesis by auto
+ case (real r)
+ with assms[of "r - 1"] show ?thesis
+ by auto
next
- case PInf with assms[of 0] show ?thesis by auto
+ case PInf
+ with assms[of 0] show ?thesis
+ by auto
next
- case MInf then show ?thesis by simp
+ case MInf
+ then show ?thesis
+ by simp
qed
lemma ereal_top:
- fixes x :: ereal assumes "\<And>B. x \<ge> ereal B" shows "x = \<infinity>"
+ fixes x :: ereal
+ assumes "\<And>B. x \<ge> ereal B"
+ shows "x = \<infinity>"
proof (cases x)
- case (real r) with assms[of "r + 1"] show ?thesis by auto
+ case (real r)
+ with assms[of "r + 1"] show ?thesis
+ by auto
next
- case MInf with assms[of 0] show ?thesis by auto
+ case MInf
+ with assms[of 0] show ?thesis
+ by auto
next
- case PInf then show ?thesis by simp
+ case PInf
+ then show ?thesis
+ by simp
qed
lemma
@@ -449,32 +522,36 @@
unfolding incseq_def by auto
lemma ereal_add_nonneg_nonneg:
- fixes a b :: ereal shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b"
+ fixes a b :: ereal
+ shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a + b"
using add_mono[of 0 a 0 b] by simp
-lemma image_eqD: "f ` A = B \<Longrightarrow> (\<forall>x\<in>A. f x \<in> B)"
+lemma image_eqD: "f ` A = B \<Longrightarrow> \<forall>x\<in>A. f x \<in> B"
by auto
lemma incseq_setsumI:
- fixes f :: "nat \<Rightarrow> 'a::{comm_monoid_add, ordered_ab_semigroup_add}"
+ fixes f :: "nat \<Rightarrow> 'a::{comm_monoid_add,ordered_ab_semigroup_add}"
assumes "\<And>i. 0 \<le> f i"
shows "incseq (\<lambda>i. setsum f {..< i})"
proof (intro incseq_SucI)
- fix n have "setsum f {..< n} + 0 \<le> setsum f {..<n} + f n"
+ fix n
+ have "setsum f {..< n} + 0 \<le> setsum f {..<n} + f n"
using assms by (rule add_left_mono)
then show "setsum f {..< n} \<le> setsum f {..< Suc n}"
by auto
qed
lemma incseq_setsumI2:
- fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::{comm_monoid_add, ordered_ab_semigroup_add}"
+ fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::{comm_monoid_add,ordered_ab_semigroup_add}"
assumes "\<And>n. n \<in> A \<Longrightarrow> incseq (f n)"
shows "incseq (\<lambda>i. \<Sum>n\<in>A. f n i)"
- using assms unfolding incseq_def by (auto intro: setsum_mono)
+ using assms
+ unfolding incseq_def by (auto intro: setsum_mono)
+
subsubsection "Multiplication"
-instantiation ereal :: "{comm_monoid_mult, sgn}"
+instantiation ereal :: "{comm_monoid_mult,sgn}"
begin
function sgn_ereal :: "ereal \<Rightarrow> ereal" where
@@ -482,28 +559,31 @@
| "sgn (\<infinity>::ereal) = 1"
| "sgn (-\<infinity>::ereal) = -1"
by (auto intro: ereal_cases)
-termination proof qed (rule wf_empty)
+termination by default (rule wf_empty)
function times_ereal where
-"ereal r * ereal p = ereal (r * p)" |
-"ereal r * \<infinity> = (if r = 0 then 0 else if r > 0 then \<infinity> else -\<infinity>)" |
-"\<infinity> * ereal r = (if r = 0 then 0 else if r > 0 then \<infinity> else -\<infinity>)" |
-"ereal r * -\<infinity> = (if r = 0 then 0 else if r > 0 then -\<infinity> else \<infinity>)" |
-"-\<infinity> * ereal r = (if r = 0 then 0 else if r > 0 then -\<infinity> else \<infinity>)" |
-"(\<infinity>::ereal) * \<infinity> = \<infinity>" |
-"-(\<infinity>::ereal) * \<infinity> = -\<infinity>" |
-"(\<infinity>::ereal) * -\<infinity> = -\<infinity>" |
-"-(\<infinity>::ereal) * -\<infinity> = \<infinity>"
+ "ereal r * ereal p = ereal (r * p)"
+| "ereal r * \<infinity> = (if r = 0 then 0 else if r > 0 then \<infinity> else -\<infinity>)"
+| "\<infinity> * ereal r = (if r = 0 then 0 else if r > 0 then \<infinity> else -\<infinity>)"
+| "ereal r * -\<infinity> = (if r = 0 then 0 else if r > 0 then -\<infinity> else \<infinity>)"
+| "-\<infinity> * ereal r = (if r = 0 then 0 else if r > 0 then -\<infinity> else \<infinity>)"
+| "(\<infinity>::ereal) * \<infinity> = \<infinity>"
+| "-(\<infinity>::ereal) * \<infinity> = -\<infinity>"
+| "(\<infinity>::ereal) * -\<infinity> = -\<infinity>"
+| "-(\<infinity>::ereal) * -\<infinity> = \<infinity>"
proof -
case (goal1 P x)
- then obtain a b where "x = (a, b)" by (cases x) auto
- with goal1 show P by (cases rule: ereal2_cases[of a b]) auto
+ then obtain a b where "x = (a, b)"
+ by (cases x) auto
+ with goal1 show P
+ by (cases rule: ereal2_cases[of a b]) auto
qed simp_all
termination by (relation "{}") simp
instance
proof
- fix a b c :: ereal show "1 * a = a"
+ fix a b c :: ereal
+ show "1 * a = a"
by (cases a) (simp_all add: one_ereal_def)
show "a * b = b * a"
by (cases rule: ereal2_cases[of a b]) simp_all
@@ -511,36 +591,39 @@
by (cases rule: ereal3_cases[of a b c])
(simp_all add: zero_ereal_def zero_less_mult_iff)
qed
+
end
lemma real_ereal_1[simp]: "real (1::ereal) = 1"
unfolding one_ereal_def by simp
lemma real_of_ereal_le_1:
- fixes a :: ereal shows "a \<le> 1 \<Longrightarrow> real a \<le> 1"
+ fixes a :: ereal
+ shows "a \<le> 1 \<Longrightarrow> real a \<le> 1"
by (cases a) (auto simp: one_ereal_def)
lemma abs_ereal_one[simp]: "\<bar>1\<bar> = (1::ereal)"
unfolding one_ereal_def by simp
lemma ereal_mult_zero[simp]:
- fixes a :: ereal shows "a * 0 = 0"
+ fixes a :: ereal
+ shows "a * 0 = 0"
by (cases a) (simp_all add: zero_ereal_def)
lemma ereal_zero_mult[simp]:
- fixes a :: ereal shows "0 * a = 0"
+ fixes a :: ereal
+ shows "0 * a = 0"
by (cases a) (simp_all add: zero_ereal_def)
-lemma ereal_m1_less_0[simp]:
- "-(1::ereal) < 0"
+lemma ereal_m1_less_0[simp]: "-(1::ereal) < 0"
by (simp add: zero_ereal_def one_ereal_def)
-lemma ereal_zero_m1[simp]:
- "1 \<noteq> (0::ereal)"
+lemma ereal_zero_m1[simp]: "1 \<noteq> (0::ereal)"
by (simp add: zero_ereal_def one_ereal_def)
lemma ereal_times_0[simp]:
- fixes x :: ereal shows "0 * x = 0"
+ fixes x :: ereal
+ shows "0 * x = 0"
by (cases x) (auto simp: zero_ereal_def)
lemma ereal_times[simp]:
@@ -549,21 +632,24 @@
by (auto simp add: times_ereal_def one_ereal_def)
lemma ereal_plus_1[simp]:
- "1 + ereal r = ereal (r + 1)" "ereal r + 1 = ereal (r + 1)"
- "1 + -(\<infinity>::ereal) = -\<infinity>" "-(\<infinity>::ereal) + 1 = -\<infinity>"
+ "1 + ereal r = ereal (r + 1)"
+ "ereal r + 1 = ereal (r + 1)"
+ "1 + -(\<infinity>::ereal) = -\<infinity>"
+ "-(\<infinity>::ereal) + 1 = -\<infinity>"
unfolding one_ereal_def by auto
lemma ereal_zero_times[simp]:
- fixes a b :: ereal shows "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
+ fixes a b :: ereal
+ shows "a * b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
by (cases rule: ereal2_cases[of a b]) auto
lemma ereal_mult_eq_PInfty[simp]:
- shows "a * b = (\<infinity>::ereal) \<longleftrightarrow>
+ "a * b = (\<infinity>::ereal) \<longleftrightarrow>
(a = \<infinity> \<and> b > 0) \<or> (a > 0 \<and> b = \<infinity>) \<or> (a = -\<infinity> \<and> b < 0) \<or> (a < 0 \<and> b = -\<infinity>)"
by (cases rule: ereal2_cases[of a b]) auto
lemma ereal_mult_eq_MInfty[simp]:
- shows "a * b = -(\<infinity>::ereal) \<longleftrightarrow>
+ "a * b = -(\<infinity>::ereal) \<longleftrightarrow>
(a = \<infinity> \<and> b < 0) \<or> (a < 0 \<and> b = \<infinity>) \<or> (a = -\<infinity> \<and> b > 0) \<or> (a > 0 \<and> b = -\<infinity>)"
by (cases rule: ereal2_cases[of a b]) auto
@@ -574,11 +660,13 @@
by (simp_all add: zero_ereal_def one_ereal_def)
lemma ereal_mult_minus_left[simp]:
- fixes a b :: ereal shows "-a * b = - (a * b)"
+ fixes a b :: ereal
+ shows "-a * b = - (a * b)"
by (cases rule: ereal2_cases[of a b]) auto
lemma ereal_mult_minus_right[simp]:
- fixes a b :: ereal shows "a * -b = - (a * b)"
+ fixes a b :: ereal
+ shows "a * -b = - (a * b)"
by (cases rule: ereal2_cases[of a b]) auto
lemma ereal_mult_infty[simp]:
@@ -590,26 +678,33 @@
by (cases a) auto
lemma ereal_mult_strict_right_mono:
- assumes "a < b" and "0 < c" "c < (\<infinity>::ereal)"
+ assumes "a < b"
+ and "0 < c"
+ and "c < (\<infinity>::ereal)"
shows "a * c < b * c"
using assms
- by (cases rule: ereal3_cases[of a b c])
- (auto simp: zero_le_mult_iff)
+ by (cases rule: ereal3_cases[of a b c]) (auto simp: zero_le_mult_iff)
lemma ereal_mult_strict_left_mono:
- "\<lbrakk> a < b ; 0 < c ; c < (\<infinity>::ereal)\<rbrakk> \<Longrightarrow> c * a < c * b"
- using ereal_mult_strict_right_mono by (simp add: mult_commute[of c])
+ "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c < (\<infinity>::ereal) \<Longrightarrow> c * a < c * b"
+ using ereal_mult_strict_right_mono
+ by (simp add: mult_commute[of c])
lemma ereal_mult_right_mono:
- fixes a b c :: ereal shows "\<lbrakk>a \<le> b; 0 \<le> c\<rbrakk> \<Longrightarrow> a*c \<le> b*c"
+ fixes a b c :: ereal
+ shows "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
using assms
- apply (cases "c = 0") apply simp
- by (cases rule: ereal3_cases[of a b c])
- (auto simp: zero_le_mult_iff)
+ apply (cases "c = 0")
+ apply simp
+ apply (cases rule: ereal3_cases[of a b c])
+ apply (auto simp: zero_le_mult_iff)
+ done
lemma ereal_mult_left_mono:
- fixes a b c :: ereal shows "\<lbrakk>a \<le> b; 0 \<le> c\<rbrakk> \<Longrightarrow> c * a \<le> c * b"
- using ereal_mult_right_mono by (simp add: mult_commute[of c])
+ fixes a b c :: ereal
+ shows "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
+ using ereal_mult_right_mono
+ by (simp add: mult_commute[of c])
lemma zero_less_one_ereal[simp]: "0 \<le> (1::ereal)"
by (simp add: one_ereal_def zero_ereal_def)
@@ -618,11 +713,13 @@
by (cases rule: ereal2_cases[of a b]) (auto simp: mult_nonneg_nonneg)
lemma ereal_right_distrib:
- fixes r a b :: ereal shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> r * (a + b) = r * a + r * b"
+ fixes r a b :: ereal
+ shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> r * (a + b) = r * a + r * b"
by (cases rule: ereal3_cases[of r a b]) (simp_all add: field_simps)
lemma ereal_left_distrib:
- fixes r a b :: ereal shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> (a + b) * r = a * r + b * r"
+ fixes r a b :: ereal
+ shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> (a + b) * r = a * r + b * r"
by (cases rule: ereal3_cases[of r a b]) (simp_all add: field_simps)
lemma ereal_mult_le_0_iff:
@@ -657,7 +754,9 @@
lemma ereal_distrib:
fixes a b c :: ereal
- assumes "a \<noteq> \<infinity> \<or> b \<noteq> -\<infinity>" "a \<noteq> -\<infinity> \<or> b \<noteq> \<infinity>" "\<bar>c\<bar> \<noteq> \<infinity>"
+ assumes "a \<noteq> \<infinity> \<or> b \<noteq> -\<infinity>"
+ and "a \<noteq> -\<infinity> \<or> b \<noteq> \<infinity>"
+ and "\<bar>c\<bar> \<noteq> \<infinity>"
shows "(a + b) * c = a * c + b * c"
using assms
by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)
@@ -670,74 +769,119 @@
lemma ereal_le_epsilon:
fixes x y :: ereal
- assumes "ALL e. 0 < e --> x <= y + e"
- shows "x <= y"
-proof-
-{ assume a: "EX r. y = ereal r"
- then obtain r where r_def: "y = ereal r" by auto
- { assume "x=(-\<infinity>)" hence ?thesis by auto }
+ assumes "\<forall>e. 0 < e \<longrightarrow> x \<le> y + e"
+ shows "x \<le> y"
+proof -
+ {
+ assume a: "\<exists>r. y = ereal r"
+ then obtain r where r_def: "y = ereal r"
+ by auto
+ {
+ assume "x = -\<infinity>"
+ then have ?thesis by auto
+ }
+ moreover
+ {
+ assume "x \<noteq> -\<infinity>"
+ then obtain p where p_def: "x = ereal p"
+ using a assms[rule_format, of 1]
+ by (cases x) auto
+ {
+ fix e
+ have "0 < e \<longrightarrow> p \<le> r + e"
+ using assms[rule_format, of "ereal e"] p_def r_def by auto
+ }
+ then have "p \<le> r"
+ apply (subst field_le_epsilon)
+ apply auto
+ done
+ then have ?thesis
+ using r_def p_def by auto
+ }
+ ultimately have ?thesis
+ by blast
+ }
moreover
- { assume "~(x=(-\<infinity>))"
- then obtain p where p_def: "x = ereal p"
- using a assms[rule_format, of 1] by (cases x) auto
- { fix e have "0 < e --> p <= r + e"
- using assms[rule_format, of "ereal e"] p_def r_def by auto }
- hence "p <= r" apply (subst field_le_epsilon) by auto
- hence ?thesis using r_def p_def by auto
- } ultimately have ?thesis by blast
-}
-moreover
-{ assume "y=(-\<infinity>) | y=\<infinity>" hence ?thesis
- using assms[rule_format, of 1] by (cases x) auto
-} ultimately show ?thesis by (cases y) auto
+ {
+ assume "y = -\<infinity> | y = \<infinity>"
+ then have ?thesis
+ using assms[rule_format, of 1] by (cases x) auto
+ }
+ ultimately show ?thesis
+ by (cases y) auto
qed
-
lemma ereal_le_epsilon2:
fixes x y :: ereal
- assumes "ALL e. 0 < e --> x <= y + ereal e"
- shows "x <= y"
-proof-
-{ fix e :: ereal assume "e>0"
- { assume "e=\<infinity>" hence "x<=y+e" by auto }
- moreover
- { assume "e~=\<infinity>"
- then obtain r where "e = ereal r" using `e>0` apply (cases e) by auto
- hence "x<=y+e" using assms[rule_format, of r] `e>0` by auto
- } ultimately have "x<=y+e" by blast
-} then show ?thesis using ereal_le_epsilon by auto
+ assumes "\<forall>e. 0 < e \<longrightarrow> x \<le> y + ereal e"
+ shows "x \<le> y"
+proof -
+ {
+ fix e :: ereal
+ assume "e > 0"
+ {
+ assume "e = \<infinity>"
+ then have "x \<le> y + e"
+ by auto
+ }
+ moreover
+ {
+ assume "e \<noteq> \<infinity>"
+ then obtain r where "e = ereal r"
+ using `e > 0` by (cases e) auto
+ then have "x \<le> y + e"
+ using assms[rule_format, of r] `e>0` by auto
+ }
+ ultimately have "x \<le> y + e"
+ by blast
+ }
+ then show ?thesis
+ using ereal_le_epsilon by auto
qed
lemma ereal_le_real:
fixes x y :: ereal
- assumes "ALL z. x <= ereal z --> y <= ereal z"
- shows "y <= x"
-by (metis assms ereal_bot ereal_cases ereal_infty_less_eq(2) ereal_less_eq(1) linorder_le_cases)
+ assumes "\<forall>z. x \<le> ereal z \<longrightarrow> y \<le> ereal z"
+ shows "y \<le> x"
+ by (metis assms ereal_bot ereal_cases ereal_infty_less_eq(2) ereal_less_eq(1) linorder_le_cases)
lemma setprod_ereal_0:
fixes f :: "'a \<Rightarrow> ereal"
- shows "(\<Prod>i\<in>A. f i) = 0 \<longleftrightarrow> (finite A \<and> (\<exists>i\<in>A. f i = 0))"
-proof cases
- assume "finite A"
+ shows "(\<Prod>i\<in>A. f i) = 0 \<longleftrightarrow> finite A \<and> (\<exists>i\<in>A. f i = 0)"
+proof (cases "finite A")
+ case True
then show ?thesis by (induct A) auto
-qed auto
+next
+ case False
+ then show ?thesis by auto
+qed
lemma setprod_ereal_pos:
- fixes f :: "'a \<Rightarrow> ereal" assumes pos: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" shows "0 \<le> (\<Prod>i\<in>I. f i)"
-proof cases
- assume "finite I" from this pos show ?thesis by induct auto
-qed simp
+ fixes f :: "'a \<Rightarrow> ereal"
+ assumes pos: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
+ shows "0 \<le> (\<Prod>i\<in>I. f i)"
+proof (cases "finite I")
+ case True
+ from this pos show ?thesis
+ by induct auto
+next
+ case False
+ then show ?thesis by simp
+qed
lemma setprod_PInf:
fixes f :: "'a \<Rightarrow> ereal"
assumes "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
shows "(\<Prod>i\<in>I. f i) = \<infinity> \<longleftrightarrow> finite I \<and> (\<exists>i\<in>I. f i = \<infinity>) \<and> (\<forall>i\<in>I. f i \<noteq> 0)"
-proof cases
- assume "finite I" from this assms show ?thesis
+proof (cases "finite I")
+ case True
+ from this assms show ?thesis
proof (induct I)
case (insert i I)
- then have pos: "0 \<le> f i" "0 \<le> setprod f I" by (auto intro!: setprod_ereal_pos)
- from insert have "(\<Prod>j\<in>insert i I. f j) = \<infinity> \<longleftrightarrow> setprod f I * f i = \<infinity>" by auto
+ then have pos: "0 \<le> f i" "0 \<le> setprod f I"
+ by (auto intro!: setprod_ereal_pos)
+ from insert have "(\<Prod>j\<in>insert i I. f j) = \<infinity> \<longleftrightarrow> setprod f I * f i = \<infinity>"
+ by auto
also have "\<dots> \<longleftrightarrow> (setprod f I = \<infinity> \<or> f i = \<infinity>) \<and> f i \<noteq> 0 \<and> setprod f I \<noteq> 0"
using setprod_ereal_pos[of I f] pos
by (cases rule: ereal2_cases[of "f i" "setprod f I"]) auto
@@ -745,13 +889,22 @@
using insert by (auto simp: setprod_ereal_0)
finally show ?case .
qed simp
-qed simp
+next
+ case False
+ then show ?thesis by simp
+qed
lemma setprod_ereal: "(\<Prod>i\<in>A. ereal (f i)) = ereal (setprod f A)"
-proof cases
- assume "finite A" then show ?thesis
+proof (cases "finite A")
+ case True
+ then show ?thesis
by induct (auto simp: one_ereal_def)
-qed (simp add: one_ereal_def)
+next
+ case False
+ then show ?thesis
+ by (simp add: one_ereal_def)
+qed
+
subsubsection {* Power *}
@@ -771,10 +924,12 @@
by (induct n) (auto simp: one_ereal_def)
lemma zero_le_power_ereal[simp]:
- fixes a :: ereal assumes "0 \<le> a"
+ fixes a :: ereal
+ assumes "0 \<le> a"
shows "0 \<le> a ^ n"
using assms by (induct n) (auto simp: ereal_zero_le_0_iff)
+
subsubsection {* Subtraction *}
lemma ereal_minus_minus_image[simp]:
@@ -783,25 +938,30 @@
by (auto simp: image_iff)
lemma ereal_uminus_lessThan[simp]:
- fixes a :: ereal shows "uminus ` {..<a} = {-a<..}"
+ fixes a :: ereal
+ shows "uminus ` {..<a} = {-a<..}"
proof -
{
- fix x assume "-a < x"
- then have "- x < - (- a)" by (simp del: ereal_uminus_uminus)
- then have "- x < a" by simp
+ fix x
+ assume "-a < x"
+ then have "- x < - (- a)"
+ by (simp del: ereal_uminus_uminus)
+ then have "- x < a"
+ by simp
}
- then show ?thesis by (auto intro!: image_eqI)
+ then show ?thesis
+ by (auto intro!: image_eqI)
qed
-lemma ereal_uminus_greaterThan[simp]:
- "uminus ` {(a::ereal)<..} = {..<-a}"
- by (metis ereal_uminus_lessThan ereal_uminus_uminus
- ereal_minus_minus_image)
+lemma ereal_uminus_greaterThan[simp]: "uminus ` {(a::ereal)<..} = {..<-a}"
+ by (metis ereal_uminus_lessThan ereal_uminus_uminus ereal_minus_minus_image)
instantiation ereal :: minus
begin
+
definition "x - y = x + -(y::ereal)"
instance ..
+
end
lemma ereal_minus[simp]:
@@ -815,8 +975,7 @@
"0 - x = -x"
by (simp_all add: minus_ereal_def)
-lemma ereal_x_minus_x[simp]:
- "x - x = (if \<bar>x\<bar> = \<infinity> then \<infinity> else 0::ereal)"
+lemma ereal_x_minus_x[simp]: "x - x = (if \<bar>x\<bar> = \<infinity> then \<infinity> else 0::ereal)"
by (cases x) simp_all
lemma ereal_eq_minus_iff:
@@ -848,9 +1007,7 @@
lemma ereal_le_minus_iff:
fixes x y z :: ereal
- shows "x \<le> z - y \<longleftrightarrow>
- (y = \<infinity> \<longrightarrow> z \<noteq> \<infinity> \<longrightarrow> x = -\<infinity>) \<and>
- (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> x + y \<le> z)"
+ shows "x \<le> z - y \<longleftrightarrow> (y = \<infinity> \<longrightarrow> z \<noteq> \<infinity> \<longrightarrow> x = -\<infinity>) \<and> (\<bar>y\<bar> \<noteq> \<infinity> \<longrightarrow> x + y \<le> z)"
by (cases rule: ereal3_cases[of x y z]) auto
lemma ereal_le_minus:
@@ -860,9 +1017,7 @@
lemma ereal_minus_less_iff:
fixes x y z :: ereal
- shows "x - y < z \<longleftrightarrow>
- y \<noteq> -\<infinity> \<and> (y = \<infinity> \<longrightarrow> x \<noteq> \<infinity> \<and> z \<noteq> -\<infinity>) \<and>
- (y \<noteq> \<infinity> \<longrightarrow> x < z + y)"
+ shows "x - y < z \<longleftrightarrow> y \<noteq> -\<infinity> \<and> (y = \<infinity> \<longrightarrow> x \<noteq> \<infinity> \<and> z \<noteq> -\<infinity>) \<and> (y \<noteq> \<infinity> \<longrightarrow> x < z + y)"
by (cases rule: ereal3_cases[of x y z]) auto
lemma ereal_minus_less:
@@ -917,31 +1072,40 @@
lemma ereal_between:
fixes x e :: ereal
- assumes "\<bar>x\<bar> \<noteq> \<infinity>" "0 < e"
- shows "x - e < x" "x < x + e"
-using assms apply (cases x, cases e) apply auto
-using assms apply (cases x, cases e) apply auto
-done
+ assumes "\<bar>x\<bar> \<noteq> \<infinity>"
+ and "0 < e"
+ shows "x - e < x"
+ and "x < x + e"
+ using assms
+ apply (cases x, cases e)
+ apply auto
+ using assms
+ apply (cases x, cases e)
+ apply auto
+ done
lemma ereal_minus_eq_PInfty_iff:
- fixes x y :: ereal shows "x - y = \<infinity> \<longleftrightarrow> y = -\<infinity> \<or> x = \<infinity>"
+ fixes x y :: ereal
+ shows "x - y = \<infinity> \<longleftrightarrow> y = -\<infinity> \<or> x = \<infinity>"
by (cases x y rule: ereal2_cases) simp_all
+
subsubsection {* Division *}
instantiation ereal :: inverse
begin
function inverse_ereal where
-"inverse (ereal r) = (if r = 0 then \<infinity> else ereal (inverse r))" |
-"inverse (\<infinity>::ereal) = 0" |
-"inverse (-\<infinity>::ereal) = 0"
+ "inverse (ereal r) = (if r = 0 then \<infinity> else ereal (inverse r))"
+| "inverse (\<infinity>::ereal) = 0"
+| "inverse (-\<infinity>::ereal) = 0"
by (auto intro: ereal_cases)
termination by (relation "{}") simp
definition "x / y = x * inverse (y :: ereal)"
instance ..
+
end
lemma real_of_ereal_inverse[simp]:
@@ -959,53 +1123,61 @@
unfolding divide_ereal_def by (auto simp: divide_real_def)
lemma ereal_divide_same[simp]:
- fixes x :: ereal shows "x / x = (if \<bar>x\<bar> = \<infinity> \<or> x = 0 then 0 else 1)"
- by (cases x)
- (simp_all add: divide_real_def divide_ereal_def one_ereal_def)
+ fixes x :: ereal
+ shows "x / x = (if \<bar>x\<bar> = \<infinity> \<or> x = 0 then 0 else 1)"
+ by (cases x) (simp_all add: divide_real_def divide_ereal_def one_ereal_def)
lemma ereal_inv_inv[simp]:
- fixes x :: ereal shows "inverse (inverse x) = (if x \<noteq> -\<infinity> then x else \<infinity>)"
+ fixes x :: ereal
+ shows "inverse (inverse x) = (if x \<noteq> -\<infinity> then x else \<infinity>)"
by (cases x) auto
lemma ereal_inverse_minus[simp]:
- fixes x :: ereal shows "inverse (- x) = (if x = 0 then \<infinity> else -inverse x)"
+ fixes x :: ereal
+ shows "inverse (- x) = (if x = 0 then \<infinity> else -inverse x)"
by (cases x) simp_all
lemma ereal_uminus_divide[simp]:
- fixes x y :: ereal shows "- x / y = - (x / y)"
+ fixes x y :: ereal
+ shows "- x / y = - (x / y)"
unfolding divide_ereal_def by simp
lemma ereal_divide_Infty[simp]:
- fixes x :: ereal shows "x / \<infinity> = 0" "x / -\<infinity> = 0"
+ fixes x :: ereal
+ shows "x / \<infinity> = 0" "x / -\<infinity> = 0"
unfolding divide_ereal_def by simp_all
-lemma ereal_divide_one[simp]:
- "x / 1 = (x::ereal)"
+lemma ereal_divide_one[simp]: "x / 1 = (x::ereal)"
unfolding divide_ereal_def by simp
-lemma ereal_divide_ereal[simp]:
- "\<infinity> / ereal r = (if 0 \<le> r then \<infinity> else -\<infinity>)"
+lemma ereal_divide_ereal[simp]: "\<infinity> / ereal r = (if 0 \<le> r then \<infinity> else -\<infinity>)"
unfolding divide_ereal_def by simp
lemma zero_le_divide_ereal[simp]:
- fixes a :: ereal assumes "0 \<le> a" "0 \<le> b"
+ fixes a :: ereal
+ assumes "0 \<le> a"
+ and "0 \<le> b"
shows "0 \<le> a / b"
using assms by (cases rule: ereal2_cases[of a b]) (auto simp: zero_le_divide_iff)
lemma ereal_le_divide_pos:
- fixes x y z :: ereal shows "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> y \<le> z / x \<longleftrightarrow> x * y \<le> z"
+ fixes x y z :: ereal
+ shows "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> y \<le> z / x \<longleftrightarrow> x * y \<le> z"
by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
lemma ereal_divide_le_pos:
- fixes x y z :: ereal shows "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> z / x \<le> y \<longleftrightarrow> z \<le> x * y"
+ fixes x y z :: ereal
+ shows "x > 0 \<Longrightarrow> x \<noteq> \<infinity> \<Longrightarrow> z / x \<le> y \<longleftrightarrow> z \<le> x * y"
by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
lemma ereal_le_divide_neg:
- fixes x y z :: ereal shows "x < 0 \<Longrightarrow> x \<noteq> -\<infinity> \<Longrightarrow> y \<le> z / x \<longleftrightarrow> z \<le> x * y"
+ fixes x y z :: ereal
+ shows "x < 0 \<Longrightarrow> x \<noteq> -\<infinity> \<Longrightarrow> y \<le> z / x \<longleftrightarrow> z \<le> x * y"
by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
lemma ereal_divide_le_neg:
- fixes x y z :: ereal shows "x < 0 \<Longrightarrow> x \<noteq> -\<infinity> \<Longrightarrow> z / x \<le> y \<longleftrightarrow> x * y \<le> z"
+ fixes x y z :: ereal
+ shows "x < 0 \<Longrightarrow> x \<noteq> -\<infinity> \<Longrightarrow> z / x \<le> y \<longleftrightarrow> x * y \<le> z"
by (cases rule: ereal3_cases[of x y z]) (auto simp: field_simps)
lemma ereal_inverse_antimono_strict:
@@ -1015,31 +1187,37 @@
lemma ereal_inverse_antimono:
fixes x y :: ereal
- shows "0 \<le> x \<Longrightarrow> x <= y \<Longrightarrow> inverse y <= inverse x"
+ shows "0 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> inverse y \<le> inverse x"
by (cases rule: ereal2_cases[of x y]) auto
lemma inverse_inverse_Pinfty_iff[simp]:
- fixes x :: ereal shows "inverse x = \<infinity> \<longleftrightarrow> x = 0"
+ fixes x :: ereal
+ shows "inverse x = \<infinity> \<longleftrightarrow> x = 0"
by (cases x) auto
lemma ereal_inverse_eq_0:
- fixes x :: ereal shows "inverse x = 0 \<longleftrightarrow> x = \<infinity> \<or> x = -\<infinity>"
+ fixes x :: ereal
+ shows "inverse x = 0 \<longleftrightarrow> x = \<infinity> \<or> x = -\<infinity>"
by (cases x) auto
lemma ereal_0_gt_inverse:
- fixes x :: ereal shows "0 < inverse x \<longleftrightarrow> x \<noteq> \<infinity> \<and> 0 \<le> x"
+ fixes x :: ereal
+ shows "0 < inverse x \<longleftrightarrow> x \<noteq> \<infinity> \<and> 0 \<le> x"
by (cases x) auto
lemma ereal_mult_less_right:
fixes a b c :: ereal
- assumes "b * a < c * a" "0 < a" "a < \<infinity>"
+ assumes "b * a < c * a"
+ and "0 < a"
+ and "a < \<infinity>"
shows "b < c"
using assms
by (cases rule: ereal3_cases[of a b c])
(auto split: split_if_asm simp: zero_less_mult_iff zero_le_mult_iff)
lemma ereal_power_divide:
- fixes x y :: ereal shows "y \<noteq> 0 \<Longrightarrow> (x / y) ^ n = x^n / y^n"
+ fixes x y :: ereal
+ shows "y \<noteq> 0 \<Longrightarrow> (x / y) ^ n = x^n / y^n"
by (cases rule: ereal2_cases[of x y])
(auto simp: one_ereal_def zero_ereal_def power_divide not_le
power_less_zero_eq zero_le_power_iff)
@@ -1047,36 +1225,47 @@
lemma ereal_le_mult_one_interval:
fixes x y :: ereal
assumes y: "y \<noteq> -\<infinity>"
- assumes z: "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y"
+ assumes z: "\<And>z. 0 < z \<Longrightarrow> z < 1 \<Longrightarrow> z * x \<le> y"
shows "x \<le> y"
proof (cases x)
- case PInf with z[of "1 / 2"] show "x \<le> y" by (simp add: one_ereal_def)
+ case PInf
+ with z[of "1 / 2"] show "x \<le> y"
+ by (simp add: one_ereal_def)
next
- case (real r) note r = this
+ case (real r)
+ note r = this
show "x \<le> y"
proof (cases y)
- case (real p) note p = this
+ case (real p)
+ note p = this
have "r \<le> p"
proof (rule field_le_mult_one_interval)
- fix z :: real assume "0 < z" and "z < 1"
- with z[of "ereal z"]
- show "z * r \<le> p" using p r by (auto simp: zero_le_mult_iff one_ereal_def)
+ fix z :: real
+ assume "0 < z" and "z < 1"
+ with z[of "ereal z"] show "z * r \<le> p"
+ using p r by (auto simp: zero_le_mult_iff one_ereal_def)
qed
- then show "x \<le> y" using p r by simp
+ then show "x \<le> y"
+ using p r by simp
qed (insert y, simp_all)
qed simp
lemma ereal_divide_right_mono[simp]:
fixes x y z :: ereal
- assumes "x \<le> y" "0 < z" shows "x / z \<le> y / z"
-using assms by (cases x y z rule: ereal3_cases) (auto intro: divide_right_mono)
+ assumes "x \<le> y"
+ and "0 < z"
+ shows "x / z \<le> y / z"
+ using assms by (cases x y z rule: ereal3_cases) (auto intro: divide_right_mono)
lemma ereal_divide_left_mono[simp]:
fixes x y z :: ereal
- assumes "y \<le> x" "0 < z" "0 < x * y"
+ assumes "y \<le> x"
+ and "0 < z"
+ and "0 < x * y"
shows "z / x \<le> z / y"
-using assms by (cases x y z rule: ereal3_cases)
- (auto intro: divide_left_mono simp: field_simps sign_simps split: split_if_asm)
+ using assms
+ by (cases x y z rule: ereal3_cases)
+ (auto intro: divide_left_mono simp: field_simps sign_simps split: split_if_asm)
lemma ereal_divide_zero_left[simp]:
fixes a :: ereal
@@ -1088,13 +1277,16 @@
shows "b / c * a = b * a / c"
by (cases a b c rule: ereal3_cases) (auto simp: field_simps sign_simps)
+
subsection "Complete lattice"
instantiation ereal :: lattice
begin
+
definition [simp]: "sup x y = (max x y :: ereal)"
definition [simp]: "inf x y = (min x y :: ereal)"
instance by default simp_all
+
end
instantiation ereal :: complete_lattice
@@ -1109,29 +1301,46 @@
lemma ereal_complete_Sup:
fixes S :: "ereal set"
shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) \<and> (\<forall>z. (\<forall>y\<in>S. y \<le> z) \<longrightarrow> x \<le> z)"
-proof cases
- assume "\<exists>x. \<forall>a\<in>S. a \<le> ereal x"
- then obtain y where y: "\<And>a. a\<in>S \<Longrightarrow> a \<le> ereal y" by auto
- then have "\<infinity> \<notin> S" by force
+proof (cases "\<exists>x. \<forall>a\<in>S. a \<le> ereal x")
+ case True
+ then obtain y where y: "\<And>a. a\<in>S \<Longrightarrow> a \<le> ereal y"
+ by auto
+ then have "\<infinity> \<notin> S"
+ by force
show ?thesis
- proof cases
- assume "S \<noteq> {-\<infinity>} \<and> S \<noteq> {}"
- with `\<infinity> \<notin> S` obtain x where x: "x \<in> S" "\<bar>x\<bar> \<noteq> \<infinity>" by auto
+ proof (cases "S \<noteq> {-\<infinity>} \<and> S \<noteq> {}")
+ case True
+ with `\<infinity> \<notin> S` obtain x where x: "x \<in> S" "\<bar>x\<bar> \<noteq> \<infinity>"
+ by auto
obtain s where s: "\<forall>x\<in>ereal -` S. x \<le> s" "\<And>z. (\<forall>x\<in>ereal -` S. x \<le> z) \<Longrightarrow> s \<le> z"
proof (atomize_elim, rule complete_real)
- show "\<exists>x. x \<in> ereal -` S" using x by auto
- show "\<exists>z. \<forall>x\<in>ereal -` S. x \<le> z" by (auto dest: y intro!: exI[of _ y])
+ show "\<exists>x. x \<in> ereal -` S"
+ using x by auto
+ show "\<exists>z. \<forall>x\<in>ereal -` S. x \<le> z"
+ by (auto dest: y intro!: exI[of _ y])
qed
show ?thesis
proof (safe intro!: exI[of _ "ereal s"])
- fix y assume "y \<in> S" with s `\<infinity> \<notin> S` show "y \<le> ereal s"
+ fix y
+ assume "y \<in> S"
+ with s `\<infinity> \<notin> S` show "y \<le> ereal s"
by (cases y) auto
next
- fix z assume "\<forall>y\<in>S. y \<le> z" with `S \<noteq> {-\<infinity>} \<and> S \<noteq> {}` show "ereal s \<le> z"
+ fix z
+ assume "\<forall>y\<in>S. y \<le> z"
+ with `S \<noteq> {-\<infinity>} \<and> S \<noteq> {}` show "ereal s \<le> z"
by (cases z) (auto intro!: s)
qed
- qed (auto intro!: exI[of _ "-\<infinity>"])
-qed (fastforce intro!: exI[of _ \<infinity>] ereal_top intro: order_trans dest: less_imp_le simp: not_le)
+ next
+ case False
+ then show ?thesis
+ by (auto intro!: exI[of _ "-\<infinity>"])
+ qed
+next
+ case False
+ then show ?thesis
+ by (fastforce intro!: exI[of _ \<infinity>] ereal_top intro: order_trans dest: less_imp_le simp: not_le)
+qed
lemma ereal_complete_uminus_eq:
fixes S :: "ereal set"
@@ -1141,23 +1350,24 @@
lemma ereal_complete_Inf:
"\<exists>x. (\<forall>y\<in>S::ereal set. x \<le> y) \<and> (\<forall>z. (\<forall>y\<in>S. z \<le> y) \<longrightarrow> z \<le> x)"
- using ereal_complete_Sup[of "uminus ` S"] unfolding ereal_complete_uminus_eq by auto
+ using ereal_complete_Sup[of "uminus ` S"]
+ unfolding ereal_complete_uminus_eq
+ by auto
instance
proof
show "Sup {} = (bot::ereal)"
- apply (auto simp: bot_ereal_def Sup_ereal_def)
- apply (rule some1_equality)
- apply (metis ereal_bot ereal_less_eq(2))
- apply (metis ereal_less_eq(2))
- done
-next
+ apply (auto simp: bot_ereal_def Sup_ereal_def)
+ apply (rule some1_equality)
+ apply (metis ereal_bot ereal_less_eq(2))
+ apply (metis ereal_less_eq(2))
+ done
show "Inf {} = (top::ereal)"
- apply (auto simp: top_ereal_def Inf_ereal_def)
- apply (rule some1_equality)
- apply (metis ereal_top ereal_less_eq(1))
- apply (metis ereal_less_eq(1))
- done
+ apply (auto simp: top_ereal_def Inf_ereal_def)
+ apply (rule some1_equality)
+ apply (metis ereal_top ereal_less_eq(1))
+ apply (metis ereal_less_eq(1))
+ done
qed (auto intro: someI2_ex ereal_complete_Sup ereal_complete_Inf
simp: Sup_ereal_def Inf_ereal_def bot_ereal_def top_ereal_def)
@@ -1183,74 +1393,89 @@
using ereal_Sup_uminus_image_eq[of "uminus ` S"] by simp
lemma ereal_SUPR_uminus:
- fixes f :: "'a => ereal"
+ fixes f :: "'a \<Rightarrow> ereal"
shows "(SUP i : R. -(f i)) = -(INF i : R. f i)"
using ereal_Sup_uminus_image_eq[of "f`R"]
by (simp add: SUP_def INF_def image_image)
lemma ereal_INFI_uminus:
- fixes f :: "'a => ereal"
- shows "(INF i : R. -(f i)) = -(SUP i : R. f i)"
+ fixes f :: "'a \<Rightarrow> ereal"
+ shows "(INF i : R. - f i) = - (SUP i : R. f i)"
using ereal_SUPR_uminus[of _ "\<lambda>x. - f x"] by simp
lemma ereal_image_uminus_shift:
- fixes X Y :: "ereal set" shows "uminus ` X = Y \<longleftrightarrow> X = uminus ` Y"
+ fixes X Y :: "ereal set"
+ shows "uminus ` X = Y \<longleftrightarrow> X = uminus ` Y"
proof
assume "uminus ` X = Y"
then have "uminus ` uminus ` X = uminus ` Y"
by (simp add: inj_image_eq_iff)
- then show "X = uminus ` Y" by (simp add: image_image)
+ then show "X = uminus ` Y"
+ by (simp add: image_image)
qed (simp add: image_image)
lemma Inf_ereal_iff:
fixes z :: ereal
- shows "(!!x. x:X ==> z <= x) ==> (EX x:X. x<y) <-> Inf X < y"
- by (metis complete_lattice_class.Inf_greatest complete_lattice_class.Inf_lower less_le_not_le linear
- order_less_le_trans)
+ shows "(\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> (\<exists>x\<in>X. x < y) \<longleftrightarrow> Inf X < y"
+ by (metis complete_lattice_class.Inf_greatest complete_lattice_class.Inf_lower
+ less_le_not_le linear order_less_le_trans)
lemma Sup_eq_MInfty:
- fixes S :: "ereal set" shows "Sup S = -\<infinity> \<longleftrightarrow> S = {} \<or> S = {-\<infinity>}"
+ fixes S :: "ereal set"
+ shows "Sup S = -\<infinity> \<longleftrightarrow> S = {} \<or> S = {-\<infinity>}"
unfolding bot_ereal_def[symmetric] by auto
lemma Inf_eq_PInfty:
- fixes S :: "ereal set" shows "Inf S = \<infinity> \<longleftrightarrow> S = {} \<or> S = {\<infinity>}"
+ fixes S :: "ereal set"
+ shows "Inf S = \<infinity> \<longleftrightarrow> S = {} \<or> S = {\<infinity>}"
using Sup_eq_MInfty[of "uminus`S"]
unfolding ereal_Sup_uminus_image_eq ereal_image_uminus_shift by simp
-lemma Inf_eq_MInfty:
- fixes S :: "ereal set" shows "-\<infinity> \<in> S \<Longrightarrow> Inf S = -\<infinity>"
+lemma Inf_eq_MInfty:
+ fixes S :: "ereal set"
+ shows "-\<infinity> \<in> S \<Longrightarrow> Inf S = -\<infinity>"
unfolding bot_ereal_def[symmetric] by auto
lemma Sup_eq_PInfty:
- fixes S :: "ereal set" shows "\<infinity> \<in> S \<Longrightarrow> Sup S = \<infinity>"
+ fixes S :: "ereal set"
+ shows "\<infinity> \<in> S \<Longrightarrow> Sup S = \<infinity>"
unfolding top_ereal_def[symmetric] by auto
lemma Sup_ereal_close:
fixes e :: ereal
- assumes "0 < e" and S: "\<bar>Sup S\<bar> \<noteq> \<infinity>" "S \<noteq> {}"
+ assumes "0 < e"
+ and S: "\<bar>Sup S\<bar> \<noteq> \<infinity>" "S \<noteq> {}"
shows "\<exists>x\<in>S. Sup S - e < x"
using assms by (cases e) (auto intro!: less_Sup_iff[THEN iffD1])
lemma Inf_ereal_close:
- fixes e :: ereal assumes "\<bar>Inf X\<bar> \<noteq> \<infinity>" "0 < e"
+ fixes e :: ereal
+ assumes "\<bar>Inf X\<bar> \<noteq> \<infinity>"
+ and "0 < e"
shows "\<exists>x\<in>X. x < Inf X + e"
proof (rule Inf_less_iff[THEN iffD1])
- show "Inf X < Inf X + e" using assms
- by (cases e) auto
+ show "Inf X < Inf X + e"
+ using assms by (cases e) auto
qed
lemma SUP_nat_Infty: "(SUP i::nat. ereal (real i)) = \<infinity>"
proof -
- { fix x ::ereal assume "x \<noteq> \<infinity>"
+ {
+ fix x :: ereal
+ assume "x \<noteq> \<infinity>"
then have "\<exists>k::nat. x < ereal (real k)"
proof (cases x)
- case MInf then show ?thesis by (intro exI[of _ 0]) auto
+ case MInf
+ then show ?thesis
+ by (intro exI[of _ 0]) auto
next
case (real r)
moreover obtain k :: nat where "r < real k"
using ex_less_of_nat by (auto simp: real_eq_of_nat)
- ultimately show ?thesis by auto
- qed simp }
+ ultimately show ?thesis
+ by auto
+ qed simp
+ }
then show ?thesis
using SUP_eq_top_iff[of UNIV "\<lambda>n::nat. ereal (real n)"]
by (auto simp: top_ereal_def)
@@ -1259,96 +1484,136 @@
lemma Inf_less:
fixes x :: ereal
assumes "(INF i:A. f i) < x"
- shows "EX i. i : A & f i <= x"
-proof(rule ccontr)
- assume "~ (EX i. i : A & f i <= x)"
- hence "ALL i:A. f i > x" by auto
- hence "(INF i:A. f i) >= x" apply (subst INF_greatest) by auto
- thus False using assms by auto
+ shows "\<exists>i. i \<in> A \<and> f i \<le> x"
+proof (rule ccontr)
+ assume "\<not> ?thesis"
+ then have "\<forall>i\<in>A. f i > x"
+ by auto
+ then have "(INF i:A. f i) \<ge> x"
+ by (subst INF_greatest) auto
+ then show False
+ using assms by auto
qed
lemma SUP_ereal_le_addI:
fixes f :: "'i \<Rightarrow> ereal"
- assumes "\<And>i. f i + y \<le> z" and "y \<noteq> -\<infinity>"
+ assumes "\<And>i. f i + y \<le> z"
+ and "y \<noteq> -\<infinity>"
shows "SUPR UNIV f + y \<le> z"
proof (cases y)
case (real r)
- then have "\<And>i. f i \<le> z - y" using assms by (simp add: ereal_le_minus_iff)
- then have "SUPR UNIV f \<le> z - y" by (rule SUP_least)
- then show ?thesis using real by (simp add: ereal_le_minus_iff)
+ then have "\<And>i. f i \<le> z - y"
+ using assms by (simp add: ereal_le_minus_iff)
+ then have "SUPR UNIV f \<le> z - y"
+ by (rule SUP_least)
+ then show ?thesis
+ using real by (simp add: ereal_le_minus_iff)
qed (insert assms, auto)
lemma SUPR_ereal_add:
fixes f g :: "nat \<Rightarrow> ereal"
- assumes "incseq f" "incseq g" and pos: "\<And>i. f i \<noteq> -\<infinity>" "\<And>i. g i \<noteq> -\<infinity>"
+ assumes "incseq f"
+ and "incseq g"
+ and pos: "\<And>i. f i \<noteq> -\<infinity>" "\<And>i. g i \<noteq> -\<infinity>"
shows "(SUP i. f i + g i) = SUPR UNIV f + SUPR UNIV g"
proof (rule SUP_eqI)
- fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> f i + g i \<le> y"
- have f: "SUPR UNIV f \<noteq> -\<infinity>" using pos
- unfolding SUP_def Sup_eq_MInfty by (auto dest: image_eqD)
- { fix j
- { fix i
+ fix y
+ assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> f i + g i \<le> y"
+ have f: "SUPR UNIV f \<noteq> -\<infinity>"
+ using pos
+ unfolding SUP_def Sup_eq_MInfty
+ by (auto dest: image_eqD)
+ {
+ fix j
+ {
+ fix i
have "f i + g j \<le> f i + g (max i j)"
- using `incseq g`[THEN incseqD] by (rule add_left_mono) auto
+ using `incseq g`[THEN incseqD]
+ by (rule add_left_mono) auto
also have "\<dots> \<le> f (max i j) + g (max i j)"
- using `incseq f`[THEN incseqD] by (rule add_right_mono) auto
+ using `incseq f`[THEN incseqD]
+ by (rule add_right_mono) auto
also have "\<dots> \<le> y" using * by auto
- finally have "f i + g j \<le> y" . }
+ finally have "f i + g j \<le> y" .
+ }
then have "SUPR UNIV f + g j \<le> y"
using assms(4)[of j] by (intro SUP_ereal_le_addI) auto
- then have "g j + SUPR UNIV f \<le> y" by (simp add: ac_simps) }
+ then have "g j + SUPR UNIV f \<le> y" by (simp add: ac_simps)
+ }
then have "SUPR UNIV g + SUPR UNIV f \<le> y"
using f by (rule SUP_ereal_le_addI)
- then show "SUPR UNIV f + SUPR UNIV g \<le> y" by (simp add: ac_simps)
+ then show "SUPR UNIV f + SUPR UNIV g \<le> y"
+ by (simp add: ac_simps)
qed (auto intro!: add_mono SUP_upper)
lemma SUPR_ereal_add_pos:
fixes f g :: "nat \<Rightarrow> ereal"
- assumes inc: "incseq f" "incseq g" and pos: "\<And>i. 0 \<le> f i" "\<And>i. 0 \<le> g i"
+ assumes inc: "incseq f" "incseq g"
+ and pos: "\<And>i. 0 \<le> f i" "\<And>i. 0 \<le> g i"
shows "(SUP i. f i + g i) = SUPR UNIV f + SUPR UNIV g"
proof (intro SUPR_ereal_add inc)
- fix i show "f i \<noteq> -\<infinity>" "g i \<noteq> -\<infinity>" using pos[of i] by auto
+ fix i
+ show "f i \<noteq> -\<infinity>" "g i \<noteq> -\<infinity>"
+ using pos[of i] by auto
qed
lemma SUPR_ereal_setsum:
fixes f g :: "'a \<Rightarrow> nat \<Rightarrow> ereal"
- assumes "\<And>n. n \<in> A \<Longrightarrow> incseq (f n)" and pos: "\<And>n i. n \<in> A \<Longrightarrow> 0 \<le> f n i"
+ assumes "\<And>n. n \<in> A \<Longrightarrow> incseq (f n)"
+ and pos: "\<And>n i. n \<in> A \<Longrightarrow> 0 \<le> f n i"
shows "(SUP i. \<Sum>n\<in>A. f n i) = (\<Sum>n\<in>A. SUPR UNIV (f n))"
-proof cases
- assume "finite A" then show ?thesis using assms
+proof (cases "finite A")
+ case True
+ then show ?thesis using assms
by induct (auto simp: incseq_setsumI2 setsum_nonneg SUPR_ereal_add_pos)
-qed simp
+next
+ case False
+ then show ?thesis by simp
+qed
lemma SUPR_ereal_cmult:
- fixes f :: "nat \<Rightarrow> ereal" assumes "\<And>i. 0 \<le> f i" "0 \<le> c"
+ fixes f :: "nat \<Rightarrow> ereal"
+ assumes "\<And>i. 0 \<le> f i"
+ and "0 \<le> c"
shows "(SUP i. c * f i) = c * SUPR UNIV f"
proof (rule SUP_eqI)
- fix i have "f i \<le> SUPR UNIV f" by (rule SUP_upper) auto
+ fix i
+ have "f i \<le> SUPR UNIV f"
+ by (rule SUP_upper) auto
then show "c * f i \<le> c * SUPR UNIV f"
using `0 \<le> c` by (rule ereal_mult_left_mono)
next
- fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> c * f i \<le> y"
+ fix y
+ assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> c * f i \<le> y"
show "c * SUPR UNIV f \<le> y"
- proof cases
- assume c: "0 < c \<and> c \<noteq> \<infinity>"
+ proof (cases "0 < c \<and> c \<noteq> \<infinity>")
+ case True
with * have "SUPR UNIV f \<le> y / c"
by (intro SUP_least) (auto simp: ereal_le_divide_pos)
- with c show ?thesis
+ with True show ?thesis
by (auto simp: ereal_le_divide_pos)
next
- { assume "c = \<infinity>" have ?thesis
- proof cases
- assume **: "\<forall>i. f i = 0"
- then have "range f = {0}" by auto
- with ** show "c * SUPR UNIV f \<le> y" using *
- by (auto simp: SUP_def min_max.sup_absorb1)
+ case False
+ {
+ assume "c = \<infinity>"
+ have ?thesis
+ proof (cases "\<forall>i. f i = 0")
+ case True
+ then have "range f = {0}"
+ by auto
+ with True show "c * SUPR UNIV f \<le> y"
+ using * by (auto simp: SUP_def min_max.sup_absorb1)
next
- assume "\<not> (\<forall>i. f i = 0)"
- then obtain i where "f i \<noteq> 0" by auto
- with *[of i] `c = \<infinity>` `0 \<le> f i` show ?thesis by (auto split: split_if_asm)
- qed }
- moreover assume "\<not> (0 < c \<and> c \<noteq> \<infinity>)"
- ultimately show ?thesis using * `0 \<le> c` by auto
+ case False
+ then obtain i where "f i \<noteq> 0"
+ by auto
+ with *[of i] `c = \<infinity>` `0 \<le> f i` show ?thesis
+ by (auto split: split_if_asm)
+ qed
+ }
+ moreover note False
+ ultimately show ?thesis
+ using * `0 \<le> c` by auto
qed
qed
@@ -1359,15 +1624,21 @@
unfolding SUP_def Sup_eq_top_iff[where 'a=ereal, unfolded top_ereal_def]
apply simp
proof safe
- fix x :: ereal assume "x \<noteq> \<infinity>"
+ fix x :: ereal
+ assume "x \<noteq> \<infinity>"
show "\<exists>i\<in>A. x < f i"
proof (cases x)
- case PInf with `x \<noteq> \<infinity>` show ?thesis by simp
+ case PInf
+ with `x \<noteq> \<infinity>` show ?thesis
+ by simp
next
- case MInf with assms[of "0"] show ?thesis by force
+ case MInf
+ with assms[of "0"] show ?thesis
+ by force
next
case (real r)
- with less_PInf_Ex_of_nat[of x] obtain n :: nat where "x < ereal (real n)" by auto
+ with less_PInf_Ex_of_nat[of x] obtain n :: nat where "x < ereal (real n)"
+ by auto
moreover obtain i where "i \<in> A" "ereal (real n) \<le> f i"
using assms ..
ultimately show ?thesis
@@ -1382,7 +1653,8 @@
case (real r)
have "\<forall>n::nat. \<exists>x. x \<in> A \<and> Sup A < x + 1 / ereal (real n)"
proof
- fix n ::nat have "\<exists>x\<in>A. Sup A - 1 / ereal (real n) < x"
+ fix n :: nat
+ have "\<exists>x\<in>A. Sup A - 1 / ereal (real n) < x"
using assms real by (intro Sup_ereal_close) (auto simp: one_ereal_def)
then obtain x where "x \<in> A" "Sup A - 1 / ereal (real n) < x" ..
then show "\<exists>x. x \<in> A \<and> Sup A < x + 1 / ereal (real n)"
@@ -1392,48 +1664,63 @@
where f: "\<forall>x. f x \<in> A \<and> Sup A < f x + 1 / ereal (real x)" ..
have "SUPR UNIV f = Sup A"
proof (rule SUP_eqI)
- fix i show "f i \<le> Sup A" using f
- by (auto intro!: complete_lattice_class.Sup_upper)
+ fix i
+ show "f i \<le> Sup A"
+ using f by (auto intro!: complete_lattice_class.Sup_upper)
next
- fix y assume bound: "\<And>i. i \<in> UNIV \<Longrightarrow> f i \<le> y"
+ fix y
+ assume bound: "\<And>i. i \<in> UNIV \<Longrightarrow> f i \<le> y"
show "Sup A \<le> y"
proof (rule ereal_le_epsilon, intro allI impI)
- fix e :: ereal assume "0 < e"
+ fix e :: ereal
+ assume "0 < e"
show "Sup A \<le> y + e"
proof (cases e)
case (real r)
- hence "0 < r" using `0 < e` by auto
- then obtain n ::nat where *: "1 / real n < r" "0 < n"
- using ex_inverse_of_nat_less by (auto simp: real_eq_of_nat inverse_eq_divide)
- have "Sup A \<le> f n + 1 / ereal (real n)" using f[THEN spec, of n]
+ then have "0 < r"
+ using `0 < e` by auto
+ then obtain n :: nat where *: "1 / real n < r" "0 < n"
+ using ex_inverse_of_nat_less
+ by (auto simp: real_eq_of_nat inverse_eq_divide)
+ have "Sup A \<le> f n + 1 / ereal (real n)"
+ using f[THEN spec, of n]
by auto
- also have "1 / ereal (real n) \<le> e" using real * by (auto simp: one_ereal_def )
- with bound have "f n + 1 / ereal (real n) \<le> y + e" by (rule add_mono) simp
+ also have "1 / ereal (real n) \<le> e"
+ using real *
+ by (auto simp: one_ereal_def )
+ with bound have "f n + 1 / ereal (real n) \<le> y + e"
+ by (rule add_mono) simp
finally show "Sup A \<le> y + e" .
qed (insert `0 < e`, auto)
qed
qed
- with f show ?thesis by (auto intro!: exI[of _ f])
+ with f show ?thesis
+ by (auto intro!: exI[of _ f])
next
case PInf
- from `A \<noteq> {}` obtain x where "x \<in> A" by auto
+ from `A \<noteq> {}` obtain x where "x \<in> A"
+ by auto
show ?thesis
- proof cases
- assume *: "\<infinity> \<in> A"
- then have "\<infinity> \<le> Sup A" by (intro complete_lattice_class.Sup_upper)
- with * show ?thesis by (auto intro!: exI[of _ "\<lambda>x. \<infinity>"])
+ proof (cases "\<infinity> \<in> A")
+ case True
+ then have "\<infinity> \<le> Sup A"
+ by (intro complete_lattice_class.Sup_upper)
+ with True show ?thesis
+ by (auto intro!: exI[of _ "\<lambda>x. \<infinity>"])
next
- assume "\<infinity> \<notin> A"
+ case False
have "\<exists>x\<in>A. 0 \<le> x"
- by (metis Infty_neq_0 PInf complete_lattice_class.Sup_least ereal_infty_less_eq2 linorder_linear)
- then obtain x where "x \<in> A" "0 \<le> x" by auto
+ by (metis Infty_neq_0 PInf complete_lattice_class.Sup_least
+ ereal_infty_less_eq2 linorder_linear)
+ then obtain x where "x \<in> A" and "0 \<le> x"
+ by auto
have "\<forall>n::nat. \<exists>f. f \<in> A \<and> x + ereal (real n) \<le> f"
proof (rule ccontr)
assume "\<not> ?thesis"
then have "\<exists>n::nat. Sup A \<le> x + ereal (real n)"
by (simp add: Sup_le_iff not_le less_imp_le Ball_def) (metis less_imp_le)
then show False using `x \<in> A` `\<infinity> \<notin> A` PInf
- by(cases x) auto
+ by (cases x) auto
qed
from choice[OF this] obtain f :: "nat \<Rightarrow> ereal"
where f: "\<forall>z. f z \<in> A \<and> x + ereal (real z) \<le> f z" ..
@@ -1444,20 +1731,26 @@
using f[THEN spec, of n] `0 \<le> x`
by (cases rule: ereal2_cases[of "f n" x]) (auto intro!: exI[of _ n])
qed
- then show ?thesis using f PInf by (auto intro!: exI[of _ f])
+ then show ?thesis
+ using f PInf by (auto intro!: exI[of _ f])
qed
next
case MInf
- with `A \<noteq> {}` have "A = {-\<infinity>}" by (auto simp: Sup_eq_MInfty)
- then show ?thesis using MInf by (auto intro!: exI[of _ "\<lambda>x. -\<infinity>"])
+ with `A \<noteq> {}` have "A = {-\<infinity>}"
+ by (auto simp: Sup_eq_MInfty)
+ then show ?thesis
+ using MInf by (auto intro!: exI[of _ "\<lambda>x. -\<infinity>"])
qed
lemma SUPR_countable_SUPR:
"A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> g`A \<and> SUPR A g = SUPR UNIV f"
- using Sup_countable_SUPR[of "g`A"] by (auto simp: SUP_def)
+ using Sup_countable_SUPR[of "g`A"]
+ by (auto simp: SUP_def)
lemma Sup_ereal_cadd:
- fixes A :: "ereal set" assumes "A \<noteq> {}" and "a \<noteq> -\<infinity>"
+ fixes A :: "ereal set"
+ assumes "A \<noteq> {}"
+ and "a \<noteq> -\<infinity>"
shows "Sup ((\<lambda>x. a + x) ` A) = a + Sup A"
proof (rule antisym)
have *: "\<And>a::ereal. \<And>A. Sup ((\<lambda>x. a + x) ` A) \<le> a + Sup A"
@@ -1465,37 +1758,46 @@
then show "Sup ((\<lambda>x. a + x) ` A) \<le> a + Sup A" .
show "a + Sup A \<le> Sup ((\<lambda>x. a + x) ` A)"
proof (cases a)
- case PInf with `A \<noteq> {}` show ?thesis by (auto simp: image_constant min_max.sup_absorb1)
+ case PInf with `A \<noteq> {}`
+ show ?thesis
+ by (auto simp: image_constant min_max.sup_absorb1)
next
case (real r)
then have **: "op + (- a) ` op + a ` A = A"
by (auto simp: image_iff ac_simps zero_ereal_def[symmetric])
- from *[of "-a" "(\<lambda>x. a + x) ` A"] real show ?thesis unfolding **
+ from *[of "-a" "(\<lambda>x. a + x) ` A"] real show ?thesis
+ unfolding **
by (cases rule: ereal2_cases[of "Sup A" "Sup (op + a ` A)"]) auto
qed (insert `a \<noteq> -\<infinity>`, auto)
qed
lemma Sup_ereal_cminus:
- fixes A :: "ereal set" assumes "A \<noteq> {}" and "a \<noteq> -\<infinity>"
+ fixes A :: "ereal set"
+ assumes "A \<noteq> {}"
+ and "a \<noteq> -\<infinity>"
shows "Sup ((\<lambda>x. a - x) ` A) = a - Inf A"
using Sup_ereal_cadd[of "uminus ` A" a] assms
- by (simp add: comp_def image_image minus_ereal_def
- ereal_Sup_uminus_image_eq)
+ by (simp add: comp_def image_image minus_ereal_def ereal_Sup_uminus_image_eq)
lemma SUPR_ereal_cminus:
fixes f :: "'i \<Rightarrow> ereal"
- fixes A assumes "A \<noteq> {}" and "a \<noteq> -\<infinity>"
+ fixes A
+ assumes "A \<noteq> {}"
+ and "a \<noteq> -\<infinity>"
shows "(SUP x:A. a - f x) = a - (INF x:A. f x)"
using Sup_ereal_cminus[of "f`A" a] assms
unfolding SUP_def INF_def image_image by auto
lemma Inf_ereal_cminus:
- fixes A :: "ereal set" assumes "A \<noteq> {}" and "\<bar>a\<bar> \<noteq> \<infinity>"
+ fixes A :: "ereal set"
+ assumes "A \<noteq> {}"
+ and "\<bar>a\<bar> \<noteq> \<infinity>"
shows "Inf ((\<lambda>x. a - x) ` A) = a - Sup A"
proof -
{
fix x
- have "-a - -x = -(a - x)" using assms by (cases x) auto
+ have "-a - -x = -(a - x)"
+ using assms by (cases x) auto
} note * = this
then have "(\<lambda>x. -a - x)`uminus`A = uminus ` (\<lambda>x. a - x) ` A"
by (auto simp: image_image)
@@ -1505,25 +1807,32 @@
qed
lemma INFI_ereal_cminus:
- fixes a :: ereal assumes "A \<noteq> {}" and "\<bar>a\<bar> \<noteq> \<infinity>"
+ fixes a :: ereal
+ assumes "A \<noteq> {}"
+ and "\<bar>a\<bar> \<noteq> \<infinity>"
shows "(INF x:A. a - f x) = a - (SUP x:A. f x)"
using Inf_ereal_cminus[of "f`A" a] assms
unfolding SUP_def INF_def image_image
by auto
lemma uminus_ereal_add_uminus_uminus:
- fixes a b :: ereal shows "a \<noteq> \<infinity> \<Longrightarrow> b \<noteq> \<infinity> \<Longrightarrow> - (- a + - b) = a + b"
+ fixes a b :: ereal
+ shows "a \<noteq> \<infinity> \<Longrightarrow> b \<noteq> \<infinity> \<Longrightarrow> - (- a + - b) = a + b"
by (cases rule: ereal2_cases[of a b]) auto
lemma INFI_ereal_add:
fixes f :: "nat \<Rightarrow> ereal"
- assumes "decseq f" "decseq g" and fin: "\<And>i. f i \<noteq> \<infinity>" "\<And>i. g i \<noteq> \<infinity>"
+ assumes "decseq f" "decseq g"
+ and fin: "\<And>i. f i \<noteq> \<infinity>" "\<And>i. g i \<noteq> \<infinity>"
shows "(INF i. f i + g i) = INFI UNIV f + INFI UNIV g"
proof -
have INF_less: "(INF i. f i) < \<infinity>" "(INF i. g i) < \<infinity>"
using assms unfolding INF_less_iff by auto
- { fix i from fin[of i] have "- ((- f i) + (- g i)) = f i + g i"
- by (rule uminus_ereal_add_uminus_uminus) }
+ {
+ fix i
+ from fin[of i] have "- ((- f i) + (- g i)) = f i + g i"
+ by (rule uminus_ereal_add_uminus_uminus)
+ }
then have "(INF i. f i + g i) = (INF i. - ((- f i) + (- g i)))"
by simp
also have "\<dots> = INFI UNIV f + INFI UNIV g"
@@ -1534,6 +1843,7 @@
finally show ?thesis .
qed
+
subsection "Relation to @{typ enat}"
definition "ereal_of_enat n = (case n of enat n \<Rightarrow> ereal (real n) | \<infinity> \<Rightarrow> \<infinity>)"
@@ -1546,50 +1856,41 @@
"ereal_of_enat \<infinity> = \<infinity>"
by (simp_all add: ereal_of_enat_def)
-lemma ereal_of_enat_le_iff[simp]:
- "ereal_of_enat m \<le> ereal_of_enat n \<longleftrightarrow> m \<le> n"
-by (cases m n rule: enat2_cases) auto
+lemma ereal_of_enat_le_iff[simp]: "ereal_of_enat m \<le> ereal_of_enat n \<longleftrightarrow> m \<le> n"
+ by (cases m n rule: enat2_cases) auto
-lemma ereal_of_enat_less_iff[simp]:
- "ereal_of_enat m < ereal_of_enat n \<longleftrightarrow> m < n"
-by (cases m n rule: enat2_cases) auto
+lemma ereal_of_enat_less_iff[simp]: "ereal_of_enat m < ereal_of_enat n \<longleftrightarrow> m < n"
+ by (cases m n rule: enat2_cases) auto
-lemma numeral_le_ereal_of_enat_iff[simp]:
- shows "numeral m \<le> ereal_of_enat n \<longleftrightarrow> numeral m \<le> n"
-by (cases n) (auto dest: natceiling_le intro: natceiling_le_eq[THEN iffD1])
+lemma numeral_le_ereal_of_enat_iff[simp]: "numeral m \<le> ereal_of_enat n \<longleftrightarrow> numeral m \<le> n"
+ by (cases n) (auto dest: natceiling_le intro: natceiling_le_eq[THEN iffD1])
-lemma numeral_less_ereal_of_enat_iff[simp]:
- shows "numeral m < ereal_of_enat n \<longleftrightarrow> numeral m < n"
-by (cases n) (auto simp: real_of_nat_less_iff[symmetric])
+lemma numeral_less_ereal_of_enat_iff[simp]: "numeral m < ereal_of_enat n \<longleftrightarrow> numeral m < n"
+ by (cases n) (auto simp: real_of_nat_less_iff[symmetric])
-lemma ereal_of_enat_ge_zero_cancel_iff[simp]:
- "0 \<le> ereal_of_enat n \<longleftrightarrow> 0 \<le> n"
-by (cases n) (auto simp: enat_0[symmetric])
+lemma ereal_of_enat_ge_zero_cancel_iff[simp]: "0 \<le> ereal_of_enat n \<longleftrightarrow> 0 \<le> n"
+ by (cases n) (auto simp: enat_0[symmetric])
-lemma ereal_of_enat_gt_zero_cancel_iff[simp]:
- "0 < ereal_of_enat n \<longleftrightarrow> 0 < n"
-by (cases n) (auto simp: enat_0[symmetric])
+lemma ereal_of_enat_gt_zero_cancel_iff[simp]: "0 < ereal_of_enat n \<longleftrightarrow> 0 < n"
+ by (cases n) (auto simp: enat_0[symmetric])
-lemma ereal_of_enat_zero[simp]:
- "ereal_of_enat 0 = 0"
-by (auto simp: enat_0[symmetric])
+lemma ereal_of_enat_zero[simp]: "ereal_of_enat 0 = 0"
+ by (auto simp: enat_0[symmetric])
-lemma ereal_of_enat_inf[simp]:
- "ereal_of_enat n = \<infinity> \<longleftrightarrow> n = \<infinity>"
+lemma ereal_of_enat_inf[simp]: "ereal_of_enat n = \<infinity> \<longleftrightarrow> n = \<infinity>"
by (cases n) auto
-
-lemma ereal_of_enat_add:
- "ereal_of_enat (m + n) = ereal_of_enat m + ereal_of_enat n"
-by (cases m n rule: enat2_cases) auto
+lemma ereal_of_enat_add: "ereal_of_enat (m + n) = ereal_of_enat m + ereal_of_enat n"
+ by (cases m n rule: enat2_cases) auto
lemma ereal_of_enat_sub:
- assumes "n \<le> m" shows "ereal_of_enat (m - n) = ereal_of_enat m - ereal_of_enat n "
-using assms by (cases m n rule: enat2_cases) auto
+ assumes "n \<le> m"
+ shows "ereal_of_enat (m - n) = ereal_of_enat m - ereal_of_enat n "
+ using assms by (cases m n rule: enat2_cases) auto
lemma ereal_of_enat_mult:
"ereal_of_enat (m * n) = ereal_of_enat m * ereal_of_enat n"
-by (cases m n rule: enat2_cases) auto
+ by (cases m n rule: enat2_cases) auto
lemmas ereal_of_enat_pushin = ereal_of_enat_add ereal_of_enat_sub ereal_of_enat_mult
lemmas ereal_of_enat_pushout = ereal_of_enat_pushin[symmetric]
@@ -1607,6 +1908,7 @@
instance
by default (simp add: open_ereal_generated)
+
end
lemma open_PInfty: "open A \<Longrightarrow> \<infinity> \<in> A \<Longrightarrow> (\<exists>x. {ereal x<..} \<subseteq> A)"
@@ -1618,8 +1920,13 @@
with Int show ?case
by (intro exI[of _ "max x z"]) fastforce
next
- { fix x have "x \<noteq> \<infinity> \<Longrightarrow> \<exists>t. x \<le> ereal t" by (cases x) auto }
- moreover case (Basis S)
+ case (Basis S)
+ {
+ fix x
+ have "x \<noteq> \<infinity> \<Longrightarrow> \<exists>t. x \<le> ereal t"
+ by (cases x) auto
+ }
+ moreover note Basis
ultimately show ?case
by (auto split: ereal.split)
qed (fastforce simp add: vimage_Union)+
@@ -1633,8 +1940,13 @@
with Int show ?case
by (intro exI[of _ "min x z"]) fastforce
next
- { fix x have "x \<noteq> - \<infinity> \<Longrightarrow> \<exists>t. ereal t \<le> x" by (cases x) auto }
- moreover case (Basis S)
+ case (Basis S)
+ {
+ fix x
+ have "x \<noteq> - \<infinity> \<Longrightarrow> \<exists>t. ereal t \<le> x"
+ by (cases x) auto
+ }
+ moreover note Basis
ultimately show ?case
by (auto split: ereal.split)
qed (fastforce simp add: vimage_Union)+
@@ -1642,13 +1954,18 @@
lemma open_ereal_vimage: "open S \<Longrightarrow> open (ereal -` S)"
unfolding open_ereal_generated
proof (induct rule: generate_topology.induct)
- case (Int A B) then show ?case by auto
+ case (Int A B)
+ then show ?case
+ by auto
next
- { fix x have
+ case (Basis S)
+ {
+ fix x have
"ereal -` {..<x} = (case x of PInfty \<Rightarrow> UNIV | MInfty \<Rightarrow> {} | ereal r \<Rightarrow> {..<r})"
"ereal -` {x<..} = (case x of PInfty \<Rightarrow> {} | MInfty \<Rightarrow> UNIV | ereal r \<Rightarrow> {r<..})"
- by (induct x) auto }
- moreover case (Basis S)
+ by (induct x) auto
+ }
+ moreover note Basis
ultimately show ?case
by (auto split: ereal.split)
qed (fastforce simp add: vimage_Union)+
@@ -1657,16 +1974,32 @@
unfolding open_generated_order[where 'a=real]
proof (induct rule: generate_topology.induct)
case (Basis S)
- moreover { fix x have "ereal ` {..< x} = { -\<infinity> <..< ereal x }" by auto (case_tac xa, auto) }
- moreover { fix x have "ereal ` {x <..} = { ereal x <..< \<infinity> }" by auto (case_tac xa, auto) }
+ moreover {
+ fix x
+ have "ereal ` {..< x} = { -\<infinity> <..< ereal x }"
+ apply auto
+ apply (case_tac xa)
+ apply auto
+ done
+ }
+ moreover {
+ fix x
+ have "ereal ` {x <..} = { ereal x <..< \<infinity> }"
+ apply auto
+ apply (case_tac xa)
+ apply auto
+ done
+ }
ultimately show ?case
by auto
qed (auto simp add: image_Union image_Int)
-lemma open_ereal_def: "open A \<longleftrightarrow> open (ereal -` A) \<and> (\<infinity> \<in> A \<longrightarrow> (\<exists>x. {ereal x <..} \<subseteq> A)) \<and> (-\<infinity> \<in> A \<longrightarrow> (\<exists>x. {..<ereal x} \<subseteq> A))"
+lemma open_ereal_def:
+ "open A \<longleftrightarrow> open (ereal -` A) \<and> (\<infinity> \<in> A \<longrightarrow> (\<exists>x. {ereal x <..} \<subseteq> A)) \<and> (-\<infinity> \<in> A \<longrightarrow> (\<exists>x. {..<ereal x} \<subseteq> A))"
(is "open A \<longleftrightarrow> ?rhs")
proof
- assume "open A" then show ?rhs
+ assume "open A"
+ then show ?rhs
using open_PInfty open_MInfty open_ereal_vimage by auto
next
assume "?rhs"
@@ -1678,14 +2011,23 @@
by (subst *) (auto simp: open_Un)
qed
-lemma open_PInfty2: assumes "open A" "\<infinity> \<in> A" obtains x where "{ereal x<..} \<subseteq> A"
+lemma open_PInfty2:
+ assumes "open A"
+ and "\<infinity> \<in> A"
+ obtains x where "{ereal x<..} \<subseteq> A"
using open_PInfty[OF assms] by auto
-lemma open_MInfty2: assumes "open A" "-\<infinity> \<in> A" obtains x where "{..<ereal x} \<subseteq> A"
+lemma open_MInfty2:
+ assumes "open A"
+ and "-\<infinity> \<in> A"
+ obtains x where "{..<ereal x} \<subseteq> A"
using open_MInfty[OF assms] by auto
-lemma ereal_openE: assumes "open A" obtains x y where
- "open (ereal -` A)" "\<infinity> \<in> A \<Longrightarrow> {ereal x<..} \<subseteq> A" "-\<infinity> \<in> A \<Longrightarrow> {..<ereal y} \<subseteq> A"
+lemma ereal_openE:
+ assumes "open A"
+ obtains x y where "open (ereal -` A)"
+ and "\<infinity> \<in> A \<Longrightarrow> {ereal x<..} \<subseteq> A"
+ and "-\<infinity> \<in> A \<Longrightarrow> {..<ereal y} \<subseteq> A"
using assms open_ereal_def by auto
lemmas open_ereal_lessThan = open_lessThan[where 'a=ereal]
@@ -1695,60 +2037,76 @@
lemmas closed_ereal_atMost = closed_atMost[where 'a=ereal]
lemmas closed_ereal_atLeastAtMost = closed_atLeastAtMost[where 'a=ereal]
lemmas closed_ereal_singleton = closed_singleton[where 'a=ereal]
-
+
lemma ereal_open_cont_interval:
fixes S :: "ereal set"
- assumes "open S" "x \<in> S" "\<bar>x\<bar> \<noteq> \<infinity>"
- obtains e where "e>0" "{x-e <..< x+e} \<subseteq> S"
-proof-
- from `open S` have "open (ereal -` S)" by (rule ereal_openE)
- then obtain e where "0 < e" and e: "\<And>y. dist y (real x) < e \<Longrightarrow> ereal y \<in> S"
+ assumes "open S"
+ and "x \<in> S"
+ and "\<bar>x\<bar> \<noteq> \<infinity>"
+ obtains e where "e > 0" and "{x-e <..< x+e} \<subseteq> S"
+proof -
+ from `open S`
+ have "open (ereal -` S)"
+ by (rule ereal_openE)
+ then obtain e where "e > 0" and e: "\<And>y. dist y (real x) < e \<Longrightarrow> ereal y \<in> S"
using assms unfolding open_dist by force
show thesis
proof (intro that subsetI)
- show "0 < ereal e" using `0 < e` by auto
- fix y assume "y \<in> {x - ereal e<..<x + ereal e}"
+ show "0 < ereal e"
+ using `0 < e` by auto
+ fix y
+ assume "y \<in> {x - ereal e<..<x + ereal e}"
with assms obtain t where "y = ereal t" "dist t (real x) < e"
- apply (cases y) by (auto simp: dist_real_def)
- then show "y \<in> S" using e[of t] by auto
+ by (cases y) (auto simp: dist_real_def)
+ then show "y \<in> S"
+ using e[of t] by auto
qed
qed
lemma ereal_open_cont_interval2:
fixes S :: "ereal set"
- assumes "open S" "x \<in> S" and x: "\<bar>x\<bar> \<noteq> \<infinity>"
- obtains a b where "a < x" "x < b" "{a <..< b} \<subseteq> S"
+ assumes "open S"
+ and "x \<in> S"
+ and x: "\<bar>x\<bar> \<noteq> \<infinity>"
+ obtains a b where "a < x" and "x < b" and "{a <..< b} \<subseteq> S"
proof -
obtain e where "0 < e" "{x - e<..<x + e} \<subseteq> S"
using assms by (rule ereal_open_cont_interval)
- with that[of "x-e" "x+e"] ereal_between[OF x, of e]
- show thesis by auto
+ with that[of "x - e" "x + e"] ereal_between[OF x, of e]
+ show thesis
+ by auto
qed
+
subsubsection {* Convergent sequences *}
-lemma lim_ereal[simp]:
- "((\<lambda>n. ereal (f n)) ---> ereal x) net \<longleftrightarrow> (f ---> x) net" (is "?l = ?r")
+lemma lim_ereal[simp]: "((\<lambda>n. ereal (f n)) ---> ereal x) net \<longleftrightarrow> (f ---> x) net"
+ (is "?l = ?r")
proof (intro iffI topological_tendstoI)
- fix S assume "?l" "open S" "x \<in> S"
+ fix S
+ assume "?l" and "open S" and "x \<in> S"
then show "eventually (\<lambda>x. f x \<in> S) net"
using `?l`[THEN topological_tendstoD, OF open_ereal, OF `open S`]
by (simp add: inj_image_mem_iff)
next
- fix S assume "?r" "open S" "ereal x \<in> S"
+ fix S
+ assume "?r" and "open S" and "ereal x \<in> S"
show "eventually (\<lambda>x. ereal (f x) \<in> S) net"
using `?r`[THEN topological_tendstoD, OF open_ereal_vimage, OF `open S`]
- using `ereal x \<in> S` by auto
+ using `ereal x \<in> S`
+ by auto
qed
lemma lim_real_of_ereal[simp]:
assumes lim: "(f ---> ereal x) net"
shows "((\<lambda>x. real (f x)) ---> x) net"
proof (intro topological_tendstoI)
- fix S assume "open S" "x \<in> S"
+ fix S
+ assume "open S" and "x \<in> S"
then have S: "open S" "ereal x \<in> ereal ` S"
by (simp_all add: inj_image_mem_iff)
- have "\<forall>x. f x \<in> ereal ` S \<longrightarrow> real (f x) \<in> S" by auto
+ have "\<forall>x. f x \<in> ereal ` S \<longrightarrow> real (f x) \<in> S"
+ by auto
from this lim[THEN topological_tendstoD, OF open_ereal, OF S]
show "eventually (\<lambda>x. real (f x) \<in> S) net"
by (rule eventually_mono)
@@ -1756,10 +2114,12 @@
lemma tendsto_PInfty: "(f ---> \<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. ereal r < f x) F)"
proof -
- { fix l :: ereal assume "\<forall>r. eventually (\<lambda>x. ereal r < f x) F"
- from this[THEN spec, of "real l"]
- have "l \<noteq> \<infinity> \<Longrightarrow> eventually (\<lambda>x. l < f x) F"
- by (cases l) (auto elim: eventually_elim1) }
+ {
+ fix l :: ereal
+ assume "\<forall>r. eventually (\<lambda>x. ereal r < f x) F"
+ from this[THEN spec, of "real l"] have "l \<noteq> \<infinity> \<Longrightarrow> eventually (\<lambda>x. l < f x) F"
+ by (cases l) (auto elim: eventually_elim1)
+ }
then show ?thesis
by (auto simp: order_tendsto_iff)
qed
@@ -1772,20 +2132,26 @@
from open_MInfty[OF this] obtain B where "{..<ereal B} \<subseteq> S" ..
moreover
assume "\<forall>r::real. eventually (\<lambda>z. f z < r) F"
- then have "eventually (\<lambda>z. f z \<in> {..< B}) F" by auto
- ultimately show "eventually (\<lambda>z. f z \<in> S) F" by (auto elim!: eventually_elim1)
+ then have "eventually (\<lambda>z. f z \<in> {..< B}) F"
+ by auto
+ ultimately show "eventually (\<lambda>z. f z \<in> S) F"
+ by (auto elim!: eventually_elim1)
next
- fix x assume "\<forall>S. open S \<longrightarrow> -\<infinity> \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
- from this[rule_format, of "{..< ereal x}"]
- show "eventually (\<lambda>y. f y < ereal x) F" by auto
+ fix x
+ assume "\<forall>S. open S \<longrightarrow> -\<infinity> \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
+ from this[rule_format, of "{..< ereal x}"] show "eventually (\<lambda>y. f y < ereal x) F"
+ by auto
qed
lemma Lim_PInfty: "f ----> \<infinity> \<longleftrightarrow> (\<forall>B. \<exists>N. \<forall>n\<ge>N. f n \<ge> ereal B)"
unfolding tendsto_PInfty eventually_sequentially
proof safe
- fix r assume "\<forall>r. \<exists>N. \<forall>n\<ge>N. ereal r \<le> f n"
- then obtain N where "\<forall>n\<ge>N. ereal (r + 1) \<le> f n" by blast
- moreover have "ereal r < ereal (r + 1)" by auto
+ fix r
+ assume "\<forall>r. \<exists>N. \<forall>n\<ge>N. ereal r \<le> f n"
+ then obtain N where "\<forall>n\<ge>N. ereal (r + 1) \<le> f n"
+ by blast
+ moreover have "ereal r < ereal (r + 1)"
+ by auto
ultimately show "\<exists>N. \<forall>n\<ge>N. ereal r < f n"
by (blast intro: less_le_trans)
qed (blast intro: less_imp_le)
@@ -1793,9 +2159,12 @@
lemma Lim_MInfty: "f ----> -\<infinity> \<longleftrightarrow> (\<forall>B. \<exists>N. \<forall>n\<ge>N. ereal B \<ge> f n)"
unfolding tendsto_MInfty eventually_sequentially
proof safe
- fix r assume "\<forall>r. \<exists>N. \<forall>n\<ge>N. f n \<le> ereal r"
- then obtain N where "\<forall>n\<ge>N. f n \<le> ereal (r - 1)" by blast
- moreover have "ereal (r - 1) < ereal r" by auto
+ fix r
+ assume "\<forall>r. \<exists>N. \<forall>n\<ge>N. f n \<le> ereal r"
+ then obtain N where "\<forall>n\<ge>N. f n \<le> ereal (r - 1)"
+ by blast
+ moreover have "ereal (r - 1) < ereal r"
+ by auto
ultimately show "\<exists>N. \<forall>n\<ge>N. f n < ereal r"
by (blast intro: le_less_trans)
qed (blast intro: less_imp_le)
@@ -1807,38 +2176,43 @@
using LIMSEQ_le_const[of f l "ereal B"] by auto
lemma tendsto_explicit:
- "f ----> f0 <-> (ALL S. open S --> f0 : S --> (EX N. ALL n>=N. f n : S))"
+ "f ----> f0 \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> f0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. f n \<in> S))"
unfolding tendsto_def eventually_sequentially by auto
-lemma Lim_bounded_PInfty2:
- "f ----> l \<Longrightarrow> ALL n>=N. f n <= ereal B \<Longrightarrow> l ~= \<infinity>"
+lemma Lim_bounded_PInfty2: "f ----> l \<Longrightarrow> \<forall>n\<ge>N. f n \<le> ereal B \<Longrightarrow> l \<noteq> \<infinity>"
using LIMSEQ_le_const2[of f l "ereal B"] by fastforce
-lemma Lim_bounded_ereal: "f ----> (l :: 'a::linorder_topology) \<Longrightarrow> ALL n>=M. f n <= C \<Longrightarrow> l<=C"
+lemma Lim_bounded_ereal: "f ----> (l :: 'a::linorder_topology) \<Longrightarrow> \<forall>n\<ge>M. f n \<le> C \<Longrightarrow> l \<le> C"
by (intro LIMSEQ_le_const2) auto
lemma Lim_bounded2_ereal:
- assumes lim:"f ----> (l :: 'a::linorder_topology)" and ge: "ALL n>=N. f n >= C"
- shows "l>=C"
+ assumes lim:"f ----> (l :: 'a::linorder_topology)"
+ and ge: "\<forall>n\<ge>N. f n \<ge> C"
+ shows "l \<ge> C"
using ge
by (intro tendsto_le[OF trivial_limit_sequentially lim tendsto_const])
(auto simp: eventually_sequentially)
lemma real_of_ereal_mult[simp]:
- fixes a b :: ereal shows "real (a * b) = real a * real b"
+ fixes a b :: ereal
+ shows "real (a * b) = real a * real b"
by (cases rule: ereal2_cases[of a b]) auto
lemma real_of_ereal_eq_0:
- fixes x :: ereal shows "real x = 0 \<longleftrightarrow> x = \<infinity> \<or> x = -\<infinity> \<or> x = 0"
+ fixes x :: ereal
+ shows "real x = 0 \<longleftrightarrow> x = \<infinity> \<or> x = -\<infinity> \<or> x = 0"
by (cases x) auto
lemma tendsto_ereal_realD:
fixes f :: "'a \<Rightarrow> ereal"
- assumes "x \<noteq> 0" and tendsto: "((\<lambda>x. ereal (real (f x))) ---> x) net"
+ assumes "x \<noteq> 0"
+ and tendsto: "((\<lambda>x. ereal (real (f x))) ---> x) net"
shows "(f ---> x) net"
proof (intro topological_tendstoI)
- fix S assume S: "open S" "x \<in> S"
- with `x \<noteq> 0` have "open (S - {0})" "x \<in> S - {0}" by auto
+ fix S
+ assume S: "open S" "x \<in> S"
+ with `x \<noteq> 0` have "open (S - {0})" "x \<in> S - {0}"
+ by auto
from tendsto[THEN topological_tendstoD, OF this]
show "eventually (\<lambda>x. f x \<in> S) net"
by (rule eventually_rev_mp) (auto simp: ereal_real)
@@ -1849,22 +2223,25 @@
assumes x: "\<bar>x\<bar> \<noteq> \<infinity>" and tendsto: "(f ---> x) net"
shows "((\<lambda>x. ereal (real (f x))) ---> x) net"
proof (intro topological_tendstoI)
- fix S assume "open S" "x \<in> S"
- with x have "open (S - {\<infinity>, -\<infinity>})" "x \<in> S - {\<infinity>, -\<infinity>}" by auto
+ fix S
+ assume "open S" and "x \<in> S"
+ with x have "open (S - {\<infinity>, -\<infinity>})" "x \<in> S - {\<infinity>, -\<infinity>}"
+ by auto
from tendsto[THEN topological_tendstoD, OF this]
show "eventually (\<lambda>x. ereal (real (f x)) \<in> S) net"
by (elim eventually_elim1) (auto simp: ereal_real)
qed
lemma ereal_mult_cancel_left:
- fixes a b c :: ereal shows "a * b = a * c \<longleftrightarrow>
- ((\<bar>a\<bar> = \<infinity> \<and> 0 < b * c) \<or> a = 0 \<or> b = c)"
- by (cases rule: ereal3_cases[of a b c])
- (simp_all add: zero_less_mult_iff)
+ fixes a b c :: ereal
+ shows "a * b = a * c \<longleftrightarrow> (\<bar>a\<bar> = \<infinity> \<and> 0 < b * c) \<or> a = 0 \<or> b = c"
+ by (cases rule: ereal3_cases[of a b c]) (simp_all add: zero_less_mult_iff)
lemma ereal_inj_affinity:
fixes m t :: ereal
- assumes "\<bar>m\<bar> \<noteq> \<infinity>" "m \<noteq> 0" "\<bar>t\<bar> \<noteq> \<infinity>"
+ assumes "\<bar>m\<bar> \<noteq> \<infinity>"
+ and "m \<noteq> 0"
+ and "\<bar>t\<bar> \<noteq> \<infinity>"
shows "inj_on (\<lambda>x. m * x + t) A"
using assms
by (cases rule: ereal2_cases[of m t])
@@ -1902,108 +2279,136 @@
lemma ereal_mult_m1[simp]: "x * ereal (-1) = -x"
by (cases x) auto
-lemma ereal_real': assumes "\<bar>x\<bar> \<noteq> \<infinity>" shows "ereal (real x) = x"
+lemma ereal_real':
+ assumes "\<bar>x\<bar> \<noteq> \<infinity>"
+ shows "ereal (real x) = x"
using assms by auto
-lemma real_ereal_id: "real o ereal = id"
-proof-
- { fix x have "(real o ereal) x = id x" by auto }
- then show ?thesis using ext by blast
+lemma real_ereal_id: "real \<circ> ereal = id"
+proof -
+ {
+ fix x
+ have "(real o ereal) x = id x"
+ by auto
+ }
+ then show ?thesis
+ using ext by blast
qed
lemma open_image_ereal: "open(UNIV-{ \<infinity> , (-\<infinity> :: ereal)})"
-by (metis range_ereal open_ereal open_UNIV)
+ by (metis range_ereal open_ereal open_UNIV)
lemma ereal_le_distrib:
- fixes a b c :: ereal shows "c * (a + b) \<le> c * a + c * b"
+ fixes a b c :: ereal
+ shows "c * (a + b) \<le> c * a + c * b"
by (cases rule: ereal3_cases[of a b c])
(auto simp add: field_simps not_le mult_le_0_iff mult_less_0_iff)
lemma ereal_pos_distrib:
- fixes a b c :: ereal assumes "0 \<le> c" "c \<noteq> \<infinity>" shows "c * (a + b) = c * a + c * b"
- using assms by (cases rule: ereal3_cases[of a b c])
- (auto simp add: field_simps not_le mult_le_0_iff mult_less_0_iff)
+ fixes a b c :: ereal
+ assumes "0 \<le> c"
+ and "c \<noteq> \<infinity>"
+ shows "c * (a + b) = c * a + c * b"
+ using assms
+ by (cases rule: ereal3_cases[of a b c])
+ (auto simp add: field_simps not_le mult_le_0_iff mult_less_0_iff)
lemma ereal_pos_le_distrib:
-fixes a b c :: ereal
-assumes "c>=0"
-shows "c * (a + b) <= c * a + c * b"
- using assms by (cases rule: ereal3_cases[of a b c])
- (auto simp add: field_simps)
+ fixes a b c :: ereal
+ assumes "c \<ge> 0"
+ shows "c * (a + b) \<le> c * a + c * b"
+ using assms
+ by (cases rule: ereal3_cases[of a b c]) (auto simp add: field_simps)
-lemma ereal_max_mono:
- "[| (a::ereal) <= b; c <= d |] ==> max a c <= max b d"
+lemma ereal_max_mono: "(a::ereal) \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> max a c \<le> max b d"
by (metis sup_ereal_def sup_mono)
-
-lemma ereal_max_least:
- "[| (a::ereal) <= x; c <= x |] ==> max a c <= x"
+lemma ereal_max_least: "(a::ereal) \<le> x \<Longrightarrow> c \<le> x \<Longrightarrow> max a c \<le> x"
by (metis sup_ereal_def sup_least)
lemma ereal_LimI_finite:
fixes x :: ereal
assumes "\<bar>x\<bar> \<noteq> \<infinity>"
- assumes "!!r. 0 < r ==> EX N. ALL n>=N. u n < x + r & x < u n + r"
+ and "\<And>r. 0 < r \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. u n < x + r \<and> x < u n + r"
shows "u ----> x"
proof (rule topological_tendstoI, unfold eventually_sequentially)
- obtain rx where rx_def: "x=ereal rx" using assms by (cases x) auto
- fix S assume "open S" "x : S"
- then have "open (ereal -` S)" unfolding open_ereal_def by auto
- with `x \<in> S` obtain r where "0 < r" and dist: "!!y. dist y rx < r ==> ereal y \<in> S"
- unfolding open_real_def rx_def by auto
+ obtain rx where rx: "x = ereal rx"
+ using assms by (cases x) auto
+ fix S
+ assume "open S" and "x \<in> S"
+ then have "open (ereal -` S)"
+ unfolding open_ereal_def by auto
+ with `x \<in> S` obtain r where "0 < r" and dist: "\<And>y. dist y rx < r \<Longrightarrow> ereal y \<in> S"
+ unfolding open_real_def rx by auto
then obtain n where
- upper: "!!N. n <= N ==> u N < x + ereal r" and
- lower: "!!N. n <= N ==> x < u N + ereal r" using assms(2)[of "ereal r"] by auto
- show "EX N. ALL n>=N. u n : S"
+ upper: "\<And>N. n \<le> N \<Longrightarrow> u N < x + ereal r" and
+ lower: "\<And>N. n \<le> N \<Longrightarrow> x < u N + ereal r"
+ using assms(2)[of "ereal r"] by auto
+ show "\<exists>N. \<forall>n\<ge>N. u n \<in> S"
proof (safe intro!: exI[of _ n])
- fix N assume "n <= N"
+ fix N
+ assume "n \<le> N"
from upper[OF this] lower[OF this] assms `0 < r`
- have "u N ~: {\<infinity>,(-\<infinity>)}" by auto
- then obtain ra where ra_def: "(u N) = ereal ra" by (cases "u N") auto
- hence "rx < ra + r" and "ra < rx + r"
- using rx_def assms `0 < r` lower[OF `n <= N`] upper[OF `n <= N`] by auto
- hence "dist (real (u N)) rx < r"
- using rx_def ra_def
+ have "u N \<notin> {\<infinity>,(-\<infinity>)}"
+ by auto
+ then obtain ra where ra_def: "(u N) = ereal ra"
+ by (cases "u N") auto
+ then have "rx < ra + r" and "ra < rx + r"
+ using rx assms `0 < r` lower[OF `n \<le> N`] upper[OF `n \<le> N`]
+ by auto
+ then have "dist (real (u N)) rx < r"
+ using rx ra_def
by (auto simp: dist_real_def abs_diff_less_iff field_simps)
- from dist[OF this] show "u N : S" using `u N ~: {\<infinity>, -\<infinity>}`
+ from dist[OF this] show "u N \<in> S"
+ using `u N \<notin> {\<infinity>, -\<infinity>}`
by (auto simp: ereal_real split: split_if_asm)
qed
qed
lemma tendsto_obtains_N:
assumes "f ----> f0"
- assumes "open S" "f0 : S"
- obtains N where "ALL n>=N. f n : S"
+ assumes "open S"
+ and "f0 \<in> S"
+ obtains N where "\<forall>n\<ge>N. f n \<in> S"
using assms using tendsto_def
using tendsto_explicit[of f f0] assms by auto
lemma ereal_LimI_finite_iff:
fixes x :: ereal
assumes "\<bar>x\<bar> \<noteq> \<infinity>"
- shows "u ----> x <-> (ALL r. 0 < r --> (EX N. ALL n>=N. u n < x + r & x < u n + r))"
- (is "?lhs <-> ?rhs")
+ shows "u ----> x \<longleftrightarrow> (\<forall>r. 0 < r \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. u n < x + r \<and> x < u n + r))"
+ (is "?lhs \<longleftrightarrow> ?rhs")
proof
assume lim: "u ----> x"
- { fix r assume "(r::ereal)>0"
- then obtain N where N_def: "ALL n>=N. u n : {x - r <..< x + r}"
+ {
+ fix r :: ereal
+ assume "r > 0"
+ then obtain N where "\<forall>n\<ge>N. u n \<in> {x - r <..< x + r}"
apply (subst tendsto_obtains_N[of u x "{x - r <..< x + r}"])
- using lim ereal_between[of x r] assms `r>0` by auto
- hence "EX N. ALL n>=N. u n < x + r & x < u n + r"
- using ereal_minus_less[of r x] by (cases r) auto
- } then show "?rhs" by auto
+ using lim ereal_between[of x r] assms `r > 0`
+ apply auto
+ done
+ then have "\<exists>N. \<forall>n\<ge>N. u n < x + r \<and> x < u n + r"
+ using ereal_minus_less[of r x]
+ by (cases r) auto
+ }
+ then show ?rhs
+ by auto
next
- assume ?rhs then show "u ----> x"
+ assume ?rhs
+ then show "u ----> x"
using ereal_LimI_finite[of x] assms by auto
qed
lemma ereal_Limsup_uminus:
- fixes f :: "'a => ereal"
- shows "Limsup net (\<lambda>x. - (f x)) = -(Liminf net f)"
+ fixes f :: "'a \<Rightarrow> ereal"
+ shows "Limsup net (\<lambda>x. - (f x)) = - Liminf net f"
unfolding Limsup_def Liminf_def ereal_SUPR_uminus ereal_INFI_uminus ..
lemma liminf_bounded_iff:
fixes x :: "nat \<Rightarrow> ereal"
- shows "C \<le> liminf x \<longleftrightarrow> (\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n)" (is "?lhs <-> ?rhs")
+ shows "C \<le> liminf x \<longleftrightarrow> (\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n)"
+ (is "?lhs \<longleftrightarrow> ?rhs")
unfolding le_Liminf_iff eventually_sequentially ..
lemma
@@ -2012,6 +2417,7 @@
and ereal_decseq_uminus[simp]: "decseq (\<lambda>i. - X i) = incseq X"
unfolding incseq_def decseq_def by auto
+
subsubsection {* Tests for code generator *}
(* A small list of simple arithmetic expressions *)
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Sep 25 12:43:20 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Sep 25 13:39:34 2013 +0200
@@ -1485,19 +1485,10 @@
text{* The expected monotonicity property. *}
-lemma Lim_within_empty: "(f ---> l) (at x within {})"
- unfolding tendsto_def eventually_at_filter by simp
-
lemma Lim_Un:
assumes "(f ---> l) (at x within S)" "(f ---> l) (at x within T)"
shows "(f ---> l) (at x within (S \<union> T))"
- using assms
- unfolding tendsto_def eventually_at_filter
- apply clarify
- apply (drule spec, drule (1) mp, drule (1) mp)
- apply (drule spec, drule (1) mp, drule (1) mp)
- apply (auto elim: eventually_elim2)
- done
+ using assms unfolding at_within_union by (rule filterlim_sup)
lemma Lim_Un_univ:
"(f ---> l) (at x within S) \<Longrightarrow> (f ---> l) (at x within T) \<Longrightarrow>
@@ -1537,7 +1528,7 @@
unfolding filter_eq_iff by (intro allI eventually_within_interior)
lemma Lim_within_LIMSEQ:
- fixes a :: "'a::metric_space"
+ fixes a :: "'a::first_countable_topology"
assumes "\<forall>S. (\<forall>n. S n \<noteq> a \<and> S n \<in> T) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
shows "(X ---> L) (at a within T)"
using assms unfolding tendsto_def [where l=L]
@@ -1551,7 +1542,7 @@
shows "(f ---> Inf (f ` ({x<..} \<inter> I))) (at x within ({x<..} \<inter> I))"
proof (cases "{x<..} \<inter> I = {}")
case True
- then show ?thesis by (simp add: Lim_within_empty)
+ then show ?thesis by simp
next
case False
show ?thesis
@@ -1623,14 +1614,6 @@
qed
qed
-lemma Lim_inv: (* TODO: delete *)
- fixes f :: "'a \<Rightarrow> real"
- and A :: "'a filter"
- assumes "(f ---> l) A"
- and "l \<noteq> 0"
- shows "((inverse \<circ> f) ---> inverse l) A"
- unfolding o_def using assms by (rule tendsto_inverse)
-
lemma Lim_null:
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
shows "(f ---> l) net \<longleftrightarrow> ((\<lambda>x. f(x) - l) ---> 0) net"
--- a/src/HOL/Topological_Spaces.thy Wed Sep 25 12:43:20 2013 +0200
+++ b/src/HOL/Topological_Spaces.thy Wed Sep 25 13:39:34 2013 +0200
@@ -490,7 +490,7 @@
unfolding le_filter_def eventually_Sup by simp }
{ show "Inf {} = (top::'a filter)"
by (auto simp: top_filter_def Inf_filter_def Sup_filter_def)
- (metis (full_types) Topological_Spaces.top_filter_def always_eventually eventually_top) }
+ (metis (full_types) top_filter_def always_eventually eventually_top) }
{ show "Sup {} = (bot::'a filter)"
by (auto simp: bot_filter_def Sup_filter_def) }
qed
@@ -754,6 +754,13 @@
lemma at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a"
unfolding filter_eq_iff eventually_at_topological by (metis open_Int Int_iff UNIV_I)
+lemma at_within_empty [simp]: "at a within {} = bot"
+ unfolding at_within_def by simp
+
+lemma at_within_union: "at x within (S \<union> T) = sup (at x within S) (at x within T)"
+ unfolding filter_eq_iff eventually_sup eventually_at_filter
+ by (auto elim!: eventually_rev_mp)
+
lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"
unfolding trivial_limit_def eventually_at_topological
by (safe, case_tac "S = {a}", simp, fast, fast)
--- a/src/Pure/PIDE/query_operation.scala Wed Sep 25 12:43:20 2013 +0200
+++ b/src/Pure/PIDE/query_operation.scala Wed Sep 25 13:39:34 2013 +0200
@@ -18,6 +18,7 @@
val WAITING = Value("waiting")
val RUNNING = Value("running")
val FINISHED = Value("finished")
+ val REMOVED = Value("removed")
}
}
@@ -37,7 +38,7 @@
private var current_query: List[String] = Nil
private var current_update_pending = false
private var current_output: List[XML.Tree] = Nil
- private var current_status = Query_Operation.Status.FINISHED
+ private var current_status = Query_Operation.Status.REMOVED
private var current_exec_id = Document_ID.none
private def reset_state()
@@ -46,7 +47,7 @@
current_query = Nil
current_update_pending = false
current_output = Nil
- current_status = Query_Operation.Status.FINISHED
+ current_status = Query_Operation.Status.REMOVED
current_exec_id = Document_ID.none
}
@@ -100,7 +101,7 @@
results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status })
val new_status =
- if (removed) Query_Operation.Status.FINISHED
+ if (removed) Query_Operation.Status.REMOVED
else
get_status(Markup.FINISHED, Query_Operation.Status.FINISHED) orElse
get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse
@@ -128,7 +129,7 @@
if (current_status != new_status) {
current_status = new_status
consume_status(new_status)
- if (new_status == Query_Operation.Status.FINISHED) {
+ if (new_status == Query_Operation.Status.REMOVED) {
remove_overlay()
editor.flush()
}
@@ -187,7 +188,7 @@
current_location match {
case Some(command)
if current_update_pending ||
- (current_status != Query_Operation.Status.FINISHED &&
+ (current_status != Query_Operation.Status.REMOVED &&
changed.commands.contains(command)) =>
Swing_Thread.later { content_update() }
case _ =>
--- a/src/Tools/jEdit/src/find_dockable.scala Wed Sep 25 12:43:20 2013 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala Wed Sep 25 13:39:34 2013 +0200
@@ -37,7 +37,7 @@
process_indicator.update("Waiting for evaluation of context ...", 5)
case Query_Operation.Status.RUNNING =>
process_indicator.update("Running find operation ...", 15)
- case Query_Operation.Status.FINISHED =>
+ case _ =>
process_indicator.update(null, 0)
}
}
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Wed Sep 25 12:43:20 2013 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Wed Sep 25 13:39:34 2013 +0200
@@ -38,7 +38,7 @@
process_indicator.update("Waiting for evaluation of context ...", 5)
case Query_Operation.Status.RUNNING =>
process_indicator.update("Sledgehammering ...", 15)
- case Query_Operation.Status.FINISHED =>
+ case _ =>
process_indicator.update(null, 0)
}
}