Theory Lightweight_Java_Equivalence

(*  Title:       Lightweight Java, the equivalence functions
    Authors:     Rok Strnisa <rok@strnisa.com>, 2006
                 Matthew Parkinson <matt@matthewp.com>, 2006
    Maintainer:  
*)

theory Lightweight_Java_Equivalence imports Lightweight_Java_Definition begin

(* BEGIN: HELPER FUNCTIONS *)

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

lemma id_map_two[simp]: "map (λ(x,y). (x,y)) list = list" by (induct list) auto

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

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

lemma map_snd[simp]: "map (λ(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 (λe. [e]) list) = list"
by (induct list) simp_all

lemma list_all_map_P [simp]: "list_all (λb. b) (map (λx. P x) list) = (∀x ∈ set list. P x)"
by (induct list) simp_all

lemma dom_single[simp]: "a : dom (Map.empty(k ↦ v)) = (a = k)"
by (simp add: dom_def)

lemma predicted_lu[rule_format, simp]:
  "x ∈ set list ⟶ map_of (map (λkey. (key, value)) list) x = Some value"
by (induct list) auto

lemma key_in_map1[simp]: "k ∉ dom M' ⟹ (M ++ M') k = M k"
apply (subgoal_tac "M' k = None")
apply (simp add: map_add_def, force simp add: domI)
done

lemma forall_cons [rule_format]: "(∀x ∈ set (s#S). P x) ∧ y ∈ set S ⟶ P y"
by (induct_tac S) simp_all

lemma mem_cong[rule_format]:
  "x ∈ set list ⟶ (f x ∈ set (map f list))"
by (induct list) auto

lemma forall_union: "⟦∀a ∈ dom A. P (A a); ∀b ∈ dom B. P (B b)⟧ ⟹ ∀x ∈ dom A ∪ 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 *)

definition
class_name_f :: "cld ⇒ dcl"
where
"class_name_f cld =
  (case cld of cld_def dcl cl fds mds ⇒ dcl)"
lemma [simp]: "(class_name cld dcl) = (class_name_f cld = dcl)"
by (force simp add: class_name_f_def split: cld.splits
          intro: class_nameI elim: class_name.cases)

definition
superclass_name_f :: "cld ⇒ cl"
where
"superclass_name_f cld =
  (case cld of cld_def dcl cl fds mds ⇒ cl)"
lemma [simp]: "(superclass_name cld cl) = (superclass_name_f cld = cl)"
by (force simp add: superclass_name_f_def split: cld.splits
          intro: superclass_nameI elim: superclass_name.cases)

definition
class_fields_f :: "cld ⇒ fds"
where
"class_fields_f cld =
  (case cld of cld_def dcl cl fds mds ⇒ fds)"
lemma [simp]: "(class_fields cld fds) = (class_fields_f cld = fds)"
by (force simp add: class_fields_f_def split: cld.splits
          intro: class_fieldsI elim: class_fields.cases)

definition
class_methods_f :: "cld ⇒ meth_defs"
where
"class_methods_f cld =
  (case cld of cld_def dcl cl fds mds ⇒ mds)"
lemma [simp]: "(class_methods cld fds) = (class_methods_f cld = fds)"
by (force simp add: class_methods_f_def split: cld.splits
          intro: class_methodsI elim: class_methods.cases)

definition
method_name_f :: "meth_def ⇒ meth"
where
"method_name_f md =
  (case md of meth_def_def meth_sig meth_body ⇒
  (case meth_sig of meth_sig_def cl meth vds ⇒ meth))"
lemma [simp]: "(method_name md m) = (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)

definition
distinct_names_f :: "P ⇒ bool"
where
"distinct_names_f P =
  (distinct (map class_name_f P))"
lemma distinct_names_map[rule_format]:
  "(∀x∈set cld_dcl_list. case_prod (λcld. (=) (class_name_f cld)) x) ∧ distinct (map snd cld_dcl_list)
      ⟶ distinct_names_f (map fst cld_dcl_list)"
apply(induct cld_dcl_list)
 apply(clarsimp simp add: distinct_names_f_def)+ apply(force)
done
lemma [simp]: "(distinct_names P) = (distinct_names_f P)"
apply(rule)
 apply(erule distinct_names.cases) apply(clarsimp simp add: distinct_names_map)
apply(simp add: distinct_names_f_def)
apply(rule_tac cld_dcl_list = "map (λcld. (cld, class_name_f cld)) P" in dn_defI)
  apply(simp) apply(induct P) apply(simp) apply(simp)
 apply(clarsimp)
apply(clarsimp) apply(induct P) apply(simp) apply(force)
done

primrec
find_cld_f :: "P ⇒ ctx ⇒ fqn ⇒ ctxcld_opt"
where
"find_cld_f []         ctx fqn = None" |
"find_cld_f (cld#clds) ctx fqn =
  (case cld of cld_def dcl cl fds mds ⇒
  (case fqn of fqn_def dcl' ⇒
  (if dcl = dcl' then Some (ctx, cld) else find_cld_f clds ctx fqn)))"
lemma [simp]: "(find_cld P ctx fqn ctxcld_opt) = (find_cld_f P ctx fqn = ctxcld_opt)"
apply(rule)
 apply(induct rule: find_cld.induct) apply(simp+)
 apply(clarsimp)
apply(induct P)
 apply(simp add: fc_emptyI)
apply(case_tac fqn) apply(rename_tac cld clds dcl) apply(case_tac cld)
apply(clarsimp) apply(rename_tac dcl' cl' vds' mds') apply(rule)
apply(clarsimp) apply(rule fc_cons_trueI) apply(simp) apply(force)
apply(force intro: fc_cons_falseI[simplified])
done

lemma find_to_mem[rule_format]:
  "find_cld_f P ctx fqn = Some (ctx', cld) ⟶ cld : set P"
apply(induct P) by (clarsimp split: cld.splits fqn.splits)+

lemma find_cld_name_eq[rule_format]:
  "∀ctxcld. find_cld_f P ctx (fqn_def dcl) = Some ctxcld ⟶ (∃cl fds mds. (ctx, cld_def dcl cl fds mds) = ctxcld)"
apply(induct P) apply(simp) apply(clarsimp split: cld.splits fqn.splits) done

primrec
find_type_f :: "P ⇒ ctx ⇒ cl ⇒ ty_opt"
where
"find_type_f P ctx cl_object = Some ty_top" |
"find_type_f P ctx (cl_fqn fqn) =
  (case fqn of fqn_def dcl ⇒
  (case find_cld_f P ctx fqn of None ⇒ None | Some (ctx', cld) ⇒
     Some (ty_def ctx' dcl)))"
lemma [simp]: "(find_type P ctx cl ty_opt) = (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(rename_tac fqn)
apply(case_tac fqn) apply(clarsimp)
apply(split option.splits) apply(rule)
 apply(force intro: ft_nullI)
by (force intro: ft_dclI)

lemma mem_remove: "cld : set P ⟹ length (remove1 cld P) < length P"
apply(induct P) by(simp, force split: if_split_asm)

lemma finite_program[rule_format, intro]:
  "∀P cld. (∃ctx ctx' fqn. find_cld_f P ctx fqn = Some (ctx', cld)) ⟶
      length (remove1 cld P) < length P"
apply(clarsimp) apply(drule find_to_mem) by (simp add: mem_remove)

lemma path_length_eq[rule_format]:
  "path_length P ctx cl nn ⟹ ∀nn'. path_length P ctx cl nn' ⟶ 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 fpr_termination[iff]:
  "∀P cld ctx ctx' fqn. find_cld_f P ctx fqn = Some (ctx', cld) ∧ acyclic_clds P
       ⟶ The (path_length P ctx' (superclass_name_f cld)) < The (path_length P ctx (cl_fqn fqn))"
apply(clarsimp)
apply(erule acyclic_clds.cases) apply(clarsimp) apply(rename_tac P)
apply(erule_tac x = ctx 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

function
find_path_rec_f :: "P ⇒ ctx ⇒ cl ⇒ ctxclds ⇒ ctxclds_opt"
where
"find_path_rec_f P ctx  cl_object   path = Some path" |
"find_path_rec_f P ctx (cl_fqn fqn) path =
  (if ~(acyclic_clds P) then None else
  (case find_cld_f P ctx fqn of None ⇒ None | Some (ctx', cld) ⇒
   find_path_rec_f P ctx'
                    (superclass_name_f cld) (path @ [(ctx',cld)])))"
by pat_completeness auto
termination
by (relation "measure (λ(P, ctx, cl, path). (THE nn. path_length P ctx cl nn))") auto

lemma [simp]: "(find_path_rec P ctx cl path path_opt) = (find_path_rec_f P ctx cl path = path_opt)"
apply(rule)
 apply(erule 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 fpr_nullI)
 apply(simp add: fpr_nullI)
apply(rule fpr_fqnI) apply(force)+
done

definition
find_path_f :: "P ⇒ ctx ⇒ cl ⇒ ctxclds_opt"
where
"find_path_f P ctx cl = find_path_rec_f P ctx cl []"
lemma [simp]: "(find_path P ctx cl path_opt) = (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

primrec
find_path_ty_f :: "P ⇒ ty ⇒ ctxclds_opt"
where
"find_path_ty_f P  ty_top          = Some []" |
"find_path_ty_f P (ty_def ctx dcl) =
   find_path_f P ctx (cl_fqn (fqn_def dcl))"
lemma [simp]: "(find_path_ty P ty ctxclds_opt) = (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(clarsimp simp add: fpty_dclI)
done

primrec
fields_in_path_f :: "ctxclds ⇒ fs"
where
"fields_in_path_f []               = []" |
"fields_in_path_f (ctxcld#ctxclds) =
  (map (λfd. case fd of fd_def cl f ⇒ f) (class_fields_f (snd ctxcld)))
     @ fields_in_path_f ctxclds"
lemma cl_f_list_map: "map (case_fd (λcl f. f)) (map (λ(x, y). fd_def x y) cl_f_list) = map (λ(cl_XXX, f_XXX). f_XXX) cl_f_list"
by (induct cl_f_list, auto)

lemma fip_ind_to_f: "∀fs. fields_in_path clds fs ⟶ 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 (case_fd (λcl f. f)) (map (λ(x, y). fd_def x y) list) = map (λ(cl, f). f) list"
apply(induct list) apply(simp) apply(clarsimp) done

lemma fd_map_split': "map (λ(x, y). fd_def x y) (map (case_fd Pair) list) = list"
apply(induct list) apply(simp split: fd.splits)+ done

lemma fd_map_split'': "map ((λ(x, y). fd_def x y) ∘ case_fd Pair) list = list"
apply(induct list)  apply(simp split: fd.splits)+ done

lemma [simp]: "∀fs. (fields_in_path ctxclds fs) = (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(clarsimp)
apply(rule_tac cld = b and ctxcld_list = ctxclds
           and cl_f_list = "map (case_fd (λcl f. (cl, f))) (class_fields_f b)" in fip_consI[simplified])
  apply(simp add: fd_map_split'')
 apply(simp add: fd_map_split')
apply(clarsimp split: fd.splits)
done

definition
fields_f :: "P ⇒ ty ⇒ fs option"
where
"fields_f P ty =
  (case find_path_ty_f P ty of None ⇒ None | Some ctxclds ⇒
    Some (fields_in_path_f ctxclds))"
lemma [simp]: "∀fs_opt. (fields P ty fs_opt) = (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(rule fields_someI) apply(simp) apply(simp)
done

primrec
methods_in_path_f :: "clds ⇒ meths"
where
"methods_in_path_f []         = []" |
"methods_in_path_f (cld#clds) =
  map (λmd. case md of meth_def_def meth_sig meth_body ⇒
         case meth_sig of meth_sig_def cl meth vds ⇒ meth)
              (class_methods_f cld) @ methods_in_path_f clds"

lemma meth_def_map[THEN mp]:
  "(∀x ∈ set list. (λ(md, cl, m, vds, mb). md = meth_def_def (meth_sig_def cl m vds) mb) x)
     ⟶ map (case_meth_def (λms mb. case ms of meth_sig_def cl m vds ⇒ m)) (map (λ(md, cl, m, vds, mb). md) list) = map (λ(md, cl, m, vds, mb). m) list"
by (induct list, auto)

lemma meth_def_map':
  "map ((λ(md, cl, m, vds, mb). md) ∘ (λmd. case md of meth_def_def (meth_sig_def cl m vds) mb ⇒ (md, cl, m, vds, mb))) list = list"
apply(induct list) by (auto split: meth_def.splits meth_sig.splits)

lemma [simp]: "∀meths. (methods_in_path clds meths) = (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(force)

apply(rule_tac
  meth_def_cl_meth_vds_meth_body_list =
   "(case a of cld_def dcl cl fds mds ⇒
    (map (λmd. (case md of meth_def_def ms mb ⇒
               (case ms of meth_sig_def cl m vds ⇒ (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(clarsimp split: meth_def.splits meth_sig.splits)
 apply(simp)
apply(clarsimp) apply(case_tac a) apply(clarsimp simp add: class_methods_f_def split: meth_def.splits meth_sig.splits)
done

definition
methods_f :: "P ⇒ ty ⇒ meths option"
where
"methods_f P ty =
  (case find_path_ty_f P ty of None ⇒ None | Some ctxclds ⇒
    Some (methods_in_path_f (map (λ(ctx, cld). cld) ctxclds)))"
lemma [simp]: "(methods P ty meths) = (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

primrec
ftype_in_fds_f :: "P ⇒ ctx ⇒ fds ⇒ f ⇒ ty_opt_bot"
where
"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' ⇒ (if f = f' then
  (case find_type_f P ctx cl of None ⇒ ty_opt_bot_bot | Some ty ⇒
     ty_opt_bot_opt (Some ty)) else ftype_in_fds_f P ctx fds f))"
lemma [simp]: "(ftype_in_fds P ctx fds f ty_opt) = (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

primrec
ftype_in_path_f :: "P ⇒ ctxclds ⇒ f ⇒ ty_opt"
where
"ftype_in_path_f P []               f = None" |
"ftype_in_path_f P (ctxcld#ctxclds) f =
  (case ctxcld of (ctx, cld) ⇒
  (case ftype_in_fds_f P ctx (class_fields_f cld) f of
     ty_opt_bot_bot ⇒ None | ty_opt_bot_opt ty_opt ⇒
  (case ty_opt of Some ty ⇒ Some ty | None ⇒
     ftype_in_path_f P ctxclds f)))"
lemma [simp]: "(ftype_in_path P ctxclds f ty_opt) = (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(hypsubst_thin)
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

definition
ftype_f :: "P ⇒ ty ⇒ f ⇒ ty_opt"
where
"ftype_f P ty f =
  (case find_path_ty_f P ty of None ⇒ None | Some ctxclds ⇒
     ftype_in_path_f P ctxclds f)"
lemma [simp]: "(ftype P ty f ty') = (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

primrec
find_meth_def_in_list_f :: "meth_defs ⇒ meth ⇒ meth_def_opt"
where
"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 ⇒
  (case ms of meth_sig_def cl m' vds ⇒
  (if m = m' then Some md else find_meth_def_in_list_f mds m)))"
lemma [simp]: "(find_meth_def_in_list mds m md_opt) = (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

primrec
find_meth_def_in_path_f :: "ctxclds ⇒ meth ⇒ ctxmeth_def_opt"
where
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) ⇒
  (case find_meth_def_in_list_f (class_methods_f cld) m of
    Some md ⇒ Some (ctx, md) |
    None ⇒ find_meth_def_in_path_f ctxclds m))"
lemma [simp]: "(find_meth_def_in_path ctxclds m ctxmeth_def_opt) = (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

definition
find_meth_def_f :: "P ⇒ ty ⇒ meth ⇒ ctxmeth_def_opt"
where
"find_meth_def_f P ty m =
  (case find_path_ty_f P ty of None ⇒ None | Some ctxclds ⇒
    find_meth_def_in_path_f ctxclds m)"
lemma [simp]: "(find_meth_def P ty m ctxmd_opt) = (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

primrec
lift_opts :: "'a option list ⇒ 'a list option"
where
"lift_opts []         = Some []" |
"lift_opts (opt#opts) =
  (case opt of None ⇒ None | Some v ⇒
  (case lift_opts opts of None ⇒ None | Some vs ⇒ Some (v#vs)))"

definition
mtype_f :: "P ⇒ ty ⇒ meth ⇒ mty option"
where
"mtype_f P ty m =
  (case find_meth_def_f P ty m of None ⇒ None | Some (ctx, md) ⇒
  (case md of meth_def_def ms mb ⇒
  (case ms of meth_sig_def cl m' vds ⇒
  (case find_type_f P ctx cl of None ⇒ None | Some ty' ⇒
  (case lift_opts (map (λvd. case vd of vd_def clk vark ⇒
    find_type_f P ctx clk) vds) of None ⇒ None | Some tys ⇒
      Some (mty_def tys ty'))))))"

lemma lift_opts_ind[rule_format]:
  "(∀x∈set list. (λ(cl, var, ty). find_type_f P ctx cl = Some ty) x)
       ⟶ lift_opts (map (case_vd (λclk vark. find_type_f P ctx clk) ∘ (λ(cl, var, ty). vd_def cl var)) list) = Some (map (λ(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) ⟶ 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) ⟶ m' = m"
apply(induct path) apply(simp) apply(clarsimp split: option.splits) by(rule find_md_m_match')

lemma vds_map_length:
  "length (map (case_vd (λclk vark. find_type_f P ctx clk)) vds) = length vds"
by (induct vds, auto)

lemma lift_opts_length[rule_format]:
  "∀tys. lift_opts ty_opts = Some tys ⟶ 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 (case_vd (λclk vark. find_type_f P ctx clk)) vds) = Some tys ⟶ 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]:
  "∀tys. length vds = length tys ⟶ vds = map (λ(cl, var, ty). vd_def cl var) (map (λ(vd, ty). case vd of vd_def cl var ⇒ (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]:
  "∀vds. length vds = length tys ⟶ tys = map ((λ(cl, var, ty). ty) ∘ (λ(vd, ty). case vd of vd_def cl var ⇒ (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]:
  "∀tys. lift_opts (map (case_vd (λclk vark. find_type_f P ctx clk)) vds) = Some tys
      ⟶ (∀(vd, ty) ∈ set (zip vds tys). case vd of vd_def cl var ⇒ 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]: "(mtype P ty m mty) = (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 (λ(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 (λ(vd, ty). case vd of vd_def cl var ⇒ (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(frule vds_tys_length_eq') apply(clarsimp)
 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

definition
is_sty_one :: "P ⇒ ty ⇒ ty ⇒ bool option"
where
"is_sty_one P ty ty' =
  (case find_path_ty_f P ty of None ⇒ None | Some ctxclds ⇒
  (case ty' of ty_top ⇒ Some True | ty_def ctx' dcl' ⇒
    Some ((ctx', dcl') : set (map (λ(ctx, cld). (ctx, class_name_f cld)) ctxclds)) ))"

lemma class_name_mem_map[rule_format]:
"(ctx, cld, class_name_f cld) ∈ set ctx_cld_dcl_list
       ⟹ (ctx, class_name_f cld)
          ∈ ((λ(ctx, cld). (ctx, class_name_f cld)) ∘ (λ(ctx, cld, dcl). (ctx, cld))) `
            set ctx_cld_dcl_list"
by (induct ctx_cld_dcl_list, auto)

lemma map_map_three:
  " ctxclds = map ((λ(ctx, cld, dcl). (ctx, cld)) ∘ (λ(ctx, cld). (ctx, cld, class_name_f cld))) ctxclds"
by (induct ctxclds, auto)

lemma mem_el_map[rule_format]:
  "(ctx, dcl) ∈ set ctxclds
       ⟹ (ctx, class_name_f dcl)
          ∈ (λ(ctx_XXX, cld_XXX, y). (ctx_XXX, y)) `
            set (map (λ(ctx, cld). (ctx, cld, class_name_f cld)) ctxclds)"
by (induct ctxclds, auto)

lemma [simp]: "(sty_one P ty ty') = (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(rename_tac ctx cld dcl)
   apply(drule_tac x = "(ctx, cld, dcl)" in bspec, simp) apply(clarsimp)
  using case_prod_conv image_iff apply fastforce
apply(clarsimp simp add: is_sty_one_def split: option.splits ty.splits)
 apply(simp add: sty_objI)
apply(rename_tac ctxclds ctx dcl)
apply(rule_tac ctx_cld_dcl_list = "map (λ(ctx, cld). (ctx, cld, class_name_f cld)) ctxclds" in sty_dclI[simplified])
  apply(clarsimp) apply(rule map_map_three)
 apply(force)
apply(rule mem_el_map, assumption)
done

lemma path_append[rule_format]:
  "find_path_rec_f P ctx cl path' = Some path ⟹ ∃path''. path = path' @ path''"
apply(induct rule: find_path_rec_f.induct)
 apply(clarsimp)
apply(force split: if_split_asm option.splits)
done

lemma all_in_path_found'[rule_format]:
  "find_path_rec_f P ctx cl path' = Some path ⟶
      (∀ctxcld ∈ set path. ctxcld ∈ set path' ∨ (∃ctx' fqn'. find_cld_f P ctx' fqn' = Some ctxcld))"
apply(induct rule: find_path_rec_f.induct)
 apply(clarsimp)
apply(rule)
apply(force split: if_split_asm option.splits)
done

lemma all_in_path_found:
  "⟦find_path_f P ctx cl = Some path; ctxcld ∈ set path⟧ ⟹ ∃ctx' fqn'. find_cld_f P ctx' fqn' = Some ctxcld"
by (unfold find_path_f_def, simp only: all_in_path_found'[of _ _ _ "[]", simplified])

lemma fpr_target_is_head':
  "find_path_rec_f P ctx cl path' = Some path ⟶
     (∀fqn ctxcld. cl = cl_fqn fqn ∧ find_cld_f P ctx fqn = Some ctxcld ⟶
          (∃path''. path = path' @ ctxcld # path''))"
apply(induct_tac P ctx cl path' rule: find_path_rec_f.induct)
 apply(simp)
apply(clarsimp split: if_split_asm option.splits)
apply(case_tac "superclass_name_f b") apply(clarsimp)
apply(clarsimp split: if_split_asm option.splits)
apply(force)
done

lemma fpr_target_is_head:
  "find_path_f P ctx (cl_fqn fqn) = Some path ⟹ ∃ctxcld. find_cld_f P ctx fqn = Some ctxcld ∧ (∃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 ⟶
     (∀fqn ctxcld path'' path_fqn.
         cl = cl_fqn fqn ∧ find_cld_f P ctx fqn = Some ctxcld ∧
         find_path_rec_f P (fst ctxcld) (superclass_name_f (snd ctxcld)) path'' = Some path_fqn ⟶
              (∃path'''. path_fqn = path'' @ path''' ∧ path = path' @ ctxcld # path'''))"
apply(induct_tac P ctx cl path' rule: find_path_rec_f.induct)
 apply(simp)
apply(clarsimp split: if_split_asm option.splits)
apply(case_tac "superclass_name_f b") apply(simp add: find_path_f_def)
apply(clarsimp split: if_split_asm option.splits)
apply(frule_tac path = path in path_append) apply(clarsimp) apply(force)
done

lemma fpr_sub_path:
  "⟦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'⟧
       ⟹ path = ctxcld # path'"
by (unfold find_path_f_def, force intro: fpr_sub_path'[rule_format, of _ _ _ "[]" _ _ _ "[]", simplified])

lemma fpr_sub_path_simp:
  "⟦find_path_rec_f P ctx (superclass_name_f cld) path'' = Some path_fqn; find_cld_f P ctx fqn = Some (ctx, cld); acyclic_clds P;
    find_path_rec_f P ctx (superclass_name_f cld) (path' @ [(ctx, cld)]) = Some path⟧
       ⟹ ∃path'''. path_fqn = path'' @ path''' ∧ 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 if_split_asm)
done

lemma fpr_same_suffix'[rule_format]:
  "find_path_rec_f P ctx cl prefix = Some path ⟶
     (∀suffix prefix'. path = prefix @ suffix ⟶
          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(force)
done

lemma fpr_same_suffix:
  "find_path_rec_f P ctx cl prefix = Some path ⟶
     (∀suffix prefix' suffix'. path = prefix @ suffix ∧
          find_path_rec_f P ctx cl prefix' = Some (prefix' @ suffix')
             ⟶ suffix = suffix')"
apply(induct_tac P ctx cl prefix rule: find_path_rec_f.induct)
 apply(clarsimp)
by (metis fpr_same_suffix' option.inject same_append_eq)

lemma fpr_mid_path'[rule_format]:
  "find_path_rec_f P ctx cl path' = Some path ⟶
     (∀ctxcld ∈ set path.
         ctxcld ∈ set path' ∨
         (∀path_fqn. find_path_rec_f P (fst ctxcld) (cl_fqn (fqn_def (class_name_f (snd ctxcld)))) path'' = Some path_fqn ⟶
              (∀path'''. path_fqn = path'' @ path''' ⟶ (∃path_rest. path = path_rest @ path'''))))"
supply [[simproc del: defined_all]]
apply(induct_tac P ctx cl path' rule: find_path_rec_f.induct)
 apply(simp)
apply(clarsimp split: option.splits)
apply(frule find_cld_name_eq) apply(clarsimp)
apply(rename_tac path' ctx' cld' cld'' ctx'' path''' cl fds mds)
apply(subgoal_tac "find_path_rec_f P ctx' (superclass_name_f cld') (path' @ [(ctx', cld')]) = Some path ⟶
              (∀ctxcld∈set path.
                  ctxcld = (ctx', cld') ∨
                  ctxcld ∈ set path' ∨
                  (∀path_fqn. case_option None (case_prod (λctx' cld. find_path_rec_f P ctx' (superclass_name_f cld) (path'' @ [(ctx', cld)])))
                               (find_cld_f P (fst ctxcld) (fqn_def (class_name_f (snd ctxcld)))) =
                              Some path_fqn ⟶
                              (∀path'''. path_fqn = path'' @ path''' ⟶ (∃path_rest. path = path_rest @ path'''))))")
 apply(erule impE) apply simp
 apply(drule_tac x = "(ctx'', cld'')" in bspec, simp) apply(clarsimp)
 apply(simp add: superclass_name_f_def)
 apply(case_tac cld') apply(rename_tac dcl' cl' fds' mds') apply(clarsimp simp add: class_name_f_def)
 apply(case_tac fqn) apply(rename_tac dcl'') apply(clarsimp)
 apply(frule find_cld_name_eq) apply(clarsimp)
 apply(frule path_append) apply(frule_tac path = "path'' @ path'''" in path_append) apply(clarsimp)
 apply(rule_tac x = path' in exI) apply(clarsimp)
 apply(frule_tac suffix = path''a and prefix' = "path'' @ [(ctx', cld_def dcl' cl' fds' mds')]" and
                suffix' = path''aa in fpr_same_suffix[rule_format]) apply(simp)
 apply(force)
apply(simp)
done

lemma fpr_mid_path:
  "⟦find_path_f P ctx cl = Some path; (ctx', cld') ∈ set path;
    find_path_f P ctx' (cl_fqn (fqn_def (class_name_f cld'))) = Some path'⟧
       ⟹ ∃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 ⟶
      (∀fqn ctxcld. cl = cl_fqn fqn ∧ find_cld_f P ctx fqn = Some ctxcld ⟶ ctxcld ∈ set path)"
apply(case_tac cl)
 apply(simp)
apply(clarsimp) apply(drule path_append) apply(force)
done

lemma fpr_first_in_path:
  "⟦find_path_f P ctx (cl_fqn fqn) = Some path; find_cld_f P ctx fqn = Some ctxcld⟧ ⟹ ctxcld ∈ 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 ⟹ ∃ctxcld. find_cld_f P ctx fqn = Some ctxcld"
apply(unfold find_path_f_def) apply(clarsimp split: if_split_asm option.splits) done

lemma ctx_cld_ctx_dcl[rule_format]:
  "(ctx, cld_def dcl cl fds mds) ∈ set path ⟶ (ctx, dcl) ∈ (λ(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) ∈ (λ(ctx, cld). (ctx, class_name_f cld)) ` set path ⟶ (∃cl fds mds. (ctx, cld_def dcl cl fds mds) ∈ set path)"
apply(induct path) apply(simp)
apply(auto) apply(case_tac b) apply(force simp add: class_name_f_def)
done

lemma ctx_dcl_mem_path:
  "find_path_f P ctx (cl_fqn (fqn_def dcl)) = Some path ⟹ (ctx, dcl) ∈ (λ(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)
done

lemma sty_reflexiveI:
  "is_sty_one P ty ty' = Some True ⟹ is_sty_one P ty ty = Some True"
apply(simp add: is_sty_one_def split: option.splits) apply(case_tac ty) apply(simp) apply(clarsimp)
apply(drule ctx_dcl_mem_path) apply(force)
done

lemma sty_transitiveI:
  "⟦is_sty_one P ty ty' = Some True; is_sty_one P ty' ty'' = Some True⟧
       ⟹ is_sty_one P ty ty'' = Some True"
apply(clarsimp simp add: is_sty_one_def split: ty.splits option.splits)
apply(rename_tac path ctx dcl path' ctx' dcl')
apply(case_tac ty) apply(simp) apply(clarsimp) apply(rename_tac ctx dcl ctx' cld' ctx'' cld'')
apply(frule fpr_mid_path) apply(simp) apply(simp) apply(force)
done

definition
is_sty_many :: "P ⇒ tys ⇒ tys ⇒ bool option"
where
"is_sty_many P tys tys' =
  (if length tys ≠ length tys' then None else
  (case lift_opts (map (λ(ty, ty'). is_sty_one P ty ty') (zip tys tys'))
     of None ⇒ None | Some bools ⇒ Some (list_all id bools)))"

lemma lift_opts_exists:
  "∀x∈set ty_ty'_list. (λ(ty, ty'). is_sty_one P ty ty' = Some True) x ⟹ ∃bools. lift_opts (map (λ(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]:
  "∀bools. (∀x∈set ty_ty'_list. (λ(ty, ty'). is_sty_one P ty ty' = Some True) x) ∧
            lift_opts (map (λ(ty, ty'). is_sty_one P ty ty') ty_ty'_list) = Some bools
                  ⟶ list_all id bools"
by (induct ty_ty'_list, auto split: option.splits)

lemma tys_tys'_list: "⋀bools ty ty'. ⟦lift_opts (map (λ(x, y). is_sty_one P x y) tys_tys'_list) = Some bools; length tys = length tys'; list_all id bools; (ty, ty') ∈ set tys_tys'_list⟧ ⟹ is_sty_one P ty ty' = Some True"
apply(induct tys_tys'_list)
 apply(simp)
apply(clarsimp split: option.splits)
by force

lemma [simp]: "(sty_many P tys tys') = (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 if_split_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(simp add: tys_tys'_list)
done

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

definition
tr_x :: "T ⇒ x ⇒ x"
where
"tr_x T x = (case T x of None ⇒ x | Some x' ⇒ x')"

definition
tr_var :: "T ⇒ var ⇒ var"
where
"tr_var T var = (case tr_x T (x_var var) of x_this ⇒ var | x_var var' ⇒ var')"

primrec
tr_s_f  :: "T ⇒ s ⇒ s" and
tr_ss_f :: "T ⇒ s list ⇒ s list"
where
"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]: "(∀x∈set s_s'_list. case x of (s_XXX, s_') ⇒ tr_s T s_XXX s_' ∧ tr_s_f T s_XXX = s_') ⟶
       tr_ss_f T (map fst s_s'_list) = map snd s_s'_list"
by (induct s_s'_list, auto)

lemma [simp]: "(∀x∈set y_y'_list. case_prod (λy_XXX. (=) (case T y_XXX of None ⇒ y_XXX | Some x' ⇒ x')) x) ⟶ 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 set_zip_tr[simp]: "(s, s') ∈ set (zip ss (tr_ss_f T ss)) ⟶ 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_ss_map:
  "tr_ss_f T (map fst s_s'_list) = map snd s_s'_list ∧ (∀x∈set s_s'_list. case_prod (tr_s T) x) ∧
   (a, b) ∈ set s_s'_list ⟶ tr_s T a (tr_s_f T a)"
apply(induct s_s'_list) by auto

lemma tr_f_to_rel: "∀s'. tr_s_f T s = s' ⟶ tr_s T s s'"
apply(induct s rule: tr_s_f.induct)
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.simps) apply(rule tr_s_ifI)
apply(simp only: tr_x_def) apply(simp only: tr_x_def) apply(simp) apply(simp)
apply(clarsimp) apply(rule tr_s_newI)
apply(clarsimp simp add: tr_x_def tr_var_def split: option.splits)
apply(clarsimp)
apply(rename_tac var x m ys)
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(simp)
apply(cut_tac T = T and s_s'_list = "[]" in tr_s_blockI[simplified])
 apply(simp)
apply(clarsimp)
apply(clarsimp) apply(rename_tac s ss)
apply(cut_tac T = T and s_s'_list = "zip (s # ss) (tr_s_f T s # tr_ss_f T ss)" in tr_s_blockI[simplified])
 apply(clarsimp) apply(rename_tac x x')
 apply(frule set_zip_tr[THEN mp]) apply(clarsimp)
 apply(erule in_set_zipE)
 apply(erule_tac ?a1.0="T" and ?a2.0="s_block ss" and ?a3.0="s_block (tr_ss_f T ss)" in tr_s.cases)
 apply(clarsimp)
 apply(rule tr_ss_map[THEN mp], force)
 apply(clarsimp)+
done

lemma tr_rel_f_eq: "((tr_s T s s') = (tr_s_f T s = s'))"
apply(rule)
 apply(erule tr_s.induct)
 apply(force 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