--- a/src/Doc/Datatypes/Datatypes.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Thu Jul 03 14:40:36 2014 +0200
@@ -877,6 +877,10 @@
@{thm list.rel_inject(1)[no_vars]} \\
@{thm list.rel_inject(2)[no_vars]}
+\item[@{text "t."}\hthm{rel\_intros}\rm:] ~ \\
+@{thm list.rel_intros(1)[no_vars]} \\
+@{thm list.rel_intros(2)[no_vars]}
+
\item[@{text "t."}\hthm{rel\_distinct} @{text "[simp]"}\rm:] ~ \\
@{thm list.rel_distinct(1)[no_vars]} \\
@{thm list.rel_distinct(2)[no_vars]}
--- a/src/Doc/Implementation/Integration.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/Doc/Implementation/Integration.thy Thu Jul 03 14:40:36 2014 +0200
@@ -13,9 +13,9 @@
is transformed by a sequence of transitions (commands) within a theory body.
This is a pure value with pure functions acting on it in a timeless and
stateless manner. Historically, the sequence of transitions was wrapped up
- as sequential command loop, such that commands are applied sequentially
- one-by-one. In contemporary Isabelle/Isar, processing toplevel commands
- usually works in parallel in multi-threaded Isabelle/ML.
+ as sequential command loop, such that commands are applied one-by-one. In
+ contemporary Isabelle/Isar, processing toplevel commands usually works in
+ parallel in multi-threaded Isabelle/ML \cite{Wenzel:2009,Wenzel:2013:ITP}.
*}
@@ -28,10 +28,10 @@
commands such as @{command definition}, or state a @{command theorem} to be
proven. A proof state accepts a rich collection of Isar proof commands for
structured proof composition, or unstructured proof scripts. When the proof
- is concluded we get back to the theory, which is then updated by defining
- the resulting fact. Further theory declarations or theorem statements with
- proofs may follow, until we eventually conclude the theory development by
- issuing @{command end} to get back to the empty toplevel.
+ is concluded we get back to the (local) theory, which is then updated by
+ defining the resulting fact. Further theory declarations or theorem
+ statements with proofs may follow, until we eventually conclude the theory
+ development by issuing @{command end} to get back to the empty toplevel.
*}
text %mlref {*
@@ -41,8 +41,6 @@
@{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\
@{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\
@{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\
- @{index_ML Toplevel.timing: "bool Unsynchronized.ref"} \\
- @{index_ML Toplevel.profiling: "int Unsynchronized.ref"} \\
\end{mldecls}
\begin{description}
@@ -59,19 +57,11 @@
toplevel state.
\item @{ML Toplevel.theory_of}~@{text "state"} selects the
- background theory of @{text "state"}, raises @{ML Toplevel.UNDEF}
+ background theory of @{text "state"}, it raises @{ML Toplevel.UNDEF}
for an empty toplevel state.
\item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
- state if available, otherwise raises @{ML Toplevel.UNDEF}.
-
- \item @{ML "Toplevel.timing := true"} makes the toplevel print timing
- information for each Isar command being executed.
-
- \item @{ML Toplevel.profiling}~@{ML_text ":="}~@{text "n"} controls
- low-level profiling of the underlying ML runtime system. For
- Poly/ML, @{text "n = 1"} means time and @{text "n = 2"} space
- profiling.
+ state if available, otherwise it raises @{ML Toplevel.UNDEF}.
\end{description}
*}
@@ -104,15 +94,14 @@
list of partial functions, which are tried in turn until the first
one succeeds. This acts like an outer case-expression for various
alternative state transitions. For example, \isakeyword{qed} works
- differently for a local proofs vs.\ the global ending of the main
+ differently for a local proofs vs.\ the global ending of an outermost
proof.
- Toplevel transitions are composed via transition transformers.
- Internally, Isar commands are put together from an empty transition
- extended by name and source position. It is then left to the
- individual command parser to turn the given concrete syntax into a
- suitable transition transformer that adjoins actual operations on a
- theory or proof state etc.
+ Transitions are composed via transition transformers. Internally, Isar
+ commands are put together from an empty transition extended by name and
+ source position. It is then left to the individual command parser to turn
+ the given concrete syntax into a suitable transition transformer that
+ adjoins actual operations on a theory or proof state.
*}
text %mlref {*
@@ -154,8 +143,8 @@
list).
\item @{ML Toplevel.end_proof}~@{text "tr"} adjoins a concluding
- proof command, that returns the resulting theory, after storing the
- resulting facts in the context etc.
+ proof command, that returns the resulting theory, after applying the
+ resulting facts to the target context.
\end{description}
*}
@@ -175,7 +164,7 @@
text %mlref {*
\begin{mldecls}
@{index_ML use_thy: "string -> unit"} \\
- @{index_ML use_thys: "string list -> unit"} \\
+ @{index_ML use_thys: "string list -> unit"} \\[0.5ex]
@{index_ML Thy_Info.get_theory: "string -> theory"} \\
@{index_ML Thy_Info.remove_thy: "string -> unit"} \\
@{index_ML Thy_Info.register_thy: "theory -> unit"} \\
@@ -184,8 +173,8 @@
\begin{description}
\item @{ML use_thy}~@{text A} ensures that theory @{text A} is fully
- up-to-date wrt.\ the external file store, reloading outdated ancestors as
- required.
+ up-to-date wrt.\ the external file store; outdated ancestors are reloaded on
+ demand.
\item @{ML use_thys} is similar to @{ML use_thy}, but handles several
theories simultaneously. Thus it acts like processing the import header of a
@@ -193,6 +182,8 @@
sub-graph of theories, the intrinsic parallelism can be exploited by the
system to speedup loading.
+ This variant is used by default in @{tool build} \cite{isabelle-sys}.
+
\item @{ML Thy_Info.get_theory}~@{text A} retrieves the theory value
presently associated with name @{text A}. Note that the result might be
outdated wrt.\ the file-system content.
@@ -202,7 +193,7 @@
\item @{ML Thy_Info.register_thy}~@{text "text thy"} registers an existing
theory value with the theory loader database and updates source version
- information according to the current file-system state.
+ information according to the file store.
\end{description}
*}
--- a/src/Doc/Implementation/Syntax.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/Doc/Implementation/Syntax.thy Thu Jul 03 14:40:36 2014 +0200
@@ -12,18 +12,18 @@
additional means for reading and printing of terms and types. This
important add-on outside the logical core is called \emph{inner
syntax} in Isabelle jargon, as opposed to the \emph{outer syntax} of
- the theory and proof language (cf.\ \cite{isabelle-isar-ref}).
+ the theory and proof language \cite{isabelle-isar-ref}.
- For example, according to \cite{church40} quantifiers are
- represented as higher-order constants @{text "All :: ('a \<Rightarrow> bool) \<Rightarrow>
- bool"} such that @{text "All (\<lambda>x::'a. B x)"} faithfully represents
- the idea that is displayed as @{text "\<forall>x::'a. B x"} via @{keyword
- "binder"} notation. Moreover, type-inference in the style of
- Hindley-Milner \cite{hindleymilner} (and extensions) enables users
- to write @{text "\<forall>x. B x"} concisely, when the type @{text "'a"} is
- already clear from the context.\footnote{Type-inference taken to the
- extreme can easily confuse users, though. Beginners often stumble
- over unexpectedly general types inferred by the system.}
+ For example, according to \cite{church40} quantifiers are represented as
+ higher-order constants @{text "All :: ('a \<Rightarrow> bool) \<Rightarrow> bool"} such that @{text
+ "All (\<lambda>x::'a. B x)"} faithfully represents the idea that is displayed in
+ Isabelle as @{text "\<forall>x::'a. B x"} via @{keyword "binder"} notation.
+ Moreover, type-inference in the style of Hindley-Milner \cite{hindleymilner}
+ (and extensions) enables users to write @{text "\<forall>x. B x"} concisely, when
+ the type @{text "'a"} is already clear from the
+ context.\footnote{Type-inference taken to the extreme can easily confuse
+ users. Beginners often stumble over unexpectedly general types inferred by
+ the system.}
\medskip The main inner syntax operations are \emph{read} for
parsing together with type-checking, and \emph{pretty} for formatted
@@ -43,18 +43,17 @@
\end{itemize}
- Some specification package might thus intercept syntax processing at
- a well-defined stage after @{text "parse"}, to a augment the
- resulting pre-term before full type-reconstruction is performed by
- @{text "check"}, for example. Note that the formal status of bound
- variables, versus free variables, versus constants must not be
- changed between these phases!
+ For example, some specification package might thus intercept syntax
+ processing at a well-defined stage after @{text "parse"}, to a augment the
+ resulting pre-term before full type-reconstruction is performed by @{text
+ "check"}. Note that the formal status of bound variables, versus free
+ variables, versus constants must not be changed between these phases.
\medskip In general, @{text check} and @{text uncheck} operate
simultaneously on a list of terms. This is particular important for
type-checking, to reconstruct types for several terms of the same context
and scope. In contrast, @{text parse} and @{text unparse} operate separately
- in single terms.
+ on single terms.
There are analogous operations to read and print types, with the same
sub-division into phases.
@@ -63,14 +62,15 @@
section {* Reading and pretty printing \label{sec:read-print} *}
-text {* Read and print operations are roughly dual to each other, such
- that for the user @{text "s' = pretty (read s)"} looks similar to
- the original source text @{text "s"}, but the details depend on many
- side-conditions. There are also explicit options to control
- suppressing of type information in the output. The default
- configuration routinely looses information, so @{text "t' = read
- (pretty t)"} might fail, or produce a differently typed term, or a
- completely different term in the face of syntactic overloading! *}
+text {*
+ Read and print operations are roughly dual to each other, such that for the
+ user @{text "s' = pretty (read s)"} looks similar to the original source
+ text @{text "s"}, but the details depend on many side-conditions. There are
+ also explicit options to control the removal of type information in the
+ output. The default configuration routinely looses information, so @{text
+ "t' = read (pretty t)"} might fail, or produce a differently typed term, or
+ a completely different term in the face of syntactic overloading.
+*}
text %mlref {*
\begin{mldecls}
@@ -98,26 +98,27 @@
If particular type-constraints are required for some of the arguments, the
read operations needs to be split into its parse and check phases. Then it
- is possible to use @{ML Type.constraint} on the intermediate pre-terms.
+ is possible to use @{ML Type.constraint} on the intermediate pre-terms
+ \secref{sec:term-check}.
\item @{ML Syntax.read_props}~@{text "ctxt strs"} parses and checks a
simultaneous list of source strings as terms of the logic, with an implicit
type-constraint for each argument to enforce type @{typ prop}; this also
- affects the inner syntax for parsing. The remaining type-reconstructions
- works as for @{ML Syntax.read_terms} above.
+ affects the inner syntax for parsing. The remaining type-reconstruction
+ works as for @{ML Syntax.read_terms}.
\item @{ML Syntax.read_typ}, @{ML Syntax.read_term}, @{ML Syntax.read_prop}
- are like the simultaneous versions above, but operate on a single argument
- only. This convenient shorthand is adequate in situations where a single
- item in its own scope is processed. Do not use @{ML "map o
- Syntax.read_term"} where @{ML Syntax.read_terms} is actually intended!
+ are like the simultaneous versions, but operate on a single argument only.
+ This convenient shorthand is adequate in situations where a single item in
+ its own scope is processed. Do not use @{ML "map o Syntax.read_term"} where
+ @{ML Syntax.read_terms} is actually intended!
\item @{ML Syntax.pretty_typ}~@{text "ctxt T"} and @{ML
Syntax.pretty_term}~@{text "ctxt t"} uncheck and pretty-print the given type
or term, respectively. Although the uncheck phase acts on a simultaneous
- list as well, this is rarely relevant in practice, so only the singleton
- case is provided as combined pretty operation. There is no distinction of
- term vs.\ proposition.
+ list as well, this is rarely used in practice, so only the singleton case is
+ provided as combined pretty operation. There is no distinction of term vs.\
+ proposition.
\item @{ML Syntax.string_of_typ} and @{ML Syntax.string_of_term} are
convenient compositions of @{ML Syntax.pretty_typ} and @{ML
@@ -130,11 +131,11 @@
@{ML Syntax.read_term}, @{ML Syntax.read_prop}, and @{ML
Syntax.string_of_term} are the most important operations in practice.
- \medskip Note that the string values that are passed in and out here are
+ \medskip Note that the string values that are passed in and out are
annotated by the system, to carry further markup that is relevant for the
Prover IDE \cite{isabelle-jedit}. User code should neither compose its own
input strings, nor try to analyze the output strings. Conceptually this is
- an abstract datatype, encoded into a concrete string for historical reasons.
+ an abstract datatype, encoded as concrete string for historical reasons.
The standard way to provide the required position markup for input works via
the outer syntax parser wrapper @{ML Parse.inner_syntax}, which is already
@@ -147,47 +148,46 @@
section {* Parsing and unparsing \label{sec:parse-unparse} *}
-text {* Parsing and unparsing converts between actual source text and
- a certain \emph{pre-term} format, where all bindings and scopes are
- resolved faithfully. Thus the names of free variables or constants
- are already determined in the sense of the logical context, but type
- information might be still missing. Pre-terms support an explicit
- language of \emph{type constraints} that may be augmented by user
- code to guide the later \emph{check} phase.
+text {*
+ Parsing and unparsing converts between actual source text and a certain
+ \emph{pre-term} format, where all bindings and scopes are already resolved
+ faithfully. Thus the names of free variables or constants are determined in
+ the sense of the logical context, but type information might be still
+ missing. Pre-terms support an explicit language of \emph{type constraints}
+ that may be augmented by user code to guide the later \emph{check} phase.
- Actual parsing is based on traditional lexical analysis and Earley
- parsing for arbitrary context-free grammars. The user can specify
- the grammar via mixfix annotations. Moreover, there are \emph{syntax
- translations} that can be augmented by the user, either
- declaratively via @{command translations} or programmatically via
- @{command parse_translation}, @{command print_translation} etc. The
- final scope-resolution is performed by the system, according to name
- spaces for types, term variables and constants etc.\ determined by
- the context.
+ Actual parsing is based on traditional lexical analysis and Earley parsing
+ for arbitrary context-free grammars. The user can specify the grammar
+ declaratively via mixfix annotations. Moreover, there are \emph{syntax
+ translations} that can be augmented by the user, either declaratively via
+ @{command translations} or programmatically via @{command
+ parse_translation}, @{command print_translation} \cite{isabelle-isar-ref}.
+ The final scope-resolution is performed by the system, according to name
+ spaces for types, term variables and constants determined by the context.
*}
text %mlref {*
\begin{mldecls}
@{index_ML Syntax.parse_typ: "Proof.context -> string -> typ"} \\
@{index_ML Syntax.parse_term: "Proof.context -> string -> term"} \\
- @{index_ML Syntax.parse_prop: "Proof.context -> string -> term"} \\
+ @{index_ML Syntax.parse_prop: "Proof.context -> string -> term"} \\[0.5ex]
@{index_ML Syntax.unparse_typ: "Proof.context -> typ -> Pretty.T"} \\
@{index_ML Syntax.unparse_term: "Proof.context -> term -> Pretty.T"} \\
\end{mldecls}
\begin{description}
- \item @{ML Syntax.parse_typ}~@{text "ctxt str"} parses a source strings as
+ \item @{ML Syntax.parse_typ}~@{text "ctxt str"} parses a source string as
pre-type that is ready to be used with subsequent check operations.
- \item @{ML Syntax.parse_term}~@{text "ctxt str"} parses a source strings as
+ \item @{ML Syntax.parse_term}~@{text "ctxt str"} parses a source string as
pre-term that is ready to be used with subsequent check operations.
- \item @{ML Syntax.parse_prop}~@{text "ctxt str"} parses a source strings as
+ \item @{ML Syntax.parse_prop}~@{text "ctxt str"} parses a source string as
pre-term that is ready to be used with subsequent check operations. The
inner syntax category is @{typ prop} and a suitable type-constraint is
- included to ensure that this information is preserved during the check
- phase.
+ included to ensure that this information is observed in subsequent type
+ reconstruction.
\item @{ML Syntax.unparse_typ}~@{text "ctxt T"} unparses a type after
uncheck operations, to turn it into a pretty tree.
@@ -198,8 +198,8 @@
\end{description}
- These operations always operate on single items; use the combinator @{ML
- map} to apply them to a list of items.
+ These operations always operate on a single item; use the combinator @{ML
+ map} to apply them to a list.
*}
@@ -216,14 +216,14 @@
before pretty printing.
A typical add-on for the check/uncheck syntax layer is the @{command
- abbreviation} mechanism. Here the user specifies syntactic
- definitions that are managed by the system as polymorphic @{text
- "let"} bindings. These are expanded during the @{text "check"}
- phase, and contracted during the @{text "uncheck"} phase, without
- affecting the type-assignment of the given terms.
+ abbreviation} mechanism \cite{isabelle-isar-ref}. Here the user specifies
+ syntactic definitions that are managed by the system as polymorphic @{text
+ "let"} bindings. These are expanded during the @{text "check"} phase, and
+ contracted during the @{text "uncheck"} phase, without affecting the
+ type-assignment of the given terms.
- \medskip The precise meaning of type checking depends on the context
- --- additional check/uncheck plugins might be defined in user space.
+ \medskip The precise meaning of type checking depends on the context ---
+ additional check/uncheck modules might be defined in user space.
For example, the @{command class} command defines a context where
@{text "check"} treats certain type instances of overloaded
@@ -237,7 +237,7 @@
\begin{mldecls}
@{index_ML Syntax.check_typs: "Proof.context -> typ list -> typ list"} \\
@{index_ML Syntax.check_terms: "Proof.context -> term list -> term list"} \\
- @{index_ML Syntax.check_props: "Proof.context -> term list -> term list"} \\
+ @{index_ML Syntax.check_props: "Proof.context -> term list -> term list"} \\[0.5ex]
@{index_ML Syntax.uncheck_typs: "Proof.context -> typ list -> typ list"} \\
@{index_ML Syntax.uncheck_terms: "Proof.context -> term list -> term list"} \\
\end{mldecls}
@@ -256,7 +256,7 @@
Applications sometimes need to check several types and terms together. The
standard approach uses @{ML Logic.mk_type} to embed the language of types
into that of terms; all arguments are appended into one list of terms that
- is checked; afterwards the original type arguments are recovered with @{ML
+ is checked; afterwards the type arguments are recovered with @{ML
Logic.dest_type}.
\item @{ML Syntax.check_props}~@{text "ctxt ts"} checks a simultaneous list
@@ -273,8 +273,8 @@
\end{description}
- These operations always operate simultaneously on multiple items; use the
- combinator @{ML singleton} to apply them to a single item.
+ These operations always operate simultaneously on a list; use the combinator
+ @{ML singleton} to apply them to a single item.
*}
end
--- a/src/HOL/Algebra/Divisibility.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/Algebra/Divisibility.thy Thu Jul 03 14:40:36 2014 +0200
@@ -1655,6 +1655,7 @@
using assms
unfolding factors_def
apply (safe, force)
+apply hypsubst_thin
apply (induct fa)
apply simp
apply (simp add: m_assoc)
--- a/src/HOL/Auth/ZhouGollmann.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/Auth/ZhouGollmann.thy Thu Jul 03 14:40:36 2014 +0200
@@ -367,6 +367,7 @@
A \<notin> bad; evs \<in> zg |]
==> Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
apply clarify
+apply hypsubst_thin
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule zg.induct)
--- a/src/HOL/BNF_LFP.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/BNF_LFP.thy Thu Jul 03 14:40:36 2014 +0200
@@ -195,5 +195,4 @@
hide_fact (open) id_transfer
-
end
--- a/src/HOL/Bali/AxCompl.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/Bali/AxCompl.thy Thu Jul 03 14:40:36 2014 +0200
@@ -1381,6 +1381,7 @@
apply (rule MGF_nested_Methd)
apply (rule ballI)
apply (drule spec, erule impE, erule_tac [2] impE, erule_tac [3] spec)
+apply hypsubst_thin
apply fast
apply (drule finite_subset)
apply (erule finite_imageI)
--- a/src/HOL/Bali/Conform.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/Bali/Conform.thy Thu Jul 03 14:40:36 2014 +0200
@@ -440,8 +440,8 @@
apply (case_tac a)
apply (case_tac "absorb j a")
apply auto
-apply (rename_tac a)
-apply (case_tac "absorb j (Some a)",auto)
+apply (rename_tac a')
+apply (case_tac "absorb j (Some a')",auto)
apply (erule conforms_NormI)
done
--- a/src/HOL/Decision_Procs/MIR.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Thu Jul 03 14:40:36 2014 +0200
@@ -5272,7 +5272,7 @@
from ee' have tt': "Inum (a#bs) (Add e (C j)) = Inum (a#bs) (Add e' (C j))" by simp
from \<sigma>_cong[OF lp tt', where c="c"] px have px':"?sp c e' j" by simp
- from ecRo jD px' cc' show ?rhs apply auto
+ from ecRo jD px' show ?rhs apply (auto simp: cc')
by (rule_tac x="(e', c')" in bexI,simp_all)
(rule_tac x="j" in bexI, simp_all add: cc'[symmetric])
next
@@ -5286,7 +5286,7 @@
and cc':"c = c'" by blast
from ee' have tt': "Inum (a#bs) (Add e (C j)) = Inum (a#bs) (Add e' (C j))" by simp
from \<sigma>_cong[OF lp tt', where c="c"] px have px':"?sp c e' j" by simp
- from ecRo jD px' cc' show ?lhs apply auto
+ from ecRo jD px' show ?lhs apply (auto simp: cc')
by (rule_tac x="(e', c')" in bexI,simp_all)
(rule_tac x="j" in bexI, simp_all add: cc'[symmetric])
qed
--- a/src/HOL/Divides.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/Divides.thy Thu Jul 03 14:40:36 2014 +0200
@@ -461,7 +461,7 @@
apply (case_tac "y = 0") apply simp
apply (auto simp add: dvd_def)
apply (subgoal_tac "-(y * k) = y * - k")
- apply (erule ssubst)
+ apply (simp only:)
apply (erule div_mult_self1_is_id)
apply simp
done
@@ -470,8 +470,7 @@
apply (case_tac "y = 0") apply simp
apply (auto simp add: dvd_def)
apply (subgoal_tac "y * k = -y * -k")
- apply (erule ssubst)
- apply (rule div_mult_self1_is_id)
+ apply (erule ssubst, rule div_mult_self1_is_id)
apply simp
apply simp
done
--- a/src/HOL/HOLCF/Library/Stream.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/HOLCF/Library/Stream.thy Thu Jul 03 14:40:36 2014 +0200
@@ -5,7 +5,7 @@
header {* General Stream domain *}
theory Stream
-imports HOLCF "~~/src/HOL/Library/Extended_Nat"
+imports "../HOLCF" "~~/src/HOL/Library/Extended_Nat"
begin
default_sort pcpo
@@ -792,8 +792,8 @@
apply (drule ex_sconc, simp)
apply (rule someI2_ex, auto)
apply (simp add: i_rt_Suc_forw)
- apply (rule_tac x="a && x" in exI, auto)
- apply (case_tac "xa=UU",auto)
+ apply (rule_tac x="a && xa" in exI, auto)
+ apply (case_tac "xaa=UU",auto)
apply (drule stream_exhaust_eq [THEN iffD1],auto)
apply (drule streams_prefix_lemma1,simp+)
apply (simp add: sconc_def)
--- a/src/HOL/Hoare_Parallel/OG_Examples.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Examples.thy Thu Jul 03 14:40:36 2014 +0200
@@ -443,7 +443,7 @@
apply (simp_all (*asm_lr*) del:length_0_conv length_greater_0_conv add: nth_list_update mod_lemma)
--{* 9 subgoals left *}
apply (force simp add:less_Suc_eq)
-apply(drule sym)
+apply(hypsubst_thin, drule sym)
apply (force simp add:less_Suc_eq)+
done
--- a/src/HOL/IMP/Abs_Int2.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/IMP/Abs_Int2.thy Thu Jul 03 14:40:36 2014 +0200
@@ -132,8 +132,10 @@
by simp (metis And(1) And(2) in_gamma_sup_UpI)
next
case (Less e1 e2) thus ?case
- by(auto split: prod.split)
- (metis (lifting) inv_aval'_correct aval''_correct inv_less')
+ apply hypsubst_thin
+ apply (auto split: prod.split)
+ apply (metis (lifting) inv_aval'_correct aval''_correct inv_less')
+ done
qed
definition "step' = Step
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy Thu Jul 03 14:40:36 2014 +0200
@@ -166,8 +166,10 @@
case (And b1 b2) thus ?case by (auto simp: in_rep_join_UpI)
next
case (Less e1 e2) thus ?case
- by (auto split: prod.split)
- (metis afilter_sound filter_less' aval'_sound Less)
+ apply hypsubst_thin
+ apply (auto split: prod.split)
+ apply (metis afilter_sound filter_less' aval'_sound Less)
+ done
qed
fun AI :: "com \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ITP.thy Thu Jul 03 14:40:36 2014 +0200
@@ -135,11 +135,16 @@
next
case (Not b) thus ?case by simp
next
- case (And b1 b2) thus ?case by(fastforce simp: in_gamma_join_UpI)
+ case (And b1 b2) thus ?case
+ apply hypsubst_thin
+ apply (fastforce simp: in_gamma_join_UpI)
+ done
next
case (Less e1 e2) thus ?case
- by (auto split: prod.split)
- (metis afilter_sound filter_less' aval''_sound Less)
+ apply hypsubst_thin
+ apply (auto split: prod.split)
+ apply (metis afilter_sound filter_less' aval''_sound Less)
+ done
qed
--- a/src/HOL/Library/Float.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/Library/Float.thy Thu Jul 03 14:40:36 2014 +0200
@@ -75,6 +75,7 @@
lemma uminus_float[simp]: "x \<in> float \<Longrightarrow> -x \<in> float"
apply (auto simp: float_def)
+ apply hypsubst_thin
apply (rule_tac x="-x" in exI)
apply (rule_tac x="xa" in exI)
apply (simp add: field_simps)
@@ -82,6 +83,7 @@
lemma times_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> x * y \<in> float"
apply (auto simp: float_def)
+ apply hypsubst_thin
apply (rule_tac x="x * xa" in exI)
apply (rule_tac x="xb + xc" in exI)
apply (simp add: powr_add)
@@ -98,6 +100,7 @@
lemma div_power_2_float[simp]: "x \<in> float \<Longrightarrow> x / 2^d \<in> float"
apply (auto simp add: float_def)
+ apply hypsubst_thin
apply (rule_tac x="x" in exI)
apply (rule_tac x="xa - d" in exI)
apply (simp add: powr_realpow[symmetric] field_simps powr_add[symmetric])
@@ -105,6 +108,7 @@
lemma div_power_2_int_float[simp]: "x \<in> float \<Longrightarrow> x / (2::int)^d \<in> float"
apply (auto simp add: float_def)
+ apply hypsubst_thin
apply (rule_tac x="x" in exI)
apply (rule_tac x="xa - d" in exI)
apply (simp add: powr_realpow[symmetric] field_simps powr_add[symmetric])
--- a/src/HOL/Library/Multiset.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/Library/Multiset.thy Thu Jul 03 14:40:36 2014 +0200
@@ -1653,7 +1653,7 @@
apply (simp (no_asm))
apply (rule_tac x = "(K - {#a#}) + Ka" in exI)
apply (simp (no_asm_simp) add: add_assoc [symmetric])
- apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong)
+ apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="?S + ?T" in arg_cong)
apply (simp add: diff_union_single_conv)
apply (simp (no_asm_use) add: trans_def)
apply blast
@@ -1664,7 +1664,7 @@
apply (rule conjI)
apply (simp add: multiset_eq_iff split: nat_diff_split)
apply (rule conjI)
- apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong, simp)
+ apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="?S + ?T" in arg_cong, simp)
apply (simp add: multiset_eq_iff split: nat_diff_split)
apply (simp (no_asm_use) add: trans_def)
apply blast
@@ -2760,7 +2760,9 @@
using inj unfolding inj_on_def inj2_def using b1 c u(3) by blast
also have "... = count N1 b1" unfolding ss1[OF c b1, symmetric]
apply(rule setsum.cong[OF refl]) apply (transfer fixing: Ms u c b1 set2)
- using True h_u[OF c b1] set2_def u(2,3)[OF c b1] u_SET[OF c b1] by fastforce
+ using True h_u[OF c b1] set2_def u(2,3)[OF c b1] u_SET[OF c b1]
+ [[hypsubst_thin = true]]
+ by fastforce
finally show ?thesis .
qed
thus "count (mmap p1 M) b1 = count N1 b1" by transfer
@@ -2796,7 +2798,9 @@
also have "... = setsum (\<lambda> b1. count M (u c b1 b2)) (set1 c)" by simp
also have "... = count N2 b2" unfolding ss2[OF c b2, symmetric] comp_def
apply(rule setsum.cong[OF refl]) apply (transfer fixing: Ms u c b2 set1)
- using True h_u1[OF c _ b2] u(2,3)[OF c _ b2] u_SET[OF c _ b2] set1_def by fastforce
+ using True h_u1[OF c _ b2] u(2,3)[OF c _ b2] u_SET[OF c _ b2] set1_def
+ [[hypsubst_thin = true]]
+ by fastforce
finally show ?thesis .
qed
thus "count (mmap p2 M) b2 = count N2 b2" by transfer
--- a/src/HOL/MacLaurin.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/MacLaurin.thy Thu Jul 03 14:40:36 2014 +0200
@@ -419,8 +419,7 @@
apply (simp (no_asm))
apply (simp (no_asm) add: sin_expansion_lemma)
apply (force intro!: derivative_eq_intros)
-apply (subst (asm) setsum.neutral, clarify, case_tac "x", simp, simp)
-apply (cases n, simp, simp)
+apply (subst (asm) setsum.neutral, auto)[1]
apply (rule ccontr, simp)
apply (drule_tac x = x in spec, simp)
apply (erule ssubst)
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Thu Jul 03 14:40:36 2014 +0200
@@ -93,7 +93,7 @@
apply( rule oconf_obj [THEN iffD2])
apply( simp (no_asm))
apply( intro strip)
-apply( case_tac "(aaa, b) = (fn, fd)")
+apply( case_tac "(ab, b) = (fn, fd)")
apply( simp)
apply( fast intro: conf_widen)
apply( fast dest: conforms_heapD [THEN hconfD] oconf_objD)
--- a/src/HOL/Nat.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/Nat.thy Thu Jul 03 14:40:36 2014 +0200
@@ -1168,7 +1168,7 @@
-- {* elimination of @{text -} on @{text nat} *}
by (cases "a < b")
(auto simp add: diff_is_0_eq [THEN iffD2] diff_add_inverse
- not_less le_less dest!: sym [of a] sym [of b] add_eq_self_zero)
+ not_less le_less dest!: add_eq_self_zero add_eq_self_zero[OF sym])
lemma nat_diff_split_asm:
"P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
--- a/src/HOL/Nominal/Examples/Class1.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/Nominal/Examples/Class1.thy Thu Jul 03 14:40:36 2014 +0200
@@ -4720,7 +4720,7 @@
apply(erule_tac l_redu.cases, simp_all add: trm.inject)
apply(erule_tac c_redu.cases, simp_all add: trm.inject)
apply(auto)
-apply(rotate_tac 1)
+apply(rotate_tac 2)
apply(erule_tac a_redu.cases, simp_all add: trm.inject)
apply(erule_tac l_redu.cases, simp_all add: trm.inject)
apply(erule_tac c_redu.cases, simp_all add: trm.inject)
@@ -4741,7 +4741,7 @@
apply(erule_tac l_redu.cases, simp_all add: trm.inject)
apply(erule_tac c_redu.cases, simp_all add: trm.inject)
apply(auto)
-apply(rotate_tac 1)
+apply(rotate_tac 2)
apply(erule_tac a_redu.cases, simp_all add: trm.inject)
apply(erule_tac l_redu.cases, simp_all add: trm.inject)
apply(erule_tac c_redu.cases, simp_all add: trm.inject)
@@ -4851,7 +4851,7 @@
apply(erule_tac l_redu.cases, simp_all add: trm.inject)
apply(erule_tac c_redu.cases, simp_all add: trm.inject)
apply(auto)
-apply(rotate_tac 2)
+apply(rotate_tac 3)
apply(erule_tac a_redu.cases, simp_all add: trm.inject)
apply(erule_tac l_redu.cases, simp_all add: trm.inject)
apply(erule_tac c_redu.cases, simp_all add: trm.inject)
@@ -4872,7 +4872,7 @@
apply(erule_tac l_redu.cases, simp_all add: trm.inject)
apply(erule_tac c_redu.cases, simp_all add: trm.inject)
apply(auto)
-apply(rotate_tac 2)
+apply(rotate_tac 3)
apply(erule_tac a_redu.cases, simp_all add: trm.inject)
apply(erule_tac l_redu.cases, simp_all add: trm.inject)
apply(erule_tac c_redu.cases, simp_all add: trm.inject)
@@ -4982,7 +4982,7 @@
apply(erule_tac l_redu.cases, simp_all add: trm.inject)
apply(erule_tac c_redu.cases, simp_all add: trm.inject)
apply(auto)
-apply(rotate_tac 2)
+apply(rotate_tac 3)
apply(erule_tac a_redu.cases, simp_all add: trm.inject)
apply(erule_tac l_redu.cases, simp_all add: trm.inject)
apply(erule_tac c_redu.cases, simp_all add: trm.inject)
@@ -5003,7 +5003,7 @@
apply(erule_tac l_redu.cases, simp_all add: trm.inject)
apply(erule_tac c_redu.cases, simp_all add: trm.inject)
apply(auto)
-apply(rotate_tac 2)
+apply(rotate_tac 3)
apply(erule_tac a_redu.cases, simp_all add: trm.inject)
apply(erule_tac l_redu.cases, simp_all add: trm.inject)
apply(erule_tac c_redu.cases, simp_all add: trm.inject)
@@ -5113,7 +5113,7 @@
apply(erule_tac l_redu.cases, simp_all add: trm.inject)
apply(erule_tac c_redu.cases, simp_all add: trm.inject)
apply(auto)
-apply(rotate_tac 2)
+apply(rotate_tac 3)
apply(erule_tac a_redu.cases, simp_all add: trm.inject)
apply(erule_tac l_redu.cases, simp_all add: trm.inject)
apply(erule_tac c_redu.cases, simp_all add: trm.inject)
--- a/src/HOL/Nominal/Examples/Class2.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/Nominal/Examples/Class2.thy Thu Jul 03 14:40:36 2014 +0200
@@ -3491,7 +3491,7 @@
using a
apply(auto simp add: ctrm.inject alpha abs_fresh calc_atm)
apply(drule_tac x="x" in meta_spec)
-apply(drule_tac x="[(a,aa)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,aa)]\<bullet>Ma" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2))
@@ -3508,7 +3508,7 @@
using a
apply(auto simp add: ntrm.inject alpha abs_fresh calc_atm)
apply(drule_tac x="a" in meta_spec)
-apply(drule_tac x="[(x,xa)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(x,xa)]\<bullet>Ma" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1))
@@ -3526,7 +3526,7 @@
using a
apply(auto simp add: ctrm.inject alpha abs_fresh calc_atm fresh_atm)
apply(drule_tac x="c" in meta_spec)
-apply(drule_tac x="[(a,c)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,c)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="c" in meta_spec)
apply(drule_tac x="[(a,c)]\<bullet>N" in meta_spec)
apply(simp)
@@ -3543,7 +3543,7 @@
apply(case_tac "a=b")
apply(simp)
apply(drule_tac x="c" in meta_spec)
-apply(drule_tac x="[(b,c)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(b,c)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="c" in meta_spec)
apply(drule_tac x="[(b,c)]\<bullet>N" in meta_spec)
apply(simp)
@@ -3561,7 +3561,7 @@
apply(case_tac "c=b")
apply(simp)
apply(drule_tac x="b" in meta_spec)
-apply(drule_tac x="[(a,b)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,b)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="a" in meta_spec)
apply(drule_tac x="[(a,b)]\<bullet>N" in meta_spec)
apply(simp)
@@ -3577,7 +3577,7 @@
apply(simp)
apply(simp)
apply(drule_tac x="c" in meta_spec)
-apply(drule_tac x="[(a,c)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,c)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="b" in meta_spec)
apply(drule_tac x="[(a,c)]\<bullet>N" in meta_spec)
apply(simp)
@@ -3594,7 +3594,7 @@
apply(case_tac "a=aa")
apply(simp)
apply(drule_tac x="c" in meta_spec)
-apply(drule_tac x="[(aa,c)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(aa,c)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="c" in meta_spec)
apply(drule_tac x="[(aa,c)]\<bullet>N" in meta_spec)
apply(simp)
@@ -3612,7 +3612,7 @@
apply(case_tac "c=aa")
apply(simp)
apply(drule_tac x="a" in meta_spec)
-apply(drule_tac x="[(a,aa)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,aa)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="[(a,aa)]\<bullet>N" in meta_spec)
apply(simp)
@@ -3628,7 +3628,7 @@
apply(simp)
apply(simp)
apply(drule_tac x="aa" in meta_spec)
-apply(drule_tac x="[(a,c)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,c)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="c" in meta_spec)
apply(drule_tac x="[(a,c)]\<bullet>N" in meta_spec)
apply(simp)
@@ -3647,7 +3647,7 @@
apply(case_tac "aa=b")
apply(simp)
apply(drule_tac x="c" in meta_spec)
-apply(drule_tac x="[(b,c)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(b,c)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="c" in meta_spec)
apply(drule_tac x="[(b,c)]\<bullet>N" in meta_spec)
apply(simp)
@@ -3665,7 +3665,7 @@
apply(case_tac "c=b")
apply(simp)
apply(drule_tac x="b" in meta_spec)
-apply(drule_tac x="[(aa,b)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(aa,b)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="[(aa,b)]\<bullet>N" in meta_spec)
apply(simp)
@@ -3681,7 +3681,7 @@
apply(simp)
apply(simp)
apply(drule_tac x="c" in meta_spec)
-apply(drule_tac x="[(aa,c)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(aa,c)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="b" in meta_spec)
apply(drule_tac x="[(aa,c)]\<bullet>N" in meta_spec)
apply(simp)
@@ -3701,7 +3701,7 @@
apply(case_tac "a=b")
apply(simp)
apply(drule_tac x="b" in meta_spec)
-apply(drule_tac x="[(b,aa)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(b,aa)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="aa" in meta_spec)
apply(drule_tac x="[(b,aa)]\<bullet>N" in meta_spec)
apply(simp)
@@ -3719,7 +3719,7 @@
apply(case_tac "aa=b")
apply(simp)
apply(drule_tac x="a" in meta_spec)
-apply(drule_tac x="[(a,b)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,b)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="a" in meta_spec)
apply(drule_tac x="[(a,b)]\<bullet>N" in meta_spec)
apply(simp)
@@ -3735,7 +3735,7 @@
apply(simp)
apply(simp)
apply(drule_tac x="a" in meta_spec)
-apply(drule_tac x="[(a,aa)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,aa)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="b" in meta_spec)
apply(drule_tac x="[(a,aa)]\<bullet>N" in meta_spec)
apply(simp)
@@ -3753,7 +3753,7 @@
apply(case_tac "a=b")
apply(simp)
apply(drule_tac x="aa" in meta_spec)
-apply(drule_tac x="[(b,c)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(b,c)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="c" in meta_spec)
apply(drule_tac x="[(b,c)]\<bullet>N" in meta_spec)
apply(simp)
@@ -3771,7 +3771,7 @@
apply(case_tac "c=b")
apply(simp)
apply(drule_tac x="aa" in meta_spec)
-apply(drule_tac x="[(a,b)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,b)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="a" in meta_spec)
apply(drule_tac x="[(a,b)]\<bullet>N" in meta_spec)
apply(simp)
@@ -3787,7 +3787,7 @@
apply(simp)
apply(simp)
apply(drule_tac x="aa" in meta_spec)
-apply(drule_tac x="[(a,c)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,c)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="b" in meta_spec)
apply(drule_tac x="[(a,c)]\<bullet>N" in meta_spec)
apply(simp)
@@ -3806,7 +3806,7 @@
lemma ANDLEFT1_elim:
assumes a: "(x):M \<in> ANDLEFT1 (B AND C) (\<parallel>(B)\<parallel>)"
obtains x' M' where "M = AndL1 (x').M' x" and "fin (AndL1 (x').M' x) x" and "(x'):M' \<in> (\<parallel>(B)\<parallel>)"
-using a
+using a [[ hypsubst_thin = true ]]
apply(auto simp add: ntrm.inject alpha abs_fresh calc_atm)
apply(drule_tac x="y" in meta_spec)
apply(drule_tac x="[(x,y)]\<bullet>M" in meta_spec)
@@ -3859,7 +3859,7 @@
lemma ANDLEFT2_elim:
assumes a: "(x):M \<in> ANDLEFT2 (B AND C) (\<parallel>(C)\<parallel>)"
obtains x' M' where "M = AndL2 (x').M' x" and "fin (AndL2 (x').M' x) x" and "(x'):M' \<in> (\<parallel>(C)\<parallel>)"
-using a
+using a [[ hypsubst_thin = true ]]
apply(auto simp add: ntrm.inject alpha abs_fresh calc_atm)
apply(drule_tac x="y" in meta_spec)
apply(drule_tac x="[(x,y)]\<bullet>M" in meta_spec)
@@ -3915,7 +3915,7 @@
using a
apply(auto simp add: ctrm.inject alpha abs_fresh calc_atm)
apply(drule_tac x="b" in meta_spec)
-apply(drule_tac x="[(a,b)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,b)]\<bullet>Ma" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(a,b)]" in fic.eqvt(2))
@@ -3927,7 +3927,7 @@
apply(case_tac "a=aa")
apply(simp)
apply(drule_tac x="b" in meta_spec)
-apply(drule_tac x="[(aa,b)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(aa,b)]\<bullet>Ma" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(aa,b)]" in fic.eqvt(2))
@@ -3940,7 +3940,7 @@
apply(case_tac "b=aa")
apply(simp)
apply(drule_tac x="a" in meta_spec)
-apply(drule_tac x="[(a,aa)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,aa)]\<bullet>Ma" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2))
@@ -3951,7 +3951,7 @@
apply(simp)
apply(simp)
apply(drule_tac x="aa" in meta_spec)
-apply(drule_tac x="[(a,b)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,b)]\<bullet>Ma" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(a,b)]" in fic.eqvt(2))
@@ -3968,7 +3968,7 @@
using a
apply(auto simp add: ctrm.inject alpha abs_fresh calc_atm)
apply(drule_tac x="b" in meta_spec)
-apply(drule_tac x="[(a,b)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,b)]\<bullet>Ma" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(a,b)]" in fic.eqvt(2))
@@ -3980,7 +3980,7 @@
apply(case_tac "a=aa")
apply(simp)
apply(drule_tac x="b" in meta_spec)
-apply(drule_tac x="[(aa,b)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(aa,b)]\<bullet>Ma" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(aa,b)]" in fic.eqvt(2))
@@ -3993,7 +3993,7 @@
apply(case_tac "b=aa")
apply(simp)
apply(drule_tac x="a" in meta_spec)
-apply(drule_tac x="[(a,aa)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,aa)]\<bullet>Ma" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2))
@@ -4004,7 +4004,7 @@
apply(simp)
apply(simp)
apply(drule_tac x="aa" in meta_spec)
-apply(drule_tac x="[(a,b)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,b)]\<bullet>Ma" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(a,b)]" in fic.eqvt(2))
@@ -4022,7 +4022,7 @@
using a
apply(auto simp add: ntrm.inject alpha abs_fresh calc_atm fresh_atm)
apply(drule_tac x="z" in meta_spec)
-apply(drule_tac x="[(x,z)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(x,z)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="z" in meta_spec)
apply(drule_tac x="[(x,z)]\<bullet>N" in meta_spec)
apply(simp)
@@ -4039,7 +4039,7 @@
apply(case_tac "x=y")
apply(simp)
apply(drule_tac x="z" in meta_spec)
-apply(drule_tac x="[(y,z)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(y,z)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="z" in meta_spec)
apply(drule_tac x="[(y,z)]\<bullet>N" in meta_spec)
apply(simp)
@@ -4057,7 +4057,7 @@
apply(case_tac "z=y")
apply(simp)
apply(drule_tac x="y" in meta_spec)
-apply(drule_tac x="[(x,y)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(x,y)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="[(x,y)]\<bullet>N" in meta_spec)
apply(simp)
@@ -4073,7 +4073,7 @@
apply(simp)
apply(simp)
apply(drule_tac x="z" in meta_spec)
-apply(drule_tac x="[(x,z)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(x,z)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="y" in meta_spec)
apply(drule_tac x="[(x,z)]\<bullet>N" in meta_spec)
apply(simp)
@@ -4090,7 +4090,7 @@
apply(case_tac "x=xa")
apply(simp)
apply(drule_tac x="z" in meta_spec)
-apply(drule_tac x="[(xa,z)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(xa,z)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="z" in meta_spec)
apply(drule_tac x="[(xa,z)]\<bullet>N" in meta_spec)
apply(simp)
@@ -4108,7 +4108,7 @@
apply(case_tac "z=xa")
apply(simp)
apply(drule_tac x="x" in meta_spec)
-apply(drule_tac x="[(x,xa)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(x,xa)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="[(x,xa)]\<bullet>N" in meta_spec)
apply(simp)
@@ -4124,7 +4124,7 @@
apply(simp)
apply(simp)
apply(drule_tac x="xa" in meta_spec)
-apply(drule_tac x="[(x,z)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(x,z)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="z" in meta_spec)
apply(drule_tac x="[(x,z)]\<bullet>N" in meta_spec)
apply(simp)
@@ -4143,7 +4143,7 @@
apply(case_tac "xa=y")
apply(simp)
apply(drule_tac x="z" in meta_spec)
-apply(drule_tac x="[(y,z)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(y,z)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="z" in meta_spec)
apply(drule_tac x="[(y,z)]\<bullet>N" in meta_spec)
apply(simp)
@@ -4161,7 +4161,7 @@
apply(case_tac "z=y")
apply(simp)
apply(drule_tac x="y" in meta_spec)
-apply(drule_tac x="[(xa,y)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(xa,y)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="[(xa,y)]\<bullet>N" in meta_spec)
apply(simp)
@@ -4177,7 +4177,7 @@
apply(simp)
apply(simp)
apply(drule_tac x="z" in meta_spec)
-apply(drule_tac x="[(xa,z)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(xa,z)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="y" in meta_spec)
apply(drule_tac x="[(xa,z)]\<bullet>N" in meta_spec)
apply(simp)
@@ -4197,7 +4197,7 @@
apply(case_tac "x=y")
apply(simp)
apply(drule_tac x="y" in meta_spec)
-apply(drule_tac x="[(y,xa)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(y,xa)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="[(y,xa)]\<bullet>N" in meta_spec)
apply(simp)
@@ -4215,7 +4215,7 @@
apply(case_tac "xa=y")
apply(simp)
apply(drule_tac x="x" in meta_spec)
-apply(drule_tac x="[(x,y)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(x,y)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="[(x,y)]\<bullet>N" in meta_spec)
apply(simp)
@@ -4231,7 +4231,7 @@
apply(simp)
apply(simp)
apply(drule_tac x="x" in meta_spec)
-apply(drule_tac x="[(x,xa)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(x,xa)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="y" in meta_spec)
apply(drule_tac x="[(x,xa)]\<bullet>N" in meta_spec)
apply(simp)
@@ -4249,7 +4249,7 @@
apply(case_tac "x=y")
apply(simp)
apply(drule_tac x="xa" in meta_spec)
-apply(drule_tac x="[(y,z)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(y,z)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="z" in meta_spec)
apply(drule_tac x="[(y,z)]\<bullet>N" in meta_spec)
apply(simp)
@@ -4267,7 +4267,7 @@
apply(case_tac "z=y")
apply(simp)
apply(drule_tac x="xa" in meta_spec)
-apply(drule_tac x="[(x,y)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(x,y)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="[(x,y)]\<bullet>N" in meta_spec)
apply(simp)
@@ -4283,7 +4283,7 @@
apply(simp)
apply(simp)
apply(drule_tac x="xa" in meta_spec)
-apply(drule_tac x="[(x,z)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(x,z)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="y" in meta_spec)
apply(drule_tac x="[(x,z)]\<bullet>N" in meta_spec)
apply(simp)
@@ -4308,7 +4308,7 @@
apply(auto simp add: ctrm.inject alpha abs_fresh calc_atm)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="b" in meta_spec)
-apply(drule_tac x="[(a,b)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,b)]\<bullet>Ma" in meta_spec)
apply(simp)
apply(drule_tac pi="[(a,b)]" in fic.eqvt(2))
apply(simp add: calc_atm)
@@ -4319,7 +4319,7 @@
apply(drule_tac x="z" in spec)
apply(drule_tac x="[(a,b)]\<bullet>P" in spec)
apply(simp add: fresh_prod fresh_left calc_atm)
-apply(drule_tac pi="[(a,b)]" and x="(x):M{a:=(z).([(a,b)]\<bullet>P)}"
+apply(drule_tac pi="[(a,b)]" and x="(x):Ma{a:=(z).([(a,b)]\<bullet>P)}"
in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(perm_simp add: calc_atm csubst_eqvt CAND_eqvt_coname)
apply(drule meta_mp)
@@ -4332,7 +4332,7 @@
apply(simp add: fresh_prod fresh_left)
apply(drule mp)
apply(simp add: calc_atm)
-apply(drule_tac pi="[(a,b)]" and x="<a>:M{x:=<([(a,b)]\<bullet>c)>.([(a,b)]\<bullet>Q)}"
+apply(drule_tac pi="[(a,b)]" and x="<a>:Ma{x:=<([(a,b)]\<bullet>c)>.([(a,b)]\<bullet>Q)}"
in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(perm_simp add: nsubst_eqvt CAND_eqvt_coname)
apply(simp add: calc_atm)
@@ -4340,7 +4340,7 @@
apply(simp)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="b" in meta_spec)
-apply(drule_tac x="[(aa,b)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(aa,b)]\<bullet>Ma" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(aa,b)]" in fic.eqvt(2))
@@ -4352,7 +4352,7 @@
apply(drule_tac x="z" in spec)
apply(drule_tac x="[(a,b)]\<bullet>P" in spec)
apply(simp add: fresh_prod fresh_left calc_atm)
-apply(drule_tac pi="[(a,b)]" and x="(x):M{a:=(z).([(a,b)]\<bullet>P)}"
+apply(drule_tac pi="[(a,b)]" and x="(x):Ma{a:=(z).([(a,b)]\<bullet>P)}"
in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(perm_simp add: calc_atm csubst_eqvt CAND_eqvt_coname)
apply(drule meta_mp)
@@ -4365,7 +4365,7 @@
apply(simp add: fresh_prod fresh_left)
apply(drule mp)
apply(simp add: calc_atm)
-apply(drule_tac pi="[(a,b)]" and x="<a>:M{x:=<([(a,b)]\<bullet>c)>.([(a,b)]\<bullet>Q)}"
+apply(drule_tac pi="[(a,b)]" and x="<a>:Ma{x:=<([(a,b)]\<bullet>c)>.([(a,b)]\<bullet>Q)}"
in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(perm_simp add: nsubst_eqvt CAND_eqvt_coname)
apply(simp add: calc_atm)
@@ -4374,7 +4374,7 @@
apply(simp)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="a" in meta_spec)
-apply(drule_tac x="[(a,aa)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,aa)]\<bullet>Ma" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(a,aa)]" in fic.eqvt(2))
@@ -4386,7 +4386,7 @@
apply(drule_tac x="z" in spec)
apply(drule_tac x="[(a,aa)]\<bullet>P" in spec)
apply(simp add: fresh_prod fresh_left calc_atm)
-apply(drule_tac pi="[(a,aa)]" and x="(x):M{aa:=(z).([(a,aa)]\<bullet>P)}"
+apply(drule_tac pi="[(a,aa)]" and x="(x):Ma{aa:=(z).([(a,aa)]\<bullet>P)}"
in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(perm_simp add: calc_atm csubst_eqvt CAND_eqvt_coname)
apply(drule meta_mp)
@@ -4399,14 +4399,14 @@
apply(simp add: fresh_prod fresh_left)
apply(drule mp)
apply(simp add: calc_atm)
-apply(drule_tac pi="[(a,aa)]" and x="<aa>:M{x:=<([(a,aa)]\<bullet>c)>.([(a,aa)]\<bullet>Q)}"
+apply(drule_tac pi="[(a,aa)]" and x="<aa>:Ma{x:=<([(a,aa)]\<bullet>c)>.([(a,aa)]\<bullet>Q)}"
in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(perm_simp add: nsubst_eqvt CAND_eqvt_coname)
apply(simp add: calc_atm)
apply(simp)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="aa" in meta_spec)
-apply(drule_tac x="[(a,b)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(a,b)]\<bullet>Ma" in meta_spec)
apply(simp)
apply(drule meta_mp)
apply(drule_tac pi="[(a,b)]" in fic.eqvt(2))
@@ -4418,7 +4418,7 @@
apply(drule_tac x="z" in spec)
apply(drule_tac x="[(a,b)]\<bullet>P" in spec)
apply(simp add: fresh_prod fresh_left calc_atm)
-apply(drule_tac pi="[(a,b)]" and x="(x):M{aa:=(z).([(a,b)]\<bullet>P)}"
+apply(drule_tac pi="[(a,b)]" and x="(x):Ma{aa:=(z).([(a,b)]\<bullet>P)}"
in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(perm_simp add: calc_atm csubst_eqvt CAND_eqvt_coname)
apply(drule meta_mp)
@@ -4430,7 +4430,7 @@
apply(simp add: fresh_prod fresh_left)
apply(drule mp)
apply(simp add: calc_atm)
-apply(drule_tac pi="[(a,b)]" and x="<aa>:M{x:=<([(a,b)]\<bullet>c)>.([(a,b)]\<bullet>Q)}"
+apply(drule_tac pi="[(a,b)]" and x="<aa>:Ma{x:=<([(a,b)]\<bullet>c)>.([(a,b)]\<bullet>Q)}"
in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
apply(perm_simp add: nsubst_eqvt CAND_eqvt_coname)
apply(simp add: calc_atm)
@@ -4443,7 +4443,7 @@
using a
apply(auto simp add: ntrm.inject alpha abs_fresh calc_atm)
apply(drule_tac x="a" in meta_spec)
-apply(drule_tac x="[(x,y)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(x,y)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="y" in meta_spec)
apply(drule_tac x="[(x,y)]\<bullet>N" in meta_spec)
apply(simp)
@@ -4460,7 +4460,7 @@
apply(case_tac "x=xa")
apply(simp)
apply(drule_tac x="a" in meta_spec)
-apply(drule_tac x="[(xa,y)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(xa,y)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="y" in meta_spec)
apply(drule_tac x="[(xa,y)]\<bullet>N" in meta_spec)
apply(simp)
@@ -4478,7 +4478,7 @@
apply(case_tac "y=xa")
apply(simp)
apply(drule_tac x="a" in meta_spec)
-apply(drule_tac x="[(x,xa)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(x,xa)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="x" in meta_spec)
apply(drule_tac x="[(x,xa)]\<bullet>N" in meta_spec)
apply(simp)
@@ -4486,7 +4486,7 @@
apply(drule_tac pi="[(x,xa)]" in fin.eqvt(1))
apply(simp add: calc_atm)
apply(drule meta_mp)
-apply(drule_tac pi="[(x,xa)]" and x="<a>:M" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
+apply(drule_tac pi="[(x,xa)]" and x="<a>:Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
apply(simp add: calc_atm CAND_eqvt_name)
apply(drule meta_mp)
apply(drule_tac pi="[(x,xa)]" and x="(xa):N" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
@@ -4494,7 +4494,7 @@
apply(simp)
apply(simp)
apply(drule_tac x="a" in meta_spec)
-apply(drule_tac x="[(x,y)]\<bullet>M" in meta_spec)
+apply(drule_tac x="[(x,y)]\<bullet>Ma" in meta_spec)
apply(drule_tac x="xa" in meta_spec)
apply(drule_tac x="[(x,y)]\<bullet>N" in meta_spec)
apply(simp)
--- a/src/HOL/Old_Number_Theory/Chinese.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Chinese.thy Thu Jul 03 14:40:36 2014 +0200
@@ -174,7 +174,7 @@
apply (rule_tac [!] funprod_zgcd)
apply safe
apply simp_all
- apply (subgoal_tac "i<n")
+ apply (subgoal_tac "ia<n")
prefer 2
apply arith
apply (case_tac [2] i)
--- a/src/HOL/Old_Number_Theory/Euler.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Euler.thy Thu Jul 03 14:40:36 2014 +0200
@@ -138,6 +138,7 @@
[\<Prod>x = a] (mod p)"
apply (auto simp add: SetS_def MultInvPair_def)
apply (frule StandardRes_SRStar_prop1a)
+ apply hypsubst_thin
apply (subgoal_tac "StandardRes p x \<noteq> StandardRes p (a * MultInv p x)")
apply (auto simp add: StandardRes_prop2 MultInvPair_distinct)
apply (frule_tac m = p and x = x and y = "(a * MultInv p x)" in
--- a/src/HOL/Old_Number_Theory/Gauss.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Gauss.thy Thu Jul 03 14:40:36 2014 +0200
@@ -170,7 +170,7 @@
apply (auto simp add: B_def)
apply (frule A_ncong_p)
apply (insert p_a_relprime p_prime a_nonzero)
- apply (frule_tac a = x and b = a in zcong_zprime_prod_zero_contra)
+ apply (frule_tac a = xa and b = a in zcong_zprime_prod_zero_contra)
apply (auto simp add: A_greater_zero)
done
@@ -180,9 +180,9 @@
lemma C_ncong_p: "x \<in> C ==> ~[x = 0](mod p)"
apply (auto simp add: C_def)
apply (frule B_ncong_p)
- apply (subgoal_tac "[x = StandardRes p x](mod p)")
+ apply (subgoal_tac "[xa = StandardRes p xa](mod p)")
defer apply (simp add: StandardRes_prop1)
- apply (frule_tac a = x and b = "StandardRes p x" and c = 0 in zcong_trans)
+ apply (frule_tac a = xa and b = "StandardRes p xa" and c = 0 in zcong_trans)
apply auto
done
--- a/src/HOL/Probability/ex/Dining_Cryptographers.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy Thu Jul 03 14:40:36 2014 +0200
@@ -239,7 +239,7 @@
ultimately
have "{dc \<in> dc_crypto. payer dc = Some i \<and> inversion dc = xs} =
{(Some i, zs), (Some i, map Not zs)}"
- using `i < n`
+ using `i < n` [[ hypsubst_thin = true ]]
proof (safe, simp_all add:dc_crypto payer_def)
fix b assume [simp]: "length b = n"
and *: "inversion (Some i, b) = xs" and "b \<noteq> zs"
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Thu Jul 03 14:40:36 2014 +0200
@@ -57,6 +57,7 @@
using a
apply(cases x, cases y, cases z)
apply(auto simp add: times_int_raw.simps intrel.simps)
+ apply(hypsubst_thin)
apply(rename_tac u v w x y z)
apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
apply(simp add: mult_ac)
@@ -69,6 +70,7 @@
using a
apply(cases x, cases y, cases z)
apply(auto simp add: times_int_raw.simps intrel.simps)
+ apply(hypsubst_thin)
apply(rename_tac u v w x y z)
apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
apply(simp add: mult_ac)
--- a/src/HOL/SET_Protocol/Purchase.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/SET_Protocol/Purchase.thy Thu Jul 03 14:40:36 2014 +0200
@@ -1119,6 +1119,7 @@
OIData, Hash PIData|}
\<in> set evs"
apply clarify
+apply hypsubst_thin
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule set_pur.induct, simp_all, auto)
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Jul 03 14:40:36 2014 +0200
@@ -1503,6 +1503,15 @@
fun mk_rel_inject_thm ((ctr_def', cxIn), (_, cyIn)) =
mk_rel_thm (unfold_thms lthy @{thms eq_sym_Unity_conv}) [ctr_def'] cxIn cyIn;
+ fun mk_rel_intro_thm thm =
+ let
+ fun impl thm = rotate_prems (~1) (impl (rotate_prems 1 (conjI RS thm)))
+ handle THM _ => thm
+ in
+ impl (thm RS iffD2)
+ handle THM _ => thm
+ end;
+
fun mk_half_rel_distinct_thm ((xctr_def', cxIn), (yctr_def', cyIn)) =
mk_rel_thm (fn thm => thm RS @{thm eq_False[THEN iffD1]}) [xctr_def', yctr_def']
cxIn cyIn;
@@ -1512,6 +1521,8 @@
RS (rel_flip RS sym RS @{thm arg_cong[of _ _ Not]} RS iffD2);
val rel_inject_thms = map mk_rel_inject_thm (op ~~ rel_infos);
+ val rel_intro_thms = map mk_rel_intro_thm rel_inject_thms;
+
val half_rel_distinct_thmss =
map (map mk_half_rel_distinct_thm) (mk_half_pairss rel_infos);
val other_half_rel_distinct_thmss =
@@ -1534,6 +1545,7 @@
(mapN, map_thms, code_nitpicksimp_attrs @ simp_attrs),
(rel_distinctN, rel_distinct_thms, simp_attrs),
(rel_injectN, rel_inject_thms, simp_attrs),
+ (rel_introsN, rel_intro_thms, []),
(setN, set_thms, code_nitpicksimp_attrs @ simp_attrs),
(sel_mapN, sel_map_thms, []),
(sel_setN, sel_set_thms, []),
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Jul 03 14:40:36 2014 +0200
@@ -127,6 +127,7 @@
val rel_coinductN: string
val rel_inductN: string
val rel_injectN: string
+ val rel_introsN: string
val rel_distinctN: string
val rvN: string
val sel_corecN: string
@@ -406,6 +407,7 @@
val rel_distinctN = relN ^ "_" ^ distinctN
val injectN = "inject"
val rel_injectN = relN ^ "_" ^ injectN
+val rel_introsN = relN ^ "_intros"
val rel_coinductN = relN ^ "_" ^ coinductN
val dtor_rel_coinductN = dtorN ^ "_" ^ rel_coinductN
val rel_inductN = relN ^ "_" ^ inductN
--- a/src/HOL/Transcendental.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/Transcendental.thy Thu Jul 03 14:40:36 2014 +0200
@@ -3046,6 +3046,7 @@
lemma tan_total: "EX! x. -(pi/2) < x & x < (pi/2) & tan x = y"
apply (cut_tac y = y in lemma_tan_total1, auto)
+ apply hypsubst_thin
apply (cut_tac x = xa and y = y in linorder_less_linear, auto)
apply (subgoal_tac [2] "\<exists>z. y < z & z < xa & DERIV tan z :> 0")
apply (subgoal_tac "\<exists>z. xa < z & z < y & DERIV tan z :> 0")
--- a/src/HOL/UNITY/Comp/Priority.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/UNITY/Comp/Priority.thy Thu Jul 03 14:40:36 2014 +0200
@@ -209,7 +209,7 @@
leadsTo {s. above i s < x}"
apply (rule leadsTo_UN)
apply (rule single_leadsTo_I, clarify)
-apply (rule_tac x = "above i x" in above_decreases_lemma)
+apply (rule_tac x = "above i xa" in above_decreases_lemma)
apply (simp_all (no_asm_use) add: Highest_iff_above0)
apply blast+
done
--- a/src/HOL/Word/Bool_List_Representation.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/Word/Bool_List_Representation.thy Thu Jul 03 14:40:36 2014 +0200
@@ -595,7 +595,7 @@
lemma takefill_same':
"l = length xs ==> takefill fill l xs = xs"
- by clarify (induct xs, auto)
+ by (induct xs arbitrary: l, auto)
lemmas takefill_same [simp] = takefill_same' [OF refl]
--- a/src/HOL/Word/Misc_Typedef.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/Word/Misc_Typedef.thy Thu Jul 03 14:40:36 2014 +0200
@@ -194,7 +194,7 @@
prefer 2
apply (simp add: comp_assoc)
apply (rule ext)
- apply (drule fun_cong)
+ apply (drule_tac f="?a o ?b" in fun_cong)
apply simp
done
--- a/src/HOL/Word/Word.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/Word/Word.thy Thu Jul 03 14:40:36 2014 +0200
@@ -3176,6 +3176,12 @@
of_bl_rep_False [where n=1 and bs="[]", simplified])
done
+lemma zip_replicate:
+ "n \<ge> length ys \<Longrightarrow> zip (replicate n x) ys = map (\<lambda>y. (x, y)) ys"
+ apply (induct ys arbitrary: n, simp_all)
+ apply (case_tac n, simp_all)
+ done
+
lemma align_lem_or [rule_format] :
"ALL x m. length x = n + m --> length y = n + m -->
drop m x = replicate n False --> take m y = replicate m False -->
@@ -3185,9 +3191,8 @@
apply clarsimp
apply (case_tac x, force)
apply (case_tac m, auto)
- apply (drule sym)
- apply auto
- apply (induct_tac list, auto)
+ apply (drule_tac t="length ?xs" in sym)
+ apply (clarsimp simp: map2_def zip_replicate o_def)
done
lemma align_lem_and [rule_format] :
@@ -3199,9 +3204,8 @@
apply clarsimp
apply (case_tac x, force)
apply (case_tac m, auto)
- apply (drule sym)
- apply auto
- apply (induct_tac list, auto)
+ apply (drule_tac t="length ?xs" in sym)
+ apply (clarsimp simp: map2_def zip_replicate o_def map_replicate_const)
done
lemma aligned_bl_add_size [OF refl]:
@@ -3676,6 +3680,7 @@
apply safe
defer
apply (clarsimp split: prod.splits)
+ apply hypsubst_thin
apply (drule word_ubin.norm_Rep [THEN ssubst])
apply (drule split_bintrunc)
apply (simp add : of_bl_def bl2bin_drop word_size
--- a/src/HOL/ZF/HOLZF.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/ZF/HOLZF.thy Thu Jul 03 14:40:36 2014 +0200
@@ -168,7 +168,7 @@
theorem Domain: "Elem x (Domain f) = (? y. Elem (Opair x y) f)"
apply (auto simp add: Domain_def Replacement)
- apply (rule_tac x="Snd x" in exI)
+ apply (rule_tac x="Snd xa" in exI)
apply (simp add: FstSnd)
apply (rule_tac x="Opair x y" in exI)
apply (simp add: isOpair Fst)
--- a/src/HOL/ex/Dedekind_Real.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/HOL/ex/Dedekind_Real.thy Thu Jul 03 14:40:36 2014 +0200
@@ -313,7 +313,7 @@
"[|A \<in> preal; B \<in> preal; y \<in> add_set A B|] ==> \<exists>u \<in> add_set A B. y < u"
apply (auto simp add: add_set_def)
apply (frule preal_exists_greater [of A], auto)
-apply (rule_tac x="u + y" in exI)
+apply (rule_tac x="u + ya" in exI)
apply (auto intro: add_strict_left_mono)
done
@@ -439,7 +439,7 @@
"[|A \<in> preal; B \<in> preal; y \<in> mult_set A B|] ==> \<exists>u \<in> mult_set A B. y < u"
apply (auto simp add: mult_set_def)
apply (frule preal_exists_greater [of A], auto)
-apply (rule_tac x="u * y" in exI)
+apply (rule_tac x="u * ya" in exI)
apply (auto intro: preal_imp_pos [of A] preal_imp_pos [of B]
mult_strict_right_mono)
done
@@ -1590,7 +1590,7 @@
"\<exists>m. (x::real) = real_of_preal m | x = 0 | x = -(real_of_preal m)"
apply (simp add: real_of_preal_def real_zero_def, cases x)
apply (auto simp add: real_minus add_ac)
-apply (cut_tac x = x and y = y in linorder_less_linear)
+apply (cut_tac x = xa and y = y in linorder_less_linear)
apply (auto dest!: less_add_left_Ex simp add: add_assoc [symmetric])
done
--- a/src/Provers/hypsubst.ML Thu Jul 03 09:55:16 2014 +0200
+++ b/src/Provers/hypsubst.ML Thu Jul 03 14:40:36 2014 +0200
@@ -47,6 +47,8 @@
signature HYPSUBST =
sig
val bound_hyp_subst_tac : Proof.context -> int -> tactic
+ val hyp_subst_tac_thin : bool -> Proof.context -> int -> tactic
+ val hyp_subst_thins : bool Config.T
val hyp_subst_tac : Proof.context -> int -> tactic
val blast_hyp_subst_tac : bool -> int -> tactic
val stac : thm -> int -> tactic
@@ -77,7 +79,8 @@
Not if it involves a variable free in the premises,
but we can't check for this -- hence bnd and bound_hyp_subst_tac
Prefer to eliminate Bound variables if possible.
- Result: true = use as is, false = reorient first *)
+ Result: true = use as is, false = reorient first
+ also returns var to substitute, relevant if it is Free *)
fun inspect_pair bnd novars (t, u) =
if novars andalso (has_tvars t orelse has_tvars u)
then raise Match (*variables in the type!*)
@@ -86,55 +89,75 @@
(Bound i, _) =>
if loose_bvar1 (u, i) orelse novars andalso has_vars u
then raise Match
- else true (*eliminates t*)
+ else (true, Bound i) (*eliminates t*)
| (_, Bound i) =>
if loose_bvar1 (t, i) orelse novars andalso has_vars t
then raise Match
- else false (*eliminates u*)
+ else (false, Bound i) (*eliminates u*)
| (t' as Free _, _) =>
if bnd orelse Logic.occs (t', u) orelse novars andalso has_vars u
then raise Match
- else true (*eliminates t*)
+ else (true, t') (*eliminates t*)
| (_, u' as Free _) =>
if bnd orelse Logic.occs (u', t) orelse novars andalso has_vars t
then raise Match
- else false (*eliminates u*)
+ else (false, u') (*eliminates u*)
| _ => raise Match);
(*Locates a substitutable variable on the left (resp. right) of an equality
assumption. Returns the number of intervening assumptions. *)
-fun eq_var bnd novars =
- let fun eq_var_aux k (Const(@{const_name Pure.all},_) $ Abs(_,_,t)) = eq_var_aux k t
- | eq_var_aux k (Const(@{const_name Pure.imp},_) $ A $ B) =
- ((k, inspect_pair bnd novars
- (Data.dest_eq (Data.dest_Trueprop A)))
- handle TERM _ => eq_var_aux (k+1) B
- | Match => eq_var_aux (k+1) B)
- | eq_var_aux k _ = raise EQ_VAR
- in eq_var_aux 0 end;
+fun eq_var bnd novars check_frees t =
+ let
+ fun check_free ts (orient, Free f)
+ = if not check_frees orelse not orient
+ orelse exists (curry Logic.occs (Free f)) ts
+ then (orient, true) else raise Match
+ | check_free ts (orient, _) = (orient, false)
+ fun eq_var_aux k (Const(@{const_name Pure.all},_) $ Abs(_,_,t)) hs = eq_var_aux k t hs
+ | eq_var_aux k (Const(@{const_name Pure.imp},_) $ A $ B) hs =
+ ((k, check_free (B :: hs) (inspect_pair bnd novars
+ (Data.dest_eq (Data.dest_Trueprop A))))
+ handle TERM _ => eq_var_aux (k+1) B (A :: hs)
+ | Match => eq_var_aux (k+1) B (A :: hs))
+ | eq_var_aux k _ _ = raise EQ_VAR
+
+ in eq_var_aux 0 t [] end;
+
+val thin_free_eq_tac = SUBGOAL (fn (t, i) => let
+ val (k, _) = eq_var false false false t
+ val ok = (eq_var false false true t |> fst) > k
+ handle EQ_VAR => true
+ in if ok then EVERY [rotate_tac k i, etac thin_rl i, rotate_tac (~k) i]
+ else no_tac
+ end handle EQ_VAR => no_tac)
(*For the simpset. Adds ALL suitable equalities, even if not first!
No vars are allowed here, as simpsets are built from meta-assumptions*)
fun mk_eqs bnd th =
- [ if inspect_pair bnd false (Data.dest_eq (Data.dest_Trueprop (Thm.prop_of th)))
+ [ if inspect_pair bnd false (Data.dest_eq (Data.dest_Trueprop (Thm.prop_of th))) |> fst
then th RS Data.eq_reflection
else Thm.symmetric(th RS Data.eq_reflection) (*reorient*) ]
handle TERM _ => [] | Match => [];
+fun bool2s true = "true" | bool2s false = "false"
+
local
in
(*Select a suitable equality assumption; substitute throughout the subgoal
If bnd is true, then it replaces Bound variables only. *)
fun gen_hyp_subst_tac ctxt bnd =
- let fun tac i st = SUBGOAL (fn (Bi, _) =>
+ SUBGOAL (fn (Bi, i) =>
let
- val (k, _) = eq_var bnd true Bi
+ val (k, (orient, is_free)) = eq_var bnd true true Bi
val hyp_subst_ctxt = empty_simpset ctxt |> Simplifier.set_mksimps (K (mk_eqs bnd))
in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ctxt i,
- etac thin_rl i, rotate_tac (~k) i]
- end handle THM _ => no_tac | EQ_VAR => no_tac) i st
- in REPEAT_DETERM1 o tac end;
+ if not is_free then etac thin_rl i
+ else if orient then etac Data.rev_mp i
+ else etac (Data.sym RS Data.rev_mp) i,
+ rotate_tac (~k) i,
+ if is_free then rtac Data.imp_intr i else all_tac]
+ end handle THM _ => no_tac | EQ_VAR => no_tac)
end;
@@ -174,6 +197,9 @@
val imp_intr_tac = rtac Data.imp_intr;
+fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
+val dup_subst = rev_dup_elim ssubst
+
(* FIXME: "etac Data.rev_mp i" will not behave as expected if goal has *)
(* premises containing meta-implications or quantifiers *)
@@ -181,26 +207,37 @@
to handle equalities containing Vars.*)
fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
let val n = length(Logic.strip_assums_hyp Bi) - 1
- val (k,symopt) = eq_var bnd false Bi
+ val (k, (orient, is_free)) = eq_var bnd false true Bi
+ val rl = if is_free then dup_subst else ssubst
+ val rl = if orient then rl else Data.sym RS rl
in
DETERM
(EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
rotate_tac 1 i,
REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
- inst_subst_tac symopt (if symopt then ssubst else Data.subst) i,
+ inst_subst_tac orient rl i,
REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)])
end
handle THM _ => no_tac | EQ_VAR => no_tac);
-(*Substitutes for Free or Bound variables*)
-fun hyp_subst_tac ctxt =
- FIRST' [ematch_tac [Data.thin_refl],
- gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac false];
+(*Substitutes for Free or Bound variables,
+ discarding equalities on Bound variables
+ and on Free variables if thin=true*)
+fun hyp_subst_tac_thin thin ctxt =
+ REPEAT_DETERM1 o FIRST' [ematch_tac [Data.thin_refl],
+ gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac false,
+ if thin then thin_free_eq_tac else K no_tac];
+
+val (hyp_subst_thins, hyp_subst_thins_setup) = Attrib.config_bool
+ @{binding hypsubst_thin} (K false);
+
+fun hyp_subst_tac ctxt = hyp_subst_tac_thin
+ (Config.get ctxt hyp_subst_thins) ctxt
(*Substitutes for Bound variables only -- this is always safe*)
fun bound_hyp_subst_tac ctxt =
- gen_hyp_subst_tac ctxt true ORELSE' vars_gen_hyp_subst_tac true;
-
+ REPEAT_DETERM1 o (gen_hyp_subst_tac ctxt true
+ ORELSE' vars_gen_hyp_subst_tac true);
(** Version for Blast_tac. Hyps that are affected by the substitution are
moved to the front. Defect: even trivial changes are noticed, such as
@@ -236,7 +273,7 @@
fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) =>
- let val (k,symopt) = eq_var false false Bi
+ let val (k, (symopt, _)) = eq_var false false false Bi
val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi)
(*omit selected equality, returning other hyps*)
val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1)
@@ -252,7 +289,6 @@
end
handle THM _ => no_tac | EQ_VAR => no_tac);
-
(*apply an equality or definition ONCE;
fails unless the substitution has an effect*)
fun stac th =
@@ -266,6 +302,11 @@
Method.setup @{binding hypsubst}
(Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac ctxt)))
"substitution using an assumption (improper)" #>
+ Method.setup @{binding hypsubst_thin}
+ (Scan.succeed (fn ctxt => SIMPLE_METHOD'
+ (CHANGED_PROP o hyp_subst_tac_thin true ctxt)))
+ "substitution using an assumption, eliminating assumptions" #>
+ hyp_subst_thins_setup #>
Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th))))
"simple substitution";
--- a/src/ZF/Coind/ECR.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/ZF/Coind/ECR.thy Thu Jul 03 14:40:36 2014 +0200
@@ -100,6 +100,7 @@
<cl,t> \<in> HasTyRel"
apply (unfold hastyenv_def)
apply (erule elab_fixE, safe)
+apply hypsubst_thin
apply (rule subst, assumption)
apply (rule_tac te="te_owr(te, f, t_fun(t1, t2))" in htr_closCI)
apply simp_all
--- a/src/ZF/Induct/Multiset.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/ZF/Induct/Multiset.thy Thu Jul 03 14:40:36 2014 +0200
@@ -931,6 +931,7 @@
apply (rule_tac x = M0 in exI, force)
(* Subgoal 2 *)
apply clarify
+apply hypsubst_thin
apply (case_tac "a \<in> mset_of (Ka) ")
apply (rule_tac x = I in exI, simp (no_asm_simp))
apply (rule_tac x = J in exI, simp (no_asm_simp))
--- a/src/ZF/Int_ZF.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/ZF/Int_ZF.thy Thu Jul 03 14:40:36 2014 +0200
@@ -661,7 +661,7 @@
apply (simp add: zless_def znegative_def zdiff_def int_def)
apply (auto dest!: less_imp_succ_add simp add: zadd zminus int_of_def)
apply (rule_tac x = k in bexI)
-apply (erule add_left_cancel, auto)
+apply (erule_tac i="succ (?v)" in add_left_cancel, auto)
done
lemma zless_imp_succ_zadd:
@@ -703,6 +703,7 @@
apply (rule_tac x = "y1#+y2" in exI)
apply (auto simp add: add_lt_mono)
apply (rule sym)
+apply hypsubst_thin
apply (erule add_left_cancel)+
apply auto
done
--- a/src/ZF/ex/LList.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/ZF/ex/LList.thy Thu Jul 03 14:40:36 2014 +0200
@@ -173,7 +173,7 @@
apply (rule_tac X = "{<l,l>. l \<in> llist (A) }" in lleq.coinduct)
apply blast
apply safe
-apply (erule_tac a=l in llist.cases, fast+)
+apply (erule_tac a=la in llist.cases, fast+)
done
--- a/src/ZF/ex/Primes.thy Thu Jul 03 09:55:16 2014 +0200
+++ b/src/ZF/ex/Primes.thy Thu Jul 03 14:40:36 2014 +0200
@@ -71,7 +71,7 @@
lemma dvd_mult_right: "[|(i#*j) dvd k; j \<in> nat|] ==> j dvd k"
apply (simp add: divides_def, clarify)
-apply (rule_tac x = "i#*k" in bexI)
+apply (rule_tac x = "i#*ka" in bexI)
apply (simp add: mult_ac)
apply (rule mult_type)
done