Theory XVcgEx

(*
    Author:      Norbert Schirmer
    Maintainer:  Norbert Schirmer, norbert.schirmer at web de

Copyright (C) 2006-2008 Norbert Schirmer
*)

section "Examples for Parallel Assignments"

theory XVcgEx
imports "../XVcg"

begin

record "globals" =
  "G_'"::"nat"
  "H_'"::"nat"

record 'g vars = "'g state" +
  A_' :: nat
  B_' :: nat
  C_' :: nat
  I_' :: nat
  M_' :: nat
  N_' :: nat
  R_' :: nat
  S_' :: nat
  Arr_' :: "nat list"
  Abr_':: string

term "BASIC
         ´A :== x,
         ´B :== y
      END"

term "BASIC
         ´G :== ´H,
         ´H :== ´G
      END"

term "BASIC
        LET (x,y) = (´A,b);
            z = ´B
        IN ´A :== x,
           ´G :== ´A + y + z
      END"


lemma "Γ⊢ ⦃´A = 0⦄
      ⦃´A < 0⦄ ⟼ BASIC
       LET (a,b,c) = foo ´A
       IN
            ´A :== a,
            ´B :== b,
            ´C :== c
      END
      ⦃´A = x ∧ ´B = y ∧ ´C = c⦄"
apply vcg
oops

lemma "Γ⊢ ⦃´A = 0⦄
      ⦃´A < 0⦄ ⟼ BASIC
       LET (a,b,c) = foo ´A
       IN
            ´A :== a,
            ´G :== b + ´B,
            ´H :== c
      END
      ⦃´A = x ∧ ´G = y ∧ ´H = c⦄"
apply vcg
oops

definition foo:: "nat ⇒ (nat × nat × nat)"
  where "foo n = (n,n+1,n+2)"

lemma "Γ⊢ ⦃´A = 0⦄
      ⦃´A < 0⦄ ⟼ BASIC
       LET (a,b,c) = foo ´A
       IN
            ´A :== a,
            ´G :== b + ´B,
            ´H :== c
      END
      ⦃´A = x ∧ ´G = y ∧ ´H = c⦄"
apply (vcg add: foo_def snd_conv fst_conv)
oops

end