src/HOLCF/ex/dagstuhl.ML

tuned;
prepare ext;

(*
    ID: $ $
*)


open Dagstuhl;

val YS_def2  = fix_prover Dagstuhl.thy  YS_def  "YS  = scons[y][YS]";
val YYS_def2 = fix_prover Dagstuhl.thy YYS_def "YYS = scons[y][scons[y][YYS]]";


val prems = goal Dagstuhl.thy "YYS << scons[y][YYS]";
by (rtac (YYS_def RS ssubst) 1);
by (rtac fix_ind 1);
by (resolve_tac adm_thms 1);
by (contX_tacR 1);
by (rtac minimal 1);
by (rtac (beta_cfun RS ssubst) 1);
by (contX_tacR 1);
by (rtac monofun_cfun_arg 1);
by (rtac monofun_cfun_arg 1);
by (atac 1);
val lemma3 = result();

val prems = goal Dagstuhl.thy "scons[y][YYS] << YYS";
by (rtac (YYS_def2 RS ssubst) 1);
back();
by (rtac monofun_cfun_arg 1);
by (rtac lemma3 1);
val lemma4 = result();

(* val  lemma5 = lemma3 RS (lemma4 RS antisym_less) *)

val prems = goal Dagstuhl.thy "scons[y][YYS] = YYS";
by (rtac antisym_less 1);
by (rtac lemma4 1);
by (rtac lemma3 1);
val lemma5 = result();

val prems = goal Dagstuhl.thy "YS = YYS";
by (rtac stream_take_lemma 1);
by (nat_ind_tac "n" 1);
by (simp_tac (HOLCF_ss addsimps stream_rews) 1);
by (res_inst_tac [("y1","y")] (YS_def2 RS ssubst) 1);
by (res_inst_tac [("y1","y")] (YYS_def2 RS ssubst) 1);
by (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1);
by (rtac (lemma5 RS sym RS subst) 1);
by (rtac refl 1);
val wir_moel = result();

(* ------------------------------------------------------------------------ *)
(* Zweite L"osung: Bernhard M"oller                                         *)
(* statt Beweis von  wir_moel "uber take_lemma beidseitige Inclusion        *)
(* verwendet lemma5                                                         *)
(* ------------------------------------------------------------------------ *)

val prems = goal Dagstuhl.thy "YYS << YS";
by (rtac (YYS_def RS ssubst) 1);
by (rtac fix_least 1);
by (rtac (beta_cfun RS ssubst) 1);
by (contX_tacR 1);
by (simp_tac (HOLCF_ss addsimps [YS_def2 RS sym]) 1);
val lemma6 = result();

val prems = goal Dagstuhl.thy "YS << YYS";
by (rtac (YS_def RS ssubst) 1);
by (rtac fix_ind 1);
by (resolve_tac adm_thms 1);
by (contX_tacR 1);
by (rtac minimal 1);
by (rtac (beta_cfun RS ssubst) 1);
by (contX_tacR 1);
by (res_inst_tac [("y2","y10")] (lemma5 RS sym RS ssubst) 1);
by (etac monofun_cfun_arg 1);
val lemma7 = result();

val  wir_moel = lemma6 RS (lemma7 RS antisym_less);


(* ------------------------------------------------------------------------ *)
(* L"osung aus Dagstuhl (F.R.)                                              *)
(* Wie oben, jedoch ohne Konstantendefinition f"ur YS, YYS                  *)
(* ------------------------------------------------------------------------ *)

val prems = goal Stream2.thy
    "(fix[LAM x. scons[y][x]]) = scons[y][fix[LAM x. scons[y][x]]]";
by (rtac (fix_eq RS ssubst) 1);
back();
back();
by (rtac (beta_cfun RS ssubst) 1);
by (contX_tacR 1);
by (rtac refl 1);
val lemma1 = result();

val prems = goal Stream2.thy
    "(fix[ LAM z. scons[y][scons[y][z]]]) = \
\     scons[y][scons[y][(fix[ LAM z. scons[y][scons[y][z]]])]]";
by (rtac (fix_eq RS ssubst) 1);
back();
back();
by (rtac (beta_cfun RS ssubst) 1);
by (contX_tacR 1);
by (rtac refl 1);
val lemma2 = result();

val prems = goal Stream2.thy
"fix[LAM z. scons[y][scons[y][z]]] << \
\ scons[y][fix[LAM z. scons[y][scons[y][z]]]]";
by (rtac fix_ind 1);
by (resolve_tac adm_thms 1);
by (contX_tacR 1);
by (rtac minimal 1);
by (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1);
by (rtac monofun_cfun_arg 1);
by (rtac monofun_cfun_arg 1);
by (atac 1);
val lemma3 = result();

val prems = goal Stream2.thy
" scons[y][fix[LAM z. scons[y][scons[y][z]]]] <<\
\ fix[LAM z. scons[y][scons[y][z]]]";
by (rtac (lemma2 RS ssubst) 1);
back();
by (rtac monofun_cfun_arg 1);
by (rtac lemma3 1);
val lemma4 = result();

val prems = goal Stream2.thy
" scons[y][fix[LAM z. scons[y][scons[y][z]]]] =\
\ fix[LAM z. scons[y][scons[y][z]]]";
by (rtac antisym_less 1);
by (rtac lemma4 1);
by (rtac lemma3 1);
val lemma5 = result();

val prems = goal Stream2.thy
    "(fix[LAM x. scons[y][x]]) = (fix[ LAM z. scons[y][scons[y][z]]])";
by (rtac stream_take_lemma 1);
by (nat_ind_tac "n" 1);
by (simp_tac (HOLCF_ss addsimps stream_rews) 1);
by (rtac (lemma1 RS ssubst) 1);
by (rtac (lemma2 RS ssubst) 1);
by (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1);
by (rtac (lemma5 RS sym RS subst) 1);
by (rtac refl 1);
val wir_moel = result();