(*******************************************************************************
 * LJAM: Isabelle/HOL proof of well-formedness preservation                    *
 * Copyright (c) 2007-2009, Rok Strnisa                                        *
 * All rights reserved.                                                        *
 *                                                                             *
 * Redistribution and use in source and binary forms, with or without          *
 * modification, are permitted provided that the following conditions are met: *
 *                                                                             *
 *   - Redistributions of source code must retain the above copyright notice,  *
 *     this list of conditions and the following disclaimer.                   *
 *                                                                             *
 *   - Redistributions in binary form must reproduce the above copyright       *
 *     notice, this list of conditions and the following disclaimer in the     *
 *     documentation and/or other materials provided with the distribution.    *
 *                                                                             *
 *   - Neither the name of the Computer Laboratory, University of Cambridge    *
 *     nor the names of its contributors may be used to endorse or promote     *
 *     products derived from this software without specific prior written      *
 *     permission.                                                             *
 *                                                                             *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" *
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE   *
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE  *
 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE    *
 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR         *
 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF        *
 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS    *
 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN     *
 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)     *
 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE  *
 * POSSIBILITY OF SUCH DAMAGE.                                                 *
 *******************************************************************************)

theory iJAM_proof imports iJAM_eq Infinite_Set begin

lemmas wf_intros = wf_object_wf_varstate_wf_heap_wf_config_wf_stmt_wf_meth_wf_class_common_wf_class_wf_md_wf_rmis_wf_r_wf_rc_wf_mh_wf_p.intros [simplified]
lemmas wf_induct = wf_object_wf_varstate_wf_heap_wf_config_wf_stmt_wf_meth_wf_class_common_wf_class_wf_md_wf_rmis_wf_r_wf_rc_wf_mh_wf_p.induct [simplified]
lemmas wf_config_normalI = wf_object_wf_varstate_wf_heap_wf_config_wf_stmt_wf_meth_wf_class_common_wf_class_wf_md_wf_rmis_wf_r_wf_rc_wf_mh_wf_p.wf_allI [simplified]
lemmas wf_objectE   = wf_object.cases[simplified]
lemmas wf_varstateE = wf_varstate.cases[simplified]
lemmas wf_heapE     = wf_heap.cases[simplified]
lemmas wf_configE   = wf_config.cases[simplified]
lemmas wf_stmtE     = wf_stmt.cases[simplified]
lemmas wf_methE     = wf_meth.cases[simplified]
lemmas wf_class_cE  = wf_class_common.cases[simplified]
lemmas wf_classE    = wf_class.cases[simplified]
lemmas wf_mdE       = wf_md.cases[simplified]
lemmas wf_rmisE     = wf_rmis.cases[simplified]
lemmas wf_rE        = wf_r.cases[simplified]
lemmas wf_rcE       = wf_rc.cases[simplified]
lemmas wf_mhE       = wf_mh.cases[simplified]
lemmas wf_programE  = wf_p.cases[simplified]

lemma wf_subvarstateI:
  "\<lbrakk>(P, G, H, L) \<in> wf_varstate; G x' = Some ty;
    (P, H, Some v, Some ty) \<in> wf_object\<rbrakk>
        \<Longrightarrow> (P, G, H, L (x' \<mapsto> v)) \<in> wf_varstate"
apply(erule wf_varstateE) apply(rule wf_varstateI) apply(simp) apply(clarsimp)
done

lemma finite_super_varstate:
  "finite (dom ((L ++ map_of (map (\<lambda>(y, cl, var, var', y). (x_var var', y)) y_cl_var_var'_v_list))(x' \<mapsto> v_oid oid))) = finite (dom L)"
apply(induct y_cl_var_var'_v_list)
 apply(clarsimp) apply(simp add: dom_def)
 apply(subgoal_tac "{a. a \<noteq> x' \<longrightarrow> (\<exists>y. L a = Some y)} = {a. a = x' \<or> (\<exists>y. L a = Some y)}")
 apply(simp add: Collect_disj_eq) apply(force)
apply(clarsimp simp add: map_add_def dom_def split: split_if_asm)
apply(subgoal_tac "{aa. aa \<noteq> x_var a \<longrightarrow> aa \<noteq> x' \<longrightarrow> (\<exists>y. option_case (L aa) Some (map_of (map (\<lambda>(y, cl, var, var', y). (x_var var', y)) y_cl_var_var'_v_list) aa) = Some y)} =
                   {aa. aa = x_var a \<or> (aa = x' \<or> (\<exists>y. option_case (L aa) Some (map_of (map (\<lambda>(y, cl, var, var', y). (x_var var', y)) y_cl_var_var'_v_list) aa) = Some y))}")
apply(simp add: Collect_disj_eq) apply(force)
done

lemma fst_map_elem:
  "(y_k, ty_k, var_k, var'_k, v_k) \<in> set y_ty_var_var'_v_list \<Longrightarrow>
      x_var var'_k \<in> fst ` (\<lambda>(y, ty, var, var', v). (x_var var', ty)) ` set y_ty_var_var'_v_list"
by (force)

lemma map_add_x_var[THEN mp]:
  "var' \<in> set (map (\<lambda>(y, cl, var, var', v). var) y_cl_var_var'_v_list) \<longrightarrow>
   x_var var' \<in> set (map (\<lambda>(y, cl, var, var', v). x_var var) y_cl_var_var'_v_list)"
by (induct y_cl_var_var'_v_list, auto)

lemma map_of_map_and_x[simp]:
  "\<lbrakk>G x = Some ty_x; L x' = None; \<forall>x\<in>set y_cl_var_var'_v_list. (\<lambda>(y, cl, var, var', v). L (x_var var') = None) x;
    \<forall>x\<in>Map.dom G. (Pa, H, L x, G x) \<in> wf_object\<rbrakk> \<Longrightarrow>
      (if x = x' then Some ty
       else (G ++ map_of (map (\<lambda>((y, cl, var, var', v), y', ty). (x_var var', ty)) (zip y_cl_var_var'_v_list y_ty_list))) x) =
          Some ty_x"
apply(subgoal_tac "x \<noteq> x'") apply(subgoal_tac "\<forall>(y, cl, var, var', v) \<in> set y_cl_var_var'_v_list. x_var var' \<noteq> x")
  apply(case_tac "map_of (map (\<lambda>((y, cl, var, var', v), y', ty). (x_var var', ty)) (zip y_cl_var_var'_v_list y_ty_list)) x")
   apply(clarsimp simp add: map_add_def)
  apply(clarsimp) apply(drule map_of_is_SomeD) apply(clarsimp) apply(rename_tac y cl var var' v y' ty)
  apply(drule_tac x = "(y, cl, var, var', v)" in bspec) apply(force simp add: set_zip)
  apply(drule_tac x = "x_var var'" in bspec, simp add: domI) apply(erule wf_objectE, simp+)
 apply(force elim: wf_objectE)+
done

lemma wf_stmt_in_G':
   "(L x' = None \<and> (\<forall>x\<in>set y_cl_var_var'_v_list. (\<lambda>(y, cl, var, var', v). L (x_var var') = None) x)
    \<and> (\<forall>x\<in>dom G. (P, H, L x, G x) \<in> wf_object) \<and> (P, G, s) \<in> wf_stmt \<longrightarrow>
       (P, (G ++ map_of (map (\<lambda>((y, cl, var, var', v), y', y). (x_var var', y)) (zip y_cl_var_var'_v_list y_ty_list)))(x' \<mapsto> ty), s) \<in> wf_stmt) \<and>
    (L x' = None \<and> (\<forall>x\<in>set y_cl_var_var'_v_list. (\<lambda>(y, cl, var, var', v). L (x_var var') = None) x)
    \<and> (\<forall>x\<in>dom G. (P, H, L x, G x) \<in> wf_object) \<and> (\<forall>s\<in>set ss. (P, G, s) \<in> wf_stmt) \<longrightarrow>
       (\<forall>s\<in>set ss. (P, (G ++ map_of (map (\<lambda>((y, cl, var, var', v), y', y). (x_var var', y)) (zip y_cl_var_var'_v_list y_ty_list)))(x' \<mapsto> ty), s) \<in> wf_stmt))"
apply(rule s.induct)

apply(clarsimp, erule wf_stmtE, simp_all, simp add: wf_blockI)

apply(clarify, erule wf_stmtE, simp_all)
apply(erule sty_option.cases, force intro: wf_var_assignI sty_optionI)

apply(clarify, erule wf_stmtE, simp_all)
apply(erule sty_option.cases, force intro: wf_field_readI sty_optionI)

apply(clarify, erule wf_stmtE, simp_all)
apply(erule sty_option.cases, force intro: wf_field_writeI sty_optionI)

apply(clarify, erule wf_stmtE, simp_all)
apply(clarsimp)
apply(rule wf_ifI)
  apply(erule disjE)
   apply(rule disjI1, erule sty_option.cases, force intro: sty_optionI)
  apply(rule disjI2, erule sty_option.cases, force intro: sty_optionI)
 apply(assumption+)

apply(clarify, erule wf_stmtE, simp_all)
apply(erule sty_option.cases, force intro: wf_newI sty_optionI)

apply(clarify, erule wf_stmtE, simp_all)
apply(rule wf_mcallI, simp, simp, simp)
 apply(clarsimp split del: split_if) apply(rename_tac y_k ty_k)
 apply(drule_tac x = "(y_k, ty_k)" in bspec, simp, clarify)
 apply(erule_tac ?a3.0 = "Some ty_k" in sty_option.cases)
 apply(force intro: sty_optionI)
apply(clarify)
apply(erule sty_option.cases)
apply(rule sty_optionI, simp+)

done

lemma map_three_in_four:
  "var_k \<in> set (map (\<lambda>(y, cl, var, u). var) y_cl_var_var'_v_list)
   \<longrightarrow> (\<exists>y cl u. (y, cl, var_k, u) \<in> set y_cl_var_var'_v_list)"
by (induct y_cl_var_var'_v_list, auto)

lemma map_var:
  "\<lbrakk>(cl_k, var_k, ty_k) \<in> set cl_var_ty_list;
    map (\<lambda>(y, cl, var, u). var) y_cl_var_var'_v_list = map (\<lambda>(cl, var, ty). var) cl_var_ty_list\<rbrakk>
      \<Longrightarrow> \<exists>y_k cl'_k u_k. (y_k, cl'_k, var_k, u_k) \<in> set y_cl_var_var'_v_list"
apply(subgoal_tac "var_k \<in> set (map (\<lambda>(y, cl, var, u). var) y_cl_var_var'_v_list)")
by (force simp add: map_three_in_four)+

lemma length_one_in_two:
  "length y_ty_list = length (map fst y_ty_list)"
by (induct y_ty_list, auto)

lemma length_two_in_two:
  "length y_ty_list = length (map snd y_ty_list)"
by (induct y_ty_list, auto)

lemma length_two_in_three:
  "length cl_var_ty_list = length (map (\<lambda>(cl, var, ty). var) cl_var_ty_list)"
by (induct cl_var_ty_list, auto)

lemma length_three_in_three:
  "length cl_var_ty_list = length (map (\<lambda>(cl, var, ty). ty) cl_var_ty_list)"
by (induct cl_var_ty_list, auto)

lemma length_three_in_four:
  "length y_cl_var_var'_v_list = length (map (\<lambda>(y, cl, var, u). var) y_cl_var_var'_v_list)"
by (induct y_cl_var_var'_v_list, auto)

lemma length_one_in_five:
  "length y_cl_var_var'_v_list = length (map (\<lambda>(y, cl, var, var', v). y) y_cl_var_var'_v_list)"
by (induct y_cl_var_var'_v_list, auto)

lemma length_three_in_five:
  "length y_cl_var_var'_v_list = length (map (\<lambda>(y, cl, var, var', v). var) y_cl_var_var'_v_list)"
by (induct y_cl_var_var'_v_list, auto)

lemma map_length_list:
  "length (map (\<lambda>((y, y'), yy, ty). (y', ty)) list) = length list"
by (induct list, auto)

lemma map_length_y:
  "map (\<lambda>(y, cl, var, var', v). y) y_cl_var_var'_v_list = map fst y_ty_list \<Longrightarrow>
   length y_cl_var_var'_v_list = length y_ty_list"
by (simp only: length_one_in_five length_one_in_two)

lemma map_length_y':
  "map fst y_y'_list = map fst y_ty_list \<Longrightarrow> length y_y'_list = length y_ty_list"
by (simp only: length_one_in_two length_two_in_two)

lemma map_length_var:
  "map (\<lambda>(y, cl, var, var', v). var) y_cl_var_var'_v_list = map (\<lambda>(cl, var, ty). var) cl_var_ty_list \<Longrightarrow>
   length y_cl_var_var'_v_list = length cl_var_ty_list"
by (simp only: length_three_in_five length_two_in_three)

lemma map_length_ty:
  "map (\<lambda>(cl, var, ty). ty) cl_var_ty_list = map snd y_ty_list \<Longrightarrow>
   length cl_var_ty_list = length y_ty_list"
by (simp only: length_three_in_three length_two_in_two)

lemma map_length_var_ty:
  "\<lbrakk>map (\<lambda>(y, cl, var, u). var) y_cl_var_var'_v_list = map (\<lambda>(cl, var, ty). var) cl_var_ty_list;
    map (\<lambda>(cl, var, ty). ty) cl_var_ty_list = map snd y_ty_list\<rbrakk> \<Longrightarrow>
   length y_cl_var_var'_v_list = length y_ty_list"
apply(rule_tac s = "length cl_var_ty_list" in trans)
apply (simp only: length_three_in_four length_two_in_three)
apply(simp only: length_three_in_three length_two_in_two)
done

lemma fun_eq_fst:
  "(fst \<circ> (\<lambda>((y, cl, var, var', v), y', y). (x_var var', y))) = (\<lambda>((y, cl, var, var', v), y', y). (x_var var'))"
by (simp add: expand_fun_eq)

lemma fst_zip_eq:
  "length y_cl_var_var'_v_list = length y_ty_list \<Longrightarrow>
   (map fst (map (\<lambda>((y, cl, var, var', v), y', y). (x_var var', y)) (zip y_cl_var_var'_v_list y_ty_list))) =
   (map (\<lambda>(y, cl, var, var', v). x_var var') y_cl_var_var'_v_list)"
apply(simp add: map_compose[THEN sym])
apply(simp add: fun_eq_fst)
apply(rule nth_equalityI)
 apply(force)
apply(clarsimp)
apply(frule nth_mem)
apply(subgoal_tac "\<exists>x. (y_cl_var_var'_v_list ! i) = x")
apply(force)
apply(rule_tac x = "y_cl_var_var'_v_list ! i" in exI)
apply(simp)
done

lemma distinct_x_var:
  "distinct (map (\<lambda>(y, cl, var, var', v). x_var var) y_cl_var_var'_v_list) =
   distinct (map (\<lambda>(y, cl, var, var', v). var) y_cl_var_var'_v_list)"
apply (induct y_cl_var_var'_v_list)
by (force simp add: contrapos_np)+

lemma distinct_x_var':
  "distinct (map (\<lambda>(y, cl, var, var', v). x_var var') y_cl_var_var'_v_list) =
   distinct (map (\<lambda>(y, cl, var, var', v). var') y_cl_var_var'_v_list)"
apply(induct y_cl_var_var'_v_list)
by (force simp add: contrapos_np)+

lemma map_fst_two:
  "map fst (map (\<lambda>(y, cl, var, var', v). (x_var var, x_var var')) y_cl_var_var'_v_list) =
   map (\<lambda>(y, cl, var, var', v). x_var var) y_cl_var_var'_v_list"
by (induct y_cl_var_var'_v_list, auto)

lemma map_fst_two':
  "map fst (map (\<lambda>(y, cl, var, var', y). (x_var var', y)) y_cl_var_var'_v_list) =
   map (\<lambda>(y, cl, var, var', y). x_var var') y_cl_var_var'_v_list"
by (induct y_cl_var_var'_v_list, auto)

lemma map_fst_var':
  "distinct (map fst (map (\<lambda>(y, cl, var, var', y). (x_var var', y)) y_cl_var_var'_v_list)) =
   distinct (map (\<lambda>(y, cl, var, var', v). var') y_cl_var_var'_v_list)"
by (simp only: map_fst_two' distinct_x_var')

lemma distinct_var:
  "\<lbrakk>distinct (map (\<lambda>(cl, var, ty). var) cl_var_ty_list);
    map (\<lambda>(y, cl, var, var', v). var) y_cl_var_var'_v_list = map (\<lambda>(cl, var, ty). var) cl_var_ty_list\<rbrakk> \<Longrightarrow>
      distinct (map fst (map (\<lambda>(y, cl, var, var', v). (x_var var, x_var var')) y_cl_var_var'_v_list))"
by (simp only: map_fst_two distinct_x_var)

lemma distinct_var':
  "\<lbrakk>map (\<lambda>(y, cl, var, u). var) y_cl_var_var'_v_list = map (\<lambda>(cl, var, ty). var) cl_var_ty_list;
    map (\<lambda>(cl, var, ty). ty) cl_var_ty_list = map snd y_ty_list\<rbrakk> \<Longrightarrow>
    distinct (map fst (map (\<lambda>((y, cl, var, var', v), y', y). (x_var var', y)) (zip y_cl_var_var'_v_list y_ty_list))) =
    distinct (map (\<lambda>(y, cl, var, var', v). var') y_cl_var_var'_v_list)"
by (simp only: map_length_var_ty fst_zip_eq distinct_x_var')

lemma weaken_list_var:
  "map (\<lambda>(y, cl, var, var', v). var) y_cl_var_var'_v_list =
   map (\<lambda>(y, cl, var, u). var) y_cl_var_var'_v_list"
by (induct y_cl_var_var'_v_list, auto)

lemma weaken_list_fd:
  "map (\<lambda>(y, cl, var, var', v). vd_def cl var) list = map (\<lambda>(y, cl, var, u). vd_def cl var) list"
by (induct list, auto)

lemma weaken_list_y:
 "map (\<lambda>(y, cl, var, var', v). y) y_cl_var_var'_v_list =
  map fst y_cl_var_var'_v_list"
by (induct y_cl_var_var'_v_list, auto)

lemma fcis_cld_mem[rule_format]:
  "find_cld_in_self_f path pn fqn = Some cld \<longrightarrow> cld \<in> set path"
by (induct_tac path rule: find_cld_in_self_f.induct, auto split: fqn.splits cld.splits)

lemma fcim_cld_mem[rule_format]:
  "find_cld_in_module_f clds fqn = Some cld \<longrightarrow> cld \<in> set clds"
by (induct clds, auto split: fqn.splits cld.splits)

lemma fcii_cld_mem[rule_format]:
  "\<forall>mi pn cld. find_cld_in_imports_f (MH, mis, fqn) = Some (ctx_def mi pn, cld)
      \<longrightarrow> (\<forall>repl mn clds ms fqns mis'. MH mi = Some (md_def repl mn clds ms fqns, mis') \<longrightarrow> cld \<in> set clds)"
apply(induct_tac MH mis fqn rule: fcii_induct) apply(simp)
apply(clarsimp) apply(case_tac "MH mi") apply(simp) apply(clarsimp) apply(rename_tac md mis'')
apply(case_tac md) apply(rename_tac repl' mn' clds' ms' fqns') apply(clarsimp split: split_if_asm)
apply(case_tac "find_cld_in_module_f clds' (rename_f br fqn)")
 apply(case_tac "find_cld_in_imports_f (MH, mis'', rename_f br fqn)")
  apply(clarsimp) 
 apply(clarsimp)
apply(clarsimp) apply(drule fcim2fcis) apply(simp add: fcis_cld_mem)
done

lemma fc_found_in_members:
  "\<lbrakk>find_cld_f (p_def RC MH) (ctx_def mi pn) fqn = Some (ctx_def mi pn, cld);
    MH mi = Some (md_def repl mn clds ms fqns, mis)\<rbrakk>
       \<Longrightarrow> cld \<in> set clds"
apply(simp add: find_cld_f_def) apply(clarsimp split: option.splits split_if_asm) 
  apply(frule fcii_cld_mem) apply(force) apply(assumption)
 apply(simp add: fcis_cld_mem)
apply(clarsimp simp add: find_cld_in_core_f_def fcim_cld_mem split: option.splits R.splits md.splits)
done

lemma wf_cld_from_lu:
  "\<lbrakk>P \<in> wf_p; find_cld_f P ctx fqn = Some (ctx_def mi pn, cld)\<rbrakk> \<Longrightarrow> (P, mi, cld) \<in> wf_class"
apply(erule wf_programE) apply(clarsimp) apply(erule wf_mhE) apply(clarsimp) apply(rename_tac MH RC)
apply(drule_tac x = mi in bspec)
 apply(drule find_cld_same_ctx) apply(simp add: find_cld_f_def)
 apply(force simp add: find_cld_in_core_f_def split: split_if_asm option.splits R.splits md.splits)
apply(clarsimp) apply(erule wf_mdE) apply(clarsimp)
apply(drule find_cld_same_ctx) apply(drule fc_found_in_members) apply(force) apply(force)
done

lemma meth_def_in_set[rule_format]:
  "(meth_defs, meth, Some meth_def) \<in> find_meth_def_in_list \<longrightarrow> meth_def \<in> set meth_defs"
apply(clarsimp) apply(induct meth_defs) by (auto split: meth_def.splits meth_sig.splits split_if_asm)

lemma find_meth_def_in_list_mem[rule_format, simp]:
  "find_meth_def_in_list_f meth_defs meth = Some meth_def \<longrightarrow> meth_def \<in> set meth_defs"
apply(induct meth_defs) apply(auto split: meth_def.splits meth_sig.splits) done

lemma find_meth_def_in_path_ex_cld[rule_format]:
   "find_meth_def_in_path_f ctxclds meth = Some (ctx, meth_def)
      \<longrightarrow> (\<exists>cld meth_defs. (ctx, cld) \<in> set ctxclds \<and> class_methods_f cld = meth_defs \<and> meth_def \<in> set meth_defs)"
apply(induct ctxclds) apply(simp) apply(clarsimp)
apply(clarsimp split: option.splits) apply(rule_tac x = cld in exI) apply(force)
apply(force)
done

lemma map_ctx_cld_dcl_two[simp]:
  "ctxclds = map (\<lambda>(ctx, cld, dcl). (ctx, cld)) (map (\<lambda>(ctx, cld). (ctx, cld, classname_f cld)) ctxclds)"
by (induct ctxclds, auto)

lemma fcii_pn_match[rule_format]:
  "\<forall>mi pn cld. find_cld_in_imports_f (MH, mibrs, fqn) = Some (ctx_def mi pn, cld)
      \<longrightarrow> package_name_f cld = pn"
apply(induct_tac MH mibrs fqn rule: fcii_induct) apply(simp)
apply(clarsimp) apply(rename_tac mi' pn cld) apply(case_tac "MH mi") apply(simp)
apply(clarsimp) apply(rename_tac md mibrs') apply(case_tac md, rename_tac repl mn clds ms fqns, clarsimp)
apply(clarsimp split: split_if_asm option.splits)
done

lemma fcic_pn_match:
  "find_cld_in_core_f P fqn = Some (ctx_def mi pn, cld) \<Longrightarrow> package_name_f cld = pn"
apply(simp add: find_cld_in_core_f_def)
apply(clarsimp split: P.splits R.splits option.splits md.splits)
done

lemma find_cld_pn_match:
  "find_cld_f P ctx fqn = Some (ctx_def mi pn, cld) \<Longrightarrow> package_name_f cld = pn"
apply(simp add: find_cld_f_def) apply(clarsimp split: split_if_asm)
apply(case_tac "find_cld_in_core_f P fqn") apply(simp)
 apply(case_tac P, rename_tac RC MH, clarsimp) apply(case_tac ctx, rename_tac mi' pn', clarsimp)
 apply(case_tac "MH mi'") apply(simp) apply(clarsimp) apply(rename_tac md mibrs)
 apply(case_tac md, rename_tac repl mn clds ms fqns, clarsimp)
 apply(case_tac "find_cld_in_self_f clds pn' fqn")
  apply(clarsimp) apply(simp add: fcii_pn_match)
 apply(clarsimp)
apply(clarsimp simp add: fcic_pn_match)
done

lemma wf_method_from_find:
  "\<lbrakk>P \<in> wf_p; (P, ty_x_d, meth, Some (ctx, meth_def)) \<in> find_meth_def\<rbrakk> \<Longrightarrow>
      \<exists>dcl. (P, ty_x_d, ty_def ctx dcl) \<in> sty_one \<and> (P, ty_def ctx dcl, meth_def) \<in> wf_meth"
apply(simp add: find_meth_def_f_def split: option.splits) apply(rename_tac path)
apply(case_tac ty_x_d) apply(simp) apply(rename_tac ctx' dcl') apply(case_tac ctx', rename_tac mi' pn', clarsimp)
apply(drule find_meth_def_in_path_ex_cld) apply(clarsimp)
apply(rule_tac x = "class_name_f cld" in exI)
apply(frule all_in_path_found) apply(simp)
apply(case_tac cld) apply(rename_tac pn am dcl cl fds mds) apply(clarsimp simp add: full_name_f_def class_name_f_def class_methods_f_def)
apply(case_tac ctx) apply(rename_tac mi pn'') apply(clarsimp) apply(frule find_cld_same_ctx) apply(clarsimp simp add: full_name_f_def)
apply(frule find_cld_pn_match) apply(clarsimp simp add: package_name_f_def)
apply(rule)
 apply(cut_tac P = P and ty = "ty_def (ctx_def mi' pn') dcl'" in sty_dclI[simplified])
    apply(simp)
   apply(force)
  apply(simp)
 apply(simp)
apply(frule wf_cld_from_lu) apply(simp)
apply(erule wf_classE) apply(erule wf_class_cE) apply(clarsimp simp: class_name_f_def)
apply(drule_tac x = "(a, b)" in bspec, simp) apply(simp)
done

lemma find_type_lift_opts[rule_format]:
  "(\<forall>x\<in>set cl_var_ty_list. (\<lambda>(cl_k, var_k, ty_k). find_type_f P ctx cl_k = Some ty_k) x) \<longrightarrow>
      lift_opts (map (vd_case (\<lambda>clk vark. find_type_f P ctx clk)) (map (\<lambda>(cl_k, var_k, ty_k). vd_def cl_k var_k) cl_var_ty_list)) =
      Some (map (\<lambda>(cl, var, ty). ty) cl_var_ty_list)"
by (induct cl_var_ty_list, auto)

lemma find_md_in_pre_path[rule_format]:
  "find_meth_def_in_path_f path m = Some ctxmd \<longrightarrow> (\<forall>path'. find_meth_def_in_path_f (path @ path') m = Some ctxmd)"
by (induct path, auto split: option.splits)

lemma lift_opts_map:
  "\<forall>x\<in>set cl_var_ty_list. (\<lambda>(cl_k, var_k, ty_k). find_type_f P ctx cl_k = Some ty_k) x \<Longrightarrow>
      lift_opts (map (vd_case (\<lambda>clk vark. find_type_f P ctx clk)) (map (\<lambda>(cl_k, var_k, ty_k). vd_def cl_k var_k) cl_var_ty_list)) = Some (map (\<lambda>(cl, var, ty). ty) cl_var_ty_list)"
by (induct cl_var_ty_list, auto)

lemma m_in_list[rule_format]:
  "(\<forall>x\<in>set md_m_list. split (\<lambda>md. op = (method_name_f md)) x) \<and>
   find_meth_def_in_list_f (map fst md_m_list) m = Some md \<longrightarrow>
       m \<in> snd ` set md_m_list"
by (induct md_m_list, auto simp add: method_name_f_def split: meth_def.splits meth_sig.splits)

lemma m_image_eq[rule_format]:
  "meth_def_def (meth_sig_def cl m list2) meth_body \<in> set meth_defs \<longrightarrow>
      m \<in> meth_def_case (\<lambda>meth_sig meth_body. case meth_sig of meth_sig_def cl meth vds \<Rightarrow> meth) ` set meth_defs"
by (induct meth_defs, auto)

lemma fmdip_to_mip[rule_format]:
  "find_meth_def_in_path_f path m = Some ctxmd \<longrightarrow> m \<in> set (methods_in_path_f (map snd path))"
apply(induct path) apply(simp) apply(clarsimp simp add: class_methods_f_def split: option.splits cld.splits)
apply(case_tac aa) apply(case_tac meth_sig) apply(clarsimp) apply(frule find_md_m_match') apply(clarsimp)
apply(frule find_meth_def_in_list_mem) apply(frule m_image_eq) apply(assumption)
done

lemma lift_opts_for_all[rule_format]:
  "lift_opts (map (vd_case (\<lambda>clk vark. find_type_f P ctx clk)) (map (\<lambda>(cl, var, ty). vd_def cl var) cl_var_ty_list)) = None \<and>
   (\<forall>x\<in>set cl_var_ty_list. (\<lambda>(cl, var, ty). find_type_f P ctx cl = Some ty) x) \<longrightarrow> False"
apply(induct cl_var_ty_list) apply(simp) apply(clarsimp) done

lemma
  "\<lbrakk>find_meth_def_f P (ty_def (ctx_def mi'' pn'') dcl'') m = Some (ctx_m, meth_def_def (meth_sig_def cl_r m' vds) mb);
    find_type_f P ctx_m cl_r = Some ty_r; lift_opts (map (vd_case (\<lambda>clk vark. find_type_f P ctx_m clk)) vds) = Some tys;
    mtype_f P (ty_def (ctx_def mi pn') dcl') m = Some mty'; mtype_f P (ty_def (ctx_def mi'' pn'') dcl'') m = Some mty'\<rbrakk>
       \<Longrightarrow> (\<exists>a b. find_meth_def_f P (ty_def (ctx_def mi pn') dcl') m = Some (a, b)) \<and>
          (\<forall>a cl list1 list2.
              ((\<exists>y. find_type_f P a cl = Some y) \<or>
               (\<forall>meth_body. find_meth_def_f P (ty_def (ctx_def mi pn') dcl') m \<noteq> Some (a, meth_def_def (meth_sig_def cl list1 list2) meth_body))) \<and>
              (\<forall>aa. (find_type_f P a cl = Some aa \<longrightarrow>
                     (\<exists>y. lift_opts (map (vd_case (\<lambda>clk vark. find_type_f P a clk)) list2) = Some y) \<or>
                     (\<forall>meth_body. find_meth_def_f P (ty_def (ctx_def mi pn') dcl') m \<noteq> Some (a, meth_def_def (meth_sig_def cl list1 list2) meth_body))) \<and>
                    (find_type_f P a cl = Some aa \<longrightarrow>
                     (\<forall>ab. lift_opts (map (vd_case (\<lambda>clk vark. find_type_f P a clk)) list2) = Some ab \<longrightarrow>
                           (\<forall>meth_body.
                               find_meth_def_f P (ty_def (ctx_def mi pn') dcl') m \<noteq> Some (a, meth_def_def (meth_sig_def cl list1 list2) meth_body)) \<or>
                           ab = tys \<and> aa = ty_r))))"
apply(clarsimp simp add: mtype_f_def split: option.splits meth_def.splits meth_sig.splits) apply(auto)
done

lemma fpr_diff_prefix[rule_format]:
  "\<forall>suffix. find_path_rec_f (P, ctx, cl, prefix) = Some (prefix @ suffix)
     \<longrightarrow> (\<forall>prefix'. find_path_rec_f (P, ctx, cl, prefix') = Some (prefix' @ suffix))"
apply(induct_tac P ctx cl prefix rule: find_path_rec_f.induct)
apply(simp) apply(clarsimp split: option.splits)
apply(frule path_append) apply(clarsimp)
done

declare find_meth_def_in_path_f.simps [simp del]
declare methods_in_path_f.simps [simp del]

lemma mty_preservation'''':
  "\<lbrakk>P \<in> wf_p; P \<in> acyclic_clds;
    find_cld_f P ctx (fqn_def pn' dcl') = Some (ctx', cld_def pn' am' dcl' (cl_fqn fqn) fds' mds');
    find_cld_f P ctx' fqn = Some (ctx'', cld'');
    find_path_rec_f (P, ctx'', superclass_name_f cld'', path @ [(ctx', cld_def pn' am' dcl' (cl_fqn fqn) fds' mds'), (ctx'', cld'')]) =
      Some (path @ (ctx', cld_def pn' am' dcl' (cl_fqn fqn) fds' mds') # (ctx'', cld'') # path');
    mtype_f P (ty_def ctx'' (class_name_f cld'')) m = Some mty\<rbrakk>
       \<Longrightarrow> mtype_f P (ty_def ctx' dcl') m = Some mty"
apply(drule find_cld_same_ctx) apply(case_tac ctx', rename_tac mi pn'', clarsimp)
apply(frule find_cld_pn_match) apply(clarsimp simp add: package_name_f_def) apply(drule wf_cld_from_lu) apply(simp add: full_name_f_def)+
apply(subgoal_tac "\<exists>ctx_m mb cl_r m' vds ty_r tys.
                   find_meth_def_f P (ty_def ctx'' (class_name_f cld'')) m = Some (ctx_m, meth_def_def (meth_sig_def cl_r m' vds) mb) \<and>
                   find_type_f P ctx_m cl_r = Some ty_r \<and> lift_opts (map (vd_case (\<lambda>clk vark. find_type_f P ctx_m clk)) vds) = Some tys")
defer apply(clarsimp simp add: mtype_f_def split: option.splits meth_def.splits meth_sig.splits) apply(clarsimp)
apply(erule wf_classE) apply(erule wf_class_cE) apply(clarsimp) apply(rename_tac mi ty_s cl_f_ty_list fs md_m_list m_mty_mty'_list)
apply(case_tac fqn) apply(rename_tac pn dcl) apply(clarsimp)
apply(case_tac ctx'') apply(rename_tac mi'' pn'')
apply(frule_tac ctx' = "ctx_def mi pn'" in find_cld_same_ctx)
apply(cut_tac prefix = "path @ [(ctx_def mi pn', cld_def pn' am' dcl' (cl_fqn (fqn_def pn dcl)) (map (\<lambda>(cl, f, ty). fd_def cl f) cl_f_ty_list)
                        (map fst md_m_list)), (ctx_def mi'' pn'', cld'')]" and
              prefix' = "[(ctx_def mi pn', cld_def pn' am' dcl' (cl_fqn (fqn_def pn dcl)) (map (\<lambda>(cl, f, ty). fd_def cl f)
                         cl_f_ty_list) (map fst md_m_list)), (ctx_def mi'' pn'', cld'')]" in fpr_diff_prefix) apply(simp)
apply(clarsimp simp add: find_meth_def_f_def find_path_f_def superclass_name_f_def class_methods_f_def)
apply(frule_tac ctx' = "ctx_def mi'' pn''" in find_cld_same_ctx)
apply(clarsimp simp add: class_name_f_def superclass_name_f_def full_name_f_def)
apply(frule find_cld_pn_match) apply(case_tac cld'', rename_tac pn''' am'' dcl'' cl' fds' mds')
apply(clarsimp simp add: package_name_f_def superclass_name_f_def)
apply(cut_tac prefix = "[(ctx_def mi pn', cld_def pn' am' dcl' (cl_fqn (fqn_def pn dcl)) (map (\<lambda>(cl, f, ty). fd_def cl f) cl_f_ty_list)
                         (map fst md_m_list)), (ctx_def mi'' pn'', cld_def pn'' am'' dcl'' cl' fds' mds')]" and
              prefix' = "[(ctx_def mi'' pn'', cld_def pn'' am'' dcl'' cl' fds' mds')]" in fpr_diff_prefix) apply(simp)
apply(simp add: methods_f_def find_path_f_def superclass_name_f_def)
apply(subgoal_tac "\<exists>ctx_m md. find_meth_def_f P (ty_def (ctx_def mi pn') dcl') m = Some (ctx_m, md)")
 apply(clarify) apply(frule fmdip_to_mip) apply(simp only: map.simps(2) snd_conv)
 apply(frule find_cld_same_ctx) apply(clarsimp) apply(rename_tac mty' mty'')
 apply(drule_tac x = "(m, mty', mty'')" in bspec, simp)+ apply(clarsimp)
 apply(simp add: find_meth_def_in_path_f.simps class_methods_f_def)
 apply(simp add: mtype_f_def)
 apply(case_tac "find_meth_def_f P (ty_def (ctx_def mi'' pn'') dcl'') m") apply(simp) apply(clarsimp)
 apply(rename_tac ctx_m md mty' ctx_m' md')
 apply(clarsimp simp add: find_meth_def_f_def find_path_f_def superclass_name_f_def)
 apply(case_tac "find_meth_def_in_list_f (map fst md_m_list) m")
  apply(clarsimp simp add: find_meth_def_in_path_f.simps class_methods_f_def)
 apply(cut_tac m = m and md_m_list = md_m_list in m_in_list) apply(simp) apply(simp)
apply(clarsimp simp add: find_meth_def_f_def class_name_f_def superclass_name_f_def find_path_f_def
                         find_meth_def_in_path_f.simps class_methods_f_def split: option.splits)
done

declare find_meth_def_in_path_f.simps [simp]
declare methods_in_path_f.simps [simp]

lemma fpr_mem_to_path:
  "\<forall>suffix. find_path_rec_f (P, ctx, cl, prefix) = Some (prefix @ suffix) \<longrightarrow>
      (\<forall>(ctx', cld') \<in> set suffix. \<forall>prefix'.
           (\<exists>path'. find_path_rec_f (P, ctx', cl_fqn (full_name_f cld'), prefix') = Some path'))"
apply(induct_tac P ctx cl prefix rule: find_path_rec_f.induct) apply(simp)
apply(clarsimp split: option.splits) apply(rename_tac prefix' ctx cld suffix ctx' cld')
apply(frule path_append) apply(clarsimp) apply(erule disjE)
 apply(clarsimp) apply(frule find_cld_same_ctx)
 apply(case_tac fqn) apply(rename_tac mi pn) apply(clarsimp)
 apply(cut_tac prefix = "prefix' @ [(ctx, cld)]" and prefix' = "prefix'a @ [(ctx, cld)]" in fpr_diff_prefix)
  apply(simp) apply(simp)
apply(drule_tac x = "(ctx', cld')" in bspec, simp) apply(clarsimp)
done

lemma fp_mem_to_path:
  "\<lbrakk>find_path_f P ctx cl = Some path; (ctx', cld') \<in> set path\<rbrakk>
      \<Longrightarrow> \<exists>path'. find_path_f P ctx' (cl_fqn (full_name_f cld')) = Some path'"
apply(cut_tac P = P and ctx = ctx and cl = cl in fpr_mem_to_path[of _ _ _ "[]"])
apply(erule_tac x = path in allE) apply(erule impE) apply(simp add: find_path_f_def)
apply(drule_tac x = "(ctx', cld')" in bspec, simp) apply(simp del: find_path_rec_f.simps)
apply(simp only: find_path_f_def)
done

lemma mty_preservation'''[rule_format]:
  "\<forall>ctx' cld' suffix. find_path_rec_f (P, ctx, cl, prefix) = Some (prefix @ (ctx', cld') # suffix) \<longrightarrow>
      P \<in> wf_p \<longrightarrow>
          (\<forall>(ctx'', cld'') \<in> set ((ctx', cld') # suffix).
              mtype_f P (ty_def ctx'' (class_name_f cld'')) m = Some mty \<longrightarrow>
                  mtype_f P (ty_def ctx' (class_name_f cld')) m = Some mty)"
apply(induct_tac P ctx cl prefix rule: find_path_rec_f.induct) apply(simp)
apply(clarsimp split: option.splits)
apply(frule path_append) apply(clarsimp) apply(rename_tac ctx' cld' suffix ctx'' cld'')
apply(case_tac cld') apply(rename_tac pn' am' dcl' cl' fds' mds')
apply(clarsimp simp add: superclass_name_f_def)
apply(case_tac cl') apply(simp) apply(rename_tac fqn')
apply(clarsimp split: split_if_asm option.splits) apply(rename_tac ctx''' cld''')
apply(case_tac fqn, rename_tac pn dcl, clarsimp) apply(frule find_cld_same_ctx)
apply(clarsimp simp add: full_name_f_def)
apply(frule path_append) apply(clarsimp) apply(erule disjE)
 apply(clarsimp simp add: class_name_f_def full_name_f_def)
 apply(rule mty_preservation'''') apply(force+) apply(simp add: class_name_f_def)
apply(drule_tac x = "(ctx'', cld'')" in bspec, simp)
apply(clarsimp simp add: class_name_f_def superclass_name_f_def)
apply(rule_tac path' = path'' in mty_preservation'''') apply(force simp add: class_name_f_def superclass_name_f_def)+
done

lemma mty_preservation':
  "\<lbrakk>P \<in> wf_p; find_path_f P ctx cl = Some ((ctx', cld') # path);
    (ctx'', cld'') \<in> set ((ctx', cld') # path); mtype_f P (ty_def ctx'' (class_name_f cld'')) m = Some mty\<rbrakk>
        \<Longrightarrow> mtype_f P (ty_def ctx' (class_name_f cld')) m = Some mty"
apply(cut_tac x = "(ctx'', cld'')" in mty_preservation'''[rule_format, of _ _ _ "[]"])
apply(simp add: find_path_f_def)+ apply(force) done

lemma lift_opts_for_all_true[rule_format]:
  "\<forall>y_ty_list.
      (\<forall>x\<in>set cl_var_ty_list. (\<lambda>(cl_k, var_k, ty_k). find_type_f P ctx cl_k = Some ty_k) x) \<and>
      lift_opts (map (vd_case (\<lambda>clk vark. find_type_f P ctx clk)) (map (\<lambda>(cl_k, var_k, ty_k). vd_def cl_k var_k) cl_var_ty_list)) = Some (map snd y_ty_list) \<longrightarrow>
          map (\<lambda>(cl, var, ty). ty) cl_var_ty_list = map snd y_ty_list"
by (induct cl_var_ty_list, auto split: option.splits)

lemma mtype_search_at_found:
  "\<lbrakk>mtype_f P (ty_def (ctx_def mi pn) dcl) meth = Some (mty_def (map snd y_ty_list) ty_r_s);
    find_cld_f P (ctx_def mi pn) (fqn_def pn dcl) = Some (ctx_def mi' pn', cld_def pn' am dcl' cl fds mds)\<rbrakk>
       \<Longrightarrow> mtype_f P (ty_def (ctx_def mi' pn') dcl') meth = Some (mty_def (map snd y_ty_list) ty_r_s)"
apply(simp add: mtype_f_def)
apply(case_tac "find_meth_def_f P (ty_def (ctx_def mi pn) dcl) meth") apply(simp) apply(clarsimp) apply(rename_tac ctx md)
apply(clarsimp split: meth_def.splits meth_sig.splits) apply(rename_tac mb cl_r m vds)
apply(case_tac "find_type_f P ctx cl_r") apply(simp) apply(clarsimp) apply(rename_tac ty_r)
apply(case_tac "lift_opts (map (vd_case (\<lambda>clk vark. find_type_f P ctx clk)) vds)") apply(simp) apply(clarsimp)
apply(simp add: find_meth_def_f_def)
apply(case_tac "find_path_f P (ctx_def mi pn) (cl_fqn (fqn_def pn dcl))") apply(simp) apply(clarsimp) apply(rename_tac path)
apply(frule fpr_target_is_head) apply(clarsimp) apply(frule fp_same_ctx) apply(simp add: full_name_f_def)
done

lemma mty_preservation:
  "\<lbrakk>P \<in> wf_p;
    find_meth_def_f P ty_x_d meth = Some (ctx, meth_def_def (meth_sig_def cl_r meth (map (\<lambda>(cl_k, var_k, ty_k). vd_def cl_k var_k) cl_var_ty_list)) meth_body);
    find_type_f P ctx cl_r = Some ty_r_d; \<forall>x\<in>set cl_var_ty_list. (\<lambda>(cl_k, var_k, ty_k). find_type_f P ctx cl_k = Some ty_k) x;
    mtype_f P ty_x_s meth = Some (mty_def (map snd y_ty_list) ty_r_s); is_sty_one P ty_x_d ty_x_s = Some True\<rbrakk>
       \<Longrightarrow> ty_r_d = ty_r_s \<and> map (\<lambda>(cl, var, ty). ty) cl_var_ty_list = map snd y_ty_list"
apply(case_tac "ty_x_d = ty_x_s")
 apply(clarsimp) apply(clarsimp simp add: mtype_f_def find_type_lift_opts split: option.splits)
apply(simp add: is_sty_one_def split: option.splits)
 apply(case_tac ty_x_s) apply(clarsimp simp add: mtype_f_def find_meth_def_f_def)
apply(clarsimp) apply(rename_tac path_d ctx_s dcl_s)
apply(case_tac ty_x_d) apply(simp) apply(clarsimp simp add: find_meth_def_f_def) apply(rename_tac ctx_d dcl_d)
apply(clarsimp simp add: find_meth_def_f_def split: option.splits)
apply(case_tac ctx_d, rename_tac mi_d pn_d, clarsimp)
apply(case_tac ctx_s, rename_tac mi_s pn_s, clarsimp split: option.splits) apply(rename_tac ctx_s cld_s)
apply(case_tac ctx_s, rename_tac mi_s' pn_s', clarsimp)
apply(case_tac cld_s, rename_tac pn_s'' am_s dcl_s' cl_s fds_s mds_s, clarsimp)
apply(frule find_cld_pn_match) apply(clarsimp simp add: package_name_f_def)
apply(drule mtype_search_at_found) apply(force)
apply(frule fpr_target_is_head) apply(clarify)
apply(rename_tac ctx_d cld_d path')
apply(frule_tac ctx = "ctx_def mi_d pn_d" and path = path' and cld' = cld_d and
                ctx'' = "ctx_def mi_s' pn_s'" and cld'' = "cld_def pn_s' am_s dcl_s' cl_s fds_s mds_s" in mty_preservation')
   apply(force)
  apply(assumption)
 apply(simp add: class_name_f_def)
apply(simp add: class_name_f_def class_methods_f_def)
apply(thin_tac "mtype_f ?P ?T ?M = ?R")
apply(simp add: mtype_f_def)
apply(case_tac "find_meth_def_f P (ty_def ctx_d (case cld_d of cld_def pd am dcl cl fds mds \<Rightarrow> dcl)) meth") apply(simp) apply(clarsimp)
apply(rename_tac ctx_m md) apply(clarsimp split: meth_def.splits meth_sig.splits) apply(rename_tac mb cl_r' meth' vds)
apply(case_tac "find_type_f P ctx_m cl_r'") apply(simp) apply(rename_tac ty_cl_r') apply(clarsimp)
apply(case_tac "lift_opts (map (vd_case (\<lambda>clk vark. find_type_f P ctx_m clk)) vds)") apply(simp) apply(rename_tac tys') apply(clarsimp)
apply(simp add: find_meth_def_f_def) apply(case_tac ctx_d, rename_tac mi_d' pn_d', clarsimp)
apply(case_tac "find_path_f P (ctx_def mi_d' pn_d') (cl_fqn (fqn_def pn_d' (case cld_d of cld_def pd am dcl cl fds mds \<Rightarrow> dcl)))") apply(simp)
apply(clarsimp) apply(rename_tac path) apply(frule fp_same_ctx)
apply(case_tac cld_d, rename_tac pn_d'' am_d dcl_d' cl_d fds_d mds_d, clarsimp simp add: full_name_f_def)
apply(frule_tac fqn = "fqn_def pn_d'' dcl_d'" in fpr_target_is_head) apply(clarsimp)
apply(frule_tac fqn = "fqn_def pn_d'' dcl_d'" in find_cld_pn_match) apply(clarsimp simp add: package_name_f_def)
apply(simp add: full_name_f_def class_methods_f_def)
apply(rule_tac P = P and ctx = ctx in lift_opts_for_all_true) apply(simp)
done

lemma map_not_mem:
  "\<lbrakk>(y_k, ty_k, var_k, var'_k, v_k) \<in> set y_ty_var_var'_v_list; x' \<notin> (\<lambda>(y, ty, var, var', v). x_var var') ` set y_ty_var_var'_v_list\<rbrakk>
         \<Longrightarrow> x_var var'_k \<noteq> x'"
by (force)

lemma map_fst:
   "map fst (map (\<lambda>(y, ty, var, var', v). (x_var var', ty)) y_ty_var_var'_v_list) = map (\<lambda>(y, ty, var, var', v). x_var var') y_ty_var_var'_v_list"
by (force simp add: map_compose [THEN sym])

lemma supertype_top:
  "(P, ty, ty') \<in> sty_one \<Longrightarrow> ty = ty_top \<longrightarrow> ty' = ty_top"
by (induct rule: sty_one.induct, auto)

lemma top_not_subtype[rule_format]:
  "(P, ty_top, ty_def ctx dcl) \<in> sty_one \<longrightarrow> False"
by (rule, drule supertype_top, simp)

lemma f_in_found_fds:
  "ftype_in_fds_f P ctx fds f = ty_opt_bot_opt (Some ty_f) \<longrightarrow> f \<in> fd_case (\<lambda>cl f. f) ` set fds"
by (induct fds, auto split: fd.splits)

lemma ftype_fields[rule_format]:
  "ftype_in_path_f P path_s f = Some ty_f \<longrightarrow> f \<in> set (fields_in_path_f path_s)"
apply(induct path_s) apply(simp) apply(clarsimp split: option.splits)
apply(case_tac b) apply(clarsimp) apply(rename_tac ctx path_s dcl cl fds mds)
apply(clarsimp simp add: class_fields_f_def split: ty_opt_bot.splits option.splits) apply(simp add: f_in_found_fds)
done

lemma no_field_hiding''':
  "\<forall>suffix. find_path_rec_f (P, ctx, cl, prefix) = Some (prefix @ suffix) \<longrightarrow> P \<in> wf_p \<longrightarrow>
     (\<forall>(ctx_s, cld_s) \<in> set suffix.
         (\<forall>prefix' suffix'. find_path_rec_f (P, ctx_s, cl_fqn (full_name_f cld_s), prefix') = Some (prefix' @ suffix') \<and>
               f \<in> set (fields_in_path_f suffix') \<longrightarrow> f \<in> set (fields_in_path_f suffix)))"
apply(induct_tac P ctx cl prefix rule: find_path_rec_f.induct) apply(simp)
apply(clarsimp split: option.splits)
apply(rename_tac ctx_d cld_d suffix ctx_s cld_s ctx_s' prefix' cld_s' suffix')
apply(frule path_append) apply(clarify)
apply(erule_tac x = "tl suffix" in allE)
apply(clarsimp)
apply(erule disjE)
 apply(clarify)
 apply(drule find_cld_same_ctx) apply(case_tac cld_d) apply(rename_tac pn am dcl cl fds mds)
 apply(clarsimp simp add: full_name_f_def) apply(clarsimp simp add: superclass_name_f_def)
 apply(frule_tac path = "prefix' @ suffix'" in path_append) apply(clarsimp)
 apply(frule_tac suffix = path'' and prefix' = "prefix' @ [(ctx_d, cld_def pn am dcl cl fds mds)]" and
                 suffix' = path''a in fpr_same_suffix[rule_format]) apply(force) apply(simp)
apply(drule_tac x = "(ctx_s, cld_s)" in bspec, simp) apply(clarsimp) apply(force)
done

lemma no_field_hiding'':
  "\<lbrakk>find_path_f P ctx cl = Some suffix; P \<in> wf_p; (ctx_s, cld_s) \<in> set suffix\<rbrakk>
      \<Longrightarrow> \<forall>prefix' suffix'.
            find_path_rec_f (P, ctx_s, cl_fqn (full_name_f cld_s), prefix') = Some (prefix' @ suffix') \<and> f \<in> set (fields_in_path_f suffix') \<longrightarrow>
                        f \<in> set (fields_in_path_f suffix)"
apply(cut_tac x = "(ctx_s, cld_s)" in no_field_hiding'''[of _ _ _ "[]", rule_format]) apply(simp add: find_path_f_def)+ done

lemma no_field_hiding':
  "\<lbrakk>P \<in> wf_p; find_path_f P ctx cl = Some path_d; (ctx_s, cld_s) \<in> set path_d;
    find_path_f P ctx_s (cl_fqn (full_name_f cld_s)) = Some path_s; f \<in> set (fields_in_path_f path_s)\<rbrakk>
       \<Longrightarrow> f \<in> set (fields_in_path_f path_d)"
apply(cut_tac no_field_hiding''[rule_format, of _ _ _ _ _ _ "[]"]) apply(assumption+) apply(unfold find_path_f_def) apply(rule) apply(simp+) done

lemma no_field_hiding:
  "\<lbrakk>P \<in> wf_p; is_sty_one P ty_x_d ty_x_s = Some True; ftype_f P ty_x_s f = Some ty_f; fields_f P ty_x_d = Some fields_oid\<rbrakk>
        \<Longrightarrow> f \<in> set fields_oid"
apply(case_tac ty_x_s) apply(simp add: ftype_f_def) apply(rename_tac ctx_s dcl_s)
apply(case_tac ctx_s, rename_tac mi_s pn_s, clarsimp) apply(simp add: is_sty_one_def split: option.splits)
apply(rename_tac path_d ctxcld_s) apply(case_tac ty_x_d) apply(simp) apply(rename_tac ctx_d dcl_d)
apply(case_tac ctx_d, rename_tac mi_d pn_d, clarsimp) apply(rename_tac ctx_s' cld_s dcl_d mi_d pn_d)
apply(clarsimp simp add: ftype_f_def fields_f_def split: option.splits) apply(rename_tac path_s)
apply(drule ftype_fields) apply(frule_tac ctx = "ctx_def mi_s pn_s" in fpr_target_is_head) apply(clarsimp) apply(frule fp_same_ctx)
apply(frule_tac ctx = "ctx_def mi_d pn_d" and cl = "cl_fqn (fqn_def pn_d dcl_d)" in no_field_hiding')
apply(force) apply(force) apply(simp) apply(force)+
done

lemma ftype_pre_path[rule_format]:
  "ftype_in_path_f P path_s f = Some ty_f \<longrightarrow> ftype_in_path_f P (path_s @ path'') f = Some ty_f"
by (induct path_s, auto split: option.splits ty_opt_bot.splits)

lemma fields_non_intersection[rule_format]:
  "f \<in> set (fields_in_path_f path'') \<and> list_inter (map (\<lambda>(cl, f, ty). f) cl_f_ty_list) (fields_in_path_f path'') = []
      \<longrightarrow> f \<notin> set (map (\<lambda>(cl, f, ty). f) cl_f_ty_list)"
by (induct cl_f_ty_list, auto)

lemma f_notin_list[rule_format]:
  "f \<notin> set (map (\<lambda>(cl, f, ty). f) cl_f_ty_list) \<longrightarrow> ftype_in_fds_f P ctx (map (\<lambda>(cl, f, ty). fd_def cl f) cl_f_ty_list) f = ty_opt_bot_opt None"
by (induct cl_f_ty_list, auto)

declare find_path_rec_f.simps[simp del]
declare ftype_in_path_f.simps[simp del]
lemma ftype_preservation''''':
  "\<lbrakk>find_path_rec_f (P, ctx, cl, prefix @ [ctxcld']) = Some (prefix @ ctxcld' # suffix);
    find_type_f P ctx cl = Some ty; fields_f P ty = Some fs;
    ftype_in_path_f P suffix f = Some ty_f;
    list_inter (map (\<lambda>(cl, f, ty). f) cl_f_ty_list) fs = []\<rbrakk>
        \<Longrightarrow> ftype_in_fds_f P ctx (map (\<lambda>(cl, f, ty). fd_def cl f) cl_f_ty_list) f = ty_opt_bot_opt None"
apply(clarsimp simp add: fields_f_def split: option.splits) apply(rename_tac path)
apply(case_tac cl) apply(simp add: find_path_rec_f.simps ftype_in_path_f.simps)
apply(clarsimp split: fqn.splits option.splits) apply(rename_tac pn dcl ctx'' cld'')
apply(case_tac ctx'', rename_tac mi'' pn'', clarsimp)
apply(frule fpr_target_is_head'[rule_format]) apply(force) apply(clarsimp simp add: class_fields_f_def)
apply(drule find_cld_same_ctx)
apply(drule_tac ctx' = "ctx_def mi'' pn''" and suffix = path'' in fpr_same_ctx)
 apply(force simp add: full_name_f_def)
apply(simp add: full_name_f_def find_path_f_def)
apply(case_tac cld'', rename_tac pn am dcl cl fds mds, clarsimp simp add: class_name_f_def)
apply(frule find_cld_pn_match) apply(clarsimp simp add: package_name_f_def)
apply(drule_tac prefix = "[]" and prefix' = "prefix @ [ctxcld']" in fpr_same_suffix[rule_format]) apply(force)
apply(clarsimp simp add: class_fields_f_def) apply(thin_tac "find_path_rec_f ?P = ?R")
apply(drule ftype_fields)
apply(cut_tac f = f and path'' = "(ctx_def mi'' pn'', cld_def pn'' am dcl cl fds mds) # path''" and cl_f_ty_list = cl_f_ty_list in fields_non_intersection)
apply(simp add: f_notin_list class_fields_f_def)+
done
declare ftype_in_path_f.simps[simp]
declare find_path_rec_f.simps[simp]

lemma ftype_preservation'''':
  "\<forall>suffix. find_path_rec_f (P, ctx, cl, prefix) = Some (prefix @ suffix) \<longrightarrow> P \<in> wf_p \<longrightarrow>
     (\<forall>(ctx, cld) \<in> set suffix.
         (\<forall>prefix' suffix'. find_path_rec_f (P, ctx, cl_fqn (full_name_f cld), prefix') = Some (prefix' @ suffix') \<and>
               ftype_in_path_f P suffix' f = Some ty \<longrightarrow> ftype_in_path_f P suffix f = Some ty))"
apply(induct_tac P ctx cl prefix rule: find_path_rec_f.induct) apply(simp)
apply(clarsimp split: option.splits) apply(rename_tac prefix ctx' cld' suffix ctx'' cld'' ctx''' prefix' cld''' suffix')
apply(frule path_append) apply(clarify) apply(erule_tac x = "tl suffix" in allE) apply(clarsimp)
apply(erule disjE)
 apply(clarsimp) apply(case_tac fqn) apply(rename_tac mi pn)
 apply(clarsimp simp add: class_name_f_def split: cld.splits)
 apply(frule path_append) back apply(clarsimp simp add: class_fields_f_def)
 apply(drule find_cld_same_ctx) apply(clarsimp)
 apply(frule_tac prefix = "prefix @ [(ctx''', cld''')]" and suffix = path'' and
                 prefix' = "prefix' @ [(ctx''', cld''')]" and suffix' = path''a
                    in fpr_same_suffix[rule_format])
 apply(clarsimp) apply(clarsimp)
apply(drule_tac x = "(ctx'', cld'')" in bspec, simp) apply(clarsimp)
apply(erule impE) apply(force)
apply(subgoal_tac "ftype_in_fds_f P ctx' (class_fields_f cld') f = ty_opt_bot_opt None") apply(simp)
apply(case_tac ctx') apply(rename_tac mi pn) apply(clarsimp) apply(case_tac fqn) apply(rename_tac pn' dcl) apply(clarsimp)
apply(clarsimp simp add: superclass_name_f_def class_fields_f_def)
apply(frule wf_cld_from_lu) apply(simp) apply(erule wf_classE) apply(erule wf_class_cE)
apply(clarsimp simp add: superclass_name_f_def class_fields_f_def)
apply(frule find_cld_pn_match) apply(clarsimp simp add: package_name_f_def)
apply(rule ftype_preservation''''') apply(simp)+
done

lemma ftype_preservation''':
  "\<lbrakk>find_path_f P ctx' cl = Some suffix; P \<in> wf_p; (ctx, cld) \<in> set suffix\<rbrakk>
      \<Longrightarrow> \<forall>prefix' suffix'.
            find_path_rec_f (P, ctx, cl_fqn (full_name_f cld), prefix') = Some (prefix' @ suffix') \<and> ftype_in_path_f P suffix' f = Some ty \<longrightarrow>
                        ftype_in_path_f P suffix f = Some ty"
apply(cut_tac x = "(ctx, cld)" in ftype_preservation''''[of _ _ _ "[]", rule_format]) apply(simp add: find_path_f_def)+ done

lemma ftype_preservation'':
  "\<lbrakk>find_path_f P ctx' cl = Some path; P \<in> wf_p; (ctx, cld) \<in> set path;
    find_path_f P ctx (cl_fqn (full_name_f cld)) = Some path'; ftype_in_path_f P path' f = Some ty\<rbrakk>
         \<Longrightarrow> ftype_in_path_f P path f = Some ty"
apply(cut_tac ftype_preservation'''[rule_format, of _ _ _ _ _ _ "[]"]) apply(assumption+) apply(unfold find_path_f_def) apply(rule) apply(simp+) done

lemma ftype_preservation'[simplified]:
  "\<lbrakk>P \<in> wf_p; (P, ty_x_d, ty_x_s) \<in> sty_one; (P, ty_x_s, f, ty_f) \<in> ftype\<rbrakk>
     \<Longrightarrow> (P, ty_x_d, f, ty_f) \<in> ftype"
apply(case_tac ty_x_s) apply(simp add: ftype_f_def) apply(rename_tac dcl)
apply(simp add: is_sty_one_def split: option.splits) apply(rename_tac path)
apply(case_tac ty_x_d) apply(clarsimp split: ctx.splits option.splits) apply(clarsimp) apply(rename_tac ctx_s dcl_s path_d ctx_d dcl_d)
apply(case_tac ctx_d, rename_tac mi_d pn_d) apply(case_tac ctx_s, rename_tac mi_s pn_s) apply(clarsimp split: option.splits) apply(rename_tac ctx cld)
apply(simp add: ftype_f_def split: option.splits) apply(rename_tac path_s)
apply(frule_tac path = path_s in fpr_target_is_head) apply(clarsimp) apply(drule fp_same_ctx)
apply(rule ftype_preservation'') apply(simp add: class_name_f_def full_name_f_def)+
done

lemma ftype_preservation[simplified]:
  "\<lbrakk>P \<in> wf_p;
    \<forall>x\<in>dom G. (P, H, L x, G x) \<in> wf_object; G x = Some ty_x_s; (P, ty_x_s, f, ty_f_s) \<in> ftype;
    L x = Some (v_oid oid_x); H oid_x = Some (ty_x_d, fs_oid); (P, ty_x_d, f, ty_f_d) \<in> ftype\<rbrakk>
     \<Longrightarrow> ty_f_s = ty_f_d"
apply(drule_tac x = x in bspec, simp add: domI) apply(erule wf_objectE) apply(simp) apply(clarsimp)
apply(erule sty_option.cases) apply(simp add: ftype_preservation')
done

lemma map_f:
  "\<forall>cl_f_ty_list. map (\<lambda>(cl, f). fd_def cl f) cl_f_list = map (\<lambda>(cl, f, ty). fd_def cl f) cl_f_ty_list \<longrightarrow>
   map (\<lambda>(cl, f). f) cl_f_list = map (\<lambda>(cl, f, ty). f) cl_f_ty_list"
by (induct cl_f_list, auto)

lemma fields_to_owner[rule_format]:
  "f \<in> set (fields_in_path_f path) \<longrightarrow> (\<exists>cld \<in> set (map snd path). \<exists>cl_f. fd_def cl_f f \<in> set (class_fields_f cld))"
apply(induct path) apply(simp) apply(clarsimp) apply(rename_tac cld path fd)
apply(clarsimp simp add: class_fields_f_def split: option.splits cld.splits fd.splits)
apply(force)
done

lemma ftype_in_fds_none[rule_format]:
  "f \<notin> (\<lambda>(cl, f, ty). f) ` set cl_f_ty_list \<longrightarrow> ftype_in_fds_f P ctx (map (\<lambda>(cl, f, ty). fd_def cl f) cl_f_ty_list) f = ty_opt_bot_opt None"
by (induct cl_f_ty_list, auto)

lemma ftype_in_fds_some[rule_format]:
  "(cl_f, f, ty_f) \<in> set cl_f_ty_list \<and> distinct (map (\<lambda>(cl, f, ty). f) cl_f_ty_list) \<and> find_type_f P ctx cl_f = Some ty_f
        \<longrightarrow> ftype_in_fds_f P ctx (map (\<lambda>(cl, f, ty). fd_def cl f) cl_f_ty_list) f = ty_opt_bot_opt (Some ty_f)"
apply(induct cl_f_ty_list) apply(simp) apply(clarsimp) apply(safe) apply(force) apply(simp)
apply(frule ftype_in_fds_none) apply(force)
done

lemma no_ty_bot[THEN mp]:
  "(\<forall>x\<in>set cl_f_ty_list. (\<lambda>(cl, f, ty). find_type_f P ctx cl = Some ty) x)
       \<longrightarrow> ftype_in_fds_f P ctx (map (\<lambda>(cl, f, ty). fd_def cl f) cl_f_ty_list) f \<noteq> ty_opt_bot_bot"
apply(induct cl_f_ty_list) apply(simp) apply(clarsimp split: split_if_asm option.splits)
done

lemma field_has_type'[rule_format]:
  "(cl_f, f, ty_f) \<in> set cl_f_ty_list \<and>
   (\<forall>(ctx, cld) \<in> set path. case ctx of ctx_def mi pn \<Rightarrow> (P, mi, cld) \<in> wf_class \<and> package_name_f cld = pn) \<and>
   (ctx_def mi pn, cld_def pn am dcl cl (map (\<lambda>(cl, f, ty). fd_def cl f) cl_f_ty_list) mds) \<in> set path \<and>
   distinct (map (\<lambda>(cl, f, ty). f) cl_f_ty_list) \<and>
   find_type_f P (ctx_def mi pn) cl_f = Some ty_f
           \<longrightarrow> (\<exists>ty'. ftype_in_path_f P path f = Some ty')"
apply(induct path) apply(simp)
apply(simp)
apply(rule) apply(elim conjE) apply(erule disjE)
 apply(clarsimp simp add: class_fields_f_def split: option.splits)
 apply(cut_tac ctx = "ctx_def mi pn" in ftype_in_fds_some) apply(force) apply(simp)
apply(clarsimp split: option.splits ty_opt_bot.splits)
apply(rename_tac ctx cld path ty') apply(case_tac ctx, rename_tac mi' pn', clarsimp)
apply(erule wf_classE) apply(erule wf_class_cE) apply(clarsimp simp add: class_fields_f_def package_name_f_def)
apply(frule no_ty_bot) apply(force)
done

lemma all_in_path_wf_pn:
  "\<lbrakk>P \<in> wf_p; find_path_f P ctx cl = Some path\<rbrakk>
     \<Longrightarrow> (\<forall>(ctx, cld) \<in> set path. case ctx of ctx_def mi pn \<Rightarrow> (P, mi, cld) \<in> wf_class \<and> package_name_f cld = pn)"
apply(clarsimp) apply(rename_tac ctx' cld')
apply(frule all_in_path_found) apply(simp)
apply(case_tac ctx', rename_tac mi pn, clarsimp) apply(frule wf_cld_from_lu) apply(simp) apply(simp)
apply(case_tac cld', rename_tac pn' am dcl cl' fds mds, clarsimp simp add: full_name_f_def)
apply(frule find_cld_pn_match) apply(simp add: package_name_f_def)
done

lemma field_has_type:
  "\<lbrakk>P \<in> wf_p; (P, ty_oid, Some f_list) \<in> fields; f \<in> set f_list\<rbrakk> \<Longrightarrow> \<exists>ty. (P, ty_oid, f, ty) \<in> ftype"
apply(simp) apply(clarsimp simp add: fields_f_def split: option.splits) apply(rename_tac path)
apply(case_tac ty_oid) apply(simp) apply(clarsimp) apply(rename_tac dcl) apply(case_tac ctx, rename_tac mi pn, clarsimp)
apply(frule fields_to_owner) apply(clarsimp) apply(rename_tac ctx' cld cl_f)

apply(frule all_in_path_wf_pn) apply(simp)

apply(frule all_in_path_found) apply(simp) apply(case_tac cld) apply(rename_tac pn' am' dcl' cl' fds' mds')
apply(clarsimp simp add: class_fields_f_def full_name_f_def) apply(case_tac ctx', rename_tac mi' pn'', clarsimp)
apply(drule wf_cld_from_lu) apply(simp)

apply(erule wf_classE) apply(erule wf_class_cE) apply(clarsimp simp add: class_fields_f_def)
apply(rename_tac cl_f ty_f) apply(drule_tac x = "(cl_f, f, ty_f)" in bspec, simp) apply(clarsimp)
apply(simp add: ftype_f_def)
apply(rule_tac cl_f = cl_f and ty_f = ty_f and cl_f_ty_list = cl_f_ty_list and mi = mia and pn = pna and
               dcl = dclb and cl = cla and mds = "(map fst meth_def_meth_list)" and am = am in field_has_type')
apply(frule find_cld_pn_match) apply(simp add: package_name_f_def)
done

lemma exists_three_in_five:
  "var_k \<in> set (map (\<lambda>(y, cl, var, var', v). var) y_cl_var_var'_v_list) \<longrightarrow>
   (\<exists>y cl var' v. (y, cl, var_k, var', v) \<in> set y_cl_var_var'_v_list)"
by (induct y_cl_var_var'_v_list, auto)

lemma map_xx[rule_format]:
  "(y, cl, var_k, var', v) \<in> set y_cl_var_var'_v_list \<longrightarrow>
   (x_var var_k, x_var var') \<in> set (map (\<lambda>(y, cl, var, var', v). (x_var var, x_var var')) y_cl_var_var'_v_list)"
by (induct y_cl_var_var'_v_list, auto)

lemma map_of_vd[rule_format]:
  "\<forall>cl_var_ty_list.
      map (\<lambda>(y, cl, var, var', v). vd_def cl var) y_cl_var_var'_v_list = map (\<lambda>(cl, var, ty). vd_def cl var) cl_var_ty_list
      \<longrightarrow> map (\<lambda>(y, cl, var, var', v). var) y_cl_var_var'_v_list = map (\<lambda>(cl, var, ty). var) cl_var_ty_list"
by (induct y_cl_var_var'_v_list, auto)

lemma mem_vd:
  "vd_def cl_k var_k \<in> set (map (\<lambda>(y, cl, var, var', v). vd_def cl var) y_cl_var_var'_v_list) \<longrightarrow>
   var_k \<in> set (map (\<lambda>(y, cl, var, var', v). var) y_cl_var_var'_v_list)"
by (induct y_cl_var_var'_v_list, auto)

lemma exists_var':
  "\<lbrakk>distinct (map (\<lambda>(cl, var, ty). var) cl_var_ty_list);
    map (\<lambda>(y, cl, var, var', v). var) y_cl_var_var'_v_list = map (\<lambda>(cl, var, ty). var) cl_var_ty_list;
    map_of (map (\<lambda>(cl, var, ty). (x_var var, ty)) cl_var_ty_list) var_k = Some ty_k\<rbrakk>
      \<Longrightarrow> \<exists>var'_k. map_of (map (\<lambda>(y, cl, var, var', v). (x_var var, x_var var')) y_cl_var_var'_v_list) var_k = Some (x_var var'_k)"
apply(drule map_of_is_SomeD) apply(clarsimp) apply(rename_tac cl_k var_k)
apply(subgoal_tac "var_k \<in> set (map (\<lambda>(y, cl, var, var', v). var) y_cl_var_var'_v_list)")
 prefer 2 apply(force)
apply(simp (no_asm_use)) apply(clarify) apply(rename_tac y_k cl_k' var_k var'_k v_k)
apply(rule_tac x = var'_k in exI)
apply(rule map_of_is_SomeI)
 apply(drule distinct_var, assumption+)
apply(rule map_xx, assumption)
done

lemma map_y:
  "\<lbrakk>((y_k, cl_k, var_k, var'_k, v_k), y'_k, ty_k) \<in> set (zip y_cl_var_var'_v_list y_ty_list);
    map (\<lambda>(y, cl, var, var', v). y) y_cl_var_var'_v_list = map fst y_ty_list\<rbrakk>
      \<Longrightarrow> (y_k, ty_k) \<in> set y_ty_list"
apply(clarsimp simp add: set_zip)
apply(drule_tac f = "\<lambda>(y, cl, var, var', v). y" in arg_cong)
apply(drule_tac f1 = "\<lambda>(y, cl, var, var', v). y" in nth_map[THEN sym])
apply(frule_tac f = "\<lambda>(y, ty). y" in arg_cong)
apply(case_tac "y_ty_list ! i")
apply(force simp add: in_set_conv_nth)
done

lemma set_zip_var'_v:
  "\<lbrakk>((y_k, cl_k, var_k, var'_k, v_k), y'_k, ty_k) \<in> set (zip y_cl_var_var'_v_list y_ty_list)\<rbrakk>
       \<Longrightarrow> (x_var var'_k, v_k) \<in> set (map (\<lambda>(y, cl, var, var', y). (x_var var', y)) y_cl_var_var'_v_list)"
apply(subgoal_tac "(y_k, cl_k, var_k, var'_k, v_k) \<in> set y_cl_var_var'_v_list")
by (force simp add: set_zip)+

lemma map_of_map_zip_none:
  "\<lbrakk>map (\<lambda>(y, cl, var, var', v). y) y_cl_var_var'_v_list = map fst y_ty_list;
    map_of (map (\<lambda>((y, cl, var, var', v), y', y). (x_var var', y)) (zip y_cl_var_var'_v_list y_ty_list)) x_G = None\<rbrakk>
      \<Longrightarrow> map_of (map (\<lambda>(y, cl, var, var', y). (x_var var', y)) y_cl_var_var'_v_list) x_G = None"
apply(drule map_length_y)
apply(clarsimp simp add: map_of_eq_None_iff)
apply(erule contrapos_np)
apply(simp only: set_map[THEN sym] fst_zip_eq)
by force

lemma map_of_map_zip_some:
  "\<lbrakk>distinct (map (\<lambda>(y, cl, var, var', v). var') y_cl_var_var'_v_list);
    map (\<lambda>(y, cl, var, var', v). y) y_cl_var_var'_v_list = map fst y_ty_list;
    map_of (map (\<lambda>((y, cl, var, var', v), y', y). (x_var var', y)) (zip y_cl_var_var'_v_list y_ty_list)) x_G = Some ty_k\<rbrakk>
      \<Longrightarrow> \<exists>v_k. map_of (map (\<lambda>(y, cl, var, var', y). (x_var var', y)) y_cl_var_var'_v_list) x_G = Some v_k"
apply(drule map_of_is_SomeD)
apply(clarsimp) apply(rename_tac y cl var var' v y')
apply(subgoal_tac "(y, cl, var, var', v) \<in> set y_cl_var_var'_v_list")
 prefer 2 apply(force simp add: set_zip)
apply(rule_tac x = v in exI)
apply(rule map_of_is_SomeI)
 apply(simp only: map_fst_two' distinct_x_var')
by force

lemma x'_not_in_list:
  "\<lbrakk>(y_k, cl_k, var_k, var'_k, v_k) \<in> set y_cl_var_var'_v_list;
    x' \<notin> (\<lambda>(y, cl, var, var', v). x_var var') ` set y_cl_var_var'_v_list\<rbrakk>
      \<Longrightarrow> x_var var'_k \<noteq> x'"
by (erule contrapos_nn, force)

lemma nth_in_set:
  "\<lbrakk>i < length y_ty_list; map fst y_ty_list ! i = y_k\<rbrakk> \<Longrightarrow> y_k \<in> set (map fst y_ty_list)"
apply(subgoal_tac "\<exists>i<length (map fst y_ty_list). map fst y_ty_list ! i = y_k")
 prefer 2 apply(rule_tac x = i in exI) apply(clarsimp)
apply(simp only: in_set_conv_nth[THEN sym])
done

lemma map_one_in_two:
  "y_k \<in> set (map fst y_ty_list) \<longrightarrow> (\<exists>ty. (y_k, ty) \<in> set y_ty_list)"
by (induct y_ty_list, auto)

lemma exists_i: (* can probably simplify a lot *)
  "\<lbrakk>distinct (map (\<lambda>(cl, var, ty). var) cl_var_ty_list);
    (y_k, cl_ka, var_k, var'_k, v_k) \<in> set y_cl_var_var'_v_list;
    (cl_k, var_k, ty_k) \<in> set cl_var_ty_list;
     map (\<lambda>(y, cl, var, var', v). var) y_cl_var_var'_v_list = map (\<lambda>(cl, var, ty). var) cl_var_ty_list\<rbrakk> \<Longrightarrow>
        \<exists>i < length cl_var_ty_list. cl_var_ty_list ! i = (cl_k, var_k, ty_k) \<and> y_cl_var_var'_v_list ! i = (y_k, cl_ka, var_k, var'_k, v_k)"
apply(simp only: in_set_conv_nth) apply(erule exE) back apply(erule conjE)
apply(rule_tac x = i in exI)
apply(simp)
apply(drule_tac f = "\<lambda>(cl, var, ty). var" in arg_cong)
apply(frule_tac f1 = "\<lambda>(cl, var, ty). var" in nth_map[THEN sym])
apply(drule_tac t = "map (\<lambda>(cl, var, ty). var) cl_var_ty_list ! i" in sym)
apply(drule_tac s = "(\<lambda>(cl, var, ty). var) (cl_var_ty_list ! i)" in trans)
apply(simp)
apply(thin_tac ?P) back back back back
apply(drule sym)
apply(simp)
apply(erule exE) apply(rename_tac j) apply(erule conjE)
apply(simp only: distinct_conv_nth)
apply(erule_tac x = i in allE)
apply(drule sym) back
apply(drule map_length_var)
apply(simp)
apply(erule_tac x = j in allE)
apply(simp)
done

lemma y_ty_match:
  "\<lbrakk>i < length cl_var_ty_list; cl_var_ty_list ! i = (cl_k, var_k, ty_k);
    y_cl_var_var'_v_list ! i = (y_k, cl_ka, var_k, var'_k, v_k);
    map (\<lambda>(y, cl, var, var', v). y) y_cl_var_var'_v_list = map fst y_ty_list;
    map (\<lambda>(cl, var, ty). ty) cl_var_ty_list = map snd y_ty_list\<rbrakk> \<Longrightarrow>
       y_ty_list ! i = (y_k, ty_k)"
apply(drule_tac f = "\<lambda>(cl, var, ty). ty" in arg_cong)
apply(frule_tac f1 = "\<lambda>(cl, var, ty). ty" in nth_map[THEN sym])
apply(drule_tac t = "map (\<lambda>(cl, var, ty). ty) cl_var_ty_list ! i" in sym)
apply(frule map_length_y) apply(frule map_length_ty)
apply(drule_tac t = "length y_ty_list" in sym) apply(simp)
apply(drule_tac f = "\<lambda>(y, cl, var, var', v). y" in arg_cong)
apply(frule_tac f1 = "\<lambda>(y, cl, var, var', v). y" in nth_map[THEN sym])
apply(drule_tac t = "map (\<lambda>(y, cl, var, var', v). y) y_cl_var_var'_v_list ! i" in sym)
apply(case_tac "y_ty_list ! i") apply(simp)
done

lemma map_of_ty_k:
  "\<lbrakk>distinct (map (\<lambda>(cl, var, ty). var) cl_var_ty_list);
    distinct (map (\<lambda>(y, cl, var, var', v). var') y_cl_var_var'_v_list);
    (y_k, cl_ka, var_k, var'_k, v_k) \<in> set y_cl_var_var'_v_list;
    (cl_k, var_k, ty_k) \<in> set cl_var_ty_list;
     map (\<lambda>(y, cl, var, var', v). y) y_cl_var_var'_v_list = map fst y_ty_list;
     map (\<lambda>(cl, var, ty). ty) cl_var_ty_list = map snd y_ty_list;
     map (\<lambda>(y, cl, var, var', v). var) y_cl_var_var'_v_list = map (\<lambda>(cl, var, ty). var) cl_var_ty_list\<rbrakk>
       \<Longrightarrow> map_of (map (\<lambda>((y, cl, var, var', v), y', y). (x_var var', y)) (zip y_cl_var_var'_v_list y_ty_list)) (x_var var'_k) = Some ty_k"
apply(frule map_length_y)
apply(rule map_of_is_SomeI)
 apply(simp only: fst_zip_eq)
 apply(simp only: distinct_x_var')
apply(clarsimp)

apply(frule map_length_var)

apply(frule exists_i, simp+) apply(erule exE)
apply(drule_tac t = "length y_ty_list" in sym) apply(clarsimp)
apply(frule y_ty_match, assumption+)

apply(subgoal_tac "zip y_cl_var_var'_v_list y_ty_list ! i = (y_cl_var_var'_v_list ! i,  y_ty_list ! i)")
 prefer 2 apply(rule nth_zip) apply(simp) apply(simp)

apply(drule_tac f = "\<lambda>((y, cl, var, var', v), y', y). (x_var var', y)" in arg_cong)
apply(subgoal_tac "i < length (zip y_cl_var_var'_v_list y_ty_list)")
 prefer 2 apply(force) (* simplify *)

apply(frule_tac f1 = "\<lambda>((y, cl, var, var', v), y', y). (x_var var', y)" in nth_map[THEN sym])
apply(drule_tac t = "map (\<lambda>((y, cl, var, var', v), y', y). (x_var var', y)) (zip y_cl_var_var'_v_list y_ty_list) ! i" in sym)
apply(drule_tac s = "(\<lambda>((y, cl, var, var', v), y', y). (x_var var', y)) (zip y_cl_var_var'_v_list y_ty_list ! i)" in trans)
apply(simp)

apply(subgoal_tac "\<exists>j<length (map (\<lambda>((y, cl, var, var', v), y', y). (x_var var', y)) (zip y_cl_var_var'_v_list y_ty_list)). map (\<lambda>((y, cl, var, var', v), y', y). (x_var var', y)) (zip y_cl_var_var'_v_list y_ty_list) ! j = (x_var var'_k, ty_k)")
 prefer 2 apply(rule_tac x = i in exI) apply(simp)
apply(simp only: in_set_conv_nth[THEN sym])
apply(simp)
done

lemma map_of_ty_k':
  "\<lbrakk>distinct (map (\<lambda>(cl, var, ty). var) cl_var_ty_list); distinct (map (\<lambda>(y, cl, var, var', v). var') y_cl_var_var'_v_list);
     x' \<notin> (\<lambda>(y, cl, var, var', v). x_var var') ` set y_cl_var_var'_v_list; map fst y_cl_var_var'_v_list = map fst y_ty_list;
     map (\<lambda>(cl, var, ty). ty) cl_var_ty_list = map snd y_ty_list; map (\<lambda>(y, cl, var, u). var) y_cl_var_var'_v_list = map (\<lambda>(cl, var, ty). var) cl_var_ty_list;
     map_of (map (\<lambda>(cl, var, y). (x_var var, y)) cl_var_ty_list) (x_var var) = Some ty_var\<rbrakk>
    \<Longrightarrow> (if x_var (option_case var (x_case (\<lambda>var'. var') var) (map_of (map (\<lambda>(y, cl, var, var', v). (x_var var, x_var var')) y_cl_var_var'_v_list) (x_var var))) = x' then Some ty_x_m
        else (G ++ map_of (map (\<lambda>((y, cl, var, var', v), y', y). (x_var var', y)) (zip y_cl_var_var'_v_list y_ty_list)))
              (x_var (option_case var (x_case (\<lambda>var'. var') var)
                       (map_of (map (\<lambda>(y, cl, var, var', v). (x_var var, x_var var')) y_cl_var_var'_v_list) (x_var var))))) =
       Some ty_var"
apply(frule exists_var') apply(simp add: weaken_list_var) apply(simp) apply(clarsimp split del: split_if) apply(clarsimp)
apply(drule map_of_is_SomeD)+ apply(clarsimp split del: split_if) apply(frule x'_not_in_list, simp+)
apply(frule map_of_ty_k) apply(simp add: weaken_list_y weaken_list_var)+
done

lemma var_not_var'_x':
  "\<lbrakk>G (x_var var) = Some ty_var; L (x_var var) = Some v_var;
    \<forall>x\<in>set y_cl_var_var'_v_list. L (x_var ((\<lambda>(y, cl, var, var', v). var') x)) = None; L x' = None\<rbrakk>
    \<Longrightarrow> (G ++ map_of (map (\<lambda>((y, cl, var, var', v), y', y). (x_var var', y)) (zip y_cl_var_var'_v_list y_ty_list)) ++ empty(x' \<mapsto> ty_x_d)) (x_var var) = Some ty_var"
apply(subgoal_tac "x_var var \<noteq> x'") prefer 2 apply(force)
apply(simp add: map_add_def)
apply(subgoal_tac "map_of (map (\<lambda>((y, cl, var, var', v), y', y). (x_var var', y)) (zip y_cl_var_var'_v_list y_ty_list)) (x_var var) = None")
 apply(simp)
apply(clarsimp simp add: map_of_eq_None_iff set_zip)
apply(rename_tac y_k cl_k var_k v_k y'_k ty_k i)
apply(drule_tac x = "(y_k, cl_k, var_k, var, v_k)" in bspec, simp)
apply(force)
done

lemma same_el:
  "\<lbrakk>distinct (map (\<lambda>(y, cl, var, var', v). var') y_cl_var_var'_v_list);
    i < length y_cl_var_var'_v_list;
    (y_i, cl_i, var_i, var'_i, v_i) = y_cl_var_var'_v_list ! i;
    (y_j, cl_j, var_j, var'_i, v_j) \<in> set y_cl_var_var'_v_list\<rbrakk>
       \<Longrightarrow> (y_i, cl_i, var_i, var'_i, v_i) = (y_j, cl_j, var_j, var'_i, v_j)"
apply(simp only: in_set_conv_nth) apply(clarsimp) apply(rename_tac j)
apply(simp only: distinct_conv_nth)
apply(erule_tac x = i in allE) apply(simp)
apply(erule_tac x = j in allE) apply(simp)
apply(drule sym) apply(simp)
done

lemma same_y:
  "\<lbrakk>map (\<lambda>(y, cl, var, var', v). y) y_cl_var_var'_v_list = map fst y_ty_list;
    i < length y_cl_var_var'_v_list;
    (y'_k, ty_k) = y_ty_list ! i; y_cl_var_var'_v_list ! i = (y_k, cl_k, var_k, var'_k, v_k)\<rbrakk>
        \<Longrightarrow> y'_k = y_k"
apply(drule_tac f = "\<lambda>(y, cl, var, var', v). y" in arg_cong)
apply(frule_tac f1 = "\<lambda>(y, cl, var, var', v). y" in nth_map[THEN sym])
apply(drule_tac f = fst in arg_cong) apply(simp)
apply(frule map_length_y) apply(simp)
done

lemma map_map_zip_y':
  "map fst y_y'_list = map fst y_ty_list \<Longrightarrow>
   map snd y_y'_list = map fst (map (\<lambda>((y, y'), yy, ty). (y', ty)) (zip y_y'_list y_ty_list))"
apply(rule nth_equalityI)
 apply(induct y_y'_list) apply(simp) apply(clarsimp) apply(frule map_length_y') apply(simp)
apply(clarsimp)
apply(case_tac "y_y'_list ! i")
apply(case_tac "y_ty_list ! i")
apply(clarsimp)
apply(subgoal_tac "i < length (map (\<lambda>((y, y'), yy, ty). (y', ty)) (zip y_y'_list y_ty_list))")
 apply(frule_tac f = fst and xs = "map (\<lambda>((y, y'), yy, ty). (y', ty)) (zip y_y'_list y_ty_list)" in nth_map)
 apply(simp)
apply(subgoal_tac "length (map (\<lambda>((y, y'), yy, ty). (y', ty)) list) = length list")
 apply(simp) apply(frule map_length_y') apply(simp)
apply(simp only: map_length_list)
done

lemma map_map_zip_ty:
  "map fst y_y'_list = map fst y_ty_list \<Longrightarrow>
   map snd (map (\<lambda>((y, y'), yy, ty). (y', ty)) (zip y_y'_list y_ty_list)) = map snd y_ty_list"
apply(frule map_length_y')
apply(rule nth_equalityI)
 apply(induct y_ty_list) apply(simp) apply(simp)
apply(clarsimp)
apply(case_tac "y_y'_list ! i")
apply(case_tac "y_ty_list ! i")
apply(simp)
done

lemma map_y_yy:
  "\<lbrakk>i < length y_y'_list; i < length y_ty_list;
    map fst y_y'_list = map fst y_ty_list;
    y_y'_list ! i = (y, y'); y_ty_list ! i = (yy, ty)\<rbrakk> \<Longrightarrow>
       y = yy"
apply(drule_tac f = fst in arg_cong)
apply(frule_tac f1 = fst in nth_map[THEN sym])
by simp


lemma var_k_of_ty_k:
  "\<lbrakk>distinct (map (\<lambda>(cl, var, ty). var) cl_var_ty_list); distinct (map (\<lambda>(y, cl, var, var', v). var') y_cl_var_var'_v_list);
    x' \<notin> (\<lambda>(y, cl, var, var', v). x_var var') ` set y_cl_var_var'_v_list;
    map fst y_cl_var_var'_v_list = map fst y_ty_list;
    map (\<lambda>(cl, var, ty). ty) cl_var_ty_list = map snd y_ty_list;
    map (\<lambda>(y, cl, var, u). var) y_cl_var_var'_v_list = map (\<lambda>(cl, var, ty). var) cl_var_ty_list;
    (if x = x_this then Some ty_x_m else map_of (map (\<lambda>(cl, var, y). (x_var var, y)) cl_var_ty_list) x) = Some ty_x\<rbrakk>
       \<Longrightarrow> (if (case if x = x_this then Some x' else map_of (map (\<lambda>(y, cl, var, var', v). (x_var var, x_var var')) y_cl_var_var'_v_list) x of None \<Rightarrow> x | Some x' \<Rightarrow> x') = x'
           then Some ty_x_m
           else (G ++ map_of (map (\<lambda>((y, cl, var, var', v), y', y). (x_var var', y)) (zip y_cl_var_var'_v_list y_ty_list)))
                 (case if x = x_this then Some x' else map_of (map (\<lambda>(y, cl, var, var', v). (x_var var, x_var var')) y_cl_var_var'_v_list) x of None \<Rightarrow> x | Some x' \<Rightarrow> x')) =
          Some ty_x"
apply(clarsimp) apply(rule) apply(rule) apply(simp) apply(clarsimp)
apply(frule exists_var') apply(simp add: weaken_list_var) apply(simp) apply(clarsimp split del: split_if)
apply(drule map_of_is_SomeD)+ apply(clarsimp split del: split_if) apply(frule x'_not_in_list, simp+)
apply(frule map_of_ty_k) apply(simp add: weaken_list_y weaken_list_var)+
done

lemma x_var_not_this: "(if x_var var = x_this then Some x' else Q) = Q" by simp

lemma subtype_through_tr:
  "\<lbrakk>distinct (map (\<lambda>(cl, var, ty). var) cl_var_ty_list); distinct (map (\<lambda>(y, cl, var, var', v). var') y_cl_var_var'_v_list);
    x' \<notin> (\<lambda>(y, cl, var, var', v). x_var var') ` set y_cl_var_var'_v_list;
    map fst y_cl_var_var'_v_list = map fst y_ty_list;
    map (\<lambda>(cl, var, ty). ty) cl_var_ty_list = map snd y_ty_list;
    map (\<lambda>(y, cl, var, u). var) y_cl_var_var'_v_list = map (\<lambda>(cl, var, ty). var) cl_var_ty_list;
    is_sty_one P ty_x ty_var = Some True; (if x = x_this then Some ty_x_m else map_of (map (\<lambda>(cl, var, y). (x_var var, y)) cl_var_ty_list) x) = Some ty_x;
    map_of (map (\<lambda>(cl, var, y). (x_var var, y)) cl_var_ty_list) (x_var var) = Some ty_var\<rbrakk>
       \<Longrightarrow> (P, if (case if x = x_this then Some x' else map_of (map (\<lambda>(y, cl, var, var', v). (x_var var, x_var var')) y_cl_var_var'_v_list) x of None \<Rightarrow> x | Some x' \<Rightarrow> x') =
                 x'
              then Some ty_x_m
              else (G ++ map_of (map (\<lambda>((y, cl, var, var', v), y', y). (x_var var', y)) (zip y_cl_var_var'_v_list y_ty_list)))
                    (case if x = x_this then Some x' else map_of (map (\<lambda>(y, cl, var, var', v). (x_var var, x_var var')) y_cl_var_var'_v_list) x of None \<Rightarrow> x | Some x' \<Rightarrow> x'),
           if x_var (option_case var (x_case (\<lambda>var'. var') var) (map_of (map (\<lambda>(y, cl, var, var', v). (x_var var, x_var var')) y_cl_var_var'_v_list) (x_var var))) = x' then Some ty_x_m
           else (G ++ map_of (map (\<lambda>((y, cl, var, var', v), y', y). (x_var var', y)) (zip y_cl_var_var'_v_list y_ty_list)))
                 (x_var (option_case var (x_case (\<lambda>var'. var') var)
                          (if x_var var = x_this then Some x' else map_of (map (\<lambda>(y, cl, var, var', v). (x_var var, x_var var')) y_cl_var_var'_v_list) (x_var var)))))
          \<in> sty_option"
apply(rule_tac ty = ty_x and ty' = ty_var in sty_optionI)
  apply(simp add: var_k_of_ty_k)
 apply(simp only: x_var_not_this) apply(rule map_of_ty_k') apply(simp+)
done

lemma subtypes_through_tr:
  "\<lbrakk>distinct (map (\<lambda>(cl, var, ty). var) cl_var_ty_list); distinct (map (\<lambda>(y, cl, var, var', v). var') y_cl_var_var'_v_list);
    x' \<notin> (\<lambda>(y, cl, var, var', v). x_var var') ` set y_cl_var_var'_v_list; map fst y_cl_var_var'_v_list = map fst y_ty_list;
    map (\<lambda>(cl, var, ty). ty) cl_var_ty_list = map snd y_ty_list; map (\<lambda>(y, cl, var, u). var) y_cl_var_var'_v_list = map (\<lambda>(cl, var, ty). var) cl_var_ty_list;
    \<forall>x\<in>set y_y'_list. split (\<lambda>y. op = (case if y = x_this then Some x' else map_of (map (\<lambda>(y, cl, var, var', v). (x_var var, x_var var')) y_cl_var_var'_v_list) y of
                                       None \<Rightarrow> y | Some x' \<Rightarrow> x')) x;
    \<forall>x\<in>set y_ty_lista. (\<lambda>(y, ty). (P, if y = x_this then Some ty_x_m else map_of (map (\<lambda>(cl, var, y). (x_var var, y)) cl_var_ty_list) y, Some ty) \<in> sty_option) x;
    map fst y_y'_list = map fst y_ty_lista; (y, y') = y_y'_list ! i; (yy, ty) = y_ty_lista ! i; i < length y_y'_list; i < length y_ty_lista\<rbrakk> \<Longrightarrow>
     (P, if y' = x' then Some ty_x_m else (G ++ map_of (map (\<lambda>((y, cl, var, var', v), y', y). (x_var var', y)) (zip y_cl_var_var'_v_list y_ty_list))) y', Some ty) \<in> sty_option"
apply(drule_tac x = "(y, y')" in bspec, simp) apply(drule_tac x = "(yy, ty)" in bspec, simp) apply(clarsimp split del: split_if)
apply(frule_tac y_ty_list = y_ty_lista in map_y_yy, assumption+) apply(erule sty_option.cases) apply(clarsimp split del: split_if)
apply(rule_tac ty = tya in sty_optionI, (simp add: var_k_of_ty_k)+)
done

lemma map_override_get:
  "(G ++ (\<lambda>u. if u = x' then Some ty_x_d else None)) x' = Some ty_x_d"
apply(simp add: map_add_def)
done

lemma s_induct':
  "\<lbrakk>\<And>ss. \<forall>s\<in>set ss. P s \<Longrightarrow> P (s_block ss); \<And>list x. P (s_ass list x); \<And>list1 x list2. P (s_read list1 x list2); \<And>x1 list x2. P (s_write x1 list x2);
    \<And>x1 x2 s1 s2. \<lbrakk>P s1; P s2\<rbrakk> \<Longrightarrow> P (s_if x1 x2 s1 s2); \<And>list1 x list2 list3. P (s_call list1 x list2 list3); \<And>list ctx cl. P (s_new list ctx cl)\<rbrakk>
         \<Longrightarrow> P s"
apply(cut_tac s.induct[of "\<lambda>ss. (\<forall>s\<in>set ss. P s)" P]) apply(simp_all) apply(force) done

lemma wf_tr_stmt_in_G':
  "\<forall>s'. distinct (map (\<lambda>(cl, var, ty). var) cl_var_ty_list)
    \<and> distinct (map (\<lambda>(y, cl, var, var', v). var') y_cl_var_var'_v_list)
    \<and> x' \<notin> (\<lambda>(y, cl, var, var', v). x_var var') ` set y_cl_var_var'_v_list
    \<and> map (\<lambda>(y, cl, var, var', v). y) y_cl_var_var'_v_list = map fst y_ty_list
    \<and> map (\<lambda>(cl, var, ty). ty) cl_var_ty_list = map snd y_ty_list
    \<and> map (\<lambda>(y, cl, var, var', v). var) y_cl_var_var'_v_list = map (\<lambda>(cl, var, ty). var) cl_var_ty_list
    \<and> is_sty_one P ty_x_d ty_x_m = Some True
    \<and> (P, map_of (map (\<lambda>(cl, var, ty). (x_var var, ty)) cl_var_ty_list)(x_this \<mapsto> ty_x_m), s') \<in> wf_stmt
    \<and> (map_of (map (\<lambda>(y, cl, var, var', v). (x_var var, x_var var')) y_cl_var_var'_v_list)(x_this \<mapsto> x'), s', s'') \<in> tr_s
    \<longrightarrow> (P, (G ++ map_of (map (\<lambda>((y, cl, var, var', v), y', y). (x_var var', y)) (zip y_cl_var_var'_v_list y_ty_list)))(x' \<mapsto> ty_x_m), s'') \<in> wf_stmt"
apply(rule s_induct')

apply(clarsimp)
apply(erule tr_s.cases, simp_all) apply(clarsimp)
apply(erule wf_stmtE, simp_all) apply(clarsimp)
apply(rule wf_blockI) apply(clarsimp) apply(rename_tac s'_s''_list s' s'')
apply(drule_tac x = "(s', s'')" in bspec, simp)+ apply(clarsimp)

apply(clarsimp) apply(rename_tac var x s')
apply(erule tr_s.cases, simp+) apply(erule wf_stmtE, simp_all)
apply(erule sty_option.cases) apply(rule wf_var_assignI) apply(clarsimp split del: split_if)
apply(rule_tac ty_x = ty in subtype_through_tr, simp+)

apply(clarsimp) apply(rename_tac var x f s')
apply(erule tr_s.cases, simp+) apply(erule wf_stmtE, simp_all)
apply(erule sty_option.cases) apply(clarsimp split del: split_if) apply(rename_tac f ty_x var x ty_f ty_var)
apply(rule wf_field_readI) apply(simp add: var_k_of_ty_k) apply(simp)
apply(rule_tac ty' = ty_var in sty_optionI) apply(simp) apply(rule map_of_ty_k', simp+)

apply(clarsimp) apply(rename_tac x f y s')
apply(erule tr_s.cases, simp+) apply(erule wf_stmtE, simp_all)
apply(erule sty_option.cases) apply(clarsimp split del: split_if) apply(rename_tac f ty_x x y ty_y ty_f)
apply(rule wf_field_writeI) apply(simp add: var_k_of_ty_k) apply(simp)
apply(rule sty_optionI, (simp add: var_k_of_ty_k)+)

apply(clarsimp) apply(rename_tac x y s1 s2 s')
apply(erule tr_s.cases, simp+) apply(erule wf_stmtE, simp_all) apply(rule wf_ifI)
  apply(erule disjE)
   apply(rule disjI1) apply(erule sty_option.cases) apply(clarsimp split del: split_if)
   apply(rule sty_optionI, (simp add: var_k_of_ty_k split del: split_if)+)
  apply(rule disjI2) apply(erule sty_option.cases) apply(clarsimp split del: split_if)
  apply(rule sty_optionI, (simp add: var_k_of_ty_k)+)
 apply(clarsimp)
apply(clarsimp)

apply(clarsimp) apply(rename_tac var x meth ys s')
apply(erule tr_s.cases, simp+) apply(erule wf_stmtE, simp_all) apply(clarsimp split del: split_if)
apply(rule_tac y_ty_list = "map (\<lambda>((y, y'), (yy, ty)). (y', ty)) (zip y_y'_list y_ty_lista)" in wf_mcallI)
    apply(simp add: map_map_zip_y')
   apply(simp add: var_k_of_ty_k)
  apply(simp add: map_map_zip_ty)
 apply(clarsimp simp add: set_zip split del: split_if) apply(simp add: subtypes_through_tr)
apply(erule sty_option.cases) apply(clarsimp split del: split_if) apply(rule sty_optionI, (simp add: map_of_ty_k')+)

apply(clarsimp) apply(rename_tac var ctx cl s')
apply(erule tr_s.cases, simp+) apply(erule wf_stmtE, simp_all) apply(clarsimp)
apply(rule wf_newI) apply(simp)
apply(erule sty_option.cases) apply(clarsimp split del: split_if) apply(rule sty_optionI, (simp add: map_of_ty_k')+)

done

lemma wf_object_heap:
  "\<lbrakk>(P, H, v_opt, Some ty') \<in> wf_object; is_sty_one Pa ty_y_s ty_f = Some True; H oid_x = Some (ty_x_d, fs_oid)\<rbrakk>
     \<Longrightarrow> (P, H(oid_x \<mapsto> (ty_x_d, fs_oid(f \<mapsto> v))), v_opt, Some ty') \<in> wf_object"
apply(erule wf_objectE) apply(clarsimp)
 apply(rule wf_nullI, simp)
apply(erule sty_option.cases) apply(clarsimp split: option.splits)
apply(rule wf_objectI) apply(force intro: sty_optionI)
done

lemma not_dom_is_none:
  "((\<lambda>(y, cl, var, var', v). x_var var') ` set y_cl_var_var'_v_list \<inter> Map.dom L = {})
     \<Longrightarrow> (\<forall>x\<in>set y_cl_var_var'_v_list. (\<lambda>(y, cl, var, var', v). L (x_var var') = None) x)"
by force

lemma type_to_val:
  "\<lbrakk>(P, G, H, L) \<in> wf_varstate; (P, G x, G y) \<in> sty_option\<rbrakk> \<Longrightarrow> \<exists>v w. L x = Some v \<and> L y = Some w"
apply(erule sty_option.cases) apply(clarsimp) apply(erule wf_varstateE)
apply(frule_tac x = x in bspec, simp add: domI) apply(drule_tac x = y in bspec, simp add: domI)
apply(elim wf_objectE) by (simp+)

lemma find_path_fields[THEN mp]:
  "find_path_ty_f P ty = Some path \<longrightarrow> (\<exists>fs. fields_in_path_f path = fs)"
by (force)

lemma replicate_eq_length:
  "replicate x c = replicate y c \<Longrightarrow> x = y"
apply(subgoal_tac "length (replicate x c) = length (replicate y c)") apply(thin_tac ?P)
apply(subgoal_tac "length (replicate x c) = x")
apply(subgoal_tac "length (replicate y c) = y")
by simp_all


lemma string_infinite:
  "infinite (UNIV :: string set)"
apply(simp add: infinite_iff_countable_subset)
apply(rule_tac x = "\<lambda>n. replicate n c" in exI) apply(rule linorder_injI)
apply(clarify) apply(frule replicate_eq_length) apply(simp)
done

lemma x_infinite:
  "infinite (UNIV :: x set)"
apply(simp add: infinite_iff_countable_subset)
apply(rule_tac x = "\<lambda>n. if n = 0 then x_this else x_var (replicate n c)" in exI)
apply(rule linorder_injI) apply(clarsimp)
done

lemma fresh_oid:
  "(P, H) \<in> wf_heap \<Longrightarrow> (\<exists>oid. oid \<notin> dom H)"
apply(erule wf_heapE) apply(clarsimp)
apply(cut_tac nat_infinite) apply(frule_tac A = "dom H" in ex_new_if_finite)
apply(assumption) apply(simp)
done

lemma fresh_x:
  "finite A \<Longrightarrow> \<exists>x::x. x \<notin> A"
apply(cut_tac x_infinite) apply(frule_tac A = A in ex_new_if_finite)
apply(assumption) apply(simp)
done

lemma fresh_var_not_in_list:
  "finite (A::x set) \<Longrightarrow> \<exists>var::var. x_var var \<notin> A \<and> var \<notin> set list"
apply(cut_tac x_infinite) apply(subgoal_tac "finite (insert x_this A)")
apply(frule_tac F = "insert x_this A" and G = "x_var ` set list" in finite_UnI) apply(simp)
apply(frule_tac A = "insert x_this A \<union> x_var ` set list" in ex_new_if_finite)
apply(assumption) apply(erule exE) apply(clarsimp) apply(case_tac a) apply(force+)
done

lemma fresh_vars[rule_format]:
  "finite (A::x set) \<longrightarrow> (\<exists>list::var list. length list = i \<and> x_var` set list \<inter> A = {} \<and> distinct list)"
apply(induct i) apply(simp)
apply(clarsimp) apply(frule fresh_var_not_in_list) apply(erule exE)
apply(rule_tac x = "var#list" in exI) apply(simp)
done

lemma fresh_x_not_in_vars':
  "finite A \<Longrightarrow> \<exists>x'. x' \<notin> A \<and> x' \<notin> (x_var ` set vars')"
apply(subgoal_tac "finite (x_var ` set vars')") apply(frule_tac G = "x_var ` set vars'" in finite_UnI) apply(assumption)
apply(cut_tac x_infinite) apply(frule_tac A = "A \<union> x_var ` set vars'" in ex_new_if_finite)
apply(simp) apply(simp) apply(simp)
done

lemma lift_opts_ft_length[rule_format]:
  "\<forall>tys. lift_opts (map (vd_case (\<lambda>clk vark. find_type_f P ctx_o clk)) vds) = Some tys \<longrightarrow> length tys = length vds"
by (induct vds, auto split: vd.splits option.splits)

lemma mtype_to_find_md:
  "\<lbrakk>P \<in> wf_p; mtype_f P ty_x_s m = Some (mty_def tys ty_r); is_sty_one P ty_x_d ty_x_s = Some True\<rbrakk> \<Longrightarrow>
      \<exists>ctx cl_r vds ss' y. find_meth_def_f P ty_x_d m = Some (ctx, meth_def_def (meth_sig_def cl_r m vds) (meth_body_def ss' y))
                       \<and> length tys = length vds"
apply(clarsimp simp add: is_sty_one_def split: option.splits ty.splits)
 apply(clarsimp simp add: mtype_f_def find_meth_def_f_def)
apply(case_tac ty_x_d) apply(clarsimp split: ctx.splits option.splits) apply(rename_tac path_d ctx_s dcl_s ctx_d dcl_d)
apply(clarsimp) apply(case_tac ctx_d, rename_tac mi_d pn_d, clarsimp) apply(case_tac ctx_s, rename_tac mi_s pn_s, clarsimp)
apply(clarsimp split: option.splits) apply(rename_tac ctx_s cld_s)
apply(clarsimp simp add: mtype_f_def split: option.splits meth_def.splits meth_sig.splits) apply(rename_tac ctx_m mb cl_r m' vds)
apply(frule lift_opts_ft_length)
apply(clarsimp simp add: find_meth_def_f_def split: option.splits) apply(rename_tac path_s)
apply(frule_tac ctx = "ctx_def mi_s pn_s" in fpr_target_is_head) apply(clarsimp)
apply(frule fp_same_ctx) apply(case_tac path_d) apply(simp) apply(rename_tac ctxcld path_d)
apply(clarify) apply(rename_tac ctx_1 cld_1 path_d) apply(frule fp_same_ctx)
apply(frule_tac mty = "mty_def tys ty_r" and m = m in mty_preservation') apply(simp) apply(simp)
 apply(simp add: mtype_f_def find_meth_def_f_def) apply(case_tac ctx_s, rename_tac mi_s' pn_s', clarsimp)
 apply(case_tac cld_s, rename_tac pn_s'' am_s dcl_s' cl_s fds_s mds_s, clarsimp simp add: full_name_f_def class_name_f_def)
 apply(frule find_cld_pn_match) apply(clarsimp simp add: package_name_f_def)
apply(clarsimp simp add: class_name_f_def mtype_f_def find_meth_def_f_def)
apply(case_tac cld_1) apply(rename_tac pn_1 am_1 dcl_1 cl_1 fds_1 mds_1) apply(clarsimp simp add: class_name_f_def)
apply(case_tac ctx_1) apply(rename_tac mi_1 pn_1) apply(clarsimp)
apply(case_tac "find_path_f P (ctx_def mi_1 pn_1) (cl_fqn (fqn_def pn_1 dcl_1))") apply(simp) apply(clarsimp)
apply(rename_tac path) apply(case_tac "find_meth_def_in_path_f path m") apply(simp) apply(clarsimp)
apply(rename_tac ctx_m' md) apply(case_tac md, rename_tac ms mb', clarsimp)
apply(case_tac ms, rename_tac cl_r' m'' vds', clarsimp) apply(case_tac "find_type_f P ctx_m' cl_r'") apply(simp) apply(clarsimp)
apply(clarsimp simp add: full_name_f_def class_methods_f_def)
apply(frule_tac ctx = "ctx_def mi_1 pn_1" in fpr_target_is_head) apply(clarsimp)
apply(frule find_cld_pn_match) apply(clarsimp simp add: package_name_f_def class_methods_f_def)
apply(case_tac "lift_opts (map (vd_case (\<lambda>clk vark. find_type_f P ctx_m' clk)) vds')") apply(simp) apply(clarsimp)
apply(frule_tac vds = vds' in lift_opts_ft_length) apply(clarsimp)
apply(case_tac mb', rename_tac ss' y, clarsimp) apply(case_tac "find_meth_def_in_list_f mds_1 m")
 apply(clarsimp) apply(frule find_md_m_match[rule_format]) apply(clarsimp)
apply(clarsimp) apply(frule find_md_m_match'[rule_format]) apply(clarsimp)
done

lemma exist_lifted_values:
  "\<lbrakk>\<forall>x\<in>dom G. (P, H, L x, G x) \<in> wf_object; \<forall>x\<in>set y_ty_list. (\<lambda>(y, ty). (P, G y, Some ty) \<in> sty_option) x\<rbrakk>
       \<Longrightarrow> \<exists>vs. lift_opts (map (\<lambda>(y, ty). L y) y_ty_list) = Some vs"
apply(induct y_ty_list) apply(simp) apply(clarsimp)
apply(erule sty_option.cases) apply(clarsimp) apply(drule_tac x = a in bspec, simp add: domI)
apply(erule wf_objectE) apply(simp) apply(simp)
done

lemma [iff]:
  "length (tr_ss_f (map_of (zip (map (vd_case (\<lambda>cl. x_var)) vds) (map x_var vars'))(x_this \<mapsto> x')) ss') = length ss'"
by (induct ss', auto)

lemma collect_suc_eq_lt[simp]:
  "{f i |i::nat. i < Suc n} = {f i |i. i = 0} \<union> {f (Suc i) |i. i < n}"
apply(induct n) apply(simp)
apply(clarsimp)
apply(simp add: less_Suc_eq)
apply(simp add: image_Collect[THEN sym])
apply(simp add: Collect_disj_eq)
apply(blast)
done

lemma [iff]:
  "\<forall>y_ty_list vars vars' vs. length y_ty_list = length vds \<and> length vars = length vds \<and> length vars' = length vds \<and> length vs = length vds \<longrightarrow>
   map (\<lambda>(y, cl, var, var', v). vd_def cl var) (zip (map fst y_ty_list) (zip (map (vd_case (\<lambda>cl var. cl)) vds) (zip (map (vd_case (\<lambda>cl var. var)) vds) (zip vars' vs)))) = vds"
apply(induct vds) apply(simp) apply(clarsimp simp add: set_zip length_Suc_conv split: vd.splits)
done

lemma vars'_eq[rule_format]:
  "\<forall>y_ty_list vds vars vs. length y_ty_list = length vars' \<and> length vds = length vars' \<and> length vars = length vars' \<and> length vs = length vars' \<longrightarrow>
   (\<lambda>(y, cl, var, var', v). x_var var') ` set (zip (map fst y_ty_list) (zip (map (vd_case (\<lambda>cl var. cl)) vds) (zip vars (zip vars' vs)))) = x_var ` set vars'"
apply(induct vars') apply(simp) apply(clarsimp simp add: set_zip length_Suc_conv)
done

lemma [iff]:
  "\<forall>y_ty_list vds vars vs. length y_ty_list = length vars' \<and> length vds = length vars' \<and> length vars = length vars' \<and> length vs = length vars' \<longrightarrow>
   map (\<lambda>(y, cl, var, var', v). var') (zip (map fst y_ty_list) (zip (map (vd_case (\<lambda>cl var. cl)) vds) (zip vars (zip vars' vs)))) = vars'"
apply(induct vars') apply(simp) apply(clarsimp simp add: set_zip length_Suc_conv)
done

lemma [iff]:
  "\<forall>y_ty_list vds vars vs. length y_ty_list = length vars' \<and> length vds = length vars' \<and> length vars = length vars' \<and> length vs = length vars' \<longrightarrow>
   map (\<lambda>(y, cl, var, var', v). (x_var var, x_var var'))
       (zip (map fst y_ty_list) (zip (map (vd_case (\<lambda>cl var. cl)) vds) (zip (map (vd_case (\<lambda>cl var. var)) vds) (zip vars' vs)))) =
     zip (map (vd_case (\<lambda>cl. x_var)) vds) (map x_var vars')"
apply(induct vars') apply(simp) apply(clarsimp simp add: set_zip length_Suc_conv split: vd.splits)
done

lemma [iff]:
  "\<forall>vds vars vars' vs. length vds = length y_ty_list \<and> length vars = length y_ty_list \<and> length vars' = length y_ty_list \<and> length vs = length y_ty_list \<longrightarrow>
   map (\<lambda>(y, cl, var, var', v). y) (zip (map fst y_ty_list) (zip (map (vd_case (\<lambda>cl var. cl)) vds) (zip vars (zip vars' vs)))) = map fst y_ty_list"
apply(induct y_ty_list) apply(simp) apply(clarsimp simp add: set_zip length_Suc_conv)
done

lemma lift_opts_mapping:
  "\<forall>vds vars vars' vs. length vds = length y_ty_list \<and> length vars = length y_ty_list \<and> length vars' = length y_ty_list \<and> length vs = length y_ty_list \<longrightarrow>
   lift_opts (map (\<lambda>(y, ty). L y) y_ty_list) = Some vs \<longrightarrow>
   (\<forall>x\<in>set (zip (map fst y_ty_list) (zip (map (vd_case (\<lambda>cl var. cl)) vds) (zip (map (vd_case (\<lambda>cl var. var)) vds) (zip vars' vs)))). (\<lambda>(y, cl, var, var', v). L y = Some v) x)"
apply(induct y_ty_list) apply(simp) apply(clarsimp simp add: set_zip length_Suc_conv split: vd.splits option.splits)
apply(rename_tac y1 y_ty_list v2 vs cl1 var1 var'1 v1 vds vars var'2 vars' i cl2 var2)
apply(erule_tac x = vds in allE) apply(erule_tac x = vars in allE) apply(erule_tac x = vars' in allE)
apply(simp) apply(case_tac i) apply(simp) apply(rename_tac j) apply(clarsimp)
apply(erule_tac x = "map fst y_ty_list ! j" in allE) apply(clarsimp)
apply(case_tac "zip (map (vd_case (\<lambda>cl var. cl)) vds) (zip (map (vd_case (\<lambda>cl var. var)) vds) (zip vars' vs)) ! j") apply(rename_tac cl1 var1 var'1 v1)
apply(erule_tac x = cl1 in allE) apply(erule_tac x = var1 in allE) apply(erule_tac x = var'1 in allE) apply(erule_tac x = v1 in allE)
apply(clarsimp) apply(erule_tac x = j in allE) apply(simp)
done

lemma length_y_ty_list_vs[rule_format]:
  "\<forall>vs. lift_opts (map (\<lambda>(y, ty). L y) y_ty_list) = Some vs \<longrightarrow> length y_ty_list = length vs"
by (induct y_ty_list, auto split: option.splits)

lemma translation_eq:
  "\<forall>x\<in>set (zip (tr_ss_f (map_of (zip (map (vd_case (\<lambda>cl. x_var)) vds) (map x_var vars'))(x_this \<mapsto> x')) ss') ss').
             (\<lambda>(s'', s'). (map_of (zip (map (vd_case (\<lambda>cl. x_var)) vds) (map x_var vars'))(x_this \<mapsto> x'), s', s'') \<in> tr_s) x"
apply(induct ss') apply(simp add: tr_rel_f_eq)+ done




theorem progress:
  "\<lbrakk>(G, config_normal P L H S) \<in> wf_config; S \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>config'. (config_normal P L H S, config') \<in> r_stmt"
apply(case_tac S)
 apply(simp)
apply(clarsimp) apply(rename_tac s ss)
apply(case_tac s)
apply(erule_tac[1-7] wf_configE) apply(simp_all)
(* s_block *)
apply(force intro: r_blockI[simplified])
(* s_ass *)
apply(clarsimp, erule wf_stmtE, simp_all, clarsimp)
apply(frule type_to_val) apply(simp) apply(clarify) apply(frule r_var_assignI) apply(force)
(* s_read *)
apply(clarsimp, erule wf_stmtE, simp_all, clarsimp)
apply(erule wf_varstateE) apply(drule_tac x = xa in bspec, simp add: domI)
apply(erule wf_objectE) apply(clarsimp) apply(frule r_field_read_npeI) apply(force)
apply(clarsimp) apply(erule sty_option.cases) back apply(clarsimp split: option.splits)
apply(erule wf_heapE) apply(drule_tac x = oid in bspec, simp add: domI) apply(clarsimp)
apply(rename_tac x oid ty_x_s ty_x_d fields_oid fs)
apply(frule no_field_hiding, simp+) apply(drule_tac x = f in bspec, simp) apply(clarsimp)
apply(erule wf_objectE) apply(clarsimp, frule_tac H = H in r_field_readI, simp, force)+
(* s_write *)
apply(clarsimp, erule wf_stmtE, simp_all, clarsimp)
apply(erule wf_varstateE) apply(frule_tac x = x in bspec, simp add: domI)
apply(erule wf_objectE) apply(clarsimp) apply(frule r_field_write_npeI) apply(force)
apply(clarsimp) apply(erule sty_option.cases) apply(clarsimp) apply(rename_tac ty_y ty_f)
apply(drule_tac x = y in bspec, simp add: domI) apply(clarsimp)
apply(erule sty_option.cases) apply(clarsimp split: option.splits)
apply(erule wf_objectE) apply(clarsimp)
apply(frule_tac H = H and y = y in r_field_writeI, simp, force)+
(* s_if *)
apply(clarsimp, erule wf_stmtE, simp_all, clarsimp) apply(erule disjE)
apply(frule type_to_val, simp, clarify) apply(case_tac "v = w")
apply(frule_tac y = y in r_if_trueI, force+)
apply(frule_tac y = y in r_if_falseI, force+)
apply(frule type_to_val, simp, clarify) apply(case_tac "v = w")
apply(frule_tac y = y and v = w in r_if_trueI, force+)
apply(frule_tac y = y and v = w in r_if_falseI, force+)
(* s_new *)
apply(clarsimp, erule wf_stmtE, simp_all, clarsimp) apply(rename_tac cl ctx ty var)
apply(erule sty_option.cases) apply(clarsimp) apply(rename_tac ty_cl ty_var)
apply(simp add: is_sty_one_def split: option.splits) apply(rename_tac path)
apply(frule find_path_fields) apply(erule exE)
apply(frule fresh_oid) apply(erule exE)
apply(frule_tac H = H and L = L and var = var and s_list = ss and f_list = fs in r_newI[simplified])
apply(clarsimp simp add: fields_f_def split: option.splits) apply(assumption) apply(simp) apply(force)
(* s_call *)
apply(clarsimp, erule wf_stmtE, simp_all, clarsimp)
apply(rename_tac ss y_ty_list x ty_x_s m ty_r_s var)
apply(erule wf_varstateE) apply(frule_tac x = x in bspec, simp add: domI) apply(clarsimp)
apply(erule wf_objectE) apply(clarsimp) apply(frule r_mcall_npeI) apply(force)
apply(elim sty_option.cases) apply(clarsimp split: option.splits)
apply(rename_tac ty_r_s ty_var_s ty_x_s ty_x_d fs_x)
apply(frule mtype_to_find_md, simp+) apply(clarsimp)
apply(frule_tac A = "dom L" and i = "length vds" in fresh_vars) apply(clarsimp) apply(rename_tac vars')
apply(frule exist_lifted_values) apply(simp) apply(clarify)
apply(frule_tac vars' = vars' in fresh_x_not_in_vars') apply(erule exE) apply(erule conjE)
apply(subgoal_tac "\<exists>vars. vars = map (\<lambda>vd. case vd of vd_def cl var \<Rightarrow> var) vds") prefer 2 apply(force) apply(erule exE)
apply(subgoal_tac "length vars = length vds") prefer 2 apply(force)
apply(frule length_y_ty_list_vs)
apply(subgoal_tac "\<exists>T. T = (map_of (zip (map (\<lambda>vd. case vd of vd_def cl var \<Rightarrow> x_var var) vds) (map x_var vars')))(x_this \<mapsto> x')") prefer 2 apply(force) apply(erule exE)
apply(frule_tac H = H and P = P and meth = m and ctx = ctx and cl = cl_r and y = y and ty = ty_x_d and x' = x' and T = T and y_cl_var_var'_v_list =
                "zip (map fst y_ty_list) (zip (map (\<lambda>vd. case vd of vd_def cl var \<Rightarrow> cl) vds) (zip vars (zip vars' vs)))"
                and s''_s'_list = "zip (tr_ss_f T ss') ss'" and var = var and s_list = ss
                in r_mcallI[simplified])
apply(force) apply(simp) apply(simp) apply(simp add: vars'_eq) apply(simp) apply(assumption) apply(simp add: vars'_eq)
apply(cut_tac L = L and y_ty_list = y_ty_list in lift_opts_mapping)
apply(erule_tac x = vds in allE) apply(erule_tac x = vars in allE) apply(erule_tac x = vars' in allE) apply(erule_tac x = vs in allE)
apply(simp) apply(simp) apply(simp) apply(simp add: translation_eq) apply(simp) apply(force)
done

lemma wf_P_change_wf_P:
  "(P, mi, P') \<in> wf_P_change \<Longrightarrow> P \<in> wf_p"
by (erule wf_P_change.cases, auto)

lemma wf_P_change_mi_dom:
  "(p_def RC MH, mi, P') \<in> wf_P_change \<Longrightarrow> mi \<notin> dom MH"
by (erule wf_P_change.cases, auto)

lemma wf_P_change_acyclic_clds:
  "(P, mi, P') \<in> wf_P_change \<Longrightarrow> P \<in> acyclic_clds"
by (force elim: wf_P_change.cases wf_programE)

lemma fmim_add[rule_format]:
  "find_md_in_mds_f mds mn = Some md' \<longrightarrow> (\<exists>md''. find_md_in_mds_f (md#mds) mn = Some md'')"
by (induct mds, auto split: md_c.splits)

lemma fmim_md_name[rule_format]:
  "find_md_in_mds_f mds mn = Some md \<longrightarrow> md_name_f md = mn"
by (induct mds, auto simp add: md_name_f_def split: md_c.splits)

lemma fmim_mds_rm[rule_format]:
  "md_name_f md = mn_std m \<longrightarrow> find_md_in_mds_f (mds_rm_f mds md) mn_core = find_md_in_mds_f mds mn_core"
by (induct mds, auto simp add: md_name_f_def split: md_c.splits)

lemma fcic_P:
  "(P, mi, P') \<in> wf_P_change \<Longrightarrow> find_cld_in_core_f P' fqn = find_cld_in_core_f P fqn"
apply(clarsimp simp add: find_cld_in_core_f_def)
apply(erule wf_P_change.cases)
  apply(erule wf_programE) apply(erule wf_rcE) apply(clarsimp) apply(drule_tac x = rn_bootstrap in bspec, simp add: domI) apply(clarsimp) apply(case_tac R)
   apply(rename_tac mds' RMIS') apply(clarsimp simp add: R_name_f_def R_body_f_def R_update_f_def)
   apply(case_tac md_c, rename_tac mn' clds_c ms fqns, clarsimp simp add: md_name_f_def)
  apply(simp add: R_name_f_def)
 apply(erule wf_programE) apply(erule wf_rcE) apply(clarsimp) apply(drule_tac x = rn_bootstrap in bspec, simp add: domI) apply(clarsimp) apply(case_tac R)
  apply(rename_tac mds' RMIS') apply(clarsimp simp add: R_name_f_def R_body_f_def R_update_f_def)
  apply(frule fmim_md_name) apply(simp add: fmim_mds_rm)
  apply(case_tac md_c, rename_tac mn' clds_c ms fqns, clarsimp simp add: md_name_f_def)
  apply(case_tac "find_md_in_mds_f mds_c1 mn_core") apply(simp) apply(rename_tac md) apply(frule_tac mn = mn_core in fmim_md_name)
  apply(case_tac md, rename_tac mn clds ms' fqns', clarsimp simp add: md_name_f_def)
 apply(simp add: R_name_f_def)
apply(clarsimp) apply(erule wf_programE) apply(erule wf_rcE) apply(clarsimp) apply(rename_tac RC MH R)
apply(drule_tac x = rn_bootstrap in bspec, simp add: domI) apply(clarsimp) apply(case_tac R)
 apply(rename_tac mds RMIS) apply(clarsimp simp add: R_name_f_def R_update_f_def)
 apply(erule contrapos_pp) back back back back back apply(clarsimp) apply(rule)
  apply(clarsimp simp add: R_body_f_def) apply(case_tac "find_md_in_mds_f mds_c mn_core") apply(simp) apply(clarsimp)
  apply(rename_tac md_core) apply(frule fmim_md_name) apply(case_tac md_core) apply(rename_tac clds' ms' fqns')
  apply(clarsimp simp add: md_name_f_def) apply(case_tac md_c) apply(simp) apply(clarsimp)
  apply(case_tac "RMISa (md_c_def repl mn_core clds' ms' fqns')") apply(simp) apply(clarsimp)
  apply(rename_tac idmi) apply(case_tac "idmi imp_dep_shared") apply(simp) apply(clarsimp)
  apply(erule wf_rE) apply(clarsimp) apply(erule wf_rmisE) apply(clarsimp)
  apply(erule_tac x = "md_c_def repl mn_core clds' ms' fqns'" in allE) apply(erule_tac x = imp_dep_shared in allE) apply(erule_tac x = mi in allE)
  apply(clarsimp) apply(force) apply(simp)
 apply(clarsimp) apply(case_tac "find_md_in_mds_f mds mn_core") apply(simp) apply(rename_tac md_core) apply(clarsimp)
 apply(case_tac "RMIS md_core") apply(simp) apply(clarsimp) apply(rename_tac idmi) apply(case_tac "idmi imp_dep_shared")
 apply(simp) apply(erule contrapos_np) apply(clarsimp) apply(erule wf_rE) apply(clarsimp) apply(erule wf_rmisE) apply(clarsimp)
 apply(erule_tac x = md_core in allE) apply(erule_tac x = imp_dep_shared in allE) apply(erule_tac x = mi in allE)
 apply(clarsimp) apply(force) apply(simp)
apply(rename_tac rn' r mds' RMIS') apply(clarsimp simp add: R_update_f_def)
done

lemma reachable_add[rule_format]:
  "(MH, mis, nn) \<in> reachable
      \<Longrightarrow> mi \<notin> dom MH \<longrightarrow> (\<lambda>u. if u = mi then Some (md', mibrs) else MH u, mis, nn) \<in> reachable"
apply(induct rule: reachable.induct)
 apply(rule, rule reachable_emptyI)
apply(clarsimp) apply(erule contrapos_np) apply(rule reachable_consI[simplified])
  apply(case_tac "mia = mi") apply(clarsimp) apply(force)
 apply(force)
apply(force)
done

lemma reachable_all[rule_format]:
  "(\<forall>mis. set mis \<subseteq> dom MH \<longrightarrow> (\<exists>nn. (MH, mis, nn) \<in> reachable)) \<and>
   (\<forall>mi\<in>dom MH. \<exists>md mibrs. MH mi = Some (md, mibrs) \<and> set (mis_of mibrs) \<subseteq> dom MH) \<and> set (mis_of mibrs') \<subseteq> dom MH \<and>
   (\<forall>a b. MH mi \<noteq> Some (a, b)) \<and> (set mis \<subseteq> dom (\<lambda>u. if u = mi then Some (md', mibrs') else MH u))
       \<longrightarrow> (\<exists>nn. (\<lambda>u. if u = mi then Some (md', mibrs') else MH u, mis, nn) \<in> reachable)"
apply(induct mis)
 apply(clarify) apply(rule_tac x = 0 in exI) apply(rule reachable_emptyI)
apply(clarsimp) apply(split split_if_asm)
 apply(clarsimp) apply(erule_tac x = "mis_of mibrs'" in allE, clarsimp)
 apply(frule_tac mi = mi and MH = MH and md' = md' and mibrs = mibrs' in reachable_add) apply(blast)
 apply(rule_tac x = "Suc (nna + nn)" in exI)
 apply(rule reachable_consI[of "\<lambda>u. if u = mi then Some (md', mibrs') else MH u" mi, simplified])
 apply(force) apply(simp add: mis_of_def) apply(assumption)
apply(rename_tac mi' mis md mibrs'' nn)
apply(drule_tac x = mi' in bspec, simp add: domI) apply(clarsimp)
apply(erule_tac x = "mis_of mibrs''" in allE) apply(clarsimp)
apply(frule_tac mi = mi and MH = MH and md' = md' and mibrs = mibrs' in reachable_add) apply(force)
apply(rule_tac x = "Suc (nna + nn)" in exI)
apply(subgoal_tac "(\<lambda>u. if u = mi then Some (md', mibrs') else MH u) mi' = Some (md, mibrs'')")
apply(rule_tac mi = mi' in reachable_consI[of "\<lambda>u. if u = mi then Some (md', mibrs') else MH u", simplified])
apply(force) apply(simp add: mis_of_def) apply(assumption) apply(force)
done

lemma dom_insert:
  "dom (\<lambda>u. if u = mi then Some (md', mis') else MH u) = insert mi (dom MH)"
apply(simp add: dom_def) apply(blast)
done

lemma list_map_fst[rule_format]: "(a, b) \<in> set list \<longrightarrow> a \<in> fst ` set list"
by (induct list, auto)

lemma acyclic_mh_add:
  "\<lbrakk>MH \<in> acyclic_mh; mi \<notin> dom MH; set (mis_of mibrs') \<subseteq> dom MH\<rbrakk> \<Longrightarrow> (\<lambda>u. if u = mi then Some (md', mibrs') else MH u) \<in> acyclic_mh"
apply(erule acyclic_mh.cases) apply(clarsimp) apply(erule contrapos_np) apply(clarsimp)
apply(rule am_defI)
  apply(cut_tac a = mi and A = "dom MH" in finite_insert) apply(simp only: dom_insert)
 apply(clarsimp) apply(rule reachable_all) apply(clarsimp simp add: mis_of_def)+
apply(rule)
 apply(clarsimp) apply(frule_tac x = aa in set_mp) apply(simp add: list_map_fst) apply(force)
apply(clarsimp) apply(drule_tac x = mia in bspec, simp add: domI) apply(clarsimp)
apply(frule_tac A = "fst ` set b" and x = aa in set_mp) apply(simp add: list_map_fst) apply(force)
done

lemma dom_subset:
  "dom MH \<subseteq> dom (\<lambda>u. if u = mi then Some (md', mis') else MH u)"
by (force simp add: subset_eq)

lemma fcii_P'[rule_format]:
  "\<forall>ctxcld_opt. find_cld_in_imports_f (MH, mibrs, fqn) = ctxcld_opt
      \<longrightarrow> (MH \<in> acyclic_mh \<and> set (mis_of mibrs) \<subseteq> dom MH \<and> mi \<notin> dom MH \<and> set (mis_of mibrs') \<subseteq> dom MH
          \<longrightarrow> find_cld_in_imports_f (MH(mi \<mapsto> (md', mibrs')), mibrs, fqn) = ctxcld_opt)"
apply(induct_tac MH mibrs fqn rule: fcii_induct) apply(simp) apply(clarsimp)
apply(rename_tac mi' br mibrs fqn) apply(rule)
 apply(clarsimp) apply(rule)
  apply(clarsimp) apply(case_tac "MH mi") apply(simp) apply(simp)
 apply(clarsimp simp add: mis_of_def)
apply(clarsimp simp add: mis_of_def) apply(rule)
 apply(clarsimp) apply(erule_tac Q = "None = ?R" in contrapos_np) apply(simp)
 apply(frule_tac mi = mi and md' = md' and mibrs' = mibrs' in acyclic_mh_add)
   apply(case_tac "mi \<in> dom MH", simp add: dom_def, assumption) apply(simp add: mis_of_def)
 apply(clarsimp) apply(frule_tac x = aa in set_mp) apply(simp add: list_map_fst) apply(simp add: dom_def)
apply(clarsimp) apply(rename_tac md'' mis'') apply(case_tac md'', rename_tac repl mn clds ms fqns', clarsimp)
apply(clarsimp split: split_if_asm)
apply(case_tac "mi \<in> dom MH") apply(simp add: dom_def)
apply(erule acyclic_mh.cases) back apply(drule_tac x = mi' in bspec, clarsimp simp add: domI)
apply(clarsimp split: option.splits)
done

lemma fcii_P:
  "\<lbrakk>(p_def RC MH, mi, p_def RC' MH') \<in> wf_P_change; set (mis_of mibrs) \<subseteq> dom MH\<rbrakk>
       \<Longrightarrow> find_cld_in_imports_f (MH', mibrs, fqn) = find_cld_in_imports_f (MH, mibrs, fqn)"
apply(erule wf_P_change.cases[simplified]) apply(simp) apply(simp) apply(clarsimp)
apply(erule contrapos_np) apply(clarsimp) apply(erule wf_programE) apply(erule wf_mhE) apply(clarsimp)
apply(subgoal_tac "\<exists>ctxcld_opt. find_cld_in_imports_f (MH, mibrs, fqn) = ctxcld_opt")
 apply(erule exE) apply(frule_tac mi = mi and md' = md and mibrs' = mi_br_list in fcii_P')
  apply(force simp add: mis_of_def)
 apply(simp)
apply(simp)
done

lemma acyclic_mh_dom:
  "\<lbrakk>MH \<in> acyclic_mh; MH mi = Some (md, mibrs)\<rbrakk> \<Longrightarrow> set (mis_of mibrs) \<subseteq> dom MH"
apply(erule acyclic_mh.cases) apply(simp) apply(drule_tac x = mi in bspec, simp add: domI)
apply(simp add: mis_of_def) done

lemma wf_P_change_map_le:
  "\<lbrakk>(p_def RC MH, mi, p_def RC' MH') \<in> wf_P_change\<rbrakk> \<Longrightarrow> MH \<subseteq>\<^sub>m MH'"
apply(erule wf_P_change.cases) apply(clarsimp) apply(clarsimp)
apply(clarsimp) apply(erule contrapos_np) apply(force simp add: map_le_def)
done

lemma wf_P_change_mh_eq:
  "\<lbrakk>(p_def RC MH, mi, p_def RC' MH') \<in> wf_P_change; mi \<noteq> mi'\<rbrakk> \<Longrightarrow> MH' mi' = MH mi'"
by (erule wf_P_change.cases, auto)

lemma ncrim_P:
  "\<lbrakk>(p_def RC MH, mi, p_def RC' MH') \<in> wf_P_change; MH mi' = Some (md, mibrs)\<rbrakk>
       \<Longrightarrow> ((p_def RC' MH', mibrs) \<in> no_core_renaming_in_mibrs) = ((p_def RC MH, mibrs) \<in> no_core_renaming_in_mibrs)"
apply(rule)
 apply(erule no_core_renaming_in_mibrs.cases) apply(clarsimp) apply(rule ncrim_defI[simplified]) apply(clarsimp)
 apply(rename_tac mi'' br fqn fqn_from fqn_to ctx cld) apply(drule_tac x = "(mi'', br)" in bspec, simp)
 apply(erule_tac x = fqn in allE) apply(clarsimp) apply(simp add: fcic_P)
 apply(drule_tac x = "(fqn_from, fqn_to)" in bspec, simp) apply(simp)
apply(erule no_core_renaming_in_mibrs.cases) apply(clarsimp) apply(rule ncrim_defI[simplified]) apply(clarsimp)
apply(rename_tac mi'' br fqn fqn_from fqn_to ctx cld) apply(drule_tac x = "(mi'', br)" in bspec, simp)
apply(erule_tac x = fqn in allE) apply(clarsimp) apply(simp add: fcic_P)
apply(drule_tac x = "(fqn_from, fqn_to)" in bspec, simp) apply(simp)
done

lemma ncr_P:
  "\<lbrakk>(P, mi, P') \<in> wf_P_change\<rbrakk> \<Longrightarrow> (P' \<in> no_core_renaming) = (P \<in> no_core_renaming)"
apply(rule)
 apply(erule no_core_renaming.cases) apply(clarsimp) apply(rename_tac MH' RC')
 apply(case_tac P, rename_tac RC MH, clarsimp) apply(rule ncr_defI) apply(clarsimp) apply(rename_tac mi' md mibrs)
 apply(frule wf_P_change_map_le) apply(drule_tac x = mi' in bspec) apply(frule map_le_implies_dom_le) apply(force)
 apply(simp add: map_le_def) apply(drule_tac x = mi' and A = "dom MH" in bspec, simp add: domI) apply(clarsimp)
 apply(simp add: ncrim_P)
apply(erule no_core_renaming.cases) apply(clarsimp)
apply(case_tac P', rename_tac RC' MH', clarsimp) apply(rule ncr_defI) apply(clarsimp)
apply(rename_tac mi' md mibrs) apply(erule wf_P_change.cases)
  apply(clarsimp) apply(erule contrapos_np) apply(drule_tac x = mi' in bspec, simp add: domI) apply(clarsimp)
  apply(erule no_core_renaming_in_mibrs.cases) apply(clarsimp) apply(rule ncrim_defI[simplified]) apply(clarsimp)
  apply(rename_tac mi'' br fqn fqn_from fqn_to ctx cld) apply(drule_tac x = "(mi'', br)" in bspec, simp)
  apply(erule_tac x = fqn in allE) apply(clarsimp) apply(frule_tac RMIS = RMIS in wrc_installI, (simp add: dom_def)+)
  apply(simp add: fcic_P) apply(drule_tac x = "(fqn_from, fqn_to)" in bspec, simp) apply(simp)
 apply(clarsimp) apply(erule contrapos_np) apply(drule_tac x = mi' in bspec, simp add: domI) apply(clarsimp)
 apply(erule no_core_renaming_in_mibrs.cases) apply(clarsimp) apply(rule ncrim_defI[simplified]) apply(clarsimp)
 apply(rename_tac mi'' br fqn fqn_from fqn_to ctx cld) apply(drule_tac x = "(mi'', br)" in bspec, simp)
 apply(erule_tac x = fqn in allE) apply(clarsimp) apply(frule_tac RMIS = RMIS in wrc_uninstallI, (simp add: dom_def)+)
 apply(simp add: fcic_P) apply(drule_tac x = "(fqn_from, fqn_to)" in bspec, simp) apply(simp)
apply(clarsimp) apply(erule contrapos_np) apply(clarsimp split: split_if_asm)
 apply(erule wf_mdE) apply(clarsimp)
apply(drule_tac x = mi' in bspec, simp add: domI) apply(clarsimp)
apply(erule no_core_renaming_in_mibrs.cases) apply(clarsimp) apply(rule ncrim_defI[simplified]) apply(clarsimp)
apply(rename_tac mi'' br fqn fqn_from fqn_to ctx cld) apply(drule_tac x = "(mi'', br)" in bspec, simp)
apply(erule_tac x = fqn in allE) apply(clarsimp) apply(frule_tac RMIS = RMIS in wrc_new_instanceI, (simp add: dom_def)+)
apply(simp add: fcic_P) apply(drule_tac x = "(fqn_from, fqn_to)" in bspec, simp) apply(simp)
done

lemma fc_P:
  "\<lbrakk>(P, mi, P') \<in> wf_P_change; mi \<noteq> mi'\<rbrakk> \<Longrightarrow> find_cld_f P' (ctx_def mi' pn) fqn = find_cld_f P (ctx_def mi' pn) fqn"
apply(clarsimp simp add: find_cld_f_def fcic_P ncr_P split: split_if_asm option.splits)
apply(case_tac P, rename_tac RC MH, clarsimp) apply(case_tac P', rename_tac RC' MH', clarsimp)
apply(clarsimp simp add: wf_P_change_mh_eq split: option.splits md.splits)
apply(rename_tac mibrs repl mn clds imps fqns) apply(frule wf_P_change_wf_P) apply(erule wf_programE)
apply(erule wf_mhE) apply(clarsimp) apply(erule acyclic_mh.cases) apply(clarsimp)
apply(drule_tac x = mi' in bspec, simp add: domI)+ apply(clarsimp)
apply(rule fcii_P) apply(simp) apply(simp add: mis_of_def)
done

lemma ft_P:
  "\<lbrakk>(P, mi, P') \<in> wf_P_change; mi \<noteq> mi'\<rbrakk> \<Longrightarrow> find_type_f P' (ctx_def mi' pn) cl = find_type_f P (ctx_def mi' pn) cl"
apply(case_tac cl) apply(simp) by (simp add: fc_P split: fqn.splits)

lemma fcii_mi_dom[rule_format]:
  "find_cld_in_imports_f (MH, mis, fqn) = Some (ctx_def mi pn, cld) \<longrightarrow> mi \<in> dom MH"
apply(induct_tac MH mis fqn rule: fcii_induct) apply(simp)
apply(clarsimp split: option.splits md.splits) apply(rule) apply(force)
apply(clarsimp) apply(force)
done

lemma fc_mi_dom:
  "find_cld_f (p_def RC MH) ctx fqn = Some (ctx_def mi pn, cld) \<Longrightarrow> mi \<in> dom MH"
apply(clarsimp simp add: find_cld_f_def split: option.splits ctx.splits md.splits split_if_asm)
 apply(frule fcii_mi_dom) apply(force)
apply(clarsimp simp add: find_cld_in_core_f_def split: option.splits R.splits md.splits)
done

lemma path_length_P_P'[rule_format]:
  "(P, ctx, fqn, nn) \<in> path_length \<Longrightarrow> (\<forall>mi' pn. ctx = ctx_def mi' pn
      \<longrightarrow> (P, mi, P') \<in> wf_P_change \<and> mi \<noteq> mi'
         \<longrightarrow> (P', ctx_def mi' pn, fqn, nn) \<in> path_length)"
apply(erule path_length.induct)
 apply(clarsimp) apply(rule pl_objI)
apply(clarsimp) apply(case_tac ctx') apply(rename_tac mi'' pn'') apply(clarsimp)
apply(case_tac P, rename_tac RC MH, clarsimp) apply(frule wf_P_change_mi_dom)
apply(frule fc_mi_dom) apply(case_tac "mi = mi''") apply(force) apply(clarsimp)
apply(erule_tac Q = "?S \<in> path_length" in contrapos_np)
apply(rule_tac ctx' = "ctx_def mi'' pn''" and cld = cld in pl_fqnI[simplified])
apply(simp add: fc_P) apply(simp) apply(simp)
done

lemma path_length_P'_P[rule_format]:
  "(P', ctx, fqn, nn) \<in> path_length \<Longrightarrow> (\<forall>mi' pn. ctx = ctx_def mi' pn
      \<longrightarrow> (P, mi, P') \<in> wf_P_change \<and> mi \<noteq> mi'
         \<longrightarrow> (P, ctx_def mi' pn, fqn, nn) \<in> path_length)"
apply(erule path_length.induct)
 apply(clarsimp) apply(rule pl_objI)
apply(clarsimp) apply(case_tac ctx') apply(rename_tac mi'' pn'') apply(clarsimp)
apply(case_tac P, rename_tac RC MH, clarsimp) apply(frule wf_P_change_mi_dom)
apply(case_tac P, rename_tac RC' MH', clarsimp)
apply(frule fc_mi_dom) apply(erule_tac Q = "?S \<in> path_length" in contrapos_np) apply(clarsimp)
apply(case_tac "mi = mi''")
 apply(clarsimp simp add: fc_P) apply(drule fc_mi_dom) apply(simp add: dom_def)
apply(clarsimp)
apply(rule_tac ctx' = "ctx_def mi'' pn''" and cld = cld in pl_fqnI[simplified])
apply(simp add: fc_P) apply(simp) apply(simp)
done

lemma fc_dom_fcic:
  "\<lbrakk>find_cld_f (p_def RC MH) (ctx_def mi pn) fqn = Some (ctx_def mi' pn', cld); mi \<notin> dom MH\<rbrakk>
       \<Longrightarrow> find_cld_in_core_f (p_def RC MH) fqn = Some (ctx_def mi' pn', cld) \<and> mi \<noteq> mi'"
by (force simp add: find_cld_f_def find_cld_in_core_f_def split: option.splits R.splits md.splits split_if_asm)

lemma [simp]: "(\<lambda>u. if u = rn then Some R else RC u) = RC(rn \<mapsto> R)" by (rule, simp)

lemma path_length_P:
  "\<lbrakk>(P, mi, P') \<in> wf_P_change; find_cld_f P' (ctx_def mi pn) fqn = Some (ctx', cld);
    (\<exists>ctx' cld. find_cld_f P (ctx_def mi pn) fqn = Some (ctx', cld)) \<longrightarrow> (\<exists>nn. (P, ctx_def mi pn, cl_fqn fqn, nn) \<in> path_length)\<rbrakk>
       \<Longrightarrow> \<exists>nn. (P', ctx_def mi pn, cl_fqn fqn, nn) \<in> path_length"
apply(erule wf_P_change.cases[simplified])
  apply(clarsimp) apply(erule_tac Q = "\<forall>nn. ?S RC rn R md mds RMIS MH nn" in contrapos_pp) apply(clarsimp)
  apply(case_tac ctx', rename_tac mi' pn', clarsimp)
  apply(frule fc_dom_fcic) apply(force) apply(frule_tac mi = mi in wrc_installI) apply(force) apply(simp) apply(force) apply(simp) apply(simp add: dom_def)
  apply(simp add: fcic_P) apply(frule wf_P_change_acyclic_clds) apply(erule acyclic_clds.cases) apply(clarsimp)
  apply(subgoal_tac "\<forall>ctx. find_cld_f (p_def RC MH) ctx fqn = Some (ctx_def mi' pn', cld)")
   apply(erule_tac x = "ctx_def mi pn" in allE) apply(erule_tac x = mi in allE) apply(erule acyclic_clds_mi.cases)
   apply(erule_tac x = pn in allE) apply(erule_tac x = fqn in allE) apply(clarsimp)
   apply(erule path_length.cases) apply(simp) apply(clarsimp) apply(rule_tac x = "Suc nna" in exI) apply(rule pl_fqnI[simplified])
   apply(force) apply(simp) apply(rule path_length_P_P') apply(simp) apply(simp) apply(force)
  apply(clarsimp simp add: find_cld_f_def fcic_P ncr_P split: split_if_asm)
 apply(clarsimp) apply(erule_tac Q = "\<forall>nn. ?S RC rn R md mds RMIS MH nn" in contrapos_pp) apply(clarsimp)
 apply(case_tac ctx', rename_tac mi' pn', clarsimp)
 apply(frule fc_dom_fcic) apply(force) apply(frule_tac mi = mi and ?mds_c1.0 = mds_c1 in wrc_uninstallI)
 apply(force) apply(force) apply(simp) apply(simp add: dom_def) apply(simp) apply(simp)
 apply(simp add: fcic_P) apply(frule wf_P_change_acyclic_clds) apply(erule acyclic_clds.cases) apply(clarsimp)
 apply(subgoal_tac "\<forall>ctx. find_cld_f (p_def RC MH) ctx fqn = Some (ctx_def mi' pn', cld)")
  apply(erule_tac x = "ctx_def mi pn" in allE) apply(erule_tac x = mi in allE) apply(erule acyclic_clds_mi.cases)
  apply(erule_tac x = pn in allE) apply(erule_tac x = fqn in allE) apply(clarsimp)
  apply(erule path_length.cases) apply(simp) apply(clarsimp) apply(rule_tac x = "Suc nna" in exI) apply(rule pl_fqnI[simplified])
  apply(force) apply(simp) apply(rule path_length_P_P') apply(simp) apply(simp) apply(force)
 apply(clarsimp simp add: find_cld_f_def fcic_P ncr_P split: split_if_asm)
apply(frule_tac mds_c = mds_c in wrc_new_instanceI, simp+) apply(force)
apply(clarsimp) apply(erule_tac Q = "\<forall>nn. ?S RC rn R md mds RMIS MH nn" in contrapos_pp) apply(clarsimp)
apply(erule wf_mdE) apply(clarsimp) apply(erule acyclic_clds_mi.cases) apply(clarsimp)
done

lemma acyclic_clds_mi_P:
  "(P, mi, P') \<in> wf_P_change \<Longrightarrow> ((mi', P) \<in> acyclic_clds_mi) = ((mi', P') \<in> acyclic_clds_mi)"
apply(rule)
 apply(erule acyclic_clds_mi.cases) apply(clarsimp) apply(rule acm_defI) apply(clarsimp)
 apply(erule_tac x = pn in allE) apply(erule_tac x = fqn in allE) apply(case_tac "mi = mi'")
  apply(clarsimp) apply(frule path_length_P) apply(force) apply(force) apply(force)
 apply(clarsimp simp add: fc_P) apply(frule path_length_P_P') apply(force) apply(force) apply(force)
apply(erule acyclic_clds_mi.cases) apply(clarsimp) apply(rule acm_defI) apply(clarsimp)
apply(erule_tac x = pn in allE) apply(erule_tac x = fqn in allE) apply(case_tac "mi = mi'")
apply(clarsimp) apply(drule wf_P_change_acyclic_clds) apply(erule acyclic_clds.cases) apply(clarsimp)
apply(erule_tac x = mi' in allE) apply(erule acyclic_clds_mi.cases) apply(clarsimp)
apply(clarsimp simp add: fc_P) apply(frule path_length_P'_P) apply(force) apply(force) apply(force)
done

lemma acyclic_clds_P:
  "(P, mi, P') \<in> wf_P_change \<Longrightarrow> (P \<in> acyclic_clds) = (P' \<in> acyclic_clds)"
apply(rule)
 apply(erule acyclic_clds.cases) apply(clarsimp) apply(rule ac_defI) apply(clarsimp) apply(rename_tac mi')
 apply(erule_tac x = mi' in allE) apply(simp add: acyclic_clds_mi_P)
apply(erule acyclic_clds.cases) apply(clarsimp) apply(rule ac_defI) apply(clarsimp) apply(rename_tac mi')
apply(erule_tac x = mi' in allE) apply(simp add: acyclic_clds_mi_P)
done

lemma fpr_P'[rule_format]:
  "\<forall>path_opt. find_path_rec_f (P, ctx, cl, prefix) = path_opt \<longrightarrow> (\<forall>mi' pn. ctx = ctx_def mi' pn
     \<longrightarrow> (\<forall>mi P'. (P, mi, P') \<in> wf_P_change \<and> mi \<noteq> mi'
         \<longrightarrow> find_path_rec_f (P', ctx, cl, prefix) = path_opt))"
apply(induct_tac P ctx cl prefix rule: find_path_rec_f.induct) apply(simp)
apply(clarsimp split: option.splits) apply(rule)
 apply(clarsimp simp add: acyclic_clds_P)
apply(clarsimp) apply(rule)
 apply(clarsimp simp add: fc_P)
apply(clarsimp) apply(rule)
 apply(clarsimp) apply(rule)
  apply(clarsimp simp add: acyclic_clds_P)
 apply(clarsimp simp add: fc_P)
apply(clarsimp) apply(rule)
 apply(clarsimp simp add: acyclic_clds_P)
apply(clarsimp simp add: fc_P)
apply(rename_tac ctx cld, case_tac ctx, rename_tac mi'' pn'', clarsimp)
apply(erule_tac x = mi in allE) apply(erule_tac x = P' in allE)
apply(subgoal_tac "mi \<noteq> mi''")
 apply(clarsimp)
apply(thin_tac "?P \<longrightarrow> ?Q") apply(case_tac P, rename_tac RC MH, simp) apply(drule wf_P_change_mi_dom)
apply(drule fc_mi_dom) apply(force)
done

lemma fpr_P:
  "\<lbrakk>(P, mi, P') \<in> wf_P_change; mi \<noteq> mi'\<rbrakk>
       \<Longrightarrow> find_path_rec_f (P', ctx_def mi' pn, cl, prefix) = find_path_rec_f (P, ctx_def mi' pn, cl, prefix)"
apply(subgoal_tac "\<exists>path_opt. find_path_rec_f (P, ctx_def mi' pn, cl, prefix) = path_opt")
 apply(erule exE) apply(frule_tac fpr_P') apply(force) apply(force) apply(simp)
by simp

lemma fp_P:
  "\<lbrakk>(P, mi, P') \<in> wf_P_change; mi \<noteq> mi'\<rbrakk> \<Longrightarrow> find_path_f P' (ctx_def mi' pn) cl = find_path_f P (ctx_def mi' pn) cl"
by (unfold find_path_f_def, force intro: fpr_P[where prefix = "[]", simplified])

lemma fpt_P:
  "\<lbrakk>(P, mi, P') \<in> wf_P_change; mi \<noteq> mi'\<rbrakk> \<Longrightarrow> find_path_ty_f P' (ty_def (ctx_def mi' pn) dcl) = find_path_ty_f P (ty_def (ctx_def mi' pn) dcl)"
apply(clarsimp simp add: fp_P split: ctx.splits) done

lemma fields_P:
  "\<lbrakk>(P, mi, P') \<in> wf_P_change; mi \<noteq> mi'\<rbrakk> \<Longrightarrow> fields_f P' (ty_def (ctx_def mi' pn) dcl) = fields_f P (ty_def (ctx_def mi' pn) dcl)"
apply(simp add: fields_f_def) apply(force simp add: fp_P) done

lemma ftif_P'[rule_format]:
  "ftype_in_fds_f P (ctx_def mi' pn) fds f = ty_opt \<longrightarrow> (P, mi, P') \<in> wf_P_change \<and> mi \<noteq> mi'
       \<longrightarrow> ftype_in_fds_f P' (ctx_def mi' pn) fds f = ty_opt"
apply(induct_tac fds rule: ftype_in_fds_f.induct) apply(simp) by (clarsimp simp add: ft_P split: fd.splits)

lemma ftif_P:
  "\<lbrakk>(P, mi, P') \<in> wf_P_change; mi \<noteq> mi'\<rbrakk> \<Longrightarrow> ftype_in_fds_f P' (ctx_def mi' pn) fds f = ftype_in_fds_f P (ctx_def mi' pn) fds f"
apply(subgoal_tac "\<exists>ty_opt. ftype_in_fds_f P (ctx_def mi' pn) fds f = ty_opt")
 apply(erule exE) apply(frule ftif_P') apply(force) apply(simp)
by simp

lemma ftip_P'[rule_format]:
  "ftype_in_path_f P path f = ty_opt \<longrightarrow> (P, mi, P') \<in> wf_P_change \<and> (\<forall>(ctx, cld) \<in> set path. case ctx of ctx_def mi' pn \<Rightarrow> mi \<noteq> mi')
        \<longrightarrow> ftype_in_path_f P' path f = ty_opt"
apply(induct_tac path rule: ftype_in_path_f.induct) apply(simp) apply(clarsimp simp add: ftif_P split: option.splits ctx.splits ty_opt_bot.splits)
done

lemma ftip_P[rule_format]:
  "\<lbrakk>(P, mi, P') \<in> wf_P_change; \<forall>(ctx, cld) \<in> set path. case ctx of ctx_def mi' pn \<Rightarrow> mi \<noteq> mi'\<rbrakk>
      \<Longrightarrow> ftype_in_path_f P' path f = ftype_in_path_f P path f"
apply(subgoal_tac "\<exists>ty_opt. ftype_in_path_f P path f = ty_opt")
 apply(erule exE) apply(frule ftip_P') apply(force) apply(simp)
by simp

lemma fc_no_mi:
  "\<lbrakk>find_cld_f P (ctx_def mi' pn) fqn = Some (ctx_def mi'' pn', cld); mi \<noteq> mi'; (P, mi, P') \<in> wf_P_change\<rbrakk>
      \<Longrightarrow> mi \<noteq> mi''"
apply(case_tac P, rename_tac RC MH, simp) apply(frule wf_P_change_mi_dom)
apply(frule fc_mi_dom) apply(force)
done

lemma fpr_no_mi[rule_format]:
  "\<forall>suffix. find_path_rec_f (P, ctx, cl, prefix) = Some (prefix @ suffix) \<longrightarrow> (\<forall>mi' pn. ctx = ctx_def mi' pn
     \<longrightarrow> (\<forall>mi P'. (P, mi, P') \<in> wf_P_change \<and> mi \<noteq> mi'
         \<longrightarrow> (\<forall>(ctx, cld) \<in> set suffix. case ctx of ctx_def mi' pn \<Rightarrow> mi \<noteq> mi')))"
apply(induct_tac P ctx cl prefix rule: find_path_rec_f.induct) apply(clarsimp)
apply(clarsimp split: option.splits) apply(frule path_append) apply(clarsimp) apply(erule disjE)
 apply(clarsimp) apply(case_tac a, clarify) apply(simp add: fc_no_mi)
apply(case_tac a) apply(rename_tac mi'' pn'') apply(clarsimp) apply(erule_tac x = mi in allE)
apply(force simp add: fc_no_mi)
done

lemma fp_no_mi:
  "\<lbrakk>(P, mi, P') \<in> wf_P_change; mi \<noteq> mi'; find_path_f P (ctx_def mi' pn) cl = Some path\<rbrakk>
      \<Longrightarrow> \<forall>(ctx, cld) \<in> set path. case ctx of ctx_def mi' pn \<Rightarrow> mi \<noteq> mi'"
apply(unfold find_path_f_def) apply(rule)
apply(rule fpr_no_mi[of _ _ _ "[]", simplified]) apply(force+)
done

lemma ftype_P:
  "\<lbrakk>(P, mi, P') \<in> wf_P_change; mi \<noteq> mi'\<rbrakk> \<Longrightarrow> ftype_f P' (ty_def (ctx_def mi' pn) dcl) f = ftype_f P (ty_def (ctx_def mi' pn) dcl) f"
apply(clarsimp simp add: ftype_f_def fpt_P ftip_P split: option.splits) apply(rule)
 apply(clarsimp simp add: fp_P)
apply(clarsimp simp add: fp_P) apply(rename_tac path)
apply(frule fp_no_mi, simp+) apply(frule ftip_P) apply(force) apply(simp)
done

lemma fmd_P:
  "\<lbrakk>(P, mi, P') \<in> wf_P_change; mi \<noteq> mi'\<rbrakk>
      \<Longrightarrow> find_meth_def_f P' (ty_def (ctx_def mi' pn) dcl) meth = find_meth_def_f P (ty_def (ctx_def mi' pn) dcl) meth"
by (simp add: find_meth_def_f_def fp_P)

lemma fmdip_ctx_mem[rule_format]:
  "\<forall>ctx md. find_meth_def_in_path_f path m = Some (ctx, md) \<longrightarrow> (\<exists>cld. (ctx, cld) \<in> set path)"
apply(induct path rule: find_meth_def_in_path_f.induct) apply(simp) apply(clarsimp)
apply(case_tac "find_meth_def_in_list_f (class_methods_f b) m") apply(force) apply(force)
done

lemma mtype_P:
  "\<lbrakk>(P, mi, P') \<in> wf_P_change; mi \<noteq> mi'\<rbrakk> \<Longrightarrow> mtype_f P' (ty_def (ctx_def mi' pn) dcl) meth = mtype_f P (ty_def (ctx_def mi' pn) dcl) meth"
apply(clarsimp simp add: mtype_f_def fmd_P split: option.splits meth_def.splits)
apply(rename_tac ctx ms mb) apply(case_tac ms, rename_tac cl m vds, clarsimp)
apply(simp add: find_meth_def_f_def) apply(case_tac "find_path_f P (ctx_def mi' pn) (cl_fqn (fqn_def pn dcl))") apply(simp) apply(clarsimp)
apply(rename_tac path) apply(frule fp_no_mi, simp+) apply(frule fmdip_ctx_mem) apply(clarsimp)
apply(drule_tac x = "(ctx, cld)" in bspec, simp) apply(clarsimp) apply(case_tac ctx, rename_tac mi'' pn', clarsimp)
apply(clarsimp simp add: ft_P split: option.splits)
done

lemma fc_some:
  "\<lbrakk>(P, mi, P') \<in> wf_P_change; find_cld_f P ctx fqn = Some (ctx', cld)\<rbrakk>
       \<Longrightarrow> find_cld_f P' ctx fqn = Some (ctx', cld)"
apply(case_tac P, rename_tac RC MH, clarsimp)
apply(case_tac ctx, rename_tac mi' pn', clarsimp)
apply(case_tac ctx', rename_tac mi'' pn'', clarsimp) apply(case_tac "mi = mi'")
 apply(frule fc_dom_fcic) apply(simp add: wf_P_change_mi_dom)
 apply(clarsimp simp add: find_cld_f_def fcic_P ncr_P split: split_if_asm)
apply(simp add: fc_P)
done

lemma fpr_some[rule_format]:
  "\<forall>path. find_path_rec_f (P, ctx, cl, prefix) = Some path \<longrightarrow> (P, mi, P') \<in> wf_P_change
       \<longrightarrow> find_path_rec_f (P', ctx, cl, prefix) = Some path"
apply(induct_tac P ctx cl prefix rule: find_path_rec_f.induct) apply(simp) apply(clarsimp) apply(rule)
 apply(clarsimp simp add: acyclic_clds_P)
apply(clarsimp simp add: acyclic_clds_P split: option.splits) apply(rule)
 apply(clarsimp) apply(frule_tac fc_some) apply(assumption) apply(simp)
apply(clarsimp) apply(frule_tac fc_some) apply(assumption) apply(simp)
done

lemma ft_some:
  "\<lbrakk>find_type_f P ctx cl = Some ty; (P, mi, P') \<in> wf_P_change\<rbrakk> \<Longrightarrow> find_type_f P' ctx cl = Some ty"
apply(case_tac P, rename_tac RC MH, clarsimp) apply(case_tac ctx, rename_tac mi' pn, clarsimp)
apply(frule wf_P_change_mi_dom) apply(case_tac "mi = mi'")
 apply(clarsimp) apply(case_tac cl) apply(simp) apply(case_tac fqn, rename_tac pn' dcl, clarsimp)
 apply(case_tac "find_cld_f (p_def RC MH) (ctx_def mi pn) (fqn_def pn' dcl)") apply(simp) apply(clarsimp)
 apply(rename_tac ctx cld) apply(erule_tac Q = "?R = ?S" in contrapos_np)
 apply(case_tac ctx, rename_tac mi' pn'', clarsimp) apply(frule fc_dom_fcic) apply(simp add: dom_def)
 apply(clarsimp simp add: find_cld_f_def fcic_P ncr_P split: split_if_asm)
apply(simp add: ft_P)
done

lemma ftif_ty_opt[rule_format]:
  "\<forall>ty_opt. ftype_in_fds_f P ctx fds f = ty_opt_bot_opt ty_opt \<longrightarrow> (P, mi, P') \<in> wf_P_change
      \<longrightarrow> ftype_in_fds_f P' ctx fds f = ty_opt_bot_opt ty_opt"
apply(induct fds) apply(simp) apply(clarsimp split: fd.splits option.splits) apply(rule)
 apply(clarsimp) apply(frule ft_some, simp, simp)
apply(clarsimp) apply(frule ft_some, simp, simp)
done

lemma ftip_some[rule_format]:
  "ftype_in_path_f (p_def RC MH) path f = Some ty' \<longrightarrow> (p_def RC MH, mi, P') \<in> wf_P_change
       \<longrightarrow> ftype_in_path_f P' path f = Some ty'"
apply(induct_tac path rule: ftype_in_path_f.induct) apply(simp) apply(clarsimp)
apply(frule wf_P_change_mi_dom)
apply(case_tac "ftype_in_fds_f (p_def RC MH) a (class_fields_f b) f")
 apply(rename_tac ty_opt) apply(case_tac ty_opt)
  apply(clarsimp) apply(erule_tac Q = "?R = ?S" in contrapos_np) apply(simp add: dom_def)
  apply(frule_tac P' = P' in ftif_ty_opt) apply(simp) apply(simp)
 apply(clarsimp) apply(erule_tac Q = "?R = ?S" in contrapos_np) apply(simp add: dom_def)
  apply(frule_tac P' = P' in ftif_ty_opt) apply(simp)
 apply(simp)
apply(clarsimp)
done

lemma fpt_some:
  "\<lbrakk>(P, mi, P') \<in> wf_P_change; find_path_ty_f P ty = Some path\<rbrakk> \<Longrightarrow> find_path_ty_f P' ty = Some path"
apply(case_tac ty) apply(simp) apply(rename_tac ctx dcl)
apply(case_tac ctx, rename_tac mi' pn, clarsimp) apply(case_tac "mi = mi'")
 apply(clarsimp) apply(case_tac P, rename_tac RC MH, clarsimp) apply(frule wf_P_change_mi_dom)
 apply(unfold find_path_f_def) apply(frule fpr_some) apply(force) apply(assumption)
 apply(clarsimp split: split_if_asm option.splits)
apply(clarsimp simp add: fp_P acyclic_clds_P split: split_if_asm option.splits)
apply(frule_tac pn = pn and cl = "cl_fqn (fqn_def pn dcl)" and mi' = mi' in fp_P) apply(simp)
apply(clarsimp simp add: find_path_f_def acyclic_clds_P split: option.splits)
done

lemma sty_option_P:
  "\<lbrakk>(P, mi, P') \<in> wf_P_change; (P, ty_opt, ty_opt') \<in> sty_option\<rbrakk> \<Longrightarrow> (P', ty_opt, ty_opt') \<in> sty_option"
apply(clarsimp simp add: is_sty_opt_iff is_sty_opt_def is_sty_one_def split: option.splits ty.splits ctx.splits)
apply(frule fpt_some) apply(simp) apply(simp) apply(rule)
 apply(clarsimp) apply(frule fpt_some) apply(simp) apply(clarsimp)
apply(clarsimp) apply(rule)
 apply(clarsimp) apply(frule fc_some) apply(simp) apply(simp)
apply(clarsimp) apply(frule fc_some) apply(simp) apply(simp)
apply(frule fpt_some) apply(simp) apply(simp)
done

lemma ftype_some:
  "\<lbrakk>(P, mi, P') \<in> wf_P_change; ftype_f P ty f = Some ty'\<rbrakk> \<Longrightarrow> ftype_f P' ty f = Some ty'"
apply(clarsimp simp add: ftype_f_def fpt_some split: option.splits)
apply(case_tac P, rename_tac RC MH, clarsimp) apply(frule ftip_some) apply(simp) apply(simp)
done

lemma fmd_some:
  "\<lbrakk>(P, mi, P') \<in> wf_P_change; find_meth_def_f P ty meth = Some (ctx, md)\<rbrakk>
      \<Longrightarrow> find_meth_def_f P' ty meth = Some (ctx, md)"
by (clarsimp simp add: find_meth_def_f_def fpt_some split: option.splits)

lemma lift_opts_some[rule_format]:
  "\<forall>tys. lift_opts (map (vd_case (\<lambda>clk vark. find_type_f P ctx clk)) vds) = Some tys \<longrightarrow> (P, mi, P') \<in> wf_P_change
     \<longrightarrow> lift_opts (map (vd_case (\<lambda>clk vark. find_type_f P' ctx clk)) vds) = Some tys"
apply(induct vds) apply(simp) apply(clarsimp) apply(rename_tac vd vds tys) apply(case_tac vd, rename_tac clk vark, clarsimp)
apply(case_tac "find_type_f P ctx clk") apply(simp) apply(clarsimp)
apply(case_tac "lift_opts (map (vd_case (\<lambda>clk vark. find_type_f P ctx clk)) vds)") apply(simp) apply(clarsimp)
apply(frule ft_some) apply(simp) apply(simp)
done

lemma mtype_some:
  "\<lbrakk>(P, mi, P') \<in> wf_P_change; mtype_f P ty meth = Some mty\<rbrakk> \<Longrightarrow> mtype_f P' ty meth = Some mty"
apply(clarsimp simp add: mtype_f_def split: option.splits)
apply(frule fmd_some) apply(simp) apply(clarsimp simp add: split: meth_def.splits meth_sig.splits option.splits)
apply(frule ft_some) apply(simp) apply(simp) apply(frule lift_opts_some) apply(simp) apply(simp)
done

lemma wf_stmt_P[rule_format]:
  "(P, T, s) \<in> wf_stmt \<longrightarrow> (P, mi, P') \<in> wf_P_change \<longrightarrow> (P', T, s) \<in> wf_stmt"
apply(rule s_induct')
apply(clarsimp) apply(erule wf_stmtE, simp_all) apply(rule wf_blockI) apply(clarsimp)
apply(clarsimp) apply(erule wf_stmtE, simp_all) apply(rule wf_var_assignI) apply(simp add: sty_option_P)+
apply(clarsimp) apply(erule wf_stmtE, simp_all) apply(rule wf_field_readI) apply(simp add: ftype_some sty_option_P)+
apply(clarsimp) apply(erule wf_stmtE, simp_all) apply(rule wf_field_writeI) apply(simp add: ftype_some sty_option_P)+
apply(clarsimp) apply(erule wf_stmtE, simp_all) apply(rule wf_ifI) apply(force simp add: ftype_some sty_option_P)+
apply(clarsimp) apply(erule wf_stmtE, simp_all) apply(rule wf_mcallI) apply(force simp add: mtype_some sty_option_P)+
apply(clarsimp) apply(erule wf_stmtE, simp_all) apply(rule wf_newI) apply(frule ft_some) apply(simp) apply(simp)
apply(force simp add: sty_option_P)+
done

lemma wf_method_P:
  "\<lbrakk>(P, mi, P') \<in> wf_P_change; (P, ty, md) \<in> wf_meth\<rbrakk> \<Longrightarrow> (P', ty, md) \<in> wf_meth"
apply(erule wf_methE) apply(clarsimp) apply(rule wf_methodI) apply(simp)
apply(clarsimp) apply(rename_tac cl var ty) apply(drule_tac x = "(cl, var, ty)" in bspec, simp) apply(clarsimp)
apply(frule_tac cl = cl in ft_some) apply(simp) apply(simp) apply(simp) apply(clarsimp)
apply(rename_tac s) apply(drule_tac x = s in bspec, simp) apply(frule wf_stmt_P, simp+)
apply(frule ft_some) apply(simp) apply(simp) apply(simp add: sty_option_P)
done

lemma methods_some:
  "\<lbrakk>(P, mi, P') \<in> wf_P_change; methods_f P ty = Some ms\<rbrakk> \<Longrightarrow> methods_f P' ty = Some ms"
by (simp add: methods_f_def fpt_some split: option.splits)

lemma fields_some:
  "\<lbrakk>(P, mi, P') \<in> wf_P_change; fields_f P ty = Some fs\<rbrakk> \<Longrightarrow> fields_f P' ty = Some fs"
by (simp add: fields_f_def fpt_some split: option.splits)

lemma wf_class_P:
  "\<lbrakk>(P, mi, P') \<in> wf_P_change; (P, mi', cld) \<in> wf_class\<rbrakk> \<Longrightarrow> (P', mi', cld) \<in> wf_class"
apply(erule wf_classE) apply(clarsimp) apply(rule wf_classI) apply(erule wf_class_cE) apply(clarsimp)
apply(rule wf_class_commonI[simplified]) apply(frule ft_some) apply(simp) apply(simp) apply(simp) apply(simp)
apply(frule fields_some) apply(simp) apply(simp) apply(simp)
apply(clarsimp) apply(rename_tac cl f ty) apply(drule_tac x = "(cl, f, ty)" in bspec, simp) apply(clarsimp)
apply(frule_tac cl = cl in ft_some) apply(simp) apply(simp)
apply(clarsimp) apply(rename_tac md m') apply(drule_tac x = "(md, m')" in bspec, simp)+ apply(clarsimp)
apply(simp add: wf_method_P) apply(simp) apply(simp) apply(simp add: methods_some)
apply(clarsimp) apply(rename_tac m' mty mty') apply(drule_tac x = "(m', mty, mty')" in bspec, simp)+ apply(simp add: mtype_some)
apply(clarsimp) apply(rename_tac m' mty mty') apply(drule_tac x = "(m', mty, mty')" in bspec, simp)+ apply(simp add: mtype_some)
apply(simp)
done

lemma wf_md_P:
  "\<lbrakk>(P, mi, P') \<in> wf_P_change; (P, mi', md) \<in> wf_md\<rbrakk> \<Longrightarrow> (P', mi', md) \<in> wf_md"
apply(erule wf_mdE) apply(clarsimp) apply(case_tac P', rename_tac RC' MH', clarsimp)
apply(rule_tac md = md and mibrs = mibrs in wf_moduleI[simplified]) apply(assumption+)
apply(clarsimp) apply(rename_tac cld fqn) apply(drule_tac x = "(cld, fqn)" in bspec, simp)+ apply(clarsimp) apply(simp add: wf_class_P)
apply(simp add: acyclic_clds_mi_P) apply(frule wf_P_change_map_le) apply(simp add: map_le_def) apply(drule_tac x = mi' in bspec, simp add: domI)
apply(simp add: ncrim_P)
done

lemma wf_object_P:
  "\<lbrakk>(P, mi, P') \<in> wf_P_change; (P, H, ty_opt, ty_opt') \<in> wf_object\<rbrakk> \<Longrightarrow> (P', H, ty_opt, ty_opt') \<in> wf_object"
apply(erule wf_objectE) apply(clarsimp) apply(rule wf_nullI) apply(simp) apply(clarsimp) apply(rule wf_objectI) by (simp add: sty_option_P)

lemma wf_heap_P:
  "\<lbrakk>(P, mi, P') \<in> wf_P_change; (P, H) \<in> wf_heap\<rbrakk> \<Longrightarrow> (P', H) \<in> wf_heap"
apply(erule wf_heapE) apply(clarsimp) apply(rule wf_heapI) apply(simp) apply(clarsimp) apply(rename_tac ty fvs)
apply(drule_tac x = oid in bspec, simp add: domI) apply(clarsimp) apply(rule_tac x = fs in exI) apply(simp add: fields_some)
apply(clarsimp) apply(drule_tac x = f in bspec, simp) apply(clarify) apply(rule_tac x = ty' in exI)
by (simp add: ftype_some wf_object_P)

lemma wf_varstate_P:
  "\<lbrakk>(P, mi, P') \<in> wf_P_change; (P, G, H, L) \<in> wf_varstate\<rbrakk> \<Longrightarrow> (P', G, H, L) \<in> wf_varstate"
apply(erule wf_varstateE) apply(clarsimp) apply(rule wf_varstateI) apply(simp) apply(clarsimp)
apply(drule_tac x = x in bspec, simp add: domI) apply(simp add: wf_object_P)
done

lemma wf_RMIS_rm:
  "(MH, RMIS) \<in> wf_rmis \<Longrightarrow> (MH, \<lambda>x. if x = md_c then None else RMIS x) \<in> wf_rmis"
apply(erule wf_rmisE) apply(rule wf_rmisI) apply(clarsimp) done

lemma wf_r_P:
  "\<lbrakk>RC (R_name_f R) = Some R; R_body_f R = (mds_c, RMIS); (p_def RC MH, R) \<in> wf_r;
    \<forall>rn\<in>dom RC. \<exists>R. RC rn = Some R \<and> R_name_f R = rn \<and> (p_def RC MH, R) \<in> wf_r;
    RMIS' = (RMIS(md_c \<mapsto> case RMIS md_c of None \<Rightarrow> [imp_dep \<mapsto> mi] | Some idmi \<Rightarrow> idmi(imp_dep \<mapsto> mi)));
    R' = R_update_f R mds_c RMIS'\<rbrakk>
       \<Longrightarrow> (p_def (RC(R_name_f R \<mapsto> R')) (MH(mi \<mapsto> (md, mibrs))), R') \<in> wf_r"
apply(case_tac R)
 apply(rename_tac mds RMIS'') apply(clarsimp simp add: R_body_f_def R_name_f_def R_update_f_def) apply(erule wf_rE)
 apply(clarsimp) apply(rule wf_bootstrap_repI) apply(simp) apply(erule wf_rmisE) apply(clarsimp)
 apply(rule wf_rmisI) apply(clarsimp split: option.splits) apply(simp)
apply(rename_tac r rn mds RMIS'') apply(clarsimp simp add: R_body_f_def R_name_f_def R_update_f_def)
apply(drule_tac x = "rn_standard r" in bspec, simp add: domI) apply(clarsimp) apply(erule wf_rE) apply(simp) apply(clarsimp)
apply(rule wf_normal_repI) apply(simp) apply(force) apply(erule wf_rmisE) apply(rule wf_rmisI) apply(clarsimp split: option.splits)
done

(*
lemma imp_mi_br_list_dom[THEN mp]:
  "(\<forall>x\<in>set imp_mi_br_list. case (\<lambda>(imp, mi, br). init_def mi rn imp) x of init_def mi rn m \<Rightarrow> mi \<in> dom MH)
       \<longrightarrow> set (mis_of (map snd imp_mi_br_list)) \<subseteq> dom MH"
by (induct imp_mi_br_list, auto simp add: mis_of_def)
*)

lemma ia_instance_map_map:
  "\<exists>rn. map (\<lambda>(imp, mi, br). ia_instance mi rn2 imp) imp_mi_br_list = map (\<lambda>(imp, mi). ia_instance mi rn imp) (map (\<lambda>(imp, mi, br). (imp, mi)) imp_mi_br_list)"
apply(rule_tac x = rn2 in exI) by (induct imp_mi_br_list, auto)

lemma imp_mi_br_list_fst_snd:
  "snd ` (\<lambda>(imp, mi, br). (imp, mi)) ` set imp_mi_br_list = fst ` snd ` set imp_mi_br_list"
by (induct imp_mi_br_list, auto)

lemma mi_infinite:
  "infinite (UNIV :: mi set)"
apply(simp add: infinite_iff_countable_subset)
apply(rule_tac x = "\<lambda>n. replicate n c" in exI) apply(rule linorder_injI)
apply(clarify) apply(frule replicate_eq_length) apply(simp)
done

lemma fresh_mi:
  "p_def RC MH \<in> wf_p \<Longrightarrow> \<exists>mi. mi \<notin> dom MH"
apply(erule wf_programE) apply(erule wf_mhE) apply(erule acyclic_mh.cases) apply(clarsimp)
apply(rule ex_new_if_finite) apply(rule mi_infinite) apply(assumption)
done

lemma map_snd': "map (\<lambda>(x, y). id y) list = map snd list" by (induct list, auto)

lemma wf_internal_action_preservation[rule_format]:
  "(config, ias, config') \<in> r_action \<Longrightarrow> \<forall>G. (G, config) \<in> wf_config \<longrightarrow>
      ((\<exists>G'. G \<subseteq>\<^sub>m G' \<and> (G', config') \<in> wf_config) \<and>
       (\<forall>RC MH L H ss imp_mi_list rn. config = config_normal (p_def RC MH) L H ss \<and> (MH, RC) \<in> wf_rc \<and> ias = map (\<lambda>(imp, mi). ia_instance mi rn imp) imp_mi_list
          \<longrightarrow> (\<forall>RC' MH'. config' = config_normal (p_def RC' MH') L H ss
              \<longrightarrow> dom MH \<subseteq> dom MH' \<and> set (map snd imp_mi_list) \<subseteq> dom MH')))"
apply(induct rule: r_action.induct)

(* r_no_action *)
apply(force)

(* r_action_list *)
apply(rule) apply(rule) apply(rule)
 apply(clarsimp) apply(erule_tac x = G in allE) apply(clarsimp) apply(erule_tac x = G' in allE) apply(clarsimp) apply(rename_tac G'')
 apply(rule_tac x = G'' in exI) apply(clarsimp) apply(rule map_le_trans) apply(simp) apply(simp)
apply(clarsimp) apply(rename_tac m mi m_mi_list)
apply(erule_tac x = G in allE) apply(clarsimp) apply(erule_tac x = G' in allE) apply(clarsimp) apply(rename_tac G'')
apply(case_tac P', rename_tac RC'' MH'', clarsimp) apply(erule_tac x = "[(m,mi)]" in allE) apply(erule_tac x = m_mi_list in allE) apply(clarsimp)
apply(erule_tac ?a1.0 = G' in wf_configE) apply(rename_tac H \<Gamma> L Exception) apply(simp) apply(clarsimp) apply(rename_tac s_list)
apply(erule wf_programE) apply(clarsimp) apply(rename_tac MH'' RC'') apply(erule impE) apply(force)
apply(clarsimp) apply(frule subset_trans) apply(simp) apply(clarsimp) apply(frule_tac A = "dom MH''" and c = mi and B = "dom MH'" in subsetD)
apply(force) apply(force)

(* r_install *)
apply(rule) apply(rule) apply(rule)
 apply(clarsimp) apply(rule_tac x = G in exI) apply(erule wf_configE) apply(simp) apply(clarsimp)
 apply(frule fresh_mi) apply(erule exE) apply(frule_tac RMIS = RMIS in wrc_installI, simp+)
 apply(erule wf_programE) apply(thin_tac "mi \<notin> dom MH") apply(clarsimp) apply(rule wf_allI)
     apply(rule wf_pI) apply(erule wf_rcE) apply(clarsimp) apply(rename_tac R_core)
     apply(frule_tac x = rn in bspec, simp add: domI) apply(frule_tac x = rn_bootstrap in bspec, simp add: domI) apply(clarsimp)
     apply(rule wf_rcI) apply(clarsimp) apply(rule) apply(clarsimp simp add: R_name_f_def R_update_f_def split: R.splits) apply(rule)
      apply(case_tac R)
       apply(rename_tac mds RMIS) apply(clarsimp simp add: R_body_f_def R_name_f_def R_update_f_def) apply(erule wf_rE) apply(clarsimp)
       apply(frule_tac md = md_c in fmim_add) apply(clarify) apply(rule wf_bootstrap_repI) apply(simp) apply(simp) apply(simp)
      apply(rename_tac r rn mds RMIS) apply(clarsimp simp add: R_body_f_def R_name_f_def R_update_f_def split: R.splits) apply(elim wf_rE) apply(clarsimp)
      apply(frule_tac md = md_c in fmim_add) apply(clarify) apply(rule wf_normal_repI) apply(simp) apply(force) apply(simp) apply(simp) apply(simp)
     apply(clarsimp) apply(rename_tac R') apply(case_tac R)
      apply(rename_tac mds RMIS) apply(clarsimp simp add: R_name_f_def R_body_f_def R_update_f_def) apply(rule)
       apply(clarsimp) apply(erule wf_rE) apply(frule_tac md = md_c in fmim_add) apply(clarsimp) apply(rule wf_bootstrap_repI)
       apply(simp) apply(simp) apply(simp) apply(clarsimp) apply(case_tac R') apply(rename_tac mds RMIS) apply(clarsimp)
       apply(drule_tac x = rn in bspec, simp add: domI) apply(simp)
      apply(rename_tac r rn' mds RMIS) apply(clarsimp) apply(drule_tac x = rn in bspec, simp add: domI) apply(clarsimp) apply(elim wf_rE) apply(simp)
      apply(clarsimp) apply(frule_tac md = md_c in fmim_add) apply(clarsimp) apply(case_tac "rn = rn_bootstrap") apply(rule wf_normal_repI) apply(simp)
      apply(simp) apply(simp) apply(rule wf_normal_repI) apply(simp) apply(simp add: dom_def) apply(simp) apply(simp) apply(simp)
     apply(rename_tac r rn' mds RMIS) apply(clarsimp simp add: R_name_f_def R_body_f_def R_update_f_def) apply(rule)
      apply(clarsimp) apply(erule wf_rE) apply(frule_tac md = md_c in fmim_add) apply(clarsimp) apply(clarsimp) apply(case_tac "rn = rn_standard ra")
      apply(rule wf_normal_repI) apply(simp) apply(simp) apply(simp) apply(rule wf_normal_repI) apply(simp) apply(simp add: dom_def) apply(simp)
     apply(clarsimp) apply(drule_tac x = rn in bspec, simp add: domI) apply(clarsimp) apply(erule_tac ?a2.0 = R' in wf_rE)
      apply(clarsimp) apply(rule wf_bootstrap_repI) apply(simp) apply(simp) apply(clarsimp) apply(case_tac "rn = rn_standard r") apply(rule wf_normal_repI)
      apply(simp) apply(simp) apply(simp) apply(rule wf_normal_repI) apply(simp) apply(simp add: dom_def) apply(simp add: domI)
    apply(clarsimp) apply(erule wf_mhE) apply(clarsimp) apply(rule wf_mhI) apply(simp) apply(clarsimp) apply(drule_tac x = mia in bspec, simp add: domI)
    apply(clarsimp) apply(rename_tac md mis) apply(erule wf_mdE) apply(clarsimp) apply(rule wf_moduleI[simplified]) apply(simp) apply(simp) apply(clarsimp)
    apply(rename_tac cld fqn) apply(drule_tac x = "(cld, fqn)" in bspec, simp add: domI)+ apply(clarsimp) apply(simp add: wf_class_P)
    apply(simp add: acyclic_clds_mi_P) apply(force simp add: ncrim_P) apply(simp add: acyclic_clds_P)
   apply(simp add: wf_heap_P)
  apply(simp add: wf_varstate_P)
 apply(clarsimp) apply(rename_tac s) apply(drule_tac x = s in bspec, simp) apply(simp add: wf_stmt_P)
apply(clarsimp)

(* r_uninstall *)
apply(rule) apply(rule) apply(rule)
 apply(clarsimp) apply(rule_tac x = G in exI) apply(erule wf_configE) apply(simp) apply(clarsimp)
 apply(frule fresh_mi) apply(erule exE) apply(frule_tac RMIS = RMIS in wrc_uninstallI, simp+)
 apply(erule wf_programE) apply(thin_tac "mi \<notin> dom MH") apply(clarsimp) apply(rule wf_allI)
    apply(rule wf_pI)
     apply(erule wf_rcE) apply(clarsimp) apply(rename_tac R_core) apply(frule_tac x = rn in bspec, simp add: domI)
     apply(frule_tac x = rn_bootstrap in bspec, simp add: domI) apply(clarsimp) apply(rule wf_rcI)
      apply(clarsimp) apply(rule) apply(clarsimp simp add: R_name_f_def R_update_f_def split: R.splits) apply(rule) apply(case_tac R)
        apply(rename_tac mds RMIS) apply(clarsimp simp add: R_body_f_def R_name_f_def R_update_f_def) apply(erule wf_rE) apply(clarsimp)
         apply(rule_tac md_c = md_ca in wf_bootstrap_repI) apply(frule fmim_md_name) apply(simp add: fmim_mds_rm) apply(simp add: wf_RMIS_rm) apply(simp)
       apply(rename_tac r rn mds RMIS) apply(clarsimp simp add: R_body_f_def R_name_f_def R_update_f_def split: R.splits) apply(elim wf_rE) apply(clarsimp)
         apply(clarify) apply(rule wf_normal_repI) apply(simp) apply(force) apply(simp add: wf_RMIS_rm) apply(simp) apply(simp)
      apply(clarsimp) apply(rename_tac R') apply(case_tac R)
       apply(rename_tac mds RMIS) apply(clarsimp simp add: R_name_f_def R_body_f_def R_update_f_def) apply(rule)
        apply(clarsimp) apply(erule wf_rE) apply(clarsimp) apply(rule_tac md_c = md_ca in wf_bootstrap_repI) apply(frule fmim_md_name)
        apply(simp add: fmim_mds_rm) apply(simp add: wf_RMIS_rm) apply(simp) apply(clarsimp) apply(case_tac R')
        apply(rename_tac mds RMIS) apply(clarsimp) apply(drule_tac x = rn in bspec, simp add: domI) apply(simp)
       apply(rename_tac r rn' mds RMIS) apply(clarsimp) apply(drule_tac x = rn in bspec, simp add: domI) apply(clarsimp) apply(elim wf_rE) apply(simp)
         apply(clarsimp) apply(case_tac "rn = rn_bootstrap") apply(rule wf_normal_repI) apply(simp) apply(simp) apply(simp) apply(rule wf_normal_repI)
           apply(simp) apply(simp add: dom_def) apply(simp) apply(simp) apply(simp)
      apply(rename_tac r rn' mds RMIS) apply(clarsimp simp add: R_name_f_def R_body_f_def R_update_f_def) apply(rule)
       apply(clarsimp) apply(erule wf_rE) apply(clarsimp) apply(case_tac "rn = rn_standard ra") apply(rule wf_normal_repI) apply(simp) apply(simp)
        apply(simp) apply(rule wf_normal_repI) apply(simp) apply(simp) apply(simp add: wf_RMIS_rm)
      apply(clarsimp) apply(drule_tac x = rn in bspec, simp add: domI) apply(clarsimp) apply(erule_tac ?a2.0 = R' in wf_rE)
       apply(clarsimp) apply(rule wf_bootstrap_repI) apply(simp) apply(simp) apply(clarsimp) apply(case_tac "rn = rn_standard r") apply(rule wf_normal_repI)
         apply(simp) apply(simp) apply(simp) apply(rule wf_normal_repI) apply(simp) apply(simp add: dom_def) apply(simp) apply(simp add: domI)
    apply(erule wf_mhE) apply(clarsimp) apply(rule wf_mhI) apply(clarsimp) apply(clarsimp) apply(drule_tac x = mia in bspec, simp add: domI) apply(clarsimp)
    apply(rename_tac md mis) apply(erule wf_mdE) apply(clarsimp) apply(rule wf_moduleI[simplified]) apply(simp) apply(simp) apply(clarsimp)
    apply(rename_tac cld fqn) apply(drule_tac x = "(cld, fqn)" in bspec, simp add: domI)+ apply(clarsimp)
    apply(simp add: wf_class_P) apply(simp add: acyclic_clds_mi_P) apply(force simp add: ncrim_P) apply(simp add: acyclic_clds_P)
   apply(simp add: wf_heap_P)
  apply(simp add: wf_varstate_P)
 apply(clarsimp) apply(rename_tac s) apply(drule_tac x = s in bspec, simp) apply(simp add: wf_stmt_P)
apply(clarsimp)

(* r_existing_instance *)
apply(rule) apply(rule) apply(rule)
 apply(rule_tac x = G in exI) apply(simp)
apply(clarsimp split: option.splits) apply(rename_tac idmis)
apply(erule wf_rcE) apply(clarsimp) apply(drule_tac x = rn2 in bspec, simp add: domI) apply(clarsimp)
apply(erule wf_rE)
 apply(clarsimp) apply(erule wf_rmisE) apply(clarsimp simp add: R_name_f_def R_body_f_def)
 apply(erule_tac x = md_c in allE) apply(erule_tac x = imp_dep in allE) apply(erule_tac x = mi in allE)
 apply(clarsimp)
apply(clarsimp) apply(erule wf_rmisE) apply(clarsimp simp add: R_name_f_def R_body_f_def)
apply(erule_tac x = md_c in allE) apply(erule_tac x = imp_dep in allE) apply(erule_tac x = mi in allE)
apply(clarsimp)

(* r_new_instance *)
apply(rule) apply(rule) apply(rule)
 (* wf_action *)
 apply(erule_tac x = G in allE) apply(simp) apply(elim conjE exE) apply(rule_tac x = G' in exI) apply(clarsimp)
 apply(erule wf_configE) apply(simp) apply(clarsimp)
 apply(erule contrapos_np) apply(clarsimp)
 apply(erule wf_configE) apply(simp) apply(clarsimp) apply(erule wf_programE) apply(clarsimp)
 apply(erule_tac x = "map (\<lambda>(imp, mi, br). (imp, mi)) imp_mi_br_list" in allE) apply(clarsimp)
 apply(erule impE) apply(rule ia_instance_map_map) apply(clarsimp)
 apply(frule_tac mi = mi and rn = rn2 and R = R2' and mds_c = mds_c3 and RMIS = RMIS3 and mi_br_list = "map snd imp_mi_br_list" and
                 md_c = "md_c_def repl (mn_std m) clds_c (map (\<lambda>(imp, mi, br). imp) imp_mi_br_list) fqns" and m = m in wrc_new_instanceI)
  apply(force) apply(simp) apply(simp) apply(simp add: dom_def) apply(simp only: imp_mi_br_list_fst_snd) apply(simp add: md_name_f_def)
  apply(simp) apply(simp) apply(simp) apply(simp add: map_snd')
 apply(erule wf_programE) apply(clarsimp)
 apply(rule wf_allI)
    apply(rule wf_pI)
      apply(erule wf_rcE)+ apply(clarsimp) apply(rename_tac RC' MH' RC MH R_core' R_core)
      apply(frule_tac x = rn2 in bspec, simp add: domI) apply(frule_tac x = rn2 in bspec, simp add: domI) back
      apply(frule_tac x = rn_bootstrap in bspec, simp add: domI) back apply(clarsimp) apply(rule wf_rcI)
       apply(clarsimp) apply(rule) apply(clarsimp simp add: R_name_f_def R_update_f_def split: R.splits)
       apply(rule) apply(drule_tac s = "R_name_f R2'" in sym) apply(simp) apply(rule wf_r_P) apply(assumption) apply(force) apply(simp) apply(simp) apply(simp) apply(simp)
       apply(clarsimp) apply(rename_tac R) apply(rule)
        apply(clarsimp) apply(rule) apply(clarsimp simp add: R_name_f_def R_update_f_def split: R.splits)
        apply(drule_tac s = "R_name_f R2'" in sym) apply(simp) apply(rule wf_r_P)  apply(assumption) apply(force) apply(simp) apply(simp) apply(simp) apply(simp)
       apply(clarsimp) apply(frule_tac x = rn in bspec, simp add: domI) apply(clarsimp) apply(erule_tac ?a2.0 = R in wf_rE)
        apply(clarsimp) apply(rule wf_bootstrap_repI) apply(simp) apply(erule wf_rmisE) apply(rule wf_rmisI) apply(clarsimp)
       apply(clarsimp simp add: R_name_f_def) apply(drule_tac x = "rn_standard r" in bspec, simp add: domI) apply(clarsimp)
       apply(erule_tac ?a2.0 = "r_standard r rn mds_c RMIS" in wf_rE) apply(simp)
       apply(clarsimp) apply(rule wf_normal_repI) apply(simp) apply(simp add: dom_def) apply(erule wf_rmisE) apply(rule wf_rmisI) apply(clarsimp)
      apply(simp add: dom_def)
     apply(erule wf_mhE)+ apply(clarsimp) apply(rule wf_mhI)
      apply(frule wf_P_change_mi_dom) apply(frule_tac MH = MHc and mi = mi and md' = md and mibrs' = "map snd imp_mi_br_list" in acyclic_mh_add)
      apply(simp) apply(simp add: mis_of_def imp_mi_br_list_fst_snd) apply(simp add: map_snd')
     apply(clarsimp) apply(drule_tac x = mia in bspec, simp add: domI) apply(clarsimp)
     apply(simp add: wf_md_P map_snd')
    apply(simp add: acyclic_clds_P map_snd')
   apply(simp add: wf_heap_P map_snd')
  apply(frule wf_varstate_P) apply(simp) apply(simp add: map_snd')
  apply(simp add: wf_varstate_P map_snd')
 apply(clarsimp) apply(rename_tac s) apply(drule_tac x = s in bspec, simp)+ apply(blast intro: wf_stmt_P)
apply(clarsimp) apply(erule_tac x = G in allE) apply(clarsimp)
apply(erule_tac x = "map (\<lambda>(imp, mi, br). (imp, mi)) imp_mi_br_list" in allE) apply(clarsimp)
apply(erule impE) apply(rule ia_instance_map_map) apply(clarsimp)
apply(frule_tac c = x in subsetD) apply(simp add: dom_def)+

done


lemma wf_action_preservation[rule_format]:
  "\<lbrakk>(config, a, config') \<in> admin_action; (G, config) \<in> wf_config\<rbrakk> \<Longrightarrow> \<exists>G'. G \<subseteq>\<^sub>m G' \<and> (G', config') \<in> wf_config"
apply(induct rule: admin_action.induct)
apply(force simp add: wf_internal_action_preservation)+
done


theorem wf_preservation:
  "\<And>G config a.
       \<lbrakk>(G, config) \<in> wf_config; (config, config') \<in> r_stmt \<or> (config, a, config') \<in> admin_action\<rbrakk>
       \<Longrightarrow> \<exists>G'. G \<subseteq>\<^sub>m G' \<and> (G', config') \<in> wf_config"
apply(erule disjE)

apply(erule r_stmt.cases)

(* s_read_npe, s_write_npe *)

(* G' = G for all cases except for mcall (case 11) *)
apply(rule_tac[1-10] x = G in exI)
apply(erule_tac[1-11] wf_configE)
apply(simp_all)

(* s_if s_block *)

apply(clarsimp) apply(erule wf_stmtE) apply(simp_all)
apply(force intro: wf_config_normalI)

(* s_ass *)

apply(clarsimp) apply(erule wf_stmtE) apply(simp_all)
apply(rule wf_config_normalI, assumption+)
 apply(erule sty_option.cases)
 apply(rule wf_subvarstateI, assumption+, simp)
 apply(erule wf_varstateE)
 apply(drule_tac x = x in bspec, simp add: domI)
 apply(erule wf_objectE)
  apply(simp add: wf_nullI)
 apply(clarsimp)
 apply(rule wf_objectI)
 apply(erule sty_option.cases, simp)
 apply(rule sty_optionI, simp+)
apply(rule_tac ty' = ty'a in sty_transitiveI, assumption+)

(* s_read *)

apply(force intro: wf_intros)

apply(clarsimp split: option.splits) apply(erule wf_stmtE) apply(simp_all)
apply(rule wf_config_normalI, assumption+)
 prefer 2 apply(assumption)
apply(clarsimp)
apply(rename_tac L oid H v s_list ty_oid fs_oid \<Gamma> x ty_x P f ty_f var)

apply(erule sty_option.cases)
apply(rule wf_subvarstateI, assumption, simp)
apply(clarsimp)
apply(case_tac v)
 apply(clarify)
 apply(rule wf_nullI, simp)
apply(clarify)

apply(rename_tac ty_f ty_var P oid_v)

apply(erule wf_heapE)
apply(drule_tac x = oid in bspec, simp add: domI)
apply(clarsimp)
apply(rename_tac H P fs_oid)

apply(erule wf_varstateE)
apply(frule_tac x = x in bspec, simp add: domI)
apply(clarsimp)
apply(erule wf_objectE)
 apply(simp)
apply(erule sty_option.cases)
apply(clarsimp split: option.splits)
apply(rename_tac L \<Gamma> H oid_x ty_x_d ty_x_s P)

apply(frule_tac ty_x_s = ty_x_s in no_field_hiding, simp+)
apply(drule_tac x = f in bspec, simp)
apply(clarsimp)
apply(frule ftype_preservation[simplified], assumption+)
apply(clarsimp)
apply(rename_tac ty_f)

apply(erule wf_objectE)
 apply(simp)
apply(clarsimp)
apply(erule sty_option.cases)
apply(clarsimp split: option.splits)
apply(rename_tac H oid_v ty_f P ty_v fs_v)

apply(rule wf_objectI)
apply(rule sty_optionI, simp+)
apply(rule sty_transitiveI, assumption+)

(* s_write *)

apply(force intro: wf_intros)

apply(clarsimp) apply(erule wf_stmtE) apply(simp_all)
apply(clarsimp split: option.splits) apply(rule)
 apply(erule wf_varstateE) apply(clarsimp) apply(rename_tac \<Gamma> P H)
 apply(drule_tac x = xa in bspec, simp add: domI)
 apply(erule wf_objectE) apply(simp) apply(clarsimp)
 apply(elim sty_option.cases) apply(simp)
apply(erule sty_option.cases)
apply(clarsimp)
apply(rule wf_config_normalI)
  apply(assumption)
  prefer 3
  apply(assumption)
 prefer 2
 apply(rename_tac L oid_x v H ss \<Gamma> x ty_x_s f y ty_y_s ty_f P ty_x_d fs_x)
 apply(erule wf_varstateE)
 apply(rule wf_varstateI) apply(simp)
 apply(clarsimp)
 apply(rename_tac L \<Gamma> P H x' y')
 apply(drule_tac x = x' in bspec, simp add: domI)
 apply(clarsimp)
 apply(erule wf_objectE)
  apply(clarsimp)
  apply(rule wf_nullI, simp)
 apply(clarsimp)
 apply(erule sty_option.cases)
 apply(clarsimp split: option.splits)
 apply(rename_tac H oid_x' ty_x'_s P ty_x'_d fs_x')
 apply(rule wf_objectI)
 apply(rule sty_optionI)
   apply(clarsimp)
   apply(rule conjI)
    apply(clarsimp)
    apply(simp)
   apply(clarsimp)
  apply(simp)
 apply(simp)

apply(rename_tac L oid_x v H ss \<Gamma> x ty_x_s f y ty_y_s ty_f P ty_x_d fs_oid)

apply(erule wf_heapE)
apply(rule wf_heapI) apply(simp)
apply(rule ballI) apply(clarsimp simp add: map_add_def) apply(rule)
 apply(clarsimp) apply(drule_tac x = oid_x in bspec, simp add: domI) apply(clarsimp)
 apply(drule_tac x = fa in bspec, simp) apply(clarsimp)
 apply(rule)
  apply(clarsimp) apply(case_tac v) apply(clarsimp simp add: wf_nullI) apply(clarsimp)
  apply(rename_tac H P fields_x_d ty_f_d oid_v)
  apply(erule wf_varstateE) apply(clarsimp)
  apply(frule ftype_preservation, assumption+) apply(clarsimp)
  apply(drule_tac x = y in bspec, simp add: domI) apply(clarsimp)
  apply(erule wf_objectE) back apply(simp) apply(clarsimp)
  apply(erule sty_option.cases) apply(clarsimp split: option.splits)
  apply(rule wf_objectI) apply(force intro: sty_optionI sty_transitiveI)
 apply(clarsimp) apply(case_tac "fs_oid fa") apply(clarsimp) apply(force elim: wf_objectE)
 apply(case_tac a) apply(force intro: wf_nullI)
 apply(clarsimp) apply(rename_tac H P fields_x_d f ty_f_d oid_v)
 apply(erule wf_varstateE) apply(clarsimp)
 apply(drule_tac x = y in bspec, simp add: domI) apply(clarsimp)
 apply(erule wf_objectE) apply(simp) apply(clarsimp)
 apply(rule wf_objectI) apply(erule sty_option.cases) apply(clarsimp split: option.splits)
 apply(safe) apply(clarsimp) apply(force intro: sty_optionI) apply(force intro: sty_optionI)
apply(drule_tac x = oid in bspec) apply(clarsimp)
apply(clarsimp) apply(drule_tac x = fa in bspec, simp)
apply(clarsimp simp add: wf_object_heap)

(* s_if *)

apply(erule wf_stmtE) apply(simp_all)
apply(force intro: wf_config_normalI)

apply(erule wf_stmtE) apply(simp_all)
apply(force intro: wf_config_normalI)

(* s_new *)

apply(erule contrapos_np)
apply(erule wf_stmtE, simp_all, clarsimp)
apply(erule sty_option.cases, clarsimp)

apply(rule wf_config_normalI)
   apply(assumption)
  prefer 3 apply(simp)
 apply(rename_tac H L ss ctx cl \<Gamma> var ty' ty_var P)
 apply(erule wf_heapE)
 apply(rule wf_heapI) apply(simp)
 apply(safe) apply(simp add: map_upd_Some_unfold) apply(split split_if_asm)
  apply(clarsimp) apply(frule field_has_type, simp+)
  apply(erule exE) apply(rule_tac x = ty in exI) apply(simp) apply(force intro: wf_nullI)
 apply(drule_tac x = oida in bspec, simp add: domI) apply(clarsimp split: option.splits)
 apply(drule_tac x = f in bspec, simp) apply(safe) apply(rule_tac x = ty'a in exI) apply(simp)
 apply(erule wf_objectE) apply(clarsimp) apply(force intro: wf_nullI)
 apply(erule sty_option.cases) apply(clarsimp split: option.splits)
 apply(rule wf_objectI) apply(clarsimp) apply(rule conjI) apply(force)
 apply(force intro: sty_optionI)
apply(rename_tac oid_new H L ss ctx cl \<Gamma> var ty_new ty_var P)
apply(erule wf_varstateE) apply(clarsimp)
apply(rule wf_varstateI) apply(simp) apply(rule ballI) apply(drule_tac x = x in bspec, simp)
apply(clarsimp) apply(rule conjI)
 apply(clarsimp) apply(rule wf_objectI) apply(clarsimp) apply(force intro: sty_optionI)
apply(rule) apply(erule wf_objectE) apply(clarsimp) apply(force intro: wf_nullI)
apply(erule sty_option.cases) apply(clarsimp split: option.splits)
apply(rule wf_objectI) apply(clarsimp) apply(rule) apply(rule) apply(force)
apply(rule) apply(force intro: sty_optionI)

(* s_call *)

apply(force intro: wf_all_exI)

(* setting the new type environment *)
apply(case_tac "H oid", simp) apply(clarsimp)
apply(erule wf_stmtE, simp_all, clarsimp)
apply(frule wf_method_from_find[simplified]) apply(simp) apply(safe)
apply(erule_tac Q = "\<forall>G'. \<Gamma>' \<subseteq>\<^sub>m G' \<longrightarrow> (G', config_normal Pa ((L ++ map_of (map (\<lambda>(y_XXX, cl_XXX, var_XXX, var_', y). (x_var var_', y))
                     y_cl_var_var'_v_list)) (x' \<mapsto> v_oid oid)) H (map fst s''_s'_list @ s_ass vara (case if y = x_this then Some x'
                         else map_of (map (\<lambda>(y_XXX, cl_XXX, var_XXX, var_', v_XXX). (x_var var_XXX, x_var var_')) y_cl_var_var'_v_list)
                               y of None \<Rightarrow> y | Some x' \<Rightarrow> x') # s_list)) \<notin> wf_config" in contrapos_pp) apply(simp only: not_all)
apply(rule_tac x = "\<Gamma>' ++
                    map_of (map (\<lambda>((y, cl, var, var', v), (y', ty)). (x_var var', ty)) (zip y_cl_var_var'_v_list y_ty_list)) ++
                    empty (x' \<mapsto> ty_def ctx dcl)" in exI)
apply(clarsimp split del: split_if) apply(rule)
 apply(clarsimp simp add: map_le_def split del: split_if) apply(rule sym)
 apply(rule_tac L = L and Pa = Pa and H = H in map_of_map_and_x) apply(assumption+) apply(simp add: not_dom_is_none) apply(erule wf_varstateE) apply(clarsimp)
apply(rename_tac ss ty_x_d fs_x y_ty_list \<Gamma> x ty_x_s P meth ty_r var dcl)
apply(erule sty_option.cases) apply(clarsimp split del: split_if) apply(rename_tac ty_r ty_var P)
apply(erule wf_varstateE, clarify) apply(rename_tac L \<Gamma> P H)

apply(frule_tac x = x in bspec, simp add: domI)
apply(frule_tac x = "x_var var" in bspec, simp add: domI)
apply(clarsimp split del: split_if)
apply(erule wf_objectE, simp, clarsimp split del: split_if) apply(rename_tac P H oid)
apply(erule sty_option.cases, clarsimp split del: split_if) apply(rename_tac ty_x_d ty_x_s P)
apply(subgoal_tac "x_var var \<in> dom L") prefer 2 apply(erule wf_objectE) apply(force) apply(force)
apply(clarify) apply(rename_tac v_var)
apply(drule not_dom_is_none)

apply(rule wf_config_normalI)
   apply(assumption)
  apply(assumption)

 (* varstate *)
 apply(rule wf_varstateI) apply(simp only: finite_super_varstate) apply(clarsimp) apply(rule)
  apply(rule wf_objectI) apply(simp) apply(rule sty_optionI, simp+)
 apply(clarsimp) apply(rule) apply(rule) apply(rule wf_objectI) apply(clarsimp) apply(rule sty_optionI, simp+)
 apply(rule) apply(erule disjE)
  apply(clarsimp) apply(drule map_of_is_SomeD) apply(clarsimp) apply(rename_tac y_k cl_k var_k var'_k v_k y'_k ty_k)
  apply(frule_tac x = "(y_k, cl_k, var_k, var'_k, v_k)" in bspec) apply(force simp add: set_zip) apply(clarsimp)
  apply(subgoal_tac "map_of (map (\<lambda>(y, cl, var, var', v). (x_var var', v)) y_cl_var_var'_v_list) (x_var var'_k) = Some v_k")
  apply(clarsimp) apply(drule map_y) apply(simp) apply(drule_tac x = "(y_k, ty_k)" in bspec, assumption) apply(clarsimp)
  apply(erule sty_option.cases) apply(clarsimp) apply(rename_tac ty_y_k ty_k P) apply(drule_tac x = y_k in bspec, simp add: domI)
  apply(clarsimp) apply(case_tac v_k) apply(clarify, rule wf_nullI, simp) apply(clarsimp) apply(rename_tac oid_y_k)
  apply(erule_tac ?a4.0 = "Some ty_y_k" in wf_objectE) apply(simp) apply(erule sty_option.cases)
  apply(clarsimp split: option.splits) apply(rule wf_objectI) apply(clarsimp) apply(rule sty_optionI, simp+)
  apply(rule_tac ty' = ty' in sty_transitiveI, assumption+)
  apply(rule map_of_is_SomeI) apply(simp add: map_fst_var') apply(rule set_zip_var'_v, simp)
 apply(clarify) apply(rename_tac x_G ty_x_G) apply(frule_tac x = x_G in bspec, simp add: domI)
 apply(case_tac "map_of (map (\<lambda>((y, cl, var, var', v), y', y). (x_var var', y)) (zip y_cl_var_var'_v_list y_ty_list)) x_G")
  apply(frule map_of_map_zip_none, simp+) apply(simp add: map_add_def)
 apply(frule map_of_map_zip_some, simp+) apply(clarsimp)
 apply(drule map_of_is_SomeD) apply(drule map_of_is_SomeD) apply(clarsimp simp add: set_zip)
 apply(frule same_el, simp+) apply(drule_tac s = "(aa, ab, ac, ai, b)" in sym)
 apply(clarsimp) apply(rename_tac y_k cl_k var_k v_k y'_k ty_k var'_k i)
 apply(frule_tac y_k = y_k and cl_k = cl_k and var_k = var_k and var'_k = var'_k and v_k = v_k in same_y, simp+) apply(clarsimp)
 apply(drule_tac x = "(y_k, ty_k)" in bspec, simp) apply(clarsimp) apply(rename_tac y_k ty_k)
 apply(erule sty_option.cases) apply(clarsimp) apply(drule_tac x = y_k in bspec, simp add: domI) apply(clarsimp)
 apply(drule_tac x = "(y_k, cl_k, var_k, var'_k, v_k)" in bspec) apply(drule_tac t = "(y_k, cl_k, var_k, var'_k, v_k)" in sym) apply(simp)
 apply(clarsimp) apply(erule_tac ?a4.0 = "Some ty" in wf_objectE) apply(clarsimp) apply(rule wf_nullI, simp)
 apply(erule sty_option.cases) apply(clarsimp split: option.splits) apply(rule wf_objectI) apply(clarsimp)
 apply(rule sty_optionI, simp+) apply(rule_tac ty' = ty'a in sty_transitiveI, assumption+)

(* assignment *)
apply(clarsimp split del: split_if) apply(rule)
 apply(rule wf_var_assignI) apply(frule wf_method_from_find) apply(simp) apply(erule exE) apply(erule wf_methE)
 apply(case_tac "ya = x_this")
  apply(clarsimp split del: split_if)
  apply(rule_tac ty' = ty_var in sty_optionI) apply(simp) apply(simp)
  apply(frule_tac ty_r_d = ty in mty_preservation, assumption+) apply(clarify)
  apply(erule sty_option.cases) apply(clarsimp) apply(rule_tac ty' = ty' in sty_transitiveI, assumption+)
 (* y != this *)
 apply(erule sty_option.cases) apply(clarsimp split del: split_if)
 apply(frule_tac var_k = ya and ty_k = tya in exists_var') apply(drule map_of_vd) apply(assumption+) apply(erule exE) apply(clarsimp)
 apply(drule_tac y = "x_var var'_k" in map_of_is_SomeD) apply(clarsimp split del: split_if) apply(rename_tac y_k cl_k var_k var'_k v_k)
 apply(frule x'_not_in_list, assumption+) apply(clarsimp) apply(drule map_of_is_SomeD)
 apply(clarsimp split del: split_if) apply(rename_tac cl_k' var_k ty_k) apply(frule mty_preservation, assumption+)
 apply(clarsimp split del: split_if) apply(drule map_of_vd) apply(frule map_of_ty_k, assumption+)
 apply(rule_tac ty = ty_k and ty' = ty_var in sty_optionI) apply(simp add: map_add_def) apply(simp)
 apply(simp) apply(rule_tac ty' = ty_r in sty_transitiveI, assumption+)
(* wf of translated statements *)
apply(clarsimp) apply(erule disjE) apply(erule wf_methE) apply(clarsimp)
 apply(frule map_of_vd[rule_format]) (*apply(case_tac ctx, clarify)*) apply(frule mty_preservation, simp+) apply(clarsimp)
 apply(rename_tac P ctx dcl cl y meth s'' s')
 apply(drule_tac x = "(s'', s')" in bspec, simp)+ apply(clarsimp)
 apply(cut_tac cl_var_ty_list = cl_var_ty_list and y_cl_var_var'_v_list = y_cl_var_var'_v_list and y_ty_list = y_ty_list and
               P = P and ty_x_d = ty_x_d and ty_x_m = "ty_def ctx dcl" and x' = x' and s'' = s'' and G = \<Gamma> in wf_tr_stmt_in_G')
 apply(clarsimp)
(* wf of non-translated statements *)
apply(cut_tac L = L and x' = x' and y_cl_var_var'_v_list = y_cl_var_var'_v_list and G = \<Gamma> and P = P and H = H and
              s = s and y_ty_list = y_ty_list and ty = "ty_def ctx dcl" and ss = ss in wf_stmt_in_G')
apply(clarsimp)

apply(simp add: wf_action_preservation)

done

end