Theory EffectMono

Up to index of Isabelle/HOL/arrays

(*  Title:      HOL/MicroJava/BV/EffMono.thy
    ID:         $Id: EffectMono.html,v 1.1 2002/11/28 16:11:18 kleing Exp $
    Author:     Gerwin Klein
    Copyright   2000 Technische Universitaet Muenchen
*)

header {* \isaheader{Monotonicity of eff and app} *}

theory EffectMono = Effect:

lemmas eff_defs [simp del] 


lemma in_address_types_finite:
  "x \<subseteq> address_types G mxs mxr mpc \<Longrightarrow> finite x"
  apply (drule finite_subset)
  apply (rule finite_address_types)
  apply assumption
  done

lemma set_SOME_lists:
  "finite s \<Longrightarrow> set (SOME l. set l = s) = s"  
  apply (erule finite_induct)
  apply simp
  apply (rule_tac a="x#(SOME l. set l = F)" in someI2)
  apply auto
  done

lemma succs_mono:
  assumes s: "s \<subseteq> s'"
  assumes finite: "finite s'" 
  shows "set (succs i pc s) \<subseteq> set (succs i pc s')"
proof (cases i)
  case (Ret pc)
  from finite have "finite (theRA pc ` s')" by (rule finite_imageI)
  moreover
  from s finite have "finite s" by (rule finite_subset)
  hence "finite (theRA pc ` s)" by (rule finite_imageI)
  ultimately  
  show ?thesis using s Ret by (auto simp add: set_SOME_lists)  
qed auto


lemma succs_eff_mono:
  "\<lbrakk>s \<subseteq> s';  finite s'; \<forall>(pc', s')\<in>set (eff i G pc et s'). pc' < mpc \<rbrakk> \<Longrightarrow> 
  \<forall>(pc', s')\<in>set (eff i G pc et s). pc' < mpc"
  apply (unfold eff_def xcpt_eff_def)
  apply auto
  apply (drule bspec)
   apply simp
   apply (rule disjI1)
   apply (rule imageI)
   apply (erule subsetD [OF succs_mono])
    apply assumption
   apply assumption
  apply simp
  done


lemma app_mono: 
"\<lbrakk>s \<subseteq> s'; finite s'; app i G C pc m mpc rT ini et s'\<rbrakk> \<Longrightarrow> app i G C pc m mpc rT ini et s"
  apply (unfold app_def)
  apply clarsimp
  apply (rule conjI)
   prefer 2
   apply (rule succs_eff_mono, assumption+)   
  apply auto
  apply (drule_tac x="((a,b),True)" in bspec)
  apply auto
  done

end

lemmas

  eff i G pc et at ==
  map (%pc'. (pc', norm_eff i G pc pc' at)) (succs i pc at) @
  xcpt_eff i G pc at et

  norm_eff i G pc pc' at ==
  eff_bool i G pc `
  (if EX idx. i = Ret idx then {s. s : at & pc' = theRA (theIdx i) s} else at)

  eff_bool i G pc ==
  %((ST, LT), z).
     (eff' (i, G, pc, ST, LT),
      if EX C p D. i = Invoke_special C init p & ST ! length p = PartInit D
      then True else z)

  xcpt_eff i G pc at et ==
  map (%C. (the (match_exception_table G C pc et),
            (%s. (([Init (Class C)], snd (fst s)), snd s)) ` at))
   (xcpt_names (i, G, pc, et))

lemma in_address_types_finite:

  x <= address_types G mxs mxr mpc ==> finite x

lemma set_SOME_lists:

  finite s ==> set (SOME l. set l = s) = s

lemma

  [| s <= s'; finite s' |] ==> set (succs i pc s) <= set (succs i pc s')

lemma succs_eff_mono:

  [| s <= s'; finite s'; ALL (pc', s'):set (eff i G pc et s'). pc' < mpc |]
  ==> ALL (pc', s'):set (eff i G pc et s). pc' < mpc

lemma app_mono:

  [| s <= s'; finite s'; app i G C pc m mpc rT ini et s' |]
  ==> app i G C pc m mpc rT ini et s