--- a/NEWS Fri Nov 13 15:06:58 2015 +0100
+++ b/NEWS Fri Nov 13 16:02:59 2015 +0100
@@ -176,6 +176,26 @@
The keyword 'when' may be used instead of 'if', to indicate 'presume'
instead of 'assume' above.
+* Assumptions ('assume', 'presume') allow structured statements using
+'if' and 'for', similar to 'have' etc. above. For example:
+
+ assume result: "C x y"
+ if "A x" and "B y"
+ for x :: 'a and y :: 'a
+
+This assumes "\<And>x y::'a. A x \<Longrightarrow> B y \<Longrightarrow> C x y" and produces a general
+result as usual: "A ?x \<Longrightarrow> B ?y \<Longrightarrow> C ?x ?y".
+
+Vacuous quantification in assumptions is omitted, i.e. a for-context
+only effects propositions according to actual use of variables. For
+example:
+
+ assume "A x" and "B y" for x and y
+
+is equivalent to:
+
+ assume "\<And>x. A x" and "\<And>y. B y"
+
* The meaning of 'show' with Pure rule statements has changed: premises
are treated in the sense of 'assume', instead of 'presume'. This means,
a goal like "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" can be solved completely as follows:
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy Fri Nov 13 15:06:58 2015 +0100
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Fri Nov 13 16:02:59 2015 +0100
@@ -349,6 +349,8 @@
@{syntax_def vars}: (@{syntax name} +) ('::' @{syntax type})?
;
@{syntax_def props}: @{syntax thmdecl}? (@{syntax prop} @{syntax prop_pat}? +)
+ ;
+ @{syntax_def props'}: (@{syntax prop} @{syntax prop_pat}? +)
\<close>}
The treatment of multiple declarations corresponds to the
--- a/src/Doc/Isar_Ref/Proof.thy Fri Nov 13 15:06:58 2015 +0100
+++ b/src/Doc/Isar_Ref/Proof.thy Fri Nov 13 16:02:59 2015 +0100
@@ -160,7 +160,11 @@
@{rail \<open>
@@{command fix} @{syntax "fixes"}
;
- (@@{command assume} | @@{command presume}) (@{syntax props} + @'and')
+ (@@{command assume} | @@{command presume}) concl prems @{syntax for_fixes}
+ ;
+ concl: (@{syntax props} + @'and')
+ ;
+ prems: (@'if' (@{syntax props'} + @'and'))?
;
@@{command def} (def + @'and')
;
@@ -181,6 +185,10 @@
"and"}; the resulting list of current facts consists of all of these
concatenated.
+ A structured assumption like \<^theory_text>\<open>assume "B x" and "A x" for x\<close> is equivalent
+ to \<^theory_text>\<open>assume "\<And>x. A x \<Longrightarrow> B x"\<close>, but vacuous quantification is avoided: a
+ for-context only effects propositions according to actual use of variables.
+
\<^descr> @{command "def"}~\<open>x \<equiv> t\<close> introduces a local (non-polymorphic) definition.
In results exported from the context, \<open>x\<close> is replaced by \<open>t\<close>. Basically,
``@{command "def"}~\<open>x \<equiv> t\<close>'' abbreviates ``@{command "fix"}~\<open>x\<close>~@{command