(*******************************************************************************
 * LJAM: Isabelle/HOL functional equivalents + some lemmas                     *
 * 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 ljam_eq imports ljam begin

(* BEGIN: HELPER FUNCTIONS *)

lemma map_id[simp]: "map id list = list" by (induct list, auto)

lemma id_map_two[simp]: "map (\<lambda>(x,y). (x,y)) list = list" by (induct list, auto)

lemma id_image_two[simp]: "(\<lambda>(x,y). (x,y)) ` set list = set list" by(induct list, auto)

lemma map_fst[simp]: "map (\<lambda>(x, y). x) list = map fst list" by (induct list, auto)

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

lemma zip_map_map_two [simp]: "zip (map fst list) (map snd list) = list"
by (induct list, auto)

lemma concat_map_singlton [simp]: "concat (map (\<lambda>e. [e]) list) = list"
by (induct_tac list, simp_all)

lemma list_all_map_P [simp]: "list_all (\<lambda>b. b) (map (\<lambda>x. P x) list) = (\<forall>x \<in> set list. P x)"
by (induct_tac list, simp_all)

lemma dom_single[simp]: "a \<in> dom (empty(k \<mapsto> v)) = (a = k)"
by (simp add: dom_def)

lemma predicted_lu[rule_format, simp]:
  "x \<in> set list \<longrightarrow> map_of (map (\<lambda>key. (key, value)) list) x = Some value"
by (induct list, auto)

lemma key_in_map1[simp]: "k \<notin> dom M' \<Longrightarrow> (M ++ M') k = M k"
by (subgoal_tac "M' k = None", simp add: map_add_def, force simp add: domI)

lemma forall_cons [rule_format]: "(\<forall>x \<in> set (s#S). P x) \<and> y \<in> set S \<longrightarrow> P y"
by (induct_tac S, simp_all)

lemma mem_cong[rule_format]:
  "x \<in> set list \<longrightarrow> (f x \<in> set (map f list))"
by (induct list, auto)

lemma forall_union: "\<lbrakk>\<forall>a \<in> dom A. P (A a); \<forall>b \<in> dom B. P (B b)\<rbrakk> \<Longrightarrow> \<forall>x \<in> dom A \<union> dom B. P ((B ++ A) x)"
apply(safe)
 apply(force)
apply(drule_tac x = x in bspec, simp add: domI)
apply(case_tac "A x = None")
 apply(force simp add: map_add_def)
by (force)

(* END: HELPER FUNCTIONS *)


constdefs
R_name_f :: "R \<Rightarrow> rn"
R_name_f_def: "R_name_f R \<equiv>
  (case R of r_bootstrap mds_c RMIS \<Rightarrow> rn_bootstrap
           | r_standard r rn mds_c RMIS \<Rightarrow> rn_standard r)"
lemma [simp]: "((R, rn) \<in> R_name) = (R_name_f R = rn)"
by (force simp add: R_name_f_def split: R.splits
          intro: R_name_bootstrapI R_name_standardI elim: R_name.cases)

constdefs
R_body_f :: "R \<Rightarrow> mds_c \<times> RMIS"
R_body_f_def: "R_body_f R \<equiv>
  (case R of r_bootstrap mds_c RMIS \<Rightarrow> (mds_c, RMIS)
           | r_standard r rn mds_c RMIS \<Rightarrow> (mds_c, RMIS))"
lemma [simp]: "((R, (mds_c, RMIS)) \<in> R_body) = (R_body_f R = (mds_c, RMIS))"
by (force simp add: R_body_f_def split: R.splits
          intro: R_body_bootstrapI R_body_standardI elim: R_body.cases)

constdefs
R_update_f :: "R \<Rightarrow> mds_c \<Rightarrow> RMIS \<Rightarrow> R"
R_update_f_def: "R_update_f R mds_c RMIS \<equiv>
  (case R of r_bootstrap mds_c' RMIS' \<Rightarrow> r_bootstrap mds_c RMIS
           | r_standard r rn mds_c' RMIS' \<Rightarrow> r_standard r rn mds_c RMIS)"
lemma [simp]: "((R, mds_c, RMIS, R') \<in> R_update) = (R_update_f R mds_c RMIS = R')"
by (force simp add: R_update_f_def split: R.splits
          intro: R_update_bootstrapI R_update_standardI elim: R_update.cases)

consts
mds_rm_f :: "mds_c \<Rightarrow> md_c \<Rightarrow> mds_c"
primrec
"mds_rm_f []            md_c = []"
"mds_rm_f (md_c'#mds_c) md_c = (if md_c'=md_c then [] else [md_c']) @ (mds_rm_f mds_c md_c)"
lemma mds_rm_f2r[rule_format]: "\<forall>md_c mds_c'. mds_rm_f mds_c md_c = mds_c' \<longrightarrow> (mds_c, md_c, mds_c') \<in> mds_rm"
by (induct mds_c rule: mds_rm_f.induct, auto split: split_if_asm intro: mds_rm.intros[simplified])
lemma [simp]: "((mds_c, md_c, mds_c') \<in> mds_rm) = (mds_rm_f mds_c md_c = mds_c')"
apply(rule)
 apply(induct mds_c md_c mds_c' rule: mds_rm.induct)
  apply(simp) apply(simp) apply(simp)
apply(auto simp add: mds_rm_f2r)
done

constdefs
md_name_f :: "md_c \<Rightarrow> mn"
md_name_f_def: "md_name_f md_c \<equiv>
  (case md_c of md_c_def mn clds_c ms fqns \<Rightarrow> mn)"
lemma [simp]: "((md_c, mn) \<in> md_name) = (md_name_f md_c = mn)"
by (force simp add: md_name_f_def split: md_c.splits
          intro: md_nameI elim: md_name.cases)

constdefs
full_name_f :: "cld \<Rightarrow> fqn"
full_name_f_def: "full_name_f cld \<equiv>
  (case cld of cld_def pn am dcl cl fds mds \<Rightarrow> fqn_def pn dcl)"
lemma [simp]: "((cld, fqn) \<in> full_name) = (full_name_f cld = fqn)"
by (force simp add: full_name_f_def split: cld.splits
          intro: full_nameI elim: full_name.cases)

constdefs
package_name_f :: "cld \<Rightarrow> pn"
package_name_f_def: "package_name_f cld \<equiv>
  (case cld of cld_def pn am dcl cl fds mds \<Rightarrow> pn)"
lemma [simp]: "((cld, pn) \<in> package_name) = (package_name_f cld = pn)"
by (force simp add: package_name_f_def split: cld.splits
          intro: package_nameI elim: package_name.cases)

constdefs
class_name_f :: "cld \<Rightarrow> dcl"
class_name_f_def: "class_name_f cld \<equiv>
  (case cld of cld_def pd am dcl cl fds mds \<Rightarrow> dcl)"
lemma [simp]: "((cld, dcl) \<in> class_name) = (class_name_f cld = dcl)"
by (force simp add: class_name_f_def split: cld.splits
          intro: class_nameI elim: class_name.cases)
 
constdefs
superclass_name_f :: "cld \<Rightarrow> cl"
superclass_name_f_def: "superclass_name_f cld \<equiv>
  (case cld of cld_def pd am dcl cl fds mds \<Rightarrow> cl)"
lemma [simp]: "((cld, cl) \<in> superclass_name) = (superclass_name_f cld = cl)"
by (force simp add: superclass_name_f_def split: cld.splits
          intro: superclass_nameI elim: superclass_name.cases)

constdefs
class_fields_f :: "cld \<Rightarrow> fds"
class_fields_f_def: "class_fields_f cld \<equiv>
  (case cld of cld_def pd am dcl cl fds mds \<Rightarrow> fds)"
lemma [simp]: "((cld, fds) \<in> class_fields) = (class_fields_f cld = fds)"
by (force simp add: class_fields_f_def split: cld.splits
          intro: class_fieldsI elim: class_fields.cases)

constdefs
class_methods_f :: "cld \<Rightarrow> meth_defs"
class_methods_f_def: "class_methods_f cld \<equiv>
  (case cld of cld_def pd am dcl cl fds mds \<Rightarrow> mds)"
lemma [simp]: "((cld, fds) \<in> class_methods) = (class_methods_f cld = fds)"
by (force simp add: class_methods_f_def split: cld.splits
          intro: class_methodsI elim: class_methods.cases)

constdefs
method_name_f :: "meth_def \<Rightarrow> meth"
method_name_f_def: "method_name_f md \<equiv>
  (case md of meth_def_def meth_sig meth_body \<Rightarrow>
  (case meth_sig of meth_sig_def cl meth vds \<Rightarrow> meth))"
lemma [simp]: "((md, m) \<in> method_name) = (method_name_f md = m)"
by (force simp add: method_name_f_def split: meth_def.splits meth_sig.splits
          intro: method_nameI elim: method_name.cases)

lemma cld_fqn_list[rule_format]:
  "(\<forall>x\<in>set cld_fqn_list. split (\<lambda>cld_XXX. op = (full_name_f cld_XXX)) x) \<and> distinct (map snd cld_fqn_list)
       \<longrightarrow> distinct (map full_name_f (map fst cld_fqn_list))"
apply(induct cld_fqn_list) apply(simp) apply(clarsimp)
apply(drule_tac x = "(aa, ba)" in bspec, simp) apply(force)
done

lemma fst_cld_fqn_list:
  "(map fst (map (\<lambda>cld. (cld, full_name_f cld)) clds)) = clds"
by (induct clds, auto)

constdefs
distinct_fqns_f :: "clds \<Rightarrow> bool"
distinct_fqns_f_def: "distinct_fqns_f clds \<equiv>
  (distinct (map full_name_f clds))"
lemma [simp]: "(clds \<in> distinct_fqns) = (distinct_fqns_f clds)"
apply(rule)
 apply(erule distinct_fqns.induct)
  apply(simp add: distinct_fqns_f_def)+
 apply(simp add: cld_fqn_list)
apply(cut_tac cld_fqn_list = "map (\<lambda>cld. (cld, full_name_f cld)) clds" in df_defI)
  apply(clarsimp)
 apply(clarsimp simp add: distinct_fqns_f_def)
 apply(simp only: atomize_imp) apply(induct clds) apply(simp) apply(clarsimp)
apply(simp add: fst_cld_fqn_list)
done

consts
find_md_in_mds_f :: "mds_c \<Rightarrow> mn \<Rightarrow> md_c_opt"
primrec
"find_md_in_mds_f []           mn = None"
"find_md_in_mds_f (md_c#mds_c) mn =
  (case md_c of md_c_def mn' clds_c ms fqns \<Rightarrow>
  (if mn = mn' then Some md_c else find_md_in_mds_f mds_c mn))"
lemma [simp]: "((mds_c, mn, md_c_opt) \<in> find_md_in_mds) = (find_md_in_mds_f mds_c mn = md_c_opt)"
apply(rule)
 apply(induct mds_c mn md_c_opt rule: find_md_in_mds.induct) apply(simp_all)
apply(induct mds_c rule: find_md_in_mds_f.induct) apply(simp) apply(rule fmim_emptyI)
apply(case_tac md_c) apply(rename_tac mn' clds_c ms fqns) apply(case_tac "mn = mn'")
 apply(clarsimp) apply(rule fmim_cons_trueI[simplified]) apply(force)
apply(clarsimp) apply(rule fmim_cons_falseI[simplified]) by(force)

consts
find_md_rec_f :: "(RC \<times> rn \<times> mn \<times> nat) \<Rightarrow> rnmd_c_opt"
recdef find_md_rec_f "measure (\<lambda>(RC, rn, mn, nn). card (dom RC) - nn)"
"find_md_rec_f (RC, rn, mn, nn) =
  (case RC rn of None \<Rightarrow> None | Some R \<Rightarrow>
  (case R of r_bootstrap mds_c RMIS \<Rightarrow>
     (case find_md_in_mds_f mds_c mn of None \<Rightarrow> None | Some md_c \<Rightarrow> Some (rn, md_c))
           | r_standard r rn' mds_c RMIS \<Rightarrow>
     (if card (dom RC) \<le> nn then None else
     (case find_md_rec_f (RC, rn', mn, Suc nn) of Some (rn'', md_c) \<Rightarrow> Some (rn'', md_c) | None \<Rightarrow>
     (case find_md_in_mds_f mds_c mn of None \<Rightarrow> None | Some md_c \<Rightarrow> Some (rn, md_c))))))"
lemma fmr_f2r[rule_format]: "\<forall>rnmd_c_opt. find_md_rec_f (RC, rn, mn, nn) = rnmd_c_opt \<longrightarrow> (RC, rn, mn, nn, rnmd_c_opt) \<in> find_md_rec"
apply(induct rule: find_md_rec_f.induct)
apply(case_tac "RC rn") apply(force intro: fmr_nullI)
apply(rename_tac R) apply(case_tac R)
 apply(rename_tac mds_c RMIS) apply(case_tac "find_md_in_mds_f mds_c mn = None")
  apply(simp, force intro: fmr_bootstrap_nullI)
 apply(simp, force intro: fmr_bootstrapI)
apply(rename_tac r rn' mds_c RMIS) apply(case_tac "card (dom RC) \<le> nn")
 apply(simp, force intro: fmr_standard_failI)
apply(case_tac "find_md_rec_f (RC, rn', mn, Suc nn)")
 apply(case_tac "find_md_in_mds_f mds_c mn")
  apply(simp, force intro: fmr_standard_nullI)
 apply(force intro: fmr_standard_selfI)
apply(simp, force intro: fmr_standard_recI)
done
lemma [simp]: "((RC, rn, mn, nn, rnmd_c_opt) \<in> find_md_rec) = (find_md_rec_f (RC, rn, mn, nn) = rnmd_c_opt)"
apply(rule) apply(induct rule: find_md_rec.induct) apply(simp add: fmr_f2r)+ done

constdefs
find_md_f :: "RC \<Rightarrow> rn \<Rightarrow> mn \<Rightarrow> rnmd_c_opt"
find_md_f_def: "find_md_f RC rn mn \<equiv> find_md_rec_f (RC, rn, mn, 0)"
lemma [simp]: "((RC, rn, mn, rnmd_c_opt) \<in> find_md) = (find_md_f RC rn mn = rnmd_c_opt)"
apply(rule)
 apply(induct rule: find_md.induct) apply(simp add: find_md_f_def)
apply(simp only: find_md_f_def) apply(force intro: fm_defI)
done

consts
find_cld_in_module_f :: "clds \<Rightarrow> fqn \<Rightarrow> cld_opt"
primrec
"find_cld_in_module_f []         fqn = None"
"find_cld_in_module_f (cld#clds) fqn =
  (if \<not> distinct_fqns_f (cld#clds) then None else
  (case fqn of fqn_def pn dcl \<Rightarrow>
  (case cld of cld_def pn' am dcl' cl fds mds \<Rightarrow>
  (if am = am_public \<and> pn = pn' \<and> dcl = dcl' then Some cld
   else find_cld_in_module_f clds fqn))))"
lemma [simp]: "((clds, fqn, cld_opt) \<in> find_cld_in_module) = (find_cld_in_module_f clds fqn = cld_opt)"
apply(rule)
 apply(induct rule: find_cld_in_module.induct) apply(simp) apply(simp) apply(simp) apply(clarsimp)
apply(simp only: atomize_imp) apply(induct_tac clds rule: find_cld_in_module_f.induct)
 apply(simp add: fcim_emptyI)
apply(clarsimp split: fqn.splits cld.splits) apply(rule)
 apply(clarsimp) apply(rule)
  apply(clarsimp) apply(rule fcim_nullI[simplified]) apply(force)
 apply(clarsimp) apply(rule fcim_cons_trueI[simplified]) apply(force) apply(force)
apply(clarsimp) apply(rule)
 apply(clarsimp) apply(rule fcim_nullI[simplified]) apply(force)
apply(clarsimp) apply(rule fcim_cons_falseI[simplified]) apply(force) apply(force) apply(simp) apply(simp)
done

constdefs
find_cld_in_core_f :: "P \<Rightarrow> fqn \<Rightarrow> ctxcld_opt"
find_cld_in_core_f_def: "find_cld_in_core_f P fqn \<equiv>
  (case P of p_def RC MH \<Rightarrow>
  (case RC rn_bootstrap of None \<Rightarrow> None | Some R \<Rightarrow>
  (case R of r_standard r rn mds RMIS \<Rightarrow> None | r_bootstrap mds RMIS \<Rightarrow>
  (case find_md_in_mds_f mds mn_core of None \<Rightarrow> None | Some md \<Rightarrow>
  (case RMIS md of None \<Rightarrow> None | Some mi \<Rightarrow>
  (case MH mi of None \<Rightarrow> None | Some (md, mis) \<Rightarrow>
  (case md of md_def mn clds ms fqns \<Rightarrow>
  (case find_cld_in_module_f clds fqn of None \<Rightarrow> None | Some cld \<Rightarrow>
     Some (ctx_def mi (package_name_f cld), cld)))))))))"
lemma [simp]: "((P, fqn, ctxcld_opt) \<in> find_cld_in_core) = (find_cld_in_core_f P fqn = ctxcld_opt)"
apply(rule)
 apply(induct rule: find_cld_in_core.induct) apply(simp add: find_cld_in_core_f_def)+
apply(case_tac P) apply(rename_tac RC MH)
apply(case_tac "RC rn_bootstrap") apply(simp add: fcic_no_rep_exI) apply(simp)
apply(rename_tac R) apply(case_tac R)
 apply(rename_tac mds RMIS) apply(simp) apply(case_tac "find_md_in_mds_f mds mn_core")
  apply(simp) apply(force intro: fcic_no_core_exI)
 apply(rename_tac md) apply(simp) apply(case_tac "RMIS md")
  apply(force intro: fcic_no_core_mi_exI)
 apply(rename_tac mi) apply(simp) apply(case_tac "MH mi")
  apply(force intro: fcic_no_mdmis_exI)
 apply(rename_tac mdmis) apply(case_tac mdmis) apply(rename_tac md mis) apply(simp)
 apply(case_tac md) apply(rename_tac mn clds ms fqns) apply(simp) apply(clarsimp split: option.splits)
  apply(force intro: fcic_falseI)
 apply(force intro: fcic_trueI)
apply(force intro: fcic_not_bootstrap_exI)
done

lemma reachable_eq[rule_format]:
  "(MH, mis, nn) \<in> reachable \<Longrightarrow> \<forall>nn'. (MH, mis, nn') \<in> reachable \<longrightarrow> nn = nn'"
apply(erule reachable.induct)
 apply(clarsimp) apply(erule reachable.cases) apply(simp) apply(simp)
apply(rule) apply(rename_tac nn'') apply(rule)
apply(erule_tac ?a3.0 = nn'' in reachable.cases) apply(clarify)
apply(clarsimp)
done

lemma reachable_bfs[iff]:
  "find_cld_in_module_f clds fqn = None \<and>
   find_cld_in_imports_f (MH, mis', fqn) = None \<and>
   fqn \<in> set fqns \<and> md = md_def mn clds ms fqns \<and> a = (md, mis') \<and> MH mi = Some a \<and> MH \<in> acyclic_mh \<and> set mis \<subseteq> dom MH \<longrightarrow>
      (THE nn. (MH, mis, nn) \<in> reachable) < (THE nn. (MH, mi # mis, nn) \<in> reachable)"
apply(clarsimp)
apply(erule acyclic_mh.cases) apply(clarsimp)
apply(drule_tac x = mi in bspec, simp add: domI) apply(clarsimp)
apply(frule_tac x = mis and R = "set mis \<subseteq> dom MH \<longrightarrow> (\<exists>nn. (MH, mis, nn) \<in> reachable)" in allE, simp)
apply(erule_tac x = mis' in allE, simp add: domI)
apply(clarsimp)
apply(frule reachable_consI) apply(simp) apply(simp)
apply(rule theI2) apply(simp) apply(simp add: reachable_eq)
apply(rule theI2) apply(simp) apply(simp add: reachable_eq)
apply(drule_tac mis = mis in reachable_eq, simp)
apply(drule_tac mis = "mi # mis" in reachable_eq, simp) apply(simp)
done

lemma reachable_bfs'[iff]:
  "\<forall>MH a b clds fqn fqns mi mis.
     fqn \<notin> set fqns \<and> (\<exists>mn ms. a = md_def mn clds ms fqns) \<and> MH mi = Some (a, b) \<and> MH \<in> acyclic_mh \<and> set mis \<subseteq> dom MH \<longrightarrow>
      (THE nn. (MH, mis, nn) \<in> reachable) < (THE nn. (MH, mi # mis, nn) \<in> reachable)"
apply(clarsimp)
apply(erule acyclic_mh.cases) apply(clarsimp)
apply(drule_tac x = mi in bspec, simp add: domI) apply(clarsimp)
apply(frule_tac x = mis and R = "set mis \<subseteq> dom MHa \<longrightarrow> (\<exists>nn. (MHa, mis, nn) \<in> reachable)" in allE, simp)
apply(erule_tac x = b in allE, simp add: domI)
apply(clarsimp)
apply(frule reachable_consI) apply(simp) apply(simp)
apply(rule theI2) apply(simp) apply(simp add: reachable_eq)
apply(rule theI2) apply(simp) apply(simp add: reachable_eq)
apply(drule_tac mis = mis in reachable_eq, simp)
apply(drule_tac mis = "mi # mis" in reachable_eq, simp) apply(simp)
done

lemma reachable_dfs[iff]:
  "\<forall>MH a b clds fqn fqns mi mis.
     fqn \<in> set fqns \<and> (\<exists>mn ms. a = md_def mn clds ms fqns) \<and> MH mi = Some (a, b) \<and> MH \<in> acyclic_mh \<and> set mis \<subseteq> dom MH \<longrightarrow>
        (THE nn. (MH, b, nn) \<in> reachable) < (THE nn. (MH, mi # mis, nn) \<in> reachable)"
apply(clarsimp) apply(erule acyclic_mh.cases) apply(clarsimp)
apply(drule_tac x = mi in bspec, simp add: domI) apply(clarsimp) apply(rename_tac MH)
apply(frule_tac x = mis and R = "set mis \<subseteq> dom MH \<longrightarrow> (\<exists>nn. (MH, mis, nn) \<in> reachable)" in allE, simp)
apply(erule_tac x = b in allE, simp add: domI)
apply(clarsimp)
apply(frule reachable_consI) apply(simp) apply(simp)
apply(rule theI2) apply(simp) apply(simp add: reachable_eq)
apply(rule theI2) apply(simp) apply(simp add: reachable_eq)
apply(drule_tac mis = b in reachable_eq) apply(simp)
apply(drule_tac mis = "mi # mis" in reachable_eq) apply(simp) apply(simp)
done

consts
find_cld_in_imports_f :: "MH \<times> mis \<times> fqn \<Rightarrow> ctxcld_opt"
recdef find_cld_in_imports_f "measure (\<lambda>(MH, mis, fqn). (THE nn. (MH, mis, nn) \<in> reachable))"
"find_cld_in_imports_f (MH, [],     fqn) = None"
fcii_rec:
"find_cld_in_imports_f (MH, mi#mis, fqn) =
  (if \<not>(MH \<in> acyclic_mh \<and> set mis \<subseteq> dom MH) then None else
  (case MH mi of None \<Rightarrow> None | Some (md, mis') \<Rightarrow>
  (case md of md_def mn clds ms fqns \<Rightarrow>
  (if fqn \<notin> set fqns then find_cld_in_imports_f (MH, mis, fqn) else
  (case find_cld_in_imports_f (MH, mis', fqn) of Some ctxcld \<Rightarrow> Some ctxcld | None \<Rightarrow>
  (case find_cld_in_module_f clds fqn of Some cld \<Rightarrow> Some (ctx_def mi (package_name_f cld), cld) | None \<Rightarrow>
     find_cld_in_imports_f (MH, mis, fqn)  ))))))"
declare fcii_rec[simp del]

lemma fcii_rec_call_valid[simp]:
  "find_cld_in_imports_f (MH, mi # mis, fqn) =
     (if \<not>(MH \<in> acyclic_mh \<and> set mis \<subseteq> dom MH) then None else
     (case MH mi of None \<Rightarrow> None | Some (md, mis') \<Rightarrow>
     (case md of md_def mn clds ms fqns \<Rightarrow>
     (if fqn \<notin> set fqns then find_cld_in_imports_f (MH, mis, fqn) else
     (case find_cld_in_imports_f (MH, mis', fqn) of Some ctxcld \<Rightarrow> Some ctxcld | None \<Rightarrow>
     (case find_cld_in_module_f clds fqn of Some cld \<Rightarrow> Some (ctx_def mi (package_name_f cld), cld) | None \<Rightarrow>
         find_cld_in_imports_f (MH, mis, fqn)))))))"
apply(clarsimp simp add: find_cld_in_imports_f.simps(2) measure_def inv_image_def split: option.splits md.splits)
apply(force intro: reachable_bfs[rule_format])
done

lemma fcii_induct:
  "\<lbrakk>\<And>MH fqn_set fqn. P MH [] fqn;
    \<And>MH mi mis fqn.
       \<lbrakk>(\<exists>clds. find_cld_in_module_f clds fqn = None \<and>
        (\<exists>mis'. find_cld_in_imports_f (MH, mis', fqn) = None \<and>
        (\<exists>fqns. fqn \<in> set fqns \<and>
        (\<exists>md. (\<exists>mn ms. md = md_def mn clds ms fqns) \<and> MH mi = Some (md, mis') \<and> MH \<in> acyclic_mh \<and> set mis \<subseteq> dom MH)))) \<longrightarrow> P MH mis fqn;
        \<forall>fqns mn clds ms mis'. fqn \<in> set fqns \<and> MH mi = Some (md_def mn clds ms fqns, mis') \<and> MH \<in> acyclic_mh \<and> set mis \<subseteq> dom MH \<longrightarrow> P MH mis' fqn;
        (\<exists>fqns. fqn \<notin> set fqns \<and> (\<exists>md. (\<exists>mn clds ms. md = md_def mn clds ms fqns) \<and>
                (\<exists>mis'. MH mi = Some (md, mis')) \<and> MH \<in> acyclic_mh \<and> set mis \<subseteq> dom MH)) \<longrightarrow> P MH mis fqn\<rbrakk>
            \<Longrightarrow> P MH (mi # mis) fqn\<rbrakk>
       \<Longrightarrow> P MH mis fqn"
apply(rule find_cld_in_imports_f.induct) apply(simp)
apply(subgoal_tac
  "((\<exists>clds. find_cld_in_module_f clds fqn = None \<and>
   (\<exists>mis'. find_cld_in_imports_f (MH, mis', fqn) = None \<and>
   (\<exists>fqns. fqn \<in> set fqns \<and>
   (\<exists>md. (\<exists>mn ms. md = md_def mn clds ms fqns) \<and> MH mi = Some (md, mis') \<and> MH \<in> acyclic_mh \<and> set mis \<subseteq> dom MH)))) \<longrightarrow> P MH mis fqn) \<and>
   (\<forall>fqns mn clds ms mis'. fqn \<in> set fqns \<and> MH mi = Some (md_def mn clds ms fqns, mis') \<and> MH \<in> acyclic_mh \<and> set mis \<subseteq> dom MH \<longrightarrow> P MH mis' fqn) \<and>
   ((\<exists>fqns. fqn \<notin> set fqns \<and> (\<exists>md. (\<exists>mn clds ms. md = md_def mn clds ms fqns) \<and>
    (\<exists>mis'. MH mi = Some (md, mis')) \<and> MH \<in> acyclic_mh \<and> set mis \<subseteq> dom MH)) \<longrightarrow> P MH mis fqn)")
 apply(simp)
apply(auto) apply(erule contrapos_np) apply(rule reachable_bfs[rule_format]) apply(force)
done

lemma fcii_f2r[rule_format]:
  "\<forall>ctxcld_opt. find_cld_in_imports_f (MH, mis, fqn) = ctxcld_opt
          \<longrightarrow> (MH, mis, fqn, ctxcld_opt) \<in> find_cld_in_imports"
apply(induct rule: fcii_induct)
 apply(force intro: fcii_emptyI[simplified])
apply(case_tac "MH \<in> acyclic_mh")
 apply(case_tac "set mis \<subseteq> dom MH")
  apply(case_tac "MH mi")
   apply(clarsimp) apply(force intro: fcii_nullI[simplified])
  apply(clarsimp) apply(rename_tac md mis') apply(case_tac md, rename_tac mn clds ms fqns, clarsimp) apply(rule)
   apply(clarsimp) apply(force intro: fcii_skipI[simplified])
  apply(case_tac "find_cld_in_imports_f (MH, mis', fqn)")
   apply(clarsimp) apply(case_tac "find_cld_in_module_f clds fqn")
    apply(clarsimp) apply(force intro: fcii_nextI[simplified])
   apply(clarsimp) apply(force intro: fcii_selfI[simplified])
  apply(clarsimp) apply(force intro: fcii_recI[simplified])
 apply(clarsimp) apply(force intro: fcii_nullI[simplified])
apply(clarsimp) apply(force intro: fcii_nullI[simplified])
done

lemma [simp]: "((MH, mis, fqn, ctxcld_opt) \<in> find_cld_in_imports) = (find_cld_in_imports_f (MH, mis, fqn) = ctxcld_opt)"
apply(rule)
 apply(induct rule: find_cld_in_imports.induct)
 apply(force split: option.splits)+
apply(simp only: atomize_imp) apply(induct rule: fcii_induct)
 apply(force intro: fcii_emptyI[simplified])
apply(simp add: fcii_f2r)
done

consts
find_cld_in_self_f :: "clds \<Rightarrow> pn \<Rightarrow> fqn \<Rightarrow> cld_opt"
primrec
"find_cld_in_self_f []         pn fqn = None"
"find_cld_in_self_f (cld#clds) pn fqn =
  (if \<not> distinct_fqns_f (cld#clds) then None else
  (case fqn of fqn_def pn' dcl \<Rightarrow>
  (case cld of cld_def pn'' am dcl' cl fds mds \<Rightarrow>
  (if pn' = pn'' \<and> dcl = dcl' \<and> (pn = pn' \<or> am = am_public) then Some cld
   else find_cld_in_self_f clds pn fqn))))"
lemma [simp]: "((clds, pn, fqn, cld_opt) \<in> find_cld_in_self) = (find_cld_in_self_f clds pn fqn = cld_opt)"
apply(rule)
 apply(induct rule: find_cld_in_self.induct) apply(simp) apply(simp) apply(simp) apply(clarsimp)
apply(simp only: atomize_imp) apply(induct_tac clds rule: find_cld_in_self_f.induct)
 apply(simp add: fcis_emptyI)
apply(clarsimp) apply(case_tac "distinct_fqns_f (cld # clds)")
 apply(clarsimp) apply(case_tac fqn, rename_tac pn' dcl, clarsimp)
 apply(case_tac cld, rename_tac pn'' am dcl' cl fds mds, clarsimp) apply(rule)
  apply(clarsimp) apply(rule fcis_cons_trueI[simplified]) apply(force) apply(force) apply(force)
 apply(clarsimp) apply(rule fcis_cons_falseI[simplified]) apply(assumption) apply(force) apply(force)
 apply(simp split: split_if_asm)
apply(case_tac fqn) apply(clarsimp) apply(force intro: fcis_nullI[simplified])
done

constdefs
find_cld_f :: "P \<Rightarrow> ctx \<Rightarrow> fqn \<Rightarrow> ctxcld_opt"
find_cld_f_def: "find_cld_f P ctx fqn \<equiv>
  (case find_cld_in_core_f P fqn of Some ctxcld \<Rightarrow> Some ctxcld | None \<Rightarrow>
  (case P of p_def RC MH \<Rightarrow> case ctx of ctx_def mi pn \<Rightarrow>
  (case MH mi of None \<Rightarrow> None | Some (md, mis) \<Rightarrow>
  (case md of md_def mn clds ms fqns \<Rightarrow>
  (case find_cld_in_imports_f (MH, mis, fqn) of Some ctxcld \<Rightarrow> Some ctxcld | None \<Rightarrow>
  (case find_cld_in_self_f clds pn fqn of None \<Rightarrow> None | Some cld \<Rightarrow>
     Some (ctx_def mi (package_name_f cld), cld)))))))"
lemma [simp]: "((P, ctx, fqn, ctxcld_opt) \<in> find_cld) = (find_cld_f P ctx fqn = ctxcld_opt)"
apply(rule)
 apply(induct rule: find_cld.induct) apply(force simp add: find_cld_f_def)+
apply(simp add: find_cld_f_def split: option.splits)
 apply(case_tac P) apply(rename_tac RC MH) apply(simp)
 apply(case_tac ctx) apply(rename_tac mi pn) apply(simp split: option.splits)
  apply(force intro: fc_nullI)
 apply(rename_tac mdmis) apply(case_tac mdmis) apply(rename_tac md mis) apply(simp)
 apply(case_tac md) apply(rename_tac mn clds ms fqns) apply(simp split: option.splits)
   apply(force intro: fc_failI)
  apply(rename_tac cld) apply(force intro: fc_selfI)
 apply(rename_tac ctxcld) apply(drule_tac s = "Some ctxcld" in sym) apply(simp) apply(force intro: fc_importsI)
apply(rename_tac ctxcld) apply(drule_tac s = "Some ctxcld" in sym) apply(force intro: fc_coreI)
done

lemma find_cld_in_self_name_eq[rule_format]:
  "\<forall>cld. find_cld_in_self_f clds pn' (fqn_def pn dcl) = Some cld \<longrightarrow> (\<exists>am cl fds mds. cld_def pn am dcl cl fds mds = cld)"
apply(induct clds rule: find_cld_in_self_f.induct) apply(simp)
apply(clarsimp split: cld.splits)
done

lemma find_cld_in_module_name_eq[rule_format]:
  "\<forall>cld. find_cld_in_module_f clds (fqn_def pn dcl) = Some cld \<longrightarrow> (\<exists>am cl fds mds. cld_def pn am dcl cl fds mds = cld)"
apply(induct clds rule: find_cld_in_module_f.induct) apply(simp)
apply(clarsimp split: cld.splits)
done

lemma find_cld_in_imports_name_eq[rule_format]:
  "\<forall>ctxcld. find_cld_in_imports_f (MH, mis, fqn) = Some ctxcld
               \<longrightarrow> (\<forall>pn dcl. fqn = fqn_def pn dcl \<longrightarrow> (\<exists>mi am cl fds mds. (ctx_def mi pn, cld_def pn am dcl cl fds mds) = ctxcld))"
apply(induct MH mis fqn rule: fcii_induct)
 apply(simp)
apply(clarsimp) apply(rename_tac ctx cld pn dcl) apply(case_tac "MH mi", simp, clarsimp)
apply(rename_tac md mis', case_tac md, rename_tac mn clds ms fqns, clarsimp)
apply(case_tac "fqn_def pn dcl \<in> set fqns")
 apply(case_tac "find_cld_in_imports_f (MH, mis', fqn_def pn dcl)")
  apply(clarsimp) apply(case_tac "find_cld_in_module_f clds (fqn_def pn dcl)") apply(simp)
  apply(rename_tac cld) apply(case_tac cld) apply(clarsimp simp add: package_name_f_def)
  apply(frule find_cld_in_module_name_eq) apply(simp)
 apply(simp)
apply(simp)
done

lemma find_cld_in_core_name_eq[rule_format]:
  "\<forall>ctxcld. find_cld_in_core_f P (fqn_def pn dcl) = Some ctxcld
               \<longrightarrow> (\<exists>mi am cl fds mds. (ctx_def mi pn, cld_def pn am dcl cl fds mds) = ctxcld)"
apply(clarsimp simp add: find_cld_in_core_f_def) apply(rename_tac ctx cld) apply(case_tac P, rename_tac RC MH, simp)
apply(clarsimp split: option.splits R.splits md.splits) apply(rename_tac mds RMIS md mi mis' mn clds mis fqns)
apply(case_tac cld) apply(rename_tac pn' am dcl' cl fds mds') apply(clarsimp) apply(drule find_cld_in_module_name_eq)
apply(clarsimp simp add: package_name_f_def)
done

lemma find_cld_name_eq[rule_format]:
  "\<forall>ctxcld. find_cld_f P ctx (fqn_def pn dcl) = Some ctxcld \<longrightarrow> (\<exists>mi am cl fds mds. (ctx_def mi pn, cld_def pn am dcl cl fds mds) = ctxcld)"
apply(rule) apply(simp add: find_cld_f_def) apply(case_tac "find_cld_in_core_f P (fqn_def pn dcl)")
 apply(simp) apply(case_tac P, rename_tac RC MH, simp) apply(case_tac ctx, rename_tac mi pn', simp) apply(case_tac "MH mi")
  apply(simp)
 apply(rename_tac mdmis, case_tac mdmis, rename_tac md mis, simp) apply(case_tac md, rename_tac mn clds ms fqns, simp)
 apply(case_tac "find_cld_in_imports_f (MH, mis, fqn_def pn dcl)")
  apply(simp) apply(case_tac "find_cld_in_self_f clds pn' (fqn_def pn dcl)")
   apply(simp)
  apply(rename_tac cld) apply(case_tac cld) apply(rename_tac pn'' am dcl' cl fds mds) apply(clarsimp simp add: package_name_f_def)
  apply(drule find_cld_in_self_name_eq) apply(simp)
 apply(clarsimp) apply(frule find_cld_in_imports_name_eq) apply(force) apply(simp)
apply(clarsimp) apply(rename_tac ctx cld) apply(drule find_cld_in_core_name_eq) apply(force)
done

consts
find_type_f :: "P \<Rightarrow> ctx \<Rightarrow> cl \<Rightarrow> ty_opt"
primrec
"find_type_f P ctx cl_object = Some ty_top"
"find_type_f P ctx (cl_fqn fqn) =
  (case fqn of fqn_def pn dcl \<Rightarrow>
  (case find_cld_f P ctx fqn of None \<Rightarrow> None
                              | Some (ctx', cld) \<Rightarrow> Some (ty_def ctx' dcl)))"
lemma [simp]: "((P, ctx, cl, ty_opt) \<in> find_type) = (find_type_f P ctx cl = ty_opt)"
apply(rule)
 apply(force elim: find_type.cases split: fqn.splits)
apply(case_tac cl) apply(force intro: ft_objI)
apply(case_tac fqn) apply(clarsimp)
apply(split option.splits) apply(rule)
 apply(force intro: ft_nullI)
by (force intro: ft_dclI)

lemma path_length_eq[rule_format]:
  "(P, ctx, cl, nn) \<in> path_length \<Longrightarrow> \<forall>nn'. (P, ctx, cl, nn') \<in> path_length \<longrightarrow> nn = nn'"
apply(erule path_length.induct)
 apply(clarsimp) apply(erule path_length.cases) apply(simp) apply(simp)
apply(rule) apply(rule)
apply(erule_tac ?a4.0 = nn' in path_length.cases) apply(clarify)
apply(clarsimp)
done

lemma [iff]:
  "\<forall>P cld ctx ctx' fqn. find_cld_f P ctx fqn = Some (ctx', cld) \<and> P \<in> acyclic_clds
       \<longrightarrow> (THE nn. (P, ctx', superclass_name_f cld, nn) \<in> path_length) < (THE nn. (P, ctx, cl_fqn fqn, nn) \<in> path_length)"
apply(clarsimp)
apply(erule acyclic_clds.cases) apply(clarsimp) apply(rename_tac P)
apply(case_tac ctx, rename_tac mi pn, clarsimp)
apply(erule_tac x = mi in allE) apply(erule acyclic_clds_mi.cases) apply(clarsimp)
apply(erule_tac x = pn in allE)
apply(erule_tac x = fqn in allE)
apply(clarsimp)
apply(rule theI2) apply(simp) apply(simp add: path_length_eq)
apply(erule path_length.cases) apply(simp) apply(clarsimp)
apply(rule theI2) apply(simp) apply(simp add: path_length_eq)
apply(drule_tac path_length_eq, simp)
apply(erule path_length.cases) apply(simp) apply(clarsimp)
apply(drule_tac path_length_eq, simp) apply(simp)
done

consts
find_path_rec_f :: "(P * ctx * cl * ctxclds) \<Rightarrow> ctxclds_opt"
recdef find_path_rec_f "measure (\<lambda>(P, ctx, cl, path). (THE nn. (P, ctx, cl, nn) \<in> path_length))"
"find_path_rec_f (P, ctx,  cl_object,   path) = Some path"
"find_path_rec_f (P, ctx, (cl_fqn fqn), path) =
  (if P \<notin> acyclic_clds then None else
  (case find_cld_f P ctx fqn of None \<Rightarrow> None | Some (ctx', cld) \<Rightarrow>
    find_path_rec_f (P, ctx', superclass_name_f cld, path @ [(ctx',cld)])))"
lemma [simp]: "((P, ctx, cl, path, path_opt) \<in> find_path_rec) = (find_path_rec_f (P, ctx, cl, path) = path_opt)"
apply(rule)
 apply(rule find_path_rec.induct) apply(simp)+
apply(induct rule: find_path_rec_f.induct)
 apply(clarsimp simp add: fpr_objI)
apply(clarsimp) apply(rule)
 apply(simp add: fpr_nullI)
apply(clarsimp split: option.splits) apply(rule)
 apply(simp add: fpr_nullI)
apply(clarsimp) apply(rule fpr_fqnI) apply(force)+
done

constdefs
find_path_f :: "P \<Rightarrow> ctx \<Rightarrow> cl \<Rightarrow> ctxclds_opt"
find_path_f_def: "find_path_f P ctx cl == find_path_rec_f (P, ctx, cl, [])"
lemma [simp]: "((P, ctx, cl, path_opt) \<in> find_path) = (find_path_f P ctx cl = path_opt)"
apply(rule)
 apply(erule find_path.cases) apply(unfold find_path_f_def) apply(simp)
apply(simp add: fp_defI)
done

consts
find_path_ty_f :: "P \<Rightarrow> ty \<Rightarrow> ctxclds_opt"
primrec
"find_path_ty_f P  ty_top          = Some []"
"find_path_ty_f P (ty_def ctx dcl) =
  (case ctx of ctx_def mi pn \<Rightarrow> find_path_f P ctx (cl_fqn (fqn_def pn dcl)))"
lemma [simp]: "((P, ty, ctxclds_opt) \<in> find_path_ty) = (find_path_ty_f P ty = ctxclds_opt)"
apply(rule)
 apply(force elim: find_path_ty.cases)
apply(case_tac ty)
 apply(clarsimp simp add: fpty_objI)
apply(rename_tac dcl) apply(simp)
apply(case_tac ctx) apply(rename_tac mi pn) apply(simp) apply(rule fpty_dclI)
apply(simp)
done

consts
fields_in_path_f :: "ctxclds \<Rightarrow> fs"
primrec
"fields_in_path_f []               = []"
"fields_in_path_f (ctxcld#ctxclds) = (map (\<lambda>fd. case fd of fd_def cl f \<Rightarrow> f) (class_fields_f (snd ctxcld))) @ fields_in_path_f ctxclds"
lemma cl_f_list_map: "map (fd_case (\<lambda>cl f. f)) (map (\<lambda>(x, y). fd_def x y) cl_f_list) = map (\<lambda>(cl_XXX, f_XXX). f_XXX) cl_f_list"
by (induct cl_f_list, auto)

lemma fip_ind_to_f: "\<forall>fs. (clds, fs) \<in> fields_in_path \<longrightarrow> fields_in_path_f clds = fs"
apply(induct clds)
 apply(clarsimp, erule fields_in_path.cases) apply(simp) apply(clarsimp)
apply(clarsimp)
apply(erule fields_in_path.cases) apply(simp) by(clarsimp simp add: cl_f_list_map)

lemma fd_map_split: "map (fd_case (\<lambda>cl f. f)) (map (\<lambda>(x, y). fd_def x y) list) = map (\<lambda>(cl, f). f) list"
apply(induct list) apply(simp) apply(clarsimp) done

lemma fd_map_split': "map (\<lambda>(x, y). fd_def x y) (map (fd_case Pair) list) = list"
apply(induct list) apply(simp split: fd.splits)+ done

lemma fd_map_split'': "map (fd_case (\<lambda>cl f. f)) list = map (\<lambda>(cl, f). f) (map (fd_case Pair) list)"
apply(induct list) apply(simp split: fd.splits)+ done

lemma [simp]: "\<forall>fs. ((ctxclds, fs) \<in> fields_in_path) = (fields_in_path_f ctxclds = fs)"
apply(induct ctxclds)
 apply(rule) apply(rule)
  apply(force elim: fields_in_path.cases)
 apply(simp add: fip_emptyI)
apply(clarsimp)
apply(rule)
 apply(erule fields_in_path.cases)
  apply(simp)
 apply(simp add: fip_ind_to_f fd_map_split)
apply(rule_tac cld = b and ctxcld_list = ctxclds
           and cl_f_list = "map (\<lambda>fd. case fd of fd_def cl f \<Rightarrow> (cl, f)) (class_fields_f b)" in fip_consI[simplified])
apply(clarsimp simp add: class_fields_f_def split: cld.splits)
apply(simp add: fd_map_split') apply(clarsimp) apply(simp)
apply(clarsimp) apply(simp add: fd_map_split'')
done

constdefs
fields_f :: "P \<Rightarrow> ty \<Rightarrow> fs option"
fields_f_def: "fields_f P ty ==
  (case find_path_ty_f P ty of None \<Rightarrow> None | Some ctxclds \<Rightarrow>
    Some (fields_in_path_f ctxclds))"
lemma [simp]: "\<forall>fs_opt. ((P, ty, fs_opt) \<in> fields) = (fields_f P ty = fs_opt)"
apply(rule) apply(rule)
 apply(case_tac fs_opt)
  apply(clarsimp) apply(erule fields.cases)
   apply(clarsimp) apply(simp add: fields_f_def)
  apply(clarsimp)
 apply(erule fields.cases)
  apply(simp)
 apply(clarsimp) apply(simp add: fields_f_def)
 apply(simp add: fields_f_def) apply(case_tac "find_path_ty_f P ty") apply(simp) apply(simp add: fields_noneI[simplified])
apply(clarsimp) apply(case_tac "find_path_ty_f P ty") apply(simp) apply(simp) apply(clarsimp)
apply(rule fields_someI) apply(simp) apply(simp)
done

consts
methods_in_path_f :: "clds \<Rightarrow> meths"
primrec
"methods_in_path_f []         = []"
"methods_in_path_f (cld#clds) =
  map (\<lambda>md. case md of meth_def_def meth_sig meth_body \<Rightarrow> case meth_sig of meth_sig_def cl meth vds \<Rightarrow> meth) (class_methods_f cld) @ methods_in_path_f clds"

lemma meth_def_map[rule_format]:
  "(\<forall>x \<in> set list. (\<lambda>(md, cl, m, vds, mb). md = meth_def_def (meth_sig_def cl m vds) mb) x)
     \<longrightarrow> map (meth_def_case (\<lambda>ms mb. case ms of meth_sig_def cl m vds \<Rightarrow> m)) (map (\<lambda>(md, cl, m, vds, mb). md) list) = map (\<lambda>(md, cl, m, vds, mb). m) list"
by (induct list, auto)

lemma meth_def_map':
  "list = map (\<lambda>(md, cl, m, vds, mb). md) (map (\<lambda>md. case md of meth_def_def ms mb \<Rightarrow>
                 case ms of meth_sig_def cl m vds \<Rightarrow> (md, cl, m, vds, mb)) list)"
apply(induct list) by (auto split: meth_def.splits meth_sig.splits)

lemma meth_def_map'':
  "map (meth_def_case (\<lambda>ms mb. case ms of meth_sig_def cl m vds \<Rightarrow> m)) list =
   map (\<lambda>(md, cl, m, vds, mb). m) (map (\<lambda>md. case md of meth_def_def ms mb \<Rightarrow> case ms of meth_sig_def cl m vds \<Rightarrow> (md, cl, m, vds, mb)) list)"
apply(induct list) by (auto split: meth_def.splits meth_sig.splits)

lemma [simp]: "\<forall>meths. ((clds, meths) \<in> methods_in_path) = (methods_in_path_f clds = meths)"
apply(induct clds)
 apply(clarsimp) apply(rule)
  apply(erule methods_in_path.cases) apply(simp) apply(clarsimp)
 apply(clarsimp) apply(rule mip_emptyI)
apply(clarsimp) apply(rule)
 apply(erule methods_in_path.cases) apply(simp) apply(clarsimp)
 apply(rule meth_def_map) apply(simp)
apply(rule_tac
  meth_def_cl_meth_vds_meth_body_list =
   "(case a of cld_def pn am dcl cl fds mds \<Rightarrow>
    (map (\<lambda>md. (case md of meth_def_def ms mb \<Rightarrow>
               (case ms of meth_sig_def cl m vds \<Rightarrow> (md, cl, m, vds, mb)))) mds))" in
  mip_consI[simplified])
   apply(clarsimp) apply(case_tac a) apply(simp add: class_methods_f_def meth_def_map')
  apply(clarsimp) apply(case_tac a) apply(clarsimp split: meth_def.splits meth_sig.splits)
 apply(simp)
apply(clarsimp) apply(case_tac a) apply(clarsimp simp add: class_methods_f_def) apply(rule meth_def_map'')
done

constdefs
methods_f :: "P \<Rightarrow> ty \<Rightarrow> meths option"
methods_f_def: "methods_f P ty ==
  (case find_path_ty_f P ty of None \<Rightarrow> None | Some ctxclds \<Rightarrow>
    Some (methods_in_path_f (map (\<lambda>(ctx, cld). cld) ctxclds)))"
lemma [simp]: "((P, ty, meths) \<in> methods) = (methods_f P ty = Some meths)"
apply(rule)
 apply(erule methods.cases) apply(clarsimp simp add: methods_f_def)
apply(simp add: methods_f_def) apply(split option.splits) apply(simp)
apply(clarsimp) apply(rule methods_methodsI) apply(simp) apply(clarsimp)
done

consts
ftype_in_fds_f :: "P \<Rightarrow> ctx \<Rightarrow> fds \<Rightarrow> f \<Rightarrow> ty_opt_bot"
primrec
"ftype_in_fds_f P ctx []       f = ty_opt_bot_opt None"
"ftype_in_fds_f P ctx (fd#fds) f =
  (case fd of fd_def cl f' \<Rightarrow>
  (if f = f' then
  (case find_type_f P ctx cl of None \<Rightarrow> ty_opt_bot_bot | Some ty \<Rightarrow> ty_opt_bot_opt (Some ty)) else
     ftype_in_fds_f P ctx fds f))"
lemma [simp]: "((P, ctx, fds, f, ty_opt) \<in> ftype_in_fds) = (ftype_in_fds_f P ctx fds f = ty_opt)"
apply(rule)
 apply(induct fds) apply(erule ftype_in_fds.cases) apply(simp) apply(simp) apply(simp) apply(simp)
 apply(erule ftype_in_fds.cases) apply(simp) apply(simp) apply(simp) apply(clarsimp)
apply(induct fds)
 apply(clarsimp) apply(rule ftif_emptyI)
apply(rename_tac fd fds) apply(case_tac fd, rename_tac cl f', clarsimp) apply(rule)
 apply(clarsimp) apply(case_tac "find_type_f P ctx cl")
  apply(simp add: ftif_cons_botI[simplified])
 apply(simp add: ftif_cons_trueI[simplified])
apply(force intro: ftif_cons_falseI[simplified])
done

consts
ftype_in_path_f :: "P \<Rightarrow> ctxclds \<Rightarrow> f \<Rightarrow> ty_opt"
primrec
"ftype_in_path_f P []               f = None"
"ftype_in_path_f P (ctxcld#ctxclds) f =
  (case ctxcld of (ctx, cld) \<Rightarrow>
  (case ftype_in_fds_f P ctx (class_fields_f cld) f of ty_opt_bot_bot \<Rightarrow> None | ty_opt_bot_opt ty_opt \<Rightarrow>
  (case ty_opt of Some ty \<Rightarrow> Some ty | None \<Rightarrow> ftype_in_path_f P ctxclds f)))"
lemma [simp]: "((P, ctxclds, f, ty_opt) \<in> ftype_in_path) = (ftype_in_path_f P ctxclds f = ty_opt)"
apply(rule)
 apply(induct rule: ftype_in_path.induct) apply(simp+)
apply(induct ctxclds) apply(simp) apply(rule ftip_emptyI)
apply(clarsimp) apply(case_tac "ftype_in_fds_f P a (class_fields_f b) f")
 apply(rename_tac ty_opt) apply(case_tac ty_opt)
  apply(simp add: ftip_cons_falseI[simplified])
 apply(simp add: ftip_cons_trueI[simplified])
apply(simp add: ftip_cons_botI[simplified])
done

constdefs
ftype_f :: "P \<Rightarrow> ty \<Rightarrow> f \<Rightarrow> ty_opt"
ftype_f_def: "ftype_f P ty f ==
  (case find_path_ty_f P ty of None \<Rightarrow> None | Some ctxclds \<Rightarrow> ftype_in_path_f P ctxclds f)"
lemma [simp]: "((P, ty, f, ty') \<in> ftype) = (ftype_f P ty f = Some ty')"
apply(rule)
 apply(induct rule: ftype.induct) apply(clarsimp simp add: ftype_f_def)
apply(clarsimp simp add: ftype_f_def split: option.splits) apply(rule ftypeI) apply(simp+)
done

consts
find_meth_def_in_list_f :: "meth_defs \<Rightarrow> meth \<Rightarrow> meth_def_opt"
primrec
"find_meth_def_in_list_f []       m = None"
"find_meth_def_in_list_f (md#mds) m =
  (case md of meth_def_def ms mb \<Rightarrow>
  (case ms of meth_sig_def cl m' vds \<Rightarrow>
  (if m = m' then Some md else find_meth_def_in_list_f mds m)))"
lemma [simp]: "((mds, m, md_opt) \<in> find_meth_def_in_list) = (find_meth_def_in_list_f mds m = md_opt)"
apply(rule)
 apply(induct rule: find_meth_def_in_list.induct) apply(simp+)
apply(induct mds) apply(simp) apply(rule fmdil_emptyI)
apply(clarsimp) apply(clarsimp split: meth_def.split meth_sig.split) apply(rule)
 apply(clarsimp) apply(rule fmdil_cons_trueI[simplified]) apply(force)
apply(clarsimp) apply(rule fmdil_cons_falseI[simplified]) apply(force+)
done

consts
find_meth_def_in_path_f :: "ctxclds \<Rightarrow> meth \<Rightarrow> ctxmeth_def_opt"
primrec
fmdip_empty: "find_meth_def_in_path_f []               m = None"
fmdip_cons:  "find_meth_def_in_path_f (ctxcld#ctxclds) m =
  (case ctxcld of (ctx, cld) \<Rightarrow>
  (case find_meth_def_in_list_f (class_methods_f cld) m of Some md \<Rightarrow> Some (ctx, md) | None \<Rightarrow>
    find_meth_def_in_path_f ctxclds m))"
lemma [simp]: "((ctxclds, m, ctxmeth_def_opt) \<in> find_meth_def_in_path) = (find_meth_def_in_path_f ctxclds m = ctxmeth_def_opt)"
apply(rule)
 apply(induct rule: find_meth_def_in_path.induct) apply(simp+)
apply(induct ctxclds) apply(simp) apply(rule fmdip_emptyI)
apply(clarsimp) apply(case_tac "find_meth_def_in_list_f (class_methods_f b) m") apply(clarsimp)
apply(simp add: fmdip_cons_falseI[simplified])
apply(simp add: fmdip_cons_trueI[simplified])
done

constdefs
find_meth_def_f :: "P \<Rightarrow> ty \<Rightarrow> meth \<Rightarrow> ctxmeth_def_opt"
find_meth_def_f_def: "find_meth_def_f P ty m ==
  (case find_path_ty_f P ty of None \<Rightarrow> None | Some ctxclds \<Rightarrow>
    find_meth_def_in_path_f ctxclds m)"
lemma [simp]: "((P, ty, m, ctxmd_opt) \<in> find_meth_def) = (find_meth_def_f P ty m = ctxmd_opt)"
apply(rule)
 apply(induct rule: find_meth_def.induct) apply(simp add: find_meth_def_f_def)+
apply(clarsimp simp add: find_meth_def_f_def split: option.splits)
apply(simp add: fmd_nullI)
apply(simp add: fmd_optI)
done

consts
lift_opts :: "'a option list \<Rightarrow> 'a list option"
primrec
"lift_opts []         = Some []"
"lift_opts (opt#opts) =
  (case opt of None \<Rightarrow> None | Some v \<Rightarrow>
  (case lift_opts opts of None \<Rightarrow> None | Some vs \<Rightarrow> Some (v#vs)))"

constdefs
mtype_f :: "P \<Rightarrow> ty \<Rightarrow> meth \<Rightarrow> mty option"
mtype_f_def: "mtype_f P ty m ==
  (case find_meth_def_f P ty m of None \<Rightarrow> None | Some (ctx, md) \<Rightarrow>
  (case md of meth_def_def ms mb \<Rightarrow>
  (case ms of meth_sig_def cl m' vds \<Rightarrow>
  (case find_type_f P ctx cl of None \<Rightarrow> None | Some ty' \<Rightarrow>
  (case lift_opts (map (\<lambda>vd. case vd of vd_def clk vark \<Rightarrow> find_type_f P ctx clk) vds) of None \<Rightarrow> None | Some tys \<Rightarrow>
    Some (mty_def tys ty'))))))"

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

lemma find_md_m_match'[rule_format]:
  "find_meth_def_in_list_f mds m = Some (meth_def_def (meth_sig_def cl m' vds) mb) \<longrightarrow> m' = m"
apply(induct mds) apply(simp) apply(clarsimp split: meth_def.splits meth_sig.splits) done

lemma find_md_m_match:
  "find_meth_def_in_path_f path m = Some (ctx, meth_def_def (meth_sig_def cl m' vds) mb) \<longrightarrow> m' = m"
apply(induct path) apply(simp) apply(clarsimp split: option.splits) by(rule find_md_m_match')

lemma vds_map_length:
  "length (map (vd_case (\<lambda>clk vark. find_type_f P ctx clk)) vds) = length vds"
by (induct vds, auto)

lemma lift_opts_length[rule_format]:
  "\<forall>tys. lift_opts ty_opts = Some tys \<longrightarrow> length ty_opts = length tys"
apply(induct ty_opts) apply(simp) by(clarsimp split: option.splits)

lemma vds_tys_length_eq[rule_format]:
  "lift_opts (map (vd_case (\<lambda>clk vark. find_type_f P ctx clk)) vds) = Some tys \<longrightarrow> length vds = length tys"
apply(rule) apply(drule lift_opts_length) apply(simp add: vds_map_length) done

lemma vds_tys_length_eq'[rule_format]:
  "\<forall>tys. length vds = length tys \<longrightarrow> vds = map (\<lambda>(cl, var, ty). vd_def cl var) (map (\<lambda>(vd, ty). case vd of vd_def cl var \<Rightarrow> (cl, var, ty)) (zip vds tys))"
apply(induct vds) apply(simp) apply(clarsimp) apply(case_tac a) apply(clarsimp)
apply(case_tac tys) apply(simp) apply(clarsimp) done

lemma vds_tys_length_eq''[rule_format]:
  "\<forall>vds. length vds = length tys \<longrightarrow> tys = map (\<lambda>(cl, var, ty::ty). ty) (map (\<lambda>(vd, ty). case vd of vd_def cl var \<Rightarrow> (cl, var, ty)) (zip vds tys))"
apply(induct tys) apply(simp) apply(clarsimp) apply(case_tac vds) apply(clarsimp) apply(clarsimp)
apply(split vd.splits) apply(simp) done

lemma lift_opts_find_type[rule_format]:
  "\<forall>tys. lift_opts (map (vd_case (\<lambda>clk vark. find_type_f P ctx clk)) vds) = Some tys
      \<longrightarrow> (\<forall>(vd, ty) \<in> set (zip vds tys). case vd of vd_def cl var \<Rightarrow> find_type_f P ctx cl = Some ty)"
apply(induct vds) apply(simp) apply(clarsimp split: vd.splits option.splits) apply(rename_tac cl' var)
apply(drule_tac x = "(vd_def cl' var, b)" in bspec, simp) apply(force) done

lemma [simp]: "((P, ty, m, mty) \<in> mtype) = (mtype_f P ty m = Some mty)"
apply(rule)
 apply(induct rule: mtype.induct) apply(clarsimp simp add: mtype_f_def)
 apply(split option.splits) apply(rule) apply(clarsimp)
 apply(rule_tac x = "map (\<lambda>(cl, var, ty). ty) cl_var_ty_list" in exI)
 apply(simp add: lift_opts_ind) apply(clarsimp) apply(simp add: lift_opts_ind)
apply(clarsimp simp add: mtype_f_def split: option.splits meth_def.splits meth_sig.splits)
apply(rename_tac ctx mb cl m' vds ty' tys)
apply(rule_tac ctx = ctx and cl = cl and meth_body = mb and ty' = ty'
           and cl_var_ty_list = "map (\<lambda>(vd, ty). case vd of vd_def cl var \<Rightarrow> (cl, var, ty)) (zip vds tys)"
           and meth_def = "meth_def_def (meth_sig_def cl m' vds) mb" in mtypeI[simplified])
 apply(simp) apply(clarsimp) apply(rule) apply(clarsimp simp add: find_meth_def_f_def split: option.splits)
 apply(simp add: find_md_m_match) apply(drule vds_tys_length_eq) apply(simp add: vds_tys_length_eq')
 apply(simp) apply(clarsimp) apply(split vd.splits) apply(clarsimp) apply(drule lift_opts_find_type) apply(simp)
 apply(clarsimp)
apply(clarsimp) apply(drule vds_tys_length_eq) apply(simp add: vds_tys_length_eq'')
done

constdefs
is_sty_one :: "P \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool option"
is_sty_one_def: "is_sty_one P ty ty' \<equiv>
  (case find_path_ty_f P ty of None \<Rightarrow> None | Some path \<Rightarrow>
  (case ty' of ty_top \<Rightarrow> Some True | ty_def ctx' dcl' \<Rightarrow>
  (case ctx' of ctx_def mi' pn' \<Rightarrow>
  (case find_cld_f P ctx' (fqn_def pn' dcl') of None \<Rightarrow> None | Some ctxcld \<Rightarrow>
     Some (ctxcld \<in> set path)))))"

lemma classname_mem_map[rule_format]:
  "(ctx, cld, class_name_f cld) \<in> set ctx_cld_dcl_list
     \<longrightarrow> (ctx, class_name_f cld) mem map (\<lambda>(ctx, cld). (ctx, class_name_f cld)) (map (\<lambda>(ctx, cld, dcl). (ctx, cld)) ctx_cld_dcl_list)"
by (induct ctx_cld_dcl_list, auto)

lemma map_map_three:
  "ctxclds = map (\<lambda>(ctx, cld, dcl). (ctx, cld)) (map (\<lambda>(ctx, cld). (ctx, cld, class_name_f cld)) ctxclds)"
by (induct ctxclds, auto)

lemma mem_el_map[rule_format]:
  "(ctx, dcl) mem map (\<lambda>(ctx, cld). (ctx, class_name_f cld)) ctxclds
     \<longrightarrow> (ctx, dcl) \<in> (\<lambda>(ctx, cld, y). (ctx, y)) ` set (map (\<lambda>(ctx, cld). (ctx, cld, class_name_f cld)) ctxclds)"
by (induct ctxclds, auto)

lemma [simp]: "((P, ty, ty') \<in> sty_one) = (is_sty_one P ty ty' = Some True)"
apply(rule)
 apply(induct rule: sty_one.induct)
  apply(simp add: is_sty_one_def)
 apply(clarsimp simp add: is_sty_one_def)
apply(clarsimp simp add: is_sty_one_def split: option.splits ty.splits)
 apply(simp add: sty_objI)
apply(rename_tac path ctx' dcl') apply(case_tac ctx', rename_tac mi' pn', clarsimp)
apply(clarsimp split: option.splits) apply(rename_tac ctx cld)
apply(force intro: sty_dclI)
done

lemma path_append[rule_format]:
  "find_path_rec_f (P, ctx, cl, path') = Some path \<Longrightarrow> \<exists>path''. path = path' @ path''"
apply(induct rule: find_path_rec_f.induct)
 apply(clarsimp)
apply(clarsimp split: split_if_asm option.splits)
done

lemma fcis_no_fqn_no_cld[rule_format]:
  "fqn_def pn dcl \<notin> full_name_f ` set clds \<longrightarrow>
      find_cld_in_self_f clds pn' (fqn_def pn dcl) = None"
by (induct clds, auto simp add: full_name_f_def split: cld.splits)

lemma fcim_no_fqn_no_cld[rule_format]:
  "fqn_def pn dcl \<notin> full_name_f ` set clds \<longrightarrow>
      find_cld_in_module_f clds (fqn_def pn dcl) = None"
by (induct clds, auto simp add: full_name_f_def split: cld.splits)

lemma find_cld_in_self_same_ctx[rule_format]:
  "\<forall>pn fqn cld. find_cld_in_self_f clds pn fqn = Some cld \<longrightarrow>
       find_cld_in_self_f clds (package_name_f cld) fqn = Some cld"
apply(induct clds) apply(simp) apply(clarsimp)
apply(case_tac fqn, rename_tac pn' dcl, clarsimp)
apply(case_tac a) apply(rename_tac pn'' am dcl' cl fds mds) apply(clarsimp)
apply(split split_if_asm)
 apply(clarsimp simp add: package_name_f_def full_name_f_def)
apply(case_tac cld) apply(rename_tac pn''' am' dcl'' cl' fds' mds')
apply(clarsimp simp add: package_name_f_def full_name_f_def) apply(rule)
 apply(clarsimp) apply(frule find_cld_in_self_name_eq) apply(clarsimp)
 apply(erule_tac x = pn in allE)
 apply(erule_tac x = "fqn_def pn'' dcl'" in allE)
 apply(erule_tac x = "cld_def pn'' am' dcl' cl' fds' mds'" in allE)
 apply(clarsimp simp add: distinct_fqns_f_def full_name_f_def fcis_no_fqn_no_cld)
apply(clarsimp)
apply(erule_tac x = pn in allE)
apply(erule_tac x = "fqn_def pn' dcl" in allE)
apply(erule_tac x = "cld_def pn''' am' dcl'' cl' fds' mds'" in allE)
apply(clarsimp)
done

lemma fcim2fcis[rule_format]:
  "\<forall>fqn cld'. find_cld_in_module_f clds fqn = Some cld'
       \<longrightarrow> find_cld_in_self_f clds (package_name_f cld') fqn = Some cld'"
apply(induct clds rule: find_cld_in_module_f.induct)
 apply(simp)
apply(clarsimp)
apply(case_tac fqn, rename_tac pn dcl, clarsimp)
apply(case_tac cld, rename_tac pn' am dcl' cl fds mds, clarsimp)
apply(case_tac "am = am_public \<and> pn = pn' \<and> dcl = dcl'") apply(clarsimp)
apply(clarsimp) apply(case_tac cld', rename_tac pn'' am'' dcl'' cl'' fds'' mds'', clarsimp)
apply(clarsimp simp add: package_name_f_def full_name_f_def distinct_fqns_f_def)
apply(drule fcim_no_fqn_no_cld) apply(force)
done

lemma fcii2fcis[rule_format]:
  "\<forall>mi' pn' cld' mn' clds' ms' fqns mis'.
      find_cld_in_imports_f (MH, mis, fqn) = Some (ctx_def mi' pn', cld') \<and>
      MH mi' = Some (md_def mn' clds' ms' fqns, mis')
          \<longrightarrow> find_cld_in_self_f clds' pn' fqn = Some cld'"
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, rename_tac mn clds ms fqns', clarsimp)
apply(case_tac "fqn \<in> set fqns'")
 apply(case_tac "find_cld_in_imports_f (MH, mis'', fqn)")
  apply(case_tac "find_cld_in_module_f clds fqn")
   apply(simp)
  apply(clarsimp simp add: fcim2fcis)
 apply(simp)
apply(simp)
done

lemma list_inter_assoc[rule_format]:
  "\<forall>ys zs. list_inter (list_inter xs ys) zs = list_inter xs (list_inter ys zs)"
apply(induct xs) apply(simp) apply(clarsimp) apply(auto simp add: list_inter_conv)
done

declare [[simp_depth_limit = 1]]
lemma found_not_in_imports[rule_format]:
  "\<forall>mi' pn' cld' mn' clds' ms' fqns mis'.
      find_cld_in_imports_f (MH, mis, fqn) = Some (ctx_def mi' pn', cld')
        \<longrightarrow> MH mi' = Some (md_def mn' clds' ms' fqns, mis')
            \<longrightarrow> find_cld_in_imports_f (MH, mis', fqn) = None"
apply(induct_tac MH mis fqn rule: fcii_induct) apply(simp)
apply(clarify) apply(simp only: fcii_rec_call_valid)
apply(split split_if_asm) apply(clarify)
apply(split option.splits) apply(clarify) apply(clarify)
apply(rename_tac md mis'') apply(case_tac md) apply(rename_tac mn clds ms fqns', clarsimp)
apply(split split_if_asm)
 apply(thin_tac "?P \<longrightarrow> ?Q") apply(thin_tac "?P") back apply(simp)
apply(split option.splits)
 apply(split option.splits)
  apply(blast)
 apply(force)
apply(force)
done
declare [[simp_depth_limit = 1000]]

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

lemma find_cld_same_ctx[rule_format]:
  "find_cld_f P ctx fqn = Some (ctx', cld') \<longrightarrow> find_cld_f P ctx' fqn = Some (ctx', cld')"
apply(simp add: find_cld_f_def split: option.splits)
apply(case_tac P, rename_tac RC MH, clarsimp)
apply(case_tac ctx, rename_tac mi pn, clarsimp split: option.splits) apply(rename_tac md mis)
apply(case_tac md, rename_tac mn clds ms fqns, clarsimp)
apply(case_tac "find_cld_in_imports_f (MH, mis, fqn)")
 apply(simp) apply(case_tac "find_cld_in_self_f clds pn fqn") apply(simp)
 apply(clarsimp) apply(drule find_cld_in_self_same_ctx) apply(clarsimp)
apply(clarsimp) apply(case_tac ctx', rename_tac mi' pn', clarsimp)
apply(clarsimp split: option.splits)
apply(subgoal_tac "\<exists>md mis'. MH mi' = Some (md, mis')") apply(clarsimp) apply(case_tac md, rename_tac mn' clds' ms' fqns', clarsimp)
apply(subgoal_tac "find_cld_in_imports_f (MH, mis', fqn) = None") (* because otherwise it would've been found before *)
apply(subgoal_tac "find_cld_in_self_f clds' pn' fqn = Some cld'")
apply(simp) apply(case_tac fqn, rename_tac pn'' dcl, clarsimp)
apply(case_tac cld') apply(rename_tac pn''' am dcl' cl fds mds)
apply(drule find_cld_in_self_name_eq) apply(clarsimp simp add: package_name_f_def)
apply(drule find_cld_in_imports_name_eq) apply(force) apply(force)
  apply(rule fcii2fcis) apply(force)
 apply(force intro: found_not_in_imports)
apply(frule fcii_mi_exists) apply(simp)
done

lemma fpr_same_with_fst_ctx[rule_format]:
  "find_path_rec_f (P, ctx, cl, prefix) = Some path \<longrightarrow>
     (\<forall>ctx_u cld suffix. path = prefix @ (ctx_u, cld) # suffix \<longrightarrow>
          find_path_rec_f (P, ctx_u, cl, prefix) = Some path)"
apply(induct_tac P ctx cl prefix rule: find_path_rec_f.induct)
 apply(simp)
apply(clarsimp) apply(case_tac "find_cld_f P ctx fqn") apply(simp)
apply(clarsimp) apply(rename_tac ctx_u' cld')
apply(frule path_append) apply(clarsimp)
apply(subgoal_tac " find_cld_f P ctx_u' fqn = Some (ctx_u', cld')")
 apply(simp)
apply(simp add: find_cld_same_ctx)
done

lemma all_in_path_found'[rule_format]:
  "\<forall>suffix. find_path_rec_f (P, ctx, cl, prefix) = Some (prefix @ suffix) \<longrightarrow>
      (\<forall>(ctx', cld') \<in> set suffix. find_cld_f P ctx' (full_name_f cld') = Some (ctx', cld'))"
apply(induct_tac P ctx cl prefix rule: find_path_rec_f.induct)
 apply(clarsimp)
apply(rule)
apply(clarsimp split: split_if_asm option.splits)
apply(frule path_append) apply(clarsimp) apply(erule disjE)
 apply(clarsimp) apply(case_tac fqn) apply(clarify) apply(frule find_cld_name_eq)
 apply(clarsimp simp add: full_name_f_def) apply(frule find_cld_same_ctx) apply(assumption)
apply(drule_tac x = "(aa, ba)" in bspec, simp) apply(simp)
done

lemma all_in_path_found:
  "\<lbrakk>find_path_f P ctx cl = Some path; (ctx', cld') \<in> set path\<rbrakk>
      \<Longrightarrow> find_cld_f P ctx' (full_name_f cld') = Some (ctx', cld')"
apply(unfold find_path_f_def)
apply(frule_tac x = "(ctx', cld')" in all_in_path_found'[of _ _ _ "[]", simplified]) apply(simp+)
done

lemma fpr_target_is_head':
  "find_path_rec_f (P, ctx, cl, path') = Some path \<longrightarrow>
     (\<forall>fqn ctxcld. cl = cl_fqn fqn \<and> find_cld_f P ctx fqn = Some ctxcld \<longrightarrow>
          (\<exists>path''. path = path' @ ctxcld # path''))"
apply(induct_tac P ctx cl path' rule: find_path_rec_f.induct)
 apply(simp)
apply(clarsimp split: split_if_asm option.splits)
apply(case_tac "superclass_name_f b") apply(clarsimp)
apply(clarsimp split: split_if_asm option.splits)
done

lemma fpr_target_is_head:
  "find_path_f P ctx (cl_fqn fqn) = Some path \<Longrightarrow> \<exists>ctxcld. find_cld_f P ctx fqn = Some ctxcld \<and> (\<exists>path''. path = ctxcld # path'')"
apply(unfold find_path_f_def) apply(frule fpr_target_is_head'[of _ _ _ "[]", THEN mp]) apply(clarsimp split: option.splits) done

lemma fpr_sub_path':
  "find_path_rec_f (P, ctx, cl, path') = Some path \<longrightarrow>
     (\<forall>fqn ctxcld path'' path_fqn.
         cl = cl_fqn fqn \<and> find_cld_f P ctx fqn = Some ctxcld \<and>
         find_path_rec_f (P, fst ctxcld, superclass_name_f (snd ctxcld), path'') = Some path_fqn \<longrightarrow>
              (\<exists>path'''. path_fqn = path'' @ path''' \<and> path = path' @ ctxcld # path'''))"
apply(induct_tac P ctx cl path' rule: find_path_rec_f.induct)
 apply(simp)
apply(clarsimp split: split_if_asm option.splits)
apply(case_tac "superclass_name_f b") apply(simp add: find_path_f_def)
apply(clarsimp split: split_if_asm option.splits)
apply(force)
done

lemma fpr_sub_path:
  "\<lbrakk>find_path_f P ctx (cl_fqn fqn) = Some path; find_cld_f P ctx fqn = Some ctxcld;
    find_path_f P (fst ctxcld) (superclass_name_f (snd ctxcld)) = Some path'\<rbrakk>
       \<Longrightarrow> path = ctxcld # path'"
by (unfold find_path_f_def, force intro: fpr_sub_path'[rule_format, of _ _ _ "[]" _ _ _ "[]", simplified])

lemma fpr_sub_path_simp:
  "\<lbrakk>find_path_rec_f (P, ctx, superclass_name_f cld, path'') = Some path_fqn;
    find_cld_f P ctx' fqn = Some (ctx, cld); P \<in> acyclic_clds;
    find_path_rec_f (P, ctx, superclass_name_f cld, path' @ [(ctx, cld)]) = Some path\<rbrakk>
       \<Longrightarrow> \<exists>path'''. path_fqn = path'' @ path''' \<and> path = path' @ (ctx, cld) # path'''"
apply(cut_tac P = P and ctx = ctx' and cl = "cl_fqn fqn" and path' = path' and path = path in fpr_sub_path')
apply(clarsimp split: option.splits split_if_asm)
done

lemma fpr_same_suffix'[rule_format]:
  "find_path_rec_f (P, ctx, cl, prefix) = Some path \<longrightarrow>
     (\<forall>suffix prefix'. path = prefix @ suffix \<longrightarrow>
          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(clarsimp)
apply(clarsimp split: option.splits)
apply(frule path_append) apply(clarify)
apply(erule_tac x = path'' in allE) apply(simp)
done

lemma fpr_same_suffix:
  "find_path_rec_f (P, ctx, cl, path_prefix) = Some path \<longrightarrow>
     (\<forall>path_suffix path_prefix' path_suffix'.
          path = path_prefix @ path_suffix \<and>
          find_path_rec_f (P, ctx, cl, path_prefix') = Some (path_prefix' @ path_suffix')
             \<longrightarrow> path_suffix = path_suffix')"
apply(induct_tac P ctx cl path_prefix rule: find_path_rec_f.induct)
 apply(clarsimp)
apply(clarsimp split: option.splits)
apply(frule path_append) apply(clarify)
apply(erule_tac x = path'' in allE)
apply(erule_tac x = "path_prefix' @ [(a, b)]" in allE)
apply(erule_tac x = "tl path_suffix'" in allE)
apply(clarsimp)
apply(case_tac fqn) apply(rename_tac pn dcl) apply(clarify) apply(frule find_cld_name_eq) apply(clarsimp)
apply(frule fpr_sub_path_simp) back apply(simp) apply(simp) apply(simp) apply(erule exE)
apply(simp)
done

lemma fpr_mid_path'[rule_format]:
  "find_path_rec_f (P, ctx, cl, path') = Some path \<longrightarrow>
     (\<forall>ctxcld \<in> set path.
         ctxcld \<in> set path' \<or>
         (\<forall>path_fqn. find_path_rec_f (P, fst ctxcld, cl_fqn (full_name_f (snd ctxcld)), path'') = Some path_fqn \<longrightarrow>
              (\<forall>path'''. path_fqn = path'' @ path''' \<longrightarrow> (\<exists>path_rest. path = path_rest @ path'''))))"
apply(induct_tac P ctx cl path' rule: find_path_rec_f.induct)
 apply(simp)
apply(clarsimp split: option.splits) apply(case_tac fqn) apply(rename_tac pn dcl) apply(clarsimp)
apply(frule find_cld_name_eq) apply(clarsimp)
apply(rename_tac path' ctx'' cld ctx' cld' path''' pn dcl mi am cl fds mds)
apply(drule_tac x = "(ctx'', cld)" in bspec, simp) apply(clarsimp)
apply(simp add: superclass_name_f_def full_name_f_def)
apply(case_tac cld') apply(rename_tac pn' am' dcl' cl' fds' mds') apply(clarsimp simp add: class_name_f_def)
apply(frule find_cld_name_eq) back apply(clarsimp)
apply(frule path_append) apply(frule path_append) back apply(clarsimp)
apply(rule_tac x = path' in exI) apply(clarsimp)
apply(subgoal_tac "find_path_rec_f (P, ctx, cl_fqn (fqn_def pn' dcl'), path') =
                   Some (path' @ (ctx_def mi pn', cld_def pn' am dcl' cl fds mds) # path''a)")
 apply(frule_tac x = "(ctx_def mi pn', cld_def pn' am dcl' cl fds mds)" in all_in_path_found') apply(simp)
 apply(simp add: full_name_f_def superclass_name_f_def)
 apply(drule_tac path_suffix = path''a and path_prefix' = "path'' @ [(ctx_def mi pn', cld_def pn' am dcl' cl fds mds)]" and
                 path_suffix' = path''aa in fpr_same_suffix[rule_format])
  apply(simp) apply(simp) apply(simp add: superclass_name_f_def)
done

lemma fpr_mid_path:
  "\<lbrakk>find_path_f P ctx cl = Some path; (ctx', cld') \<in> set path; find_path_f P ctx' (cl_fqn (full_name_f cld')) = Some path'\<rbrakk>
       \<Longrightarrow> \<exists>path''. path = path'' @ path'"
apply(cut_tac  P = P and ctx = ctx and cl = cl and path' = "[]" and path = path and ctxcld = "(ctx', cld')" and path'' = "[]" in fpr_mid_path')
apply(unfold find_path_f_def, assumption) apply(assumption) apply(simp)
done

lemma fpr_first_in_path'[rule_format]:
  "find_path_rec_f (P, ctx, cl, path') = Some path \<longrightarrow>
      (\<forall>fqn ctxcld. cl = cl_fqn fqn \<and> find_cld_f P ctx fqn = Some ctxcld \<longrightarrow> ctxcld \<in> set path)"
apply(case_tac cl)
 apply(simp)
apply(clarsimp) apply(drule path_append) apply(force)
done

lemma fpr_first_in_path:
  "\<lbrakk>find_path_f P ctx (cl_fqn fqn) = Some path; find_cld_f P ctx fqn = Some ctxcld\<rbrakk> \<Longrightarrow> ctxcld \<in> set path"
by (unfold find_path_f_def, force intro: fpr_first_in_path'[of _ _ _ "[]", simplified])

lemma cld_for_path:
  "find_path_f P ctx (cl_fqn fqn) = Some path \<Longrightarrow> \<exists>ctxcld. find_cld_f P ctx fqn = Some ctxcld"
apply(unfold find_path_f_def) apply(clarsimp split: split_if_asm option.splits) done

lemma ctx_cld_ctx_dcl[rule_format]:
  "(ctx, cld_def pn am dcl cl fds mds) \<in> set path \<longrightarrow> (ctx, dcl) \<in> (\<lambda>(ctx, cld). (ctx, class_name_f cld)) ` set path"
by (induct path, auto simp add: class_name_f_def)

lemma ctx_dcl_ctx_cld[rule_format]:
  "(ctx, dcl) \<in> (\<lambda>(ctx, cld). (ctx, class_name_f cld)) ` set path \<longrightarrow> (\<exists>pn am cl fds mds. (ctx, cld_def pn am dcl cl fds mds) \<in> set path)"
apply(clarsimp) apply(rename_tac cld) apply(case_tac cld) apply(rename_tac pn am dcl cl fds mds)
apply(force simp add: class_name_f_def)
done

lemma ctx_dcl_mem_path:
  "find_path_f P ctx (cl_fqn (fqn_def pn dcl)) = Some path \<Longrightarrow> \<exists>ctx'. (ctx', dcl) \<in> (\<lambda>(ctx, cld). (ctx, class_name_f cld)) ` set path"
apply(frule cld_for_path) apply(erule exE)
apply(frule fpr_first_in_path) apply(assumption)
apply(frule find_cld_name_eq) apply(elim exE)
apply(clarsimp simp add: ctx_cld_ctx_dcl class_name_f_def) apply(force)
done

lemma sty_reflexiveI:
  "is_sty_one P ty ty' = Some True \<Longrightarrow> is_sty_one P ty ty = Some True"
apply(simp add: is_sty_one_def split: option.splits)
apply(case_tac ty')
 apply(clarsimp) apply(rename_tac path) apply(case_tac ty)
  apply(clarsimp)
 apply(rename_tac ctx dcl, clarsimp) apply(case_tac ctx, rename_tac mi pn, clarsimp)
 apply(frule fpr_target_is_head) apply(clarsimp)
apply(rename_tac ctx' dcl') apply(clarsimp)
apply(case_tac ctx', rename_tac mi' pn', clarsimp)
apply(clarsimp split: option.splits) apply(rename_tac ctx cld)
apply(case_tac ty) apply(simp)
apply(rename_tac ctx' dcl') apply(clarsimp) apply(case_tac ctx', rename_tac mi pn, clarsimp)
apply(frule fpr_target_is_head) apply(clarsimp)
done

lemma fpr_same_ctx'[rule_format]:
  "find_path_rec_f (P, ctx, cl, prefix) = Some path \<longrightarrow>
     (\<forall>suffix ctx' cld'. path = prefix @ (ctx', cld') # suffix \<and>
                         find_cld_f P ctx' (full_name_f cld') = Some (ctx', cld') \<longrightarrow>
          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(rename_tac path') apply(clarsimp)
apply(case_tac "find_cld_f P ctx fqn", simp, clarsimp) apply(rename_tac ctx'' cld'')
apply(frule path_append) apply(clarsimp)
done

lemma fpr_same_ctx[rule_format]:
  "find_path_f P ctx cl = Some ((ctx', cld') # path')
     \<Longrightarrow> find_path_f P ctx' (cl_fqn (full_name_f cld')) = Some ((ctx', cld') # path')"
apply(frule_tac ctx' = ctx' and cld' = cld' in all_in_path_found) apply(simp)
by (unfold find_path_f_def, simp add: fpr_same_ctx'[of _ _ _ "[]", simplified])

lemma sty_transitiveI:
  "\<lbrakk>is_sty_one P ty ty' = Some True; is_sty_one P ty' ty'' = Some True\<rbrakk>
       \<Longrightarrow> is_sty_one P ty ty'' = Some True"
apply(clarsimp simp add: is_sty_one_def split: option.splits) apply(rename_tac path_ty path_ty')
apply(case_tac ty')
 apply(clarsimp) apply(case_tac ty'')
  apply(clarsimp)
 apply(clarsimp split: ctx.splits option.splits)
apply(clarsimp) apply(rename_tac dcl', case_tac ctx, rename_tac mi' pn', clarsimp split: option.splits)
apply(rename_tac ctx' cld') apply(case_tac ty'')
 apply(clarsimp)
apply(rename_tac ctx_ty'' dcl'') apply(clarsimp) apply(case_tac ctx_ty'', rename_tac mi'' pn'', clarsimp split: option.splits)
apply(rename_tac ctx'' cld'') apply(case_tac ty) apply(simp)
apply(rename_tac ctx dcl, clarsimp) apply(case_tac ctx, rename_tac mi pn, clarsimp)
apply(frule_tac path = path_ty and path' = path_ty' in fpr_mid_path) apply(force)
apply(frule_tac path = path_ty' in fpr_target_is_head) apply(clarsimp)
apply(frule all_in_path_found) apply(force)
apply(frule_tac ctx = "ctx_def mi' pn'" in  fpr_same_ctx) apply(simp add: full_name_f_def)
apply(clarsimp)
done

constdefs
is_sty_many :: "P \<Rightarrow> tys \<Rightarrow> tys \<Rightarrow> bool option"
is_sty_many_def: "is_sty_many P tys tys' \<equiv>
  (if length tys \<noteq> length tys' then None else
  (case lift_opts (map (\<lambda>(ty, ty'). is_sty_one P ty ty') (zip tys tys'))
     of None \<Rightarrow> None | Some bools \<Rightarrow> Some (list_all id bools)))"

lemma lift_opts_exists:
  "\<forall>x\<in>set ty_ty'_list. (\<lambda>(ty, ty'). is_sty_one P ty ty' = Some True) x \<Longrightarrow> \<exists>bools. lift_opts (map (\<lambda>(ty, ty'). is_sty_one P ty ty') ty_ty'_list) = Some bools"
by (induct ty_ty'_list, auto)

lemma lift_opts_all_true[rule_format]:
  "\<forall>bools. (\<forall>x\<in>set ty_ty'_list. (\<lambda>(ty, ty'). is_sty_one P ty ty' = Some True) x) \<and>
            lift_opts (map (\<lambda>(ty, ty'). is_sty_one P ty ty') ty_ty'_list) = Some bools
                  \<longrightarrow> list_all id bools"
by (induct ty_ty'_list, auto split: option.splits)

lemma [simp]: "((P, tys, tys') \<in> sty_many) = (is_sty_many P tys tys' = Some True)"
apply(rule)
 apply(erule sty_many.cases) apply(clarsimp simp add: is_sty_many_def split: option.splits) apply(rule)
  apply(simp add: lift_opts_exists)
 apply(force intro: lift_opts_all_true)
apply(clarsimp simp add: is_sty_many_def split: option.splits split_if_asm)
apply(rule_tac ty_ty'_list = "zip tys tys'" in sty_manyI)
  apply(simp add: map_fst_zip[THEN sym])
 apply(simp add: map_snd_zip[THEN sym])
apply(clarsimp)
apply(rename_tac bools ty ty')
apply(induct "zip tys tys'")
 apply(simp)
apply(clarsimp split: option.splits)
apply(force)
done

constdefs
is_sty_opt :: "P \<Rightarrow> ty_opt \<Rightarrow> ty_opt \<Rightarrow> bool option"
is_sty_opt_def: "is_sty_opt P ty_opt ty_opt' \<equiv>
  (case ty_opt of None \<Rightarrow> None | Some ty \<Rightarrow>
  (case ty_opt' of None \<Rightarrow> None | Some ty' \<Rightarrow>
     is_sty_one P ty ty'))"

lemma is_sty_opt_iff: "((P, ty_opt, ty_opt') \<in> sty_option) = (is_sty_opt P ty_opt ty_opt' = Some True)"
apply(rule)
 apply(erule sty_option.cases) apply(clarsimp simp add: is_sty_opt_def)
apply(simp add: is_sty_opt_def sty_optionI split: option.splits)
done

(* TODO: here will go all the other definitions for functions equivalent to
   relations concerning well-formedness *)

constdefs
tr_x :: "T \<Rightarrow> x \<Rightarrow> x"
tr_x_def: "tr_x T x \<equiv>
  (case T x of None \<Rightarrow> x | Some x' \<Rightarrow> x')"

tr_var :: "T \<Rightarrow> var \<Rightarrow> var"
tr_var_def: "tr_var T var \<equiv>
  (case tr_x T (x_var var) of x_this \<Rightarrow> var | x_var var' \<Rightarrow> var')"

consts
tr_s_f  :: "T \<Rightarrow> s \<Rightarrow> s"
tr_ss_f :: "T \<Rightarrow> s list \<Rightarrow> s list"
primrec
"tr_s_f T (s_block ss)        = s_block (tr_ss_f T ss)"
"tr_s_f T (s_ass var x)       = s_ass (tr_var T var) (tr_x T x)"
"tr_s_f T (s_read var x f)    = s_read (tr_var T var) (tr_x T x) f"
"tr_s_f T (s_write x f y)     = s_write (tr_x T x) f (tr_x T y)"
"tr_s_f T (s_if x y s1 s2)    = s_if (tr_x T x) (tr_x T y) (tr_s_f T s1) (tr_s_f T s2)"
"tr_s_f T (s_call var x m ys) = s_call (tr_var T var) (tr_x T x) m (map (tr_x T) ys)"
"tr_s_f T (s_new var ctx cl)  = s_new (tr_var T var) ctx cl"

"tr_ss_f T [] = []"
"tr_ss_f T (s#ss) = tr_s_f T s # tr_ss_f T ss"

lemma [simp]: "\<forall>x\<in>set s_s'_list. (\<lambda>(s_XXX, s_'). (T, s_XXX, s_') \<in> tr_s \<and> tr_s_f T s_XXX = s_') x \<Longrightarrow> tr_ss_f T (map fst s_s'_list) = map snd s_s'_list"
by (induct s_s'_list, auto)

lemma [simp]: "(\<forall>x\<in>set y_y'_list. split (\<lambda>y_XXX. op = (case T y_XXX of None \<Rightarrow> y_XXX | Some x' \<Rightarrow> x')) x) \<longrightarrow> map (tr_x T) (map fst y_y'_list) = map snd y_y'_list"
apply(induct y_y'_list) apply(simp) apply(clarsimp) apply(simp only: tr_x_def) done

lemma tr_induct:
  "\<lbrakk>\<And>ss. (\<And>x. x \<in> set ss \<Longrightarrow> P x) \<Longrightarrow> P (s_block ss); \<And>var x. P (s_ass var x);
    \<And>var x f. P (s_read var x f); \<And>x f y. P (s_write x f y);
    \<And>x y s1 s2. \<lbrakk>P s1; P s2\<rbrakk> \<Longrightarrow> P (s_if x y s1 s2); \<And>var x m ys. P (s_call var x m ys);
    \<And>var ctx cl. P (s_new var ctx cl)\<rbrakk> \<Longrightarrow> P s"
apply(cut_tac tr_s_f_tr_ss_f.induct[of "\<lambda>ss. (\<forall>s\<in>set ss. P s)" P])
apply(simp_all) apply(force) done

lemma [simp]: "(s, s') \<in> set (zip ss (tr_ss_f T ss)) \<longrightarrow> s' = tr_s_f T s" by (induct ss, auto)

lemma [iff]: "length ss = length (tr_ss_f T ss)" by (induct ss, auto)

lemma tr_f_to_rel: "\<forall>s'. tr_s_f T s = s' \<longrightarrow> (T, s, s') \<in> tr_s"
apply(rule_tac s = s in tr_induct)
apply(simp) apply(cut_tac T = T and s_s'_list = "zip ss (tr_ss_f T ss)" in tr_s_blockI[simplified])
apply(clarsimp)
apply(subgoal_tac "\<forall>x. x \<in> set ss \<longrightarrow> (T, x, tr_s_f T x) \<in> tr_s")
apply(erule_tac x = a in allE) apply(subgoal_tac "a \<in> set ss") apply(subgoal_tac "b = tr_s_f T a") apply(simp)
apply(simp) apply(force simp add: set_zip) apply(simp) apply(subgoal_tac "length ss = length (tr_ss_f T ss)")
apply(simp only: map_fst_zip) apply(simp) apply(simp)
apply(clarsimp) apply(rule tr_s_var_assignI)
apply(clarsimp simp add: tr_x_def tr_var_def split: option.splits)
apply(simp add: tr_x_def)
apply(clarsimp) apply(rule tr_s_field_readI)
apply(clarsimp simp add: tr_x_def tr_var_def split: option.splits)
apply(simp add: tr_x_def)
apply(clarsimp) apply(rule tr_s_field_writeI)
apply(simp add: tr_x_def) apply(simp add: tr_x_def)
apply(clarsimp simp only: tr_s_f_tr_ss_f.simps) apply(rule tr_s_ifI)
apply(simp only: tr_x_def) apply(simp only: tr_x_def) apply(simp) apply(simp)
apply(clarify)
apply(cut_tac T = T and var = var and var' = "tr_var T var" and x = x and
              x' = "tr_x T x" and y_y'_list = "zip ys (map (tr_x T) ys)" and
              meth = m in tr_s_mcallI)
apply(clarsimp simp add: tr_x_def tr_var_def split: option.splits)
apply(simp only: tr_x_def) apply(clarsimp simp add: set_zip tr_x_def) apply(simp)
apply(clarsimp) apply(rule tr_s_newI)
apply(clarsimp simp add: tr_x_def tr_var_def split: option.splits)
done

lemma tr_rel_f_eq: "(((T, s, s') \<in> tr_s) = (tr_s_f T s = s'))"
apply(rule)
 apply(erule tr_s.induct) apply(simp add: tr_x_def tr_var_def split: option.splits)+
apply(cut_tac T = T and s = s in tr_f_to_rel) apply(simp)
done

end