src/HOLCF/Sprod2.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 4721 c8a8482a8124
child 7499 23e090051cb8
permissions -rw-r--r--
made tutorial first;
slotosch@2640
     1
(*  Title:      HOLCF/Sprod2.ML
nipkow@243
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Franz Regensburger
nipkow@243
     4
    Copyright   1993 Technische Universitaet Muenchen
nipkow@243
     5
slotosch@2640
     6
Lemmas for Sprod2.thy
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
open Sprod2;
nipkow@243
    10
slotosch@2640
    11
(* for compatibility with old HOLCF-Version *)
wenzelm@3842
    12
qed_goal "inst_sprod_po" thy "(op <<)=(%x y. Isfst x<<Isfst y&Issnd x<<Issnd y)"
slotosch@2640
    13
 (fn prems => 
clasohm@1461
    14
        [
slotosch@3323
    15
	(fold_goals_tac [less_sprod_def]),
slotosch@2640
    16
	(rtac refl 1)
clasohm@1461
    17
        ]);
nipkow@243
    18
nipkow@243
    19
(* ------------------------------------------------------------------------ *)
nipkow@243
    20
(* type sprod is pointed                                                    *)
nipkow@243
    21
(* ------------------------------------------------------------------------ *)
nipkow@243
    22
slotosch@2640
    23
qed_goal "minimal_sprod" thy "Ispair UU UU << p"
nipkow@243
    24
(fn prems =>
clasohm@1461
    25
        [
slotosch@2640
    26
        (simp_tac(Sprod0_ss addsimps[inst_sprod_po,minimal])1)
slotosch@2640
    27
        ]);
slotosch@2640
    28
slotosch@2640
    29
bind_thm ("UU_sprod_def",minimal_sprod RS minimal2UU RS sym);
slotosch@2640
    30
wenzelm@3842
    31
qed_goal "least_sprod" thy "? x::'a**'b.!y. x<<y"
slotosch@2640
    32
(fn prems =>
slotosch@2640
    33
        [
slotosch@2640
    34
        (res_inst_tac [("x","Ispair UU UU")] exI 1),
slotosch@2640
    35
        (rtac (minimal_sprod RS allI) 1)
clasohm@1461
    36
        ]);
nipkow@243
    37
nipkow@243
    38
(* ------------------------------------------------------------------------ *)
nipkow@243
    39
(* Ispair is monotone in both arguments                                     *)
nipkow@243
    40
(* ------------------------------------------------------------------------ *)
nipkow@243
    41
clasohm@892
    42
qed_goalw "monofun_Ispair1" Sprod2.thy [monofun] "monofun(Ispair)"
nipkow@243
    43
(fn prems =>
clasohm@1461
    44
        [
clasohm@1461
    45
        (strip_tac 1),
clasohm@1461
    46
        (rtac (less_fun RS iffD2) 1),
clasohm@1461
    47
        (strip_tac 1),
slotosch@2640
    48
        (res_inst_tac [("Q","xa=UU")] (excluded_middle RS disjE) 1),
slotosch@2640
    49
        (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
slotosch@2640
    50
        (forward_tac [notUU_I] 1),
clasohm@1461
    51
        (atac 1),
slotosch@2640
    52
        (REPEAT(asm_simp_tac(Sprod0_ss 
slotosch@2640
    53
                addsimps[inst_sprod_po,refl_less,minimal]) 1))
clasohm@1461
    54
        ]);
nipkow@243
    55
clasohm@892
    56
qed_goalw "monofun_Ispair2" Sprod2.thy [monofun] "monofun(Ispair(x))"
nipkow@243
    57
(fn prems =>
clasohm@1461
    58
        [
clasohm@1461
    59
        (strip_tac 1),
slotosch@2640
    60
        (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
slotosch@2640
    61
        (res_inst_tac [("Q","xa=UU")] (excluded_middle RS disjE) 1),
slotosch@2640
    62
        (forward_tac [notUU_I] 1),
clasohm@1461
    63
        (atac 1),
slotosch@2640
    64
        (REPEAT(asm_simp_tac(Sprod0_ss 
slotosch@2640
    65
                addsimps[inst_sprod_po,refl_less,minimal]) 1))
clasohm@1461
    66
        ]);
nipkow@243
    67
slotosch@2640
    68
wenzelm@4031
    69
qed_goal "monofun_Ispair" Sprod2.thy 
regensbu@1168
    70
 "[|x1<<x2; y1<<y2|] ==> Ispair x1 y1 << Ispair x2 y2"
nipkow@243
    71
(fn prems =>
clasohm@1461
    72
        [
clasohm@1461
    73
        (cut_facts_tac prems 1),
clasohm@1461
    74
        (rtac trans_less 1),
clasohm@1461
    75
        (rtac (monofun_Ispair1 RS monofunE RS spec RS spec RS mp RS 
clasohm@1461
    76
        (less_fun RS iffD1 RS spec)) 1),
clasohm@1461
    77
        (rtac (monofun_Ispair2 RS monofunE RS spec RS spec RS mp) 2),
clasohm@1461
    78
        (atac 1),
clasohm@1461
    79
        (atac 1)
clasohm@1461
    80
        ]);
nipkow@243
    81
nipkow@243
    82
nipkow@243
    83
(* ------------------------------------------------------------------------ *)
nipkow@243
    84
(* Isfst and Issnd are monotone                                             *)
nipkow@243
    85
(* ------------------------------------------------------------------------ *)
nipkow@243
    86
slotosch@2640
    87
qed_goalw "monofun_Isfst" Sprod2.thy [monofun] "monofun(Isfst)"
slotosch@2640
    88
(fn prems => [(simp_tac (HOL_ss addsimps [inst_sprod_po]) 1)]);
nipkow@243
    89
clasohm@892
    90
qed_goalw "monofun_Issnd" Sprod2.thy [monofun] "monofun(Issnd)"
slotosch@2640
    91
(fn prems => [(simp_tac (HOL_ss addsimps [inst_sprod_po]) 1)]);
nipkow@243
    92
nipkow@243
    93
(* ------------------------------------------------------------------------ *)
nipkow@243
    94
(* the type 'a ** 'b is a cpo                                               *)
nipkow@243
    95
(* ------------------------------------------------------------------------ *)
nipkow@243
    96
clasohm@892
    97
qed_goal "lub_sprod" Sprod2.thy 
oheimb@4721
    98
"[|chain(S)|] ==> range(S) <<| \
wenzelm@3842
    99
\ Ispair (lub(range(%i. Isfst(S i)))) (lub(range(%i. Issnd(S i))))"
nipkow@243
   100
(fn prems =>
clasohm@1461
   101
        [
clasohm@1461
   102
        (cut_facts_tac prems 1),
slotosch@2640
   103
        (rtac (conjI RS is_lubI) 1),
slotosch@2640
   104
        (rtac (allI RS ub_rangeI) 1),
clasohm@1461
   105
        (res_inst_tac [("t","S(i)")] (surjective_pairing_Sprod RS ssubst) 1),
clasohm@1461
   106
        (rtac monofun_Ispair 1),
clasohm@1461
   107
        (rtac is_ub_thelub 1),
clasohm@1461
   108
        (etac (monofun_Isfst RS ch2ch_monofun) 1),
clasohm@1461
   109
        (rtac is_ub_thelub 1),
clasohm@1461
   110
        (etac (monofun_Issnd RS ch2ch_monofun) 1),
clasohm@1461
   111
        (strip_tac 1),
clasohm@1461
   112
        (res_inst_tac [("t","u")] (surjective_pairing_Sprod RS ssubst) 1),
clasohm@1461
   113
        (rtac monofun_Ispair 1),
clasohm@1461
   114
        (rtac is_lub_thelub 1),
clasohm@1461
   115
        (etac (monofun_Isfst RS ch2ch_monofun) 1),
clasohm@1461
   116
        (etac (monofun_Isfst RS ub2ub_monofun) 1),
clasohm@1461
   117
        (rtac is_lub_thelub 1),
clasohm@1461
   118
        (etac (monofun_Issnd RS ch2ch_monofun) 1),
clasohm@1461
   119
        (etac (monofun_Issnd RS ub2ub_monofun) 1)
clasohm@1461
   120
        ]);
nipkow@243
   121
oheimb@1779
   122
bind_thm ("thelub_sprod", lub_sprod RS thelubI);
regensbu@1168
   123
nipkow@243
   124
clasohm@892
   125
qed_goal "cpo_sprod" Sprod2.thy 
oheimb@4721
   126
        "chain(S::nat=>'a**'b)==>? x. range(S)<<| x"
nipkow@243
   127
(fn prems =>
clasohm@1461
   128
        [
clasohm@1461
   129
        (cut_facts_tac prems 1),
clasohm@1461
   130
        (rtac exI 1),
clasohm@1461
   131
        (etac lub_sprod 1)
clasohm@1461
   132
        ]);
nipkow@243
   133
nipkow@243
   134
nipkow@243
   135
nipkow@243
   136
nipkow@243
   137
nipkow@243
   138
nipkow@243
   139
nipkow@243
   140