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_prover2 Coind.thy nats_def |
|
15 "nats = scons`dzero`(smap`dsucc`nats)"; |
|
16 |
|
17 val from_def2 = fix_prover2 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 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 (!simpset addsimps (coind_rews @ stream_rews)) 1), |
|
62 (simp_tac (!simpset addsimps (coind_rews @ stream_rews)) 1), |
|
63 (rtac trans 1), |
|
64 (rtac nats_def2 1), |
|
65 (simp_tac (!simpset addsimps (coind_rews @ dnat_rews)) 1), |
|
66 (rtac trans 1), |
|
67 (etac iterator3 1), |
|
68 (rtac trans 1), |
|
69 (Asm_simp_tac 1), |
|
70 (rtac trans 1), |
|
71 (etac smap2 1), |
|
72 (rtac cfun_arg_cong 1), |
|
73 (asm_simp_tac (!simpset 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 (!simpset 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 (!simpset 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 |
|
107 val nats_eq_from = prove_goal Coind.thy "nats = from`dzero" |
|
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 (!simpset addsimps coind_rews) 1), |
|
117 (res_inst_tac [("x","UU::dnat")] exI 1), |
|
118 (simp_tac (!simpset 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 (!simpset 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 (!simpset addsimps stream_rews) 1), |
|
130 (rtac refl 1), |
|
131 (rtac trans 1), |
|
132 (rtac (from RS ssubst) 1), |
|
133 (asm_simp_tac (!simpset addsimps stream_rews) 1), |
|
134 (rtac refl 1), |
|
135 (res_inst_tac [("x","dzero")] exI 1), |
|
136 (asm_simp_tac (!simpset addsimps coind_rews) 1) |
|
137 ]); |
|
138 |
|