# HG changeset patch # User wenzelm # Date 1272315568 -7200 # Node ID 1b5b9bbab0063088740862bb98f4e7ed4a095258 # Parent 49c7dee21a7f3344b28446452a2cee9bbb3f548a# Parent 641a521bfc1953cfe91530aa15ce4f7507aff663 merged diff -r 49c7dee21a7f -r 1b5b9bbab006 NEWS --- a/NEWS Mon Apr 26 11:08:49 2010 -0700 +++ b/NEWS Mon Apr 26 22:59:28 2010 +0200 @@ -103,6 +103,9 @@ datatype constructors have been renamed from InfixName to Infix etc. Minor INCOMPATIBILITY. +* Command 'example_proof' opens an empty proof body. This allows to +experiment with Isar, without producing any persistent result. + * Commands 'type_notation' and 'no_type_notation' declare type syntax within a local theory context, with explicit checking of the constructors involved (in contrast to the raw 'syntax' versions). diff -r 49c7dee21a7f -r 1b5b9bbab006 doc-src/IsarRef/Thy/Framework.thy --- a/doc-src/IsarRef/Thy/Framework.thy Mon Apr 26 11:08:49 2010 -0700 +++ b/doc-src/IsarRef/Thy/Framework.thy Mon Apr 26 22:59:28 2010 +0200 @@ -79,8 +79,7 @@ text_raw {*\medskip\begin{minipage}{0.6\textwidth}*} (*<*) -lemma True -proof +example_proof (*>*) assume "x \ A" and "x \ B" then have "x \ A \ B" .. @@ -107,8 +106,7 @@ *} (*<*) -lemma True -proof +example_proof (*>*) assume "x \ A" and "x \ B" then have "x \ A \ B" by (rule IntI) @@ -130,8 +128,7 @@ text_raw {*\medskip\begin{minipage}{0.6\textwidth}*} (*<*) -lemma True -proof +example_proof (*>*) have "x \ \\" proof @@ -178,8 +175,7 @@ text_raw {*\medskip\begin{minipage}{0.6\textwidth}*} (*<*) -lemma True -proof +example_proof (*>*) assume "x \ \\" then have C @@ -212,8 +208,7 @@ *} (*<*) -lemma True -proof +example_proof (*>*) assume "x \ \\" then obtain A where "x \ A" and "A \ \" .. @@ -817,8 +812,7 @@ *} text_raw {* \begingroup\footnotesize *} -(*<*)lemma True -proof +(*<*)example_proof (*>*) txt_raw {* \begin{minipage}[t]{0.18\textwidth} *} have "A \ B" @@ -877,8 +871,7 @@ text_raw {*\begin{minipage}{0.5\textwidth}*} (*<*) -lemma True -proof +example_proof (*>*) have "\x y. A x \ B y \ C x y" proof - @@ -987,8 +980,7 @@ *} (*<*) -lemma True -proof +example_proof (*>*) have "a = b" sorry also have "\ = c" sorry diff -r 49c7dee21a7f -r 1b5b9bbab006 doc-src/IsarRef/Thy/Proof.thy --- a/doc-src/IsarRef/Thy/Proof.thy Mon Apr 26 11:08:49 2010 -0700 +++ b/doc-src/IsarRef/Thy/Proof.thy Mon Apr 26 22:59:28 2010 +0200 @@ -46,6 +46,28 @@ section {* Proof structure *} +subsection {* Example proofs *} + +text {* + \begin{matharray}{rcl} + @{command_def "example_proof"} & : & @{text "local_theory \ proof(state)"} \\ + \end{matharray} + + \begin{description} + + \item @{command "example_proof"} opens an empty proof body. This + allows to experiment with Isar, without producing any persistent + result. + + Structurally, this is like a vacous @{command "lemma"} statement + followed by ``@{command "proof"}~@{text "-"}'', which means the + example proof may be closed by a regular @{command "qed"}, or + discontinued by @{command "oops"}. + + \end{description} +*} + + subsection {* Blocks *} text {* diff -r 49c7dee21a7f -r 1b5b9bbab006 doc-src/IsarRef/Thy/document/Framework.tex --- a/doc-src/IsarRef/Thy/document/Framework.tex Mon Apr 26 11:08:49 2010 -0700 +++ b/doc-src/IsarRef/Thy/document/Framework.tex Mon Apr 26 22:59:28 2010 +0200 @@ -97,11 +97,11 @@ \medskip\begin{minipage}{0.6\textwidth} % \isadelimproof -% +\ \ \ \ % \endisadelimproof % \isatagproof -\ \ \ \ \isacommand{assume}\isamarkupfalse% +\isacommand{assume}\isamarkupfalse% \ {\isachardoublequoteopen}x\ {\isasymin}\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}x\ {\isasymin}\ B{\isachardoublequoteclose}\isanewline \ \ \ \ \isacommand{then}\isamarkupfalse% \ \isacommand{have}\isamarkupfalse% @@ -135,11 +135,11 @@ \isamarkuptrue% % \isadelimproof -% +\ \ \ \ % \endisadelimproof % \isatagproof -\ \ \ \ \isacommand{assume}\isamarkupfalse% +\isacommand{assume}\isamarkupfalse% \ {\isachardoublequoteopen}x\ {\isasymin}\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}x\ {\isasymin}\ B{\isachardoublequoteclose}\isanewline \ \ \ \ \isacommand{then}\isamarkupfalse% \ \isacommand{have}\isamarkupfalse% @@ -166,11 +166,11 @@ \medskip\begin{minipage}{0.6\textwidth} % \isadelimproof -% +\ \ \ \ % \endisadelimproof % \isatagproof -\ \ \ \ \isacommand{have}\isamarkupfalse% +\isacommand{have}\isamarkupfalse% \ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymInter}{\isasymA}{\isachardoublequoteclose}\isanewline \ \ \ \ \isacommand{proof}\isamarkupfalse% \isanewline @@ -198,9 +198,9 @@ {\isafoldnoproof}% % \isadelimnoproof -\isanewline % \endisadelimnoproof +\isanewline % \isadelimproof \ \ \ \ % @@ -251,11 +251,11 @@ \medskip\begin{minipage}{0.6\textwidth} % \isadelimproof -% +\ \ \ \ % \endisadelimproof % \isatagproof -\ \ \ \ \isacommand{assume}\isamarkupfalse% +\isacommand{assume}\isamarkupfalse% \ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}{\isasymA}{\isachardoublequoteclose}\isanewline \ \ \ \ \isacommand{then}\isamarkupfalse% \ \isacommand{have}\isamarkupfalse% @@ -286,9 +286,9 @@ {\isafoldnoproof}% % \isadelimnoproof -\isanewline % \endisadelimnoproof +\isanewline % \isadelimproof \ \ \ \ % @@ -326,11 +326,11 @@ \isamarkuptrue% % \isadelimproof -% +\ \ \ \ % \endisadelimproof % \isatagproof -\ \ \ \ \isacommand{assume}\isamarkupfalse% +\isacommand{assume}\isamarkupfalse% \ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}{\isasymA}{\isachardoublequoteclose}\isanewline \ \ \ \ \isacommand{then}\isamarkupfalse% \ \isacommand{obtain}\isamarkupfalse% @@ -1186,9 +1186,9 @@ {\isafoldproof}% % \isadelimproof -\isanewline % \endisadelimproof +\isanewline % \isadelimnoproof \ \ \ \ \ \ % @@ -1201,9 +1201,9 @@ {\isafoldnoproof}% % \isadelimnoproof -\isanewline % \endisadelimnoproof +\isanewline % \isadelimproof \ \ % @@ -1268,11 +1268,11 @@ \begin{minipage}{0.5\textwidth} % \isadelimproof -% +\ \ % \endisadelimproof % \isatagproof -\ \ \isacommand{have}\isamarkupfalse% +\isacommand{have}\isamarkupfalse% \ {\isachardoublequoteopen}{\isasymAnd}x\ y{\isachardot}\ A\ x\ {\isasymLongrightarrow}\ B\ y\ {\isasymLongrightarrow}\ C\ x\ y{\isachardoublequoteclose}\isanewline \ \ \isacommand{proof}\isamarkupfalse% \ {\isacharminus}\isanewline @@ -1300,9 +1300,9 @@ {\isafoldnoproof}% % \isadelimnoproof -\isanewline % \endisadelimnoproof +\isanewline % \isadelimproof \ \ % @@ -1342,9 +1342,9 @@ {\isafoldnoproof}% % \isadelimnoproof -\isanewline % \endisadelimnoproof +\isanewline % \isadelimproof \ \ % @@ -1456,11 +1456,11 @@ \isamarkuptrue% % \isadelimproof -% +\ \ % \endisadelimproof % \isatagproof -\ \ \isacommand{have}\isamarkupfalse% +\isacommand{have}\isamarkupfalse% \ {\isachardoublequoteopen}a\ {\isacharequal}\ b{\isachardoublequoteclose}\ \isacommand{sorry}\isamarkupfalse% \isanewline \ \ \isacommand{also}\isamarkupfalse% diff -r 49c7dee21a7f -r 1b5b9bbab006 doc-src/IsarRef/Thy/document/Proof.tex --- a/doc-src/IsarRef/Thy/document/Proof.tex Mon Apr 26 11:08:49 2010 -0700 +++ b/doc-src/IsarRef/Thy/document/Proof.tex Mon Apr 26 22:59:28 2010 +0200 @@ -65,6 +65,30 @@ } \isamarkuptrue% % +\isamarkupsubsection{Example proofs% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{}{command}{example\_proof}\hypertarget{command.example-proof}{\hyperlink{command.example-proof}{\mbox{\isa{\isacommand{example{\isacharunderscore}proof}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}} \\ + \end{matharray} + + \begin{description} + + \item \hyperlink{command.example-proof}{\mbox{\isa{\isacommand{example{\isacharunderscore}proof}}}} opens an empty proof body. This + allows to experiment with Isar, without producing any persistent + result. + + Structurally, this is like a vacous \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} statement + followed by ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'', which means the + example proof may be closed by a regular \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}, or + discontinued by \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}}. + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% \isamarkupsubsection{Blocks% } \isamarkuptrue% diff -r 49c7dee21a7f -r 1b5b9bbab006 etc/isar-keywords-ZF.el --- a/etc/isar-keywords-ZF.el Mon Apr 26 11:08:49 2010 -0700 +++ b/etc/isar-keywords-ZF.el Mon Apr 26 22:59:28 2010 +0200 @@ -66,6 +66,7 @@ "done" "enable_pr" "end" + "example_proof" "exit" "extract" "extract_type" @@ -425,6 +426,7 @@ (defconst isar-keywords-theory-goal '("corollary" + "example_proof" "instance" "interpretation" "lemma" diff -r 49c7dee21a7f -r 1b5b9bbab006 etc/isar-keywords.el --- a/etc/isar-keywords.el Mon Apr 26 11:08:49 2010 -0700 +++ b/etc/isar-keywords.el Mon Apr 26 22:59:28 2010 +0200 @@ -94,6 +94,7 @@ "enable_pr" "end" "equivariance" + "example_proof" "exit" "export_code" "extract" @@ -562,6 +563,7 @@ "code_pred" "corollary" "cpodef" + "example_proof" "function" "instance" "interpretation" diff -r 49c7dee21a7f -r 1b5b9bbab006 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Mon Apr 26 11:08:49 2010 -0700 +++ b/src/Pure/Isar/isar_syn.ML Mon Apr 26 22:59:28 2010 +0200 @@ -510,6 +510,13 @@ val _ = gen_theorem true Thm.corollaryK; val _ = + OuterSyntax.local_theory_to_proof "example_proof" + "example proof body, without any result" K.thy_schematic_goal + (Scan.succeed + (Specification.schematic_theorem_cmd "" NONE (K I) + Attrib.empty_binding [] (Element.Shows []) false #> Proof.enter_forward)); + +val _ = OuterSyntax.command "have" "state local goal" (K.tag_proof K.prf_goal) (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have)); diff -r 49c7dee21a7f -r 1b5b9bbab006 src/Pure/Isar/overloading.ML --- a/src/Pure/Isar/overloading.ML Mon Apr 26 11:08:49 2010 -0700 +++ b/src/Pure/Isar/overloading.ML Mon Apr 26 22:59:28 2010 +0200 @@ -67,8 +67,8 @@ fun improve_term_check ts ctxt = let - val { primary_constraints, secondary_constraints, improve, subst, - consider_abbrevs, passed, ... } = ImprovableSyntax.get ctxt; + val { secondary_constraints, improve, subst, consider_abbrevs, passed, ... } = + ImprovableSyntax.get ctxt; val tsig = (Sign.tsig_of o ProofContext.theory_of) ctxt; val is_abbrev = consider_abbrevs andalso ProofContext.abbrev_mode ctxt; val passed_or_abbrev = passed orelse is_abbrev; diff -r 49c7dee21a7f -r 1b5b9bbab006 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Mon Apr 26 11:08:49 2010 -0700 +++ b/src/Pure/Isar/proof.ML Mon Apr 26 22:59:28 2010 +0200 @@ -792,7 +792,7 @@ fun implicit_vars props = let - val (var_props, props') = take_prefix is_var props; + val (var_props, _) = take_prefix is_var props; val explicit_vars = fold Term.add_vars var_props []; val vars = filter_out (member (op =) explicit_vars) (fold Term.add_vars props []); in map (Logic.mk_term o Var) vars end; @@ -845,11 +845,10 @@ fun generic_qed after_ctxt state = let - val (goal_ctxt, {statement, goal, after_qed, ...}) = current_goal state; + val (goal_ctxt, {statement = (_, stmt, _), goal, after_qed, ...}) = current_goal state; val outer_state = state |> close_block; val outer_ctxt = context_of outer_state; - val ((_, pos), stmt, _) = statement; val props = flat (tl stmt) |> Variable.exportT_terms goal_ctxt outer_ctxt; diff -r 49c7dee21a7f -r 1b5b9bbab006 src/Pure/Isar/rule_cases.ML --- a/src/Pure/Isar/rule_cases.ML Mon Apr 26 11:08:49 2010 -0700 +++ b/src/Pure/Isar/rule_cases.ML Mon Apr 26 22:59:28 2010 +0200 @@ -368,7 +368,7 @@ 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 (Thm.prop_of rule) + let val (As, C) = Logic.strip_horn prop in Logic.list_implies (map rename As, C) end; in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end; diff -r 49c7dee21a7f -r 1b5b9bbab006 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Mon Apr 26 11:08:49 2010 -0700 +++ b/src/Pure/Isar/toplevel.ML Mon Apr 26 22:59:28 2010 +0200 @@ -661,6 +661,7 @@ if immediate orelse null proof_trs orelse OuterKeyword.is_schematic_goal (name_of tr) orelse + exists (OuterKeyword.is_qed_global o name_of) proof_trs orelse not (can proof_of st') orelse Proof.is_relevant (proof_of st') then diff -r 49c7dee21a7f -r 1b5b9bbab006 src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Mon Apr 26 11:08:49 2010 -0700 +++ b/src/Pure/meta_simplifier.ML Mon Apr 26 22:59:28 2010 +0200 @@ -834,7 +834,6 @@ in if msg then trace_thm (fn () => "SUCCEEDED") ss thm' else (); SOME thm'' end handle THM _ => let - val thy = Thm.theory_of_thm thm; val _ $ _ $ prop0 = Thm.prop_of thm; in trace_thm (fn () => "Proved wrong thm (Check subgoaler?)") ss thm'; diff -r 49c7dee21a7f -r 1b5b9bbab006 src/Pure/tactic.ML --- a/src/Pure/tactic.ML Mon Apr 26 11:08:49 2010 -0700 +++ b/src/Pure/tactic.ML Mon Apr 26 22:59:28 2010 +0200 @@ -188,9 +188,6 @@ let val (_, _, Bi, _) = dest_state (st, i) in Term.rename_wrt_term Bi (Logic.strip_params Bi) end; -(*params of subgoal i as they are printed*) -fun params_of_state i st = rev (innermost_params i st); - (*** Applications of cut_rl ***)