244
|
1 |
(* Title: HOLCF/coind.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Franz Regensburger
|
|
4 |
Copyright 1993 Technische Universitaet Muenchen
|
|
5 |
*)
|
|
6 |
|
|
7 |
open Coind;
|
|
8 |
|
|
9 |
(* ------------------------------------------------------------------------- *)
|
|
10 |
(* expand fixed point properties *)
|
|
11 |
(* ------------------------------------------------------------------------- *)
|
|
12 |
|
|
13 |
|
|
14 |
val nats_def2 = fix_prover Coind.thy nats_def
|
|
15 |
"nats = scons[dzero][smap[dsucc][nats]]";
|
|
16 |
|
|
17 |
val from_def2 = fix_prover Coind.thy from_def
|
|
18 |
"from = (LAM n.scons[n][from[dsucc[n]]])";
|
|
19 |
|
|
20 |
|
|
21 |
|
|
22 |
(* ------------------------------------------------------------------------- *)
|
|
23 |
(* recursive properties *)
|
|
24 |
(* ------------------------------------------------------------------------- *)
|
|
25 |
|
|
26 |
|
1043
|
27 |
val from = prove_goal Coind.thy "from[n] = scons[n][from[dsucc[n]]]"
|
244
|
28 |
(fn prems =>
|
|
29 |
[
|
|
30 |
(rtac trans 1),
|
|
31 |
(rtac (from_def2 RS ssubst) 1),
|
|
32 |
(simp_tac HOLCF_ss 1),
|
|
33 |
(rtac refl 1)
|
|
34 |
]);
|
|
35 |
|
|
36 |
|
1043
|
37 |
val from1 = prove_goal Coind.thy "from[UU] = UU"
|
244
|
38 |
(fn prems =>
|
|
39 |
[
|
|
40 |
(rtac trans 1),
|
|
41 |
(rtac (from RS ssubst) 1),
|
|
42 |
(resolve_tac stream_constrdef 1),
|
|
43 |
(rtac refl 1)
|
|
44 |
]);
|
|
45 |
|
|
46 |
val coind_rews =
|
|
47 |
[iterator1, iterator2, iterator3, smap1, smap2,from1];
|
|
48 |
|
|
49 |
|
|
50 |
(* ------------------------------------------------------------------------- *)
|
|
51 |
(* the example *)
|
|
52 |
(* prove: nats = from[dzero] *)
|
|
53 |
(* ------------------------------------------------------------------------- *)
|
|
54 |
|
|
55 |
|
1043
|
56 |
val coind_lemma1 = prove_goal Coind.thy "iterator[n][smap[dsucc]][nats] =\
|
244
|
57 |
\ scons[n][iterator[dsucc[n]][smap[dsucc]][nats]]"
|
|
58 |
(fn prems =>
|
|
59 |
[
|
297
|
60 |
(res_inst_tac [("s","n")] dnat_ind 1),
|
244
|
61 |
(simp_tac (HOLCF_ss addsimps (coind_rews @ stream_rews)) 1),
|
|
62 |
(simp_tac (HOLCF_ss addsimps (coind_rews @ stream_rews)) 1),
|
|
63 |
(rtac trans 1),
|
|
64 |
(rtac nats_def2 1),
|
|
65 |
(simp_tac (HOLCF_ss addsimps (coind_rews @ dnat_rews)) 1),
|
|
66 |
(rtac trans 1),
|
|
67 |
(etac iterator3 1),
|
|
68 |
(rtac trans 1),
|
|
69 |
(asm_simp_tac HOLCF_ss 1),
|
|
70 |
(rtac trans 1),
|
|
71 |
(etac smap2 1),
|
|
72 |
(rtac cfun_arg_cong 1),
|
|
73 |
(asm_simp_tac (HOLCF_ss addsimps ([iterator3 RS sym] @ dnat_rews)) 1)
|
|
74 |
]);
|
|
75 |
|
|
76 |
|
1043
|
77 |
val nats_eq_from = prove_goal Coind.thy "nats = from[dzero]"
|
244
|
78 |
(fn prems =>
|
|
79 |
[
|
|
80 |
(res_inst_tac [("R",
|
|
81 |
"% p q.? n. p = iterator[n][smap[dsucc]][nats] & q = from[n]")] stream_coind 1),
|
|
82 |
(res_inst_tac [("x","dzero")] exI 2),
|
|
83 |
(asm_simp_tac (HOLCF_ss addsimps coind_rews) 2),
|
|
84 |
(rewrite_goals_tac [stream_bisim_def]),
|
|
85 |
(strip_tac 1),
|
|
86 |
(etac exE 1),
|
|
87 |
(res_inst_tac [("Q","n=UU")] classical2 1),
|
|
88 |
(rtac disjI1 1),
|
|
89 |
(asm_simp_tac (HOLCF_ss addsimps coind_rews) 1),
|
|
90 |
(rtac disjI2 1),
|
|
91 |
(etac conjE 1),
|
|
92 |
(hyp_subst_tac 1),
|
|
93 |
(res_inst_tac [("x","n")] exI 1),
|
|
94 |
(res_inst_tac [("x","iterator[dsucc[n]][smap[dsucc]][nats]")] exI 1),
|
|
95 |
(res_inst_tac [("x","from[dsucc[n]]")] exI 1),
|
|
96 |
(etac conjI 1),
|
|
97 |
(rtac conjI 1),
|
|
98 |
(rtac coind_lemma1 1),
|
|
99 |
(rtac conjI 1),
|
|
100 |
(rtac from 1),
|
|
101 |
(res_inst_tac [("x","dsucc[n]")] exI 1),
|
|
102 |
(fast_tac HOL_cs 1)
|
|
103 |
]);
|
|
104 |
|
|
105 |
(* another proof using stream_coind_lemma2 *)
|
|
106 |
|
1043
|
107 |
val nats_eq_from = prove_goal Coind.thy "nats = from[dzero]"
|
244
|
108 |
(fn prems =>
|
|
109 |
[
|
|
110 |
(res_inst_tac [("R","% p q.? n. p = \
|
|
111 |
\ iterator[n][smap[dsucc]][nats] & q = from[n]")] stream_coind 1),
|
|
112 |
(rtac stream_coind_lemma2 1),
|
|
113 |
(strip_tac 1),
|
|
114 |
(etac exE 1),
|
|
115 |
(res_inst_tac [("Q","n=UU")] classical2 1),
|
|
116 |
(asm_simp_tac (HOLCF_ss addsimps coind_rews) 1),
|
|
117 |
(res_inst_tac [("x","UU::dnat")] exI 1),
|
|
118 |
(simp_tac (HOLCF_ss addsimps coind_rews addsimps stream_rews) 1),
|
|
119 |
(etac conjE 1),
|
|
120 |
(hyp_subst_tac 1),
|
|
121 |
(rtac conjI 1),
|
|
122 |
(rtac (coind_lemma1 RS ssubst) 1),
|
|
123 |
(rtac (from RS ssubst) 1),
|
|
124 |
(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
|
|
125 |
(res_inst_tac [("x","dsucc[n]")] exI 1),
|
|
126 |
(rtac conjI 1),
|
|
127 |
(rtac trans 1),
|
|
128 |
(rtac (coind_lemma1 RS ssubst) 1),
|
|
129 |
(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
|
|
130 |
(rtac refl 1),
|
|
131 |
(rtac trans 1),
|
|
132 |
(rtac (from RS ssubst) 1),
|
|
133 |
(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
|
|
134 |
(rtac refl 1),
|
|
135 |
(res_inst_tac [("x","dzero")] exI 1),
|
|
136 |
(asm_simp_tac (HOLCF_ss addsimps coind_rews) 1)
|
|
137 |
]);
|
|
138 |
|