Theory Infra

           (*-------------------------------------------*
            |                CSP-Prover                 |
            |               November 2004               |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory Infra = Complex_Main: 

(*****************************************************
           Convenient technique for proofs
 *****************************************************)

(*--------------------------*
 |    remove assumeption    |
 *--------------------------*)

lemma rem_asmE: "[| A ; R |] ==> R"
by simp

(*****************************************************
                  Infinite Sequence
 *****************************************************)

types 'a infinite_seq = "nat => 'a"           (* synonym *)

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

lemma eq_iff: "((x::'a::order) = y) = (x <= y & y <= x)"
apply (rule iffI)
apply (simp)
apply (rule order_antisym)
by (simp_all)

lemma eq_iffI: "[| x <= y ; y <= x |] ==> ((x::'a::order) = y)"
by (simp add: eq_iff)

lemma eq_iffE: "[| (x::'a::order) = y ; [| x <= y ; y <= x |] ==> R |] ==> R"
by (simp add: eq_iff)

(********************************************************** 
              inducrive function --> ALL n
 **********************************************************)

consts
  inductivefun :: "('a => bool) => ('a => 'a) => bool"

defs
 inductivefun_def :
     "inductivefun R f == (ALL x. R x --> R (f x))"

lemma inductivefun_all_n:
  "[| inductivefun R f ; R x |] ==> (ALL n. R ((f^n) x))"
apply (intro allI)
apply (induct_tac n)
apply (simp)
apply (simp add: inductivefun_def)
done

(*****************************************************
                      nat
 *****************************************************)

lemma nat_zero_or_Suc: "ALL n::nat. n=0 | (EX m::nat. n=Suc m)"
apply (intro allI)
apply (induct_tac n)
apply (simp)
apply (rule disjI2)
apply (erule disjE)
apply (rule_tac x=0 in exI)
apply (simp)
apply (erule exE)
apply (rule_tac x="Suc m" in exI)
apply (simp)
done

(*** min ***)

lemma min_is1: "(m::'a::order) <= n ==> min m n = m"
by (simp add: min_def)

lemma min_is2: "(n::'a::order) <= m ==> min m n = n"
apply (simp add: min_def)
apply (force)
done

lemmas min_is = min_is1 min_is2

(*** max ***)

lemma max_is1: "(m::'a::order) <= n ==> max m n = n"
by (simp add: max_def)

lemma max_is2: "(n::'a::order) <= m ==> max m n = m"
apply (simp add: max_def)
apply (force)
done

lemmas max_is = max_is1 max_is2

(*****************************************************
               Small lemmas for List 
 *****************************************************)

lemma one_list_decompo: 
   "([a] = s @ t) = ((s =[] & t = [a]) | (s = [a] & t = []))"
by (induct_tac s, auto)

lemma list_nil_or_unnil: "ALL t. (t = []) | (EX a s. t = a # s)"
apply (intro allI)
by (induct_tac t, auto)

lemma list_last_nil_or_unnil: "ALL t. (t = []) | (EX s a. t =s @ [a])"
apply (intro allI)
by (induct_tac t, auto)

(****** butlast ******)

lemma notin_butlast_decompo:
  "e ~: set (butlast (s @ t))
      = ((e ~: set s & e ~: set (butlast t)) | (e ~: set (butlast s) & t = []))"
apply (induct_tac s)
by (auto)

lemma in_butlast_decompo:
  "e : set (butlast (s @ t))
      = ((e : set s | e : set (butlast t)) & (e : set (butlast s) | t ~= []))"
apply (induct_tac s)
by (auto)

lemma butlast_subseteq : "set (butlast s) <= set s"
apply (induct_tac s)
by (auto)

(*** length s = 1 ***)

lemma list_length_one: "(length s = Suc 0) = (EX a. s =[a])"
apply (induct_tac s)
by (auto)

(****** list app app ******)

(*** lm ***)

lemma list_app_app_only_if:
  "ALL s1 s2 t1 t2. (s1 @ s2 = t1 @ t2)
       --> ((EX u. s1 = t1 @ u & t2 = u @ s2) |
            (EX u. t1 = s1 @ u & s2 = u @ t2)   )"
apply (rule allI)
apply (induct_tac s1)
apply (intro allI impI)
apply (rule disjI2)
apply (rule_tac x="t1" in exI)
apply (simp)

 (* step *)

apply (intro allI impI)
apply (insert list_nil_or_unnil)
apply (rotate_tac -1)
apply (drule_tac x="t1" in spec)
apply (erule disjE)

  (* t1 = [] *)
 apply (simp)

  (* t1 ~= [] *)
 apply (elim exE)
 apply (simp)
done

(*** list app app ***)

lemma list_app_app:
  "(s1 @ s2 = t1 @ t2) =
      ((EX u. s1 = t1 @ u & t2 = u @ s2) |
       (EX u. t1 = s1 @ u & s2 = u @ t2))"
apply (rule iffI)
apply (simp add: list_app_app_only_if)
apply (auto)
done

(*** list app [a] ***)

lemma list_app_decompo_one:
  "(s @ t = [a]) = ((s = [a] & t = []) | (s = [] & t = [a]))"
apply (induct_tac s)
by (auto)

(*****************************************************
                    Real number
 *****************************************************)

lemma real_mult_add_distrib: "(x::real) * (y + z) = x * y + x * z"
apply (subgoal_tac "x * (y + z) = (y + z) * x")
apply (simp add: real_add_mult_distrib)
apply (simp add: real_mult_commute)
done

lemma real_mult_order_eq : "[| 0 <= x; 0 <= y |] ==> (0::real) <= x * y"
apply (case_tac "x = 0", simp)
apply (case_tac "y = 0", simp)
apply (subgoal_tac "0 < x * y")
apply (simp)
apply (simp add: real_mult_order)
done

lemma real_div_le_eq:
   "0 < (z::real) ==> (x <= y / z) = (x * z <= y)"
apply (rule iffI)
apply (insert mult_right_mono[of x "y/z" z], simp)
apply (insert real_mult_le_cancel_iff1[of z x "y/z"], simp)
done

lemma real_div_less_eq:
   "0 < (z::real) ==> (x < y / z) = (x * z < y)"
apply (rule iffI)
apply (insert real_mult_less_iff1[of z x "y/z"], simp)
apply (insert mult_less_cancel_right[of x "y/z" z], simp)
done

lemma real_less_div_eq:
   "0 < (z::real) ==> (x / z < y) = (x < y * z)"
apply (rule iffI)
apply (insert real_mult_less_iff1[of z "x/z" y], simp)
apply (insert mult_less_cancel_right[of "x/z" y z], simp)
done

lemma real_mult_div_commute: 
     "[| (0::real) <= x ; 0 < y ; 0 < z ; 0 < r |]
        ==> (x < y * z / r) = (r * x / z < y)"
apply (simp add: real_div_less_eq)
apply (simp add: real_less_div_eq)
apply (simp add: real_mult_commute)
done

lemma real_mult_less_iff2: "(0::real) < z ==> (z*x < z*y) = (x < y)"
by (simp add: real_mult_commute)

lemma real_mult_less_if2: "[| (0::real) < z ; (x::real) < y |] ==> z*x < z*y"
by (simp add: real_mult_less_iff2)

lemma real_mult_less_if1: "[| (0::real) < z ; (x::real) < y |] ==> x*z < y*z"
by (simp)

(*** rev_power_decreasing ***)

lemma rev_power_decreasing:
  "[| (0::real) < r ; r < 1 ; r ^ n <= r ^ m |] ==> m <= n"

apply (case_tac "m <= n")
 apply (simp)

(* else n < m --> contradiction *)
apply (insert power_decreasing[of "Suc n" m r])
apply (simp)
apply (subgoal_tac "r * r ^ n <  1 * r ^ n")
apply (simp)
apply (rule real_mult_less_if1)
by (simp_all)

(*** rev_power_decreasing_strict ***)

lemma rev_power_decreasing_strict :
  "[| (0::real) < r ; r < 1 ; r ^ n < r ^ m |] ==> m < n"
apply (case_tac "m < n")
 apply (simp)

(* else n <= m --> contradiction *)
apply (insert power_decreasing[of n m r])
by (simp)

(*****************************************************
               Small lemmas for Set
 *****************************************************)

lemma notin_subset: "[| S <= T ; a ~: T |] ==> a ~: S"
by (auto)

lemma notin_set_butlast: "a ~: set s ==> a ~: set (butlast s)"
apply (rule notin_subset[of _ "set s"])
by (simp_all add: butlast_subseteq)

lemma in_set_butlast: "a : set (butlast s) ==> a : set s"
apply (erule contrapos_pp)
by (simp add: notin_set_butlast)

lemma in_image_set: "x : f ` X = (EX y. x = f y & y:X)"
by (auto)

lemma inj_image_diff_dist: "inj f ==> f ` (A - B) = f ` A - f ` B"
by (auto simp add: inj_on_def)

lemma inj_image_Int_dist: "inj f ==> f ` (A Int B) = f ` A Int f ` B"
by (auto simp add: inj_on_def)

lemma subsetE: "[| A <= B ; [| ALL x:A. x:B |] ==> R |] ==> R"
by (auto)

(*****************************************************
            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

(*-----------------------*
 |       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

(*-----------------------*
 |       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

(*-----------------------*
 |     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)

(*****************************
         powr --> pow  
 *****************************)

lemma nat_powr_pow:
  "(0::real) < r ==> r powr (real n) = r ^ n"
apply (induct_tac n)
apply (simp)
apply (simp add: real_of_nat_Suc)
apply (simp add: powr_add)
done

(*****************************************************
              Exponentail convergence
 *****************************************************)

lemma powr_less_mono_inv:
  "[| (1::real) < a ; (x::real) < y |]
     ==> (inverse a) powr y < (inverse a) powr x"
apply (simp add: powr_def)
apply (auto simp add: ln_inverse)
done

lemma powr_less_mono_conv:
  "[| (0::real) < a ; a < (1::real) ; (x::real) < y |]
    ==> a powr y < a powr x"
apply (insert powr_less_mono_inv[of "inverse a" x y])
apply (simp)
apply (subgoal_tac "1 < inverse a")
apply (simp)
apply (rule inverse_less_imp_less)
apply (simp_all)
done

lemma powr_convergence:
  "[| (0::real) < alpha ; alpha < (1::real) ; (0::real) < x |]
      ==> (EX n::nat. alpha powr (real n) < x)"
apply (insert powr_log_cancel[of "alpha" x])
apply (insert reals_Archimedean2[of "log alpha x"])
apply (erule exE) 
apply (subgoal_tac "alpha powr real n < alpha powr log alpha x")
apply (rule_tac x="n" in exI)
apply (simp)
apply (insert powr_less_mono_conv[of "alpha" "log alpha x"])
by (simp)

lemma pow_convergence:
  "[| (0::real) <= alpha ; alpha < (1::real) ; (0::real) < x |]
   ==> (EX n::nat. alpha^n < x)"

apply (case_tac "alpha=0")
 apply (rule_tac x="1" in exI)
 apply (simp)

apply (case_tac "0 < alpha")
 apply (insert powr_convergence[of "alpha" x])
 apply (simp)
 apply (erule exE)
 apply (rule_tac x="n" in exI)
 apply (simp add: nat_powr_pow)

apply (simp add: real_less_le)
done

(*** if 0 <=alpha < 1 then alpha^n ----> 0 ***)

lemma zero_isGLB_pow:
  "[| (0::real) <= alpha ; alpha < 1 |] 
   ==> (0 isGLB {r. EX n. r = alpha ^ n})"
apply (simp add: isGLB_def isLB_def)
apply (rule conjI)

(* lb *)

apply (intro allI impI)
apply (erule exE)
apply (simp add: zero_le_power)

(* glb *)

apply (intro allI impI)
apply (case_tac "y <=0")
apply (simp)

 (* 0 < y *)
 apply (subgoal_tac "EX n. alpha ^ n < y")
 apply (simp)
 apply (erule exE)
 apply (drule_tac x="alpha ^ n" in spec)
 apply (simp)
 apply (drule_tac x="n" in spec)
 apply (simp)

 apply (simp add: pow_convergence)
done

(*** GLB ***)

lemma zero_GLB_pow:
  "[| (0::real) <= alpha ; alpha < 1 |] 
   ==> GLB {r. EX n. r = alpha ^ n} = 0"
apply (subgoal_tac "{r. EX n. r = alpha ^ n} hasGLB")
apply (simp add: GLB_iff zero_isGLB_pow)
apply (insert zero_isGLB_pow[of alpha])
apply (simp add: hasGLB_def)
apply (rule_tac x="0" in exI)
by (simp)

(*****************************************************
                    Progression
 *****************************************************)

consts
  prog_sum0 :: "nat => (nat => real) => real"
  prog_sum  :: "nat => nat => (nat => real) => real"
  geo_prop  :: "real => real => nat => real"

primrec
  "prog_sum0 (Suc n) f = (prog_sum0 n f) + f (Suc n)"
  "prog_sum0 0 f = 0"

defs
  prog_sum_def : 
    "prog_sum m n f == (prog_sum0 n f) - (prog_sum0 m f)"

  geo_prop_def :
    "geo_prop K alpha == (%n. (alpha^(n - (Suc 0))) * K)"

lemma geo_prog_sum0: 
  "prog_sum0 n (geo_prop K alpha) * ((1::real) - alpha)
       = K*((1::real)-(alpha^n))"
apply (induct_tac n)
apply (simp)
apply (simp add: geo_prop_def)
apply (simp add: real_add_mult_distrib)
apply (simp add: right_diff_distrib)
done

lemma geo_prog_sum: 
  "prog_sum m n (geo_prop K alpha) * ((1::real) - alpha)
       = K*((alpha^m)-(alpha^n))"
apply (unfold prog_sum_def)
apply (simp add: left_diff_distrib)
apply (simp add: geo_prog_sum0)
apply (simp add: right_diff_distrib)
done

lemmas geo_prog_sum_sym = geo_prog_sum[THEN sym]

lemma geo_prog_sum_div: 
  "alpha < (1::real)
    ==> prog_sum m n (geo_prop K alpha)
      = K*((alpha^m)-(alpha^n)) / ((1::real)-alpha)"
by (simp add: geo_prog_sum_sym)

lemma geo_prog_sum_infinite: 
  "[| (0::real) <= K ; (0::real) <= alpha |]
   ==>  prog_sum m n (geo_prop K alpha) * ((1::real)-alpha)
       <= K*(alpha^m)"
apply (simp add: geo_prog_sum)
apply (simp add: right_diff_distrib)
apply (simp add: zero_le_power real_mult_order_eq)
done

lemma geo_prog_sum_infinite_div: 
  "[| (0::real) <= K ; (0::real) <= alpha ; alpha < (1::real) |] 
   ==> prog_sum m n (geo_prop K alpha) <= K*(alpha^m)/((1::real)-alpha)"
apply (simp add: real_div_le_eq)
apply (simp_all add: geo_prog_sum_infinite)
done

(*****************************************************
                      fun (Product)
 *****************************************************)

(*******************************
        <= in fun
 *******************************)

instance fun :: (type,order) ord 
by (intro_classes)

defs (overloaded)
  order_prod_def:
     "xp <= yp  ==  ALL x. (xp x <= yp x)"
  order_less_prod_def:
     "xp < yp  ==  (ALL x. (xp x <= yp x)) &
                   (EX  x. (xp x ~= yp x))"

(*** order in prod ***)

instance fun :: (type,order) order
apply (intro_classes)
apply (unfold order_prod_def order_less_prod_def)
apply (simp)
apply (blast intro: order_trans)

apply (simp add: expand_fun_eq)
apply (blast intro: order_antisym)

apply (auto simp add: expand_fun_eq)
done

lemma order_prod_inv: "[| ALL x. f x <= g x |] ==> f <= g"
by (simp add: order_prod_def)

(*****************************************************
                   fun (Projection)
 *****************************************************)

consts
 proj_fun :: "'i => ('i => 'x) => 'x"

defs
 proj_fun_def : "proj_fun i == (%x. x i)"

(*** lub for projection ***)

(*** only if ***)

lemma prod_LUB_decompo_only_if:
  "x isLUB X ==> ALL i. (proj_fun i) x isLUB (proj_fun i) ` X"
apply (simp add: proj_fun_def)
apply (simp add: isLUB_def)
apply (auto)

 (*** upper ***)

apply (simp add: isUB_def)
apply (auto)
apply (drule_tac x="xa" in spec)
apply (simp add: order_prod_def)

 (*** least ***)

apply (drule_tac x="(%j. if (i=j) then y else (x j))" in spec)
apply (drule mp)

 apply (simp add: isUB_def)
 apply (intro allI impI)
 apply (simp add: order_prod_def)

 apply (simp add: order_prod_def)
 apply (drule_tac x="i" in spec)
 apply (simp)
done

(*** if ***)

lemma prod_LUB_decompo_if: 
  "ALL i. (proj_fun i) x isLUB (proj_fun i) ` X ==> x isLUB X"
apply (simp add: isLUB_def)
apply (rule conjI)

 (*** upper ***)

apply (simp add: isUB_def)
apply (auto)
apply (simp add: order_prod_def)
apply (intro allI)
apply (rename_tac y i)
apply (drule_tac x="i" in spec)

apply (erule conjE)
apply (drule_tac x="y i" in spec)
apply (simp add: proj_fun_def)

 (*** least ***)

apply (simp add: order_prod_def)
apply (intro allI)
apply (rename_tac y i)
apply (drule_tac x="i" in spec)

apply (erule conjE)
apply (drule_tac x="y i" in spec)
apply (simp add: proj_fun_def)
apply (drule mp)

 apply (simp add: isUB_def)
 apply (intro allI impI)
 apply (simp add: image_def)
 apply (erule bexE)
 apply (drule_tac x="xa" in spec)
 apply (simp add: order_prod_def)
 apply (simp)
done

(*** iff ***)

lemma prod_LUB_decompo: 
  "x isLUB X = (ALL i. (proj_fun i) x isLUB (proj_fun i) ` X)"
apply (rule iffI)
apply (simp add: prod_LUB_decompo_only_if)
apply (simp add: prod_LUB_decompo_if)
done

(*****************************************************
                         Pair
 *****************************************************)

consts
  pair_fun :: "('x => 'y) => ('x => 'z) => ('x => ('y * 'z))" 
                                           ("(2_ **/ _)" [51,52] 52)
defs
  pair_fun_def : "f ** g == (%x. (f x, g x))"

(*** lemmas ***)

lemma fst_pair_fun[simp]: "fst o (f ** g) = f"
by (simp add: expand_fun_eq pair_fun_def)

lemma snd_pair_fun[simp]: "snd o (f ** g) = g"
by (simp add: expand_fun_eq pair_fun_def)

lemma pair_eq_decompo:
  "ALL (xc::('x * 'y)) (yc::('x * 'y)).
      (xc = yc) = ((fst xc = fst yc) & (snd xc = snd yc))"
by (simp)

lemma pair_neq_decompo:
  "ALL (xc::('x * 'y)) (yc::('x * 'y)).
      (xc ~= yc) = ((fst xc ~= fst yc) | (snd xc ~= snd yc))"
by (simp)

(*******************************
         <= in pair
 *******************************)

instance * :: (order,order) ord 
by (intro_classes)

defs (overloaded)
  order_pair_def:
     "xc <= yc  ==  (fst xc <= fst yc) & (snd xc <= snd yc)"
  order_less_pair_def:
     "xc <  yc  ==  (fst xc <= fst yc) & (snd xc <=  snd yc) &
                   ((fst xc ~= fst yc) | (snd xc ~=  snd yc))"

(*** order in pair ***)

instance * :: (order,order) order
apply (intro_classes)
apply (unfold order_pair_def order_less_pair_def)
apply (simp)
apply (blast intro: order_trans)

apply (simp add: pair_eq_decompo)
apply (blast intro: order_antisym)

apply (auto simp add: pair_neq_decompo)
done

(*** LUB is decomposed for * ***)

(* only if *)

lemma pair_LUB_decompo_fst_only_if:
  "xc isLUB (Xc::('x::order * 'y::order) set)
   ==> (fst xc isLUB fst ` Xc)"
apply (simp add: isLUB_def isUB_def)
apply (simp add: image_def)
apply (rule conjI)

      (* UB *)
apply (intro allI impI)
apply (simp add: order_pair_def)
apply (erule bexE)
apply (elim conjE)
apply (drule_tac x="fst x" in spec)
apply (drule_tac x="snd x" in spec)
apply (simp)

      (* LUB *)
apply (intro allI impI)
apply (simp add: order_pair_def)
apply (elim conjE)
apply (rotate_tac -1)
apply (drule_tac x="y" in spec)
apply (rotate_tac -1)
apply (drule_tac x="snd xc" in spec)
apply (drule mp)

 apply (intro allI impI)
 apply (drule_tac x="a" in spec)
 apply (drule mp)
  apply (rule_tac x="(a, b)" in bexI, simp)
 apply (simp)

 apply (drule_tac x="a" in spec)
 apply (drule_tac x="b" in spec)
 apply (simp)
 apply (simp)
done

lemma pair_LUB_decompo_snd_only_if:
  "xc isLUB (Xc::('x::order * 'y::order) set)
   ==> (snd xc isLUB snd ` Xc)"
apply (simp add: isLUB_def isUB_def)
apply (simp add: image_def)
apply (rule conjI)

      (* UB *)
apply (intro allI impI)
apply (simp add: order_pair_def)
apply (erule bexE)
apply (elim conjE)
apply (drule_tac x="fst x" in spec)
apply (drule_tac x="snd x" in spec)
apply (simp)

      (* LUB *)
apply (intro allI impI)
apply (simp add: order_pair_def)
apply (elim conjE)
apply (rotate_tac -1)
apply (drule_tac x="fst xc" in spec)
apply (rotate_tac -1)
apply (drule_tac x="y" in spec)
apply (drule mp)

 apply (intro allI impI)
 apply (drule_tac x="b" in spec)
 apply (drule mp)
  apply (rule_tac x="(a, b)" in bexI, simp)
 apply (simp)

 apply (drule_tac x="a" in spec)
 apply (drule_tac x="b" in spec)
 apply (simp)
 apply (simp)
done

(* if *)

lemma pair_LUB_decompo_if:
  "(fst xc isLUB fst ` Xc) & (snd xc isLUB snd ` Xc)
          ==> xc isLUB (Xc::('x::order * 'y::order) set)"
apply (simp add: isLUB_def isUB_def)
apply (simp add: image_def)
apply (rule conjI)

apply (intro allI impI)
apply (simp add: order_pair_def)
apply (elim conjE)
apply (drule_tac x="a" in spec)
apply (drule mp)
apply (rule_tac x="(a, b)" in bexI)
apply (simp)
apply (simp)

apply (rotate_tac 1)
apply (drule_tac x="b" in spec)
apply (drule mp)
apply (rule_tac x="(a, b)" in bexI)
apply (simp)
apply (simp)
apply (simp)

(*** least ***)

apply (intro allI impI)
apply (elim conjE)
apply (rotate_tac 2)
apply (drule_tac x="a" in spec)
apply (rotate_tac 1)
apply (drule_tac x="b" in spec)

apply (drule mp)
apply (intro allI impI)
apply (erule bexE)
apply (drule_tac x="y" in spec)
apply (rotate_tac -1)
apply (drule_tac x="snd x" in spec)
apply (simp add: order_pair_def)

apply (drule mp)
apply (intro allI impI)
apply (erule bexE)
apply (drule_tac x="fst x" in spec)
apply (rotate_tac -1)
apply (drule_tac x="y" in spec)
apply (simp add: order_pair_def)

apply (simp add: order_pair_def)
done

(* iff *)

lemma pair_LUB_decompo:
  "xc isLUB (Xc::('x::order * 'y::order) set)
   = ((fst xc isLUB fst ` Xc) & (snd xc isLUB snd ` Xc))"
apply (rule iffI)
apply (simp add: pair_LUB_decompo_fst_only_if pair_LUB_decompo_snd_only_if)
apply (simp add: pair_LUB_decompo_if)
done

end