# HG changeset patch # User wenzelm # Date 1434228262 -7200 # Node ID abee0de69a894b18597770826492195f71f42ecc # Parent 310853646597beaad3d552edc6d65377c9c3daf1# Parent 2761a2249c83b7ba54e66356dafddf311715410f merged diff -r 310853646597 -r abee0de69a89 NEWS --- 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 -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" } 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 + then have something + proof cases + case a + then show ?thesis + next + case b + then show ?thesis + next + case c + then show ?thesis + qed + *** Pure *** diff -r 310853646597 -r abee0de69a89 src/Doc/Isar_Ref/Proof.thy --- 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} *) \ 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') \} \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. \ @@ -853,15 +853,6 @@ subsection \Emulating tactic scripts \label{sec:tactic-commands}\ text \ - 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) \ proof(prove)"} \\ @{command_def "apply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \ proof(prove)"} \\ @@ -872,6 +863,15 @@ @{command_def "back"}@{text "\<^sup>*"} & : & @{text "proof \ 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 \ @@{command supply} (@{syntax thmdef}? @{syntax thmrefs} + @'and') ; @@ -979,83 +979,125 @@ (*<*)end(*>*) -section \Generalized elimination \label{sec:obtain}\ +section \Generalized elimination and case splitting \label{sec:obtain}\ text \ \begin{matharray}{rcl} + @{command_def "consider"} & : & @{text "proof(state) | proof(chain) \ proof(prove)"} \\ @{command_def "obtain"} & : & @{text "proof(state) | proof(chain) \ proof(prove)"} \\ @{command_def "guess"}@{text "\<^sup>*"} & : & @{text "proof(state) | proof(chain) \ 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 "\x. B x \ (\x. B x \ thesis) \ thesis"} \\ + @{text "A \ B \ (A \ B \ thesis) \ thesis"} \\ + @{text "A \ B \ (A \ thesis) \ (B \ thesis) \ 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 \ - @@{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') \} - The derived Isar command @{command "obtain"} is defined as follows - (where @{text "b\<^sub>1, \, b\<^sub>k"} shall refer to (optional) - facts indicated for forward chaining). + \begin{description} + + \item @{command consider}~@{text "(a) \<^vec>x \ \<^vec>A \<^vec>x + | (b) \<^vec>y \ \<^vec>B \<^vec>y | \ "} 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 "\using b\<^sub>1 \ b\<^sub>k\"}~~@{command "obtain"}~@{text "x\<^sub>1 \ x\<^sub>m \ a: \\<^sub>1 \ \\<^sub>n \proof\ \"} \\[1ex] - \quad @{command "have"}~@{text "\thesis. (\x\<^sub>1 \ x\<^sub>m. \\<^sub>1 \ \ \\<^sub>n \ thesis) \ thesis"} \\ - \quad @{command "proof"}~@{method succeed} \\ - \qquad @{command "fix"}~@{text thesis} \\ - \qquad @{command "assume"}~@{text "that [Pure.intro?]: \x\<^sub>1 \ x\<^sub>m. \\<^sub>1 \ \ \\<^sub>n \ thesis"} \\ - \qquad @{command "then"}~@{command "show"}~@{text thesis} \\ - \quad\qquad @{command "apply"}~@{text -} \\ - \quad\qquad @{command "using"}~@{text "b\<^sub>1 \ b\<^sub>k \proof\"} \\ - \quad @{command "qed"} \\ - \quad @{command "fix"}~@{text "x\<^sub>1 \ x\<^sub>m"}~@{command "assume"}@{text "\<^sup>* a: \\<^sub>1 \ \\<^sub>n"} \\ + @{command "consider"}~@{text "(a) \<^vec>x \ \<^vec>A \<^vec>x | (b) \<^vec>y \ \<^vec>B \<^vec>y | \ \"} \\[1ex] + \quad @{command "have"}~@{text "[case_names a b \]: thesis"} \\ + \qquad @{text "\ a [Pure.intro?]: \\<^vec>x. \<^vec>A \<^vec>x \ thesis"} \\ + \qquad @{text "\ b [Pure.intro?]: \\<^vec>y. \<^vec>B \<^vec>y \ thesis"} \\ + \qquad @{text "\ \"} \\ + \qquad @{text "\ thesis"} \\ + \qquad @{command "apply"}~@{text "(insert a b \)"} \\ \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 \ \<^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 \ a: \<^vec>A \<^vec>x \proof\ \"} \\[1ex] + \quad @{command "have"}~@{text "thesis"} \\ + \qquad @{text "\ that [Pure.intro?]: \\<^vec>x. \<^vec>A \<^vec>x \ thesis"} \\ + \qquad @{text "\ thesis"} \\ + \qquad @{command "apply"}~@{text "(insert that)"} \\ + \qquad @{text "\proof\"} \\ + \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 "\x\<^sub>1 \ x\<^sub>m. \\<^sub>1 \ \ - \\<^sub>n \ 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, \, - 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 + "\\<^vec>x. \<^vec>A \<^vec>x \ 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. \ @@ -1372,6 +1414,7 @@ \medskip \begin{tabular}{llll} facts & & arguments & rule \\\hline + @{text "\ R"} & @{method cases} & & implicit rule @{text R} \\ & @{method cases} & & classical case split \\ & @{method cases} & @{text t} & datatype exhaustion (type of @{text t}) \\ @{text "\ A t"} & @{method cases} & @{text "\"} & inductive predicate/set elimination (of @{text A}) \\ diff -r 310853646597 -r abee0de69a89 src/Doc/isar.sty --- 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}} diff -r 310853646597 -r abee0de69a89 src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy --- 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 \ F" then have "a y \ ?S" by blast with xi have "a y \ xi" by (rule lub.upper) - } moreover { + } + moreover { fix y assume y: "y \ F" from xi have "xi \ b y" proof (rule lub.least) @@ -78,7 +79,8 @@ from u y have "a u \ b y" by (rule r) with au show "au \ b y" by (simp only:) qed - } ultimately show "\xi. \y \ F. a y \ xi \ xi \ b y" by blast + } + ultimately show "\xi. \y \ F. a y \ xi \ xi \ b y" by blast qed text \ diff -r 310853646597 -r abee0de69a89 src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy --- 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}\ - from cM c'' c' have "graph H'' h'' \ graph H' h' \ graph H' h' \ graph H'' h''" - (is "?case1 \ ?case2") .. + from cM c'' c' consider "graph H'' h'' \ graph H' h'" | "graph H' h' \ graph H'' h''" + by (blast dest: chainsD) then show ?thesis - proof - assume ?case1 + proof cases + case 1 have "(x, h x) \ graph H'' h''" by fact also have "\ \ graph H' h'" by fact finally have xh:"(x, h x) \ graph H' h'" . @@ -139,14 +139,16 @@ moreover from cM u and c' have "graph H' h' \ graph H h" by blast ultimately show ?thesis using * by blast next - assume ?case2 + case 2 from x_hx have "x \ H''" .. - moreover { + moreover have "y \ H''" + proof - have "(y, h y) \ graph H' h'" by (rule y_hy) also have "\ \ graph H'' h''" by fact finally have "(y, h y) \ graph H'' h''" . - } then have "y \ H''" .. - moreover from cM u and c'' have "graph H'' h'' \ graph H h" by blast + then show ?thesis .. + qed + moreover from u c'' have "graph H'' h'' \ 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}\ - from cM G1 G2 have "G1 \ G2 \ G2 \ G1" (is "?case1 \ ?case2") .. + from cM G1 G2 consider "G1 \ G2" | "G2 \ G1" + by (blast dest: chainsD) then show ?thesis - proof - assume ?case1 + proof cases + case 1 with xy' G2_rep have "(x, y) \ 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) \ graph H1 h1" by blast then have "z = h1 x" .. also diff -r 310853646597 -r abee0de69a89 src/HOL/Isar_Examples/Hoare_Ex.thy --- 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 \ i \ n" for s i - using prems by simp + using that by simp show "s = ?sum n" if "?inv s i \ \ i \ n" for s i - using prems by simp + using that by simp qed qed diff -r 310853646597 -r abee0de69a89 src/HOL/Isar_Examples/Nested_Datatype.thy --- 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 diff -r 310853646597 -r abee0de69a89 src/HOL/Isar_Examples/Structured_Statements.thy --- /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 \Structured statements within Isar proofs\ + +theory Structured_Statements +imports Main +begin + +notepad +begin + + fix A B :: bool + + have iff_comm: "(A \ B) \ (B \ A)" + proof + show "B \ A" if "A \ B" + proof + show B using that .. + show A using that .. + qed + show "A \ B" if "B \ A" + proof + show A using that .. + show B using that .. + qed + qed + + text \Alternative proof, avoiding redundant copy of symmetric argument.\ + have iff_comm: "(A \ B) \ (B \ A)" + proof + show "B \ A" if "A \ B" for A B + proof + show B using that .. + show A using that .. + qed + then show "A \ B" if "B \ A" + by this (rule that) + qed + +end + +end \ No newline at end of file diff -r 310853646597 -r abee0de69a89 src/HOL/Library/Convex.thy --- 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 = "\j. a j / (1 - a i)" have a_nonneg: "?a j \ 0" if "j \ s" for j - using i0 insert prems by fastforce + using i0 insert that by fastforce have "(\ j \ insert i s. a j) = 1" using insert by auto then have "(\ j \ s. a j) = 1 - a i" diff -r 310853646597 -r abee0de69a89 src/HOL/Library/Fundamental_Theorem_Algebra.thy --- 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: "\m 0 \ (\z. cmod (1 + b * z ^ m) < 1)" assume n: "n \ 0" let ?P = "\z n. cmod (1 + b * z ^ n) < 1" - { - assume e: "even n" + show "\z. ?P z n" + proof cases + assume "even n" then have "\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 "\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 "\m. n = Suc (2 * m)" + by (simp add: m power_mult) + then show ?thesis .. + next + assume "odd n" + then have "\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] \odd n\ have "\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 \odd n\, 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 "\z. ?P z n" .. - } - ultimately show "\z. ?P z n" by blast + then show ?thesis .. + qed qed text \Bolzano-Weierstrass type property for closed disc in complex plane.\ @@ -1020,51 +1018,44 @@ "(\x. poly p x = (0::complex) \ poly q x = 0) \ p dvd (q ^ (degree p)) \ (p = 0 \ q = 0)" proof - - show ?thesis - proof (cases "p = 0") - case True + consider "p = 0" | "p \ 0" "degree p = 0" | n where "p \ 0" "degree p = Suc n" + by (cases "degree p") auto + then show ?thesis + proof cases + case 1 then have eq: "(\x. poly p x = (0::complex) \ poly q x = 0) \ 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 \p \ 0\ obtain k where k: "p = [:k:]" "k \ 0" - by (cases p) (simp split: if_splits) - then have th1: "\x. poly p x \ 0" + case 2 + then obtain k where k: "p = [:k:]" "k \ 0" + by (cases p) (simp split: if_splits) + then have th1: "\x. poly p x \ 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 \ 0" + then have "poly (q ^ (Suc n)) x \ 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 \ 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 \ 0" - then have "poly (q ^ (Suc n)) x \ 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 "\x. poly (pCons a (pCons b p)) x = (0::complex)" proof - have False if "h \ 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: "\ (\ h t. h \ 0 \ t = 0 \ pCons a (pCons b p) = pCons h t)" by blast from fundamental_theorem_of_algebra_alt[OF th] show ?thesis diff -r 310853646597 -r abee0de69a89 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy --- 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 \finite simplices\ unfolding F_eq by auto show "card {s \ simplices. face f s} = 1" if "f \ ?F" "bnd f" for f - using bnd prems by auto + using bnd that by auto show "card {s \ simplices. face f s} = 2" if "f \ ?F" "\ bnd f" for f - using nbnd prems by auto + using nbnd that by auto show "odd (card {f \ {f. \s\simplices. face f s}. rl ` f = {..n} \ bnd f})" using odd_card by simp diff -r 310853646597 -r abee0de69a89 src/HOL/ROOT --- 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" diff -r 310853646597 -r abee0de69a89 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- 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 = diff -r 310853646597 -r abee0de69a89 src/Pure/Isar/auto_bind.ML --- 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; diff -r 310853646597 -r abee0de69a89 src/Pure/Isar/element.ML --- 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; diff -r 310853646597 -r abee0de69a89 src/Pure/Isar/isar_syn.ML --- 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 _ = diff -r 310853646597 -r abee0de69a89 src/Pure/Isar/object_logic.ML --- 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; diff -r 310853646597 -r abee0de69a89 src/Pure/Isar/obtain.ML --- 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! - - - obtain x where "A x" == - - have "!!thesis. (!!x. A x ==> thesis) ==> thesis" - proof succeed - fix thesis - assume that [intro?]: "!!x. A x ==> thesis" - - show thesis - apply (insert that) - - qed - fix x assm <> "A x" - - - - guess x == - - { - fix thesis - have "PROP ?guess" - apply magic -- {* turns goal into "thesis ==> #thesis" *} - - apply_end magic -- {* turns final "(!!x. P x ==> thesis) ==> #thesis" into - "#((!!x. A x ==> thesis) ==> thesis)" which is a finished goal state *} - - } - fix x assm <> "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" == + + have thesis if a [intro?]: "!!x. A x ==> thesis" for thesis + apply (insert that) + + fix x assm <> "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 **) + +(* + + guess x == + + { + fix thesis + have "PROP ?guess" + apply magic -- {* turns goal into "thesis ==> #thesis" *} + + apply_end magic -- {* turns final "(!!x. P x ==> thesis) ==> #thesis" into + "#((!!x. A x ==> thesis) ==> thesis)" which is a finished goal state *} + + } + fix x assm <> "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; diff -r 310853646597 -r abee0de69a89 src/Pure/Isar/parse.ML --- 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) []; diff -r 310853646597 -r abee0de69a89 src/Pure/Isar/parse_spec.ML --- 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"; diff -r 310853646597 -r abee0de69a89 src/Pure/Isar/proof.ML --- 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))); diff -r 310853646597 -r abee0de69a89 src/Pure/Isar/rule_cases.ML --- 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 **) diff -r 310853646597 -r abee0de69a89 src/Pure/Isar/specification.ML --- 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); diff -r 310853646597 -r abee0de69a89 src/Pure/Pure.thy --- 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" diff -r 310853646597 -r abee0de69a89 src/Pure/logic.ML --- 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) = diff -r 310853646597 -r abee0de69a89 src/Tools/induct.ML --- 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;