9 (* ------------------------------------------------------------------------- *) |
9 (* ------------------------------------------------------------------------- *) |
10 (* expand fixed point properties *) |
10 (* expand fixed point properties *) |
11 (* ------------------------------------------------------------------------- *) |
11 (* ------------------------------------------------------------------------- *) |
12 |
12 |
13 |
13 |
14 val nats_def2 = fix_prover Coind.thy nats_def |
14 val nats_def2 = fix_prover2 Coind.thy nats_def |
15 "nats = scons[dzero][smap[dsucc][nats]]"; |
15 "nats = scons`dzero`(smap`dsucc`nats)"; |
16 |
16 |
17 val from_def2 = fix_prover Coind.thy from_def |
17 val from_def2 = fix_prover2 Coind.thy from_def |
18 "from = (LAM n.scons[n][from[dsucc[n]]])"; |
18 "from = (LAM n.scons`n`(from`(dsucc`n)))"; |
19 |
19 |
20 |
20 |
21 |
21 |
22 (* ------------------------------------------------------------------------- *) |
22 (* ------------------------------------------------------------------------- *) |
23 (* recursive properties *) |
23 (* recursive properties *) |
24 (* ------------------------------------------------------------------------- *) |
24 (* ------------------------------------------------------------------------- *) |
25 |
25 |
26 |
26 |
27 val from = prove_goal Coind.thy "from[n] = scons[n][from[dsucc[n]]]" |
27 val from = prove_goal Coind.thy "from`n = scons`n`(from`(dsucc`n))" |
28 (fn prems => |
28 (fn prems => |
29 [ |
29 [ |
30 (rtac trans 1), |
30 (rtac trans 1), |
31 (rtac (from_def2 RS ssubst) 1), |
31 (rtac (from_def2 RS ssubst) 1), |
32 (simp_tac HOLCF_ss 1), |
32 (simp_tac HOLCF_ss 1), |
33 (rtac refl 1) |
33 (rtac refl 1) |
34 ]); |
34 ]); |
35 |
35 |
36 |
36 |
37 val from1 = prove_goal Coind.thy "from[UU] = UU" |
37 val from1 = prove_goal Coind.thy "from`UU = UU" |
38 (fn prems => |
38 (fn prems => |
39 [ |
39 [ |
40 (rtac trans 1), |
40 (rtac trans 1), |
41 (rtac (from RS ssubst) 1), |
41 (rtac (from RS ssubst) 1), |
42 (resolve_tac stream_constrdef 1), |
42 (resolve_tac stream_constrdef 1), |
47 [iterator1, iterator2, iterator3, smap1, smap2,from1]; |
47 [iterator1, iterator2, iterator3, smap1, smap2,from1]; |
48 |
48 |
49 |
49 |
50 (* ------------------------------------------------------------------------- *) |
50 (* ------------------------------------------------------------------------- *) |
51 (* the example *) |
51 (* the example *) |
52 (* prove: nats = from[dzero] *) |
52 (* prove: nats = from`dzero *) |
53 (* ------------------------------------------------------------------------- *) |
53 (* ------------------------------------------------------------------------- *) |
54 |
54 |
55 |
55 |
56 val coind_lemma1 = prove_goal Coind.thy "iterator[n][smap[dsucc]][nats] =\ |
56 val coind_lemma1 = prove_goal Coind.thy "iterator`n`(smap`dsucc)`nats =\ |
57 \ scons[n][iterator[dsucc[n]][smap[dsucc]][nats]]" |
57 \ scons`n`(iterator`(dsucc`n)`(smap`dsucc)`nats)" |
58 (fn prems => |
58 (fn prems => |
59 [ |
59 [ |
60 (res_inst_tac [("s","n")] dnat_ind 1), |
60 (res_inst_tac [("s","n")] dnat_ind 1), |
61 (simp_tac (HOLCF_ss addsimps (coind_rews @ stream_rews)) 1), |
61 (simp_tac (HOLCF_ss addsimps (coind_rews @ stream_rews)) 1), |
62 (simp_tac (HOLCF_ss addsimps (coind_rews @ stream_rews)) 1), |
62 (simp_tac (HOLCF_ss addsimps (coind_rews @ stream_rews)) 1), |
72 (rtac cfun_arg_cong 1), |
72 (rtac cfun_arg_cong 1), |
73 (asm_simp_tac (HOLCF_ss addsimps ([iterator3 RS sym] @ dnat_rews)) 1) |
73 (asm_simp_tac (HOLCF_ss addsimps ([iterator3 RS sym] @ dnat_rews)) 1) |
74 ]); |
74 ]); |
75 |
75 |
76 |
76 |
77 val nats_eq_from = prove_goal Coind.thy "nats = from[dzero]" |
77 val nats_eq_from = prove_goal Coind.thy "nats = from`dzero" |
78 (fn prems => |
78 (fn prems => |
79 [ |
79 [ |
80 (res_inst_tac [("R", |
80 (res_inst_tac [("R", |
81 "% p q.? n. p = iterator[n][smap[dsucc]][nats] & q = from[n]")] stream_coind 1), |
81 "% p q.? n. p = iterator`n`(smap`dsucc)`nats & q = from`n")] stream_coind 1), |
82 (res_inst_tac [("x","dzero")] exI 2), |
82 (res_inst_tac [("x","dzero")] exI 2), |
83 (asm_simp_tac (HOLCF_ss addsimps coind_rews) 2), |
83 (asm_simp_tac (HOLCF_ss addsimps coind_rews) 2), |
84 (rewrite_goals_tac [stream_bisim_def]), |
84 (rewrite_goals_tac [stream_bisim_def]), |
85 (strip_tac 1), |
85 (strip_tac 1), |
86 (etac exE 1), |
86 (etac exE 1), |
89 (asm_simp_tac (HOLCF_ss addsimps coind_rews) 1), |
89 (asm_simp_tac (HOLCF_ss addsimps coind_rews) 1), |
90 (rtac disjI2 1), |
90 (rtac disjI2 1), |
91 (etac conjE 1), |
91 (etac conjE 1), |
92 (hyp_subst_tac 1), |
92 (hyp_subst_tac 1), |
93 (res_inst_tac [("x","n")] exI 1), |
93 (res_inst_tac [("x","n")] exI 1), |
94 (res_inst_tac [("x","iterator[dsucc[n]][smap[dsucc]][nats]")] 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), |
95 (res_inst_tac [("x","from`(dsucc`n)")] exI 1), |
96 (etac conjI 1), |
96 (etac conjI 1), |
97 (rtac conjI 1), |
97 (rtac conjI 1), |
98 (rtac coind_lemma1 1), |
98 (rtac coind_lemma1 1), |
99 (rtac conjI 1), |
99 (rtac conjI 1), |
100 (rtac from 1), |
100 (rtac from 1), |
101 (res_inst_tac [("x","dsucc[n]")] exI 1), |
101 (res_inst_tac [("x","dsucc`n")] exI 1), |
102 (fast_tac HOL_cs 1) |
102 (fast_tac HOL_cs 1) |
103 ]); |
103 ]); |
104 |
104 |
105 (* another proof using stream_coind_lemma2 *) |
105 (* another proof using stream_coind_lemma2 *) |
106 |
106 |
107 val nats_eq_from = prove_goal Coind.thy "nats = from[dzero]" |
107 val nats_eq_from = prove_goal Coind.thy "nats = from`dzero" |
108 (fn prems => |
108 (fn prems => |
109 [ |
109 [ |
110 (res_inst_tac [("R","% p q.? n. p = \ |
110 (res_inst_tac [("R","% p q.? n. p = \ |
111 \ iterator[n][smap[dsucc]][nats] & q = from[n]")] stream_coind 1), |
111 \ iterator`n`(smap`dsucc)`nats & q = from`n")] stream_coind 1), |
112 (rtac stream_coind_lemma2 1), |
112 (rtac stream_coind_lemma2 1), |
113 (strip_tac 1), |
113 (strip_tac 1), |
114 (etac exE 1), |
114 (etac exE 1), |
115 (res_inst_tac [("Q","n=UU")] classical2 1), |
115 (res_inst_tac [("Q","n=UU")] classical2 1), |
116 (asm_simp_tac (HOLCF_ss addsimps coind_rews) 1), |
116 (asm_simp_tac (HOLCF_ss addsimps coind_rews) 1), |
120 (hyp_subst_tac 1), |
120 (hyp_subst_tac 1), |
121 (rtac conjI 1), |
121 (rtac conjI 1), |
122 (rtac (coind_lemma1 RS ssubst) 1), |
122 (rtac (coind_lemma1 RS ssubst) 1), |
123 (rtac (from RS ssubst) 1), |
123 (rtac (from RS ssubst) 1), |
124 (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1), |
124 (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1), |
125 (res_inst_tac [("x","dsucc[n]")] exI 1), |
125 (res_inst_tac [("x","dsucc`n")] exI 1), |
126 (rtac conjI 1), |
126 (rtac conjI 1), |
127 (rtac trans 1), |
127 (rtac trans 1), |
128 (rtac (coind_lemma1 RS ssubst) 1), |
128 (rtac (coind_lemma1 RS ssubst) 1), |
129 (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1), |
129 (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1), |
130 (rtac refl 1), |
130 (rtac refl 1), |