Quelle  Operational.thy

(*<*)
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]_sv⟩"  
| 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]_\<tau>_v s'[z::=v]_sv 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']_\<tau>_b[z::=v]_\<tau>_v s'[bv::=b']_sb[z::=v]_sv 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]_sv⟩" 
| 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]_sv⟩ "
| 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> "
| delta_sim_consI: "[ Θ ⊨ δ ∼ Δ ; Θ ; {||} ; GNil ⊨ v <== τ ; u ∉ fst ` set δ ] ==> Θ ⊨ ((u,v)#δ) ∼ ((u,τ)#_\<Delta>Δ)" 

equivariance delta_sim
nominal_inductive delta_sim .

inductive_cases delta_sim_elims[elim!]:
  "Θ ⊨ [] ∼ []_\<Delta>"
  "Θ ⊨ ((u,v)#ds) ∼ (u,τ) #_\<Delta> 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 G ⊨ ⟨ δ_of G , s⟩ <== τ
\<rbrakk> ==> ⊨ ⟨ AP_prog Θ Φ G s⟩ <== τ"

inductive_cases config_type_prog_elims [elim!]:
  "⊨ ⟨ AP_prog Θ Φ G s⟩ <== τ"

end