src/HOL/UNITY/Lift_prog.thy
changeset 13812 91713a1915ee
parent 13805 3786b2fd6808
child 13836 6d0392fc6dc5
     1.1 --- a/src/HOL/UNITY/Lift_prog.thy	Sat Feb 08 14:46:22 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Lift_prog.thy	Sat Feb 08 16:05:33 2003 +0100
     1.3 @@ -47,7 +47,7 @@
     1.4  apply (auto split add: nat_diff_split)
     1.5  done
     1.6  
     1.7 -(*** Injectiveness proof ***)
     1.8 +subsection{*Injectiveness proof*}
     1.9  
    1.10  lemma insert_map_inject1: "(insert_map i x f) = (insert_map i y g) ==> x=y"
    1.11  by (drule_tac x = i in fun_cong, simp)
    1.12 @@ -80,7 +80,7 @@
    1.13  apply (rule inj_onI, auto)
    1.14  done
    1.15  
    1.16 -(*** Surjectiveness proof ***)
    1.17 +subsection{*Surjectiveness proof*}
    1.18  
    1.19  lemma lift_map_drop_map_eq [simp]: "!!s. lift_map i (drop_map i s) = s"
    1.20  apply (unfold lift_map_def drop_map_def)
    1.21 @@ -111,7 +111,11 @@
    1.22  lemma sub_apply [simp]: "sub i f = f i"
    1.23  by (simp add: sub_def)
    1.24  
    1.25 -(*** lift_set ***)
    1.26 +lemma all_total_lift: "all_total F ==> all_total (lift i F)"
    1.27 +by (simp add: lift_def rename_def Extend.all_total_extend)
    1.28 +
    1.29 +
    1.30 +subsection{*The Operator @{term lift_set}*}
    1.31  
    1.32  lemma lift_set_empty [simp]: "lift_set i {} = {}"
    1.33  by (unfold lift_set_def, auto)
    1.34 @@ -133,9 +137,7 @@
    1.35  done
    1.36  
    1.37  lemma lift_set_Un_distrib: "lift_set i (A \<union> B) = lift_set i A \<union> lift_set i B"
    1.38 -apply (unfold lift_set_def)
    1.39 -apply (simp add: image_Un)
    1.40 -done
    1.41 +by (simp add: lift_set_def image_Un)
    1.42  
    1.43  lemma lift_set_Diff_distrib: "lift_set i (A-B) = lift_set i A - lift_set i B"
    1.44  apply (unfold lift_set_def)
    1.45 @@ -143,7 +145,7 @@
    1.46  done
    1.47  
    1.48  
    1.49 -(*** the lattice operations ***)
    1.50 +subsection{*The Lattice Operations*}
    1.51  
    1.52  lemma bij_lift [iff]: "bij (lift i)"
    1.53  by (simp add: lift_def)
    1.54 @@ -157,7 +159,7 @@
    1.55  lemma lift_JN [simp]: "lift j (JOIN I F) = (\<Squnion>i \<in> I. lift j (F i))"
    1.56  by (simp add: lift_def)
    1.57  
    1.58 -(*** Safety: co, stable, invariant ***)
    1.59 +subsection{*Safety: constrains, stable, invariant*}
    1.60  
    1.61  lemma lift_constrains: 
    1.62       "(lift i F \<in> (lift_set i A) co (lift_set i B)) = (F \<in> A co B)"
    1.63 @@ -169,29 +171,21 @@
    1.64  
    1.65  lemma lift_invariant: 
    1.66       "(lift i F \<in> invariant (lift_set i A)) = (F \<in> invariant A)"
    1.67 -apply (unfold lift_def lift_set_def)
    1.68 -apply (simp add: rename_invariant)
    1.69 -done
    1.70 +by (simp add: lift_def lift_set_def rename_invariant)
    1.71  
    1.72  lemma lift_Constrains: 
    1.73       "(lift i F \<in> (lift_set i A) Co (lift_set i B)) = (F \<in> A Co B)"
    1.74 -apply (unfold lift_def lift_set_def)
    1.75 -apply (simp add: rename_Constrains)
    1.76 -done
    1.77 +by (simp add: lift_def lift_set_def rename_Constrains)
    1.78  
    1.79  lemma lift_Stable: 
    1.80       "(lift i F \<in> Stable (lift_set i A)) = (F \<in> Stable A)"
    1.81 -apply (unfold lift_def lift_set_def)
    1.82 -apply (simp add: rename_Stable)
    1.83 -done
    1.84 +by (simp add: lift_def lift_set_def rename_Stable)
    1.85  
    1.86  lemma lift_Always: 
    1.87       "(lift i F \<in> Always (lift_set i A)) = (F \<in> Always A)"
    1.88 -apply (unfold lift_def lift_set_def)
    1.89 -apply (simp add: rename_Always)
    1.90 -done
    1.91 +by (simp add: lift_def lift_set_def rename_Always)
    1.92  
    1.93 -(*** Progress: transient, ensures ***)
    1.94 +subsection{*Progress: transient, ensures*}
    1.95  
    1.96  lemma lift_transient: 
    1.97       "(lift i F \<in> transient (lift_set i A)) = (F \<in> transient A)"
    1.98 @@ -223,16 +217,12 @@
    1.99  apply (simp add: o_def)
   1.100  done
   1.101  
   1.102 -lemma lift_guarantees_eq_lift_inv: "(lift i F \<in> X guarantees Y) =  
   1.103 +lemma lift_guarantees_eq_lift_inv:
   1.104 +     "(lift i F \<in> X guarantees Y) =  
   1.105        (F \<in> (rename (drop_map i) ` X) guarantees (rename (drop_map i) ` Y))"
   1.106  by (simp add: bij_lift_map [THEN rename_guarantees_eq_rename_inv] lift_def)
   1.107  
   1.108  
   1.109 -(*** We devote an ENORMOUS effort to proving lift_transient_eq_disj, 
   1.110 -     which is used only in TimerArray and perhaps isn't even essential
   1.111 -     there!
   1.112 -***)
   1.113 -
   1.114  (*To preserve snd means that the second component is there just to allow
   1.115    guarantees properties to be stated.  Converse fails, for lift i F can 
   1.116    change function components other than i*)
   1.117 @@ -293,59 +283,9 @@
   1.118  apply (erule constrains_imp_subset [THEN lift_set_mono])
   1.119  done
   1.120  
   1.121 -(** Lemmas for the transient theorem **)
   1.122 -
   1.123 -lemma insert_map_upd_same: "(insert_map i t f)(i := s) = insert_map i s f"
   1.124 -by (rule ext, auto)
   1.125 -
   1.126 -lemma insert_map_upd:
   1.127 -     "(insert_map j t f)(i := s) =  
   1.128 -      (if i=j then insert_map i s f  
   1.129 -       else if i<j then insert_map j t (f(i:=s))  
   1.130 -       else insert_map j t (f(i - Suc 0 := s)))"
   1.131 -apply (rule ext) 
   1.132 -apply (simp split add: nat_diff_split) 
   1.133 - txt{*This simplification is VERY slow*}
   1.134 -done
   1.135 -
   1.136 -lemma insert_map_eq_diff:
   1.137 -     "[| insert_map i s f = insert_map j t g;  i\<noteq>j |]  
   1.138 -      ==> \<exists>g'. insert_map i s' f = insert_map j t g'"
   1.139 -apply (subst insert_map_upd_same [symmetric])
   1.140 -apply (erule ssubst)
   1.141 -apply (simp only: insert_map_upd if_False split: split_if, blast)
   1.142 -done
   1.143 -
   1.144 -lemma lift_map_eq_diff: 
   1.145 -     "[| lift_map i (s,(f,uu)) = lift_map j (t,(g,vv));  i\<noteq>j |]  
   1.146 -      ==> \<exists>g'. lift_map i (s',(f,uu)) = lift_map j (t,(g',vv))"
   1.147 -apply (unfold lift_map_def, auto)
   1.148 -apply (blast dest: insert_map_eq_diff)
   1.149 -done
   1.150 -
   1.151 -lemma lift_transient_eq_disj:
   1.152 -     "F \<in> preserves snd  
   1.153 -      ==> (lift i F \<in> transient (lift_set j (A <*> UNIV))) =  
   1.154 -          (i=j & F \<in> transient (A <*> UNIV) | A={})"
   1.155 -apply (case_tac "i=j")
   1.156 -apply (auto simp add: lift_transient)
   1.157 -apply (auto simp add: lift_set_def lift_def transient_def rename_def 
   1.158 -                      extend_def Domain_extend_act)
   1.159 -apply (drule subsetD, blast, auto)
   1.160 -apply (rename_tac s f uu s' f' uu')
   1.161 -apply (subgoal_tac "f'=f & uu'=uu")
   1.162 - prefer 2 apply (force dest!: preserves_imp_eq, auto)
   1.163 -apply (drule sym)
   1.164 -apply (drule subsetD)
   1.165 -apply (rule ImageI)
   1.166 -apply (erule bij_lift_map [THEN good_map_bij, 
   1.167 -                           THEN Extend.intro, 
   1.168 -                           THEN Extend.mem_extend_act_iff [THEN iffD2]], force)
   1.169 -apply (erule lift_map_eq_diff [THEN exE], auto)
   1.170 -done
   1.171 -
   1.172  (*USELESS??*)
   1.173 -lemma lift_map_image_Times: "lift_map i ` (A <*> UNIV) =  
   1.174 +lemma lift_map_image_Times:
   1.175 +     "lift_map i ` (A <*> UNIV) =  
   1.176        (\<Union>s \<in> A. \<Union>f. {insert_map i s f}) <*> UNIV"
   1.177  apply (auto intro!: bexI image_eqI simp add: lift_map_def)
   1.178  apply (rule split_conv [symmetric])
   1.179 @@ -368,7 +308,7 @@
   1.180  done
   1.181  
   1.182  
   1.183 -(*** Lemmas to handle function composition (o) more consistently ***)
   1.184 +subsection{*Lemmas to Handle Function Composition (o) More Consistently*}
   1.185  
   1.186  (*Lets us prove one version of a theorem and store others*)
   1.187  lemma o_equiv_assoc: "f o g = h ==> f' o f o g = f' o h"
   1.188 @@ -388,15 +328,18 @@
   1.189  done
   1.190  
   1.191  
   1.192 -(*** More lemmas about extend and project 
   1.193 -     They could be moved to {Extend,Project}.ML, but DON'T need the locale ***)
   1.194 +subsection{*More lemmas about extend and project*}
   1.195  
   1.196 -lemma extend_act_extend_act: "extend_act h' (extend_act h act) =  
   1.197 +text{*They could be moved to theory Extend or Project*}
   1.198 +
   1.199 +lemma extend_act_extend_act:
   1.200 +     "extend_act h' (extend_act h act) =  
   1.201        extend_act (%(x,(y,y')). h'(h(x,y),y')) act"
   1.202  apply (auto elim!: rev_bexI simp add: extend_act_def, blast) 
   1.203  done
   1.204  
   1.205 -lemma project_act_project_act: "project_act h (project_act h' act) =  
   1.206 +lemma project_act_project_act:
   1.207 +     "project_act h (project_act h' act) =  
   1.208        project_act (%(x,(y,y')). h'(h(x,y),y')) act"
   1.209  by (auto elim!: rev_bexI simp add: project_act_def)
   1.210  
   1.211 @@ -407,7 +350,7 @@
   1.212  by (simp add: extend_act_def project_act_def, blast)
   1.213  
   1.214  
   1.215 -(*** OK and "lift" ***)
   1.216 +subsection{*OK and "lift"*}
   1.217  
   1.218  lemma act_in_UNION_preserves_fst:
   1.219       "act \<subseteq> {(x,x'). fst x = fst x'} ==> act \<in> UNION (preserves fst) Acts"