# HG changeset patch
# User nipkow
# Date 764513106 -3600
# Node ID febeb36a4ba4aea9d7fd30a1bd9c73704ba8e787
# Parent  3a0485439396c4730ee99b86bfe76770357079e0
Franz fragen

diff -r 3a0485439396 -r febeb36a4ba4 src/HOLCF/ex/Dagstuhl.ML
--- /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();
+
+
+
diff -r 3a0485439396 -r febeb36a4ba4 src/HOLCF/ex/Dagstuhl.thy
--- /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
+
diff -r 3a0485439396 -r febeb36a4ba4 src/HOLCF/ex/dagstuhl.ML
--- /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();
+
+
+
diff -r 3a0485439396 -r febeb36a4ba4 src/HOLCF/ex/dagstuhl.thy
--- /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
+