section ‹Examples›

theory OG_Examples imports OG_Syntax begin

subsection ‹Mutual Exclusion›

subsubsection ‹Peterson's Algorithm I›

text ‹Eike Best. "Semantics of Sequential and Parallel Programs", page 217.›

record Petersons_mutex_1 =
 pr1 :: nat
 pr2 :: nat
 in1 :: bool
 in2 :: bool
 hold :: nat

lemma Petersons_mutex_1:
  "∥- {🚫pr1=0 ∧ ¬🚫in1 ∧ 🚫pr2=0 ∧ ¬🚫in2 }
  COBEGIN {🚫pr1=0 ∧ ¬🚫in1}
  WHILE True INV {🚫pr1=0 ∧ ¬🚫in1}
  DO
  {🚫pr1=0 ∧ ¬🚫in1} ⟨ 🚫in1:=True,,🚫pr1:=1 ⟩;;
  {🚫pr1=1 ∧ 🚫in1} ⟨ 🚫hold:=1,,🚫pr1:=2 ⟩;;
  {🚫pr1=2 ∧ 🚫in1 ∧ (🚫hold=1 ∨ 🚫hold=2 ∧ 🚫pr2=2)}
  AWAIT (¬🚫in2 ∨ ¬(🚫hold=1)) THEN 🚫pr1:=3 END;;
  {🚫pr1=3 ∧ 🚫in1 ∧ (🚫hold=1 ∨ 🚫hold=2 ∧ 🚫pr2=2)}
   ⟨🚫in1:=False,,🚫pr1:=0⟩
  OD {🚫pr1=0 ∧ ¬🚫in1}
  ∥
  {🚫pr2=0 ∧ ¬🚫in2}
  WHILE True INV {🚫pr2=0 ∧ ¬🚫in2}
  DO
  {🚫pr2=0 ∧ ¬🚫in2} ⟨ 🚫in2:=True,,🚫pr2:=1 ⟩;;
  {🚫pr2=1 ∧ 🚫in2} ⟨ 🚫hold:=2,,🚫pr2:=2 ⟩;;
  {🚫pr2=2 ∧ 🚫in2 ∧ (🚫hold=2 ∨ (🚫hold=1 ∧ 🚫pr1=2))}
  AWAIT (¬🚫in1 ∨ ¬(🚫hold=2)) THEN 🚫pr2:=3 END;;
  {🚫pr2=3 ∧ 🚫in2 ∧ (🚫hold=2 ∨ (🚫hold=1 ∧ 🚫pr1=2))}
    ⟨🚫in2:=False,,🚫pr2:=0⟩
  OD {🚫pr2=0 ∧ ¬🚫in2}
  COEND
  {🚫pr1=0 ∧ ¬🚫in1 ∧ 🚫pr2=0 ∧ ¬🚫in2}"
apply oghoare
― ‹104 verification conditions.›
apply auto
done

subsubsection ‹Peterson's Algorithm II: A Busy Wait Solution›

text ‹Apt and Olderog. "Verification of sequential and concurrent Programs", page 282.›

record Busy_wait_mutex =
 flag1 :: bool
 flag2 :: bool
 turn  :: nat
 after1 :: bool
 after2 :: bool

lemma Busy_wait_mutex:
 "∥- {True}
  🚫flag1:=False,, 🚫flag2:=False,,
  COBEGIN {¬🚫flag1}
        WHILE True
        INV {¬🚫flag1}
        DO {¬🚫flag1} ⟨ 🚫flag1:=True,,🚫after1:=False ⟩;;
           {🚫flag1 ∧ ¬🚫after1} ⟨ 🚫turn:=1,,🚫after1:=True ⟩;;
           {🚫flag1 ∧ 🚫after1 ∧ (🚫turn=1 ∨ 🚫turn=2)}
            WHILE ¬(🚫flag2 ⟶ 🚫turn=2)
            INV {🚫flag1 ∧ 🚫after1 ∧ (🚫turn=1 ∨ 🚫turn=2)}
            DO {🚫flag1 ∧ 🚫after1 ∧ (🚫turn=1 ∨ 🚫turn=2)} SKIP OD;;
           {🚫flag1 ∧ 🚫after1 ∧ (🚫flag2 ∧ 🚫after2 ⟶ 🚫turn=2)}
            🚫flag1:=False
        OD
       {False}
  ∥
     {¬🚫flag2}
        WHILE True
        INV {¬🚫flag2}
        DO {¬🚫flag2} ⟨ 🚫flag2:=True,,🚫after2:=False ⟩;;
           {🚫flag2 ∧ ¬🚫after2} ⟨ 🚫turn:=2,,🚫after2:=True ⟩;;
           {🚫flag2 ∧ 🚫after2 ∧ (🚫turn=1 ∨ 🚫turn=2)}
            WHILE ¬(🚫flag1 ⟶ 🚫turn=1)
            INV {🚫flag2 ∧ 🚫after2 ∧ (🚫turn=1 ∨ 🚫turn=2)}
            DO {🚫flag2 ∧ 🚫after2 ∧ (🚫turn=1 ∨ 🚫turn=2)} SKIP OD;;
           {🚫flag2 ∧ 🚫after2 ∧ (🚫flag1 ∧ 🚫after1 ⟶ 🚫turn=1)}
            🚫flag2:=False
        OD
       {False}
  COEND
  {False}"
apply oghoare
― ‹122 vc›
apply auto
done

subsubsection ‹Peterson's Algorithm III: A Solution using Semaphores›

record  Semaphores_mutex =
 out :: bool
 who :: nat

lemma Semaphores_mutex:
 "∥- {i≠j}
  🚫out:=True ,,
  COBEGIN {i≠j}
       WHILE True INV {i≠j}
       DO {i≠j} AWAIT 🚫out THEN 🚫out:=False,, 🚫who:=i END;;
          {¬🚫out ∧ 🚫who=i ∧ i≠j} 🚫out:=True OD
       {False}
  ∥
       {i≠j}
       WHILE True INV {i≠j}
       DO {i≠j} AWAIT 🚫out THEN 🚫out:=False,,🚫who:=j END;;
          {¬🚫out ∧ 🚫who=j ∧ i≠j} 🚫out:=True OD
       {False}
  COEND
  {False}"
apply oghoare
― ‹38 vc›
apply auto
done

subsubsection ‹Peterson's Algorithm III: Parameterized version:›

lemma Semaphores_parameterized_mutex:
 "0<n ==> ∥- {True}
  🚫out:=True ,,
 COBEGIN
  SCHEME [0≤ i< n]
    {True}
     WHILE True INV {True}
      DO {True} AWAIT 🚫out THEN 🚫out:=False,, 🚫who:=i END;;
         {¬🚫out ∧ 🚫who=i} 🚫out:=True OD
    {False}
 COEND
  {False}"
apply oghoare
― ‹20 vc›
apply auto
done

subsubsection‹The Ticket Algorithm›

record Ticket_mutex =
 num :: nat
 nextv :: nat
 turn :: "nat list"
 index :: nat

lemma Ticket_mutex:
 "[ 0<n; I=«n=length 🚫turn ∧ 0<🚫nextv ∧ (∀k l. k<n ∧ l<n ∧ k≠l
    ⟶ 🚫turn!k < 🚫num ∧ (🚫turn!k =0 ∨ 🚫turn!k≠🚫turn!l))¬ ]
   ==> ∥- {n=length 🚫turn}
   🚫index:= 0,,
   WHILE 🚫index < n INV {n=length 🚫turn ∧ (∀i<🚫index. 🚫turn!i=0)}
    DO 🚫turn:= 🚫turn[🚫index:=0],, 🚫index:=🚫index +1 OD,,
  🚫num:=1 ,, 🚫nextv:=1 ,,
 COBEGIN
  SCHEME [0≤ i< n]
    {🚫I}
     WHILE True INV {🚫I}
      DO {🚫I} ⟨ 🚫turn :=🚫turn[i:=🚫num],, 🚫num:=🚫num+1 ⟩;;
         {🚫I} WAIT 🚫turn!i=🚫nextv END;;
         {🚫I ∧ 🚫turn!i=🚫nextv} 🚫nextv:=🚫nextv+1
      OD
    {False}
 COEND
  {False}"
apply oghoare
― ‹35 vc›
apply simp_all
― ‹16 vc›
apply(tactic ‹ALLGOALS (clarify_tac context)›)
― ‹11 vc›
apply simp_all
apply(tactic ‹ALLGOALS (clarify_tac context)›)
― ‹10 subgoals left›
apply(erule less_SucE)
 apply simp
apply simp
― ‹9 subgoals left›
apply(case_tac "i=k")
 apply force
apply simp
apply(case_tac "i=l")
 apply force
apply force
― ‹8 subgoals left›
prefer 8
apply force
apply force
― ‹6 subgoals left›
prefer 6
apply(erule_tac x=j in allE)
apply fastforce
― ‹5 subgoals left›
prefer 5
apply(case_tac [!] "j=k")
― ‹10 subgoals left›
apply simp_all
apply(erule_tac x=k in allE)
apply force
― ‹9 subgoals left›
apply(case_tac "j=l")
 apply simp
 apply(erule_tac x=k in allE)
 apply(erule_tac x=k in allE)
 apply(erule_tac x=l in allE)
 apply force
apply(erule_tac x=k in allE)
apply(erule_tac x=k in allE)
apply(erule_tac x=l in allE)
apply force
― ‹8 subgoals left›
apply force
apply(case_tac "j=l")
 apply simp
apply(erule_tac x=k in allE)
apply(erule_tac x=l in allE)
apply force
apply force
apply force
― ‹5 subgoals left›
apply(erule_tac x=k in allE)
apply(erule_tac x=l in allE)
apply(case_tac "j=l")
 apply force
apply force
apply force
― ‹3 subgoals left›
apply(erule_tac x=k in allE)
apply(erule_tac x=l in allE)
apply(case_tac "j=l")
 apply force
apply force
apply force
― ‹1 subgoals left›
apply(erule_tac x=k in allE)
apply(erule_tac x=l in allE)
apply(case_tac "j=l")
 apply force
apply force
done

subsection‹Parallel Zero Search›

text ‹Synchronized Zero Search. Zero-6›

text ‹Apt and Olderog. "Verification of sequential and concurrent Programs" page 294:›

record Zero_search =
   turn :: nat
   found :: bool
   x :: nat
   y :: nat

lemma Zero_search:
  "[I1= « a≤🚫x ∧ (🚫found ⟶ (a<🚫x ∧ f(🚫x)=0) ∨ (🚫y≤a ∧ f(🚫y)=0))
      ∧ (¬🚫found ∧ a<🚫 x ⟶ f(🚫x)≠0) ¬ ;
    I2= «🚫y≤a+1 ∧ (🚫found ⟶ (a<🚫x ∧ f(🚫x)=0) ∨ (🚫y≤a ∧ f(🚫y)=0))
      ∧ (¬🚫found ∧ 🚫y≤a ⟶ f(🚫y)≠0) ¬ ] ==>
  ∥- {∃ u. f(u)=0}
  🚫turn:=1,, 🚫found:= False,,
  🚫x:=a,, 🚫y:=a+1 ,,
  COBEGIN {🚫I1}
       WHILE ¬🚫found
       INV {🚫I1}
       DO {a≤🚫x ∧ (🚫found ⟶ 🚫y≤a ∧ f(🚫y)=0) ∧ (a<🚫x ⟶ f(🚫x)≠0)}
          WAIT 🚫turn=1 END;;
          {a≤🚫x ∧ (🚫found ⟶ 🚫y≤a ∧ f(🚫y)=0) ∧ (a<🚫x ⟶ f(🚫x)≠0)}
          🚫turn:=2;;
          {a≤🚫x ∧ (🚫found ⟶ 🚫y≤a ∧ f(🚫y)=0) ∧ (a<🚫x ⟶ f(🚫x)≠0)}
          ⟨ 🚫x:=🚫x+1,,
            IF f(🚫x)=0 THEN 🚫found:=True ELSE SKIP FI⟩
       OD;;
       {🚫I1 ∧ 🚫found}
       🚫turn:=2
       {🚫I1 ∧ 🚫found}
  ∥
      {🚫I2}
       WHILE ¬🚫found
       INV {🚫I2}
       DO {🚫y≤a+1 ∧ (🚫found ⟶ a<🚫x ∧ f(🚫x)=0) ∧ (🚫y≤a ⟶ f(🚫y)≠0)}
          WAIT 🚫turn=2 END;;
          {🚫y≤a+1 ∧ (🚫found ⟶ a<🚫x ∧ f(🚫x)=0) ∧ (🚫y≤a ⟶ f(🚫y)≠0)}
          🚫turn:=1;;
          {🚫y≤a+1 ∧ (🚫found ⟶ a<🚫x ∧ f(🚫x)=0) ∧ (🚫y≤a ⟶ f(🚫y)≠0)}
          ⟨ 🚫y:=(🚫y - 1),,
            IF f(🚫y)=0 THEN 🚫found:=True ELSE SKIP FI⟩
       OD;;
       {🚫I2 ∧ 🚫found}
       🚫turn:=1
       {🚫I2 ∧ 🚫found}
  COEND
  {f(🚫x)=0 ∨ f(🚫y)=0}"
apply oghoare
― ‹98 verification conditions›
apply auto
― ‹auto takes about 3 minutes !!›
done

text ‹Easier Version: without AWAIT. Apt and Olderog. page 256:›

lemma Zero_Search_2:
"[I1=« a≤🚫x ∧ (🚫found ⟶ (a<🚫x ∧ f(🚫x)=0) ∨ (🚫y≤a ∧ f(🚫y)=0))
    ∧ (¬🚫found ∧ a<🚫x ⟶ f(🚫x)≠0)¬;
 I2= «🚫y≤a+1 ∧ (🚫found ⟶ (a<🚫x ∧ f(🚫x)=0) ∨ (🚫y≤a ∧ f(🚫y)=0))
    ∧ (¬🚫found ∧ 🚫y≤a ⟶ f(🚫y)≠0)¬] ==>
  ∥- {∃u. f(u)=0}
  🚫found:= False,,
  🚫x:=a,, 🚫y:=a+1,,
  COBEGIN {🚫I1}
       WHILE ¬🚫found
       INV {🚫I1}
       DO {a≤🚫x ∧ (🚫found ⟶ 🚫y≤a ∧ f(🚫y)=0) ∧ (a<🚫x ⟶ f(🚫x)≠0)}
          ⟨ 🚫x:=🚫x+1,,IF f(🚫x)=0 THEN 🚫found:=True ELSE SKIP FI⟩
       OD
       {🚫I1 ∧ 🚫found}
  ∥
      {🚫I2}
       WHILE ¬🚫found
       INV {🚫I2}
       DO {🚫y≤a+1 ∧ (🚫found ⟶ a<🚫x ∧ f(🚫x)=0) ∧ (🚫y≤a ⟶ f(🚫y)≠0)}
          ⟨ 🚫y:=(🚫y - 1),,IF f(🚫y)=0 THEN 🚫found:=True ELSE SKIP FI⟩
       OD
       {🚫I2 ∧ 🚫found}
  COEND
  {f(🚫x)=0 ∨ f(🚫y)=0}"
apply oghoare
― ‹20 vc›
apply auto
― ‹auto takes aprox. 2 minutes.›
done

subsection ‹Producer/Consumer›

subsubsection ‹Previous lemmas›

lemma nat_lemma2: "[ b = m*(n::nat) + t; a = s*n + u; t=u; b-a < n ] ==> m ≤ s"
proof -
  assume "b = m*(n::nat) + t" "a = s*n + u" "t=u"
  hence "(m - s) * n = b - a" by (simp add: diff_mult_distrib)
  also assume "… < n"
  finally have "m - s < 1" by simp
  thus ?thesis by arith
qed

lemma mod_lemma: "[ (c::nat) ≤ a; a < b; b - c < n ] ==> b mod n ≠ a mod n"
apply(subgoal_tac "b=b div n*n + b mod n" )
 prefer 2  apply (simp add: div_mult_mod_eq [symmetric])
apply(subgoal_tac "a=a div n*n + a mod n")
 prefer 2
 apply(simp add: div_mult_mod_eq [symmetric])
apply(subgoal_tac "b - a ≤ b - c")
 prefer 2 apply arith
apply(drule le_less_trans)
back
 apply assumption
apply(frule less_not_refl2)
apply(drule less_imp_le)
apply (drule_tac m = "a" and k = n in div_le_mono)
apply(safe)
apply(frule_tac b = "b" and a = "a" and n = "n" in nat_lemma2, assumption, assumption)
apply assumption
apply(drule order_antisym, assumption)
apply(rotate_tac -3)
apply(simp)
done


subsubsection ‹Producer/Consumer Algorithm›

record Producer_consumer =
  ins :: nat
  outs :: nat
  li :: nat
  lj :: nat
  vx :: nat
  vy :: nat
  buffer :: "nat list"
  b :: "nat list"

text ‹The whole proof takes aprox. 4 minutes.›

lemma Producer_consumer:
  "[INIT= «0<length a ∧ 0<length 🚫buffer ∧ length 🚫b=length a¬ ;
    I= «(∀k<🚫ins. 🚫outs≤k ⟶ (a ! k) = 🚫buffer ! (k mod (length 🚫buffer))) ∧
            🚫outs≤🚫ins ∧ 🚫ins-🚫outs≤length 🚫buffer¬ ;
    I1= «🚫I ∧ 🚫li≤length a¬ ;
    p1= «🚫I1 ∧ 🚫li=🚫ins¬ ;
    I2 = «🚫I ∧ (∀k<🚫lj. (a ! k)=(🚫b ! k)) ∧ 🚫lj≤length a¬ ;
    p2 = «🚫I2 ∧ 🚫lj=🚫outs¬ ] ==>
  ∥- {🚫INIT}
 🚫ins:=0,, 🚫outs:=0,, 🚫li:=0,, 🚫lj:=0,,
 COBEGIN {🚫p1 ∧ 🚫INIT}
   WHILE 🚫li <length a
     INV {🚫p1 ∧ 🚫INIT}
   DO {🚫p1 ∧ 🚫INIT ∧ 🚫li<length a}
       🚫vx:= (a ! 🚫li);;
      {🚫p1 ∧ 🚫INIT ∧ 🚫li<length a ∧ 🚫vx=(a ! 🚫li)}
        WAIT 🚫ins-🚫outs < length 🚫buffer END;;
      {🚫p1 ∧ 🚫INIT ∧ 🚫li<length a ∧ 🚫vx=(a ! 🚫li)
         ∧ 🚫ins-🚫outs < length 🚫buffer}
       🚫buffer:=(list_update 🚫buffer (🚫ins mod (length 🚫buffer)) 🚫vx);;
      {🚫p1 ∧ 🚫INIT ∧ 🚫li<length a
         ∧ (a ! 🚫li)=(🚫buffer ! (🚫ins mod (length 🚫buffer)))
         ∧ 🚫ins-🚫outs <length 🚫buffer}
       🚫ins:=🚫ins+1;;
      {🚫I1 ∧ 🚫INIT ∧ (🚫li+1)=🚫ins ∧ 🚫li<length a}
       🚫li:=🚫li+1
   OD
  {🚫p1 ∧ 🚫INIT ∧ 🚫li=length a}
  ∥
  {🚫p2 ∧ 🚫INIT}
   WHILE 🚫lj < length a
     INV {🚫p2 ∧ 🚫INIT}
   DO {🚫p2 ∧ 🚫lj<length a ∧ 🚫INIT}
        WAIT 🚫outs<🚫ins END;;
      {🚫p2 ∧ 🚫lj<length a ∧ 🚫outs<🚫ins ∧ 🚫INIT}
       🚫vy:=(🚫buffer ! (🚫outs mod (length 🚫buffer)));;
      {🚫p2 ∧ 🚫lj<length a ∧ 🚫outs<🚫ins ∧ 🚫vy=(a ! 🚫lj) ∧ 🚫INIT}
       🚫outs:=🚫outs+1;;
      {🚫I2 ∧ (🚫lj+1)=🚫outs ∧ 🚫lj<length a ∧ 🚫vy=(a ! 🚫lj) ∧ 🚫INIT}
       🚫b:=(list_update 🚫b 🚫lj 🚫vy);;
      {🚫I2 ∧ (🚫lj+1)=🚫outs ∧ 🚫lj<length a ∧ (a ! 🚫lj)=(🚫b ! 🚫lj) ∧ 🚫INIT}
       🚫lj:=🚫lj+1
   OD
  {🚫p2 ∧ 🚫lj=length a ∧ 🚫INIT}
 COEND
 { ∀k<length a. (a ! k)=(🚫b ! k)}"
apply oghoare
― ‹138 vc›
apply(tactic ‹ALLGOALS (clarify_tac context)›)
― ‹112 subgoals left›
apply(simp_all (no_asm))
― ‹43 subgoals left›
apply(tactic ‹ALLGOALS (conjI_Tac context (K all_tac))›)
― ‹419 subgoals left›
apply(tactic ‹ALLGOALS (clarify_tac context)›)
― ‹99 subgoals left›
apply(simp_all only:length_0_conv [THEN sym])
― ‹20 subgoals left›
apply (simp_all del:length_0_conv length_greater_0_conv add: nth_list_update mod_lemma)
― ‹9 subgoals left›
apply (force simp add:less_Suc_eq)
apply(hypsubst_thin, drule sym)
apply (force simp add:less_Suc_eq)+
done

subsection ‹Parameterized Examples›

subsubsection ‹Set Elements of an Array to Zero›

record Example1 =
  a :: "nat → nat"

lemma Example1:
 "∥- {True}
   COBEGIN SCHEME [0≤i<n] {True} 🚫a:=🚫a (i:=0) {🚫a i=0} COEND
  {∀i < n. 🚫a i = 0}"
apply oghoare
apply simp_all
done

text ‹Same example with lists as auxiliary variables.›
record Example1_list =
  A :: "nat list"
lemma Example1_list:
 "∥- {n < length 🚫A}
   COBEGIN
     SCHEME [0≤i<n] {n < length 🚫A} 🚫A:=🚫A[i:=0] {🚫A!i=0}
   COEND
    {∀i < n. 🚫A!i = 0}"
apply oghoare
apply force+
done

subsubsection ‹Increment a Variable in Parallel›

text ‹First some lemmas about summation properties.›
(*
lemma Example2_lemma1: "!!b. j<n \<Longrightarrow> (\<Sum>i::nat<n. b i) = (0::nat) \<Longrightarrow> b j = 0 "
apply(induct n)
 apply simp_all
apply(force simp add: less_Suc_eq)
done
*)
lemma Example2_lemma2_aux: "!!b. j<n ==>
 (∑i=0..<n. (b i::nat)) =
 (∑i=0..<j. b i) + b j + (∑i=0..<n-(Suc j) . b (Suc j + i))"
apply(induct n)
 apply simp_all
apply(simp add:less_Suc_eq)
 apply(auto)
apply(subgoal_tac "n - j = Suc(n- Suc j)")
  apply simp
apply arith
done

lemma Example2_lemma2_aux2:
  "!!b. j≤ s ==> (∑i::nat=0..<j. (b (s:=t)) i) = (∑i=0..<j. b i)"
apply(induct j)
 apply simp_all
done

lemma Example2_lemma2:
 "!!b. [j<n; b j=0] ==> Suc (∑i::nat=0..<n. b i)=(∑i=0..<n. (b (j := Suc 0)) i)"
apply(frule_tac b="(b (j:=(Suc 0)))" in Example2_lemma2_aux)
apply(erule_tac  t="sum (b(j := (Suc 0))) {0..<n}" in ssubst)
apply(frule_tac b=b in Example2_lemma2_aux)
apply(erule_tac  t="sum b {0..<n}" in ssubst)
apply(subgoal_tac "Suc (sum b {0..<j} + b j + (∑i=0..<n - Suc j. b (Suc j + i)))=(sum b {0..<j} + Suc (b j) + (∑i=0..<n - Suc j. b (Suc j + i)))")
apply(rotate_tac -1)
apply(erule ssubst)
apply(subgoal_tac "j≤j")
 apply(drule_tac b="b" and t="(Suc 0)" in Example2_lemma2_aux2)
apply(rotate_tac -1)
apply(erule ssubst)
apply simp_all
done


record Example2 =
 c :: "nat → nat"
 x :: nat

lemma Example_2: "0<n ==>
 ∥- {🚫x=0 ∧ (∑i=0..<n. 🚫c i)=0}
 COBEGIN
   SCHEME [0≤i<n]
  {🚫x=(∑i=0..<n. 🚫c i) ∧ 🚫c i=0}
   ⟨ 🚫x:=🚫x+(Suc 0),, 🚫c:=🚫c (i:=(Suc 0)) ⟩
  {🚫x=(∑i=0..<n. 🚫c i) ∧ 🚫c i=(Suc 0)}
 COEND
 {🚫x=n}"
apply oghoare
apply (simp_all cong del: sum.cong_simp)
apply (tactic ‹ALLGOALS (clarify_tac context)›)
apply (simp_all cong del: sum.cong_simp)
   apply(erule (1) Example2_lemma2)
  apply(erule (1) Example2_lemma2)
 apply(erule (1) Example2_lemma2)
apply(simp)
done

end