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