# HG changeset patch
# User ballarin
# Date 1224170387 -7200
# Node ID 983c1855a7aff2aa487a80fa119726041fd28755
# Parent  2ededdda7294985c1cc50bc385782034c1c7e07f
More occurrences of 'includes' gone.

diff -r 2ededdda7294 -r 983c1855a7af src/FOL/ex/LocaleTest.thy
--- a/src/FOL/ex/LocaleTest.thy	Thu Oct 16 17:07:20 2008 +0200
+++ b/src/FOL/ex/LocaleTest.thy	Thu Oct 16 17:19:47 2008 +0200
@@ -682,13 +682,6 @@
   "(x ++ y) ++ z = x ++ (y ++ z)"
   by (simp add: r_def assoc)
 
-lemma (in Rpair_semi)
-  includes Rsemi_rev prodP (infixl "***" 65) rprodP (infixl "+++" 65)
-  constrains prod :: "['a, 'a] => 'a"
-    and rprodP :: "[('a, 'a) pair, ('a, 'a) pair] => ('a, 'a) pair"
-  shows "(x +++ y) +++ z = x +++ (y +++ z)"
-  apply (rule r_assoc) done
-
 
 subsection {* Import of Locales with Predicates as Interpretation *}
 
diff -r 2ededdda7294 -r 983c1855a7af src/HOL/Statespace/StateSpaceEx.thy
--- a/src/HOL/Statespace/StateSpaceEx.thy	Thu Oct 16 17:07:20 2008 +0200
+++ b/src/HOL/Statespace/StateSpaceEx.thy	Thu Oct 16 17:19:47 2008 +0200
@@ -201,10 +201,12 @@
 implemented correctly in future Isabelle versions. *}
 
 lemma 
- includes foo
- shows True
+  assumes "foo f a b c p1 i1 p2 i2 p3 i3 p4 i4"
+  shows True
+proof
+  interpret foo [f a b c p1 i1 p2 i2 p3 i3 p4 i4] by fact
   term "s<a := i>\<cdot>a = i"
-  by simp
+qed
 
 (*
 lemma 
diff -r 2ededdda7294 -r 983c1855a7af src/HOLCF/Algebraic.thy
--- a/src/HOLCF/Algebraic.thy	Thu Oct 16 17:07:20 2008 +0200
+++ b/src/HOLCF/Algebraic.thy	Thu Oct 16 17:19:47 2008 +0200
@@ -157,10 +157,11 @@
 end
 
 lemma pre_deflation_d_f:
-  includes finite_deflation d
+  assumes "finite_deflation d"
   assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x"
   shows "pre_deflation (d oo f)"
 proof
+  interpret d: finite_deflation [d] by fact
   fix x
   show "\<And>x. (d oo f)\<cdot>x \<sqsubseteq> x"
     by (simp, rule trans_less [OF d.less f])
@@ -169,10 +170,11 @@
 qed
 
 lemma eventual_iterate_oo_fixed_iff:
-  includes finite_deflation d
+  assumes "finite_deflation d"
   assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x"
   shows "eventual (\<lambda>n. iterate n\<cdot>(d oo f))\<cdot>x = x \<longleftrightarrow> d\<cdot>x = x \<and> f\<cdot>x = x"
 proof -
+  interpret d: finite_deflation [d] by fact
   let ?e = "d oo f"
   interpret e: pre_deflation ["d oo f"]
     using `finite_deflation d` f
@@ -480,10 +482,11 @@
 is an algebraic deflation. *}
 
 lemma
-  includes ep_pair e p
+  assumes "ep_pair e p"
   constrains e :: "'a::profinite \<rightarrow> 'b::profinite"
   shows "\<exists>d. cast\<cdot>d = e oo p"
 proof
+  interpret ep_pair [e p] by fact
   let ?a = "\<lambda>i. e oo approx i oo p"
   have a: "\<And>i. finite_deflation (?a i)"
     apply (rule finite_deflation_e_d_p)
@@ -507,13 +510,14 @@
 an algebraic deflation, then the cpo is bifinite. *}
 
 lemma
-  includes ep_pair e p
+  assumes "ep_pair e p"
   constrains e :: "'a::cpo \<rightarrow> 'b::profinite"
   assumes d: "\<And>x. cast\<cdot>d\<cdot>x = e\<cdot>(p\<cdot>x)"
   obtains a :: "nat \<Rightarrow> 'a \<rightarrow> 'a" where
     "\<And>i. finite_deflation (a i)"
     "(\<Squnion>i. a i) = ID"
 proof
+  interpret ep_pair [e p] by fact
   let ?a = "\<lambda>i. p oo cast\<cdot>(approx i\<cdot>d) oo e"
   show "\<And>i. finite_deflation (?a i)"
     apply (rule finite_deflation_p_d_e)
diff -r 2ededdda7294 -r 983c1855a7af src/HOLCF/CompactBasis.thy
--- a/src/HOLCF/CompactBasis.thy	Thu Oct 16 17:07:20 2008 +0200
+++ b/src/HOLCF/CompactBasis.thy	Thu Oct 16 17:19:47 2008 +0200
@@ -237,14 +237,17 @@
   where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)"
 
 lemma fold_pd_PDUnit:
-  includes ab_semigroup_idem_mult f
+  assumes "ab_semigroup_idem_mult f"
   shows "fold_pd g f (PDUnit x) = g x"
 unfolding fold_pd_def Rep_PDUnit by simp
 
 lemma fold_pd_PDPlus:
-  includes ab_semigroup_idem_mult f
+  assumes "ab_semigroup_idem_mult f"
   shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
-unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2)
+proof -
+  interpret ab_semigroup_idem_mult [f] by fact
+  show ?thesis unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2)
+qed
 
 text {* Take function for powerdomain basis *}
 
diff -r 2ededdda7294 -r 983c1855a7af src/HOLCF/Deflation.thy
--- a/src/HOLCF/Deflation.thy	Thu Oct 16 17:07:20 2008 +0200
+++ b/src/HOLCF/Deflation.thy	Thu Oct 16 17:19:47 2008 +0200
@@ -78,12 +78,14 @@
 *}
 
 lemma deflation_less_comp1:
-  includes deflation f
-  includes deflation g
+  assumes "deflation f"
+  assumes "deflation g"
   shows "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>(g\<cdot>x) = f\<cdot>x"
 proof (rule antisym_less)
+  interpret g: deflation [g] by fact
   from g.less show "f\<cdot>(g\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
 next
+  interpret f: deflation [f] by fact
   assume "f \<sqsubseteq> g" hence "f\<cdot>x \<sqsubseteq> g\<cdot>x" by (rule monofun_cfun_fun)
   hence "f\<cdot>(f\<cdot>x) \<sqsubseteq> f\<cdot>(g\<cdot>x)" by (rule monofun_cfun_arg)
   also have "f\<cdot>(f\<cdot>x) = f\<cdot>x" by (rule f.idem)
@@ -215,9 +217,10 @@
 by (simp add: deflation.intro e_p_less)
 
 lemma deflation_e_d_p:
-  includes deflation d
+  assumes "deflation d"
   shows "deflation (e oo d oo p)"
 proof
+  interpret deflation [d] by fact
   fix x :: 'b
   show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
     by (simp add: idem)
@@ -226,9 +229,10 @@
 qed
 
 lemma finite_deflation_e_d_p:
-  includes finite_deflation d
+  assumes "finite_deflation d"
   shows "finite_deflation (e oo d oo p)"
 proof
+  interpret finite_deflation [d] by fact
   fix x :: 'b
   show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
     by (simp add: idem)
@@ -243,39 +247,47 @@
 qed
 
 lemma deflation_p_d_e:
-  includes deflation d
+  assumes "deflation d"
   assumes d: "\<And>x. d\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>x)"
   shows "deflation (p oo d oo e)"
- apply (default, simp_all)
-  apply (rule antisym_less)
-   apply (rule monofun_cfun_arg)
-   apply (rule trans_less [OF d])
-   apply (simp add: e_p_less)
-  apply (rule monofun_cfun_arg)
-  apply (rule rev_trans_less)
-  apply (rule monofun_cfun_arg)
-  apply (rule d)
-  apply (simp add: d.idem)
- apply (rule sq_ord_less_eq_trans)
-  apply (rule monofun_cfun_arg)
-  apply (rule d.less)
- apply (rule e_inverse)
-done
+proof -
+  interpret d: deflation [d] by fact
+  show ?thesis
+   apply (default, simp_all)
+    apply (rule antisym_less)
+     apply (rule monofun_cfun_arg)
+     apply (rule trans_less [OF d])
+     apply (simp add: e_p_less)
+    apply (rule monofun_cfun_arg)
+    apply (rule rev_trans_less)
+    apply (rule monofun_cfun_arg)
+    apply (rule d)
+    apply (simp add: d.idem)
+   apply (rule sq_ord_less_eq_trans)
+    apply (rule monofun_cfun_arg)
+    apply (rule d.less)
+   apply (rule e_inverse)
+  done
+qed
 
 lemma finite_deflation_p_d_e:
-  includes finite_deflation d
+  assumes "finite_deflation d"
   assumes d: "\<And>x. d\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>x)"
   shows "finite_deflation (p oo d oo e)"
- apply (rule finite_deflation.intro)
-  apply (rule deflation_p_d_e)
-   apply (rule `deflation d`)
-  apply (rule d)
- apply (rule finite_deflation_axioms.intro)
- apply (rule finite_range_imp_finite_fixes)
- apply (simp add: range_composition [where f="\<lambda>x. p\<cdot>x"])
- apply (simp add: range_composition [where f="\<lambda>x. d\<cdot>x"])
- apply (simp add: d.finite_image)
-done
+proof -
+  interpret d: finite_deflation [d] by fact
+  show ?thesis
+   apply (rule finite_deflation.intro)
+    apply (rule deflation_p_d_e)
+     apply (rule `finite_deflation d` [THEN finite_deflation.axioms(1)])
+    apply (rule d)
+   apply (rule finite_deflation_axioms.intro)
+   apply (rule finite_range_imp_finite_fixes)
+   apply (simp add: range_composition [where f="\<lambda>x. p\<cdot>x"])
+   apply (simp add: range_composition [where f="\<lambda>x. d\<cdot>x"])
+   apply (simp add: d.finite_image)
+  done
+qed
 
 end