src/HOLCF/Cprod2.ML
author oheimb
Fri, 31 May 1996 19:55:19 +0200
changeset 1779 1155c06fa956
parent 1461 6bcb44e4d6e5
child 2033 639de962ded4
permissions -rw-r--r--
introduced forgotten bind_thm calls
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
     1
(*  Title:      HOLCF/cprod2.ML
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: 1267
diff changeset
     3
    Author:     Franz Regensburger
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     4
    Copyright   1993 Technische Universitaet Muenchen
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     5
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     6
Lemmas for cprod2.thy 
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
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
     9
open Cprod2;
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    10
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 243
diff changeset
    11
qed_goal "less_cprod3a" Cprod2.thy 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    12
        "p1=(UU,UU) ==> p1 << p2"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    13
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    14
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    15
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    16
        (rtac (inst_cprod_po RS ssubst) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    17
        (rtac (less_cprod1b RS ssubst) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    18
        (hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    19
        (Asm_simp_tac  1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    20
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    21
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 243
diff changeset
    22
qed_goal "less_cprod3b" Cprod2.thy
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    23
 "(p1 << p2) = (fst(p1)<<fst(p2) & snd(p1)<<snd(p2))"
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    24
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    25
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    26
        (rtac (inst_cprod_po RS ssubst) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    27
        (rtac less_cprod1b 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    28
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    29
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 243
diff changeset
    30
qed_goal "less_cprod4a" Cprod2.thy 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    31
        "(x1,x2) << (UU,UU) ==> x1=UU & x2=UU"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    32
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    33
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    34
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    35
        (rtac less_cprod2a 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    36
        (etac (inst_cprod_po RS subst) 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    37
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    38
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 243
diff changeset
    39
qed_goal "less_cprod4b" Cprod2.thy 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    40
        "p << (UU,UU) ==> p = (UU,UU)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    41
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    42
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    43
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    44
        (rtac less_cprod2b 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    45
        (etac (inst_cprod_po RS subst) 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    46
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    47
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 243
diff changeset
    48
qed_goal "less_cprod4c" Cprod2.thy
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 899
diff changeset
    49
 " (xa,ya) << (x,y) ==> xa<<x & ya << y"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    50
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    51
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    52
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    53
        (rtac less_cprod2c 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    54
        (etac (inst_cprod_po RS subst) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    55
        (REPEAT (atac 1))
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    56
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    57
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    58
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    59
(* type cprod is pointed                                                    *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    60
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    61
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 899
diff changeset
    62
qed_goal "minimal_cprod" Cprod2.thy  "(UU,UU)<<p"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    63
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    64
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    65
        (rtac less_cprod3a 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    66
        (rtac refl 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    67
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    68
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    69
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    70
(* Pair <_,_>  is monotone in both arguments                                *)
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
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 243
diff changeset
    73
qed_goalw "monofun_pair1" Cprod2.thy [monofun] "monofun(Pair)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    74
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    75
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    76
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    77
        (rtac (less_fun RS iffD2) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    78
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    79
        (rtac (less_cprod3b RS iffD2) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    80
        (Simp_tac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    81
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    82
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 243
diff changeset
    83
qed_goalw "monofun_pair2" Cprod2.thy [monofun] "monofun(Pair(x))"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    84
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    85
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    86
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    87
        (rtac (less_cprod3b RS iffD2) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    88
        (Simp_tac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    89
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    90
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 243
diff changeset
    91
qed_goal "monofun_pair" Cprod2.thy 
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 899
diff changeset
    92
 "[|x1<<x2; y1<<y2|] ==> (x1,y1) << (x2,y2)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
    93
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    94
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    95
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    96
        (rtac trans_less 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    97
        (rtac (monofun_pair1 RS monofunE RS spec RS spec RS mp RS 
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    98
        (less_fun RS iffD1 RS spec)) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
    99
        (rtac (monofun_pair2 RS monofunE RS spec RS spec RS mp) 2),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   100
        (atac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   101
        (atac 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   102
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   103
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   104
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   105
(* fst and snd are monotone                                                 *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   106
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   107
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 243
diff changeset
   108
qed_goalw "monofun_fst" Cprod2.thy [monofun] "monofun(fst)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   109
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   110
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   111
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   112
        (res_inst_tac [("p","x")] PairE 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   113
        (hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   114
        (res_inst_tac [("p","y")] PairE 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   115
        (hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   116
        (Asm_simp_tac  1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   117
        (etac (less_cprod4c RS conjunct1) 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   118
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   119
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 243
diff changeset
   120
qed_goalw "monofun_snd" Cprod2.thy [monofun] "monofun(snd)"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   121
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   122
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   123
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   124
        (res_inst_tac [("p","x")] PairE 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   125
        (hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   126
        (res_inst_tac [("p","y")] PairE 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   127
        (hyp_subst_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   128
        (Asm_simp_tac  1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   129
        (etac (less_cprod4c RS conjunct2) 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   130
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   131
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   132
(* ------------------------------------------------------------------------ *)
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   133
(* the type 'a * 'b is a cpo                                                *)
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
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 243
diff changeset
   136
qed_goal "lub_cprod" Cprod2.thy 
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   137
" is_chain(S) ==> range(S) <<| \
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 899
diff changeset
   138
\   (lub(range(%i.fst(S i))),lub(range(%i.snd(S i)))) "
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   139
 (fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   140
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   141
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   142
        (rtac is_lubI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   143
        (rtac conjI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   144
        (rtac ub_rangeI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   145
        (rtac allI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   146
        (res_inst_tac [("t","S(i)")] (surjective_pairing RS ssubst) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   147
        (rtac monofun_pair 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   148
        (rtac is_ub_thelub 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   149
        (etac (monofun_fst RS ch2ch_monofun) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   150
        (rtac is_ub_thelub 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   151
        (etac (monofun_snd RS ch2ch_monofun) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   152
        (strip_tac 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   153
        (res_inst_tac [("t","u")] (surjective_pairing RS ssubst) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   154
        (rtac monofun_pair 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   155
        (rtac is_lub_thelub 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   156
        (etac (monofun_fst RS ch2ch_monofun) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   157
        (etac (monofun_fst RS ub2ub_monofun) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   158
        (rtac is_lub_thelub 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   159
        (etac (monofun_snd RS ch2ch_monofun) 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   160
        (etac (monofun_snd RS ub2ub_monofun) 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   161
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   162
1779
1155c06fa956 introduced forgotten bind_thm calls
oheimb
parents: 1461
diff changeset
   163
bind_thm ("thelub_cprod", lub_cprod RS thelubI);
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 899
diff changeset
   164
(*
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 899
diff changeset
   165
"is_chain ?S1 ==>
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 899
diff changeset
   166
 lub (range ?S1) =
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 899
diff changeset
   167
 (lub (range (%i. fst (?S1 i))), lub (range (%i. snd (?S1 i))))" : thm
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   168
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 899
diff changeset
   169
*)
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   170
892
d0dc8d057929 added qed, qed_goal[w]
clasohm
parents: 243
diff changeset
   171
qed_goal "cpo_cprod" Cprod2.thy 
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   172
        "is_chain(S::nat=>'a*'b)==>? x.range(S)<<| x"
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   173
(fn prems =>
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   174
        [
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   175
        (cut_facts_tac prems 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   176
        (rtac exI 1),
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   177
        (etac lub_cprod 1)
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1267
diff changeset
   178
        ]);
243
c22b85994e17 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff changeset
   179
1168
74be52691d62 The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents: 899
diff changeset
   180