--- a/NEWS Sat Jun 13 19:23:41 2015 +0100
+++ b/NEWS Sat Jun 13 22:44:22 2015 +0200
@@ -24,13 +24,13 @@
for x :: 'a and y :: 'a
<proof>
-The local assumptions are always bound to the name "prems". The result
-is exported from context of the statement as usual. The above roughly
+The local assumptions are bound to the name "that". The result is
+exported from context of the statement as usual. The above roughly
corresponds to a raw proof block like this:
{
fix x :: 'a and y :: 'a
- assume prems: "A x" "B y"
+ assume that: "A x" "B y"
have "C x y" <proof>
}
note result = this
@@ -38,6 +38,27 @@
* New command 'supply' supports fact definitions during goal refinement
('apply' scripts).
+* New command 'consider' states rules for generalized elimination and
+case splitting. This is like a toplevel statement "theorem obtains" used
+within a proof body; or like a multi-branch 'obtain' without activation
+of the local context elements yet.
+
+* Proof method "cases" allows to specify the rule as first entry of
+chained facts. This is particularly useful with 'consider':
+
+ consider (a) A | (b) B | (c) C <proof>
+ then have something
+ proof cases
+ case a
+ then show ?thesis <proof>
+ next
+ case b
+ then show ?thesis <proof>
+ next
+ case c
+ then show ?thesis <proof>
+ qed
+
*** Pure ***
--- a/src/Doc/Isar_Ref/Proof.thy Sat Jun 13 19:23:41 2015 +0100
+++ b/src/Doc/Isar_Ref/Proof.thy Sat Jun 13 22:44:22 2015 +0200
@@ -435,21 +435,22 @@
@@{command schematic_corollary}) (stmt | statement)
;
(@@{command have} | @@{command show} | @@{command hence} | @@{command thus})
- stmt if_prems @{syntax for_fixes}
+ stmt (@'if' stmt)? @{syntax for_fixes}
;
@@{command print_statement} @{syntax modes}? @{syntax thmrefs}
;
stmt: (@{syntax props} + @'and')
;
- if_prems: (@'if' stmt)?
- ;
statement: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} *) \<newline>
conclusion
;
- conclusion: @'shows' stmt | @'obtains' (@{syntax par_name}? obtain_case + '|')
+ conclusion: @'shows' stmt | @'obtains' @{syntax obtain_clauses}
;
- obtain_case: (@{syntax vars} + @'and') @'where' (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
+ @{syntax_def obtain_clauses}: (@{syntax par_name}? obtain_case + '|')
+ ;
+ @{syntax_def obtain_case}: (@{syntax vars} + @'and') @'where'
+ (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
\<close>}
\begin{description}
@@ -523,11 +524,10 @@
@{variable_ref "?thesis"}) to be bound automatically, see also
\secref{sec:term-abbrev}.
- The optional case names of @{element_ref "obtains"} have a twofold
- meaning: (1) in the proof of this claim they refer to the local context
- introductions, (2) in the resulting rule they become annotations for
- symbolic case splits, e.g.\ for the @{method_ref cases} method
- (\secref{sec:cases-induct}).
+ Structured goal statements involving @{keyword_ref "if"} define the
+ special fact ``@{text that}'' to refer to these assumptions in the proof
+ body. The user may provide separate names according to the syntax of the
+ statement.
\<close>
@@ -853,15 +853,6 @@
subsection \<open>Emulating tactic scripts \label{sec:tactic-commands}\<close>
text \<open>
- The Isar provides separate commands to accommodate tactic-style
- proof scripts within the same system. While being outside the
- orthodox Isar proof language, these might come in handy for
- interactive exploration and debugging, or even actual tactical proof
- within new-style theories (to benefit from document preparation, for
- example). See also \secref{sec:tactics} for actual tactics, that
- have been encapsulated as proof methods. Proper proof methods may
- be used in scripts, too.
-
\begin{matharray}{rcl}
@{command_def "supply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
@{command_def "apply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
@@ -872,6 +863,15 @@
@{command_def "back"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
\end{matharray}
+ The Isar language provides separate commands to accommodate tactic-style
+ proof scripts within the same system. While being outside the
+ orthodox Isar proof language, these might come in handy for
+ interactive exploration and debugging, or even actual tactical proof
+ within new-style theories (to benefit from document preparation, for
+ example). See also \secref{sec:tactics} for actual tactics, that
+ have been encapsulated as proof methods. Proper proof methods may
+ be used in scripts, too.
+
@{rail \<open>
@@{command supply} (@{syntax thmdef}? @{syntax thmrefs} + @'and')
;
@@ -979,83 +979,125 @@
(*<*)end(*>*)
-section \<open>Generalized elimination \label{sec:obtain}\<close>
+section \<open>Generalized elimination and case splitting \label{sec:obtain}\<close>
text \<open>
\begin{matharray}{rcl}
+ @{command_def "consider"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
@{command_def "obtain"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
@{command_def "guess"}@{text "\<^sup>*"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
\end{matharray}
- Generalized elimination means that additional elements with certain
- properties may be introduced in the current context, by virtue of a
- locally proven ``soundness statement''. Technically speaking, the
- @{command "obtain"} language element is like a declaration of
- @{command "fix"} and @{command "assume"} (see also see
- \secref{sec:proof-context}), together with a soundness proof of its
- additional claim. According to the nature of existential reasoning,
- assumptions get eliminated from any result exported from the context
- later, provided that the corresponding parameters do \emph{not}
- occur in the conclusion.
+ Generalized elimination means that hypothetical parameters and premises
+ may be introduced in the current context, potentially with a split into
+ cases. This works by virtue of a locally proven rule that establishes the
+ soundness of this temporary context extension. As representative examples,
+ one may think of standard rules from Isabelle/HOL like this:
+
+ \medskip
+ \begin{tabular}{ll}
+ @{text "\<exists>x. B x \<Longrightarrow> (\<And>x. B x \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\
+ @{text "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\
+ @{text "A \<or> B \<Longrightarrow> (A \<Longrightarrow> thesis) \<Longrightarrow> (B \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\
+ \end{tabular}
+ \medskip
+
+ In general, these particular rules and connectives need to get involved at
+ all: this concept works directly in Isabelle/Pure via Isar commands
+ defined below. In particular, the logic of elimination and case splitting
+ is delegated to an Isar proof, which often involves automated tools.
@{rail \<open>
- @@{command obtain} @{syntax par_name}? (@{syntax vars} + @'and')
+ @@{command consider} @{syntax obtain_clauses}
+ ;
+ @@{command obtain} @{syntax par_name}? (@{syntax "fixes"} + @'and')
@'where' (@{syntax props} + @'and')
;
- @@{command guess} (@{syntax vars} + @'and')
+ @@{command guess} (@{syntax "fixes"} + @'and')
\<close>}
- The derived Isar command @{command "obtain"} is defined as follows
- (where @{text "b\<^sub>1, \<dots>, b\<^sub>k"} shall refer to (optional)
- facts indicated for forward chaining).
+ \begin{description}
+
+ \item @{command consider}~@{text "(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x
+ | (b) \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots> "} states a rule for case
+ splitting into separate subgoals, such that each case involves new
+ parameters and premises. After the proof is finished, the resulting rule
+ may be used directly with the @{method cases} proof method
+ (\secref{sec:cases-induct}), in order to perform actual case-splitting of
+ the proof text via @{command case} and @{command next} as usual.
+
+ Optional names in round parentheses refer to case names: in the proof of
+ the rule this is a fact name, in the resulting rule it is used as
+ annotation with the @{attribute_ref case_names} attribute.
+
+ \medskip Formally, the command @{command consider} is defined as derived
+ Isar language element as follows:
+
\begin{matharray}{l}
- @{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]
- \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"} \\
- \quad @{command "proof"}~@{method succeed} \\
- \qquad @{command "fix"}~@{text thesis} \\
- \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"} \\
- \qquad @{command "then"}~@{command "show"}~@{text thesis} \\
- \quad\qquad @{command "apply"}~@{text -} \\
- \quad\qquad @{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>k \<langle>proof\<rangle>"} \\
- \quad @{command "qed"} \\
- \quad @{command "fix"}~@{text "x\<^sub>1 \<dots> x\<^sub>m"}~@{command "assume"}@{text "\<^sup>* a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} \\
+ @{command "consider"}~@{text "(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x | (b) \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots> \<equiv>"} \\[1ex]
+ \quad @{command "have"}~@{text "[case_names a b \<dots>]: thesis"} \\
+ \qquad @{text "\<IF> a [Pure.intro?]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis"} \\
+ \qquad @{text "\<AND> b [Pure.intro?]: \<And>\<^vec>y. \<^vec>B \<^vec>y \<Longrightarrow> thesis"} \\
+ \qquad @{text "\<AND> \<dots>"} \\
+ \qquad @{text "\<FOR> thesis"} \\
+ \qquad @{command "apply"}~@{text "(insert a b \<dots>)"} \\
\end{matharray}
- Typically, the soundness proof is relatively straight-forward, often
- just by canonical automated tools such as ``@{command "by"}~@{text
- simp}'' or ``@{command "by"}~@{text blast}''. Accordingly, the
- ``@{text that}'' reduction above is declared as simplification and
- introduction rule.
+ See also \secref{sec:goals} for @{keyword "obtains"} in toplevel goal
+ statements, as well as @{command print_statement} to print existing rules
+ in a similar format.
- In a sense, @{command "obtain"} represents at the level of Isar
- proofs what would be meta-logical existential quantifiers and
- conjunctions. This concept has a broad range of useful
- applications, ranging from plain elimination (or introduction) of
- object-level existential and conjunctions, to elimination over
- results of symbolic evaluation of recursive definitions, for
- example. Also note that @{command "obtain"} without parameters acts
- much like @{command "have"}, where the result is treated as a
- genuine assumption.
+ \item @{command obtain}~@{text "\<^vec>x \<WHERE> \<^vec>A \<^vec>x"}
+ states a generalized elimination rule with exactly one case. After the
+ proof is finished, it is activated for the subsequent proof text: the
+ context is augmented via @{command fix}~@{text "\<^vec>x"} @{command
+ assume}~@{text "\<^vec>A \<^vec>x"}, with special provisions to export
+ later results by discharging these assumptions again.
+
+ Note that according to the parameter scopes within the elimination rule,
+ results \emph{must not} refer to hypothetical parameters; otherwise the
+ export will fail! This restriction conforms to the usual manner of
+ existential reasoning in Natural Deduction.
+
+ \medskip Formally, the command @{command obtain} is defined as derived
+ Isar language element as follows, using an instrumented variant of
+ @{command assume}:
- An alternative name to be used instead of ``@{text that}'' above may
- be given in parentheses.
+ \begin{matharray}{l}
+ @{command "obtain"}~@{text "\<^vec>x \<WHERE> a: \<^vec>A \<^vec>x \<langle>proof\<rangle> \<equiv>"} \\[1ex]
+ \quad @{command "have"}~@{text "thesis"} \\
+ \qquad @{text "\<IF> that [Pure.intro?]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis"} \\
+ \qquad @{text "\<FOR> thesis"} \\
+ \qquad @{command "apply"}~@{text "(insert that)"} \\
+ \qquad @{text "\<langle>proof\<rangle>"} \\
+ \quad @{command "fix"}~@{text "\<^vec>x"}~@{command "assume"}@{text "\<^sup>* a: \<^vec>A \<^vec>x"} \\
+ \end{matharray}
+
+ \item @{command guess} is similar to @{command obtain}, but it derives the
+ obtained context elements from the course of tactical reasoning in the
+ proof. Thus it can considerably obscure the proof: it is classified as
+ \emph{improper}.
- \medskip The improper variant @{command "guess"} is similar to
- @{command "obtain"}, but derives the obtained statement from the
- course of reasoning! The proof starts with a fixed goal @{text
- thesis}. The subsequent proof may refine this to anything of the
- form like @{text "\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots>
- \<phi>\<^sub>n \<Longrightarrow> thesis"}, but must not introduce new subgoals. The
- final goal state is then used as reduction rule for the obtain
- scheme described above. Obtained parameters @{text "x\<^sub>1, \<dots>,
- x\<^sub>m"} are marked as internal by default, which prevents the
- proof context from being polluted by ad-hoc variables. The variable
- names and type constraints given as arguments for @{command "guess"}
- specify a prefix of obtained parameters explicitly in the text.
+ A proof with @{command guess} starts with a fixed goal @{text thesis}. The
+ subsequent refinement steps may turn this to anything of the form @{text
+ "\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis"}, but without splitting into new
+ subgoals. The final goal state is then used as reduction rule for the
+ obtain pattern described above. Obtained parameters @{text "\<^vec>x"} are
+ marked as internal by default, and thus inaccessible in the proof text.
+ The variable names and type constraints given as arguments for @{command
+ "guess"} specify a prefix of accessible parameters.
- It is important to note that the facts introduced by @{command
- "obtain"} and @{command "guess"} may not be polymorphic: any
- type-variables occurring here are fixed in the present context!
+ \end{description}
+
+ In the proof of @{command consider} and @{command obtain} the local
+ premises are always bound to the fact name ``@{text that}'', according to
+ structured Isar statements involving @{keyword_ref "if"}
+ (\secref{sec:goals}).
+
+ Facts that are established by @{command "obtain"} and @{command "guess"}
+ may not be polymorphic: any type-variables occurring here are fixed in the
+ present context. This is a natural consequence of the role of @{command
+ fix} and @{command assume} in these constructs.
\<close>
@@ -1372,6 +1414,7 @@
\medskip
\begin{tabular}{llll}
facts & & arguments & rule \\\hline
+ @{text "\<turnstile> R"} & @{method cases} & & implicit rule @{text R} \\
& @{method cases} & & classical case split \\
& @{method cases} & @{text t} & datatype exhaustion (type of @{text t}) \\
@{text "\<turnstile> A t"} & @{method cases} & @{text "\<dots>"} & inductive predicate/set elimination (of @{text A}) \\
--- a/src/Doc/isar.sty Sat Jun 13 19:23:41 2015 +0100
+++ b/src/Doc/isar.sty Sat Jun 13 22:44:22 2015 +0200
@@ -13,6 +13,7 @@
\newcommand{\indexouternonterm}[1]{\indexdef{}{syntax}{#1}}
\newcommand{\indexisarelem}[1]{\indexdef{}{element}{#1}}
+\newcommand{\isasymIF}{\isakeyword{if}}
\newcommand{\isasymFOR}{\isakeyword{for}}
\newcommand{\isasymAND}{\isakeyword{and}}
\newcommand{\isasymIS}{\isakeyword{is}}
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy Sat Jun 13 19:23:41 2015 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy Sat Jun 13 22:44:22 2015 +0200
@@ -69,7 +69,8 @@
fix y assume "y \<in> F"
then have "a y \<in> ?S" by blast
with xi have "a y \<le> xi" by (rule lub.upper)
- } moreover {
+ }
+ moreover {
fix y assume y: "y \<in> F"
from xi have "xi \<le> b y"
proof (rule lub.least)
@@ -78,7 +79,8 @@
from u y have "a u \<le> b y" by (rule r)
with au show "au \<le> b y" by (simp only:)
qed
- } ultimately show "\<exists>xi. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y" by blast
+ }
+ ultimately show "\<exists>xi. \<forall>y \<in> F. a y \<le> xi \<and> xi \<le> b y" by blast
qed
text \<open>
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Sat Jun 13 19:23:41 2015 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Sat Jun 13 22:44:22 2015 +0200
@@ -126,11 +126,11 @@
@{text x} and @{text y} are contained in the greater
one. \label{cases1}\<close>
- from cM c'' c' have "graph H'' h'' \<subseteq> graph H' h' \<or> graph H' h' \<subseteq> graph H'' h''"
- (is "?case1 \<or> ?case2") ..
+ from cM c'' c' consider "graph H'' h'' \<subseteq> graph H' h'" | "graph H' h' \<subseteq> graph H'' h''"
+ by (blast dest: chainsD)
then show ?thesis
- proof
- assume ?case1
+ proof cases
+ case 1
have "(x, h x) \<in> graph H'' h''" by fact
also have "\<dots> \<subseteq> graph H' h'" by fact
finally have xh:"(x, h x) \<in> graph H' h'" .
@@ -139,14 +139,16 @@
moreover from cM u and c' have "graph H' h' \<subseteq> graph H h" by blast
ultimately show ?thesis using * by blast
next
- assume ?case2
+ case 2
from x_hx have "x \<in> H''" ..
- moreover {
+ moreover have "y \<in> H''"
+ proof -
have "(y, h y) \<in> graph H' h'" by (rule y_hy)
also have "\<dots> \<subseteq> graph H'' h''" by fact
finally have "(y, h y) \<in> graph H'' h''" .
- } then have "y \<in> H''" ..
- moreover from cM u and c'' have "graph H'' h'' \<subseteq> graph H h" by blast
+ then show ?thesis ..
+ qed
+ moreover from u c'' have "graph H'' h'' \<subseteq> graph H h" by blast
ultimately show ?thesis using ** by blast
qed
qed
@@ -179,10 +181,11 @@
or vice versa, since both @{text "G\<^sub>1"} and @{text
"G\<^sub>2"} are members of @{text c}. \label{cases2}\<close>
- from cM G1 G2 have "G1 \<subseteq> G2 \<or> G2 \<subseteq> G1" (is "?case1 \<or> ?case2") ..
+ from cM G1 G2 consider "G1 \<subseteq> G2" | "G2 \<subseteq> G1"
+ by (blast dest: chainsD)
then show ?thesis
- proof
- assume ?case1
+ proof cases
+ case 1
with xy' G2_rep have "(x, y) \<in> graph H2 h2" by blast
then have "y = h2 x" ..
also
@@ -190,7 +193,7 @@
then have "z = h2 x" ..
finally show ?thesis .
next
- assume ?case2
+ case 2
with xz' G1_rep have "(x, z) \<in> graph H1 h1" by blast
then have "z = h1 x" ..
also
--- a/src/HOL/Isar_Examples/Hoare_Ex.thy Sat Jun 13 19:23:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Hoare_Ex.thy Sat Jun 13 22:44:22 2015 +0200
@@ -224,9 +224,9 @@
proof hoare
show "?inv 0 1" by simp
show "?inv (s + i) (i + 1)" if "?inv s i \<and> i \<noteq> n" for s i
- using prems by simp
+ using that by simp
show "s = ?sum n" if "?inv s i \<and> \<not> i \<noteq> n" for s i
- using prems by simp
+ using that by simp
qed
qed
--- a/src/HOL/Isar_Examples/Nested_Datatype.thy Sat Jun 13 19:23:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Nested_Datatype.thy Sat Jun 13 22:44:22 2015 +0200
@@ -39,10 +39,10 @@
proof (induct t rule: subst_term.induct)
show "?P (Var a)" for a by simp
show "?P (App b ts)" if "?Q ts" for b ts
- using prems by (simp only: subst_simps)
+ using that by (simp only: subst_simps)
show "?Q []" by simp
show "?Q (t # ts)" if "?P t" "?Q ts" for t ts
- using prems by (simp only: subst_simps)
+ using that by (simp only: subst_simps)
qed
qed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_Examples/Structured_Statements.thy Sat Jun 13 22:44:22 2015 +0200
@@ -0,0 +1,44 @@
+(* Title: HOL/Isar_Examples/Structured_Statements.thy
+ Author: Makarius
+*)
+
+section \<open>Structured statements within Isar proofs\<close>
+
+theory Structured_Statements
+imports Main
+begin
+
+notepad
+begin
+
+ fix A B :: bool
+
+ have iff_comm: "(A \<and> B) \<longleftrightarrow> (B \<and> A)"
+ proof
+ show "B \<and> A" if "A \<and> B"
+ proof
+ show B using that ..
+ show A using that ..
+ qed
+ show "A \<and> B" if "B \<and> A"
+ proof
+ show A using that ..
+ show B using that ..
+ qed
+ qed
+
+ text \<open>Alternative proof, avoiding redundant copy of symmetric argument.\<close>
+ have iff_comm: "(A \<and> B) \<longleftrightarrow> (B \<and> A)"
+ proof
+ show "B \<and> A" if "A \<and> B" for A B
+ proof
+ show B using that ..
+ show A using that ..
+ qed
+ then show "A \<and> B" if "B \<and> A"
+ by this (rule that)
+ qed
+
+end
+
+end
\ No newline at end of file
--- a/src/HOL/Library/Convex.thy Sat Jun 13 19:23:41 2015 +0100
+++ b/src/HOL/Library/Convex.thy Sat Jun 13 22:44:22 2015 +0200
@@ -538,7 +538,7 @@
by auto
let ?a = "\<lambda>j. a j / (1 - a i)"
have a_nonneg: "?a j \<ge> 0" if "j \<in> s" for j
- using i0 insert prems by fastforce
+ using i0 insert that by fastforce
have "(\<Sum> j \<in> insert i s. a j) = 1"
using insert by auto
then have "(\<Sum> j \<in> s. a j) = 1 - a i"
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Sat Jun 13 19:23:41 2015 +0100
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Sat Jun 13 22:44:22 2015 +0200
@@ -159,8 +159,9 @@
assume IH: "\<forall>m<n. m \<noteq> 0 \<longrightarrow> (\<exists>z. cmod (1 + b * z ^ m) < 1)"
assume n: "n \<noteq> 0"
let ?P = "\<lambda>z n. cmod (1 + b * z ^ n) < 1"
- {
- assume e: "even n"
+ show "\<exists>z. ?P z n"
+ proof cases
+ assume "even n"
then have "\<exists>m. n = 2 * m"
by presburger
then obtain m where m: "n = 2 * m"
@@ -170,19 +171,17 @@
with IH[rule_format, of m] obtain z where z: "?P z m"
by blast
from z have "?P (csqrt z) n"
- by (simp add: m power_mult power2_csqrt)
- then have "\<exists>z. ?P z n" ..
- }
- moreover
- {
- assume o: "odd n"
- have th0: "cmod (complex_of_real (cmod b) / b) = 1"
- using b by (simp add: norm_divide)
- from o have "\<exists>m. n = Suc (2 * m)"
+ by (simp add: m power_mult)
+ then show ?thesis ..
+ next
+ assume "odd n"
+ then have "\<exists>m. n = Suc (2 * m)"
by presburger+
then obtain m where m: "n = Suc (2 * m)"
by blast
- from unimodular_reduce_norm[OF th0] o
+ have th0: "cmod (complex_of_real (cmod b) / b) = 1"
+ using b by (simp add: norm_divide)
+ from unimodular_reduce_norm[OF th0] \<open>odd n\<close>
have "\<exists>v. cmod (complex_of_real (cmod b) / b + v^n) < 1"
apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1")
apply (rule_tac x="1" in exI)
@@ -206,7 +205,7 @@
then obtain v where v: "cmod (complex_of_real (cmod b) / b + v^n) < 1"
by blast
let ?w = "v / complex_of_real (root n (cmod b))"
- from odd_real_root_pow[OF o, of "cmod b"]
+ from odd_real_root_pow[OF \<open>odd n\<close>, of "cmod b"]
have th1: "?w ^ n = v^n / complex_of_real (cmod b)"
by (simp add: power_divide of_real_power[symmetric])
have th2:"cmod (complex_of_real (cmod b) / b) = 1"
@@ -222,9 +221,8 @@
done
from mult_left_less_imp_less[OF th4 th3]
have "?P ?w n" unfolding th1 .
- then have "\<exists>z. ?P z n" ..
- }
- ultimately show "\<exists>z. ?P z n" by blast
+ then show ?thesis ..
+ qed
qed
text \<open>Bolzano-Weierstrass type property for closed disc in complex plane.\<close>
@@ -1020,51 +1018,44 @@
"(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow>
p dvd (q ^ (degree p)) \<or> (p = 0 \<and> q = 0)"
proof -
- show ?thesis
- proof (cases "p = 0")
- case True
+ consider "p = 0" | "p \<noteq> 0" "degree p = 0" | n where "p \<noteq> 0" "degree p = Suc n"
+ by (cases "degree p") auto
+ then show ?thesis
+ proof cases
+ case 1
then have eq: "(\<forall>x. poly p x = (0::complex) \<longrightarrow> poly q x = 0) \<longleftrightarrow> q = 0"
by (auto simp add: poly_all_0_iff_0)
{
assume "p dvd (q ^ (degree p))"
then obtain r where r: "q ^ (degree p) = p * r" ..
- from r True have False by simp
+ from r 1 have False by simp
}
- with eq True show ?thesis by blast
+ with eq 1 show ?thesis by blast
next
- case False
- show ?thesis
- proof (cases "degree p = 0")
- case True
- with \<open>p \<noteq> 0\<close> obtain k where k: "p = [:k:]" "k \<noteq> 0"
- by (cases p) (simp split: if_splits)
- then have th1: "\<forall>x. poly p x \<noteq> 0"
+ case 2
+ then obtain k where k: "p = [:k:]" "k \<noteq> 0"
+ by (cases p) (simp split: if_splits)
+ then have th1: "\<forall>x. poly p x \<noteq> 0"
+ by simp
+ from k 2(2) have "q ^ (degree p) = p * [:1/k:]"
+ by (simp add: one_poly_def)
+ then have th2: "p dvd (q ^ (degree p))" ..
+ from 2(1) th1 th2 show ?thesis
+ by blast
+ next
+ case 3
+ {
+ assume "p dvd (q ^ (Suc n))"
+ then obtain u where u: "q ^ (Suc n) = p * u" ..
+ fix x
+ assume h: "poly p x = 0" "poly q x \<noteq> 0"
+ then have "poly (q ^ (Suc n)) x \<noteq> 0"
by simp
- from k True have "q ^ (degree p) = p * [:1/k:]"
- by (simp add: one_poly_def)
- then have th2: "p dvd (q ^ (degree p))" ..
- from False th1 th2 show ?thesis
- by blast
- next
- case False
- assume dp: "degree p \<noteq> 0"
- then obtain n where n: "degree p = Suc n "
- by (cases "degree p") auto
- {
- assume "p dvd (q ^ (Suc n))"
- then obtain u where u: "q ^ (Suc n) = p * u" ..
- {
- fix x
- assume h: "poly p x = 0" "poly q x \<noteq> 0"
- then have "poly (q ^ (Suc n)) x \<noteq> 0"
- by simp
- then have False using u h(1)
- by (simp only: poly_mult) simp
- }
- }
- with n nullstellensatz_lemma[of p q "degree p"] dp
- show ?thesis by auto
- qed
+ then have False using u h(1)
+ by (simp only: poly_mult) simp
+ }
+ with 3 nullstellensatz_lemma[of p q "degree p"]
+ show ?thesis by auto
qed
qed
@@ -1191,7 +1182,7 @@
shows "\<exists>x. poly (pCons a (pCons b p)) x = (0::complex)"
proof -
have False if "h \<noteq> 0" "t = 0" and "pCons a (pCons b p) = pCons h t" for h t
- using l prems by simp
+ using l that by simp
then have th: "\<not> (\<exists> h t. h \<noteq> 0 \<and> t = 0 \<and> pCons a (pCons b p) = pCons h t)"
by blast
from fundamental_theorem_of_algebra_alt[OF th] show ?thesis
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Sat Jun 13 19:23:41 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Sat Jun 13 22:44:22 2015 +0200
@@ -190,10 +190,10 @@
using \<open>finite simplices\<close> unfolding F_eq by auto
show "card {s \<in> simplices. face f s} = 1" if "f \<in> ?F" "bnd f" for f
- using bnd prems by auto
+ using bnd that by auto
show "card {s \<in> simplices. face f s} = 2" if "f \<in> ?F" "\<not> bnd f" for f
- using nbnd prems by auto
+ using nbnd that by auto
show "odd (card {f \<in> {f. \<exists>s\<in>simplices. face f s}. rl ` f = {..n} \<and> bnd f})"
using odd_card by simp
--- a/src/HOL/ROOT Sat Jun 13 19:23:41 2015 +0100
+++ b/src/HOL/ROOT Sat Jun 13 22:44:22 2015 +0200
@@ -623,6 +623,7 @@
Peirce
Puzzle
Summation
+ Structured_Statements
document_files
"root.bib"
"root.tex"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sat Jun 13 19:23:41 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sat Jun 13 22:44:22 2015 +0200
@@ -222,7 +222,7 @@
fun is_low_level_class_const s =
s = @{const_name equal_class.equal} orelse String.isSubstring sep_class_sep s
-val sep_that = Long_Name.separator ^ Obtain.thatN
+val sep_that = Long_Name.separator ^ Auto_Bind.thatN
val skolem_thesis = Name.skolem Auto_Bind.thesisN
fun is_that_fact th =
--- a/src/Pure/Isar/auto_bind.ML Sat Jun 13 19:23:41 2015 +0100
+++ b/src/Pure/Isar/auto_bind.ML Sat Jun 13 22:44:22 2015 +0200
@@ -8,7 +8,7 @@
sig
val thesisN: string
val thisN: string
- val premsN: string
+ val thatN: string
val assmsN: string
val abs_params: term -> term -> term
val goal: Proof.context -> term list -> (indexname * term option) list
@@ -23,8 +23,8 @@
val thesisN = "thesis";
val thisN = "this";
+val thatN = "that";
val assmsN = "assms";
-val premsN = "prems";
fun strip_judgment ctxt = Object_Logic.drop_judgment ctxt o Logic.strip_assums_concl;
--- a/src/Pure/Isar/element.ML Sat Jun 13 19:23:41 2015 +0100
+++ b/src/Pure/Isar/element.ML Sat Jun 13 22:44:22 2015 +0200
@@ -7,9 +7,12 @@
signature ELEMENT =
sig
+ type ('typ, 'term) obtain = binding * ((binding * 'typ option * mixfix) list * 'term list)
+ type obtains = (string, string) obtain list
+ type obtains_i = (typ, term) obtain list
datatype ('typ, 'term) stmt =
Shows of (Attrib.binding * ('term * 'term list) list) list |
- Obtains of (binding * ((binding * 'typ option) list * 'term list)) list
+ Obtains of ('typ, 'term) obtain list
type statement = (string, string) stmt
type statement_i = (typ, term) stmt
datatype ('typ, 'term, 'fact) ctxt =
@@ -61,9 +64,13 @@
(* statement *)
+type ('typ, 'term) obtain = binding * ((binding * 'typ option * mixfix) list * 'term list);
+type obtains = (string, string) obtain list;
+type obtains_i = (typ, term) obtain list;
+
datatype ('typ, 'term) stmt =
Shows of (Attrib.binding * ('term * 'term list) list) list |
- Obtains of (binding * ((binding * 'typ option) list * 'term list)) list;
+ Obtains of ('typ, 'term) obtain list;
type statement = (string, string) stmt;
type statement_i = (typ, term) stmt;
@@ -125,14 +132,14 @@
fun prt_show (a, ts) =
Pretty.block (Pretty.breaks (prt_binding a ":" @ prt_terms (map fst ts)));
- fun prt_var (x, SOME T) = Pretty.block
+ fun prt_var (x, SOME T, _) = Pretty.block
[Pretty.str (Binding.name_of x ^ " ::"), Pretty.brk 1, prt_typ T]
- | prt_var (x, NONE) = Pretty.str (Binding.name_of x);
+ | prt_var (x, NONE, _) = Pretty.str (Binding.name_of x);
val prt_vars = separate (Pretty.keyword2 "and") o map prt_var;
- fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (prt_terms ts))
- | prt_obtain (_, (xs, ts)) = Pretty.block (Pretty.breaks
- (prt_vars xs @ [Pretty.keyword2 "where"] @ prt_terms ts));
+ fun prt_obtain (_, ([], props)) = Pretty.block (Pretty.breaks (prt_terms props))
+ | prt_obtain (_, (vars, props)) = Pretty.block (Pretty.breaks
+ (prt_vars vars @ [Pretty.keyword2 "where"] @ prt_terms props));
in
fn Shows shows => pretty_items "shows" "and" (map prt_show shows)
| Obtains obtains => pretty_items "obtains" "|" (map prt_obtain obtains)
@@ -209,7 +216,7 @@
fun obtain prop ctxt =
let
val ((ps, prop'), ctxt') = Variable.focus prop ctxt;
- fun fix (x, T) = (Binding.name (Variable.revert_fixed ctxt' x), SOME T);
+ fun fix (x, T) = (Binding.name (Variable.revert_fixed ctxt' x), SOME T, NoSyn);
val xs = map (fix o #2) ps;
val As = Logic.strip_imp_prems prop';
in ((Binding.empty, (xs, As)), ctxt') end;
--- a/src/Pure/Isar/isar_syn.ML Sat Jun 13 19:23:41 2015 +0100
+++ b/src/Pure/Isar/isar_syn.ML Sat Jun 13 22:44:22 2015 +0200
@@ -491,7 +491,8 @@
val structured_statement =
- Parse_Spec.statement -- Parse_Spec.if_prems -- Parse.for_fixes >> (fn ((a, b), c) => (c, b, a));
+ Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes
+ >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows));
val _ =
Outer_Syntax.command @{command_keyword have} "state local goal"
@@ -570,8 +571,12 @@
>> (Toplevel.proof o Proof.def_cmd));
val _ =
+ Outer_Syntax.command @{command_keyword consider} "state cases rule"
+ (Parse_Spec.obtains >> (Toplevel.proof' o Obtain.consider_cmd));
+
+val _ =
Outer_Syntax.command @{command_keyword obtain} "generalized elimination"
- (Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement
+ (Parse.parbinding -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement
>> (fn ((x, y), z) => Toplevel.proof' (Obtain.obtain_cmd x y z)));
val _ =
--- a/src/Pure/Isar/object_logic.ML Sat Jun 13 19:23:41 2015 +0100
+++ b/src/Pure/Isar/object_logic.ML Sat Jun 13 22:44:22 2015 +0200
@@ -125,7 +125,7 @@
val aT = TFree (Name.aT, []);
val T =
the_default (aT --> propT) (Sign.const_type (Proof_Context.theory_of ctxt) c)
- |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
+ |> Term.map_type_tvar (fn ((a, _), S) => TFree (a, S));
val U = Term.domain_type T handle Match => aT;
in Const (c, T) $ Free (x, U) end;
--- a/src/Pure/Isar/obtain.ML Sat Jun 13 19:23:41 2015 +0100
+++ b/src/Pure/Isar/obtain.ML Sat Jun 13 22:44:22 2015 +0200
@@ -1,47 +1,21 @@
(* Title: Pure/Isar/obtain.ML
Author: Markus Wenzel, TU Muenchen
-The 'obtain' and 'guess' language elements -- generalized existence at
-the level of proof texts: 'obtain' involves a proof that certain
-fixes/assumes may be introduced into the present context; 'guess' is
-similar, but derives these elements from the course of reasoning!
-
- <chain_facts>
- obtain x where "A x" <proof> ==
-
- have "!!thesis. (!!x. A x ==> thesis) ==> thesis"
- proof succeed
- fix thesis
- assume that [intro?]: "!!x. A x ==> thesis"
- <chain_facts>
- show thesis
- apply (insert that)
- <proof>
- qed
- fix x assm <<obtain_export>> "A x"
-
-
- <chain_facts>
- guess x <proof body> <proof end> ==
-
- {
- fix thesis
- <chain_facts> have "PROP ?guess"
- apply magic -- {* turns goal into "thesis ==> #thesis" *}
- <proof body>
- apply_end magic -- {* turns final "(!!x. P x ==> thesis) ==> #thesis" into
- "#((!!x. A x ==> thesis) ==> thesis)" which is a finished goal state *}
- <proof end>
- }
- fix x assm <<obtain_export>> "A x"
+Generalized existence and cases rules within Isar proof text.
*)
signature OBTAIN =
sig
- val thatN: string
- val obtain: string -> (binding * typ option * mixfix) list ->
+ val obtains_attributes: ('typ, 'term) Element.obtain list -> attribute list
+ val parse_clause: Proof.context -> term ->
+ (binding * typ option * mixfix) list -> string list -> term
+ val read_obtains: Proof.context -> term -> Element.obtains -> (binding * term) list
+ val cert_obtains: Proof.context -> term -> Element.obtains_i -> (binding * term) list
+ val consider: Element.obtains_i -> bool -> Proof.state -> Proof.state
+ val consider_cmd: Element.obtains -> bool -> Proof.state -> Proof.state
+ val obtain: binding -> (binding * typ option * mixfix) list ->
(Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state
- val obtain_cmd: string -> (binding * string option * mixfix) list ->
+ val obtain_cmd: binding -> (binding * string option * mixfix) list ->
(Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
((string * cterm) list * thm list) * Proof.context
@@ -52,7 +26,9 @@
structure Obtain: OBTAIN =
struct
-(** obtain_export **)
+(** specification elements **)
+
+(* obtain_export *)
(*
[x, A x]
@@ -92,33 +68,136 @@
(eliminate ctxt rule xs As, eliminate_term ctxt xs);
+(* result declaration *)
-(** obtain **)
+fun obtains_attributes (obtains: ('typ, 'term) Element.obtain list) =
+ let
+ val case_names = obtains |> map_index (fn (i, (b, _)) =>
+ if Binding.is_empty b then string_of_int (i + 1) else Name_Space.base_name b);
+ in [Rule_Cases.consumes (~ (length obtains)), Rule_Cases.case_names case_names] end;
+
-fun bind_judgment ctxt name =
+(* obtain thesis *)
+
+fun obtain_thesis ctxt =
let
- val ([x], ctxt') = Proof_Context.add_fixes [(Binding.name name, NONE, NoSyn)] ctxt;
- val (t as _ $ Free v) = Object_Logic.fixed_judgment ctxt x;
+ val ([x], ctxt') =
+ Proof_Context.add_fixes [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)] ctxt;
+ val t = Object_Logic.fixed_judgment ctxt x;
+ val v = dest_Free (Object_Logic.drop_judgment ctxt t);
in ((v, t), ctxt') end;
-val thatN = "that";
+
+(* obtain clauses *)
+
+local
+
+fun prepare_clause parse_prop ctxt thesis vars raw_props =
+ let
+ val (xs', ctxt') = ctxt |> Proof_Context.add_fixes vars;
+ val xs = map (Variable.check_name o #1) vars;
+ in
+ Logic.list_implies (map (parse_prop ctxt') raw_props, thesis)
+ |> fold_rev (Logic.all_constraint (Variable.default_type ctxt')) (xs ~~ xs')
+ end;
+
+fun prepare_obtains prep_var parse_prop ctxt thesis raw_obtains =
+ let
+ val all_types =
+ fold_map prep_var (maps (fn (_, (vs, _)) => vs) raw_obtains)
+ (ctxt |> Context_Position.set_visible false)
+ |> #1 |> map_filter (fn (_, opt_T, _) => opt_T);
+ val types_ctxt = fold Variable.declare_typ all_types ctxt;
+
+ val clauses =
+ raw_obtains |> map (fn (_, (raw_vars, raw_props)) =>
+ let
+ val (vars, vars_ctxt) = fold_map prep_var raw_vars types_ctxt;
+ val clause = prepare_clause parse_prop vars_ctxt thesis vars raw_props;
+ in clause end)
+ |> Syntax.check_terms ctxt;
+ in map fst raw_obtains ~~ clauses end;
+
+in
+
+val parse_clause = prepare_clause Syntax.parse_prop;
+
+val read_obtains = prepare_obtains Proof_Context.read_var Syntax.parse_prop;
+val cert_obtains = prepare_obtains Proof_Context.cert_var (K I);
+
+end;
+
+
+
+(** consider: generalized elimination and cases rule **)
+
+(*
+ consider x where (a) "A x" | y (b) where "B x" | ... ==
+
+ have thesis
+ if a [intro?]: "!!x. A x ==> thesis"
+ and b [intro?]: "!!x. B x ==> thesis"
+ and ...
+ for thesis
+ apply (insert that)
+*)
+
+local
+
+fun gen_consider prep_obtains raw_obtains int state =
+ let
+ val _ = Proof.assert_forward_or_chain state;
+ val ctxt = Proof.context_of state;
+
+ val ((_, thesis), thesis_ctxt) = obtain_thesis ctxt;
+ val obtains = prep_obtains thesis_ctxt thesis raw_obtains;
+ val atts = Rule_Cases.cases_open :: obtains_attributes raw_obtains;
+ in
+ state
+ |> Proof.have NONE (K I)
+ [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
+ (map (fn (a, A) => ((a, [Context_Rules.intro_query NONE]), [(A, [])])) obtains)
+ [((Binding.empty, atts), [(thesis, [])])] int
+ |> (fn state' => state'
+ |> Proof.refine_insert (Assumption.local_prems_of (Proof.context_of state') ctxt))
+ end;
+
+in
+
+val consider = gen_consider cert_obtains;
+val consider_cmd = gen_consider read_obtains;
+
+end;
+
+
+
+(** obtain: augmented context based on generalized existence rule **)
+
+(*
+ obtain (a) x where "A x" <proof> ==
+
+ have thesis if a [intro?]: "!!x. A x ==> thesis" for thesis
+ apply (insert that)
+ <proof>
+ fix x assm <<obtain_export>> "A x"
+*)
local
fun gen_obtain prep_att prep_var prep_propp
- name raw_vars raw_asms int state =
+ that_binding raw_vars raw_asms int state =
let
val _ = Proof.assert_forward_or_chain state;
val ctxt = Proof.context_of state;
- val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
- (*obtain vars*)
- val ((xs', vars), fix_ctxt) = ctxt
+ (*vars*)
+ val ((_, thesis), thesis_ctxt) = obtain_thesis ctxt;
+ val ((xs', vars), fix_ctxt) = thesis_ctxt
|> fold_map prep_var raw_vars
|-> (fn vars => Proof_Context.add_fixes vars ##>> pair vars);
val xs = map (Variable.check_name o #1) vars;
- (*obtain asms*)
+ (*asms*)
val (propss, binds) = prep_propp fix_ctxt (map snd raw_asms);
val props = flat propss;
val declare_asms =
@@ -128,7 +207,7 @@
map (fn ((b, raw_atts), _) => (b, map (prep_att fix_ctxt) raw_atts)) raw_asms ~~
map (map (rpair [])) propss;
- (*obtain params*)
+ (*params*)
val (params, params_ctxt) =
declare_asms fix_ctxt |> fold_map Proof_Context.inferred_param xs' |>> map Free;
val cparams = map (Thm.cterm_of params_ctxt) params;
@@ -136,37 +215,27 @@
val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt;
- (*obtain statements*)
- val thesisN = singleton (Name.variant_list xs) Auto_Bind.thesisN;
- val (thesis_var, thesis) = #1 (bind_judgment params_ctxt thesisN);
-
- val that_name = if name = "" then thatN else name;
+ (*statements*)
val that_prop =
Logic.list_rename_params xs
(fold_rev Logic.all params (Logic.list_implies (props, thesis)));
- val obtain_prop =
- Logic.list_rename_params [Auto_Bind.thesisN]
- (Logic.all (Free thesis_var) (Logic.mk_implies (that_prop, thesis)));
- fun after_qed _ =
- Proof.local_qed (NONE, false)
- #> `Proof.the_fact #-> (fn rule =>
- Proof.fix vars
- #> Proof.map_context declare_asms
- #> Proof.assm (obtain_export params_ctxt rule cparams) asms);
+ fun after_qed (result_ctxt, results) state' =
+ let val [rule] = Proof_Context.export result_ctxt (Proof.context_of state') (flat results) in
+ state'
+ |> Proof.fix vars
+ |> Proof.map_context declare_asms
+ |> Proof.assm (obtain_export params_ctxt rule cparams) asms
+ end;
in
state
- |> Proof.enter_forward
- |> Proof.have NONE (K I) [] [] [(Thm.empty_binding, [(obtain_prop, [])])] int
+ |> Proof.have NONE after_qed
+ [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
+ [((that_binding, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
+ [(Thm.empty_binding, [(thesis, [])])] int
+ |> (fn state' => state'
+ |> Proof.refine_insert (Assumption.local_prems_of (Proof.context_of state') ctxt))
|> Proof.map_context (fold Variable.bind_term binds')
- |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
- |> Proof.fix [(Binding.name thesisN, NONE, NoSyn)]
- |> Proof.assume
- [((Binding.name that_name, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
- |> `Proof.the_facts
- ||> Proof.chain_facts chain_facts
- ||> Proof.show NONE after_qed [] [] [(Thm.empty_binding, [(thesis, [])])] false
- |-> Proof.refine_insert
end;
in
@@ -191,7 +260,7 @@
fun result tac facts ctxt =
let
- val ((thesis_var, thesis), thesis_ctxt) = bind_judgment ctxt Auto_Bind.thesisN;
+ val ((thesis_var, thesis), thesis_ctxt) = obtain_thesis ctxt;
val st = Goal.init (Thm.cterm_of ctxt thesis);
val rule =
(case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) st of
@@ -211,7 +280,23 @@
-(** guess **)
+(** guess: obtain based on tactical result **)
+
+(*
+ <chain_facts>
+ guess x <proof body> <proof end> ==
+
+ {
+ fix thesis
+ <chain_facts> have "PROP ?guess"
+ apply magic -- {* turns goal into "thesis ==> #thesis" *}
+ <proof body>
+ apply_end magic -- {* turns final "(!!x. P x ==> thesis) ==> #thesis" into
+ "#((!!x. A x ==> thesis) ==> thesis)" which is a finished goal state *}
+ <proof end>
+ }
+ fix x assm <<obtain_export>> "A x"
+*)
local
@@ -274,7 +359,7 @@
val ctxt = Proof.context_of state;
val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
- val (thesis_var, thesis) = #1 (bind_judgment ctxt Auto_Bind.thesisN);
+ val (thesis_var, thesis) = #1 (obtain_thesis ctxt);
val vars = ctxt
|> fold_map prep_var raw_vars |-> fold_map inferred_type
|> fst |> polymorphic ctxt;
--- a/src/Pure/Isar/parse.ML Sat Jun 13 19:23:41 2015 +0100
+++ b/src/Pure/Isar/parse.ML Sat Jun 13 22:44:22 2015 +0200
@@ -90,7 +90,7 @@
val where_: string parser
val const_decl: (string * string * mixfix) parser
val const_binding: (binding * string * mixfix) parser
- val params: (binding * string option) list parser
+ val params: (binding * string option * mixfix) list parser
val fixes: (binding * string option * mixfix) list parser
val for_fixes: (binding * string option * mixfix) list parser
val ML_source: Input.source parser
@@ -358,13 +358,12 @@
val const_decl = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
val const_binding = binding -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
-val params = Scan.repeat1 binding -- Scan.option ($$$ "::" |-- !!! typ)
- >> (fn (xs, T) => map (rpair T) xs);
+val param_mixfix = binding -- Scan.option ($$$ "::" |-- typ) -- mixfix' >> (single o triple1);
+val params =
+ Scan.repeat1 binding -- Scan.option ($$$ "::" |-- !!! typ)
+ >> (fn (xs, T) => map (fn x => (x, T, NoSyn)) xs);
-val fixes =
- and_list1 (binding -- Scan.option ($$$ "::" |-- typ) -- mixfix' >> (single o triple1) ||
- params >> map (fn (x, y) => (x, y, NoSyn))) >> flat;
-
+val fixes = and_list1 (param_mixfix || params) >> flat;
val for_fixes = Scan.optional ($$$ "for" |-- !!! fixes) [];
--- a/src/Pure/Isar/parse_spec.ML Sat Jun 13 19:23:41 2015 +0100
+++ b/src/Pure/Isar/parse_spec.ML Sat Jun 13 22:44:22 2015 +0200
@@ -24,7 +24,8 @@
val locale_expression: bool -> Expression.expression parser
val context_element: Element.context parser
val statement: (Attrib.binding * (string * string list) list) list parser
- val if_prems: (Attrib.binding * (string * string list) list) list parser
+ val if_statement: (Attrib.binding * (string * string list) list) list parser
+ val obtains: Element.obtains parser
val general_statement: (Element.context list * Element.statement) parser
val statement_keyword: string parser
end;
@@ -72,7 +73,7 @@
val locale_fixes =
Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- Parse.mixfix
>> (single o Parse.triple1) ||
- Parse.params >> map (fn (x, y) => (x, y, NoSyn))) >> flat;
+ Parse.params) >> flat;
val locale_insts =
Scan.optional
@@ -131,18 +132,19 @@
(* statements *)
val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
-
-val if_prems = Scan.optional (Parse.$$$ "if" |-- Parse.!!! statement) [];
+val if_statement = Scan.optional (Parse.$$$ "if" |-- Parse.!!! statement) [];
val obtain_case =
Parse.parbinding --
- (Scan.optional (Parse.and_list1 Parse.params --| Parse.where_ >> flat) [] --
+ (Scan.optional (Parse.and_list1 Parse.fixes --| Parse.where_ >> flat) [] --
(Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat));
+val obtains = Parse.enum1 "|" obtain_case;
+
val general_statement =
statement >> (fn x => ([], Element.Shows x)) ||
Scan.repeat context_element --
- (Parse.$$$ "obtains" |-- Parse.!!! (Parse.enum1 "|" obtain_case) >> Element.Obtains ||
+ (Parse.$$$ "obtains" |-- Parse.!!! obtains >> Element.Obtains ||
Parse.$$$ "shows" |-- Parse.!!! statement >> Element.Shows);
val statement_keyword = Parse.$$$ "obtains" || Parse.$$$ "shows";
--- a/src/Pure/Isar/proof.ML Sat Jun 13 19:23:41 2015 +0100
+++ b/src/Pure/Isar/proof.ML Sat Jun 13 22:44:22 2015 +0200
@@ -373,7 +373,7 @@
val {context = ctxt, facts, mode, goal = _} = top state;
val verbose = Config.get ctxt Proof_Context.verbose;
- fun prt_goal (SOME (_, (_, {using, goal, ...}))) =
+ fun prt_goal (SOME (_, (_, {statement = _, using, goal, before_qed = _, after_qed = _}))) =
pretty_sep
(pretty_facts ctxt "using"
(if mode <> Backward orelse null using then NONE else SOME using))
@@ -1012,7 +1012,7 @@
|> (fn (premss, ctxt') => ctxt'
|> not (null assumes_propss) ?
(snd o Proof_Context.note_thmss ""
- [((Binding.name Auto_Bind.premsN, []),
+ [((Binding.name Auto_Bind.thatN, []),
[(Assumption.local_prems_of ctxt' ctxt, [])])])
|> (snd o Proof_Context.note_thmss ""
(assumes_bindings ~~ map (map (fn th => ([th], []))) premss)));
--- a/src/Pure/Isar/rule_cases.ML Sat Jun 13 19:23:41 2015 +0100
+++ b/src/Pure/Isar/rule_cases.ML Sat Jun 13 22:44:22 2015 +0200
@@ -47,11 +47,13 @@
val case_conclusion: string * string list -> attribute
val is_inner_rule: thm -> bool
val inner_rule: attribute
+ val is_cases_open: thm -> bool
+ val cases_open: attribute
+ val internalize_params: thm -> thm
val save: thm -> thm -> thm
val get: thm -> ((string * string list) * string list) list * int
val rename_params: string list list -> thm -> thm
val params: string list list -> attribute
- val internalize_params: thm -> thm
val mutual_rule: Proof.context -> thm list -> (int list * thm) option
val strict_mutual_rule: Proof.context -> thm list -> int list * thm
end;
@@ -201,7 +203,9 @@
-(** consume facts **)
+(** annotations and operations on rules **)
+
+(* consume facts *)
local
@@ -256,8 +260,7 @@
fun consumes n = Thm.mixed_attribute (apsnd (put_consumes (SOME n)));
-
-(** equality constraints **)
+(* equality constraints *)
val constraints_tagN = "constraints";
@@ -281,8 +284,7 @@
fun constraints n = Thm.mixed_attribute (apsnd (put_constraints (SOME n)));
-
-(** case names **)
+(* case names *)
val implode_args = space_implode ";";
val explode_args = space_explode ";";
@@ -303,8 +305,7 @@
fun case_names cs = Thm.mixed_attribute (apsnd (name cs));
-
-(** hyp names **)
+(* hyp names *)
val implode_hyps = implode_args o map (suffix "," o space_implode ",");
val explode_hyps = map (space_explode "," o unsuffix ",") o explode_args;
@@ -325,8 +326,7 @@
Thm.mixed_attribute (apsnd (name cs #> add_cases_hyp_names (SOME hs)));
-
-(** case conclusions **)
+(* case conclusions *)
val case_concl_tagN = "case_conclusion";
@@ -355,8 +355,7 @@
fun case_conclusion concl = Thm.mixed_attribute (apsnd (add_case_concl concl));
-
-(** inner rule **)
+(* inner rule *)
val inner_rule_tagN = "inner_rule";
@@ -372,6 +371,35 @@
val inner_rule = Thm.mixed_attribute (apsnd (put_inner_rule true));
+(* parameter names *)
+
+val cases_open_tagN = "cases_open";
+
+fun is_cases_open th =
+ AList.defined (op =) (Thm.get_tags th) cases_open_tagN;
+
+fun put_cases_open cases_open =
+ Thm.untag_rule cases_open_tagN
+ #> cases_open ? Thm.tag_rule (cases_open_tagN, "");
+
+val save_cases_open = put_cases_open o is_cases_open;
+
+val cases_open = Thm.mixed_attribute (apsnd (put_cases_open true));
+
+fun internalize_params rule =
+ if is_cases_open rule then rule
+ else
+ let
+ fun rename prem =
+ let val xs =
+ map (Name.internal o Name.clean o fst) (Logic.strip_params prem)
+ in Logic.list_rename_params xs prem end;
+ fun rename_prems prop =
+ let val (As, C) = Logic.strip_horn prop
+ in Logic.list_implies (map rename As, C) end;
+ in Thm.renamed_prop (rename_prems (Thm.prop_of rule)) rule end;
+
+
(** case declarations **)
@@ -383,7 +411,8 @@
save_case_names th #>
save_cases_hyp_names th #>
save_case_concls th #>
- save_inner_rule th;
+ save_inner_rule th #>
+ save_cases_open th;
fun get th =
let
@@ -410,20 +439,6 @@
fun params xss = Thm.rule_attribute (K (rename_params xss));
-(* internalize parameter names *)
-
-fun internalize_params rule =
- let
- fun rename prem =
- let val xs =
- map (Name.internal o Name.clean o fst) (Logic.strip_params prem)
- in Logic.list_rename_params xs prem end;
- fun rename_prems prop =
- let val (As, C) = Logic.strip_horn prop
- in Logic.list_implies (map rename As, C) end;
- in Thm.renamed_prop (rename_prems (Thm.prop_of rule)) rule end;
-
-
(** mutual_rule **)
--- a/src/Pure/Isar/specification.ML Sat Jun 13 19:23:41 2015 +0100
+++ b/src/Pure/Isar/specification.ML Sat Jun 13 22:44:22 2015 +0200
@@ -103,32 +103,14 @@
local
-fun close_forms ctxt i xs As =
+fun close_forms ctxt i As =
let
- val commons = map #1 xs;
- val _ =
- (case duplicates (op =) commons of [] => ()
- | dups => error ("Duplicate local variables " ^ commas_quote dups));
- val frees = rev (fold (Variable.add_free_names ctxt) As (rev commons));
+ val xs = rev (fold (Variable.add_free_names ctxt) As []);
val types =
- map (Type_Infer.param i o rpair []) (Name.invent Name.context Name.aT (length frees));
- val uniform_typing = the o AList.lookup (op =) (frees ~~ types);
-
- fun abs_body lev y (Abs (x, T, b)) = Abs (x, T, abs_body (lev + 1) y b)
- | abs_body lev y (t $ u) = abs_body lev y t $ abs_body lev y u
- | abs_body lev y (t as Free (x, T)) =
- if x = y then Type.constraint (uniform_typing x) (Type.constraint T (Bound lev))
- else t
- | abs_body _ _ a = a;
- fun close (y, U) B =
- let val B' = abs_body 0 y (Term.incr_boundvars 1 B)
- in if Term.is_dependent B' then Logic.all_const dummyT $ Abs (y, U, B') else B end;
- fun close_form A =
- let
- val occ_frees = rev (Variable.add_free_names ctxt A []);
- val bounds = xs @ map (rpair dummyT) (subtract (op =) commons occ_frees);
- in fold_rev close bounds A end;
- in map close_form As end;
+ map (Type_Infer.param i o rpair []) (Name.invent Name.context Name.aT (length xs));
+ val uniform_typing = AList.lookup (op =) (xs ~~ types);
+ val close = fold_rev (Logic.dependent_all_constraint uniform_typing) (xs ~~ xs);
+ in map close As end;
fun prepare prep_var parse_prop prep_att do_close raw_vars raw_specss ctxt =
let
@@ -145,7 +127,7 @@
val specs =
(if do_close then
#1 (fold_map
- (fn Ass => fn i => (burrow (close_forms params_ctxt i []) Ass, i + 1)) Asss' idx)
+ (fn Ass => fn i => (burrow (close_forms params_ctxt i) Ass, i + 1)) Asss' idx)
else Asss')
|> flat |> burrow (Syntax.check_props params_ctxt);
val specs_ctxt = params_ctxt |> (fold o fold) Variable.declare_term specs;
@@ -347,11 +329,9 @@
in (([], prems, stmt, NONE), goal_ctxt) end
| Element.Obtains obtains =>
let
- val case_names = obtains |> map_index (fn (i, (b, _)) =>
- if Binding.is_empty b then string_of_int (i + 1) else Name_Space.base_name b);
val constraints = obtains |> map (fn (_, (vars, _)) =>
Element.Constrains
- (vars |> map_filter (fn (x, SOME T) => SOME (Variable.check_name x, T) | _ => NONE)));
+ (vars |> map_filter (fn (x, SOME T, _) => SOME (Variable.check_name x, T) | _ => NONE)));
val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
@@ -360,7 +340,7 @@
fun assume_case ((name, (vars, _)), asms) ctxt' =
let
- val bs = map fst vars;
+ val bs = map (fn (b, _, _) => b) vars;
val xs = map Variable.check_name bs;
val props = map fst asms;
val (params, _) = ctxt'
@@ -377,8 +357,7 @@
|>> (fn [(_, [th])] => th)
end;
- val more_atts = map (Attrib.internal o K)
- [Rule_Cases.consumes (~ (length obtains)), Rule_Cases.case_names case_names];
+ val more_atts = map (Attrib.internal o K) (Obtain.obtains_attributes obtains);
val prems = Assumption.local_prems_of elems_ctxt ctxt;
val stmt = [((Binding.empty, []), [(thesis, [])])];
@@ -386,7 +365,7 @@
|> (snd o Proof_Context.add_fixes [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)])
|> fold_map assume_case (obtains ~~ propp)
|-> (fn ths =>
- Proof_Context.note_thmss "" [((Binding.name Obtain.thatN, []), [(ths, [])])] #>
+ Proof_Context.note_thmss "" [((Binding.name Auto_Bind.thatN, []), [(ths, [])])] #>
#2 #> pair ths);
in ((more_atts, prems, stmt, SOME facts), goal_ctxt) end);
--- a/src/Pure/Pure.thy Sat Jun 13 19:23:41 2015 +0100
+++ b/src/Pure/Pure.thy Sat Jun 13 22:44:22 2015 +0200
@@ -55,6 +55,7 @@
and "supply" :: prf_script % "proof"
and "using" "unfolding" :: prf_decl % "proof"
and "fix" "assume" "presume" "def" :: prf_asm % "proof"
+ and "consider" :: prf_goal % "proof"
and "obtain" :: prf_asm_goal % "proof"
and "guess" :: prf_asm_goal_script % "proof"
and "let" "write" :: prf_decl % "proof"
--- a/src/Pure/logic.ML Sat Jun 13 19:23:41 2015 +0100
+++ b/src/Pure/logic.ML Sat Jun 13 22:44:22 2015 +0200
@@ -12,6 +12,8 @@
val is_all: term -> bool
val dest_all: term -> (string * typ) * term
val list_all: (string * typ) list * term -> term
+ val all_constraint: (string -> typ option) -> string * string -> term -> term
+ val dependent_all_constraint: (string -> typ option) -> string * string -> term -> term
val mk_equals: term * term -> term
val dest_equals: term -> term * term
val implies: term
@@ -109,6 +111,35 @@
| list_all ((a, T) :: vars, t) = all_const T $ Abs (a, T, list_all (vars, t));
+(* operations before type-inference *)
+
+local
+
+fun abs_body default_type z tm =
+ let
+ fun abs lev (Abs (x, T, b)) = Abs (x, T, abs (lev + 1) b)
+ | abs lev (t $ u) = abs lev t $ abs lev u
+ | abs lev (a as Free (x, T)) =
+ if x = z then
+ Type.constraint (the_default dummyT (default_type x))
+ (Type.constraint T (Bound lev))
+ else a
+ | abs _ a = a;
+ in abs 0 (Term.incr_boundvars 1 tm) end;
+
+in
+
+fun all_constraint default_type (y, z) t =
+ all_const dummyT $ Abs (y, dummyT, abs_body default_type z t);
+
+fun dependent_all_constraint default_type (y, z) t =
+ let val t' = abs_body default_type z t
+ in if Term.is_dependent t' then all_const dummyT $ Abs (y, dummyT, t') else t end;
+
+end;
+
+
+
(** equality **)
fun mk_equals (t, u) =
--- a/src/Tools/induct.ML Sat Jun 13 19:23:41 2015 +0100
+++ b/src/Tools/induct.ML Sat Jun 13 22:44:22 2015 +0200
@@ -483,25 +483,32 @@
|> simp ? mark_constraints (Rule_Cases.get_constraints r) ctxt
|> pair (Rule_Cases.get r);
+ val (opt_rule', facts') =
+ (case (opt_rule, facts) of
+ (NONE, th :: ths) =>
+ if is_some (Object_Logic.elim_concl ctxt th) then (SOME th, ths)
+ else (opt_rule, facts)
+ | _ => (opt_rule, facts));
+
val ruleq =
- (case opt_rule of
+ (case opt_rule' of
SOME r => Seq.single (inst_rule r)
| NONE =>
- (get_casesP ctxt facts @ get_casesT ctxt insts @ [Induct_Args.cases_default])
+ (get_casesP ctxt facts' @ get_casesT ctxt insts @ [Induct_Args.cases_default])
|> tap (trace_rules ctxt casesN)
|> Seq.of_list |> Seq.maps (Seq.try inst_rule));
in
fn i => fn st =>
ruleq
- |> Seq.maps (Rule_Cases.consume ctxt [] facts)
- |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
+ |> Seq.maps (Rule_Cases.consume ctxt [] facts')
+ |> Seq.maps (fn ((cases, (_, facts'')), rule) =>
let
val rule' = rule
|> simp ? (simplified_rule' ctxt #> unmark_constraints ctxt);
in
CASES (Rule_Cases.make_common ctxt
(Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
- ((Method.insert_tac more_facts THEN' resolve_tac ctxt [rule'] THEN_ALL_NEW
+ ((Method.insert_tac facts'' THEN' resolve_tac ctxt [rule'] THEN_ALL_NEW
(if simp then TRY o trivial_tac ctxt else K all_tac)) i) st
end)
end;