src/HOLCF/ex/Dagstuhl.ML
changeset 892 d0dc8d057929
parent 299 febeb36a4ba4
child 895 7a1e07fbffea
equal deleted inserted replaced
891:a5ad535a241a 892:d0dc8d057929
    18 by (rtac (beta_cfun RS ssubst) 1);
    18 by (rtac (beta_cfun RS ssubst) 1);
    19 by (contX_tacR 1);
    19 by (contX_tacR 1);
    20 by (rtac monofun_cfun_arg 1);
    20 by (rtac monofun_cfun_arg 1);
    21 by (rtac monofun_cfun_arg 1);
    21 by (rtac monofun_cfun_arg 1);
    22 by (atac 1);
    22 by (atac 1);
    23 val lemma3 = result();
    23 qed "lemma3";
    24 
    24 
    25 val prems = goal Dagstuhl.thy "scons[y][YYS] << YYS";
    25 val prems = goal Dagstuhl.thy "scons[y][YYS] << YYS";
    26 by (rtac (YYS_def2 RS ssubst) 1);
    26 by (rtac (YYS_def2 RS ssubst) 1);
    27 back();
    27 back();
    28 by (rtac monofun_cfun_arg 1);
    28 by (rtac monofun_cfun_arg 1);
    29 by (rtac lemma3 1);
    29 by (rtac lemma3 1);
    30 val lemma4 = result();
    30 qed "lemma4";
    31 
    31 
    32 (* val  lemma5 = lemma3 RS (lemma4 RS antisym_less) *)
    32 (* val  lemma5 = lemma3 RS (lemma4 RS antisym_less) *)
    33 
    33 
    34 val prems = goal Dagstuhl.thy "scons[y][YYS] = YYS";
    34 val prems = goal Dagstuhl.thy "scons[y][YYS] = YYS";
    35 by (rtac antisym_less 1);
    35 by (rtac antisym_less 1);
    36 by (rtac lemma4 1);
    36 by (rtac lemma4 1);
    37 by (rtac lemma3 1);
    37 by (rtac lemma3 1);
    38 val lemma5 = result();
    38 qed "lemma5";
    39 
    39 
    40 val prems = goal Dagstuhl.thy "YS = YYS";
    40 val prems = goal Dagstuhl.thy "YS = YYS";
    41 by (rtac stream_take_lemma 1);
    41 by (rtac stream_take_lemma 1);
    42 by (nat_ind_tac "n" 1);
    42 by (nat_ind_tac "n" 1);
    43 by (simp_tac (HOLCF_ss addsimps stream_rews) 1);
    43 by (simp_tac (HOLCF_ss addsimps stream_rews) 1);
    44 by (res_inst_tac [("y1","y")] (YS_def2 RS ssubst) 1);
    44 by (res_inst_tac [("y1","y")] (YS_def2 RS ssubst) 1);
    45 by (res_inst_tac [("y1","y")] (YYS_def2 RS ssubst) 1);
    45 by (res_inst_tac [("y1","y")] (YYS_def2 RS ssubst) 1);
    46 by (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1);
    46 by (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1);
    47 by (rtac (lemma5 RS sym RS subst) 1);
    47 by (rtac (lemma5 RS sym RS subst) 1);
    48 by (rtac refl 1);
    48 by (rtac refl 1);
    49 val wir_moel = result();
    49 qed "wir_moel";
    50 
    50 
    51 (* ------------------------------------------------------------------------ *)
    51 (* ------------------------------------------------------------------------ *)
    52 (* Zweite L"osung: Bernhard M"oller                                         *)
    52 (* Zweite L"osung: Bernhard M"oller                                         *)
    53 (* statt Beweis von  wir_moel "uber take_lemma beidseitige Inclusion        *)
    53 (* statt Beweis von  wir_moel "uber take_lemma beidseitige Inclusion        *)
    54 (* verwendet lemma5                                                         *)
    54 (* verwendet lemma5                                                         *)
    58 by (rtac (YYS_def RS ssubst) 1);
    58 by (rtac (YYS_def RS ssubst) 1);
    59 by (rtac fix_least 1);
    59 by (rtac fix_least 1);
    60 by (rtac (beta_cfun RS ssubst) 1);
    60 by (rtac (beta_cfun RS ssubst) 1);
    61 by (contX_tacR 1);
    61 by (contX_tacR 1);
    62 by (simp_tac (HOLCF_ss addsimps [YS_def2 RS sym]) 1);
    62 by (simp_tac (HOLCF_ss addsimps [YS_def2 RS sym]) 1);
    63 val lemma6 = result();
    63 qed "lemma6";
    64 
    64 
    65 val prems = goal Dagstuhl.thy "YS << YYS";
    65 val prems = goal Dagstuhl.thy "YS << YYS";
    66 by (rtac (YS_def RS ssubst) 1);
    66 by (rtac (YS_def RS ssubst) 1);
    67 by (rtac fix_ind 1);
    67 by (rtac fix_ind 1);
    68 by (resolve_tac adm_thms 1);
    68 by (resolve_tac adm_thms 1);
    70 by (rtac minimal 1);
    70 by (rtac minimal 1);
    71 by (rtac (beta_cfun RS ssubst) 1);
    71 by (rtac (beta_cfun RS ssubst) 1);
    72 by (contX_tacR 1);
    72 by (contX_tacR 1);
    73 by (res_inst_tac [("y2","y10")] (lemma5 RS sym RS ssubst) 1);
    73 by (res_inst_tac [("y2","y10")] (lemma5 RS sym RS ssubst) 1);
    74 by (etac monofun_cfun_arg 1);
    74 by (etac monofun_cfun_arg 1);
    75 val lemma7 = result();
    75 qed "lemma7";
    76 
    76 
    77 val  wir_moel = lemma6 RS (lemma7 RS antisym_less);
    77 val  wir_moel = lemma6 RS (lemma7 RS antisym_less);
    78 
    78 
    79 
    79 
    80 (* ------------------------------------------------------------------------ *)
    80 (* ------------------------------------------------------------------------ *)
    88 back();
    88 back();
    89 back();
    89 back();
    90 by (rtac (beta_cfun RS ssubst) 1);
    90 by (rtac (beta_cfun RS ssubst) 1);
    91 by (contX_tacR 1);
    91 by (contX_tacR 1);
    92 by (rtac refl 1);
    92 by (rtac refl 1);
    93 val lemma1 = result();
    93 qed "lemma1";
    94 
    94 
    95 val prems = goal Stream2.thy
    95 val prems = goal Stream2.thy
    96     "(fix[ LAM z. scons[y][scons[y][z]]]) = \
    96     "(fix[ LAM z. scons[y][scons[y][z]]]) = \
    97 \     scons[y][scons[y][(fix[ LAM z. scons[y][scons[y][z]]])]]";
    97 \     scons[y][scons[y][(fix[ LAM z. scons[y][scons[y][z]]])]]";
    98 by (rtac (fix_eq RS ssubst) 1);
    98 by (rtac (fix_eq RS ssubst) 1);
    99 back();
    99 back();
   100 back();
   100 back();
   101 by (rtac (beta_cfun RS ssubst) 1);
   101 by (rtac (beta_cfun RS ssubst) 1);
   102 by (contX_tacR 1);
   102 by (contX_tacR 1);
   103 by (rtac refl 1);
   103 by (rtac refl 1);
   104 val lemma2 = result();
   104 qed "lemma2";
   105 
   105 
   106 val prems = goal Stream2.thy
   106 val prems = goal Stream2.thy
   107 "fix[LAM z. scons[y][scons[y][z]]] << \
   107 "fix[LAM z. scons[y][scons[y][z]]] << \
   108 \ scons[y][fix[LAM z. scons[y][scons[y][z]]]]";
   108 \ scons[y][fix[LAM z. scons[y][scons[y][z]]]]";
   109 by (rtac fix_ind 1);
   109 by (rtac fix_ind 1);
   112 by (rtac minimal 1);
   112 by (rtac minimal 1);
   113 by (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1);
   113 by (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1);
   114 by (rtac monofun_cfun_arg 1);
   114 by (rtac monofun_cfun_arg 1);
   115 by (rtac monofun_cfun_arg 1);
   115 by (rtac monofun_cfun_arg 1);
   116 by (atac 1);
   116 by (atac 1);
   117 val lemma3 = result();
   117 qed "lemma3";
   118 
   118 
   119 val prems = goal Stream2.thy
   119 val prems = goal Stream2.thy
   120 " scons[y][fix[LAM z. scons[y][scons[y][z]]]] <<\
   120 " scons[y][fix[LAM z. scons[y][scons[y][z]]]] <<\
   121 \ fix[LAM z. scons[y][scons[y][z]]]";
   121 \ fix[LAM z. scons[y][scons[y][z]]]";
   122 by (rtac (lemma2 RS ssubst) 1);
   122 by (rtac (lemma2 RS ssubst) 1);
   123 back();
   123 back();
   124 by (rtac monofun_cfun_arg 1);
   124 by (rtac monofun_cfun_arg 1);
   125 by (rtac lemma3 1);
   125 by (rtac lemma3 1);
   126 val lemma4 = result();
   126 qed "lemma4";
   127 
   127 
   128 val prems = goal Stream2.thy
   128 val prems = goal Stream2.thy
   129 " scons[y][fix[LAM z. scons[y][scons[y][z]]]] =\
   129 " scons[y][fix[LAM z. scons[y][scons[y][z]]]] =\
   130 \ fix[LAM z. scons[y][scons[y][z]]]";
   130 \ fix[LAM z. scons[y][scons[y][z]]]";
   131 by (rtac antisym_less 1);
   131 by (rtac antisym_less 1);
   132 by (rtac lemma4 1);
   132 by (rtac lemma4 1);
   133 by (rtac lemma3 1);
   133 by (rtac lemma3 1);
   134 val lemma5 = result();
   134 qed "lemma5";
   135 
   135 
   136 val prems = goal Stream2.thy
   136 val prems = goal Stream2.thy
   137     "(fix[LAM x. scons[y][x]]) = (fix[ LAM z. scons[y][scons[y][z]]])";
   137     "(fix[LAM x. scons[y][x]]) = (fix[ LAM z. scons[y][scons[y][z]]])";
   138 by (rtac stream_take_lemma 1);
   138 by (rtac stream_take_lemma 1);
   139 by (nat_ind_tac "n" 1);
   139 by (nat_ind_tac "n" 1);
   141 by (rtac (lemma1 RS ssubst) 1);
   141 by (rtac (lemma1 RS ssubst) 1);
   142 by (rtac (lemma2 RS ssubst) 1);
   142 by (rtac (lemma2 RS ssubst) 1);
   143 by (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1);
   143 by (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1);
   144 by (rtac (lemma5 RS sym RS subst) 1);
   144 by (rtac (lemma5 RS sym RS subst) 1);
   145 by (rtac refl 1);
   145 by (rtac refl 1);
   146 val wir_moel = result();
   146 qed "wir_moel";
   147 
   147 
   148 
   148 
   149 
   149