src/HOLCF/lift1.ML
changeset 243 c22b85994e17
child 248 0d0a6a17a02f
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/lift1.ML	Wed Jan 19 17:35:01 1994 +0100
     1.3 @@ -0,0 +1,188 @@
     1.4 +(*  Title: 	HOLCF/lift1.ML
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Franz Regensburger
     1.7 +    Copyright   1993  Technische Universitaet Muenchen
     1.8 +*)
     1.9 +
    1.10 +open Lift1;
    1.11 +
    1.12 +val Exh_Lift = prove_goalw Lift1.thy [UU_lift_def,Iup_def ]
    1.13 +	"z = UU_lift | (? x. z = Iup(x))"
    1.14 + (fn prems =>
    1.15 +	[
    1.16 +	(rtac (Rep_Lift_inverse RS subst) 1),
    1.17 +	(res_inst_tac [("s","Rep_Lift(z)")] sumE 1),
    1.18 +	(rtac disjI1 1),
    1.19 +	(res_inst_tac [("f","Abs_Lift")] arg_cong 1),
    1.20 +	(rtac (unique_void2 RS subst) 1),
    1.21 +	(atac 1),
    1.22 +	(rtac disjI2 1),
    1.23 +	(rtac exI 1),
    1.24 +	(res_inst_tac [("f","Abs_Lift")] arg_cong 1),
    1.25 +	(atac 1)
    1.26 +	]);
    1.27 +
    1.28 +val inj_Abs_Lift = prove_goal Lift1.thy "inj(Abs_Lift)"
    1.29 + (fn prems =>
    1.30 +	[
    1.31 +	(rtac inj_inverseI 1),
    1.32 +	(rtac Abs_Lift_inverse 1)
    1.33 +	]);
    1.34 +
    1.35 +val inj_Rep_Lift = prove_goal Lift1.thy "inj(Rep_Lift)"
    1.36 + (fn prems =>
    1.37 +	[
    1.38 +	(rtac inj_inverseI 1),
    1.39 +	(rtac Rep_Lift_inverse 1)
    1.40 +	]);
    1.41 +
    1.42 +val inject_Iup = prove_goalw Lift1.thy [Iup_def] "Iup(x)=Iup(y) ==> x=y"
    1.43 + (fn prems =>
    1.44 +	[
    1.45 +	(cut_facts_tac prems 1),
    1.46 +	(rtac (inj_Inr RS injD) 1),
    1.47 +	(rtac (inj_Abs_Lift RS injD) 1),
    1.48 +	(atac 1)
    1.49 +	]);
    1.50 +
    1.51 +val defined_Iup=prove_goalw Lift1.thy [Iup_def,UU_lift_def] "~ Iup(x)=UU_lift"
    1.52 + (fn prems =>
    1.53 +	[
    1.54 +	(rtac notI 1),
    1.55 +	(rtac notE 1),
    1.56 +	(rtac Inl_not_Inr 1),
    1.57 +	(rtac sym 1),
    1.58 +	(etac (inj_Abs_Lift RS  injD) 1)
    1.59 +	]);
    1.60 +
    1.61 +
    1.62 +val liftE = prove_goal  Lift1.thy
    1.63 +	"[| p=UU_lift ==> Q; !!x. p=Iup(x)==>Q|] ==>Q"
    1.64 + (fn prems =>
    1.65 +	[
    1.66 +	(rtac (Exh_Lift RS disjE) 1),
    1.67 +	(eresolve_tac prems 1),
    1.68 +	(etac exE 1),
    1.69 +	(eresolve_tac prems 1)
    1.70 +	]);
    1.71 +
    1.72 +val Ilift1 = prove_goalw  Lift1.thy [Ilift_def,UU_lift_def]
    1.73 +	"Ilift(f)(UU_lift)=UU"
    1.74 + (fn prems =>
    1.75 +	[
    1.76 +	(rtac (Abs_Lift_inverse RS ssubst) 1),
    1.77 +	(rtac (case_Inl RS ssubst) 1),
    1.78 +	(rtac refl 1)
    1.79 +	]);
    1.80 +
    1.81 +val Ilift2 = prove_goalw  Lift1.thy [Ilift_def,Iup_def]
    1.82 +	"Ilift(f)(Iup(x))=f[x]"
    1.83 + (fn prems =>
    1.84 +	[
    1.85 +	(rtac (Abs_Lift_inverse RS ssubst) 1),
    1.86 +	(rtac (case_Inr RS ssubst) 1),
    1.87 +	(rtac refl 1)
    1.88 +	]);
    1.89 +
    1.90 +val Lift_ss = Cfun_ss addsimps [Ilift1,Ilift2];
    1.91 +
    1.92 +val less_lift1a = prove_goalw  Lift1.thy [less_lift_def,UU_lift_def]
    1.93 +	"less_lift(UU_lift)(z)"
    1.94 + (fn prems =>
    1.95 +	[
    1.96 +	(rtac (Abs_Lift_inverse RS ssubst) 1),
    1.97 +	(rtac (case_Inl RS ssubst) 1),
    1.98 +	(rtac TrueI 1)
    1.99 +	]);
   1.100 +
   1.101 +val less_lift1b = prove_goalw  Lift1.thy [Iup_def,less_lift_def,UU_lift_def]
   1.102 +	"~less_lift(Iup(x),UU_lift)"
   1.103 + (fn prems =>
   1.104 +	[
   1.105 +	(rtac notI 1),
   1.106 +	(rtac iffD1 1),
   1.107 +	(atac 2),
   1.108 +	(rtac (Abs_Lift_inverse RS ssubst) 1),
   1.109 +	(rtac (Abs_Lift_inverse RS ssubst) 1),
   1.110 +	(rtac (case_Inr RS ssubst) 1),
   1.111 +	(rtac (case_Inl RS ssubst) 1),
   1.112 +	(rtac refl 1)
   1.113 +	]);
   1.114 +
   1.115 +val less_lift1c = prove_goalw  Lift1.thy [Iup_def,less_lift_def,UU_lift_def]
   1.116 +	"less_lift(Iup(x),Iup(y))=(x<<y)"
   1.117 + (fn prems =>
   1.118 +	[
   1.119 +	(rtac (Abs_Lift_inverse RS ssubst) 1),
   1.120 +	(rtac (Abs_Lift_inverse RS ssubst) 1),
   1.121 +	(rtac (case_Inr RS ssubst) 1),
   1.122 +	(rtac (case_Inr RS ssubst) 1),
   1.123 +	(rtac refl 1)
   1.124 +	]);
   1.125 +
   1.126 +
   1.127 +val refl_less_lift = prove_goal  Lift1.thy "less_lift(p,p)"
   1.128 + (fn prems =>
   1.129 +	[
   1.130 +	(res_inst_tac [("p","p")] liftE 1),
   1.131 +	(hyp_subst_tac 1),
   1.132 +	(rtac less_lift1a 1),
   1.133 +	(hyp_subst_tac 1),
   1.134 +	(rtac (less_lift1c RS iffD2) 1),
   1.135 +	(rtac refl_less 1)
   1.136 +	]);
   1.137 +
   1.138 +val antisym_less_lift = prove_goal  Lift1.thy 
   1.139 +	"[|less_lift(p1,p2);less_lift(p2,p1)|] ==> p1=p2"
   1.140 + (fn prems =>
   1.141 +	[
   1.142 +	(cut_facts_tac prems 1),
   1.143 +	(res_inst_tac [("p","p1")] liftE 1),
   1.144 +	(hyp_subst_tac 1),
   1.145 +	(res_inst_tac [("p","p2")] liftE 1),
   1.146 +	(hyp_subst_tac 1),
   1.147 +	(rtac refl 1),
   1.148 +	(hyp_subst_tac 1),
   1.149 +	(res_inst_tac [("P","less_lift(Iup(x),UU_lift)")] notE 1),
   1.150 +	(rtac less_lift1b 1),
   1.151 +	(atac 1),
   1.152 +	(hyp_subst_tac 1),
   1.153 +	(res_inst_tac [("p","p2")] liftE 1),
   1.154 +	(hyp_subst_tac 1),
   1.155 +	(res_inst_tac [("P","less_lift(Iup(x),UU_lift)")] notE 1),
   1.156 +	(rtac less_lift1b 1),
   1.157 +	(atac 1),
   1.158 +	(hyp_subst_tac 1),
   1.159 +	(rtac arg_cong 1),
   1.160 +	(rtac antisym_less 1),
   1.161 +	(etac (less_lift1c RS iffD1) 1),
   1.162 +	(etac (less_lift1c RS iffD1) 1)
   1.163 +	]);
   1.164 +
   1.165 +val trans_less_lift = prove_goal  Lift1.thy 
   1.166 +	"[|less_lift(p1,p2);less_lift(p2,p3)|] ==> less_lift(p1,p3)"
   1.167 + (fn prems =>
   1.168 +	[
   1.169 +	(cut_facts_tac prems 1),
   1.170 +	(res_inst_tac [("p","p1")] liftE 1),
   1.171 +	(hyp_subst_tac 1),
   1.172 +	(rtac less_lift1a 1),
   1.173 +	(hyp_subst_tac 1),
   1.174 +	(res_inst_tac [("p","p2")] liftE 1),
   1.175 +	(hyp_subst_tac 1),
   1.176 +	(rtac notE 1),
   1.177 +	(rtac less_lift1b 1),
   1.178 +	(atac 1),
   1.179 +	(hyp_subst_tac 1),
   1.180 +	(res_inst_tac [("p","p3")] liftE 1),
   1.181 +	(hyp_subst_tac 1),
   1.182 +	(rtac notE 1),
   1.183 +	(rtac less_lift1b 1),
   1.184 +	(atac 1),
   1.185 +	(hyp_subst_tac 1),
   1.186 +	(rtac (less_lift1c RS iffD2) 1),
   1.187 +	(rtac trans_less 1),
   1.188 +	(etac (less_lift1c RS iffD1) 1),
   1.189 +	(etac (less_lift1c RS iffD1) 1)
   1.190 +	]);
   1.191 +