prensani@13020: prensani@13020: header {* \section{Examples} *} prensani@13020: prensani@13020: theory RG_Examples = RG_Syntax: prensani@13020: prensani@13020: lemmas definitions [simp]= stable_def Pre_def Rely_def Guar_def Post_def Com_def prensani@13020: prensani@13020: subsection {* Set Elements of an Array to Zero *} prensani@13020: prensani@13020: lemma le_less_trans2: "\(j::nat) j\ \ i (a::nat) < c; b\d \ \ a + b < c + d" prensani@13020: by simp prensani@13020: prensani@13020: record Example1 = prensani@13020: A :: "nat list" prensani@13020: prensani@13020: lemma Example1: prensani@13020: "\ COBEGIN prensani@13020: SCHEME [0 \ i < n] prensani@13020: (\A := \A [i := 0], prensani@13020: \ n < length \A \, prensani@13020: \ length \A = length \A \ \A ! i = \A ! i \, prensani@13020: \ length \A = length \A \ (\j j \ \A ! j = \A ! j) \, prensani@13020: \ \A ! i = 0 \) prensani@13020: COEND prensani@13020: SAT [\ n < length \A \, \ \A = \A \, \ True \, \ \i < n. \A ! i = 0 \]" prensani@13020: apply(rule Parallel) prensani@13020: apply simp prensani@13020: apply clarify prensani@13020: apply simp prensani@13020: apply(erule disjE) prensani@13020: apply simp prensani@13020: apply clarify prensani@13020: apply simp prensani@13020: apply auto prensani@13020: apply(rule Basic) prensani@13020: apply auto prensani@13020: done prensani@13020: prensani@13020: lemma Example1_parameterized: prensani@13020: "k < t \ prensani@13020: \ COBEGIN prensani@13020: SCHEME [k*n\i<(Suc k)*n] (\A:=\A[i:=0], prensani@13020: \t*n < length \A\, prensani@13020: \t*n < length \A \ length \A=length \A \ \A!i = \A!i\, prensani@13020: \t*n < length \A \ length \A=length \A \ (\jA . i\j \ \A!j = \A!j)\, prensani@13020: \\A!i=0\) prensani@13020: COEND prensani@13020: SAT [\t*n < length \A\, prensani@13020: \t*n < length \A \ length \A=length \A \ (\iA!(k*n+i)=\A!(k*n+i))\, prensani@13020: \t*n < length \A \ length \A=length \A \ prensani@13020: (\iA . (i \A!i = \A!i) \ ((Suc k)*n \ i\ \A!i = \A!i))\, prensani@13020: \\iA!(k*n+i) = 0\]" prensani@13020: apply(rule Parallel) prensani@13020: apply simp prensani@13020: apply clarify prensani@13020: apply simp prensani@13020: apply(erule disjE) prensani@13020: apply clarify prensani@13020: apply simp prensani@13020: apply clarify prensani@13020: apply simp prensani@13020: apply clarify prensani@13020: apply simp prensani@13020: apply(erule_tac x="k*n +i" in allE) prensani@13020: apply(subgoal_tac "k*n+i COBEGIN prensani@13020: (\ \x:=\x+1;; \c_0:=\c_0 + 1 \, prensani@13020: \\x=\c_0 + \c_1 \ \c_0=0\, prensani@13020: \\c_0 = \c_0 \ prensani@13020: (\x=\c_0 + \c_1 prensani@13020: \ \x = \c_0 + \c_1)\, prensani@13020: \\c_1 = \c_1 \ prensani@13020: (\x=\c_0 + \c_1 prensani@13020: \ \x =\c_0 + \c_1)\, prensani@13020: \\x=\c_0 + \c_1 \ \c_0=1 \) prensani@13020: \ prensani@13020: (\ \x:=\x+1;; \c_1:=\c_1+1 \, prensani@13020: \\x=\c_0 + \c_1 \ \c_1=0 \, prensani@13020: \\c_1 = \c_1 \ prensani@13020: (\x=\c_0 + \c_1 prensani@13020: \ \x = \c_0 + \c_1)\, prensani@13020: \\c_0 = \c_0 \ prensani@13020: (\x=\c_0 + \c_1 prensani@13020: \ \x =\c_0 + \c_1)\, prensani@13020: \\x=\c_0 + \c_1 \ \c_1=1\) prensani@13020: COEND prensani@13020: SAT [\\x=0 \ \c_0=0 \ \c_1=0\, prensani@13020: \\x=\x \ \c_0= \c_0 \ \c_1=\c_1\, prensani@13020: \True\, prensani@13020: \\x=2\]" prensani@13020: apply(rule Parallel) prensani@13020: apply simp_all prensani@13020: apply clarify prensani@13020: apply(case_tac i) prensani@13020: apply simp prensani@13020: apply(erule disjE) prensani@13020: apply clarify prensani@13020: apply simp prensani@13020: apply clarify prensani@13020: apply simp prensani@13020: apply(case_tac j,simp) prensani@13020: apply simp prensani@13020: apply simp prensani@13020: apply(erule disjE) prensani@13020: apply clarify prensani@13020: apply simp prensani@13020: apply clarify prensani@13020: apply simp prensani@13020: apply(case_tac j,simp,simp) prensani@13020: apply clarify prensani@13020: apply(case_tac i,simp,simp) prensani@13020: apply clarify prensani@13020: apply simp prensani@13020: apply(erule_tac x=0 in all_dupE) prensani@13020: apply(erule_tac x=1 in allE,simp) prensani@13020: apply clarify prensani@13020: apply(case_tac i,simp) prensani@13020: apply(rule Await) prensani@13020: apply simp_all prensani@13020: apply(clarify) prensani@13020: apply(rule Seq) prensani@13020: prefer 2 prensani@13020: apply(rule Basic) prensani@13020: apply simp_all prensani@13020: apply(rule subset_refl) prensani@13020: apply(rule Basic) prensani@13020: apply simp_all prensani@13020: apply clarify prensani@13020: apply simp prensani@13020: apply(rule Await) prensani@13020: apply simp_all prensani@13020: apply(clarify) prensani@13020: apply(rule Seq) prensani@13020: prefer 2 prensani@13020: apply(rule Basic) prensani@13020: apply simp_all prensani@13020: apply(rule subset_refl) prensani@13020: apply(rule Basic) prensani@13020: apply simp_all prensani@13020: apply clarify prensani@13020: apply simp prensani@13020: done prensani@13020: prensani@13020: subsubsection {* Parameterized *} prensani@13020: prensani@13020: lemma Example2_lemma1: "j (\i b j = 0 " prensani@13020: apply(induct n) prensani@13020: apply simp_all prensani@13020: apply(force simp add: less_Suc_eq) prensani@13020: done prensani@13020: prensani@13020: lemma Example2_lemma2_aux: prensani@13020: "j (\iii s \ (\iij \ Suc (\i< n. b i)=(\i< n. (b (j:=1)) i)" prensani@13020: apply(frule_tac b="(b (j:=1))" in Example2_lemma2_aux) prensani@13020: apply(erule_tac t="Summation (b(j := 1)) n" in ssubst) prensani@13020: apply(frule_tac b=b in Example2_lemma2_aux) prensani@13020: apply(erule_tac t="Summation b n" in ssubst) prensani@13020: apply(subgoal_tac "Suc (Summation b j + b j + (\iij") prensani@13020: apply(drule_tac b="b" and t=1 in Example2_lemma2_aux2) prensani@13020: apply(rotate_tac -1) prensani@13020: apply(erule ssubst) prensani@13020: apply simp_all prensani@13020: done prensani@13020: prensani@13020: lemma Example2_lemma2_Suc0: "\j \ Suc (\i< n. b i)=(\i< n. (b (j:=Suc 0)) i)" prensani@13020: by(simp add:Example2_lemma2) prensani@13020: prensani@13020: lemma Example2_lemma3: "\i< n. b i = 1 \ (\i nat" prensani@13020: y :: nat prensani@13020: prensani@13020: lemma Example2_parameterized: "0 prensani@13020: \ COBEGIN SCHEME [0\i \y:=\y+1;; \C:=\C (i:=1) \, prensani@13020: \\y=(\iC i) \ \C i=0\, prensani@13020: \\C i = \C i \ prensani@13020: (\y=(\iC i) \ \y =(\iC i))\, prensani@13020: \(\jj \ \C j = \C j) \ prensani@13020: (\y=(\iC i) \ \y =(\iC i))\, prensani@13020: \\y=(\iC i) \ \C i=1\) prensani@13020: COEND prensani@13020: SAT [\\y=0 \ (\iC i)=0 \, \\C=\C \ \y=\y\, \True\, \\y=n\]" prensani@13020: apply(rule Parallel) prensani@13020: apply force prensani@13020: apply force prensani@13020: apply(force elim:Example2_lemma1) prensani@13020: apply clarify prensani@13020: apply simp prensani@13020: apply(force intro:Example2_lemma3) prensani@13020: apply clarify prensani@13020: apply simp prensani@13020: apply(rule Await) prensani@13020: apply simp_all prensani@13020: apply clarify prensani@13020: apply(rule Seq) prensani@13020: prefer 2 prensani@13020: apply(rule Basic) prensani@13020: apply(rule subset_refl) prensani@13020: apply simp+ prensani@13020: apply(rule Basic) prensani@13020: apply simp prensani@13020: apply clarify prensani@13020: apply simp prensani@13020: apply(force elim:Example2_lemma2_Suc0) prensani@13020: apply simp+ prensani@13020: done prensani@13020: prensani@13020: subsection {* Find Least Element *} prensani@13020: prensani@13020: text {* A previous lemma: *} prensani@13020: prensani@13020: lemma mod_aux :"\i < (n::nat); a mod n = i; j < a + n; j mod n = i; a < j\ \ False" prensani@13020: apply(subgoal_tac "a=a div n*n + a mod n" ) prensani@13020: prefer 2 apply (simp (no_asm_use) only: mod_div_equality [symmetric]) prensani@13020: apply(subgoal_tac "j=j div n*n + j mod n") prensani@13020: prefer 2 apply (simp (no_asm_use) only: mod_div_equality [symmetric]) prensani@13020: apply simp prensani@13020: apply(subgoal_tac "a div n*n < j div n*n") prensani@13020: prefer 2 apply arith prensani@13020: apply(subgoal_tac "j div n*n < (a div n + 1)*n") prensani@13020: prefer 2 apply simp prensani@13020: apply (simp only:mult_less_cancel2) prensani@13020: apply arith prensani@13020: done prensani@13020: prensani@13020: record Example3 = prensani@13020: X :: "nat \ nat" prensani@13020: Y :: "nat \ nat" prensani@13020: prensani@13020: lemma Example3: "m mod n=0 \ prensani@13020: \ COBEGIN prensani@13020: SCHEME [0\ijX i < \Y j) DO prensani@13020: IF P(B!(\X i)) THEN \Y:=\Y (i:=\X i) prensani@13020: ELSE \X:= \X (i:=(\X i)+ n) FI prensani@13020: OD, prensani@13020: \(\X i) mod n=i \ (\j<\X i. j mod n=i \ \P(B!j)) \ (\Y i P(B!(\Y i)) \ \Y i\ m+i)\, prensani@13020: \(\jj \ \Y j \ \Y j) \ \X i = \X i \ prensani@13020: \Y i = \Y i\, prensani@13020: \(\jj \ \X j = \X j \ \Y j = \Y j) \ prensani@13020: \Y i \ \Y i\, prensani@13020: \(\X i) mod n=i \ (\j<\X i. j mod n=i \ \P(B!j)) \ (\Y i P(B!(\Y i)) \ \Y i\ m+i) \ (\jY j \ \X i) \) prensani@13020: COEND prensani@13020: SAT [\ \iX i=i \ \Y i=m+i \,\\X=\X \ \Y=\Y\,\True\, prensani@13020: \\iX i) mod n=i \ (\j<\X i. j mod n=i \ \P(B!j)) \ prensani@13020: (\Y i P(B!(\Y i)) \ \Y i\ m+i) \ (\jY j \ \X i)\]" prensani@13020: apply(rule Parallel) prensani@13099: --{*5 subgoals left *} prensani@13020: apply force+ prensani@13020: apply clarify prensani@13020: apply simp prensani@13020: apply(rule While) prensani@13020: apply force prensani@13020: apply force prensani@13020: apply force prensani@13020: apply(rule_tac "pre'"="\ \X i mod n = i \ (\j. j<\X i \ j mod n = i \ \P(B!j)) \ (\Y i < n * q \ P (B!(\Y i))) \ \X i<\Y i\" in Conseq) prensani@13020: apply force prensani@13020: apply(rule subset_refl)+ prensani@13020: apply(rule Cond) prensani@13020: apply force prensani@13020: apply(rule Basic) prensani@13020: apply force prensani@13020: apply force prensani@13020: apply force prensani@13020: apply force prensani@13020: apply(rule Basic) prensani@13020: apply simp prensani@13020: apply clarify prensani@13020: apply simp prensani@13020: apply(case_tac "X x (j mod n)\ j") prensani@13020: apply(drule le_imp_less_or_eq) prensani@13020: apply(erule disjE) prensani@13020: apply(drule_tac j=j and n=n and i="j mod n" and a="X x (j mod n)" in mod_aux) prensani@13020: apply assumption+ prensani@13020: apply simp+ prensani@13020: apply(erule_tac x=j in allE) prensani@13020: apply force prensani@13020: apply simp prensani@13020: apply clarify prensani@13020: apply(rule conjI) prensani@13020: apply clarify prensani@13020: apply simp prensani@13020: apply(erule not_sym) prensani@13020: apply force prensani@13020: apply force+ prensani@13020: done prensani@13020: prensani@13020: text {* Same but with a list as auxiliary variable: *} prensani@13020: prensani@13020: record Example3_list = prensani@13020: X :: "nat list" prensani@13020: Y :: "nat list" prensani@13020: prensani@13020: lemma Example3_list: "m mod n=0 \ \ (COBEGIN SCHEME [0\ijX!i < \Y!j) DO prensani@13020: IF P(B!(\X!i)) THEN \Y:=\Y[i:=\X!i] ELSE \X:= \X[i:=(\X!i)+ n] FI prensani@13020: OD, prensani@13020: \nX \ nY \ (\X!i) mod n=i \ (\j<\X!i. j mod n=i \ \P(B!j)) \ (\Y!i P(B!(\Y!i)) \ \Y!i\ m+i)\, prensani@13020: \(\jj \ \Y!j \ \Y!j) \ \X!i = \X!i \ prensani@13020: \Y!i = \Y!i \ length \X = length \X \ length \Y = length \Y\, prensani@13020: \(\jj \ \X!j = \X!j \ \Y!j = \Y!j) \ prensani@13020: \Y!i \ \Y!i \ length \X = length \X \ length \Y = length \Y\, prensani@13020: \(\X!i) mod n=i \ (\j<\X!i. j mod n=i \ \P(B!j)) \ (\Y!i P(B!(\Y!i)) \ \Y!i\ m+i) \ (\jY!j \ \X!i) \) COEND) prensani@13020: SAT [\nX \ nY \ (\iX!i=i \ \Y!i=m+i) \, prensani@13020: \\X=\X \ \Y=\Y\, prensani@13020: \True\, prensani@13020: \\iX!i) mod n=i \ (\j<\X!i. j mod n=i \ \P(B!j)) \ prensani@13020: (\Y!i P(B!(\Y!i)) \ \Y!i\ m+i) \ (\jY!j \ \X!i)\]" prensani@13020: apply(rule Parallel) prensani@13099: --{* 5 subgoals left *} prensani@13020: apply force+ prensani@13020: apply clarify prensani@13020: apply simp prensani@13020: apply(rule While) prensani@13020: apply force prensani@13020: apply force prensani@13020: apply force prensani@13020: apply(rule_tac "pre'"="\nX \ nY \ \X ! i mod n = i \ (\j. j < \X ! i \ j mod n = i \ \ P (B ! j)) \ (\Y ! i < n * q \ P (B ! (\Y ! i))) \ \X!i<\Y!i\" in Conseq) prensani@13020: apply force prensani@13020: apply(rule subset_refl)+ prensani@13020: apply(rule Cond) prensani@13020: apply force prensani@13020: apply(rule Basic) prensani@13020: apply force prensani@13020: apply force prensani@13020: apply force prensani@13020: apply force prensani@13020: apply(rule Basic) prensani@13020: apply simp prensani@13020: apply clarify prensani@13020: apply simp prensani@13020: apply(rule allI) prensani@13020: apply(rule impI)+ prensani@13020: apply(case_tac "X x ! i\ j") prensani@13020: apply(drule le_imp_less_or_eq) prensani@13020: apply(erule disjE) prensani@13020: apply(drule_tac j=j and n=n and i=i and a="X x ! i" in mod_aux) prensani@13020: apply assumption+ prensani@13020: apply simp prensani@13020: apply force+ prensani@13020: done prensani@13020: prensani@13020: end