(*
    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