71 |
71 |
72 (*** Even Stronger version of coinduct [by Martin Coen] |
72 (*** Even Stronger version of coinduct [by Martin Coen] |
73 - instead of the condition X <= f(X) |
73 - instead of the condition X <= f(X) |
74 consider X <= (f(X) Un f(f(X)) ...) Un gfp(X) ***) |
74 consider X <= (f(X) Un f(f(X)) ...) Un gfp(X) ***) |
75 |
75 |
76 val [prem] = goal Gfp.thy "mono(f) ==> mono(%x.f(x) Un X Un B)"; |
76 val [prem] = goal Gfp.thy "mono(f) ==> mono(%x. f(x) Un X Un B)"; |
77 by (REPEAT (ares_tac [subset_refl, monoI, Un_mono, prem RS monoD] 1)); |
77 by (REPEAT (ares_tac [subset_refl, monoI, Un_mono, prem RS monoD] 1)); |
78 qed "coinduct3_mono_lemma"; |
78 qed "coinduct3_mono_lemma"; |
79 |
79 |
80 val [prem,mono] = goal Gfp.thy |
80 val [prem,mono] = goal Gfp.thy |
81 "[| X <= f(lfp(%x.f(x) Un X Un gfp(f))); mono(f) |] ==> \ |
81 "[| X <= f(lfp(%x. f(x) Un X Un gfp(f))); mono(f) |] ==> \ |
82 \ lfp(%x.f(x) Un X Un gfp(f)) <= f(lfp(%x.f(x) Un X Un gfp(f)))"; |
82 \ lfp(%x. f(x) Un X Un gfp(f)) <= f(lfp(%x. f(x) Un X Un gfp(f)))"; |
83 by (rtac subset_trans 1); |
83 by (rtac subset_trans 1); |
84 by (rtac (mono RS coinduct3_mono_lemma RS lfp_lemma3) 1); |
84 by (rtac (mono RS coinduct3_mono_lemma RS lfp_lemma3) 1); |
85 by (rtac (Un_least RS Un_least) 1); |
85 by (rtac (Un_least RS Un_least) 1); |
86 by (rtac subset_refl 1); |
86 by (rtac subset_refl 1); |
87 by (rtac prem 1); |
87 by (rtac prem 1); |
90 by (stac (mono RS coinduct3_mono_lemma RS lfp_Tarski) 1); |
90 by (stac (mono RS coinduct3_mono_lemma RS lfp_Tarski) 1); |
91 by (rtac Un_upper2 1); |
91 by (rtac Un_upper2 1); |
92 qed "coinduct3_lemma"; |
92 qed "coinduct3_lemma"; |
93 |
93 |
94 val prems = goal Gfp.thy |
94 val prems = goal Gfp.thy |
95 "[| mono(f); a:X; X <= f(lfp(%x.f(x) Un X Un gfp(f))) |] ==> a : gfp(f)"; |
95 "[| mono(f); a:X; X <= f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)"; |
96 by (rtac (coinduct3_lemma RSN (2,weak_coinduct)) 1); |
96 by (rtac (coinduct3_lemma RSN (2,weak_coinduct)) 1); |
97 by (resolve_tac (prems RL [coinduct3_mono_lemma RS lfp_Tarski RS ssubst]) 1); |
97 by (resolve_tac (prems RL [coinduct3_mono_lemma RS lfp_Tarski RS ssubst]) 1); |
98 by (rtac (UnI2 RS UnI1) 1); |
98 by (rtac (UnI2 RS UnI1) 1); |
99 by (REPEAT (resolve_tac prems 1)); |
99 by (REPEAT (resolve_tac prems 1)); |
100 qed "coinduct3"; |
100 qed "coinduct3"; |
121 by (rtac def_coinduct 1); |
121 by (rtac def_coinduct 1); |
122 by (REPEAT (ares_tac (prems @ [subsetI,CollectI]) 1)); |
122 by (REPEAT (ares_tac (prems @ [subsetI,CollectI]) 1)); |
123 qed "def_Collect_coinduct"; |
123 qed "def_Collect_coinduct"; |
124 |
124 |
125 val rew::prems = goal Gfp.thy |
125 val rew::prems = goal Gfp.thy |
126 "[| A==gfp(f); mono(f); a:X; X <= f(lfp(%x.f(x) Un X Un A)) |] ==> a: A"; |
126 "[| A==gfp(f); mono(f); a:X; X <= f(lfp(%x. f(x) Un X Un A)) |] ==> a: A"; |
127 by (rewtac rew); |
127 by (rewtac rew); |
128 by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct3]) 1)); |
128 by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct3]) 1)); |
129 qed "def_coinduct3"; |
129 qed "def_coinduct3"; |
130 |
130 |
131 (*Monotonicity of gfp!*) |
131 (*Monotonicity of gfp!*) |