summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sun, 07 Feb 2016 19:43:40 +0100 | |

changeset 62271 | 4cfe65cfd369 |

parent 62270 | 77e3ffb5aeb3 |

child 62272 | e6669fdfe759 |

more explicit dummy proofs;

--- a/src/Doc/Isar_Ref/First_Order_Logic.thy Sun Feb 07 19:33:42 2016 +0100 +++ b/src/Doc/Isar_Ref/First_Order_Logic.thy Sun Feb 07 19:43:40 2016 +0100 @@ -418,47 +418,47 @@ have "A \<longrightarrow> B" proof assume A - show B sorry %noproof + show B \<proof> qed text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) - have "A \<longrightarrow> B" and A sorry %noproof + have "A \<longrightarrow> B" and A \<proof> then have B .. text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) - have A sorry %noproof + have A \<proof> then have "A \<or> B" .. - have B sorry %noproof + have B \<proof> then have "A \<or> B" .. text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) - have "A \<or> B" sorry %noproof + have "A \<or> B" \<proof> then have C proof assume A - then show C sorry %noproof + then show C \<proof> next assume B - then show C sorry %noproof + then show C \<proof> qed text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) - have A and B sorry %noproof + have A and B \<proof> then have "A \<and> B" .. text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) - have "A \<and> B" sorry %noproof + have "A \<and> B" \<proof> then obtain A and B .. text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) - have "\<bottom>" sorry %noproof + have "\<bottom>" \<proof> then have A .. text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) @@ -470,12 +470,12 @@ have "\<not> A" proof assume A - then show "\<bottom>" sorry %noproof + then show "\<bottom>" \<proof> qed text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) - have "\<not> A" and A sorry %noproof + have "\<not> A" and A \<proof> then have B .. text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) @@ -483,24 +483,24 @@ have "\<forall>x. B x" proof fix x - show "B x" sorry %noproof + show "B x" \<proof> qed text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) - have "\<forall>x. B x" sorry %noproof + have "\<forall>x. B x" \<proof> then have "B a" .. text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) have "\<exists>x. B x" proof - show "B a" sorry %noproof + show "B a" \<proof> qed text_raw \<open>\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}\<close>(*<*)next(*>*) - have "\<exists>x. B x" sorry %noproof + have "\<exists>x. B x" \<proof> then obtain a where "B a" .. text_raw \<open>\end{minipage}\<close>

--- a/src/Doc/Isar_Ref/Framework.thy Sun Feb 07 19:33:42 2016 +0100 +++ b/src/Doc/Isar_Ref/Framework.thy Sun Feb 07 19:43:40 2016 +0100 @@ -141,7 +141,7 @@ proof fix A assume "A \<in> \<A>" - show "x \<in> A" sorry %noproof + show "x \<in> A" \<proof> qed (*<*) end @@ -192,7 +192,7 @@ proof fix A assume "x \<in> A" and "A \<in> \<A>" - show C sorry %noproof + show C \<proof> qed (*<*) end @@ -664,25 +664,25 @@ text_raw \<open>\begin{minipage}[t]{0.45\textwidth}\<close> { fix x - have "B x" sorry %noproof + have "B x" \<proof> } note \<open>\<And>x. B x\<close> text_raw \<open>\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*) { assume A - have B sorry %noproof + have B \<proof> } note \<open>A \<Longrightarrow> B\<close> text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*) { def x \<equiv> a - have "B x" sorry %noproof + have "B x" \<proof> } note \<open>B a\<close> text_raw \<open>\end{minipage}\quad\begin{minipage}[t]{0.45\textwidth}\<close>(*<*)next(*>*) { - obtain x where "A x" sorry %noproof - have B sorry %noproof + obtain x where "A x" \<proof> + have B \<proof> } note \<open>B\<close> text_raw \<open>\end{minipage}\<close> @@ -754,7 +754,7 @@ shows "C x y" proof - from \<open>A x\<close> and \<open>B y\<close> - show "C x y" sorry %noproof + show "C x y" \<proof> qed text_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close> @@ -763,7 +763,7 @@ obtains x and y where "A x" and "B y" proof - - have "A a" and "B b" sorry %noproof + have "A a" and "B b" \<proof> then show thesis .. qed @@ -833,7 +833,7 @@ proof assume A show B - sorry %noproof + \<proof> qed text_raw \<open>\end{minipage}\quad \begin{minipage}[t]{0.06\textwidth} @@ -892,7 +892,7 @@ proof - fix x and y assume "A x" and "B y" - show "C x y" sorry %noproof + show "C x y" \<proof> qed text_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close> @@ -904,7 +904,7 @@ proof - fix x assume "A x" fix y assume "B y" - show "C x y" sorry %noproof + show "C x y" \<proof> qed text_raw \<open>\end{minipage}\\[3ex]\begin{minipage}{0.5\textwidth}\<close> @@ -916,7 +916,7 @@ proof - fix y assume "B y" fix x assume "A x" - show "C x y" sorry + show "C x y" \<proof> qed text_raw \<open>\end{minipage}\begin{minipage}{0.5\textwidth}\<close> @@ -927,7 +927,7 @@ proof - fix y assume "B y" fix x - show "C x y" sorry + show "C x y" \<proof> qed (*<*) end @@ -1000,9 +1000,9 @@ notepad begin (*>*) - have "a = b" sorry - also have "\<dots> = c" sorry - also have "\<dots> = d" sorry + have "a = b" \<proof> + also have "\<dots> = c" \<proof> + also have "\<dots> = d" \<proof> finally have "a = d" . (*<*) end

--- a/src/Doc/Isar_Ref/Proof_Script.thy Sun Feb 07 19:33:42 2016 +0100 +++ b/src/Doc/Isar_Ref/Proof_Script.thy Sun Feb 07 19:43:40 2016 +0100 @@ -133,24 +133,24 @@ lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z" and "\<And>u v. X u \<Longrightarrow> Y v" - subgoal sorry - subgoal sorry + subgoal \<proof> + subgoal \<proof> done lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z" and "\<And>u v. X u \<Longrightarrow> Y v" - subgoal for x y z sorry - subgoal for u v sorry + subgoal for x y z \<proof> + subgoal for u v \<proof> done lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z" and "\<And>u v. X u \<Longrightarrow> Y v" subgoal premises for x y z using \<open>A x\<close> \<open>B y\<close> - sorry + \<proof> subgoal premises for u v using \<open>X u\<close> - sorry + \<proof> done lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z" @@ -159,21 +159,21 @@ proof - have "A x" by (fact prems) moreover have "B y" by (fact prems) - ultimately show ?thesis sorry + ultimately show ?thesis \<proof> qed subgoal premises prems for u v proof - have "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z" by (fact r) moreover have "X u" by (fact prems) - ultimately show ?thesis sorry + ultimately show ?thesis \<proof> qed done lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z" subgoal premises prems for \<dots> z proof - - from prems show "C z" sorry + from prems show "C z" \<proof> qed done

--- a/src/Doc/Isar_Ref/Synopsis.thy Sun Feb 07 19:33:42 2016 +0100 +++ b/src/Doc/Isar_Ref/Synopsis.thy Sun Feb 07 19:43:40 2016 +0100 @@ -53,7 +53,7 @@ assume a: A txt \<open>Via proof (``let''):\<close> - have b: B sorry + have b: B \<proof> txt \<open>Via abbreviation (``let''):\<close> note c = a b @@ -156,8 +156,8 @@ notepad begin { - have a: A sorry - have b: B sorry + have a: A \<proof> + have b: B \<proof> note a b } note this @@ -174,15 +174,15 @@ begin { - have a: A sorry + have a: A \<proof> next have b: B proof - - show B sorry + show B \<proof> next - have c: C sorry + have c: C \<proof> next - have d: D sorry + have d: D \<proof> qed } @@ -190,19 +190,19 @@ { { - have a: A sorry + have a: A \<proof> } { have b: B proof - { - show B sorry + show B \<proof> } { - have c: C sorry + have c: C \<proof> } { - have d: D sorry + have d: D \<proof> } qed } @@ -235,7 +235,7 @@ have "x = y" proof - term ?thesis - show ?thesis sorry + show ?thesis \<proof> term ?thesis \<comment> \<open>static!\<close> qed term "\<dots>" @@ -260,31 +260,31 @@ notepad begin txt \<open>Plain bottom-up calculation:\<close> - have "a = b" sorry + have "a = b" \<proof> also - have "b = c" sorry + have "b = c" \<proof> also - have "c = d" sorry + have "c = d" \<proof> finally have "a = d" . txt \<open>Variant using the \<open>\<dots>\<close> abbreviation:\<close> - have "a = b" sorry + have "a = b" \<proof> also - have "\<dots> = c" sorry + have "\<dots> = c" \<proof> also - have "\<dots> = d" sorry + have "\<dots> = d" \<proof> finally have "a = d" . txt \<open>Top-down version with explicit claim at the head:\<close> have "a = d" proof - - have "a = b" sorry + have "a = b" \<proof> also - have "\<dots> = c" sorry + have "\<dots> = c" \<proof> also - have "\<dots> = d" sorry + have "\<dots> = d" \<proof> finally show ?thesis . qed @@ -292,11 +292,11 @@ txt \<open>Mixed inequalities (require suitable base type):\<close> fix a b c d :: nat - have "a < b" sorry + have "a < b" \<proof> also - have "b \<le> c" sorry + have "b \<le> c" \<proof> also - have "c = d" sorry + have "c = d" \<proof> finally have "a < d" . end @@ -321,31 +321,31 @@ notepad begin txt \<open>A vacuous proof:\<close> - have A sorry + have A \<proof> moreover - have B sorry + have B \<proof> moreover - have C sorry + have C \<proof> ultimately have A and B and C . next txt \<open>Slightly more content (trivial bigstep reasoning):\<close> - have A sorry + have A \<proof> moreover - have B sorry + have B \<proof> moreover - have C sorry + have C \<proof> ultimately have "A \<and> B \<and> C" by blast next txt \<open>More ambitious bigstep reasoning involving structured results:\<close> - have "A \<or> B \<or> C" sorry + have "A \<or> B \<or> C" \<proof> moreover - { assume A have R sorry } + { assume A have R \<proof> } moreover - { assume B have R sorry } + { assume B have R \<proof> } moreover - { assume C have R sorry } + { assume C have R \<proof> } ultimately have R by blast \<comment> \<open>``big-bang integration'' of proof blocks (occasionally fragile)\<close> end @@ -367,11 +367,11 @@ fix n :: nat have "P n" proof (rule nat.induct) \<comment> \<open>fragile rule application!\<close> - show "P 0" sorry + show "P 0" \<proof> next fix n :: nat assume "P n" - show "P (Suc n)" sorry + show "P (Suc n)" \<proof> qed end @@ -394,10 +394,10 @@ have "P n" proof (induct n) case 0 - show ?case sorry + show ?case \<proof> next case (Suc n) - from Suc.hyps show ?case sorry + from Suc.hyps show ?case \<proof> qed end @@ -456,29 +456,29 @@ have "P n" proof (induct n) case 0 - show "P 0" sorry + show "P 0" \<proof> next case (Suc n) - from \<open>P n\<close> show "P (Suc n)" sorry + from \<open>P n\<close> show "P (Suc n)" \<proof> qed have "A n \<Longrightarrow> P n" proof (induct n) case 0 - from \<open>A 0\<close> show "P 0" sorry + from \<open>A 0\<close> show "P 0" \<proof> next case (Suc n) from \<open>A n \<Longrightarrow> P n\<close> - and \<open>A (Suc n)\<close> show "P (Suc n)" sorry + and \<open>A (Suc n)\<close> show "P (Suc n)" \<proof> qed have "\<And>x. Q x n" proof (induct n) case 0 - show "Q x 0" sorry + show "Q x 0" \<proof> next case (Suc n) - from \<open>\<And>x. Q x n\<close> show "Q x (Suc n)" sorry + from \<open>\<And>x. Q x n\<close> show "Q x (Suc n)" \<proof> txt \<open>Local quantification admits arbitrary instances:\<close> note \<open>Q a n\<close> and \<open>Q b n\<close> qed @@ -502,11 +502,11 @@ then have "Q x n" proof (induct n arbitrary: x) case 0 - from \<open>A x 0\<close> show "Q x 0" sorry + from \<open>A x 0\<close> show "Q x 0" \<proof> next case (Suc n) from \<open>\<And>x. A x n \<Longrightarrow> Q x n\<close> \<comment> \<open>arbitrary instances can be produced here\<close> - and \<open>A x (Suc n)\<close> show "Q x (Suc n)" sorry + and \<open>A x (Suc n)\<close> show "Q x (Suc n)" \<proof> qed end @@ -532,13 +532,13 @@ case 0 note prem = \<open>A (a x)\<close> and defn = \<open>0 = a x\<close> - show "P (a x)" sorry + show "P (a x)" \<proof> next case (Suc n) note hyp = \<open>\<And>x. n = a x \<Longrightarrow> A (a x) \<Longrightarrow> P (a x)\<close> and prem = \<open>A (a x)\<close> and defn = \<open>Suc n = a x\<close> - show "P (a x)" sorry + show "P (a x)" \<proof> qed end @@ -628,7 +628,7 @@ begin { fix x - have "B x" sorry + have "B x" \<proof> } have "\<And>x. B x" by fact @@ -636,7 +636,7 @@ { assume A - have B sorry + have B \<proof> } have "A \<Longrightarrow> B" by fact @@ -644,15 +644,15 @@ { def x \<equiv> t - have "B x" sorry + have "B x" \<proof> } have "B t" by fact next { - obtain x :: 'a where "B x" sorry - have C sorry + obtain x :: 'a where "B x" \<proof> + have C \<proof> } have C by fact @@ -703,7 +703,7 @@ proof - fix x assume "A x" - show "B x" sorry + show "B x" \<proof> qed have "\<And>x. A x \<Longrightarrow> B x" @@ -711,7 +711,7 @@ { fix x assume "A x" - show "B x" sorry + show "B x" \<proof> } \<comment> "implicit block structure made explicit" note \<open>\<And>x. A x \<Longrightarrow> B x\<close> \<comment> "side exit for the resulting rule" @@ -730,36 +730,36 @@ begin assume r1: "A \<Longrightarrow> B \<Longrightarrow> C" \<comment> \<open>simple rule (Horn clause)\<close> - have A sorry \<comment> "prefix of facts via outer sub-proof" + have A \<proof> \<comment> "prefix of facts via outer sub-proof" then have C proof (rule r1) - show B sorry \<comment> "remaining rule premises via inner sub-proof" + show B \<proof> \<comment> "remaining rule premises via inner sub-proof" qed have C proof (rule r1) - show A sorry - show B sorry + show A \<proof> + show B \<proof> qed - have A and B sorry + have A and B \<proof> then have C proof (rule r1) qed - have A and B sorry + have A and B \<proof> then have C by (rule r1) next assume r2: "A \<Longrightarrow> (\<And>x. B1 x \<Longrightarrow> B2 x) \<Longrightarrow> C" \<comment> \<open>nested rule\<close> - have A sorry + have A \<proof> then have C proof (rule r2) fix x assume "B1 x" - show "B2 x" sorry + show "B2 x" \<proof> qed txt \<open>The compound rule premise @{prop "\<And>x. B1 x \<Longrightarrow> B2 x"} is better @@ -777,35 +777,35 @@ notepad begin - have "A \<longrightarrow> B" and A sorry + have "A \<longrightarrow> B" and A \<proof> then have B .. - have A sorry + have A \<proof> then have "A \<or> B" .. - have B sorry + have B \<proof> then have "A \<or> B" .. - have "A \<or> B" sorry + have "A \<or> B" \<proof> then have C proof assume A - then show C sorry + then show C \<proof> next assume B - then show C sorry + then show C \<proof> qed - have A and B sorry + have A and B \<proof> then have "A \<and> B" .. - have "A \<and> B" sorry + have "A \<and> B" \<proof> then have A .. - have "A \<and> B" sorry + have "A \<and> B" \<proof> then have B .. - have False sorry + have False \<proof> then have A .. have True .. @@ -813,36 +813,36 @@ have "\<not> A" proof assume A - then show False sorry + then show False \<proof> qed - have "\<not> A" and A sorry + have "\<not> A" and A \<proof> then have B .. have "\<forall>x. P x" proof fix x - show "P x" sorry + show "P x" \<proof> qed - have "\<forall>x. P x" sorry + have "\<forall>x. P x" \<proof> then have "P a" .. have "\<exists>x. P x" proof - show "P a" sorry + show "P a" \<proof> qed - have "\<exists>x. P x" sorry + have "\<exists>x. P x" \<proof> then have C proof fix a assume "P a" - show C sorry + show C \<proof> qed txt \<open>Less awkward version using @{command obtain}:\<close> - have "\<exists>x. P x" sorry + have "\<exists>x. P x" \<proof> then obtain a where "P a" .. end @@ -853,32 +853,32 @@ begin have "A \<and> B" proof \<comment> \<open>two strictly isolated subproofs\<close> - show A sorry + show A \<proof> next - show B sorry + show B \<proof> qed have "A \<and> B" proof \<comment> \<open>one simultaneous sub-proof\<close> - show A and B sorry + show A and B \<proof> qed have "A \<and> B" proof \<comment> \<open>two subproofs in the same context\<close> - show A sorry - show B sorry + show A \<proof> + show B \<proof> qed have "A \<and> B" proof \<comment> \<open>swapped order\<close> - show B sorry - show A sorry + show B \<proof> + show A \<proof> qed have "A \<and> B" proof \<comment> \<open>sequential subproofs\<close> - show A sorry - show B using \<open>A\<close> sorry + show A \<proof> + show B using \<open>A\<close> \<proof> qed end @@ -893,23 +893,23 @@ notepad begin - have "x \<in> A" and "x \<in> B" sorry + have "x \<in> A" and "x \<in> B" \<proof> then have "x \<in> A \<inter> B" .. - have "x \<in> A" sorry + have "x \<in> A" \<proof> then have "x \<in> A \<union> B" .. - have "x \<in> B" sorry + have "x \<in> B" \<proof> then have "x \<in> A \<union> B" .. - have "x \<in> A \<union> B" sorry + have "x \<in> A \<union> B" \<proof> then have C proof assume "x \<in> A" - then show C sorry + then show C \<proof> next assume "x \<in> B" - then show C sorry + then show C \<proof> qed next @@ -917,19 +917,19 @@ proof fix a assume "a \<in> A" - show "x \<in> a" sorry + show "x \<in> a" \<proof> qed - have "x \<in> \<Inter>A" sorry + have "x \<in> \<Inter>A" \<proof> then have "x \<in> a" proof - show "a \<in> A" sorry + show "a \<in> A" \<proof> qed - have "a \<in> A" and "x \<in> a" sorry + have "a \<in> A" and "x \<in> a" \<proof> then have "x \<in> \<Union>A" .. - have "x \<in> \<Union>A" sorry + have "x \<in> \<Union>A" \<proof> then obtain a where "a \<in> A" and "x \<in> a" .. end @@ -965,16 +965,16 @@ (\<And>x y. B2 x y \<Longrightarrow> C2 x y \<Longrightarrow> R) \<Longrightarrow> (* case 2 *) R (* main conclusion *)" - have A1 and A2 sorry + have A1 and A2 \<proof> then have R proof (rule r) fix x y assume "B1 x y" and "C1 x y" - show ?thesis sorry + show ?thesis \<proof> next fix x y assume "B2 x y" and "C2 x y" - show ?thesis sorry + show ?thesis \<proof> qed end @@ -1007,7 +1007,7 @@ obtains (case1) x y where "B1 x y" and "C1 x y" | (case2) x y where "B2 x y" and "C2 x y" - sorry + \<proof> subsubsection \<open>Example\<close> @@ -1024,10 +1024,10 @@ have C proof (cases "x = y" rule: tertium_non_datur) case T - from \<open>x = y\<close> show ?thesis sorry + from \<open>x = y\<close> show ?thesis \<proof> next case F - from \<open>x \<noteq> y\<close> show ?thesis sorry + from \<open>x \<noteq> y\<close> show ?thesis \<proof> qed end @@ -1047,10 +1047,10 @@ have C proof (cases x) case Foo - from \<open>x = Foo\<close> show ?thesis sorry + from \<open>x = Foo\<close> show ?thesis \<proof> next case (Bar a) - from \<open>x = Bar a\<close> show ?thesis sorry + from \<open>x = Bar a\<close> show ?thesis \<proof> qed end @@ -1065,13 +1065,13 @@ begin fix B :: "'a \<Rightarrow> bool" - obtain x where "B x" sorry + obtain x where "B x" \<proof> note \<open>B x\<close> txt \<open>Conclusions from this context may not mention @{term x} again!\<close> { - obtain x where "B x" sorry - from \<open>B x\<close> have C sorry + obtain x where "B x" \<proof> + from \<open>B x\<close> have C \<proof> } note \<open>C\<close> end

--- a/src/Doc/Isar_Ref/document/style.sty Sun Feb 07 19:33:42 2016 +0100 +++ b/src/Doc/Isar_Ref/document/style.sty Sun Feb 07 19:43:40 2016 +0100 @@ -16,7 +16,6 @@ %% Isar \newcommand{\isasymBBAR}{{\,\newdimen{\tmpheight}\settoheight\tmpheight{\isacharbar}\rule{1pt}{\tmpheight}\,}} -\isafoldtag{noproof}\def\isafoldnoproof{~\isafold{proof}} \renewcommand{\isacommand}[1]{\isakeyword{\isadigitreset#1}} \newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}}