Theory BigSmallInvariants

chapter ‹Generated by Lem from ‹semantics/alt_semantics/proofs/bigSmallInvariants.lem›.›

theory "BigSmallInvariants" 

imports
  Main
  "HOL-Library.Datatype_Records"
  "LEM.Lem_pervasives"
  "Lib"
  "Namespace"
  "Ast"
  "SemanticPrimitives"
  "SmallStep"
  "BigStep"

begin 

― ‹‹open import Pervasives››
― ‹‹open import Lib››
― ‹‹open import Namespace››
― ‹‹open import Ast››
― ‹‹open import SemanticPrimitives››
― ‹‹open import SmallStep››
― ‹‹open import BigStep››

― ‹‹ ------ Auxiliary relations for proving big/small step equivalence ------ ››

inductive
evaluate_ctxt  :: "(v)sem_env ⇒ 'ffi state ⇒ ctxt_frame ⇒ v ⇒ 'ffi state*((v),(v))result ⇒ bool "  where

"raise" : " ⋀ env s v1.

evaluate_ctxt env s (Craise () ) v1 (s, Rerr (Rraise v1))"

|

"handle" : " ⋀ env s v1 pes.

evaluate_ctxt env s (Chandle ()  pes) v1 (s, Rval v1)"

|

"app1" : " ⋀ env e v1 vs1 vs2 es env' bv s1 s2.
evaluate_list False env s1 es (s2, Rval vs2) ∧
((do_opapp ((List.rev vs2 @ [v1]) @ vs1) = Some (env',e)) ∧
evaluate False env' s2 e bv)
==>
evaluate_ctxt env s1 (Capp Opapp vs1 ()  es) v1 bv "

|

"app2" : " ⋀ env v1 vs1 vs2 es s1 s2.
evaluate_list False env s1 es (s2, Rval vs2) ∧
(do_opapp ((List.rev vs2 @ [v1]) @ vs1) = None)
==>
evaluate_ctxt env s1 (Capp Opapp vs1 ()  es) v1 (s2, Rerr (Rabort Rtype_error))"

|

"app3" : " ⋀ env op0 v1 vs1 vs2 es res s1 s2 new_refs new_ffi.
(op0 ≠ Opapp) ∧
(evaluate_list False env s1 es (s2, Rval vs2) ∧
(do_app ((refs   s2),(ffi   s2)) op0 ((List.rev vs2 @ [v1]) @ vs1) = Some ((new_refs, new_ffi) ,res)))
==>
evaluate_ctxt env s1 (Capp op0 vs1 ()  es) v1 (( s2 (| ffi := new_ffi, refs := new_refs |)), res)"

|

"app4" : " ⋀ env op0 v1 vs1 vs2 es s1 s2.
(op0 ≠ Opapp) ∧
(evaluate_list False env s1 es (s2, Rval vs2) ∧
(do_app ((refs   s2),(ffi   s2)) op0 ((List.rev vs2 @ [v1]) @ vs1) = None))
==>
evaluate_ctxt env s1 (Capp op0 vs1 ()  es) v1 (s2, Rerr (Rabort Rtype_error))"

|

"app5" : " ⋀ env op0 es vs v1 err s s'.
evaluate_list False env s es (s', Rerr err)
==>
evaluate_ctxt env s (Capp op0 vs ()  es) v1 (s', Rerr err)"

|

"log1" : " ⋀ env op0 e2 v1 e' bv s.
(do_log op0 v1 e2 = Some (Exp e')) ∧
evaluate False env s e' bv
==>
evaluate_ctxt env s (Clog op0 ()  e2) v1 bv "

|

"log2" : " ⋀ env op0 e2 v1 v' s.
do_log op0 v1 e2 = Some (Val v')
==>
evaluate_ctxt env s (Clog op0 ()  e2) v1 (s, Rval v')"

|

"log3" : " ⋀ env op0 e2 v1 s.
(do_log op0 v1 e2 = None)
==>
evaluate_ctxt env s (Clog op0 ()  e2) v1 (s, Rerr (Rabort Rtype_error))"

|
"if1" : " ⋀ env e2 e3 v1 e' bv s.
(do_if v1 e2 e3 = Some e') ∧
evaluate False env s e' bv
==>
evaluate_ctxt env s (Cif ()  e2 e3) v1 bv "

|

"if2" : " ⋀ env e2 e3 v1 s.
do_if v1 e2 e3 = None
==>
evaluate_ctxt env s (Cif ()  e2 e3) v1 (s, Rerr (Rabort Rtype_error))"

|

"mat" : " ⋀ env pes v1 bv s err_v.
evaluate_match False env s v1 pes err_v bv
==>
evaluate_ctxt env s (Cmat ()  pes err_v) v1 bv "

|

"lt" : " ⋀ env n e2 v1 bv s.
evaluate False ( env (| v := (nsOptBind n v1(v   env)) |)) s e2 bv
==>
evaluate_ctxt env s (Clet n ()  e2) v1 bv "

|

"con1" : " ⋀ env cn es vs v1 vs' s1 s2 v'.
do_con_check(c   env) cn ((List.length vs + List.length es) +( 1 :: nat)) ∧
((build_conv(c   env) cn ((List.rev vs' @ [v1]) @ vs) = Some v') ∧
evaluate_list False env s1 es (s2, Rval vs'))
==>
evaluate_ctxt env s1 (Ccon cn vs ()  es) v1 (s2, Rval v')"

|

"con2" : " ⋀ env cn es vs v1 s.
¬ (do_con_check(c   env) cn ((List.length vs + List.length es) +( 1 :: nat)))
==>
evaluate_ctxt env s (Ccon cn vs ()  es) v1 (s, Rerr (Rabort Rtype_error))"

|

"con3" : " ⋀ env cn es vs v1 err s s'.
do_con_check(c   env) cn ((List.length vs + List.length es) +( 1 :: nat)) ∧
evaluate_list False env s es (s', Rerr err)
==>
evaluate_ctxt env s (Ccon cn vs ()  es) v1 (s', Rerr err)"

|

"tannot" : " ⋀ env v1 s t0.

evaluate_ctxt env s (Ctannot ()  t0) v1 (s, Rval v1)"

|

"lannot" : " ⋀ env v1 s l.

evaluate_ctxt env s (Clannot ()  l) v1 (s, Rval v1)"

inductive
evaluate_ctxts  :: " 'ffi state ⇒(ctxt)list ⇒((v),(v))result ⇒ 'ffi state*((v),(v))result ⇒ bool "  where

"empty" : " ⋀ res s.

evaluate_ctxts s [] res (s, res)"

|

"cons_val" : " ⋀ c1 cs env v1 res bv s1 s2.
evaluate_ctxt env s1 c1 v1 (s2, res) ∧
evaluate_ctxts s2 cs res bv
==>
evaluate_ctxts s1 ((c1,env)# cs) (Rval v1) bv "

|

"cons_err" : " ⋀ c1 cs env err s bv.
evaluate_ctxts s cs (Rerr err) bv ∧
(((∀ pes.  c1 ≠ Chandle ()  pes)) ∨
 ((∀ v1.  err ≠ Rraise v1)))
==>
evaluate_ctxts s ((c1,env)# cs) (Rerr err) bv "

|

"cons_handle" : " ⋀ cs env s s' res1 res2 pes v1.
evaluate_match False env s v1 pes v1 (s', res1) ∧
evaluate_ctxts s' cs res1 res2
==>
evaluate_ctxts s ((Chandle ()  pes,env)# cs) (Rerr (Rraise v1)) res2 "

inductive
evaluate_state  :: " 'ffi small_state ⇒ 'ffi state*((v),(v))result ⇒ bool "  where

"exp" : " ⋀ env e c1 res bv ffi0 refs0 st.
evaluate False env  (| clock =(( 0 :: nat)), refs = refs0, ffi = ffi0, defined_types = ({}), defined_mods = 
 ({})  |) e (st, res) ∧
evaluate_ctxts st c1 res bv
==>
evaluate_state (env, (refs0, ffi0), Exp e, c1) bv "

|

"vl" : " ⋀ env ffi0 refs0 v1 c1 bv.
evaluate_ctxts  (| clock =(( 0 :: nat)), refs = refs0, ffi = ffi0, defined_types = ({}), defined_mods = 
 ({})  |) c1 (Rval v1) bv
==>
evaluate_state (env, (refs0, ffi0), Val v1, c1) bv "
end