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