src/HOLCF/ex/Dagstuhl.ML
changeset 1168 74be52691d62
parent 897 55d15c603e3a
child 1267 bca91b4e1710
equal deleted inserted replaced
1167:cbd32a0f2f41 1168:74be52691d62
     1 (*
       
     2 (* $Id$ *)
     1 (* $Id$ *)
     3 *)
       
     4 
       
     5 
     2 
     6 open Dagstuhl;
     3 open Dagstuhl;
     7 
     4 
     8 val YS_def2  = fix_prover Dagstuhl.thy  YS_def  "YS  = scons[y][YS]";
     5 val YS_def2  = fix_prover2 Dagstuhl.thy  YS_def  "YS = scons`y`YS";
     9 val YYS_def2 = fix_prover Dagstuhl.thy YYS_def "YYS = scons[y][scons[y][YYS]]";
     6 val YYS_def2 = fix_prover2 Dagstuhl.thy YYS_def "YYS = scons`y`(scons`y`YYS)";
    10 
     7 
    11 
     8 
    12 val prems = goal Dagstuhl.thy "YYS << scons[y][YYS]";
     9 val prems = goal Dagstuhl.thy "YYS << scons`y`YYS";
    13 by (rtac (YYS_def RS ssubst) 1);
    10 by (rewrite_goals_tac [YYS_def]);
    14 by (rtac fix_ind 1);
    11 by (rtac fix_ind 1);
    15 by (resolve_tac adm_thms 1);
    12 by (resolve_tac adm_thms 1);
    16 by (contX_tacR 1);
    13 by (cont_tacR 1);
    17 by (rtac minimal 1);
    14 by (rtac minimal 1);
    18 by (rtac (beta_cfun RS ssubst) 1);
    15 by (rtac (beta_cfun RS ssubst) 1);
    19 by (contX_tacR 1);
    16 by (cont_tacR 1);
    20 by (rtac monofun_cfun_arg 1);
    17 by (rtac monofun_cfun_arg 1);
    21 by (rtac monofun_cfun_arg 1);
    18 by (rtac monofun_cfun_arg 1);
    22 by (atac 1);
    19 by (atac 1);
    23 qed "lemma3";
    20 val lemma3 = result();
    24 
    21 
    25 val prems = goal Dagstuhl.thy "scons[y][YYS] << YYS";
    22 val prems = goal Dagstuhl.thy "scons`y`YYS << YYS";
    26 by (rtac (YYS_def2 RS ssubst) 1);
    23 by (rtac (YYS_def2 RS ssubst) 1);
    27 back();
    24 back();
    28 by (rtac monofun_cfun_arg 1);
    25 by (rtac monofun_cfun_arg 1);
    29 by (rtac lemma3 1);
    26 by (rtac lemma3 1);
    30 qed "lemma4";
    27 val lemma4=result();
    31 
    28 
    32 (* val  lemma5 = lemma3 RS (lemma4 RS antisym_less) *)
    29 (* val  lemma5 = lemma3 RS (lemma4 RS antisym_less) *)
    33 
    30 
    34 val prems = goal Dagstuhl.thy "scons[y][YYS] = YYS";
    31 val prems = goal Dagstuhl.thy "scons`y`YYS = YYS";
    35 by (rtac antisym_less 1);
    32 by (rtac antisym_less 1);
    36 by (rtac lemma4 1);
    33 by (rtac lemma4 1);
    37 by (rtac lemma3 1);
    34 by (rtac lemma3 1);
    38 qed "lemma5";
    35 val lemma5=result();
    39 
    36 
    40 val prems = goal Dagstuhl.thy "YS = YYS";
    37 val prems = goal Dagstuhl.thy "YS = YYS";
    41 by (rtac stream_take_lemma 1);
    38 by (rtac stream_take_lemma 1);
    42 by (nat_ind_tac "n" 1);
    39 by (nat_ind_tac "n" 1);
    43 by (simp_tac (HOLCF_ss addsimps stream_rews) 1);
    40 by (simp_tac (HOLCF_ss addsimps stream_rews) 1);
    44 by (res_inst_tac [("y1","y")] (YS_def2 RS ssubst) 1);
    41 by (rtac (YS_def2 RS ssubst) 1);
    45 by (res_inst_tac [("y1","y")] (YYS_def2 RS ssubst) 1);
    42 by (rtac (YYS_def2 RS ssubst) 1);
    46 by (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1);
    43 by (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1);
    47 by (rtac (lemma5 RS sym RS subst) 1);
    44 by (rtac (lemma5 RS sym RS subst) 1);
    48 by (rtac refl 1);
    45 by (rtac refl 1);
    49 qed "wir_moel";
    46 val wir_moel=result();
    50 
    47 
    51 (* ------------------------------------------------------------------------ *)
    48 (* ------------------------------------------------------------------------ *)
    52 (* Zweite L"osung: Bernhard M"oller                                         *)
    49 (* Zweite L"osung: Bernhard M"oller                                         *)
    53 (* statt Beweis von  wir_moel "uber take_lemma beidseitige Inclusion        *)
    50 (* statt Beweis von  wir_moel "uber take_lemma beidseitige Inclusion        *)
    54 (* verwendet lemma5                                                         *)
    51 (* verwendet lemma5                                                         *)
    55 (* ------------------------------------------------------------------------ *)
    52 (* ------------------------------------------------------------------------ *)
    56 
    53 
    57 val prems = goal Dagstuhl.thy "YYS << YS";
    54 val prems = goal Dagstuhl.thy "YYS << YS";
    58 by (rtac (YYS_def RS ssubst) 1);
    55 by (rewrite_goals_tac [YYS_def]);
    59 by (rtac fix_least 1);
    56 by (rtac fix_least 1);
    60 by (rtac (beta_cfun RS ssubst) 1);
    57 by (rtac (beta_cfun RS ssubst) 1);
    61 by (contX_tacR 1);
    58 by (cont_tacR 1);
    62 by (simp_tac (HOLCF_ss addsimps [YS_def2 RS sym]) 1);
    59 by (simp_tac (HOLCF_ss addsimps [YS_def2 RS sym]) 1);
    63 qed "lemma6";
    60 val lemma6=result();
    64 
    61 
    65 val prems = goal Dagstuhl.thy "YS << YYS";
    62 val prems = goal Dagstuhl.thy "YS << YYS";
    66 by (rtac (YS_def RS ssubst) 1);
    63 by (rewrite_goals_tac [YS_def]);
    67 by (rtac fix_ind 1);
    64 by (rtac fix_ind 1);
    68 by (resolve_tac adm_thms 1);
    65 by (resolve_tac adm_thms 1);
    69 by (contX_tacR 1);
    66 by (cont_tacR 1);
    70 by (rtac minimal 1);
    67 by (rtac minimal 1);
    71 by (rtac (beta_cfun RS ssubst) 1);
    68 by (rtac (beta_cfun RS ssubst) 1);
    72 by (contX_tacR 1);
    69 by (cont_tacR 1);
    73 by (res_inst_tac [("y2","y10")] (lemma5 RS sym RS ssubst) 1);
    70 by (rtac (lemma5 RS sym RS ssubst) 1);
    74 by (etac monofun_cfun_arg 1);
    71 by (etac monofun_cfun_arg 1);
    75 qed "lemma7";
    72 val lemma7 = result();
    76 
    73 
    77 val  wir_moel = lemma6 RS (lemma7 RS antisym_less);
    74 val  wir_moel = lemma6 RS (lemma7 RS antisym_less);
    78 
    75 
    79 
       
    80 (* ------------------------------------------------------------------------ *)
       
    81 (* L"osung aus Dagstuhl (F.R.)                                              *)
       
    82 (* Wie oben, jedoch ohne Konstantendefinition f"ur YS, YYS                  *)
       
    83 (* ------------------------------------------------------------------------ *)
       
    84 
       
    85 val prems = goal Stream2.thy
       
    86     "(fix[LAM x. scons[y][x]]) = scons[y][fix[LAM x. scons[y][x]]]";
       
    87 by (rtac (fix_eq RS ssubst) 1);
       
    88 back();
       
    89 back();
       
    90 by (rtac (beta_cfun RS ssubst) 1);
       
    91 by (contX_tacR 1);
       
    92 by (rtac refl 1);
       
    93 qed "lemma1";
       
    94 
       
    95 val prems = goal Stream2.thy
       
    96     "(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);
       
    99 back();
       
   100 back();
       
   101 by (rtac (beta_cfun RS ssubst) 1);
       
   102 by (contX_tacR 1);
       
   103 by (rtac refl 1);
       
   104 qed "lemma2";
       
   105 
       
   106 val prems = goal Stream2.thy
       
   107 "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);
       
   110 by (resolve_tac adm_thms 1);
       
   111 by (contX_tacR 1);
       
   112 by (rtac minimal 1);
       
   113 by (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1);
       
   114 by (rtac monofun_cfun_arg 1);
       
   115 by (rtac monofun_cfun_arg 1);
       
   116 by (atac 1);
       
   117 qed "lemma3";
       
   118 
       
   119 val prems = goal Stream2.thy
       
   120 " scons[y][fix[LAM z. scons[y][scons[y][z]]]] <<\
       
   121 \ fix[LAM z. scons[y][scons[y][z]]]";
       
   122 by (rtac (lemma2 RS ssubst) 1);
       
   123 back();
       
   124 by (rtac monofun_cfun_arg 1);
       
   125 by (rtac lemma3 1);
       
   126 qed "lemma4";
       
   127 
       
   128 val prems = goal Stream2.thy
       
   129 " scons[y][fix[LAM z. scons[y][scons[y][z]]]] =\
       
   130 \ fix[LAM z. scons[y][scons[y][z]]]";
       
   131 by (rtac antisym_less 1);
       
   132 by (rtac lemma4 1);
       
   133 by (rtac lemma3 1);
       
   134 qed "lemma5";
       
   135 
       
   136 val prems = goal Stream2.thy
       
   137     "(fix[LAM x. scons[y][x]]) = (fix[ LAM z. scons[y][scons[y][z]]])";
       
   138 by (rtac stream_take_lemma 1);
       
   139 by (nat_ind_tac "n" 1);
       
   140 by (simp_tac (HOLCF_ss addsimps stream_rews) 1);
       
   141 by (rtac (lemma1 RS ssubst) 1);
       
   142 by (rtac (lemma2 RS ssubst) 1);
       
   143 by (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1);
       
   144 by (rtac (lemma5 RS sym RS subst) 1);
       
   145 by (rtac refl 1);
       
   146 qed "wir_moel";
       
   147 
       
   148 
       
   149