src/HOLCF/Cprod2.ML
author paulson
Tue Jul 04 15:58:11 2000 +0200 (2000-07-04)
changeset 9245 428385c4bc50
parent 4721 c8a8482a8124
child 9248 e1dee89de037
permissions -rw-r--r--
removed most batch-style proofs
paulson@9245
     1
(*  Title:      HOLCF/Cprod2
nipkow@243
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Franz Regensburger
nipkow@243
     4
    Copyright   1993 Technische Universitaet Muenchen
nipkow@243
     5
paulson@9245
     6
Class Instance *::(pcpo,pcpo)po
nipkow@243
     7
*)
nipkow@243
     8
slotosch@2640
     9
(* for compatibility with old HOLCF-Version *)
paulson@9245
    10
val prems = goal thy "(op <<)=(%x y. fst x<<fst y & snd x<<snd y)";
paulson@9245
    11
by (fold_goals_tac [less_cprod_def]);
paulson@9245
    12
by (rtac refl 1);
paulson@9245
    13
qed "inst_cprod_po";
slotosch@2640
    14
paulson@9245
    15
val prems = goalw thy [inst_cprod_po RS eq_reflection] 
paulson@9245
    16
 "(x1,y1) << (x2,y2) ==> x1 << x2 & y1 << y2";
paulson@9245
    17
by (cut_facts_tac prems 1);
paulson@9245
    18
by (etac conjE 1);
paulson@9245
    19
by (dtac (fst_conv RS subst) 1);
paulson@9245
    20
by (dtac (fst_conv RS subst) 1);
paulson@9245
    21
by (dtac (fst_conv RS subst) 1);
paulson@9245
    22
by (dtac (snd_conv RS subst) 1);
paulson@9245
    23
by (dtac (snd_conv RS subst) 1);
paulson@9245
    24
by (dtac (snd_conv RS subst) 1);
paulson@9245
    25
by (rtac conjI 1);
paulson@9245
    26
by (atac 1);
paulson@9245
    27
by (atac 1);
paulson@9245
    28
qed "less_cprod4c";
nipkow@243
    29
nipkow@243
    30
(* ------------------------------------------------------------------------ *)
nipkow@243
    31
(* type cprod is pointed                                                    *)
nipkow@243
    32
(* ------------------------------------------------------------------------ *)
nipkow@243
    33
paulson@9245
    34
val prems = goal thy  "(UU,UU)<<p";
paulson@9245
    35
by (simp_tac(simpset() addsimps[inst_cprod_po])1);
paulson@9245
    36
qed "minimal_cprod";
slotosch@2640
    37
slotosch@2640
    38
bind_thm ("UU_cprod_def",minimal_cprod RS minimal2UU RS sym);
slotosch@2640
    39
paulson@9245
    40
val prems = goal thy "? x::'a*'b.!y. x<<y";
paulson@9245
    41
by (res_inst_tac [("x","(UU,UU)")] exI 1);
paulson@9245
    42
by (rtac (minimal_cprod RS allI) 1);
paulson@9245
    43
qed "least_cprod";
nipkow@243
    44
nipkow@243
    45
(* ------------------------------------------------------------------------ *)
nipkow@243
    46
(* Pair <_,_>  is monotone in both arguments                                *)
nipkow@243
    47
(* ------------------------------------------------------------------------ *)
nipkow@243
    48
paulson@9245
    49
val prems = goalw thy [monofun]  "monofun Pair";
paulson@9245
    50
by (strip_tac 1);
paulson@9245
    51
by (rtac (less_fun RS iffD2) 1);
paulson@9245
    52
by (strip_tac 1);
paulson@9245
    53
by (asm_simp_tac (simpset() addsimps [inst_cprod_po]) 1);
paulson@9245
    54
qed "monofun_pair1";
nipkow@243
    55
paulson@9245
    56
val prems = goalw thy [monofun]  "monofun(Pair x)";
paulson@9245
    57
by (asm_simp_tac (simpset() addsimps [inst_cprod_po]) 1);
paulson@9245
    58
qed "monofun_pair2";
nipkow@243
    59
paulson@9245
    60
val prems = goal thy "[|x1<<x2; y1<<y2|] ==> (x1::'a::cpo,y1::'b::cpo)<<(x2,y2)";
paulson@9245
    61
by (cut_facts_tac prems 1);
paulson@9245
    62
by (rtac trans_less 1);
paulson@9245
    63
by (rtac (monofun_pair1 RS monofunE RS spec RS spec RS mp RS (less_fun RS iffD1 RS spec)) 1);
paulson@9245
    64
by (rtac (monofun_pair2 RS monofunE RS spec RS spec RS mp) 2);
paulson@9245
    65
by (atac 1);
paulson@9245
    66
by (atac 1);
paulson@9245
    67
qed "monofun_pair";
nipkow@243
    68
nipkow@243
    69
(* ------------------------------------------------------------------------ *)
nipkow@243
    70
(* fst and snd are monotone                                                 *)
nipkow@243
    71
(* ------------------------------------------------------------------------ *)
nipkow@243
    72
paulson@9245
    73
val prems = goalw thy [monofun]  "monofun fst";
paulson@9245
    74
by (strip_tac 1);
paulson@9245
    75
by (res_inst_tac [("p","x")] PairE 1);
paulson@9245
    76
by (hyp_subst_tac 1);
paulson@9245
    77
by (res_inst_tac [("p","y")] PairE 1);
paulson@9245
    78
by (hyp_subst_tac 1);
paulson@9245
    79
by (Asm_simp_tac  1);
paulson@9245
    80
by (etac (less_cprod4c RS conjunct1) 1);
paulson@9245
    81
qed "monofun_fst";
nipkow@243
    82
paulson@9245
    83
val prems = goalw thy [monofun]  "monofun snd";
paulson@9245
    84
by (strip_tac 1);
paulson@9245
    85
by (res_inst_tac [("p","x")] PairE 1);
paulson@9245
    86
by (hyp_subst_tac 1);
paulson@9245
    87
by (res_inst_tac [("p","y")] PairE 1);
paulson@9245
    88
by (hyp_subst_tac 1);
paulson@9245
    89
by (Asm_simp_tac  1);
paulson@9245
    90
by (etac (less_cprod4c RS conjunct2) 1);
paulson@9245
    91
qed "monofun_snd";
nipkow@243
    92
nipkow@243
    93
(* ------------------------------------------------------------------------ *)
nipkow@243
    94
(* the type 'a * 'b is a cpo                                                *)
nipkow@243
    95
(* ------------------------------------------------------------------------ *)
nipkow@243
    96
paulson@9245
    97
val prems = goal thy 
paulson@9245
    98
"chain S ==> range S<<|(lub(range(%i. fst(S i))),lub(range(%i. snd(S i))))";
paulson@9245
    99
by (cut_facts_tac prems 1);
paulson@9245
   100
by (rtac (conjI RS is_lubI) 1);
paulson@9245
   101
by (rtac (allI RS ub_rangeI) 1);
paulson@9245
   102
by (res_inst_tac [("t","S i")] (surjective_pairing RS ssubst) 1);
paulson@9245
   103
by (rtac monofun_pair 1);
paulson@9245
   104
by (rtac is_ub_thelub 1);
paulson@9245
   105
by (etac (monofun_fst RS ch2ch_monofun) 1);
paulson@9245
   106
by (rtac is_ub_thelub 1);
paulson@9245
   107
by (etac (monofun_snd RS ch2ch_monofun) 1);
paulson@9245
   108
by (strip_tac 1);
paulson@9245
   109
by (res_inst_tac [("t","u")] (surjective_pairing RS ssubst) 1);
paulson@9245
   110
by (rtac monofun_pair 1);
paulson@9245
   111
by (rtac is_lub_thelub 1);
paulson@9245
   112
by (etac (monofun_fst RS ch2ch_monofun) 1);
paulson@9245
   113
by (etac (monofun_fst RS ub2ub_monofun) 1);
paulson@9245
   114
by (rtac is_lub_thelub 1);
paulson@9245
   115
by (etac (monofun_snd RS ch2ch_monofun) 1);
paulson@9245
   116
by (etac (monofun_snd RS ub2ub_monofun) 1);
paulson@9245
   117
qed "lub_cprod";
nipkow@243
   118
oheimb@1779
   119
bind_thm ("thelub_cprod", lub_cprod RS thelubI);
regensbu@1168
   120
(*
oheimb@4721
   121
"chain ?S1 ==>
regensbu@1168
   122
 lub (range ?S1) =
regensbu@1168
   123
 (lub (range (%i. fst (?S1 i))), lub (range (%i. snd (?S1 i))))" : thm
nipkow@243
   124
regensbu@1168
   125
*)
nipkow@243
   126
paulson@9245
   127
val prems = goal thy "chain(S::nat=>'a::cpo*'b::cpo)==>? x. range S<<| x";
paulson@9245
   128
by (cut_facts_tac prems 1);
paulson@9245
   129
by (rtac exI 1);
paulson@9245
   130
by (etac lub_cprod 1);
paulson@9245
   131
qed "cpo_cprod";
nipkow@243
   132
regensbu@1168
   133