equal
deleted
inserted
replaced
17 |
17 |
18 definition games_gfp :: "ZF set" where |
18 definition games_gfp :: "ZF set" where |
19 "games_gfp \<equiv> gfp fixgames" |
19 "games_gfp \<equiv> gfp fixgames" |
20 |
20 |
21 lemma mono_fixgames: "mono (fixgames)" |
21 lemma mono_fixgames: "mono (fixgames)" |
22 apply (auto simp add: mono_def fixgames_def) |
22 by (auto simp add: mono_def fixgames_def) |
23 apply (rule_tac x=l in exI) |
|
24 apply (rule_tac x=r in exI) |
|
25 apply auto |
|
26 done |
|
27 |
23 |
28 lemma games_lfp_unfold: "games_lfp = fixgames games_lfp" |
24 lemma games_lfp_unfold: "games_lfp = fixgames games_lfp" |
29 by (auto simp add: def_lfp_unfold games_lfp_def mono_fixgames) |
25 by (auto simp add: def_lfp_unfold games_lfp_def mono_fixgames) |
30 |
26 |
31 lemma games_gfp_unfold: "games_gfp = fixgames games_gfp" |
27 lemma games_gfp_unfold: "games_gfp = fixgames games_gfp" |
972 done |
968 done |
973 } |
969 } |
974 qed |
970 qed |
975 |
971 |
976 end |
972 end |
|
973 |