Theory identityEnvironment_lemmas

(*  Title:      Certificate Safe to SVM
    Author:     Javier de Dios and Ricardo Peña
    Copyright:  October 2008, Universidad Complutense de Madrid
*)



header {* Certification of the translation CoreSafe to SVM. identityEnvironment property *}

theory identityEnvironment_lemmas
imports Main "../CoreSafe/SafeRASemantics" SVMSemantics CoreSafeToSVM CertifSafeToSVM_definitions
                                           basic_properties

begin


(* Lemmas for identityEnvironment *)

fun addEnv_good :: "Env => (string ×  nat) list => bool" where
 "addEnv_good rho xs = (∀ x ∈ set (map fst xs). x ∉ domRho rho)"

declare identityEnvironment.simps [simp del]
declare envAdd.simps [simp del]
declare envSearch.simps [simp del]
declare decreasing.simps [simp del]
declare addEnv_good.simps [simp del]
declare rho_good.simps [simp del]
declare rho_good'.simps [simp del]

lemma length_decreasing_leq_length:
  "length xs ≤ length (decreasing (length xs))"
apply (induct xs, simp, clarsimp)
by (subst decreasing.simps,simp)


lemma length_decreasing_eq_length:
  "(length (decreasing (length xs))) = length xs"
apply (induct xs, simp)
by (subst decreasing.simps, simp)+

lemma rho_good_addEnv [rule_format]:
  "length rho > 0 --> rho_good rho 
   --> rho_good ( rho + zip xs (decreasing (length xs)))"
apply (induct xs, simp)
 apply (case_tac rho, simp, clarsimp)
 apply (rename_tac delta m l ret)
 apply (simp add: envAdd.simps add: rho_good.simps) 
apply clarsimp
apply (case_tac rho, simp)
apply (rename_tac x xs delta rest)
apply (subst decreasing.simps, simp)
apply (simp add: envAdd.simps, clarsimp)
apply (rename_tac delta m n rest)
apply (simp add: Let_def add: rho_good.simps)  
apply (simp add: rho_good'.simps)
apply (rule conjI, rule length_decreasing_leq_length)
apply (rule ballI, rule conjI, rule impI, rule length_decreasing_leq_length)
apply (rule impI, erule conjE)
apply (erule_tac x="xa" in ballE) apply simp
apply simp
done


lemma envSearch'_monotone [rule_format]:
  "rho_good' rho --> x∈ domRho rho 
  --> envSearch' rho x (Suc l) = Suc (envSearch' rho x l)"
apply (induct rho arbitrary: l, simp, auto)
apply (simp add: rho_good'.simps, erule conjE)
apply (case_tac rho) apply simp 
apply (erule_tac x="x" in ballE) apply (elim conjE) apply simp 
apply (simp add: dom_def)

apply clarsimp
apply (rename_tac delta m n l l' delta' m' n' rest)
apply (unfold rho_good'.simps, erule conjE) 
apply (erule_tac x="x" in ballE) apply (elim conjE) apply simp
apply (simp add: dom_def)
apply clarsimp
apply (rename_tac delta m n rho l)
apply (case_tac "delta x", simp) apply simp 
apply (erule_tac x="x" in ballE, simp) apply (elim conjE)
apply simp
by (simp add: dom_def)

lemma envSearch'_monotone_Suc [rule_format]:
  "rho_good' rho --> x∈ domRho rho 
  --> envSearch' rho x (Suc (Suc l)) = Suc (Suc (envSearch' rho x l))"
apply (induct rho arbitrary: l, simp, auto)
apply (simp add: rho_good'.simps, erule conjE)
apply (case_tac rho) apply simp 
apply (erule_tac x="x" in ballE) apply (elim conjE) apply simp 
apply (simp add: dom_def)

apply clarsimp
apply (rename_tac delta m n l l' delta' m' n' rest)
apply (unfold rho_good'.simps, erule conjE) 
apply (erule_tac x="x" in ballE) apply (elim conjE) apply simp
apply (simp add: dom_def)
apply clarsimp
apply (rename_tac delta m n rho l)
apply (case_tac "delta x", simp) apply simp 
apply (erule_tac x="x" in ballE, simp) apply (elim conjE)
apply simp
by (simp add: dom_def)


lemma envAdd_monotone_dom:
  "[|x ≠ x1; x ∈ domRho (rho + [(x1, 1)]); length rho > 0|]
  ==> x ∈ domRho rho"
apply (simp)
apply (case_tac rho) apply simp
apply (simp add: envAdd.simps add: envSearch.simps, clarsimp)
done


lemma domRho_addEnv_aux [rule_format]:
   "x ∉ set xs -->  distinct xs --> i < length xs -->  xs ! i ∈ domRho (rho + zip (x # xs) (decreasing (Suc (length xs))))
   --> xs ! i ∈ domRho (rho + zip xs (decreasing (length xs)))"
apply (clarsimp, case_tac rho, simp)
apply (simp add: envAdd.simps)
apply (clarsimp, rename_tac delta m l rest)
apply (simp add: envAdd.simps add: Let_def)
apply (erule disjE, rule disjI1, simp)
 apply (subgoal_tac 
   "(zip (x # xs) (decreasing (Suc (length xs)))) =  
   ((x,Suc (length xs)) # zip xs (decreasing (length xs)))",simp)
  apply (erule disjE, clarsimp, simp)
 apply (subst decreasing.simps, simp)
by simp


lemma addEnv_good_aux [rule_format]:
   "x ∉ set xs -->  distinct xs --> addEnv_good rho (zip (x # xs) (decreasing (Suc (length xs))))
   --> addEnv_good rho (zip xs (decreasing (length xs)))"
apply (case_tac rho, simp)
 apply (simp add: addEnv_good.simps)
apply (clarsimp, rename_tac delta m l rest)
apply (simp add: addEnv_good.simps)
apply (subgoal_tac 
  "(zip (x # xs) (decreasing (Suc (length xs)))) =  
   ((x,Suc (length xs)) # zip xs (decreasing (length xs)))")
apply (rule ballI)
 apply (erule_tac x="xa" in ballE, clarsimp, clarsimp)
by (subst decreasing.simps, simp)


lemma z_in_domRho_addEnv [rule_format]:
 "length rho > 0 -->  distinct xs --> i < length xs --> xs!i ∈ domRho (rho + zip xs (decreasing (length xs))) --> rho_good rho
  --> addEnv_good rho  (zip xs (decreasing (length xs))) 
  -->  (rho + zip xs (decreasing (length xs)))  |> (xs ! i) = i"
apply (induct xs i rule: list_induct3, simp_all)

apply (clarsimp, subst decreasing.simps, simp, simp add: envAdd.simps)
apply (case_tac rho, simp, clarsimp)
apply (simp add: Let_def)
apply (rename_tac x xs delta m rest)
apply (simp add: envSearch.simps)

apply clarsimp
apply (subgoal_tac "xs ! i ∈ domRho (rho + zip xs (decreasing (length xs)))",simp)
 prefer 2 apply (rule domRho_addEnv_aux, assumption+)
apply (subgoal_tac "addEnv_good rho (zip xs (decreasing (length xs)))",simp) 
 prefer 2 apply (rule addEnv_good_aux, assumption+)
apply (case_tac "xs=[]",simp)
apply (subgoal_tac "length rho > 0") prefer 2 apply simp
apply (frule_tac xs="xs" in rho_good_addEnv,assumption)
apply (case_tac rho, simp)
apply (rename_tac tup rest, clarsimp) 
apply (rename_tac delta m n rest)
apply (subst decreasing.simps, simp)
apply (simp add: envAdd.simps add: Let_def add: envSearch.simps)
apply (rule conjI, clarsimp, rule impI)
apply (case_tac "((delta ++ map_of (map (λ(x, j). (x, m + j)) (zip xs (decreasing (length xs))))) (xs ! i))")
 apply (rule_tac s="None" in ssubst,assumption, clarsimp)
 apply (erule disjE)+ apply (simp add: dom_def)
 apply (erule disjE)+ apply (simp add: dom_def)
  apply (unfold rho_good.simps, simp) apply (elim conjE)
  apply (unfold rho_good'.simps, simp) apply (elim conjE)
  apply (subst envSearch'_monotone, simp, assumption+, simp)
 apply (erule disjE)+ apply (simp add: dom_def)
  apply (subst envSearch'_monotone, simp, assumption+, simp)
 apply (erule disjE)+ apply (simp add: dom_def)
  apply (subst envSearch'_monotone, simp, assumption+, simp)
 apply (erule disjE)+ apply (simp add: dom_def)
  apply (subst envSearch'_monotone, simp, assumption+, simp)
apply (rename_tac l)
apply (rule_tac s="Some l" in ssubst,assumption, simp)
apply (subgoal_tac "(length (decreasing (length xs))) = length xs",simp)
 prefer 2 apply (rule length_decreasing_eq_length)
apply (elim conjE, erule_tac x="xs!i" in ballE) 
 apply (elim conjE) 
 apply (erule_tac x="xs!i" in ballE) 
  apply (elim conjE,simp) 
 apply (simp, elim conjE, simp add: addEnv_good.simps)
apply (subgoal_tac "xs ! i ∈  dom (map_of (map (λ(x, j). (x, m + j)) (zip xs (decreasing (length xs)))))",simp)
 apply (erule_tac x="xs!i" in ballE) 
  apply (elim conjE,simp)
 apply simp
by clarsimp


lemma z_in_domRho [rule_format]:
 " length rho > 0 -->  z ∉ set xs --> distinct xs -->  z ∈ domRho rho --> rho_good rho 
  --> addEnv_good rho  (zip xs (decreasing (length xs)))
  --> (rho + zip xs (decreasing (length xs)))  |> z = (rho |> z) + length xs"
apply (induct xs, simp_all)

apply (clarsimp, simp add: envAdd.simps)
apply (case_tac rho, simp, clarsimp)
apply (simp add: envSearch.simps)

apply clarsimp
apply (subgoal_tac "addEnv_good rho (zip xs (decreasing (length xs)))",simp)
 prefer 2 apply (rule_tac x="a" in addEnv_good_aux, assumption+)
apply (case_tac "xs=[]",simp) 
 apply (subgoal_tac "length rho > 0") prefer 2 apply simp
 apply (frule_tac xs="xs" in rho_good_addEnv,assumption)
 apply (case_tac rho, simp)
 apply (rename_tac tup rest, clarsimp, rename_tac delta m n rest)
 apply (subst decreasing.simps, simp, simp add: envAdd.simps)
 apply (simp add: Let_def add: envSearch.simps)
 apply (erule disjE)
  apply (case_tac "delta z",simp) 
   apply (simp add: dom_def)
  apply (simp, unfold rho_good.simps, simp, elim conjE)
  apply (simp, unfold rho_good'.simps)
  apply (elim conjE, erule_tac x="z" in ballE) 
   apply (elim conjE) apply simp
  apply (simp add: dom_def)
 apply clarsimp
 apply (case_tac "delta z",simp)
  apply (subst envSearch'_monotone, simp, assumption+, simp)
 apply clarsimp
 apply (erule_tac x="z" in ballE) 
  apply (erule_tac x="z" in ballE, clarsimp)
   apply arith
  apply (simp add: dom_def)
 apply (simp add: dom_def)
apply (rename_tac x xs)
apply (subgoal_tac "length rho > 0") prefer 2 apply simp
apply (frule_tac xs="xs" in rho_good_addEnv,assumption)
apply (case_tac rho, simp)
apply (rename_tac tup rest, clarsimp, rename_tac delta m n rest)
apply (subst decreasing.simps, simp)
apply (simp add: envAdd.simps add: Let_def add: envSearch.simps)
apply (case_tac "((delta ++ map_of (map (λ(x, j). (x, m + j)) (zip xs (decreasing (length xs))))) z)")
 apply (rule_tac s="None" in ssubst,assumption, clarsimp)
 apply (erule disjE)+ apply (simp add: dom_def) 
 apply (unfold rho_good.simps,simp, elim conjE)
 apply (unfold rho_good'.simps)
 apply (subst envSearch'_monotone,simp, assumption+, simp)

apply (rename_tac l,clarsimp)
apply (drule_tac s="m + min (length xs) (length (decreasing (length xs))) - l" in sym, simp)
apply (erule_tac x="z" and
                 A="dom (map_of (map (λ(x, j). (x, m + j)) (zip xs (decreasing (length xs))))) ∪ dom delta" in ballE)
 apply (elim conjE)
 apply (erule_tac P="map_of (map (λ(x, j). (x, m + j)) (zip xs (decreasing (length xs)))) z = Some l" in disjE,simp)
 apply clarsimp
 apply (subgoal_tac "(delta ++ map_of (map (λ(x, j). (x, m + j)) (zip xs (decreasing (length xs))))) z = Some l",simp)
 apply (simp add: map_add_def)
by clarsimp

lemma stackobject_nth [rule_format]:
"length vs > 0 --> i < length vs --> ((map Val vs) @  S) ! i = Val (vs!i)"
apply (induct vs i rule: list_induct3, simp_all)
by clarsimp

lemma stackobject_nth_plus [rule_format]:
"length vs > 0 --> i < length vs --> ((map Val vs) @  S) !+ i = Val (vs!i)"
apply (induct vs i rule: list_induct3, simp_all)
by clarsimp


lemma stackobject_envSearch [rule_format]:
  "length vs > 0 -->  (map Val vs @  S) ! ((rho |> z) + length vs) = S ! rho |> z"
apply (induct vs, simp_all)
by (case_tac "vs=[]", simp, simp)

lemma stackobject_envSearch_plus [rule_format]:
  "length vs > 0 -->  (map Val vs @  S) !+ (((rho |> z) + length vs)) = S !+ (rho |> z)"
apply (induct vs, simp_all)
by (case_tac "vs=[]", simp, simp)


lemma extend_nth [rule_format]:
  "length xs > 0 -->  length xs = length vs --> distinct xs --> i < length xs
   --> extend E1 xs vs (xs ! i) = Some (vs ! i)"
apply (induct xs vs arbitrary: i rule: list_induct2', simp_all) 
apply (case_tac "xs=[]", simp)
apply (simp add: extend_def, clarsimp)
apply (case_tac i, simp)
 apply (simp add: extend_def)
apply (simp)
apply (simp add: extend_def)
by (rule impI,clarsimp) 


lemma extend_nth_the [rule_format]:
  "length xs > 0 -->  length xs = length vs --> distinct xs --> i < length xs
   --> the (extend E1 xs vs (xs ! i)) = (vs ! i)"
apply (induct xs vs arbitrary: i rule: list_induct2', simp_all) 
apply (case_tac "xs=[]", simp)
apply (simp add: extend_def, clarsimp)
apply (case_tac i, simp)
 apply (simp add: extend_def)
apply (simp)
apply (simp add: extend_def)
by (rule impI,clarsimp) 

lemma not_in_extend: " z ∉ set xs ==> E1 z = extend E1 xs vs z"
apply (induct xs vs rule: list_induct2')
by (simp, simp add: extend_def)+

lemma dom_decreasing:
  "[|  length xs = length vs|]  
   ==> dom (map_of (map (λ(x, j). (x, m + j)) (zip xs (decreasing (length vs))))) = set xs"
apply (induct xs vs rule:list_induct2', simp_all)
by (simp add: decreasing.simps)

lemma domRho_case: 
 "[| length rho > 0; domRho rho = dom E1 ∪ dom E2 - {self}; ∀ x ∈ set xs. x≠ self; length xs = length vs; distinct xs |] 
       ==> domRho (rho + zip xs (decreasing (length vs))) = dom (extend E1 xs vs) ∪ dom E2 - {self}"
apply (unfold envAdd.simps)
apply (case_tac rho) apply (simp)
apply (clarsimp) 
apply (simp add: Let_def) 
apply (simp add: extend_def)
apply (subgoal_tac "dom (map_of (map (λ(x, j). (x, aa + j)) (zip xs (decreasing (length vs))))) = set xs")
apply (subgoal_tac "dom (map_of (zip xs vs)) = set xs")
apply simp apply blast apply simp
by (rule dom_decreasing,assumption)

lemma envAdd_list_monotone_dom:
  "[|x ∉ set xs; x ∈ domRho (rho + zip xs (decreasing (length xs))); length rho > 0|]
  ==> x ∈ domRho rho"
apply (case_tac rho, simp)
apply (simp add: envAdd.simps, clarsimp, simp add: Let_def)
apply (erule disjE)
 apply (subgoal_tac "length (decreasing (length xs)) = length xs")
  apply (drule_tac t="length xs" in sym)
  apply (frule_tac m="aa" in dom_decreasing, simp)
 apply (rule length_decreasing_eq_length)
by (simp add: dom_def)

lemma set_conv_nth_not: "∀i<length xs. z ≠ xs ! i ==> z ∉ set xs"
by (auto simp:set_conv_nth)


lemma envPlusPlus_rho_suc_rho [rule_format]:
   "length rho > 0 -->  rho_good rho --> x∈ domRho rho -->  rho ++ |> x = rho |> x + 2"
apply (induct rho,simp,clarsimp)
apply (rename_tac delta m n rho)
apply (simp add: envPlusPlus.simps add: envSearch.simps add: rho_good.simps, elim conjE, simp add: rho_good'.simps, auto)
apply (erule_tac x="x" in ballE, erule conjE, simp, simp add: dom_def)+
apply (case_tac "delta x",simp)
apply (case_tac rho,simp)
apply (rule envSearch'_monotone_Suc, simp, assumption+)
apply (erule_tac x="x" in ballE,simp, arith)
apply (simp add: dom_def)
apply (case_tac "delta x",simp)
apply (case_tac rho,simp)
apply (rule envSearch'_monotone_Suc, simp, assumption+) 
apply (erule_tac x="x" in ballE,simp, arith)
by (simp add: dom_def)


lemma envPlusPlus_monotone_dom:
  "length rho > 0 ==> domRho rho =  domRho (rho ++)"
by (simp, case_tac rho,simp,clarsimp)

lemma envAdd_rho_suc_rho [rule_format]:
  "length rho > 0 -->  rho_good rho --> x≠x1 --> x∈ domRho rho -->  (rho + [(x1, 1)]) |> x = (rho |> x) + 1"
apply (induct rho,simp,clarsimp)
apply (rename_tac delta m n rho)
apply (simp add: envAdd.simps add: envSearch.simps add: rho_good.simps, elim conjE, simp add: rho_good'.simps, auto)
apply (erule_tac x="x" in ballE, erule conjE, simp, simp add: dom_def)+
apply (case_tac "delta x",simp)
apply (case_tac rho,simp)
apply (rule envSearch'_monotone, simp, assumption+) 
apply (erule_tac x="x" in ballE,simp, arith)
apply (simp add: dom_def)
apply (case_tac "delta x",simp)
apply (case_tac rho,simp)
apply (rule envSearch'_monotone, simp, assumption+) 
apply (erule_tac x="x" in ballE,simp, arith)
by (simp add: dom_def)


lemma identityEnvironment_e1:
  "[| length rho > 0; (E1,E2) \<Join> (rho,S); rho_good rho;  self ∈ dom (snd (E1, E2)); dom E1 ∩ dom E2 = {} |]
  ==> (E1,E2) \<Join> (rho++,Cont (k0, q2) # S)" 
apply (subgoal_tac "self ∉ dom E1")
 prefer 2 apply simp apply blast
apply (unfold identityEnvironment.simps)
apply (elim conjE)
apply (subgoal_tac "domRho rho =  domRho (rho ++)")
 apply (rule conjI, simp)
 apply (rule conjI)
  apply (rule ballI)
  apply (erule_tac x="x" in ballE)
  apply (subgoal_tac "x∈ domRho rho") 
   apply (frule envPlusPlus_rho_suc_rho)  apply simp apply simp apply simp apply blast 
 apply (simp add: dom_def)
  apply (rule ballI)
  apply (erule_tac x="r" and A="dom E2 - {self}" in ballE)
  apply (subgoal_tac "r∈ domRho rho") 
   apply (frule envPlusPlus_rho_suc_rho)  apply simp apply simp apply simp apply blast 
 apply (simp add: dom_def)
by (erule envPlusPlus_monotone_dom)


lemma identityEnvironment_e2:
  "[|(E1,E2) \<Join> (rho,S); length rho > 0; x1 ∉ dom E1;  x1 ≠ self; rho_good rho;
    self ∈ dom E2; dom (E1(x1 \<mapsto> v1)) ∩ dom E2 = {}; boundVar (Let x1 = ConstrE C as r a' In e2 a) ∩ dom E2 = {}|] 
  ==> (E1(x1 \<mapsto> v1), E2) \<Join> (rho + [(x1, 1)],Val v1 # S)"
apply (subgoal_tac "dom E1 ∩ dom E2 = {}")
 prefer 2 apply simp
apply (unfold identityEnvironment.simps)
apply (elim conjE)
 apply (rule conjI)
prefer 2
 apply (rule conjI)
 apply (rule ballI)
apply (erule_tac x="x" in ballE)
apply (case_tac "x=x1") 
 apply (subgoal_tac "(Val v1 # S) !+ ((rho + [(x1, 1)])  |> x1) = (Val v1 # S) ! 0") 
 apply (subgoal_tac "(Val v1 # S) ! 0 = Val v1") 
  apply (simp, simp, simp add: envAdd.simps add: envSearch.simps, induct rho, simp, clarsimp)  
(* x ≠ x1 *)
apply (subgoal_tac "(Val v1 # S) !+ ((rho + [(x1, 1)]) |> x) = (Val v1 # S) !+ ((rho |> x) + 1)") 
 prefer 2 apply (frule_tac x="x" in envAdd_rho_suc_rho,assumption+)
apply (subgoal_tac "∀ x ∈ dom E1. x ≠ self")
 prefer 2 apply blast apply simp apply blast
 apply simp 
apply (subgoal_tac "(Val v1 # S) !+ (((rho |> x) + 1)) = S !+ (rho |> x)") 
 prefer 2 apply (induct rho,simp,simp)
apply (case_tac " S !+ (rho |> x)")
 apply (simp,simp,simp)
apply (case_tac "x=x1") 
 apply (subgoal_tac "(Val v1 # S) !+ ((rho + [(x1, 1)])  |> x1) = (Val v1 # S) ! 0") 
 apply (subgoal_tac "(Val v1 # S) ! 0 = Val v1") 
  apply (simp, simp, simp add: envAdd.simps add: envSearch.simps, induct rho, simp, clarsimp)
 apply (subgoal_tac "x ∉  domRho (rho + [(x1, 1)]) ") 
prefer 2 apply (simp add: envAdd.simps add: envSearch.simps, induct rho, simp, clarsimp)
apply simp

 apply (rule ballI)
apply (erule_tac x="r" and A="dom E2 - {self}" in ballE)
apply (subgoal_tac "r≠x1")
apply (subgoal_tac "r ∈ domRho rho") 
apply (subgoal_tac "length rho > 0")
apply (subgoal_tac "(Val v1 # S) !+ ((rho + [(x1, 1)]) |> r) = (Val v1 # S) !+ ((rho |> r) + 1)") 
 prefer 2 thm envAdd_rho_suc_rho apply (frule_tac x="r" in envAdd_rho_suc_rho,assumption+) 
 apply simp 
apply (subgoal_tac "(Val v1 # S) !+ (((rho |> r) + 1)) = S !+ (rho |> r)") 
 prefer 2 apply (induct rho,simp,simp)
apply (case_tac " S !+ (rho |> r)")
 apply (simp,simp,simp) apply simp apply blast apply blast apply simp
apply (unfold envAdd.simps)
by (case_tac rho, simp, clarsimp, blast)



lemma identityEnvironment_e2_let2:
  "[|(E1,E2) \<Join> (rho,S); length rho > 0; x1 ∉ dom E1;  x1 ≠ self; rho_good rho;
    self ∈ dom E2; dom (E1(x1 \<mapsto> Loc pa)) ∩ dom E2 = {};  boundVar (Let x1 = ConstrE C as r a' In e2 a) ∩ dom E2 = {}|] 
  ==> (E1(x1 \<mapsto> Loc pa), E2) \<Join> ( rho + [(x1, 1)] ,  Val (Loc pa) # S)"
by (rule identityEnvironment_e2,assumption+)

lemma addEnv_empty [rule_format]:
  " length rho > 0 --> rho_good rho --> rho + [] = rho"
apply (induct rho,simp,clarsimp)
apply (case_tac rho,clarsimp)
 apply (simp add: envAdd.simps add: rho_good.simps)
apply clarsimp
by (simp add: envAdd.simps add: rho_good.simps) 


lemma addEnv_dom_empty [rule_format]:
  " length rho > 0 --> domRho (rho + []) = domRho rho"
apply (induct rho,simp,simp)
apply (case_tac rho, simp)
apply (simp add: envAdd.simps,clarsimp)
by (simp add: envAdd.simps,clarsimp)

lemma extend_empty:
  "extend E1 [] [] = E1"
by (simp add: extend_def)


lemma qq3 [rule_format]:
  "i < length xs 
   --> length rho > 0
   --> xs!i ∈ domRho (rho + zip xs (decreasing (length xs)))" 
apply (induct xs i rule: list_induct3, simp_all)
 apply (case_tac rho,simp,clarsimp)
 apply (rename_tac delta m l ret)
 apply (simp add: envAdd.simps add: rho_good.simps) 
 apply (simp add: Let_def)
 apply (subst decreasing.simps, simp,clarsimp)
apply (case_tac rho,simp,clarsimp)
apply (rename_tac delta m l ret)
apply (simp add: envAdd.simps add: rho_good.simps) 
apply (simp add: Let_def)
by (subst decreasing.simps, simp)

lemma pattern_extend_case_good [rule_format]:
  "i < length alts 
   --> alts!i = (pati, ei) 
   --> pati = ConstrP C ps ms 
   --> xs = map pat2var ps
   --> boundVar (Case (VarE x a) Of alts a') ∩ dom E2 = {} 
   --> set xs ∩ dom E2 = {}"
apply (induct alts arbitrary: i,simp,simp)
by (case_tac i,clarsimp,auto)

lemma pattern_extend_cased_good [rule_format]:
  "i < length alts 
   --> alts!i = (pati, ei) 
   --> pati = ConstrP C ps ms 
   --> xs = map pat2var ps
   --> boundVar (CaseD (VarE x a) Of alts a') ∩ dom E2 = {} 
   --> set xs ∩ dom E2 = {}"
apply (induct alts arbitrary: i,simp,simp)
by (case_tac i,clarsimp,auto)

lemma identityEnvironment_case_aux:
  "[|length rho > 0; 
   nr = int (length vs);  rho_good rho;
   addEnv_good rho (zip xs (decreasing (length xs)));
   (E1, E2) \<Join> (rho,S); def_extend E1 xs vs;
   self ∈ dom E2;  dom E1 ∩ dom E2 = {};
   set xs ∩ dom E2 = {}|]
   ==>  (extend E1 xs vs, E2) \<Join> ( rho + zip xs (decreasing (length xs)) , map Val vs @ S)"
apply (unfold def_extend_def, elim conjE)
apply (case_tac "xs=[]")
 apply simp
  apply (simp add: extend_def, subst addEnv_empty,simp,assumption,simp)
apply (unfold identityEnvironment.simps)
apply (elim conjE)
apply (rule conjI) 
 apply (clarsimp, rule sym)
 apply (rule domRho_case, simp, rule sym, simp, assumption+) 

apply (rule conjI)
apply (rule ballI) apply (rename_tac z)
apply (erule_tac x="z" in ballE)
 apply (case_tac "∃ i<length xs. z = xs!i")
  apply (erule exE, erule conjE)
  apply (subgoal_tac "length rho > 0") prefer 2 apply simp 
  apply (frule_tac i="i" in z_in_domRho_addEnv,assumption+,simp)
  apply (drule sym [where t="length vs"]) apply simp
  apply (frule qq3) apply simp apply simp apply simp apply simp
  apply (subst stackobject_nth_plus, simp, clarsimp,clarsimp,simp) 
  apply (rule extend_nth_the) apply (simp,clarsimp,assumption,simp,simp) 
(* x ≠ xs!i *)
 apply simp
 apply (drule_tac t="length vs" in sym,simp)
 apply (frule set_conv_nth_not)
 apply (subgoal_tac "z ∈ domRho rho")
  apply (subgoal_tac "length rho > 0") prefer 2 apply simp 
  apply (frule z_in_domRho, assumption+, simp) 
  apply (subgoal_tac "(map Val vs @  S) !+ (((rho |> z) + length vs)) =
                    S !+ (rho |> z)") prefer 2 apply (rule stackobject_envSearch_plus, simp) 
  apply simp
  apply (erule_tac x="z" in ballE)
   apply (case_tac " S !+ (rho |> z)", simp)
     apply (subgoal_tac "E1 z = extend E1 xs vs z",simp)
     apply (rule not_in_extend, assumption+)
    apply simp
   apply simp
  apply (simp add: extend_def)
  apply (simp add: extend_def) apply blast
(* z ∉ set xs *)
apply simp 
apply (subgoal_tac "z ∈ domRho rho")
 apply (subgoal_tac "length rho > 0") prefer 2 apply simp  
 apply (frule z_in_domRho, assumption+, simp) 
 apply (subgoal_tac "(map Val vs @  S) !+ (((rho |> z) + length vs)) =
                    S !+ (rho |> z)") prefer 2 apply (rule stackobject_envSearch_plus, simp,clarsimp)
 apply simp
 apply (erule_tac x="z" in ballE)
  apply (case_tac " S !+ (rho |> z)", simp)
    apply (subgoal_tac "E1 z = extend E1 xs vs z",simp)
    apply (rule not_in_extend, assumption+)
   apply simp
  apply simp
 apply (simp add: extend_def)
apply (simp add: extend_def)
apply (subgoal_tac "z ≠ self",blast) 
apply blast

apply (rule ballI) apply (rename_tac z)
apply (erule_tac x="z" and  A="dom E2 - {self}" in ballE)
 prefer 2 apply simp
(* z ∉ set xs *)
apply simp
apply (subgoal_tac "z ∉ set xs")
apply (subgoal_tac "z ∈ domRho rho")
 apply (subgoal_tac "length rho > 0") prefer 2 apply simp  
 apply (frule z_in_domRho, assumption+, simp) 
 apply (subgoal_tac "(map Val vs @  S) !+ (((rho |> z) + length vs)) =
                    S !+ (rho |> z)") prefer 2 apply (rule stackobject_envSearch_plus, simp,clarsimp)
 apply simp
apply blast
apply (elim conjE)
by blast

lemma identityEnvironment_case:
  "[|length rho > 0; 
   i < length alts;
   alts!i = (pati, ei);
   pati = ConstrP C ps ms;
   xs = map pat2var ps;
   nr = int (length vs);  rho_good rho;
   addEnv_good rho (zip xs (decreasing (length xs)));
   (E1, E2) \<Join> (rho,S); def_extend E1 xs vs;
   self ∈ dom E2;  dom (extend E1 xs vs) ∩ dom E2 = {};
   boundVar (Case (VarE x a) Of alts a') ∩ dom E2 = {}|]
   ==>  (extend E1 xs vs, E2) \<Join> ( rho + zip xs (decreasing (length xs)) , map Val vs @ S)"
apply (frule_tac ?E2.0="E2" in pattern_extend_case_good,assumption+) 
apply (erule_tac V="xs = map pat2var ps" in thin_rl)
apply (subgoal_tac "dom E1 ∩ dom E2 = {}")
 prefer 2 apply (simp add: extend_def) apply blast
by (rule identityEnvironment_case_aux,assumption+) 

lemma identityEnvironment_cased:
  "[|length rho > 0; 
   i < length alts;
   alts!i = (pati, ei);
   pati = ConstrP C ps ms;
   xs = map pat2var ps;
   nr = int (length vs);  rho_good rho;
   addEnv_good rho (zip xs (decreasing (length xs)));
   (E1, E2) \<Join> (rho,S); def_extend E1 xs vs;
   self ∈ dom E2;  dom (extend E1 xs vs) ∩ dom E2 = {};
   boundVar (CaseD (VarE x a) Of alts a') ∩ dom E2 = {}|]
   ==>  (extend E1 xs vs, E2) \<Join> ( rho + zip xs (decreasing (length xs)) , map Val vs @ S)"
apply (frule_tac ?E2.0="E2" in pattern_extend_cased_good,assumption+) 
apply (erule_tac V="xs = map pat2var ps" in thin_rl)
apply (subgoal_tac "dom E1 ∩ dom E2 = {}")
 prefer 2 apply (simp add: extend_def) apply blast
by (rule identityEnvironment_case_aux,assumption+) 


declare item2Stack.simps [simp del]
declare atom2item.simps [simp del]

lemma length_xs_eq_map_item_atom_as:
 "length as = length xs ==> length xs = length (map (item2Stack k S) (map (atom2item rho) as))"
by (induct as,clarsimp,clarsimp)


(** length lemmas **)
lemma length_decreasing_add_eq_length_add:
  "length (decreasing (length xs + length ys)) = (length xs + length ys)"
apply (induct xs ys rule:list_induct2')
 apply (simp, subst decreasing.simps,simp) 
 apply (simp, subst decreasing.simps, simp, rule length_decreasing_eq_length)
 apply (simp, subst decreasing.simps, simp, rule length_decreasing_eq_length)
by (simp, subst decreasing.simps,simp, subst decreasing.simps,simp)


(** dom lemmas **)
lemma dom_map_zip [rule_format]:
  "distinct xs --> length xs = length ys
   --> dom (map_of (map (λ(x, y). (x, y)) (zip xs ys))) = set xs"
apply (induct xs arbitrary: ys, simp, clarsimp)
by (case_tac ys,simp,clarsimp) 


lemma dom_map_zip2 [rule_format]:
  "distinct xs --> length xs = length ys
   --> dom (map_of (zip xs ys)) = set xs"
by (induct xs arbitrary: ys, simp, clarsimp)
 


lemma domRho_app:
  "[| distinct (xs @ rs); self ∉ set xs; self ∉ set rs;
    length as = length xs; length rr = length rs;
    E1' = map_of (zip xs (map (atom2val E1) as)); 
    E2' = map_of (zip rs (map (the o E2) rr))(self \<mapsto> Suc k) |]
   ==> dom E1' ∪ dom E2' - {self} = domRho ([(empty, 0, 0)] + zip (xs @ rs) (decreasing (length xs + length rs)))"
apply clarsimp
apply (simp add: envAdd.simps, simp add: Let_def)
apply (subst dom_map_zip, simp, subst length_decreasing_add_eq_length_add, simp)
apply (subgoal_tac "(set xs ∪ set rs) ∩ {self} = {}",simp)
by blast

lemma xs_i_in_domRho:
  "[|distinct xs; distinct rs; set xs ∩ set rs = {}; i < length xs|] 
   ==> xs ! i ∈ domRho ([(empty, 0, 0)] + zip (xs @ rs) (decreasing (length xs + length rs)))"
apply (simp add: envAdd.simps, simp add: Let_def)
apply (subst dom_map_zip, simp)
 apply (subst length_decreasing_add_eq_length_add, simp)
by clarsimp


lemma rs_j_in_domRho:
  "[|distinct xs; distinct rs; set xs ∩ set rs = {}; j < length rs|] 
   ==> rs ! j ∈ domRho ([(empty, 0, 0)] + zip (xs @ rs) (decreasing (length xs + length rs)))"
apply (simp add: envAdd.simps, simp add: Let_def)
apply (subst dom_map_zip, simp)
 apply (subst length_decreasing_add_eq_length_add,simp)
by clarsimp

lemma rho_good_xs:
"rho_good ([(empty, 0, 0)] + zip xs (decreasing (length xs)))"
apply (induct xs) 
 apply (simp add: envAdd.simps, simp add: Let_def, simp add: rho_good.simps, simp add: rho_good'.simps)
apply (clarsimp, subst decreasing.simps, simp)
apply (simp add: envAdd.simps, simp add: Let_def, simp add: rho_good.simps, simp add: rho_good'.simps)
apply (rule conjI)
 apply (rule length_decreasing_leq_length)
apply (rule ballI)
 apply (rule conjI, rule impI, rule length_decreasing_leq_length)
apply (rule impI, erule_tac x="x" in ballE)
 apply (clarsimp, arith)
by (simp add: dom_def)


lemma rho_good_xs_ys [rule_format]:
  "distinct (xs @ ys) --> rho_good ([(empty, 0, 0)] + zip (xs @ ys) (decreasing (length xs + length ys)))"
apply (induct xs)
 apply (simp, rule impI, rule rho_good_xs)
apply (clarsimp, subst decreasing.simps, simp)
apply (simp add: envAdd.simps, simp add: Let_def, simp add: rho_good.simps, simp add: rho_good'.simps)
apply (rule conjI)
 apply (subst length_decreasing_add_eq_length_add, simp)
apply (rule ballI, rule conjI)
 apply (rule impI, subst length_decreasing_add_eq_length_add, simp)
apply (rule impI, clarsimp)
apply (erule_tac x="x" in ballE) 
 apply (elim conjE,simp)
by (simp add: dom_def)

lemma elements_domRho:
"[| distinct (append xs rs); x ∈ domRho ([(empty, 0, 0)] + zip (xs @ rs) (decreasing (length xs + length rs))) |] 
   ==> (∃ i<length xs. x = xs!i) ∨ (∃ j<length rs. x = rs!j)"
apply (simp add: envAdd.simps, simp add: Let_def)
apply (subgoal_tac "dom (map_of (map (λ(x, y). (x, y)) (zip (xs @ rs) (decreasing (length xs + length rs))))) = 
                    set (append xs rs)",simp)
 prefer 2 apply (rule dom_map_zip, simp, simp, subst length_decreasing_add_eq_length_add, simp)
by (auto simp:set_conv_nth)



lemma addEnv_empty_xs_i [rule_format]:
  " distinct (xs @ rs) --> i < length xs --> xs!i ∈ domRho ([(empty, 0, 0)] + zip (xs @ rs) (decreasing (length xs + length rs)))
    --> rho_good ([(empty, 0, 0)] + zip (xs @ rs) (decreasing (length xs + length rs)))
    --> ([(empty, 0, 0)] + zip (xs @ rs) (decreasing (length xs + length rs))) |> (xs!i) = i"
apply (induct xs i rule: list_induct3)

  apply simp

  apply (clarsimp, subst decreasing.simps, simp)
  apply (simp add: envAdd.simps, simp add: Let_def, simp add: envSearch.simps)

  apply clarsimp

  apply clarsimp
  apply (subgoal_tac "xs ! i ∈ domRho ([(empty, 0, 0)] + zip (xs @ rs) (decreasing (length xs + length rs)))",simp)
   apply (subgoal_tac "rho_good ([(empty, 0, 0)] + zip (xs @ rs) (decreasing (length xs + length rs)))",simp)
    apply (subst decreasing.simps, simp, simp add: envAdd.simps, simp add: Let_def, simp add: envSearch.simps)
    apply (rule conjI)
     apply (clarsimp, rule impI)
    apply (case_tac "(map_of (map (λ(x, y). (x, y)) (zip (xs @ rs) (decreasing (length xs + length rs)))) (xs ! i))")
     apply (rule_tac s="None" in ssubst,assumption, clarsimp)
    apply clarsimp
    apply (subst length_decreasing_add_eq_length_add,simp)
    apply (subst length_decreasing_add_eq_length_add,simp)
    apply (subgoal_tac "min (length xs + length rs) (length (decreasing (length xs + length rs))) = (length xs + length rs)", simp)
     apply (simp add: rho_good.simps, simp add: rho_good'.simps)
     apply (erule_tac x="(xs ! (length xs + length rs - a))" in ballE)
      apply (elim conjE, erule_tac x="(xs ! (length xs + length rs - a))" in ballE)
       apply (elim conjE,clarsimp,arith)
      apply (simp add: dom_def)
     apply clarsimp
    apply (subst length_decreasing_add_eq_length_add,simp)
   apply (rule rho_good_xs_ys,simp)
 by (rule xs_i_in_domRho,assumption+)






lemma map_arguments_i [rule_format]:
  "i < length as --> (∀ a ∈ set (map (item2Stack k S) (map (atom2item rho) as)). ∃ v. a = Val v)
   --> append (append (map (item2Stack k S) (map (atom2item rho) as)) (map (item2Stack k S) (map (region2item rho) rr)))
                             (drop td S) !+ i =
                      ((map (item2Stack k S) (map (atom2item rho) as))!+ i)"
by (induct as i rule: list_induct3, clarsimp+)

(*
lemma map_arguments_i [rule_format]:
  "i < length as
   --> append (append (map (item2Stack k S) (map (atom2item rho) as)) (map (item2Stack k S) (map (region2item rho) rr)))
                             (drop td S) !+ i =
                      ((map (item2Stack k S) (map (atom2item rho) as))!+ i)"
apply (induct as i rule: list_induct3, clarsimp+)
*)

lemma map_of_length [rule_format]:
" map_of (map (λ(x, y). (x, y)) (zip ys (decreasing (length ys)))) x = Some y -->
             y ≤ length ys ∧ y ≤ length (decreasing (length ys)) ∧ Suc 0 ≤ y"
apply (induct ys,simp,clarsimp)
apply (subgoal_tac "(decreasing (Suc (length ys))) = (Suc (length ys)) # (decreasing (length ys))",simp)
 apply (split split_if_asm,simp) 
  apply (subst length_decreasing_eq_length,simp)
 apply simp
by (subst decreasing.simps, simp)


lemma rho_good_map_of:
  "rho_good [(map_of (map (λ(x, y). (x, y)) (zip (xs @ r # rs) (decreasing (Suc (length xs + length rs))))),
              min (Suc (length xs + length rs)) (length (decreasing (Suc (length xs + length rs)))), 0)]"
apply (induct xs) 
 apply (simp add: rho_good.simps, simp add: rho_good'.simps)
 apply (rule ballI, clarsimp)
 apply (subgoal_tac "decreasing (Suc (length rs)) = Suc (length rs) # decreasing (length rs)",simp)
  apply (split split_if_asm)
   apply (simp, subst length_decreasing_eq_length, simp)
  apply (frule map_of_length,simp)
 apply (subst decreasing.simps,simp)
apply clarsimp
apply (subgoal_tac "decreasing (Suc (length xs + length rs)) = 
                    Suc (length xs + length rs) # decreasing (length xs + length rs)",simp)
 apply (subst decreasing.simps,simp)
 apply (simp add: rho_good.simps, simp add: rho_good'.simps)
 apply (rule conjI)
  apply (subst decreasing.simps, simp)
  apply (subst length_decreasing_add_eq_length_add, simp)
 apply clarsimp
 apply (rule conjI) 
  apply (rule impI, subst decreasing.simps, simp)
  apply (subst length_decreasing_add_eq_length_add, simp)
 apply (rule impI) 
 apply (erule_tac x="x" in ballE,clarsimp)
  apply (subgoal_tac "min (length xs + length rs) (length (decreasing (length xs + length rs))) = 
                      (length xs + length rs)",simp)
   apply (subst decreasing.simps,simp)
  apply (subst length_decreasing_add_eq_length_add,simp)
 apply (simp add: dom_def)
by (subst decreasing.simps,simp)


lemma addEnv_empty_xs_r [rule_format]:
  " r ∉ set xs --> distinct xs --> r ∉ set rs --> distinct rs -->  set xs ∩ set rs = {}
    --> ([(empty, 0, 0)] + zip (xs @ r # rs) (decreasing (Suc (length xs + length rs)))) |> r = length xs"
apply (induct xs)
 apply (clarsimp, subst decreasing.simps, simp)
 apply (simp add: envAdd.simps, simp add: Let_def, simp add: envSearch.simps) 
apply (clarsimp, subst decreasing.simps, simp)
apply (simp add: envAdd.simps, simp add: Let_def, simp add: envSearch.simps) 
apply (case_tac "(map_of (map (λ(x, y). (x, y)) (zip (xs @ r # rs) (decreasing (Suc (length xs + length rs))))) r)",simp)
 apply (subgoal_tac "r ∈ dom (map_of (map (λ(x, y). (x, y)) (zip (xs @ r # rs) (decreasing (Suc (length xs + length rs))))))")
  prefer 2 apply (subst dom_map_zip, simp, simp, subst decreasing.simps, simp, subst length_decreasing_add_eq_length_add, simp, simp) 
 apply (simp add: dom_def)
apply clarsimp
apply (subgoal_tac
  "rho_good [(map_of (map (λ(x, y). (x, y)) (zip (xs @ r # rs) (decreasing (Suc (length xs + length rs))))),
            min (Suc (length xs + length rs)) (length (decreasing (Suc (length xs + length rs)))), 0)]")
 apply (simp add: rho_good.simps, simp add: rho_good'.simps)
 apply (erule_tac x="r" in ballE)
  apply (elim conjE, clarsimp, arith)
 apply (simp add: dom_def)
by (rule rho_good_map_of)


lemma map_of_rs_j_aux [rule_format]:
  " x ∉ set rs --> j < length rs --> r ∉ set rs --> r ∉ set xs --> set xs ∩ set rs = {}
   --> map_of (map (λ(x, y). (x, y)) (zip (x # xs @ r # rs) (decreasing (Suc (Suc (length xs + length rs)))))) (rs ! j) = Some y
   --> map_of (map (λ(x, y). (x, y)) (zip (x # xs @ rs) (decreasing (Suc (length xs + length rs))))) (rs ! j) = Some y"
apply (induct xs) 
 apply (clarsimp, subst decreasing.simps, simp)
 apply (subgoal_tac "(decreasing (Suc (Suc (length rs)))) = (Suc (Suc (length rs))) # Suc (length rs) # (decreasing (length rs))")
  apply (clarsimp, rule conjI) 
   apply (rule impI,clarsimp)
  apply (rule impI, clarsimp) 
  apply (subgoal_tac "r ≠ rs ! j",simp,clarsimp)
 apply (subst decreasing.simps, simp, subst decreasing.simps, simp)
apply (clarsimp, subst decreasing.simps, simp)
apply (subgoal_tac "(decreasing (Suc (Suc (Suc (length xs + length rs))))) =
                    (Suc (Suc (Suc (length xs + length rs)))) # (decreasing (Suc (Suc (length xs + length rs))))",simp)
 apply (subgoal_tac "(decreasing (Suc (Suc (length xs + length rs)))) =
                     (Suc (Suc (length xs + length rs))) # (decreasing (Suc (length xs + length rs)))",simp)
  apply (subgoal_tac "(decreasing (Suc (length xs + length rs))) =
                      (Suc (length xs + length rs)) # (decreasing (length xs + length rs))",simp)
   apply (rule conjI) 
    apply (rule impI, clarsimp)
   apply (rule impI, rule conjI) 
    apply (rule impI, clarsimp)
   apply clarsimp
by (subst decreasing.simps, simp)+



lemma addEnv_empty_rs_r_j [rule_format]:
  "distinct xs --> distinct rs --> set xs ∩ set rs = {} --> j < length rs 
   -->  rs!j ∈ domRho ([(empty, 0, 0)] + zip (xs @ rs) (decreasing (length xs + length rs)))
   --> ([(empty, 0, 0)] + zip (xs @ rs) (decreasing (length xs + length rs))) |> (rs!j) = (length xs + j)"
apply (induct rs j rule: list_induct3)

  apply simp

  apply clarsimp
  apply (rename_tac r rs, rule addEnv_empty_xs_r, assumption+)

  apply clarsimp

  apply clarsimp
  apply (rename_tac r rs j)
  apply (subgoal_tac "rs ! j ∈ domRho ([(empty, 0, 0)] + zip (xs @ rs) (decreasing (length xs + length rs)))",simp)
  prefer 2 apply (frule_tac xs="xs" and rs="rs" in rs_j_in_domRho, assumption+)

  apply (case_tac xs,clarsimp)
   apply (subst decreasing.simps, simp)
   apply (subgoal_tac "rho_good ([(empty, 0, 0)] + zip rs (decreasing (length rs)))")
    prefer 2 apply (rule rho_good_xs)
   apply (simp add: envAdd.simps add: Let_def add: envSearch.simps)
   apply (case_tac "(map_of (map (λ(x, y). (x, y)) (zip rs (decreasing (length rs)))) (rs ! j))",clarsimp)
   apply (clarsimp, rule conjI) 
    apply (clarsimp)
   apply (rule impI) 
   apply (subgoal_tac "(min (length rs) (length (decreasing (length rs)))) = length rs",simp)
    apply (simp add: rho_good.simps, simp add: rho_good'.simps)
    apply (erule_tac x="rs ! (length rs - a)" in ballE) 
     apply (elim conjE, clarsimp, arith)
    apply (clarsimp) 
   apply (subst length_decreasing_eq_length, simp)
  apply clarsimp  
  apply (rename_tac r rs j x xs)
  apply (simp add: envAdd.simps, simp add: Let_def, simp add: envSearch.simps, clarsimp)
  apply (subgoal_tac "(min (Suc (length xs + length rs)) (length (decreasing (Suc (length xs + length rs))))) =
                       (Suc (length xs + length rs))",simp)
   prefer 2 apply (subst decreasing.simps, simp)
   apply (subst length_decreasing_add_eq_length_add, simp)
  apply (subgoal_tac "min (Suc (Suc (length xs + length rs))) (length (decreasing (Suc (Suc (length xs + length rs))))) =
                     (Suc (Suc (length xs + length rs)))",simp)
   prefer 2 apply (subst decreasing.simps, simp)
  apply (frule_tac x="x" and r="r" and j="j" and xs="xs" and rs="rs" in map_of_rs_j_aux, assumption+)
  by (clarsimp, arith)


declare identityEnvironment.simps [simp del] 

(***********************************)

lemma in_set_conv_nth_1:
 " x ∈ set xs ==> ∃ i<length xs. x = xs!i"
by(auto simp:set_conv_nth)

lemma conv_nth_in_set:
  "i < length xs ==> xs!i ∈ set xs"
by(auto simp:set_conv_nth)

lemma xi1:
 "[|i < length xs; length as = length xs; xi = xs ! i; distinct xs; as ! i = VarE x a|]
  ==> Val (the (map_of (zip xs (map (atom2val E1) as)) (xs ! i))) = Val (the (E1 (x)))"
apply (induct xs as arbitrary:i rule: list_induct2',simp,simp,simp,clarsimp)
apply (rule conjI) 
 apply (rule impI,clarsimp)
 apply (case_tac i,simp,clarsimp)
apply (rule impI)
by (case_tac i,simp,clarsimp)

lemma ri1:
 "[|i < length rs; length rr = length rs; ri = rs ! i; distinct rs |]
  ==> Reg (the (map_of (zip rs (map (the o E2) rr)) (rs ! i))) = Reg (the (E2 (rr ! i)))"
apply (induct rr rs arbitrary:i rule: list_induct2',simp,simp,simp,clarsimp)
apply (rule conjI) 
 apply (rule impI,clarsimp)
 apply (case_tac i,simp,clarsimp) 
apply (rule impI)
by (case_tac i,simp,clarsimp)


lemma app_var_arguments_good [rule_format]:
  "i < length as 
   --> as ! i = VarE x a 
   --> fvs' as ⊆ dom E1 
   --> x ∈ dom E1"
apply (induct as arbitrary:i,simp,clarsimp)
apply (case_tac i) 
by (simp add:dom_def)+ 


lemma identityEnvironment_App:
  "[|length rho> 0; rho_good rho; distinct (append xs rs); length as = length xs; length rr = length rs;
    ∀ a ∈ set as. atom a; self ∉ set xs; self ∉ set rs;
    fvReg (AppE f as rr a) ⊆ dom (snd (E1, E2));
    fv (AppE f as rr a) ⊆ dom (fst (E1, E2));
    E1' = map_of (zip xs (map (atom2val E1) as));
    E2' = map_of (zip rs (map (the o E2) rr))(self \<mapsto> Suc k); 
    n = length xs; 
    l = length rs;
    (E1, E2) \<Join> (rho ,S)|]
    ==>  (E1', E2') \<Join> ( [(empty, 0, 0)] +
                          zip (xs @ rs)
                           (decreasing
                             (length xs + length rs)) ,  map (item2Stack k S) (map (atom2item rho) as) @ 
                                                         map (item2Stack k S) (map (region2item rho) rr) @ drop td S) "
apply (subst identityEnvironment.simps, rule conjI)
apply (rule domRho_app,assumption+)
apply (rule conjI)

(* E1 *)
apply clarsimp
apply (simp add: identityEnvironment.simps) apply (elim conjE)
apply (frule in_set_conv_nth_1)
(* x = xi *)
 apply (erule exE, elim conjE,simp)
 apply (erule_tac x="as!i" in ballE)
 apply (case_tac "as!i", simp_all) 
 (* ConstE *)
 apply (rule xiConstE)
 (* VarE *)
 apply (rename_tac xi i x a)
 apply (erule_tac x="x" and A="dom E1" in ballE)
 apply (subgoal_tac "Val (the (map_of (zip xs (map (atom2val E1) as)) (xs ! i))) = 
                     Val (the (E1 (x)))", simp)
  prefer 2  apply (rule xi1,assumption+)
 apply (subgoal_tac "S !+ (rho |> (x)) = 
                     append (append (map (item2Stack k S) (map (atom2item rho) as)) (map (item2Stack k S) (map (region2item rho) rr)))
                            (drop td S) !+ i",simp)
  prefer 2 apply (rule xi2) 
 apply (subgoal_tac "([(empty, 0, 0)] + zip (xs @ rs) (decreasing (length xs + length rs))) |> (xs!i) = i",simp)
 apply (rule xi3)
apply (subgoal_tac "i < length as")
apply (frule app_var_arguments_good,assumption+,simp,simp)



(* E2 *)
apply (simp add: identityEnvironment.simps) apply (elim conjE)
apply (rule ballI) 
apply (rule conjI)
apply (rule impI) apply simp
apply (rule impI)
apply (frule in_set_conv_nth_1)
(* x = rj *)
apply (erule exE, elim conjE) apply simp 
 apply (erule_tac x="rr!i" and A="dom E2 - {self}" in ballE)
 apply (subgoal_tac "Reg (the (map_of (zip rs (map (the o E2) rr)) (rs ! i))) = 
                     Reg (the (E2 (rr ! i)))", simp)
  prefer 2 apply (rule ri1,assumption+)
 apply (subgoal_tac "S !+ (rho |> (rr ! i)) = 
                     append (append (map (item2Stack k S) (map (atom2item rho) as)) (map (item2Stack k S) (map (region2item rho) rr)))
                            (drop td S) !+  (length xs + i)",simp)
  prefer 2 apply (rule ri2)
 apply (subgoal_tac "(length xs + i) = ([(empty, 0, 0)] + zip (xs @ rs) (decreasing (length xs + length rs))) |> (rs!i)",simp)
 apply (rule ri3)
apply (subgoal_tac "∀ r ∈ set rr. r ∈ dom E2 - {self}",clarsimp)
apply (rule good_app_region_arguments)
done

end