Theory FNF_F_sf_def

Up to index of Isabelle/HOL/HOL-Complex/CSP/CSP_T/CSP_F/FNF_F

theory FNF_F_sf_def
imports CSP_F
begin
           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2005         |
            |                January 2006               |
            |                  April 2006  (modified)   |
            |                  March 2007  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory FNF_F_sf_def
imports CSP_F
begin

(*  The following simplification rules are deleted in this theory file *)
(*  because they unexpectly rewrite UnionT and InterT.                 *)
(*                  disj_not1: (~ P | Q) = (P --> Q)                   *)

declare disj_not1 [simp del]

(*  The following simplification rules are deleted in this theory file *)
(*       P (if Q then x else y) = ((Q --> P x) & (~ Q --> P y))        *)

declare split_if [split del]

(*****************************************************************

         1. definition of full sequential-formed process
         2. 
         3. 

 *****************************************************************)

(*==========================================================*
 |                                                          |
 |                    Definition of fsfF                    |
 |                                                          |
 *==========================================================*)

consts
  fsfF_proc :: "('p,'a) proc set"

inductive "fsfF_proc"

intros
fsfF_proc_int_nat:
  "[| N ~= {} ; ALL n:N. Rf n : fsfF_proc |]
   ==> (!nat :N .. Rf) : fsfF_proc"

fsfF_proc_int_set:
  "[| Xs ~= {} ; ALL X:Xs. Rf X : fsfF_proc |]
   ==> (!set :Xs .. Rf) : fsfF_proc"

fsfF_proc_ext:
  "[| ALL a:A. Pf a : fsfF_proc ;
      Q = SKIP | Q = DIV | Q = STOP |]
   ==> ((? :A -> Pf) [+] Q) : fsfF_proc"

lemmas fsfF_proc_int = fsfF_proc_int_nat fsfF_proc_int_set

(*-------------------------------------------*
 |   sequential-formed SSKIP, SDIV, SSTOP    |
 *-------------------------------------------*)

consts
  SSKIP     :: "('p,'a) proc"
  SDIV      :: "('p,'a) proc"
  SSTOP     :: "('p,'a) proc"

defs
  SSKIP_def : "SSKIP == (? y:{} -> DIV) [+] SKIP"
  SDIV_def  : "SDIV  == (? y:{} -> DIV) [+] DIV"
  SSTOP_def : "SSTOP == (? y:{} -> DIV) [+] STOP"

(*** small lemmas ***)

(* in *)

lemma fsfF_SSKIP_in[simp]: "SSKIP : fsfF_proc"
apply (simp add: SSKIP_def)
apply (simp add: fsfF_proc.intros)
done

lemma fsfF_SDIV_in[simp]: "SDIV : fsfF_proc"
apply (simp add: SDIV_def)
apply (simp add: fsfF_proc.intros)
done

lemma fsfF_SSTOP_in[simp]: "SSTOP : fsfF_proc"
apply (simp add: SSTOP_def)
apply (simp add: fsfF_proc.intros)
done

(* eqF *)

lemma cspF_SSKIP_eqF: "SKIP =F SSKIP"
apply (simp add: SSKIP_def)
apply (rule cspF_rw_right)
apply (rule cspF_Ext_choice_rule)
apply (simp)
done

lemma cspF_SDIV_eqF: "DIV =F SDIV"
apply (simp add: SDIV_def)
apply (rule cspF_rw_right)
apply (rule cspF_Ext_choice_rule)
apply (simp)
done

lemma cspF_SSTOP_eqF: "STOP =F SSTOP"
apply (simp add: SSTOP_def)
apply (rule cspF_rw_right)
apply (rule cspF_Ext_choice_rule)
apply (simp)
done

(*----------------------------------------------------------*
 |                          iff                             |
 *----------------------------------------------------------*)

(* proc *)

lemma fsfF_proc_iff:
  "(SP : fsfF_proc) = 
    ((EX N Rf.
        N ~= {} & SP = !nat :N .. Rf & (ALL n:N. Rf n : fsfF_proc)) |
     (EX Xs Rf.
        Xs ~= {} & SP = !set :Xs .. Rf & (ALL X:Xs. Rf X : fsfF_proc)) |
     (EX A Pf Q.
        SP = (? :A -> Pf) [+] Q & (ALL a:A. Pf a : fsfF_proc) &
        (Q = SKIP | Q = DIV | Q = STOP)))"

apply (rule iffI)

(* => *)
 apply (erule fsfF_proc.elims)
 apply (simp_all)

(* <= *)
 apply (elim conjE exE disjE)
 apply (simp_all add: fsfF_proc.intros)
done

lemma fsfF_procI:
   "((EX N Rf.
        N ~= {} & SP = !nat :N .. Rf & (ALL n:N. Rf n : fsfF_proc)) |
     (EX Xs Rf.
        Xs ~= {} & SP = !set :Xs .. Rf & (ALL X:Xs. Rf X : fsfF_proc)) |
     (EX A Pf Q.
        SP = (? :A -> Pf) [+] Q & (ALL a:A. Pf a : fsfF_proc) &
        (Q = SKIP | Q = DIV | Q = STOP)))
    ==> SP : fsfF_proc"
apply (simp add: fsfF_proc_iff[of SP])
done

lemma fsfF_procE:
  "[| SP : fsfF_proc ;
     ((EX N Rf.
        N ~= {} & SP = !nat :N .. Rf & (ALL n:N. Rf n : fsfF_proc)) |
     (EX Xs Rf.
        Xs ~= {} & SP = !set :Xs .. Rf & (ALL X:Xs. Rf X : fsfF_proc)) |
     (EX A Pf Q.
        SP = (? :A -> Pf) [+] Q & (ALL a:A. Pf a : fsfF_proc) &
        (Q = SKIP | Q = DIV | Q = STOP)))
      ==> S |]
    ==> S"
apply (simp add: fsfF_proc_iff[of SP])
done

(*----------------------------------------------------------*
 |                    subexpression                         |
 *----------------------------------------------------------*)

(* proc *)

lemma Rf_fsfF_proc_nat:
  "[| !nat :N .. Rf : fsfF_proc ; n:N |]
   ==> Rf n : fsfF_proc"
apply (erule fsfF_procE)
apply (elim disjE conjE exE)
apply (simp_all)
done

lemma Rf_fsfF_proc_set:
  "[| !set :Xs .. Rf : fsfF_proc ; X:Xs |]
   ==> Rf X : fsfF_proc"
apply (erule fsfF_procE)
apply (elim disjE conjE exE)
apply (simp_all)
done

lemma Pf_fsfF_proc:
  "[| (? :A -> Pf) [+] Q : fsfF_proc ; a:A |]
   ==> Pf a : fsfF_proc"
apply (erule fsfF_procE)
apply (simp)
done

lemma Qf_range:
  "(? :A -> Pf) [+] Q : fsfF_proc 
   ==> Q = SKIP | Q = DIV | Q = STOP"
apply (erule fsfF_procE)
apply (simp)
done

(*======================================================*
 |                                                      |
 |    function to decompose : fsfF_decompo_int, ext     |
 |                                                      |
 *======================================================*)

consts
  fsfF_N ::
     "('p,'a) proc => nat set"
  fsfF_Xs ::
     "('p,'a) proc => 'a set set"
  fsfF_Rf_nat ::
     "('p,'a) proc => (nat => ('p,'a) proc)"
  fsfF_Rf_set ::
     "('p,'a) proc => ('a set => ('p,'a) proc)"

  fsfF_A ::
     "('p,'a) proc => 'a set"
  fsfF_Pf ::
     "('p,'a) proc => ('a => ('p,'a) proc)"
  fsfF_Q ::
     "('p,'a) proc => ('p,'a) proc"

(* they are partial functions *)

recdef fsfF_N "{}"
  "fsfF_N (!nat :N .. Rf) = N"
recdef fsfF_Xs "{}"
  "fsfF_Xs (!set :Xs .. Rf) = Xs"
recdef fsfF_Rf_nat "{}"
  "fsfF_Rf_nat (!nat :N .. Rf) = Rf"
recdef fsfF_Rf_set "{}"
  "fsfF_Rf_set (!set :Xs .. Rf) = Rf"
recdef fsfF_A "{}"
  "fsfF_A ((? :A -> Pf) [+] Q) = A"
recdef fsfF_Pf "{}"
  "fsfF_Pf ((? :A -> Pf) [+] Q) = Pf"
recdef fsfF_Q "{}"
  "fsfF_Q ((? :A -> Pf) [+] Q) = Q"

(*------------------------*
 |     decomposition      |
 *------------------------*)

lemma cspF_fsfF_proc_decompo:
   "P : fsfF_proc ==>
     ((P = (!nat : fsfF_N P .. fsfF_Rf_nat P)) |
      (P = (!set : fsfF_Xs P .. fsfF_Rf_set P)) |
      (P = (? : fsfF_A P -> fsfF_Pf P [+] fsfF_Q P)))"
apply (erule fsfF_proc.elims)
apply (simp_all)
done

(****************** to add them again ******************)

declare split_if    [split]
declare disj_not1   [simp]

end

lemmas fsfF_proc_int: 

  [| N ≠ {}; ∀n∈N. Rf n ∈ fsfF_proc |] ==> !nat :N .. Rf ∈ fsfF_proc
  [| Xs ≠ {}; ∀X∈Xs. Rf X ∈ fsfF_proc |] ==> !set :Xs .. Rf ∈ fsfF_proc

lemmas fsfF_proc_int: 

  [| N ≠ {}; ∀n∈N. Rf n ∈ fsfF_proc |] ==> !nat :N .. Rf ∈ fsfF_proc
  [| Xs ≠ {}; ∀X∈Xs. Rf X ∈ fsfF_proc |] ==> !set :Xs .. Rf ∈ fsfF_proc

lemma fsfF_SSKIP_in: 

  SSKIP ∈ fsfF_proc

lemma fsfF_SDIV_in: 

  SDIV ∈ fsfF_proc

lemma fsfF_SSTOP_in: 

  SSTOP ∈ fsfF_proc

lemma cspF_SSKIP_eqF: 

  SKIP =F SSKIP

lemma cspF_SDIV_eqF: 

  DIV =F SDIV

lemma cspF_SSTOP_eqF: 

  STOP =F SSTOP

lemma fsfF_proc_iff: 

  (SP ∈ fsfF_proc) =
  ((∃N Rf. N ≠ {} ∧ SP = !nat :N .. Rf ∧ (∀n∈N. Rf n ∈ fsfF_proc)) ∨
   (∃Xs Rf. Xs ≠ {} ∧ SP = !set :Xs .. Rf ∧ (∀X∈Xs. Rf X ∈ fsfF_proc)) ∨
   (∃A Pf Q.
       SP = ? :A -> Pf [+] Q ∧
       (∀a∈A. Pf a ∈ fsfF_proc) ∧ (Q = SKIP ∨ Q = DIV ∨ Q = STOP)))

lemma fsfF_procI: 

  (∃N Rf. N ≠ {} ∧ SP = !nat :N .. Rf ∧ (∀n∈N. Rf n ∈ fsfF_proc)) ∨
  (∃Xs Rf. Xs ≠ {} ∧ SP = !set :Xs .. Rf ∧ (∀X∈Xs. Rf X ∈ fsfF_proc)) ∨
  (∃A Pf Q.
      SP = ? :A -> Pf [+] Q ∧
      (∀a∈A. Pf a ∈ fsfF_proc) ∧ (Q = SKIP ∨ Q = DIV ∨ Q = STOP))
  ==> SP ∈ fsfF_proc

lemma fsfF_procE: 

  [| SP ∈ fsfF_proc;
     (∃N Rf. N ≠ {} ∧ SP = !nat :N .. Rf ∧ (∀n∈N. Rf n ∈ fsfF_proc)) ∨
     (∃Xs Rf. Xs ≠ {} ∧ SP = !set :Xs .. Rf ∧ (∀X∈Xs. Rf X ∈ fsfF_proc)) ∨
     (∃A Pf Q.
         SP = ? :A -> Pf [+] Q ∧
         (∀a∈A. Pf a ∈ fsfF_proc) ∧ (Q = SKIP ∨ Q = DIV ∨ Q = STOP))
     ==> S |]
  ==> S

lemma Rf_fsfF_proc_nat: 

  [| !nat :N .. Rf ∈ fsfF_proc; n ∈ N |] ==> Rf n ∈ fsfF_proc

lemma Rf_fsfF_proc_set: 

  [| !set :Xs .. Rf ∈ fsfF_proc; X ∈ Xs |] ==> Rf X ∈ fsfF_proc

lemma Pf_fsfF_proc: 

  [| ? :A -> Pf [+] Q ∈ fsfF_proc; a ∈ A |] ==> Pf a ∈ fsfF_proc

lemma Qf_range: 

  ? :A -> Pf [+] Q ∈ fsfF_proc ==> Q = SKIP ∨ Q = DIV ∨ Q = STOP

lemma cspF_fsfF_proc_decompo: 

  P ∈ fsfF_proc
  ==> P = !nat :fsfF_N P .. fsfF_Rf_nat P ∨
      P = !set :fsfF_Xs P .. fsfF_Rf_set P ∨
      P = ? :fsfF_A P -> fsfF_Pf P [+] fsfF_Q P