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