Theory Dyn

Up to index of Isabelle/HOL/sHowe

Dyn = Closed +

consts


eval :: "(uexp  * uexp) set"
value :: "(uexp) set"



syntax 

 ">>"  :: [uexp, uexp] => bool   (infixl 50)
"@value"  :: "uexp => bool"



translations

"e >> v" == "(e,v) : eval"

"value e"  == "(e) : value "



constdefs

  converges :: uexp  => bool
  "converges p == ? v. p >> v"




inductive eval
intrs
eval_abs  "cloAbstr E  ==> (lam x . E x) >> (lam x.  E x)"
eval_app  "[|p1 >> (lam x . N x); cloAbstr N; cloexp p2; (N p2) >> v|] ==> (p1 $ p2) >> v"


inductive value
intrs
(* valabs "[|abstr E; !p. cloexp p --> cloexp (E p)|] ==> value (lam x .  E x)"*)
valabs "[|cloAbstr E |] ==> value (lam x .  E x)"


end

Big Step Evaluation

theorem eval_Abs_E:

  [| bLam E >> v;
     !!Ea. [| cloAbstr Ea; lambda E = lambda Ea; v = bLam Ea |] ==> P |]
  ==> P

theorem eval_App_E:

  [| e $ e1 >> v;
     !!N p1 p2.
        [| p1 >> bLam N; cloAbstr N; cloexp p2; N p2 >> v; e = p1 & e1 = p2 |]
        ==> P |]
  ==> P

theorem eval_cloexp:

  e >> v ==> cloexp e & cloexp v

theorem eval_determ:

  e >> v ==> ALL v1. e >> v1 --> v = v1

Convergence

theorem convergesE:

  [| converges p; !!v. p >> v ==> Q |] ==> Q

theorem converges_App:

  converges (f $ p) ==> converges f

Values

theorem value_sound:

  e >> v ==> value v

theorem val_to_eval:

  value v ==> v >> v

theorem value_cloexp:

  value v ==> cloexp v

theorem eval_value:

  p >> v ==> v >> v