Theory EffectMono

(*  Title:      HOL/MicroJava/BV/EffMono.thy
    ID:         $Id: EffectMono.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     Gerwin Klein
    Copyright   2000 Technische Universitaet Muenchen
*)

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

theory EffectMono = Effect:

declare not_Err_eq [iff]

lemma appi_mono: 
  assumes wf: "wf_prog p P"
  assumes less: "P \<turnstile> τ ≤i τ'"
  shows "appi (i,P,mxs,mpc,rT,τ') ==> appi (i,P,mxs,mpc,rT,τ)"
(*<*)
proof -
  assume app: "appi (i,P,mxs,mpc,rT,τ')"
  
  obtain ST LT ST' LT' where
    [simp]: "τ = (ST,LT)" and
    [simp]: "τ' = (ST',LT')" 
    by (cases τ, cases τ')

  from less have [simp]: "size ST = size ST'" and [simp]: "size LT = size LT'"
    by (auto dest: list_all2_lengthD)

  note [iff] = list_all2_Cons2 widen_Class  
  note [simp] = fun_of_def 

  from app less show "appi (i,P,mxs,mpc,rT,τ)"
  proof (cases i)
    case Load
    with app less show ?thesis by (auto dest!: list_all2_nthD)
  next
    case (Invoke M n)
    with app have n: "n < size ST'" by simp
    
    { assume "ST!n = NT" hence ?thesis using n app Invoke by simp }
    moreover {
      assume "ST'!n = NT"
      moreover with n less have "ST!n = NT" 
        by (auto dest: list_all2_nthD)
      ultimately have ?thesis using n app Invoke by simp
    }
    moreover {
      assume ST: "ST!n ≠ NT" and ST': "ST'!n ≠ NT" 

      from ST' app Invoke obtain D Ts T m C' where
        D:   "ST' ! n = Class D" and
        Ts:  "P \<turnstile> rev (take n ST') [≤] Ts" and
        D_M: "P \<turnstile> D sees M: Ts->T = m in C'"
        by auto

      from n D less have "P \<turnstile> ST!n ≤ ST'!n" 
        by (fastsimp dest: list_all2_nthD2)
      with D ST obtain D' where
        D': "ST!n = Class D'" and DsubC: "P \<turnstile> D' \<preceq>* D" by auto

      from wf D_M DsubC obtain Ts' T' m' C'' where
        D'_M: "P \<turnstile> D' sees M: Ts'->T' = m' in C''" and
        Ts': "P \<turnstile> Ts [≤] Ts'"
        by (blast dest: sees_method_mono) 

      from less have "P \<turnstile> rev (take n ST) [≤] rev (take n ST')" by simp
      also note Ts also note Ts' 
      finally have "P \<turnstile> rev (take n ST) [≤] Ts'" .
      with D'_M D' app less Invoke have ?thesis by fastsimp
    }
    ultimately show ?thesis by blast
  next 
    case Getfield
    with app less show ?thesis by (fastsimp intro: rtrancl_trans)
  next
    case (Putfield F C)
    with app less show ?thesis by (fastsimp intro: widen_trans rtrancl_trans)
  next
    case Return
    with app less show ?thesis by (fastsimp intro: widen_trans)
  qed (auto elim!: refTE not_refTE)
qed
(*>*)

lemma succs_mono:
  assumes wf: "wf_prog p P" and appi: "appi (i,P,mxs,mpc,rT,τ')"
  shows "P \<turnstile> τ ≤i τ' ==> set (succs i τ pc) ⊆ set (succs i τ' pc)"
(*<*)
proof (cases i)
  case (Invoke M n)
  obtain ST LT ST' LT' where 
    [simp]: "τ = (ST,LT)" and [simp]: "τ' = (ST',LT')" by (cases τ, cases τ') 
  assume "P \<turnstile> τ ≤i τ'"
  moreover
  with appi Invoke have "n < size ST" by (auto dest: list_all2_lengthD)
  ultimately
  have "P \<turnstile> ST!n ≤ ST'!n" by (auto simp add: fun_of_def dest: list_all2_nthD)
  with Invoke show ?thesis by auto 
qed auto
(*>*)
  

lemma app_mono: 
  assumes wf: "wf_prog p P"
  assumes less': "P \<turnstile> τ ≤' τ'"
  shows "app i P m rT pc mpc xt τ' ==> app i P m rT pc mpc xt τ"
(*<*)
proof (cases τ)
  case None thus ?thesis by simp
next
  case (Some τ1) 
  moreover
  with less' obtain τ2 where τ2: "τ' = Some τ2" by (cases τ') auto
  ultimately have less: "P \<turnstile> τ1 ≤i τ2" using less' by simp
  
  assume "app i P m rT pc mpc xt τ'"
  with Some τ2 obtain
    appi: "appi (i, P, pc, m, rT, τ2)" and
    xcpt: "xcpt_app i P pc m xt τ2" and
    succs: "∀(pc',s')∈set (eff i P pc xt (Some τ2)). pc' < mpc"
    by (auto simp add: app_def)
  
  from wf less appi have "appi (i, P, pc, m, rT, τ1)" by (rule appi_mono)
  moreover
  from less have "size (fst τ1) = size (fst τ2)" 
    by (cases τ1, cases τ2) (auto dest: list_all2_lengthD)
  with xcpt have "xcpt_app i P pc m xt τ1" by (simp add: xcpt_app_def)
  moreover
  from wf appi less have "∀pc. set (succs i τ1 pc) ⊆ set (succs i τ2 pc)"
    by (blast dest: succs_mono)
  with succs
  have "∀(pc',s')∈set (eff i P pc xt (Some τ1)). pc' < mpc"
    by (cases τ1, cases τ2)
       (auto simp add: eff_def norm_eff_def xcpt_eff_def dest: bspec, blast)
  ultimately
  show ?thesis using Some by (simp add: app_def)
qed
(*>*)


lemma effi_mono:
  assumes wf: "wf_prog p P"
  assumes less: "P \<turnstile> τ ≤i τ'"
  assumes appi: "app i P m rT pc mpc xt (Some τ')"
  assumes succs: "succs i τ pc ≠ []"  "succs i τ' pc ≠ []"
  shows "P \<turnstile> effi (i,P,τ) ≤i effi (i,P,τ')"
(*<*)
proof -
  obtain ST LT ST' LT' where
    [simp]: "τ = (ST,LT)" and
    [simp]: "τ' = (ST',LT')" 
    by (cases τ, cases τ')
  
  note [simp] = eff_def app_def fun_of_def 

  from less have "P \<turnstile> (Some τ) ≤' (Some τ')" by simp
  from wf this appi 
  have app: "app i P m rT pc mpc xt (Some τ)" by (rule app_mono)

  from less app appi show ?thesis
  proof (cases i)
    case Throw with succs have False by simp
    thus ?thesis ..
  next
    case Return with succs have False by simp
    thus ?thesis ..
  next
    case (Load i)
    from Load app obtain y where
       y:  "i < size LT" "LT!i = OK y" by clarsimp
    from Load appi obtain y' where
       y': "i < size LT'" "LT'!i = OK y'" by clarsimp

    from less have "P \<turnstile> LT [≤\<top>] LT'" by simp
    with y y' have "P \<turnstile> y ≤ y'" by (auto dest: list_all2_nthD)    
    with Load less y y' app appi
    show ?thesis by auto
  next
    case Store with less app appi
    show ?thesis by (auto simp add: list_all2_update_cong) 
  next
    case (Invoke M n) 
    with appi have n: "n < size ST'" by simp
    from less have [simp]: "size ST = size ST'" 
      by (auto dest: list_all2_lengthD)

    from Invoke succs have ST: "ST!n ≠ NT" and ST': "ST'!n ≠ NT"
      by (auto split: split_if_asm)
    
    from ST' appi Invoke obtain D Ts T m C' where
      D:   "ST' ! n = Class D" and
      D_M: "P \<turnstile> D sees M: Ts->T = m in C'"
      by auto

    from n D less have "P \<turnstile> ST!n ≤ ST'!n" 
      by (fastsimp dest: list_all2_nthD2)
    with D ST obtain D' where
      D': "ST ! n = Class D'" and DsubC: "P \<turnstile> D' \<preceq>* D"
      by (auto simp: widen_Class)
      
    from wf D_M DsubC obtain Ts' T' m' C'' where
      D'_M: "P \<turnstile> D' sees M: Ts'->T' = m' in C''" and
      Ts': "P \<turnstile> T' ≤ T"
      by (blast dest: sees_method_mono) 

    with Invoke n D D' D_M less 
    show ?thesis by (auto intro: list_all2_dropI)
  qed auto
qed
(*>*)

end