merged
authorwenzelm
Thu, 28 Jul 2016 20:39:51 +0200
changeset 63559 113cee845044
parent 63556 36e9732988ce (diff)
parent 63558 0aa33085c8b1 (current diff)
child 63560 3e3097ac37d1
child 63561 fba08009ff3e
merged
--- a/CONTRIBUTORS	Thu Jul 28 20:39:46 2016 +0200
+++ b/CONTRIBUTORS	Thu Jul 28 20:39:51 2016 +0200
@@ -17,12 +17,19 @@
   Reasoning support for monotonicity, continuity and
   admissibility in chain-complete partial orders.
 
+* May 2016: Manuel Eberl
+  Code generation for Probability Mass Functions.
+
 * June 2016: Andreas Lochbihler
   Formalisation of discrete subprobability distributions.
 
 * July 2016: Daniel Stuewe
   Height-size proofs in HOL/Data_Structures
 
+* July 2016: Manuel Eberl
+  Algebraic foundation for primes; generalization from nat
+  to general factorial rings
+
 Contributions to Isabelle2016
 -----------------------------
 
--- a/NEWS	Thu Jul 28 20:39:46 2016 +0200
+++ b/NEWS	Thu Jul 28 20:39:51 2016 +0200
@@ -173,6 +173,14 @@
 
 *** HOL ***
 
+* Number_Theory: algebraic foundation for primes: Introduction of 
+predicates "is_prime", "irreducible", a "prime_factorization" 
+function, the "factorial_ring" typeclass with instance proofs for 
+nat, int, poly.
+
+* Probability: Code generation and QuickCheck for Probability Mass 
+Functions.
+
 * Theory Set_Interval.thy: substantial new theorems on indexed sums
 and products.
 
@@ -816,6 +824,9 @@
 
 *** Document preparation ***
 
+* Text and ML antiquotation @{locale} for locales, similar to existing
+antiquotations for classes.
+
 * Commands 'paragraph' and 'subparagraph' provide additional section
 headings. Thus there are 6 levels of standard headings, as in HTML.
 
--- a/src/Doc/Typeclass_Hierarchy/Setup.thy	Thu Jul 28 20:39:46 2016 +0200
+++ b/src/Doc/Typeclass_Hierarchy/Setup.thy	Thu Jul 28 20:39:51 2016 +0200
@@ -1,5 +1,5 @@
 theory Setup
-imports Complex_Main "~~/src/HOL/Library/Lattice_Syntax"
+imports Complex_Main "~~/src/HOL/Library/Multiset" "~~/src/HOL/Library/Lattice_Syntax"
 begin
 
 ML_file "../antiquote_setup.ML"
@@ -11,6 +11,29 @@
 
 setup \<open>Config.put_global Printer.show_type_emphasis false\<close>
 
+setup \<open>
+let
+  fun strip_all t =
+    if Logic.is_all t
+    then
+      case snd (dest_comb t) of Abs (w, T, t') =>
+        strip_all t' |>> cons (w, T)
+    else ([], t);
+  fun frugal (w, T as TFree (v, sort)) visited =
+        if member (op =) visited v
+        then ((w, dummyT), visited) else ((w, T), v :: visited)
+    | frugal (w, T) visited = ((w, dummyT), visited);
+  fun frugal_sorts t =
+    let
+      val (vTs, body) = strip_all t
+      val (vTs', _) = fold_map frugal vTs [];
+    in Logic.list_all (vTs', map_types (K dummyT) body) end;
+in
+  Term_Style.setup @{binding frugal_sorts}
+    (Scan.succeed (K frugal_sorts))
+end
+\<close>
+
 declare [[show_sorts]]
 
 end
--- a/src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy	Thu Jul 28 20:39:46 2016 +0200
+++ b/src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy	Thu Jul 28 20:39:51 2016 +0200
@@ -6,7 +6,7 @@
 
 text \<open>
   The {Isabelle/HOL} type-class hierarchy entered the stage
-  in a quite ancient era -- first related \emph{NEWS} entries date
+  in a quite ancient era -- first related \<^emph>\<open>NEWS\<close> entries date
   back to release {Isabelle99-1}.  Since then, there have been
   ongoing modifications and additions, leading to ({Isabelle2016})
   more than 180 type-classes.  This sheer complexity makes access
@@ -79,8 +79,8 @@
       types, hence also sharing of notation and names: there
       is only one plus operation using infix syntax @{text "+"},
       only one zero written @{text 0}, and neutrality
-      (@{thm add_0_left [all, no_vars]} and
-      @{thm add_0_right [all, no_vars]})
+      (@{thm (frugal_sorts) add_0_left [all, no_vars]} and
+      @{thm (frugal_sorts) add_0_right [all, no_vars]})
       is referred to
       uniformly by names @{fact add_0_left} and @{fact add_0_right}.
 
@@ -128,20 +128,20 @@
 
 section \<open>The hierarchy\<close>
 
-subsection \<open>Syntactic type classes\<close>
+subsection \<open>Syntactic type classes \label{sec:syntactic-type-class}\<close>
 
 text \<open>
   At the top of the hierarchy there are a couple of syntactic type
   classes, ie. classes with operations but with no axioms,
   most notably:
 
-    \<^item> @{class plus} with @{term [source] "(a::'a::plus) + b"}
+    \<^item> @{command class} @{class plus} with @{term [source] "(a::'a::plus) + b"}
 
-    \<^item> @{class zero} with @{term [source] "0::'a::zero"}
+    \<^item> @{command class} @{class zero} with @{term [source] "0::'a::zero"}
 
-    \<^item> @{class times} with @{term [source] "(a::'a::times) * b"}
+    \<^item> @{command class} @{class times} with @{term [source] "(a::'a::times) * b"}
 
-    \<^item> @{class one} with @{term [source] "1::'a::one"}
+    \<^item> @{command class} @{class one} with @{term [source] "1::'a::one"}
 
   \noindent Before the introduction of the @{command class} statement in
   Isabelle \cite{Haftmann-Wenzel:2006:classes} it was impossible
@@ -173,4 +173,196 @@
   not provable without particular type constraints.
 \<close>
 
+
+subsection \<open>Additive and multiplicative semigroups and monoids\<close>
+
+text \<open>
+  In common literature, notation for semigroups and monoids
+  is either multiplicative @{text "(*, 1)"} or additive
+  @{text "(+, 0)"} with underlying properties isomorphic.
+  In {Isabelle/HOL}, this is accomplished using the following
+  abstract setup:
+
+    \<^item> A @{locale semigroup} introduces an abstract binary
+      associative operation.
+
+    \<^item> A @{locale monoid} is an extension of @{locale semigroup}
+      with a neutral element.
+
+    \<^item> Both @{locale semigroup} and @{locale monoid} provide
+      dedicated syntax for their operations @{text "(\<^bold>*, \<^bold>1)"}.
+      This syntax is not visible on the global theory level
+      but only for abstract reasoning inside the respective
+      locale.
+
+    \<^item> Concrete global syntax is added building on existing
+      syntactic type classes \secref{sec:syntactic-type-class}
+      using the following classes:
+
+        \<^item> @{command class} @{class semigroup_mult} = @{class times}
+
+        \<^item> @{command class} @{class monoid_mult} = @{class one} + @{class semigroup_mult}
+
+        \<^item> @{command class} @{class semigroup_add} = @{class plus}
+
+        \<^item> @{command class} @{class monoid_add} = @{class zero} + @{class semigroup_add}
+
+      Locales @{locale semigroup} and @{locale monoid} are
+      interpreted (using @{command sublocale}) into their
+      corresponding type classes, with prefixes @{text add}
+      and @{text mult}; hence facts derived in @{locale semigroup}
+      and @{locale monoid} are propagated simultaneously to
+      \<^emph>\<open>both\<close> using a consistent naming policy, ie.
+
+        \<^item> @{fact semigroup.assoc}: @{thm (frugal_sorts) semigroup.assoc [all, no_vars]}
+
+        \<^item> @{fact mult.assoc}: @{thm (frugal_sorts) mult.assoc [all, no_vars]}
+
+        \<^item> @{fact add.assoc}: @{thm (frugal_sorts) add.assoc [all, no_vars]}
+
+        \<^item> @{fact monoid.right_neutral}: @{thm (frugal_sorts) monoid.right_neutral [all, no_vars]}
+
+        \<^item> @{fact mult.right_neutral}: @{thm (frugal_sorts) mult.right_neutral [all, no_vars]}
+
+        \<^item> @{fact add.right_neutral}: @{thm (frugal_sorts) add.right_neutral [all, no_vars]}
+
+    \<^item> Note that the syntax in @{locale semigroup} and @{locale monoid}
+      is bold; this avoids clashes when writing properties
+      inside one of these locales in presence of that global
+      concrete type class syntax.
+
+  \noindent That hierarchy extends in a straightforward manner
+  to abelian semigroups and commutative monoids\footnote{The
+  designation \<^emph>\<open>abelian\<close> is quite standard concerning
+  (semi)groups, but not for monoids}:
+
+    \<^item> Locales @{locale abel_semigroup} and @{locale comm_monoid}
+      add commutativity as property.
+
+    \<^item> Concrete syntax emerges through
+
+        \<^item> @{command class} @{class ab_semigroup_add} = @{class semigroup_add}
+
+        \<^item> @{command class} @{class ab_semigroup_mult} = @{class semigroup_mult}
+
+        \<^item> @{command class} @{class comm_monoid_add} = @{class zero} + @{class ab_semigroup_add}
+
+        \<^item> @{command class} @{class comm_monoid_mult} = @{class one} + @{class ab_semigroup_mult}
+  
+      and corresponding interpretation of the locales above, yielding
+
+        \<^item> @{fact abel_semigroup.commute}: @{thm (frugal_sorts) abel_semigroup.commute [all, no_vars]}
+
+        \<^item> @{fact mult.commute}: @{thm (frugal_sorts) mult.commute [all, no_vars]}
+
+        \<^item> @{fact add.commute}: @{thm (frugal_sorts) add.commute [all, no_vars]}
+\<close>
+
+paragraph \<open>Named collection of theorems\<close>
+
+text \<open>
+  Locale interpretation interacts smoothly with named collections of
+  theorems as introduced by command @{command named_theorems}.  In our
+  example, rules concerning associativity and commutativity are no
+  simplification rules by default since they desired orientation may
+  vary depending on the situation.  However, there is a collection
+  @{fact ac_simps} where facts @{fact abel_semigroup.assoc},
+  @{fact abel_semigroup.commute} and @{fact abel_semigroup.left_commute}
+  are declared as members.  Due to interpretation, also
+  @{fact mult.assoc}, @{fact mult.commute} and @{fact mult.left_commute}
+  are also members of @{fact ac_simps}, as any corresponding facts
+  stemming from interpretation of @{locale abel_semigroup}.
+  Hence adding @{fact ac_simps} to the simplification rules for
+  a single method call uses all associativity and commutativity
+  rules known by means of interpretation.
+\<close>
+
+
+subsection \<open>Additive and multiplicative groups\<close>
+
+text \<open>
+  The hierarchy for inverse group operations takes into account
+  that there are weaker algebraic structures with only a partially
+  inverse operation.  E. g. the natural numbers have bounded
+  subtraction @{term "m - (n::nat)"} which is only an inverse
+  operation if @{term "m \<ge> (n::nat)"};  unary minus @{text "-"}
+  is pointless on the natural numbers.
+
+  Hence for both additive and multiplicative notation there
+  are syntactic classes for inverse operations, both unary
+  and binary:
+
+    \<^item> @{command class} @{class minus} with @{term [source] "(a::'a::minus) - b"}
+
+    \<^item> @{command class} @{class uminus} with @{term [source] "- a::'a::uminus"}
+
+    \<^item> @{command class} @{class divide} with @{term [source] "(a::'a::divide) div b"}
+
+    \<^item> @{command class} @{class inverse} = @{class divide} with @{term [source] "inverse a::'a::inverse"}
+        \\ and @{term [source] "(a::'a::inverse) / b"}
+
+  \noindent Here @{class inverse} specializes the ``partial'' syntax
+  @{term [source] "a div b"} to the more specific
+  @{term [source] "a / b"}. 
+
+  Semantic properties are added by
+
+    \<^item> @{command class} @{class cancel_ab_semigroup_add} = @{class ab_semigroup_add} + @{class minus}
+
+    \<^item> @{command class} @{class cancel_comm_monoid_add} = @{class cancel_ab_semigroup_add} + @{class comm_monoid_add}
+
+  \noindent which specify a minimal binary partially inverse operation as
+
+    \<^item> @{fact add_diff_cancel_left'}: @{thm (frugal_sorts) add_diff_cancel_left' [all, no_vars]}
+
+    \<^item> @{fact diff_diff_add}: @{thm (frugal_sorts) diff_diff_add [all, no_vars]}
+
+  \noindent which in turn allow to derive facts like
+
+    \<^item> @{fact add_left_imp_eq}: @{thm (frugal_sorts) add_left_imp_eq [all, no_vars]}
+
+  \noindent The total inverse operation is established as follows:
+
+    \<^item> Locale @{locale group} extends the abstract hierarchy with
+      the inverse operation.
+
+    \<^item> The concrete additive inverse operation emerges through
+
+      \<^item> @{command class} @{class group_add} = @{class minus} + @{class uminus} + @{class monoid_add} (in @{theory Groups}) \\
+
+      \<^item> @{command class} @{class ab_group_add} = @{class minus} + @{class uminus} + @{class comm_monoid_add} (in @{theory Groups})
+
+      and corresponding interpretation of locale @{locale group}, yielding e.g.
+
+      \<^item> @{fact group.left_inverse}: @{thm (frugal_sorts) group.left_inverse [all, no_vars]}
+
+      \<^item> @{fact add.left_inverse}: @{thm (frugal_sorts) add.left_inverse [all, no_vars]}
+
+  \noindent There is no multiplicative counterpart.  Why?  In rings,
+  the multiplicative group excludes the zero element, hence
+  the inverse operation is not total.  See further \secref{sec:rings}.
+\<close>
+
+paragraph \<open>Mitigating against redundancy by default simplification rules\<close>
+
+text \<open>
+  Inverse operations imposes some redundancy on the type class
+  hierarchy: in a group with a total inverse operation, the
+  unary operation is simpler and more primitive than the binary
+  one; but we cannot eliminate the binary one in favour of
+  a mere syntactic abbreviation since the binary one is vital
+  to express a partial inverse operation.
+
+  This is mitigated by providing suitable default simplification
+  rules: expression involving the unary inverse operation are
+  simplified to binary inverse operation whenever appropriate.
+  The rationale is that simplification is a central device in
+  explorative proving, where proof obligation remaining after certain
+  default proof steps including simplification are inspected
+  to get an idea what is missing to finish a proof.  When
+  preferable normal forms are encoded into
+  default simplification rules, proof obligations after simplification
+  are normalized and hence more proof-friendly.
+\<close>
+
 end
--- a/src/Doc/more_antiquote.ML	Thu Jul 28 20:39:46 2016 +0200
+++ b/src/Doc/more_antiquote.ML	Thu Jul 28 20:39:51 2016 +0200
@@ -25,21 +25,18 @@
 
 end;
 
+
 (* code theorem antiquotation *)
 
 local
 
-fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
-
-fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
-
 fun no_vars ctxt thm =
   let
     val ctxt' = Variable.set_body false ctxt;
     val ((_, [thm]), _) = Variable.import true [thm] ctxt';
   in thm end;
 
-fun pretty_code_thm ctxt source raw_const =
+fun pretty_code_thm ctxt raw_const =
   let
     val thy = Proof_Context.theory_of ctxt;
     val const = Code.check_const thy raw_const;
@@ -51,13 +48,13 @@
       |> these
       |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
       |> map (holize o no_vars ctxt o Axclass.overload ctxt);
-  in Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty_thm ctxt source thms) end;
+  in Thy_Output.output ctxt (map (Thy_Output.pretty_thm ctxt) thms) end;
 
 in
 
 val _ =
   Theory.setup (Thy_Output.antiquotation @{binding code_thms} Args.term
-    (fn {source, context, ...} => pretty_code_thm context source));
+    (fn {context, ...} => pretty_code_thm context));
 
 end;
 
--- a/src/HOL/Filter.thy	Thu Jul 28 20:39:46 2016 +0200
+++ b/src/HOL/Filter.thy	Thu Jul 28 20:39:51 2016 +0200
@@ -618,6 +618,12 @@
   unfolding at_top_def
   by (subst eventually_INF_base) (auto simp: eventually_principal intro: max.cobounded1 max.cobounded2)
 
+lemma eventually_at_top_linorderI:
+  fixes c::"'a::linorder"
+  assumes "\<And>x. c \<le> x \<Longrightarrow> P x"
+  shows "eventually P at_top"
+  using assms by (auto simp: eventually_at_top_linorder)
+
 lemma eventually_ge_at_top:
   "eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top"
   unfolding eventually_at_top_linorder by auto
--- a/src/HOL/Limits.thy	Thu Jul 28 20:39:46 2016 +0200
+++ b/src/HOL/Limits.thy	Thu Jul 28 20:39:51 2016 +0200
@@ -1401,6 +1401,14 @@
 lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) \<longlongrightarrow> 0) F"
  by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff)
 
+lemma real_tendsto_divide_at_top:
+  fixes c::"real"
+  assumes "(f \<longlongrightarrow> c) F"
+  assumes "filterlim g at_top F"
+  shows "((\<lambda>x. f x / g x) \<longlongrightarrow> 0) F"
+  by (auto simp: divide_inverse_commute
+      intro!: tendsto_mult[THEN tendsto_eq_rhs] tendsto_inverse_0_at_top assms)
+
 lemma mult_nat_left_at_top: "c > 0 \<Longrightarrow> filterlim (\<lambda>x. c * x) at_top sequentially"
   for c :: nat
   by (rule filterlim_subseq) (auto simp: subseq_def)
@@ -1489,6 +1497,13 @@
   qed
 qed
 
+lemma filterlim_at_top_mult_tendsto_pos:
+  assumes f: "(f \<longlongrightarrow> c) F"
+    and c: "0 < c"
+    and g: "LIM x F. g x :> at_top"
+  shows "LIM x F. (g x * f x:: real) :> at_top"
+  by (auto simp: mult.commute intro!: filterlim_tendsto_pos_mult_at_top f c g)
+
 lemma filterlim_tendsto_pos_mult_at_bot:
   fixes c :: real
   assumes "(f \<longlongrightarrow> c) F" "0 < c" "filterlim g at_bot F"
@@ -2139,6 +2154,26 @@
 lemma LIMSEQ_divide_realpow_zero: "1 < x \<Longrightarrow> (\<lambda>n. a / (x ^ n) :: real) \<longlonglongrightarrow> 0"
   by (rule tendsto_divide_0 [OF tendsto_const filterlim_realpow_sequentially_gt1]) simp
 
+lemma
+  tendsto_power_zero:
+  fixes x::"'a::real_normed_algebra_1"
+  assumes "filterlim f at_top F"
+  assumes "norm x < 1"
+  shows "((\<lambda>y. x ^ (f y)) \<longlongrightarrow> 0) F"
+proof (rule tendstoI)
+  fix e::real assume "0 < e"
+  from tendstoD[OF LIMSEQ_power_zero[OF \<open>norm x < 1\<close>] \<open>0 < e\<close>]
+  have "\<forall>\<^sub>F xa in sequentially. norm (x ^ xa) < e"
+    by simp
+  then obtain N where N: "norm (x ^ n) < e" if "n \<ge> N" for n
+    by (auto simp: eventually_sequentially)
+  have "\<forall>\<^sub>F i in F. f i \<ge> N"
+    using \<open>filterlim f sequentially F\<close>
+    by (simp add: filterlim_at_top)
+  then show "\<forall>\<^sub>F i in F. dist (x ^ f i) 0 < e"
+    by (eventually_elim) (auto simp: N)
+qed
+
 text \<open>Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}.\<close>
 
 lemma LIMSEQ_rabs_realpow_zero: "\<bar>c\<bar> < 1 \<Longrightarrow> (\<lambda>n. \<bar>c\<bar> ^ n :: real) \<longlonglongrightarrow> 0"
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Thu Jul 28 20:39:46 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Thu Jul 28 20:39:51 2016 +0200
@@ -2397,6 +2397,47 @@
 lemma abs_tan_ge: "\<bar>x\<bar> < pi/2 \<Longrightarrow> \<bar>x\<bar> \<le> \<bar>tan x\<bar>"
   by (metis abs_arctan_le abs_less_iff arctan_tan minus_less_iff)
 
+lemma arctan_bounds:
+  assumes "0 \<le> x" "x < 1"
+  shows arctan_lower_bound:
+    "(\<Sum>k<2 * n. (- 1) ^ k * (1 / real (k * 2 + 1) * x ^ (k * 2 + 1))) \<le> arctan x"
+    (is "(\<Sum>k<_. (- 1)^ k * ?a k) \<le> _")
+    and arctan_upper_bound:
+    "arctan x \<le> (\<Sum>k<2 * n + 1. (- 1) ^ k * (1 / real (k * 2 + 1) * x ^ (k * 2 + 1)))"
+proof -
+  have tendsto_zero: "?a \<longlonglongrightarrow> 0"
+    using assms
+    apply -
+    apply (rule tendsto_eq_rhs[where x="0 * 0"])
+    subgoal by (intro tendsto_mult real_tendsto_divide_at_top)
+        (auto simp: filterlim_real_sequentially filterlim_sequentially_iff_filterlim_real
+          intro!: real_tendsto_divide_at_top tendsto_power_zero filterlim_real_sequentially
+           tendsto_eq_intros filterlim_at_top_mult_tendsto_pos filterlim_tendsto_add_at_top)
+    subgoal by simp
+    done
+  have nonneg: "0 \<le> ?a n" for n
+    by (force intro!: divide_nonneg_nonneg mult_nonneg_nonneg zero_le_power assms)
+  have le: "?a (Suc n) \<le> ?a n" for n
+    by (rule mult_mono[OF _ power_decreasing]) (auto simp: divide_simps assms less_imp_le)
+  from summable_Leibniz'(4)[of ?a, OF tendsto_zero nonneg le, of n]
+    summable_Leibniz'(2)[of ?a, OF tendsto_zero nonneg le, of n]
+    assms
+  show "(\<Sum>k<2*n. (- 1)^ k * ?a k) \<le> arctan x" "arctan x \<le> (\<Sum>k<2 * n + 1. (- 1)^ k * ?a k)"
+    by (auto simp: arctan_series)
+qed
+
+subsection \<open>Bounds on pi using real arctangent\<close>
+
+lemma pi_machin: "pi = 16 * arctan (1 / 5) - 4 * arctan (1 / 239)"
+  using machin
+  by simp
+
+lemma pi_approx: "3.141592653588 \<le> pi" "pi \<le> 3.1415926535899"
+  unfolding pi_machin
+  using arctan_bounds[of "1/5"   4]
+        arctan_bounds[of "1/239" 4]
+  by (simp_all add: eval_nat_numeral)
+
 
 subsection\<open>Inverse Sine\<close>
 
--- a/src/HOL/Real_Vector_Spaces.thy	Thu Jul 28 20:39:46 2016 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Thu Jul 28 20:39:51 2016 +0200
@@ -1766,6 +1766,31 @@
   apply linarith
   done
 
+lemma filterlim_nat_sequentially: "filterlim nat sequentially at_top"
+  unfolding filterlim_at_top
+  apply (rule allI)
+  subgoal for Z by (auto intro!: eventually_at_top_linorderI[where c="int Z"])
+  done
+
+lemma filterlim_floor_sequentially: "filterlim floor at_top at_top"
+  unfolding filterlim_at_top
+  apply (rule allI)
+  subgoal for Z by (auto simp: le_floor_iff intro!: eventually_at_top_linorderI[where c="of_int Z"])
+  done
+
+lemma filterlim_sequentially_iff_filterlim_real:
+  "filterlim f sequentially F \<longleftrightarrow> filterlim (\<lambda>x. real (f x)) at_top F"
+  apply (rule iffI)
+  subgoal using filterlim_compose filterlim_real_sequentially by blast
+  subgoal premises prems
+  proof -
+    have "filterlim (\<lambda>x. nat (floor (real (f x)))) sequentially F"
+      by (intro filterlim_compose[OF filterlim_nat_sequentially]
+          filterlim_compose[OF filterlim_floor_sequentially] prems)
+    then show ?thesis by simp
+  qed
+  done
+
 
 subsubsection \<open>Limits of Sequences\<close>
 
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Jul 28 20:39:46 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Jul 28 20:39:51 2016 +0200
@@ -2148,11 +2148,11 @@
         warn (order_strong_conn (op =) Int_Graph.make Int_Graph.topological_order deps sccs)
       end;
 
-    val fp_eqs = map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctrXs_repTs;
+    val fp_eqs = map dest_TFree Xs ~~ ctrXs_repTs;
 
     val killed_As =
       map_filter (fn (A, set_bos) => if exists is_none set_bos then SOME A else NONE)
-        (unsorted_As ~~ transpose set_boss);
+        (As ~~ transpose set_boss);
 
     val (((pre_bnfs, absT_infos), _), (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0,
              dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors,
@@ -2161,7 +2161,7 @@
              xtor_co_rec_transfers, xtor_co_rec_o_maps, ...},
            lthy)) =
       fixpoint_bnf I (construct_fp mixfixes map_bs rel_bs pred_bs set_bss) fp_bs
-        (map dest_TFree unsorted_As) (map dest_TFree killed_As) fp_eqs empty_comp_cache no_defs_lthy
+        (map dest_TFree As) (map dest_TFree killed_As) fp_eqs empty_comp_cache no_defs_lthy
       handle BAD_DEAD (X, X_backdrop) =>
         (case X_backdrop of
           Type (bad_tc, _) =>
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Thu Jul 28 20:39:46 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Thu Jul 28 20:39:51 2016 +0200
@@ -157,12 +157,7 @@
     val ctr_Tss = map (map fastype_of) ctrss;
 
     val As' = fold (fold Term.add_tfreesT) ctr_Tss [];
-    val unsorted_As' = map (apsnd (K @{sort type})) As';
     val As = map TFree As';
-    val unsorted_As = map TFree unsorted_As';
-
-    val unsortAT = Term.typ_subst_atomic (As ~~ unsorted_As);
-    val unsorted_fpTs = map unsortAT fpTs;
 
     val ((Cs, Xs), _) =
       no_defs_lthy
@@ -217,8 +212,8 @@
     val kss = map (fn n => 1 upto n) ns;
     val mss = map (map length) ctr_Tsss;
 
-    val fp_eqs = map dest_TFree Xs ~~ map unsortAT ctrXs_repTs;
-    val key = key_of_fp_eqs fp unsorted_As unsorted_fpTs fp_eqs;
+    val fp_eqs = map dest_TFree Xs ~~ ctrXs_repTs;
+    val key = key_of_fp_eqs fp As fpTs fp_eqs;
   in
     (case n2m_sugar_of no_defs_lthy key of
       SOME n2m_sugar => (n2m_sugar, no_defs_lthy)
@@ -232,7 +227,7 @@
         val Type (s, Us) :: _ = fpTs;
         val killed_As' =
           (case bnf_of no_defs_lthy s of
-            NONE => unsorted_As'
+            NONE => As'
           | SOME bnf =>
             let
               val Type (_, Ts) = T_of_bnf bnf;
@@ -246,8 +241,8 @@
 
         val (((pre_bnfs, absT_infos), _), (fp_res as {xtor_co_recs = xtor_co_recs0, xtor_co_induct,
                dtor_injects, dtor_ctors, xtor_co_rec_thms, ...}, lthy)) =
-          fixpoint_bnf I (construct_mutualized_fp fp mutual_cliques unsorted_fpTs indexed_fp_ress)
-            fp_bs unsorted_As' killed_As' fp_eqs empty_comp_cache no_defs_lthy;
+          fixpoint_bnf I (construct_mutualized_fp fp mutual_cliques fpTs indexed_fp_ress)
+            fp_bs As' killed_As' fp_eqs empty_comp_cache no_defs_lthy;
 
         val time = time lthy;
         val timer = time (Timer.startRealTimer ());
--- a/src/Pure/ML/ml_antiquotations.ML	Thu Jul 28 20:39:46 2016 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Thu Jul 28 20:39:51 2016 +0200
@@ -89,6 +89,15 @@
       ML_Syntax.print_string (Method.check_name ctxt (name, pos)))));
 
 
+(* locales *)
+
+val _ = Theory.setup
+ (ML_Antiquotation.inline @{binding locale}
+   (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
+      Locale.check (Proof_Context.theory_of ctxt) (name, pos)
+      |> ML_Syntax.print_string)));
+
+
 (* type classes *)
 
 fun class syn = Args.context -- Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, s) =>
--- a/src/Pure/Thy/thy_output.ML	Thu Jul 28 20:39:46 2016 +0200
+++ b/src/Pure/Thy/thy_output.ML	Thu Jul 28 20:39:51 2016 +0200
@@ -572,6 +572,11 @@
     val ctxt' = Variable.auto_fixes eq ctxt;
   in Proof_Context.pretty_term_abbrev ctxt' eq end;
 
+fun pretty_locale ctxt (name, pos) =
+  let
+    val thy = Proof_Context.theory_of ctxt
+  in (Pretty.str o Locale.extern thy o Locale.check thy) (name, pos) end;
+
 fun pretty_class ctxt =
   Pretty.str o Proof_Context.extern_class ctxt o Proof_Context.read_class ctxt;
 
@@ -647,6 +652,7 @@
   basic_entity @{binding const} (Args.const {proper = true, strict = false}) pretty_const #>
   basic_entity @{binding abbrev} (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #>
   basic_entity @{binding typ} Args.typ_abbrev Syntax.pretty_typ #>
+  basic_entity @{binding locale} (Scan.lift (Parse.position Args.name)) pretty_locale #>
   basic_entity @{binding class} (Scan.lift Args.embedded_inner_syntax) pretty_class #>
   basic_entity @{binding type} (Scan.lift Args.embedded) pretty_type #>
   basic_entities @{binding prf} Attrib.thms (pretty_prf false) #>