src/Doc/ProgProve/Isar.thy
 changeset 51445 1c9538a04e63 parent 51443 4edb82207c5c child 52059 2f970c7f722b
equal inserted replaced
51444:027cdce376d5 51445:1c9538a04e63
   979
   979
   980 text{* Normally not all cases will be impossible. As a simple exercise,
   980 text{* Normally not all cases will be impossible. As a simple exercise,
   981 prove that \mbox{@{prop"\<not> ev(Suc(Suc(Suc 0)))"}.}
   981 prove that \mbox{@{prop"\<not> ev(Suc(Suc(Suc 0)))"}.}
   982
   982
   983 \subsection{Advanced rule induction}
   983 \subsection{Advanced rule induction}

   984 \label{sec:advanced-rule-induction}
   984
   985
   985 So far, rule induction was always applied to goals of the form @{text"I x y z \<Longrightarrow> \<dots>"}
   986 So far, rule induction was always applied to goals of the form @{text"I x y z \<Longrightarrow> \<dots>"}
   986 where @{text I} is some inductively defined predicate and @{text x}, @{text y}, @{text z}
   987 where @{text I} is some inductively defined predicate and @{text x}, @{text y}, @{text z}
   987 are variables. In some rare situations one needs to deal with an assumption where
   988 are variables. In some rare situations one needs to deal with an assumption where
   988 not all arguments @{text r}, @{text s}, @{text t} are variables:
   989 not all arguments @{text r}, @{text s}, @{text t} are variables: