1 (* Title: LCF/ex.ML |
1 (* Title: LCF/ex.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1991 University of Cambridge |
4 Copyright 1991 University of Cambridge |
5 |
5 |
6 Some examples from Lawrence Paulson's book Logic and Computation. |
6 Some examples from Lawrence Paulson's book Logic and Computation. |
7 *) |
7 *) |
8 |
8 |
9 |
9 |
10 LCF_build_completed; (*Cause examples to fail if LCF did*) |
10 LCF_build_completed; (*Cause examples to fail if LCF did*) |
11 |
11 |
12 proof_timing := true; |
12 proof_timing := true; |
13 |
13 |
14 (*** Section 10.4 ***) |
14 (*** Section 10.4 ***) |
15 |
15 |
16 val ex_thy = extend_theory thy "Ex 10.4" |
16 val ex_thy = |
17 ([], [], [], [], [], |
17 thy |
18 [(["P"], "'a => tr"), |
18 |> add_consts |
19 (["G","H"], "'a => 'a"), |
19 [("P", "'a => tr", NoSyn), |
20 (["K"], "('a => 'a) => ('a => 'a)") |
20 ("G", "'a => 'a", NoSyn), |
21 ], |
21 ("H", "'a => 'a", NoSyn), |
22 None) |
22 ("K", "('a => 'a) => ('a => 'a)", NoSyn)] |
23 [ ("P_strict", "P(UU) = UU"), |
23 |> add_axioms |
24 ("K", "K = (%h x. P(x) => x | h(h(G(x))))"), |
24 [("P_strict", "P(UU) = UU"), |
25 ("H", "H = FIX(K)") |
25 ("K", "K = (%h x. P(x) => x | h(h(G(x))))"), |
26 ]; |
26 ("H", "H = FIX(K)")] |
|
27 |> add_thyname "Ex 10.4"; |
|
28 |
27 val ax = get_axiom ex_thy; |
29 val ax = get_axiom ex_thy; |
28 |
30 |
29 val P_strict = ax"P_strict"; |
31 val P_strict = ax"P_strict"; |
30 val K = ax"K"; |
32 val K = ax"K"; |
31 val H = ax"H"; |
33 val H = ax"H"; |
53 val H_idemp = rewrite_rule [mk_meta_eq (H RS sym)] H_idemp_lemma; |
55 val H_idemp = rewrite_rule [mk_meta_eq (H RS sym)] H_idemp_lemma; |
54 |
56 |
55 |
57 |
56 (*** Example 3.8 ***) |
58 (*** Example 3.8 ***) |
57 |
59 |
58 val ex_thy = extend_theory thy "Ex 3.8" |
60 val ex_thy = |
59 ([], [], [], [], [], |
61 thy |
60 [(["P"], "'a => tr"), |
62 |> add_consts |
61 (["F","G"], "'a => 'a"), |
63 [("P", "'a => tr", NoSyn), |
62 (["H"], "'a => 'b => 'b"), |
64 ("F", "'a => 'a", NoSyn), |
63 (["K"], "('a => 'b => 'b) => ('a => 'b => 'b)") |
65 ("G", "'a => 'a", NoSyn), |
64 ], |
66 ("H", "'a => 'b => 'b", NoSyn), |
65 None) |
67 ("K", "('a => 'b => 'b) => ('a => 'b => 'b)", NoSyn)] |
66 [ ("F_strict", "F(UU) = UU"), |
68 |> add_axioms |
67 ("K", "K = (%h x y. P(x) => y | F(h(G(x),y)))"), |
69 [("F_strict", "F(UU) = UU"), |
68 ("H", "H = FIX(K)") |
70 ("K", "K = (%h x y. P(x) => y | F(h(G(x),y)))"), |
69 ]; |
71 ("H", "H = FIX(K)")] |
|
72 |> add_thyname "Ex 3.8"; |
|
73 |
70 val ax = get_axiom ex_thy; |
74 val ax = get_axiom ex_thy; |
71 |
75 |
72 val F_strict = ax"F_strict"; |
76 val F_strict = ax"F_strict"; |
73 val K = ax"K"; |
77 val K = ax"K"; |
74 val H = ax"H"; |
78 val H = ax"H"; |
83 result(); |
87 result(); |
84 |
88 |
85 |
89 |
86 (*** Addition with fixpoint of successor ***) |
90 (*** Addition with fixpoint of successor ***) |
87 |
91 |
88 val ex_thy = extend_theory thy "fix ex" |
92 val ex_thy = |
89 ([], [], [], [], [], |
93 thy |
90 [(["s"], "'a => 'a"), |
94 |> add_consts |
91 (["p"], "'a => 'a => 'a") |
95 [("s", "'a => 'a", NoSyn), |
92 ], |
96 ("p", "'a => 'a => 'a", NoSyn)] |
93 None) |
97 |> add_axioms |
94 [ ("p_strict", "p(UU) = UU"), |
98 [("p_strict", "p(UU) = UU"), |
95 ("p_s", "p(s(x),y) = s(p(x,y))") |
99 ("p_s", "p(s(x),y) = s(p(x,y))")] |
96 ]; |
100 |> add_thyname "fix ex"; |
|
101 |
97 val ax = get_axiom ex_thy; |
102 val ax = get_axiom ex_thy; |
98 |
103 |
99 val p_strict = ax"p_strict"; |
104 val p_strict = ax"p_strict"; |
100 val p_s = ax"p_s"; |
105 val p_s = ax"p_s"; |
101 |
106 |