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