author wenzelm Sat Jun 13 22:44:22 2015 +0200 (2015-06-13) changeset 60460 abee0de69a89 parent 60442 310853646597 parent 60459 2761a2249c83 child 60461 22995ec9fefd child 60464 16bed2709b70
merged
 NEWS file | annotate | diff | revisions
     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.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.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.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.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.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.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}{\indexdef{}{syntax}{#1}}
3.5  \newcommand{\indexisarelem}{\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.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.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;
`
{"ft_lang_label":"__label__en","ft_lang_prob":0.5455979,"math_prob":0.9611726,"size":65292,"snap":"2020-34-2020-40","text_gpt3_token_len":22519,"char_repetition_ratio":0.12146183,"word_repetition_ratio":0.116373226,"special_character_ratio":0.46491146,"punctuation_ratio":0.22614549,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.98506314,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2020-08-07T10:31:14Z\",\"WARC-Record-ID\":\"<urn:uuid:5f795754-fc28-4107-b6d0-c7cb930368b5>\",\"Content-Length\":\"204134\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:eac0d8a7-82d5-487e-a1ca-9e10d71cb1f0>\",\"WARC-Concurrent-To\":\"<urn:uuid:3de7c0bf-df4a-43d2-ba24-476af8bc0bca>\",\"WARC-IP-Address\":\"131.159.46.82\",\"WARC-Target-URI\":\"http://isabelle.in.tum.de/repos/isabelle/rev/abee0de69a89\",\"WARC-Payload-Digest\":\"sha1:KENTKXYJ3LHG4EDT5X5CMRAA6ME35N4O\",\"WARC-Block-Digest\":\"sha1:OYGAJMYEZZY65SCBMU3QPXDQ765IWZ5N\",\"WARC-Identified-Payload-Type\":\"application/xhtml+xml\",\"warc_filename\":\"/cc_download/warc_2020/CC-MAIN-2020-34/CC-MAIN-2020-34_segments_1596439737172.50_warc_CC-MAIN-20200807083754-20200807113754-00548.warc.gz\"}"}