# HG changeset patch
# User paulson
# Date 971865059 -7200
# Node ID e0428c2778f1c43c13e812180bf0157e3fb48bdf
# Parent  9ac0fe356ea76e6a57b209df50847b88d2eea260
wellfounded -> well-founded

diff -r 9ac0fe356ea7 -r e0428c2778f1 doc-src/TutorialI/Advanced/WFrec.thy
--- a/doc-src/TutorialI/Advanced/WFrec.thy	Tue Oct 17 22:25:23 2000 +0200
+++ b/doc-src/TutorialI/Advanced/WFrec.thy	Wed Oct 18 12:30:59 2000 +0200
@@ -21,28 +21,28 @@
 component decreases (as in the inner call in the third equation).
 
 In general, \isacommand{recdef} supports termination proofs based on
-arbitrary \emph{wellfounded relations}, i.e.\ \emph{wellfounded
-recursion}\indexbold{recursion!wellfounded}\index{wellfounded
-recursion|see{recursion, wellfounded}}.  A relation $<$ is
-\bfindex{wellfounded} if it has no infinite descending chain $\cdots <
+arbitrary \emph{well-founded relations}, i.e.\ \emph{well-founded
+recursion}\indexbold{recursion!well-founded}\index{well-founded
+recursion|see{recursion, well-founded}}.  A relation $<$ is
+\bfindex{well-founded} if it has no infinite descending chain $\cdots <
 a@2 < a@1 < a@0$. Clearly, a function definition is total iff the set
 of all pairs $(r,l)$, where $l$ is the argument on the left-hand side
 of an equation and $r$ the argument of some recursive call on the
-corresponding right-hand side, induces a wellfounded relation.  For a
-systematic account of termination proofs via wellfounded relations
+corresponding right-hand side, induces a well-founded relation.  For a
+systematic account of termination proofs via well-founded relations
 see, for example, \cite{Baader-Nipkow}. The HOL library formalizes
-some of the theory of wellfounded relations. For example
+some of the theory of well-founded relations. For example
 @{prop"wf r"}\index{*wf|bold} means that relation @{term[show_types]"r::('a*'a)set"} is
-wellfounded.
+well-founded.
 
 Each \isacommand{recdef} definition should be accompanied (after the
-name of the function) by a wellfounded relation on the argument type
+name of the function) by a well-founded relation on the argument type
 of the function. For example, \isaindexbold{measure} is defined by
 @{prop[display]"measure(f::'a \<Rightarrow> nat) \<equiv> {(y,x). f y < f x}"}
-and it has been proved that @{term"measure f"} is always wellfounded.
+and it has been proved that @{term"measure f"} is always well-founded.
 
 In addition to @{term measure}, the library provides
-a number of further constructions for obtaining wellfounded relations.
+a number of further constructions for obtaining well-founded relations.
 Above we have already met @{text"<*lex*>"} of type
 @{typ[display,source]"('a \<times> 'a)set \<Rightarrow> ('b \<times> 'b)set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b))set"}
 Of course the lexicographic product can also be interated, as in the following
@@ -60,7 +60,7 @@
 text{*
 Lexicographic products of measure functions already go a long way. A
 further useful construction is the embedding of some type in an
-existing wellfounded relation via the inverse image of a function:
+existing well-founded relation via the inverse image of a function:
 @{thm[display,show_types]inv_image_def[no_vars]}
 \begin{sloppypar}
 \noindent
@@ -72,13 +72,13 @@
 %Finally there is also {finite_psubset} the proper subset relation on finite sets
 
 All the above constructions are known to \isacommand{recdef}. Thus you
-will never have to prove wellfoundedness of any relation composed
+will never have to prove well-foundedness of any relation composed
 solely of these building blocks. But of course the proof of
 termination of your function definition, i.e.\ that the arguments
 decrease with every recursive call, may still require you to provide
 additional lemmas.
 
-It is also possible to use your own wellfounded relations with \isacommand{recdef}.
+It is also possible to use your own well-founded relations with \isacommand{recdef}.
 Here is a simplistic example:
 *}
 
@@ -90,8 +90,8 @@
 text{*
 Since \isacommand{recdef} is not prepared for @{term id}, the identity
 function, this leads to the complaint that it could not prove
-@{prop"wf (id less_than)"}, the wellfoundedness of @{term"id
-less_than"}. We should first have proved that @{term id} preserves wellfoundedness
+@{prop"wf (id less_than)"}, the well-foundedness of @{term"id
+less_than"}. We should first have proved that @{term id} preserves well-foundedness
 *}
 
 lemma wf_id: "wf r \<Longrightarrow> wf(id r)"
diff -r 9ac0fe356ea7 -r e0428c2778f1 doc-src/TutorialI/Advanced/document/WFrec.tex
--- a/doc-src/TutorialI/Advanced/document/WFrec.tex	Tue Oct 17 22:25:23 2000 +0200
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex	Wed Oct 18 12:30:59 2000 +0200
@@ -23,30 +23,30 @@
 component decreases (as in the inner call in the third equation).
 
 In general, \isacommand{recdef} supports termination proofs based on
-arbitrary \emph{wellfounded relations}, i.e.\ \emph{wellfounded
-recursion}\indexbold{recursion!wellfounded}\index{wellfounded
-recursion|see{recursion, wellfounded}}.  A relation $<$ is
-\bfindex{wellfounded} if it has no infinite descending chain $\cdots <
+arbitrary \emph{well-founded relations}, i.e.\ \emph{well-founded
+recursion}\indexbold{recursion!well-founded}\index{well-founded
+recursion|see{recursion, well-founded}}.  A relation $<$ is
+\bfindex{well-founded} if it has no infinite descending chain $\cdots <
 a@2 < a@1 < a@0$. Clearly, a function definition is total iff the set
 of all pairs $(r,l)$, where $l$ is the argument on the left-hand side
 of an equation and $r$ the argument of some recursive call on the
-corresponding right-hand side, induces a wellfounded relation.  For a
-systematic account of termination proofs via wellfounded relations
+corresponding right-hand side, induces a well-founded relation.  For a
+systematic account of termination proofs via well-founded relations
 see, for example, \cite{Baader-Nipkow}. The HOL library formalizes
-some of the theory of wellfounded relations. For example
+some of the theory of well-founded relations. For example
 \isa{wf\ r}\index{*wf|bold} means that relation \isa{r{\isasymColon}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set} is
-wellfounded.
+well-founded.
 
 Each \isacommand{recdef} definition should be accompanied (after the
-name of the function) by a wellfounded relation on the argument type
+name of the function) by a well-founded relation on the argument type
 of the function. For example, \isaindexbold{measure} is defined by
 \begin{isabelle}%
 \ \ \ \ \ measure\ f\ {\isasymequiv}\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\ f\ y\ {\isacharless}\ f\ x{\isacharbraceright}%
 \end{isabelle}
-and it has been proved that \isa{measure\ f} is always wellfounded.
+and it has been proved that \isa{measure\ f} is always well-founded.
 
 In addition to \isa{measure}, the library provides
-a number of further constructions for obtaining wellfounded relations.
+a number of further constructions for obtaining well-founded relations.
 Above we have already met \isa{{\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}} of type
 \begin{isabelle}%
 \ \ \ \ \ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ {\isasymtimes}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}{\isacharparenright}set{\isachardoublequote}%
@@ -64,7 +64,7 @@
 \begin{isamarkuptext}%
 Lexicographic products of measure functions already go a long way. A
 further useful construction is the embedding of some type in an
-existing wellfounded relation via the inverse image of a function:
+existing well-founded relation via the inverse image of a function:
 \begin{isabelle}%
 \ \ \ \ \ inv{\isacharunderscore}image\ {\isacharparenleft}r{\isasymColon}{\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set{\isacharparenright}\ {\isacharparenleft}f{\isasymColon}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isacharparenright}\ {\isasymequiv}\isanewline
 \ \ \ \ \ {\isacharbraceleft}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharcomma}\ y{\isasymColon}{\isacharprime}a{\isacharparenright}{\isachardot}\ {\isacharparenleft}f\ x{\isacharcomma}\ f\ y{\isacharparenright}\ {\isasymin}\ r{\isacharbraceright}%
@@ -79,13 +79,13 @@
 %Finally there is also {finite_psubset} the proper subset relation on finite sets
 
 All the above constructions are known to \isacommand{recdef}. Thus you
-will never have to prove wellfoundedness of any relation composed
+will never have to prove well-foundedness of any relation composed
 solely of these building blocks. But of course the proof of
 termination of your function definition, i.e.\ that the arguments
 decrease with every recursive call, may still require you to provide
 additional lemmas.
 
-It is also possible to use your own wellfounded relations with \isacommand{recdef}.
+It is also possible to use your own well-founded relations with \isacommand{recdef}.
 Here is a simplistic example:%
 \end{isamarkuptext}%
 \isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
@@ -95,7 +95,7 @@
 \begin{isamarkuptext}%
 Since \isacommand{recdef} is not prepared for \isa{id}, the identity
 function, this leads to the complaint that it could not prove
-\isa{wf\ {\isacharparenleft}id\ less{\isacharunderscore}than{\isacharparenright}}, the wellfoundedness of \isa{id\ less{\isacharunderscore}than}. We should first have proved that \isa{id} preserves wellfoundedness%
+\isa{wf\ {\isacharparenleft}id\ less{\isacharunderscore}than{\isacharparenright}}, the well-foundedness of \isa{id\ less{\isacharunderscore}than}. We should first have proved that \isa{id} preserves well-foundedness%
 \end{isamarkuptext}%
 \isacommand{lemma}\ wf{\isacharunderscore}id{\isacharcolon}\ {\isachardoublequote}wf\ r\ {\isasymLongrightarrow}\ wf{\isacharparenleft}id\ r{\isacharparenright}{\isachardoublequote}\isanewline
 \isacommand{by}\ simp%
diff -r 9ac0fe356ea7 -r e0428c2778f1 doc-src/TutorialI/CTL/CTLind.thy
--- a/doc-src/TutorialI/CTL/CTLind.thy	Tue Oct 17 22:25:23 2000 +0200
+++ b/doc-src/TutorialI/CTL/CTLind.thy	Wed Oct 18 12:30:59 2000 +0200
@@ -16,7 +16,7 @@
 then @{prop"s \<in> lfp(af A)"}. We prove this by inductively defining the set
 @{term"Avoid s A"} of states reachable from @{term s} by a finite @{term
 A}-avoiding path:
-% Second proof of opposite direction, directly by wellfounded induction
+% Second proof of opposite direction, directly by well-founded induction
 % on the initial segment of M that avoids A.
 *}
 
@@ -66,14 +66,14 @@
   "\<forall>p\<in>Paths s. \<exists>i. p i \<in> A \<Longrightarrow> t \<in> Avoid s A \<longrightarrow> t \<in> lfp(af A)";
 txt{*\noindent
 The trick is not to induct on @{prop"t \<in> Avoid s A"}, as already the base
-case would be a problem, but to proceed by wellfounded induction @{term
+case would be a problem, but to proceed by well-founded induction @{term
 t}. Hence @{prop"t \<in> Avoid s A"} needs to be brought into the conclusion as
 well, which the directive @{text rule_format} undoes at the end (see below).
-But induction with respect to which wellfounded relation? The restriction
+But induction with respect to which well-founded relation? The restriction
 of @{term M} to @{term"Avoid s A"}:
 @{term[display]"{(y,x). (x,y) \<in> M \<and> x \<in> Avoid s A \<and> y \<in> Avoid s A \<and> x \<notin> A}"}
 As we shall see in a moment, the absence of infinite @{term A}-avoiding paths
-starting from @{term s} implies wellfoundedness of this relation. For the
+starting from @{term s} implies well-foundedness of this relation. For the
 moment we assume this and proceed with the induction:
 *}
 
@@ -100,8 +100,8 @@
 
 txt{*
 Having proved the main goal we return to the proof obligation that the above
-relation is indeed wellfounded. This is proved by contraposition: we assume
-the relation is not wellfounded. Thus there exists an infinite @{term
+relation is indeed well-founded. This is proved by contraposition: we assume
+the relation is not well-founded. Thus there exists an infinite @{term
 A}-avoiding path all in @{term"Avoid s A"}, by theorem
 @{thm[source]wf_iff_no_infinite_down_chain}:
 @{thm[display]wf_iff_no_infinite_down_chain[no_vars]}
diff -r 9ac0fe356ea7 -r e0428c2778f1 doc-src/TutorialI/Misc/AdvancedInd.thy
--- a/doc-src/TutorialI/Misc/AdvancedInd.thy	Tue Oct 17 22:25:23 2000 +0200
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy	Wed Oct 18 12:30:59 2000 +0200
@@ -290,16 +290,16 @@
 text{*
 
 Finally we should mention that HOL already provides the mother of all
-inductions, \textbf{wellfounded
-induction}\indexbold{induction!wellfounded}\index{wellfounded
-induction|see{induction, wellfounded}} (@{thm[source]wf_induct}):
+inductions, \textbf{well-founded
+induction}\indexbold{induction!well-founded}\index{well-founded
+induction|see{induction, well-founded}} (@{thm[source]wf_induct}):
 @{thm[display]wf_induct[no_vars]}
-where @{term"wf r"} means that the relation @{term r} is wellfounded
-(see \S\ref{sec:wellfounded}).
+where @{term"wf r"} means that the relation @{term r} is well-founded
+(see \S\ref{sec:well-founded}).
 For example, theorem @{thm[source]nat_less_induct} can be viewed (and
 derived) as a special case of @{thm[source]wf_induct} where 
 @{term r} is @{text"<"} on @{typ nat}. The details can be found in the HOL library.
-For a mathematical account of wellfounded induction see, for example, \cite{Baader-Nipkow}.
+For a mathematical account of well-founded induction see, for example, \cite{Baader-Nipkow}.
 *};
 
 (*<*)