1(*
2    Author:      Norbert Schirmer
3    Maintainer:  Norbert Schirmer, norbert.schirmer at web de
4    License:     LGPL
5*)
6
7(*  Title:      XVcg.thy
8    Author:     Norbert Schirmer, TU Muenchen
9
10Copyright (C) 2006-2008 Norbert Schirmer
11Some rights reserved, TU Muenchen
12
13This library is free software; you can redistribute it and/or modify
14it under the terms of the GNU Lesser General Public License as
15published by the Free Software Foundation; either version 2.1 of the
16License, or (at your option) any later version.
17
18This library is distributed in the hope that it will be useful, but
19WITHOUT ANY WARRANTY; without even the implied warranty of
20MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
21Lesser General Public License for more details.
22
23You should have received a copy of the GNU Lesser General Public
24License along with this library; if not, write to the Free Software
25Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
26USA
27*)
28
29theory XVcg
30imports Vcg
31
32begin
33
34
35text \<open>We introduce a syntactic variant of the let-expression so that we can
36safely unfold it during verification condition generation. With the new
37theorem attribute \<open>vcg_simp\<close> we can declare equalities to be used
38by the verification condition generator, while simplifying assertions.
39\<close>
40
41syntax
42"_Let'" :: "[letbinds, basicblock] => basicblock"  ("(LET (_)/ IN (_))" 23)
43
44translations
45  "_Let' (_binds b bs) e"  == "_Let' b (_Let' bs e)"
46  "_Let' (_bind x a) e"    == "CONST Let' a (%x. e)"
47
48
49lemma Let'_unfold [vcg_simp]: "Let' x f = f x"
50  by (simp add: Let'_def Let_def)
51
52lemma Let'_split_conv [vcg_simp]:
53  "(Let' x  (\<lambda>p. (case_prod (f p) (g p)))) =
54   (Let' x  (\<lambda>p. (f p) (fst (g p)) (snd (g p))))"
55  by (simp add: split_def)
56
57end
58