:: The { \bf for } (going up) Macro Instruction :: by Piotr Rudnicki :: :: Received June 4, 1998 :: Copyright (c) 1998-2021 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, SCMFSA6C, SCMFSA6B, FUNCT_1, XBOOLE_0, FUNCT_4, CARD_1, AMISTD_2, RELAT_1, GRAPHSP, AMI_3, PARTFUN1, COMPLEX1, SCMFSA8B, SCMFSA_9, ARYTM_3, CARD_3, SFMASTR1, ARYTM_1, AMISTD_1, XXREAL_0, SCMFSA6A, TARSKI, SCMFSA9A, FINSEQ_1, GRAPH_2, AOFA_I00, FUNCT_2, FINSEQ_2, SFMASTR3, NAT_1, COMPOS_1, MEMSTR_0, EXTPRO_1; notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, 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, SCMFSA8B, SCMFSA_9, SFMASTR1, SCMFSA9A, XXREAL_0, NAT_1, SCMFSA_M, SCMFSA_X, FINSEQ_6; 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, SCMFSA_X, PRE_POLY, SCMFSA10, COMPOS_2, AMISTD_2, AMI_3, SCMFSA8C, FINSEQ_6; registrations SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, FINSET_1, XREAL_0, NAT_1, INT_1, CARD_3, SCMFSA_2, SF_MASTR, SCMFSA6B, SCMFSA6C, SCMFSA7B, SCMFSA8A, SCMFSA8B, SCMFSA_9, SFMASTR1, VALUED_0, AFINSQ_1, COMPOS_1, EXTPRO_1, FUNCT_4, MEMSTR_0, AMI_3, SCMFSA_M, PRE_POLY, AMISTD_1, SCMFSA6A, SCMFSA8C, SCMFSA10, COMPOS_2, SCMFSA_X; requirements REAL, NUMERALS, 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 MacroInstruction of SCM+FSA, Ig for good MacroInstruction of SCM+FSA, i, k for Nat, p for Instruction-Sequence of SCM+FSA; ::$CT 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)/.|.s.bb.|; theorem :: SFMASTR3:6 :: see SCMFSA_2:99 Exec((f, aa) := bb, s).f = s.f+*(|.s.aa.|, s.bb); registration let a be read-write Int-Location, b be Int-Location, I, J be good MacroInstruction of SCM+FSA; cluster if>0(a, b, I, J) -> good; end; theorem :: SFMASTR3:7 for I,J being MacroInstruction of SCM+FSA holds UsedILoc if>0(aa, bb, I, J) = {aa, bb} \/ (UsedILoc I) \/ UsedILoc J; ::$CT theorem :: SFMASTR3:9 for I,J being really-closed MacroInstruction of SCM+FSA holds 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 MacroInstruction of SCM+FSA, s be State of SCM+FSA; func StepForUp(a, b, c, I, p,s) -> sequence of product the_Values_of SCM+FSA equals :: SFMASTR3:def 1 StepWhile>0(1-stRWNotIn ({a, b, c} \/ UsedILoc I), I ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, b, c} \/ UsedILoc I), intloc 0), p, s+*(1-stRWNotIn ({a, b, c} \/ UsedILoc 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 UsedILoc 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} \/ UsedILoc 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 MacroInstruction of SCM+FSA, s be State of SCM+FSA; pred ProperForUpBody a, b, c, I, s, p means :: SFMASTR3:def 2 for i being Nat st i < s.c-s.b+1 holds I is_halting_on StepForUp(a, b, c, I,p,s).i, p +* while>0(1-stRWNotIn ({a, b, c} \/ UsedILoc I), I ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, b, c} \/ UsedILoc I), intloc 0)); end; theorem :: SFMASTR3:17 for I being parahalting MacroInstruction of SCM+FSA holds ProperForUpBody aa, bb, cc, I, s, p; theorem :: SFMASTR3:18 for Ig being good really-closed MacroInstruction of SCM+FSA holds StepForUp(a,bb,cc,Ig,p,s).k.intloc 0 = 1 & Ig is_halting_on StepForUp(a,bb,cc,Ig,p,s).k, p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedILoc Ig), Ig ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedILoc Ig), intloc 0)) implies StepForUp(a,bb,cc,Ig,p,s).(k+1).intloc 0 = 1; theorem :: SFMASTR3:19 for Ig being good really-closed MacroInstruction of SCM+FSA holds 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} \/ UsedILoc Ig)) + k = s.cc-s.bb+1; theorem :: SFMASTR3:20 for Ig being good really-closed MacroInstruction of SCM+FSA holds 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} \/ UsedILoc Ig)) > 0 iff k < s.cc-s.bb+1; theorem :: SFMASTR3:21 for Ig being good really-closed MacroInstruction of SCM+FSA holds 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} \/ UsedILoc Ig \/ FinSeq-Locations) = IExec(Ig ";" AddTo(a, intloc 0), p +* while>0(1-stRWNotIn ({a, bb, cc} \/ UsedILoc Ig), Ig ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, bb, cc} \/ UsedILoc Ig), intloc 0)), StepForUp(a, bb, cc, Ig, p, s).k) | ({a, bb, cc} \/ UsedILoc Ig \/ FinSeq-Locations); definition let a, b, c be Int-Location, I be MacroInstruction of SCM+FSA; func for-up(a, b, c, I) -> MacroInstruction of SCM+FSA equals :: SFMASTR3:def 3 (1-stRWNotIn ({a, b, c} \/ UsedILoc I)) := c ";" SubFrom(1-stRWNotIn ({a, b, c} \/ UsedILoc I), b) ";" AddTo(1-stRWNotIn ({a, b, c} \/ UsedILoc I), intloc 0) ";" (a := b) ";" while>0( 1-stRWNotIn ({a, b, c} \/ UsedILoc I), I ";" AddTo(a, intloc 0) ";" SubFrom(1-stRWNotIn ({a, b, c} \/ UsedILoc I), intloc 0)); end; registration let a, b, c be Int-Location, I be really-closed MacroInstruction of SCM+FSA; cluster for-up(a, b, c, I) -> really-closed; end; reserve I for MacroInstruction of SCM+FSA; theorem :: SFMASTR3:22 {aa, bb, cc} \/ UsedILoc I c= UsedILoc for-up(aa, bb, cc, I); registration let a be read-write Int-Location, b, c be Int-Location, I be good MacroInstruction of SCM+FSA; cluster for-up(a, b, c, I) -> good; end; theorem :: SFMASTR3:23 a <> aa & aa <> 1-stRWNotIn ({a, bb, cc} \/ UsedILoc I) & I does not destroy aa implies for-up(a, bb, cc, I) does not destroy aa; theorem :: SFMASTR3:24 for I being really-closed MacroInstruction of SCM+FSA holds s.intloc 0 = 1 & s.bb > s.cc implies (for x st x <> a & x in {bb , cc} \/ UsedILoc 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 for Ig being good really-closed MacroInstruction of SCM+FSA holds 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 for Ig being good really-closed MacroInstruction of SCM+FSA holds s.intloc 0 = 1 & (ProperForUpBody a,bb,cc,Ig,s,p or Ig is parahalting) implies 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) -> MacroInstruction 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 really-closed; end; theorem :: SFMASTR3:27 c <> aa implies FinSeqMin(f, aa, bb, c) does not destroy aa; theorem :: SFMASTR3:28 {aa, bb, c} c= UsedILoc FinSeqMin(f, aa, bb, c); theorem :: SFMASTR3:29 s.intloc 0 = 1 implies 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, |.s.aa.|, |.s.bb.|); begin :: A swap macro instruction definition let f be FinSeq-Location, a, b be Int-Location; func swap(f, a, b) -> MacroInstruction 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= UsedILoc swap(f, aa, bb); theorem :: SFMASTR3:36 UsedI*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;