src/HOLCF/Cfun2.ML
author clasohm
Tue Feb 07 11:59:32 1995 +0100 (1995-02-07)
changeset 892 d0dc8d057929
parent 297 5ef75ff3baeb
child 1168 74be52691d62
permissions -rw-r--r--
added qed, qed_goal[w]
nipkow@243
     1
(*  Title: 	HOLCF/cfun2.thy
nipkow@243
     2
    ID:         $Id$
nipkow@243
     3
    Author: 	Franz Regensburger
nipkow@243
     4
    Copyright   1993 Technische Universitaet Muenchen
nipkow@243
     5
nipkow@243
     6
Lemmas for cfun2.thy 
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
open Cfun2;
nipkow@243
    10
nipkow@243
    11
(* ------------------------------------------------------------------------ *)
nipkow@243
    12
(* access to less_cfun in class po                                          *)
nipkow@243
    13
(* ------------------------------------------------------------------------ *)
nipkow@243
    14
clasohm@892
    15
qed_goal "less_cfun" Cfun2.thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))"
nipkow@243
    16
(fn prems =>
nipkow@243
    17
	[
nipkow@243
    18
	(rtac (inst_cfun_po RS ssubst) 1),
nipkow@243
    19
	(fold_goals_tac [less_cfun_def]),
nipkow@243
    20
	(rtac refl 1)
nipkow@243
    21
	]);
nipkow@243
    22
nipkow@243
    23
(* ------------------------------------------------------------------------ *)
nipkow@243
    24
(* Type 'a ->'b  is pointed                                                 *)
nipkow@243
    25
(* ------------------------------------------------------------------------ *)
nipkow@243
    26
clasohm@892
    27
qed_goalw "minimal_cfun" Cfun2.thy [UU_cfun_def] "UU_cfun << f"
nipkow@243
    28
(fn prems =>
nipkow@243
    29
	[
nipkow@243
    30
	(rtac (less_cfun RS ssubst) 1),
nipkow@243
    31
	(rtac (Abs_Cfun_inverse2 RS ssubst) 1),
nipkow@243
    32
	(rtac contX_const 1),
nipkow@243
    33
	(fold_goals_tac [UU_fun_def]),
nipkow@243
    34
	(rtac minimal_fun 1)
nipkow@243
    35
	]);
nipkow@243
    36
nipkow@243
    37
(* ------------------------------------------------------------------------ *)
nipkow@243
    38
(* fapp yields continuous functions in 'a => 'b                             *)
nipkow@243
    39
(* this is continuity of fapp in its 'second' argument                      *)
nipkow@243
    40
(* contX_fapp2 ==> monofun_fapp2 & contlub_fapp2                            *)
nipkow@243
    41
(* ------------------------------------------------------------------------ *)
nipkow@243
    42
clasohm@892
    43
qed_goal "contX_fapp2" Cfun2.thy "contX(fapp(fo))"
nipkow@243
    44
(fn prems =>
nipkow@243
    45
	[
nipkow@243
    46
	(res_inst_tac [("P","contX")] CollectD 1),
nipkow@243
    47
	(fold_goals_tac [Cfun_def]),
nipkow@243
    48
	(rtac Rep_Cfun 1)
nipkow@243
    49
	]);
nipkow@243
    50
nipkow@243
    51
val monofun_fapp2 = contX_fapp2 RS contX2mono;
nipkow@243
    52
(* monofun(fapp(?fo1)) *)
nipkow@243
    53
nipkow@243
    54
nipkow@243
    55
val contlub_fapp2 = contX_fapp2 RS contX2contlub;
nipkow@243
    56
(* contlub(fapp(?fo1)) *)
nipkow@243
    57
nipkow@243
    58
(* ------------------------------------------------------------------------ *)
nipkow@243
    59
(* expanded thms contX_fapp2, contlub_fapp2                                 *)
nipkow@243
    60
(* looks nice with mixfix syntac _[_]                                       *)
nipkow@243
    61
(* ------------------------------------------------------------------------ *)
nipkow@243
    62
nipkow@243
    63
val contX_cfun_arg = (contX_fapp2 RS contXE RS spec RS mp);
nipkow@243
    64
(* is_chain(?x1) ==> range(%i. ?fo3[?x1(i)]) <<| ?fo3[lub(range(?x1))]      *)
nipkow@243
    65
 
nipkow@243
    66
val contlub_cfun_arg = (contlub_fapp2 RS contlubE RS spec RS mp);
nipkow@243
    67
(* is_chain(?x1) ==> ?fo4[lub(range(?x1))] = lub(range(%i. ?fo4[?x1(i)]))   *)
nipkow@243
    68
nipkow@243
    69
nipkow@243
    70
nipkow@243
    71
(* ------------------------------------------------------------------------ *)
nipkow@243
    72
(* fapp is monotone in its 'first' argument                                 *)
nipkow@243
    73
(* ------------------------------------------------------------------------ *)
nipkow@243
    74
clasohm@892
    75
qed_goalw "monofun_fapp1" Cfun2.thy [monofun] "monofun(fapp)"
nipkow@243
    76
(fn prems =>
nipkow@243
    77
	[
nipkow@243
    78
	(strip_tac 1),
nipkow@243
    79
	(etac (less_cfun RS subst) 1)
nipkow@243
    80
	]);
nipkow@243
    81
nipkow@243
    82
nipkow@243
    83
(* ------------------------------------------------------------------------ *)
nipkow@243
    84
(* monotonicity of application fapp in mixfix syntax [_]_                   *)
nipkow@243
    85
(* ------------------------------------------------------------------------ *)
nipkow@243
    86
clasohm@892
    87
qed_goal "monofun_cfun_fun" Cfun2.thy  "f1 << f2 ==> f1[x] << f2[x]"
nipkow@243
    88
(fn prems =>
nipkow@243
    89
	[
nipkow@243
    90
	(cut_facts_tac prems 1),
nipkow@243
    91
	(res_inst_tac [("x","x")] spec 1),
nipkow@243
    92
	(rtac (less_fun RS subst) 1),
nipkow@243
    93
	(etac (monofun_fapp1 RS monofunE RS spec RS spec RS mp) 1)
nipkow@243
    94
	]);
nipkow@243
    95
nipkow@243
    96
nipkow@243
    97
val monofun_cfun_arg = (monofun_fapp2 RS monofunE RS spec RS spec RS mp);
nipkow@243
    98
(* ?x2 << ?x1 ==> ?fo5[?x2] << ?fo5[?x1]                                    *)
nipkow@243
    99
nipkow@243
   100
(* ------------------------------------------------------------------------ *)
nipkow@243
   101
(* monotonicity of fapp in both arguments in mixfix syntax [_]_             *)
nipkow@243
   102
(* ------------------------------------------------------------------------ *)
nipkow@243
   103
clasohm@892
   104
qed_goal "monofun_cfun" Cfun2.thy
nipkow@243
   105
	"[|f1<<f2;x1<<x2|] ==> f1[x1] << f2[x2]"
nipkow@243
   106
(fn prems =>
nipkow@243
   107
	[
nipkow@243
   108
	(cut_facts_tac prems 1),
nipkow@243
   109
	(rtac trans_less 1),
nipkow@243
   110
	(etac monofun_cfun_arg 1),
nipkow@243
   111
	(etac monofun_cfun_fun 1)
nipkow@243
   112
	]);
nipkow@243
   113
nipkow@243
   114
nipkow@243
   115
(* ------------------------------------------------------------------------ *)
nipkow@243
   116
(* ch2ch - rules for the type 'a -> 'b                                      *)
nipkow@243
   117
(* use MF2 lemmas from Cont.ML                                              *)
nipkow@243
   118
(* ------------------------------------------------------------------------ *)
nipkow@243
   119
clasohm@892
   120
qed_goal "ch2ch_fappR" Cfun2.thy 
nipkow@243
   121
 "is_chain(Y) ==> is_chain(%i. f[Y(i)])"
nipkow@243
   122
(fn prems =>
nipkow@243
   123
	[
nipkow@243
   124
	(cut_facts_tac prems 1),
nipkow@243
   125
	(etac (monofun_fapp2 RS ch2ch_MF2R) 1)
nipkow@243
   126
	]);
nipkow@243
   127
nipkow@243
   128
nipkow@243
   129
val ch2ch_fappL = (monofun_fapp1 RS ch2ch_MF2L);
nipkow@243
   130
(* is_chain(?F) ==> is_chain(%i. ?F(i)[?x])                                 *)
nipkow@243
   131
nipkow@243
   132
nipkow@243
   133
(* ------------------------------------------------------------------------ *)
nipkow@243
   134
(*  the lub of a chain of continous functions is monotone                   *)
nipkow@243
   135
(* use MF2 lemmas from Cont.ML                                              *)
nipkow@243
   136
(* ------------------------------------------------------------------------ *)
nipkow@243
   137
clasohm@892
   138
qed_goal "lub_cfun_mono" Cfun2.thy 
nipkow@243
   139
	"is_chain(F) ==> monofun(% x.lub(range(% j.F(j)[x])))"
nipkow@243
   140
(fn prems =>
nipkow@243
   141
	[
nipkow@243
   142
	(cut_facts_tac prems 1),
nipkow@243
   143
	(rtac lub_MF2_mono 1),
nipkow@243
   144
	(rtac monofun_fapp1 1),
nipkow@243
   145
	(rtac (monofun_fapp2 RS allI) 1),
nipkow@243
   146
	(atac 1)
nipkow@243
   147
	]);
nipkow@243
   148
nipkow@243
   149
(* ------------------------------------------------------------------------ *)
nipkow@243
   150
(* a lemma about the exchange of lubs for type 'a -> 'b                     *)
nipkow@243
   151
(* use MF2 lemmas from Cont.ML                                              *)
nipkow@243
   152
(* ------------------------------------------------------------------------ *)
nipkow@243
   153
clasohm@892
   154
qed_goal "ex_lubcfun" Cfun2.thy
nipkow@243
   155
	"[| is_chain(F); is_chain(Y) |] ==>\
nipkow@243
   156
\		lub(range(%j. lub(range(%i. F(j)[Y(i)])))) =\
nipkow@243
   157
\		lub(range(%i. lub(range(%j. F(j)[Y(i)]))))"
nipkow@243
   158
(fn prems =>
nipkow@243
   159
	[
nipkow@243
   160
	(cut_facts_tac prems 1),
nipkow@243
   161
	(rtac ex_lubMF2 1),
nipkow@243
   162
	(rtac monofun_fapp1 1),
nipkow@243
   163
	(rtac (monofun_fapp2 RS allI) 1),
nipkow@243
   164
	(atac 1),
nipkow@243
   165
	(atac 1)
nipkow@243
   166
	]);
nipkow@243
   167
nipkow@243
   168
(* ------------------------------------------------------------------------ *)
nipkow@243
   169
(* the lub of a chain of cont. functions is continuous                      *)
nipkow@243
   170
(* ------------------------------------------------------------------------ *)
nipkow@243
   171
clasohm@892
   172
qed_goal "contX_lubcfun" Cfun2.thy 
nipkow@243
   173
	"is_chain(F) ==> contX(% x.lub(range(% j.F(j)[x])))"
nipkow@243
   174
(fn prems =>
nipkow@243
   175
	[
nipkow@243
   176
	(cut_facts_tac prems 1),
nipkow@243
   177
	(rtac monocontlub2contX 1),
nipkow@243
   178
	(etac lub_cfun_mono 1),
nipkow@243
   179
	(rtac contlubI 1),
nipkow@243
   180
	(strip_tac 1),
nipkow@243
   181
	(rtac (contlub_cfun_arg RS ext RS ssubst) 1),
nipkow@243
   182
	(atac 1),
nipkow@243
   183
	(etac ex_lubcfun 1),
nipkow@243
   184
	(atac 1)
nipkow@243
   185
	]);
nipkow@243
   186
nipkow@243
   187
(* ------------------------------------------------------------------------ *)
nipkow@243
   188
(* type 'a -> 'b is chain complete                                          *)
nipkow@243
   189
(* ------------------------------------------------------------------------ *)
nipkow@243
   190
clasohm@892
   191
qed_goal "lub_cfun" Cfun2.thy 
nipkow@243
   192
  "is_chain(CCF) ==> range(CCF) <<| fabs(% x.lub(range(% i.CCF(i)[x])))"
nipkow@243
   193
(fn prems =>
nipkow@243
   194
	[
nipkow@243
   195
	(cut_facts_tac prems 1),
nipkow@243
   196
	(rtac is_lubI 1),
nipkow@243
   197
	(rtac conjI 1),
nipkow@243
   198
	(rtac ub_rangeI 1),  
nipkow@243
   199
	(rtac allI 1),
nipkow@243
   200
	(rtac (less_cfun RS ssubst) 1),
nipkow@243
   201
	(rtac (Abs_Cfun_inverse2 RS ssubst) 1),
nipkow@243
   202
	(etac contX_lubcfun 1),
nipkow@243
   203
	(rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1),
nipkow@243
   204
	(etac (monofun_fapp1 RS ch2ch_monofun) 1),
nipkow@243
   205
	(strip_tac 1),
nipkow@243
   206
	(rtac (less_cfun RS ssubst) 1),
nipkow@243
   207
	(rtac (Abs_Cfun_inverse2 RS ssubst) 1),
nipkow@243
   208
	(etac contX_lubcfun 1),
nipkow@243
   209
	(rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1),
nipkow@243
   210
	(etac (monofun_fapp1 RS ch2ch_monofun) 1),
nipkow@243
   211
	(etac (monofun_fapp1 RS ub2ub_monofun) 1)
nipkow@243
   212
	]);
nipkow@243
   213
nipkow@243
   214
val thelub_cfun = (lub_cfun RS thelubI);
nipkow@243
   215
(* 
nipkow@243
   216
is_chain(?CCF1) ==> lub(range(?CCF1)) = fabs(%x. lub(range(%i. ?CCF1(i)[x])))
nipkow@243
   217
*)
nipkow@243
   218
clasohm@892
   219
qed_goal "cpo_cfun" Cfun2.thy 
nipkow@243
   220
  "is_chain(CCF::nat=>('a::pcpo->'b::pcpo)) ==> ? x. range(CCF) <<| x"
nipkow@243
   221
(fn prems =>
nipkow@243
   222
	[
nipkow@243
   223
	(cut_facts_tac prems 1),
nipkow@243
   224
	(rtac exI 1),
nipkow@243
   225
	(etac lub_cfun 1)
nipkow@243
   226
	]);
nipkow@243
   227
nipkow@243
   228
nipkow@243
   229
(* ------------------------------------------------------------------------ *)
nipkow@243
   230
(* Extensionality in 'a -> 'b                                               *)
nipkow@243
   231
(* ------------------------------------------------------------------------ *)
nipkow@243
   232
clasohm@892
   233
qed_goal "ext_cfun" Cfun1.thy "(!!x. f[x] = g[x]) ==> f = g"
nipkow@243
   234
 (fn prems =>
nipkow@243
   235
	[
nipkow@243
   236
	(res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
nipkow@243
   237
	(res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
nipkow@243
   238
	(res_inst_tac [("f","fabs")] arg_cong 1),
nipkow@243
   239
	(rtac ext 1),
nipkow@243
   240
	(resolve_tac prems 1)
nipkow@243
   241
	]);
nipkow@243
   242
nipkow@243
   243
(* ------------------------------------------------------------------------ *)
nipkow@243
   244
(* Monotonicity of fabs                                                     *)
nipkow@243
   245
(* ------------------------------------------------------------------------ *)
nipkow@243
   246
clasohm@892
   247
qed_goal "semi_monofun_fabs" Cfun2.thy 
nipkow@243
   248
	"[|contX(f);contX(g);f<<g|]==>fabs(f)<<fabs(g)"
nipkow@243
   249
 (fn prems =>
nipkow@243
   250
	[
nipkow@243
   251
	(rtac (less_cfun RS iffD2) 1),
nipkow@243
   252
	(rtac (Abs_Cfun_inverse2 RS ssubst) 1),
nipkow@243
   253
	(resolve_tac prems 1),
nipkow@243
   254
	(rtac (Abs_Cfun_inverse2 RS ssubst) 1),
nipkow@243
   255
	(resolve_tac prems 1),
nipkow@243
   256
	(resolve_tac prems 1)
nipkow@243
   257
	]);
nipkow@243
   258
nipkow@243
   259
(* ------------------------------------------------------------------------ *)
nipkow@243
   260
(* Extenionality wrt. << in 'a -> 'b                                        *)
nipkow@243
   261
(* ------------------------------------------------------------------------ *)
nipkow@243
   262
clasohm@892
   263
qed_goal "less_cfun2" Cfun2.thy "(!!x. f[x] << g[x]) ==> f << g"
nipkow@243
   264
 (fn prems =>
nipkow@243
   265
	[
nipkow@243
   266
	(res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1),
nipkow@243
   267
	(res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1),
nipkow@243
   268
	(rtac semi_monofun_fabs 1),
nipkow@243
   269
	(rtac contX_fapp2 1),
nipkow@243
   270
	(rtac contX_fapp2 1),
nipkow@243
   271
	(rtac (less_fun RS iffD2) 1),
nipkow@243
   272
	(rtac allI 1),
nipkow@243
   273
	(resolve_tac prems 1)
nipkow@243
   274
	]);
nipkow@243
   275
nipkow@243
   276