Theory Wellformed

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

chapter ‹Wellformed Terms›

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

named_theorems ms_wb "Facts for helping with well-sortedness"

section ‹Definitions›

inductive wfV :: "Θ ⇒ ℬ ⇒ Γ ⇒ v ⇒ b ⇒ bool" (" _ ; _ ; _ ⊢⇩w⇩f _ : _ " [50,50,50] 50)  and
  wfC :: "Θ ⇒ ℬ ⇒ Γ ⇒ c ⇒ bool" (" _ ; _ ; _   ⊢⇩w⇩f _ " [50,50] 50)  and         
  wfG :: "Θ ⇒ ℬ ⇒ Γ ⇒ bool" (" _ ; _  ⊢⇩w⇩f _ " [50,50] 50) and
  wfT :: "Θ ⇒ ℬ ⇒ Γ ⇒ τ ⇒ bool" (" _ ; _ ; _   ⊢⇩w⇩f _ " [50,50] 50)  and
  wfTs :: "Θ ⇒ ℬ ⇒ Γ ⇒ (string*τ) list ⇒ bool" (" _ ; _  ; _ ⊢⇩w⇩f _ " [50,50] 50)  and 
  wfTh :: "Θ ⇒ bool" ("   ⊢⇩w⇩f _ " [50] 50)  and
  wfB :: "Θ ⇒ ℬ ⇒ b ⇒ bool" (" _ ; _  ⊢⇩w⇩f _ " [50,50] 50) and
  wfCE :: "Θ ⇒ ℬ ⇒ Γ ⇒ ce ⇒ b ⇒ bool" ("  _ ; _ ; _ ⊢⇩w⇩f _ : _ " [50,50,50] 50) and
  wfTD :: "Θ ⇒ type_def ⇒ bool" (" _ ⊢⇩w⇩f _ " [50,50] 50)          
  where

wfB_intI:  "⊢⇩w⇩f Θ ⟹ Θ; ℬ ⊢⇩w⇩f B_int" 
| wfB_boolI:  "⊢⇩w⇩f Θ ⟹ Θ; ℬ ⊢⇩w⇩f B_bool" 
| wfB_unitI:  "⊢⇩w⇩f Θ ⟹ Θ; ℬ ⊢⇩w⇩f B_unit" 
| wfB_bitvecI:  "⊢⇩w⇩f Θ ⟹ Θ; ℬ ⊢⇩w⇩f B_bitvec" 
| wfB_pairI:  "⟦ Θ; ℬ ⊢⇩w⇩f b1 ; Θ; ℬ ⊢⇩w⇩f b2 ⟧ ⟹ Θ; ℬ ⊢⇩w⇩f B_pair b1 b2" 

| wfB_consI:  "⟦
   ⊢⇩w⇩f Θ; 
   (AF_typedef s dclist) ∈ set Θ 
⟧ ⟹ 
   Θ; ℬ ⊢⇩w⇩f B_id s"

| wfB_appI:  "⟦ 
   ⊢⇩w⇩f Θ; 
   Θ; ℬ ⊢⇩w⇩f b;
   (AF_typedef_poly s bv dclist) ∈ set Θ 
⟧ ⟹ 
   Θ; ℬ ⊢⇩w⇩f B_app s b"

| wfV_varI: "⟦ Θ; ℬ ⊢⇩w⇩f Γ ; Some (b,c) = lookup Γ x ⟧ ⟹ Θ; ℬ; Γ ⊢⇩w⇩f V_var x : b"
| wfV_litI: "Θ; ℬ ⊢⇩w⇩f Γ  ⟹ Θ; ℬ; Γ ⊢⇩w⇩f V_lit l : base_for_lit l"

| wfV_pairI: "⟦
   Θ; ℬ; Γ ⊢⇩w⇩f v1 : b1 ; 
   Θ; ℬ; Γ ⊢⇩w⇩f v2 : b2 
⟧ ⟹ 
   Θ; ℬ; Γ ⊢⇩w⇩f (V_pair v1 v2) : B_pair b1 b2"

| wfV_consI: "⟦   
   AF_typedef s dclist ∈ set Θ;
   (dc, ⦃ x : b'  | c ⦄) ∈ set dclist ;
   Θ; ℬ; Γ ⊢⇩w⇩f v : b' 
⟧ ⟹ 
   Θ; ℬ; Γ ⊢⇩w⇩f V_cons s dc v : B_id s"

| wfV_conspI: "⟦   
    AF_typedef_poly s bv dclist ∈ set Θ;
    (dc, ⦃ x : b'  | c ⦄) ∈ set dclist ;
    Θ ;  ℬ  ⊢⇩w⇩f b;
    atom bv ♯ (Θ, ℬ, Γ, b , v);
    Θ; ℬ; Γ ⊢⇩w⇩f v : b'[bv::=b]⇩b⇩b 
⟧ ⟹
    Θ; ℬ; Γ ⊢⇩w⇩f V_consp s dc b v : B_app s b"

| wfCE_valI : "⟦             
    Θ; ℬ; Γ ⊢⇩w⇩f v  : b 
⟧ ⟹ 
    Θ; ℬ; Γ  ⊢⇩w⇩f CE_val v  : b"

| wfCE_plusI: "⟦               
    Θ; ℬ; Γ ⊢⇩w⇩f v1 : B_int; 
    Θ; ℬ; Γ ⊢⇩w⇩f v2 : B_int 
⟧ ⟹ 
    Θ; ℬ; Γ  ⊢⇩w⇩f CE_op Plus v1 v2 : B_int"

| wfCE_leqI:"⟦
    Θ; ℬ; Γ ⊢⇩w⇩f v1 : B_int; 
    Θ; ℬ; Γ ⊢⇩w⇩f v2 : B_int 
⟧ ⟹
    Θ; ℬ; Γ ⊢⇩w⇩f CE_op LEq v1 v2 : B_bool"

| wfCE_eqI:"⟦
    Θ; ℬ; Γ ⊢⇩w⇩f v1 : b; 
    Θ; ℬ; Γ ⊢⇩w⇩f v2 : b 
⟧ ⟹
    Θ; ℬ; Γ ⊢⇩w⇩f CE_op Eq v1 v2 : B_bool"

| wfCE_fstI: "⟦               
    Θ; ℬ; Γ ⊢⇩w⇩f v1 : B_pair b1 b2  
⟧ ⟹ 
    Θ; ℬ; Γ  ⊢⇩w⇩f CE_fst v1 : b1"

| wfCE_sndI: "⟦             
    Θ; ℬ; Γ ⊢⇩w⇩f v1 : B_pair b1 b2  
⟧ ⟹  
    Θ; ℬ; Γ  ⊢⇩w⇩f CE_snd v1 : b2"

| wfCE_concatI: "⟦ 
    Θ; ℬ; Γ ⊢⇩w⇩f v1 : B_bitvec ; 
    Θ; ℬ; Γ ⊢⇩w⇩f v2 : B_bitvec 
⟧ ⟹ 
    Θ; ℬ; Γ  ⊢⇩w⇩f CE_concat v1 v2 : B_bitvec"

| wfCE_lenI: "⟦                
    Θ; ℬ; Γ ⊢⇩w⇩f v1 : B_bitvec 
⟧ ⟹ 
    Θ; ℬ; Γ  ⊢⇩w⇩f CE_len v1 : B_int"

| wfTI : "⟦ 
    atom z ♯  (Θ, ℬ, Γ) ; 
    Θ; ℬ ⊢⇩w⇩f b;
    Θ; ℬ ; (z,b,C_true) #⇩Γ Γ ⊢⇩w⇩f c 
⟧ ⟹ 
    Θ; ℬ; Γ ⊢⇩w⇩f ⦃ z : b | c ⦄"

| wfC_eqI: "⟦  
                Θ; ℬ; Γ  ⊢⇩w⇩f e1  : b ; 
                 Θ; ℬ; Γ  ⊢⇩w⇩f e2  : b  ⟧ ⟹ 
                Θ; ℬ; Γ ⊢⇩w⇩f C_eq e1 e2" 
| wfC_trueI: " Θ; ℬ ⊢⇩w⇩f Γ  ⟹ Θ; ℬ; Γ  ⊢⇩w⇩f C_true "
| wfC_falseI: " Θ; ℬ ⊢⇩w⇩f Γ  ⟹ Θ; ℬ; Γ ⊢⇩w⇩f C_false "

| wfC_conjI: "⟦ Θ; ℬ; Γ ⊢⇩w⇩f c1 ; Θ; ℬ; Γ ⊢⇩w⇩f c2 ⟧ ⟹ Θ; ℬ; Γ ⊢⇩w⇩f C_conj c1 c2"
| wfC_disjI: "⟦ Θ; ℬ; Γ ⊢⇩w⇩f c1 ; Θ; ℬ; Γ ⊢⇩w⇩f c2 ⟧ ⟹ Θ; ℬ; Γ ⊢⇩w⇩f C_disj c1 c2"
| wfC_notI: "⟦  Θ; ℬ; Γ ⊢⇩w⇩f c1  ⟧ ⟹ Θ; ℬ; Γ ⊢⇩w⇩f C_not c1"
| wfC_impI: "⟦  Θ; ℬ; Γ ⊢⇩w⇩f c1 ; 
                Θ; ℬ; Γ  ⊢⇩w⇩f c2 ⟧ ⟹ Θ; ℬ; Γ ⊢⇩w⇩f C_imp c1 c2"

| wfG_nilI: " ⊢⇩w⇩f Θ  ⟹ Θ; ℬ ⊢⇩w⇩f GNil"
| wfG_cons1I: "⟦  c ∉ { TRUE, FALSE } ; 
                  Θ; ℬ  ⊢⇩w⇩f Γ ; 
                  atom x ♯ Γ ; 
                  Θ  ; ℬ ; (x,b,C_true)#⇩ΓΓ ⊢⇩w⇩f c ; wfB Θ ℬ b  
               ⟧ ⟹  Θ; ℬ  ⊢⇩w⇩f ((x,b,c)#⇩ΓΓ)"
| wfG_cons2I: "⟦  c ∈ { TRUE, FALSE } ; 
                  Θ; ℬ  ⊢⇩w⇩f Γ ; 
                  atom x ♯ Γ ;  
                  wfB Θ ℬ b   
                ⟧ ⟹  Θ; ℬ ⊢⇩w⇩f ((x,b,c)#⇩ΓΓ)"

| wfTh_emptyI: " ⊢⇩w⇩f []"

| wfTh_consI: "⟦      
        (name_of_type tdef) ∉ name_of_type ` set Θ ;
        ⊢⇩w⇩f Θ ; 
       Θ ⊢⇩w⇩f  tdef ⟧  ⟹  ⊢⇩w⇩f tdef#Θ"

| wfTD_simpleI: "⟦
        Θ ; {||} ; GNil ⊢⇩w⇩f lst
      ⟧ ⟹ 
        Θ ⊢⇩w⇩f (AF_typedef s lst )"

| wfTD_poly: "⟦ 
        Θ ; {|bv|} ; GNil ⊢⇩w⇩f lst 
       ⟧ ⟹
      Θ ⊢⇩w⇩f (AF_typedef_poly s bv lst)"

| wfTs_nil: "Θ; ℬ ⊢⇩w⇩f Γ ⟹ Θ; ℬ; Γ ⊢⇩w⇩f []::(string*τ) list"
| wfTs_cons: "⟦ Θ; ℬ; Γ ⊢⇩w⇩f τ ; 
                dc ∉ fst ` set ts;
                Θ; ℬ; Γ ⊢⇩w⇩f ts::(string*τ) list ⟧ ⟹ Θ; ℬ; Γ ⊢⇩w⇩f ((dc,τ)#ts)"

inductive_cases wfC_elims:
  "Θ; ℬ; Γ ⊢⇩w⇩f C_true"
  "Θ; ℬ; Γ ⊢⇩w⇩f C_false"
  "Θ; ℬ; Γ ⊢⇩w⇩f C_eq e1 e2"
  "Θ; ℬ; Γ ⊢⇩w⇩f C_conj c1 c2"
  "Θ; ℬ; Γ ⊢⇩w⇩f C_disj c1 c2"
  "Θ; ℬ; Γ ⊢⇩w⇩f C_not c1"
  "Θ; ℬ; Γ ⊢⇩w⇩f C_imp c1 c2"

inductive_cases wfV_elims:
  "Θ; ℬ; Γ ⊢⇩w⇩f V_var x : b"
  "Θ; ℬ; Γ ⊢⇩w⇩f V_lit l : b"
  "Θ; ℬ; Γ ⊢⇩w⇩f V_pair v1 v2 : b"
  "Θ; ℬ; Γ ⊢⇩w⇩f V_cons tyid dc v : b"
  "Θ; ℬ; Γ ⊢⇩w⇩f V_consp tyid dc b v : b'"

inductive_cases wfCE_elims:
  " Θ; ℬ; Γ ⊢⇩w⇩f CE_val v : b"
  " Θ; ℬ; Γ ⊢⇩w⇩f CE_op Plus v1 v2 : b"
  " Θ; ℬ; Γ ⊢⇩w⇩f CE_op LEq v1 v2 : b"
  " Θ; ℬ; Γ ⊢⇩w⇩f CE_fst v1 : b"
  " Θ; ℬ; Γ ⊢⇩w⇩f CE_snd v1 : b"
  " Θ; ℬ; Γ ⊢⇩w⇩f CE_concat v1 v2 : b"
  " Θ; ℬ; Γ ⊢⇩w⇩f CE_len v1 : b"
  " Θ; ℬ; Γ ⊢⇩w⇩f CE_op opp v1 v2 : b"
  " Θ; ℬ; Γ ⊢⇩w⇩f CE_op Eq v1 v2 : b"

inductive_cases wfT_elims:
  "Θ; ℬ ; Γ ⊢⇩w⇩f τ::τ"
  "Θ; ℬ ; Γ ⊢⇩w⇩f ⦃ z : b | c ⦄"

inductive_cases wfG_elims:
  "Θ; ℬ ⊢⇩w⇩f GNil"
  "Θ; ℬ ⊢⇩w⇩f (x,b,c)#⇩ΓΓ"
  "Θ; ℬ ⊢⇩w⇩f (x,b,TRUE)#⇩ΓΓ"
  "Θ; ℬ ⊢⇩w⇩f (x,b,FALSE)#⇩ΓΓ"

inductive_cases wfTh_elims:
  " ⊢⇩w⇩f []"
  " ⊢⇩w⇩f td#Π"  

inductive_cases wfTD_elims:
  "Θ ⊢⇩w⇩f (AF_typedef s lst )"  
  "Θ ⊢⇩w⇩f (AF_typedef_poly s bv lst )" 

inductive_cases wfTs_elims:
  "Θ; ℬ ; GNil ⊢⇩w⇩f ([]::((string*τ) list))"
  "Θ; ℬ ; GNil ⊢⇩w⇩f ((t#ts)::((string*τ) list))"

inductive_cases wfB_elims:
  " Θ; ℬ ⊢⇩w⇩f B_pair b1 b2" 
  " Θ; ℬ ⊢⇩w⇩f B_id s"
  " Θ; ℬ ⊢⇩w⇩f B_app s b"

equivariance wfV 

text ‹This setup of 'avoiding' is not complete and for some of lemmas, such as weakening,
do 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 Γ 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 Γ v)
  then show ?case by auto
next
  case (3 z Γ Θ ℬ b c)
  then show ?case using τ.fresh fresh_star_def fresh_prodN by fastforce
next
  case (4 z Γ Θ ℬ b c)
  then show ?case by auto
qed

inductive 
  wfE :: "Θ ⇒ Φ ⇒ ℬ ⇒ Γ ⇒ Δ ⇒ e ⇒ b ⇒ bool" (" _ ; _ ; _ ; _ ; _ ⊢⇩w⇩f _ : _ " [50,50,50] 50)  and
  wfS :: "Θ ⇒ Φ ⇒ ℬ ⇒ Γ ⇒ Δ ⇒ s ⇒ b ⇒ bool" (" _ ; _ ; _ ; _ ; _ ⊢⇩w⇩f _ : _ " [50,50,50] 50)  and
  wfCS :: "Θ ⇒ Φ ⇒ ℬ ⇒ Γ ⇒ Δ ⇒  tyid ⇒ string ⇒ τ ⇒ branch_s ⇒ b ⇒ bool" (" _ ; _ ; _ ; _ ; _ ; _ ; _ ; _ ⊢⇩w⇩f _ : _ " [50,50,50,50,50] 50)  and
  wfCSS :: "Θ ⇒ Φ ⇒ ℬ ⇒ Γ ⇒ Δ ⇒  tyid ⇒ (string * τ) list ⇒ branch_list ⇒ b ⇒ bool" (" _ ; _ ; _ ; _ ; _ ; _ ; _ ⊢⇩w⇩f _ : _ " [50,50,50,50,50] 50)  and       
  wfPhi :: "Θ ⇒ Φ ⇒ bool" (" _  ⊢⇩w⇩f _ " [50,50] 50)  and
  wfD :: "Θ ⇒ ℬ ⇒ Γ ⇒ Δ ⇒ bool" (" _ ; _ ; _ ⊢⇩w⇩f _ " [50,50] 50) and       
  wfFTQ :: "Θ ⇒ Φ ⇒ fun_typ_q ⇒ bool"  (" _  ; _ ⊢⇩w⇩f _ " [50] 50) and
  wfFT :: "Θ ⇒ Φ ⇒ ℬ ⇒ fun_typ ⇒ bool"  (" _ ; _ ; _ ⊢⇩w⇩f _ " [50] 50)  where

wfE_valI : "⟦
   Θ ⊢⇩w⇩f Φ; 
   Θ; ℬ; Γ ⊢⇩w⇩f Δ;
   Θ; ℬ; Γ ⊢⇩w⇩f v  : b 
⟧ ⟹ 
    Θ; Φ; ℬ; Γ; Δ  ⊢⇩w⇩f AE_val v  : b"

| wfE_plusI: "⟦ 
   Θ ⊢⇩w⇩f Φ; 
   Θ; ℬ; Γ ⊢⇩w⇩f Δ;
   Θ; ℬ; Γ ⊢⇩w⇩f v1 : B_int; 
   Θ; ℬ; Γ ⊢⇩w⇩f v2 : B_int 
⟧ ⟹ 
   Θ; Φ; ℬ; Γ; Δ  ⊢⇩w⇩f AE_op Plus v1 v2 : B_int"

| wfE_leqI:"⟦   
   Θ ⊢⇩w⇩f Φ ;
   Θ; ℬ; Γ ⊢⇩w⇩f Δ; 
   Θ; ℬ; Γ ⊢⇩w⇩f v1 : B_int; 
   Θ; ℬ; Γ ⊢⇩w⇩f v2 : B_int
⟧ ⟹ 
   Θ; Φ; ℬ; Γ; Δ  ⊢⇩w⇩f AE_op LEq v1 v2 : B_bool"

| wfE_eqI:"⟦   
   Θ ⊢⇩w⇩f Φ ;
   Θ; ℬ; Γ ⊢⇩w⇩f Δ; 
   Θ; ℬ; Γ ⊢⇩w⇩f v1 : b; 
   Θ; ℬ; Γ ⊢⇩w⇩f v2 : b;
   b ∈ { B_bool, B_int, B_unit }
⟧ ⟹ 
   Θ; Φ; ℬ; Γ; Δ  ⊢⇩w⇩f AE_op Eq v1 v2 : B_bool"

| wfE_fstI: "⟦  
   Θ ⊢⇩w⇩f Φ; 
   Θ; ℬ; Γ ⊢⇩w⇩f Δ; 
   Θ; ℬ; Γ ⊢⇩w⇩f v1 : B_pair b1 b2 
 ⟧ ⟹ 
   Θ; Φ; ℬ; Γ; Δ ⊢⇩w⇩f AE_fst v1 : b1"

| wfE_sndI: "⟦  
   Θ ⊢⇩w⇩f Φ ; 
   Θ; ℬ; Γ ⊢⇩w⇩f Δ;
   Θ; ℬ; Γ ⊢⇩w⇩f v1 : B_pair b1 b2  
⟧ ⟹  
   Θ; Φ; ℬ; Γ; Δ ⊢⇩w⇩f AE_snd v1 : b2"

| wfE_concatI: "⟦
   Θ ⊢⇩w⇩f Φ ;
   Θ; ℬ; Γ ⊢⇩w⇩f Δ; 
   Θ; ℬ; Γ ⊢⇩w⇩f v1 : B_bitvec; 
   Θ; ℬ; Γ ⊢⇩w⇩f v2 : B_bitvec 
⟧ ⟹ 
   Θ ; Φ ; ℬ ; Γ; Δ  ⊢⇩w⇩f AE_concat v1 v2 : B_bitvec"

| wfE_splitI: "⟦
   Θ ⊢⇩w⇩f Φ ;
   Θ; ℬ; Γ ⊢⇩w⇩f Δ; 
   Θ; ℬ; Γ ⊢⇩w⇩f v1 : B_bitvec; 
   Θ; ℬ; Γ ⊢⇩w⇩f v2 : B_int 
⟧ ⟹ 
   Θ ; Φ ; ℬ ; Γ; Δ  ⊢⇩w⇩f AE_split v1 v2 : B_pair B_bitvec B_bitvec"

| wfE_lenI: "⟦
   Θ ⊢⇩w⇩f Φ ; 
   Θ; ℬ; Γ ⊢⇩w⇩f Δ; 
   Θ; ℬ; Γ ⊢⇩w⇩f v1 : B_bitvec 
⟧ ⟹ 
   Θ; Φ; ℬ; Γ; Δ  ⊢⇩w⇩f AE_len v1 : B_int"

| wfE_appI:  "⟦
   Θ ⊢⇩w⇩f Φ ; 
   Θ; ℬ; Γ ⊢⇩w⇩f Δ; 
   Some (AF_fundef f (AF_fun_typ_none (AF_fun_typ x b c τ s))) = lookup_fun Φ f ;  
   Θ; ℬ; Γ ⊢⇩w⇩f v : b
⟧ ⟹   
   Θ; Φ; ℬ; Γ; Δ ⊢⇩w⇩f AE_app f v : b_of τ"

| wfE_appPI:  "⟦
    Θ ⊢⇩w⇩f Φ ; 
    Θ; ℬ; Γ ⊢⇩w⇩f Δ; 
    Θ; ℬ  ⊢⇩w⇩f b'; 
    atom bv ♯  (Φ, Θ, ℬ, Γ, Δ, 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;  
    Θ; ℬ; Γ ⊢⇩w⇩f v : (b[bv::=b']⇩b)
⟧ ⟹   
    Θ; Φ; ℬ; Γ; Δ ⊢⇩w⇩f (AE_appP f b' v) : ((b_of τ)[bv::=b']⇩b)"

| wfE_mvarI: "⟦  
   Θ ⊢⇩w⇩f Φ ; 
   Θ; ℬ; Γ ⊢⇩w⇩f Δ; 
   (u,τ) ∈ setD Δ 
⟧ ⟹ 
   Θ; Φ; ℬ; Γ; Δ ⊢⇩w⇩f AE_mvar u : b_of τ" 

| wfS_valI: "⟦ 
    Θ ⊢⇩w⇩f Φ ;  
    Θ; ℬ; Γ ⊢⇩w⇩f v : b ; 
    Θ; ℬ; Γ ⊢⇩w⇩f Δ 
⟧  ⟹ 
    Θ; Φ; ℬ; Γ; Δ ⊢⇩w⇩f (AS_val v) : b"

| wfS_letI: "⟦ 
    wfE Θ Φ ℬ Γ Δ  e b'  ;
    Θ ; Φ ; ℬ ; (x,b',C_true) #⇩Γ Γ ; Δ ⊢⇩w⇩f s : b;
    Θ; ℬ; Γ ⊢⇩w⇩f Δ ;
    atom x ♯ (Φ, Θ, ℬ, Γ, Δ, e, b)
⟧ ⟹ 
    Θ; Φ; ℬ; Γ; Δ ⊢⇩w⇩f LET x = e IN s : b"

| wfS_assertI: "⟦ 
    Θ ; Φ ; ℬ ; (x,B_bool,c) #⇩Γ Γ ; Δ ⊢⇩w⇩f s : b;
    Θ; ℬ; Γ ⊢⇩w⇩f c ;
    Θ; ℬ; Γ ⊢⇩w⇩f Δ ;
    atom x ♯ (Φ, Θ, ℬ, Γ, Δ, c, b, s)
⟧ ⟹ 
    Θ; Φ; ℬ; Γ; Δ ⊢⇩w⇩f ASSERT c IN  s : b"

| wfS_let2I: "⟦ 
   Θ; Φ; ℬ; Γ; Δ  ⊢⇩w⇩f s1 : b_of τ  ; 
   Θ; ℬ; Γ ⊢⇩w⇩f τ;
   Θ ; Φ ; ℬ ; (x,b_of τ,C_true) #⇩Γ Γ ; Δ ⊢⇩w⇩f s2 : b ;
   atom x ♯ (Φ, Θ, ℬ, Γ, Δ, s1, b,τ)            
⟧ ⟹ 
   Θ; Φ; ℬ; Γ; Δ ⊢⇩w⇩f LET x : τ = s1 IN s2 : b"

| wfS_ifI: "⟦  
   Θ; ℬ; Γ ⊢⇩w⇩f v  : B_bool; 
   Θ; Φ; ℬ; Γ; Δ ⊢⇩w⇩f s1 : b ; 
   Θ; Φ; ℬ; Γ; Δ ⊢⇩w⇩f s2 : b 
⟧ ⟹
   Θ; Φ; ℬ; Γ; Δ ⊢⇩w⇩f IF v THEN s1 ELSE s2 : b"

| wfS_varI : "⟦ 
   wfT Θ ℬ Γ  τ ;  
   Θ; ℬ; Γ ⊢⇩w⇩f v  : b_of τ; 
   atom u ♯ (Φ, Θ, ℬ, Γ, Δ, τ, v, b);
   Θ ; Φ ; ℬ ; Γ ;  (u,τ)#⇩ΔΔ ⊢⇩w⇩f s : b 
⟧ ⟹ 
   Θ; Φ; ℬ; Γ; Δ ⊢⇩w⇩f VAR u : τ = v IN s : b "

| wfS_assignI: "⟦ 
   (u,τ) ∈ setD Δ ;   
   Θ; ℬ; Γ ⊢⇩w⇩f Δ ;  
   Θ ⊢⇩w⇩f Φ ;
   Θ; ℬ; Γ ⊢⇩w⇩f v  : b_of τ 
⟧ ⟹
   Θ; Φ; ℬ; Γ; Δ ⊢⇩w⇩f u ::= v : B_unit"

| wfS_whileI: "⟦ 
  Θ; Φ; ℬ; Γ; Δ ⊢⇩w⇩f s1 : B_bool ; 
  Θ; Φ; ℬ; Γ; Δ ⊢⇩w⇩f s2 : b
⟧ ⟹  
  Θ; Φ; ℬ; Γ; Δ ⊢⇩w⇩f WHILE s1 DO { s2 } : b"

| wfS_seqI: "⟦
  Θ; Φ; ℬ; Γ; Δ ⊢⇩w⇩f s1 : B_unit ; 
  Θ; Φ; ℬ; Γ; Δ ⊢⇩w⇩f s2 : b 
⟧ ⟹ 
  Θ; Φ; ℬ; Γ; Δ ⊢⇩w⇩f s1 ;; s2 : b"

| wfS_matchI: "⟦ 
  wfV Θ  ℬ Γ  v  (B_id tid) ;
  (AF_typedef tid dclist ) ∈ set Θ;
  wfD Θ  ℬ Γ  Δ ;  
  Θ ⊢⇩w⇩f Φ ;
  Θ ; Φ ; ℬ ; Γ ;  Δ ; tid ; dclist ⊢⇩w⇩f cs : b 
⟧ ⟹ 
  Θ; Φ; ℬ; Γ; Δ ⊢⇩w⇩f AS_match v cs : b "

| wfS_branchI: "⟦ 
  Θ ; Φ ; ℬ ; (x,b_of τ,C_true) #⇩Γ Γ ;  Δ ⊢⇩w⇩f s : b ;
  atom x ♯ (Φ, Θ, ℬ, Γ, Δ, Γ,τ);
  Θ; ℬ; Γ ⊢⇩w⇩f Δ 
⟧  ⟹ 
  Θ ; Φ ; ℬ ; Γ ;  Δ ; tid ; dc ;  τ  ⊢⇩w⇩f  dc x ⇒ s : b"

| wfS_finalI: "⟦       
  Θ; Φ; ℬ; Γ; Δ ; tid ; dc ; t  ⊢⇩w⇩f cs : b    
 ⟧ ⟹  
  Θ ; Φ ; ℬ ; Γ ;  Δ ; tid ; [(dc,t)] ⊢⇩w⇩f AS_final cs  : b "

| wfS_cons: "⟦           
  Θ; Φ; ℬ; Γ; Δ ; tid ; dc ; t  ⊢⇩w⇩f cs : b;
  Θ; Φ; ℬ; Γ; Δ ; tid ; dclist ⊢⇩w⇩f css : b
 ⟧ ⟹  
  Θ ; Φ ; ℬ ; Γ ;  Δ ; tid ; (dc,t)#dclist ⊢⇩w⇩f AS_cons cs css : b "

| wfD_emptyI: "Θ; ℬ ⊢⇩w⇩f Γ ⟹ Θ  ; ℬ ; Γ  ⊢⇩w⇩f []⇩Δ"

| wfD_cons: "⟦ 
  Θ  ; ℬ ; Γ  ⊢⇩w⇩f Δ::Δ ; 
  Θ  ; ℬ ; Γ ⊢⇩w⇩f τ; 
  u ∉ fst ` setD Δ 
⟧ ⟹ 
  Θ; ℬ; Γ ⊢⇩w⇩f ((u,τ) #⇩Δ Δ)"

| wfPhi_emptyI: " ⊢⇩w⇩f Θ ⟹ Θ ⊢⇩w⇩f []"

| wfPhi_consI: "⟦ 
  f ∉ name_of_fun ` set Φ; 
  Θ ; Φ  ⊢⇩w⇩f ft;
  Θ ⊢⇩w⇩f Φ
⟧ ⟹  
  Θ  ⊢⇩w⇩f ((AF_fundef f ft)#Φ)"  

| wfFTNone: " Θ ; Φ ; {||} ⊢⇩w⇩f ft ⟹  Θ ; Φ ⊢⇩w⇩f AF_fun_typ_none ft"
| wfFTSome: " Θ ; Φ ; {| bv |} ⊢⇩w⇩f ft ⟹  Θ ; Φ ⊢⇩w⇩f AF_fun_typ_some bv ft"

| wfFTI: "⟦
  Θ ; B  ⊢⇩w⇩f b; 
  supp s ⊆ {atom x} ∪ supp B ;
  supp c ⊆ { atom x } ;
  Θ ; B ; (x,b,c) #⇩Γ GNil ⊢⇩w⇩f τ;
  Θ ⊢⇩w⇩f Φ        
⟧ ⟹ 
  Θ ; Φ ; B ⊢⇩w⇩f (AF_fun_typ x b c τ s)"

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

inductive_cases wfCS_elims:
  "Θ; Φ; ℬ; Γ; Δ ; tid ; dc ; t ⊢⇩w⇩f (cs::branch_s) : b"
  "Θ; Φ; ℬ; Γ; Δ ; tid ; dc  ⊢⇩w⇩f (cs::branch_list) : b"

inductive_cases wfPhi_elims:
  " Θ  ⊢⇩w⇩f []"
  " Θ  ⊢⇩w⇩f ((AF_fundef f ft)#Π)"  
  " Θ  ⊢⇩w⇩f (fd#Φ::Φ)"  

declare[[ simproc del: alpha_lst]]

inductive_cases wfFTQ_elims:
  "Θ ; Φ  ⊢⇩w⇩f AF_fun_typ_none ft"
  "Θ ; Φ  ⊢⇩w⇩f AF_fun_typ_some bv ft"
  "Θ ; Φ  ⊢⇩w⇩f AF_fun_typ_some bv (AF_fun_typ x b c τ s)"

inductive_cases wfFT_elims:
  "Θ ; Φ ; ℬ  ⊢⇩w⇩f AF_fun_typ x b c τ s"

declare[[ simproc add: alpha_lst]]

inductive_cases wfD_elims:
  "Π ; ℬ ; (Γ::Γ) ⊢⇩w⇩f []⇩Δ"
  "Π ; ℬ ; (Γ::Γ) ⊢⇩w⇩f (u,τ) #⇩Δ Δ::Δ"

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' 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' bv v τ f x b c s)
  then show ?case by auto
next
  case (3 Φ Θ ℬ Γ Δ 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 Φ Θ ℬ Γ Δ e b' x s b)
  then show ?case by auto
next
  case (5 Θ Φ ℬ 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 Θ Φ ℬ x c Γ Δ s b)
  then show ?case by auto
next
  case (7 Φ Θ ℬ Γ Δ 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 Φ Θ ℬ Γ Δ s1 τ x s2 b)
  then show ?case by auto
next
  case (9 Θ ℬ Γ τ 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 Θ ℬ Γ τ v u Φ Δ b s)
  then show ?case by auto
next
  case (11 Φ Θ ℬ 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 Φ Θ ℬ 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
⟧ ⟹ wfVDs  ((AV_def u τ v)#ts)"

equivariance wfVDs 
nominal_inductive wfVDs .  

end