Theory Sim

Up to index of Isabelle/HOL/sHowe

theory Sim = Kleene
files [Sim.ML]:
```(*
File: Sim.thy
Author: Simon Ambler (sja4@mcs.le.ac.uk), modified by AM

Simulation for terms under normal order reduction.
*)

Sim = Kleene  +

consts

sim    :: "(uexp * uexp ) set"

syntax

"@sim" :: "[uexp,uexp] => bool"
("((_) /<sim> (_) )" [50,50] 50)

translations
"s <sim> t " == "(s,t) : sim"

constdefs

bisim :: "[uexp,uexp] => bool"
("(_) /=~= (_) " [50,50] 50)
"s =~= t  == s <sim> t  & t <sim> s"

coinductive sim
intrs

sim_Fun

"[|cloexp r; cloexp s;! t. r >> lam x . t x --> ( cloAbstr t  --> (? u. s >> lam x . u x & cloAbstr u  &
(! p.  cloexp p --> (t  p) <sim> (u  p)  )))|] ==> r <sim> s"

end```

Simulation

theorem sim_cloexp:

`  s <sim> t  ==> cloexp s & cloexp t`

theorem sim_refl:

`  cloexp s ==> s <sim> s `

theorem sim_trans:

`  [| s <sim> t ; t <sim> u  |] ==> s <sim> u `

theorem kleene_sim:

`  p <kleene> q  ==> p <sim> q `

theorem sim_beta_conv1:

`  [| cloAbstr e; cloexp t |] ==> (lam x. e x) \$ t <sim> e t `

theorem sim_beta_conv2:

`  [| cloAbstr e; cloexp t |] ==> e t <sim> (lam x. e x) \$ t `

theorem sim_eval1:

`  p >> q ==> p <sim> q `

theorem sim_eval2:

`  q >> p ==> p <sim> q `

theorem not_converges_sim:

`  [| cloexp p; cloexp q; ¬ converges p |] ==> p <sim> q `

theorem divrg_sim:

`  [| cloexp q; divrg p |] ==> p <sim> q `

theorem sim_converges:

`  [| s <sim> t ; converges s |] ==> converges t`

Bisimulation

theorem bisim_refl:

`  cloexp s ==> s =~= s `

theorem bisim_sym:

`  s =~= t  ==> t =~= s `

theorem bisim_trans:

`  [| s =~= t ; t =~= u  |] ==> s =~= u `