src/HOLCF/Lift.thy
changeset 16755 fd02f9d06e43
parent 16749 c96aaaf25f48
child 16757 b8bfd086f7d4
equal deleted inserted replaced
16754:1b979f8b7e8e 16755:fd02f9d06e43
    31 lemma Def_inject: "(Def x = Def y) = (x = y)"
    31 lemma Def_inject: "(Def x = Def y) = (x = y)"
    32 by (simp add: Def_def Abs_lift_inject lift_def)
    32 by (simp add: Def_def Abs_lift_inject lift_def)
    33 
    33 
    34 lemma lift_induct: "\<lbrakk>P \<bottom>; \<And>x. P (Def x)\<rbrakk> \<Longrightarrow> P y"
    34 lemma lift_induct: "\<lbrakk>P \<bottom>; \<And>x. P (Def x)\<rbrakk> \<Longrightarrow> P y"
    35 apply (induct y)
    35 apply (induct y)
    36 apply (rule_tac p=y in upE1)
    36 apply (rule_tac p=y in upE)
    37 apply (simp add: Abs_lift_strict)
    37 apply (simp add: Abs_lift_strict)
    38 apply (case_tac x)
    38 apply (case_tac x)
    39 apply (simp add: Def_def)
    39 apply (simp add: Def_def)
    40 done
    40 done
    41 
    41 
   196 text {*
   196 text {*
   197   \medskip Extension of @{text cont_tac} and installation of simplifier.
   197   \medskip Extension of @{text cont_tac} and installation of simplifier.
   198 *}
   198 *}
   199 
   199 
   200 lemmas cont_lemmas_ext [simp] =
   200 lemmas cont_lemmas_ext [simp] =
       
   201   cont2cont_flift1
   201   cont_flift1_arg_and_not_arg cont2cont_lambda
   202   cont_flift1_arg_and_not_arg cont2cont_lambda
   202   cont_Rep_CFun_app cont_Rep_CFun_app_app cont_if
   203   cont_Rep_CFun_app cont_Rep_CFun_app_app cont_if
   203 
   204 
   204 ML {*
   205 ML {*
   205 val cont_lemmas2 = cont_lemmas1 @ thms "cont_lemmas_ext";
   206 val cont_lemmas2 = cont_lemmas1 @ thms "cont_lemmas_ext";
   207 fun cont_tac  i = resolve_tac cont_lemmas2 i;
   208 fun cont_tac  i = resolve_tac cont_lemmas2 i;
   208 fun cont_tacR i = REPEAT (cont_tac i);
   209 fun cont_tacR i = REPEAT (cont_tac i);
   209 
   210 
   210 local val flift1_def = thm "flift1_def"
   211 local val flift1_def = thm "flift1_def"
   211 in fun cont_tacRs i =
   212 in fun cont_tacRs i =
   212   simp_tac (simpset() addsimps [flift1_def]) i THEN
   213   simp_tac (simpset() (* addsimps [flift1_def] *)) i THEN
   213   REPEAT (cont_tac i)
   214   REPEAT (cont_tac i)
   214 end;
   215 end;
   215 *}
   216 *}
   216 
   217 
   217 end
   218 end