AMI_2: On a Mathematical Model of Programs

:: On a Mathematical Model of Programs
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received December 29, 1992
:: Copyright (c) 1992-2021 Association of Mizar Users

:: Na razie potrzebny w SCM_INST
::definition
:: func SCM-Data-Loc equals
:: [:{1},NAT:];
:: coherence;
::end;

definition

func SCM-Memory -> set equals :: AMI_2:def 1
{NAT} \/ SCM-Data-Loc;

end;

:: deftheorem defines SCM-Memory AMI_2:def 1 :

registration

cluster SCM-Memory -> non empty ;

end;

definition

:: original: SCM-Data-Loc
redefine func SCM-Data-Loc -> Subset of SCM-Memory;
coherence by XBOOLE_1:7;

end;

Lm1: now :: thesis:

let k be Element of SCM-Memory ; :: thesis:
( k in {NAT} or k in SCM-Data-Loc ) by XBOOLE_0:def 3;
hence ( k = NAT or k in SCM-Data-Loc ) by TARSKI:def 1; :: thesis:

end;

Lm2: not NAT in SCM-Data-Loc

proof end;

definition

::$CD 2

func SCM-OK -> Function of SCM-Memory,(Segm 2) means :Def2: :: AMI_2:def 4
for k being Element of SCM-Memory holds
( ( k = NAT implies it . k = 0 ) & ( k in SCM-Data-Loc implies it . k = 1 ) );

proof end;

proof end;

end;

:: deftheorem AMI_2:def 2 :

:: deftheorem AMI_2:def 3 :

:: deftheorem Def2 defines SCM-OK AMI_2:def 4 :

theorem :: AMI_2:1

canceled;

::$CT

definition

func SCM-VAL -> ManySortedSet of Segm 2 equals :: AMI_2:def 5
<%NAT,INT%>;

end;

:: deftheorem defines SCM-VAL AMI_2:def 5 :

Lm3: NAT in SCM-Memory

proof end;

theorem :: AMI_2:2

canceled;

theorem :: AMI_2:3

canceled;

theorem :: AMI_2:4

canceled;

theorem :: AMI_2:5

canceled;

::$CT 4

theorem Th1: :: AMI_2:6

(SCM-VAL * SCM-OK) . NAT = NAT

proof end;

theorem Th2: :: AMI_2:7

for i being Element of SCM-Memory st i in SCM-Data-Loc holds
(SCM-VAL * SCM-OK) . i = INT

proof end;

Lm4: dom SCM-OK = SCM-Memory
by PARTFUN1:def 2;

len <%NAT,INT%> = 2
by AFINSQ_1:38;

then rng SCM-OK c= dom SCM-VAL
by RELAT_1:def 19;

then Lm5: dom (SCM-VAL * SCM-OK) = SCM-Memory
by Lm4, RELAT_1:27;

registration

cluster SCM-OK * SCM-VAL -> non-empty ;

proof end;

end;

definition

mode SCM-State is Element of product (SCM-VAL * SCM-OK);

end;

theorem :: AMI_2:8

for a being Element of SCM-Data-Loc holds (SCM-VAL * SCM-OK) . a = INT by Th2;

theorem Th4: :: AMI_2:9

pi ((product (SCM-VAL * SCM-OK)),NAT) = NAT by Th1, Lm5, Lm3, CARD_3:12;

theorem Th5: :: AMI_2:10

for a being Element of SCM-Data-Loc holds pi ((product (SCM-VAL * SCM-OK)),a) = INT

proof end;

definition

let s be SCM-State;

func IC s -> Element of NAT equals :: AMI_2:def 6
s . NAT;

coherence by Th4, CARD_3:def 6;

end;

:: deftheorem defines IC AMI_2:def 6 :

definition

let s be SCM-State;
let u be natural Number ;

func SCM-Chg (s,u) -> SCM-State equals :: AMI_2:def 7
s +* (NAT .--> u);

proof end;

end;

:: deftheorem defines SCM-Chg AMI_2:def 7 :

theorem :: AMI_2:11

for s being SCM-State
for u being natural Number holds (SCM-Chg (s,u)) . NAT = u

proof end;

theorem :: AMI_2:12

for s being SCM-State
for u being natural Number
for mk being Element of SCM-Data-Loc holds (SCM-Chg (s,u)) . mk = s . mk

proof end;

theorem :: AMI_2:13

for s being SCM-State
for u, v being natural Number holds (SCM-Chg (s,u)) . v = s . v

proof end;

definition

let s be SCM-State;
let t be Element of SCM-Data-Loc ;
let u be Integer;

func SCM-Chg (s,t,u) -> SCM-State equals :: AMI_2:def 8
s +* (t .--> u);

proof end;

end;

:: deftheorem defines SCM-Chg AMI_2:def 8 :

theorem :: AMI_2:14

for s being SCM-State
for t being Element of SCM-Data-Loc
for u being Integer holds (SCM-Chg (s,t,u)) . NAT = s . NAT

proof end;

theorem :: AMI_2:15

for s being SCM-State
for t being Element of SCM-Data-Loc
for u being Integer holds (SCM-Chg (s,t,u)) . t = u

proof end;

theorem :: AMI_2:16

for s being SCM-State
for t being Element of SCM-Data-Loc
for u being Integer
for mk being Element of SCM-Data-Loc st mk <> t holds
(SCM-Chg (s,t,u)) . mk = s . mk

proof end;

registration

let s be SCM-State;
let a be Element of SCM-Data-Loc ;

cluster s . a -> integer ;

proof end;

end;

registration

let x, y be ExtReal;
let a, b be Nat;

cluster IFGT (x,y,a,b) -> natural ;

end;

definition

let x be Element of SCM-Instr ;
let s be SCM-State;

func SCM-Exec-Res (x,s) -> SCM-State equals :: AMI_2:def 14
SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),((IC s) + 1)) if ex mk, ml being Element of SCM-Data-Loc st x = [1,{},<*mk,ml*>]
SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) + (s . (x address_2))))),((IC s) + 1)) if ex mk, ml being Element of SCM-Data-Loc st x = [2,{},<*mk,ml*>]
SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) - (s . (x address_2))))),((IC s) + 1)) if ex mk, ml being Element of SCM-Data-Loc st x = [3,{},<*mk,ml*>]
SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) * (s . (x address_2))))),((IC s) + 1)) if ex mk, ml being Element of SCM-Data-Loc st x = [4,{},<*mk,ml*>]
SCM-Chg ((SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) div (s . (x address_2))))),(x address_2),((s . (x address_1)) mod (s . (x address_2))))),((IC s) + 1)) if ex mk, ml being Element of SCM-Data-Loc st x = [5,{},<*mk,ml*>]
SCM-Chg (s,(x jump_address)) if ex mk being Nat st x = [6,<*mk*>,{}]
SCM-Chg (s,(IFEQ ((s . (x cond_address)),0,(x cjump_address),((IC s) + 1)))) if ex mk being Nat ex ml being Element of SCM-Data-Loc st x = [7,<*mk*>,<*ml*>]
SCM-Chg (s,(IFGT ((s . (x cond_address)),0,(x cjump_address),((IC s) + 1)))) if ex mk being Nat ex ml being Element of SCM-Data-Loc st x = [8,<*mk*>,<*ml*>]
otherwise s;

consistency by XTUPLE_0:3;
coherence ;

end;

:: deftheorem AMI_2:def 9 :

:: deftheorem AMI_2:def 10 :

:: deftheorem AMI_2:def 11 :

:: deftheorem AMI_2:def 12 :

:: deftheorem AMI_2:def 13 :

:: deftheorem defines SCM-Exec-Res AMI_2:def 14 :

definition

func SCM-Exec -> Action of SCM-Instr,(product (SCM-VAL * SCM-OK)) means :: AMI_2:def 15
for x being Element of SCM-Instr
for y being SCM-State holds (it . x) . y = SCM-Exec-Res (x,y);

proof end;

proof end;

end;

:: deftheorem defines SCM-Exec AMI_2:def 15 :

theorem :: AMI_2:17

canceled;

theorem :: AMI_2:18

canceled;

theorem :: AMI_2:19

canceled;

:: missing, 2007.07.27, A.T.
::$CT 3

theorem :: AMI_2:20

not NAT in SCM-Data-Loc by Lm2;

:: missing, 2007.07.27, A.T.
::$CT 3

theorem :: AMI_2:21

canceled;

::$CT

theorem :: AMI_2:22

NAT in SCM-Memory by Lm3;

theorem :: AMI_2:23

for x being set st x in SCM-Data-Loc holds
ex k being Nat st x = [1,k]

proof end;

theorem :: AMI_2:24

for k being Nat holds [1,k] in SCM-Data-Loc

proof end;

theorem :: AMI_2:25

canceled;

::$CT

theorem :: AMI_2:26

for k being Element of SCM-Memory holds
( k = NAT or k in SCM-Data-Loc ) by Lm1;

theorem :: AMI_2:27

dom (SCM-VAL * SCM-OK) = SCM-Memory by Lm5;

theorem :: AMI_2:28

for s being SCM-State holds dom s = SCM-Memory by Lm5, CARD_3:9;

definition

let x be set ;

attr x is Int-like means :: AMI_2:def 16
x in SCM-Data-Loc ;

end;

:: deftheorem defines Int-like AMI_2:def 16 :

theorem :: AMI_2:29

for S being SCM-State holds S is SCM-Memory -defined total Function ;