src/HOL/HOLCF/Cfun.thy
changeset 41322 43a5b9a0ee8a
parent 41031 9883d1417ce1
child 41400 1a7557cc686a
equal deleted inserted replaced
41321:4e72b6fc9dd4 41322:43a5b9a0ee8a
   140 
   140 
   141   The simproc does not solve any more goals that would be solved by
   141   The simproc does not solve any more goals that would be solved by
   142   using @{text beta_cfun} as a simp rule.  The advantage of the
   142   using @{text beta_cfun} as a simp rule.  The advantage of the
   143   simproc is that it can avoid deeply-nested calls to the simplifier
   143   simproc is that it can avoid deeply-nested calls to the simplifier
   144   that would otherwise be caused by large continuity side conditions.
   144   that would otherwise be caused by large continuity side conditions.
   145 *}
   145 
   146 
   146   Update: The simproc now uses rule @{text Abs_cfun_inverse2} instead
   147 simproc_setup beta_cfun_proc ("Abs_cfun f\<cdot>x") = {*
   147   of @{text beta_cfun}, to avoid problems with eta-contraction.
       
   148 *}
       
   149 
       
   150 simproc_setup beta_cfun_proc ("Rep_cfun (Abs_cfun f)") = {*
   148   fn phi => fn ss => fn ct =>
   151   fn phi => fn ss => fn ct =>
   149     let
   152     let
   150       val dest = Thm.dest_comb;
   153       val dest = Thm.dest_comb;
   151       val (f, x) = (apfst (snd o dest o snd o dest) o dest) ct;
   154       val f = (snd o dest o snd o dest) ct;
   152       val [T, U] = Thm.dest_ctyp (ctyp_of_term f);
   155       val [T, U] = Thm.dest_ctyp (ctyp_of_term f);
   153       val tr = instantiate' [SOME T, SOME U] [SOME f, SOME x]
   156       val tr = instantiate' [SOME T, SOME U] [SOME f]
   154           (mk_meta_eq @{thm beta_cfun});
   157           (mk_meta_eq @{thm Abs_cfun_inverse2});
   155       val rules = Cont2ContData.get (Simplifier.the_context ss);
   158       val rules = Cont2ContData.get (Simplifier.the_context ss);
   156       val tac = SOLVED' (REPEAT_ALL_NEW (match_tac rules));
   159       val tac = SOLVED' (REPEAT_ALL_NEW (match_tac rules));
   157     in SOME (perhaps (SINGLE (tac 1)) tr) end
   160     in SOME (perhaps (SINGLE (tac 1)) tr) end
   158 *}
   161 *}
   159 
   162 
   249 by (simp add: contlub_cfun_fun contlub_cfun_arg diag_lub)
   252 by (simp add: contlub_cfun_fun contlub_cfun_arg diag_lub)
   250 
   253 
   251 lemma lub_LAM:
   254 lemma lub_LAM:
   252   "\<lbrakk>\<And>x. chain (\<lambda>i. F i x); \<And>i. cont (\<lambda>x. F i x)\<rbrakk>
   255   "\<lbrakk>\<And>x. chain (\<lambda>i. F i x); \<And>i. cont (\<lambda>x. F i x)\<rbrakk>
   253     \<Longrightarrow> (\<Squnion>i. \<Lambda> x. F i x) = (\<Lambda> x. \<Squnion>i. F i x)"
   256     \<Longrightarrow> (\<Squnion>i. \<Lambda> x. F i x) = (\<Lambda> x. \<Squnion>i. F i x)"
   254 apply (simp add: lub_cfun)
   257 by (simp add: lub_cfun lub_fun ch2ch_lambda)
   255 apply (simp add: Abs_cfun_inverse2)
       
   256 apply (simp add: lub_fun ch2ch_lambda)
       
   257 done
       
   258 
   258 
   259 lemmas lub_distribs = lub_APP lub_LAM
   259 lemmas lub_distribs = lub_APP lub_LAM
   260 
   260 
   261 text {* strictness *}
   261 text {* strictness *}
   262 
   262