secc
/
seL4-L4.verified
mirror of https://github.com/seL4/l4v.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

c-parser: update Simpl from AFP; update license 

Pull in Simpl update from AFP-2023 and the associated license change to
BSD-3-Clause.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2024-02-18 14:46:20 +11:00
parent ade6239fad
commit 2f6199408d
No known key found for this signature in database
GPG Key ID: 20A847CE6AB7F5F3
39 changed files with 3501 additions and 2722 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
.reuse/dep5
View File

@ -6,7 +6,7 @@ Source: https://github.com/seL4/l4v/
# AFP entry https://www.isa-afp.org/entries/Simpl.html
Files: tools/c-parser/Simpl/*
Copyright: 2008, Norbert Schirmer, TU Muenchen
License: LGPL-2.1-only
License: BSD-3-Clause
# AFP entry Word_Lib
Files: lib/Word_Lib/Word_Next.thy

21
tools/c-parser/Simpl/AlternativeSmallStep.thy
View File

@ -1,29 +1,8 @@
(*
Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: AlternativeSmallStep.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2006-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
section \<open>Alternative Small Step Semantics\<close>

423
tools/c-parser/Simpl/COPYRIGHT
View File

@ -1,423 +0,0 @@
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION
0. This License Agreement applies to any software library or other
program which contains a notice placed by the copyright holder or
other authorized party saying it may be distributed under the terms of
this Lesser General Public License (also called "this License"). Each
licensee is addressed as "you".
A "library" means a collection of software functions and/or data
prepared so as to be conveniently linked with application programs
(which use some of those functions and data) to form executables.
The "Library", below, refers to any such software library or work
which has been distributed under these terms. A "work based on the
Library" means either the Library or any derivative work under
copyright law: that is to say, a work containing the Library or a
portion of it, either verbatim or with modifications and/or translated
straightforwardly into another language. (Hereinafter, translation is
included without limitation in the term "modification".)
"Source code" for a work means the preferred form of the work for
making modifications to it. For a library, complete source code means
all the source code for all modules it contains, plus any associated
interface definition files, plus the scripts used to control
compilation and installation of the library.
Activities other than copying, distribution and modification are not
covered by this License; they are outside its scope. The act of
running a program using the Library is not restricted, and output from
such a program is covered only if its contents constitute a work based
on the Library (independent of the use of the Library in a tool for
writing it). Whether that is true depends on what the Library does and
what the program that uses the Library does.
1. You may copy and distribute verbatim copies of the Library's
complete source code as you receive it, in any medium, provided that
you conspicuously and appropriately publish on each copy an
appropriate copyright notice and disclaimer of warranty; keep intact
all the notices that refer to this License and to the absence of any
warranty; and distribute a copy of this License along with the
Library.
You may charge a fee for the physical act of transferring a copy, and
you may at your option offer warranty protection in exchange for a
fee.
2. You may modify your copy or copies of the Library or any portion of
it, thus forming a work based on the Library, and copy and distribute
such modifications or work under the terms of Section 1 above,
provided that you also meet all of these conditions:
a) The modified work must itself be a software library.
b) You must cause the files modified to carry prominent notices
stating that you changed the files and the date of any change.
c) You must cause the whole of the work to be licensed at no charge to
all third parties under the terms of this License.
d) If a facility in the modified Library refers to a function or a
table of data to be supplied by an application program that uses the
facility, other than as an argument passed when the facility is
invoked, then you must make a good faith effort to ensure that, in the
event an application does not supply such function or table, the
facility still operates, and performs whatever part of its purpose
remains meaningful.
(For example, a function in a library to compute square roots has a
purpose that is entirely well-defined independent of the
application. Therefore, Subsection 2d requires that any
application-supplied function or table used by this function must be
optional: if the application does not supply it, the square root
function must still compute square roots.)
These requirements apply to the modified work as a whole. If
identifiable sections of that work are not derived from the Library,
and can be reasonably considered independent and separate works in
themselves, then this License, and its terms, do not apply to those
sections when you distribute them as separate works. But when you
distribute the same sections as part of a whole which is a work based
on the Library, the distribution of the whole must be on the terms of
this License, whose permissions for other licensees extend to the
entire whole, and thus to each and every part regardless of who wrote
it.
Thus, it is not the intent of this section to claim rights or contest
your rights to work written entirely by you; rather, the intent is to
exercise the right to control the distribution of derivative or
collective works based on the Library.
In addition, mere aggregation of another work not based on the Library
with the Library (or with a work based on the Library) on a volume of
a storage or distribution medium does not bring the other work under
the scope of this License.
3. You may opt to apply the terms of the ordinary GNU General Public
License instead of this License to a given copy of the Library. To do
this, you must alter all the notices that refer to this License, so
that they refer to the ordinary GNU General Public License, version 2,
instead of to this License. (If a newer version than version 2 of the
ordinary GNU General Public License has appeared, then you can specify
that version instead if you wish.) Do not make any other change in
these notices.
Once this change is made in a given copy, it is irreversible for that
copy, so the ordinary GNU General Public License applies to all
subsequent copies and derivative works made from that copy.
This option is useful when you wish to copy part of the code of the
Library into a program that is not a library.
4. You may copy and distribute the Library (or a portion or derivative
of it, under Section 2) in object code or executable form under the
terms of Sections 1 and 2 above provided that you accompany it with
the complete corresponding machine-readable source code, which must be
distributed under the terms of Sections 1 and 2 above on a medium
customarily used for software interchange.
If distribution of object code is made by offering access to copy from
a designated place, then offering equivalent access to copy the source
code from the same place satisfies the requirement to distribute the
source code, even though third parties are not compelled to copy the
source along with the object code.
5. A program that contains no derivative of any portion of the
Library, but is designed to work with the Library by being compiled or
linked with it, is called a "work that uses the Library". Such a work,
in isolation, is not a derivative work of the Library, and therefore
falls outside the scope of this License.
However, linking a "work that uses the Library" with the Library
creates an executable that is a derivative of the Library (because it
contains portions of the Library), rather than a "work that uses the
library". The executable is therefore covered by this License. Section
6 states terms for distribution of such executables.
When a "work that uses the Library" uses material from a header file
that is part of the Library, the object code for the work may be a
derivative work of the Library even though the source code is
not. Whether this is true is especially significant if the work can be
linked without the Library, or if the work is itself a library. The
threshold for this to be true is not precisely defined by law.
If such an object file uses only numerical parameters, data structure
layouts and accessors, and small macros and small inline functions
(ten lines or less in length), then the use of the object file is
unrestricted, regardless of whether it is legally a derivative
work. (Executables containing this object code plus portions of the
Library will still fall under Section 6.)
Otherwise, if the work is a derivative of the Library, you may
distribute the object code for the work under the terms of Section
6. Any executables containing that work also fall under Section 6,
whether or not they are linked directly with the Library itself.
6. As an exception to the Sections above, you may also combine or link
a "work that uses the Library" with the Library to produce a work
containing portions of the Library, and distribute that work under
terms of your choice, provided that the terms permit modification of
the work for the customer's own use and reverse engineering for
debugging such modifications.
You must give prominent notice with each copy of the work that the
Library is used in it and that the Library and its use are covered by
this License. You must supply a copy of this License. If the work
during execution displays copyright notices, you must include the
copyright notice for the Library among them, as well as a reference
directing the user to the copy of this License. Also, you must do one
of these things:
a) Accompany the work with the complete corresponding machine-readable
source code for the Library including whatever changes were used in
the work (which must be distributed under Sections 1 and 2 above);
and, if the work is an executable linked with the Library, with the
complete machine-readable "work that uses the Library", as object code
and/or source code, so that the user can modify the Library and then
relink to produce a modified executable containing the modified
Library. (It is understood that the user who changes the contents of
definitions files in the Library will not necessarily be able to
recompile the application to use the modified definitions.)
b) Use a suitable shared library mechanism for linking with the
Library. A suitable mechanism is one that (1) uses at run time a copy
of the library already present on the user's computer system, rather
than copying library functions into the executable, and (2) will
operate properly with a modified version of the library, if the user
installs one, as long as the modified version is interface-compatible
with the version that the work was made with.
c) Accompany the work with a written offer, valid for at least three
years, to give the same user the materials specified in Subsection 6a,
above, for a charge no more than the cost of performing this
distribution.
d) If distribution of the work is made by offering access to copy from
a designated place, offer equivalent access to copy the above
specified materials from the same place.
e) Verify that the user has already received a copy of these materials
or that you have already sent this user a copy.
For an executable, the required form of the "work that uses the
Library" must include any data and utility programs needed for
reproducing the executable from it. However, as a special exception,
the materials to be distributed need not include anything that is
normally distributed (in either source or binary form) with the major
components (compiler, kernel, and so on) of the operating system on
which the executable runs, unless that component itself accompanies
the executable.
It may happen that this requirement contradicts the license
restrictions of other proprietary libraries that do not normally
accompany the operating system. Such a contradiction means you cannot
use both them and the Library together in an executable that you
distribute.
7. You may place library facilities that are a work based on the
Library side-by-side in a single library together with other library
facilities not covered by this License, and distribute such a combined
library, provided that the separate distribution of the work based on
the Library and of the other library facilities is otherwise
permitted, and provided that you do these two things:
a) Accompany the combined library with a copy of the same work based
on the Library, uncombined with any other library facilities. This
must be distributed under the terms of the Sections above.
b) Give prominent notice with the combined library of the fact that
part of it is a work based on the Library, and explaining where to
find the accompanying uncombined form of the same work.
8. You may not copy, modify, sublicense, link with, or distribute the
Library except as expressly provided under this License. Any attempt
otherwise to copy, modify, sublicense, link with, or distribute the
Library is void, and will automatically terminate your rights under
this License. However, parties who have received copies, or rights,
from you under this License will not have their licenses terminated so
long as such parties remain in full compliance.
9. You are not required to accept this License, since you have not
signed it. However, nothing else grants you permission to modify or
distribute the Library or its derivative works. These actions are
prohibited by law if you do not accept this License. Therefore, by
modifying or distributing the Library (or any work based on the
Library), you indicate your acceptance of this License to do so, and
all its terms and conditions for copying, distributing or modifying
the Library or works based on it.
10. Each time you redistribute the Library (or any work based on the
Library), the recipient automatically receives a license from the
original licensor to copy, distribute, link with or modify the Library
subject to these terms and conditions. You may not impose any further
restrictions on the recipients' exercise of the rights granted
herein. You are not responsible for enforcing compliance by third
parties with this License.
11. If, as a consequence of a court judgment or allegation of patent
infringement or for any other reason (not limited to patent issues),
conditions are imposed on you (whether by court order, agreement or
otherwise) that contradict the conditions of this License, they do not
excuse you from the conditions of this License. If you cannot
distribute so as to satisfy simultaneously your obligations under this
License and any other pertinent obligations, then as a consequence you
may not distribute the Library at all. For example, if a patent
license would not permit royalty-free redistribution of the Library by
all those who receive copies directly or indirectly through you, then
the only way you could satisfy both it and this License would be to
refrain entirely from distribution of the Library.
If any portion of this section is held invalid or unenforceable under
any particular circumstance, the balance of the section is intended to
apply, and the section as a whole is intended to apply in other
circumstances.
It is not the purpose of this section to induce you to infringe any
patents or other property right claims or to contest validity of any
such claims; this section has the sole purpose of protecting the
integrity of the free software distribution system which is
implemented by public license practices. Many people have made
generous contributions to the wide range of software distributed
through that system in reliance on consistent application of that
system; it is up to the author/donor to decide if he or she is willing
to distribute software through any other system and a licensee cannot
impose that choice.
This section is intended to make thoroughly clear what is believed to
be a consequence of the rest of this License.
12. If the distribution and/or use of the Library is restricted in
certain countries either by patents or by copyrighted interfaces, the
original copyright holder who places the Library under this License
may add an explicit geographical distribution limitation excluding
those countries, so that distribution is permitted only in or among
countries not thus excluded. In such case, this License incorporates
the limitation as if written in the body of this License.
13. The Free Software Foundation may publish revised and/or new
versions of the Lesser General Public License from time to time. Such
new versions will be similar in spirit to the present version, but may
differ in detail to address new problems or concerns.
Each version is given a distinguishing version number. If the Library
specifies a version number of this License which applies to it and
"any later version", you have the option of following the terms and
conditions either of that version or of any later version published by
the Free Software Foundation. If the Library does not specify a
license version number, you may choose any version ever published by
the Free Software Foundation.
14. If you wish to incorporate parts of the Library into other free
programs whose distribution conditions are incompatible with these,
write to the author to ask for permission. For software which is
copyrighted by the Free Software Foundation, write to the Free
Software Foundation; we sometimes make exceptions for this. Our
decision will be guided by the two goals of preserving the free status
of all derivatives of our free software and of promoting the sharing
and reuse of software generally.
NO WARRANTY
15. BECAUSE THE LIBRARY IS LICENSED FREE OF CHARGE, THERE IS NO
WARRANTY FOR THE LIBRARY, TO THE EXTENT PERMITTED BY APPLICABLE
LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS
AND/OR OTHER PARTIES PROVIDE THE LIBRARY "AS IS" WITHOUT WARRANTY OF
ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO,
THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE
LIBRARY IS WITH YOU. SHOULD THE LIBRARY PROVE DEFECTIVE, YOU ASSUME
THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
16. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN
WRITING WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY
AND/OR REDISTRIBUTE THE LIBRARY AS PERMITTED ABOVE, BE LIABLE TO YOU
FOR DAMAGES, INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR
CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THE
LIBRARY (INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING
RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD PARTIES OR A
FAILURE OF THE LIBRARY TO OPERATE WITH ANY OTHER SOFTWARE), EVEN IF
SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH
DAMAGES.
END OF TERMS AND CONDITIONS

3
tools/c-parser/Simpl/DPC0Expressions.thy
View File

@ -1,7 +1,8 @@
(*
Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
Copyright (C) 2006-2008 Norbert Schirmer
*)
section \<open>SHORTENED! Parallel expressions in DPC/Hoare.\<close>

3
tools/c-parser/Simpl/DPC0Library.thy
View File

@ -1,7 +1,8 @@
(*
Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
Copyright (C) 2006-2008 Norbert Schirmer
*)
section \<open>DPC0 standard library\<close>

23
tools/c-parser/Simpl/Generalise.thy
View File

@ -1,29 +1,8 @@
(*
Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: Generalise.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2005-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
Copyright (C) 2006-2008 Norbert Schirmer
*)
theory Generalise imports "HOL-Statespace.DistinctTreeProver"

23
tools/c-parser/Simpl/HeapList.thy
View File

@ -1,28 +1,7 @@
(* Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: HeapList.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2004-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
Copyright (C) 2006-2008 Norbert Schirmer
*)
section \<open>Paths and Lists in the Heap\<close>

23
tools/c-parser/Simpl/Hoare.thy
View File

@ -1,29 +1,8 @@
(*
Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: Hoare.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2004-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
Copyright (C) 2006-2008 Norbert Schirmer
*)
section \<open>Auxiliary Definitions/Lemmas to Facilitate Hoare Logic\<close>

416
tools/c-parser/Simpl/HoarePartial.thy
View File

@ -1,29 +1,10 @@
(*
Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: HoarePartial.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2004-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
Copyright (c) 2022 Apple Inc. All rights reserved.
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
section \<open>Derived Hoare Rules for Partial Correctness\<close>
@ -199,6 +180,11 @@ lemma Seq [trans, intro?]:
"\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c\<^sub>1 R,A; \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> R c\<^sub>2 Q,A\<rbrakk> \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (Seq c\<^sub>1 c\<^sub>2) Q,A"
by (rule hoarep.Seq)
lemma SeqSame:
"\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c\<^sub>1 Q,A; \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> Q c\<^sub>2 Q,A\<rbrakk> \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (Seq c\<^sub>1 c\<^sub>2) Q,A"
by (rule hoarep.Seq)
lemma SeqSwap:
"\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> R c2 Q,A; \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c1 R,A\<rbrakk> \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (Seq c1 c2) Q,A"
by (rule Seq)
@ -207,6 +193,9 @@ lemma BSeq:
"\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c\<^sub>1 R,A; \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> R c\<^sub>2 Q,A\<rbrakk> \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (bseq c\<^sub>1 c\<^sub>2) Q,A"
by (unfold bseq_def) (rule Seq)
lemma BSeqSame:
"\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c\<^sub>1 Q,A; \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> Q c\<^sub>2 Q,A\<rbrakk> \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (bseq c\<^sub>1 c\<^sub>2) Q,A"
by (rule BSeq)
lemma Cond:
assumes wp: "P \<subseteq> {s. (s\<in>b \<longrightarrow> s\<in>P\<^sub>1) \<and> (s\<notin>b \<longrightarrow> s\<in>P\<^sub>2)}"
@ -312,6 +301,11 @@ apply (rule Guarantee [THEN conseqPre])
apply auto
done
lemma GuardStripSame:
"\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A; f \<in> F\<rbrakk>
\<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (Guard f g c) Q,A"
by (rule GuardStrip [OF subset_refl])
lemma GuardStripSwap:
"\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> R c Q,A; P \<subseteq> R; f \<in> F\<rbrakk>
\<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (Guard f g c) Q,A"
@ -452,18 +446,18 @@ using adapt
apply blast
done
lemma Block:
lemma Block_exn:
assumes adapt: "P \<subseteq> {s. init s \<in> P' s}"
assumes bdy: "\<forall>s. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P' s) bdy {t. return s t \<in> R s t},{t. return s t \<in> A}"
assumes bdy: "\<forall>s. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P' s) bdy {t. return s t \<in> R s t},{t. result_exn (return s t) t \<in> A}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (block init bdy return c) Q,A"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (block_exn init bdy return result_exn c) Q,A"
apply (rule conseq [where P'="\<lambda>Z. {s. s=Z \<and> init s \<in> P' Z}" and Q'="\<lambda>Z. Q" and
A'="\<lambda>Z. A"])
prefer 2
using adapt
apply blast
apply (rule allI)
apply (unfold block_def)
apply (unfold block_exn_def)
apply (rule DynCom)
apply (rule ballI)
apply clarsimp
@ -478,7 +472,7 @@ apply (rule SeqSwap)
apply (rule c [rule_format])
apply (rule Basic)
apply clarsimp
apply (rule_tac R="{t. return Z t \<in> A}" in Catch)
apply (rule_tac R="{t. result_exn (return Z t) t \<in> A}" in Catch)
apply (rule_tac R="{i. i \<in> P' Z}" in Seq)
apply (rule Basic)
apply clarsimp
@ -490,6 +484,14 @@ apply (rule Basic)
apply simp
done
lemma Block:
assumes adapt: "P \<subseteq> {s. init s \<in> P' s}"
assumes bdy: "\<forall>s. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P' s) bdy {t. return s t \<in> R s t},{t. return s t \<in> A}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (block init bdy return c) Q,A"
unfolding block_def
by (rule Block_exn [OF adapt bdy c])
lemma BlockSwap:
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
@ -500,22 +502,22 @@ using adapt bdy c
by (rule Block)
lemma BlockSpec:
lemma Block_exnSpec:
assumes adapt: "P \<subseteq> {s. \<exists>Z. init s \<in> P' Z \<and>
(\<forall>t. t \<in> Q' Z \<longrightarrow> return s t \<in> R s t) \<and>
(\<forall>t. t \<in> A' Z \<longrightarrow> return s t \<in> A)}"
(\<forall>t. t \<in> A' Z \<longrightarrow> (result_exn (return s t) t) \<in> A)}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes bdy: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P' Z) bdy (Q' Z),(A' Z)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (block init bdy return c) Q,A"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (block_exn init bdy return result_exn c) Q,A"
apply (rule conseq [where P'="\<lambda>Z. {s. init s \<in> P' Z \<and>
(\<forall>t. t \<in> Q' Z \<longrightarrow> return s t \<in> R s t) \<and>
(\<forall>t. t \<in> A' Z \<longrightarrow> return s t \<in> A)}" and Q'="\<lambda>Z. Q" and
(\<forall>t. t \<in> A' Z \<longrightarrow> (result_exn (return s t) t) \<in> A)}" and Q'="\<lambda>Z. Q" and
A'="\<lambda>Z. A"])
prefer 2
using adapt
apply blast
apply (rule allI)
apply (unfold block_def)
apply (unfold block_exn_def)
apply (rule DynCom)
apply (rule ballI)
apply clarsimp
@ -530,7 +532,7 @@ apply (rule SeqSwap)
apply (rule c [rule_format])
apply (rule Basic)
apply clarsimp
apply (rule_tac R="{t. return s t \<in> A}" in Catch)
apply (rule_tac R="{t. (result_exn (return s t) t) \<in> A}" in Catch)
apply (rule_tac R="{i. i \<in> P' Z}" in Seq)
apply (rule Basic)
apply clarsimp
@ -542,7 +544,18 @@ apply (rule SeqSwap)
apply (rule Throw)
apply (rule Basic)
apply simp
done
done
lemma BlockSpec:
assumes adapt: "P \<subseteq> {s. \<exists>Z. init s \<in> P' Z \<and>
(\<forall>t. t \<in> Q' Z \<longrightarrow> return s t \<in> R s t) \<and>
(\<forall>t. t \<in> A' Z \<longrightarrow> return s t \<in> A)}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes bdy: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P' Z) bdy (Q' Z),(A' Z)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (block init bdy return c) Q,A"
unfolding block_def
by (rule Block_exnSpec [OF adapt c bdy])
lemma Throw: "P \<subseteq> A \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P Throw Q,A"
by (rule hoarep.Throw [THEN conseqPre])
@ -551,6 +564,9 @@ lemmas Catch = hoarep.Catch
lemma CatchSwap: "\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> R c\<^sub>2 Q,A; \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c\<^sub>1 Q,R\<rbrakk> \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P Catch c\<^sub>1 c\<^sub>2 Q,A"
by (rule hoarep.Catch)
lemma CatchSame: "\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c\<^sub>1 Q,A; \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> A c\<^sub>2 Q,A\<rbrakk> \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P Catch c\<^sub>1 c\<^sub>2 Q,A"
by (rule hoarep.Catch)
lemma raise: "P \<subseteq> {s. f s \<in> A} \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P raise f Q,A"
apply (simp add: raise_def)
apply (rule Seq)
@ -575,6 +591,18 @@ lemma condCatchSwap: "\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> R
\<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub>P condCatch c\<^sub>1 b c\<^sub>2 Q,A"
by (rule condCatch)
lemma condCatchSame:
assumes c1: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c\<^sub>1 Q,A"
assumes c2: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> A c\<^sub>2 Q,A"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub>P condCatch c\<^sub>1 b c\<^sub>2 Q,A"
proof -
have eq: "((b \<inter> A) \<union> (-b \<inter> A)) = A" by blast
show ?thesis
apply (rule condCatch [OF _ c2])
apply (simp add: eq)
apply (rule c1)
done
qed
lemma ProcSpec:
assumes adapt: "P \<subseteq> {s. \<exists>Z. init s \<in> P' Z \<and>
@ -587,6 +615,17 @@ using adapt c p
apply (unfold call_def)
by (rule BlockSpec)
lemma Proc_exnSpec:
assumes adapt: "P \<subseteq> {s. \<exists>Z. init s \<in> P' Z \<and>
(\<forall>t. t \<in> Q' Z \<longrightarrow> return s t \<in> R s t) \<and>
(\<forall>t. t \<in> A' Z \<longrightarrow> result_exn (return s t) t \<in> A)}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes p: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P' Z) Call p (Q' Z),(A' Z)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (call_exn init p return result_exn c) Q,A"
using adapt c p
apply (unfold call_exn_def)
by (rule Block_exnSpec)
lemma ProcSpec':
assumes adapt: "P \<subseteq> {s. \<exists>Z. init s \<in> P' Z \<and>
(\<forall>t \<in> Q' Z. return s t \<in> R s t) \<and>
@ -603,6 +642,17 @@ apply (rule_tac x=Z in exI)
apply blast
done
lemma Proc_exnSpecNoAbrupt:
assumes adapt: "P \<subseteq> {s. \<exists>Z. init s \<in> P' Z \<and>
(\<forall>t. t \<in> Q' Z \<longrightarrow> return s t \<in> R s t)}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes p: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P' Z) Call p (Q' Z),{}"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (call_exn init p return result_exn c) Q,A"
apply (rule Proc_exnSpec [OF _ c p])
using adapt
apply simp
done
lemma ProcSpecNoAbrupt:
assumes adapt: "P \<subseteq> {s. \<exists>Z. init s \<in> P' Z \<and>
(\<forall>t. t \<in> Q' Z \<longrightarrow> return s t \<in> R s t)}"
@ -719,8 +769,32 @@ apply (rule ProcBody [where \<Gamma>=\<Gamma>, OF _ bdy [rule_format] body])
apply simp
done
lemma Call_exnBody:
assumes adapt: "P \<subseteq> {s. init s \<in> P' s}"
assumes bdy: "\<forall>s. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P' s) body {t. return s t \<in> R s t},{t. result_exn (return s t) t \<in> A}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes body: "\<Gamma> p = Some body"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (call_exn init p return result_exn c) Q,A"
apply (unfold call_exn_def)
apply (rule Block_exn [OF adapt _ c])
apply (rule allI)
apply (rule ProcBody [where \<Gamma>=\<Gamma>, OF _ bdy [rule_format] body])
apply simp
done
lemmas ProcModifyReturn = HoarePartialProps.ProcModifyReturn
lemmas ProcModifyReturnSameFaults = HoarePartialProps.ProcModifyReturnSameFaults
lemmas Proc_exnModifyReturn = HoarePartialProps.Proc_exnModifyReturn
lemmas Proc_exnModifyReturnSameFaults = HoarePartialProps.Proc_exnModifyReturnSameFaults
lemma Proc_exnModifyReturnNoAbr:
assumes spec: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (call_exn init p return' result_exn c) Q,A"
assumes result_conform:
"\<forall>s t. t \<in> Modif (init s) \<longrightarrow> (return' s t) = (return s t)"
assumes modifies_spec:
"\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} Call p (Modif \<sigma>),{}"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (call_exn init p return result_exn c) Q,A"
by (rule Proc_exnModifyReturn [OF spec result_conform _ modifies_spec]) simp
lemma ProcModifyReturnNoAbr:
assumes spec: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (call init p return' c) Q,A"
@ -731,6 +805,15 @@ lemma ProcModifyReturnNoAbr:
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (call init p return c) Q,A"
by (rule ProcModifyReturn [OF spec result_conform _ modifies_spec]) simp
lemma Proc_exnModifyReturnNoAbrSameFaults:
assumes spec: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (call_exn init p return' result_exn c) Q,A"
assumes result_conform:
"\<forall>s t. t \<in> Modif (init s) \<longrightarrow> (return' s t) = (return s t)"
assumes modifies_spec:
"\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} Call p (Modif \<sigma>),{}"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (call_exn init p return result_exn c) Q,A"
by (rule Proc_exnModifyReturnSameFaults [OF spec result_conform _ modifies_spec]) simp
lemma ProcModifyReturnNoAbrSameFaults:
assumes spec: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (call init p return' c) Q,A"
assumes result_conform:
@ -740,21 +823,20 @@ lemma ProcModifyReturnNoAbrSameFaults:
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (call init p return c) Q,A"
by (rule ProcModifyReturnSameFaults [OF spec result_conform _ modifies_spec]) simp
lemma DynProc:
lemma DynProc_exn:
assumes adapt: "P \<subseteq> {s. \<exists>Z. init s \<in> P' s Z \<and>
(\<forall>t. t \<in> Q' s Z \<longrightarrow> return s t \<in> R s t) \<and>
(\<forall>t. t \<in> A' s Z \<longrightarrow> return s t \<in> A)}"
(\<forall>t. t \<in> A' s Z \<longrightarrow> result_exn (return s t) t \<in> A)}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes p: "\<forall>s\<in> P. \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P' s Z) Call (p s) (Q' s Z),(A' s Z)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P dynCall init p return c Q,A"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P dynCall_exn f UNIV init p return result_exn c Q,A"
apply (rule conseq [where P'="\<lambda>Z. {s. s=Z \<and> s \<in> P}"
and Q'="\<lambda>Z. Q" and A'="\<lambda>Z. A"])
prefer 2
using adapt
apply blast
apply (rule allI)
apply (unfold dynCall_def call_def block_def)
apply (unfold dynCall_exn_def call_exn_def maybe_guard_UNIV block_exn_def guards.simps)
apply (rule DynCom)
apply clarsimp
apply (rule DynCom)
@ -788,7 +870,41 @@ apply (rule SeqSwap)
apply (rule c [rule_format])
apply (rule Basic)
apply clarsimp
done
done
lemma DynProc_exn_guards_cons:
assumes p: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P dynCall_exn f UNIV init p return result_exn c Q,A"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (g \<inter> P) dynCall_exn f g init p return result_exn c Q,A"
using p apply (clarsimp simp add: dynCall_exn_def maybe_guard_def)
apply (rule Guard)
apply (rule subset_refl)
apply assumption
done
lemma DynProc:
assumes adapt: "P \<subseteq> {s. \<exists>Z. init s \<in> P' s Z \<and>
(\<forall>t. t \<in> Q' s Z \<longrightarrow> return s t \<in> R s t) \<and>
(\<forall>t. t \<in> A' s Z \<longrightarrow> return s t \<in> A)}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes p: "\<forall>s\<in> P. \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P' s Z) Call (p s) (Q' s Z),(A' s Z)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P dynCall init p return c Q,A"
using adapt c p unfolding dynCall_dynCall_exn by (rule DynProc_exn)
lemma DynProc_exn':
assumes adapt: "P \<subseteq> {s. \<exists>Z. init s \<in> P' s Z \<and>
(\<forall>t \<in> Q' s Z. return s t \<in> R s t) \<and>
(\<forall>t \<in> A' s Z. result_exn (return s t) t \<in> A)}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes p: "\<forall>s\<in> P. \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P' s Z) Call (p s) (Q' s Z),(A' s Z)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P dynCall_exn f UNIV init p return result_exn c Q,A"
proof -
from adapt have "P \<subseteq> {s. \<exists>Z. init s \<in> P' s Z \<and>
(\<forall>t. t \<in> Q' s Z \<longrightarrow> return s t \<in> R s t) \<and>
(\<forall>t. t \<in> A' s Z \<longrightarrow> result_exn (return s t) t \<in> A)}"
by blast
from this c p show ?thesis
by (rule DynProc_exn)
qed
lemma DynProc':
assumes adapt: "P \<subseteq> {s. \<exists>Z. init s \<in> P' s Z \<and>
@ -797,28 +913,20 @@ lemma DynProc':
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes p: "\<forall>s\<in> P. \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P' s Z) Call (p s) (Q' s Z),(A' s Z)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P dynCall init p return c Q,A"
proof -
from adapt have "P \<subseteq> {s. \<exists>Z. init s \<in> P' s Z \<and>
(\<forall>t. t \<in> Q' s Z \<longrightarrow> return s t \<in> R s t) \<and>
(\<forall>t. t \<in> A' s Z \<longrightarrow> return s t \<in> A)}"
by blast
from this c p show ?thesis
by (rule DynProc)
qed
using adapt c p unfolding dynCall_dynCall_exn by (rule DynProc_exn')
lemma DynProcStaticSpec:
lemma DynProc_exnStaticSpec:
assumes adapt: "P \<subseteq> {s. s \<in> S \<and> (\<exists>Z. init s \<in> P' Z \<and>
(\<forall>\<tau>. \<tau> \<in> Q' Z \<longrightarrow> return s \<tau> \<in> R s \<tau>) \<and>
(\<forall>\<tau>. \<tau> \<in> A' Z \<longrightarrow> return s \<tau> \<in> A))}"
(\<forall>\<tau>. \<tau> \<in> A' Z \<longrightarrow> result_exn (return s \<tau>) \<tau> \<in> A))}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes spec: "\<forall>s\<in>S. \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P' Z) Call (p s) (Q' Z),(A' Z)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall_exn f UNIV init p return result_exn c) Q,A"
proof -
from adapt have P_S: "P \<subseteq> S"
by blast
have "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P \<inter> S) (dynCall init p return c) Q,A"
apply (rule DynProc [where P'="\<lambda>s Z. P' Z" and Q'="\<lambda>s Z. Q' Z"
have "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P \<inter> S) (dynCall_exn f UNIV init p return result_exn c) Q,A"
apply (rule DynProc_exn [where P'="\<lambda>s Z. P' Z" and Q'="\<lambda>s Z. Q' Z"
and A'="\<lambda>s Z. A' Z", OF _ c])
apply clarsimp
apply (frule in_mono [rule_format, OF adapt])
@ -830,6 +938,26 @@ proof -
by (rule conseqPre) (insert P_S,blast)
qed
lemma DynProcStaticSpec:
assumes adapt: "P \<subseteq> {s. s \<in> S \<and> (\<exists>Z. init s \<in> P' Z \<and>
(\<forall>\<tau>. \<tau> \<in> Q' Z \<longrightarrow> return s \<tau> \<in> R s \<tau>) \<and>
(\<forall>\<tau>. \<tau> \<in> A' Z \<longrightarrow> return s \<tau> \<in> A))}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes spec: "\<forall>s\<in>S. \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P' Z) Call (p s) (Q' Z),(A' Z)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
using adapt c spec unfolding dynCall_dynCall_exn by (rule DynProc_exnStaticSpec)
lemma DynProc_exnProcPar:
assumes adapt: "P \<subseteq> {s. p s = q \<and> (\<exists>Z. init s \<in> P' Z \<and>
(\<forall>\<tau>. \<tau> \<in> Q' Z \<longrightarrow> return s \<tau> \<in> R s \<tau>) \<and>
(\<forall>\<tau>. \<tau> \<in> A' Z \<longrightarrow> result_exn (return s \<tau>) \<tau> \<in> A))}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes spec: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P' Z) Call q (Q' Z),(A' Z)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall_exn f UNIV init p return result_exn c) Q,A"
apply (rule DynProc_exnStaticSpec [where S="{s. p s = q}",simplified, OF adapt c])
using spec
apply simp
done
lemma DynProcProcPar:
assumes adapt: "P \<subseteq> {s. p s = q \<and> (\<exists>Z. init s \<in> P' Z \<and>
@ -843,17 +971,16 @@ shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall init p return
apply simp
done
lemma DynProcProcParNoAbrupt:
lemma DynProc_exnProcParNoAbrupt:
assumes adapt: "P \<subseteq> {s. p s = q \<and> (\<exists>Z. init s \<in> P' Z \<and>
(\<forall>\<tau>. \<tau> \<in> Q' Z \<longrightarrow> return s \<tau> \<in> R s \<tau>))}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes spec: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P' Z) Call q (Q' Z),{}"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall_exn f UNIV init p return result_exn c) Q,A"
proof -
have "P \<subseteq> {s. p s = q \<and> (\<exists> Z. init s \<in> P' Z \<and>
(\<forall>t. t \<in> Q' Z \<longrightarrow> return s t \<in> R s t) \<and>
(\<forall>t. t \<in> {} \<longrightarrow> return s t \<in> A))}"
(\<forall>t. t \<in> {} \<longrightarrow> result_exn (return s t) t \<in> A))}"
(is "P \<subseteq> ?P'")
proof
fix s
@ -872,12 +999,42 @@ proof -
note P = this
show ?thesis
apply -
apply (rule DynProcStaticSpec [where S="{s. p s = q}",simplified, OF P c])
apply (rule DynProc_exnStaticSpec [where S="{s. p s = q}",simplified, OF P c])
apply (insert spec)
apply auto
done
qed
lemma DynProcProcParNoAbrupt:
assumes adapt: "P \<subseteq> {s. p s = q \<and> (\<exists>Z. init s \<in> P' Z \<and>
(\<forall>\<tau>. \<tau> \<in> Q' Z \<longrightarrow> return s \<tau> \<in> R s \<tau>))}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes spec: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> (P' Z) Call q (Q' Z),{}"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
using adapt c spec unfolding dynCall_dynCall_exn by (rule DynProc_exnProcParNoAbrupt)
lemma DynProc_exnModifyReturnNoAbr:
assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall_exn f g init p return' result_exn c) Q,A"
assumes ret_nrm_modif: "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
assumes modif_clause:
"\<forall>s \<in> P. \<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),{}"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall_exn f g init p return result_exn c) Q,A"
proof -
from ret_nrm_modif
have "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
by iprover
then
have ret_nrm_modif': "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
by simp
have ret_abr_modif': "\<forall>s t. t \<in> {}
\<longrightarrow> result_exn (return' s t) t = result_exn (return s t) t"
by simp
from to_prove ret_nrm_modif' ret_abr_modif' modif_clause show ?thesis
by (rule dynProc_exnModifyReturn)
qed
lemma DynProcModifyReturnNoAbr:
assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall init p return' c) Q,A"
@ -885,7 +1042,17 @@ lemma DynProcModifyReturnNoAbr:
\<longrightarrow> return' s t = return s t"
assumes modif_clause:
"\<forall>s \<in> P. \<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),{}"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
using to_prove ret_nrm_modif modif_clause unfolding dynCall_dynCall_exn
by (rule DynProc_exnModifyReturnNoAbr)
lemma ProcDyn_exnModifyReturnNoAbrSameFaults:
assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall_exn f g init p return' result_exn c) Q,A"
assumes ret_nrm_modif: "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
assumes modif_clause:
"\<forall>s \<in> P. \<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} (Call (p s)) (Modif \<sigma>),{}"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall_exn f g init p return result_exn c) Q,A"
proof -
from ret_nrm_modif
have "\<forall>s t. t \<in> (Modif (init s))
@ -896,34 +1063,43 @@ proof -
\<longrightarrow> return' s t = return s t"
by simp
have ret_abr_modif': "\<forall>s t. t \<in> {}
\<longrightarrow> return' s t = return s t"
\<longrightarrow> result_exn (return' s t) t = result_exn (return s t) t"
by simp
from to_prove ret_nrm_modif' ret_abr_modif' modif_clause show ?thesis
by (rule dynProcModifyReturn)
from to_prove ret_nrm_modif' ret_abr_modif' modif_clause show ?thesis
by (rule dynProc_exnModifyReturnSameFaults)
qed
lemma ProcDynModifyReturnNoAbrSameFaults:
assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall init p return' c) Q,A"
assumes ret_nrm_modif: "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
assumes modif_clause:
"\<forall>s \<in> P. \<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} (Call (p s)) (Modif \<sigma>),{}"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
using to_prove ret_nrm_modif modif_clause unfolding dynCall_dynCall_exn
by (rule ProcDyn_exnModifyReturnNoAbrSameFaults)
lemma Proc_exnProcParModifyReturn:
assumes q: "P \<subseteq> {s. p s = q} \<inter> P'"
\<comment> \<open>@{thm[source] DynProcProcPar} introduces the same constraint as first conjunction in
@{term P'}, so the vcg can simplify it.\<close>
assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P' (dynCall_exn f g init p return' result_exn c) Q,A"
assumes ret_nrm_modif: "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
assumes ret_abr_modif: "\<forall>s t. t \<in> (ModifAbr (init s))
\<longrightarrow> result_exn (return' s t) t = result_exn (return s t) t"
assumes modif_clause:
"\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} (Call q) (Modif \<sigma>),(ModifAbr \<sigma>)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall_exn f g init p return result_exn c) Q,A"
proof -
from ret_nrm_modif
have "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
by iprover
then
have ret_nrm_modif': "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
by simp
have ret_abr_modif': "\<forall>s t. t \<in> {}
\<longrightarrow> return' s t = return s t"
by simp
from to_prove ret_nrm_modif' ret_abr_modif' modif_clause show ?thesis
by (rule dynProcModifyReturnSameFaults)
from to_prove have "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall_exn f g init p return' result_exn c) Q,A"
by (rule conseqPre) blast
from this ret_nrm_modif
ret_abr_modif
have "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall_exn f g init p return result_exn c) Q,A"
by (rule dynProc_exnModifyReturn) (insert modif_clause,auto)
from this q show ?thesis
by (rule conseqPre)
qed
@ -938,19 +1114,34 @@ lemma ProcProcParModifyReturn:
\<longrightarrow> return' s t = return s t"
assumes modif_clause:
"\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} (Call q) (Modif \<sigma>),(ModifAbr \<sigma>)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
using q to_prove ret_nrm_modif ret_abr_modif modif_clause unfolding dynCall_dynCall_exn
by (rule Proc_exnProcParModifyReturn)
lemma Proc_exnProcParModifyReturnSameFaults:
assumes q: "P \<subseteq> {s. p s = q} \<inter> P'"
\<comment> \<open>@{thm[source] DynProcProcPar} introduces the same constraint as first conjunction in
@{term P'}, so the vcg can simplify it.\<close>
assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P' (dynCall_exn f g init p return' result_exn c) Q,A"
assumes ret_nrm_modif: "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
assumes ret_abr_modif: "\<forall>s t. t \<in> (ModifAbr (init s))
\<longrightarrow> result_exn (return' s t) t = result_exn (return s t) t"
assumes modif_clause:
"\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} Call q (Modif \<sigma>),(ModifAbr \<sigma>)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall_exn f g init p return result_exn c) Q,A"
proof -
from to_prove have "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall init p return' c) Q,A"
from to_prove
have "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall_exn f g init p return' result_exn c) Q,A"
by (rule conseqPre) blast
from this ret_nrm_modif
ret_abr_modif
have "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall init p return c) Q,A"
by (rule dynProcModifyReturn) (insert modif_clause,auto)
have "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall_exn f g init p return result_exn c) Q,A"
by (rule dynProc_exnModifyReturnSameFaults) (insert modif_clause,auto)
from this q show ?thesis
by (rule conseqPre)
qed
lemma ProcProcParModifyReturnSameFaults:
assumes q: "P \<subseteq> {s. p s = q} \<inter> P'"
\<comment> \<open>@{thm[source] DynProcProcPar} introduces the same constraint as first conjunction in
@ -962,20 +1153,30 @@ lemma ProcProcParModifyReturnSameFaults:
\<longrightarrow> return' s t = return s t"
assumes modif_clause:
"\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} Call q (Modif \<sigma>),(ModifAbr \<sigma>)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
using q to_prove ret_nrm_modif ret_abr_modif modif_clause unfolding dynCall_dynCall_exn
by (rule Proc_exnProcParModifyReturnSameFaults)
lemma Proc_exnProcParModifyReturnNoAbr:
assumes q: "P \<subseteq> {s. p s = q} \<inter> P'"
\<comment> \<open>@{thm[source] DynProcProcParNoAbrupt} introduces the same constraint as
first conjunction in @{term P'}, so the vcg can simplify it.\<close>
assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P' (dynCall_exn f g init p return' result_exn c) Q,A"
assumes ret_nrm_modif: "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
assumes modif_clause:
"\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} (Call q) (Modif \<sigma>),{}"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall_exn f g init p return result_exn c) Q,A"
proof -
from to_prove
have "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall init p return' c) Q,A"
from to_prove have "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall_exn f g init p return' result_exn c) Q,A"
by (rule conseqPre) blast
from this ret_nrm_modif
ret_abr_modif
have "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall init p return c) Q,A"
by (rule dynProcModifyReturnSameFaults) (insert modif_clause,auto)
have "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall_exn f g init p return result_exn c) Q,A"
by (rule DynProc_exnModifyReturnNoAbr) (insert modif_clause,auto)
from this q show ?thesis
by (rule conseqPre)
qed
lemma ProcProcParModifyReturnNoAbr:
assumes q: "P \<subseteq> {s. p s = q} \<inter> P'"
\<comment> \<open>@{thm[source] DynProcProcParNoAbrupt} introduces the same constraint as
@ -985,13 +1186,27 @@ lemma ProcProcParModifyReturnNoAbr:
\<longrightarrow> return' s t = return s t"
assumes modif_clause:
"\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} (Call q) (Modif \<sigma>),{}"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
using q to_prove ret_nrm_modif modif_clause unfolding dynCall_dynCall_exn
by (rule Proc_exnProcParModifyReturnNoAbr)
lemma Proc_exnProcParModifyReturnNoAbrSameFaults:
assumes q: "P \<subseteq> {s. p s = q} \<inter> P'"
\<comment> \<open>@{thm[source] DynProcProcParNoAbrupt} introduces the same constraint as
first conjunction in @{term P'}, so the vcg can simplify it.\<close>
assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P' (dynCall_exn f g init p return' result_exn c) Q,A"
assumes ret_nrm_modif: "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
assumes modif_clause:
"\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} (Call q) (Modif \<sigma>),{}"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall_exn f g init p return result_exn c) Q,A"
proof -
from to_prove have "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall init p return' c) Q,A"
from to_prove have
"\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall_exn f g init p return' result_exn c) Q,A"
by (rule conseqPre) blast
from this ret_nrm_modif
have "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall init p return c) Q,A"
by (rule DynProcModifyReturnNoAbr) (insert modif_clause,auto)
have "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall_exn f g init p return result_exn c) Q,A"
by (rule ProcDyn_exnModifyReturnNoAbrSameFaults) (insert modif_clause,auto)
from this q show ?thesis
by (rule conseqPre)
qed
@ -1005,17 +1220,10 @@ lemma ProcProcParModifyReturnNoAbrSameFaults:
\<longrightarrow> return' s t = return s t"
assumes modif_clause:
"\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} (Call q) (Modif \<sigma>),{}"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
proof -
from to_prove have
"\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall init p return' c) Q,A"
by (rule conseqPre) blast
from this ret_nrm_modif
have "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall init p return c) Q,A"
by (rule ProcDynModifyReturnNoAbrSameFaults) (insert modif_clause,auto)
from this q show ?thesis
by (rule conseqPre)
qed
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
using q to_prove ret_nrm_modif modif_clause unfolding dynCall_dynCall_exn
by (rule Proc_exnProcParModifyReturnNoAbrSameFaults)
lemma MergeGuards_iff: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P merge_guards c Q,A = \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P c Q,A"
by (auto intro: MergeGuardsI MergeGuardsD)
@ -1207,6 +1415,6 @@ lemma WhileConj [intro?]:
(simp add: HoarePartialDef.While [THEN conseqPrePost]
Collect_conj_eq Collect_neg_eq)
(* FIXME: Add rules for guarded while *)
(* fixme: Add rules for guarded while *)
end

23
tools/c-parser/Simpl/HoarePartialDef.thy
View File

@ -1,29 +1,8 @@
(*
Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: HoarePartialDef.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2004-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
Copyright (C) 2006-2008 Norbert Schirmer
*)
section \<open>Hoare Logic for Partial Correctness\<close>

725
tools/c-parser/Simpl/HoarePartialProps.thy
View File

@ -1,29 +1,10 @@
(*
Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: HoarePartialProps.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2004-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
Copyright (c) 2022 Apple Inc. All rights reserved.
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
section \<open>Properties of Partial Correctness Hoare Logic\<close>
@ -1336,27 +1317,27 @@ done
subsubsection \<open>Modify Return\<close>
lemma ProcModifyReturn_sound:
assumes valid_call: "\<forall>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P call init p return' c Q,A"
lemma Proc_exnModifyReturn_sound:
assumes valid_call: "\<forall>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P call_exn init p return' result_exn c Q,A"
assumes valid_modif:
"\<forall>\<sigma>. \<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/UNIV\<^esub> {\<sigma>} Call p (Modif \<sigma>),(ModifAbr \<sigma>)"
assumes ret_modif:
"\<forall>s t. t \<in> Modif (init s)
\<longrightarrow> return' s t = return s t"
assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s)
\<longrightarrow> return' s t = return s t"
shows "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P (call init p return c) Q,A"
\<longrightarrow> result_exn (return' s t) t = result_exn (return s t) t"
shows "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P (call_exn init p return result_exn c) Q,A"
proof (rule cnvalidI)
fix s t
assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
then have ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/UNIV\<^esub> P (Call p) Q,A"
by (auto intro: nvalid_augment_Faults)
assume exec: "\<Gamma>\<turnstile>\<langle>call init p return c,Normal s\<rangle> =n\<Rightarrow> t"
assume exec: "\<Gamma>\<turnstile>\<langle>call_exn init p return result_exn c,Normal s\<rangle> =n\<Rightarrow> t"
assume P: "s \<in> P"
assume t_notin_F: "t \<notin> Fault ` F"
from exec
show "t \<in> Normal ` Q \<union> Abrupt ` A"
proof (cases rule: execn_call_Normal_elim)
proof (cases rule: execn_call_exn_Normal_elim)
fix bdy m t'
assume bdy: "\<Gamma> p = Some bdy"
assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Normal t'"
@ -1372,8 +1353,8 @@ proof (rule cnvalidI)
Normal (return s t')"
by simp
with exec_body exec_c bdy n
have "\<Gamma>\<turnstile>\<langle>call init p return' c,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_call)
have "\<Gamma>\<turnstile>\<langle>call_exn init p return' result_exn c,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_call_exn)
from cnvalidD [OF valid_call [rule_format] ctxt this] P t_notin_F
show ?thesis
by simp
@ -1382,19 +1363,19 @@ proof (rule cnvalidI)
assume bdy: "\<Gamma> p = Some bdy"
assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Abrupt t'"
assume n: "n = Suc m"
assume t: "t = Abrupt (return s t')"
assume t: "t = Abrupt (result_exn (return s t') t')"
also from exec_body n bdy
have "\<Gamma>\<turnstile>\<langle>Call p,Normal (init s)\<rangle> =n\<Rightarrow> Abrupt t'"
by (auto simp add: intro: execn.intros)
from cnvalidD [OF valid_modif [rule_format, of n "init s"] ctxt' this] P
have "t' \<in> ModifAbr (init s)"
by auto
with ret_modifAbr have "Abrupt (return s t') = Abrupt (return' s t')"
with ret_modifAbr have "Abrupt (result_exn (return s t') t') = Abrupt (result_exn (return' s t') t')"
by simp
finally have "t = Abrupt (return' s t')" .
finally have "t = Abrupt (result_exn (return' s t') t')" .
with exec_body bdy n
have "\<Gamma>\<turnstile>\<langle>call init p return' c,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_callAbrupt)
have "\<Gamma>\<turnstile>\<langle>call_exn init p return' result_exn c,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_call_exnAbrupt)
from cnvalidD [OF valid_call [rule_format] ctxt this] P t_notin_F
show ?thesis
by simp
@ -1403,8 +1384,8 @@ proof (rule cnvalidI)
assume bdy: "\<Gamma> p = Some bdy"
assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Fault f" "n = Suc m"
"t = Fault f"
with bdy have "\<Gamma>\<turnstile>\<langle>call init p return' c ,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_callFault)
with bdy have "\<Gamma>\<turnstile>\<langle>call_exn init p return' result_exn c ,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_call_exnFault)
from valid_call [rule_format] ctxt this P t_notin_F
show ?thesis
by (rule cnvalidD)
@ -1413,8 +1394,8 @@ proof (rule cnvalidI)
assume bdy: "\<Gamma> p = Some bdy"
assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Stuck" "n = Suc m"
"t = Stuck"
with bdy have "\<Gamma>\<turnstile>\<langle>call init p return' c ,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_callStuck)
with bdy have "\<Gamma>\<turnstile>\<langle>call_exn init p return' result_exn c ,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_call_exnStuck)
from valid_call [rule_format] ctxt this P t_notin_F
show ?thesis
by (rule cnvalidD)
@ -1422,14 +1403,48 @@ proof (rule cnvalidI)
fix m
assume "\<Gamma> p = None"
and "n = Suc m" "t = Stuck"
then have "\<Gamma>\<turnstile>\<langle>call init p return' c ,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_callUndefined)
then have "\<Gamma>\<turnstile>\<langle>call_exn init p return' result_exn c ,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_call_exnUndefined)
from valid_call [rule_format] ctxt this P t_notin_F
show ?thesis
by (rule cnvalidD)
qed
qed
lemma ProcModifyReturn_sound:
assumes valid_call: "\<forall>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P call init p return' c Q,A"
assumes valid_modif:
"\<forall>\<sigma>. \<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/UNIV\<^esub> {\<sigma>} Call p (Modif \<sigma>),(ModifAbr \<sigma>)"
assumes ret_modif:
"\<forall>s t. t \<in> Modif (init s)
\<longrightarrow> return' s t = return s t"
assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s)
\<longrightarrow> return' s t = return s t"
shows "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P (call init p return c) Q,A"
using valid_call valid_modif ret_modif ret_modifAbr
unfolding call_call_exn
by (rule Proc_exnModifyReturn_sound)
lemma Proc_exnModifyReturn:
assumes spec: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (call_exn init p return' result_exn c) Q,A"
assumes result_conform:
"\<forall>s t. t \<in> Modif (init s) \<longrightarrow> (return' s t) = (return s t)"
assumes return_conform:
"\<forall>s t. t \<in> ModifAbr (init s)
\<longrightarrow> (result_exn (return' s t) t) = (result_exn (return s t) t)"
assumes modifies_spec:
"\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} Call p (Modif \<sigma>),(ModifAbr \<sigma>)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (call_exn init p return result_exn c) Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule Proc_exnModifyReturn_sound
[where Modif=Modif and ModifAbr=ModifAbr,
OF _ _ result_conform return_conform] )
using spec
apply (blast intro: hoare_cnvalid)
using modifies_spec
apply (blast intro: hoare_cnvalid)
done
lemma ProcModifyReturn:
assumes spec: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (call init p return' c) Q,A"
@ -1440,37 +1455,30 @@ lemma ProcModifyReturn:
\<longrightarrow> (return' s t) = (return s t)"
assumes modifies_spec:
"\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} Call p (Modif \<sigma>),(ModifAbr \<sigma>)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (call init p return c) Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule ProcModifyReturn_sound
[where Modif=Modif and ModifAbr=ModifAbr,
OF _ _ result_conform return_conform] )
using spec
apply (blast intro: hoare_cnvalid)
using modifies_spec
apply (blast intro: hoare_cnvalid)
done
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (call init p return c) Q,A"
using spec result_conform return_conform modifies_spec
unfolding call_call_exn
by (rule Proc_exnModifyReturn)
lemma ProcModifyReturnSameFaults_sound:
assumes valid_call: "\<forall>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P call init p return' c Q,A"
lemma Proc_exnModifyReturnSameFaults_sound:
assumes valid_call: "\<forall>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P call_exn init p return' result_exn c Q,A"
assumes valid_modif:
"\<forall>\<sigma>. \<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> {\<sigma>} Call p (Modif \<sigma>),(ModifAbr \<sigma>)"
assumes ret_modif:
"\<forall>s t. t \<in> Modif (init s)
\<longrightarrow> return' s t = return s t"
assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s)
\<longrightarrow> return' s t = return s t"
shows "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P (call init p return c) Q,A"
\<longrightarrow> result_exn (return' s t) t = result_exn (return s t) t"
shows "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P (call_exn init p return result_exn c) Q,A"
proof (rule cnvalidI)
fix s t
assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
assume exec: "\<Gamma>\<turnstile>\<langle>call init p return c,Normal s\<rangle> =n\<Rightarrow> t"
assume exec: "\<Gamma>\<turnstile>\<langle>call_exn init p return result_exn c,Normal s\<rangle> =n\<Rightarrow> t"
assume P: "s \<in> P"
assume t_notin_F: "t \<notin> Fault ` F"
from exec
show "t \<in> Normal ` Q \<union> Abrupt ` A"
proof (cases rule: execn_call_Normal_elim)
proof (cases rule: execn_call_exn_Normal_elim)
fix bdy m t'
assume bdy: "\<Gamma> p = Some bdy"
assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Normal t'"
@ -1486,8 +1494,8 @@ proof (rule cnvalidI)
Normal (return s t')"
by simp
with exec_body exec_c bdy n
have "\<Gamma>\<turnstile>\<langle>call init p return' c,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_call)
have "\<Gamma>\<turnstile>\<langle>call_exn init p return' result_exn c,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_call_exn)
from cnvalidD [OF valid_call [rule_format] ctxt this] P t_notin_F
show ?thesis
by simp
@ -1496,7 +1504,7 @@ proof (rule cnvalidI)
assume bdy: "\<Gamma> p = Some bdy"
assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Abrupt t'"
assume n: "n = Suc m"
assume t: "t = Abrupt (return s t')"
assume t: "t = Abrupt (result_exn (return s t') t')"
also
from exec_body n bdy
have "\<Gamma>\<turnstile>\<langle>Call p,Normal (init s)\<rangle> =n \<Rightarrow> Abrupt t'"
@ -1504,12 +1512,12 @@ proof (rule cnvalidI)
from cnvalidD [OF valid_modif [rule_format, of n "init s"] ctxt this] P
have "t' \<in> ModifAbr (init s)"
by auto
with ret_modifAbr have "Abrupt (return s t') = Abrupt (return' s t')"
with ret_modifAbr have "Abrupt (result_exn (return s t') t') = Abrupt (result_exn (return' s t') t')"
by simp
finally have "t = Abrupt (return' s t')" .
finally have "t = Abrupt (result_exn (return' s t') t')" .
with exec_body bdy n
have "\<Gamma>\<turnstile>\<langle>call init p return' c,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_callAbrupt)
have "\<Gamma>\<turnstile>\<langle>call_exn init p return' result_exn c,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_call_exnAbrupt)
from cnvalidD [OF valid_call [rule_format] ctxt this] P t_notin_F
show ?thesis
by simp
@ -1518,8 +1526,8 @@ proof (rule cnvalidI)
assume bdy: "\<Gamma> p = Some bdy"
assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Fault f" "n = Suc m" and
t: "t = Fault f"
with bdy have "\<Gamma>\<turnstile>\<langle>call init p return' c ,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_callFault)
with bdy have "\<Gamma>\<turnstile>\<langle>call_exn init p return' result_exn c ,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_call_exnFault)
from cnvalidD [OF valid_call [rule_format] ctxt this P] t t_notin_F
show ?thesis
by simp
@ -1528,8 +1536,8 @@ proof (rule cnvalidI)
assume bdy: "\<Gamma> p = Some bdy"
assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Stuck" "n = Suc m"
"t = Stuck"
with bdy have "\<Gamma>\<turnstile>\<langle>call init p return' c ,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_callStuck)
with bdy have "\<Gamma>\<turnstile>\<langle>call_exn init p return' result_exn c ,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_call_exnStuck)
from valid_call [rule_format] ctxt this P t_notin_F
show ?thesis
by (rule cnvalidD)
@ -1537,14 +1545,49 @@ proof (rule cnvalidI)
fix m
assume "\<Gamma> p = None"
and "n = Suc m" "t = Stuck"
then have "\<Gamma>\<turnstile>\<langle>call init p return' c ,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_callUndefined)
then have "\<Gamma>\<turnstile>\<langle>call_exn init p return' result_exn c ,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_call_exnUndefined)
from valid_call [rule_format] ctxt this P t_notin_F
show ?thesis
by (rule cnvalidD)
qed
qed
lemma ProcModifyReturnSameFaults_sound:
assumes valid_call: "\<forall>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P call init p return' c Q,A"
assumes valid_modif:
"\<forall>\<sigma>. \<forall>n. \<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> {\<sigma>} Call p (Modif \<sigma>),(ModifAbr \<sigma>)"
assumes ret_modif:
"\<forall>s t. t \<in> Modif (init s)
\<longrightarrow> return' s t = return s t"
assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s)
\<longrightarrow> return' s t = return s t"
shows "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P (call init p return c) Q,A"
using valid_call valid_modif ret_modif ret_modifAbr
unfolding call_call_exn
by (rule Proc_exnModifyReturnSameFaults_sound)
lemma Proc_exnModifyReturnSameFaults:
assumes spec: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (call_exn init p return' result_exn c) Q,A"
assumes result_conform:
"\<forall>s t. t \<in> Modif (init s) \<longrightarrow> (return' s t) = (return s t)"
assumes return_conform:
"\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> (result_exn (return' s t) t) = (result_exn (return s t) t)"
assumes modifies_spec:
"\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} Call p (Modif \<sigma>),(ModifAbr \<sigma>)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (call_exn init p return result_exn c) Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule Proc_exnModifyReturnSameFaults_sound
[where Modif=Modif and ModifAbr=ModifAbr,
OF _ _ result_conform return_conform])
using spec
apply (blast intro: hoare_cnvalid)
using modifies_spec
apply (blast intro: hoare_cnvalid)
done
lemma ProcModifyReturnSameFaults:
assumes spec: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (call init p return' c) Q,A"
@ -1554,20 +1597,146 @@ lemma ProcModifyReturnSameFaults:
"\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> (return' s t) = (return s t)"
assumes modifies_spec:
"\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} Call p (Modif \<sigma>),(ModifAbr \<sigma>)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (call init p return c) Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule ProcModifyReturnSameFaults_sound
[where Modif=Modif and ModifAbr=ModifAbr,
OF _ _ result_conform return_conform])
using spec
apply (blast intro: hoare_cnvalid)
using modifies_spec
apply (blast intro: hoare_cnvalid)
done
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (call init p return c) Q,A"
using spec result_conform return_conform modifies_spec
unfolding call_call_exn
by (rule Proc_exnModifyReturnSameFaults)
subsubsection \<open>DynCall\<close>
lemma dynProc_exnModifyReturn_sound:
assumes valid_call: "\<And>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P dynCall_exn f g init p return' result_exn c Q,A"
assumes valid_modif:
"\<forall>s \<in> P. \<forall>\<sigma>. \<forall>n.
\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/UNIV\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),(ModifAbr \<sigma>)"
assumes ret_modif:
"\<forall>s t. t \<in> Modif (init s)
\<longrightarrow> return' s t = return s t"
assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s)
\<longrightarrow> result_exn (return' s t) t = result_exn (return s t) t"
shows "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P (dynCall_exn f g init p return result_exn c) Q,A"
proof (rule cnvalidI)
fix s t
assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
then have ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/UNIV\<^esub> P (Call p) Q,A"
by (auto intro: nvalid_augment_Faults)
assume exec: "\<Gamma>\<turnstile>\<langle>dynCall_exn f g init p return result_exn c,Normal s\<rangle> =n\<Rightarrow> t"
assume t_notin_F: "t \<notin> Fault ` F"
assume P: "s \<in> P"
with valid_modif
have valid_modif': "\<forall>\<sigma>. \<forall>n.
\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/UNIV\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),(ModifAbr \<sigma>)"
by blast
from exec thm execn_Normal_elim_cases
have exec_call: "\<Gamma>\<turnstile>\<langle>maybe_guard f g (call_exn init (p s) return result_exn c),Normal s\<rangle> =n\<Rightarrow> t"
by (cases rule: execn_dynCall_exn_Normal_elim)
then show "t \<in> Normal ` Q \<union> Abrupt ` A"
proof (cases rule: execn_maybe_guard_Normal_elim_cases)
case noFault
from noFault have guards_ok: "s \<in> g" by simp
from noFault have "\<Gamma>\<turnstile> \<langle>call_exn init (p s) return result_exn c,Normal s\<rangle> =n\<Rightarrow> t" by simp
then show "t \<in> Normal ` Q \<union> Abrupt ` A"
proof (cases rule: execn_call_exn_Normal_elim)
fix bdy m t'
assume bdy: "\<Gamma> (p s) = Some bdy"
assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Normal t'"
assume exec_c: "\<Gamma>\<turnstile>\<langle>c s t',Normal (return s t')\<rangle> =Suc m\<Rightarrow> t"
assume n: "n = Suc m"
from exec_body n bdy
have "\<Gamma>\<turnstile>\<langle>Call (p s) ,Normal (init s)\<rangle> =n\<Rightarrow> Normal t'"
by (auto simp add: intro: execn.intros)
from cnvalidD [OF valid_modif' [rule_format, of n "init s"] ctxt' this] P
have "t' \<in> Modif (init s)"
by auto
with ret_modif have "Normal (return' s t') = Normal (return s t')"
by simp
with exec_body exec_c bdy n
have "\<Gamma>\<turnstile>\<langle>call_exn init (p s) return' result_exn c,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_call_exn)
from execn_maybe_guard_noFault [OF this guards_ok]
have "\<Gamma>\<turnstile>\<langle>dynCall_exn f g init p return' result_exn c,Normal s\<rangle> =n\<Rightarrow> t"
by (simp add: dynCall_exn_def execn_maybe_guard_DynCom)
from cnvalidD [OF valid_call ctxt this] P t_notin_F
show ?thesis
by simp
next
fix bdy m t'
assume bdy: "\<Gamma> (p s) = Some bdy"
assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Abrupt t'"
assume n: "n = Suc m"
assume t: "t = Abrupt (result_exn (return s t') t')"
also from exec_body n bdy
have "\<Gamma>\<turnstile>\<langle>Call (p s) ,Normal (init s)\<rangle> =n\<Rightarrow> Abrupt t'"
by (auto simp add: intro: execn.intros)
from cnvalidD [OF valid_modif' [rule_format, of n "init s"] ctxt' this] P
have "t' \<in> ModifAbr (init s)"
by auto
with ret_modifAbr have "Abrupt (result_exn (return s t') t') = Abrupt (result_exn (return' s t') t')"
by simp
finally have "t = Abrupt (result_exn (return' s t') t')" .
with exec_body bdy n
have "\<Gamma>\<turnstile>\<langle>call_exn init (p s) return' result_exn c,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_call_exnAbrupt)
from execn_maybe_guard_noFault [OF this guards_ok]
have "\<Gamma>\<turnstile>\<langle>dynCall_exn f g init p return' result_exn c,Normal s\<rangle> =n\<Rightarrow> t"
by (simp add: dynCall_exn_def execn_maybe_guard_DynCom)
from cnvalidD [OF valid_call ctxt this] P t_notin_F
show ?thesis
by simp
next
fix bdy m f'
assume bdy: "\<Gamma> (p s) = Some bdy"
assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Fault f'" "n = Suc m"
"t = Fault f'"
with bdy have "\<Gamma>\<turnstile>\<langle>call_exn init (p s) return' result_exn c ,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_call_exnFault)
from execn_maybe_guard_noFault [OF this guards_ok]
have "\<Gamma>\<turnstile>\<langle>dynCall_exn f g init p return' result_exn c,Normal s\<rangle> =n\<Rightarrow> t"
by (simp add: dynCall_exn_def execn_maybe_guard_DynCom)
from valid_call ctxt this P t_notin_F
show ?thesis
by (rule cnvalidD)
next
fix bdy m
assume bdy: "\<Gamma> (p s) = Some bdy"
assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Stuck" "n = Suc m"
"t = Stuck"
with bdy have "\<Gamma>\<turnstile>\<langle>call_exn init (p s) return' result_exn c ,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_call_exnStuck)
from execn_maybe_guard_noFault [OF this guards_ok]
have "\<Gamma>\<turnstile>\<langle>dynCall_exn f g init p return' result_exn c,Normal s\<rangle> =n\<Rightarrow> t"
by (simp add: dynCall_exn_def execn_maybe_guard_DynCom)
from valid_call ctxt this P t_notin_F
show ?thesis
by (rule cnvalidD)
next
fix m
assume "\<Gamma> (p s) = None"
and "n = Suc m" "t = Stuck"
hence "\<Gamma>\<turnstile>\<langle>call_exn init (p s) return' result_exn c ,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_call_exnUndefined)
from execn_maybe_guard_noFault [OF this guards_ok]
have "\<Gamma>\<turnstile>\<langle>dynCall_exn f g init p return' result_exn c,Normal s\<rangle> =n\<Rightarrow> t"
by (simp add: dynCall_exn_def execn_maybe_guard_DynCom)
from valid_call ctxt this P t_notin_F
show ?thesis
by (rule cnvalidD)
qed
next
case (someFault)
then obtain guards_fail:"s \<notin> g"
and t: "t = Fault f" by simp
from execn_maybe_guard_Fault [OF guards_fail] t
have "\<Gamma>\<turnstile>\<langle>dynCall_exn f g init p return' result_exn c,Normal s\<rangle> =n\<Rightarrow> t"
by (simp add: dynCall_exn_def execn_maybe_guard_DynCom)
from cnvalidD [OF valid_call ctxt this] P t_notin_F
show ?thesis by simp
qed
qed
lemma dynProcModifyReturn_sound:
assumes valid_call: "\<And>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P dynCall init p return' c Q,A"
assumes valid_modif:
@ -1579,104 +1748,30 @@ assumes ret_modif:
assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s)
\<longrightarrow> return' s t = return s t"
shows "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
proof (rule cnvalidI)
fix s t
assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
then have ctxt': "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/UNIV\<^esub> P (Call p) Q,A"
by (auto intro: nvalid_augment_Faults)
assume exec: "\<Gamma>\<turnstile>\<langle>dynCall init p return c,Normal s\<rangle> =n\<Rightarrow> t"
assume t_notin_F: "t \<notin> Fault ` F"
assume P: "s \<in> P"
with valid_modif
have valid_modif': "\<forall>\<sigma>. \<forall>n.
\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/UNIV\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),(ModifAbr \<sigma>)"
by blast
from exec
have "\<Gamma>\<turnstile>\<langle>call init (p s) return c,Normal s\<rangle> =n\<Rightarrow> t"
by (cases rule: execn_dynCall_Normal_elim)
then show "t \<in> Normal ` Q \<union> Abrupt ` A"
proof (cases rule: execn_call_Normal_elim)
fix bdy m t'
assume bdy: "\<Gamma> (p s) = Some bdy"
assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Normal t'"
assume exec_c: "\<Gamma>\<turnstile>\<langle>c s t',Normal (return s t')\<rangle> =Suc m\<Rightarrow> t"
assume n: "n = Suc m"
from exec_body n bdy
have "\<Gamma>\<turnstile>\<langle>Call (p s) ,Normal (init s)\<rangle> =n\<Rightarrow> Normal t'"
by (auto simp add: intro: execn.intros)
from cnvalidD [OF valid_modif' [rule_format, of n "init s"] ctxt' this] P
have "t' \<in> Modif (init s)"
by auto
with ret_modif have "Normal (return' s t') = Normal (return s t')"
by simp
with exec_body exec_c bdy n
have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_call)
hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t"
by (rule execn_dynCall)
from cnvalidD [OF valid_call ctxt this] P t_notin_F
show ?thesis
by simp
next
fix bdy m t'
assume bdy: "\<Gamma> (p s) = Some bdy"
assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Abrupt t'"
assume n: "n = Suc m"
assume t: "t = Abrupt (return s t')"
also from exec_body n bdy
have "\<Gamma>\<turnstile>\<langle>Call (p s) ,Normal (init s)\<rangle> =n\<Rightarrow> Abrupt t'"
by (auto simp add: intro: execn.intros)
from cnvalidD [OF valid_modif' [rule_format, of n "init s"] ctxt' this] P
have "t' \<in> ModifAbr (init s)"
by auto
with ret_modifAbr have "Abrupt (return s t') = Abrupt (return' s t')"
by simp
finally have "t = Abrupt (return' s t')" .
with exec_body bdy n
have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_callAbrupt)
hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t"
by (rule execn_dynCall)
from cnvalidD [OF valid_call ctxt this] P t_notin_F
show ?thesis
by simp
next
fix bdy m f
assume bdy: "\<Gamma> (p s) = Some bdy"
assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Fault f" "n = Suc m"
"t = Fault f"
with bdy have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_callFault)
hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t"
by (rule execn_dynCall)
from valid_call ctxt this P t_notin_F
show ?thesis
by (rule cnvalidD)
next
fix bdy m
assume bdy: "\<Gamma> (p s) = Some bdy"
assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Stuck" "n = Suc m"
"t = Stuck"
with bdy have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_callStuck)
hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t"
by (rule execn_dynCall)
from valid_call ctxt this P t_notin_F
show ?thesis
by (rule cnvalidD)
next
fix m
assume "\<Gamma> (p s) = None"
and "n = Suc m" "t = Stuck"
hence "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_callUndefined)
hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t"
by (rule execn_dynCall)
from valid_call ctxt this P t_notin_F
show ?thesis
by (rule cnvalidD)
qed
qed
using valid_call valid_modif ret_modif ret_modifAbr
unfolding dynCall_dynCall_exn
by (rule dynProc_exnModifyReturn_sound)
lemma dynProc_exnModifyReturn:
assumes dyn_call: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P dynCall_exn f g init p return' result_exn c Q,A"
assumes ret_modif:
"\<forall>s t. t \<in> Modif (init s)
\<longrightarrow> return' s t = return s t"
assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s)
\<longrightarrow> result_exn (return' s t) t = result_exn (return s t) t"
assumes modif:
"\<forall>s \<in> P. \<forall>\<sigma>.
\<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),(ModifAbr \<sigma>)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall_exn f g init p return result_exn c) Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule dynProc_exnModifyReturn_sound [where Modif=Modif and ModifAbr=ModifAbr,
OF hoare_cnvalid [OF dyn_call] _ ret_modif ret_modifAbr])
apply (intro ballI allI)
apply (rule hoare_cnvalid [OF modif [rule_format]])
apply assumption
done
lemma dynProcModifyReturn:
assumes dyn_call: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P dynCall init p return' c Q,A"
@ -1688,15 +1783,138 @@ assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s)
assumes modif:
"\<forall>s \<in> P. \<forall>\<sigma>.
\<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),(ModifAbr \<sigma>)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule dynProcModifyReturn_sound [where Modif=Modif and ModifAbr=ModifAbr,
OF hoare_cnvalid [OF dyn_call] _ ret_modif ret_modifAbr])
apply (intro ballI allI)
apply (rule hoare_cnvalid [OF modif [rule_format]])
apply assumption
done
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
using dyn_call ret_modif ret_modifAbr modif
unfolding dynCall_dynCall_exn
by (rule dynProc_exnModifyReturn)
lemma dynProc_exnModifyReturnSameFaults_sound:
assumes valid_call: "\<And>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P dynCall_exn f g init p return' result_exn c Q,A"
assumes valid_modif:
"\<forall>s \<in> P. \<forall>\<sigma>. \<forall>n.
\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),(ModifAbr \<sigma>)"
assumes ret_modif:
"\<forall>s t. t \<in> Modif (init s) \<longrightarrow> return' s t = return s t"
assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> result_exn (return' s t) t = result_exn (return s t) t"
shows "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P (dynCall_exn f g init p return result_exn c) Q,A"
proof (rule cnvalidI)
fix s t
assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
assume exec: "\<Gamma>\<turnstile>\<langle>dynCall_exn f g init p return result_exn c,Normal s\<rangle> =n\<Rightarrow> t"
assume t_notin_F: "t \<notin> Fault ` F"
assume P: "s \<in> P"
with valid_modif
have valid_modif': "\<forall>\<sigma>. \<forall>n.
\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),(ModifAbr \<sigma>)"
by blast
from exec
have exec_call: "\<Gamma>\<turnstile>\<langle>maybe_guard f g (call_exn init (p s) return result_exn c),Normal s\<rangle> =n\<Rightarrow> t"
by (cases rule: execn_dynCall_exn_Normal_elim)
then show "t \<in> Normal ` Q \<union> Abrupt ` A"
proof (cases rule: execn_maybe_guard_Normal_elim_cases)
case noFault
from noFault have guards_ok: "s \<in> g" by simp
from noFault have "\<Gamma>\<turnstile> \<langle>call_exn init (p s) return result_exn c,Normal s\<rangle> =n\<Rightarrow> t" by simp
then show "t \<in> Normal ` Q \<union> Abrupt ` A"
proof (cases rule: execn_call_exn_Normal_elim)
fix bdy m t'
assume bdy: "\<Gamma> (p s) = Some bdy"
assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Normal t'"
assume exec_c: "\<Gamma>\<turnstile>\<langle>c s t',Normal (return s t')\<rangle> =Suc m\<Rightarrow> t"
assume n: "n = Suc m"
from exec_body n bdy
have "\<Gamma>\<turnstile>\<langle>Call (p s) ,Normal (init s)\<rangle> =n \<Rightarrow> Normal t'"
by (auto simp add: intro: execn.Call)
from cnvalidD [OF valid_modif' [rule_format, of n "init s"] ctxt this] P
have "t' \<in> Modif (init s)"
by auto
with ret_modif have "Normal (return' s t') = Normal (return s t')"
by simp
with exec_body exec_c bdy n
have "\<Gamma>\<turnstile>\<langle>call_exn init (p s) return' result_exn c,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_call_exn)
from execn_maybe_guard_noFault [OF this guards_ok]
have "\<Gamma>\<turnstile>\<langle>dynCall_exn f g init p return' result_exn c,Normal s\<rangle> =n\<Rightarrow> t"
by (simp add: dynCall_exn_def execn_maybe_guard_DynCom)
from cnvalidD [OF valid_call ctxt this] P t_notin_F
show ?thesis
by simp
next
fix bdy m t'
assume bdy: "\<Gamma> (p s) = Some bdy"
assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Abrupt t'"
assume n: "n = Suc m"
assume t: "t = Abrupt (result_exn (return s t') t')"
also from exec_body n bdy
have "\<Gamma>\<turnstile>\<langle>Call (p s) ,Normal (init s)\<rangle> =n \<Rightarrow> Abrupt t'"
by (auto simp add: intro: execn.intros)
from cnvalidD [OF valid_modif' [rule_format, of n "init s"] ctxt this] P
have "t' \<in> ModifAbr (init s)"
by auto
with ret_modifAbr have "Abrupt (result_exn (return s t') t') = Abrupt (result_exn (return' s t') t')"
by simp
finally have "t = Abrupt (result_exn (return' s t') t')" .
with exec_body bdy n
have "\<Gamma>\<turnstile>\<langle>call_exn init (p s) return' result_exn c,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_call_exnAbrupt)
from execn_maybe_guard_noFault [OF this guards_ok]
have "\<Gamma>\<turnstile>\<langle>dynCall_exn f g init p return' result_exn c,Normal s\<rangle> =n\<Rightarrow> t"
by (simp add: dynCall_exn_def execn_maybe_guard_DynCom)
from cnvalidD [OF valid_call ctxt this] P t_notin_F
show ?thesis
by simp
next
fix bdy m f'
assume bdy: "\<Gamma> (p s) = Some bdy"
assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Fault f'" "n = Suc m" and
t: "t = Fault f'"
with bdy have "\<Gamma>\<turnstile>\<langle>call_exn init (p s) return' result_exn c ,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_call_exnFault)
from execn_maybe_guard_noFault [OF this guards_ok]
have "\<Gamma>\<turnstile>\<langle>dynCall_exn f g init p return' result_exn c,Normal s\<rangle> =n\<Rightarrow> t"
by (simp add: dynCall_exn_def execn_maybe_guard_DynCom)
from cnvalidD [OF valid_call ctxt this P] t t_notin_F
show ?thesis
by simp
next
fix bdy m
assume bdy: "\<Gamma> (p s) = Some bdy"
assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Stuck" "n = Suc m"
"t = Stuck"
with bdy have "\<Gamma>\<turnstile>\<langle>call_exn init (p s) return' result_exn c ,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_call_exnStuck)
from execn_maybe_guard_noFault [OF this guards_ok]
have "\<Gamma>\<turnstile>\<langle>dynCall_exn f g init p return' result_exn c,Normal s\<rangle> =n\<Rightarrow> t"
by (simp add: dynCall_exn_def execn_maybe_guard_DynCom)
from valid_call ctxt this P t_notin_F
show ?thesis
by (rule cnvalidD)
next
fix m
assume "\<Gamma> (p s) = None"
and "n = Suc m" "t = Stuck"
hence "\<Gamma>\<turnstile>\<langle>call_exn init (p s) return' result_exn c ,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_call_exnUndefined)
from execn_maybe_guard_noFault [OF this guards_ok]
have "\<Gamma>\<turnstile>\<langle>dynCall_exn f g init p return' result_exn c,Normal s\<rangle> =n\<Rightarrow> t"
by (simp add: dynCall_exn_def execn_maybe_guard_DynCom)
from valid_call ctxt this P t_notin_F
show ?thesis
by (rule cnvalidD)
qed
next
case (someFault)
then obtain guards_fail:"s \<notin> g"
and t: "t = Fault f" by simp
from execn_maybe_guard_Fault [OF guards_fail] t
have "\<Gamma>\<turnstile>\<langle>dynCall_exn f g init p return' result_exn c,Normal s\<rangle> =n\<Rightarrow> t"
by (simp add: dynCall_exn_def execn_guards_DynCom)
from cnvalidD [OF valid_call ctxt this] P t_notin_F
show ?thesis by simp
qed
qed
lemma dynProcModifyReturnSameFaults_sound:
assumes valid_call: "\<And>n. \<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P dynCall init p return' c Q,A"
@ -1707,102 +1925,29 @@ assumes ret_modif:
"\<forall>s t. t \<in> Modif (init s) \<longrightarrow> return' s t = return s t"
assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s) \<longrightarrow> return' s t = return s t"
shows "\<Gamma>,\<Theta> \<Turnstile>n:\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
proof (rule cnvalidI)
fix s t
assume ctxt: "\<forall>(P, p, Q, A)\<in>\<Theta>. \<Gamma> \<Turnstile>n:\<^bsub>/F\<^esub> P (Call p) Q,A"
assume exec: "\<Gamma>\<turnstile>\<langle>dynCall init p return c,Normal s\<rangle> =n\<Rightarrow> t"
assume t_notin_F: "t \<notin> Fault ` F"
assume P: "s \<in> P"
with valid_modif
have valid_modif': "\<forall>\<sigma>. \<forall>n.
\<Gamma>,\<Theta>\<Turnstile>n:\<^bsub>/F\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),(ModifAbr \<sigma>)"
by blast
from exec
have "\<Gamma>\<turnstile>\<langle>call init (p s) return c,Normal s\<rangle> =n\<Rightarrow> t"
by (cases rule: execn_dynCall_Normal_elim)
then show "t \<in> Normal ` Q \<union> Abrupt ` A"
proof (cases rule: execn_call_Normal_elim)
fix bdy m t'
assume bdy: "\<Gamma> (p s) = Some bdy"
assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Normal t'"
assume exec_c: "\<Gamma>\<turnstile>\<langle>c s t',Normal (return s t')\<rangle> =Suc m\<Rightarrow> t"
assume n: "n = Suc m"
from exec_body n bdy
have "\<Gamma>\<turnstile>\<langle>Call (p s) ,Normal (init s)\<rangle> =n \<Rightarrow> Normal t'"
by (auto simp add: intro: execn.Call)
from cnvalidD [OF valid_modif' [rule_format, of n "init s"] ctxt this] P
have "t' \<in> Modif (init s)"
by auto
with ret_modif have "Normal (return' s t') = Normal (return s t')"
by simp
with exec_body exec_c bdy n
have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_call)
hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t"
by (rule execn_dynCall)
from cnvalidD [OF valid_call ctxt this] P t_notin_F
show ?thesis
by simp
next
fix bdy m t'
assume bdy: "\<Gamma> (p s) = Some bdy"
assume exec_body: "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Abrupt t'"
assume n: "n = Suc m"
assume t: "t = Abrupt (return s t')"
also from exec_body n bdy
have "\<Gamma>\<turnstile>\<langle>Call (p s) ,Normal (init s)\<rangle> =n \<Rightarrow> Abrupt t'"
by (auto simp add: intro: execn.intros)
from cnvalidD [OF valid_modif' [rule_format, of n "init s"] ctxt this] P
have "t' \<in> ModifAbr (init s)"
by auto
with ret_modifAbr have "Abrupt (return s t') = Abrupt (return' s t')"
by simp
finally have "t = Abrupt (return' s t')" .
with exec_body bdy n
have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_callAbrupt)
hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t"
by (rule execn_dynCall)
from cnvalidD [OF valid_call ctxt this] P t_notin_F
show ?thesis
by simp
next
fix bdy m f
assume bdy: "\<Gamma> (p s) = Some bdy"
assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Fault f" "n = Suc m" and
t: "t = Fault f"
with bdy have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_callFault)
hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t"
by (rule execn_dynCall)
from cnvalidD [OF valid_call ctxt this P] t t_notin_F
show ?thesis
by simp
next
fix bdy m
assume bdy: "\<Gamma> (p s) = Some bdy"
assume "\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =m\<Rightarrow> Stuck" "n = Suc m"
"t = Stuck"
with bdy have "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_callStuck)
hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t"
by (rule execn_dynCall)
from valid_call ctxt this P t_notin_F
show ?thesis
by (rule cnvalidD)
next
fix m
assume "\<Gamma> (p s) = None"
and "n = Suc m" "t = Stuck"
hence "\<Gamma>\<turnstile>\<langle>call init (p s) return' c ,Normal s\<rangle> =n\<Rightarrow> t"
by (auto intro: execn_callUndefined)
hence "\<Gamma>\<turnstile>\<langle>dynCall init p return' c,Normal s\<rangle> =n\<Rightarrow> t"
by (rule execn_dynCall)
from valid_call ctxt this P t_notin_F
show ?thesis
by (rule cnvalidD)
qed
qed
using valid_call valid_modif ret_modif ret_modifAbr
unfolding dynCall_dynCall_exn
by (rule dynProc_exnModifyReturnSameFaults_sound)
lemma dynProc_exnModifyReturnSameFaults:
assumes dyn_call: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P dynCall_exn f g init p return' result_exn c Q,A"
assumes ret_modif:
"\<forall>s t. t \<in> Modif (init s)
\<longrightarrow> return' s t = return s t"
assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s)
\<longrightarrow> result_exn (return' s t) t = result_exn (return s t) t"
assumes modif:
"\<forall>s \<in> P. \<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),(ModifAbr \<sigma>)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall_exn f g init p return result_exn c) Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule dynProc_exnModifyReturnSameFaults_sound
[where Modif=Modif and ModifAbr=ModifAbr,
OF hoare_cnvalid [OF dyn_call] _ ret_modif ret_modifAbr])
apply (intro ballI allI)
apply (rule hoare_cnvalid [OF modif [rule_format]])
apply assumption
done
lemma dynProcModifyReturnSameFaults:
assumes dyn_call: "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P dynCall init p return' c Q,A"
@ -1813,16 +1958,10 @@ assumes ret_modifAbr: "\<forall>s t. t \<in> ModifAbr (init s)
\<longrightarrow> return' s t = return s t"
assumes modif:
"\<forall>s \<in> P. \<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),(ModifAbr \<sigma>)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
apply (rule hoare_complete')
apply (rule allI)
apply (rule dynProcModifyReturnSameFaults_sound
[where Modif=Modif and ModifAbr=ModifAbr,
OF hoare_cnvalid [OF dyn_call] _ ret_modif ret_modifAbr])
apply (intro ballI allI)
apply (rule hoare_cnvalid [OF modif [rule_format]])
apply assumption
done
shows "\<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
using dyn_call ret_modif ret_modifAbr modif
unfolding dynCall_dynCall_exn
by (rule dynProc_exnModifyReturnSameFaults)
subsubsection \<open>Conjunction of Postcondition\<close>

403
tools/c-parser/Simpl/HoareTotal.thy
View File

@ -1,29 +1,10 @@
(*
Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: HoareTotal.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2004-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
Copyright (c) 2022 Apple Inc. All rights reserved.
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
section \<open>Derived Hoare Rules for Total Correctness\<close>
@ -475,18 +456,18 @@ using adapt
apply blast
done
lemma Block:
lemma Block_exn:
assumes adapt: "P \<subseteq> {s. init s \<in> P' s}"
assumes bdy: "\<forall>s. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' s) bdy {t. return s t \<in> R s t},{t. return s t \<in> A}"
assumes bdy: "\<forall>s. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' s) bdy {t. return s t \<in> R s t},{t. result_exn (return s t) t \<in> A}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (block init bdy return c) Q,A"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (block_exn init bdy return result_exn c) Q,A"
apply (rule conseq [where P'="\<lambda>Z. {s. s=Z \<and> init s \<in> P' Z}" and Q'="\<lambda>Z. Q" and
A'="\<lambda>Z. A"])
prefer 2
using adapt
apply blast
apply (rule allI)
apply (unfold block_def)
apply (unfold block_exn_def)
apply (rule HoareTotalDef.DynCom)
apply (rule ballI)
apply clarsimp
@ -501,7 +482,7 @@ apply (rule SeqSwap)
apply (rule c [rule_format])
apply (rule Basic)
apply clarsimp
apply (rule_tac R="{t. return Z t \<in> A}" in HoareTotalDef.Catch)
apply (rule_tac R="{t. result_exn (return Z t) t \<in> A}" in HoareTotalDef.Catch)
apply (rule_tac R="{i. i \<in> P' Z}" in Seq)
apply (rule Basic)
apply clarsimp
@ -513,6 +494,13 @@ apply (rule Basic)
apply simp
done
lemma Block:
assumes adapt: "P \<subseteq> {s. init s \<in> P' s}"
assumes bdy: "\<forall>s. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' s) bdy {t. return s t \<in> R s t},{t. return s t \<in> A}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (block init bdy return c) Q,A"
using adapt bdy c unfolding block_def by (rule Block_exn)
lemma BlockSwap:
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes bdy: "\<forall>s. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' s) bdy {t. return s t \<in> R s t},{t. return s t \<in> A}"
@ -521,22 +509,30 @@ shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (block init bdy
using adapt bdy c
by (rule Block)
lemma BlockSpec:
lemma Block_exnSwap:
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes bdy: "\<forall>s. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' s) bdy {t. return s t \<in> R s t},{t. result_exn (return s t) t \<in> A}"
assumes adapt: "P \<subseteq> {s. init s \<in> P' s}"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (block_exn init bdy return result_exn c) Q,A"
using adapt bdy c
by (rule Block_exn)
lemma Block_exnSpec:
assumes adapt: "P \<subseteq> {s. \<exists>Z. init s \<in> P' Z \<and>
(\<forall>t. t \<in> Q' Z \<longrightarrow> return s t \<in> R s t) \<and>
(\<forall>t. t \<in> A' Z \<longrightarrow> return s t \<in> A)}"
(\<forall>t. t \<in> A' Z \<longrightarrow> result_exn (return s t) t \<in> A)}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes bdy: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) bdy (Q' Z),(A' Z)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (block init bdy return c) Q,A"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (block_exn init bdy return result_exn c) Q,A"
apply (rule conseq [where P'="\<lambda>Z. {s. init s \<in> P' Z \<and>
(\<forall>t. t \<in> Q' Z \<longrightarrow> return s t \<in> R s t) \<and>
(\<forall>t. t \<in> A' Z \<longrightarrow> return s t \<in> A)}" and Q'="\<lambda>Z. Q" and
(\<forall>t. t \<in> A' Z \<longrightarrow> result_exn (return s t) t \<in> A)}" and Q'="\<lambda>Z. Q" and
A'="\<lambda>Z. A"])
prefer 2
using adapt
apply blast
apply (rule allI)
apply (unfold block_def)
apply (unfold block_exn_def)
apply (rule HoareTotalDef.DynCom)
apply (rule ballI)
apply clarsimp
@ -551,7 +547,7 @@ apply (rule SeqSwap)
apply (rule c [rule_format])
apply (rule Basic)
apply clarsimp
apply (rule_tac R="{t. return s t \<in> A}" in HoareTotalDef.Catch)
apply (rule_tac R="{t. result_exn (return s t) t \<in> A}" in HoareTotalDef.Catch)
apply (rule_tac R="{i. i \<in> P' Z}" in Seq)
apply (rule Basic)
apply clarsimp
@ -565,6 +561,15 @@ apply (rule Basic)
apply simp
done
lemma BlockSpec:
assumes adapt: "P \<subseteq> {s. \<exists>Z. init s \<in> P' Z \<and>
(\<forall>t. t \<in> Q' Z \<longrightarrow> return s t \<in> R s t) \<and>
(\<forall>t. t \<in> A' Z \<longrightarrow> return s t \<in> A)}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes bdy: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) bdy (Q' Z),(A' Z)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (block init bdy return c) Q,A"
using adapt c bdy unfolding block_def by (rule Block_exnSpec)
lemma Throw: "P \<subseteq> A \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P Throw Q,A"
by (rule hoaret.Throw [THEN conseqPre])
@ -597,6 +602,16 @@ lemma condCatchSwap: "\<lbrakk>\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<
\<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P condCatch c\<^sub>1 b c\<^sub>2 Q,A"
by (rule condCatch)
lemma Proc_exnSpec:
assumes adapt: "P \<subseteq> {s. \<exists>Z. init s \<in> P' Z \<and>
(\<forall>t. t \<in> Q' Z \<longrightarrow> return s t \<in> R s t) \<and>
(\<forall>t. t \<in> A' Z \<longrightarrow> result_exn (return s t) t \<in> A)}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes p: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) Call p (Q' Z),(A' Z)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call_exn init p return result_exn c) Q,A"
using adapt c p
apply (unfold call_exn_def)
by (rule Block_exnSpec)
lemma ProcSpec:
assumes adapt: "P \<subseteq> {s. \<exists>Z. init s \<in> P' Z \<and>
@ -609,14 +624,14 @@ using adapt c p
apply (unfold call_def)
by (rule BlockSpec)
lemma ProcSpec':
lemma Proc_exnSpec':
assumes adapt: "P \<subseteq> {s. \<exists>Z. init s \<in> P' Z \<and>
(\<forall>t \<in> Q' Z. return s t \<in> R s t) \<and>
(\<forall>t \<in> A' Z. return s t \<in> A)}"
(\<forall>t \<in> A' Z. result_exn (return s t) t \<in> A)}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes p: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) Call p (Q' Z),(A' Z)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return c) Q,A"
apply (rule ProcSpec [OF _ c p])
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call_exn init p return result_exn c) Q,A"
apply (rule Proc_exnSpec [OF _ c p])
apply (insert adapt)
apply clarsimp
apply (drule (1) subsetD)
@ -625,6 +640,26 @@ apply (rule_tac x=Z in exI)
apply blast
done
lemma ProcSpec':
assumes adapt: "P \<subseteq> {s. \<exists>Z. init s \<in> P' Z \<and>
(\<forall>t \<in> Q' Z. return s t \<in> R s t) \<and>
(\<forall>t \<in> A' Z. return s t \<in> A)}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes p: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) Call p (Q' Z),(A' Z)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return c) Q,A"
using adapt c p unfolding call_call_exn by (rule Proc_exnSpec')
lemma Proc_exnSpecNoAbrupt:
assumes adapt: "P \<subseteq> {s. \<exists>Z. init s \<in> P' Z \<and>
(\<forall>t. t \<in> Q' Z \<longrightarrow> return s t \<in> R s t)}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes p: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) Call p (Q' Z),{}"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call_exn init p return result_exn c) Q,A"
apply (rule Proc_exnSpec [OF _ c p])
using adapt
apply simp
done
lemma ProcSpecNoAbrupt:
assumes adapt: "P \<subseteq> {s. \<exists>Z. init s \<in> P' Z \<and>
@ -764,9 +799,25 @@ apply (rule ProcBody [where \<Gamma>=\<Gamma>, OF _ bdy [rule_format] body])
apply simp
done
lemma Call_exnBody:
assumes adapt: "P \<subseteq> {s. init s \<in> P' s}"
assumes bdy: "\<forall>s. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' s) body {t. return s t \<in> R s t},{t. result_exn (return s t) t \<in> A}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes body: "\<Gamma> p = Some body"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call_exn init p return result_exn c) Q,A"
apply (unfold call_exn_def)
apply (rule Block_exn [OF adapt _ c])
apply (rule allI)
apply (rule ProcBody [where \<Gamma>=\<Gamma>, OF _ bdy [rule_format] body])
apply simp
done
lemmas ProcModifyReturn = HoareTotalProps.ProcModifyReturn
lemmas ProcModifyReturnSameFaults = HoareTotalProps.ProcModifyReturnSameFaults
lemmas Proc_exnModifyReturn = HoareTotalProps.Proc_exnModifyReturn
lemmas Proc_exnModifyReturnSameFaults = HoareTotalProps.Proc_exnModifyReturnSameFaults
lemma ProcModifyReturnNoAbr:
assumes spec: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return' c) Q,A"
assumes result_conform:
@ -776,6 +827,15 @@ lemma ProcModifyReturnNoAbr:
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return c) Q,A"
by (rule ProcModifyReturn [OF spec result_conform _ modifies_spec]) simp
lemma Proc_exnModifyReturnNoAbr:
assumes spec: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call_exn init p return' result_exn c) Q,A"
assumes result_conform:
"\<forall>s t. t \<in> Modif (init s) \<longrightarrow> (return' s t) = (return s t)"
assumes modifies_spec:
"\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} Call p (Modif \<sigma>),{}"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call_exn init p return result_exn c) Q,A"
by (rule Proc_exnModifyReturn [OF spec result_conform _ modifies_spec]) simp
lemma ProcModifyReturnNoAbrSameFaults:
assumes spec: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return' c) Q,A"
@ -786,21 +846,29 @@ lemma ProcModifyReturnNoAbrSameFaults:
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call init p return c) Q,A"
by (rule ProcModifyReturnSameFaults [OF spec result_conform _ modifies_spec]) simp
lemma Proc_exnModifyReturnNoAbrSameFaults:
assumes spec: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call_exn init p return' result_exn c) Q,A"
assumes result_conform:
"\<forall>s t. t \<in> Modif (init s) \<longrightarrow> (return' s t) = (return s t)"
assumes modifies_spec:
"\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} Call p (Modif \<sigma>),{}"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (call_exn init p return result_exn c) Q,A"
by (rule Proc_exnModifyReturnSameFaults [OF spec result_conform _ modifies_spec]) simp
lemma DynProc:
lemma DynProc_exn:
assumes adapt: "P \<subseteq> {s. \<exists>Z. init s \<in> P' s Z \<and>
(\<forall>t. t \<in> Q' s Z \<longrightarrow> return s t \<in> R s t) \<and>
(\<forall>t. t \<in> A' s Z \<longrightarrow> return s t \<in> A)}"
(\<forall>t. t \<in> A' s Z \<longrightarrow> result_exn (return s t) t \<in> A)}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes p: "\<forall>s\<in> P. \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' s Z) Call (p s) (Q' s Z),(A' s Z)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P dynCall init p return c Q,A"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P dynCall_exn f UNIV init p return result_exn c Q,A"
apply (rule conseq [where P'="\<lambda>Z. {s. s=Z \<and> s \<in> P}"
and Q'="\<lambda>Z. Q" and A'="\<lambda>Z. A"])
prefer 2
using adapt
apply blast
apply (rule allI)
apply (unfold dynCall_def call_def block_def)
apply (unfold dynCall_exn_def maybe_guard_UNIV call_exn_def block_exn_def guards.simps)
apply (rule HoareTotalDef.DynCom)
apply clarsimp
apply (rule HoareTotalDef.DynCom)
@ -834,7 +902,41 @@ apply (rule SeqSwap)
apply (rule c [rule_format])
apply (rule Basic)
apply clarsimp
done
done
lemma DynProc_exn_guards_cons:
assumes p: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P dynCall_exn f UNIV init p return result_exn c Q,A"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (g \<inter> P) dynCall_exn f g init p return result_exn c Q,A"
using p apply (clarsimp simp add: dynCall_exn_def maybe_guard_def)
apply (rule Guard)
apply (rule subset_refl)
apply assumption
done
lemma DynProc:
assumes adapt: "P \<subseteq> {s. \<exists>Z. init s \<in> P' s Z \<and>
(\<forall>t. t \<in> Q' s Z \<longrightarrow> return s t \<in> R s t) \<and>
(\<forall>t. t \<in> A' s Z \<longrightarrow> return s t \<in> A)}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes p: "\<forall>s\<in> P. \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' s Z) Call (p s) (Q' s Z),(A' s Z)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P dynCall init p return c Q,A"
using adapt c p unfolding dynCall_dynCall_exn by (rule DynProc_exn)
lemma DynProc_exn':
assumes adapt: "P \<subseteq> {s. \<exists>Z. init s \<in> P' s Z \<and>
(\<forall>t \<in> Q' s Z. return s t \<in> R s t) \<and>
(\<forall>t \<in> A' s Z. result_exn (return s t) t \<in> A)}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes p: "\<forall>s\<in> P. \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' s Z) Call (p s) (Q' s Z),(A' s Z)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P dynCall_exn f UNIV init p return result_exn c Q,A"
proof -
from adapt have "P \<subseteq> {s. \<exists>Z. init s \<in> P' s Z \<and>
(\<forall>t. t \<in> Q' s Z \<longrightarrow> return s t \<in> R s t) \<and>
(\<forall>t. t \<in> A' s Z \<longrightarrow> result_exn (return s t) t \<in> A)}"
by blast
from this c p show ?thesis
by (rule DynProc_exn)
qed
lemma DynProc':
assumes adapt: "P \<subseteq> {s. \<exists>Z. init s \<in> P' s Z \<and>
@ -843,27 +945,20 @@ lemma DynProc':
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes p: "\<forall>s\<in> P. \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' s Z) Call (p s) (Q' s Z),(A' s Z)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P dynCall init p return c Q,A"
proof -
from adapt have "P \<subseteq> {s. \<exists>Z. init s \<in> P' s Z \<and>
(\<forall>t. t \<in> Q' s Z \<longrightarrow> return s t \<in> R s t) \<and>
(\<forall>t. t \<in> A' s Z \<longrightarrow> return s t \<in> A)}"
by blast
from this c p show ?thesis
by (rule DynProc)
qed
using adapt c p unfolding dynCall_dynCall_exn by (rule DynProc_exn')
lemma DynProcStaticSpec:
lemma DynProc_exnStaticSpec:
assumes adapt: "P \<subseteq> {s. s \<in> S \<and> (\<exists>Z. init s \<in> P' Z \<and>
(\<forall>\<tau>. \<tau> \<in> Q' Z \<longrightarrow> return s \<tau> \<in> R s \<tau>) \<and>
(\<forall>\<tau>. \<tau> \<in> A' Z \<longrightarrow> return s \<tau> \<in> A))}"
(\<forall>\<tau>. \<tau> \<in> A' Z \<longrightarrow> result_exn (return s \<tau>) \<tau> \<in> A))}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes spec: "\<forall>s\<in>S. \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) Call (p s) (Q' Z),(A' Z)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall_exn f UNIV init p return result_exn c) Q,A"
proof -
from adapt have P_S: "P \<subseteq> S"
by blast
have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P \<inter> S) (dynCall init p return c) Q,A"
apply (rule DynProc [where P'="\<lambda>s Z. P' Z" and Q'="\<lambda>s Z. Q' Z"
have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P \<inter> S) (dynCall_exn f UNIV init p return result_exn c) Q,A"
apply (rule DynProc_exn [where P'="\<lambda>s Z. P' Z" and Q'="\<lambda>s Z. Q' Z"
and A'="\<lambda>s Z. A' Z", OF _ c])
apply clarsimp
apply (frule in_mono [rule_format, OF adapt])
@ -876,6 +971,26 @@ proof -
qed
lemma DynProcStaticSpec:
assumes adapt: "P \<subseteq> {s. s \<in> S \<and> (\<exists>Z. init s \<in> P' Z \<and>
(\<forall>\<tau>. \<tau> \<in> Q' Z \<longrightarrow> return s \<tau> \<in> R s \<tau>) \<and>
(\<forall>\<tau>. \<tau> \<in> A' Z \<longrightarrow> return s \<tau> \<in> A))}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes spec: "\<forall>s\<in>S. \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) Call (p s) (Q' Z),(A' Z)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
using adapt c spec unfolding dynCall_dynCall_exn by (rule DynProc_exnStaticSpec)
lemma DynProc_exnProcPar:
assumes adapt: "P \<subseteq> {s. p s = q \<and> (\<exists>Z. init s \<in> P' Z \<and>
(\<forall>\<tau>. \<tau> \<in> Q' Z \<longrightarrow> return s \<tau> \<in> R s \<tau>) \<and>
(\<forall>\<tau>. \<tau> \<in> A' Z \<longrightarrow> result_exn (return s \<tau>) \<tau> \<in> A))}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes spec: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) Call q (Q' Z),(A' Z)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall_exn f UNIV init p return result_exn c) Q,A"
apply (rule DynProc_exnStaticSpec [where S="{s. p s = q}",simplified, OF adapt c])
using spec
apply simp
done
lemma DynProcProcPar:
assumes adapt: "P \<subseteq> {s. p s = q \<and> (\<exists>Z. init s \<in> P' Z \<and>
@ -889,17 +1004,16 @@ shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p
apply simp
done
lemma DynProcProcParNoAbrupt:
lemma DynProc_exnProcParNoAbrupt:
assumes adapt: "P \<subseteq> {s. p s = q \<and> (\<exists>Z. init s \<in> P' Z \<and>
(\<forall>\<tau>. \<tau> \<in> Q' Z \<longrightarrow> return s \<tau> \<in> R s \<tau>))}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes spec: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) Call q (Q' Z),{}"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall_exn f UNIV init p return result_exn c) Q,A"
proof -
have "P \<subseteq> {s. p s = q \<and> (\<exists> Z. init s \<in> P' Z \<and>
(\<forall>t. t \<in> Q' Z \<longrightarrow> return s t \<in> R s t) \<and>
(\<forall>t. t \<in> {} \<longrightarrow> return s t \<in> A))}"
(\<forall>t. t \<in> {} \<longrightarrow> result_exn (return s t) t \<in> A))}"
(is "P \<subseteq> ?P'")
proof
fix s
@ -918,19 +1032,60 @@ proof -
note P = this
show ?thesis
apply -
apply (rule DynProcStaticSpec [where S="{s. p s = q}",simplified, OF P c])
apply (rule DynProc_exnStaticSpec [where S="{s. p s = q}",simplified, OF P c])
apply (insert spec)
apply auto
done
qed
lemma DynProcProcParNoAbrupt:
assumes adapt: "P \<subseteq> {s. p s = q \<and> (\<exists>Z. init s \<in> P' Z \<and>
(\<forall>\<tau>. \<tau> \<in> Q' Z \<longrightarrow> return s \<tau> \<in> R s \<tau>))}"
assumes c: "\<forall>s t. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (R s t) (c s t) Q,A"
assumes spec: "\<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (P' Z) Call q (Q' Z),{}"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
using adapt c spec unfolding dynCall_dynCall_exn by (rule DynProc_exnProcParNoAbrupt)
lemma DynProc_exnModifyReturnNoAbr:
assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall_exn f g init p return' result_exn c) Q,A"
assumes ret_nrm_modif: "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
assumes modif_clause:
"\<forall>s \<in> P. \<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),{}"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall_exn f g init p return result_exn c) Q,A"
proof -
from ret_nrm_modif
have "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
by iprover
then
have ret_nrm_modif': "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
by simp
have ret_abr_modif': "\<forall>s t. t \<in> {}
\<longrightarrow> result_exn (return' s t) t = result_exn (return s t) t"
by simp
from to_prove ret_nrm_modif' ret_abr_modif' modif_clause show ?thesis
by (rule dynProc_exnModifyReturn)
qed
lemma DynProcModifyReturnNoAbr:
assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return' c) Q,A"
assumes ret_nrm_modif: "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
assumes modif_clause:
"\<forall>s \<in> P. \<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} Call (p s) (Modif \<sigma>),{}"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
using to_prove ret_nrm_modif modif_clause unfolding dynCall_dynCall_exn
by (rule DynProc_exnModifyReturnNoAbr)
lemma ProcDyn_exnModifyReturnNoAbrSameFaults:
assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall_exn f g init p return' result_exn c) Q,A"
assumes ret_nrm_modif: "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
assumes modif_clause:
"\<forall>s \<in> P. \<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} (Call (p s)) (Modif \<sigma>),{}"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall_exn f g init p return result_exn c) Q,A"
proof -
from ret_nrm_modif
have "\<forall>s t. t \<in> (Modif (init s))
@ -941,33 +1096,44 @@ proof -
\<longrightarrow> return' s t = return s t"
by simp
have ret_abr_modif': "\<forall>s t. t \<in> {}
\<longrightarrow> return' s t = return s t"
\<longrightarrow> result_exn (return' s t) t = result_exn (return s t) t"
by simp
from to_prove ret_nrm_modif' ret_abr_modif' modif_clause show ?thesis
by (rule dynProcModifyReturn)
by (rule dynProc_exnModifyReturnSameFaults)
qed
lemma ProcDynModifyReturnNoAbrSameFaults:
assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return' c) Q,A"
assumes ret_nrm_modif: "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
assumes modif_clause:
"\<forall>s \<in> P. \<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} (Call (p s)) (Modif \<sigma>),{}"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
using to_prove ret_nrm_modif modif_clause unfolding dynCall_dynCall_exn
by (rule ProcDyn_exnModifyReturnNoAbrSameFaults)
lemma Proc_exnProcParModifyReturn:
assumes q: "P \<subseteq> {s. p s = q} \<inter> P'"
\<comment> \<open>@{thm[source] DynProcProcPar} introduces the same constraint as first conjunction in
@{term P'}, so the vcg can simplify it.\<close>
assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P' (dynCall_exn f g init p return' result_exn c) Q,A"
assumes ret_nrm_modif: "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
assumes ret_abr_modif: "\<forall>s t. t \<in> (ModifAbr (init s))
\<longrightarrow> result_exn (return' s t) t = result_exn (return s t) t"
assumes modif_clause:
"\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} (Call q) (Modif \<sigma>),(ModifAbr \<sigma>)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall_exn f g init p return result_exn c) Q,A"
proof -
from ret_nrm_modif
have "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
by iprover
then
have ret_nrm_modif': "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
by simp
have ret_abr_modif': "\<forall>s t. t \<in> {}
\<longrightarrow> return' s t = return s t"
by simp
from to_prove ret_nrm_modif' ret_abr_modif' modif_clause show ?thesis
by (rule dynProcModifyReturnSameFaults)
from to_prove have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall_exn f g init p return' result_exn c) Q,A"
by (rule conseqPre) blast
from this ret_nrm_modif
ret_abr_modif
have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall_exn f g init p return result_exn c) Q,A"
by (rule dynProc_exnModifyReturn) (insert modif_clause,auto)
from this q show ?thesis
by (rule conseqPre)
qed
lemma ProcProcParModifyReturn:
@ -981,20 +1147,35 @@ lemma ProcProcParModifyReturn:
\<longrightarrow> return' s t = return s t"
assumes modif_clause:
"\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} (Call q) (Modif \<sigma>),(ModifAbr \<sigma>)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
using q to_prove ret_nrm_modif ret_abr_modif modif_clause unfolding dynCall_dynCall_exn
by (rule Proc_exnProcParModifyReturn)
lemma Proc_exnProcParModifyReturnSameFaults:
assumes q: "P \<subseteq> {s. p s = q} \<inter> P'"
\<comment> \<open>@{thm[source] DynProcProcPar} introduces the same constraint as first conjunction in
@{term P'}, so the vcg can simplify it.\<close>
assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P' (dynCall_exn f g init p return' result_exn c) Q,A"
assumes ret_nrm_modif: "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
assumes ret_abr_modif: "\<forall>s t. t \<in> (ModifAbr (init s))
\<longrightarrow> result_exn (return' s t) t = result_exn (return s t) t"
assumes modif_clause:
"\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} Call q (Modif \<sigma>),(ModifAbr \<sigma>)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall_exn f g init p return result_exn c) Q,A"
proof -
from to_prove have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall init p return' c) Q,A"
from to_prove
have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall_exn f g init p return' result_exn c) Q,A"
by (rule conseqPre) blast
from this ret_nrm_modif
ret_abr_modif
have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall init p return c) Q,A"
by (rule dynProcModifyReturn) (insert modif_clause,auto)
have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall_exn f g init p return result_exn c) Q,A"
by (rule dynProc_exnModifyReturnSameFaults) (insert modif_clause,auto)
from this q show ?thesis
by (rule conseqPre)
qed
lemma ProcProcParModifyReturnSameFaults:
assumes q: "P \<subseteq> {s. p s = q} \<inter> P'"
\<comment> \<open>@{thm[source] DynProcProcPar} introduces the same constraint as first conjunction in
@ -1006,15 +1187,26 @@ lemma ProcProcParModifyReturnSameFaults:
\<longrightarrow> return' s t = return s t"
assumes modif_clause:
"\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} Call q (Modif \<sigma>),(ModifAbr \<sigma>)"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
using q to_prove ret_nrm_modif ret_abr_modif modif_clause unfolding dynCall_dynCall_exn
by (rule Proc_exnProcParModifyReturnSameFaults)
lemma Proc_exnProcParModifyReturnNoAbr:
assumes q: "P \<subseteq> {s. p s = q} \<inter> P'"
\<comment> \<open>@{thm[source] DynProcProcParNoAbrupt} introduces the same constraint as
first conjunction in @{term P'}, so the vcg can simplify it.\<close>
assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P' (dynCall_exn f g init p return' result_exn c) Q,A"
assumes ret_nrm_modif: "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
assumes modif_clause:
"\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} (Call q) (Modif \<sigma>),{}"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall_exn f g init p return result_exn c) Q,A"
proof -
from to_prove
have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall init p return' c) Q,A"
from to_prove have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall_exn f g init p return' result_exn c) Q,A"
by (rule conseqPre) blast
from this ret_nrm_modif
ret_abr_modif
have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall init p return c) Q,A"
by (rule dynProcModifyReturnSameFaults) (insert modif_clause,auto)
have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall_exn f g init p return result_exn c) Q,A"
by (rule DynProc_exnModifyReturnNoAbr) (insert modif_clause,auto)
from this q show ?thesis
by (rule conseqPre)
qed
@ -1028,18 +1220,32 @@ lemma ProcProcParModifyReturnNoAbr:
\<longrightarrow> return' s t = return s t"
assumes modif_clause:
"\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} (Call q) (Modif \<sigma>),{}"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
using q to_prove ret_nrm_modif modif_clause unfolding dynCall_dynCall_exn
by (rule Proc_exnProcParModifyReturnNoAbr)
lemma Proc_exnProcParModifyReturnNoAbrSameFaults:
assumes q: "P \<subseteq> {s. p s = q} \<inter> P'"
\<comment> \<open>@{thm[source] DynProcProcParNoAbrupt} introduces the same constraint as
first conjunction in @{term P'}, so the vcg can simplify it.\<close>
assumes to_prove: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P' (dynCall_exn f g init p return' result_exn c) Q,A"
assumes ret_nrm_modif: "\<forall>s t. t \<in> (Modif (init s))
\<longrightarrow> return' s t = return s t"
assumes modif_clause:
"\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} (Call q) (Modif \<sigma>),{}"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall_exn f g init p return result_exn c) Q,A"
proof -
from to_prove have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall init p return' c) Q,A"
from to_prove have
"\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall_exn f g init p return' result_exn c) Q,A"
by (rule conseqPre) blast
from this ret_nrm_modif
have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall init p return c) Q,A"
by (rule DynProcModifyReturnNoAbr) (insert modif_clause,auto)
have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall_exn f g init p return result_exn c) Q,A"
by (rule ProcDyn_exnModifyReturnNoAbrSameFaults) (insert modif_clause,auto)
from this q show ?thesis
by (rule conseqPre)
qed
lemma ProcProcParModifyReturnNoAbrSameFaults:
assumes q: "P \<subseteq> {s. p s = q} \<inter> P'"
\<comment> \<open>@{thm[source] DynProcProcParNoAbrupt} introduces the same constraint as
@ -1049,17 +1255,10 @@ lemma ProcProcParModifyReturnNoAbrSameFaults:
\<longrightarrow> return' s t = return s t"
assumes modif_clause:
"\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>\<^bsub>/F\<^esub> {\<sigma>} (Call q) (Modif \<sigma>),{}"
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
proof -
from to_prove have
"\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall init p return' c) Q,A"
by (rule conseqPre) blast
from this ret_nrm_modif
have "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({s. p s = q} \<inter> P') (dynCall init p return c) Q,A"
by (rule ProcDynModifyReturnNoAbrSameFaults) (insert modif_clause,auto)
from this q show ?thesis
by (rule conseqPre)
qed
shows "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P (dynCall init p return c) Q,A"
using q to_prove ret_nrm_modif modif_clause unfolding dynCall_dynCall_exn
by (rule Proc_exnProcParModifyReturnNoAbrSameFaults)
lemma MergeGuards_iff: "\<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P merge_guards c Q,A = \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> P c Q,A"
by (auto intro: MergeGuardsI MergeGuardsD)

23
tools/c-parser/Simpl/HoareTotalDef.thy
View File

@ -1,29 +1,8 @@
(*
Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: HoareTotalDef.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2004-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
Copyright (C) 2006-2008 Norbert Schirmer
*)
section \<open>Hoare Logic for Total Correctness\<close>

856
tools/c-parser/Simpl/HoareTotalProps.thy
View File

File diff suppressed because it is too large Load Diff

174
tools/c-parser/Simpl/Language.thy
View File

@ -1,29 +1,9 @@
(*
Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: Language.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2004-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
Copyright (c) 2022 Apple Inc. All rights reserved.
*)
section \<open>The Simpl Syntax\<close>
@ -76,13 +56,43 @@ definition
"bseq = Seq"
definition
block:: "['s\<Rightarrow>'s,('s,'p,'f) com,'s\<Rightarrow>'s\<Rightarrow>'s,'s\<Rightarrow>'s\<Rightarrow>('s,'p,'f) com]\<Rightarrow>('s,'p,'f) com"
block_exn:: "['s\<Rightarrow>'s,('s,'p,'f) com,'s\<Rightarrow>'s\<Rightarrow>'s,'s\<Rightarrow>'s\<Rightarrow>'s,'s\<Rightarrow>'s\<Rightarrow>('s,'p,'f) com]\<Rightarrow>('s,'p,'f) com"
where
"block init bdy return c =
DynCom (\<lambda>s. (Seq (Catch (Seq (Basic init) bdy) (Seq (Basic (return s)) Throw))
"block_exn init bdy return result_exn c =
DynCom (\<lambda>s. (Seq (Catch (Seq (Basic init) bdy) (Seq (Basic (\<lambda>t. result_exn (return s t) t)) Throw))
(DynCom (\<lambda>t. Seq (Basic (return s)) (c s t))))
)"
definition
call_exn:: "('s\<Rightarrow>'s) \<Rightarrow> 'p \<Rightarrow> ('s \<Rightarrow> 's \<Rightarrow> 's)\<Rightarrow> ('s \<Rightarrow> 's \<Rightarrow> 's) \<Rightarrow>('s\<Rightarrow>'s\<Rightarrow>('s,'p,'f) com)\<Rightarrow>('s,'p,'f)com" where
"call_exn init p return result_exn c = block_exn init (Call p) return result_exn c"
primrec guards:: "('f \<times> 's set ) list \<Rightarrow> ('s,'p,'f) com \<Rightarrow> ('s,'p,'f) com"
where
"guards [] c = c" |
"guards (g#gs) c = Guard (fst g) (snd g) (guards gs c)"
definition maybe_guard:: "'f \<Rightarrow> 's set \<Rightarrow> ('s,'p,'f) com \<Rightarrow> ('s,'p,'f) com"
where
"maybe_guard f g c = (if g = UNIV then c else Guard f g c)"
lemma maybe_guard_UNIV [simp]: "maybe_guard f UNIV c = c"
by (simp add: maybe_guard_def)
definition
dynCall_exn:: "'f \<Rightarrow> 's set \<Rightarrow> ('s \<Rightarrow> 's) \<Rightarrow> ('s \<Rightarrow> 'p) \<Rightarrow>
('s \<Rightarrow> 's \<Rightarrow> 's) \<Rightarrow> ('s \<Rightarrow> 's \<Rightarrow> 's) \<Rightarrow> ('s \<Rightarrow> 's \<Rightarrow> ('s,'p,'f) com) \<Rightarrow> ('s,'p,'f) com" where
"dynCall_exn f g init p return result_exn c =
maybe_guard f g (DynCom (\<lambda>s. call_exn init (p s) return result_exn c))"
definition
block:: "['s\<Rightarrow>'s,('s,'p,'f) com,'s\<Rightarrow>'s\<Rightarrow>'s,'s\<Rightarrow>'s\<Rightarrow>('s,'p,'f) com]\<Rightarrow>('s,'p,'f) com"
where
"block init bdy return c = block_exn init bdy return (\<lambda>s t. s) c"
definition
call:: "('s\<Rightarrow>'s) \<Rightarrow> 'p \<Rightarrow> ('s \<Rightarrow> 's \<Rightarrow> 's)\<Rightarrow>('s\<Rightarrow>'s\<Rightarrow>('s,'p,'f) com)\<Rightarrow>('s,'p,'f)com" where
"call init p return c = block init (Call p) return c"
@ -92,11 +102,14 @@ definition
('s \<Rightarrow> 's \<Rightarrow> 's) \<Rightarrow> ('s \<Rightarrow> 's \<Rightarrow> ('s,'p,'f) com) \<Rightarrow> ('s,'p,'f) com" where
"dynCall init p return c = DynCom (\<lambda>s. call init (p s) return c)"
definition
fcall:: "('s\<Rightarrow>'s) \<Rightarrow> 'p \<Rightarrow> ('s \<Rightarrow> 's \<Rightarrow> 's)\<Rightarrow>('s \<Rightarrow> 'v) \<Rightarrow> ('v\<Rightarrow>('s,'p,'f) com)
\<Rightarrow>('s,'p,'f)com" where
"fcall init p return result c = call init p return (\<lambda>s t. c (result t))"
definition
lem:: "'x \<Rightarrow> ('s,'p,'f)com \<Rightarrow>('s,'p,'f)com" where
"lem x c = c"
@ -112,10 +125,6 @@ definition guaranteeStrip:: "'f \<Rightarrow> 's set \<Rightarrow> ('s,'p,'f) co
definition guaranteeStripPair:: "'f \<Rightarrow> 's set \<Rightarrow> ('f \<times> 's set)"
where "guaranteeStripPair f g = (f,g)"
primrec guards:: "('f \<times> 's set ) list \<Rightarrow> ('s,'p,'f) com \<Rightarrow> ('s,'p,'f) com"
where
"guards [] c = c" |
"guards (g#gs) c = Guard (fst g) (snd g) (guards gs c)"
definition
while:: "('f \<times> 's set) list \<Rightarrow> 's bexp \<Rightarrow> ('s,'p,'f) com \<Rightarrow> ('s, 'p, 'f) com"
@ -160,6 +169,13 @@ lemma snd_guaranteeStripPair: "snd (guaranteeStripPair f g) = g"
by (simp add: guaranteeStripPair_def)
lemma call_call_exn: "call init p return result = call_exn init p return (\<lambda>s t. s) result"
by (simp add: call_def call_exn_def block_def)
lemma dynCall_dynCall_exn: "dynCall init p return result = dynCall_exn undefined UNIV init p return (\<lambda>s t. s) result"
by (simp add: dynCall_def dynCall_exn_def call_call_exn)
subsection \<open>Operations on Simpl-Syntax\<close>
@ -313,6 +329,10 @@ lemma flatten_bind [simp]: "flatten (bind e c) = [bind e c]"
lemma flatten_bseq [simp]: "flatten (bseq c1 c2) = flatten c1 @ flatten c2"
by (simp add: bseq_def)
lemma flatten_block_exn [simp]:
"flatten (block_exn init bdy return result_exn result) = [block_exn init bdy return result_exn result]"
by (simp add: block_exn_def)
lemma flatten_block [simp]:
"flatten (block init bdy return result) = [block init bdy return result]"
by (simp add: block_def)
@ -323,6 +343,12 @@ lemma flatten_call [simp]: "flatten (call init p return result) = [call init p r
lemma flatten_dynCall [simp]: "flatten (dynCall init p return result) = [dynCall init p return result]"
by (simp add: dynCall_def)
lemma flatten_call_exn [simp]: "flatten (call_exn init p return result_exn result) = [call_exn init p return result_exn result]"
by (simp add: call_exn_def)
lemma flatten_dynCall_exn [simp]: "flatten (dynCall_exn f g init p return result_exn result) = [dynCall_exn f g init p return result_exn result]"
by (simp add: dynCall_exn_def maybe_guard_def)
lemma flatten_fcall [simp]: "flatten (fcall init p return result c) = [fcall init p return result c]"
by (simp add: fcall_def)
@ -373,9 +399,9 @@ lemma normalize_bseq [simp]:
((flatten (normalize c1)) @ (flatten (normalize c2)))"
by (simp add: bseq_def)
lemma normalize_block [simp]: "normalize (block init bdy return c) =
block init (normalize bdy) return (\<lambda>s t. normalize (c s t))"
apply (simp add: block_def)
lemma normalize_block_exn [simp]: "normalize (block_exn init bdy return result_exn c) =
block_exn init (normalize bdy) return result_exn (\<lambda>s t. normalize (c s t))"
apply (simp add: block_exn_def)
apply (rule ext)
apply (simp)
apply (cases "flatten (normalize bdy)")
@ -397,15 +423,32 @@ lemma normalize_block [simp]: "normalize (block init bdy return c) =
apply simp
done
lemma normalize_block [simp]: "normalize (block init bdy return c) =
block init (normalize bdy) return (\<lambda>s t. normalize (c s t))"
by (simp add: block_def)
lemma normalize_call [simp]:
"normalize (call init p return c) = call init p return (\<lambda>i t. normalize (c i t))"
by (simp add: call_def)
lemma normalize_call_exn [simp]:
"normalize (call_exn init p return result_exn c) = call_exn init p return result_exn (\<lambda>i t. normalize (c i t))"
by (simp add: call_exn_def)
lemma normalize_dynCall [simp]:
"normalize (dynCall init p return c) =
dynCall init p return (\<lambda>s t. normalize (c s t))"
by (simp add: dynCall_def)
lemma normalize_guards [simp]:
"normalize (guards gs c) = guards gs (normalize c)"
by (induct gs) auto
lemma normalize_dynCall_exn [simp]:
"normalize (dynCall_exn f g init p return result_exn c) =
dynCall_exn f g init p return result_exn (\<lambda>s t. normalize (c s t))"
by (simp add: dynCall_exn_def maybe_guard_def)
lemma normalize_fcall [simp]:
"normalize (fcall init p return result c) =
fcall init p return result (\<lambda>v. normalize (c v))"
@ -421,9 +464,6 @@ lemma normalize_guaranteeStrip [simp]:
"normalize (guaranteeStrip f g c) = guaranteeStrip f g (normalize c)"
by (simp add: guaranteeStrip_def)
lemma normalize_guards [simp]:
"normalize (guards gs c) = guards gs (normalize c)"
by (induct gs) auto
text \<open>Sequencial composition with guards in the body is not preserved by
normalize\<close>
@ -506,6 +546,11 @@ lemma strip_guards_bseq [simp]:
"strip_guards F (bseq c1 c2) = bseq (strip_guards F c1) (strip_guards F c2)"
by (simp add: bseq_def)
lemma strip_guards_block_exn [simp]:
"strip_guards F (block_exn init bdy return result_exn c) =
block_exn init (strip_guards F bdy) return result_exn (\<lambda>s t. strip_guards F (c s t))"
by (simp add: block_exn_def)
lemma strip_guards_block [simp]:
"strip_guards F (block init bdy return c) =
block init (strip_guards F bdy) return (\<lambda>s t. strip_guards F (c s t))"
@ -516,11 +561,25 @@ lemma strip_guards_call [simp]:
call init p return (\<lambda>s t. strip_guards F (c s t))"
by (simp add: call_def)
lemma strip_guards_call_exn [simp]:
"strip_guards F (call_exn init p return result_exn c) =
call_exn init p return result_exn (\<lambda>s t. strip_guards F (c s t))"
by (simp add: call_exn_def)
lemma strip_guards_dynCall [simp]:
"strip_guards F (dynCall init p return c) =
dynCall init p return (\<lambda>s t. strip_guards F (c s t))"
by (simp add: dynCall_def)
lemma strip_guards_guards [simp]: "strip_guards F (guards gs c) =
guards (filter (\<lambda>(f,g). f \<notin> F) gs) (strip_guards F c)"
by (induct gs) auto
lemma strip_guards_dynCall_exn [simp]:
"strip_guards F (dynCall_exn f g init p return result_exn c) =
dynCall_exn f (if f \<in> F then UNIV else g) init p return result_exn (\<lambda>s t. strip_guards F (c s t))"
by (simp add: dynCall_exn_def maybe_guard_def)
lemma strip_guards_fcall [simp]:
"strip_guards F (fcall init p return result c) =
fcall init p return result (\<lambda>v. strip_guards F (c v))"
@ -540,9 +599,7 @@ lemma strip_guards_guaranteeStrip [simp]:
lemma guaranteeStripPair_split_conv [simp]: "case_prod c (guaranteeStripPair f g) = c f g"
by (simp add: guaranteeStripPair_def)
lemma strip_guards_guards [simp]: "strip_guards F (guards gs c) =
guards (filter (\<lambda>(f,g). f \<notin> F) gs) (strip_guards F c)"
by (induct gs) auto
lemma strip_guards_while [simp]:
"strip_guards F (while gs b c) =
@ -602,6 +659,11 @@ lemma mark_guards_bseq [simp]:
"mark_guards f (bseq c1 c2) = bseq (mark_guards f c1) (mark_guards f c2)"
by (simp add: bseq_def)
lemma mark_guards_block_exn [simp]:
"mark_guards f (block_exn init bdy return result_exn c) =
block_exn init (mark_guards f bdy) return result_exn (\<lambda>s t. mark_guards f (c s t))"
by (simp add: block_exn_def)
lemma mark_guards_block [simp]:
"mark_guards f (block init bdy return c) =
block init (mark_guards f bdy) return (\<lambda>s t. mark_guards f (c s t))"
@ -612,11 +674,25 @@ lemma mark_guards_call [simp]:
call init p return (\<lambda>s t. mark_guards f (c s t))"
by (simp add: call_def)
lemma mark_guards_call_exn [simp]:
"mark_guards f (call_exn init p return result_exn c) =
call_exn init p return result_exn (\<lambda>s t. mark_guards f (c s t))"
by (simp add: call_exn_def)
lemma mark_guards_dynCall [simp]:
"mark_guards f (dynCall init p return c) =
dynCall init p return (\<lambda>s t. mark_guards f (c s t))"
by (simp add: dynCall_def)
lemma mark_guards_guards [simp]:
"mark_guards f (guards gs c) = guards (map (\<lambda>(f',g). (f,g)) gs) (mark_guards f c)"
by (induct gs) auto
lemma mark_guards_dynCall_exn [simp]:
"mark_guards f (dynCall_exn f' g init p return result_exn c) =
dynCall_exn f g init p return result_exn (\<lambda>s t. mark_guards f (c s t))"
by (simp add: dynCall_exn_def maybe_guard_def)
lemma mark_guards_fcall [simp]:
"mark_guards f (fcall init p return result c) =
fcall init p return result (\<lambda>v. mark_guards f (c v))"
@ -631,9 +707,6 @@ lemma mark_guards_guaranteeStrip [simp]:
"mark_guards f (guaranteeStrip f' g c) = guaranteeStrip f g (mark_guards f c)"
by (simp add: guaranteeStrip_def)
lemma mark_guards_guards [simp]:
"mark_guards f (guards gs c) = guards (map (\<lambda>(f',g). (f,g)) gs) (mark_guards f c)"
by (induct gs) auto
lemma mark_guards_while [simp]:
"mark_guards f (while gs b c) =
@ -664,6 +737,7 @@ lemmas mark_guards_simps = mark_guards.simps mark_guards_raise
definition is_Guard:: "('s,'p,'f) com \<Rightarrow> bool"
where "is_Guard c = (case c of Guard f g c' \<Rightarrow> True | _ \<Rightarrow> False)"
lemma is_Guard_basic_simps [simp]:
"is_Guard (guards (pg# pgs) c) = True"
"is_Guard Skip = False"
"is_Guard (Basic f) = False"
"is_Guard (Spec r) = False"
@ -679,14 +753,18 @@ lemma is_Guard_basic_simps [simp]:
"is_Guard (condCatch c1 b c2) = False"
"is_Guard (bind e cv) = False"
"is_Guard (bseq c1 c2) = False"
"is_Guard (block_exn init bdy return result_exn cont) = False"
"is_Guard (block init bdy return cont) = False"
"is_Guard (call init p return cont) = False"
"is_Guard (dynCall init P return cont) = False"
"is_Guard (call_exn init p return result_exn cont) = False"
"is_Guard (dynCall_exn f UNIV init P return result_exn cont) = False"
"is_Guard (fcall init p return result cont') = False"
"is_Guard (whileAnno b I V c) = False"
"is_Guard (guaranteeStrip F g c) = True"
by (auto simp add: is_Guard_def raise_def condCatch_def bind_def bseq_def
block_def call_def dynCall_def fcall_def whileAnno_def guaranteeStrip_def)
block_def block_exn_def call_def dynCall_def call_exn_def dynCall_exn_def
fcall_def whileAnno_def guaranteeStrip_def)
lemma is_Guard_switch [simp]:
@ -776,6 +854,9 @@ lemmas merge_guards_res_simps = merge_guards_res_Skip merge_guards_res_Basic
merge_guards_res_DynCom merge_guards_res_Throw merge_guards_res_Catch
merge_guards_res_Guard
lemma merge_guards_guards_empty: "merge_guards (guards [] c) = merge_guards c"
by (simp)
lemma merge_guards_raise: "merge_guards (raise g) = raise g"
by (simp add: raise_def)
@ -792,6 +873,11 @@ lemma merge_guards_bseq [simp]:
"merge_guards (bseq c1 c2) = bseq (merge_guards c1) (merge_guards c2)"
by (simp add: bseq_def)
lemma merge_guards_block_exn [simp]:
"merge_guards (block_exn init bdy return result_exn c) =
block_exn init (merge_guards bdy) return result_exn (\<lambda>s t. merge_guards (c s t))"
by (simp add: block_exn_def)
lemma merge_guards_block [simp]:
"merge_guards (block init bdy return c) =
block init (merge_guards bdy) return (\<lambda>s t. merge_guards (c s t))"
@ -802,6 +888,11 @@ lemma merge_guards_call [simp]:
call init p return (\<lambda>s t. merge_guards (c s t))"
by (simp add: call_def)
lemma merge_guards_call_exn [simp]:
"merge_guards (call_exn init p return result_exn c) =
call_exn init p return result_exn (\<lambda>s t. merge_guards (c s t))"
by (simp add: call_exn_def)
lemma merge_guards_dynCall [simp]:
"merge_guards (dynCall init p return c) =
dynCall init p return (\<lambda>s t. merge_guards (c s t))"
@ -843,6 +934,7 @@ text \<open>@{term "merge_guards"} for guard-lists as in @{const guards}, @{cons
lemmas merge_guards_simps = merge_guards.simps merge_guards_raise
merge_guards_condCatch merge_guards_bind merge_guards_bseq merge_guards_block
merge_guards_dynCall merge_guards_fcall merge_guards_switch
merge_guards_block_exn merge_guards_call_exn
merge_guards_guaranteeStrip merge_guards_whileAnno merge_guards_specAnno
primrec noguards:: "('s,'p,'f) com \<Rightarrow> bool"

759
tools/c-parser/Simpl/Semantic.thy
View File

@ -1,29 +1,9 @@
(*
Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: Semantic.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2004-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
Copyright (c) 2022 Apple Inc. All rights reserved.
*)
section \<open>Big-Step Semantics for Simpl\<close>
@ -178,33 +158,62 @@ inductive_cases exec_Normal_elim_cases [cases set]:
"\<Gamma>\<turnstile>\<langle>Throw,Normal s\<rangle> \<Rightarrow> t"
"\<Gamma>\<turnstile>\<langle>Catch c1 c2,Normal s\<rangle> \<Rightarrow> t"
lemma exec_block_exn:
"\<lbrakk>\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t; \<Gamma>\<turnstile>\<langle>c s t,Normal (return s t)\<rangle> \<Rightarrow> u\<rbrakk>
\<Longrightarrow>
\<Gamma>\<turnstile>\<langle>block_exn init bdy return result_exn c,Normal s\<rangle> \<Rightarrow> u"
apply (unfold block_exn_def)
by (fastforce intro: exec.intros)
lemma exec_block:
"\<lbrakk>\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t; \<Gamma>\<turnstile>\<langle>c s t,Normal (return s t)\<rangle> \<Rightarrow> u\<rbrakk>
\<Longrightarrow>
\<Gamma>\<turnstile>\<langle>block init bdy return c,Normal s\<rangle> \<Rightarrow> u"
apply (unfold block_def)
by (fastforce intro: exec.intros)
unfolding block_def
by (rule exec_block_exn)
lemma exec_block_exnAbrupt:
"\<lbrakk>\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Abrupt t\<rbrakk>
\<Longrightarrow>
\<Gamma>\<turnstile>\<langle>block_exn init bdy return result_exn c,Normal s\<rangle> \<Rightarrow> Abrupt (result_exn (return s t) t)"
apply (unfold block_exn_def)
by (fastforce intro: exec.intros)
lemma exec_blockAbrupt:
"\<lbrakk>\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Abrupt t\<rbrakk>
\<Longrightarrow>
\<Gamma>\<turnstile>\<langle>block init bdy return c,Normal s\<rangle> \<Rightarrow> Abrupt (return s t)"
apply (unfold block_def)
by (fastforce intro: exec.intros)
unfolding block_def
by (rule exec_block_exnAbrupt)
lemma exec_block_exnFault:
"\<lbrakk>\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Fault f\<rbrakk>
\<Longrightarrow>
\<Gamma>\<turnstile>\<langle>block_exn init bdy return result_exn c,Normal s\<rangle> \<Rightarrow> Fault f"
apply (unfold block_exn_def)
by (fastforce intro: exec.intros)
lemma exec_blockFault:
"\<lbrakk>\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Fault f\<rbrakk>
\<Longrightarrow>
\<Gamma>\<turnstile>\<langle>block init bdy return c,Normal s\<rangle> \<Rightarrow> Fault f"
apply (unfold block_def)
by (fastforce intro: exec.intros)
unfolding block_def
by (rule exec_block_exnFault)
lemma exec_block_exnStuck:
"\<lbrakk>\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Stuck\<rbrakk>
\<Longrightarrow>
\<Gamma>\<turnstile>\<langle>block_exn init bdy return result_exn c,Normal s\<rangle> \<Rightarrow> Stuck"
apply (unfold block_exn_def)
by (fastforce intro: exec.intros)
lemma exec_blockStuck:
"\<lbrakk>\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Stuck\<rbrakk>
\<Longrightarrow>
\<Gamma>\<turnstile>\<langle>block init bdy return c,Normal s\<rangle> \<Rightarrow> Stuck"
apply (unfold block_def)
by (fastforce intro: exec.intros)
unfolding block_def
by (rule exec_block_exnStuck)
lemma exec_call:
"\<lbrakk>\<Gamma> p=Some bdy;\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t; \<Gamma>\<turnstile>\<langle>c s t,Normal (return s t)\<rangle> \<Rightarrow> u\<rbrakk>
@ -216,7 +225,6 @@ apply (erule (1) Call)
apply assumption
done
lemma exec_callAbrupt:
"\<lbrakk>\<Gamma> p=Some bdy;\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Abrupt t\<rbrakk>
\<Longrightarrow>
@ -253,6 +261,52 @@ apply (rule exec_blockStuck)
apply (erule CallUndefined)
done
lemma exec_call_exn:
"\<lbrakk>\<Gamma> p=Some bdy;\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t; \<Gamma>\<turnstile>\<langle>c s t,Normal (return s t)\<rangle> \<Rightarrow> u\<rbrakk>
\<Longrightarrow>
\<Gamma>\<turnstile>\<langle>call_exn init p return result_exn c,Normal s\<rangle> \<Rightarrow> u"
apply (simp add: call_exn_def)
apply (rule exec_block_exn)
apply (erule (1) Call)
apply assumption
done
lemma exec_call_exnAbrupt:
"\<lbrakk>\<Gamma> p=Some bdy;\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Abrupt t\<rbrakk>
\<Longrightarrow>
\<Gamma>\<turnstile>\<langle>call_exn init p return result_exn c,Normal s\<rangle> \<Rightarrow> Abrupt (result_exn (return s t) t)"
apply (simp add: call_exn_def)
apply (rule exec_block_exnAbrupt)
apply (erule (1) Call)
done
lemma exec_call_exnFault:
"\<lbrakk>\<Gamma> p=Some bdy; \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Fault f\<rbrakk>
\<Longrightarrow>
\<Gamma>\<turnstile>\<langle>call_exn init p return result_exn c,Normal s\<rangle> \<Rightarrow> Fault f"
apply (simp add: call_exn_def)
apply (rule exec_block_exnFault)
apply (erule (1) Call)
done
lemma exec_call_exnStuck:
"\<lbrakk>\<Gamma> p=Some bdy; \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Stuck\<rbrakk>
\<Longrightarrow>
\<Gamma>\<turnstile>\<langle>call_exn init p return result_exn c,Normal s\<rangle> \<Rightarrow> Stuck"
apply (simp add: call_exn_def)
apply (rule exec_block_exnStuck)
apply (erule (1) Call)
done
lemma exec_call_exnUndefined:
"\<lbrakk>\<Gamma> p=None\<rbrakk>
\<Longrightarrow>
\<Gamma>\<turnstile>\<langle>call_exn init p return result_exn c,Normal s\<rangle> \<Rightarrow> Stuck"
apply (simp add: call_exn_def)
apply (rule exec_block_exnStuck)
apply (erule CallUndefined)
done
lemma Fault_end: assumes exec: "\<Gamma>\<turnstile>\<langle>c,s\<rangle> \<Rightarrow> t" and s: "s=Fault f"
shows "t=Fault f"
@ -283,9 +337,8 @@ lemma exec_Call_body':
by (rule exec_Call_body_aux)
lemma exec_block_Normal_elim [consumes 1]:
assumes exec_block: "\<Gamma>\<turnstile>\<langle>block init bdy return c,Normal s\<rangle> \<Rightarrow> t"
lemma exec_block_exn_Normal_elim [consumes 1]:
assumes exec_block: "\<Gamma>\<turnstile>\<langle>block_exn init bdy return result_exn c,Normal s\<rangle> \<Rightarrow> t"
assumes Normal:
"\<And>t'.
\<lbrakk>\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t';
@ -294,7 +347,7 @@ assumes Normal:
assumes Abrupt:
"\<And>t'.
\<lbrakk>\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Abrupt t';
t = Abrupt (return s t')\<rbrakk>
t = Abrupt (result_exn (return s t') t')\<rbrakk>
\<Longrightarrow> P"
assumes Fault:
"\<And>f.
@ -309,7 +362,7 @@ assumes
"\<lbrakk>\<Gamma> p = None; t = Stuck\<rbrakk> \<Longrightarrow> P"
shows "P"
using exec_block
apply (unfold block_def)
apply (unfold block_exn_def)
apply (elim exec_Normal_elim_cases)
apply simp_all
apply (case_tac s')
@ -337,6 +390,96 @@ apply (drule Stuck_end) apply simp
apply (rule Stuck,assumption+)
done
lemma exec_block_Normal_elim [consumes 1]:
assumes exec_block: "\<Gamma>\<turnstile>\<langle>block init bdy return c,Normal s\<rangle> \<Rightarrow> t"
assumes Normal:
"\<And>t'.
\<lbrakk>\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t';
\<Gamma>\<turnstile>\<langle>c s t',Normal (return s t')\<rangle> \<Rightarrow> t\<rbrakk>
\<Longrightarrow> P"
assumes Abrupt:
"\<And>t'.
\<lbrakk>\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Abrupt t';
t = Abrupt (return s t')\<rbrakk>
\<Longrightarrow> P"
assumes Fault:
"\<And>f.
\<lbrakk>\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Fault f;
t = Fault f\<rbrakk>
\<Longrightarrow> P"
assumes Stuck:
"\<lbrakk>\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Stuck;
t = Stuck\<rbrakk>
\<Longrightarrow> P"
assumes
Undef: "\<lbrakk>\<Gamma> p = None; t = Stuck\<rbrakk> \<Longrightarrow> P"
shows "P"
by (rule exec_block_exn_Normal_elim [OF exec_block [simplified block_def]
Normal Abrupt Fault Stuck Undef ])
lemma exec_call_exn_Normal_elim [consumes 1]:
assumes exec_call: "\<Gamma>\<turnstile>\<langle>call_exn init p return result_exn c,Normal s\<rangle> \<Rightarrow> t"
assumes Normal:
"\<And>bdy t'.
\<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t';
\<Gamma>\<turnstile>\<langle>c s t',Normal (return s t')\<rangle> \<Rightarrow> t\<rbrakk>
\<Longrightarrow> P"
assumes Abrupt:
"\<And>bdy t'.
\<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Abrupt t';
t = Abrupt (result_exn (return s t') t')\<rbrakk>
\<Longrightarrow> P"
assumes Fault:
"\<And>bdy f.
\<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Fault f;
t = Fault f\<rbrakk>
\<Longrightarrow> P"
assumes Stuck:
"\<And>bdy.
\<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Stuck;
t = Stuck\<rbrakk>
\<Longrightarrow> P"
assumes Undef:
"\<lbrakk>\<Gamma> p = None; t = Stuck\<rbrakk> \<Longrightarrow> P"
shows "P"
using exec_call
apply (unfold call_exn_def)
apply (cases "\<Gamma> p")
apply (erule exec_block_exn_Normal_elim)
apply (elim exec_Normal_elim_cases)
apply simp
apply simp
apply (elim exec_Normal_elim_cases)
apply simp
apply simp
apply (elim exec_Normal_elim_cases)
apply simp
apply simp
apply (elim exec_Normal_elim_cases)
apply simp
apply (rule Undef,assumption,assumption)
apply (rule Undef,assumption+)
apply (erule exec_block_exn_Normal_elim)
apply (elim exec_Normal_elim_cases)
apply simp
apply (rule Normal,assumption+)
apply simp
apply (elim exec_Normal_elim_cases)
apply simp
apply (rule Abrupt,assumption+)
apply simp
apply (elim exec_Normal_elim_cases)
apply simp
apply (rule Fault, assumption+)
apply simp
apply (elim exec_Normal_elim_cases)
apply simp
apply (rule Stuck,assumption,assumption,assumption)
apply simp
apply (rule Undef,assumption+)
done
lemma exec_call_Normal_elim [consumes 1]:
assumes exec_call: "\<Gamma>\<turnstile>\<langle>call init p return c,Normal s\<rangle> \<Rightarrow> t"
assumes Normal:
@ -362,42 +505,8 @@ assumes Stuck:
assumes Undef:
"\<lbrakk>\<Gamma> p = None; t = Stuck\<rbrakk> \<Longrightarrow> P"
shows "P"
using exec_call
apply (unfold call_def)
apply (cases "\<Gamma> p")
apply (erule exec_block_Normal_elim)
apply (elim exec_Normal_elim_cases)
apply simp
apply simp
apply (elim exec_Normal_elim_cases)
apply simp
apply simp
apply (elim exec_Normal_elim_cases)
apply simp
apply simp
apply (elim exec_Normal_elim_cases)
apply simp
apply (rule Undef,assumption,assumption)
apply (rule Undef,assumption+)
apply (erule exec_block_Normal_elim)
apply (elim exec_Normal_elim_cases)
apply simp
apply (rule Normal,assumption+)
apply simp
apply (elim exec_Normal_elim_cases)
apply simp
apply (rule Abrupt,assumption+)
apply simp
apply (elim exec_Normal_elim_cases)
apply simp
apply (rule Fault, assumption+)
apply simp
apply (elim exec_Normal_elim_cases)
apply simp
apply (rule Stuck,assumption,assumption,assumption)
apply simp
apply (rule Undef,assumption+)
done
using exec_call [simplified call_call_exn] Normal Abrupt Fault Stuck Undef
by (rule exec_call_exn_Normal_elim)
lemma exec_dynCall:
@ -407,6 +516,13 @@ lemma exec_dynCall:
apply (simp add: dynCall_def)
by (rule DynCom)
lemma exec_dynCall_exn:
"\<lbrakk>\<Gamma>\<turnstile>\<langle>call_exn init (p s) return result_exn c,Normal s\<rangle> \<Rightarrow> t\<rbrakk>
\<Longrightarrow>
\<Gamma>\<turnstile>\<langle>dynCall_exn f UNIV init p return result_exn c,Normal s\<rangle> \<Rightarrow> t"
apply (simp add: dynCall_exn_def)
by (rule DynCom)
lemma exec_dynCall_Normal_elim:
assumes exec: "\<Gamma>\<turnstile>\<langle>dynCall init p return c,Normal s\<rangle> \<Rightarrow> t"
assumes call: "\<Gamma>\<turnstile>\<langle>call init (p s) return c,Normal s\<rangle> \<Rightarrow> t \<Longrightarrow> P"
@ -417,6 +533,137 @@ lemma exec_dynCall_Normal_elim:
apply (rule call,assumption)
done
lemma exec_guards_Normal_elim_cases [consumes 1, case_names noFault someFault]:
assumes exec_guards: "\<Gamma>\<turnstile>\<langle>guards gs c,Normal s\<rangle> \<Rightarrow> t"
assumes noFault: "\<forall>f g. (f, g) \<in> set gs \<longrightarrow> s \<in> g \<Longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t \<Longrightarrow> P"
assumes someFault: "\<And>f g. find (\<lambda>(f,g). s \<notin> g) gs = Some (f, g) \<Longrightarrow> t = Fault f \<Longrightarrow> P"
shows "P"
using exec_guards noFault someFault
proof (induct gs)
case Nil
then show ?case by simp
next
case (Cons pg gs)
obtain f g where pg: "pg = (f, g)"
by (cases pg) auto
show ?thesis
proof (cases "s \<in> g")
case True
from Cons.prems(1) have exec_gs: "\<Gamma>\<turnstile> \<langle>guards gs c,Normal s\<rangle> \<Rightarrow> t"
by (simp add: pg) (meson True pg exec_Normal_elim_cases)
from Cons.hyps [OF exec_gs] Cons.prems(2,3)
show ?thesis
by (simp add: pg True)
next
case False
from Cons.prems(1) have t: "t = Fault f"
by (simp add: pg) (meson False pg exec_Normal_elim_cases)
from t Cons.prems(3)
show ?thesis
by (simp add: pg False)
qed
qed
lemma exec_guards_noFault:
assumes exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t"
assumes noFault: "\<forall>f g. (f, g) \<in> set gs \<longrightarrow> s \<in> g"
shows "\<Gamma>\<turnstile>\<langle>guards gs c,Normal s\<rangle> \<Rightarrow> t"
using exec noFault by (induct gs) (auto intro: exec.intros)
lemma exec_guards_Fault:
assumes Fault: "find (\<lambda>(f,g). s \<notin> g) gs = Some (f, g)"
shows "\<Gamma>\<turnstile>\<langle>guards gs c,Normal s\<rangle> \<Rightarrow> Fault f"
using Fault by (induct gs) (auto intro: exec.intros split: prod.splits if_split_asm)
lemma exec_guards_DynCom:
assumes exec_c: "\<Gamma>\<turnstile>\<langle>guards gs (c s), Normal s\<rangle> \<Rightarrow> t"
shows "\<Gamma>\<turnstile>\<langle>guards gs (DynCom c), Normal s\<rangle> \<Rightarrow> t"
using exec_c apply (induct gs)
apply (fastforce intro: exec.intros)
apply simp
by (metis exec.Guard exec.GuardFault exec_Normal_elim_cases)
lemma exec_guards_DynCom_Normal_elim:
assumes exec: "\<Gamma>\<turnstile>\<langle>guards gs (DynCom c), Normal s\<rangle> \<Rightarrow> t"
assumes call: "\<Gamma>\<turnstile>\<langle>guards gs (c s), Normal s\<rangle> \<Rightarrow> t \<Longrightarrow> P"
shows "P"
using exec call proof (induct gs)
case Nil
then show ?case
apply simp
apply (erule exec_Normal_elim_cases)
apply simp
done
next
case (Cons g gs)
then show ?case
apply (cases g)
apply simp
apply (erule exec_Normal_elim_cases)
apply simp
apply (meson Guard)
apply simp
apply (meson GuardFault)
done
qed
lemma exec_maybe_guard_DynCom:
assumes exec_c: "\<Gamma>\<turnstile>\<langle>maybe_guard f g (c s), Normal s\<rangle> \<Rightarrow> t"
shows "\<Gamma>\<turnstile>\<langle>maybe_guard f g (DynCom c), Normal s\<rangle> \<Rightarrow> t"
using exec_c
by (metis DynCom Guard GuardFault exec_Normal_elim_cases(5) maybe_guard_def)
lemma exec_maybe_guard_Normal_elim_cases [consumes 1, case_names noFault someFault]:
assumes exec_guards: "\<Gamma>\<turnstile>\<langle>maybe_guard f g c,Normal s\<rangle> \<Rightarrow> t"
assumes noFault: "s \<in> g \<Longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t \<Longrightarrow> P"
assumes someFault: "s \<notin> g \<Longrightarrow> t = Fault f \<Longrightarrow> P"
shows "P"
using exec_guards noFault someFault
by (metis UNIV_I exec_Normal_elim_cases(5) maybe_guard_def)
lemma exec_maybe_guard_noFault:
assumes exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> \<Rightarrow> t"
assumes noFault: "s \<in> g"
shows "\<Gamma>\<turnstile>\<langle>maybe_guard f g c,Normal s\<rangle> \<Rightarrow> t"
using exec noFault
by (simp add: Guard maybe_guard_def)
lemma exec_maybe_guard_Fault:
assumes Fault: "s \<notin> g"
shows "\<Gamma>\<turnstile>\<langle>maybe_guard f g c,Normal s\<rangle> \<Rightarrow> Fault f"
using Fault
by (metis GuardFault iso_tuple_UNIV_I maybe_guard_def)
lemma exec_maybe_guard_DynCom_Normal_elim:
assumes exec: "\<Gamma>\<turnstile>\<langle>maybe_guard f g (DynCom c), Normal s\<rangle> \<Rightarrow> t"
assumes call: "\<Gamma>\<turnstile>\<langle>maybe_guard f g (c s), Normal s\<rangle> \<Rightarrow> t \<Longrightarrow> P"
shows "P"
using exec call
apply (cases "g=UNIV")
subgoal
apply simp
apply (erule exec_Normal_elim_cases)
apply simp
done
subgoal
apply (simp add: maybe_guard_def)
apply (erule exec_Normal_elim_cases)
apply (meson Guard exec_Normal_elim_cases(12))
by (meson GuardFault)
done
lemma exec_dynCall_exn_Normal_elim:
assumes exec: "\<Gamma>\<turnstile>\<langle>dynCall_exn f g init p return result_exn c,Normal s\<rangle> \<Rightarrow> t"
assumes call: "\<Gamma>\<turnstile>\<langle>maybe_guard f g (call_exn init (p s) return result_exn c),Normal s\<rangle> \<Rightarrow> t \<Longrightarrow> P"
shows "P"
using exec
apply (simp add: dynCall_exn_def)
apply (erule exec_maybe_guard_DynCom_Normal_elim)
by (rule call)
lemma exec_Call_body:
"\<Gamma> p=Some bdy \<Longrightarrow>
@ -564,33 +811,61 @@ lemma execn_Abrupt_end: assumes exec: "\<Gamma>\<turnstile>\<langle>c,s\<rangle>
shows "t=Abrupt s'"
using exec s by (induct) auto
lemma execn_block_exn:
"\<lbrakk>\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =n\<Rightarrow> Normal t; \<Gamma>\<turnstile>\<langle>c s t,Normal (return s t)\<rangle> =n\<Rightarrow> u\<rbrakk>
\<Longrightarrow>
\<Gamma>\<turnstile>\<langle>block_exn init bdy return result_exn c,Normal s\<rangle> =n\<Rightarrow> u"
apply (unfold block_exn_def)
by (fastforce intro: execn.intros)
lemma execn_block:
"\<lbrakk>\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =n\<Rightarrow> Normal t; \<Gamma>\<turnstile>\<langle>c s t,Normal (return s t)\<rangle> =n\<Rightarrow> u\<rbrakk>
\<Longrightarrow>
\<Gamma>\<turnstile>\<langle>block init bdy return c,Normal s\<rangle> =n\<Rightarrow> u"
apply (unfold block_def)
by (fastforce intro: execn.intros)
unfolding block_def
by (rule execn_block_exn)
lemma execn_block_exnAbrupt:
"\<lbrakk>\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =n\<Rightarrow> Abrupt t\<rbrakk>
\<Longrightarrow>
\<Gamma>\<turnstile>\<langle>block_exn init bdy return result_exn c,Normal s\<rangle> =n\<Rightarrow> Abrupt (result_exn (return s t) t)"
apply (unfold block_exn_def)
by (fastforce intro: execn.intros)
lemma execn_blockAbrupt:
"\<lbrakk>\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =n\<Rightarrow> Abrupt t\<rbrakk>
\<Longrightarrow>
\<Gamma>\<turnstile>\<langle>block init bdy return c,Normal s\<rangle> =n\<Rightarrow> Abrupt (return s t)"
apply (unfold block_def)
by (fastforce intro: execn.intros)
unfolding block_def
by (rule execn_block_exnAbrupt)
lemma execn_block_exnFault:
"\<lbrakk>\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =n\<Rightarrow> Fault f\<rbrakk>
\<Longrightarrow>
\<Gamma>\<turnstile>\<langle>block_exn init bdy return result_exn c,Normal s\<rangle> =n\<Rightarrow> Fault f"
apply (unfold block_exn_def)
by (fastforce intro: execn.intros)
lemma execn_blockFault:
"\<lbrakk>\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =n\<Rightarrow> Fault f\<rbrakk>
\<Longrightarrow>
\<Gamma>\<turnstile>\<langle>block init bdy return c,Normal s\<rangle> =n\<Rightarrow> Fault f"
apply (unfold block_def)
by (fastforce intro: execn.intros)
unfolding block_def
by (rule execn_block_exnFault)
lemma execn_block_exnStuck:
"\<lbrakk>\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =n\<Rightarrow> Stuck\<rbrakk>
\<Longrightarrow>
\<Gamma>\<turnstile>\<langle>block_exn init bdy return result_exn c,Normal s\<rangle> =n\<Rightarrow> Stuck"
apply (unfold block_exn_def)
by (fastforce intro: execn.intros)
lemma execn_blockStuck:
"\<lbrakk>\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =n\<Rightarrow> Stuck\<rbrakk>
\<Longrightarrow>
\<Gamma>\<turnstile>\<langle>block init bdy return c,Normal s\<rangle> =n\<Rightarrow> Stuck"
apply (unfold block_def)
by (fastforce intro: execn.intros)
unfolding block_def
by (rule execn_block_exnStuck)
lemma execn_call:
@ -604,6 +879,17 @@ apply (erule (1) Call)
apply assumption
done
lemma execn_call_exn:
"\<lbrakk>\<Gamma> p=Some bdy;\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =n\<Rightarrow> Normal t;
\<Gamma>\<turnstile>\<langle>c s t,Normal (return s t)\<rangle> =Suc n\<Rightarrow> u\<rbrakk>
\<Longrightarrow>
\<Gamma>\<turnstile>\<langle>call_exn init p return result_exn c,Normal s\<rangle> =Suc n\<Rightarrow> u"
apply (simp add: call_exn_def)
apply (rule execn_block_exn)
apply (erule (1) Call)
apply assumption
done
lemma execn_callAbrupt:
"\<lbrakk>\<Gamma> p=Some bdy;\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =n\<Rightarrow> Abrupt t\<rbrakk>
@ -614,6 +900,15 @@ apply (rule execn_blockAbrupt)
apply (erule (1) Call)
done
lemma execn_call_exnAbrupt:
"\<lbrakk>\<Gamma> p=Some bdy;\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =n\<Rightarrow> Abrupt t\<rbrakk>
\<Longrightarrow>
\<Gamma>\<turnstile>\<langle>call_exn init p return result_exn c,Normal s\<rangle> =Suc n\<Rightarrow> Abrupt (result_exn (return s t) t)"
apply (simp add: call_exn_def)
apply (rule execn_block_exnAbrupt)
apply (erule (1) Call)
done
lemma execn_callFault:
"\<lbrakk>\<Gamma> p=Some bdy; \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =n\<Rightarrow> Fault f\<rbrakk>
\<Longrightarrow>
@ -623,6 +918,15 @@ apply (rule execn_blockFault)
apply (erule (1) Call)
done
lemma execn_call_exnFault:
"\<lbrakk>\<Gamma> p=Some bdy; \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =n\<Rightarrow> Fault f\<rbrakk>
\<Longrightarrow>
\<Gamma>\<turnstile>\<langle>call_exn init p return result_exn c,Normal s\<rangle> =Suc n\<Rightarrow> Fault f"
apply (simp add: call_exn_def)
apply (rule execn_block_exnFault)
apply (erule (1) Call)
done
lemma execn_callStuck:
"\<lbrakk>\<Gamma> p=Some bdy; \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =n\<Rightarrow> Stuck\<rbrakk>
\<Longrightarrow>
@ -632,6 +936,15 @@ apply (rule execn_blockStuck)
apply (erule (1) Call)
done
lemma execn_call_exnStuck:
"\<lbrakk>\<Gamma> p=Some bdy; \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =n\<Rightarrow> Stuck\<rbrakk>
\<Longrightarrow>
\<Gamma>\<turnstile>\<langle>call_exn init p return result_exn c,Normal s\<rangle> =Suc n\<Rightarrow> Stuck"
apply (simp add: call_exn_def)
apply (rule execn_block_exnStuck)
apply (erule (1) Call)
done
lemma execn_callUndefined:
"\<lbrakk>\<Gamma> p=None\<rbrakk>
\<Longrightarrow>
@ -641,8 +954,17 @@ apply (rule execn_blockStuck)
apply (erule CallUndefined)
done
lemma execn_block_Normal_elim [consumes 1]:
assumes execn_block: "\<Gamma>\<turnstile>\<langle>block init bdy return c,Normal s\<rangle> =n\<Rightarrow> t"
lemma execn_call_exnUndefined:
"\<lbrakk>\<Gamma> p=None\<rbrakk>
\<Longrightarrow>
\<Gamma>\<turnstile>\<langle>call_exn init p return result_exn c,Normal s\<rangle> =Suc n\<Rightarrow> Stuck"
apply (simp add: call_exn_def)
apply (rule execn_block_exnStuck)
apply (erule CallUndefined)
done
lemma execn_block_exn_Normal_elim [consumes 1]:
assumes execn_block: "\<Gamma>\<turnstile>\<langle>block_exn init bdy return result_exn c,Normal s\<rangle> =n\<Rightarrow> t"
assumes Normal:
"\<And>t'.
\<lbrakk>\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =n\<Rightarrow> Normal t';
@ -651,7 +973,7 @@ assumes Normal:
assumes Abrupt:
"\<And>t'.
\<lbrakk>\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =n\<Rightarrow> Abrupt t';
t = Abrupt (return s t')\<rbrakk>
t = Abrupt (result_exn (return s t') t')\<rbrakk>
\<Longrightarrow> P"
assumes Fault:
"\<And>f.
@ -666,7 +988,7 @@ assumes Undef:
"\<lbrakk>\<Gamma> p = None; t = Stuck\<rbrakk> \<Longrightarrow> P"
shows "P"
using execn_block
apply (unfold block_def)
apply (unfold block_exn_def)
apply (elim execn_Normal_elim_cases)
apply simp_all
apply (case_tac s')
@ -694,6 +1016,99 @@ apply (drule execn_Stuck_end) apply simp
apply (rule Stuck,assumption+)
done
lemma execn_block_Normal_elim [consumes 1]:
assumes execn_block: "\<Gamma>\<turnstile>\<langle>block init bdy return c,Normal s\<rangle> =n\<Rightarrow> t"
assumes Normal:
"\<And>t'.
\<lbrakk>\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =n\<Rightarrow> Normal t';
\<Gamma>\<turnstile>\<langle>c s t',Normal (return s t')\<rangle> =n\<Rightarrow> t\<rbrakk>
\<Longrightarrow> P"
assumes Abrupt:
"\<And>t'.
\<lbrakk>\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =n\<Rightarrow> Abrupt t';
t = Abrupt (return s t')\<rbrakk>
\<Longrightarrow> P"
assumes Fault:
"\<And>f.
\<lbrakk>\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =n\<Rightarrow> Fault f;
t = Fault f\<rbrakk>
\<Longrightarrow> P"
assumes Stuck:
"\<lbrakk>\<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =n\<Rightarrow> Stuck;
t = Stuck\<rbrakk>
\<Longrightarrow> P"
assumes Undef:
"\<lbrakk>\<Gamma> p = None; t = Stuck\<rbrakk> \<Longrightarrow> P"
shows "P"
using execn_block [unfolded block_def] Normal Abrupt Fault Stuck Undef
by (rule execn_block_exn_Normal_elim)
lemma execn_call_exn_Normal_elim [consumes 1]:
assumes exec_call: "\<Gamma>\<turnstile>\<langle>call_exn init p return result_exn c,Normal s\<rangle> =n\<Rightarrow> t"
assumes Normal:
"\<And>bdy i t'.
\<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =i\<Rightarrow> Normal t';
\<Gamma>\<turnstile>\<langle>c s t',Normal (return s t')\<rangle> =Suc i\<Rightarrow> t; n = Suc i\<rbrakk>
\<Longrightarrow> P"
assumes Abrupt:
"\<And>bdy i t'.
\<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =i\<Rightarrow> Abrupt t'; n = Suc i;
t = Abrupt (result_exn (return s t') t')\<rbrakk>
\<Longrightarrow> P"
assumes Fault:
"\<And>bdy i f.
\<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =i\<Rightarrow> Fault f; n = Suc i;
t = Fault f\<rbrakk>
\<Longrightarrow> P"
assumes Stuck:
"\<And>bdy i.
\<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> =i\<Rightarrow> Stuck; n = Suc i;
t = Stuck\<rbrakk>
\<Longrightarrow> P"
assumes Undef:
"\<And>i. \<lbrakk>\<Gamma> p = None; n = Suc i; t = Stuck\<rbrakk> \<Longrightarrow> P"
shows "P"
using exec_call
apply (unfold call_exn_def)
apply (cases n)
apply (simp only: block_exn_def)
apply (fastforce elim: execn_Normal_elim_cases)
apply (cases "\<Gamma> p")
apply (erule execn_block_exn_Normal_elim)
apply (elim execn_Normal_elim_cases)
apply simp
apply simp
apply (elim execn_Normal_elim_cases)
apply simp
apply simp
apply (elim execn_Normal_elim_cases)
apply simp
apply simp
apply (elim execn_Normal_elim_cases)
apply simp
apply (rule Undef,assumption,assumption,assumption)
apply (rule Undef,assumption+)
apply (erule execn_block_exn_Normal_elim)
apply (elim execn_Normal_elim_cases)
apply simp
apply (rule Normal,assumption+)
apply simp
apply (elim execn_Normal_elim_cases)
apply simp
apply (rule Abrupt,assumption+)
apply simp
apply (elim execn_Normal_elim_cases)
apply simp
apply (rule Fault,assumption+)
apply simp
apply (elim execn_Normal_elim_cases)
apply simp
apply (rule Stuck,assumption,assumption,assumption,assumption)
apply (rule Undef,assumption,assumption,assumption)
apply (rule Undef,assumption+)
done
lemma execn_call_Normal_elim [consumes 1]:
assumes exec_call: "\<Gamma>\<turnstile>\<langle>call init p return c,Normal s\<rangle> =n\<Rightarrow> t"
assumes Normal:
@ -719,45 +1134,9 @@ assumes Stuck:
assumes Undef:
"\<And>i. \<lbrakk>\<Gamma> p = None; n = Suc i; t = Stuck\<rbrakk> \<Longrightarrow> P"
shows "P"
using exec_call
apply (unfold call_def)
apply (cases n)
apply (simp only: block_def)
apply (fastforce elim: execn_Normal_elim_cases)
apply (cases "\<Gamma> p")
apply (erule execn_block_Normal_elim)
apply (elim execn_Normal_elim_cases)
apply simp
apply simp
apply (elim execn_Normal_elim_cases)
apply simp
apply simp
apply (elim execn_Normal_elim_cases)
apply simp
apply simp
apply (elim execn_Normal_elim_cases)
apply simp
apply (rule Undef,assumption,assumption,assumption)
apply (rule Undef,assumption+)
apply (erule execn_block_Normal_elim)
apply (elim execn_Normal_elim_cases)
apply simp
apply (rule Normal,assumption+)
apply simp
apply (elim execn_Normal_elim_cases)
apply simp
apply (rule Abrupt,assumption+)
apply simp
apply (elim execn_Normal_elim_cases)
apply simp
apply (rule Fault,assumption+)
apply simp
apply (elim execn_Normal_elim_cases)
apply simp
apply (rule Stuck,assumption,assumption,assumption,assumption)
apply (rule Undef,assumption,assumption,assumption)
apply (rule Undef,assumption+)
done
using exec_call [simplified call_call_exn] Normal Abrupt Fault Stuck Undef
by (rule execn_call_exn_Normal_elim)
lemma execn_dynCall:
"\<lbrakk>\<Gamma>\<turnstile>\<langle>call init (p s) return c,Normal s\<rangle> =n\<Rightarrow> t\<rbrakk>
@ -766,6 +1145,13 @@ lemma execn_dynCall:
apply (simp add: dynCall_def)
by (rule DynCom)
lemma execn_dynCall_exn:
"\<lbrakk>\<Gamma>\<turnstile>\<langle>call_exn init (p s) return result_exn c,Normal s\<rangle> =n\<Rightarrow> t\<rbrakk>
\<Longrightarrow>
\<Gamma>\<turnstile>\<langle>dynCall_exn f UNIV init p return result_exn c,Normal s\<rangle> =n\<Rightarrow> t"
apply (simp add: dynCall_exn_def)
by (rule DynCom)
lemma execn_dynCall_Normal_elim:
assumes exec: "\<Gamma>\<turnstile>\<langle>dynCall init p return c,Normal s\<rangle> =n\<Rightarrow> t"
assumes "\<Gamma>\<turnstile>\<langle>call init (p s) return c,Normal s\<rangle> =n\<Rightarrow> t \<Longrightarrow> P"
@ -776,9 +1162,134 @@ lemma execn_dynCall_Normal_elim:
apply fact
done
lemma execn_guards_Normal_elim_cases [consumes 1, case_names noFault someFault]:
assumes exec_guards: "\<Gamma>\<turnstile>\<langle>guards gs c,Normal s\<rangle> =n\<Rightarrow> t"
assumes noFault: "\<forall>f g. (f, g) \<in> set gs \<longrightarrow> s \<in> g \<Longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t \<Longrightarrow> P"
assumes someFault: "\<And>f g. find (\<lambda>(f,g). s \<notin> g) gs = Some (f, g) \<Longrightarrow> t = Fault f \<Longrightarrow> P"
shows "P"
using exec_guards noFault someFault
proof (induct gs)
case Nil
then show ?case by simp
next
case (Cons pg gs)
obtain f g where pg: "pg = (f, g)"
by (cases pg) auto
show ?thesis
proof (cases "s \<in> g")
case True
from Cons.prems(1) have exec_gs: "\<Gamma>\<turnstile> \<langle>guards gs c,Normal s\<rangle> =n\<Rightarrow> t"
by (simp add: pg) (meson True pg execn_Normal_elim_cases)
from Cons.hyps [OF exec_gs] Cons.prems(2,3)
show ?thesis
by (simp add: pg True)
next
case False
from Cons.prems(1) have t: "t = Fault f"
by (simp add: pg) (meson False pg execn_Normal_elim_cases)
from t Cons.prems(3)
show ?thesis
by (simp add: pg False)
qed
qed
lemma execn_maybe_guard_Normal_elim_cases [consumes 1, case_names noFault someFault]:
assumes exec_guards: "\<Gamma>\<turnstile>\<langle>maybe_guard f g c,Normal s\<rangle> =n\<Rightarrow> t"
assumes noFault: "s \<in> g \<Longrightarrow> \<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t \<Longrightarrow> P"
assumes someFault: "s \<notin> g \<Longrightarrow> t = Fault f \<Longrightarrow> P"
shows "P"
using exec_guards noFault someFault
by (metis UNIV_I execn_Normal_elim_cases(5) maybe_guard_def)
lemma execn_guards_noFault:
assumes exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t"
assumes noFault: "\<forall>f g. (f, g) \<in> set gs \<longrightarrow> s \<in> g"
shows "\<Gamma>\<turnstile>\<langle>guards gs c,Normal s\<rangle> =n\<Rightarrow> t"
using exec noFault by (induct gs) (auto intro: execn.intros)
lemma execn_guards_Fault:
assumes Fault: "find (\<lambda>(f,g). s \<notin> g) gs = Some (f, g)"
shows "\<Gamma>\<turnstile>\<langle>guards gs c,Normal s\<rangle> =n\<Rightarrow> Fault f"
using Fault by (induct gs) (auto intro: execn.intros split: prod.splits if_split_asm)
lemma execn_maybe_guard_noFault:
assumes exec: "\<Gamma>\<turnstile>\<langle>c,Normal s\<rangle> =n\<Rightarrow> t"
assumes noFault: "s \<in> g"
shows "\<Gamma>\<turnstile>\<langle>maybe_guard f g c,Normal s\<rangle> =n\<Rightarrow> t"
using exec noFault
by (auto intro: execn.intros simp add: maybe_guard_def)
lemma execn_maybe_guard_Fault:
assumes Fault: "s \<notin> g"
shows "\<Gamma>\<turnstile>\<langle>maybe_guard f g c,Normal s\<rangle> =n\<Rightarrow> Fault f"
using Fault by (auto simp add: maybe_guard_def intro: execn.intros split: prod.splits if_split_asm)
lemma execn_guards_DynCom_Normal_elim:
assumes exec: "\<Gamma>\<turnstile>\<langle>guards gs (DynCom c), Normal s\<rangle> =n\<Rightarrow> t"
assumes call: "\<Gamma>\<turnstile>\<langle>guards gs (c s), Normal s\<rangle> =n\<Rightarrow> t \<Longrightarrow> P"
shows "P"
using exec call proof (induct gs)
case Nil
then show ?case
apply simp
apply (erule execn_Normal_elim_cases)
apply simp
done
next
case (Cons g gs)
then show ?case
apply (cases g)
apply simp
apply (erule execn_Normal_elim_cases)
apply simp
apply (meson execn.Guard)
apply simp
apply (meson execn.GuardFault)
done
qed
lemma execn_maybe_guard_DynCom_Normal_elim:
assumes exec: "\<Gamma>\<turnstile>\<langle>maybe_guard f g (DynCom c), Normal s\<rangle> =n\<Rightarrow> t"
assumes call: "\<Gamma>\<turnstile>\<langle>maybe_guard f g (c s), Normal s\<rangle> =n\<Rightarrow> t \<Longrightarrow> P"
shows "P"
using exec call
by (metis execn.Guard execn.GuardFault execn_Normal_elim_cases(12) execn_Normal_elim_cases(5) maybe_guard_def)
lemma execn_guards_DynCom:
assumes exec_c: "\<Gamma>\<turnstile>\<langle>guards gs (c s), Normal s\<rangle> =n\<Rightarrow> t"
shows "\<Gamma>\<turnstile>\<langle>guards gs (DynCom c), Normal s\<rangle> =n\<Rightarrow> t"
using exec_c apply (induct gs)
apply (fastforce intro: execn.intros)
apply simp
by (metis execn.Guard execn.GuardFault execn_Normal_elim_cases)
lemma execn_maybe_guard_DynCom:
assumes exec_c: "\<Gamma>\<turnstile>\<langle>maybe_guard f g (c s), Normal s\<rangle> =n\<Rightarrow> t"
shows "\<Gamma>\<turnstile>\<langle>maybe_guard f g (DynCom c), Normal s\<rangle> =n\<Rightarrow> t"
using exec_c
apply (cases "g = UNIV")
subgoal
apply simp
apply (rule execn.intros)
apply simp
done
subgoal
apply (simp add: maybe_guard_def)
by (metis execn.DynCom execn.Guard execn.GuardFault execn_Normal_elim_cases(5))
done
lemma execn_dynCall_exn_Normal_elim:
assumes exec: "\<Gamma>\<turnstile>\<langle>dynCall_exn f g init p return result_exn c,Normal s\<rangle> =n\<Rightarrow> t"
assumes "\<Gamma>\<turnstile>\<langle>maybe_guard f g (call_exn init (p s) return result_exn c),Normal s\<rangle> =n\<Rightarrow> t \<Longrightarrow> P"
shows "P"
using exec
apply (simp add: dynCall_exn_def)
apply (erule execn_maybe_guard_DynCom_Normal_elim)
apply fact
done
lemma execn_Seq':
"\<lbrakk>\<Gamma>\<turnstile>\<langle>c1,s\<rangle> =n\<Rightarrow> s'; \<Gamma>\<turnstile>\<langle>c2,s'\<rangle> =n\<Rightarrow> s''\<rbrakk>
@ -4379,7 +4890,7 @@ subsection "Restriction of Procedure Environment"
lemma restrict_SomeD: "(m|\<^bsub>A\<^esub>) x = Some y \<Longrightarrow> m x = Some y"
by (auto simp add: restrict_map_def split: if_split_asm)
(* FIXME: To Map *)
(* fixme: To Map *)
lemma restrict_dom_same [simp]: "m|\<^bsub>dom m\<^esub> = m"
apply (rule ext)
apply (clarsimp simp add: restrict_map_def)

23
tools/c-parser/Simpl/Simpl.thy
View File

@ -1,28 +1,7 @@
(* Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: Simpl.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2008 Norbert Schirmer
Some rights reserved, TU Muenchen
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
Copyright (C) 2006-2008 Norbert Schirmer
*)
(*<*)
theory Simpl

23
tools/c-parser/Simpl/Simpl_Heap.thy
View File

@ -1,28 +1,7 @@
(* Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: Heap.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2004-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
Copyright (C) 2006-2008 Norbert Schirmer
*)
theory Simpl_Heap

21
tools/c-parser/Simpl/SmallStep.thy
View File

@ -1,29 +1,8 @@
(*
Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: SmallStep.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2006-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
section \<open>Small-Step Semantics and Infinite Computations\<close>

38
tools/c-parser/Simpl/StateSpace.thy
View File

@ -1,29 +1,10 @@
(*
Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: StateSpace.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2004-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
Copyright (c) 2022 Apple Inc. All rights reserved.
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
section \<open>State Space Template\<close>
@ -37,10 +18,21 @@ definition
where
"upd_globals upd s = s\<lparr>globals := upd (globals s)\<rparr>"
record ('g, 'n, 'val) stateSP = "'g state" +
locals :: "'n \<Rightarrow> 'val"
named_theorems state_simp
lemma upd_globals_conv: "upd_globals f = (\<lambda>s. s\<lparr>globals := f (globals s)\<rparr>)"
lemma upd_globals_conv [state_simp]: "upd_globals f = (\<lambda>s. s\<lparr>globals := f (globals s)\<rparr>)"
by (rule ext) (simp add: upd_globals_def)
record ('g, 'l) state_locals = "'g state" +
locals :: 'l
(*
record ('g, 'n, 'val) stateSP = "'g state" +
locals :: "'n \<Rightarrow> 'val"
*)
type_synonym ('g, 'n, 'val) stateSP = "('g, 'n \<Rightarrow> 'val) state_locals"
type_synonym ('g, 'n, 'val, 'x) stateSP_scheme = "('g, 'n \<Rightarrow> 'val, 'x) state_locals_scheme"
end

22
tools/c-parser/Simpl/SyntaxTest.thy
View File

@ -1,30 +1,10 @@
(*
Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: SyntaxTest.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2006-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
(*<*)
theory SyntaxTest imports HeapList Vcg begin

141
tools/c-parser/Simpl/Termination.thy
View File

@ -1,29 +1,9 @@
(*
Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: Termination.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2004-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
Copyright (c) 2022 Apple Inc. All rights reserved.
*)
section \<open>Terminating Programs\<close>
@ -207,17 +187,24 @@ next
qed
qed
lemma terminates_block_exn:
"\<lbrakk>\<Gamma>\<turnstile>bdy \<down> Normal (init s);
\<forall>t. \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t \<longrightarrow> \<Gamma>\<turnstile>c s t \<down> Normal (return s t)\<rbrakk>
\<Longrightarrow> \<Gamma>\<turnstile>block_exn init bdy return result_exn c \<down> Normal s"
apply (unfold block_exn_def)
apply (fastforce intro: terminates.intros elim!: exec_Normal_elim_cases
dest!: not_isAbrD)
done
lemma terminates_block:
"\<lbrakk>\<Gamma>\<turnstile>bdy \<down> Normal (init s);
\<forall>t. \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t \<longrightarrow> \<Gamma>\<turnstile>c s t \<down> Normal (return s t)\<rbrakk>
\<Longrightarrow> \<Gamma>\<turnstile>block init bdy return c \<down> Normal s"
apply (unfold block_def)
apply (fastforce intro: terminates.intros elim!: exec_Normal_elim_cases
dest!: not_isAbrD)
done
unfolding block_def
by (rule terminates_block_exn)
lemma terminates_block_elim [cases set, consumes 1]:
assumes termi: "\<Gamma>\<turnstile>block init bdy return c \<down> Normal s"
lemma terminates_block_exn_elim [cases set, consumes 1]:
assumes termi: "\<Gamma>\<turnstile>block_exn init bdy return result_exn c \<down> Normal s"
assumes e: "\<lbrakk>\<Gamma>\<turnstile>bdy \<down> Normal (init s);
\<forall>t. \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t \<longrightarrow> \<Gamma>\<turnstile>c s t \<down> Normal (return s t)
\<rbrakk> \<Longrightarrow> P"
@ -227,7 +214,7 @@ proof -
by (auto intro: exec.intros)
with termi
have "\<Gamma>\<turnstile>bdy \<down> Normal (init s)"
apply (unfold block_def)
apply (unfold block_exn_def)
apply (elim terminates_Normal_elim_cases)
by simp
moreover
@ -238,10 +225,10 @@ proof -
proof -
from exec_bdy
have "\<Gamma>\<turnstile>\<langle>Catch (Seq (Basic init) bdy)
(Seq (Basic (return s)) Throw),Normal s\<rangle> \<Rightarrow> Normal t"
(Seq (Basic (\<lambda>t. result_exn (return s t) t)) Throw),Normal s\<rangle> \<Rightarrow> Normal t"
by (fastforce intro: exec.intros)
with termi have "\<Gamma>\<turnstile>DynCom (\<lambda>t. Seq (Basic (return s)) (c s t)) \<down> Normal t"
apply (unfold block_def)
apply (unfold block_exn_def)
apply (elim terminates_Normal_elim_cases)
by simp
thus ?thesis
@ -253,6 +240,14 @@ proof -
ultimately show P by (iprover intro: e)
qed
lemma terminates_block_elim [cases set, consumes 1]:
assumes termi: "\<Gamma>\<turnstile>block init bdy return c \<down> Normal s"
assumes e: "\<lbrakk>\<Gamma>\<turnstile>bdy \<down> Normal (init s);
\<forall>t. \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t \<longrightarrow> \<Gamma>\<turnstile>c s t \<down> Normal (return s t)
\<rbrakk> \<Longrightarrow> P"
shows P
using termi e unfolding block_def by (rule terminates_block_exn_elim)
lemma terminates_call:
"\<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>bdy \<down> Normal (init s);
@ -264,6 +259,16 @@ lemma terminates_call:
apply (auto elim: exec_Normal_elim_cases)
done
lemma terminates_call_exn:
"\<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>bdy \<down> Normal (init s);
\<forall>t. \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t \<longrightarrow> \<Gamma>\<turnstile>c s t \<down> Normal (return s t)\<rbrakk>
\<Longrightarrow> \<Gamma>\<turnstile>call_exn init p return result_exn c \<down> Normal s"
apply (unfold call_exn_def)
apply (rule terminates_block_exn)
apply (iprover intro: terminates.intros)
apply (auto elim: exec_Normal_elim_cases)
done
lemma terminates_callUndefined:
"\<lbrakk>\<Gamma> p = None\<rbrakk>
\<Longrightarrow> \<Gamma>\<turnstile>call init p return result \<down> Normal s"
@ -273,8 +278,17 @@ lemma terminates_callUndefined:
apply (auto elim: exec_Normal_elim_cases)
done
lemma terminates_call_elim [cases set, consumes 1]:
assumes termi: "\<Gamma>\<turnstile>call init p return c \<down> Normal s"
lemma terminates_call_exnUndefined:
"\<lbrakk>\<Gamma> p = None\<rbrakk>
\<Longrightarrow> \<Gamma>\<turnstile>call_exn init p return result_exn result \<down> Normal s"
apply (unfold call_exn_def)
apply (rule terminates_block_exn)
apply (iprover intro: terminates.intros)
apply (auto elim: exec_Normal_elim_cases)
done
lemma terminates_call_exn_elim [cases set, consumes 1]:
assumes termi: "\<Gamma>\<turnstile>call_exn init p return result_exn c \<down> Normal s"
assumes bdy: "\<And>bdy. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>bdy \<down> Normal (init s);
\<forall>t. \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t \<longrightarrow> \<Gamma>\<turnstile>c s t \<down> Normal (return s t)\<rbrakk> \<Longrightarrow> P"
assumes undef: "\<lbrakk>\<Gamma> p = None\<rbrakk> \<Longrightarrow> P"
@ -282,8 +296,8 @@ shows P
apply (cases "\<Gamma> p")
apply (erule undef)
using termi
apply (unfold call_def)
apply (erule terminates_block_elim)
apply (unfold call_exn_def)
apply (erule terminates_block_exn_elim)
apply (erule terminates_Normal_elim_cases)
apply simp
apply (frule (1) bdy)
@ -292,6 +306,15 @@ apply assumption
apply simp
done
lemma terminates_call_elim [cases set, consumes 1]:
assumes termi: "\<Gamma>\<turnstile>call init p return c \<down> Normal s"
assumes bdy: "\<And>bdy. \<lbrakk>\<Gamma> p = Some bdy; \<Gamma>\<turnstile>bdy \<down> Normal (init s);
\<forall>t. \<Gamma>\<turnstile>\<langle>bdy,Normal (init s)\<rangle> \<Rightarrow> Normal t \<longrightarrow> \<Gamma>\<turnstile>c s t \<down> Normal (return s t)\<rbrakk> \<Longrightarrow> P"
assumes undef: "\<lbrakk>\<Gamma> p = None\<rbrakk> \<Longrightarrow> P"
shows P
using termi bdy undef unfolding call_call_exn by (rule terminates_call_exn_elim)
lemma terminates_dynCall:
"\<lbrakk>\<Gamma>\<turnstile>call init (p s) return c \<down> Normal s\<rbrakk>
\<Longrightarrow> \<Gamma>\<turnstile>dynCall init p return c \<down> Normal s"
@ -299,6 +322,28 @@ lemma terminates_dynCall:
apply (auto intro: terminates.intros terminates_call)
done
lemma terminates_guards: "\<Gamma>\<turnstile>c \<down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>guards gs c \<down> Normal s"
by (induct gs) (auto intro: terminates.intros)
lemma terminates_guards_Fault: "find (\<lambda>(f, g). s \<notin> g) gs = Some (f, g) \<Longrightarrow> \<Gamma>\<turnstile>guards gs c \<down> Normal s"
by (induct gs) (auto intro: terminates.intros split: if_split_asm prod.splits)
lemma terminates_maybe_guard_Fault: "s \<notin> g \<Longrightarrow> \<Gamma>\<turnstile>maybe_guard f g c \<down> Normal s"
by (metis UNIV_I maybe_guard_def terminates.GuardFault)
lemma terminates_guards_DynCom: "\<Gamma>\<turnstile>(c s) \<down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>guards gs (DynCom c) \<down> Normal s"
by (induct gs) (auto intro: terminates.intros)
lemma terminates_maybe_guard_DynCom: "\<Gamma>\<turnstile>(c s) \<down> Normal s \<Longrightarrow> \<Gamma>\<turnstile>maybe_guard f g (DynCom c) \<down> Normal s"
by (metis maybe_guard_def terminates.DynCom terminates.Guard terminates.GuardFault)
lemma terminates_dynCall_exn:
"\<lbrakk>\<Gamma>\<turnstile>call_exn init (p s) return result_exn c \<down> Normal s\<rbrakk>
\<Longrightarrow> \<Gamma>\<turnstile>dynCall_exn f g init p return result_exn c \<down> Normal s"
apply (unfold dynCall_exn_def)
by (rule terminates_maybe_guard_DynCom)
lemma terminates_dynCall_elim [cases set, consumes 1]:
assumes termi: "\<Gamma>\<turnstile>dynCall init p return c \<down> Normal s"
assumes "\<lbrakk>\<Gamma>\<turnstile>call init (p s) return c \<down> Normal s\<rbrakk> \<Longrightarrow> P"
@ -309,6 +354,34 @@ apply (elim terminates_Normal_elim_cases)
apply fact
done
lemma terminates_guards_elim [cases set, consumes 1, case_names noFault someFault]:
assumes termi: "\<Gamma>\<turnstile>guards gs c \<down> Normal s"
assumes noFault: "\<lbrakk>\<forall>f g. (f, g) \<in> set gs \<longrightarrow> s \<in> g; \<Gamma>\<turnstile>c \<down> Normal s\<rbrakk> \<Longrightarrow> P"
assumes someFault: "\<And>f g. find (\<lambda>(f,g). s \<notin> g) gs = Some (f, g) \<Longrightarrow> P"
shows P
using termi noFault someFault
by (induct gs)
(auto elim: terminates_Normal_elim_cases split: if_split_asm prod.splits)
lemma terminates_maybe_guard_elim [cases set, consumes 1, case_names noFault someFault]:
assumes termi: "\<Gamma>\<turnstile>maybe_guard f g c \<down> Normal s"
assumes noFault: "\<lbrakk>s \<in> g; \<Gamma>\<turnstile>c \<down> Normal s\<rbrakk> \<Longrightarrow> P"
assumes someFault: "s \<notin> g \<Longrightarrow> P"
shows P
using termi noFault someFault
by (metis maybe_guard_def terminates_Normal_elim_cases(2))
lemma terminates_dynCall_exn_elim [cases set, consumes 1, case_names noFault someFault]:
assumes termi: "\<Gamma>\<turnstile>dynCall_exn f g init p return result_exn c \<down> Normal s"
assumes noFault: "\<lbrakk>s \<in> g;
\<Gamma>\<turnstile>call_exn init (p s) return result_exn c \<down> Normal s\<rbrakk> \<Longrightarrow> P"
assumes someFault: "s \<notin> g \<Longrightarrow> P"
shows P
using termi noFault someFault
apply (unfold dynCall_exn_def)
apply (erule terminates_maybe_guard_elim)
apply (auto elim: terminates_Normal_elim_cases)
done
(* ************************************************************************* *)
subsection \<open>Lemmas about @{const "sequence"}, @{const "flatten"} and

35
tools/c-parser/Simpl/UserGuide.thy
View File

@ -1,28 +1,8 @@
(* Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: UserGuide.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2004-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
Copyright (c) 2022 Apple Inc. All rights reserved.
*)
section \<open>User Guide \label{sec:UserGuide}\<close>
@ -222,7 +202,7 @@ for procedure calls (that creates the proper @{term init}, @{term return} and
@{term result} functions on the fly) and creates locales and statespaces to
reason about the procedure. The purpose of locales is to set up logical contexts
to support modular reasoning. Locales can be seen as freeze-dried proof contexts that
get alive as you setup a new lemma or theorem (\<^cite>\<open>"Ballarin-04-locales"\<close>).
get alive as you setup a new lemma or theorem (\cite{Ballarin-04-locales}).
The locale the user deals with is named \<open>Square_impl\<close>.
It defines the procedure name (internally @{term "Square_'proc"}), the procedure body
(named \<open>Square_body\<close>) and the statespaces for parameters and local and
@ -344,7 +324,7 @@ subsubsection \<open>Usage\<close>
text\<open>Let us see how we can use procedure specifications.\<close>
(* FIXME: maybe don't show this at all *)
(* fixme: maybe don't show this at all *)
lemma (in Square_impl)
shows "\<Gamma>\<turnstile>\<lbrace>\<acute>I = 2\<rbrace> \<acute>R :== CALL Square(\<acute>I) \<lbrace>\<acute>R = 4\<rbrace>"
txt \<open>Remember that we have already proven @{thm [source] "Square_spec"} in the locale
@ -537,7 +517,7 @@ the lookup of variable \<open>x\<close> in the state
\<open>\<sigma>\<close>.
The approach to specify procedures on lists
basically follows \<^cite>\<open>"MehtaN-CADE03"\<close>. From the pointer structure
basically follows \cite{MehtaN-CADE03}. From the pointer structure
in the heap we (relationally) abstract to HOL lists of references. Then
we can specify further properties on the level of HOL lists, rather then
on the heap. The basic abstractions are:
@ -795,7 +775,7 @@ since the lists are already uniquely determined by the relational abstraction:
\<close>
text \<open>
The next contrived example is taken from \<^cite>\<open>"Homeier-95-vcg"\<close>, to illustrate
The next contrived example is taken from \cite{Homeier-95-vcg}, to illustrate
a more complex termination criterion for mutually recursive procedures. The procedures
do not calculate anything useful.
@ -873,7 +853,8 @@ apply (hoare_rule HoareTotal_ProcRec2
\<close>
txt \<open>@{subgoals [margin=75,display]}\<close>
apply simp_all
by (vcg,force)+
by (vcg,simp)+
text \<open>By doing some arithmetic we can express the termination condition with a single
measure function.
\<close>
@ -1534,7 +1515,7 @@ procedures init' (|p) =
subsubsection \<open>Extending State Spaces\<close>
text \<open>
The records in Isabelle are
extensible \<^cite>\<open>"Nipkow-02-hol" and "NaraschewskiW-TPHOLs98"\<close>. In principle this can be exploited
extensible \cite{Nipkow-02-hol,NaraschewskiW-TPHOLs98}. In principle this can be exploited
during verification. The state space can be extended while we we add procedures.
But there is one major drawback:
\begin{itemize}

51
tools/c-parser/Simpl/Vcg.thy
View File

@ -1,28 +1,9 @@
(* Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: Vcg.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2004-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
Copyright (c) 2022 Apple Inc. All rights reserved.
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
section \<open>Facilitating the Hoare Logic\<close>
@ -374,6 +355,9 @@ syntax "_Call" :: "'p \<Rightarrow> actuals \<Rightarrow> (('a,string,'f) com)"
"_GuardedCall" :: "'p \<Rightarrow> actuals \<Rightarrow> (('a,string,'f) com)" ("CALL\<^sub>g __" [1000,1000] 21)
"_CallAss":: "'a \<Rightarrow> 'p \<Rightarrow> actuals \<Rightarrow> (('a,string,'f) com)"
("_ :== CALL __" [30,1000,1000] 21)
"_Call_exn" :: "'p \<Rightarrow> actuals \<Rightarrow> (('a,string,'f) com)" ("CALL\<^sub>e __" [1000,1000] 21)
"_CallAss_exn":: "'a \<Rightarrow> 'p \<Rightarrow> actuals \<Rightarrow> (('a,string,'f) com)"
("_ :== CALL\<^sub>e __" [30,1000,1000] 21)
"_Proc" :: "'p \<Rightarrow> actuals \<Rightarrow> (('a,string,'f) com)" ("PROC __" 21)
"_ProcAss":: "'a \<Rightarrow> 'p \<Rightarrow> actuals \<Rightarrow> (('a,string,'f) com)"
("_ :== PROC __" [30,1000,1000] 21)
@ -383,6 +367,9 @@ syntax "_Call" :: "'p \<Rightarrow> actuals \<Rightarrow> (('a,string,'f) com)"
"_GuardedDynCall" :: "'p \<Rightarrow> actuals \<Rightarrow> (('a,string,'f) com)" ("DYNCALL\<^sub>g __" [1000,1000] 21)
"_DynCallAss":: "'a \<Rightarrow> 'p \<Rightarrow> actuals \<Rightarrow> (('a,string,'f) com)"
("_ :== DYNCALL __" [30,1000,1000] 21)
"_DynCall_exn" :: "'p \<Rightarrow> actuals \<Rightarrow> (('a,string,'f) com)" ("DYNCALL\<^sub>e __" [1000,1000] 21)
"_DynCallAss_exn":: "'a \<Rightarrow> 'p \<Rightarrow> actuals \<Rightarrow> (('a,string,'f) com)"
("_ :== DYNCALL\<^sub>e __" [30,1000,1000] 21)
"_GuardedDynCallAss":: "'a \<Rightarrow> 'p \<Rightarrow> actuals \<Rightarrow> (('a,string,'f) com)"
("_ :== DYNCALL\<^sub>g __" [30,1000,1000] 21)
@ -440,7 +427,7 @@ parse_translation \<open>
| idx (x::xs) y = if x=y then 0 else (idx xs y)+1
fun gen_update ctxt names (name,t) =
Hoare_Syntax.update_comp ctxt [] false true name (Bound (idx names name)) t
Hoare_Syntax.update_comp ctxt NONE [] false true name (Bound (idx names name)) t
fun gen_updates ctxt names t = Library.foldr (gen_update ctxt names) (names,t)
@ -528,17 +515,21 @@ parse_translation \<open>
parse_translation \<open>
[(@{syntax_const "_antiquoteOld"}, Hoare_Syntax.antiquoteOld_tr),
(@{syntax_const "_Call"}, Hoare_Syntax.call_tr false false),
(@{syntax_const "_Call"}, Hoare_Syntax.call_tr false false []),
(@{syntax_const "_Call_exn"}, Hoare_Syntax.call_tr false true []),
(@{syntax_const "_FCall"}, Hoare_Syntax.fcall_tr),
(@{syntax_const "_CallAss"}, Hoare_Syntax.call_ass_tr false false),
(@{syntax_const "_GuardedCall"}, Hoare_Syntax.call_tr false true),
(@{syntax_const "_GuardedCallAss"}, Hoare_Syntax.call_ass_tr false true),
(@{syntax_const "_CallAss"}, Hoare_Syntax.call_ass_tr false false []),
(@{syntax_const "_CallAss_exn"}, Hoare_Syntax.call_ass_tr false true []),
(@{syntax_const "_GuardedCall"}, Hoare_Syntax.call_tr false true []),
(@{syntax_const "_GuardedCallAss"}, Hoare_Syntax.call_ass_tr false true []),
(@{syntax_const "_Proc"}, Hoare_Syntax.proc_tr),
(@{syntax_const "_ProcAss"}, Hoare_Syntax.proc_ass_tr),
(@{syntax_const "_DynCall"}, Hoare_Syntax.call_tr true false),
(@{syntax_const "_DynCallAss"}, Hoare_Syntax.call_ass_tr true false),
(@{syntax_const "_GuardedDynCall"}, Hoare_Syntax.call_tr true true),
(@{syntax_const "_GuardedDynCallAss"}, Hoare_Syntax.call_ass_tr true true),
(@{syntax_const "_DynCall"}, Hoare_Syntax.call_tr true false []),
(@{syntax_const "_DynCall_exn"}, Hoare_Syntax.call_tr true true []),
(@{syntax_const "_DynCallAss"}, Hoare_Syntax.call_ass_tr true false []),
(@{syntax_const "_DynCallAss_exn"}, Hoare_Syntax.call_ass_tr true true []),
(@{syntax_const "_GuardedDynCall"}, Hoare_Syntax.call_tr true true []),
(@{syntax_const "_GuardedDynCallAss"}, Hoare_Syntax.call_ass_tr true true []),
(@{syntax_const "_BasicBlock"}, Hoare_Syntax.basic_assigns_tr)]
\<close>
@ -656,6 +647,8 @@ print_translation \<open>
print_translation \<open>
[(@{const_syntax call}, Hoare_Syntax.call_tr'),
(@{const_syntax dynCall}, Hoare_Syntax.dyn_call_tr'),
(@{const_syntax call_exn}, Hoare_Syntax.call_exn_tr'),
(@{const_syntax dynCall_exn}, Hoare_Syntax.dyn_call_exn_tr'),
(@{const_syntax fcall}, Hoare_Syntax.fcall_tr'),
(@{const_syntax Call}, Hoare_Syntax.proc_tr')]
\<close>

21
tools/c-parser/Simpl/XVcg.thy
View File

@ -1,29 +1,8 @@
(*
Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: XVcg.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2006-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
theory XVcg

21
tools/c-parser/Simpl/ex/Closure.thy
View File

@ -1,29 +1,8 @@
(*
Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: Closure.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2006-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
section "Experiments with Closures"

28
tools/c-parser/Simpl/ex/ClosureEx.thy
View File

@ -1,29 +1,8 @@
(*
Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: ClosureEx.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2006-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
theory ClosureEx
@ -163,13 +142,18 @@ apply (simp only: simp_thms)
apply clarsimp
done
declare [[hoare_trace = 1]]
ML \<open>
val hoare_tacs = #hoare_tacs (Hoare.get_data @{context});
\<close>
lemma (in NewCounter_impl')
shows "\<Gamma>\<turnstile> \<lbrace>1 \<le> \<acute>free\<rbrace>
\<acute>c :== CALL NewCounter ();;
dynCallClosure (\<lambda>s. s) upd c_' (\<lambda>s t. s\<lparr>globals := globals t\<rparr>)
(\<lambda>s t. Basic (\<lambda>u. u\<lparr>r_' := r_' t\<rparr>))
\<lbrace>\<acute>r=1\<rbrace>"
apply vcg_step
apply vcg_step
apply (rule dynCallClosure)
prefer 2
apply vcg_step

25
tools/c-parser/Simpl/ex/Compose.thy
View File

@ -1,29 +1,10 @@
(*
Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: Compose.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2006-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
Copyright (c) 2022 Apple Inc. All rights reserved.
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
section "Experiments on State Composition"
@ -1272,7 +1253,7 @@ lemma lift\<^sub>c_block [simp]: "lift\<^sub>c prj inject (block init bdy return
block (lift\<^sub>f prj inject init) (lift\<^sub>c prj inject bdy)
(\<lambda>s. (lift\<^sub>f prj inject (return (prj s))))
(\<lambda>s t. lift\<^sub>c prj inject (c (prj s) (prj t)))"
by (simp add: block_def)
by (simp add: block_def block_exn_def)
(*
lemma lift\<^sub>c_block [simp]: "lift\<^sub>c prj inject (block init bdy return c) =
@ -1294,7 +1275,7 @@ lemma rename_whileAnno [simp]: "rename h (whileAnno b I V c) =
lemma rename_block [simp]: "rename h (block init bdy return c) =
block init (rename h bdy) return (\<lambda>s t. rename h (c s t))"
by (simp add: block_def)
by (simp add: block_def block_exn_def)
lemma rename_call [simp]: "rename h (call init p return c) =
call init (h p) return (\<lambda>s t. rename h (c s t))"

21
tools/c-parser/Simpl/ex/ComposeEx.thy
View File

@ -1,29 +1,8 @@
(*
Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: ComposeEx.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2006-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
theory ComposeEx imports Compose "../Vcg" "../HeapList" begin

21
tools/c-parser/Simpl/ex/ProcParEx.thy
View File

@ -1,29 +1,8 @@
(*
Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: ProcParEx.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2006-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
section "Examples for Procedures as Parameters"

23
tools/c-parser/Simpl/ex/ProcParExSP.thy
View File

@ -1,29 +1,10 @@
(*
Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: ProcParEx.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2007-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
Copyright (c) 2022 Apple Inc. All rights reserved.
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
section "Examples for Procedures as Parameters using Statespaces"
@ -87,7 +68,7 @@ declare [[hoare_use_call_tr' = true]]
end
(* FIXME: typing issue with modifies locale*)
(* fixme: typing issue with modifies locale*)
procedures
LEQ (i::nat,j::nat | r::bool) "\<acute>r :== \<acute>i \<le> \<acute>j"
LEQ_spec: "\<forall>\<sigma>. \<Gamma>\<turnstile> {\<sigma>} PROC LEQ(\<acute>i,\<acute>j,\<acute>r) \<lbrace>\<acute>r = (\<^bsup>\<sigma>\<^esup>i \<le> \<^bsup>\<sigma>\<^esup>j)\<rbrace>"

23
tools/c-parser/Simpl/ex/Quicksort.thy
View File

@ -1,29 +1,8 @@
(*
Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: Quicksort.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2004-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
Copyright (C) 2006-2008 Norbert Schirmer
*)
section "Example: Quicksort on Heap Lists"

23
tools/c-parser/Simpl/ex/VcgEx.thy
View File

@ -1,29 +1,8 @@
(*
Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: VcgEx.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2004-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
Copyright (C) 2006-2008 Norbert Schirmer
*)
section \<open>Examples using the Verification Environment\<close>

23
tools/c-parser/Simpl/ex/VcgExSP.thy
View File

@ -1,29 +1,8 @@
(*
Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: VcgEx.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2004-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
Copyright (C) 2006-2008 Norbert Schirmer
*)
section \<open>Examples using Statespaces\<close>

50
tools/c-parser/Simpl/ex/VcgExTotal.thy
View File

@ -1,29 +1,9 @@
(*
Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: VcgExTotal.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2006-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
section \<open>Examples for Total Correctness\<close>
@ -318,7 +298,10 @@ lemma (in pedal_coast_clique)
measure (\<lambda>p. if p = coast_'proc then 1 else 0))
(\<lambda>(s,p). (\<^bsup>s\<^esup>N + \<^bsup>s\<^esup>M,p))"])
apply simp_all
apply (vcg,force)+
apply vcg
apply simp
apply vcg
apply simp
done
lemma (in pedal_coast_clique)
@ -329,7 +312,10 @@ lemma (in pedal_coast_clique)
measure (\<lambda>p. if p = coast_'proc then 1 else 0))
(\<lambda>(s,p). (\<^bsup>s\<^esup>N + \<^bsup>s\<^esup>M,p))"])
apply simp_all
apply (vcg,force)+
apply vcg
apply simp
apply vcg
apply simp
done
@ -341,7 +327,11 @@ lemma (in pedal_coast_clique)
apply(hoare_rule HoareTotal_ProcRec2
[where ?r= "measure (\<lambda>(s,p). \<^bsup>s\<^esup>N + \<^bsup>s\<^esup>M + (if p = coast_'proc then 1 else 0))"])
apply simp_all
apply (vcg,force)+
apply vcg
apply simp
apply arith
apply vcg
apply simp
done
@ -352,8 +342,11 @@ lemma (in pedal_coast_clique)
[where ?r= "(\<lambda>(s,p). \<^bsup>s\<^esup>N) <*mlex*> (\<lambda>(s,p). \<^bsup>s\<^esup>M) <*mlex*>
measure (\<lambda>(s,p). if p = coast_'proc then 1 else 0)"])
apply simp_all
apply (vcg,force)+
done
apply vcg
apply simp
apply vcg
apply simp
done
lemma (in pedal_coast_clique)
@ -363,8 +356,11 @@ lemma (in pedal_coast_clique)
[where ?r= "measure (\<lambda>s. \<^bsup>s\<^esup>N + \<^bsup>s\<^esup>M) <*lex*>
measure (\<lambda>p. if p = coast_'proc then 1 else 0)"])
apply simp_all
apply (vcg,force)+
done
apply vcg
apply simp
apply vcg
apply simp
done
end

21
tools/c-parser/Simpl/ex/XVcgEx.thy
View File

@ -1,29 +1,8 @@
(*
Author: Norbert Schirmer
Maintainer: Norbert Schirmer, norbert.schirmer at web de
License: LGPL
*)
(* Title: XVcgEx.thy
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2006-2008 Norbert Schirmer
Some rights reserved, TU Muenchen
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
*)
section "Examples for Parallel Assignments"

81
tools/c-parser/Simpl/generalise_state.ML
View File

@ -1,41 +1,30 @@
(* Title: generalise_state.ML
Author: Norbert Schirmer, TU Muenchen
Copyright (C) 2005-2007 Norbert Schirmer
This library is free software; you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as
published by the Free Software Foundation; either version 2.1 of the
License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but
WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
USA
Copyright (C) 2006-2008 Norbert Schirmer
Copyright (c) 2022 Apple Inc. All rights reserved.
*)
signature SPLIT_STATE =
sig
val isState: term -> bool
val abs_state: term -> term option
sig val isState: Proof.context -> term -> bool
val abs_state: Proof.context -> term -> term option
val abs_var: Proof.context -> term -> (string * typ)
val split_state: Proof.context -> string -> typ -> term -> (term * term list)
val ex_tac: Proof.context -> term list -> tactic
val ex_tac: Proof.context -> term list -> int -> tactic
(* the term-list is the list of selectors as
returned by split_state. They may be used to
construct the instatiation of the existentially
construct the instantiation of the existentially
quantified state.
*)
end;
functor GeneraliseFun (structure SplitState: SPLIT_STATE) =
signature GENERALISE =
sig
val GENERALISE: Proof.context -> int -> tactic
end
functor Generalise (structure SplitState: SPLIT_STATE) : GENERALISE =
struct
val genConj = @{thm generaliseConj};
@ -131,7 +120,7 @@ fun split_thm qnt ctxt s T t =
(HOLogic.mk_Trueprop (list_exists (vs, t')),
HOLogic.mk_Trueprop (HOLogic.mk_exists (s,T,t))))
in (case qnt of
Hol_ex => Goal.prove ctxt [] [] prop (fn _ => SplitState.ex_tac ctxt vars)
Hol_ex => Goal.prove ctxt [] [] prop (fn _ => SplitState.ex_tac ctxt vars 1)
| _ => let
val rP = conc_of genRefl';
val thm0 = Thm.instantiate (TVars.empty, Vars.make [(dest_Var rP, Thm.cterm_of ctxt prop)]) genRefl';
@ -170,7 +159,7 @@ fun decomp ctxt (Const (@{const_name HOL.conj}, _) $ t $ t', ct) =
val genAll' = Drule.rename_bvars [(s,x)] genAll;
val (Const (@{const_name Pure.all},_)$Abs (s',_,_)) = genAllShift |> Thm.prems_of |> hd |> dest_prop;
val genAllShift' = Drule.rename_bvars [(s',x)] genAllShift;
in if SplitState.isState (allc$Abs abst)
in if SplitState.isState ctxt (allc$Abs abst)
then ([Thm.term_of cb],[cb], fn [thm] =>
let val P = HOLogic.dest_Trueprop (dest_prop (prem_of thm));
val thm' = split_thm Hol_all ctxt x' T P;
@ -190,7 +179,7 @@ fun decomp ctxt (Const (@{const_name HOL.conj}, _) $ t $ t', ct) =
val Free (x',_) = Thm.term_of cx';
val (Const (@{const_name Pure.all},_)$Abs (s,_,_)) = genEx |> Thm.prems_of |> hd |> dest_prop;
val genEx' = Drule.rename_bvars [(s,x)] genEx;
in if SplitState.isState (exc$Abs abst)
in if SplitState.isState ctxt (exc$Abs abst)
then ([Thm.term_of cb],[cb], fn [thm] =>
let val P = HOLogic.dest_Trueprop (dest_prop (prem_of thm));
val thm' = split_thm Hol_ex ctxt x' T P;
@ -229,7 +218,7 @@ fun decomp ctxt (Const (@{const_name HOL.conj}, _) $ t $ t', ct) =
val gen_all' = Drule.rename_bvars [(s,x)] gen_all;
val (Const (@{const_name Pure.all},_)$Abs (s',_,_)) = gen_allShift |> Thm.prems_of |> hd |> dest_prop;
val gen_allShift' = Drule.rename_bvars [(s',x)] gen_allShift;
in if SplitState.isState (allc$Abs abst)
in if SplitState.isState ctxt (allc$Abs abst)
then ([Thm.term_of cb],[cb], fn [thm] =>
let val P = dest_prop (prem_of thm);
val thm' = split_thm Meta_all ctxt x' T P;
@ -255,30 +244,26 @@ fun generalise ctxt ct = gen_thm (decomp ctxt) (Thm.term_of ct,ct);
*)
fun init ct = Thm.instantiate' [] [SOME ct] protectRefl;
fun generalise_over_tac ctxt P i st =
let
val t = List.nth (Thm.prems_of st, i - 1); (* FIXME !? *)
in (case P t of
SOME t' =>
let
val ct = Thm.cterm_of ctxt t';
val meta_spec_protect' = infer_instantiate ctxt [(("x", 0), ct)] @{thm meta_spec_protect};
in
(init (Thm.adjust_maxidx_cterm 0 (List.nth (Drule.cprems_of st, i - 1)))
|> resolve_tac ctxt [meta_spec_protect'] 1
|> Seq.maps (fn st' =>
Thm.bicompose NONE {flatten = true, match = false, incremented = false}
(false, Goal.conclude st', Thm.nprems_of st') i st))
end
| NONE => no_tac st)
end;
fun generalise_over_tac ctxt P = SUBGOAL (fn (t, i) => fn st =>
(case P t of
SOME t' =>
let
val ct = Thm.cterm_of ctxt t';
val meta_spec_protect' = infer_instantiate ctxt [(("x", 0), ct)] @{thm meta_spec_protect};
in
(init (Thm.adjust_maxidx_cterm 0 (List.nth (Drule.cprems_of st, i - 1)))
|> resolve_tac ctxt [meta_spec_protect'] 1
|> Seq.maps (fn st' =>
Thm.bicompose NONE {flatten = true, match = false, incremented = false}
(false, Goal.conclude st', Thm.nprems_of st') i st))
end
| NONE => no_tac st))
fun generalise_over_all_states_tac ctxt i =
REPEAT (generalise_over_tac ctxt SplitState.abs_state i);
REPEAT (generalise_over_tac ctxt (SplitState.abs_state ctxt) i);
fun generalise_tac ctxt i st =
fun generalise_tac ctxt = CSUBGOAL (fn (ct, i) => fn st =>
let
val ct = List.nth (Drule.cprems_of st, i - 1);
val ct' = Thm.dest_equals_rhs (Thm.cprop_of (Thm.eta_conversion ct));
val r = Goal.conclude (generalise ctxt ct');
in (init (Thm.adjust_maxidx_cterm 0 (List.nth (Drule.cprems_of st, i - 1)))
@ -286,7 +271,7 @@ fun generalise_tac ctxt i st =
|> Seq.maps (fn st' =>
Thm.bicompose NONE {flatten = true, match = false, incremented = false}
(false, Goal.conclude st', Thm.nprems_of st') i st))
end
end)
fun GENERALISE ctxt i =
generalise_over_all_states_tac ctxt i THEN

1012
tools/c-parser/Simpl/hoare.ML
View File

File diff suppressed because it is too large Load Diff

576
tools/c-parser/Simpl/hoare_syntax.ML
View File

File diff suppressed because it is too large Load Diff