More occurrences of 'includes' gone.
authorballarin
Thu Oct 16 17:19:47 2008 +0200 (2008-10-16)
changeset 28611983c1855a7af
parent 28610 2ededdda7294
child 28612 a024b0cef522
More occurrences of 'includes' gone.
src/FOL/ex/LocaleTest.thy
src/HOL/Statespace/StateSpaceEx.thy
src/HOLCF/Algebraic.thy
src/HOLCF/CompactBasis.thy
src/HOLCF/Deflation.thy
     1.1 --- a/src/FOL/ex/LocaleTest.thy	Thu Oct 16 17:07:20 2008 +0200
     1.2 +++ b/src/FOL/ex/LocaleTest.thy	Thu Oct 16 17:19:47 2008 +0200
     1.3 @@ -682,13 +682,6 @@
     1.4    "(x ++ y) ++ z = x ++ (y ++ z)"
     1.5    by (simp add: r_def assoc)
     1.6  
     1.7 -lemma (in Rpair_semi)
     1.8 -  includes Rsemi_rev prodP (infixl "***" 65) rprodP (infixl "+++" 65)
     1.9 -  constrains prod :: "['a, 'a] => 'a"
    1.10 -    and rprodP :: "[('a, 'a) pair, ('a, 'a) pair] => ('a, 'a) pair"
    1.11 -  shows "(x +++ y) +++ z = x +++ (y +++ z)"
    1.12 -  apply (rule r_assoc) done
    1.13 -
    1.14  
    1.15  subsection {* Import of Locales with Predicates as Interpretation *}
    1.16  
     2.1 --- a/src/HOL/Statespace/StateSpaceEx.thy	Thu Oct 16 17:07:20 2008 +0200
     2.2 +++ b/src/HOL/Statespace/StateSpaceEx.thy	Thu Oct 16 17:19:47 2008 +0200
     2.3 @@ -201,10 +201,12 @@
     2.4  implemented correctly in future Isabelle versions. *}
     2.5  
     2.6  lemma 
     2.7 - includes foo
     2.8 - shows True
     2.9 +  assumes "foo f a b c p1 i1 p2 i2 p3 i3 p4 i4"
    2.10 +  shows True
    2.11 +proof
    2.12 +  interpret foo [f a b c p1 i1 p2 i2 p3 i3 p4 i4] by fact
    2.13    term "s<a := i>\<cdot>a = i"
    2.14 -  by simp
    2.15 +qed
    2.16  
    2.17  (*
    2.18  lemma 
     3.1 --- a/src/HOLCF/Algebraic.thy	Thu Oct 16 17:07:20 2008 +0200
     3.2 +++ b/src/HOLCF/Algebraic.thy	Thu Oct 16 17:19:47 2008 +0200
     3.3 @@ -157,10 +157,11 @@
     3.4  end
     3.5  
     3.6  lemma pre_deflation_d_f:
     3.7 -  includes finite_deflation d
     3.8 +  assumes "finite_deflation d"
     3.9    assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x"
    3.10    shows "pre_deflation (d oo f)"
    3.11  proof
    3.12 +  interpret d: finite_deflation [d] by fact
    3.13    fix x
    3.14    show "\<And>x. (d oo f)\<cdot>x \<sqsubseteq> x"
    3.15      by (simp, rule trans_less [OF d.less f])
    3.16 @@ -169,10 +170,11 @@
    3.17  qed
    3.18  
    3.19  lemma eventual_iterate_oo_fixed_iff:
    3.20 -  includes finite_deflation d
    3.21 +  assumes "finite_deflation d"
    3.22    assumes f: "\<And>x. f\<cdot>x \<sqsubseteq> x"
    3.23    shows "eventual (\<lambda>n. iterate n\<cdot>(d oo f))\<cdot>x = x \<longleftrightarrow> d\<cdot>x = x \<and> f\<cdot>x = x"
    3.24  proof -
    3.25 +  interpret d: finite_deflation [d] by fact
    3.26    let ?e = "d oo f"
    3.27    interpret e: pre_deflation ["d oo f"]
    3.28      using `finite_deflation d` f
    3.29 @@ -480,10 +482,11 @@
    3.30  is an algebraic deflation. *}
    3.31  
    3.32  lemma
    3.33 -  includes ep_pair e p
    3.34 +  assumes "ep_pair e p"
    3.35    constrains e :: "'a::profinite \<rightarrow> 'b::profinite"
    3.36    shows "\<exists>d. cast\<cdot>d = e oo p"
    3.37  proof
    3.38 +  interpret ep_pair [e p] by fact
    3.39    let ?a = "\<lambda>i. e oo approx i oo p"
    3.40    have a: "\<And>i. finite_deflation (?a i)"
    3.41      apply (rule finite_deflation_e_d_p)
    3.42 @@ -507,13 +510,14 @@
    3.43  an algebraic deflation, then the cpo is bifinite. *}
    3.44  
    3.45  lemma
    3.46 -  includes ep_pair e p
    3.47 +  assumes "ep_pair e p"
    3.48    constrains e :: "'a::cpo \<rightarrow> 'b::profinite"
    3.49    assumes d: "\<And>x. cast\<cdot>d\<cdot>x = e\<cdot>(p\<cdot>x)"
    3.50    obtains a :: "nat \<Rightarrow> 'a \<rightarrow> 'a" where
    3.51      "\<And>i. finite_deflation (a i)"
    3.52      "(\<Squnion>i. a i) = ID"
    3.53  proof
    3.54 +  interpret ep_pair [e p] by fact
    3.55    let ?a = "\<lambda>i. p oo cast\<cdot>(approx i\<cdot>d) oo e"
    3.56    show "\<And>i. finite_deflation (?a i)"
    3.57      apply (rule finite_deflation_p_d_e)
     4.1 --- a/src/HOLCF/CompactBasis.thy	Thu Oct 16 17:07:20 2008 +0200
     4.2 +++ b/src/HOLCF/CompactBasis.thy	Thu Oct 16 17:19:47 2008 +0200
     4.3 @@ -237,14 +237,17 @@
     4.4    where "fold_pd g f t = fold1 f (g ` Rep_pd_basis t)"
     4.5  
     4.6  lemma fold_pd_PDUnit:
     4.7 -  includes ab_semigroup_idem_mult f
     4.8 +  assumes "ab_semigroup_idem_mult f"
     4.9    shows "fold_pd g f (PDUnit x) = g x"
    4.10  unfolding fold_pd_def Rep_PDUnit by simp
    4.11  
    4.12  lemma fold_pd_PDPlus:
    4.13 -  includes ab_semigroup_idem_mult f
    4.14 +  assumes "ab_semigroup_idem_mult f"
    4.15    shows "fold_pd g f (PDPlus t u) = f (fold_pd g f t) (fold_pd g f u)"
    4.16 -unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2)
    4.17 +proof -
    4.18 +  interpret ab_semigroup_idem_mult [f] by fact
    4.19 +  show ?thesis unfolding fold_pd_def Rep_PDPlus by (simp add: image_Un fold1_Un2)
    4.20 +qed
    4.21  
    4.22  text {* Take function for powerdomain basis *}
    4.23  
     5.1 --- a/src/HOLCF/Deflation.thy	Thu Oct 16 17:07:20 2008 +0200
     5.2 +++ b/src/HOLCF/Deflation.thy	Thu Oct 16 17:19:47 2008 +0200
     5.3 @@ -78,12 +78,14 @@
     5.4  *}
     5.5  
     5.6  lemma deflation_less_comp1:
     5.7 -  includes deflation f
     5.8 -  includes deflation g
     5.9 +  assumes "deflation f"
    5.10 +  assumes "deflation g"
    5.11    shows "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>(g\<cdot>x) = f\<cdot>x"
    5.12  proof (rule antisym_less)
    5.13 +  interpret g: deflation [g] by fact
    5.14    from g.less show "f\<cdot>(g\<cdot>x) \<sqsubseteq> f\<cdot>x" by (rule monofun_cfun_arg)
    5.15  next
    5.16 +  interpret f: deflation [f] by fact
    5.17    assume "f \<sqsubseteq> g" hence "f\<cdot>x \<sqsubseteq> g\<cdot>x" by (rule monofun_cfun_fun)
    5.18    hence "f\<cdot>(f\<cdot>x) \<sqsubseteq> f\<cdot>(g\<cdot>x)" by (rule monofun_cfun_arg)
    5.19    also have "f\<cdot>(f\<cdot>x) = f\<cdot>x" by (rule f.idem)
    5.20 @@ -215,9 +217,10 @@
    5.21  by (simp add: deflation.intro e_p_less)
    5.22  
    5.23  lemma deflation_e_d_p:
    5.24 -  includes deflation d
    5.25 +  assumes "deflation d"
    5.26    shows "deflation (e oo d oo p)"
    5.27  proof
    5.28 +  interpret deflation [d] by fact
    5.29    fix x :: 'b
    5.30    show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
    5.31      by (simp add: idem)
    5.32 @@ -226,9 +229,10 @@
    5.33  qed
    5.34  
    5.35  lemma finite_deflation_e_d_p:
    5.36 -  includes finite_deflation d
    5.37 +  assumes "finite_deflation d"
    5.38    shows "finite_deflation (e oo d oo p)"
    5.39  proof
    5.40 +  interpret finite_deflation [d] by fact
    5.41    fix x :: 'b
    5.42    show "(e oo d oo p)\<cdot>((e oo d oo p)\<cdot>x) = (e oo d oo p)\<cdot>x"
    5.43      by (simp add: idem)
    5.44 @@ -243,39 +247,47 @@
    5.45  qed
    5.46  
    5.47  lemma deflation_p_d_e:
    5.48 -  includes deflation d
    5.49 +  assumes "deflation d"
    5.50    assumes d: "\<And>x. d\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>x)"
    5.51    shows "deflation (p oo d oo e)"
    5.52 - apply (default, simp_all)
    5.53 -  apply (rule antisym_less)
    5.54 -   apply (rule monofun_cfun_arg)
    5.55 -   apply (rule trans_less [OF d])
    5.56 -   apply (simp add: e_p_less)
    5.57 -  apply (rule monofun_cfun_arg)
    5.58 -  apply (rule rev_trans_less)
    5.59 -  apply (rule monofun_cfun_arg)
    5.60 -  apply (rule d)
    5.61 -  apply (simp add: d.idem)
    5.62 - apply (rule sq_ord_less_eq_trans)
    5.63 -  apply (rule monofun_cfun_arg)
    5.64 -  apply (rule d.less)
    5.65 - apply (rule e_inverse)
    5.66 -done
    5.67 +proof -
    5.68 +  interpret d: deflation [d] by fact
    5.69 +  show ?thesis
    5.70 +   apply (default, simp_all)
    5.71 +    apply (rule antisym_less)
    5.72 +     apply (rule monofun_cfun_arg)
    5.73 +     apply (rule trans_less [OF d])
    5.74 +     apply (simp add: e_p_less)
    5.75 +    apply (rule monofun_cfun_arg)
    5.76 +    apply (rule rev_trans_less)
    5.77 +    apply (rule monofun_cfun_arg)
    5.78 +    apply (rule d)
    5.79 +    apply (simp add: d.idem)
    5.80 +   apply (rule sq_ord_less_eq_trans)
    5.81 +    apply (rule monofun_cfun_arg)
    5.82 +    apply (rule d.less)
    5.83 +   apply (rule e_inverse)
    5.84 +  done
    5.85 +qed
    5.86  
    5.87  lemma finite_deflation_p_d_e:
    5.88 -  includes finite_deflation d
    5.89 +  assumes "finite_deflation d"
    5.90    assumes d: "\<And>x. d\<cdot>x \<sqsubseteq> e\<cdot>(p\<cdot>x)"
    5.91    shows "finite_deflation (p oo d oo e)"
    5.92 - apply (rule finite_deflation.intro)
    5.93 -  apply (rule deflation_p_d_e)
    5.94 -   apply (rule `deflation d`)
    5.95 -  apply (rule d)
    5.96 - apply (rule finite_deflation_axioms.intro)
    5.97 - apply (rule finite_range_imp_finite_fixes)
    5.98 - apply (simp add: range_composition [where f="\<lambda>x. p\<cdot>x"])
    5.99 - apply (simp add: range_composition [where f="\<lambda>x. d\<cdot>x"])
   5.100 - apply (simp add: d.finite_image)
   5.101 -done
   5.102 +proof -
   5.103 +  interpret d: finite_deflation [d] by fact
   5.104 +  show ?thesis
   5.105 +   apply (rule finite_deflation.intro)
   5.106 +    apply (rule deflation_p_d_e)
   5.107 +     apply (rule `finite_deflation d` [THEN finite_deflation.axioms(1)])
   5.108 +    apply (rule d)
   5.109 +   apply (rule finite_deflation_axioms.intro)
   5.110 +   apply (rule finite_range_imp_finite_fixes)
   5.111 +   apply (simp add: range_composition [where f="\<lambda>x. p\<cdot>x"])
   5.112 +   apply (simp add: range_composition [where f="\<lambda>x. d\<cdot>x"])
   5.113 +   apply (simp add: d.finite_image)
   5.114 +  done
   5.115 +qed
   5.116  
   5.117  end
   5.118