src/HOL/HoareParallel/RG_Examples.thy
 author prensani Tue Mar 05 17:11:25 2002 +0100 (2002-03-05) changeset 13020 791e3b4c4039 child 13099 4bb592cdde0e permissions -rw-r--r--
HoareParallel Theories
 prensani@13020 ` 1` prensani@13020 ` 2` ```header {* \section{Examples} *} ``` prensani@13020 ` 3` prensani@13020 ` 4` ```theory RG_Examples = RG_Syntax: ``` prensani@13020 ` 5` prensani@13020 ` 6` ```lemmas definitions [simp]= stable_def Pre_def Rely_def Guar_def Post_def Com_def ``` prensani@13020 ` 7` prensani@13020 ` 8` ```subsection {* Set Elements of an Array to Zero *} ``` prensani@13020 ` 9` prensani@13020 ` 10` ```lemma le_less_trans2: "\(j::nat) j\ \ i (a::nat) < c; b\d \ \ a + b < c + d" ``` prensani@13020 ` 14` ```by simp ``` prensani@13020 ` 15` prensani@13020 ` 16` ```record Example1 = ``` prensani@13020 ` 17` ``` A :: "nat list" ``` prensani@13020 ` 18` prensani@13020 ` 19` ```lemma Example1: ``` prensani@13020 ` 20` ``` "\ COBEGIN ``` prensani@13020 ` 21` ``` SCHEME [0 \ i < n] ``` prensani@13020 ` 22` ``` (\A := \A [i := 0], ``` prensani@13020 ` 23` ``` \ n < length \A \, ``` prensani@13020 ` 24` ``` \ length \A = length \A \ \A ! i = \A ! i \, ``` prensani@13020 ` 25` ``` \ length \A = length \A \ (\j j \ \A ! j = \A ! j) \, ``` prensani@13020 ` 26` ``` \ \A ! i = 0 \) ``` prensani@13020 ` 27` ``` COEND ``` prensani@13020 ` 28` ``` SAT [\ n < length \A \, \ \A = \A \, \ True \, \ \i < n. \A ! i = 0 \]" ``` prensani@13020 ` 29` ```apply(rule Parallel) ``` prensani@13020 ` 30` ``` apply simp ``` prensani@13020 ` 31` ``` apply clarify ``` prensani@13020 ` 32` ``` apply simp ``` prensani@13020 ` 33` ``` apply(erule disjE) ``` prensani@13020 ` 34` ``` apply simp ``` prensani@13020 ` 35` ``` apply clarify ``` prensani@13020 ` 36` ``` apply simp ``` prensani@13020 ` 37` ``` apply auto ``` prensani@13020 ` 38` ```apply(rule Basic) ``` prensani@13020 ` 39` ```apply auto ``` prensani@13020 ` 40` ```done ``` prensani@13020 ` 41` prensani@13020 ` 42` ```lemma Example1_parameterized: ``` prensani@13020 ` 43` ```"k < t \ ``` prensani@13020 ` 44` ``` \ COBEGIN ``` prensani@13020 ` 45` ``` SCHEME [k*n\i<(Suc k)*n] (\A:=\A[i:=0], ``` prensani@13020 ` 46` ``` \t*n < length \A\, ``` prensani@13020 ` 47` ``` \t*n < length \A \ length \A=length \A \ \A!i = \A!i\, ``` prensani@13020 ` 48` ``` \t*n < length \A \ length \A=length \A \ (\jA . i\j \ \A!j = \A!j)\, ``` prensani@13020 ` 49` ``` \\A!i=0\) ``` prensani@13020 ` 50` ``` COEND ``` prensani@13020 ` 51` ``` SAT [\t*n < length \A\, ``` prensani@13020 ` 52` ``` \t*n < length \A \ length \A=length \A \ (\iA!(k*n+i)=\A!(k*n+i))\, ``` prensani@13020 ` 53` ``` \t*n < length \A \ length \A=length \A \ ``` prensani@13020 ` 54` ``` (\iA . (i \A!i = \A!i) \ ((Suc k)*n \ i\ \A!i = \A!i))\, ``` prensani@13020 ` 55` ``` \\iA!(k*n+i) = 0\]" ``` prensani@13020 ` 56` ```apply(rule Parallel) ``` prensani@13020 ` 57` ``` apply simp ``` prensani@13020 ` 58` ``` apply clarify ``` prensani@13020 ` 59` ``` apply simp ``` prensani@13020 ` 60` ``` apply(erule disjE) ``` prensani@13020 ` 61` ``` apply clarify ``` prensani@13020 ` 62` ``` apply simp ``` prensani@13020 ` 63` ``` apply clarify ``` prensani@13020 ` 64` ``` apply simp ``` prensani@13020 ` 65` ``` apply clarify ``` prensani@13020 ` 66` ``` apply simp ``` prensani@13020 ` 67` ``` apply(erule_tac x="k*n +i" in allE) ``` prensani@13020 ` 68` ``` apply(subgoal_tac "k*n+i COBEGIN ``` prensani@13020 ` 109` ``` (\ \x:=\x+1;; \c_0:=\c_0 + 1 \, ``` prensani@13020 ` 110` ``` \\x=\c_0 + \c_1 \ \c_0=0\, ``` prensani@13020 ` 111` ``` \\c_0 = \c_0 \ ``` prensani@13020 ` 112` ``` (\x=\c_0 + \c_1 ``` prensani@13020 ` 113` ``` \ \x = \c_0 + \c_1)\, ``` prensani@13020 ` 114` ``` \\c_1 = \c_1 \ ``` prensani@13020 ` 115` ``` (\x=\c_0 + \c_1 ``` prensani@13020 ` 116` ``` \ \x =\c_0 + \c_1)\, ``` prensani@13020 ` 117` ``` \\x=\c_0 + \c_1 \ \c_0=1 \) ``` prensani@13020 ` 118` ``` \ ``` prensani@13020 ` 119` ``` (\ \x:=\x+1;; \c_1:=\c_1+1 \, ``` prensani@13020 ` 120` ``` \\x=\c_0 + \c_1 \ \c_1=0 \, ``` prensani@13020 ` 121` ``` \\c_1 = \c_1 \ ``` prensani@13020 ` 122` ``` (\x=\c_0 + \c_1 ``` prensani@13020 ` 123` ``` \ \x = \c_0 + \c_1)\, ``` prensani@13020 ` 124` ``` \\c_0 = \c_0 \ ``` prensani@13020 ` 125` ``` (\x=\c_0 + \c_1 ``` prensani@13020 ` 126` ``` \ \x =\c_0 + \c_1)\, ``` prensani@13020 ` 127` ``` \\x=\c_0 + \c_1 \ \c_1=1\) ``` prensani@13020 ` 128` ``` COEND ``` prensani@13020 ` 129` ``` SAT [\\x=0 \ \c_0=0 \ \c_1=0\, ``` prensani@13020 ` 130` ``` \\x=\x \ \c_0= \c_0 \ \c_1=\c_1\, ``` prensani@13020 ` 131` ``` \True\, ``` prensani@13020 ` 132` ``` \\x=2\]" ``` prensani@13020 ` 133` ```apply(rule Parallel) ``` prensani@13020 ` 134` ``` apply simp_all ``` prensani@13020 ` 135` ``` apply clarify ``` prensani@13020 ` 136` ``` apply(case_tac i) ``` prensani@13020 ` 137` ``` apply simp ``` prensani@13020 ` 138` ``` apply(erule disjE) ``` prensani@13020 ` 139` ``` apply clarify ``` prensani@13020 ` 140` ``` apply simp ``` prensani@13020 ` 141` ``` apply clarify ``` prensani@13020 ` 142` ``` apply simp ``` prensani@13020 ` 143` ``` apply(case_tac j,simp) ``` prensani@13020 ` 144` ``` apply simp ``` prensani@13020 ` 145` ``` apply simp ``` prensani@13020 ` 146` ``` apply(erule disjE) ``` prensani@13020 ` 147` ``` apply clarify ``` prensani@13020 ` 148` ``` apply simp ``` prensani@13020 ` 149` ``` apply clarify ``` prensani@13020 ` 150` ``` apply simp ``` prensani@13020 ` 151` ``` apply(case_tac j,simp,simp) ``` prensani@13020 ` 152` ``` apply clarify ``` prensani@13020 ` 153` ``` apply(case_tac i,simp,simp) ``` prensani@13020 ` 154` ``` apply clarify ``` prensani@13020 ` 155` ``` apply simp ``` prensani@13020 ` 156` ``` apply(erule_tac x=0 in all_dupE) ``` prensani@13020 ` 157` ``` apply(erule_tac x=1 in allE,simp) ``` prensani@13020 ` 158` ```apply clarify ``` prensani@13020 ` 159` ```apply(case_tac i,simp) ``` prensani@13020 ` 160` ``` apply(rule Await) ``` prensani@13020 ` 161` ``` apply simp_all ``` prensani@13020 ` 162` ``` apply(clarify) ``` prensani@13020 ` 163` ``` apply(rule Seq) ``` prensani@13020 ` 164` ``` prefer 2 ``` prensani@13020 ` 165` ``` apply(rule Basic) ``` prensani@13020 ` 166` ``` apply simp_all ``` prensani@13020 ` 167` ``` apply(rule subset_refl) ``` prensani@13020 ` 168` ``` apply(rule Basic) ``` prensani@13020 ` 169` ``` apply simp_all ``` prensani@13020 ` 170` ``` apply clarify ``` prensani@13020 ` 171` ``` apply simp ``` prensani@13020 ` 172` ```apply(rule Await) ``` prensani@13020 ` 173` ``` apply simp_all ``` prensani@13020 ` 174` ```apply(clarify) ``` prensani@13020 ` 175` ```apply(rule Seq) ``` prensani@13020 ` 176` ``` prefer 2 ``` prensani@13020 ` 177` ``` apply(rule Basic) ``` prensani@13020 ` 178` ``` apply simp_all ``` prensani@13020 ` 179` ``` apply(rule subset_refl) ``` prensani@13020 ` 180` ```apply(rule Basic) ``` prensani@13020 ` 181` ```apply simp_all ``` prensani@13020 ` 182` ```apply clarify ``` prensani@13020 ` 183` ```apply simp ``` prensani@13020 ` 184` ```done ``` prensani@13020 ` 185` prensani@13020 ` 186` ```subsubsection {* Parameterized *} ``` prensani@13020 ` 187` prensani@13020 ` 188` ```lemma Example2_lemma1: "j (\i b j = 0 " ``` prensani@13020 ` 189` ```apply(induct n) ``` prensani@13020 ` 190` ``` apply simp_all ``` prensani@13020 ` 191` ```apply(force simp add: less_Suc_eq) ``` prensani@13020 ` 192` ```done ``` prensani@13020 ` 193` prensani@13020 ` 194` ```lemma Example2_lemma2_aux: ``` prensani@13020 ` 195` ``` "j (\iii s \ (\iij \ Suc (\i< n. b i)=(\i< n. (b (j:=1)) i)" ``` prensani@13020 ` 211` ```apply(frule_tac b="(b (j:=1))" in Example2_lemma2_aux) ``` prensani@13020 ` 212` ```apply(erule_tac t="Summation (b(j := 1)) n" in ssubst) ``` prensani@13020 ` 213` ```apply(frule_tac b=b in Example2_lemma2_aux) ``` prensani@13020 ` 214` ```apply(erule_tac t="Summation b n" in ssubst) ``` prensani@13020 ` 215` ```apply(subgoal_tac "Suc (Summation b j + b j + (\iij") ``` prensani@13020 ` 219` ``` apply(drule_tac b="b" and t=1 in Example2_lemma2_aux2) ``` prensani@13020 ` 220` ``` apply(rotate_tac -1) ``` prensani@13020 ` 221` ``` apply(erule ssubst) ``` prensani@13020 ` 222` ```apply simp_all ``` prensani@13020 ` 223` ```done ``` prensani@13020 ` 224` prensani@13020 ` 225` ```lemma Example2_lemma2_Suc0: "\j \ Suc (\i< n. b i)=(\i< n. (b (j:=Suc 0)) i)" ``` prensani@13020 ` 226` ```by(simp add:Example2_lemma2) ``` prensani@13020 ` 227` prensani@13020 ` 228` ```lemma Example2_lemma3: "\i< n. b i = 1 \ (\i nat" ``` prensani@13020 ` 235` ``` y :: nat ``` prensani@13020 ` 236` prensani@13020 ` 237` ```lemma Example2_parameterized: "0 ``` prensani@13020 ` 238` ``` \ COBEGIN SCHEME [0\i \y:=\y+1;; \C:=\C (i:=1) \, ``` prensani@13020 ` 240` ``` \\y=(\iC i) \ \C i=0\, ``` prensani@13020 ` 241` ``` \\C i = \C i \ ``` prensani@13020 ` 242` ``` (\y=(\iC i) \ \y =(\iC i))\, ``` prensani@13020 ` 243` ``` \(\jj \ \C j = \C j) \ ``` prensani@13020 ` 244` ``` (\y=(\iC i) \ \y =(\iC i))\, ``` prensani@13020 ` 245` ``` \\y=(\iC i) \ \C i=1\) ``` prensani@13020 ` 246` ``` COEND ``` prensani@13020 ` 247` ``` SAT [\\y=0 \ (\iC i)=0 \, \\C=\C \ \y=\y\, \True\, \\y=n\]" ``` prensani@13020 ` 248` ```apply(rule Parallel) ``` prensani@13020 ` 249` ```apply force ``` prensani@13020 ` 250` ```apply force ``` prensani@13020 ` 251` ```apply(force elim:Example2_lemma1) ``` prensani@13020 ` 252` ```apply clarify ``` prensani@13020 ` 253` ```apply simp ``` prensani@13020 ` 254` ```apply(force intro:Example2_lemma3) ``` prensani@13020 ` 255` ```apply clarify ``` prensani@13020 ` 256` ```apply simp ``` prensani@13020 ` 257` ```apply(rule Await) ``` prensani@13020 ` 258` ```apply simp_all ``` prensani@13020 ` 259` ```apply clarify ``` prensani@13020 ` 260` ```apply(rule Seq) ``` prensani@13020 ` 261` ```prefer 2 ``` prensani@13020 ` 262` ```apply(rule Basic) ``` prensani@13020 ` 263` ```apply(rule subset_refl) ``` prensani@13020 ` 264` ```apply simp+ ``` prensani@13020 ` 265` ```apply(rule Basic) ``` prensani@13020 ` 266` ```apply simp ``` prensani@13020 ` 267` ```apply clarify ``` prensani@13020 ` 268` ```apply simp ``` prensani@13020 ` 269` ```apply(force elim:Example2_lemma2_Suc0) ``` prensani@13020 ` 270` ```apply simp+ ``` prensani@13020 ` 271` ```done ``` prensani@13020 ` 272` prensani@13020 ` 273` ```subsection {* Find Least Element *} ``` prensani@13020 ` 274` prensani@13020 ` 275` ```text {* A previous lemma: *} ``` prensani@13020 ` 276` prensani@13020 ` 277` ```lemma mod_aux :"\i < (n::nat); a mod n = i; j < a + n; j mod n = i; a < j\ \ False" ``` prensani@13020 ` 278` ```apply(subgoal_tac "a=a div n*n + a mod n" ) ``` prensani@13020 ` 279` ``` prefer 2 apply (simp (no_asm_use) only: mod_div_equality [symmetric]) ``` prensani@13020 ` 280` ```apply(subgoal_tac "j=j div n*n + j mod n") ``` prensani@13020 ` 281` ``` prefer 2 apply (simp (no_asm_use) only: mod_div_equality [symmetric]) ``` prensani@13020 ` 282` ```apply simp ``` prensani@13020 ` 283` ```apply(subgoal_tac "a div n*n < j div n*n") ``` prensani@13020 ` 284` ```prefer 2 apply arith ``` prensani@13020 ` 285` ```apply(subgoal_tac "j div n*n < (a div n + 1)*n") ``` prensani@13020 ` 286` ```prefer 2 apply simp ``` prensani@13020 ` 287` ```apply (simp only:mult_less_cancel2) ``` prensani@13020 ` 288` ```apply arith ``` prensani@13020 ` 289` ```done ``` prensani@13020 ` 290` prensani@13020 ` 291` ```record Example3 = ``` prensani@13020 ` 292` ``` X :: "nat \ nat" ``` prensani@13020 ` 293` ``` Y :: "nat \ nat" ``` prensani@13020 ` 294` prensani@13020 ` 295` ```lemma Example3: "m mod n=0 \ ``` prensani@13020 ` 296` ``` \ COBEGIN ``` prensani@13020 ` 297` ``` SCHEME [0\ijX i < \Y j) DO ``` prensani@13020 ` 299` ``` IF P(B!(\X i)) THEN \Y:=\Y (i:=\X i) ``` prensani@13020 ` 300` ``` ELSE \X:= \X (i:=(\X i)+ n) FI ``` prensani@13020 ` 301` ``` OD, ``` prensani@13020 ` 302` ``` \(\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 ` 303` ``` \(\jj \ \Y j \ \Y j) \ \X i = \X i \ ``` prensani@13020 ` 304` ``` \Y i = \Y i\, ``` prensani@13020 ` 305` ``` \(\jj \ \X j = \X j \ \Y j = \Y j) \ ``` prensani@13020 ` 306` ``` \Y i \ \Y i\, ``` prensani@13020 ` 307` ``` \(\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 ` 308` ``` COEND ``` prensani@13020 ` 309` ``` SAT [\ \iX i=i \ \Y i=m+i \,\\X=\X \ \Y=\Y\,\True\, ``` prensani@13020 ` 310` ``` \\iX i) mod n=i \ (\j<\X i. j mod n=i \ \P(B!j)) \ ``` prensani@13020 ` 311` ``` (\Y i P(B!(\Y i)) \ \Y i\ m+i) \ (\jY j \ \X i)\]" ``` prensani@13020 ` 312` ```apply(rule Parallel) ``` prensani@13020 ` 313` ```(*5*) ``` prensani@13020 ` 314` ```apply force+ ``` prensani@13020 ` 315` ```apply clarify ``` prensani@13020 ` 316` ```apply simp ``` prensani@13020 ` 317` ```apply(rule While) ``` prensani@13020 ` 318` ``` apply force ``` prensani@13020 ` 319` ``` apply force ``` prensani@13020 ` 320` ``` apply force ``` prensani@13020 ` 321` ``` 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 ` 322` ``` apply force ``` prensani@13020 ` 323` ``` apply(rule subset_refl)+ ``` prensani@13020 ` 324` ``` apply(rule Cond) ``` prensani@13020 ` 325` ``` apply force ``` prensani@13020 ` 326` ``` apply(rule Basic) ``` prensani@13020 ` 327` ``` apply force ``` prensani@13020 ` 328` ``` apply force ``` prensani@13020 ` 329` ``` apply force ``` prensani@13020 ` 330` ``` apply force ``` prensani@13020 ` 331` ``` apply(rule Basic) ``` prensani@13020 ` 332` ``` apply simp ``` prensani@13020 ` 333` ``` apply clarify ``` prensani@13020 ` 334` ``` apply simp ``` prensani@13020 ` 335` ``` apply(case_tac "X x (j mod n)\ j") ``` prensani@13020 ` 336` ``` apply(drule le_imp_less_or_eq) ``` prensani@13020 ` 337` ``` apply(erule disjE) ``` prensani@13020 ` 338` ``` 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 ` 339` ``` apply assumption+ ``` prensani@13020 ` 340` ``` apply simp+ ``` prensani@13020 ` 341` ``` apply(erule_tac x=j in allE) ``` prensani@13020 ` 342` ``` apply force ``` prensani@13020 ` 343` ``` apply simp ``` prensani@13020 ` 344` ``` apply clarify ``` prensani@13020 ` 345` ``` apply(rule conjI) ``` prensani@13020 ` 346` ``` apply clarify ``` prensani@13020 ` 347` ``` apply simp ``` prensani@13020 ` 348` ``` apply(erule not_sym) ``` prensani@13020 ` 349` ``` apply force ``` prensani@13020 ` 350` ```apply force+ ``` prensani@13020 ` 351` ```done ``` prensani@13020 ` 352` prensani@13020 ` 353` ```text {* Same but with a list as auxiliary variable: *} ``` prensani@13020 ` 354` prensani@13020 ` 355` ```record Example3_list = ``` prensani@13020 ` 356` ``` X :: "nat list" ``` prensani@13020 ` 357` ``` Y :: "nat list" ``` prensani@13020 ` 358` prensani@13020 ` 359` ```lemma Example3_list: "m mod n=0 \ \ (COBEGIN SCHEME [0\ijX!i < \Y!j) DO ``` prensani@13020 ` 361` ``` IF P(B!(\X!i)) THEN \Y:=\Y[i:=\X!i] ELSE \X:= \X[i:=(\X!i)+ n] FI ``` prensani@13020 ` 362` ``` OD, ``` prensani@13020 ` 363` ``` \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 ` 364` ``` \(\jj \ \Y!j \ \Y!j) \ \X!i = \X!i \ ``` prensani@13020 ` 365` ``` \Y!i = \Y!i \ length \X = length \X \ length \Y = length \Y\, ``` prensani@13020 ` 366` ``` \(\jj \ \X!j = \X!j \ \Y!j = \Y!j) \ ``` prensani@13020 ` 367` ``` \Y!i \ \Y!i \ length \X = length \X \ length \Y = length \Y\, ``` prensani@13020 ` 368` ``` \(\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 ` 369` ``` SAT [\nX \ nY \ (\iX!i=i \ \Y!i=m+i) \, ``` prensani@13020 ` 370` ``` \\X=\X \ \Y=\Y\, ``` prensani@13020 ` 371` ``` \True\, ``` prensani@13020 ` 372` ``` \\iX!i) mod n=i \ (\j<\X!i. j mod n=i \ \P(B!j)) \ ``` prensani@13020 ` 373` ``` (\Y!i P(B!(\Y!i)) \ \Y!i\ m+i) \ (\jY!j \ \X!i)\]" ``` prensani@13020 ` 374` ```apply(rule Parallel) ``` prensani@13020 ` 375` ```(*5*) ``` prensani@13020 ` 376` ```apply force+ ``` prensani@13020 ` 377` ```apply clarify ``` prensani@13020 ` 378` ```apply simp ``` prensani@13020 ` 379` ```apply(rule While) ``` prensani@13020 ` 380` ``` apply force ``` prensani@13020 ` 381` ``` apply force ``` prensani@13020 ` 382` ``` apply force ``` prensani@13020 ` 383` ``` 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 ` 384` ``` apply force ``` prensani@13020 ` 385` ``` apply(rule subset_refl)+ ``` prensani@13020 ` 386` ``` apply(rule Cond) ``` prensani@13020 ` 387` ``` apply force ``` prensani@13020 ` 388` ``` apply(rule Basic) ``` prensani@13020 ` 389` ``` apply force ``` prensani@13020 ` 390` ``` apply force ``` prensani@13020 ` 391` ``` apply force ``` prensani@13020 ` 392` ``` apply force ``` prensani@13020 ` 393` ``` apply(rule Basic) ``` prensani@13020 ` 394` ``` apply simp ``` prensani@13020 ` 395` ``` apply clarify ``` prensani@13020 ` 396` ``` apply simp ``` prensani@13020 ` 397` ``` apply(rule allI) ``` prensani@13020 ` 398` ``` apply(rule impI)+ ``` prensani@13020 ` 399` ``` apply(case_tac "X x ! i\ j") ``` prensani@13020 ` 400` ``` apply(drule le_imp_less_or_eq) ``` prensani@13020 ` 401` ``` apply(erule disjE) ``` prensani@13020 ` 402` ``` apply(drule_tac j=j and n=n and i=i and a="X x ! i" in mod_aux) ``` prensani@13020 ` 403` ``` apply assumption+ ``` prensani@13020 ` 404` ``` apply simp ``` prensani@13020 ` 405` ```apply force+ ``` prensani@13020 ` 406` ```done ``` prensani@13020 ` 407` prensani@13020 ` 408` `end`