Theory Sim

Up to index of Isabelle/HOL/sHowe

(*
      File: Sim.thy
    Author: Simon Ambler (sja4@mcs.le.ac.uk), modified by AM
 Copyright: Leicester University, 1998.


        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