src/HOLCF/lift2.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 243 c22b85994e17
permissions -rw-r--r--
made tutorial first;
     1 (*  Title: 	HOLCF/lift2.ML
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Lemmas for lift2.thy 
     7 *)
     8 
     9 open Lift2;
    10 
    11 (* -------------------------------------------------------------------------*)
    12 (* type ('a)u is pointed                                                    *)
    13 (* ------------------------------------------------------------------------ *)
    14 
    15 val minimal_lift = prove_goal Lift2.thy "UU_lift << z"
    16  (fn prems =>
    17 	[
    18 	(rtac (inst_lift_po RS ssubst) 1),
    19 	(rtac less_lift1a 1)
    20 	]);
    21 
    22 (* -------------------------------------------------------------------------*)
    23 (* access to less_lift in class po                                          *)
    24 (* ------------------------------------------------------------------------ *)
    25 
    26 val less_lift2b = prove_goal Lift2.thy "~ Iup(x) << UU_lift"
    27  (fn prems =>
    28 	[
    29 	(rtac (inst_lift_po RS ssubst) 1),
    30 	(rtac less_lift1b 1)
    31 	]);
    32 
    33 val less_lift2c = prove_goal Lift2.thy "(Iup(x)<<Iup(y)) = (x<<y)"
    34  (fn prems =>
    35 	[
    36 	(rtac (inst_lift_po RS ssubst) 1),
    37 	(rtac less_lift1c 1)
    38 	]);
    39 
    40 (* ------------------------------------------------------------------------ *)
    41 (* Iup and Ilift are monotone                                               *)
    42 (* ------------------------------------------------------------------------ *)
    43 
    44 val monofun_Iup = prove_goalw Lift2.thy [monofun] "monofun(Iup)"
    45  (fn prems =>
    46 	[
    47 	(strip_tac 1),
    48 	(etac (less_lift2c RS iffD2) 1)
    49 	]);
    50 
    51 val monofun_Ilift1 = prove_goalw Lift2.thy [monofun] "monofun(Ilift)"
    52  (fn prems =>
    53 	[
    54 	(strip_tac 1),
    55 	(rtac (less_fun RS iffD2) 1),
    56 	(strip_tac 1),
    57 	(res_inst_tac [("p","xa")] liftE 1),
    58 	(asm_simp_tac Lift_ss 1),
    59 	(asm_simp_tac Lift_ss 1),
    60 	(etac monofun_cfun_fun 1)
    61 	]);
    62 
    63 val monofun_Ilift2 = prove_goalw Lift2.thy [monofun] "monofun(Ilift(f))"
    64  (fn prems =>
    65 	[
    66 	(strip_tac 1),
    67 	(res_inst_tac [("p","x")] liftE 1),
    68 	(asm_simp_tac Lift_ss 1),
    69 	(asm_simp_tac Lift_ss 1),
    70 	(res_inst_tac [("p","y")] liftE 1),
    71 	(hyp_subst_tac 1),
    72 	(hyp_subst_tac 1),
    73 	(rtac notE 1),
    74 	(rtac less_lift2b 1),
    75 	(atac 1),
    76 	(asm_simp_tac Lift_ss 1),
    77 	(rtac monofun_cfun_arg 1),
    78 	(hyp_subst_tac 1),
    79 	(hyp_subst_tac 1),
    80 	(etac (less_lift2c  RS iffD1) 1)
    81 	]);
    82 
    83 (* ------------------------------------------------------------------------ *)
    84 (* Some kind of surjectivity lemma                                          *)
    85 (* ------------------------------------------------------------------------ *)
    86 
    87 
    88 val lift_lemma1 = prove_goal Lift2.thy  "z=Iup(x) ==> Iup(Ilift(LAM x.x)(z)) = z"
    89  (fn prems =>
    90 	[
    91 	(cut_facts_tac prems 1),
    92 	(asm_simp_tac Lift_ss 1)
    93 	]);
    94 
    95 (* ------------------------------------------------------------------------ *)
    96 (* ('a)u is a cpo                                                           *)
    97 (* ------------------------------------------------------------------------ *)
    98 
    99 val lub_lift1a = prove_goal Lift2.thy 
   100 "[|is_chain(Y);? i x.Y(i)=Iup(x)|] ==>\
   101 \ range(Y) <<| Iup(lub(range(%i.(Ilift (LAM x.x) (Y(i))))))"
   102  (fn prems =>
   103 	[
   104 	(cut_facts_tac prems 1),
   105 	(rtac is_lubI 1),
   106 	(rtac conjI 1),
   107 	(rtac ub_rangeI 1),
   108 	(rtac allI 1),
   109 	(res_inst_tac [("p","Y(i)")] liftE 1),
   110 	(res_inst_tac [("s","UU_lift"),("t","Y(i)")] subst 1),
   111 	(etac sym 1),
   112 	(rtac minimal_lift 1),
   113 	(res_inst_tac [("t","Y(i)")] (lift_lemma1 RS subst) 1),
   114 	(atac 1),
   115 	(rtac (less_lift2c RS iffD2) 1),
   116 	(rtac is_ub_thelub 1),
   117 	(etac (monofun_Ilift2 RS ch2ch_monofun) 1),
   118 	(strip_tac 1),
   119 	(res_inst_tac [("p","u")] liftE 1),
   120 	(etac exE 1),
   121 	(etac exE 1),
   122 	(res_inst_tac [("P","Y(i)<<UU_lift")] notE 1),
   123 	(res_inst_tac [("s","Iup(x)"),("t","Y(i)")] ssubst 1),
   124 	(atac 1),
   125 	(rtac less_lift2b 1),
   126 	(hyp_subst_tac 1),
   127 	(etac (ub_rangeE RS spec) 1),
   128 	(res_inst_tac [("t","u")] (lift_lemma1 RS subst) 1),
   129 	(atac 1),
   130 	(rtac (less_lift2c RS iffD2) 1),
   131 	(rtac is_lub_thelub 1),
   132 	(etac (monofun_Ilift2 RS ch2ch_monofun) 1),
   133 	(etac (monofun_Ilift2 RS ub2ub_monofun) 1)
   134 	]);
   135 
   136 val lub_lift1b = prove_goal Lift2.thy 
   137 "[|is_chain(Y);!i x.~Y(i)=Iup(x)|] ==>\
   138 \ range(Y) <<| UU_lift"
   139  (fn prems =>
   140 	[
   141 	(cut_facts_tac prems 1),
   142 	(rtac is_lubI 1),
   143 	(rtac conjI 1),
   144 	(rtac ub_rangeI 1),
   145 	(rtac allI 1),
   146 	(res_inst_tac [("p","Y(i)")] liftE 1),
   147 	(res_inst_tac [("s","UU_lift"),("t","Y(i)")] ssubst 1),
   148 	(atac 1),
   149 	(rtac refl_less 1),
   150 	(rtac notE 1),
   151 	(dtac spec 1),
   152 	(dtac spec 1),
   153 	(atac 1),
   154 	(atac 1),
   155 	(strip_tac 1),
   156 	(rtac minimal_lift 1)
   157 	]);
   158 
   159 val thelub_lift1a = lub_lift1a RS thelubI;
   160 (* [| is_chain(?Y1); ? i x. ?Y1(i) = Iup(x) |] ==>                *)
   161 (* lub(range(?Y1)) = Iup(lub(range(%i. Ilift(LAM x. x,?Y1(i)))))  *)
   162 
   163 val thelub_lift1b = lub_lift1b RS thelubI;
   164 (* [| is_chain(?Y1); ! i x. ~ ?Y1(i) = Iup(x) |] ==>              *)
   165 (*                                     lub(range(?Y1)) = UU_lift  *)
   166 
   167 
   168 val cpo_lift = prove_goal Lift2.thy 
   169 	"is_chain(Y::nat=>('a)u) ==> ? x.range(Y) <<|x"
   170  (fn prems =>
   171 	[
   172 	(cut_facts_tac prems 1),
   173 	(rtac disjE 1),
   174 	(rtac exI 2),
   175 	(etac lub_lift1a 2),
   176 	(atac 2),
   177 	(rtac exI 2),
   178 	(etac lub_lift1b 2),
   179 	(atac 2),
   180 	(fast_tac HOL_cs 1)
   181 	]);
   182