Theory FNF_F_sf_induct

           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2005         |
            |                January 2006               |
            |                  March 2007  (modified)   |
            |                 August 2007  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory FNF_F_sf_induct
imports FNF_F_sf_int
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. induction method for full sequentialization
         2. 
         3. 

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

(*============================================================*
 |                         Pfun P1 P2                         |
 *============================================================*)

consts
  fsfF_induct2_rel ::
  "(('p,'a) proc => ('p,'a) proc => ('p,'a) proc) =>

   ('a set => ('a => ('p,'a) proc) => ('p,'a) proc =>
    'a set => ('a => ('p,'a) proc) => ('p,'a) proc => 
    ('a => ('p,'a) proc) =>
    ('a => ('p,'a) proc) => 
    ('a => ('p,'a) proc) => ('p,'a) proc) =>

   (('p,'a) proc * ('p,'a) proc * ('p,'a) proc) set"

  fsfF_induct2 ::
  "(('p,'a) proc => ('p,'a) proc => ('p,'a) proc) =>

   ('a set => ('a => ('p,'a) proc) => ('p,'a) proc => 
    'a set => ('a => ('p,'a) proc) => ('p,'a) proc => 
    ('a => ('p,'a) proc) =>
    ('a => ('p,'a) proc) =>
    ('a => ('p,'a) proc) => ('p,'a) proc) =>

   ('p,'a) proc => ('p,'a) proc => ('p,'a) proc"

(* 

   Pfun P1 P2
   SP_step  A1 Pf1 Q1 A2 Pf2 Q2 SPf SPf1 SPf2

*)

(*** relation ***)

inductive 
  "fsfF_induct2_rel Pfun SP_step"

intros
fsfF_induct2_rel_etc_left:
  "[| P1 ~: fsfF_proc |]
   ==> (P1, P2, Pfun P1 P2)
   : fsfF_induct2_rel Pfun SP_step"

fsfF_induct2_rel_etc_right:
  "[| P2 ~: fsfF_proc |]
   ==> (P1, P2, Pfun P1 P2)
   : fsfF_induct2_rel Pfun SP_step"

fsfF_induct2_rel_step_int_left:
  "[| ALL c. if (c: sumset C1)
             then (Rf1 c, P2, SRf c) : fsfF_induct2_rel Pfun SP_step
             else SRf c = DIV ;                           
      sumset C1 ~= {} ; ALL c: sumset C1. Rf1 c : fsfF_proc ;
      P2 : fsfF_proc |]
   ==>
   ((!! :C1 .. Rf1), P2, !! c:C1 .. SRf c)
   : fsfF_induct2_rel Pfun SP_step"

fsfF_induct2_rel_step_int_right:
  "[| ALL c. if (c: sumset C2)
             then (P1, Rf2 c, SRf c) : fsfF_induct2_rel Pfun SP_step
             else SRf c = DIV ;                           
      sumset C2 ~= {} ; ALL c: sumset C2. Rf2 c : fsfF_proc ;
      P1 : fsfF_proc ; (EX A Pf Q. P1 = (? :A -> Pf) [+] Q) |]
   ==>
   (P1, (!! :C2 .. Rf2),  !! c:C2 .. SRf c)
   : fsfF_induct2_rel Pfun SP_step"

fsfF_induct2_rel_step:
  "[| ALL a. if (a:A1 & a:A2) 
             then (Pf1 a, Pf2 a, SPf a) : fsfF_induct2_rel Pfun SP_step
             else SPf a = DIV ;
      ALL a. if a:A1 
             then (Pf1 a, (? :A2 -> Pf2) [+] Q2, SPf1 a) : fsfF_induct2_rel Pfun SP_step
             else SPf1 a = DIV ;
      ALL a. if a:A2
             then ((? :A1 -> Pf1) [+] Q1, Pf2 a, SPf2 a) : fsfF_induct2_rel Pfun SP_step
             else SPf2 a = DIV ;
      ALL a:A1. Pf1 a : fsfF_proc ;
      ALL a:A2. Pf2 a : fsfF_proc ;
      Q1 = SKIP | Q1 = DIV | Q1 = STOP ;
      Q2 = SKIP | Q2 = DIV | Q2 = STOP |]
   ==> 
   ((? :A1 -> Pf1) [+] Q1, (? :A2 -> Pf2) [+] Q2, 
    SP_step A1 Pf1 Q1 A2 Pf2 Q2 SPf SPf1 SPf2)
   : fsfF_induct2_rel Pfun SP_step"

(*** function ***)

defs
  fsfF_induct2_def:
    "fsfF_induct2 Pfun SP_step ==
     (%P1 P2. THE SP. (P1, P2, SP) 
      : fsfF_induct2_rel Pfun SP_step)"

(****************************************************************
 |                      uniquness                               |
 ****************************************************************)

lemma fsfF_induct2_rel_unique_in_lm:
   "(P1, P2, SP1) : fsfF_induct2_rel Pfun SP_step
    ==> (ALL SP2. ((P1, P2, SP2) : fsfF_induct2_rel Pfun SP_step
                   --> SP1 = SP2))"
apply (rule fsfF_induct2_rel.induct[of P1 P2 SP1])
apply (simp)

(* etc_left *)
apply (intro allI impI)
apply (rotate_tac -1)
apply (erule fsfF_induct2_rel.elims)
apply (simp_all)
apply (simp add: fsfF_proc_int)
apply (simp add: fsfF_proc_ext)

(* etc_right *)
apply (intro allI impI)
apply (rotate_tac -1)
apply (erule fsfF_induct2_rel.elims)
apply (simp_all)
apply (simp add: fsfF_proc_int)
apply (simp add: fsfF_proc_ext)

(* step_int_left *)
apply (intro allI impI)
apply (rotate_tac -1)
apply (erule fsfF_induct2_rel.elims, simp_all)

 apply (elim conjE exE)
 apply (rotate_tac -3)
 apply (drule sym)
 apply (simp add: fsfF_proc_int)

 apply (subgoal_tac "SRf = SRfa", simp)
 apply (simp add: expand_fun_eq)
 apply (intro allI)
 apply (drule_tac x="x" in spec)+
 apply (case_tac "x : sumset C1")
 apply (simp)
 apply (simp)

 apply (elim conjE exE)
 apply (rotate_tac -3)
 apply (drule sym)
 apply (simp)

 apply (elim conjE exE)
 apply (simp)

(* step_int_right *)
apply (intro allI impI)
apply (rotate_tac -1)
apply (erule fsfF_induct2_rel.elims, simp_all)

 apply (elim conjE exE)
 apply (rotate_tac -2)
 apply (drule sym)
 apply (simp add: fsfF_proc_int)

 apply (subgoal_tac "SRf = SRfa", simp)
 apply (simp add: expand_fun_eq)
 apply (intro allI)
 apply (drule_tac x="x" in spec)+
 apply (case_tac "x : sumset C2")
 apply (simp)
 apply (simp)

(* step *)
apply (intro allI impI)
apply (rotate_tac -1)
apply (erule fsfF_induct2_rel.elims, simp_all)

 apply (elim conjE exE)
 apply (rotate_tac -3)
 apply (drule sym)
 apply (simp add: fsfF_proc_ext)

 apply (elim conjE exE)
 apply (rotate_tac -2)
 apply (drule sym)
 apply (simp add: fsfF_proc_ext)

 apply (subgoal_tac "SPf = SPfa & SPf1 = SPf1a & SPf2 = SPf2a ", simp)
 apply (elim conjE)

  apply (rule conjI)
  apply (simp add: expand_fun_eq)
  apply (rule allI)
  apply (drule_tac x="x" in spec)+
  apply (case_tac "x : A1a & x : A2a")
  apply (simp_all)

  apply (rule conjI)
  apply (simp (no_asm_simp) add: expand_fun_eq)
  apply (rule allI)
  apply (drule_tac x="x" in spec)+
  apply (case_tac "x : A1a")
  apply (simp_all)

  apply (simp (no_asm_simp) add: expand_fun_eq)
  apply (rule allI)
  apply (drule_tac x="x" in spec)+
  apply (case_tac "x : A2a")
  apply (simp_all)
done

(*-----------------------*
 |        unique         |
 *-----------------------*)

lemma fsfF_induct2_rel_unique:
   "[| (P1, P2, SP1) : fsfF_induct2_rel Pfun SP_step;
       (P1, P2, SP2) : fsfF_induct2_rel Pfun SP_step |]
    ==> SP1 = SP2"
by (simp add: fsfF_induct2_rel_unique_in_lm)

lemma fsfF_induct2_rel_EX1:
   "(EX SP. (P1, P2, SP) : fsfF_induct2_rel Pfun SP_step)
 = (EX! SP. (P1, P2, SP) : fsfF_induct2_rel Pfun SP_step)"
apply (rule iffI)

 apply (erule exE)
 apply (rule_tac a="SP" in ex1I)
 apply (simp)
 apply (simp add: fsfF_induct2_rel_unique)

 apply (elim ex1_implies_exE)
 apply (simp)
done

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

(* etc_left *)

lemma fsfF_induct2_rel_etc_left_iff:
  "P1 ~: fsfF_proc
   ==> (P1, P2, SP) : fsfF_induct2_rel Pfun SP_step
       = (SP = Pfun P1 P2)"
apply (rule)
apply (erule fsfF_induct2_rel.elims, simp_all)
 apply (simp add: fsfF_proc_int)
 apply (simp add: fsfF_proc_ext)
apply (simp add: fsfF_induct2_rel_etc_left)
done

(* etc_right *)

lemma fsfF_induct2_rel_etc_right_iff:
  "P2 ~: fsfF_proc
   ==> (P1, P2, SP) : fsfF_induct2_rel Pfun SP_step
       = (SP = Pfun P1 P2)"
apply (rule)
apply (erule fsfF_induct2_rel.elims, simp_all)

 apply (simp add: fsfF_proc_int)
 apply (simp add: fsfF_proc_ext)
apply (simp add: fsfF_induct2_rel_etc_right)
done

(* step_int_left *)

lemma fsfF_induct2_rel_step_int_left_iff:
  "[| ALL c. if c: sumset C1 then 
               (Rf1 c, P2, SRf c) : fsfF_induct2_rel Pfun SP_step
             else SRf c = DIV ;
      sumset C1 ~= {} ; ALL c. Rf1 c : fsfF_proc ;
      P2 : fsfF_proc |]
   ==>
   ((!! :C1 .. Rf1), P2, SP) : fsfF_induct2_rel Pfun SP_step
   = (SP = !! :C1 .. SRf)"
apply (rule)
apply (erule fsfF_induct2_rel.elims, simp_all)
 apply (elim conjE)
 apply (rotate_tac -3)
 apply (drule sym)
 apply (simp add: fsfF_proc_int)

 apply (subgoal_tac "SRfa = SRf", simp)
 apply (simp add: expand_fun_eq)
 apply (rule allI)
 apply (drule_tac x="x" in spec)+
 apply (case_tac "x : sumset C1a")
 apply (simp add: fsfF_induct2_rel_unique)

 apply (simp)
 apply (elim conjE)
 apply (rotate_tac -3)
 apply (drule sym)
 apply (simp)

apply (simp add: fsfF_induct2_rel_step_int_left)
done

(* step *)

lemma fsfF_induct2_rel_step_iff:
  "[| ALL a. if (a:A1 & a:A2) 
             then (Pf1 a, Pf2 a, SPf a) : fsfF_induct2_rel Pfun SP_step
             else SPf a = DIV ;
      ALL a. if a:A1 
             then (Pf1 a, (? :A2 -> Pf2) [+] Q2, SPf1 a) : fsfF_induct2_rel Pfun SP_step
             else SPf1 a = DIV ;
      ALL a. if a:A2
             then ((? :A1 -> Pf1) [+] Q1, Pf2 a, SPf2 a) : fsfF_induct2_rel Pfun SP_step
             else SPf2 a = DIV ;
      ALL a:A1. Pf1 a : fsfF_proc ;
      ALL a:A2. Pf2 a : fsfF_proc ;
      Q1 = SKIP | Q1 = DIV | Q1 = STOP ;
      Q2 = SKIP | Q2 = DIV | Q2 = STOP |]
   ==> 
   ((? :A1 -> Pf1) [+] Q1, (? :A2 -> Pf2) [+] Q2, SP) : fsfF_induct2_rel Pfun SP_step
   = (SP = SP_step A1 Pf1 Q1 A2 Pf2 Q2 SPf SPf1 SPf2)"
apply (rule)
apply (erule fsfF_induct2_rel.elims, simp_all)
 apply (elim conjE)
 apply (rotate_tac -3)
 apply (drule sym)
 apply (simp add: fsfF_proc_ext)

 apply (elim conjE)
 apply (rotate_tac -2)
 apply (drule sym)
 apply (simp add: fsfF_proc_ext)

 apply (subgoal_tac "SPf = SPfa & SPf1 = SPf1a & SPf2 = SPf2a ", simp)
 apply (simp (no_asm_simp) add: expand_fun_eq)
 apply (intro allI conjI)
 apply (elim conjE)
 apply (drule_tac x="x" in spec)+
 apply (case_tac "x : A1a & x : A2a")
 apply (simp add: fsfF_induct2_rel_unique)
 apply (simp)
 apply (drule_tac x="x" in spec)+
 apply (case_tac "x : A1a")
 apply (simp add: fsfF_induct2_rel_unique)
 apply (simp)
 apply (drule_tac x="x" in spec)+
 apply (case_tac "x : A2a")
 apply (simp add: fsfF_induct2_rel_unique)
 apply (simp)

apply (simp add: fsfF_induct2_rel_step)
done

(****************************************************************
 |                      existency                               |
 ****************************************************************)

(*** exists ***)

lemma fsfF_induct2_rel_exists_notin1:
   "P1 ~: fsfF_proc
    ==> (EX SP. (P1, P2, SP)
                : fsfF_induct2_rel Pfun SP_step)"
apply (rule_tac x="Pfun P1 P2" in exI)
apply (simp add: fsfF_induct2_rel.intros)
done

lemma fsfF_induct2_rel_exists_notin2:
   "P2 ~: fsfF_proc
    ==> (EX SP. (P1, P2, SP)
                : fsfF_induct2_rel Pfun SP_step)"
apply (rule_tac x="Pfun P1 P2" in exI)
apply (simp add: fsfF_induct2_rel.intros)
done

(*** in fsfF_proc ***)

(********* P1 and P2 *********)

lemma fsfF_induct2_rel_exists_in_lm1:
 "P2 : fsfF_proc ==>
   (ALL a:A. Pf a : fsfF_proc &
   (ALL P2. EX SP. (Pf a, P2, SP) : fsfF_induct2_rel Pfun SP_step)) &
   (Q = SKIP | Q = DIV | Q = STOP)
    --> (EX SP. (? :A -> Pf [+] Q, P2, SP) : fsfF_induct2_rel Pfun SP_step)"
apply (rule fsfF_proc.induct[of P2])
apply (simp)

(* proc int *)
apply (intro allI impI)
apply (elim conjE)
apply (simp add: Ball_def)
apply (simp add: dist_ALL_imply_conjE)
apply (elim conjE)
apply (simp add: choice_ALL_imply_EX)
apply (erule exE)
apply (rule_tac x="!! c:C .. (if c: sumset C then f c else DIV)" in exI)
apply (rule fsfF_induct2_rel.intros)
apply (simp_all)
apply (rule allI)
apply (simp split: split_if)
apply (rule fsfF_proc_ext)
apply (simp_all)

(* step *)
apply (intro allI impI)
apply (elim conjE)
apply (rotate_tac -2)
apply (erule dist_BALL_conjE)

apply (simp add: exchange_ALL_BALL)
apply (frule_tac x="? :Aa -> Pfa [+] Qa" in spec)
apply (erule ALL_BALL_funE)
apply (drule_tac x="Pfa" in spec)
apply (simp add: choice_BALL_EX)
apply (elim exE)
apply (erule dist_BALL_conjE)
apply (simp add: choice_BALL_EX)
apply (elim exE)
apply (rename_tac Aa Pfa Qa SPf1 SPf SPf2)
apply (rule_tac x="SP_step A Pf Q Aa Pfa Qa 
                   (%a. if (a:A & a:Aa) then SPf a else DIV)
                   (%a. if (a:A) then SPf1 a else DIV)
                   (%a. if (a:Aa) then SPf2 a else DIV)" in exI)
apply (rule fsfF_induct2_rel.intros)
apply (simp_all)
apply (simp split: split_if)
apply (simp split: split_if)
apply (simp split: split_if)
done

lemma fsfF_induct2_rel_exists_in_lm:
   "P1 : fsfF_proc
      ==> (ALL P2. (EX SP. (P1, P2, SP) 
              : fsfF_induct2_rel Pfun SP_step))"
apply (rule fsfF_proc.induct[of P1])
apply (simp)

apply (intro allI)
apply (case_tac "P2 ~: fsfF_proc")
apply (simp add: fsfF_induct2_rel_exists_notin2)
apply (simp)

(* P2 : fsfF_proc *)
apply (erule dist_BALL_conjE)
apply (simp add: exchange_ALL_BALL)
apply (drule_tac x="P2" in spec)
apply (simp add: choice_BALL_EX)
apply (erule exE)
apply (rule_tac x="!! c:C .. (if c: sumset C then f c else DIV)" in exI)
apply (rule fsfF_induct2_rel.intros)
apply (simp_all)
apply (rule allI)
apply (simp split: split_if)

apply (intro allI)
apply (case_tac "P2 ~: fsfF_proc")
apply (simp add: fsfF_induct2_rel_exists_notin2)
apply (simp)

(* step *)
apply (case_tac "P2 ~: fsfF_proc")
apply (simp add: fsfF_induct2_rel_exists_notin2)
apply (simp add: fsfF_induct2_rel_exists_in_lm1)
done

lemma fsfF_induct2_rel_exists_in:
   "P1 : fsfF_proc
    ==> (EX SP. (P1, P2, SP) :  fsfF_induct2_rel Pfun SP_step)"
apply (insert fsfF_induct2_rel_exists_in_lm
              [of P1 Pfun SP_step])
apply (simp_all)
done

(*-----------------------*
 |        exists         |
 *-----------------------*)

lemma fsfF_induct2_rel_exists:
   "EX SP. (P1, P2, SP) :  fsfF_induct2_rel Pfun SP_step"
apply (case_tac "P1 ~: fsfF_proc")
apply (simp add: fsfF_induct2_rel_exists_notin1)
apply (simp add: fsfF_induct2_rel_exists_in)
done

(*-----------------------*
 |    uniquely exists    |
 *-----------------------*)

lemma fsfF_induct2_rel_unique_exists:
   "EX! SP. (P1, P2, SP) :  fsfF_induct2_rel Pfun SP_step"
apply (simp add: fsfF_induct2_rel_EX1[THEN sym])
apply (simp add: fsfF_induct2_rel_exists)
done

(*------------------------------------------------------------*
 |                        in fsfF_proc                        |
 *------------------------------------------------------------*)

lemma fsfF_induct2_rel_in_lm:
   "[| (P1, P2, SP) : fsfF_induct2_rel Pfun SP_step ;

    !! A1 Pf1 Q1 A2 Pf2 Q2 SPf SPf1 SPf2. 
                   [| ALL a:A1. Pf1 a : fsfF_proc ; 
                      ALL a:A2. Pf2 a : fsfF_proc ; 
                      ALL a:(A1 Int A2). SPf a : fsfF_proc ;
                      ALL a:A1. SPf1 a : fsfF_proc ;
                      ALL a:A2. SPf2 a : fsfF_proc ;

                      Q1 = SKIP | Q1 = DIV | Q1 = STOP ;
                      Q2 = SKIP | Q2 = DIV | Q2 = STOP |]
        ==> SP_step A1 Pf1 Q1 A2 Pf2 Q2 SPf SPf1 SPf2 : fsfF_proc |]

    ==> (P1 : fsfF_proc & P2 : fsfF_proc)
             --> SP : fsfF_proc"
apply (rule fsfF_induct2_rel.induct[of P1 P2 SP])
apply (simp_all)
apply (intro impI)
apply (rule fsfF_proc.intros)
apply (simp_all)
apply (intro impI)
apply (rule fsfF_proc.intros)
apply (simp_all)
done

(*------------------------------------*
 |                 in                 |
 *------------------------------------*)

lemma fsfF_induct2_rel_in:
   "[| (P1, P2, SP) : fsfF_induct2_rel Pfun SP_step ;
       P1 : fsfF_proc ;
       P2 : fsfF_proc ;

    !! A1 Pf1 Q1 A2 Pf2 Q2 SPf SPf1 SPf2. 
                   [| ALL a:A1. Pf1 a : fsfF_proc ; 
                      ALL a:A2. Pf2 a : fsfF_proc ; 
                      ALL a:(A1 Int A2). SPf a : fsfF_proc ;
                      ALL a:A1. SPf1 a : fsfF_proc ;
                      ALL a:A2. SPf2 a : fsfF_proc ;

                      Q1 = SKIP | Q1 = DIV | Q1 = STOP ;
                      Q2 = SKIP | Q2 = DIV | Q2 = STOP |]
        ==> SP_step A1 Pf1 Q1 A2 Pf2 Q2 SPf SPf1 SPf2 : fsfF_proc |]

    ==> SP : fsfF_proc"
apply (simp add: fsfF_induct2_rel_in_lm)
done

(*------------------------------------------------------------*
 |             syntactical transformation to fsfF             |
 *------------------------------------------------------------*)

(*** relation ***)

lemma cspF_fsfF_induct2_rel_eqF:
    "[| (P1, P2, SP) : fsfF_induct2_rel Pfun SP_step ;

    !!C1 Rf1 P2. sumset C1 ~= {} ==> 
      Pfun (!! :C1 .. Rf1) P2 =F (!! c:C1 .. Pfun (Rf1 c) P2) ;
    !!P1 C2 Rf2. sumset C2 ~= {} ==>
      Pfun P1 (!! :C2 .. Rf2) =F (!! c:C2 .. Pfun P1 (Rf2 c)) ;

    !!A1 Pf1 Q1 A2 Pf2 Q2. [| Q1 = SKIP | Q1 = DIV | Q1 = STOP ;
                              Q2 = SKIP | Q2 = DIV | Q2 = STOP |]
             ==> Pfun (? :A1 -> Pf1 [+] Q1) (? :A2 -> Pf2 [+] Q2)
                 =F SP_step A1 Pf1 Q1 A2 Pf2 Q2
                   (%a. Pfun (Pf1 a) (Pf2 a))
                   (%a. Pfun (Pf1 a) (? :A2 -> Pf2 [+] Q2))
                   (%a. Pfun (? :A1 -> Pf1 [+] Q1) (Pf2 a)) ;

    !!A1 Pf1 Q1 A2 Pf2 Q2 SPf SQf SPf1 SQf1 SPf2 SQf2. 
         [| ALL a:(A1 Int A2). SPf a =F SQf a ; 
            ALL a:A1. SPf1 a =F SQf1 a ; ALL a:A2. SPf2 a =F SQf2 a |]
      ==> SP_step A1 Pf1 Q1 A2 Pf2 Q2 SPf SPf1 SPf2 =F
          SP_step A1 Pf1 Q1 A2 Pf2 Q2 SQf SQf1 SQf2 |]

  ==> Pfun P1 P2 =F SP"
apply (rule fsfF_induct2_rel.induct[of P1 P2 SP])
apply (simp_all)

(* etc *)
apply (rule cspF_reflex)
apply (rule cspF_reflex)

(* step_int_left *)
apply (rule cspF_rw_left)
apply (subgoal_tac
   "Pfun (!! :C1 .. Rf1) P2a =F (!! c:C1 .. (Pfun (Rf1 c) P2a))")
apply (assumption)
apply (simp_all)

(* step_int_right *)
apply (rule cspF_rw_left)
apply (subgoal_tac 
  "Pfun P1a (!! :C2 .. Rf2) =F (!! c:C2 .. (Pfun P1a (Rf2 c)))")
apply (assumption)
apply (simp_all)

(* step *)
apply (rule cspF_rw_left)
apply (subgoal_tac 
  "Pfun (? :A1 -> Pf1 [+] Q1) (? :A2 -> Pf2 [+] Q2) =F 
          SP_step A1 Pf1 Q1 A2 Pf2 Q2 
                  (%a. Pfun (Pf1 a) (Pf2 a))
                  (%a. Pfun (Pf1 a) (? :A2 -> Pf2 [+] Q2))
                  (%a. Pfun (? :A1 -> Pf1 [+] Q1) (Pf2 a))")
apply (assumption)
apply (simp_all)
done

(*************************************************************
                  relation --> function
 *************************************************************)

lemma fsfF_induct2_in_rel:
    "(P1, P2, fsfF_induct2 Pfun SP_step P1 P2)
     : fsfF_induct2_rel Pfun SP_step"
apply (simp add: fsfF_induct2_def)
apply (rule theI'
  [of "(%R. (P1, P2, R) : fsfF_induct2_rel Pfun SP_step)"])
apply (simp add: fsfF_induct2_rel_unique_exists)
done

lemma fsfF_induct2_from_rel:
    "((P1, P2, SP) : fsfF_induct2_rel Pfun SP_step) 
   = (fsfF_induct2 Pfun SP_step P1 P2 = SP)"
apply (rule iffI)
apply (simp add: fsfF_induct2_def)
apply (simp add: fsfF_induct2_rel_unique_exists the1_equality)

apply (drule sym)
apply (simp add: fsfF_induct2_in_rel)
done

lemma fsfF_induct2_to_rel:
    "(fsfF_induct2 Pfun SP_step P1 P2 = SP)
   = ((P1, P2, SP) : fsfF_induct2_rel Pfun SP_step)"
by (simp add: fsfF_induct2_from_rel)

(*************************************************************
                          function
 *************************************************************)

lemma fsfF_induct2_etc:
  "[| P1 ~: fsfF_proc | P2 ~: fsfF_proc |]
   ==> fsfF_induct2 Pfun SP_step P1 P2 = Pfun P1 P2"
apply (simp add: fsfF_induct2_to_rel)
apply (erule disjE)
apply (simp add: fsfF_induct2_rel_etc_left_iff)
apply (simp add: fsfF_induct2_rel_etc_right_iff)
done

lemma fsfF_induct2_step_int_left:
  "[| sumset C1 ~= {} ; ALL c: sumset C1. Rf1 c : fsfF_proc ;
      P2 : fsfF_proc |]
   ==>
   fsfF_induct2 Pfun SP_step (!! :C1 .. Rf1) P2
   = !! c:C1 .. (if c: sumset C1 then 
                 fsfF_induct2 Pfun SP_step (Rf1 c) P2 else DIV)"
apply (simp add: fsfF_induct2_to_rel)
apply (rule fsfF_induct2_rel_step_int_left)
apply (simp_all)
apply (simp split: split_if)
apply (simp add: fsfF_induct2_in_rel)
done

lemma fsfF_induct2_step_int_right:
  "[| sumset C2 ~= {} ; ALL c: sumset C2. Rf2 c : fsfF_proc ;
      P1 : fsfF_proc ; (EX A Pf Q. P1 = (? :A -> Pf) [+] Q) |]
   ==>
   fsfF_induct2 Pfun SP_step P1 (!! :C2 .. Rf2)
   = !! c:C2 .. (if c: sumset C2 then 
                 fsfF_induct2 Pfun SP_step P1 (Rf2 c) else DIV)"
apply (simp add: fsfF_induct2_to_rel)
apply (rule fsfF_induct2_rel_step_int_right)
apply (simp_all)
apply (simp split: split_if)
apply (simp add: fsfF_induct2_in_rel)
done

lemma fsfF_induct2_step:
  "[| ALL a:A1. Pf1 a : fsfF_proc ;
      ALL a:A2. Pf2 a : fsfF_proc ;
      Q1 = SKIP | Q1 = DIV | Q1 = STOP ;
      Q2 = SKIP | Q2 = DIV | Q2 = STOP |]
   ==> 
   fsfF_induct2 Pfun SP_step 
               ((? :A1 -> Pf1) [+] Q1) ((? :A2 -> Pf2) [+] Q2)
 = (SP_step  A1 Pf1 Q1 A2 Pf2 Q2
   (%a. if a:A1 Int A2 then fsfF_induct2 Pfun SP_step (Pf1 a) (Pf2 a) else DIV)
   (%a. if a:A1 then fsfF_induct2 Pfun SP_step (Pf1 a) ((? :A2 -> Pf2) [+] Q2) else DIV)
   (%a. if a:A2 then fsfF_induct2 Pfun SP_step ((? :A1 -> Pf1) [+] Q1) (Pf2 a) else DIV))"
apply (simp add: fsfF_induct2_to_rel)
apply (rule fsfF_induct2_rel_step)
apply (simp_all split: split_if)
apply (simp_all add: fsfF_induct2_in_rel)
done

lemmas fsfF_induct2 =
       fsfF_induct2_etc
       fsfF_induct2_step_int_left
       fsfF_induct2_step_int_right
       fsfF_induct2_step

(*------------------------------------------------------------*
 |                        in fsfF_proc                        |
 *------------------------------------------------------------*)

lemma fsfF_induct2_in:
   "[| P1 : fsfF_proc ;
       P2 : fsfF_proc ;

    !! A1 Pf1 Q1 A2 Pf2 Q2 SPf SPf1 SPf2. 
                   [| ALL a:A1. Pf1 a : fsfF_proc ; 
                      ALL a:A2. Pf2 a : fsfF_proc ; 
                      ALL a:(A1 Int A2). SPf a : fsfF_proc ;
                      ALL a:A1. SPf1 a : fsfF_proc ;
                      ALL a:A2. SPf2 a : fsfF_proc ;

                      Q1 = SKIP | Q1 = DIV | Q1 = STOP ;
                      Q2 = SKIP | Q2 = DIV | Q2 = STOP |]
        ==> SP_step A1 Pf1 Q1 A2 Pf2 Q2 SPf SPf1 SPf2 : fsfF_proc |]
    ==> fsfF_induct2 Pfun SP_step P1 P2 : fsfF_proc"
apply (rule fsfF_induct2_rel_in
            [of P1 P2 _ Pfun SP_step])
apply (simp_all add: fsfF_induct2_in_rel)
done

(*------------------------------------------------------------*
 |             syntactical transformation to fsfF             |
 *------------------------------------------------------------*)

lemma cspF_fsfF_induct2_eqF:
"[| 
    !!C1 Rf1 P2. sumset C1 ~= {} ==> 
    Pfun (!! :C1 .. Rf1) P2 =F (!! c:C1 .. Pfun (Rf1 c) P2);
    !!P1 C2 Rf2. sumset C2 ~= {} ==> 
    Pfun P1 (!! :C2 .. Rf2) =F (!! c:C2 .. Pfun P1 (Rf2 c));

    !!A1 Pf1 Q1 A2 Pf2 Q2. [| Q1 = SKIP | Q1 = DIV | Q1 = STOP ;
                              Q2 = SKIP | Q2 = DIV | Q2 = STOP |]
             ==> Pfun (? :A1 -> Pf1 [+] Q1) (? :A2 -> Pf2 [+] Q2)
                 =F SP_step A1 Pf1 Q1 A2 Pf2 Q2
                   (%a. Pfun (Pf1 a) (Pf2 a))
                   (%a. Pfun (Pf1 a) (? :A2 -> Pf2 [+] Q2))
                   (%a. Pfun (? :A1 -> Pf1 [+] Q1) (Pf2 a)) ;

    !!A1 Pf1 Q1 A2 Pf2 Q2 SPf SQf SPf1 SQf1 SPf2 SQf2. 
         [| ALL a:(A1 Int A2). SPf a =F SQf a ; 
            ALL a:A1. SPf1 a =F SQf1 a ; ALL a:A2. SPf2 a =F SQf2 a |]
      ==> SP_step A1 Pf1 Q1 A2 Pf2 Q2 SPf SPf1 SPf2 =F
          SP_step A1 Pf1 Q1 A2 Pf2 Q2 SQf SQf1 SQf2 |]

  ==> Pfun P1 P2 =F fsfF_induct2 Pfun SP_step P1 P2"
apply (rule cspF_fsfF_induct2_rel_eqF
            [of P1 P2 "fsfF_induct2 Pfun SP_step P1 P2"
                Pfun SP_step])
apply (simp_all add: fsfF_induct2_in_rel)
done

(*===========================================================*
 |                                                           |
 |               fsfF_induct1 (take one process)             |
 |                                                           |
 *===========================================================*)

consts
  fsfF_induct1 ::
  "(('p,'a) proc => ('p,'a) proc) =>
   ('a set => ('a => ('p,'a) proc) => ('p,'a) proc =>
              ('a => ('p,'a) proc) => ('p,'a) proc) =>
   ('p,'a) proc => ('p,'a) proc"

(* 
   Pfun P1
   SP_step  A1 Pf1 Q1 SPf1
*)

defs
  fsfF_induct1_def :
    "fsfF_induct1 Pfun SP_step == (%P1. 
       (fsfF_induct2 (%P1 P2. Pfun P1) 
                     (%A1 Pf1 Q1 A2 Pf2 Q2 SPf SPf1 SPf2. SP_step A1 Pf1 Q1 SPf1)
                      P1 SDIV))"

(*------------------------------------------------------------*
 |                        in fsfF_proc                        |
 *------------------------------------------------------------*)

lemma fsfF_induct1_in:
    "[| P1 : fsfF_proc ;
    !! A Pf Q SPf. [| ALL a:A. Pf a : fsfF_proc ; 
                      ALL a:A. SPf a : fsfF_proc ; 
                      Q = SKIP | Q = DIV | Q = STOP |]
            ==> SP_step A Pf Q SPf : fsfF_proc |]
     ==> fsfF_induct1  Pfun SP_step P1 : fsfF_proc"
apply (simp add: fsfF_induct1_def)
apply (rule fsfF_induct2_in)
apply (simp_all)
done

(*------------------------------------------------------------*
 |             syntactical transformation to fsfF             |
 *------------------------------------------------------------*)

lemma cspF_fsfF_induct1_eqF:
    "[| !!C1 Rf1. sumset C1 ~= {} ==>
         Pfun (!! :C1 .. Rf1) =F (!! c:C1 .. Pfun (Rf1 c)) ;

        !!A1 Pf1 Q1. Q1 = SKIP | Q1 = DIV | Q1 = STOP
             ==> Pfun (? :A1 -> Pf1 [+] Q1)
                 =F SP_step A1 Pf1 Q1 (%a. Pfun (Pf1 a)) ;

        !!A1 Pf1 Q1 SPf SQf. ALL a:A1. SPf a =F SQf a 
             ==> SP_step A1 Pf1 Q1 SPf =F SP_step A1 Pf1 Q1 SQf |]
     ==> Pfun P1 =F fsfF_induct1 Pfun SP_step P1"
apply (simp add: fsfF_induct1_def)
apply (rule cspF_rw_right)
apply (rule cspF_fsfF_induct2_eqF[THEN cspF_sym])
apply (simp_all)
apply (simp add: cspF_Rep_int_choice_unit[THEN cspF_sym])
done

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

declare split_if    [split]
declare disj_not1   [simp]

end