1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory WP
8imports
9  WP_Pre
10  WPFix
11  Apply_Debug
12  MLUtils
13begin
14
15definition
16  triple_judgement :: "('a \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
17where
18 "triple_judgement pre body property = (\<forall>s. pre s \<longrightarrow> property s body)"
19
20definition
21  postcondition :: "('r \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> ('r \<times> 's) set)
22            \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
23where
24 "postcondition P f = (\<lambda>a b. \<forall>(rv, s) \<in> f a b. P rv s)"
25
26definition
27  postconditions :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool)"
28where
29 "postconditions P Q = (\<lambda>a b. P a b \<and> Q a b)"
30
31lemma conj_TrueI: "P \<Longrightarrow> True \<and> P" by simp
32lemma conj_TrueI2: "P \<Longrightarrow> P \<and> True" by simp
33
34ML_file "WP-method.ML"
35
36declare [[wp_trace = false, wp_trace_instantiation = false]]
37
38setup WeakestPre.setup
39
40method_setup wp = \<open>WeakestPre.apply_wp_args\<close>
41  "applies weakest precondition rules"
42
43end
44