src/HOLCF/ex/hoare.thy

Replaced nat_ind_tac by induct_tac.

(*  Title:	HOLCF/ex/hoare.thy
    ID:         $Id$
    Author: 	Franz Regensburger
    Copyright	1993 Technische Universitaet Muenchen

Theory for an example by C.A.R. Hoare 

p x = if b1(x) 
         then p(g(x))
         else x fi

q x = if b1(x) orelse b2(x) 
         then q (g(x))
         else x fi

Prove: for all b1 b2 g . 
            q o p  = q 

In order to get a nice notation we fix the functions b1,b2 and g in the
signature of this example

*)

Hoare = Tr2 +

consts
	b1:: "'a -> tr"
	b2:: "'a -> tr"
	 g:: "'a -> 'a"
	p :: "'a -> 'a"
	q :: "'a -> 'a"

rules

  p_def  "p == fix[LAM f. LAM x.\
\                 If b1[x] then f[g[x]] else x fi]"

  q_def  "q == fix[LAM f. LAM x.\
\                 If b1[x] orelse b2[x] then f[g[x]] else x fi]"


end