2820

1 
(* Title: LCF/ex/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 
(*** Section 10.4 ***)


11 


12 
val ex_thy =


13 
thy

3768

14 
> Theory.add_consts

2820

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


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


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


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

4026

19 
> PureThy.add_store_axioms

2820

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


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


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

3768

23 
> Theory.add_name "Ex 10.4";

2820

24 


25 
val ax = get_axiom ex_thy;


26 


27 
val P_strict = ax"P_strict";


28 
val K = ax"K";


29 
val H = ax"H";


30 


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


32 


33 


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


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


36 


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


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


39 


40 
val ex_ss = ex_ss addsimps [H_strict];


41 


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

4423

43 
by (induct_tac "K" 1);


44 
by (simp_tac ex_ss 1);


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


46 
by (strip_tac 1);


47 
by (stac H_unfold 1);


48 
by (asm_simp_tac ex_ss 1);

2820

49 
val H_idemp_lemma = topthm();


50 


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


52 


53 


54 
(*** Example 3.8 ***)


55 


56 
val ex_thy =


57 
thy

3768

58 
> Theory.add_consts

2820

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


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


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


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


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

4026

64 
> PureThy.add_store_axioms

2820

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


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


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

3768

68 
> Theory.add_name "Ex 3.8";

2820

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))";

4423

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);

2820

83 
result();


84 


85 


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


87 


88 
val ex_thy =


89 
thy

3768

90 
> Theory.add_consts

2820

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


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

4026

93 
> PureThy.add_store_axioms

2820

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


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

3768

96 
> Theory.add_name "fix ex";

2820

97 


98 
val ax = get_axiom ex_thy;


99 


100 
val p_strict = ax"p_strict";


101 
val p_s = ax"p_s";


102 


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


104 


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

4423

106 
by (induct_tac "s" 1);


107 
by (simp_tac ex_ss 1);


108 
by (simp_tac ex_ss 1);

2820

109 
result();


110 


111 


112 
(*** Prefixpoints ***)


113 


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

4423

115 
by (rewtac eq_def);

2820

116 
by (rtac conjI 1);

4423

117 
by (induct_tac "f" 1);

2820

118 
by (rtac minimal 1);

4423

119 
by (strip_tac 1);

2820

120 
by (rtac less_trans 1);


121 
by (resolve_tac asms 2);


122 
by (etac less_ap_term 1);


123 
by (resolve_tac asms 1);


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


125 
result();
