1 theory Ind_Prelims

     1 theory Ind_Prelims

     3 begin

     3 begin

     4 

     4 

     5 section{* Preliminaries *}

     5 section{* Preliminaries *}

     6   

     6   

     7 text {*

     7 text {*

    13   showing how to define inductive predicates and then also how

    13   showing how to define inductive predicates and then also how

    14   to generate a reasoning infrastructure for them. From the examples 

    14   to generate a reasoning infrastructure for them. From the examples 

    15   we will figure out a general method for

    15   we will figure out a general method for

    16   defining inductive predicates.  The aim in this section is \emph{not} to

    16   defining inductive predicates.  The aim in this section is \emph{not} to

    17   write proofs that are as beautiful as possible, but as close as possible to

    17   write proofs that are as beautiful as possible, but as close as possible to

    21 

    19 

    22   We first consider the transitive closure of a relation @{text R}. The 

    20   We first consider the transitive closure of a relation @{text R}. The 

    23   ``pencil-and-paper'' specification for the transitive closure is:

    21   ``pencil-and-paper'' specification for the transitive closure is:

    24 

    22 

    25   \begin{center}\small

    23   \begin{center}\small

   159     done

   157     done

   160 qed

   158 qed

   161 

   159 

   162 text {*

   160 text {*

   163   Now we are done. It might be surprising that we are not using the automatic

   161   Now we are done. It might be surprising that we are not using the automatic

   165   "blast"} would easily dispense of it.

   163   "blast"} would easily dispense of it.

   166 *}

   164 *}

   167 

   165 

   168 lemma trcl_step_blast: 

   166 lemma trcl_step_blast: 

   169 shows "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"

   167 shows "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"