1.1 --- a/src/HOLCF/Cfun.thy	Wed Jan 14 13:47:14 2009 -0800
     1.2 +++ b/src/HOLCF/Cfun.thy	Wed Jan 14 17:11:29 2009 -0800
     1.3 @@ -7,8 +7,7 @@
     1.4  header {* The type of continuous functions *}
     1.5  
     1.6  theory Cfun
     1.7 -imports Pcpodef Ffun
     1.8 -uses ("Tools/cont_proc.ML")
     1.9 +imports Pcpodef Product_Cpo
    1.10  begin
    1.11  
    1.12  defaultsort cpo
    1.13 @@ -301,7 +300,7 @@
    1.14  
    1.15  text {* cont2cont lemma for @{term Rep_CFun} *}
    1.16  
    1.17 -lemma cont2cont_Rep_CFun:
    1.18 +lemma cont2cont_Rep_CFun [cont2cont]:
    1.19    assumes f: "cont (\<lambda>x. f x)"
    1.20    assumes t: "cont (\<lambda>x. t x)"
    1.21    shows "cont (\<lambda>x. (f x)\<cdot>(t x))"
    1.22 @@ -321,6 +320,11 @@
    1.23  
    1.24  text {* cont2cont Lemma for @{term "%x. LAM y. f x y"} *}
    1.25  
    1.26 +text {*
    1.27 +  Not suitable as a cont2cont rule, because on nested lambdas
    1.28 +  it causes exponential blow-up in the number of subgoals.
    1.29 +*}
    1.30 +
    1.31  lemma cont2cont_LAM:
    1.32    assumes f1: "\<And>x. cont (\<lambda>y. f x y)"
    1.33    assumes f2: "\<And>y. cont (\<lambda>x. f x y)"
    1.34 @@ -331,17 +335,40 @@
    1.35    from f2 show "cont f" by (rule cont2cont_lambda)
    1.36  qed
    1.37  
    1.38 -text {* continuity simplification procedure *}
    1.39 +text {*
    1.40 +  This version does work as a cont2cont rule, since it
    1.41 +  has only a single subgoal.
    1.42 +*}
    1.43 +
    1.44 +lemma cont2cont_LAM' [cont2cont]:
    1.45 +  fixes f :: "'a::cpo \<Rightarrow> 'b::cpo \<Rightarrow> 'c::cpo"
    1.46 +  assumes f: "cont (\<lambda>p. f (fst p) (snd p))"
    1.47 +  shows "cont (\<lambda>x. \<Lambda> y. f x y)"
    1.48 +proof (rule cont2cont_LAM)
    1.49 +  fix x :: 'a
    1.50 +  have "cont (\<lambda>y. (x, y))"
    1.51 +    by (rule cont_pair2)
    1.52 +  with f have "cont (\<lambda>y. f (fst (x, y)) (snd (x, y)))"
    1.53 +    by (rule cont2cont_app3)
    1.54 +  thus "cont (\<lambda>y. f x y)"
    1.55 +    by (simp only: fst_conv snd_conv)
    1.56 +next
    1.57 +  fix y :: 'b
    1.58 +  have "cont (\<lambda>x. (x, y))"
    1.59 +    by (rule cont_pair1)
    1.60 +  with f have "cont (\<lambda>x. f (fst (x, y)) (snd (x, y)))"
    1.61 +    by (rule cont2cont_app3)
    1.62 +  thus "cont (\<lambda>x. f x y)"
    1.63 +    by (simp only: fst_conv snd_conv)
    1.64 +qed
    1.65 +
    1.66 +lemma cont2cont_LAM_discrete [cont2cont]:
    1.67 +  "(\<And>y::'a::discrete_cpo. cont (\<lambda>x. f x y)) \<Longrightarrow> cont (\<lambda>x. \<Lambda> y. f x y)"
    1.68 +by (simp add: cont2cont_LAM)
    1.69  
    1.70  lemmas cont_lemmas1 =
    1.71    cont_const cont_id cont_Rep_CFun2 cont2cont_Rep_CFun cont2cont_LAM
    1.72  
    1.73 -use "Tools/cont_proc.ML";
    1.74 -setup ContProc.setup;
    1.75 -
    1.76 -(*val cont_tac = (fn i => (resolve_tac cont_lemmas i));*)
    1.77 -(*val cont_tacR = (fn i => (REPEAT (cont_tac i)));*)
    1.78 -
    1.79  subsection {* Miscellaneous *}
    1.80  
    1.81  text {* Monotonicity of @{term Abs_CFun} *}
    1.82 @@ -530,7 +557,8 @@
    1.83    monocontlub2cont [OF monofun_strictify2 contlub_strictify2, standard]
    1.84  
    1.85  lemma strictify_conv_if: "strictify\<cdot>f\<cdot>x = (if x = \<bottom> then \<bottom> else f\<cdot>x)"
    1.86 -by (unfold strictify_def, simp add: cont_strictify1 cont_strictify2)
    1.87 +  unfolding strictify_def
    1.88 +  by (simp add: cont_strictify1 cont_strictify2 cont2cont_LAM)
    1.89  
    1.90  lemma strictify1 [simp]: "strictify\<cdot>f\<cdot>\<bottom> = \<bottom>"
    1.91  by (simp add: strictify_conv_if)

     2.1 --- a/src/HOLCF/Cont.thy	Wed Jan 14 13:47:14 2009 -0800
     2.2 +++ b/src/HOLCF/Cont.thy	Wed Jan 14 17:11:29 2009 -0800
     2.3 @@ -135,18 +135,50 @@
     2.4  apply (erule cpo_lubI)
     2.5  done
     2.6  
     2.7 +subsection {* Continuity simproc *}
     2.8 +
     2.9 +ML {*
    2.10 +structure Cont2ContData = NamedThmsFun
    2.11 +  ( val name = "cont2cont" val description = "continuity intro rule" )
    2.12 +*}
    2.13 +
    2.14 +setup {* Cont2ContData.setup *}
    2.15 +
    2.16 +text {*
    2.17 +  Given the term @{term "cont f"}, the procedure tries to construct the
    2.18 +  theorem @{term "cont f == True"}. If this theorem cannot be completely
    2.19 +  solved by the introduction rules, then the procedure returns a
    2.20 +  conditional rewrite rule with the unsolved subgoals as premises.
    2.21 +*}
    2.22 +
    2.23 +setup {*
    2.24 +let
    2.25 +  fun solve_cont thy ss t =
    2.26 +    let
    2.27 +      val tr = instantiate' [] [SOME (cterm_of thy t)] Eq_TrueI;
    2.28 +      val rules = Cont2ContData.get (Simplifier.the_context ss);
    2.29 +      val tac = REPEAT_ALL_NEW (resolve_tac rules);
    2.30 +    in Option.map fst (Seq.pull (tac 1 tr)) end
    2.31 +
    2.32 +  val proc =
    2.33 +    Simplifier.simproc @{theory} "cont_proc" ["cont f"] solve_cont;
    2.34 +in
    2.35 +  Simplifier.map_simpset (fn ss => ss addsimprocs [proc])
    2.36 +end
    2.37 +*}
    2.38 +
    2.39  subsection {* Continuity of basic functions *}
    2.40  
    2.41  text {* The identity function is continuous *}
    2.42  
    2.43 -lemma cont_id: "cont (\<lambda>x. x)"
    2.44 +lemma cont_id [cont2cont]: "cont (\<lambda>x. x)"
    2.45  apply (rule contI)
    2.46  apply (erule cpo_lubI)
    2.47  done
    2.48  
    2.49  text {* constant functions are continuous *}
    2.50  
    2.51 -lemma cont_const: "cont (\<lambda>x. c)"
    2.52 +lemma cont_const [cont2cont]: "cont (\<lambda>x. c)"
    2.53  apply (rule contI)
    2.54  apply (rule lub_const)
    2.55  done

     3.1 --- a/src/HOLCF/Cprod.thy	Wed Jan 14 13:47:14 2009 -0800
     3.2 +++ b/src/HOLCF/Cprod.thy	Wed Jan 14 17:11:29 2009 -0800
     3.3 @@ -12,23 +12,6 @@
     3.4  
     3.5  subsection {* Type @{typ unit} is a pcpo *}
     3.6  
     3.7 -instantiation unit :: sq_ord
     3.8 -begin
     3.9 -
    3.10 -definition
    3.11 -  less_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<equiv> True"
    3.12 -
    3.13 -instance ..
    3.14 -end
    3.15 -
    3.16 -instance unit :: discrete_cpo
    3.17 -by intro_classes simp
    3.18 -
    3.19 -instance unit :: finite_po ..
    3.20 -
    3.21 -instance unit :: pcpo
    3.22 -by intro_classes simp
    3.23 -
    3.24  definition
    3.25    unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a" where
    3.26    "unit_when = (\<Lambda> a _. a)"
    3.27 @@ -39,165 +22,6 @@
    3.28  lemma unit_when [simp]: "unit_when\<cdot>a\<cdot>u = a"
    3.29  by (simp add: unit_when_def)
    3.30  
    3.31 -
    3.32 -subsection {* Product type is a partial order *}
    3.33 -
    3.34 -instantiation "*" :: (sq_ord, sq_ord) sq_ord
    3.35 -begin
    3.36 -
    3.37 -definition
    3.38 -  less_cprod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
    3.39 -
    3.40 -instance ..
    3.41 -end
    3.42 -
    3.43 -instance "*" :: (po, po) po
    3.44 -proof
    3.45 -  fix x :: "'a \<times> 'b"
    3.46 -  show "x \<sqsubseteq> x"
    3.47 -    unfolding less_cprod_def by simp
    3.48 -next
    3.49 -  fix x y :: "'a \<times> 'b"
    3.50 -  assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
    3.51 -    unfolding less_cprod_def Pair_fst_snd_eq
    3.52 -    by (fast intro: antisym_less)
    3.53 -next
    3.54 -  fix x y z :: "'a \<times> 'b"
    3.55 -  assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
    3.56 -    unfolding less_cprod_def
    3.57 -    by (fast intro: trans_less)
    3.58 -qed
    3.59 -
    3.60 -subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
    3.61 -
    3.62 -lemma prod_lessI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q"
    3.63 -unfolding less_cprod_def by simp
    3.64 -
    3.65 -lemma Pair_less_iff [simp]: "(a, b) \<sqsubseteq> (c, d) = (a \<sqsubseteq> c \<and> b \<sqsubseteq> d)"
    3.66 -unfolding less_cprod_def by simp
    3.67 -
    3.68 -text {* Pair @{text "(_,_)"}  is monotone in both arguments *}
    3.69 -
    3.70 -lemma monofun_pair1: "monofun (\<lambda>x. (x, y))"
    3.71 -by (simp add: monofun_def)
    3.72 -
    3.73 -lemma monofun_pair2: "monofun (\<lambda>y. (x, y))"
    3.74 -by (simp add: monofun_def)
    3.75 -
    3.76 -lemma monofun_pair:
    3.77 -  "\<lbrakk>x1 \<sqsubseteq> x2; y1 \<sqsubseteq> y2\<rbrakk> \<Longrightarrow> (x1, y1) \<sqsubseteq> (x2, y2)"
    3.78 -by simp
    3.79 -
    3.80 -text {* @{term fst} and @{term snd} are monotone *}
    3.81 -
    3.82 -lemma monofun_fst: "monofun fst"
    3.83 -by (simp add: monofun_def less_cprod_def)
    3.84 -
    3.85 -lemma monofun_snd: "monofun snd"
    3.86 -by (simp add: monofun_def less_cprod_def)
    3.87 -
    3.88 -subsection {* Product type is a cpo *}
    3.89 -
    3.90 -lemma is_lub_Pair:
    3.91 -  "\<lbrakk>range X <<| x; range Y <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (X i, Y i)) <<| (x, y)"
    3.92 -apply (rule is_lubI [OF ub_rangeI])
    3.93 -apply (simp add: less_cprod_def is_ub_lub)
    3.94 -apply (frule ub2ub_monofun [OF monofun_fst])
    3.95 -apply (drule ub2ub_monofun [OF monofun_snd])
    3.96 -apply (simp add: less_cprod_def is_lub_lub)
    3.97 -done
    3.98 -
    3.99 -lemma lub_cprod:
   3.100 -  fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)"
   3.101 -  assumes S: "chain S"
   3.102 -  shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
   3.103 -proof -
   3.104 -  have "chain (\<lambda>i. fst (S i))"
   3.105 -    using monofun_fst S by (rule ch2ch_monofun)
   3.106 -  hence 1: "range (\<lambda>i. fst (S i)) <<| (\<Squnion>i. fst (S i))"
   3.107 -    by (rule cpo_lubI)
   3.108 -  have "chain (\<lambda>i. snd (S i))"
   3.109 -    using monofun_snd S by (rule ch2ch_monofun)
   3.110 -  hence 2: "range (\<lambda>i. snd (S i)) <<| (\<Squnion>i. snd (S i))"
   3.111 -    by (rule cpo_lubI)
   3.112 -  show "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
   3.113 -    using is_lub_Pair [OF 1 2] by simp
   3.114 -qed
   3.115 -
   3.116 -lemma thelub_cprod:
   3.117 -  "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo)
   3.118 -    \<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
   3.119 -by (rule lub_cprod [THEN thelubI])
   3.120 -
   3.121 -instance "*" :: (cpo, cpo) cpo
   3.122 -proof
   3.123 -  fix S :: "nat \<Rightarrow> ('a \<times> 'b)"
   3.124 -  assume "chain S"
   3.125 -  hence "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
   3.126 -    by (rule lub_cprod)
   3.127 -  thus "\<exists>x. range S <<| x" ..
   3.128 -qed
   3.129 -
   3.130 -instance "*" :: (finite_po, finite_po) finite_po ..
   3.131 -
   3.132 -instance "*" :: (discrete_cpo, discrete_cpo) discrete_cpo
   3.133 -proof
   3.134 -  fix x y :: "'a \<times> 'b"
   3.135 -  show "x \<sqsubseteq> y \<longleftrightarrow> x = y"
   3.136 -    unfolding less_cprod_def Pair_fst_snd_eq
   3.137 -    by simp
   3.138 -qed
   3.139 -
   3.140 -subsection {* Product type is pointed *}
   3.141 -
   3.142 -lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
   3.143 -by (simp add: less_cprod_def)
   3.144 -
   3.145 -instance "*" :: (pcpo, pcpo) pcpo
   3.146 -by intro_classes (fast intro: minimal_cprod)
   3.147 -
   3.148 -lemma inst_cprod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
   3.149 -by (rule minimal_cprod [THEN UU_I, symmetric])
   3.150 -
   3.151 -
   3.152 -subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
   3.153 -
   3.154 -lemma cont_pair1: "cont (\<lambda>x. (x, y))"
   3.155 -apply (rule contI)
   3.156 -apply (rule is_lub_Pair)
   3.157 -apply (erule cpo_lubI)
   3.158 -apply (rule lub_const)
   3.159 -done
   3.160 -
   3.161 -lemma cont_pair2: "cont (\<lambda>y. (x, y))"
   3.162 -apply (rule contI)
   3.163 -apply (rule is_lub_Pair)
   3.164 -apply (rule lub_const)
   3.165 -apply (erule cpo_lubI)
   3.166 -done
   3.167 -
   3.168 -lemma contlub_fst: "contlub fst"
   3.169 -apply (rule contlubI)
   3.170 -apply (simp add: thelub_cprod)
   3.171 -done
   3.172 -
   3.173 -lemma contlub_snd: "contlub snd"
   3.174 -apply (rule contlubI)
   3.175 -apply (simp add: thelub_cprod)
   3.176 -done
   3.177 -
   3.178 -lemma cont_fst: "cont fst"
   3.179 -apply (rule monocontlub2cont)
   3.180 -apply (rule monofun_fst)
   3.181 -apply (rule contlub_fst)
   3.182 -done
   3.183 -
   3.184 -lemma cont_snd: "cont snd"
   3.185 -apply (rule monocontlub2cont)
   3.186 -apply (rule monofun_snd)
   3.187 -apply (rule contlub_snd)
   3.188 -done
   3.189 -
   3.190  subsection {* Continuous versions of constants *}
   3.191  
   3.192  definition

     4.1 --- a/src/HOLCF/Fixrec.thy	Wed Jan 14 13:47:14 2009 -0800
     4.2 +++ b/src/HOLCF/Fixrec.thy	Wed Jan 14 17:11:29 2009 -0800
     4.3 @@ -55,6 +55,7 @@
     4.4    "maybe_when\<cdot>f\<cdot>r\<cdot>fail = f"
     4.5    "maybe_when\<cdot>f\<cdot>r\<cdot>(return\<cdot>x) = r\<cdot>x"
     4.6  by (simp_all add: return_def fail_def maybe_when_def cont_Rep_maybe
     4.7 +                  cont2cont_LAM
     4.8                    cont_Abs_maybe Abs_maybe_inverse Rep_maybe_strict)
     4.9  
    4.10  translations

     5.1 --- a/src/HOLCF/HOLCF.thy	Wed Jan 14 13:47:14 2009 -0800
     5.2 +++ b/src/HOLCF/HOLCF.thy	Wed Jan 14 17:11:29 2009 -0800
     5.3 @@ -10,6 +10,7 @@
     5.4  uses
     5.5    "holcf_logic.ML"
     5.6    "Tools/cont_consts.ML"
     5.7 +  "Tools/cont_proc.ML"
     5.8    "Tools/domain/domain_library.ML"
     5.9    "Tools/domain/domain_syntax.ML"
    5.10    "Tools/domain/domain_axioms.ML"

     6.1 --- a/src/HOLCF/IsaMakefile	Wed Jan 14 13:47:14 2009 -0800
     6.2 +++ b/src/HOLCF/IsaMakefile	Wed Jan 14 17:11:29 2009 -0800
     6.3 @@ -1,5 +1,3 @@
     6.4 -#
     6.5 -# $Id$
     6.6  #
     6.7  # IsaMakefile for HOLCF
     6.8  #
     6.9 @@ -54,6 +52,7 @@
    6.10    Pcpodef.thy \
    6.11    Pcpo.thy \
    6.12    Porder.thy \
    6.13 +  Product_Cpo.thy \
    6.14    Sprod.thy \
    6.15    Ssum.thy \
    6.16    Tr.thy \

     7.1 --- a/src/HOLCF/Ssum.thy	Wed Jan 14 13:47:14 2009 -0800
     7.2 +++ b/src/HOLCF/Ssum.thy	Wed Jan 14 17:11:29 2009 -0800
     7.3 @@ -188,7 +188,7 @@
     7.4  
     7.5  lemma beta_sscase:
     7.6    "sscase\<cdot>f\<cdot>g\<cdot>s = (\<Lambda><t, x, y>. If t then f\<cdot>x else g\<cdot>y fi)\<cdot>(Rep_Ssum s)"
     7.7 -unfolding sscase_def by (simp add: cont_Rep_Ssum)
     7.8 +unfolding sscase_def by (simp add: cont_Rep_Ssum cont2cont_LAM)
     7.9  
    7.10  lemma sscase1 [simp]: "sscase\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>"
    7.11  unfolding beta_sscase by (simp add: Rep_Ssum_strict)

     8.1 --- a/src/HOLCF/Up.thy	Wed Jan 14 13:47:14 2009 -0800
     8.2 +++ b/src/HOLCF/Up.thy	Wed Jan 14 17:11:29 2009 -0800
     8.3 @@ -282,10 +282,10 @@
     8.4  text {* properties of fup *}
     8.5  
     8.6  lemma fup1 [simp]: "fup\<cdot>f\<cdot>\<bottom> = \<bottom>"
     8.7 -by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo)
     8.8 +by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo cont2cont_LAM)
     8.9  
    8.10  lemma fup2 [simp]: "fup\<cdot>f\<cdot>(up\<cdot>x) = f\<cdot>x"
    8.11 -by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2)
    8.12 +by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2 cont2cont_LAM)
    8.13  
    8.14  lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x"
    8.15  by (cases x, simp_all)

     9.1 --- a/src/HOLCF/ex/Stream.thy	Wed Jan 14 13:47:14 2009 -0800
     9.2 +++ b/src/HOLCF/ex/Stream.thy	Wed Jan 14 17:11:29 2009 -0800
     9.3 @@ -521,7 +521,7 @@
     9.4  section "smap"
     9.5  
     9.6  lemma smap_unfold: "smap = (\<Lambda> f t. case t of x&&xs \<Rightarrow> f$x && smap$f$xs)"
     9.7 -by (insert smap_def [THEN eq_reflection, THEN fix_eq2], auto)
     9.8 +by (insert smap_def [where 'a='a and 'b='b, THEN eq_reflection, THEN fix_eq2], auto)
     9.9  
    9.10  lemma smap_empty [simp]: "smap\<cdot>f\<cdot>\<bottom> = \<bottom>"
    9.11  by (subst smap_unfold, simp)
    9.12 @@ -540,7 +540,7 @@
    9.13  lemma sfilter_unfold:
    9.14   "sfilter = (\<Lambda> p s. case s of x && xs \<Rightarrow>
    9.15    If p\<cdot>x then x && sfilter\<cdot>p\<cdot>xs else sfilter\<cdot>p\<cdot>xs fi)"
    9.16 -by (insert sfilter_def [THEN eq_reflection, THEN fix_eq2], auto)
    9.17 +by (insert sfilter_def [where 'a='a, THEN eq_reflection, THEN fix_eq2], auto)
    9.18  
    9.19  lemma strict_sfilter: "sfilter\<cdot>\<bottom> = \<bottom>"
    9.20  apply (rule ext_cfun)