src/HOLCF/Up1.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
oheimb@2278
     1
(*  Title:      HOLCF/Up1.ML
oheimb@2278
     2
    ID:         $Id$
oheimb@2278
     3
    Author:     Franz Regensburger
paulson@9245
     4
wenzelm@12030
     5
Lifting.
oheimb@2278
     6
*)
oheimb@2278
     7
paulson@9169
     8
Goal "Rep_Up (Abs_Up y) = y";
paulson@9169
     9
by (simp_tac (simpset() addsimps [Up_def,Abs_Up_inverse]) 1);
paulson@9169
    10
qed "Abs_Up_inverse2";
slotosch@2640
    11
paulson@9248
    12
Goalw [Iup_def] "z = Abs_Up(Inl ()) | (? x. z = Iup x)";
paulson@9245
    13
by (rtac (Rep_Up_inverse RS subst) 1);
paulson@9245
    14
by (res_inst_tac [("s","Rep_Up z")] sumE 1);
paulson@9245
    15
by (rtac disjI1 1);
paulson@9245
    16
by (res_inst_tac [("f","Abs_Up")] arg_cong 1);
paulson@9245
    17
by (rtac (unit_eq RS subst) 1);
paulson@9245
    18
by (atac 1);
paulson@9245
    19
by (rtac disjI2 1);
paulson@9245
    20
by (rtac exI 1);
paulson@9245
    21
by (res_inst_tac [("f","Abs_Up")] arg_cong 1);
paulson@9245
    22
by (atac 1);
paulson@9245
    23
qed "Exh_Up";
oheimb@2278
    24
paulson@9169
    25
Goal "inj(Abs_Up)";
paulson@9169
    26
by (rtac inj_inverseI 1);
paulson@9169
    27
by (rtac Abs_Up_inverse2 1);
paulson@9169
    28
qed "inj_Abs_Up";
oheimb@2278
    29
paulson@9169
    30
Goal "inj(Rep_Up)";
paulson@9169
    31
by (rtac inj_inverseI 1);
paulson@9169
    32
by (rtac Rep_Up_inverse 1);
paulson@9169
    33
qed "inj_Rep_Up";
oheimb@2278
    34
paulson@9248
    35
Goalw [Iup_def] "Iup x=Iup y ==> x=y";
paulson@9245
    36
by (rtac (inj_Inr RS injD) 1);
paulson@9245
    37
by (rtac (inj_Abs_Up RS injD) 1);
paulson@9245
    38
by (atac 1);
paulson@9245
    39
qed "inject_Iup";
oheimb@2278
    40
paulson@9169
    41
AddSDs [inject_Iup];
paulson@9169
    42
paulson@9248
    43
Goalw [Iup_def] "Iup x~=Abs_Up(Inl ())";
paulson@9245
    44
by (rtac notI 1);
paulson@9245
    45
by (rtac notE 1);
paulson@9245
    46
by (rtac Inl_not_Inr 1);
paulson@9245
    47
by (rtac sym 1);
paulson@9245
    48
by (etac (inj_Abs_Up RS  injD) 1);
paulson@9245
    49
qed "defined_Iup";
oheimb@2278
    50
oheimb@2278
    51
paulson@9169
    52
val prems = Goal "[| p=Abs_Up(Inl ()) ==> Q; !!x. p=Iup(x)==>Q|] ==>Q";
paulson@9169
    53
by (rtac (Exh_Up RS disjE) 1);
paulson@9169
    54
by (eresolve_tac prems 1);
paulson@9169
    55
by (etac exE 1);
paulson@9169
    56
by (eresolve_tac prems 1);
paulson@9169
    57
qed "upE";
oheimb@2278
    58
paulson@9248
    59
Goalw [Ifup_def] "Ifup(f)(Abs_Up(Inl ()))=UU";
paulson@9245
    60
by (stac Abs_Up_inverse2 1);
paulson@9245
    61
by (stac sum_case_Inl 1);
paulson@9245
    62
by (rtac refl 1);
paulson@9245
    63
qed "Ifup1";
oheimb@2278
    64
paulson@9248
    65
Goalw [Ifup_def,Iup_def]
nipkow@10834
    66
        "Ifup(f)(Iup(x))=f$x";
paulson@9245
    67
by (stac Abs_Up_inverse2 1);
paulson@9245
    68
by (stac sum_case_Inr 1);
paulson@9245
    69
by (rtac refl 1);
paulson@9245
    70
qed "Ifup2";
oheimb@2278
    71
oheimb@8161
    72
val Up0_ss = (simpset_of Cfun3.thy) delsimps [range_composition] 
oheimb@8161
    73
	     addsimps [Ifup1,Ifup2];
oheimb@2278
    74
paulson@9169
    75
Addsimps [Ifup1,Ifup2];
paulson@9169
    76
paulson@9248
    77
Goalw [less_up_def]
paulson@9245
    78
        "Abs_Up(Inl ())<< z";
paulson@9245
    79
by (stac Abs_Up_inverse2 1);
paulson@9245
    80
by (stac sum_case_Inl 1);
paulson@9245
    81
by (rtac TrueI 1);
paulson@9245
    82
qed "less_up1a";
oheimb@2278
    83
paulson@9248
    84
Goalw [Iup_def,less_up_def]
paulson@9245
    85
        "~(Iup x) << (Abs_Up(Inl ()))";
paulson@9245
    86
by (rtac notI 1);
paulson@9245
    87
by (rtac iffD1 1);
paulson@9245
    88
by (atac 2);
paulson@9245
    89
by (stac Abs_Up_inverse2 1);
paulson@9245
    90
by (stac Abs_Up_inverse2 1);
paulson@9245
    91
by (stac sum_case_Inr 1);
paulson@9245
    92
by (stac sum_case_Inl 1);
paulson@9245
    93
by (rtac refl 1);
paulson@9245
    94
qed "less_up1b";
oheimb@2278
    95
paulson@9248
    96
Goalw [Iup_def,less_up_def]
paulson@9245
    97
        "(Iup x) << (Iup y)=(x<<y)";
paulson@9245
    98
by (stac Abs_Up_inverse2 1);
paulson@9245
    99
by (stac Abs_Up_inverse2 1);
paulson@9245
   100
by (stac sum_case_Inr 1);
paulson@9245
   101
by (stac sum_case_Inr 1);
paulson@9245
   102
by (rtac refl 1);
paulson@9245
   103
qed "less_up1c";
oheimb@2278
   104
paulson@9169
   105
AddIffs [less_up1a, less_up1b, less_up1c];
oheimb@2278
   106
paulson@9169
   107
Goal "(p::'a u) << p";
paulson@9169
   108
by (res_inst_tac [("p","p")] upE 1);
paulson@9169
   109
by Auto_tac;
paulson@9169
   110
qed "refl_less_up";
oheimb@2278
   111
paulson@9169
   112
Goal "[|(p1::'a u) << p2;p2 << p1|] ==> p1=p2";
paulson@9169
   113
by (res_inst_tac [("p","p1")] upE 1);
paulson@9169
   114
by (hyp_subst_tac 1);
paulson@9169
   115
by (res_inst_tac [("p","p2")] upE 1);
paulson@9169
   116
by (etac sym 1);
paulson@9169
   117
by (hyp_subst_tac 1);
paulson@9169
   118
by (res_inst_tac [("P","(Iup x) << (Abs_Up(Inl ()))")] notE 1);
paulson@9169
   119
by (rtac less_up1b 1);
paulson@9169
   120
by (atac 1);
paulson@9169
   121
by (hyp_subst_tac 1);
paulson@9169
   122
by (res_inst_tac [("p","p2")] upE 1);
paulson@9169
   123
by (hyp_subst_tac 1);
paulson@9169
   124
by (res_inst_tac [("P","(Iup x) << (Abs_Up(Inl ()))")] notE 1);
paulson@9169
   125
by (rtac less_up1b 1);
paulson@9169
   126
by (atac 1);
paulson@9169
   127
by (blast_tac (claset() addIs [arg_cong, antisym_less, less_up1c RS iffD1]) 1);
paulson@9169
   128
qed "antisym_less_up";
oheimb@2278
   129
paulson@9169
   130
Goal "[|(p1::'a u) << p2;p2 << p3|] ==> p1 << p3";
paulson@9169
   131
by (res_inst_tac [("p","p1")] upE 1);
paulson@9169
   132
by (hyp_subst_tac 1);
paulson@9169
   133
by (rtac less_up1a 1);
paulson@9169
   134
by (hyp_subst_tac 1);
paulson@9169
   135
by (res_inst_tac [("p","p2")] upE 1);
paulson@9169
   136
by (hyp_subst_tac 1);
paulson@9169
   137
by (rtac notE 1);
paulson@9169
   138
by (rtac less_up1b 1);
paulson@9169
   139
by (atac 1);
paulson@9169
   140
by (res_inst_tac [("p","p3")] upE 1);
paulson@9169
   141
by Auto_tac;
paulson@9169
   142
by (blast_tac (claset() addIs [trans_less]) 1);
paulson@9169
   143
qed "trans_less_up";
oheimb@2278
   144