Quelle  XVcgEx.thy

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