# 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 \<Turnstile> 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<n. abs(f(i+1) - f i) <= #1) --> 
+  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.