PIPBasics.thy
changeset 141 f70344294e99
parent 140 389ef8b1959c
child 142 10c16b85a839
equal deleted inserted replaced
140:389ef8b1959c 141:f70344294e99
    31 next
    31 next
    32   show "g ` A \<subseteq> f ` A"
    32   show "g ` A \<subseteq> f ` A"
    33    by (rule image_subsetI, auto intro:h[symmetric])
    33    by (rule image_subsetI, auto intro:h[symmetric])
    34 qed
    34 qed
    35 
    35 
    36 lemma Max_fg_mono:
    36 
    37   assumes "finite A"
       
    38   and "\<forall> a \<in> A. f a \<le> g a"
       
    39   shows "Max (f ` A) \<le> Max (g ` A)"
       
    40 proof(cases "A = {}")
       
    41   case True
       
    42   thus ?thesis by auto
       
    43 next
       
    44   case False
       
    45   show ?thesis
       
    46   proof(rule Max.boundedI)
       
    47     from assms show "finite (f ` A)" by auto
       
    48   next
       
    49     from False show "f ` A \<noteq> {}" by auto
       
    50   next
       
    51     fix fa
       
    52     assume "fa \<in> f ` A"
       
    53     then obtain a where h_fa: "a \<in> A" "fa = f a" by auto
       
    54     show "fa \<le> Max (g ` A)"
       
    55     proof(rule Max_ge_iff[THEN iffD2])
       
    56       from assms show "finite (g ` A)" by auto
       
    57     next
       
    58       from False show "g ` A \<noteq> {}" by auto
       
    59     next
       
    60       from h_fa have "g a \<in> g ` A" by auto
       
    61       moreover have "fa \<le> g a" using h_fa assms(2) by auto
       
    62       ultimately show "\<exists>a\<in>g ` A. fa \<le> a" by auto
       
    63     qed
       
    64   qed
       
    65 qed 
       
    66 
       
    67 lemma Max_f_mono:
       
    68   assumes seq: "A \<subseteq> B"
       
    69   and np: "A \<noteq> {}"
       
    70   and fnt: "finite B"
       
    71   shows "Max (f ` A) \<le> Max (f ` B)"
       
    72 proof(rule Max_mono)
       
    73   from seq show "f ` A \<subseteq> f ` B" by auto
       
    74 next
       
    75   from np show "f ` A \<noteq> {}" by auto
       
    76 next
       
    77   from fnt and seq show "finite (f ` B)" by auto
       
    78 qed
       
    79 
       
    80 lemma Max_UNION: 
       
    81   assumes "finite A"
       
    82   and "A \<noteq> {}"
       
    83   and "\<forall> M \<in> f ` A. finite M"
       
    84   and "\<forall> M \<in> f ` A. M \<noteq> {}"
       
    85   shows "Max (\<Union>x\<in> A. f x) = Max (Max ` f ` A)" (is "?L = ?R")
       
    86   using assms[simp]
       
    87 proof -
       
    88   have "?L = Max (\<Union>(f ` A))"
       
    89     by (fold Union_image_eq, simp)
       
    90   also have "... = ?R"
       
    91     by (subst Max_Union, simp+)
       
    92   finally show ?thesis .
       
    93 qed
       
    94 
       
    95 lemma max_Max_eq:
       
    96   assumes "finite A"
       
    97     and "A \<noteq> {}"
       
    98     and "x = y"
       
    99   shows "max x (Max A) = Max ({y} \<union> A)" (is "?L = ?R")
       
   100 proof -
       
   101   have "?R = Max (insert y A)" by simp
       
   102   also from assms have "... = ?L"
       
   103       by (subst Max.insert, simp+)
       
   104   finally show ?thesis by simp
       
   105 qed
       
   106 
    37 
   107 section {* Lemmas do not depend on trace validity *}
    38 section {* Lemmas do not depend on trace validity *}
   108 
    39 
   109 text {* The following lemma serves to proof @{text "preced_tm_lt"} *}
    40 text {* The following lemma serves to proof @{text "preced_tm_lt"} *}
   110 
    41 
  3819   the maximum precedence of its own subtree, by applying 
  3750   the maximum precedence of its own subtree, by applying 
  3820   the absorbing property of @{term Max} (lemma @{thm Max_UNION}) 
  3751   the absorbing property of @{term Max} (lemma @{thm Max_UNION}) 
  3821   over the union of subtrees, the following equation can be derived:
  3752   over the union of subtrees, the following equation can be derived:
  3822 *}
  3753 *}
  3823 
  3754 
  3824 thm the_preced_def cpreceds_def
  3755 
       
  3756 lemma cp_alt_def3:
       
  3757   shows "cp s th = Max (preceds (subtree (tG s) th) s)"
       
  3758 unfolding cp_alt_def2
       
  3759 unfolding image_def
       
  3760 unfolding the_preced_def
       
  3761 by meson
       
  3762 
       
  3763 lemma KK:
       
  3764   shows "(\<Union>x\<in>C. B x) = (\<Union> {B x |x. x \<in> C})"
       
  3765 (*  and "\<Union>" *)
       
  3766 by (simp_all add: Setcompr_eq_image)
       
  3767 
       
  3768 lemma Max_Segments: 
       
  3769   assumes "finite C" "\<forall>x\<in> C. finite (B x)" "\<forall>x\<in> C. B x \<noteq> {}" "{B x |x. x \<in> C} \<noteq> {}" 
       
  3770   shows "Max (\<Union>x \<in> C. B x) = Max {Max (B x) | x. x \<in> C}"
       
  3771 using assms
       
  3772 apply(subst KK(1))
       
  3773 apply(subst Max_Union)
       
  3774 apply(auto)[3]
       
  3775 apply(simp add: Setcompr_eq_image)
       
  3776 apply(simp add: image_eq_UN)
       
  3777 done 
  3825 
  3778 
  3826 lemma max_cp_readys_max_preced_tG:
  3779 lemma max_cp_readys_max_preced_tG:
  3827   shows "Max (cp s ` readys s) = Max (the_preced s ` threads s)" (is "?L = ?R")
  3780   shows "Max (cp s ` readys s) = Max (preceds (threads s) s)" (is "?L = ?R")
  3828 proof(cases "readys s = {}")
  3781 proof(cases "readys s = {}")
  3829   case False
  3782   case False
  3830   have "?R = 
  3783   have "Max (preceds (threads s) s) = Max (preceds (\<Union>th\<in>readys s. subtree (tG s) th) s)"
  3831     Max (the_preced s ` (\<Union>th\<in>readys s. subtree (tG s) th))"
  3784     unfolding threads_alt_def1 by simp
  3832     by (simp add: threads_alt_def1)  
  3785   also have "... = Max {Max (preceds (subtree (tG s) th) s) | th. th \<in> readys s}"
  3833   also have "... = Max (\<Union>x\<in>readys s. the_preced s ` subtree (tG s) x) "
  3786     apply(subst Max_Segments[symmetric])
  3834     by (unfold image_UN, simp)
  3787     prefer 5  
  3835   also have "... = Max (Max ` (\<lambda>x. the_preced s ` subtree (tG s) x) ` readys s)" 
  3788     apply(rule arg_cong)
  3836   proof(rule Max_UNION)
  3789     back
  3837     show "\<forall>M\<in>(\<lambda>x. the_preced s ` subtree (tG s) x) ` readys s. finite M"
  3790     apply(blast)
  3838       using fsbttGs.finite_subtree by auto
  3791     apply (simp add: finite_readys)
  3839   qed (auto simp:False subtree_def finite_readys)
  3792     apply (simp add: fsbttGs.finite_subtree)
  3840   also have "... = Max ((Max \<circ> (\<lambda>x. the_preced s ` subtree (tG s) x)) ` readys s)"
  3793     apply blast
  3841     by (simp add: image_comp)
  3794     using False by blast
  3842   also have "... = ?L" (is "Max (?f ` ?A) = Max (?g ` ?A)")
  3795   also have "... = Max {cp s th | th. th \<in> readys s}"
  3843   proof -
  3796     unfolding cp_alt_def3 ..
  3844     have "(?f ` ?A) = (?g ` ?A)"
  3797   finally show "Max (cp s ` readys s) = Max (preceds (threads s) s)"
  3845     proof(rule f_image_eq)
  3798    by (simp add: Setcompr_eq_image image_def) 
  3846       fix th1 
       
  3847       assume "th1 \<in> ?A"
       
  3848       thus "?f th1 = ?g th1"
       
  3849         by (unfold cp_alt_def2, simp)
       
  3850     qed
       
  3851     thus ?thesis by simp
       
  3852   qed
       
  3853   finally show ?thesis by simp
       
  3854 qed (auto simp:threads_alt_def)
  3799 qed (auto simp:threads_alt_def)
       
  3800 
       
  3801 
       
  3802 lemma LL:
       
  3803 shows "the_preced s ` threads s = preceds (threads s) s"
       
  3804 using the_preced_def by auto
  3855 
  3805 
  3856 
  3806 
  3857 text {*
  3807 text {*
  3858   The following lemma is simply a corollary of @{thm max_cp_readys_max_preced_tG}
  3808   The following lemma is simply a corollary of @{thm max_cp_readys_max_preced_tG}
  3859   and @{thm max_cp_eq}:
  3809   and @{thm max_cp_eq}:
  3860 *}
  3810 *}
  3861 lemma max_cp_readys_threads:
  3811 lemma max_cp_readys_threads:
  3862   shows "Max (cp s ` readys s) = Max (cp s ` threads s)" 
  3812   shows "Max (cp s ` readys s) = Max (cp s ` threads s)" 
  3863     using max_cp_readys_max_preced_tG max_cp_eq by auto
  3813     apply(simp add: max_cp_readys_max_preced_tG)
       
  3814     apply(simp add: max_cp_eq)
       
  3815     apply(simp add: LL)
       
  3816     done
  3864 
  3817 
  3865 end
  3818 end
  3866 
  3819 
  3867 
  3820 
  3868 section {* Relating @{term cntP}, @{term cntV}, @{term cntCS} and @{term pvD} *}
  3821 section {* Relating @{term cntP}, @{term cntV}, @{term cntCS} and @{term pvD} *}