src/HOLCF/Up3.ML
author paulson
Fri, 21 Nov 2003 11:15:40 +0100
changeset 14265 95b42e69436c
parent 12030 46d57d0290a2
child 14981 e73f8140af78
permissions -rw-r--r--
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
     1
(*  Title:      HOLCF/Up3.ML
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
     2
    ID:         $Id$
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
     3
    Author:     Franz Regensburger
12030
wenzelm
parents: 10834
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
     5
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
     6
Class instance of  ('a)u for class pcpo
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
     7
*)
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
     8
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2566
diff changeset
     9
(* for compatibility with old HOLCF-Version *)
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    10
Goal "UU = Abs_Up(Inl ())";
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    11
by (simp_tac (HOL_ss addsimps [UU_def,UU_up_def]) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    12
qed "inst_up_pcpo";
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2566
diff changeset
    13
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    14
(* -------------------------------------------------------------------------*)
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    15
(* some lemmas restated for class pcpo                                      *)
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    16
(* ------------------------------------------------------------------------ *)
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    17
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    18
Goal "~ Iup(x) << UU";
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    19
by (stac inst_up_pcpo 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    20
by (rtac less_up2b 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    21
qed "less_up3b";
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    22
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    23
Goal "Iup(x) ~= UU";
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    24
by (stac inst_up_pcpo 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    25
by (rtac defined_Iup 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    26
qed "defined_Iup2";
10230
5eb935d6cc69 tidying and renaming of contrapos rules
paulson
parents: 9248
diff changeset
    27
AddIffs [defined_Iup2];
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    28
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    29
(* ------------------------------------------------------------------------ *)
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    30
(* continuity for Iup                                                       *)
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    31
(* ------------------------------------------------------------------------ *)
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    32
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    33
Goal "contlub(Iup)";
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    34
by (rtac contlubI 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    35
by (strip_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    36
by (rtac trans 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    37
by (rtac (thelub_up1a RS sym) 2);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    38
by (fast_tac HOL_cs 3);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    39
by (etac (monofun_Iup RS ch2ch_monofun) 2);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    40
by (res_inst_tac [("f","Iup")] arg_cong  1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    41
by (rtac lub_equal 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    42
by (atac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    43
by (rtac (monofun_Ifup2 RS ch2ch_monofun) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    44
by (etac (monofun_Iup RS ch2ch_monofun) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    45
by (asm_simp_tac Up0_ss 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    46
qed "contlub_Iup";
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    47
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    48
Goal "cont(Iup)";
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    49
by (rtac monocontlub2cont 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    50
by (rtac monofun_Iup 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    51
by (rtac contlub_Iup 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    52
qed "cont_Iup";
10230
5eb935d6cc69 tidying and renaming of contrapos rules
paulson
parents: 9248
diff changeset
    53
AddIffs [cont_Iup];
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    54
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    55
(* ------------------------------------------------------------------------ *)
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    56
(* continuity for Ifup                                                     *)
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    57
(* ------------------------------------------------------------------------ *)
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    58
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    59
Goal "contlub(Ifup)";
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    60
by (rtac contlubI 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    61
by (strip_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    62
by (rtac trans 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    63
by (rtac (thelub_fun RS sym) 2);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    64
by (etac (monofun_Ifup1 RS ch2ch_monofun) 2);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    65
by (rtac ext 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    66
by (res_inst_tac [("p","x")] upE 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    67
by (asm_simp_tac Up0_ss 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    68
by (rtac (lub_const RS thelubI RS sym) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    69
by (asm_simp_tac Up0_ss 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    70
by (etac contlub_cfun_fun 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
    71
qed "contlub_Ifup1";
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    72
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
    73
8161
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
    74
Goal "contlub(Ifup(f))";
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
    75
by (rtac contlubI 1);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
    76
by (strip_tac 1);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
    77
by (rtac disjE 1);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
    78
by   (stac thelub_up1a 2);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
    79
by     (atac 2);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
    80
by    (atac 2);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
    81
by   (asm_simp_tac Up0_ss 2);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
    82
by   (stac thelub_up1b 3);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
    83
by     (atac 3);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
    84
by    (atac 3);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
    85
by   (fast_tac HOL_cs 1);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
    86
by  (asm_simp_tac Up0_ss 2);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
    87
by  (rtac (chain_UU_I_inverse RS sym) 2);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
    88
by  (rtac allI 2);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
    89
by  (res_inst_tac [("p","Y(i)")] upE 2);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
    90
by   (asm_simp_tac Up0_ss 2);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
    91
by  (rtac notE 2);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
    92
by   (dtac spec 2);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
    93
by   (etac spec 2);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
    94
by  (atac 2);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
    95
by (stac contlub_cfun_arg 1);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
    96
by  (etac (monofun_Ifup2 RS ch2ch_monofun) 1);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
    97
by (rtac lub_equal2 1);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
    98
by   (rtac (monofun_Rep_CFun2 RS ch2ch_monofun) 2);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
    99
by   (etac (monofun_Ifup2 RS ch2ch_monofun) 2);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
   100
by  (etac (monofun_Ifup2 RS ch2ch_monofun) 2);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
   101
by (rtac (chain_mono2 RS exE) 1);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
   102
by   (atac 2);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
   103
by  (etac exE 1);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
   104
by  (etac exE 1);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
   105
by  (rtac exI 1);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
   106
by  (res_inst_tac [("s","Iup(x)"),("t","Y(i)")] ssubst 1);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
   107
by   (atac 1);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
   108
by  (rtac defined_Iup2 1);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
   109
by (rtac exI 1);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
   110
by (strip_tac 1);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
   111
by (res_inst_tac [("p","Y(i)")] upE 1);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
   112
by  (asm_simp_tac Up0_ss 2);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
   113
by (res_inst_tac [("P","Y(i) = UU")] notE 1);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
   114
by  (fast_tac HOL_cs 1);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
   115
by (stac inst_up_pcpo 1);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
   116
by (atac 1);
bde1391fd0a5 added range_composition (also to simpset)
oheimb
parents: 5291
diff changeset
   117
qed "contlub_Ifup2";
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   118
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   119
Goal "cont(Ifup)";
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   120
by (rtac monocontlub2cont 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   121
by (rtac monofun_Ifup1 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   122
by (rtac contlub_Ifup1 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   123
qed "cont_Ifup1";
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   124
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   125
Goal "cont(Ifup(f))";
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   126
by (rtac monocontlub2cont 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   127
by (rtac monofun_Ifup2 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   128
by (rtac contlub_Ifup2 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   129
qed "cont_Ifup2";
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   130
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   131
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   132
(* ------------------------------------------------------------------------ *)
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   133
(* continuous versions of lemmas for ('a)u                                  *)
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   134
(* ------------------------------------------------------------------------ *)
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   135
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   136
Goalw [up_def] "z = UU | (EX x. z = up$x)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   137
by (simp_tac (Up0_ss addsimps [cont_Iup]) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   138
by (stac inst_up_pcpo 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   139
by (rtac Exh_Up 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   140
qed "Exh_Up1";
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   141
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   142
Goalw [up_def] "up$x=up$y ==> x=y";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   143
by (rtac inject_Iup 1);
10230
5eb935d6cc69 tidying and renaming of contrapos rules
paulson
parents: 9248
diff changeset
   144
by Auto_tac;
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   145
qed "inject_up";
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   146
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   147
Goalw [up_def] " up$x ~= UU";
10230
5eb935d6cc69 tidying and renaming of contrapos rules
paulson
parents: 9248
diff changeset
   148
by Auto_tac;
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   149
qed "defined_up";
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   150
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   151
val prems = Goalw [up_def] 
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   152
        "[| p=UU ==> Q; !!x. p=up$x==>Q|] ==>Q";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   153
by (rtac upE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   154
by (resolve_tac prems 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   155
by (etac (inst_up_pcpo RS ssubst) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   156
by (resolve_tac (tl prems) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   157
by (asm_simp_tac (Up0_ss addsimps [cont_Iup]) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   158
qed "upE1";
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   159
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
   160
val tac = (simp_tac (simpset() addsimps [cont_Iup,cont_Ifup1,
2566
cbf02fc74332 changed handling of cont_lemmas and adm_lemmas
oheimb
parents: 2278
diff changeset
   161
                cont_Ifup2,cont2cont_CF1L]) 1);
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   162
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   163
Goalw [up_def,fup_def] "fup$f$UU=UU";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   164
by (stac inst_up_pcpo 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   165
by (stac beta_cfun 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   166
by tac;
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   167
by (stac beta_cfun 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   168
by tac;
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   169
by (simp_tac (Up0_ss addsimps [cont_Iup,cont_Ifup1,cont_Ifup2]) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   170
qed "fup1";
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   171
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   172
Goalw [up_def,fup_def] "fup$f$(up$x)=f$x";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   173
by (stac beta_cfun 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   174
by (rtac cont_Iup 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   175
by (stac beta_cfun 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   176
by tac;
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   177
by (stac beta_cfun 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   178
by (rtac cont_Ifup2 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   179
by (simp_tac (Up0_ss addsimps [cont_Iup,cont_Ifup1,cont_Ifup2]) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   180
qed "fup2";
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   181
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   182
Goalw [up_def,fup_def] "~ up$x << UU";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   183
by (simp_tac (Up0_ss addsimps [cont_Iup]) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   184
by (rtac less_up3b 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   185
qed "less_up4b";
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   186
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   187
Goalw [up_def,fup_def]
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   188
         "(up$x << up$y) = (x<<y)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   189
by (simp_tac (Up0_ss addsimps [cont_Iup]) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   190
by (rtac less_up2c 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   191
qed "less_up4c";
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   192
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   193
Goalw [up_def,fup_def] 
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   194
"[| chain(Y); EX i x. Y(i) = up$x |] ==>\
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   195
\      lub(range(Y)) = up$(lub(range(%i. fup$(LAM x. x)$(Y i))))";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   196
by (stac beta_cfun 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   197
by tac;
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   198
by (stac beta_cfun 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   199
by tac;
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   200
by (stac (beta_cfun RS ext) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   201
by tac;
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   202
by (rtac thelub_up1a 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   203
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   204
by (etac exE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   205
by (etac exE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   206
by (rtac exI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   207
by (rtac exI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   208
by (etac box_equals 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   209
by (rtac refl 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   210
by (simp_tac (Up0_ss addsimps [cont_Iup]) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   211
qed "thelub_up2a";
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   212
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   213
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   214
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   215
Goalw [up_def,fup_def] 
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   216
"[| chain(Y); ! i x. Y(i) ~= up$x |] ==> lub(range(Y)) = UU";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   217
by (stac inst_up_pcpo 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   218
by (rtac thelub_up1b 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   219
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   220
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   221
by (dtac spec 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   222
by (dtac spec 1);
10230
5eb935d6cc69 tidying and renaming of contrapos rules
paulson
parents: 9248
diff changeset
   223
by (asm_full_simp_tac (Up0_ss addsimps [cont_Iup]) 1);
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 9169
diff changeset
   224
qed "thelub_up2b";
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   225
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   226
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   227
Goal "(EX x. z = up$x) = (z~=UU)";
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   228
by (rtac iffI 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   229
by (etac exE 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   230
by (hyp_subst_tac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   231
by (rtac defined_up 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   232
by (res_inst_tac [("p","z")] upE1 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   233
by (etac notE 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   234
by (atac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   235
by (etac exI 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   236
qed "up_lemma2";
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   237
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   238
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   239
Goal "[| chain(Y); lub(range(Y)) = up$x |] ==> EX i x. Y(i) = up$x";
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   240
by (rtac exE 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   241
by (rtac chain_UU_I_inverse2 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   242
by (rtac (up_lemma2 RS iffD1) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   243
by (etac exI 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   244
by (rtac exI 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   245
by (rtac (up_lemma2 RS iffD2) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   246
by (atac 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   247
qed "thelub_up2a_rev";
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   248
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   249
Goal "[| chain(Y); lub(range(Y)) = UU |] ==> ! i x.  Y(i) ~= up$x";
10230
5eb935d6cc69 tidying and renaming of contrapos rules
paulson
parents: 9248
diff changeset
   250
by (blast_tac (claset() addSDs [chain_UU_I RS spec, 
5eb935d6cc69 tidying and renaming of contrapos rules
paulson
parents: 9248
diff changeset
   251
                                exI RS (up_lemma2 RS iffD1)]) 1);
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   252
qed "thelub_up2b_rev";
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   253
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   254
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   255
Goal "chain(Y) ==> lub(range(Y)) = UU | \
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   256
\                  lub(range(Y)) = up$(lub(range(%i. fup$(LAM x. x)$(Y i))))";
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   257
by (rtac disjE 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   258
by (rtac disjI1 2);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   259
by (rtac thelub_up2b 2);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   260
by (atac 2);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   261
by (atac 2);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   262
by (rtac disjI2 2);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   263
by (rtac thelub_up2a 2);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   264
by (atac 2);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   265
by (atac 2);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   266
by (fast_tac HOL_cs 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   267
qed "thelub_up3";
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   268
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 10230
diff changeset
   269
Goal "fup$up$x=x";
9169
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   270
by (res_inst_tac [("p","x")] upE1 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   271
by (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [fup1,fup2]) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   272
by (asm_simp_tac ((simpset_of Cfun3.thy) addsimps [fup1,fup2]) 1);
85a47aa21f74 tidying and unbatchifying
paulson
parents: 8161
diff changeset
   273
qed "fup3";
2278
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   274
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   275
(* ------------------------------------------------------------------------ *)
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   276
(* install simplifier for ('a)u                                             *)
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   277
(* ------------------------------------------------------------------------ *)
d63ffafce255 *** empty log message ***
oheimb
parents:
diff changeset
   278
3327
9b8e638f8602 Eliminated ccc1. Moved ID,oo into Cfun.
slotosch
parents: 2640
diff changeset
   279
Addsimps [fup1,fup2,defined_up];