src/HOL/HOLCF/Cfun.thy
 changeset 41322 43a5b9a0ee8a parent 41031 9883d1417ce1 child 41400 1a7557cc686a
equal 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 `