author | clasohm |
Wed, 04 Oct 1995 14:01:44 +0100 | |
changeset 1267 | bca91b4e1710 |
parent 1168 | 74be52691d62 |
permissions | -rw-r--r-- |
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 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
14 |
val nats_def2 = fix_prover2 Coind.thy nats_def |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
15 |
"nats = scons`dzero`(smap`dsucc`nats)"; |
244 | 16 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
17 |
val from_def2 = fix_prover2 Coind.thy from_def |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
18 |
"from = (LAM n.scons`n`(from`(dsucc`n)))"; |
244 | 19 |
|
20 |
||
21 |
||
22 |
(* ------------------------------------------------------------------------- *) |
|
23 |
(* recursive properties *) |
|
24 |
(* ------------------------------------------------------------------------- *) |
|
25 |
||
26 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
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), |
|
1267 | 32 |
(Simp_tac 1), |
244 | 33 |
(rtac refl 1) |
34 |
]); |
|
35 |
||
36 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
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 *) |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
52 |
(* prove: nats = from`dzero *) |
244 | 53 |
(* ------------------------------------------------------------------------- *) |
54 |
||
55 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
56 |
val coind_lemma1 = prove_goal Coind.thy "iterator`n`(smap`dsucc)`nats =\ |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
57 |
\ scons`n`(iterator`(dsucc`n)`(smap`dsucc)`nats)" |
244 | 58 |
(fn prems => |
59 |
[ |
|
297 | 60 |
(res_inst_tac [("s","n")] dnat_ind 1), |
1267 | 61 |
(simp_tac (!simpset addsimps (coind_rews @ stream_rews)) 1), |
62 |
(simp_tac (!simpset addsimps (coind_rews @ stream_rews)) 1), |
|
244 | 63 |
(rtac trans 1), |
64 |
(rtac nats_def2 1), |
|
1267 | 65 |
(simp_tac (!simpset addsimps (coind_rews @ dnat_rews)) 1), |
244 | 66 |
(rtac trans 1), |
67 |
(etac iterator3 1), |
|
68 |
(rtac trans 1), |
|
1267 | 69 |
(Asm_simp_tac 1), |
244 | 70 |
(rtac trans 1), |
71 |
(etac smap2 1), |
|
72 |
(rtac cfun_arg_cong 1), |
|
1267 | 73 |
(asm_simp_tac (!simpset addsimps ([iterator3 RS sym] @ dnat_rews)) 1) |
244 | 74 |
]); |
75 |
||
76 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
77 |
val nats_eq_from = prove_goal Coind.thy "nats = from`dzero" |
244 | 78 |
(fn prems => |
79 |
[ |
|
80 |
(res_inst_tac [("R", |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
81 |
"% p q.? n. p = iterator`n`(smap`dsucc)`nats & q = from`n")] stream_coind 1), |
244 | 82 |
(res_inst_tac [("x","dzero")] exI 2), |
1267 | 83 |
(asm_simp_tac (!simpset addsimps coind_rews) 2), |
244 | 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), |
|
1267 | 89 |
(asm_simp_tac (!simpset addsimps coind_rews) 1), |
244 | 90 |
(rtac disjI2 1), |
91 |
(etac conjE 1), |
|
92 |
(hyp_subst_tac 1), |
|
93 |
(res_inst_tac [("x","n")] exI 1), |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
94 |
(res_inst_tac [("x","iterator`(dsucc`n)`(smap`dsucc)`nats")] exI 1), |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
95 |
(res_inst_tac [("x","from`(dsucc`n)")] exI 1), |
244 | 96 |
(etac conjI 1), |
97 |
(rtac conjI 1), |
|
98 |
(rtac coind_lemma1 1), |
|
99 |
(rtac conjI 1), |
|
100 |
(rtac from 1), |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
101 |
(res_inst_tac [("x","dsucc`n")] exI 1), |
244 | 102 |
(fast_tac HOL_cs 1) |
103 |
]); |
|
104 |
||
105 |
(* another proof using stream_coind_lemma2 *) |
|
106 |
||
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
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 = \ |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
111 |
\ iterator`n`(smap`dsucc)`nats & q = from`n")] stream_coind 1), |
244 | 112 |
(rtac stream_coind_lemma2 1), |
113 |
(strip_tac 1), |
|
114 |
(etac exE 1), |
|
115 |
(res_inst_tac [("Q","n=UU")] classical2 1), |
|
1267 | 116 |
(asm_simp_tac (!simpset addsimps coind_rews) 1), |
244 | 117 |
(res_inst_tac [("x","UU::dnat")] exI 1), |
1267 | 118 |
(simp_tac (!simpset addsimps coind_rews addsimps stream_rews) 1), |
244 | 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), |
|
1267 | 124 |
(asm_simp_tac (!simpset addsimps stream_rews) 1), |
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
1043
diff
changeset
|
125 |
(res_inst_tac [("x","dsucc`n")] exI 1), |
244 | 126 |
(rtac conjI 1), |
127 |
(rtac trans 1), |
|
128 |
(rtac (coind_lemma1 RS ssubst) 1), |
|
1267 | 129 |
(asm_simp_tac (!simpset addsimps stream_rews) 1), |
244 | 130 |
(rtac refl 1), |
131 |
(rtac trans 1), |
|
132 |
(rtac (from RS ssubst) 1), |
|
1267 | 133 |
(asm_simp_tac (!simpset addsimps stream_rews) 1), |
244 | 134 |
(rtac refl 1), |
135 |
(res_inst_tac [("x","dzero")] exI 1), |
|
1267 | 136 |
(asm_simp_tac (!simpset addsimps coind_rews) 1) |
244 | 137 |
]); |
138 |