(*****************************************************************************)
(* Create "Sugar2SemanticsTheory" containing abstract syntax and semantics   *)
(* of the basic language, initially following the Accellera documentation,   *)
(* but now incorporating changes  resulting from proof experiments,          *)
(* see: http://www.cl.cam.ac.uk/~mjcg/Sugar/                                 *)
(*****************************************************************************)

(******************************************************************************
* In the Sugar 2 documentation: 
*
*    http://www.haifa.il.ibm.com/projects/verification/sugar/literature.html
* 
* a model is a quintuple (S,S0,R,P,L) where
* 
*  - S  : 'state                    is a set of states
*  - S0 : 'state -> bool            is a subset of S, the initial states
*  - R  : 'state # 'state -> bool   is a transition relation 
*  - P  : 'prop                     is a set of atomic proposition
*  - L  : 'state -> ('prop -> bool) maps each state to the 
*                                   set of propositions true in that state
* 
* N.B. terms that follow are not contrained to use type variables
*      'state and 'prop, but may use 'a, 'b etc 
*      or whatever typechecking assigns.
******************************************************************************)

(*****************************************************************************)
(* START BOILERPLATE                                                         *)
(*****************************************************************************)

(******************************************************************************
* Load theory of paths and additional definitions of functions on lists 
* (commented out for compilation)
******************************************************************************)
(*
load "PathTheory"; load "rich_listTheory"; load "intLib";
*)

(******************************************************************************
* Boilerplate needed for compilation
******************************************************************************)
open HolKernel Parse boolLib bossLib;

(******************************************************************************
* Open theories of paths and lists
******************************************************************************)
open PathTheory listTheory rich_listTheory;

(******************************************************************************
* Set default parsing to natural numbers rather than integers 
******************************************************************************)
val _ = intLib.deprecate_int();

(*****************************************************************************)
(* END BOILERPLATE                                                           *)
(*****************************************************************************)

(******************************************************************************
* Start a new theory called Sugar2Semantics
******************************************************************************)
val _ = new_theory "Sugar2Semantics";

(******************************************************************************
* Stop ``S`` parsing to the S-combinator
******************************************************************************)
val _ = hide "S";

(******************************************************************************
* KRIPKE_STRUCTURE M iff M is a well-formed Kripke structure
* i.e. every initial state is a state, 
* and L maps each state to a set of propositions.
* For many results the structure M=(S,S0,R,P,L) does not need
* to be a well-formed Kripke structure.
******************************************************************************)
val KRIPKE_STRUCTURE_def =
 Define
  `KRIPKE_STRUCTURE
    (S: 'state -> bool,
     S0:'state -> bool,
     R: 'state # 'state -> bool,
     P: 'prop -> bool,
     L: 'state -> ('prop -> bool)) = 
   (!s. S0 s ==> S s)
   /\
   (!s p . L s p ==> P p)`;

(******************************************************************************
* A useful special case (possibly the only one we'll need) is to
* identify propositions with predicates on states, and then we just need
* to specify the set of itial state B and transition relation R
*******************************************************************************)
val SIMPLE_KRIPKE_STRUCTURE_def =
 Define
  `SIMPLE_KRIPKE_STRUCTURE (B:'state -> bool) (R:'state#'state->bool) = 
    ((\s:'state. T), 
     B, 
     R, 
     (\f:'state -> bool. T), 
     (\(s:'state) (f:'state -> bool). f s))`;

(******************************************************************************
* Sanity check that a simple Kripke structure is a Kripke structure
******************************************************************************)
val SIMPLE_KRIPKE_STRUCTURE =
 store_thm
  ("SIMPLE_KRIPKE_STRUCTURE",
   ``KRIPKE_STRUCTURE(SIMPLE_KRIPKE_STRUCTURE B R)``,
   RW_TAC std_ss [KRIPKE_STRUCTURE_def,SIMPLE_KRIPKE_STRUCTURE_def]);
   
(******************************************************************************
* Boolean expressions (added B_TRUE for use in definition of F_SEM)
******************************************************************************)
val bexp_def =
 Hol_datatype
  `bexp = B_PROP   of 'a                         (* atomic proposition       *)
        | B_NOT    of bexp                       (* negation                 *)
        | B_AND    of bexp # bexp`;              (* conjunction              *)

(******************************************************************************
* Definition of truth
******************************************************************************)

val B_OR_def =
 Define `B_OR(b1,b2) = B_NOT(B_AND(B_NOT b1, B_NOT b2))`;

(******************************************************************************
* Definition of truth
******************************************************************************)

val B_TRUE_def =
 Define `B_TRUE = B_OR(B_PROP ARB, B_NOT(B_PROP ARB))`;

(******************************************************************************
* Definition of falsity
******************************************************************************)

val B_FALSE_def =
 Define `B_FALSE = B_NOT B_TRUE`;

(******************************************************************************
* Sugar Extended Regular Expressions (SEREs) 
******************************************************************************)
val sere_def =
 Hol_datatype
  `sere = S_BOOL        of 'a bexp               (* boolean expression       *)
        | S_CAT         of sere # sere           (* r1 ;  r2                 *)
        | S_FUSION      of sere # sere           (* r1 :  r2                 *)
        | S_OR          of sere # sere           (* r1 |  r2                 *)
        | S_RIG_AND     of sere # sere           (* r1 && r2                 *)
        | S_FLEX_AND    of sere # sere           (* r1 & r2                  *)
        | S_REPEAT      of sere                  (* r[*]                     *)
        | S_CLOCK       of sere # 'a bexp`;      (* r@clk                    *)

(******************************************************************************
* Formulas of Sugar Foundation Language (FL)
******************************************************************************)
val fl_def =
 Hol_datatype
  `fl = F_BOOL         of 'a bexp                (* boolean expression       *)
      | F_NOT          of fl                     (* \neg f                   *)
      | F_AND          of fl # fl                (* f1 \wedge f2             *)
      | F_NEXT         of fl                     (* X! f                     *)
      | F_UNTIL        of fl # fl                (* [f1 U f2]                *)
      | F_SUFFIX_IMP   of 'a sere # fl           (* {r}(f)                   *)
      | F_STRONG_IMP   of 'a sere # 'a sere      (* r1 |-> r2!               *)
      | F_WEAK_IMP     of 'a sere # 'a sere      (* r1 |-> r2                *)
      | F_ABORT        of fl # 'a bexp           (* f abort b                *)
      | F_WEAK_CLOCK   of fl # 'a bexp           (* r@clk                    *)
      | F_STRONG_CLOCK of fl # 'a bexp`;         (* r@clk!                   *)

(******************************************************************************
* Formulas of Sugar Optional Branching Extension (OBE)
******************************************************************************)
val obe_def =
 Hol_datatype
  `obe = O_BOOL        of 'a bexp                (* boolean expression       *)
       | O_NOT         of obe                    (* \neg f                   *)
       | O_AND         of obe # obe              (* f1 \wedge f2             *)
       | O_EX          of obe                    (* EX f                     *)
       | O_EU          of obe # obe              (* E[f1 U f2]               *)
       | O_EG          of obe`;                  (* EG f                     *)

(******************************************************************************
* Selectors for components of a model M = (S,S0,R,P,L)
******************************************************************************)

val getS_def  = Define `getS  (S,S0,R,P,L) = S`;
val getS0_def = Define `getS0 (S,S0,R,P,L) = S0`;
val getR_def  = Define `getR  (S,S0,R,P,L) = R`;
val getP_def  = Define `getP  (S,S0,R,P,L) = P`;
val getL_def  = Define `getL  (S,S0,R,P,L) = L`;

(******************************************************************************
* L and \hat{L} operators used in the semantics
******************************************************************************)
val L_def    = Define `L M = getL M`;
val LHAT_def = Define `LHAT M = MAP (getL M)`;

(******************************************************************************
* B_SEM M l b means "l |= b" 
* and also that b only contains atomic propositions in getP M
******************************************************************************)
val B_SEM_def =
 Define
  `(B_SEM M l (B_PROP(p:'p)) = p IN (getP M) /\ p IN l)
   /\
   (B_SEM M l (B_NOT b)      = ~(B_SEM M l b))
   /\
   (B_SEM M l (B_AND(b1,b2)) = B_SEM M l b1 /\ B_SEM M l b2)`;

val B_SEM =
 store_thm
  ("B_SEM",
   ``(B_SEM M l (B_PROP(p:'p)) = p IN (getP M) /\ p IN l)
     /\
     (B_SEM M l B_TRUE         = T)
     /\
     (B_SEM M l B_FALSE        = F)
     /\
     (B_SEM M l (B_NOT b)      = ~(B_SEM M l b))
     /\
     (B_SEM M l (B_AND(b1,b2)) = B_SEM M l b1 /\ B_SEM M l b2)
     /\
     (B_SEM M l (B_OR(b1,b2)) = B_SEM M l b1 \/ B_SEM M l b2)``,
   RW_TAC std_ss [B_SEM_def,B_OR_def,B_TRUE_def,B_FALSE_def]
    THEN PROVE_TAC[]);

(******************************************************************************
* Unclocked semantics of SEREs
* US_SEM M w r means "w is in the language of r" in the unclocked semantics
******************************************************************************)
val US_SEM_def =
 Define
  `(US_SEM M w (S_BOOL b) = ?l. (w = [l]) /\ B_SEM M l b)
   /\
   (US_SEM M w (S_CAT(r1,r2)) = 
     ?w1 w2. (w = w1 <> w2) /\ US_SEM M w1 r1 /\ US_SEM M w2 r2)
   /\
   (US_SEM M w (S_FUSION(r1,r2)) = 
     ?w1 w2 l. (w = w1 <> [l] <> w2) /\ 
               US_SEM M (w1<>[l]) r1 /\ US_SEM M ([l]<>w2) r2) 
   /\
   (US_SEM M w (S_OR(r1,r2)) = 
     US_SEM M w r1 \/ US_SEM M w r2) 
   /\
   (US_SEM M w (S_RIG_AND(r1,r2)) = 
     US_SEM M w r1 /\ US_SEM M w r2) 
   /\
   (US_SEM M w (S_FLEX_AND(r1,r2)) = 
     ?w1 w2. (w = w1 <> w2) /\ 
             ((US_SEM M w r1 /\ US_SEM M w1 r2) 
              \/
              (US_SEM M w r2 /\ US_SEM M w1 r1) ))
   /\
   (US_SEM M w (S_REPEAT r) = 
     ?wlist. (w = CONCAT wlist) /\ EVERY (\w. US_SEM M w r) wlist)`;

(******************************************************************************
* Clocked semantics of SEREs
* S_SEM M w c r means "w is in the language of r in context c"
******************************************************************************)
val S_SEM_def =
 Define
  `(S_SEM M w c (S_BOOL b) = 
     ?n. n >= 1                                               /\ 
         (LENGTH w = n)                                       /\ 
         (!i. 1 <= i /\ i < n ==> B_SEM M (EL (i-1) w) (B_NOT c)) /\
         B_SEM M (EL (n-1) w) (B_AND(c,b)))
   /\
   (S_SEM M w c (S_CAT(r1,r2)) = 
     ?w1 w2. (w = w1 <> w2) /\ S_SEM M w1 c r1 /\ S_SEM M w2 c r2)
   /\
   (S_SEM M w c (S_FUSION(r1,r2)) = 
     ?w1 w2 l. (w = w1 <> [l] <> w2) /\ 
               S_SEM M (w1<>[l]) c r1 /\ S_SEM M ([l]<>w2) c r2) 
   /\
   (S_SEM M w c (S_OR(r1,r2)) = 
     S_SEM M w c r1 \/ S_SEM M w c r2) 
   /\
   (S_SEM M w c (S_RIG_AND(r1,r2)) = 
     S_SEM M w c r1 /\ S_SEM M w c r2) 
   /\
   (S_SEM M w c (S_FLEX_AND(r1,r2)) = 
     ?w1 w2. (w = w1 <> w2) /\ 
             ((S_SEM M w c r1 /\ S_SEM M w1 c r2) 
              \/
              (S_SEM M w c r2 /\ S_SEM M w1 c r1) ))
   /\
   (S_SEM M w c (S_REPEAT r) = 
     ?wlist. (w = CONCAT wlist) /\ EVERY (\w. S_SEM M w c r) wlist)
   /\
   (S_SEM M w c (S_CLOCK(r,c1)) =
     S_SEM M w c1 r)`;

(******************************************************************************
* Unclocked semantics of Sugar formulas
* UF_SEM M p f means "p |= f"  in the unclocked semantics
* (F_WEAK_IMP case unfolded to make totality proof go through)
******************************************************************************)
val UF_SEM_def =
 Define
   `(UF_SEM M p (F_BOOL b) = 
      B_SEM M (L M (PATH_EL p 0)) b)
    /\
    (UF_SEM M p (F_NOT f) = 
      ~(UF_SEM M p f)) 
    /\
    (UF_SEM M p (F_AND(f1,f2)) = 
      UF_SEM M p f1 /\ UF_SEM M p f2)
    /\
    (UF_SEM M p (F_NEXT f) = 
      PL p 1 /\ UF_SEM M (RESTN p 1) f)
    /\
    (UF_SEM M p (F_UNTIL(f1,f2)) = 
      ?k :: PL p. UF_SEM M (RESTN p k) f2 /\
                  !j :: PL p. j < k ==> UF_SEM M (RESTN p j) f1)
    /\
    (UF_SEM M p (F_SUFFIX_IMP(r,f)) = 
      !j :: PL p. US_SEM M (LHAT M (PATH_SEG p (0,j))) r
                  ==>
                  UF_SEM M (RESTN p j) f)
    /\
    (UF_SEM M p (F_STRONG_IMP(r1,r2)) = 
      !j :: PL p. US_SEM M (LHAT M (PATH_SEG p (0,j))) r1
                  ==>
                  ?k :: PL p. j <= k /\ US_SEM M (LHAT M (PATH_SEG p (j,k))) r2)
    /\
    (UF_SEM M p (F_WEAK_IMP(r1,r2)) = 
      !j :: PL p. US_SEM M (LHAT M (PATH_SEG p (0,j))) r1 ==>
                  (?k :: PL p. j <= k /\ US_SEM M (LHAT M (PATH_SEG p (j,k))) r2) 
                  \/
                  !k :: PL p. 
                   j <= k ==> ?w. US_SEM M (LHAT M (PATH_SEG p (j,k)) <> w) r2)  
    /\
    (UF_SEM M p (F_ABORT (f,b)) =
      UF_SEM M p f 
      \/
      ?j :: PL p. 0 < j
        /\
        ?p'. (* IS_INFINITE_PATH p'          /\ *)
             UF_SEM M (RESTN p j) (F_BOOL b) /\ 
             UF_SEM M (PATH_CAT(PATH_SEG p (0,j-1),p')) f)`;

(******************************************************************************
* UF_SEM M p f means "p |= f"  in the unclocked semantics
* Derivation of folded equation
******************************************************************************)
val UF_SEM =
 store_thm
  ("UF_SEM",
   ``(UF_SEM M p (F_BOOL b) = 
       B_SEM M (L M (PATH_EL p 0)) b)
     /\
     (UF_SEM M p (F_NOT f) = 
       ~(UF_SEM M p f)) 
     /\
     (UF_SEM M p (F_AND(f1,f2)) = 
       UF_SEM M p f1 /\ UF_SEM M p f2)
     /\
     (UF_SEM M p (F_NEXT f) = 
       PL p 1 /\ UF_SEM M (RESTN p 1) f)
     /\
     (UF_SEM M p (F_UNTIL(f1,f2)) = 
       ?k :: PL p. UF_SEM M (RESTN p k) f2 /\
                   !j :: PL p. j < k ==> UF_SEM M (RESTN p j) f1)
     /\
     (UF_SEM M p (F_SUFFIX_IMP(r,f)) = 
       !j :: PL p. US_SEM M (LHAT M (PATH_SEG p (0,j))) r
                   ==>
                   UF_SEM M (RESTN p j) f)
     /\
     (UF_SEM M p (F_STRONG_IMP(r1,r2)) = 
       !j :: PL p. US_SEM M (LHAT M (PATH_SEG p (0,j))) r1
                   ==>
                   ?k :: PL p. j <= k /\ US_SEM M (LHAT M (PATH_SEG p (j,k))) r2)
     /\
    (UF_SEM M p (F_WEAK_IMP(r1,r2)) = 
       !j :: PL p. US_SEM M (LHAT M (PATH_SEG p (0,j))) r1 ==>
                   (?k :: PL p. j <= k /\ US_SEM M (LHAT M (PATH_SEG p (j,k))) r2) 
                   \/  
                    !k :: PL p. 
                      j <= k ==> ?w. US_SEM M (LHAT M (PATH_SEG p (j,k)) <> w) r2)  
     /\
     (UF_SEM M p (F_ABORT (f,b)) =
       UF_SEM M p f 
       \/
       ?j :: PL p. 0 < j 
        /\
        ?p'. (* IS_INFINITE_PATH p'          /\ *)
             UF_SEM M (RESTN p j) (F_BOOL b) /\ 
             UF_SEM M (PATH_CAT(PATH_SEG p (0,j-1),p')) f)``,
   SIMP_TAC std_ss [UF_SEM_def]);

(******************************************************************************
* FIRST_RISE M p c i  =  LHAT(p(0,i))  |=T=  {(\neg c)[*];c}
* (i is the first rising edge of clock c in path p)
******************************************************************************)
val FIRST_RISE_def =
 Define
  `FIRST_RISE M p c i =
    S_SEM
     M
     (MAP (getL M) (PATH_SEG p (0,i)))
     B_TRUE
     (S_CAT(S_REPEAT(S_BOOL(B_NOT c)),S_BOOL c))`;

(******************************************************************************
* NEXT_RISE M p c (i,j)  =   Lhat(p(i,j))  |=T=  {(\neg c)[*];c}
* (i is the first rising edge after j of clock c in path p)
******************************************************************************)
val NEXT_RISE_def =
 Define
  `NEXT_RISE M p c (i,j) =
    S_SEM
     M
     (MAP (getL M) (PATH_SEG p (i,j)))
     B_TRUE
     (S_CAT(S_REPEAT(S_BOOL(B_NOT c)),S_BOOL c))`;

(******************************************************************************
* Contexts (strong or weak clock)
******************************************************************************)
val context_def =
 Hol_datatype
  `context = STRONG_CLOCK  of 'a bexp       (* strong clock: c!              *)
           | WEAK_CLOCK    of 'a bexp`;     (* weak clock:  c                *)

(******************************************************************************
* Clocked semantics of Sugar formulas
* Definition due to Konrad Slind that uses
* cunning feature of TFL to prove that F_SEM is total
******************************************************************************)
val F_SEM_defn = 
  Hol_defn 
  "F_SEM"
  `(F_SEM M p (STRONG_CLOCK c) (F_BOOL b) = 
      ?i :: PL p. FIRST_RISE M p c i /\ B_SEM M (L M (PATH_EL p i)) b)
    /\
    (F_SEM M p (STRONG_CLOCK c) (F_NOT f) = 
      ~(F_SEM M p (WEAK_CLOCK c) f))
    /\
    (F_SEM M p (STRONG_CLOCK c) (F_AND(f1,f2)) = 
      ?i :: PL p. FIRST_RISE M p c i                      /\ 
                  F_SEM M (RESTN p i) (STRONG_CLOCK c) f1 /\
                  F_SEM M (RESTN p i) (STRONG_CLOCK c) f2)
    /\
    (F_SEM M p (STRONG_CLOCK c) (F_NEXT f) = 
      ?i :: PL p. FIRST_RISE M p c i 
                  /\ 
                  ?j :: PL p. i < j         /\ 
                    NEXT_RISE M p c (i+1,j) /\
                    F_SEM M (RESTN p j) (STRONG_CLOCK c) f)
    /\
    (F_SEM M p (STRONG_CLOCK c) (F_UNTIL(f1,f2)) = 
      ?i k :: PL p. k >= i                                               /\
                    FIRST_RISE M p c i                                   /\
                    F_SEM M (RESTN p k) (WEAK_CLOCK B_TRUE) (F_BOOL c)   /\  
                    F_SEM M (RESTN p k) (STRONG_CLOCK c) f2              /\
                    !j :: PL p. i <= j /\ j < k /\ 
                          F_SEM M (RESTN p j) (WEAK_CLOCK B_TRUE) (F_BOOL c) 
                          ==>
                          F_SEM M (RESTN p j) (STRONG_CLOCK c) f1)
    /\
(*
    (F_SEM M p (STRONG_CLOCK c) (F_UNTIL(f1,f2)) = 
      ?i :: PL p. (?k :: PL p. i <= k                /\ 
                               NEXT_RISE M p c (i,k) /\ 
                               F_SEM M (RESTN p k) (STRONG_CLOCK c) f2)
                  /\
                  !j :: PL p. j < i ==>
                              ?k :: PL p. j <= k                /\ 
                                          NEXT_RISE M p c (j,k) /\ 
                                          F_SEM M (RESTN p k) (STRONG_CLOCK c) f1)
*)
    (F_SEM M p (STRONG_CLOCK c) (F_SUFFIX_IMP(r,f)) = 
      ?i :: PL p. FIRST_RISE M p c i /\ 
                  !j :: PL p. i <= j /\ S_SEM M (LHAT M (PATH_SEG p (i,j))) c r
                        ==>
                        F_SEM M (RESTN p j) (STRONG_CLOCK c) f)
    /\
    (F_SEM M p (STRONG_CLOCK c) (F_STRONG_IMP(r1,r2)) = 
      ?i :: PL p. FIRST_RISE M p c i /\ 
                  !j :: PL p. i <= j /\ S_SEM M (LHAT M (PATH_SEG p (i,j))) c r1
                              ==>
                              ?k :: PL p. j <= k /\ S_SEM M (LHAT M (PATH_SEG p (j,k))) c r2)
    /\
    (F_SEM M p (STRONG_CLOCK c) (F_WEAK_IMP(r1,r2)) = 
     F_SEM M p (STRONG_CLOCK c) (F_STRONG_IMP(r1,r2))
      \/
     (F_SEM M p (WEAK_CLOCK c) (F_WEAK_IMP(r1,r2))
      /\
      !j :: PL p. ?k :: PL p. j <= k /\ NEXT_RISE M p c (j,k)))
    /\
    (F_SEM M p (STRONG_CLOCK c) (F_ABORT (f,b)) =
      ?i :: PL p. FIRST_RISE M p c i /\
                  (F_SEM M (RESTN p i) (STRONG_CLOCK c) f 
                   \/
                   ?j :: PL p. i < j 
                    /\ ?p'. (* IS_INFINITE_PATH p'                                       /\ *)
                            F_SEM M (RESTN p j) (WEAK_CLOCK B_TRUE) (F_BOOL(B_AND(c,b))) /\ 
                            F_SEM M (PATH_CAT(PATH_SEG p (i,j-1),p')) (STRONG_CLOCK c) f))
    /\
    (F_SEM M p (STRONG_CLOCK c) (F_WEAK_CLOCK(f,c1)) =   
      F_SEM M p (WEAK_CLOCK c1) f)
    /\
    (F_SEM M p (STRONG_CLOCK c) (F_STRONG_CLOCK(f,c1)) =   
      F_SEM M p (STRONG_CLOCK c1) f)
    /\ 
(******************************************************************************
* Start of weak clock clauses
******************************************************************************)
   (F_SEM M p (WEAK_CLOCK c) (F_BOOL b) =
     !i :: PL p. FIRST_RISE M p c i ==> B_SEM M (L M (PATH_EL p i)) b)
    /\
    (F_SEM M p (WEAK_CLOCK c) (F_NOT f) = 
      ~(F_SEM M p (STRONG_CLOCK c) f)) 
    /\
    (F_SEM M p (WEAK_CLOCK c) (F_AND(f1,f2)) = 
      !i :: PL p. FIRST_RISE M p c i
                  ==>
                 (F_SEM M (RESTN p i) (WEAK_CLOCK c) f1 /\
                  F_SEM M (RESTN p i) (WEAK_CLOCK c) f2))
    /\
    (F_SEM M p (WEAK_CLOCK c) (F_NEXT f) = 
      !i :: PL p. FIRST_RISE M p c i 
                  ==>
                  ?j :: PL p. i < j         /\
                    NEXT_RISE M p c (i+1,j) /\
                    F_SEM M (RESTN p j) (WEAK_CLOCK c) f)
    /\
    (F_SEM M p (WEAK_CLOCK c) (F_UNTIL(f1,f2)) = 
     (?i :: PL p. FIRST_RISE M p c i /\
          ?l :: PL p.
            i <= l /\
            ((?k :: PL p. l <= k /\ NEXT_RISE M p c (l,k) /\ F_SEM M (RESTN p k) (WEAK_CLOCK c) f2) \/
             !m :: PL p. l <= m ==> F_SEM M (RESTN p m) (WEAK_CLOCK B_TRUE) (F_BOOL (B_NOT c))) /\
            !j :: PL p.
              i <= j /\ j < l ==>
              (?k :: PL p. j <= k /\ NEXT_RISE M p c (j,k) /\ F_SEM M (RESTN p k) (WEAK_CLOCK c) f1) \/
              !m :: PL p. j <= m ==> F_SEM M (RESTN p m) (WEAK_CLOCK B_TRUE) (F_BOOL (B_NOT c))) \/
       !i :: PL p. F_SEM M (RESTN p i) (WEAK_CLOCK B_TRUE) (F_BOOL (B_NOT c)))
    /\
(*
    (F_SEM M p (WEAK_CLOCK c) (F_UNTIL(f1,f2)) = 
      F_SEM M p (STRONG_CLOCK c) (F_UNTIL(f1,f2))  
      \/
      (?k :: PL p. !l :: PL p. 
        l >= k  (* changed from l > k *)
        ==>
        F_SEM M (RESTN p l) (WEAK_CLOCK B_TRUE) (F_BOOL(B_NOT c)) /\ 
        !j :: PL p. j <= k 
                    ==>
                    F_SEM M (RESTN p j) (WEAK_CLOCK B_TRUE) (F_BOOL c)
                    ==>
                    F_SEM M (RESTN p j) (WEAK_CLOCK c) f1))
    /\
    (F_SEM M p (WEAK_CLOCK c) (F_UNTIL(f1,f2)) = 
      ?i :: PL p. ((?k :: PL p. i <= k                /\ 
                                NEXT_RISE M p c (i,k) /\ 
                                F_SEM M (RESTN p k) (WEAK_CLOCK c) f2)
                   \/
                   !k :: PL p. i <= k
                               ==>
                               F_SEM M (RESTN p k) (WEAK_CLOCK B_TRUE) (F_BOOL(B_NOT c)))
                  /\
                  !j :: PL p. j < i ==>
                              (?k :: PL p. j <= k                /\ 
                                           NEXT_RISE M p c (j,k) /\ 
                                           F_SEM M (RESTN p k) (WEAK_CLOCK c) f1)
                              \/
                              !k :: PL p. j <= k
                                          ==>
                                          F_SEM M (RESTN p k) (WEAK_CLOCK B_TRUE) (F_BOOL(B_NOT c)))
*)
    (F_SEM M p (WEAK_CLOCK c) (F_SUFFIX_IMP(r,f)) = 
      !i :: PL p. FIRST_RISE M p c i ==>
                  !j :: PL p. i <= j /\ S_SEM M (LHAT M (PATH_SEG p (i,j))) c r
                              ==>
                              F_SEM M (RESTN p j) (WEAK_CLOCK c) f)
    /\
    (F_SEM M p (WEAK_CLOCK c) (F_STRONG_IMP(r1,r2)) = 
      F_SEM M p (STRONG_CLOCK c) (F_STRONG_IMP(r1,r2))  
      \/
      (F_SEM M p (WEAK_CLOCK c) (F_WEAK_IMP(r1,r2)) 
       /\
       ?k :: PL p. !l :: PL p. 
        l >= k   (* changed from l > k *)
        ==> 
        F_SEM M (RESTN p l) (WEAK_CLOCK B_TRUE) (F_BOOL(B_NOT c))))
    /\
    (F_SEM M p (WEAK_CLOCK c) (F_WEAK_IMP(r1,r2)) = 
      !i :: PL p. FIRST_RISE M p c i
                  ==>
                  !j :: PL p. i <= j /\ S_SEM M (LHAT M (PATH_SEG p (i,j))) c r1
                              ==>
                              ((?k :: PL p. j <= k /\ S_SEM M (LHAT M (PATH_SEG p (j,k))) c r2)
                               \/
                               !k :: PL p. 
                                j <= k ==> ?w. S_SEM M (LHAT M (PATH_SEG p (j,k)) <> w) c r2))
    /\
    (F_SEM M p (WEAK_CLOCK c) (F_ABORT (f,b)) =
      !i :: PL p. FIRST_RISE M p c i 
                  ==>
                  (F_SEM M (RESTN p i) (WEAK_CLOCK c) f 
                   \/
                   ?j :: PL p. i < j /\ 
                     ?p'. (* IS_INFINITE_PATH p' /\ *)
                          F_SEM M (RESTN p j) (WEAK_CLOCK B_TRUE) (F_BOOL(B_AND(c,b)))
                          /\
                          F_SEM M (PATH_CAT(PATH_SEG p (i,j-1),p')) (WEAK_CLOCK c) f))
    /\
    (F_SEM M p (WEAK_CLOCK c) (F_WEAK_CLOCK(f,c1)) =   
      F_SEM M p (WEAK_CLOCK c1) f)
    /\
    (F_SEM M p (WEAK_CLOCK c) (F_STRONG_CLOCK(f,c1)) =   
      F_SEM M p (STRONG_CLOCK c1) f)`;

val new_fl_size_def = 
 Define `(new_fl_size (F_BOOL _) = 0) /\
         (new_fl_size other      = fl_size (\a.0) other)`;

val new_context_size_def = 
  Define `(new_context_size (STRONG_CLOCK _) = 0) /\
          (new_context_size (WEAK_CLOCK _) = 1)`;

val (F_SEM_def, F_SEM_ind) = Count.apply Defn.tprove
 (F_SEM_defn,
  WF_REL_TAC `inv_image ($< LEX $<) 
                (\(u,v,w,x). 
                   (if (?c d. ((w = WEAK_CLOCK c) /\ (x = F_WEAK_IMP d)) \/
                              ((w = STRONG_CLOCK c) /\ (x = F_STRONG_IMP d)))
                        then 0 else new_fl_size x, 
                      new_context_size w))`
   THEN EVAL_TAC THEN RW_TAC arith_ss [DECIDE (Term `0 < 1 + x`)]
   THEN ((Cases_on `f` THEN EVAL_TAC THEN DECIDE_TAC) ORELSE
         (Cases_on `f1` THEN EVAL_TAC THEN DECIDE_TAC) ORELSE
         (Cases_on `f2` THEN EVAL_TAC THEN DECIDE_TAC)));

val _ = save_thm("F_SEM_def",F_SEM_def);
val _ = save_thm("F_SEM_ind",F_SEM_ind);

(******************************************************************************
* PATH M p is true iff p is a path with respect to transition relation getR M
******************************************************************************)
val PATH_def = Define `PATH M p = !n. (getR M)(PATH_EL p n, PATH_EL p (n+1))`;

(******************************************************************************
* O_SEM M s f means "M, s |= f" 
******************************************************************************)
val O_SEM_def =
 Define
  `(O_SEM M s (O_BOOL b) = B_SEM M (L M s) b)
   /\
   (O_SEM M s (O_NOT f) = ~(O_SEM M s f)) 
   /\
   (O_SEM M s (O_AND(f1,f2)) = O_SEM M s f1 /\ O_SEM M s f2)
   /\
   (O_SEM M s (O_EX f) = 
     ?p. PATH M p                                 /\ 
         (IS_FINITE_PATH p ==> 1 < PATH_LENGTH p) /\ 
         (PATH_EL p 0 = s) /\ O_SEM M (PATH_EL p 1) f)
   /\
   (O_SEM M s (O_EU(f1,f2)) = 
     ?p. PATH M p          /\ 
         (PATH_EL p 0 = s) /\ 
         ?k :: PL p. O_SEM M (PATH_EL p k) f2  /\ 
                     !j. j < k ==> O_SEM M (PATH_EL p j) f1)
   /\
   (O_SEM M s (O_EG f) = 
     ?p. PATH M p /\ (PATH_EL p 0 = s) /\ !j :: PL p. O_SEM M (PATH_EL p j) f)`;

(******************************************************************************
* Rules for compiling clocked SEREs to unclocked SEREs
* (from B.1, page 66, of Sugar 2.0 Accellera document)
******************************************************************************)
val S_CLOCK_COMP_def =
 Define
  `(S_CLOCK_COMP c (S_BOOL b) = 
     (S_CAT (S_REPEAT (S_BOOL (B_NOT c)),S_BOOL(B_AND(c, b)))))
   /\
   (S_CLOCK_COMP c (S_CAT(r1,r2)) =  
     S_CAT(S_CLOCK_COMP c r1, S_CLOCK_COMP c r2))
   /\
   (S_CLOCK_COMP c (S_FUSION(r1,r2)) = 
     S_FUSION(S_CLOCK_COMP c r1, S_CLOCK_COMP c r2))
   /\
   (S_CLOCK_COMP c (S_OR(r1,r2)) = 
     S_OR(S_CLOCK_COMP c r1, S_CLOCK_COMP c r2))
   /\
   (S_CLOCK_COMP c (S_RIG_AND(r1,r2))  = 
     S_RIG_AND(S_CLOCK_COMP c r1, S_CLOCK_COMP c r2))
   /\
   (S_CLOCK_COMP c (S_FLEX_AND(r1,r2)) = 
     S_FLEX_AND(S_CLOCK_COMP c r1, S_CLOCK_COMP c r2))
   /\
   (S_CLOCK_COMP c (S_REPEAT r) = 
     S_REPEAT(S_CLOCK_COMP c r))
   /\
   (S_CLOCK_COMP c (S_CLOCK(r, c1)) = 
     S_CLOCK_COMP c1 r)`;

(******************************************************************************
* Some abbreviations needed for definition of F_CLOCK_COMP
******************************************************************************)

val F_U_CLOCK_def =
 Define
  `F_U_CLOCK c f = F_UNTIL(F_BOOL(B_NOT c),F_AND(F_BOOL c, f))`;

val F_OR_def =
 Define
  `F_OR(f1,f2) = F_NOT(F_AND(F_NOT f1, F_NOT f2))`;

val F_F_def =
 Define
  `F_F f = F_UNTIL(F_BOOL B_TRUE, f)`;
      
val F_G_def =
 Define
  `F_G f = F_NOT(F_F(F_NOT f))`;

val F_WEAK_NEXT_def =
 Define `F_WEAK_NEXT f = F_NOT(F_NEXT(F_NOT f))`;

val F_W_def =
 Define
  `F_W(f1,f2) = F_OR(F_UNTIL(f1,f2), F_G f1)`;

val F_W_CLOCK_def =
 Define
  `F_W_CLOCK c f = F_W(F_BOOL(B_NOT c),F_AND(F_BOOL c, f))`;

(******************************************************************************
* Rules for compiling clocked FL formulas to unclocked formulas
* (from B.1, page 66 and 67, of Sugar 2.0 Accellera document)
*
* Update from IBM: the correct rewrite rules for X! should be:
*  
*  (X! f)@clk! = [!clk U clk & X! (!clk U clk & (f@clk!))]
*  (X! f)@clk  = [!clk W clk & X! (!clk U clk & (f@clk!))]
*  
* Change by MJCG on 12.09.02:
*  (X! f)@clk  = [!clk W clk & X! (!clk U clk & (f@clk))]
******************************************************************************)
val F_CLOCK_COMP_def =
 Define
  `(F_CLOCK_COMP (STRONG_CLOCK c) (F_BOOL b) = 
     F_U_CLOCK c (F_BOOL b))
    /\
    (F_CLOCK_COMP (STRONG_CLOCK c) (F_NOT f) = 
      F_NOT(F_CLOCK_COMP (WEAK_CLOCK c) f))
    /\
    (F_CLOCK_COMP (STRONG_CLOCK c) (F_AND(f1,f2)) = 
      F_U_CLOCK c (F_AND(F_CLOCK_COMP (STRONG_CLOCK c) f1, 
                         F_CLOCK_COMP (STRONG_CLOCK c) f2)))
    /\
    (F_CLOCK_COMP (STRONG_CLOCK c) (F_NEXT f) = 
      F_U_CLOCK c (F_NEXT(F_U_CLOCK c (F_CLOCK_COMP (STRONG_CLOCK c) f))))
    /\
(*
    (F_CLOCK_COMP (STRONG_CLOCK c) (F_UNTIL(f1,f2)) = 
      F_UNTIL(F_U_CLOCK c (F_CLOCK_COMP (STRONG_CLOCK c) f1),
              F_U_CLOCK c (F_CLOCK_COMP (STRONG_CLOCK c) f2)))
*)
    (F_CLOCK_COMP (STRONG_CLOCK c) (F_UNTIL(f1,f2)) = 
      F_U_CLOCK c (F_UNTIL(F_U_CLOCK c (F_CLOCK_COMP (STRONG_CLOCK c) f1),
                           F_U_CLOCK c (F_CLOCK_COMP (STRONG_CLOCK c) f2))))
    /\
    (F_CLOCK_COMP (STRONG_CLOCK c) (F_SUFFIX_IMP(r,f)) = 
      F_U_CLOCK c (F_SUFFIX_IMP(S_CLOCK_COMP c r, 
                                F_CLOCK_COMP (STRONG_CLOCK c) f)))
    /\
    (F_CLOCK_COMP (STRONG_CLOCK c) (F_STRONG_IMP(r1,r2)) = 
      F_U_CLOCK c (F_STRONG_IMP (S_CLOCK_COMP c r1,
                                 S_CLOCK_COMP c r2)))
    /\
    (F_CLOCK_COMP (STRONG_CLOCK c) (F_WEAK_IMP(r1,r2)) = 
      F_U_CLOCK c (F_OR
                    (F_STRONG_IMP(S_CLOCK_COMP c r1, S_CLOCK_COMP c r2),
                     F_AND
                      (F_G(F_F(F_BOOL c)),
                       F_WEAK_IMP(S_CLOCK_COMP c r1, S_CLOCK_COMP c r2)))))
    /\
    (F_CLOCK_COMP (STRONG_CLOCK c) (F_ABORT (f,b)) =
      F_U_CLOCK c (F_ABORT(F_CLOCK_COMP (STRONG_CLOCK c) f, B_AND(c,b))))
    /\
    (F_CLOCK_COMP (STRONG_CLOCK c) (F_WEAK_CLOCK(f,c1)) =   
      F_CLOCK_COMP (WEAK_CLOCK c1) f)
    /\
    (F_CLOCK_COMP (STRONG_CLOCK c) (F_STRONG_CLOCK(f,c1)) =   
      F_CLOCK_COMP (STRONG_CLOCK c1) f)
    /\ 
(******************************************************************************
* Start of weak clock clauses
******************************************************************************)
    (F_CLOCK_COMP (WEAK_CLOCK c) (F_BOOL b) = 
      F_W_CLOCK c (F_BOOL b))
    /\
    (F_CLOCK_COMP (WEAK_CLOCK c) (F_NOT f) = 
      F_NOT(F_CLOCK_COMP (STRONG_CLOCK c) f))
    /\
    (F_CLOCK_COMP (WEAK_CLOCK c) (F_AND(f1,f2)) = 
      F_W_CLOCK c (F_AND(F_CLOCK_COMP (WEAK_CLOCK c) f1, 
                         F_CLOCK_COMP (WEAK_CLOCK c) f2)))
    /\
    (F_CLOCK_COMP (WEAK_CLOCK c) (F_NEXT f) = 
      F_W_CLOCK c (F_NEXT(F_U_CLOCK c (F_CLOCK_COMP (WEAK_CLOCK c) f))))
    /\
(*
    (F_CLOCK_COMP (WEAK_CLOCK c) (F_UNTIL(f1,f2)) = 
      F_UNTIL(F_W_CLOCK c (F_CLOCK_COMP (WEAK_CLOCK c) f1), 
              F_W_CLOCK c (F_CLOCK_COMP (WEAK_CLOCK c) f2)))
*)
    (F_CLOCK_COMP (WEAK_CLOCK c) (F_UNTIL(f1,f2)) = 
      F_W_CLOCK c (F_UNTIL(F_W_CLOCK c (F_CLOCK_COMP (WEAK_CLOCK c) f1),
                           F_W_CLOCK c (F_CLOCK_COMP (WEAK_CLOCK c) f2))))
    /\
    (F_CLOCK_COMP (WEAK_CLOCK c) (F_SUFFIX_IMP(r,f)) = 
      F_W_CLOCK c (F_SUFFIX_IMP(S_CLOCK_COMP c r, 
                                F_CLOCK_COMP (WEAK_CLOCK c) f)))
    /\
    (F_CLOCK_COMP (WEAK_CLOCK c) (F_STRONG_IMP(r1,r2)) = 
      F_W_CLOCK c (F_OR
                    (F_STRONG_IMP(S_CLOCK_COMP c r1, S_CLOCK_COMP c r2),
                     F_AND
                      (F_F(F_G(F_BOOL(B_NOT c))),
                       F_WEAK_IMP(S_CLOCK_COMP c r1, S_CLOCK_COMP c r2)))))
    /\
    (F_CLOCK_COMP (WEAK_CLOCK c) (F_WEAK_IMP(r1,r2)) = 
      F_W_CLOCK c (F_WEAK_IMP (S_CLOCK_COMP c r1,
                               S_CLOCK_COMP c r2)))
    /\
    (F_CLOCK_COMP (WEAK_CLOCK c) (F_ABORT (f,b)) =
      F_W_CLOCK c (F_ABORT(F_CLOCK_COMP (WEAK_CLOCK c) f, B_AND(c,b))))
    /\
    (F_CLOCK_COMP (WEAK_CLOCK c) (F_WEAK_CLOCK(f,c1)) =   
      F_CLOCK_COMP (WEAK_CLOCK c1) f)
    /\
    (F_CLOCK_COMP (WEAK_CLOCK c) (F_STRONG_CLOCK(f,c1)) =   
      F_CLOCK_COMP (STRONG_CLOCK c1) f)`;

val _ = export_theory();