Theory Kleene

Up to index of Isabelle/HOL/sHowe

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


        Kleene equivalence of terms.
*)

Kleene = Divrg +

constdefs


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

  "kleene p q == cloexp p & cloexp q & (! v. (p >> v) = (q >> v))"
(*
constdefs

  expAbstr ::  "[uexp => uexp] => bool"

  "expAbstr e == abstr e & (!t. isexp t --> isexp (e t))"
*)
end

theorem kleene_cloexp1:

  s <kleene> t  ==> cloexp s

theorem kleene_cloexp2:

  s <kleene> t  ==> cloexp t

theorem kleene_cloexp:

  s <kleene> t  ==> cloexp s & cloexp t

theorem kleene_refl:

  cloexp s ==> s <kleene> s 

theorem kleene_sym:

  s <kleene> t  ==> t <kleene> s 

theorem kleene_trans:

  [| s <kleene> t ; t <kleene> u  |] ==> s <kleene> u 

theorem kleene_beta:

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

theorem eval_same_kleene:

  [| s >> v; t >> v |] ==> s <kleene> t 

theorem eval_kleene:

  s >> v ==> s <kleene> v 

theorem kleene_eval2:

  EX v. p >> v & q >> v ==> p <kleene> q 

theorem kleene_App:

  [| s <kleene> t ; cloexp u |] ==> s $ u <kleene> t $ u