420

1 
(* Title: LCF/ex.ML

0

2 
ID: $Id$

420

3 
Author: Tobias Nipkow

0

4 
Copyright 1991 University of Cambridge


5 


6 
Some examples from Lawrence Paulson's book Logic and Computation.


7 
*)


8 


9 

420

10 
LCF_build_completed; (*Cause examples to fail if LCF did*)

0

11 


12 
proof_timing := true;


13 


14 
(*** Section 10.4 ***)


15 

420

16 
val ex_thy =


17 
thy


18 
> add_consts


19 
[("P", "'a => tr", NoSyn),


20 
("G", "'a => 'a", NoSyn),


21 
("H", "'a => 'a", NoSyn),


22 
("K", "('a => 'a) => ('a => 'a)", NoSyn)]


23 
> add_axioms


24 
[("P_strict", "P(UU) = UU"),


25 
("K", "K = (%h x. P(x) => x  h(h(G(x))))"),


26 
("H", "H = FIX(K)")]


27 
> add_thyname "Ex 10.4";


28 

0

29 
val ax = get_axiom ex_thy;


30 


31 
val P_strict = ax"P_strict";


32 
val K = ax"K";


33 
val H = ax"H";


34 


35 
val ex_ss = LCF_ss addsimps [P_strict,K];


36 


37 


38 
val H_unfold = prove_goal ex_thy "H = K(H)"


39 
(fn _ => [stac H 1, rtac (FIX_eq RS sym) 1]);


40 


41 
val H_strict = prove_goal ex_thy "H(UU)=UU"


42 
(fn _ => [stac H_unfold 1, simp_tac ex_ss 1]);


43 


44 
val ex_ss = ex_ss addsimps [H_strict];


45 


46 
goal ex_thy "ALL x. H(FIX(K,x)) = FIX(K,x)";


47 
by(induct_tac "K" 1);


48 
by(simp_tac ex_ss 1);


49 
by(simp_tac (ex_ss setloop (split_tac [COND_cases_iff])) 1);


50 
by(strip_tac 1);


51 
by(stac H_unfold 1);


52 
by(asm_simp_tac ex_ss 1);


53 
val H_idemp_lemma = topthm();


54 


55 
val H_idemp = rewrite_rule [mk_meta_eq (H RS sym)] H_idemp_lemma;


56 


57 


58 
(*** Example 3.8 ***)


59 

420

60 
val ex_thy =


61 
thy


62 
> add_consts


63 
[("P", "'a => tr", NoSyn),


64 
("F", "'a => 'a", NoSyn),


65 
("G", "'a => 'a", NoSyn),


66 
("H", "'a => 'b => 'b", NoSyn),


67 
("K", "('a => 'b => 'b) => ('a => 'b => 'b)", NoSyn)]


68 
> add_axioms


69 
[("F_strict", "F(UU) = UU"),


70 
("K", "K = (%h x y. P(x) => y  F(h(G(x),y)))"),


71 
("H", "H = FIX(K)")]


72 
> add_thyname "Ex 3.8";


73 

0

74 
val ax = get_axiom ex_thy;


75 


76 
val F_strict = ax"F_strict";


77 
val K = ax"K";


78 
val H = ax"H";


79 


80 
val ex_ss = LCF_ss addsimps [F_strict,K];


81 


82 
goal ex_thy "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))";


83 
by(stac H 1);


84 
by(induct_tac "K::('a=>'b=>'b)=>('a=>'b=>'b)" 1);


85 
by(simp_tac ex_ss 1);


86 
by(asm_simp_tac (ex_ss setloop (split_tac [COND_cases_iff])) 1);


87 
result();


88 


89 


90 
(*** Addition with fixpoint of successor ***)


91 

420

92 
val ex_thy =


93 
thy


94 
> add_consts


95 
[("s", "'a => 'a", NoSyn),


96 
("p", "'a => 'a => 'a", NoSyn)]


97 
> add_axioms


98 
[("p_strict", "p(UU) = UU"),


99 
("p_s", "p(s(x),y) = s(p(x,y))")]


100 
> add_thyname "fix ex";


101 

0

102 
val ax = get_axiom ex_thy;


103 


104 
val p_strict = ax"p_strict";


105 
val p_s = ax"p_s";


106 


107 
val ex_ss = LCF_ss addsimps [p_strict,p_s];


108 


109 
goal ex_thy "p(FIX(s),y) = FIX(s)";


110 
by(induct_tac "s" 1);


111 
by(simp_tac ex_ss 1);


112 
by(simp_tac ex_ss 1);


113 
result();


114 


115 


116 
(*** Prefixpoints ***)


117 


118 
val asms = goal thy "[ f(p) << p; !!q. f(q) << q ==> p << q ] ==> FIX(f)=p";


119 
by(rewtac eq_def);


120 
by (rtac conjI 1);


121 
by(induct_tac "f" 1);


122 
by (rtac minimal 1);


123 
by(strip_tac 1);


124 
by (rtac less_trans 1);


125 
by (resolve_tac asms 2);


126 
by (etac less_ap_term 1);


127 
by (resolve_tac asms 1);


128 
by (rtac (FIX_eq RS eq_imp_less1) 1);


129 
result();


130 


131 
maketest"END: file for LCF examples";
