1.1 --- a/doc-src/TutorialI/Advanced/document/simp.tex Thu Oct 19 21:25:15 2000 +0200
1.2 +++ b/doc-src/TutorialI/Advanced/document/simp.tex Fri Oct 20 08:46:41 2000 +0200
1.3 @@ -97,10 +97,10 @@
1.4 simplifier recognizes their special status automatically.
1.5
1.6 Permutative rewrite rules are most effective in the case of
1.7 -associative-commutative operators. (Associativity by itself is not
1.8 -permutative.) When dealing with an AC-operator~$f$, keep the
1.9 +associative-commutative functions. (Associativity by itself is not
1.10 +permutative.) When dealing with an AC-function~$f$, keep the
1.11 following points in mind:
1.12 -\begin{itemize}\index{associative-commutative operators}
1.13 +\begin{itemize}\index{associative-commutative function}
1.14
1.15 \item The associative law must always be oriented from left to right,
1.16 namely $f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if
2.1 --- a/doc-src/TutorialI/Advanced/simp.thy Thu Oct 19 21:25:15 2000 +0200
2.2 +++ b/doc-src/TutorialI/Advanced/simp.thy Fri Oct 20 08:46:41 2000 +0200
2.3 @@ -86,10 +86,10 @@
2.4 simplifier recognizes their special status automatically.
2.5
2.6 Permutative rewrite rules are most effective in the case of
2.7 -associative-commutative operators. (Associativity by itself is not
2.8 -permutative.) When dealing with an AC-operator~$f$, keep the
2.9 +associative-commutative functions. (Associativity by itself is not
2.10 +permutative.) When dealing with an AC-function~$f$, keep the
2.11 following points in mind:
2.12 -\begin{itemize}\index{associative-commutative operators}
2.13 +\begin{itemize}\index{associative-commutative function}
2.14
2.15 \item The associative law must always be oriented from left to right,
2.16 namely $f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if
3.1 --- a/doc-src/TutorialI/CTL/Base.thy Thu Oct 19 21:25:15 2000 +0200
3.2 +++ b/doc-src/TutorialI/CTL/Base.thy Fri Oct 20 08:46:41 2000 +0200
3.3 @@ -1,6 +1,6 @@
3.4 (*<*)theory Base = Main:(*>*)
3.5
3.6 -section{*Case study: Verified model checkers*}
3.7 +section{*Case study: Verified model checking*}
3.8
3.9 text{*
3.10 Model checking is a very popular technique for the verification of finite
3.11 @@ -50,18 +50,20 @@
3.12 which is false.
3.13
3.14 Abstracting from this concrete example, we assume there is some type of
3.15 -states
3.16 +states:
3.17 *}
3.18
3.19 typedecl state
3.20
3.21 text{*\noindent
3.22 -which we merely declare rather than define because it is an implicit
3.23 -parameter of our model. Of course it would have been more generic to make
3.24 -@{typ state} a type parameter of everything but fixing @{typ state} as above
3.25 -reduces clutter.
3.26 -Similarly we declare an arbitrary but fixed transition system, i.e.\
3.27 -relation between states:
3.28 +Command \isacommand{typedecl} merely declares a new type but without
3.29 +defining it (see also \S\ref{sec:typedecl}). Thus we know nothing
3.30 +about the type other than its existence. That is exactly what we need
3.31 +because @{typ state} really is an implicit parameter of our model. Of
3.32 +course it would have been more generic to make @{typ state} a type
3.33 +parameter of everything but declaring @{typ state} globally as above
3.34 +reduces clutter. Similarly we declare an arbitrary but fixed
3.35 +transition system, i.e.\ relation between states:
3.36 *}
3.37
3.38 consts M :: "(state \<times> state)set";
4.1 --- a/doc-src/TutorialI/CTL/CTL.thy Thu Oct 19 21:25:15 2000 +0200
4.2 +++ b/doc-src/TutorialI/CTL/CTL.thy Fri Oct 20 08:46:41 2000 +0200
4.3 @@ -87,7 +87,7 @@
4.4 apply(erule lfp_induct);
4.5 apply(rule mono_ef);
4.6 apply(simp);
4.7 - apply(blast intro: r_into_rtrancl rtrancl_trans);
4.8 + apply(blast intro: rtrancl_trans);
4.9 apply(rule subsetI);
4.10 apply(simp, clarify);
4.11 apply(erule converse_rtrancl_induct);
4.12 @@ -112,10 +112,9 @@
4.13 @{thm[source]lfp_lowerbound}:
4.14 @{thm[display]lfp_lowerbound[of _ "S",no_vars]}
4.15 The instance of the premise @{prop"f S \<subseteq> S"} is proved pointwise,
4.16 -starting with simplification and clarification:
4.17 +a decision that clarification takes for us:
4.18 *};
4.19 apply(rule lfp_lowerbound);
4.20 -apply(rule subsetI);
4.21 apply(clarsimp simp add: af_def Paths_def);
4.22 (*ML"Pretty.setmargin 70";
4.23 pr(latex xsymbols symbols);*)
4.24 @@ -380,24 +379,116 @@
4.25 done
4.26
4.27 text{*
4.28 +
4.29 The above language is not quite CTL. The latter also includes an
4.30 -until-operator, which is the subject of the following exercise.
4.31 -It is not definable in terms of the other operators!
4.32 +until-operator @{term"EU f g"} with semantics ``there exist a path
4.33 +where @{term f} is true until @{term g} becomes true''. With the help
4.34 +of an auxiliary function
4.35 +*}
4.36 +
4.37 +consts until:: "state set \<Rightarrow> state set \<Rightarrow> state \<Rightarrow> state list \<Rightarrow> bool"
4.38 +primrec
4.39 +"until A B s [] = (s \<in> B)"
4.40 +"until A B s (t#p) = (s \<in> A \<and> (s,t) \<in> M \<and> until A B t p)"
4.41 +(*<*)constdefs
4.42 + eusem :: "state set \<Rightarrow> state set \<Rightarrow> state set"
4.43 +"eusem A B \<equiv> {s. \<exists>p. until A B s p}"(*>*)
4.44 +
4.45 +text{*\noindent
4.46 +the semantics of @{term EU} is straightforward:
4.47 +@{text[display]"s \<Turnstile> EU f g = (\<exists>p. until A B s p)"}
4.48 +Note that @{term EU} is not definable in terms of the other operators!
4.49 +
4.50 +Model checking @{term EU} is again a least fixed point construction:
4.51 +@{text[display]"mc(EU f g) = lfp(\<lambda>T. mc g \<union> mc f \<inter> (M^-1 ^^ T))"}
4.52 +
4.53 \begin{exercise}
4.54 -Extend the datatype of formulae by the binary until operator @{term"EU f g"} with semantics
4.55 -``there exist a path where @{term f} is true until @{term g} becomes true''
4.56 -@{text[display]"s \<Turnstile> EU f g = (\<exists>p\<in>Paths s. \<exists>j. p j \<Turnstile> g \<and> (\<exists>i < j. p i \<Turnstile> f))"}
4.57 -and model checking algorithm
4.58 -@{text[display]"mc(EU f g) = lfp(\<lambda>T. mc g \<union> mc f \<inter> (M^-1 ^^ T))"}
4.59 -Prove the equivalence between semantics and model checking, i.e.\ that
4.60 +Extend the datatype of formulae by the above until operator
4.61 +and prove the equivalence between semantics and model checking, i.e.\ that
4.62 @{prop[display]"mc(EU f g) = {s. s \<Turnstile> EU f g}"}
4.63 %For readability you may want to annotate {term EU} with its customary syntax
4.64 %{text[display]"| EU formula formula E[_ U _]"}
4.65 %which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}.
4.66 \end{exercise}
4.67 -For more CTL exercises see, for example \cite{Huth-Ryan-book}.
4.68 -\bigskip
4.69 +For more CTL exercises see, for example, \cite{Huth-Ryan-book}.
4.70 +*}
4.71
4.72 +(*<*)
4.73 +constdefs
4.74 + eufix :: "state set \<Rightarrow> state set \<Rightarrow> state set \<Rightarrow> state set"
4.75 +"eufix A B T \<equiv> B \<union> A \<inter> (M^-1 ^^ T)"
4.76 +
4.77 +lemma "lfp(eufix A B) \<subseteq> eusem A B"
4.78 +apply(rule lfp_lowerbound)
4.79 +apply(clarsimp simp add:eusem_def eufix_def);
4.80 +apply(erule disjE);
4.81 + apply(rule_tac x = "[]" in exI);
4.82 + apply simp
4.83 +apply(clarsimp);
4.84 +apply(rule_tac x = "y#xc" in exI);
4.85 +apply simp;
4.86 +done
4.87 +
4.88 +lemma mono_eufix: "mono(eufix A B)";
4.89 +apply(simp add: mono_def eufix_def);
4.90 +apply blast;
4.91 +done
4.92 +
4.93 +lemma "eusem A B \<subseteq> lfp(eufix A B)";
4.94 +apply(clarsimp simp add:eusem_def);
4.95 +apply(erule rev_mp);
4.96 +apply(rule_tac x = x in spec);
4.97 +apply(induct_tac p);
4.98 + apply(rule ssubst[OF lfp_unfold[OF mono_eufix]]);
4.99 + apply(simp add:eufix_def);
4.100 +apply(clarsimp);
4.101 +apply(rule ssubst[OF lfp_unfold[OF mono_eufix]]);
4.102 +apply(simp add:eufix_def);
4.103 +apply blast;
4.104 +done
4.105 +
4.106 +(*
4.107 +constdefs
4.108 + eusem :: "state set \<Rightarrow> state set \<Rightarrow> state set"
4.109 +"eusem A B \<equiv> {s. \<exists>p\<in>Paths s. \<exists>j. p j \<in> B \<and> (\<forall>i < j. p i \<in> A)}"
4.110 +
4.111 +axioms
4.112 +M_total: "\<exists>t. (s,t) \<in> M"
4.113 +
4.114 +consts apath :: "state \<Rightarrow> (nat \<Rightarrow> state)"
4.115 +primrec
4.116 +"apath s 0 = s"
4.117 +"apath s (Suc i) = (SOME t. (apath s i,t) \<in> M)"
4.118 +
4.119 +lemma [iff]: "apath s \<in> Paths s";
4.120 +apply(simp add:Paths_def);
4.121 +apply(blast intro: M_total[THEN someI_ex])
4.122 +done
4.123 +
4.124 +constdefs
4.125 + pcons :: "state \<Rightarrow> (nat \<Rightarrow> state) \<Rightarrow> (nat \<Rightarrow> state)"
4.126 +"pcons s p == \<lambda>i. case i of 0 \<Rightarrow> s | Suc j \<Rightarrow> p j"
4.127 +
4.128 +lemma pcons_PathI: "[| (s,t) : M; p \<in> Paths t |] ==> pcons s p \<in> Paths s";
4.129 +by(simp add:Paths_def pcons_def split:nat.split);
4.130 +
4.131 +lemma "lfp(eufix A B) \<subseteq> eusem A B"
4.132 +apply(rule lfp_lowerbound)
4.133 +apply(clarsimp simp add:eusem_def eufix_def);
4.134 +apply(erule disjE);
4.135 + apply(rule_tac x = "apath x" in bexI);
4.136 + apply(rule_tac x = 0 in exI);
4.137 + apply simp;
4.138 + apply simp;
4.139 +apply(clarify);
4.140 +apply(rule_tac x = "pcons xb p" in bexI);
4.141 + apply(rule_tac x = "j+1" in exI);
4.142 + apply (simp add:pcons_def split:nat.split);
4.143 +apply (simp add:pcons_PathI)
4.144 +done
4.145 +*)
4.146 +(*>*)
4.147 +text{*
4.148 Let us close this section with a few words about the executability of our model checkers.
4.149 It is clear that if all sets are finite, they can be represented as lists and the usual
4.150 set operations are easily implemented. Only @{term lfp} requires a little thought.
5.1 --- a/doc-src/TutorialI/CTL/CTLind.thy Thu Oct 19 21:25:15 2000 +0200
5.2 +++ b/doc-src/TutorialI/CTL/CTLind.thy Fri Oct 20 08:46:41 2000 +0200
5.3 @@ -3,12 +3,15 @@
5.4 subsection{*CTL revisited*}
5.5
5.6 text{*\label{sec:CTL-revisited}
5.7 +The purpose of this section is twofold: we want to demonstrate
5.8 +some of the induction principles and heuristics discussed above and we want to
5.9 +show how inductive definitions can simplify proofs.
5.10 In \S\ref{sec:CTL} we gave a fairly involved proof of the correctness of a
5.11 model checker for CTL. In particular the proof of the
5.12 @{thm[source]infinity_lemma} on the way to @{thm[source]AF_lemma2} is not as
5.13 simple as one might intuitively expect, due to the @{text SOME} operator
5.14 -involved. The purpose of this section is to show how an inductive definition
5.15 -can help to simplify the proof of @{thm[source]AF_lemma2}.
5.16 +involved. Below we give a simpler proof of @{thm[source]AF_lemma2}
5.17 +based on an auxiliary inductive definition.
5.18
5.19 Let us call a (finite or infinite) path \emph{@{term A}-avoiding} if it does
5.20 not touch any node in the set @{term A}. Then @{thm[source]AF_lemma2} says
6.1 --- a/doc-src/TutorialI/CTL/document/Base.tex Thu Oct 19 21:25:15 2000 +0200
6.2 +++ b/doc-src/TutorialI/CTL/document/Base.tex Fri Oct 20 08:46:41 2000 +0200
6.3 @@ -2,7 +2,7 @@
6.4 \begin{isabellebody}%
6.5 \def\isabellecontext{Base}%
6.6 %
6.7 -\isamarkupsection{Case study: Verified model checkers}
6.8 +\isamarkupsection{Case study: Verified model checking}
6.9 %
6.10 \begin{isamarkuptext}%
6.11 Model checking is a very popular technique for the verification of finite
6.12 @@ -52,17 +52,19 @@
6.13 which is false.
6.14
6.15 Abstracting from this concrete example, we assume there is some type of
6.16 -states%
6.17 +states:%
6.18 \end{isamarkuptext}%
6.19 \isacommand{typedecl}\ state%
6.20 \begin{isamarkuptext}%
6.21 \noindent
6.22 -which we merely declare rather than define because it is an implicit
6.23 -parameter of our model. Of course it would have been more generic to make
6.24 -\isa{state} a type parameter of everything but fixing \isa{state} as above
6.25 -reduces clutter.
6.26 -Similarly we declare an arbitrary but fixed transition system, i.e.\
6.27 -relation between states:%
6.28 +Command \isacommand{typedecl} merely declares a new type but without
6.29 +defining it (see also \S\ref{sec:typedecl}). Thus we know nothing
6.30 +about the type other than its existence. That is exactly what we need
6.31 +because \isa{state} really is an implicit parameter of our model. Of
6.32 +course it would have been more generic to make \isa{state} a type
6.33 +parameter of everything but declaring \isa{state} globally as above
6.34 +reduces clutter. Similarly we declare an arbitrary but fixed
6.35 +transition system, i.e.\ relation between states:%
6.36 \end{isamarkuptext}%
6.37 \isacommand{consts}\ M\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}state\ {\isasymtimes}\ state{\isacharparenright}set{\isachardoublequote}%
6.38 \begin{isamarkuptext}%
7.1 --- a/doc-src/TutorialI/CTL/document/CTL.tex Thu Oct 19 21:25:15 2000 +0200
7.2 +++ b/doc-src/TutorialI/CTL/document/CTL.tex Fri Oct 20 08:46:41 2000 +0200
7.3 @@ -66,10 +66,9 @@
7.4 \ \ \ \ \ f\ S\ {\isasymsubseteq}\ S\ {\isasymLongrightarrow}\ lfp\ f\ {\isasymsubseteq}\ S%
7.5 \end{isabelle}
7.6 The instance of the premise \isa{f\ S\ {\isasymsubseteq}\ S} is proved pointwise,
7.7 -starting with simplification and clarification:%
7.8 +a decision that clarification takes for us:%
7.9 \end{isamarkuptxt}%
7.10 \isacommand{apply}{\isacharparenleft}rule\ lfp{\isacharunderscore}lowerbound{\isacharparenright}\isanewline
7.11 -\isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
7.12 \isacommand{apply}{\isacharparenleft}clarsimp\ simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}%
7.13 \begin{isamarkuptxt}%
7.14 \begin{isabelle}
7.15 @@ -282,19 +281,30 @@
7.16 \isacommand{done}%
7.17 \begin{isamarkuptext}%
7.18 The above language is not quite CTL. The latter also includes an
7.19 -until-operator, which is the subject of the following exercise.
7.20 -It is not definable in terms of the other operators!
7.21 -\begin{exercise}
7.22 -Extend the datatype of formulae by the binary until operator \isa{EU\ f\ g} with semantics
7.23 -``there exist a path where \isa{f} is true until \isa{g} becomes true''
7.24 +until-operator \isa{EU\ f\ g} with semantics ``there exist a path
7.25 +where \isa{f} is true until \isa{g} becomes true''. With the help
7.26 +of an auxiliary function%
7.27 +\end{isamarkuptext}%
7.28 +\isacommand{consts}\ until{\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ set\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ {\isasymRightarrow}\ state\ list\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
7.29 +\isacommand{primrec}\isanewline
7.30 +{\isachardoublequote}until\ A\ B\ s\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ {\isacharequal}\ {\isacharparenleft}s\ {\isasymin}\ B{\isacharparenright}{\isachardoublequote}\isanewline
7.31 +{\isachardoublequote}until\ A\ B\ s\ {\isacharparenleft}t{\isacharhash}p{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}s\ {\isasymin}\ A\ {\isasymand}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ until\ A\ B\ t\ p{\isacharparenright}{\isachardoublequote}%
7.32 +\begin{isamarkuptext}%
7.33 +\noindent
7.34 +the semantics of \isa{EU} is straightforward:
7.35 \begin{isabelle}%
7.36 -\ \ \ \ \ s\ {\isasymTurnstile}\ EU\ f\ g\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymexists}j{\isachardot}\ p\ j\ {\isasymTurnstile}\ g\ {\isasymand}\ {\isacharparenleft}{\isasymexists}i\ {\isacharless}\ j{\isachardot}\ p\ i\ {\isasymTurnstile}\ f{\isacharparenright}{\isacharparenright}%
7.37 +\ \ \ \ \ s\ {\isasymTurnstile}\ EU\ f\ g\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ until\ A\ B\ s\ p{\isacharparenright}%
7.38 \end{isabelle}
7.39 -and model checking algorithm
7.40 +Note that \isa{EU} is not definable in terms of the other operators!
7.41 +
7.42 +Model checking \isa{EU} is again a least fixed point construction:
7.43 \begin{isabelle}%
7.44 \ \ \ \ \ mc{\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ g\ {\isasymunion}\ mc\ f\ {\isasyminter}\ {\isacharparenleft}M{\isacharcircum}{\isacharminus}{\isadigit{1}}\ {\isacharcircum}{\isacharcircum}\ T{\isacharparenright}{\isacharparenright}%
7.45 \end{isabelle}
7.46 -Prove the equivalence between semantics and model checking, i.e.\ that
7.47 +
7.48 +\begin{exercise}
7.49 +Extend the datatype of formulae by the above until operator
7.50 +and prove the equivalence between semantics and model checking, i.e.\ that
7.51 \begin{isabelle}%
7.52 \ \ \ \ \ mc\ {\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ EU\ f\ g{\isacharbraceright}%
7.53 \end{isabelle}
7.54 @@ -302,9 +312,10 @@
7.55 %{text[display]"| EU formula formula E[_ U _]"}
7.56 %which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}.
7.57 \end{exercise}
7.58 -For more CTL exercises see, for example \cite{Huth-Ryan-book}.
7.59 -\bigskip
7.60 -
7.61 +For more CTL exercises see, for example, \cite{Huth-Ryan-book}.%
7.62 +\end{isamarkuptext}%
7.63 +%
7.64 +\begin{isamarkuptext}%
7.65 Let us close this section with a few words about the executability of our model checkers.
7.66 It is clear that if all sets are finite, they can be represented as lists and the usual
7.67 set operations are easily implemented. Only \isa{lfp} requires a little thought.
8.1 --- a/doc-src/TutorialI/Misc/AdvancedInd.thy Thu Oct 19 21:25:15 2000 +0200
8.2 +++ b/doc-src/TutorialI/Misc/AdvancedInd.thy Fri Oct 20 08:46:41 2000 +0200
8.3 @@ -6,7 +6,8 @@
8.4 Now that we have learned about rules and logic, we take another look at the
8.5 finer points of induction. The two questions we answer are: what to do if the
8.6 proposition to be proved is not directly amenable to induction, and how to
8.7 -utilize and even derive new induction schemas.
8.8 +utilize and even derive new induction schemas. We conclude with some slightly subtle
8.9 +examples of induction.
8.10 *};
8.11
8.12 subsection{*Massaging the proposition*};
8.13 @@ -82,7 +83,7 @@
8.14 Here is a simple example (which is proved by @{text"blast"}):
8.15 *};
8.16
8.17 -lemma simple: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y & A y";
8.18 +lemma simple: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y \<and> A y";
8.19 (*<*)by blast;(*>*)
8.20
8.21 text{*\noindent
8.22 @@ -105,7 +106,7 @@
8.23 statement of your original lemma, thus avoiding the intermediate step:
8.24 *};
8.25
8.26 -lemma myrule[rule_format]: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y & A y";
8.27 +lemma myrule[rule_format]: "\<forall>y. A y \<longrightarrow> B y \<longrightarrow> B y \<and> A y";
8.28 (*<*)
8.29 by blast;
8.30 (*>*)
8.31 @@ -129,6 +130,9 @@
8.32 replace it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as
8.33 \[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C \]
8.34 For an example see \S\ref{sec:CTL-revisited} below.
8.35 +
8.36 +Of course, all premises that share free variables with $t$ need to be pulled into
8.37 +the conclusion as well, under the @{text"\<forall>"}, again using @{text"\<longrightarrow>"} as shown above.
8.38 *};
8.39
8.40 subsection{*Beyond structural and recursion induction*};
8.41 @@ -149,7 +153,7 @@
8.42 Here is an example of its application.
8.43 *};
8.44
8.45 -consts f :: "nat => nat";
8.46 +consts f :: "nat \<Rightarrow> nat";
8.47 axioms f_ax: "f(f(n)) < f(Suc(n))";
8.48
8.49 text{*\noindent
8.50 @@ -289,7 +293,6 @@
8.51 by(insert induct_lem, blast);
8.52
8.53 text{*
8.54 -
8.55 Finally we should mention that HOL already provides the mother of all
8.56 inductions, \textbf{well-founded
8.57 induction}\indexbold{induction!well-founded}\index{well-founded
9.1 --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Thu Oct 19 21:25:15 2000 +0200
9.2 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Fri Oct 20 08:46:41 2000 +0200
9.3 @@ -7,7 +7,8 @@
9.4 Now that we have learned about rules and logic, we take another look at the
9.5 finer points of induction. The two questions we answer are: what to do if the
9.6 proposition to be proved is not directly amenable to induction, and how to
9.7 -utilize and even derive new induction schemas.%
9.8 +utilize and even derive new induction schemas. We conclude with some slightly subtle
9.9 +examples of induction.%
9.10 \end{isamarkuptext}%
9.11 %
9.12 \isamarkupsubsection{Massaging the proposition}
9.13 @@ -77,7 +78,7 @@
9.14 which can yield a fairly complex conclusion.
9.15 Here is a simple example (which is proved by \isa{blast}):%
9.16 \end{isamarkuptext}%
9.17 -\isacommand{lemma}\ simple{\isacharcolon}\ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isacharampersand}\ A\ y{\isachardoublequote}%
9.18 +\isacommand{lemma}\ simple{\isacharcolon}\ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymand}\ A\ y{\isachardoublequote}%
9.19 \begin{isamarkuptext}%
9.20 \noindent
9.21 You can get the desired lemma by explicit
9.22 @@ -96,7 +97,7 @@
9.23 You can go one step further and include these derivations already in the
9.24 statement of your original lemma, thus avoiding the intermediate step:%
9.25 \end{isamarkuptext}%
9.26 -\isacommand{lemma}\ myrule{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isacharampersand}\ A\ y{\isachardoublequote}%
9.27 +\isacommand{lemma}\ myrule{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymlongrightarrow}\ B\ y\ {\isasymand}\ A\ y{\isachardoublequote}%
9.28 \begin{isamarkuptext}%
9.29 \bigskip
9.30
9.31 @@ -115,7 +116,10 @@
9.32 a premise $t \in R$, where $t$ is not just an $n$-tuple of variables, we
9.33 replace it with $(x@1,\dots,x@k) \in R$, and rephrase the conclusion $C$ as
9.34 \[ \forall y@1 \dots y@n.~ (x@1,\dots,x@k) = t \longrightarrow C \]
9.35 -For an example see \S\ref{sec:CTL-revisited} below.%
9.36 +For an example see \S\ref{sec:CTL-revisited} below.
9.37 +
9.38 +Of course, all premises that share free variables with $t$ need to be pulled into
9.39 +the conclusion as well, under the \isa{{\isasymforall}}, again using \isa{{\isasymlongrightarrow}} as shown above.%
9.40 \end{isamarkuptext}%
9.41 %
9.42 \isamarkupsubsection{Beyond structural and recursion induction}
9.43 @@ -138,7 +142,7 @@
9.44 \end{isabelle}
9.45 Here is an example of its application.%
9.46 \end{isamarkuptext}%
9.47 -\isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isacharequal}{\isachargreater}\ nat{\isachardoublequote}\isanewline
9.48 +\isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
9.49 \isacommand{axioms}\ f{\isacharunderscore}ax{\isacharcolon}\ {\isachardoublequote}f{\isacharparenleft}f{\isacharparenleft}n{\isacharparenright}{\isacharparenright}\ {\isacharless}\ f{\isacharparenleft}Suc{\isacharparenleft}n{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
9.50 \begin{isamarkuptext}%
9.51 \noindent
10.1 --- a/doc-src/TutorialI/todo.tobias Thu Oct 19 21:25:15 2000 +0200
10.2 +++ b/doc-src/TutorialI/todo.tobias Fri Oct 20 08:46:41 2000 +0200
10.3 @@ -1,27 +1,21 @@
10.4 -General questions
10.5 -=================
10.6 -
10.7 -Here is an initial list:
10.8 -clarify, clarsimp, hyp_subst_tac, rename_tac, rotate_tac, split
10.9 -single step tactics: (e/d/f)rule, insert
10.10 -with instantiation: (e/d/f)rule_tac, insert_tac
10.11 +Implementation
10.12 +==============
10.13
10.14 Hide global names like Node.
10.15 Why is comp needed in addition to op O?
10.16 Explain in syntax section!
10.17
10.18 -Implementation
10.19 -==============
10.20 +defs with = and pattern matching
10.21
10.22 -swap in classical.ML has ugly name Pa in it. Rename.
10.23 +replace "simp only split" by "split_tac".
10.24
10.25 -Induction rules for int: int_le/ge_induct?
10.26 -Needed for ifak example. But is that example worth it?
10.27 +arithmetic: allow mixed nat/int formulae
10.28 +-> simplify proof of part1 in Inductive/AB.thy
10.29
10.30 Add map_cong?? (upto 10% slower)
10.31 -But we should install UN_cong and INT_cong too.
10.32
10.33 -defs with = and pattern matching
10.34 +Recdef: Get rid of function name in header.
10.35 +Support mutual recursion (Konrad?)
10.36
10.37 use arith_tac in recdef to solve termination conditions?
10.38 -> new example in Recdef/termination
10.39 @@ -34,15 +28,18 @@
10.40
10.41 it would be nice if one could get id to the enclosing quotes in the [source] option.
10.42
10.43 -arithmetic: allow mixed nat/int formulae
10.44 --> simplify proof of part1 in Inductive/AB.thy
10.45 +More predefined functions for datatypes: map?
10.46 +
10.47 +Induction rules for int: int_le/ge_induct?
10.48 +Needed for ifak example. But is that example worth it?
10.49 +
10.50
10.51 Minor fixes in the tutorial
10.52 ===========================
10.53
10.54 -replace simp only split by split_tac.
10.55 +explanation of absence of contrapos_pn in Rules?
10.56
10.57 -get rid of use_thy?
10.58 +get rid of use_thy in tutorial?
10.59
10.60 Explain typographic conventions?
10.61
10.62 @@ -62,27 +59,19 @@
10.63
10.64 Syntax section: syntax annotations nor just for consts but also for constdefs and datatype.
10.65
10.66 -Prove EU exercise in CTL.
10.67 -
10.68
10.69 Minor additions to the tutorial, unclear where
10.70 ==============================================
10.71
10.72 Tacticals: , ? +
10.73
10.74 -"typedecl" is used in CTL/Base, but where is it introduced?
10.75 -In More Types chapter? Rephrase the CTL bit accordingly.
10.76 -
10.77 -print_simpset (-> print_simps?)
10.78 -(Another subsection Useful theorems, methods, and commands?)
10.79 -
10.80 Mention that simp etc (big step tactics) insist on change?
10.81
10.82 Rules: Introduce "by" (as a kind of shorthand for apply+done, except that it
10.83 does more.)
10.84
10.85 A list of further useful commands (rules? tricks?)
10.86 -prefer, defer
10.87 +prefer, defer, print_simpset (-> print_simps?)
10.88
10.89 An overview of the automatic methods: simp, auto, fast, blast, force,
10.90 clarify, clarsimp (intro, elim?)
10.91 @@ -134,12 +123,8 @@
10.92
10.93 Sets via ordered list of intervals. (Isa/Interval(2))
10.94
10.95 -Sets: PDL and CTL
10.96 -
10.97 -Ind. defs: Grammar (for same number of as and bs),
10.98 propositional logic (soundness and completeness?),
10.99 predicate logic (soundness?),
10.100 -CTL proof.
10.101
10.102 Tautology checker. Based on Ifexpr or prop.logic?
10.103 Include forward reference in relevant section.
10.104 @@ -159,33 +144,18 @@
10.105 Additional topics
10.106 =================
10.107
10.108 -Beef up recdef (see below).
10.109 -Nested recursion? Mutual recursion?
10.110 -
10.111 -Nested inductive datatypes: better recursion and induction
10.112 -(see below)
10.113 +Recdef with nested recursion?
10.114
10.115 Extensionality: applications in
10.116 - boolean expressions: valif o bool2if = value
10.117 - Advanced datatypes exercise subst (f o g) = subst f o subst g
10.118
10.119 A look at the library?
10.120 -Functions. Relations. Lfp/Gfp. Map.
10.121 +Map.
10.122 If WF is discussed, make a link to it from AdvancedInd.
10.123
10.124 Prototyping?
10.125
10.126 -
10.127 -Isabelle
10.128 -========
10.129 -
10.130 -Get rid of function name in recdef header
10.131 -
10.132 -More predefined functions for datatypes: map?
10.133 -
10.134 -1 and 2 on nat?
10.135 -
10.136 -
10.137 ==============================================================
10.138 Recdef:
10.139