src/Doc/ProgProve/Isar.thy
changeset 51445 1c9538a04e63
parent 51443 4edb82207c5c
child 52059 2f970c7f722b
equal deleted 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: