# HG changeset patch # User nipkow # Date 1380116955 -7200 # Node ID b65b4e70a258bc53890258bc6bee37048c85b6a6 # Parent 87941795956c65e32c0c1e94080211cd785ee695# Parent ac5b8687f1d9dffafae5bfff7e0a4ea797d1d491 merged diff -r ac5b8687f1d9 -r b65b4e70a258 src/HOL/BNF/Tools/bnf_ctr_sugar.ML --- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Wed Sep 25 15:49:09 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Wed Sep 25 15:49:15 2013 +0200 @@ -40,9 +40,9 @@ 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) * @@ -215,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), diff -r ac5b8687f1d9 -r b65b4e70a258 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Wed Sep 25 15:49:09 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Wed Sep 25 15:49:15 2013 +0200 @@ -51,17 +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) - | invert_prems ts = [mk_disjs (map s_not ts)]; -fun invert_prems_disj [t] = map s_not (HOLogic.disjuncts t) - | invert_prems_disj ts = [mk_disjs (map (mk_conjs o map s_not o HOLogic.disjuncts) ts)]; fun abstract vs = let fun a n (t $ u) = a n t $ a n u | a n (Abs (v, T, b)) = Abs (v, T, a (n + 1) b) @@ -455,7 +444,7 @@ val matchedss = AList.lookup (op =) matchedsss fun_name |> the_default []; val prems = map (abstract (List.rev fun_args)) prems'; val real_prems = - (if catch_all orelse sequential then maps invert_prems_disj matchedss else []) @ + (if catch_all orelse sequential then maps negate_disj matchedss else []) @ (if catch_all then [] else prems); val matchedsss' = AList.delete (op =) fun_name matchedsss @@ -584,17 +573,21 @@ fun build_corec_args_direct_call lthy has_call sel_eqns sel = let val maybe_sel_eqn = find_first (equal sel o #sel) sel_eqns; - fun rewrite_q t = if has_call t then @{term False} else @{term True}; - fun rewrite_g t = if has_call t then undef_const else t; - fun rewrite_h t = if has_call t then HOLogic.mk_tuple (snd (strip_comb t)) else undef_const; - fun massage _ NONE t = t - | massage f (SOME {fun_args, rhs_term, ...}) t = - massage_direct_corec_call lthy has_call f [] (range_type (fastype_of t)) rhs_term - |> abs_tuple fun_args; in - (massage rewrite_q maybe_sel_eqn, - massage rewrite_g maybe_sel_eqn, - massage rewrite_h maybe_sel_eqn) + if is_none maybe_sel_eqn then (I, I, I) else + let + val {fun_args, rhs_term, ... } = the maybe_sel_eqn; + fun rewrite_q t = if has_call t then @{term False} else @{term True}; + fun rewrite_g t = if has_call t then undef_const else t; + fun rewrite_h t = if has_call t then HOLogic.mk_tuple (snd (strip_comb t)) else undef_const; + fun massage f t = + massage_direct_corec_call lthy has_call f [] (range_type (fastype_of t)) rhs_term + |> abs_tuple fun_args; + in + (massage rewrite_q, + massage rewrite_g, + massage rewrite_h) + end end; fun build_corec_arg_indirect_call lthy has_call sel_eqns sel = @@ -692,7 +685,7 @@ ctr = #ctr (nth ctr_specs n), ctr_no = n, disc = #disc (nth ctr_specs n), - prems = maps (invert_prems o #prems) disc_eqns, + prems = maps (negate_conj o #prems) disc_eqns, auto_gen = true, user_eqn = undef_const}; in @@ -791,7 +784,7 @@ let val (SOME ctr_spec) = find_first (equal ctr o #ctr) ctr_specs; val ctr_no = find_index (equal ctr o #ctr) ctr_specs; - val prems = the_default (maps (invert_prems o #prems) disc_eqns) + val prems = the_default (maps (negate_conj o #prems) disc_eqns) (find_first (equal ctr_no o #ctr_no) disc_eqns |> Option.map #prems); val sel_corec = find_index (equal sel) (#sels ctr_spec) |> nth (#sel_corecs ctr_spec); @@ -814,16 +807,10 @@ fun prove_ctr disc_alist sel_alist disc_eqns sel_eqns {ctr, disc, sels, collapse, ...} = if not (exists (equal ctr o #ctr) disc_eqns) andalso not (exists (equal ctr o #ctr) sel_eqns) -(* -andalso (warning ("no eqns for ctr " ^ Syntax.string_of_term lthy ctr); true) -*) orelse (* don't try to prove theorems when some sel_eqns are missing *) filter (equal ctr o #ctr) sel_eqns |> fst o finds ((op =) o apsnd #sel) sels |> exists (null o snd) -(* -andalso (warning ("sel_eqn(s) missing for ctr " ^ Syntax.string_of_term lthy ctr); true) -*) then [] else let val (fun_name, fun_T, fun_args, prems) = @@ -847,7 +834,7 @@ mk_primcorec_ctr_of_dtr_tac lthy m collapse maybe_disc_thm sel_thms |> K |> Goal.prove lthy [] [] t |> single - end; + end; val disc_alists = map3 (maps oo prove_disc) corec_specs exclssss disc_eqnss; val sel_alists = map4 (map ooo prove_sel) corec_specs disc_eqnss exclssss sel_eqnss; @@ -857,12 +844,13 @@ val ctr_thmss = map5 (maps oooo prove_ctr) disc_alists sel_alists disc_eqnss sel_eqnss (map #ctr_specs corec_specs); - val safess = map (map (K false)) ctr_thmss; (* FIXME: "true" for non-corecursive theorems *) + val safess = map (map (not o exists_subterm (member (op =) (map SOME fun_names) o + try (fst o dest_Free)) o snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o + Logic.strip_imp_concl o drop_All o prop_of)) ctr_thmss; val safe_ctr_thmss = map (map snd o filter fst o (op ~~)) (safess ~~ ctr_thmss); - fun mk_simp_thms disc_thms sel_thms ctr_thms = disc_thms @ sel_thms @ ctr_thms; - - val simp_thmss = map3 mk_simp_thms disc_thmss sel_thmss safe_ctr_thmss; + val simp_thmss = + map3 (fn x => fn y => fn z => x @ y @ z) disc_thmss sel_thmss safe_ctr_thmss; val common_name = mk_common_name fun_names; diff -r ac5b8687f1d9 -r b65b4e70a258 src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Wed Sep 25 15:49:09 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Wed Sep 25 15:49:15 2013 +0200 @@ -51,6 +51,13 @@ nested_map_comps: thm list, ctr_specs: corec_ctr_spec list} + val s_not: term -> term + val mk_conjs: term list -> term + val mk_disjs: term list -> term + val s_not_disj: term -> term list + val negate_conj: term list -> term list + val negate_disj: term list -> term list + 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 +67,9 @@ 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: Proof.context -> (term -> term list -> 'a -> 'a) -> typ list -> - term -> 'a -> 'a + 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 +146,24 @@ 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 + (* TODO: is the next case really needed? *) + | 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}; + +val s_not_disj = map s_not o HOLogic.disjuncts; + +fun negate_conj [t] = s_not_disj t + | negate_conj ts = [mk_disjs (map s_not ts)]; + +fun negate_disj [t] = s_not_disj t + | negate_disj ts = [mk_disjs (map (mk_conjs o s_not_disj) ts)]; + 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 +200,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,25 +222,33 @@ massage_call end; -fun case_of ctxt = ctr_sugar_of ctxt #> Option.map (fst o dest_Const o #casex); - fun fold_rev_let_if_case ctxt f bound_Ts = let - fun fld t = + val thy = Proof_Context.theory_of ctxt; + + fun fld conds 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 Let}, _), [arg1, arg2]) => fld conds (betapply (arg2, arg1)) + | (Const (@{const_name If}, _), [cond, then_branch, else_branch]) => + fld (conds @ conjuncts cond) then_branch + o fld (conds @ s_not_disj cond) else_branch | (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 fold_rev fld branches else f t - | _ => f t) + 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 (append conds o conjuncts) conds' ~~ branches)) + | _ => f conds t) end - | _ => f t) + | _ => f conds t) in - fld + 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; @@ -224,7 +258,7 @@ (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) + 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 @@ -234,7 +268,7 @@ val branches' = map massage_rec branches; val casex' = Const (c, map typof branches' ---> typof obj); in - list_comb (casex', branches') $ tap check_obj obj + Term.list_comb (casex', branches') $ tap check_obj obj end else massage_leaf t @@ -269,7 +303,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 @@ -288,7 +322,8 @@ (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 @@ -309,7 +344,8 @@ fun expand_ctr_term ctxt s Ts t = (case ctr_sugar_of ctxt s of - SOME {ctrs, casex, ...} => list_comb (mk_case Ts (Type (s, Ts)) casex, map (mk_ctr Ts) ctrs) $ t + 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 = @@ -325,7 +361,8 @@ fun massage_corec_code_rhs ctxt massage_ctr = massage_let_if_case ctxt (K false) (uncurry massage_ctr o Term.strip_comb); -fun fold_rev_corec_code_rhs ctxt f = fold_rev_let_if_case ctxt (uncurry f o Term.strip_comb); +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; diff -r ac5b8687f1d9 -r b65b4e70a258 src/HOL/BNF/Tools/bnf_util.ML --- a/src/HOL/BNF/Tools/bnf_util.ML Wed Sep 25 15:49:09 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_util.ML Wed Sep 25 15:49:15 2013 +0200 @@ -134,6 +134,8 @@ val list_all_free: term list -> term -> term val list_exists_free: term list -> term -> term + val conjuncts: term -> term list + (*parameterized terms*) val mk_nthN: int -> term -> int -> term @@ -637,15 +639,19 @@ fun rapp u t = betapply (t, u); -val list_all_free = +fun list_quant_free quant_const = fold_rev (fn free => fn P => let val (x, T) = Term.dest_Free free; - in HOLogic.all_const T $ Term.absfree (x, T) P end); + in quant_const T $ Term.absfree (x, T) P end); + +val list_all_free = list_quant_free HOLogic.all_const; +val list_exists_free = list_quant_free HOLogic.exists_const; -val list_exists_free = - fold_rev (fn free => fn P => - let val (x, T) = Term.dest_Free free; - in HOLogic.exists_const T $ Term.absfree (x, T) P end); +(*Like dest_conj, but flattens conjunctions however nested*) +fun conjuncts_aux (Const (@{const_name HOL.conj}, _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs) + | conjuncts_aux t conjs = t::conjs; + +fun conjuncts t = conjuncts_aux t []; fun find_indices eq xs ys = map_filter I (map_index (fn (i, y) => if member eq xs y then SOME i else NONE) ys); diff -r ac5b8687f1d9 -r b65b4e70a258 src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Wed Sep 25 15:49:09 2013 +0200 +++ b/src/HOL/Library/Extended_Real.thy Wed Sep 25 15:49:15 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 "(\::ereal) = PInfty" - instance .. + +definition "(\::ereal) = PInfty" +instance .. + end declare [[coercion "ereal :: real \ 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]: "\ = 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 \ a = b" + fixes a b :: ereal + shows "-a = -b \ a = b" by (cases rule: ereal2_cases[of a b]) simp_all function of_ereal :: "ereal \ real" where -"of_ereal (ereal r) = r" | -"of_ereal \ = 0" | -"of_ereal (-\) = 0" + "of_ereal (ereal r) = r" +| "of_ereal \ = 0" +| "of_ereal (-\) = 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 \ of_ereal" lemma real_of_ereal[simp]: - "real (- x :: ereal) = - (real x)" - "real (ereal r) = r" - "real (\::ereal) = 0" + "real (- x :: ereal) = - (real x)" + "real (ereal r) = r" + "real (\::ereal) = 0" by (cases x) (simp_all add: real_of_ereal_def) lemma range_ereal[simp]: "range ereal = UNIV - {\, -\}" proof safe - fix x assume "x \ range ereal" "x \ \" - then show "x = -\" by (cases x) auto + fix x + assume "x \ range ereal" "x \ \" + then show "x = -\" + by (cases x) auto qed auto lemma ereal_range_uminus[simp]: "range uminus = (UNIV::ereal set)" proof safe - fix x :: ereal show "x \ range uminus" by (intro image_eqI[of _ _ "-x"]) auto + fix x :: ereal + show "x \ range uminus" + by (intro image_eqI[of _ _ "-x"]) auto qed auto instantiation ereal :: abs begin - function abs_ereal where - "\ereal r\ = ereal \r\" - | "\-\\ = (\::ereal)" - | "\\\ = (\::ereal)" - by (auto intro: ereal_cases) - termination proof qed (rule wf_empty) - instance .. + +function abs_ereal where + "\ereal r\ = ereal \r\" +| "\-\\ = (\::ereal)" +| "\\\ = (\::ereal)" +by (auto intro: ereal_cases) +termination proof qed (rule wf_empty) + +instance .. + end -lemma abs_eq_infinity_cases[elim!]: "\ \x :: ereal\ = \ ; x = \ \ P ; x = -\ \ P \ \ P" - by (cases x) auto +lemma abs_eq_infinity_cases[elim!]: + fixes x :: ereal + assumes "\x\ = \" + obtains "x = \" | "x = -\" + using assms by (cases x) auto -lemma abs_neq_infinity_cases[elim!]: "\ \x :: ereal\ \ \ ; \r. x = ereal r \ P \ \ P" +lemma abs_neq_infinity_cases[elim!]: + fixes x :: ereal + assumes "\x\ \ \" + obtains r where "x = ereal r" + using assms by (cases x) auto + +lemma abs_ereal_uminus[simp]: + fixes x :: ereal + shows "\- x\ = \x\" by (cases x) auto -lemma abs_ereal_uminus[simp]: "\- x\ = \x::ereal\" - by (cases x) auto +lemma ereal_infinity_cases: + fixes a :: ereal + shows "a \ \ \ a \ -\ \ \a\ \ \" + by auto -lemma ereal_infinity_cases: "(a::ereal) \ \ \ a \ -\ \ \a\ \ \" - 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)" | -"\ + a = (\::ereal)" | -"a + \ = (\::ereal)" | -"ereal r + -\ = - \" | -"-\ + ereal p = -(\::ereal)" | -"-\ + -\ = -(\::ereal)" + "ereal r + ereal p = ereal (r + p)" +| "\ + a = (\::ereal)" +| "a + \ = (\::ereal)" +| "ereal r + -\ = - \" +| "-\ + ereal p = -(\::ereal)" +| "-\ + -\ = -(\::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]: "\0\ = (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 \ a = 0" + fixes a :: ereal + shows "-a = 0 \ a = 0" by (cases a) simp_all lemma ereal_plus_eq_PInfty[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_plus_eq_MInfty[simp]: - fixes a b :: ereal shows "a + b = -\ \ - (a = -\ \ b = -\) \ a \ \ \ b \ \" + fixes a b :: ereal + shows "a + b = -\ \ (a = -\ \ b = -\) \ a \ \ \ b \ \" by (cases rule: ereal2_cases[of a b]) auto lemma ereal_add_cancel_left: - fixes a b :: ereal assumes "a \ -\" - shows "a + b = a + c \ (a = \ \ b = c)" + fixes a b :: ereal + assumes "a \ -\" + shows "a + b = a + c \ a = \ \ 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 \ -\" - shows "b + a = c + a \ (a = \ \ b = c)" + fixes a b :: ereal + assumes "a \ -\" + shows "b + a = c + a \ a = \ \ b = c" using assms by (cases rule: ereal3_cases[of a b c]) auto -lemma ereal_real: - "ereal (real x) = (if \x\ = \ then 0 else x)" +lemma ereal_real: "ereal (real x) = (if \x\ = \ then 0 else x)" by (cases x) simp_all lemma real_of_ereal_add: @@ -219,6 +248,7 @@ (if (\a\ = \) \ (\b\ = \) \ (\a\ \ \) \ (\b\ \ \) 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 "\ \ x \ x = \" - "x \ -\ \ x = -\" + and "x \ -\ \ x = -\" 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 \ y \ y \ x " by (cases rule: ereal2_cases[of x y]) auto - { assume "x \ y" "y \ x" then show "x = y" - by (cases rule: ereal2_cases[of x y]) auto } - { assume "x \ y" "y \ z" then show "x \ z" - by (cases rule: ereal3_cases[of x y z]) auto } + { + assume "x \ y" "y \ x" + then show "x = y" + by (cases rule: ereal2_cases[of x y]) auto + } + { + assume "x \ y" "y \ z" + then show "x \ 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 \ b" then show "c + a \ c + b" + fix a b c :: ereal + assume "a \ b" + then show "c + a \ c + b" by (cases rule: ereal3_cases[of a b c]) auto qed lemma real_of_ereal_positive_mono: - fixes x y :: ereal shows "\0 \ x; x \ y; y \ \\ \ real x \ real y" + fixes x y :: ereal + shows "0 \ x \ x \ y \ y \ \ \ real x \ real y" by (cases rule: ereal2_cases[of x y]) auto lemma ereal_MInfty_lessI[intro, simp]: - fixes a :: ereal shows "a \ -\ \ -\ < a" + fixes a :: ereal + shows "a \ -\ \ -\ < a" by (cases a) auto lemma ereal_less_PInfty[intro, simp]: - fixes a :: ereal shows "a \ \ \ a < \" + fixes a :: ereal + shows "a \ \ \ a < \" by (cases a) auto lemma ereal_less_ereal_Ex: @@ -321,12 +362,16 @@ lemma less_PInf_Ex_of_nat: "x \ \ \ (\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 \ b" "c \ d" shows "a + c \ b + d" + fixes a b c d :: ereal + assumes "a \ b" + and "c \ d" + shows "a + c \ 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 \ - b \ b \ a" + fixes a b :: ereal + shows "- a \ - b \ b \ a" by (cases rule: ereal2_cases[of a b]) auto lemma ereal_minus_less_minus[simp]: - fixes a b :: ereal shows "- a < - b \ b < a" + fixes a b :: ereal + shows "- a < - b \ b < a" by (cases rule: ereal2_cases[of a b]) auto lemma ereal_le_real_iff: - "x \ real y \ ((\y\ \ \ \ ereal x \ y) \ (\y\ = \ \ x \ 0))" + "x \ real y \ (\y\ \ \ \ ereal x \ y) \ (\y\ = \ \ x \ 0)" by (cases y) auto lemma real_le_ereal_iff: - "real y \ x \ ((\y\ \ \ \ y \ ereal x) \ (\y\ = \ \ 0 \ x))" + "real y \ x \ (\y\ \ \ \ y \ ereal x) \ (\y\ = \ \ 0 \ x)" by (cases y) auto lemma ereal_less_real_iff: - "x < real y \ ((\y\ \ \ \ ereal x < y) \ (\y\ = \ \ x < 0))" + "x < real y \ (\y\ \ \ \ ereal x < y) \ (\y\ = \ \ x < 0)" by (cases y) auto lemma real_less_ereal_iff: - "real y < x \ ((\y\ \ \ \ y < ereal x) \ (\y\ = \ \ 0 < x))" + "real y < x \ (\y\ \ \ \ y < ereal x) \ (\y\ = \ \ 0 < x)" by (cases y) auto lemma real_of_ereal_pos: - fixes x :: ereal shows "0 \ x \ 0 \ real x" by (cases x) auto + fixes x :: ereal + shows "0 \ x \ 0 \ 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 \ \x :: ereal\" by (cases x) auto -lemma real_of_ereal_le_0[simp]: "real (x :: ereal) \ 0 \ (x \ 0 \ x = \)" +lemma real_of_ereal_le_0[simp]: "real (x :: ereal) \ 0 \ x \ 0 \ x = \" by (cases x) auto lemma abs_real_of_ereal[simp]: "\real (x :: ereal)\ = real \x\" by (cases x) auto lemma zero_less_real_of_ereal: - fixes x :: ereal shows "0 < real x \ (0 < x \ x \ \)" + fixes x :: ereal + shows "0 < real x \ 0 < x \ x \ \" by (cases x) auto lemma ereal_0_le_uminus_iff[simp]: - fixes a :: ereal shows "0 \ -a \ a \ 0" + fixes a :: ereal + shows "0 \ - a \ a \ 0" by (cases rule: ereal2_cases[of a]) auto lemma ereal_uminus_le_0_iff[simp]: - fixes a :: ereal shows "-a \ 0 \ 0 \ a" + fixes a :: ereal + shows "- a \ 0 \ 0 \ a" by (cases rule: ereal2_cases[of a]) auto lemma ereal_add_strict_mono: fixes a b c d :: ereal - assumes "a = b" "0 \ a" "a \ \" "c < d" + assumes "a = b" + and "0 \ a" + and "a \ \" + 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 "\a\ \ \ \ c < b \ a + c < a + b" +lemma ereal_less_add: + fixes a b c :: ereal + shows "\a\ \ \ \ c < b \ a + c < a + b" by (cases rule: ereal2_cases[of b c]) auto -lemma ereal_uminus_eq_reorder: "- a = b \ a = (-b::ereal)" by auto +lemma ereal_uminus_eq_reorder: "- a = b \ a = (-b::ereal)" + by auto lemma ereal_uminus_less_reorder: "- a < b \ -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 "\B. x \ ereal B" shows "x = - \" + fixes x :: ereal + assumes "\B. x \ ereal B" + shows "x = - \" 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 "\B. x \ ereal B" shows "x = \" + fixes x :: ereal + assumes "\B. x \ ereal B" + shows "x = \" 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 \ a \ 0 \ b \ 0 \ a + b" + fixes a b :: ereal + shows "0 \ a \ 0 \ b \ 0 \ a + b" using add_mono[of 0 a 0 b] by simp -lemma image_eqD: "f ` A = B \ (\x\A. f x \ B)" +lemma image_eqD: "f ` A = B \ \x\A. f x \ B" by auto lemma incseq_setsumI: - fixes f :: "nat \ 'a::{comm_monoid_add, ordered_ab_semigroup_add}" + fixes f :: "nat \ 'a::{comm_monoid_add,ordered_ab_semigroup_add}" assumes "\i. 0 \ f i" shows "incseq (\i. setsum f {..< i})" proof (intro incseq_SucI) - fix n have "setsum f {..< n} + 0 \ setsum f {.. setsum f {.. setsum f {..< Suc n}" by auto qed lemma incseq_setsumI2: - fixes f :: "'i \ nat \ 'a::{comm_monoid_add, ordered_ab_semigroup_add}" + fixes f :: "'i \ nat \ 'a::{comm_monoid_add,ordered_ab_semigroup_add}" assumes "\n. n \ A \ incseq (f n)" shows "incseq (\i. \n\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 \ ereal" where @@ -482,28 +559,31 @@ | "sgn (\::ereal) = 1" | "sgn (-\::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 * \ = (if r = 0 then 0 else if r > 0 then \ else -\)" | -"\ * ereal r = (if r = 0 then 0 else if r > 0 then \ else -\)" | -"ereal r * -\ = (if r = 0 then 0 else if r > 0 then -\ else \)" | -"-\ * ereal r = (if r = 0 then 0 else if r > 0 then -\ else \)" | -"(\::ereal) * \ = \" | -"-(\::ereal) * \ = -\" | -"(\::ereal) * -\ = -\" | -"-(\::ereal) * -\ = \" + "ereal r * ereal p = ereal (r * p)" +| "ereal r * \ = (if r = 0 then 0 else if r > 0 then \ else -\)" +| "\ * ereal r = (if r = 0 then 0 else if r > 0 then \ else -\)" +| "ereal r * -\ = (if r = 0 then 0 else if r > 0 then -\ else \)" +| "-\ * ereal r = (if r = 0 then 0 else if r > 0 then -\ else \)" +| "(\::ereal) * \ = \" +| "-(\::ereal) * \ = -\" +| "(\::ereal) * -\ = -\" +| "-(\::ereal) * -\ = \" 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 \ 1 \ real a \ 1" + fixes a :: ereal + shows "a \ 1 \ real a \ 1" by (cases a) (auto simp: one_ereal_def) lemma abs_ereal_one[simp]: "\1\ = (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 \ (0::ereal)" +lemma ereal_zero_m1[simp]: "1 \ (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 + -(\::ereal) = -\" "-(\::ereal) + 1 = -\" + "1 + ereal r = ereal (r + 1)" + "ereal r + 1 = ereal (r + 1)" + "1 + -(\::ereal) = -\" + "-(\::ereal) + 1 = -\" unfolding one_ereal_def by auto lemma ereal_zero_times[simp]: - fixes a b :: ereal shows "a * b = 0 \ a = 0 \ b = 0" + fixes a b :: ereal + shows "a * b = 0 \ a = 0 \ b = 0" by (cases rule: ereal2_cases[of a b]) auto lemma ereal_mult_eq_PInfty[simp]: - shows "a * b = (\::ereal) \ + "a * b = (\::ereal) \ (a = \ \ b > 0) \ (a > 0 \ b = \) \ (a = -\ \ b < 0) \ (a < 0 \ b = -\)" by (cases rule: ereal2_cases[of a b]) auto lemma ereal_mult_eq_MInfty[simp]: - shows "a * b = -(\::ereal) \ + "a * b = -(\::ereal) \ (a = \ \ b < 0) \ (a < 0 \ b = \) \ (a = -\ \ b > 0) \ (a > 0 \ b = -\)" 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 < (\::ereal)" + assumes "a < b" + and "0 < c" + and "c < (\::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: - "\ a < b ; 0 < c ; c < (\::ereal)\ \ c * a < c * b" - using ereal_mult_strict_right_mono by (simp add: mult_commute[of c]) + "a < b \ 0 < c \ c < (\::ereal) \ 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 "\a \ b; 0 \ c\ \ a*c \ b*c" + fixes a b c :: ereal + shows "a \ b \ 0 \ c \ a * c \ 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 "\a \ b; 0 \ c\ \ c * a \ c * b" - using ereal_mult_right_mono by (simp add: mult_commute[of c]) + fixes a b c :: ereal + shows "a \ b \ 0 \ c \ c * a \ c * b" + using ereal_mult_right_mono + by (simp add: mult_commute[of c]) lemma zero_less_one_ereal[simp]: "0 \ (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 \ a \ 0 \ b \ r * (a + b) = r * a + r * b" + fixes r a b :: ereal + shows "0 \ a \ 0 \ b \ 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 \ a \ 0 \ b \ (a + b) * r = a * r + b * r" + fixes r a b :: ereal + shows "0 \ a \ 0 \ b \ (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 \ \ \ b \ -\" "a \ -\ \ b \ \" "\c\ \ \" + assumes "a \ \ \ b \ -\" + and "a \ -\ \ b \ \" + and "\c\ \ \" 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=(-\)" hence ?thesis by auto } + assumes "\e. 0 < e \ x \ y + e" + shows "x \ y" +proof - + { + assume a: "\r. y = ereal r" + then obtain r where r_def: "y = ereal r" + by auto + { + assume "x = -\" + then have ?thesis by auto + } + moreover + { + assume "x \ -\" + 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 + } + then have "p \ 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=(-\))" - 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=(-\) | y=\" hence ?thesis - using assms[rule_format, of 1] by (cases x) auto -} ultimately show ?thesis by (cases y) auto + { + assume "y = -\ | y = \" + 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=\" hence "x<=y+e" by auto } - moreover - { assume "e~=\" - 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 "\e. 0 < e \ x \ y + ereal e" + shows "x \ y" +proof - + { + fix e :: ereal + assume "e > 0" + { + assume "e = \" + then have "x \ y + e" + by auto + } + moreover + { + assume "e \ \" + then obtain r where "e = ereal r" + using `e > 0` by (cases e) auto + then have "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 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 "\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) lemma setprod_ereal_0: fixes f :: "'a \ ereal" - shows "(\i\A. f i) = 0 \ (finite A \ (\i\A. f i = 0))" -proof cases - assume "finite A" + shows "(\i\A. f i) = 0 \ finite A \ (\i\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 \ ereal" assumes pos: "\i. i \ I \ 0 \ f i" shows "0 \ (\i\I. f i)" -proof cases - assume "finite I" from this pos show ?thesis by induct auto -qed simp + fixes f :: "'a \ ereal" + assumes pos: "\i. i \ I \ 0 \ f i" + shows "0 \ (\i\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 \ ereal" assumes "\i. i \ I \ 0 \ f i" shows "(\i\I. f i) = \ \ finite I \ (\i\I. f i = \) \ (\i\I. f i \ 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 \ f i" "0 \ setprod f I" by (auto intro!: setprod_ereal_pos) - from insert have "(\j\insert i I. f j) = \ \ setprod f I * f i = \" by auto + then have pos: "0 \ f i" "0 \ setprod f I" + by (auto intro!: setprod_ereal_pos) + from insert have "(\j\insert i I. f j) = \ \ setprod f I * f i = \" + by auto also have "\ \ (setprod f I = \ \ f i = \) \ f i \ 0 \ setprod f I \ 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: "(\i\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 \ a" + fixes a :: ereal + assumes "0 \ a" shows "0 \ 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 ` {..x\ = \ then \ else 0::ereal)" +lemma ereal_x_minus_x[simp]: "x - x = (if \x\ = \ then \ 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 \ z - y \ - (y = \ \ z \ \ \ x = -\) \ - (\y\ \ \ \ x + y \ z)" + shows "x \ z - y \ (y = \ \ z \ \ \ x = -\) \ (\y\ \ \ \ x + y \ 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 \ - y \ -\ \ (y = \ \ x \ \ \ z \ -\) \ - (y \ \ \ x < z + y)" + shows "x - y < z \ y \ -\ \ (y = \ \ x \ \ \ z \ -\) \ (y \ \ \ 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 "\x\ \ \" "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 "\x\ \ \" + 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 = \ \ y = -\ \ x = \" + fixes x y :: ereal + shows "x - y = \ \ y = -\ \ x = \" 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 \ else ereal (inverse r))" | -"inverse (\::ereal) = 0" | -"inverse (-\::ereal) = 0" + "inverse (ereal r) = (if r = 0 then \ else ereal (inverse r))" +| "inverse (\::ereal) = 0" +| "inverse (-\::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 \x\ = \ \ 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 \x\ = \ \ 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 \ -\ then x else \)" + fixes x :: ereal + shows "inverse (inverse x) = (if x \ -\ then x else \)" by (cases x) auto lemma ereal_inverse_minus[simp]: - fixes x :: ereal shows "inverse (- x) = (if x = 0 then \ else -inverse x)" + fixes x :: ereal + shows "inverse (- x) = (if x = 0 then \ 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 / \ = 0" "x / -\ = 0" + fixes x :: ereal + shows "x / \ = 0" "x / -\ = 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]: - "\ / ereal r = (if 0 \ r then \ else -\)" +lemma ereal_divide_ereal[simp]: "\ / ereal r = (if 0 \ r then \ else -\)" unfolding divide_ereal_def by simp lemma zero_le_divide_ereal[simp]: - fixes a :: ereal assumes "0 \ a" "0 \ b" + fixes a :: ereal + assumes "0 \ a" + and "0 \ b" shows "0 \ 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 \ x \ \ \ y \ z / x \ x * y \ z" + fixes x y z :: ereal + shows "x > 0 \ x \ \ \ y \ z / x \ x * y \ 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 \ x \ \ \ z / x \ y \ z \ x * y" + fixes x y z :: ereal + shows "x > 0 \ x \ \ \ z / x \ y \ z \ 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 \ x \ -\ \ y \ z / x \ z \ x * y" + fixes x y z :: ereal + shows "x < 0 \ x \ -\ \ y \ z / x \ z \ 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 \ x \ -\ \ z / x \ y \ x * y \ z" + fixes x y z :: ereal + shows "x < 0 \ x \ -\ \ z / x \ y \ x * y \ 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 \ x \ x <= y \ inverse y <= inverse x" + shows "0 \ x \ x \ y \ inverse y \ inverse x" by (cases rule: ereal2_cases[of x y]) auto lemma inverse_inverse_Pinfty_iff[simp]: - fixes x :: ereal shows "inverse x = \ \ x = 0" + fixes x :: ereal + shows "inverse x = \ \ x = 0" by (cases x) auto lemma ereal_inverse_eq_0: - fixes x :: ereal shows "inverse x = 0 \ x = \ \ x = -\" + fixes x :: ereal + shows "inverse x = 0 \ x = \ \ x = -\" by (cases x) auto lemma ereal_0_gt_inverse: - fixes x :: ereal shows "0 < inverse x \ x \ \ \ 0 \ x" + fixes x :: ereal + shows "0 < inverse x \ x \ \ \ 0 \ x" by (cases x) auto lemma ereal_mult_less_right: fixes a b c :: ereal - assumes "b * a < c * a" "0 < a" "a < \" + assumes "b * a < c * a" + and "0 < a" + and "a < \" 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 \ 0 \ (x / y) ^ n = x^n / y^n" + fixes x y :: ereal + shows "y \ 0 \ (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 \ -\" - assumes z: "\z. \ 0 < z ; z < 1 \ \ z * x \ y" + assumes z: "\z. 0 < z \ z < 1 \ z * x \ y" shows "x \ y" proof (cases x) - case PInf with z[of "1 / 2"] show "x \ y" by (simp add: one_ereal_def) + case PInf + with z[of "1 / 2"] show "x \ y" + by (simp add: one_ereal_def) next - case (real r) note r = this + case (real r) + note r = this show "x \ y" proof (cases y) - case (real p) note p = this + case (real p) + note p = this have "r \ 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 \ 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 \ p" + using p r by (auto simp: zero_le_mult_iff one_ereal_def) qed - then show "x \ y" using p r by simp + then show "x \ 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 \ y" "0 < z" shows "x / z \ y / z" -using assms by (cases x y z rule: ereal3_cases) (auto intro: divide_right_mono) + assumes "x \ y" + and "0 < z" + shows "x / z \ 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 \ x" "0 < z" "0 < x * y" + assumes "y \ x" + and "0 < z" + and "0 < x * y" shows "z / x \ 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 "\x. (\y\S. y \ x) \ (\z. (\y\S. y \ z) \ x \ z)" -proof cases - assume "\x. \a\S. a \ ereal x" - then obtain y where y: "\a. a\S \ a \ ereal y" by auto - then have "\ \ S" by force +proof (cases "\x. \a\S. a \ ereal x") + case True + then obtain y where y: "\a. a\S \ a \ ereal y" + by auto + then have "\ \ S" + by force show ?thesis - proof cases - assume "S \ {-\} \ S \ {}" - with `\ \ S` obtain x where x: "x \ S" "\x\ \ \" by auto + proof (cases "S \ {-\} \ S \ {}") + case True + with `\ \ S` obtain x where x: "x \ S" "\x\ \ \" + by auto obtain s where s: "\x\ereal -` S. x \ s" "\z. (\x\ereal -` S. x \ z) \ s \ z" proof (atomize_elim, rule complete_real) - show "\x. x \ ereal -` S" using x by auto - show "\z. \x\ereal -` S. x \ z" by (auto dest: y intro!: exI[of _ y]) + show "\x. x \ ereal -` S" + using x by auto + show "\z. \x\ereal -` S. x \ z" + by (auto dest: y intro!: exI[of _ y]) qed show ?thesis proof (safe intro!: exI[of _ "ereal s"]) - fix y assume "y \ S" with s `\ \ S` show "y \ ereal s" + fix y + assume "y \ S" + with s `\ \ S` show "y \ ereal s" by (cases y) auto next - fix z assume "\y\S. y \ z" with `S \ {-\} \ S \ {}` show "ereal s \ z" + fix z + assume "\y\S. y \ z" + with `S \ {-\} \ S \ {}` show "ereal s \ z" by (cases z) (auto intro!: s) qed - qed (auto intro!: exI[of _ "-\"]) -qed (fastforce intro!: exI[of _ \] ereal_top intro: order_trans dest: less_imp_le simp: not_le) + next + case False + then show ?thesis + by (auto intro!: exI[of _ "-\"]) + qed +next + case False + then show ?thesis + by (fastforce intro!: exI[of _ \] 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: "\x. (\y\S::ereal set. x \ y) \ (\z. (\y\S. z \ y) \ z \ 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 \ 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 \ ereal" + shows "(INF i : R. - f i) = - (SUP i : R. f i)" using ereal_SUPR_uminus[of _ "\x. - f x"] by simp lemma ereal_image_uminus_shift: - fixes X Y :: "ereal set" shows "uminus ` X = Y \ X = uminus ` Y" + fixes X Y :: "ereal set" + shows "uminus ` X = Y \ 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 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 "(\x. x \ X \ z \ x) \ (\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) lemma Sup_eq_MInfty: - fixes S :: "ereal set" shows "Sup S = -\ \ S = {} \ S = {-\}" + fixes S :: "ereal set" + shows "Sup S = -\ \ S = {} \ S = {-\}" unfolding bot_ereal_def[symmetric] by auto lemma Inf_eq_PInfty: - fixes S :: "ereal set" shows "Inf S = \ \ S = {} \ S = {\}" + fixes S :: "ereal set" + shows "Inf S = \ \ S = {} \ S = {\}" 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 "-\ \ S \ Inf S = -\" +lemma Inf_eq_MInfty: + fixes S :: "ereal set" + shows "-\ \ S \ Inf S = -\" unfolding bot_ereal_def[symmetric] by auto lemma Sup_eq_PInfty: - fixes S :: "ereal set" shows "\ \ S \ Sup S = \" + fixes S :: "ereal set" + shows "\ \ S \ Sup S = \" unfolding top_ereal_def[symmetric] by auto lemma Sup_ereal_close: fixes e :: ereal - assumes "0 < e" and S: "\Sup S\ \ \" "S \ {}" + assumes "0 < e" + and S: "\Sup S\ \ \" "S \ {}" shows "\x\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 "\Inf X\ \ \" "0 < e" + fixes e :: ereal + assumes "\Inf X\ \ \" + and "0 < e" shows "\x\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)) = \" proof - - { fix x ::ereal assume "x \ \" + { + fix x :: ereal + assume "x \ \" then have "\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 "\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 "\i. i \ A \ f i \ x" +proof (rule ccontr) + assume "\ ?thesis" + then have "\i\A. f i > x" + by auto + then have "(INF i:A. f i) \ x" + by (subst INF_greatest) auto + then show False + using assms by auto qed lemma SUP_ereal_le_addI: fixes f :: "'i \ ereal" - assumes "\i. f i + y \ z" and "y \ -\" + assumes "\i. f i + y \ z" + and "y \ -\" shows "SUPR UNIV f + y \ z" proof (cases y) case (real r) - then have "\i. f i \ z - y" using assms by (simp add: ereal_le_minus_iff) - then have "SUPR UNIV f \ z - y" by (rule SUP_least) - then show ?thesis using real by (simp add: ereal_le_minus_iff) + then have "\i. f i \ z - y" + using assms by (simp add: ereal_le_minus_iff) + then have "SUPR UNIV f \ 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 \ ereal" - assumes "incseq f" "incseq g" and pos: "\i. f i \ -\" "\i. g i \ -\" + assumes "incseq f" + and "incseq g" + and pos: "\i. f i \ -\" "\i. g i \ -\" shows "(SUP i. f i + g i) = SUPR UNIV f + SUPR UNIV g" proof (rule SUP_eqI) - fix y assume *: "\i. i \ UNIV \ f i + g i \ y" - have f: "SUPR UNIV f \ -\" using pos - unfolding SUP_def Sup_eq_MInfty by (auto dest: image_eqD) - { fix j - { fix i + fix y + assume *: "\i. i \ UNIV \ f i + g i \ y" + have f: "SUPR UNIV f \ -\" + using pos + unfolding SUP_def Sup_eq_MInfty + by (auto dest: image_eqD) + { + fix j + { + fix i have "f i + g j \ 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 "\ \ 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 "\ \ y" using * by auto - finally have "f i + g j \ y" . } + finally have "f i + g j \ y" . + } then have "SUPR UNIV f + g j \ y" using assms(4)[of j] by (intro SUP_ereal_le_addI) auto - then have "g j + SUPR UNIV f \ y" by (simp add: ac_simps) } + then have "g j + SUPR UNIV f \ y" by (simp add: ac_simps) + } then have "SUPR UNIV g + SUPR UNIV f \ y" using f by (rule SUP_ereal_le_addI) - then show "SUPR UNIV f + SUPR UNIV g \ y" by (simp add: ac_simps) + then show "SUPR UNIV f + SUPR UNIV g \ y" + by (simp add: ac_simps) qed (auto intro!: add_mono SUP_upper) lemma SUPR_ereal_add_pos: fixes f g :: "nat \ ereal" - assumes inc: "incseq f" "incseq g" and pos: "\i. 0 \ f i" "\i. 0 \ g i" + assumes inc: "incseq f" "incseq g" + and pos: "\i. 0 \ f i" "\i. 0 \ 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 \ -\" "g i \ -\" using pos[of i] by auto + fix i + show "f i \ -\" "g i \ -\" + using pos[of i] by auto qed lemma SUPR_ereal_setsum: fixes f g :: "'a \ nat \ ereal" - assumes "\n. n \ A \ incseq (f n)" and pos: "\n i. n \ A \ 0 \ f n i" + assumes "\n. n \ A \ incseq (f n)" + and pos: "\n i. n \ A \ 0 \ f n i" shows "(SUP i. \n\A. f n i) = (\n\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 \ ereal" assumes "\i. 0 \ f i" "0 \ c" + fixes f :: "nat \ ereal" + assumes "\i. 0 \ f i" + and "0 \ c" shows "(SUP i. c * f i) = c * SUPR UNIV f" proof (rule SUP_eqI) - fix i have "f i \ SUPR UNIV f" by (rule SUP_upper) auto + fix i + have "f i \ SUPR UNIV f" + by (rule SUP_upper) auto then show "c * f i \ c * SUPR UNIV f" using `0 \ c` by (rule ereal_mult_left_mono) next - fix y assume *: "\i. i \ UNIV \ c * f i \ y" + fix y + assume *: "\i. i \ UNIV \ c * f i \ y" show "c * SUPR UNIV f \ y" - proof cases - assume c: "0 < c \ c \ \" + proof (cases "0 < c \ c \ \") + case True with * have "SUPR UNIV f \ 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 = \" have ?thesis - proof cases - assume **: "\i. f i = 0" - then have "range f = {0}" by auto - with ** show "c * SUPR UNIV f \ y" using * - by (auto simp: SUP_def min_max.sup_absorb1) + case False + { + assume "c = \" + have ?thesis + proof (cases "\i. f i = 0") + case True + then have "range f = {0}" + by auto + with True show "c * SUPR UNIV f \ y" + using * by (auto simp: SUP_def min_max.sup_absorb1) next - assume "\ (\i. f i = 0)" - then obtain i where "f i \ 0" by auto - with *[of i] `c = \` `0 \ f i` show ?thesis by (auto split: split_if_asm) - qed } - moreover assume "\ (0 < c \ c \ \)" - ultimately show ?thesis using * `0 \ c` by auto + case False + then obtain i where "f i \ 0" + by auto + with *[of i] `c = \` `0 \ f i` show ?thesis + by (auto split: split_if_asm) + qed + } + moreover note False + ultimately show ?thesis + using * `0 \ 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 \ \" + fix x :: ereal + assume "x \ \" show "\i\A. x < f i" proof (cases x) - case PInf with `x \ \` show ?thesis by simp + case PInf + with `x \ \` 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 \ A" "ereal (real n) \ f i" using assms .. ultimately show ?thesis @@ -1382,7 +1653,8 @@ case (real r) have "\n::nat. \x. x \ A \ Sup A < x + 1 / ereal (real n)" proof - fix n ::nat have "\x\A. Sup A - 1 / ereal (real n) < x" + fix n :: nat + have "\x\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 \ A" "Sup A - 1 / ereal (real n) < x" .. then show "\x. x \ A \ Sup A < x + 1 / ereal (real n)" @@ -1392,48 +1664,63 @@ where f: "\x. f x \ A \ Sup A < f x + 1 / ereal (real x)" .. have "SUPR UNIV f = Sup A" proof (rule SUP_eqI) - fix i show "f i \ Sup A" using f - by (auto intro!: complete_lattice_class.Sup_upper) + fix i + show "f i \ Sup A" + using f by (auto intro!: complete_lattice_class.Sup_upper) next - fix y assume bound: "\i. i \ UNIV \ f i \ y" + fix y + assume bound: "\i. i \ UNIV \ f i \ y" show "Sup A \ y" proof (rule ereal_le_epsilon, intro allI impI) - fix e :: ereal assume "0 < e" + fix e :: ereal + assume "0 < e" show "Sup A \ 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 \ 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 \ f n + 1 / ereal (real n)" + using f[THEN spec, of n] by auto - also have "1 / ereal (real n) \ e" using real * by (auto simp: one_ereal_def ) - with bound have "f n + 1 / ereal (real n) \ y + e" by (rule add_mono) simp + also have "1 / ereal (real n) \ e" + using real * + by (auto simp: one_ereal_def ) + with bound have "f n + 1 / ereal (real n) \ y + e" + by (rule add_mono) simp finally show "Sup A \ 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 \ {}` obtain x where "x \ A" by auto + from `A \ {}` obtain x where "x \ A" + by auto show ?thesis - proof cases - assume *: "\ \ A" - then have "\ \ Sup A" by (intro complete_lattice_class.Sup_upper) - with * show ?thesis by (auto intro!: exI[of _ "\x. \"]) + proof (cases "\ \ A") + case True + then have "\ \ Sup A" + by (intro complete_lattice_class.Sup_upper) + with True show ?thesis + by (auto intro!: exI[of _ "\x. \"]) next - assume "\ \ A" + case False have "\x\A. 0 \ x" - by (metis Infty_neq_0 PInf complete_lattice_class.Sup_least ereal_infty_less_eq2 linorder_linear) - then obtain x where "x \ A" "0 \ 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 \ A" and "0 \ x" + by auto have "\n::nat. \f. f \ A \ x + ereal (real n) \ f" proof (rule ccontr) assume "\ ?thesis" then have "\n::nat. Sup A \ 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 \ A` `\ \ A` PInf - by(cases x) auto + by (cases x) auto qed from choice[OF this] obtain f :: "nat \ ereal" where f: "\z. f z \ A \ x + ereal (real z) \ f z" .. @@ -1444,20 +1731,26 @@ using f[THEN spec, of n] `0 \ 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 \ {}` have "A = {-\}" by (auto simp: Sup_eq_MInfty) - then show ?thesis using MInf by (auto intro!: exI[of _ "\x. -\"]) + with `A \ {}` have "A = {-\}" + by (auto simp: Sup_eq_MInfty) + then show ?thesis + using MInf by (auto intro!: exI[of _ "\x. -\"]) qed lemma SUPR_countable_SUPR: "A \ {} \ \f::nat \ ereal. range f \ g`A \ 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 \ {}" and "a \ -\" + fixes A :: "ereal set" + assumes "A \ {}" + and "a \ -\" shows "Sup ((\x. a + x) ` A) = a + Sup A" proof (rule antisym) have *: "\a::ereal. \A. Sup ((\x. a + x) ` A) \ a + Sup A" @@ -1465,37 +1758,46 @@ then show "Sup ((\x. a + x) ` A) \ a + Sup A" . show "a + Sup A \ Sup ((\x. a + x) ` A)" proof (cases a) - case PInf with `A \ {}` show ?thesis by (auto simp: image_constant min_max.sup_absorb1) + case PInf with `A \ {}` + 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" "(\x. a + x) ` A"] real show ?thesis unfolding ** + from *[of "-a" "(\x. a + x) ` A"] real show ?thesis + unfolding ** by (cases rule: ereal2_cases[of "Sup A" "Sup (op + a ` A)"]) auto qed (insert `a \ -\`, auto) qed lemma Sup_ereal_cminus: - fixes A :: "ereal set" assumes "A \ {}" and "a \ -\" + fixes A :: "ereal set" + assumes "A \ {}" + and "a \ -\" shows "Sup ((\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 \ ereal" - fixes A assumes "A \ {}" and "a \ -\" + fixes A + assumes "A \ {}" + and "a \ -\" 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 \ {}" and "\a\ \ \" + fixes A :: "ereal set" + assumes "A \ {}" + and "\a\ \ \" shows "Inf ((\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 "(\x. -a - x)`uminus`A = uminus ` (\x. a - x) ` A" by (auto simp: image_image) @@ -1505,25 +1807,32 @@ qed lemma INFI_ereal_cminus: - fixes a :: ereal assumes "A \ {}" and "\a\ \ \" + fixes a :: ereal + assumes "A \ {}" + and "\a\ \ \" 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 \ \ \ b \ \ \ - (- a + - b) = a + b" + fixes a b :: ereal + shows "a \ \ \ b \ \ \ - (- a + - b) = a + b" by (cases rule: ereal2_cases[of a b]) auto lemma INFI_ereal_add: fixes f :: "nat \ ereal" - assumes "decseq f" "decseq g" and fin: "\i. f i \ \" "\i. g i \ \" + assumes "decseq f" "decseq g" + and fin: "\i. f i \ \" "\i. g i \ \" shows "(INF i. f i + g i) = INFI UNIV f + INFI UNIV g" proof - have INF_less: "(INF i. f i) < \" "(INF i. g i) < \" 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 "\ = 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 \ ereal (real n) | \ \ \)" @@ -1546,50 +1856,41 @@ "ereal_of_enat \ = \" by (simp_all add: ereal_of_enat_def) -lemma ereal_of_enat_le_iff[simp]: - "ereal_of_enat m \ ereal_of_enat n \ m \ n" -by (cases m n rule: enat2_cases) auto +lemma ereal_of_enat_le_iff[simp]: "ereal_of_enat m \ ereal_of_enat n \ 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 \ 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 \ m < n" + by (cases m n rule: enat2_cases) auto -lemma numeral_le_ereal_of_enat_iff[simp]: - shows "numeral m \ ereal_of_enat n \ numeral m \ n" -by (cases n) (auto dest: natceiling_le intro: natceiling_le_eq[THEN iffD1]) +lemma numeral_le_ereal_of_enat_iff[simp]: "numeral m \ ereal_of_enat n \ numeral m \ 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 \ 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 \ numeral m < n" + by (cases n) (auto simp: real_of_nat_less_iff[symmetric]) -lemma ereal_of_enat_ge_zero_cancel_iff[simp]: - "0 \ ereal_of_enat n \ 0 \ n" -by (cases n) (auto simp: enat_0[symmetric]) +lemma ereal_of_enat_ge_zero_cancel_iff[simp]: "0 \ ereal_of_enat n \ 0 \ n" + by (cases n) (auto simp: enat_0[symmetric]) -lemma ereal_of_enat_gt_zero_cancel_iff[simp]: - "0 < ereal_of_enat n \ 0 < n" -by (cases n) (auto simp: enat_0[symmetric]) +lemma ereal_of_enat_gt_zero_cancel_iff[simp]: "0 < ereal_of_enat n \ 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 = \ \ n = \" +lemma ereal_of_enat_inf[simp]: "ereal_of_enat n = \ \ n = \" 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 \ 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 \ 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 \ \ \ A \ (\x. {ereal x<..} \ A)" @@ -1618,8 +1920,13 @@ with Int show ?case by (intro exI[of _ "max x z"]) fastforce next - { fix x have "x \ \ \ \t. x \ ereal t" by (cases x) auto } - moreover case (Basis S) + case (Basis S) + { + fix x + have "x \ \ \ \t. x \ 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 \ - \ \ \t. ereal t \ x" by (cases x) auto } - moreover case (Basis S) + case (Basis S) + { + fix x + have "x \ - \ \ \t. ereal t \ 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 \ 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 -` {.. UNIV | MInfty \ {} | ereal r \ {.. {} | MInfty \ UNIV | ereal r \ {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} = { -\ <..< ereal x }" by auto (case_tac xa, auto) } - moreover { fix x have "ereal ` {x <..} = { ereal x <..< \ }" by auto (case_tac xa, auto) } + moreover { + fix x + have "ereal ` {..< x} = { -\ <..< ereal x }" + apply auto + apply (case_tac xa) + apply auto + done + } + moreover { + fix x + have "ereal ` {x <..} = { ereal x <..< \ }" + 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 \ open (ereal -` A) \ (\ \ A \ (\x. {ereal x <..} \ A)) \ (-\ \ A \ (\x. {.. A))" +lemma open_ereal_def: + "open A \ open (ereal -` A) \ (\ \ A \ (\x. {ereal x <..} \ A)) \ (-\ \ A \ (\x. {.. A))" (is "open A \ ?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" "\ \ A" obtains x where "{ereal x<..} \ A" +lemma open_PInfty2: + assumes "open A" + and "\ \ A" + obtains x where "{ereal x<..} \ A" using open_PInfty[OF assms] by auto -lemma open_MInfty2: assumes "open A" "-\ \ A" obtains x where "{.. A" +lemma open_MInfty2: + assumes "open A" + and "-\ \ A" + obtains x where "{.. A" using open_MInfty[OF assms] by auto -lemma ereal_openE: assumes "open A" obtains x y where - "open (ereal -` A)" "\ \ A \ {ereal x<..} \ A" "-\ \ A \ {.. A" +lemma ereal_openE: + assumes "open A" + obtains x y where "open (ereal -` A)" + and "\ \ A \ {ereal x<..} \ A" + and "-\ \ A \ {.. 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 \ S" "\x\ \ \" - obtains e where "e>0" "{x-e <..< x+e} \ S" -proof- - from `open S` have "open (ereal -` S)" by (rule ereal_openE) - then obtain e where "0 < e" and e: "\y. dist y (real x) < e \ ereal y \ S" + assumes "open S" + and "x \ S" + and "\x\ \ \" + obtains e where "e > 0" and "{x-e <..< x+e} \ S" +proof - + from `open S` + have "open (ereal -` S)" + by (rule ereal_openE) + then obtain e where "e > 0" and e: "\y. dist y (real x) < e \ ereal y \ 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 \ {x - ereal e<.. {x - ereal e<.. S" using e[of t] by auto + by (cases y) (auto simp: dist_real_def) + then show "y \ S" + using e[of t] by auto qed qed lemma ereal_open_cont_interval2: fixes S :: "ereal set" - assumes "open S" "x \ S" and x: "\x\ \ \" - obtains a b where "a < x" "x < b" "{a <..< b} \ S" + assumes "open S" + and "x \ S" + and x: "\x\ \ \" + obtains a b where "a < x" and "x < b" and "{a <..< b} \ S" proof - obtain e where "0 < e" "{x - e<.. 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]: - "((\n. ereal (f n)) ---> ereal x) net \ (f ---> x) net" (is "?l = ?r") +lemma lim_ereal[simp]: "((\n. ereal (f n)) ---> ereal x) net \ (f ---> x) net" + (is "?l = ?r") proof (intro iffI topological_tendstoI) - fix S assume "?l" "open S" "x \ S" + fix S + assume "?l" and "open S" and "x \ S" then show "eventually (\x. f x \ 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 \ S" + fix S + assume "?r" and "open S" and "ereal x \ S" show "eventually (\x. ereal (f x) \ S) net" using `?r`[THEN topological_tendstoD, OF open_ereal_vimage, OF `open S`] - using `ereal x \ S` by auto + using `ereal x \ S` + by auto qed lemma lim_real_of_ereal[simp]: assumes lim: "(f ---> ereal x) net" shows "((\x. real (f x)) ---> x) net" proof (intro topological_tendstoI) - fix S assume "open S" "x \ S" + fix S + assume "open S" and "x \ S" then have S: "open S" "ereal x \ ereal ` S" by (simp_all add: inj_image_mem_iff) - have "\x. f x \ ereal ` S \ real (f x) \ S" by auto + have "\x. f x \ ereal ` S \ real (f x) \ S" + by auto from this lim[THEN topological_tendstoD, OF open_ereal, OF S] show "eventually (\x. real (f x) \ S) net" by (rule eventually_mono) @@ -1756,10 +2114,12 @@ lemma tendsto_PInfty: "(f ---> \) F \ (\r. eventually (\x. ereal r < f x) F)" proof - - { fix l :: ereal assume "\r. eventually (\x. ereal r < f x) F" - from this[THEN spec, of "real l"] - have "l \ \ \ eventually (\x. l < f x) F" - by (cases l) (auto elim: eventually_elim1) } + { + fix l :: ereal + assume "\r. eventually (\x. ereal r < f x) F" + from this[THEN spec, of "real l"] have "l \ \ \ eventually (\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 "{.. S" .. moreover assume "\r::real. eventually (\z. f z < r) F" - then have "eventually (\z. f z \ {..< B}) F" by auto - ultimately show "eventually (\z. f z \ S) F" by (auto elim!: eventually_elim1) + then have "eventually (\z. f z \ {..< B}) F" + by auto + ultimately show "eventually (\z. f z \ S) F" + by (auto elim!: eventually_elim1) next - fix x assume "\S. open S \ -\ \ S \ eventually (\x. f x \ S) F" - from this[rule_format, of "{..< ereal x}"] - show "eventually (\y. f y < ereal x) F" by auto + fix x + assume "\S. open S \ -\ \ S \ eventually (\x. f x \ S) F" + from this[rule_format, of "{..< ereal x}"] show "eventually (\y. f y < ereal x) F" + by auto qed lemma Lim_PInfty: "f ----> \ \ (\B. \N. \n\N. f n \ ereal B)" unfolding tendsto_PInfty eventually_sequentially proof safe - fix r assume "\r. \N. \n\N. ereal r \ f n" - then obtain N where "\n\N. ereal (r + 1) \ f n" by blast - moreover have "ereal r < ereal (r + 1)" by auto + fix r + assume "\r. \N. \n\N. ereal r \ f n" + then obtain N where "\n\N. ereal (r + 1) \ f n" + by blast + moreover have "ereal r < ereal (r + 1)" + by auto ultimately show "\N. \n\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 ----> -\ \ (\B. \N. \n\N. ereal B \ f n)" unfolding tendsto_MInfty eventually_sequentially proof safe - fix r assume "\r. \N. \n\N. f n \ ereal r" - then obtain N where "\n\N. f n \ ereal (r - 1)" by blast - moreover have "ereal (r - 1) < ereal r" by auto + fix r + assume "\r. \N. \n\N. f n \ ereal r" + then obtain N where "\n\N. f n \ ereal (r - 1)" + by blast + moreover have "ereal (r - 1) < ereal r" + by auto ultimately show "\N. \n\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 \ (\S. open S \ f0 \ S \ (\N. \n\N. f n \ S))" unfolding tendsto_def eventually_sequentially by auto -lemma Lim_bounded_PInfty2: - "f ----> l \ ALL n>=N. f n <= ereal B \ l ~= \" +lemma Lim_bounded_PInfty2: "f ----> l \ \n\N. f n \ ereal B \ l \ \" using LIMSEQ_le_const2[of f l "ereal B"] by fastforce -lemma Lim_bounded_ereal: "f ----> (l :: 'a::linorder_topology) \ ALL n>=M. f n <= C \ l<=C" +lemma Lim_bounded_ereal: "f ----> (l :: 'a::linorder_topology) \ \n\M. f n \ C \ l \ 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: "\n\N. f n \ C" + shows "l \ 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 \ x = \ \ x = -\ \ x = 0" + fixes x :: ereal + shows "real x = 0 \ x = \ \ x = -\ \ x = 0" by (cases x) auto lemma tendsto_ereal_realD: fixes f :: "'a \ ereal" - assumes "x \ 0" and tendsto: "((\x. ereal (real (f x))) ---> x) net" + assumes "x \ 0" + and tendsto: "((\x. ereal (real (f x))) ---> x) net" shows "(f ---> x) net" proof (intro topological_tendstoI) - fix S assume S: "open S" "x \ S" - with `x \ 0` have "open (S - {0})" "x \ S - {0}" by auto + fix S + assume S: "open S" "x \ S" + with `x \ 0` have "open (S - {0})" "x \ S - {0}" + by auto from tendsto[THEN topological_tendstoD, OF this] show "eventually (\x. f x \ S) net" by (rule eventually_rev_mp) (auto simp: ereal_real) @@ -1849,22 +2223,25 @@ assumes x: "\x\ \ \" and tendsto: "(f ---> x) net" shows "((\x. ereal (real (f x))) ---> x) net" proof (intro topological_tendstoI) - fix S assume "open S" "x \ S" - with x have "open (S - {\, -\})" "x \ S - {\, -\}" by auto + fix S + assume "open S" and "x \ S" + with x have "open (S - {\, -\})" "x \ S - {\, -\}" + by auto from tendsto[THEN topological_tendstoD, OF this] show "eventually (\x. ereal (real (f x)) \ 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 \ - ((\a\ = \ \ 0 < b * c) \ a = 0 \ 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 \ (\a\ = \ \ 0 < b * c) \ a = 0 \ 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 "\m\ \ \" "m \ 0" "\t\ \ \" + assumes "\m\ \ \" + and "m \ 0" + and "\t\ \ \" shows "inj_on (\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 "\x\ \ \" shows "ereal (real x) = x" +lemma ereal_real': + assumes "\x\ \ \" + 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 \ 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-{ \ , (-\ :: 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) \ c * a + c * b" + fixes a b c :: ereal + shows "c * (a + b) \ 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 \ c" "c \ \" 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 \ c" + and "c \ \" + 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 \ 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) -lemma ereal_max_mono: - "[| (a::ereal) <= b; c <= d |] ==> max a c <= max b d" +lemma ereal_max_mono: "(a::ereal) \ b \ c \ d \ max a c \ 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) \ x \ c \ x \ max a c \ x" by (metis sup_ereal_def sup_least) lemma ereal_LimI_finite: fixes x :: ereal assumes "\x\ \ \" - assumes "!!r. 0 < r ==> EX N. ALL n>=N. u n < x + r & x < u n + r" + and "\r. 0 < r \ \N. \n\N. u n < x + r \ 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 \ S` obtain r where "0 < r" and dist: "!!y. dist y rx < r ==> ereal y \ 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 \ S" + then have "open (ereal -` S)" + unfolding open_ereal_def by auto + with `x \ S` obtain r where "0 < r" and dist: "\y. dist y rx < r \ ereal y \ 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: "\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 "\N. \n\N. u n \ S" proof (safe intro!: exI[of _ n]) - fix N assume "n <= N" + fix N + assume "n \ N" from upper[OF this] lower[OF this] assms `0 < r` - have "u N ~: {\,(-\)}" 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 \ {\,(-\)}" + 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 \ N`] upper[OF `n \ 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 ~: {\, -\}` + from dist[OF this] show "u N \ S" + using `u N \ {\, -\}` 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 \ S" + obtains N where "\n\N. f n \ S" using assms using tendsto_def using tendsto_explicit[of f f0] assms by auto lemma ereal_LimI_finite_iff: fixes x :: ereal assumes "\x\ \ \" - 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 \ (\r. 0 < r \ (\N. \n\N. u n < x + r \ x < u n + r))" + (is "?lhs \ ?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 "\n\N. u n \ {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 "\N. \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 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 (\x. - (f x)) = -(Liminf net f)" + fixes f :: "'a \ ereal" + shows "Limsup net (\x. - (f x)) = - Liminf net f" unfolding Limsup_def Liminf_def ereal_SUPR_uminus ereal_INFI_uminus .. lemma liminf_bounded_iff: fixes x :: "nat \ ereal" - shows "C \ liminf x \ (\BN. \n\N. B < x n)" (is "?lhs <-> ?rhs") + shows "C \ liminf x \ (\BN. \n\N. B < x n)" + (is "?lhs \ ?rhs") unfolding le_Liminf_iff eventually_sequentially .. lemma @@ -2012,6 +2417,7 @@ and ereal_decseq_uminus[simp]: "decseq (\i. - X i) = incseq X" unfolding incseq_def decseq_def by auto + subsubsection {* Tests for code generator *} (* A small list of simple arithmetic expressions *) diff -r ac5b8687f1d9 -r b65b4e70a258 src/Pure/PIDE/query_operation.scala --- a/src/Pure/PIDE/query_operation.scala Wed Sep 25 15:49:09 2013 +0200 +++ b/src/Pure/PIDE/query_operation.scala Wed Sep 25 15:49:15 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 _ => diff -r ac5b8687f1d9 -r b65b4e70a258 src/Tools/jEdit/src/find_dockable.scala --- a/src/Tools/jEdit/src/find_dockable.scala Wed Sep 25 15:49:09 2013 +0200 +++ b/src/Tools/jEdit/src/find_dockable.scala Wed Sep 25 15:49:15 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) } } diff -r ac5b8687f1d9 -r b65b4e70a258 src/Tools/jEdit/src/sledgehammer_dockable.scala --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Wed Sep 25 15:49:09 2013 +0200 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Wed Sep 25 15:49:15 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) } }