# HG changeset patch # User huffman # Date 1120784972 -7200 # Node ID b8bfd086f7d4351df9a5f159dcd6f7889b55a674 # Parent e05c8039873a7cf3d092f06ff4c74332a4e9c6f8 replaced old continuity rules with new lemma cont2cont_lift_case diff -r e05c8039873a -r b8bfd086f7d4 src/HOLCF/Lift.ML --- a/src/HOLCF/Lift.ML Fri Jul 08 02:42:42 2005 +0200 +++ b/src/HOLCF/Lift.ML Fri Jul 08 03:09:32 2005 +0200 @@ -24,10 +24,6 @@ val Lift_exhaust = thm "Lift_exhaust"; val cont_Rep_CFun_app = thm "cont_Rep_CFun_app"; val cont_Rep_CFun_app_app = thm "cont_Rep_CFun_app_app"; -val cont_flift1_arg = thm "cont_flift1_arg"; -val cont_flift1_arg_and_not_arg = thm "cont_flift1_arg_and_not_arg"; -val cont_flift1_not_arg = thm "cont_flift1_not_arg"; -(*val cont_flift2_arg = thm "cont_flift2_arg";*) val cont_if = thm "cont_if"; val flift1_Def = thm "flift1_Def"; val flift1_strict = thm "flift1_strict"; diff -r e05c8039873a -r b8bfd086f7d4 src/HOLCF/Lift.thy --- a/src/HOLCF/Lift.thy Fri Jul 08 02:42:42 2005 +0200 +++ b/src/HOLCF/Lift.thy Fri Jul 08 03:09:32 2005 +0200 @@ -149,6 +149,15 @@ apply (simp add: cont2cont_lambda) done +lemma cont2cont_lift_case: + "\\y. cont (\x. f x y); cont g\ \ cont (\x. lift_case UU (f x) (g x))" +apply (subgoal_tac "cont (\x. (FLIFT y. f x y)\(g x))") +apply (simp add: flift1_def cont_lift_case2) +apply (simp add: cont2cont_flift1) +done + +text {* rewrites for @{term flift1}, @{term flift2} *} + lemma flift1_Def [simp]: "flift1 f\(Def x) = (f x)" by (simp add: flift1_def cont_lift_case2) @@ -164,42 +173,12 @@ lemma flift2_defined [simp]: "x \ \ \ (flift2 f)\x \ \" by (erule lift_definedE, simp) -text {* old continuity rules *} - -lemma cont_flift1_arg: "cont (lift_case UU f)" - -- {* @{text flift1} is continuous in its argument itself. *} - apply (rule flatdom_strict2cont) - apply simp - done - -lemma cont_flift1_not_arg: "!!f. [| !! a. cont (%y. (f y) a) |] ==> - cont (%y. lift_case UU (f y))" - -- {* @{text flift1} is continuous in a variable that occurs only - in the @{text Def} branch. *} - apply (rule cont2cont_CF1L_rev) - apply (intro strip) - apply (case_tac y) - apply simp - apply simp - done - -lemma cont_flift1_arg_and_not_arg: "!!f. [| !! a. cont (%y. (f y) a); cont g|] ==> - cont (%y. lift_case UU (f y) (g y))" - -- {* @{text flift1} is continuous in a variable that occurs either - in the @{text Def} branch or in the argument. *} - apply (rule_tac t=g in cont2cont_app) - apply (rule cont_flift1_not_arg) - apply auto - apply (rule cont_flift1_arg) - done - text {* \medskip Extension of @{text cont_tac} and installation of simplifier. *} lemmas cont_lemmas_ext [simp] = - cont2cont_flift1 - cont_flift1_arg_and_not_arg cont2cont_lambda + cont2cont_flift1 cont2cont_lift_case cont2cont_lambda cont_Rep_CFun_app cont_Rep_CFun_app_app cont_if ML {* @@ -210,7 +189,7 @@ local val flift1_def = thm "flift1_def" in fun cont_tacRs i = - simp_tac (simpset() (* addsimps [flift1_def] *)) i THEN + simp_tac (simpset()) i THEN REPEAT (cont_tac i) end; *}