Theory OpenHowe

Up to index of Isabelle/HOL/sHowe

(*
      File: OpenHowe.thy
    Author: AM
 Copyright: Leicester University, 2001
Time-stamp: <2002-04-16 18:29:37 am133>

        Howe relation.
*)

OpenHowe = OpenSim + 


consts

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

syntax

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



translations

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


rules

open_ss "n# env |- s <opensim> t ==> !p. (env |-- p) --> (env |- subst s n p <opensim> subst t n p)"

howe_subst "[| !a. a # env |-  N (VAR a) <howe> N' (VAR a); abstr N; abstr N'; env |- m <howe> m'|] ==> env |- (N m) <howe> (N' m')"


howe_sub " [| env |- s <howe> t;  (env = n # env1); env1 |- a <howe> b|]  ==> env1 |-  subst s n a <howe> subst t n b"



inductive howe
intrs


hVAR    "[| env |- VAR x <opensim> M |] ==> env |- VAR x <howe> M" 

hbLam   "[| !y. y#env |- N (VAR y) <howe> N' (VAR y); abstr N; abstr N'; \
                \ env |- bLam N' <opensim> Q |] \
        \ ==> env |- bLam N <howe> Q "

hApp    "[| env |- M1 <howe> M1'; env |-  M2 <howe> M2'; \
                \ env |-  (M1' $ M2') <opensim> N |] \
        \ ==> env |- (M1 $ M2) <howe> N"

end

theorem opensim_refl_i:

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

theorem howe_iwff:

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

theorem howe_wff:

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

theorem howe_Nil_cloexp:

  [] |- s <howe> t  ==> cloexp s & cloexp t

theorem howe_refl:

  env |-- s ==> env |- s <howe> s 

theorem howe_trans:

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

theorem opensim_howe:

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

theorem howe_cong_App:

  [| env |- M <howe> M' ; env |- N <howe> N'  |] ==> env |- M $ N <howe> M' $ N' 

theorem howe_cong_bLam:

  [| abstr M; abstr N; ALL x. x # env |- M (VAR x) <howe> N (VAR x)  |]
  ==> env |- bLam M <howe> bLam N 

theorem open_ss_mp:

  [| n # env |- s <opensim> t ; env |-- p |]
  ==> env |- subst s n p <opensim> subst t n p 

theorem howe_lift:

  [| ALL n. n # env |- N (VAR n) <howe> N' (VAR n) ; abstr N; abstr N';
     env |-- q |]
  ==> env |- N q <howe> N' q 

theorem howeApp_E:

  [| env |- p1 $ p2 <howe> N ;
     !!M1 M1' M2 M2'.
        [| env |- M1 <howe> M1' ; env |- M2 <howe> M2' ;
           env |- M1' $ M2' <opensim> N ; p1 = M1 & p2 = M2 |]
        ==> P |]
  ==> P

theorem howebLam_E:

  [| env |- bLam E <howe> N ;
     !!Na N'.
        [| ALL y. y # env |- Na (VAR y) <howe> N' (VAR y) ; abstr Na; abstr N';
           env |- bLam N' <opensim> N ; lambda E = lambda Na |]
        ==> P |]
  ==> P

theorem cand_eval_bLam:

  [| abstr M; [] |- bLam M <howe> P  |]
  ==> EX N. P >> bLam N & abstr N & (ALL Q. cloexp Q --> [] |- M Q <howe> N Q )

theorem down_howe_closure:

  [| P >> v; [] |- P <howe> Q  |] ==> [] |- v <howe> Q 

theorem howe_sim:

  [] |- M <howe> N  ==> M <sim> N 

theorem howe_opensim:

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

theorem howe_is_sim:

  (env |- M <opensim> N ) = (env |- M <howe> N )

theorem sim_cong_App:

  [| M <sim> M' ; N <sim> N'  |] ==> M $ N <sim> M' $ N' 

theorem opensim_cong_App:

  [| env |- M <opensim> M' ; env |- N <opensim> N'  |]
  ==> env |- M $ N <opensim> M' $ N' 

theorem opensim_cong_bLam:

  [| abstr M; abstr N; ALL x. x # env |- M (VAR x) <opensim> N (VAR x)  |]
  ==> env |- bLam M <opensim> bLam N