Up to index of Isabelle/HOL/HOL-Complex/CSP/CSP_T/CSP_F
theory CSP_F_law_etc (*-------------------------------------------*
| CSP-Prover on Isabelle2004 |
| April 2006 |
| March 2007 (modified) |
| |
| Yoshinao Isobe (AIST JAPAN) |
*-------------------------------------------*)
theory CSP_F_law_etc
imports CSP_F_law_aux CSP_T_law_etc
begin
(*------------------------*
|~| --> !!
*------------------------*)
lemma cspF_Int_choice_to_Rep:
"(P |~| Q) =F[M,M] (!nat n:{0, (Suc 0)} .. (IF (n = 0) THEN P ELSE Q))"
apply (rule cspF_rw_right)
apply (subgoal_tac
"(!nat n:{0, Suc 0} .. IF (n = 0) THEN P ELSE Q) =F[M,M]
(!nat n:({0} Un {Suc 0}) .. IF (n = 0) THEN P ELSE Q)")
apply (assumption)
apply (rule cspF_decompo)
apply (fast)
apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_Rep_int_choice_union_Int)
apply (rule cspF_decompo)
apply (rule cspF_rw_right)
apply (rule cspF_Rep_int_choice_singleton)
apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_IF)
apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_Rep_int_choice_singleton)
apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_IF)
apply (simp)
done
(*** cspF_Rep_int_choice_set_input ***)
lemma cspF_Rep_int_choice_sum_set_input:
"!! c:C .. (!set X:(Xsf c) .. (? :X -> (Pff c)))
=F[M,M] !set X:(Union {Xsf c |c. c : sumset C}) ..
(? a:X -> (!! c:{c:C. EX X. X:(Xsf c) & a:X}s .. (Pff c a)))"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Rep_int_choice_sum_set_input)
apply (rule order_antisym)
(* <= *)
apply (rule)
apply (simp add: in_failures)
apply (elim disjE conjE bexE exE)
apply (simp_all)
apply (rule_tac x="Xsf c" in exI)
apply (rule conjI)
apply (force)
apply (rule_tac x="Xa" in bexI)
apply (simp)
apply (simp)
apply (rule_tac x="Xsf c" in exI)
apply (rule conjI)
apply (force)
apply (rule conjI)
apply (force)
apply (force)
(* => *)
apply (rule)
apply (simp add: in_failures)
apply (elim disjE conjE exE bexE)
apply (simp)
apply (rule_tac x="c" in bexI)
apply (rule_tac x="Xa" in bexI)
apply (simp_all)
apply (rule_tac x="ca" in bexI)
apply (simp)
apply (force)
apply (simp)
done
lemma cspF_Rep_int_choice_set_input:
"!nat n:N .. (!set X:(Xsf n) .. (? :X -> (Pff n)))
=F[M,M] !set X:(Union {Xsf n |n. n : N}) ..
(? a:X -> (!nat n:{n:N. EX X. X:(Xsf n) & a:X} .. (Pff n a)))"
apply (simp add: Rep_int_choice_nat_def)
apply (rule cspF_rw_left)
apply (rule cspF_Rep_int_choice_sum_set_input)
apply (rule cspF_decompo)
apply (force)
apply (simp)
done
(*** cspF_Rep_int_choice_set_set_DIV ***)
lemma cspF_Rep_int_choice_set_set_DIV:
"[| Xs ~= {} ; Ys ~= {} |] ==>
!set X:Xs .. (!set Y:Ys .. (? a:(X Un Y) -> DIV))
=F[M,M] !set Z:{X Un Y |X Y. X:Xs & Y:Ys} .. (? a:Z -> DIV)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Rep_int_choice_set_set_DIV)
apply (rule order_antisym)
(* <= *)
apply (rule)
apply (simp add: in_failures)
apply (elim conjE bexE exE)
apply (rule_tac x="Xa Un Xb" in exI)
apply (force)
(* => *)
apply (rule)
apply (simp add: in_failures)
apply (elim conjE bexE exE)
apply (simp)
apply (rule_tac x="Xb" in bexI)
apply (rule_tac x="Y" in bexI)
apply (simp_all)
done
(*********************************************************
(P [+] SKIP) |~| (Q [+] SKIP)
*********************************************************)
(* p.289 *)
lemma cspF_Int_choice_Ext_choice_SKIP:
"(P [+] SKIP) |~| (Q [+] SKIP) =F[M,M] (P [+] Q [+] SKIP)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Int_choice_Ext_choice_SKIP)
apply (rule order_antisym)
(* => *)
apply (rule, simp add: in_traces in_failures)
apply (force)
(* <= *)
apply (rule, simp add: in_traces in_failures)
apply (force)
done
(*********************************************************
(P [+] DIV) |~| (Q [+] DIV)
*********************************************************)
lemma cspF_Int_choice_Ext_choice_DIV:
"(P [+] DIV) |~| (Q [+] DIV) =F[M,M] (P [+] Q [+] DIV)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Int_choice_Ext_choice_DIV)
apply (rule order_antisym)
(* => *)
apply (rule, simp add: in_traces in_failures)
apply (force)
(* <= *)
apply (rule, simp add: in_traces in_failures)
apply (force)
done
(*********************************************************
(P [+] SKIP) |~| (Q [+] DIV)
*********************************************************)
lemma cspF_Int_choice_Ext_choice_SKIP_DIV:
"(P [+] SKIP) |~| (Q [+] DIV) =F[M,M] (P [+] Q [+] SKIP)"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Int_choice_Ext_choice_SKIP_DIV)
apply (rule order_antisym)
apply (rule, simp add: in_traces in_failures, force)+
done
(*********************************************************
(P [+] DIV) |~| (Q [+] SKIP)
*********************************************************)
lemma cspF_Int_choice_Ext_choice_DIV_SKIP:
"(P [+] DIV) |~| (Q [+] SKIP) =F[M,M] (P [+] Q [+] SKIP)"
apply (rule cspF_rw_left)
apply (rule cspF_commut)
apply (rule cspF_rw_left)
apply (rule cspF_Int_choice_Ext_choice_SKIP_DIV)
apply (rule cspF_rw_left)
apply (rule cspF_decompo)
apply (rule cspF_commut)
apply (rule cspF_reflex)
apply (rule cspF_reflex)
done
(*********************************************************
(P [+] SKIP or DIV) |~| (Q [+] DIV or SKIP)
*********************************************************)
lemma cspF_Int_choice_Ext_choice_SKIP_or_DIV:
"[| P2 = SKIP | P2 = DIV ; Q2 = SKIP | Q2 = DIV |] ==>
(P1 [+] P2) |~| (Q1 [+] Q2) =F[M,M] (P1 [+] Q1 [+] (P2 |~| Q2))"
apply (elim disjE)
apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_decompo)
apply (rule cspF_reflex)
apply (rule cspF_idem)
apply (simp add: cspF_Int_choice_Ext_choice_SKIP)
apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_decompo)
apply (rule cspF_reflex)
apply (rule cspF_unit)
apply (simp add: cspF_Int_choice_Ext_choice_SKIP_DIV)
apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_decompo)
apply (rule cspF_reflex)
apply (rule cspF_unit)
apply (simp add: cspF_Int_choice_Ext_choice_DIV_SKIP)
apply (simp)
apply (rule cspF_rw_right)
apply (rule cspF_decompo)
apply (rule cspF_reflex)
apply (rule cspF_unit)
apply (simp add: cspF_Int_choice_Ext_choice_DIV)
done
(*********************************************************
(P [+] DIV) |~| P
*********************************************************)
lemma cspF_Ext_choice_DIV_Int_choice_Id:
"(P [+] DIV) |~| P =F[M,M] P"
apply (simp add: cspF_cspT_semantics)
apply (simp add: cspT_Ext_choice_DIV_Int_choice_Id)
apply (rule order_antisym)
(* => *)
apply (rule, simp add: in_failures)
apply (elim disjE conjE exE)
apply (simp_all add: in_traces)
apply (rule memF_F2)
apply (rule proc_F4)
apply (simp)
apply (simp)
apply (simp)
(* <= *)
apply (rule, simp add: in_failures)
done
end
lemma cspF_Int_choice_to_Rep:
P |~| Q =F[M,M] !nat n:{0, Suc 0} .. IF (n = 0) THEN P ELSE Q
lemma cspF_Rep_int_choice_sum_set_input:
!! c:C .. !set X:Xsf c .. ? :X -> Pff c =F[M,M] !set X:Union {Xsf c |c. c ∈ sumset C} .. ? a:X -> (!! c:{c:C. ∃X. X ∈ Xsf c ∧ a ∈ X}s .. Pff c a)
lemma cspF_Rep_int_choice_set_input:
!nat n:N .. !set X:Xsf n .. ? :X -> Pff n =F[M,M] !set X:Union {Xsf n |n. n ∈ N} .. ? a:X -> (!nat n:{n : N. ∃X. X ∈ Xsf n ∧ a ∈ X} .. Pff n a)
lemma cspF_Rep_int_choice_set_set_DIV:
[| Xs ≠ {}; Ys ≠ {} |] ==> !set X:Xs .. !set Y:Ys .. ? a:(X ∪ Y) -> DIV =F[M,M] !set Z:{X ∪ Y |X Y. X ∈ Xs ∧ Y ∈ Ys} .. ? a:Z -> DIV
lemma cspF_Int_choice_Ext_choice_SKIP:
P [+] SKIP |~| Q [+] SKIP =F[M,M] P [+] Q [+] SKIP
lemma cspF_Int_choice_Ext_choice_DIV:
P [+] DIV |~| Q [+] DIV =F[M,M] P [+] Q [+] DIV
lemma cspF_Int_choice_Ext_choice_SKIP_DIV:
P [+] SKIP |~| Q [+] DIV =F[M,M] P [+] Q [+] SKIP
lemma cspF_Int_choice_Ext_choice_DIV_SKIP:
P [+] DIV |~| Q [+] SKIP =F[M,M] P [+] Q [+] SKIP
lemma cspF_Int_choice_Ext_choice_SKIP_or_DIV:
[| P2.0 = SKIP ∨ P2.0 = DIV; Q2.0 = SKIP ∨ Q2.0 = DIV |] ==> P1.0 [+] P2.0 |~| Q1.0 [+] Q2.0 =F[M,M] P1.0 [+] Q1.0 [+] (P2.0 |~| Q2.0)
lemma cspF_Ext_choice_DIV_Int_choice_Id:
P [+] DIV |~| P =F[M,M] P