Theory FNF_F_nf_id

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

theory FNF_F_nf_id
imports FNF_F_nf_def
begin
           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2005         |
            |               February 2006               |
            |                  April 2006  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory FNF_F_nf_id = FNF_F_nf_def:

(*  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. =F --> =
         2. 
         3. 

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

(*---------------------------------------------------------*
 |              syntactically identical ?                  |
 *---------------------------------------------------------*)

(*===========================================================*
 |                      fnfF_nat_proc                        |
 *===========================================================*)

(*** Q ***)

lemma fnfF_syntactical_equality_Q_lm:
  "[| ? :A1 -> Pf1 [+] DIV |~| !set Y:Ys1 .. ? a:Y -> DIV <=F 
      ? :A2 -> Pf2 [+] SKIP |~| !set Y:Ys2 .. ? a:Y -> DIV |]
   ==> False"
apply (simp add: cspF_semantics)
apply (elim conjE)
apply (simp add: subdomT_iff)
apply (drule_tac x="<Tick>" in spec)
apply (simp add: in_traces)
done

lemma fnfF_syntactical_equality_Q:
  "[| Q1 = SKIP | Q1 = DIV ; Q2 = SKIP | Q2 = DIV ;
      ? :A1 -> Pf1 [+] Q1 |~| !set Y:Ys1 .. ? a:Y -> DIV =F 
      ? :A2 -> Pf2 [+] Q2 |~| !set Y:Ys2 .. ? a:Y -> DIV |]
   ==> Q1 = Q2"
apply (elim disjE)
apply (simp_all  add: cspF_eq_ref_iff)
apply (insert fnfF_syntactical_equality_Q_lm
       [of A2 Pf2 Ys2 A1 Pf1 Ys1])
apply (simp)
apply (insert fnfF_syntactical_equality_Q_lm
       [of A1 Pf1 Ys1 A2 Pf2 Ys2])
apply (simp)
done

(*** A ***)

lemma fnfF_syntactical_equality_Union_lm:
  "[| Union Ys1 <= A1 ; Union Ys2 <= A2 ; 
      Q = SKIP | Q = DIV ;
      ? :A1 -> Pf1 [+] Q |~| !set Y:Ys1 .. ? a:Y -> DIV <=F 
      ? :A2 -> Pf2 [+] Q |~| !set Y:Ys2 .. ? a:Y -> DIV |]
   ==> A2 <= A1"
apply (simp add: cspF_semantics)
apply (elim conjE)
apply (simp add: subdomT_iff)
apply (rule subsetI)
apply (drule_tac x="<Ev x>" in spec)
apply (erule disjE)
apply (simp add: in_traces)
apply (elim disjE bexE)
apply (simp)
apply (force)
apply (simp add: in_traces)
apply (elim disjE bexE)
apply (simp)
apply (force)
done

lemma fnfF_syntactical_equality_Union:
  "[| Union Ys1 <= A1 ; Union Ys2 <= A2 ; 
      Q = SKIP | Q = DIV ;
      ? :A1 -> Pf1 [+] Q |~| !set Y:Ys1 .. ? a:Y -> DIV =F 
      ? :A2 -> Pf2 [+] Q |~| !set Y:Ys2 .. ? a:Y -> DIV |]
   ==> A1 = A2"
apply (simp add: cspF_eq_ref_iff)
apply (rule equalityI)
apply (simp add: fnfF_syntactical_equality_Union_lm[of Ys2 A2 Ys1 A1 Q Pf2 Pf1])
apply (simp add: fnfF_syntactical_equality_Union_lm[of Ys1 A1 Ys2 A2 Q Pf1 Pf2])
done

(*** Yf ***)

lemma fnfF_syntactical_equality_Yf_DIV_lm:
  "[| Union Ys1 <= A ; Union Ys2 <= A ; 
      fnfF_set_condition A Ys1 ;
      ? :A -> Pf1 [+] DIV |~| !set Y:Ys1 .. ? a:Y -> DIV <=F
      ? :A -> Pf2 [+] DIV |~| !set Y:Ys2 .. ? a:Y -> DIV |]
   ==> Ys2 <= Ys1"
apply (rule subsetI)
apply (simp add: cspF_semantics)
apply (elim conjE)
apply (simp add: subsetF_iff)
apply (simp add: in_failures)
apply (simp add: in_traces)
apply (drule_tac x="<>" in spec)
apply (simp)
apply (drule_tac x="UNIV - (Ev ` x)" in spec)
apply (drule mp)
apply (rule_tac x="x" in bexI)
apply (simp_all)
apply (elim conjE bexE)
apply (subgoal_tac "a <= x")
apply (unfold fnfF_set_condition_def)
apply (drule_tac x="x" in spec)
apply (drule mp)
apply (rule conjI)
apply (rule_tac x="a" in bexI)
apply (simp)
apply (simp)
apply (rule subsetI)
apply (simp)
apply (rule disjI1)
apply (subgoal_tac "xa : Union Ys2")
apply (force)
apply (force)
apply (simp)

apply (fold fnfF_set_condition_def)
apply (auto)
done

lemma fnfF_syntactical_equality_Yf_SKIP_lm:
  "[| Union Ys1 <= A ; Union Ys2 <= A ; 
      fnfF_set_condition A Ys1 ;
      ? :A -> Pf1 [+] SKIP |~| !set Y:Ys1 .. ? a:Y -> DIV <=F
      ? :A -> Pf2 [+] SKIP |~| !set Y:Ys2 .. ? a:Y -> DIV |]
   ==> Ys2 <= Ys1"
apply (rule subsetI)
apply (simp add: cspF_semantics)
apply (elim conjE)
apply (simp add: subsetF_iff)
apply (simp add: in_failures)
apply (simp add: in_traces)
apply (drule_tac x="<>" in spec)
apply (simp)
apply (drule_tac x="UNIV - (Ev ` x)" in spec)
apply (drule mp)
apply (rule_tac x="x" in bexI)
apply (simp_all)

apply (case_tac "UNIV - Ev ` x <= Evset")
apply (simp add: Evset_def)
apply (force)

apply (simp)
apply (elim conjE bexE)
apply (subgoal_tac "a <= x")
apply (unfold fnfF_set_condition_def)
apply (drule_tac x="x" in spec)
apply (drule mp)
apply (rule conjI)
apply (rule_tac x="a" in bexI)
apply (simp)
apply (simp)

apply (rule subsetI)
apply (simp)
apply (rule disjI1)
apply (subgoal_tac "xa : Union Ys2")
apply (force)
apply (force)
apply (simp)

apply (fold fnfF_set_condition_def)
apply (auto)
done

lemma fnfF_syntactical_equality_Yf:
  "[| Union Ys1 <= A ; Union Ys2 <= A ; 
      fnfF_set_condition A Ys1 ; fnfF_set_condition A Ys2 ;
      Q = SKIP | Q = DIV ;
      ? :A -> Pf1 [+] Q |~| !set Y:Ys1 .. ? a:Y -> DIV =F
      ? :A -> Pf2 [+] Q |~| !set Y:Ys2 .. ? a:Y -> DIV |]
   ==> Ys1 = Ys2"
apply (simp add: cspF_eq_ref_iff)
apply (erule disjE)
apply (rule equalityI)
apply (simp add: fnfF_syntactical_equality_Yf_SKIP_lm[of Ys2 A Ys1 Pf2 Pf1])
apply (simp add: fnfF_syntactical_equality_Yf_SKIP_lm[of Ys1 A Ys2 Pf1 Pf2])
apply (rule equalityI)
apply (simp add: fnfF_syntactical_equality_Yf_DIV_lm[of Ys2 A Ys1 Pf2 Pf1])
apply (simp add: fnfF_syntactical_equality_Yf_DIV_lm[of Ys1 A Ys2 Pf1 Pf2])
done

(*** Pf ***)

(* T DIV *)

lemma fnfF_syntactical_equality_Pf_T_DIV_lm:
  "[| a:A ;
      ? :A -> Pf1 [+] DIV |~| !set Y:Ys .. ? a:Y -> DIV <=T
      ? :A -> Pf2 [+] DIV |~| !set Y:Ys .. ? a:Y -> DIV |]
   ==> Pf1 a <=T Pf2 a"
apply (simp add: cspT_semantics)

apply (simp add: subdomT_iff)
apply (simp add: in_traces)
apply (intro allI impI)
apply (drule_tac x="<Ev a> ^^ t" in spec)
apply (insert trace_nil_or_Tick_or_Ev)
apply (drule_tac x="t" in spec)
apply (elim disjE conjE exE)
apply (auto)
done

(* T SKIP *)

lemma fnfF_syntactical_equality_Pf_T_SKIP_lm:
  "[| a:A ;
      ? :A -> Pf1 [+] SKIP |~| !set Y:Ys .. ? a:Y -> DIV <=T
      ? :A -> Pf2 [+] SKIP |~| !set Y:Ys .. ? a:Y -> DIV |]
   ==> Pf1 a <=T Pf2 a"
apply (simp add: cspT_semantics)

apply (simp add: subdomT_iff)
apply (simp add: in_traces)
apply (intro allI impI)
apply (drule_tac x="<Ev a> ^^ t" in spec)
apply (insert trace_nil_or_Tick_or_Ev)
apply (drule_tac x="t" in spec)
apply (elim disjE conjE exE)
apply (auto)
done

(* F DIV *)

lemma fnfF_syntactical_equality_Pf_F_DIV_lm:
  "[| a:A ;
      ? :A -> Pf1 [+] DIV |~| !set Y:Ys .. ? a:Y -> DIV <=F
      ? :A -> Pf2 [+] DIV |~| !set Y:Ys .. ? a:Y -> DIV |]
   ==> Pf1 a <=F Pf2 a"
apply (simp add: cspF_cspT_semantics)
apply (erule conjE)
apply (rule conjI)
apply (rule fnfF_syntactical_equality_Pf_T_DIV_lm)
apply (simp)
apply (simp)

apply (simp add: subsetF_iff)
apply (simp add: in_failures)
apply (intro allI impI)
apply (drule_tac x="<Ev a> ^^ s" in spec)
apply (drule_tac x="X" in spec)
apply (insert trace_nil_or_Tick_or_Ev)
apply (drule_tac x="s" in spec)
apply (elim disjE conjE exE)

apply (force)
apply (force)
apply (force)
done

(* F SKIP *)

lemma fnfF_syntactical_equality_Pf_F_SKIP_lm:
  "[| a:A ;
      ? :A -> Pf1 [+] SKIP |~| !set Y:Ys .. ? a:Y -> DIV <=F
      ? :A -> Pf2 [+] SKIP |~| !set Y:Ys .. ? a:Y -> DIV |]
   ==> Pf1 a <=F Pf2 a"
apply (simp add: cspF_cspT_semantics)
apply (erule conjE)
apply (rule conjI)
apply (rule fnfF_syntactical_equality_Pf_T_SKIP_lm)
apply (simp)
apply (simp)

apply (simp add: subsetF_iff)
apply (simp add: in_failures)
apply (intro allI impI)
apply (drule_tac x="<Ev a> ^^ s" in spec)
apply (drule_tac x="X" in spec)
apply (insert trace_nil_or_Tick_or_Ev)
apply (drule_tac x="s" in spec)
apply (elim disjE conjE exE)

apply (force)
apply (force)
apply (force)
done

lemma fnfF_syntactical_equality_Pf:
  "[| a:A ; Q = SKIP | Q = DIV ;
      ? :A -> Pf1 [+] Q |~| !set Y:Ys .. ? a:Y -> DIV =F
      ? :A -> Pf2 [+] Q |~| !set Y:Ys .. ? a:Y -> DIV |]
   ==> Pf1 a =F Pf2 a"
apply (simp add: cspF_eq_ref_iff)
apply (erule disjE)
apply (simp add: fnfF_syntactical_equality_Pf_F_SKIP_lm[of a A Pf1 Ys Pf2])
apply (simp add: fnfF_syntactical_equality_Pf_F_SKIP_lm[of a A Pf2 Ys Pf1])
apply (simp add: fnfF_syntactical_equality_Pf_F_DIV_lm[of a A Pf1 Ys Pf2])
apply (simp add: fnfF_syntactical_equality_Pf_F_DIV_lm[of a A Pf2 Ys Pf1])
done

(*------------------------------------------------------------------*
 |                fnfF_proc ---> syntactical equality               |
 *------------------------------------------------------------------*)

lemma fnfF_syntactical_equality_only_if_lm:
   "P1 : fnfF_proc ==> 
    ALL P2. (P2 : fnfF_proc & P1 =F P2) --> P1 = P2"
apply (rule fnfF_proc.induct[of P1])
apply (simp)

apply (intro allI impI)
apply (elim conjE)
apply (rotate_tac -2)
apply (erule fnfF_proc.elims)
apply (simp)

apply (subgoal_tac "Q = Qa")
apply (subgoal_tac "A = Aa")
apply (subgoal_tac "Ys = Ysa")
apply (subgoal_tac "Pf = Pfa")
apply (simp)

(* Pf *)
apply (simp add: expand_fun_eq)
apply (rule allI)
apply (drule_tac x="x" in spec)
apply (drule_tac x="x" in spec)
apply (case_tac "x:Aa")
 apply (simp)
 apply (elim bexE conjE)
 apply (drule_tac x="Pfa x" in spec)
 apply (drule mp)
  apply (rule conjI)
   apply (simp)
   apply (simp only: fnfF_syntactical_equality_Pf)
 apply (simp)
 apply (simp)

apply (simp add: fnfF_syntactical_equality_Yf)
apply (rule fnfF_syntactical_equality_Union)
apply (simp_all)
apply (rule fnfF_syntactical_equality_Q)
apply (simp_all)
done

lemma fnfF_syntactical_equality_only_if:
   "[| P1 : fnfF_proc ; 
       P2 : fnfF_proc ; 
        P1 =F P2 |]
    ==> P1 = P2"
apply (simp add: fnfF_syntactical_equality_only_if_lm)
done

(*--------------------------*
 |         theorem          |
 *--------------------------*)

theorem fnfF_syntactical_equality:
   "[| P1 : fnfF_proc ; P2 : fnfF_proc |] ==>
    (P1 =F P2) = (P1 = P2)"
apply (rule iffI)
apply (simp only: fnfF_syntactical_equality_only_if)
apply (simp)
done

(*===========================================================*
 |                        XfnfF_proc                         |
 *===========================================================*)

theorem XfnfF_syntactical_equality:
   "[| P1 : XfnfF_proc ; P2 : XfnfF_proc |] ==>
    (P1 =F P2) = (P1 = P2)"
apply (rule iffI)
apply (simp add: XfnfF_proc_def)
apply (elim conjE exE)
apply (simp)
apply (subgoal_tac "Pf = Pfa")
apply (simp)
apply (simp add: expand_fun_eq)
apply (rule allI)
apply (drule_tac x="x" in spec)+
apply (subgoal_tac "Pf x =F Pfa x")
apply (simp add: fnfF_syntactical_equality)

apply (rule cspF_rw_left)
apply (simp)
apply (rule cspF_rw_right)
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (simp)
apply (simp)
done

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

declare split_if    [split]
declare disj_not1   [simp]

end

lemma fnfF_syntactical_equality_Q_lm: 

  ? :A1.0 -> Pf1.0 [+] DIV |~| !set Y:Ys1.0 .. ? a:Y -> DIV <=F 
  ? :A2.0 -> Pf2.0 [+] SKIP |~| !set Y:Ys2.0 .. ? a:Y -> DIV
  ==> False

lemma fnfF_syntactical_equality_Q: 

  [| Q1.0 = SKIP ∨ Q1.0 = DIV; Q2.0 = SKIP ∨ Q2.0 = DIV;
     ? :A1.0 -> Pf1.0 [+] Q1.0 |~| !set Y:Ys1.0 .. ? a:Y -> DIV =F 
     ? :A2.0 -> Pf2.0 [+] Q2.0 |~| !set Y:Ys2.0 .. ? a:Y -> DIV |]
  ==> Q1.0 = Q2.0

lemma fnfF_syntactical_equality_Union_lm: 

  [| Union Ys1.0 ⊆ A1.0; Union Ys2.0 ⊆ A2.0; Q = SKIP ∨ Q = DIV;
     ? :A1.0 -> Pf1.0 [+] Q |~| !set Y:Ys1.0 .. ? a:Y -> DIV <=F 
     ? :A2.0 -> Pf2.0 [+] Q |~| !set Y:Ys2.0 .. ? a:Y -> DIV |]
  ==> A2.0 ⊆ A1.0

lemma fnfF_syntactical_equality_Union: 

  [| Union Ys1.0 ⊆ A1.0; Union Ys2.0 ⊆ A2.0; Q = SKIP ∨ Q = DIV;
     ? :A1.0 -> Pf1.0 [+] Q |~| !set Y:Ys1.0 .. ? a:Y -> DIV =F 
     ? :A2.0 -> Pf2.0 [+] Q |~| !set Y:Ys2.0 .. ? a:Y -> DIV |]
  ==> A1.0 = A2.0

lemma fnfF_syntactical_equality_Yf_DIV_lm: 

  [| Union Ys1.0 ⊆ A; Union Ys2.0 ⊆ A; fnfF_set_condition A Ys1.0;
     ? :A -> Pf1.0 [+] DIV |~| !set Y:Ys1.0 .. ? a:Y -> DIV <=F 
     ? :A -> Pf2.0 [+] DIV |~| !set Y:Ys2.0 .. ? a:Y -> DIV |]
  ==> Ys2.0 ⊆ Ys1.0

lemma fnfF_syntactical_equality_Yf_SKIP_lm: 

  [| Union Ys1.0 ⊆ A; Union Ys2.0 ⊆ A; fnfF_set_condition A Ys1.0;
     ? :A -> Pf1.0 [+] SKIP |~| !set Y:Ys1.0 .. ? a:Y -> DIV <=F 
     ? :A -> Pf2.0 [+] SKIP |~| !set Y:Ys2.0 .. ? a:Y -> DIV |]
  ==> Ys2.0 ⊆ Ys1.0

lemma fnfF_syntactical_equality_Yf: 

  [| Union Ys1.0 ⊆ A; Union Ys2.0 ⊆ A; fnfF_set_condition A Ys1.0;
     fnfF_set_condition A Ys2.0; Q = SKIP ∨ Q = DIV;
     ? :A -> Pf1.0 [+] Q |~| !set Y:Ys1.0 .. ? a:Y -> DIV =F 
     ? :A -> Pf2.0 [+] Q |~| !set Y:Ys2.0 .. ? a:Y -> DIV |]
  ==> Ys1.0 = Ys2.0

lemma fnfF_syntactical_equality_Pf_T_DIV_lm: 

  [| a ∈ A;
     ? :A -> Pf1.0 [+] DIV |~| !set Y:Ys .. ? a:Y -> DIV <=T 
     ? :A -> Pf2.0 [+] DIV |~| !set Y:Ys .. ? a:Y -> DIV |]
  ==> Pf1.0 a <=T Pf2.0 a

lemma fnfF_syntactical_equality_Pf_T_SKIP_lm: 

  [| a ∈ A;
     ? :A -> Pf1.0 [+] SKIP |~| !set Y:Ys .. ? a:Y -> DIV <=T 
     ? :A -> Pf2.0 [+] SKIP |~| !set Y:Ys .. ? a:Y -> DIV |]
  ==> Pf1.0 a <=T Pf2.0 a

lemma fnfF_syntactical_equality_Pf_F_DIV_lm: 

  [| a ∈ A;
     ? :A -> Pf1.0 [+] DIV |~| !set Y:Ys .. ? a:Y -> DIV <=F 
     ? :A -> Pf2.0 [+] DIV |~| !set Y:Ys .. ? a:Y -> DIV |]
  ==> Pf1.0 a <=F Pf2.0 a

lemma fnfF_syntactical_equality_Pf_F_SKIP_lm: 

  [| a ∈ A;
     ? :A -> Pf1.0 [+] SKIP |~| !set Y:Ys .. ? a:Y -> DIV <=F 
     ? :A -> Pf2.0 [+] SKIP |~| !set Y:Ys .. ? a:Y -> DIV |]
  ==> Pf1.0 a <=F Pf2.0 a

lemma fnfF_syntactical_equality_Pf: 

  [| a ∈ A; Q = SKIP ∨ Q = DIV;
     ? :A -> Pf1.0 [+] Q |~| !set Y:Ys .. ? a:Y -> DIV =F 
     ? :A -> Pf2.0 [+] Q |~| !set Y:Ys .. ? a:Y -> DIV |]
  ==> Pf1.0 a =F Pf2.0 a

lemma fnfF_syntactical_equality_only_if_lm: 

  P1.0 ∈ fnfF_proc ==> ∀P2. P2 ∈ fnfF_proc ∧ P1.0 =F P2 --> P1.0 = P2

lemma fnfF_syntactical_equality_only_if: 

  [| P1.0 ∈ fnfF_proc; P2.0 ∈ fnfF_proc; P1.0 =F P2.0 |] ==> P1.0 = P2.0

theorem fnfF_syntactical_equality: 

  [| P1.0 ∈ fnfF_proc; P2.0 ∈ fnfF_proc |] ==> (P1.0 =F P2.0) = (P1.0 = P2.0)

theorem XfnfF_syntactical_equality: 

  [| P1.0 ∈ XfnfF_proc; P2.0 ∈ XfnfF_proc |] ==> (P1.0 =F P2.0) = (P1.0 = P2.0)