transfinite.mlw 11.6 KB
Newer Older
1 2 3 4 5 6 7 8

(* Definition and lemmas about the transfinite sequence
   generated by an inflationary function on a chain-complete order. *)

module IterateCommon

  use import order.Chain

9 10
  (* Transfinite reachability of an inflationary function
     in chain-complete orders. *)
11 12 13 14 15 16 17 18 19 20 21 22
  inductive tr_reach ('a -> 'a -> bool) ('a -> 'a) (_ _:'a) =
    | Reach_base : forall o f,x:'a. tr_reach o f x x
    | Reach_succ : forall o f,x y:'a. tr_reach o f x y -> tr_reach o f x (f y)
    | Reach_chain : forall o f x c,y:'a.
      chain o c /\ c x /\ (forall y. c y -> tr_reach o f x y) /\
      supremum o c y -> tr_reach o f x y

  predicate separator (o:'a -> 'a -> bool) (f:'a -> 'a) (base x:'a) =
    o x base \/ o (f base) x

end

23
module Iterates "W:non_conservative_extension:N" (* => IterateProof *)
24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39

  use import order.Chain
  use export IterateCommon

  (* tr_reach is a chain, and there are no
     tr_reach element between any z and its 'sucessor' f z. *)
  axiom tr_reach_separated : forall o f,x y z:'a.
    order o /\ inflationary o f /\ tr_reach o f x y /\ tr_reach o f x z ->
    separator o f z y

  (* For chain-complete orders, there is a maximum tr_reach element,
     which is a fixpoint of the growth function
     (the fixpoint part is the Bourbaki-Witt theorem) *)
  function fixpoint_above (o:'a -> 'a -> bool) (f:'a -> 'a) 'a : 'a

  axiom tr_reach_maximum : forall o f,x:'a.
40
    order o /\ inflationary o f /\ q_chain_complete o ->
41 42 43
    f (fixpoint_above o f x) = fixpoint_above o f x /\
    maximum o (tr_reach o f x) (fixpoint_above o f x)

44
  (* Transfinite chain stop at the first encountered fixpoint. *)
45 46 47 48 49 50 51 52 53 54 55 56 57
  axiom tr_reach_fixpoint : forall o f,x y:'a.
    order o /\ inflationary o f /\ f y = y /\ tr_reach o f x y ->
    maximum o (tr_reach o f x) y

  (* transifinite reachability relation is compatible with the base order. *)
  axiom tr_reach_compare : forall o f,x y:'a.
    preorder o /\ inflationary o f /\ tr_reach o f x y -> o x y

  (* transfinite reachability relation is transitive. *)
  axiom tr_reach_transitive : forall o f,x y z:'a.
    preorder o /\ inflationary o f ->
    tr_reach o f x y /\ ("induction" tr_reach o f y z) -> tr_reach o f x z

58
  (* the set of reachable states from a given one is a well-founded chain
59 60
     for the base order relation. *)
  axiom tr_reach_wf : forall o f,x:'a.
61 62
    order o /\ inflationary o f ->
      wf_chain o (tr_reach o f x) && chain o (tr_reach o f x)
63 64 65 66 67

end

module IterateProof

68 69 70
  use import ho_set.Set
  use import order.WfChain
  use import order.LimUniq
71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108
  use import choice.Choice
  use import IterateCommon

  lemma tr_reach_compare : forall o f,x y:'a.
    preorder o /\ inflationary o f -> ("induction" tr_reach o f x y) -> o x y

  predicate near_all_separator (o:'a -> 'a -> bool) (f:'a -> 'a) (u a:'a) =
    tr_reach o f u a /\
    forall c b. tr_reach o f u c /\ tr_reach o f u b /\ o c a /\ not o a c ->
      separator o f c b

  (* Any element <= a is a separator. *)
  predicate all_separator (o:'a -> 'a -> bool) (f:'a -> 'a) (u a:'a) =
    tr_reach o f u a /\
    forall c b. tr_reach o f u c /\ tr_reach o f u b /\ o c a ->
      separator o f c b

  lemma separation : forall o f,u base:'a.
    order o /\ inflationary o f /\ near_all_separator o f u base ->
    (forall o1 f1 u1 x. o1 = o /\ f1 = f /\ u1 = u ->
      ("induction" tr_reach o1 f1 u1 x) -> separator o f base x)

  lemma all_separation : forall o,f,u:'a.
    order o /\ inflationary o f ->
    (forall o1 f1 u1 x. o1 = o /\ f1 = f /\ u1 = u ->
      ("induction" tr_reach o1 f1 u1 x) -> all_separator o f u x)
    by (forall a. all_separator o f u a ->
        near_all_separator o f u (f a) by forall c b. o c (f a) /\
            not o (f a) c /\ tr_reach o f u c /\ tr_reach o f u b ->
            separator o f c b by separator o f a c)
      /\ forall ch a. ch u /\ (forall y. ch y -> all_separator o f u y) /\
        chain o ch /\ supremum o ch a ->
        near_all_separator o f u a by forall c b. o c a /\
          not o a c /\ tr_reach o f u c /\ tr_reach o f u b ->
          separator o f c b
            by exists x. ch x /\ not o x c so separator o f x c

  function fixpoint_above (o:'a -> 'a -> bool) (f:'a -> 'a) (u:'a) : 'a =
109
    sup o (tr_reach o f u)
110 111

  lemma fixpoint_max_proof : forall o f,u:'a.
112
    order o /\ q_chain_complete o /\ inflationary o f ->
113 114 115
    (forall x y. tr_reach o f u x /\ tr_reach o f u y ->
        separator o f x y && (o x y \/ o y x)) &&
      chain o (tr_reach o f u) && let y = fixpoint_above o f u in
116 117
      (maximum o (tr_reach o f u) y by tr_reach o f u u)
      && (f y = y by o (f y) y /\ o y (f y))
118 119 120 121

  lemma fixpoint_is_max_proof : forall o f,x y:'a.
    order o /\ inflationary o f /\ tr_reach o f x y /\ f y = y ->
    maximum o (tr_reach o f x) y
122 123 124
    by (forall o1 f1 x1 y1. o1 = o /\ f1 = f /\ x1 = x ->
      "induction" tr_reach o1 f1 x1 y1 -> o y1 y)
    by forall c x. supremum o c x /\ upper_bound o c y -> o x y
125 126

  predicate all_acc (o:'a -> 'a -> bool) (f:'a -> 'a) (x:'a) (y:'a) =
127 128 129 130 131
    forall z. tr_reach o f x z /\ o z y ->
      acc_on (lower o) (tr_reach o f x) z
  (*predicate all_not_in (o:'a -> 'a -> bool) (f:'a -> 'a) (x:'a)
                       (s:'a -> bool) (y:'a) =
    forall z. tr_reach o f x z /\ o z y -> not s z*)
132

133
  lemma tr_reach_wf : forall o f,x:'a.
134
    order o /\ inflationary o f ->
135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162
      let s = tr_reach o f x in
      wf_chain o s
      by (chain o s by forall x y. s x /\ s y -> o x y \/ o y x
        by separator o f x y) /\
        let lo = lower o in
        let a = all_acc o f x in
        wf_on lo s
      by (forall o1 f1 x1 y. o1 = o /\ f1 = f /\ x1 = x ->
        ("induction" tr_reach o1 f1 x1 y) -> a y)
      by (forall y. s y /\ a y -> a (f y)
        by forall z. s z /\ o z (f y) ->
          acc_on lo s z
        by "case_split" (o z y || (z = f y so
          forall z. s z /\ lo z (f y) -> acc_on lo s z
          by o z y by separator o f y z)) by separator o f y z)
      /\ forall c y. chain o c /\ c x /\
        (forall y. c y -> s y /\ a y) /\ supremum o c y -> a y
      by forall z. s z /\ lo z y -> acc_on lo s z
      by (exists t. c t /\ o z t) ||
         (false by upper_bound o c z
          by forall t. c t -> separator o f t z)

  lemma add_chain : forall o f x y c,z:'a.
    preorder o /\ inflationary o f /\ c y /\ chain o c /\
    (forall t. c t -> tr_reach o f x t) /\ supremum o c z /\
    tr_reach o f x y ->
    tr_reach o f x z by chain o (add c x) so supremum o (add c x) z
      by sext (upper_bound o (add c x)) (upper_bound o c)
163

164
  clone Iterates with
165 166 167 168 169 170 171 172 173 174 175 176 177
    function fixpoint_above = fixpoint_above,
    goal tr_reach_separated,
    goal tr_reach_maximum,
    goal tr_reach_fixpoint,
    goal tr_reach_compare,
    goal tr_reach_transitive,
    goal tr_reach_wf

end

module ChainExtensionCommon

  use import Iterates
178
  use import ho_set.Set
179 180 181 182 183
  use import order.Chain

  predicate ub_builder (o:'a -> 'a -> bool) (f:('a -> bool) -> 'a) =
    forall ch. chain o ch -> upper_bound o ch (f ch)

184 185 186
  function extends_ch (o:'a -> 'a -> bool) (f:('a -> bool) -> 'a)
                      (ch:'a -> bool) : 'a -> bool =
    if chain o ch then add ch (f ch) else ch
187 188 189 190 191 192 193 194 195

  predicate reach_ch (o:'a -> 'a -> bool) (f:('a -> bool) -> 'a)
                     (x y:'a -> bool) =
    tr_reach (subchain o) (extends_ch o f) x y

end


(* Special shape of iterates: chain extension.
196
   This module contain the machinery to build chain iterates. *)
197
module ChainExtension "W:non_conservative_extension:N"
198
                      (* => ChainExtensionProof *)
199

200
  use import order.SubChain
201 202 203 204 205
  use export ChainExtensionCommon

  axiom extends_inflationary : forall o:'a -> 'a -> bool,f.
    ub_builder o f -> inflationary (subchain o) (extends_ch o f)

206
  axiom extends_preserve_chains : forall o:'a -> 'a -> bool,f ch.
207
    ub_builder o f /\ chain o ch /\ reflexive o ->
208 209 210 211 212
    chain o (extends_ch o f ch)

  axiom extends_preserve_wf_chains : forall o:'a -> 'a -> bool,f ch.
    ub_builder o f /\ wf_chain o ch /\ reflexive o ->
    wf_chain o (extends_ch o f ch)
213 214 215 216 217

  axiom reach_only_chains : forall o:'a -> 'a -> bool,f ch1 ch2.
    ub_builder o f /\ chain o ch1 /\ reach_ch o f ch1 ch2 /\
    reflexive o -> chain o ch2

218 219 220 221 222 223 224 225 226
  axiom reach_only_wf_chains : forall o:'a -> 'a -> bool,f ch1 ch2.
    ub_builder o f /\ wf_chain o ch1 /\ reach_ch o f ch1 ch2 /\
    reflexive o -> wf_chain o ch2

  axiom reach_ch_interval : forall o:'a -> 'a -> bool,f ch1 chm ch2.
    ub_builder o f /\ reach_ch o f ch1 ch2 /\ order o /\
    subchain o ch1 chm /\ subchain o chm ch2 ->
    reach_ch o f ch1 chm

227 228 229 230
end

module ChainExtensionProof

231 232 233
  use import ho_set.SubsetOrder
  use import order.SubChain
  use import order.WfChain
234 235 236 237
  use import choice.Choice
  use import Iterates
  use import ChainExtensionCommon

238
  lemma extends_preserve_chains : forall o:'a -> 'a -> bool,f ch.
239 240 241
    ub_builder o f /\ chain o ch /\ reflexive o ->
    chain o (extends_ch o f ch)

242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262
  lemma extends_preserve_wf_chains : forall o:'a -> 'a -> bool,f ch.
    ub_builder o f /\ wf_chain o ch /\ reflexive o ->
    wf_chain o (extends_ch o f ch)
    by let nx = extends_ch o f ch in
      forall s2 y. s2 y /\ subset s2 nx ->
      (exists z. minimum o s2 z)
    by (chain o ch
      by let s2 = \x. ch x /\ exists y. ch y /\ not o x y /\ not o y x in
        not (exists y:'a. s2 y so subset s2 ch
        so exists u. minimum o s2 u
        so exists z. ch z /\ not o u z /\ o z u so s2 z)
        so (forall x y. ch x /\ ch y /\ not o x y /\ not o y x -> false
          by s2 x)
    ) so nx = add ch (f ch)
    so (exists z. s2 z /\ z <> f ch
      so let s3 = inter s2 ch in
        subset s3 ch /\ s3 z
      so exists z. minimum o s3 z
      so minimum o s2 z
    ) || (y = f ch so minimum o s2 y)

263 264 265 266
  lemma reach_only_chains : forall o f,ch1 ch2:'a -> bool.
    ub_builder o f /\ reflexive o /\ chain o ch1 /\ reach_ch o f ch1 ch2 ->
    chain o ch2
    by forall o1 f1 b1 x. o1 = o /\ f1 = f /\ b1 = ch1 ->
267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303
      ("induction" tr_reach (subchain o1) (extends_ch o1 f1) b1 x) ->
        chain o1 x

  lemma reach_only_wf_chains : forall o f,ch1 ch2:'a -> bool.
    ub_builder o f /\ reflexive o /\ wf_chain o ch1 /\ reach_ch o f ch1 ch2 ->
    wf_chain o ch2
    by forall o1 f1 b1 x. o1 = o /\ f1 = f /\ b1 = ch1 ->
      ("induction" tr_reach (subchain o1) (extends_ch o1 f1) b1 x) ->
        wf_chain o1 x

  lemma reach_ch_interval : forall o:'a -> 'a -> bool,f ch1 chm ch2.
    ub_builder o f /\ reach_ch o f ch1 ch2 /\ order o /\
    subchain o ch1 chm /\ subchain o chm ch2 ->
    not (not reach_ch o f ch1 chm
      so let sb = subchain o in
        let xt = extends_ch o f in
      (forall o1 f1 b1 ch0. o1 = sb /\ f1 = xt /\ b1 = ch1 ->
        ("induction" tr_reach o1 f1 b1 ch0) ->
        sb ch0 chm)
      by inflationary sb xt
      so (forall ch0. reach_ch o f ch1 ch0 /\ sb ch0 chm ->
          sb (xt ch0) chm
          by if sb (xt ch0) chm then true else
            xt ch0 = add ch0 (f ch0)
            so reach_ch o f ch1 (xt ch0)
            so (if sb (xt ch0) ch2 then true else
              false by separator sb xt ch0 ch2 so sb ch2 ch0
              so order sb so sb ch2 ch0)
            so (if not chm (f ch0) then true else
              false by subset (xt ch0) chm so
                forall a b. xt ch0 a /\ chm b /\ not xt ch0 b -> o a b)
            so sext ch0 chm
            by forall x. chm x -> if ch0 x then true else
              false by ch2 x so not xt ch0 x so xt ch0 (f ch0)
              so ch2 (f ch0) so o (f ch0) x so o x (f ch0))
        /\ (forall chh y. (forall x. chh x -> sb x chm) /\
          supremum sb chh y -> sb y chm by upper_bound sb chh chm))
304

305
  clone ChainExtension with
306
    goal extends_inflationary,
307 308 309 310 311
    goal extends_preserve_chains,
    goal extends_preserve_wf_chains,
    goal reach_only_chains,
    goal reach_only_wf_chains,
    goal reach_ch_interval
312 313

end