theory stlc_metatheory imports stlc begin

(* This thy file runs against Isabelle snapshot from 26 March
2007. Known not to work against Isabelle 2005. *)

locale tmp

(* ******************************************************************************** *)
-- "library lemmas"

lemma list_all_map: "list_all f (map g xs) = list_all (f o g) xs" 
  apply(induct_tac xs, auto) done

lemma list_all_cong: "(! x : set xs. P x = Q x) \<Longrightarrow> (list_all P xs = list_all Q xs)"
  apply(simp add: list_all_iff) done

lemma map_of: " x \<notin> fst ` set G1 \<longrightarrow> (D ++ map_of G1) x = D x"
  apply(induct_tac G1) apply(auto) apply(simp add: map_add_def) done

lemma P_imp_P: "P \<Longrightarrow> P" by force

lemma list_all_id_map: "list_all (% x. x) (map f xs) = list_all f xs" 
  apply(induct xs, auto) done

lemma (in tmp) list_decomp[rule_format]: 
  "map_of G' x = Some Ta \<longrightarrow> (\<exists>G1 G2. (G' = (G1 @ (x, Ta) # G2)) \<and> x \<notin> fst ` set G1)"
  apply(induct_tac G')
  apply(force)
  apply(intro allI impI) apply(case_tac a) apply(rename_tac x' T')
  apply(case_tac "x'=x") apply(force)
  apply(erule impE) apply(drule_tac not_sym) apply(force)
  apply(elim exE)
  apply(rule_tac x="a#G1" in exI) apply(force)
  done
    (* boring *)

(* ******************************************************************************** *)
-- "tapl proofs"

lemma (in tmp) proj_compose: "! u.
  ((\<lambda>(l_x, x_x, t_x). f l_x x_x t_x) ((\<lambda>(l, x, t, T). (l, x, t)) u))
  = ((\<lambda>(l_x, x_x, t_x, T). f l_x x_x t_x) u)" 
  apply(force) done

lemma (in tmp) tmp: "
  ! t_T_list.
  v_list @ ta # t_list = map (\<lambda>(t_x, T_x). t_x) t_T_list 
  \<longrightarrow> (? T_v_list T_ta T_t_list. 
  length T_v_list = length v_list 
  & length T_t_list = length t_list 
  & t_T_list = zip (v_list @ ta # t_list) (T_v_list @ T_ta # T_t_list))"
  apply(induct_tac v_list) 
   apply(rule,rule) 
   apply(rule_tac x="[]" in exI)
   apply(rule_tac x="snd (hd t_T_list)" in exI)
   apply(rule_tac x="map snd (tl t_T_list)" in exI) 
   apply(simp) 
   apply(rule) apply(case_tac t_T_list) apply(force) apply(force)
   apply(case_tac t_T_list) apply(force)
   apply(simp)
   apply(rule, force)
   apply(induct_tac list, force, force)

   apply(intro allI impI)
   apply(case_tac t_T_list) apply(force)
   apply(rename_tac tl_t_T_list)
   apply(simp) apply(drule_tac x="tl_t_T_list" in spec) 
   apply(erule impE, force)
   apply(elim exE conjE)
   apply(rule_tac x="snd aa#T_v_list" in exI)
   apply(rule, force)
   apply(force)
   done
  (* FIXME too ugly *)

lemma set_list_minus: "set (list_minus xs ys) = set xs - set ys" 
  apply(induct_tac xs, auto) done

lemma is_v_of_t_list: "is_v_of_t_list xs = list_all is_v_of_t xs" 
  apply(induct_tac xs, auto) done

lemma fv_t_list: "
  (t,T) : set t_T_list --> set (fv_t t) <= set (fv_t_list (map (\<lambda>(t_x, T_x). t_x) t_T_list))" 
  apply(induct_tac t_T_list) apply(force) apply(force) done

lemma context_lem: "
  ! G t T. (G,t,T) : typing
  \<longrightarrow> (! G'. (! x. x : set (fv_t t) \<longrightarrow> (map_of G x = map_of G' x))
  \<longrightarrow> (G',t,T) : typing)" 
  apply(intro allI, rule)
  apply(erule typing.induct)
   (* 25 subgoals *)
   apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   (* TmVar *)
   apply(force intro: typing.intros tmp.list_decomp[rule_format] simp: map_of)
   (* TmAbs *)
   apply(force intro: typing.intros simp: set_list_minus)
   (* TmApp *)
   apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   (* TmLet *)
   apply(force intro: typing.intros simp: set_list_minus)
   apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   (* TmCaseSm *)
   apply(force intro: typing.intros simp: set_list_minus)
   apply(force intro: typing.intros)
   (* TmTuple *)
   apply(intro allI impI, simp)
   apply(rule typing.intros) apply(simp add: list_all_id_map) apply(simp add: list_all_iff)
   apply(intro ballI) apply(case_tac x) apply(rename_tac t T)
   apply(simp) apply(drule_tac x="(t,T)" in bspec) apply(force) apply(simp) apply(elim conjE) 
   apply(drule_tac x=G' in spec) apply(erule impE) 
    apply(subgoal_tac "(t, T) \<in> set t_T_list \<longrightarrow> set (fv_t t) <= set (fv_t_list (map (\<lambda>(t_x, T_x). t_x) t_T_list))") prefer 2 apply(induct_tac t_T_list) apply(force,force)
    apply(force)
   apply(force)
   (* TmProjTp *)
   apply(intro allI impI) apply(rule typing.intros) apply(force) apply(force) (* force alone fails on this case *)
   (*TmVariant *)
   apply(intro allI impI) apply(rule typing.intros) apply(force) apply(force) (* force alone fails on this case *)
   (* TmCase *)
   apply(intro allI impI, simp)
   apply(rule typing.intros)
    apply(force)
    apply(simp add: list_all_iff)
    apply(rule)
    apply(simp add: split_paired_all) apply(rename_tac l x t T)
    apply(drule_tac x="(l,x,t,T)" in bspec) apply(force)
    apply(simp) apply(elim conjE)
    apply(drule_tac x="(x, T) # G'" in spec) back 
    apply(erule impE) 
     apply(intro allI impI) apply(case_tac "xa = x") apply(force) apply(simp)
     apply(drule_tac x=xa in spec) apply(elim conjE)
     apply(subgoal_tac "
(l,x,t,T) : set l_x_t_T_list 
\<longrightarrow> set (fv_t t) <= {x} Un set (fv_C_list (map (\<lambda>(l_x, x_x, t_x, T_x). CCase l_x x_x t_x) l_x_t_T_list))
       ") prefer 2 apply(induct_tac l_x_t_T_list) apply(force) apply(force simp add: set_list_minus) (* should be lemma *)
    apply(force)
    
    apply(force)
    apply(force)
  done

lemma fv_lem: "
  ! G t Ty. (G,t,Ty) : typing 
  \<longrightarrow> (! x. x : set (fv_t t) 
  \<longrightarrow> (? Ty'. map_of G x = Some Ty'))"
  apply(intro allI, rule, erule typing.induct)
  apply(force simp: set_list_minus)+
  (* TmTuple *)
  apply(intro allI impI, simp add: set_list_minus list_all_iff)
  apply(subgoal_tac "
    x \<in> set (fv_t_list (map (\<lambda>(t_x, T_x). t_x) t_T_list))
    \<longrightarrow> (? t T. (t,T) : set t_T_list & x : set (fv_t t))"
  ) prefer 2 apply(induct_tac t_T_list) apply(force) apply(force) (* should be lemma *)
  apply(force)
  (* TmProjTp *)
  apply(force simp: set_list_minus)
  apply(force simp: set_list_minus)
  (* TmCase *)
  apply(intro allI impI, simp add: set_list_minus list_all_iff)
  apply(erule disjE) apply(force)
  apply(subgoal_tac "
    x \<in> set (fv_C_list (map (\<lambda>(l_x, x_x, t_x, T_x). CCase l_x x_x t_x) l_x_t_T_list))
    \<longrightarrow> (? l x' t T. (l,x',t,T) : set l_x_t_T_list & x : set (fv_t t) - {x'})
    ") prefer 2 apply(induct_tac l_x_t_T_list) apply(force) apply(simp add: set_list_minus) apply(rule) apply(simp add: split_paired_all) apply(rename_tac l x' t T list) apply(simp add: set_list_minus) apply(rule) apply(rule_tac x=l in exI, rule_tac x=x' in exI, rule_tac x=t in exI) apply(force) apply(blast) (* should be lemma, automation struggling *)
  apply(simp)
  apply(elim exE conjE)
  apply(drule_tac x="(l,x',t,Ta)" in bspec) apply(force)
  apply(simp) apply(elim conjE)
  apply(force)
  done

lemma weakening_lem: "
  !G t Ty. (G, t, Ty) : typing  -->
  (!G'. (!x T1. (map_of G x = Some T1) \<longrightarrow> (map_of G' x = Some T1)) 
  --> (G', t, Ty) : typing)"
  apply(intro allI impI)
  apply(rule context_lem[rule_format]) apply(assumption)
  apply(force dest: fv_lem[rule_format])
  done

lemma weakening_lem: "
  ([], t, Ty) : typing  ==> (G', t, Ty) : typing"
  apply(rule weakening_lem[rule_format]) by(force+)

lemma canon_val_lem: "
  ! G t T. (G,t,T) : typing 
  \<longrightarrow> is_v_of_t t
  \<longrightarrow> ((T = TyBool \<longrightarrow> t = TmTrue | t = TmFalse)
  & (T = TyNat \<longrightarrow> t = TmZero | (? t'. t = TmSucc t' & is_v_of_t t'))
  & (~ (? x. T = TyId x))
  & (! T1 T2. T = TyArr T1 T2 \<longrightarrow> (? x T3 t'. t = TmAbs x T3 t'))
  & (T = TyUnit \<longrightarrow> (t = TmUnit))
  & (! T1 T2. T = TyPair T1 T2 \<longrightarrow> (? t' t''. t = TmPair t' t''))
  & (! T1 T2. T = TySum T1 T2 \<longrightarrow> (? t'. t = TmInl t' | t = TmInr t'))
  & (! Tl. T = TyTuple Tl \<longrightarrow> (? tl. t = TmTuple tl & length tl = length Tl))
  & (! l_T_list. T = TyVariant l_T_list \<longrightarrow> (? j t'. t = (TmVariant ((% (l,T). l) (l_T_list ! (j - 1::nat))) t' T) & 1 <= j & j <= length l_T_list)))"
  apply(intro allI, rule)
  apply(erule typing.induct)
  apply(simp_all)
  (* one goal left *)
  apply(rule, simp)
  apply(case_tac "(\<lambda>(l_x, T_x). T_x) (l_T_list ! (j - Suc 0))")
  apply(simp_all)
  apply(rule_tac x=j in exI, force)+
  done

lemma progress_thm: "
  ! G t T. (G,t,T) : typing \<longrightarrow> G = [] \<longrightarrow> is_v_of_t t \<or> (? t'. (t,t') : red)" (* FIXME should be reduces iff not v? *)
  apply(intro allI, rule)
  apply(erule_tac typing.induct)
   apply(force)
   apply(force)
   (* TmIf *)
   apply(intro allI impI, simp) 
   apply(elim disjE) (* 7 subgoals *)
    apply(force dest: canon_val_lem[rule_format] intro: red.intros)
    apply(force dest: canon_val_lem[rule_format] intro: red.intros)
    apply(force dest: canon_val_lem[rule_format] intro: red.intros)
    apply(force dest: canon_val_lem[rule_format] intro: red.intros)
    apply(force dest: canon_val_lem[rule_format] intro: red.intros)
    apply(force dest: canon_val_lem[rule_format] intro: red.intros)
    apply(force dest: canon_val_lem[rule_format] intro: red.intros)
    apply(force dest: canon_val_lem[rule_format] intro: red.intros)
   (* TmZero *)
   apply(force intro: red.intros elim: red.elims)
   apply(force intro: red.intros elim: red.elims)
   (* TmPred *)
   apply(intro allI impI, simp) 
   apply(elim disjE) (* 2 subgoals *)
    apply(frule_tac canon_val_lem[rule_format]) apply(assumption) apply(force intro: red.intros)
    apply(force intro: red.intros)
   (* TmIszero *)
   apply(intro allI impI, simp)
   apply(elim disjE)
    apply(frule_tac canon_val_lem[rule_format]) apply(assumption) apply(force intro: red.intros)
    apply(force intro: red.intros)
   (* TmVar *)
   apply(force dest: canon_val_lem[rule_format] intro: red.intros)
   apply(force dest: canon_val_lem[rule_format] intro: red.intros)
   (* TmApp *)
   apply(intro allI impI, simp)
   apply(elim disjE)  (* 4 subgoals *)
    apply(frule_tac canon_val_lem[rule_format]) apply(assumption) apply(force intro: red.intros)
    apply(force intro: red.intros)
    apply(force intro: red.intros)
    apply(force intro: red.intros)
   (* TmUnit *)
   apply(force dest: canon_val_lem[rule_format] intro: red.intros)
   (* TmSeq *)
   apply(intro allI impI, simp)
   apply(elim disjE)  (* 4 subgoals *)
    apply(frule_tac canon_val_lem[rule_format]) apply(assumption) apply(force intro: red.intros)
    apply(frule_tac canon_val_lem[rule_format]) apply(assumption) apply(force intro: red.intros)
    apply(force intro: red.intros)
    apply(force intro: red.intros)
   (* TmAscribe *)
   apply(force dest: canon_val_lem[rule_format] intro: red.intros)
   apply(force intro: red.intros elim: red.elims)
   apply(force intro: red.intros elim: red.elims)
   (* TmProj1 *)
   apply(intro allI impI, simp)
   apply(elim disjE)  (* 2 subgoals *)
    apply(frule_tac canon_val_lem[rule_format]) apply(assumption) apply(force intro: red.intros)
    apply(force intro: red.intros)
   (* TmProj2 *)
   apply(intro allI impI, simp)
   apply(elim disjE)  (* 2 subgoals *)
    apply(frule_tac canon_val_lem[rule_format]) apply(assumption) apply(force intro: red.intros)
    apply(force intro: red.intros)
   (* TmInl *)
   apply(force dest: canon_val_lem[rule_format] intro: red.intros)
   (* TmInR *)
   apply(force dest: canon_val_lem[rule_format] intro: red.intros)
   (* TmCaseSm *)
   apply(intro allI impI, simp)
   apply(elim disjE)  (* 2 subgoals *)
    apply(frule_tac canon_val_lem[rule_format]) apply(assumption) apply(force intro: red.intros)
    apply(force intro: red.intros)
   (* TmFix *)
   apply(intro allI impI, simp)
   apply(elim disjE)  (* 2 subgoals *)
    apply(frule_tac canon_val_lem[rule_format]) apply(assumption) apply(force intro: red.intros)
    apply(force intro: red.intros)
   (* TmTuple *)
   apply(intro allI impI, simp)
   apply(erule rev_mp) 
   apply(induct_tac t_T_list)
    apply(force)
    apply(intro allI impI, simp, elim conjE exE)
    apply(case_tac a) apply(rename_tac t T) apply(simp) apply(elim conjE)
    apply(erule disjE) back
     (* is_v_of_t t*)
     apply(simp)
     apply(erule disjE)
      apply(rule disjI1) apply(force)
      apply(rule disjI2) apply(elim exE) apply(erule red.elims) apply(simp_all)
      apply(rule_tac x="TmTuple (t#v_list @ t'a # t_list)" in exI) 
      apply(subgoal_tac "(TmTuple ((t#v_list) @ [ta] @ t_list), TmTuple ((t#v_list) @ [t'a] @ t_list)) : red") apply(force) 
      apply(rule red.intros) apply(force) apply(force)

     (* ? t'. (t,t') : red *)
     apply(rule disjI2)
     apply(elim exE conjE)
     apply(rule_tac x="(TmTuple (t' # map (\<lambda>(t_x, T_x). t_x) list))" in exI)
     apply(subgoal_tac "
(TmTuple ([] @ [t] @ map (\<lambda>(t_x, T_x). t_x) list), TmTuple ([] @ [t'] @ map (\<lambda>(t_x, T_x). t_x) list)) \<in> red
       ") apply(force)
     apply(rule red.intros) apply(force) apply(force)
     (* FIXME could these be combined? is this any better than what we had before? *)
   (* TmProjTp *)
   apply(rule, simp)
   apply(erule disjE)
    (* is_v_of_t t1 *)
    apply(erule typing.elims, simp_all)
    apply(simp add: list_all_id_map)
    apply(rule_tac x="((%v_x . v_x) (List.nth (map (\<lambda>(t_x, T_x). t_x) t_T_list) (j - 1)))" in exI)
    apply(rule E_ProjTupleI)
     apply(force simp add: is_v_of_t_list) 
     apply(force)
    (* ? t'. (t1, t') : red *)
    apply(force dest: canon_val_lem[rule_format] intro: red.intros)
   (* TmVariant *)
   apply(force dest: canon_val_lem[rule_format] intro: red.intros)
   (* TmCase *)
   apply(rule, simp)
   apply(erule disjE)
    (* is_v_of_t ta *)
    apply(simp add: list_all_id_map)
    apply(frule_tac canon_val_lem[rule_format]) apply(assumption) 
    apply(simp)
    apply(elim exE conjE)
    apply(simp)
    apply(subgoal_tac "! xs::(label*termvar*t*T). ((\<lambda>(l, T). l) ((\<lambda>(l_x, x_x, t_x, y). (l_x, y)) xs) = (\<lambda>(l_x, x_x, t_x, y). (l_x)) xs)") prefer 2 apply(force)
    apply(simp only:) (* FIXME note these E rules are very bad for proof *)
    apply(subgoal_tac "? l_x_t_list. l_x_t_list = map (% (l,x,t,T). (l,x,t)) l_x_t_T_list") prefer 2 apply(force)
    apply(elim exE conjE)
    apply(subgoal_tac "(map (\<lambda>(l_x, x_x, t_x, T_x). CCase l_x x_x t_x) l_x_t_T_list) = (map (\<lambda>(l_x, x_x, t_x). CCase l_x x_x t_x) l_x_t_list)") prefer 2 
     apply(subgoal_tac "
       ! l_x_t_list. l_x_t_list = map (\<lambda>(l, x, t, T). (l, x, t)) l_x_t_T_list
       \<longrightarrow> (map (\<lambda>(l_x, x_x, t_x, T_x). CCase l_x x_x t_x) l_x_t_T_list =
          map (\<lambda>(l_x, x_x, t_x). CCase l_x x_x t_x) l_x_t_list)
       ") prefer 2 apply(induct_tac l_x_t_T_list) apply(force) apply(force)
     apply(force)
    apply(simp only:)
    apply(subgoal_tac "((\<lambda>(l_x, x_x, t_x, T_x). l_x) (l_x_t_T_list ! (j - Suc 0))) = ((\<lambda>(l_x, x_x, t_x). l_x) (l_x_t_list ! (j - Suc 0))) ") prefer 2 apply(force simp add: tmp.proj_compose) 
    apply(simp only: one_is_Suc_zero[symmetric])
    apply(rule_tac x="?t" in exI)
    apply(rule_tac E_CaseVariantI)
     apply(force)
     apply(force)
    (* FIXME too ugly? *)
    
    apply(subgoal_tac "? l_x_t_list. l_x_t_list = map (% (l,x,t,T). (l,x,t)) l_x_t_T_list") prefer 2 apply(force) apply(elim exE conjE)
    apply(subgoal_tac "(map (\<lambda>(l_x, x_x, t_x, T_x). CCase l_x x_x t_x) l_x_t_T_list) = (map (\<lambda>(l_x, x_x, t_x). CCase l_x x_x t_x) l_x_t_list)") prefer 2 
     apply(subgoal_tac "
       ! l_x_t_list. l_x_t_list = map (\<lambda>(l, x, t, T). (l, x, t)) l_x_t_T_list
       \<longrightarrow> (map (\<lambda>(l_x, x_x, t_x, T_x). CCase l_x x_x t_x) l_x_t_T_list =
          map (\<lambda>(l_x, x_x, t_x). CCase l_x x_x t_x) l_x_t_list)
       ") prefer 2 apply(induct_tac l_x_t_T_list) apply(force) apply(force)
     apply(force)
    apply(simp only:)
    apply(force dest: canon_val_lem[rule_format] intro: red.intros)
  done
(* FIXME too ugly *)

lemma subst_t_list_map: "subst_t_list t' x (map (\<lambda>(t_x, T_x). t_x) t_T_list) = (map (\<lambda>(t_x, T_x). t_x) (map (% (t,T). (subst_t t' x t,T)) t_T_list))"
  apply(induct t_T_list) apply(auto) done

lemma subst_C_list_map: "(subst_C_list t' x (map (\<lambda>(l_x, x_x, t_x, T_x). CCase l_x x_x t_x) l_x_t_T_list))
=
(map (\<lambda>(l_x, x_x, t_x, T_x). CCase l_x x_x t_x) (map (% (ll,xx,tt,TT). (ll,xx,(if x mem [xx] then tt else subst_t t' x tt),TT)) l_x_t_T_list))
  "
  apply(induct_tac l_x_t_T_list) 
  apply(simp)
  apply(simp)
  apply(clarsimp)
  done

lemma subst_lem: "
!G t Ty. (G, t, Ty) : typing
--> ( (*! x T1 t'.*) ((map_of G x = Some Tone) & ([], t', Tone) : typing)
--> (G, (subst_t t' x t), Ty) : typing)"
  apply(intro allI, rule) apply(erule typing.induct)
   (* 25 goals! *)
   apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   (* TmIf *)
   apply(simp) apply(intro allI impI, elim conjE) apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   (* TmVar *)
   apply(intro allI impI, elim conjE) apply(simp) apply(rule)
    apply(rule) apply(subgoal_tac "Tone = T") prefer 2 apply(elim exE conjE) apply(force simp add: map_of_append map_of  map_of.simps) apply(force intro: weakening_lem[rule_format])
    apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   (* TmCaseSm *)
   apply(force intro: typing.intros)
   apply(force intro: typing.intros)
   (* TmTuple *) (* tjr: this is a different approach from Scott, avoids nested induction *)
   apply(rule)
   apply(simp)
   apply(simp add: subst_t_list_map)
   apply(subgoal_tac "
(Ga, TmTuple (map (\<lambda>(t_x, T_x). t_x) (map (\<lambda>(t, T). (subst_t t' x t, T)) t_T_list)), TyTuple (map (\<lambda>(t_x, T_x). T_x) (map (\<lambda>(t, T). (subst_t t' x t, T)) t_T_list))) \<in> typing
     ") prefer 2 
    apply(rule typing.intros) 
    apply(simp add: list_all_map) apply(force simp: list_all_iff)
   apply(simp add: map_compose[symmetric])
   apply(subgoal_tac "
(Ga, TmTuple (map ((\<lambda>(t_x, T_x). t_x) \<circ> (\<lambda>(t, y). (subst_t t' x t, y))) t_T_list), TyTuple (map ((\<lambda>(t_x, T_x). T_x) \<circ> (\<lambda>(t, y). (subst_t t' x t, y))) t_T_list))
=
(Ga, TmTuple (map ((\<lambda>(t_x, T_x). t_x) \<circ> (\<lambda>(t, y). (subst_t t' x t, y))) t_T_list), TyTuple (map (\<lambda>(t_x, T_x). T_x) t_T_list))
     ") apply(force)
   apply(rule cong) back back back back apply(force) apply(rule cong) back back apply(rule) apply(rule map_cong) apply(rule) apply(force)   
   (* TmProjTp *)
   apply(force intro: typing.intros simp del: one_is_Suc_zero)
   (* TmVariant *)
   apply(force intro: typing.intros simp del: one_is_Suc_zero)
   (* TmCase *)
   apply(intro allI impI, elim conjE)
   apply(simp)
   apply(simp add: subst_C_list_map)
   apply(rule typing.intros)
    apply(subgoal_tac "
(map (\<lambda>(l_x, x_x, t_x, T_x). (l_x, T_x)) (map (\<lambda>(ll, xx, tt, TT). (ll, xx, if x = xx then tt else subst_t t' x tt, TT)) l_x_t_T_list))
=
(map (\<lambda>(l_x, x_x, t_x, y). (l_x, y)) l_x_t_T_list)
      ") apply(force)
    apply(simp add: map_compose[symmetric])
    apply(force)
    
    apply(simp add: map_compose[symmetric])
    apply(simp add: list_all_iff) apply(force)

    apply(simp add: map_compose[symmetric])
    apply(subgoal_tac "
((\<lambda>(l_x::label, x_x::termvar, t_x::t, T_x::T). l_x) \<circ> (\<lambda>(ll, xx, tt, TT). (ll, xx, if x = xx then tt else subst_t t' x tt, TT)))
=
(\<lambda>(l_x, x_x, t_x, T_x). l_x)
      ") apply(force)
    apply(rule ext) apply(force)
  done

lemma x_notin_fv_subst_t_x: "fv_t v = [] ==> x ~: set (fv_t (subst_t v x t))"
  apply(subgoal_tac "set (fv_t v) = {}") prefer 2 apply(force)
  apply(thin_tac "?P")
  (* P2 t \<longrightarrow> P1 (CCase list1 list2 t) 
    \<And>list. ?P3.0 list \<Longrightarrow> ?P2.0 (TmTuple list)
    \<And>t list. \<lbrakk>?P2.0 t; ?P4.0 list\<rbrakk> \<Longrightarrow> ?P2.0 (TmCase t list)
    *)
  apply(subgoal_tac "x ~: set (fv_C (subst_C v x C)) & x \<notin> set (fv_t (subst_t v x t)) & x \<notin> set (fv_t_list (subst_t_list v x list1)) & x ~: set (fv_C_list (subst_C_list v x list2))") apply(force)
  apply(rule C_t.induct[of 
    (*P2*) "(% t. x \<notin> set (fv_t (subst_t v x t)))" 
    (*P1*) "% C. x ~: set (fv_C (subst_C v x C))"
    (*P3*) "% list1. x \<notin> set (fv_t_list (subst_t_list v x list1))"
    (*P4*) "% list2. x ~: set (fv_C_list (subst_C_list v x list2))"
    ]) 
  apply(simp_all add: set_list_minus)
  apply(intro allI impI) apply(simp)
  done

lemma strengthen: "
  ([(x, T)], subst_t v2 x t12, T2) \<in> typing \<Longrightarrow> fv_t v2 = [] \<Longrightarrow> ([], subst_t v2 x t12, T2) \<in> typing"
  apply(erule_tac context_lem[rule_format]) 
  apply(subgoal_tac "xa ~= x") apply(force) 
  apply(subgoal_tac "x ~: set (fv_t (subst_t v2 x t12))") prefer 2 apply(rule x_notin_fv_subst_t_x) apply(force)
  apply(force)
  done

lemma typing_fv_t_nil: "
  ([],t,T) : typing \<Longrightarrow> fv_t t = []"
  apply(insert fv_lem)
  apply(drule_tac x="[]" in spec)
  apply(force)
  done

lemma preservation_thm: "
  !t t'. (t, t') : red --> (!Ty. ([], t, Ty) : typing --> ([], t', Ty) : typing)"
  apply(intro allI, rule)
  apply(erule red.induct)
   (* 38 subgoals! *)
   apply(force intro: typing.intros elim: typing.elims)
   apply(force intro: typing.intros elim: typing.elims)
   (* TmIf *)
   apply(intro allI impI) apply(simp) apply(force intro!: typing.intros elim: typing.elims)
   apply(force intro: typing.intros elim: typing.elims)
   apply(force intro: typing.intros elim: typing.elims)
   apply(force intro: typing.intros elim: typing.elims)
   apply(force intro: typing.intros elim: typing.elims)
   apply(force intro: typing.intros elim: typing.elims)
   apply(force intro: typing.intros elim: typing.elims)
   apply(force intro: typing.intros elim: typing.elims)
   (* TmApp *)
   apply(intro allI impI) apply(erule typing.elims) apply(simp_all) apply(elim conjE) apply(force intro: typing.intros)
   apply(intro allI impI) apply(erule typing.elims) apply(simp_all) apply(elim conjE) apply(force intro: typing.intros)
   apply(intro allI impI) 
   apply(erule typing.elims) apply(simp_all) 
   apply(erule typing.elims) apply(simp_all)
   apply(elim conjE) apply(drule_tac t=xa in sym, drule_tac t=G in sym, drule_tac t=Ga in sym, drule_tac t=T1 in sym, drule_tac t=t2a in sym) apply(simp) 
   apply(subgoal_tac "([(x,T)], subst_t v2 x t12, Ty) \<in> typing") apply(force dest: strengthen typing_fv_t_nil)
   apply(rule subst_lem[rule_format]) apply(force) apply(force)
   (* TmSeq *)
   apply(force intro: typing.intros elim: typing.elims)
   apply(force intro: typing.intros elim: typing.elims)
   apply(force intro: typing.intros elim: typing.elims)
   apply(force intro: typing.intros elim: typing.elims)
   (* TmLet *)
   apply(intro allI impI) 
   apply(erule typing.elims) apply(simp_all) 
   apply(elim conjE) apply(drule_tac t=G in sym, drule_tac t=xa in sym, drule_tac t=t1 in sym, drule_tac t=t2a in sym, drule_tac t=T2 in sym) apply(simp)
   apply(subgoal_tac "([(xa,T1)], subst_t v1 x t2, Ty) \<in> typing") apply(force dest: strengthen typing_fv_t_nil) 
   apply(rule subst_lem[rule_format]) apply(force) apply(force)

   apply(intro allI impI) 
   apply(erule typing.elims) apply(simp_all) 
   apply(force intro: typing.intros elim: typing.elims)
   (* TmProj1 *)
   apply(force intro: typing.intros elim: typing.elims)
   apply(force intro: typing.intros elim: typing.elims)
   (* TmProj1 *)
   apply(intro allI impI) apply(erule typing.elims) apply(simp_all) apply(force intro: typing.intros elim: typing.elims)
   (* TmProj2 *)
   apply(intro allI impI) apply(erule typing.elims) apply(simp_all) apply(force intro: typing.intros elim: typing.elims)
   apply(force intro: typing.intros elim: typing.elims)
   apply(force intro: typing.intros elim: typing.elims)
   (* TmCaseSm *)
   apply(intro allI impI) 
   apply(erule typing.elims) apply(simp_all) 
   apply(elim conjE) apply(drule_tac t=G in sym, drule_tac t=t0 in sym, drule_tac t=x1a in sym, drule_tac t=t1a in sym, drule_tac t=x2a in sym, drule_tac t=t2a in sym) apply(simp) 
   apply(subgoal_tac "([(x1,T1)], subst_t v0 x1 t1, T) \<in> typing") apply(force dest: strengthen typing_fv_t_nil)
   apply(rule subst_lem[rule_format]) apply(force) apply(rule, force) apply(erule typing.elims) apply(simp_all) (* solves goal *)

   apply(intro allI impI) 
   apply(erule typing.elims) apply(simp_all) 
   apply(elim conjE) apply(drule_tac t=G in sym, drule_tac t=t0 in sym, drule_tac t=x1a in sym, drule_tac t=t1a in sym, drule_tac t=x2a in sym, drule_tac t=t2a in sym) apply(simp) 
   apply(subgoal_tac "([(x2,T2)], subst_t v0 x2 t2, T) \<in> typing") apply(force dest: strengthen typing_fv_t_nil) 
   apply(rule subst_lem[rule_format]) apply(force) apply(rule, force) apply(erule typing.elims) apply(simp_all) (* solves goal *)

   apply(force intro: typing.intros elim: typing.elims)
   apply(force intro: typing.intros elim: typing.elims)
   apply(force intro: typing.intros elim: typing.elims)
   (* TmFix *)
   apply(intro allI impI)
   apply(frule P_imp_P)
   apply(erule typing.elims, simp_all)
   apply(erule typing.elims) back apply(simp_all)
   apply(elim conjE) apply(drule_tac t=G in sym, drule_tac t=Ga in sym, drule_tac t=xa in sym, drule_tac t=T1b in sym, drule_tac t=t2a in sym, drule_tac t=T1b in sym) apply(simp)
   apply(subgoal_tac "([(x,T1)], subst_t (TmFix (TmAbs x T1 t2)) x t2, T1) \<in> typing") apply(force dest: strengthen typing_fv_t_nil)
   apply(rule subst_lem[rule_format]) apply(force) apply(rule, force) apply(force)

   apply(force intro: typing.intros elim: typing.elims)   
   (* TmProjTp *)
   apply(intro allI impI) apply(erule typing.elims, simp_all) apply(elim conjE) apply(clarsimp)
   apply(erule typing.elims, simp_all) apply(elim conjE) apply(clarsimp)
   apply(simp add: list_all_id_map) 
   apply(case_tac "(t_T_list ! (ja - Suc 0))") apply(rename_tac t T)
   apply(simp) apply(simp add: list_all_iff) apply(drule_tac x="(t,T)" in bspec) back apply(drule_tac t="(t,T)" in sym) apply(force simp: nth_mem)
   apply(force)
   (* TmProjTp *)
   apply(force intro: typing.intros elim: typing.elims)
   (* TmTuple *)
   apply(intro allI impI)
   apply(erule typing.elims, simp_all) apply(elim conjE) apply(simp add: list_all_id_map)
   (* probably want to prove a lemma about if one elt in a list reduces, then the types are preserved\<dots> *)
   apply(drule_tac tmp.tmp[rule_format]) apply(elim exE) apply(simp del: zip_append)
   apply(subgoal_tac "
     (map (\<lambda>(t_x, T_x). T_x) (zip (v_list @ ta # t_list) (T_v_list @ T_ta # T_t_list)))
     = (map (\<lambda>(t_x, T_x). T_x) (zip (v_list @ t'a # t_list) (T_v_list @ T_ta # T_t_list)))") prefer 2 apply(force) apply(simp del: zip_append)
   apply(subgoal_tac "v_list @ t'a # t_list = (map (\<lambda>(t_x, T_x). t_x) (zip (v_list @ t'a # t_list) (T_v_list @ T_ta # T_t_list)))") prefer 2
    apply(subgoal_tac "(\<lambda>((t_x::t), (T_x::T)). t_x) = fst") prefer 2 apply(force intro: ext)
    apply(rule sym) apply(simp only:) apply(force simp: map_fst_zip)
   apply(drule_tac t="v_list @ t'a # t_list" in ssubst) prefer 2 apply(assumption) back back (* hack around simplifier *)
   apply(rule typing.intros) apply(force simp: list_all_id_map) 
   (* TmCase *)
   apply(intro allI impI) apply(erule typing.elims, simp_all) (* something funny may be happening- this goal was solved outright at some point *) 
   apply(clarsimp) apply(simp add: list_all_id_map)
   apply(subgoal_tac "l_x_t_list = map (% (l,x,t,T). (l,x,t)) l_x_t_T_list") prefer 2 
    apply(subgoal_tac "! l_x_t_list.        
      map (\<lambda>(l_x, x, y). CCase l_x x y) l_x_t_list =
        map (\<lambda>(l_x, x_x, t_x, T_x). CCase l_x x_x t_x) l_x_t_T_list
\<longrightarrow> l_x_t_list = map (% (l,x,t,T). (l,x,t)) l_x_t_T_list") prefer 2 apply(rule list.induct) back apply(force) apply(force)
    apply(force)
   apply(simp) (* apply(thin_tac "l_x_t_list = ?P") *)
   apply(simp only: tmp.proj_compose[rule_format])
   apply(subgoal_tac "? xs ys z. l_x_t_T_list = xs@z#ys & (j - Suc 0) = length xs") prefer 2
    apply(subgoal_tac "! j. Suc 0 <= j & j <= length l_x_t_T_list \<longrightarrow> 
(\<exists>xs ys z. l_x_t_T_list = xs @ z # ys \<and> j - Suc 0 = length xs)") prefer 2
     apply(rule list.induct) apply(force) apply(intro allI impI) apply(case_tac ja) apply(force) apply(case_tac nat) apply(force) apply(drule_tac x=nat in spec) apply(erule impE) apply(force) apply(elim exE conjE) apply(rule_tac x="a#xs" in exI) apply(force) 
    apply(force)
   apply(elim exE conjE)
   apply(simp add: nth_append_length) apply(simp add: split_paired_all) apply(rename_tac l x t T)
   apply(subgoal_tac "([(x,T)],subst_t v x t, Taa) \<in> typing ") apply(force dest: strengthen typing_fv_t_nil)
   apply(rule_tac Tone=T in subst_lem[rule_format]) apply(force) apply(rule) apply(force) 
   apply(erule typing.elims, simp_all) 
   apply(elim conjE) apply(drule_tac s=l in sym) apply(drule_tac s=v in sym) apply(drule_tac s="[]" in sym) apply(drule_tac t="l_T_list" in sym)
   apply(simp)
   apply(subgoal_tac "ja = j") prefer 2
    apply(subgoal_tac "
      (\<lambda>(l_x, T_x). l_x) ((map (\<lambda>(l_x, x_x, t_x, y). (l_x, y)) xs @ (l, T) # map (\<lambda>(l_x, x_x, t_x, y). (l_x, y)) ys) ! (ja - Suc 0)) = l
      & l \<notin> (\<lambda>(l_x, x_x, t_x, T_x). l_x) ` set ys
      & l \<notin> (\<lambda>(l_x, x_x, t_x, T_x). l_x) ` set xs
      ") prefer 2 apply(force)
    apply(subgoal_tac "ja - Suc 0 = length xs") apply(force)
    apply(subgoal_tac "ja - Suc 0 < length xs | ja - Suc 0 = length xs | length xs < ja - Suc 0") prefer 2 apply(arith)
    apply(elim disjE) 
     apply(simp add: nth_append) apply(subgoal_tac "l : (\<lambda>(l_x, T_x). l_x) ` ((\<lambda>(l_x, x_x, t_x, y). (l_x, y)) ` (set xs))") prefer 2 apply(force) apply(force)
     apply(force)
     apply(simp add: nth_append)
     apply(case_tac "(ja - Suc (length xs))") apply(force)
     apply(subgoal_tac "l : (\<lambda>(l_x, T_x). l_x) ` ((\<lambda>(l_x, x_x, t_x, y). (l_x, y)) ` (set ys))") prefer 2 apply(force) 
     apply(elim conjE)
     apply(erule_tac P="l : ?P" in rev_mp) apply(erule_tac P="l ~: ?P" in rev_mp) (* hack to remove unnecessary asms *)
     apply(thin_tac "?P")+ apply(force)
   apply(simp)
   apply(subgoal_tac "length xs = length (map (\<lambda>(l, x, t, T). (l, T)) xs)") prefer 2 apply(simp add: length_map)
   apply(simp add: nth_append_length del: length_map)
   (* FIXME this is too ugly *)
   (* TmCase *)
   apply(force intro: typing.intros elim: typing.elims)
   apply(force intro: typing.intros elim: typing.elims)
  done

end