:: A Tree of Execution of a Macroinstruction
::  by Artur Korni{\l}owicz
::
:: Received December 10, 2003
:: Copyright (c) 2003 Association of Mizar Users

environ

 vocabularies AMISTD_3, AMI_1, TREES_2, GOBOARD5, AMI_3, RELAT_1, FINSET_1,
      FUNCT_1, AMISTD_1, SQUARE_1, WAYBEL_0, BOOLE, ORDINAL1, FINSEQ_1, CARD_1,
      CARD_3, ORDINAL2, ARYTM, PARTFUN1, TREES_1, TARSKI, WELLORD1, WELLORD2,
      AMISTD_2, FRECHET, FINSEQ_2, CAT_1, FUNCOP_1, MEMBERED, NAT_1;
 notations TARSKI, XBOOLE_0, SETFAM_1, ZFMISC_1, SUBSET_1, FINSET_1, CARD_1,
      NUMBERS, ORDINAL1, ORDINAL2, MEMBERED, SEQ_4, XXREAL_0, NAT_1, RELAT_1,
      FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, WELLORD1, WELLORD2, FUNCOP_1,
      FINSEQ_1, FINSEQ_2, TREES_1, TREES_2, STRUCT_0, AMI_1, AMI_3, AMISTD_1,
      AMISTD_2;
 constructors WELLORD1, PARTFUN1, WELLORD2, BINOP_1, ORDINAL2, XXREAL_0, NAT_1,
      ORDERS_1, FINSEQ_2, SEQ_4, REALSET1, TREES_2, AMI_5, AMISTD_2, ARYTM_3;
 registrations XBOOLE_0, RELAT_1, ORDINAL1, FUNCOP_1, ARYTM_3, FINSET_1,
      FRAENKEL, XXREAL_0, NAT_1, CARD_1, MEMBERED, FINSEQ_1, CARD_3, SEQ_4,
      REALSET1, CARD_4, TREES_2, CARD_5, FINSEQ_6, HEYTING2, NECKLACE, AMI_1,
      AMISTD_1, SETFAM_1;
 requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;


begin

:: Preliminaries

reserve x, y, z, X for set,
        m, n for natural number,
        O for Ordinal,
        R, S for Relation;

registration
  let D be set, f be PartFunc of D,NAT, n be set;
  cluster f.n -> natural;
end;

registration
  let R be empty Relation, X be set;
  cluster R|X -> empty;
end;

theorem :: AMISTD_3:1
  dom R = {x} & rng R = {y} implies R = x .--> y;

theorem :: AMISTD_3:2
  field {[x,x]} = {x};

registration
  let X be infinite set, a be set;
  cluster X --> a -> infinite;
end;

registration
  cluster infinite Function;
end;

registration
  let R be finite Relation;
  cluster field R -> finite;
end;

registration
  let R be infinite Relation;
  cluster field R -> infinite;
end;

registration
  cluster RelIncl {} -> empty;
end;

registration
  let X be non empty set;
  cluster RelIncl X -> non empty;
end;

canceled 2;

theorem :: AMISTD_3:5
  RelIncl {x} = {[x,x]};

theorem :: AMISTD_3:6
  RelIncl X c= [:X,X:];

registration
  let X be finite set;
  cluster RelIncl X -> finite;
end;

theorem :: AMISTD_3:7
  RelIncl X is finite implies X is finite;

registration
  let X be infinite set;
  cluster RelIncl X -> infinite;
end;

theorem :: AMISTD_3:8
    R,S are_isomorphic & R is well-ordering implies S is well-ordering;

theorem :: AMISTD_3:9
  R,S are_isomorphic & R is finite implies S is finite;

theorem :: AMISTD_3:10
  x .--> y is_isomorphism_of {[x,x]},{[y,y]};

theorem :: AMISTD_3:11
    {[x,x]}, {[y,y]} are_isomorphic;

registration
  cluster order_type_of {} -> empty;
end;

theorem :: AMISTD_3:12
    order_type_of RelIncl O = O;

theorem :: AMISTD_3:13
  for X being finite set st X c= O holds order_type_of RelIncl X = card X;

theorem :: AMISTD_3:14
  {x} c= O implies order_type_of RelIncl {x} = 1;

theorem :: AMISTD_3:15
  {x} c= O implies
  canonical_isomorphism_of (RelIncl order_type_of RelIncl {x}, RelIncl {x})
    = 0 .--> x;

registration
  let O be Ordinal,
      X be Subset of O,
      n be set;
  cluster canonical_isomorphism_of
              (RelIncl order_type_of RelIncl X,RelIncl X).n
          -> ordinal;
end;

registration
  let X be natural-membered set,
      n be set;
  cluster canonical_isomorphism_of
              (RelIncl order_type_of RelIncl X,RelIncl X).n
          -> natural;
end;

:: Trees

theorem :: AMISTD_3:16
  n |-> x = m |-> x implies n = m;

theorem :: AMISTD_3:17
  for T being Tree, t being Element of T holds t|Seg n in T;

theorem :: AMISTD_3:18
  for T1, T2 being Tree st
    for n being Element of NAT holds T1-level n = T2-level n holds
  T1 = T2;

definition
  func TrivialInfiniteTree equals
:: AMISTD_3:def 1
   { k |-> 0 where k is Element of NAT: not contradiction };
end;

registration
  cluster TrivialInfiniteTree -> non empty Tree-like;
end;

theorem :: AMISTD_3:19
  NAT,TrivialInfiniteTree are_equipotent;

registration
  cluster TrivialInfiniteTree -> infinite;
end;

theorem :: AMISTD_3:20
  for n being Element of NAT holds TrivialInfiniteTree-level n = { n |-> 0 };

:: First Location

reserve
  N for with_non-empty_elements set,
  S for standard (IC-Ins-separated definite
        (non empty non void AMI-Struct over N)),
  L, l1 for Instruction-Location of S,
  J for Instruction of S,
  F for Subset of the Instruction-Locations of S;

definition
  let N be with_non-empty_elements set;
  let S be standard (IC-Ins-separated definite
           (non empty non void AMI-Struct over N));
  let F be FinPartState of S such that
   F is non empty and
   F is programmed;
  func FirstLoc F -> Instruction-Location of S means
:: AMISTD_3:def 2
  ex M being non empty Subset of NAT st
     M = { locnum l where l is Instruction-Location of S
                        : l in dom F } &
     it = il.(S, min M);
end;

theorem :: AMISTD_3:21
  for F being non empty programmed FinPartState of S holds
   FirstLoc F in dom F;

theorem :: AMISTD_3:22
    for F, G being non empty programmed FinPartState of S st F c= G holds
   FirstLoc G <= FirstLoc F;

theorem :: AMISTD_3:23
  for F being non empty programmed FinPartState of S st l1 in dom F holds
   FirstLoc F <= l1;

theorem :: AMISTD_3:24
    for F being lower non empty programmed FinPartState of S holds
   FirstLoc F = il.(S,0);

:: LocNums

definition
 let N be with_non-empty_elements set,
     S be standard (IC-Ins-separated definite
          (non empty non void AMI-Struct over N)),
    F be Subset of the Instruction-Locations of S;
 func LocNums F -> Subset of NAT equals
:: AMISTD_3:def 3
   {locnum l where l is Instruction-Location of S : l in F};
end;

theorem :: AMISTD_3:25
  locnum l1 in LocNums F iff l1 in F;

registration
 let N be with_non-empty_elements set,
     S be standard (IC-Ins-separated definite
          (non empty non void AMI-Struct over N)),
     F be empty Subset of the Instruction-Locations of S;
 cluster LocNums F -> empty;
end;

registration
 let N be with_non-empty_elements set,
     S be standard (IC-Ins-separated definite
          (non empty non void AMI-Struct over N)),
     F be non empty Subset of the Instruction-Locations of S;
 cluster LocNums F -> non empty;
end;

theorem :: AMISTD_3:26
  F = {il.(S,n)} implies LocNums F = {n};

theorem :: AMISTD_3:27
  F, LocNums F are_equipotent;

theorem :: AMISTD_3:28
  Card F c= order_type_of RelIncl LocNums F;

theorem :: AMISTD_3:29
  S is realistic & J is halting implies LocNums NIC(J,L) = {locnum L};

theorem :: AMISTD_3:30
    S is realistic & J is sequential implies
   LocNums NIC(J,L) = {locnum NextLoc L};

:: LocSeq

definition
  let N be with_non-empty_elements set,
      S be standard (IC-Ins-separated definite
           (non empty non void AMI-Struct over N)),
      M be Subset of the Instruction-Locations of S;
  func LocSeq M -> T-Sequence of the Instruction-Locations of S means
:: AMISTD_3:def 4
   dom it = Card M &
   for m being set st m in Card M holds
    it.m = il.(S, canonical_isomorphism_of
                  (RelIncl order_type_of RelIncl LocNums M,
                   RelIncl LocNums M).m);
end;

theorem :: AMISTD_3:31
    F = {il.(S,n)} implies LocSeq F = 0 .--> il.(S,n);

registration
  let N be with_non-empty_elements set,
      S be standard (IC-Ins-separated definite
           (non empty non void AMI-Struct over N)),
      M be Subset of the Instruction-Locations of S;
  cluster LocSeq M -> one-to-one;
end;

:: Tree of Execution

definition
  let N be with_non-empty_elements set,
      S be standard (IC-Ins-separated definite
           (non empty non void AMI-Struct over N)),
      M be FinPartState of S;
  func ExecTree(M) -> IL-DecoratedTree of S means
:: AMISTD_3:def 5

  it.{} = FirstLoc(M) &
  for t being Element of dom it holds
    succ t = { t^<*k*> where k is Element of NAT:
    k in Card NIC(pi(M,it.t),it.t) } &
     for m being Element of NAT st m in Card NIC(pi(M,it.t),it.t) holds
      it.(t^<*m*>) = (LocSeq NIC(pi(M,it.t),it.t)).m;
end;

theorem :: AMISTD_3:32
    for S being standard halting realistic
        (IC-Ins-separated definite (non empty non void AMI-Struct over N))
  holds
  ExecTree Stop S = TrivialInfiniteTree --> il.(S,0);