src/Doc/Tutorial/Misc/AdvancedInd.thy
changeset 58860 fee7cfa69c50
parent 48994 c84278efa9d5
child 63178 b9e1d53124f5
     1.1 --- a/src/Doc/Tutorial/Misc/AdvancedInd.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/Doc/Tutorial/Misc/AdvancedInd.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -1,5 +1,5 @@
     1.4  (*<*)
     1.5 -theory AdvancedInd imports Main begin;
     1.6 +theory AdvancedInd imports Main begin
     1.7  (*>*)
     1.8  
     1.9  text{*\noindent
    1.10 @@ -9,9 +9,9 @@
    1.11  (\S\ref{sec:ind-var-in-prems}), and how to utilize (\S\ref{sec:complete-ind})
    1.12  and even derive (\S\ref{sec:derive-ind}) new induction schemas. We conclude
    1.13  with an extended example of induction (\S\ref{sec:CTL-revisited}).
    1.14 -*};
    1.15 +*}
    1.16  
    1.17 -subsection{*Massaging the Proposition*};
    1.18 +subsection{*Massaging the Proposition*}
    1.19  
    1.20  text{*\label{sec:ind-var-in-prems}
    1.21  Often we have assumed that the theorem to be proved is already in a form
    1.22 @@ -19,7 +19,7 @@
    1.23  Here is an example.
    1.24  Since @{term"hd"} and @{term"last"} return the first and last element of a
    1.25  non-empty list, this lemma looks easy to prove:
    1.26 -*};
    1.27 +*}
    1.28  
    1.29  lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs"
    1.30  apply(induct_tac xs)
    1.31 @@ -51,11 +51,11 @@
    1.32  implication~(@{text"\<longrightarrow>"}), letting
    1.33  \attrdx{rule_format} (\S\ref{sec:forward}) convert the
    1.34  result to the usual @{text"\<Longrightarrow>"} form:
    1.35 -*};
    1.36 -(*<*)oops;(*>*)
    1.37 -lemma hd_rev [rule_format]: "xs \<noteq> [] \<longrightarrow> hd(rev xs) = last xs";
    1.38 +*}
    1.39 +(*<*)oops(*>*)
    1.40 +lemma hd_rev [rule_format]: "xs \<noteq> [] \<longrightarrow> hd(rev xs) = last xs"
    1.41  (*<*)
    1.42 -apply(induct_tac xs);
    1.43 +apply(induct_tac xs)
    1.44  (*>*)
    1.45  
    1.46  txt{*\noindent
    1.47 @@ -112,7 +112,7 @@
    1.48  *}
    1.49  (*<*)by auto(*>*)
    1.50  
    1.51 -subsection{*Beyond Structural and Recursion Induction*};
    1.52 +subsection{*Beyond Structural and Recursion Induction*}
    1.53  
    1.54  text{*\label{sec:complete-ind}
    1.55  So far, inductive proofs were by structural induction for
    1.56 @@ -130,7 +130,7 @@
    1.57  @{thm[display]"nat_less_induct"[no_vars]}
    1.58  As an application, we prove a property of the following
    1.59  function:
    1.60 -*};
    1.61 +*}
    1.62  
    1.63  axiomatization f :: "nat \<Rightarrow> nat"
    1.64    where f_ax: "f(f(n)) < f(Suc(n))"
    1.65 @@ -148,17 +148,17 @@
    1.66  The axiom for @{term"f"} implies @{prop"n <= f n"}, which can
    1.67  be proved by induction on \mbox{@{term"f n"}}. Following the recipe outlined
    1.68  above, we have to phrase the proposition as follows to allow induction:
    1.69 -*};
    1.70 +*}
    1.71  
    1.72 -lemma f_incr_lem: "\<forall>i. k = f i \<longrightarrow> i \<le> f i";
    1.73 +lemma f_incr_lem: "\<forall>i. k = f i \<longrightarrow> i \<le> f i"
    1.74  
    1.75  txt{*\noindent
    1.76  To perform induction on @{term k} using @{thm[source]nat_less_induct}, we use
    1.77  the same general induction method as for recursion induction (see
    1.78  \S\ref{sec:fun-induction}):
    1.79 -*};
    1.80 +*}
    1.81  
    1.82 -apply(induct_tac k rule: nat_less_induct);
    1.83 +apply(induct_tac k rule: nat_less_induct)
    1.84  
    1.85  txt{*\noindent
    1.86  We get the following proof state:
    1.87 @@ -203,17 +203,17 @@
    1.88  proofs are easy to write but hard to read and understand.
    1.89  
    1.90  The desired result, @{prop"i <= f i"}, follows from @{thm[source]f_incr_lem}:
    1.91 -*};
    1.92 +*}
    1.93  
    1.94 -lemmas f_incr = f_incr_lem[rule_format, OF refl];
    1.95 +lemmas f_incr = f_incr_lem[rule_format, OF refl]
    1.96  
    1.97  text{*\noindent
    1.98  The final @{thm[source]refl} gets rid of the premise @{text"?k = f ?i"}. 
    1.99  We could have included this derivation in the original statement of the lemma:
   1.100 -*};
   1.101 +*}
   1.102  
   1.103 -lemma f_incr[rule_format, OF refl]: "\<forall>i. k = f i \<longrightarrow> i \<le> f i";
   1.104 -(*<*)oops;(*>*)
   1.105 +lemma f_incr[rule_format, OF refl]: "\<forall>i. k = f i \<longrightarrow> i \<le> f i"
   1.106 +(*<*)oops(*>*)
   1.107  
   1.108  text{*
   1.109  \begin{exercise}
   1.110 @@ -237,7 +237,7 @@
   1.111  where @{term f} may be any function into type @{typ nat}.
   1.112  *}
   1.113  
   1.114 -subsection{*Derivation of New Induction Schemas*};
   1.115 +subsection{*Derivation of New Induction Schemas*}
   1.116  
   1.117  text{*\label{sec:derive-ind}
   1.118  \index{induction!deriving new schemas}%
   1.119 @@ -246,18 +246,18 @@
   1.120  of @{thm[source]nat_less_induct}. Assume we only have structural induction
   1.121  available for @{typ"nat"} and want to derive complete induction.  We
   1.122  must generalize the statement as shown:
   1.123 -*};
   1.124 +*}
   1.125  
   1.126 -lemma induct_lem: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> \<forall>m<n. P m";
   1.127 -apply(induct_tac n);
   1.128 +lemma induct_lem: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> \<forall>m<n. P m"
   1.129 +apply(induct_tac n)
   1.130  
   1.131  txt{*\noindent
   1.132  The base case is vacuously true. For the induction step (@{prop"m <
   1.133  Suc n"}) we distinguish two cases: case @{prop"m < n"} is true by induction
   1.134  hypothesis and case @{prop"m = n"} follows from the assumption, again using
   1.135  the induction hypothesis:
   1.136 -*};
   1.137 - apply(blast);
   1.138 +*}
   1.139 + apply(blast)
   1.140  by(blast elim: less_SucE)
   1.141  
   1.142  text{*\noindent
   1.143 @@ -270,10 +270,10 @@
   1.144  and remove the trivial condition @{prop"n < Suc n"}. Fortunately, this
   1.145  happens automatically when we add the lemma as a new premise to the
   1.146  desired goal:
   1.147 -*};
   1.148 +*}
   1.149  
   1.150 -theorem nat_less_induct: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> P n";
   1.151 -by(insert induct_lem, blast);
   1.152 +theorem nat_less_induct: "(\<And>n::nat. \<forall>m<n. P m \<Longrightarrow> P n) \<Longrightarrow> P n"
   1.153 +by(insert induct_lem, blast)
   1.154  
   1.155  text{*
   1.156  HOL already provides the mother of