src/HOLCF/Up1.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 4098 71e05eb27fb6
child 6543 da7b170fc8a7
permissions -rw-r--r--
tidying
oheimb@2278
     1
(*  Title:      HOLCF/Up1.ML
oheimb@2278
     2
    ID:         $Id$
oheimb@2278
     3
    Author:     Franz Regensburger
oheimb@2278
     4
    Copyright   1993  Technische Universitaet Muenchen
oheimb@2278
     5
*)
oheimb@2278
     6
oheimb@2278
     7
open Up1;
oheimb@2278
     8
slotosch@2640
     9
qed_goal "Abs_Up_inverse2" thy "Rep_Up (Abs_Up y) = y"
slotosch@2640
    10
 (fn prems =>
slotosch@2640
    11
        [
wenzelm@4098
    12
	(simp_tac (simpset() addsimps [Up_def,Abs_Up_inverse]) 1)
slotosch@2640
    13
	]);
slotosch@2640
    14
slotosch@2640
    15
qed_goalw "Exh_Up" thy [Iup_def ]
slotosch@2640
    16
        "z = Abs_Up(Inl ()) | (? x. z = Iup x)"
oheimb@2278
    17
 (fn prems =>
oheimb@2278
    18
        [
oheimb@2278
    19
        (rtac (Rep_Up_inverse RS subst) 1),
slotosch@2640
    20
        (res_inst_tac [("s","Rep_Up z")] sumE 1),
oheimb@2278
    21
        (rtac disjI1 1),
oheimb@2278
    22
        (res_inst_tac [("f","Abs_Up")] arg_cong 1),
slotosch@2640
    23
        (rtac (unit_eq RS subst) 1),
oheimb@2278
    24
        (atac 1),
oheimb@2278
    25
        (rtac disjI2 1),
oheimb@2278
    26
        (rtac exI 1),
oheimb@2278
    27
        (res_inst_tac [("f","Abs_Up")] arg_cong 1),
oheimb@2278
    28
        (atac 1)
oheimb@2278
    29
        ]);
oheimb@2278
    30
slotosch@2640
    31
qed_goal "inj_Abs_Up" thy "inj(Abs_Up)"
oheimb@2278
    32
 (fn prems =>
oheimb@2278
    33
        [
oheimb@2278
    34
        (rtac inj_inverseI 1),
slotosch@2640
    35
        (rtac Abs_Up_inverse2 1)
oheimb@2278
    36
        ]);
oheimb@2278
    37
slotosch@2640
    38
qed_goal "inj_Rep_Up" thy "inj(Rep_Up)"
oheimb@2278
    39
 (fn prems =>
oheimb@2278
    40
        [
oheimb@2278
    41
        (rtac inj_inverseI 1),
oheimb@2278
    42
        (rtac Rep_Up_inverse 1)
oheimb@2278
    43
        ]);
oheimb@2278
    44
slotosch@2640
    45
qed_goalw "inject_Iup" thy [Iup_def] "Iup x=Iup y ==> x=y"
oheimb@2278
    46
 (fn prems =>
oheimb@2278
    47
        [
oheimb@2278
    48
        (cut_facts_tac prems 1),
oheimb@2278
    49
        (rtac (inj_Inr RS injD) 1),
oheimb@2278
    50
        (rtac (inj_Abs_Up RS injD) 1),
oheimb@2278
    51
        (atac 1)
oheimb@2278
    52
        ]);
oheimb@2278
    53
slotosch@2640
    54
qed_goalw "defined_Iup" thy [Iup_def] "Iup x~=Abs_Up(Inl ())"
oheimb@2278
    55
 (fn prems =>
oheimb@2278
    56
        [
oheimb@2278
    57
        (rtac notI 1),
oheimb@2278
    58
        (rtac notE 1),
oheimb@2278
    59
        (rtac Inl_not_Inr 1),
oheimb@2278
    60
        (rtac sym 1),
oheimb@2278
    61
        (etac (inj_Abs_Up RS  injD) 1)
oheimb@2278
    62
        ]);
oheimb@2278
    63
oheimb@2278
    64
slotosch@2640
    65
qed_goal "upE"  thy
slotosch@2640
    66
        "[| p=Abs_Up(Inl ()) ==> Q; !!x. p=Iup(x)==>Q|] ==>Q"
oheimb@2278
    67
 (fn prems =>
oheimb@2278
    68
        [
oheimb@2278
    69
        (rtac (Exh_Up RS disjE) 1),
oheimb@2278
    70
        (eresolve_tac prems 1),
oheimb@2278
    71
        (etac exE 1),
oheimb@2278
    72
        (eresolve_tac prems 1)
oheimb@2278
    73
        ]);
oheimb@2278
    74
slotosch@2640
    75
qed_goalw "Ifup1"  thy [Ifup_def]
slotosch@2640
    76
        "Ifup(f)(Abs_Up(Inl ()))=UU"
oheimb@2278
    77
 (fn prems =>
oheimb@2278
    78
        [
slotosch@2640
    79
        (stac Abs_Up_inverse2 1),
oheimb@2278
    80
        (stac sum_case_Inl 1),
oheimb@2278
    81
        (rtac refl 1)
oheimb@2278
    82
        ]);
oheimb@2278
    83
slotosch@2640
    84
qed_goalw "Ifup2"  thy [Ifup_def,Iup_def]
oheimb@2278
    85
        "Ifup(f)(Iup(x))=f`x"
oheimb@2278
    86
 (fn prems =>
oheimb@2278
    87
        [
slotosch@2640
    88
        (stac Abs_Up_inverse2 1),
oheimb@2278
    89
        (stac sum_case_Inr 1),
oheimb@2278
    90
        (rtac refl 1)
oheimb@2278
    91
        ]);
oheimb@2278
    92
wenzelm@4098
    93
val Up0_ss = (simpset_of Cfun3.thy) addsimps [Ifup1,Ifup2];
oheimb@2278
    94
slotosch@2640
    95
qed_goalw "less_up1a"  thy [less_up_def]
slotosch@3323
    96
        "Abs_Up(Inl ())<< z"
oheimb@2278
    97
 (fn prems =>
oheimb@2278
    98
        [
slotosch@2640
    99
        (stac Abs_Up_inverse2 1),
oheimb@2278
   100
        (stac sum_case_Inl 1),
oheimb@2278
   101
        (rtac TrueI 1)
oheimb@2278
   102
        ]);
oheimb@2278
   103
slotosch@2640
   104
qed_goalw "less_up1b" thy [Iup_def,less_up_def]
slotosch@3323
   105
        "~(Iup x) << (Abs_Up(Inl ()))"
oheimb@2278
   106
 (fn prems =>
oheimb@2278
   107
        [
oheimb@2278
   108
        (rtac notI 1),
oheimb@2278
   109
        (rtac iffD1 1),
oheimb@2278
   110
        (atac 2),
slotosch@2640
   111
        (stac Abs_Up_inverse2 1),
slotosch@2640
   112
        (stac Abs_Up_inverse2 1),
oheimb@2278
   113
        (stac sum_case_Inr 1),
oheimb@2278
   114
        (stac sum_case_Inl 1),
oheimb@2278
   115
        (rtac refl 1)
oheimb@2278
   116
        ]);
oheimb@2278
   117
slotosch@2640
   118
qed_goalw "less_up1c"  thy [Iup_def,less_up_def]
slotosch@3323
   119
        " (Iup x) << (Iup y)=(x<<y)"
oheimb@2278
   120
 (fn prems =>
oheimb@2278
   121
        [
slotosch@2640
   122
        (stac Abs_Up_inverse2 1),
slotosch@2640
   123
        (stac Abs_Up_inverse2 1),
oheimb@2278
   124
        (stac sum_case_Inr 1),
oheimb@2278
   125
        (stac sum_case_Inr 1),
oheimb@2278
   126
        (rtac refl 1)
oheimb@2278
   127
        ]);
oheimb@2278
   128
oheimb@2278
   129
slotosch@3323
   130
qed_goal "refl_less_up"  thy "(p::'a u) << p"
oheimb@2278
   131
 (fn prems =>
oheimb@2278
   132
        [
oheimb@2278
   133
        (res_inst_tac [("p","p")] upE 1),
oheimb@2278
   134
        (hyp_subst_tac 1),
oheimb@2278
   135
        (rtac less_up1a 1),
oheimb@2278
   136
        (hyp_subst_tac 1),
oheimb@2278
   137
        (rtac (less_up1c RS iffD2) 1),
oheimb@2278
   138
        (rtac refl_less 1)
oheimb@2278
   139
        ]);
oheimb@2278
   140
slotosch@2640
   141
qed_goal "antisym_less_up"  thy 
slotosch@3323
   142
        "!!p1.[|(p1::'a u) << p2;p2 << p1|] ==> p1=p2"
oheimb@2278
   143
 (fn _ =>
oheimb@2278
   144
        [
oheimb@2278
   145
        (res_inst_tac [("p","p1")] upE 1),
oheimb@2278
   146
        (hyp_subst_tac 1),
oheimb@2278
   147
        (res_inst_tac [("p","p2")] upE 1),
oheimb@2278
   148
        (etac sym 1),
oheimb@2278
   149
        (hyp_subst_tac 1),
slotosch@3323
   150
        (res_inst_tac [("P","(Iup x) << (Abs_Up(Inl ()))")] notE 1),
oheimb@2278
   151
        (rtac less_up1b 1),
oheimb@2278
   152
        (atac 1),
oheimb@2278
   153
        (hyp_subst_tac 1),
oheimb@2278
   154
        (res_inst_tac [("p","p2")] upE 1),
oheimb@2278
   155
        (hyp_subst_tac 1),
slotosch@3323
   156
        (res_inst_tac [("P","(Iup x) << (Abs_Up(Inl ()))")] notE 1),
oheimb@2278
   157
        (rtac less_up1b 1),
oheimb@2278
   158
        (atac 1),
oheimb@2278
   159
        (hyp_subst_tac 1),
oheimb@2278
   160
        (rtac arg_cong 1),
oheimb@2278
   161
        (rtac antisym_less 1),
oheimb@2278
   162
        (etac (less_up1c RS iffD1) 1),
oheimb@2278
   163
        (etac (less_up1c RS iffD1) 1)
oheimb@2278
   164
        ]);
oheimb@2278
   165
slotosch@2640
   166
qed_goal "trans_less_up"  thy 
slotosch@3323
   167
        "[|(p1::'a u) << p2;p2 << p3|] ==> p1 << p3"
oheimb@2278
   168
 (fn prems =>
oheimb@2278
   169
        [
oheimb@2278
   170
        (cut_facts_tac prems 1),
oheimb@2278
   171
        (res_inst_tac [("p","p1")] upE 1),
oheimb@2278
   172
        (hyp_subst_tac 1),
oheimb@2278
   173
        (rtac less_up1a 1),
oheimb@2278
   174
        (hyp_subst_tac 1),
oheimb@2278
   175
        (res_inst_tac [("p","p2")] upE 1),
oheimb@2278
   176
        (hyp_subst_tac 1),
oheimb@2278
   177
        (rtac notE 1),
oheimb@2278
   178
        (rtac less_up1b 1),
oheimb@2278
   179
        (atac 1),
oheimb@2278
   180
        (hyp_subst_tac 1),
oheimb@2278
   181
        (res_inst_tac [("p","p3")] upE 1),
oheimb@2278
   182
        (hyp_subst_tac 1),
oheimb@2278
   183
        (rtac notE 1),
oheimb@2278
   184
        (rtac less_up1b 1),
oheimb@2278
   185
        (atac 1),
oheimb@2278
   186
        (hyp_subst_tac 1),
oheimb@2278
   187
        (rtac (less_up1c RS iffD2) 1),
oheimb@2278
   188
        (rtac trans_less 1),
oheimb@2278
   189
        (etac (less_up1c RS iffD1) 1),
oheimb@2278
   190
        (etac (less_up1c RS iffD1) 1)
oheimb@2278
   191
        ]);
oheimb@2278
   192