0

1 
(* Title: LCF/ex.ML


2 
ID: $Id$


3 
Author: Tobias Nipkow


4 
Copyright 1991 University of Cambridge


5 


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


7 
*)


8 


9 


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


11 


12 
proof_timing := true;


13 


14 
(*** Section 10.4 ***)


15 


16 
val ex_thy = extend_theory thy "Ex 10.4"


17 
([], [], [], [],


18 
[(["P"], "'a => tr"),


19 
(["G","H"], "'a => 'a"),


20 
(["K"], "('a => 'a) => ('a => 'a)")


21 
],


22 
None)


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


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


25 
("H", "H = FIX(K)")


26 
];


27 
val ax = get_axiom ex_thy;


28 


29 
val P_strict = ax"P_strict";


30 
val K = ax"K";


31 
val H = ax"H";


32 


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


34 


35 


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


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


38 


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


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


41 


42 
val ex_ss = ex_ss addsimps [H_strict];


43 


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


45 
by(induct_tac "K" 1);


46 
by(simp_tac ex_ss 1);


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


48 
by(strip_tac 1);


49 
by(stac H_unfold 1);


50 
by(asm_simp_tac ex_ss 1);


51 
val H_idemp_lemma = topthm();


52 


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


54 


55 


56 
(*** Example 3.8 ***)


57 


58 
val ex_thy = extend_theory thy "Ex 3.8"


59 
([], [], [], [],


60 
[(["P"], "'a => tr"),


61 
(["F","G"], "'a => 'a"),


62 
(["H"], "'a => 'b => 'b"),


63 
(["K"], "('a => 'b => 'b) => ('a => 'b => 'b)")


64 
],


65 
None)


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


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


68 
("H", "H = FIX(K)")


69 
];


70 
val ax = get_axiom ex_thy;


71 


72 
val F_strict = ax"F_strict";


73 
val K = ax"K";


74 
val H = ax"H";


75 


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


77 


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


79 
by(stac H 1);


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


81 
by(simp_tac ex_ss 1);


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


83 
result();


84 


85 


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


87 


88 
val ex_thy = extend_theory thy "fix ex"


89 
([], [], [], [],


90 
[(["s"], "'a => 'a"),


91 
(["p"], "'a => 'a => 'a")


92 
],


93 
None)


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


95 
("p_s", "p(s(x),y) = s(p(x,y))")


96 
];


97 
val ax = get_axiom ex_thy;


98 


99 
val p_strict = ax"p_strict";


100 
val p_s = ax"p_s";


101 


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


103 


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


105 
by(induct_tac "s" 1);


106 
by(simp_tac ex_ss 1);


107 
by(simp_tac ex_ss 1);


108 
result();


109 


110 


111 
(*** Prefixpoints ***)


112 


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


114 
by(rewtac eq_def);


115 
by (rtac conjI 1);


116 
by(induct_tac "f" 1);


117 
by (rtac minimal 1);


118 
by(strip_tac 1);


119 
by (rtac less_trans 1);


120 
by (resolve_tac asms 2);


121 
by (etac less_ap_term 1);


122 
by (resolve_tac asms 1);


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


124 
result();


125 


126 
maketest"END: file for LCF examples";
