src/HOLCF/Cprod3.ML
author nipkow
Sun, 22 Dec 2002 10:43:43 +0100
changeset 13763 f94b569cd610
parent 12030 46d57d0290a2
child 14981 e73f8140af78
permissions -rw-r--r--
added print translations tha avoid eta contraction for important binders.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
     1
(*  Title:      HOLCF/Cprod3
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: 1274
diff changeset
     3
    Author:     Franz Regensburger
12030
wenzelm
parents: 10834
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: 4721
diff changeset
     6
Class instance of * for class pcpo and cpo.
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: 2566
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 "UU = (UU,UU)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    11
by (simp_tac (HOL_ss addsimps [UU_def,UU_cprod_def]) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    12
qed "inst_cprod_pcpo";
2640
ee4dfce170a0 Changes of HOLCF from Oscar Slotosch:
slotosch
parents: 2566
diff changeset
    13
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    14
(* ------------------------------------------------------------------------ *)
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 899
diff changeset
    15
(* continuity of (_,_) , fst, snd                                           *)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    16
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    17
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
    18
Goal 
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
    19
"chain(Y::(nat=>'a::cpo)) ==>\
2840
7e03e61612b0 generalized theorems and class instances for Cprod.
slotosch
parents: 2640
diff changeset
    20
\ (lub(range(Y)),(x::'b::cpo)) =\
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    21
\ (lub(range(%i. fst(Y i,x))),lub(range(%i. snd(Y i,x))))";
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    22
by (res_inst_tac [("f1","Pair")] (arg_cong RS cong) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    23
by (rtac lub_equal 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    24
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    25
by (rtac (monofun_fst RS ch2ch_monofun) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    26
by (rtac ch2ch_fun 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    27
by (rtac (monofun_pair1 RS ch2ch_monofun) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    28
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    29
by (rtac allI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    30
by (Simp_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    31
by (rtac sym 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    32
by (Simp_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    33
by (rtac (lub_const RS thelubI) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    34
qed "Cprod3_lemma1";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    35
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
    36
Goal "contlub(Pair)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    37
by (rtac contlubI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    38
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    39
by (rtac (expand_fun_eq RS iffD2) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    40
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    41
by (stac (lub_fun RS thelubI) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    42
by (etac (monofun_pair1 RS ch2ch_monofun) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    43
by (rtac trans 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    44
by (rtac (thelub_cprod RS sym) 2);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    45
by (rtac ch2ch_fun 2);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    46
by (etac (monofun_pair1 RS ch2ch_monofun) 2);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    47
by (etac Cprod3_lemma1 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    48
qed "contlub_pair1";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    49
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
    50
Goal 
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
    51
"chain(Y::(nat=>'a::cpo)) ==>\
2840
7e03e61612b0 generalized theorems and class instances for Cprod.
slotosch
parents: 2640
diff changeset
    52
\ ((x::'b::cpo),lub(range Y)) =\
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    53
\ (lub(range(%i. fst(x,Y i))),lub(range(%i. snd(x, Y i))))";
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    54
by (res_inst_tac [("f1","Pair")] (arg_cong RS cong) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    55
by (rtac sym 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    56
by (Simp_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    57
by (rtac (lub_const RS thelubI) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    58
by (rtac lub_equal 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    59
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    60
by (rtac (monofun_snd RS ch2ch_monofun) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    61
by (rtac (monofun_pair2 RS ch2ch_monofun) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    62
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    63
by (rtac allI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    64
by (Simp_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    65
qed "Cprod3_lemma2";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    66
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
    67
Goal "contlub(Pair(x))";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    68
by (rtac contlubI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    69
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    70
by (rtac trans 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    71
by (rtac (thelub_cprod RS sym) 2);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    72
by (etac (monofun_pair2 RS ch2ch_monofun) 2);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    73
by (etac Cprod3_lemma2 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    74
qed "contlub_pair2";
243
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
Goal "cont(Pair)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    77
by (rtac monocontlub2cont 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    78
by (rtac monofun_pair1 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    79
by (rtac contlub_pair1 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    80
qed "cont_pair1";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    81
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
    82
Goal "cont(Pair(x))";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    83
by (rtac monocontlub2cont 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    84
by (rtac monofun_pair2 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    85
by (rtac contlub_pair2 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    86
qed "cont_pair2";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    87
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
    88
Goal "contlub(fst)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    89
by (rtac contlubI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    90
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    91
by (stac (lub_cprod RS thelubI) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    92
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    93
by (Simp_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    94
qed "contlub_fst";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    95
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
    96
Goal "contlub(snd)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    97
by (rtac contlubI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    98
by (strip_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
    99
by (stac (lub_cprod RS thelubI) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   100
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   101
by (Simp_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   102
qed "contlub_snd";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   103
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   104
Goal "cont(fst)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   105
by (rtac monocontlub2cont 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   106
by (rtac monofun_fst 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   107
by (rtac contlub_fst 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   108
qed "cont_fst";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   109
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   110
Goal "cont(snd)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   111
by (rtac monocontlub2cont 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   112
by (rtac monofun_snd 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   113
by (rtac contlub_snd 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   114
qed "cont_snd";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   115
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   116
(* 
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   117
 -------------------------------------------------------------------------- 
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   118
 more lemmas for Cprod3.thy 
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   119
 
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   120
 -------------------------------------------------------------------------- 
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
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   123
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   124
(* convert all lemmas to the continuous versions                            *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   125
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   126
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   127
Goalw [cpair_def]
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9248
diff changeset
   128
        "(LAM x y.(x,y))$a$b = (a,b)";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   129
by (stac beta_cfun 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   130
by (simp_tac (simpset() addsimps [cont_pair1,cont_pair2,cont2cont_CF1L]) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   131
by (stac beta_cfun 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   132
by (rtac cont_pair2 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   133
by (rtac refl 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   134
qed "beta_cfun_cprod";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   135
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   136
Goalw [cpair_def]
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   137
        " <a,b>=<aa,ba>  ==> a=aa & b=ba";
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   138
by (dtac (beta_cfun_cprod RS subst) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   139
by (dtac (beta_cfun_cprod RS subst) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   140
by (etac Pair_inject 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   141
by (fast_tac HOL_cs 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   142
qed "inject_cpair";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   143
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   144
Goalw [cpair_def] "UU = <UU,UU>";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   145
by (rtac sym 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   146
by (rtac trans 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   147
by (rtac beta_cfun_cprod 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   148
by (rtac sym 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   149
by (rtac inst_cprod_pcpo 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   150
qed "inst_cprod_pcpo2";
243
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
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   153
 "<a,b> = UU ==> a = UU & b = UU";
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   154
by (dtac (inst_cprod_pcpo2 RS subst) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   155
by (etac inject_cpair 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   156
qed "defined_cpair_rev";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   157
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   158
Goalw [cpair_def]
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   159
        "? a b. z=<a,b>";
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   160
by (rtac PairE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   161
by (rtac exI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   162
by (rtac exI 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   163
by (etac (beta_cfun_cprod RS ssubst) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   164
qed "Exh_Cprod2";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   165
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   166
val prems = Goalw [cpair_def] "[|!!x y. [|p=<x,y> |] ==> Q|] ==> Q";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   167
by (rtac PairE 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   168
by (resolve_tac prems 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   169
by (etac (beta_cfun_cprod RS ssubst) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   170
qed "cprodE";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   171
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   172
Goalw [cfst_def,cpair_def] 
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9248
diff changeset
   173
        "cfst$<x,y>=x";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   174
by (stac beta_cfun_cprod 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   175
by (stac beta_cfun 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   176
by (rtac cont_fst 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   177
by (Simp_tac  1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   178
qed "cfst2";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   179
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   180
Goalw [csnd_def,cpair_def] 
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9248
diff changeset
   181
        "csnd$<x,y>=y";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   182
by (stac beta_cfun_cprod 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   183
by (stac beta_cfun 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   184
by (rtac cont_snd 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   185
by (Simp_tac  1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   186
qed "csnd2";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   187
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9248
diff changeset
   188
Goal "cfst$UU = UU";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   189
by (simp_tac (HOL_ss addsimps [inst_cprod_pcpo2,cfst2]) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   190
qed "cfst_strict";
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   191
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9248
diff changeset
   192
Goal "csnd$UU = UU";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   193
by (simp_tac (HOL_ss addsimps [inst_cprod_pcpo2,csnd2]) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   194
qed "csnd_strict";
2444
150644698367 added cfst_strict and csnd_strict
oheimb
parents: 2033
diff changeset
   195
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9248
diff changeset
   196
Goalw [cfst_def,csnd_def,cpair_def] "<cfst$p , csnd$p> = p";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   197
by (stac beta_cfun_cprod 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   198
by (stac beta_cfun 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   199
by (rtac cont_snd 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   200
by (stac beta_cfun 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   201
by (rtac cont_fst 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   202
by (rtac (surjective_pairing RS sym) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   203
qed "surjective_pairing_Cprod2";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   204
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   205
Goalw [cfst_def,csnd_def,cpair_def]
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   206
 "<xa,ya> << <x,y> ==> xa<<x & ya << y";
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   207
by (rtac less_cprod4c 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   208
by (dtac (beta_cfun_cprod RS subst) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   209
by (dtac (beta_cfun_cprod RS subst) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   210
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   211
qed "less_cprod5c";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   212
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   213
Goalw [cfst_def,csnd_def,cpair_def]
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
   214
"[|chain(S)|] ==> range(S) <<| \
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9248
diff changeset
   215
\ <(lub(range(%i. cfst$(S i)))) , lub(range(%i. csnd$(S i)))>";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   216
by (stac beta_cfun_cprod 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   217
by (stac (beta_cfun RS ext) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   218
by (rtac cont_snd 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   219
by (stac (beta_cfun RS ext) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   220
by (rtac cont_fst 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   221
by (rtac lub_cprod 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   222
by (atac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   223
qed "lub_cprod2";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   224
1779
1155c06fa956 introduced forgotten bind_thm calls
oheimb
parents: 1461
diff changeset
   225
bind_thm ("thelub_cprod2", lub_cprod2 RS thelubI);
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 899
diff changeset
   226
(*
4721
c8a8482a8124 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
oheimb
parents: 4098
diff changeset
   227
chain ?S1 ==>
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 899
diff changeset
   228
 lub (range ?S1) =
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9248
diff changeset
   229
 <lub (range (%i. cfst$(?S1 i))), lub (range (%i. csnd$(?S1 i)))>" 
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 899
diff changeset
   230
*)
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   231
Goalw [csplit_def]
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9248
diff changeset
   232
        "csplit$f$<x,y> = f$x$y";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   233
by (stac beta_cfun 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   234
by (Simp_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   235
by (simp_tac (simpset() addsimps [cfst2,csnd2]) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   236
qed "csplit2";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   237
9248
e1dee89de037 massive tidy-up: goal -> Goal, remove use of prems, etc.
paulson
parents: 9245
diff changeset
   238
Goalw [csplit_def]
10834
a7897aebbffc *** empty log message ***
nipkow
parents: 9248
diff changeset
   239
  "csplit$cpair$z=z";
9245
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   240
by (stac beta_cfun 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   241
by (Simp_tac 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   242
by (simp_tac (simpset() addsimps [surjective_pairing_Cprod2]) 1);
428385c4bc50 removed most batch-style proofs
paulson
parents: 4721
diff changeset
   243
qed "csplit3";
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   244
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   245
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   246
(* install simplifier for Cprod                                             *)
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
1267
bca91b4e1710 added local simpsets
clasohm
parents: 1168
diff changeset
   249
Addsimps [cfst2,csnd2,csplit2];
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   250
1274
ea0668a1c0ba added 8bit pragmas
regensbu
parents: 1267
diff changeset
   251
val Cprod_rews = [cfst2,csnd2,csplit2];