The Mizar abstract of RELOC

Journal of Formalized Mathematics
Volume 6, 1994
University of Bialystok
Copyright (c) 1994 Association of Mizar Users
The abstract of the Mizar article:: Relocatability
by
Yasushi Tanaka
Received June 16, 1994
MML identifier: RELOC
[ Mizar article, MML identifier index ]
environ

 vocabulary AMI_1, AMI_3, ARYTM_1, CAT_1, QC_LANG1, AMI_2, AMI_5, RELAT_1,
      FUNCT_1, NAT_1, FINSET_1, ARYTM_3, FUNCT_4, BOOLE, CARD_3, PARTFUN1,
      RELOC;
 notation TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, XREAL_0, CARD_3, INT_1, NAT_1,
      RELAT_1, FUNCT_1, FUNCT_2, PARTFUN1, FUNCT_4, CQC_LANG, FINSET_1,
      STRUCT_0, AMI_1, AMI_2, AMI_3, BINARITH, AMI_5;
 constructors DOMAIN_1, BINARITH, AMI_5, MEMBERED, XBOOLE_0;
 clusters AMI_1, AMI_3, AMI_5, FUNCT_1, RELSET_1, INT_1, FRAENKEL, XBOOLE_0,
      MEMBERED, ZFMISC_1, NUMBERS, ORDINAL2;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;


begin  :: Relocatability

reserve j, k, m for Nat;

definition
let loc be Instruction-Location of SCM , k be Nat;
func loc + k -> Instruction-Location of SCM means
:: RELOC:def 1

ex m being Nat st loc = il.m & it = il.(m+k);

func loc -' k -> Instruction-Location of SCM means
:: RELOC:def 2

ex m being Nat st loc = il.m & it = il.(m -' k);
end;

theorem :: RELOC:1
 for loc being Instruction-Location of SCM ,k being Nat
  holds loc + k -' k = loc;

theorem :: RELOC:2
 for l1,l2 being Instruction-Location of SCM , k being Nat
  holds
    Start-At(l1 + k) = Start-At(l2 +k) iff Start-At l1 = Start-At l2;

theorem :: RELOC:3
 for l1,l2 being Instruction-Location of SCM , k being Nat
  st Start-At l1 = Start-At l2
  holds
    Start-At(l1 -' k) = Start-At(l2 -' k);

definition
  let I be Instruction of SCM , k be Nat;
  func IncAddr (I,k) -> Instruction of SCM equals
:: RELOC:def 3

   goto (((@I) jump_address )@ +k) if InsCode I = 6,
   ((@I) cond_address) @ =0_goto (((@I) cjump_address)@ +k)
       if InsCode I = 7,
   ((@I) cond_address) @ >0_goto (((@I) cjump_address)@ +k)
       if InsCode I = 8
  otherwise I;
end;

theorem :: RELOC:4
   for k being Nat holds IncAddr(halt SCM,k) = halt SCM;

theorem :: RELOC:5
  for k being Nat, a,b being Data-Location
   holds IncAddr(a:=b ,k) = a:=b;

theorem :: RELOC:6
  for k being Nat, a,b being Data-Location
   holds IncAddr(AddTo(a,b),k) = AddTo(a,b);

theorem :: RELOC:7
  for k being Nat, a,b being Data-Location
   holds IncAddr(SubFrom(a,b),k) = SubFrom(a,b);

theorem :: RELOC:8
  for k being Nat, a,b being Data-Location
   holds IncAddr(MultBy(a,b),k) = MultBy(a,b);

theorem :: RELOC:9
  for k being Nat, a,b being Data-Location
   holds IncAddr(Divide(a,b),k) = Divide(a,b);

theorem :: RELOC:10
  for k being Nat,loc being Instruction-Location of SCM
   holds IncAddr(goto loc,k) = goto (loc + k);

theorem :: RELOC:11
  for k being Nat,loc being Instruction-Location of SCM,
      a being Data-Location
   holds IncAddr(a=0_goto loc,k) = a=0_goto (loc + k);

theorem :: RELOC:12
  for k being Nat,loc being Instruction-Location of SCM,
      a being Data-Location
   holds IncAddr(a>0_goto loc,k) = a>0_goto (loc + k);

theorem :: RELOC:13
 for I being Instruction of SCM, k being Nat
  holds InsCode (IncAddr (I, k)) = InsCode I;

theorem :: RELOC:14
 for II, I being Instruction of SCM,
     k being Nat st
  (InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or
   InsCode I = 4 or InsCode I = 5) & IncAddr (II, k) = I holds II = I;

definition
 let p be programmed FinPartState of SCM , k be Nat;
 func Shift ( p , k ) -> programmed FinPartState of SCM means
:: RELOC:def 4

 dom it = { il.(m+k):il.m in dom p } &
 for m st il.m in dom p holds it.il.(m+k) = p.il.m;
end;


theorem :: RELOC:15
 for l being Instruction-Location of SCM , k being Nat,
     p being programmed FinPartState of SCM st l in dom p
   holds Shift(p,k).(l + k) = p.l;

theorem :: RELOC:16
   for p being programmed FinPartState of SCM, k being Nat
  holds dom Shift(p,k) =
         { il+k where il is Instruction-Location of SCM: il in dom p};

theorem :: RELOC:17
   for p being programmed FinPartState of SCM, k being Nat
 holds dom Shift(p,k) c= the Instruction-Locations of SCM;

definition
 let p be programmed FinPartState of SCM, k be Nat;
 func IncAddr ( p , k ) -> programmed FinPartState of SCM means
:: RELOC:def 5

 dom it = dom p &
 for m st il.m in dom p holds it.il.m = IncAddr(pi(p,il.m),k);
end;

theorem :: RELOC:18
  for p being programmed FinPartState of SCM , k being Nat
  for l being Instruction-Location of SCM st l in dom p
    holds IncAddr (p,k).l = IncAddr(pi(p,l),k);

theorem :: RELOC:19
 for i being Nat,
     p being programmed FinPartState of SCM
   holds
    Shift(IncAddr(p,i),i) = IncAddr(Shift(p,i),i);

definition
 let p be FinPartState of SCM , k be Nat;
 func Relocated ( p, k ) -> FinPartState of SCM equals
:: RELOC:def 6

 Start-At ((IC p)+k)+* IncAddr(Shift(ProgramPart(p),k),k)+*DataPart p;
end;

theorem :: RELOC:20
 for p being FinPartState of SCM
  holds dom IncAddr(Shift(ProgramPart(p),k),k) c= SCM-Instr-Loc;

theorem :: RELOC:21
 for p being FinPartState of SCM,k being Nat
  holds DataPart(Relocated(p,k)) = DataPart(p);

theorem :: RELOC:22
 for p being FinPartState of SCM,k being Nat
  holds ProgramPart(Relocated(p,k)) = IncAddr(Shift(ProgramPart(p),k),k);

theorem :: RELOC:23
 for p being FinPartState of SCM
 holds dom ProgramPart(Relocated(p,k))
           = { il.(j+k):il.j in dom ProgramPart(p) };

theorem :: RELOC:24
 for p being FinPartState of SCM, k being Nat,
     l being Instruction-Location of SCM
  holds l in dom p iff l+k in dom Relocated(p,k);

theorem :: RELOC:25
 for p being FinPartState of SCM , k being Nat
  holds IC SCM in dom Relocated (p,k);

theorem :: RELOC:26
 for p being FinPartState of SCM, k being Nat
  holds IC Relocated (p,k) = (IC p) + k;

theorem :: RELOC:27
 for p being FinPartState of SCM,
     k being Nat,
     loc being Instruction-Location of SCM,
     I being Instruction of SCM
  st loc in dom ProgramPart p & I = p.loc
  holds IncAddr(I, k) = (Relocated (p, k)).(loc + k);

theorem :: RELOC:28
 for p being FinPartState of SCM,k being Nat
  holds Start-At (IC p + k) c= Relocated (p,k);

theorem :: RELOC:29
 for s being data-only FinPartState of SCM,
     p being FinPartState of SCM,
     k being Nat st IC SCM in dom p
  holds
   Relocated((p +* s), k) = Relocated (p,k) +* s;

theorem :: RELOC:30
 for k being Nat,
     p being autonomic FinPartState of SCM ,
     s1, s2 being State of SCM
    st p c= s1 & Relocated (p,k) c= s2
  holds p c= s1 +* s2|SCM-Data-Loc;

theorem :: RELOC:31
 for s being State of SCM
  holds Exec(IncAddr(CurInstr s,k),s +* Start-At (IC s + k))
      = Following(s) +* Start-At (IC Following(s) + k);

theorem :: RELOC:32
 for INS being Instruction of SCM,
     s being State of SCM,
     p being FinPartState of SCM,
     i, j, k being Nat
  st IC s = il.(j+k)
 holds Exec(INS, s +* Start-At (IC s -' k))
     = Exec(IncAddr(INS, k), s) +* Start-At (IC Exec(IncAddr(INS,k), s) -' k);

begin :: Main theorems of Relocatability

theorem :: RELOC:33
   for k being Nat
 for p being autonomic FinPartState of SCM st IC SCM in dom p
 for s being State of SCM st
     p c= s
 for i being Nat
  holds (Computation (s +* Relocated (p,k))).i
       = (Computation s).i +* Start-At (IC (Computation s ).i + k)
        +* ProgramPart (Relocated (p,k));

theorem :: RELOC:34
 for k being Nat,
     p being autonomic FinPartState of SCM ,
     s1, s2, s3 being State of SCM
    st IC SCM in dom p & p c= s1 & Relocated (p,k) c= s2 &
       s3 = s1 +* s2|SCM-Data-Loc
    holds for i being Nat holds
     IC (Computation s1).i + k = IC (Computation s2).i &
     IncAddr(CurInstr((Computation s1).i), k) = CurInstr((Computation s2).i) &
     (Computation s1).i|dom (DataPart p)
          = (Computation s2).i|dom (DataPart (Relocated (p,k))) &
     (Computation s3).i|SCM-Data-Loc = (Computation s2).i|SCM-Data-Loc;

theorem :: RELOC:35
 for p being autonomic FinPartState of SCM ,
     k being Nat
  st IC SCM in dom p
  holds
  p is halting iff Relocated (p,k) is halting;

theorem :: RELOC:36
 for k being Nat
 for p being autonomic FinPartState of SCM st IC SCM in dom p
 for s being State of SCM st Relocated(p,k) c= s
  holds
  for i being Nat holds
    (Computation s).i
     = (Computation(s +* p)).i +* Start-At (IC(Computation(s +* p)).i + k)
       +* s|dom ProgramPart p +* ProgramPart (Relocated (p,k));

theorem :: RELOC:37
  for k being Nat
  for p being FinPartState of SCM st IC SCM in dom p
  for s being State of SCM st p c= s & Relocated(p,k) is autonomic
 holds
  for i being Nat holds
   (Computation s).i
    = (Computation(s +* Relocated(p,k))).i
      +* Start-At (IC(Computation(s +* Relocated(p,k))).i -' k)
      +* s|dom ProgramPart Relocated(p,k) +* ProgramPart (p);

theorem :: RELOC:38
 for p being FinPartState of SCM st IC SCM in dom p
 for k being Nat
   holds
  p is autonomic iff Relocated (p,k) is autonomic;

theorem :: RELOC:39
 for p being halting autonomic FinPartState of SCM st IC SCM in dom p
 for k being Nat holds
  DataPart(Result(p)) = DataPart(Result(Relocated(p,k)));

:: Relocatability

theorem :: RELOC:40
   for F being PartFunc of FinPartSt SCM, FinPartSt SCM,
     p being FinPartState of SCM st IC SCM in dom p & F is data-only
 for k being Nat
   holds
 p computes F iff Relocated ( p,k) computes F;
The abstract of the Mizar article:

Relocatability
