IOA/example/Correctness.thy
changeset 252 a4dc62a46ee4
parent 251 f04b33ce250f
child 253 132634d24019
equal deleted inserted replaced
251:f04b33ce250f 252:a4dc62a46ee4
     1 (*  Title:      HOL/IOA/example/Correctness.thy
       
     2     ID:         $Id$
       
     3     Author:     Tobias Nipkow & Konrad Slind
       
     4     Copyright   1994  TU Muenchen
       
     5 
       
     6 The main correctness proof: Impl implements Spec
       
     7 *)
       
     8 
       
     9 Correctness = Solve + Impl + Spec +
       
    10 
       
    11 consts
       
    12 
       
    13 hom :: "'m impl_state => 'm list"
       
    14 
       
    15 defs
       
    16 
       
    17 hom_def 
       
    18 "hom(s) == rq(rec(s)) @ if(rbit(rec(s)) = sbit(sen(s)),  
       
    19                           sq(sen(s)),                   
       
    20                           ttl(sq(sen(s))))"
       
    21 
       
    22 end