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