Quelle  Wellformed.thy

(*<*)
theory Wellformed
  imports  IVSubst BTVSubst
begin
  (*>*)

chapter ‹Wellformed Terms›

text ‹We require that expressions and values are well-formed. This includes a notion
  well-sortedness. We identify a sort with a basic type and
  the judgement as two clusters of mutually recursive
  predicates. Some of the proofs are across all of the predicates and
  they seemed at first to be daunting, they have all
  out well.›

named_theorems ms_wb "Facts for helping with well-sortedness"

section ‹Definitions›

inductive wfV :: "Θ ==> B ==> Γ ==> v ==> b ==> bool" (‹ _ ; _ ; _ ⊨_wf _ : _ › [50,50,50] 50)  and
  wfC :: "Θ ==> B ==> Γ ==> c ==> bool" (‹ _ ; _ ; _ ⊨_wf _ › [50,50] 50)  and         
  wfG :: "Θ ==> B ==> Γ ==> bool" (‹ _ ; _ ⊨_wf _ › [50,50] 50) and
  wfT :: "Θ ==> B ==> Γ ==> τ ==> bool" (‹ _ ; _ ; _ ⊨_wf _ › [50,50] 50)  and
  wfTs :: "Θ ==> B ==> Γ ==> (string*τ) list ==> bool" (‹ _ ; _ ; _ ⊨_wf _ › [50,50] 50)  and 
  wfTh :: "Θ ==> bool" (‹ ⊨_wf _ › [50] 50)  and
  wfB :: "Θ ==> B ==> b ==> bool" (‹ _ ; _ ⊨_wf _ › [50,50] 50) and
  wfCE :: "Θ ==> B ==> Γ ==> ce ==> b ==> bool" (‹ _ ; _ ; _ ⊨_wf _ : _ › [50,50,50] 50) and
  wfTD :: "Θ ==> type_def ==> bool" (‹ _ ⊨_wf _ › [50,50] 50)          
  where

wfB_intI:  "⊨_wf Θ ==> Θ; B ⊨_wf B_int" 
| wfB_boolI:  "⊨_wf Θ ==> Θ; B ⊨_wf B_bool" 
| wfB_unitI:  "⊨_wf Θ ==> Θ; B ⊨_wf B_unit" 
| wfB_bitvecI:  "⊨_wf Θ ==> Θ; B ⊨_wf B_bitvec" 
| wfB_pairI:  "[ Θ; B ⊨_wf b1 ; Θ; B ⊨_wf b2 ] ==> Θ; B ⊨_wf B_pair b1 b2" 

| wfB_consI:  "[
   ⊨_wf Θ;
   (AF_typedef s dclist) ∈ set Θ
\<rbrakk> ==>
   Θ; B ⊨_wf B_id s"

| wfB_appI:  "[
   ⊨_wf Θ;
   Θ; B ⊨_wf b;
   (AF_typedef_poly s bv dclist) ∈ set Θ
\<rbrakk> ==>
   Θ; B ⊨_wf B_app s b"

| wfV_varI: "[ Θ; B ⊨_wf Γ ; Some (b,c) = lookup Γ x ] ==> Θ; B; Γ ⊨_wf V_var x : b"
| wfV_litI: "Θ; B ⊨_wf Γ ==> Θ; B; Γ ⊨_wf V_lit l : base_for_lit l"

| wfV_pairI: "[
   Θ; B; Γ ⊨_wf v1 : b1 ;
   Θ; B; Γ ⊨_wf v2 : b2
\<rbrakk> ==>
   Θ; B; Γ ⊨_wf (V_pair v1 v2) : B_pair b1 b2"

| wfV_consI: "[
   AF_typedef s dclist ∈ set Θ;
   (dc, { x : b' | c }) ∈ set dclist ;
   Θ; B; Γ ⊨_wf v : b'
\<rbrakk> ==>
   Θ; B; Γ ⊨_wf V_cons s dc v : B_id s"

| wfV_conspI: "[
    AF_typedef_poly s bv dclist ∈ set Θ;
    (dc, { x : b' | c }) ∈ set dclist ;
    Θ ; B ⊨_wf b;
    atom bv ♯ (Θ, B, Γ, b , v);
    Θ; B; Γ ⊨_wf v : b'[bv::=b]_bb
\<rbrakk> ==>
    Θ; B; Γ ⊨_wf V_consp s dc b v : B_app s b"

| wfCE_valI : "[
    Θ; B; Γ ⊨_wf v : b
\<rbrakk> ==>
    Θ; B; Γ ⊨_wf CE_val v : b"

| wfCE_plusI: "[
    Θ; B; Γ ⊨_wf v1 : B_int;
    Θ; B; Γ ⊨_wf v2 : B_int
\<rbrakk> ==>
    Θ; B; Γ ⊨_wf CE_op Plus v1 v2 : B_int"

| wfCE_leqI:"[
    Θ; B; Γ ⊨_wf v1 : B_int;
    Θ; B; Γ ⊨_wf v2 : B_int
\<rbrakk> ==>
    Θ; B; Γ ⊨_wf CE_op LEq v1 v2 : B_bool"

| wfCE_eqI:"[
    Θ; B; Γ ⊨_wf v1 : b;
    Θ; B; Γ ⊨_wf v2 : b
\<rbrakk> ==>
    Θ; B; Γ ⊨_wf CE_op Eq v1 v2 : B_bool"

| wfCE_fstI: "[
    Θ; B; Γ ⊨_wf v1 : B_pair b1 b2
\<rbrakk> ==>
    Θ; B; Γ ⊨_wf CE_fst v1 : b1"

| wfCE_sndI: "[
    Θ; B; Γ ⊨_wf v1 : B_pair b1 b2
\<rbrakk> ==>
    Θ; B; Γ ⊨_wf CE_snd v1 : b2"

| wfCE_concatI: "[
    Θ; B; Γ ⊨_wf v1 : B_bitvec ;
    Θ; B; Γ ⊨_wf v2 : B_bitvec
\<rbrakk> ==>
    Θ; B; Γ ⊨_wf CE_concat v1 v2 : B_bitvec"

| wfCE_lenI: "[
    Θ; B; Γ ⊨_wf v1 : B_bitvec
\<rbrakk> ==>
    Θ; B; Γ ⊨_wf CE_len v1 : B_int"

| wfTI : "[
    atom z ♯ (Θ, B, Γ) ;
    Θ; B ⊨_wf b;
    Θ; B ; (z,b,C_true) #_\<Gamma> Γ ⊨_wf c
\<rbrakk> ==>
    Θ; B; Γ ⊨_wf { z : b | c }"

| wfC_eqI: "[
                Θ; B; Γ ⊨_wf e1 : b ;
                 Θ; B; Γ ⊨_wf e2 : b ] ==>
                Θ; B; Γ ⊨_wf C_eq e1 e2" 
| wfC_trueI: " Θ; B ⊨_wf Γ ==> Θ; B; Γ ⊨_wf C_true "
| wfC_falseI: " Θ; B ⊨_wf Γ ==> Θ; B; Γ ⊨_wf C_false "

| wfC_conjI: "[ Θ; B; Γ ⊨_wf c1 ; Θ; B; Γ ⊨_wf c2 ] ==> Θ; B; Γ ⊨_wf C_conj c1 c2"
| wfC_disjI: "[ Θ; B; Γ ⊨_wf c1 ; Θ; B; Γ ⊨_wf c2 ] ==> Θ; B; Γ ⊨_wf C_disj c1 c2"
| wfC_notI: "[ Θ; B; Γ ⊨_wf c1 ] ==> Θ; B; Γ ⊨_wf C_not c1"
| wfC_impI: "[ Θ; B; Γ ⊨_wf c1 ;
                Θ; B; Γ ⊨_wf c2 ] ==> Θ; B; Γ ⊨_wf C_imp c1 c2"

| wfG_nilI: " ⊨_wf Θ ==> Θ; B ⊨_wf GNil"
| wfG_cons1I: "[ c ∉ { TRUE, FALSE } ;
                  Θ; B ⊨_wf Γ ;
                  atom x ♯ Γ ;
                  Θ ; B ; (x,b,C_true)#_\<Gamma>Γ ⊨_wf c ; wfB Θ B b
               ] ==> Θ; B ⊨_wf ((x,b,c)#_\<Gamma>Γ)"
| wfG_cons2I: "[ c ∈ { TRUE, FALSE } ;
                  Θ; B ⊨_wf Γ ;
                  atom x ♯ Γ ;
                  wfB Θ B b
                ] ==> Θ; B ⊨_wf ((x,b,c)#_\<Gamma>Γ)"

| wfTh_emptyI: " ⊨_wf []"

| wfTh_consI: "[
        (name_of_type tdef) ∉ name_of_type ` set Θ ;
        ⊨_wf Θ ;
       Θ ⊨_wf tdef ] ==> ⊨_wf tdef#Θ"

| wfTD_simpleI: "[
        Θ ; {||} ; GNil ⊨_wf lst
      ] ==>
        Θ ⊨_wf (AF_typedef s lst )"

| wfTD_poly: "[
        Θ ; {|bv|} ; GNil ⊨_wf lst
       ] ==>
      Θ ⊨_wf (AF_typedef_poly s bv lst)"

| wfTs_nil: "Θ; B ⊨_wf Γ ==> Θ; B; Γ ⊨_wf []::(string*τ) list"
| wfTs_cons: "[ Θ; B; Γ ⊨_wf τ ;
                dc ∉ fst ` set ts;
                Θ; B; Γ ⊨_wf ts::(string*τ) list ] ==> Θ; B; Γ ⊨_wf ((dc,τ)#ts)"

inductive_cases wfC_elims:
  "Θ; B; Γ ⊨_wf C_true"
  "Θ; B; Γ ⊨_wf C_false"
  "Θ; B; Γ ⊨_wf C_eq e1 e2"
  "Θ; B; Γ ⊨_wf C_conj c1 c2"
  "Θ; B; Γ ⊨_wf C_disj c1 c2"
  "Θ; B; Γ ⊨_wf C_not c1"
  "Θ; B; Γ ⊨_wf C_imp c1 c2"

inductive_cases wfV_elims:
  "Θ; B; Γ ⊨_wf V_var x : b"
  "Θ; B; Γ ⊨_wf V_lit l : b"
  "Θ; B; Γ ⊨_wf V_pair v1 v2 : b"
  "Θ; B; Γ ⊨_wf V_cons tyid dc v : b"
  "Θ; B; Γ ⊨_wf V_consp tyid dc b v : b'"

inductive_cases wfCE_elims:
  " Θ; B; Γ ⊨_wf CE_val v : b"
  " Θ; B; Γ ⊨_wf CE_op Plus v1 v2 : b"
  " Θ; B; Γ ⊨_wf CE_op LEq v1 v2 : b"
  " Θ; B; Γ ⊨_wf CE_fst v1 : b"
  " Θ; B; Γ ⊨_wf CE_snd v1 : b"
  " Θ; B; Γ ⊨_wf CE_concat v1 v2 : b"
  " Θ; B; Γ ⊨_wf CE_len v1 : b"
  " Θ; B; Γ ⊨_wf CE_op opp v1 v2 : b"
  " Θ; B; Γ ⊨_wf CE_op Eq v1 v2 : b"

inductive_cases wfT_elims:
  "Θ; B ; Γ ⊨_wf τ::τ"
  "Θ; B ; Γ ⊨_wf { z : b | c }"

inductive_cases wfG_elims:
  "Θ; B ⊨_wf GNil"
  "Θ; B ⊨_wf (x,b,c)#_\<Gamma>Γ"
  "Θ; B ⊨_wf (x,b,TRUE)#_\<Gamma>Γ"
  "Θ; B ⊨_wf (x,b,FALSE)#_\<Gamma>Γ"

inductive_cases wfTh_elims:
  " ⊨_wf []"
  " ⊨_wf td#Π"  

inductive_cases wfTD_elims:
  "Θ ⊨_wf (AF_typedef s lst )"  
  "Θ ⊨_wf (AF_typedef_poly s bv lst )" 

inductive_cases wfTs_elims:
  "Θ; B ; GNil ⊨_wf ([]::((string*τ) list))"
  "Θ; B ; GNil ⊨_wf ((t#ts)::((string*τ) list))"

inductive_cases wfB_elims:
  " Θ; B ⊨_wf B_pair b1 b2" 
  " Θ; B ⊨_wf B_id s"
  " Θ; B ⊨_wf B_app s b"

equivariance wfV 

text ‹This setup of 'avoiding' is not complete and for some of lemmas, such as weakening,
  it the hard way›
nominal_inductive wfV 
  avoids   wfV_conspI: bv | wfTI: z
proof(goal_cases)
  case (1 s bv dclist Θ dc x b' c B b Γ v)

  moreover hence "atom bv ♯ V_consp s dc b v" using v.fresh fresh_prodN pure_fresh by metis
  moreover have "atom bv ♯ B_app s b" using b.fresh fresh_prodN pure_fresh 1 by metis
  ultimately show ?case using b.fresh v.fresh pure_fresh  fresh_star_def fresh_prodN by fastforce
next
  case (2 s bv dclist Θ dc x b' c B b Γ v)
  then show ?case by auto
next
  case (3 z Γ Θ B b c)
  then show ?case using τ.fresh fresh_star_def fresh_prodN by fastforce
next
  case (4 z Γ Θ B b c)
  then show ?case by auto
qed

inductive 
  wfE :: "Θ ==> Φ ==> B ==> Γ ==> Δ ==> e ==> b ==> bool" (‹ _ ; _ ; _ ; _ ; _ ⊨_wf _ : _ › [50,50,50] 50)  and
  wfS :: "Θ ==> Φ ==> B ==> Γ ==> Δ ==> s ==> b ==> bool" (‹ _ ; _ ; _ ; _ ; _ ⊨_wf _ : _ › [50,50,50] 50)  and
  wfCS :: "Θ ==> Φ ==> B ==> Γ ==> Δ ==> tyid ==> string ==> τ ==> branch_s ==> b ==> bool" (‹ _ ; _ ; _ ; _ ; _ ; _ ; _ ; _ ⊨_wf _ : _ › [50,50,50,50,50] 50)  and
  wfCSS :: "Θ ==> Φ ==> B ==> Γ ==> Δ ==> tyid ==> (string * τ) list ==> branch_list ==> b ==> bool" (‹ _ ; _ ; _ ; _ ; _ ; _ ; _ ⊨_wf _ : _ › [50,50,50,50,50] 50)  and       
  wfPhi :: "Θ ==> Φ ==> bool" (‹ _ ⊨_wf _ › [50,50] 50)  and
  wfD :: "Θ ==> B ==> Γ ==> Δ ==> bool" (‹ _ ; _ ; _ ⊨_wf _ › [50,50] 50) and       
  wfFTQ :: "Θ ==> Φ ==> fun_typ_q ==> bool"  (‹ _ ; _ ⊨_wf _ › [50] 50) and
  wfFT :: "Θ ==> Φ ==> B ==> fun_typ ==> bool"  (‹ _ ; _ ; _ ⊨_wf _ › [50] 50)  where

wfE_valI : "[
   Θ ⊨_wf Φ;
   Θ; B; Γ ⊨_wf Δ;
   Θ; B; Γ ⊨_wf v : b
\<rbrakk> ==>
    Θ; Φ; B; Γ; Δ ⊨_wf AE_val v : b"

| wfE_plusI: "[
   Θ ⊨_wf Φ;
   Θ; B; Γ ⊨_wf Δ;
   Θ; B; Γ ⊨_wf v1 : B_int;
   Θ; B; Γ ⊨_wf v2 : B_int
\<rbrakk> ==>
   Θ; Φ; B; Γ; Δ ⊨_wf AE_op Plus v1 v2 : B_int"

| wfE_leqI:"[
   Θ ⊨_wf Φ ;
   Θ; B; Γ ⊨_wf Δ;
   Θ; B; Γ ⊨_wf v1 : B_int;
   Θ; B; Γ ⊨_wf v2 : B_int
\<rbrakk> ==>
   Θ; Φ; B; Γ; Δ ⊨_wf AE_op LEq v1 v2 : B_bool"

| wfE_eqI:"[
   Θ ⊨_wf Φ ;
   Θ; B; Γ ⊨_wf Δ;
   Θ; B; Γ ⊨_wf v1 : b;
   Θ; B; Γ ⊨_wf v2 : b;
   b ∈ { B_bool, B_int, B_unit }
\<rbrakk> ==>
   Θ; Φ; B; Γ; Δ ⊨_wf AE_op Eq v1 v2 : B_bool"

| wfE_fstI: "[
   Θ ⊨_wf Φ;
   Θ; B; Γ ⊨_wf Δ;
   Θ; B; Γ ⊨_wf v1 : B_pair b1 b2
 ] ==>
   Θ; Φ; B; Γ; Δ ⊨_wf AE_fst v1 : b1"

| wfE_sndI: "[
   Θ ⊨_wf Φ ;
   Θ; B; Γ ⊨_wf Δ;
   Θ; B; Γ ⊨_wf v1 : B_pair b1 b2
\<rbrakk> ==>
   Θ; Φ; B; Γ; Δ ⊨_wf AE_snd v1 : b2"

| wfE_concatI: "[
   Θ ⊨_wf Φ ;
   Θ; B; Γ ⊨_wf Δ;
   Θ; B; Γ ⊨_wf v1 : B_bitvec;
   Θ; B; Γ ⊨_wf v2 : B_bitvec
\<rbrakk> ==>
   Θ ; Φ ; B ; Γ; Δ ⊨_wf AE_concat v1 v2 : B_bitvec"

| wfE_splitI: "[
   Θ ⊨_wf Φ ;
   Θ; B; Γ ⊨_wf Δ;
   Θ; B; Γ ⊨_wf v1 : B_bitvec;
   Θ; B; Γ ⊨_wf v2 : B_int
\<rbrakk> ==>
   Θ ; Φ ; B ; Γ; Δ ⊨_wf AE_split v1 v2 : B_pair B_bitvec B_bitvec"

| wfE_lenI: "[
   Θ ⊨_wf Φ ;
   Θ; B; Γ ⊨_wf Δ;
   Θ; B; Γ ⊨_wf v1 : B_bitvec
\<rbrakk> ==>
   Θ; Φ; B; Γ; Δ ⊨_wf AE_len v1 : B_int"

| wfE_appI:  "[
   Θ ⊨_wf Φ ;
   Θ; B; Γ ⊨_wf Δ;
   Some (AF_fundef f (AF_fun_typ_none (AF_fun_typ x b c τ s))) = lookup_fun Φ f ;
   Θ; B; Γ ⊨_wf v : b
\<rbrakk> ==>
   Θ; Φ; B; Γ; Δ ⊨_wf AE_app f v : b_of τ"

| wfE_appPI:  "[
    Θ ⊨_wf Φ ;
    Θ; B; Γ ⊨_wf Δ;
    Θ; B ⊨_wf b';
    atom bv ♯ (Φ, Θ, B, Γ, Δ, b', v, (b_of τ)[bv::=b']_b);
    Some (AF_fundef f (AF_fun_typ_some bv (AF_fun_typ x b c τ s))) = lookup_fun Φ f;
    Θ; B; Γ ⊨_wf v : (b[bv::=b']_b)
\<rbrakk> ==>
    Θ; Φ; B; Γ; Δ ⊨_wf (AE_appP f b' v) : ((b_of τ)[bv::=b']_b)"

| wfE_mvarI: "[
   Θ ⊨_wf Φ ;
   Θ; B; Γ ⊨_wf Δ;
   (u,τ) ∈ setD Δ
\<rbrakk> ==>
   Θ; Φ; B; Γ; Δ ⊨_wf AE_mvar u : b_of τ" 

| wfS_valI: "[
    Θ ⊨_wf Φ ;
    Θ; B; Γ ⊨_wf v : b ;
    Θ; B; Γ ⊨_wf Δ
\<rbrakk> ==>
    Θ; Φ; B; Γ; Δ ⊨_wf (AS_val v) : b"

| wfS_letI: "[
    wfE Θ Φ B Γ Δ e b' ;
    Θ ; Φ ; B ; (x,b',C_true) #_\<Gamma> Γ ; Δ ⊨_wf s : b;
    Θ; B; Γ ⊨_wf Δ ;
    atom x ♯ (Φ, Θ, B, Γ, Δ, e, b)
\<rbrakk> ==>
    Θ; Φ; B; Γ; Δ ⊨_wf LET x = e IN s : b"

| wfS_assertI: "[
    Θ ; Φ ; B ; (x,B_bool,c) #_\<Gamma> Γ ; Δ ⊨_wf s : b;
    Θ; B; Γ ⊨_wf c ;
    Θ; B; Γ ⊨_wf Δ ;
    atom x ♯ (Φ, Θ, B, Γ, Δ, c, b, s)
\<rbrakk> ==>
    Θ; Φ; B; Γ; Δ ⊨_wf ASSERT c IN s : b"

| wfS_let2I: "[
   Θ; Φ; B; Γ; Δ ⊨_wf s1 : b_of τ ;
   Θ; B; Γ ⊨_wf τ;
   Θ ; Φ ; B ; (x,b_of τ,C_true) #_\<Gamma> Γ ; Δ ⊨_wf s2 : b ;
   atom x ♯ (Φ, Θ, B, Γ, Δ, s1, b,τ)
\<rbrakk> ==>
   Θ; Φ; B; Γ; Δ ⊨_wf LET x : τ = s1 IN s2 : b"

| wfS_ifI: "[
   Θ; B; Γ ⊨_wf v : B_bool;
   Θ; Φ; B; Γ; Δ ⊨_wf s1 : b ;
   Θ; Φ; B; Γ; Δ ⊨_wf s2 : b
\<rbrakk> ==>
   Θ; Φ; B; Γ; Δ ⊨_wf IF v THEN s1 ELSE s2 : b"

| wfS_varI : "[
   wfT Θ B Γ τ ;
   Θ; B; Γ ⊨_wf v : b_of τ;
   atom u ♯ (Φ, Θ, B, Γ, Δ, τ, v, b);
   Θ ; Φ ; B ; Γ ; (u,τ)#_\<Delta>Δ ⊨_wf s : b
\<rbrakk> ==>
   Θ; Φ; B; Γ; Δ ⊨_wf VAR u : τ = v IN s : b "

| wfS_assignI: "[
   (u,τ) ∈ setD Δ ;
   Θ; B; Γ ⊨_wf Δ ;
   Θ ⊨_wf Φ ;
   Θ; B; Γ ⊨_wf v : b_of τ
\<rbrakk> ==>
   Θ; Φ; B; Γ; Δ ⊨_wf u ::= v : B_unit"

| wfS_whileI: "[
  Θ; Φ; B; Γ; Δ ⊨_wf s1 : B_bool ;
  Θ; Φ; B; Γ; Δ ⊨_wf s2 : b
\<rbrakk> ==>
  Θ; Φ; B; Γ; Δ ⊨_wf WHILE s1 DO { s2 } : b"

| wfS_seqI: "[
  Θ; Φ; B; Γ; Δ ⊨_wf s1 : B_unit ;
  Θ; Φ; B; Γ; Δ ⊨_wf s2 : b
\<rbrakk> ==>
  Θ; Φ; B; Γ; Δ ⊨_wf s1 ;; s2 : b"

| wfS_matchI: "[
  wfV Θ B Γ v (B_id tid) ;
  (AF_typedef tid dclist ) ∈ set Θ;
  wfD Θ B Γ Δ ;
  Θ ⊨_wf Φ ;
  Θ ; Φ ; B ; Γ ; Δ ; tid ; dclist ⊨_wf cs : b
\<rbrakk> ==>
  Θ; Φ; B; Γ; Δ ⊨_wf AS_match v cs : b "

| wfS_branchI: "[
  Θ ; Φ ; B ; (x,b_of τ,C_true) #_\<Gamma> Γ ; Δ ⊨_wf s : b ;
  atom x ♯ (Φ, Θ, B, Γ, Δ, Γ,τ);
  Θ; B; Γ ⊨_wf Δ
\<rbrakk> ==>
  Θ ; Φ ; B ; Γ ; Δ ; tid ; dc ; τ ⊨_wf dc x ==> s : b"

| wfS_finalI: "[
  Θ; Φ; B; Γ; Δ ; tid ; dc ; t ⊨_wf cs : b
 ] ==>
  Θ ; Φ ; B ; Γ ; Δ ; tid ; [(dc,t)] ⊨_wf AS_final cs : b "

| wfS_cons: "[
  Θ; Φ; B; Γ; Δ ; tid ; dc ; t ⊨_wf cs : b;
  Θ; Φ; B; Γ; Δ ; tid ; dclist ⊨_wf css : b
 ] ==>
  Θ ; Φ ; B ; Γ ; Δ ; tid ; (dc,t)#dclist ⊨_wf AS_cons cs css : b "

| wfD_emptyI: "Θ; B ⊨_wf Γ ==> Θ ; B ; Γ ⊨_wf []_\<Delta>"

| wfD_cons: "[
  Θ ; B ; Γ ⊨_wf Δ::Δ ;
  Θ ; B ; Γ ⊨_wf τ;
  u ∉ fst ` setD Δ
\<rbrakk> ==>
  Θ; B; Γ ⊨_wf ((u,τ) #_\<Delta> Δ)"

| wfPhi_emptyI: " ⊨_wf Θ ==> Θ ⊨_wf []"

| wfPhi_consI: "[
  f ∉ name_of_fun ` set Φ;
  Θ ; Φ ⊨_wf ft;
  Θ ⊨_wf Φ
\<rbrakk> ==>
  Θ ⊨_wf ((AF_fundef f ft)#Φ)"  

| wfFTNone: " Θ ; Φ ; {||} ⊨_wf ft ==> Θ ; Φ ⊨_wf AF_fun_typ_none ft"
| wfFTSome: " Θ ; Φ ; {| bv |} ⊨_wf ft ==> Θ ; Φ ⊨_wf AF_fun_typ_some bv ft"

| wfFTI: "[
  Θ ; B ⊨_wf b;
  supp s ⊆ {atom x} ∪ supp B ;
  supp c ⊆ { atom x } ;
  Θ ; B ; (x,b,c) #_\<Gamma> GNil ⊨_wf τ;
  Θ ⊨_wf Φ
\<rbrakk> ==>
  Θ ; Φ ; B ⊨_wf (AF_fun_typ x b c τ s)"

inductive_cases wfE_elims:
  "Θ; Φ; B; Γ; Δ ⊨_wf AE_val v : b"
  "Θ; Φ; B; Γ; Δ ⊨_wf AE_op Plus v1 v2 : b"
  "Θ; Φ; B; Γ; Δ ⊨_wf AE_op LEq v1 v2 : b"
  "Θ; Φ; B; Γ; Δ ⊨_wf AE_fst v1 : b"
  "Θ; Φ; B; Γ; Δ ⊨_wf AE_snd v1 : b"
  "Θ; Φ; B; Γ; Δ ⊨_wf AE_concat v1 v2 : b"
  "Θ; Φ; B; Γ; Δ ⊨_wf AE_len v1 : b"
  "Θ; Φ; B; Γ; Δ ⊨_wf AE_op opp v1 v2 : b"
  "Θ; Φ; B; Γ; Δ ⊨_wf AE_app f v: b"
  "Θ; Φ; B; Γ; Δ ⊨_wf AE_appP f b' v: b"
  "Θ; Φ; B; Γ; Δ ⊨_wf AE_mvar u : b"
  "Θ; Φ; B; Γ; Δ ⊨_wf AE_op Eq v1 v2 : b"

inductive_cases wfCS_elims:
  "Θ; Φ; B; Γ; Δ ; tid ; dc ; t ⊨_wf (cs::branch_s) : b"
  "Θ; Φ; B; Γ; Δ ; tid ; dc ⊨_wf (cs::branch_list) : b"

inductive_cases wfPhi_elims:
  " Θ ⊨_wf []"
  " Θ ⊨_wf ((AF_fundef f ft)#Π)"  
  " Θ ⊨_wf (fd#Φ::Φ)"  

declare[[ simproc del: alpha_lst]]

inductive_cases wfFTQ_elims:
  "Θ ; Φ ⊨_wf AF_fun_typ_none ft"
  "Θ ; Φ ⊨_wf AF_fun_typ_some bv ft"
  "Θ ; Φ ⊨_wf AF_fun_typ_some bv (AF_fun_typ x b c τ s)"

inductive_cases wfFT_elims:
  "Θ ; Φ ; B ⊨_wf AF_fun_typ x b c τ s"

declare[[ simproc add: alpha_lst]]

inductive_cases wfD_elims:
  "Π ; B ; (Γ::Γ) ⊨_wf []_\<Delta>"
  "Π ; B ; (Γ::Γ) ⊨_wf (u,τ) #_\<Delta> Δ::Δ"

equivariance wfE 

nominal_inductive wfE 
  avoids   wfE_appPI: bv |  wfS_varI: u |  wfS_letI: x | wfS_let2I: x  | wfS_branchI: x | wfS_assertI: x

proof(goal_cases)
  case (1 Θ Φ B Γ Δ b' bv v τ f x b c s)
  moreover hence "atom bv ♯ AE_appP f b' v" using pure_fresh fresh_prodN e.fresh  by auto
  ultimately show ?case using fresh_star_def by fastforce
next
  case (2 Θ Φ B Γ Δ b' bv v τ f x b c s)
  then show ?case by auto
next
  case (3 Φ Θ B Γ Δ e b' x s b)
  moreover hence "atom x ♯ LET x = e IN s" using  fresh_prodN by auto
  ultimately show ?case using fresh_prodN fresh_star_def by fastforce 
next
  case (4 Φ Θ B Γ Δ e b' x s b)
  then show ?case by auto
next
  case (5 Θ Φ B x c Γ Δ s b)
  hence "atom x ♯ ASSERT c IN s" using  s_branch_s_branch_list.fresh by auto
  then show ?case using fresh_prodN fresh_star_def 5 by fastforce 
next
  case (6 Θ Φ B x c Γ Δ s b)
  then show ?case by auto
next
  case (7 Φ Θ B Γ Δ s1 τ x s2 b)
  hence "atom x ♯ τ ∧ atom x ♯ s1" using fresh_prodN by metis
  moreover hence "atom x ♯ LET x : τ = s1 IN s2" 
    using  s_branch_s_branch_list.fresh(3)[of "atom x" x "τ" s1 s2 ] fresh_prodN by simp
  ultimately show ?case using fresh_prodN fresh_star_def 7 by fastforce 
next
  case (8 Φ Θ B Γ Δ s1 τ x s2 b)
  then show ?case by auto
next
  case (9 Θ B Γ τ v u Φ Δ b s)
  moreover hence " atom u ♯ AS_var u τ v s" using fresh_prodN s_branch_s_branch_list.fresh by simp
  ultimately show ?case using fresh_star_def fresh_prodN s_branch_s_branch_list.fresh by fastforce
next
  case (10 Θ B Γ τ v u Φ Δ b s)
  then show ?case by auto
next
  case (11 Φ Θ B x τ Γ Δ s b tid dc)
  moreover have "atom x ♯ (dc x ==> s)" using pure_fresh  s_branch_s_branch_list.fresh by auto
  ultimately show ?case using fresh_prodN fresh_star_def pure_fresh by fastforce 
next
  case (12 Φ Θ B x τ Γ Δ s b tid dc)
  then show ?case by auto
qed

inductive  wfVDs :: "var_def list ==> bool" where

wfVDs_nilI: "wfVDs []"

| wfVDs_consI: "[
   atom u ♯ ts;
   wfV ([]::Θ) {||} GNil v (b_of τ);
   wfT ([]::Θ) {||} GNil τ;
   wfVDs ts
\<rbrakk> ==> wfVDs ((AV_def u τ v)#ts)"

equivariance wfVDs 
nominal_inductive wfVDs .  

end