# HG changeset patch # User wenzelm # Date 1469731191 -7200 # Node ID 113cee845044eedee8da6d6dccc300dfdaaffabc # Parent 36e9732988ceecdadd0f05eee5f468b50c2e9c1e# Parent 0aa33085c8b129dc46018f28f82dfbcb4fce370e merged diff -r 0aa33085c8b1 -r 113cee845044 CONTRIBUTORS --- 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 ----------------------------- diff -r 0aa33085c8b1 -r 113cee845044 NEWS --- 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. diff -r 0aa33085c8b1 -r 113cee845044 src/Doc/Typeclass_Hierarchy/Setup.thy --- 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 \Config.put_global Printer.show_type_emphasis false\ +setup \ +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 +\ + declare [[show_sorts]] end diff -r 0aa33085c8b1 -r 113cee845044 src/Doc/Typeclass_Hierarchy/Typeclass_Hierarchy.thy --- 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 \ 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>\NEWS\ 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 \The hierarchy\ -subsection \Syntactic type classes\ +subsection \Syntactic type classes \label{sec:syntactic-type-class}\ text \ 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. \ + +subsection \Additive and multiplicative semigroups and monoids\ + +text \ + 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>\both\ 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>\abelian\ 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]} +\ + +paragraph \Named collection of theorems\ + +text \ + 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. +\ + + +subsection \Additive and multiplicative groups\ + +text \ + 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 \ (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}. +\ + +paragraph \Mitigating against redundancy by default simplification rules\ + +text \ + 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. +\ + end diff -r 0aa33085c8b1 -r 113cee845044 src/Doc/more_antiquote.ML --- 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; diff -r 0aa33085c8b1 -r 113cee845044 src/HOL/Filter.thy --- 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 "\x. c \ x \ P x" + shows "eventually P at_top" + using assms by (auto simp: eventually_at_top_linorder) + lemma eventually_ge_at_top: "eventually (\x. (c::_::linorder) \ x) at_top" unfolding eventually_at_top_linorder by auto diff -r 0aa33085c8b1 -r 113cee845044 src/HOL/Limits.thy --- 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 \ ((\x. inverse (f x) :: real) \ 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 \ c) F" + assumes "filterlim g at_top F" + shows "((\x. f x / g x) \ 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 \ filterlim (\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 \ 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 \ c) F" "0 < c" "filterlim g at_bot F" @@ -2139,6 +2154,26 @@ lemma LIMSEQ_divide_realpow_zero: "1 < x \ (\n. a / (x ^ n) :: real) \ 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 "((\y. x ^ (f y)) \ 0) F" +proof (rule tendstoI) + fix e::real assume "0 < e" + from tendstoD[OF LIMSEQ_power_zero[OF \norm x < 1\] \0 < e\] + have "\\<^sub>F xa in sequentially. norm (x ^ xa) < e" + by simp + then obtain N where N: "norm (x ^ n) < e" if "n \ N" for n + by (auto simp: eventually_sequentially) + have "\\<^sub>F i in F. f i \ N" + using \filterlim f sequentially F\ + by (simp add: filterlim_at_top) + then show "\\<^sub>F i in F. dist (x ^ f i) 0 < e" + by (eventually_elim) (auto simp: N) +qed + text \Limit of @{term "c^n"} for @{term"\c\ < 1"}.\ lemma LIMSEQ_rabs_realpow_zero: "\c\ < 1 \ (\n. \c\ ^ n :: real) \ 0" diff -r 0aa33085c8b1 -r 113cee845044 src/HOL/Multivariate_Analysis/Complex_Transcendental.thy --- 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: "\x\ < pi/2 \ \x\ \ \tan x\" by (metis abs_arctan_le abs_less_iff arctan_tan minus_less_iff) +lemma arctan_bounds: + assumes "0 \ x" "x < 1" + shows arctan_lower_bound: + "(\k<2 * n. (- 1) ^ k * (1 / real (k * 2 + 1) * x ^ (k * 2 + 1))) \ arctan x" + (is "(\k<_. (- 1)^ k * ?a k) \ _") + and arctan_upper_bound: + "arctan x \ (\k<2 * n + 1. (- 1) ^ k * (1 / real (k * 2 + 1) * x ^ (k * 2 + 1)))" +proof - + have tendsto_zero: "?a \ 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 \ ?a n" for n + by (force intro!: divide_nonneg_nonneg mult_nonneg_nonneg zero_le_power assms) + have le: "?a (Suc n) \ ?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 "(\k<2*n. (- 1)^ k * ?a k) \ arctan x" "arctan x \ (\k<2 * n + 1. (- 1)^ k * ?a k)" + by (auto simp: arctan_series) +qed + +subsection \Bounds on pi using real arctangent\ + +lemma pi_machin: "pi = 16 * arctan (1 / 5) - 4 * arctan (1 / 239)" + using machin + by simp + +lemma pi_approx: "3.141592653588 \ pi" "pi \ 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\Inverse Sine\ diff -r 0aa33085c8b1 -r 113cee845044 src/HOL/Real_Vector_Spaces.thy --- 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 \ filterlim (\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 (\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 \Limits of Sequences\ diff -r 0aa33085c8b1 -r 113cee845044 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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, _) => diff -r 0aa33085c8b1 -r 113cee845044 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- 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 ()); diff -r 0aa33085c8b1 -r 113cee845044 src/Pure/ML/ml_antiquotations.ML --- 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) => diff -r 0aa33085c8b1 -r 113cee845044 src/Pure/Thy/thy_output.ML --- 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) #>