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