# HG changeset patch
# User berghofe
# Date 1160756971 -7200
# Node ID 3b2821e0d541984fcec9e14dc7b0950219871df1
# Parent  10b0821a4d11c369ac9ec0877a8e85b6b33399a5
Adapted to changes in FixedPoint theory.

diff -r 10b0821a4d11 -r 3b2821e0d541 src/HOL/UNITY/Simple/Common.thy
--- a/src/HOL/UNITY/Simple/Common.thy	Fri Oct 13 18:28:51 2006 +0200
+++ b/src/HOL/UNITY/Simple/Common.thy	Fri Oct 13 18:29:31 2006 +0200
@@ -38,7 +38,7 @@
 apply (drule_tac M = "{t. t \<le> n}" in Elimination_sing)
 apply (simp add: atMost_def Stable_def common_def maxfg_def le_max_iff_disj)
 apply (erule Constrains_weaken_R)
-apply (blast intro: order_eq_refl fmono gmono le_trans)
+apply (blast intro: order_eq_refl le_trans dest: fmono gmono)
 done
 
 lemma common_safety:
diff -r 10b0821a4d11 -r 3b2821e0d541 src/HOL/UNITY/Transformers.thy
--- a/src/HOL/UNITY/Transformers.thy	Fri Oct 13 18:28:51 2006 +0200
+++ b/src/HOL/UNITY/Transformers.thy	Fri Oct 13 18:29:31 2006 +0200
@@ -88,7 +88,7 @@
 done
 
 lemma wens_Id [simp]: "wens F Id B = B"
-by (simp add: wens_def gfp_def wp_def awp_def, blast)
+by (simp add: wens_def gfp_def wp_def awp_def Join_set_eq, blast)
 
 text{*These two theorems justify the claim that @{term wens} returns the
 weakest assertion satisfying the ensures property*}
@@ -101,7 +101,7 @@
 
 lemma wens_ensures: "act \<in> Acts F ==> F \<in> (wens F act B) ensures B"
 by (simp add: wens_def gfp_def constrains_def awp_def wp_def
-              ensures_def transient_def, blast) 
+              ensures_def transient_def Join_set_eq, blast)
 
 text{*These two results constitute assertion (4.13) of the thesis*}
 lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B"
@@ -110,7 +110,7 @@
 done
 
 lemma wens_weakening: "B \<subseteq> wens F act B"
-by (simp add: wens_def gfp_def, blast)
+by (simp add: wens_def gfp_def Join_set_eq, blast)
 
 text{*Assertion (6), or 4.16 in the thesis*}
 lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B" 
@@ -120,7 +120,7 @@
 
 text{*Assertion 4.17 in the thesis*}
 lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A" 
-by (simp add: wens_def gfp_def wp_def awp_def constrains_def, blast)
+by (simp add: wens_def gfp_def wp_def awp_def constrains_def Join_set_eq, blast)
   --{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff}
       is declared as an iff-rule, then it's almost impossible to prove. 
       One proof is via @{text meson} after expanding all definitions, but it's
@@ -332,7 +332,7 @@
 
 lemma wens_single_eq:
      "wens (mk_program (init, {act}, allowed)) act B = B \<union> wp act B"
-by (simp add: wens_def gfp_def wp_def, blast)
+by (simp add: wens_def gfp_def wp_def Join_set_eq, blast)
 
 
 text{*Next, we express the @{term "wens_set"} for single-assignment programs*}
diff -r 10b0821a4d11 -r 3b2821e0d541 src/HOL/ex/CTL.thy
--- a/src/HOL/ex/CTL.thy	Fri Oct 13 18:28:51 2006 +0200
+++ b/src/HOL/ex/CTL.thy	Fri Oct 13 18:29:31 2006 +0200
@@ -82,7 +82,7 @@
   First of all, we use the de-Morgan property of fixed points
 *}
 
-lemma lfp_gfp: "lfp f = - gfp (\<lambda>s . - (f (- s)))"
+lemma lfp_gfp: "lfp f = - gfp (\<lambda>s::'a set. - (f (- s)))"
 proof
   show "lfp f \<subseteq> - gfp (\<lambda>s. - f (- s))"
   proof
@@ -90,7 +90,8 @@
     show "x \<in> - gfp (\<lambda>s. - f (- s))"
     proof
       assume "x \<in> gfp (\<lambda>s. - f (- s))"
-      then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)" by (unfold gfp_def) auto
+      then obtain u where "x \<in> u" and "u \<subseteq> - f (- u)"
+	by (auto simp add: gfp_def Join_set_eq)
       then have "f (- u) \<subseteq> - u" by auto
       then have "lfp f \<subseteq> - u" by (rule lfp_lowerbound)
       from l and this have "x \<notin> u" by auto
@@ -107,10 +108,10 @@
   qed
 qed
 
-lemma lfp_gfp': "- lfp f = gfp (\<lambda>s. - (f (- s)))"
+lemma lfp_gfp': "- lfp f = gfp (\<lambda>s::'a set. - (f (- s)))"
   by (simp add: lfp_gfp)
 
-lemma gfp_lfp': "- gfp f = lfp (\<lambda>s. - (f (- s)))"
+lemma gfp_lfp': "- gfp f = lfp (\<lambda>s::'a set. - (f (- s)))"
   by (simp add: lfp_gfp)
 
 text {*
diff -r 10b0821a4d11 -r 3b2821e0d541 src/HOL/ex/MT.ML
--- a/src/HOL/ex/MT.ML	Fri Oct 13 18:28:51 2006 +0200
+++ b/src/HOL/ex/MT.ML	Fri Oct 13 18:29:31 2006 +0200
@@ -70,7 +70,7 @@
   " [| x:lfp(f); mono(f); !!y. y:f(lfp(f) Int {x. P(x)}) ==> P(y) |] ==> \
 \   P(x)";
 by (cut_facts_tac prems 1);
-by (etac lfp_induct 1);
+by (etac (thm "lfp_induct_set") 1);
 by (assume_tac 1);
 by (eresolve_tac prems 1);
 qed "lfp_ind2";