src/HOLCF/lift1.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 248 0d0a6a17a02f
permissions -rw-r--r--
made tutorial first;
nipkow@243
     1
(*  Title: 	HOLCF/lift1.ML
nipkow@243
     2
    ID:         $Id$
nipkow@243
     3
    Author: 	Franz Regensburger
nipkow@243
     4
    Copyright   1993  Technische Universitaet Muenchen
nipkow@243
     5
*)
nipkow@243
     6
nipkow@243
     7
open Lift1;
nipkow@243
     8
nipkow@243
     9
val Exh_Lift = prove_goalw Lift1.thy [UU_lift_def,Iup_def ]
nipkow@243
    10
	"z = UU_lift | (? x. z = Iup(x))"
nipkow@243
    11
 (fn prems =>
nipkow@243
    12
	[
nipkow@243
    13
	(rtac (Rep_Lift_inverse RS subst) 1),
nipkow@243
    14
	(res_inst_tac [("s","Rep_Lift(z)")] sumE 1),
nipkow@243
    15
	(rtac disjI1 1),
nipkow@243
    16
	(res_inst_tac [("f","Abs_Lift")] arg_cong 1),
nipkow@243
    17
	(rtac (unique_void2 RS subst) 1),
nipkow@243
    18
	(atac 1),
nipkow@243
    19
	(rtac disjI2 1),
nipkow@243
    20
	(rtac exI 1),
nipkow@243
    21
	(res_inst_tac [("f","Abs_Lift")] arg_cong 1),
nipkow@243
    22
	(atac 1)
nipkow@243
    23
	]);
nipkow@243
    24
nipkow@243
    25
val inj_Abs_Lift = prove_goal Lift1.thy "inj(Abs_Lift)"
nipkow@243
    26
 (fn prems =>
nipkow@243
    27
	[
nipkow@243
    28
	(rtac inj_inverseI 1),
nipkow@243
    29
	(rtac Abs_Lift_inverse 1)
nipkow@243
    30
	]);
nipkow@243
    31
nipkow@243
    32
val inj_Rep_Lift = prove_goal Lift1.thy "inj(Rep_Lift)"
nipkow@243
    33
 (fn prems =>
nipkow@243
    34
	[
nipkow@243
    35
	(rtac inj_inverseI 1),
nipkow@243
    36
	(rtac Rep_Lift_inverse 1)
nipkow@243
    37
	]);
nipkow@243
    38
nipkow@243
    39
val inject_Iup = prove_goalw Lift1.thy [Iup_def] "Iup(x)=Iup(y) ==> x=y"
nipkow@243
    40
 (fn prems =>
nipkow@243
    41
	[
nipkow@243
    42
	(cut_facts_tac prems 1),
nipkow@243
    43
	(rtac (inj_Inr RS injD) 1),
nipkow@243
    44
	(rtac (inj_Abs_Lift RS injD) 1),
nipkow@243
    45
	(atac 1)
nipkow@243
    46
	]);
nipkow@243
    47
nipkow@243
    48
val defined_Iup=prove_goalw Lift1.thy [Iup_def,UU_lift_def] "~ Iup(x)=UU_lift"
nipkow@243
    49
 (fn prems =>
nipkow@243
    50
	[
nipkow@243
    51
	(rtac notI 1),
nipkow@243
    52
	(rtac notE 1),
nipkow@243
    53
	(rtac Inl_not_Inr 1),
nipkow@243
    54
	(rtac sym 1),
nipkow@243
    55
	(etac (inj_Abs_Lift RS  injD) 1)
nipkow@243
    56
	]);
nipkow@243
    57
nipkow@243
    58
nipkow@243
    59
val liftE = prove_goal  Lift1.thy
nipkow@243
    60
	"[| p=UU_lift ==> Q; !!x. p=Iup(x)==>Q|] ==>Q"
nipkow@243
    61
 (fn prems =>
nipkow@243
    62
	[
nipkow@243
    63
	(rtac (Exh_Lift RS disjE) 1),
nipkow@243
    64
	(eresolve_tac prems 1),
nipkow@243
    65
	(etac exE 1),
nipkow@243
    66
	(eresolve_tac prems 1)
nipkow@243
    67
	]);
nipkow@243
    68
nipkow@243
    69
val Ilift1 = prove_goalw  Lift1.thy [Ilift_def,UU_lift_def]
nipkow@243
    70
	"Ilift(f)(UU_lift)=UU"
nipkow@243
    71
 (fn prems =>
nipkow@243
    72
	[
nipkow@243
    73
	(rtac (Abs_Lift_inverse RS ssubst) 1),
nipkow@248
    74
	(rtac (sum_case_Inl RS ssubst) 1),
nipkow@243
    75
	(rtac refl 1)
nipkow@243
    76
	]);
nipkow@243
    77
nipkow@243
    78
val Ilift2 = prove_goalw  Lift1.thy [Ilift_def,Iup_def]
nipkow@243
    79
	"Ilift(f)(Iup(x))=f[x]"
nipkow@243
    80
 (fn prems =>
nipkow@243
    81
	[
nipkow@243
    82
	(rtac (Abs_Lift_inverse RS ssubst) 1),
nipkow@248
    83
	(rtac (sum_case_Inr RS ssubst) 1),
nipkow@243
    84
	(rtac refl 1)
nipkow@243
    85
	]);
nipkow@243
    86
nipkow@243
    87
val Lift_ss = Cfun_ss addsimps [Ilift1,Ilift2];
nipkow@243
    88
nipkow@243
    89
val less_lift1a = prove_goalw  Lift1.thy [less_lift_def,UU_lift_def]
nipkow@243
    90
	"less_lift(UU_lift)(z)"
nipkow@243
    91
 (fn prems =>
nipkow@243
    92
	[
nipkow@243
    93
	(rtac (Abs_Lift_inverse RS ssubst) 1),
nipkow@248
    94
	(rtac (sum_case_Inl RS ssubst) 1),
nipkow@243
    95
	(rtac TrueI 1)
nipkow@243
    96
	]);
nipkow@243
    97
nipkow@243
    98
val less_lift1b = prove_goalw  Lift1.thy [Iup_def,less_lift_def,UU_lift_def]
nipkow@243
    99
	"~less_lift(Iup(x),UU_lift)"
nipkow@243
   100
 (fn prems =>
nipkow@243
   101
	[
nipkow@243
   102
	(rtac notI 1),
nipkow@243
   103
	(rtac iffD1 1),
nipkow@243
   104
	(atac 2),
nipkow@243
   105
	(rtac (Abs_Lift_inverse RS ssubst) 1),
nipkow@243
   106
	(rtac (Abs_Lift_inverse RS ssubst) 1),
nipkow@248
   107
	(rtac (sum_case_Inr RS ssubst) 1),
nipkow@248
   108
	(rtac (sum_case_Inl RS ssubst) 1),
nipkow@243
   109
	(rtac refl 1)
nipkow@243
   110
	]);
nipkow@243
   111
nipkow@243
   112
val less_lift1c = prove_goalw  Lift1.thy [Iup_def,less_lift_def,UU_lift_def]
nipkow@243
   113
	"less_lift(Iup(x),Iup(y))=(x<<y)"
nipkow@243
   114
 (fn prems =>
nipkow@243
   115
	[
nipkow@243
   116
	(rtac (Abs_Lift_inverse RS ssubst) 1),
nipkow@243
   117
	(rtac (Abs_Lift_inverse RS ssubst) 1),
nipkow@248
   118
	(rtac (sum_case_Inr RS ssubst) 1),
nipkow@248
   119
	(rtac (sum_case_Inr RS ssubst) 1),
nipkow@243
   120
	(rtac refl 1)
nipkow@243
   121
	]);
nipkow@243
   122
nipkow@243
   123
nipkow@243
   124
val refl_less_lift = prove_goal  Lift1.thy "less_lift(p,p)"
nipkow@243
   125
 (fn prems =>
nipkow@243
   126
	[
nipkow@243
   127
	(res_inst_tac [("p","p")] liftE 1),
nipkow@243
   128
	(hyp_subst_tac 1),
nipkow@243
   129
	(rtac less_lift1a 1),
nipkow@243
   130
	(hyp_subst_tac 1),
nipkow@243
   131
	(rtac (less_lift1c RS iffD2) 1),
nipkow@243
   132
	(rtac refl_less 1)
nipkow@243
   133
	]);
nipkow@243
   134
nipkow@243
   135
val antisym_less_lift = prove_goal  Lift1.thy 
nipkow@243
   136
	"[|less_lift(p1,p2);less_lift(p2,p1)|] ==> p1=p2"
nipkow@243
   137
 (fn prems =>
nipkow@243
   138
	[
nipkow@243
   139
	(cut_facts_tac prems 1),
nipkow@243
   140
	(res_inst_tac [("p","p1")] liftE 1),
nipkow@243
   141
	(hyp_subst_tac 1),
nipkow@243
   142
	(res_inst_tac [("p","p2")] liftE 1),
nipkow@243
   143
	(hyp_subst_tac 1),
nipkow@243
   144
	(rtac refl 1),
nipkow@243
   145
	(hyp_subst_tac 1),
nipkow@243
   146
	(res_inst_tac [("P","less_lift(Iup(x),UU_lift)")] notE 1),
nipkow@243
   147
	(rtac less_lift1b 1),
nipkow@243
   148
	(atac 1),
nipkow@243
   149
	(hyp_subst_tac 1),
nipkow@243
   150
	(res_inst_tac [("p","p2")] liftE 1),
nipkow@243
   151
	(hyp_subst_tac 1),
nipkow@243
   152
	(res_inst_tac [("P","less_lift(Iup(x),UU_lift)")] notE 1),
nipkow@243
   153
	(rtac less_lift1b 1),
nipkow@243
   154
	(atac 1),
nipkow@243
   155
	(hyp_subst_tac 1),
nipkow@243
   156
	(rtac arg_cong 1),
nipkow@243
   157
	(rtac antisym_less 1),
nipkow@243
   158
	(etac (less_lift1c RS iffD1) 1),
nipkow@243
   159
	(etac (less_lift1c RS iffD1) 1)
nipkow@243
   160
	]);
nipkow@243
   161
nipkow@243
   162
val trans_less_lift = prove_goal  Lift1.thy 
nipkow@243
   163
	"[|less_lift(p1,p2);less_lift(p2,p3)|] ==> less_lift(p1,p3)"
nipkow@243
   164
 (fn prems =>
nipkow@243
   165
	[
nipkow@243
   166
	(cut_facts_tac prems 1),
nipkow@243
   167
	(res_inst_tac [("p","p1")] liftE 1),
nipkow@243
   168
	(hyp_subst_tac 1),
nipkow@243
   169
	(rtac less_lift1a 1),
nipkow@243
   170
	(hyp_subst_tac 1),
nipkow@243
   171
	(res_inst_tac [("p","p2")] liftE 1),
nipkow@243
   172
	(hyp_subst_tac 1),
nipkow@243
   173
	(rtac notE 1),
nipkow@243
   174
	(rtac less_lift1b 1),
nipkow@243
   175
	(atac 1),
nipkow@243
   176
	(hyp_subst_tac 1),
nipkow@243
   177
	(res_inst_tac [("p","p3")] liftE 1),
nipkow@243
   178
	(hyp_subst_tac 1),
nipkow@243
   179
	(rtac notE 1),
nipkow@243
   180
	(rtac less_lift1b 1),
nipkow@243
   181
	(atac 1),
nipkow@243
   182
	(hyp_subst_tac 1),
nipkow@243
   183
	(rtac (less_lift1c RS iffD2) 1),
nipkow@243
   184
	(rtac trans_less 1),
nipkow@243
   185
	(etac (less_lift1c RS iffD1) 1),
nipkow@243
   186
	(etac (less_lift1c RS iffD1) 1)
nipkow@243
   187
	]);
nipkow@243
   188