Theory SyntaxL

(*<*)
theory SyntaxL
  imports Syntax IVSubst
begin
  (*>*)

chapter ‹Syntax Lemmas›

section ‹Support, lookup and contexts›

lemma supp_v_tau [simp]:
  assumes "atom z ♯ v"
  shows "supp (⦃ z : b | CE_val (V_var z)  ==  CE_val v  ⦄) = supp v ∪ supp b" 
  using assms τ.supp c.supp ce.supp 
  by (simp add: fresh_def supp_at_base)

lemma supp_v_var_tau [simp]:
  assumes "z ≠ x"
  shows  "supp (⦃ z : b | CE_val (V_var z)  ==  CE_val (V_var x)  ⦄) = { atom x } ∪ supp b"
  using supp_v_tau assms
  using supp_at_base by fastforce

text ‹ Sometimes we need to work with a version of a binder where the variable is fresh 
in something else, such as  a bigger context. I think these could be generated automatically ›

lemma obtain_fresh_fun_def:
  fixes t::"'b::fs" 
  shows  "∃y::x. atom y ♯ (s,c,τ,t) ∧ (AF_fundef f (AF_fun_typ_none (AF_fun_typ x b c τ s))  = AF_fundef f (AF_fun_typ_none (AF_fun_typ y b ((y ↔ x) ∙ c ) ((y ↔ x) ∙ τ) ((y ↔ x) ∙ s))))"
proof -
  obtain y::x where y: "atom y ♯ (s,c,τ,t)" using obtain_fresh by blast
  moreover have "AF_fundef f (AF_fun_typ_none (AF_fun_typ y b ((y ↔ x) ∙ c ) ((y ↔ x) ∙ τ) ((y ↔ x) ∙ s))) =  (AF_fundef f (AF_fun_typ_none (AF_fun_typ  x b c τ s)))" 
  proof(cases "x=y")
    case True
    then show ?thesis  using fun_def.eq_iff Abs1_eq_iff(3)  flip_commute flip_fresh_fresh fresh_PairD by auto
  next
    case False

    have  "(AF_fun_typ y b ((y ↔ x) ∙ c) ((y ↔ x) ∙ τ) ((y ↔ x) ∙ s)) =(AF_fun_typ x b c τ s)" proof(subst fun_typ.eq_iff, subst Abs1_eq_iff(3))
      show  ‹(y = x ∧ (((y ↔ x) ∙ c, (y ↔ x) ∙ τ), (y ↔ x) ∙ s) = ((c, τ), s) ∨
         y ≠ x ∧ (((y ↔ x) ∙ c, (y ↔ x) ∙ τ), (y ↔ x) ∙ s) = (y ↔ x) ∙ ((c, τ), s) ∧ atom y ♯ ((c, τ), s)) ∧
         b = b› using False flip_commute flip_fresh_fresh fresh_PairD y by auto
    qed
    thus ?thesis by metis
  qed
  ultimately show  ?thesis using y fresh_Pair by metis
qed

lemma lookup_fun_member:
  assumes "Some (AF_fundef f ft) = lookup_fun Φ f"
  shows "AF_fundef f ft ∈ set Φ"
  using assms proof (induct Φ)
  case Nil
  then show ?case by auto
next
  case (Cons a Φ)
  then show ?case using lookup_fun.simps
    by (metis fun_def.exhaust insert_iff list.simps(15) option.inject)
qed

lemma rig_dom_eq:
  "dom (G[x ⟼ c]) = dom G"
proof(induct G rule: Γ.induct)
  case GNil
  then show ?case using replace_in_g.simps by presburger
next
  case (GCons xbc Γ')
  obtain x' and b' and c' where xbc: "xbc=(x',b',c')" using prod_cases3 by blast
  then show ?case using replace_in_g.simps GCons by simp
qed

lemma lookup_in_rig_eq:
  assumes "Some (b,c) = lookup Γ x" 
  shows "Some (b,c') = lookup (Γ[x⟼c']) x"
  using assms proof(induct Γ rule: Γ_induct)
  case GNil
  then show ?case by auto
next
  case (GCons x b c Γ')
  then show ?case using replace_in_g.simps lookup.simps by auto
qed

lemma lookup_in_rig_neq:
  assumes "Some (b,c) = lookup Γ y" and "x≠y"
  shows "Some (b,c) = lookup (Γ[x⟼c']) y"
  using assms proof(induct Γ rule: Γ_induct)
  case GNil
  then show ?case by auto
next
  case (GCons x' b' c' Γ')
  then show ?case using replace_in_g.simps lookup.simps by auto
qed

lemma lookup_in_rig:
  assumes "Some (b,c) = lookup Γ y" 
  shows "∃c''. Some (b,c'') = lookup (Γ[x⟼c']) y"
proof(cases "x=y")
  case True
  then show ?thesis using lookup_in_rig_eq using assms by blast
next
  case False
  then show ?thesis using lookup_in_rig_neq using assms by blast
qed

lemma lookup_inside[simp]:
  assumes "x ∉ fst ` toSet Γ'"
  shows "Some (b1,c1) = lookup (Γ'@(x,b1,c1)#⇩ΓΓ) x"
  using assms by(induct Γ',auto)

lemma lookup_inside2:
  assumes "Some (b1,c1) = lookup (Γ'@((x,b0,c0)#⇩ΓΓ)) y" and "x≠y"
  shows "Some (b1,c1) = lookup (Γ'@((x,b0,c0')#⇩ΓΓ)) y" 
  using assms by(induct Γ' rule: Γ.induct,auto+)

fun tail:: "'a list ⇒ 'a list" where
  "tail [] = []"
| "tail (x#xs) = xs"

lemma lookup_options:
  assumes "Some (b,c) = lookup (xt#⇩ΓG) x"
  shows  "((x,b,c) = xt) ∨ (Some (b,c) = lookup G x)"
  by (metis assms lookup.simps(2) option.inject surj_pair)

lemma lookup_x:
  assumes "Some (b,c) = lookup G x"
  shows "x ∈ fst ` toSet G"
  using assms
  by(induct "G" rule: Γ.induct ,auto+)

lemma GCons_eq_appendI:
  fixes xs1::Γ
  shows "[| x #⇩Γ xs1 = ys; xs = xs1 @ zs |] ==> x #⇩Γ xs = ys @ zs"
  by (drule sym) simp

lemma split_G: "x : toSet xs ⟹ ∃ys zs. xs = ys @ x #⇩Γ zs"
proof (induct xs)
  case GNil thus ?case by simp
next
  case GCons thus ?case using  GCons_eq_appendI 
    by (metis Un_iff append_g.simps(1) singletonD toSet.simps(2))
qed

lemma lookup_not_empty:
  assumes "Some τ = lookup G x"
  shows "G ≠ GNil"
  using assms by auto

lemma lookup_in_g:
  assumes "Some (b,c) = lookup Γ x"
  shows "(x,b,c) ∈ toSet Γ"
  using assms apply(induct Γ, simp)
  using lookup_options by fastforce

lemma lookup_split:
  fixes Γ::Γ
  assumes "Some (b,c) = lookup Γ x"
  shows "∃G G' . Γ =  G'@(x,b,c)#⇩ΓG"
  by (meson assms(1) lookup_in_g split_G)

lemma toSet_splitU[simp]:
  "(x',b',c') ∈ toSet (Γ' @ (x, b, c) #⇩Γ Γ) ⟷ (x',b',c') ∈ (toSet Γ' ∪ {(x, b, c)} ∪ toSet Γ)"
  using append_g_toSetU toSet.simps by auto

lemma toSet_splitP[simp]:
  "(∀(x', b', c')∈toSet (Γ' @ (x, b, c) #⇩Γ Γ). P x' b' c') ⟷ (∀ (x', b', c')∈toSet Γ'. P x' b' c') ∧ P x b c ∧ (∀ (x', b', c')∈toSet Γ. P x' b' c')"  (is "?A ⟷ ?B")
  using toSet_splitU by force

lemma lookup_restrict:
  assumes "Some (b',c') = lookup (Γ'@(x,b,c)#⇩ΓΓ) y" and "x ≠ y" 
  shows "Some (b',c') = lookup (Γ'@Γ) y"
  using assms  proof(induct Γ' rule:Γ_induct)
  case GNil
  then show ?case by auto
next
  case (GCons x1 b1 c1 Γ')
  then show ?case by auto
qed

lemma supp_list_member:
  fixes x::"'a::fs" and l::"'a list"
  assumes "x ∈ set l"
  shows "supp x ⊆ supp l"
  using assms apply(induct l, auto)
  using supp_Cons by auto

lemma GNil_append:
  assumes "GNil = G1@G2"
  shows "G1 = GNil ∧ G2 = GNil"
proof(rule ccontr)
  assume "¬ (G1 = GNil ∧ G2 = GNil)"
  hence "G1@G2 ≠ GNil" using append_g.simps   by (metis Γ.distinct(1) Γ.exhaust)
  thus False using assms by auto
qed

lemma GCons_eq_append_conv:
  fixes xs::Γ
  shows "x#⇩Γxs = ys@zs = (ys = GNil ∧ x#⇩Γxs = zs ∨ (∃ys'. x#⇩Γys' = ys ∧ xs = ys'@zs))"
  by(cases ys) auto

lemma dclist_distinct_unique:
  assumes  "(dc, const) ∈ set dclist2" and  "(cons, const1) ∈ set dclist2" and "dc=cons" and  "distinct (List.map fst dclist2)"
  shows "(const) = const1"
proof -
  have  "(cons, const) = (dc, const1)" 
    using assms     by (metis (no_types, lifting) assms(3) assms(4) distinct.simps(1) distinct.simps(2) empty_iff insert_iff list.set(1) list.simps(15) list.simps(8) list.simps(9) map_of_eq_Some_iff)
  thus ?thesis by auto
qed

lemma fresh_d_fst_d:
  assumes "atom u ♯ δ"
  shows  "u ∉ fst ` set δ"
  using assms proof(induct δ)
  case Nil
  then show ?case by auto
next
  case (Cons ut δ')
  obtain u' and t' where *:"ut = (u',t') " by fastforce
  hence "atom u ♯ ut ∧ atom u ♯ δ'" using fresh_Cons Cons by auto
  moreover hence "atom u ♯ fst ut" using * fresh_Pair[of "atom u" u' t'] Cons by auto
  ultimately show ?case using Cons by auto
qed

lemma bv_not_in_bset_supp:
  fixes bv::bv
  assumes "bv |∉| B"
  shows "atom bv ∉ supp B"
proof - 
  have *:"supp B = fset (fimage atom B)"
    by (metis fimage.rep_eq finite_fset supp_finite_set_at_base supp_fset)
  thus ?thesis using assms 
    by fastforce
qed

lemma u_fresh_d:
  assumes "atom u ♯ D"
  shows "u ∉ fst ` setD D"
  using assms proof(induct D rule: Δ_induct)
  case DNil
  then show ?case by auto
next
  case (DCons u' t' Δ')
  then show ?case unfolding setD.simps 
    using fresh_DCons fresh_Pair  by (simp add: fresh_Pair fresh_at_base(2))
qed

section ‹Type Definitions›

lemma exist_fresh_bv:
  fixes tm::"'a::fs"
  shows  "∃bva2 dclist2. AF_typedef_poly tyid bva dclist = AF_typedef_poly tyid bva2 dclist2 ∧ 
             atom bva2 ♯ tm" 
proof -
  obtain bva2::bv where *:"atom bva2 ♯ (bva, dclist,tyid,tm)" using obtain_fresh by metis
  moreover hence "bva2 ≠ bva" using fresh_at_base by auto
  moreover have " dclist = (bva ↔ bva2) ∙ (bva2 ↔ bva) ∙ dclist" by simp
  moreover have "atom bva ♯ (bva2 ↔ bva) ∙ dclist" proof -
    have "atom bva2 ♯ dclist" using * fresh_prodN by auto
    hence "atom ((bva2 ↔ bva) ∙ bva2) ♯ (bva2 ↔ bva) ∙ dclist" using fresh_eqvt True_eqvt 
    proof -
      have "(bva2 ↔ bva) ∙ atom bva2 ♯ (bva2 ↔ bva) ∙ dclist"
        by (metis True_eqvt ‹atom bva2 ♯ dclist› fresh_eqvt) (* 62 ms *)
      then show ?thesis
        by simp (* 125 ms *)
    qed
    thus ?thesis by auto
  qed
  ultimately have "AF_typedef_poly tyid bva dclist = AF_typedef_poly tyid bva2 ((bva2 ↔ bva ) ∙ dclist)"    
    unfolding type_def.eq_iff   Abs1_eq_iff by metis
  thus ?thesis using * fresh_prodN by metis
qed

lemma obtain_fresh_bv:
  fixes tm::"'a::fs"
  obtains bva2::bv and  dclist2 where "AF_typedef_poly tyid bva dclist = AF_typedef_poly tyid bva2 dclist2 ∧ 
             atom bva2 ♯ tm" 
  using exist_fresh_bv by metis

section ‹Function Definitions›

lemma fun_typ_flip:
  fixes bv1::bv and c::bv
  shows   "(bv1 ↔ c) ∙ AF_fun_typ x1 b1 c1 τ1 s1 = AF_fun_typ x1 ((bv1 ↔ c) ∙ b1) ((bv1 ↔ c) ∙ c1) ((bv1 ↔ c) ∙ τ1) ((bv1 ↔ c) ∙ s1)"
  using fun_typ.perm_simps flip_fresh_fresh supp_at_base  fresh_def
    flip_fresh_fresh fresh_def supp_at_base 
  by (simp add: flip_fresh_fresh)

lemma fun_def_eq:
  assumes  "AF_fundef fa (AF_fun_typ_none (AF_fun_typ xa ba ca τa sa)) = AF_fundef f (AF_fun_typ_none (AF_fun_typ x b c τ s))"
  shows "f = fa" and "b = ba" and "[[atom xa]]lst. sa = [[atom x]]lst. s" and "[[atom xa]]lst. τa = [[atom x]]lst. τ" and
    " [[atom xa]]lst. ca = [[atom x]]lst. c"
  using fun_def.eq_iff fun_typ_q.eq_iff fun_typ.eq_iff lst_snd lst_fst  using assms apply metis
  using fun_def.eq_iff fun_typ_q.eq_iff fun_typ.eq_iff lst_snd lst_fst  using assms apply metis
proof - 
  have "([[atom xa]]lst. ((ca, τa), sa) = [[atom x]]lst. ((c, τ), s))" using assms  fun_def.eq_iff fun_typ_q.eq_iff  fun_typ.eq_iff by auto
  thus "[[atom xa]]lst. sa = [[atom x]]lst. s" and "[[atom xa]]lst. τa = [[atom x]]lst. τ" and
    " [[atom xa]]lst. ca = [[atom x]]lst. c" using lst_snd lst_fst by metis+
qed

lemma fun_arg_unique_aux: 
  assumes "AF_fun_typ x1 b1 c1 τ1' s1' = AF_fun_typ x2 b2 c2 τ2' s2'"
  shows "⦃ x1 : b1 | c1 ⦄ = ⦃ x2 : b2 | c2⦄"
proof - 
  have " ([[atom x1]]lst. c1 = [[atom x2]]lst. c2)" using fun_def_eq assms by metis
  moreover have "b1 = b2" using fun_typ.eq_iff assms  by metis
  ultimately show ?thesis using τ.eq_iff by fast
qed

lemma fresh_x_neq:
  fixes x::x and y::x
  shows "atom x ♯ y = (x ≠ y)"
  using fresh_at_base  fresh_def by auto

lemma obtain_fresh_z3:
  fixes tm::"'b::fs"
  obtains z::x where "⦃ x : b  | c ⦄ =  ⦃ z : b  | c[x::=V_var z]⇩c⇩v ⦄ ∧  atom z ♯ tm ∧ atom z ♯ (x,c)" 
proof -
  obtain z::x and c'::c where z:"⦃ x : b  | c ⦄ =  ⦃ z : b | c' ⦄ ∧  atom z ♯ (tm,x,c)" using obtain_fresh_z2 b_of.simps by metis
  hence "c' = c[x::=V_var z]⇩c⇩v" proof - 
    have "([[atom z]]lst. c' = [[atom x]]lst. c)" using z τ.eq_iff by metis
    hence "c' = (z ↔ x) ∙ c" using Abs1_eq_iff[of z c' x c]  fresh_x_neq  fresh_prodN by fastforce
    also have "... = c[x::=V_var z]⇩c⇩v"
      using subst_v_c_def  flip_subst_v[of z c x] z fresh_prod3 by metis
    finally show ?thesis by auto
  qed
  thus ?thesis using z fresh_prodN that by metis
qed

lemma u_fresh_v:
  fixes u::u and t::v
  shows "atom u ♯ t" 
  by(nominal_induct t rule:v.strong_induct,auto)

lemma u_fresh_ce:
  fixes u::u and t::ce
  shows "atom u ♯ t" 
  apply(nominal_induct t rule:ce.strong_induct)
  using  u_fresh_v pure_fresh 
       apply (auto simp add:  opp.fresh ce.fresh opp.fresh opp.exhaust)
  unfolding ce.fresh opp.fresh opp.exhaust  by (simp add: fresh_opp_all)

lemma u_fresh_c:
  fixes u::u and t::c
  shows "atom u ♯ t" 
  by(nominal_induct t rule:c.strong_induct,auto simp add: c.fresh u_fresh_ce)

lemma u_fresh_g:
  fixes u::u and t::Γ
  shows "atom u ♯ t" 
  by(induct t rule:Γ_induct, auto simp add: u_fresh_b u_fresh_c  fresh_GCons fresh_GNil)

lemma u_fresh_t:
  fixes u::u and t::τ
  shows "atom u ♯ t" 
  by(nominal_induct t rule:τ.strong_induct,auto simp add: τ.fresh u_fresh_c u_fresh_b)

lemma b_of_c_of_eq:
  assumes "atom z ♯ τ" 
  shows "⦃ z : b_of τ |  c_of τ z ⦄ = τ" 
  using assms proof(nominal_induct τ avoiding: z rule: τ.strong_induct)
  case (T_refined_type x1a x2a x3a)

  hence " ⦃ z : b_of ⦃ x1a : x2a  | x3a ⦄  | c_of ⦃ x1a : x2a  | x3a ⦄ z ⦄ = ⦃ z : x2a | x3a[x1a::=V_var z]⇩c⇩v ⦄" 
    using b_of.simps c_of.simps c_of_eq by auto
  moreover have "⦃ z : x2a | x3a[x1a::=V_var z]⇩c⇩v ⦄ = ⦃ x1a : x2a  | x3a ⦄" using T_refined_type τ.fresh by auto
  ultimately show  ?case by auto
qed

lemma fresh_d_not_in:
  assumes "atom u2 ♯ Δ'" 
  shows   "u2 ∉ fst ` setD Δ'" 
  using assms proof(induct Δ' rule: Δ_induct)
  case DNil
  then show ?case by simp
next
  case (DCons u t Δ')
  hence *: "atom u2 ♯ Δ' ∧ atom u2 ♯ (u,t)" 
    by (simp add: fresh_def supp_DCons)
  hence "u2 ∉ fst ` setD Δ'" using DCons by auto
  moreover have "u2 ≠ u" using * fresh_Pair 
    by (metis eq_fst_iff not_self_fresh)
  ultimately  show ?case by simp
qed

end