src/HOLCF/Cfun2.ML
author paulson
Fri, 21 Nov 2003 11:15:40 +0100
changeset 14265 95b42e69436c
parent 12484 7ad150f5fc10
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:
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
     1
(*  Title:      HOLCF/Cfun2
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1168
diff changeset
     3
    Author:     Franz Regensburger
12030
wenzelm
parents: 11341
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     5
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
     6
Class Instance ->::(cpo,cpo)po
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     7
*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     8
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2033
diff changeset
     9
(* for compatibility with old HOLCF-Version *)
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
    10
Goal "(op <<)=(%f1 f2. Rep_CFun f1 << Rep_CFun f2)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
    11
by (fold_goals_tac [less_cfun_def]);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
    12
by (rtac refl 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
    13
qed "inst_cfun_po";
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2033
diff changeset
    14
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    15
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    16
(* access to less_cfun in class po                                          *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    17
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    18
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
    19
Goal "( f1 << f2 ) = (Rep_CFun(f1) << Rep_CFun(f2))";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
    20
by (simp_tac (simpset() addsimps [inst_cfun_po]) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
    21
qed "less_cfun";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    22
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    23
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    24
(* Type 'a ->'b  is pointed                                                 *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    25
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    26
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
    27
Goal "Abs_CFun(% x. UU) << f";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
    28
by (stac less_cfun 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
    29
by (stac Abs_Cfun_inverse2 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
    30
by (rtac cont_const 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
    31
by (rtac minimal_fun 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
    32
qed "minimal_cfun";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    33
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2033
diff changeset
    34
bind_thm ("UU_cfun_def",minimal_cfun RS minimal2UU RS sym);
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2033
diff changeset
    35
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
    36
Goal "? x::'a->'b::pcpo.!y. x<<y";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
    37
by (res_inst_tac [("x","Abs_CFun(% x. UU)")] exI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
    38
by (rtac (minimal_cfun RS allI) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
    39
qed "least_cfun";
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2033
diff changeset
    40
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    41
(* ------------------------------------------------------------------------ *)
5291
5706f0ef1d43 eliminated fabs,fapp.
slotosch
parents: 4721
diff changeset
    42
(* Rep_CFun yields continuous functions in 'a => 'b                             *)
5706f0ef1d43 eliminated fabs,fapp.
slotosch
parents: 4721
diff changeset
    43
(* this is continuity of Rep_CFun in its 'second' argument                      *)
5706f0ef1d43 eliminated fabs,fapp.
slotosch
parents: 4721
diff changeset
    44
(* cont_Rep_CFun2 ==> monofun_Rep_CFun2 & contlub_Rep_CFun2                            *)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    45
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    46
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
    47
Goal "cont(Rep_CFun(fo))";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
    48
by (res_inst_tac [("P","cont")] CollectD 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
    49
by (fold_goals_tac [CFun_def]);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
    50
by (rtac Rep_Cfun 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
    51
qed "cont_Rep_CFun2";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    52
5291
5706f0ef1d43 eliminated fabs,fapp.
slotosch
parents: 4721
diff changeset
    53
bind_thm ("monofun_Rep_CFun2", cont_Rep_CFun2 RS cont2mono);
5706f0ef1d43 eliminated fabs,fapp.
slotosch
parents: 4721
diff changeset
    54
(* monofun(Rep_CFun(?fo1)) *)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    55
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    56
5291
5706f0ef1d43 eliminated fabs,fapp.
slotosch
parents: 4721
diff changeset
    57
bind_thm ("contlub_Rep_CFun2", cont_Rep_CFun2 RS cont2contlub);
5706f0ef1d43 eliminated fabs,fapp.
slotosch
parents: 4721
diff changeset
    58
(* contlub(Rep_CFun(?fo1)) *)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    59
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    60
(* ------------------------------------------------------------------------ *)
5291
5706f0ef1d43 eliminated fabs,fapp.
slotosch
parents: 4721
diff changeset
    61
(* expanded thms cont_Rep_CFun2, contlub_Rep_CFun2                                 *)
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 892
diff changeset
    62
(* looks nice with mixfix syntac                                            *)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    63
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    64
5291
5706f0ef1d43 eliminated fabs,fapp.
slotosch
parents: 4721
diff changeset
    65
bind_thm ("cont_cfun_arg", (cont_Rep_CFun2 RS contE RS spec RS mp));
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9248
diff changeset
    66
(* chain(?x1) ==> range (%i. ?fo3$(?x1 i)) <<| ?fo3$(lub (range ?x1))    *)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    67
 
5291
5706f0ef1d43 eliminated fabs,fapp.
slotosch
parents: 4721
diff changeset
    68
bind_thm ("contlub_cfun_arg", (contlub_Rep_CFun2 RS contlubE RS spec RS mp));
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9248
diff changeset
    69
(* chain(?x1) ==> ?fo4$(lub (range ?x1)) = lub (range (%i. ?fo4$(?x1 i))) *)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    70
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    71
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    72
(* ------------------------------------------------------------------------ *)
5291
5706f0ef1d43 eliminated fabs,fapp.
slotosch
parents: 4721
diff changeset
    73
(* Rep_CFun is monotone in its 'first' argument                                 *)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    74
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    75
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
    76
Goalw [monofun] "monofun(Rep_CFun)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
    77
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
    78
by (etac (less_cfun RS subst) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
    79
qed "monofun_Rep_CFun1";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    80
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    81
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    82
(* ------------------------------------------------------------------------ *)
5291
5706f0ef1d43 eliminated fabs,fapp.
slotosch
parents: 4721
diff changeset
    83
(* monotonicity of application Rep_CFun in mixfix syntax [_]_                   *)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    84
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    85
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9248
diff changeset
    86
Goal  "f1 << f2 ==> f1$x << f2$x";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
    87
by (res_inst_tac [("x","x")] spec 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
    88
by (rtac (less_fun RS subst) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
    89
by (etac (monofun_Rep_CFun1 RS monofunE RS spec RS spec RS mp) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
    90
qed "monofun_cfun_fun";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    91
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    92
5291
5706f0ef1d43 eliminated fabs,fapp.
slotosch
parents: 4721
diff changeset
    93
bind_thm ("monofun_cfun_arg", monofun_Rep_CFun2 RS monofunE RS spec RS spec RS mp);
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9248
diff changeset
    94
(* ?x2 << ?x1 ==> ?fo5$?x2 << ?fo5$?x1                                      *)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    95
11341
100edbd42dba added chain_monofun
oheimb
parents: 10834
diff changeset
    96
Goal "chain Y ==> chain (%i. f\\<cdot>(Y i))";
12484
7ad150f5fc10 isatool expandshort;
wenzelm
parents: 12030
diff changeset
    97
by (rtac chainI 1);
7ad150f5fc10 isatool expandshort;
wenzelm
parents: 12030
diff changeset
    98
by (rtac monofun_cfun_arg 1);
7ad150f5fc10 isatool expandshort;
wenzelm
parents: 12030
diff changeset
    99
by (etac chainE 1);
11341
100edbd42dba added chain_monofun
oheimb
parents: 10834
diff changeset
   100
qed "chain_monofun";
100edbd42dba added chain_monofun
oheimb
parents: 10834
diff changeset
   101
100edbd42dba added chain_monofun
oheimb
parents: 10834
diff changeset
   102
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   103
(* ------------------------------------------------------------------------ *)
5291
5706f0ef1d43 eliminated fabs,fapp.
slotosch
parents: 4721
diff changeset
   104
(* monotonicity of Rep_CFun in both arguments in mixfix syntax [_]_             *)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   105
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   106
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9248
diff changeset
   107
Goal "[|f1<<f2;x1<<x2|] ==> f1$x1 << f2$x2";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   108
by (rtac trans_less 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   109
by (etac monofun_cfun_arg 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   110
by (etac monofun_cfun_fun 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   111
qed "monofun_cfun";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   112
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   113
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9248
diff changeset
   114
Goal "f$x = UU ==> f$UU = UU";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   115
by (rtac (eq_UU_iff RS iffD2) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   116
by (etac subst 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   117
by (rtac (minimal RS monofun_cfun_arg) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   118
qed "strictI";
1989
8e0ff1bfcfea added stric
oheimb
parents: 1779
diff changeset
   119
8e0ff1bfcfea added stric
oheimb
parents: 1779
diff changeset
   120
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   121
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   122
(* ch2ch - rules for the type 'a -> 'b                                      *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   123
(* use MF2 lemmas from Cont.ML                                              *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   124
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   125
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9248
diff changeset
   126
Goal "chain(Y) ==> chain(%i. f$(Y i))";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   127
by (etac (monofun_Rep_CFun2 RS ch2ch_MF2R) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   128
qed "ch2ch_Rep_CFunR";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   129
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   130
5291
5706f0ef1d43 eliminated fabs,fapp.
slotosch
parents: 4721
diff changeset
   131
bind_thm ("ch2ch_Rep_CFunL", monofun_Rep_CFun1 RS ch2ch_MF2L);
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9248
diff changeset
   132
(* chain(?F) ==> chain (%i. ?F i$?x)                                  *)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   133
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   134
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   135
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   136
(*  the lub of a chain of continous functions is monotone                   *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   137
(* use MF2 lemmas from Cont.ML                                              *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   138
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   139
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9248
diff changeset
   140
Goal "chain(F) ==> monofun(% x. lub(range(% j.(F j)$x)))";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   141
by (rtac lub_MF2_mono 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   142
by (rtac monofun_Rep_CFun1 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   143
by (rtac (monofun_Rep_CFun2 RS allI) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   144
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   145
qed "lub_cfun_mono";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   146
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   147
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   148
(* a lemma about the exchange of lubs for type 'a -> 'b                     *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   149
(* use MF2 lemmas from Cont.ML                                              *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   150
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   151
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   152
Goal "[| chain(F); chain(Y) |] ==>\
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9248
diff changeset
   153
\               lub(range(%j. lub(range(%i. F(j)$(Y i))))) =\
a7897aebbffc *** empty log message ***
nipkow
parents: 9248
diff changeset
   154
\               lub(range(%i. lub(range(%j. F(j)$(Y i)))))";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   155
by (rtac ex_lubMF2 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   156
by (rtac monofun_Rep_CFun1 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   157
by (rtac (monofun_Rep_CFun2 RS allI) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   158
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   159
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   160
qed "ex_lubcfun";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   161
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   162
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   163
(* the lub of a chain of cont. functions is continuous                      *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   164
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   165
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9248
diff changeset
   166
Goal "chain(F) ==> cont(% x. lub(range(% j. F(j)$x)))";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   167
by (rtac monocontlub2cont 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   168
by (etac lub_cfun_mono 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   169
by (rtac contlubI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   170
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   171
by (stac (contlub_cfun_arg RS ext) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   172
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   173
by (etac ex_lubcfun 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   174
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   175
qed "cont_lubcfun";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   176
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   177
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   178
(* type 'a -> 'b is chain complete                                          *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   179
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   180
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9248
diff changeset
   181
Goal "chain(CCF) ==> range(CCF) <<| (LAM x. lub(range(% i. CCF(i)$x)))";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   182
by (rtac is_lubI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   183
by (rtac ub_rangeI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   184
by (stac less_cfun 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   185
by (stac Abs_Cfun_inverse2 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   186
by (etac cont_lubcfun 1);
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   187
by (rtac (lub_fun RS is_lubD1 RS ub_rangeD) 1);
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   188
by (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   189
by (stac less_cfun 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   190
by (stac Abs_Cfun_inverse2 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   191
by (etac cont_lubcfun 1);
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   192
by (rtac (lub_fun RS is_lub_lub) 1);
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   193
by (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   194
by (etac (monofun_Rep_CFun1 RS ub2ub_monofun) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   195
qed "lub_cfun";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   196
1779
1155c06fa956 introduced forgotten bind_thm calls
oheimb
parents: 1461
diff changeset
   197
bind_thm ("thelub_cfun", lub_cfun RS thelubI);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   198
(* 
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9248
diff changeset
   199
chain(?CCF1) ==>  lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i$x)))
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   200
*)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   201
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   202
Goal "chain(CCF::nat=>('a->'b)) ==> ? x. range(CCF) <<| x";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   203
by (rtac exI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   204
by (etac lub_cfun 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   205
qed "cpo_cfun";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   206
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   207
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   208
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   209
(* Extensionality in 'a -> 'b                                               *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   210
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   211
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9248
diff changeset
   212
val prems = Goal "(!!x. f$x = g$x) ==> f = g";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   213
by (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   214
by (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   215
by (res_inst_tac [("f","Abs_CFun")] arg_cong 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   216
by (rtac ext 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   217
by (resolve_tac prems 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   218
qed "ext_cfun";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   219
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   220
(* ------------------------------------------------------------------------ *)
5291
5706f0ef1d43 eliminated fabs,fapp.
slotosch
parents: 4721
diff changeset
   221
(* Monotonicity of Abs_CFun                                                     *)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   222
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   223
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   224
Goal "[| cont(f); cont(g); f<<g|] ==> Abs_CFun(f)<<Abs_CFun(g)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   225
by (rtac (less_cfun RS iffD2) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   226
by (stac Abs_Cfun_inverse2 1);
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   227
by (assume_tac 1);
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   228
by (stac Abs_Cfun_inverse2 1);
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   229
by (assume_tac 1);
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   230
by (assume_tac 1);
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   231
qed "semi_monofun_Abs_CFun";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   232
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   233
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   234
(* Extenionality wrt. << in 'a -> 'b                                        *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   235
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   236
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9248
diff changeset
   237
val prems = Goal "(!!x. f$x << g$x) ==> f << g";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   238
by (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   239
by (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   240
by (rtac semi_monofun_Abs_CFun 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   241
by (rtac cont_Rep_CFun2 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   242
by (rtac cont_Rep_CFun2 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   243
by (rtac (less_fun RS iffD2) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   244
by (rtac allI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   245
by (resolve_tac prems 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 5291
diff changeset
   246
qed "less_cfun2";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   247
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   248