--- a/src/CCL/CCL.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/CCL/CCL.thy Mon Mar 23 21:14:49 2015 +0100
@@ -476,7 +476,7 @@
method_setup eq_coinduct3 = {*
Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt =>
SIMPLE_METHOD'
- (Rule_Insts.res_inst_tac ctxt [((("R", 0), Position.none), s)] @{thm eq_coinduct3}))
+ (Rule_Insts.res_inst_tac ctxt [((("R", 0), Position.none), s)] [] @{thm eq_coinduct3}))
*}
--- a/src/CCL/Wfd.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/CCL/Wfd.thy Mon Mar 23 21:14:49 2015 +0100
@@ -49,7 +49,7 @@
method_setup wfd_strengthen = {*
Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt =>
SIMPLE_METHOD' (fn i =>
- Rule_Insts.res_inst_tac ctxt [((("Q", 0), Position.none), s)] @{thm wfd_strengthen_lemma} i
+ Rule_Insts.res_inst_tac ctxt [((("Q", 0), Position.none), s)] [] @{thm wfd_strengthen_lemma} i
THEN assume_tac ctxt (i + 1)))
*}
@@ -448,7 +448,7 @@
in
fun rcall_tac ctxt i =
- let fun tac ps rl i = Rule_Insts.res_inst_tac ctxt ps rl i THEN atac i
+ let fun tac ps rl i = Rule_Insts.res_inst_tac ctxt ps [] rl i THEN atac i
in IHinst tac @{thms rcallTs} i end
THEN eresolve_tac ctxt @{thms rcall_lemmas} i
@@ -468,7 +468,7 @@
(*** Clean up Correctness Condictions ***)
fun clean_ccs_tac ctxt =
- let fun tac ps rl i = Rule_Insts.eres_inst_tac ctxt ps rl i THEN atac i in
+ let fun tac ps rl i = Rule_Insts.eres_inst_tac ctxt ps [] rl i THEN atac i in
TRY (REPEAT_FIRST (IHinst tac @{thms hyprcallTs} ORELSE'
eresolve_tac ctxt ([asm_rl, @{thm SubtypeE}] @ @{thms rmIHs}) ORELSE'
hyp_subst_tac ctxt))
--- a/src/CTT/CTT.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/CTT/CTT.thy Mon Mar 23 21:14:49 2015 +0100
@@ -422,15 +422,15 @@
fun NE_tac ctxt sp i =
TRY (rtac @{thm EqE} i) THEN
- Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), sp)] @{thm NE} i
+ Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), sp)] [] @{thm NE} i
fun SumE_tac ctxt sp i =
TRY (rtac @{thm EqE} i) THEN
- Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), sp)] @{thm SumE} i
+ Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), sp)] [] @{thm SumE} i
fun PlusE_tac ctxt sp i =
TRY (rtac @{thm EqE} i) THEN
- Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), sp)] @{thm PlusE} i
+ Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), sp)] [] @{thm PlusE} i
(** Predicate logic reasoning, WITH THINNING!! Procedures adapted from NJ. **)
--- a/src/Doc/Implementation/Tactic.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/Doc/Implementation/Tactic.thy Mon Mar 23 21:14:49 2015 +0100
@@ -395,15 +395,21 @@
text %mlref \<open>
\begin{mldecls}
@{index_ML Rule_Insts.res_inst_tac: "Proof.context ->
- ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\
+ ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list ->
+ thm -> int -> tactic"} \\
@{index_ML Rule_Insts.eres_inst_tac: "Proof.context ->
- ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\
+ ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list ->
+ thm -> int -> tactic"} \\
@{index_ML Rule_Insts.dres_inst_tac: "Proof.context ->
- ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\
+ ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list ->
+ thm -> int -> tactic"} \\
@{index_ML Rule_Insts.forw_inst_tac: "Proof.context ->
- ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\
- @{index_ML Rule_Insts.subgoal_tac: "Proof.context -> string -> int -> tactic"} \\
- @{index_ML Rule_Insts.thin_tac: "Proof.context -> string -> int -> tactic"} \\
+ ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list ->
+ thm -> int -> tactic"} \\
+ @{index_ML Rule_Insts.subgoal_tac: "Proof.context -> string ->
+ (binding * string option * mixfix) list -> int -> tactic"} \\
+ @{index_ML Rule_Insts.thin_tac: "Proof.context -> string ->
+ (binding * string option * mixfix) list -> int -> tactic"} \\
@{index_ML rename_tac: "string list -> int -> tactic"} \\
\end{mldecls}
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Mon Mar 23 21:14:49 2015 +0100
@@ -44,8 +44,7 @@
@{rail \<open>
(@@{command chapter} | @@{command section} | @@{command subsection} |
- @@{command subsubsection} | @@{command text} | @@{command txt})
- @{syntax target}? @{syntax text}
+ @@{command subsubsection} | @@{command text} | @@{command txt}) @{syntax text}
;
@@{command text_raw} @{syntax text}
\<close>}
@@ -74,7 +73,7 @@
Except for @{command "text_raw"}, the text passed to any of the above
markup commands may refer to formal entities via \emph{document
antiquotations}, see also \secref{sec:antiq}. These are interpreted in the
- present theory or proof context, or the named @{text "target"}.
+ present theory or proof context.
\medskip The proof markup commands closely resemble those for theory
specifications, but have a different formal status and produce
--- a/src/Doc/Isar_Ref/Generic.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/Doc/Isar_Ref/Generic.thy Mon Mar 23 21:14:49 2015 +0100
@@ -300,19 +300,20 @@
@{rail \<open>
(@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
- @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goal_spec}? \<newline>
+ @@{method frule_tac} | @@{method cut_tac}) @{syntax goal_spec}? \<newline>
( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} )
;
- @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +)
+ dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and') @{syntax for_fixes}
+ ;
+ @@{method thin_tac} @{syntax goal_spec}? @{syntax prop} @{syntax for_fixes}
+ ;
+ @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +) @{syntax for_fixes}
;
@@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +)
;
@@{method rotate_tac} @{syntax goal_spec}? @{syntax int}?
;
(@@{method tactic} | @@{method raw_tactic}) @{syntax text}
- ;
-
- dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and')
\<close>}
\begin{description}
@@ -480,7 +481,7 @@
\begin{center}
\small
- \begin{supertabular}{|l|l|p{0.3\textwidth}|}
+ \begin{tabular}{|l|l|p{0.3\textwidth}|}
\hline
Isar method & ML tactic & behavior \\\hline
@@ -503,7 +504,7 @@
mode: an assumption is only used for simplifying assumptions which
are to the right of it \\\hline
- \end{supertabular}
+ \end{tabular}
\end{center}
\<close>
@@ -997,11 +998,10 @@
the Simplifier loop! Note that a version of this simplification
procedure is already active in Isabelle/HOL.\<close>
-simproc_setup unit ("x::unit") = \<open>
- fn _ => fn _ => fn ct =>
+simproc_setup unit ("x::unit") =
+ \<open>fn _ => fn _ => fn ct =>
if HOLogic.is_unit (Thm.term_of ct) then NONE
- else SOME (mk_meta_eq @{thm unit_eq})
-\<close>
+ else SOME (mk_meta_eq @{thm unit_eq})\<close>
text \<open>Since the Simplifier applies simplification procedures
frequently, it is important to make the failure check in ML
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Mon Mar 23 21:14:49 2015 +0100
@@ -100,9 +100,8 @@
@{rail \<open>
(@@{command (HOL) inductive} | @@{command (HOL) inductive_set} |
@@{command (HOL) coinductive} | @@{command (HOL) coinductive_set})
- @{syntax target}? \<newline>
- @{syntax "fixes"} (@'for' @{syntax "fixes"})? (@'where' clauses)? \<newline>
- (@'monos' @{syntax thmrefs})?
+ @{syntax "fixes"} @{syntax "for_fixes"} \<newline>
+ (@'where' clauses)? (@'monos' @{syntax thmrefs})?
;
clauses: (@{syntax thmdecl}? @{syntax prop} + '|')
;
@@ -266,9 +265,9 @@
\end{matharray}
@{rail \<open>
- @@{command (HOL) primrec} @{syntax target}? @{syntax "fixes"} @'where' equations
+ @@{command (HOL) primrec} @{syntax "fixes"} @'where' equations
;
- (@@{command (HOL) fun} | @@{command (HOL) function}) @{syntax target}? functionopts?
+ (@@{command (HOL) fun} | @@{command (HOL) function}) functionopts?
@{syntax "fixes"} \<newline> @'where' equations
;
@@ -322,7 +321,7 @@
command can then be used to establish that the function is total.
\item @{command (HOL) "fun"} is a shorthand notation for ``@{command
- (HOL) "function"}~@{text "(sequential)"}, followed by automated
+ (HOL) "function"}~@{text "(sequential)"}'', followed by automated
proof attempts regarding pattern matching and termination. See
@{cite "isabelle-function"} for further details.
@@ -575,8 +574,7 @@
\end{matharray}
@{rail \<open>
- @@{command (HOL) partial_function} @{syntax target}?
- '(' @{syntax nameref} ')' @{syntax "fixes"} \<newline>
+ @@{command (HOL) partial_function} '(' @{syntax nameref} ')' @{syntax "fixes"} \<newline>
@'where' @{syntax thmdecl}? @{syntax prop}
\<close>}
@@ -1592,25 +1590,25 @@
\end{matharray}
@{rail \<open>
- @@{command (HOL) setup_lifting} \<newline>
- @{syntax thmref} @{syntax thmref}? (@'parametric' @{syntax thmref})?;
+ @@{command (HOL) setup_lifting} @{syntax thmref} @{syntax thmref}? \<newline>
+ (@'parametric' @{syntax thmref})?
\<close>}
@{rail \<open>
@@{command (HOL) lift_definition} @{syntax name} '::' @{syntax type} @{syntax mixfix}? \<newline>
- 'is' @{syntax term} (@'parametric' (@{syntax thmref}+))?;
+ 'is' @{syntax term} (@'parametric' (@{syntax thmref}+))?
\<close>}
@{rail \<open>
- @@{command (HOL) lifting_forget} @{syntax nameref};
+ @@{command (HOL) lifting_forget} @{syntax nameref}
\<close>}
@{rail \<open>
- @@{command (HOL) lifting_update} @{syntax nameref};
+ @@{command (HOL) lifting_update} @{syntax nameref}
\<close>}
@{rail \<open>
- @@{attribute (HOL) lifting_restore} @{syntax thmref} (@{syntax thmref} @{syntax thmref})?;
+ @@{attribute (HOL) lifting_restore} @{syntax thmref} (@{syntax thmref} @{syntax thmref})?
\<close>}
\begin{description}
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Mon Mar 23 21:14:49 2015 +0100
@@ -521,10 +521,10 @@
entities within the current context.
@{rail \<open>
- (@@{command type_notation} | @@{command no_type_notation}) @{syntax target}?
- @{syntax mode}? \<newline> (@{syntax nameref} @{syntax mixfix} + @'and')
+ (@@{command type_notation} | @@{command no_type_notation}) @{syntax mode}? \<newline>
+ (@{syntax nameref} @{syntax mixfix} + @'and')
;
- (@@{command notation} | @@{command no_notation}) @{syntax target}? @{syntax mode}? \<newline>
+ (@@{command notation} | @@{command no_notation}) @{syntax mode}? \<newline>
(@{syntax nameref} @{syntax mixfix} + @'and')
;
@@{command write} @{syntax mode}? (@{syntax nameref} @{syntax mixfix} + @'and')
@@ -1165,6 +1165,8 @@
@{attribute_def syntax_ast_stats} & : & @{text attribute} & default @{text false} \\
\end{tabular}
+ \medskip
+
Unlike mixfix notation for existing formal entities
(\secref{sec:notation}), raw syntax declarations provide full access
to the priority grammar of the inner syntax, without any sanity
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Mon Mar 23 21:14:49 2015 +0100
@@ -352,7 +352,20 @@
another level of iteration, with explicit @{keyword_ref "and"}
separators; e.g.\ see @{command "fix"} and @{command "assume"} in
\secref{sec:proof-context}.
-\<close>
+
+ @{rail \<open>
+ @{syntax_def "fixes"}:
+ ((@{syntax name} ('::' @{syntax type})? @{syntax mixfix}? | @{syntax vars}) + @'and')
+ ;
+ @{syntax_def "for_fixes"}: (@'for' @{syntax "fixes"})?
+ \<close>}
+
+ The category @{syntax "fixes"} is a richer variant of @{syntax vars}: it
+ admits specification of mixfix syntax for the entities that are introduced
+ into the context. An optional suffix ``@{keyword "for"}~@{text "fixes"}''
+ is admitted in many situations to indicate a so-called ``eigen-context''
+ of a formal element: the result will be exported and thus generalized over
+ the given variables.\<close>
subsection \<open>Attributes and theorems \label{sec:syn-att}\<close>
--- a/src/Doc/Isar_Ref/Proof.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/Doc/Isar_Ref/Proof.thy Mon Mar 23 21:14:49 2015 +0100
@@ -184,7 +184,7 @@
\<phi>[t]"}.
@{rail \<open>
- @@{command fix} (@{syntax vars} + @'and')
+ @@{command fix} @{syntax "fixes"}
;
(@@{command assume} | @@{command presume}) (@{syntax props} + @'and')
;
@@ -432,7 +432,7 @@
@{rail \<open>
(@@{command lemma} | @@{command theorem} | @@{command corollary} |
@@{command schematic_lemma} | @@{command schematic_theorem} |
- @@{command schematic_corollary}) @{syntax target}? (goal | longgoal)
+ @@{command schematic_corollary}) (goal | statement)
;
(@@{command have} | @@{command show} | @@{command hence} | @@{command thus}) goal
;
@@ -441,7 +441,8 @@
goal: (@{syntax props} + @'and')
;
- longgoal: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} * ) conclusion
+ statement: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} *) \<newline>
+ conclusion
;
conclusion: @'shows' goal | @'obtains' (@{syntax parname}? case + '|')
;
@@ -737,13 +738,11 @@
;
@@{attribute OF} @{syntax thmrefs}
;
- @@{attribute of} @{syntax insts} ('concl' ':' @{syntax insts})? \<newline>
- (@'for' (@{syntax vars} + @'and'))?
+ @@{attribute of} @{syntax insts} ('concl' ':' @{syntax insts})? @{syntax for_fixes}
;
@@{attribute "where"}
((@{syntax name} | @{syntax var} | @{syntax typefree} | @{syntax typevar}) '='
- (@{syntax type} | @{syntax term}) * @'and') \<newline>
- (@'for' (@{syntax vars} + @'and'))?
+ (@{syntax type} | @{syntax term}) * @'and') \<newline> @{syntax for_fixes}
\<close>}
\begin{description}
@@ -935,8 +934,7 @@
\end{matharray}
@{rail \<open>
- @@{command method_setup} @{syntax target}?
- @{syntax name} '=' @{syntax text} @{syntax text}?
+ @@{command method_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
\<close>}
\begin{description}
--- a/src/Doc/Isar_Ref/Spec.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy Mon Mar 23 21:14:49 2015 +0100
@@ -4,21 +4,18 @@
chapter \<open>Specifications\<close>
-text \<open>
- The Isabelle/Isar theory format integrates specifications and
- proofs, supporting interactive development with unlimited undo
- operation. There is an integrated document preparation system (see
- \chref{ch:document-prep}), for typesetting formal developments
- together with informal text. The resulting hyper-linked PDF
- documents can be used both for WWW presentation and printed copies.
+text \<open>The Isabelle/Isar theory format integrates specifications and proofs,
+ with support for interactive development by continuous document editing.
+ There is a separate document preparation system (see
+ \chref{ch:document-prep}), for typesetting formal developments together
+ with informal text. The resulting hyper-linked PDF documents can be used
+ both for WWW presentation and printed copies.
The Isar proof language (see \chref{ch:proofs}) is embedded into the
theory language as a proper sub-language. Proof mode is entered by
stating some @{command theorem} or @{command lemma} at the theory
level, and left again with the final conclusion (e.g.\ via @{command
- qed}). Some theory specification mechanisms also require a proof,
- such as @{command typedef} in HOL, which demands non-emptiness of
- the representing sets.
+ qed}).
\<close>
@@ -30,28 +27,36 @@
@{command_def (global) "end"} & : & @{text "theory \<rightarrow> toplevel"} \\
\end{matharray}
- Isabelle/Isar theories are defined via theory files, which may
- contain both specifications and proofs; occasionally definitional
- mechanisms also require some explicit proof. The theory body may be
- sub-structured by means of \emph{local theory targets}, such as
- @{command "locale"} and @{command "class"}.
+ Isabelle/Isar theories are defined via theory files, which consist of an
+ outermost sequence of definition--statement--proof elements. Some
+ definitions are self-sufficient (e.g.\ @{command fun} in Isabelle/HOL),
+ with foundational proofs performed internally. Other definitions require
+ an explicit proof as justification (e.g.\ @{command function} and
+ @{command termination} in Isabelle/HOL). Plain statements like @{command
+ theorem} or @{command lemma} are merely a special case of that, defining a
+ theorem from a given proposition and its proof.
- The first proper command of a theory is @{command "theory"}, which
- indicates imports of previous theories and optional dependencies on
- other source files (usually in ML). Just preceding the initial
- @{command "theory"} command there may be an optional @{command
- "header"} declaration, which is only relevant to document
- preparation: see also the other section markup commands in
- \secref{sec:markup}.
+ The theory body may be sub-structured by means of \emph{local theory
+ targets}, such as @{command "locale"} and @{command "class"}. It is also
+ possible to use @{command context}~@{keyword "begin"}~\dots~@{command end}
+ blocks to delimited a local theory context: a \emph{named context} to
+ augment a locale or class specification, or an \emph{unnamed context} to
+ refer to local parameters and assumptions that are discharged later. See
+ \secref{sec:target} for more details.
- A theory is concluded by a final @{command (global) "end"} command,
- one that does not belong to a local theory target. No further
- commands may follow such a global @{command (global) "end"},
- although some user-interfaces might pretend that trailing input is
- admissible.
+ \medskip A theory is commenced by the @{command "theory"} command, which
+ indicates imports of previous theories, according to an acyclic
+ foundational order. Before the initial @{command "theory"} command, there
+ may be optional document header material (like @{command section} or
+ @{command text}, see \secref{sec:markup}). The document header is outside
+ of the formal theory context, though.
+
+ A theory is concluded by a final @{command (global) "end"} command, one
+ that does not belong to a local theory target. No further commands may
+ follow such a global @{command (global) "end"}.
@{rail \<open>
- @@{command theory} @{syntax name} imports keywords? \<newline> @'begin'
+ @@{command theory} @{syntax name} imports? keywords? \<newline> @'begin'
;
imports: @'imports' (@{syntax name} +)
;
@@ -72,6 +77,11 @@
up-to-date: changed files are automatically rechecked whenever a
theory header specification is processed.
+ Empty imports are only allowed in the bootstrap process of the special
+ theory @{theory Pure}, which is the start of any other formal development
+ based on Isabelle. Regular user theories usually refer to some more
+ complex entry point, such as theory @{theory Main} in Isabelle/HOL.
+
The optional @{keyword_def "keywords"} specification declares outer
syntax (\chref{ch:outer-syntax}) that is introduced in this theory
later on (rare in end-user applications). Both minor keywords and
@@ -85,8 +95,8 @@
with and without proof, respectively. Additional @{syntax tags}
provide defaults for document preparation (\secref{sec:tags}).
- It is possible to specify an alternative completion via @{text "==
- text"}, while the default is the corresponding keyword name.
+ It is possible to specify an alternative completion via @{verbatim
+ "=="}~@{text "text"}, while the default is the corresponding keyword name.
\item @{command (global) "end"} concludes the current theory
definition. Note that some other commands, e.g.\ local theory
@@ -106,9 +116,9 @@
@{command_def (local) "end"} & : & @{text "local_theory \<rightarrow> theory"} \\
\end{matharray}
- A local theory target is a context managed separately within the
- enclosing theory. Contexts may introduce parameters (fixed
- variables) and assumptions (hypotheses). Definitions and theorems
+ A local theory target is a specification context that is managed
+ separately within the enclosing theory. Contexts may introduce parameters
+ (fixed variables) and assumptions (hypotheses). Definitions and theorems
depending on the context may be added incrementally later on.
\emph{Named contexts} refer to locales (cf.\ \secref{sec:locale}) or
@@ -150,20 +160,24 @@
(global) "end"} has a different meaning: it concludes the theory
itself (\secref{sec:begin-thy}).
- \item @{text "("}@{keyword_def "in"}~@{text "c)"} given after any
- local theory command specifies an immediate target, e.g.\
- ``@{command "definition"}~@{text "(\<IN> c) \<dots>"}'' or ``@{command
- "theorem"}~@{text "(\<IN> c) \<dots>"}''. This works both in a local or
- global theory context; the current target context will be suspended
- for this command only. Note that ``@{text "(\<IN> -)"}'' will
- always produce a global result independently of the current target
- context.
+ \item @{text "("}@{keyword_def "in"}~@{text "c)"} given after any local
+ theory command specifies an immediate target, e.g.\ ``@{command
+ "definition"}~@{text "(\<IN> c)"}'' or ``@{command "theorem"}~@{text
+ "(\<IN> c)"}''. This works both in a local or global theory context; the
+ current target context will be suspended for this command only. Note that
+ ``@{text "(\<IN> -)"}'' will always produce a global result independently
+ of the current target context.
\end{description}
- The exact meaning of results produced within a local theory context
- depends on the underlying target infrastructure (locale, type class
- etc.). The general idea is as follows, considering a context named
+ Any specification element that operates on @{text local_theory} according
+ to this manual implicitly allows the above target syntax @{text
+ "("}@{keyword "in"}~@{text "c)"}, but individual syntax diagrams omit that
+ aspect for clarity.
+
+ \medskip The exact meaning of results produced within a local theory
+ context depends on the underlying target infrastructure (locale, type
+ class etc.). The general idea is as follows, considering a context named
@{text c} with parameter @{text x} and assumption @{text "A[x]"}.
Definitions are exported by introducing a global version with
@@ -178,11 +192,7 @@
generalizing the parameters of the context. For example, @{text "a:
B[x]"} becomes @{text "c.a: A[?x] \<Longrightarrow> B[?x]"}, again for arbitrary
@{text "?x"}.
-
- \medskip The Isabelle/HOL library contains numerous applications of
- locales and classes, e.g.\ see @{file "~~/src/HOL/Algebra"}. An
- example for an unnamed auxiliary contexts is given in @{file
- "~~/src/HOL/Isar_Examples/Group_Context.thy"}.\<close>
+\<close>
section \<open>Bundled declarations \label{sec:bundle}\<close>
@@ -211,8 +221,7 @@
locale interpretation (\secref{sec:locale}).
@{rail \<open>
- @@{command bundle} @{syntax target}? \<newline>
- @{syntax name} '=' @{syntax thmrefs} (@'for' (@{syntax vars} + @'and'))?
+ @@{command bundle} @{syntax name} '=' @{syntax thmrefs} @{syntax for_fixes}
;
(@@{command include} | @@{command including}) (@{syntax nameref}+)
;
@@ -274,10 +283,9 @@
``abbreviation''.
@{rail \<open>
- @@{command definition} @{syntax target}? \<newline>
- (decl @'where')? @{syntax thmdecl}? @{syntax prop}
+ @@{command definition} (decl @'where')? @{syntax thmdecl}? @{syntax prop}
;
- @@{command abbreviation} @{syntax target}? @{syntax mode}? \<newline>
+ @@{command abbreviation} @{syntax mode}? \<newline>
(decl @'where')? @{syntax prop}
;
@@ -337,10 +345,6 @@
@{rail \<open>
@@{command axiomatization} @{syntax "fixes"}? (@'where' specs)?
;
-
- @{syntax_def "fixes"}: ((@{syntax name} ('::' @{syntax type})?
- @{syntax mixfix}? | @{syntax vars}) + @'and')
- ;
specs: (@{syntax thmdecl}? @{syntax props} + @'and')
\<close>}
@@ -389,9 +393,9 @@
@{rail \<open>
(@@{command declaration} | @@{command syntax_declaration})
- ('(' @'pervasive' ')')? \<newline> @{syntax target}? @{syntax text}
+ ('(' @'pervasive' ')')? \<newline> @{syntax text}
;
- @@{command declare} @{syntax target}? (@{syntax thmrefs} + @'and')
+ @@{command declare} (@{syntax thmrefs} + @'and')
\<close>}
\begin{description}
@@ -455,7 +459,7 @@
omitted according to roundup.
@{rail \<open>
- @{syntax_def locale_expr}: (instance + '+') (@'for' (@{syntax "fixes"} + @'and'))?
+ @{syntax_def locale_expr}: (instance + '+') @{syntax for_fixes}
;
instance: (qualifier ':')? @{syntax nameref} (pos_insts | named_insts)
;
@@ -515,7 +519,7 @@
@{syntax locale_expr} ('+' (@{syntax context_elem}+))?
;
@{syntax_def context_elem}:
- @'fixes' (@{syntax "fixes"} + @'and') |
+ @'fixes' @{syntax "fixes"} |
@'constrains' (@{syntax name} '::' @{syntax type} + @'and') |
@'assumes' (@{syntax props} + @'and') |
@'defines' (@{syntax thmdecl}? @{syntax prop} @{syntax prop_pat}? + @'and') |
@@ -913,7 +917,7 @@
@@{command instance} (() | (@{syntax nameref} + @'and') '::' @{syntax arity} |
@{syntax nameref} ('<' | '\<subseteq>') @{syntax nameref} )
;
- @@{command subclass} @{syntax target}? @{syntax nameref}
+ @@{command subclass} @{syntax nameref}
;
@@{command class_deps} ( ( @{syntax sort} | ( '(' ( @{syntax sort} + @'|' ) ')' ) ) \<newline>
( @{syntax sort} | ( '(' ( @{syntax sort} + @'|' ) ')' ) )? )?
@@ -1133,8 +1137,7 @@
(@@{command ML} | @@{command ML_prf} | @@{command ML_val} |
@@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text}
;
- @@{command attribute_setup} @{syntax target}?
- @{syntax name} '=' @{syntax text} @{syntax text}?
+ @@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
\<close>}
\begin{description}
@@ -1398,12 +1401,10 @@
\end{matharray}
@{rail \<open>
- (@@{command lemmas} | @@{command theorems}) @{syntax target}? \<newline>
- (@{syntax thmdef}? @{syntax thmrefs} + @'and')
- (@'for' (@{syntax vars} + @'and'))?
+ (@@{command lemmas} | @@{command theorems}) (@{syntax thmdef}? @{syntax thmrefs} + @'and')
+ @{syntax for_fixes}
;
- @@{command named_theorems} @{syntax target}?
- (@{syntax name} @{syntax text}? + @'and')
+ @@{command named_theorems} (@{syntax name} @{syntax text}? + @'and')
\<close>}
\begin{description}
--- a/src/Doc/Tutorial/Protocol/Message.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/Doc/Tutorial/Protocol/Message.thy Mon Mar 23 21:14:49 2015 +0100
@@ -856,7 +856,8 @@
(EVERY
[ (*push in occurrences of X...*)
(REPEAT o CHANGED)
- (Rule_Insts.res_inst_tac ctxt [((("x", 1), Position.none), "X")] (insert_commute RS ssubst) 1),
+ (Rule_Insts.res_inst_tac ctxt [((("x", 1), Position.none), "X")] []
+ (insert_commute RS ssubst) 1),
(*...allowing further simplifications*)
simp_tac ctxt 1,
REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])),
--- a/src/FOL/FOL.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/FOL/FOL.thy Mon Mar 23 21:14:49 2015 +0100
@@ -66,13 +66,13 @@
done
ML {*
- fun case_tac ctxt a =
- Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), a)] @{thm case_split}
+ fun case_tac ctxt a fixes =
+ Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), a)] fixes @{thm case_split}
*}
method_setup case_tac = {*
- Args.goal_spec -- Scan.lift Args.name_inner_syntax >>
- (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s))
+ Args.goal_spec -- Scan.lift (Args.name_inner_syntax -- Parse.for_fixes) >>
+ (fn (quant, (s, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s fixes))
*} "case_tac emulation (dynamic instantiation!)"
--- a/src/HOL/Auth/Message.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/HOL/Auth/Message.thy Mon Mar 23 21:14:49 2015 +0100
@@ -866,7 +866,8 @@
(EVERY
[ (*push in occurrences of X...*)
(REPEAT o CHANGED)
- (Rule_Insts.res_inst_tac ctxt [((("x", 1), Position.none), "X")] (insert_commute RS ssubst) 1),
+ (Rule_Insts.res_inst_tac ctxt [((("x", 1), Position.none), "X")] []
+ (insert_commute RS ssubst) 1),
(*...allowing further simplifications*)
simp_tac ctxt 1,
REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])),
--- a/src/HOL/Bali/WellType.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/HOL/Bali/WellType.thy Mon Mar 23 21:14:49 2015 +0100
@@ -660,10 +660,10 @@
(* 17 subgoals *)
apply (tactic {* ALLGOALS (fn i =>
if i = 11 then EVERY'
- [Rule_Insts.thin_tac @{context} "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean",
- Rule_Insts.thin_tac @{context} "?E,dt\<Turnstile>e1\<Colon>-?T1",
- Rule_Insts.thin_tac @{context} "?E,dt\<Turnstile>e2\<Colon>-?T2"] i
- else Rule_Insts.thin_tac @{context} "All ?P" i) *})
+ [Rule_Insts.thin_tac @{context} "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean" [],
+ Rule_Insts.thin_tac @{context} "?E,dt\<Turnstile>e1\<Colon>-?T1" [],
+ Rule_Insts.thin_tac @{context} "?E,dt\<Turnstile>e2\<Colon>-?T2" []] i
+ else Rule_Insts.thin_tac @{context} "All ?P" [] i) *})
(*apply (safe del: disjE elim!: wt_elim_cases)*)
apply (tactic {*ALLGOALS (eresolve_tac @{context} @{thms wt_elim_cases})*})
apply (simp_all (no_asm_use) split del: split_if_asm)
--- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Mon Mar 23 21:14:49 2015 +0100
@@ -1081,7 +1081,7 @@
ML {*
fun Seq_case_tac ctxt s i =
- Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] @{thm Seq_cases} i
+ Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] [] @{thm Seq_cases} i
THEN hyp_subst_tac ctxt i THEN hyp_subst_tac ctxt (i+1) THEN hyp_subst_tac ctxt (i+2);
(* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *)
@@ -1093,7 +1093,7 @@
(* rws are definitions to be unfolded for admissibility check *)
fun Seq_induct_tac ctxt s rws i =
- Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] @{thm Seq_induct} i
+ Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] [] @{thm Seq_induct} i
THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt (i+1))))
THEN simp_tac (ctxt addsimps rws) i;
@@ -1102,12 +1102,12 @@
THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt i)));
fun pair_tac ctxt s =
- Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), s)] @{thm PairE}
+ Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), s)] [] @{thm PairE}
THEN' hyp_subst_tac ctxt THEN' asm_full_simp_tac ctxt;
(* induction on a sequence of pairs with pairsplitting and simplification *)
fun pair_induct_tac ctxt s rws i =
- Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] @{thm Seq_induct} i
+ Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] [] @{thm Seq_induct} i
THEN pair_tac ctxt "a" (i+3)
THEN (REPEAT_DETERM (CHANGED (simp_tac ctxt (i+1))))
THEN simp_tac (ctxt addsimps rws) i;
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Mon Mar 23 15:08:02 2015 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Mon Mar 23 21:14:49 2015 +0100
@@ -135,7 +135,8 @@
val take_ss =
simpset_of (put_simpset HOL_ss @{context} addsimps (@{thm Rep_cfun_strict1} :: take_rews))
fun quant_tac ctxt i = EVERY
- (map (fn name => Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), name)] spec i) x_names)
+ (map (fn name =>
+ Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), name)] [] spec i) x_names)
(* FIXME: move this message to domain_take_proofs.ML *)
val is_finite = #is_finite take_info
@@ -182,7 +183,7 @@
asm_simp_tac (put_simpset take_ss ctxt) 1 THEN
(resolve_tac ctxt prems' THEN_ALL_NEW etac spec) 1
fun cases_tacs (cons, exhaust) =
- Rule_Insts.res_inst_tac ctxt [((("y", 0), Position.none), "x")] exhaust 1 ::
+ Rule_Insts.res_inst_tac ctxt [((("y", 0), Position.none), "x")] [] exhaust 1 ::
asm_simp_tac (put_simpset take_ss ctxt addsimps prems) 1 ::
map con_tac cons
val tacs = tacs1 @ maps cases_tacs (conss ~~ exhausts)
--- a/src/HOL/IMPP/Hoare.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/HOL/IMPP/Hoare.thy Mon Mar 23 21:14:49 2015 +0100
@@ -286,7 +286,7 @@
apply (blast) (* cut *)
apply (blast) (* weaken *)
apply (tactic {* ALLGOALS (EVERY'
- [REPEAT o Rule_Insts.thin_tac @{context} "hoare_derivs ?x ?y",
+ [REPEAT o Rule_Insts.thin_tac @{context} "hoare_derivs ?x ?y" [],
simp_tac @{context}, clarify_tac @{context}, REPEAT o smp_tac @{context} 1]) *})
apply (simp_all (no_asm_use) add: triple_valid_def2)
apply (intro strip, tactic "smp_tac @{context} 2 1", blast) (* conseq *)
--- a/src/HOL/NanoJava/Equivalence.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/HOL/NanoJava/Equivalence.thy Mon Mar 23 21:14:49 2015 +0100
@@ -105,8 +105,8 @@
apply (rule hoare_ehoare.induct)
(*18*)
apply (tactic {* ALLGOALS (REPEAT o dresolve_tac @{context} [@{thm all_conjunct2}, @{thm all3_conjunct2}]) *})
-apply (tactic {* ALLGOALS (REPEAT o Rule_Insts.thin_tac @{context} "hoare ?x ?y") *})
-apply (tactic {* ALLGOALS (REPEAT o Rule_Insts.thin_tac @{context} "ehoare ?x ?y") *})
+apply (tactic {* ALLGOALS (REPEAT o Rule_Insts.thin_tac @{context} "hoare ?x ?y" []) *})
+apply (tactic {* ALLGOALS (REPEAT o Rule_Insts.thin_tac @{context} "ehoare ?x ?y" []) *})
apply (simp_all only: cnvalid1_eq cenvalid_def2)
apply fast
apply fast
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Mon Mar 23 15:08:02 2015 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Mon Mar 23 21:14:49 2015 +0100
@@ -19,7 +19,7 @@
val ps = Logic.strip_params (Thm.term_of cgoal);
val Ts = map snd ps;
val tinst' = map (fn (t, u) =>
- (head_of (Logic.incr_indexes (Ts, j) t),
+ (head_of (Logic.incr_indexes ([], Ts, j) t),
fold_rev Term.abs ps u)) tinst;
val th' = instf
(map (apply2 (Thm.ctyp_of ctxt)) tyinst')
--- a/src/HOL/SET_Protocol/Message_SET.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/HOL/SET_Protocol/Message_SET.thy Mon Mar 23 21:14:49 2015 +0100
@@ -871,7 +871,8 @@
(EVERY
[ (*push in occurrences of X...*)
(REPEAT o CHANGED)
- (Rule_Insts.res_inst_tac ctxt [((("x", 1), Position.none), "X")] (insert_commute RS ssubst) 1),
+ (Rule_Insts.res_inst_tac ctxt [((("x", 1), Position.none), "X")] []
+ (insert_commute RS ssubst) 1),
(*...allowing further simplifications*)
simp_tac ctxt 1,
REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])),
--- a/src/HOL/TLA/TLA.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/HOL/TLA/TLA.thy Mon Mar 23 21:14:49 2015 +0100
@@ -300,15 +300,15 @@
fun merge_temp_box_tac ctxt i =
REPEAT_DETERM (EVERY [etac @{thm box_conjE_temp} i, atac i,
- Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "behavior")] @{thm box_thin} i])
+ Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "behavior")] [] @{thm box_thin} i])
fun merge_stp_box_tac ctxt i =
REPEAT_DETERM (EVERY [etac @{thm box_conjE_stp} i, atac i,
- Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "state")] @{thm box_thin} i])
+ Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "state")] [] @{thm box_thin} i])
fun merge_act_box_tac ctxt i =
REPEAT_DETERM (EVERY [etac @{thm box_conjE_act} i, atac i,
- Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "state * state")] @{thm box_thin} i])
+ Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "state * state")] [] @{thm box_thin} i])
*}
method_setup merge_box = {* Scan.succeed (K (SIMPLE_METHOD' merge_box_tac)) *}
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Mon Mar 23 21:14:49 2015 +0100
@@ -185,7 +185,7 @@
else
let
fun instantiate param =
- (map (Rule_Insts.eres_inst_tac ctxt [((("x", 0), Position.none), param)]) thms
+ (map (Rule_Insts.eres_inst_tac ctxt [((("x", 0), Position.none), param)] []) thms
|> FIRST')
val attempts = map instantiate parameters
in
@@ -221,7 +221,7 @@
else
let
fun instantiates param =
- Rule_Insts.eres_inst_tac ctxt [((("x", 0), Position.none), param)] thm
+ Rule_Insts.eres_inst_tac ctxt [((("x", 0), Position.none), param)] [] thm
val quantified_var = head_quantified_variable ctxt i st
in
@@ -427,7 +427,7 @@
fun instantiate_vars ctxt vars : tactic =
map (fn var =>
Rule_Insts.eres_inst_tac ctxt
- [((("x", 0), Position.none), var)] @{thm allE} 1)
+ [((("x", 0), Position.none), var)] [] @{thm allE} 1)
vars
|> EVERY
@@ -673,7 +673,7 @@
else
let
fun instantiate const_name =
- Rule_Insts.dres_inst_tac ctxt [((("sk", 0), Position.none), const_name ^ parameters)]
+ Rule_Insts.dres_inst_tac ctxt [((("sk", 0), Position.none), const_name ^ parameters)] []
@{thm leo2_skolemise}
val attempts = map instantiate candidate_consts
in
@@ -1556,7 +1556,7 @@
val tecs =
map (fn t_s => (* FIXME proper context!? *)
- Rule_Insts.eres_inst_tac @{context} [((("x", 0), Position.none), t_s)] @{thm allE}
+ Rule_Insts.eres_inst_tac @{context} [((("x", 0), Position.none), t_s)] [] @{thm allE}
THEN' atac)
in
(TRY o etac @{thm forall_pos_lift})
@@ -1735,7 +1735,7 @@
member (op =) (Term.add_frees hyp_body []) (hd hyp_prefix) then
no_tac st
else
- Rule_Insts.eres_inst_tac ctxt [((("x", 0), Position.none), "(@X. False)")]
+ Rule_Insts.eres_inst_tac ctxt [((("x", 0), Position.none), "(@X. False)")] []
@{thm allE} i st
end
end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Mon Mar 23 15:08:02 2015 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Mon Mar 23 21:14:49 2015 +0100
@@ -62,7 +62,7 @@
let
val ctxt = Proof_Context.init_global thy
val maxidx = fold (Term.maxidx_term o Thm.prop_of) intros ~1
- val pats = map (Logic.incr_indexes ([], maxidx + 1)) pats
+ val pats = map (Logic.incr_indexes ([], [], maxidx + 1)) pats
val (((pred, intros), pats), ctxt') = import (pred, intros) pats ctxt
val result_pats = map Var (fold_rev Term.add_vars pats [])
fun mk_fresh_name names =
--- a/src/HOL/UNITY/UNITY_tactics.ML Mon Mar 23 15:08:02 2015 +0100
+++ b/src/HOL/UNITY/UNITY_tactics.ML Mon Mar 23 21:14:49 2015 +0100
@@ -44,9 +44,9 @@
(*now there are two subgoals: co & transient*)
simp_tac (ctxt addsimps [@{thm mk_total_program_def}]) 2,
Rule_Insts.res_inst_tac ctxt
- [((("act", 0), Position.none), sact)] @{thm totalize_transientI} 2
+ [((("act", 0), Position.none), sact)] [] @{thm totalize_transientI} 2
ORELSE Rule_Insts.res_inst_tac ctxt
- [((("act", 0), Position.none), sact)] @{thm transientI} 2,
+ [((("act", 0), Position.none), sact)] [] @{thm transientI} 2,
(*simplify the command's domain*)
simp_tac (ctxt addsimps @{thms Domain_unfold}) 3,
constrains_tac ctxt 1,
--- a/src/LCF/LCF.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/LCF/LCF.thy Mon Mar 23 21:14:49 2015 +0100
@@ -321,7 +321,7 @@
method_setup induct = {*
Scan.lift Args.name_inner_syntax >> (fn v => fn ctxt =>
SIMPLE_METHOD' (fn i =>
- Rule_Insts.res_inst_tac ctxt [((("f", 0), Position.none), v)] @{thm induct} i THEN
+ Rule_Insts.res_inst_tac ctxt [((("f", 0), Position.none), v)] [] @{thm induct} i THEN
REPEAT (resolve_tac ctxt @{thms adm_lemmas} i)))
*}
@@ -381,7 +381,7 @@
ML {*
fun induct2_tac ctxt (f, g) i =
Rule_Insts.res_inst_tac ctxt
- [((("f", 0), Position.none), f), ((("g", 0), Position.none), g)] @{thm induct2} i THEN
+ [((("f", 0), Position.none), f), ((("g", 0), Position.none), g)] [] @{thm induct2} i THEN
REPEAT(resolve_tac ctxt @{thms adm_lemmas} i)
*}
--- a/src/Pure/Isar/code.ML Mon Mar 23 15:08:02 2015 +0100
+++ b/src/Pure/Isar/code.ML Mon Mar 23 21:14:49 2015 +0100
@@ -1084,7 +1084,7 @@
val args_of = snd o take_prefix is_Var o rev o snd o strip_comb
o map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of;
val args = args_of thm;
- val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1);
+ val incr_idx = Logic.incr_indexes ([], [], Thm.maxidx_of thm + 1);
fun matches_args args' =
let
val k = length args' - length args
--- a/src/Pure/Isar/parse.ML Mon Mar 23 15:08:02 2015 +0100
+++ b/src/Pure/Isar/parse.ML Mon Mar 23 21:14:49 2015 +0100
@@ -91,7 +91,6 @@
val const_decl: (string * string * mixfix) parser
val const_binding: (binding * string * mixfix) parser
val params: (binding * string option) list parser
- val simple_fixes: (binding * string option) list parser
val fixes: (binding * string option * mixfix) list parser
val for_fixes: (binding * string option * mixfix) list parser
val ML_source: Input.source parser
@@ -360,8 +359,6 @@
val params = Scan.repeat1 binding -- Scan.option ($$$ "::" |-- !!! typ)
>> (fn (xs, T) => map (rpair T) xs);
-val simple_fixes = and_list1 params >> flat;
-
val fixes =
and_list1 (binding -- Scan.option ($$$ "::" |-- typ) -- mixfix' >> (single o triple1) ||
params >> map (fn (x, y) => (x, y, NoSyn))) >> flat;
--- a/src/Pure/Isar/parse_spec.ML Mon Mar 23 15:08:02 2015 +0100
+++ b/src/Pure/Isar/parse_spec.ML Mon Mar 23 21:14:49 2015 +0100
@@ -132,8 +132,9 @@
val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
val obtain_case =
- Parse.parbinding -- (Scan.optional (Parse.simple_fixes --| Parse.where_) [] --
- (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat));
+ Parse.parbinding --
+ (Scan.optional (Parse.and_list1 Parse.params --| Parse.where_ >> flat) [] --
+ (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat));
val general_statement =
statement >> (fn x => ([], Element.Shows x)) ||
--- a/src/Pure/Proof/extraction.ML Mon Mar 23 15:08:02 2015 +0100
+++ b/src/Pure/Proof/extraction.ML Mon Mar 23 21:14:49 2015 +0100
@@ -101,7 +101,7 @@
get_first (fn (_, (prems, (tm1, tm2))) =>
let
fun ren t = the_default t (Term.rename_abs tm1 tm t);
- val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1);
+ val inc = Logic.incr_indexes ([], [], maxidx_of_term tm + 1);
val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm) (Vartab.empty, Vartab.empty);
val prems' = map (apply2 (Envir.subst_term env o inc o ren)) prems;
val env' = Envir.Envir
--- a/src/Pure/Tools/rule_insts.ML Mon Mar 23 15:08:02 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML Mon Mar 23 21:14:49 2015 +0100
@@ -14,20 +14,28 @@
val read_instantiate: Proof.context ->
((indexname * Position.T) * string) list -> string list -> thm -> thm
val res_inst_tac: Proof.context ->
- ((indexname * Position.T) * string) list -> thm -> int -> tactic
+ ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm ->
+ int -> tactic
val eres_inst_tac: Proof.context ->
- ((indexname * Position.T) * string) list -> thm -> int -> tactic
+ ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm ->
+ int -> tactic
val cut_inst_tac: Proof.context ->
- ((indexname * Position.T) * string) list -> thm -> int -> tactic
+ ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm ->
+ int -> tactic
val forw_inst_tac: Proof.context ->
- ((indexname * Position.T) * string) list -> thm -> int -> tactic
+ ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm ->
+ int -> tactic
val dres_inst_tac: Proof.context ->
- ((indexname * Position.T) * string) list -> thm -> int -> tactic
- val thin_tac: Proof.context -> string -> int -> tactic
- val subgoal_tac: Proof.context -> string -> int -> tactic
+ ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm ->
+ int -> tactic
+ val thin_tac: Proof.context -> string -> (binding * string option * mixfix) list ->
+ int -> tactic
+ val subgoal_tac: Proof.context -> string -> (binding * string option * mixfix) list ->
+ int -> tactic
val make_elim_preserve: Proof.context -> thm -> thm
val method:
- (Proof.context -> ((indexname * Position.T) * string) list -> thm -> int -> tactic) ->
+ (Proof.context -> ((indexname * Position.T) * string) list ->
+ (binding * string option * mixfix) list -> thm -> int -> tactic) ->
(Proof.context -> thm list -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
end;
@@ -124,15 +132,15 @@
fun where_rule ctxt mixed_insts fixes thm =
let
val ctxt' = ctxt
- |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2
- |> Variable.declare_thm thm;
+ |> Variable.declare_thm thm
+ |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2;
val (inst_tvars, inst_vars) = read_insts ctxt' mixed_insts thm;
in
thm
|> Drule.instantiate_normalize
(map (apply2 (Thm.ctyp_of ctxt) o apfst TVar) inst_tvars,
map (apply2 (Thm.cterm_of ctxt) o apfst Var) inst_vars)
- |> singleton (Proof_Context.export ctxt' ctxt)
+ |> singleton (Variable.export ctxt' ctxt)
|> Rule_Cases.save thm
end;
@@ -192,7 +200,7 @@
(* resolution after lifting and instantiation; may refer to parameters of the subgoal *)
-fun bires_inst_tac bires_flag ctxt mixed_insts thm i st = CSUBGOAL (fn (cgoal, _) =>
+fun bires_inst_tac bires_flag ctxt mixed_insts fixes thm i st = CSUBGOAL (fn (cgoal, _) =>
let
(* goal parameters *)
@@ -210,25 +218,32 @@
val paramTs = map #2 params;
- (* lift and instantiate rule *)
+ (* local fixes *)
+
+ val (fixed, fixes_ctxt) = param_ctxt
+ |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes;
- val (inst_tvars, inst_vars) = read_insts param_ctxt mixed_insts thm;
+ val (inst_tvars, inst_vars) = read_insts fixes_ctxt mixed_insts thm;
+
+
+ (* lift and instantiate rule *)
val inc = Thm.maxidx_of st + 1;
fun lift_var ((a, j), T) =
Var ((a, j + inc), paramTs ---> Logic.incr_tvar inc T);
fun lift_term t =
fold_rev Term.absfree (param_names ~~ paramTs)
- (Logic.incr_indexes (paramTs, inc) t);
+ (Logic.incr_indexes (fixed, paramTs, inc) t);
val inst_tvars' = inst_tvars
- |> map (apply2 (Thm.ctyp_of param_ctxt o Logic.incr_tvar inc) o apfst TVar);
+ |> map (apply2 (Thm.ctyp_of fixes_ctxt o Logic.incr_tvar inc) o apfst TVar);
val inst_vars' = inst_vars
- |> map (fn (v, t) => apply2 (Thm.cterm_of param_ctxt) (lift_var v, lift_term t));
+ |> map (fn (v, t) => apply2 (Thm.cterm_of fixes_ctxt) (lift_var v, lift_term t));
val thm' =
Drule.instantiate_normalize (inst_tvars', inst_vars')
- (Thm.lift_rule cgoal thm);
+ (Thm.lift_rule cgoal thm)
+ |> singleton (Variable.export fixes_ctxt param_ctxt);
in
compose_tac param_ctxt (bires_flag, thm', Thm.nprems_of thm) i
end) i st;
@@ -256,25 +271,27 @@
end;
(*instantiate and cut -- for atomic fact*)
-fun cut_inst_tac ctxt insts rule = res_inst_tac ctxt insts (make_elim_preserve ctxt rule);
+fun cut_inst_tac ctxt insts fixes rule =
+ res_inst_tac ctxt insts fixes (make_elim_preserve ctxt rule);
(*forward tactic applies a rule to an assumption without deleting it*)
-fun forw_inst_tac ctxt insts rule = cut_inst_tac ctxt insts rule THEN' assume_tac ctxt;
+fun forw_inst_tac ctxt insts fixes rule =
+ cut_inst_tac ctxt insts fixes rule THEN' assume_tac ctxt;
(*dresolve tactic applies a rule to replace an assumption*)
-fun dres_inst_tac ctxt insts rule = eres_inst_tac ctxt insts (make_elim_preserve ctxt rule);
+fun dres_inst_tac ctxt insts fixes rule =
+ eres_inst_tac ctxt insts fixes (make_elim_preserve ctxt rule);
(* derived tactics *)
(*deletion of an assumption*)
-fun thin_tac ctxt s =
- eres_inst_tac ctxt [((("V", 0), Position.none), s)] Drule.thin_rl;
+fun thin_tac ctxt s fixes =
+ eres_inst_tac ctxt [((("V", 0), Position.none), s)] fixes Drule.thin_rl;
(*Introduce the given proposition as lemma and subgoal*)
-fun subgoal_tac ctxt A =
- DETERM o res_inst_tac ctxt [((("psi", 0), Position.none), A)] cut_rl;
-
+fun subgoal_tac ctxt A fixes =
+ DETERM o res_inst_tac ctxt [((("psi", 0), Position.none), A)] fixes cut_rl;
(* method wrapper *)
@@ -282,14 +299,16 @@
fun method inst_tac tac =
Args.goal_spec --
Scan.optional (Scan.lift
- (Parse.and_list1 (Parse.position Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_inner_syntax))
- --| Args.$$$ "in")) [] --
+ (Parse.and_list1
+ (Parse.position Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_inner_syntax)) --
+ Parse.for_fixes --| Args.$$$ "in")) ([], []) --
Attrib.thms >>
- (fn ((quant, insts), thms) => fn ctxt => METHOD (fn facts =>
- if null insts then quant (Method.insert_tac facts THEN' tac ctxt thms)
+ (fn ((quant, (insts, fixes)), thms) => fn ctxt => METHOD (fn facts =>
+ if null insts andalso null fixes
+ then quant (Method.insert_tac facts THEN' tac ctxt thms)
else
(case thms of
- [thm] => quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm)
+ [thm] => quant (Method.insert_tac facts THEN' inst_tac ctxt insts fixes thm)
| _ => error "Cannot have instantiations with multiple rules")));
@@ -309,13 +328,13 @@
Method.setup @{binding cut_tac} (method cut_inst_tac (K cut_rules_tac))
"cut rule (dynamic instantiation)" #>
Method.setup @{binding subgoal_tac}
- (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name_inner_syntax) >>
- (fn (quant, props) => fn ctxt =>
- SIMPLE_METHOD'' quant (EVERY' (map (subgoal_tac ctxt) props))))
+ (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name_inner_syntax -- Parse.for_fixes) >>
+ (fn (quant, (props, fixes)) => fn ctxt =>
+ SIMPLE_METHOD'' quant (EVERY' (map (fn prop => subgoal_tac ctxt prop fixes) props))))
"insert subgoal (dynamic instantiation)" #>
Method.setup @{binding thin_tac}
- (Args.goal_spec -- Scan.lift Args.name_inner_syntax >>
- (fn (quant, prop) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop)))
- "remove premise (dynamic instantiation)");
+ (Args.goal_spec -- Scan.lift (Args.name_inner_syntax -- Parse.for_fixes) >>
+ (fn (quant, (prop, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop fixes)))
+ "remove premise (dynamic instantiation)");
end;
--- a/src/Pure/logic.ML Mon Mar 23 15:08:02 2015 +0100
+++ b/src/Pure/logic.ML Mon Mar 23 21:14:49 2015 +0100
@@ -61,8 +61,8 @@
val rlist_abs: (string * typ) list * term -> term
val incr_tvar_same: int -> typ Same.operation
val incr_tvar: int -> typ -> typ
- val incr_indexes_same: typ list * int -> term Same.operation
- val incr_indexes: typ list * int -> term -> term
+ val incr_indexes_same: string list * typ list * int -> term Same.operation
+ val incr_indexes: string list * typ list * int -> term -> term
val lift_abs: int -> term -> term -> term
val lift_all: int -> term -> term -> term
val strip_assums_hyp: term -> term list
@@ -367,14 +367,18 @@
(*For all variables in the term, increment indexnames and lift over the Us
result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
-fun incr_indexes_same ([], 0) = Same.same
- | incr_indexes_same (Ts, k) =
+fun incr_indexes_same ([], [], 0) = Same.same
+ | incr_indexes_same (fixed, Ts, k) =
let
val n = length Ts;
val incrT = incr_tvar_same k;
fun incr lev (Var ((x, i), T)) =
combound (Var ((x, i + k), Ts ---> Same.commit incrT T), lev, n)
+ | incr lev (Free (x, T)) =
+ if member (op =) fixed x then
+ combound (Free (x, Ts ---> Same.commit incrT T), lev, n)
+ else Free (x, incrT T)
| incr lev (Abs (x, T, body)) =
(Abs (x, incrT T, incr (lev + 1) body handle Same.SAME => body)
handle Same.SAME => Abs (x, T, incr (lev + 1) body))
@@ -382,7 +386,6 @@
(incr lev t $ (incr lev u handle Same.SAME => u)
handle Same.SAME => t $ incr lev u)
| incr _ (Const (c, T)) = Const (c, incrT T)
- | incr _ (Free (x, T)) = Free (x, incrT T)
| incr _ (Bound _) = raise Same.SAME;
in incr 0 end;
@@ -397,14 +400,14 @@
let
fun lift Ts (Const ("Pure.imp", _) $ _ $ B) t = lift Ts B t
| lift Ts (Const ("Pure.all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t)
- | lift Ts _ t = incr_indexes (rev Ts, inc) t;
+ | lift Ts _ t = incr_indexes ([], rev Ts, inc) t;
in lift [] end;
fun lift_all inc =
let
fun lift Ts ((c as Const ("Pure.imp", _)) $ A $ B) t = c $ A $ lift Ts B t
| lift Ts ((c as Const ("Pure.all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t)
- | lift Ts _ t = incr_indexes (rev Ts, inc) t;
+ | lift Ts _ t = incr_indexes ([], rev Ts, inc) t;
in lift [] end;
(*Strips assumptions in goal, yielding list of hypotheses. *)
--- a/src/Pure/more_unify.ML Mon Mar 23 15:08:02 2015 +0100
+++ b/src/Pure/more_unify.ML Mon Mar 23 21:14:49 2015 +0100
@@ -28,7 +28,7 @@
val maxidx = fold (Term.maxidx_term o #2) pairs ~1;
val offset = maxidx + 1;
- val pairs' = map (apfst (Logic.incr_indexes ([], offset))) pairs;
+ val pairs' = map (apfst (Logic.incr_indexes ([], [], offset))) pairs;
val maxidx' = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) pairs' ~1;
val pat_tvars = fold (Term.add_tvars o #1) pairs' [];
--- a/src/Pure/proofterm.ML Mon Mar 23 15:08:02 2015 +0100
+++ b/src/Pure/proofterm.ML Mon Mar 23 21:14:49 2015 +0100
@@ -834,7 +834,7 @@
fun lift_proof Bi inc prop prf =
let
fun lift'' Us Ts t =
- strip_abs Ts (Logic.incr_indexes (Us, inc) (mk_abs Ts t));
+ strip_abs Ts (Logic.incr_indexes ([], Us, inc) (mk_abs Ts t));
fun lift' Us Ts (Abst (s, T, prf)) =
(Abst (s, Same.map_option (Logic.incr_tvar_same inc) T, lifth' Us (dummyT::Ts) prf)
@@ -878,7 +878,7 @@
fun incr_indexes i =
Same.commit (map_proof_terms_same
- (Logic.incr_indexes_same ([], i)) (Logic.incr_tvar_same i));
+ (Logic.incr_indexes_same ([], [], i)) (Logic.incr_tvar_same i));
(***** proof by assumption *****)
--- a/src/Pure/thm.ML Mon Mar 23 15:08:02 2015 +0100
+++ b/src/Pure/thm.ML Mon Mar 23 21:14:49 2015 +0100
@@ -278,7 +278,7 @@
fun incr_indexes_cterm i (ct as Cterm {thy, t, T, maxidx, sorts}) =
if i < 0 then raise CTERM ("negative increment", [ct])
else if i = 0 then ct
- else Cterm {thy = thy, t = Logic.incr_indexes ([], i) t,
+ else Cterm {thy = thy, t = Logic.incr_indexes ([], [], i) t,
T = Logic.incr_tvar i T, maxidx = maxidx + i, sorts = sorts};
@@ -1306,8 +1306,8 @@
maxidx = maxidx + i,
shyps = shyps,
hyps = hyps,
- tpairs = map (apply2 (Logic.incr_indexes ([], i))) tpairs,
- prop = Logic.incr_indexes ([], i) prop});
+ tpairs = map (apply2 (Logic.incr_indexes ([], [], i))) tpairs,
+ prop = Logic.incr_indexes ([], [], i) prop});
(*Solve subgoal Bi of proof state B1...Bn/C by assumption. *)
fun assumption opt_ctxt i state =
--- a/src/Sequents/LK0.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/Sequents/LK0.thy Mon Mar 23 21:14:49 2015 +0100
@@ -153,12 +153,12 @@
ML {*
(*Cut and thin, replacing the right-side formula*)
fun cutR_tac ctxt s i =
- Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s) ] @{thm cut} i THEN
+ Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s)] [] @{thm cut} i THEN
rtac @{thm thinR} i
(*Cut and thin, replacing the left-side formula*)
fun cutL_tac ctxt s i =
- Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s)] @{thm cut} i THEN
+ Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s)] [] @{thm cut} i THEN
rtac @{thm thinL} (i + 1)
*}
--- a/src/Tools/induct_tacs.ML Mon Mar 23 15:08:02 2015 +0100
+++ b/src/Tools/induct_tacs.ML Mon Mar 23 21:14:49 2015 +0100
@@ -44,7 +44,7 @@
(case Induct.vars_of (Thm.term_of (Thm.cprem_of rule 1)) of
Var (xi, _) :: _ => xi
| _ => raise THM ("Malformed cases rule", 0, [rule]));
- in Rule_Insts.res_inst_tac ctxt [((xi, Position.none), s)] rule i st end
+ in Rule_Insts.res_inst_tac ctxt [((xi, Position.none), s)] [] rule i st end
handle THM _ => Seq.empty;
fun case_tac ctxt s = gen_case_tac ctxt s NONE;
@@ -104,7 +104,7 @@
val concls = Logic.dest_conjunctions (Thm.concl_of rule);
val insts = maps prep_inst (concls ~~ varss) handle ListPair.UnequalLengths =>
error "Induction rule has different numbers of variables";
- in Rule_Insts.res_inst_tac ctxt insts rule' i st end
+ in Rule_Insts.res_inst_tac ctxt insts [] rule' i st end
handle THM _ => Seq.empty;
end;
--- a/src/ZF/AC/AC16_WO4.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/ZF/AC/AC16_WO4.thy Mon Mar 23 21:14:49 2015 +0100
@@ -295,7 +295,7 @@
apply (rule lam_type)
apply (frule ex1_superset_a [THEN theI], fast+, clarify)
apply (rule cons_eqE [of _ a])
-apply (drule_tac A = "THE c. ?P (c) " and C = y in eq_imp_Int_eq)
+apply (drule_tac A = "THE c. P (c)" and C = y for P in eq_imp_Int_eq)
apply (simp_all add: the_eq_cons)
done
--- a/src/ZF/AC/HH.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/ZF/AC/HH.thy Mon Mar 23 21:14:49 2015 +0100
@@ -57,7 +57,7 @@
prefer 2 apply assumption+
apply (rule leI [THEN le_imp_subset, THEN subset_imp_Diff_eq, THEN ssubst],
assumption)
-apply (rule_tac t = "%z. z-?X" in subst_context)
+apply (rule_tac t = "%z. z-X" for X in subst_context)
apply (rule Diff_UN_eq_self)
apply (drule Ord_DiffE, assumption)
apply (fast elim: ltE, auto)
@@ -162,7 +162,7 @@
lemma f_subsets_imp_UN_HH_eq_x:
"\<forall>z \<in> Pow(x)-{0}. f`z \<in> Pow(z)-{0}
==> x - (\<Union>j \<in> (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0"
-apply (case_tac "?P \<in> {0}", fast)
+apply (case_tac "P \<in> {0}" for P, fast)
apply (drule Diff_subset [THEN PowI, THEN DiffI])
apply (drule bspec, assumption)
apply (drule f_subset_imp_HH_subset)
--- a/src/ZF/AC/WO2_AC16.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/ZF/AC/WO2_AC16.thy Mon Mar 23 21:14:49 2015 +0100
@@ -563,7 +563,7 @@
apply (elim exE)
apply (rename_tac h)
apply (rule_tac x = "\<Union>j<a. recfunAC16 (h,f,j,a) " in exI)
-apply (rule_tac P="%z. ?Y & (\<forall>x \<in> z. ?Z (x))"
+apply (rule_tac P="%z. Y & (\<forall>x \<in> z. Z(x))" for Y Z
in bij_is_surj [THEN surj_image_eq, THEN subst], assumption)
apply (rule lemma_simp_induct)
apply (blast del: conjI notI
--- a/src/ZF/AC/WO6_WO1.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/ZF/AC/WO6_WO1.thy Mon Mar 23 21:14:49 2015 +0100
@@ -390,7 +390,7 @@
apply (fast intro!: Ord_oadd domain_gg1 UN_gg1_eq gg1_lepoll_m)
(* case 2 *)
apply (elim oexE conjE)
-apply (rule_tac A = "f`?B" in not_emptyE, assumption)
+apply (rule_tac A = "f`B" for B in not_emptyE, assumption)
apply (rule CollectI)
apply (erule succ_natD)
apply (rule_tac x = "a++a" in exI)
--- a/src/ZF/Cardinal.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/ZF/Cardinal.thy Mon Mar 23 21:14:49 2015 +0100
@@ -59,7 +59,7 @@
"g \<in> Y->X
==> g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) =
X - lfp(X, %W. X - g``(Y - f``W))"
-apply (rule_tac P = "%u. ?v = X-u"
+apply (rule_tac P = "%u. v = X-u" for v
in decomp_bnd_mono [THEN lfp_unfold, THEN ssubst])
apply (simp add: double_complement fun_is_rel [THEN image_subset])
done
@@ -1079,7 +1079,7 @@
prefer 2 apply (blast del: allE elim: equalityE, clarify)
apply (subgoal_tac "B = {f(u) . u \<in> A - {z}}")
apply (blast intro: Diff_sing_Finite)
-apply (thin_tac "\<forall>A. ?P(A) \<longrightarrow> Finite(A)")
+apply (thin_tac "\<forall>A. P(A) \<longrightarrow> Finite(A)" for P)
apply (rule equalityI)
apply (blast intro: elim: equalityE)
apply (blast intro: elim: equalityCE)
--- a/src/ZF/Coind/Map.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/ZF/Coind/Map.thy Mon Mar 23 21:14:49 2015 +0100
@@ -111,7 +111,7 @@
(*Remaining subgoal*)
apply (rule excluded_middle [THEN disjE])
apply (erule image_Sigma1)
-apply (drule_tac psi = "?uu \<notin> B" in asm_rl)
+apply (drule_tac psi = "uu \<notin> B" for uu in asm_rl)
apply (auto simp add: qbeta)
done
--- a/src/ZF/Constructible/Normal.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/ZF/Constructible/Normal.thy Mon Mar 23 21:14:49 2015 +0100
@@ -284,7 +284,7 @@
==> F(\<Union>(X)) = (\<Union>y\<in>X. F(y))"
apply (frule Ord_set_cases)
apply (erule disjE, force)
-apply (thin_tac "X=0 \<longrightarrow> ?Q", auto)
+apply (thin_tac "X=0 \<longrightarrow> Q" for Q, auto)
txt{*The trival case of @{term "\<Union>X \<in> X"}*}
apply (rule equalityI, blast intro: Ord_Union_eq_succD)
apply (simp add: mono_le_subset_def UN_subset_iff le_subset_iff)
--- a/src/ZF/Constructible/Relative.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/ZF/Constructible/Relative.thy Mon Mar 23 21:14:49 2015 +0100
@@ -1024,9 +1024,9 @@
apply blast
txt{*Final, difficult case: the left-to-right direction of the theorem.*}
apply (insert power_ax, simp add: power_ax_def)
-apply (frule_tac x="A \<union> B" and P="\<lambda>x. rex(M,?Q(x))" in rspec)
+apply (frule_tac x="A \<union> B" and P="\<lambda>x. rex(M,Q(x))" for Q in rspec)
apply (blast, clarify)
-apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec)
+apply (drule_tac x=z and P="\<lambda>x. rex(M,Q(x))" for Q in rspec)
apply assumption
apply (blast intro: cartprod_iff_lemma)
done
@@ -1035,9 +1035,9 @@
"[| M(A); M(B) |] ==> \<exists>C[M]. cartprod(M,A,B,C)"
apply (simp del: cartprod_abs add: cartprod_iff)
apply (insert power_ax, simp add: power_ax_def)
-apply (frule_tac x="A \<union> B" and P="\<lambda>x. rex(M,?Q(x))" in rspec)
+apply (frule_tac x="A \<union> B" and P="\<lambda>x. rex(M,Q(x))" for Q in rspec)
apply (blast, clarify)
-apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec, auto)
+apply (drule_tac x=z and P="\<lambda>x. rex(M,Q(x))" for Q in rspec, auto)
apply (intro rexI conjI, simp+)
apply (insert cartprod_separation [of A B], simp)
done
--- a/src/ZF/Constructible/WFrec.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/ZF/Constructible/WFrec.thy Mon Mar 23 21:14:49 2015 +0100
@@ -180,7 +180,7 @@
==> restrict(Y, r -`` {x}) = f"
apply (subgoal_tac "\<forall>y \<in> r-``{x}. \<forall>z. <y,z>:Y \<longleftrightarrow> <y,z>:f")
apply (simp (no_asm_simp) add: restrict_def)
- apply (thin_tac "rall(M,?P)")+ --{*essential for efficiency*}
+ apply (thin_tac "rall(M,P)" for P)+ --{*essential for efficiency*}
apply (frule is_recfun_type [THEN fun_is_rel], blast)
apply (frule pair_components_in_M, assumption, clarify)
apply (rule iffI)
--- a/src/ZF/Induct/Multiset.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/ZF/Induct/Multiset.thy Mon Mar 23 21:14:49 2015 +0100
@@ -363,7 +363,7 @@
lemma msize_eq_0_iff: "multiset(M) ==> msize(M)=#0 \<longleftrightarrow> M=0"
apply (simp add: msize_def, auto)
-apply (rule_tac P = "setsum (?u,?v) \<noteq> #0" in swap)
+apply (rule_tac P = "setsum (u,v) \<noteq> #0" for u v in swap)
apply blast
apply (drule not_empty_multiset_imp_exist, assumption, clarify)
apply (subgoal_tac "Finite (mset_of (M) - {a}) ")
@@ -571,7 +571,7 @@
apply (simp add: multiset_def multiset_fun_iff)
apply (rule_tac x = A in exI, force)
apply (simp_all add: mset_of_def)
-apply (drule_tac psi = "\<forall>x \<in> A. ?u (x) " in asm_rl)
+apply (drule_tac psi = "\<forall>x \<in> A. u(x)" for u in asm_rl)
apply (drule_tac x = a in bspec)
apply (simp (no_asm_simp))
apply (subgoal_tac "cons (a, A) = A")
@@ -596,7 +596,7 @@
apply (simp (no_asm_simp) add: multiset_def multiset_fun_iff)
apply blast
apply (simp (no_asm_simp) add: mset_of_def)
-apply (drule_tac b = "if ?u then ?v else ?w" in sym, simp_all)
+apply (drule_tac b = "if u then v else w" for u v w in sym, simp_all)
apply (subgoal_tac "{x \<in> A - {a} . 0 < funrestrict (M, A - {x}) ` x} = A - {a}")
apply (auto intro!: setsum_cong simp add: zdiff_eq_iff zadd_commute multiset_def multiset_fun_iff mset_of_def)
done
@@ -815,7 +815,7 @@
apply (subgoal_tac "aa \<in> A")
prefer 2 apply blast
apply (drule_tac x = "M0 +# M" and P =
- "%x. x \<in> acc(multirel1(A, r)) \<longrightarrow> ?Q(x)" in spec)
+ "%x. x \<in> acc(multirel1(A, r)) \<longrightarrow> Q(x)" for Q in spec)
apply (simp add: munion_assoc [symmetric])
(* subgoal 3 \<in> additional conditions *)
apply (auto intro!: multirel1_base [THEN fieldI2] simp add: Mult_iff_multiset)
@@ -942,7 +942,7 @@
apply (simp add: mdiff_union_single_conv melem_diff_single, clarify)
apply (erule disjE, simp)
apply (erule disjE, simp)
-apply (drule_tac x = a and P = "%x. x :# Ka \<longrightarrow> ?Q(x)" in spec)
+apply (drule_tac x = a and P = "%x. x :# Ka \<longrightarrow> Q(x)" for Q in spec)
apply clarify
apply (rule_tac x = xa in exI)
apply (simp (no_asm_simp))
@@ -1005,7 +1005,7 @@
apply (drule sym, rotate_tac -1, simp)
apply (erule_tac V = "$# x = msize (J') " in thin_rl)
apply (frule_tac M = K and P = "%x. <x,a> \<in> r" in multiset_partition)
-apply (erule_tac P = "\<forall>k \<in> mset_of (K) . ?P (k) " in rev_mp)
+apply (erule_tac P = "\<forall>k \<in> mset_of (K) . P(k)" for P in rev_mp)
apply (erule ssubst)
apply (simp add: Ball_def, auto)
apply (subgoal_tac "< (I +# {# x \<in> K. <x, a> \<in> r#}) +# {# x \<in> K. <x, a> \<notin> r#}, (I +# {# x \<in> K. <x, a> \<in> r#}) +# J'> \<in> multirel(A, r) ")
@@ -1119,7 +1119,7 @@
lemma munion_multirel_mono1:
"[|<M, N> \<in> multirel(A, r); K \<in> Mult(A)|] ==> <M +# K, N +# K> \<in> multirel(A, r)"
apply (frule multirel_type [THEN subsetD])
-apply (rule_tac P = "%x. <x,?u> \<in> multirel(A, r) " in munion_commute [THEN subst])
+apply (rule_tac P = "%x. <x,u> \<in> multirel(A, r)" for u in munion_commute [THEN subst])
apply (subst munion_commute [of N])
apply (rule munion_multirel_mono2)
apply (auto simp add: Mult_iff_multiset)
--- a/src/ZF/Induct/Mutil.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/ZF/Induct/Mutil.thy Mon Mar 23 21:14:49 2015 +0100
@@ -147,7 +147,7 @@
==> t' \<notin> tiling(domino)"
apply (rule notI)
apply (drule tiling_domino_0_1)
- apply (erule_tac x = "|?A|" in eq_lt_E)
+ apply (erule_tac x = "|A|" for A in eq_lt_E)
apply (subgoal_tac "t \<in> tiling (domino)")
prefer 2 (*Requires a small simpset that won't move the succ applications*)
apply (simp only: nat_succI add_type dominoes_tile_matrix)
--- a/src/ZF/Induct/Primrec.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/ZF/Induct/Primrec.thy Mon Mar 23 21:14:49 2015 +0100
@@ -334,7 +334,7 @@
apply (simp add: add_le_self [THEN ack_lt_mono1])
txt {* ind step *}
apply (rule succ_leI [THEN lt_trans1])
- apply (rule_tac j = "g ` ?ll #+ ?mm" in lt_trans1)
+ apply (rule_tac j = "g ` ll #+ mm" for ll mm in lt_trans1)
apply (erule_tac [2] bspec)
apply (rule nat_le_refl [THEN add_le_mono])
apply typecheck
--- a/src/ZF/Int_ZF.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/ZF/Int_ZF.thy Mon Mar 23 21:14:49 2015 +0100
@@ -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_tac i="succ (?v)" in add_left_cancel, auto)
+apply (erule_tac i="succ (v)" for v in add_left_cancel, auto)
done
lemma zless_imp_succ_zadd:
--- a/src/ZF/Order.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/ZF/Order.thy Mon Mar 23 21:14:49 2015 +0100
@@ -670,8 +670,8 @@
apply (auto simp: subset_def preorder_on_def refl_def vimage_def image_def)
apply blast
unfolding trans_on_def
- apply (erule_tac P = "(\<lambda>x. \<forall>y\<in>field(?r).
- \<forall>z\<in>field(?r). \<langle>x, y\<rangle> \<in> ?r \<longrightarrow> \<langle>y, z\<rangle> \<in> ?r \<longrightarrow> \<langle>x, z\<rangle> \<in> ?r)" in rev_ballE)
+ apply (erule_tac P = "(\<lambda>x. \<forall>y\<in>field(r).
+ \<forall>z\<in>field(r). \<langle>x, y\<rangle> \<in> r \<longrightarrow> \<langle>y, z\<rangle> \<in> r \<longrightarrow> \<langle>x, z\<rangle> \<in> r)" for r in rev_ballE)
(* instance obtained from proof term generated by best *)
apply best
apply blast
--- a/src/ZF/Resid/Residuals.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/ZF/Resid/Residuals.thy Mon Mar 23 21:14:49 2015 +0100
@@ -129,7 +129,7 @@
subst_rec(v1 |> v2, u1 |> u2,n))"
apply (erule Scomp.induct, safe)
apply (simp_all add: lift_rec_Var subst_Var residuals_lift_rec)
-apply (drule_tac psi = "\<forall>x.?P (x) " in asm_rl)
+apply (drule_tac psi = "\<forall>x. P(x)" for P in asm_rl)
apply (simp add: substitution)
done
@@ -159,7 +159,7 @@
lemma preservation [rule_format]:
"u ~ v ==> regular(v) \<longrightarrow> u|>v = (u un v)|>v"
apply (erule Scomp.induct, safe)
-apply (drule_tac [3] psi = "Fun (?u) |> ?v = ?w" in asm_rl)
+apply (drule_tac [3] psi = "Fun (u) |> v = w" for u v w in asm_rl)
apply (auto simp add: union_preserve_comp comp_sym_iff)
done
--- a/src/ZF/Tools/induct_tacs.ML Mon Mar 23 15:08:02 2015 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Mon Mar 23 21:14:49 2015 +0100
@@ -9,8 +9,10 @@
signature DATATYPE_TACTICS =
sig
- val induct_tac: Proof.context -> string -> int -> tactic
- val exhaust_tac: Proof.context -> string -> int -> tactic
+ val exhaust_tac: Proof.context -> string -> (binding * string option * mixfix) list ->
+ int -> tactic
+ val induct_tac: Proof.context -> string -> (binding * string option * mixfix) list ->
+ int -> tactic
val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
val rep_datatype: Facts.ref * Token.src list -> Facts.ref * Token.src list ->
(Facts.ref * Token.src list) list -> (Facts.ref * Token.src list) list -> theory -> theory
@@ -88,7 +90,7 @@
(2) exhaustion works for VARIABLES in the premises, not general terms
**)
-fun exhaust_induct_tac exh ctxt var i state = SUBGOAL (fn _ =>
+fun exhaust_induct_tac exh ctxt var fixes i state = SUBGOAL (fn _ =>
let
val thy = Proof_Context.theory_of ctxt
val ({context = ctxt', asms, ...}, _) = Subgoal.focus ctxt i state
@@ -101,11 +103,11 @@
[] => error "induction is not available for this datatype"
| major::_ => FOLogic.dest_Trueprop major)
in
- Rule_Insts.eres_inst_tac ctxt [((ixn, Position.none), var)] rule i
+ Rule_Insts.eres_inst_tac ctxt [((ixn, Position.none), var)] fixes rule i
end
handle Find_tname msg =>
if exh then (*try boolean case analysis instead*)
- case_tac ctxt var i
+ case_tac ctxt var fixes i
else error msg) i state;
val exhaust_tac = exhaust_induct_tac true;
@@ -177,12 +179,12 @@
val _ =
Theory.setup
(Method.setup @{binding induct_tac}
- (Args.goal_spec -- Scan.lift Args.name >>
- (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (induct_tac ctxt s)))
+ (Args.goal_spec -- Scan.lift (Args.name -- Parse.for_fixes) >>
+ (fn (quant, (s, xs)) => fn ctxt => SIMPLE_METHOD'' quant (induct_tac ctxt s xs)))
"induct_tac emulation (dynamic instantiation!)" #>
Method.setup @{binding case_tac}
- (Args.goal_spec -- Scan.lift Args.name >>
- (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (exhaust_tac ctxt s)))
+ (Args.goal_spec -- Scan.lift (Args.name -- Parse.for_fixes) >>
+ (fn (quant, (s, xs)) => fn ctxt => SIMPLE_METHOD'' quant (exhaust_tac ctxt s xs)))
"datatype case_tac emulation (dynamic instantiation!)");
--- a/src/ZF/UNITY/AllocImpl.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/ZF/UNITY/AllocImpl.thy Mon Mar 23 21:14:49 2015 +0100
@@ -167,8 +167,8 @@
apply (drule_tac f = "lift (rel) " in preserves_imp_eq)
apply assumption+
apply (force dest: ActsD)
-apply (erule_tac V = "\<forall>x \<in> Acts (alloc_prog) \<union> Acts (G). ?P(x)" in thin_rl)
-apply (erule_tac V = "alloc_prog \<in> stable (?u)" in thin_rl)
+apply (erule_tac V = "\<forall>x \<in> Acts (alloc_prog) \<union> Acts (G). P(x)" for P in thin_rl)
+apply (erule_tac V = "alloc_prog \<in> stable (u)" for u in thin_rl)
apply (drule_tac a = "xc`rel" and f = "lift (rel)" in Increasing_imp_Stable)
apply (auto simp add: Stable_def Constrains_def constrains_def)
apply (drule bspec, force)
@@ -219,7 +219,7 @@
transient({s\<in>state. k \<le> length(s`rel)} \<inter>
{s\<in>state. succ(s`NbR) = k})"
apply auto
-apply (erule_tac V = "G\<notin>?u" in thin_rl)
+apply (erule_tac V = "G\<notin>u" for u in thin_rl)
apply (rule_tac act = alloc_rel_act in transientI)
apply (simp (no_asm) add: alloc_prog_def [THEN def_prg_Acts])
apply (simp (no_asm) add: alloc_rel_act_def [THEN def_act_eq, THEN act_subset])
@@ -329,7 +329,7 @@
{s\<in>state. k < length(s`ask)} \<inter> {s\<in>state. length(s`giv)=k}
Ensures {s\<in>state. ~ k <length(s`ask)} \<union> {s\<in>state. length(s`giv) \<noteq> k}"
apply (rule EnsuresI, auto)
-apply (erule_tac [2] V = "G\<notin>?u" in thin_rl)
+apply (erule_tac [2] V = "G\<notin>u" for u in thin_rl)
apply (rule_tac [2] act = alloc_giv_act in transientI)
prefer 2
apply (simp add: alloc_prog_def [THEN def_prg_Acts])
@@ -573,7 +573,7 @@
apply (rule LeadsTo_weaken_R)
apply (rule Always_LeadsToD [OF safety length_ask_giv], assumption+, clarify)
apply (simp add: INT_iff)
-apply (drule_tac x = "length(x ` giv)" and P = "%x. ?f (x) \<le> NbT" in bspec)
+apply (drule_tac x = "length(x ` giv)" and P = "%x. f (x) \<le> NbT" for f in bspec)
apply simp
apply (blast intro: le_trans)
done
--- a/src/ZF/UNITY/Comp.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/ZF/UNITY/Comp.thy Mon Mar 23 21:14:49 2015 +0100
@@ -305,8 +305,8 @@
(*The G case remains*)
apply (auto dest: ActsD simp add: preserves_def stable_def constrains_def ball_conj_distrib all_conj_distrib)
(*We have a G-action, so delete assumptions about F-actions*)
-apply (erule_tac V = "\<forall>act \<in> Acts (F) . ?P (act)" in thin_rl)
-apply (erule_tac V = "\<forall>k\<in>A. \<forall>act \<in> Acts (F) . ?P (k,act)" in thin_rl)
+apply (erule_tac V = "\<forall>act \<in> Acts (F). P (act)" for P in thin_rl)
+apply (erule_tac V = "\<forall>k\<in>A. \<forall>act \<in> Acts (F) . P (k,act)" for P in thin_rl)
apply (subgoal_tac "f (x) = f (xa) ")
apply (auto dest!: bspec)
done
--- a/src/ZF/UNITY/Distributor.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/ZF/UNITY/Distributor.thy Mon Mar 23 21:14:49 2015 +0100
@@ -131,7 +131,7 @@
apply (subgoal_tac "length (s ` iIn) \<in> nat")
apply typecheck
apply (subgoal_tac "m \<in> nat")
-apply (drule_tac x = "nth(m, s`iIn) " and P = "%elt. ?X (elt) \<longrightarrow> elt<Nclients" in bspec)
+apply (drule_tac x = "nth(m, s`iIn) " and P = "%elt. X (elt) \<longrightarrow> elt<Nclients" for X in bspec)
apply (simp add: ltI)
apply (simp_all add: Ord_mem_iff_lt)
apply (blast dest: ltD)
--- a/src/ZF/UNITY/Follows.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/ZF/UNITY/Follows.thy Mon Mar 23 21:14:49 2015 +0100
@@ -114,14 +114,14 @@
apply (rule single_LeadsTo_I, auto)
apply (drule_tac x = "g (sa) " and A = B in bspec)
apply auto
-apply (drule_tac x = "f (sa) " and P = "%j. F \<in> ?X (j) \<longmapsto>w ?Y (j) " in bspec)
+apply (drule_tac x = "f (sa) " and P = "%j. F \<in> X(j) \<longmapsto>w Y(j)" for X Y in bspec)
apply auto
apply (rule PSP_Stable [THEN LeadsTo_weaken], blast, blast)
apply auto
apply (force simp add: part_order_def refl_def)
apply (force simp add: part_order_def refl_def)
-apply (drule_tac x = "f1 (x) " and x1 = "f (sa) " and P2 = "%x y. \<forall>u\<in>B. ?P (x,y,u) " in bspec [THEN bspec])
-apply (drule_tac [3] x = "g (x) " and x1 = "g (sa) " and P2 = "%x y. ?P (x,y) \<longrightarrow> ?d (x,y) \<in> t" in bspec [THEN bspec])
+apply (drule_tac x = "f1 (x)" and x1 = "f (sa) " and P2 = "%x y. \<forall>u\<in>B. P (x,y,u)" for P in bspec [THEN bspec])
+apply (drule_tac [3] x = "g (x) " and x1 = "g (sa) " and P2 = "%x y. P (x,y) \<longrightarrow> d (x,y) \<in> t" for P d in bspec [THEN bspec])
apply auto
apply (rule_tac b = "h (f (sa), g (sa))" and A = C in trans_onD)
apply (auto simp add: part_order_def)
@@ -135,7 +135,7 @@
F:{x \<in> state. <k, h(f(x), g(x))> \<in> t} LeadsTo {x \<in> state. <k, h(f(x), g1(x))> \<in> t}"
apply (unfold mono2_def Increasing_def)
apply (rule single_LeadsTo_I, auto)
-apply (drule_tac x = "f (sa) " and P = "%k. F \<in> Stable (?X (k))" in bspec)
+apply (drule_tac x = "f (sa) " and P = "%k. F \<in> Stable (X (k))" for X in bspec)
apply auto
apply (drule_tac x = "g (sa) " in bspec)
apply auto
@@ -144,7 +144,7 @@
apply (force simp add: part_order_def refl_def)
apply (force simp add: part_order_def refl_def)
apply (drule_tac x = "f (x) " and x1 = "f (sa) " in bspec [THEN bspec])
-apply (drule_tac [3] x = "g1 (x) " and x1 = "g (sa) " and P2 = "%x y. ?P (x,y) \<longrightarrow> ?d (x,y) \<in> t" in bspec [THEN bspec])
+apply (drule_tac [3] x = "g1 (x) " and x1 = "g (sa) " and P2 = "%x y. P (x,y) \<longrightarrow> d (x,y) \<in> t" for P d in bspec [THEN bspec])
apply auto
apply (rule_tac b = "h (f (sa), g (sa))" and A = C in trans_onD)
apply (auto simp add: part_order_def)
--- a/src/ZF/UNITY/GenPrefix.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/ZF/UNITY/GenPrefix.thy Mon Mar 23 21:14:49 2015 +0100
@@ -281,9 +281,9 @@
apply (simp_all add: nth_append length_type length_app)
apply (rule conjI)
apply (blast intro: gen_prefix.append)
-apply (erule_tac V = "length (xs) < length (ys) \<longrightarrow>?u" in thin_rl)
+apply (erule_tac V = "length (xs) < length (ys) \<longrightarrow>u" for u in thin_rl)
apply (erule_tac a = zs in list.cases, auto)
-apply (rule_tac P1 = "%x. <?u (x), ?v>:?w" in nat_diff_split [THEN iffD2])
+apply (rule_tac P1 = "%x. <u(x), v>:w" for u v w in nat_diff_split [THEN iffD2])
apply auto
apply (simplesubst append_cons_conv)
apply (rule_tac [2] gen_prefix.append)
@@ -407,7 +407,7 @@
declare same_prefix_prefix [simp]
lemma same_prefix_prefix_Nil: "xs \<in> list(A) ==> <xs@ys,xs> \<in> prefix(A) \<longleftrightarrow> (<ys,[]> \<in> prefix(A))"
-apply (rule_tac P = "%x. <?u, x>:?v \<longleftrightarrow> ?w (x) " in app_right_Nil [THEN subst])
+apply (rule_tac P = "%x. <u, x>:v \<longleftrightarrow> w(x)" for u v w in app_right_Nil [THEN subst])
apply (rule_tac [2] same_prefix_prefix, auto)
done
declare same_prefix_prefix_Nil [simp]
--- a/src/ZF/UNITY/Increasing.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/ZF/UNITY/Increasing.thy Mon Mar 23 21:14:49 2015 +0100
@@ -67,8 +67,8 @@
apply (drule_tac x = "f (xb) " in bspec)
apply (rotate_tac [2] -1)
apply (drule_tac [2] x = act in bspec, simp_all)
-apply (drule_tac A = "act``?u" and c = xa in subsetD, blast)
-apply (drule_tac x = "f (xa) " and x1 = "f (xb) " in bspec [THEN bspec])
+apply (drule_tac A = "act``u" and c = xa for u in subsetD, blast)
+apply (drule_tac x = "f(xa) " and x1 = "f(xb)" in bspec [THEN bspec])
apply (rule_tac [3] b = "g (f (xb))" and A = B in trans_onD)
apply simp_all
done
@@ -137,8 +137,8 @@
apply clarify
apply (rotate_tac -2)
apply (drule_tac x = act in bspec)
-apply (drule_tac [2] A = "act``?u" and c = xa in subsetD, simp_all, blast)
-apply (drule_tac x = "f (xa) " and x1 = "f (xb) " in bspec [THEN bspec])
+apply (drule_tac [2] A = "act``u" and c = xa for u in subsetD, simp_all, blast)
+apply (drule_tac x = "f(xa)" and x1 = "f(xb)" in bspec [THEN bspec])
apply (rule_tac [3] b = "g (f (xb))" and A = B in trans_onD)
apply simp_all
done
@@ -181,8 +181,8 @@
apply (drule_tac x = act in bspec)
apply (rotate_tac [2] -3)
apply (drule_tac [2] x = act in bspec, simp_all)
-apply (drule_tac A = "act``?u" and c = xa in subsetD)
-apply (drule_tac [2] A = "act``?u" and c = xa in subsetD, blast, blast)
+apply (drule_tac A = "act``u" and c = xa for u in subsetD)
+apply (drule_tac [2] A = "act``u" and c = xa for u in subsetD, blast, blast)
apply (rotate_tac -4)
apply (drule_tac x = "f (xa) " and x1 = "f (xb) " in bspec [THEN bspec])
apply (rotate_tac [3] -1)
@@ -213,8 +213,8 @@
apply (drule_tac x = act in bspec)
apply (rotate_tac [2] -3)
apply (drule_tac [2] x = act in bspec, simp_all)
-apply (drule_tac A = "act``?u" and c = x in subsetD)
-apply (drule_tac [2] A = "act``?u" and c = x in subsetD, blast, blast)
+apply (drule_tac A = "act``u" and c = x for u in subsetD)
+apply (drule_tac [2] A = "act``u" and c = x for u in subsetD, blast, blast)
apply (rotate_tac -9)
apply (drule_tac x = "f (x) " and x1 = "f (xa) " in bspec [THEN bspec])
apply (rotate_tac [3] -1)
--- a/src/ZF/UNITY/Merge.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/ZF/UNITY/Merge.thy Mon Mar 23 21:14:49 2015 +0100
@@ -166,7 +166,7 @@
apply (subgoal_tac "xa \<in> nat")
apply (simp_all add: Ord_mem_iff_lt)
prefer 2 apply (blast intro: lt_trans)
-apply (drule_tac x = "nth (xa, x`iOut)" and P = "%elt. ?X (elt) \<longrightarrow> elt<Nclients" in bspec)
+apply (drule_tac x = "nth (xa, x`iOut)" and P = "%elt. X (elt) \<longrightarrow> elt<Nclients" for X in bspec)
apply (simp add: ltI nat_into_Ord)
apply (blast dest: ltD)
done
--- a/src/ZF/UNITY/SubstAx.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/ZF/UNITY/SubstAx.thy Mon Mar 23 21:14:49 2015 +0100
@@ -359,7 +359,8 @@
@{thm EnsuresI}, @{thm ensuresI}] 1),
(*now there are two subgoals: co & transient*)
simp_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems program})) 2,
- Rule_Insts.res_inst_tac ctxt [((("act", 0), Position.none), sact)] @{thm transientI} 2,
+ Rule_Insts.res_inst_tac ctxt
+ [((("act", 0), Position.none), sact)] [] @{thm transientI} 2,
(*simplify the command's domain*)
simp_tac (ctxt addsimps [@{thm domain_def}]) 3,
(* proving the domain part *)
--- a/src/ZF/UNITY/WFair.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/ZF/UNITY/WFair.thy Mon Mar 23 21:14:49 2015 +0100
@@ -517,7 +517,7 @@
apply (unfold field_def)
apply (simp add: measure_def)
apply (rule equalityI, force, clarify)
-apply (erule_tac V = "x\<notin>range (?y) " in thin_rl)
+apply (erule_tac V = "x\<notin>range (y)" for y in thin_rl)
apply (erule nat_induct)
apply (rule_tac [2] b = "succ (succ (xa))" in domainI)
apply (rule_tac b = "succ (0) " in domainI)
--- a/src/ZF/WF.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/ZF/WF.thy Mon Mar 23 21:14:49 2015 +0100
@@ -230,7 +230,7 @@
"[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))"
apply (unfold is_recfun_def)
txt{*replace f only on the left-hand side*}
-apply (erule_tac P = "%x.?t(x) = ?u" in ssubst)
+apply (erule_tac P = "%x. t(x) = u" for t u in ssubst)
apply (simp add: underI)
done
@@ -244,7 +244,7 @@
apply (intro impI)
apply (elim ssubst)
apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def)
-apply (rule_tac t = "%z. H (?x,z) " in subst_context)
+apply (rule_tac t = "%z. H (x, z)" for x in subst_context)
apply (subgoal_tac "\<forall>y\<in>r-``{x}. \<forall>z. <y,z>:f \<longleftrightarrow> <y,z>:g")
apply (blast dest: transD)
apply (simp add: apply_iff)
@@ -291,7 +291,7 @@
apply (rule lam_cong [OF refl])
apply (drule underD)
apply (fold is_recfun_def)
-apply (rule_tac t = "%z. H(?x,z)" in subst_context)
+apply (rule_tac t = "%z. H(x, z)" for x in subst_context)
apply (rule fun_extension)
apply (blast intro: is_recfun_type)
apply (rule lam_type [THEN restrict_type2])
--- a/src/ZF/Zorn.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/ZF/Zorn.thy Mon Mar 23 21:14:49 2015 +0100
@@ -469,7 +469,7 @@
apply (erule lamE) apply simp
apply assumption
- apply (thin_tac "C \<subseteq> ?X")
+ apply (thin_tac "C \<subseteq> X" for X)
apply (fast elim: lamE)
done
have "?A \<in> Chain(r)"
--- a/src/ZF/ex/Limit.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/ZF/ex/Limit.thy Mon Mar 23 21:14:49 2015 +0100
@@ -1833,8 +1833,8 @@
apply (rename_tac [5] y)
apply (rule_tac [5] P =
"%z. rel(DD`succ(y),
- (ee`y O Rp(?DD(y)`y,?DD(y)`succ(y),?ee(y)`y)) ` (x`succ(y)),
- z)"
+ (ee`y O Rp(DD'(y)`y,DD'(y)`succ(y),ee'(y)`y)) ` (x`succ(y)),
+ z)" for DD' ee'
in id_conv [THEN subst])
apply (rule_tac [6] rel_cf)
(* Dinf and cont_fun doesn't go well together, both Pi(_,%x._). *)
--- a/src/ZF/ex/Primes.thy Mon Mar 23 15:08:02 2015 +0100
+++ b/src/ZF/ex/Primes.thy Mon Mar 23 21:14:49 2015 +0100
@@ -93,7 +93,7 @@
lemma gcd_non_0_raw:
"[| 0<n; n \<in> nat |] ==> gcd(m,n) = gcd(n, m mod n)"
apply (simp add: gcd_def)
-apply (rule_tac P = "%z. ?left (z) = ?right" in transrec [THEN ssubst])
+apply (rule_tac P = "%z. left (z) = right" for left right in transrec [THEN ssubst])
apply (simp add: ltD [THEN mem_imp_not_eq, THEN not_sym]
mod_less_divisor [THEN ltD])
done