:: The Basic Properties of { \bf SCM } over Ring
:: by Artur Korni{\l}owicz
::
:: Received November 29, 1998
:: Copyright (c) 1998-2012 Association of Mizar Users


begin

definition
let R be Ring;
func SCM R ->  strict AMI-Struct over 2 means :Def1: :: SCMRING2:def 1
( the carrier of it = SCM-Memory & the ZeroF of it = NAT & the InstructionsF of it = SCM-Instr R & the Object-Kind of it = SCM-OK & the ValuesF of it = SCM-VAL R & the Execution of it = SCM-Exec R );
existence
 ex b1 being strict AMI-Struct over 2 st
( the carrier of b1 = SCM-Memory & the ZeroF of b1 = NAT & the InstructionsF of b1 = SCM-Instr R & the Object-Kind of b1 = SCM-OK & the ValuesF of b1 = SCM-VAL R & the Execution of b1 = SCM-Exec R )
proofend;
uniqueness
 for b1, b2 being strict AMI-Struct over 2 st the carrier of b1 = SCM-Memory & the ZeroF of b1 = NAT & the InstructionsF of b1 = SCM-Instr R & the Object-Kind of b1 = SCM-OK & the ValuesF of b1 = SCM-VAL R & the Execution of b1 = SCM-Exec R & the carrier of b2 = SCM-Memory & the ZeroF of b2 = NAT & the InstructionsF of b2 = SCM-Instr R & the Object-Kind of b2 = SCM-OK & the ValuesF of b2 = SCM-VAL R & the Execution of b2 = SCM-Exec R holds
b1 = b2 ;
end;

:: deftheorem Def1 defines SCM SCMRING2:def_1_:_
 for R being Ring
for b2 being strict AMI-Struct over 2 holds
( b2 = SCM R iff ( the carrier of b2 = SCM-Memory & the ZeroF of b2 = NAT & the InstructionsF of b2 = SCM-Instr R & the Object-Kind of b2 = SCM-OK & the ValuesF of b2 = SCM-VAL R & the Execution of b2 = SCM-Exec R ) );

registration
let R be Ring;
cluster SCM R ->  non empty strict ;
coherence
 not SCM R is empty by Def1;
end;

Lm1: now__::_thesis:_for_R_being_Ring_holds_the_Values_of_(SCM_R)_=_(SCM-VAL_R)_*_SCM-OK
let R be Ring; ::_thesis: the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK
thus  the_Values_of (SCM R) = the ValuesF of (SCM R) * the Object-Kind of (SCM R)
.= the ValuesF of (SCM R) * SCM-OK by Def1
.= (SCM-VAL R) * SCM-OK by Def1 ; ::_thesis: verum
end;

registration
let R be Ring;
cluster SCM R ->  with_non-empty_values strict ;
coherence
 SCM R is with_non-empty_values
proofend;
end;

Lm2:  for R being Ring holds the carrier of (SCM R) \ {NAT} = SCM-Data-Loc
proofend;

registration
let R be Ring;
cluster Int-like for Element of the carrier of (SCM R);
existence
 ex b1 being Object of (SCM R) st b1 is Int-like
proofend;
end;

definition
let R be Ring;
mode Data-Location of R is Int-like Object of (SCM R);
canceled;
end;

:: deftheorem  SCMRING2:def_2_:_
canceled;

theorem Th1: :: SCMRING2:1
for x being set
for R being Ring holds
( x is Data-Location of R iff x in Data-Locations ) by Def1, AMI_2:def_16, AMI_3:27;

definition
let R be Ring;
let s be State of (SCM R);
let a be Data-Location of R;
:: original:.
redefine funcs . a ->  Element of R;
coherence
 s . a is Element of R
proofend;
end;

theorem :: SCMRING2:2
for R being Ring holds [0,{},{}] is Instruction of (SCM R)
proofend;

theorem Th3: :: SCMRING2:3
for S being non empty 1-sorted
for x being set
for R being Ring
for d1, d2 being Data-Location of R st x in {1,2,3,4} holds
[x,{},<*d1,d2*>] in SCM-Instr S
proofend;

theorem Th4: :: SCMRING2:4
for S being non empty 1-sorted
for t being Element of S
for R being Ring
for d1 being Data-Location of R holds [5,{},<*d1,t*>] in SCM-Instr S
proofend;

theorem Th5: :: SCMRING2:5
for S being non empty 1-sorted
for i1 being Element of NAT holds [6,<*i1*>,{}] in SCM-Instr S by SCMRINGI:10;

theorem Th6: :: SCMRING2:6
for S being non empty 1-sorted
for R being Ring
for d1 being Data-Location of R
for i1 being Element of NAT holds [7,<*i1*>,<*d1*>] in SCM-Instr S
proofend;

definition
let R be Ring;
let a, b be Data-Location of R;
funca := b ->  Instruction of (SCM R) equals :: SCMRING2:def 3
[1,{},<*a,b*>];
coherence
 [1,{},<*a,b*>] is Instruction of (SCM R)
proofend;
func AddTo (a,b) ->  Instruction of (SCM R) equals :: SCMRING2:def 4
[2,{},<*a,b*>];
coherence
 [2,{},<*a,b*>] is Instruction of (SCM R)
proofend;
func SubFrom (a,b) ->  Instruction of (SCM R) equals :: SCMRING2:def 5
[3,{},<*a,b*>];
coherence
 [3,{},<*a,b*>] is Instruction of (SCM R)
proofend;
func MultBy (a,b) ->  Instruction of (SCM R) equals :: SCMRING2:def 6
[4,{},<*a,b*>];
coherence
 [4,{},<*a,b*>] is Instruction of (SCM R)
proofend;
end;

:: deftheorem  defines := SCMRING2:def_3_:_
 for R being Ring
for a, b being Data-Location of R holds a := b = [1,{},<*a,b*>];

:: deftheorem  defines AddTo SCMRING2:def_4_:_
 for R being Ring
for a, b being Data-Location of R holds AddTo (a,b) = [2,{},<*a,b*>];

:: deftheorem  defines SubFrom SCMRING2:def_5_:_
 for R being Ring
for a, b being Data-Location of R holds SubFrom (a,b) = [3,{},<*a,b*>];

:: deftheorem  defines MultBy SCMRING2:def_6_:_
 for R being Ring
for a, b being Data-Location of R holds MultBy (a,b) = [4,{},<*a,b*>];

definition
let R be Ring;
let a be Data-Location of R;
let r be Element of R;
funca := r ->  Instruction of (SCM R) equals :: SCMRING2:def 7
[5,{},<*a,r*>];
coherence
 [5,{},<*a,r*>] is Instruction of (SCM R)
proofend;
end;

:: deftheorem  defines := SCMRING2:def_7_:_
 for R being Ring
for a being Data-Location of R
for r being Element of R holds a := r = [5,{},<*a,r*>];

definition
let R be Ring;
let l be Element of NAT ;
func goto (l,R) ->  Instruction of (SCM R) equals :: SCMRING2:def 8
[6,<*l*>,{}];
coherence
 [6,<*l*>,{}] is Instruction of (SCM R)
proofend;
end;

:: deftheorem  defines goto SCMRING2:def_8_:_
 for R being Ring
for l being Element of NAT holds goto (l,R) = [6,<*l*>,{}];

definition
let R be Ring;
let l be Element of NAT ;
let a be Data-Location of R;
funca =0_goto l ->  Instruction of (SCM R) equals :: SCMRING2:def 9
[7,<*l*>,<*a*>];
coherence
 [7,<*l*>,<*a*>] is Instruction of (SCM R)
proofend;
end;

:: deftheorem  defines =0_goto SCMRING2:def_9_:_
 for R being Ring
for l being Element of NAT
for a being Data-Location of R holds a =0_goto l = [7,<*l*>,<*a*>];

theorem Th7: :: SCMRING2:7
for R being Ring
for I being set holds
( I is Instruction of (SCM R) iff ( I = [0,{},{}] or ex a, b being Data-Location of R st I = a := b or ex a, b being Data-Location of R st I = AddTo (a,b) or ex a, b being Data-Location of R st I = SubFrom (a,b) or ex a, b being Data-Location of R st I = MultBy (a,b) or ex i1 being Element of NAT st I = goto (i1,R) or ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st I = a := r ) )
proofend;

registration
let R be Ring;
cluster SCM R ->  IC-Ins-separated strict ;
coherence
 SCM R is IC-Ins-separated
proofend;
end;

theorem :: SCMRING2:8
for R being Ring holds IC = NAT by Def1;

theorem :: SCMRING2:9
for R being Ring
for s being State of (SCM R)
for S being SCM-State of R st S = s holds
IC s = IC S by Def1;

theorem Th10: :: SCMRING2:10
for R being Ring
for s being State of (SCM R)
for I being Instruction of (SCM R)
for i being Element of SCM-Instr R st i = I holds
for S being SCM-State of R st S = s holds
Exec (I,s) = SCM-Exec-Res (i,S)
proofend;

begin

theorem Th11: :: SCMRING2:11
for R being Ring
for a, b being Data-Location of R
for s being State of (SCM R) holds
( (Exec ((a := b),s)) . (IC ) = succ (IC s) &amp; (Exec ((a := b),s)) . a = s . b &amp; ( for c being Data-Location of R st c <> a holds
(Exec ((a := b),s)) . c = s . c ) )
proofend;

theorem Th12: :: SCMRING2:12
for R being Ring
for a, b being Data-Location of R
for s being State of (SCM R) holds
( (Exec ((AddTo (a,b)),s)) . (IC ) = succ (IC s) &amp; (Exec ((AddTo (a,b)),s)) . a = (s . a) + (s . b) &amp; ( for c being Data-Location of R st c <> a holds
(Exec ((AddTo (a,b)),s)) . c = s . c ) )
proofend;

theorem Th13: :: SCMRING2:13
for R being Ring
for a, b being Data-Location of R
for s being State of (SCM R) holds
( (Exec ((SubFrom (a,b)),s)) . (IC ) = succ (IC s) &amp; (Exec ((SubFrom (a,b)),s)) . a = (s . a) - (s . b) &amp; ( for c being Data-Location of R st c <> a holds
(Exec ((SubFrom (a,b)),s)) . c = s . c ) )
proofend;

theorem Th14: :: SCMRING2:14
for R being Ring
for a, b being Data-Location of R
for s being State of (SCM R) holds
( (Exec ((MultBy (a,b)),s)) . (IC ) = succ (IC s) &amp; (Exec ((MultBy (a,b)),s)) . a = (s . a) * (s . b) &amp; ( for c being Data-Location of R st c <> a holds
(Exec ((MultBy (a,b)),s)) . c = s . c ) )
proofend;

theorem :: SCMRING2:15
for R being Ring
for c being Data-Location of R
for i1 being Element of NAT
for s being State of (SCM R) holds
( (Exec ((goto (i1,R)),s)) . (IC ) = i1 &amp; (Exec ((goto (i1,R)),s)) . c = s . c )
proofend;

theorem Th16: :: SCMRING2:16
for R being Ring
for a, c being Data-Location of R
for i1 being Element of NAT
for s being State of (SCM R) holds
( ( s . a = 0. R implies (Exec ((a =0_goto i1),s)) . (IC ) = i1 ) &amp; ( s . a <> 0. R implies (Exec ((a =0_goto i1),s)) . (IC ) = succ (IC s) ) &amp; (Exec ((a =0_goto i1),s)) . c = s . c )
proofend;

theorem Th17: :: SCMRING2:17
for R being Ring
for r being Element of R
for a being Data-Location of R
for s being State of (SCM R) holds
( (Exec ((a := r),s)) . (IC ) = succ (IC s) &amp; (Exec ((a := r),s)) . a = r &amp; ( for c being Data-Location of R st c <> a holds
(Exec ((a := r),s)) . c = s . c ) )
proofend;

begin

theorem Th18: :: SCMRING2:18
for R being Ring
for I being Instruction of (SCM R) st ex s being State of (SCM R) st (Exec (I,s)) . (IC ) = succ (IC s) holds
not I is halting
proofend;

theorem Th19: :: SCMRING2:19
for R being Ring
for I being Instruction of (SCM R) st I = [0,{},{}] holds
I is halting
proofend;

Lm3:  for R being Ring
for a, b being Data-Location of R holds not a := b is halting
proofend;

Lm4:  for R being Ring
for a, b being Data-Location of R holds not AddTo (a,b) is halting
proofend;

Lm5:  for R being Ring
for a, b being Data-Location of R holds not SubFrom (a,b) is halting
proofend;

Lm6:  for R being Ring
for a, b being Data-Location of R holds not MultBy (a,b) is halting
proofend;

Lm7:  for R being Ring
for i1 being Element of NAT holds not goto (i1,R) is halting
proofend;

Lm8:  for R being Ring
for a being Data-Location of R
for i1 being Element of NAT holds not a =0_goto i1 is halting
proofend;

Lm9:  for R being Ring
for r being Element of R
for a being Data-Location of R holds not a := r is halting
proofend;

registration
let R be Ring;
let a, b be Data-Location of R;
clustera := b ->  non halting ;
coherence
 not a := b is halting by Lm3;
cluster AddTo (a,b) ->  non halting ;
coherence
 not AddTo (a,b) is halting by Lm4;
cluster SubFrom (a,b) ->  non halting ;
coherence
 not SubFrom (a,b) is halting by Lm5;
cluster MultBy (a,b) ->  non halting ;
coherence
 not MultBy (a,b) is halting by Lm6;
end;

registration
let R be Ring;
let i1 be Element of NAT ;
cluster goto (i1,R) ->  non halting ;
coherence
 not goto (i1,R) is halting by Lm7;
end;

registration
let R be Ring;
let a be Data-Location of R;
let i1 be Element of NAT ;
clustera =0_goto i1 ->  non halting ;
coherence
 not a =0_goto i1 is halting by Lm8;
end;

registration
let R be Ring;
let a be Data-Location of R;
let r be Element of R;
clustera := r ->  non halting ;
coherence
 not a := r is halting by Lm9;
end;

Lm10:  for R being Ring
for W being Instruction of (SCM R) st W is halting holds
W = [0,{},{}]
proofend;

registration
let R be Ring;
cluster SCM R ->  strict halting ;
coherence
 SCM R is halting
proofend;
end;

theorem :: SCMRING2:20
for R being Ring
for I being Instruction of (SCM R) st I is halting holds
I = halt (SCM R) by Lm10;

theorem :: SCMRING2:21
for R being Ring holds halt (SCM R) = [0,{},{}] ;

theorem Th22: :: SCMRING2:22
for R being Ring holds Data-Locations = Data-Locations
proofend;

theorem :: SCMRING2:23
for x being set
for R being Ring holds
( x is Data-Location of R iff x in Data-Locations )
proofend;

theorem :: SCMRING2:24
for R being Ring holds the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK by Lm1;

theorem :: SCMRING2:25
for R being Ring holds the carrier of (SCM R) \ {NAT} = SCM-Data-Loc by Lm2;