--- 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) #>