Theory EffectMono

(*  Title:      JinjaThreads/BV/EffectMono.thy
    Author:     Gerwin Klein, Andreas Lochbihler
*)

section ‹Monotonicity of eff and app›

theory EffectMono
imports
  Effect
begin

declare not_Err_eq [iff]

declare widens_trans[trans]

lemma app⇩i_mono: 
  assumes wf: "wf_prog p P"
  assumes less: "P ⊢ τ ≤⇩i τ'"
  shows "app⇩i (i,P,mxs,mpc,rT,τ') ⟹ app⇩i (i,P,mxs,mpc,rT,τ)"
proof -
  assume app: "app⇩i (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 "app⇩i (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: "class_type_of' (ST' ! n) = ⌊D⌋"
        and Ts: "P ⊢ rev (take n ST') [≤] Ts"
        and D_M: "P ⊢ D sees M: Ts→T = m in C'"
        by fastforce

      from less have "P ⊢ ST!n ≤ ST'!n"
        by(auto dest: list_all2_nthD2[OF _ n])
      with D obtain D' where D': "class_type_of' (ST ! n) = ⌊D'⌋" 
        and DsubC: "P ⊢ D' ≼⇧* D"
        using ST by(rule widen_is_class_type_of)
      from wf D_M DsubC obtain Ts' T' m' C'' where
        D'_M: "P ⊢ D' sees M: Ts'→T' = m' in C''" and
        Ts': "P ⊢ Ts [≤] Ts'"
        by (blast dest: sees_method_mono)
      from less have "P ⊢ rev (take n ST) [≤] rev (take n ST')" by simp
      also note Ts also note Ts' 
      finally have "P ⊢ rev (take n ST) [≤] Ts'" .
      with D'_M D' app less Invoke D have ?thesis by(auto)
    }
    ultimately show ?thesis by blast
  next 
    case Getfield
    with app less show ?thesis
      by(fastforce simp add: sees_field_def widen_Array dest: has_fields_fun)
  next
    case Putfield
    with app less show ?thesis
      by (fastforce intro: widen_trans rtrancl_trans simp add: sees_field_def widen_Array dest: has_fields_fun)
  next
    case CAS
    with app less show ?thesis
      by (fastforce intro: widen_trans rtrancl_trans simp add: sees_field_def widen_Array dest: has_fields_fun)
  next
    case Return
    with app less show ?thesis by (fastforce intro: widen_trans)
  next
    case ALoad
    with app less show ?thesis by(auto simp add: widen_Array)
  next
    case AStore
    with app less show ?thesis by(auto simp add: widen_Array)
  next
    case ALength
    with app less show ?thesis by(auto simp add: widen_Array)
  next
    case (Checkcast T)
    with app less show ?thesis
      by(auto elim!: refTE simp: widen_Array)
  next
    case (Instanceof T)
    with app less show ?thesis
      by(auto elim!: refTE simp: widen_Array)
  next
    case ThrowExc
    with app less show ?thesis
      by(auto elim!: refTE simp: widen_Array)
  next
    case MEnter
    with app less show ?thesis
      by(auto elim!: refTE simp: widen_Array)
  next
    case MExit
    with app less show ?thesis
      by(auto elim!: refTE simp: widen_Array)
  next
    case (BinOpInstr bop)
    with app less show ?thesis by(force dest: WTrt_binop_widen_mono)
  next
    case Dup
    with app less show ?thesis
      by(auto dest: list_all2_lengthD)
  next
    case Swap
    with app less show ?thesis
      by(auto dest: list_all2_lengthD)
  qed (auto elim!: refTE not_refTE)
qed

lemma succs_mono:
  assumes wf: "wf_prog p P" and app⇩i: "app⇩i (i,P,mxs,mpc,rT,τ')"
  shows "P ⊢ τ ≤⇩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 ⊢ τ ≤⇩i τ'"
  moreover
  with app⇩i Invoke have "n < size ST" by (auto dest: list_all2_lengthD)
  ultimately
  have "P ⊢ ST!n ≤ ST'!n" by (auto simp add: fun_of_def dest: list_all2_nthD)
  with Invoke show ?thesis by auto 
next
  case ALoad
  obtain ST LT ST' LT' where 
    [simp]: "τ = (ST,LT)" and [simp]: "τ' = (ST',LT')" by (cases τ, cases τ') 
  assume "P ⊢ τ ≤⇩i τ'"
  moreover
  with app⇩i ALoad have "1 < size ST" by (auto dest: list_all2_lengthD)
  ultimately
  have "P ⊢ ST!1 ≤ ST'!1" by (auto simp add: fun_of_def dest: list_all2_nthD)
  with ALoad show ?thesis by auto
next 
  case AStore
  obtain ST LT ST' LT' where 
    [simp]: "τ = (ST,LT)" and [simp]: "τ' = (ST',LT')" by (cases τ, cases τ') 
  assume "P ⊢ τ ≤⇩i τ'"
  moreover
  with app⇩i AStore have "2 < size ST" by (auto dest: list_all2_lengthD)
  ultimately
  have "P ⊢ ST!2 ≤ ST'!2" by (auto simp add: fun_of_def dest: list_all2_nthD)
  with AStore show ?thesis by auto
next
  case ALength
  obtain ST LT ST' LT' where 
    [simp]: "τ = (ST,LT)" and [simp]: "τ' = (ST',LT')" by (cases τ, cases τ') 
  assume "P ⊢ τ ≤⇩i τ'"
  moreover
  with app⇩i ALength have "0 < size ST" by (auto dest: list_all2_lengthD)
  ultimately
  have "P ⊢ ST!0 ≤ ST'!0" by (auto simp add: fun_of_def dest: list_all2_nthD)
  with ALength show ?thesis by auto
next
  case MEnter
  obtain ST LT ST' LT' where 
    [simp]: "τ = (ST,LT)" and [simp]: "τ' = (ST',LT')" by (cases τ, cases τ') 
  assume "P ⊢ τ ≤⇩i τ'"
  moreover
  with app⇩i MEnter have "0 < size ST" by (auto dest: list_all2_lengthD)
  ultimately
  have "P ⊢ ST!0 ≤ ST'!0" by (auto simp add: fun_of_def dest: list_all2_nthD)
  with MEnter show ?thesis by auto
next
  case MExit
  obtain ST LT ST' LT' where 
    [simp]: "τ = (ST,LT)" and [simp]: "τ' = (ST',LT')" by (cases τ, cases τ') 
  assume "P ⊢ τ ≤⇩i τ'"
  moreover
  with app⇩i MExit have "0 < size ST" by (auto dest: list_all2_lengthD)
  ultimately
  have "P ⊢ ST!0 ≤ ST'!0" by (auto simp add: fun_of_def dest: list_all2_nthD)
  with MExit show ?thesis by auto
qed auto

lemma app_mono: 
  assumes wf: "wf_prog p P"
  assumes less': "P ⊢ τ ≤' τ'"
  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 ⊢ τ⇩1 ≤⇩i τ⇩2" using less' by simp
  
  assume "app i P m rT pc mpc xt τ'"
  with Some τ⇩2 obtain
    app⇩i: "app⇩i (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 app⇩i have "app⇩i (i, P, pc, m, rT, τ⇩1)" by (rule app⇩i_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 app⇩i 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)
  ultimately
  show ?thesis using Some by (simp add: app_def)
qed

lemma eff⇩i_mono:
  assumes wf: "wf_prog p P"
  assumes less: "P ⊢ τ ≤⇩i τ'"
  assumes app⇩i: "app i P m rT pc mpc xt (Some τ')"
  assumes succs: "succs i τ pc ≠ []"  "succs i τ' pc ≠ []"
  shows "P ⊢ eff⇩i (i,P,τ) ≤⇩i eff⇩i (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 ⊢ (Some τ) ≤' (Some τ')" by simp
  from wf this app⇩i 
  have app: "app i P m rT pc mpc xt (Some τ)" by (rule app_mono)

  from less app app⇩i show ?thesis
  proof (cases i)
    case ThrowExc 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 app⇩i obtain y' where
       y': "i < size LT'" "LT'!i = OK y'" by clarsimp

    from less have "P ⊢ LT [≤⇩⊤] LT'" by simp
    with y y' have "P ⊢ y ≤ y'" by (auto dest: list_all2_nthD)    
    with Load less y y' app app⇩i
    show ?thesis by auto
  next
    case Store with less app app⇩i
    show ?thesis by (auto simp add: list_all2_update_cong) 
  next
    case (Invoke M n) 
    with app⇩i 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)
    
    from ST' app⇩i Invoke obtain D Ts T m C'
      where D: "class_type_of' (ST' ! n) = ⌊D⌋"
      and Ts: "P ⊢ rev (take n ST') [≤] Ts"
      and D_M: "P ⊢ D sees M: Ts→T = m in C'"
      by fastforce

    from less have "P ⊢ ST!n ≤ ST'!n" by(auto dest: list_all2_nthD2[OF _ n])
    with D obtain D' where D': "class_type_of' (ST ! n) = ⌊D'⌋" 
      and DsubC: "P ⊢ D' ≼⇧* D"
      using ST by(rule widen_is_class_type_of)

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

    show ?thesis using Invoke n D D' D_M less D'_M Ts' ‹P ⊢ T' ≤ T›
      by(auto intro: list_all2_dropI)
  next
    case ALoad with less app app⇩i succs
    show ?thesis by(auto split: if_split_asm dest: Array_Array_widen)
  next
    case AStore with less app app⇩i succs
    show ?thesis by(auto split: if_split_asm dest: Array_Array_widen)
  next
    case (BinOpInstr bop)
    with less app app⇩i succs show ?thesis
      by auto(force dest: WTrt_binop_widen_mono WTrt_binop_fun)
  qed auto
qed

end