--- a/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Wed Jan 10 15:25:09 2018 +0100
@@ -193,4 +193,4 @@
setup Exhaustive_Generators.setup_exhaustive_datatype_interpretation
declare [[quickcheck_full_support = false]]
-end
\ No newline at end of file
+end
--- a/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Guided_Attacker_Example.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Guided_Attacker_Example.thy Wed Jan 10 15:25:09 2018 +0100
@@ -97,4 +97,4 @@
done
qed
-end
\ No newline at end of file
+end
--- a/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Unguided_Attacker_Example.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Unguided_Attacker_Example.thy Wed Jan 10 15:25:09 2018 +0100
@@ -93,4 +93,4 @@
done
qed
-end
\ No newline at end of file
+end
--- a/src/Benchmarks/Record_Benchmark/Record_Benchmark.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/Benchmarks/Record_Benchmark/Record_Benchmark.thy Wed Jan 10 15:25:09 2018 +0100
@@ -424,4 +424,4 @@
print_record many_B
-end
\ No newline at end of file
+end
--- a/src/CTT/CTT.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/CTT/CTT.thy Wed Jan 10 15:25:09 2018 +0100
@@ -434,7 +434,7 @@
(*0 subgoals vs 1 or more*)
val (safe0_brls, safep_brls) =
- List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls
+ List.partition (curry (=) 0 o subgoals_of_brl) safe_brls
fun safestep_tac ctxt thms i =
form_tac ctxt ORELSE
--- a/src/Doc/Corec/Corec.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/Doc/Corec/Corec.thy Wed Jan 10 15:25:09 2018 +0100
@@ -280,7 +280,7 @@
@{command corec}, @{command corecursive}, and @{command friend_of_corec}. In
particular, nesting through the function type can be expressed using
@{text \<lambda>}-abstractions and function applications rather than through composition
-(@{term "op \<circ>"}, the map function for @{text \<Rightarrow>}). For example:
+(@{term "(\<circ>)"}, the map function for @{text \<Rightarrow>}). For example:
\<close>
codatatype 'a language =
@@ -892,7 +892,7 @@
text \<open>
The @{method transfer_prover_eq} proof method replaces the equality relation
-@{term "op ="} with compound relator expressions according to
+@{term "(=)"} with compound relator expressions according to
@{thm [source] relator_eq} before calling @{method transfer_prover} on the
current subgoal. It tends to work better than plain @{method transfer_prover} on
the parametricity proof obligations of @{command corecursive} and
--- a/src/Doc/Datatypes/Datatypes.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Wed Jan 10 15:25:09 2018 +0100
@@ -1410,7 +1410,7 @@
\noindent
The same principle applies for arbitrary type constructors through which
recursion is possible. Notably, the map function for the function type
-(@{text \<Rightarrow>}) is simply composition (@{text "op \<circ>"}):
+(@{text \<Rightarrow>}) is simply composition (@{text "(\<circ>)"}):
\<close>
primrec (*<*)(in early) (*>*)relabel_ft :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
@@ -1436,7 +1436,7 @@
text \<open>
\noindent
For recursion through curried $n$-ary functions, $n$ applications of
-@{term "op \<circ>"} are necessary. The examples below illustrate the case where
+@{term "(\<circ>)"} are necessary. The examples below illustrate the case where
$n = 2$:
\<close>
@@ -1446,7 +1446,7 @@
primrec (*<*)(in early) (*>*)relabel_ft2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
"relabel_ft2 f (FTLeaf2 x) = FTLeaf2 (f x)"
- | "relabel_ft2 f (FTNode2 g) = FTNode2 (op \<circ> (op \<circ> (relabel_ft2 f)) g)"
+ | "relabel_ft2 f (FTNode2 g) = FTNode2 ((\<circ>) ((\<circ>) (relabel_ft2 f)) g)"
text \<open>\blankline\<close>
@@ -2264,7 +2264,7 @@
text \<open>
\noindent
The map function for the function type (@{text \<Rightarrow>}) is composition
-(@{text "op \<circ>"}). For convenience, corecursion through functions can
+(@{text "(\<circ>)"}). For convenience, corecursion through functions can
also be expressed using $\lambda$-abstractions and function application rather
than through composition. For example:
\<close>
@@ -2291,7 +2291,7 @@
text \<open>
\noindent
For recursion through curried $n$-ary functions, $n$ applications of
-@{term "op \<circ>"} are necessary. The examples below illustrate the case where
+@{term "(\<circ>)"} are necessary. The examples below illustrate the case where
$n = 2$:
\<close>
@@ -2303,7 +2303,7 @@
primcorec
(*<*)(in early) (*>*)sm2_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> ('a, 'b) sm2"
where
- "sm2_of_dfa \<delta> F q = SM2 (q \<in> F) (op \<circ> (op \<circ> (sm2_of_dfa \<delta> F)) (\<delta> q))"
+ "sm2_of_dfa \<delta> F q = SM2 (q \<in> F) ((\<circ>) ((\<circ>) (sm2_of_dfa \<delta> F)) (\<delta> q))"
text \<open>\blankline\<close>
@@ -2782,7 +2782,7 @@
text \<open>\blankline\<close>
- lift_definition map_fn :: "('a \<Rightarrow> 'b) \<Rightarrow> ('d, 'a) fn \<Rightarrow> ('d, 'b) fn" is "op \<circ>" .
+ lift_definition map_fn :: "('a \<Rightarrow> 'b) \<Rightarrow> ('d, 'a) fn \<Rightarrow> ('d, 'b) fn" is "(\<circ>)" .
lift_definition set_fn :: "('d, 'a) fn \<Rightarrow> 'a set" is range .
text \<open>\blankline\<close>
@@ -2795,7 +2795,7 @@
lift_definition
rel_fn :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('d, 'a) fn \<Rightarrow> ('d, 'b) fn \<Rightarrow> bool"
is
- "rel_fun (op =)" .
+ "rel_fun (=)" .
text \<open>\blankline\<close>
@@ -2819,7 +2819,7 @@
by transfer auto
next
fix f :: "'a \<Rightarrow> 'b"
- show "set_fn \<circ> map_fn f = op ` f \<circ> set_fn"
+ show "set_fn \<circ> map_fn f = (`) f \<circ> set_fn"
by transfer (auto simp add: comp_def)
next
show "card_order (natLeq +c |UNIV :: 'd set| )"
--- a/src/Doc/Eisbach/Preface.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/Doc/Eisbach/Preface.thy Wed Jan 10 15:25:09 2018 +0100
@@ -33,4 +33,4 @@
with existing Isar concepts such as @{command named_theorems}.
\<close>
-end
\ No newline at end of file
+end
--- a/src/Doc/How_to_Prove_it/How_to_Prove_it.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/Doc/How_to_Prove_it/How_to_Prove_it.thy Wed Jan 10 15:25:09 2018 +0100
@@ -131,4 +131,4 @@
(*<*)
end
-(*>*)
\ No newline at end of file
+(*>*)
--- a/src/Doc/Isar_Ref/Framework.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/Doc/Isar_Ref/Framework.thy Wed Jan 10 15:25:09 2018 +0100
@@ -1028,4 +1028,4 @@
..\<close>''.
\<close>
-end
\ No newline at end of file
+end
--- a/src/Doc/Isar_Ref/Generic.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/Doc/Isar_Ref/Generic.thy Wed Jan 10 15:25:09 2018 +0100
@@ -387,7 +387,7 @@
lemma "0 + (x + 0) = x + 0 + 0" apply simp? oops
text \<open>
- The above attempt \<^emph>\<open>fails\<close>, because @{term "0"} and @{term "op +"} in the
+ The above attempt \<^emph>\<open>fails\<close>, because @{term "0"} and @{term "(+)"} in the
HOL library are declared as generic type class operations, without stating
any algebraic laws yet. More specific types are required to get access to
certain standard simplifications of the theory context, e.g.\ like this:\<close>
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Wed Jan 10 15:25:09 2018 +0100
@@ -1452,7 +1452,7 @@
\<open>Quotient_thm\<close>). Optional theorems \<open>pcr_def\<close> and \<open>pcr_cr_eq_thm\<close> can be
specified to register the parametrized correspondence relation for \<open>\<tau>\<close>.
E.g.\ for @{typ "'a dlist"}, \<open>pcr_def\<close> is \<open>pcr_dlist A \<equiv> list_all2 A \<circ>\<circ>
- cr_dlist\<close> and \<open>pcr_cr_eq_thm\<close> is \<open>pcr_dlist (op =) = (op =)\<close>. This attribute
+ cr_dlist\<close> and \<open>pcr_cr_eq_thm\<close> is \<open>pcr_dlist (=) = (=)\<close>. This attribute
is rather used for low-level manipulation with set-up of the Lifting package
because using of the bundle \<open>\<tau>.lifting\<close> together with the commands @{command
(HOL) lifting_forget} and @{command (HOL) lifting_update} is preferred for
@@ -1539,7 +1539,7 @@
Lemmas involving predicates on relations can also be registered using the
same attribute. For example:
- \<open>bi_unique A \<Longrightarrow> (list_all2 A ===> op =) distinct distinct\<close> \\
+ \<open>bi_unique A \<Longrightarrow> (list_all2 A ===> (=)) distinct distinct\<close> \\
\<open>\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (rel_prod A B)\<close>
Preservation of predicates on relations (\<open>bi_unique, bi_total, right_unique,
@@ -1555,7 +1555,7 @@
quantifiers are transferred.
\<^descr> @{attribute (HOL) relator_eq} attribute collects identity laws for
- relators of various type constructors, e.g. @{term "rel_set (op =) = (op =)"}.
+ relators of various type constructors, e.g. @{term "rel_set (=) = (=)"}.
The @{method (HOL) transfer} method uses these lemmas to infer
transfer rules for non-polymorphic constants on the fly. For examples see
\<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property
@@ -1894,7 +1894,7 @@
@{term "Quickcheck_Narrowing.sum (Quickcheck_Narrowing.cons [])
(Quickcheck_Narrowing.apply
(Quickcheck_Narrowing.apply
- (Quickcheck_Narrowing.cons (op #))
+ (Quickcheck_Narrowing.cons (#))
narrowing)
narrowing)"}.
If a symbolic variable of type @{typ "_ list"} is evaluated, it is
@@ -1909,7 +1909,7 @@
"Quickcheck_Narrowing.Narrowing_constructor i args"}, where @{term "i ::
integer"} denotes the index in the sum of refinements. In the above
example for lists, @{term "0"} corresponds to @{term "[]"} and @{term "1"}
- to @{term "op #"}.
+ to @{term "(#)"}.
The command @{command (HOL) "code_datatype"} sets up @{const
partial_term_of} such that the @{term "i"}-th refinement is interpreted as
--- a/src/Doc/Isar_Ref/Proof_Script.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/Doc/Isar_Ref/Proof_Script.thy Wed Jan 10 15:25:09 2018 +0100
@@ -278,4 +278,4 @@
definitions, it should not never appear in production theories.
\<close>
-end
\ No newline at end of file
+end
--- a/src/Doc/Isar_Ref/Symbols.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/Doc/Isar_Ref/Symbols.thy Wed Jan 10 15:25:09 2018 +0100
@@ -37,4 +37,4 @@
\end{center}
\<close>
-end
\ No newline at end of file
+end
--- a/src/Doc/JEdit/JEdit.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/Doc/JEdit/JEdit.thy Wed Jan 10 15:25:09 2018 +0100
@@ -2171,4 +2171,4 @@
which sometimes helps in low-memory situations.
\<close>
-end
\ No newline at end of file
+end
--- a/src/Doc/Locales/Examples1.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/Doc/Locales/Examples1.thy Wed Jan 10 15:25:09 2018 +0100
@@ -19,8 +19,8 @@
Section~\ref{sec:local-interpretation}.
As an example, consider the type of integers @{typ int}. The
- relation @{term "op \<le>"} is a total order over @{typ int}. We start
- with the interpretation that @{term "op \<le>"} is a partial order. The
+ relation @{term "(\<le>)"} is a total order over @{typ int}. We start
+ with the interpretation that @{term "(\<le>)"} is a partial order. The
facilities of the interpretation command are explored gradually in
three versions.
\<close>
@@ -32,11 +32,11 @@
text \<open>
The command \isakeyword{interpretation} is for the interpretation of
locale in theories. In the following example, the parameter of locale
- @{text partial_order} is replaced by @{term "op \<le> :: int \<Rightarrow> int \<Rightarrow>
+ @{text partial_order} is replaced by @{term "(\<le>) :: int \<Rightarrow> int \<Rightarrow>
bool"} and the locale instance is interpreted in the current
theory.\<close>
- interpretation %visible int: partial_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
+ interpretation %visible int: partial_order "(\<le>) :: int \<Rightarrow> int \<Rightarrow> bool"
txt \<open>\normalsize
The argument of the command is a simple \emph{locale expression}
consisting of the name of the interpreted locale, which is
@@ -70,17 +70,17 @@
The prefix @{text int} is applied to all names introduced in locale
conclusions including names introduced in definitions. The
qualified name @{text int.less} is short for
- the interpretation of the definition, which is @{text "partial_order.less op \<le>"}.
+ the interpretation of the definition, which is @{text "partial_order.less (\<le>)"}.
Qualified name and expanded form may be used almost
interchangeably.%
-\footnote{Since @{term "op \<le>"} is polymorphic, for @{text "partial_order.less op \<le>"} a
+\footnote{Since @{term "(\<le>)"} is polymorphic, for @{text "partial_order.less (\<le>)"} a
more general type will be inferred than for @{text int.less} which
is over type @{typ int}.}
The former is preferred on output, as for example in the theorem
@{thm [source] int.less_le_trans}: @{thm [display, indent=2]
int.less_le_trans}
Both notations for the strict order are not satisfactory. The
- constant @{term "op <"} is the strict order for @{typ int}.
+ constant @{term "(<)"} is the strict order for @{typ int}.
In order to allow for the desired replacement, interpretation
accepts \emph{equations} in addition to the parameter instantiation.
These follow the locale expression and are indicated with the
--- a/src/Doc/Locales/Examples2.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/Doc/Locales/Examples2.thy Wed Jan 10 15:25:09 2018 +0100
@@ -1,18 +1,18 @@
theory Examples2
imports Examples
begin
- interpretation %visible int: partial_order "op \<le> :: [int, int] \<Rightarrow> bool"
+ interpretation %visible int: partial_order "(\<le>) :: [int, int] \<Rightarrow> bool"
rewrites "int.less x y = (x < y)"
proof -
txt \<open>\normalsize The goals are now:
@{subgoals [display]}
The proof that~@{text \<le>} is a partial order is as above.\<close>
- show "partial_order (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)"
+ show "partial_order ((\<le>) :: int \<Rightarrow> int \<Rightarrow> bool)"
by unfold_locales auto
txt \<open>\normalsize The second goal is shown by unfolding the
definition of @{term "partial_order.less"}.\<close>
- show "partial_order.less op \<le> x y = (x < y)"
- unfolding partial_order.less_def [OF \<open>partial_order (op \<le>)\<close>]
+ show "partial_order.less (\<le>) x y = (x < y)"
+ unfolding partial_order.less_def [OF \<open>partial_order (\<le>)\<close>]
by auto
qed
--- a/src/Doc/Main/Main_Doc.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/Doc/Main/Main_Doc.thy Wed Jan 10 15:25:09 2018 +0100
@@ -297,7 +297,7 @@
@{const Transitive_Closure.trancl} & @{term_type_only Transitive_Closure.trancl "('a*'a)set\<Rightarrow>('a*'a)set"}\\
@{const Transitive_Closure.reflcl} & @{term_type_only Transitive_Closure.reflcl "('a*'a)set\<Rightarrow>('a*'a)set"}\\
@{const Transitive_Closure.acyclic} & @{term_type_only Transitive_Closure.acyclic "('a*'a)set\<Rightarrow>bool"}\\
-@{const compower} & @{term_type_only "op ^^ :: ('a*'a)set\<Rightarrow>nat\<Rightarrow>('a*'a)set" "('a*'a)set\<Rightarrow>nat\<Rightarrow>('a*'a)set"}\\
+@{const compower} & @{term_type_only "(^^) :: ('a*'a)set\<Rightarrow>nat\<Rightarrow>('a*'a)set" "('a*'a)set\<Rightarrow>nat\<Rightarrow>('a*'a)set"}\\
\end{tabular}
\subsubsection*{Syntax}
@@ -345,15 +345,15 @@
\<^bigskip>
\begin{tabular}{@ {} lllllll @ {}}
-@{term "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
-@{term "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
-@{term "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
-@{term "op ^ :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
-@{term "op div :: nat \<Rightarrow> nat \<Rightarrow> nat"}&
-@{term "op mod :: nat \<Rightarrow> nat \<Rightarrow> nat"}&
-@{term "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"}\\
-@{term "op \<le> :: nat \<Rightarrow> nat \<Rightarrow> bool"} &
-@{term "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"} &
+@{term "(+) :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
+@{term "(-) :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
+@{term "( * ) :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
+@{term "(^) :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
+@{term "(div) :: nat \<Rightarrow> nat \<Rightarrow> nat"}&
+@{term "(mod) :: nat \<Rightarrow> nat \<Rightarrow> nat"}&
+@{term "(dvd) :: nat \<Rightarrow> nat \<Rightarrow> bool"}\\
+@{term "(\<le>) :: nat \<Rightarrow> nat \<Rightarrow> bool"} &
+@{term "(<) :: nat \<Rightarrow> nat \<Rightarrow> bool"} &
@{term "min :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
@{term "max :: nat \<Rightarrow> nat \<Rightarrow> nat"} &
@{term "Min :: nat set \<Rightarrow> nat"} &
@@ -362,8 +362,8 @@
\begin{tabular}{@ {} l @ {~::~} l @ {}}
@{const Nat.of_nat} & @{typeof Nat.of_nat}\\
-@{term "op ^^ :: ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"} &
- @{term_type_only "op ^^ :: ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"}
+@{term "(^^) :: ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"} &
+ @{term_type_only "(^^) :: ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"}
\end{tabular}
\section*{Int}
@@ -372,16 +372,16 @@
\<^bigskip>
\begin{tabular}{@ {} llllllll @ {}}
-@{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} &
-@{term "op - :: int \<Rightarrow> int \<Rightarrow> int"} &
+@{term "(+) :: int \<Rightarrow> int \<Rightarrow> int"} &
+@{term "(-) :: int \<Rightarrow> int \<Rightarrow> int"} &
@{term "uminus :: int \<Rightarrow> int"} &
-@{term "op * :: int \<Rightarrow> int \<Rightarrow> int"} &
-@{term "op ^ :: int \<Rightarrow> nat \<Rightarrow> int"} &
-@{term "op div :: int \<Rightarrow> int \<Rightarrow> int"}&
-@{term "op mod :: int \<Rightarrow> int \<Rightarrow> int"}&
-@{term "op dvd :: int \<Rightarrow> int \<Rightarrow> bool"}\\
-@{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"} &
-@{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"} &
+@{term "( * ) :: int \<Rightarrow> int \<Rightarrow> int"} &
+@{term "(^) :: int \<Rightarrow> nat \<Rightarrow> int"} &
+@{term "(div) :: int \<Rightarrow> int \<Rightarrow> int"}&
+@{term "(mod) :: int \<Rightarrow> int \<Rightarrow> int"}&
+@{term "(dvd) :: int \<Rightarrow> int \<Rightarrow> bool"}\\
+@{term "(\<le>) :: int \<Rightarrow> int \<Rightarrow> bool"} &
+@{term "(<) :: int \<Rightarrow> int \<Rightarrow> bool"} &
@{term "min :: int \<Rightarrow> int \<Rightarrow> int"} &
@{term "max :: int \<Rightarrow> int \<Rightarrow> int"} &
@{term "Min :: int set \<Rightarrow> int"} &
--- a/src/Doc/Prog_Prove/Basics.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/Doc/Prog_Prove/Basics.thy Wed Jan 10 15:25:09 2018 +0100
@@ -40,9 +40,9 @@
\begin{warn}
There are many predefined infix symbols like @{text "+"} and @{text"\<le>"}.
-The name of the corresponding binary function is @{term"op +"},
+The name of the corresponding binary function is @{term"(+)"},
not just @{text"+"}. That is, @{term"x + y"} is nice surface syntax
-(``syntactic sugar'') for \noquotes{@{term[source]"op + x y"}}.
+(``syntactic sugar'') for \noquotes{@{term[source]"(+) x y"}}.
\end{warn}
HOL also supports some basic constructs from functional programming:
@@ -152,4 +152,4 @@
*}
(*<*)
end
-(*>*)
\ No newline at end of file
+(*>*)
--- a/src/Doc/Prog_Prove/LaTeXsugar.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/Doc/Prog_Prove/LaTeXsugar.thy Wed Jan 10 15:25:09 2018 +0100
@@ -60,4 +60,4 @@
*}
end
-(*>*)
\ No newline at end of file
+(*>*)
--- a/src/Doc/System/Environment.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/Doc/System/Environment.thy Wed Jan 10 15:25:09 2018 +0100
@@ -505,4 +505,4 @@
characters are \<open>\<^bold>X\<^bold>Y\<close>.
\<close>
-end
\ No newline at end of file
+end
--- a/src/Doc/System/Misc.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/Doc/System/Misc.thy Wed Jan 10 15:25:09 2018 +0100
@@ -226,4 +226,4 @@
id of the @{setting ISABELLE_HOME} directory.
\<close>
-end
\ No newline at end of file
+end
--- a/src/Doc/System/Presentation.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/Doc/System/Presentation.thy Wed Jan 10 15:25:09 2018 +0100
@@ -286,4 +286,4 @@
isabelle latex -o pdf\<close>}
\<close>
-end
\ No newline at end of file
+end
--- a/src/Doc/Tutorial/Types/Pairs.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/Doc/Tutorial/Types/Pairs.thy Wed Jan 10 15:25:09 2018 +0100
@@ -110,7 +110,7 @@
@{subgoals[display,indent=0]}
Again, simplification produces a term suitable for @{thm[source]prod.split}
as above. If you are worried about the strange form of the premise:
-@{text"case_prod (op =)"} is short for @{term"\<lambda>(x,y). x=y"}.
+@{text"case_prod (=)"} is short for @{term"\<lambda>(x,y). x=y"}.
The same proof procedure works for
*}
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Wed Jan 10 15:25:09 2018 +0100
@@ -68,7 +68,7 @@
and linv: "inv(x) ** x = one"
print_locale! lgrp thm lgrp_def lgrp_axioms_def
-locale add_lgrp = semi "op ++" for sum (infixl "++" 60) +
+locale add_lgrp = semi "(++)" for sum (infixl "++" 60) +
fixes zero and neg
assumes lzero: "zero ++ x = x"
and lneg: "neg(x) ++ x = zero"
@@ -106,7 +106,7 @@
end
print_locale! logic
-locale use_decl = l: logic + semi "op ||"
+locale use_decl = l: logic + semi "(||)"
print_locale! use_decl thm use_decl_def
locale extra_type =
@@ -376,7 +376,7 @@
end
-sublocale order_with_def < dual: order' "op >>"
+sublocale order_with_def < dual: order' "(>>)"
apply unfold_locales
unfolding greater_def
apply (rule refl) apply (blast intro: trans)
@@ -438,13 +438,13 @@
subsection \<open>Sublocale, then interpretation in theory\<close>
-interpretation int?: lgrp "op +" "0" "minus"
+interpretation int?: lgrp "(+)" "0" "minus"
proof unfold_locales
qed (rule int_assoc int_zero int_minus)+
thm int.assoc int.semi_axioms
-interpretation int2?: semi "op +"
+interpretation int2?: semi "(+)"
by unfold_locales (* subsumed, thm int2.assoc not generated *)
ML \<open>(Global_Theory.get_thms @{theory} "int2.assoc";
@@ -457,7 +457,7 @@
subsection \<open>Interpretation in theory, then sublocale\<close>
-interpretation fol: logic "op +" "minus"
+interpretation fol: logic "(+)" "minus"
by unfold_locales (rule int_assoc int_minus2)+
locale logic2 =
@@ -503,11 +503,11 @@
end
-interpretation x: logic_o "op \<and>" "Not"
+interpretation x: logic_o "(\<and>)" "Not"
rewrites bool_logic_o: "x.lor_o(x, y) \<longleftrightarrow> x \<or> y"
proof -
- show bool_logic_o: "PROP logic_o(op \<and>, Not)" by unfold_locales fast+
- show "logic_o.lor_o(op \<and>, Not, x, y) \<longleftrightarrow> x \<or> y"
+ show bool_logic_o: "PROP logic_o((\<and>), Not)" by unfold_locales fast+
+ show "logic_o.lor_o((\<and>), Not, x, y) \<longleftrightarrow> x \<or> y"
by (unfold logic_o.lor_o_def [OF bool_logic_o]) fast
qed
@@ -759,8 +759,8 @@
text \<open>Interpreted versions\<close>
-lemma "0 = glob_one ((op +))" by (rule int.def.one_def)
-lemma "- x = glob_inv(op +, x)" by (rule int.def.inv_def)
+lemma "0 = glob_one ((+))" by (rule int.def.one_def)
+lemma "- x = glob_inv((+), x)" by (rule int.def.inv_def)
text \<open>Roundup applies rewrite morphisms at declaration level in DFS tree\<close>
@@ -792,18 +792,18 @@
lemma True
proof
- interpret "local": lgrp "op +" "0" "minus"
+ interpret "local": lgrp "(+)" "0" "minus"
by unfold_locales (* subsumed *)
{
fix zero :: int
assume "!!x. zero + x = x" "!!x. (-x) + x = zero"
- then interpret local_fixed: lgrp "op +" zero "minus"
+ then interpret local_fixed: lgrp "(+)" zero "minus"
by unfold_locales
thm local_fixed.lone
- print_dependencies! lgrp "op +" 0 minus + lgrp "op +" zero minus
+ print_dependencies! lgrp "(+)" 0 minus + lgrp "(+)" zero minus
}
assume "!!x zero. zero + x = x" "!!x zero. (-x) + x = zero"
- then interpret local_free: lgrp "op +" zero "minus" for zero
+ then interpret local_free: lgrp "(+)" zero "minus" for zero
by unfold_locales
thm local_free.lone [where ?zero = 0]
qed
--- a/src/FOLP/IFOLP.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/FOLP/IFOLP.thy Wed Jan 10 15:25:09 2018 +0100
@@ -259,7 +259,7 @@
and concl = discard_proof (Logic.strip_assums_concl prem)
in
if exists (fn hyp => hyp aconv concl) hyps
- then case distinct (op =) (filter (fn hyp => Term.could_unify (hyp, concl)) hyps) of
+ then case distinct (=) (filter (fn hyp => Term.could_unify (hyp, concl)) hyps) of
[_] => assume_tac ctxt i
| _ => no_tac
else no_tac
@@ -522,7 +522,7 @@
lemmas pred_congs = pred1_cong pred2_cong pred3_cong
(*special case for the equality predicate!*)
-lemmas eq_cong = pred2_cong [where P = "op ="]
+lemmas eq_cong = pred2_cong [where P = "(=)"]
(*** Simplifications of assumed implications.
--- a/src/HOL/Algebra/Complete_Lattice.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Algebra/Complete_Lattice.thy Wed Jan 10 15:25:09 2018 +0100
@@ -1171,7 +1171,7 @@
subsubsection \<open>The Powerset of a Set is a Complete Lattice\<close>
theorem powerset_is_complete_lattice:
- "complete_lattice \<lparr>carrier = Pow A, eq = op =, le = (op \<subseteq>)\<rparr>"
+ "complete_lattice \<lparr>carrier = Pow A, eq = (=), le = (\<subseteq>)\<rparr>"
(is "complete_lattice ?L")
proof (rule partial_order.complete_latticeI)
show "partial_order ?L"
--- a/src/HOL/Algebra/Divisibility.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Algebra/Divisibility.thy Wed Jan 10 15:25:09 2018 +0100
@@ -145,7 +145,7 @@
definition associated :: "[_, 'a, 'a] \<Rightarrow> bool" (infix "\<sim>\<index>" 55)
where "a \<sim>\<^bsub>G\<^esub> b \<longleftrightarrow> a divides\<^bsub>G\<^esub> b \<and> b divides\<^bsub>G\<^esub> a"
-abbreviation "division_rel G \<equiv> \<lparr>carrier = carrier G, eq = op \<sim>\<^bsub>G\<^esub>, le = (op divides\<^bsub>G\<^esub>)\<rparr>"
+abbreviation "division_rel G \<equiv> \<lparr>carrier = carrier G, eq = (\<sim>\<^bsub>G\<^esub>), le = (divides\<^bsub>G\<^esub>)\<rparr>"
definition properfactor :: "[_, 'a, 'a] \<Rightarrow> bool"
where "properfactor G a b \<longleftrightarrow> a divides\<^bsub>G\<^esub> b \<and> \<not>(b divides\<^bsub>G\<^esub> a)"
@@ -857,13 +857,13 @@
subsubsection \<open>Function definitions\<close>
definition factors :: "[_, 'a list, 'a] \<Rightarrow> bool"
- where "factors G fs a \<longleftrightarrow> (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>\<^bsub>G\<^esub>) fs \<one>\<^bsub>G\<^esub> = a"
+ where "factors G fs a \<longleftrightarrow> (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (\<otimes>\<^bsub>G\<^esub>) fs \<one>\<^bsub>G\<^esub> = a"
definition wfactors ::"[_, 'a list, 'a] \<Rightarrow> bool"
- where "wfactors G fs a \<longleftrightarrow> (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>\<^bsub>G\<^esub>) fs \<one>\<^bsub>G\<^esub> \<sim>\<^bsub>G\<^esub> a"
+ where "wfactors G fs a \<longleftrightarrow> (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (\<otimes>\<^bsub>G\<^esub>) fs \<one>\<^bsub>G\<^esub> \<sim>\<^bsub>G\<^esub> a"
abbreviation list_assoc :: "('a,_) monoid_scheme \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "[\<sim>]\<index>" 44)
- where "list_assoc G \<equiv> list_all2 (op \<sim>\<^bsub>G\<^esub>)"
+ where "list_assoc G \<equiv> list_all2 (\<sim>\<^bsub>G\<^esub>)"
definition essentially_equal :: "[_, 'a list, 'a list] \<Rightarrow> bool"
where "essentially_equal G fs1 fs2 \<longleftrightarrow> (\<exists>fs1'. fs1 <~~> fs1' \<and> fs1' [\<sim>]\<^bsub>G\<^esub> fs2)"
@@ -1043,12 +1043,12 @@
lemma (in monoid) multlist_closed [simp, intro]:
assumes ascarr: "set fs \<subseteq> carrier G"
- shows "foldr (op \<otimes>) fs \<one> \<in> carrier G"
+ shows "foldr (\<otimes>) fs \<one> \<in> carrier G"
using ascarr by (induct fs) simp_all
lemma (in comm_monoid) multlist_dividesI (*[intro]*):
assumes "f \<in> set fs" and "f \<in> carrier G" and "set fs \<subseteq> carrier G"
- shows "f divides (foldr (op \<otimes>) fs \<one>)"
+ shows "f divides (foldr (\<otimes>) fs \<one>)"
using assms
apply (induct fs)
apply simp
@@ -1062,7 +1062,7 @@
lemma (in comm_monoid_cancel) multlist_listassoc_cong:
assumes "fs [\<sim>] fs'"
and "set fs \<subseteq> carrier G" and "set fs' \<subseteq> carrier G"
- shows "foldr (op \<otimes>) fs \<one> \<sim> foldr (op \<otimes>) fs' \<one>"
+ shows "foldr (\<otimes>) fs \<one> \<sim> foldr (\<otimes>) fs' \<one>"
using assms
proof (induct fs arbitrary: fs', simp)
case (Cons a as fs')
@@ -1073,16 +1073,16 @@
assume "a \<sim> b"
and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"
and ascarr: "set as \<subseteq> carrier G"
- then have p: "a \<otimes> foldr op \<otimes> as \<one> \<sim> b \<otimes> foldr op \<otimes> as \<one>"
+ then have p: "a \<otimes> foldr (\<otimes>) as \<one> \<sim> b \<otimes> foldr (\<otimes>) as \<one>"
by (fast intro: mult_cong_l)
also
assume "as [\<sim>] bs"
and bscarr: "set bs \<subseteq> carrier G"
- and "\<And>fs'. \<lbrakk>as [\<sim>] fs'; set fs' \<subseteq> carrier G\<rbrakk> \<Longrightarrow> foldr op \<otimes> as \<one> \<sim> foldr op \<otimes> fs' \<one>"
- then have "foldr op \<otimes> as \<one> \<sim> foldr op \<otimes> bs \<one>" by simp
- with ascarr bscarr bcarr have "b \<otimes> foldr op \<otimes> as \<one> \<sim> b \<otimes> foldr op \<otimes> bs \<one>"
+ and "\<And>fs'. \<lbrakk>as [\<sim>] fs'; set fs' \<subseteq> carrier G\<rbrakk> \<Longrightarrow> foldr (\<otimes>) as \<one> \<sim> foldr (\<otimes>) fs' \<one>"
+ then have "foldr (\<otimes>) as \<one> \<sim> foldr (\<otimes>) bs \<one>" by simp
+ with ascarr bscarr bcarr have "b \<otimes> foldr (\<otimes>) as \<one> \<sim> b \<otimes> foldr (\<otimes>) bs \<one>"
by (fast intro: mult_cong_r)
- finally show "a \<otimes> foldr op \<otimes> as \<one> \<sim> b \<otimes> foldr op \<otimes> bs \<one>"
+ finally show "a \<otimes> foldr (\<otimes>) as \<one> \<sim> b \<otimes> foldr (\<otimes>) bs \<one>"
by (simp add: ascarr bscarr acarr bcarr)
qed
qed
@@ -1090,21 +1090,21 @@
lemma (in comm_monoid) multlist_perm_cong:
assumes prm: "as <~~> bs"
and ascarr: "set as \<subseteq> carrier G"
- shows "foldr (op \<otimes>) as \<one> = foldr (op \<otimes>) bs \<one>"
+ shows "foldr (\<otimes>) as \<one> = foldr (\<otimes>) bs \<one>"
using prm ascarr
apply (induct, simp, clarsimp simp add: m_ac, clarsimp)
proof clarsimp
fix xs ys zs
assume "xs <~~> ys" "set xs \<subseteq> carrier G"
then have "set ys \<subseteq> carrier G" by (rule perm_closed)
- moreover assume "set ys \<subseteq> carrier G \<Longrightarrow> foldr op \<otimes> ys \<one> = foldr op \<otimes> zs \<one>"
- ultimately show "foldr op \<otimes> ys \<one> = foldr op \<otimes> zs \<one>" by simp
+ moreover assume "set ys \<subseteq> carrier G \<Longrightarrow> foldr (\<otimes>) ys \<one> = foldr (\<otimes>) zs \<one>"
+ ultimately show "foldr (\<otimes>) ys \<one> = foldr (\<otimes>) zs \<one>" by simp
qed
lemma (in comm_monoid_cancel) multlist_ee_cong:
assumes "essentially_equal G fs fs'"
and "set fs \<subseteq> carrier G" and "set fs' \<subseteq> carrier G"
- shows "foldr (op \<otimes>) fs \<one> \<sim> foldr (op \<otimes>) fs' \<one>"
+ shows "foldr (\<otimes>) fs \<one> \<sim> foldr (\<otimes>) fs' \<one>"
using assms
apply (elim essentially_equalE)
apply (simp add: multlist_perm_cong multlist_listassoc_cong perm_closed)
@@ -1116,27 +1116,27 @@
lemma wfactorsI:
fixes G (structure)
assumes "\<forall>f\<in>set fs. irreducible G f"
- and "foldr (op \<otimes>) fs \<one> \<sim> a"
+ and "foldr (\<otimes>) fs \<one> \<sim> a"
shows "wfactors G fs a"
using assms unfolding wfactors_def by simp
lemma wfactorsE:
fixes G (structure)
assumes wf: "wfactors G fs a"
- and e: "\<lbrakk>\<forall>f\<in>set fs. irreducible G f; foldr (op \<otimes>) fs \<one> \<sim> a\<rbrakk> \<Longrightarrow> P"
+ and e: "\<lbrakk>\<forall>f\<in>set fs. irreducible G f; foldr (\<otimes>) fs \<one> \<sim> a\<rbrakk> \<Longrightarrow> P"
shows "P"
using wf unfolding wfactors_def by (fast dest: e)
lemma (in monoid) factorsI:
assumes "\<forall>f\<in>set fs. irreducible G f"
- and "foldr (op \<otimes>) fs \<one> = a"
+ and "foldr (\<otimes>) fs \<one> = a"
shows "factors G fs a"
using assms unfolding factors_def by simp
lemma factorsE:
fixes G (structure)
assumes f: "factors G fs a"
- and e: "\<lbrakk>\<forall>f\<in>set fs. irreducible G f; foldr (op \<otimes>) fs \<one> = a\<rbrakk> \<Longrightarrow> P"
+ and e: "\<lbrakk>\<forall>f\<in>set fs. irreducible G f; foldr (\<otimes>) fs \<one> = a\<rbrakk> \<Longrightarrow> P"
shows "P"
using f unfolding factors_def by (simp add: e)
@@ -1185,14 +1185,14 @@
from fs wf have "irreducible G f" by (simp add: wfactors_def)
then have fnunit: "f \<notin> Units G" by (fast elim: irreducibleE)
- from fs wf have a: "f \<otimes> foldr (op \<otimes>) fs' \<one> \<sim> a" by (simp add: wfactors_def)
+ from fs wf have a: "f \<otimes> foldr (\<otimes>) fs' \<one> \<sim> a" by (simp add: wfactors_def)
note aunit
also from fs wf
- have a: "f \<otimes> foldr (op \<otimes>) fs' \<one> \<sim> a" by (simp add: wfactors_def)
- have "a \<sim> f \<otimes> foldr (op \<otimes>) fs' \<one>"
+ have a: "f \<otimes> foldr (\<otimes>) fs' \<one> \<sim> a" by (simp add: wfactors_def)
+ have "a \<sim> f \<otimes> foldr (\<otimes>) fs' \<one>"
by (simp add: Units_closed[OF aunit] a[symmetric])
- finally have "f \<otimes> foldr (op \<otimes>) fs' \<one> \<in> Units G" by simp
+ finally have "f \<otimes> foldr (\<otimes>) fs' \<one> \<in> Units G" by simp
then have "f \<in> Units G" by (intro unit_factor[of f], simp+)
with fnunit show ?thesis by contradiction
qed
@@ -1209,10 +1209,10 @@
apply (elim wfactorsE, intro wfactorsI)
apply (metis assms(2) assms(4) assms(5) irrlist_listassoc_cong)
proof -
- from asc[symmetric] have "foldr op \<otimes> fs' \<one> \<sim> foldr op \<otimes> fs \<one>"
+ from asc[symmetric] have "foldr (\<otimes>) fs' \<one> \<sim> foldr (\<otimes>) fs \<one>"
by (simp add: multlist_listassoc_cong carr)
- also assume "foldr op \<otimes> fs \<one> \<sim> a"
- finally show "foldr op \<otimes> fs' \<one> \<sim> a" by (simp add: carr)
+ also assume "foldr (\<otimes>) fs \<one> \<sim> a"
+ finally show "foldr (\<otimes>) fs' \<one> \<sim> a" by (simp add: carr)
qed
lemma (in comm_monoid) wfactors_perm_cong_l:
@@ -1251,8 +1251,8 @@
shows "wfactors G fs a'"
using fac
proof (elim wfactorsE, intro wfactorsI)
- assume "foldr op \<otimes> fs \<one> \<sim> a" also note aa'
- finally show "foldr op \<otimes> fs \<one> \<sim> a'" by simp
+ assume "foldr (\<otimes>) fs \<one> \<sim> a" also note aa'
+ finally show "foldr (\<otimes>) fs \<one> \<sim> a'" by simp
qed
@@ -1296,11 +1296,11 @@
using afs bfs
proof (elim wfactorsE)
from prm have [simp]: "set bs \<subseteq> carrier G" by (simp add: perm_closed)
- assume "foldr op \<otimes> as \<one> \<sim> a"
- then have "a \<sim> foldr op \<otimes> as \<one>" by (rule associated_sym, simp+)
+ assume "foldr (\<otimes>) as \<one> \<sim> a"
+ then have "a \<sim> foldr (\<otimes>) as \<one>" by (rule associated_sym, simp+)
also from prm
- have "foldr op \<otimes> as \<one> = foldr op \<otimes> bs \<one>" by (rule multlist_perm_cong, simp)
- also assume "foldr op \<otimes> bs \<one> \<sim> b"
+ have "foldr (\<otimes>) as \<one> = foldr (\<otimes>) bs \<one>" by (rule multlist_perm_cong, simp)
+ also assume "foldr (\<otimes>) bs \<one> \<sim> b"
finally show "a \<sim> b" by simp
qed
@@ -1313,11 +1313,11 @@
shows "a \<sim> b"
using afs bfs
proof (elim wfactorsE)
- assume "foldr op \<otimes> as \<one> \<sim> a"
- then have "a \<sim> foldr op \<otimes> as \<one>" by (rule associated_sym, simp+)
+ assume "foldr (\<otimes>) as \<one> \<sim> a"
+ then have "a \<sim> foldr (\<otimes>) as \<one>" by (rule associated_sym, simp+)
also from assoc
- have "foldr op \<otimes> as \<one> \<sim> foldr op \<otimes> bs \<one>" by (rule multlist_listassoc_cong, simp+)
- also assume "foldr op \<otimes> bs \<one> \<sim> b"
+ have "foldr (\<otimes>) as \<one> \<sim> foldr (\<otimes>) bs \<one>" by (rule multlist_listassoc_cong, simp+)
+ also assume "foldr (\<otimes>) bs \<one> \<sim> b"
finally show "a \<sim> b" by simp
qed
@@ -2912,10 +2912,10 @@
lemma (in comm_monoid_cancel) multlist_prime_pos:
assumes carr: "a \<in> carrier G" "set as \<subseteq> carrier G"
and aprime: "prime G a"
- and "a divides (foldr (op \<otimes>) as \<one>)"
+ and "a divides (foldr (\<otimes>) as \<one>)"
shows "\<exists>i<length as. a divides (as!i)"
proof -
- have r[rule_format]: "set as \<subseteq> carrier G \<and> a divides (foldr (op \<otimes>) as \<one>)
+ have r[rule_format]: "set as \<subseteq> carrier G \<and> a divides (foldr (\<otimes>) as \<one>)
\<longrightarrow> (\<exists>i. i < length as \<and> a divides (as!i))"
apply (induct as)
apply clarsimp defer 1
@@ -2928,10 +2928,10 @@
by (elim primeE, simp)
next
fix aa as
- assume ih[rule_format]: "a divides foldr op \<otimes> as \<one> \<longrightarrow> (\<exists>i<length as. a divides as ! i)"
+ assume ih[rule_format]: "a divides foldr (\<otimes>) as \<one> \<longrightarrow> (\<exists>i<length as. a divides as ! i)"
and carr': "aa \<in> carrier G" "set as \<subseteq> carrier G"
- and "a divides aa \<otimes> foldr op \<otimes> as \<one>"
- with carr aprime have "a divides aa \<or> a divides foldr op \<otimes> as \<one>"
+ and "a divides aa \<otimes> foldr (\<otimes>) as \<one>"
+ with carr aprime have "a divides aa \<or> a divides foldr (\<otimes>) as \<one>"
by (intro prime_divides) simp+
then show "\<exists>i<Suc (length as). a divides (aa # as) ! i"
proof
@@ -2940,7 +2940,7 @@
have "0 < Suc (length as)" by simp
with p1 show ?thesis by fast
next
- assume "a divides foldr op \<otimes> as \<one>"
+ assume "a divides foldr (\<otimes>) as \<one>"
from ih [OF this] obtain i where "a divides as ! i" and len: "i < length as" by auto
then have p1: "a divides (aa#as) ! (Suc i)" by simp
from len have "Suc i < Suc (length as)" by simp
@@ -2998,9 +2998,9 @@
note carr [simp] = acarr ahcarr ascarr as'carr a'carr
note ahdvda
- also from afs' have "a divides (foldr (op \<otimes>) as' \<one>)"
+ also from afs' have "a divides (foldr (\<otimes>) as' \<one>)"
by (elim wfactorsE associatedE, simp)
- finally have "ah divides (foldr (op \<otimes>) as' \<one>)"
+ finally have "ah divides (foldr (\<otimes>) as' \<one>)"
by simp
with ahprime have "\<exists>i<length as'. ah divides as'!i"
by (intro multlist_prime_pos) simp_all
--- a/src/HOL/Algebra/Group.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Algebra/Group.thy Wed Jan 10 15:25:09 2018 +0100
@@ -676,7 +676,7 @@
(* Contributed by Joachim Breitner *)
lemma (in group) int_pow_is_hom:
- "x \<in> carrier G \<Longrightarrow> (op[^] x) \<in> hom \<lparr> carrier = UNIV, mult = op +, one = 0::int \<rparr> G "
+ "x \<in> carrier G \<Longrightarrow> (([^]) x) \<in> hom \<lparr> carrier = UNIV, mult = (+), one = 0::int \<rparr> G "
unfolding hom_def by (simp add: int_pow_mult)
@@ -773,7 +773,7 @@
text_raw \<open>\label{sec:subgroup-lattice}\<close>
theorem (in group) subgroups_partial_order:
- "partial_order \<lparr>carrier = {H. subgroup H G}, eq = op =, le = (op \<subseteq>)\<rparr>"
+ "partial_order \<lparr>carrier = {H. subgroup H G}, eq = (=), le = (\<subseteq>)\<rparr>"
by standard simp_all
lemma (in group) subgroup_self:
@@ -818,7 +818,7 @@
qed
theorem (in group) subgroups_complete_lattice:
- "complete_lattice \<lparr>carrier = {H. subgroup H G}, eq = op =, le = (op \<subseteq>)\<rparr>"
+ "complete_lattice \<lparr>carrier = {H. subgroup H G}, eq = (=), le = (\<subseteq>)\<rparr>"
(is "complete_lattice ?L")
proof (rule partial_order.complete_lattice_criterion1)
show "partial_order ?L" by (rule subgroups_partial_order)
--- a/src/HOL/Algebra/IntRing.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Algebra/IntRing.thy Wed Jan 10 15:25:09 2018 +0100
@@ -23,7 +23,7 @@
subsection \<open>\<open>\<Z>\<close>: The Set of Integers as Algebraic Structure\<close>
abbreviation int_ring :: "int ring" ("\<Z>")
- where "int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = (op +)\<rparr>"
+ where "int_ring \<equiv> \<lparr>carrier = UNIV, mult = ( * ), one = 1, zero = 0, add = (+)\<rparr>"
lemma int_Zcarr [intro!, simp]: "k \<in> carrier \<Z>"
by simp
@@ -172,27 +172,27 @@
by simp_all
interpretation int (* FIXME [unfolded UNIV] *) :
- partial_order "\<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr>"
- rewrites "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> = UNIV"
- and "le \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> x y = (x \<le> y)"
- and "lless \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> x y = (x < y)"
+ partial_order "\<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr>"
+ rewrites "carrier \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> = UNIV"
+ and "le \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> x y = (x \<le> y)"
+ and "lless \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> x y = (x < y)"
proof -
- show "partial_order \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr>"
+ show "partial_order \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr>"
by standard simp_all
- show "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> = UNIV"
+ show "carrier \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> = UNIV"
by simp
- show "le \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> x y = (x \<le> y)"
+ show "le \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> x y = (x \<le> y)"
by simp
- show "lless \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> x y = (x < y)"
+ show "lless \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> x y = (x < y)"
by (simp add: lless_def) auto
qed
interpretation int (* FIXME [unfolded UNIV] *) :
- lattice "\<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr>"
- rewrites "join \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> x y = max x y"
- and "meet \<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr> x y = min x y"
+ lattice "\<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr>"
+ rewrites "join \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> x y = max x y"
+ and "meet \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> x y = min x y"
proof -
- let ?Z = "\<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr>"
+ let ?Z = "\<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr>"
show "lattice ?Z"
apply unfold_locales
apply (simp add: least_def Upper_def)
@@ -214,7 +214,7 @@
qed
interpretation int (* [unfolded UNIV] *) :
- total_order "\<lparr>carrier = UNIV::int set, eq = op =, le = (op \<le>)\<rparr>"
+ total_order "\<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr>"
by standard clarsimp
--- a/src/HOL/Algebra/Multiplicative_Group.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Algebra/Multiplicative_Group.thy Wed Jan 10 15:25:09 2018 +0100
@@ -580,7 +580,7 @@
lemma mult_mult_of: "mult (mult_of R) = mult R"
by (simp add: mult_of_def)
-lemma nat_pow_mult_of: "op [^]\<^bsub>mult_of R\<^esub> = (op [^]\<^bsub>R\<^esub> :: _ \<Rightarrow> nat \<Rightarrow> _)"
+lemma nat_pow_mult_of: "([^]\<^bsub>mult_of R\<^esub>) = (([^]\<^bsub>R\<^esub>) :: _ \<Rightarrow> nat \<Rightarrow> _)"
by (simp add: mult_of_def fun_eq_iff nat_pow_def)
lemma one_mult_of: "\<one>\<^bsub>mult_of R\<^esub> = \<one>\<^bsub>R\<^esub>"
@@ -762,7 +762,7 @@
note mult_of_simps[simp]
have finite': "finite (carrier (mult_of R))" using finite by (rule finite_mult_of)
- interpret G:group "mult_of R" rewrites "op [^]\<^bsub>mult_of R\<^esub> = (op [^] :: _ \<Rightarrow> nat \<Rightarrow> _)" and "\<one>\<^bsub>mult_of R\<^esub> = \<one>"
+ interpret G:group "mult_of R" rewrites "([^]\<^bsub>mult_of R\<^esub>) = (([^]) :: _ \<Rightarrow> nat \<Rightarrow> _)" and "\<one>\<^bsub>mult_of R\<^esub> = \<one>"
by (rule field_mult_group) simp_all
from exists
@@ -826,7 +826,7 @@
have finite': "finite (carrier (mult_of R))" using finite by (rule finite_mult_of)
interpret G: group "mult_of R" rewrites
- "op [^]\<^bsub>mult_of R\<^esub> = (op [^] :: _ \<Rightarrow> nat \<Rightarrow> _)" and "\<one>\<^bsub>mult_of R\<^esub> = \<one>"
+ "([^]\<^bsub>mult_of R\<^esub>) = (([^]) :: _ \<Rightarrow> nat \<Rightarrow> _)" and "\<one>\<^bsub>mult_of R\<^esub> = \<one>"
by (rule field_mult_group) (simp_all add: fun_eq_iff nat_pow_def)
let ?N = "\<lambda> x . card {a \<in> carrier (mult_of R). group.ord (mult_of R) a = x}"
--- a/src/HOL/Algebra/Order.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Algebra/Order.thy Wed Jan 10 15:25:09 2018 +0100
@@ -22,7 +22,7 @@
abbreviation inv_gorder :: "_ \<Rightarrow> 'a gorder" where
"inv_gorder L \<equiv>
\<lparr> carrier = carrier L,
- eq = op .=\<^bsub>L\<^esub>,
+ eq = (.=\<^bsub>L\<^esub>),
le = (\<lambda> x y. y \<sqsubseteq>\<^bsub>L \<^esub>x) \<rparr>"
lemma inv_gorder_inv:
@@ -591,7 +591,7 @@
subsection \<open>Partial orders where \<open>eq\<close> is the Equality\<close>
locale partial_order = weak_partial_order +
- assumes eq_is_equal: "op .= = op ="
+ assumes eq_is_equal: "(.=) = (=)"
begin
declare weak_le_antisym [rule del]
--- a/src/HOL/Algebra/QuotRing.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Algebra/QuotRing.thy Wed Jan 10 15:25:09 2018 +0100
@@ -115,7 +115,7 @@
text \<open>This is a ring homomorphism\<close>
-lemma (in ideal) rcos_ring_hom: "(op +> I) \<in> ring_hom R (R Quot I)"
+lemma (in ideal) rcos_ring_hom: "((+>) I) \<in> ring_hom R (R Quot I)"
apply (rule ring_hom_memI)
apply (simp add: FactRing_def a_rcosetsI[OF a_subset])
apply (simp add: FactRing_def rcoset_mult_add)
@@ -123,7 +123,7 @@
apply (simp add: FactRing_def)
done
-lemma (in ideal) rcos_ring_hom_ring: "ring_hom_ring R (R Quot I) (op +> I)"
+lemma (in ideal) rcos_ring_hom_ring: "ring_hom_ring R (R Quot I) ((+>) I)"
apply (rule ring_hom_ringI)
apply (rule is_ring, rule quotient_is_ring)
apply (simp add: FactRing_def a_rcosetsI[OF a_subset])
@@ -151,7 +151,7 @@
text \<open>Cosets as a ring homomorphism on crings\<close>
lemma (in ideal) rcos_ring_hom_cring:
assumes "cring R"
- shows "ring_hom_cring R (R Quot I) (op +> I)"
+ shows "ring_hom_cring R (R Quot I) ((+>) I)"
proof -
interpret cring R by fact
show ?thesis
@@ -203,7 +203,7 @@
text \<open>Generating right cosets of a prime ideal is a homomorphism
on commutative rings\<close>
-lemma (in primeideal) rcos_ring_hom_cring: "ring_hom_cring R (R Quot I) (op +> I)"
+lemma (in primeideal) rcos_ring_hom_cring: "ring_hom_cring R (R Quot I) ((+>) I)"
by (rule rcos_ring_hom_cring) (rule is_cring)
--- a/src/HOL/Algebra/Sylow.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Algebra/Sylow.thy Wed Jan 10 15:25:09 2018 +0100
@@ -80,7 +80,7 @@
proof
show "inj_on (\<lambda>z\<in>H. m1 \<otimes> z) H"
by (simp add: inj_on_def l_cancel [of m1 x y, THEN iffD1] H_def m1)
- show "restrict (op \<otimes> m1) H \<in> H \<rightarrow> M1"
+ show "restrict ((\<otimes>) m1) H \<in> H \<rightarrow> M1"
proof (rule restrictI)
fix z
assume zH: "z \<in> H"
--- a/src/HOL/Algebra/UnivPoly.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy Wed Jan 10 15:25:09 2018 +0100
@@ -1808,7 +1808,7 @@
definition
INTEG :: "int ring"
- where "INTEG = \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = (op +)\<rparr>"
+ where "INTEG = \<lparr>carrier = UNIV, mult = ( * ), one = 1, zero = 0, add = (+)\<rparr>"
lemma INTEG_cring: "cring INTEG"
by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
--- a/src/HOL/Analysis/Ball_Volume.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Ball_Volume.thy Wed Jan 10 15:25:09 2018 +0100
@@ -144,7 +144,7 @@
(auto simp: mult_ac ennreal_mult' [symmetric] indicator_def intro!: nn_integral_cong)
also have "(\<integral>\<^sup>+ (y::real). indicator {-r..r} y * (sqrt (r ^ 2 - y ^ 2)) ^ card A \<partial>lborel) =
(\<integral>\<^sup>+ (y::real). r ^ card A * indicator {-1..1} y * (sqrt (1 - y ^ 2)) ^ card A
- \<partial>(distr lborel borel (op * (1/r))))" using \<open>r > 0\<close>
+ \<partial>(distr lborel borel (( * ) (1/r))))" using \<open>r > 0\<close>
by (subst nn_integral_distr)
(auto simp: indicator_def field_simps real_sqrt_divide intro!: nn_integral_cong)
also have "\<dots> = (\<integral>\<^sup>+ x. ennreal (r ^ Suc (card A)) *
--- a/src/HOL/Analysis/Binary_Product_Measure.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Binary_Product_Measure.thy Wed Jan 10 15:25:09 2018 +0100
@@ -163,7 +163,7 @@
lemma measurable_split_conv:
"(\<lambda>(x, y). f x y) \<in> measurable A B \<longleftrightarrow> (\<lambda>x. f (fst x) (snd x)) \<in> measurable A B"
- by (intro arg_cong2[where f="op \<in>"]) auto
+ by (intro arg_cong2[where f="(\<in>)"]) auto
lemma measurable_pair_swap': "(\<lambda>(x,y). (y, x)) \<in> measurable (M1 \<Otimes>\<^sub>M M2) (M2 \<Otimes>\<^sub>M M1)"
by (auto intro!: measurable_Pair simp: measurable_split_conv)
--- a/src/HOL/Analysis/Bochner_Integration.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Bochner_Integration.thy Wed Jan 10 15:25:09 2018 +0100
@@ -497,7 +497,7 @@
have "ennreal (norm (?s - ?t)) = norm (simple_bochner_integral M (\<lambda>x. s x - t x))"
using s t by (subst simple_bochner_integral_diff) auto
also have "\<dots> \<le> simple_bochner_integral M (\<lambda>x. norm (s x - t x))"
- using simple_bochner_integrable_compose2[of "op -" M "s" "t"] s t
+ using simple_bochner_integrable_compose2[of "(-)" M "s" "t"] s t
by (auto intro!: simple_bochner_integral_norm_bound)
also have "\<dots> = (\<integral>\<^sup>+x. norm (s x - t x) \<partial>M)"
using simple_bochner_integrable_compose2[of "\<lambda>x y. norm (x - y)" M "s" "t"] s t
@@ -1855,7 +1855,7 @@
have sf[measurable]: "\<And>i. simple_function M (s' i)"
unfolding s'_def using s(1)
- by (intro simple_function_compose2[where h="op *\<^sub>R"] simple_function_indicator) auto
+ by (intro simple_function_compose2[where h="( *\<^sub>R)"] simple_function_indicator) auto
{ fix i
have "\<And>z. {y. s' i z = y \<and> y \<in> s' i ` space M \<and> y \<noteq> 0 \<and> z \<in> space M} =
@@ -2282,7 +2282,7 @@
shows "integrable (density M g) f \<longleftrightarrow> integrable M (\<lambda>x. g x *\<^sub>R f x)"
unfolding integrable_iff_bounded using nn
apply (simp add: nn_integral_density less_top[symmetric])
- apply (intro arg_cong2[where f="op ="] refl nn_integral_cong_AE)
+ apply (intro arg_cong2[where f="(=)"] refl nn_integral_cong_AE)
apply (auto simp: ennreal_mult)
done
--- a/src/HOL/Analysis/Borel_Space.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Borel_Space.thy Wed Jan 10 15:25:09 2018 +0100
@@ -110,8 +110,8 @@
show "eventually (\<lambda>h. (f (x + h) - f x) / h \<ge> 0) (at 0)"
proof (subst eventually_at_topological, intro exI conjI ballI impI)
have "open (interior A)" by simp
- hence "open (op + (-x) ` interior A)" by (rule open_translation)
- also have "(op + (-x) ` interior A) = ?A'" by auto
+ hence "open ((+) (-x) ` interior A)" by (rule open_translation)
+ also have "((+) (-x) ` interior A) = ?A'" by auto
finally show "open ?A'" .
next
from \<open>x \<in> interior A\<close> show "0 \<in> ?A'" by auto
@@ -1701,7 +1701,7 @@
definition [simp]: "is_borel f M \<longleftrightarrow> f \<in> borel_measurable M"
-lemma is_borel_transfer[transfer_rule]: "rel_fun (rel_fun op = pcr_ennreal) op = is_borel is_borel"
+lemma is_borel_transfer[transfer_rule]: "rel_fun (rel_fun (=) pcr_ennreal) (=) is_borel is_borel"
unfolding is_borel_def[abs_def]
proof (safe intro!: rel_funI ext dest!: rel_fun_eq_pcr_ennreal[THEN iffD1])
fix f and M :: "'a measure"
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy Wed Jan 10 15:25:09 2018 +0100
@@ -569,7 +569,7 @@
qed (auto simp: assms intro!: blinfun.comp)
lemma transfer_bounded_bilinear_bounded_linear[transfer_rule]:
- "(rel_fun (rel_fun op = (pcr_blinfun op = op =)) op =) bounded_bilinear bounded_linear"
+ "(rel_fun (rel_fun (=) (pcr_blinfun (=) (=))) (=)) bounded_bilinear bounded_linear"
by (auto simp: pcr_blinfun_def cr_blinfun_def rel_fun_def OO_def
intro!: transfer_bounded_bilinear_bounded_linearI)
@@ -623,7 +623,7 @@
lift_definition blinfun_compose::
"'a::real_normed_vector \<Rightarrow>\<^sub>L 'b::real_normed_vector \<Rightarrow>
'c::real_normed_vector \<Rightarrow>\<^sub>L 'a \<Rightarrow>
- 'c \<Rightarrow>\<^sub>L 'b" (infixl "o\<^sub>L" 55) is "op o"
+ 'c \<Rightarrow>\<^sub>L 'b" (infixl "o\<^sub>L" 55) is "(o)"
parametric comp_transfer
unfolding o_def
by (rule bounded_linear_compose)
@@ -635,7 +635,7 @@
"norm (f o\<^sub>L g) \<le> norm f * norm g"
by transfer (rule onorm_compose)
-lemma bounded_bilinear_blinfun_compose[bounded_bilinear]: "bounded_bilinear op o\<^sub>L"
+lemma bounded_bilinear_blinfun_compose[bounded_bilinear]: "bounded_bilinear (o\<^sub>L)"
by unfold_locales
(auto intro!: blinfun_eqI exI[where x=1] simp: blinfun.bilinear_simps norm_blinfun_compose)
@@ -645,7 +645,7 @@
by (auto simp: blinfun.bilinear_simps intro!: blinfun_eqI)
-lift_definition blinfun_inner_right::"'a::real_inner \<Rightarrow> 'a \<Rightarrow>\<^sub>L real" is "op \<bullet>"
+lift_definition blinfun_inner_right::"'a::real_inner \<Rightarrow> 'a \<Rightarrow>\<^sub>L real" is "(\<bullet>)"
by (rule bounded_linear_inner_right)
declare blinfun_inner_right.rep_eq[simp]
@@ -661,7 +661,7 @@
by transfer (rule bounded_bilinear.flip[OF bounded_bilinear_inner])
-lift_definition blinfun_scaleR_right::"real \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a::real_normed_vector" is "op *\<^sub>R"
+lift_definition blinfun_scaleR_right::"real \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a::real_normed_vector" is "( *\<^sub>R)"
by (rule bounded_linear_scaleR_right)
declare blinfun_scaleR_right.rep_eq[simp]
@@ -677,7 +677,7 @@
by transfer (rule bounded_bilinear.flip[OF bounded_bilinear_scaleR])
-lift_definition blinfun_mult_right::"'a \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a::real_normed_algebra" is "op *"
+lift_definition blinfun_mult_right::"'a \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'a::real_normed_algebra" is "( * )"
by (rule bounded_linear_mult_right)
declare blinfun_mult_right.rep_eq[simp]
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Wed Jan 10 15:25:09 2018 +0100
@@ -146,7 +146,7 @@
by (subst card_Un_disjoint[symmetric])
(auto simp: nF_def intro!: sum.cong arg_cong[where f=card])
also have "\<dots> = 1 * card {f\<in>F. compo' f \<and> bnd f} + 2 * card {f\<in>F. compo' f \<and> \<not> bnd f}"
- using assms(4,5) by (fastforce intro!: arg_cong2[where f="op +"] sum_multicount)
+ using assms(4,5) by (fastforce intro!: arg_cong2[where f="(+)"] sum_multicount)
finally have "odd ((\<Sum>s | s \<in> S \<and> \<not> compo s. nF s) + card {s\<in>S. compo s})"
using assms(6,8) by simp
moreover have "(\<Sum>s | s \<in> S \<and> \<not> compo s. nF s) =
@@ -4221,13 +4221,13 @@
show "ANR (C \<inter> \<Union>\<U>)"
unfolding Int_Union
proof (rule Suc)
- show "finite (op \<inter> C ` \<U>)"
+ show "finite ((\<inter>) C ` \<U>)"
by (simp add: insert.hyps(1))
- show "\<And>Ca. Ca \<in> op \<inter> C ` \<U> \<Longrightarrow> closed Ca"
+ show "\<And>Ca. Ca \<in> (\<inter>) C ` \<U> \<Longrightarrow> closed Ca"
by (metis (no_types, hide_lams) Suc.prems(2) closed_Int subsetD imageE insert.prems insertI1 insertI2)
- show "\<And>Ca. Ca \<in> op \<inter> C ` \<U> \<Longrightarrow> convex Ca"
+ show "\<And>Ca. Ca \<in> (\<inter>) C ` \<U> \<Longrightarrow> convex Ca"
by (metis (mono_tags, lifting) Suc.prems(3) convex_Int imageE insert.prems insert_subset subsetCE)
- show "card (op \<inter> C ` \<U>) < n"
+ show "card ((\<inter>) C ` \<U>) < n"
proof -
have "card \<T> \<le> n"
by (meson Suc.prems(4) not_less not_less_eq)
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Wed Jan 10 15:25:09 2018 +0100
@@ -39,7 +39,7 @@
instantiation vec :: (times, finite) times
begin
-definition "op * \<equiv> (\<lambda> x y. (\<chi> i. (x$i) * (y$i)))"
+definition "( * ) \<equiv> (\<lambda> x y. (\<chi> i. (x$i) * (y$i)))"
instance ..
end
@@ -714,9 +714,9 @@
unfolding matrix_vector_mul_assoc B matrix_vector_mul_lid . }
moreover
{ assume A: "\<forall>x y. A *v x = A *v y \<longrightarrow> x = y"
- hence i: "inj (op *v A)" unfolding inj_on_def by auto
+ hence i: "inj (( *v) A)" unfolding inj_on_def by auto
from linear_injective_left_inverse[OF matrix_vector_mul_linear i]
- obtain g where g: "linear g" "g \<circ> op *v A = id" by blast
+ obtain g where g: "linear g" "g \<circ> ( *v) A = id" by blast
have "matrix g ** A = mat 1"
unfolding matrix_eq matrix_vector_mul_lid matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)]
using g(2) by (simp add: fun_eq_iff)
@@ -738,11 +738,11 @@
{ fix x :: "real ^ 'm"
have "A *v (B *v x) = x"
by (simp add: matrix_vector_mul_lid matrix_vector_mul_assoc AB) }
- hence "surj (op *v A)" unfolding surj_def by metis }
+ hence "surj (( *v) A)" unfolding surj_def by metis }
moreover
- { assume sf: "surj (op *v A)"
+ { assume sf: "surj (( *v) A)"
from linear_surjective_right_inverse[OF matrix_vector_mul_linear sf]
- obtain g:: "real ^'m \<Rightarrow> real ^'n" where g: "linear g" "op *v A \<circ> g = id"
+ obtain g:: "real ^'m \<Rightarrow> real ^'n" where g: "linear g" "( *v) A \<circ> g = id"
by blast
have "A ** (matrix g) = mat 1"
@@ -878,7 +878,7 @@
proof -
{ fix A A' :: "real ^'n^'n"
assume AA': "A ** A' = mat 1"
- have sA: "surj (op *v A)"
+ have sA: "surj (( *v) A)"
unfolding surj_def
apply clarify
apply (rule_tac x="(A' *v y)" in exI)
@@ -1235,7 +1235,7 @@
where "finite s" "cbox (x - (\<chi> i. d)) (x + (\<chi> i. d)) = convex hull s"
proof -
from assms obtain s where "finite s"
- and "cbox (x - sum (op *\<^sub>R d) Basis) (x + sum (op *\<^sub>R d) Basis) = convex hull s"
+ and "cbox (x - sum (( *\<^sub>R) d) Basis) (x + sum (( *\<^sub>R) d) Basis) = convex hull s"
by (rule cube_convex_hull)
with that[of s] show thesis
by (simp add: const_vector_cart)
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Wed Jan 10 15:25:09 2018 +0100
@@ -236,7 +236,7 @@
lemma continuous_on_joinpaths_D1:
"continuous_on {0..1} (g1 +++ g2) \<Longrightarrow> continuous_on {0..1} g1"
- apply (rule continuous_on_eq [of _ "(g1 +++ g2) o (op*(inverse 2))"])
+ apply (rule continuous_on_eq [of _ "(g1 +++ g2) o (( * )(inverse 2))"])
apply (rule continuous_intros | simp)+
apply (auto elim!: continuous_on_subset simp: joinpaths_def)
done
@@ -251,10 +251,10 @@
lemma piecewise_differentiable_D1:
"(g1 +++ g2) piecewise_differentiable_on {0..1} \<Longrightarrow> g1 piecewise_differentiable_on {0..1}"
apply (clarsimp simp add: piecewise_differentiable_on_def dest!: continuous_on_joinpaths_D1)
- apply (rule_tac x="insert 1 ((op*2)`s)" in exI)
+ apply (rule_tac x="insert 1 ((( * )2)`s)" in exI)
apply simp
apply (intro ballI)
- apply (rule_tac d="dist (x/2) (1/2)" and f = "(g1 +++ g2) o (op*(inverse 2))"
+ apply (rule_tac d="dist (x/2) (1/2)" and f = "(g1 +++ g2) o (( * )(inverse 2))"
in differentiable_transform_within)
apply (auto simp: dist_real_def joinpaths_def)
apply (rule differentiable_chain_within derivative_intros | simp)+
@@ -537,40 +537,40 @@
and co12: "continuous_on ({0..1} - s) (\<lambda>x. vector_derivative (g1 +++ g2) (at x))"
and g12D: "\<forall>x\<in>{0..1} - s. g1 +++ g2 differentiable at x"
using assms by (auto simp: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
- then have g1D: "g1 differentiable at x" if "x \<in> {0..1} - insert 1 (op * 2 ` s)" for x
- apply (rule_tac d="dist (x/2) (1/2)" and f = "(g1 +++ g2) o (op*(inverse 2))" in differentiable_transform_within)
+ then have g1D: "g1 differentiable at x" if "x \<in> {0..1} - insert 1 (( * ) 2 ` s)" for x
+ apply (rule_tac d="dist (x/2) (1/2)" and f = "(g1 +++ g2) o (( * )(inverse 2))" in differentiable_transform_within)
using that
apply (simp_all add: dist_real_def joinpaths_def)
apply (rule differentiable_chain_at derivative_intros | force)+
done
- have [simp]: "vector_derivative (g1 \<circ> op * 2) (at (x/2)) = 2 *\<^sub>R vector_derivative g1 (at x)"
- if "x \<in> {0..1} - insert 1 (op * 2 ` s)" for x
+ have [simp]: "vector_derivative (g1 \<circ> ( * ) 2) (at (x/2)) = 2 *\<^sub>R vector_derivative g1 (at x)"
+ if "x \<in> {0..1} - insert 1 (( * ) 2 ` s)" for x
apply (subst vector_derivative_chain_at)
using that
apply (rule derivative_eq_intros g1D | simp)+
done
have "continuous_on ({0..1/2} - insert (1/2) s) (\<lambda>x. vector_derivative (g1 +++ g2) (at x))"
using co12 by (rule continuous_on_subset) force
- then have coDhalf: "continuous_on ({0..1/2} - insert (1/2) s) (\<lambda>x. vector_derivative (g1 o op*2) (at x))"
+ then have coDhalf: "continuous_on ({0..1/2} - insert (1/2) s) (\<lambda>x. vector_derivative (g1 o ( * )2) (at x))"
apply (rule continuous_on_eq [OF _ vector_derivative_at])
- apply (rule_tac f="g1 o op*2" and d="dist x (1/2)" in has_vector_derivative_transform_within)
+ apply (rule_tac f="g1 o ( * )2" and d="dist x (1/2)" in has_vector_derivative_transform_within)
apply (simp_all add: dist_norm joinpaths_def vector_derivative_works [symmetric])
apply (force intro: g1D differentiable_chain_at)
apply auto
done
- have "continuous_on ({0..1} - insert 1 (op * 2 ` s))
- ((\<lambda>x. 1/2 * vector_derivative (g1 o op*2) (at x)) o op*(1/2))"
+ have "continuous_on ({0..1} - insert 1 (( * ) 2 ` s))
+ ((\<lambda>x. 1/2 * vector_derivative (g1 o ( * )2) (at x)) o ( * )(1/2))"
apply (rule continuous_intros)+
using coDhalf
apply (simp add: scaleR_conv_of_real image_set_diff image_image)
done
- then have con_g1: "continuous_on ({0..1} - insert 1 (op * 2 ` s)) (\<lambda>x. vector_derivative g1 (at x))"
+ then have con_g1: "continuous_on ({0..1} - insert 1 (( * ) 2 ` s)) (\<lambda>x. vector_derivative g1 (at x))"
by (rule continuous_on_eq) (simp add: scaleR_conv_of_real)
have "continuous_on {0..1} g1"
using continuous_on_joinpaths_D1 assms piecewise_C1_differentiable_on_def by blast
with \<open>finite s\<close> show ?thesis
apply (clarsimp simp add: piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
- apply (rule_tac x="insert 1 ((op*2)`s)" in exI)
+ apply (rule_tac x="insert 1 ((( * )2)`s)" in exI)
apply (simp add: g1D con_g1)
done
qed
@@ -785,7 +785,7 @@
proof -
obtain s where "finite s" "g C1_differentiable_on ({0..1} - s)"
using assms by (auto simp: valid_path_def piecewise_C1_differentiable_on_def)
- then have "finite (op - 1 ` s)" "(reversepath g C1_differentiable_on ({0..1} - op - 1 ` s))"
+ then have "finite ((-) 1 ` s)" "(reversepath g C1_differentiable_on ({0..1} - (-) 1 ` s))"
apply (auto simp: reversepath_def)
apply (rule C1_differentiable_compose [of "\<lambda>x::real. 1-x" _ g, unfolded o_def])
apply (auto simp: C1_differentiable_on_eq)
@@ -805,7 +805,7 @@
shows "(f has_contour_integral (-i)) (reversepath g)"
proof -
{ fix s x
- assume xs: "g C1_differentiable_on ({0..1} - s)" "x \<notin> op - 1 ` s" "0 \<le> x" "x \<le> 1"
+ assume xs: "g C1_differentiable_on ({0..1} - s)" "x \<notin> (-) 1 ` s" "0 \<le> x" "x \<le> 1"
have "vector_derivative (\<lambda>x. g (1 - x)) (at x within {0..1}) =
- vector_derivative g (at (1 - x) within {0..1})"
proof -
@@ -870,7 +870,7 @@
using assms
apply (auto simp: valid_path_def piecewise_C1_differentiable_on_def continuous_on_joinpaths)
apply (rule continuous_intros | simp)+
- apply (force intro: finite_vimageI [where h = "op*2"] inj_onI)
+ apply (force intro: finite_vimageI [where h = "( * )2"] inj_onI)
done
moreover have "(g2 o (\<lambda>x. 2*x-1)) piecewise_C1_differentiable_on {1/2..1}"
apply (rule piecewise_C1_differentiable_compose)
@@ -941,9 +941,9 @@
apply (auto simp: algebra_simps vector_derivative_works)
done
have "((\<lambda>x. f ((g1 +++ g2) x) * vector_derivative (g1 +++ g2) (at x)) has_integral i1) {0..1/2}"
- apply (rule has_integral_spike_finite [OF _ _ i1, of "insert (1/2) (op*2 -` s1)"])
+ apply (rule has_integral_spike_finite [OF _ _ i1, of "insert (1/2) (( * )2 -` s1)"])
using s1
- apply (force intro: finite_vimageI [where h = "op*2"] inj_onI)
+ apply (force intro: finite_vimageI [where h = "( * )2"] inj_onI)
apply (clarsimp simp add: joinpaths_def scaleR_conv_of_real mult_ac g1)
done
moreover have "((\<lambda>x. f ((g1 +++ g2) x) * vector_derivative (g1 +++ g2) (at x)) has_integral i2) {1/2..1}"
@@ -1437,7 +1437,7 @@
by (simp add: has_vector_derivative_def scaleR_conv_of_real)
have "(f has_field_derivative (f' (g x))) (at (g x) within g ` {a..b})"
using assms by (metis a atLeastAtMost_iff b DERIV_subset image_subset_iff less_eq_real_def)
- then have fdiff: "(f has_derivative op * (f' (g x))) (at (g x) within g ` {a..b})"
+ then have fdiff: "(f has_derivative ( * ) (f' (g x))) (at (g x) within g ` {a..b})"
by (simp add: has_field_derivative_def)
have "((\<lambda>x. f (g x)) has_vector_derivative f' (g x) * vector_derivative g (at x within {a..b})) (at x within {a..b})"
using diff_chain_within [OF gdiff fdiff]
@@ -3589,11 +3589,11 @@
assumes \<gamma>: "valid_path \<gamma>" and 0: "0 \<notin> path_image \<gamma>"
shows "winding_number(uminus \<circ> \<gamma>) 0 = winding_number \<gamma> 0"
proof -
- have "op / 1 contour_integrable_on \<gamma>"
+ have "(/) 1 contour_integrable_on \<gamma>"
using "0" \<gamma> contour_integrable_inversediff by fastforce
- then have "((\<lambda>z. 1/z) has_contour_integral contour_integral \<gamma> (op / 1)) \<gamma>"
+ then have "((\<lambda>z. 1/z) has_contour_integral contour_integral \<gamma> ((/) 1)) \<gamma>"
by (rule has_contour_integral_integral)
- then have "((\<lambda>z. 1 / - z) has_contour_integral - contour_integral \<gamma> (op / 1)) \<gamma>"
+ then have "((\<lambda>z. 1 / - z) has_contour_integral - contour_integral \<gamma> ((/) 1)) \<gamma>"
using has_contour_integral_neg by auto
then show ?thesis
using assms
@@ -5914,7 +5914,7 @@
case 0 then show ?case by simp
next
case (Suc n z)
- have holo0: "f holomorphic_on op * u ` s"
+ have holo0: "f holomorphic_on ( * ) u ` s"
by (meson fg f holomorphic_on_subset image_subset_iff)
have holo1: "(\<lambda>w. f (u * w)) holomorphic_on s"
apply (rule holomorphic_on_compose [where g=f, unfolded o_def])
@@ -5942,7 +5942,7 @@
apply (blast intro: fg)
done
also have "... = u * u ^ n * deriv ((deriv ^^ n) f) (u * z)"
- apply (subst complex_derivative_chain [where g = "(deriv ^^ n) f" and f = "op* u", unfolded o_def])
+ apply (subst complex_derivative_chain [where g = "(deriv ^^ n) f" and f = "( * ) u", unfolded o_def])
apply (rule derivative_intros)
using Suc.prems field_differentiable_def f fg has_field_derivative_higher_deriv t apply blast
apply (simp add: deriv_linear)
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Wed Jan 10 15:25:09 2018 +0100
@@ -16,7 +16,7 @@
lemma has_derivative_mult_right:
fixes c:: "'a :: real_normed_algebra"
- shows "((op * c) has_derivative (op * c)) F"
+ shows "((( * ) c) has_derivative (( * ) c)) F"
by (rule has_derivative_mult_right [OF has_derivative_id])
lemma has_derivative_of_real[derivative_intros, simp]:
@@ -25,7 +25,7 @@
lemma has_vector_derivative_real_field:
"DERIV f (of_real a) :> f' \<Longrightarrow> ((\<lambda>x. f (of_real x)) has_vector_derivative f') (at a within s)"
- using has_derivative_compose[of of_real of_real a _ f "op * f'"]
+ using has_derivative_compose[of of_real of_real a _ f "( * ) f'"]
by (simp add: scaleR_conv_of_real ac_simps has_vector_derivative_def has_field_derivative_def)
lemmas has_vector_derivative_real_complex = has_vector_derivative_real_field
@@ -69,10 +69,10 @@
shows "b \<le> Im(l)"
by (metis assms tendsto_le [OF _ _ tendsto_const] tendsto_Im)
-lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = op * 0"
+lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = ( * ) 0"
by auto
-lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = op * 1"
+lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = ( * ) 1"
by auto
lemma continuous_mult_left:
@@ -315,7 +315,7 @@
lemma holomorphic_cong: "s = t ==> (\<And>x. x \<in> s \<Longrightarrow> f x = g x) \<Longrightarrow> f holomorphic_on s \<longleftrightarrow> g holomorphic_on t"
by (metis holomorphic_transform)
-lemma holomorphic_on_linear [simp, holomorphic_intros]: "(op * c) holomorphic_on s"
+lemma holomorphic_on_linear [simp, holomorphic_intros]: "(( * ) c) holomorphic_on s"
unfolding holomorphic_on_def by (metis field_differentiable_linear)
lemma holomorphic_on_const [simp, holomorphic_intros]: "(\<lambda>z. c) holomorphic_on s"
@@ -570,7 +570,7 @@
finally show ?thesis .
qed
-lemma analytic_on_linear [analytic_intros,simp]: "(op * c) analytic_on s"
+lemma analytic_on_linear [analytic_intros,simp]: "(( * ) c) analytic_on s"
by (auto simp add: analytic_on_holomorphic)
lemma analytic_on_const [analytic_intros,simp]: "(\<lambda>z. c) analytic_on s"
@@ -839,7 +839,7 @@
show ?thesis
unfolding has_field_derivative_def
proof (rule has_derivative_sequence [OF cvs _ _ x])
- show "\<forall>n. \<forall>x\<in>s. (f n has_derivative (op * (f' n x))) (at x within s)"
+ show "\<forall>n. \<forall>x\<in>s. (f n has_derivative (( * ) (f' n x))) (at x within s)"
by (metis has_field_derivative_def df)
next show "(\<lambda>n. f n x) \<longlonglongrightarrow> l"
by (rule tf)
@@ -906,9 +906,9 @@
then obtain g where g: "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>n. f n x) sums g x"
"\<And>x. x \<in> s \<Longrightarrow> (g has_field_derivative g' x) (at x within s)" by blast
from g[OF x] show "summable (\<lambda>n. f n x)" by (auto simp: summable_def)
- from g(2)[OF x] have g': "(g has_derivative op * (g' x)) (at x)"
+ from g(2)[OF x] have g': "(g has_derivative ( * ) (g' x)) (at x)"
by (simp add: has_field_derivative_def s)
- have "((\<lambda>x. \<Sum>n. f n x) has_derivative op * (g' x)) (at x)"
+ have "((\<lambda>x. \<Sum>n. f n x) has_derivative ( * ) (g' x)) (at x)"
by (rule has_derivative_transform_within_open[OF g' \<open>open s\<close> x])
(insert g, auto simp: sums_iff)
thus "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)" unfolding differentiable_def
--- a/src/HOL/Analysis/Conformal_Mappings.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Conformal_Mappings.thy Wed Jan 10 15:25:09 2018 +0100
@@ -1141,10 +1141,10 @@
done
with \<open>e>0\<close> show ?thesis by force
qed
- have "inj (op * (deriv f \<xi>))"
+ have "inj (( * ) (deriv f \<xi>))"
using dnz by simp
- then obtain g' where g': "linear g'" "g' \<circ> op * (deriv f \<xi>) = id"
- using linear_injective_left_inverse [of "op * (deriv f \<xi>)"]
+ then obtain g' where g': "linear g'" "g' \<circ> ( * ) (deriv f \<xi>) = id"
+ using linear_injective_left_inverse [of "( * ) (deriv f \<xi>)"]
by (auto simp: linear_times)
show ?thesis
apply (rule has_derivative_locally_injective [OF S, where f=f and f' = "\<lambda>z h. deriv f z * h" and g' = g'])
@@ -2093,10 +2093,10 @@
apply (simp add: C_def False fo)
apply (simp add: derivative_intros dfa complex_derivative_chain)
done
- have sb1: "op * (C * r) ` (\<lambda>z. f (a + of_real r * z) / (C * r)) ` ball 0 1
+ have sb1: "( * ) (C * r) ` (\<lambda>z. f (a + of_real r * z) / (C * r)) ` ball 0 1
\<subseteq> f ` ball a r"
using \<open>0 < r\<close> by (auto simp: dist_norm norm_mult C_def False)
- have sb2: "ball (C * r * b) r' \<subseteq> op * (C * r) ` ball b t"
+ have sb2: "ball (C * r * b) r' \<subseteq> ( * ) (C * r) ` ball b t"
if "1 / 12 < t" for b t
proof -
have *: "r * cmod (deriv f a) / 12 \<le> r * (t * cmod (deriv f a))"
@@ -2602,7 +2602,7 @@
by (metis DiffD2 Ints_cases insertI1 subset_eq valid_path_imp_path)
define p_circ where "p_circ \<equiv> circlepath p (h p)"
define p_circ_pt where "p_circ_pt \<equiv> linepath (p+h p) (p+h p)"
- define n_circ where "n_circ \<equiv> \<lambda>n. (op +++ p_circ ^^ n) p_circ_pt"
+ define n_circ where "n_circ \<equiv> \<lambda>n. ((+++) p_circ ^^ n) p_circ_pt"
define cp where "cp \<equiv> if n\<ge>0 then reversepath (n_circ (nat n)) else n_circ (nat (- n))"
have n_circ:"valid_path (n_circ k)"
"winding_number (n_circ k) p = k"
@@ -3861,7 +3861,7 @@
then show "h field_differentiable at (\<gamma> x)"
unfolding t_def field_differentiable_def by blast
qed
- then have " (op / 1 has_contour_integral 0) (h \<circ> \<gamma>)
+ then have " ((/) 1 has_contour_integral 0) (h \<circ> \<gamma>)
= ((\<lambda>x. deriv h x / h x) has_contour_integral 0) \<gamma>"
unfolding has_contour_integral
apply (intro has_integral_spike_eq[OF negligible_finite, OF \<open>finite spikes\<close>])
--- a/src/HOL/Analysis/Connected.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Connected.thy Wed Jan 10 15:25:09 2018 +0100
@@ -2165,14 +2165,14 @@
unfolding dist_norm
using norm_scaleR[of c "(1 / c) *\<^sub>R y - x", unfolded scaleR_right_diff_distrib, unfolded scaleR_scaleR] assms(1)
assms(1)[unfolded zero_less_abs_iff[symmetric]] by (simp del:zero_less_abs_iff)
- then have "y \<in> op *\<^sub>R c ` s"
- using rev_image_eqI[of "(1 / c) *\<^sub>R y" s y "op *\<^sub>R c"]
+ then have "y \<in> ( *\<^sub>R) c ` s"
+ using rev_image_eqI[of "(1 / c) *\<^sub>R y" s y "( *\<^sub>R) c"]
using e[THEN spec[where x="(1 / c) *\<^sub>R y"]]
using assms(1)
unfolding dist_norm scaleR_scaleR
by auto
}
- ultimately have "\<exists>e>0. \<forall>x'. dist x' (c *\<^sub>R x) < e \<longrightarrow> x' \<in> op *\<^sub>R c ` s"
+ ultimately have "\<exists>e>0. \<forall>x'. dist x' (c *\<^sub>R x) < e \<longrightarrow> x' \<in> ( *\<^sub>R) c ` s"
apply (rule_tac x="e * \<bar>c\<bar>" in exI, auto)
done
}
@@ -2199,7 +2199,7 @@
have "continuous (at x) (\<lambda>x. x - a)"
by (intro continuous_diff continuous_ident continuous_const)
}
- moreover have "{x. x - a \<in> S} = op + a ` S"
+ moreover have "{x. x - a \<in> S} = (+) a ` S"
by force
ultimately show ?thesis
by (metis assms continuous_open_vimage vimage_def)
@@ -2212,10 +2212,10 @@
proof -
have *: "(\<lambda>x. a + c *\<^sub>R x) = (\<lambda>x. a + x) \<circ> (\<lambda>x. c *\<^sub>R x)"
unfolding o_def ..
- have "op + a ` op *\<^sub>R c ` S = (op + a \<circ> op *\<^sub>R c) ` S"
+ have "(+) a ` ( *\<^sub>R) c ` S = ((+) a \<circ> ( *\<^sub>R) c) ` S"
by auto
then show ?thesis
- using assms open_translation[of "op *\<^sub>R c ` S" a]
+ using assms open_translation[of "( *\<^sub>R) c ` S" a]
unfolding *
by auto
qed
@@ -2225,13 +2225,13 @@
shows "interior ((\<lambda>x. a + x) ` S) = (\<lambda>x. a + x) ` (interior S)"
proof (rule set_eqI, rule)
fix x
- assume "x \<in> interior (op + a ` S)"
- then obtain e where "e > 0" and e: "ball x e \<subseteq> op + a ` S"
+ assume "x \<in> interior ((+) a ` S)"
+ then obtain e where "e > 0" and e: "ball x e \<subseteq> (+) a ` S"
unfolding mem_interior by auto
then have "ball (x - a) e \<subseteq> S"
unfolding subset_eq Ball_def mem_ball dist_norm
by (auto simp: diff_diff_eq)
- then show "x \<in> op + a ` interior S"
+ then show "x \<in> (+) a ` interior S"
unfolding image_iff
apply (rule_tac x="x - a" in bexI)
unfolding mem_interior
@@ -2240,7 +2240,7 @@
done
next
fix x
- assume "x \<in> op + a ` interior S"
+ assume "x \<in> (+) a ` interior S"
then obtain y e where "e > 0" and e: "ball y e \<subseteq> S" and y: "x = a + y"
unfolding image_iff Bex_def mem_interior by auto
{
@@ -2251,12 +2251,12 @@
using e[unfolded subset_eq, THEN bspec[where x="z - a"]]
unfolding mem_ball dist_norm y group_add_class.diff_diff_eq2 *
by auto
- then have "z \<in> op + a ` S"
+ then have "z \<in> (+) a ` S"
unfolding image_iff by (auto intro!: bexI[where x="z - a"])
}
- then have "ball x e \<subseteq> op + a ` S"
+ then have "ball x e \<subseteq> (+) a ` S"
unfolding subset_eq by auto
- then show "x \<in> interior (op + a ` S)"
+ then show "x \<in> interior ((+) a ` S)"
unfolding mem_interior using \<open>e > 0\<close> by auto
qed
@@ -2574,7 +2574,7 @@
assumes "compact s"
shows "compact ((\<lambda>x. a + c *\<^sub>R x) ` s)"
proof -
- have "op + a ` op *\<^sub>R c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s"
+ have "(+) a ` ( *\<^sub>R) c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s"
by auto
then show ?thesis
using compact_translation[OF compact_scaling[OF assms], of a c] by auto
@@ -3007,7 +3007,7 @@
assumes "closed S"
shows "closed ((\<lambda>x. a + x) ` S)"
proof -
- have "(\<Union>x\<in> {a}. \<Union>y \<in> S. {x + y}) = (op + a ` S)" by auto
+ have "(\<Union>x\<in> {a}. \<Union>y \<in> S. {x + y}) = ((+) a ` S)" by auto
then show ?thesis
using compact_closed_sums[OF compact_sing[of a] assms] by auto
qed
@@ -3038,7 +3038,7 @@
fixes a :: "'a::real_normed_vector"
shows "closure ((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (closure s)"
proof -
- have *: "op + a ` (- s) = - op + a ` s"
+ have *: "(+) a ` (- s) = - (+) a ` s"
apply auto
unfolding image_iff
apply (rule_tac x="x - a" in bexI, auto)
@@ -3058,7 +3058,7 @@
lemma sphere_translation:
fixes a :: "'n::euclidean_space"
- shows "sphere (a+c) r = op+ a ` sphere c r"
+ shows "sphere (a+c) r = (+) a ` sphere c r"
apply safe
apply (rule_tac x="x-a" in image_eqI)
apply (auto simp: dist_norm algebra_simps)
@@ -3066,7 +3066,7 @@
lemma cball_translation:
fixes a :: "'n::euclidean_space"
- shows "cball (a+c) r = op+ a ` cball c r"
+ shows "cball (a+c) r = (+) a ` cball c r"
apply safe
apply (rule_tac x="x-a" in image_eqI)
apply (auto simp: dist_norm algebra_simps)
@@ -3074,7 +3074,7 @@
lemma ball_translation:
fixes a :: "'n::euclidean_space"
- shows "ball (a+c) r = op+ a ` ball c r"
+ shows "ball (a+c) r = (+) a ` ball c r"
apply safe
apply (rule_tac x="x-a" in image_eqI)
apply (auto simp: dist_norm algebra_simps)
@@ -3420,7 +3420,7 @@
lemma homeomorphism_translation:
fixes a :: "'a :: real_normed_vector"
- shows "homeomorphism (op + a ` S) S (op + (- a)) (op + a)"
+ shows "homeomorphism ((+) a ` S) S ((+) (- a)) ((+) a)"
unfolding homeomorphism_def by (auto simp: algebra_simps continuous_intros)
lemma homeomorphism_ident: "homeomorphism T T (\<lambda>a. a) (\<lambda>a. a)"
@@ -3639,7 +3639,7 @@
assumes "c \<noteq> 0"
shows "s homeomorphic ((\<lambda>x. a + c *\<^sub>R x) ` s)"
proof -
- have *: "op + a ` op *\<^sub>R c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s" by auto
+ have *: "(+) a ` ( *\<^sub>R) c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s" by auto
show ?thesis
using homeomorphic_trans
using homeomorphic_scaling[OF assms, of s]
@@ -4540,9 +4540,9 @@
proof
show "countable ((\<lambda>C. S \<inter> C) ` \<C>)"
by (simp add: \<open>countable \<C>\<close>)
- show "\<And>C. C \<in> op \<inter> S ` \<C> \<Longrightarrow> openin (subtopology euclidean S) C"
+ show "\<And>C. C \<in> (\<inter>) S ` \<C> \<Longrightarrow> openin (subtopology euclidean S) C"
using ope by auto
- show "\<And>T. openin (subtopology euclidean S) T \<Longrightarrow> \<exists>\<U>\<subseteq>op \<inter> S ` \<C>. T = \<Union>\<U>"
+ show "\<And>T. openin (subtopology euclidean S) T \<Longrightarrow> \<exists>\<U>\<subseteq>(\<inter>) S ` \<C>. T = \<Union>\<U>"
by (metis \<C> image_mono inf_Sup openin_open)
qed
qed
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Wed Jan 10 15:25:09 2018 +0100
@@ -124,7 +124,7 @@
by (rule ccontr) auto
lemma subset_translation_eq [simp]:
- fixes a :: "'a::real_vector" shows "op + a ` s \<subseteq> op + a ` t \<longleftrightarrow> s \<subseteq> t"
+ fixes a :: "'a::real_vector" shows "(+) a ` s \<subseteq> (+) a ` t \<longleftrightarrow> s \<subseteq> t"
by auto
lemma translate_inj_on:
@@ -714,7 +714,7 @@
assumes "convex S"
shows "convex ((\<lambda>x. a + c *\<^sub>R x) ` S)"
proof -
- have "(\<lambda>x. a + c *\<^sub>R x) ` S = op + a ` op *\<^sub>R c ` S"
+ have "(\<lambda>x. a + c *\<^sub>R x) ` S = (+) a ` ( *\<^sub>R) c ` S"
by auto
then show ?thesis
using convex_translation[OF convex_scaling[OF assms], of a c] by auto
@@ -1330,12 +1330,12 @@
lemma closure_scaleR:
fixes S :: "'a::real_normed_vector set"
- shows "(op *\<^sub>R c) ` (closure S) = closure ((op *\<^sub>R c) ` S)"
+ shows "(( *\<^sub>R) c) ` (closure S) = closure ((( *\<^sub>R) c) ` S)"
proof
- show "(op *\<^sub>R c) ` (closure S) \<subseteq> closure ((op *\<^sub>R c) ` S)"
+ show "(( *\<^sub>R) c) ` (closure S) \<subseteq> closure ((( *\<^sub>R) c) ` S)"
using bounded_linear_scaleR_right
by (rule closure_bounded_linear_image_subset)
- show "closure ((op *\<^sub>R c) ` S) \<subseteq> (op *\<^sub>R c) ` (closure S)"
+ show "closure ((( *\<^sub>R) c) ` S) \<subseteq> (( *\<^sub>R) c) ` (closure S)"
by (intro closure_minimal image_mono closure_subset closed_scaling closed_closure)
qed
@@ -2154,7 +2154,7 @@
lemma cone_iff:
assumes "S \<noteq> {}"
- shows "cone S \<longleftrightarrow> 0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (op *\<^sub>R c) ` S = S)"
+ shows "cone S \<longleftrightarrow> 0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (( *\<^sub>R) c) ` S = S)"
proof -
{
assume "cone S"
@@ -2164,7 +2164,7 @@
{
fix x
assume "x \<in> S"
- then have "x \<in> (op *\<^sub>R c) ` S"
+ then have "x \<in> (( *\<^sub>R) c) ` S"
unfolding image_def
using \<open>cone S\<close> \<open>c>0\<close> mem_cone[of S x "1/c"]
exI[of "(\<lambda>t. t \<in> S \<and> x = c *\<^sub>R t)" "(1 / c) *\<^sub>R x"]
@@ -2173,19 +2173,19 @@
moreover
{
fix x
- assume "x \<in> (op *\<^sub>R c) ` S"
+ assume "x \<in> (( *\<^sub>R) c) ` S"
then have "x \<in> S"
using \<open>cone S\<close> \<open>c > 0\<close>
unfolding cone_def image_def \<open>c > 0\<close> by auto
}
- ultimately have "(op *\<^sub>R c) ` S = S" by auto
+ ultimately have "(( *\<^sub>R) c) ` S = S" by auto
}
- then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (op *\<^sub>R c) ` S = S)"
+ then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (( *\<^sub>R) c) ` S = S)"
using \<open>cone S\<close> cone_contains_0[of S] assms by auto
}
moreover
{
- assume a: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (op *\<^sub>R c) ` S = S)"
+ assume a: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> (( *\<^sub>R) c) ` S = S)"
{
fix x
assume "x \<in> S"
@@ -2271,9 +2271,9 @@
then show ?thesis by auto
next
case False
- then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> op *\<^sub>R c ` S = S)"
+ then have "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ( *\<^sub>R) c ` S = S)"
using cone_iff[of S] assms by auto
- then have "0 \<in> closure S \<and> (\<forall>c. c > 0 \<longrightarrow> op *\<^sub>R c ` closure S = closure S)"
+ then have "0 \<in> closure S \<and> (\<forall>c. c > 0 \<longrightarrow> ( *\<^sub>R) c ` closure S = closure S)"
using closure_subset by (auto simp add: closure_scaleR)
then show ?thesis
using False cone_iff[of "closure S"] by auto
@@ -3344,7 +3344,7 @@
proof -
obtain x where x: "x \<in> S \<and> x \<in> affine hull (S - {x})"
using assms affine_dependent_def by auto
- have "op + a ` (S - {x}) = op + a ` S - {a + x}"
+ have "(+) a ` (S - {x}) = (+) a ` S - {a + x}"
by auto
then have "a + x \<in> affine hull ((\<lambda>x. a + x) ` S - {a + x})"
using affine_hull_translation[of a "S - {x}"] x by auto
@@ -3409,7 +3409,7 @@
assumes "a \<notin> S"
shows "affine_dependent (insert a S) \<longleftrightarrow> dependent ((\<lambda>x. -a + x) ` S)"
proof -
- have "(op + (- a) ` S) = {x - a| x . x : S}" by auto
+ have "((+) (- a) ` S) = {x - a| x . x : S}" by auto
then show ?thesis
using affine_dependent_translation_eq[of "(insert a S)" "-a"]
affine_dependent_imp_dependent2 assms
@@ -3448,7 +3448,7 @@
then have "insert 0 ((\<lambda>x. -a+x) ` (s - {a})) = (\<lambda>x. -a+x) ` s"
by auto
then have "span ((\<lambda>x. -a+x) ` (s - {a}))=span ((\<lambda>x. -a+x) ` s)"
- using span_insert_0[of "op + (- a) ` (s - {a})"] by (auto simp del: uminus_add_conv_diff)
+ using span_insert_0[of "(+) (- a) ` (s - {a})"] by (auto simp del: uminus_add_conv_diff)
moreover have "{x - a |x. x \<in> (s - {a})} = ((\<lambda>x. -a+x) ` (s - {a}))"
by auto
moreover have "insert a (s - {a}) = insert a s"
@@ -4024,14 +4024,14 @@
case False
then obtain c S' where "c \<notin> S'" "S = insert c S'"
by (meson equals0I mk_disjoint_insert)
- have "dim (op + (-c) ` S) < DIM('a)"
+ have "dim ((+) (-c) ` S) < DIM('a)"
by (metis \<open>S = insert c S'\<close> aff_dim_eq_dim assms hull_inc insertI1 of_nat_less_imp_less)
- then obtain a where "a \<noteq> 0" "span (op + (-c) ` S) \<subseteq> {x. a \<bullet> x = 0}"
+ then obtain a where "a \<noteq> 0" "span ((+) (-c) ` S) \<subseteq> {x. a \<bullet> x = 0}"
using lowdim_subset_hyperplane by blast
moreover
- have "a \<bullet> w = a \<bullet> c" if "span (op + (- c) ` S) \<subseteq> {x. a \<bullet> x = 0}" "w \<in> S" for w
+ have "a \<bullet> w = a \<bullet> c" if "span ((+) (- c) ` S) \<subseteq> {x. a \<bullet> x = 0}" "w \<in> S" for w
proof -
- have "w-c \<in> span (op + (- c) ` S)"
+ have "w-c \<in> span ((+) (- c) ` S)"
by (simp add: span_superset \<open>w \<in> S\<close>)
with that have "w-c \<in> {x. a \<bullet> x = 0}"
by blast
@@ -4235,7 +4235,7 @@
unfolding cball_def dist_norm by auto
then have "aff_dim (cball (0 :: 'n::euclidean_space) e) \<le> aff_dim (cball a e)"
using aff_dim_translation_eq[of a "cball 0 e"]
- aff_dim_subset[of "op + a ` cball 0 e" "cball a e"]
+ aff_dim_subset[of "(+) a ` cball 0 e" "cball a e"]
by auto
moreover have "aff_dim (cball (0 :: 'n::euclidean_space) e) = int (DIM('n))"
using hull_inc[of "(0 :: 'n::euclidean_space)" "cball 0 e"]
@@ -4805,7 +4805,7 @@
assume "S \<noteq> {}"
then obtain L where L: "subspace L" "affine_parallel S L"
using assms affine_parallel_subspace[of S] by auto
- then obtain a where a: "S = (op + a ` L)"
+ then obtain a where a: "S = ((+) a ` L)"
using affine_parallel_def[of L S] affine_parallel_commut by auto
from L have "closed L" using closed_subspace by auto
then have "closed S"
@@ -5000,7 +5000,7 @@
translation_assoc[of "-a" "a"]
by auto
then have "((\<lambda>x. a + x) ` rel_interior S) \<supseteq> rel_interior ((\<lambda>x. a + x) ` S)"
- using translation_inverse_subset[of a "rel_interior (op + a ` S)" "rel_interior S"]
+ using translation_inverse_subset[of a "rel_interior ((+) a ` S)" "rel_interior S"]
by auto
then show ?thesis
using rel_interior_translation_aux[of a S] by auto
@@ -5141,7 +5141,7 @@
shows "affine hull (insert 0 d) = {x::'a::euclidean_space. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0}"
(is "affine hull (insert 0 ?A) = ?B")
proof -
- have *: "\<And>A. op + (0::'a) ` A = A" "\<And>A. op + (- (0::'a)) ` A = A"
+ have *: "\<And>A. (+) (0::'a) ` A = A" "\<And>A. (+) (- (0::'a)) ` A = A"
by auto
show ?thesis
unfolding affine_hull_insert_span_gen span_substd_basis[OF assms,symmetric] * ..
@@ -5982,7 +5982,7 @@
unfolding k_def
proof (subst less_cSUP_iff)
show "T \<noteq> {}" by fact
- show "bdd_above (op \<bullet> a ` T)"
+ show "bdd_above ((\<bullet>) a ` T)"
using ab[rule_format, of y] \<open>y \<in> S\<close>
by (intro bdd_aboveI2[where M="inner a y - b"]) (auto simp: field_simps intro: less_imp_le)
qed (auto intro!: bexI[of _ x] \<open>0<b\<close>)
@@ -6073,7 +6073,7 @@
using assms(3-5) by fastforce
then have *: "\<And>x y. x \<in> t \<Longrightarrow> y \<in> s \<Longrightarrow> inner a y \<le> inner a x"
by (force simp add: inner_diff)
- then have bdd: "bdd_above ((op \<bullet> a)`s)"
+ then have bdd: "bdd_above (((\<bullet>) a)`s)"
using \<open>t \<noteq> {}\<close> by (auto intro: bdd_aboveI2[OF *])
show ?thesis
using \<open>a\<noteq>0\<close>
@@ -6209,19 +6209,19 @@
then show ?thesis by auto
next
case False
- then have *: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> op *\<^sub>R c ` S = S)"
+ then have *: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ( *\<^sub>R) c ` S = S)"
using cone_iff[of S] assms by auto
{
fix c :: real
assume "c > 0"
- then have "op *\<^sub>R c ` (convex hull S) = convex hull (op *\<^sub>R c ` S)"
+ then have "( *\<^sub>R) c ` (convex hull S) = convex hull (( *\<^sub>R) c ` S)"
using convex_hull_scaling[of _ S] by auto
also have "\<dots> = convex hull S"
using * \<open>c > 0\<close> by auto
- finally have "op *\<^sub>R c ` (convex hull S) = convex hull S"
+ finally have "( *\<^sub>R) c ` (convex hull S) = convex hull S"
by auto
}
- then have "0 \<in> convex hull S" "\<And>c. c > 0 \<Longrightarrow> (op *\<^sub>R c ` (convex hull S)) = (convex hull S)"
+ then have "0 \<in> convex hull S" "\<And>c. c > 0 \<Longrightarrow> (( *\<^sub>R) c ` (convex hull S)) = (convex hull S)"
using * hull_subset[of S convex] by auto
then show ?thesis
using \<open>S \<noteq> {}\<close> cone_iff[of "convex hull S"] by auto
@@ -7030,7 +7030,7 @@
fixes a :: "'a::euclidean_space"
assumes "cbox a b \<noteq> {}"
shows "cbox a b =
- op + a ` (\<lambda>x. \<Sum>k\<in>Basis. ((b \<bullet> k - a \<bullet> k) * (x \<bullet> k)) *\<^sub>R k) ` cbox 0 One"
+ (+) a ` (\<lambda>x. \<Sum>k\<in>Basis. ((b \<bullet> k - a \<bullet> k) * (x \<bullet> k)) *\<^sub>R k) ` cbox 0 One"
using assms
apply (simp add: box_ne_empty image_stretch_interval cbox_translation [symmetric])
apply (simp add: min_def max_def algebra_simps sum_subtractf euclidean_representation)
@@ -7048,7 +7048,7 @@
by (blast intro: unit_cube_convex_hull)
have lin: "linear (\<lambda>x. \<Sum>k\<in>Basis. ((b \<bullet> k - a \<bullet> k) * (x \<bullet> k)) *\<^sub>R k)"
by (rule linear_compose_sum) (auto simp: algebra_simps linearI)
- have "finite (op + a ` (\<lambda>x. \<Sum>k\<in>Basis. ((b \<bullet> k - a \<bullet> k) * (x \<bullet> k)) *\<^sub>R k) ` s)"
+ have "finite ((+) a ` (\<lambda>x. \<Sum>k\<in>Basis. ((b \<bullet> k - a \<bullet> k) * (x \<bullet> k)) *\<^sub>R k) ` s)"
by (rule finite_imageI \<open>finite s\<close>)+
then show ?thesis
apply (rule that)
--- a/src/HOL/Analysis/Derivative.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Derivative.thy Wed Jan 10 15:25:09 2018 +0100
@@ -91,7 +91,7 @@
lemma has_derivative_right:
fixes f :: "real \<Rightarrow> real"
and y :: "real"
- shows "(f has_derivative (op * y)) (at x within ({x <..} \<inter> I)) \<longleftrightarrow>
+ shows "(f has_derivative (( * ) y)) (at x within ({x <..} \<inter> I)) \<longleftrightarrow>
((\<lambda>t. (f x - f t) / (x - t)) \<longlongrightarrow> y) (at x within ({x <..} \<inter> I))"
proof -
have "((\<lambda>t. (f t - (f x + y * (t - x))) / \<bar>t - x\<bar>) \<longlongrightarrow> 0) (at x within ({x<..} \<inter> I)) \<longleftrightarrow>
@@ -245,7 +245,7 @@
lemma has_derivative_sqnorm_at [derivative_intros, simp]:
"((\<lambda>x. (norm x)\<^sup>2) has_derivative (\<lambda>x. 2 *\<^sub>R (a \<bullet> x))) (at a)"
-using has_derivative_bilinear_at [of id id a id id "op \<bullet>"]
+using has_derivative_bilinear_at [of id id a id id "(\<bullet>)"]
by (auto simp: inner_commute dot_square_norm bounded_bilinear_inner)
lemma differentiable_sqnorm_at [derivative_intros, simp]:
@@ -1112,7 +1112,7 @@
shows "norm (f (x0 + a) - f x0) \<le> norm a * B"
proof -
let ?G = "(\<lambda>x. x0 + x *\<^sub>R a) ` {0..1}"
- have "?G = op + x0 ` (\<lambda>x. x *\<^sub>R a) ` {0..1}" by auto
+ have "?G = (+) x0 ` (\<lambda>x. x *\<^sub>R a) ` {0..1}" by auto
also have "convex \<dots>"
by (intro convex_translation convex_scaled convex_real_interval)
finally have "convex ?G" .
@@ -1164,7 +1164,7 @@
assumes "convex s" "\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative 0) (at x within s)"
shows "\<exists>c. \<forall>x\<in>s. f (x) = (c :: 'a :: real_normed_field)"
proof (rule has_derivative_zero_constant)
- have A: "op * 0 = (\<lambda>_. 0 :: 'a)" by (intro ext) simp
+ have A: "( * ) 0 = (\<lambda>_. 0 :: 'a)" by (intro ext) simp
fix x assume "x \<in> s" thus "(f has_derivative (\<lambda>h. 0)) (at x within s)"
using assms(2)[of x] by (simp add: has_field_derivative_def A)
qed fact
@@ -2292,9 +2292,9 @@
then obtain g where g: "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>n. f n x) sums g x"
"\<And>x. x \<in> s \<Longrightarrow> (g has_field_derivative g' x) (at x within s)" by blast
from g[OF x] show "summable (\<lambda>n. f n x)" by (auto simp: summable_def)
- from g(2)[OF x] have g': "(g has_derivative op * (g' x)) (at x)"
+ from g(2)[OF x] have g': "(g has_derivative ( * ) (g' x)) (at x)"
by (simp add: has_field_derivative_def s)
- have "((\<lambda>x. \<Sum>n. f n x) has_derivative op * (g' x)) (at x)"
+ have "((\<lambda>x. \<Sum>n. f n x) has_derivative ( * ) (g' x)) (at x)"
by (rule has_derivative_transform_within_open[OF g' \<open>open s\<close> x])
(insert g, auto simp: sums_iff)
thus "(\<lambda>x. \<Sum>n. f n x) differentiable (at x)" unfolding differentiable_def
@@ -2645,7 +2645,7 @@
unfolding field_differentiable_def
by (metis DERIV_subset top_greatest)
-lemma field_differentiable_linear [simp,derivative_intros]: "(op * c) field_differentiable F"
+lemma field_differentiable_linear [simp,derivative_intros]: "(( * ) c) field_differentiable F"
proof -
show ?thesis
unfolding field_differentiable_def has_field_derivative_def mult_commute_abs
@@ -2675,7 +2675,7 @@
by (metis field_differentiable_add)
lemma field_differentiable_add_const [simp,derivative_intros]:
- "op + c field_differentiable F"
+ "(+) c field_differentiable F"
by (simp add: field_differentiable_add)
lemma field_differentiable_sum [derivative_intros]:
--- a/src/HOL/Analysis/Determinants.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Determinants.thy Wed Jan 10 15:25:09 2018 +0100
@@ -819,7 +819,7 @@
unfolding matrix_right_invertible_independent_rows
by blast
have *: "\<And>(a::real^'n) b. a + b = 0 \<Longrightarrow> -a = b"
- apply (drule_tac f="op + (- a)" in cong[OF refl])
+ apply (drule_tac f="(+) (- a)" in cong[OF refl])
apply (simp only: ab_left_minus add.assoc[symmetric])
apply simp
done
--- a/src/HOL/Analysis/Embed_Measure.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Embed_Measure.thy Wed Jan 10 15:25:09 2018 +0100
@@ -159,15 +159,15 @@
from assms(1) interpret sigma_finite_measure M .
from sigma_finite_countable obtain A where
A_props: "countable A" "A \<subseteq> sets M" "\<Union>A = space M" "\<And>X. X\<in>A \<Longrightarrow> emeasure M X \<noteq> \<infinity>" by blast
- from A_props have "countable (op ` f`A)" by auto
+ from A_props have "countable ((`) f`A)" by auto
moreover
- from inj and A_props have "op ` f`A \<subseteq> sets (embed_measure M f)"
+ from inj and A_props have "(`) f`A \<subseteq> sets (embed_measure M f)"
by (auto simp: sets_embed_measure)
moreover
- from A_props and inj have "\<Union>(op ` f`A) = space (embed_measure M f)"
+ from A_props and inj have "\<Union>((`) f`A) = space (embed_measure M f)"
by (auto simp: space_embed_measure intro!: imageI)
moreover
- from A_props and inj have "\<forall>a\<in>op ` f ` A. emeasure (embed_measure M f) a \<noteq> \<infinity>"
+ from A_props and inj have "\<forall>a\<in>(`) f ` A. emeasure (embed_measure M f) a \<noteq> \<infinity>"
by (intro ballI, subst emeasure_embed_measure)
(auto simp: inj_vimage_image_eq intro: in_sets_embed_measure)
ultimately show ?thesis by - (standard, blast)
@@ -189,7 +189,7 @@
by(rule embed_measure_count_space')(erule subset_inj_on, simp)
lemma sets_embed_measure_alt:
- "inj f \<Longrightarrow> sets (embed_measure M f) = (op` f) ` sets M"
+ "inj f \<Longrightarrow> sets (embed_measure M f) = ((`) f) ` sets M"
by (auto simp: sets_embed_measure)
lemma emeasure_embed_measure_image':
@@ -210,7 +210,7 @@
assumes "inj f"
shows "embed_measure A f = embed_measure B f \<longleftrightarrow> A = B" (is "?M = ?N \<longleftrightarrow> _")
proof
- from assms have I: "inj (op` f)" by (auto intro: injI dest: injD)
+ from assms have I: "inj ((`) f)" by (auto intro: injI dest: injD)
assume asm: "?M = ?N"
hence "sets (embed_measure A f) = sets (embed_measure B f)" by simp
with assms have "sets A = sets B" by (simp only: I inj_image_eq_iff sets_embed_measure_alt)
@@ -369,7 +369,7 @@
lemma nn_integral_monotone_convergence_SUP_countable:
fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> ennreal"
assumes nonempty: "Y \<noteq> {}"
- and chain: "Complete_Partial_Order.chain op \<le> (f ` Y)"
+ and chain: "Complete_Partial_Order.chain (\<le>) (f ` Y)"
and countable: "countable B"
shows "(\<integral>\<^sup>+ x. (SUP i:Y. f i x) \<partial>count_space B) = (SUP i:Y. (\<integral>\<^sup>+ x. f i x \<partial>count_space B))"
(is "?lhs = ?rhs")
@@ -383,7 +383,7 @@
by(simp add: nn_integral_count_space_indicator ennreal_indicator[symmetric] SUP_mult_right_ennreal nonempty)
also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. ?f i x \<partial>count_space UNIV)"
proof(rule nn_integral_monotone_convergence_SUP_nat)
- show "Complete_Partial_Order.chain op \<le> (?f ` Y)"
+ show "Complete_Partial_Order.chain (\<le>) (?f ` Y)"
by(rule chain_imageI[OF chain, unfolded image_image])(auto intro!: le_funI split: split_indicator dest: le_funD)
qed fact
also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. f i (from_nat_into B x) \<partial>count_space (to_nat_on B ` B))"
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Wed Jan 10 15:25:09 2018 +0100
@@ -1041,10 +1041,10 @@
and eq1: "\<And>c x. \<lbrakk>(a + c *\<^sub>R x) \<in> S; 0 \<le> c; a + x \<in> S\<rbrakk> \<Longrightarrow> c = 1"
shows "negligible S"
proof -
- have "negligible (op + (-a) ` S)"
+ have "negligible ((+) (-a) ` S)"
proof (subst negligible_on_intervals, intro allI)
fix u v
- show "negligible (op + (- a) ` S \<inter> cbox u v)"
+ show "negligible ((+) (- a) ` S \<inter> cbox u v)"
unfolding negligible_iff_null_sets
apply (rule starlike_negligible_compact)
apply (simp add: assms closed_translation closed_Int_compact, clarify)
@@ -1831,7 +1831,7 @@
qed
also have "\<dots> = (\<Sum>(i,l) \<in> d \<times> snd ` p. norm (integral (i\<inter>l) f))"
by (simp add: sum.cartesian_product)
- also have "\<dots> = (\<Sum>x \<in> d \<times> snd ` p. norm (integral (case_prod op \<inter> x) f))"
+ also have "\<dots> = (\<Sum>x \<in> d \<times> snd ` p. norm (integral (case_prod (\<inter>) x) f))"
by (force simp: split_def intro!: sum.cong)
also have "\<dots> = (\<Sum>k\<in>{i \<inter> l |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral k f))"
proof -
--- a/src/HOL/Analysis/Euclidean_Space.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Euclidean_Space.thy Wed Jan 10 15:25:09 2018 +0100
@@ -242,7 +242,7 @@
lemma DIM_prod[simp]: "DIM('a \<times> 'b) = DIM('a) + DIM('b)"
unfolding Basis_prod_def
- by (subst card_Un_disjoint) (auto intro!: card_image arg_cong2[where f="op +"] inj_onI)
+ by (subst card_Un_disjoint) (auto intro!: card_image arg_cong2[where f="(+)"] inj_onI)
end
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Wed Jan 10 15:25:09 2018 +0100
@@ -142,13 +142,13 @@
instantiation vec :: (plus, finite) plus
begin
- definition "op + \<equiv> (\<lambda> x y. (\<chi> i. x$i + y$i))"
+ definition "(+) \<equiv> (\<lambda> x y. (\<chi> i. x$i + y$i))"
instance ..
end
instantiation vec :: (minus, finite) minus
begin
- definition "op - \<equiv> (\<lambda> x y. (\<chi> i. x$i - y$i))"
+ definition "(-) \<equiv> (\<lambda> x y. (\<chi> i. x$i - y$i))"
instance ..
end
--- a/src/HOL/Analysis/Finite_Product_Measure.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy Wed Jan 10 15:25:09 2018 +0100
@@ -929,7 +929,7 @@
using E by (subst insert) (auto intro!: prod.cong)
also have "(\<Prod>j\<in>I. if j \<in> J - {i} then emeasure (M j) (E j) else emeasure (M j) (space (M j))) *
emeasure (M i) (if i \<in> J then E i else space (M i)) = (\<Prod>j\<in>insert i I. ?f J E j)"
- using insert by (auto simp: mult.commute intro!: arg_cong2[where f="op *"] prod.cong)
+ using insert by (auto simp: mult.commute intro!: arg_cong2[where f="( * )"] prod.cong)
also have "\<dots> = (\<Prod>j\<in>J \<union> ?I. ?f J E j)"
using insert(1,2) J E by (intro prod.mono_neutral_right) auto
finally show "?\<mu> ?p = \<dots>" .
--- a/src/HOL/Analysis/Further_Topology.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Further_Topology.thy Wed Jan 10 15:25:09 2018 +0100
@@ -527,7 +527,7 @@
and gh: "\<And>x. x \<in> rel_frontier D \<Longrightarrow> g x = h x"
by (metis *)
have "D \<inter> E \<subseteq> rel_frontier D"
- if "E \<in> \<G> \<union> {D. Bex \<F> (op face_of D) \<and> aff_dim D < int p}" for E
+ if "E \<in> \<G> \<union> {D. Bex \<F> ((face_of) D) \<and> aff_dim D < int p}" for E
proof (rule face_of_subset_rel_frontier)
show "D \<inter> E face_of D"
using that \<open>C \<in> \<F>\<close> \<open>D face_of C\<close> face
@@ -2173,21 +2173,21 @@
case False
obtain a b where "a \<in> S" "a \<in> U" "b \<in> V"
using False fim ope openin_contains_cball by fastforce
- have "openin (subtopology euclidean (op + (- b) ` V)) ((op + (- b) \<circ> f \<circ> op + a) ` op + (- a) ` S)"
+ have "openin (subtopology euclidean ((+) (- b) ` V)) (((+) (- b) \<circ> f \<circ> (+) a) ` (+) (- a) ` S)"
proof (rule invariance_of_domain_subspaces)
- show "openin (subtopology euclidean (op + (- a) ` U)) (op + (- a) ` S)"
+ show "openin (subtopology euclidean ((+) (- a) ` U)) ((+) (- a) ` S)"
by (metis ope homeomorphism_imp_open_map homeomorphism_translation translation_galois)
- show "subspace (op + (- a) ` U)"
+ show "subspace ((+) (- a) ` U)"
by (simp add: \<open>a \<in> U\<close> affine_diffs_subspace \<open>affine U\<close>)
- show "subspace (op + (- b) ` V)"
+ show "subspace ((+) (- b) ` V)"
by (simp add: \<open>b \<in> V\<close> affine_diffs_subspace \<open>affine V\<close>)
- show "dim (op + (- b) ` V) \<le> dim (op + (- a) ` U)"
+ show "dim ((+) (- b) ` V) \<le> dim ((+) (- a) ` U)"
by (metis \<open>a \<in> U\<close> \<open>b \<in> V\<close> aff_dim_eq_dim affine_hull_eq aff of_nat_le_iff)
- show "continuous_on (op + (- a) ` S) (op + (- b) \<circ> f \<circ> op + a)"
+ show "continuous_on ((+) (- a) ` S) ((+) (- b) \<circ> f \<circ> (+) a)"
by (metis contf continuous_on_compose homeomorphism_cont2 homeomorphism_translation translation_galois)
- show "(op + (- b) \<circ> f \<circ> op + a) ` op + (- a) ` S \<subseteq> op + (- b) ` V"
+ show "((+) (- b) \<circ> f \<circ> (+) a) ` (+) (- a) ` S \<subseteq> (+) (- b) ` V"
using fim by auto
- show "inj_on (op + (- b) \<circ> f \<circ> op + a) (op + (- a) ` S)"
+ show "inj_on ((+) (- b) \<circ> f \<circ> (+) a) ((+) (- a) ` S)"
by (auto simp: inj_on_def) (meson inj_onD injf)
qed
then show ?thesis
@@ -2204,19 +2204,19 @@
proof -
obtain a b where "a \<in> S" "a \<in> U" "b \<in> V"
using \<open>S \<noteq> {}\<close> fim ope openin_contains_cball by fastforce
- have "dim (op + (- a) ` U) \<le> dim (op + (- b) ` V)"
+ have "dim ((+) (- a) ` U) \<le> dim ((+) (- b) ` V)"
proof (rule invariance_of_dimension_subspaces)
- show "openin (subtopology euclidean (op + (- a) ` U)) (op + (- a) ` S)"
+ show "openin (subtopology euclidean ((+) (- a) ` U)) ((+) (- a) ` S)"
by (metis ope homeomorphism_imp_open_map homeomorphism_translation translation_galois)
- show "subspace (op + (- a) ` U)"
+ show "subspace ((+) (- a) ` U)"
by (simp add: \<open>a \<in> U\<close> affine_diffs_subspace \<open>affine U\<close>)
- show "subspace (op + (- b) ` V)"
+ show "subspace ((+) (- b) ` V)"
by (simp add: \<open>b \<in> V\<close> affine_diffs_subspace \<open>affine V\<close>)
- show "continuous_on (op + (- a) ` S) (op + (- b) \<circ> f \<circ> op + a)"
+ show "continuous_on ((+) (- a) ` S) ((+) (- b) \<circ> f \<circ> (+) a)"
by (metis contf continuous_on_compose homeomorphism_cont2 homeomorphism_translation translation_galois)
- show "(op + (- b) \<circ> f \<circ> op + a) ` op + (- a) ` S \<subseteq> op + (- b) ` V"
+ show "((+) (- b) \<circ> f \<circ> (+) a) ` (+) (- a) ` S \<subseteq> (+) (- b) ` V"
using fim by auto
- show "inj_on (op + (- b) \<circ> f \<circ> op + a) (op + (- a) ` S)"
+ show "inj_on ((+) (- b) \<circ> f \<circ> (+) a) ((+) (- a) ` S)"
by (auto simp: inj_on_def) (meson inj_onD injf)
qed (use \<open>S \<noteq> {}\<close> in auto)
then show ?thesis
@@ -2762,7 +2762,7 @@
case False
then obtain a b where "a \<in> S" "b \<in> T"
by blast
- then have "subspace (op + (- a) ` S)" "subspace (op + (- b) ` T)"
+ then have "subspace ((+) (- a) ` S)" "subspace ((+) (- b) ` T)"
using affine_diffs_subspace assms by blast+
then show ?thesis
by (metis affine_imp_convex assms homeomorphic_affine_sets homeomorphic_convex_sets)
@@ -3539,12 +3539,12 @@
by (intro conjI contg continuous_intros)
show "(complex_of_real \<circ> g) ` S \<subseteq> \<real>"
by auto
- show "continuous_on \<real> (exp \<circ> op*\<i>)"
+ show "continuous_on \<real> (exp \<circ> ( * )\<i>)"
by (intro continuous_intros)
- show "(exp \<circ> op*\<i>) ` \<real> \<subseteq> sphere 0 1"
+ show "(exp \<circ> ( * )\<i>) ` \<real> \<subseteq> sphere 0 1"
by (auto simp: complex_is_Real_iff)
qed (auto simp: convex_Reals convex_imp_contractible)
- moreover have "\<And>x. x \<in> S \<Longrightarrow> (exp \<circ> op*\<i> \<circ> (complex_of_real \<circ> g)) x = f x"
+ moreover have "\<And>x. x \<in> S \<Longrightarrow> (exp \<circ> ( * )\<i> \<circ> (complex_of_real \<circ> g)) x = f x"
by (simp add: g)
ultimately show ?lhs
apply (rule_tac x=a in exI)
--- a/src/HOL/Analysis/Gamma_Function.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Gamma_Function.thy Wed Jan 10 15:25:09 2018 +0100
@@ -2038,7 +2038,7 @@
moreover from z double_in_nonpos_Ints_imp[of z] have "2 * z \<notin> \<int>\<^sub>\<le>\<^sub>0" by auto
hence "?g \<longlonglongrightarrow> ?powr 2 (2*z) * Gamma z * Gamma (z+1/2) / Gamma (2*z)"
- using LIMSEQ_subseq_LIMSEQ[OF Gamma_series'_LIMSEQ, of "op*2" "2*z"]
+ using LIMSEQ_subseq_LIMSEQ[OF Gamma_series'_LIMSEQ, of "( * )2" "2*z"]
by (intro tendsto_intros Gamma_series'_LIMSEQ)
(simp_all add: o_def strict_mono_def Gamma_eq_zero_iff)
ultimately have "?h \<longlonglongrightarrow> ?powr 2 (2*z) * Gamma z * Gamma (z+1/2) / Gamma (2*z)"
@@ -3088,7 +3088,7 @@
proof (rule nn_integral_cong, goal_cases)
case (1 t)
have "(\<integral>\<^sup>+u. ennreal (indicator ({0..}\<times>{0..}) (t,u) * t powr (a - 1) *
- u powr (b - 1) / exp (t + u)) \<partial>distr lborel borel (op + (-t))) =
+ u powr (b - 1) / exp (t + u)) \<partial>distr lborel borel ((+) (-t))) =
(\<integral>\<^sup>+u. ennreal (indicator ({0..}\<times>{t..}) (t,u) * t powr (a - 1) *
(u - t) powr (b - 1) / exp u) \<partial>lborel)"
by (subst nn_integral_distr) (auto intro!: nn_integral_cong simp: indicator_def)
@@ -3116,10 +3116,10 @@
case True
have "(\<integral>\<^sup>+t. ennreal (indicator {0..u} t * t powr (a - 1) * (u - t) powr (b - 1)) \<partial>lborel) =
(\<integral>\<^sup>+t. ennreal (indicator {0..1} t * (u * t) powr (a - 1) * (u - u * t) powr (b - 1))
- \<partial>distr lborel borel (op * (1 / u)))" (is "_ = nn_integral _ ?f")
+ \<partial>distr lborel borel (( * ) (1 / u)))" (is "_ = nn_integral _ ?f")
using True
by (subst nn_integral_distr) (auto simp: indicator_def field_simps intro!: nn_integral_cong)
- also have "distr lborel borel (op * (1 / u)) = density lborel (\<lambda>_. u)"
+ also have "distr lborel borel (( * ) (1 / u)) = density lborel (\<lambda>_. u)"
using \<open>u > 0\<close> by (subst lborel_distr_mult) auto
also have "nn_integral \<dots> ?f = (\<integral>\<^sup>+x. ennreal (indicator {0..1} x * (u * (u * x) powr (a - 1) *
(u * (1 - x)) powr (b - 1))) \<partial>lborel)" using \<open>u > 0\<close>
--- a/src/HOL/Analysis/Great_Picard.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Great_Picard.thy Wed Jan 10 15:25:09 2018 +0100
@@ -596,7 +596,7 @@
proof (cases "k=1")
case True
then have "\<exists>x. k * x + l \<noteq> a + x" for a
- using l non [of a] ext [of f "op + a"]
+ using l non [of a] ext [of f "(+) a"]
by (metis add.commute diff_eq_eq)
with True show ?thesis by auto
next
--- a/src/HOL/Analysis/Harmonic_Numbers.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Harmonic_Numbers.thy Wed Jan 10 15:25:09 2018 +0100
@@ -225,7 +225,7 @@
by (intro summable_Leibniz(1) decseq_imp_monoseq decseq_SucI) simp_all
hence A: "(\<lambda>n. \<Sum>k<n. (-1)^k / real_of_nat (Suc k)) \<longlonglongrightarrow> (\<Sum>k. (-1)^k / real_of_nat (Suc k))"
by (simp add: summable_sums_iff divide_inverse sums_def)
- from filterlim_compose[OF this filterlim_subseq[of "op * (2::nat)"]]
+ from filterlim_compose[OF this filterlim_subseq[of "( * ) (2::nat)"]]
have "(\<lambda>n. \<Sum>k<2*n. (-1)^k / real_of_nat (Suc k)) \<longlonglongrightarrow> (\<Sum>k. (-1)^k / real_of_nat (Suc k))"
by (simp add: strict_mono_def)
ultimately have "(\<Sum>k. (- 1) ^ k / real_of_nat (Suc k)) = ln 2" by (intro LIMSEQ_unique)
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Jan 10 15:25:09 2018 +0100
@@ -1396,7 +1396,7 @@
lemma operative_integralI:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
- shows "operative (lift_option op +) (Some 0)
+ shows "operative (lift_option (+)) (Some 0)
(\<lambda>i. if f integrable_on i then Some (integral i f) else None)"
proof -
interpret comm_monoid "lift_option plus" "Some (0::'b)"
@@ -1408,7 +1408,7 @@
fix k :: 'a
assume k: "k \<in> Basis"
show "(if f integrable_on cbox a b then Some (integral (cbox a b) f) else None) =
- lift_option op + (if f integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c} then Some (integral (cbox a b \<inter> {x. x \<bullet> k \<le> c}) f) else None)
+ lift_option (+) (if f integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c} then Some (integral (cbox a b \<inter> {x. x \<bullet> k \<le> c}) f) else None)
(if f integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k} then Some (integral (cbox a b \<inter> {x. c \<le> x \<bullet> k}) f) else None)"
proof (cases "f integrable_on cbox a b")
case True
@@ -2176,11 +2176,11 @@
unfolding sum_distrib_left by (metis divide_inverse inverse_eq_divide power_one_over)
also have "\<dots> < e/2 * 2"
proof (rule mult_strict_left_mono)
- have "sum (op ^ (1/2)) {..N + 1} = sum (op ^ (1/2::real)) {..<N + 2}"
+ have "sum ((^) (1/2)) {..N + 1} = sum ((^) (1/2::real)) {..<N + 2}"
using lessThan_Suc_atMost by auto
also have "... < 2"
by (auto simp: geometric_sum)
- finally show "sum (op ^ (1/2::real)) {..N + 1} < 2" .
+ finally show "sum ((^) (1/2::real)) {..N + 1} < 2" .
qed (use \<open>0 < e\<close> in auto)
finally show ?thesis by auto
qed
@@ -2479,9 +2479,9 @@
qed
qed
-lemma comm_monoid_set_F_and: "comm_monoid_set.F op \<and> True f s \<longleftrightarrow> (finite s \<longrightarrow> (\<forall>x\<in>s. f x))"
+lemma comm_monoid_set_F_and: "comm_monoid_set.F (\<and>) True f s \<longleftrightarrow> (finite s \<longrightarrow> (\<forall>x\<in>s. f x))"
proof -
- interpret bool: comm_monoid_set "op \<and>" True
+ interpret bool: comm_monoid_set "(\<and>)" True
proof qed auto
show ?thesis
by (induction s rule: infinite_finite_induct) auto
@@ -2587,8 +2587,8 @@
fix e :: real
assume e: "e > 0"
{
- assume "\<forall>e>0. ?P e op <"
- then show "?P (e * content (cbox a b)) op \<le>"
+ assume "\<forall>e>0. ?P e (<)"
+ then show "?P (e * content (cbox a b)) (\<le>)"
apply (erule_tac x="e * content (cbox a b)" in allE)
apply (erule impE)
defer
@@ -2598,8 +2598,8 @@
done
}
{
- assume "\<forall>e>0. ?P (e * content (cbox a b)) op \<le>"
- then show "?P e op <"
+ assume "\<forall>e>0. ?P (e * content (cbox a b)) (\<le>)"
+ then show "?P e (<)"
apply (erule_tac x="e/2 / content (cbox a b)" in allE)
apply (erule impE)
defer
@@ -2983,7 +2983,7 @@
"\<lambda>i. if f integrable_on i then Some (integral i f) else None"
using operative_integralI by (rule operative_realI)
from \<open>a \<le> c\<close> \<open>c \<le> b\<close> ac cb coalesce_less_eq
- have *: "lift_option op +
+ have *: "lift_option (+)
(if f integrable_on {a..c} then Some (integral {a..c} f) else None)
(if f integrable_on {c..b} then Some (integral {c..b} f) else None) =
(if f integrable_on {a..b} then Some (integral {a..b} f) else None)"
@@ -4609,9 +4609,9 @@
lemma negligible_translation:
assumes "negligible S"
- shows "negligible (op + c ` S)"
+ shows "negligible ((+) c ` S)"
proof -
- have inj: "inj (op + c)"
+ have inj: "inj ((+) c)"
by simp
show ?thesis
using assms
@@ -4620,9 +4620,9 @@
assume "\<forall>x y. (indicator S has_integral 0) (cbox x y)"
then have *: "(indicator S has_integral 0) (cbox (a-c) (b-c))"
by (meson Diff_iff assms has_integral_negligible indicator_simps(2))
- have eq: "indicator (op + c ` S) = (\<lambda>x. indicator S (x - c))"
+ have eq: "indicator ((+) c ` S) = (\<lambda>x. indicator S (x - c))"
by (force simp add: indicator_def)
- show "(indicator (op + c ` S) has_integral 0) (cbox a b)"
+ show "(indicator ((+) c ` S) has_integral 0) (cbox a b)"
using has_integral_affinity [OF *, of 1 "-c"]
cbox_translation [of "c" "-c+a" "-c+b"]
by (simp add: eq add.commute)
@@ -4630,7 +4630,7 @@
qed
lemma negligible_translation_rev:
- assumes "negligible (op + c ` S)"
+ assumes "negligible ((+) c ` S)"
shows "negligible S"
by (metis negligible_translation [OF assms, of "-c"] translation_galois)
@@ -4838,8 +4838,8 @@
using real_arch_simple by blast
have "ball 0 B \<subseteq> ?cube n" if n: "n \<ge> N" for n
proof -
- have "sum (op *\<^sub>R (- real n)) Basis \<bullet> i \<le> x \<bullet> i \<and>
- x \<bullet> i \<le> sum (op *\<^sub>R (real n)) Basis \<bullet> i"
+ have "sum (( *\<^sub>R) (- real n)) Basis \<bullet> i \<le> x \<bullet> i \<and>
+ x \<bullet> i \<le> sum (( *\<^sub>R) (real n)) Basis \<bullet> i"
if "norm x < B" "i \<in> Basis" for x i::'n
using Basis_le_norm[of i x] n N that by (auto simp add: field_simps sum_negf)
then show ?thesis
@@ -4874,7 +4874,7 @@
fix x :: 'n
assume x: "x \<in> ball 0 B"
have "\<lbrakk>norm (0 - x) < B; i \<in> Basis\<rbrakk>
- \<Longrightarrow> sum (op *\<^sub>R (-n)) Basis \<bullet> i\<le> x \<bullet> i \<and> x \<bullet> i \<le> sum (op *\<^sub>R n) Basis \<bullet> i" for i
+ \<Longrightarrow> sum (( *\<^sub>R) (-n)) Basis \<bullet> i\<le> x \<bullet> i \<and> x \<bullet> i \<le> sum (( *\<^sub>R) n) Basis \<bullet> i" for i
using Basis_le_norm[of i x] n by (auto simp add: field_simps sum_negf)
then show "x \<in> ?cube n"
using x by (auto simp: mem_box dist_norm)
@@ -5925,7 +5925,7 @@
and bou: "bounded (range(\<lambda>k. integral S (f k)))"
shows "g integrable_on S \<and> (\<lambda>k. integral S (f k)) \<longlonglongrightarrow> integral S g"
proof -
- have *: "range(\<lambda>k. integral S (\<lambda>x. - f k x)) = op *\<^sub>R (- 1) ` (range(\<lambda>k. integral S (f k)))"
+ have *: "range(\<lambda>k. integral S (\<lambda>x. - f k x)) = ( *\<^sub>R) (- 1) ` (range(\<lambda>k. integral S (f k)))"
by force
have "(\<lambda>x. - g x) integrable_on S \<and> (\<lambda>k. integral S (\<lambda>x. - f k x)) \<longlonglongrightarrow> integral S (\<lambda>x. - g x)"
proof (rule monotone_convergence_increasing)
--- a/src/HOL/Analysis/Homeomorphism.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Homeomorphism.thy Wed Jan 10 15:25:09 2018 +0100
@@ -549,31 +549,31 @@
and starlike_compact_projective2:
"S homeomorphic cball a 1 \<inter> affine hull S"
proof -
- have 1: "compact (op+ (-a) ` S)" by (meson assms compact_translation)
- have 2: "0 \<in> rel_interior (op+ (-a) ` S)"
+ have 1: "compact ((+) (-a) ` S)" by (meson assms compact_translation)
+ have 2: "0 \<in> rel_interior ((+) (-a) ` S)"
by (simp add: a rel_interior_translation)
- have 3: "open_segment 0 x \<subseteq> rel_interior (op+ (-a) ` S)" if "x \<in> (op+ (-a) ` S)" for x
+ have 3: "open_segment 0 x \<subseteq> rel_interior ((+) (-a) ` S)" if "x \<in> ((+) (-a) ` S)" for x
proof -
have "x+a \<in> S" using that by auto
then have "open_segment a (x+a) \<subseteq> rel_interior S" by (metis star)
then show ?thesis using open_segment_translation
using rel_interior_translation by fastforce
qed
- have "S - rel_interior S homeomorphic (op+ (-a) ` S) - rel_interior (op+ (-a) ` S)"
+ have "S - rel_interior S homeomorphic ((+) (-a) ` S) - rel_interior ((+) (-a) ` S)"
by (metis rel_interior_translation translation_diff homeomorphic_translation)
- also have "... homeomorphic sphere 0 1 \<inter> affine hull (op+ (-a) ` S)"
+ also have "... homeomorphic sphere 0 1 \<inter> affine hull ((+) (-a) ` S)"
by (rule starlike_compact_projective1_0 [OF 1 2 3])
- also have "... = op+ (-a) ` (sphere a 1 \<inter> affine hull S)"
+ also have "... = (+) (-a) ` (sphere a 1 \<inter> affine hull S)"
by (metis affine_hull_translation left_minus sphere_translation translation_Int)
also have "... homeomorphic sphere a 1 \<inter> affine hull S"
using homeomorphic_translation homeomorphic_sym by blast
finally show "S - rel_interior S homeomorphic sphere a 1 \<inter> affine hull S" .
- have "S homeomorphic (op+ (-a) ` S)"
+ have "S homeomorphic ((+) (-a) ` S)"
by (metis homeomorphic_translation)
- also have "... homeomorphic cball 0 1 \<inter> affine hull (op+ (-a) ` S)"
+ also have "... homeomorphic cball 0 1 \<inter> affine hull ((+) (-a) ` S)"
by (rule starlike_compact_projective2_0 [OF 1 2 3])
- also have "... = op+ (-a) ` (cball a 1 \<inter> affine hull S)"
+ also have "... = (+) (-a) ` (cball a 1 \<inter> affine hull S)"
by (metis affine_hull_translation left_minus cball_translation translation_Int)
also have "... homeomorphic cball a 1 \<inter> affine hull S"
using homeomorphic_translation homeomorphic_sym by blast
@@ -623,13 +623,13 @@
have starT: "\<And>x. x \<in> T \<Longrightarrow> open_segment b x \<subseteq> rel_interior T"
using rel_interior_closure_convex_segment
b \<open>convex T\<close> closure_subset subsetCE by blast
- let ?aS = "op+ (-a) ` S" and ?bT = "op+ (-b) ` T"
+ let ?aS = "(+) (-a) ` S" and ?bT = "(+) (-b) ` T"
have 0: "0 \<in> affine hull ?aS" "0 \<in> affine hull ?bT"
by (metis a b subsetD hull_inc image_eqI left_minus rel_interior_subset)+
have subs: "subspace (span ?aS)" "subspace (span ?bT)"
by (rule subspace_span)+
moreover
- have "dim (span (op + (- a) ` S)) = dim (span (op + (- b) ` T))"
+ have "dim (span ((+) (- a) ` S)) = dim (span ((+) (- b) ` T))"
by (metis 0 aff_dim_translation_eq aff_dim_zero affeq dim_span nat_int)
ultimately obtain f g where "linear f" "linear g"
and fim: "f ` span ?aS = span ?bT"
@@ -649,9 +649,9 @@
by (metis b affine_hull_span_0 subsetD hull_inc image_eqI left_minus rel_interior_subset)
have "S homeomorphic cball a 1 \<inter> affine hull S"
by (rule starlike_compact_projective2 [OF \<open>compact S\<close> a starS])
- also have "... homeomorphic op+ (-a) ` (cball a 1 \<inter> affine hull S)"
+ also have "... homeomorphic (+) (-a) ` (cball a 1 \<inter> affine hull S)"
by (metis homeomorphic_translation)
- also have "... = cball 0 1 \<inter> op+ (-a) ` (affine hull S)"
+ also have "... = cball 0 1 \<inter> (+) (-a) ` (affine hull S)"
by (auto simp: dist_norm)
also have "... = cball 0 1 \<inter> span ?aS"
using eqspanS affine_hull_translation by blast
@@ -666,9 +666,9 @@
using gim gno apply (force simp:, clarify)
by (metis IntI fim1 gf image_eqI)
qed (auto simp: fg gf)
- also have "... = cball 0 1 \<inter> op+ (-b) ` (affine hull T)"
+ also have "... = cball 0 1 \<inter> (+) (-b) ` (affine hull T)"
using eqspanT affine_hull_translation by blast
- also have "... = op+ (-b) ` (cball b 1 \<inter> affine hull T)"
+ also have "... = (+) (-b) ` (cball b 1 \<inter> affine hull T)"
by (auto simp: dist_norm)
also have "... homeomorphic (cball b 1 \<inter> affine hull T)"
by (metis homeomorphic_translation homeomorphic_sym)
@@ -678,9 +678,9 @@
have "S - rel_interior S homeomorphic sphere a 1 \<inter> affine hull S"
by (rule starlike_compact_projective1 [OF \<open>compact S\<close> a starS])
- also have "... homeomorphic op+ (-a) ` (sphere a 1 \<inter> affine hull S)"
+ also have "... homeomorphic (+) (-a) ` (sphere a 1 \<inter> affine hull S)"
by (metis homeomorphic_translation)
- also have "... = sphere 0 1 \<inter> op+ (-a) ` (affine hull S)"
+ also have "... = sphere 0 1 \<inter> (+) (-a) ` (affine hull S)"
by (auto simp: dist_norm)
also have "... = sphere 0 1 \<inter> span ?aS"
using eqspanS affine_hull_translation by blast
@@ -695,9 +695,9 @@
using gim gno apply (force simp:, clarify)
by (metis IntI fim1 gf image_eqI)
qed (auto simp: fg gf)
- also have "... = sphere 0 1 \<inter> op+ (-b) ` (affine hull T)"
+ also have "... = sphere 0 1 \<inter> (+) (-b) ` (affine hull T)"
using eqspanT affine_hull_translation by blast
- also have "... = op+ (-b) ` (sphere b 1 \<inter> affine hull T)"
+ also have "... = (+) (-b) ` (sphere b 1 \<inter> affine hull T)"
by (auto simp: dist_norm)
also have "... homeomorphic (sphere b 1 \<inter> affine hull T)"
by (metis homeomorphic_translation homeomorphic_sym)
@@ -833,11 +833,11 @@
then have inj: "inj (\<lambda>x::'a. x /\<^sub>R norm (a - b))"
by (simp add: inj_on_def)
have "((sphere a r \<inter> T) - {b}) homeomorphic
- op+ (-a) ` ((sphere a r \<inter> T) - {b})"
+ (+) (-a) ` ((sphere a r \<inter> T) - {b})"
by (rule homeomorphic_translation)
- also have "... homeomorphic op *\<^sub>R (inverse r) ` op + (- a) ` (sphere a r \<inter> T - {b})"
+ also have "... homeomorphic ( *\<^sub>R) (inverse r) ` (+) (- a) ` (sphere a r \<inter> T - {b})"
by (metis \<open>0 < r\<close> homeomorphic_scaling inverse_inverse_eq inverse_zero less_irrefl)
- also have "... = sphere 0 1 \<inter> (op *\<^sub>R (inverse r) ` op + (- a) ` T) - {(b - a) /\<^sub>R r}"
+ also have "... = sphere 0 1 \<inter> (( *\<^sub>R) (inverse r) ` (+) (- a) ` T) - {(b - a) /\<^sub>R r}"
using assms by (auto simp: dist_norm norm_minus_commute divide_simps)
also have "... homeomorphic p"
apply (rule homeomorphic_punctured_affine_sphere_affine_01)
@@ -928,27 +928,27 @@
then obtain a where "a \<in> S" by auto
obtain i::'n where i: "i \<in> Basis" "i \<noteq> 0"
using SOME_Basis Basis_zero by force
- have "0 \<in> affine hull (op + (- a) ` S)"
+ have "0 \<in> affine hull ((+) (- a) ` S)"
by (simp add: \<open>a \<in> S\<close> hull_inc)
- then have "dim (op + (- a) ` S) = aff_dim (op + (- a) ` S)"
+ then have "dim ((+) (- a) ` S) = aff_dim ((+) (- a) ` S)"
by (simp add: aff_dim_zero)
also have "... < DIM('n)"
by (simp add: aff_dim_translation_eq assms)
- finally have dd: "dim (op + (- a) ` S) < DIM('n)"
+ finally have dd: "dim ((+) (- a) ` S) < DIM('n)"
by linarith
obtain T where "subspace T" and Tsub: "T \<subseteq> {x. i \<bullet> x = 0}"
- and dimT: "dim T = dim (op + (- a) ` S)"
- apply (rule choose_subspace_of_subspace [of "dim (op + (- a) ` S)" "{x::'n. i \<bullet> x = 0}"])
+ and dimT: "dim T = dim ((+) (- a) ` S)"
+ apply (rule choose_subspace_of_subspace [of "dim ((+) (- a) ` S)" "{x::'n. i \<bullet> x = 0}"])
apply (simp add: dim_hyperplane [OF \<open>i \<noteq> 0\<close>])
apply (metis DIM_positive Suc_pred dd not_le not_less_eq_eq)
apply (metis span_eq subspace_hyperplane)
done
- have "subspace (span (op + (- a) ` S))"
+ have "subspace (span ((+) (- a) ` S))"
using subspace_span by blast
then obtain h k where "linear h" "linear k"
- and heq: "h ` span (op + (- a) ` S) = T"
- and keq:"k ` T = span (op + (- a) ` S)"
- and hinv [simp]: "\<And>x. x \<in> span (op + (- a) ` S) \<Longrightarrow> k(h x) = x"
+ and heq: "h ` span ((+) (- a) ` S) = T"
+ and keq:"k ` T = span ((+) (- a) ` S)"
+ and hinv [simp]: "\<And>x. x \<in> span ((+) (- a) ` S) \<Longrightarrow> k(h x) = x"
and kinv [simp]: "\<And>x. x \<in> T \<Longrightarrow> h(k x) = x"
apply (rule isometries_subspaces [OF _ \<open>subspace T\<close>])
apply (auto simp: dimT)
@@ -964,38 +964,38 @@
by (metis DIM_positive Suc_eq_plus1 add.left_neutral diff_add_cancel not_le not_less_eq_eq of_nat_1 of_nat_diff)
then obtain f g where fg: "homeomorphism (sphere 0 1 - {i}) {x. i \<bullet> x = 0} f g"
by (force simp: homeomorphic_def)
- have "h ` op + (- a) ` S \<subseteq> T"
+ have "h ` (+) (- a) ` S \<subseteq> T"
using heq span_clauses(1) span_linear_image by blast
- then have "g ` h ` op + (- a) ` S \<subseteq> g ` {x. i \<bullet> x = 0}"
+ then have "g ` h ` (+) (- a) ` S \<subseteq> g ` {x. i \<bullet> x = 0}"
using Tsub by (simp add: image_mono)
also have "... \<subseteq> sphere 0 1 - {i}"
by (simp add: fg [unfolded homeomorphism_def])
- finally have gh_sub_sph: "(g \<circ> h) ` op + (- a) ` S \<subseteq> sphere 0 1 - {i}"
+ finally have gh_sub_sph: "(g \<circ> h) ` (+) (- a) ` S \<subseteq> sphere 0 1 - {i}"
by (metis image_comp)
- then have gh_sub_cb: "(g \<circ> h) ` op + (- a) ` S \<subseteq> cball 0 1"
+ then have gh_sub_cb: "(g \<circ> h) ` (+) (- a) ` S \<subseteq> cball 0 1"
by (metis Diff_subset order_trans sphere_cball)
have [simp]: "\<And>u. u \<in> S \<Longrightarrow> norm (g (h (u - a))) = 1"
using gh_sub_sph [THEN subsetD] by (auto simp: o_def)
- have ghcont: "continuous_on (op + (- a) ` S) (\<lambda>x. g (h x))"
+ have ghcont: "continuous_on ((+) (- a) ` S) (\<lambda>x. g (h x))"
apply (rule continuous_on_compose2 [OF homeomorphism_cont2 [OF fg] hcont], force)
done
- have kfcont: "continuous_on ((g \<circ> h \<circ> op + (- a)) ` S) (\<lambda>x. k (f x))"
+ have kfcont: "continuous_on ((g \<circ> h \<circ> (+) (- a)) ` S) (\<lambda>x. k (f x))"
apply (rule continuous_on_compose2 [OF kcont])
using homeomorphism_cont1 [OF fg] gh_sub_sph apply (force intro: continuous_on_subset, blast)
done
- have "S homeomorphic op + (- a) ` S"
+ have "S homeomorphic (+) (- a) ` S"
by (simp add: homeomorphic_translation)
- also have Shom: "\<dots> homeomorphic (g \<circ> h) ` op + (- a) ` S"
+ also have Shom: "\<dots> homeomorphic (g \<circ> h) ` (+) (- a) ` S"
apply (simp add: homeomorphic_def homeomorphism_def)
apply (rule_tac x="g \<circ> h" in exI)
apply (rule_tac x="k \<circ> f" in exI)
apply (auto simp: ghcont kfcont span_clauses(1) homeomorphism_apply2 [OF fg] image_comp)
apply (force simp: o_def homeomorphism_apply2 [OF fg] span_clauses(1))
done
- finally have Shom: "S homeomorphic (g \<circ> h) ` op + (- a) ` S" .
+ finally have Shom: "S homeomorphic (g \<circ> h) ` (+) (- a) ` S" .
show ?thesis
- apply (rule_tac U = "ball 0 1 \<union> image (g o h) (op + (- a) ` S)"
- and T = "image (g o h) (op + (- a) ` S)"
+ apply (rule_tac U = "ball 0 1 \<union> image (g o h) ((+) (- a) ` S)"
+ and T = "image (g o h) ((+) (- a) ` S)"
in that)
apply (rule convex_intermediate_ball [of 0 1], force)
using gh_sub_cb apply force
@@ -2210,26 +2210,26 @@
and pq'_eq: "\<And>t. t \<in> {0..1} \<Longrightarrow> p (q' t) = (f \<circ> g +++ reversepath g') t"
using covering_space_lift_homotopic_path [OF cov homotopic_paths_sym [OF homS] \<open>path q\<close> piq refl refl]
by auto
- have "q' t = (h \<circ> op *\<^sub>R 2) t" if "0 \<le> t" "t \<le> 1/2" for t
- proof (rule covering_space_lift_unique [OF cov, of q' 0 "h \<circ> op *\<^sub>R 2" "{0..1/2}" "f \<circ> g \<circ> op *\<^sub>R 2" t])
- show "q' 0 = (h \<circ> op *\<^sub>R 2) 0"
+ have "q' t = (h \<circ> ( *\<^sub>R) 2) t" if "0 \<le> t" "t \<le> 1/2" for t
+ proof (rule covering_space_lift_unique [OF cov, of q' 0 "h \<circ> ( *\<^sub>R) 2" "{0..1/2}" "f \<circ> g \<circ> ( *\<^sub>R) 2" t])
+ show "q' 0 = (h \<circ> ( *\<^sub>R) 2) 0"
by (metis \<open>pathstart q' = pathstart q\<close> comp_def g h pastq pathstart_def pth_4(2))
- show "continuous_on {0..1/2} (f \<circ> g \<circ> op *\<^sub>R 2)"
+ show "continuous_on {0..1/2} (f \<circ> g \<circ> ( *\<^sub>R) 2)"
apply (intro continuous_intros continuous_on_compose continuous_on_path [OF \<open>path g\<close>] continuous_on_subset [OF contf])
using g(2) path_image_def by fastforce+
- show "(f \<circ> g \<circ> op *\<^sub>R 2) ` {0..1/2} \<subseteq> S"
+ show "(f \<circ> g \<circ> ( *\<^sub>R) 2) ` {0..1/2} \<subseteq> S"
using g(2) path_image_def fim by fastforce
- show "(h \<circ> op *\<^sub>R 2) ` {0..1/2} \<subseteq> C"
+ show "(h \<circ> ( *\<^sub>R) 2) ` {0..1/2} \<subseteq> C"
using h path_image_def by fastforce
show "q' ` {0..1/2} \<subseteq> C"
using \<open>path_image q' \<subseteq> C\<close> path_image_def by fastforce
- show "\<And>x. x \<in> {0..1/2} \<Longrightarrow> (f \<circ> g \<circ> op *\<^sub>R 2) x = p (q' x)"
+ show "\<And>x. x \<in> {0..1/2} \<Longrightarrow> (f \<circ> g \<circ> ( *\<^sub>R) 2) x = p (q' x)"
by (auto simp: joinpaths_def pq'_eq)
- show "\<And>x. x \<in> {0..1/2} \<Longrightarrow> (f \<circ> g \<circ> op *\<^sub>R 2) x = p ((h \<circ> op *\<^sub>R 2) x)"
+ show "\<And>x. x \<in> {0..1/2} \<Longrightarrow> (f \<circ> g \<circ> ( *\<^sub>R) 2) x = p ((h \<circ> ( *\<^sub>R) 2) x)"
by (simp add: phg)
show "continuous_on {0..1/2} q'"
by (simp add: continuous_on_path \<open>path q'\<close>)
- show "continuous_on {0..1/2} (h \<circ> op *\<^sub>R 2)"
+ show "continuous_on {0..1/2} (h \<circ> ( *\<^sub>R) 2)"
apply (intro continuous_intros continuous_on_compose continuous_on_path [OF \<open>path h\<close>], force)
done
qed (use that in auto)
--- a/src/HOL/Analysis/Improper_Integral.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Improper_Integral.thy Wed Jan 10 15:25:09 2018 +0100
@@ -967,7 +967,7 @@
by (simp add: sum.union_disjoint T''_eq disj \<open>finite A\<close> \<open>finite B\<close>)
also have "... = (\<Sum>(x,K) \<in> A. norm (integral K h - integral K f)) +
(\<Sum>(x,K) \<in> B. norm (?CI K h x + integral K f))"
- by (auto simp: A_def B_def f norm_minus_commute intro!: sum.cong arg_cong2 [where f= "op+"])
+ by (auto simp: A_def B_def f norm_minus_commute intro!: sum.cong arg_cong2 [where f= "(+)"])
also have "... \<le> (\<Sum>(x,K)\<in>A. norm (integral K h)) +
(\<Sum>(x,K)\<in>(\<lambda>(x,K). (x,K \<inter> {x. x \<bullet> i \<le> c})) ` A. norm (integral K h))
+ ((\<Sum>(x,K)\<in>B. norm (?CI K h x)) +
@@ -1663,4 +1663,4 @@
qed
end
-
\ No newline at end of file
+
--- a/src/HOL/Analysis/Inner_Product.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Inner_Product.thy Wed Jan 10 15:25:09 2018 +0100
@@ -239,7 +239,7 @@
instantiation real :: real_inner
begin
-definition inner_real_def [simp]: "inner = op *"
+definition inner_real_def [simp]: "inner = ( * )"
instance
proof
--- a/src/HOL/Analysis/Lebesgue_Measure.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Wed Jan 10 15:25:09 2018 +0100
@@ -750,10 +750,10 @@
finally show "lebesgue = density (distr lebesgue lebesgue T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))" .
qed
-lemma lebesgue_measurable_scaling[measurable]: "op *\<^sub>R x \<in> lebesgue \<rightarrow>\<^sub>M lebesgue"
+lemma lebesgue_measurable_scaling[measurable]: "( *\<^sub>R) x \<in> lebesgue \<rightarrow>\<^sub>M lebesgue"
proof cases
assume "x = 0"
- then have "op *\<^sub>R x = (\<lambda>x. 0::'a)"
+ then have "( *\<^sub>R) x = (\<lambda>x. 0::'a)"
by (auto simp: fun_eq_iff)
then show ?thesis by auto
next
@@ -843,9 +843,9 @@
lemma lborel_distr_mult:
assumes "(c::real) \<noteq> 0"
- shows "distr lborel borel (op * c) = density lborel (\<lambda>_. inverse \<bar>c\<bar>)"
+ shows "distr lborel borel (( * ) c) = density lborel (\<lambda>_. inverse \<bar>c\<bar>)"
proof-
- have "distr lborel borel (op * c) = distr lborel lborel (op * c)" by (simp cong: distr_cong)
+ have "distr lborel borel (( * ) c) = distr lborel lborel (( * ) c)" by (simp cong: distr_cong)
also from assms have "... = density lborel (\<lambda>_. inverse \<bar>c\<bar>)"
by (subst lborel_real_affine[of "inverse c" 0]) (auto simp: o_def distr_density_distr)
finally show ?thesis .
@@ -853,18 +853,18 @@
lemma lborel_distr_mult':
assumes "(c::real) \<noteq> 0"
- shows "lborel = density (distr lborel borel (op * c)) (\<lambda>_. \<bar>c\<bar>)"
+ shows "lborel = density (distr lborel borel (( * ) c)) (\<lambda>_. \<bar>c\<bar>)"
proof-
have "lborel = density lborel (\<lambda>_. 1)" by (rule density_1[symmetric])
also from assms have "(\<lambda>_. 1 :: ennreal) = (\<lambda>_. inverse \<bar>c\<bar> * \<bar>c\<bar>)" by (intro ext) simp
also have "density lborel ... = density (density lborel (\<lambda>_. inverse \<bar>c\<bar>)) (\<lambda>_. \<bar>c\<bar>)"
by (subst density_density_eq) (auto simp: ennreal_mult)
- also from assms have "density lborel (\<lambda>_. inverse \<bar>c\<bar>) = distr lborel borel (op * c)"
+ also from assms have "density lborel (\<lambda>_. inverse \<bar>c\<bar>) = distr lborel borel (( * ) c)"
by (rule lborel_distr_mult[symmetric])
finally show ?thesis .
qed
-lemma lborel_distr_plus: "distr lborel borel (op + c) = (lborel :: real measure)"
+lemma lborel_distr_plus: "distr lborel borel ((+) c) = (lborel :: real measure)"
by (subst lborel_real_affine[of 1 c]) (auto simp: density_1 one_ennreal_def[symmetric])
interpretation lborel: sigma_finite_measure lborel
@@ -885,7 +885,7 @@
"box (la, lb) (ua, ub) = box la ua \<times> box lb ub"
using lu[of _ 0] lu[of 0] by (auto intro!: inj_onI simp add: Basis_prod_def ball_Un box_def)
show "emeasure (lborel \<Otimes>\<^sub>M lborel) (box (la, lb) (ua, ub)) =
- ennreal (prod (op \<bullet> ((ua, ub) - (la, lb))) Basis)"
+ ennreal (prod ((\<bullet>) ((ua, ub) - (la, lb))) Basis)"
by (simp add: lborel.emeasure_pair_measure_Times Basis_prod_def prod.union_disjoint
prod.reindex ennreal_mult inner_diff_left prod_nonneg)
qed (simp add: borel_prod[symmetric])
@@ -994,7 +994,7 @@
let ?f = "\<lambda>n. root DIM('a) (Suc n)"
- have vimage_eq_image: "op *\<^sub>R (?f n) -` S = op *\<^sub>R (1 / ?f n) ` S" for n
+ have vimage_eq_image: "( *\<^sub>R) (?f n) -` S = ( *\<^sub>R) (1 / ?f n) ` S" for n
apply safe
subgoal for x by (rule image_eqI[of _ _ "?f n *\<^sub>R x"]) auto
subgoal by auto
@@ -1016,20 +1016,20 @@
by (intro summable_iff_suminf_neq_top) (auto simp add: inverse_eq_divide)
then have "top * emeasure lebesgue S = (\<Sum>n. (1 / ?f n)^DIM('a) * emeasure lebesgue S)"
unfolding ennreal_suminf_multc eq by simp
- also have "\<dots> = (\<Sum>n. emeasure lebesgue (op *\<^sub>R (?f n) -` S))"
+ also have "\<dots> = (\<Sum>n. emeasure lebesgue (( *\<^sub>R) (?f n) -` S))"
unfolding vimage_eq_image using emeasure_lebesgue_affine[of "1 / ?f n" 0 S for n] by simp
- also have "\<dots> = emeasure lebesgue (\<Union>n. op *\<^sub>R (?f n) -` S)"
+ also have "\<dots> = emeasure lebesgue (\<Union>n. ( *\<^sub>R) (?f n) -` S)"
proof (intro suminf_emeasure)
- show "disjoint_family (\<lambda>n. op *\<^sub>R (?f n) -` S)"
+ show "disjoint_family (\<lambda>n. ( *\<^sub>R) (?f n) -` S)"
unfolding disjoint_family_on_def
proof safe
fix m n :: nat and x assume "m \<noteq> n" "?f m *\<^sub>R x \<in> S" "?f n *\<^sub>R x \<in> S"
with eq1[of "?f m / ?f n" "?f n *\<^sub>R x"] show "x \<in> {}"
by auto
qed
- have "op *\<^sub>R (?f i) -` S \<in> sets lebesgue" for i
+ have "( *\<^sub>R) (?f i) -` S \<in> sets lebesgue" for i
using measurable_sets[OF lebesgue_measurable_scaling[of "?f i"] S] by auto
- then show "range (\<lambda>i. op *\<^sub>R (?f i) -` S) \<subseteq> sets lebesgue"
+ then show "range (\<lambda>i. ( *\<^sub>R) (?f i) -` S) \<subseteq> sets lebesgue"
by auto
qed
also have "\<dots> \<le> emeasure lebesgue (ball 0 M :: 'a set)"
--- a/src/HOL/Analysis/Linear_Algebra.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy Wed Jan 10 15:25:09 2018 +0100
@@ -980,7 +980,7 @@
by (intro sum.mono_neutral_cong_left) (auto intro: X)
also have "\<dots> = (\<Sum>z\<in>{z. X x z \<noteq> 0}. X x z *\<^sub>R z) + (\<Sum>z\<in>{z. X y z \<noteq> 0}. X y z *\<^sub>R z)"
by (auto simp add: scaleR_add_left sum.distrib
- intro!: arg_cong2[where f="op +"] sum.mono_neutral_cong_right X)
+ intro!: arg_cong2[where f="(+)"] sum.mono_neutral_cong_right X)
also have "\<dots> = x + y"
by (simp add: X(3)[symmetric])
also have "\<dots> = (\<Sum>z | X (x + y) z \<noteq> 0. X (x + y) z *\<^sub>R z)"
@@ -1024,7 +1024,7 @@
show "g (x + y) = g x + g y"
unfolding g_def X_add *
by (auto simp add: scaleR_add_left sum.distrib
- intro!: arg_cong2[where f="op +"] sum.mono_neutral_cong_right X)
+ intro!: arg_cong2[where f="(+)"] sum.mono_neutral_cong_right X)
next
show "g (r *\<^sub>R x) = r *\<^sub>R g x" for r x
by (auto simp add: g_def X_cmult scaleR_sum_right intro!: sum.mono_neutral_cong_left X)
@@ -1398,7 +1398,7 @@
by (simp add: norm_eq_sqrt_inner)
-text\<open>Equality of vectors in terms of @{term "op \<bullet>"} products.\<close>
+text\<open>Equality of vectors in terms of @{term "(\<bullet>)"} products.\<close>
lemma linear_componentwise:
fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
--- a/src/HOL/Analysis/Measure_Space.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy Wed Jan 10 15:25:09 2018 +0100
@@ -2348,7 +2348,7 @@
case True
show ?thesis
proof (rule emeasure_measure_of[OF restrict_space_def])
- show "op \<inter> \<Omega> ` sets M \<subseteq> Pow (\<Omega> \<inter> space M)" "A \<in> sets (restrict_space M \<Omega>)"
+ show "(\<inter>) \<Omega> ` sets M \<subseteq> Pow (\<Omega> \<inter> space M)" "A \<in> sets (restrict_space M \<Omega>)"
using \<open>A \<subseteq> \<Omega>\<close> \<open>A \<in> sets M\<close> sets.space_closed by (auto simp: sets_restrict_space)
show "positive (sets (restrict_space M \<Omega>)) (emeasure M)"
by (auto simp: positive_def)
@@ -2427,7 +2427,7 @@
from sigma_finite_countable obtain C
where C: "countable C" "C \<subseteq> sets M" "(\<Union>C) = space M" "\<forall>a\<in>C. emeasure M a \<noteq> \<infinity>"
by blast
- let ?C = "op \<inter> A ` C"
+ let ?C = "(\<inter>) A ` C"
from C have "countable ?C" "?C \<subseteq> sets (restrict_space M A)" "(\<Union>?C) = space (restrict_space M A)"
by(auto simp add: sets_restrict_space space_restrict_space)
moreover {
@@ -2861,7 +2861,7 @@
also have "\<dots> = ?S (\<Union>i. X i)"
unfolding UN_extend_simps(4)
by (auto simp add: suminf_add[symmetric] Diff_eq[symmetric] simp del: UN_simps
- intro!: SUP_cong arg_cong2[where f="op +"] suminf_emeasure
+ intro!: SUP_cong arg_cong2[where f="(+)"] suminf_emeasure
disjoint_family_on_bisimulation[OF \<open>disjoint_family X\<close>])
finally show "(\<Sum>i. ?S (X i)) = ?S (\<Union>i. X i)" .
qed
@@ -3395,13 +3395,13 @@
lemma emeasure_SUP_chain:
assumes sets: "\<And>i. i \<in> A \<Longrightarrow> sets (M i) = sets N" "X \<in> sets N"
- assumes ch: "Complete_Partial_Order.chain op \<le> (M ` A)" and "A \<noteq> {}"
+ assumes ch: "Complete_Partial_Order.chain (\<le>) (M ` A)" and "A \<noteq> {}"
shows "emeasure (SUP i:A. M i) X = (SUP i:A. emeasure (M i) X)"
proof (subst emeasure_SUP[OF sets \<open>A \<noteq> {}\<close>])
show "(SUP J:{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> A}. emeasure (SUPREMUM J M) X) = (SUP i:A. emeasure (M i) X)"
proof (rule SUP_eq)
fix J assume "J \<in> {J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> A}"
- then have J: "Complete_Partial_Order.chain op \<le> (M ` J)" "finite J" "J \<noteq> {}" and "J \<subseteq> A"
+ then have J: "Complete_Partial_Order.chain (\<le>) (M ` J)" "finite J" "J \<noteq> {}" and "J \<subseteq> A"
using ch[THEN chain_subset, of "M`J"] by auto
with in_chain_finite[OF J(1)] obtain j where "j \<in> J" "(SUP j:J. M j) = M j"
by auto
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Wed Jan 10 15:25:09 2018 +0100
@@ -276,11 +276,11 @@
thus ?thesis by (simp_all add: comp_def)
qed
-lemmas simple_function_add[intro, simp] = simple_function_compose2[where h="op +"]
- and simple_function_diff[intro, simp] = simple_function_compose2[where h="op -"]
+lemmas simple_function_add[intro, simp] = simple_function_compose2[where h="(+)"]
+ and simple_function_diff[intro, simp] = simple_function_compose2[where h="(-)"]
and simple_function_uminus[intro, simp] = simple_function_compose[where g="uminus"]
- and simple_function_mult[intro, simp] = simple_function_compose2[where h="op *"]
- and simple_function_div[intro, simp] = simple_function_compose2[where h="op /"]
+ and simple_function_mult[intro, simp] = simple_function_compose2[where h="( * )"]
+ and simple_function_div[intro, simp] = simple_function_compose2[where h="(/)"]
and simple_function_inverse[intro, simp] = simple_function_compose[where g="inverse"]
and simple_function_max[intro, simp] = simple_function_compose2[where h=max]
@@ -760,7 +760,7 @@
using assms by (intro simple_function_partition) auto
also have "\<dots> = (\<Sum>y\<in>(\<lambda>x. (f x, indicator A x::ennreal))`space M.
if snd y = 1 then fst y * emeasure M (f -` {fst y} \<inter> space M \<inter> A) else 0)"
- by (auto simp: indicator_def split: if_split_asm intro!: arg_cong2[where f="op *"] arg_cong2[where f=emeasure] sum.cong)
+ by (auto simp: indicator_def split: if_split_asm intro!: arg_cong2[where f="( * )"] arg_cong2[where f=emeasure] sum.cong)
also have "\<dots> = (\<Sum>y\<in>(\<lambda>x. (f x, 1::ennreal))`A. fst y * emeasure M (f -` {fst y} \<inter> space M \<inter> A))"
using assms by (subst sum.If_cases) (auto intro!: simple_functionD(1) simp: eq)
also have "\<dots> = (\<Sum>y\<in>fst`(\<lambda>x. (f x, 1::ennreal))`A. y * emeasure M (f -` {y} \<inter> space M \<inter> A))"
@@ -1873,7 +1873,7 @@
lemma nn_integral_monotone_convergence_SUP_nat:
fixes f :: "'a \<Rightarrow> nat \<Rightarrow> ennreal"
- assumes chain: "Complete_Partial_Order.chain op \<le> (f ` Y)"
+ assumes chain: "Complete_Partial_Order.chain (\<le>) (f ` Y)"
and nonempty: "Y \<noteq> {}"
shows "(\<integral>\<^sup>+ x. (SUP i:Y. f i x) \<partial>count_space UNIV) = (SUP i:Y. (\<integral>\<^sup>+ x. f i x \<partial>count_space UNIV))"
(is "?lhs = ?rhs" is "integral\<^sup>N ?M _ = _")
@@ -1913,7 +1913,7 @@
case True
let ?Y = "I ` {..<m}"
have "f ` ?Y \<subseteq> f ` Y" using I by auto
- with chain have chain': "Complete_Partial_Order.chain op \<le> (f ` ?Y)" by(rule chain_subset)
+ with chain have chain': "Complete_Partial_Order.chain (\<le>) (f ` ?Y)" by(rule chain_subset)
hence "Sup (f ` ?Y) \<in> f ` ?Y"
by(rule ccpo_class.in_chain_finite)(auto simp add: True lessThan_empty_iff)
then obtain m' where "m' < m" and m': "(SUP i:?Y. f i) = f (I m')" by auto
--- a/src/HOL/Analysis/Path_Connected.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy Wed Jan 10 15:25:09 2018 +0100
@@ -1659,7 +1659,7 @@
fixes a :: "'a :: topological_group_add"
shows "path_connected ((\<lambda>x. a + x) ` S) = path_connected S"
proof -
- have "\<forall>x y. op + (x::'a) ` op + (0 - x) ` y = y"
+ have "\<forall>x y. (+) (x::'a) ` (+) (0 - x) ` y = y"
by (simp add: image_image)
then show ?thesis
by (metis (no_types) path_connected_translationI)
@@ -1738,7 +1738,7 @@
case True then show ?thesis
by (simp add: path_component_refl_eq pathstart_def)
next
- case False have "continuous_on {0..1} (p o (op* y))"
+ case False have "continuous_on {0..1} (p o (( * ) y))"
apply (rule continuous_intros)+
using p [unfolded path_def] y
apply (auto simp: mult_le_one intro: continuous_on_subset [of _ p])
@@ -2012,7 +2012,7 @@
by (intro path_connected_continuous_image path_connected_punctured_universe assms)
with eq have "path_connected (sphere (0::'a) r)"
by auto
- then have "path_connected(op + a ` (sphere (0::'a) r))"
+ then have "path_connected((+) a ` (sphere (0::'a) r))"
by (simp add: path_connected_translation)
then show ?thesis
by (metis add.right_neutral sphere_translation)
@@ -2241,7 +2241,7 @@
assumes "DIM('a) = 1" and "r > 0"
obtains x y where "sphere a r = {x,y} \<and> dist x y = 2*r"
proof -
- have "sphere a r = op + a ` sphere 0 r"
+ have "sphere a r = (+) a ` sphere 0 r"
by (metis add.right_neutral sphere_translation)
then show ?thesis
using sphere_1D_doubleton_zero [OF assms]
@@ -2282,7 +2282,7 @@
assumes 2: "2 \<le> DIM('N)" and pc: "path_connected {r. 0 \<le> r \<and> P r}"
shows "path_connected {x. P(norm(x - a))}"
proof -
- have "{x. P(norm(x - a))} = op+ a ` {x. P(norm x)}"
+ have "{x. P(norm(x - a))} = (+) a ` {x. P(norm x)}"
by force
moreover have "path_connected {x::'N. P(norm x)}"
proof -
@@ -6534,13 +6534,13 @@
next
case False
then obtain a b where ab: "a \<in> S" "b \<in> T" by auto
- then have ss: "subspace (op + (- a) ` S)" "subspace (op + (- b) ` T)"
+ then have ss: "subspace ((+) (- a) ` S)" "subspace ((+) (- b) ` T)"
using affine_diffs_subspace assms by blast+
- have dd: "dim (op + (- a) ` S) = dim (op + (- b) ` T)"
+ have dd: "dim ((+) (- a) ` S) = dim ((+) (- b) ` T)"
using assms ab by (simp add: aff_dim_eq_dim [OF hull_inc] image_def)
- have "S homeomorphic (op + (- a) ` S)"
+ have "S homeomorphic ((+) (- a) ` S)"
by (simp add: homeomorphic_translation)
- also have "... homeomorphic (op + (- b) ` T)"
+ also have "... homeomorphic ((+) (- b) ` T)"
by (rule homeomorphic_subspaces [OF ss dd])
also have "... homeomorphic T"
using homeomorphic_sym homeomorphic_translation by auto
@@ -6792,7 +6792,7 @@
lemma homotopy_eqv_translation:
fixes S :: "'a::real_normed_vector set"
- shows "op + a ` S homotopy_eqv S"
+ shows "(+) a ` S homotopy_eqv S"
apply (rule homeomorphic_imp_homotopy_eqv)
using homeomorphic_translation homeomorphic_sym by blast
--- a/src/HOL/Analysis/Polytope.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Polytope.thy Wed Jan 10 15:25:09 2018 +0100
@@ -18,9 +18,9 @@
unfolding face_of_def by blast
lemma face_of_translation_eq [simp]:
- "(op + a ` T face_of op + a ` S) \<longleftrightarrow> T face_of S"
+ "((+) a ` T face_of (+) a ` S) \<longleftrightarrow> T face_of S"
proof -
- have *: "\<And>a T S. T face_of S \<Longrightarrow> (op + a ` T face_of op + a ` S)"
+ have *: "\<And>a T S. T face_of S \<Longrightarrow> ((+) a ` T face_of (+) a ` S)"
apply (simp add: face_of_def Ball_def, clarify)
apply (drule open_segment_translation_eq [THEN iffD1])
using inj_image_mem_iff inj_add_left apply metis
@@ -1125,7 +1125,7 @@
and ab: "\<And>x. x \<in> closure(convex hull {x. x extreme_point_of S}) \<Longrightarrow> b < a \<bullet> x"
using separating_hyperplane_closed_point [of "closure(convex hull {x. x extreme_point_of S})"]
by blast
- have "continuous_on S (op \<bullet> a)"
+ have "continuous_on S ((\<bullet>) a)"
by (rule continuous_intros)+
then obtain m where "m \<in> S" and m: "\<And>y. y \<in> S \<Longrightarrow> a \<bullet> m \<le> a \<bullet> y"
using continuous_attains_inf [of S "\<lambda>x. a \<bullet> x"] \<open>compact S\<close> \<open>u \<in> S\<close>
@@ -1206,9 +1206,9 @@
show "S \<subseteq> convex hull {x. x extreme_point_of S}"
proof
fix a assume [simp]: "a \<in> S"
- have 1: "compact (op + (- a) ` S)"
+ have 1: "compact ((+) (- a) ` S)"
by (simp add: \<open>compact S\<close> compact_translation)
- have 2: "convex (op + (- a) ` S)"
+ have 2: "convex ((+) (- a) ` S)"
by (simp add: \<open>convex S\<close> convex_translation)
show a_invex: "a \<in> convex hull {x. x extreme_point_of S}"
using Krein_Milman_Minkowski_aux [OF refl 1 2]
@@ -1630,9 +1630,9 @@
proof -
obtain v where "finite v" "S = convex hull v"
using assms polytope_def by auto
- have "finite (op hull convex ` {T. T \<subseteq> v})"
+ have "finite ((hull) convex ` {T. T \<subseteq> v})"
by (simp add: \<open>finite v\<close>)
- moreover have "{F. F face_of S} \<subseteq> (op hull convex ` {T. T \<subseteq> v})"
+ moreover have "{F. F face_of S} \<subseteq> ((hull) convex ` {T. T \<subseteq> v})"
by (metis (no_types, lifting) \<open>finite v\<close> \<open>S = convex hull v\<close> face_of_convex_hull_subset finite_imp_compact image_eqI mem_Collect_eq subsetI)
ultimately show ?thesis
by (blast intro: finite_subset)
@@ -2503,9 +2503,9 @@
case 1 then show ?thesis .
next
case 2
- have "Collect (op \<in> x) \<notin> Collect (op \<in> (\<Union>{A. A facet_of S}))"
+ have "Collect ((\<in>) x) \<notin> Collect ((\<in>) (\<Union>{A. A facet_of S}))"
using xnot by fastforce
- then have "F \<notin> Collect (op \<in> h)"
+ then have "F \<notin> Collect ((\<in>) h)"
using 2 \<open>x \<in> S\<close> facet by blast
with \<open>h \<in> F\<close> have "\<Inter>F \<subseteq> S \<inter> {x. a h \<bullet> x = b h}" by blast
with 2 that \<open>x \<in> \<Inter>F\<close> show ?thesis
@@ -2661,7 +2661,7 @@
apply (auto simp: \<open>bij h\<close> bij_is_surj image_f_inv_f)
done
have "inj h" using bij_is_inj assms by blast
- then have injim: "inj_on (op ` h) A" for A
+ then have injim: "inj_on ((`) h) A" for A
by (simp add: inj_on_def inj_image_eq_iff)
show ?thesis
using \<open>linear h\<close> \<open>inj h\<close>
--- a/src/HOL/Analysis/Riemann_Mapping.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Riemann_Mapping.thy Wed Jan 10 15:25:09 2018 +0100
@@ -138,17 +138,17 @@
proof (intro bdd_aboveI exI ballI, clarify)
show "norm (deriv f 0) \<le> 1 / r" if "f \<in> F" for f
proof -
- have r01: "op * (complex_of_real r) ` ball 0 1 \<subseteq> S"
+ have r01: "( * ) (complex_of_real r) ` ball 0 1 \<subseteq> S"
using that \<open>r > 0\<close> by (auto simp: norm_mult r [THEN subsetD])
- then have "f holomorphic_on op * (complex_of_real r) ` ball 0 1"
+ then have "f holomorphic_on ( * ) (complex_of_real r) ` ball 0 1"
using holomorphic_on_subset [OF holF] by (simp add: that)
then have holf: "f \<circ> (\<lambda>z. (r * z)) holomorphic_on (ball 0 1)"
by (intro holomorphic_intros holomorphic_on_compose)
- have f0: "(f \<circ> op * (complex_of_real r)) 0 = 0"
+ have f0: "(f \<circ> ( * ) (complex_of_real r)) 0 = 0"
using F_def that by auto
have "f ` S \<subseteq> ball 0 1"
using F_def that by blast
- with r01 have fr1: "\<And>z. norm z < 1 \<Longrightarrow> norm ((f \<circ> op*(of_real r))z) < 1"
+ with r01 have fr1: "\<And>z. norm z < 1 \<Longrightarrow> norm ((f \<circ> ( * )(of_real r))z) < 1"
by force
have *: "((\<lambda>w. f (r * w)) has_field_derivative deriv f (r * z) * r) (at z)"
if "z \<in> ball 0 1" for z::complex
@@ -162,7 +162,7 @@
using * [of 0] by simp
have deq: "deriv (\<lambda>x. f (complex_of_real r * x)) 0 = deriv f 0 * complex_of_real r"
using DERIV_imp_deriv df0 by blast
- have "norm (deriv (f \<circ> op * (complex_of_real r)) 0) \<le> 1"
+ have "norm (deriv (f \<circ> ( * ) (complex_of_real r)) 0) \<le> 1"
by (auto intro: Schwarz_Lemma [OF holf f0 fr1, of 0])
with \<open>r > 0\<close> show ?thesis
by (simp add: deq norm_mult divide_simps o_def)
--- a/src/HOL/Analysis/Set_Integral.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Set_Integral.thy Wed Jan 10 15:25:09 2018 +0100
@@ -310,7 +310,7 @@
by (auto intro!: set_integral_Un set_integrable_subset[OF f])
also have "\<dots> = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
using ae
- by (intro arg_cong2[where f="op+"] set_integral_cong_set)
+ by (intro arg_cong2[where f="(+)"] set_integral_cong_set)
(auto intro!: set_borel_measurable_subset[OF f'])
finally show ?thesis .
qed
--- a/src/HOL/Analysis/Sigma_Algebra.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Sigma_Algebra.thy Wed Jan 10 15:25:09 2018 +0100
@@ -217,7 +217,7 @@
subsubsection \<open>Restricted algebras\<close>
abbreviation (in algebra)
- "restricted_space A \<equiv> (op \<inter> A) ` M"
+ "restricted_space A \<equiv> ((\<inter>) A) ` M"
lemma (in algebra) restricted_algebra:
assumes "A \<in> M" shows "algebra A (restricted_space A)"
@@ -617,11 +617,11 @@
lemma sigma_sets_Int:
assumes "A \<in> sigma_sets sp st" "A \<subseteq> sp"
- shows "op \<inter> A ` sigma_sets sp st = sigma_sets A (op \<inter> A ` st)"
+ shows "(\<inter>) A ` sigma_sets sp st = sigma_sets A ((\<inter>) A ` st)"
proof (intro equalityI subsetI)
- fix x assume "x \<in> op \<inter> A ` sigma_sets sp st"
+ fix x assume "x \<in> (\<inter>) A ` sigma_sets sp st"
then obtain y where "y \<in> sigma_sets sp st" "x = y \<inter> A" by auto
- then have "x \<in> sigma_sets (A \<inter> sp) (op \<inter> A ` st)"
+ then have "x \<in> sigma_sets (A \<inter> sp) ((\<inter>) A ` st)"
proof (induct arbitrary: x)
case (Compl a)
then show ?case
@@ -632,11 +632,11 @@
by (auto intro!: sigma_sets.Union
simp add: UN_extend_simps simp del: UN_simps)
qed (auto intro!: sigma_sets.intros(2-))
- then show "x \<in> sigma_sets A (op \<inter> A ` st)"
+ then show "x \<in> sigma_sets A ((\<inter>) A ` st)"
using \<open>A \<subseteq> sp\<close> by (simp add: Int_absorb2)
next
- fix x assume "x \<in> sigma_sets A (op \<inter> A ` st)"
- then show "x \<in> op \<inter> A ` sigma_sets sp st"
+ fix x assume "x \<in> sigma_sets A ((\<inter>) A ` st)"
+ then show "x \<in> (\<inter>) A ` sigma_sets sp st"
proof induct
case (Compl a)
then obtain x where "a = A \<inter> x" "x \<in> sigma_sets sp st" by auto
@@ -2087,7 +2087,7 @@
subsubsection \<open>Restricted Space Sigma Algebra\<close>
definition restrict_space where
- "restrict_space M \<Omega> = measure_of (\<Omega> \<inter> space M) ((op \<inter> \<Omega>) ` sets M) (emeasure M)"
+ "restrict_space M \<Omega> = measure_of (\<Omega> \<inter> space M) (((\<inter>) \<Omega>) ` sets M) (emeasure M)"
lemma space_restrict_space: "space (restrict_space M \<Omega>) = \<Omega> \<inter> space M"
using sets.sets_into_space unfolding restrict_space_def by (subst space_measure_of) auto
@@ -2095,10 +2095,10 @@
lemma space_restrict_space2: "\<Omega> \<in> sets M \<Longrightarrow> space (restrict_space M \<Omega>) = \<Omega>"
by (simp add: space_restrict_space sets.sets_into_space)
-lemma sets_restrict_space: "sets (restrict_space M \<Omega>) = (op \<inter> \<Omega>) ` sets M"
+lemma sets_restrict_space: "sets (restrict_space M \<Omega>) = ((\<inter>) \<Omega>) ` sets M"
unfolding restrict_space_def
proof (subst sets_measure_of)
- show "op \<inter> \<Omega> ` sets M \<subseteq> Pow (\<Omega> \<inter> space M)"
+ show "(\<inter>) \<Omega> ` sets M \<subseteq> Pow (\<Omega> \<inter> space M)"
by (auto dest: sets.sets_into_space)
have "sigma_sets (\<Omega> \<inter> space M) {((\<lambda>x. x) -` X) \<inter> (\<Omega> \<inter> space M) | X. X \<in> sets M} =
(\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M"
@@ -2106,9 +2106,9 @@
(auto simp add: sets.sigma_sets_eq)
moreover have "{((\<lambda>x. x) -` X) \<inter> (\<Omega> \<inter> space M) | X. X \<in> sets M} = (\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M"
by auto
- moreover have "(\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M = (op \<inter> \<Omega>) ` sets M"
+ moreover have "(\<lambda>X. X \<inter> (\<Omega> \<inter> space M)) ` sets M = ((\<inter>) \<Omega>) ` sets M"
by (intro image_cong) (auto dest: sets.sets_into_space)
- ultimately show "sigma_sets (\<Omega> \<inter> space M) (op \<inter> \<Omega> ` sets M) = op \<inter> \<Omega> ` sets M"
+ ultimately show "sigma_sets (\<Omega> \<inter> space M) ((\<inter>) \<Omega> ` sets M) = (\<inter>) \<Omega> ` sets M"
by simp
qed
--- a/src/HOL/Analysis/Starlike.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Analysis/Starlike.thy Wed Jan 10 15:25:09 2018 +0100
@@ -1277,13 +1277,13 @@
using as(3)
unfolding substdbasis_expansion_unique[OF assms]
by auto
- then have **: "sum u ?D = sum (op \<bullet> x) ?D"
+ then have **: "sum u ?D = sum ((\<bullet>) x) ?D"
apply -
apply (rule sum.cong)
using assms
apply auto
done
- have "(\<forall>i\<in>Basis. 0 \<le> x\<bullet>i) \<and> sum (op \<bullet> x) ?D \<le> 1"
+ have "(\<forall>i\<in>Basis. 0 \<le> x\<bullet>i) \<and> sum ((\<bullet>) x) ?D \<le> 1"
proof (rule,rule)
fix i :: 'a
assume i: "i \<in> Basis"
@@ -1296,11 +1296,11 @@
using \<open>(\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0)\<close>[rule_format, OF i] by auto
ultimately show "0 \<le> x\<bullet>i" by auto
qed (insert as(2)[unfolded **], auto)
- then show "(\<forall>i\<in>Basis. 0 \<le> x\<bullet>i) \<and> sum (op \<bullet> x) ?D \<le> 1 \<and> (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0)"
+ then show "(\<forall>i\<in>Basis. 0 \<le> x\<bullet>i) \<and> sum ((\<bullet>) x) ?D \<le> 1 \<and> (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0)"
using \<open>(\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0)\<close> by auto
next
fix x :: "'a::euclidean_space"
- assume as: "\<forall>i\<in>Basis. 0 \<le> x \<bullet> i" "sum (op \<bullet> x) ?D \<le> 1" "(\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0)"
+ assume as: "\<forall>i\<in>Basis. 0 \<le> x \<bullet> i" "sum ((\<bullet>) x) ?D \<le> 1" "(\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0)"
show "\<exists>u. (\<forall>x\<in>?D. 0 \<le> u x) \<and> sum u ?D \<le> 1 \<and> (\<Sum>x\<in>?D. u x *\<^sub>R x) = x"
using as d
unfolding substdbasis_expansion_unique[OF assms]
@@ -1329,8 +1329,8 @@
proof -
fix x :: 'a
fix e
- assume "e > 0" and as: "\<forall>xa. dist x xa < e \<longrightarrow> (\<forall>x\<in>Basis. 0 \<le> xa \<bullet> x) \<and> sum (op \<bullet> xa) Basis \<le> 1"
- show "(\<forall>xa\<in>Basis. 0 < x \<bullet> xa) \<and> sum (op \<bullet> x) Basis < 1"
+ assume "e > 0" and as: "\<forall>xa. dist x xa < e \<longrightarrow> (\<forall>x\<in>Basis. 0 \<le> xa \<bullet> x) \<and> sum ((\<bullet>) xa) Basis \<le> 1"
+ show "(\<forall>xa\<in>Basis. 0 < x \<bullet> xa) \<and> sum ((\<bullet>) x) Basis < 1"
apply safe
proof -
fix i :: 'a
@@ -1346,12 +1346,12 @@
have "\<And>i. i \<in> Basis \<Longrightarrow> (x + (e / 2) *\<^sub>R (SOME i. i\<in>Basis)) \<bullet> i =
x\<bullet>i + (if i = (SOME i. i\<in>Basis) then e/2 else 0)"
by (auto simp: SOME_Basis inner_Basis inner_simps)
- then have *: "sum (op \<bullet> (x + (e / 2) *\<^sub>R (SOME i. i\<in>Basis))) Basis =
+ then have *: "sum ((\<bullet>) (x + (e / 2) *\<^sub>R (SOME i. i\<in>Basis))) Basis =
sum (\<lambda>i. x\<bullet>i + (if (SOME i. i\<in>Basis) = i then e/2 else 0)) Basis"
apply (rule_tac sum.cong)
apply auto
done
- have "sum (op \<bullet> x) Basis < sum (op \<bullet> (x + (e / 2) *\<^sub>R (SOME i. i\<in>Basis))) Basis"
+ have "sum ((\<bullet>) x) Basis < sum ((\<bullet>) (x + (e / 2) *\<^sub>R (SOME i. i\<in>Basis))) Basis"
unfolding * sum.distrib
using \<open>e > 0\<close> DIM_positive[where 'a='a]
apply (subst sum.delta')
@@ -1362,18 +1362,18 @@
apply (drule_tac as[rule_format])
apply auto
done
- finally show "sum (op \<bullet> x) Basis < 1" by auto
+ finally show "sum ((\<bullet>) x) Basis < 1" by auto
qed
next
fix x :: 'a
- assume as: "\<forall>i\<in>Basis. 0 < x \<bullet> i" "sum (op \<bullet> x) Basis < 1"
+ assume as: "\<forall>i\<in>Basis. 0 < x \<bullet> i" "sum ((\<bullet>) x) Basis < 1"
obtain a :: 'b where "a \<in> UNIV" using UNIV_witness ..
- let ?d = "(1 - sum (op \<bullet> x) Basis) / real (DIM('a))"
- show "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> (\<forall>i\<in>Basis. 0 \<le> y \<bullet> i) \<and> sum (op \<bullet> y) Basis \<le> 1"
- proof (rule_tac x="min (Min ((op \<bullet> x) ` Basis)) D" for D in exI, intro conjI impI allI)
+ let ?d = "(1 - sum ((\<bullet>) x) Basis) / real (DIM('a))"
+ show "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> (\<forall>i\<in>Basis. 0 \<le> y \<bullet> i) \<and> sum ((\<bullet>) y) Basis \<le> 1"
+ proof (rule_tac x="min (Min (((\<bullet>) x) ` Basis)) D" for D in exI, intro conjI impI allI)
fix y
- assume y: "dist x y < min (Min (op \<bullet> x ` Basis)) ?d"
- have "sum (op \<bullet> y) Basis \<le> sum (\<lambda>i. x\<bullet>i + ?d) Basis"
+ assume y: "dist x y < min (Min ((\<bullet>) x ` Basis)) ?d"
+ have "sum ((\<bullet>) y) Basis \<le> sum (\<lambda>i. x\<bullet>i + ?d) Basis"
proof (rule sum_mono)
fix i :: 'a
assume i: "i \<in> Basis"
@@ -1389,7 +1389,7 @@
also have "\<dots> \<le> 1"
unfolding sum.distrib sum_constant
by (auto simp add: Suc_le_eq)
- finally show "sum (op \<bullet> y) Basis \<le> 1" .
+ finally show "sum ((\<bullet>) y) Basis \<le> 1" .
show "(\<forall>i\<in>Basis. 0 \<le> y \<bullet> i)"
proof safe
fix i :: 'a
@@ -1405,11 +1405,11 @@
by (auto simp: inner_simps)
qed
next
- have "Min ((op \<bullet> x) ` Basis) > 0"
+ have "Min (((\<bullet>) x) ` Basis) > 0"
using as by simp
moreover have "?d > 0"
using as by (auto simp: Suc_le_eq)
- ultimately show "0 < min (Min (op \<bullet> x ` Basis)) ((1 - sum (op \<bullet> x) Basis) / real DIM('a))"
+ ultimately show "0 < min (Min ((\<bullet>) x ` Basis)) ((1 - sum ((\<bullet>) x) Basis) / real DIM('a))"
by linarith
qed
qed
@@ -1436,7 +1436,7 @@
show "0 < ?a \<bullet> i"
unfolding **[OF i] by (auto simp add: Suc_le_eq DIM_positive)
next
- have "sum (op \<bullet> ?a) ?D = sum (\<lambda>i. inverse (2 * real DIM('a))) ?D"
+ have "sum ((\<bullet>) ?a) ?D = sum (\<lambda>i. inverse (2 * real DIM('a))) ?D"
apply (rule sum.cong)
apply rule
apply auto
@@ -1444,7 +1444,7 @@
also have "\<dots> < 1"
unfolding sum_constant divide_inverse[symmetric]
by (auto simp add: field_simps)
- finally show "sum (op \<bullet> ?a) ?D < 1" by auto
+ finally show "sum ((\<bullet>) ?a) ?D < 1" by auto
qed
qed
@@ -1478,11 +1478,11 @@
"ball x e \<inter> {xa. (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> xa\<bullet>i = 0)} \<subseteq> convex hull (insert 0 ?p)"
using mem_rel_interior_ball[of x "convex hull (insert 0 ?p)"] h0 by auto
then have as: "\<forall>xa. dist x xa < e \<and> (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> xa\<bullet>i = 0) \<longrightarrow>
- (\<forall>i\<in>d. 0 \<le> xa \<bullet> i) \<and> sum (op \<bullet> xa) d \<le> 1"
+ (\<forall>i\<in>d. 0 \<le> xa \<bullet> i) \<and> sum ((\<bullet>) xa) d \<le> 1"
unfolding ball_def unfolding substd_simplex[OF assms] using assms by auto
have x0: "(\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0)"
using x rel_interior_subset substd_simplex[OF assms] by auto
- have "(\<forall>i\<in>d. 0 < x \<bullet> i) \<and> sum (op \<bullet> x) d < 1 \<and> (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0)"
+ have "(\<forall>i\<in>d. 0 < x \<bullet> i) \<and> sum ((\<bullet>) x) d < 1 \<and> (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0)"
apply rule
apply rule
proof -
@@ -1509,14 +1509,14 @@
by auto
have "\<And>i. i \<in> Basis \<Longrightarrow> (x + (e / 2) *\<^sub>R a) \<bullet> i = x\<bullet>i + (if i = a then e/2 else 0)"
using a d by (auto simp: inner_simps inner_Basis)
- then have *: "sum (op \<bullet> (x + (e / 2) *\<^sub>R a)) d =
+ then have *: "sum ((\<bullet>) (x + (e / 2) *\<^sub>R a)) d =
sum (\<lambda>i. x\<bullet>i + (if a = i then e/2 else 0)) d"
using d by (intro sum.cong) auto
have "a \<in> Basis"
using \<open>a \<in> d\<close> d by auto
then have h1: "(\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> (x + (e / 2) *\<^sub>R a) \<bullet> i = 0)"
using x0 d \<open>a\<in>d\<close> by (auto simp add: inner_add_left inner_Basis)
- have "sum (op \<bullet> x) d < sum (op \<bullet> (x + (e / 2) *\<^sub>R a)) d"
+ have "sum ((\<bullet>) x) d < sum ((\<bullet>) (x + (e / 2) *\<^sub>R a)) d"
unfolding * sum.distrib
using \<open>e > 0\<close> \<open>a \<in> d\<close>
using \<open>finite d\<close>
@@ -1524,7 +1524,7 @@
also have "\<dots> \<le> 1"
using ** h1 as[rule_format, of "x + (e / 2) *\<^sub>R a"]
by auto
- finally show "sum (op \<bullet> x) d < 1 \<and> (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0)"
+ finally show "sum ((\<bullet>) x) d < 1 \<and> (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0)"
using x0 by auto
qed
}
@@ -1543,28 +1543,28 @@
unfolding substd_simplex[OF assms] by fastforce
obtain a where a: "a \<in> d"
using \<open>d \<noteq> {}\<close> by auto
- let ?d = "(1 - sum (op \<bullet> x) d) / real (card d)"
+ let ?d = "(1 - sum ((\<bullet>) x) d) / real (card d)"
have "0 < card d" using \<open>d \<noteq> {}\<close> \<open>finite d\<close>
by (simp add: card_gt_0_iff)
- have "Min ((op \<bullet> x) ` d) > 0"
+ have "Min (((\<bullet>) x) ` d) > 0"
using as \<open>d \<noteq> {}\<close> \<open>finite d\<close> by (simp add: Min_gr_iff)
moreover have "?d > 0" using as using \<open>0 < card d\<close> by auto
- ultimately have h3: "min (Min ((op \<bullet> x) ` d)) ?d > 0"
+ ultimately have h3: "min (Min (((\<bullet>) x) ` d)) ?d > 0"
by auto
have "x \<in> rel_interior (convex hull (insert 0 ?p))"
unfolding rel_interior_ball mem_Collect_eq h0
apply (rule,rule h2)
unfolding substd_simplex[OF assms]
- apply (rule_tac x="min (Min ((op \<bullet> x) ` d)) ?d" in exI)
+ apply (rule_tac x="min (Min (((\<bullet>) x) ` d)) ?d" in exI)
apply (rule, rule h3)
apply safe
unfolding mem_ball
proof -
fix y :: 'a
- assume y: "dist x y < min (Min (op \<bullet> x ` d)) ?d"
+ assume y: "dist x y < min (Min ((\<bullet>) x ` d)) ?d"
assume y2: "\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> y\<bullet>i = 0"
- have "sum (op \<bullet> y) d \<le> sum (\<lambda>i. x\<bullet>i + ?d) d"
+ have "sum ((\<bullet>) y) d \<le> sum (\<lambda>i. x\<bullet>i + ?d) d"
proof (rule sum_mono)
fix i
assume "i \<in> d"
@@ -1581,7 +1581,7 @@
also have "\<dots> \<le> 1"
unfolding sum.distrib sum_constant using \<open>0 < card d\<close>
by auto
- finally show "sum (op \<bullet> y) d \<le> 1" .
+ finally show "sum ((\<bullet>) y) d \<le> 1" .
fix i :: 'a
assume i: "i \<in> Basis"
@@ -1590,7 +1590,7 @@
case True
have "norm (x - y) < x\<bullet>i"
using y[unfolded min_less_iff_conj dist_norm, THEN conjunct1]
- using Min_gr_iff[of "op \<bullet> x ` d" "norm (x - y)"] \<open>0 < card d\<close> \<open>i:d\<close>
+ using Min_gr_iff[of "(\<bullet>) x ` d" "norm (x - y)"] \<open>0 < card d\<close> \<open>i:d\<close>
by (simp add: card_gt_0_iff)
then show "0 \<le> y\<bullet>i"
using Basis_le_norm[OF i, of "x - y"] and as(1)[rule_format]
@@ -1600,7 +1600,7 @@
}
ultimately have
"\<And>x. x \<in> rel_interior (convex hull insert 0 d) \<longleftrightarrow>
- x \<in> {x. (\<forall>i\<in>d. 0 < x \<bullet> i) \<and> sum (op \<bullet> x) d < 1 \<and> (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0)}"
+ x \<in> {x. (\<forall>i\<in>d. 0 < x \<bullet> i) \<and> sum ((\<bullet>) x) d < 1 \<and> (\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0)}"
by blast
then show ?thesis by (rule set_eqI)
qed
@@ -1645,12 +1645,12 @@
by auto
finally show "0 < ?a \<bullet> i" by auto
next
- have "sum (op \<bullet> ?a) ?D = sum (\<lambda>i. inverse (2 * real (card d))) ?D"
+ have "sum ((\<bullet>) ?a) ?D = sum (\<lambda>i. inverse (2 * real (card d))) ?D"
by (rule sum.cong) (rule refl, rule **)
also have "\<dots> < 1"
unfolding sum_constant divide_real_def[symmetric]
by (auto simp add: field_simps)
- finally show "sum (op \<bullet> ?a) ?D < 1" by auto
+ finally show "sum ((\<bullet>) ?a) ?D < 1" by auto
next
fix i
assume "i \<in> Basis" and "i \<notin> d"
@@ -1748,10 +1748,10 @@
{
assume "S \<noteq> {}"
then obtain a where "a \<in> S" by auto
- then have "0 \<in> op + (-a) ` S"
+ then have "0 \<in> (+) (-a) ` S"
using assms exI[of "(\<lambda>x. x \<in> S \<and> - a + x = 0)" a] by auto
- then have "rel_interior (op + (-a) ` S) \<noteq> {}"
- using rel_interior_convex_nonempty_aux[of "op + (-a) ` S"]
+ then have "rel_interior ((+) (-a) ` S) \<noteq> {}"
+ using rel_interior_convex_nonempty_aux[of "(+) (-a) ` S"]
convex_translation[of S "-a"] assms
by auto
then have "rel_interior S \<noteq> {}"
@@ -2958,22 +2958,22 @@
lemma rel_interior_scaleR:
fixes S :: "'n::euclidean_space set"
assumes "c \<noteq> 0"
- shows "(op *\<^sub>R c) ` (rel_interior S) = rel_interior ((op *\<^sub>R c) ` S)"
- using rel_interior_injective_linear_image[of "(op *\<^sub>R c)" S]
- linear_conv_bounded_linear[of "op *\<^sub>R c"] linear_scaleR injective_scaleR[of c] assms
+ shows "(( *\<^sub>R) c) ` (rel_interior S) = rel_interior ((( *\<^sub>R) c) ` S)"
+ using rel_interior_injective_linear_image[of "(( *\<^sub>R) c)" S]
+ linear_conv_bounded_linear[of "( *\<^sub>R) c"] linear_scaleR injective_scaleR[of c] assms
by auto
lemma rel_interior_convex_scaleR:
fixes S :: "'n::euclidean_space set"
assumes "convex S"
- shows "(op *\<^sub>R c) ` (rel_interior S) = rel_interior ((op *\<^sub>R c) ` S)"
+ shows "(( *\<^sub>R) c) ` (rel_interior S) = rel_interior ((( *\<^sub>R) c) ` S)"
by (metis assms linear_scaleR rel_interior_convex_linear_image)
lemma convex_rel_open_scaleR:
fixes S :: "'n::euclidean_space set"
assumes "convex S"
and "rel_open S"
- shows "convex ((op *\<^sub>R c) ` S) \<and> rel_open ((op *\<^sub>R c) ` S)"
+ shows "convex ((( *\<^sub>R) c) ` S) \<and> rel_open ((( *\<^sub>R) c) ` S)"
by (metis assms convex_scaling rel_interior_convex_scaleR rel_open_def)
lemma convex_rel_open_finite_inter:
@@ -3142,10 +3142,10 @@
by (simp add: rel_interior_empty cone_0)
next
case False
- then have *: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> op *\<^sub>R c ` S = S)"
+ then have *: "0 \<in> S \<and> (\<forall>c. c > 0 \<longrightarrow> ( *\<^sub>R) c ` S = S)"
using cone_iff[of S] assms by auto
then have *: "0 \<in> ({0} \<union> rel_interior S)"
- and "\<forall>c. c > 0 \<longrightarrow> op *\<^sub>R c ` ({0} \<union> rel_interior S) = ({0} \<union> rel_interior S)"
+ and "\<forall>c. c > 0 \<longrightarrow> ( *\<^sub>R) c ` ({0} \<union> rel_interior S) = ({0} \<union> rel_interior S)"
by (auto simp add: rel_interior_scaleR)
then show ?thesis
using cone_iff[of "{0} \<union> rel_interior S"] by auto
@@ -3155,7 +3155,7 @@
fixes S :: "'m::euclidean_space set"
assumes "convex S"
shows "(c, x) \<in> rel_interior (cone hull ({(1 :: real)} \<times> S)) \<longleftrightarrow>
- c > 0 \<and> x \<in> ((op *\<^sub>R c) ` (rel_interior S))"
+ c > 0 \<and> x \<in> ((( *\<^sub>R) c) ` (rel_interior S))"
proof (cases "S = {}")
case True
then show ?thesis
@@ -3188,9 +3188,9 @@
{
fix c :: real
assume "c > 0"
- then have "f c = (op *\<^sub>R c ` S)"
+ then have "f c = (( *\<^sub>R) c ` S)"
using f_def cone_hull_expl[of "{1 :: real} \<times> S"] by auto
- then have "rel_interior (f c) = op *\<^sub>R c ` rel_interior S"
+ then have "rel_interior (f c) = ( *\<^sub>R) c ` rel_interior S"
using rel_interior_convex_scaleR[of S c] assms by auto
}
then show ?thesis using * ** by auto
@@ -5154,9 +5154,9 @@
let ?\<C> = "insert (U \<union> V) ((\<lambda>S. N - S) ` \<F>)"
obtain \<D> where "\<D> \<subseteq> ?\<C>" "finite \<D>" "K \<subseteq> \<Union>\<D>"
proof (rule compactE [OF \<open>compact K\<close>])
- show "K \<subseteq> \<Union>insert (U \<union> V) (op - N ` \<F>)"
+ show "K \<subseteq> \<Union>insert (U \<union> V) ((-) N ` \<F>)"
using \<open>K \<subseteq> N\<close> ABeq \<open>A \<subseteq> U\<close> \<open>B \<subseteq> V\<close> by auto
- show "\<And>B. B \<in> insert (U \<union> V) (op - N ` \<F>) \<Longrightarrow> open B"
+ show "\<And>B. B \<in> insert (U \<union> V) ((-) N ` \<F>) \<Longrightarrow> open B"
by (auto simp: \<open>open U\<close> \<open>open V\<close> open_Un \<open>open N\<close> cc compact_imp_closed open_Diff)
qed
then have "finite(\<D> - {U \<union> V})"
@@ -5195,7 +5195,7 @@
by auto
next
assume "N - X \<subseteq> N - J"
- with J have "N - X \<union> UNION \<H> (op - N) \<subseteq> N - J"
+ with J have "N - X \<union> UNION \<H> ((-) N) \<subseteq> N - J"
by auto
with \<open>J \<in> \<H>\<close> show ?thesis
by blast
@@ -5234,9 +5234,9 @@
using X by blast
moreover have "connected (\<Inter>T\<in>\<F>. X \<inter> T)"
proof (rule connected_chain)
- show "\<And>T. T \<in> op \<inter> X ` \<F> \<Longrightarrow> compact T \<and> connected T"
+ show "\<And>T. T \<in> (\<inter>) X ` \<F> \<Longrightarrow> compact T \<and> connected T"
using cc X by auto (metis inf.absorb2 inf.orderE local.linear)
- show "\<And>S T. S \<in> op \<inter> X ` \<F> \<and> T \<in> op \<inter> X ` \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
+ show "\<And>S T. S \<in> (\<inter>) X ` \<F> \<and> T \<in> (\<inter>) X ` \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
using local.linear by blast
qed
ultimately show ?thesis
@@ -5599,7 +5599,7 @@
using assms interior_subset by blast
then obtain e where "e > 0" and e: "cball a e \<subseteq> T"
using mem_interior_cball by blast
- have *: "x \<in> op + a ` span ((\<lambda>x. x - a) ` (S \<inter> T))" if "x \<in> S" for x
+ have *: "x \<in> (+) a ` span ((\<lambda>x. x - a) ` (S \<inter> T))" if "x \<in> S" for x
proof (cases "x = a")
case True with that span_0 eq_add_iff image_def mem_Collect_eq show ?thesis
by blast
@@ -5870,19 +5870,19 @@
done
next