forked from isabelle-utp/utp-main
-
Notifications
You must be signed in to change notification settings - Fork 0
/
utp_wp.thy
61 lines (42 loc) · 1.7 KB
/
utp_wp.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
section {* Weakest Precondition Calculus *}
theory utp_wp
imports utp_hoare
begin
text {* A very quick implementation of wp -- more laws still needed! *}
named_theorems wp
method wp_tac = (simp add: wp)
consts
uwp :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" (infix "wp" 60)
definition wp_upred :: "('\<alpha>, '\<beta>) urel \<Rightarrow> '\<beta> cond \<Rightarrow> '\<alpha> cond" where
"wp_upred Q r = \<lfloor>\<not> (Q ;; (\<not> \<lceil>r\<rceil>\<^sub><)) :: ('\<alpha>, '\<beta>) urel\<rfloor>\<^sub><"
adhoc_overloading
uwp wp_upred
declare wp_upred_def [urel_defs]
lemma wp_true [wp]: "p wp true = true"
by (rel_simp)
theorem wp_assigns_r [wp]:
"\<langle>\<sigma>\<rangle>\<^sub>a wp r = \<sigma> \<dagger> r"
by rel_auto
theorem wp_skip_r [wp]:
"II wp r = r"
by rel_auto
theorem wp_abort [wp]:
"r \<noteq> true \<Longrightarrow> true wp r = false"
by rel_auto
theorem wp_conj [wp]:
"P wp (q \<and> r) = (P wp q \<and> P wp r)"
by rel_auto
theorem wp_seq_r [wp]: "(P ;; Q) wp r = P wp (Q wp r)"
by rel_auto
theorem wp_cond [wp]: "(P \<triangleleft> b \<triangleright>\<^sub>r Q) wp r = ((b \<Rightarrow> P wp r) \<and> ((\<not> b) \<Rightarrow> Q wp r))"
by rel_auto
lemma wp_USUP_pre [wp]: "P wp (\<Squnion>i\<in>{0..n} \<bullet> Q(i)) = (\<Squnion>i\<in>{0..n} \<bullet> P wp Q(i))"
by (rel_auto)
theorem wp_hoare_link:
"\<lbrace>p\<rbrace>Q\<lbrace>r\<rbrace>\<^sub>u \<longleftrightarrow> (Q wp r \<sqsubseteq> p)"
by rel_auto
text {* If two programs have the same weakest precondition for any postcondition then the programs
are the same. *}
theorem wp_eq_intro: "\<lbrakk> \<And> r. P wp r = Q wp r \<rbrakk> \<Longrightarrow> P = Q"
by (rel_auto robust, fastforce+)
end