1.1 --- a/NEWS Mon Apr 26 11:08:49 2010 -0700
1.2 +++ b/NEWS Mon Apr 26 22:59:28 2010 +0200
1.3 @@ -103,6 +103,9 @@
1.4 datatype constructors have been renamed from InfixName to Infix etc.
1.5 Minor INCOMPATIBILITY.
1.6
1.7 +* Command 'example_proof' opens an empty proof body. This allows to
1.8 +experiment with Isar, without producing any persistent result.
1.9 +
1.10 * Commands 'type_notation' and 'no_type_notation' declare type syntax
1.11 within a local theory context, with explicit checking of the
1.12 constructors involved (in contrast to the raw 'syntax' versions).
2.1 --- a/doc-src/IsarRef/Thy/Framework.thy Mon Apr 26 11:08:49 2010 -0700
2.2 +++ b/doc-src/IsarRef/Thy/Framework.thy Mon Apr 26 22:59:28 2010 +0200
2.3 @@ -79,8 +79,7 @@
2.4 text_raw {*\medskip\begin{minipage}{0.6\textwidth}*}
2.5
2.6 (*<*)
2.7 -lemma True
2.8 -proof
2.9 +example_proof
2.10 (*>*)
2.11 assume "x \<in> A" and "x \<in> B"
2.12 then have "x \<in> A \<inter> B" ..
2.13 @@ -107,8 +106,7 @@
2.14 *}
2.15
2.16 (*<*)
2.17 -lemma True
2.18 -proof
2.19 +example_proof
2.20 (*>*)
2.21 assume "x \<in> A" and "x \<in> B"
2.22 then have "x \<in> A \<inter> B" by (rule IntI)
2.23 @@ -130,8 +128,7 @@
2.24 text_raw {*\medskip\begin{minipage}{0.6\textwidth}*}
2.25
2.26 (*<*)
2.27 -lemma True
2.28 -proof
2.29 +example_proof
2.30 (*>*)
2.31 have "x \<in> \<Inter>\<A>"
2.32 proof
2.33 @@ -178,8 +175,7 @@
2.34 text_raw {*\medskip\begin{minipage}{0.6\textwidth}*}
2.35
2.36 (*<*)
2.37 -lemma True
2.38 -proof
2.39 +example_proof
2.40 (*>*)
2.41 assume "x \<in> \<Union>\<A>"
2.42 then have C
2.43 @@ -212,8 +208,7 @@
2.44 *}
2.45
2.46 (*<*)
2.47 -lemma True
2.48 -proof
2.49 +example_proof
2.50 (*>*)
2.51 assume "x \<in> \<Union>\<A>"
2.52 then obtain A where "x \<in> A" and "A \<in> \<A>" ..
2.53 @@ -817,8 +812,7 @@
2.54 *}
2.55
2.56 text_raw {* \begingroup\footnotesize *}
2.57 -(*<*)lemma True
2.58 -proof
2.59 +(*<*)example_proof
2.60 (*>*)
2.61 txt_raw {* \begin{minipage}[t]{0.18\textwidth} *}
2.62 have "A \<longrightarrow> B"
2.63 @@ -877,8 +871,7 @@
2.64 text_raw {*\begin{minipage}{0.5\textwidth}*}
2.65
2.66 (*<*)
2.67 -lemma True
2.68 -proof
2.69 +example_proof
2.70 (*>*)
2.71 have "\<And>x y. A x \<Longrightarrow> B y \<Longrightarrow> C x y"
2.72 proof -
2.73 @@ -987,8 +980,7 @@
2.74 *}
2.75
2.76 (*<*)
2.77 -lemma True
2.78 -proof
2.79 +example_proof
2.80 (*>*)
2.81 have "a = b" sorry
2.82 also have "\<dots> = c" sorry
3.1 --- a/doc-src/IsarRef/Thy/Proof.thy Mon Apr 26 11:08:49 2010 -0700
3.2 +++ b/doc-src/IsarRef/Thy/Proof.thy Mon Apr 26 22:59:28 2010 +0200
3.3 @@ -46,6 +46,28 @@
3.4
3.5 section {* Proof structure *}
3.6
3.7 +subsection {* Example proofs *}
3.8 +
3.9 +text {*
3.10 + \begin{matharray}{rcl}
3.11 + @{command_def "example_proof"} & : & @{text "local_theory \<rightarrow> proof(state)"} \\
3.12 + \end{matharray}
3.13 +
3.14 + \begin{description}
3.15 +
3.16 + \item @{command "example_proof"} opens an empty proof body. This
3.17 + allows to experiment with Isar, without producing any persistent
3.18 + result.
3.19 +
3.20 + Structurally, this is like a vacous @{command "lemma"} statement
3.21 + followed by ``@{command "proof"}~@{text "-"}'', which means the
3.22 + example proof may be closed by a regular @{command "qed"}, or
3.23 + discontinued by @{command "oops"}.
3.24 +
3.25 + \end{description}
3.26 +*}
3.27 +
3.28 +
3.29 subsection {* Blocks *}
3.30
3.31 text {*
4.1 --- a/doc-src/IsarRef/Thy/document/Framework.tex Mon Apr 26 11:08:49 2010 -0700
4.2 +++ b/doc-src/IsarRef/Thy/document/Framework.tex Mon Apr 26 22:59:28 2010 +0200
4.3 @@ -97,11 +97,11 @@
4.4 \medskip\begin{minipage}{0.6\textwidth}
4.5 %
4.6 \isadelimproof
4.7 -%
4.8 +\ \ \ \ %
4.9 \endisadelimproof
4.10 %
4.11 \isatagproof
4.12 -\ \ \ \ \isacommand{assume}\isamarkupfalse%
4.13 +\isacommand{assume}\isamarkupfalse%
4.14 \ {\isachardoublequoteopen}x\ {\isasymin}\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}x\ {\isasymin}\ B{\isachardoublequoteclose}\isanewline
4.15 \ \ \ \ \isacommand{then}\isamarkupfalse%
4.16 \ \isacommand{have}\isamarkupfalse%
4.17 @@ -135,11 +135,11 @@
4.18 \isamarkuptrue%
4.19 %
4.20 \isadelimproof
4.21 -%
4.22 +\ \ \ \ %
4.23 \endisadelimproof
4.24 %
4.25 \isatagproof
4.26 -\ \ \ \ \isacommand{assume}\isamarkupfalse%
4.27 +\isacommand{assume}\isamarkupfalse%
4.28 \ {\isachardoublequoteopen}x\ {\isasymin}\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}x\ {\isasymin}\ B{\isachardoublequoteclose}\isanewline
4.29 \ \ \ \ \isacommand{then}\isamarkupfalse%
4.30 \ \isacommand{have}\isamarkupfalse%
4.31 @@ -166,11 +166,11 @@
4.32 \medskip\begin{minipage}{0.6\textwidth}
4.33 %
4.34 \isadelimproof
4.35 -%
4.36 +\ \ \ \ %
4.37 \endisadelimproof
4.38 %
4.39 \isatagproof
4.40 -\ \ \ \ \isacommand{have}\isamarkupfalse%
4.41 +\isacommand{have}\isamarkupfalse%
4.42 \ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymInter}{\isasymA}{\isachardoublequoteclose}\isanewline
4.43 \ \ \ \ \isacommand{proof}\isamarkupfalse%
4.44 \isanewline
4.45 @@ -198,9 +198,9 @@
4.46 {\isafoldnoproof}%
4.47 %
4.48 \isadelimnoproof
4.49 -\isanewline
4.50 %
4.51 \endisadelimnoproof
4.52 +\isanewline
4.53 %
4.54 \isadelimproof
4.55 \ \ \ \ %
4.56 @@ -251,11 +251,11 @@
4.57 \medskip\begin{minipage}{0.6\textwidth}
4.58 %
4.59 \isadelimproof
4.60 -%
4.61 +\ \ \ \ %
4.62 \endisadelimproof
4.63 %
4.64 \isatagproof
4.65 -\ \ \ \ \isacommand{assume}\isamarkupfalse%
4.66 +\isacommand{assume}\isamarkupfalse%
4.67 \ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}{\isasymA}{\isachardoublequoteclose}\isanewline
4.68 \ \ \ \ \isacommand{then}\isamarkupfalse%
4.69 \ \isacommand{have}\isamarkupfalse%
4.70 @@ -286,9 +286,9 @@
4.71 {\isafoldnoproof}%
4.72 %
4.73 \isadelimnoproof
4.74 -\isanewline
4.75 %
4.76 \endisadelimnoproof
4.77 +\isanewline
4.78 %
4.79 \isadelimproof
4.80 \ \ \ \ %
4.81 @@ -326,11 +326,11 @@
4.82 \isamarkuptrue%
4.83 %
4.84 \isadelimproof
4.85 -%
4.86 +\ \ \ \ %
4.87 \endisadelimproof
4.88 %
4.89 \isatagproof
4.90 -\ \ \ \ \isacommand{assume}\isamarkupfalse%
4.91 +\isacommand{assume}\isamarkupfalse%
4.92 \ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}{\isasymA}{\isachardoublequoteclose}\isanewline
4.93 \ \ \ \ \isacommand{then}\isamarkupfalse%
4.94 \ \isacommand{obtain}\isamarkupfalse%
4.95 @@ -1186,9 +1186,9 @@
4.96 {\isafoldproof}%
4.97 %
4.98 \isadelimproof
4.99 -\isanewline
4.100 %
4.101 \endisadelimproof
4.102 +\isanewline
4.103 %
4.104 \isadelimnoproof
4.105 \ \ \ \ \ \ %
4.106 @@ -1201,9 +1201,9 @@
4.107 {\isafoldnoproof}%
4.108 %
4.109 \isadelimnoproof
4.110 -\isanewline
4.111 %
4.112 \endisadelimnoproof
4.113 +\isanewline
4.114 %
4.115 \isadelimproof
4.116 \ \ %
4.117 @@ -1268,11 +1268,11 @@
4.118 \begin{minipage}{0.5\textwidth}
4.119 %
4.120 \isadelimproof
4.121 -%
4.122 +\ \ %
4.123 \endisadelimproof
4.124 %
4.125 \isatagproof
4.126 -\ \ \isacommand{have}\isamarkupfalse%
4.127 +\isacommand{have}\isamarkupfalse%
4.128 \ {\isachardoublequoteopen}{\isasymAnd}x\ y{\isachardot}\ A\ x\ {\isasymLongrightarrow}\ B\ y\ {\isasymLongrightarrow}\ C\ x\ y{\isachardoublequoteclose}\isanewline
4.129 \ \ \isacommand{proof}\isamarkupfalse%
4.130 \ {\isacharminus}\isanewline
4.131 @@ -1300,9 +1300,9 @@
4.132 {\isafoldnoproof}%
4.133 %
4.134 \isadelimnoproof
4.135 -\isanewline
4.136 %
4.137 \endisadelimnoproof
4.138 +\isanewline
4.139 %
4.140 \isadelimproof
4.141 \ \ %
4.142 @@ -1342,9 +1342,9 @@
4.143 {\isafoldnoproof}%
4.144 %
4.145 \isadelimnoproof
4.146 -\isanewline
4.147 %
4.148 \endisadelimnoproof
4.149 +\isanewline
4.150 %
4.151 \isadelimproof
4.152 \ \ %
4.153 @@ -1456,11 +1456,11 @@
4.154 \isamarkuptrue%
4.155 %
4.156 \isadelimproof
4.157 -%
4.158 +\ \ %
4.159 \endisadelimproof
4.160 %
4.161 \isatagproof
4.162 -\ \ \isacommand{have}\isamarkupfalse%
4.163 +\isacommand{have}\isamarkupfalse%
4.164 \ {\isachardoublequoteopen}a\ {\isacharequal}\ b{\isachardoublequoteclose}\ \isacommand{sorry}\isamarkupfalse%
4.165 \isanewline
4.166 \ \ \isacommand{also}\isamarkupfalse%
5.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex Mon Apr 26 11:08:49 2010 -0700
5.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex Mon Apr 26 22:59:28 2010 +0200
5.3 @@ -65,6 +65,30 @@
5.4 }
5.5 \isamarkuptrue%
5.6 %
5.7 +\isamarkupsubsection{Example proofs%
5.8 +}
5.9 +\isamarkuptrue%
5.10 +%
5.11 +\begin{isamarkuptext}%
5.12 +\begin{matharray}{rcl}
5.13 + \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}} \\
5.14 + \end{matharray}
5.15 +
5.16 + \begin{description}
5.17 +
5.18 + \item \hyperlink{command.example-proof}{\mbox{\isa{\isacommand{example{\isacharunderscore}proof}}}} opens an empty proof body. This
5.19 + allows to experiment with Isar, without producing any persistent
5.20 + result.
5.21 +
5.22 + Structurally, this is like a vacous \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} statement
5.23 + followed by ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'', which means the
5.24 + example proof may be closed by a regular \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}, or
5.25 + discontinued by \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}}.
5.26 +
5.27 + \end{description}%
5.28 +\end{isamarkuptext}%
5.29 +\isamarkuptrue%
5.30 +%
5.31 \isamarkupsubsection{Blocks%
5.32 }
5.33 \isamarkuptrue%
6.1 --- a/etc/isar-keywords-ZF.el Mon Apr 26 11:08:49 2010 -0700
6.2 +++ b/etc/isar-keywords-ZF.el Mon Apr 26 22:59:28 2010 +0200
6.3 @@ -66,6 +66,7 @@
6.4 "done"
6.5 "enable_pr"
6.6 "end"
6.7 + "example_proof"
6.8 "exit"
6.9 "extract"
6.10 "extract_type"
6.11 @@ -425,6 +426,7 @@
6.12
6.13 (defconst isar-keywords-theory-goal
6.14 '("corollary"
6.15 + "example_proof"
6.16 "instance"
6.17 "interpretation"
6.18 "lemma"
7.1 --- a/etc/isar-keywords.el Mon Apr 26 11:08:49 2010 -0700
7.2 +++ b/etc/isar-keywords.el Mon Apr 26 22:59:28 2010 +0200
7.3 @@ -94,6 +94,7 @@
7.4 "enable_pr"
7.5 "end"
7.6 "equivariance"
7.7 + "example_proof"
7.8 "exit"
7.9 "export_code"
7.10 "extract"
7.11 @@ -562,6 +563,7 @@
7.12 "code_pred"
7.13 "corollary"
7.14 "cpodef"
7.15 + "example_proof"
7.16 "function"
7.17 "instance"
7.18 "interpretation"
8.1 --- a/src/Pure/Isar/isar_syn.ML Mon Apr 26 11:08:49 2010 -0700
8.2 +++ b/src/Pure/Isar/isar_syn.ML Mon Apr 26 22:59:28 2010 +0200
8.3 @@ -510,6 +510,13 @@
8.4 val _ = gen_theorem true Thm.corollaryK;
8.5
8.6 val _ =
8.7 + OuterSyntax.local_theory_to_proof "example_proof"
8.8 + "example proof body, without any result" K.thy_schematic_goal
8.9 + (Scan.succeed
8.10 + (Specification.schematic_theorem_cmd "" NONE (K I)
8.11 + Attrib.empty_binding [] (Element.Shows []) false #> Proof.enter_forward));
8.12 +
8.13 +val _ =
8.14 OuterSyntax.command "have" "state local goal"
8.15 (K.tag_proof K.prf_goal)
8.16 (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have));
9.1 --- a/src/Pure/Isar/overloading.ML Mon Apr 26 11:08:49 2010 -0700
9.2 +++ b/src/Pure/Isar/overloading.ML Mon Apr 26 22:59:28 2010 +0200
9.3 @@ -67,8 +67,8 @@
9.4
9.5 fun improve_term_check ts ctxt =
9.6 let
9.7 - val { primary_constraints, secondary_constraints, improve, subst,
9.8 - consider_abbrevs, passed, ... } = ImprovableSyntax.get ctxt;
9.9 + val { secondary_constraints, improve, subst, consider_abbrevs, passed, ... } =
9.10 + ImprovableSyntax.get ctxt;
9.11 val tsig = (Sign.tsig_of o ProofContext.theory_of) ctxt;
9.12 val is_abbrev = consider_abbrevs andalso ProofContext.abbrev_mode ctxt;
9.13 val passed_or_abbrev = passed orelse is_abbrev;
10.1 --- a/src/Pure/Isar/proof.ML Mon Apr 26 11:08:49 2010 -0700
10.2 +++ b/src/Pure/Isar/proof.ML Mon Apr 26 22:59:28 2010 +0200
10.3 @@ -792,7 +792,7 @@
10.4
10.5 fun implicit_vars props =
10.6 let
10.7 - val (var_props, props') = take_prefix is_var props;
10.8 + val (var_props, _) = take_prefix is_var props;
10.9 val explicit_vars = fold Term.add_vars var_props [];
10.10 val vars = filter_out (member (op =) explicit_vars) (fold Term.add_vars props []);
10.11 in map (Logic.mk_term o Var) vars end;
10.12 @@ -845,11 +845,10 @@
10.13
10.14 fun generic_qed after_ctxt state =
10.15 let
10.16 - val (goal_ctxt, {statement, goal, after_qed, ...}) = current_goal state;
10.17 + val (goal_ctxt, {statement = (_, stmt, _), goal, after_qed, ...}) = current_goal state;
10.18 val outer_state = state |> close_block;
10.19 val outer_ctxt = context_of outer_state;
10.20
10.21 - val ((_, pos), stmt, _) = statement;
10.22 val props =
10.23 flat (tl stmt)
10.24 |> Variable.exportT_terms goal_ctxt outer_ctxt;
11.1 --- a/src/Pure/Isar/rule_cases.ML Mon Apr 26 11:08:49 2010 -0700
11.2 +++ b/src/Pure/Isar/rule_cases.ML Mon Apr 26 22:59:28 2010 +0200
11.3 @@ -368,7 +368,7 @@
11.4 map (Name.internal o Name.clean o fst) (Logic.strip_params prem)
11.5 in Logic.list_rename_params (xs, prem) end;
11.6 fun rename_prems prop =
11.7 - let val (As, C) = Logic.strip_horn (Thm.prop_of rule)
11.8 + let val (As, C) = Logic.strip_horn prop
11.9 in Logic.list_implies (map rename As, C) end;
11.10 in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end;
11.11
12.1 --- a/src/Pure/Isar/toplevel.ML Mon Apr 26 11:08:49 2010 -0700
12.2 +++ b/src/Pure/Isar/toplevel.ML Mon Apr 26 22:59:28 2010 +0200
12.3 @@ -661,6 +661,7 @@
12.4 if immediate orelse
12.5 null proof_trs orelse
12.6 OuterKeyword.is_schematic_goal (name_of tr) orelse
12.7 + exists (OuterKeyword.is_qed_global o name_of) proof_trs orelse
12.8 not (can proof_of st') orelse
12.9 Proof.is_relevant (proof_of st')
12.10 then
13.1 --- a/src/Pure/meta_simplifier.ML Mon Apr 26 11:08:49 2010 -0700
13.2 +++ b/src/Pure/meta_simplifier.ML Mon Apr 26 22:59:28 2010 +0200
13.3 @@ -834,7 +834,6 @@
13.4 in if msg then trace_thm (fn () => "SUCCEEDED") ss thm' else (); SOME thm'' end
13.5 handle THM _ =>
13.6 let
13.7 - val thy = Thm.theory_of_thm thm;
13.8 val _ $ _ $ prop0 = Thm.prop_of thm;
13.9 in
13.10 trace_thm (fn () => "Proved wrong thm (Check subgoaler?)") ss thm';
14.1 --- a/src/Pure/tactic.ML Mon Apr 26 11:08:49 2010 -0700
14.2 +++ b/src/Pure/tactic.ML Mon Apr 26 22:59:28 2010 +0200
14.3 @@ -188,9 +188,6 @@
14.4 let val (_, _, Bi, _) = dest_state (st, i)
14.5 in Term.rename_wrt_term Bi (Logic.strip_params Bi) end;
14.6
14.7 -(*params of subgoal i as they are printed*)
14.8 -fun params_of_state i st = rev (innermost_params i st);
14.9 -
14.10
14.11 (*** Applications of cut_rl ***)
14.12