Theory Infra_order

Up to index of Isabelle/HOL/HOL-Complex/CSP

theory Infra_order
imports Infra_common
begin

           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2004         |
            |               November 2004               |
            |                   June 2005  (modified)   |
            |                   July 2005  (modified)   |
            |                                           |
            |        CSP-Prover on Isabelle2005         |
            |                October 2005  (modified)   |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory Infra_order
imports Infra_common
begin

(*****************************************************
                    order
 *****************************************************)

lemma order_antisymE:
  "[| (a::'a::order) = b ; [| a <= b ; b <= a |] ==> P |] ==> P"
apply (simp)
done

(*****************************************************
            Upper Bound and Lower Bound
 *****************************************************)

consts
  isUB  :: "'a::order => 'a::order set => bool"  ("_ isUB _" [55,55] 55)
  isLUB :: "'a::order => 'a::order set => bool"  ("_ isLUB _"[55,55] 55)
  isLB  :: "'a::order => 'a::order set => bool"  ("_ isLB _" [55,55] 55)
  isGLB :: "'a::order => 'a::order set => bool"  ("_ isGLB _"[55,55] 55)

defs
  isUB_def  : "x isUB X  == ALL y. y:X --> y <= x"
  isLUB_def : "x isLUB X == (x isUB X) & (ALL y. y isUB X --> x <= y)"
  isLB_def  : "x isLB X  == ALL y. y:X --> x <= y"
  isGLB_def : "x isGLB X == (x isLB X) & (ALL y. y isLB X --> y <= x)"

consts
  hasLUB :: "'a::order set => bool" ("_ hasLUB" [1000] 55) 
  hasGLB :: "'a::order set => bool" ("_ hasGLB" [1000] 55) 

defs
  hasLUB_def: "X hasLUB == (EX x. x isLUB X)"
  hasGLB_def: "X hasGLB == (EX x. x isGLB X)"

consts
  LUB    :: "'a::order set => 'a::order"
  GLB    :: "'a::order set => 'a::order"

defs
  LUB_def    : "LUB X == if (X hasLUB) then THE x. (x isLUB X) else the None"
  GLB_def    : "GLB X == if (X hasGLB) then THE x. (x isGLB X) else the None"

(*** LUB is unique ***)

lemma LUB_unique : "[| x isLUB X ; y isLUB X |] ==> x = y"
apply (unfold isLUB_def)
apply (elim conjE)
apply (drule_tac x="y" in spec)
apply (drule_tac x="x" in spec)
by (simp)

(*** GLB is unique ***)

lemma GLB_unique : "[| x isGLB X ; y isGLB X |] ==> x = y"
apply (unfold isGLB_def)
apply (elim conjE)
apply (drule_tac x="y" in spec)
apply (drule_tac x="x" in spec)
by (simp)

(*-----------------------*
 |       the LUB         |
 *-----------------------*)

lemma isLUB_to_LUB : "X hasLUB ==> x isLUB X = (x = LUB X)"
apply (simp add: LUB_def)
apply (rule iffI)

apply (rule sym)
apply (rule the_equality)
apply (simp)
apply (simp add: LUB_unique)

apply (simp add: hasLUB_def)
apply (erule exE)
apply (rule theI[of "(%x. x isLUB X)"])
apply (simp)
apply (simp add: LUB_unique)
done

lemmas LUB_to_isLUB = isLUB_to_LUB[THEN sym]

lemma LUB_to_isLUB_sym :
    "X hasLUB ==> (LUB X = x) = x isLUB X"
by (auto simp add: isLUB_to_LUB)

lemmas LUB_iff = LUB_to_isLUB LUB_to_isLUB_sym

lemma LUB_is: "X hasLUB ==> (LUB X) isLUB X"
apply (insert LUB_to_isLUB[of X "LUB X"])
by (simp)

lemma isLUB_LUB : "x isLUB X ==> (LUB X = x)"
apply (subgoal_tac "X hasLUB")
apply (simp add: LUB_iff)
apply (simp add: hasLUB_def)
apply (rule_tac x="x" in exI, simp)
done

(*-----------------------*
 |       the GLB         |
 *-----------------------*)

lemma isGLB_to_GLB : "X hasGLB ==> x isGLB X = (x = GLB X)"
apply (simp add: GLB_def)
apply (rule iffI)

apply (rule sym)
apply (rule the_equality)
apply (simp)
apply (simp add: GLB_unique)

apply (simp add: hasGLB_def)
apply (erule exE)
apply (rule theI[of "(%x. x isGLB X)"])
apply (simp)
apply (simp add: GLB_unique)
done

lemmas GLB_to_isGLB = isGLB_to_GLB[THEN sym]

lemma GLB_to_isGLB_sym :
    "X hasGLB ==> (GLB X = x) = x isGLB X"
by (auto simp add: isGLB_to_GLB)

lemmas GLB_iff = GLB_to_isGLB GLB_to_isGLB_sym

lemma GLB_is: "X hasGLB ==> (GLB X) isGLB X"
apply (insert GLB_to_isGLB[of X "GLB X"])
by (simp)

lemma isGLB_GLB : "x isGLB X ==> (GLB X = x)"
apply (subgoal_tac "X hasGLB")
apply (simp add: GLB_iff)
apply (simp add: hasGLB_def)
apply (rule_tac x="x" in exI, simp)
done

(*-----------------------*
 |     LUB subset        |
 *-----------------------*)

lemma isLUB_subset : "[| x isLUB X ; y isLUB Y ; X <= Y |] ==> x <= y"
apply (simp add: isLUB_def)
apply (elim conjE)

apply (drule_tac x="y" in spec)
apply (rotate_tac -1)
apply (drule mp)

apply (simp add: isUB_def)
apply (intro allI impI)
apply (rotate_tac 2)
apply (drule_tac x="ya" in spec)
apply (force)
by (simp)

(*-----------------------*
 |     GLB subset        |
 *-----------------------*)

lemma isGLB_subset : "[| x isGLB X ; y isGLB Y ; X <= Y |] ==> y <= x"
apply (simp add: isGLB_def)
apply (elim conjE)

apply (drule_tac x="y" in spec)
apply (rotate_tac -1)
apply (drule mp)

apply (simp add: isLB_def)
apply (intro allI impI)
apply (rotate_tac 2)
apply (drule_tac x="ya" in spec)
apply (force)
by (simp)

(*--------------------------*
 |  GLB exists for nat set  |
 *--------------------------*)

lemma EX_GLB_nat_lm: 
  "ALL m m'. m' <= m & m' : (X::nat set) --> (EX n. n isGLB X & n:X)"
apply (rule allI)
apply (induct_tac m)

(* base *)
apply (intro allI impI)
apply (rule_tac x="0" in exI)
apply (erule conjE)
apply (simp add: isGLB_def isLB_def)
apply (intro allI impI)
apply (drule_tac x="0" in spec)
apply (simp)

(* step *)
apply (intro allI impI)
apply (case_tac "EX m''. m'' <= n & m'':X")
apply (erule exE)
apply (drule_tac x="m''" in spec)
apply (simp)

apply (rule_tac x="m'" in exI)
apply (simp add: isGLB_def isLB_def)
apply (intro allI impI)

apply (case_tac "y < m'")
apply (drule_tac x="y" in spec)
by (auto)

(*** EX ***)

lemma EX_GLB_nat: 
  "(X::nat set) ~= {} ==> (EX n. n isGLB X & n:X)"
apply (subgoal_tac "EX m. m:X")
apply (erule exE)
apply (insert EX_GLB_nat_lm[of X])
apply (drule_tac x="m" in spec)
apply (drule_tac x="m" in spec)
apply (simp)
by (auto)

(*--------------------------*
 |       LUB is least       |
 *--------------------------*)

lemma LUB_least: "[| ALL x:X. x <= Y ; X hasLUB |]==> LUB X <= Y"
apply (insert LUB_is[of X])
apply (simp add: isLUB_def)
apply (elim conjE)
apply (drule_tac x="Y" in spec)
apply (simp add: isUB_def)
done

(*--------------------------*
 |       GLB is great       |
 *--------------------------*)

lemma GLB_great: "[| ALL x:X. Y <= x ; X hasGLB |]==> Y <= GLB X"
apply (insert GLB_is[of X])
apply (simp add: isGLB_def)
apply (elim conjE)
apply (drule_tac x="Y" in spec)
apply (simp add: isLB_def)
done

(*--------------------------*
 |       Union isLUB        |
 *--------------------------*)

(* Union X is an upper bound of X *)

lemma Union_isUB : "(Union X) isUB X"
apply (simp add: isUB_def)
apply (simp add: subset_iff)
apply (intro allI impI)
apply (rule_tac x=y in bexI)
by (auto)

(* UnionT Ts is the least upper bound of Ts *)

lemma Union_isLUB : "Union X isLUB X"
apply (simp add: isLUB_def Union_isUB)
apply (simp add: isUB_def)
apply (simp add: subset_iff)
apply (intro allI impI)
apply (erule bexE)
apply (drule_tac x="Xa" in spec)
by (simp)

(* the least upper bound of X is Union X *)

lemma isLUB_Union_only_if: "x isLUB X ==> x = Union X"
apply (insert Union_isLUB[of X])
apply (rule LUB_unique)
by (simp_all)

(* iff *)

lemma isLUB_Union : "(x isLUB X) = (x = Union X)"
apply (rule iffI)
apply (simp add: isLUB_Union_only_if)
apply (simp add: Union_isLUB)
done

(* LUB is Union X *)

lemma LUB_Union : "LUB X = Union X"
by (simp add: isLUB_LUB Union_isLUB)

(*****************************************************
                   MIN and MAX
 *****************************************************)

consts
  isMAX :: "'a::order => 'a::order set => bool"  ("_ isMAX _"[55,55] 55)
  isMIN :: "'a::order => 'a::order set => bool"  ("_ isMIN _"[55,55] 55)

defs
  isMAX_def : "x isMAX X == (x isUB X) & (x : X)"
  isMIN_def : "x isMIN X == (x isLB X) & (x : X)"

consts
  hasMAX :: "'a::order set => bool" ("_ hasMAX" [1000] 55) 
  hasMIN :: "'a::order set => bool" ("_ hasMIN" [1000] 55) 

defs
  hasMAX_def: "X hasMAX == (EX x. x isMAX X)"
  hasMIN_def: "X hasMIN == (EX x. x isMIN X)"

consts
  MAX    :: "'a::order set => 'a::order"
  MIN    :: "'a::order set => 'a::order"

defs
  MAX_def    : "MAX X == if (X hasMAX) then THE x. (x isMAX X) else the None"
  MIN_def    : "MIN X == if (X hasMIN) then THE x. (x isMIN X) else the None"

(*** MAX is unique ***)

lemma MAX_unique : "[| x isMAX X ; y isMAX X |] ==> x = y"
apply (unfold isMAX_def isUB_def)
apply (elim conjE)
apply (drule_tac x="y" in spec)
apply (drule_tac x="x" in spec)
by (simp)

(*** MIN is unique ***)

lemma MIN_unique : "[| x isMIN X ; y isMIN X |] ==> x = y"
apply (unfold isMIN_def isLB_def)
apply (elim conjE)
apply (drule_tac x="y" in spec)
apply (drule_tac x="x" in spec)
by (simp)

(*-----------------------*
 |       the MAX         |
 *-----------------------*)

lemma isMAX_to_MAX : "X hasMAX ==> x isMAX X = (x = MAX X)"
apply (simp add: MAX_def)
apply (rule iffI)

apply (rule sym)
apply (rule the_equality)
apply (simp)
apply (simp add: MAX_unique)

apply (simp add: hasMAX_def)
apply (erule exE)
apply (rule theI[of "(%x. x isMAX X)"])
apply (simp)
apply (simp add: MAX_unique)
done

lemmas MAX_to_isMAX = isMAX_to_MAX[THEN sym]

lemma MAX_to_isMAX_sym :
    "X hasMAX ==> (MAX X = x) = x isMAX X"
by (auto simp add: isMAX_to_MAX)

lemmas MAX_iff = MAX_to_isMAX MAX_to_isMAX_sym

(*-----------------------*
 |       the MIN         |
 *-----------------------*)

lemma isMIN_to_MIN : "X hasMIN ==> x isMIN X = (x = MIN X)"
apply (simp add: MIN_def)
apply (rule iffI)

apply (rule sym)
apply (rule the_equality)
apply (simp)
apply (simp add: MIN_unique)

apply (simp add: hasMIN_def)
apply (erule exE)
apply (rule theI[of "(%x. x isMIN X)"])
apply (simp)
apply (simp add: MIN_unique)
done

lemmas MIN_to_isMIN = isMIN_to_MIN[THEN sym]

lemma MIN_to_isMIN_sym :
    "X hasMIN ==> (MIN X = x) = x isMIN X"
by (auto simp add: isMIN_to_MIN)

lemmas MIN_iff = MIN_to_isMIN MIN_to_isMIN_sym

(*-----------------------*
 |     MAX subset        |
 *-----------------------*)

lemma isMAX_subset : "[| x isMAX X ; y isMAX Y ; X <= Y |] ==> x <= y"
apply (simp add: isMAX_def isUB_def)
apply (elim conjE)

apply (rotate_tac 3)
apply (drule_tac x="x" in spec)
by (force)

(*-----------------------*
 |     MIN subset        |
 *-----------------------*)

lemma isMIN_subset : "[| x isMIN X ; y isMIN Y ; X <= Y |] ==> y <= x"
apply (simp add: isMIN_def isLB_def)
apply (elim conjE)

apply (rotate_tac 3)
apply (drule_tac x="x" in spec)
by (force)

(*--------------------------*
 |  MIN exists for nat set  |
 *--------------------------*)

lemma EX_MIN_nat_lm: 
  "ALL m m'. m' <= m & m' : (X::nat set) --> (EX n. n isMIN X)"
apply (rule allI)
apply (induct_tac m)

(* base *)
apply (intro allI impI)
apply (rule_tac x="0" in exI)
apply (erule conjE)
apply (simp add: isMIN_def isLB_def)

(* step *)
apply (intro allI impI)
apply (case_tac "EX m''. m'' <= n & m'':X")
apply (erule exE)
apply (drule_tac x="m''" in spec)
apply (simp)

apply (rule_tac x="m'" in exI)
apply (simp add: isMIN_def isLB_def)
apply (intro allI impI)

apply (case_tac "y < m'")
apply (drule_tac x="y" in spec)
by (auto)

(*** EX ***)

lemma EX_MIN_nat: 
  "(X::nat set) ~= {} ==> EX n. n isMIN X"
apply (subgoal_tac "EX m. m:X")
apply (erule exE)
apply (insert EX_MIN_nat_lm[of X])
apply (drule_tac x="m" in spec)
apply (drule_tac x="m" in spec)
apply (simp)
by (auto)

(*****************************************************
                   Fixed Point
 *****************************************************)

consts
 isUFP :: "'a        => ('a       => 'a        ) => bool" (infixl "isUFP" 55) 
 isLFP :: "'a::order => ('a::order => 'a::order) => bool" (infixl "isLFP" 55)
 isGFP :: "'a::order => ('a::order => 'a::order) => bool" (infixl "isGFP" 55)

defs
  isUFP_def : "x isUFP f == (x = f x & (ALL y. y = f y --> x  = y))"
  isLFP_def : "x isLFP f == (x = f x & (ALL y. y = f y --> x <= y))"
  isGFP_def : "x isGFP f == (x = f x & (ALL y. y = f y --> y <= x))"

consts
  hasUFP:: "('a        => 'a       ) => bool" ("_ hasUFP" [1000] 55) 
  hasLFP:: "('a::order => 'a::order) => bool" ("_ hasLFP" [1000] 55) 
  hasGFP:: "('a::order => 'a::order) => bool" ("_ hasGFP" [1000] 55) 

defs
  hasUFP_def: "f hasUFP == (EX x. x isUFP f)"
  hasLFP_def: "f hasLFP == (EX x. x isLFP f)"
  hasGFP_def: "f hasGFP == (EX x. x isGFP f)"

consts
  UFP    :: "('a        => 'a       ) => 'a"
  LFP    :: "('a::order => 'a::order) => 'a::order"
  GFP    :: "('a::order => 'a::order) => 'a::order"

defs
  UFP_def : "UFP f == if (f hasUFP) then (THE x. x isUFP f) else the None"
  LFP_def : "LFP f == if (f hasLFP) then (THE x. x isLFP f) else the None"
  GFP_def : "GFP f == if (f hasGFP) then (THE x. x isGFP f) else the None"

(*******************************
            lemmas 
 *******************************)

(*** UFP is unique ***)

lemma UFP_unique : "[| x isUFP f ; y isUFP f |] ==> x = y"
by (simp add: isUFP_def)

(*** LFP is unique ***)

lemma LFP_unique : "[| x isLFP f ; y isLFP f |] ==> x = y"
apply (unfold isLFP_def)
apply (erule conjE)+
apply (drule_tac x="y" in spec)
apply (drule_tac x="x" in spec)
by (simp)

(*** GFP is unique ***)

lemma GFP_unique : "[| x isGFP f ; y isGFP f |] ==> x = y"
apply (unfold isGFP_def)
apply (erule conjE)+
apply (drule_tac x="y" in spec)
apply (drule_tac x="x" in spec)
by (simp)

(*-----------------------*
 |       the UFP         |
 *-----------------------*)

lemma isUFP_to_UFP : "f hasUFP ==> x isUFP f = (x = UFP f)"
apply (simp add: UFP_def)
apply (rule iffI)

apply (rule sym)
apply (rule the_equality)
apply (simp)
apply (simp add: UFP_unique)

apply (simp add: hasUFP_def)
apply (erule exE)
apply (rule theI[of "(%x. x isUFP f)"])
apply (simp)
apply (simp add: UFP_unique)
done

lemmas UFP_to_isUFP = isUFP_to_UFP[THEN sym]

lemma UFP_to_isUFP_sym :
    "f hasUFP ==> (UFP f = x) = x isUFP f"
by (auto simp add: isUFP_to_UFP)

lemmas UFP_iff = UFP_to_isUFP UFP_to_isUFP_sym

(*** UFP is ***)

lemma UFP_is : "f hasUFP ==> (UFP f) isUFP f"
by (simp add: isUFP_to_UFP)

lemma isUFP_UFP : "x isUFP f ==> (UFP f = x)"
apply (subgoal_tac "f hasUFP")
apply (simp add: UFP_iff)
apply (simp add: hasUFP_def)
apply (rule_tac x="x" in exI, simp)
done

(*** UFP is fixed point ***)

lemma UFP_fp_lm : "[| f hasUFP ; x = UFP f |] ==> f x = x"
apply (simp add: UFP_iff)
apply (simp add: isUFP_def)
done

lemma UFP_fp : "f hasUFP ==> f (UFP f) = UFP f"
by (simp add: UFP_fp_lm)

(*** unique solution ***)

lemma hasUFP_unique_solution : 
  "[| f hasUFP ; f x = x ; f y = y |] ==> x = y"
apply (simp add: hasUFP_def)
apply (erule exE)
apply (simp add: isUFP_def)
apply (erule conjE)
apply (frule_tac x="x" in spec)
apply (drule_tac x="y" in spec)
apply (simp)
done

(*-----------------------*
 |       the LFP         |
 *-----------------------*)

lemma isLFP_to_LFP : "f hasLFP ==> x isLFP f = (x = LFP f)"
apply (simp add: LFP_def)
apply (rule iffI)

apply (rule sym)
apply (rule the_equality)
apply (simp)
apply (simp add: LFP_unique)

apply (simp add: hasLFP_def)
apply (erule exE)
apply (rule theI[of "(%x. x isLFP f)"])
apply (simp)
apply (simp add: LFP_unique)
done

lemmas LFP_to_isLFP = isLFP_to_LFP[THEN sym]

lemma LFP_to_isLFP_sym :
    "f hasLFP ==> (LFP f = x) = x isLFP f"
by (auto simp add: isLFP_to_LFP)

lemmas LFP_iff = LFP_to_isLFP LFP_to_isLFP_sym

(*** LFP is ***)

lemma LFP_is : "f hasLFP ==> (LFP f) isLFP f"
by (simp add: isLFP_to_LFP)

lemma isLFP_LFP : "x isLFP f ==> (LFP f = x)"
apply (subgoal_tac "f hasLFP")
apply (simp add: LFP_iff)
apply (simp add: hasLFP_def)
apply (rule_tac x="x" in exI, simp)
done

(*** LFP is fixed point ***)

lemma LFP_fp_lm : "[| f hasLFP ; x = LFP f |] ==> f x = x"
apply (simp add: LFP_iff)
apply (simp add: isLFP_def)
done

lemma LFP_fp : "f hasLFP ==> f (LFP f) = LFP f"
by (simp add: LFP_fp_lm)

(*** LFP is least ***)

lemma LFP_least : "[| f hasLFP ; f x = x |] ==> LFP f <= x"
apply (insert LFP_is[of f])
apply (simp add: isLFP_def)
done

(*-----------------------*
 |       the GFP         |
 *-----------------------*)

lemma isGFP_to_GFP : "f hasGFP ==> x isGFP f = (x = GFP f)"
apply (simp add: GFP_def)
apply (rule iffI)

apply (rule sym)
apply (rule the_equality)
apply (simp)
apply (simp add: GFP_unique)

apply (simp add: hasGFP_def)
apply (erule exE)
apply (rule theI[of "(%x. x isGFP f)"])
apply (simp)
apply (simp add: GFP_unique)
done

lemmas GFP_to_isGFP = isGFP_to_GFP[THEN sym]

lemma GFP_to_isGFP_sym :
    "f hasGFP ==> (GFP f = x) = x isGFP f"
by (auto simp add: isGFP_to_GFP)

lemmas GFP_iff = GFP_to_isGFP GFP_to_isGFP_sym

(*** GFP is ***)

lemma GFP_is : "f hasGFP ==> (GFP f) isGFP f"
by (simp add: isGFP_to_GFP)

lemma isGFP_GFP : "x isGFP f ==> (GFP f = x)"
apply (subgoal_tac "f hasGFP")
apply (simp add: GFP_iff)
apply (simp add: hasGFP_def)
apply (rule_tac x="x" in exI, simp)
done

(*** GFP is fixed point ***)

lemma GFP_fp_lm : "[| f hasGFP ; x = GFP f |] ==> f x = x"
apply (simp add: GFP_iff)
apply (simp add: isGFP_def)
done

lemma GFP_fp : "f hasGFP ==> f (GFP f) = GFP f"
by (simp add: GFP_fp_lm)

(*** GFP is greatest ***)

lemma GFP_greatest : "[| f hasGFP ; f x = x |] ==> x <= GFP f"
apply (insert GFP_is[of f])
apply (simp add: isGFP_def)
done

(*-----------------------*
 |     UFP --> LFP       |
 *-----------------------*)

lemma hasUFP_hasLFP: "f hasUFP ==> f hasLFP"
apply (simp add: hasUFP_def hasLFP_def)
apply (simp add: isUFP_def isLFP_def)
by (auto)

lemma hasUFP_LFP_UFP: "f hasUFP ==> LFP f = UFP f"
apply (simp add: isUFP_to_UFP[THEN sym])
apply (insert LFP_is[of f])
apply (simp add: hasUFP_hasLFP)
apply (simp add: hasUFP_def)
apply (simp add: isUFP_def isLFP_def)
apply (intro allI impI)
apply (elim conjE exE)
apply (rotate_tac -1)
apply (frule_tac x="y" in spec)
apply (drule_tac x="LFP f" in spec)
by (simp)

(*-----------------------*
 |     UFP --> GFP       |
 *-----------------------*)

lemma hasUFP_hasGFP: "f hasUFP ==> f hasGFP"
apply (simp add: hasUFP_def hasGFP_def)
apply (simp add: isUFP_def isGFP_def)
by (auto)

lemma hasUFP_GFP_UFP: "f hasUFP ==> GFP f = UFP f"
apply (simp add: isUFP_to_UFP[THEN sym])
apply (insert GFP_is[of f])
apply (simp add: hasUFP_hasGFP)
apply (simp add: hasUFP_def)
apply (simp add: isUFP_def isGFP_def)
apply (intro allI impI)
apply (elim conjE exE)
apply (rotate_tac -1)
apply (frule_tac x="y" in spec)
apply (drule_tac x="GFP f" in spec)
by (simp)

end

lemma order_antisymE:

  [| a = b; [| ab; ba |] ==> P |] ==> P

lemma LUB_unique:

  [| x isLUB X; y isLUB X |] ==> x = y

lemma GLB_unique:

  [| x isGLB X; y isGLB X |] ==> x = y

lemma isLUB_to_LUB:

  X hasLUB ==> x isLUB X = (x = LUB X)

lemmas LUB_to_isLUB:

  X1 hasLUB ==> (x1 = LUB X1) = x1 isLUB X1

lemmas LUB_to_isLUB:

  X1 hasLUB ==> (x1 = LUB X1) = x1 isLUB X1

lemma LUB_to_isLUB_sym:

  X hasLUB ==> (LUB X = x) = x isLUB X

lemmas LUB_iff:

  X1 hasLUB ==> (x1 = LUB X1) = x1 isLUB X1
  X hasLUB ==> (LUB X = x) = x isLUB X

lemmas LUB_iff:

  X1 hasLUB ==> (x1 = LUB X1) = x1 isLUB X1
  X hasLUB ==> (LUB X = x) = x isLUB X

lemma LUB_is:

  X hasLUB ==> LUB X isLUB X

lemma isLUB_LUB:

  x isLUB X ==> LUB X = x

lemma isGLB_to_GLB:

  X hasGLB ==> x isGLB X = (x = GLB X)

lemmas GLB_to_isGLB:

  X1 hasGLB ==> (x1 = GLB X1) = x1 isGLB X1

lemmas GLB_to_isGLB:

  X1 hasGLB ==> (x1 = GLB X1) = x1 isGLB X1

lemma GLB_to_isGLB_sym:

  X hasGLB ==> (GLB X = x) = x isGLB X

lemmas GLB_iff:

  X1 hasGLB ==> (x1 = GLB X1) = x1 isGLB X1
  X hasGLB ==> (GLB X = x) = x isGLB X

lemmas GLB_iff:

  X1 hasGLB ==> (x1 = GLB X1) = x1 isGLB X1
  X hasGLB ==> (GLB X = x) = x isGLB X

lemma GLB_is:

  X hasGLB ==> GLB X isGLB X

lemma isGLB_GLB:

  x isGLB X ==> GLB X = x

lemma isLUB_subset:

  [| x isLUB X; y isLUB Y; XY |] ==> xy

lemma isGLB_subset:

  [| x isGLB X; y isGLB Y; XY |] ==> yx

lemma EX_GLB_nat_lm:

m m'. m'mm'X --> (∃n. n isGLB XnX)

lemma EX_GLB_nat:

  X ≠ {} ==> ∃n. n isGLB XnX

lemma LUB_least:

  [| ∀xX. xY; X hasLUB |] ==> LUB XY

lemma GLB_great:

  [| ∀xX. Yx; X hasGLB |] ==> Y ≤ GLB X

lemma Union_isUB:

  Union X isUB X

lemma Union_isLUB:

  Union X isLUB X

lemma isLUB_Union_only_if:

  x isLUB X ==> x = Union X

lemma isLUB_Union:

  x isLUB X = (x = Union X)

lemma LUB_Union:

  LUB X = Union X

lemma MAX_unique:

  [| x isMAX X; y isMAX X |] ==> x = y

lemma MIN_unique:

  [| x isMIN X; y isMIN X |] ==> x = y

lemma isMAX_to_MAX:

  X hasMAX ==> x isMAX X = (x = MAX X)

lemmas MAX_to_isMAX:

  X1 hasMAX ==> (x1 = MAX X1) = x1 isMAX X1

lemmas MAX_to_isMAX:

  X1 hasMAX ==> (x1 = MAX X1) = x1 isMAX X1

lemma MAX_to_isMAX_sym:

  X hasMAX ==> (MAX X = x) = x isMAX X

lemmas MAX_iff:

  X1 hasMAX ==> (x1 = MAX X1) = x1 isMAX X1
  X hasMAX ==> (MAX X = x) = x isMAX X

lemmas MAX_iff:

  X1 hasMAX ==> (x1 = MAX X1) = x1 isMAX X1
  X hasMAX ==> (MAX X = x) = x isMAX X

lemma isMIN_to_MIN:

  X hasMIN ==> x isMIN X = (x = MIN X)

lemmas MIN_to_isMIN:

  X1 hasMIN ==> (x1 = MIN X1) = x1 isMIN X1

lemmas MIN_to_isMIN:

  X1 hasMIN ==> (x1 = MIN X1) = x1 isMIN X1

lemma MIN_to_isMIN_sym:

  X hasMIN ==> (MIN X = x) = x isMIN X

lemmas MIN_iff:

  X1 hasMIN ==> (x1 = MIN X1) = x1 isMIN X1
  X hasMIN ==> (MIN X = x) = x isMIN X

lemmas MIN_iff:

  X1 hasMIN ==> (x1 = MIN X1) = x1 isMIN X1
  X hasMIN ==> (MIN X = x) = x isMIN X

lemma isMAX_subset:

  [| x isMAX X; y isMAX Y; XY |] ==> xy

lemma isMIN_subset:

  [| x isMIN X; y isMIN Y; XY |] ==> yx

lemma EX_MIN_nat_lm:

m m'. m'mm'X --> (∃n. n isMIN X)

lemma EX_MIN_nat:

  X ≠ {} ==> ∃n. n isMIN X

lemma UFP_unique:

  [| x isUFP f; y isUFP f |] ==> x = y

lemma LFP_unique:

  [| x isLFP f; y isLFP f |] ==> x = y

lemma GFP_unique:

  [| x isGFP f; y isGFP f |] ==> x = y

lemma isUFP_to_UFP:

  f hasUFP ==> x isUFP f = (x = UFP f)

lemmas UFP_to_isUFP:

  f1 hasUFP ==> (x1 = UFP f1) = x1 isUFP f1

lemmas UFP_to_isUFP:

  f1 hasUFP ==> (x1 = UFP f1) = x1 isUFP f1

lemma UFP_to_isUFP_sym:

  f hasUFP ==> (UFP f = x) = x isUFP f

lemmas UFP_iff:

  f1 hasUFP ==> (x1 = UFP f1) = x1 isUFP f1
  f hasUFP ==> (UFP f = x) = x isUFP f

lemmas UFP_iff:

  f1 hasUFP ==> (x1 = UFP f1) = x1 isUFP f1
  f hasUFP ==> (UFP f = x) = x isUFP f

lemma UFP_is:

  f hasUFP ==> UFP f isUFP f

lemma isUFP_UFP:

  x isUFP f ==> UFP f = x

lemma UFP_fp_lm:

  [| f hasUFP; x = UFP f |] ==> f x = x

lemma UFP_fp:

  f hasUFP ==> f (UFP f) = UFP f

lemma hasUFP_unique_solution:

  [| f hasUFP; f x = x; f y = y |] ==> x = y

lemma isLFP_to_LFP:

  f hasLFP ==> x isLFP f = (x = LFP f)

lemmas LFP_to_isLFP:

  f1 hasLFP ==> (x1 = LFP f1) = x1 isLFP f1

lemmas LFP_to_isLFP:

  f1 hasLFP ==> (x1 = LFP f1) = x1 isLFP f1

lemma LFP_to_isLFP_sym:

  f hasLFP ==> (LFP f = x) = x isLFP f

lemmas LFP_iff:

  f1 hasLFP ==> (x1 = LFP f1) = x1 isLFP f1
  f hasLFP ==> (LFP f = x) = x isLFP f

lemmas LFP_iff:

  f1 hasLFP ==> (x1 = LFP f1) = x1 isLFP f1
  f hasLFP ==> (LFP f = x) = x isLFP f

lemma LFP_is:

  f hasLFP ==> LFP f isLFP f

lemma isLFP_LFP:

  x isLFP f ==> LFP f = x

lemma LFP_fp_lm:

  [| f hasLFP; x = LFP f |] ==> f x = x

lemma LFP_fp:

  f hasLFP ==> f (LFP f) = LFP f

lemma LFP_least:

  [| f hasLFP; f x = x |] ==> LFP fx

lemma isGFP_to_GFP:

  f hasGFP ==> x isGFP f = (x = GFP f)

lemmas GFP_to_isGFP:

  f1 hasGFP ==> (x1 = GFP f1) = x1 isGFP f1

lemmas GFP_to_isGFP:

  f1 hasGFP ==> (x1 = GFP f1) = x1 isGFP f1

lemma GFP_to_isGFP_sym:

  f hasGFP ==> (GFP f = x) = x isGFP f

lemmas GFP_iff:

  f1 hasGFP ==> (x1 = GFP f1) = x1 isGFP f1
  f hasGFP ==> (GFP f = x) = x isGFP f

lemmas GFP_iff:

  f1 hasGFP ==> (x1 = GFP f1) = x1 isGFP f1
  f hasGFP ==> (GFP f = x) = x isGFP f

lemma GFP_is:

  f hasGFP ==> GFP f isGFP f

lemma isGFP_GFP:

  x isGFP f ==> GFP f = x

lemma GFP_fp_lm:

  [| f hasGFP; x = GFP f |] ==> f x = x

lemma GFP_fp:

  f hasGFP ==> f (GFP f) = GFP f

lemma GFP_greatest:

  [| f hasGFP; f x = x |] ==> x ≤ GFP f

lemma hasUFP_hasLFP:

  f hasUFP ==> f hasLFP

lemma hasUFP_LFP_UFP:

  f hasUFP ==> LFP f = UFP f

lemma hasUFP_hasGFP:

  f hasUFP ==> f hasGFP

lemma hasUFP_GFP_UFP:

  f hasUFP ==> GFP f = UFP f