Up to index of Isabelle/HOL/HOL-Complex/CSP/CSP_T/CSP_F/DFP
theory DFP_DFtick (*-------------------------------------------*
| DFtick |
| |
| June 2007 |
| |
| Yoshinao Isobe (AIST JAPAN) |
*-------------------------------------------*)
theory DFP_DFtick
imports DFP_Deadlock
begin
(*****************************************************************
1. The most abstract deadlockfree process DFtick
*****************************************************************)
declare csp_prefix_ss_def[simp]
(*********************************************************
event
*********************************************************)
datatype DFtickName = DFtick
(*** Spc ***)
consts
DFtickfun ::
"DFtickName => (DFtickName, 'a) proc"
primrec
"DFtickfun (DFtick) = (! x -> $(DFtick)) |~| SKIP "
defs (overloaded)
Set_DFtickfun_def [simp]: "PNfun == DFtickfun"
(*---------------------------------------------------*
| n-replicted spec |
*---------------------------------------------------*)
datatype RDFtickName = RDFtick
(*** Spc ***)
consts
NatDFtick ::
"nat => (RDFtickName, 'a) proc
=> (RDFtickName, 'a) proc"
primrec
"NatDFtick 0 P = P"
"NatDFtick (Suc n) P = ((! x -> NatDFtick n P) |~| SKIP) |~| P"
consts
RDFtickfun ::
"RDFtickName
=> (RDFtickName, 'a) proc"
primrec
"RDFtickfun (RDFtick)
= (! x -> (!nat n .. NatDFtick n ($(RDFtick))) |~| SKIP)"
defs (overloaded)
Set_RDFtickfun_def [simp]: "PNfun == RDFtickfun"
(*********************************************************
DFtick lemma
*********************************************************)
lemma guardedfun_DFtick[simp]:
"guardedfun DFtickfun"
by (simp add: guardedfun_def, rule allI, induct_tac p, simp_all)
lemma guardedfun_RDFtick[simp]:
"guardedfun RDFtickfun"
apply (simp add: guardedfun_def)
apply (rule allI)
apply (induct_tac p)
apply (simp)
apply (rule allI)
apply (induct_tac n)
apply (simp_all)
done
(* -------------------------------------------------*
| |
| syntactical approach --> semantical approach |
| |
* -------------------------------------------------*)
(*** sub ***)
lemma DFtick_is_DeadlockFree:
"($DFtick) isDeadlockFree"
apply (simp add: DeadlockFree_def)
apply (rule allI)
apply (induct_tac s rule: induct_trace)
(* base case *)
apply (simp)
apply (subgoal_tac
"((DFtickfun (DFtick))::(DFtickName, 'a) proc) =F
($(DFtick)::(DFtickName, 'a) proc)")
apply (simp add: cspF_eqF_semantics)
apply (erule conjE)
apply (rotate_tac 1)
apply (drule sym)
apply (simp)
apply (rotate_tac 1)
apply (drule sym)
apply (simp (no_asm) add: in_failures)
apply (simp add: Evset_def)
apply (force)
apply (tactic {* cspF_unwind_tac 1 *})
apply (simp add: CPOmode_or_CMSmode_or_MIXmode)
apply (subgoal_tac
"failures (($DFtick)::(DFtickName, 'a) proc) MF =
failures ((DFtickfun DFtick)::(DFtickName, 'a) proc) MF")
apply (simp)
apply (rotate_tac -1)
apply (drule sym)
apply (simp (no_asm) add: in_failures)
apply (intro impI)
apply (simp add: in_failures)
apply (subgoal_tac
"(($DFtick)::(DFtickName, 'a) proc) =F
((DFtickfun DFtick)::(DFtickName, 'a) proc)")
apply (simp add: cspF_eqF_semantics)
apply (tactic {* cspF_unwind_tac 1 *})
apply (simp add: CPOmode_or_CMSmode_or_MIXmode)
done
(*** main ***)
lemma DFtick_DeadlockFree:
"$DFtick <=F P ==> P isDeadlockFree"
apply (insert DFtick_is_DeadlockFree)
apply (simp add: DeadlockFree_def)
apply (simp add: cspF_refF_semantics)
apply (auto)
done
(* -------------------------------------------------*
| |
| semantical approach --> syntactical approach |
| |
* -------------------------------------------------*)
lemma traces_included_in_DFtick:
"t :t traces ((FIX DFtickfun) (DFtick)) (fstF o MF)"
apply (induct_tac t rule: induct_trace)
(* <> *)
apply (simp)
(* <Tick> *)
apply (simp add: FIX_def)
apply (simp add: in_traces)
apply (rule_tac x="Suc 0" in exI)
apply (simp add: FIXn_def)
apply (simp add: Subst_procfun_prod_def)
apply (simp add: in_traces)
(* <Eva>^^s *)
apply (simp add: FIX_def)
apply (simp add: in_traces)
apply (erule disjE)
apply (simp)
apply (rule_tac x="Suc 0" in exI)
apply (simp add: FIXn_def)
apply (simp add: Subst_procfun_prod_def)
apply (simp add: in_traces)
apply (erule exE)
apply (rule_tac x="Suc n" in exI)
apply (simp add: FIXn_def)
apply (simp add: Subst_procfun_prod_def)
apply (simp add: in_traces)
done
lemma failures_included_in_DFtick_lm:
"(X ~= UNIV | Tick : sett t) -->
(t,X) :f failures ((FIX DFtickfun) (DFtick)) MF"
apply (induct_tac t rule: induct_trace)
(* <> *)
apply (simp add: FIX_def)
apply (intro impI)
apply (simp add: in_failures)
apply (rule_tac x="Suc 0" in exI)
apply (simp add: FIXn_def)
apply (simp add: Subst_procfun_prod_def)
apply (simp add: in_failures)
apply (case_tac "EX x. x ~: X")
apply (elim exE)
apply (case_tac "x = Tick")
apply (simp)
apply (simp add: Evset_def)
apply (force)
apply (simp add: not_Tick_to_Ev)
apply (force)
apply (force)
(* <Tick> *)
apply (simp add: FIX_def)
apply (simp add: in_failures)
apply (rule_tac x="Suc 0" in exI)
apply (simp add: FIXn_def)
apply (simp add: Subst_procfun_prod_def)
apply (simp add: in_failures)
(* <Eva>^^s *)
apply (intro impI)
apply (simp add: FIX_def)
apply (simp add: in_failures)
apply (erule exE)
apply (rule_tac x="Suc n" in exI)
apply (simp add: FIXn_def)
apply (simp add: Subst_procfun_prod_def)
apply (simp add: in_failures)
done
lemma failures_included_in_DFtick:
"[| X ~= UNIV | Tick : sett t |] ==>
(t,X) :f failures ((FIX DFtickfun) (DFtick)) MF"
by (simp add: failures_included_in_DFtick_lm)
lemma DeadlockFree_DFtick:
"P isDeadlockFree ==> $DFtick <=F P"
apply (rule cspF_rw_left)
apply (rule cspF_FIX)
prefer 2
apply (simp)
apply (simp add: CPOmode_or_CMSmode_or_MIXmode)
apply (simp add: cspF_refF_semantics)
apply (rule conjI)
(* trace *)
apply (simp add: subdomT_iff)
apply (simp add: traces_included_in_DFtick)
(* failures *)
apply (simp add: subsetF_iff)
apply (intro allI impI)
apply (rule failures_included_in_DFtick)
apply (simp add: DeadlockFree_def)
apply (drule_tac x="s" in spec)
apply (auto)
done
(* -------------------------------------------------*
| |
| syntactical approach <--> semantical approach |
| |
* -------------------------------------------------*)
theorem DeadlockFree_DFtick_ref:
"P isDeadlockFree = ($DFtick <=F P)"
apply (rule)
apply (simp add: DeadlockFree_DFtick)
apply (simp add: DFtick_DeadlockFree)
done
(*================================================================*
| |
| n-replicted DF specification |
| |
*================================================================*)
(*******************************************************************
relating function between DFtickName and Rep...
*******************************************************************)
(*** ref1 ***)
consts
RepDF_to_DF :: "RDFtickName =>
(DFtickName, 'a) proc"
primrec
"RepDF_to_DF (RDFtick) = ($DFtick)"
lemma RDFtick_DFtick_ref1_induct_lm:
"(($DFtick)::(DFtickName, 'a) proc)
<=F (NatDFtick n (($RDFtick)::(RDFtickName,'a)proc)) << RepDF_to_DF"
apply (induct_tac n)
apply (simp_all)
apply (rule cspF_Int_choice_right)
apply (rule cspF_rw_left)
apply (rule cspF_unwind)
apply (simp_all)
apply (simp add: CPOmode_or_CMSmode_or_MIXmode)
apply (simp)
done
lemma RDFtick_DFtick_ref1:
"$DFtick <=F $RDFtick"
apply (rule cspF_fp_induct_right[of _ _ "RepDF_to_DF"])
apply (simp)
apply (simp add: CPOmode_or_CMSmode_or_MIXmode)
apply (simp)
apply (induct_tac p)
apply (simp)
apply (rule cspF_rw_left)
apply (rule cspF_unwind)
apply (simp)
apply (simp add: CPOmode_or_CMSmode_or_MIXmode)
apply (simp)
apply (rule cspF_decompo)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_Rep_int_choice_right)
apply (simp add: RDFtick_DFtick_ref1_induct_lm)
apply (simp)
done
(*** ref2 ***)
consts
DF_to_RepDF :: "DFtickName =>
(RDFtickName, 'a) proc"
primrec
"DF_to_RepDF (DFtick) = ($RDFtick)"
lemma RDFtick_DFtick_ref2:
"$RDFtick <=F $DFtick"
apply (rule cspF_fp_induct_right[of _ _ "DF_to_RepDF"])
apply (simp)
apply (simp add: CPOmode_or_CMSmode_or_MIXmode)
apply (simp)
apply (induct_tac p)
apply (simp)
apply (rule cspF_rw_left)
apply (rule cspF_unwind)
apply (simp)
apply (simp add: CPOmode_or_CMSmode_or_MIXmode)
apply (simp)
apply (rule cspF_decompo)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_decompo)
apply (simp)
apply (rule cspF_Rep_int_choice_left)
apply (rule_tac x="0" in exI)
apply (simp)
apply (simp)
done
(**************************** =F****************************)
lemma RDFtick_DFtick:
"$RDFtick =F $DFtick"
apply (simp add: cspF_eq_ref_iff)
apply (simp add: RDFtick_DFtick_ref1)
apply (simp add: RDFtick_DFtick_ref2)
done
(* ---------------------------------------------------*
| |
| syntactical approach 2 <--> semantical approach |
| |
* ---------------------------------------------------*)
theorem DeadlockFree_RDFtick_ref:
"P isDeadlockFree = ($RDFtick <=F P)"
apply (simp add: DeadlockFree_DFtick_ref)
apply (rule)
apply (rule cspF_rw_left)
apply (rule RDFtick_DFtick)
apply (simp)
apply (rule cspF_rw_left)
apply (rule RDFtick_DFtick[THEN cspF_sym])
apply (simp)
done
(* ------------------------------------------------------------------ *)
declare csp_prefix_ss_def[simp del]
end
lemma guardedfun_DFtick:
guardedfun DFtickfun
lemma guardedfun_RDFtick:
guardedfun RDFtickfun
lemma DFtick_is_DeadlockFree:
($DFtick) isDeadlockFree
lemma DFtick_DeadlockFree:
$DFtick <=F P ==> P isDeadlockFree
lemma traces_included_in_DFtick:
t :t traces ((FIX DFtickfun) DFtick) (fstF o MF)
lemma failures_included_in_DFtick_lm:
X ≠ UNIV ∨ Tick ∈ sett t --> (t, X) :f failures ((FIX DFtickfun) DFtick) MF
lemma failures_included_in_DFtick:
X ≠ UNIV ∨ Tick ∈ sett t ==> (t, X) :f failures ((FIX DFtickfun) DFtick) MF
lemma DeadlockFree_DFtick:
P isDeadlockFree ==> $DFtick <=F P
theorem DeadlockFree_DFtick_ref:
P isDeadlockFree = ($DFtick <=F P)
lemma RDFtick_DFtick_ref1_induct_lm:
$DFtick <=F (NatDFtick n ($RDFtick)) << RepDF_to_DF
lemma RDFtick_DFtick_ref1:
$DFtick <=F $RDFtick
lemma RDFtick_DFtick_ref2:
$RDFtick <=F $DFtick
lemma RDFtick_DFtick:
$RDFtick =F $DFtick
theorem DeadlockFree_RDFtick_ref:
P isDeadlockFree = ($RDFtick <=F P)