1(*---------------------------------------------------------------------------
2    An example by C.A.R. Hoare (example found in Isabelle/HOLCF sources)
3
4        p x = if b1 x 
5                 then p (g x)
6                 else x fi
7
8        q x = if b1 x orelse b2 x 
9                 then q (g x)
10                 else x fi
11
12    Prove: for all b1 b2 g. q o p = q 
13
14    Our Assumptions: 
15
16        (1) that we are interested in total correctness;
17        (2) that "orelse" can be translated to disjunction
18
19    We attack the problem by making schematic definitions, which 
20    become constrained by termination conditions. The main insight
21    driving the proof is that if the function named "q" above 
22    terminates then so does "p". 
23 ---------------------------------------------------------------------------*)
24
25load "bossLib"; open bossLib;
26
27val G_def = DefineSchema `G x = if b1 x then G (g x) else x`
28val H_def = DefineSchema `H x = if b1 x \/ b2 x then H (g x) else x`;
29
30val THM = Q.prove 
31(`WF R /\ (!x. b1 x \/ b2 x ==> R (g x) x)
32       ==> 
33 (H b1 b2 g o G b1 g = H b1 b2 g)`,
34RW_TAC std_ss [combinTheory.o_DEF,FUN_EQ_THM] 
35 THEN Q.ID_SPEC_TAC `x`
36 THEN recInduct (fetch "-" "H_ind")
37 THEN RW_TAC std_ss []
38 THEN `!x. b1 x ==> R (g x) x` by PROVE_TAC[]
39 THEN ONCE_REWRITE_TAC [G_def]
40 THEN PROVE_TAC [H_def]);
41
42
43