# HG changeset patch # User nipkow # Date 971452928 -7200 # Node ID e61e7e1eacaf3bed04d8073f7c79a49320f915fa # Parent e928bdf62014555829696347523f323cce5356f0 *** empty log message *** diff -r e928bdf62014 -r e61e7e1eacaf doc-src/TutorialI/Advanced/advanced.tex --- a/doc-src/TutorialI/Advanced/advanced.tex Fri Oct 13 11:15:56 2000 +0200 +++ b/doc-src/TutorialI/Advanced/advanced.tex Fri Oct 13 18:02:08 2000 +0200 @@ -43,4 +43,5 @@ \label{sec:advanced-ind} \index{induction|(} \input{Misc/document/AdvancedInd.tex} +\input{CTL/document/CTLind.tex} \index{induction|)} diff -r e928bdf62014 -r e61e7e1eacaf doc-src/TutorialI/CTL/CTL.thy --- a/doc-src/TutorialI/CTL/CTL.thy Fri Oct 13 11:15:56 2000 +0200 +++ b/doc-src/TutorialI/CTL/CTL.thy Fri Oct 13 18:02:08 2000 +0200 @@ -364,9 +364,13 @@ done; text{* -The main theorem is proved as for PDL, except that we also derive the necessary equality -@{text"lfp(af A) = ..."} by combining @{thm[source]AF_lemma1} and @{thm[source]AF_lemma2} -on the spot: +If you found the above proofs somewhat complicated we recommend you read +\S\ref{sec:CTL-revisited} where we shown how inductive definitions lead to +simpler arguments. + +The main theorem is proved as for PDL, except that we also derive the +necessary equality @{text"lfp(af A) = ..."} by combining +@{thm[source]AF_lemma1} and @{thm[source]AF_lemma2} on the spot: *} theorem "mc f = {s. s \ f}"; diff -r e928bdf62014 -r e61e7e1eacaf doc-src/TutorialI/CTL/document/CTL.tex --- a/doc-src/TutorialI/CTL/document/CTL.tex Fri Oct 13 11:15:56 2000 +0200 +++ b/doc-src/TutorialI/CTL/document/CTL.tex Fri Oct 13 18:02:08 2000 +0200 @@ -5,6 +5,7 @@ \isamarkupsubsection{Computation tree logic---CTL} % \begin{isamarkuptext}% +\label{sec:CTL} The semantics of PDL only needs transitive reflexive closure. Let us now be a bit more adventurous and introduce a new temporal operator that goes beyond transitive reflexive closure. We extend the datatype @@ -265,9 +266,13 @@ \ \isacommand{apply}{\isacharparenleft}auto\ dest{\isacharcolon}not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharparenright}\isanewline \isacommand{done}% \begin{isamarkuptext}% -The main theorem is proved as for PDL, except that we also derive the necessary equality -\isa{lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isacharequal}\ {\isachardot}{\isachardot}{\isachardot}} by combining \isa{AF{\isacharunderscore}lemma{\isadigit{1}}} and \isa{AF{\isacharunderscore}lemma{\isadigit{2}}} -on the spot:% +If you found the above proofs somewhat complicated we recommend you read +\S\ref{sec:CTL-revisited} where we shown how inductive definitions lead to +simpler arguments. + +The main theorem is proved as for PDL, except that we also derive the +necessary equality \isa{lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isacharequal}\ {\isachardot}{\isachardot}{\isachardot}} by combining +\isa{AF{\isacharunderscore}lemma{\isadigit{1}}} and \isa{AF{\isacharunderscore}lemma{\isadigit{2}}} on the spot:% \end{isamarkuptext}% \isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline diff -r e928bdf62014 -r e61e7e1eacaf doc-src/TutorialI/Inductive/AB.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Inductive/AB.thy Fri Oct 13 18:02:08 2000 +0200 @@ -0,0 +1,121 @@ +theory AB = Main:; + +datatype alfa = a | b; + +lemma [simp]: "(x ~= a) = (x = b) & (x ~= b) = (x = a)"; +apply(case_tac x); +by(auto); + +consts S :: "alfa list set" + A :: "alfa list set" + B :: "alfa list set"; + +inductive S A B +intros +"[] : S" +"w : A ==> b#w : S" +"w : B ==> a#w : S" + +"w : S ==> a#w : A" +"[| v:A; w:A |] ==> b#v@w : A" + +"w : S ==> b#w : B" +"[| v:B; w:B |] ==> a#v@w : B"; + +thm S_A_B.induct[no_vars]; + +lemma "(w : S --> size[x:w. x=a] = size[x:w. x=b]) & + (w : A --> size[x:w. x=a] = size[x:w. x=b] + 1) & + (w : B --> size[x:w. x=b] = size[x:w. x=a] + 1)"; +apply(rule S_A_B.induct); +by(auto); + +lemma intermed_val[rule_format(no_asm)]: + "(!i + f 0 <= k & k <= f n --> (? i <= n. f i = (k::int))"; +apply(induct n); + apply(simp); + apply(arith); +apply(rule); +apply(erule impE); + apply(simp); +apply(rule); +apply(erule_tac x = n in allE); +apply(simp); +apply(case_tac "k = f(n+1)"); + apply(force); +apply(erule impE); + apply(simp add:zabs_def split:split_if_asm); + apply(arith); +by(blast intro:le_SucI); + +lemma step1: "ALL i < size w. + abs((int(size[x:take (i+1) w . P x]) - int(size[x:take (i+1) w . ~P x])) - + (int(size[x:take i w . P x]) - int(size[x:take i w . ~P x]))) <= #1"; +apply(induct w); + apply(simp); +apply(simp add:take_Cons split:nat.split); +apply(clarsimp); +apply(rule conjI); + apply(clarify); + apply(erule allE); + apply(erule impE); + apply(assumption); + apply(arith); +apply(clarify); +apply(erule allE); +apply(erule impE); + apply(assumption); +by(arith); + + +lemma part1: + "size[x:w. P x] = Suc(Suc(size[x:w. ~P x])) ==> + EX i<=size w. size[x:take i w. P x] = size[x:take i w. ~P x]+1"; +apply(insert intermed_val[OF step1, of "P" "w" "#1"]); +apply(simp); +apply(erule exE); +apply(rule_tac x=i in exI); +apply(simp); +apply(rule int_int_eq[THEN iffD1]); +apply(simp); +by(arith); + +lemma part2: +"[| size[x:take i xs @ drop i xs. P x] = size[x:take i xs @ drop i xs. ~P x]+2; + size[x:take i xs. P x] = size[x:take i xs. ~P x]+1 |] + ==> size[x:drop i xs. P x] = size[x:drop i xs. ~P x]+1"; +by(simp del:append_take_drop_id); + +lemmas [simp] = S_A_B.intros; + +lemma "(size[x:w. x=a] = size[x:w. x=b] --> w : S) & + (size[x:w. x=a] = size[x:w. x=b] + 1 --> w : A) & + (size[x:w. x=b] = size[x:w. x=a] + 1 --> w : B)"; +apply(induct_tac w rule: length_induct); +apply(case_tac "xs"); + apply(simp); +apply(simp); +apply(rule conjI); + apply(clarify); + apply(frule part1[of "%x. x=a", simplified]); + apply(erule exE); + apply(erule conjE); + apply(drule part2[of "%x. x=a", simplified]); + apply(assumption); + apply(rule_tac n1=i and t=list in subst[OF append_take_drop_id]); + apply(rule S_A_B.intros); + apply(force simp add:min_less_iff_disj); + apply(force split add: nat_diff_split); +apply(clarify); +apply(frule part1[of "%x. x=b", simplified]); +apply(erule exE); +apply(erule conjE); +apply(drule part2[of "%x. x=b", simplified]); + apply(assumption); +apply(rule_tac n1=i and t=list in subst[OF append_take_drop_id]); +apply(rule S_A_B.intros); + apply(force simp add:min_less_iff_disj); +by(force simp add:min_less_iff_disj split add: nat_diff_split); + +end; diff -r e928bdf62014 -r e61e7e1eacaf doc-src/TutorialI/Inductive/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Inductive/ROOT.ML Fri Oct 13 18:02:08 2000 +0200 @@ -0,0 +1,3 @@ +use "../settings.ML"; +use_thy "AB"; + diff -r e928bdf62014 -r e61e7e1eacaf doc-src/TutorialI/Inductive/document/AB.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Inductive/document/AB.tex Fri Oct 13 18:02:08 2000 +0200 @@ -0,0 +1,129 @@ +% +\begin{isabellebody}% +\def\isabellecontext{AB}% +\isacommand{theory}\ AB\ {\isacharequal}\ Main{\isacharcolon}\isanewline +\isanewline +\isacommand{datatype}\ alfa\ {\isacharequal}\ a\ {\isacharbar}\ b\isanewline +\isanewline +\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x\ {\isachartilde}{\isacharequal}\ a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ b{\isacharparenright}\ {\isacharampersand}\ {\isacharparenleft}x\ {\isachartilde}{\isacharequal}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ a{\isacharparenright}{\isachardoublequote}\isanewline +\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ x{\isacharparenright}\isanewline +\isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline +\isanewline +\isacommand{consts}\ S\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline +\ \ \ \ \ \ \ A\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline +\ \ \ \ \ \ \ B\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}alfa\ list\ set{\isachardoublequote}\isanewline +\isanewline +\isacommand{inductive}\ S\ A\ B\isanewline +\isakeyword{intros}\isanewline +{\isachardoublequote}{\isacharbrackleft}{\isacharbrackright}\ {\isacharcolon}\ S{\isachardoublequote}\isanewline +{\isachardoublequote}w\ {\isacharcolon}\ A\ {\isacharequal}{\isacharequal}{\isachargreater}\ b{\isacharhash}w\ {\isacharcolon}\ S{\isachardoublequote}\isanewline +{\isachardoublequote}w\ {\isacharcolon}\ B\ {\isacharequal}{\isacharequal}{\isachargreater}\ a{\isacharhash}w\ {\isacharcolon}\ S{\isachardoublequote}\isanewline +\isanewline +{\isachardoublequote}w\ {\isacharcolon}\ S\ {\isacharequal}{\isacharequal}{\isachargreater}\ a{\isacharhash}w\ {\isacharcolon}\ A{\isachardoublequote}\isanewline +{\isachardoublequote}{\isacharbrackleft}{\isacharbar}\ v{\isacharcolon}A{\isacharsemicolon}\ w{\isacharcolon}A\ {\isacharbar}{\isacharbrackright}\ {\isacharequal}{\isacharequal}{\isachargreater}\ b{\isacharhash}v{\isacharat}w\ {\isacharcolon}\ A{\isachardoublequote}\isanewline +\isanewline +{\isachardoublequote}w\ {\isacharcolon}\ S\ {\isacharequal}{\isacharequal}{\isachargreater}\ b{\isacharhash}w\ {\isacharcolon}\ B{\isachardoublequote}\isanewline +{\isachardoublequote}{\isacharbrackleft}{\isacharbar}\ v{\isacharcolon}B{\isacharsemicolon}\ w{\isacharcolon}B\ {\isacharbar}{\isacharbrackright}\ {\isacharequal}{\isacharequal}{\isachargreater}\ a{\isacharhash}v{\isacharat}w\ {\isacharcolon}\ B{\isachardoublequote}\isanewline +\isanewline +\isacommand{thm}\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}induct{\isacharbrackleft}no{\isacharunderscore}vars{\isacharbrackright}\isanewline +\isanewline +\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}w\ {\isacharcolon}\ S\ {\isacharminus}{\isacharminus}{\isachargreater}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}{\isacharparenright}\ {\isacharampersand}\isanewline +\ \ \ \ \ \ \ {\isacharparenleft}w\ {\isacharcolon}\ A\ {\isacharminus}{\isacharminus}{\isachargreater}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharampersand}\isanewline +\ \ \ \ \ \ \ {\isacharparenleft}w\ {\isacharcolon}\ B\ {\isacharminus}{\isacharminus}{\isachargreater}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline +\isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}induct{\isacharparenright}\isanewline +\isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline +\isanewline +\isacommand{lemma}\ intermed{\isacharunderscore}val{\isacharbrackleft}rule{\isacharunderscore}format{\isacharparenleft}no{\isacharunderscore}asm{\isacharparenright}{\isacharbrackright}{\isacharcolon}\isanewline +\ {\isachardoublequote}{\isacharparenleft}{\isacharbang}i{\isacharless}n{\isachardot}\ abs{\isacharparenleft}f{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isacharparenright}\ {\isacharless}{\isacharequal}\ {\isacharhash}{\isadigit{1}}{\isacharparenright}\ {\isacharminus}{\isacharminus}{\isachargreater}\ \isanewline +\ \ f\ {\isadigit{0}}\ {\isacharless}{\isacharequal}\ k\ {\isacharampersand}\ k\ {\isacharless}{\isacharequal}\ f\ n\ {\isacharminus}{\isacharminus}{\isachargreater}\ {\isacharparenleft}{\isacharquery}\ i\ {\isacharless}{\isacharequal}\ n{\isachardot}\ f\ i\ {\isacharequal}\ {\isacharparenleft}k{\isacharcolon}{\isacharcolon}int{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline +\isacommand{apply}{\isacharparenleft}induct\ n{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}rule{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}erule\ impE{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}rule{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ n\ \isakeyword{in}\ allE{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ {\isachardoublequote}k\ {\isacharequal}\ f{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}force{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}erule\ impE{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}zabs{\isacharunderscore}def\ split{\isacharcolon}split{\isacharunderscore}if{\isacharunderscore}asm{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline +\isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}le{\isacharunderscore}SucI{\isacharparenright}\isanewline +\isanewline +\isacommand{lemma}\ step{\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}ALL\ i\ {\isacharless}\ size\ w{\isachardot}\isanewline +\ \ abs{\isacharparenleft}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w\ {\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\ int{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w\ {\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharminus}\isanewline +\ \ \ \ \ \ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}take\ i\ w\ {\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\ int{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}take\ i\ w\ {\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharless}{\isacharequal}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}\isanewline +\isacommand{apply}{\isacharparenleft}induct\ w{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}take{\isacharunderscore}Cons\ split{\isacharcolon}nat{\isachardot}split{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}erule\ allE{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}erule\ impE{\isacharparenright}\isanewline +\ \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}erule\ allE{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}erule\ impE{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline +\isacommand{by}{\isacharparenleft}arith{\isacharparenright}\isanewline +\isanewline +\isanewline +\isacommand{lemma}\ part{\isadigit{1}}{\isacharcolon}\isanewline +\ {\isachardoublequote}size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ Suc{\isacharparenleft}Suc{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}{\isacharequal}{\isachargreater}\isanewline +\ \ EX\ i{\isacharless}{\isacharequal}size\ w{\isachardot}\ size{\isacharbrackleft}x{\isacharcolon}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}take\ i\ w{\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequote}\isanewline +\isacommand{apply}{\isacharparenleft}insert\ intermed{\isacharunderscore}val{\isacharbrackleft}OF\ step{\isadigit{1}}{\isacharcomma}\ of\ {\isachardoublequote}P{\isachardoublequote}\ {\isachardoublequote}w{\isachardoublequote}\ {\isachardoublequote}{\isacharhash}{\isadigit{1}}{\isachardoublequote}{\isacharbrackright}{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x{\isacharequal}i\ \isakeyword{in}\ exI{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}rule\ int{\isacharunderscore}int{\isacharunderscore}eq{\isacharbrackleft}THEN\ iffD{\isadigit{1}}{\isacharbrackright}{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline +\isacommand{by}{\isacharparenleft}arith{\isacharparenright}\isanewline +\isanewline +\isacommand{lemma}\ part{\isadigit{2}}{\isacharcolon}\isanewline +{\isachardoublequote}{\isacharbrackleft}{\isacharbar}\ size{\isacharbrackleft}x{\isacharcolon}take\ i\ xs\ {\isacharat}\ drop\ i\ xs{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}take\ i\ xs\ {\isacharat}\ drop\ i\ xs{\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{2}}{\isacharsemicolon}\isanewline +\ \ \ \ size{\isacharbrackleft}x{\isacharcolon}take\ i\ xs{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}take\ i\ xs{\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}\ {\isacharbar}{\isacharbrackright}\isanewline +\ {\isacharequal}{\isacharequal}{\isachargreater}\ size{\isacharbrackleft}x{\isacharcolon}drop\ i\ xs{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}drop\ i\ xs{\isachardot}\ {\isachartilde}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequote}\isanewline +\isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharparenright}\isanewline +\isanewline +\isacommand{lemmas}\ {\isacharbrackleft}simp{\isacharbrackright}\ {\isacharequal}\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros\isanewline +\isanewline +\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharminus}{\isacharminus}{\isachargreater}\ w\ {\isacharcolon}\ S{\isacharparenright}\ {\isacharampersand}\isanewline +\ \ \ \ \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}{\isacharminus}{\isachargreater}\ w\ {\isacharcolon}\ A{\isacharparenright}\ {\isacharampersand}\isanewline +\ \ \ \ \ \ \ {\isacharparenleft}size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}b{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isacharcolon}w{\isachardot}\ x{\isacharequal}a{\isacharbrackright}\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}{\isacharminus}{\isachargreater}\ w\ {\isacharcolon}\ B{\isacharparenright}{\isachardoublequote}\isanewline +\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ {\isachardoublequote}xs{\isachardoublequote}{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isacharpercent}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}erule\ conjE{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isacharpercent}x{\isachardot}\ x{\isacharequal}a{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline +\ \ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ n{\isadigit{1}}{\isacharequal}i\ \isakeyword{and}\ t{\isacharequal}list\ \isakeyword{in}\ subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isanewline +\ \ \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}force\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}clarify{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}frule\ part{\isadigit{1}}{\isacharbrackleft}of\ {\isachardoublequote}{\isacharpercent}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}erule\ exE{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}erule\ conjE{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}drule\ part{\isadigit{2}}{\isacharbrackleft}of\ {\isachardoublequote}{\isacharpercent}x{\isachardot}\ x{\isacharequal}b{\isachardoublequote}{\isacharcomma}\ simplified{\isacharbrackright}{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}assumption{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ n{\isadigit{1}}{\isacharequal}i\ \isakeyword{and}\ t{\isacharequal}list\ \isakeyword{in}\ subst{\isacharbrackleft}OF\ append{\isacharunderscore}take{\isacharunderscore}drop{\isacharunderscore}id{\isacharbrackright}{\isacharparenright}\isanewline +\isacommand{apply}{\isacharparenleft}rule\ S{\isacharunderscore}A{\isacharunderscore}B{\isachardot}intros{\isacharparenright}\isanewline +\ \isacommand{apply}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj{\isacharparenright}\isanewline +\isacommand{by}{\isacharparenleft}force\ simp\ add{\isacharcolon}min{\isacharunderscore}less{\isacharunderscore}iff{\isacharunderscore}disj\ split\ add{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharparenright}\isanewline +\isanewline +\isacommand{end}\isanewline +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: diff -r e928bdf62014 -r e61e7e1eacaf doc-src/TutorialI/IsaMakefile --- a/doc-src/TutorialI/IsaMakefile Fri Oct 13 11:15:56 2000 +0200 +++ b/doc-src/TutorialI/IsaMakefile Fri Oct 13 18:02:08 2000 +0200 @@ -4,7 +4,7 @@ ## targets -default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Advanced HOL-CTL HOL-Misc styles +default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Recdef HOL-Advanced HOL-CTL HOL-Inductive HOL-Misc styles images: test: all: default @@ -110,6 +110,14 @@ @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL CTL @rm -f tutorial.dvi +## HOL-Inductive + +HOL-Inductive: HOL $(LOG)/HOL-Inductive.gz + +$(LOG)/HOL-Inductive.gz: $(OUT)/HOL Inductive/AB.thy Inductive/ROOT.ML + @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Inductive + @rm -f tutorial.dvi + ## HOL-Misc HOL-Misc: HOL $(LOG)/HOL-Misc.gz @@ -126,4 +134,4 @@ ## clean clean: - @rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz $(LOG)/HOL-Advanced.gz $(LOG)/HOL-CTL.gz + @rm -f tutorial.dvi $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-CodeGen.gz $(LOG)/HOL-Misc.gz $(LOG)/HOL-ToyList.gz $(LOG)/HOL-ToyList2.gz $(LOG)/HOL-Trie.gz $(LOG)/HOL-Datatype.gz $(LOG)/HOL-Recdef.gz $(LOG)/HOL-Advanced.gz $(LOG)/HOL-CTL.gz $(LOG)/HOL-Inductive.gz diff -r e928bdf62014 -r e61e7e1eacaf doc-src/TutorialI/Misc/AdvancedInd.thy --- a/doc-src/TutorialI/Misc/AdvancedInd.thy Fri Oct 13 11:15:56 2000 +0200 +++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Fri Oct 13 18:02:08 2000 +0200 @@ -9,10 +9,9 @@ utilize and even derive new induction schemas. *}; -subsection{*Massaging the proposition\label{sec:ind-var-in-prems}*}; +subsection{*Massaging the proposition*}; -text{* -\noindent +text{*\label{sec:ind-var-in-prems} So far we have assumed that the theorem we want to prove is already in a form that is amenable to induction, but this is not always the case: *}; @@ -115,15 +114,25 @@ A second reason why your proposition may not be amenable to induction is that you want to induct on a whole term, rather than an individual variable. In -general, when inducting on some term $t$ you must rephrase the conclusion as -\[ \forall y@1 \dots y@n.~ x = t \longrightarrow C \] where $y@1 \dots y@n$ -are the free variables in $t$ and $x$ is new, and perform induction on $x$ -afterwards. An example appears below. +general, when inducting on some term $t$ you must rephrase the conclusion $C$ +as +\[ \forall y@1 \dots y@n.~ x = t \longrightarrow C \] +where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is new, and +perform induction on $x$ afterwards. An example appears in +\S\ref{sec:complete-ind} below. + +The very same problem may occur in connection with rule induction. Remember +that it requires a premise of the form $(x@1,\dots,x@k) \in R$, where $R$ is +some inductively defined set and the $x@i$ are variables. If instead we have +a premise $t \in R$, where $t$ is not just an $n$-tuple of variables, we +replace it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as +\[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C \] +For an example see \S\ref{sec:CTL-revisited} below. *}; subsection{*Beyond structural and recursion induction*}; -text{* +text{*\label{sec:complete-ind} So far, inductive proofs where by structural induction for primitive recursive functions and recursion induction for total recursive functions. But sometimes structural induction is awkward and there is no diff -r e928bdf62014 -r e61e7e1eacaf doc-src/TutorialI/Misc/document/AdvancedInd.tex --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Fri Oct 13 11:15:56 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Fri Oct 13 18:02:08 2000 +0200 @@ -10,10 +10,10 @@ utilize and even derive new induction schemas.% \end{isamarkuptext}% % -\isamarkupsubsection{Massaging the proposition\label{sec:ind-var-in-prems}} +\isamarkupsubsection{Massaging the proposition} % \begin{isamarkuptext}% -\noindent +\label{sec:ind-var-in-prems} So far we have assumed that the theorem we want to prove is already in a form that is amenable to induction, but this is not always the case:% \end{isamarkuptext}% @@ -101,15 +101,26 @@ A second reason why your proposition may not be amenable to induction is that you want to induct on a whole term, rather than an individual variable. In -general, when inducting on some term $t$ you must rephrase the conclusion as -\[ \forall y@1 \dots y@n.~ x = t \longrightarrow C \] where $y@1 \dots y@n$ -are the free variables in $t$ and $x$ is new, and perform induction on $x$ -afterwards. An example appears below.% +general, when inducting on some term $t$ you must rephrase the conclusion $C$ +as +\[ \forall y@1 \dots y@n.~ x = t \longrightarrow C \] +where $y@1 \dots y@n$ are the free variables in $t$ and $x$ is new, and +perform induction on $x$ afterwards. An example appears in +\S\ref{sec:complete-ind} below. + +The very same problem may occur in connection with rule induction. Remember +that it requires a premise of the form $(x@1,\dots,x@k) \in R$, where $R$ is +some inductively defined set and the $x@i$ are variables. If instead we have +a premise $t \in R$, where $t$ is not just an $n$-tuple of variables, we +replace it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as +\[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C \] +For an example see \S\ref{sec:CTL-revisited} below.% \end{isamarkuptext}% % \isamarkupsubsection{Beyond structural and recursion induction} % \begin{isamarkuptext}% +\label{sec:complete-ind} So far, inductive proofs where by structural induction for primitive recursive functions and recursion induction for total recursive functions. But sometimes structural induction is awkward and there is no diff -r e928bdf62014 -r e61e7e1eacaf doc-src/TutorialI/todo.tobias --- a/doc-src/TutorialI/todo.tobias Fri Oct 13 11:15:56 2000 +0200 +++ b/doc-src/TutorialI/todo.tobias Fri Oct 13 18:02:08 2000 +0200 @@ -48,7 +48,8 @@ an example of induction: !y. A --> B --> C ?? -Advanced Ind expects rulify, mp and spec. How much really? +Advanced Ind expects rule_format incl (no_asm) (which it currently explains! +Where explained? Appendix: Lexical: long ids. @@ -58,9 +59,6 @@ mention split_split in advanced pair section. -Advanced: -rule induction where premise not atomic (x1...xn) : R. - recdef with nested recursion: either an example or at least a pointer to the literature. In Recdef/termination.thy, at the end. %FIXME, with one exception: nested recursion.