# Theory Dyn

Up to index of Isabelle/HOL/sHowe

theory Dyn = Closed
files [Dyn.ML]:
```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`