Theory SubstMethods

theory SubstMethods
  (* Its seems that it's best to load the Eisbach tools last *)
  imports  IVSubst WellformedL "HOL-Eisbach.Eisbach_Tools" 
begin

text ‹
 See Eisbach/Examples.thy as well as Eisbach User Manual.

Freshness for various substitution situations. It seems that if undirected and we throw all the 
facts at them to try to solve in one shot, the automatic methods are *sometimes*  unable
to handle the different variants, so some guidance is needed. 
First we split into subgoals using fresh\_prodN and intro conjI

The 'add', for example, will be induction premises that will contain freshness facts or freshness conditions from
prior obtains

Use different arguments for different things or just lump into one bucket›

method fresh_subst_mth_aux uses add = (
    (match conclusion in  "atom z ♯ (Γ::Γ)[x::=v]Γv" for z x v Γ  ⇒ ‹auto simp add: fresh_subst_gv_if[of "atom z" Γ v x] add›)
  | (match conclusion in  "atom z ♯ (v'::v)[x::=v]vv" for z x v v' ⇒ ‹auto simp add: v.fresh fresh_subst_v_if pure_fresh subst_v_v_def  add› )
  | (match conclusion in  "atom z ♯ (ce::ce)[x::=v]cev" for z x v ce ⇒ ‹auto simp add: fresh_subst_v_if subst_v_ce_def  add› )
  | (match conclusion in  "atom z ♯ (Δ::Δ)[x::=v]Δv" for z x v Δ ⇒ ‹auto simp add: fresh_subst_v_if fresh_subst_dv_if  add› )
  | (match conclusion in  "atom z ♯ Γ'[x::=v]Γv @ Γ" for z x v Γ' Γ ⇒ ‹metis  add › )
  | (match conclusion in  "atom z ♯ (τ::τ)[x::=v]τv" for z x v τ ⇒ ‹auto simp add: v.fresh fresh_subst_v_if pure_fresh subst_v_τ_def  add› )
  | (match conclusion in  "atom z ♯ ({||} :: bv fset)" for z  ⇒ ‹auto simp add: fresh_empty_fset›)
    (* tbc delta and types *)
  | (auto simp add: add x_fresh_b pure_fresh) (* Cases where there is no subst and so can most likely get what we want from induction premises *)
    )

method fresh_mth uses add = (
    (unfold fresh_prodN, intro conjI)?,
    (fresh_subst_mth_aux add: add)+)


notepad
begin
  fix Γ::Γ and z::x and x::x and v::v and Θ::Θ and v'::v and w::x and tyid::string and dc::string and b::b and ce::ce and bv::bv

  assume as:"atom z ♯ (Γ,v',Θ, v,w,ce) ∧ atom bv ♯  (Γ,v',Θ, v,w,ce,b) "

  have "atom z ♯ Γ[x::=v]Γv" 
    by (fresh_mth add: as)

  hence "atom z ♯ v'[x::=v]vv" 
    by (fresh_mth add: as)

  hence "atom z ♯ Γ" 
    by (fresh_mth add: as)

  hence "atom z ♯ Θ" 
    by (fresh_mth add: as)

  hence "atom z ♯  (CE_val v == ce)[x::=v]cv"
    using as by auto

  hence "atom bv ♯  (CE_val v == ce)[x::=v]cv"
    using as by auto

  have "atom z ♯ (Θ,Γ[x::=v]Γv,v'[x::=v]vv,w, V_pair v v, V_consp tyid dc b v, (CE_val v == ce)[x::=v]cv) " 
    by (fresh_mth add: as)

  have "atom bv ♯ (Θ,Γ[x::=v]Γv,v'[x::=v]vv,w, V_pair v v, V_consp tyid dc b v) " 
    by (fresh_mth add: as)

end




end