merged
authorwenzelm
Sat Jun 13 22:44:22 2015 +0200 (2015-06-13)
changeset 60460abee0de69a89
parent 60442 310853646597
parent 60459 2761a2249c83
child 60461 22995ec9fefd
child 60464 16bed2709b70
merged
NEWS
     1.1 --- a/NEWS	Sat Jun 13 19:23:41 2015 +0100
     1.2 +++ b/NEWS	Sat Jun 13 22:44:22 2015 +0200
     1.3 @@ -24,13 +24,13 @@
     1.4      for x :: 'a and y :: 'a
     1.5      <proof>
     1.6  
     1.7 -The local assumptions are always bound to the name "prems".  The result
     1.8 -is exported from context of the statement as usual.  The above roughly
     1.9 +The local assumptions are bound to the name "that". The result is
    1.10 +exported from context of the statement as usual. The above roughly
    1.11  corresponds to a raw proof block like this:
    1.12  
    1.13    {
    1.14      fix x :: 'a and y :: 'a
    1.15 -    assume prems: "A x" "B y"
    1.16 +    assume that: "A x" "B y"
    1.17      have "C x y" <proof>
    1.18    }
    1.19    note result = this
    1.20 @@ -38,6 +38,27 @@
    1.21  * New command 'supply' supports fact definitions during goal refinement
    1.22  ('apply' scripts).
    1.23  
    1.24 +* New command 'consider' states rules for generalized elimination and
    1.25 +case splitting. This is like a toplevel statement "theorem obtains" used
    1.26 +within a proof body; or like a multi-branch 'obtain' without activation
    1.27 +of the local context elements yet.
    1.28 +
    1.29 +* Proof method "cases" allows to specify the rule as first entry of
    1.30 +chained facts.  This is particularly useful with 'consider':
    1.31 +
    1.32 +  consider (a) A | (b) B | (c) C <proof>
    1.33 +  then have something
    1.34 +  proof cases
    1.35 +    case a
    1.36 +    then show ?thesis <proof>
    1.37 +  next
    1.38 +    case b
    1.39 +    then show ?thesis <proof>
    1.40 +  next
    1.41 +    case c
    1.42 +    then show ?thesis <proof>
    1.43 +  qed
    1.44 +
    1.45  
    1.46  *** Pure ***
    1.47  
     2.1 --- a/src/Doc/Isar_Ref/Proof.thy	Sat Jun 13 19:23:41 2015 +0100
     2.2 +++ b/src/Doc/Isar_Ref/Proof.thy	Sat Jun 13 22:44:22 2015 +0200
     2.3 @@ -435,21 +435,22 @@
     2.4       @@{command schematic_corollary}) (stmt | statement)
     2.5      ;
     2.6      (@@{command have} | @@{command show} | @@{command hence} | @@{command thus})
     2.7 -      stmt if_prems @{syntax for_fixes}
     2.8 +      stmt (@'if' stmt)? @{syntax for_fixes}
     2.9      ;
    2.10      @@{command print_statement} @{syntax modes}? @{syntax thmrefs}
    2.11      ;
    2.12    
    2.13      stmt: (@{syntax props} + @'and')
    2.14      ;
    2.15 -    if_prems: (@'if' stmt)?
    2.16 -    ;
    2.17      statement: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} *) \<newline>
    2.18        conclusion
    2.19      ;
    2.20 -    conclusion: @'shows' stmt | @'obtains' (@{syntax par_name}? obtain_case + '|')
    2.21 +    conclusion: @'shows' stmt | @'obtains' @{syntax obtain_clauses}
    2.22      ;
    2.23 -    obtain_case: (@{syntax vars} + @'and') @'where' (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
    2.24 +    @{syntax_def obtain_clauses}: (@{syntax par_name}? obtain_case + '|')
    2.25 +    ;
    2.26 +    @{syntax_def obtain_case}: (@{syntax vars} + @'and') @'where'
    2.27 +      (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
    2.28    \<close>}
    2.29  
    2.30    \begin{description}
    2.31 @@ -523,11 +524,10 @@
    2.32    @{variable_ref "?thesis"}) to be bound automatically, see also
    2.33    \secref{sec:term-abbrev}.
    2.34  
    2.35 -  The optional case names of @{element_ref "obtains"} have a twofold
    2.36 -  meaning: (1) in the proof of this claim they refer to the local context
    2.37 -  introductions, (2) in the resulting rule they become annotations for
    2.38 -  symbolic case splits, e.g.\ for the @{method_ref cases} method
    2.39 -  (\secref{sec:cases-induct}).
    2.40 +  Structured goal statements involving @{keyword_ref "if"} define the
    2.41 +  special fact ``@{text that}'' to refer to these assumptions in the proof
    2.42 +  body. The user may provide separate names according to the syntax of the
    2.43 +  statement.
    2.44  \<close>
    2.45  
    2.46  
    2.47 @@ -853,15 +853,6 @@
    2.48  subsection \<open>Emulating tactic scripts \label{sec:tactic-commands}\<close>
    2.49  
    2.50  text \<open>
    2.51 -  The Isar provides separate commands to accommodate tactic-style
    2.52 -  proof scripts within the same system.  While being outside the
    2.53 -  orthodox Isar proof language, these might come in handy for
    2.54 -  interactive exploration and debugging, or even actual tactical proof
    2.55 -  within new-style theories (to benefit from document preparation, for
    2.56 -  example).  See also \secref{sec:tactics} for actual tactics, that
    2.57 -  have been encapsulated as proof methods.  Proper proof methods may
    2.58 -  be used in scripts, too.
    2.59 -
    2.60    \begin{matharray}{rcl}
    2.61      @{command_def "supply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
    2.62      @{command_def "apply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
    2.63 @@ -872,6 +863,15 @@
    2.64      @{command_def "back"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
    2.65    \end{matharray}
    2.66  
    2.67 +  The Isar language provides separate commands to accommodate tactic-style
    2.68 +  proof scripts within the same system.  While being outside the
    2.69 +  orthodox Isar proof language, these might come in handy for
    2.70 +  interactive exploration and debugging, or even actual tactical proof
    2.71 +  within new-style theories (to benefit from document preparation, for
    2.72 +  example).  See also \secref{sec:tactics} for actual tactics, that
    2.73 +  have been encapsulated as proof methods.  Proper proof methods may
    2.74 +  be used in scripts, too.
    2.75 +
    2.76    @{rail \<open>
    2.77      @@{command supply} (@{syntax thmdef}? @{syntax thmrefs} + @'and')
    2.78      ;
    2.79 @@ -979,83 +979,125 @@
    2.80  (*<*)end(*>*)
    2.81  
    2.82  
    2.83 -section \<open>Generalized elimination \label{sec:obtain}\<close>
    2.84 +section \<open>Generalized elimination and case splitting \label{sec:obtain}\<close>
    2.85  
    2.86  text \<open>
    2.87    \begin{matharray}{rcl}
    2.88 +    @{command_def "consider"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
    2.89      @{command_def "obtain"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
    2.90      @{command_def "guess"}@{text "\<^sup>*"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
    2.91    \end{matharray}
    2.92  
    2.93 -  Generalized elimination means that additional elements with certain
    2.94 -  properties may be introduced in the current context, by virtue of a
    2.95 -  locally proven ``soundness statement''.  Technically speaking, the
    2.96 -  @{command "obtain"} language element is like a declaration of
    2.97 -  @{command "fix"} and @{command "assume"} (see also see
    2.98 -  \secref{sec:proof-context}), together with a soundness proof of its
    2.99 -  additional claim.  According to the nature of existential reasoning,
   2.100 -  assumptions get eliminated from any result exported from the context
   2.101 -  later, provided that the corresponding parameters do \emph{not}
   2.102 -  occur in the conclusion.
   2.103 +  Generalized elimination means that hypothetical parameters and premises
   2.104 +  may be introduced in the current context, potentially with a split into
   2.105 +  cases. This works by virtue of a locally proven rule that establishes the
   2.106 +  soundness of this temporary context extension. As representative examples,
   2.107 +  one may think of standard rules from Isabelle/HOL like this:
   2.108 +
   2.109 +  \medskip
   2.110 +  \begin{tabular}{ll}
   2.111 +  @{text "\<exists>x. B x \<Longrightarrow> (\<And>x. B x \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\
   2.112 +  @{text "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\
   2.113 +  @{text "A \<or> B \<Longrightarrow> (A \<Longrightarrow> thesis) \<Longrightarrow> (B \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\
   2.114 +  \end{tabular}
   2.115 +  \medskip
   2.116 +
   2.117 +  In general, these particular rules and connectives need to get involved at
   2.118 +  all: this concept works directly in Isabelle/Pure via Isar commands
   2.119 +  defined below. In particular, the logic of elimination and case splitting
   2.120 +  is delegated to an Isar proof, which often involves automated tools.
   2.121  
   2.122    @{rail \<open>
   2.123 -    @@{command obtain} @{syntax par_name}? (@{syntax vars} + @'and')
   2.124 +    @@{command consider} @{syntax obtain_clauses}
   2.125 +    ;
   2.126 +    @@{command obtain} @{syntax par_name}? (@{syntax "fixes"} + @'and')
   2.127        @'where' (@{syntax props} + @'and')
   2.128      ;
   2.129 -    @@{command guess} (@{syntax vars} + @'and')
   2.130 +    @@{command guess} (@{syntax "fixes"} + @'and')
   2.131    \<close>}
   2.132  
   2.133 -  The derived Isar command @{command "obtain"} is defined as follows
   2.134 -  (where @{text "b\<^sub>1, \<dots>, b\<^sub>k"} shall refer to (optional)
   2.135 -  facts indicated for forward chaining).
   2.136 +  \begin{description}
   2.137 +
   2.138 +  \item @{command consider}~@{text "(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x
   2.139 +  | (b) \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots> "} states a rule for case
   2.140 +  splitting into separate subgoals, such that each case involves new
   2.141 +  parameters and premises. After the proof is finished, the resulting rule
   2.142 +  may be used directly with the @{method cases} proof method
   2.143 +  (\secref{sec:cases-induct}), in order to perform actual case-splitting of
   2.144 +  the proof text via @{command case} and @{command next} as usual.
   2.145 +
   2.146 +  Optional names in round parentheses refer to case names: in the proof of
   2.147 +  the rule this is a fact name, in the resulting rule it is used as
   2.148 +  annotation with the @{attribute_ref case_names} attribute.
   2.149 +
   2.150 +  \medskip Formally, the command @{command consider} is defined as derived
   2.151 +  Isar language element as follows:
   2.152 +
   2.153    \begin{matharray}{l}
   2.154 -    @{text "\<langle>using b\<^sub>1 \<dots> b\<^sub>k\<rangle>"}~~@{command "obtain"}~@{text "x\<^sub>1 \<dots> x\<^sub>m \<WHERE> a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n  \<langle>proof\<rangle> \<equiv>"} \\[1ex]
   2.155 -    \quad @{command "have"}~@{text "\<And>thesis. (\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\
   2.156 -    \quad @{command "proof"}~@{method succeed} \\
   2.157 -    \qquad @{command "fix"}~@{text thesis} \\
   2.158 -    \qquad @{command "assume"}~@{text "that [Pure.intro?]: \<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> thesis"} \\
   2.159 -    \qquad @{command "then"}~@{command "show"}~@{text thesis} \\
   2.160 -    \quad\qquad @{command "apply"}~@{text -} \\
   2.161 -    \quad\qquad @{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>k  \<langle>proof\<rangle>"} \\
   2.162 -    \quad @{command "qed"} \\
   2.163 -    \quad @{command "fix"}~@{text "x\<^sub>1 \<dots> x\<^sub>m"}~@{command "assume"}@{text "\<^sup>* a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} \\
   2.164 +    @{command "consider"}~@{text "(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x | (b) \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots> \<equiv>"} \\[1ex]
   2.165 +    \quad @{command "have"}~@{text "[case_names a b \<dots>]: thesis"} \\
   2.166 +    \qquad @{text "\<IF> a [Pure.intro?]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis"} \\
   2.167 +    \qquad @{text "\<AND> b [Pure.intro?]: \<And>\<^vec>y. \<^vec>B \<^vec>y \<Longrightarrow> thesis"} \\
   2.168 +    \qquad @{text "\<AND> \<dots>"} \\
   2.169 +    \qquad @{text "\<FOR> thesis"} \\
   2.170 +    \qquad @{command "apply"}~@{text "(insert a b \<dots>)"} \\
   2.171    \end{matharray}
   2.172  
   2.173 -  Typically, the soundness proof is relatively straight-forward, often
   2.174 -  just by canonical automated tools such as ``@{command "by"}~@{text
   2.175 -  simp}'' or ``@{command "by"}~@{text blast}''.  Accordingly, the
   2.176 -  ``@{text that}'' reduction above is declared as simplification and
   2.177 -  introduction rule.
   2.178 +  See also \secref{sec:goals} for @{keyword "obtains"} in toplevel goal
   2.179 +  statements, as well as @{command print_statement} to print existing rules
   2.180 +  in a similar format.
   2.181  
   2.182 -  In a sense, @{command "obtain"} represents at the level of Isar
   2.183 -  proofs what would be meta-logical existential quantifiers and
   2.184 -  conjunctions.  This concept has a broad range of useful
   2.185 -  applications, ranging from plain elimination (or introduction) of
   2.186 -  object-level existential and conjunctions, to elimination over
   2.187 -  results of symbolic evaluation of recursive definitions, for
   2.188 -  example.  Also note that @{command "obtain"} without parameters acts
   2.189 -  much like @{command "have"}, where the result is treated as a
   2.190 -  genuine assumption.
   2.191 +  \item @{command obtain}~@{text "\<^vec>x \<WHERE> \<^vec>A \<^vec>x"}
   2.192 +  states a generalized elimination rule with exactly one case. After the
   2.193 +  proof is finished, it is activated for the subsequent proof text: the
   2.194 +  context is augmented via @{command fix}~@{text "\<^vec>x"} @{command
   2.195 +  assume}~@{text "\<^vec>A \<^vec>x"}, with special provisions to export
   2.196 +  later results by discharging these assumptions again.
   2.197 +
   2.198 +  Note that according to the parameter scopes within the elimination rule,
   2.199 +  results \emph{must not} refer to hypothetical parameters; otherwise the
   2.200 +  export will fail! This restriction conforms to the usual manner of
   2.201 +  existential reasoning in Natural Deduction.
   2.202 +
   2.203 +  \medskip Formally, the command @{command obtain} is defined as derived
   2.204 +  Isar language element as follows, using an instrumented variant of
   2.205 +  @{command assume}:
   2.206  
   2.207 -  An alternative name to be used instead of ``@{text that}'' above may
   2.208 -  be given in parentheses.
   2.209 +  \begin{matharray}{l}
   2.210 +    @{command "obtain"}~@{text "\<^vec>x \<WHERE> a: \<^vec>A \<^vec>x  \<langle>proof\<rangle> \<equiv>"} \\[1ex]
   2.211 +    \quad @{command "have"}~@{text "thesis"} \\
   2.212 +    \qquad @{text "\<IF> that [Pure.intro?]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis"} \\
   2.213 +    \qquad @{text "\<FOR> thesis"} \\
   2.214 +    \qquad @{command "apply"}~@{text "(insert that)"} \\
   2.215 +    \qquad @{text "\<langle>proof\<rangle>"} \\
   2.216 +    \quad @{command "fix"}~@{text "\<^vec>x"}~@{command "assume"}@{text "\<^sup>* a: \<^vec>A \<^vec>x"} \\
   2.217 +  \end{matharray}
   2.218 +
   2.219 +  \item @{command guess} is similar to @{command obtain}, but it derives the
   2.220 +  obtained context elements from the course of tactical reasoning in the
   2.221 +  proof. Thus it can considerably obscure the proof: it is classified as
   2.222 +  \emph{improper}.
   2.223  
   2.224 -  \medskip The improper variant @{command "guess"} is similar to
   2.225 -  @{command "obtain"}, but derives the obtained statement from the
   2.226 -  course of reasoning!  The proof starts with a fixed goal @{text
   2.227 -  thesis}.  The subsequent proof may refine this to anything of the
   2.228 -  form like @{text "\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots>
   2.229 -  \<phi>\<^sub>n \<Longrightarrow> thesis"}, but must not introduce new subgoals.  The
   2.230 -  final goal state is then used as reduction rule for the obtain
   2.231 -  scheme described above.  Obtained parameters @{text "x\<^sub>1, \<dots>,
   2.232 -  x\<^sub>m"} are marked as internal by default, which prevents the
   2.233 -  proof context from being polluted by ad-hoc variables.  The variable
   2.234 -  names and type constraints given as arguments for @{command "guess"}
   2.235 -  specify a prefix of obtained parameters explicitly in the text.
   2.236 +  A proof with @{command guess} starts with a fixed goal @{text thesis}. The
   2.237 +  subsequent refinement steps may turn this to anything of the form @{text
   2.238 +  "\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis"}, but without splitting into new
   2.239 +  subgoals. The final goal state is then used as reduction rule for the
   2.240 +  obtain pattern described above. Obtained parameters @{text "\<^vec>x"} are
   2.241 +  marked as internal by default, and thus inaccessible in the proof text.
   2.242 +  The variable names and type constraints given as arguments for @{command
   2.243 +  "guess"} specify a prefix of accessible parameters.
   2.244  
   2.245 -  It is important to note that the facts introduced by @{command
   2.246 -  "obtain"} and @{command "guess"} may not be polymorphic: any
   2.247 -  type-variables occurring here are fixed in the present context!
   2.248 +  \end{description}
   2.249 +
   2.250 +  In the proof of @{command consider} and @{command obtain} the local
   2.251 +  premises are always bound to the fact name ``@{text that}'', according to
   2.252 +  structured Isar statements involving @{keyword_ref "if"}
   2.253 +  (\secref{sec:goals}).
   2.254 +
   2.255 +  Facts that are established by @{command "obtain"} and @{command "guess"}
   2.256 +  may not be polymorphic: any type-variables occurring here are fixed in the
   2.257 +  present context. This is a natural consequence of the role of @{command
   2.258 +  fix} and @{command assume} in these constructs.
   2.259  \<close>
   2.260  
   2.261  
   2.262 @@ -1372,6 +1414,7 @@
   2.263    \medskip
   2.264    \begin{tabular}{llll}
   2.265      facts           &                 & arguments   & rule \\\hline
   2.266 +    @{text "\<turnstile> R"}   & @{method cases} &             & implicit rule @{text R} \\
   2.267                      & @{method cases} &             & classical case split \\
   2.268                      & @{method cases} & @{text t}   & datatype exhaustion (type of @{text t}) \\
   2.269      @{text "\<turnstile> A t"} & @{method cases} & @{text "\<dots>"} & inductive predicate/set elimination (of @{text A}) \\
     3.1 --- a/src/Doc/isar.sty	Sat Jun 13 19:23:41 2015 +0100
     3.2 +++ b/src/Doc/isar.sty	Sat Jun 13 22:44:22 2015 +0200
     3.3 @@ -13,6 +13,7 @@
     3.4  \newcommand{\indexouternonterm}[1]{\indexdef{}{syntax}{#1}}
     3.5  \newcommand{\indexisarelem}[1]{\indexdef{}{element}{#1}}
     3.6  
     3.7 +\newcommand{\isasymIF}{\isakeyword{if}}
     3.8  \newcommand{\isasymFOR}{\isakeyword{for}}
     3.9  \newcommand{\isasymAND}{\isakeyword{and}}
    3.10  \newcommand{\isasymIS}{\isakeyword{is}}
     4.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Sat Jun 13 19:23:41 2015 +0100
     4.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Sat Jun 13 22:44:22 2015 +0200
     4.3 @@ -69,7 +69,8 @@
     4.4      fix y assume "y \<in> F"
     4.5      then have "a y \<in> ?S" by blast
     4.6      with xi have "a y \<le> xi" by (rule lub.upper)
     4.7 -  } moreover {
     4.8 +  }
     4.9 +  moreover {
    4.10      fix y assume y: "y \<in> F"
    4.11      from xi have "xi \<le> b y"
    4.12      proof (rule lub.least)
    4.13 @@ -78,7 +79,8 @@
    4.14        from u y have "a u \<le> b y" by (rule r)
    4.15        with au show "au \<le> b y" by (simp only:)
    4.16      qed
    4.17 -  } ultimately show "\<exists>xi. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y" by blast
    4.18 +  }
    4.19 +  ultimately show "\<exists>xi. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y" by blast
    4.20  qed
    4.21  
    4.22  text \<open>
     5.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Sat Jun 13 19:23:41 2015 +0100
     5.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Sat Jun 13 22:44:22 2015 +0200
     5.3 @@ -126,11 +126,11 @@
     5.4      @{text x} and @{text y} are contained in the greater
     5.5      one. \label{cases1}\<close>
     5.6  
     5.7 -  from cM c'' c' have "graph H'' h'' \<subseteq> graph H' h' \<or> graph H' h' \<subseteq> graph H'' h''"
     5.8 -    (is "?case1 \<or> ?case2") ..
     5.9 +  from cM c'' c' consider "graph H'' h'' \<subseteq> graph H' h'" | "graph H' h' \<subseteq> graph H'' h''"
    5.10 +    by (blast dest: chainsD)
    5.11    then show ?thesis
    5.12 -  proof
    5.13 -    assume ?case1
    5.14 +  proof cases
    5.15 +    case 1
    5.16      have "(x, h x) \<in> graph H'' h''" by fact
    5.17      also have "\<dots> \<subseteq> graph H' h'" by fact
    5.18      finally have xh:"(x, h x) \<in> graph H' h'" .
    5.19 @@ -139,14 +139,16 @@
    5.20      moreover from cM u and c' have "graph H' h' \<subseteq> graph H h" by blast
    5.21      ultimately show ?thesis using * by blast
    5.22    next
    5.23 -    assume ?case2
    5.24 +    case 2
    5.25      from x_hx have "x \<in> H''" ..
    5.26 -    moreover {
    5.27 +    moreover have "y \<in> H''"
    5.28 +    proof -
    5.29        have "(y, h y) \<in> graph H' h'" by (rule y_hy)
    5.30        also have "\<dots> \<subseteq> graph H'' h''" by fact
    5.31        finally have "(y, h y) \<in> graph H'' h''" .
    5.32 -    } then have "y \<in> H''" ..
    5.33 -    moreover from cM u and c'' have "graph H'' h'' \<subseteq> graph H h" by blast
    5.34 +      then show ?thesis ..
    5.35 +    qed
    5.36 +    moreover from u c'' have "graph H'' h'' \<subseteq> graph H h" by blast
    5.37      ultimately show ?thesis using ** by blast
    5.38    qed
    5.39  qed
    5.40 @@ -179,10 +181,11 @@
    5.41      or vice versa, since both @{text "G\<^sub>1"} and @{text
    5.42      "G\<^sub>2"} are members of @{text c}. \label{cases2}\<close>
    5.43  
    5.44 -  from cM G1 G2 have "G1 \<subseteq> G2 \<or> G2 \<subseteq> G1" (is "?case1 \<or> ?case2") ..
    5.45 +  from cM G1 G2 consider "G1 \<subseteq> G2" | "G2 \<subseteq> G1"
    5.46 +    by (blast dest: chainsD)
    5.47    then show ?thesis
    5.48 -  proof
    5.49 -    assume ?case1
    5.50 +  proof cases
    5.51 +    case 1
    5.52      with xy' G2_rep have "(x, y) \<in> graph H2 h2" by blast
    5.53      then have "y = h2 x" ..
    5.54      also
    5.55 @@ -190,7 +193,7 @@
    5.56      then have "z = h2 x" ..
    5.57      finally show ?thesis .
    5.58    next
    5.59 -    assume ?case2
    5.60 +    case 2
    5.61      with xz' G1_rep have "(x, z) \<in> graph H1 h1" by blast
    5.62      then have "z = h1 x" ..
    5.63      also
     6.1 --- a/src/HOL/Isar_Examples/Hoare_Ex.thy	Sat Jun 13 19:23:41 2015 +0100
     6.2 +++ b/src/HOL/Isar_Examples/Hoare_Ex.thy	Sat Jun 13 22:44:22 2015 +0200
     6.3 @@ -224,9 +224,9 @@
     6.4    proof hoare
     6.5      show "?inv 0 1" by simp
     6.6      show "?inv (s + i) (i + 1)" if "?inv s i \<and> i \<noteq> n" for s i
     6.7 -      using prems by simp
     6.8 +      using that by simp
     6.9      show "s = ?sum n" if "?inv s i \<and> \<not> i \<noteq> n" for s i
    6.10 -      using prems by simp
    6.11 +      using that by simp
    6.12    qed
    6.13  qed
    6.14  
     7.1 --- a/src/HOL/Isar_Examples/Nested_Datatype.thy	Sat Jun 13 19:23:41 2015 +0100
     7.2 +++ b/src/HOL/Isar_Examples/Nested_Datatype.thy	Sat Jun 13 22:44:22 2015 +0200
     7.3 @@ -39,10 +39,10 @@
     7.4    proof (induct t rule: subst_term.induct)
     7.5      show "?P (Var a)" for a by simp
     7.6      show "?P (App b ts)" if "?Q ts" for b ts
     7.7 -      using prems by (simp only: subst_simps)
     7.8 +      using that by (simp only: subst_simps)
     7.9      show "?Q []" by simp
    7.10      show "?Q (t # ts)" if "?P t" "?Q ts" for t ts
    7.11 -      using prems by (simp only: subst_simps)
    7.12 +      using that by (simp only: subst_simps)
    7.13    qed
    7.14  qed
    7.15  
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Isar_Examples/Structured_Statements.thy	Sat Jun 13 22:44:22 2015 +0200
     8.3 @@ -0,0 +1,44 @@
     8.4 +(*  Title:      HOL/Isar_Examples/Structured_Statements.thy
     8.5 +    Author:     Makarius
     8.6 +*)
     8.7 +
     8.8 +section \<open>Structured statements within Isar proofs\<close>
     8.9 +
    8.10 +theory Structured_Statements
    8.11 +imports Main
    8.12 +begin
    8.13 +
    8.14 +notepad
    8.15 +begin
    8.16 +
    8.17 +  fix A B :: bool
    8.18 +
    8.19 +  have iff_comm: "(A \<and> B) \<longleftrightarrow> (B \<and> A)"
    8.20 +  proof
    8.21 +    show "B \<and> A" if "A \<and> B"
    8.22 +    proof
    8.23 +      show B using that ..
    8.24 +      show A using that ..
    8.25 +    qed
    8.26 +    show "A \<and> B" if "B \<and> A"
    8.27 +    proof
    8.28 +      show A using that ..
    8.29 +      show B using that ..
    8.30 +    qed
    8.31 +  qed
    8.32 +
    8.33 +  text \<open>Alternative proof, avoiding redundant copy of symmetric argument.\<close>
    8.34 +  have iff_comm: "(A \<and> B) \<longleftrightarrow> (B \<and> A)"
    8.35 +  proof
    8.36 +    show "B \<and> A" if "A \<and> B" for A B
    8.37 +    proof
    8.38 +      show B using that ..
    8.39 +      show A using that ..
    8.40 +    qed
    8.41 +    then show "A \<and> B" if "B \<and> A"
    8.42 +      by this (rule that)
    8.43 +  qed
    8.44 +
    8.45 +end
    8.46 +
    8.47 +end
    8.48 \ No newline at end of file
     9.1 --- a/src/HOL/Library/Convex.thy	Sat Jun 13 19:23:41 2015 +0100
     9.2 +++ b/src/HOL/Library/Convex.thy	Sat Jun 13 22:44:22 2015 +0200
     9.3 @@ -538,7 +538,7 @@
     9.4        by auto
     9.5      let ?a = "\<lambda>j. a j / (1 - a i)"
     9.6      have a_nonneg: "?a j \<ge> 0" if "j \<in> s" for j
     9.7 -      using i0 insert prems by fastforce
     9.8 +      using i0 insert that by fastforce
     9.9      have "(\<Sum> j \<in> insert i s. a j) = 1"
    9.10        using insert by auto
    9.11      then have "(\<Sum> j \<in> s. a j) = 1 - a i"
    10.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sat Jun 13 19:23:41 2015 +0100
    10.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sat Jun 13 22:44:22 2015 +0200
    10.3 @@ -159,8 +159,9 @@
    10.4    assume IH: "\<forall>m<n. m \<noteq> 0 \<longrightarrow> (\<exists>z. cmod (1 + b * z ^ m) < 1)"
    10.5    assume n: "n \<noteq> 0"
    10.6    let ?P = "\<lambda>z n. cmod (1 + b * z ^ n) < 1"
    10.7 -  {
    10.8 -    assume e: "even n"
    10.9 +  show "\<exists>z. ?P z n"
   10.10 +  proof cases
   10.11 +    assume "even n"
   10.12      then have "\<exists>m. n = 2 * m"
   10.13        by presburger
   10.14      then obtain m where m: "n = 2 * m"
   10.15 @@ -170,19 +171,17 @@
   10.16      with IH[rule_format, of m] obtain z where z: "?P z m"
   10.17        by blast
   10.18      from z have "?P (csqrt z) n"
   10.19 -      by (simp add: m power_mult power2_csqrt)
   10.20 -    then have "\<exists>z. ?P z n" ..
   10.21 -  }
   10.22 -  moreover
   10.23 -  {
   10.24 -    assume o: "odd n"
   10.25 -    have th0: "cmod (complex_of_real (cmod b) / b) = 1"
   10.26 -      using b by (simp add: norm_divide)
   10.27 -    from o have "\<exists>m. n = Suc (2 * m)"
   10.28 +      by (simp add: m power_mult)
   10.29 +    then show ?thesis ..
   10.30 +  next
   10.31 +    assume "odd n"
   10.32 +    then have "\<exists>m. n = Suc (2 * m)"
   10.33        by presburger+
   10.34      then obtain m where m: "n = Suc (2 * m)"
   10.35        by blast
   10.36 -    from unimodular_reduce_norm[OF th0] o
   10.37 +    have th0: "cmod (complex_of_real (cmod b) / b) = 1"
   10.38 +      using b by (simp add: norm_divide)
   10.39 +    from unimodular_reduce_norm[OF th0] \<open>odd n\<close>
   10.40      have "\<exists>v. cmod (complex_of_real (cmod b) / b + v^n) < 1"
   10.41        apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1")
   10.42        apply (rule_tac x="1" in exI)
   10.43 @@ -206,7 +205,7 @@
   10.44      then obtain v where v: "cmod (complex_of_real (cmod b) / b + v^n) < 1"
   10.45        by blast
   10.46      let ?w = "v / complex_of_real (root n (cmod b))"
   10.47 -    from odd_real_root_pow[OF o, of "cmod b"]
   10.48 +    from odd_real_root_pow[OF \<open>odd n\<close>, of "cmod b"]
   10.49      have th1: "?w ^ n = v^n / complex_of_real (cmod b)"
   10.50        by (simp add: power_divide of_real_power[symmetric])
   10.51      have th2:"cmod (complex_of_real (cmod b) / b) = 1"
   10.52 @@ -222,9 +221,8 @@
   10.53        done
   10.54      from mult_left_less_imp_less[OF th4 th3]
   10.55      have "?P ?w n" unfolding th1 .
   10.56 -    then have "\<exists>z. ?P z n" ..
   10.57 -  }
   10.58 -  ultimately show "\<exists>z. ?P z n" by blast
   10.59 +    then show ?thesis ..
   10.60 +  qed
   10.61  qed
   10.62  
   10.63  text \<open>Bolzano-Weierstrass type property for closed disc in complex plane.\<close>
   10.64 @@ -1020,51 +1018,44 @@
   10.65    "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow>
   10.66      p dvd (q ^ (degree p)) \<or> (p = 0 \<and> q = 0)"
   10.67  proof -
   10.68 -  show ?thesis
   10.69 -  proof (cases "p = 0")
   10.70 -    case True
   10.71 +  consider "p = 0" | "p \<noteq> 0" "degree p = 0" | n where "p \<noteq> 0" "degree p = Suc n"
   10.72 +    by (cases "degree p") auto
   10.73 +  then show ?thesis
   10.74 +  proof cases
   10.75 +    case 1
   10.76      then have eq: "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow> q = 0"
   10.77        by (auto simp add: poly_all_0_iff_0)
   10.78      {
   10.79        assume "p dvd (q ^ (degree p))"
   10.80        then obtain r where r: "q ^ (degree p) = p * r" ..
   10.81 -      from r True have False by simp
   10.82 +      from r 1 have False by simp
   10.83      }
   10.84 -    with eq True show ?thesis by blast
   10.85 +    with eq 1 show ?thesis by blast
   10.86    next
   10.87 -    case False
   10.88 -    show ?thesis
   10.89 -    proof (cases "degree p = 0")
   10.90 -      case True
   10.91 -      with \<open>p \<noteq> 0\<close> obtain k where k: "p = [:k:]" "k \<noteq> 0"
   10.92 -        by (cases p) (simp split: if_splits)
   10.93 -      then have th1: "\<forall>x. poly p x \<noteq> 0"
   10.94 +    case 2
   10.95 +    then obtain k where k: "p = [:k:]" "k \<noteq> 0"
   10.96 +      by (cases p) (simp split: if_splits)
   10.97 +    then have th1: "\<forall>x. poly p x \<noteq> 0"
   10.98 +      by simp
   10.99 +    from k 2(2) have "q ^ (degree p) = p * [:1/k:]"
  10.100 +      by (simp add: one_poly_def)
  10.101 +    then have th2: "p dvd (q ^ (degree p))" ..
  10.102 +    from 2(1) th1 th2 show ?thesis
  10.103 +      by blast
  10.104 +  next
  10.105 +    case 3
  10.106 +    {
  10.107 +      assume "p dvd (q ^ (Suc n))"
  10.108 +      then obtain u where u: "q ^ (Suc n) = p * u" ..
  10.109 +      fix x
  10.110 +      assume h: "poly p x = 0" "poly q x \<noteq> 0"
  10.111 +      then have "poly (q ^ (Suc n)) x \<noteq> 0"
  10.112          by simp
  10.113 -      from k True have "q ^ (degree p) = p * [:1/k:]"
  10.114 -        by (simp add: one_poly_def)
  10.115 -      then have th2: "p dvd (q ^ (degree p))" ..
  10.116 -      from False th1 th2 show ?thesis
  10.117 -        by blast
  10.118 -    next
  10.119 -      case False
  10.120 -      assume dp: "degree p \<noteq> 0"
  10.121 -      then obtain n where n: "degree p = Suc n "
  10.122 -        by (cases "degree p") auto
  10.123 -      {
  10.124 -        assume "p dvd (q ^ (Suc n))"
  10.125 -        then obtain u where u: "q ^ (Suc n) = p * u" ..
  10.126 -        {
  10.127 -          fix x
  10.128 -          assume h: "poly p x = 0" "poly q x \<noteq> 0"
  10.129 -          then have "poly (q ^ (Suc n)) x \<noteq> 0"
  10.130 -            by simp
  10.131 -          then have False using u h(1)
  10.132 -            by (simp only: poly_mult) simp
  10.133 -        }
  10.134 -      }
  10.135 -      with n nullstellensatz_lemma[of p q "degree p"] dp
  10.136 -      show ?thesis by auto
  10.137 -    qed
  10.138 +      then have False using u h(1)
  10.139 +        by (simp only: poly_mult) simp
  10.140 +    }
  10.141 +    with 3 nullstellensatz_lemma[of p q "degree p"]
  10.142 +    show ?thesis by auto
  10.143    qed
  10.144  qed
  10.145  
  10.146 @@ -1191,7 +1182,7 @@
  10.147    shows "\<exists>x. poly (pCons a (pCons b p)) x = (0::complex)"
  10.148  proof -
  10.149    have False if "h \<noteq> 0" "t = 0" and "pCons a (pCons b p) = pCons h t" for h t
  10.150 -    using l prems by simp
  10.151 +    using l that by simp
  10.152    then have th: "\<not> (\<exists> h t. h \<noteq> 0 \<and> t = 0 \<and> pCons a (pCons b p) = pCons h t)"
  10.153      by blast
  10.154    from fundamental_theorem_of_algebra_alt[OF th] show ?thesis
    11.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sat Jun 13 19:23:41 2015 +0100
    11.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sat Jun 13 22:44:22 2015 +0200
    11.3 @@ -190,10 +190,10 @@
    11.4      using \<open>finite simplices\<close> unfolding F_eq by auto
    11.5  
    11.6    show "card {s \<in> simplices. face f s} = 1" if "f \<in> ?F" "bnd f" for f
    11.7 -    using bnd prems by auto
    11.8 +    using bnd that by auto
    11.9  
   11.10    show "card {s \<in> simplices. face f s} = 2" if "f \<in> ?F" "\<not> bnd f" for f
   11.11 -    using nbnd prems by auto
   11.12 +    using nbnd that by auto
   11.13  
   11.14    show "odd (card {f \<in> {f. \<exists>s\<in>simplices. face f s}. rl ` f = {..n} \<and> bnd f})"
   11.15      using odd_card by simp
    12.1 --- a/src/HOL/ROOT	Sat Jun 13 19:23:41 2015 +0100
    12.2 +++ b/src/HOL/ROOT	Sat Jun 13 22:44:22 2015 +0200
    12.3 @@ -623,6 +623,7 @@
    12.4      Peirce
    12.5      Puzzle
    12.6      Summation
    12.7 +    Structured_Statements
    12.8    document_files
    12.9      "root.bib"
   12.10      "root.tex"
    13.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sat Jun 13 19:23:41 2015 +0100
    13.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sat Jun 13 22:44:22 2015 +0200
    13.3 @@ -222,7 +222,7 @@
    13.4  fun is_low_level_class_const s =
    13.5    s = @{const_name equal_class.equal} orelse String.isSubstring sep_class_sep s
    13.6  
    13.7 -val sep_that = Long_Name.separator ^ Obtain.thatN
    13.8 +val sep_that = Long_Name.separator ^ Auto_Bind.thatN
    13.9  val skolem_thesis = Name.skolem Auto_Bind.thesisN
   13.10  
   13.11  fun is_that_fact th =
    14.1 --- a/src/Pure/Isar/auto_bind.ML	Sat Jun 13 19:23:41 2015 +0100
    14.2 +++ b/src/Pure/Isar/auto_bind.ML	Sat Jun 13 22:44:22 2015 +0200
    14.3 @@ -8,7 +8,7 @@
    14.4  sig
    14.5    val thesisN: string
    14.6    val thisN: string
    14.7 -  val premsN: string
    14.8 +  val thatN: string
    14.9    val assmsN: string
   14.10    val abs_params: term -> term -> term
   14.11    val goal: Proof.context -> term list -> (indexname * term option) list
   14.12 @@ -23,8 +23,8 @@
   14.13  
   14.14  val thesisN = "thesis";
   14.15  val thisN = "this";
   14.16 +val thatN = "that";
   14.17  val assmsN = "assms";
   14.18 -val premsN = "prems";
   14.19  
   14.20  fun strip_judgment ctxt = Object_Logic.drop_judgment ctxt o Logic.strip_assums_concl;
   14.21  
    15.1 --- a/src/Pure/Isar/element.ML	Sat Jun 13 19:23:41 2015 +0100
    15.2 +++ b/src/Pure/Isar/element.ML	Sat Jun 13 22:44:22 2015 +0200
    15.3 @@ -7,9 +7,12 @@
    15.4  
    15.5  signature ELEMENT =
    15.6  sig
    15.7 +  type ('typ, 'term) obtain = binding * ((binding * 'typ option * mixfix) list * 'term list)
    15.8 +  type obtains = (string, string) obtain list
    15.9 +  type obtains_i = (typ, term) obtain list
   15.10    datatype ('typ, 'term) stmt =
   15.11      Shows of (Attrib.binding * ('term * 'term list) list) list |
   15.12 -    Obtains of (binding * ((binding * 'typ option) list * 'term list)) list
   15.13 +    Obtains of ('typ, 'term) obtain list
   15.14    type statement = (string, string) stmt
   15.15    type statement_i = (typ, term) stmt
   15.16    datatype ('typ, 'term, 'fact) ctxt =
   15.17 @@ -61,9 +64,13 @@
   15.18  
   15.19  (* statement *)
   15.20  
   15.21 +type ('typ, 'term) obtain = binding * ((binding * 'typ option * mixfix) list * 'term list);
   15.22 +type obtains = (string, string) obtain list;
   15.23 +type obtains_i = (typ, term) obtain list;
   15.24 +
   15.25  datatype ('typ, 'term) stmt =
   15.26    Shows of (Attrib.binding * ('term * 'term list) list) list |
   15.27 -  Obtains of (binding * ((binding * 'typ option) list * 'term list)) list;
   15.28 +  Obtains of ('typ, 'term) obtain list;
   15.29  
   15.30  type statement = (string, string) stmt;
   15.31  type statement_i = (typ, term) stmt;
   15.32 @@ -125,14 +132,14 @@
   15.33      fun prt_show (a, ts) =
   15.34        Pretty.block (Pretty.breaks (prt_binding a ":" @ prt_terms (map fst ts)));
   15.35  
   15.36 -    fun prt_var (x, SOME T) = Pretty.block
   15.37 +    fun prt_var (x, SOME T, _) = Pretty.block
   15.38            [Pretty.str (Binding.name_of x ^ " ::"), Pretty.brk 1, prt_typ T]
   15.39 -      | prt_var (x, NONE) = Pretty.str (Binding.name_of x);
   15.40 +      | prt_var (x, NONE, _) = Pretty.str (Binding.name_of x);
   15.41      val prt_vars = separate (Pretty.keyword2 "and") o map prt_var;
   15.42  
   15.43 -    fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (prt_terms ts))
   15.44 -      | prt_obtain (_, (xs, ts)) = Pretty.block (Pretty.breaks
   15.45 -          (prt_vars xs @ [Pretty.keyword2 "where"] @ prt_terms ts));
   15.46 +    fun prt_obtain (_, ([], props)) = Pretty.block (Pretty.breaks (prt_terms props))
   15.47 +      | prt_obtain (_, (vars, props)) = Pretty.block (Pretty.breaks
   15.48 +          (prt_vars vars @ [Pretty.keyword2 "where"] @ prt_terms props));
   15.49    in
   15.50      fn Shows shows => pretty_items "shows" "and" (map prt_show shows)
   15.51       | Obtains obtains => pretty_items "obtains" "|" (map prt_obtain obtains)
   15.52 @@ -209,7 +216,7 @@
   15.53  fun obtain prop ctxt =
   15.54    let
   15.55      val ((ps, prop'), ctxt') = Variable.focus prop ctxt;
   15.56 -    fun fix (x, T) = (Binding.name (Variable.revert_fixed ctxt' x), SOME T);
   15.57 +    fun fix (x, T) = (Binding.name (Variable.revert_fixed ctxt' x), SOME T, NoSyn);
   15.58      val xs = map (fix o #2) ps;
   15.59      val As = Logic.strip_imp_prems prop';
   15.60    in ((Binding.empty, (xs, As)), ctxt') end;
    16.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Jun 13 19:23:41 2015 +0100
    16.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Jun 13 22:44:22 2015 +0200
    16.3 @@ -491,7 +491,8 @@
    16.4  
    16.5  
    16.6  val structured_statement =
    16.7 -  Parse_Spec.statement -- Parse_Spec.if_prems -- Parse.for_fixes >> (fn ((a, b), c) => (c, b, a));
    16.8 +  Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes
    16.9 +    >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows));
   16.10  
   16.11  val _ =
   16.12    Outer_Syntax.command @{command_keyword have} "state local goal"
   16.13 @@ -570,8 +571,12 @@
   16.14      >> (Toplevel.proof o Proof.def_cmd));
   16.15  
   16.16  val _ =
   16.17 +  Outer_Syntax.command @{command_keyword consider} "state cases rule"
   16.18 +    (Parse_Spec.obtains >> (Toplevel.proof' o Obtain.consider_cmd));
   16.19 +
   16.20 +val _ =
   16.21    Outer_Syntax.command @{command_keyword obtain} "generalized elimination"
   16.22 -    (Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement
   16.23 +    (Parse.parbinding -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement
   16.24        >> (fn ((x, y), z) => Toplevel.proof' (Obtain.obtain_cmd x y z)));
   16.25  
   16.26  val _ =
    17.1 --- a/src/Pure/Isar/object_logic.ML	Sat Jun 13 19:23:41 2015 +0100
    17.2 +++ b/src/Pure/Isar/object_logic.ML	Sat Jun 13 22:44:22 2015 +0200
    17.3 @@ -125,7 +125,7 @@
    17.4      val aT = TFree (Name.aT, []);
    17.5      val T =
    17.6        the_default (aT --> propT) (Sign.const_type (Proof_Context.theory_of ctxt) c)
    17.7 -      |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
    17.8 +      |> Term.map_type_tvar (fn ((a, _), S) => TFree (a, S));
    17.9      val U = Term.domain_type T handle Match => aT;
   17.10    in Const (c, T) $ Free (x, U) end;
   17.11  
    18.1 --- a/src/Pure/Isar/obtain.ML	Sat Jun 13 19:23:41 2015 +0100
    18.2 +++ b/src/Pure/Isar/obtain.ML	Sat Jun 13 22:44:22 2015 +0200
    18.3 @@ -1,47 +1,21 @@
    18.4  (*  Title:      Pure/Isar/obtain.ML
    18.5      Author:     Markus Wenzel, TU Muenchen
    18.6  
    18.7 -The 'obtain' and 'guess' language elements -- generalized existence at
    18.8 -the level of proof texts: 'obtain' involves a proof that certain
    18.9 -fixes/assumes may be introduced into the present context; 'guess' is
   18.10 -similar, but derives these elements from the course of reasoning!
   18.11 -
   18.12 -  <chain_facts>
   18.13 -  obtain x where "A x" <proof> ==
   18.14 -
   18.15 -  have "!!thesis. (!!x. A x ==> thesis) ==> thesis"
   18.16 -  proof succeed
   18.17 -    fix thesis
   18.18 -    assume that [intro?]: "!!x. A x ==> thesis"
   18.19 -    <chain_facts>
   18.20 -    show thesis
   18.21 -      apply (insert that)
   18.22 -      <proof>
   18.23 -  qed
   18.24 -  fix x assm <<obtain_export>> "A x"
   18.25 -
   18.26 -
   18.27 -  <chain_facts>
   18.28 -  guess x <proof body> <proof end> ==
   18.29 -
   18.30 -  {
   18.31 -    fix thesis
   18.32 -    <chain_facts> have "PROP ?guess"
   18.33 -      apply magic      -- {* turns goal into "thesis ==> #thesis" *}
   18.34 -      <proof body>
   18.35 -      apply_end magic  -- {* turns final "(!!x. P x ==> thesis) ==> #thesis" into
   18.36 -        "#((!!x. A x ==> thesis) ==> thesis)" which is a finished goal state *}
   18.37 -      <proof end>
   18.38 -  }
   18.39 -  fix x assm <<obtain_export>> "A x"
   18.40 +Generalized existence and cases rules within Isar proof text.
   18.41  *)
   18.42  
   18.43  signature OBTAIN =
   18.44  sig
   18.45 -  val thatN: string
   18.46 -  val obtain: string -> (binding * typ option * mixfix) list ->
   18.47 +  val obtains_attributes: ('typ, 'term) Element.obtain list -> attribute list
   18.48 +  val parse_clause: Proof.context -> term ->
   18.49 +    (binding * typ option * mixfix) list -> string list -> term
   18.50 +  val read_obtains: Proof.context -> term -> Element.obtains -> (binding * term) list
   18.51 +  val cert_obtains: Proof.context -> term -> Element.obtains_i -> (binding * term) list
   18.52 +  val consider: Element.obtains_i -> bool -> Proof.state -> Proof.state
   18.53 +  val consider_cmd: Element.obtains -> bool -> Proof.state -> Proof.state
   18.54 +  val obtain: binding -> (binding * typ option * mixfix) list ->
   18.55      (Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state
   18.56 -  val obtain_cmd: string -> (binding * string option * mixfix) list ->
   18.57 +  val obtain_cmd: binding -> (binding * string option * mixfix) list ->
   18.58      (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
   18.59    val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
   18.60      ((string * cterm) list * thm list) * Proof.context
   18.61 @@ -52,7 +26,9 @@
   18.62  structure Obtain: OBTAIN =
   18.63  struct
   18.64  
   18.65 -(** obtain_export **)
   18.66 +(** specification elements **)
   18.67 +
   18.68 +(* obtain_export *)
   18.69  
   18.70  (*
   18.71    [x, A x]
   18.72 @@ -92,33 +68,136 @@
   18.73    (eliminate ctxt rule xs As, eliminate_term ctxt xs);
   18.74  
   18.75  
   18.76 +(* result declaration *)
   18.77  
   18.78 -(** obtain **)
   18.79 +fun obtains_attributes (obtains: ('typ, 'term) Element.obtain list) =
   18.80 +  let
   18.81 +    val case_names = obtains |> map_index (fn (i, (b, _)) =>
   18.82 +      if Binding.is_empty b then string_of_int (i + 1) else Name_Space.base_name b);
   18.83 +  in [Rule_Cases.consumes (~ (length obtains)), Rule_Cases.case_names case_names] end;
   18.84 +
   18.85  
   18.86 -fun bind_judgment ctxt name =
   18.87 +(* obtain thesis *)
   18.88 +
   18.89 +fun obtain_thesis ctxt =
   18.90    let
   18.91 -    val ([x], ctxt') = Proof_Context.add_fixes [(Binding.name name, NONE, NoSyn)] ctxt;
   18.92 -    val (t as _ $ Free v) = Object_Logic.fixed_judgment ctxt x;
   18.93 +    val ([x], ctxt') =
   18.94 +      Proof_Context.add_fixes [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)] ctxt;
   18.95 +    val t = Object_Logic.fixed_judgment ctxt x;
   18.96 +    val v = dest_Free (Object_Logic.drop_judgment ctxt t);
   18.97    in ((v, t), ctxt') end;
   18.98  
   18.99 -val thatN = "that";
  18.100 +
  18.101 +(* obtain clauses *)
  18.102 +
  18.103 +local
  18.104 +
  18.105 +fun prepare_clause parse_prop ctxt thesis vars raw_props =
  18.106 +  let
  18.107 +    val (xs', ctxt') = ctxt |> Proof_Context.add_fixes vars;
  18.108 +    val xs = map (Variable.check_name o #1) vars;
  18.109 +  in
  18.110 +    Logic.list_implies (map (parse_prop ctxt') raw_props, thesis)
  18.111 +    |> fold_rev (Logic.all_constraint (Variable.default_type ctxt')) (xs ~~ xs')
  18.112 +  end;
  18.113 +
  18.114 +fun prepare_obtains prep_var parse_prop ctxt thesis raw_obtains =
  18.115 +  let
  18.116 +    val all_types =
  18.117 +      fold_map prep_var (maps (fn (_, (vs, _)) => vs) raw_obtains)
  18.118 +        (ctxt |> Context_Position.set_visible false)
  18.119 +      |> #1 |> map_filter (fn (_, opt_T, _) => opt_T);
  18.120 +    val types_ctxt = fold Variable.declare_typ all_types ctxt;
  18.121 +
  18.122 +    val clauses =
  18.123 +      raw_obtains |> map (fn (_, (raw_vars, raw_props)) =>
  18.124 +        let
  18.125 +          val (vars, vars_ctxt) = fold_map prep_var raw_vars types_ctxt;
  18.126 +          val clause = prepare_clause parse_prop vars_ctxt thesis vars raw_props;
  18.127 +        in clause end)
  18.128 +      |> Syntax.check_terms ctxt;
  18.129 +  in map fst raw_obtains ~~ clauses end;
  18.130 +
  18.131 +in
  18.132 +
  18.133 +val parse_clause = prepare_clause Syntax.parse_prop;
  18.134 +
  18.135 +val read_obtains = prepare_obtains Proof_Context.read_var Syntax.parse_prop;
  18.136 +val cert_obtains = prepare_obtains Proof_Context.cert_var (K I);
  18.137 +
  18.138 +end;
  18.139 +
  18.140 +
  18.141 +
  18.142 +(** consider: generalized elimination and cases rule **)
  18.143 +
  18.144 +(*
  18.145 +  consider x where (a) "A x" | y (b) where "B x" | ... ==
  18.146 +
  18.147 +  have thesis
  18.148 +    if a [intro?]: "!!x. A x ==> thesis"
  18.149 +    and b [intro?]: "!!x. B x ==> thesis"
  18.150 +    and ...
  18.151 +    for thesis
  18.152 +    apply (insert that)
  18.153 +*)
  18.154 +
  18.155 +local
  18.156 +
  18.157 +fun gen_consider prep_obtains raw_obtains int state =
  18.158 +  let
  18.159 +    val _ = Proof.assert_forward_or_chain state;
  18.160 +    val ctxt = Proof.context_of state;
  18.161 +
  18.162 +    val ((_, thesis), thesis_ctxt) = obtain_thesis ctxt;
  18.163 +    val obtains = prep_obtains thesis_ctxt thesis raw_obtains;
  18.164 +    val atts = Rule_Cases.cases_open :: obtains_attributes raw_obtains;
  18.165 +  in
  18.166 +    state
  18.167 +    |> Proof.have NONE (K I)
  18.168 +      [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
  18.169 +      (map (fn (a, A) => ((a, [Context_Rules.intro_query NONE]), [(A, [])])) obtains)
  18.170 +      [((Binding.empty, atts), [(thesis, [])])] int
  18.171 +    |> (fn state' => state'
  18.172 +        |> Proof.refine_insert (Assumption.local_prems_of (Proof.context_of state') ctxt))
  18.173 +  end;
  18.174 +
  18.175 +in
  18.176 +
  18.177 +val consider = gen_consider cert_obtains;
  18.178 +val consider_cmd = gen_consider read_obtains;
  18.179 +
  18.180 +end;
  18.181 +
  18.182 +
  18.183 +
  18.184 +(** obtain: augmented context based on generalized existence rule **)
  18.185 +
  18.186 +(*
  18.187 +  obtain (a) x where "A x" <proof> ==
  18.188 +
  18.189 +  have thesis if a [intro?]: "!!x. A x ==> thesis" for thesis
  18.190 +    apply (insert that)
  18.191 +    <proof>
  18.192 +  fix x assm <<obtain_export>> "A x"
  18.193 +*)
  18.194  
  18.195  local
  18.196  
  18.197  fun gen_obtain prep_att prep_var prep_propp
  18.198 -    name raw_vars raw_asms int state =
  18.199 +    that_binding raw_vars raw_asms int state =
  18.200    let
  18.201      val _ = Proof.assert_forward_or_chain state;
  18.202      val ctxt = Proof.context_of state;
  18.203 -    val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
  18.204  
  18.205 -    (*obtain vars*)
  18.206 -    val ((xs', vars), fix_ctxt) = ctxt
  18.207 +    (*vars*)
  18.208 +    val ((_, thesis), thesis_ctxt) = obtain_thesis ctxt;
  18.209 +    val ((xs', vars), fix_ctxt) = thesis_ctxt
  18.210        |> fold_map prep_var raw_vars
  18.211        |-> (fn vars => Proof_Context.add_fixes vars ##>> pair vars);
  18.212      val xs = map (Variable.check_name o #1) vars;
  18.213  
  18.214 -    (*obtain asms*)
  18.215 +    (*asms*)
  18.216      val (propss, binds) = prep_propp fix_ctxt (map snd raw_asms);
  18.217      val props = flat propss;
  18.218      val declare_asms =
  18.219 @@ -128,7 +207,7 @@
  18.220        map (fn ((b, raw_atts), _) => (b, map (prep_att fix_ctxt) raw_atts)) raw_asms ~~
  18.221        map (map (rpair [])) propss;
  18.222  
  18.223 -    (*obtain params*)
  18.224 +    (*params*)
  18.225      val (params, params_ctxt) =
  18.226        declare_asms fix_ctxt |> fold_map Proof_Context.inferred_param xs' |>> map Free;
  18.227      val cparams = map (Thm.cterm_of params_ctxt) params;
  18.228 @@ -136,37 +215,27 @@
  18.229  
  18.230      val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt;
  18.231  
  18.232 -    (*obtain statements*)
  18.233 -    val thesisN = singleton (Name.variant_list xs) Auto_Bind.thesisN;
  18.234 -    val (thesis_var, thesis) = #1 (bind_judgment params_ctxt thesisN);
  18.235 -
  18.236 -    val that_name = if name = "" then thatN else name;
  18.237 +    (*statements*)
  18.238      val that_prop =
  18.239        Logic.list_rename_params xs
  18.240          (fold_rev Logic.all params (Logic.list_implies (props, thesis)));
  18.241 -    val obtain_prop =
  18.242 -      Logic.list_rename_params [Auto_Bind.thesisN]
  18.243 -        (Logic.all (Free thesis_var) (Logic.mk_implies (that_prop, thesis)));
  18.244  
  18.245 -    fun after_qed _ =
  18.246 -      Proof.local_qed (NONE, false)
  18.247 -      #> `Proof.the_fact #-> (fn rule =>
  18.248 -        Proof.fix vars
  18.249 -        #> Proof.map_context declare_asms
  18.250 -        #> Proof.assm (obtain_export params_ctxt rule cparams) asms);
  18.251 +    fun after_qed (result_ctxt, results) state' =
  18.252 +      let val [rule] = Proof_Context.export result_ctxt (Proof.context_of state') (flat results) in
  18.253 +        state'
  18.254 +        |> Proof.fix vars
  18.255 +        |> Proof.map_context declare_asms
  18.256 +        |> Proof.assm (obtain_export params_ctxt rule cparams) asms
  18.257 +      end;
  18.258    in
  18.259      state
  18.260 -    |> Proof.enter_forward
  18.261 -    |> Proof.have NONE (K I) [] [] [(Thm.empty_binding, [(obtain_prop, [])])] int
  18.262 +    |> Proof.have NONE after_qed
  18.263 +      [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
  18.264 +      [((that_binding, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
  18.265 +      [(Thm.empty_binding, [(thesis, [])])] int
  18.266 +    |> (fn state' => state'
  18.267 +        |> Proof.refine_insert (Assumption.local_prems_of (Proof.context_of state') ctxt))
  18.268      |> Proof.map_context (fold Variable.bind_term binds')
  18.269 -    |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
  18.270 -    |> Proof.fix [(Binding.name thesisN, NONE, NoSyn)]
  18.271 -    |> Proof.assume
  18.272 -      [((Binding.name that_name, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
  18.273 -    |> `Proof.the_facts
  18.274 -    ||> Proof.chain_facts chain_facts
  18.275 -    ||> Proof.show NONE after_qed [] [] [(Thm.empty_binding, [(thesis, [])])] false
  18.276 -    |-> Proof.refine_insert
  18.277    end;
  18.278  
  18.279  in
  18.280 @@ -191,7 +260,7 @@
  18.281  
  18.282  fun result tac facts ctxt =
  18.283    let
  18.284 -    val ((thesis_var, thesis), thesis_ctxt) = bind_judgment ctxt Auto_Bind.thesisN;
  18.285 +    val ((thesis_var, thesis), thesis_ctxt) = obtain_thesis ctxt;
  18.286      val st = Goal.init (Thm.cterm_of ctxt thesis);
  18.287      val rule =
  18.288        (case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) st of
  18.289 @@ -211,7 +280,23 @@
  18.290  
  18.291  
  18.292  
  18.293 -(** guess **)
  18.294 +(** guess: obtain based on tactical result **)
  18.295 +
  18.296 +(*
  18.297 +  <chain_facts>
  18.298 +  guess x <proof body> <proof end> ==
  18.299 +
  18.300 +  {
  18.301 +    fix thesis
  18.302 +    <chain_facts> have "PROP ?guess"
  18.303 +      apply magic      -- {* turns goal into "thesis ==> #thesis" *}
  18.304 +      <proof body>
  18.305 +      apply_end magic  -- {* turns final "(!!x. P x ==> thesis) ==> #thesis" into
  18.306 +        "#((!!x. A x ==> thesis) ==> thesis)" which is a finished goal state *}
  18.307 +      <proof end>
  18.308 +  }
  18.309 +  fix x assm <<obtain_export>> "A x"
  18.310 +*)
  18.311  
  18.312  local
  18.313  
  18.314 @@ -274,7 +359,7 @@
  18.315      val ctxt = Proof.context_of state;
  18.316      val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
  18.317  
  18.318 -    val (thesis_var, thesis) = #1 (bind_judgment ctxt Auto_Bind.thesisN);
  18.319 +    val (thesis_var, thesis) = #1 (obtain_thesis ctxt);
  18.320      val vars = ctxt
  18.321        |> fold_map prep_var raw_vars |-> fold_map inferred_type
  18.322        |> fst |> polymorphic ctxt;
    19.1 --- a/src/Pure/Isar/parse.ML	Sat Jun 13 19:23:41 2015 +0100
    19.2 +++ b/src/Pure/Isar/parse.ML	Sat Jun 13 22:44:22 2015 +0200
    19.3 @@ -90,7 +90,7 @@
    19.4    val where_: string parser
    19.5    val const_decl: (string * string * mixfix) parser
    19.6    val const_binding: (binding * string * mixfix) parser
    19.7 -  val params: (binding * string option) list parser
    19.8 +  val params: (binding * string option * mixfix) list parser
    19.9    val fixes: (binding * string option * mixfix) list parser
   19.10    val for_fixes: (binding * string option * mixfix) list parser
   19.11    val ML_source: Input.source parser
   19.12 @@ -358,13 +358,12 @@
   19.13  val const_decl = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
   19.14  val const_binding = binding -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
   19.15  
   19.16 -val params = Scan.repeat1 binding -- Scan.option ($$$ "::" |-- !!! typ)
   19.17 -  >> (fn (xs, T) => map (rpair T) xs);
   19.18 +val param_mixfix = binding -- Scan.option ($$$ "::" |-- typ) -- mixfix' >> (single o triple1);
   19.19 +val params =
   19.20 +  Scan.repeat1 binding -- Scan.option ($$$ "::" |-- !!! typ)
   19.21 +    >> (fn (xs, T) => map (fn x => (x, T, NoSyn)) xs);
   19.22  
   19.23 -val fixes =
   19.24 -  and_list1 (binding -- Scan.option ($$$ "::" |-- typ) -- mixfix' >> (single o triple1) ||
   19.25 -    params >> map (fn (x, y) => (x, y, NoSyn))) >> flat;
   19.26 -
   19.27 +val fixes = and_list1 (param_mixfix || params) >> flat;
   19.28  val for_fixes = Scan.optional ($$$ "for" |-- !!! fixes) [];
   19.29  
   19.30  
    20.1 --- a/src/Pure/Isar/parse_spec.ML	Sat Jun 13 19:23:41 2015 +0100
    20.2 +++ b/src/Pure/Isar/parse_spec.ML	Sat Jun 13 22:44:22 2015 +0200
    20.3 @@ -24,7 +24,8 @@
    20.4    val locale_expression: bool -> Expression.expression parser
    20.5    val context_element: Element.context parser
    20.6    val statement: (Attrib.binding * (string * string list) list) list parser
    20.7 -  val if_prems: (Attrib.binding * (string * string list) list) list parser
    20.8 +  val if_statement: (Attrib.binding * (string * string list) list) list parser
    20.9 +  val obtains: Element.obtains parser
   20.10    val general_statement: (Element.context list * Element.statement) parser
   20.11    val statement_keyword: string parser
   20.12  end;
   20.13 @@ -72,7 +73,7 @@
   20.14  val locale_fixes =
   20.15    Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- Parse.mixfix
   20.16      >> (single o Parse.triple1) ||
   20.17 -  Parse.params >> map (fn (x, y) => (x, y, NoSyn))) >> flat;
   20.18 +  Parse.params) >> flat;
   20.19  
   20.20  val locale_insts =
   20.21    Scan.optional
   20.22 @@ -131,18 +132,19 @@
   20.23  (* statements *)
   20.24  
   20.25  val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
   20.26 -
   20.27 -val if_prems = Scan.optional (Parse.$$$ "if" |-- Parse.!!! statement) [];
   20.28 +val if_statement = Scan.optional (Parse.$$$ "if" |-- Parse.!!! statement) [];
   20.29  
   20.30  val obtain_case =
   20.31    Parse.parbinding --
   20.32 -    (Scan.optional (Parse.and_list1 Parse.params --| Parse.where_ >> flat) [] --
   20.33 +    (Scan.optional (Parse.and_list1 Parse.fixes --| Parse.where_ >> flat) [] --
   20.34        (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat));
   20.35  
   20.36 +val obtains = Parse.enum1 "|" obtain_case;
   20.37 +
   20.38  val general_statement =
   20.39    statement >> (fn x => ([], Element.Shows x)) ||
   20.40    Scan.repeat context_element --
   20.41 -   (Parse.$$$ "obtains" |-- Parse.!!! (Parse.enum1 "|" obtain_case) >> Element.Obtains ||
   20.42 +   (Parse.$$$ "obtains" |-- Parse.!!! obtains >> Element.Obtains ||
   20.43      Parse.$$$ "shows" |-- Parse.!!! statement >> Element.Shows);
   20.44  
   20.45  val statement_keyword = Parse.$$$ "obtains" || Parse.$$$ "shows";
    21.1 --- a/src/Pure/Isar/proof.ML	Sat Jun 13 19:23:41 2015 +0100
    21.2 +++ b/src/Pure/Isar/proof.ML	Sat Jun 13 22:44:22 2015 +0200
    21.3 @@ -373,7 +373,7 @@
    21.4      val {context = ctxt, facts, mode, goal = _} = top state;
    21.5      val verbose = Config.get ctxt Proof_Context.verbose;
    21.6  
    21.7 -    fun prt_goal (SOME (_, (_, {using, goal, ...}))) =
    21.8 +    fun prt_goal (SOME (_, (_, {statement = _, using, goal, before_qed = _, after_qed = _}))) =
    21.9            pretty_sep
   21.10              (pretty_facts ctxt "using"
   21.11                (if mode <> Backward orelse null using then NONE else SOME using))
   21.12 @@ -1012,7 +1012,7 @@
   21.13            |> (fn (premss, ctxt') => ctxt'
   21.14                  |> not (null assumes_propss) ?
   21.15                    (snd o Proof_Context.note_thmss ""
   21.16 -                    [((Binding.name Auto_Bind.premsN, []),
   21.17 +                    [((Binding.name Auto_Bind.thatN, []),
   21.18                        [(Assumption.local_prems_of ctxt' ctxt, [])])])
   21.19                  |> (snd o Proof_Context.note_thmss ""
   21.20                      (assumes_bindings ~~ map (map (fn th => ([th], []))) premss)));
    22.1 --- a/src/Pure/Isar/rule_cases.ML	Sat Jun 13 19:23:41 2015 +0100
    22.2 +++ b/src/Pure/Isar/rule_cases.ML	Sat Jun 13 22:44:22 2015 +0200
    22.3 @@ -47,11 +47,13 @@
    22.4    val case_conclusion: string * string list -> attribute
    22.5    val is_inner_rule: thm -> bool
    22.6    val inner_rule: attribute
    22.7 +  val is_cases_open: thm -> bool
    22.8 +  val cases_open: attribute
    22.9 +  val internalize_params: thm -> thm
   22.10    val save: thm -> thm -> thm
   22.11    val get: thm -> ((string * string list) * string list) list * int
   22.12    val rename_params: string list list -> thm -> thm
   22.13    val params: string list list -> attribute
   22.14 -  val internalize_params: thm -> thm
   22.15    val mutual_rule: Proof.context -> thm list -> (int list * thm) option
   22.16    val strict_mutual_rule: Proof.context -> thm list -> int list * thm
   22.17  end;
   22.18 @@ -201,7 +203,9 @@
   22.19  
   22.20  
   22.21  
   22.22 -(** consume facts **)
   22.23 +(** annotations and operations on rules **)
   22.24 +
   22.25 +(* consume facts *)
   22.26  
   22.27  local
   22.28  
   22.29 @@ -256,8 +260,7 @@
   22.30  fun consumes n = Thm.mixed_attribute (apsnd (put_consumes (SOME n)));
   22.31  
   22.32  
   22.33 -
   22.34 -(** equality constraints **)
   22.35 +(* equality constraints *)
   22.36  
   22.37  val constraints_tagN = "constraints";
   22.38  
   22.39 @@ -281,8 +284,7 @@
   22.40  fun constraints n = Thm.mixed_attribute (apsnd (put_constraints (SOME n)));
   22.41  
   22.42  
   22.43 -
   22.44 -(** case names **)
   22.45 +(* case names *)
   22.46  
   22.47  val implode_args = space_implode ";";
   22.48  val explode_args = space_explode ";";
   22.49 @@ -303,8 +305,7 @@
   22.50  fun case_names cs = Thm.mixed_attribute (apsnd (name cs));
   22.51  
   22.52  
   22.53 -
   22.54 -(** hyp names **)
   22.55 +(* hyp names *)
   22.56  
   22.57  val implode_hyps = implode_args o map (suffix "," o space_implode ",");
   22.58  val explode_hyps = map (space_explode "," o unsuffix ",") o explode_args;
   22.59 @@ -325,8 +326,7 @@
   22.60    Thm.mixed_attribute (apsnd (name cs #> add_cases_hyp_names (SOME hs)));
   22.61  
   22.62  
   22.63 -
   22.64 -(** case conclusions **)
   22.65 +(* case conclusions *)
   22.66  
   22.67  val case_concl_tagN = "case_conclusion";
   22.68  
   22.69 @@ -355,8 +355,7 @@
   22.70  fun case_conclusion concl = Thm.mixed_attribute (apsnd (add_case_concl concl));
   22.71  
   22.72  
   22.73 -
   22.74 -(** inner rule **)
   22.75 +(* inner rule *)
   22.76  
   22.77  val inner_rule_tagN = "inner_rule";
   22.78  
   22.79 @@ -372,6 +371,35 @@
   22.80  val inner_rule = Thm.mixed_attribute (apsnd (put_inner_rule true));
   22.81  
   22.82  
   22.83 +(* parameter names *)
   22.84 +
   22.85 +val cases_open_tagN = "cases_open";
   22.86 +
   22.87 +fun is_cases_open th =
   22.88 +  AList.defined (op =) (Thm.get_tags th) cases_open_tagN;
   22.89 +
   22.90 +fun put_cases_open cases_open =
   22.91 +  Thm.untag_rule cases_open_tagN
   22.92 +  #> cases_open ? Thm.tag_rule (cases_open_tagN, "");
   22.93 +
   22.94 +val save_cases_open = put_cases_open o is_cases_open;
   22.95 +
   22.96 +val cases_open = Thm.mixed_attribute (apsnd (put_cases_open true));
   22.97 +
   22.98 +fun internalize_params rule =
   22.99 +  if is_cases_open rule then rule
  22.100 +  else
  22.101 +    let
  22.102 +      fun rename prem =
  22.103 +        let val xs =
  22.104 +          map (Name.internal o Name.clean o fst) (Logic.strip_params prem)
  22.105 +        in Logic.list_rename_params xs prem end;
  22.106 +      fun rename_prems prop =
  22.107 +        let val (As, C) = Logic.strip_horn prop
  22.108 +        in Logic.list_implies (map rename As, C) end;
  22.109 +    in Thm.renamed_prop (rename_prems (Thm.prop_of rule)) rule end;
  22.110 +
  22.111 +
  22.112  
  22.113  (** case declarations **)
  22.114  
  22.115 @@ -383,7 +411,8 @@
  22.116    save_case_names th #>
  22.117    save_cases_hyp_names th #>
  22.118    save_case_concls th #>
  22.119 -  save_inner_rule th;
  22.120 +  save_inner_rule th #>
  22.121 +  save_cases_open th;
  22.122  
  22.123  fun get th =
  22.124    let
  22.125 @@ -410,20 +439,6 @@
  22.126  fun params xss = Thm.rule_attribute (K (rename_params xss));
  22.127  
  22.128  
  22.129 -(* internalize parameter names *)
  22.130 -
  22.131 -fun internalize_params rule =
  22.132 -  let
  22.133 -    fun rename prem =
  22.134 -      let val xs =
  22.135 -        map (Name.internal o Name.clean o fst) (Logic.strip_params prem)
  22.136 -      in Logic.list_rename_params xs prem end;
  22.137 -    fun rename_prems prop =
  22.138 -      let val (As, C) = Logic.strip_horn prop
  22.139 -      in Logic.list_implies (map rename As, C) end;
  22.140 -  in Thm.renamed_prop (rename_prems (Thm.prop_of rule)) rule end;
  22.141 -
  22.142 -
  22.143  
  22.144  (** mutual_rule **)
  22.145  
    23.1 --- a/src/Pure/Isar/specification.ML	Sat Jun 13 19:23:41 2015 +0100
    23.2 +++ b/src/Pure/Isar/specification.ML	Sat Jun 13 22:44:22 2015 +0200
    23.3 @@ -103,32 +103,14 @@
    23.4  
    23.5  local
    23.6  
    23.7 -fun close_forms ctxt i xs As =
    23.8 +fun close_forms ctxt i As =
    23.9    let
   23.10 -    val commons = map #1 xs;
   23.11 -    val _ =
   23.12 -      (case duplicates (op =) commons of [] => ()
   23.13 -      | dups => error ("Duplicate local variables " ^ commas_quote dups));
   23.14 -    val frees = rev (fold (Variable.add_free_names ctxt) As (rev commons));
   23.15 +    val xs = rev (fold (Variable.add_free_names ctxt) As []);
   23.16      val types =
   23.17 -      map (Type_Infer.param i o rpair []) (Name.invent Name.context Name.aT (length frees));
   23.18 -    val uniform_typing = the o AList.lookup (op =) (frees ~~ types);
   23.19 -
   23.20 -    fun abs_body lev y (Abs (x, T, b)) = Abs (x, T, abs_body (lev + 1) y b)
   23.21 -      | abs_body lev y (t $ u) = abs_body lev y t $ abs_body lev y u
   23.22 -      | abs_body lev y (t as Free (x, T)) =
   23.23 -          if x = y then Type.constraint (uniform_typing x) (Type.constraint T (Bound lev))
   23.24 -          else t
   23.25 -      | abs_body _ _ a = a;
   23.26 -    fun close (y, U) B =
   23.27 -      let val B' = abs_body 0 y (Term.incr_boundvars 1 B)
   23.28 -      in if Term.is_dependent B' then Logic.all_const dummyT $ Abs (y, U, B') else B end;
   23.29 -    fun close_form A =
   23.30 -      let
   23.31 -        val occ_frees = rev (Variable.add_free_names ctxt A []);
   23.32 -        val bounds = xs @ map (rpair dummyT) (subtract (op =) commons occ_frees);
   23.33 -      in fold_rev close bounds A end;
   23.34 -  in map close_form As end;
   23.35 +      map (Type_Infer.param i o rpair []) (Name.invent Name.context Name.aT (length xs));
   23.36 +    val uniform_typing = AList.lookup (op =) (xs ~~ types);
   23.37 +    val close = fold_rev (Logic.dependent_all_constraint uniform_typing) (xs ~~ xs);
   23.38 +  in map close As end;
   23.39  
   23.40  fun prepare prep_var parse_prop prep_att do_close raw_vars raw_specss ctxt =
   23.41    let
   23.42 @@ -145,7 +127,7 @@
   23.43      val specs =
   23.44        (if do_close then
   23.45          #1 (fold_map
   23.46 -            (fn Ass => fn i => (burrow (close_forms params_ctxt i []) Ass, i + 1)) Asss' idx)
   23.47 +            (fn Ass => fn i => (burrow (close_forms params_ctxt i) Ass, i + 1)) Asss' idx)
   23.48        else Asss')
   23.49        |> flat |> burrow (Syntax.check_props params_ctxt);
   23.50      val specs_ctxt = params_ctxt |> (fold o fold) Variable.declare_term specs;
   23.51 @@ -347,11 +329,9 @@
   23.52        in (([], prems, stmt, NONE), goal_ctxt) end
   23.53    | Element.Obtains obtains =>
   23.54        let
   23.55 -        val case_names = obtains |> map_index (fn (i, (b, _)) =>
   23.56 -          if Binding.is_empty b then string_of_int (i + 1) else Name_Space.base_name b);
   23.57          val constraints = obtains |> map (fn (_, (vars, _)) =>
   23.58            Element.Constrains
   23.59 -            (vars |> map_filter (fn (x, SOME T) => SOME (Variable.check_name x, T) | _ => NONE)));
   23.60 +            (vars |> map_filter (fn (x, SOME T, _) => SOME (Variable.check_name x, T) | _ => NONE)));
   23.61  
   23.62          val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
   23.63          val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
   23.64 @@ -360,7 +340,7 @@
   23.65  
   23.66          fun assume_case ((name, (vars, _)), asms) ctxt' =
   23.67            let
   23.68 -            val bs = map fst vars;
   23.69 +            val bs = map (fn (b, _, _) => b) vars;
   23.70              val xs = map Variable.check_name bs;
   23.71              val props = map fst asms;
   23.72              val (params, _) = ctxt'
   23.73 @@ -377,8 +357,7 @@
   23.74              |>> (fn [(_, [th])] => th)
   23.75            end;
   23.76  
   23.77 -        val more_atts = map (Attrib.internal o K)
   23.78 -          [Rule_Cases.consumes (~ (length obtains)), Rule_Cases.case_names case_names];
   23.79 +        val more_atts = map (Attrib.internal o K) (Obtain.obtains_attributes obtains);
   23.80          val prems = Assumption.local_prems_of elems_ctxt ctxt;
   23.81          val stmt = [((Binding.empty, []), [(thesis, [])])];
   23.82  
   23.83 @@ -386,7 +365,7 @@
   23.84            |> (snd o Proof_Context.add_fixes [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)])
   23.85            |> fold_map assume_case (obtains ~~ propp)
   23.86            |-> (fn ths =>
   23.87 -            Proof_Context.note_thmss "" [((Binding.name Obtain.thatN, []), [(ths, [])])] #>
   23.88 +            Proof_Context.note_thmss "" [((Binding.name Auto_Bind.thatN, []), [(ths, [])])] #>
   23.89              #2 #> pair ths);
   23.90        in ((more_atts, prems, stmt, SOME facts), goal_ctxt) end);
   23.91  
    24.1 --- a/src/Pure/Pure.thy	Sat Jun 13 19:23:41 2015 +0100
    24.2 +++ b/src/Pure/Pure.thy	Sat Jun 13 22:44:22 2015 +0200
    24.3 @@ -55,6 +55,7 @@
    24.4    and "supply" :: prf_script % "proof"
    24.5    and "using" "unfolding" :: prf_decl % "proof"
    24.6    and "fix" "assume" "presume" "def" :: prf_asm % "proof"
    24.7 +  and "consider" :: prf_goal % "proof"
    24.8    and "obtain" :: prf_asm_goal % "proof"
    24.9    and "guess" :: prf_asm_goal_script % "proof"
   24.10    and "let" "write" :: prf_decl % "proof"
    25.1 --- a/src/Pure/logic.ML	Sat Jun 13 19:23:41 2015 +0100
    25.2 +++ b/src/Pure/logic.ML	Sat Jun 13 22:44:22 2015 +0200
    25.3 @@ -12,6 +12,8 @@
    25.4    val is_all: term -> bool
    25.5    val dest_all: term -> (string * typ) * term
    25.6    val list_all: (string * typ) list * term -> term
    25.7 +  val all_constraint: (string -> typ option) -> string * string -> term -> term
    25.8 +  val dependent_all_constraint: (string -> typ option) -> string * string -> term -> term
    25.9    val mk_equals: term * term -> term
   25.10    val dest_equals: term -> term * term
   25.11    val implies: term
   25.12 @@ -109,6 +111,35 @@
   25.13    | list_all ((a, T) :: vars, t) = all_const T $ Abs (a, T, list_all (vars, t));
   25.14  
   25.15  
   25.16 +(* operations before type-inference *)
   25.17 +
   25.18 +local
   25.19 +
   25.20 +fun abs_body default_type z tm =
   25.21 +  let
   25.22 +    fun abs lev (Abs (x, T, b)) = Abs (x, T, abs (lev + 1) b)
   25.23 +      | abs lev (t $ u) = abs lev t $ abs lev u
   25.24 +      | abs lev (a as Free (x, T)) =
   25.25 +          if x = z then
   25.26 +            Type.constraint (the_default dummyT (default_type x))
   25.27 +              (Type.constraint T (Bound lev))
   25.28 +          else a
   25.29 +      | abs _ a = a;
   25.30 +  in abs 0 (Term.incr_boundvars 1 tm) end;
   25.31 +
   25.32 +in
   25.33 +
   25.34 +fun all_constraint default_type (y, z) t =
   25.35 +  all_const dummyT $ Abs (y, dummyT, abs_body default_type z t);
   25.36 +
   25.37 +fun dependent_all_constraint default_type (y, z) t =
   25.38 +  let val t' = abs_body default_type z t
   25.39 +  in if Term.is_dependent t' then all_const dummyT $ Abs (y, dummyT, t') else t end;
   25.40 +
   25.41 +end;
   25.42 +
   25.43 +
   25.44 +
   25.45  (** equality **)
   25.46  
   25.47  fun mk_equals (t, u) =
    26.1 --- a/src/Tools/induct.ML	Sat Jun 13 19:23:41 2015 +0100
    26.2 +++ b/src/Tools/induct.ML	Sat Jun 13 22:44:22 2015 +0200
    26.3 @@ -483,25 +483,32 @@
    26.4        |> simp ? mark_constraints (Rule_Cases.get_constraints r) ctxt
    26.5        |> pair (Rule_Cases.get r);
    26.6  
    26.7 +    val (opt_rule', facts') =
    26.8 +      (case (opt_rule, facts) of
    26.9 +        (NONE, th :: ths) =>
   26.10 +          if is_some (Object_Logic.elim_concl ctxt th) then (SOME th, ths)
   26.11 +          else (opt_rule, facts)
   26.12 +      | _ => (opt_rule, facts));
   26.13 +
   26.14      val ruleq =
   26.15 -      (case opt_rule of
   26.16 +      (case opt_rule' of
   26.17          SOME r => Seq.single (inst_rule r)
   26.18        | NONE =>
   26.19 -          (get_casesP ctxt facts @ get_casesT ctxt insts @ [Induct_Args.cases_default])
   26.20 +          (get_casesP ctxt facts' @ get_casesT ctxt insts @ [Induct_Args.cases_default])
   26.21            |> tap (trace_rules ctxt casesN)
   26.22            |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
   26.23    in
   26.24      fn i => fn st =>
   26.25        ruleq
   26.26 -      |> Seq.maps (Rule_Cases.consume ctxt [] facts)
   26.27 -      |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
   26.28 +      |> Seq.maps (Rule_Cases.consume ctxt [] facts')
   26.29 +      |> Seq.maps (fn ((cases, (_, facts'')), rule) =>
   26.30          let
   26.31            val rule' = rule
   26.32              |> simp ? (simplified_rule' ctxt #> unmark_constraints ctxt);
   26.33          in
   26.34            CASES (Rule_Cases.make_common ctxt
   26.35                (Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
   26.36 -            ((Method.insert_tac more_facts THEN' resolve_tac ctxt [rule'] THEN_ALL_NEW
   26.37 +            ((Method.insert_tac facts'' THEN' resolve_tac ctxt [rule'] THEN_ALL_NEW
   26.38                  (if simp then TRY o trivial_tac ctxt else K all_tac)) i) st
   26.39          end)
   26.40    end;