author wenzelm Thu, 22 Mar 2012 21:43:26 +0100 changeset 47088 eba1cea4eef6 parent 47087 08c22e8ffe70 (current diff) parent 47082 737d7bc8e50f (diff) child 47089 29e92b644d6c child 47090 6b53d954255b
merged;
```--- 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 @@

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

@@ -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])
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
+fun define_overloaded (c, U) v (b_def, rhs) =
+  ##>> 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
@@ -155,7 +155,7 @@
(Thm.def_binding_optional (Binding.name v) b_def,
Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs)))
-  ##> 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;
```