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 |
|
27 val from = prove_goal Coind.thy "from[n] = scons[n][from[dsucc[n]]]" |
|
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 |
|
37 val from1 = prove_goal Coind.thy "from[UU] = UU" |
|
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 |
|
56 val coind_lemma1 = prove_goal Coind.thy "iterator[n][smap[dsucc]][nats] =\ |
|
57 \ scons[n][iterator[dsucc[n]][smap[dsucc]][nats]]" |
|
58 (fn prems => |
|
59 [ |
|
60 (res_inst_tac [("s","n")] dnat_ind 1), |
|
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 |
|
77 val nats_eq_from = prove_goal Coind.thy "nats = from[dzero]" |
|
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 (hyp_subst_tac 1), |
|
94 (res_inst_tac [("x","n")] exI 1), |
|
95 (res_inst_tac [("x","iterator[dsucc[n]][smap[dsucc]][nats]")] exI 1), |
|
96 (res_inst_tac [("x","from[dsucc[n]]")] exI 1), |
|
97 (etac conjI 1), |
|
98 (rtac conjI 1), |
|
99 (rtac coind_lemma1 1), |
|
100 (rtac conjI 1), |
|
101 (rtac from 1), |
|
102 (res_inst_tac [("x","dsucc[n]")] exI 1), |
|
103 (fast_tac HOL_cs 1) |
|
104 ]); |
|
105 |
|
106 (* another proof using stream_coind_lemma2 *) |
|
107 |
|
108 val nats_eq_from = prove_goal Coind.thy "nats = from[dzero]" |
|
109 (fn prems => |
|
110 [ |
|
111 (res_inst_tac [("R","% p q.? n. p = \ |
|
112 \ iterator[n][smap[dsucc]][nats] & q = from[n]")] stream_coind 1), |
|
113 (rtac stream_coind_lemma2 1), |
|
114 (strip_tac 1), |
|
115 (etac exE 1), |
|
116 (res_inst_tac [("Q","n=UU")] classical2 1), |
|
117 (asm_simp_tac (HOLCF_ss addsimps coind_rews) 1), |
|
118 (res_inst_tac [("x","UU::dnat")] exI 1), |
|
119 (simp_tac (HOLCF_ss addsimps coind_rews addsimps stream_rews) 1), |
|
120 (etac conjE 1), |
|
121 (hyp_subst_tac 1), |
|
122 (hyp_subst_tac 1), |
|
123 (rtac conjI 1), |
|
124 (rtac (coind_lemma1 RS ssubst) 1), |
|
125 (rtac (from RS ssubst) 1), |
|
126 (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1), |
|
127 (res_inst_tac [("x","dsucc[n]")] exI 1), |
|
128 (rtac conjI 1), |
|
129 (rtac trans 1), |
|
130 (rtac (coind_lemma1 RS ssubst) 1), |
|
131 (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1), |
|
132 (rtac refl 1), |
|
133 (rtac trans 1), |
|
134 (rtac (from RS ssubst) 1), |
|
135 (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1), |
|
136 (rtac refl 1), |
|
137 (res_inst_tac [("x","dzero")] exI 1), |
|
138 (asm_simp_tac (HOLCF_ss addsimps coind_rews) 1) |
|
139 ]); |
|
140 |
|