(*-------------------------------------------*
| CSP-Prover on Isabelle2004 |
| December 2004 |
| |
| CSP-Prover on Isabelle2005 |
| October 2005 (modified) |
| |
| Yoshinao Isobe (AIST JAPAN) |
*-------------------------------------------*)
theory CPO = Infra:
(*****************************************************************
1. Complete partial order (cpo)
2. Continuity
3. Tarski Theorem
*****************************************************************)
consts
directed :: "'a::order set => bool"
defs
directed_def : "directed X == ((X ~= {}) &
(ALL x y. x : X & y : X -->
(EX z. z : X & x <= z & y <= z)))"
axclass bot0 < order
consts Bot :: "'a::bot0" (* Bottom *)
axclass
bot < bot0
bottom_bot : "Bot <= (x::'a::bot0)"
axclass
cpo < order
complete_cpo : "(directed (X::'a::order set)) ==> X hasLUB"
(*** pointed cpo ***)
axclass cpo_bot < cpo, bot
consts
continuous :: "('a::cpo => 'b::cpo) => bool"
admissible :: "('a::cpo => bool) => bool"
defs
continuous_def : "continuous f == ALL X.
directed X --> ((f ` X) hasLUB & LUB (f ` X) = f (LUB X))"
admissible_def : "admissible P == ALL X.
directed X --> (ALL x:X. P x) --> P (LUB X)"
(**********************************************************
small lemmas
**********************************************************)
lemma complete_cpo_lm:
"ALL (X::'a::cpo set). directed X --> X hasLUB"
by (simp add: complete_cpo)
(*** another definition of continuous ***)
lemma continuous_only_if: "continuous f ==>
directed X --> (EX x. ((f x) isLUB (f ` X) & x isLUB X))"
apply (intro allI impI)
apply (insert complete_cpo_lm)
apply (drule_tac x="X" in spec)
apply (simp)
apply (insert LUB_is[of X], simp)
apply (simp add: hasLUB_def)
apply (erule exE)
apply (rule_tac x="x" in exI)
apply (simp add: continuous_def)
apply (drule_tac x="X" in spec)
apply (simp)
apply (erule conjE)
apply (simp add: LUB_iff)
apply (insert LUB_unique[of "LUB X" X])
by (simp)
lemma continuous_if:
"ALL X. directed X --> (EX x. ((f x) isLUB (f ` X) & x isLUB X))
==> continuous f"
apply (simp add: continuous_def)
apply (intro allI impI)
apply (drule_tac x="X" in spec)
apply (simp)
apply (elim conjE exE)
apply (subgoal_tac "(f ` X) hasLUB", simp)
apply (simp add: LUB_iff)
apply (subgoal_tac "x = LUB X", simp)
apply (rule LUB_unique)
apply (simp)
apply (rule LUB_is)
apply (simp add: hasLUB_def)
apply (rule_tac x="x" in exI, simp)
apply (simp add: hasLUB_def)
apply (rule_tac x="f x" in exI, simp)
done
(*** iff ***)
lemma continuous_iff: "continuous f =
(ALL X. directed X --> (EX x. ((f x) isLUB (f ` X) & x isLUB X)))"
apply (rule iffI)
apply (simp add: continuous_only_if)
apply (simp add: continuous_if)
done
(**********************************************************
lemmas and theorems for Tarski
**********************************************************)
(* LUB is not affected by Bot *)
lemma LUB_with_Bot:
"((x::('a::cpo_bot)) isLUB {x. f x | x = Bot}) = (x isLUB {x. f x})"
apply (rule iffI)
apply (simp add: isLUB_def isUB_def)
apply (erule conjE)
apply (intro allI impI)
apply (rotate_tac 1)
apply (drule_tac x="y" in spec)
apply (rotate_tac -1)
apply (drule mp)
apply (intro allI)
apply (drule_tac x="ya" in spec)
apply (simp add: bottom_bot)
apply (assumption)
apply (simp add: isLUB_def isUB_def bottom_bot)
done
(************************************************************)
(* if x<=y then {x,y} is a directed set. *)
(* this is used in a proof for continuous_mono *)
lemma directed_x_y: "x <= y ==> directed {x, y}"
apply (simp add: directed_def)
apply (intro allI impI)
apply (rule_tac x="y" in exI)
by (auto)
(* the least upper bound of a set {x,y} *)
(* this is used in a proof for continuous_mono *)
lemma LUB_x_y: "[| x <= y ; z isLUB {x, y} |] ==> z = y"
apply (simp only: isUB_def isLUB_def)
apply (elim conjE)
apply (drule_tac x="y" in spec, simp)
apply (drule_tac x="y" in spec, simp)
done
(************************ continuity *****************************)
(* f is continuous --> f is monotonic *)
lemma continuous_mono: "continuous f ==> mono f"
apply (simp add: continuous_iff mono_def)
apply (intro allI impI)
apply (drule_tac x="{A,B}" in spec)
apply (simp add: directed_x_y)
apply (erule exE)
apply (erule conjE)
apply (subgoal_tac "x = B")
apply (simp add: isUB_def isLUB_def)
apply (simp add: LUB_x_y)
done
(* directed and functions *)
lemma directed_continuous:
"[| continuous f ; directed X |] ==> directed (f ` X)"
apply (insert continuous_mono[of f])
apply (simp add: continuous_iff directed_def)
apply (drule_tac x="X" in spec)
apply (simp)
apply (intro allI impI)
apply (simp add: in_image_set)
apply (elim conjE exE)
apply (drule_tac x="ya" in spec)
apply (drule_tac x="yb" in spec)
apply (simp)
apply (elim conjE exE)
apply (rule_tac x="f z" in exI)
apply (rule conjI)
apply (rule_tac x="z" in exI, simp)
by (simp add: mono_def)
(* composition of continuous functions *)
lemma compo_continuous:
"[| continuous f ; continuous g |] ==> continuous (g o f)"
apply (insert directed_continuous[of f])
apply (simp add: continuous_iff)
apply (intro allI impI)
apply (drule_tac x="X" in spec)
apply (drule_tac x="f ` X" in spec)
apply (simp)
apply (elim conjE exE)
apply (rule_tac x="x" in exI)
apply (simp add: image_compose)
apply (subgoal_tac "xa = f x", simp)
apply (simp add: LUB_unique)
done
(*********************** Tarski continuous ****************************)
lemma Tarski_directed_lm1:
"mono (f::('a::cpo_bot => 'a::cpo_bot)) ==> (f ^ n) Bot <= (f ^ (n+1)) Bot"
apply (induct_tac n)
apply (simp add: bottom_bot)
apply (simp add: mono_def)
done
lemma Tarski_directed_lm2:
"mono (f::('a::cpo_bot => 'a::cpo_bot)) ==> (f ^ n) Bot <= (f ^ (n+m)) Bot"
apply (induct_tac m)
apply (simp)
apply (insert Tarski_directed_lm1[of f])
apply (rule order_trans)
apply (simp)
apply (simp)
done
lemma Tarski_directed:
"mono (f::('a::cpo_bot => 'a::cpo_bot)) ==> directed {x. EX n. x = (f^n) Bot}"
apply (simp add: directed_def)
apply (rule conjI)
apply (rule_tac x="Bot" in exI)
apply (rule_tac x="0" in exI)
apply (simp)
apply (intro allI impI)
apply (elim conjE exE)
apply (rename_tac x y n m)
apply (case_tac "m <= n")
apply (rule_tac x="x" in exI)
apply (rule conjI)
apply (rule_tac x="n" in exI)
apply (assumption)
apply (simp)
apply (subgoal_tac "(f ^ m) Bot <= (f ^ (m + (n-m))) Bot", simp)
apply (rule Tarski_directed_lm2, simp)
apply (rule_tac x="y" in exI)
apply (rule conjI)
apply (rule_tac x="m" in exI)
apply (assumption)
(* ~ m <= n *)
apply (simp)
apply (subgoal_tac "(f ^ n) Bot <= (f ^ (n + (m-n))) Bot", simp)
apply (rule Tarski_directed_lm2, simp)
done
lemma Tarski_image_expand_lm:
"f ` {x. EX n. x = (f ^ n) Bot} = {x. EX n. x = f ((f ^ n) Bot)}"
apply (auto simp add: image_Collect)
done
lemma Tarski_by_continuity:
"continuous (f::('a::cpo_bot => 'a::cpo_bot)) ==>
(EX x. f x isLUB {x. EX n. x = f((f^n) Bot)} &
x isLUB {x. EX n. x = (f^n) Bot })"
apply (insert continuous_mono[of f])
apply (simp)
apply (simp add: continuous_iff)
apply (drule_tac x="{x. EX n. x = (f ^ n) Bot}" in spec)
apply (simp add: Tarski_directed)
apply (erule exE)
apply (rule_tac x="x" in exI)
apply (simp add: Tarski_image_expand_lm)
done
(******)
lemma Tarski_LUB_lm:
"(EX n. (x = ((f::('a::cpo_bot => 'a::cpo_bot)) ^ n) Bot) )
= ((EX n. x = (f ^ (Suc n)) Bot) | x = Bot)"
apply (rule iffI)
(* ==> *)
apply (erule exE)
apply (insert nat_zero_or_Suc)
apply (drule_tac x="n" in spec)
apply (erule disjE)
apply (simp)
apply (erule exE)
apply (rule disjI1)
apply (rule_tac x="m" in exI)
apply (simp)
(* <== *)
apply (erule disjE)
apply (erule exE)
apply (rule_tac x="Suc n" in exI)
apply (simp)
apply (rule_tac x="0" in exI)
apply (simp)
done
(******)
lemma Tarski_LUB:
"ALL (f::('a::cpo_bot => 'a::cpo_bot)) x.
(x::'a::cpo_bot) isLUB {x. EX n. x = f((f^n) Bot)} =
x isLUB {x. EX n. x = (f^n) Bot }"
apply (simp add: Tarski_LUB_lm LUB_with_Bot)
done
(******)
lemma Tarski_least_lm:
"[| mono (f::('a::cpo_bot => 'a::cpo_bot)) ; y = f y |]
==> (f^n) Bot <= y"
apply (induct_tac n)
apply (simp add: bottom_bot)
apply (simp add: mono_def)
apply (drule_tac x="(f ^ n) Bot" in spec)
apply (drule_tac x="y" in spec)
by (simp)
lemma Tarski_least:
"[| mono (f::('a::cpo_bot => 'a::cpo_bot)) ;
x isLUB {x. EX n. x = (f^n) Bot } ; y = f y |]
==> x <= y"
apply (simp add: isLUB_def)
apply (erule conjE)
apply (drule_tac x="y" in spec)
apply (drule mp)
apply (simp add: isUB_def)
apply (intro allI impI)
apply (erule exE)
apply (simp add: Tarski_least_lm)
by (assumption)
(*-------------------*
| Tarski |
*-------------------*)
theorem Tarski_thm:
"continuous (f::('a::cpo_bot => 'a::cpo_bot)) ==>
f hasLFP & LFP f isLUB {x. EX n. x = (f^n) Bot}"
apply (insert Tarski_by_continuity[of f])
apply (simp add: Tarski_LUB)
apply (erule exE)
apply (subgoal_tac "x isLFP f") (* ...1 *)
apply (simp add: isLFP_LFP hasLFP_def)
apply (rule_tac x="x" in exI, simp)
(* 1 *)
apply (simp add: isLFP_def)
apply (erule conjE)
apply (simp add: LUB_unique)
apply (intro allI impI)
apply (rule Tarski_least[of f])
apply (simp_all add: continuous_mono)
done
(*-------------------*
| Tarski LUB |
*-------------------*)
theorem Tarski_thm_LFP_LUB:
"continuous (f::('a::cpo_bot => 'a::cpo_bot)) ==>
LFP f = LUB {x. EX n. x = (f^n) Bot}"
apply (insert Tarski_thm[of f])
apply (auto simp add: isLUB_LUB)
done
(*--------------------*
| Tarski (existency) |
*--------------------*)
theorem Tarski_thm_EX:
"continuous (f::('a::cpo_bot => 'a::cpo_bot)) ==> f hasLFP"
by (simp add: Tarski_thm)
(*========================================================*
| Fixed Point Induction (pointed CPO) |
*========================================================*)
theorem cpo_fixpoint_induction:
"[| (R::'a::cpo_bot => bool) Bot ; continuous f ; admissible R ;
inductivefun R f |]
==> f hasLFP & R (LFP f)"
apply (insert Tarski_thm[of f], simp)
apply (simp add: admissible_def)
apply (drule_tac x="{x. EX n. x = (f^n) Bot }" in spec)
apply (simp add: Tarski_directed continuous_mono)
apply (auto simp add: inductivefun_all_n)
apply (simp add: isLUB_LUB)
done
(*----------------------------------------------------------*
| |
| Fixed point induction for refinement (CPO) |
| |
*----------------------------------------------------------*)
(************************************************************
admissibility lemma for refinement for cpo
************************************************************)
lemma admissible_Rev_fun: "admissible (Rev_fun X)"
apply (simp add: Rev_fun_def)
apply (simp add: admissible_def)
by (auto simp add: LUB_least complete_cpo)
(*** Bot ***)
lemma Rev_fun_Bot: "Rev_fun (X::'a::bot) Bot"
by (simp add: Rev_fun_def bottom_bot)
(************************************************************
Fixed Point Induction (CPO) for refinement
************************************************************)
theorem cpo_fixpoint_induction_rev:
"[| continuous f ; f X <= X |]
==> LFP f <= (X::'a::cpo_bot)"
apply (insert cpo_fixpoint_induction[of "(Rev_fun X)" f])
apply (simp add: admissible_Rev_fun Rev_fun_Bot)
apply (subgoal_tac "inductivefun (Rev_fun X) f")
apply (simp add: Rev_fun_def)
(* inductiveness *)
apply (simp add: inductivefun_def Rev_fun_def)
apply (intro allI impI)
apply (insert continuous_mono[of f])
apply (simp add: mono_def)
apply (drule_tac x="x" in spec)
apply (drule_tac x="X" in spec)
by (simp)
(*** EX version ***)
theorem cpo_fixpoint_induction_rev_EX:
"[| continuous f ; f X <= X ; Y isLFP f |]
==> Y <= (X::'a::cpo_bot)"
apply (insert cpo_fixpoint_induction_rev[of f X])
by (auto simp add: isLFP_LFP)
(*****************************************************************)
end
lemma complete_cpo_lm:
∀X. directed X --> X hasLUB
lemma continuous_only_if:
continuous f ==> directed X --> (∃x. f x isLUB f ` X ∧ x isLUB X)
lemma continuous_if:
∀X. directed X --> (∃x. f x isLUB f ` X ∧ x isLUB X) ==> continuous f
lemma continuous_iff:
continuous f = (∀X. directed X --> (∃x. f x isLUB f ` X ∧ x isLUB X))
lemma LUB_with_Bot:
x isLUB {x. f x ∨ x = Bot} = x isLUB {x. f x}
lemma directed_x_y:
x ≤ y ==> directed {x, y}
lemma LUB_x_y:
[| x ≤ y; z isLUB {x, y} |] ==> z = y
lemma continuous_mono:
continuous f ==> mono f
lemma directed_continuous:
[| continuous f; directed X |] ==> directed (f ` X)
lemma compo_continuous:
[| continuous f; continuous g |] ==> continuous (g o f)
lemma Tarski_directed_lm1:
mono f ==> (f ^ n) Bot ≤ (f ^ (n + 1)) Bot
lemma Tarski_directed_lm2:
mono f ==> (f ^ n) Bot ≤ (f ^ (n + m)) Bot
lemma Tarski_directed:
mono f ==> directed {x. ∃n. x = (f ^ n) Bot}
lemma Tarski_image_expand_lm:
f ` {x. ∃n. x = (f ^ n) Bot} = {x. ∃n. x = f ((f ^ n) Bot)}
lemma Tarski_by_continuity:
continuous f ==> ∃x. f x isLUB {x. ∃n. x = f ((f ^ n) Bot)} ∧ x isLUB {x. ∃n. x = (f ^ n) Bot}
lemma Tarski_LUB_lm:
(∃n. x = (f ^ n) Bot) = ((∃n. x = (f ^ Suc n) Bot) ∨ x = Bot)
lemma Tarski_LUB:
∀f x. x isLUB {x. ∃n. x = f ((f ^ n) Bot)} = x isLUB {x. ∃n. x = (f ^ n) Bot}
lemma Tarski_least_lm:
[| mono f; y = f y |] ==> (f ^ n) Bot ≤ y
lemma Tarski_least:
[| mono f; x isLUB {x. ∃n. x = (f ^ n) Bot}; y = f y |] ==> x ≤ y
theorem Tarski_thm:
continuous f ==> f hasLFP ∧ LFP f isLUB {x. ∃n. x = (f ^ n) Bot}
theorem Tarski_thm_LFP_LUB:
continuous f ==> LFP f = LUB {x. ∃n. x = (f ^ n) Bot}
theorem Tarski_thm_EX:
continuous f ==> f hasLFP
theorem cpo_fixpoint_induction:
[| R Bot; continuous f; admissible R; inductivefun R f |] ==> f hasLFP ∧ R (LFP f)
lemma admissible_Rev_fun:
admissible (Rev_fun X)
lemma Rev_fun_Bot:
Rev_fun X Bot
theorem cpo_fixpoint_induction_rev:
[| continuous f; f X ≤ X |] ==> LFP f ≤ X
theorem cpo_fixpoint_induction_rev_EX:
[| continuous f; f X ≤ X; Y isLFP f |] ==> Y ≤ X