src/HOL/UNITY/ProgressSets.thy
changeset 13885 de6fac7d5351
parent 13874 0da2141606c6
child 13888 16f424af58a2
     1.1 --- a/src/HOL/UNITY/ProgressSets.thy	Tue Mar 25 10:03:11 2003 +0100
     1.2 +++ b/src/HOL/UNITY/ProgressSets.thy	Wed Mar 26 12:25:56 2003 +0100
     1.3 @@ -318,12 +318,18 @@
     1.4  
     1.5  
     1.6  
     1.7 -subsubsection {*Derived Relation from a Lattice*}
     1.8 +subsubsection {*Lattices and Relations*}
     1.9  text{*From Meier's thesis, section 4.5.3*}
    1.10  
    1.11  constdefs
    1.12    relcl :: "'a set set => ('a * 'a) set"
    1.13 +    -- {*Derived relation from a lattice*}
    1.14      "relcl L == {(x,y). y \<in> cl L {x}}"
    1.15 +  
    1.16 +  latticeof :: "('a * 'a) set => 'a set set"
    1.17 +    -- {*Derived lattice from a relation: the set of upwards-closed sets*}
    1.18 +    "latticeof r == {X. \<forall>s t. s \<in> X & (s,t) \<in> r --> t \<in> X}"
    1.19 +
    1.20  
    1.21  lemma relcl_refl: "(a,a) \<in> relcl L"
    1.22  by (simp add: relcl_def subset_cl [THEN subsetD])
    1.23 @@ -340,14 +346,59 @@
    1.24  lemma trans_relcl: "lattice L ==> trans (relcl L)"
    1.25  by (blast intro: relcl_trans transI)
    1.26  
    1.27 -text{*Related to equation (4.71) of Meier's thesis*}
    1.28 +lemma lattice_latticeof: "lattice (latticeof r)"
    1.29 +by (auto simp add: lattice_def latticeof_def)
    1.30 +
    1.31 +lemma lattice_singletonI:
    1.32 +     "[|lattice L; !!s. s \<in> X ==> {s} \<in> L|] ==> X \<in> L"
    1.33 +apply (cut_tac UN_singleton [of X]) 
    1.34 +apply (erule subst) 
    1.35 +apply (simp only: UN_in_lattice) 
    1.36 +done
    1.37 +
    1.38 +text{*Equation (4.71) of Meier's thesis.  He gives no proof.*}
    1.39 +lemma cl_latticeof:
    1.40 +     "[|refl UNIV r; trans r|] 
    1.41 +      ==> cl (latticeof r) X = {t. \<exists>s. s\<in>X & (s,t) \<in> r}" 
    1.42 +apply (rule equalityI) 
    1.43 + apply (rule cl_least) 
    1.44 +  apply (simp (no_asm_use) add: latticeof_def trans_def, blast)
    1.45 + apply (simp add: latticeof_def refl_def, blast)
    1.46 +apply (simp add: latticeof_def, clarify)
    1.47 +apply (unfold cl_def, blast) 
    1.48 +done
    1.49 +
    1.50 +text{*Related to (4.71).*}
    1.51  lemma cl_eq_Collect_relcl:
    1.52       "lattice L ==> cl L X = {t. \<exists>s. s\<in>X & (s,t) \<in> relcl L}" 
    1.53 -apply (cut_tac UN_singleton [of X, symmetric]) 
    1.54 -apply (erule ssubst) 
    1.55 +apply (cut_tac UN_singleton [of X]) 
    1.56 +apply (erule subst) 
    1.57  apply (force simp only: relcl_def cl_UN)
    1.58  done
    1.59  
    1.60 +text{*Meier's theorem of section 4.5.3*}
    1.61 +theorem latticeof_relcl_eq: "lattice L ==> latticeof (relcl L) = L"
    1.62 +apply (rule equalityI) 
    1.63 + prefer 2 apply (force simp add: latticeof_def relcl_def cl_def, clarify) 
    1.64 +apply (rename_tac X)
    1.65 +apply (rule cl_subset_in_lattice)   
    1.66 + prefer 2 apply assumption
    1.67 +apply (drule cl_ident_iff [OF lattice_latticeof, THEN iffD2])
    1.68 +apply (drule equalityD1)   
    1.69 +apply (rule subset_trans) 
    1.70 + prefer 2 apply assumption
    1.71 +apply (thin_tac "?U \<subseteq> X") 
    1.72 +apply (cut_tac A=X in UN_singleton) 
    1.73 +apply (erule subst) 
    1.74 +apply (simp only: cl_UN lattice_latticeof 
    1.75 +                  cl_latticeof [OF refl_relcl trans_relcl]) 
    1.76 +apply (simp add: relcl_def) 
    1.77 +done
    1.78 +
    1.79 +theorem relcl_latticeof_eq:
    1.80 +     "[|refl UNIV r; trans r|] ==> relcl (latticeof r) = r"
    1.81 +by (simp add: relcl_def cl_latticeof, blast)
    1.82 +
    1.83  
    1.84  subsubsection {*Decoupling Theorems*}
    1.85  
    1.86 @@ -421,7 +472,7 @@
    1.87             cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T\<inter>M)))"
    1.88  
    1.89  
    1.90 -lemma commutativity1:
    1.91 +lemma commutativity1_lemma:
    1.92    assumes commutes: "commutes F T B L" 
    1.93        and lattice:  "lattice L"
    1.94        and BL: "B \<in> L"
    1.95 @@ -439,6 +490,20 @@
    1.96  apply (blast intro: rev_subsetD [OF _ wp_mono]) 
    1.97  done
    1.98  
    1.99 +lemma commutativity1:
   1.100 +  assumes leadsTo: "F \<in> A leadsTo B"
   1.101 +      and lattice:  "lattice L"
   1.102 +      and BL: "B \<in> L"
   1.103 +      and TL: "T \<in> L"
   1.104 +      and Fstable: "F \<in> stable T"
   1.105 +      and Gco: "!!X. X\<in>L ==> G \<in> X-B co X"
   1.106 +      and commutes: "commutes F T B L" 
   1.107 +  shows "F\<squnion>G \<in> T\<inter>A leadsTo B"
   1.108 +by (rule progress_set_Union [OF leadsTo _ Fstable subset_refl BL Gco],
   1.109 +    simp add: progress_set_def commutativity1_lemma commutes lattice BL TL) 
   1.110 +
   1.111 +
   1.112 +
   1.113  text{*Possibly move to Relation.thy, after @{term single_valued}*}
   1.114  constdefs
   1.115    funof :: "[('a*'b)set, 'a] => 'b"
   1.116 @@ -462,8 +527,8 @@
   1.117  subsubsection{*Commutativity of Functions and Relation*}
   1.118  text{*Thesis, page 109*}
   1.119  
   1.120 -(*FIXME: this proof is an unGodly mess*)
   1.121 -lemma commutativity2:
   1.122 +(*FIXME: this proof is an ungodly mess*)
   1.123 +lemma commutativity2_lemma:
   1.124    assumes dcommutes: 
   1.125          "\<forall>act \<in> Acts F. 
   1.126           \<forall>s \<in> T. \<forall>t. (s,t) \<in> relcl L --> 
   1.127 @@ -478,8 +543,8 @@
   1.128  apply (simp add: commutes_def, clarify)  
   1.129  apply (rename_tac t)
   1.130  apply (subgoal_tac "\<exists>s. (s,t) \<in> relcl L & s \<in> T \<inter> wp act M") 
   1.131 - prefer 2 apply (force simp add: cl_eq_Collect_relcl [OF lattice], simp) 
   1.132 -apply clarify 
   1.133 + prefer 2 
   1.134 + apply (force simp add: cl_eq_Collect_relcl [OF lattice], simp, clarify) 
   1.135  apply (subgoal_tac "\<forall>u\<in>L. s \<in> u --> t \<in> u") 
   1.136   prefer 2 
   1.137   apply (intro ballI impI) 
   1.138 @@ -504,4 +569,25 @@
   1.139  apply (blast intro: TL cl_mono [THEN [2] rev_subsetD])  
   1.140  done
   1.141  
   1.142 +
   1.143 +lemma commutativity2:
   1.144 +  assumes leadsTo: "F \<in> A leadsTo B"
   1.145 +      and dcommutes: 
   1.146 +        "\<forall>act \<in> Acts F. 
   1.147 +         \<forall>s \<in> T. \<forall>t. (s,t) \<in> relcl L --> 
   1.148 +                      s \<in> B | t \<in> B | (funof act s, funof act t) \<in> relcl L"
   1.149 +      and determ: "!!act. act \<in> Acts F ==> single_valued act"
   1.150 +      and total: "!!act. act \<in> Acts F ==> Domain act = UNIV"
   1.151 +      and lattice:  "lattice L"
   1.152 +      and BL: "B \<in> L"
   1.153 +      and TL: "T \<in> L"
   1.154 +      and Fstable: "F \<in> stable T"
   1.155 +      and Gco: "!!X. X\<in>L ==> G \<in> X-B co X"
   1.156 +  shows "F\<squnion>G \<in> T\<inter>A leadsTo B"
   1.157 +apply (rule commutativity1 [OF leadsTo lattice]) 
   1.158 +apply (simp_all add: Gco commutativity2_lemma dcommutes determ total
   1.159 +                     lattice BL TL Fstable)
   1.160 +done
   1.161 +
   1.162 +
   1.163  end