Theory Operational

(*<*)
theory Operational
  imports Typing
begin
  (*>*)

chapter ‹Operational Semantics›

text ‹ Here we define the operational semantics in terms of a small-step reduction relation. ›

section ‹Reduction Rules›

text ‹ The store for mutable variables ›
type_synonym δ = "(u*v) list"

nominal_function update_d :: "δ ⇒ u ⇒ v ⇒ δ" where
  "update_d [] _ _ = []"
| "update_d ((u',v')#δ) u v = (if u = u' then ((u,v)#δ) else ((u',v')# (update_d δ u v)))"
  by(auto,simp add: eqvt_def update_d_graph_aux_def ,metis neq_Nil_conv old.prod.exhaust)
nominal_termination (eqvt) by lexicographic_order

text ‹ Relates constructor to the branch in the case and binding variable and statement ›
inductive find_branch :: "dc ⇒ branch_list  ⇒ branch_s  ⇒ bool" where
  find_branch_finalI:  "dc' = dc                                  ⟹ find_branch dc' (AS_final (AS_branch dc x s ))  (AS_branch dc x s)"
| find_branch_branch_eqI: "dc' = dc                               ⟹ find_branch dc' (AS_cons  (AS_branch dc x s) css)    (AS_branch dc x s)"
| find_branch_branch_neqI:  "⟦ dc ≠ dc'; find_branch dc' css cs ⟧ ⟹ find_branch dc' (AS_cons  (AS_branch dc x s) css) cs"
equivariance find_branch
nominal_inductive find_branch .

inductive_cases find_branch_elims[elim!]:
  "find_branch dc (AS_final cs') cs"
  "find_branch dc (AS_cons cs' css) cs"

nominal_function lookup_branch :: "dc ⇒ branch_list ⇒ branch_s option" where
  "lookup_branch dc (AS_final (AS_branch dc' x s)) = (if dc = dc' then (Some (AS_branch dc' x s)) else None)"
| "lookup_branch dc (AS_cons (AS_branch dc' x s) css) = (if dc = dc' then (Some (AS_branch dc' x s)) else lookup_branch dc css)"
       apply(auto,simp add: eqvt_def lookup_branch_graph_aux_def)
  by(metis neq_Nil_conv old.prod.exhaust s_branch_s_branch_list.strong_exhaust)
nominal_termination (eqvt) by lexicographic_order

text ‹ Reduction rules ›
inductive reduce_stmt :: "Φ ⇒ δ ⇒ s ⇒ δ ⇒ s ⇒ bool"  (" _  ⊢ ⟨ _ , _⟩ ⟶ ⟨  _ , _⟩" [50, 50, 50] 50)  where
  reduce_if_trueI:  " Φ ⊢ ⟨δ, AS_if [L_true]⇧v s1 s2⟩ ⟶ ⟨δ, s1⟩ "
| reduce_if_falseI: " Φ ⊢ ⟨δ, AS_if [L_false]⇧v s1 s2⟩ ⟶ ⟨δ, s2⟩ "
| reduce_let_valI:  " Φ ⊢ ⟨δ, AS_let x (AE_val v)  s⟩ ⟶ ⟨δ, s[x::=v]⇩s⇩v⟩"  
| reduce_let_plusI: " Φ ⊢  ⟨δ, AS_let x (AE_op Plus ((V_lit (L_num n1))) ((V_lit (L_num n2))))  s⟩ ⟶ 
                           ⟨δ, AS_let x (AE_val (V_lit (L_num ( (( n1)+(n2)))))) s ⟩ "  
| reduce_let_leqI:  "b = (if (n1 ≤ n2) then L_true else L_false) ⟹ 
             Φ  ⊢  ⟨δ,  AS_let x  ((AE_op LEq (V_lit (L_num n1)) (V_lit (L_num n2)))) s⟩ ⟶ 
                                                          ⟨δ, AS_let x  (AE_val (V_lit b)) s⟩"  
| reduce_let_eqI:  "b = (if (n1 = n2) then L_true else L_false) ⟹ 
             Φ  ⊢  ⟨δ,  AS_let x  ((AE_op Eq (V_lit n1) (V_lit n2))) s⟩ ⟶ 
                                                          ⟨δ, AS_let x  (AE_val (V_lit b)) s⟩"  
| reduce_let_appI:  "Some (AF_fundef f (AF_fun_typ_none (AF_fun_typ z b c τ s'))) = lookup_fun Φ f ⟹  
             Φ  ⊢  ⟨δ, AS_let x  ((AE_app f v)) s⟩ ⟶ ⟨δ,  AS_let2 x τ[z::=v]⇩τ⇩v s'[z::=v]⇩s⇩v s⟩ "     
| reduce_let_appPI:  "Some (AF_fundef f (AF_fun_typ_some bv (AF_fun_typ z b c τ s'))) = lookup_fun Φ f ⟹  
             Φ  ⊢  ⟨δ, AS_let x  ((AE_appP f b' v)) s⟩ ⟶ ⟨δ,  AS_let2 x τ[bv::=b']⇩τ⇩b[z::=v]⇩τ⇩v s'[bv::=b']⇩s⇩b[z::=v]⇩s⇩v s⟩ "  
| reduce_let_fstI:  "Φ ⊢ ⟨δ, AS_let x (AE_fst (V_pair v1 v2))  s⟩ ⟶ ⟨δ, AS_let x (AE_val v1)  s⟩"
| reduce_let_sndI:  "Φ ⊢ ⟨δ, AS_let x (AE_snd (V_pair v1 v2))  s⟩ ⟶ ⟨δ, AS_let x (AE_val v2)  s⟩"
| reduce_let_concatI:  "Φ ⊢ ⟨δ, AS_let x (AE_concat (V_lit (L_bitvec v1))  (V_lit (L_bitvec v2)))  s⟩ ⟶ 
                            ⟨δ, AS_let x (AE_val (V_lit (L_bitvec (v1@v2))))  s⟩"
| reduce_let_splitI: " split n v (v1 , v2 )  ⟹ Φ ⊢ ⟨δ, AS_let x (AE_split (V_lit (L_bitvec v))  (V_lit (L_num n)))  s⟩ ⟶ 
                            ⟨δ, AS_let x (AE_val (V_pair (V_lit (L_bitvec v1)) (V_lit (L_bitvec v2))))  s⟩"
| reduce_let_lenI:  "Φ ⊢ ⟨δ, AS_let x (AE_len (V_lit (L_bitvec v)))  s⟩ ⟶ 
                              ⟨δ, AS_let x (AE_val (V_lit (L_num (int (List.length v)))))  s⟩"
| reduce_let_mvar:  "(u,v) ∈ set δ ⟹  Φ ⊢ ⟨δ, AS_let x (AE_mvar u)  s⟩ ⟶ ⟨δ, AS_let x (AE_val v) s ⟩" 
| reduce_assert1I: "Φ ⊢ ⟨δ, AS_assert c (AS_val v)⟩ ⟶ ⟨δ, AS_val v⟩" 
| reduce_assert2I:  " Φ  ⊢ ⟨δ, s ⟩ ⟶ ⟨ δ', s'⟩ ⟹ Φ  ⊢ ⟨δ, AS_assert c s⟩ ⟶ ⟨ δ', AS_assert c s'⟩"  
| reduce_varI: "atom u ♯ δ ⟹  Φ  ⊢  ⟨δ, AS_var u τ v s ⟩ ⟶ ⟨ ((u,v)#δ) , s⟩"
| reduce_assignI: "  Φ  ⊢  ⟨δ, AS_assign u v ⟩ ⟶ ⟨ update_d δ u v , AS_val (V_lit L_unit)⟩"
| reduce_seq1I: "Φ   ⊢  ⟨δ, AS_seq (AS_val (V_lit L_unit )) s ⟩ ⟶ ⟨δ, s⟩"
| reduce_seq2I: "⟦s1 ≠ AS_val v ; Φ  ⊢  ⟨δ, s1⟩ ⟶ ⟨ δ', s1'⟩ ⟧ ⟹ 
                          Φ  ⊢  ⟨δ, AS_seq s1 s2⟩ ⟶ ⟨ δ', AS_seq s1' s2⟩"
| reduce_let2_valI:  "Φ  ⊢  ⟨δ, AS_let2 x t (AS_val v) s⟩ ⟶ ⟨δ, s[x::=v]⇩s⇩v⟩" 
| reduce_let2I:  " Φ  ⊢ ⟨δ, s1 ⟩ ⟶ ⟨ δ', s1'⟩ ⟹ Φ  ⊢ ⟨δ, AS_let2 x t s1 s2⟩ ⟶ ⟨ δ', AS_let2 x t s1' s2⟩"  

| reduce_caseI:  "⟦ Some (AS_branch dc x' s') = lookup_branch dc cs ⟧ ⟹  Φ ⊢  ⟨δ, AS_match (V_cons tyid dc v) cs⟩  ⟶ ⟨δ, s'[x'::=v]⇩s⇩v⟩ "
| reduce_whileI: "⟦ atom x ♯ (s1,s2); atom z ♯ x ⟧ ⟹ 
                    Φ  ⊢  ⟨δ, AS_while s1 s2 ⟩ ⟶ 
            ⟨δ, AS_let2 x (⦃ z : B_bool | TRUE ⦄) s1 (AS_if (V_var x) (AS_seq s2 (AS_while s1 s2))  (AS_val (V_lit L_unit))) ⟩"

equivariance reduce_stmt
nominal_inductive reduce_stmt .

inductive_cases reduce_stmt_elims[elim!]:
  "Φ ⊢ ⟨δ, AS_if (V_lit L_true) s1 s2⟩ ⟶ ⟨δ , s1⟩"
  "Φ ⊢ ⟨δ, AS_if (V_lit L_false) s1 s2⟩ ⟶ ⟨δ,s2⟩"
  "Φ ⊢ ⟨δ, AS_let x (AE_val v)  s⟩ ⟶ ⟨δ,s'⟩"
  "Φ ⊢ ⟨δ, AS_let x  (AE_op Plus ((V_lit (L_num n1))) ((V_lit (L_num n2))))  s⟩ ⟶ 
            ⟨δ, AS_let x  (AE_val (V_lit (L_num ( (( n1)+(n2)))))) s ⟩"
  "Φ ⊢ ⟨δ, AS_let x  ((AE_op LEq (V_lit (L_num n1)) (V_lit (L_num n2)))) s⟩ ⟶ ⟨δ, AS_let x  (AE_val (V_lit b)) s⟩"
  "Φ ⊢ ⟨δ, AS_let x  ((AE_app f v)) s⟩ ⟶ ⟨δ, AS_let2 x τ (subst_sv s' x v ) s⟩ "  
  "Φ ⊢ ⟨δ, AS_let x  ((AE_len v)) s⟩ ⟶ ⟨δ, AS_let x  v' s⟩ "  
  "Φ ⊢ ⟨δ, AS_let x  ((AE_concat v1 v2)) s⟩ ⟶ ⟨δ, AS_let x  v' s⟩ " 
  "Φ ⊢ ⟨δ, AS_seq s1 s2⟩ ⟶ ⟨ δ' ,s'⟩"
  "Φ ⊢ ⟨δ, AS_let x  ((AE_appP  f b v)) s⟩ ⟶ ⟨δ, AS_let2 x τ (subst_sv s' z v) s⟩ "  
  "Φ ⊢ ⟨δ, AS_let x  ((AE_split v1 v2)) s⟩ ⟶ ⟨δ, AS_let x  v' s⟩ " 
  "Φ ⊢ ⟨δ, AS_assert c s ⟩ ⟶ ⟨δ, s'⟩ "
  "Φ ⊢ ⟨δ, AS_let x  ((AE_op Eq (V_lit (n1)) (V_lit (n2)))) s⟩ ⟶ ⟨δ, AS_let x  (AE_val (V_lit b)) s⟩"

inductive reduce_stmt_many :: "Φ ⇒ δ ⇒ s ⇒ δ ⇒ s ⇒ bool"    ("_ ⊢ ⟨ _ , _⟩ ⟶⇧* ⟨  _ , _⟩" [50, 50, 50] 50)  where  
  reduce_stmt_many_oneI:  "Φ ⊢ ⟨δ, s⟩ ⟶ ⟨δ', s'⟩  ⟹ Φ ⊢ ⟨δ  , s⟩ ⟶⇧* ⟨δ', s'⟩ "
| reduce_stmt_many_manyI:  "⟦ Φ ⊢ ⟨δ, s⟩ ⟶   ⟨δ', s'⟩ ; Φ ⊢  ⟨δ', s'⟩ ⟶⇧* ⟨δ'', s''⟩ ⟧ ⟹ Φ ⊢  ⟨δ, s⟩ ⟶⇧* ⟨δ'', s''⟩"

nominal_function  convert_fds :: "fun_def list ⇒ (f*fun_def) list" where
  "convert_fds [] = []"
| "convert_fds ((AF_fundef f (AF_fun_typ_none (AF_fun_typ x b c τ s)))#fs) = ((f,AF_fundef f (AF_fun_typ_none (AF_fun_typ x b c τ s)))#convert_fds fs)"
| "convert_fds ((AF_fundef f (AF_fun_typ_some bv (AF_fun_typ x b c τ s)))#fs) = ((f,AF_fundef f (AF_fun_typ_some bv (AF_fun_typ x b c τ s)))#convert_fds fs)"
  apply(auto)
  apply (simp add: eqvt_def convert_fds_graph_aux_def )
  using fun_def.exhaust fun_typ.exhaust fun_typ_q.exhaust neq_Nil_conv 
  by metis
nominal_termination (eqvt) by lexicographic_order

nominal_function  convert_tds :: "type_def list ⇒ (f*type_def) list" where
  "convert_tds [] = []"
| "convert_tds ((AF_typedef s dclist)#fs) = ((s,AF_typedef s dclist)#convert_tds fs)"
| "convert_tds ((AF_typedef_poly s bv dclist)#fs) = ((s,AF_typedef_poly s bv dclist)#convert_tds fs)"
  apply(auto)
  apply (simp add: eqvt_def convert_tds_graph_aux_def )
  by (metis type_def.exhaust neq_Nil_conv)
nominal_termination (eqvt) by lexicographic_order

inductive reduce_prog :: "p ⇒ v ⇒ bool" where
  "⟦ reduce_stmt_many Φ [] s δ (AS_val v) ⟧ ⟹  reduce_prog (AP_prog Θ Φ [] s) v"

section ‹Reduction Typing›

text ‹ Checks that the store is consistent with @{typ Δ} ›
inductive delta_sim :: "Θ ⇒ δ ⇒ Δ ⇒ bool" ( "_  ⊢ _ ∼ _ " [50,50] 50 )  where
  delta_sim_nilI:  "Θ ⊢ [] ∼ []⇩Δ "
| delta_sim_consI: "⟦ Θ ⊢ δ ∼ Δ ; Θ ; {||} ; GNil ⊢ v ⇐ τ ; u ∉ fst ` set δ   ⟧ ⟹ Θ ⊢ ((u,v)#δ) ∼ ((u,τ)#⇩ΔΔ)" 

equivariance delta_sim
nominal_inductive delta_sim .

inductive_cases delta_sim_elims[elim!]:
  "Θ ⊢ [] ∼ []⇩Δ"
  "Θ ⊢ ((u,v)#ds) ∼ (u,τ) #⇩Δ D"
  "Θ ⊢ ((u,v)#ds) ∼ D"

text ‹A typing judgement that combines typing of the statement, the store and the condition that definitions are well-typed›
inductive config_type ::  "Θ ⇒ Φ ⇒ Δ ⇒ δ ⇒ s ⇒ τ ⇒  bool"   ("_ ; _ ; _ ⊢ ⟨ _ , _⟩ ⇐ _ " [50, 50, 50] 50)  where 
  config_typeI: "⟦ Θ ; Φ ; {||} ; GNil ; Δ ⊢ s ⇐ τ; 
                (∀ fd ∈ set Φ. Θ ; Φ ⊢ fd) ;
                Θ  ⊢ δ ∼ Δ ⟧
                ⟹ Θ ; Φ ; Δ ⊢ ⟨ δ  , s⟩ ⇐  τ"
equivariance config_type
nominal_inductive config_type .

inductive_cases config_type_elims [elim!]:
  " Θ ; Φ  ; Δ ⊢ ⟨ δ  , s⟩ ⇐  τ"

nominal_function δ_of  :: "var_def list ⇒ δ" where
  "δ_of [] = []"
| "δ_of ((AV_def u t v)#vs) = (u,v) #  (δ_of vs)" 
  apply auto
  using  eqvt_def δ_of_graph_aux_def neq_Nil_conv old.prod.exhaust apply force
  using  eqvt_def δ_of_graph_aux_def neq_Nil_conv old.prod.exhaust 
  by (metis var_def.strong_exhaust)
nominal_termination (eqvt) by lexicographic_order

inductive config_type_prog :: "p ⇒ τ ⇒ bool"  (" ⊢ ⟨ _⟩ ⇐ _") where
  "⟦
  Θ ; Φ ; Δ_of 𝒢 ⊢ ⟨ δ_of 𝒢  , s⟩ ⇐  τ
⟧ ⟹ ⊢  ⟨ AP_prog Θ Φ 𝒢 s⟩ ⇐ τ"

inductive_cases config_type_prog_elims [elim!]:
  "⊢  ⟨ AP_prog Θ Φ 𝒢 s⟩ ⇐ τ"

end