:: The { \bf for } (going up) Macro Instruction :: by Piotr Rudnicki :: :: Received June 4, 1998 :: Copyright (c) 1998-2012 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, FSM_1, SCMFSA_2, SF_MASTR, AMI_1, SCMFSA7B, SUBSET_1, UNIALG_2, SCMFSA6C, SCMFSA6B, FUNCT_1, XBOOLE_0, FUNCT_4, CARD_1, AMISTD_2, RELAT_1, GRAPHSP, AMI_3, PARTFUN1, COMPLEX1, SCMFSA8B, TURING_1, SCMFSA_9, ARYTM_3, FUNCOP_1, SCMFSA8A, CARD_3, SFMASTR1, ARYTM_1, XXREAL_0, SCMFSA6A, TARSKI, SCMFSA9A, FINSEQ_1, GRAPH_2, AOFA_I00, FUNCT_2, FINSEQ_2, SFMASTR3, NAT_1, PBOOLE, COMPOS_1, MEMSTR_0, EXTPRO_1; notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, NUMBERS, XCMPLX_0, CARD_3, INT_2, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4, FUNCT_7, PBOOLE, FUNCOP_1, GRAPH_2, FINSEQ_1, FINSEQ_2, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, AMISTD_1, SCMFSA_2, SCMFSA6A, SCMFSA6B, SF_MASTR, SCMFSA6C, SCMFSA7B, SCMFSA8A, SCMFSA8B, SCMFSA_9, SFMASTR1, SCMFSA9A, XXREAL_0, ORDINAL1, NAT_1, SCMFSA_M; constructors SETWISEO, REAL_1, INT_2, MESFUNC1, SCMFSA6A, SCMFSA6B, SCMFSA6C, SCMFSA8A, SCMFSA8B, SCMFSA_9, SFMASTR1, SCMFSA9A, RELSET_1, FUNCT_4, PBOOLE, GRAPH_2, SCMFSA7B, MEMSTR_0, AMISTD_1, FINSEQ_2, SCMFSA_M, SF_MASTR, FUNCT_7; registrations SUBSET_1, SETFAM_1, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, CARD_3, SCMFSA_2, SF_MASTR, SCMFSA6B, SCMFSA6C, SCMFSA7B, SCMFSA8A, SCMFSA8B, SCMFSA_9, SFMASTR1, XBOOLE_0, VALUED_0, AFINSQ_1, FUNCOP_1, COMPOS_1, EXTPRO_1, PBOOLE, FUNCT_4, MEMSTR_0, SCMFSA6A, FINSEQ_1, AMI_3, COMPOS_0, SCMFSA_M, PRE_POLY; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: SCM+FSA preliminaries reserve s for State of SCM+FSA, a, c for read-write Int-Location, aa, bb, cc, dd, x for Int-Location, f for FinSeq-Location, I, J for Program of SCM+FSA, Ig for good Program of SCM+FSA, i, k for Element of NAT, p for Instruction-Sequence of SCM+FSA; theorem :: SFMASTR3:1 I is_closed_on Initialized s,p & I is_halting_on Initialized s,p & I does not destroy aa implies IExec(I,p,s).aa = (Initialized s).aa; theorem :: SFMASTR3:2 s.intloc 0 = 1 implies DataPart IExec(Stop SCM+FSA,p,s) = DataPart s; theorem :: SFMASTR3:3 Stop SCM+FSA does not refer aa; theorem :: SFMASTR3:4 aa <> bb implies cc := bb does not refer aa; theorem :: SFMASTR3:5 :: change SCMFSA_2:98 Exec(a := (f, bb), s).a = (s.f)/.abs(s.bb); theorem :: SFMASTR3:6 :: see SCMFSA_2:99 Exec((f, aa) := bb, s).f = s.f+*(abs(s.aa), s.bb); registration let a be read-write Int-Location, b be Int-Location, I, J be good Program of SCM+FSA; cluster if>0(a, b, I, J) -> good; end; theorem :: SFMASTR3:7 UsedIntLoc if>0(aa, bb, I, J) = {aa, bb} \/ (UsedIntLoc I) \/ UsedIntLoc J; theorem :: SFMASTR3:8 I does not destroy aa implies while>0(bb, I) does not destroy aa; theorem :: SFMASTR3:9 cc <> aa & I does not destroy cc & J does not destroy cc implies if>0(aa, bb, I, J) does not destroy cc; begin :: The for-up macro instruction definition let p; let a, b, c be Int-Location, I be Program of SCM+FSA, s be State of SCM+FSA; func StepForUp(a, b, c, I, p,s) -> Function of NAT, product the_Values_of SCM+FSA equals :: SFMASTR3:def 1 StepWhile>0(1-stRWNotIn ({a, b, c} \/ UsedIntLoc I), I ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, b, c} \/ UsedIntLoc I), intloc 0), p, s+*(1-stRWNotIn ({a, b, c} \/ UsedIntLoc I), s.c-s.b+1)+*(a, s.b)); end; theorem :: SFMASTR3:10 s.intloc 0 = 1 implies StepForUp(a,bb,cc,I,p,s).0.intloc 0 = 1; theorem :: SFMASTR3:11 StepForUp(a,bb,cc,I,p,s).0.a = s.bb; theorem :: SFMASTR3:12 a <> bb implies StepForUp(a,bb,cc,I,p,s).0.bb = s.bb; theorem :: SFMASTR3:13 a <> cc implies StepForUp(a,bb,cc,I,p,s).0.cc = s.cc; theorem :: SFMASTR3:14 a <> dd & dd in UsedIntLoc I implies StepForUp(a,bb,cc,I,p,s). 0.dd = s.dd; theorem :: SFMASTR3:15 StepForUp(a,bb,cc,I,p,s).0.f = s.f; theorem :: SFMASTR3:16 s.intloc 0 = 1 implies for aux being read-write Int-Location st aux = 1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I) holds DataPart IExec( aux := cc ";" SubFrom(aux, bb) ";" AddTo(aux, intloc 0) ";" (a := bb),p,s) = DataPart(s+*(aux, s.cc-s.bb+1)+*(a, s.bb)); definition let p; let a, b, c be Int-Location, I be Program of SCM+FSA, s be State of SCM+FSA; pred ProperForUpBody a, b, c, I, s, p means :: SFMASTR3:def 2 for i being Element of NAT st i < s.c-s.b+1 holds I is_closed_on StepForUp(a, b, c, I,p,s).i, p +* while>0(1-stRWNotIn ({a, b, c} \/ UsedIntLoc I), I ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, b, c} \/ UsedIntLoc I), intloc 0)) & I is_halting_on StepForUp(a, b, c, I,p,s).i, p +* while>0(1-stRWNotIn ({a, b, c} \/ UsedIntLoc I), I ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, b, c} \/ UsedIntLoc I), intloc 0)); end; theorem :: SFMASTR3:17 for I being parahalting Program of SCM+FSA holds ProperForUpBody aa, bb, cc, I, s, p; theorem :: SFMASTR3:18 StepForUp(a,bb,cc,Ig,p,s).k.intloc 0 = 1 & Ig is_closed_on StepForUp(a,bb,cc,Ig,p,s).k, p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc Ig), Ig ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc Ig), intloc 0)) & Ig is_halting_on StepForUp(a,bb,cc,Ig,p,s).k, p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc Ig), Ig ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc Ig), intloc 0)) implies StepForUp(a,bb,cc,Ig,p,s).(k+1).intloc 0 = 1; theorem :: SFMASTR3:19 s.intloc 0 = 1 & ProperForUpBody a,bb,cc,Ig,s,p implies for k st k <= s.cc-s.bb+1 holds StepForUp(a,bb,cc,Ig,p,s).k.intloc 0 = 1 & (Ig does not destroy a implies StepForUp(a,bb,cc,Ig,p,s).k.a = k+s.bb & StepForUp(a, bb, cc, Ig,p, s).k.a <= s.cc+1) & StepForUp(a,bb,cc,Ig,p,s).k.(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc Ig)) + k = s.cc-s.bb+1; theorem :: SFMASTR3:20 s.intloc 0 = 1 & ProperForUpBody a,bb,cc,Ig,s,p implies for k holds StepForUp(a,bb,cc,Ig,p,s).k.(1-stRWNotIn({a, bb, cc} \/ UsedIntLoc Ig)) > 0 iff k < s.cc-s.bb+1; theorem :: SFMASTR3:21 s.intloc 0 = 1 & ProperForUpBody a,bb,cc,Ig,s,p & k < s.cc-s. bb+1 implies StepForUp(a,bb,cc,Ig,p,s).(k+1) | ({a, bb, cc} \/ UsedIntLoc Ig \/ FinSeq-Locations) = IExec(Ig ";" AddTo(a, intloc 0), p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc Ig), Ig ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc Ig), intloc 0)), StepForUp(a, bb, cc, Ig, p, s).k) | ({a, bb, cc} \/ UsedIntLoc Ig \/ FinSeq-Locations); definition let a, b, c be Int-Location, I be Program of SCM+FSA; func for-up(a, b, c, I) -> Program of SCM+FSA equals :: SFMASTR3:def 3 (1-stRWNotIn ({a, b, c} \/ UsedIntLoc I)) := c ";" SubFrom(1-stRWNotIn ({a, b, c} \/ UsedIntLoc I), b) ";" AddTo(1-stRWNotIn ({a, b, c} \/ UsedIntLoc I), intloc 0) ";" (a := b) ";" while>0( 1-stRWNotIn ({a, b, c} \/ UsedIntLoc I), I ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, b, c} \/ UsedIntLoc I), intloc 0) ); end; theorem :: SFMASTR3:22 {aa, bb, cc} \/ UsedIntLoc I c= UsedIntLoc for-up(aa, bb, cc, I); registration let a be read-write Int-Location, b, c be Int-Location, I be good Program of SCM+FSA; cluster for-up(a, b, c, I) -> good; end; theorem :: SFMASTR3:23 a <> aa & aa <> 1-stRWNotIn ({a, bb, cc} \/ UsedIntLoc I) & I does not destroy aa implies for-up(a, bb, cc, I) does not destroy aa; theorem :: SFMASTR3:24 s.intloc 0 = 1 & s.bb > s.cc implies (for x st x <> a & x in {bb , cc} \/ UsedIntLoc I holds IExec(for-up(a, bb, cc, I),p,s).x = s.x) & for f holds IExec(for-up(a, bb, cc, I),p,s).f = s.f; theorem :: SFMASTR3:25 s.intloc 0 = 1 & k = s.cc-s.bb+1 & (ProperForUpBody a, bb, cc, Ig, s,p or Ig is parahalting) implies DataPart IExec(for-up(a, bb, cc, Ig),p, s) = DataPart StepForUp(a,bb,cc,Ig,p,s).k; theorem :: SFMASTR3:26 s.intloc 0 = 1 & (ProperForUpBody a,bb,cc,Ig,s,p or Ig is parahalting) implies for-up(a, bb, cc, Ig) is_closed_on s,p & for-up(a, bb, cc, Ig) is_halting_on s,p; begin :: Finding minimum in a section of an array definition let start, finish, minpos be Int-Location, f be FinSeq-Location; func FinSeqMin(f, start, finish, minpos) -> Program of SCM+FSA equals :: SFMASTR3:def 4 minpos := start ";" for-up ( 3-rdRWNotIn {start, finish, minpos}, start, finish, (1 -stRWNotIn {start, finish, minpos}) := (f, 3-rdRWNotIn {start, finish, minpos}) ";" ((2-ndRWNotIn {start, finish, minpos}) := (f, minpos)) ";" if>0((2 -ndRWNotIn {start, finish, minpos}), (1-stRWNotIn {start, finish, minpos}), Macro (minpos := (3-rdRWNotIn {start, finish, minpos})), Stop SCM+FSA) ); end; :: set aux1 = 1-stRWNotIn {start, finish, min_pos}; :: set aux2 = 2-ndRWNotIn {start, finish, min_pos}; :: set cv = 3-rdRWNotIn {start, finish, min_pos}; registration let start, finish be Int-Location, minpos be read-write Int-Location, f be FinSeq-Location; cluster FinSeqMin(f, start, finish, minpos) -> good; end; theorem :: SFMASTR3:27 c <> aa implies FinSeqMin(f, aa, bb, c) does not destroy aa; theorem :: SFMASTR3:28 {aa, bb, c} c= UsedIntLoc FinSeqMin(f, aa, bb, c); theorem :: SFMASTR3:29 s.intloc 0 = 1 implies FinSeqMin(f, aa, bb, c) is_closed_on s,p & FinSeqMin(f, aa, bb, c) is_halting_on s,p; theorem :: SFMASTR3:30 aa <> c & bb <> c & s.intloc 0 = 1 implies IExec(FinSeqMin(f, aa, bb, c),p, s).f = s.f & IExec(FinSeqMin(f, aa, bb, c),p, s).aa = s.aa & IExec(FinSeqMin(f, aa, bb, c),p, s).bb = s.bb; theorem :: SFMASTR3:31 1 <= s.aa & s.aa <= s.bb & s.bb <= len (s.f) & aa <> c & bb <> c & s.intloc 0 = 1 implies IExec(FinSeqMin(f, aa, bb, c),p,s).c = min_at(s.f, abs(s.aa), abs(s.bb)); begin :: A swap macro instruction definition let f be FinSeq-Location, a, b be Int-Location; func swap(f, a, b) -> Program of SCM+FSA equals :: SFMASTR3:def 5 1-stRWNotIn {a, b} := (f,a) ";" (2-ndRWNotIn {a, b} := (f,b)) ";" ((f,a) := (2-ndRWNotIn {a, b})) ";" ((f,b ) := (1-stRWNotIn {a, b})); end; registration let f be FinSeq-Location, a, b be Int-Location; cluster swap(f, a, b) -> good parahalting; end; theorem :: SFMASTR3:32 cc <> 1-stRWNotIn {aa, bb} & cc <> 2-ndRWNotIn {aa, bb} implies swap(f, aa, bb) does not destroy cc; theorem :: SFMASTR3:33 1 <= s.aa & s.aa <= len (s.f) & 1 <= s.bb & s.bb <= len (s.f) & s.intloc 0 = 1 implies IExec(swap(f,aa,bb),p,s).f = s.f+*(s.aa, s.f.(s.bb))+*( s.bb, s.f.(s.aa)); theorem :: SFMASTR3:34 1 <= s.aa & s.aa <= len (s.f) & 1 <= s.bb & s.bb <= len (s.f) & s. intloc 0 = 1 implies IExec(swap(f,aa,bb),p,s).f.(s.aa) = s.f.(s.bb) & IExec(swap(f,aa,bb),p,s).f.(s.bb) = s.f.(s.aa); theorem :: SFMASTR3:35 {aa, bb} c= UsedIntLoc swap(f, aa, bb); theorem :: SFMASTR3:36 UsedInt*Loc swap(f, aa, bb) = {f}; begin :: Selection sort definition let f be FinSeq-Location; func Selection-sort f -> Program of SCM+FSA equals :: SFMASTR3:def 6 (1-stNotUsed swap(f, 1 -stRWNotIn {} Int-Locations, 2-ndRWNotIn {} Int-Locations)) :=len f ";" for-up ( 1-stRWNotIn {} Int-Locations, intloc 0, (1-stNotUsed swap(f, 1-stRWNotIn {} Int-Locations, 2-ndRWNotIn {} Int-Locations)), FinSeqMin(f, 1-stRWNotIn {} Int-Locations, (1-stNotUsed swap(f, 1-stRWNotIn {} Int-Locations, 2-ndRWNotIn {} Int-Locations)), 2-ndRWNotIn {} Int-Locations) ";" swap(f, 1-stRWNotIn {} Int-Locations, 2-ndRWNotIn {} Int-Locations) ); end; theorem :: SFMASTR3:37 for S being State of SCM+FSA st S = IExec(Selection-sort f,p,s) holds S.f is_non_decreasing_on 1, len (S.f) & ex p being Permutation of dom(s.f) st S.f = (s.f) * p;