--- 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).
--- 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 \<in> A" and "x \<in> B"
then have "x \<in> A \<inter> B" ..
@@ -107,8 +106,7 @@
*}
(*<*)
-lemma True
-proof
+example_proof
(*>*)
assume "x \<in> A" and "x \<in> B"
then have "x \<in> A \<inter> B" by (rule IntI)
@@ -130,8 +128,7 @@
text_raw {*\medskip\begin{minipage}{0.6\textwidth}*}
(*<*)
-lemma True
-proof
+example_proof
(*>*)
have "x \<in> \<Inter>\<A>"
proof
@@ -178,8 +175,7 @@
text_raw {*\medskip\begin{minipage}{0.6\textwidth}*}
(*<*)
-lemma True
-proof
+example_proof
(*>*)
assume "x \<in> \<Union>\<A>"
then have C
@@ -212,8 +208,7 @@
*}
(*<*)
-lemma True
-proof
+example_proof
(*>*)
assume "x \<in> \<Union>\<A>"
then obtain A where "x \<in> A" and "A \<in> \<A>" ..
@@ -817,8 +812,7 @@
*}
text_raw {* \begingroup\footnotesize *}
-(*<*)lemma True
-proof
+(*<*)example_proof
(*>*)
txt_raw {* \begin{minipage}[t]{0.18\textwidth} *}
have "A \<longrightarrow> B"
@@ -877,8 +871,7 @@
text_raw {*\begin{minipage}{0.5\textwidth}*}
(*<*)
-lemma True
-proof
+example_proof
(*>*)
have "\<And>x y. A x \<Longrightarrow> B y \<Longrightarrow> C x y"
proof -
@@ -987,8 +980,7 @@
*}
(*<*)
-lemma True
-proof
+example_proof
(*>*)
have "a = b" sorry
also have "\<dots> = c" sorry
--- 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 \<rightarrow> 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 {*
--- 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%
--- 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%
--- 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"
--- 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"
--- 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));
--- 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;
--- 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;
--- 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;
--- 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
--- 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';
--- 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 ***)