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