Adapted to changes in FixedPoint theory.
authorberghofe
Fri Oct 13 18:29:31 2006 +0200 (2006-10-13)
changeset 210263b2821e0d541
parent 21025 10b0821a4d11
child 21027 3f89f99d746e
Adapted to changes in FixedPoint theory.
src/HOL/UNITY/Simple/Common.thy
src/HOL/UNITY/Transformers.thy
src/HOL/ex/CTL.thy
src/HOL/ex/MT.ML
     1.1 --- a/src/HOL/UNITY/Simple/Common.thy	Fri Oct 13 18:28:51 2006 +0200
     1.2 +++ b/src/HOL/UNITY/Simple/Common.thy	Fri Oct 13 18:29:31 2006 +0200
     1.3 @@ -38,7 +38,7 @@
     1.4  apply (drule_tac M = "{t. t \<le> n}" in Elimination_sing)
     1.5  apply (simp add: atMost_def Stable_def common_def maxfg_def le_max_iff_disj)
     1.6  apply (erule Constrains_weaken_R)
     1.7 -apply (blast intro: order_eq_refl fmono gmono le_trans)
     1.8 +apply (blast intro: order_eq_refl le_trans dest: fmono gmono)
     1.9  done
    1.10  
    1.11  lemma common_safety:
     2.1 --- a/src/HOL/UNITY/Transformers.thy	Fri Oct 13 18:28:51 2006 +0200
     2.2 +++ b/src/HOL/UNITY/Transformers.thy	Fri Oct 13 18:29:31 2006 +0200
     2.3 @@ -88,7 +88,7 @@
     2.4  done
     2.5  
     2.6  lemma wens_Id [simp]: "wens F Id B = B"
     2.7 -by (simp add: wens_def gfp_def wp_def awp_def, blast)
     2.8 +by (simp add: wens_def gfp_def wp_def awp_def Join_set_eq, blast)
     2.9  
    2.10  text{*These two theorems justify the claim that @{term wens} returns the
    2.11  weakest assertion satisfying the ensures property*}
    2.12 @@ -101,7 +101,7 @@
    2.13  
    2.14  lemma wens_ensures: "act \<in> Acts F ==> F \<in> (wens F act B) ensures B"
    2.15  by (simp add: wens_def gfp_def constrains_def awp_def wp_def
    2.16 -              ensures_def transient_def, blast) 
    2.17 +              ensures_def transient_def Join_set_eq, blast)
    2.18  
    2.19  text{*These two results constitute assertion (4.13) of the thesis*}
    2.20  lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B"
    2.21 @@ -110,7 +110,7 @@
    2.22  done
    2.23  
    2.24  lemma wens_weakening: "B \<subseteq> wens F act B"
    2.25 -by (simp add: wens_def gfp_def, blast)
    2.26 +by (simp add: wens_def gfp_def Join_set_eq, blast)
    2.27  
    2.28  text{*Assertion (6), or 4.16 in the thesis*}
    2.29  lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B" 
    2.30 @@ -120,7 +120,7 @@
    2.31  
    2.32  text{*Assertion 4.17 in the thesis*}
    2.33  lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A" 
    2.34 -by (simp add: wens_def gfp_def wp_def awp_def constrains_def, blast)
    2.35 +by (simp add: wens_def gfp_def wp_def awp_def constrains_def Join_set_eq, blast)
    2.36    --{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff}
    2.37        is declared as an iff-rule, then it's almost impossible to prove. 
    2.38        One proof is via @{text meson} after expanding all definitions, but it's
    2.39 @@ -332,7 +332,7 @@
    2.40  
    2.41  lemma wens_single_eq:
    2.42       "wens (mk_program (init, {act}, allowed)) act B = B \<union> wp act B"
    2.43 -by (simp add: wens_def gfp_def wp_def, blast)
    2.44 +by (simp add: wens_def gfp_def wp_def Join_set_eq, blast)
    2.45  
    2.46  
    2.47  text{*Next, we express the @{term "wens_set"} for single-assignment programs*}
     3.1 --- a/src/HOL/ex/CTL.thy	Fri Oct 13 18:28:51 2006 +0200
     3.2 +++ b/src/HOL/ex/CTL.thy	Fri Oct 13 18:29:31 2006 +0200
     3.3 @@ -82,7 +82,7 @@
     3.4    First of all, we use the de-Morgan property of fixed points
     3.5  *}
     3.6  
     3.7 -lemma lfp_gfp: "lfp f = - gfp (\<lambda>s . - (f (- s)))"
     3.8 +lemma lfp_gfp: "lfp f = - gfp (\<lambda>s::'a set. - (f (- s)))"
     3.9  proof
    3.10    show "lfp f \<subseteq> - gfp (\<lambda>s. - f (- s))"
    3.11    proof
    3.12 @@ -90,7 +90,8 @@
    3.13      show "x \<in> - gfp (\<lambda>s. - f (- s))"
    3.14      proof
    3.15        assume "x \<in> gfp (\<lambda>s. - f (- s))"
    3.16 -      then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)" by (unfold gfp_def) auto
    3.17 +      then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)"
    3.18 +	by (auto simp add: gfp_def Join_set_eq)
    3.19        then have "f (- u) \<subseteq> - u" by auto
    3.20        then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound)
    3.21        from l and this have "x \<notin> u" by auto
    3.22 @@ -107,10 +108,10 @@
    3.23    qed
    3.24  qed
    3.25  
    3.26 -lemma lfp_gfp': "- lfp f = gfp (\<lambda>s. - (f (- s)))"
    3.27 +lemma lfp_gfp': "- lfp f = gfp (\<lambda>s::'a set. - (f (- s)))"
    3.28    by (simp add: lfp_gfp)
    3.29  
    3.30 -lemma gfp_lfp': "- gfp f = lfp (\<lambda>s. - (f (- s)))"
    3.31 +lemma gfp_lfp': "- gfp f = lfp (\<lambda>s::'a set. - (f (- s)))"
    3.32    by (simp add: lfp_gfp)
    3.33  
    3.34  text {*
     4.1 --- a/src/HOL/ex/MT.ML	Fri Oct 13 18:28:51 2006 +0200
     4.2 +++ b/src/HOL/ex/MT.ML	Fri Oct 13 18:29:31 2006 +0200
     4.3 @@ -70,7 +70,7 @@
     4.4    " [| x:lfp(f); mono(f); !!y. y:f(lfp(f) Int {x. P(x)}) ==> P(y) |] ==> \
     4.5  \   P(x)";
     4.6  by (cut_facts_tac prems 1);
     4.7 -by (etac lfp_induct 1);
     4.8 +by (etac (thm "lfp_induct_set") 1);
     4.9  by (assume_tac 1);
    4.10  by (eresolve_tac prems 1);
    4.11  qed "lfp_ind2";