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