--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Dagstuhl.ML Thu Mar 24 13:45:06 1994 +0100
@@ -0,0 +1,149 @@
+(*
+ 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();
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Dagstuhl.thy Thu Mar 24 13:45:06 1994 +0100
@@ -0,0 +1,17 @@
+(*
+ ID: $ $
+*)
+
+Dagstuhl = Stream2 +
+
+consts
+ YS :: "'a stream"
+ YYS :: "'a stream"
+
+rules
+
+YS_def "YS = fix[LAM x. scons[y][x]]"
+YYS_def "YYS = fix[LAM z. scons[y][scons[y][z]]]"
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/dagstuhl.ML Thu Mar 24 13:45:06 1994 +0100
@@ -0,0 +1,149 @@
+(*
+ 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();
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/dagstuhl.thy Thu Mar 24 13:45:06 1994 +0100
@@ -0,0 +1,17 @@
+(*
+ ID: $ $
+*)
+
+Dagstuhl = Stream2 +
+
+consts
+ YS :: "'a stream"
+ YYS :: "'a stream"
+
+rules
+
+YS_def "YS = fix[LAM x. scons[y][x]]"
+YYS_def "YYS = fix[LAM z. scons[y][scons[y][z]]]"
+
+end
+