# HG changeset patch # User oheimb # Date 849266542 -3600 # Node ID d63ffafce255988ae0c360842ee80f0f3a43a1ce # Parent 9174de6c714373f6dacc7238572f17cb68f85bd4 *** empty log message *** diff -r 9174de6c7143 -r d63ffafce255 src/HOLCF/Cfun1.thy --- a/src/HOLCF/Cfun1.thy Fri Nov 29 12:17:30 1996 +0100 +++ b/src/HOLCF/Cfun1.thy Fri Nov 29 12:22:22 1996 +0100 @@ -65,4 +65,9 @@ end (* start 8bit 2 *) +ML +val parse_ast_translation = ("¤", fn asts => Appl (Constant "LAM " :: asts)) :: + parse_ast_translation; +val print_ast_translation = ("LAM ", fn asts => Appl (Constant "¤" :: asts)) :: + print_ast_translation; (* end 8bit 2 *) diff -r 9174de6c7143 -r d63ffafce255 src/HOLCF/Cprod3.thy --- a/src/HOLCF/Cprod3.thy Fri Nov 29 12:17:30 1996 +0100 +++ b/src/HOLCF/Cprod3.thy Fri Nov 29 12:22:22 1996 +0100 @@ -82,6 +82,9 @@ (* reverse translation <= does not work yet !! *) (* start 8bit 1 *) +translations + "Let x = a in e" == "CLet`a`(¤ x.e)" + (* end 8bit 1 *) end diff -r 9174de6c7143 -r d63ffafce255 src/HOLCF/Lift1.ML --- a/src/HOLCF/Lift1.ML Fri Nov 29 12:17:30 1996 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,186 +0,0 @@ -(* Title: HOLCF/lift1.ML - ID: $Id$ - Author: Franz Regensburger - Copyright 1993 Technische Universitaet Muenchen -*) - -open Lift1; - -qed_goalw "Exh_Lift" Lift1.thy [UU_lift_def,Iup_def ] - "z = UU_lift | (? x. z = Iup(x))" - (fn prems => - [ - (rtac (Rep_Lift_inverse RS subst) 1), - (res_inst_tac [("s","Rep_Lift(z)")] sumE 1), - (rtac disjI1 1), - (res_inst_tac [("f","Abs_Lift")] arg_cong 1), - (rtac (unique_void2 RS subst) 1), - (atac 1), - (rtac disjI2 1), - (rtac exI 1), - (res_inst_tac [("f","Abs_Lift")] arg_cong 1), - (atac 1) - ]); - -qed_goal "inj_Abs_Lift" Lift1.thy "inj(Abs_Lift)" - (fn prems => - [ - (rtac inj_inverseI 1), - (rtac Abs_Lift_inverse 1) - ]); - -qed_goal "inj_Rep_Lift" Lift1.thy "inj(Rep_Lift)" - (fn prems => - [ - (rtac inj_inverseI 1), - (rtac Rep_Lift_inverse 1) - ]); - -qed_goalw "inject_Iup" Lift1.thy [Iup_def] "Iup(x)=Iup(y) ==> x=y" - (fn prems => - [ - (cut_facts_tac prems 1), - (rtac (inj_Inr RS injD) 1), - (rtac (inj_Abs_Lift RS injD) 1), - (atac 1) - ]); - -qed_goalw "defined_Iup" Lift1.thy [Iup_def,UU_lift_def] "Iup(x)~=UU_lift" - (fn prems => - [ - (rtac notI 1), - (rtac notE 1), - (rtac Inl_not_Inr 1), - (rtac sym 1), - (etac (inj_Abs_Lift RS injD) 1) - ]); - - -qed_goal "liftE" Lift1.thy - "[| p=UU_lift ==> Q; !!x. p=Iup(x)==>Q|] ==>Q" - (fn prems => - [ - (rtac (Exh_Lift RS disjE) 1), - (eresolve_tac prems 1), - (etac exE 1), - (eresolve_tac prems 1) - ]); - -qed_goalw "Ilift1" Lift1.thy [Ilift_def,UU_lift_def] - "Ilift(f)(UU_lift)=UU" - (fn prems => - [ - (stac Abs_Lift_inverse 1), - (stac sum_case_Inl 1), - (rtac refl 1) - ]); - -qed_goalw "Ilift2" Lift1.thy [Ilift_def,Iup_def] - "Ilift(f)(Iup(x))=f`x" - (fn prems => - [ - (stac Abs_Lift_inverse 1), - (stac sum_case_Inr 1), - (rtac refl 1) - ]); - -val Lift0_ss = (simpset_of "Cfun3") addsimps [Ilift1,Ilift2]; - -qed_goalw "less_lift1a" Lift1.thy [less_lift_def,UU_lift_def] - "less_lift(UU_lift)(z)" - (fn prems => - [ - (stac Abs_Lift_inverse 1), - (stac sum_case_Inl 1), - (rtac TrueI 1) - ]); - -qed_goalw "less_lift1b" Lift1.thy [Iup_def,less_lift_def,UU_lift_def] - "~less_lift (Iup x) UU_lift" - (fn prems => - [ - (rtac notI 1), - (rtac iffD1 1), - (atac 2), - (stac Abs_Lift_inverse 1), - (stac Abs_Lift_inverse 1), - (stac sum_case_Inr 1), - (stac sum_case_Inl 1), - (rtac refl 1) - ]); - -qed_goalw "less_lift1c" Lift1.thy [Iup_def,less_lift_def,UU_lift_def] - "less_lift (Iup x) (Iup y)=(x< - [ - (stac Abs_Lift_inverse 1), - (stac Abs_Lift_inverse 1), - (stac sum_case_Inr 1), - (stac sum_case_Inr 1), - (rtac refl 1) - ]); - - -qed_goal "refl_less_lift" Lift1.thy "less_lift p p" - (fn prems => - [ - (res_inst_tac [("p","p")] liftE 1), - (hyp_subst_tac 1), - (rtac less_lift1a 1), - (hyp_subst_tac 1), - (rtac (less_lift1c RS iffD2) 1), - (rtac refl_less 1) - ]); - -qed_goal "antisym_less_lift" Lift1.thy - "!!p1. [|less_lift p1 p2;less_lift p2 p1|] ==> p1=p2" - (fn _ => - [ - (res_inst_tac [("p","p1")] liftE 1), - (hyp_subst_tac 1), - (res_inst_tac [("p","p2")] liftE 1), - (etac sym 1), - (hyp_subst_tac 1), - (res_inst_tac [("P","less_lift (Iup x) UU_lift")] notE 1), - (rtac less_lift1b 1), - (atac 1), - (hyp_subst_tac 1), - (res_inst_tac [("p","p2")] liftE 1), - (hyp_subst_tac 1), - (res_inst_tac [("P","less_lift (Iup x) UU_lift")] notE 1), - (rtac less_lift1b 1), - (atac 1), - (hyp_subst_tac 1), - (rtac arg_cong 1), - (rtac antisym_less 1), - (etac (less_lift1c RS iffD1) 1), - (etac (less_lift1c RS iffD1) 1) - ]); - -qed_goal "trans_less_lift" Lift1.thy - "[|less_lift p1 p2;less_lift p2 p3|] ==> less_lift p1 p3" - (fn prems => - [ - (cut_facts_tac prems 1), - (res_inst_tac [("p","p1")] liftE 1), - (hyp_subst_tac 1), - (rtac less_lift1a 1), - (hyp_subst_tac 1), - (res_inst_tac [("p","p2")] liftE 1), - (hyp_subst_tac 1), - (rtac notE 1), - (rtac less_lift1b 1), - (atac 1), - (hyp_subst_tac 1), - (res_inst_tac [("p","p3")] liftE 1), - (hyp_subst_tac 1), - (rtac notE 1), - (rtac less_lift1b 1), - (atac 1), - (hyp_subst_tac 1), - (rtac (less_lift1c RS iffD2) 1), - (rtac trans_less 1), - (etac (less_lift1c RS iffD1) 1), - (etac (less_lift1c RS iffD1) 1) - ]); - diff -r 9174de6c7143 -r d63ffafce255 src/HOLCF/Lift1.thy --- a/src/HOLCF/Lift1.thy Fri Nov 29 12:17:30 1996 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,56 +0,0 @@ -(* Title: HOLCF/Lift1.thy - ID: $Id$ - Author: Franz Regensburger - Copyright 1993 Technische Universitaet Muenchen - - -Lifting - -*) - -Lift1 = Cfun3 + Sum + - -(* new type for lifting *) - -types "u" 1 - -arities "u" :: (pcpo)term - -consts - - Rep_Lift :: "('a)u => (void + 'a)" - Abs_Lift :: "(void + 'a) => ('a)u" - - Iup :: "'a => ('a)u" - UU_lift :: "('a)u" - Ilift :: "('a->'b)=>('a)u => 'b" - less_lift :: "('a)u => ('a)u => bool" - -rules - - (*faking a type definition... *) - (* ('a)u is isomorphic to void + 'a *) - - Rep_Lift_inverse "Abs_Lift(Rep_Lift(p)) = p" - Abs_Lift_inverse "Rep_Lift(Abs_Lift(p)) = p" - - (*defining the abstract constants*) - -defs - UU_lift_def "UU_lift == Abs_Lift(Inl(UU))" - Iup_def "Iup(x) == Abs_Lift(Inr(x))" - - Ilift_def "Ilift(f)(x)== - case Rep_Lift(x) of Inl(y) => UU | Inr(z) => f`z" - - less_lift_def "less_lift(x1)(x2) == - (case Rep_Lift(x1) of - Inl(y1) => True - | Inr(y2) => - (case Rep_Lift(x2) of Inl(z1) => False - | Inr(z2) => y2< - [ - (stac inst_lift_po 1), - (rtac less_lift1a 1) - ]); - -(* -------------------------------------------------------------------------*) -(* access to less_lift in class po *) -(* ------------------------------------------------------------------------ *) - -qed_goal "less_lift2b" Lift2.thy "~ Iup(x) << UU_lift" - (fn prems => - [ - (stac inst_lift_po 1), - (rtac less_lift1b 1) - ]); - -qed_goal "less_lift2c" Lift2.thy "(Iup(x)< - [ - (stac inst_lift_po 1), - (rtac less_lift1c 1) - ]); - -(* ------------------------------------------------------------------------ *) -(* Iup and Ilift are monotone *) -(* ------------------------------------------------------------------------ *) - -qed_goalw "monofun_Iup" Lift2.thy [monofun] "monofun(Iup)" - (fn prems => - [ - (strip_tac 1), - (etac (less_lift2c RS iffD2) 1) - ]); - -qed_goalw "monofun_Ilift1" Lift2.thy [monofun] "monofun(Ilift)" - (fn prems => - [ - (strip_tac 1), - (rtac (less_fun RS iffD2) 1), - (strip_tac 1), - (res_inst_tac [("p","xa")] liftE 1), - (asm_simp_tac Lift0_ss 1), - (asm_simp_tac Lift0_ss 1), - (etac monofun_cfun_fun 1) - ]); - -qed_goalw "monofun_Ilift2" Lift2.thy [monofun] "monofun(Ilift(f))" - (fn prems => - [ - (strip_tac 1), - (res_inst_tac [("p","x")] liftE 1), - (asm_simp_tac Lift0_ss 1), - (asm_simp_tac Lift0_ss 1), - (res_inst_tac [("p","y")] liftE 1), - (hyp_subst_tac 1), - (rtac notE 1), - (rtac less_lift2b 1), - (atac 1), - (asm_simp_tac Lift0_ss 1), - (rtac monofun_cfun_arg 1), - (hyp_subst_tac 1), - (etac (less_lift2c RS iffD1) 1) - ]); - -(* ------------------------------------------------------------------------ *) -(* Some kind of surjectivity lemma *) -(* ------------------------------------------------------------------------ *) - - -qed_goal "lift_lemma1" Lift2.thy "z=Iup(x) ==> Iup(Ilift(LAM x.x)(z)) = z" - (fn prems => - [ - (cut_facts_tac prems 1), - (asm_simp_tac Lift0_ss 1) - ]); - -(* ------------------------------------------------------------------------ *) -(* ('a)u is a cpo *) -(* ------------------------------------------------------------------------ *) - -qed_goal "lub_lift1a" Lift2.thy -"[|is_chain(Y);? i x.Y(i)=Iup(x)|] ==>\ -\ range(Y) <<| Iup(lub(range(%i.(Ilift (LAM x.x) (Y(i))))))" - (fn prems => - [ - (cut_facts_tac prems 1), - (rtac is_lubI 1), - (rtac conjI 1), - (rtac ub_rangeI 1), - (rtac allI 1), - (res_inst_tac [("p","Y(i)")] liftE 1), - (res_inst_tac [("s","UU_lift"),("t","Y(i)")] subst 1), - (etac sym 1), - (rtac minimal_lift 1), - (res_inst_tac [("t","Y(i)")] (lift_lemma1 RS subst) 1), - (atac 1), - (rtac (less_lift2c RS iffD2) 1), - (rtac is_ub_thelub 1), - (etac (monofun_Ilift2 RS ch2ch_monofun) 1), - (strip_tac 1), - (res_inst_tac [("p","u")] liftE 1), - (etac exE 1), - (etac exE 1), - (res_inst_tac [("P","Y(i)<\ -\ range(Y) <<| UU_lift" - (fn prems => - [ - (cut_facts_tac prems 1), - (rtac is_lubI 1), - (rtac conjI 1), - (rtac ub_rangeI 1), - (rtac allI 1), - (res_inst_tac [("p","Y(i)")] liftE 1), - (res_inst_tac [("s","UU_lift"),("t","Y(i)")] ssubst 1), - (atac 1), - (rtac refl_less 1), - (rtac notE 1), - (dtac spec 1), - (dtac spec 1), - (atac 1), - (atac 1), - (strip_tac 1), - (rtac minimal_lift 1) - ]); - -bind_thm ("thelub_lift1a", lub_lift1a RS thelubI); -(* -[| is_chain ?Y1; ? i x. ?Y1 i = Iup x |] ==> - lub (range ?Y1) = Iup (lub (range (%i. Ilift (LAM x. x) (?Y1 i)))) -*) - -bind_thm ("thelub_lift1b", lub_lift1b RS thelubI); -(* -[| is_chain ?Y1; ! i x. ?Y1 i ~= Iup x |] ==> - lub (range ?Y1) = UU_lift -*) - -qed_goal "cpo_lift" Lift2.thy - "is_chain(Y::nat=>('a)u) ==> ? x.range(Y) <<|x" - (fn prems => - [ - (cut_facts_tac prems 1), - (rtac disjE 1), - (rtac exI 2), - (etac lub_lift1a 2), - (atac 2), - (rtac exI 2), - (etac lub_lift1b 2), - (atac 2), - (fast_tac HOL_cs 1) - ]); - diff -r 9174de6c7143 -r d63ffafce255 src/HOLCF/Lift2.thy --- a/src/HOLCF/Lift2.thy Fri Nov 29 12:17:30 1996 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,25 +0,0 @@ -(* Title: HOLCF/lift2.thy - ID: $Id$ - Author: Franz Regensburger - Copyright 1993 Technische Universitaet Muenchen - -Class Instance u::(pcpo)po - -*) - -Lift2 = Lift1 + - -(* Witness for the above arity axiom is lift1.ML *) - -arities "u" :: (pcpo)po - -rules - -(* instance of << for type ('a)u *) - -inst_lift_po "((op <<)::[('a)u,('a)u]=>bool) = less_lift" - -end - - - diff -r 9174de6c7143 -r d63ffafce255 src/HOLCF/Lift3.ML --- a/src/HOLCF/Lift3.ML Fri Nov 29 12:17:30 1996 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,347 +0,0 @@ -(* Title: HOLCF/lift3.ML - ID: $Id$ - Author: Franz Regensburger - Copyright 1993 Technische Universitaet Muenchen - -Lemmas for lift3.thy -*) - -open Lift3; - -(* -------------------------------------------------------------------------*) -(* some lemmas restated for class pcpo *) -(* ------------------------------------------------------------------------ *) - -qed_goal "less_lift3b" Lift3.thy "~ Iup(x) << UU" - (fn prems => - [ - (stac inst_lift_pcpo 1), - (rtac less_lift2b 1) - ]); - -qed_goal "defined_Iup2" Lift3.thy "Iup(x) ~= UU" - (fn prems => - [ - (stac inst_lift_pcpo 1), - (rtac defined_Iup 1) - ]); - -(* ------------------------------------------------------------------------ *) -(* continuity for Iup *) -(* ------------------------------------------------------------------------ *) - -qed_goal "contlub_Iup" Lift3.thy "contlub(Iup)" - (fn prems => - [ - (rtac contlubI 1), - (strip_tac 1), - (rtac trans 1), - (rtac (thelub_lift1a RS sym) 2), - (fast_tac HOL_cs 3), - (etac (monofun_Iup RS ch2ch_monofun) 2), - (res_inst_tac [("f","Iup")] arg_cong 1), - (rtac lub_equal 1), - (atac 1), - (rtac (monofun_Ilift2 RS ch2ch_monofun) 1), - (etac (monofun_Iup RS ch2ch_monofun) 1), - (asm_simp_tac Lift0_ss 1) - ]); - -qed_goal "cont_Iup" Lift3.thy "cont(Iup)" - (fn prems => - [ - (rtac monocontlub2cont 1), - (rtac monofun_Iup 1), - (rtac contlub_Iup 1) - ]); - - -(* ------------------------------------------------------------------------ *) -(* continuity for Ilift *) -(* ------------------------------------------------------------------------ *) - -qed_goal "contlub_Ilift1" Lift3.thy "contlub(Ilift)" - (fn prems => - [ - (rtac contlubI 1), - (strip_tac 1), - (rtac trans 1), - (rtac (thelub_fun RS sym) 2), - (etac (monofun_Ilift1 RS ch2ch_monofun) 2), - (rtac ext 1), - (res_inst_tac [("p","x")] liftE 1), - (asm_simp_tac Lift0_ss 1), - (rtac (lub_const RS thelubI RS sym) 1), - (asm_simp_tac Lift0_ss 1), - (etac contlub_cfun_fun 1) - ]); - - -qed_goal "contlub_Ilift2" Lift3.thy "contlub(Ilift(f))" - (fn prems => - [ - (rtac contlubI 1), - (strip_tac 1), - (rtac disjE 1), - (stac thelub_lift1a 2), - (atac 2), - (atac 2), - (asm_simp_tac Lift0_ss 2), - (stac thelub_lift1b 3), - (atac 3), - (atac 3), - (fast_tac HOL_cs 1), - (asm_simp_tac Lift0_ss 2), - (rtac (chain_UU_I_inverse RS sym) 2), - (rtac allI 2), - (res_inst_tac [("p","Y(i)")] liftE 2), - (asm_simp_tac Lift0_ss 2), - (rtac notE 2), - (dtac spec 2), - (etac spec 2), - (atac 2), - (stac contlub_cfun_arg 1), - (etac (monofun_Ilift2 RS ch2ch_monofun) 1), - (rtac lub_equal2 1), - (rtac (monofun_fapp2 RS ch2ch_monofun) 2), - (etac (monofun_Ilift2 RS ch2ch_monofun) 2), - (etac (monofun_Ilift2 RS ch2ch_monofun) 2), - (rtac (chain_mono2 RS exE) 1), - (atac 2), - (etac exE 1), - (etac exE 1), - (rtac exI 1), - (res_inst_tac [("s","Iup(x)"),("t","Y(i)")] ssubst 1), - (atac 1), - (rtac defined_Iup2 1), - (rtac exI 1), - (strip_tac 1), - (res_inst_tac [("p","Y(i)")] liftE 1), - (asm_simp_tac Lift0_ss 2), - (res_inst_tac [("P","Y(i) = UU")] notE 1), - (fast_tac HOL_cs 1), - (stac inst_lift_pcpo 1), - (atac 1) - ]); - -qed_goal "cont_Ilift1" Lift3.thy "cont(Ilift)" - (fn prems => - [ - (rtac monocontlub2cont 1), - (rtac monofun_Ilift1 1), - (rtac contlub_Ilift1 1) - ]); - -qed_goal "cont_Ilift2" Lift3.thy "cont(Ilift(f))" - (fn prems => - [ - (rtac monocontlub2cont 1), - (rtac monofun_Ilift2 1), - (rtac contlub_Ilift2 1) - ]); - - -(* ------------------------------------------------------------------------ *) -(* continuous versions of lemmas for ('a)u *) -(* ------------------------------------------------------------------------ *) - -qed_goalw "Exh_Lift1" Lift3.thy [up_def] "z = UU | (? x. z = up`x)" - (fn prems => - [ - (simp_tac (Lift0_ss addsimps [cont_Iup]) 1), - (stac inst_lift_pcpo 1), - (rtac Exh_Lift 1) - ]); - -qed_goalw "inject_up" Lift3.thy [up_def] "up`x=up`y ==> x=y" - (fn prems => - [ - (cut_facts_tac prems 1), - (rtac inject_Iup 1), - (etac box_equals 1), - (simp_tac (Lift0_ss addsimps [cont_Iup]) 1), - (simp_tac (Lift0_ss addsimps [cont_Iup]) 1) - ]); - -qed_goalw "defined_up" Lift3.thy [up_def] " up`x ~= UU" - (fn prems => - [ - (simp_tac (Lift0_ss addsimps [cont_Iup]) 1), - (rtac defined_Iup2 1) - ]); - -qed_goalw "liftE1" Lift3.thy [up_def] - "[| p=UU ==> Q; !!x. p=up`x==>Q|] ==>Q" - (fn prems => - [ - (rtac liftE 1), - (resolve_tac prems 1), - (etac (inst_lift_pcpo RS ssubst) 1), - (resolve_tac (tl prems) 1), - (asm_simp_tac (Lift0_ss addsimps [cont_Iup]) 1) - ]); - - -qed_goalw "lift1" Lift3.thy [up_def,lift_def] "lift`f`UU=UU" - (fn prems => - [ - (stac inst_lift_pcpo 1), - (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1, - cont_Ilift2,cont2cont_CF1L]) 1)), - (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1, - cont_Ilift2,cont2cont_CF1L]) 1)), - (simp_tac (Lift0_ss addsimps [cont_Iup,cont_Ilift1,cont_Ilift2]) 1) - ]); - -qed_goalw "lift2" Lift3.thy [up_def,lift_def] "lift`f`(up`x)=f`x" - (fn prems => - [ - (stac beta_cfun 1), - (rtac cont_Iup 1), - (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1, - cont_Ilift2,cont2cont_CF1L]) 1)), - (stac beta_cfun 1), - (rtac cont_Ilift2 1), - (simp_tac (Lift0_ss addsimps [cont_Iup,cont_Ilift1,cont_Ilift2]) 1) - ]); - -qed_goalw "less_lift4b" Lift3.thy [up_def,lift_def] "~ up`x << UU" - (fn prems => - [ - (simp_tac (Lift0_ss addsimps [cont_Iup]) 1), - (rtac less_lift3b 1) - ]); - -qed_goalw "less_lift4c" Lift3.thy [up_def,lift_def] - "(up`x << up`y) = (x< - [ - (simp_tac (Lift0_ss addsimps [cont_Iup]) 1), - (rtac less_lift2c 1) - ]); - -qed_goalw "thelub_lift2a" Lift3.thy [up_def,lift_def] -"[| is_chain(Y); ? i x. Y(i) = up`x |] ==>\ -\ lub(range(Y)) = up`(lub(range(%i. lift`(LAM x. x)`(Y i))))" - (fn prems => - [ - (cut_facts_tac prems 1), - (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1, - cont_Ilift2,cont2cont_CF1L]) 1)), - (stac beta_cfun 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1, - cont_Ilift2,cont2cont_CF1L]) 1)), - - (stac (beta_cfun RS ext) 1), - (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1, - cont_Ilift2,cont2cont_CF1L]) 1)), - (rtac thelub_lift1a 1), - (atac 1), - (etac exE 1), - (etac exE 1), - (rtac exI 1), - (rtac exI 1), - (etac box_equals 1), - (rtac refl 1), - (simp_tac (Lift0_ss addsimps [cont_Iup]) 1) - ]); - - - -qed_goalw "thelub_lift2b" Lift3.thy [up_def,lift_def] -"[| is_chain(Y); ! i x. Y(i) ~= up`x |] ==> lub(range(Y)) = UU" - (fn prems => - [ - (cut_facts_tac prems 1), - (stac inst_lift_pcpo 1), - (rtac thelub_lift1b 1), - (atac 1), - (strip_tac 1), - (dtac spec 1), - (dtac spec 1), - (rtac swap 1), - (atac 1), - (dtac notnotD 1), - (etac box_equals 1), - (rtac refl 1), - (simp_tac (Lift0_ss addsimps [cont_Iup]) 1) - ]); - - -qed_goal "lift_lemma2" Lift3.thy " (? x.z = up`x) = (z~=UU)" - (fn prems => - [ - (rtac iffI 1), - (etac exE 1), - (hyp_subst_tac 1), - (rtac defined_up 1), - (res_inst_tac [("p","z")] liftE1 1), - (etac notE 1), - (atac 1), - (etac exI 1) - ]); - - -qed_goal "thelub_lift2a_rev" Lift3.thy -"[| is_chain(Y); lub(range(Y)) = up`x |] ==> ? i x. Y(i) = up`x" - (fn prems => - [ - (cut_facts_tac prems 1), - (rtac exE 1), - (rtac chain_UU_I_inverse2 1), - (rtac (lift_lemma2 RS iffD1) 1), - (etac exI 1), - (rtac exI 1), - (rtac (lift_lemma2 RS iffD2) 1), - (atac 1) - ]); - -qed_goal "thelub_lift2b_rev" Lift3.thy -"[| is_chain(Y); lub(range(Y)) = UU |] ==> ! i x. Y(i) ~= up`x" - (fn prems => - [ - (cut_facts_tac prems 1), - (rtac allI 1), - (rtac (not_ex RS iffD1) 1), - (rtac contrapos 1), - (etac (lift_lemma2 RS iffD1) 2), - (fast_tac (HOL_cs addSDs [chain_UU_I RS spec]) 1) - ]); - - -qed_goal "thelub_lift3" Lift3.thy -"is_chain(Y) ==> lub(range(Y)) = UU |\ -\ lub(range(Y)) = up`(lub(range(%i. lift`(LAM x.x)`(Y i))))" - (fn prems => - [ - (cut_facts_tac prems 1), - (rtac disjE 1), - (rtac disjI1 2), - (rtac thelub_lift2b 2), - (atac 2), - (atac 2), - (rtac disjI2 2), - (rtac thelub_lift2a 2), - (atac 2), - (atac 2), - (fast_tac HOL_cs 1) - ]); - -qed_goal "lift3" Lift3.thy "lift`up`x=x" - (fn prems => - [ - (res_inst_tac [("p","x")] liftE1 1), - (asm_simp_tac ((simpset_of "Cfun3") addsimps [lift1,lift2]) 1), - (asm_simp_tac ((simpset_of "Cfun3") addsimps [lift1,lift2]) 1) - ]); - -(* ------------------------------------------------------------------------ *) -(* install simplifier for ('a)u *) -(* ------------------------------------------------------------------------ *) - -val lift_rews = [lift1,lift2,defined_up]; - diff -r 9174de6c7143 -r d63ffafce255 src/HOLCF/Lift3.thy --- a/src/HOLCF/Lift3.thy Fri Nov 29 12:17:30 1996 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,36 +0,0 @@ -(* Title: HOLCF/lift3.thy - ID: $Id$ - Author: Franz Regensburger - Copyright 1993 Technische Universitaet Muenchen - - -Class instance of ('a)u for class pcpo - -*) - -Lift3 = Lift2 + - -arities "u" :: (pcpo)pcpo (* Witness lift2.ML *) - -consts - up :: "'a -> ('a)u" - lift :: "('a->'c)-> ('a)u -> 'c" - -rules - - inst_lift_pcpo "(UU::('a)u) = UU_lift" - -defs - up_def "up == (LAM x.Iup(x))" - lift_def "lift == (LAM f p.Ilift(f)(p))" - -translations -"case l of up`x => t1" == "lift`(LAM x.t1)`l" - -(* start 8bit 1 *) -(* end 8bit 1 *) - -end - - - diff -r 9174de6c7143 -r d63ffafce255 src/HOLCF/Pcpo.thy --- a/src/HOLCF/Pcpo.thy Fri Nov 29 12:17:30 1996 +0100 +++ b/src/HOLCF/Pcpo.thy Fri Nov 29 12:22:22 1996 +0100 @@ -14,5 +14,11 @@ inst_void_pcpo "(UU::void) = UU_void" (* start 8bit 1 *) +syntax + "GUU" :: "'a::pcpo" ("Ø") + +translations + "Ø" == "UU" + (* end 8bit 1 *) end diff -r 9174de6c7143 -r d63ffafce255 src/HOLCF/Porder.thy --- a/src/HOLCF/Porder.thy Fri Nov 29 12:17:30 1996 +0100 +++ b/src/HOLCF/Porder.thy Fri Nov 29 12:22:22 1996 +0100 @@ -43,6 +43,13 @@ lub "lub(S) = (@x. S <<| x)" (* start 8bit 1 *) + +syntax + "Glub" :: "[pttrn, 'a] => 'a" ("(3×_./ _)" 10) + +translations + "×x.t" == "lub(range(%x.t))" + (* end 8bit 1 *) end diff -r 9174de6c7143 -r d63ffafce255 src/HOLCF/Porder0.thy --- a/src/HOLCF/Porder0.thy Fri Nov 29 12:17:30 1996 +0100 +++ b/src/HOLCF/Porder0.thy Fri Nov 29 12:22:22 1996 +0100 @@ -40,6 +40,12 @@ inst_void_po "((op <<)::[void,void]=>bool) = less_void" (* start 8bit 1 *) +syntax + "Ý" :: "['a,'a::po] => bool" (infixl 55) + +translations + "x Ý y" == "x << y" + (* end 8bit 1 *) end diff -r 9174de6c7143 -r d63ffafce255 src/HOLCF/ROOT.ML --- a/src/HOLCF/ROOT.ML Fri Nov 29 12:17:30 1996 +0100 +++ b/src/HOLCF/ROOT.ML Fri Nov 29 12:22:22 1996 +0100 @@ -11,6 +11,8 @@ init_thy_reader(); (* start 8bit 1 *) +val banner = + "HOLCF with sections axioms,ops,domain,generated and 8bit characters"; (* end 8bit 1 *) writeln banner; diff -r 9174de6c7143 -r d63ffafce255 src/HOLCF/Sprod0.thy --- a/src/HOLCF/Sprod0.thy Fri Nov 29 12:17:30 1996 +0100 +++ b/src/HOLCF/Sprod0.thy Fri Nov 29 12:22:22 1996 +0100 @@ -51,6 +51,14 @@ &(! a b. ~a=UU & ~b=UU & p=Ispair a b --> z=b)" (* start 8bit 1 *) +types + +('a, 'b) "õ" (infixr 20) + +translations + +(type) "x õ y" == (type) "x ** y" + (* end 8bit 1 *) end diff -r 9174de6c7143 -r d63ffafce255 src/HOLCF/Sprod3.thy --- a/src/HOLCF/Sprod3.thy Fri Nov 29 12:17:30 1996 +0100 +++ b/src/HOLCF/Sprod3.thy Fri Nov 29 12:22:22 1996 +0100 @@ -34,6 +34,12 @@ ssplit_def "ssplit == (LAM f. strictify`(LAM p.f`(sfst`p)`(ssnd`p)))" (* start 8bit 1 *) +syntax + "@Gstuple" :: "['a, args] => 'a ** 'b" ("(1É_,/ _Ê)") + +translations + "Éx, y, zÊ" == "Éx, Éy, zÊÊ" + "Éx, yÊ" == "(|x,y|)" (* end 8bit 1 *) end diff -r 9174de6c7143 -r d63ffafce255 src/HOLCF/Ssum0.thy --- a/src/HOLCF/Ssum0.thy Fri Nov 29 12:17:30 1996 +0100 +++ b/src/HOLCF/Ssum0.thy Fri Nov 29 12:22:22 1996 +0100 @@ -52,6 +52,14 @@ &(!b. b~=UU & s=Isinr(b) --> z=g`b)" (* start 8bit 1 *) +types + +('a, 'b) "ó" (infixr 10) + +translations + +(type) "x ó y" == (type) "x ++ y" + (* end 8bit 1 *) end diff -r 9174de6c7143 -r d63ffafce255 src/HOLCF/Ssum3.thy --- a/src/HOLCF/Ssum3.thy Fri Nov 29 12:17:30 1996 +0100 +++ b/src/HOLCF/Ssum3.thy Fri Nov 29 12:22:22 1996 +0100 @@ -30,6 +30,9 @@ "case s of sinl`x => t1 | sinr`y => t2" == "sswhen`(LAM x.t1)`(LAM y.t2)`s" (* start 8bit 1 *) +translations +"case s of sinl`x => t1 | sinr`y => t2" == "sswhen`(¤x.t1)`(¤y.t2)`s" + (* end 8bit 1 *) end diff -r 9174de6c7143 -r d63ffafce255 src/HOLCF/Tr1.thy --- a/src/HOLCF/Tr1.thy Fri Nov 29 12:17:30 1996 +0100 +++ b/src/HOLCF/Tr1.thy Fri Nov 29 12:22:22 1996 +0100 @@ -43,6 +43,14 @@ (LAM e1 e2 t. sswhen`(LAM x.e1)`(LAM y.e2)`(rep_tr`t))" (* start 8bit 1 *) +syntax + "GeqTT" :: "tr => bool" ("(Å_Æ)") + "GeqFF" :: "tr => bool" ("(Ç_È)") + +translations + "ÅxÆ" == "x = TT" + "ÇxÈ" == "x = FF" + (* end 8bit 1 *) diff -r 9174de6c7143 -r d63ffafce255 src/HOLCF/Up1.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Up1.ML Fri Nov 29 12:22:22 1996 +0100 @@ -0,0 +1,186 @@ +(* Title: HOLCF/Up1.ML + ID: $Id$ + Author: Franz Regensburger + Copyright 1993 Technische Universitaet Muenchen +*) + +open Up1; + +qed_goalw "Exh_Up" Up1.thy [UU_up_def,Iup_def ] + "z = UU_up | (? x. z = Iup(x))" + (fn prems => + [ + (rtac (Rep_Up_inverse RS subst) 1), + (res_inst_tac [("s","Rep_Up(z)")] sumE 1), + (rtac disjI1 1), + (res_inst_tac [("f","Abs_Up")] arg_cong 1), + (rtac (unique_void2 RS subst) 1), + (atac 1), + (rtac disjI2 1), + (rtac exI 1), + (res_inst_tac [("f","Abs_Up")] arg_cong 1), + (atac 1) + ]); + +qed_goal "inj_Abs_Up" Up1.thy "inj(Abs_Up)" + (fn prems => + [ + (rtac inj_inverseI 1), + (rtac Abs_Up_inverse 1) + ]); + +qed_goal "inj_Rep_Up" Up1.thy "inj(Rep_Up)" + (fn prems => + [ + (rtac inj_inverseI 1), + (rtac Rep_Up_inverse 1) + ]); + +qed_goalw "inject_Iup" Up1.thy [Iup_def] "Iup(x)=Iup(y) ==> x=y" + (fn prems => + [ + (cut_facts_tac prems 1), + (rtac (inj_Inr RS injD) 1), + (rtac (inj_Abs_Up RS injD) 1), + (atac 1) + ]); + +qed_goalw "defined_Iup" Up1.thy [Iup_def,UU_up_def] "Iup(x)~=UU_up" + (fn prems => + [ + (rtac notI 1), + (rtac notE 1), + (rtac Inl_not_Inr 1), + (rtac sym 1), + (etac (inj_Abs_Up RS injD) 1) + ]); + + +qed_goal "upE" Up1.thy + "[| p=UU_up ==> Q; !!x. p=Iup(x)==>Q|] ==>Q" + (fn prems => + [ + (rtac (Exh_Up RS disjE) 1), + (eresolve_tac prems 1), + (etac exE 1), + (eresolve_tac prems 1) + ]); + +qed_goalw "Ifup1" Up1.thy [Ifup_def,UU_up_def] + "Ifup(f)(UU_up)=UU" + (fn prems => + [ + (stac Abs_Up_inverse 1), + (stac sum_case_Inl 1), + (rtac refl 1) + ]); + +qed_goalw "Ifup2" Up1.thy [Ifup_def,Iup_def] + "Ifup(f)(Iup(x))=f`x" + (fn prems => + [ + (stac Abs_Up_inverse 1), + (stac sum_case_Inr 1), + (rtac refl 1) + ]); + +val Up0_ss = (simpset_of "Cfun3") addsimps [Ifup1,Ifup2]; + +qed_goalw "less_up1a" Up1.thy [less_up_def,UU_up_def] + "less_up(UU_up)(z)" + (fn prems => + [ + (stac Abs_Up_inverse 1), + (stac sum_case_Inl 1), + (rtac TrueI 1) + ]); + +qed_goalw "less_up1b" Up1.thy [Iup_def,less_up_def,UU_up_def] + "~less_up (Iup x) UU_up" + (fn prems => + [ + (rtac notI 1), + (rtac iffD1 1), + (atac 2), + (stac Abs_Up_inverse 1), + (stac Abs_Up_inverse 1), + (stac sum_case_Inr 1), + (stac sum_case_Inl 1), + (rtac refl 1) + ]); + +qed_goalw "less_up1c" Up1.thy [Iup_def,less_up_def,UU_up_def] + "less_up (Iup x) (Iup y)=(x< + [ + (stac Abs_Up_inverse 1), + (stac Abs_Up_inverse 1), + (stac sum_case_Inr 1), + (stac sum_case_Inr 1), + (rtac refl 1) + ]); + + +qed_goal "refl_less_up" Up1.thy "less_up p p" + (fn prems => + [ + (res_inst_tac [("p","p")] upE 1), + (hyp_subst_tac 1), + (rtac less_up1a 1), + (hyp_subst_tac 1), + (rtac (less_up1c RS iffD2) 1), + (rtac refl_less 1) + ]); + +qed_goal "antisym_less_up" Up1.thy + "!!p1. [|less_up p1 p2;less_up p2 p1|] ==> p1=p2" + (fn _ => + [ + (res_inst_tac [("p","p1")] upE 1), + (hyp_subst_tac 1), + (res_inst_tac [("p","p2")] upE 1), + (etac sym 1), + (hyp_subst_tac 1), + (res_inst_tac [("P","less_up (Iup x) UU_up")] notE 1), + (rtac less_up1b 1), + (atac 1), + (hyp_subst_tac 1), + (res_inst_tac [("p","p2")] upE 1), + (hyp_subst_tac 1), + (res_inst_tac [("P","less_up (Iup x) UU_up")] notE 1), + (rtac less_up1b 1), + (atac 1), + (hyp_subst_tac 1), + (rtac arg_cong 1), + (rtac antisym_less 1), + (etac (less_up1c RS iffD1) 1), + (etac (less_up1c RS iffD1) 1) + ]); + +qed_goal "trans_less_up" Up1.thy + "[|less_up p1 p2;less_up p2 p3|] ==> less_up p1 p3" + (fn prems => + [ + (cut_facts_tac prems 1), + (res_inst_tac [("p","p1")] upE 1), + (hyp_subst_tac 1), + (rtac less_up1a 1), + (hyp_subst_tac 1), + (res_inst_tac [("p","p2")] upE 1), + (hyp_subst_tac 1), + (rtac notE 1), + (rtac less_up1b 1), + (atac 1), + (hyp_subst_tac 1), + (res_inst_tac [("p","p3")] upE 1), + (hyp_subst_tac 1), + (rtac notE 1), + (rtac less_up1b 1), + (atac 1), + (hyp_subst_tac 1), + (rtac (less_up1c RS iffD2) 1), + (rtac trans_less 1), + (etac (less_up1c RS iffD1) 1), + (etac (less_up1c RS iffD1) 1) + ]); + diff -r 9174de6c7143 -r d63ffafce255 src/HOLCF/Up1.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Up1.thy Fri Nov 29 12:22:22 1996 +0100 @@ -0,0 +1,51 @@ +(* Title: HOLCF/Up1.thy + ID: $Id$ + Author: Franz Regensburger + Copyright 1993 Technische Universitaet Muenchen + + +Lifting + +*) + +Up1 = Cfun3 + Sum + + +(* new type for lifting *) + +types "u" 1 + +arities "u" :: (pcpo)term + +consts + + Rep_Up :: "('a)u => (void + 'a)" + Abs_Up :: "(void + 'a) => ('a)u" + + Iup :: "'a => ('a)u" + UU_up :: "('a)u" + Ifup :: "('a->'b)=>('a)u => 'b" + less_up :: "('a)u => ('a)u => bool" + +rules + + (*faking a type definition... *) + (* ('a)u is isomorphic to void + 'a *) + + Rep_Up_inverse "Abs_Up(Rep_Up(p)) = p" + Abs_Up_inverse "Rep_Up(Abs_Up(p)) = p" + + (*defining the abstract constants*) + +defs + + UU_up_def "UU_up == Abs_Up(Inl(UU))" + Iup_def "Iup x == Abs_Up(Inr(x))" + + Ifup_def "Ifup(f)(x)== case Rep_Up(x) of Inl(y) => UU | Inr(z) => f`z" + + less_up_def "less_up(x1)(x2) == (case Rep_Up(x1) of + Inl(y1) => True + | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False + | Inr(z2) => y2< + [ + (stac inst_up_po 1), + (rtac less_up1a 1) + ]); + +(* -------------------------------------------------------------------------*) +(* access to less_up in class po *) +(* ------------------------------------------------------------------------ *) + +qed_goal "less_up2b" Up2.thy "~ Iup(x) << UU_up" + (fn prems => + [ + (stac inst_up_po 1), + (rtac less_up1b 1) + ]); + +qed_goal "less_up2c" Up2.thy "(Iup(x)< + [ + (stac inst_up_po 1), + (rtac less_up1c 1) + ]); + +(* ------------------------------------------------------------------------ *) +(* Iup and Ifup are monotone *) +(* ------------------------------------------------------------------------ *) + +qed_goalw "monofun_Iup" Up2.thy [monofun] "monofun(Iup)" + (fn prems => + [ + (strip_tac 1), + (etac (less_up2c RS iffD2) 1) + ]); + +qed_goalw "monofun_Ifup1" Up2.thy [monofun] "monofun(Ifup)" + (fn prems => + [ + (strip_tac 1), + (rtac (less_fun RS iffD2) 1), + (strip_tac 1), + (res_inst_tac [("p","xa")] upE 1), + (asm_simp_tac Up0_ss 1), + (asm_simp_tac Up0_ss 1), + (etac monofun_cfun_fun 1) + ]); + +qed_goalw "monofun_Ifup2" Up2.thy [monofun] "monofun(Ifup(f))" + (fn prems => + [ + (strip_tac 1), + (res_inst_tac [("p","x")] upE 1), + (asm_simp_tac Up0_ss 1), + (asm_simp_tac Up0_ss 1), + (res_inst_tac [("p","y")] upE 1), + (hyp_subst_tac 1), + (rtac notE 1), + (rtac less_up2b 1), + (atac 1), + (asm_simp_tac Up0_ss 1), + (rtac monofun_cfun_arg 1), + (hyp_subst_tac 1), + (etac (less_up2c RS iffD1) 1) + ]); + +(* ------------------------------------------------------------------------ *) +(* Some kind of surjectivity lemma *) +(* ------------------------------------------------------------------------ *) + + +qed_goal "up_lemma1" Up2.thy "z=Iup(x) ==> Iup(Ifup(LAM x.x)(z)) = z" + (fn prems => + [ + (cut_facts_tac prems 1), + (asm_simp_tac Up0_ss 1) + ]); + +(* ------------------------------------------------------------------------ *) +(* ('a)u is a cpo *) +(* ------------------------------------------------------------------------ *) + +qed_goal "lub_up1a" Up2.thy +"[|is_chain(Y);? i x.Y(i)=Iup(x)|] ==>\ +\ range(Y) <<| Iup(lub(range(%i.(Ifup (LAM x.x) (Y(i))))))" + (fn prems => + [ + (cut_facts_tac prems 1), + (rtac is_lubI 1), + (rtac conjI 1), + (rtac ub_rangeI 1), + (rtac allI 1), + (res_inst_tac [("p","Y(i)")] upE 1), + (res_inst_tac [("s","UU_up"),("t","Y(i)")] subst 1), + (etac sym 1), + (rtac minimal_up 1), + (res_inst_tac [("t","Y(i)")] (up_lemma1 RS subst) 1), + (atac 1), + (rtac (less_up2c RS iffD2) 1), + (rtac is_ub_thelub 1), + (etac (monofun_Ifup2 RS ch2ch_monofun) 1), + (strip_tac 1), + (res_inst_tac [("p","u")] upE 1), + (etac exE 1), + (etac exE 1), + (res_inst_tac [("P","Y(i)<\ +\ range(Y) <<| UU_up" + (fn prems => + [ + (cut_facts_tac prems 1), + (rtac is_lubI 1), + (rtac conjI 1), + (rtac ub_rangeI 1), + (rtac allI 1), + (res_inst_tac [("p","Y(i)")] upE 1), + (res_inst_tac [("s","UU_up"),("t","Y(i)")] ssubst 1), + (atac 1), + (rtac refl_less 1), + (rtac notE 1), + (dtac spec 1), + (dtac spec 1), + (atac 1), + (atac 1), + (strip_tac 1), + (rtac minimal_up 1) + ]); + +bind_thm ("thelub_up1a", lub_up1a RS thelubI); +(* +[| is_chain ?Y1; ? i x. ?Y1 i = Iup x |] ==> + lub (range ?Y1) = Iup (lub (range (%i. Iup (LAM x. x) (?Y1 i)))) +*) + +bind_thm ("thelub_up1b", lub_up1b RS thelubI); +(* +[| is_chain ?Y1; ! i x. ?Y1 i ~= Iup x |] ==> + lub (range ?Y1) = UU_up +*) + +qed_goal "cpo_up" Up2.thy + "is_chain(Y::nat=>('a)u) ==> ? x.range(Y) <<|x" + (fn prems => + [ + (cut_facts_tac prems 1), + (rtac disjE 1), + (rtac exI 2), + (etac lub_up1a 2), + (atac 2), + (rtac exI 2), + (etac lub_up1b 2), + (atac 2), + (fast_tac HOL_cs 1) + ]); + diff -r 9174de6c7143 -r d63ffafce255 src/HOLCF/Up2.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Up2.thy Fri Nov 29 12:22:22 1996 +0100 @@ -0,0 +1,25 @@ +(* Title: HOLCF/Up2.thy + ID: $Id$ + Author: Franz Regensburger + Copyright 1993 Technische Universitaet Muenchen + +Class Instance u::(pcpo)po + +*) + +Up2 = Up1 + + +(* Witness for the above arity axiom is up1.ML *) + +arities "u" :: (pcpo)po + +rules + +(* instance of << for type ('a)u *) + +inst_up_po "((op <<)::[('a)u,('a)u]=>bool) = less_up" + +end + + + diff -r 9174de6c7143 -r d63ffafce255 src/HOLCF/Up3.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Up3.ML Fri Nov 29 12:22:22 1996 +0100 @@ -0,0 +1,347 @@ +(* Title: HOLCF/Up3.ML + ID: $Id$ + Author: Franz Regensburger + Copyright 1993 Technische Universitaet Muenchen + +Lemmas for Up3.thy +*) + +open Up3; + +(* -------------------------------------------------------------------------*) +(* some lemmas restated for class pcpo *) +(* ------------------------------------------------------------------------ *) + +qed_goal "less_up3b" Up3.thy "~ Iup(x) << UU" + (fn prems => + [ + (stac inst_up_pcpo 1), + (rtac less_up2b 1) + ]); + +qed_goal "defined_Iup2" Up3.thy "Iup(x) ~= UU" + (fn prems => + [ + (stac inst_up_pcpo 1), + (rtac defined_Iup 1) + ]); + +(* ------------------------------------------------------------------------ *) +(* continuity for Iup *) +(* ------------------------------------------------------------------------ *) + +qed_goal "contlub_Iup" Up3.thy "contlub(Iup)" + (fn prems => + [ + (rtac contlubI 1), + (strip_tac 1), + (rtac trans 1), + (rtac (thelub_up1a RS sym) 2), + (fast_tac HOL_cs 3), + (etac (monofun_Iup RS ch2ch_monofun) 2), + (res_inst_tac [("f","Iup")] arg_cong 1), + (rtac lub_equal 1), + (atac 1), + (rtac (monofun_Ifup2 RS ch2ch_monofun) 1), + (etac (monofun_Iup RS ch2ch_monofun) 1), + (asm_simp_tac Up0_ss 1) + ]); + +qed_goal "cont_Iup" Up3.thy "cont(Iup)" + (fn prems => + [ + (rtac monocontlub2cont 1), + (rtac monofun_Iup 1), + (rtac contlub_Iup 1) + ]); + + +(* ------------------------------------------------------------------------ *) +(* continuity for Ifup *) +(* ------------------------------------------------------------------------ *) + +qed_goal "contlub_Ifup1" Up3.thy "contlub(Ifup)" + (fn prems => + [ + (rtac contlubI 1), + (strip_tac 1), + (rtac trans 1), + (rtac (thelub_fun RS sym) 2), + (etac (monofun_Ifup1 RS ch2ch_monofun) 2), + (rtac ext 1), + (res_inst_tac [("p","x")] upE 1), + (asm_simp_tac Up0_ss 1), + (rtac (lub_const RS thelubI RS sym) 1), + (asm_simp_tac Up0_ss 1), + (etac contlub_cfun_fun 1) + ]); + + +qed_goal "contlub_Ifup2" Up3.thy "contlub(Ifup(f))" + (fn prems => + [ + (rtac contlubI 1), + (strip_tac 1), + (rtac disjE 1), + (stac thelub_up1a 2), + (atac 2), + (atac 2), + (asm_simp_tac Up0_ss 2), + (stac thelub_up1b 3), + (atac 3), + (atac 3), + (fast_tac HOL_cs 1), + (asm_simp_tac Up0_ss 2), + (rtac (chain_UU_I_inverse RS sym) 2), + (rtac allI 2), + (res_inst_tac [("p","Y(i)")] upE 2), + (asm_simp_tac Up0_ss 2), + (rtac notE 2), + (dtac spec 2), + (etac spec 2), + (atac 2), + (stac contlub_cfun_arg 1), + (etac (monofun_Ifup2 RS ch2ch_monofun) 1), + (rtac lub_equal2 1), + (rtac (monofun_fapp2 RS ch2ch_monofun) 2), + (etac (monofun_Ifup2 RS ch2ch_monofun) 2), + (etac (monofun_Ifup2 RS ch2ch_monofun) 2), + (rtac (chain_mono2 RS exE) 1), + (atac 2), + (etac exE 1), + (etac exE 1), + (rtac exI 1), + (res_inst_tac [("s","Iup(x)"),("t","Y(i)")] ssubst 1), + (atac 1), + (rtac defined_Iup2 1), + (rtac exI 1), + (strip_tac 1), + (res_inst_tac [("p","Y(i)")] upE 1), + (asm_simp_tac Up0_ss 2), + (res_inst_tac [("P","Y(i) = UU")] notE 1), + (fast_tac HOL_cs 1), + (stac inst_up_pcpo 1), + (atac 1) + ]); + +qed_goal "cont_Ifup1" Up3.thy "cont(Ifup)" + (fn prems => + [ + (rtac monocontlub2cont 1), + (rtac monofun_Ifup1 1), + (rtac contlub_Ifup1 1) + ]); + +qed_goal "cont_Ifup2" Up3.thy "cont(Ifup(f))" + (fn prems => + [ + (rtac monocontlub2cont 1), + (rtac monofun_Ifup2 1), + (rtac contlub_Ifup2 1) + ]); + + +(* ------------------------------------------------------------------------ *) +(* continuous versions of lemmas for ('a)u *) +(* ------------------------------------------------------------------------ *) + +qed_goalw "Exh_Up1" Up3.thy [up_def] "z = UU | (? x. z = up`x)" + (fn prems => + [ + (simp_tac (Up0_ss addsimps [cont_Iup]) 1), + (stac inst_up_pcpo 1), + (rtac Exh_Up 1) + ]); + +qed_goalw "inject_up" Up3.thy [up_def] "up`x=up`y ==> x=y" + (fn prems => + [ + (cut_facts_tac prems 1), + (rtac inject_Iup 1), + (etac box_equals 1), + (simp_tac (Up0_ss addsimps [cont_Iup]) 1), + (simp_tac (Up0_ss addsimps [cont_Iup]) 1) + ]); + +qed_goalw "defined_up" Up3.thy [up_def] " up`x ~= UU" + (fn prems => + [ + (simp_tac (Up0_ss addsimps [cont_Iup]) 1), + (rtac defined_Iup2 1) + ]); + +qed_goalw "upE1" Up3.thy [up_def] + "[| p=UU ==> Q; !!x. p=up`x==>Q|] ==>Q" + (fn prems => + [ + (rtac upE 1), + (resolve_tac prems 1), + (etac (inst_up_pcpo RS ssubst) 1), + (resolve_tac (tl prems) 1), + (asm_simp_tac (Up0_ss addsimps [cont_Iup]) 1) + ]); + + +qed_goalw "fup1" Up3.thy [up_def,fup_def] "fup`f`UU=UU" + (fn prems => + [ + (stac inst_up_pcpo 1), + (stac beta_cfun 1), + (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1, + cont_Ifup2,cont2cont_CF1L]) 1)), + (stac beta_cfun 1), + (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1, + cont_Ifup2,cont2cont_CF1L]) 1)), + (simp_tac (Up0_ss addsimps [cont_Iup,cont_Ifup1,cont_Ifup2]) 1) + ]); + +qed_goalw "fup2" Up3.thy [up_def,fup_def] "fup`f`(up`x)=f`x" + (fn prems => + [ + (stac beta_cfun 1), + (rtac cont_Iup 1), + (stac beta_cfun 1), + (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1, + cont_Ifup2,cont2cont_CF1L]) 1)), + (stac beta_cfun 1), + (rtac cont_Ifup2 1), + (simp_tac (Up0_ss addsimps [cont_Iup,cont_Ifup1,cont_Ifup2]) 1) + ]); + +qed_goalw "less_up4b" Up3.thy [up_def,fup_def] "~ up`x << UU" + (fn prems => + [ + (simp_tac (Up0_ss addsimps [cont_Iup]) 1), + (rtac less_up3b 1) + ]); + +qed_goalw "less_up4c" Up3.thy [up_def,fup_def] + "(up`x << up`y) = (x< + [ + (simp_tac (Up0_ss addsimps [cont_Iup]) 1), + (rtac less_up2c 1) + ]); + +qed_goalw "thelub_up2a" Up3.thy [up_def,fup_def] +"[| is_chain(Y); ? i x. Y(i) = up`x |] ==>\ +\ lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))" + (fn prems => + [ + (cut_facts_tac prems 1), + (stac beta_cfun 1), + (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1, + cont_Ifup2,cont2cont_CF1L]) 1)), + (stac beta_cfun 1), + (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1, + cont_Ifup2,cont2cont_CF1L]) 1)), + + (stac (beta_cfun RS ext) 1), + (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1, + cont_Ifup2,cont2cont_CF1L]) 1)), + (rtac thelub_up1a 1), + (atac 1), + (etac exE 1), + (etac exE 1), + (rtac exI 1), + (rtac exI 1), + (etac box_equals 1), + (rtac refl 1), + (simp_tac (Up0_ss addsimps [cont_Iup]) 1) + ]); + + + +qed_goalw "thelub_up2b" Up3.thy [up_def,fup_def] +"[| is_chain(Y); ! i x. Y(i) ~= up`x |] ==> lub(range(Y)) = UU" + (fn prems => + [ + (cut_facts_tac prems 1), + (stac inst_up_pcpo 1), + (rtac thelub_up1b 1), + (atac 1), + (strip_tac 1), + (dtac spec 1), + (dtac spec 1), + (rtac swap 1), + (atac 1), + (dtac notnotD 1), + (etac box_equals 1), + (rtac refl 1), + (simp_tac (Up0_ss addsimps [cont_Iup]) 1) + ]); + + +qed_goal "up_lemma2" Up3.thy " (? x.z = up`x) = (z~=UU)" + (fn prems => + [ + (rtac iffI 1), + (etac exE 1), + (hyp_subst_tac 1), + (rtac defined_up 1), + (res_inst_tac [("p","z")] upE1 1), + (etac notE 1), + (atac 1), + (etac exI 1) + ]); + + +qed_goal "thelub_up2a_rev" Up3.thy +"[| is_chain(Y); lub(range(Y)) = up`x |] ==> ? i x. Y(i) = up`x" + (fn prems => + [ + (cut_facts_tac prems 1), + (rtac exE 1), + (rtac chain_UU_I_inverse2 1), + (rtac (up_lemma2 RS iffD1) 1), + (etac exI 1), + (rtac exI 1), + (rtac (up_lemma2 RS iffD2) 1), + (atac 1) + ]); + +qed_goal "thelub_up2b_rev" Up3.thy +"[| is_chain(Y); lub(range(Y)) = UU |] ==> ! i x. Y(i) ~= up`x" + (fn prems => + [ + (cut_facts_tac prems 1), + (rtac allI 1), + (rtac (not_ex RS iffD1) 1), + (rtac contrapos 1), + (etac (up_lemma2 RS iffD1) 2), + (fast_tac (HOL_cs addSDs [chain_UU_I RS spec]) 1) + ]); + + +qed_goal "thelub_up3" Up3.thy +"is_chain(Y) ==> lub(range(Y)) = UU |\ +\ lub(range(Y)) = up`(lub(range(%i. fup`(LAM x.x)`(Y i))))" + (fn prems => + [ + (cut_facts_tac prems 1), + (rtac disjE 1), + (rtac disjI1 2), + (rtac thelub_up2b 2), + (atac 2), + (atac 2), + (rtac disjI2 2), + (rtac thelub_up2a 2), + (atac 2), + (atac 2), + (fast_tac HOL_cs 1) + ]); + +qed_goal "fup3" Up3.thy "fup`up`x=x" + (fn prems => + [ + (res_inst_tac [("p","x")] upE1 1), + (asm_simp_tac ((simpset_of "Cfun3") addsimps [fup1,fup2]) 1), + (asm_simp_tac ((simpset_of "Cfun3") addsimps [fup1,fup2]) 1) + ]); + +(* ------------------------------------------------------------------------ *) +(* install simplifier for ('a)u *) +(* ------------------------------------------------------------------------ *) + +val up_rews = [fup1,fup2,defined_up]; + diff -r 9174de6c7143 -r d63ffafce255 src/HOLCF/Up3.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Up3.thy Fri Nov 29 12:22:22 1996 +0100 @@ -0,0 +1,40 @@ +(* Title: HOLCF/Up3.thy + ID: $Id$ + Author: Franz Regensburger + Copyright 1993 Technische Universitaet Muenchen + + +Class instance of ('a)u for class pcpo + +*) + +Up3 = Up2 + + +arities "u" :: (pcpo)pcpo (* Witness up2.ML *) + +consts + up :: "'a -> ('a)u" + fup :: "('a->'c)-> ('a)u -> 'c" + +rules + + inst_up_pcpo "(UU::('a)u) = UU_up" + +defs + up_def "up == (LAM x.Iup(x))" + fup_def "fup == (LAM f p.Ifup(f)(p))" + +translations + +"case l of up`x => t1" == "fup`(LAM x.t1)`l" + +(* start 8bit 1 *) +translations + +"case l of up`x => t1" == "fup`(¤x.t1)`l" +(* end 8bit 1 *) + +end + + +