# HG changeset patch
# User huffman
# Date 1231981889 28800
# Node ID 9905b660612bce3988711fa08f5a68788b31e233
# Parent  ec072307c69bd8e527bb09a981384f37eaa18127
change to simpler, more extensible continuity simproc

define attribute [cont2cont] for continuity rules;
new continuity simproc just applies cont2cont rules repeatedly;
split theory Product_Cpo from Cprod, so Cfun can import Product_Cpo;
add lemma cont2cont_LAM', which is suitable as a cont2cont rule.

diff -r ec072307c69b -r 9905b660612b src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Wed Jan 14 13:47:14 2009 -0800
+++ b/src/HOLCF/Cfun.thy	Wed Jan 14 17:11:29 2009 -0800
@@ -7,8 +7,7 @@
 header {* The type of continuous functions *}
 
 theory Cfun
-imports Pcpodef Ffun
-uses ("Tools/cont_proc.ML")
+imports Pcpodef Product_Cpo
 begin
 
 defaultsort cpo
@@ -301,7 +300,7 @@
 
 text {* cont2cont lemma for @{term Rep_CFun} *}
 
-lemma cont2cont_Rep_CFun:
+lemma cont2cont_Rep_CFun [cont2cont]:
   assumes f: "cont (\<lambda>x. f x)"
   assumes t: "cont (\<lambda>x. t x)"
   shows "cont (\<lambda>x. (f x)\<cdot>(t x))"
@@ -321,6 +320,11 @@
 
 text {* cont2cont Lemma for @{term "%x. LAM y. f x y"} *}
 
+text {*
+  Not suitable as a cont2cont rule, because on nested lambdas
+  it causes exponential blow-up in the number of subgoals.
+*}
+
 lemma cont2cont_LAM:
   assumes f1: "\<And>x. cont (\<lambda>y. f x y)"
   assumes f2: "\<And>y. cont (\<lambda>x. f x y)"
@@ -331,17 +335,40 @@
   from f2 show "cont f" by (rule cont2cont_lambda)
 qed
 
-text {* continuity simplification procedure *}
+text {*
+  This version does work as a cont2cont rule, since it
+  has only a single subgoal.
+*}
+
+lemma cont2cont_LAM' [cont2cont]:
+  fixes f :: "'a::cpo \<Rightarrow> 'b::cpo \<Rightarrow> 'c::cpo"
+  assumes f: "cont (\<lambda>p. f (fst p) (snd p))"
+  shows "cont (\<lambda>x. \<Lambda> y. f x y)"
+proof (rule cont2cont_LAM)
+  fix x :: 'a
+  have "cont (\<lambda>y. (x, y))"
+    by (rule cont_pair2)
+  with f have "cont (\<lambda>y. f (fst (x, y)) (snd (x, y)))"
+    by (rule cont2cont_app3)
+  thus "cont (\<lambda>y. f x y)"
+    by (simp only: fst_conv snd_conv)
+next
+  fix y :: 'b
+  have "cont (\<lambda>x. (x, y))"
+    by (rule cont_pair1)
+  with f have "cont (\<lambda>x. f (fst (x, y)) (snd (x, y)))"
+    by (rule cont2cont_app3)
+  thus "cont (\<lambda>x. f x y)"
+    by (simp only: fst_conv snd_conv)
+qed
+
+lemma cont2cont_LAM_discrete [cont2cont]:
+  "(\<And>y::'a::discrete_cpo. cont (\<lambda>x. f x y)) \<Longrightarrow> cont (\<lambda>x. \<Lambda> y. f x y)"
+by (simp add: cont2cont_LAM)
 
 lemmas cont_lemmas1 =
   cont_const cont_id cont_Rep_CFun2 cont2cont_Rep_CFun cont2cont_LAM
 
-use "Tools/cont_proc.ML";
-setup ContProc.setup;
-
-(*val cont_tac = (fn i => (resolve_tac cont_lemmas i));*)
-(*val cont_tacR = (fn i => (REPEAT (cont_tac i)));*)
-
 subsection {* Miscellaneous *}
 
 text {* Monotonicity of @{term Abs_CFun} *}
@@ -530,7 +557,8 @@
   monocontlub2cont [OF monofun_strictify2 contlub_strictify2, standard]
 
 lemma strictify_conv_if: "strictify\<cdot>f\<cdot>x = (if x = \<bottom> then \<bottom> else f\<cdot>x)"
-by (unfold strictify_def, simp add: cont_strictify1 cont_strictify2)
+  unfolding strictify_def
+  by (simp add: cont_strictify1 cont_strictify2 cont2cont_LAM)
 
 lemma strictify1 [simp]: "strictify\<cdot>f\<cdot>\<bottom> = \<bottom>"
 by (simp add: strictify_conv_if)
diff -r ec072307c69b -r 9905b660612b src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Wed Jan 14 13:47:14 2009 -0800
+++ b/src/HOLCF/Cont.thy	Wed Jan 14 17:11:29 2009 -0800
@@ -135,18 +135,50 @@
 apply (erule cpo_lubI)
 done
 
+subsection {* Continuity simproc *}
+
+ML {*
+structure Cont2ContData = NamedThmsFun
+  ( val name = "cont2cont" val description = "continuity intro rule" )
+*}
+
+setup {* Cont2ContData.setup *}
+
+text {*
+  Given the term @{term "cont f"}, the procedure tries to construct the
+  theorem @{term "cont f == True"}. If this theorem cannot be completely
+  solved by the introduction rules, then the procedure returns a
+  conditional rewrite rule with the unsolved subgoals as premises.
+*}
+
+setup {*
+let
+  fun solve_cont thy ss t =
+    let
+      val tr = instantiate' [] [SOME (cterm_of thy t)] Eq_TrueI;
+      val rules = Cont2ContData.get (Simplifier.the_context ss);
+      val tac = REPEAT_ALL_NEW (resolve_tac rules);
+    in Option.map fst (Seq.pull (tac 1 tr)) end
+
+  val proc =
+    Simplifier.simproc @{theory} "cont_proc" ["cont f"] solve_cont;
+in
+  Simplifier.map_simpset (fn ss => ss addsimprocs [proc])
+end
+*}
+
 subsection {* Continuity of basic functions *}
 
 text {* The identity function is continuous *}
 
-lemma cont_id: "cont (\<lambda>x. x)"
+lemma cont_id [cont2cont]: "cont (\<lambda>x. x)"
 apply (rule contI)
 apply (erule cpo_lubI)
 done
 
 text {* constant functions are continuous *}
 
-lemma cont_const: "cont (\<lambda>x. c)"
+lemma cont_const [cont2cont]: "cont (\<lambda>x. c)"
 apply (rule contI)
 apply (rule lub_const)
 done
diff -r ec072307c69b -r 9905b660612b src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Wed Jan 14 13:47:14 2009 -0800
+++ b/src/HOLCF/Cprod.thy	Wed Jan 14 17:11:29 2009 -0800
@@ -12,23 +12,6 @@
 
 subsection {* Type @{typ unit} is a pcpo *}
 
-instantiation unit :: sq_ord
-begin
-
-definition
-  less_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<equiv> True"
-
-instance ..
-end
-
-instance unit :: discrete_cpo
-by intro_classes simp
-
-instance unit :: finite_po ..
-
-instance unit :: pcpo
-by intro_classes simp
-
 definition
   unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a" where
   "unit_when = (\<Lambda> a _. a)"
@@ -39,165 +22,6 @@
 lemma unit_when [simp]: "unit_when\<cdot>a\<cdot>u = a"
 by (simp add: unit_when_def)
 
-
-subsection {* Product type is a partial order *}
-
-instantiation "*" :: (sq_ord, sq_ord) sq_ord
-begin
-
-definition
-  less_cprod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
-
-instance ..
-end
-
-instance "*" :: (po, po) po
-proof
-  fix x :: "'a \<times> 'b"
-  show "x \<sqsubseteq> x"
-    unfolding less_cprod_def by simp
-next
-  fix x y :: "'a \<times> 'b"
-  assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
-    unfolding less_cprod_def Pair_fst_snd_eq
-    by (fast intro: antisym_less)
-next
-  fix x y z :: "'a \<times> 'b"
-  assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
-    unfolding less_cprod_def
-    by (fast intro: trans_less)
-qed
-
-subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
-
-lemma prod_lessI: "\<lbrakk>fst p \<sqsubseteq> fst q; snd p \<sqsubseteq> snd q\<rbrakk> \<Longrightarrow> p \<sqsubseteq> q"
-unfolding less_cprod_def by simp
-
-lemma Pair_less_iff [simp]: "(a, b) \<sqsubseteq> (c, d) = (a \<sqsubseteq> c \<and> b \<sqsubseteq> d)"
-unfolding less_cprod_def by simp
-
-text {* Pair @{text "(_,_)"}  is monotone in both arguments *}
-
-lemma monofun_pair1: "monofun (\<lambda>x. (x, y))"
-by (simp add: monofun_def)
-
-lemma monofun_pair2: "monofun (\<lambda>y. (x, y))"
-by (simp add: monofun_def)
-
-lemma monofun_pair:
-  "\<lbrakk>x1 \<sqsubseteq> x2; y1 \<sqsubseteq> y2\<rbrakk> \<Longrightarrow> (x1, y1) \<sqsubseteq> (x2, y2)"
-by simp
-
-text {* @{term fst} and @{term snd} are monotone *}
-
-lemma monofun_fst: "monofun fst"
-by (simp add: monofun_def less_cprod_def)
-
-lemma monofun_snd: "monofun snd"
-by (simp add: monofun_def less_cprod_def)
-
-subsection {* Product type is a cpo *}
-
-lemma is_lub_Pair:
-  "\<lbrakk>range X <<| x; range Y <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (X i, Y i)) <<| (x, y)"
-apply (rule is_lubI [OF ub_rangeI])
-apply (simp add: less_cprod_def is_ub_lub)
-apply (frule ub2ub_monofun [OF monofun_fst])
-apply (drule ub2ub_monofun [OF monofun_snd])
-apply (simp add: less_cprod_def is_lub_lub)
-done
-
-lemma lub_cprod:
-  fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)"
-  assumes S: "chain S"
-  shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
-proof -
-  have "chain (\<lambda>i. fst (S i))"
-    using monofun_fst S by (rule ch2ch_monofun)
-  hence 1: "range (\<lambda>i. fst (S i)) <<| (\<Squnion>i. fst (S i))"
-    by (rule cpo_lubI)
-  have "chain (\<lambda>i. snd (S i))"
-    using monofun_snd S by (rule ch2ch_monofun)
-  hence 2: "range (\<lambda>i. snd (S i)) <<| (\<Squnion>i. snd (S i))"
-    by (rule cpo_lubI)
-  show "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
-    using is_lub_Pair [OF 1 2] by simp
-qed
-
-lemma thelub_cprod:
-  "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo)
-    \<Longrightarrow> (\<Squnion>i. S i) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
-by (rule lub_cprod [THEN thelubI])
-
-instance "*" :: (cpo, cpo) cpo
-proof
-  fix S :: "nat \<Rightarrow> ('a \<times> 'b)"
-  assume "chain S"
-  hence "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
-    by (rule lub_cprod)
-  thus "\<exists>x. range S <<| x" ..
-qed
-
-instance "*" :: (finite_po, finite_po) finite_po ..
-
-instance "*" :: (discrete_cpo, discrete_cpo) discrete_cpo
-proof
-  fix x y :: "'a \<times> 'b"
-  show "x \<sqsubseteq> y \<longleftrightarrow> x = y"
-    unfolding less_cprod_def Pair_fst_snd_eq
-    by simp
-qed
-
-subsection {* Product type is pointed *}
-
-lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
-by (simp add: less_cprod_def)
-
-instance "*" :: (pcpo, pcpo) pcpo
-by intro_classes (fast intro: minimal_cprod)
-
-lemma inst_cprod_pcpo: "\<bottom> = (\<bottom>, \<bottom>)"
-by (rule minimal_cprod [THEN UU_I, symmetric])
-
-
-subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
-
-lemma cont_pair1: "cont (\<lambda>x. (x, y))"
-apply (rule contI)
-apply (rule is_lub_Pair)
-apply (erule cpo_lubI)
-apply (rule lub_const)
-done
-
-lemma cont_pair2: "cont (\<lambda>y. (x, y))"
-apply (rule contI)
-apply (rule is_lub_Pair)
-apply (rule lub_const)
-apply (erule cpo_lubI)
-done
-
-lemma contlub_fst: "contlub fst"
-apply (rule contlubI)
-apply (simp add: thelub_cprod)
-done
-
-lemma contlub_snd: "contlub snd"
-apply (rule contlubI)
-apply (simp add: thelub_cprod)
-done
-
-lemma cont_fst: "cont fst"
-apply (rule monocontlub2cont)
-apply (rule monofun_fst)
-apply (rule contlub_fst)
-done
-
-lemma cont_snd: "cont snd"
-apply (rule monocontlub2cont)
-apply (rule monofun_snd)
-apply (rule contlub_snd)
-done
-
 subsection {* Continuous versions of constants *}
 
 definition
diff -r ec072307c69b -r 9905b660612b src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Wed Jan 14 13:47:14 2009 -0800
+++ b/src/HOLCF/Fixrec.thy	Wed Jan 14 17:11:29 2009 -0800
@@ -55,6 +55,7 @@
   "maybe_when\<cdot>f\<cdot>r\<cdot>fail = f"
   "maybe_when\<cdot>f\<cdot>r\<cdot>(return\<cdot>x) = r\<cdot>x"
 by (simp_all add: return_def fail_def maybe_when_def cont_Rep_maybe
+                  cont2cont_LAM
                   cont_Abs_maybe Abs_maybe_inverse Rep_maybe_strict)
 
 translations
diff -r ec072307c69b -r 9905b660612b src/HOLCF/HOLCF.thy
--- a/src/HOLCF/HOLCF.thy	Wed Jan 14 13:47:14 2009 -0800
+++ b/src/HOLCF/HOLCF.thy	Wed Jan 14 17:11:29 2009 -0800
@@ -10,6 +10,7 @@
 uses
   "holcf_logic.ML"
   "Tools/cont_consts.ML"
+  "Tools/cont_proc.ML"
   "Tools/domain/domain_library.ML"
   "Tools/domain/domain_syntax.ML"
   "Tools/domain/domain_axioms.ML"
diff -r ec072307c69b -r 9905b660612b src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Wed Jan 14 13:47:14 2009 -0800
+++ b/src/HOLCF/IsaMakefile	Wed Jan 14 17:11:29 2009 -0800
@@ -1,5 +1,3 @@
-#
-# $Id$
 #
 # IsaMakefile for HOLCF
 #
@@ -54,6 +52,7 @@
   Pcpodef.thy \
   Pcpo.thy \
   Porder.thy \
+  Product_Cpo.thy \
   Sprod.thy \
   Ssum.thy \
   Tr.thy \
diff -r ec072307c69b -r 9905b660612b src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Wed Jan 14 13:47:14 2009 -0800
+++ b/src/HOLCF/Ssum.thy	Wed Jan 14 17:11:29 2009 -0800
@@ -188,7 +188,7 @@
 
 lemma beta_sscase:
   "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)"
-unfolding sscase_def by (simp add: cont_Rep_Ssum)
+unfolding sscase_def by (simp add: cont_Rep_Ssum cont2cont_LAM)
 
 lemma sscase1 [simp]: "sscase\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>"
 unfolding beta_sscase by (simp add: Rep_Ssum_strict)
diff -r ec072307c69b -r 9905b660612b src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Wed Jan 14 13:47:14 2009 -0800
+++ b/src/HOLCF/Up.thy	Wed Jan 14 17:11:29 2009 -0800
@@ -282,10 +282,10 @@
 text {* properties of fup *}
 
 lemma fup1 [simp]: "fup\<cdot>f\<cdot>\<bottom> = \<bottom>"
-by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo)
+by (simp add: fup_def cont_Ifup1 cont_Ifup2 inst_up_pcpo cont2cont_LAM)
 
 lemma fup2 [simp]: "fup\<cdot>f\<cdot>(up\<cdot>x) = f\<cdot>x"
-by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2)
+by (simp add: up_def fup_def cont_Iup cont_Ifup1 cont_Ifup2 cont2cont_LAM)
 
 lemma fup3 [simp]: "fup\<cdot>up\<cdot>x = x"
 by (cases x, simp_all)
diff -r ec072307c69b -r 9905b660612b src/HOLCF/ex/Stream.thy
--- a/src/HOLCF/ex/Stream.thy	Wed Jan 14 13:47:14 2009 -0800
+++ b/src/HOLCF/ex/Stream.thy	Wed Jan 14 17:11:29 2009 -0800
@@ -521,7 +521,7 @@
 section "smap"
 
 lemma smap_unfold: "smap = (\<Lambda> f t. case t of x&&xs \<Rightarrow> f$x && smap$f$xs)"
-by (insert smap_def [THEN eq_reflection, THEN fix_eq2], auto)
+by (insert smap_def [where 'a='a and 'b='b, THEN eq_reflection, THEN fix_eq2], auto)
 
 lemma smap_empty [simp]: "smap\<cdot>f\<cdot>\<bottom> = \<bottom>"
 by (subst smap_unfold, simp)
@@ -540,7 +540,7 @@
 lemma sfilter_unfold:
  "sfilter = (\<Lambda> p s. case s of x && xs \<Rightarrow>
   If p\<cdot>x then x && sfilter\<cdot>p\<cdot>xs else sfilter\<cdot>p\<cdot>xs fi)"
-by (insert sfilter_def [THEN eq_reflection, THEN fix_eq2], auto)
+by (insert sfilter_def [where 'a='a, THEN eq_reflection, THEN fix_eq2], auto)
 
 lemma strict_sfilter: "sfilter\<cdot>\<bottom> = \<bottom>"
 apply (rule ext_cfun)