
diff -r 993471c762b8 -r 95d51043d2a3 src/HOL/UNITY/Guar.thy
--- a/src/HOL/UNITY/Guar.thy	Tue Jul 15 08:25:20 2003 +0200
+++ b/src/HOL/UNITY/Guar.thy	Tue Jul 15 15:12:22 2003 +0200
@@ -26,10 +26,10 @@
                      program_less_le)+)
 
 
-constdefs
+text{*Existential and Universal properties.  I formalize the two-program
+      case, proving equivalence with Chandy and Sanders's n-ary definitions*}
 
-  (*Existential and Universal properties.  I formalize the two-program
-    case, proving equivalence with Chandy and Sanders's n-ary definitions*)
+constdefs
 
   ex_prop  :: "'a program set => bool"
    "ex_prop X == \<forall>F G. F ok G -->F \<in> X | G \<in> X --> (F\<squnion>G) \<in> X"
@@ -44,6 +44,11 @@
    "strict_uv_prop X == 
       SKIP \<in> X & (\<forall>F G. F ok G --> (F \<in> X & G \<in> X) = (F\<squnion>G \<in> X))"
 
+
+text{*Guarantees properties*}
+
+constdefs
+
   guar :: "['a program set, 'a program set] => 'a program set"
           (infixl "guarantees" 55)  (*higher than membership, lower than Co*)
    "X guarantees Y == {F. \<forall>G. F ok G --> F\<squnion>G \<in> X --> F\<squnion>G \<in> Y}"
@@ -64,7 +69,7 @@
   refines :: "['a program, 'a program, 'a program set] => bool"
 			("(3_ refines _ wrt _)" [10,10,10] 10)
   "G refines F wrt X ==
-     \<forall>H. (F ok H  & G ok H & F\<squnion>H \<in> welldef \<inter> X) --> 
+     \<forall>H. (F ok H & G ok H & F\<squnion>H \<in> welldef \<inter> X) --> 
          (G\<squnion>H \<in> welldef \<inter> X)"
 
   iso_refines :: "['a program, 'a program, 'a program set] => bool"
@@ -79,7 +84,8 @@
 by (auto intro: ok_sym simp add: OK_iff_ok)
 
 
-(*** existential properties ***)
+subsection{*Existential Properties*}
+
 lemma ex1 [rule_format]: 
  "[| ex_prop X; finite GG |] ==>  
      GG \<inter> X \<noteq> {}--> OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X"
@@ -109,14 +115,14 @@
 lemma ex_prop_equiv: 
      "ex_prop X = (\<forall>G. G \<in> X = (\<forall>H. (G component_of H) --> H \<in> X))"
 apply auto
-apply (unfold ex_prop_def component_of_def, safe, blast) 
-apply blast 
+apply (unfold ex_prop_def component_of_def, safe, blast, blast) 
 apply (subst Join_commute) 
 apply (drule ok_sym, blast) 
 done
 
 
-(*** universal properties ***)
+subsection{*Universal Properties*}
+
 lemma uv1 [rule_format]: 
      "[| uv_prop X; finite GG |] 
       ==> GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X"
@@ -143,23 +149,20 @@
       (\<forall>GG. finite GG & GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G): X)"
 by (blast intro: uv1 uv2)
 
-(*** guarantees ***)
+subsection{*Guarantees*}
 
 lemma guaranteesI:
-     "(!!G. [| F ok G; F\<squnion>G \<in> X |] ==> F\<squnion>G \<in> Y)  
-      ==> F \<in> X guarantees Y"
+     "(!!G. [| F ok G; F\<squnion>G \<in> X |] ==> F\<squnion>G \<in> Y) ==> F \<in> X guarantees Y"
 by (simp add: guar_def component_def)
 
 lemma guaranteesD: 
-     "[| F \<in> X guarantees Y;  F ok G;  F\<squnion>G \<in> X |]  
-      ==> F\<squnion>G \<in> Y"
+     "[| F \<in> X guarantees Y;  F ok G;  F\<squnion>G \<in> X |] ==> F\<squnion>G \<in> Y"
 by (unfold guar_def component_def, blast)
 
 (*This version of guaranteesD matches more easily in the conclusion
   The major premise can no longer be  F \<subseteq> H since we need to reason about G*)
 lemma component_guaranteesD: 
-     "[| F \<in> X guarantees Y;  F\<squnion>G = H;  H \<in> X;  F ok G |]  
-      ==> H \<in> Y"
+     "[| F \<in> X guarantees Y;  F\<squnion>G = H;  H \<in> X;  F ok G |] ==> H \<in> Y"
 by (unfold guar_def, blast)
 
 lemma guarantees_weaken: 
@@ -185,10 +188,7 @@
 done
 
 lemma guarantees_imp: "(Y = UNIV guarantees Y) ==> ex_prop(Y)"
-apply (simp (no_asm_use) add: guar_def ex_prop_equiv)
-apply safe
-apply (auto simp add: component_of_def dest: sym)
-done
+by (auto simp add: guar_def ex_prop_equiv component_of_def dest: sym)
 
 lemma ex_prop_equiv2: "(ex_prop Y) = (Y = UNIV guarantees Y)"
 apply (rule iffI)
@@ -197,7 +197,7 @@
 done
 
 
-(** Distributive laws.  Re-orient to perform miniscoping **)
+subsection{*Distributive Laws.  Re-Orient to Perform Miniscoping*}
 
 lemma guarantees_UN_left: 
      "(\<Union>i \<in> I. X i) guarantees Y = (\<Inter>i \<in> I. X i guarantees Y)"
@@ -237,7 +237,6 @@
 lemma combining1: 
     "[| F \<in> V guarantees X;  F \<in> (X \<inter> Y) guarantees Z |] 
      ==> F \<in> (V \<inter> Y) guarantees Z"
-
 by (unfold guar_def, blast)
 
 lemma combining2: 
@@ -259,30 +258,26 @@
 by (unfold guar_def, blast)
 
 
-(*** Additional guarantees laws, by lcp ***)
+subsection{*Guarantees: Additional Laws (by lcp)*}
 
 lemma guarantees_Join_Int: 
     "[| F \<in> U guarantees V;  G \<in> X guarantees Y; F ok G |]  
      ==> F\<squnion>G \<in> (U \<inter> X) guarantees (V \<inter> Y)"
-apply (unfold guar_def)
-apply (simp (no_asm))
-apply safe
-apply (simp add: Join_assoc)
+apply (simp add: guar_def, safe)
+ apply (simp add: Join_assoc)
 apply (subgoal_tac "F\<squnion>G\<squnion>Ga = G\<squnion>(F\<squnion>Ga) ")
-apply (simp add: ok_commute)
-apply (simp (no_asm_simp) add: Join_ac)
+ apply (simp add: ok_commute)
+apply (simp add: Join_ac)
 done
 
 lemma guarantees_Join_Un: 
     "[| F \<in> U guarantees V;  G \<in> X guarantees Y; F ok G |]   
      ==> F\<squnion>G \<in> (U \<union> X) guarantees (V \<union> Y)"
-apply (unfold guar_def)
-apply (simp (no_asm))
-apply safe
-apply (simp add: Join_assoc)
+apply (simp add: guar_def, safe)
+ apply (simp add: Join_assoc)
 apply (subgoal_tac "F\<squnion>G\<squnion>Ga = G\<squnion>(F\<squnion>Ga) ")
-apply (simp add: ok_commute)
-apply (simp (no_asm_simp) add: Join_ac)
+ apply (simp add: ok_commute)
+apply (simp add: Join_ac)
 done
 
 lemma guarantees_JN_INT: 
@@ -308,17 +303,13 @@
 done
 
 
-(*** guarantees laws for breaking down the program, by lcp ***)
+subsection{*Guarantees Laws for Breaking Down the Program (by lcp)*}
 
 lemma guarantees_Join_I1: 
      "[| F \<in> X guarantees Y;  F ok G |] ==> F\<squnion>G \<in> X guarantees Y"
-apply (unfold guar_def)
-apply (simp (no_asm))
-apply safe
-apply (simp add: Join_assoc)
-done
+by (simp add: guar_def Join_assoc)
 
-lemma guarantees_Join_I2:
+lemma guarantees_Join_I2:         
      "[| G \<in> X guarantees Y;  F ok G |] ==> F\<squnion>G \<in> X guarantees Y"
 apply (simp add: Join_commute [of _ G] ok_commute [of _ G])
 apply (blast intro: guarantees_Join_I1)
@@ -329,7 +320,8 @@
       ==> (\<Squnion>i \<in> I. (F i)) \<in> X guarantees Y"
 apply (unfold guar_def, clarify)
 apply (drule_tac x = "JOIN (I-{i}) F\<squnion>G" in spec)
-apply (auto intro: OK_imp_ok simp add: JN_Join_diff JN_Join_diff Join_assoc [symmetric])
+apply (auto intro: OK_imp_ok 
+            simp add: JN_Join_diff JN_Join_diff Join_assoc [symmetric])
 done
 
 
@@ -346,12 +338,11 @@
 lemma refines_refl: "F refines F wrt X"
 by (unfold refines_def, blast)
 
-
-(* Goalw [refines_def]
+(*We'd like transitivity, but how do we get it?*)
+lemma refines_trans:
      "[| H refines G wrt X;  G refines F wrt X |] ==> H refines F wrt X"
-by Auto_tac
-qed "refines_trans"; *)
-
+apply (simp add: refines_def) 
+oops
 
 
 lemma strict_ex_refine_lemma: 
@@ -406,21 +397,14 @@
     "(F \<in> X guarantees Y) = (\<forall>H. H \<in> X \<longrightarrow> (F component_of H \<longrightarrow> H \<in> Y))"
 by (unfold guar_def component_of_def, auto)
 
-lemma wg_weakest: "!!X. F:(X guarantees Y) ==> X \<subseteq> (wg F Y)"
+lemma wg_weakest: "!!X. F\<in> (X guarantees Y) ==> X \<subseteq> (wg F Y)"
 by (unfold wg_def, auto)
 
-lemma wg_guarantees: "F:((wg F Y) guarantees Y)"
+lemma wg_guarantees: "F\<in> ((wg F Y) guarantees Y)"
 by (unfold wg_def guar_def, blast)
 
-lemma wg_equiv: 
-  "(H \<in> wg F X) = (F component_of H --> H \<in> X)"
-apply (unfold wg_def)
-apply (simp (no_asm) add: guarantees_equiv)
-apply (rule iffI)
-apply (rule_tac [2] x = "{H}" in exI)
-apply (blast+)
-done
-
+lemma wg_equiv: "(H \<in> wg F X) = (F component_of H --> H \<in> X)"
+by (simp add: guarantees_equiv wg_def, blast)
 
 lemma component_of_wg: "F component_of H ==> (H \<in> wg F X) = (H \<in> X)"
 by (simp add: wg_equiv)
@@ -447,93 +431,62 @@
 by (unfold wx_def, auto)
 
 lemma wx_ex_prop: "ex_prop (wx X)"
-apply (unfold wx_def)
-apply (simp (no_asm) add: ex_prop_equiv)
-apply safe
-apply blast
-apply auto
+apply (simp add: wx_def ex_prop_equiv, safe, blast)
+apply force 
 done
 
 lemma wx_weakest: "\<forall>Z. Z<= X --> ex_prop Z --> Z \<subseteq> wx X"
-by (unfold wx_def, auto)
+by (auto simp add: wx_def)
 
 (* Proposition 6 *)
 lemma wx'_ex_prop: "ex_prop({F. \<forall>G. F ok G --> F\<squnion>G \<in> X})"
 apply (unfold ex_prop_def, safe)
-apply (drule_tac x = "G\<squnion>Ga" in spec)
-apply (force simp add: ok_Join_iff1 Join_assoc)
+ apply (drule_tac x = "G\<squnion>Ga" in spec)
+ apply (force simp add: ok_Join_iff1 Join_assoc)
 apply (drule_tac x = "F\<squnion>Ga" in spec)
-apply (simp (no_asm_use) add: ok_Join_iff1)
-apply safe
-apply (simp (no_asm_simp) add: ok_commute)
-apply (subgoal_tac "F\<squnion>G = G\<squnion>F")
-apply (simp (no_asm_simp) add: Join_assoc)
-apply (simp (no_asm) add: Join_commute)
+apply (simp add: ok_Join_iff1 ok_commute  Join_ac) 
 done
 
-(* Equivalence with the other definition of wx *)
-
-lemma wx_equiv: 
- "wx X = {F. \<forall>G. F ok G --> (F\<squnion>G):X}"
+text{* Equivalence with the other definition of wx *}
 
+lemma wx_equiv: "wx X = {F. \<forall>G. F ok G --> (F\<squnion>G) \<in> X}"
 apply (unfold wx_def, safe)
-apply (simp (no_asm_use) add: ex_prop_def)
-apply (drule_tac x = x in spec)
-apply (drule_tac x = G in spec)
-apply (frule_tac c = "x\<squnion>G" in subsetD, safe)
+ apply (simp add: ex_prop_def, blast) 
 apply (simp (no_asm))
 apply (rule_tac x = "{F. \<forall>G. F ok G --> F\<squnion>G \<in> X}" in exI, safe)
 apply (rule_tac [2] wx'_ex_prop)
-apply (rotate_tac 1)
-apply (drule_tac x = SKIP in spec, auto)
+apply (drule_tac x = SKIP in spec)+
+apply auto 
 done
 
 
-(* Propositions 7 to 11 are about this second definition of wx. And
-   they are the same as the ones proved for the first definition of wx by equivalence *)
+text{* Propositions 7 to 11 are about this second definition of wx. 
+   They are the same as the ones proved for the first definition of wx,
+ by equivalence *}
    
 (* Proposition 12 *)
 (* Main result of the paper *)
-lemma guarantees_wx_eq: 
-   "(X guarantees Y) = wx(-X \<union> Y)"
-apply (unfold guar_def)
-apply (simp (no_asm) add: wx_equiv)
-done
+lemma guarantees_wx_eq: "(X guarantees Y) = wx(-X \<union> Y)"
+by (simp add: guar_def wx_equiv)
 
-(* {* Corollary, but this result has already been proved elsewhere *}
- "ex_prop(X guarantees Y)"
-  by (simp_tac (simpset() addsimps [guar_wx_iff, wx_ex_prop]) 1);
-  qed "guarantees_ex_prop";
-*)
 
 (* Rules given in section 7 of Chandy and Sander's
     Reasoning About Program composition paper *)
-
 lemma stable_guarantees_Always:
-     "Init F \<subseteq> A ==> F:(stable A) guarantees (Always A)"
+     "Init F \<subseteq> A ==> F \<in> (stable A) guarantees (Always A)"
 apply (rule guaranteesI)
-apply (simp (no_asm) add: Join_commute)
+apply (simp add: Join_commute)
 apply (rule stable_Join_Always1)
-apply (simp_all add: invariant_def Join_stable)
+ apply (simp_all add: invariant_def Join_stable)
 done
 
-(* To be moved to WFair.ML *)
-lemma leadsTo_Basis': "[| F \<in> A co A \<union> B; F \<in> transient A |] ==> F \<in> A leadsTo B"
-apply (drule_tac B = "A-B" in constrains_weaken_L)
-apply (drule_tac [2] B = "A-B" in transient_strengthen)
-apply (rule_tac [3] ensuresI [THEN leadsTo_Basis])
-apply (blast+)
-done
-
-
-
 lemma constrains_guarantees_leadsTo:
      "F \<in> transient A ==> F \<in> (A co A \<union> B) guarantees (A leadsTo (B-A))"
 apply (rule guaranteesI)
 apply (rule leadsTo_Basis')
-apply (drule constrains_weaken_R)
-prefer 2 apply assumption
-apply blast
+ apply (drule constrains_weaken_R)
+  prefer 2 apply assumption
+ apply blast
 apply (blast intro: Join_transient_I1)
 done
 




