src/HOLCF/ex/Dagstuhl.ML
author regensbu
Tue, 07 Feb 1995 17:35:49 +0100
changeset 896 56b9c2626e81
parent 895 7a1e07fbffea
child 897 55d15c603e3a
permissions -rw-r--r--
ID for the file
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
896
56b9c2626e81 ID for the file
regensbu
parents: 895
diff changeset
     1
(* $Id$ *)
299
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
     2
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
     3
open Dagstuhl;
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
     4
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
     5
val YS_def2  = fix_prover Dagstuhl.thy  YS_def  "YS  = scons[y][YS]";
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
     6
val YYS_def2 = fix_prover Dagstuhl.thy YYS_def "YYS = scons[y][scons[y][YYS]]";
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
     7
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
     8
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
     9
val prems = goal Dagstuhl.thy "YYS << scons[y][YYS]";
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    10
by (rtac (YYS_def RS ssubst) 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    11
by (rtac fix_ind 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    12
by (resolve_tac adm_thms 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    13
by (contX_tacR 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    14
by (rtac minimal 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    15
by (rtac (beta_cfun RS ssubst) 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    16
by (contX_tacR 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    17
by (rtac monofun_cfun_arg 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    18
by (rtac monofun_cfun_arg 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    19
by (atac 1);
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 299
diff changeset
    20
qed "lemma3";
299
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    21
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    22
val prems = goal Dagstuhl.thy "scons[y][YYS] << YYS";
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    23
by (rtac (YYS_def2 RS ssubst) 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    24
back();
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    25
by (rtac monofun_cfun_arg 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    26
by (rtac lemma3 1);
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 299
diff changeset
    27
qed "lemma4";
299
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    28
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    29
(* val  lemma5 = lemma3 RS (lemma4 RS antisym_less) *)
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    30
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    31
val prems = goal Dagstuhl.thy "scons[y][YYS] = YYS";
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    32
by (rtac antisym_less 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    33
by (rtac lemma4 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    34
by (rtac lemma3 1);
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 299
diff changeset
    35
qed "lemma5";
299
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    36
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    37
val prems = goal Dagstuhl.thy "YS = YYS";
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    38
by (rtac stream_take_lemma 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    39
by (nat_ind_tac "n" 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    40
by (simp_tac (HOLCF_ss addsimps stream_rews) 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    41
by (res_inst_tac [("y1","y")] (YS_def2 RS ssubst) 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    42
by (res_inst_tac [("y1","y")] (YYS_def2 RS ssubst) 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    43
by (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    44
by (rtac (lemma5 RS sym RS subst) 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    45
by (rtac refl 1);
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 299
diff changeset
    46
qed "wir_moel";
299
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    47
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    48
(* ------------------------------------------------------------------------ *)
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    49
(* Zweite L"osung: Bernhard M"oller                                         *)
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    50
(* statt Beweis von  wir_moel "uber take_lemma beidseitige Inclusion        *)
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    51
(* verwendet lemma5                                                         *)
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    52
(* ------------------------------------------------------------------------ *)
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    53
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    54
val prems = goal Dagstuhl.thy "YYS << YS";
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    55
by (rtac (YYS_def RS ssubst) 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    56
by (rtac fix_least 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    57
by (rtac (beta_cfun RS ssubst) 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    58
by (contX_tacR 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    59
by (simp_tac (HOLCF_ss addsimps [YS_def2 RS sym]) 1);
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 299
diff changeset
    60
qed "lemma6";
299
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    61
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    62
val prems = goal Dagstuhl.thy "YS << YYS";
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    63
by (rtac (YS_def RS ssubst) 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    64
by (rtac fix_ind 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    65
by (resolve_tac adm_thms 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    66
by (contX_tacR 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    67
by (rtac minimal 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    68
by (rtac (beta_cfun RS ssubst) 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    69
by (contX_tacR 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    70
by (res_inst_tac [("y2","y10")] (lemma5 RS sym RS ssubst) 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    71
by (etac monofun_cfun_arg 1);
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 299
diff changeset
    72
qed "lemma7";
299
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    73
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    74
val  wir_moel = lemma6 RS (lemma7 RS antisym_less);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    75
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    76
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    77
(* ------------------------------------------------------------------------ *)
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    78
(* L"osung aus Dagstuhl (F.R.)                                              *)
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    79
(* Wie oben, jedoch ohne Konstantendefinition f"ur YS, YYS                  *)
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    80
(* ------------------------------------------------------------------------ *)
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    81
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    82
val prems = goal Stream2.thy
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    83
    "(fix[LAM x. scons[y][x]]) = scons[y][fix[LAM x. scons[y][x]]]";
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    84
by (rtac (fix_eq RS ssubst) 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    85
back();
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    86
back();
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    87
by (rtac (beta_cfun RS ssubst) 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    88
by (contX_tacR 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    89
by (rtac refl 1);
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 299
diff changeset
    90
qed "lemma1";
299
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    91
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    92
val prems = goal Stream2.thy
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    93
    "(fix[ LAM z. scons[y][scons[y][z]]]) = \
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    94
\     scons[y][scons[y][(fix[ LAM z. scons[y][scons[y][z]]])]]";
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    95
by (rtac (fix_eq RS ssubst) 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    96
back();
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    97
back();
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    98
by (rtac (beta_cfun RS ssubst) 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
    99
by (contX_tacR 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   100
by (rtac refl 1);
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 299
diff changeset
   101
qed "lemma2";
299
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   102
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   103
val prems = goal Stream2.thy
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   104
"fix[LAM z. scons[y][scons[y][z]]] << \
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   105
\ scons[y][fix[LAM z. scons[y][scons[y][z]]]]";
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   106
by (rtac fix_ind 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   107
by (resolve_tac adm_thms 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   108
by (contX_tacR 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   109
by (rtac minimal 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   110
by (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   111
by (rtac monofun_cfun_arg 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   112
by (rtac monofun_cfun_arg 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   113
by (atac 1);
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 299
diff changeset
   114
qed "lemma3";
299
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   115
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   116
val prems = goal Stream2.thy
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   117
" scons[y][fix[LAM z. scons[y][scons[y][z]]]] <<\
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   118
\ fix[LAM z. scons[y][scons[y][z]]]";
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   119
by (rtac (lemma2 RS ssubst) 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   120
back();
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   121
by (rtac monofun_cfun_arg 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   122
by (rtac lemma3 1);
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 299
diff changeset
   123
qed "lemma4";
299
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   124
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   125
val prems = goal Stream2.thy
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   126
" scons[y][fix[LAM z. scons[y][scons[y][z]]]] =\
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   127
\ fix[LAM z. scons[y][scons[y][z]]]";
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   128
by (rtac antisym_less 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   129
by (rtac lemma4 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   130
by (rtac lemma3 1);
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 299
diff changeset
   131
qed "lemma5";
299
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   132
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   133
val prems = goal Stream2.thy
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   134
    "(fix[LAM x. scons[y][x]]) = (fix[ LAM z. scons[y][scons[y][z]]])";
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   135
by (rtac stream_take_lemma 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   136
by (nat_ind_tac "n" 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   137
by (simp_tac (HOLCF_ss addsimps stream_rews) 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   138
by (rtac (lemma1 RS ssubst) 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   139
by (rtac (lemma2 RS ssubst) 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   140
by (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   141
by (rtac (lemma5 RS sym RS subst) 1);
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   142
by (rtac refl 1);
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 299
diff changeset
   143
qed "wir_moel";
299
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   144
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   145
febeb36a4ba4 Franz fragen
nipkow
parents:
diff changeset
   146