Theory OpenSim

Up to index of Isabelle/HOL/sHowe

(*
      File: OpenSim.thy
    Author: Simon Ambler & AM
 Copyright: Leicester University, 1998--2002
Time-stamp: <2002-04-11 17:38:10 am133>

        Extension of simulation to open terms.
*)

OpenSim = Sim +

consts

  opensim    :: "( var list * uexp * uexp ) set"

syntax

  "@opensim" :: "[var list, uexp,  uexp] => bool"
                ("((_) |- /(_) /<opensim> (_) )" [50,50] 50)

translations

  "env |- s <opensim> t " == "(env,s,t) : opensim"

constdefs


  extends :: "['a list, 'a list] => bool"
  "extends l k == (! x. x mem k --> x mem l)"

(*
rules 
 osim_weak "env |- s <opensim> t ==> !n. (n # env) |- s <opensim> t"*)

inductive opensim
intrs

  opensim_Nil  "[| cloexp s; cloexp t ; s <sim> t|]  ==> [] |- s <opensim> t "
(*
  opensim_Cons 
"[|! p.  cloexp p --> (env |- (E  p) <opensim> (F  p)) ; abstr E; abstr F; newFor n (E p); newFor n (F p)|] \
        \ ==>  n # env |- (E (VAR n)) <opensim> (F(VAR n))"
*)
  opensim_Cons 
"[|isexp s;isexp t;! p.  cloexp p --> env |- subst s n p <opensim> subst t n p|] \
        \ ==>  n # env |- s <opensim> t"

end

theorem opensim_wff1:

  env |- s <opensim> t  ==> env |- s

theorem opensim_wff2:

  env |- s <opensim> t  ==> env |- t

theorem opensim_wff:

  env |- s <opensim> t  ==> env |- s & env |- t

theorem opensim_iwff:

  env |- s <opensim> t  ==> env |-- s & env |-- t

theorem opensim_sim:

  [] |- s <opensim> t  ==> s <sim> t 

theorem sim_opensim:

  s <sim> t  ==> env |- s <opensim> t 

theorem opensim_refl:

  env |- s ==> env |- s <opensim> s 

theorem opensim_refl_i:

  env |-- s ==> env |- s <opensim> s 

theorem opensim_trans:

  [| env |- s <opensim> t ; env |- t <opensim> u  |] ==> env |- s <opensim> u