change cpodef-generated cont_Rep rules to cont2cont format
authorhuffman
Tue Nov 30 15:56:19 2010 -0800 (2010-11-30)
changeset 40834a1249aeff5b6
parent 40833 4f130bd9e17e
child 40835 fc750e794458
change cpodef-generated cont_Rep rules to cont2cont format
src/HOL/HOLCF/Cfun.thy
src/HOL/HOLCF/Cpodef.thy
src/HOL/HOLCF/Domain.thy
src/HOL/HOLCF/Fixrec.thy
src/HOL/HOLCF/Lift.thy
src/HOL/HOLCF/Ssum.thy
src/HOL/HOLCF/ex/Pattern_Match.thy
     1.1 --- a/src/HOL/HOLCF/Cfun.thy	Tue Nov 30 15:34:51 2010 -0800
     1.2 +++ b/src/HOL/HOLCF/Cfun.thy	Tue Nov 30 15:56:19 2010 -0800
     1.3 @@ -192,7 +192,7 @@
     1.4  subsection {* Continuity of application *}
     1.5  
     1.6  lemma cont_Rep_cfun1: "cont (\<lambda>f. f\<cdot>x)"
     1.7 -by (rule cont_Rep_cfun [THEN cont2cont_fun])
     1.8 +by (rule cont_Rep_cfun [OF cont_id, THEN cont2cont_fun])
     1.9  
    1.10  lemma cont_Rep_cfun2: "cont (\<lambda>x. f\<cdot>x)"
    1.11  apply (cut_tac x=f in Rep_cfun)
     2.1 --- a/src/HOL/HOLCF/Cpodef.thy	Tue Nov 30 15:34:51 2010 -0800
     2.2 +++ b/src/HOL/HOLCF/Cpodef.thy	Tue Nov 30 15:56:19 2010 -0800
     2.3 @@ -131,7 +131,8 @@
     2.4    assumes type: "type_definition Rep Abs A"
     2.5      and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     2.6      and adm: "adm (\<lambda>x. x \<in> A)"
     2.7 -  shows "cont Rep"
     2.8 +  shows "cont (\<lambda>x. f x) \<Longrightarrow> cont (\<lambda>x. Rep (f x))"
     2.9 + apply (erule cont_apply [OF _ _ cont_const])
    2.10   apply (rule contI)
    2.11   apply (simp only: typedef_lub [OF type below adm])
    2.12   apply (simp only: Abs_inverse_lub_Rep [OF type below adm])
    2.13 @@ -166,7 +167,7 @@
    2.14    shows "compact (Rep k) \<Longrightarrow> compact k"
    2.15  proof (unfold compact_def)
    2.16    have cont_Rep: "cont Rep"
    2.17 -    by (rule typedef_cont_Rep [OF type below adm])
    2.18 +    by (rule typedef_cont_Rep [OF type below adm cont_id])
    2.19    assume "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> x)"
    2.20    with cont_Rep have "adm (\<lambda>x. \<not> Rep k \<sqsubseteq> Rep x)" by (rule adm_subst)
    2.21    thus "adm (\<lambda>x. \<not> k \<sqsubseteq> x)" by (unfold below)
     3.1 --- a/src/HOL/HOLCF/Domain.thy	Tue Nov 30 15:34:51 2010 -0800
     3.2 +++ b/src/HOL/HOLCF/Domain.thy	Tue Nov 30 15:56:19 2010 -0800
     3.3 @@ -113,7 +113,7 @@
     3.4    have emb_beta: "\<And>x. emb\<cdot>x = Rep x"
     3.5      unfolding emb
     3.6      apply (rule beta_cfun)
     3.7 -    apply (rule typedef_cont_Rep [OF type below adm_defl_set])
     3.8 +    apply (rule typedef_cont_Rep [OF type below adm_defl_set cont_id])
     3.9      done
    3.10    have prj_beta: "\<And>y. prj\<cdot>y = Abs (cast\<cdot>t\<cdot>y)"
    3.11      unfolding prj
     4.1 --- a/src/HOL/HOLCF/Fixrec.thy	Tue Nov 30 15:34:51 2010 -0800
     4.2 +++ b/src/HOL/HOLCF/Fixrec.thy	Tue Nov 30 15:56:19 2010 -0800
     4.3 @@ -80,19 +80,17 @@
     4.4  
     4.5  text {* rewrite rules for mplus *}
     4.6  
     4.7 -lemmas cont2cont_Rep_match = cont_Rep_match [THEN cont_compose]
     4.8 -
     4.9  lemma mplus_strict [simp]: "\<bottom> +++ m = \<bottom>"
    4.10  unfolding mplus_def
    4.11 -by (simp add: cont2cont_Rep_match Rep_match_strict)
    4.12 +by (simp add: cont_Rep_match Rep_match_strict)
    4.13  
    4.14  lemma mplus_fail [simp]: "fail +++ m = m"
    4.15  unfolding mplus_def fail_def
    4.16 -by (simp add: cont2cont_Rep_match Abs_match_inverse)
    4.17 +by (simp add: cont_Rep_match Abs_match_inverse)
    4.18  
    4.19  lemma mplus_succeed [simp]: "succeed\<cdot>x +++ m = succeed\<cdot>x"
    4.20  unfolding mplus_def succeed_def
    4.21 -by (simp add: cont2cont_Rep_match cont_Abs_match Abs_match_inverse)
    4.22 +by (simp add: cont_Rep_match cont_Abs_match Abs_match_inverse)
    4.23  
    4.24  lemma mplus_fail2 [simp]: "m +++ fail = m"
    4.25  by (cases m, simp_all)
     5.1 --- a/src/HOL/HOLCF/Lift.thy	Tue Nov 30 15:34:51 2010 -0800
     5.2 +++ b/src/HOL/HOLCF/Lift.thy	Tue Nov 30 15:56:19 2010 -0800
     5.3 @@ -87,7 +87,7 @@
     5.4  
     5.5  lemma cont2cont_lift_case [simp]:
     5.6    "\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. lift_case \<bottom> (f x) (g x))"
     5.7 -unfolding lift_case_eq by (simp add: cont_Rep_lift [THEN cont_compose])
     5.8 +unfolding lift_case_eq by (simp add: cont_Rep_lift)
     5.9  
    5.10  subsection {* Further operations *}
    5.11  
     6.1 --- a/src/HOL/HOLCF/Ssum.thy	Tue Nov 30 15:34:51 2010 -0800
     6.2 +++ b/src/HOL/HOLCF/Ssum.thy	Tue Nov 30 15:56:19 2010 -0800
     6.3 @@ -172,7 +172,7 @@
     6.4  
     6.5  lemma beta_sscase:
     6.6    "sscase\<cdot>f\<cdot>g\<cdot>s = (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y) (Rep_ssum s)"
     6.7 -unfolding sscase_def by (simp add: cont_Rep_ssum [THEN cont_compose])
     6.8 +unfolding sscase_def by (simp add: cont_Rep_ssum)
     6.9  
    6.10  lemma sscase1 [simp]: "sscase\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>"
    6.11  unfolding beta_sscase by (simp add: Rep_ssum_strict)
     7.1 --- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Tue Nov 30 15:34:51 2010 -0800
     7.2 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Tue Nov 30 15:56:19 2010 -0800
     7.3 @@ -63,7 +63,7 @@
     7.4    "match_bind\<cdot>fail\<cdot>k = fail"
     7.5    "match_bind\<cdot>(succeed\<cdot>x)\<cdot>k = k\<cdot>x"
     7.6  unfolding match_bind_def fail_def succeed_def
     7.7 -by (simp_all add: cont2cont_Rep_match cont_Abs_match
     7.8 +by (simp_all add: cont_Rep_match cont_Abs_match
     7.9    Rep_match_strict Abs_match_inverse)
    7.10  
    7.11  subsection {* Case branch combinator *}