Theory Kripke

(*  Title:      statecharts/CTL/Kripke.thy

    Author:     Steffen Helke, Software Engineering Group
    Copyright   2010 Technische Universitaet Berlin
*)


section ‹Kripke Structures and CTL›
theory Kripke
imports Main
begin

definition
  Kripke :: "['s set,
              's set,
              ('s * 's) set,
              ('s  'a set)]
             => bool" where

  "Kripke S S0 R L =
                (S0  S  
                 R <= S × S  
                 (Domain R) = S  
                 (dom L) = S)"

lemma Kripke_EmptySet:
 "({@x. True}, {@x. True},{(@x. True, @x. True)}, Map.empty(@x. True  {@x. True}))  
   {(S,S0,R,L) | S S0 R L. Kripke S S0 R L}"
by (unfold Kripke_def Domain_unfold, auto)

definition
  "kripke =
    {(S,S0,T,L) |
        (S::('s set))
        (S0::('s set))
        (T::(('s * 's) set))
        (L::('s  ('a  set))).
                      Kripke S S0 T L}"

typedef ('s,'a) kripke =
    "kripke :: ('s set * 's set * ('s * 's) set * ('s  'a set)) set"
  unfolding kripke_def
  apply (rule exI)
  apply (rule Kripke_EmptySet)
  done

definition
  Statuses :: "('s,'a) kripke => 's set" where
  "Statuses = fst o Rep_kripke"

definition
   InitStatuses :: "('s,'a) kripke  => 's set" where
  "InitStatuses == fst o snd o Rep_kripke"

definition
   StepRel :: "('s,'a) kripke => ('s * 's) set" where
  "StepRel == fst o snd o snd o Rep_kripke"

definition
   LabelFun :: "('s,'a) kripke => ('s  'a set)" where
  "LabelFun == snd o snd o snd o Rep_kripke"

definition
   Paths :: "[('s,'a) kripke, 's] =>
             (nat => 's) set" where
  "Paths M S == { p . S = p (0::nat)  (i. (p i, p (i+1))  (StepRel M))}"

datatype ('s,'a) ctl =  Atom "'a"
                          | AND "('s,'a) ctl" "('s,'a) ctl"
                          | OR  "('s,'a) ctl" "('s,'a) ctl"
                          | IMPLIES "('s,'a) ctl" "('s,'a) ctl"
                          | CAX "('s,'a) ctl"
                          | AF  "('s,'a) ctl"
                          | AG  "('s,'a) ctl"
                          | AU  "('s,'a) ctl" "('s,'a) ctl"
                          | AR  "('s,'a) ctl" "('s,'a) ctl"


primrec
   eval_ctl :: "[('s,'a) kripke, 's, ('s,'a) ctl] => bool"  ("_,_ |=c= _" [92,91,90]90) 
   where
     "(M,S |=c= (Atom P))        = (P  the ((LabelFun M) S))"
   | "(M,S |=c= (AND F1 F2))     = ((M,S |=c= F1)  (M,S |=c= F2))"
   | "(M,S |=c= (OR F1 F2))      = ((M,S |=c= F1)  (M,S |=c= F2))"
   | "(M,S |=c= (IMPLIES F1 F2)) = ((M,S |=c= F1)  (M,S |=c= F2))"
   | "(M,S |=c= (CAX F))         = ( T. (S,T)  (StepRel M)  (M,T |=c= F))"
   | "(M,S |=c= (AF F))          = ( P  Paths M S.  i. (M,(P i) |=c= F))"
   | "(M,S |=c= (AG F))          = ( P  Paths M S.  i. (M,(P i) |=c= F))"
   | "(M,S |=c= (AU F G))        = ( P  Paths M S.
                                      i. (M,(P i) |=c= G)  
                                       ( j. j < i  (M,(P j) |=c= F)))"
   | "(M,S |=c= (AR F G))        = ( P  Paths M S.
                                      i. (M,(P i) |=c= G)  
                                       ( j. j < i  (M,(P j) |=c= F)))"

end