Structure companionTheory

signature companionTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val B_join_def : thm
    val companion_def : thm
    val compatible_def : thm
    val endo_def : thm
    val endo_lift_def : thm
    val higher_compat_def : thm
    val higher_monotone : thm
    val lift_rel : thm
    val set_B_def : thm
    val set_T_def : thm
    val set_companion_def : thm
    val set_compatible_def : thm
  
  (*  Theorems  *)
    val B_greatest_fixpoint_is_companion : thm
    val Bf_compatible_f : thm
    val Tf_idem : thm
    val companion_bot_gfp : thm
    val companion_coinduct : thm
    val companion_expansive : thm
    val companion_idem : thm
    val companion_mono : thm
    val compatible_B_functional_postfix : thm
    val compatible_below_companion : thm
    val compatible_companion : thm
    val compatible_compose : thm
    val compatible_const_gfp : thm
    val compatible_id : thm
    val compatible_self : thm
    val doubling_compatible_B : thm
    val endo_comp : thm
    val endo_function : thm
    val endo_in : thm
    val endo_poset : thm
    val enhanced_gfp : thm
    val lift_rel_comp : thm
    val lub_is_gfp : thm
    val param_coind : thm
    val param_coind_done : thm
    val param_coind_init : thm
    val param_coind_upto_f : thm
    val set_companion : thm
    val set_companion_coinduct : thm
    val set_companion_compatible : thm
    val set_compatible : thm
    val set_compatible_compose : thm
    val set_compatible_enhance : thm
    val set_compatible_id : thm
    val set_compatible_self : thm
    val set_gfp_sub_companion : thm
    val set_higher_complete : thm
    val set_param_coind : thm
    val set_param_coind_done : thm
    val set_param_coind_init : thm
    val set_param_coind_upto_f : thm
    val t_below_Tf : thm
(*
   [fixedPoint] Parent theory of "companion"
   
   [hol] Parent theory of "companion"
   
   [B_join_def]  Definition
      
      ⊢ ∀s r b B.
          B_join (s,r) b B ⇔
          function (endo (s,r)) (endo (s,r)) B ∧
          monotonic (endo_lift (s,r)) B ∧
          ∀g x.
            lub (s,r) {f x | endo (s,r) f ∧ lift_rel (s,r) (f ∘ b) (b ∘ g)}
              (B g x)
   
   [companion_def]  Definition
      
      ⊢ ∀s r b t.
          companion (s,r) b t ⇔
          function s s t ∧ ∀x. lub (s,r) {f x | compatible (s,r) b f} (t x)
   
   [compatible_def]  Definition
      
      ⊢ ∀s r b f.
          compatible (s,r) b f ⇔
          function s s f ∧ monotonic (s,r) f ∧
          lift_rel (s,r) (f ∘ b) (b ∘ f)
   
   [endo_def]  Definition
      
      ⊢ ∀s r f.
          endo (s,r) f ⇔
          monotonic (s,r) f ∧ ∀x. if s x then s (f x) else f x = @y. ¬s y
   
   [endo_lift_def]  Definition
      
      ⊢ ∀s r. endo_lift (s,r) = (endo (s,r),lift_rel (s,r))
   
   [higher_compat_def]  Definition
      
      ⊢ ∀fn b.
          higher_compat fn b ⇔
          (∀f. monotone f ⇒ monotone (fn f)) ∧ higher_monotone fn ∧
          ∀f X. monotone f ⇒ fn (set_B b f) X ⊆ set_B b (fn f) X
   
   [higher_monotone]  Definition
      
      ⊢ ∀fn.
          higher_monotone fn ⇔
          ∀f g.
            monotone f ∧ monotone g ∧ (∀X. f X ⊆ g X) ⇒ ∀X. fn f X ⊆ fn g X
   
   [lift_rel]  Definition
      
      ⊢ ∀s r f g. lift_rel (s,r) f g ⇔ ∀x. s x ⇒ r (f x) (g x)
   
   [set_B_def]  Definition
      
      ⊢ ∀b. set_B b =
            (λg X. BIGUNION {f X | monotone f ∧ ∀Y. f (b Y) ⊆ b (g Y)})
   
   [set_T_def]  Definition
      
      ⊢ ∀b. set_T b =
            (λf X.
                 BIGUNION
                   {fn f X | fn | monotone (fn f) ∧ higher_compat fn b})
   
   [set_companion_def]  Definition
      
      ⊢ ∀b X. set_companion b X = BIGUNION {f X | set_compatible b f}
   
   [set_compatible_def]  Definition
      
      ⊢ ∀b f. set_compatible b f ⇔ monotone f ∧ ∀X. f (b X) ⊆ b (f X)
   
   [B_greatest_fixpoint_is_companion]  Theorem
      
      ⊢ poset (s,r) ∧ endo (s,r) b ∧ endo (s,r) t ∧ companion (s,r) b t ∧
        B_join (s,r) b B ⇒
        po_gfp (endo_lift (s,r)) B t
   
   [Bf_compatible_f]  Theorem
      
      ⊢ poset (s,r) ∧ endo (s,r) b ∧ endo (s,r) f ∧ B_join (s,r) b B ⇒
        lift_rel (s,r) (B f ∘ b) (b ∘ f)
   
   [Tf_idem]  Theorem
      
      ⊢ poset (s,r) ∧ endo (s,r) b ∧ B_join (s,r) b B ∧ endo (s,r) t ∧
        companion (s,r) b t ∧ companion (endo_lift (s,r)) B T' ∧
        bottom (endo_lift (s,r)) bot ∧ endo (s,r) f ⇒
        T' f ∘ T' f = T' f
   
   [companion_bot_gfp]  Theorem
      
      ⊢ poset (s,r) ∧ monotonic (s,r) b ∧ function s s b ∧
        bottom (s,r) bot ∧ po_gfp (s,r) b gfix ∧ companion (s,r) b t ⇒
        t bot = gfix
   
   [companion_coinduct]  Theorem
      
      ⊢ poset (s,r) ∧ monotonic (s,r) b ∧ function s s b ∧
        companion (s,r) b t ∧ po_gfp (s,r) b gfix ∧ s x ∧ r x ((b ∘ t) x) ⇒
        r x gfix
   
   [companion_expansive]  Theorem
      
      ⊢ poset (s,r) ∧ function s s b ∧ monotonic (s,r) b ∧
        companion (s,r) b t ∧ s x ⇒
        r x (t x)
   
   [companion_idem]  Theorem
      
      ⊢ poset (s,r) ∧ function s s b ∧ monotonic (s,r) b ∧
        companion (s,r) b t ∧ s x ⇒
        t (t x) = t x
   
   [companion_mono]  Theorem
      
      ⊢ poset (s,r) ∧ function s s b ∧ monotonic (s,r) b ∧
        companion (s,r) b t ⇒
        monotonic (s,r) t
   
   [compatible_B_functional_postfix]  Theorem
      
      ⊢ poset (s,r) ∧ endo (s,r) b ∧ B_join (s,r) b B ∧ endo (s,r) f ⇒
        (lift_rel (s,r) f (B f) ⇔ lift_rel (s,r) (f ∘ b) (b ∘ f))
   
   [compatible_below_companion]  Theorem
      
      ⊢ poset (s,r) ∧ compatible (s,r) b f ∧ companion (s,r) b t ⇒
        lift_rel (s,r) f t
   
   [compatible_companion]  Theorem
      
      ⊢ poset (s,r) ∧ function s s b ∧ monotonic (s,r) b ∧
        companion (s,r) b t ⇒
        compatible (s,r) b t
   
   [compatible_compose]  Theorem
      
      ⊢ poset (s,r) ∧ function s s b ∧ monotonic (s,r) b ∧
        compatible (s,r) b f ∧ compatible (s,r) b g ⇒
        compatible (s,r) b (f ∘ g)
   
   [compatible_const_gfp]  Theorem
      
      ⊢ poset (s,r) ∧ function s s b ∧ monotonic (s,r) b ∧
        po_gfp (s,r) b fp ⇒
        compatible (s,r) b (K fp)
   
   [compatible_id]  Theorem
      
      ⊢ poset (s,r) ∧ function s s b ∧ monotonic (s,r) b ⇒
        compatible (s,r) b I
   
   [compatible_self]  Theorem
      
      ⊢ poset (s,r) ∧ function s s b ∧ monotonic (s,r) b ⇒
        compatible (s,r) b b
   
   [doubling_compatible_B]  Theorem
      
      ⊢ poset (s,r) ∧ endo (s,r) b ∧ B_join (s,r) b B ⇒
        compatible (endo_lift (s,r)) B (λf. f ∘ f)
   
   [endo_comp]  Theorem
      
      ⊢ endo (s,r) f ∧ endo (s,r) g ⇒ endo (s,r) (f ∘ g)
   
   [endo_function]  Theorem
      
      ⊢ endo (s,r) f ⇒ function s s f
   
   [endo_in]  Theorem
      
      ⊢ endo (s,r) t ∧ s x ⇒ s (t x)
   
   [endo_poset]  Theorem
      
      ⊢ poset (s,r) ⇒ poset (endo_lift (s,r))
   
   [enhanced_gfp]  Theorem
      
      ⊢ poset (s,r) ∧ monotonic (s,r) b ∧ function s s b ∧
        po_gfp (s,r) b gfix ∧ companion (s,r) b t ∧
        po_gfp (s,r) (b ∘ t) efix ⇒
        efix = gfix
   
   [lift_rel_comp]  Theorem
      
      ⊢ poset (s,r) ∧ function s s g ∧ function s s f ∧ function s s f' ∧
        function s s g' ∧ monotonic (s,r) f ∧ monotonic (s,r) f' ∧
        lift_rel (s,r) f f' ∧ lift_rel (s,r) g g' ⇒
        lift_rel (s,r) (f ∘ g) (f' ∘ g')
   
   [lub_is_gfp]  Theorem
      
      ⊢ poset (s,r) ∧ function s s f ∧ monotonic (s,r) f ∧
        lub (s,r) {x | r x (f x)} l ⇒
        po_gfp (s,r) f l
   
   [param_coind]  Theorem
      
      ⊢ complete (s,r) ∧ complete (endo_lift (s,r)) ∧ poset (s,r) ∧
        endo (s,r) b ∧ companion (s,r) b t ∧ endo (s,r) t ∧
        B_join (s,r) b B ∧ companion (endo_lift (s,r)) B T' ∧
        po_gfp (s,r) b gfix ∧ s x ∧ s y ∧ lub (s,r) {x; y} xy ⇒
        r y (b (t xy)) ⇒
        r y (t x)
   
   [param_coind_done]  Theorem
      
      ⊢ poset (s,r) ∧ monotonic (s,r) b ∧ function s s b ∧
        companion (s,r) b t ⇒
        s x ∧ s y ∧ r y x ⇒
        r y (t x)
   
   [param_coind_init]  Theorem
      
      ⊢ poset (s,r) ∧ monotonic (s,r) b ∧ function s s b ∧
        bottom (s,r) bot ∧ po_gfp (s,r) b gfix ∧ companion (s,r) b t ⇒
        r x (t bot) ⇒
        r x gfix
   
   [param_coind_upto_f]  Theorem
      
      ⊢ poset (s,r) ∧ monotonic (s,r) b ∧ function s s b ∧
        companion (s,r) b t ⇒
        function s s f ∧ (∀x. r (f x) (t x)) ⇒
        s x ∧ s y ∧ r y (f (t x)) ⇒
        r y (t x)
   
   [set_companion]  Theorem
      
      ⊢ companion (𝕌(:α -> bool),$SUBSET) b (set_companion b)
   
   [set_companion_coinduct]  Theorem
      
      ⊢ monotone b ∧ X ⊆ (b ∘ set_companion b) X ⇒ X ⊆ gfp b
   
   [set_companion_compatible]  Theorem
      
      ⊢ monotone b ⇒ set_compatible b (set_companion b)
   
   [set_compatible]  Theorem
      
      ⊢ set_compatible b f ⇒ compatible (𝕌(:α -> bool),$SUBSET) b f
   
   [set_compatible_compose]  Theorem
      
      ⊢ monotone b ⇒
        set_compatible b f ∧ set_compatible b g ⇒
        set_compatible b (f ∘ g)
   
   [set_compatible_enhance]  Theorem
      
      ⊢ monotone b ∧ set_compatible b f ∧ Y ⊆ f X ⇒ Y ⊆ set_companion b X
   
   [set_compatible_id]  Theorem
      
      ⊢ monotone b ⇒ set_compatible b I
   
   [set_compatible_self]  Theorem
      
      ⊢ monotone b ⇒ set_compatible b b
   
   [set_gfp_sub_companion]  Theorem
      
      ⊢ monotone b ⇒ gfp b ⊆ set_companion b x
   
   [set_higher_complete]  Theorem
      
      ⊢ complete (endo_lift (𝕌(:α -> bool),$SUBSET))
   
   [set_param_coind]  Theorem
      
      ⊢ monotone b ⇒
        Y ⊆ b (set_companion b (X ∪ Y)) ⇒
        Y ⊆ set_companion b X
   
   [set_param_coind_done]  Theorem
      
      ⊢ monotone b ∧ Y ⊆ X ⇒ Y ⊆ set_companion b X
   
   [set_param_coind_init]  Theorem
      
      ⊢ monotone b ∧ X ⊆ set_companion b ∅ ⇒ X ⊆ gfp b
   
   [set_param_coind_upto_f]  Theorem
      
      ⊢ monotone b ∧ (∀X. f X ⊆ set_companion b X) ∧
        Y ⊆ f (set_companion b X) ⇒
        Y ⊆ set_companion b X
   
   [t_below_Tf]  Theorem
      
      ⊢ poset (s,r) ∧ endo (s,r) b ∧ endo (s,r) t ∧ companion (s,r) b t ∧
        B_join (s,r) b B ∧ bottom (endo_lift (s,r)) bot ∧
        companion (endo_lift (s,r)) B T' ∧ endo (s,r) f ⇒
        lift_rel (s,r) t (T' f)
   
   
*)
end

HOL 4, Trindemossen-2