--- a/src/HOL/Library/Extended_Real.thy Thu Mar 22 18:54:39 2012 +0100
+++ b/src/HOL/Library/Extended_Real.thy Thu Mar 22 21:43:26 2012 +0100
@@ -14,7 +14,7 @@
text {*
For more lemmas about the extended real numbers go to
- @{text "src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy"}
+ @{file "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy"}
*}
@@ -127,7 +127,7 @@
instantiation ereal :: number
begin
definition [simp]: "number_of x = ereal (number_of x)"
-instance proof qed
+instance ..
end
instantiation ereal :: abs
@@ -184,11 +184,12 @@
instance
proof
- fix a :: ereal show "0 + a = a"
+ fix a b c :: ereal
+ show "0 + a = a"
by (cases a) (simp_all add: zero_ereal_def)
- fix b :: ereal show "a + b = b + a"
+ show "a + b = b + a"
by (cases rule: ereal2_cases[of a b]) simp_all
- fix c :: ereal show "a + b + c = a + (b + c)"
+ show "a + b + c = a + (b + c)"
by (cases rule: ereal3_cases[of a b c]) simp_all
qed
end
@@ -232,7 +233,8 @@
lemma real_of_ereal_add:
fixes a b :: ereal
- shows "real (a + b) = (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)"
+ shows "real (a + b) =
+ (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}"
@@ -240,13 +242,14 @@
instantiation ereal :: linorder
begin
-function less_ereal where
-" ereal x < ereal y \<longleftrightarrow> x < y" |
-"(\<infinity>::ereal) < a \<longleftrightarrow> False" |
-" a < -(\<infinity>::ereal) \<longleftrightarrow> False" |
-"ereal x < \<infinity> \<longleftrightarrow> True" |
-" -\<infinity> < ereal r \<longleftrightarrow> True" |
-" -\<infinity> < (\<infinity>::ereal) \<longleftrightarrow> True"
+function less_ereal
+where
+ " ereal x < ereal y \<longleftrightarrow> x < y"
+| "(\<infinity>::ereal) < a \<longleftrightarrow> False"
+| " a < -(\<infinity>::ereal) \<longleftrightarrow> False"
+| "ereal x < \<infinity> \<longleftrightarrow> True"
+| " -\<infinity> < ereal r \<longleftrightarrow> True"
+| " -\<infinity> < (\<infinity>::ereal) \<longleftrightarrow> True"
proof -
case (goal1 P x)
moreover then obtain a b where "x = (a,b)" by (cases x) auto
@@ -290,17 +293,19 @@
instance
proof
- fix x :: ereal show "x \<le> x"
+ fix x y z :: ereal
+ show "x \<le> x"
by (cases x) simp_all
- fix y :: ereal show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
+ show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
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 }
- { fix z assume "x \<le> y" "y \<le> z" then show "x \<le> z"
+ { assume "x \<le> y" "y \<le> z" then show "x \<le> z"
by (cases rule: ereal3_cases[of x y z]) auto }
qed
+
end
instance ereal :: ordered_ab_semigroup_add
@@ -430,16 +435,20 @@
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
-next case PInf with assms[of 0] show ?thesis by auto
-next case MInf then show ?thesis by simp
+next
+ case PInf with assms[of 0] show ?thesis by auto
+next
+ case MInf then show ?thesis by simp
qed
lemma ereal_top:
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
-next case MInf with assms[of 0] show ?thesis by auto
-next case PInf then show ?thesis by simp
+next
+ case MInf with assms[of 0] show ?thesis by auto
+next
+ case PInf then show ?thesis by simp
qed
lemma
@@ -516,11 +525,11 @@
instance
proof
- fix a :: ereal show "1 * a = a"
+ fix a b c :: ereal show "1 * a = a"
by (cases a) (simp_all add: one_ereal_def)
- fix b :: ereal show "a * b = b * a"
+ show "a * b = b * a"
by (cases rule: ereal2_cases[of a b]) simp_all
- fix c :: ereal show "a * b * c = a * (b * c)"
+ show "a * b * c = a * (b * c)"
by (cases rule: ereal3_cases[of a b c])
(simp_all add: zero_ereal_def zero_less_mult_iff)
qed
@@ -668,11 +677,11 @@
shows "x <= y"
proof-
{ assume a: "EX r. y = ereal r"
- from this obtain r where r_def: "y = ereal r" by auto
+ then obtain r where r_def: "y = ereal r" by auto
{ assume "x=(-\<infinity>)" hence ?thesis by auto }
moreover
{ assume "~(x=(-\<infinity>))"
- from this obtain p where p_def: "x = ereal p"
+ 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 }
@@ -696,10 +705,10 @@
{ assume "e=\<infinity>" hence "x<=y+e" by auto }
moreover
{ assume "e~=\<infinity>"
- from this obtain r where "e = ereal r" using `e>0` apply (cases e) by auto
+ 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
-} from this show ?thesis using ereal_le_epsilon by auto
+} then show ?thesis using ereal_le_epsilon by auto
qed
lemma ereal_le_real:
@@ -790,11 +799,14 @@
lemma ereal_uminus_lessThan[simp]:
fixes a :: ereal shows "uminus ` {..<a} = {-a<..}"
-proof (safe intro!: image_eqI)
- fix x assume "-a < x"
- then have "- x < - (- a)" by (simp del: ereal_uminus_uminus)
- then show "- x < a" by simp
-qed auto
+proof -
+ {
+ 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)
+qed
lemma ereal_uminus_greaterThan[simp]:
"uminus ` {(a::ereal)<..} = {..<-a}"
@@ -923,7 +935,8 @@
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 by (cases x, cases e) auto
+using assms apply (cases x, cases e) apply auto
+done
subsubsection {* Division *}
@@ -939,7 +952,7 @@
definition "x / y = x * inverse (y :: ereal)"
-instance proof qed
+instance ..
end
lemma real_of_ereal_inverse[simp]:
@@ -1092,7 +1105,7 @@
begin
definition [simp]: "sup x y = (max x y :: ereal)"
definition [simp]: "inf x y = (min x y :: ereal)"
-instance proof qed simp_all
+instance by default simp_all
end
instantiation ereal :: complete_lattice
@@ -1161,7 +1174,7 @@
proof-
def S1 == "uminus ` S"
hence "S1 ~= {}" using assms by auto
-from this obtain x where x_def: "(ALL y:S1. y <= x) & (ALL z. (ALL y:S1. y <= z) --> x <= z)"
+then obtain x where x_def: "(ALL y:S1. y <= x) & (ALL z. (ALL y:S1. y <= z) --> x <= z)"
using ereal_complete_Sup[of S1] by auto
{ fix z assume "ALL y:S. z <= y"
hence "ALL y:S1. y <= -z" unfolding S1_def by auto
@@ -1372,8 +1385,8 @@
proof-
{ assume "?rhs"
{ assume "~(x <= (SUP i:A. f i))" hence "(SUP i:A. f i)<x" by (simp add: not_le)
- from this obtain y where y_def: "(SUP i:A. f i)<y & y<x" using ereal_dense by auto
- from this obtain i where "i : A & y <= f i" using `?rhs` by auto
+ then obtain y where y_def: "(SUP i:A. f i)<y & y<x" using ereal_dense by auto
+ then obtain i where "i : A & y <= f i" using `?rhs` by auto
hence "y <= (SUP i:A. f i)" using SUP_upper[of i A f] by auto
hence False using y_def by auto
} hence "?lhs" by auto
@@ -1391,8 +1404,8 @@
proof-
{ assume "?rhs"
{ assume "~((INF i:A. f i) <= x)" hence "x < (INF i:A. f i)" by (simp add: not_le)
- from this obtain y where y_def: "x<y & y<(INF i:A. f i)" using ereal_dense by auto
- from this obtain i where "i : A & f i <= y" using `?rhs` by auto
+ then obtain y where y_def: "x<y & y<(INF i:A. f i)" using ereal_dense by auto
+ then obtain i where "i : A & f i <= y" using `?rhs` by auto
hence "(INF i:A. f i) <= y" using INF_lower[of i A f] by auto
hence False using y_def by auto
} hence "?lhs" by auto
@@ -2023,7 +2036,7 @@
shows "Y ----> L"
proof-
{ fix S assume "open S" and "L:S"
- from this obtain N1 where "ALL n>=N1. X n : S"
+ then obtain N1 where "ALL n>=N1. X n : S"
using assms unfolding tendsto_def eventually_sequentially by auto
hence "ALL n>=max N N1. Y n : S" using assms by auto
hence "EX N. ALL n>=N. Y n : S" apply(rule_tac x="max N N1" in exI) by auto
@@ -2058,14 +2071,14 @@
hence ?thesis by auto }
moreover
{ assume "EX B. C = ereal B"
- from this obtain B where B_def: "C=ereal B" by auto
+ then obtain B where B_def: "C=ereal B" by auto
hence "~(l=\<infinity>)" using Lim_bounded_PInfty2 assms by auto
- from this obtain m where m_def: "ereal m=l" using `~(l=(-\<infinity>))` by (cases l) auto
- from this obtain N where N_def: "ALL n>=N. f n : {ereal(m - 1) <..< ereal(m+1)}"
+ then obtain m where m_def: "ereal m=l" using `~(l=(-\<infinity>))` by (cases l) auto
+ then obtain N where N_def: "ALL n>=N. f n : {ereal(m - 1) <..< ereal(m+1)}"
apply (subst tendsto_obtains_N[of f l "{ereal(m - 1) <..< ereal(m+1)}"]) using assms by auto
{ fix n assume "n>=N"
hence "EX r. ereal r = f n" using N_def by (cases "f n") auto
- } from this obtain g where g_def: "ALL n>=N. ereal (g n) = f n" by metis
+ } then obtain g where g_def: "ALL n>=N. ereal (g n) = f n" by metis
hence "(%n. ereal (g n)) ----> l" using tail_same_limit[of f l N] assms by auto
hence *: "(%n. g n) ----> m" using m_def by auto
{ fix n assume "n>=max N M"
@@ -2175,7 +2188,7 @@
fix N assume "n <= N"
from upper[OF this] lower[OF this] assms `0 < r`
have "u N ~: {\<infinity>,(-\<infinity>)}" by auto
- from this obtain ra where ra_def: "(u N) = ereal ra" by (cases "u N") 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"
@@ -2194,7 +2207,7 @@
proof
assume lim: "u ----> x"
{ fix r assume "(r::ereal)>0"
- from this obtain N where N_def: "ALL n>=N. u n : {x - r <..< x + r}"
+ then obtain N where N_def: "ALL 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"
@@ -2537,8 +2550,8 @@
lemma real_ereal_id: "real o ereal = id"
proof-
-{ fix x have "(real o ereal) x = id x" by auto }
-from this show ?thesis using ext by blast
+ { 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)})"
--- a/src/Pure/Isar/class.ML Thu Mar 22 18:54:39 2012 +0100
+++ b/src/Pure/Isar/class.ML Thu Mar 22 21:43:26 2012 +0100
@@ -145,10 +145,12 @@
fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy;
val base_morphism = #base_morph oo the_class_data;
+
fun morphism thy class =
(case Element.eq_morphism thy (these_defs thy [class]) of
SOME eq_morph => base_morphism thy class $> eq_morph
| NONE => base_morphism thy class);
+
val export_morphism = #export_morph oo the_class_data;
fun print_classes ctxt =
@@ -228,9 +230,9 @@
val intros = (snd o rules thy) sup :: map_filter I
[Option.map (Drule.export_without_context_open o Element.conclude_witness) some_wit,
(fst o rules thy) sub];
- val tac = EVERY (map (TRYALL o Tactic.rtac) intros);
- val classrel = Skip_Proof.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
- (K tac);
+ val classrel =
+ Skip_Proof.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
+ (K (EVERY (map (TRYALL o Tactic.rtac) intros)));
val diff_sort = Sign.complete_sort thy [sup]
|> subtract (op =) (Sign.complete_sort thy [sub])
|> filter (is_class thy);
@@ -312,13 +314,13 @@
val class_prefix = Logic.const_of_class o Long_Name.base_name;
+local
+
fun target_extension f class lthy =
lthy
|> Local_Theory.raw_theory f
- |> Local_Theory.target (synchronize_class_syntax [class]
- (base_sort (Proof_Context.theory_of lthy) class));
-
-local
+ |> Local_Theory.map_contexts
+ (synchronize_class_syntax [class] (base_sort (Proof_Context.theory_of lthy) class));
fun target_const class ((c, mx), (type_params, dict)) thy =
let
@@ -478,10 +480,11 @@
(* target *)
-fun define_overloaded (c, U) v (b_def, rhs) = Local_Theory.background_theory_result
- (AxClass.declare_overloaded (c, U) ##>> AxClass.define_overloaded b_def (c, rhs))
+fun define_overloaded (c, U) v (b_def, rhs) =
+ Local_Theory.background_theory_result (AxClass.declare_overloaded (c, U)
+ ##>> AxClass.define_overloaded b_def (c, rhs))
##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v))
- ##> Local_Theory.target synchronize_inst_syntax;
+ ##> Local_Theory.map_contexts synchronize_inst_syntax;
fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
(case instantiation_param lthy b of
@@ -554,7 +557,7 @@
abbrev = Generic_Target.abbrev
(fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
Generic_Target.theory_abbrev prmode ((b, mx), t)),
- declaration = K Generic_Target.theory_declaration,
+ declaration = K Generic_Target.standard_declaration,
pretty = pretty,
exit = Local_Theory.target_of o conclude}
end;
@@ -603,8 +606,8 @@
val (tycos, vs, sort) = read_multi_arity thy raw_arities;
val sorts = map snd vs;
val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
- fun after_qed results = Proof_Context.background_theory
- ((fold o fold) AxClass.add_arity results);
+ fun after_qed results =
+ Proof_Context.background_theory ((fold o fold) AxClass.add_arity results);
in
thy
|> Proof_Context.init_global
--- a/src/Pure/Isar/generic_target.ML Thu Mar 22 18:54:39 2012 +0100
+++ b/src/Pure/Isar/generic_target.ML Thu Mar 22 21:43:26 2012 +0100
@@ -20,7 +20,9 @@
string * bool -> (binding * mixfix) * term -> local_theory ->
(term * term) * local_theory
- val theory_declaration: declaration -> local_theory -> local_theory
+ val background_declaration: declaration -> local_theory -> local_theory
+ val standard_declaration: declaration -> local_theory -> local_theory
+
val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
term list * term list -> local_theory -> (term * thm) * local_theory
val theory_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list ->
@@ -88,8 +90,7 @@
(*note*)
val ([(res_name, [res])], lthy4) = lthy3
- |> Local_Theory.notes_kind ""
- [((if internal then Binding.empty else b_def, atts), [([def], [])])];
+ |> Local_Theory.notes [((if internal then Binding.empty else b_def, atts), [([def], [])])];
in ((lhs, (res_name, res)), lthy4) end;
@@ -180,20 +181,24 @@
end;
+(* declaration *)
+
+fun background_declaration decl lthy =
+ let
+ val theory_decl =
+ Local_Theory.standard_form lthy
+ (Proof_Context.init_global (Proof_Context.theory_of lthy)) decl;
+ in Local_Theory.background_theory (Context.theory_map theory_decl) lthy end;
+
+fun standard_declaration decl =
+ background_declaration decl #>
+ (fn lthy => Local_Theory.map_contexts (fn ctxt =>
+ Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt) lthy);
+
+
(** primitive theory operations **)
-fun theory_declaration decl lthy =
- let
- val global_decl = Morphism.form
- (Morphism.transform (Local_Theory.global_morphism lthy) decl);
- in
- lthy
- |> Local_Theory.background_theory (Context.theory_map global_decl)
- |> Local_Theory.target (Context.proof_map global_decl)
- |> Context.proof_map (Morphism.form decl)
- end;
-
fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
let
val (const, lthy2) = lthy
--- a/src/Pure/Isar/local_theory.ML Thu Mar 22 18:54:39 2012 +0100
+++ b/src/Pure/Isar/local_theory.ML Thu Mar 22 21:43:26 2012 +0100
@@ -33,7 +33,7 @@
val propagate_ml_env: generic_theory -> generic_theory
val standard_morphism: local_theory -> Proof.context -> morphism
val target_morphism: local_theory -> morphism
- val global_morphism: local_theory -> morphism
+ val standard_form: local_theory -> Proof.context -> (morphism -> 'a) -> 'a
val operations_of: local_theory -> operations
val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
(term * (string * thm)) * local_theory
@@ -99,7 +99,12 @@
);
fun map_contexts f =
- (Data.map o map) (fn {naming, operations, target} => make_lthy (naming, operations, f target))
+ (Data.map o map) (fn {naming, operations, target} =>
+ make_lthy (naming, operations,
+ target
+ |> Context_Position.set_visible false
+ |> f
+ |> Context_Position.restore_visible target))
#> f;
fun assert lthy =
@@ -178,10 +183,11 @@
fun target_result f lthy =
let
- val (res, ctxt') = target_of lthy
+ val target = target_of lthy;
+ val (res, ctxt') = target
|> Context_Position.set_visible false
|> f
- ||> Context_Position.restore_visible lthy;
+ ||> Context_Position.restore_visible target;
val thy' = Proof_Context.theory_of ctxt';
val lthy' = lthy
|> map_target (K ctxt')
@@ -208,8 +214,8 @@
fun target_morphism lthy = standard_morphism lthy (target_of lthy);
-fun global_morphism lthy =
- standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy));
+fun standard_form lthy ctxt x =
+ Morphism.form (Morphism.transform (standard_morphism lthy ctxt) x);
--- a/src/Pure/Isar/named_target.ML Thu Mar 22 18:54:39 2012 +0100
+++ b/src/Pure/Isar/named_target.ML Thu Mar 22 21:43:26 2012 +0100
@@ -61,12 +61,10 @@
end;
fun target_declaration (Target {target, ...}) {syntax, pervasive} decl lthy =
- if target = "" then Generic_Target.theory_declaration decl lthy
+ if target = "" then Generic_Target.standard_declaration decl lthy
else
lthy
- |> pervasive ? Local_Theory.background_theory
- (Context.theory_map
- (Morphism.form (Morphism.transform (Local_Theory.global_morphism lthy) decl)))
+ |> pervasive ? Generic_Target.background_declaration decl
|> locale_declaration target syntax decl
|> Context.proof_map (Morphism.form decl);
@@ -133,7 +131,7 @@
lthy
|> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)
|> Local_Theory.target (Locale.add_thmss locale kind local_facts')
- end
+ end;
fun target_notes (Target {target, is_locale, ...}) =
if is_locale then locale_notes target
--- a/src/Pure/Isar/overloading.ML Thu Mar 22 18:54:39 2012 +0100
+++ b/src/Pure/Isar/overloading.ML Thu Mar 22 21:43:26 2012 +0100
@@ -155,7 +155,7 @@
(Thm.def_binding_optional (Binding.name v) b_def,
Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs)))
##> map_overloading (filter_out (fn (_, (v', _)) => v' = v))
- ##> Local_Theory.target synchronize_syntax
+ ##> Local_Theory.map_contexts synchronize_syntax
#-> (fn (_, def) => pair (Const (c, U), def));
fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
@@ -208,7 +208,7 @@
abbrev = Generic_Target.abbrev
(fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
Generic_Target.theory_abbrev prmode ((b, mx), t)),
- declaration = K Generic_Target.theory_declaration,
+ declaration = K Generic_Target.standard_declaration,
pretty = pretty,
exit = Local_Theory.target_of o conclude}
end;
--- a/src/Pure/Isar/specification.ML Thu Mar 22 18:54:39 2012 +0100
+++ b/src/Pure/Isar/specification.ML Thu Mar 22 21:43:26 2012 +0100
@@ -220,8 +220,7 @@
val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]);
val ([(def_name, [th'])], lthy4) = lthy3
- |> Local_Theory.notes_kind ""
- [((name, Code.add_default_eqn_attrib :: atts), [([th], [])])];
+ |> Local_Theory.notes [((name, Code.add_default_eqn_attrib :: atts), [([th], [])])];
val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs;